# HG changeset patch # User wenzelm # Date 1298045010 -3600 # Node ID a68f503805ed9a97598c602e4e4b4ce8753d4df1 # Parent 5f79a9e425075417e75928bc2f0880cb6fcdb045 modernized specifications; diff -r 5f79a9e42507 -r a68f503805ed src/FOL/FOL.thy --- a/src/FOL/FOL.thy Fri Feb 18 16:36:42 2011 +0100 +++ b/src/FOL/FOL.thy Fri Feb 18 17:03:30 2011 +0100 @@ -18,7 +18,7 @@ subsection {* The classical axiom *} -axioms +axiomatization where classical: "(~P ==> P) ==> P" diff -r 5f79a9e42507 -r a68f503805ed src/FOL/IFOL.thy --- a/src/FOL/IFOL.thy Fri Feb 18 16:36:42 2011 +0100 +++ b/src/FOL/IFOL.thy Fri Feb 18 17:03:30 2011 +0100 @@ -88,42 +88,39 @@ finalconsts False All Ex eq conj disj imp -axioms - +axiomatization where (* Equality *) - - refl: "a=a" + refl: "a=a" and subst: "a=b \ P(a) \ P(b)" + +axiomatization where (* Propositional logic *) - - conjI: "[| P; Q |] ==> P&Q" - conjunct1: "P&Q ==> P" - conjunct2: "P&Q ==> Q" + conjI: "[| P; Q |] ==> P&Q" and + conjunct1: "P&Q ==> P" and + conjunct2: "P&Q ==> Q" and - disjI1: "P ==> P|Q" - disjI2: "Q ==> P|Q" - disjE: "[| P|Q; P ==> R; Q ==> R |] ==> R" + disjI1: "P ==> P|Q" and + disjI2: "Q ==> P|Q" and + disjE: "[| P|Q; P ==> R; Q ==> R |] ==> R" and - impI: "(P ==> Q) ==> P-->Q" - mp: "[| P-->Q; P |] ==> Q" + impI: "(P ==> Q) ==> P-->Q" and + mp: "[| P-->Q; P |] ==> Q" and FalseE: "False ==> P" +axiomatization where (* Quantifiers *) + allI: "(!!x. P(x)) ==> (ALL x. P(x))" and + spec: "(ALL x. P(x)) ==> P(x)" and - allI: "(!!x. P(x)) ==> (ALL x. P(x))" - spec: "(ALL x. P(x)) ==> P(x)" - - exI: "P(x) ==> (EX x. P(x))" + exI: "P(x) ==> (EX x. P(x))" and exE: "[| EX x. P(x); !!x. P(x) ==> R |] ==> R" -axioms - +axiomatization where (* Reflection, admissible *) - - eq_reflection: "(x=y) ==> (x==y)" + eq_reflection: "(x=y) ==> (x==y)" and iff_reflection: "(P<->Q) ==> (P==Q)" diff -r 5f79a9e42507 -r a68f503805ed src/FOL/ex/Locale_Test/Locale_Test1.thy --- a/src/FOL/ex/Locale_Test/Locale_Test1.thy Fri Feb 18 16:36:42 2011 +0100 +++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy Fri Feb 18 17:03:30 2011 +0100 @@ -13,10 +13,10 @@ zero :: int ("0") minus :: "int => int" ("- _") -axioms - int_assoc: "(x + y::int) + z = x + (y + z)" - int_zero: "0 + x = x" - int_minus: "(-x) + x = 0" +axiomatization where + int_assoc: "(x + y::int) + z = x + (y + z)" and + int_zero: "0 + x = x" and + int_minus: "(-x) + x = 0" and int_minus2: "-(-x) = x" section {* Inference of parameter types *} @@ -527,13 +527,12 @@ end -consts - gle :: "'a => 'a => o" gless :: "'a => 'a => o" - gle' :: "'a => 'a => o" gless' :: "'a => 'a => o" - -axioms - grefl: "gle(x, x)" gless_def: "gless(x, y) <-> gle(x, y) & x ~= y" - grefl': "gle'(x, x)" gless'_def: "gless'(x, y) <-> gle'(x, y) & x ~= y" +axiomatization + gle :: "'a => 'a => o" and gless :: "'a => 'a => o" and + gle' :: "'a => 'a => o" and gless' :: "'a => 'a => o" +where + grefl: "gle(x, x)" and gless_def: "gless(x, y) <-> gle(x, y) & x ~= y" and + grefl': "gle'(x, x)" and gless'_def: "gless'(x, y) <-> gle'(x, y) & x ~= y" text {* Setup *} diff -r 5f79a9e42507 -r a68f503805ed src/FOL/ex/Nat.thy --- a/src/FOL/ex/Nat.thy Fri Feb 18 16:36:42 2011 +0100 +++ b/src/FOL/ex/Nat.thy Fri Feb 18 17:03:30 2011 +0100 @@ -12,21 +12,19 @@ typedecl nat arities nat :: "term" -consts - Zero :: nat ("0") - Suc :: "nat => nat" +axiomatization + Zero :: nat ("0") and + Suc :: "nat => nat" and rec :: "[nat, 'a, [nat, 'a] => 'a] => 'a" - add :: "[nat, nat] => nat" (infixl "+" 60) +where + induct: "[| P(0); !!x. P(x) ==> P(Suc(x)) |] ==> P(n)" and + Suc_inject: "Suc(m)=Suc(n) ==> m=n" and + Suc_neq_0: "Suc(m)=0 ==> R" and + rec_0: "rec(0,a,f) = a" and + rec_Suc: "rec(Suc(m), a, f) = f(m, rec(m,a,f))" -axioms - induct: "[| P(0); !!x. P(x) ==> P(Suc(x)) |] ==> P(n)" - Suc_inject: "Suc(m)=Suc(n) ==> m=n" - Suc_neq_0: "Suc(m)=0 ==> R" - rec_0: "rec(0,a,f) = a" - rec_Suc: "rec(Suc(m), a, f) = f(m, rec(m,a,f))" - -defs - add_def: "m+n == rec(m, n, %x y. Suc(y))" +definition add :: "[nat, nat] => nat" (infixl "+" 60) + where "m + n == rec(m, n, %x y. Suc(y))" subsection {* Proofs about the natural numbers *} diff -r 5f79a9e42507 -r a68f503805ed src/FOL/ex/Prolog.thy --- a/src/FOL/ex/Prolog.thy Fri Feb 18 16:36:42 2011 +0100 +++ b/src/FOL/ex/Prolog.thy Fri Feb 18 17:03:30 2011 +0100 @@ -11,15 +11,16 @@ typedecl 'a list arities list :: ("term") "term" -consts - Nil :: "'a list" - Cons :: "['a, 'a list]=> 'a list" (infixr ":" 60) - app :: "['a list, 'a list, 'a list] => o" + +axiomatization + Nil :: "'a list" and + Cons :: "['a, 'a list]=> 'a list" (infixr ":" 60) and + app :: "['a list, 'a list, 'a list] => o" and rev :: "['a list, 'a list] => o" -axioms - appNil: "app(Nil,ys,ys)" - appCons: "app(xs,ys,zs) ==> app(x:xs, ys, x:zs)" - revNil: "rev(Nil,Nil)" +where + appNil: "app(Nil,ys,ys)" and + appCons: "app(xs,ys,zs) ==> app(x:xs, ys, x:zs)" and + revNil: "rev(Nil,Nil)" and revCons: "[| rev(xs,ys); app(ys, x:Nil, zs) |] ==> rev(x:xs, zs)" schematic_lemma "app(a:b:c:Nil, d:e:Nil, ?x)" diff -r 5f79a9e42507 -r a68f503805ed src/FOLP/FOLP.thy --- a/src/FOLP/FOLP.thy Fri Feb 18 16:36:42 2011 +0100 +++ b/src/FOLP/FOLP.thy Fri Feb 18 17:03:30 2011 +0100 @@ -11,10 +11,8 @@ ("classical.ML") ("simp.ML") ("simpdata.ML") begin -consts - cla :: "[p=>p]=>p" -axioms - classical: "(!!x. x:~P ==> f(x):P) ==> cla(f):P" +axiomatization cla :: "[p=>p]=>p" + where classical: "(!!x. x:~P ==> f(x):P) ==> cla(f):P" (*** Classical introduction rules for | and EX ***) diff -r 5f79a9e42507 -r a68f503805ed src/ZF/Coind/Language.thy --- a/src/ZF/Coind/Language.thy Fri Feb 18 16:36:42 2011 +0100 +++ b/src/ZF/Coind/Language.thy Fri Feb 18 17:03:30 2011 +0100 @@ -5,14 +5,14 @@ theory Language imports Main begin -consts - Const :: i (* Abstract type of constants *) - c_app :: "[i,i] => i" (* Abstract constructor for fun application*) - text{*these really can't be definitions without losing the abstraction*} -axioms - constNEE: "c \ Const ==> c \ 0" + +axiomatization + Const :: i and (* Abstract type of constants *) + c_app :: "[i,i] => i" (* Abstract constructor for fun application*) +where + constNEE: "c \ Const ==> c \ 0" and c_appI: "[| c1 \ Const; c2 \ Const |] ==> c_app(c1,c2) \ Const" diff -r 5f79a9e42507 -r a68f503805ed src/ZF/Coind/Static.thy --- a/src/ZF/Coind/Static.thy Fri Feb 18 16:36:42 2011 +0100 +++ b/src/ZF/Coind/Static.thy Fri Feb 18 17:03:30 2011 +0100 @@ -9,11 +9,8 @@ parameter of the proof. A concrete version could be defined inductively. ***) -consts - isof :: "[i,i] => o" - -axioms - isof_app: "[|isof(c1,t_fun(t1,t2)); isof(c2,t1)|] ==> isof(c_app(c1,c2),t2)" +axiomatization isof :: "[i,i] => o" + where isof_app: "[|isof(c1,t_fun(t1,t2)); isof(c2,t1)|] ==> isof(c_app(c1,c2),t2)" (*Its extension to environments*) diff -r 5f79a9e42507 -r a68f503805ed src/ZF/UNITY/AllocBase.thy --- a/src/ZF/UNITY/AllocBase.thy Fri Feb 18 16:36:42 2011 +0100 +++ b/src/ZF/UNITY/AllocBase.thy Fri Feb 18 17:03:30 2011 +0100 @@ -7,17 +7,16 @@ theory AllocBase imports Follows MultisetSum Guar begin -consts - NbT :: i (* Number of tokens in system *) - Nclients :: i (* Number of clients *) - abbreviation (input) tokbag :: i (* tokbags could be multisets...or any ordered type?*) where "tokbag == nat" -axioms - NbT_pos: "NbT \ nat-{0}" +axiomatization + NbT :: i and (* Number of tokens in system *) + Nclients :: i (* Number of clients *) +where + NbT_pos: "NbT \ nat-{0}" and Nclients_pos: "Nclients \ nat-{0}" text{*This function merely sums the elements of a list*} @@ -27,9 +26,7 @@ "tokens(Nil) = 0" "tokens (Cons(x,xs)) = x #+ tokens(xs)" -consts - bag_of :: "i => i" - +consts bag_of :: "i => i" primrec "bag_of(Nil) = 0" "bag_of(Cons(x,xs)) = {#x#} +# bag_of(xs)" @@ -38,7 +35,7 @@ text{*Definitions needed in Client.thy. We define a recursive predicate using 0 and 1 to code the truth values.*} consts all_distinct0 :: "i=>i" - primrec +primrec "all_distinct0(Nil) = 1" "all_distinct0(Cons(a, l)) = (if a \ set_of_list(l) then 0 else all_distinct0(l))" diff -r 5f79a9e42507 -r a68f503805ed src/ZF/UNITY/AllocImpl.thy --- a/src/ZF/UNITY/AllocImpl.thy Fri Feb 18 16:36:42 2011 +0100 +++ b/src/ZF/UNITY/AllocImpl.thy Fri Feb 18 17:03:30 2011 +0100 @@ -16,9 +16,9 @@ available_tok :: i (*number of free tokens (T in paper)*) where "available_tok == Var([succ(succ(2))])" -axioms +axiomatization where alloc_type_assumes [simp]: - "type_of(NbR) = nat & type_of(available_tok)=nat" + "type_of(NbR) = nat & type_of(available_tok)=nat" and alloc_default_val_assumes [simp]: "default_val(NbR) = 0 & default_val(available_tok)=0" diff -r 5f79a9e42507 -r a68f503805ed src/ZF/UNITY/ClientImpl.thy --- a/src/ZF/UNITY/ClientImpl.thy Fri Feb 18 16:36:42 2011 +0100 +++ b/src/ZF/UNITY/ClientImpl.thy Fri Feb 18 17:03:30 2011 +0100 @@ -12,13 +12,13 @@ abbreviation "rel == Var([1])" (* input history: tokens released *) abbreviation "tok == Var([2])" (* the number of available tokens *) -axioms +axiomatization where type_assumes: "type_of(ask) = list(tokbag) & type_of(giv) = list(tokbag) & - type_of(rel) = list(tokbag) & type_of(tok) = nat" + type_of(rel) = list(tokbag) & type_of(tok) = nat" and default_val_assumes: - "default_val(ask) = Nil & default_val(giv) = Nil & - default_val(rel) = Nil & default_val(tok) = 0" + "default_val(ask) = Nil & default_val(giv) = Nil & + default_val(rel) = Nil & default_val(tok) = 0" (*Array indexing is translated to list indexing as A[n] == nth(n-1,A). *) diff -r 5f79a9e42507 -r a68f503805ed src/ZF/UNITY/Mutex.thy --- a/src/ZF/UNITY/Mutex.thy Fri Feb 18 16:36:42 2011 +0100 +++ b/src/ZF/UNITY/Mutex.thy Fri Feb 18 17:03:30 2011 +0100 @@ -27,11 +27,11 @@ abbreviation "u == Var([0,1])" abbreviation "v == Var([1,0])" -axioms --{** Type declarations **} - p_type: "type_of(p)=bool & default_val(p)=0" - m_type: "type_of(m)=int & default_val(m)=#0" - n_type: "type_of(n)=int & default_val(n)=#0" - u_type: "type_of(u)=bool & default_val(u)=0" +axiomatization where --{** Type declarations **} + p_type: "type_of(p)=bool & default_val(p)=0" and + m_type: "type_of(m)=int & default_val(m)=#0" and + n_type: "type_of(n)=int & default_val(n)=#0" and + u_type: "type_of(u)=bool & default_val(u)=0" and v_type: "type_of(v)=bool & default_val(v)=0" definition diff -r 5f79a9e42507 -r a68f503805ed src/ZF/ZF.thy --- a/src/ZF/ZF.thy Fri Feb 18 16:36:42 2011 +0100 +++ b/src/ZF/ZF.thy Fri Feb 18 17:03:30 2011 +0100 @@ -207,21 +207,21 @@ subset_def: "A <= B == \x\A. x\B" -axioms +axiomatization where (* ZF axioms -- see Suppes p.238 Axioms for Union, Pow and Replace state existence only, uniqueness is derivable using extensionality. *) - extension: "A = B <-> A <= B & B <= A" - Union_iff: "A \ Union(C) <-> (\B\C. A\B)" - Pow_iff: "A \ Pow(B) <-> A <= B" + extension: "A = B <-> A <= B & B <= A" and + Union_iff: "A \ Union(C) <-> (\B\C. A\B)" and + Pow_iff: "A \ Pow(B) <-> A <= B" and (*We may name this set, though it is not uniquely defined.*) - infinity: "0\Inf & (\y\Inf. succ(y): Inf)" + infinity: "0\Inf & (\y\Inf. succ(y): Inf)" and (*This formulation facilitates case analysis on A.*) - foundation: "A=0 | (\x\A. \y\x. y~:A)" + foundation: "A=0 | (\x\A. \y\x. y~:A)" and (*Schema axiom since predicate P is a higher-order variable*) replacement: "(\x\A. \y z. P(x,y) & P(x,z) --> y=z) ==> diff -r 5f79a9e42507 -r a68f503805ed src/ZF/ex/LList.thy --- a/src/ZF/ex/LList.thy Fri Feb 18 16:36:42 2011 +0100 +++ b/src/ZF/ex/LList.thy Fri Feb 18 17:03:30 2011 +0100 @@ -43,11 +43,9 @@ lconst :: "i => i" where "lconst(a) == lfp(univ(a), %l. LCons(a,l))" -consts - flip :: "i => i" -axioms - flip_LNil: "flip(LNil) = LNil" - +axiomatization flip :: "i => i" +where + flip_LNil: "flip(LNil) = LNil" and flip_LCons: "[| x \ bool; l \ llist(bool) |] ==> flip(LCons(x,l)) = LCons(not(x), flip(l))"