Email Gateway (Aug 18 2022 at 11:49): Email Gateway (Aug 18 2022 at 11:49):From: Clemens Ballarin <ballarin@in.tum.de>
Hi Michael,
The current implementation is incomplete. The syntax introduced by
the definition is not available while M2 is read. You need to use
the global constant, applied to the parameters, instead. That is:
locale M2 = L + assumes "L.c1 c0 x = 3"
The tutorial on locale interpretation (http://cl-
informatik.uibk.ac.at/users/clemens/publications/TUM-I0723.pdf)
elaborates on this issue.
Clemens
Email Gateway (Aug 18 2022 at 11:56):From: Michael Norrish <Michael.Norrish@nicta.com.au>
The following theory file presents a number of strange behaviours that
I don't understand. In particular, just about every time I have
written "doesn't work", I expected it to work. Are these bugs, or are
my intuitions completely broken?
(This is the 2008-04-07 version.)
Any help much appreciated.
Michael.
theory Scratch
imports Main
begin
locale L =
fixes c0 :: "'a => 'a"
begin
definition "c1 x = c0 (c0 x)"
end
(* works - makes L's alpha be nat*)
locale M1 = L +
assumes "c0 x = Suc 3"
ML "set show_types"
thm M1_def
(* Doesn't work *)
(* locale M2 = L + assumes "c1 x = 3" *)
(* Doesn't work either *)
(* locale M3 = L + assumes "L.c1 x = 3" *)
(* Works *)
locale N1 = M1 + assumes "c0 x = x"
thm N1_def
thm N1_axioms_def
(* Doesn't work *)
(* locale N2 = M1 + assumes "ALL x. L.c1 x = x" *)
(* Doesn't work properly - makes c1 a variable.
Also creates something in the N2 locale called c0.N2_axioms,
which is a pretty weird choice of name.
*)
locale N3 = L + assumes "c1 x = x"
print_locale N3
thm N3_def
(* works, but if this works, why doesn't N2 work? *)
locale N4 = L + assumes "L.c1 x = x"
end
Last updated: May 03 2024 at 08:18 UTC