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