modernized specifications;
authorwenzelm
Fri Feb 18 17:03:30 2011 +0100 (2011-02-18)
changeset 41779a68f503805ed
parent 41778 5f79a9e42507
child 41780 7eb9eac392b6
modernized specifications;
src/FOL/FOL.thy
src/FOL/IFOL.thy
src/FOL/ex/Locale_Test/Locale_Test1.thy
src/FOL/ex/Nat.thy
src/FOL/ex/Prolog.thy
src/FOLP/FOLP.thy
src/ZF/Coind/Language.thy
src/ZF/Coind/Static.thy
src/ZF/UNITY/AllocBase.thy
src/ZF/UNITY/AllocImpl.thy
src/ZF/UNITY/ClientImpl.thy
src/ZF/UNITY/Mutex.thy
src/ZF/ZF.thy
src/ZF/ex/LList.thy
     1.1 --- a/src/FOL/FOL.thy	Fri Feb 18 16:36:42 2011 +0100
     1.2 +++ b/src/FOL/FOL.thy	Fri Feb 18 17:03:30 2011 +0100
     1.3 @@ -18,7 +18,7 @@
     1.4  
     1.5  subsection {* The classical axiom *}
     1.6  
     1.7 -axioms
     1.8 +axiomatization where
     1.9    classical: "(~P ==> P) ==> P"
    1.10  
    1.11  
     2.1 --- a/src/FOL/IFOL.thy	Fri Feb 18 16:36:42 2011 +0100
     2.2 +++ b/src/FOL/IFOL.thy	Fri Feb 18 17:03:30 2011 +0100
     2.3 @@ -88,42 +88,39 @@
     2.4  finalconsts
     2.5    False All Ex eq conj disj imp
     2.6  
     2.7 -axioms
     2.8 -
     2.9 +axiomatization where
    2.10    (* Equality *)
    2.11 -
    2.12 -  refl:         "a=a"
    2.13 +  refl:         "a=a" and
    2.14    subst:        "a=b \<Longrightarrow> P(a) \<Longrightarrow> P(b)"
    2.15  
    2.16 +
    2.17 +axiomatization where
    2.18    (* Propositional logic *)
    2.19 -
    2.20 -  conjI:        "[| P;  Q |] ==> P&Q"
    2.21 -  conjunct1:    "P&Q ==> P"
    2.22 -  conjunct2:    "P&Q ==> Q"
    2.23 +  conjI:        "[| P;  Q |] ==> P&Q" and
    2.24 +  conjunct1:    "P&Q ==> P" and
    2.25 +  conjunct2:    "P&Q ==> Q" and
    2.26  
    2.27 -  disjI1:       "P ==> P|Q"
    2.28 -  disjI2:       "Q ==> P|Q"
    2.29 -  disjE:        "[| P|Q;  P ==> R;  Q ==> R |] ==> R"
    2.30 +  disjI1:       "P ==> P|Q" and
    2.31 +  disjI2:       "Q ==> P|Q" and
    2.32 +  disjE:        "[| P|Q;  P ==> R;  Q ==> R |] ==> R" and
    2.33  
    2.34 -  impI:         "(P ==> Q) ==> P-->Q"
    2.35 -  mp:           "[| P-->Q;  P |] ==> Q"
    2.36 +  impI:         "(P ==> Q) ==> P-->Q" and
    2.37 +  mp:           "[| P-->Q;  P |] ==> Q" and
    2.38  
    2.39    FalseE:       "False ==> P"
    2.40  
    2.41 +axiomatization where
    2.42    (* Quantifiers *)
    2.43 +  allI:         "(!!x. P(x)) ==> (ALL x. P(x))" and
    2.44 +  spec:         "(ALL x. P(x)) ==> P(x)" and
    2.45  
    2.46 -  allI:         "(!!x. P(x)) ==> (ALL x. P(x))"
    2.47 -  spec:         "(ALL x. P(x)) ==> P(x)"
    2.48 -
    2.49 -  exI:          "P(x) ==> (EX x. P(x))"
    2.50 +  exI:          "P(x) ==> (EX x. P(x))" and
    2.51    exE:          "[| EX x. P(x);  !!x. P(x) ==> R |] ==> R"
    2.52  
    2.53  
    2.54 -axioms
    2.55 -
    2.56 +axiomatization where
    2.57    (* Reflection, admissible *)
    2.58 -
    2.59 -  eq_reflection:  "(x=y)   ==> (x==y)"
    2.60 +  eq_reflection:  "(x=y)   ==> (x==y)" and
    2.61    iff_reflection: "(P<->Q) ==> (P==Q)"
    2.62  
    2.63  
     3.1 --- a/src/FOL/ex/Locale_Test/Locale_Test1.thy	Fri Feb 18 16:36:42 2011 +0100
     3.2 +++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy	Fri Feb 18 17:03:30 2011 +0100
     3.3 @@ -13,10 +13,10 @@
     3.4    zero :: int ("0")
     3.5    minus :: "int => int" ("- _")
     3.6  
     3.7 -axioms
     3.8 -  int_assoc: "(x + y::int) + z = x + (y + z)"
     3.9 -  int_zero: "0 + x = x"
    3.10 -  int_minus: "(-x) + x = 0"
    3.11 +axiomatization where
    3.12 +  int_assoc: "(x + y::int) + z = x + (y + z)" and
    3.13 +  int_zero: "0 + x = x" and
    3.14 +  int_minus: "(-x) + x = 0" and
    3.15    int_minus2: "-(-x) = x"
    3.16  
    3.17  section {* Inference of parameter types *}
    3.18 @@ -527,13 +527,12 @@
    3.19  
    3.20  end
    3.21  
    3.22 -consts
    3.23 -  gle :: "'a => 'a => o" gless :: "'a => 'a => o"
    3.24 -  gle' :: "'a => 'a => o" gless' :: "'a => 'a => o"
    3.25 -
    3.26 -axioms
    3.27 -  grefl: "gle(x, x)" gless_def: "gless(x, y) <-> gle(x, y) & x ~= y"
    3.28 -  grefl': "gle'(x, x)" gless'_def: "gless'(x, y) <-> gle'(x, y) & x ~= y"
    3.29 +axiomatization
    3.30 +  gle :: "'a => 'a => o" and gless :: "'a => 'a => o" and
    3.31 +  gle' :: "'a => 'a => o" and gless' :: "'a => 'a => o"
    3.32 +where
    3.33 +  grefl: "gle(x, x)" and gless_def: "gless(x, y) <-> gle(x, y) & x ~= y" and
    3.34 +  grefl': "gle'(x, x)" and gless'_def: "gless'(x, y) <-> gle'(x, y) & x ~= y"
    3.35  
    3.36  text {* Setup *}
    3.37  
     4.1 --- a/src/FOL/ex/Nat.thy	Fri Feb 18 16:36:42 2011 +0100
     4.2 +++ b/src/FOL/ex/Nat.thy	Fri Feb 18 17:03:30 2011 +0100
     4.3 @@ -12,21 +12,19 @@
     4.4  typedecl nat
     4.5  arities nat :: "term"
     4.6  
     4.7 -consts
     4.8 -  Zero :: nat    ("0")
     4.9 -  Suc :: "nat => nat"
    4.10 +axiomatization
    4.11 +  Zero :: nat  ("0") and
    4.12 +  Suc :: "nat => nat" and
    4.13    rec :: "[nat, 'a, [nat, 'a] => 'a] => 'a"
    4.14 -  add :: "[nat, nat] => nat"    (infixl "+" 60)
    4.15 +where
    4.16 +  induct: "[| P(0);  !!x. P(x) ==> P(Suc(x)) |]  ==> P(n)" and
    4.17 +  Suc_inject: "Suc(m)=Suc(n) ==> m=n" and
    4.18 +  Suc_neq_0: "Suc(m)=0 ==> R" and
    4.19 +  rec_0: "rec(0,a,f) = a" and
    4.20 +  rec_Suc: "rec(Suc(m), a, f) = f(m, rec(m,a,f))"
    4.21  
    4.22 -axioms
    4.23 -  induct:      "[| P(0);  !!x. P(x) ==> P(Suc(x)) |]  ==> P(n)"
    4.24 -  Suc_inject:  "Suc(m)=Suc(n) ==> m=n"
    4.25 -  Suc_neq_0:   "Suc(m)=0      ==> R"
    4.26 -  rec_0:       "rec(0,a,f) = a"
    4.27 -  rec_Suc:     "rec(Suc(m), a, f) = f(m, rec(m,a,f))"
    4.28 -
    4.29 -defs
    4.30 -  add_def:     "m+n == rec(m, n, %x y. Suc(y))"
    4.31 +definition add :: "[nat, nat] => nat"  (infixl "+" 60)
    4.32 +  where "m + n == rec(m, n, %x y. Suc(y))"
    4.33  
    4.34  
    4.35  subsection {* Proofs about the natural numbers *}
     5.1 --- a/src/FOL/ex/Prolog.thy	Fri Feb 18 16:36:42 2011 +0100
     5.2 +++ b/src/FOL/ex/Prolog.thy	Fri Feb 18 17:03:30 2011 +0100
     5.3 @@ -11,15 +11,16 @@
     5.4  
     5.5  typedecl 'a list
     5.6  arities list :: ("term") "term"
     5.7 -consts
     5.8 -  Nil     :: "'a list"
     5.9 -  Cons    :: "['a, 'a list]=> 'a list"    (infixr ":" 60)
    5.10 -  app     :: "['a list, 'a list, 'a list] => o"
    5.11 +
    5.12 +axiomatization
    5.13 +  Nil     :: "'a list" and
    5.14 +  Cons    :: "['a, 'a list]=> 'a list"    (infixr ":" 60) and
    5.15 +  app     :: "['a list, 'a list, 'a list] => o" and
    5.16    rev     :: "['a list, 'a list] => o"
    5.17 -axioms
    5.18 -  appNil:  "app(Nil,ys,ys)"
    5.19 -  appCons: "app(xs,ys,zs) ==> app(x:xs, ys, x:zs)"
    5.20 -  revNil:  "rev(Nil,Nil)"
    5.21 +where
    5.22 +  appNil:  "app(Nil,ys,ys)" and
    5.23 +  appCons: "app(xs,ys,zs) ==> app(x:xs, ys, x:zs)" and
    5.24 +  revNil:  "rev(Nil,Nil)" and
    5.25    revCons: "[| rev(xs,ys);  app(ys, x:Nil, zs) |] ==> rev(x:xs, zs)"
    5.26  
    5.27  schematic_lemma "app(a:b:c:Nil, d:e:Nil, ?x)"
     6.1 --- a/src/FOLP/FOLP.thy	Fri Feb 18 16:36:42 2011 +0100
     6.2 +++ b/src/FOLP/FOLP.thy	Fri Feb 18 17:03:30 2011 +0100
     6.3 @@ -11,10 +11,8 @@
     6.4    ("classical.ML") ("simp.ML") ("simpdata.ML")
     6.5  begin
     6.6  
     6.7 -consts
     6.8 -  cla :: "[p=>p]=>p"
     6.9 -axioms
    6.10 -  classical: "(!!x. x:~P ==> f(x):P) ==> cla(f):P"
    6.11 +axiomatization cla :: "[p=>p]=>p"
    6.12 +  where classical: "(!!x. x:~P ==> f(x):P) ==> cla(f):P"
    6.13  
    6.14  
    6.15  (*** Classical introduction rules for | and EX ***)
     7.1 --- a/src/ZF/Coind/Language.thy	Fri Feb 18 16:36:42 2011 +0100
     7.2 +++ b/src/ZF/Coind/Language.thy	Fri Feb 18 17:03:30 2011 +0100
     7.3 @@ -5,14 +5,14 @@
     7.4  
     7.5  theory Language imports Main begin
     7.6  
     7.7 -consts
     7.8 -  Const :: i                    (* Abstract type of constants *)
     7.9 -  c_app :: "[i,i] => i"         (* Abstract constructor for fun application*)
    7.10 -
    7.11  
    7.12  text{*these really can't be definitions without losing the abstraction*}
    7.13 -axioms
    7.14 -  constNEE:  "c \<in> Const ==> c \<noteq> 0"
    7.15 +
    7.16 +axiomatization
    7.17 +  Const :: i  and               (* Abstract type of constants *)
    7.18 +  c_app :: "[i,i] => i"         (* Abstract constructor for fun application*)
    7.19 +where
    7.20 +  constNEE:  "c \<in> Const ==> c \<noteq> 0" and
    7.21    c_appI:    "[| c1 \<in> Const; c2 \<in> Const |] ==> c_app(c1,c2) \<in> Const"
    7.22  
    7.23  
     8.1 --- a/src/ZF/Coind/Static.thy	Fri Feb 18 16:36:42 2011 +0100
     8.2 +++ b/src/ZF/Coind/Static.thy	Fri Feb 18 17:03:30 2011 +0100
     8.3 @@ -9,11 +9,8 @@
     8.4       parameter of the proof.  A concrete version could be defined inductively.
     8.5  ***)
     8.6  
     8.7 -consts
     8.8 -  isof :: "[i,i] => o"
     8.9 -
    8.10 -axioms
    8.11 -  isof_app: "[|isof(c1,t_fun(t1,t2)); isof(c2,t1)|] ==> isof(c_app(c1,c2),t2)"
    8.12 +axiomatization isof :: "[i,i] => o"
    8.13 +  where isof_app: "[|isof(c1,t_fun(t1,t2)); isof(c2,t1)|] ==> isof(c_app(c1,c2),t2)"
    8.14  
    8.15  (*Its extension to environments*)
    8.16  
     9.1 --- a/src/ZF/UNITY/AllocBase.thy	Fri Feb 18 16:36:42 2011 +0100
     9.2 +++ b/src/ZF/UNITY/AllocBase.thy	Fri Feb 18 17:03:30 2011 +0100
     9.3 @@ -7,17 +7,16 @@
     9.4  
     9.5  theory AllocBase imports Follows MultisetSum Guar begin
     9.6  
     9.7 -consts
     9.8 -  NbT      :: i  (* Number of tokens in system *)
     9.9 -  Nclients :: i  (* Number of clients *)
    9.10 -
    9.11  abbreviation (input)
    9.12    tokbag   :: i  (* tokbags could be multisets...or any ordered type?*)
    9.13  where
    9.14    "tokbag == nat"
    9.15  
    9.16 -axioms
    9.17 -  NbT_pos:      "NbT \<in> nat-{0}"
    9.18 +axiomatization
    9.19 +  NbT :: i and  (* Number of tokens in system *)
    9.20 +  Nclients :: i  (* Number of clients *)
    9.21 +where
    9.22 +  NbT_pos: "NbT \<in> nat-{0}" and
    9.23    Nclients_pos: "Nclients \<in> nat-{0}"
    9.24    
    9.25  text{*This function merely sums the elements of a list*}
    9.26 @@ -27,9 +26,7 @@
    9.27    "tokens(Nil) = 0"
    9.28    "tokens (Cons(x,xs)) = x #+ tokens(xs)"
    9.29  
    9.30 -consts
    9.31 -  bag_of :: "i => i"
    9.32 -
    9.33 +consts bag_of :: "i => i"
    9.34  primrec
    9.35    "bag_of(Nil)    = 0"
    9.36    "bag_of(Cons(x,xs)) = {#x#} +# bag_of(xs)"
    9.37 @@ -38,7 +35,7 @@
    9.38  text{*Definitions needed in Client.thy.  We define a recursive predicate
    9.39  using 0 and 1 to code the truth values.*}
    9.40  consts all_distinct0 :: "i=>i"
    9.41 - primrec
    9.42 +primrec
    9.43    "all_distinct0(Nil) = 1"
    9.44    "all_distinct0(Cons(a, l)) =
    9.45       (if a \<in> set_of_list(l) then 0 else all_distinct0(l))"
    10.1 --- a/src/ZF/UNITY/AllocImpl.thy	Fri Feb 18 16:36:42 2011 +0100
    10.2 +++ b/src/ZF/UNITY/AllocImpl.thy	Fri Feb 18 17:03:30 2011 +0100
    10.3 @@ -16,9 +16,9 @@
    10.4    available_tok :: i  (*number of free tokens (T in paper)*)  where
    10.5    "available_tok == Var([succ(succ(2))])"
    10.6  
    10.7 -axioms
    10.8 +axiomatization where
    10.9    alloc_type_assumes [simp]:
   10.10 -  "type_of(NbR) = nat & type_of(available_tok)=nat"
   10.11 +  "type_of(NbR) = nat & type_of(available_tok)=nat" and
   10.12  
   10.13    alloc_default_val_assumes [simp]:
   10.14    "default_val(NbR)  = 0 & default_val(available_tok)=0"
    11.1 --- a/src/ZF/UNITY/ClientImpl.thy	Fri Feb 18 16:36:42 2011 +0100
    11.2 +++ b/src/ZF/UNITY/ClientImpl.thy	Fri Feb 18 17:03:30 2011 +0100
    11.3 @@ -12,13 +12,13 @@
    11.4  abbreviation "rel == Var([1])" (* input history: tokens released *)
    11.5  abbreviation "tok == Var([2])" (* the number of available tokens *)
    11.6  
    11.7 -axioms
    11.8 +axiomatization where
    11.9    type_assumes:
   11.10    "type_of(ask) = list(tokbag) & type_of(giv) = list(tokbag) & 
   11.11 -   type_of(rel) = list(tokbag) & type_of(tok) = nat"
   11.12 +   type_of(rel) = list(tokbag) & type_of(tok) = nat" and
   11.13    default_val_assumes:
   11.14 -  "default_val(ask) = Nil & default_val(giv)  = Nil & 
   11.15 -   default_val(rel)  = Nil & default_val(tok)  = 0"
   11.16 +  "default_val(ask) = Nil & default_val(giv) = Nil & 
   11.17 +   default_val(rel) = Nil & default_val(tok) = 0"
   11.18  
   11.19  
   11.20  (*Array indexing is translated to list indexing as A[n] == nth(n-1,A). *)
    12.1 --- a/src/ZF/UNITY/Mutex.thy	Fri Feb 18 16:36:42 2011 +0100
    12.2 +++ b/src/ZF/UNITY/Mutex.thy	Fri Feb 18 17:03:30 2011 +0100
    12.3 @@ -27,11 +27,11 @@
    12.4  abbreviation "u == Var([0,1])"
    12.5  abbreviation "v == Var([1,0])"
    12.6  
    12.7 -axioms --{** Type declarations  **}
    12.8 -  p_type:  "type_of(p)=bool & default_val(p)=0"
    12.9 -  m_type:  "type_of(m)=int  & default_val(m)=#0"
   12.10 -  n_type:  "type_of(n)=int  & default_val(n)=#0"
   12.11 -  u_type:  "type_of(u)=bool & default_val(u)=0"
   12.12 +axiomatization where --{** Type declarations  **}
   12.13 +  p_type:  "type_of(p)=bool & default_val(p)=0" and
   12.14 +  m_type:  "type_of(m)=int  & default_val(m)=#0" and
   12.15 +  n_type:  "type_of(n)=int  & default_val(n)=#0" and
   12.16 +  u_type:  "type_of(u)=bool & default_val(u)=0" and
   12.17    v_type:  "type_of(v)=bool & default_val(v)=0"
   12.18  
   12.19  definition
    13.1 --- a/src/ZF/ZF.thy	Fri Feb 18 16:36:42 2011 +0100
    13.2 +++ b/src/ZF/ZF.thy	Fri Feb 18 17:03:30 2011 +0100
    13.3 @@ -207,21 +207,21 @@
    13.4    subset_def:    "A <= B == \<forall>x\<in>A. x\<in>B"
    13.5  
    13.6  
    13.7 -axioms
    13.8 +axiomatization where
    13.9  
   13.10    (* ZF axioms -- see Suppes p.238
   13.11       Axioms for Union, Pow and Replace state existence only,
   13.12       uniqueness is derivable using extensionality. *)
   13.13  
   13.14 -  extension:     "A = B <-> A <= B & B <= A"
   13.15 -  Union_iff:     "A \<in> Union(C) <-> (\<exists>B\<in>C. A\<in>B)"
   13.16 -  Pow_iff:       "A \<in> Pow(B) <-> A <= B"
   13.17 +  extension:     "A = B <-> A <= B & B <= A" and
   13.18 +  Union_iff:     "A \<in> Union(C) <-> (\<exists>B\<in>C. A\<in>B)" and
   13.19 +  Pow_iff:       "A \<in> Pow(B) <-> A <= B" and
   13.20  
   13.21    (*We may name this set, though it is not uniquely defined.*)
   13.22 -  infinity:      "0\<in>Inf & (\<forall>y\<in>Inf. succ(y): Inf)"
   13.23 +  infinity:      "0\<in>Inf & (\<forall>y\<in>Inf. succ(y): Inf)" and
   13.24  
   13.25    (*This formulation facilitates case analysis on A.*)
   13.26 -  foundation:    "A=0 | (\<exists>x\<in>A. \<forall>y\<in>x. y~:A)"
   13.27 +  foundation:    "A=0 | (\<exists>x\<in>A. \<forall>y\<in>x. y~:A)" and
   13.28  
   13.29    (*Schema axiom since predicate P is a higher-order variable*)
   13.30    replacement:   "(\<forall>x\<in>A. \<forall>y z. P(x,y) & P(x,z) --> y=z) ==>
    14.1 --- a/src/ZF/ex/LList.thy	Fri Feb 18 16:36:42 2011 +0100
    14.2 +++ b/src/ZF/ex/LList.thy	Fri Feb 18 17:03:30 2011 +0100
    14.3 @@ -43,11 +43,9 @@
    14.4    lconst   :: "i => i"  where
    14.5    "lconst(a) == lfp(univ(a), %l. LCons(a,l))"
    14.6  
    14.7 -consts
    14.8 -  flip     :: "i => i"
    14.9 -axioms
   14.10 -  flip_LNil:   "flip(LNil) = LNil"
   14.11 -
   14.12 +axiomatization flip :: "i => i"
   14.13 +where
   14.14 +  flip_LNil:   "flip(LNil) = LNil" and
   14.15    flip_LCons:  "[| x \<in> bool; l \<in> llist(bool) |] 
   14.16                  ==> flip(LCons(x,l)) = LCons(not(x), flip(l))"
   14.17