dropped locale (open)
authorhaftmann
Fri Jul 25 12:03:32 2008 +0200 (2008-07-25 ago)
changeset 276818cedebf55539
parent 27680 5a557a5afc48
child 27682 25aceefd4786
dropped locale (open)
NEWS
doc-src/IsarRef/Thy/Spec.thy
src/FOL/ex/LocaleTest.thy
src/HOL/Hyperreal/SEQ.thy
src/HOL/Library/Eval.thy
src/HOL/MetisExamples/Tarski.thy
src/HOL/MicroJava/BV/Err.thy
src/HOL/MicroJava/BV/Kildall.thy
src/HOL/MicroJava/BV/LBVComplete.thy
src/HOL/MicroJava/BV/LBVCorrect.thy
src/HOL/MicroJava/BV/LBVJVM.thy
src/HOL/MicroJava/BV/LBVSpec.thy
src/HOL/MicroJava/BV/Listn.thy
src/HOL/MicroJava/BV/Product.thy
src/HOL/MicroJava/BV/Semilat.thy
src/HOL/MicroJava/BV/SemilatAlg.thy
src/HOL/NSA/Filter.thy
src/HOL/Statespace/state_space.ML
src/HOL/ex/Tarski.thy
src/HOLCF/Deflation.thy
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/locale.ML
src/Pure/Pure.thy
     1.1 --- a/NEWS	Fri Jul 25 12:03:31 2008 +0200
     1.2 +++ b/NEWS	Fri Jul 25 12:03:32 2008 +0200
     1.3 @@ -19,6 +19,8 @@
     1.4  
     1.5  *** Pure ***
     1.6  
     1.7 +* dropped "locale (open)".  INCOMPATBILITY.
     1.8 +
     1.9  * Command 'instance': attached definitions no longer accepted.
    1.10  INCOMPATIBILITY, use proper 'instantiation' target.
    1.11  
    1.12 @@ -34,6 +36,10 @@
    1.13  
    1.14  *** HOL ***
    1.15  
    1.16 +* HOL/Orderings: added class "preorder" as superclass of "order".  INCOMPATIBILITY:
    1.17 +Instantiation proofs for order, linorder etc. slightly changed.  Some theorems
    1.18 +named order_class.* now named preorder_class.*.
    1.19 +
    1.20  * HOL/Ring_and_Field and HOL/Divides: Definition of "op dvd" has been moved
    1.21  to separate class dvd in Ring_and_Field;  a couple of lemmas on dvd has been
    1.22  generalized to class comm_semiring_1.  Likewise a bunch of lemmas from Divides
     2.1 --- a/doc-src/IsarRef/Thy/Spec.thy	Fri Jul 25 12:03:31 2008 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/Spec.thy	Fri Jul 25 12:03:32 2008 +0200
     2.3 @@ -298,7 +298,7 @@
     2.4    \indexisarelem{fixes}\indexisarelem{constrains}\indexisarelem{assumes}
     2.5    \indexisarelem{defines}\indexisarelem{notes}\indexisarelem{includes}
     2.6    \begin{rail}
     2.7 -    'locale' ('(open)')? name ('=' localeexpr)? 'begin'?
     2.8 +    'locale' name ('=' localeexpr)? 'begin'?
     2.9      ;
    2.10      'print\_locale' '!'? localeexpr
    2.11      ;
    2.12 @@ -415,11 +415,6 @@
    2.13    \secref{sec:object-logic}).  Separate introduction rules @{text
    2.14    loc_axioms.intro} and @{text loc.intro} are provided as well.
    2.15    
    2.16 -  The @{text "(open)"} option of a locale specification prevents both
    2.17 -  the current @{text loc_axioms} and cumulative @{text loc} predicate
    2.18 -  constructions.  Predicates are also omitted for empty specification
    2.19 -  texts.
    2.20 -
    2.21    \item [@{command "print_locale"}~@{text "import + body"}] prints the
    2.22    specified locale expression in a flattened form.  The notable
    2.23    special case @{command "print_locale"}~@{text loc} just prints the
     3.1 --- a/src/FOL/ex/LocaleTest.thy	Fri Jul 25 12:03:31 2008 +0200
     3.2 +++ b/src/FOL/ex/LocaleTest.thy	Fri Jul 25 12:03:32 2008 +0200
     3.3 @@ -37,7 +37,7 @@
     3.4  
     3.5  subsection {* Renaming with Syntax *}
     3.6  
     3.7 -locale (open) LS = var mult +
     3.8 +locale LS = var mult +
     3.9    assumes "mult(x, y) = mult(y, x)"
    3.10  
    3.11  print_locale LS
    3.12 @@ -95,7 +95,7 @@
    3.13  
    3.14  locale IA = fixes a assumes asm_A: "a = a"
    3.15  
    3.16 -locale (open) IB = fixes b assumes asm_B [simp]: "b = b"
    3.17 +locale IB = fixes b assumes asm_B [simp]: "b = b"
    3.18  
    3.19  locale IC = IA + IB + assumes asm_C: "c = c"
    3.20    (* TODO: independent type var in c, prohibit locale declaration *)
    3.21 @@ -230,10 +230,10 @@
    3.22  
    3.23  (* Definition involving free variable in assm *)
    3.24  
    3.25 -locale (open) IG = fixes g assumes asm_G: "g --> x"
    3.26 +locale IG = fixes g assumes asm_G: "g --> x"
    3.27    notes asm_G2 = asm_G
    3.28  
    3.29 -interpretation i8: IG ["False"] by fast
    3.30 +interpretation i8: IG ["False"] by (rule IG.intro) fast
    3.31  
    3.32  thm i8.asm_G2
    3.33  
    3.34 @@ -346,10 +346,10 @@
    3.35  
    3.36  text {* Naming convention for global objects: prefixes R and r *}
    3.37  
    3.38 -locale (open) Rsemi = var prod (infixl "**" 65) +
    3.39 +locale Rsemi = var prod (infixl "**" 65) +
    3.40    assumes assoc: "(x ** y) ** z = x ** (y ** z)"
    3.41  
    3.42 -locale (open) Rlgrp = Rsemi + var one + var inv +
    3.43 +locale Rlgrp = Rsemi + var one + var inv +
    3.44    assumes lone: "one ** x = x"
    3.45      and linv: "inv(x) ** x = one"
    3.46  
    3.47 @@ -361,7 +361,7 @@
    3.48    then show "y = z" by (simp add: lone linv)
    3.49  qed simp
    3.50  
    3.51 -locale (open) Rrgrp = Rsemi + var one + var inv +
    3.52 +locale Rrgrp = Rsemi + var one + var inv +
    3.53    assumes rone: "x ** one = x"
    3.54      and rinv: "x ** inv(x) = one"
    3.55  
    3.56 @@ -375,7 +375,7 @@
    3.57  qed simp
    3.58  
    3.59  interpretation Rlgrp < Rrgrp
    3.60 -  proof -
    3.61 +  proof
    3.62      {
    3.63        fix x
    3.64        have "inv(x) ** x ** one = inv(x) ** x" by (simp add: linv lone)
    3.65 @@ -405,7 +405,7 @@
    3.66  (* circular interpretation *)
    3.67  
    3.68  interpretation Rrgrp < Rlgrp
    3.69 -  proof -
    3.70 +  proof
    3.71      {
    3.72        fix x
    3.73        have "one ** (x ** inv(x)) = x ** inv(x)" by (simp add: rinv rone)
    3.74 @@ -451,35 +451,35 @@
    3.75  
    3.76  (* circle of three locales, forward direction *)
    3.77  
    3.78 -locale (open) RA1 = var A + var B + assumes p: "A <-> B"
    3.79 -locale (open) RA2 = var A + var B + assumes q: "A & B | ~ A & ~ B"
    3.80 -locale (open) RA3 = var A + var B + assumes r: "(A --> B) & (B --> A)"
    3.81 +locale RA1 = var A + var B + assumes p: "A <-> B"
    3.82 +locale RA2 = var A + var B + assumes q: "A & B | ~ A & ~ B"
    3.83 +locale RA3 = var A + var B + assumes r: "(A --> B) & (B --> A)"
    3.84  
    3.85  interpretation RA1 < RA2
    3.86    print_facts
    3.87 -  using p apply fast done
    3.88 +  using p apply unfold_locales apply fast done
    3.89  interpretation RA2 < RA3
    3.90    print_facts
    3.91 -  using q apply fast done
    3.92 +  using q apply unfold_locales apply fast done
    3.93  interpretation RA3 < RA1
    3.94    print_facts
    3.95 -  using r apply fast done
    3.96 +  using r apply unfold_locales apply fast done
    3.97  
    3.98  (* circle of three locales, backward direction *)
    3.99  
   3.100 -locale (open) RB1 = var A + var B + assumes p: "A <-> B"
   3.101 -locale (open) RB2 = var A + var B + assumes q: "A & B | ~ A & ~ B"
   3.102 -locale (open) RB3 = var A + var B + assumes r: "(A --> B) & (B --> A)"
   3.103 +locale RB1 = var A + var B + assumes p: "A <-> B"
   3.104 +locale RB2 = var A + var B + assumes q: "A & B | ~ A & ~ B"
   3.105 +locale RB3 = var A + var B + assumes r: "(A --> B) & (B --> A)"
   3.106  
   3.107  interpretation RB1 < RB2
   3.108    print_facts
   3.109 -  using p apply fast done
   3.110 +  using p apply unfold_locales apply fast done
   3.111  interpretation RB3 < RB1
   3.112    print_facts
   3.113 -  using r apply fast done
   3.114 +  using r apply unfold_locales apply fast done
   3.115  interpretation RB2 < RB3
   3.116    print_facts
   3.117 -  using q apply fast done
   3.118 +  using q apply unfold_locales apply fast done
   3.119  
   3.120  lemma (in RB1) True
   3.121    print_facts
   3.122 @@ -579,7 +579,7 @@
   3.123    r_inv : "rinv(x) # x = rone"
   3.124  
   3.125  interpretation Rbool: Rlgrp ["op #" "rone" "rinv"]
   3.126 -proof -
   3.127 +proof
   3.128    fix x y z
   3.129    {
   3.130      show "(x # y) # z = x # (y # z)" by (rule i_assoc)
   3.131 @@ -653,6 +653,9 @@
   3.132  interpretation R2: Rqlgrp ["op #" "rone" "rinv"] 
   3.133    apply unfold_locales  (* FIXME: unfold_locales is too eager and shouldn't
   3.134                            solve this. *)
   3.135 +  apply (rule i_assoc)
   3.136 +  apply (rule r_one)
   3.137 +  apply (rule r_inv)
   3.138    done
   3.139  
   3.140  print_interps Rqsemi
     4.1 --- a/src/HOL/Hyperreal/SEQ.thy	Fri Jul 25 12:03:31 2008 +0200
     4.2 +++ b/src/HOL/Hyperreal/SEQ.thy	Fri Jul 25 12:03:32 2008 +0200
     4.3 @@ -926,12 +926,17 @@
     4.4    "(\<bar>x - a\<bar> < (r::real)) = (a - r < x \<and> x < a + r)"
     4.5  by auto
     4.6  
     4.7 -locale (open) real_Cauchy =
     4.8 +locale real_Cauchy =
     4.9    fixes X :: "nat \<Rightarrow> real"
    4.10    assumes X: "Cauchy X"
    4.11    fixes S :: "real set"
    4.12    defines S_def: "S \<equiv> {x::real. \<exists>N. \<forall>n\<ge>N. x < X n}"
    4.13  
    4.14 +lemma real_CauchyI:
    4.15 +  assumes "Cauchy X"
    4.16 +  shows "real_Cauchy X"
    4.17 +by unfold_locales (fact assms)
    4.18 +
    4.19  lemma (in real_Cauchy) mem_S: "\<forall>n\<ge>N. x < X n \<Longrightarrow> x \<in> S"
    4.20  by (unfold S_def, auto)
    4.21  
    4.22 @@ -1010,7 +1015,9 @@
    4.23  lemma real_Cauchy_convergent:
    4.24    fixes X :: "nat \<Rightarrow> real"
    4.25    shows "Cauchy X \<Longrightarrow> convergent X"
    4.26 -unfolding convergent_def by (rule real_Cauchy.LIMSEQ_ex)
    4.27 +unfolding convergent_def
    4.28 +by (rule real_Cauchy.LIMSEQ_ex)
    4.29 + (rule real_CauchyI)
    4.30  
    4.31  instance real :: banach
    4.32  by intro_classes (rule real_Cauchy_convergent)
     5.1 --- a/src/HOL/Library/Eval.thy	Fri Jul 25 12:03:31 2008 +0200
     5.2 +++ b/src/HOL/Library/Eval.thy	Fri Jul 25 12:03:32 2008 +0200
     5.3 @@ -177,7 +177,7 @@
     5.4  notation (output)
     5.5    rterm_of ("\<guillemotleft>_\<guillemotright>")
     5.6  
     5.7 -locale (open) rterm_syntax =
     5.8 +locale rterm_syntax =
     5.9    fixes rterm_of_syntax :: "'a \<Rightarrow> 'b" ("\<guillemotleft>_\<guillemotright>")
    5.10  
    5.11  parse_translation {*
     6.1 --- a/src/HOL/MetisExamples/Tarski.thy	Fri Jul 25 12:03:31 2008 +0200
     6.2 +++ b/src/HOL/MetisExamples/Tarski.thy	Fri Jul 25 12:03:32 2008 +0200
     6.3 @@ -69,10 +69,6 @@
     6.4                          (\<forall>S. S \<subseteq> pset cl --> (\<exists>L. isLub S cl L)) &
     6.5                          (\<forall>S. S \<subseteq> pset cl --> (\<exists>G. isGlb S cl G))}"
     6.6  
     6.7 -  CLF :: "('a potype * ('a => 'a)) set"
     6.8 -  "CLF == SIGMA cl: CompleteLattice.
     6.9 -            {f. f: pset cl -> pset cl & monotone f (pset cl) (order cl)}"
    6.10 -
    6.11    induced :: "['a set, ('a * 'a) set] => ('a *'a)set"
    6.12    "induced A r == {(a,b). a : A & b: A & (a,b): r}"
    6.13  
    6.14 @@ -93,7 +89,7 @@
    6.15    dual :: "'a potype => 'a potype"
    6.16    "dual po == (| pset = pset po, order = converse (order po) |)"
    6.17  
    6.18 -locale (open) PO =
    6.19 +locale PO =
    6.20    fixes cl :: "'a potype"
    6.21      and A  :: "'a set"
    6.22      and r  :: "('a * 'a) set"
    6.23 @@ -101,17 +97,21 @@
    6.24    defines A_def: "A == pset cl"
    6.25       and  r_def: "r == order cl"
    6.26  
    6.27 -locale (open) CL = PO +
    6.28 +locale CL = PO +
    6.29    assumes cl_co:  "cl : CompleteLattice"
    6.30  
    6.31 -locale (open) CLF = CL +
    6.32 +definition CLF_set :: "('a potype * ('a => 'a)) set" where
    6.33 +  "CLF_set = (SIGMA cl: CompleteLattice.
    6.34 +            {f. f: pset cl -> pset cl & monotone f (pset cl) (order cl)})"
    6.35 +
    6.36 +locale CLF = CL +
    6.37    fixes f :: "'a => 'a"
    6.38      and P :: "'a set"
    6.39 -  assumes f_cl:  "(cl,f) : CLF" (*was the equivalent "f : CLF``{cl}"*)
    6.40 +  assumes f_cl:  "(cl,f) : CLF_set" (*was the equivalent "f : CLF``{cl}"*)
    6.41    defines P_def: "P == fix f A"
    6.42  
    6.43  
    6.44 -locale (open) Tarski = CLF +
    6.45 +locale Tarski = CLF +
    6.46    fixes Y     :: "'a set"
    6.47      and intY1 :: "'a set"
    6.48      and v     :: "'a"
    6.49 @@ -230,9 +230,9 @@
    6.50  
    6.51  lemmas CL_imp_PO = CL_subset_PO [THEN subsetD]
    6.52  
    6.53 -declare CL_imp_PO [THEN PO.PO_imp_refl, simp]
    6.54 -declare CL_imp_PO [THEN PO.PO_imp_sym, simp]
    6.55 -declare CL_imp_PO [THEN PO.PO_imp_trans, simp]
    6.56 +declare PO.PO_imp_refl  [OF PO.intro [OF CL_imp_PO], simp]
    6.57 +declare PO.PO_imp_sym   [OF PO.intro [OF CL_imp_PO], simp]
    6.58 +declare PO.PO_imp_trans [OF PO.intro [OF CL_imp_PO], simp]
    6.59  
    6.60  lemma (in CL) CO_refl: "refl A r"
    6.61  by (rule PO_imp_refl)
    6.62 @@ -385,7 +385,10 @@
    6.63  apply (simp add: A_def)
    6.64  apply (rule dualA_iff [THEN subst])
    6.65  apply (rule CL.lub_in_lattice)
    6.66 +apply (rule CL.intro)
    6.67 +apply (rule PO.intro)
    6.68  apply (rule dualPO)
    6.69 +apply (rule CL_axioms.intro)
    6.70  apply (rule CL_dualCL)
    6.71  apply (simp add: dualA_iff)
    6.72  done
    6.73 @@ -395,7 +398,10 @@
    6.74  apply (simp add: r_def)
    6.75  apply (rule dualr_iff [THEN subst])
    6.76  apply (rule CL.lub_upper)
    6.77 +apply (rule CL.intro)
    6.78 +apply (rule PO.intro)
    6.79  apply (rule dualPO)
    6.80 +apply (rule CL_axioms.intro)
    6.81  apply (rule CL_dualCL)
    6.82  apply (simp add: dualA_iff A_def, assumption)
    6.83  done
    6.84 @@ -414,10 +420,10 @@
    6.85  lemma (in CLF) [simp]:
    6.86      "f: pset cl -> pset cl & monotone f (pset cl) (order cl)" 
    6.87  apply (insert f_cl)
    6.88 -apply (unfold CLF_def)
    6.89 +apply (unfold CLF_set_def)
    6.90  apply (erule SigmaE2) 
    6.91  apply (erule CollectE) 
    6.92 -apply assumption; 
    6.93 +apply assumption
    6.94  done
    6.95  
    6.96  lemma (in CLF) f_in_funcset: "f \<in> A -> A"
    6.97 @@ -428,12 +434,14 @@
    6.98  
    6.99  (*never proved, 2007-01-22*)
   6.100  ML_command{*ResAtp.problem_name:="Tarski__CLF_CLF_dual"*}
   6.101 -  declare (in CLF) CLF_def[simp] CL_dualCL[simp] monotone_dual[simp] dualA_iff[simp]
   6.102 -lemma (in CLF) CLF_dual: "(dual cl, f) \<in> CLF" 
   6.103 +declare (in CLF) CLF_set_def [simp] CL_dualCL [simp] monotone_dual [simp] dualA_iff [simp]
   6.104 +
   6.105 +lemma (in CLF) CLF_dual: "(dual cl, f) \<in> CLF_set" 
   6.106  apply (simp del: dualA_iff)
   6.107  apply (simp)
   6.108  done
   6.109 -  declare  (in CLF) CLF_def[simp del] CL_dualCL[simp del] monotone_dual[simp del]
   6.110 +
   6.111 +declare (in CLF) CLF_set_def[simp del] CL_dualCL[simp del] monotone_dual[simp del]
   6.112            dualA_iff[simp del]
   6.113  
   6.114  
   6.115 @@ -639,8 +647,13 @@
   6.116  apply (simp add: glb_dual_lub P_def A_def r_def)
   6.117  apply (rule dualA_iff [THEN subst])
   6.118  apply (rule CLF.lubH_is_fixp)
   6.119 +apply (rule CLF.intro)
   6.120 +apply (rule CL.intro)
   6.121 +apply (rule PO.intro)
   6.122  apply (rule dualPO)
   6.123 +apply (rule CL_axioms.intro)
   6.124  apply (rule CL_dualCL)
   6.125 +apply (rule CLF_axioms.intro)
   6.126  apply (rule CLF_dual)
   6.127  apply (simp add: dualr_iff dualA_iff)
   6.128  done
   6.129 @@ -657,8 +670,8 @@
   6.130  (*never proved, 2007-01-22*)
   6.131  ML_command{*ResAtp.problem_name:="Tarski__T_thm_1_glb_simpler"*}  (*ALL THEOREMS*)
   6.132  (*sledgehammer;*)
   6.133 -apply (simp add: CLF.T_thm_1_lub [of _ f, OF dualPO CL_dualCL]
   6.134 -                 dualPO CL_dualCL CLF_dual dualr_iff)
   6.135 +apply (simp add: CLF.T_thm_1_lub [of _ f, OF CLF.intro, OF CL.intro CLF_axioms.intro, OF PO.intro CL_axioms.intro,
   6.136 +  OF dualPO CL_dualCL] dualPO CL_dualCL CLF_dual dualr_iff)
   6.137  done
   6.138  
   6.139  subsection {* interval *}
   6.140 @@ -729,7 +742,7 @@
   6.141       "[| a \<in> A; b \<in> A; interval r a b \<noteq> {}; S \<subseteq> interval r a b; isGlb S cl G;
   6.142           S \<noteq> {} |] ==> G \<in> interval r a b"
   6.143  apply (simp add: interval_dual)
   6.144 -apply (simp add: CLF.L_in_interval [of _ f]
   6.145 +apply (simp add: CLF.L_in_interval [of _ f, OF CLF.intro, OF CL.intro CLF_axioms.intro, OF PO.intro CL_axioms.intro]
   6.146                   dualA_iff A_def dualPO CL_dualCL CLF_dual isGlb_dual_isLub)
   6.147  done
   6.148  
   6.149 @@ -851,7 +864,7 @@
   6.150  ML_command{*ResAtp.problem_name:="Tarski__Top_in_lattice_simpler"*}  (*ALL THEOREMS*)
   6.151  (*sledgehammer*)
   6.152  apply (rule dualA_iff [THEN subst])
   6.153 -apply (blast intro!: CLF.Bot_in_lattice dualPO CL_dualCL CLF_dual)
   6.154 +apply (blast intro!: CLF.Bot_in_lattice [OF CLF.intro, OF CL.intro CLF_axioms.intro, OF PO.intro CL_axioms.intro] dualPO CL_dualCL CLF_dual)
   6.155  done
   6.156  
   6.157  lemma (in CLF) Top_prop: "x \<in> A ==> (x, Top cl) \<in> r"
   6.158 @@ -868,7 +881,7 @@
   6.159  (*sledgehammer*) 
   6.160  apply (simp add: Bot_dual_Top r_def)
   6.161  apply (rule dualr_iff [THEN subst])
   6.162 -apply (simp add: CLF.Top_prop [of _ f]
   6.163 +apply (simp add: CLF.Top_prop [of _ f, OF CLF.intro, OF CL.intro CLF_axioms.intro, OF PO.intro CL_axioms.intro]
   6.164                   dualA_iff A_def dualPO CL_dualCL CLF_dual)
   6.165  done
   6.166  
   6.167 @@ -996,8 +1009,8 @@
   6.168  apply (unfold P_def)
   6.169  apply (rule_tac A = "intY1" in fixf_subset)
   6.170  apply (rule intY1_subset)
   6.171 -apply (simp add: CLF.glbH_is_fixp [OF _ intY1_is_cl, simplified]
   6.172 -                 v_def CL_imp_PO intY1_is_cl CLF_def intY1_func intY1_mono)
   6.173 +apply (simp add: CLF.glbH_is_fixp [OF CLF.intro, OF CL.intro CLF_axioms.intro, OF PO.intro CL_axioms.intro, OF _ intY1_is_cl, simplified]
   6.174 +                 v_def CL_imp_PO intY1_is_cl CLF_set_def intY1_func intY1_mono)
   6.175  done
   6.176  
   6.177  ML_command{*ResAtp.problem_name:="Tarski__z_in_interval"*}  (*ALL THEOREMS*)
   6.178 @@ -1042,7 +1055,7 @@
   6.179  apply (rule_tac b = "Top cl" in interval_imp_mem)
   6.180  apply (simp add: v_def)
   6.181  apply (fold intY1_def)
   6.182 -apply (rule CL.glb_in_lattice [OF _ intY1_is_cl, simplified])
   6.183 +apply (rule CL.glb_in_lattice [OF CL.intro, OF PO.intro CL_axioms.intro, OF _ intY1_is_cl, simplified])
   6.184   apply (simp add: CL_imp_PO intY1_is_cl, force)
   6.185  -- {* @{text v} is LEAST ub *}
   6.186  apply clarify
   6.187 @@ -1058,7 +1071,7 @@
   6.188  (*never proved, 2007-01-22*)
   6.189  ML_command{*ResAtp.problem_name:="Tarski__tarski_full_lemma_simplest"*} 
   6.190  (*sledgehammer*) 
   6.191 -apply (rule CL.glb_lower [OF _ intY1_is_cl, simplified])
   6.192 +apply (rule CL.glb_lower [OF CL.intro, OF PO.intro CL_axioms.intro, OF _ intY1_is_cl, simplified])
   6.193    apply (simp add: CL_imp_PO intY1_is_cl)
   6.194   apply force
   6.195  apply (simp add: induced_def intY1_f_closed z_in_interval)
   6.196 @@ -1087,7 +1100,8 @@
   6.197  ML_command{*ResAtp.problem_name:="Tarski__Tarski_full_simpler"*}
   6.198  (*sledgehammer*) 
   6.199  apply (simp add: P_def A_def r_def)
   6.200 -apply (blast intro!: Tarski.tarski_full_lemma cl_po cl_co f_cl)
   6.201 +apply (blast intro!: Tarski.tarski_full_lemma [OF Tarski.intro, OF CLF.intro Tarski_axioms.intro,
   6.202 +  OF CL.intro CLF_axioms.intro, OF PO.intro CL_axioms.intro] cl_po cl_co f_cl)
   6.203  done
   6.204    declare (in CLF) fixf_po[rule del] P_def [simp del] A_def [simp del] r_def [simp del]
   6.205           Tarski.tarski_full_lemma [rule del] cl_po [rule del] cl_co [rule del]
     7.1 --- a/src/HOL/MicroJava/BV/Err.thy	Fri Jul 25 12:03:31 2008 +0200
     7.2 +++ b/src/HOL/MicroJava/BV/Err.thy	Fri Jul 25 12:03:32 2008 +0200
     7.3 @@ -8,7 +8,9 @@
     7.4  
     7.5  header {* \isaheader{The Error Type} *}
     7.6  
     7.7 -theory Err imports Semilat begin
     7.8 +theory Err
     7.9 +imports Semilat
    7.10 +begin
    7.11  
    7.12  datatype 'a err = Err | OK 'a
    7.13  
    7.14 @@ -228,20 +230,20 @@
    7.15  
    7.16  lemma semilat_le_err_Err_plus [simp]:
    7.17    "\<lbrakk> x: err A; semilat(err A, le r, f) \<rbrakk> \<Longrightarrow> Err +_f x = Err"
    7.18 -  by (blast intro: semilat.le_iff_plus_unchanged [THEN iffD1]
    7.19 -                   semilat.le_iff_plus_unchanged2 [THEN iffD1])
    7.20 +  by (blast intro: Semilat.le_iff_plus_unchanged [OF Semilat.intro, THEN iffD1]
    7.21 +                   Semilat.le_iff_plus_unchanged2 [OF Semilat.intro, THEN iffD1])
    7.22  
    7.23  lemma semilat_le_err_plus_Err [simp]:
    7.24    "\<lbrakk> x: err A; semilat(err A, le r, f) \<rbrakk> \<Longrightarrow> x +_f Err = Err"
    7.25 -  by (blast intro: semilat.le_iff_plus_unchanged [THEN iffD1]
    7.26 -                   semilat.le_iff_plus_unchanged2 [THEN iffD1])
    7.27 +  by (blast intro: Semilat.le_iff_plus_unchanged [OF Semilat.intro, THEN iffD1]
    7.28 +                   Semilat.le_iff_plus_unchanged2 [OF Semilat.intro, THEN iffD1])
    7.29  
    7.30  lemma semilat_le_err_OK1:
    7.31    "\<lbrakk> x:A; y:A; semilat(err A, le r, f); OK x +_f OK y = OK z \<rbrakk> 
    7.32    \<Longrightarrow> x <=_r z";
    7.33  apply (rule OK_le_err_OK [THEN iffD1])
    7.34  apply (erule subst)
    7.35 -apply (simp add:semilat.ub1)
    7.36 +apply (simp add: Semilat.ub1 [OF Semilat.intro])
    7.37  done
    7.38  
    7.39  lemma semilat_le_err_OK2:
    7.40 @@ -249,7 +251,7 @@
    7.41    \<Longrightarrow> y <=_r z"
    7.42  apply (rule OK_le_err_OK [THEN iffD1])
    7.43  apply (erule subst)
    7.44 -apply (simp add:semilat.ub2)
    7.45 +apply (simp add: Semilat.ub2 [OF Semilat.intro])
    7.46  done
    7.47  
    7.48  lemma eq_order_le:
    7.49 @@ -265,13 +267,13 @@
    7.50    have plus_le_conv3: "\<And>A x y z f r. 
    7.51      \<lbrakk> semilat (A,r,f); x +_f y <=_r z; x:A; y:A; z:A \<rbrakk> 
    7.52      \<Longrightarrow> x <=_r z \<and> y <=_r z"
    7.53 -    by (rule semilat.plus_le_conv [THEN iffD1])
    7.54 +    by (rule Semilat.plus_le_conv [OF Semilat.intro, THEN iffD1])
    7.55    from prems show ?thesis
    7.56    apply (rule_tac iffI)
    7.57     apply clarify
    7.58     apply (drule OK_le_err_OK [THEN iffD2])
    7.59     apply (drule OK_le_err_OK [THEN iffD2])
    7.60 -   apply (drule semilat.lub[of _ _ _ "OK x" _ "OK y"])
    7.61 +   apply (drule Semilat.lub [OF Semilat.intro, of _ _ _ "OK x" _ "OK y"])
    7.62          apply assumption
    7.63         apply assumption
    7.64        apply simp
    7.65 @@ -283,10 +285,10 @@
    7.66    apply (rename_tac z)
    7.67    apply (subgoal_tac "OK z: err A")
    7.68    apply (drule eq_order_le)
    7.69 -    apply (erule semilat.orderI)
    7.70 +    apply (erule Semilat.orderI [OF Semilat.intro])
    7.71     apply (blast dest: plus_le_conv3) 
    7.72    apply (erule subst)
    7.73 -  apply (blast intro: semilat.closedI closedD)
    7.74 +  apply (blast intro: Semilat.closedI [OF Semilat.intro] closedD)
    7.75    done 
    7.76  qed
    7.77  
     8.1 --- a/src/HOL/MicroJava/BV/Kildall.thy	Fri Jul 25 12:03:31 2008 +0200
     8.2 +++ b/src/HOL/MicroJava/BV/Kildall.thy	Fri Jul 25 12:03:32 2008 +0200
     8.3 @@ -8,7 +8,9 @@
     8.4  
     8.5  header {* \isaheader{Kildall's Algorithm}\label{sec:Kildall} *}
     8.6  
     8.7 -theory Kildall imports SemilatAlg While_Combinator begin
     8.8 +theory Kildall
     8.9 +imports SemilatAlg While_Combinator
    8.10 +begin
    8.11  
    8.12  
    8.13  consts
    8.14 @@ -43,10 +45,10 @@
    8.15  "merges f (p'#ps) ss = (let (p,s) = p' in merges f ps (ss[p := s +_f ss!p]))"
    8.16  
    8.17  
    8.18 -lemmas [simp] = Let_def semilat.le_iff_plus_unchanged [symmetric]
    8.19 +lemmas [simp] = Let_def Semilat.le_iff_plus_unchanged [OF Semilat.intro, symmetric]
    8.20  
    8.21  
    8.22 -lemma (in semilat) nth_merges:
    8.23 +lemma (in Semilat) nth_merges:
    8.24   "\<And>ss. \<lbrakk>p < length ss; ss \<in> list n A; \<forall>(p,t)\<in>set ps. p<n \<and> t\<in>A \<rbrakk> \<Longrightarrow>
    8.25    (merges f ps ss)!p = map snd [(p',t') \<leftarrow> ps. p'=p] ++_f ss!p"
    8.26    (is "\<And>ss. \<lbrakk>_; _; ?steptype ps\<rbrakk> \<Longrightarrow> ?P ss ps")
    8.27 @@ -82,7 +84,7 @@
    8.28    by (induct_tac ps, auto)
    8.29  
    8.30  
    8.31 -lemma (in semilat) merges_preserves_type_lemma:
    8.32 +lemma (in Semilat) merges_preserves_type_lemma:
    8.33  shows "\<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>(p,x) \<in> set ps. p<n \<and> x\<in>A)
    8.34            \<longrightarrow> merges f ps xs \<in> list n A"
    8.35  apply (insert closedI)
    8.36 @@ -92,12 +94,12 @@
    8.37  apply clarsimp
    8.38  done
    8.39  
    8.40 -lemma (in semilat) merges_preserves_type [simp]:
    8.41 +lemma (in Semilat) merges_preserves_type [simp]:
    8.42   "\<lbrakk> xs \<in> list n A; \<forall>(p,x) \<in> set ps. p<n \<and> x\<in>A \<rbrakk>
    8.43    \<Longrightarrow> merges f ps xs \<in> list n A"
    8.44  by (simp add: merges_preserves_type_lemma)
    8.45  
    8.46 -lemma (in semilat) merges_incr_lemma:
    8.47 +lemma (in Semilat) merges_incr_lemma:
    8.48   "\<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>(p,x)\<in>set ps. p<size xs \<and> x \<in> A) \<longrightarrow> xs <=[r] merges f ps xs"
    8.49  apply (induct_tac ps)
    8.50   apply simp
    8.51 @@ -111,13 +113,13 @@
    8.52  apply (blast intro!: listE_set intro: closedD listE_length [THEN nth_in])
    8.53  done
    8.54  
    8.55 -lemma (in semilat) merges_incr:
    8.56 +lemma (in Semilat) merges_incr:
    8.57   "\<lbrakk> xs \<in> list n A; \<forall>(p,x)\<in>set ps. p<size xs \<and> x \<in> A \<rbrakk> 
    8.58    \<Longrightarrow> xs <=[r] merges f ps xs"
    8.59    by (simp add: merges_incr_lemma)
    8.60  
    8.61  
    8.62 -lemma (in semilat) merges_same_conv [rule_format]:
    8.63 +lemma (in Semilat) merges_same_conv [rule_format]:
    8.64   "(\<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>(p,x)\<in>set ps. p<size xs \<and> x\<in>A) \<longrightarrow> 
    8.65       (merges f ps xs = xs) = (\<forall>(p,x)\<in>set ps. x <=_r xs!p))"
    8.66    apply (induct_tac ps)
    8.67 @@ -150,7 +152,7 @@
    8.68    done
    8.69  
    8.70  
    8.71 -lemma (in semilat) list_update_le_listI [rule_format]:
    8.72 +lemma (in Semilat) list_update_le_listI [rule_format]:
    8.73    "set xs <= A \<longrightarrow> set ys <= A \<longrightarrow> xs <=[r] ys \<longrightarrow> p < size xs \<longrightarrow>  
    8.74     x <=_r ys!p \<longrightarrow> x\<in>A \<longrightarrow> xs[p := x +_f xs!p] <=[r] ys"
    8.75    apply(insert semilat)
    8.76 @@ -158,7 +160,7 @@
    8.77    apply (simp add: list_all2_conv_all_nth nth_list_update)
    8.78    done
    8.79  
    8.80 -lemma (in semilat) merges_pres_le_ub:
    8.81 +lemma (in Semilat) merges_pres_le_ub:
    8.82    assumes "set ts <= A" and "set ss <= A"
    8.83      and "\<forall>(p,t)\<in>set ps. t <=_r ts!p \<and> t \<in> A \<and> p < size ts" and "ss <=[r] ts"
    8.84    shows "merges f ps ss <=[r] ts"
    8.85 @@ -206,7 +208,7 @@
    8.86  
    8.87  (** iter **)
    8.88  
    8.89 -lemma (in semilat) stable_pres_lemma:
    8.90 +lemma (in Semilat) stable_pres_lemma:
    8.91  shows "\<lbrakk>pres_type step n A; bounded step n; 
    8.92       ss \<in> list n A; p \<in> w; \<forall>q\<in>w. q < n; 
    8.93       \<forall>q. q < n \<longrightarrow> q \<notin> w \<longrightarrow> stable r step ss q; q < n; 
    8.94 @@ -284,7 +286,7 @@
    8.95   done
    8.96  
    8.97  
    8.98 -lemma (in semilat) merges_bounded_lemma:
    8.99 +lemma (in Semilat) merges_bounded_lemma:
   8.100   "\<lbrakk> mono r step n A; bounded step n; 
   8.101      \<forall>(p',s') \<in> set (step p (ss!p)). s' \<in> A; ss \<in> list n A; ts \<in> list n A; p < n; 
   8.102      ss <=[r] ts; \<forall>p. p < n \<longrightarrow> stable r step ts p \<rbrakk> 
   8.103 @@ -319,7 +321,7 @@
   8.104    ss <[r] merges f qs ss \<or> 
   8.105    merges f qs ss = ss \<and> {q. \<exists>t. (q,t)\<in>set qs \<and> t +_f ss!q \<noteq> ss!q} Un (w-{p}) < w" (is "PROP ?P")
   8.106  proof -
   8.107 -  interpret semilat [A r f] by fact
   8.108 +  interpret Semilat [A r f] using assms by (rule Semilat.intro)
   8.109    show "PROP ?P" apply(insert semilat)
   8.110      apply (unfold lesssub_def)
   8.111      apply (simp (no_asm_simp) add: merges_incr)
   8.112 @@ -349,7 +351,7 @@
   8.113     (\<forall>ts\<in>list n A. ss0 <=[r] ts \<and> stables r step ts \<longrightarrow> ss' <=[r] ts)"
   8.114    (is "PROP ?P")
   8.115  proof -
   8.116 -  interpret semilat [A r f] by fact
   8.117 +  interpret Semilat [A r f] using assms by (rule Semilat.intro)
   8.118    show "PROP ?P" apply(insert semilat)
   8.119  apply (unfold iter_def stables_def)
   8.120  apply (rule_tac P = "%(ss,w).
   8.121 @@ -455,7 +457,7 @@
   8.122                   kildall r f step ss0 <=[r] ts)"
   8.123    (is "PROP ?P")
   8.124  proof -
   8.125 -  interpret semilat [A r f] by fact
   8.126 +  interpret Semilat [A r f] using assms by (rule Semilat.intro)
   8.127    show "PROP ?P"
   8.128  apply (unfold kildall_def)
   8.129  apply(case_tac "iter f step ss0 (unstables r step ss0)")
   8.130 @@ -472,7 +474,7 @@
   8.131    \<Longrightarrow> is_bcv r T step n A (kildall r f step)"
   8.132    (is "PROP ?P")
   8.133  proof -
   8.134 -  interpret semilat [A r f] by fact
   8.135 +  interpret Semilat [A r f] using assms by (rule Semilat.intro)
   8.136    show "PROP ?P"
   8.137  apply(unfold is_bcv_def wt_step_def)
   8.138  apply(insert semilat kildall_properties[of A])
     9.1 --- a/src/HOL/MicroJava/BV/LBVComplete.thy	Fri Jul 25 12:03:31 2008 +0200
     9.2 +++ b/src/HOL/MicroJava/BV/LBVComplete.thy	Fri Jul 25 12:03:32 2008 +0200
     9.3 @@ -25,7 +25,7 @@
     9.4  by (force simp: list_ex_iff is_target_def mem_iff)
     9.5  
     9.6  
     9.7 -locale (open) lbvc = lbv + 
     9.8 +locale lbvc = lbv + 
     9.9    fixes phi :: "'a list" ("\<phi>")
    9.10    fixes c   :: "'a list" 
    9.11    defines cert_def: "c \<equiv> make_cert step \<phi> \<bottom>"
    9.12 @@ -197,7 +197,7 @@
    9.13    have "merge c pc ?step (c!Suc pc) =
    9.14      (if \<forall>(pc',s')\<in>set ?step. pc'\<noteq>pc+1 \<longrightarrow> s' <=_r c!pc'
    9.15      then map snd [(p',t') \<leftarrow> ?step.p'=pc+1] ++_f c!Suc pc
    9.16 -    else \<top>)" by (rule merge_def)
    9.17 +    else \<top>)" unfolding merge_def by (rule lbv.merge_def [OF lbvc.axioms(1), OF lbvc_axioms])
    9.18    moreover {
    9.19      fix pc' s' assume s': "(pc', s') \<in> set ?step" and suc_pc: "pc' \<noteq> pc+1"
    9.20      with less have "s' <=_r \<phi>!pc'" by auto
    10.1 --- a/src/HOL/MicroJava/BV/LBVCorrect.thy	Fri Jul 25 12:03:31 2008 +0200
    10.2 +++ b/src/HOL/MicroJava/BV/LBVCorrect.thy	Fri Jul 25 12:03:32 2008 +0200
    10.3 @@ -6,9 +6,11 @@
    10.4  
    10.5  header {* \isaheader{Correctness of the LBV} *}
    10.6  
    10.7 -theory LBVCorrect imports LBVSpec Typing_Framework begin
    10.8 +theory LBVCorrect
    10.9 +imports LBVSpec Typing_Framework
   10.10 +begin
   10.11  
   10.12 -locale (open) lbvs = lbv +
   10.13 +locale lbvs = lbv +
   10.14    fixes s0  :: 'a ("s\<^sub>0")
   10.15    fixes c   :: "'a list"
   10.16    fixes ins :: "'b list"
    11.1 --- a/src/HOL/MicroJava/BV/LBVJVM.thy	Fri Jul 25 12:03:31 2008 +0200
    11.2 +++ b/src/HOL/MicroJava/BV/LBVJVM.thy	Fri Jul 25 12:03:32 2008 +0200
    11.3 @@ -122,7 +122,7 @@
    11.4    moreover
    11.5    from lbv have "0 < length ins" by (simp add: wt_lbv_def)
    11.6    ultimately
    11.7 -  show ?thesis by (rule lbvs.wtl_sound_strong)
    11.8 +  show ?thesis by (rule lbvs.wtl_sound_strong [OF lbvs.intro, OF lbv.intro lbvs_axioms.intro, OF Semilat.intro lbv_axioms.intro])
    11.9  qed
   11.10    
   11.11  lemma wt_lbv_wt_method:
   11.12 @@ -274,7 +274,7 @@
   11.13    note length 
   11.14    ultimately
   11.15    have "wtl_inst_list ins ?cert ?f ?r Err (OK None) ?step 0 ?start \<noteq> Err"
   11.16 -    by (rule lbvc.wtl_complete)
   11.17 +    by (rule lbvc.wtl_complete [OF lbvc.intro, OF lbv.intro lbvc_axioms.intro, OF Semilat.intro lbv_axioms.intro])
   11.18    moreover
   11.19    from 0 length have "phi \<noteq> []" by auto
   11.20    moreover
    12.1 --- a/src/HOL/MicroJava/BV/LBVSpec.thy	Fri Jul 25 12:03:31 2008 +0200
    12.2 +++ b/src/HOL/MicroJava/BV/LBVSpec.thy	Fri Jul 25 12:03:32 2008 +0200
    12.3 @@ -6,7 +6,9 @@
    12.4  
    12.5  header {* \isaheader{The Lightweight Bytecode Verifier} *}
    12.6  
    12.7 -theory LBVSpec imports SemilatAlg Opt begin
    12.8 +theory LBVSpec
    12.9 +imports SemilatAlg Opt
   12.10 +begin
   12.11  
   12.12  types
   12.13    's certificate = "'s list"   
   12.14 @@ -51,7 +53,7 @@
   12.15    "bottom r B \<equiv> \<forall>x. B <=_r x"
   12.16  
   12.17  
   12.18 -locale (open) lbv = semilat +
   12.19 +locale lbv = Semilat +
   12.20    fixes T :: "'a" ("\<top>") 
   12.21    fixes B :: "'a" ("\<bottom>") 
   12.22    fixes step :: "'a step_type" 
   12.23 @@ -118,7 +120,7 @@
   12.24  
   12.25  
   12.26  
   12.27 -lemma (in semilat) pp_ub1':
   12.28 +lemma (in Semilat) pp_ub1':
   12.29    assumes S: "snd`set S \<subseteq> A" 
   12.30    assumes y: "y \<in> A" and ab: "(a, b) \<in> set S" 
   12.31    shows "b <=_r map snd [(p', t') \<leftarrow> S . p' = a] ++_f y"
    13.1 --- a/src/HOL/MicroJava/BV/Listn.thy	Fri Jul 25 12:03:31 2008 +0200
    13.2 +++ b/src/HOL/MicroJava/BV/Listn.thy	Fri Jul 25 12:03:32 2008 +0200
    13.3 @@ -283,21 +283,21 @@
    13.4  done
    13.5  
    13.6  
    13.7 -lemma (in semilat) plus_list_ub1 [rule_format]:
    13.8 +lemma (in Semilat) plus_list_ub1 [rule_format]:
    13.9   "\<lbrakk> set xs <= A; set ys <= A; size xs = size ys \<rbrakk> 
   13.10    \<Longrightarrow> xs <=[r] xs +[f] ys"
   13.11  apply (unfold unfold_lesub_list)
   13.12  apply (simp add: Listn.le_def list_all2_conv_all_nth)
   13.13  done
   13.14  
   13.15 -lemma (in semilat) plus_list_ub2:
   13.16 +lemma (in Semilat) plus_list_ub2:
   13.17   "\<lbrakk>set xs <= A; set ys <= A; size xs = size ys \<rbrakk>
   13.18    \<Longrightarrow> ys <=[r] xs +[f] ys"
   13.19  apply (unfold unfold_lesub_list)
   13.20  apply (simp add: Listn.le_def list_all2_conv_all_nth)
   13.21  done
   13.22  
   13.23 -lemma (in semilat) plus_list_lub [rule_format]:
   13.24 +lemma (in Semilat) plus_list_lub [rule_format]:
   13.25  shows "!xs ys zs. set xs <= A \<longrightarrow> set ys <= A \<longrightarrow> set zs <= A 
   13.26    \<longrightarrow> size xs = n & size ys = n \<longrightarrow> 
   13.27    xs <=[r] zs & ys <=[r] zs \<longrightarrow> xs +[f] ys <=[r] zs"
   13.28 @@ -305,7 +305,7 @@
   13.29  apply (simp add: Listn.le_def list_all2_conv_all_nth)
   13.30  done
   13.31  
   13.32 -lemma (in semilat) list_update_incr [rule_format]:
   13.33 +lemma (in Semilat) list_update_incr [rule_format]:
   13.34   "x\<in> A \<Longrightarrow> set xs <= A \<longrightarrow> 
   13.35    (!i. i<size xs \<longrightarrow> xs <=[r] xs[i := x +_f xs!i])"
   13.36  apply (unfold unfold_lesub_list)
   13.37 @@ -380,7 +380,7 @@
   13.38  lemma Listn_sl_aux:
   13.39  assumes "semilat (A, r, f)" shows "semilat (Listn.sl n (A,r,f))"
   13.40  proof -
   13.41 -  interpret semilat [A r f] by fact
   13.42 +  interpret Semilat [A r f] using assms by (rule Semilat.intro)
   13.43  show ?thesis
   13.44  apply (unfold Listn.sl_def)
   13.45  apply (simp (no_asm) only: semilat_Def split_conv)
   13.46 @@ -517,9 +517,9 @@
   13.47  apply (unfold Err.sl_def)
   13.48  apply (simp only: split_conv)
   13.49  apply (simp (no_asm) only: semilat_Def plussub_def)
   13.50 -apply (simp (no_asm_simp) only: semilat.closedI closed_lift2_sup)
   13.51 +apply (simp (no_asm_simp) only: Semilat.closedI [OF Semilat.intro] closed_lift2_sup)
   13.52  apply (rule conjI)
   13.53 - apply (drule semilat.orderI)
   13.54 + apply (drule Semilat.orderI [OF Semilat.intro])
   13.55   apply simp
   13.56  apply (simp (no_asm) only: unfold_lesub_err Err.le_def err_def sup_def lift2_def)
   13.57  apply (simp (no_asm_simp) add: coalesce_eq_OK1_D coalesce_eq_OK2_D split: err.split)
    14.1 --- a/src/HOL/MicroJava/BV/Product.thy	Fri Jul 25 12:03:31 2008 +0200
    14.2 +++ b/src/HOL/MicroJava/BV/Product.thy	Fri Jul 25 12:03:32 2008 +0200
    14.3 @@ -8,7 +8,9 @@
    14.4  
    14.5  header {* \isaheader{Products as Semilattices} *}
    14.6  
    14.7 -theory Product imports Err begin
    14.8 +theory Product
    14.9 +imports Err
   14.10 +begin
   14.11  
   14.12  constdefs
   14.13   le :: "'a ord \<Rightarrow> 'b ord \<Rightarrow> ('a * 'b) ord"
   14.14 @@ -79,13 +81,13 @@
   14.15    have plus_le_conv2:
   14.16      "\<And>r f z. \<lbrakk> z : err A; semilat (err A, r, f); OK x : err A; OK y : err A;
   14.17                   OK x +_f OK y <=_r z\<rbrakk> \<Longrightarrow> OK x <=_r z \<and> OK y <=_r z"
   14.18 -    by (rule semilat.plus_le_conv [THEN iffD1])
   14.19 +    by (rule Semilat.plus_le_conv [OF Semilat.intro, THEN iffD1])
   14.20    from prems show ?thesis
   14.21    apply (rule_tac iffI)
   14.22     apply clarify
   14.23     apply (drule OK_le_err_OK [THEN iffD2])
   14.24     apply (drule OK_le_err_OK [THEN iffD2])
   14.25 -   apply (drule semilat.lub[of _ _ _ "OK x" _ "OK y"])
   14.26 +   apply (drule Semilat.lub [OF Semilat.intro, of _ _ _ "OK x" _ "OK y"])
   14.27          apply assumption
   14.28         apply assumption
   14.29        apply simp
   14.30 @@ -101,7 +103,7 @@
   14.31        apply simp
   14.32        apply blast
   14.33       apply simp
   14.34 -    apply (blast dest: semilat.orderI order_refl)
   14.35 +    apply (blast dest: Semilat.orderI [OF Semilat.intro] order_refl)
   14.36     apply blast
   14.37    apply (erule subst)
   14.38    apply (unfold semilat_def err_def closed_def)
   14.39 @@ -115,15 +117,15 @@
   14.40  apply (simp (no_asm_simp) only: split_tupled_all)
   14.41  apply simp
   14.42  apply (simp (no_asm) only: semilat_Def)
   14.43 -apply (simp (no_asm_simp) only: semilat.closedI closed_lift2_sup)
   14.44 +apply (simp (no_asm_simp) only: Semilat.closedI [OF Semilat.intro] closed_lift2_sup)
   14.45  apply (simp (no_asm) only: unfold_lesub_err Err.le_def unfold_plussub_lift2 sup_def)
   14.46  apply (auto elim: semilat_le_err_OK1 semilat_le_err_OK2
   14.47              simp add: lift2_def  split: err.split)
   14.48 -apply (blast dest: semilat.orderI)
   14.49 -apply (blast dest: semilat.orderI)
   14.50 +apply (blast dest: Semilat.orderI [OF Semilat.intro])
   14.51 +apply (blast dest: Semilat.orderI [OF Semilat.intro])
   14.52  
   14.53  apply (rule OK_le_err_OK [THEN iffD1])
   14.54 -apply (erule subst, subst OK_lift2_OK [symmetric], rule semilat.lub)
   14.55 +apply (erule subst, subst OK_lift2_OK [symmetric], rule Semilat.lub [OF Semilat.intro])
   14.56  apply simp
   14.57  apply simp
   14.58  apply simp
   14.59 @@ -132,7 +134,7 @@
   14.60  apply simp
   14.61  
   14.62  apply (rule OK_le_err_OK [THEN iffD1])
   14.63 -apply (erule subst, subst OK_lift2_OK [symmetric], rule semilat.lub)
   14.64 +apply (erule subst, subst OK_lift2_OK [symmetric], rule Semilat.lub [OF Semilat.intro])
   14.65  apply simp
   14.66  apply simp
   14.67  apply simp
    15.1 --- a/src/HOL/MicroJava/BV/Semilat.thy	Fri Jul 25 12:03:31 2008 +0200
    15.2 +++ b/src/HOL/MicroJava/BV/Semilat.thy	Fri Jul 25 12:03:32 2008 +0200
    15.3 @@ -71,7 +71,7 @@
    15.4   some_lub :: "'a ord \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a"
    15.5  "some_lub r x y == SOME z. is_lub r x y z";
    15.6  
    15.7 -locale (open) semilat =
    15.8 +locale Semilat =
    15.9    fixes A :: "'a set"
   15.10      and r :: "'a ord"
   15.11      and f :: "'a binop"
   15.12 @@ -122,11 +122,11 @@
   15.13  apply (rule refl [THEN eq_reflection])
   15.14  done
   15.15  
   15.16 -lemma (in semilat) orderI [simp, intro]:
   15.17 +lemma (in Semilat) orderI [simp, intro]:
   15.18    "order r"
   15.19    by (insert semilat) (simp add: semilat_Def)
   15.20  
   15.21 -lemma (in semilat) closedI [simp, intro]:
   15.22 +lemma (in Semilat) closedI [simp, intro]:
   15.23    "closed A f"
   15.24    by (insert semilat) (simp add: semilat_Def)
   15.25  
   15.26 @@ -138,41 +138,41 @@
   15.27    by (simp add: closed_def)
   15.28  
   15.29  
   15.30 -lemma (in semilat) closed_f [simp, intro]:
   15.31 +lemma (in Semilat) closed_f [simp, intro]:
   15.32    "\<lbrakk>x:A; y:A\<rbrakk>  \<Longrightarrow> x +_f y : A"
   15.33    by (simp add: closedD [OF closedI])
   15.34  
   15.35 -lemma (in semilat) refl_r [intro, simp]:
   15.36 +lemma (in Semilat) refl_r [intro, simp]:
   15.37    "x <=_r x"
   15.38    by simp
   15.39  
   15.40 -lemma (in semilat) antisym_r [intro?]:
   15.41 +lemma (in Semilat) antisym_r [intro?]:
   15.42    "\<lbrakk> x <=_r y; y <=_r x \<rbrakk> \<Longrightarrow> x = y"
   15.43    by (rule order_antisym) auto
   15.44    
   15.45 -lemma (in semilat) trans_r [trans, intro?]:
   15.46 +lemma (in Semilat) trans_r [trans, intro?]:
   15.47    "\<lbrakk>x <=_r y; y <=_r z\<rbrakk> \<Longrightarrow> x <=_r z"
   15.48    by (auto intro: order_trans)    
   15.49    
   15.50  
   15.51 -lemma (in semilat) ub1 [simp, intro?]:
   15.52 +lemma (in Semilat) ub1 [simp, intro?]:
   15.53    "\<lbrakk> x:A; y:A \<rbrakk> \<Longrightarrow> x <=_r x +_f y"
   15.54    by (insert semilat) (unfold semilat_Def, simp)
   15.55  
   15.56 -lemma (in semilat) ub2 [simp, intro?]:
   15.57 +lemma (in Semilat) ub2 [simp, intro?]:
   15.58    "\<lbrakk> x:A; y:A \<rbrakk> \<Longrightarrow> y <=_r x +_f y"
   15.59    by (insert semilat) (unfold semilat_Def, simp)
   15.60  
   15.61 -lemma (in semilat) lub [simp, intro?]:
   15.62 +lemma (in Semilat) lub [simp, intro?]:
   15.63   "\<lbrakk> x <=_r z; y <=_r z; x:A; y:A; z:A \<rbrakk> \<Longrightarrow> x +_f y <=_r z";
   15.64    by (insert semilat) (unfold semilat_Def, simp)
   15.65  
   15.66  
   15.67 -lemma (in semilat) plus_le_conv [simp]:
   15.68 +lemma (in Semilat) plus_le_conv [simp]:
   15.69    "\<lbrakk> x:A; y:A; z:A \<rbrakk> \<Longrightarrow> (x +_f y <=_r z) = (x <=_r z & y <=_r z)"
   15.70    by (blast intro: ub1 ub2 lub order_trans)
   15.71  
   15.72 -lemma (in semilat) le_iff_plus_unchanged:
   15.73 +lemma (in Semilat) le_iff_plus_unchanged:
   15.74    "\<lbrakk> x:A; y:A \<rbrakk> \<Longrightarrow> (x <=_r y) = (x +_f y = y)"
   15.75  apply (rule iffI)
   15.76   apply (blast intro: antisym_r refl_r lub ub2)
   15.77 @@ -180,7 +180,7 @@
   15.78  apply simp
   15.79  done
   15.80  
   15.81 -lemma (in semilat) le_iff_plus_unchanged2:
   15.82 +lemma (in Semilat) le_iff_plus_unchanged2:
   15.83    "\<lbrakk> x:A; y:A \<rbrakk> \<Longrightarrow> (x <=_r y) = (y +_f x = y)"
   15.84  apply (rule iffI)
   15.85   apply (blast intro: order_antisym lub order_refl ub1)
   15.86 @@ -189,7 +189,7 @@
   15.87  done 
   15.88  
   15.89  
   15.90 -lemma (in semilat) plus_assoc [simp]:
   15.91 +lemma (in Semilat) plus_assoc [simp]:
   15.92    assumes a: "a \<in> A" and b: "b \<in> A" and c: "c \<in> A"
   15.93    shows "a +_f (b +_f c) = a +_f b +_f c"
   15.94  proof -
   15.95 @@ -227,7 +227,7 @@
   15.96    qed
   15.97  qed
   15.98  
   15.99 -lemma (in semilat) plus_com_lemma:
  15.100 +lemma (in Semilat) plus_com_lemma:
  15.101    "\<lbrakk>a \<in> A; b \<in> A\<rbrakk> \<Longrightarrow> a +_f b <=_r b +_f a"
  15.102  proof -
  15.103    assume a: "a \<in> A" and b: "b \<in> A"  
  15.104 @@ -238,7 +238,7 @@
  15.105    ultimately show ?thesis ..
  15.106  qed
  15.107  
  15.108 -lemma (in semilat) plus_commutative:
  15.109 +lemma (in Semilat) plus_commutative:
  15.110    "\<lbrakk>a \<in> A; b \<in> A\<rbrakk> \<Longrightarrow> a +_f b = b +_f a"
  15.111  by(blast intro: order_antisym plus_com_lemma)
  15.112  
    16.1 --- a/src/HOL/MicroJava/BV/SemilatAlg.thy	Fri Jul 25 12:03:31 2008 +0200
    16.2 +++ b/src/HOL/MicroJava/BV/SemilatAlg.thy	Fri Jul 25 12:03:32 2008 +0200
    16.3 @@ -6,7 +6,9 @@
    16.4  
    16.5  header {* \isaheader{More on Semilattices} *}
    16.6  
    16.7 -theory SemilatAlg imports Typing_Framework Product begin
    16.8 +theory SemilatAlg
    16.9 +imports Typing_Framework Product
   16.10 +begin
   16.11  
   16.12  
   16.13  constdefs 
   16.14 @@ -65,7 +67,7 @@
   16.15  lemma plusplus_closed: assumes "semilat (A, r, f)" shows
   16.16    "\<And>y. \<lbrakk> set x \<subseteq> A; y \<in> A\<rbrakk> \<Longrightarrow> x ++_f y \<in> A" (is "PROP ?P")
   16.17  proof -
   16.18 -  interpret semilat [A r f] by fact
   16.19 +  interpret Semilat [A r f] using assms by (rule Semilat.intro)
   16.20    show "PROP ?P" proof (induct x)
   16.21      show "\<And>y. y \<in> A \<Longrightarrow> [] ++_f y \<in> A" by simp
   16.22      fix y x xs
   16.23 @@ -78,7 +80,7 @@
   16.24    qed
   16.25  qed
   16.26  
   16.27 -lemma (in semilat) pp_ub2:
   16.28 +lemma (in Semilat) pp_ub2:
   16.29   "\<And>y. \<lbrakk> set x \<subseteq> A; y \<in> A\<rbrakk> \<Longrightarrow> y <=_r x ++_f y"
   16.30  proof (induct x)
   16.31    from semilat show "\<And>y. y <=_r [] ++_f y" by simp
   16.32 @@ -98,7 +100,7 @@
   16.33  qed
   16.34  
   16.35  
   16.36 -lemma (in semilat) pp_ub1:
   16.37 +lemma (in Semilat) pp_ub1:
   16.38  shows "\<And>y. \<lbrakk>set ls \<subseteq> A; y \<in> A; x \<in> set ls\<rbrakk> \<Longrightarrow> x <=_r ls ++_f y"
   16.39  proof (induct ls)
   16.40    show "\<And>y. x \<in> set [] \<Longrightarrow> x <=_r [] ++_f y" by simp
   16.41 @@ -134,7 +136,7 @@
   16.42  qed
   16.43  
   16.44  
   16.45 -lemma (in semilat) pp_lub:
   16.46 +lemma (in Semilat) pp_lub:
   16.47    assumes z: "z \<in> A"
   16.48    shows 
   16.49    "\<And>y. y \<in> A \<Longrightarrow> set xs \<subseteq> A \<Longrightarrow> \<forall>x \<in> set xs. x <=_r z \<Longrightarrow> y <=_r z \<Longrightarrow> xs ++_f y <=_r z"
   16.50 @@ -162,7 +164,7 @@
   16.51    shows "\<lbrakk>\<forall>(p,s) \<in> set S. s \<in> A; y \<in> A; (a,b) \<in> set S\<rbrakk> 
   16.52    \<Longrightarrow> b <=_r map snd [(p', t')\<leftarrow>S. p' = a] ++_f y" 
   16.53  proof -
   16.54 -  interpret semilat [A r f] by fact
   16.55 +  interpret Semilat [A r f] using assms by (rule Semilat.intro)
   16.56  
   16.57    let "b <=_r ?map ++_f y" = ?thesis
   16.58  
    17.1 --- a/src/HOL/NSA/Filter.thy	Fri Jul 25 12:03:31 2008 +0200
    17.2 +++ b/src/HOL/NSA/Filter.thy	Fri Jul 25 12:03:32 2008 +0200
    17.3 @@ -196,7 +196,7 @@
    17.4  subsection {* Ultrafilter Theorem *}
    17.5  
    17.6  text "A locale makes proof of ultrafilter Theorem more modular"
    17.7 -locale (open) UFT =
    17.8 +locale UFT =
    17.9    fixes   frechet :: "'a set set"
   17.10    and     superfrechet :: "'a set set set"
   17.11  
   17.12 @@ -402,7 +402,7 @@
   17.13    qed
   17.14  qed
   17.15  
   17.16 -lemmas freeultrafilter_Ex = UFT.freeultrafilter_ex
   17.17 +lemmas freeultrafilter_Ex = UFT.freeultrafilter_ex [OF UFT.intro]
   17.18  
   17.19  hide (open) const filter
   17.20  
    18.1 --- a/src/HOL/Statespace/state_space.ML	Fri Jul 25 12:03:31 2008 +0200
    18.2 +++ b/src/HOL/Statespace/state_space.ML	Fri Jul 25 12:03:32 2008 +0200
    18.3 @@ -312,7 +312,7 @@
    18.4                        ([]))])];
    18.5  
    18.6    in thy
    18.7 -     |> Locale.add_locale_i (SOME "") name vars [assumes]
    18.8 +     |> Locale.add_locale_i "" name vars [assumes]
    18.9       ||> ProofContext.theory_of
   18.10       ||> interprete_parent name dist_thm_full_name parent_expr
   18.11       |> #2
   18.12 @@ -459,11 +459,11 @@
   18.13             (suffix namespaceN name) nameT parents_expr
   18.14             (map fst parent_comps) (map fst components)
   18.15       |> Context.theory_map (add_statespace full_name args parents components [])
   18.16 -     |> Locale.add_locale_i (SOME "") (suffix valuetypesN name) (Locale.Merge locs)
   18.17 +     |> Locale.add_locale_i "" (suffix valuetypesN name) (Locale.Merge locs)
   18.18              [Element.Constrains constrains]
   18.19       |> ProofContext.theory_of o #2
   18.20       |> fold interprete_parent_valuetypes parents
   18.21 -     |> Locale.add_locale (SOME "") name
   18.22 +     |> Locale.add_locale "" name
   18.23                (Locale.Merge [Locale.Locale (suffix namespaceN full_name)
   18.24                              ,Locale.Locale (suffix valuetypesN full_name)]) fixestate
   18.25       |> ProofContext.theory_of o #2
    19.1 --- a/src/HOL/ex/Tarski.thy	Fri Jul 25 12:03:31 2008 +0200
    19.2 +++ b/src/HOL/ex/Tarski.thy	Fri Jul 25 12:03:32 2008 +0200
    19.3 @@ -5,7 +5,9 @@
    19.4  
    19.5  header {* The Full Theorem of Tarski *}
    19.6  
    19.7 -theory Tarski imports Main FuncSet begin
    19.8 +theory Tarski
    19.9 +imports Main FuncSet
   19.10 +begin
   19.11  
   19.12  text {*
   19.13    Minimal version of lattice theory plus the full theorem of Tarski:
   19.14 @@ -81,8 +83,8 @@
   19.15                          (\<forall>S. S \<subseteq> pset cl --> (\<exists>G. isGlb S cl G))}"
   19.16  
   19.17  definition
   19.18 -  CLF :: "('a potype * ('a => 'a)) set" where
   19.19 -  "CLF = (SIGMA cl: CompleteLattice.
   19.20 +  CLF_set :: "('a potype * ('a => 'a)) set" where
   19.21 +  "CLF_set = (SIGMA cl: CompleteLattice.
   19.22              {f. f: pset cl -> pset cl & monotone f (pset cl) (order cl)})"
   19.23  
   19.24  definition
   19.25 @@ -105,25 +107,36 @@
   19.26    dual :: "'a potype => 'a potype" where
   19.27    "dual po = (| pset = pset po, order = converse (order po) |)"
   19.28  
   19.29 -locale (open) PO =
   19.30 +locale S =
   19.31    fixes cl :: "'a potype"
   19.32      and A  :: "'a set"
   19.33      and r  :: "('a * 'a) set"
   19.34 -  assumes cl_po:  "cl : PartialOrder"
   19.35    defines A_def: "A == pset cl"
   19.36       and  r_def: "r == order cl"
   19.37  
   19.38 -locale (open) CL = PO +
   19.39 +locale PO = S +
   19.40 +  assumes cl_po:  "cl : PartialOrder"
   19.41 +
   19.42 +locale CL = S +
   19.43    assumes cl_co:  "cl : CompleteLattice"
   19.44  
   19.45 -locale (open) CLF = CL +
   19.46 +interpretation CL < PO
   19.47 +apply (simp_all add: A_def r_def)
   19.48 +apply unfold_locales
   19.49 +using cl_co unfolding CompleteLattice_def by auto
   19.50 +
   19.51 +locale CLF = S +
   19.52    fixes f :: "'a => 'a"
   19.53      and P :: "'a set"
   19.54 -  assumes f_cl:  "(cl,f) : CLF" (*was the equivalent "f : CLF``{cl}"*)
   19.55 +  assumes f_cl:  "(cl,f) : CLF_set" (*was the equivalent "f : CLF_set``{cl}"*)
   19.56    defines P_def: "P == fix f A"
   19.57  
   19.58 +interpretation CLF < CL
   19.59 +apply (simp_all add: A_def r_def)
   19.60 +apply unfold_locales
   19.61 +using f_cl unfolding CLF_set_def by auto
   19.62  
   19.63 -locale (open) Tarski = CLF +
   19.64 +locale Tarski = CLF +
   19.65    fixes Y     :: "'a set"
   19.66      and intY1 :: "'a set"
   19.67      and v     :: "'a"
   19.68 @@ -138,17 +151,24 @@
   19.69  
   19.70  subsection {* Partial Order *}
   19.71  
   19.72 -lemma (in PO) PO_imp_refl: "refl A r"
   19.73 +lemma (in PO) dual:
   19.74 +  "PO (dual cl)"
   19.75 +apply unfold_locales
   19.76 +using cl_po
   19.77 +unfolding PartialOrder_def dual_def
   19.78 +by auto
   19.79 +
   19.80 +lemma (in PO) PO_imp_refl [simp]: "refl A r"
   19.81  apply (insert cl_po)
   19.82  apply (simp add: PartialOrder_def A_def r_def)
   19.83  done
   19.84  
   19.85 -lemma (in PO) PO_imp_sym: "antisym r"
   19.86 +lemma (in PO) PO_imp_sym [simp]: "antisym r"
   19.87  apply (insert cl_po)
   19.88  apply (simp add: PartialOrder_def r_def)
   19.89  done
   19.90  
   19.91 -lemma (in PO) PO_imp_trans: "trans r"
   19.92 +lemma (in PO) PO_imp_trans [simp]: "trans r"
   19.93  apply (insert cl_po)
   19.94  apply (simp add: PartialOrder_def r_def)
   19.95  done
   19.96 @@ -242,9 +262,9 @@
   19.97  
   19.98  lemmas CL_imp_PO = CL_subset_PO [THEN subsetD]
   19.99  
  19.100 -declare CL_imp_PO [THEN PO.PO_imp_refl, simp]
  19.101 +(*declare CL_imp_PO [THEN PO.PO_imp_refl, simp]
  19.102  declare CL_imp_PO [THEN PO.PO_imp_sym, simp]
  19.103 -declare CL_imp_PO [THEN PO.PO_imp_trans, simp]
  19.104 +declare CL_imp_PO [THEN PO.PO_imp_trans, simp]*)
  19.105  
  19.106  lemma (in CL) CO_refl: "refl A r"
  19.107  by (rule PO_imp_refl)
  19.108 @@ -287,11 +307,15 @@
  19.109  apply (fold r_def, fast)
  19.110  done
  19.111  
  19.112 +lemma (in PO) trans:
  19.113 +  "(x, y) \<in> r \<Longrightarrow> (y, z) \<in> r \<Longrightarrow> (x, z) \<in> r"
  19.114 +using cl_po apply (auto simp add: PartialOrder_def r_def)
  19.115 +unfolding trans_def by blast 
  19.116 +
  19.117  lemma (in PO) interval_not_empty:
  19.118 -     "[| trans r; interval r a b \<noteq> {} |] ==> (a, b) \<in> r"
  19.119 +  "interval r a b \<noteq> {} ==> (a, b) \<in> r"
  19.120  apply (simp add: interval_def)
  19.121 -apply (unfold trans_def, blast)
  19.122 -done
  19.123 +using trans by blast
  19.124  
  19.125  lemma (in PO) interval_imp_mem: "x \<in> interval r a b ==> (a, x) \<in> r"
  19.126  by (simp add: interval_def)
  19.127 @@ -322,6 +346,13 @@
  19.128        ==> S <<= cl"
  19.129  by (simp add: sublattice_def A_def r_def)
  19.130  
  19.131 +lemma (in CL) dual:
  19.132 +  "CL (dual cl)"
  19.133 +apply unfold_locales
  19.134 +using cl_co unfolding CompleteLattice_def
  19.135 +apply (simp add: dualPO isGlb_dual_isLub [symmetric] isLub_dual_isGlb [symmetric] dualA_iff)
  19.136 +done
  19.137 +
  19.138  
  19.139  subsection {* lub *}
  19.140  
  19.141 @@ -396,8 +427,7 @@
  19.142  apply (simp add: A_def)
  19.143  apply (rule dualA_iff [THEN subst])
  19.144  apply (rule CL.lub_in_lattice)
  19.145 -apply (rule dualPO)
  19.146 -apply (rule CL_dualCL)
  19.147 +apply (rule dual)
  19.148  apply (simp add: dualA_iff)
  19.149  done
  19.150  
  19.151 @@ -406,8 +436,7 @@
  19.152  apply (simp add: r_def)
  19.153  apply (rule dualr_iff [THEN subst])
  19.154  apply (rule CL.lub_upper)
  19.155 -apply (rule dualPO)
  19.156 -apply (rule CL_dualCL)
  19.157 +apply (rule dual)
  19.158  apply (simp add: dualA_iff A_def, assumption)
  19.159  done
  19.160  
  19.161 @@ -419,7 +448,7 @@
  19.162  lemma (in CLF) [simp]:
  19.163      "f: pset cl -> pset cl & monotone f (pset cl) (order cl)"
  19.164  apply (insert f_cl)
  19.165 -apply (simp add: CLF_def)
  19.166 +apply (simp add: CLF_set_def)
  19.167  done
  19.168  
  19.169  declare (in CLF) f_cl [simp]
  19.170 @@ -431,11 +460,17 @@
  19.171  lemma (in CLF) monotone_f: "monotone f A r"
  19.172  by (simp add: A_def r_def)
  19.173  
  19.174 -lemma (in CLF) CLF_dual: "(dual cl, f) \<in> CLF"
  19.175 -apply (simp add: CLF_def  CL_dualCL monotone_dual)
  19.176 +lemma (in CLF) CLF_dual: "(dual cl, f) \<in> CLF_set"
  19.177 +apply (simp add: CLF_set_def  CL_dualCL monotone_dual)
  19.178  apply (simp add: dualA_iff)
  19.179  done
  19.180  
  19.181 +lemma (in CLF) dual:
  19.182 +  "CLF (dual cl) f"
  19.183 +apply (rule CLF.intro)
  19.184 +apply (rule CLF_dual)
  19.185 +done
  19.186 +
  19.187  
  19.188  subsection {* fixed points *}
  19.189  
  19.190 @@ -534,16 +569,14 @@
  19.191  apply (simp add: glb_dual_lub P_def A_def r_def)
  19.192  apply (rule dualA_iff [THEN subst])
  19.193  apply (rule CLF.lubH_is_fixp)
  19.194 -apply (rule dualPO)
  19.195 -apply (rule CL_dualCL)
  19.196 -apply (rule CLF_dual)
  19.197 +apply (rule dual)
  19.198  apply (simp add: dualr_iff dualA_iff)
  19.199  done
  19.200  
  19.201  lemma (in CLF) T_thm_1_glb: "glb P cl = glb {x. (f x, x) \<in> r & x \<in> A} cl"
  19.202  apply (simp add: glb_dual_lub P_def A_def r_def)
  19.203  apply (rule dualA_iff [THEN subst])
  19.204 -apply (simp add: CLF.T_thm_1_lub [of _ f, OF dualPO CL_dualCL]
  19.205 +apply (simp add: CLF.T_thm_1_lub [of _ f, OF dual]
  19.206                   dualPO CL_dualCL CLF_dual dualr_iff)
  19.207  done
  19.208  
  19.209 @@ -603,8 +636,8 @@
  19.210       "[| a \<in> A; b \<in> A; interval r a b \<noteq> {}; S \<subseteq> interval r a b; isGlb S cl G;
  19.211           S \<noteq> {} |] ==> G \<in> interval r a b"
  19.212  apply (simp add: interval_dual)
  19.213 -apply (simp add: CLF.L_in_interval [of _ f]
  19.214 -                 dualA_iff A_def dualPO CL_dualCL CLF_dual isGlb_dual_isLub)
  19.215 +apply (simp add: CLF.L_in_interval [of _ f, OF dual]
  19.216 +                 dualA_iff A_def isGlb_dual_isLub)
  19.217  done
  19.218  
  19.219  lemma (in CLF) intervalPO:
  19.220 @@ -655,7 +688,6 @@
  19.221  apply (rule conjI)
  19.222  apply (rule reflE, assumption)
  19.223  apply (rule interval_not_empty)
  19.224 -apply (rule CO_trans)
  19.225  apply (simp add: interval_def)
  19.226  -- {* @{text "S \<noteq> {}"} *}
  19.227  apply simp
  19.228 @@ -700,7 +732,7 @@
  19.229  lemma (in CLF) Top_in_lattice: "Top cl \<in> A"
  19.230  apply (simp add: Top_dual_Bot A_def)
  19.231  apply (rule dualA_iff [THEN subst])
  19.232 -apply (blast intro!: CLF.Bot_in_lattice dualPO CL_dualCL CLF_dual)
  19.233 +apply (rule CLF.Bot_in_lattice [OF dual])
  19.234  done
  19.235  
  19.236  lemma (in CLF) Top_prop: "x \<in> A ==> (x, Top cl) \<in> r"
  19.237 @@ -714,8 +746,8 @@
  19.238  lemma (in CLF) Bot_prop: "x \<in> A ==> (Bot cl, x) \<in> r"
  19.239  apply (simp add: Bot_dual_Top r_def)
  19.240  apply (rule dualr_iff [THEN subst])
  19.241 -apply (simp add: CLF.Top_prop [of _ f]
  19.242 -                 dualA_iff A_def dualPO CL_dualCL CLF_dual)
  19.243 +apply (rule CLF.Top_prop [OF dual])
  19.244 +apply (simp add: dualA_iff A_def)
  19.245  done
  19.246  
  19.247  lemma (in CLF) Top_intv_not_empty: "x \<in> A  ==> interval r x (Top cl) \<noteq> {}"
  19.248 @@ -731,9 +763,9 @@
  19.249  prefer 2 apply assumption
  19.250  apply (simp add: A_def)
  19.251  apply (rule dualA_iff [THEN subst])
  19.252 -apply (blast intro!: CLF.Top_in_lattice dualPO CL_dualCL CLF_dual)
  19.253 -apply (simp add: CLF.Top_intv_not_empty [of _ f]
  19.254 -                 dualA_iff A_def dualPO CL_dualCL CLF_dual)
  19.255 +apply (rule CLF.Top_in_lattice [OF dual])
  19.256 +apply (rule CLF.Top_intv_not_empty [OF dual])
  19.257 +apply (simp add: dualA_iff A_def)
  19.258  done
  19.259  
  19.260  subsection {* fixed points form a partial order *}
  19.261 @@ -817,8 +849,12 @@
  19.262  apply (unfold P_def)
  19.263  apply (rule_tac A = "intY1" in fixf_subset)
  19.264  apply (rule intY1_subset)
  19.265 -apply (simp add: CLF.glbH_is_fixp [OF _ intY1_is_cl, simplified]
  19.266 -                 v_def CL_imp_PO intY1_is_cl CLF_def intY1_func intY1_mono)
  19.267 +unfolding v_def
  19.268 +apply (rule CLF.glbH_is_fixp [OF CLF.intro, unfolded CLF_set_def, of "\<lparr>pset = intY1, order = induced intY1 r\<rparr>", simplified])
  19.269 +apply auto
  19.270 +apply (rule intY1_is_cl)
  19.271 +apply (rule intY1_func)
  19.272 +apply (rule intY1_mono)
  19.273  done
  19.274  
  19.275  lemma (in Tarski) z_in_interval:
  19.276 @@ -859,17 +895,15 @@
  19.277  apply (rule_tac b = "Top cl" in interval_imp_mem)
  19.278  apply (simp add: v_def)
  19.279  apply (fold intY1_def)
  19.280 -apply (rule CL.glb_in_lattice [OF _ intY1_is_cl, simplified])
  19.281 - apply (simp add: CL_imp_PO intY1_is_cl, force)
  19.282 --- {* @{text v} is LEAST ub *}
  19.283 -apply clarify
  19.284 +apply (rule CL.glb_in_lattice [OF CL.intro [OF intY1_is_cl], simplified])
  19.285 +apply auto
  19.286  apply (rule indI)
  19.287    prefer 3 apply assumption
  19.288   prefer 2 apply (simp add: v_in_P)
  19.289  apply (unfold v_def)
  19.290  apply (rule indE)
  19.291  apply (rule_tac [2] intY1_subset)
  19.292 -apply (rule CL.glb_lower [OF _ intY1_is_cl, simplified])
  19.293 +apply (rule CL.glb_lower [OF CL.intro [OF intY1_is_cl], simplified])
  19.294    apply (simp add: CL_imp_PO intY1_is_cl)
  19.295   apply force
  19.296  apply (simp add: induced_def intY1_f_closed z_in_interval)
  19.297 @@ -888,7 +922,7 @@
  19.298  apply (rule CompleteLatticeI_simp)
  19.299  apply (rule fixf_po, clarify)
  19.300  apply (simp add: P_def A_def r_def)
  19.301 -apply (blast intro!: Tarski.tarski_full_lemma cl_po cl_co f_cl)
  19.302 -done
  19.303 +apply (rule Tarski.tarski_full_lemma [OF Tarski.intro [OF _ Tarski_axioms.intro]])
  19.304 +proof - show "CLF cl f" by unfold_locales qed
  19.305  
  19.306  end
    20.1 --- a/src/HOLCF/Deflation.thy	Fri Jul 25 12:03:31 2008 +0200
    20.2 +++ b/src/HOLCF/Deflation.thy	Fri Jul 25 12:03:32 2008 +0200
    20.3 @@ -323,7 +323,7 @@
    20.4   apply (erule ep_pair.e_p_less)
    20.5  done
    20.6  
    20.7 -locale (open) pcpo_ep_pair = ep_pair +
    20.8 +locale pcpo_ep_pair = ep_pair +
    20.9    constrains e :: "'a::pcpo \<rightarrow> 'b::pcpo"
   20.10    constrains p :: "'b::pcpo \<rightarrow> 'a::pcpo"
   20.11  begin
    21.1 --- a/src/Pure/Isar/isar_syn.ML	Fri Jul 25 12:03:31 2008 +0200
    21.2 +++ b/src/Pure/Isar/isar_syn.ML	Fri Jul 25 12:03:32 2008 +0200
    21.3 @@ -387,11 +387,10 @@
    21.4  
    21.5  val _ =
    21.6    OuterSyntax.command "locale" "define named proof context" K.thy_decl
    21.7 -    ((P.opt_keyword "open" >> (fn true => NONE | false => SOME "")) --
    21.8 -      P.name -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (Locale.empty, []) -- P.opt_begin
    21.9 -      >> (fn (((is_open, name), (expr, elems)), begin) =>
   21.10 +    (P.name -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (Locale.empty, []) -- P.opt_begin
   21.11 +      >> (fn ((name, (expr, elems)), begin) =>
   21.12            (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
   21.13 -            (Locale.add_locale is_open name expr elems #-> TheoryTarget.begin)));
   21.14 +            (Locale.add_locale "" name expr elems #-> TheoryTarget.begin)));
   21.15  
   21.16  val _ =
   21.17    OuterSyntax.command "interpretation"
    22.1 --- a/src/Pure/Isar/locale.ML	Fri Jul 25 12:03:31 2008 +0200
    22.2 +++ b/src/Pure/Isar/locale.ML	Fri Jul 25 12:03:32 2008 +0200
    22.3 @@ -81,9 +81,9 @@
    22.4    val print_locale: theory -> bool -> expr -> Element.context list -> unit
    22.5    val print_registrations: bool -> string -> Proof.context -> unit
    22.6  
    22.7 -  val add_locale: string option -> bstring -> expr -> Element.context list -> theory
    22.8 +  val add_locale: string -> bstring -> expr -> Element.context list -> theory
    22.9      -> string * Proof.context
   22.10 -  val add_locale_i: string option -> bstring -> expr -> Element.context_i list -> theory
   22.11 +  val add_locale_i: string -> bstring -> expr -> Element.context_i list -> theory
   22.12      -> string * Proof.context
   22.13  
   22.14    (* Tactics *)
   22.15 @@ -122,27 +122,11 @@
   22.16  
   22.17  (* legacy operations *)
   22.18  
   22.19 -fun gen_merge_lists _ xs [] = xs
   22.20 -  | gen_merge_lists _ [] ys = ys
   22.21 -  | gen_merge_lists eq xs ys = xs @ filter_out (member eq xs) ys;
   22.22 -
   22.23 -fun merge_lists xs ys = gen_merge_lists (op =) xs ys;
   22.24 -fun merge_alists xs = gen_merge_lists (eq_fst (op =)) xs;
   22.25 -
   22.26 -fun legacy_unvarifyT thm =
   22.27 -  let
   22.28 -    val cT = Thm.ctyp_of (Thm.theory_of_thm thm);
   22.29 -    val tvars = rev (Thm.fold_terms Term.add_tvars thm []);
   22.30 -    val tfrees = map (fn ((x, _), S) => SOME (cT (TFree (x, S)))) tvars;
   22.31 -  in Drule.instantiate' tfrees [] thm end;
   22.32 -
   22.33 -fun legacy_unvarify raw_thm =
   22.34 -  let
   22.35 -    val thm = legacy_unvarifyT raw_thm;
   22.36 -    val ct = Thm.cterm_of (Thm.theory_of_thm thm);
   22.37 -    val vars = rev (Thm.fold_terms Term.add_vars thm []);
   22.38 -    val frees = map (fn ((x, _), T) => SOME (ct (Free (x, T)))) vars;
   22.39 -  in Drule.instantiate' [] frees thm end;
   22.40 +fun merge_lists _ xs [] = xs
   22.41 +  | merge_lists _ [] ys = ys
   22.42 +  | merge_lists eq xs ys = xs @ filter_out (member eq xs) ys;
   22.43 +
   22.44 +fun merge_alists eq xs = merge_lists (eq_fst eq) xs;
   22.45  
   22.46  
   22.47  (** locale elements and expressions **)
   22.48 @@ -370,13 +354,13 @@
   22.49        {elems = elems', decls = (decls1', decls2'), regs = regs', ...}: locale) =
   22.50       {axiom = axiom,
   22.51        imports = imports,
   22.52 -      elems = gen_merge_lists (eq_snd (op =)) elems elems',
   22.53 +      elems = merge_lists (eq_snd (op =)) elems elems',
   22.54        params = params,
   22.55        lparams = lparams,
   22.56        decls =
   22.57         (Library.merge (eq_snd (op =)) (decls1, decls1'),
   22.58          Library.merge (eq_snd (op =)) (decls2, decls2')),
   22.59 -      regs = merge_alists regs regs',
   22.60 +      regs = merge_alists (op =) regs regs',
   22.61        intros = intros,
   22.62        dests = dests};
   22.63    fun merge _ ((space1, locs1), (space2, locs2)) =
   22.64 @@ -398,29 +382,18 @@
   22.65  
   22.66  (** access locales **)
   22.67  
   22.68 -fun print_locales thy =
   22.69 -  let val (space, locs) = LocalesData.get thy in
   22.70 -    Pretty.strs ("locales:" :: map #1 (NameSpace.extern_table (space, locs)))
   22.71 -    |> Pretty.writeln
   22.72 -  end;
   22.73 -
   22.74  val intern = NameSpace.intern o #1 o LocalesData.get;
   22.75  val extern = NameSpace.extern o #1 o LocalesData.get;
   22.76  
   22.77 -fun declare_locale name thy =
   22.78 +fun get_locale thy name = Symtab.lookup (#2 (LocalesData.get thy)) name;
   22.79 +
   22.80 +fun the_locale thy name = case get_locale thy name
   22.81 + of SOME loc => loc
   22.82 +  | NONE => error ("Unknown locale " ^ quote name);
   22.83 +
   22.84 +fun add_locale name loc thy =
   22.85    thy |> LocalesData.map (fn (space, locs) =>
   22.86 -    (Sign.declare_name thy name space, locs));
   22.87 -
   22.88 -fun put_locale name loc =
   22.89 -  LocalesData.map (fn (space, locs) =>
   22.90 -    (space, Symtab.update (name, loc) locs));
   22.91 -
   22.92 -fun get_locale thy name = Symtab.lookup (#2 (LocalesData.get thy)) name;
   22.93 -
   22.94 -fun the_locale thy name =
   22.95 -  (case get_locale thy name of
   22.96 -    SOME loc => loc
   22.97 -  | NONE => error ("Unknown locale " ^ quote name));
   22.98 +    (Sign.declare_name thy name space, Symtab.update (name, loc) locs));
   22.99  
  22.100  fun change_locale name f thy =
  22.101    let
  22.102 @@ -429,9 +402,16 @@
  22.103      val (axiom', imports', elems', params', lparams', decls', regs', intros', dests') =
  22.104        f (axiom, imports, elems, params, lparams, decls, regs, intros, dests);
  22.105    in
  22.106 -    put_locale name {axiom = axiom', imports = imports', elems = elems',
  22.107 -      params = params', lparams = lparams', decls = decls', regs = regs',
  22.108 -      intros = intros', dests = dests'} thy
  22.109 +    thy
  22.110 +    |> (LocalesData.map o apsnd) (Symtab.update (name, {axiom = axiom',
  22.111 +          imports = imports', elems = elems', params = params', lparams = lparams',
  22.112 +          decls = decls', regs = regs', intros = intros', dests = dests'}))
  22.113 +  end;
  22.114 +
  22.115 +fun print_locales thy =
  22.116 +  let val (space, locs) = LocalesData.get thy in
  22.117 +    Pretty.strs ("locales:" :: map #1 (NameSpace.extern_table (space, locs)))
  22.118 +    |> Pretty.writeln
  22.119    end;
  22.120  
  22.121  
  22.122 @@ -754,7 +734,7 @@
  22.123              val {imports, params, ...} = the_locale thy name;
  22.124              val parms = map (fst o fst) params;
  22.125              val (parms', types', syn') = params_of imports;
  22.126 -            val all_parms = merge_lists parms' parms;
  22.127 +            val all_parms = merge_lists (op =) parms' parms;
  22.128              val all_types = merge_tenvs [] types' (params |> map fst |> Symtab.make);
  22.129              val all_syn = merge_syn expr syn' (params |> map (apfst fst) |> Symtab.make);
  22.130            in (all_parms, all_types, all_syn) end
  22.131 @@ -782,14 +762,14 @@
  22.132                     let
  22.133                       val (parms', types', syn') = params_of e
  22.134                     in
  22.135 -                     (merge_lists parms parms', merge_tenvs [] types types',
  22.136 +                     (merge_lists (op =) parms parms', merge_tenvs [] types types',
  22.137                        merge_syn e syn syn')
  22.138                     end)
  22.139              es ([], Symtab.empty, Symtab.empty)
  22.140  
  22.141        val (parms, types, syn) = params_of expr;
  22.142      in
  22.143 -      (merge_lists prev_parms parms, merge_tenvs fixed_params prev_types types,
  22.144 +      (merge_lists (op =) prev_parms parms, merge_tenvs fixed_params prev_types types,
  22.145         merge_syn expr prev_syn syn)
  22.146      end;
  22.147  
  22.148 @@ -901,7 +881,7 @@
  22.149  
  22.150              val (_, ids'', _) = add_with_regs ((name, map #1 params), Assumed []) ([], ids', ids');
  22.151              val ids_ax = if top then fst (fold_map (axiomify ps) ids'' axiom) else ids'';
  22.152 -            in (ids_ax, merge_lists parms' ps) end
  22.153 +            in (ids_ax, merge_lists (op =) parms' ps) end
  22.154        | identify top (Rename (e, xs)) =
  22.155            let
  22.156              val (ids', parms') = identify top e;
  22.157 @@ -916,7 +896,7 @@
  22.158                     let
  22.159                       val (ids', parms') = identify top e
  22.160                     in
  22.161 -                     (merge_alists ids ids', merge_lists parms parms')
  22.162 +                     (merge_alists (op =) ids ids', merge_lists (op =) parms parms')
  22.163                     end)
  22.164              es ([], []);
  22.165  
  22.166 @@ -969,11 +949,11 @@
  22.167  
  22.168  (* NB: derived ids contain only facts at this stage *)
  22.169  
  22.170 -fun activate_elem _ _ ((ctxt, mode), Fixes fixes) =
  22.171 -      ((ctxt |> ProofContext.add_fixes_i fixes |> snd, mode), [])
  22.172 -  | activate_elem _ _ ((ctxt, mode), Constrains _) =
  22.173 -      ((ctxt, mode), [])
  22.174 -  | activate_elem ax_in_ctxt _ ((ctxt, Assumed axs), Assumes asms) =
  22.175 +fun activate_elem _ _ (Fixes fixes) (ctxt, mode) =
  22.176 +      ([], (ctxt |> ProofContext.add_fixes_i fixes |> snd, mode))
  22.177 +  | activate_elem _ _ (Constrains _) (ctxt, mode) =
  22.178 +      ([], (ctxt, mode))
  22.179 +  | activate_elem ax_in_ctxt _ (Assumes asms) (ctxt, Assumed axs) =
  22.180        let
  22.181          val asms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) asms;
  22.182          val ts = maps (map #1 o #2) asms';
  22.183 @@ -981,10 +961,10 @@
  22.184          val (_, ctxt') =
  22.185            ctxt |> fold Variable.auto_fixes ts
  22.186            |> ProofContext.add_assms_i (axioms_export (if ax_in_ctxt then ps else [])) asms';
  22.187 -      in ((ctxt', Assumed qs), []) end
  22.188 -  | activate_elem _ _ ((ctxt, Derived ths), Assumes asms) =
  22.189 -      ((ctxt, Derived ths), [])
  22.190 -  | activate_elem _ _ ((ctxt, Assumed axs), Defines defs) =
  22.191 +      in ([], (ctxt', Assumed qs)) end
  22.192 +  | activate_elem _ _ (Assumes asms) (ctxt, Derived ths) =
  22.193 +      ([], (ctxt, Derived ths))
  22.194 +  | activate_elem _ _ (Defines defs) (ctxt, Assumed axs) =
  22.195        let
  22.196          val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs;
  22.197          val asms = defs' |> map (fn ((name, atts), (t, ps)) =>
  22.198 @@ -993,21 +973,20 @@
  22.199          val (_, ctxt') =
  22.200            ctxt |> fold (Variable.auto_fixes o #1) asms
  22.201            |> ProofContext.add_assms_i LocalDefs.def_export (map #2 asms);
  22.202 -      in ((ctxt', Assumed axs), []) end
  22.203 -  | activate_elem _ _ ((ctxt, Derived ths), Defines defs) =
  22.204 -      ((ctxt, Derived ths), [])
  22.205 -  | activate_elem _ is_ext ((ctxt, mode), Notes (kind, facts)) =
  22.206 +      in ([], (ctxt', Assumed axs)) end
  22.207 +  | activate_elem _ _ (Defines defs) (ctxt, Derived ths) =
  22.208 +      ([], (ctxt, Derived ths))
  22.209 +  | activate_elem _ is_ext (Notes (kind, facts)) (ctxt, mode) =
  22.210        let
  22.211          val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts;
  22.212          val (res, ctxt') = ctxt |> ProofContext.note_thmss_i kind facts';
  22.213 -      in ((ctxt', mode), if is_ext then res else []) end;
  22.214 +      in (if is_ext then res else [], (ctxt', mode)) end;
  22.215  
  22.216  fun activate_elems ax_in_ctxt (((name, ps), mode), elems) ctxt =
  22.217    let
  22.218      val thy = ProofContext.theory_of ctxt;
  22.219 -    val ((ctxt', _), res) =
  22.220 -      foldl_map (activate_elem ax_in_ctxt (name = ""))
  22.221 -        ((ProofContext.qualified_names ctxt, mode), elems)
  22.222 +    val (res, (ctxt', _)) = fold_map (activate_elem ax_in_ctxt (name = ""))
  22.223 +        elems (ProofContext.qualified_names ctxt, mode)
  22.224        handle ERROR msg => err_in_locale ctxt msg [(name, map fst ps)];
  22.225      val ctxt'' = if name = "" then ctxt'
  22.226            else let
  22.227 @@ -1037,10 +1016,10 @@
  22.228  
  22.229  in
  22.230  
  22.231 -(* CB: activate_facts prep_facts (ctxt, elemss),
  22.232 +(* CB: activate_facts prep_facts elemss ctxt,
  22.233     where elemss is a list of pairs consisting of identifiers and
  22.234     context elements, extends ctxt by the context elements yielding
  22.235 -   ctxt' and returns (ctxt', (elemss', facts)).
  22.236 +   ctxt' and returns ((elemss', facts), ctxt').
  22.237     Identifiers in the argument are of the form ((name, ps), axs) and
  22.238     assumptions use the axioms in the identifiers to set up exporters
  22.239     in ctxt'.  elemss' does not contain identifiers and is obtained
  22.240 @@ -1048,9 +1027,9 @@
  22.241     If read_facts or cert_facts is used for prep_facts, these also remove
  22.242     the internal/external markers from elemss. *)
  22.243  
  22.244 -fun activate_facts ax_in_ctxt prep_facts (ctxt, args) =
  22.245 -  let val ((elemss, factss), ctxt') = activate_elemss ax_in_ctxt prep_facts args ctxt |>> split_list
  22.246 -  in (ctxt', (elemss, flat factss)) end;
  22.247 +fun activate_facts ax_in_ctxt prep_facts args =
  22.248 +  activate_elemss ax_in_ctxt prep_facts args
  22.249 +  #>> (apsnd flat o split_list);
  22.250  
  22.251  end;
  22.252  
  22.253 @@ -1107,29 +1086,26 @@
  22.254  
  22.255  local
  22.256  
  22.257 -fun declare_int_elem (ctxt, Fixes fixes) =
  22.258 -      (ctxt |> ProofContext.add_fixes_i (map (fn (x, T, mx) =>
  22.259 -        (x, Option.map (Term.map_type_tfree (TypeInfer.param 0)) T, mx)) fixes) |> snd, [])
  22.260 -  | declare_int_elem (ctxt, _) = (ctxt, []);
  22.261 -
  22.262 -fun declare_ext_elem prep_vars (ctxt, Fixes fixes) =
  22.263 +fun declare_int_elem (Fixes fixes) ctxt =
  22.264 +      ([], ctxt |> ProofContext.add_fixes_i (map (fn (x, T, mx) =>
  22.265 +        (x, Option.map (Term.map_type_tfree (TypeInfer.param 0)) T, mx)) fixes) |> snd)
  22.266 +  | declare_int_elem _ ctxt = ([], ctxt);
  22.267 +
  22.268 +fun declare_ext_elem prep_vars (Fixes fixes) ctxt =
  22.269        let val (vars, _) = prep_vars fixes ctxt
  22.270 -      in (ctxt |> ProofContext.add_fixes_i vars |> snd, []) end
  22.271 -  | declare_ext_elem prep_vars (ctxt, Constrains csts) =
  22.272 +      in ([], ctxt |> ProofContext.add_fixes_i vars |> snd) end
  22.273 +  | declare_ext_elem prep_vars (Constrains csts) ctxt =
  22.274        let val (_, ctxt') = prep_vars (map (fn (x, T) => (x, SOME T, NoSyn)) csts) ctxt
  22.275 -      in (ctxt', []) end
  22.276 -  | declare_ext_elem _ (ctxt, Assumes asms) = (ctxt, map #2 asms)
  22.277 -  | declare_ext_elem _ (ctxt, Defines defs) = (ctxt, map (fn (_, (t, ps)) => [(t, ps)]) defs)
  22.278 -  | declare_ext_elem _ (ctxt, Notes _) = (ctxt, []);
  22.279 -
  22.280 -fun declare_elems prep_vars (ctxt, (((name, ps), Assumed _), elems)) =
  22.281 -    let val (ctxt', propps) =
  22.282 -      (case elems of
  22.283 -        Int es => foldl_map declare_int_elem (ctxt, es)
  22.284 -      | Ext e => foldl_map (declare_ext_elem prep_vars) (ctxt, [e]))
  22.285 -      handle ERROR msg => err_in_locale ctxt msg [(name, map fst ps)]
  22.286 -    in (ctxt', propps) end
  22.287 -  | declare_elems _ (ctxt, ((_, Derived _), elems)) = (ctxt, []);
  22.288 +      in ([], ctxt') end
  22.289 +  | declare_ext_elem _ (Assumes asms) ctxt = (map #2 asms, ctxt)
  22.290 +  | declare_ext_elem _ (Defines defs) ctxt = (map (fn (_, (t, ps)) => [(t, ps)]) defs, ctxt)
  22.291 +  | declare_ext_elem _ (Notes _) ctxt = ([], ctxt);
  22.292 +
  22.293 +fun declare_elems prep_vars (((name, ps), Assumed _), elems) ctxt = ((case elems
  22.294 +     of Int es => fold_map declare_int_elem es ctxt
  22.295 +      | Ext e => declare_ext_elem prep_vars e ctxt |>> single)
  22.296 +          handle ERROR msg => err_in_locale ctxt msg [(name, map fst ps)])
  22.297 +  | declare_elems _ ((_, Derived _), elems) ctxt = ([], ctxt);
  22.298  
  22.299  in
  22.300  
  22.301 @@ -1144,10 +1120,10 @@
  22.302        raw_elemss
  22.303        |> map_filter (fn (id, Int es) => SOME (id, es) | _ => NONE)
  22.304        |> unify_elemss ctxt_with_fixed fixed_params;
  22.305 -    val (_, raw_elemss') =
  22.306 -      foldl_map (fn ((_, es) :: elemss, (id, Int _)) => (elemss, (id, Int es)) | x => x)
  22.307 -        (int_elemss, raw_elemss);
  22.308 -  in foldl_map (declare_elems prep_vars) (ctxt, raw_elemss') end;
  22.309 +    val (raw_elemss', _) =
  22.310 +      fold_map (curry (fn ((id, Int _), (_, es) :: elemss) => ((id, Int es), elemss) | x => x))
  22.311 +        raw_elemss int_elemss;
  22.312 +  in fold_map (declare_elems prep_vars) raw_elemss' ctxt end;
  22.313  
  22.314  end;
  22.315  
  22.316 @@ -1325,7 +1301,7 @@
  22.317      (* CB: raw_elemss are list of pairs consisting of identifiers and
  22.318         context elements, the latter marked as internal or external. *)
  22.319      val raw_elemss = rem_dup_defines raw_elemss;
  22.320 -    val (raw_ctxt, raw_proppss) = declare_elemss prep_vars fixed_params raw_elemss context;
  22.321 +    val (raw_proppss, raw_ctxt) = declare_elemss prep_vars fixed_params raw_elemss context;
  22.322      (* CB: raw_ctxt is context with additional fixed variables derived from
  22.323         the fixes elements in raw_elemss,
  22.324         raw_proppss contains assumptions and definitions from the
  22.325 @@ -1512,11 +1488,11 @@
  22.326      (* CB: all_elemss and parms contain the correct parameter types *)
  22.327  
  22.328      val (ps, qs) = chop (length raw_import_params_elemss + length raw_import_elemss) all_elemss';
  22.329 -    val (import_ctxt, (import_elemss, _)) =
  22.330 -      activate_facts false prep_facts (context, ps);
  22.331 -
  22.332 -    val (ctxt, (elemss, _)) =
  22.333 -      activate_facts false prep_facts (ProofContext.set_stmt true import_ctxt, qs);
  22.334 +    val ((import_elemss, _), import_ctxt) =
  22.335 +      activate_facts false prep_facts ps context;
  22.336 +
  22.337 +    val ((elemss, _), ctxt) =
  22.338 +      activate_facts false prep_facts qs (ProofContext.set_stmt true import_ctxt);
  22.339    in
  22.340      ((((import_ctxt, import_elemss), (ctxt, elemss, syn)),
  22.341        (parms, spec, defs)), concl)
  22.342 @@ -1707,9 +1683,9 @@
  22.343  
  22.344  fun add_thmss loc kind args ctxt =
  22.345    let
  22.346 -    val (ctxt', ([(_, [Notes args'])], _)) =
  22.347 +    val (([(_, [Notes args'])], _), ctxt') =
  22.348        activate_facts true cert_facts
  22.349 -        (ctxt, [((("", []), Assumed []), [Ext (Notes (kind, args))])]);
  22.350 +        [((("", []), Assumed []), [Ext (Notes (kind, args))])] ctxt;
  22.351      val ctxt'' = ctxt' |> ProofContext.theory
  22.352        (change_locale loc
  22.353          (fn (axiom, imports, elems, params, lparams, decls, regs, intros, dests) =>
  22.354 @@ -1923,20 +1899,19 @@
  22.355  
  22.356  fun gen_add_locale prep_ctxt prep_expr
  22.357      predicate_name bname raw_imports raw_body thy =
  22.358 -    (* predicate_name: NONE - open locale without predicate
  22.359 -        SOME "" - locale with predicate named as locale
  22.360 -        SOME "name" - locale with predicate named "name" *)
  22.361 +    (* predicate_name: "" - locale with predicate named as locale
  22.362 +        "name" - locale with predicate named "name" *)
  22.363    let
  22.364 +    val thy_ctxt = ProofContext.init thy;
  22.365      val name = Sign.full_name thy bname;
  22.366      val _ = is_some (get_locale thy name) andalso
  22.367        error ("Duplicate definition of locale " ^ quote name);
  22.368  
  22.369 -    val thy_ctxt = ProofContext.init thy;
  22.370      val (((import_ctxt, import_elemss), (body_ctxt, body_elemss, syn)),
  22.371        text as (parms, ((_, exts'), _), defs)) =
  22.372 -      prep_ctxt raw_imports raw_body thy_ctxt;
  22.373 +        prep_ctxt raw_imports raw_body thy_ctxt;
  22.374      val elemss = import_elemss @ body_elemss |>
  22.375 -        map_filter (fn ((id, Assumed axs), elems) => SOME (id, elems) | _ => NONE);
  22.376 +      map_filter (fn ((id, Assumed axs), elems) => SOME (id, elems) | _ => NONE);
  22.377      val imports = prep_expr thy raw_imports;
  22.378  
  22.379      val extraTs = List.foldr Term.add_term_tfrees [] exts' \\
  22.380 @@ -1944,27 +1919,18 @@
  22.381      val _ = if null extraTs then ()
  22.382        else warning ("Additional type variable(s) in locale specification " ^ quote bname);
  22.383  
  22.384 -    val ((((elemss', predicate as (predicate_statement, predicate_axioms), stmt'), intros),
  22.385 -          pred_thy), (imports, regs)) =
  22.386 -      case predicate_name
  22.387 -       of SOME predicate_name =>
  22.388 -            let
  22.389 -              val predicate_name' = case predicate_name of "" => bname | _ => predicate_name;
  22.390 -              val (elemss', defns) = change_defines_elemss thy elemss [];
  22.391 -              val elemss'' = elemss' @ [(("", []), defns)];
  22.392 -              val (((elemss''', predicate as (_, axioms), stmt'), intros), thy') =
  22.393 -                define_preds predicate_name' text elemss'' thy;
  22.394 -              fun mk_regs elemss wits =
  22.395 -                fold_map (fn (id, elems) => fn wts => let
  22.396 -                    val ts = List.concat (List.mapPartial (fn (Assumes asms) =>
  22.397 -                      SOME (List.concat (map (map #1 o #2) asms)) | _ => NONE) elems);
  22.398 -                    val (wts1, wts2) = chop (length ts) wts
  22.399 -                  in ((apsnd (map fst) id, wts1), wts2) end) elemss wits |> fst;
  22.400 -              val regs = mk_regs elemss''' axioms |>
  22.401 -                    map_filter (fn (("", _), _) => NONE | e => SOME e);
  22.402 -            in ((((elemss''', predicate, stmt'), intros), thy'), (empty, regs)) end
  22.403 -        | NONE => ((((elemss, ([], []), []), ([], [])), thy), (imports, []));
  22.404 -
  22.405 +    val predicate_name' = case predicate_name of "" => bname | _ => predicate_name;
  22.406 +    val (elemss'_, defns) = change_defines_elemss thy elemss [];
  22.407 +    val elemss''_ = elemss'_ @ [(("", []), defns)];
  22.408 +    val (((elemss', predicate as (pred_statement, pred_axioms), stmt'), intros), thy') =
  22.409 +      define_preds predicate_name' text elemss''_ thy;
  22.410 +    fun mk_regs elemss wits = fold_map (fn (id, elems) => fn wts => let
  22.411 +        val ts = flat (map_filter (fn (Assumes asms) =>
  22.412 +          SOME (maps (map #1 o #2) asms) | _ => NONE) elems);
  22.413 +        val (wts1, wts2) = chop (length ts) wts;
  22.414 +      in ((apsnd (map fst) id, wts1), wts2) end) elemss wits |> fst;
  22.415 +    val regs = mk_regs elemss' pred_axioms
  22.416 +      |> map_filter (fn (("", _), _) => NONE | e => SOME e);
  22.417      fun axiomify axioms elemss =
  22.418        (axioms, elemss) |> foldl_map (fn (axs, (id, elems)) => let
  22.419                     val ts = flat (map_filter (fn (Assumes asms) =>
  22.420 @@ -1972,28 +1938,26 @@
  22.421                     val (axs1, axs2) = chop (length ts) axs;
  22.422                   in (axs2, ((id, Assumed axs1), elems)) end)
  22.423          |> snd;
  22.424 -    val (ctxt, (_, facts)) = activate_facts true (K I)
  22.425 -      (ProofContext.init pred_thy, axiomify predicate_axioms elemss');
  22.426 -    val view_ctxt = Assumption.add_view thy_ctxt predicate_statement ctxt;
  22.427 +    val ((_, facts), ctxt) = activate_facts true (K I)
  22.428 +      (axiomify pred_axioms elemss') (ProofContext.init thy');
  22.429 +    val view_ctxt = Assumption.add_view thy_ctxt pred_statement ctxt;
  22.430      val export = Thm.close_derivation o Goal.norm_result o
  22.431        singleton (ProofContext.export view_ctxt thy_ctxt);
  22.432      val facts' = facts |> map (fn (a, ths) => ((a, []), [(map export ths, [])]));
  22.433      val elems' = maps #2 (filter (equal "" o #1 o #1) elemss');
  22.434      val elems'' = map_filter (fn (Fixes _) => NONE | e => SOME e) elems';
  22.435 -    val axs' = map (Element.assume_witness pred_thy) stmt';
  22.436 -    val loc_ctxt = pred_thy
  22.437 +    val axs' = map (Element.assume_witness thy') stmt';
  22.438 +    val loc_ctxt = thy'
  22.439        |> PureThy.note_thmss_qualified Thm.assumptionK bname facts' |> snd
  22.440 -      |> declare_locale name
  22.441 -      |> put_locale name
  22.442 -       {axiom = axs',
  22.443 -        imports = imports,
  22.444 +      |> add_locale name {axiom = axs',
  22.445 +        imports = empty,
  22.446          elems = map (fn e => (e, stamp ())) elems'',
  22.447          params = params_of elemss' |> map (fn (x, SOME T) => ((x, T), the (Symtab.lookup syn x))),
  22.448          lparams = map #1 (params_of' body_elemss),
  22.449          decls = ([], []),
  22.450          regs = regs,
  22.451          intros = intros,
  22.452 -        dests = map Element.conclude_witness predicate_axioms}
  22.453 +        dests = map Element.conclude_witness pred_axioms}
  22.454        |> init name;
  22.455    in (name, loc_ctxt) end;
  22.456  
  22.457 @@ -2005,9 +1969,9 @@
  22.458  end;
  22.459  
  22.460  val _ = Context.>> (Context.map_theory
  22.461 - (add_locale_i (SOME "") "var" empty [Fixes [(Name.internal "x", NONE, NoSyn)]] #>
  22.462 + (add_locale_i "" "var" empty [Fixes [(Name.internal "x", NONE, NoSyn)]] #>
  22.463    snd #> ProofContext.theory_of #>
  22.464 -  add_locale_i (SOME "") "struct" empty [Fixes [(Name.internal "S", NONE, Structure)]] #>
  22.465 +  add_locale_i "" "struct" empty [Fixes [(Name.internal "S", NONE, Structure)]] #>
  22.466    snd #> ProofContext.theory_of));
  22.467  
  22.468  
    23.1 --- a/src/Pure/Pure.thy	Fri Jul 25 12:03:31 2008 +0200
    23.2 +++ b/src/Pure/Pure.thy	Fri Jul 25 12:03:32 2008 +0200
    23.3 @@ -26,7 +26,7 @@
    23.4  
    23.5  subsection {* Embedded terms *}
    23.6  
    23.7 -locale (open) meta_term_syntax =
    23.8 +locale meta_term_syntax =
    23.9    fixes meta_term :: "'a => prop"  ("TERM _")
   23.10  
   23.11  lemmas [intro?] = termI
   23.12 @@ -34,7 +34,7 @@
   23.13  
   23.14  subsection {* Meta-level conjunction *}
   23.15  
   23.16 -locale (open) meta_conjunction_syntax =
   23.17 +locale meta_conjunction_syntax =
   23.18    fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
   23.19  
   23.20  lemma all_conjunction: