1268

1 
(* Title: FOL/IFOL.thy

35

2 
ID: $Id$

79

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory

35

4 
Copyright 1993 University of Cambridge


5 

2205

6 
Intuitionistic firstorder logic.

35

7 
*)


8 

79

9 
IFOL = Pure +

0

10 

3906

11 
global


12 

79

13 
classes


14 
term < logic


15 


16 
default


17 
term

0

18 

79

19 
types

278

20 
o

0

21 

79

22 
arities


23 
o :: logic

0

24 

79

25 


26 
consts

0

27 

1322

28 
Trueprop :: o => prop ("(_)" 5)


29 
True, False :: o

79

30 


31 
(* Connectives *)


32 

1322

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

35

34 

1322

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


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


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


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


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

79

40 


41 
(* Quantifiers *)


42 

1322

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


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


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

79

46 

0

47 

2257

48 

928

49 
syntax

1322

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

928

51 

35

52 
translations

79

53 
"x ~= y" == "~ (x = y)"


54 

2257

55 
syntax (symbols)


56 
Not :: o => o ("\\<not> _" [40] 40)


57 
"op &" :: [o, o] => o (infixr "\\<and>" 35)


58 
"op " :: [o, o] => o (infixr "\\<or>" 30)


59 
"op >" :: [o, o] => o (infixr "\\<midarrow>\\<rightarrow>" 25)


60 
"op <>" :: [o, o] => o (infixr "\\<leftarrow>\\<rightarrow>" 25)

2367

61 
"ALL " :: [idts, o] => o ("(3\\<forall>_./ _)" [0, 10] 10)


62 
"EX " :: [idts, o] => o ("(3\\<exists>_./ _)" [0, 10] 10)


63 
"EX! " :: [idts, o] => o ("(3\\<exists>!_./ _)" [0, 10] 10)

2257

64 
"op ~=" :: ['a, 'a] => o (infixl "\\<noteq>" 50)

2205

65 

35

66 

3906

67 
path IFOL


68 

0

69 
rules


70 

79

71 
(* Equality *)

0

72 

79

73 
refl "a=a"


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

0

75 

79

76 
(* Propositional logic *)

0

77 

79

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


79 
conjunct1 "P&Q ==> P"


80 
conjunct2 "P&Q ==> Q"

0

81 

79

82 
disjI1 "P ==> PQ"


83 
disjI2 "Q ==> PQ"


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

0

85 

79

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


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

0

88 

79

89 
FalseE "False ==> P"

0

90 

79

91 
(* Definitions *)

0

92 

79

93 
True_def "True == False>False"


94 
not_def "~P == P>False"


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


96 


97 
(* Unique existence *)

0

98 

79

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

0

100 

79

101 
(* Quantifiers *)

0

102 

3835

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


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

0

105 

3835

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


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

0

108 


109 
(* Reflection *)


110 

79

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


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

0

113 


114 
end
