0

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):PQ"


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


76 
disjE "[ a:PQ; !!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:PQ ==> when(a,%x.inl(x),%y.inr(y)) = p : PQ"


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 
