author  wenzelm 
Sun, 28 Oct 2001 21:10:47 +0100  
changeset 11976  075df6e46cef 
parent 11953  f98623fdf6ef 
child 12019  abe9b7c6016e 
permissions  rwrr 
1268  1 
(* Title: FOL/IFOL.thy 
35  2 
ID: $Id$ 
11677  3 
Author: Lawrence C Paulson and Markus Wenzel 
4 
*) 

35  5 

11677  6 
header {* Intuitionistic firstorder logic *} 
35  7 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

8 
theory IFOL = Pure 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

9 
files ("IFOL_lemmas.ML") ("fologic.ML") ("hypsubstdata.ML") ("intprover.ML"): 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

10 

0  11 

11677  12 
subsection {* Syntax and axiomatic basis *} 
13 

3906  14 
global 
15 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

16 
classes "term" < logic 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

17 
defaultsort "term" 
0  18 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

19 
typedecl o 
79  20 

11747  21 
judgment 
22 
Trueprop :: "o => prop" ("(_)" 5) 

0  23 

11747  24 
consts 
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

25 
True :: o 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

26 
False :: o 
79  27 

28 
(* Connectives *) 

29 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

30 
"=" :: "['a, 'a] => o" (infixl 50) 
35  31 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

32 
Not :: "o => o" ("~ _" [40] 40) 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

33 
& :: "[o, o] => o" (infixr 35) 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

34 
"" :: "[o, o] => o" (infixr 30) 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

35 
> :: "[o, o] => o" (infixr 25) 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

36 
<> :: "[o, o] => o" (infixr 25) 
79  37 

38 
(* Quantifiers *) 

39 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

40 
All :: "('a => o) => o" (binder "ALL " 10) 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

41 
Ex :: "('a => o) => o" (binder "EX " 10) 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

42 
Ex1 :: "('a => o) => o" (binder "EX! " 10) 
79  43 

0  44 

928  45 
syntax 
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

46 
"~=" :: "['a, 'a] => o" (infixl 50) 
35  47 
translations 
79  48 
"x ~= y" == "~ (x = y)" 
49 

2257  50 
syntax (symbols) 
11677  51 
Not :: "o => o" ("\<not> _" [40] 40) 
52 
"op &" :: "[o, o] => o" (infixr "\<and>" 35) 

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

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

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

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

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

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

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

2205  60 

6027
9dd06eeda95c
added new print_mode "xsymbols" for extended symbol support
oheimb
parents:
4854
diff
changeset

61 
syntax (xsymbols) 
11677  62 
"op >" :: "[o, o] => o" (infixr "\<longrightarrow>" 25) 
63 
"op <>" :: "[o, o] => o" (infixr "\<longleftrightarrow>" 25) 

35  64 

6340  65 
syntax (HTML output) 
11677  66 
Not :: "o => o" ("\<not> _" [40] 40) 
6340  67 

68 

3932  69 
local 
3906  70 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

71 
axioms 
0  72 

79  73 
(* Equality *) 
0  74 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

75 
refl: "a=a" 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

76 
subst: "[ a=b; P(a) ] ==> P(b)" 
0  77 

79  78 
(* Propositional logic *) 
0  79 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

80 
conjI: "[ P; Q ] ==> P&Q" 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

81 
conjunct1: "P&Q ==> P" 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

82 
conjunct2: "P&Q ==> Q" 
0  83 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

84 
disjI1: "P ==> PQ" 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

85 
disjI2: "Q ==> PQ" 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

86 
disjE: "[ PQ; P ==> R; Q ==> R ] ==> R" 
0  87 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

88 
impI: "(P ==> Q) ==> P>Q" 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

89 
mp: "[ P>Q; P ] ==> Q" 
0  90 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

91 
FalseE: "False ==> P" 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

92 

0  93 

79  94 
(* Definitions *) 
0  95 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

96 
True_def: "True == False>False" 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

97 
not_def: "~P == P>False" 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

