# HG changeset patch
# User wenzelm
# Date 1362055605 -3600
# Node ID f0e5af7aa68bb75e733ef39cdfc8f28856ddeb9f
# Parent  4a96f9e28e6d25ef9b427374751f9c74a639cfc5
eliminated legacy 'axioms';

diff -r 4a96f9e28e6d -r f0e5af7aa68b src/FOLP/IFOLP.thy
--- a/src/FOLP/IFOLP.thy	Thu Feb 28 13:33:01 2013 +0100
+++ b/src/FOLP/IFOLP.thy	Thu Feb 28 13:46:45 2013 +0100
@@ -80,71 +80,84 @@
   in [(@{const_syntax Proof}, proof_tr')] end
 *}
 
-axioms
 
 (**** Propositional logic ****)
 
 (*Equality*)
 (* Like Intensional Equality in MLTT - but proofs distinct from terms *)
 
-ieqI:      "ideq(a) : a=a"
+axiomatization where
+ieqI:      "ideq(a) : a=a" and
 ieqE:      "[| p : a=b;  !!x. f(x) : P(x,x) |] ==> idpeel(p,f) : P(a,b)"
 
 (* Truth and Falsity *)
 
-TrueI:     "tt : True"
+axiomatization where
+TrueI:     "tt : True" and
 FalseE:    "a:False ==> contr(a):P"
 
 (* Conjunction *)
 
-conjI:     "[| a:P;  b:Q |] ==> <a,b> : P&Q"
-conjunct1: "p:P&Q ==> fst(p):P"
+axiomatization where
+conjI:     "[| a:P;  b:Q |] ==> <a,b> : P&Q" and
+conjunct1: "p:P&Q ==> fst(p):P" and
 conjunct2: "p:P&Q ==> snd(p):Q"
 
 (* Disjunction *)
 
-disjI1:    "a:P ==> inl(a):P|Q"
-disjI2:    "b:Q ==> inr(b):P|Q"
+axiomatization where
+disjI1:    "a:P ==> inl(a):P|Q" and
+disjI2:    "b:Q ==> inr(b):P|Q" and
 disjE:     "[| a:P|Q;  !!x. x:P ==> f(x):R;  !!x. x:Q ==> g(x):R
            |] ==> when(a,f,g):R"
 
 (* Implication *)
 
-impI:      "(!!x. x:P ==> f(x):Q) ==> lam x. f(x):P-->Q"
-mp:        "[| f:P-->Q;  a:P |] ==> f`a:Q"
+axiomatization where
+impI:      "\<And>P Q f. (!!x. x:P ==> f(x):Q) ==> lam x. f(x):P-->Q" and
+mp:        "\<And>P Q f. [| f:P-->Q;  a:P |] ==> f`a:Q"
 
 (*Quantifiers*)
 
-allI:      "(!!x. f(x) : P(x)) ==> all x. f(x) : ALL x. P(x)"
-spec:      "(f:ALL x. P(x)) ==> f^x : P(x)"
+axiomatization where
+allI:      "\<And>P. (!!x. f(x) : P(x)) ==> all x. f(x) : ALL x. P(x)" and
+spec:      "\<And>P f. (f:ALL x. P(x)) ==> f^x : P(x)"
 
-exI:       "p : P(x) ==> [x,p] : EX x. P(x)"
+axiomatization where
+exI:       "p : P(x) ==> [x,p] : EX x. P(x)" and
 exE:       "[| p: EX x. P(x);  !!x u. u:P(x) ==> f(x,u) : R |] ==> xsplit(p,f):R"
 
 (**** Equality between proofs ****)
 
-prefl:     "a : P ==> a = a : P"
-psym:      "a = b : P ==> b = a : P"
+axiomatization where
+prefl:     "a : P ==> a = a : P" and
+psym:      "a = b : P ==> b = a : P" and
 ptrans:    "[| a = b : P;  b = c : P |] ==> a = c : P"
 
+axiomatization where
 idpeelB:   "[| !!x. f(x) : P(x,x) |] ==> idpeel(ideq(a),f) = f(a) : P(a,a)"
 
-fstB:      "a:P ==> fst(<a,b>) = a : P"
-sndB:      "b:Q ==> snd(<a,b>) = b : Q"
+axiomatization where
+fstB:      "a:P ==> fst(<a,b>) = a : P" and
+sndB:      "b:Q ==> snd(<a,b>) = b : Q" and
 pairEC:    "p:P&Q ==> p = <fst(p),snd(p)> : P&Q"
 
