1.1 --- a/src/FOLP/IFOLP.thy Thu Feb 28 13:33:01 2013 +0100
1.2 +++ b/src/FOLP/IFOLP.thy Thu Feb 28 13:46:45 2013 +0100
1.3 @@ -80,71 +80,84 @@
1.4 in [(@{const_syntax Proof}, proof_tr')] end
1.5 *}
1.6
1.7 -axioms
1.8
1.9 (**** Propositional logic ****)
1.10
1.11 (*Equality*)
1.12 (* Like Intensional Equality in MLTT - but proofs distinct from terms *)
1.13
1.14 -ieqI: "ideq(a) : a=a"
1.15 +axiomatization where
1.16 +ieqI: "ideq(a) : a=a" and
1.17 ieqE: "[| p : a=b; !!x. f(x) : P(x,x) |] ==> idpeel(p,f) : P(a,b)"
1.18
1.19 (* Truth and Falsity *)
1.20
1.21 -TrueI: "tt : True"
1.22 +axiomatization where
1.23 +TrueI: "tt : True" and
1.24 FalseE: "a:False ==> contr(a):P"
1.25
1.26 (* Conjunction *)
1.27
1.28 -conjI: "[| a:P; b:Q |] ==> <a,b> : P&Q"
1.29 -conjunct1: "p:P&Q ==> fst(p):P"
1.30 +axiomatization where
1.31 +conjI: "[| a:P; b:Q |] ==> <a,b> : P&Q" and
1.32 +conjunct1: "p:P&Q ==> fst(p):P" and
1.33 conjunct2: "p:P&Q ==> snd(p):Q"
1.34
1.35 (* Disjunction *)
1.36
1.37 -disjI1: "a:P ==> inl(a):P|Q"
1.38 -disjI2: "b:Q ==> inr(b):P|Q"
1.39 +axiomatization where
1.40 +disjI1: "a:P ==> inl(a):P|Q" and
1.41 +disjI2: "b:Q ==> inr(b):P|Q" and
1.42 disjE: "[| a:P|Q; !!x. x:P ==> f(x):R; !!x. x:Q ==> g(x):R
1.43 |] ==> when(a,f,g):R"
1.44
1.45 (* Implication *)
1.46
1.47 -impI: "(!!x. x:P ==> f(x):Q) ==> lam x. f(x):P-->Q"
1.48 -mp: "[| f:P-->Q; a:P |] ==> f`a:Q"
1.49 +axiomatization where
1.50 +impI: "\<And>P Q f. (!!x. x:P ==> f(x):Q) ==> lam x. f(x):P-->Q" and
1.51 +mp: "\<And>P Q f. [| f:P-->Q; a:P |] ==> f`a:Q"
1.52
1.53 (*Quantifiers*)
1.54
1.55 -allI: "(!!x. f(x) : P(x)) ==> all x. f(x) : ALL x. P(x)"
1.56 -spec: "(f:ALL x. P(x)) ==> f^x : P(x)"
1.57 +axiomatization where
1.58 +allI: "\<And>P. (!!x. f(x) : P(x)) ==> all x. f(x) : ALL x. P(x)" and
1.59 +spec: "\<And>P f. (f:ALL x. P(x)) ==> f^x : P(x)"
1.60
1.61 -exI: "p : P(x) ==> [x,p] : EX x. P(x)"
1.62 +axiomatization where
1.63 +exI: "p : P(x) ==> [x,p] : EX x. P(x)" and
1.64 exE: "[| p: EX x. P(x); !!x u. u:P(x) ==> f(x,u) : R |] ==> xsplit(p,f):R"
1.65
1.66 (**** Equality between proofs ****)
1.67
1.68 -prefl: "a : P ==> a = a : P"
1.69 -psym: "a = b : P ==> b = a : P"
1.70 +axiomatization where
1.71 +prefl: "a : P ==> a = a : P" and
1.72 +psym: "a = b : P ==> b = a : P" and
1.73 ptrans: "[| a = b : P; b = c : P |] ==> a = c : P"
1.74
1.75 +axiomatization where
1.76 idpeelB: "[| !!x. f(x) : P(x,x) |] ==> idpeel(ideq(a),f) = f(a) : P(a,a)"
1.77
1.78 -fstB: "a:P ==> fst(<a,b>) = a : P"
1.79 -sndB: "b:Q ==> snd(<a,b>) = b : Q"
1.80 +axiomatization where
1.81 +fstB: "a:P ==> fst(<a,b>) = a : P" and
1.82 +sndB: "b:Q ==> snd(<a,b>) = b : Q" and
1.83 pairEC: "p:P&Q ==> p = <fst(p),snd(p)> : P&Q"
1.84
1.85 -whenBinl: "[| a:P; !!x. x:P ==> f(x) : Q |] ==> when(inl(a),f,g) = f(a) : Q"
1.86 -whenBinr: "[| b:P; !!x. x:P ==> g(x) : Q |] ==> when(inr(b),f,g) = g(b) : Q"
1.87 +axiomatization where
1.88 +whenBinl: "[| a:P; !!x. x:P ==> f(x) : Q |] ==> when(inl(a),f,g) = f(a) : Q" and
1.89 +whenBinr: "[| b:P; !!x. x:P ==> g(x) : Q |] ==> when(inr(b),f,g) = g(b) : Q" and
1.90 plusEC: "a:P|Q ==> when(a,%x. inl(x),%y. inr(y)) = a : P|Q"
1.91
1.92 -applyB: "[| a:P; !!x. x:P ==> b(x) : Q |] ==> (lam x. b(x)) ` a = b(a) : Q"
1.93 +axiomatization where
1.94 +applyB: "[| a:P; !!x. x:P ==> b(x) : Q |] ==> (lam x. b(x)) ` a = b(a) : Q" and
1.95 funEC: "f:P ==> f = lam x. f`x : P"
1.96
1.97 +axiomatization where
1.98 specB: "[| !!x. f(x) : P(x) |] ==> (all x. f(x)) ^ a = f(a) : P(a)"
1.99
1.100
1.101 (**** Definitions ****)
1.102
1.103 +defs
1.104 not_def: "~P == P-->False"
1.105 iff_def: "P<->Q == (P-->Q) & (Q-->P)"
1.106
1.107 @@ -152,7 +165,8 @@
1.108 ex1_def: "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)"
1.109
1.110 (*Rewriting -- special constants to flag normalized terms and formulae*)
1.111 -norm_eq: "nrm : norm(x) = x"
1.112 +axiomatization where
1.113 +norm_eq: "nrm : norm(x) = x" and
1.114 NORM_iff: "NRM : NORM(P) <-> P"
1.115
1.116 (*** Sequent-style elimination rules for & --> and ALL ***)
2.1 --- a/src/FOLP/ex/Nat.thy Thu Feb 28 13:33:01 2013 +0100
2.2 +++ b/src/FOLP/ex/Nat.thy Thu Feb 28 13:46:45 2013 +0100
2.3 @@ -12,34 +12,30 @@
2.4 typedecl nat
2.5 arities nat :: "term"
2.6
2.7 -consts
2.8 - Zero :: nat ("0")
2.9 - Suc :: "nat => nat"
2.10 - rec :: "[nat, 'a, [nat, 'a] => 'a] => 'a"
2.11 - add :: "[nat, nat] => nat" (infixl "+" 60)
2.12 +axiomatization
2.13 + Zero :: nat ("0") and
2.14 + Suc :: "nat => nat" and
2.15 + rec :: "[nat, 'a, [nat, 'a] => 'a] => 'a" and
2.16
2.17 (*Proof terms*)
2.18 - nrec :: "[nat, p, [nat, p] => p] => p"
2.19 - ninj :: "p => p"
2.20 - nneq :: "p => p"
2.21 - rec0 :: "p"
2.22 + nrec :: "[nat, p, [nat, p] => p] => p" and
2.23 + ninj :: "p => p" and
2.24 + nneq :: "p => p" and
2.25 + rec0 :: "p" and
2.26 recSuc :: "p"
2.27 +where
2.28 + induct: "[| b:P(0); !!x u. u:P(x) ==> c(x,u):P(Suc(x))
2.29 + |] ==> nrec(n,b,c):P(n)" and
2.30
2.31 -axioms
2.32 - induct: "[| b:P(0); !!x u. u:P(x) ==> c(x,u):P(Suc(x))
2.33 - |] ==> nrec(n,b,c):P(n)"
2.34 + Suc_inject: "p:Suc(m)=Suc(n) ==> ninj(p) : m=n" and
2.35 + Suc_neq_0: "p:Suc(m)=0 ==> nneq(p) : R" and
2.36 + rec_0: "rec0 : rec(0,a,f) = a" and
2.37 + rec_Suc: "recSuc : rec(Suc(m), a, f) = f(m, rec(m,a,f))" and
2.38 + nrecB0: "b: A ==> nrec(0,b,c) = b : A" and
2.39 + nrecBSuc: "c(n,nrec(n,b,c)) : A ==> nrec(Suc(n),b,c) = c(n,nrec(n,b,c)) : A"
2.40
2.41 - Suc_inject: "p:Suc(m)=Suc(n) ==> ninj(p) : m=n"
2.42 - Suc_neq_0: "p:Suc(m)=0 ==> nneq(p) : R"
2.43 - rec_0: "rec0 : rec(0,a,f) = a"
2.44 - rec_Suc: "recSuc : rec(Suc(m), a, f) = f(m, rec(m,a,f))"
2.45 -
2.46 -defs
2.47 - add_def: "m+n == rec(m, n, %x y. Suc(y))"
2.48 -
2.49 -axioms
2.50 - nrecB0: "b: A ==> nrec(0,b,c) = b : A"
2.51 - nrecBSuc: "c(n,nrec(n,b,c)) : A ==> nrec(Suc(n),b,c) = c(n,nrec(n,b,c)) : A"
2.52 +definition add :: "[nat, nat] => nat" (infixl "+" 60)
2.53 + where "m + n == rec(m, n, %x y. Suc(y))"
2.54
2.55
2.56 subsection {* Proofs about the natural numbers *}