Email Gateway (Aug 22 2022 at 20:17): Email Gateway (Aug 22 2022 at 20:17):From: mailing-list anonymous <mailing.list.anonymous@gmail.com>
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:
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?
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
Email Gateway (Aug 22 2022 at 20:19):From: Lawrence Paulson <lp15@cam.ac.uk>
On 18 Jul 2019, at 00:11, mailing-list anonymous <mailing.list.anonymous@gmail.com> wrote:
More specifically, I have the following questions, the second being of
certain practical significance:
- 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?
I think it’s terrible style, and as your example shows, you have to work quite hard to accomplish this.
- 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?
I think so.
Larry
Email Gateway (Aug 22 2022 at 20:19):From: mailing-list anonymous <mailing.list.anonymous@gmail.com>
Dear Lawrence Paulson/All,
Thank you for your reply.
I believe that it would be useful to explain what you stated in your email
in the implementation manual. Of course, while it is difficult/impossible
to introduce new theorems that use variables with the same name and
different types using Isar commands only, it is very easy to do so via the
public ML interface, even by mistake. Unless I have missed something, this
issue does not seem to be covered at all (I believe that the manual merely
states that the type inference mechanism rejects such cases). Given that
using the variables with the same name and different types is considered to
be a 'terrible' style, it makes me wonder why the public ML interface
permits it at all... are there any use cases or any plans to exploit this
feature of the logic in the future?
Thank you
Email Gateway (Aug 22 2022 at 20:20):From: Lawrence Paulson <lp15@cam.ac.uk>
As a general rule, style is a matter of choice. This particular issue does not seem to arise frequently in practice. It is more common in the HOL world, but even there it doesn’t appear to be a source of controversy.
Larry Paulson
Last updated: Apr 27 2024 at 04:17 UTC