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

[mailing-list anonymous]

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 --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20190513/8714b28a/attachment.html>