--- a/src/HOL/Hoare_Parallel/Gar_Coll.thy Tue Dec 13 14:55:42 2011 +0100
+++ b/src/HOL/Hoare_Parallel/Gar_Coll.thy Tue Dec 13 15:19:30 2011 +0100
@@ -379,19 +379,18 @@
subsubsection {* Appending garbage nodes to the free list *}
-consts Append_to_free :: "nat \<times> edges \<Rightarrow> edges"
-
-axioms
- Append_to_free0: "length (Append_to_free (i, e)) = length e"
+axiomatization Append_to_free :: "nat \<times> edges \<Rightarrow> edges"
+where
+ Append_to_free0: "length (Append_to_free (i, e)) = length e" and
Append_to_free1: "Proper_Edges (m, e)
- \<Longrightarrow> Proper_Edges (m, Append_to_free(i, e))"
+ \<Longrightarrow> Proper_Edges (m, Append_to_free(i, e))" and
Append_to_free2: "i \<notin> Reach e
\<Longrightarrow> n \<in> Reach (Append_to_free(i, e)) = ( n = i \<or> n \<in> Reach e)"
definition AppendInv :: "gar_coll_state \<Rightarrow> nat \<Rightarrow> bool" where
"AppendInv \<equiv> \<guillemotleft>\<lambda>ind. \<forall>i<length \<acute>M. ind\<le>i \<longrightarrow> i\<in>Reach \<acute>E \<longrightarrow> \<acute>M!i=Black\<guillemotright>"
-definition Append :: " gar_coll_state ann_com" where
+definition Append :: "gar_coll_state ann_com" where
"Append \<equiv>
.{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>Safe}.
\<acute>ind:=0;;
--- a/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy Tue Dec 13 14:55:42 2011 +0100
+++ b/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy Tue Dec 13 15:19:30 2011 +0100
@@ -380,13 +380,12 @@
subsubsection {* Appending garbage nodes to the free list *}
-consts Append_to_free :: "nat \<times> edges \<Rightarrow> edges"
-
-axioms
- Append_to_free0: "length (Append_to_free (i, e)) = length e"
- Append_to_free1: "Proper_Edges (m, e)
- \<Longrightarrow> Proper_Edges (m, Append_to_free(i, e))"
- Append_to_free2: "i \<notin> Reach e
+axiomatization Append_to_free :: "nat \<times> edges \<Rightarrow> edges"
+where
+ Append_to_free0: "length (Append_to_free (i, e)) = length e" and
+ Append_to_free1: "Proper_Edges (m, e)
+ \<Longrightarrow> Proper_Edges (m, Append_to_free(i, e))" and
+ Append_to_free2: "i \<notin> Reach e
\<Longrightarrow> n \<in> Reach (Append_to_free(i, e)) = ( n = i \<or> n \<in> Reach e)"
definition Mul_AppendInv :: "mul_gar_coll_state \<Rightarrow> nat \<Rightarrow> bool" where
--- a/src/HOL/Import/HOLLightList.thy Tue Dec 13 14:55:42 2011 +0100
+++ b/src/HOL/Import/HOLLightList.thy Tue Dec 13 15:19:30 2011 +0100
@@ -326,10 +326,14 @@
The definitions of TL and ZIP are different for empty lists.
*)
-axioms
+axiomatization where
DEF_HD: "hd = (SOME HD. \<forall>t h. HD (h # t) = h)"
+
+axiomatization where
DEF_LAST: "last =
(SOME LAST. \<forall>h t. LAST (h # t) = (if t = [] then h else LAST t))"
+
+axiomatization where
DEF_EL: "list_el =
(SOME EL. (\<forall>l. EL 0 l = hd l) \<and> (\<forall>n l. EL (Suc n) l = EL n (tl l)))"
--- a/src/HOL/MicroJava/J/Example.thy Tue Dec 13 14:55:42 2011 +0100
+++ b/src/HOL/MicroJava/J/Example.thy Tue Dec 13 15:19:30 2011 +0100
@@ -39,17 +39,19 @@
datatype cnam' = Base' | Ext'
datatype vnam' = vee' | x' | e'
-consts
- cnam' :: "cnam' => cname"
- vnam' :: "vnam' => vnam"
+text {*
+ @{text cnam'} and @{text vnam'} are intended to be isomorphic
+ to @{text cnam} and @{text vnam}
+*}
--- "@{text cnam'} and @{text vnam'} are intended to be isomorphic
- to @{text cnam} and @{text vnam}"
-axioms
- inj_cnam': "(cnam' x = cnam' y) = (x = y)"
- inj_vnam': "(vnam' x = vnam' y) = (x = y)"
+axiomatization cnam' :: "cnam' => cname"
+where
+ inj_cnam': "(cnam' x = cnam' y) = (x = y)" and
+ surj_cnam': "\<exists>m. n = cnam' m"
- surj_cnam': "\<exists>m. n = cnam' m"
+axiomatization vnam' :: "vnam' => vnam"
+where
+ inj_vnam': "(vnam' x = vnam' y) = (x = y)" and
surj_vnam': "\<exists>m. n = vnam' m"
declare inj_cnam' [simp] inj_vnam' [simp]
@@ -65,11 +67,11 @@
abbreviation e :: vname
where "e == VName (vnam' e')"
-axioms
- Base_not_Object: "Base \<noteq> Object"
- Ext_not_Object: "Ext \<noteq> Object"
- Base_not_Xcpt: "Base \<noteq> Xcpt z"
- Ext_not_Xcpt: "Ext \<noteq> Xcpt z"
+axiomatization where
+ Base_not_Object: "Base \<noteq> Object" and
+ Ext_not_Object: "Ext \<noteq> Object" and
+ Base_not_Xcpt: "Base \<noteq> Xcpt z" and
+ Ext_not_Xcpt: "Ext \<noteq> Xcpt z" and
e_not_This: "e \<noteq> This"
declare Base_not_Object [simp] Ext_not_Object [simp]
--- a/src/HOL/MicroJava/J/JListExample.thy Tue Dec 13 14:55:42 2011 +0100
+++ b/src/HOL/MicroJava/J/JListExample.thy Tue Dec 13 15:19:30 2011 +0100
@@ -111,7 +111,9 @@
"HOL.equal l4_nam l3_nam \<longleftrightarrow> False"
by(simp_all add: distinct_fields distinct_fields[symmetric] distinct_vars distinct_vars[symmetric] equal_vnam_def)
-axioms nat_to_loc'_inject: "nat_to_loc' l = nat_to_loc' l' \<longleftrightarrow> l = l'"
+axiomatization where
+ nat_to_loc'_inject: "nat_to_loc' l = nat_to_loc' l' \<longleftrightarrow> l = l'"
+
lemma equal_loc'_code [code]:
"HOL.equal (nat_to_loc' l) (nat_to_loc' l') \<longleftrightarrow> l = l'"
by(simp add: equal_loc'_def nat_to_loc'_inject)
--- a/src/HOL/MicroJava/JVM/JVMListExample.thy Tue Dec 13 14:55:42 2011 +0100
+++ b/src/HOL/MicroJava/JVM/JVMListExample.thy Tue Dec 13 15:19:30 2011 +0100
@@ -13,30 +13,31 @@
anonymous, we describe distinctness of names in the example by axioms:
*}
axiomatization list_nam test_nam :: cnam
-where distinct_classes: "list_nam \<noteq> test_nam"
+ where distinct_classes: "list_nam \<noteq> test_nam"
axiomatization append_name makelist_name :: mname
-where distinct_methods: "append_name \<noteq> makelist_name"
+ where distinct_methods: "append_name \<noteq> makelist_name"
axiomatization val_nam next_nam :: vnam
-where distinct_fields: "val_nam \<noteq> next_nam"
+ where distinct_fields: "val_nam \<noteq> next_nam"
-axioms nat_to_loc'_inject: "nat_to_loc' l = nat_to_loc' l' \<longleftrightarrow> l = l'"
+axiomatization
+ where nat_to_loc'_inject: "nat_to_loc' l = nat_to_loc' l' \<longleftrightarrow> l = l'"
-definition list_name :: cname where
- "list_name == Cname list_nam"
+definition list_name :: cname
+ where "list_name = Cname list_nam"
-definition test_name :: cname where
- "test_name == Cname test_nam"
+definition test_name :: cname
+ where "test_name = Cname test_nam"
-definition val_name :: vname where
- "val_name == VName val_nam"
+definition val_name :: vname
+ where "val_name = VName val_nam"
-definition next_name :: vname where
- "next_name == VName next_nam"
+definition next_name :: vname
+ where "next_name = VName next_nam"
definition append_ins :: bytecode where
- "append_ins ==
+ "append_ins =
[Load 0,
Getfield next_name list_name,
Dup,
@@ -53,14 +54,14 @@
Return]"
definition list_class :: "jvm_method class" where
- "list_class ==
+ "list_class =
(Object,
[(val_name, PrimT Integer), (next_name, Class list_name)],
[((append_name, [Class list_name]), PrimT Void,
(3, 0, append_ins,[(1,2,8,Xcpt NullPointer)]))])"
definition make_list_ins :: bytecode where
- "make_list_ins ==
+ "make_list_ins =
[New list_name,
Dup,
Store 0,
@@ -86,12 +87,12 @@
Return]"
definition test_class :: "jvm_method class" where
- "test_class ==
+ "test_class =
(Object, [],
[((makelist_name, []), PrimT Void, (3, 2, make_list_ins,[]))])"
definition E :: jvm_prog where
- "E == SystemClasses @ [(list_name, list_class), (test_name, test_class)]"
+ "E = SystemClasses @ [(list_name, list_class), (test_name, test_class)]"
code_datatype list_nam test_nam
lemma equal_cnam_code [code]:
--- a/src/HOL/NanoJava/AxSem.thy Tue Dec 13 14:55:42 2011 +0100
+++ b/src/HOL/NanoJava/AxSem.thy Tue Dec 13 15:19:30 2011 +0100
@@ -99,17 +99,18 @@
subsection "Fully polymorphic variants, required for Example only"
-axioms
-
+axiomatization where
Conseq:"[| \<forall>Z. A \<turnstile> {P' Z} c {Q' Z};
\<forall>s t. (\<forall>Z. P' Z s --> Q' Z t) --> (P s --> Q t) |] ==>
A \<turnstile> {P} c {Q }"
- eConseq:"[| \<forall>Z. A \<turnstile>\<^sub>e {P' Z} e {Q' Z};
+axiomatization where
+ eConseq:"[| \<forall>Z. A \<turnstile>\<^sub>e {P' Z} e {Q' Z};
\<forall>s v t. (\<forall>Z. P' Z s --> Q' Z v t) --> (P s --> Q v t) |] ==>
A \<turnstile>\<^sub>e {P} e {Q }"
- Impl: "\<forall>Z. A\<union> (\<Union>Z. (\<lambda>Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms) |\<turnstile>
+axiomatization where
+ Impl: "\<forall>Z. A\<union> (\<Union>Z. (\<lambda>Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms) |\<turnstile>
(\<lambda>Cm. (P Z Cm, body Cm, Q Z Cm))`Ms ==>
A |\<turnstile> (\<lambda>Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms"
--- a/src/HOL/SET_Protocol/Public_SET.thy Tue Dec 13 14:55:42 2011 +0100
+++ b/src/HOL/SET_Protocol/Public_SET.thy Tue Dec 13 15:19:30 2011 +0100
@@ -46,7 +46,7 @@
done
(*>*)
-axioms
+axiomatization where
(*No private key equals any public key (essential to ensure that private
keys are private!) *)
privateKey_neq_publicKey [iff]:
--- a/src/HOL/UNITY/Comp/AllocBase.thy Tue Dec 13 14:55:42 2011 +0100
+++ b/src/HOL/UNITY/Comp/AllocBase.thy Tue Dec 13 15:19:30 2011 +0100
@@ -7,12 +7,10 @@
theory AllocBase imports "../UNITY_Main" begin
-consts
- NbT :: nat (*Number of tokens in system*)
- Nclients :: nat (*Number of clients*)
+consts Nclients :: nat (*Number of clients*)
-axioms
- NbT_pos: "0 < NbT"
+axiomatization NbT :: nat (*Number of tokens in system*)
+ where NbT_pos: "0 < NbT"
(*This function merely sums the elements of a list*)
primrec tokens :: "nat list => nat" where
--- a/src/HOL/UNITY/Comp/PriorityAux.thy Tue Dec 13 14:55:42 2011 +0100
+++ b/src/HOL/UNITY/Comp/PriorityAux.thy Tue Dec 13 15:19:30 2011 +0100
@@ -45,7 +45,7 @@
--{* Our alternative definition *}
"derive i r q == A i r = {} & (q = reverse i r)"
-axioms
+axiomatization where
finite_vertex_univ: "finite (UNIV :: vertex set)"
--{* we assume that the universe of vertices is finite *}
--- a/src/HOL/UNITY/Simple/Reachability.thy Tue Dec 13 14:55:42 2011 +0100
+++ b/src/HOL/UNITY/Simple/Reachability.thy Tue Dec 13 15:19:30 2011 +0100
@@ -44,27 +44,27 @@
"final == (\<Inter>v\<in>V. reachable v <==> {s. (root, v) \<in> REACHABLE}) \<inter>
(INTER E (nmsg_eq 0))"
-axioms
+axiomatization
+where
+ Graph1: "root \<in> V" and
- Graph1: "root \<in> V"
-
- Graph2: "(v,w) \<in> E ==> (v \<in> V) & (w \<in> V)"
+ Graph2: "(v,w) \<in> E ==> (v \<in> V) & (w \<in> V)" and
- MA1: "F \<in> Always (reachable root)"
+ MA1: "F \<in> Always (reachable root)" and
- MA2: "v \<in> V ==> F \<in> Always (- reachable v \<union> {s. ((root,v) \<in> REACHABLE)})"
+ MA2: "v \<in> V ==> F \<in> Always (- reachable v \<union> {s. ((root,v) \<in> REACHABLE)})" and
- MA3: "[|v \<in> V;w \<in> V|] ==> F \<in> Always (-(nmsg_gt 0 (v,w)) \<union> (reachable v))"
+ MA3: "[|v \<in> V;w \<in> V|] ==> F \<in> Always (-(nmsg_gt 0 (v,w)) \<union> (reachable v))" and
MA4: "(v,w) \<in> E ==>
- F \<in> Always (-(reachable v) \<union> (nmsg_gt 0 (v,w)) \<union> (reachable w))"
+ F \<in> Always (-(reachable v) \<union> (nmsg_gt 0 (v,w)) \<union> (reachable w))" and
MA5: "[|v \<in> V; w \<in> V|]
- ==> F \<in> Always (nmsg_gte 0 (v,w) \<inter> nmsg_lte (Suc 0) (v,w))"
+ ==> F \<in> Always (nmsg_gte 0 (v,w) \<inter> nmsg_lte (Suc 0) (v,w))" and
- MA6: "[|v \<in> V|] ==> F \<in> Stable (reachable v)"
+ MA6: "[|v \<in> V|] ==> F \<in> Stable (reachable v)" and
- MA6b: "[|v \<in> V;w \<in> W|] ==> F \<in> Stable (reachable v \<inter> nmsg_lte k (v,w))"
+ MA6b: "[|v \<in> V;w \<in> W|] ==> F \<in> Stable (reachable v \<inter> nmsg_lte k (v,w))" and
MA7: "[|v \<in> V;w \<in> V|] ==> F \<in> UNIV LeadsTo nmsg_eq 0 (v,w)"
--- a/src/HOL/ZF/HOLZF.thy Tue Dec 13 14:55:42 2011 +0100
+++ b/src/HOL/ZF/HOLZF.thy Tue Dec 13 15:19:30 2011 +0100
@@ -34,13 +34,13 @@
definition subset :: "ZF \<Rightarrow> ZF \<Rightarrow> bool" where
"subset A B == ! x. Elem x A \<longrightarrow> Elem x B"
-axioms
- Empty: "Not (Elem x Empty)"
- Ext: "(x = y) = (! z. Elem z x = Elem z y)"
- Sum: "Elem z (Sum x) = (? y. Elem z y & Elem y x)"
- Power: "Elem y (Power x) = (subset y x)"
- Repl: "Elem b (Repl A f) = (? a. Elem a A & b = f a)"
- Regularity: "A \<noteq> Empty \<longrightarrow> (? x. Elem x A & (! y. Elem y x \<longrightarrow> Not (Elem y A)))"
+axiomatization where
+ Empty: "Not (Elem x Empty)" and
+ Ext: "(x = y) = (! z. Elem z x = Elem z y)" and
+ Sum: "Elem z (Sum x) = (? y. Elem z y & Elem y x)" and
+ Power: "Elem y (Power x) = (subset y x)" and
+ Repl: "Elem b (Repl A f) = (? a. Elem a A & b = f a)" and
+ Regularity: "A \<noteq> Empty \<longrightarrow> (? x. Elem x A & (! y. Elem y x \<longrightarrow> Not (Elem y A)))" and
Infinity: "Elem Empty Inf & (! x. Elem x Inf \<longrightarrow> Elem (SucNat x) Inf)"
definition Sep :: "ZF \<Rightarrow> (ZF \<Rightarrow> bool) \<Rightarrow> ZF" where