All logics ported to new locales.
authorballarin
Fri Dec 19 16:39:23 2008 +0100 (2008-12-19)
changeset 292494dc278c8dc59
parent 29248 f1f1bccf2fc5
child 29250 96b1b4d5157d
All logics ported to new locales.
src/FOL/IsaMakefile
src/FOL/ex/LocaleTest.thy
src/FOL/ex/NewLocaleTest.thy
src/FOL/ex/ROOT.ML
src/HOL/ROOT.ML
src/HOL/main.ML
src/HOL/plain.ML
src/Pure/Isar/ROOT.ML
src/Pure/Isar/specification.ML
src/Pure/Isar/theory_target.ML
src/ZF/ROOT.ML
     1.1 --- a/src/FOL/IsaMakefile	Fri Dec 19 15:05:37 2008 +0100
     1.2 +++ b/src/FOL/IsaMakefile	Fri Dec 19 16:39:23 2008 +0100
     1.3 @@ -46,7 +46,7 @@
     1.4  FOL-ex: FOL $(LOG)/FOL-ex.gz
     1.5  
     1.6  $(LOG)/FOL-ex.gz: $(OUT)/FOL ex/First_Order_Logic.thy ex/If.thy		\
     1.7 -  ex/IffOracle.thy ex/LocaleTest.thy ex/Nat.thy ex/Natural_Numbers.thy	\
     1.8 +  ex/IffOracle.thy ex/Nat.thy ex/Natural_Numbers.thy	\
     1.9    ex/NewLocaleSetup.thy ex/NewLocaleTest.thy    \
    1.10    ex/Miniscope.thy ex/Prolog.thy ex/ROOT.ML ex/Classical.thy		\
    1.11    ex/document/root.tex ex/Foundation.thy ex/Intuitionistic.thy		\
     2.1 --- a/src/FOL/ex/LocaleTest.thy	Fri Dec 19 15:05:37 2008 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,765 +0,0 @@
     2.4 -(*  Title:      FOL/ex/LocaleTest.thy
     2.5 -    ID:         $Id$
     2.6 -    Author:     Clemens Ballarin
     2.7 -    Copyright (c) 2005 by Clemens Ballarin
     2.8 -
     2.9 -Collection of regression tests for locales.
    2.10 -*)
    2.11 -
    2.12 -header {* Test of Locale Interpretation *}
    2.13 -
    2.14 -theory LocaleTest
    2.15 -imports FOL
    2.16 -begin
    2.17 -
    2.18 -ML {* set Toplevel.debug *}
    2.19 -ML {* set show_hyps *}
    2.20 -ML {* set show_sorts *}
    2.21 -
    2.22 -ML {*
    2.23 -  fun check_thm name = let
    2.24 -    val thy = the_context ();
    2.25 -    val thm = PureThy.get_thm thy name;
    2.26 -    val {prop, hyps, ...} = rep_thm thm;
    2.27 -    val prems = Logic.strip_imp_prems prop;
    2.28 -    val _ = if null hyps then ()
    2.29 -        else error ("Theorem " ^ quote name ^ " has meta hyps.\n" ^
    2.30 -          "Consistency check of locales package failed.");
    2.31 -    val _ = if null prems then ()
    2.32 -        else error ("Theorem " ^ quote name ^ " has premises.\n" ^
    2.33 -          "Consistency check of locales package failed.");
    2.34 -  in () end;
    2.35 -*}
    2.36 -
    2.37 -section {* Context Elements and Locale Expressions *}
    2.38 -
    2.39 -text {* Naming convention for global objects: prefixes L and l *}
    2.40 -
    2.41 -subsection {* Renaming with Syntax *}
    2.42 -
    2.43 -locale LS = var mult +
    2.44 -  assumes "mult(x, y) = mult(y, x)"
    2.45 -
    2.46 -print_locale LS
    2.47 -
    2.48 -locale LS' = LS mult (infixl "**" 60)
    2.49 -
    2.50 -print_locale LS'
    2.51 -
    2.52 -locale LT = var mult (infixl "**" 60) +
    2.53 -  assumes "x ** y = y ** x"
    2.54 -
    2.55 -locale LU = LT mult (infixl "**" 60) + LT add (infixl "++" 55) + var h +
    2.56 -  assumes hom: "h(x ** y) = h(x) ++ h(y)"
    2.57 -
    2.58 -
    2.59 -(* FIXME: graceful handling of type errors?
    2.60 -locale LY = LT mult (infixl "**" 60) + LT add (binder "++" 55) + var h +
    2.61 -  assumes "mult(x) == add"
    2.62 -*)
    2.63 -
    2.64 -
    2.65 -locale LV = LU _ add
    2.66 -
    2.67 -locale LW = LU _ mult (infixl "**" 60)
    2.68 -
    2.69 -
    2.70 -subsection {* Constrains *}
    2.71 -
    2.72 -locale LZ = fixes a (structure)
    2.73 -locale LZ' = LZ +
    2.74 -  constrains a :: "'a => 'b"
    2.75 -  assumes "a (x :: 'a) = a (y)"
    2.76 -print_locale LZ'
    2.77 -
    2.78 -
    2.79 -section {* Interpretation *}
    2.80 -
    2.81 -text {* Naming convention for global objects: prefixes I and i *}
    2.82 -
    2.83 -text {* interpretation input syntax *}
    2.84 -
    2.85 -locale IL
    2.86 -locale IM = fixes a and b and c
    2.87 -
    2.88 -interpretation test: IL + IM a b c [x y z] .
    2.89 -
    2.90 -print_interps IL    (* output: test *)
    2.91 -print_interps IM    (* output: test *)
    2.92 -
    2.93 -interpretation test: IL print_interps IM .
    2.94 -
    2.95 -interpretation IL .
    2.96 -
    2.97 -text {* Processing of locale expression *}
    2.98 -
    2.99 -locale IA = fixes a assumes asm_A: "a = a"
   2.100 -
   2.101 -locale IB = fixes b assumes asm_B [simp]: "b = b"
   2.102 -
   2.103 -locale IC = IA + IB + assumes asm_C: "b = b"
   2.104 -
   2.105 -locale IC' = IA + IB + assumes asm_C: "c = c"
   2.106 -  (* independent type var in c *)
   2.107 -
   2.108 -locale ID = IA + IB + fixes d defines def_D: "d == (a = b)"
   2.109 -
   2.110 -theorem (in ID) True ..
   2.111 -
   2.112 -typedecl i
   2.113 -arities i :: "term"
   2.114 -
   2.115 -
   2.116 -interpretation i1: IC ["X::i" "Y::i"] by unfold_locales auto
   2.117 -
   2.118 -print_interps IA  (* output: i1 *)
   2.119 -
   2.120 -(* possible accesses *)
   2.121 -thm i1.a.asm_A thm LocaleTest.IA_locale.i1.a.asm_A thm IA_locale.i1.a.asm_A
   2.122 -thm i1.asm_A thm LocaleTest.i1.asm_A
   2.123 -
   2.124 -ML {* check_thm "i1.a.asm_A" *}
   2.125 -
   2.126 -(* without prefix *)
   2.127 -
   2.128 -interpretation IC ["W::i" "Z::i"] by intro_locales  (* subsumed by i1: IC *)
   2.129 -interpretation IC ["W::'a" "Z::i"] by unfold_locales auto
   2.130 -  (* subsumes i1: IA and i1: IC *)
   2.131 -
   2.132 -print_interps IA  (* output: <no prefix>, i1 *)
   2.133 -
   2.134 -(* possible accesses *)
   2.135 -thm asm_C thm a_b.asm_C thm LocaleTest.IC_locale.a_b.asm_C thm IC_locale.a_b.asm_C
   2.136 -
   2.137 -ML {* check_thm "asm_C" *}
   2.138 -
   2.139 -interpretation i2: ID [X "Y::i" "Y = X"]
   2.140 -  by (simp add: eq_commute) unfold_locales
   2.141 -
   2.142 -print_interps IA  (* output: <no prefix>, i1 *)
   2.143 -print_interps ID  (* output: i2 *)
   2.144 -
   2.145 -
   2.146 -interpretation i3: ID [X "Y::i"] by simp unfold_locales
   2.147 -
   2.148 -(* duplicate: thm not added *)
   2.149 -
   2.150 -(* thm i3.a.asm_A *)
   2.151 -
   2.152 -
   2.153 -print_interps IA  (* output: <no prefix>, i1 *)
   2.154 -print_interps IB  (* output: i1 *)
   2.155 -print_interps IC  (* output: <no prefix, i1 *)
   2.156 -print_interps ID  (* output: i2, i3 *)
   2.157 -
   2.158 -
   2.159 -interpretation i10: ID + ID a' b' d' [X "Y::i" _ u "v::i" _] by intro_locales
   2.160 -
   2.161 -corollary (in ID) th_x: True ..
   2.162 -
   2.163 -(* possible accesses: for each registration *)
   2.164 -
   2.165 -thm i2.th_x thm i3.th_x
   2.166 -
   2.167 -ML {* check_thm "i2.th_x"; check_thm "i3.th_x" *}
   2.168 -
   2.169 -lemma (in ID) th_y: "d == (a = b)" by (rule d_def)
   2.170 -
   2.171 -thm i2.th_y thm i3.th_y
   2.172 -
   2.173 -ML {* check_thm "i2.th_y"; check_thm "i3.th_y" *}
   2.174 -
   2.175 -lemmas (in ID) th_z = th_y
   2.176 -
   2.177 -thm i2.th_z
   2.178 -
   2.179 -ML {* check_thm "i2.th_z" *}
   2.180 -
   2.181 -
   2.182 -subsection {* Interpretation in Proof Contexts *}
   2.183 -
   2.184 -locale IF = fixes f assumes asm_F: "f & f --> f"
   2.185 -
   2.186 -consts default :: "'a"
   2.187 -
   2.188 -theorem True
   2.189 -proof -
   2.190 -  fix alpha::i and beta
   2.191 -  have alpha_A: "IA(alpha)" by unfold_locales
   2.192 -  interpret i5: IA [alpha] by intro_locales  (* subsumed *)
   2.193 -  print_interps IA  (* output: <no prefix>, i1 *)
   2.194 -  interpret i6: IC [alpha beta] by unfold_locales auto
   2.195 -  print_interps IA   (* output: <no prefix>, i1 *)
   2.196 -  print_interps IC   (* output: <no prefix>, i1, i6 *)
   2.197 -  interpret i11: IF ["default = default"] by (fast intro: IF.intro)
   2.198 -  thm i11.asm_F [where 'a = i]     (* default has schematic type *)
   2.199 -qed rule
   2.200 -
   2.201 -theorem (in IA) True
   2.202 -proof -
   2.203 -  print_interps! IA
   2.204 -  fix beta and gamma
   2.205 -  interpret i9: ID [a beta _]
   2.206 -    apply - apply assumption
   2.207 -    apply unfold_locales
   2.208 -    apply (rule refl) done
   2.209 -qed rule
   2.210 -
   2.211 -
   2.212 -(* Definition involving free variable *)
   2.213 -
   2.214 -ML {* reset show_sorts *}
   2.215 -
   2.216 -locale IE = fixes e defines e_def: "e(x) == x & x"
   2.217 -  notes e_def2 = e_def
   2.218 -
   2.219 -lemma (in IE) True thm e_def by fast
   2.220 -
   2.221 -interpretation i7: IE ["%x. x"] by simp
   2.222 -
   2.223 -thm i7.e_def2 (* has no premise *)
   2.224 -
   2.225 -ML {* check_thm "i7.e_def2" *}
   2.226 -
   2.227 -locale IE' = fixes e defines e_def: "e == (%x. x & x)"
   2.228 -  notes e_def2 = e_def
   2.229 -
   2.230 -interpretation i7': IE' ["(%x. x)"] by simp
   2.231 -
   2.232 -thm i7'.e_def2
   2.233 -
   2.234 -ML {* check_thm "i7'.e_def2" *}
   2.235 -
   2.236 -(* Definition involving free variable in assm *)
   2.237 -
   2.238 -locale IG = fixes g assumes asm_G: "g --> x"
   2.239 -  notes asm_G2 = asm_G
   2.240 -
   2.241 -interpretation i8: IG ["False"] by unfold_locales fast
   2.242 -
   2.243 -thm i8.asm_G2
   2.244 -
   2.245 -ML {* check_thm "i8.asm_G2" *}
   2.246 -
   2.247 -text {* Locale without assumptions *}
   2.248 -
   2.249 -locale IL1 = notes rev_conjI [intro] = conjI [THEN iffD1 [OF conj_commute]]
   2.250 -
   2.251 -lemma "[| P; Q |] ==> P & Q"
   2.252 -proof -
   2.253 -  interpret my: IL1 .          txt {* No chained fact required. *}
   2.254 -  assume Q and P               txt {* order reversed *}
   2.255 -  then show "P & Q" ..         txt {* Applies @{thm my.rev_conjI}. *}
   2.256 -qed
   2.257 -
   2.258 -locale IL11 = notes rev_conjI = conjI [THEN iffD1 [OF conj_commute]]
   2.259 -
   2.260 -
   2.261 -subsection {* Simple locale with assumptions *}
   2.262 -
   2.263 -consts ibin :: "[i, i] => i" (infixl "#" 60)
   2.264 -
   2.265 -axioms i_assoc: "(x # y) # z = x # (y # z)"
   2.266 -  i_comm: "x # y = y # x"
   2.267 -
   2.268 -locale IL2 =
   2.269 -  fixes OP (infixl "+" 60)
   2.270 -  assumes assoc: "(x + y) + z = x + (y + z)"
   2.271 -    and comm: "x + y = y + x"
   2.272 -
   2.273 -lemma (in IL2) lcomm: "x + (y + z) = y + (x + z)"
   2.274 -proof -
   2.275 -  have "x + (y + z) = (x + y) + z" by (simp add: assoc)
   2.276 -  also have "... = (y + x) + z" by (simp add: comm)
   2.277 -  also have "... = y + (x + z)" by (simp add: assoc)
   2.278 -  finally show ?thesis .
   2.279 -qed
   2.280 -
   2.281 -lemmas (in IL2) AC = comm assoc lcomm
   2.282 -
   2.283 -lemma "(x::i) # y # z # w = y # x # w # z"
   2.284 -proof -
   2.285 -  interpret my: IL2 ["op #"] by (rule IL2.intro [of "op #", OF i_assoc i_comm])
   2.286 -  show ?thesis by (simp only: my.OP.AC)  (* or my.AC *)
   2.287 -qed
   2.288 -
   2.289 -subsection {* Nested locale with assumptions *}
   2.290 -
   2.291 -locale IL3 =
   2.292 -  fixes OP (infixl "+" 60)
   2.293 -  assumes assoc: "(x + y) + z = x + (y + z)"
   2.294 -
   2.295 -locale IL4 = IL3 +
   2.296 -  assumes comm: "x + y = y + x"
   2.297 -
   2.298 -lemma (in IL4) lcomm: "x + (y + z) = y + (x + z)"
   2.299 -proof -
   2.300 -  have "x + (y + z) = (x + y) + z" by (simp add: assoc)
   2.301 -  also have "... = (y + x) + z" by (simp add: comm)
   2.302 -  also have "... = y + (x + z)" by (simp add: assoc)
   2.303 -  finally show ?thesis .
   2.304 -qed
   2.305 -
   2.306 -lemmas (in IL4) AC = comm assoc lcomm
   2.307 -
   2.308 -lemma "(x::i) # y # z # w = y # x # w # z"
   2.309 -proof -
   2.310 -  interpret my: IL4 ["op #"]
   2.311 -    by (auto intro: IL4.intro IL3.intro IL4_axioms.intro i_assoc i_comm)
   2.312 -  show ?thesis by (simp only: my.OP.AC)  (* or simply AC *)
   2.313 -qed
   2.314 -
   2.315 -text {* Locale with definition *}
   2.316 -
   2.317 -text {* This example is admittedly not very creative :-) *}
   2.318 -
   2.319 -locale IL5 = IL4 + var A +
   2.320 -  defines A_def: "A == True"
   2.321 -
   2.322 -lemma (in IL5) lem: A
   2.323 -  by (unfold A_def) rule
   2.324 -
   2.325 -lemma "IL5(op #) ==> True"
   2.326 -proof -
   2.327 -  assume "IL5(op #)"
   2.328 -  then interpret IL5 ["op #"] by (auto intro: IL5.axioms)
   2.329 -  show ?thesis by (rule lem)  (* lem instantiated to True *)
   2.330 -qed
   2.331 -
   2.332 -text {* Interpretation in a context with target *}
   2.333 -
   2.334 -lemma (in IL4)
   2.335 -  fixes A (infixl "$" 60)
   2.336 -  assumes A: "IL4(A)"
   2.337 -  shows "(x::i) $ y $ z $ w = y $ x $ w $ z"
   2.338 -proof -
   2.339 -  from A interpret A: IL4 ["A"] by (auto intro: IL4.axioms)
   2.340 -  show ?thesis by (simp only: A.OP.AC)
   2.341 -qed
   2.342 -
   2.343 -
   2.344 -section {* Interpretation in Locales *}
   2.345 -
   2.346 -text {* Naming convention for global objects: prefixes R and r *}
   2.347 -
   2.348 -(* locale with many parameters ---
   2.349 -   interpretations generate alternating group A5 *)
   2.350 -
   2.351 -locale RA5 = var A + var B + var C + var D + var E +
   2.352 -  assumes eq: "A <-> B <-> C <-> D <-> E"
   2.353 -
   2.354 -interpretation RA5 < RA5 _ _ D E C
   2.355 -print_facts
   2.356 -print_interps RA5
   2.357 -  using A_B_C_D_E.eq apply (blast intro: RA5.intro) done
   2.358 -
   2.359 -interpretation RA5 < RA5 C _ E _ A
   2.360 -print_facts
   2.361 -print_interps RA5
   2.362 -  using A_B_C_D_E.eq apply (blast intro: RA5.intro) done
   2.363 -
   2.364 -interpretation RA5 < RA5 B C A _ _
   2.365 -print_facts
   2.366 -print_interps RA5
   2.367 -  using A_B_C_D_E.eq apply (blast intro: RA5.intro) done
   2.368 -
   2.369 -interpretation RA5 < RA5 _ C D B _ .
   2.370 -  (* Any even permutation of parameters is subsumed by the above. *)
   2.371 -
   2.372 -(* circle of three locales, forward direction *)
   2.373 -
   2.374 -locale RA1 = var A + var B + assumes p: "A <-> B"
   2.375 -locale RA2 = var A + var B + assumes q: "A & B | ~ A & ~ B"
   2.376 -locale RA3 = var A + var B + assumes r: "(A --> B) & (B --> A)"
   2.377 -
   2.378 -interpretation RA1 < RA2
   2.379 -  print_facts
   2.380 -  using p apply unfold_locales apply fast done
   2.381 -interpretation RA2 < RA3
   2.382 -  print_facts
   2.383 -  using q apply unfold_locales apply fast done
   2.384 -interpretation RA3 < RA1
   2.385 -  print_facts
   2.386 -  using r apply unfold_locales apply fast done
   2.387 -
   2.388 -(* circle of three locales, backward direction *)
   2.389 -
   2.390 -locale RB1 = var A + var B + assumes p: "A <-> B"
   2.391 -locale RB2 = var A + var B + assumes q: "A & B | ~ A & ~ B"
   2.392 -locale RB3 = var A + var B + assumes r: "(A --> B) & (B --> A)"
   2.393 -
   2.394 -interpretation RB1 < RB2
   2.395 -  print_facts
   2.396 -  using p apply unfold_locales apply fast done
   2.397 -interpretation RB3 < RB1
   2.398 -  print_facts
   2.399 -  using r apply unfold_locales apply fast done
   2.400 -interpretation RB2 < RB3
   2.401 -  print_facts
   2.402 -  using q apply unfold_locales apply fast done
   2.403 -
   2.404 -lemma (in RB1) True
   2.405 -  print_facts
   2.406 -  ..
   2.407 -
   2.408 -
   2.409 -(* Group example *)
   2.410 -
   2.411 -locale Rsemi = var prod (infixl "**" 65) +
   2.412 -  assumes assoc: "(x ** y) ** z = x ** (y ** z)"
   2.413 -
   2.414 -locale Rlgrp = Rsemi + var one + var inv +
   2.415 -  assumes lone: "one ** x = x"
   2.416 -    and linv: "inv(x) ** x = one"
   2.417 -
   2.418 -lemma (in Rlgrp) lcancel:
   2.419 -  "x ** y = x ** z <-> y = z"
   2.420 -proof
   2.421 -  assume "x ** y = x ** z"
   2.422 -  then have "inv(x) ** x ** y = inv(x) ** x ** z" by (simp add: assoc)
   2.423 -  then show "y = z" by (simp add: lone linv)
   2.424 -qed simp
   2.425 -
   2.426 -locale Rrgrp = Rsemi + var one + var inv +
   2.427 -  assumes rone: "x ** one = x"
   2.428 -    and rinv: "x ** inv(x) = one"
   2.429 -
   2.430 -lemma (in Rrgrp) rcancel:
   2.431 -  "y ** x = z ** x <-> y = z"
   2.432 -proof
   2.433 -  assume "y ** x = z ** x"
   2.434 -  then have "y ** (x ** inv(x)) = z ** (x ** inv(x))"
   2.435 -    by (simp add: assoc [symmetric])
   2.436 -  then show "y = z" by (simp add: rone rinv)
   2.437 -qed simp
   2.438 -
   2.439 -interpretation Rlgrp < Rrgrp
   2.440 -  proof unfold_locales
   2.441 -    {
   2.442 -      fix x
   2.443 -      have "inv(x) ** x ** one = inv(x) ** x" by (simp add: linv lone)
   2.444 -      then show "x ** one = x" by (simp add: assoc lcancel)
   2.445 -    }
   2.446 -    note rone = this
   2.447 -    {
   2.448 -      fix x
   2.449 -      have "inv(x) ** x ** inv(x) = inv(x) ** one"
   2.450 -	by (simp add: linv lone rone)
   2.451 -      then show "x ** inv(x) = one" by (simp add: assoc lcancel)
   2.452 -    }
   2.453 -  qed
   2.454 -
   2.455 -(* effect on printed locale *)
   2.456 -
   2.457 -print_locale! Rlgrp
   2.458 -
   2.459 -(* use of derived theorem *)
   2.460 -
   2.461 -lemma (in Rlgrp)
   2.462 -  "y ** x = z ** x <-> y = z"
   2.463 -  apply (rule rcancel)
   2.464 -  print_interps Rrgrp thm lcancel rcancel
   2.465 -  done
   2.466 -
   2.467 -(* circular interpretation *)
   2.468 -
   2.469 -interpretation Rrgrp < Rlgrp
   2.470 -  proof unfold_locales
   2.471 -    {
   2.472 -      fix x
   2.473 -      have "one ** (x ** inv(x)) = x ** inv(x)" by (simp add: rinv rone)
   2.474 -      then show "one ** x = x" by (simp add: assoc [symmetric] rcancel)
   2.475 -    }
   2.476 -    note lone = this
   2.477 -    {
   2.478 -      fix x
   2.479 -      have "inv(x) ** (x ** inv(x)) = one ** inv(x)"
   2.480 -	by (simp add: rinv lone rone)
   2.481 -      then show "inv(x) ** x = one" by (simp add: assoc [symmetric] rcancel)
   2.482 -    }
   2.483 -  qed
   2.484 -
   2.485 -(* effect on printed locale *)
   2.486 -
   2.487 -print_locale! Rrgrp
   2.488 -print_locale! Rlgrp
   2.489 -
   2.490 -subsection {* Interaction of Interpretation in Theories and Locales:
   2.491 -  in Locale, then in Theory *}
   2.492 -
   2.493 -consts
   2.494 -  rone :: i
   2.495 -  rinv :: "i => i"
   2.496 -
   2.497 -axioms
   2.498 -  r_one : "rone # x = x"
   2.499 -  r_inv : "rinv(x) # x = rone"
   2.500 -
   2.501 -interpretation Rbool: Rlgrp ["op #" "rone" "rinv"]
   2.502 -proof
   2.503 -  fix x y z
   2.504 -  {
   2.505 -    show "(x # y) # z = x # (y # z)" by (rule i_assoc)
   2.506 -  next
   2.507 -    show "rone # x = x" by (rule r_one)
   2.508 -  next
   2.509 -    show "rinv(x) # x = rone" by (rule r_inv)
   2.510 -  }
   2.511 -qed
   2.512 -
   2.513 -(* derived elements *)
   2.514 -
   2.515 -print_interps Rrgrp
   2.516 -print_interps Rlgrp
   2.517 -
   2.518 -lemma "y # x = z # x <-> y = z" by (rule Rbool.rcancel)
   2.519 -
   2.520 -(* adding lemma to derived element *)
   2.521 -
   2.522 -lemma (in Rrgrp) new_cancel:
   2.523 -  "b ** a = c ** a <-> b = c"
   2.524 -  by (rule rcancel)
   2.525 -
   2.526 -thm Rbool.new_cancel (* additional prems discharged!! *)
   2.527 -
   2.528 -ML {* check_thm "Rbool.new_cancel" *}
   2.529 -
   2.530 -lemma "b # a = c # a <-> b = c" by (rule Rbool.new_cancel)
   2.531 -
   2.532 -
   2.533 -subsection {* Interaction of Interpretation in Theories and Locales:
   2.534 -  in Theory, then in Locale *}
   2.535 -
   2.536 -(* Another copy of the group example *)
   2.537 -
   2.538 -locale Rqsemi = var prod (infixl "**" 65) +
   2.539 -  assumes assoc: "(x ** y) ** z = x ** (y ** z)"
   2.540 -
   2.541 -locale Rqlgrp = Rqsemi + var one + var inv +
   2.542 -  assumes lone: "one ** x = x"
   2.543 -    and linv: "inv(x) ** x = one"
   2.544 -
   2.545 -lemma (in Rqlgrp) lcancel:
   2.546 -  "x ** y = x ** z <-> y = z"
   2.547 -proof
   2.548 -  assume "x ** y = x ** z"
   2.549 -  then have "inv(x) ** x ** y = inv(x) ** x ** z" by (simp add: assoc)
   2.550 -  then show "y = z" by (simp add: lone linv)
   2.551 -qed simp
   2.552 -
   2.553 -locale Rqrgrp = Rqsemi + var one + var inv +
   2.554 -  assumes rone: "x ** one = x"
   2.555 -    and rinv: "x ** inv(x) = one"
   2.556 -
   2.557 -lemma (in Rqrgrp) rcancel:
   2.558 -  "y ** x = z ** x <-> y = z"
   2.559 -proof
   2.560 -  assume "y ** x = z ** x"
   2.561 -  then have "y ** (x ** inv(x)) = z ** (x ** inv(x))"
   2.562 -    by (simp add: assoc [symmetric])
   2.563 -  then show "y = z" by (simp add: rone rinv)
   2.564 -qed simp
   2.565 -
   2.566 -interpretation Rqrgrp < Rrgrp
   2.567 -  apply unfold_locales
   2.568 -  apply (rule assoc)
   2.569 -  apply (rule rone)
   2.570 -  apply (rule rinv)
   2.571 -  done
   2.572 -
   2.573 -interpretation R2: Rqlgrp ["op #" "rone" "rinv"] 
   2.574 -  apply unfold_locales  (* FIXME: unfold_locales is too eager and shouldn't
   2.575 -                          solve this. *)
   2.576 -  apply (rule i_assoc)
   2.577 -  apply (rule r_one)
   2.578 -  apply (rule r_inv)
   2.579 -  done
   2.580 -
   2.581 -print_interps Rqsemi
   2.582 -print_interps Rqlgrp
   2.583 -print_interps Rlgrp  (* no interpretations yet *)
   2.584 -
   2.585 -
   2.586 -interpretation Rqlgrp < Rqrgrp
   2.587 -  proof unfold_locales
   2.588 -    {
   2.589 -      fix x
   2.590 -      have "inv(x) ** x ** one = inv(x) ** x" by (simp add: linv lone)
   2.591 -      then show "x ** one = x" by (simp add: assoc lcancel)
   2.592 -    }
   2.593 -    note rone = this
   2.594 -    {
   2.595 -      fix x
   2.596 -      have "inv(x) ** x ** inv(x) = inv(x) ** one"
   2.597 -	by (simp add: linv lone rone)
   2.598 -      then show "x ** inv(x) = one" by (simp add: assoc lcancel)
   2.599 -    }
   2.600 -  qed
   2.601 -
   2.602 -print_interps! Rqrgrp
   2.603 -print_interps! Rsemi  (* witness must not have meta hyps *)
   2.604 -print_interps! Rrgrp  (* witness must not have meta hyps *)
   2.605 -print_interps! Rlgrp  (* witness must not have meta hyps *)
   2.606 -thm R2.rcancel
   2.607 -thm R2.lcancel
   2.608 -
   2.609 -ML {* check_thm "R2.rcancel"; check_thm "R2.lcancel" *}
   2.610 -
   2.611 -
   2.612 -subsection {* Generation of Witness Theorems for Transitive Interpretations *}
   2.613 -
   2.614 -locale Rtriv = var x +
   2.615 -  assumes x: "x = x"
   2.616 -
   2.617 -locale Rtriv2 = var x + var y +
   2.618 -  assumes x: "x = x" and y: "y = y"
   2.619 -
   2.620 -interpretation Rtriv2 < Rtriv x
   2.621 -  apply unfold_locales
   2.622 -  apply (rule x)
   2.623 -  done
   2.624 -
   2.625 -interpretation Rtriv2 < Rtriv y
   2.626 -  apply unfold_locales
   2.627 -  apply (rule y)
   2.628 -  done
   2.629 -
   2.630 -print_locale Rtriv2
   2.631 -
   2.632 -locale Rtriv3 = var x + var y + var z +
   2.633 -  assumes x: "x = x" and y: "y = y" and z: "z = z"
   2.634 -
   2.635 -interpretation Rtriv3 < Rtriv2 x y
   2.636 -  apply unfold_locales
   2.637 -  apply (rule x)
   2.638 -  apply (rule y)
   2.639 -  done
   2.640 -
   2.641 -print_locale Rtriv3
   2.642 -
   2.643 -interpretation Rtriv3 < Rtriv2 x z
   2.644 -  apply unfold_locales
   2.645 -  apply (rule x_y_z.x)
   2.646 -  apply (rule z)
   2.647 -  done
   2.648 -
   2.649 -ML {* set show_types *}
   2.650 -
   2.651 -print_locale Rtriv3
   2.652 -
   2.653 -
   2.654 -subsection {* Normalisation Replaces Assumed Element by Derived Element *}
   2.655 -
   2.656 -typedecl ('a, 'b) pair
   2.657 -arities pair :: ("term", "term") "term"
   2.658 -
   2.659 -consts
   2.660 -  pair :: "['a, 'b] => ('a, 'b) pair"
   2.661 -  fst :: "('a, 'b) pair => 'a"
   2.662 -  snd :: "('a, 'b) pair => 'b"
   2.663 -
   2.664 -axioms
   2.665 -  fst [simp]: "fst(pair(x, y)) = x"
   2.666 -  snd [simp]: "snd(pair(x, y)) = y"
   2.667 -
   2.668 -locale Rpair = var prod (infixl "**" 65) + var prodP (infixl "***" 65) +
   2.669 -  defines P_def: "x *** y == pair(fst(x) ** fst(y), snd(x) ** snd(y))"
   2.670 -
   2.671 -locale Rpair_semi = Rpair + Rsemi
   2.672 -
   2.673 -interpretation Rpair_semi < Rsemi prodP (infixl "***" 65)
   2.674 -proof unfold_locales
   2.675 -  fix x y z
   2.676 -  show "(x *** y) *** z = x *** (y *** z)"
   2.677 -    apply (simp only: P_def) apply (simp add: assoc) (* FIXME: unfold P_def fails *)
   2.678 -    done
   2.679 -qed
   2.680 -
   2.681 -locale Rsemi_rev = Rsemi + var rprod (infixl "++" 65) +
   2.682 -  defines r_def: "x ++ y == y ** x"
   2.683 -
   2.684 -lemma (in Rsemi_rev) r_assoc:
   2.685 -  "(x ++ y) ++ z = x ++ (y ++ z)"
   2.686 -  by (simp add: r_def assoc)
   2.687 -
   2.688 -
   2.689 -subsection {* Import of Locales with Predicates as Interpretation *}
   2.690 -
   2.691 -locale Ra =
   2.692 -  assumes Ra: "True"
   2.693 -
   2.694 -locale Rb = Ra +
   2.695 -  assumes Rb: "True"
   2.696 -
   2.697 -locale Rc = Rb +
   2.698 -  assumes Rc: "True"
   2.699 -
   2.700 -print_locale! Rc
   2.701 -
   2.702 -
   2.703 -section {* Interpretation of Defined Concepts *}
   2.704 -
   2.705 -text {* Naming convention for global objects: prefixes D and d *}
   2.706 -
   2.707 -
   2.708 -subsection {* Simple examples *}
   2.709 -
   2.710 -locale Da = fixes a :: o
   2.711 -  assumes true: a
   2.712 -
   2.713 -text {* In the following examples, @{term "~ a"} is the defined concept. *}
   2.714 -
   2.715 -lemma (in Da) not_false: "~ a <-> False"
   2.716 -  apply simp apply (rule true) done
   2.717 -
   2.718 -interpretation D1: Da ["True"]
   2.719 -  where "~ True == False"
   2.720 -  apply -
   2.721 -  apply unfold_locales [1] apply rule
   2.722 -  by simp
   2.723 -
   2.724 -thm D1.not_false
   2.725 -lemma "False <-> False" apply (rule D1.not_false) done
   2.726 -
   2.727 -interpretation D2: Da ["x | ~ x"]
   2.728 -  where "~ (x | ~ x) <-> ~ x & x"
   2.729 -  apply -
   2.730 -  apply unfold_locales [1] apply fast
   2.731 -  by simp
   2.732 -
   2.733 -thm D2.not_false
   2.734 -lemma "~ x & x <-> False" apply (rule D2.not_false) done
   2.735 -
   2.736 -print_interps! Da
   2.737 -
   2.738 -(* Subscriptions of interpretations *)
   2.739 -
   2.740 -lemma (in Da) not_false2: "~a <-> False"
   2.741 -  apply simp apply (rule true) done
   2.742 -
   2.743 -thm D1.not_false2 D2.not_false2
   2.744 -lemma "False <-> False" apply (rule D1.not_false2) done
   2.745 -lemma "~x & x <-> False" apply (rule D2.not_false2) done
   2.746 -
   2.747 -(* Unfolding in attributes *)
   2.748 -
   2.749 -locale Db = Da +
   2.750 -  fixes b :: o
   2.751 -  assumes a_iff_b: "~a <-> b"
   2.752 -
   2.753 -lemmas (in Db) not_false_b = not_false [unfolded a_iff_b]
   2.754 -
   2.755 -interpretation D2: Db ["x | ~ x" "~ (x <-> x)"]
   2.756 -  apply unfold_locales apply fast done
   2.757 -
   2.758 -thm D2.not_false_b
   2.759 -lemma "~(x <-> x) <-> False" apply (rule D2.not_false_b) done
   2.760 -
   2.761 -(* Subscription and attributes *)
   2.762 -
   2.763 -lemmas (in Db) not_false_b2 = not_false [unfolded a_iff_b]
   2.764 -
   2.765 -thm D2.not_false_b2
   2.766 -lemma "~(x <-> x) <-> False" apply (rule D2.not_false_b2) done
   2.767 -
   2.768 -end
     3.1 --- a/src/FOL/ex/NewLocaleTest.thy	Fri Dec 19 15:05:37 2008 +0100
     3.2 +++ b/src/FOL/ex/NewLocaleTest.thy	Fri Dec 19 16:39:23 2008 +0100
     3.3 @@ -8,7 +8,6 @@
     3.4  imports NewLocaleSetup
     3.5  begin
     3.6  
     3.7 -ML_val {* set new_locales *}
     3.8  ML_val {* set Toplevel.debug *}
     3.9  
    3.10  
     4.1 --- a/src/FOL/ex/ROOT.ML	Fri Dec 19 15:05:37 2008 +0100
     4.2 +++ b/src/FOL/ex/ROOT.ML	Fri Dec 19 16:39:23 2008 +0100
     4.3 @@ -29,6 +29,5 @@
     4.4  ];
     4.5  
     4.6  (*regression test for locales -- sets several global flags!*)
     4.7 -no_document use_thy "LocaleTest";
     4.8  no_document use_thy "NewLocaleTest";
     4.9  
     5.1 --- a/src/HOL/ROOT.ML	Fri Dec 19 15:05:37 2008 +0100
     5.2 +++ b/src/HOL/ROOT.ML	Fri Dec 19 16:39:23 2008 +0100
     5.3 @@ -3,7 +3,6 @@
     5.4  Classical Higher-order Logic -- batteries included.
     5.5  *)
     5.6  
     5.7 -set new_locales;
     5.8  use_thy "Complex_Main";
     5.9  
    5.10  val HOL_proofs = ! Proofterm.proofs;
     6.1 --- a/src/HOL/main.ML	Fri Dec 19 15:05:37 2008 +0100
     6.2 +++ b/src/HOL/main.ML	Fri Dec 19 16:39:23 2008 +0100
     6.3 @@ -4,5 +4,4 @@
     6.4  Classical Higher-order Logic -- only "Main".
     6.5  *)
     6.6  
     6.7 -set new_locales;
     6.8  use_thy "Main";
     7.1 --- a/src/HOL/plain.ML	Fri Dec 19 15:05:37 2008 +0100
     7.2 +++ b/src/HOL/plain.ML	Fri Dec 19 16:39:23 2008 +0100
     7.3 @@ -3,5 +3,4 @@
     7.4  Classical Higher-order Logic -- plain Tool bootstrap.
     7.5  *)
     7.6  
     7.7 -set new_locales;
     7.8  use_thy "Plain";
     8.1 --- a/src/Pure/Isar/ROOT.ML	Fri Dec 19 15:05:37 2008 +0100
     8.2 +++ b/src/Pure/Isar/ROOT.ML	Fri Dec 19 16:39:23 2008 +0100
     8.3 @@ -51,7 +51,6 @@
     8.4  use "obtain.ML";
     8.5  
     8.6  (*local theories and targets*)
     8.7 -val new_locales = ref false;
     8.8  use "local_theory.ML";
     8.9  use "overloading.ML";
    8.10  use "locale.ML";
     9.1 --- a/src/Pure/Isar/specification.ML	Fri Dec 19 15:05:37 2008 +0100
     9.2 +++ b/src/Pure/Isar/specification.ML	Fri Dec 19 16:39:23 2008 +0100
     9.3 @@ -59,18 +59,6 @@
     9.4  structure Specification: SPECIFICATION =
     9.5  struct
     9.6  
     9.7 -(* new locales *)
     9.8 -
     9.9 -fun cert_stmt body concl ctxt =
    9.10 -  let val (_, _, ctxt', concl') = Locale.cert_context_statement NONE body concl ctxt
    9.11 -  in (concl', ctxt') end;
    9.12 -fun read_stmt body concl ctxt =
    9.13 -  let val (_, _, ctxt', concl') = Locale.read_context_statement NONE body concl ctxt
    9.14 -  in (concl', ctxt') end;
    9.15 -  
    9.16 -fun cert_context_statement x = if !new_locales then Expression.cert_statement x else cert_stmt x;
    9.17 -fun read_context_statement x = if !new_locales then Expression.read_statement x else read_stmt x;
    9.18 -
    9.19  (* diagnostics *)
    9.20  
    9.21  fun print_consts _ _ [] = ()
    9.22 @@ -370,8 +358,8 @@
    9.23  
    9.24  in
    9.25  
    9.26 -val theorem = gen_theorem (K I) cert_context_statement;
    9.27 -val theorem_cmd = gen_theorem Attrib.intern_src read_context_statement;
    9.28 +val theorem = gen_theorem (K I) Expression.cert_statement;
    9.29 +val theorem_cmd = gen_theorem Attrib.intern_src Expression.read_statement;
    9.30  
    9.31  fun add_theorem_hook f = TheoremHook.map (cons (f, stamp ()));
    9.32  
    10.1 --- a/src/Pure/Isar/theory_target.ML	Fri Dec 19 15:05:37 2008 +0100
    10.2 +++ b/src/Pure/Isar/theory_target.ML	Fri Dec 19 16:39:23 2008 +0100
    10.3 @@ -25,19 +25,19 @@
    10.4  (* new locales *)
    10.5  
    10.6  fun locale_extern new_locale x = 
    10.7 -  if !new_locales andalso new_locale then NewLocale.extern x else Locale.extern x;
    10.8 +  if new_locale then NewLocale.extern x else Locale.extern x;
    10.9  fun locale_add_type_syntax new_locale x =
   10.10 -  if !new_locales andalso new_locale then NewLocale.add_type_syntax x else Locale.add_type_syntax x;
   10.11 +  if new_locale then NewLocale.add_type_syntax x else Locale.add_type_syntax x;
   10.12  fun locale_add_term_syntax new_locale x =
   10.13 -  if !new_locales andalso new_locale then NewLocale.add_term_syntax x else Locale.add_term_syntax x;
   10.14 +  if new_locale then NewLocale.add_term_syntax x else Locale.add_term_syntax x;
   10.15  fun locale_add_declaration new_locale x =
   10.16 -  if !new_locales andalso new_locale then NewLocale.add_declaration x else Locale.add_declaration x;
   10.17 +  if new_locale then NewLocale.add_declaration x else Locale.add_declaration x;
   10.18  fun locale_add_thmss new_locale x =
   10.19 -  if !new_locales andalso new_locale then NewLocale.add_thmss x else Locale.add_thmss x;
   10.20 +  if new_locale then NewLocale.add_thmss x else Locale.add_thmss x;
   10.21  fun locale_init new_locale x =
   10.22 -  if !new_locales andalso new_locale then NewLocale.init x else Locale.init x;
   10.23 +  if new_locale then NewLocale.init x else Locale.init x;
   10.24  fun locale_intern new_locale x =
   10.25 -  if !new_locales andalso new_locale then NewLocale.intern x else Locale.intern x;
   10.26 +  if new_locale then NewLocale.intern x else Locale.intern x;
   10.27  
   10.28  (* context data *)
   10.29  
    11.1 --- a/src/ZF/ROOT.ML	Fri Dec 19 15:05:37 2008 +0100
    11.2 +++ b/src/ZF/ROOT.ML	Fri Dec 19 16:39:23 2008 +0100
    11.3 @@ -8,6 +8,5 @@
    11.4  Paulson.
    11.5  *)
    11.6  
    11.7 -set new_locales;
    11.8  use_thys ["Main", "Main_ZFC"];
    11.9