--- a/NEWS Fri Jul 25 12:03:31 2008 +0200
+++ b/NEWS Fri Jul 25 12:03:32 2008 +0200
@@ -19,6 +19,8 @@
*** Pure ***
+* dropped "locale (open)". INCOMPATBILITY.
+
* Command 'instance': attached definitions no longer accepted.
INCOMPATIBILITY, use proper 'instantiation' target.
@@ -34,6 +36,10 @@
*** HOL ***
+* HOL/Orderings: added class "preorder" as superclass of "order". INCOMPATIBILITY:
+Instantiation proofs for order, linorder etc. slightly changed. Some theorems
+named order_class.* now named preorder_class.*.
+
* HOL/Ring_and_Field and HOL/Divides: Definition of "op dvd" has been moved
to separate class dvd in Ring_and_Field; a couple of lemmas on dvd has been
generalized to class comm_semiring_1. Likewise a bunch of lemmas from Divides
--- a/doc-src/IsarRef/Thy/Spec.thy Fri Jul 25 12:03:31 2008 +0200
+++ b/doc-src/IsarRef/Thy/Spec.thy Fri Jul 25 12:03:32 2008 +0200
@@ -298,7 +298,7 @@
\indexisarelem{fixes}\indexisarelem{constrains}\indexisarelem{assumes}
\indexisarelem{defines}\indexisarelem{notes}\indexisarelem{includes}
\begin{rail}
- 'locale' ('(open)')? name ('=' localeexpr)? 'begin'?
+ 'locale' name ('=' localeexpr)? 'begin'?
;
'print\_locale' '!'? localeexpr
;
@@ -415,11 +415,6 @@
\secref{sec:object-logic}). Separate introduction rules @{text
loc_axioms.intro} and @{text loc.intro} are provided as well.
- The @{text "(open)"} option of a locale specification prevents both
- the current @{text loc_axioms} and cumulative @{text loc} predicate
- constructions. Predicates are also omitted for empty specification
- texts.
-
\item [@{command "print_locale"}~@{text "import + body"}] prints the
specified locale expression in a flattened form. The notable
special case @{command "print_locale"}~@{text loc} just prints the
--- a/src/FOL/ex/LocaleTest.thy Fri Jul 25 12:03:31 2008 +0200
+++ b/src/FOL/ex/LocaleTest.thy Fri Jul 25 12:03:32 2008 +0200
@@ -37,7 +37,7 @@
subsection {* Renaming with Syntax *}
-locale (open) LS = var mult +
+locale LS = var mult +
assumes "mult(x, y) = mult(y, x)"
print_locale LS
@@ -95,7 +95,7 @@
locale IA = fixes a assumes asm_A: "a = a"
-locale (open) IB = fixes b assumes asm_B [simp]: "b = b"
+locale IB = fixes b assumes asm_B [simp]: "b = b"
locale IC = IA + IB + assumes asm_C: "c = c"
(* TODO: independent type var in c, prohibit locale declaration *)
@@ -230,10 +230,10 @@
(* Definition involving free variable in assm *)
-locale (open) IG = fixes g assumes asm_G: "g --> x"
+locale IG = fixes g assumes asm_G: "g --> x"
notes asm_G2 = asm_G
-interpretation i8: IG ["False"] by fast
+interpretation i8: IG ["False"] by (rule IG.intro) fast
thm i8.asm_G2
@@ -346,10 +346,10 @@
text {* Naming convention for global objects: prefixes R and r *}
-locale (open) Rsemi = var prod (infixl "**" 65) +
+locale Rsemi = var prod (infixl "**" 65) +
assumes assoc: "(x ** y) ** z = x ** (y ** z)"
-locale (open) Rlgrp = Rsemi + var one + var inv +
+locale Rlgrp = Rsemi + var one + var inv +
assumes lone: "one ** x = x"
and linv: "inv(x) ** x = one"
@@ -361,7 +361,7 @@
then show "y = z" by (simp add: lone linv)
qed simp
-locale (open) Rrgrp = Rsemi + var one + var inv +
+locale Rrgrp = Rsemi + var one + var inv +
assumes rone: "x ** one = x"
and rinv: "x ** inv(x) = one"
@@ -375,7 +375,7 @@
qed simp
interpretation Rlgrp < Rrgrp
- proof -
+ proof
{
fix x
have "inv(x) ** x ** one = inv(x) ** x" by (simp add: linv lone)
@@ -405,7 +405,7 @@
(* circular interpretation *)
interpretation Rrgrp < Rlgrp
- proof -
+ proof
{
fix x
have "one ** (x ** inv(x)) = x ** inv(x)" by (simp add: rinv rone)
@@ -451,35 +451,35 @@
(* circle of three locales, forward direction *)
-locale (open) RA1 = var A + var B + assumes p: "A <-> B"
-locale (open) RA2 = var A + var B + assumes q: "A & B | ~ A & ~ B"
-locale (open) RA3 = var A + var B + assumes r: "(A --> B) & (B --> A)"
+locale RA1 = var A + var B + assumes p: "A <-> B"
+locale RA2 = var A + var B + assumes q: "A & B | ~ A & ~ B"
+locale RA3 = var A + var B + assumes r: "(A --> B) & (B --> A)"
interpretation RA1 < RA2
print_facts
- using p apply fast done
+ using p apply unfold_locales apply fast done
interpretation RA2 < RA3
print_facts
- using q apply fast done
+ using q apply unfold_locales apply fast done
interpretation RA3 < RA1
print_facts
- using r apply fast done
+ using r apply unfold_locales apply fast done
(* circle of three locales, backward direction *)
-locale (open) RB1 = var A + var B + assumes p: "A <-> B"
-locale (open) RB2 = var A + var B + assumes q: "A & B | ~ A & ~ B"
-locale (open) RB3 = var A + var B + assumes r: "(A --> B) & (B --> A)"
+locale RB1 = var A + var B + assumes p: "A <-> B"
+locale RB2 = var A + var B + assumes q: "A & B | ~ A & ~ B"
+locale RB3 = var A + var B + assumes r: "(A --> B) & (B --> A)"
interpretation RB1 < RB2
print_facts
- using p apply fast done
+ using p apply unfold_locales apply fast done
interpretation RB3 < RB1
print_facts
- using r apply fast done
+ using r apply unfold_locales apply fast done
interpretation RB2 < RB3
print_facts
- using q apply fast done
+ using q apply unfold_locales apply fast done
lemma (in RB1) True
print_facts
@@ -579,7 +579,7 @@
r_inv : "rinv(x) # x = rone"
interpretation Rbool: Rlgrp ["op #" "rone" "rinv"]
-proof -
+proof
fix x y z
{
show "(x # y) # z = x # (y # z)" by (rule i_assoc)
@@ -653,6 +653,9 @@
interpretation R2: Rqlgrp ["op #" "rone" "rinv"]
apply unfold_locales (* FIXME: unfold_locales is too eager and shouldn't
solve this. *)
+ apply (rule i_assoc)
+ apply (rule r_one)
+ apply (rule r_inv)
done
print_interps Rqsemi
--- a/src/HOL/Hyperreal/SEQ.thy Fri Jul 25 12:03:31 2008 +0200
+++ b/src/HOL/Hyperreal/SEQ.thy Fri Jul 25 12:03:32 2008 +0200
@@ -926,12 +926,17 @@
"(\<bar>x - a\<bar> < (r::real)) = (a - r < x \<and> x < a + r)"
by auto
-locale (open) real_Cauchy =
+locale real_Cauchy =
fixes X :: "nat \<Rightarrow> real"
assumes X: "Cauchy X"
fixes S :: "real set"
defines S_def: "S \<equiv> {x::real. \<exists>N. \<forall>n\<ge>N. x < X n}"
+lemma real_CauchyI:
+ assumes "Cauchy X"
+ shows "real_Cauchy X"
+by unfold_locales (fact assms)
+
lemma (in real_Cauchy) mem_S: "\<forall>n\<ge>N. x < X n \<Longrightarrow> x \<in> S"
by (unfold S_def, auto)
@@ -1010,7 +1015,9 @@
lemma real_Cauchy_convergent:
fixes X :: "nat \<Rightarrow> real"
shows "Cauchy X \<Longrightarrow> convergent X"
-unfolding convergent_def by (rule real_Cauchy.LIMSEQ_ex)
+unfolding convergent_def
+by (rule real_Cauchy.LIMSEQ_ex)
+ (rule real_CauchyI)
instance real :: banach
by intro_classes (rule real_Cauchy_convergent)
--- a/src/HOL/Library/Eval.thy Fri Jul 25 12:03:31 2008 +0200
+++ b/src/HOL/Library/Eval.thy Fri Jul 25 12:03:32 2008 +0200
@@ -177,7 +177,7 @@
notation (output)
rterm_of ("\<guillemotleft>_\<guillemotright>")
-locale (open) rterm_syntax =
+locale rterm_syntax =
fixes rterm_of_syntax :: "'a \<Rightarrow> 'b" ("\<guillemotleft>_\<guillemotright>")
parse_translation {*
--- a/src/HOL/MetisExamples/Tarski.thy Fri Jul 25 12:03:31 2008 +0200
+++ b/src/HOL/MetisExamples/Tarski.thy Fri Jul 25 12:03:32 2008 +0200
@@ -69,10 +69,6 @@
(\<forall>S. S \<subseteq> pset cl --> (\<exists>L. isLub S cl L)) &
(\<forall>S. S \<subseteq> pset cl --> (\<exists>G. isGlb S cl G))}"
- CLF :: "('a potype * ('a => 'a)) set"
- "CLF == SIGMA cl: CompleteLattice.
- {f. f: pset cl -> pset cl & monotone f (pset cl) (order cl)}"
-
induced :: "['a set, ('a * 'a) set] => ('a *'a)set"
"induced A r == {(a,b). a : A & b: A & (a,b): r}"
@@ -93,7 +89,7 @@
dual :: "'a potype => 'a potype"
"dual po == (| pset = pset po, order = converse (order po) |)"
-locale (open) PO =
+locale PO =
fixes cl :: "'a potype"
and A :: "'a set"
and r :: "('a * 'a) set"
@@ -101,17 +97,21 @@
defines A_def: "A == pset cl"
and r_def: "r == order cl"
-locale (open) CL = PO +
+locale CL = PO +
assumes cl_co: "cl : CompleteLattice"
-locale (open) CLF = CL +
+definition CLF_set :: "('a potype * ('a => 'a)) set" where
+ "CLF_set = (SIGMA cl: CompleteLattice.
+ {f. f: pset cl -> pset cl & monotone f (pset cl) (order cl)})"
+
+locale CLF = CL +
fixes f :: "'a => 'a"
and P :: "'a set"
- assumes f_cl: "(cl,f) : CLF" (*was the equivalent "f : CLF``{cl}"*)
+ assumes f_cl: "(cl,f) : CLF_set" (*was the equivalent "f : CLF``{cl}"*)
defines P_def: "P == fix f A"
-locale (open) Tarski = CLF +
+locale Tarski = CLF +
fixes Y :: "'a set"
and intY1 :: "'a set"
and v :: "'a"
@@ -230,9 +230,9 @@
lemmas CL_imp_PO = CL_subset_PO [THEN subsetD]
-declare CL_imp_PO [THEN PO.PO_imp_refl, simp]
-declare CL_imp_PO [THEN PO.PO_imp_sym, simp]
-declare CL_imp_PO [THEN PO.PO_imp_trans, simp]
+declare PO.PO_imp_refl [OF PO.intro [OF CL_imp_PO], simp]
+declare PO.PO_imp_sym [OF PO.intro [OF CL_imp_PO], simp]
+declare PO.PO_imp_trans [OF PO.intro [OF CL_imp_PO], simp]
lemma (in CL) CO_refl: "refl A r"
by (rule PO_imp_refl)
@@ -385,7 +385,10 @@
apply (simp add: A_def)
apply (rule dualA_iff [THEN subst])
apply (rule CL.lub_in_lattice)
+apply (rule CL.intro)
+apply (rule PO.intro)
apply (rule dualPO)
+apply (rule CL_axioms.intro)
apply (rule CL_dualCL)
apply (simp add: dualA_iff)
done
@@ -395,7 +398,10 @@
apply (simp add: r_def)
apply (rule dualr_iff [THEN subst])
apply (rule CL.lub_upper)
+apply (rule CL.intro)
+apply (rule PO.intro)
apply (rule dualPO)
+apply (rule CL_axioms.intro)
apply (rule CL_dualCL)
apply (simp add: dualA_iff A_def, assumption)
done
@@ -414,10 +420,10 @@
lemma (in CLF) [simp]:
"f: pset cl -> pset cl & monotone f (pset cl) (order cl)"
apply (insert f_cl)
-apply (unfold CLF_def)
+apply (unfold CLF_set_def)
apply (erule SigmaE2)
apply (erule CollectE)
-apply assumption;
+apply assumption
done
lemma (in CLF) f_in_funcset: "f \<in> A -> A"
@@ -428,12 +434,14 @@
(*never proved, 2007-01-22*)
ML_command{*ResAtp.problem_name:="Tarski__CLF_CLF_dual"*}
- declare (in CLF) CLF_def[simp] CL_dualCL[simp] monotone_dual[simp] dualA_iff[simp]
-lemma (in CLF) CLF_dual: "(dual cl, f) \<in> CLF"
+declare (in CLF) CLF_set_def [simp] CL_dualCL [simp] monotone_dual [simp] dualA_iff [simp]
+
+lemma (in CLF) CLF_dual: "(dual cl, f) \<in> CLF_set"
apply (simp del: dualA_iff)
apply (simp)
done
- declare (in CLF) CLF_def[simp del] CL_dualCL[simp del] monotone_dual[simp del]
+
+declare (in CLF) CLF_set_def[simp del] CL_dualCL[simp del] monotone_dual[simp del]
dualA_iff[simp del]
@@ -639,8 +647,13 @@
apply (simp add: glb_dual_lub P_def A_def r_def)
apply (rule dualA_iff [THEN subst])
apply (rule CLF.lubH_is_fixp)
+apply (rule CLF.intro)
+apply (rule CL.intro)
+apply (rule PO.intro)
apply (rule dualPO)
+apply (rule CL_axioms.intro)
apply (rule CL_dualCL)
+apply (rule CLF_axioms.intro)
apply (rule CLF_dual)
apply (simp add: dualr_iff dualA_iff)
done
@@ -657,8 +670,8 @@
(*never proved, 2007-01-22*)
ML_command{*ResAtp.problem_name:="Tarski__T_thm_1_glb_simpler"*} (*ALL THEOREMS*)
(*sledgehammer;*)
-apply (simp add: CLF.T_thm_1_lub [of _ f, OF dualPO CL_dualCL]
- dualPO CL_dualCL CLF_dual dualr_iff)
+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,
+ OF dualPO CL_dualCL] dualPO CL_dualCL CLF_dual dualr_iff)
done
subsection {* interval *}
@@ -729,7 +742,7 @@
"[| a \<in> A; b \<in> A; interval r a b \<noteq> {}; S \<subseteq> interval r a b; isGlb S cl G;
S \<noteq> {} |] ==> G \<in> interval r a b"
apply (simp add: interval_dual)
-apply (simp add: CLF.L_in_interval [of _ f]
+apply (simp add: CLF.L_in_interval [of _ f, OF CLF.intro, OF CL.intro CLF_axioms.intro, OF PO.intro CL_axioms.intro]
dualA_iff A_def dualPO CL_dualCL CLF_dual isGlb_dual_isLub)
done
@@ -851,7 +864,7 @@
ML_command{*ResAtp.problem_name:="Tarski__Top_in_lattice_simpler"*} (*ALL THEOREMS*)
(*sledgehammer*)
apply (rule dualA_iff [THEN subst])
-apply (blast intro!: CLF.Bot_in_lattice dualPO CL_dualCL CLF_dual)
+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)
done
lemma (in CLF) Top_prop: "x \<in> A ==> (x, Top cl) \<in> r"
@@ -868,7 +881,7 @@
(*sledgehammer*)
apply (simp add: Bot_dual_Top r_def)
apply (rule dualr_iff [THEN subst])
-apply (simp add: CLF.Top_prop [of _ f]
+apply (simp add: CLF.Top_prop [of _ f, OF CLF.intro, OF CL.intro CLF_axioms.intro, OF PO.intro CL_axioms.intro]
dualA_iff A_def dualPO CL_dualCL CLF_dual)
done
@@ -996,8 +1009,8 @@
apply (unfold P_def)
apply (rule_tac A = "intY1" in fixf_subset)
apply (rule intY1_subset)
-apply (simp add: CLF.glbH_is_fixp [OF _ intY1_is_cl, simplified]
- v_def CL_imp_PO intY1_is_cl CLF_def intY1_func intY1_mono)
+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]
+ v_def CL_imp_PO intY1_is_cl CLF_set_def intY1_func intY1_mono)
done
ML_command{*ResAtp.problem_name:="Tarski__z_in_interval"*} (*ALL THEOREMS*)
@@ -1042,7 +1055,7 @@
apply (rule_tac b = "Top cl" in interval_imp_mem)
apply (simp add: v_def)
apply (fold intY1_def)
-apply (rule CL.glb_in_lattice [OF _ intY1_is_cl, simplified])
+apply (rule CL.glb_in_lattice [OF CL.intro, OF PO.intro CL_axioms.intro, OF _ intY1_is_cl, simplified])
apply (simp add: CL_imp_PO intY1_is_cl, force)
-- {* @{text v} is LEAST ub *}
apply clarify
@@ -1058,7 +1071,7 @@
(*never proved, 2007-01-22*)
ML_command{*ResAtp.problem_name:="Tarski__tarski_full_lemma_simplest"*}
(*sledgehammer*)
-apply (rule CL.glb_lower [OF _ intY1_is_cl, simplified])
+apply (rule CL.glb_lower [OF CL.intro, OF PO.intro CL_axioms.intro, OF _ intY1_is_cl, simplified])
apply (simp add: CL_imp_PO intY1_is_cl)
apply force
apply (simp add: induced_def intY1_f_closed z_in_interval)
@@ -1087,7 +1100,8 @@
ML_command{*ResAtp.problem_name:="Tarski__Tarski_full_simpler"*}
(*sledgehammer*)
apply (simp add: P_def A_def r_def)
-apply (blast intro!: Tarski.tarski_full_lemma cl_po cl_co f_cl)
+apply (blast intro!: Tarski.tarski_full_lemma [OF Tarski.intro, OF CLF.intro Tarski_axioms.intro,
+ OF CL.intro CLF_axioms.intro, OF PO.intro CL_axioms.intro] cl_po cl_co f_cl)
done
declare (in CLF) fixf_po[rule del] P_def [simp del] A_def [simp del] r_def [simp del]
Tarski.tarski_full_lemma [rule del] cl_po [rule del] cl_co [rule del]
--- a/src/HOL/MicroJava/BV/Err.thy Fri Jul 25 12:03:31 2008 +0200
+++ b/src/HOL/MicroJava/BV/Err.thy Fri Jul 25 12:03:32 2008 +0200
@@ -8,7 +8,9 @@
header {* \isaheader{The Error Type} *}
-theory Err imports Semilat begin
+theory Err
+imports Semilat
+begin
datatype 'a err = Err | OK 'a
@@ -228,20 +230,20 @@
lemma semilat_le_err_Err_plus [simp]:
"\<lbrakk> x: err A; semilat(err A, le r, f) \<rbrakk> \<Longrightarrow> Err +_f x = Err"
- by (blast intro: semilat.le_iff_plus_unchanged [THEN iffD1]
- semilat.le_iff_plus_unchanged2 [THEN iffD1])
+ by (blast intro: Semilat.le_iff_plus_unchanged [OF Semilat.intro, THEN iffD1]
+ Semilat.le_iff_plus_unchanged2 [OF Semilat.intro, THEN iffD1])
lemma semilat_le_err_plus_Err [simp]:
"\<lbrakk> x: err A; semilat(err A, le r, f) \<rbrakk> \<Longrightarrow> x +_f Err = Err"
- by (blast intro: semilat.le_iff_plus_unchanged [THEN iffD1]
- semilat.le_iff_plus_unchanged2 [THEN iffD1])
+ by (blast intro: Semilat.le_iff_plus_unchanged [OF Semilat.intro, THEN iffD1]
+ Semilat.le_iff_plus_unchanged2 [OF Semilat.intro, THEN iffD1])
lemma semilat_le_err_OK1:
"\<lbrakk> x:A; y:A; semilat(err A, le r, f); OK x +_f OK y = OK z \<rbrakk>
\<Longrightarrow> x <=_r z";
apply (rule OK_le_err_OK [THEN iffD1])
apply (erule subst)
-apply (simp add:semilat.ub1)
+apply (simp add: Semilat.ub1 [OF Semilat.intro])
done
lemma semilat_le_err_OK2:
@@ -249,7 +251,7 @@
\<Longrightarrow> y <=_r z"
apply (rule OK_le_err_OK [THEN iffD1])
apply (erule subst)
-apply (simp add:semilat.ub2)
+apply (simp add: Semilat.ub2 [OF Semilat.intro])
done
lemma eq_order_le:
@@ -265,13 +267,13 @@
have plus_le_conv3: "\<And>A x y z f r.
\<lbrakk> semilat (A,r,f); x +_f y <=_r z; x:A; y:A; z:A \<rbrakk>
\<Longrightarrow> x <=_r z \<and> y <=_r z"
- by (rule semilat.plus_le_conv [THEN iffD1])
+ by (rule Semilat.plus_le_conv [OF Semilat.intro, THEN iffD1])
from prems show ?thesis
apply (rule_tac iffI)
apply clarify
apply (drule OK_le_err_OK [THEN iffD2])
apply (drule OK_le_err_OK [THEN iffD2])
- apply (drule semilat.lub[of _ _ _ "OK x" _ "OK y"])
+ apply (drule Semilat.lub [OF Semilat.intro, of _ _ _ "OK x" _ "OK y"])
apply assumption
apply assumption
apply simp
@@ -283,10 +285,10 @@
apply (rename_tac z)
apply (subgoal_tac "OK z: err A")
apply (drule eq_order_le)
- apply (erule semilat.orderI)
+ apply (erule Semilat.orderI [OF Semilat.intro])
apply (blast dest: plus_le_conv3)
apply (erule subst)
- apply (blast intro: semilat.closedI closedD)
+ apply (blast intro: Semilat.closedI [OF Semilat.intro] closedD)
done
qed
--- a/src/HOL/MicroJava/BV/Kildall.thy Fri Jul 25 12:03:31 2008 +0200
+++ b/src/HOL/MicroJava/BV/Kildall.thy Fri Jul 25 12:03:32 2008 +0200
@@ -8,7 +8,9 @@
header {* \isaheader{Kildall's Algorithm}\label{sec:Kildall} *}
-theory Kildall imports SemilatAlg While_Combinator begin
+theory Kildall
+imports SemilatAlg While_Combinator
+begin
consts
@@ -43,10 +45,10 @@
"merges f (p'#ps) ss = (let (p,s) = p' in merges f ps (ss[p := s +_f ss!p]))"
-lemmas [simp] = Let_def semilat.le_iff_plus_unchanged [symmetric]
+lemmas [simp] = Let_def Semilat.le_iff_plus_unchanged [OF Semilat.intro, symmetric]
-lemma (in semilat) nth_merges:
+lemma (in Semilat) nth_merges:
"\<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>
(merges f ps ss)!p = map snd [(p',t') \<leftarrow> ps. p'=p] ++_f ss!p"
(is "\<And>ss. \<lbrakk>_; _; ?steptype ps\<rbrakk> \<Longrightarrow> ?P ss ps")
@@ -82,7 +84,7 @@
by (induct_tac ps, auto)
-lemma (in semilat) merges_preserves_type_lemma:
+lemma (in Semilat) merges_preserves_type_lemma:
shows "\<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>(p,x) \<in> set ps. p<n \<and> x\<in>A)
\<longrightarrow> merges f ps xs \<in> list n A"
apply (insert closedI)
@@ -92,12 +94,12 @@
apply clarsimp
done
-lemma (in semilat) merges_preserves_type [simp]:
+lemma (in Semilat) merges_preserves_type [simp]:
"\<lbrakk> xs \<in> list n A; \<forall>(p,x) \<in> set ps. p<n \<and> x\<in>A \<rbrakk>
\<Longrightarrow> merges f ps xs \<in> list n A"
by (simp add: merges_preserves_type_lemma)
-lemma (in semilat) merges_incr_lemma:
+lemma (in Semilat) merges_incr_lemma:
"\<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"
apply (induct_tac ps)
apply simp
@@ -111,13 +113,13 @@
apply (blast intro!: listE_set intro: closedD listE_length [THEN nth_in])
done
-lemma (in semilat) merges_incr:
+lemma (in Semilat) merges_incr:
"\<lbrakk> xs \<in> list n A; \<forall>(p,x)\<in>set ps. p<size xs \<and> x \<in> A \<rbrakk>
\<Longrightarrow> xs <=[r] merges f ps xs"
by (simp add: merges_incr_lemma)
-lemma (in semilat) merges_same_conv [rule_format]:
+lemma (in Semilat) merges_same_conv [rule_format]:
"(\<forall>xs. xs \<in> list n A \<longrightarrow> (\<forall>(p,x)\<in>set ps. p<size xs \<and> x\<in>A) \<longrightarrow>
(merges f ps xs = xs) = (\<forall>(p,x)\<in>set ps. x <=_r xs!p))"
apply (induct_tac ps)
@@ -150,7 +152,7 @@
done
-lemma (in semilat) list_update_le_listI [rule_format]:
+lemma (in Semilat) list_update_le_listI [rule_format]:
"set xs <= A \<longrightarrow> set ys <= A \<longrightarrow> xs <=[r] ys \<longrightarrow> p < size xs \<longrightarrow>
x <=_r ys!p \<longrightarrow> x\<in>A \<longrightarrow> xs[p := x +_f xs!p] <=[r] ys"
apply(insert semilat)
@@ -158,7 +160,7 @@
apply (simp add: list_all2_conv_all_nth nth_list_update)
done
-lemma (in semilat) merges_pres_le_ub:
+lemma (in Semilat) merges_pres_le_ub:
assumes "set ts <= A" and "set ss <= A"
and "\<forall>(p,t)\<in>set ps. t <=_r ts!p \<and> t \<in> A \<and> p < size ts" and "ss <=[r] ts"
shows "merges f ps ss <=[r] ts"
@@ -206,7 +208,7 @@
(** iter **)
-lemma (in semilat) stable_pres_lemma:
+lemma (in Semilat) stable_pres_lemma:
shows "\<lbrakk>pres_type step n A; bounded step n;
ss \<in> list n A; p \<in> w; \<forall>q\<in>w. q < n;
\<forall>q. q < n \<longrightarrow> q \<notin> w \<longrightarrow> stable r step ss q; q < n;
@@ -284,7 +286,7 @@
done
-lemma (in semilat) merges_bounded_lemma:
+lemma (in Semilat) merges_bounded_lemma:
"\<lbrakk> mono r step n A; bounded step n;
\<forall>(p',s') \<in> set (step p (ss!p)). s' \<in> A; ss \<in> list n A; ts \<in> list n A; p < n;
ss <=[r] ts; \<forall>p. p < n \<longrightarrow> stable r step ts p \<rbrakk>
@@ -319,7 +321,7 @@
ss <[r] merges f qs ss \<or>
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")
proof -
- interpret semilat [A r f] by fact
+ interpret Semilat [A r f] using assms by (rule Semilat.intro)
show "PROP ?P" apply(insert semilat)
apply (unfold lesssub_def)
apply (simp (no_asm_simp) add: merges_incr)
@@ -349,7 +351,7 @@
(\<forall>ts\<in>list n A. ss0 <=[r] ts \<and> stables r step ts \<longrightarrow> ss' <=[r] ts)"
(is "PROP ?P")
proof -
- interpret semilat [A r f] by fact
+ interpret Semilat [A r f] using assms by (rule Semilat.intro)
show "PROP ?P" apply(insert semilat)
apply (unfold iter_def stables_def)
apply (rule_tac P = "%(ss,w).
@@ -455,7 +457,7 @@
kildall r f step ss0 <=[r] ts)"
(is "PROP ?P")
proof -
- interpret semilat [A r f] by fact
+ interpret Semilat [A r f] using assms by (rule Semilat.intro)
show "PROP ?P"
apply (unfold kildall_def)
apply(case_tac "iter f step ss0 (unstables r step ss0)")
@@ -472,7 +474,7 @@
\<Longrightarrow> is_bcv r T step n A (kildall r f step)"
(is "PROP ?P")
proof -
- interpret semilat [A r f] by fact
+ interpret Semilat [A r f] using assms by (rule Semilat.intro)
show "PROP ?P"
apply(unfold is_bcv_def wt_step_def)
apply(insert semilat kildall_properties[of A])
--- a/src/HOL/MicroJava/BV/LBVComplete.thy Fri Jul 25 12:03:31 2008 +0200
+++ b/src/HOL/MicroJava/BV/LBVComplete.thy Fri Jul 25 12:03:32 2008 +0200
@@ -25,7 +25,7 @@
by (force simp: list_ex_iff is_target_def mem_iff)
-locale (open) lbvc = lbv +
+locale lbvc = lbv +
fixes phi :: "'a list" ("\<phi>")
fixes c :: "'a list"
defines cert_def: "c \<equiv> make_cert step \<phi> \<bottom>"
@@ -197,7 +197,7 @@
have "merge c pc ?step (c!Suc pc) =
(if \<forall>(pc',s')\<in>set ?step. pc'\<noteq>pc+1 \<longrightarrow> s' <=_r c!pc'
then map snd [(p',t') \<leftarrow> ?step.p'=pc+1] ++_f c!Suc pc
- else \<top>)" by (rule merge_def)
+ else \<top>)" unfolding merge_def by (rule lbv.merge_def [OF lbvc.axioms(1), OF lbvc_axioms])
moreover {
fix pc' s' assume s': "(pc', s') \<in> set ?step" and suc_pc: "pc' \<noteq> pc+1"
with less have "s' <=_r \<phi>!pc'" by auto
--- a/src/HOL/MicroJava/BV/LBVCorrect.thy Fri Jul 25 12:03:31 2008 +0200
+++ b/src/HOL/MicroJava/BV/LBVCorrect.thy Fri Jul 25 12:03:32 2008 +0200
@@ -6,9 +6,11 @@
header {* \isaheader{Correctness of the LBV} *}
-theory LBVCorrect imports LBVSpec Typing_Framework begin
+theory LBVCorrect
+imports LBVSpec Typing_Framework
+begin
-locale (open) lbvs = lbv +
+locale lbvs = lbv +
fixes s0 :: 'a ("s\<^sub>0")
fixes c :: "'a list"
fixes ins :: "'b list"
--- a/src/HOL/MicroJava/BV/LBVJVM.thy Fri Jul 25 12:03:31 2008 +0200
+++ b/src/HOL/MicroJava/BV/LBVJVM.thy Fri Jul 25 12:03:32 2008 +0200
@@ -122,7 +122,7 @@
moreover
from lbv have "0 < length ins" by (simp add: wt_lbv_def)
ultimately
- show ?thesis by (rule lbvs.wtl_sound_strong)
+ show ?thesis by (rule lbvs.wtl_sound_strong [OF lbvs.intro, OF lbv.intro lbvs_axioms.intro, OF Semilat.intro lbv_axioms.intro])
qed
lemma wt_lbv_wt_method:
@@ -274,7 +274,7 @@
note length
ultimately
have "wtl_inst_list ins ?cert ?f ?r Err (OK None) ?step 0 ?start \<noteq> Err"
- by (rule lbvc.wtl_complete)
+ by (rule lbvc.wtl_complete [OF lbvc.intro, OF lbv.intro lbvc_axioms.intro, OF Semilat.intro lbv_axioms.intro])
moreover
from 0 length have "phi \<noteq> []" by auto
moreover
--- a/src/HOL/MicroJava/BV/LBVSpec.thy Fri Jul 25 12:03:31 2008 +0200
+++ b/src/HOL/MicroJava/BV/LBVSpec.thy Fri Jul 25 12:03:32 2008 +0200
@@ -6,7 +6,9 @@
header {* \isaheader{The Lightweight Bytecode Verifier} *}
-theory LBVSpec imports SemilatAlg Opt begin
+theory LBVSpec
+imports SemilatAlg Opt
+begin
types
's certificate = "'s list"
@@ -51,7 +53,7 @@
"bottom r B \<equiv> \<forall>x. B <=_r x"
-locale (open) lbv = semilat +
+locale lbv = Semilat +
fixes T :: "'a" ("\<top>")
fixes B :: "'a" ("\<bottom>")
fixes step :: "'a step_type"
@@ -118,7 +120,7 @@
-lemma (in semilat) pp_ub1':
+lemma (in Semilat) pp_ub1':
assumes S: "snd`set S \<subseteq> A"
assumes y: "y \<in> A" and ab: "(a, b) \<in> set S"
shows "b <=_r map snd [(p', t') \<leftarrow> S . p' = a] ++_f y"
--- a/src/HOL/MicroJava/BV/Listn.thy Fri Jul 25 12:03:31 2008 +0200
+++ b/src/HOL/MicroJava/BV/Listn.thy Fri Jul 25 12:03:32 2008 +0200
@@ -283,21 +283,21 @@
done
-lemma (in semilat) plus_list_ub1 [rule_format]:
+lemma (in Semilat) plus_list_ub1 [rule_format]:
"\<lbrakk> set xs <= A; set ys <= A; size xs = size ys \<rbrakk>
\<Longrightarrow> xs <=[r] xs +[f] ys"
apply (unfold unfold_lesub_list)
apply (simp add: Listn.le_def list_all2_conv_all_nth)
done
-lemma (in semilat) plus_list_ub2:
+lemma (in Semilat) plus_list_ub2:
"\<lbrakk>set xs <= A; set ys <= A; size xs = size ys \<rbrakk>
\<Longrightarrow> ys <=[r] xs +[f] ys"
apply (unfold unfold_lesub_list)
apply (simp add: Listn.le_def list_all2_conv_all_nth)
done
-lemma (in semilat) plus_list_lub [rule_format]:
+lemma (in Semilat) plus_list_lub [rule_format]:
shows "!xs ys zs. set xs <= A \<longrightarrow> set ys <= A \<longrightarrow> set zs <= A
\<longrightarrow> size xs = n & size ys = n \<longrightarrow>
xs <=[r] zs & ys <=[r] zs \<longrightarrow> xs +[f] ys <=[r] zs"
@@ -305,7 +305,7 @@
apply (simp add: Listn.le_def list_all2_conv_all_nth)
done
-lemma (in semilat) list_update_incr [rule_format]:
+lemma (in Semilat) list_update_incr [rule_format]:
"x\<in> A \<Longrightarrow> set xs <= A \<longrightarrow>
(!i. i<size xs \<longrightarrow> xs <=[r] xs[i := x +_f xs!i])"
apply (unfold unfold_lesub_list)
@@ -380,7 +380,7 @@
lemma Listn_sl_aux:
assumes "semilat (A, r, f)" shows "semilat (Listn.sl n (A,r,f))"
proof -
- interpret semilat [A r f] by fact
+ interpret Semilat [A r f] using assms by (rule Semilat.intro)
show ?thesis
apply (unfold Listn.sl_def)
apply (simp (no_asm) only: semilat_Def split_conv)
@@ -517,9 +517,9 @@
apply (unfold Err.sl_def)
apply (simp only: split_conv)
apply (simp (no_asm) only: semilat_Def plussub_def)
-apply (simp (no_asm_simp) only: semilat.closedI closed_lift2_sup)
+apply (simp (no_asm_simp) only: Semilat.closedI [OF Semilat.intro] closed_lift2_sup)
apply (rule conjI)
- apply (drule semilat.orderI)
+ apply (drule Semilat.orderI [OF Semilat.intro])
apply simp
apply (simp (no_asm) only: unfold_lesub_err Err.le_def err_def sup_def lift2_def)
apply (simp (no_asm_simp) add: coalesce_eq_OK1_D coalesce_eq_OK2_D split: err.split)
--- a/src/HOL/MicroJava/BV/Product.thy Fri Jul 25 12:03:31 2008 +0200
+++ b/src/HOL/MicroJava/BV/Product.thy Fri Jul 25 12:03:32 2008 +0200
@@ -8,7 +8,9 @@
header {* \isaheader{Products as Semilattices} *}
-theory Product imports Err begin
+theory Product
+imports Err
+begin
constdefs
le :: "'a ord \<Rightarrow> 'b ord \<Rightarrow> ('a * 'b) ord"
@@ -79,13 +81,13 @@
have plus_le_conv2:
"\<And>r f z. \<lbrakk> z : err A; semilat (err A, r, f); OK x : err A; OK y : err A;
OK x +_f OK y <=_r z\<rbrakk> \<Longrightarrow> OK x <=_r z \<and> OK y <=_r z"
- by (rule semilat.plus_le_conv [THEN iffD1])
+ by (rule Semilat.plus_le_conv [OF Semilat.intro, THEN iffD1])
from prems show ?thesis
apply (rule_tac iffI)
apply clarify
apply (drule OK_le_err_OK [THEN iffD2])
apply (drule OK_le_err_OK [THEN iffD2])
- apply (drule semilat.lub[of _ _ _ "OK x" _ "OK y"])
+ apply (drule Semilat.lub [OF Semilat.intro, of _ _ _ "OK x" _ "OK y"])
apply assumption
apply assumption
apply simp
@@ -101,7 +103,7 @@
apply simp
apply blast
apply simp
- apply (blast dest: semilat.orderI order_refl)
+ apply (blast dest: Semilat.orderI [OF Semilat.intro] order_refl)
apply blast
apply (erule subst)
apply (unfold semilat_def err_def closed_def)
@@ -115,15 +117,15 @@
apply (simp (no_asm_simp) only: split_tupled_all)
apply simp
apply (simp (no_asm) only: semilat_Def)
-apply (simp (no_asm_simp) only: semilat.closedI closed_lift2_sup)
+apply (simp (no_asm_simp) only: Semilat.closedI [OF Semilat.intro] closed_lift2_sup)
apply (simp (no_asm) only: unfold_lesub_err Err.le_def unfold_plussub_lift2 sup_def)
apply (auto elim: semilat_le_err_OK1 semilat_le_err_OK2
simp add: lift2_def split: err.split)
-apply (blast dest: semilat.orderI)
-apply (blast dest: semilat.orderI)
+apply (blast dest: Semilat.orderI [OF Semilat.intro])
+apply (blast dest: Semilat.orderI [OF Semilat.intro])
apply (rule OK_le_err_OK [THEN iffD1])
-apply (erule subst, subst OK_lift2_OK [symmetric], rule semilat.lub)
+apply (erule subst, subst OK_lift2_OK [symmetric], rule Semilat.lub [OF Semilat.intro])
apply simp
apply simp
apply simp
@@ -132,7 +134,7 @@
apply simp
apply (rule OK_le_err_OK [THEN iffD1])
-apply (erule subst, subst OK_lift2_OK [symmetric], rule semilat.lub)
+apply (erule subst, subst OK_lift2_OK [symmetric], rule Semilat.lub [OF Semilat.intro])
apply simp
apply simp
apply simp
--- a/src/HOL/MicroJava/BV/Semilat.thy Fri Jul 25 12:03:31 2008 +0200
+++ b/src/HOL/MicroJava/BV/Semilat.thy Fri Jul 25 12:03:32 2008 +0200
@@ -71,7 +71,7 @@
some_lub :: "'a ord \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a"
"some_lub r x y == SOME z. is_lub r x y z";
-locale (open) semilat =
+locale Semilat =
fixes A :: "'a set"
and r :: "'a ord"
and f :: "'a binop"
@@ -122,11 +122,11 @@
apply (rule refl [THEN eq_reflection])
done
-lemma (in semilat) orderI [simp, intro]:
+lemma (in Semilat) orderI [simp, intro]:
"order r"
by (insert semilat) (simp add: semilat_Def)
-lemma (in semilat) closedI [simp, intro]:
+lemma (in Semilat) closedI [simp, intro]:
"closed A f"
by (insert semilat) (simp add: semilat_Def)
@@ -138,41 +138,41 @@
by (simp add: closed_def)
-lemma (in semilat) closed_f [simp, intro]:
+lemma (in Semilat) closed_f [simp, intro]:
"\<lbrakk>x:A; y:A\<rbrakk> \<Longrightarrow> x +_f y : A"
by (simp add: closedD [OF closedI])
-lemma (in semilat) refl_r [intro, simp]:
+lemma (in Semilat) refl_r [intro, simp]:
"x <=_r x"
by simp
-lemma (in semilat) antisym_r [intro?]:
+lemma (in Semilat) antisym_r [intro?]:
"\<lbrakk> x <=_r y; y <=_r x \<rbrakk> \<Longrightarrow> x = y"
by (rule order_antisym) auto
-lemma (in semilat) trans_r [trans, intro?]:
+lemma (in Semilat) trans_r [trans, intro?]:
"\<lbrakk>x <=_r y; y <=_r z\<rbrakk> \<Longrightarrow> x <=_r z"
by (auto intro: order_trans)
-lemma (in semilat) ub1 [simp, intro?]:
+lemma (in Semilat) ub1 [simp, intro?]:
"\<lbrakk> x:A; y:A \<rbrakk> \<Longrightarrow> x <=_r x +_f y"
by (insert semilat) (unfold semilat_Def, simp)
-lemma (in semilat) ub2 [simp, intro?]:
+lemma (in Semilat) ub2 [simp, intro?]:
"\<lbrakk> x:A; y:A \<rbrakk> \<Longrightarrow> y <=_r x +_f y"
by (insert semilat) (unfold semilat_Def, simp)
-lemma (in semilat) lub [simp, intro?]:
+lemma (in Semilat) lub [simp, intro?]:
"\<lbrakk> x <=_r z; y <=_r z; x:A; y:A; z:A \<rbrakk> \<Longrightarrow> x +_f y <=_r z";
by (insert semilat) (unfold semilat_Def, simp)
-lemma (in semilat) plus_le_conv [simp]:
+lemma (in Semilat) plus_le_conv [simp]:
"\<lbrakk> x:A; y:A; z:A \<rbrakk> \<Longrightarrow> (x +_f y <=_r z) = (x <=_r z & y <=_r z)"
by (blast intro: ub1 ub2 lub order_trans)
-lemma (in semilat) le_iff_plus_unchanged:
+lemma (in Semilat) le_iff_plus_unchanged:
"\<lbrakk> x:A; y:A \<rbrakk> \<Longrightarrow> (x <=_r y) = (x +_f y = y)"
apply (rule iffI)
apply (blast intro: antisym_r refl_r lub ub2)
@@ -180,7 +180,7 @@
apply simp
done
-lemma (in semilat) le_iff_plus_unchanged2:
+lemma (in Semilat) le_iff_plus_unchanged2:
"\<lbrakk> x:A; y:A \<rbrakk> \<Longrightarrow> (x <=_r y) = (y +_f x = y)"
apply (rule iffI)
apply (blast intro: order_antisym lub order_refl ub1)
@@ -189,7 +189,7 @@
done
-lemma (in semilat) plus_assoc [simp]:
+lemma (in Semilat) plus_assoc [simp]:
assumes a: "a \<in> A" and b: "b \<in> A" and c: "c \<in> A"
shows "a +_f (b +_f c) = a +_f b +_f c"
proof -
@@ -227,7 +227,7 @@
qed
qed
-lemma (in semilat) plus_com_lemma:
+lemma (in Semilat) plus_com_lemma:
"\<lbrakk>a \<in> A; b \<in> A\<rbrakk> \<Longrightarrow> a +_f b <=_r b +_f a"
proof -
assume a: "a \<in> A" and b: "b \<in> A"
@@ -238,7 +238,7 @@
ultimately show ?thesis ..
qed
-lemma (in semilat) plus_commutative:
+lemma (in Semilat) plus_commutative:
"\<lbrakk>a \<in> A; b \<in> A\<rbrakk> \<Longrightarrow> a +_f b = b +_f a"
by(blast intro: order_antisym plus_com_lemma)
--- a/src/HOL/MicroJava/BV/SemilatAlg.thy Fri Jul 25 12:03:31 2008 +0200
+++ b/src/HOL/MicroJava/BV/SemilatAlg.thy Fri Jul 25 12:03:32 2008 +0200
@@ -6,7 +6,9 @@
header {* \isaheader{More on Semilattices} *}
-theory SemilatAlg imports Typing_Framework Product begin
+theory SemilatAlg
+imports Typing_Framework Product
+begin
constdefs
@@ -65,7 +67,7 @@
lemma plusplus_closed: assumes "semilat (A, r, f)" shows
"\<And>y. \<lbrakk> set x \<subseteq> A; y \<in> A\<rbrakk> \<Longrightarrow> x ++_f y \<in> A" (is "PROP ?P")
proof -
- interpret semilat [A r f] by fact
+ interpret Semilat [A r f] using assms by (rule Semilat.intro)
show "PROP ?P" proof (induct x)
show "\<And>y. y \<in> A \<Longrightarrow> [] ++_f y \<in> A" by simp
fix y x xs
@@ -78,7 +80,7 @@
qed
qed
-lemma (in semilat) pp_ub2:
+lemma (in Semilat) pp_ub2:
"\<And>y. \<lbrakk> set x \<subseteq> A; y \<in> A\<rbrakk> \<Longrightarrow> y <=_r x ++_f y"
proof (induct x)
from semilat show "\<And>y. y <=_r [] ++_f y" by simp
@@ -98,7 +100,7 @@
qed
-lemma (in semilat) pp_ub1:
+lemma (in Semilat) pp_ub1:
shows "\<And>y. \<lbrakk>set ls \<subseteq> A; y \<in> A; x \<in> set ls\<rbrakk> \<Longrightarrow> x <=_r ls ++_f y"
proof (induct ls)
show "\<And>y. x \<in> set [] \<Longrightarrow> x <=_r [] ++_f y" by simp
@@ -134,7 +136,7 @@
qed
-lemma (in semilat) pp_lub:
+lemma (in Semilat) pp_lub:
assumes z: "z \<in> A"
shows
"\<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"
@@ -162,7 +164,7 @@
shows "\<lbrakk>\<forall>(p,s) \<in> set S. s \<in> A; y \<in> A; (a,b) \<in> set S\<rbrakk>
\<Longrightarrow> b <=_r map snd [(p', t')\<leftarrow>S. p' = a] ++_f y"
proof -
- interpret semilat [A r f] by fact
+ interpret Semilat [A r f] using assms by (rule Semilat.intro)
let "b <=_r ?map ++_f y" = ?thesis
--- a/src/HOL/NSA/Filter.thy Fri Jul 25 12:03:31 2008 +0200
+++ b/src/HOL/NSA/Filter.thy Fri Jul 25 12:03:32 2008 +0200
@@ -196,7 +196,7 @@
subsection {* Ultrafilter Theorem *}
text "A locale makes proof of ultrafilter Theorem more modular"
-locale (open) UFT =
+locale UFT =
fixes frechet :: "'a set set"
and superfrechet :: "'a set set set"
@@ -402,7 +402,7 @@
qed
qed
-lemmas freeultrafilter_Ex = UFT.freeultrafilter_ex
+lemmas freeultrafilter_Ex = UFT.freeultrafilter_ex [OF UFT.intro]
hide (open) const filter
--- a/src/HOL/Statespace/state_space.ML Fri Jul 25 12:03:31 2008 +0200
+++ b/src/HOL/Statespace/state_space.ML Fri Jul 25 12:03:32 2008 +0200
@@ -312,7 +312,7 @@
([]))])];
in thy
- |> Locale.add_locale_i (SOME "") name vars [assumes]
+ |> Locale.add_locale_i "" name vars [assumes]
||> ProofContext.theory_of
||> interprete_parent name dist_thm_full_name parent_expr
|> #2
@@ -459,11 +459,11 @@
(suffix namespaceN name) nameT parents_expr
(map fst parent_comps) (map fst components)
|> Context.theory_map (add_statespace full_name args parents components [])
- |> Locale.add_locale_i (SOME "") (suffix valuetypesN name) (Locale.Merge locs)
+ |> Locale.add_locale_i "" (suffix valuetypesN name) (Locale.Merge locs)
[Element.Constrains constrains]
|> ProofContext.theory_of o #2
|> fold interprete_parent_valuetypes parents
- |> Locale.add_locale (SOME "") name
+ |> Locale.add_locale "" name
(Locale.Merge [Locale.Locale (suffix namespaceN full_name)
,Locale.Locale (suffix valuetypesN full_name)]) fixestate
|> ProofContext.theory_of o #2
--- a/src/HOL/ex/Tarski.thy Fri Jul 25 12:03:31 2008 +0200
+++ b/src/HOL/ex/Tarski.thy Fri Jul 25 12:03:32 2008 +0200
@@ -5,7 +5,9 @@
header {* The Full Theorem of Tarski *}
-theory Tarski imports Main FuncSet begin
+theory Tarski
+imports Main FuncSet
+begin
text {*
Minimal version of lattice theory plus the full theorem of Tarski:
@@ -81,8 +83,8 @@
(\<forall>S. S \<subseteq> pset cl --> (\<exists>G. isGlb S cl G))}"
definition
- CLF :: "('a potype * ('a => 'a)) set" where
- "CLF = (SIGMA cl: CompleteLattice.
+ CLF_set :: "('a potype * ('a => 'a)) set" where
+ "CLF_set = (SIGMA cl: CompleteLattice.
{f. f: pset cl -> pset cl & monotone f (pset cl) (order cl)})"
definition
@@ -105,25 +107,36 @@
dual :: "'a potype => 'a potype" where
"dual po = (| pset = pset po, order = converse (order po) |)"
-locale (open) PO =
+locale S =
fixes cl :: "'a potype"
and A :: "'a set"
and r :: "('a * 'a) set"
- assumes cl_po: "cl : PartialOrder"
defines A_def: "A == pset cl"
and r_def: "r == order cl"
-locale (open) CL = PO +
+locale PO = S +
+ assumes cl_po: "cl : PartialOrder"
+
+locale CL = S +
assumes cl_co: "cl : CompleteLattice"
-locale (open) CLF = CL +
+interpretation CL < PO
+apply (simp_all add: A_def r_def)
+apply unfold_locales
+using cl_co unfolding CompleteLattice_def by auto
+
+locale CLF = S +
fixes f :: "'a => 'a"
and P :: "'a set"
- assumes f_cl: "(cl,f) : CLF" (*was the equivalent "f : CLF``{cl}"*)
+ assumes f_cl: "(cl,f) : CLF_set" (*was the equivalent "f : CLF_set``{cl}"*)
defines P_def: "P == fix f A"
+interpretation CLF < CL
+apply (simp_all add: A_def r_def)
+apply unfold_locales
+using f_cl unfolding CLF_set_def by auto
-locale (open) Tarski = CLF +
+locale Tarski = CLF +
fixes Y :: "'a set"
and intY1 :: "'a set"
and v :: "'a"
@@ -138,17 +151,24 @@
subsection {* Partial Order *}
-lemma (in PO) PO_imp_refl: "refl A r"
+lemma (in PO) dual:
+ "PO (dual cl)"
+apply unfold_locales
+using cl_po
+unfolding PartialOrder_def dual_def
+by auto
+
+lemma (in PO) PO_imp_refl [simp]: "refl A r"
apply (insert cl_po)
apply (simp add: PartialOrder_def A_def r_def)
done
-lemma (in PO) PO_imp_sym: "antisym r"
+lemma (in PO) PO_imp_sym [simp]: "antisym r"
apply (insert cl_po)
apply (simp add: PartialOrder_def r_def)
done
-lemma (in PO) PO_imp_trans: "trans r"
+lemma (in PO) PO_imp_trans [simp]: "trans r"
apply (insert cl_po)
apply (simp add: PartialOrder_def r_def)
done
@@ -242,9 +262,9 @@
lemmas CL_imp_PO = CL_subset_PO [THEN subsetD]
-declare CL_imp_PO [THEN PO.PO_imp_refl, simp]
+(*declare CL_imp_PO [THEN PO.PO_imp_refl, simp]
declare CL_imp_PO [THEN PO.PO_imp_sym, simp]
-declare CL_imp_PO [THEN PO.PO_imp_trans, simp]
+declare CL_imp_PO [THEN PO.PO_imp_trans, simp]*)
lemma (in CL) CO_refl: "refl A r"
by (rule PO_imp_refl)
@@ -287,11 +307,15 @@
apply (fold r_def, fast)
done
+lemma (in PO) trans:
+ "(x, y) \<in> r \<Longrightarrow> (y, z) \<in> r \<Longrightarrow> (x, z) \<in> r"
+using cl_po apply (auto simp add: PartialOrder_def r_def)
+unfolding trans_def by blast
+
lemma (in PO) interval_not_empty:
- "[| trans r; interval r a b \<noteq> {} |] ==> (a, b) \<in> r"
+ "interval r a b \<noteq> {} ==> (a, b) \<in> r"
apply (simp add: interval_def)
-apply (unfold trans_def, blast)
-done
+using trans by blast
lemma (in PO) interval_imp_mem: "x \<in> interval r a b ==> (a, x) \<in> r"
by (simp add: interval_def)
@@ -322,6 +346,13 @@
==> S <<= cl"
by (simp add: sublattice_def A_def r_def)
+lemma (in CL) dual:
+ "CL (dual cl)"
+apply unfold_locales
+using cl_co unfolding CompleteLattice_def
+apply (simp add: dualPO isGlb_dual_isLub [symmetric] isLub_dual_isGlb [symmetric] dualA_iff)
+done
+
subsection {* lub *}
@@ -396,8 +427,7 @@
apply (simp add: A_def)
apply (rule dualA_iff [THEN subst])
apply (rule CL.lub_in_lattice)
-apply (rule dualPO)
-apply (rule CL_dualCL)
+apply (rule dual)
apply (simp add: dualA_iff)
done
@@ -406,8 +436,7 @@
apply (simp add: r_def)
apply (rule dualr_iff [THEN subst])
apply (rule CL.lub_upper)
-apply (rule dualPO)
-apply (rule CL_dualCL)
+apply (rule dual)
apply (simp add: dualA_iff A_def, assumption)
done
@@ -419,7 +448,7 @@
lemma (in CLF) [simp]:
"f: pset cl -> pset cl & monotone f (pset cl) (order cl)"
apply (insert f_cl)
-apply (simp add: CLF_def)
+apply (simp add: CLF_set_def)
done
declare (in CLF) f_cl [simp]
@@ -431,11 +460,17 @@
lemma (in CLF) monotone_f: "monotone f A r"
by (simp add: A_def r_def)
-lemma (in CLF) CLF_dual: "(dual cl, f) \<in> CLF"
-apply (simp add: CLF_def CL_dualCL monotone_dual)
+lemma (in CLF) CLF_dual: "(dual cl, f) \<in> CLF_set"
+apply (simp add: CLF_set_def CL_dualCL monotone_dual)
apply (simp add: dualA_iff)
done
+lemma (in CLF) dual:
+ "CLF (dual cl) f"
+apply (rule CLF.intro)
+apply (rule CLF_dual)
+done
+
subsection {* fixed points *}
@@ -534,16 +569,14 @@
apply (simp add: glb_dual_lub P_def A_def r_def)
apply (rule dualA_iff [THEN subst])
apply (rule CLF.lubH_is_fixp)
-apply (rule dualPO)
-apply (rule CL_dualCL)
-apply (rule CLF_dual)
+apply (rule dual)
apply (simp add: dualr_iff dualA_iff)
done
lemma (in CLF) T_thm_1_glb: "glb P cl = glb {x. (f x, x) \<in> r & x \<in> A} cl"
apply (simp add: glb_dual_lub P_def A_def r_def)
apply (rule dualA_iff [THEN subst])
-apply (simp add: CLF.T_thm_1_lub [of _ f, OF dualPO CL_dualCL]
+apply (simp add: CLF.T_thm_1_lub [of _ f, OF dual]
dualPO CL_dualCL CLF_dual dualr_iff)
done
@@ -603,8 +636,8 @@
"[| a \<in> A; b \<in> A; interval r a b \<noteq> {}; S \<subseteq> interval r a b; isGlb S cl G;
S \<noteq> {} |] ==> G \<in> interval r a b"
apply (simp add: interval_dual)
-apply (simp add: CLF.L_in_interval [of _ f]
- dualA_iff A_def dualPO CL_dualCL CLF_dual isGlb_dual_isLub)
+apply (simp add: CLF.L_in_interval [of _ f, OF dual]
+ dualA_iff A_def isGlb_dual_isLub)
done
lemma (in CLF) intervalPO:
@@ -655,7 +688,6 @@
apply (rule conjI)
apply (rule reflE, assumption)
apply (rule interval_not_empty)
-apply (rule CO_trans)
apply (simp add: interval_def)
-- {* @{text "S \<noteq> {}"} *}
apply simp
@@ -700,7 +732,7 @@
lemma (in CLF) Top_in_lattice: "Top cl \<in> A"
apply (simp add: Top_dual_Bot A_def)
apply (rule dualA_iff [THEN subst])
-apply (blast intro!: CLF.Bot_in_lattice dualPO CL_dualCL CLF_dual)
+apply (rule CLF.Bot_in_lattice [OF dual])
done
lemma (in CLF) Top_prop: "x \<in> A ==> (x, Top cl) \<in> r"
@@ -714,8 +746,8 @@
lemma (in CLF) Bot_prop: "x \<in> A ==> (Bot cl, x) \<in> r"
apply (simp add: Bot_dual_Top r_def)
apply (rule dualr_iff [THEN subst])
-apply (simp add: CLF.Top_prop [of _ f]
- dualA_iff A_def dualPO CL_dualCL CLF_dual)
+apply (rule CLF.Top_prop [OF dual])
+apply (simp add: dualA_iff A_def)
done
lemma (in CLF) Top_intv_not_empty: "x \<in> A ==> interval r x (Top cl) \<noteq> {}"
@@ -731,9 +763,9 @@
prefer 2 apply assumption
apply (simp add: A_def)
apply (rule dualA_iff [THEN subst])
-apply (blast intro!: CLF.Top_in_lattice dualPO CL_dualCL CLF_dual)
-apply (simp add: CLF.Top_intv_not_empty [of _ f]
- dualA_iff A_def dualPO CL_dualCL CLF_dual)
+apply (rule CLF.Top_in_lattice [OF dual])
+apply (rule CLF.Top_intv_not_empty [OF dual])
+apply (simp add: dualA_iff A_def)
done
subsection {* fixed points form a partial order *}
@@ -817,8 +849,12 @@
apply (unfold P_def)
apply (rule_tac A = "intY1" in fixf_subset)
apply (rule intY1_subset)
-apply (simp add: CLF.glbH_is_fixp [OF _ intY1_is_cl, simplified]
- v_def CL_imp_PO intY1_is_cl CLF_def intY1_func intY1_mono)
+unfolding v_def
+apply (rule CLF.glbH_is_fixp [OF CLF.intro, unfolded CLF_set_def, of "\<lparr>pset = intY1, order = induced intY1 r\<rparr>", simplified])
+apply auto
+apply (rule intY1_is_cl)
+apply (rule intY1_func)
+apply (rule intY1_mono)
done
lemma (in Tarski) z_in_interval:
@@ -859,17 +895,15 @@
apply (rule_tac b = "Top cl" in interval_imp_mem)
apply (simp add: v_def)
apply (fold intY1_def)
-apply (rule CL.glb_in_lattice [OF _ intY1_is_cl, simplified])
- apply (simp add: CL_imp_PO intY1_is_cl, force)
--- {* @{text v} is LEAST ub *}
-apply clarify
+apply (rule CL.glb_in_lattice [OF CL.intro [OF intY1_is_cl], simplified])
+apply auto
apply (rule indI)
prefer 3 apply assumption
prefer 2 apply (simp add: v_in_P)
apply (unfold v_def)
apply (rule indE)
apply (rule_tac [2] intY1_subset)
-apply (rule CL.glb_lower [OF _ intY1_is_cl, simplified])
+apply (rule CL.glb_lower [OF CL.intro [OF intY1_is_cl], simplified])
apply (simp add: CL_imp_PO intY1_is_cl)
apply force
apply (simp add: induced_def intY1_f_closed z_in_interval)
@@ -888,7 +922,7 @@
apply (rule CompleteLatticeI_simp)
apply (rule fixf_po, clarify)
apply (simp add: P_def A_def r_def)
-apply (blast intro!: Tarski.tarski_full_lemma cl_po cl_co f_cl)
-done
+apply (rule Tarski.tarski_full_lemma [OF Tarski.intro [OF _ Tarski_axioms.intro]])
+proof - show "CLF cl f" by unfold_locales qed
end
--- a/src/HOLCF/Deflation.thy Fri Jul 25 12:03:31 2008 +0200
+++ b/src/HOLCF/Deflation.thy Fri Jul 25 12:03:32 2008 +0200
@@ -323,7 +323,7 @@
apply (erule ep_pair.e_p_less)
done
-locale (open) pcpo_ep_pair = ep_pair +
+locale pcpo_ep_pair = ep_pair +
constrains e :: "'a::pcpo \<rightarrow> 'b::pcpo"
constrains p :: "'b::pcpo \<rightarrow> 'a::pcpo"
begin
--- a/src/Pure/Isar/isar_syn.ML Fri Jul 25 12:03:31 2008 +0200
+++ b/src/Pure/Isar/isar_syn.ML Fri Jul 25 12:03:32 2008 +0200
@@ -387,11 +387,10 @@
val _ =
OuterSyntax.command "locale" "define named proof context" K.thy_decl
- ((P.opt_keyword "open" >> (fn true => NONE | false => SOME "")) --
- P.name -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (Locale.empty, []) -- P.opt_begin
- >> (fn (((is_open, name), (expr, elems)), begin) =>
+ (P.name -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (Locale.empty, []) -- P.opt_begin
+ >> (fn ((name, (expr, elems)), begin) =>
(begin ? Toplevel.print) o Toplevel.begin_local_theory begin
- (Locale.add_locale is_open name expr elems #-> TheoryTarget.begin)));
+ (Locale.add_locale "" name expr elems #-> TheoryTarget.begin)));
val _ =
OuterSyntax.command "interpretation"
--- a/src/Pure/Isar/locale.ML Fri Jul 25 12:03:31 2008 +0200
+++ b/src/Pure/Isar/locale.ML Fri Jul 25 12:03:32 2008 +0200
@@ -81,9 +81,9 @@
val print_locale: theory -> bool -> expr -> Element.context list -> unit
val print_registrations: bool -> string -> Proof.context -> unit
- val add_locale: string option -> bstring -> expr -> Element.context list -> theory
+ val add_locale: string -> bstring -> expr -> Element.context list -> theory
-> string * Proof.context
- val add_locale_i: string option -> bstring -> expr -> Element.context_i list -> theory
+ val add_locale_i: string -> bstring -> expr -> Element.context_i list -> theory
-> string * Proof.context
(* Tactics *)
@@ -122,27 +122,11 @@
(* legacy operations *)
-fun gen_merge_lists _ xs [] = xs
- | gen_merge_lists _ [] ys = ys
- | gen_merge_lists eq xs ys = xs @ filter_out (member eq xs) ys;
-
-fun merge_lists xs ys = gen_merge_lists (op =) xs ys;
-fun merge_alists xs = gen_merge_lists (eq_fst (op =)) xs;
-
-fun legacy_unvarifyT thm =
- let
- val cT = Thm.ctyp_of (Thm.theory_of_thm thm);
- val tvars = rev (Thm.fold_terms Term.add_tvars thm []);
- val tfrees = map (fn ((x, _), S) => SOME (cT (TFree (x, S)))) tvars;
- in Drule.instantiate' tfrees [] thm end;
-
-fun legacy_unvarify raw_thm =
- let
- val thm = legacy_unvarifyT raw_thm;
- val ct = Thm.cterm_of (Thm.theory_of_thm thm);
- val vars = rev (Thm.fold_terms Term.add_vars thm []);
- val frees = map (fn ((x, _), T) => SOME (ct (Free (x, T)))) vars;
- in Drule.instantiate' [] frees thm end;
+fun merge_lists _ xs [] = xs
+ | merge_lists _ [] ys = ys
+ | merge_lists eq xs ys = xs @ filter_out (member eq xs) ys;
+
+fun merge_alists eq xs = merge_lists (eq_fst eq) xs;
(** locale elements and expressions **)
@@ -370,13 +354,13 @@
{elems = elems', decls = (decls1', decls2'), regs = regs', ...}: locale) =
{axiom = axiom,
imports = imports,
- elems = gen_merge_lists (eq_snd (op =)) elems elems',
+ elems = merge_lists (eq_snd (op =)) elems elems',
params = params,
lparams = lparams,
decls =
(Library.merge (eq_snd (op =)) (decls1, decls1'),
Library.merge (eq_snd (op =)) (decls2, decls2')),
- regs = merge_alists regs regs',
+ regs = merge_alists (op =) regs regs',
intros = intros,
dests = dests};
fun merge _ ((space1, locs1), (space2, locs2)) =
@@ -398,29 +382,18 @@
(** access locales **)
-fun print_locales thy =
- let val (space, locs) = LocalesData.get thy in
- Pretty.strs ("locales:" :: map #1 (NameSpace.extern_table (space, locs)))
- |> Pretty.writeln
- end;
-
val intern = NameSpace.intern o #1 o LocalesData.get;
val extern = NameSpace.extern o #1 o LocalesData.get;
-fun declare_locale name thy =
+fun get_locale thy name = Symtab.lookup (#2 (LocalesData.get thy)) name;
+
+fun the_locale thy name = case get_locale thy name
+ of SOME loc => loc
+ | NONE => error ("Unknown locale " ^ quote name);
+
+fun add_locale name loc thy =
thy |> LocalesData.map (fn (space, locs) =>
- (Sign.declare_name thy name space, locs));
-
-fun put_locale name loc =
- LocalesData.map (fn (space, locs) =>
- (space, Symtab.update (name, loc) locs));
-
-fun get_locale thy name = Symtab.lookup (#2 (LocalesData.get thy)) name;
-
-fun the_locale thy name =
- (case get_locale thy name of
- SOME loc => loc
- | NONE => error ("Unknown locale " ^ quote name));
+ (Sign.declare_name thy name space, Symtab.update (name, loc) locs));
fun change_locale name f thy =
let
@@ -429,9 +402,16 @@
val (axiom', imports', elems', params', lparams', decls', regs', intros', dests') =
f (axiom, imports, elems, params, lparams, decls, regs, intros, dests);
in
- put_locale name {axiom = axiom', imports = imports', elems = elems',
- params = params', lparams = lparams', decls = decls', regs = regs',
- intros = intros', dests = dests'} thy
+ thy
+ |> (LocalesData.map o apsnd) (Symtab.update (name, {axiom = axiom',
+ imports = imports', elems = elems', params = params', lparams = lparams',
+ decls = decls', regs = regs', intros = intros', dests = dests'}))
+ end;
+
+fun print_locales thy =
+ let val (space, locs) = LocalesData.get thy in
+ Pretty.strs ("locales:" :: map #1 (NameSpace.extern_table (space, locs)))
+ |> Pretty.writeln
end;
@@ -754,7 +734,7 @@
val {imports, params, ...} = the_locale thy name;
val parms = map (fst o fst) params;
val (parms', types', syn') = params_of imports;
- val all_parms = merge_lists parms' parms;
+ val all_parms = merge_lists (op =) parms' parms;
val all_types = merge_tenvs [] types' (params |> map fst |> Symtab.make);
val all_syn = merge_syn expr syn' (params |> map (apfst fst) |> Symtab.make);
in (all_parms, all_types, all_syn) end
@@ -782,14 +762,14 @@
let
val (parms', types', syn') = params_of e
in
- (merge_lists parms parms', merge_tenvs [] types types',
+ (merge_lists (op =) parms parms', merge_tenvs [] types types',
merge_syn e syn syn')
end)
es ([], Symtab.empty, Symtab.empty)
val (parms, types, syn) = params_of expr;
in
- (merge_lists prev_parms parms, merge_tenvs fixed_params prev_types types,
+ (merge_lists (op =) prev_parms parms, merge_tenvs fixed_params prev_types types,
merge_syn expr prev_syn syn)
end;
@@ -901,7 +881,7 @@
val (_, ids'', _) = add_with_regs ((name, map #1 params), Assumed []) ([], ids', ids');
val ids_ax = if top then fst (fold_map (axiomify ps) ids'' axiom) else ids'';
- in (ids_ax, merge_lists parms' ps) end
+ in (ids_ax, merge_lists (op =) parms' ps) end
| identify top (Rename (e, xs)) =
let
val (ids', parms') = identify top e;
@@ -916,7 +896,7 @@
let
val (ids', parms') = identify top e
in
- (merge_alists ids ids', merge_lists parms parms')
+ (merge_alists (op =) ids ids', merge_lists (op =) parms parms')
end)
es ([], []);
@@ -969,11 +949,11 @@
(* NB: derived ids contain only facts at this stage *)
-fun activate_elem _ _ ((ctxt, mode), Fixes fixes) =
- ((ctxt |> ProofContext.add_fixes_i fixes |> snd, mode), [])
- | activate_elem _ _ ((ctxt, mode), Constrains _) =
- ((ctxt, mode), [])
- | activate_elem ax_in_ctxt _ ((ctxt, Assumed axs), Assumes asms) =
+fun activate_elem _ _ (Fixes fixes) (ctxt, mode) =
+ ([], (ctxt |> ProofContext.add_fixes_i fixes |> snd, mode))
+ | activate_elem _ _ (Constrains _) (ctxt, mode) =
+ ([], (ctxt, mode))
+ | activate_elem ax_in_ctxt _ (Assumes asms) (ctxt, Assumed axs) =
let
val asms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) asms;
val ts = maps (map #1 o #2) asms';
@@ -981,10 +961,10 @@
val (_, ctxt') =
ctxt |> fold Variable.auto_fixes ts
|> ProofContext.add_assms_i (axioms_export (if ax_in_ctxt then ps else [])) asms';
- in ((ctxt', Assumed qs), []) end
- | activate_elem _ _ ((ctxt, Derived ths), Assumes asms) =
- ((ctxt, Derived ths), [])
- | activate_elem _ _ ((ctxt, Assumed axs), Defines defs) =
+ in ([], (ctxt', Assumed qs)) end
+ | activate_elem _ _ (Assumes asms) (ctxt, Derived ths) =
+ ([], (ctxt, Derived ths))
+ | activate_elem _ _ (Defines defs) (ctxt, Assumed axs) =
let
val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs;
val asms = defs' |> map (fn ((name, atts), (t, ps)) =>
@@ -993,21 +973,20 @@
val (_, ctxt') =
ctxt |> fold (Variable.auto_fixes o #1) asms
|> ProofContext.add_assms_i LocalDefs.def_export (map #2 asms);
- in ((ctxt', Assumed axs), []) end
- | activate_elem _ _ ((ctxt, Derived ths), Defines defs) =
- ((ctxt, Derived ths), [])
- | activate_elem _ is_ext ((ctxt, mode), Notes (kind, facts)) =
+ in ([], (ctxt', Assumed axs)) end
+ | activate_elem _ _ (Defines defs) (ctxt, Derived ths) =
+ ([], (ctxt, Derived ths))
+ | activate_elem _ is_ext (Notes (kind, facts)) (ctxt, mode) =
let
val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts;
val (res, ctxt') = ctxt |> ProofContext.note_thmss_i kind facts';
- in ((ctxt', mode), if is_ext then res else []) end;
+ in (if is_ext then res else [], (ctxt', mode)) end;
fun activate_elems ax_in_ctxt (((name, ps), mode), elems) ctxt =
let
val thy = ProofContext.theory_of ctxt;
- val ((ctxt', _), res) =
- foldl_map (activate_elem ax_in_ctxt (name = ""))
- ((ProofContext.qualified_names ctxt, mode), elems)
+ val (res, (ctxt', _)) = fold_map (activate_elem ax_in_ctxt (name = ""))
+ elems (ProofContext.qualified_names ctxt, mode)
handle ERROR msg => err_in_locale ctxt msg [(name, map fst ps)];
val ctxt'' = if name = "" then ctxt'
else let
@@ -1037,10 +1016,10 @@
in
-(* CB: activate_facts prep_facts (ctxt, elemss),
+(* CB: activate_facts prep_facts elemss ctxt,
where elemss is a list of pairs consisting of identifiers and
context elements, extends ctxt by the context elements yielding
- ctxt' and returns (ctxt', (elemss', facts)).
+ ctxt' and returns ((elemss', facts), ctxt').
Identifiers in the argument are of the form ((name, ps), axs) and
assumptions use the axioms in the identifiers to set up exporters
in ctxt'. elemss' does not contain identifiers and is obtained
@@ -1048,9 +1027,9 @@
If read_facts or cert_facts is used for prep_facts, these also remove
the internal/external markers from elemss. *)
-fun activate_facts ax_in_ctxt prep_facts (ctxt, args) =
- let val ((elemss, factss), ctxt') = activate_elemss ax_in_ctxt prep_facts args ctxt |>> split_list
- in (ctxt', (elemss, flat factss)) end;
+fun activate_facts ax_in_ctxt prep_facts args =
+ activate_elemss ax_in_ctxt prep_facts args
+ #>> (apsnd flat o split_list);
end;
@@ -1107,29 +1086,26 @@
local
-fun declare_int_elem (ctxt, Fixes fixes) =
- (ctxt |> ProofContext.add_fixes_i (map (fn (x, T, mx) =>
- (x, Option.map (Term.map_type_tfree (TypeInfer.param 0)) T, mx)) fixes) |> snd, [])
- | declare_int_elem (ctxt, _) = (ctxt, []);
-
-fun declare_ext_elem prep_vars (ctxt, Fixes fixes) =
+fun declare_int_elem (Fixes fixes) ctxt =
+ ([], ctxt |> ProofContext.add_fixes_i (map (fn (x, T, mx) =>
+ (x, Option.map (Term.map_type_tfree (TypeInfer.param 0)) T, mx)) fixes) |> snd)
+ | declare_int_elem _ ctxt = ([], ctxt);
+
+fun declare_ext_elem prep_vars (Fixes fixes) ctxt =
let val (vars, _) = prep_vars fixes ctxt
- in (ctxt |> ProofContext.add_fixes_i vars |> snd, []) end
- | declare_ext_elem prep_vars (ctxt, Constrains csts) =
+ in ([], ctxt |> ProofContext.add_fixes_i vars |> snd) end
+ | declare_ext_elem prep_vars (Constrains csts) ctxt =
let val (_, ctxt') = prep_vars (map (fn (x, T) => (x, SOME T, NoSyn)) csts) ctxt
- in (ctxt', []) end
- | declare_ext_elem _ (ctxt, Assumes asms) = (ctxt, map #2 asms)
- | declare_ext_elem _ (ctxt, Defines defs) = (ctxt, map (fn (_, (t, ps)) => [(t, ps)]) defs)
- | declare_ext_elem _ (ctxt, Notes _) = (ctxt, []);
-
-fun declare_elems prep_vars (ctxt, (((name, ps), Assumed _), elems)) =
- let val (ctxt', propps) =
- (case elems of
- Int es => foldl_map declare_int_elem (ctxt, es)
- | Ext e => foldl_map (declare_ext_elem prep_vars) (ctxt, [e]))
- handle ERROR msg => err_in_locale ctxt msg [(name, map fst ps)]
- in (ctxt', propps) end
- | declare_elems _ (ctxt, ((_, Derived _), elems)) = (ctxt, []);
+ in ([], ctxt') end
+ | declare_ext_elem _ (Assumes asms) ctxt = (map #2 asms, ctxt)
+ | declare_ext_elem _ (Defines defs) ctxt = (map (fn (_, (t, ps)) => [(t, ps)]) defs, ctxt)
+ | declare_ext_elem _ (Notes _) ctxt = ([], ctxt);
+
+fun declare_elems prep_vars (((name, ps), Assumed _), elems) ctxt = ((case elems
+ of Int es => fold_map declare_int_elem es ctxt
+ | Ext e => declare_ext_elem prep_vars e ctxt |>> single)
+ handle ERROR msg => err_in_locale ctxt msg [(name, map fst ps)])
+ | declare_elems _ ((_, Derived _), elems) ctxt = ([], ctxt);
in
@@ -1144,10 +1120,10 @@
raw_elemss
|> map_filter (fn (id, Int es) => SOME (id, es) | _ => NONE)
|> unify_elemss ctxt_with_fixed fixed_params;
- val (_, raw_elemss') =
- foldl_map (fn ((_, es) :: elemss, (id, Int _)) => (elemss, (id, Int es)) | x => x)
- (int_elemss, raw_elemss);
- in foldl_map (declare_elems prep_vars) (ctxt, raw_elemss') end;
+ val (raw_elemss', _) =
+ fold_map (curry (fn ((id, Int _), (_, es) :: elemss) => ((id, Int es), elemss) | x => x))
+ raw_elemss int_elemss;
+ in fold_map (declare_elems prep_vars) raw_elemss' ctxt end;
end;
@@ -1325,7 +1301,7 @@
(* CB: raw_elemss are list of pairs consisting of identifiers and
context elements, the latter marked as internal or external. *)
val raw_elemss = rem_dup_defines raw_elemss;
- val (raw_ctxt, raw_proppss) = declare_elemss prep_vars fixed_params raw_elemss context;
+ val (raw_proppss, raw_ctxt) = declare_elemss prep_vars fixed_params raw_elemss context;
(* CB: raw_ctxt is context with additional fixed variables derived from
the fixes elements in raw_elemss,
raw_proppss contains assumptions and definitions from the
@@ -1512,11 +1488,11 @@
(* CB: all_elemss and parms contain the correct parameter types *)
val (ps, qs) = chop (length raw_import_params_elemss + length raw_import_elemss) all_elemss';
- val (import_ctxt, (import_elemss, _)) =
- activate_facts false prep_facts (context, ps);
-
- val (ctxt, (elemss, _)) =
- activate_facts false prep_facts (ProofContext.set_stmt true import_ctxt, qs);
+ val ((import_elemss, _), import_ctxt) =
+ activate_facts false prep_facts ps context;
+
+ val ((elemss, _), ctxt) =
+ activate_facts false prep_facts qs (ProofContext.set_stmt true import_ctxt);
in
((((import_ctxt, import_elemss), (ctxt, elemss, syn)),
(parms, spec, defs)), concl)
@@ -1707,9 +1683,9 @@
fun add_thmss loc kind args ctxt =
let
- val (ctxt', ([(_, [Notes args'])], _)) =
+ val (([(_, [Notes args'])], _), ctxt') =
activate_facts true cert_facts
- (ctxt, [((("", []), Assumed []), [Ext (Notes (kind, args))])]);
+ [((("", []), Assumed []), [Ext (Notes (kind, args))])] ctxt;
val ctxt'' = ctxt' |> ProofContext.theory
(change_locale loc
(fn (axiom, imports, elems, params, lparams, decls, regs, intros, dests) =>
@@ -1923,20 +1899,19 @@
fun gen_add_locale prep_ctxt prep_expr
predicate_name bname raw_imports raw_body thy =
- (* predicate_name: NONE - open locale without predicate
- SOME "" - locale with predicate named as locale
- SOME "name" - locale with predicate named "name" *)
+ (* predicate_name: "" - locale with predicate named as locale
+ "name" - locale with predicate named "name" *)
let
+ val thy_ctxt = ProofContext.init thy;
val name = Sign.full_name thy bname;
val _ = is_some (get_locale thy name) andalso
error ("Duplicate definition of locale " ^ quote name);
- val thy_ctxt = ProofContext.init thy;
val (((import_ctxt, import_elemss), (body_ctxt, body_elemss, syn)),
text as (parms, ((_, exts'), _), defs)) =
- prep_ctxt raw_imports raw_body thy_ctxt;
+ prep_ctxt raw_imports raw_body thy_ctxt;
val elemss = import_elemss @ body_elemss |>
- map_filter (fn ((id, Assumed axs), elems) => SOME (id, elems) | _ => NONE);
+ map_filter (fn ((id, Assumed axs), elems) => SOME (id, elems) | _ => NONE);
val imports = prep_expr thy raw_imports;
val extraTs = List.foldr Term.add_term_tfrees [] exts' \\
@@ -1944,27 +1919,18 @@
val _ = if null extraTs then ()
else warning ("Additional type variable(s) in locale specification " ^ quote bname);
- val ((((elemss', predicate as (predicate_statement, predicate_axioms), stmt'), intros),
- pred_thy), (imports, regs)) =
- case predicate_name
- of SOME predicate_name =>
- let
- val predicate_name' = case predicate_name of "" => bname | _ => predicate_name;
- val (elemss', defns) = change_defines_elemss thy elemss [];
- val elemss'' = elemss' @ [(("", []), defns)];
- val (((elemss''', predicate as (_, axioms), stmt'), intros), thy') =
- define_preds predicate_name' text elemss'' thy;
- fun mk_regs elemss wits =
- fold_map (fn (id, elems) => fn wts => let
- val ts = List.concat (List.mapPartial (fn (Assumes asms) =>
- SOME (List.concat (map (map #1 o #2) asms)) | _ => NONE) elems);
- val (wts1, wts2) = chop (length ts) wts
- in ((apsnd (map fst) id, wts1), wts2) end) elemss wits |> fst;
- val regs = mk_regs elemss''' axioms |>
- map_filter (fn (("", _), _) => NONE | e => SOME e);
- in ((((elemss''', predicate, stmt'), intros), thy'), (empty, regs)) end
- | NONE => ((((elemss, ([], []), []), ([], [])), thy), (imports, []));
-
+ val predicate_name' = case predicate_name of "" => bname | _ => predicate_name;
+ val (elemss'_, defns) = change_defines_elemss thy elemss [];
+ val elemss''_ = elemss'_ @ [(("", []), defns)];
+ val (((elemss', predicate as (pred_statement, pred_axioms), stmt'), intros), thy') =
+ define_preds predicate_name' text elemss''_ thy;
+ fun mk_regs elemss wits = fold_map (fn (id, elems) => fn wts => let
+ val ts = flat (map_filter (fn (Assumes asms) =>
+ SOME (maps (map #1 o #2) asms) | _ => NONE) elems);
+ val (wts1, wts2) = chop (length ts) wts;
+ in ((apsnd (map fst) id, wts1), wts2) end) elemss wits |> fst;
+ val regs = mk_regs elemss' pred_axioms
+ |> map_filter (fn (("", _), _) => NONE | e => SOME e);
fun axiomify axioms elemss =
(axioms, elemss) |> foldl_map (fn (axs, (id, elems)) => let
val ts = flat (map_filter (fn (Assumes asms) =>
@@ -1972,28 +1938,26 @@
val (axs1, axs2) = chop (length ts) axs;
in (axs2, ((id, Assumed axs1), elems)) end)
|> snd;
- val (ctxt, (_, facts)) = activate_facts true (K I)
- (ProofContext.init pred_thy, axiomify predicate_axioms elemss');
- val view_ctxt = Assumption.add_view thy_ctxt predicate_statement ctxt;
+ val ((_, facts), ctxt) = activate_facts true (K I)
+ (axiomify pred_axioms elemss') (ProofContext.init thy');
+ val view_ctxt = Assumption.add_view thy_ctxt pred_statement ctxt;
val export = Thm.close_derivation o Goal.norm_result o
singleton (ProofContext.export view_ctxt thy_ctxt);
val facts' = facts |> map (fn (a, ths) => ((a, []), [(map export ths, [])]));
val elems' = maps #2 (filter (equal "" o #1 o #1) elemss');
val elems'' = map_filter (fn (Fixes _) => NONE | e => SOME e) elems';
- val axs' = map (Element.assume_witness pred_thy) stmt';
- val loc_ctxt = pred_thy
+ val axs' = map (Element.assume_witness thy') stmt';
+ val loc_ctxt = thy'
|> PureThy.note_thmss_qualified Thm.assumptionK bname facts' |> snd
- |> declare_locale name
- |> put_locale name
- {axiom = axs',
- imports = imports,
+ |> add_locale name {axiom = axs',
+ imports = empty,
elems = map (fn e => (e, stamp ())) elems'',
params = params_of elemss' |> map (fn (x, SOME T) => ((x, T), the (Symtab.lookup syn x))),
lparams = map #1 (params_of' body_elemss),
decls = ([], []),
regs = regs,
intros = intros,
- dests = map Element.conclude_witness predicate_axioms}
+ dests = map Element.conclude_witness pred_axioms}
|> init name;
in (name, loc_ctxt) end;
@@ -2005,9 +1969,9 @@
end;
val _ = Context.>> (Context.map_theory
- (add_locale_i (SOME "") "var" empty [Fixes [(Name.internal "x", NONE, NoSyn)]] #>
+ (add_locale_i "" "var" empty [Fixes [(Name.internal "x", NONE, NoSyn)]] #>
snd #> ProofContext.theory_of #>
- add_locale_i (SOME "") "struct" empty [Fixes [(Name.internal "S", NONE, Structure)]] #>
+ add_locale_i "" "struct" empty [Fixes [(Name.internal "S", NONE, Structure)]] #>
snd #> ProofContext.theory_of));
--- a/src/Pure/Pure.thy Fri Jul 25 12:03:31 2008 +0200
+++ b/src/Pure/Pure.thy Fri Jul 25 12:03:32 2008 +0200
@@ -26,7 +26,7 @@
subsection {* Embedded terms *}
-locale (open) meta_term_syntax =
+locale meta_term_syntax =
fixes meta_term :: "'a => prop" ("TERM _")
lemmas [intro?] = termI
@@ -34,7 +34,7 @@
subsection {* Meta-level conjunction *}
-locale (open) meta_conjunction_syntax =
+locale meta_conjunction_syntax =
fixes meta_conjunction :: "prop => prop => prop" (infixr "&&" 2)
lemma all_conjunction: