35

1 
(* Title: FOL/ifol.thy


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1993 University of Cambridge


5 


6 
Intuitionistic firstorder logic


7 
*)


8 

0

9 
IFOL = Pure +


10 


11 
classes term < logic


12 


13 
default term


14 


15 
types o 0


16 


17 
arities o :: logic


18 


19 
consts


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

35

21 
True, False :: "o"

0

22 
(*Connectives*)

35

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


24 

0

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


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


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


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


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

35

30 

0

31 
(*Quantifiers*)


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


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


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


35 

35

36 
translations


37 
"x ~= y" == "~ (x=y)"


38 

0

39 
rules


40 


41 
(*Equality*)


42 


43 
refl "a=a"


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


45 


46 
(*Propositional logic*)


47 


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


49 
conjunct1 "P&Q ==> P"


50 
conjunct2 "P&Q ==> Q"


51 


52 
disjI1 "P ==> PQ"


53 
disjI2 "Q ==> PQ"


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


55 


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


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


58 


59 
FalseE "False ==> P"


60 


61 
(*Definitions*)


62 

35

63 
True_def "True == False>False"


64 
not_def "~P == P>False"

0

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


66 


67 
(*Unique existence*)


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


69 


70 
(*Quantifiers*)


71 


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


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


74 


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


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


77 


78 
(* Reflection *)


79 


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


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


82 


83 
end
