Thank you for reporting this.You are right with your understanding of the (intended) behavior of unoverload_type.
I guess all of my test cases involved type classes depending on "syntactic" type classes, that is why I did not notice this omission.
@Makarius: Could you please add the attached exported changeset to isabelle-release?
Otherwise I'll push the change to isabelle-dev. Best regards, Fabian On 5/13/2019 2:18 AM, mailing-list anonymous wrote:
Dear Fabian Immler/All,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.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):fun params_of_super_classes thy class =Sorts.super_classes (Sign.classes_of thy) class |> maps (params_of_class thy)| fun params_of_super_classes thy class =class :: Sorts.super_classes (Sign.classes_of thy) class |> maps (params_of_class thy)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).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.Thank you theory unoverload_type_test imports "HOL-Types_To_Sets.Prerequisites" "HOL-Types_To_Sets.Types_To_Sets" begin class ss_ord = fixes F :: "'a ⇒ nat" assumes Fx: "F x = 1" locale ss_ord_ow = fixes U and F' :: "'aq ⇒ nat" assumes Fx: "x ∈ U ⟹ F' x = 1" lemma ss_ord_transfer[transfer_rule]: includes lifting_syntax assumes[transfer_rule]: "right_total A" "bi_unique A" shows "((A ===> (=)) ===> (=)) (ss_ord_ow (Collect (Domainp A))) class.ss_ord" unfolding ss_ord_ow_def class.ss_ord_def apply transfer_prover_start apply transfer_step+ by simp lemma ss_ord: "class.ss_ord = ss_ord_ow UNIV" unfolding class.ss_ord_def ss_ord_ow_def by simp locale local_typedef_ss_ord_ow = local_typedef 𝔘 s + ss_ord_ow 𝔘 F for 𝔘 :: "'aq set" and F and s :: "'s itself" begin context includes lifting_syntax begin definition F_S :: "'s ⇒ nat" where "F_S = (rep ---> id) F" lemma F_S_transfer[transfer_rule]: "(cr_S ===> (=)) F F_S" apply(intro rel_funI) unfolding F_S_def cr_S_def by simp end sublocale type: ss_ord F_S by transfer (unfold Collect_mem_eq, rule ss_ord_ow_axioms) lemma type_ss_ord_ow: "ss_ord_ow UNIV F_S" proof - have "class.ss_ord F_S" by (rule type.ss_ord_axioms) thus ?thesis unfolding ss_ord by assumption qed end setup ‹Sign.add_const_constraint (\<^const_name>‹F›, SOME \<^typ>‹'a ⇒ nat›)› context ss_ord_ow begin context includes lifting_syntaxassumes ltd: "∃(Rep::'s ⇒ 'aq) (Abs::'aq ⇒ 's). type_definition Rep Abs U"begin interpretation lt: local_typedef_ss_ord_ow U F' "TYPE('s)" by unfold_locales fact (*works as expected*) lemmas_with[ unfolded ss_ord, internalize_sort "'a::ss_ord", unoverload "F :: 'a ⇒ nat", unfolded ss_ord, rule_format, OF lt.type_ss_ord_ow, untransferred ]: ut_error = ss_ord_class.Fx (*does not seem to work without the amendment to params_of_super_classes*) lemmas_with[ unfolded ss_ord, unoverload_type 'a, where 'a = 's, unfolded ss_ord, OF lt.type_ss_ord_ow, untransferred ]: ut_error = ss_ord_class.Fx end end end --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.
# HG changeset patch # User immler # Date 1557747599 -7200 # Mon May 13 13:39:59 2019 +0200 # Node ID e20071180875d1789d55226e967d660fa589d1ef # Parent ad0306b89cfb39e9f7790e8157a1931c0d732b31 amended to unoverload actually all parameters of a type variable diff -r ad0306b89cfb -r e20071180875 src/HOL/Types_To_Sets/unoverload_type.ML --- a/src/HOL/Types_To_Sets/unoverload_type.ML Sat May 11 15:53:11 2019 +0200 +++ b/src/HOL/Types_To_Sets/unoverload_type.ML Mon May 13 13:39:59 2019 +0200 @@ -16,7 +16,7 @@ fun params_of_class thy class = try (Axclass.get_info thy #> #params) class |> these fun params_of_super_classes thy class = - Sorts.super_classes (Sign.classes_of thy) class |> maps (params_of_class thy) + class::Sorts.super_classes (Sign.classes_of thy) class |> maps (params_of_class thy) fun params_of_sort thy sort = maps (params_of_super_classes thy) sort
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
