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 ***)