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

mailing-list anonymous mailing.list.anonymous at gmail.com
Mon May 13 02:18:00 CEST 2019

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
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

Thank you

theory unoverload_type_test

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"
    "((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"

  includes lifting_syntax

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


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


setup โ€นSign.add_const_constraint
  (\<^const_name>โ€นFโ€บ, SOME \<^typ>โ€น'a โ‡’ natโ€บ)โ€บ

context ss_ord_ow

  includes lifting_syntax
  assumes ltd: "โˆƒ(Rep::'s โ‡’ 'aq) (Abs::'aq โ‡’ 's). type_definition Rep Abs

interpretation lt: local_typedef_ss_ord_ow U F' "TYPE('s)"
  by unfold_locales fact

(*works as expected*)
    unfolded ss_ord,
    internalize_sort "'a::ss_ord",
    unoverload "F :: 'a โ‡’ nat",
    unfolded ss_ord,
    OF lt.type_ss_ord_ow,
  ut_error = ss_ord_class.Fx

(*does not seem to work without the amendment to params_of_super_classes*)
    unfolded ss_ord,
    unoverload_type 'a,
    where 'a = 's,
    unfolded ss_ord,
    OF lt.type_ss_ord_ow,
  ut_error = ss_ord_class.Fx




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>

More information about the isabelle-dev mailing list