98 
iff_def: "P<>Q == (P>Q) & (Q>P)" 
79  99 

100 
(* Unique existence *) 

0  101 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

102 
ex1_def: "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) > y=x)" 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

103 

0  104 

79  105 
(* Quantifiers *) 
0  106 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

107 
allI: "(!!x. P(x)) ==> (ALL x. P(x))" 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

108 
spec: "(ALL x. P(x)) ==> P(x)" 
0  109 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

110 
exI: "P(x) ==> (EX x. P(x))" 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

111 
exE: "[ EX x. P(x); !!x. P(x) ==> R ] ==> R" 
0  112 

113 
(* Reflection *) 

114 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

115 
eq_reflection: "(x=y) ==> (x==y)" 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

116 
iff_reflection: "(P<>Q) ==> (P==Q)" 
0  117 

4092  118 

11677  119 
subsection {* Lemmas and proof tools *} 
120 

9886  121 
setup Simplifier.setup 
122 
use "IFOL_lemmas.ML" 

11734  123 

124 
declare impE [Pure.elim] iffD1 [Pure.elim] iffD2 [Pure.elim] 

125 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

126 
use "fologic.ML" 
9886  127 
use "hypsubstdata.ML" 
128 
setup hypsubst_setup 

7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

129 
use "intprover.ML" 
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

130 

4092  131 

11677  132 
subsection {* Atomizing metalevel rules *} 
133 

11747  134 
lemma atomize_all [atomize]: "(!!x. P(x)) == Trueprop (ALL x. P(x))" 
11976  135 
proof 
11677  136 
assume "!!x. P(x)" 
137 
show "ALL x. P(x)" by (rule allI) 

138 
next 

139 
assume "ALL x. P(x)" 

140 
thus "!!x. P(x)" by (rule allE) 

141 
qed 

142 

11747  143 
lemma atomize_imp [atomize]: "(A ==> B) == Trueprop (A > B)" 
11976  144 
proof 
11677  145 
assume r: "A ==> B" 
146 
show "A > B" by (rule impI) (rule r) 

147 
next 

148 
assume "A > B" and A 

149 
thus B by (rule mp) 

150 
qed 

151 

11747  152 
lemma atomize_eq [atomize]: "(x == y) == Trueprop (x = y)" 
11976  153 
proof 
11677  154 
assume "x == y" 
155 
show "x = y" by (unfold prems) (rule refl) 

156 
next 

157 
assume "x = y" 

158 
thus "x == y" by (rule eq_reflection) 

159 
qed 

160 

11953  161 
lemma atomize_conj [atomize]: "(!!C. (A ==> B ==> PROP C) ==> PROP C) == Trueprop (A & B)" 
11976  162 
proof 
11953  163 
assume "!!C. (A ==> B ==> PROP C) ==> PROP C" 
164 
show "A & B" by (rule conjI) 

165 
next 

166 
fix C 

167 
assume "A & B" 

168 
assume "A ==> B ==> PROP C" 

169 
thus "PROP C" 

170 
proof this 

171 
show A by (rule conjunct1) 

172 
show B by (rule conjunct2) 

173 
qed 

174 
qed 

175 

11771  176 
declare atomize_all [symmetric, rulify] atomize_imp [symmetric, rulify] 
177 

11848  178 

179 
subsection {* Calculational rules *} 

180 

181 
lemma forw_subst: "a = b ==> P(b) ==> P(a)" 

182 
by (rule ssubst) 

183 

184 
lemma back_subst: "P(a) ==> a = b ==> P(b)" 

185 
by (rule subst) 

186 

187 
text {* 

188 
Note that this list of rules is in reverse order of priorities. 

189 
*} 

190 

191 
lemmas trans_rules [trans] = 

192 
forw_subst 

193 
back_subst 

194 
rev_mp 

195 
mp 

196 
transitive 

197 
trans 

198 

199 
lemmas [Pure.elim] = sym 

200 

4854  201 
end 