# HG changeset patch
# User wenzelm
# Date 1323785932 -3600
# Node ID 66c68453455c3181d2117420f08f30f88930cb09
# Parent  67110d6c66dee6279c7328824015ee7d661dd797
modernized specifications;

diff -r 67110d6c66de -r 66c68453455c src/HOL/Hoare_Parallel/Gar_Coll.thy
--- a/src/HOL/Hoare_Parallel/Gar_Coll.thy	Tue Dec 13 14:04:20 2011 +0100
+++ b/src/HOL/Hoare_Parallel/Gar_Coll.thy	Tue Dec 13 15:18:52 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;;
diff -r 67110d6c66de -r 66c68453455c src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy
--- a/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy	Tue Dec 13 14:04:20 2011 +0100
+++ b/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy	Tue Dec 13 15:18:52 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
diff -r 67110d6c66de -r 66c68453455c src/HOL/Import/HOLLightList.thy
--- a/src/HOL/Import/HOLLightList.thy	Tue Dec 13 14:04:20 2011 +0100
+++ b/src/HOL/Import/HOLLightList.thy	Tue Dec 13 15:18:52 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)))"
 
diff -r 67110d6c66de -r 66c68453455c src/HOL/MicroJava/J/Example.thy
--- a/src/HOL/MicroJava/J/Example.thy	Tue Dec 13 14:04:20 2011 +0100
+++ b/src/HOL/MicroJava/J/Example.thy	Tue Dec 13 15:18:52 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]
diff -r 67110d6c66de -r 66c68453455c src/HOL/MicroJava/J/JListExample.thy
--- a/src/HOL/MicroJava/J/JListExample.thy	Tue Dec 13 14:04:20 2011 +0100
+++ b/src/HOL/MicroJava/J/JListExample.thy	Tue Dec 13 15:18:52 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)
diff -r 67110d6c66de -r 66c68453455c src/HOL/MicroJava/JVM/JVMListExample.thy
--- a/src/HOL/MicroJava/JVM/JVMListExample.thy	Tue Dec 13 14:04:20 2011 +0100
+++ b/src/HOL/MicroJava/JVM/JVMListExample.thy	Tue Dec 13 15:18:52 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]:
diff -r 67110d6c66de -r 66c68453455c src/HOL/NanoJava/AxSem.thy
--- a/src/HOL/NanoJava/AxSem.thy	Tue Dec 13 14:04:20 2011 +0100
+++ b/src/HOL/NanoJava/AxSem.thy	Tue Dec 13 15:18:52 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"
 
diff -r 67110d6c66de -r 66c68453455c src/HOL/SET_Protocol/Public_SET.thy
--- a/src/HOL/SET_Protocol/Public_SET.thy	Tue Dec 13 14:04:20 2011 +0100
+++ b/src/HOL/SET_Protocol/Public_SET.thy	Tue Dec 13 15:18:52 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]:
diff -r 67110d6c66de -r 66c68453455c src/HOL/UNITY/Comp/AllocBase.thy
--- a/src/HOL/UNITY/Comp/AllocBase.thy	Tue Dec 13 14:04:20 2011 +0100
+++ b/src/HOL/UNITY/Comp/AllocBase.thy	Tue Dec 13 15:18:52 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
diff -r 67110d6c66de -r 66c68453455c src/HOL/UNITY/Comp/PriorityAux.thy
--- a/src/HOL/UNITY/Comp/PriorityAux.thy	Tue Dec 13 14:04:20 2011 +0100
+++ b/src/HOL/UNITY/Comp/PriorityAux.thy	Tue Dec 13 15:18:52 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  *}
 
diff -r 67110d6c66de -r 66c68453455c src/HOL/UNITY/Simple/Reachability.thy
--- a/src/HOL/UNITY/Simple/Reachability.thy	Tue Dec 13 14:04:20 2011 +0100
+++ b/src/HOL/UNITY/Simple/Reachability.thy	Tue Dec 13 15:18:52 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)"
 
diff -r 67110d6c66de -r 66c68453455c src/HOL/ZF/HOLZF.thy
--- a/src/HOL/ZF/HOLZF.thy	Tue Dec 13 14:04:20 2011 +0100
+++ b/src/HOL/ZF/HOLZF.thy	Tue Dec 13 15:18:52 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