0

1 
IFOLP = Pure +


2 


3 
classes term < logic


4 


5 
default term


6 

283

7 
types


8 
p


9 
o

0

10 

283

11 
arities


12 
p,o :: logic

0

13 


14 
consts


15 
(*** Judgements ***)


16 
"@Proof" :: "[p,o]=>prop" ("(_ /: _)" [10,10] 5)


17 
Proof :: "[o,p]=>prop"


18 
EqProof :: "[p,p,o]=>prop" ("(3_ /= _ :/ _)" [10,10,10] 5)


19 


20 
(*** Logical Connectives  Type Formers ***)


21 
"=" :: "['a,'a] => o" (infixl 50)


22 
True,False :: "o"


23 
"Not" :: "o => o" ("~ _" [40] 40)


24 
"&" :: "[o,o] => o" (infixr 35)


25 
"" :: "[o,o] => o" (infixr 30)


26 
">" :: "[o,o] => o" (infixr 25)


27 
"<>" :: "[o,o] => o" (infixr 25)


28 
(*Quantifiers*)


29 
All :: "('a => o) => o" (binder "ALL " 10)


30 
Ex :: "('a => o) => o" (binder "EX " 10)


31 
Ex1 :: "('a => o) => o" (binder "EX! " 10)


32 
(*Rewriting gadgets*)


33 
NORM :: "o => o"


34 
norm :: "'a => 'a"


35 


36 
(*** Proof Term Formers ***)


37 
tt :: "p"


38 
contr :: "p=>p"


39 
fst,snd :: "p=>p"


40 
pair :: "[p,p]=>p" ("(1<_,/_>)")


41 
split :: "[p, [p,p]=>p] =>p"


42 
inl,inr :: "p=>p"


43 
when :: "[p, p=>p, p=>p]=>p"


44 
lambda :: "(p => p) => p" (binder "lam " 20)


45 
"`" :: "[p,p]=>p" (infixl 60)


46 
alll :: "['a=>p]=>p" (binder "all " 15)


47 
"^" :: "[p,'a]=>p" (infixl 50)


48 
exists :: "['a,p]=>p" ("(1[_,/_])")


49 
xsplit :: "[p,['a,p]=>p]=>p"


50 
ideq :: "'a=>p"


51 
idpeel :: "[p,'a=>p]=>p"


52 
nrm, NRM :: "p"


53 


54 
rules


55 


56 
(**** Propositional logic ****)


57 


58 
(*Equality*)


59 
(* Like Intensional Equality in MLTT  but proofs distinct from terms *)


60 


61 
ieqI "ideq(a) : a=a"


62 
ieqE "[ p : a=b; !!x.f(x) : P(x,x) ] ==> idpeel(p,f) : P(a,b)"


63 


64 
(* Truth and Falsity *)


65 


66 
TrueI "tt : True"


67 
FalseE "a:False ==> contr(a):P"


68 


69 
(* Conjunction *)


70 


71 
conjI "[ a:P; b:Q ] ==> <a,b> : P&Q"


72 
conjunct1 "p:P&Q ==> fst(p):P"


73 
conjunct2 "p:P&Q ==> snd(p):Q"


74 


75 
(* Disjunction *)


76 


77 
disjI1 "a:P ==> inl(a):PQ"


78 
disjI2 "b:Q ==> inr(b):PQ"


79 
disjE "[ a:PQ; !!x.x:P ==> f(x):R; !!x.x:Q ==> g(x):R \


80 
\ ] ==> when(a,f,g):R"


81 


82 
(* Implication *)


83 


84 
impI "(!!x.x:P ==> f(x):Q) ==> lam x.f(x):P>Q"


85 
mp "[ f:P>Q; a:P ] ==> f`a:Q"


86 


87 
(*Quantifiers*)


88 


89 
allI "(!!x. f(x) : P(x)) ==> all x.f(x) : ALL x.P(x)"


90 
spec "(f:ALL x.P(x)) ==> f^x : P(x)"


91 


92 
exI "p : P(x) ==> [x,p] : EX x.P(x)"


93 
exE "[ p: EX x.P(x); !!x u. u:P(x) ==> f(x,u) : R ] ==> xsplit(p,f):R"


94 


95 
(**** Equality between proofs ****)


96 


97 
prefl "a : P ==> a = a : P"


98 
psym "a = b : P ==> b = a : P"


99 
ptrans "[ a = b : P; b = c : P ] ==> a = c : P"


100 


101 
idpeelB "[ !!x.f(x) : P(x,x) ] ==> idpeel(ideq(a),f) = f(a) : P(a,a)"


102 


103 
fstB "a:P ==> fst(<a,b>) = a : P"


104 
sndB "b:Q ==> snd(<a,b>) = b : Q"


105 
pairEC "p:P&Q ==> p = <fst(p),snd(p)> : P&Q"


106 


107 
whenBinl "[ a:P; !!x.x:P ==> f(x) : Q ] ==> when(inl(a),f,g) = f(a) : Q"


108 
whenBinr "[ b:P; !!x.x:P ==> g(x) : Q ] ==> when(inr(b),f,g) = g(b) : Q"


109 
plusEC "a:PQ ==> when(a,%x.inl(x),%y.inr(y)) = p : PQ"


110 


111 
applyB "[ a:P; !!x.x:P ==> b(x) : Q ] ==> (lam x.b(x)) ` a = b(a) : Q"


112 
funEC "f:P ==> f = lam x.f`x : P"


113 


114 
specB "[ !!x.f(x) : P(x) ] ==> (all x.f(x)) ^ a = f(a) : P(a)"


115 


116 


117 
(**** Definitions ****)


118 


119 
not_def "~P == P>False"


120 
iff_def "P<>Q == (P>Q) & (Q>P)"


121 


122 
(*Unique existence*)


123 
ex1_def "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) > y=x)"


124 


125 
(*Rewriting  special constants to flag normalized terms and formulae*)


126 
norm_eq "nrm : norm(x) = x"


127 
NORM_iff "NRM : NORM(P) <> P"


128 


129 
end


130 


131 
ML


132 


133 
(*show_proofs:=true displays the proof terms  they are ENORMOUS*)


134 
val show_proofs = ref false;


135 


136 
fun proof_tr [p,P] = Const("Proof",dummyT) $ P $ p;


137 


138 
fun proof_tr' [P,p] =


139 
if !show_proofs then Const("@Proof",dummyT) $ p $ P


140 
else P (*this case discards the proof term*);


141 


142 
val parse_translation = [("@Proof", proof_tr)];


143 
val print_translation = [("Proof", proof_tr')];


144 
