[isabelle] strange locale behaviours in presence of local definitions



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





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