[isabelle-dev] Minor issue in HOL-Types_To_Sets/unoverload_type.ML

[Fabian Immler]

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_syntax
>    assumes 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.
-------------- next part --------------
# 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
 
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5581 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20190513/fffbf86a/attachment.bin>