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: