author  wenzelm 
Tue, 31 Jan 2006 00:43:14 +0100  
changeset 18861  38269ef5175a 
parent 18813  fc35dcc2558b 
child 19120  353d349740de 
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 

15481  8 
theory IFOL 
9 
imports Pure 

16417  10 
uses ("IFOL_lemmas.ML") ("fologic.ML") ("hypsubstdata.ML") ("intprover.ML") 
15481  11 
begin 
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

12 

0  13 

11677  14 
subsection {* Syntax and axiomatic basis *} 
15 

3906  16 
global 
17 

14854  18 
classes "term" 
18523  19 
finalconsts term_class 
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

20 
defaultsort "term" 
0  21 

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

22 
typedecl o 
79  23 

11747  24 
judgment 
25 
Trueprop :: "o => prop" ("(_)" 5) 

0  26 

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

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

29 
False :: o 
79  30 

31 
(* Connectives *) 

32 

17276  33 
"op =" :: "['a, 'a] => o" (infixl "=" 50) 
35  34 

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

35 
Not :: "o => o" ("~ _" [40] 40) 
17276  36 
"op &" :: "[o, o] => o" (infixr "&" 35) 
37 
"op " :: "[o, o] => o" (infixr "" 30) 

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

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

79  40 

41 
(* Quantifiers *) 

42 

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

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

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

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

0  47 

928  48 
syntax 
12662  49 
"_not_equal" :: "['a, 'a] => o" (infixl "~=" 50) 
35  50 
translations 
79  51 
"x ~= y" == "~ (x = y)" 
52 

12114
a8e860c86252
eliminated old "symbols" syntax, use "xsymbols" instead;
wenzelm
parents:
12019
diff
changeset

53 
syntax (xsymbols) 
11677  54 
Not :: "o => o" ("\<not> _" [40] 40) 
55 
"op &" :: "[o, o] => o" (infixr "\<and>" 35) 

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

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

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

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

12662  60 
"_not_equal" :: "['a, 'a] => o" (infixl "\<noteq>" 50) 
11677  61 
"op >" :: "[o, o] => o" (infixr "\<longrightarrow>" 25) 
62 
"op <>" :: "[o, o] => o" (infixr "\<longleftrightarrow>" 25) 

35  63 

6340  64 
syntax (HTML output) 
11677  65 
Not :: "o => o" ("\<not> _" [40] 40) 
14565  66 
"op &" :: "[o, o] => o" (infixr "\<and>" 35) 
67 
"op " :: "[o, o] => o" (infixr "\<or>" 30) 

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

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

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

71 
"_not_equal" :: "['a, 'a] => o" (infixl "\<noteq>" 50) 

6340  72 

73 

3932  74 
local 
3906  75 

14236  76 
finalconsts 
77 
False All Ex 

78 
"op =" 

79 
"op &" 

80 
"op " 

81 
"op >" 

82 

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

83 
axioms 
0  84 

79  85 
(* Equality *) 
0  86 

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

87 
refl: "a=a" 
0  88 

79  89 
(* Propositional logic *) 
0  90 

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

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

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

93 
conjunct2: "P&Q ==> Q" 
0  94 

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

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

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

97 
disjE: "[ PQ; P ==> R; Q ==> R ] ==> R" 
0  98 

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

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

100 
mp: "[ P>Q; P ] ==> Q" 
0  101 

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

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

103 

79  104 
(* Quantifiers *) 
0  105 

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

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

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

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

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

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

112 
(* Reflection *) 

113 

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

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

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

4092  117 

15377  118 
text{*Thanks to Stephan Merz*} 
119 
theorem subst: 

120 
assumes eq: "a = b" and p: "P(a)" 

121 
shows "P(b)" 

122 
proof  

123 
from eq have meta: "a \<equiv> b" 

124 
by (rule eq_reflection) 

125 
from p show ?thesis 

126 
by (unfold meta) 

127 
qed 

128 

129 

14236  130 
defs 
131 
(* Definitions *) 

132 

133 
True_def: "True == False>False" 

134 
not_def: "~P == P>False" 

135 
iff_def: "P<>Q == (P>Q) & (Q>P)" 

136 

137 
(* Unique existence *) 

138 

139 
ex1_def: "Ex1(P) == EX x. P(x) & (ALL y. P(y) > y=x)" 

140 

13779  141 

11677  142 
subsection {* Lemmas and proof tools *} 
143 

9886  144 
use "IFOL_lemmas.ML" 
11734  145 

18481  146 
ML {* 
147 
structure ProjectRule = ProjectRuleFun 

148 
(struct 

149 
val conjunct1 = thm "conjunct1"; 

150 
val conjunct2 = thm "conjunct2"; 

151 
val mp = thm "mp"; 

152 
end) 

153 
*} 

154 

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

155 
use "fologic.ML" 
9886  156 
use "hypsubstdata.ML" 
157 
setup hypsubst_setup 

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

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

159 

4092  160 

12875  161 
subsection {* Intuitionistic Reasoning *} 
12368  162 

12349  163 
lemma impE': 
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12875
diff
changeset

164 
assumes 1: "P > Q" 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12875
diff
changeset

165 
and 2: "Q ==> R" 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12875
diff
changeset

166 
and 3: "P > Q ==> P" 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12875
diff
changeset

167 
shows R 
12349  168 
proof  
169 
from 3 and 1 have P . 

12368  170 
with 1 have Q by (rule impE) 
12349  171 
with 2 show R . 
172 
qed 

173 

174 
lemma allE': 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12875
diff
changeset

175 
assumes 1: "ALL x. P(x)" 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12875
diff
changeset

