src/FOLP/IFOLP.thy
changeset 0 a5a9c433f639
child 283 76caebd18756
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/FOLP/IFOLP.thy	Thu Sep 16 12:20:38 1993 +0200
     1.3 @@ -0,0 +1,141 @@
     1.4 +IFOLP = Pure +
     1.5 +
     1.6 +classes term < logic
     1.7 +
     1.8 +default term
     1.9 +
    1.10 +types p,o 0
    1.11 +
    1.12 +arities p,o :: logic
    1.13 +
    1.14 +consts	
    1.15 +      (*** Judgements ***)
    1.16 + "@Proof"   	::   "[p,o]=>prop"	("(_ /: _)" [10,10] 5)
    1.17 + Proof  	::   "[o,p]=>prop"
    1.18 + EqProof        ::   "[p,p,o]=>prop"    ("(3_ /= _ :/ _)" [10,10,10] 5)
    1.19 +        
    1.20 +      (*** Logical Connectives -- Type Formers ***)
    1.21 + "="		::	"['a,'a] => o"	(infixl 50)
    1.22 + True,False	::	"o"
    1.23 + "Not"		::	"o => o"	("~ _" [40] 40)
    1.24 + "&"		::	"[o,o] => o"	(infixr 35)
    1.25 + "|"		::	"[o,o] => o"	(infixr 30)
    1.26 + "-->"		::	"[o,o] => o"	(infixr 25)
    1.27 + "<->"		::	"[o,o] => o"	(infixr 25)
    1.28 +      (*Quantifiers*)
    1.29 + All		::	"('a => o) => o"	(binder "ALL " 10)
    1.30 + Ex		::	"('a => o) => o"	(binder "EX " 10)
    1.31 + Ex1		::	"('a => o) => o"	(binder "EX! " 10)
    1.32 +      (*Rewriting gadgets*)
    1.33 + NORM		::	"o => o"
    1.34 + norm		::	"'a => 'a"
    1.35 +
    1.36 +      (*** Proof Term Formers ***)
    1.37 + tt		:: "p"
    1.38 + contr		:: "p=>p"
    1.39 + fst,snd	:: "p=>p"
    1.40 + pair		:: "[p,p]=>p"		("(1<_,/_>)")
    1.41 + split		:: "[p, [p,p]=>p] =>p"
    1.42 + inl,inr	:: "p=>p"
    1.43 + when		:: "[p, p=>p, p=>p]=>p"
    1.44 + lambda		:: "(p => p) => p"	(binder "lam " 20)
    1.45 + "`"		:: "[p,p]=>p"		(infixl 60)
    1.46 + alll           :: "['a=>p]=>p"         (binder "all " 15)
    1.47 + "^"            :: "[p,'a]=>p"          (infixl 50)
    1.48 + exists		:: "['a,p]=>p"		("(1[_,/_])")
    1.49 + xsplit         :: "[p,['a,p]=>p]=>p"
    1.50 + ideq           :: "'a=>p"
    1.51 + idpeel         :: "[p,'a=>p]=>p"
    1.52 + nrm, NRM       :: "p"
    1.53 +
    1.54 +rules
    1.55 +
    1.56 +(**** Propositional logic ****)
    1.57 +
    1.58 +(*Equality*)
    1.59 +(* Like Intensional Equality in MLTT - but proofs distinct from terms *)
    1.60 +
    1.61 +ieqI	  "ideq(a) : a=a"
    1.62 +ieqE      "[| p : a=b;  !!x.f(x) : P(x,x) |] ==> idpeel(p,f) : P(a,b)"
    1.63 +
    1.64 +(* Truth and Falsity *)
    1.65 +
    1.66 +TrueI     "tt : True"
    1.67 +FalseE    "a:False ==> contr(a):P"
    1.68 +
    1.69 +(* Conjunction *)
    1.70 +
    1.71 +conjI     "[| a:P;  b:Q |] ==> <a,b> : P&Q"
    1.72 +conjunct1 "p:P&Q ==> fst(p):P"
    1.73 +conjunct2 "p:P&Q ==> snd(p):Q"
    1.74 +
    1.75 +(* Disjunction *)
    1.76 +
    1.77 +disjI1    "a:P ==> inl(a):P|Q"
    1.78 +disjI2    "b:Q ==> inr(b):P|Q"
    1.79 +disjE     "[| a:P|Q;  !!x.x:P ==> f(x):R;  !!x.x:Q ==> g(x):R \
    1.80 +\          |] ==> when(a,f,g):R"
    1.81 +
    1.82 +(* Implication *)
    1.83 +
    1.84 +impI      "(!!x.x:P ==> f(x):Q) ==> lam x.f(x):P-->Q"
    1.85 +mp        "[| f:P-->Q;  a:P |] ==> f`a:Q"
    1.86 +
    1.87 +(*Quantifiers*)
    1.88 +
    1.89 +allI	  "(!!x. f(x) : P(x)) ==> all x.f(x) : ALL x.P(x)"
    1.90 +spec	  "(f:ALL x.P(x)) ==> f^x : P(x)"
    1.91 +
    1.92 +exI	  "p : P(x) ==> [x,p] : EX x.P(x)"
    1.93 +exE	  "[| p: EX x.P(x);  !!x u. u:P(x) ==> f(x,u) : R |] ==> xsplit(p,f):R"
    1.94 +
    1.95 +(**** Equality between proofs ****)
    1.96 +
    1.97 +prefl     "a : P ==> a = a : P"
    1.98 +psym      "a = b : P ==> b = a : P"
    1.99 +ptrans    "[| a = b : P;  b = c : P |] ==> a = c : P"
   1.100 +
   1.101 +idpeelB   "[| !!x.f(x) : P(x,x) |] ==> idpeel(ideq(a),f) = f(a) : P(a,a)"
   1.102 +
   1.103 +fstB      "a:P ==> fst(<a,b>) = a : P"
   1.104 +sndB      "b:Q ==> snd(<a,b>) = b : Q"
   1.105 +pairEC    "p:P&Q ==> p = <fst(p),snd(p)> : P&Q"
   1.106 +
   1.107 +whenBinl  "[| a:P;  !!x.x:P ==> f(x) : Q |] ==> when(inl(a),f,g) = f(a) : Q"
   1.108 +whenBinr  "[| b:P;  !!x.x:P ==> g(x) : Q |] ==> when(inr(b),f,g) = g(b) : Q"
   1.109 +plusEC    "a:P|Q ==> when(a,%x.inl(x),%y.inr(y)) = p : P|Q"
   1.110 +
   1.111 +applyB     "[| a:P;  !!x.x:P ==> b(x) : Q |] ==> (lam x.b(x)) ` a = b(a) : Q"
   1.112 +funEC      "f:P ==> f = lam x.f`x : P"
   1.113 +
   1.114 +specB      "[| !!x.f(x) : P(x) |] ==> (all x.f(x)) ^ a = f(a) : P(a)"
   1.115 +
   1.116 +
   1.117 +(**** Definitions ****)
   1.118 +
   1.119 +not_def 	     "~P == P-->False"
   1.120 +iff_def         "P<->Q == (P-->Q) & (Q-->P)"
   1.121 +
   1.122 +(*Unique existence*)
   1.123 +ex1_def   "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)"
   1.124 +
   1.125 +(*Rewriting -- special constants to flag normalized terms and formulae*)
   1.126 +norm_eq	"nrm : norm(x) = x"
   1.127 +NORM_iff	"NRM : NORM(P) <-> P"
   1.128 +
   1.129 +end
   1.130 +
   1.131 +ML
   1.132 +
   1.133 +(*show_proofs:=true displays the proof terms -- they are ENORMOUS*)
   1.134 +val show_proofs = ref false;
   1.135 +
   1.136 +fun proof_tr [p,P] = Const("Proof",dummyT) $ P $ p;
   1.137 +
   1.138 +fun proof_tr' [P,p] = 
   1.139 +    if !show_proofs then Const("@Proof",dummyT) $ p $ P 
   1.140 +    else P  (*this case discards the proof term*);
   1.141 +
   1.142 +val  parse_translation = [("@Proof", proof_tr)];
   1.143 +val print_translation  = [("Proof", proof_tr')];
   1.144 +