0

1 
IFOL = Pure +


2 


3 
classes term < logic


4 


5 
default term


6 


7 
types o 0


8 


9 
arities o :: logic


10 


11 
consts


12 
Trueprop :: "o => prop" ("(_)" [0] 5)


13 
True,False :: "o"


14 
(*Connectives*)


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


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


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


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


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


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


21 
(*Quantifiers*)


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


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


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


25 


26 
rules


27 


28 
(*Equality*)


29 


30 
refl "a=a"


31 
subst "[ a=b; P(a) ] ==> P(b)"


32 


33 
(*Propositional logic*)


34 


35 
conjI "[ P; Q ] ==> P&Q"


36 
conjunct1 "P&Q ==> P"


37 
conjunct2 "P&Q ==> Q"


38 


39 
disjI1 "P ==> PQ"


40 
disjI2 "Q ==> PQ"


41 
disjE "[ PQ; P ==> R; Q ==> R ] ==> R"


42 


43 
impI "(P ==> Q) ==> P>Q"


44 
mp "[ P>Q; P ] ==> Q"


45 


46 
FalseE "False ==> P"


47 


48 
(*Definitions*)


49 


50 
True_def "True == False>False"


51 
not_def "~P == P>False"


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


53 


54 
(*Unique existence*)


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


56 


57 
(*Quantifiers*)


58 


59 
allI "(!!x. P(x)) ==> (ALL x.P(x))"


60 
spec "(ALL x.P(x)) ==> P(x)"


61 


62 
exI "P(x) ==> (EX x.P(x))"


63 
exE "[ EX x.P(x); !!x. P(x) ==> R ] ==> R"


64 


65 
(* Reflection *)


66 


67 
eq_reflection "(x=y) ==> (x==y)"


68 
iff_reflection "(P<>Q) ==> (P==Q)"


69 


70 
end