176 
and 2: "P(x) ==> ALL x. P(x) ==> Q" 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12875
diff
changeset

177 
shows Q 
12349  178 
proof  
179 
from 1 have "P(x)" by (rule spec) 

180 
from this and 1 show Q by (rule 2) 

181 
qed 

182 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12875
diff
changeset

183 
lemma notE': 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12875
diff
changeset

184 
assumes 1: "~ P" 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12875
diff
changeset

185 
and 2: "~ P ==> P" 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12875
diff
changeset

186 
shows R 
12349  187 
proof  
188 
from 2 and 1 have P . 

189 
with 1 show R by (rule notE) 

190 
qed 

191 

192 
lemmas [Pure.elim!] = disjE iffE FalseE conjE exE 

193 
and [Pure.intro!] = iffI conjI impI TrueI notI allI refl 

194 
and [Pure.elim 2] = allE notE' impE' 

195 
and [Pure.intro] = exI disjI2 disjI1 

196 

18708  197 
setup {* ContextRules.addSWrapper (fn tac => hyp_subst_tac ORELSE' tac) *} 
12349  198 

199 

12368  200 
lemma iff_not_sym: "~ (Q <> P) ==> ~ (P <> Q)" 
17591  201 
by iprover 
12368  202 

203 
lemmas [sym] = sym iff_sym not_sym iff_not_sym 

204 
and [Pure.elim?] = iffD1 iffD2 impE 

205 

206 

13435  207 
lemma eq_commute: "a=b <> b=a" 
208 
apply (rule iffI) 

209 
apply (erule sym)+ 

210 
done 

211 

212 

11677  213 
subsection {* Atomizing metalevel rules *} 
214 

11747  215 
lemma atomize_all [atomize]: "(!!x. P(x)) == Trueprop (ALL x. P(x))" 
11976  216 
proof 
11677  217 
assume "!!x. P(x)" 
12368  218 
show "ALL x. P(x)" .. 
11677  219 
next 
220 
assume "ALL x. P(x)" 

12368  221 
thus "!!x. P(x)" .. 
11677  222 
qed 
223 

11747  224 
lemma atomize_imp [atomize]: "(A ==> B) == Trueprop (A > B)" 
11976  225 
proof 
12368  226 
assume "A ==> B" 
227 
thus "A > B" .. 

11677  228 
next 
229 
assume "A > B" and A 

230 
thus B by (rule mp) 

231 
qed 

232 

11747  233 
lemma atomize_eq [atomize]: "(x == y) == Trueprop (x = y)" 
11976  234 
proof 
11677  235 
assume "x == y" 
236 
show "x = y" by (unfold prems) (rule refl) 

237 
next 

238 
assume "x = y" 

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

240 
qed 

241 

18813  242 
lemma atomize_iff [atomize]: "(A == B) == Trueprop (A <> B)" 
243 
proof 

244 
assume "A == B" 

245 
show "A <> B" by (unfold prems) (rule iff_refl) 

246 
next 

247 
assume "A <> B" 

248 
thus "A == B" by (rule iff_reflection) 

249 
qed 

250 

12875  251 
lemma atomize_conj [atomize]: 
252 
"(!!C. (A ==> B ==> PROP C) ==> PROP C) == Trueprop (A & B)" 

11976  253 
proof 
11953  254 
assume "!!C. (A ==> B ==> PROP C) ==> PROP C" 
255 
show "A & B" by (rule conjI) 

256 
next 

257 
fix C 

258 
assume "A & B" 

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

260 
thus "PROP C" 

261 
proof this 

262 
show A by (rule conjunct1) 

263 
show B by (rule conjunct2) 

264 
qed 

265 
qed 

266 

12368  267 
lemmas [symmetric, rulify] = atomize_all atomize_imp 
18861  268 
and [symmetric, defn] = atomize_all atomize_imp atomize_eq atomize_iff 
11771  269 

11848  270 

271 
subsection {* Calculational rules *} 

272 

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

274 
by (rule ssubst) 

275 

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

277 
by (rule subst) 

278 

279 
text {* 

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

281 
*} 

282 

12019  283 
lemmas basic_trans_rules [trans] = 
11848  284 
forw_subst 
285 
back_subst 

286 
rev_mp 

287 
mp 

288 
trans 

289 

13779  290 
subsection {* ``Let'' declarations *} 
291 

292 
nonterminals letbinds letbind 

293 

294 
constdefs 

14854  295 
Let :: "['a::{}, 'a => 'b] => ('b::{})" 
13779  296 
"Let(s, f) == f(s)" 
297 

298 
syntax 

299 
"_bind" :: "[pttrn, 'a] => letbind" ("(2_ =/ _)" 10) 

300 
"" :: "letbind => letbinds" ("_") 

301 
"_binds" :: "[letbind, letbinds] => letbinds" ("_;/ _") 

302 
"_Let" :: "[letbinds, 'a] => 'a" ("(let (_)/ in (_))" 10) 

303 

304 
translations 

305 
"_Let(_binds(b, bs), e)" == "_Let(b, _Let(bs, e))" 

306 
"let x = a in e" == "Let(a, %x. e)" 

307 

308 

309 
lemma LetI: 

310 
assumes prem: "(!!x. x=t ==> P(u(x)))" 

311 
shows "P(let x=t in u(x))" 

312 
apply (unfold Let_def) 

313 
apply (rule refl [THEN prem]) 

314 
done 

315 

316 
ML 

317 
{* 

318 
val Let_def = thm "Let_def"; 

319 
val LetI = thm "LetI"; 

320 
*} 

321 

4854  322 
end 