<div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div>Dear Fabian Immler/All,</div><div><br></div><div>I hope it is appropriate to post this issue on isabelle-dev: I do not want to flood the main discussion with obscure issues in auxiliary packages.</div><div><br></div><div>I cannot seem to understand why the function params_of_super_classes in HOL-Types_To_Sets/unoverload_type.ML does not include the class for which the parameters need to be obtained. This causes an issue whenever I try to unoverload a type, whose sort contains a parameter that belongs to it. This issue can be resolved with the following amendment (I cannot be certain if this amendment could cause other issues somewhere, but it seems unlikely):</div><div><div><br></div><div><div>fun params_of_super_classes thy class =</div><div>  Sorts.super_classes (Sign.classes_of thy) class |> maps (params_of_class thy)</div></div><div>       |</div><div>fun params_of_super_classes thy class =</div><div>  class :: Sorts.super_classes (Sign.classes_of thy) class |> maps (params_of_class thy)</div></div><div><br></div><div>It is my understanding that the attribute unoverload_type was defined as a substitute for the combination of attributes internalize_sort + unoverload. However, unlike unoverload_type, internalize_sort + unoverload can be used for classes with parameters that are defined within the class (see the example after my signature). </div><div><br></div><div>If the behaviour of unoverload_type is intended, I would like to understand why it is different from internalize_sort + unoverload. Otherwise, I would appreciate if this issue could be resolved before the next release of Isabelle.</div><div><br></div><div>Thank you</div><div><br></div><div dir="ltr">theory unoverload_type_test</div><div dir="ltr">  imports </div><div dir="ltr">    "HOL-Types_To_Sets.Prerequisites"</div><div dir="ltr">    "HOL-Types_To_Sets.Types_To_Sets"</div><div dir="ltr">begin</div><div dir="ltr"><br></div><div dir="ltr">class ss_ord = </div><div dir="ltr">  fixes F :: "'a ⇒ nat"</div><div dir="ltr">  assumes Fx: "F x = 1"</div><div dir="ltr"><br></div><div dir="ltr">locale ss_ord_ow =</div><div dir="ltr">  fixes U and F' :: "'aq ⇒ nat"</div><div dir="ltr">  assumes Fx: "x ∈ U ⟹ F' x = 1"</div><div dir="ltr"><br></div><div dir="ltr">lemma ss_ord_transfer[transfer_rule]:</div><div dir="ltr">  includes lifting_syntax</div><div dir="ltr">  assumes[transfer_rule]: "right_total A" "bi_unique A" </div><div dir="ltr">  shows </div><div dir="ltr">    "((A ===> (=)) ===> (=)) </div><div dir="ltr">    (ss_ord_ow (Collect (Domainp A))) class.ss_ord"</div><div dir="ltr">  unfolding ss_ord_ow_def class.ss_ord_def</div><div dir="ltr">  apply transfer_prover_start</div><div dir="ltr">  apply transfer_step+  </div><div dir="ltr">  by simp</div><div dir="ltr"><br></div><div dir="ltr">lemma ss_ord: "class.ss_ord = ss_ord_ow UNIV"</div><div dir="ltr">  unfolding class.ss_ord_def ss_ord_ow_def by simp</div><div dir="ltr"><br></div><div dir="ltr">locale local_typedef_ss_ord_ow = </div><div dir="ltr">  local_typedef 𝔘 s + ss_ord_ow 𝔘 F </div><div dir="ltr">  for 𝔘 :: "'aq set" and F and s :: "'s itself" </div><div dir="ltr">begin</div><div dir="ltr"><br></div><div dir="ltr">context </div><div dir="ltr">  includes lifting_syntax </div><div dir="ltr">begin</div><div dir="ltr"><br></div><div dir="ltr">definition F_S :: "'s ⇒ nat" where "F_S = (rep ---> id) F"</div><div dir="ltr"><br></div><div dir="ltr">lemma F_S_transfer[transfer_rule]: </div><div dir="ltr">  "(cr_S ===> (=)) F F_S"</div><div dir="ltr">  apply(intro rel_funI) unfolding F_S_def cr_S_def by simp</div><div dir="ltr">  </div><div dir="ltr">end</div><div dir="ltr"><br></div><div dir="ltr">sublocale type: ss_ord F_S </div><div dir="ltr">  by transfer (unfold Collect_mem_eq, rule ss_ord_ow_axioms)</div><div dir="ltr"><br></div><div dir="ltr">lemma type_ss_ord_ow: "ss_ord_ow UNIV F_S"</div><div dir="ltr">proof -</div><div dir="ltr">  have "class.ss_ord F_S" by (rule type.ss_ord_axioms)</div><div dir="ltr">  thus ?thesis unfolding ss_ord by assumption</div><div dir="ltr">qed</div><div dir="ltr"><br></div><div dir="ltr">end</div><div dir="ltr"><br></div><div dir="ltr">setup ‹Sign.add_const_constraint</div><div dir="ltr">  (\<^const_name>‹F›, SOME \<^typ>‹'a ⇒ nat›)›</div><div dir="ltr"><br></div><div dir="ltr">context ss_ord_ow</div><div dir="ltr">begin</div><div dir="ltr"><br></div><div dir="ltr">context </div><div dir="ltr">  includes lifting_syntax </div><div dir="ltr">  assumes ltd: "∃(Rep::'s ⇒ 'aq) (Abs::'aq ⇒ 's). type_definition Rep Abs U" </div><div dir="ltr">begin</div><div dir="ltr"><br></div><div dir="ltr">interpretation lt: local_typedef_ss_ord_ow U F' "TYPE('s)" </div><div dir="ltr">  by unfold_locales fact</div><div dir="ltr"><br></div><div dir="ltr">(*works as expected*)</div><div dir="ltr">lemmas_with[</div><div dir="ltr">    unfolded ss_ord,</div><div dir="ltr">    internalize_sort "'a::ss_ord",</div><div dir="ltr">    unoverload "F :: 'a ⇒ nat",</div><div dir="ltr">    unfolded ss_ord,</div><div dir="ltr">    rule_format,</div><div dir="ltr">    OF lt.type_ss_ord_ow,</div><div dir="ltr">    untransferred</div><div dir="ltr">    ]:</div><div dir="ltr">  ut_error = ss_ord_class.Fx</div><div dir="ltr"><br></div><div dir="ltr">(*does not seem to work without the amendment to params_of_super_classes*)</div><div dir="ltr">lemmas_with[</div><div dir="ltr">    unfolded ss_ord,</div><div dir="ltr">    unoverload_type 'a,</div><div dir="ltr">    where 'a = 's,</div><div dir="ltr">    unfolded ss_ord,</div><div dir="ltr">    OF lt.type_ss_ord_ow,</div><div dir="ltr">    untransferred</div><div dir="ltr">    ]:</div><div dir="ltr">  ut_error = ss_ord_class.Fx</div><div dir="ltr"><br></div><div dir="ltr">end</div><div dir="ltr"><br></div><div dir="ltr">end</div><div dir="ltr"><br></div><div dir="ltr">end</div><div><br></div><div><br></div>-- <br><div dir="ltr" class="gmail_signature"><div dir="ltr">Please accept my apologies for posting anonymously. This is done to protect my privacy. I can make my identity and my real contact details available upon request in private communication under the condition that they are not to be mentioned on the mailing list.  </div></div></div></div></div></div></div>