-whenBinl:  "[| a:P;  !!x. x:P ==> f(x) : Q |] ==> when(inl(a),f,g) = f(a) : Q"
-whenBinr:  "[| b:P;  !!x. x:P ==> g(x) : Q |] ==> when(inr(b),f,g) = g(b) : Q"
+axiomatization where
+whenBinl:  "[| a:P;  !!x. x:P ==> f(x) : Q |] ==> when(inl(a),f,g) = f(a) : Q" and
+whenBinr:  "[| b:P;  !!x. x:P ==> g(x) : Q |] ==> when(inr(b),f,g) = g(b) : Q" and
 plusEC:    "a:P|Q ==> when(a,%x. inl(x),%y. inr(y)) = a : P|Q"
 
-applyB:     "[| a:P;  !!x. x:P ==> b(x) : Q |] ==> (lam x. b(x)) ` a = b(a) : Q"
+axiomatization where
+applyB:     "[| a:P;  !!x. x:P ==> b(x) : Q |] ==> (lam x. b(x)) ` a = b(a) : Q" and
 funEC:      "f:P ==> f = lam x. f`x : P"
 
+axiomatization where
 specB:      "[| !!x. f(x) : P(x) |] ==> (all x. f(x)) ^ a = f(a) : P(a)"
 
 
 (**** Definitions ****)
 
+defs
 not_def:              "~P == P-->False"
 iff_def:         "P<->Q == (P-->Q) & (Q-->P)"
 
@@ -152,7 +165,8 @@
 ex1_def:   "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)"
 
 (*Rewriting -- special constants to flag normalized terms and formulae*)
-norm_eq: "nrm : norm(x) = x"
+axiomatization where
+norm_eq: "nrm : norm(x) = x" and
 NORM_iff:        "NRM : NORM(P) <-> P"
 
 (*** Sequent-style elimination rules for & --> and ALL ***)
diff -r 4a96f9e28e6d -r f0e5af7aa68b src/FOLP/ex/Nat.thy
--- a/src/FOLP/ex/Nat.thy	Thu Feb 28 13:33:01 2013 +0100
+++ b/src/FOLP/ex/Nat.thy	Thu Feb 28 13:46:45 2013 +0100
@@ -12,34 +12,30 @@
 typedecl nat
 arities nat :: "term"
 
-consts
-  Zero :: nat    ("0")
-  Suc :: "nat => nat"
-  rec :: "[nat, 'a, [nat, 'a] => 'a] => 'a"
-  add :: "[nat, nat] => nat"    (infixl "+" 60)
+axiomatization
+  Zero :: nat    ("0") and
+  Suc :: "nat => nat" and
+  rec :: "[nat, 'a, [nat, 'a] => 'a] => 'a" and
 
   (*Proof terms*)
-  nrec :: "[nat, p, [nat, p] => p] => p"
-  ninj :: "p => p"
-  nneq :: "p => p"
-  rec0 :: "p"
+  nrec :: "[nat, p, [nat, p] => p] => p" and
+  ninj :: "p => p" and
+  nneq :: "p => p" and
+  rec0 :: "p" and
   recSuc :: "p"
-
-axioms
+where
   induct:     "[| b:P(0); !!x u. u:P(x) ==> c(x,u):P(Suc(x))
-              |] ==> nrec(n,b,c):P(n)"
+              |] ==> nrec(n,b,c):P(n)" and
 
-  Suc_inject: "p:Suc(m)=Suc(n) ==> ninj(p) : m=n"
-  Suc_neq_0:  "p:Suc(m)=0      ==> nneq(p) : R"
-  rec_0:      "rec0 : rec(0,a,f) = a"
-  rec_Suc:    "recSuc : rec(Suc(m), a, f) = f(m, rec(m,a,f))"
+  Suc_inject: "p:Suc(m)=Suc(n) ==> ninj(p) : m=n" and
+  Suc_neq_0:  "p:Suc(m)=0      ==> nneq(p) : R" and
+  rec_0:      "rec0 : rec(0,a,f) = a" and
+  rec_Suc:    "recSuc : rec(Suc(m), a, f) = f(m, rec(m,a,f))" and
+  nrecB0:     "b: A ==> nrec(0,b,c) = b : A" and
+  nrecBSuc:   "c(n,nrec(n,b,c)) : A ==> nrec(Suc(n),b,c) = c(n,nrec(n,b,c)) : A"
 
-defs
-  add_def:    "m+n == rec(m, n, %x y. Suc(y))"
-
-axioms
-  nrecB0:     "b: A ==> nrec(0,b,c) = b : A"
-  nrecBSuc:   "c(n,nrec(n,b,c)) : A ==> nrec(Suc(n),b,c) = c(n,nrec(n,b,c)) : A"
+definition add :: "[nat, nat] => nat"    (infixl "+" 60)
+  where "m + n == rec(m, n, %x y. Suc(y))"
 
 
 subsection {* Proofs about the natural numbers *}