[isabelle] On the status of occurrences of variables with identical names/indexnames and different types in the same context/theorem/term



Dear All,

Recently, I encountered an issue which I find slightly difficult to
understand. I have already mentioned this issue on the mailing list, but
only as a side remark in a reply to another thread (
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2019-July/msg00060.html).
As far as I am concerned, the question in the aforementioned thread was
already answered in full and there is no reason to keep the thread alive.
Furthermore, I am slightly worried that most of the regular users who can
easily provide commentary on the remark would not have read it because of
where it was posted (to make matters even worse, I failed to present the
issue in the most comprehensive manner, for which I apologize). Therefore,
I hope it is appropriate to repost the issue as an explicit thread.

Effectively, the issue comes down to establishing the recommended practices
with regard to the use of different types for variables with identical
names/indexnames in a single context/theorem/term in Isabelle/HOL. The
problem is that, on one hand, there is much infrastructure in place to
prevent users from using different types for variables with identical
names/indexnames. Nevertheless, on the other hand, the logic does allow it
and it is not too difficult to introduce theorems (even accidentally) which
use different types for variables with the same name/indexname.

More specifically, I have the following questions, the second being of
certain practical significance:
1. Is introducing theorems that use differing types for variables with the
identical names/indexnames is considered to be a bad style, is it
completely illegal or, perhaps, it is actively exploited by user packages
that I am not aware of?
2. Is it acceptable for the user packages to assume that all variables in
the theorems that they receive as inputs from the users do not have any
occurrences of variables with the identical names/indexnames and different
types?

An example of a theorem that has occurrences of variables with the same
name, but different types:

locale myloc =
  fixes B :: "'b::plus"
  assumes "B ≡ B"
begin

ML ‹

fun mk_eq_thm' lthy =
let
  val T = TFree ("'b", ["HOL.type"])
  val ct = Free ("B", T) |> Thm.cterm_of lthy
  val thm = ct |> Thm.reflexive
  val thm = Thm.implies_intr
    (@{term True} |> HOLogic.mk_Trueprop |> Thm.cterm_of lthy)
    thm
  val lthy = Local_Theory.note ((@{binding mythm'}, []), single thm) lthy
    |> snd
in lthy end

›

local_setup ‹mk_eq_thm'›

definition C where "C = (B = B)"
lemma True_C: "C = True" unfolding C_def by auto

declare [[show_sorts]]
lemmas mythm'' = mythm'[folded True_C, unfolded C_def]
(* theorem mythm'': (B::'b::plus) = B ⟹ B::'b::type ≡ B *)

end

Thank you

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



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.