src/FOLP/IFOLP.thy
changeset 0 a5a9c433f639
child 283 76caebd18756
equal deleted inserted replaced
-1:000000000000 0:a5a9c433f639
       
     1 IFOLP = Pure +
       
     2 
       
     3 classes term < logic
       
     4 
       
     5 default term
       
     6 
       
     7 types p,o 0
       
     8 
       
     9 arities p,o :: logic
       
    10 
       
    11 consts	
       
    12       (*** Judgements ***)
       
    13  "@Proof"   	::   "[p,o]=>prop"	("(_ /: _)" [10,10] 5)
       
    14  Proof  	::   "[o,p]=>prop"
       
    15  EqProof        ::   "[p,p,o]=>prop"    ("(3_ /= _ :/ _)" [10,10,10] 5)
       
    16         
       
    17       (*** Logical Connectives -- Type Formers ***)
       
    18  "="		::	"['a,'a] => o"	(infixl 50)
       
    19  True,False	::	"o"
       
    20  "Not"		::	"o => o"	("~ _" [40] 40)
       
    21  "&"		::	"[o,o] => o"	(infixr 35)
       
    22  "|"		::	"[o,o] => o"	(infixr 30)
       
    23  "-->"		::	"[o,o] => o"	(infixr 25)
       
    24  "<->"		::	"[o,o] => o"	(infixr 25)
       
    25       (*Quantifiers*)
       
    26  All		::	"('a => o) => o"	(binder "ALL " 10)
       
    27  Ex		::	"('a => o) => o"	(binder "EX " 10)
       
    28  Ex1		::	"('a => o) => o"	(binder "EX! " 10)
       
    29       (*Rewriting gadgets*)
       
    30  NORM		::	"o => o"
       
    31  norm		::	"'a => 'a"
       
    32 
       
    33       (*** Proof Term Formers ***)
       
    34  tt		:: "p"
       
    35  contr		:: "p=>p"
       
    36  fst,snd	:: "p=>p"
       
    37  pair		:: "[p,p]=>p"		("(1<_,/_>)")
       
    38  split		:: "[p, [p,p]=>p] =>p"
       
    39  inl,inr	:: "p=>p"
       
    40  when		:: "[p, p=>p, p=>p]=>p"
       
    41  lambda		:: "(p => p) => p"	(binder "lam " 20)
       
    42  "`"		:: "[p,p]=>p"		(infixl 60)
       
    43  alll           :: "['a=>p]=>p"         (binder "all " 15)
       
    44  "^"            :: "[p,'a]=>p"          (infixl 50)
       
    45  exists		:: "['a,p]=>p"		("(1[_,/_])")
       
    46  xsplit         :: "[p,['a,p]=>p]=>p"
       
    47  ideq           :: "'a=>p"
       
    48  idpeel         :: "[p,'a=>p]=>p"
       
    49  nrm, NRM       :: "p"
       
    50 
       
    51 rules
       
    52 
       
    53 (**** Propositional logic ****)
       
    54 
       
    55 (*Equality*)
       
    56 (* Like Intensional Equality in MLTT - but proofs distinct from terms *)
       
    57 
       
    58 ieqI	  "ideq(a) : a=a"
       
    59 ieqE      "[| p : a=b;  !!x.f(x) : P(x,x) |] ==> idpeel(p,f) : P(a,b)"
       
    60 
       
    61 (* Truth and Falsity *)
       
    62 
       
    63 TrueI     "tt : True"
       
    64 FalseE    "a:False ==> contr(a):P"
       
    65 
       
    66 (* Conjunction *)
       
    67 
       
    68 conjI     "[| a:P;  b:Q |] ==> <a,b> : P&Q"
       
    69 conjunct1 "p:P&Q ==> fst(p):P"
       
    70 conjunct2 "p:P&Q ==> snd(p):Q"
       
    71 
       
    72 (* Disjunction *)
       
    73 
       
    74 disjI1    "a:P ==> inl(a):P|Q"
       
    75 disjI2    "b:Q ==> inr(b):P|Q"
       
    76 disjE     "[| a:P|Q;  !!x.x:P ==> f(x):R;  !!x.x:Q ==> g(x):R \
       
    77 \          |] ==> when(a,f,g):R"
       
    78 
       
    79 (* Implication *)
       
    80 
       
    81 impI      "(!!x.x:P ==> f(x):Q) ==> lam x.f(x):P-->Q"
       
    82 mp        "[| f:P-->Q;  a:P |] ==> f`a:Q"
       
    83 
       
    84 (*Quantifiers*)
       
    85 
       
    86 allI	  "(!!x. f(x) : P(x)) ==> all x.f(x) : ALL x.P(x)"
       
    87 spec	  "(f:ALL x.P(x)) ==> f^x : P(x)"
       
    88 
       
    89 exI	  "p : P(x) ==> [x,p] : EX x.P(x)"
       
    90 exE	  "[| p: EX x.P(x);  !!x u. u:P(x) ==> f(x,u) : R |] ==> xsplit(p,f):R"
       
    91 
       
    92 (**** Equality between proofs ****)
       
    93 
       
    94 prefl     "a : P ==> a = a : P"
       
    95 psym      "a = b : P ==> b = a : P"
       
    96 ptrans    "[| a = b : P;  b = c : P |] ==> a = c : P"
       
    97 
       
    98 idpeelB   "[| !!x.f(x) : P(x,x) |] ==> idpeel(ideq(a),f) = f(a) : P(a,a)"
       
    99 
       
   100 fstB      "a:P ==> fst(<a,b>) = a : P"
       
   101 sndB      "b:Q ==> snd(<a,b>) = b : Q"
       
   102 pairEC    "p:P&Q ==> p = <fst(p),snd(p)> : P&Q"
       
   103 
       
   104 whenBinl  "[| a:P;  !!x.x:P ==> f(x) : Q |] ==> when(inl(a),f,g) = f(a) : Q"
       
   105 whenBinr  "[| b:P;  !!x.x:P ==> g(x) : Q |] ==> when(inr(b),f,g) = g(b) : Q"
       
   106 plusEC    "a:P|Q ==> when(a,%x.inl(x),%y.inr(y)) = p : P|Q"
       
   107 
       
   108 applyB     "[| a:P;  !!x.x:P ==> b(x) : Q |] ==> (lam x.b(x)) ` a = b(a) : Q"
       
   109 funEC      "f:P ==> f = lam x.f`x : P"
       
   110 
       
   111 specB      "[| !!x.f(x) : P(x) |] ==> (all x.f(x)) ^ a = f(a) : P(a)"
       
   112 
       
   113 
       
   114 (**** Definitions ****)
       
   115 
       
   116 not_def 	     "~P == P-->False"
       
   117 iff_def         "P<->Q == (P-->Q) & (Q-->P)"
       
   118 
       
   119 (*Unique existence*)
       
   120 ex1_def   "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)"
       
   121 
       
   122 (*Rewriting -- special constants to flag normalized terms and formulae*)
       
   123 norm_eq	"nrm : norm(x) = x"
       
   124 NORM_iff	"NRM : NORM(P) <-> P"
       
   125 
       
   126 end
       
   127 
       
   128 ML
       
   129 
       
   130 (*show_proofs:=true displays the proof terms -- they are ENORMOUS*)
       
   131 val show_proofs = ref false;
       
   132 
       
   133 fun proof_tr [p,P] = Const("Proof",dummyT) $ P $ p;
       
   134 
       
   135 fun proof_tr' [P,p] = 
       
   136     if !show_proofs then Const("@Proof",dummyT) $ p $ P 
       
   137     else P  (*this case discards the proof term*);
       
   138 
       
   139 val  parse_translation = [("@Proof", proof_tr)];
       
   140 val print_translation  = [("Proof", proof_tr')];
       
   141