src/FOLP/IFOLP.thy
 changeset 51306 f0e5af7aa68b parent 48891 c0eafbd55de3 child 52143 36ffe23b25f8
```     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 ***)
```