1.1 --- a/src/HOL/Hoare_Parallel/Gar_Coll.thy	Tue Dec 13 14:04:20 2011 +0100
     1.2 +++ b/src/HOL/Hoare_Parallel/Gar_Coll.thy	Tue Dec 13 15:18:52 2011 +0100
     1.3 @@ -379,19 +379,18 @@
     1.4  
     1.5  subsubsection {* Appending garbage nodes to the free list *}
     1.6  
     1.7 -consts Append_to_free :: "nat \<times> edges \<Rightarrow> edges"
     1.8 -
     1.9 -axioms
    1.10 -  Append_to_free0: "length (Append_to_free (i, e)) = length e"
    1.11 +axiomatization Append_to_free :: "nat \<times> edges \<Rightarrow> edges"
    1.12 +where
    1.13 +  Append_to_free0: "length (Append_to_free (i, e)) = length e" and
    1.14    Append_to_free1: "Proper_Edges (m, e) 
    1.15 -                   \<Longrightarrow> Proper_Edges (m, Append_to_free(i, e))"
    1.16 +                   \<Longrightarrow> Proper_Edges (m, Append_to_free(i, e))" and
    1.17    Append_to_free2: "i \<notin> Reach e 
    1.18       \<Longrightarrow> n \<in> Reach (Append_to_free(i, e)) = ( n = i \<or> n \<in> Reach e)"
    1.19  
    1.20  definition AppendInv :: "gar_coll_state \<Rightarrow> nat \<Rightarrow> bool" where
    1.21    "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>"
    1.22  
    1.23 -definition Append :: " gar_coll_state ann_com" where
    1.24 +definition Append :: "gar_coll_state ann_com" where
    1.25     "Append \<equiv>
    1.26    .{\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>Safe}.
    1.27    \<acute>ind:=0;;

     2.1 --- a/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy	Tue Dec 13 14:04:20 2011 +0100
     2.2 +++ b/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy	Tue Dec 13 15:18:52 2011 +0100
     2.3 @@ -380,13 +380,12 @@
     2.4  
     2.5  subsubsection {* Appending garbage nodes to the free list *}
     2.6  
     2.7 -consts  Append_to_free :: "nat \<times> edges \<Rightarrow> edges"
     2.8 -
     2.9 -axioms
    2.10 -  Append_to_free0: "length (Append_to_free (i, e)) = length e"
    2.11 -  Append_to_free1: "Proper_Edges (m, e) 
    2.12 -                    \<Longrightarrow> Proper_Edges (m, Append_to_free(i, e))"
    2.13 -  Append_to_free2: "i \<notin> Reach e 
    2.14 +axiomatization Append_to_free :: "nat \<times> edges \<Rightarrow> edges"
    2.15 +where
    2.16 +  Append_to_free0: "length (Append_to_free (i, e)) = length e" and
    2.17 +  Append_to_free1: "Proper_Edges (m, e)
    2.18 +                    \<Longrightarrow> Proper_Edges (m, Append_to_free(i, e))" and
    2.19 +  Append_to_free2: "i \<notin> Reach e
    2.20             \<Longrightarrow> n \<in> Reach (Append_to_free(i, e)) = ( n = i \<or> n \<in> Reach e)"
    2.21  
    2.22  definition Mul_AppendInv :: "mul_gar_coll_state \<Rightarrow> nat \<Rightarrow> bool" where

     3.1 --- a/src/HOL/Import/HOLLightList.thy	Tue Dec 13 14:04:20 2011 +0100
     3.2 +++ b/src/HOL/Import/HOLLightList.thy	Tue Dec 13 15:18:52 2011 +0100
     3.3 @@ -326,10 +326,14 @@
     3.4  
     3.5     The definitions of TL and ZIP are different for empty lists.
     3.6   *)
     3.7 -axioms
     3.8 +axiomatization where
     3.9    DEF_HD: "hd = (SOME HD. \<forall>t h. HD (h # t) = h)"
    3.10 +
    3.11 +axiomatization where
    3.12    DEF_LAST: "last =
    3.13      (SOME LAST. \<forall>h t. LAST (h # t) = (if t = [] then h else LAST t))"
    3.14 +
    3.15 +axiomatization where
    3.16    DEF_EL: "list_el =
    3.17      (SOME EL. (\<forall>l. EL 0 l = hd l) \<and> (\<forall>n l. EL (Suc n) l = EL n (tl l)))"
    3.18  

     4.1 --- a/src/HOL/MicroJava/J/Example.thy	Tue Dec 13 14:04:20 2011 +0100
     4.2 +++ b/src/HOL/MicroJava/J/Example.thy	Tue Dec 13 15:18:52 2011 +0100
     4.3 @@ -39,17 +39,19 @@
     4.4  datatype cnam' = Base' | Ext'
     4.5  datatype vnam' = vee' | x' | e'
     4.6  
     4.7 -consts
     4.8 -  cnam' :: "cnam' => cname"
     4.9 -  vnam' :: "vnam' => vnam"
    4.10 +text {*
    4.11 +  @{text cnam'} and @{text vnam'} are intended to be isomorphic 
    4.12 +  to @{text cnam} and @{text vnam}
    4.13 +*}
    4.14  
    4.15 --- "@{text cnam'} and @{text vnam'} are intended to be isomorphic 
    4.16 -    to @{text cnam} and @{text vnam}"
    4.17 -axioms 
    4.18 -  inj_cnam':  "(cnam' x = cnam' y) = (x = y)"
    4.19 -  inj_vnam':  "(vnam' x = vnam' y) = (x = y)"
    4.20 +axiomatization cnam' :: "cnam' => cname"
    4.21 +where
    4.22 +  inj_cnam':  "(cnam' x = cnam' y) = (x = y)" and
    4.23 +  surj_cnam': "\<exists>m. n = cnam' m"
    4.24  
    4.25 -  surj_cnam': "\<exists>m. n = cnam' m"
    4.26 +axiomatization vnam' :: "vnam' => vnam"
    4.27 +where
    4.28 +  inj_vnam':  "(vnam' x = vnam' y) = (x = y)" and
    4.29    surj_vnam': "\<exists>m. n = vnam' m"
    4.30  
    4.31  declare inj_cnam' [simp] inj_vnam' [simp]
    4.32 @@ -65,11 +67,11 @@
    4.33  abbreviation e :: vname
    4.34    where "e == VName (vnam' e')"
    4.35  
    4.36 -axioms
    4.37 -  Base_not_Object: "Base \<noteq> Object"
    4.38 -  Ext_not_Object:  "Ext  \<noteq> Object"
    4.39 -  Base_not_Xcpt:   "Base \<noteq> Xcpt z"
    4.40 -  Ext_not_Xcpt:    "Ext  \<noteq> Xcpt z"
    4.41 +axiomatization where
    4.42 +  Base_not_Object: "Base \<noteq> Object" and
    4.43 +  Ext_not_Object:  "Ext  \<noteq> Object" and
    4.44 +  Base_not_Xcpt:   "Base \<noteq> Xcpt z" and
    4.45 +  Ext_not_Xcpt:    "Ext  \<noteq> Xcpt z" and
    4.46    e_not_This:      "e \<noteq> This"  
    4.47  
    4.48  declare Base_not_Object [simp] Ext_not_Object [simp]

     5.1 --- a/src/HOL/MicroJava/J/JListExample.thy	Tue Dec 13 14:04:20 2011 +0100
     5.2 +++ b/src/HOL/MicroJava/J/JListExample.thy	Tue Dec 13 15:18:52 2011 +0100
     5.3 @@ -111,7 +111,9 @@
     5.4    "HOL.equal l4_nam l3_nam \<longleftrightarrow> False"
     5.5    by(simp_all add: distinct_fields distinct_fields[symmetric] distinct_vars distinct_vars[symmetric] equal_vnam_def)
     5.6  
     5.7 -axioms nat_to_loc'_inject: "nat_to_loc' l = nat_to_loc' l' \<longleftrightarrow> l = l'"
     5.8 +axiomatization where
     5.9 +  nat_to_loc'_inject: "nat_to_loc' l = nat_to_loc' l' \<longleftrightarrow> l = l'"
    5.10 +
    5.11  lemma equal_loc'_code [code]:
    5.12    "HOL.equal (nat_to_loc' l) (nat_to_loc' l') \<longleftrightarrow> l = l'"
    5.13    by(simp add: equal_loc'_def nat_to_loc'_inject)

     6.1 --- a/src/HOL/MicroJava/JVM/JVMListExample.thy	Tue Dec 13 14:04:20 2011 +0100
     6.2 +++ b/src/HOL/MicroJava/JVM/JVMListExample.thy	Tue Dec 13 15:18:52 2011 +0100
     6.3 @@ -13,30 +13,31 @@
     6.4    anonymous, we describe distinctness of names in the example by axioms:
     6.5  *}
     6.6  axiomatization list_nam test_nam :: cnam
     6.7 -where distinct_classes: "list_nam \<noteq> test_nam"
     6.8 +  where distinct_classes: "list_nam \<noteq> test_nam"
     6.9  
    6.10  axiomatization append_name makelist_name :: mname
    6.11 -where distinct_methods: "append_name \<noteq> makelist_name"
    6.12 +  where distinct_methods: "append_name \<noteq> makelist_name"
    6.13  
    6.14  axiomatization val_nam next_nam :: vnam
    6.15 -where distinct_fields: "val_nam \<noteq> next_nam"
    6.16 +  where distinct_fields: "val_nam \<noteq> next_nam"
    6.17  
    6.18 -axioms nat_to_loc'_inject: "nat_to_loc' l = nat_to_loc' l' \<longleftrightarrow> l = l'"
    6.19 +axiomatization
    6.20 +  where nat_to_loc'_inject: "nat_to_loc' l = nat_to_loc' l' \<longleftrightarrow> l = l'"
    6.21  
    6.22 -definition list_name :: cname where
    6.23 -  "list_name == Cname list_nam"
    6.24 +definition list_name :: cname
    6.25 +  where "list_name = Cname list_nam"
    6.26    
    6.27 -definition test_name :: cname where
    6.28 -  "test_name == Cname test_nam"
    6.29 +definition test_name :: cname
    6.30 +  where "test_name = Cname test_nam"
    6.31  
    6.32 -definition val_name :: vname where
    6.33 -  "val_name == VName val_nam"
    6.34 +definition val_name :: vname
    6.35 +  where "val_name = VName val_nam"
    6.36  
    6.37 -definition next_name :: vname where
    6.38 -  "next_name == VName next_nam"
    6.39 +definition next_name :: vname
    6.40 +  where "next_name = VName next_nam"
    6.41  
    6.42  definition append_ins :: bytecode where
    6.43 -  "append_ins == 
    6.44 +  "append_ins =
    6.45         [Load 0,
    6.46          Getfield next_name list_name,
    6.47          Dup,
    6.48 @@ -53,14 +54,14 @@
    6.49          Return]"
    6.50  
    6.51  definition list_class :: "jvm_method class" where
    6.52 -  "list_class ==
    6.53 +  "list_class =
    6.54      (Object,
    6.55       [(val_name, PrimT Integer), (next_name, Class list_name)],
    6.56       [((append_name, [Class list_name]), PrimT Void,
    6.57          (3, 0, append_ins,[(1,2,8,Xcpt NullPointer)]))])"
    6.58  
    6.59  definition make_list_ins :: bytecode where
    6.60 -  "make_list_ins ==
    6.61 +  "make_list_ins =
    6.62         [New list_name,
    6.63          Dup,
    6.64          Store 0,
    6.65 @@ -86,12 +87,12 @@
    6.66          Return]"
    6.67  
    6.68  definition test_class :: "jvm_method class" where
    6.69 -  "test_class ==
    6.70 +  "test_class =
    6.71      (Object, [],
    6.72       [((makelist_name, []), PrimT Void, (3, 2, make_list_ins,[]))])"
    6.73  
    6.74  definition E :: jvm_prog where
    6.75 -  "E == SystemClasses @ [(list_name, list_class), (test_name, test_class)]"
    6.76 +  "E = SystemClasses @ [(list_name, list_class), (test_name, test_class)]"
    6.77  
    6.78  code_datatype list_nam test_nam
    6.79  lemma equal_cnam_code [code]:

     7.1 --- a/src/HOL/NanoJava/AxSem.thy	Tue Dec 13 14:04:20 2011 +0100
     7.2 +++ b/src/HOL/NanoJava/AxSem.thy	Tue Dec 13 15:18:52 2011 +0100
     7.3 @@ -99,17 +99,18 @@
     7.4  
     7.5  subsection "Fully polymorphic variants, required for Example only"
     7.6  
     7.7 -axioms
     7.8 -
     7.9 +axiomatization where
    7.10    Conseq:"[| \<forall>Z. A \<turnstile> {P' Z} c {Q' Z};
    7.11               \<forall>s t. (\<forall>Z. P' Z s --> Q' Z t) --> (P s --> Q t) |] ==>
    7.12                   A \<turnstile> {P} c {Q }"
    7.13  
    7.14 - eConseq:"[| \<forall>Z. A \<turnstile>\<^sub>e {P' Z} e {Q' Z};
    7.15 +axiomatization where
    7.16 +  eConseq:"[| \<forall>Z. A \<turnstile>\<^sub>e {P' Z} e {Q' Z};
    7.17               \<forall>s v t. (\<forall>Z. P' Z s --> Q' Z v t) --> (P s --> Q v t) |] ==>
    7.18                   A \<turnstile>\<^sub>e {P} e {Q }"
    7.19  
    7.20 - Impl: "\<forall>Z. A\<union> (\<Union>Z. (\<lambda>Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms) |\<turnstile> 
    7.21 +axiomatization where
    7.22 +  Impl: "\<forall>Z. A\<union> (\<Union>Z. (\<lambda>Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms) |\<turnstile> 
    7.23                            (\<lambda>Cm. (P Z Cm, body Cm, Q Z Cm))`Ms ==>
    7.24                      A |\<turnstile> (\<lambda>Cm. (P Z Cm, Impl Cm, Q Z Cm))`Ms"
    7.25  

     8.1 --- a/src/HOL/SET_Protocol/Public_SET.thy	Tue Dec 13 14:04:20 2011 +0100
     8.2 +++ b/src/HOL/SET_Protocol/Public_SET.thy	Tue Dec 13 15:18:52 2011 +0100
     8.3 @@ -46,7 +46,7 @@
     8.4     done                       
     8.5  (*>*)
     8.6  
     8.7 -axioms
     8.8 +axiomatization where
     8.9    (*No private key equals any public key (essential to ensure that private
    8.10      keys are private!) *)
    8.11    privateKey_neq_publicKey [iff]:

     9.1 --- a/src/HOL/UNITY/Comp/AllocBase.thy	Tue Dec 13 14:04:20 2011 +0100
     9.2 +++ b/src/HOL/UNITY/Comp/AllocBase.thy	Tue Dec 13 15:18:52 2011 +0100
     9.3 @@ -7,12 +7,10 @@
     9.4  
     9.5  theory AllocBase imports "../UNITY_Main" begin
     9.6  
     9.7 -consts
     9.8 -  NbT      :: nat       (*Number of tokens in system*)
     9.9 -  Nclients :: nat       (*Number of clients*)
    9.10 +consts Nclients :: nat  (*Number of clients*)
    9.11  
    9.12 -axioms
    9.13 -  NbT_pos:  "0 < NbT"
    9.14 +axiomatization NbT :: nat  (*Number of tokens in system*)
    9.15 +  where NbT_pos: "0 < NbT"
    9.16  
    9.17  (*This function merely sums the elements of a list*)
    9.18  primrec tokens :: "nat list => nat" where

    10.1 --- a/src/HOL/UNITY/Comp/PriorityAux.thy	Tue Dec 13 14:04:20 2011 +0100
    10.2 +++ b/src/HOL/UNITY/Comp/PriorityAux.thy	Tue Dec 13 15:18:52 2011 +0100
    10.3 @@ -45,7 +45,7 @@
    10.4      --{* Our alternative definition *}
    10.5    "derive i r q == A i r = {} & (q = reverse i r)"
    10.6  
    10.7 -axioms
    10.8 +axiomatization where
    10.9    finite_vertex_univ:  "finite (UNIV :: vertex set)"
   10.10      --{* we assume that the universe of vertices is finite  *}
   10.11  

    11.1 --- a/src/HOL/UNITY/Simple/Reachability.thy	Tue Dec 13 14:04:20 2011 +0100
    11.2 +++ b/src/HOL/UNITY/Simple/Reachability.thy	Tue Dec 13 15:18:52 2011 +0100
    11.3 @@ -44,27 +44,27 @@
    11.4    "final == (\<Inter>v\<in>V. reachable v <==> {s. (root, v) \<in> REACHABLE}) \<inter> 
    11.5              (INTER E (nmsg_eq 0))"
    11.6  
    11.7 -axioms
    11.8 +axiomatization
    11.9 +where
   11.10 +    Graph1: "root \<in> V" and
   11.11  
   11.12 -    Graph1: "root \<in> V"
   11.13 +    Graph2: "(v,w) \<in> E ==> (v \<in> V) & (w \<in> V)" and
   11.14  
   11.15 -    Graph2: "(v,w) \<in> E ==> (v \<in> V) & (w \<in> V)"
   11.16 +    MA1:  "F \<in> Always (reachable root)" and
   11.17  
   11.18 -    MA1:  "F \<in> Always (reachable root)"
   11.19 +    MA2:  "v \<in> V ==> F \<in> Always (- reachable v \<union> {s. ((root,v) \<in> REACHABLE)})" and
   11.20  
   11.21 -    MA2:  "v \<in> V ==> F \<in> Always (- reachable v \<union> {s. ((root,v) \<in> REACHABLE)})"
   11.22 -
   11.23 -    MA3:  "[|v \<in> V;w \<in> V|] ==> F \<in> Always (-(nmsg_gt 0 (v,w)) \<union> (reachable v))"
   11.24 +    MA3:  "[|v \<in> V;w \<in> V|] ==> F \<in> Always (-(nmsg_gt 0 (v,w)) \<union> (reachable v))" and
   11.25  
   11.26      MA4:  "(v,w) \<in> E ==> 
   11.27 -           F \<in> Always (-(reachable v) \<union> (nmsg_gt 0 (v,w)) \<union> (reachable w))"
   11.28 +           F \<in> Always (-(reachable v) \<union> (nmsg_gt 0 (v,w)) \<union> (reachable w))" and
   11.29  
   11.30      MA5:  "[|v \<in> V; w \<in> V|] 
   11.31 -           ==> F \<in> Always (nmsg_gte 0 (v,w) \<inter> nmsg_lte (Suc 0) (v,w))"
   11.32 +           ==> F \<in> Always (nmsg_gte 0 (v,w) \<inter> nmsg_lte (Suc 0) (v,w))" and
   11.33  
   11.34 -    MA6:  "[|v \<in> V|] ==> F \<in> Stable (reachable v)"
   11.35 +    MA6:  "[|v \<in> V|] ==> F \<in> Stable (reachable v)" and
   11.36  
   11.37 -    MA6b: "[|v \<in> V;w \<in> W|] ==> F \<in> Stable (reachable v \<inter> nmsg_lte k (v,w))"
   11.38 +    MA6b: "[|v \<in> V;w \<in> W|] ==> F \<in> Stable (reachable v \<inter> nmsg_lte k (v,w))" and
   11.39  
   11.40      MA7:  "[|v \<in> V;w \<in> V|] ==> F \<in> UNIV LeadsTo nmsg_eq 0 (v,w)"
   11.41  

    12.1 --- a/src/HOL/ZF/HOLZF.thy	Tue Dec 13 14:04:20 2011 +0100
    12.2 +++ b/src/HOL/ZF/HOLZF.thy	Tue Dec 13 15:18:52 2011 +0100
    12.3 @@ -34,13 +34,13 @@
    12.4  definition subset :: "ZF \<Rightarrow> ZF \<Rightarrow> bool" where
    12.5    "subset A B == ! x. Elem x A \<longrightarrow> Elem x B"
    12.6  
    12.7 -axioms
    12.8 -  Empty: "Not (Elem x Empty)"
    12.9 -  Ext: "(x = y) = (! z. Elem z x = Elem z y)"
   12.10 -  Sum: "Elem z (Sum x) = (? y. Elem z y & Elem y x)"
   12.11 -  Power: "Elem y (Power x) = (subset y x)"
   12.12 -  Repl: "Elem b (Repl A f) = (? a. Elem a A & b = f a)"
   12.13 -  Regularity: "A \<noteq> Empty \<longrightarrow> (? x. Elem x A & (! y. Elem y x \<longrightarrow> Not (Elem y A)))"
   12.14 +axiomatization where
   12.15 +  Empty: "Not (Elem x Empty)" and
   12.16 +  Ext: "(x = y) = (! z. Elem z x = Elem z y)" and
   12.17 +  Sum: "Elem z (Sum x) = (? y. Elem z y & Elem y x)" and
   12.18 +  Power: "Elem y (Power x) = (subset y x)" and
   12.19 +  Repl: "Elem b (Repl A f) = (? a. Elem a A & b = f a)" and
   12.20 +  Regularity: "A \<noteq> Empty \<longrightarrow> (? x. Elem x A & (! y. Elem y x \<longrightarrow> Not (Elem y A)))" and
   12.21    Infinity: "Elem Empty Inf & (! x. Elem x Inf \<longrightarrow> Elem (SucNat x) Inf)"
   12.22  
   12.23  definition Sep :: "ZF \<Rightarrow> (ZF \<Rightarrow> bool) \<Rightarrow> ZF" where