--- 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"
--- 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 \<Longrightarrow> P(a) \<Longrightarrow> 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)"
--- 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 *}
--- 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 *}
--- 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)"
--- 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 ***)
--- 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 \<in> Const ==> c \<noteq> 0"
+
+axiomatization
+ Const :: i and (* Abstract type of constants *)
+ c_app :: "[i,i] => i" (* Abstract constructor for fun application*)
+where
+ constNEE: "c \<in> Const ==> c \<noteq> 0" and
c_appI: "[| c1 \<in> Const; c2 \<in> Const |] ==> c_app(c1,c2) \<in> Const"
--- 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*)
--- 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 \<in> nat-{0}"
+axiomatization
+ NbT :: i and (* Number of tokens in system *)
+ Nclients :: i (* Number of clients *)
+where
+ NbT_pos: "NbT \<in> nat-{0}" and
Nclients_pos: "Nclients \<in> 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 \<in> set_of_list(l) then 0 else all_distinct0(l))"
--- 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"
--- 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). *)
--- 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
--- 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 == \<forall>x\<in>A. x\<in>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 \<in> Union(C) <-> (\<exists>B\<in>C. A\<in>B)"
- Pow_iff: "A \<in> Pow(B) <-> A <= B"
+ extension: "A = B <-> A <= B & B <= A" and
+ Union_iff: "A \<in> Union(C) <-> (\<exists>B\<in>C. A\<in>B)" and
+ Pow_iff: "A \<in> Pow(B) <-> A <= B" and
(*We may name this set, though it is not uniquely defined.*)
- infinity: "0\<in>Inf & (\<forall>y\<in>Inf. succ(y): Inf)"
+ infinity: "0\<in>Inf & (\<forall>y\<in>Inf. succ(y): Inf)" and
(*This formulation facilitates case analysis on A.*)
- foundation: "A=0 | (\<exists>x\<in>A. \<forall>y\<in>x. y~:A)"
+ foundation: "A=0 | (\<exists>x\<in>A. \<forall>y\<in>x. y~:A)" and
(*Schema axiom since predicate P is a higher-order variable*)
replacement: "(\<forall>x\<in>A. \<forall>y z. P(x,y) & P(x,z) --> y=z) ==>
--- 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 \<in> bool; l \<in> llist(bool) |]
==> flip(LCons(x,l)) = LCons(not(x), flip(l))"