author  wenzelm 
Sun, 09 Apr 2006 18:51:13 +0200  
changeset 19380  b808efaa5828 
parent 19363  667b5ea637dd 
child 19656  09be06943252 
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 

19363  48 
abbreviation 
19120
353d349740de
not_equal: replaced syntax translation by abbreviation;
wenzelm
parents:
18861
diff
changeset

49 
not_equal :: "['a, 'a] => o" (infixl "~=" 50) 
353d349740de
not_equal: replaced syntax translation by abbreviation;
wenzelm
parents:
18861
diff
changeset

50 
"x ~= y == ~ (x = y)" 
79  51 

19363  52 
abbreviation (xsymbols) 
19380  53 
not_equal1 (infixl "\<noteq>" 50) 
19363  54 
"x \<noteq> y == ~ (x = y)" 
55 

56 
abbreviation (HTML output) 

19380  57 
not_equal2 (infixl "\<noteq>" 50) 
58 
"not_equal2 == not_equal" 

19363  59 

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

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

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

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

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

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

67 
"op >" :: "[o, o] => o" (infixr "\<longrightarrow>" 25) 

68 
"op <>" :: "[o, o] => o" (infixr "\<longleftrightarrow>" 25) 

35  69 

6340  70 
syntax (HTML output) 
11677  71 
Not :: "o => o" ("\<not> _" [40] 40) 
14565  72 
"op &" :: "[o, o] => o" (infixr "\<and>" 35) 
73 
"op " :: "[o, o] => o" (infixr "\<or>" 30) 

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

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

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

6340  77 

78 

3932  79 
local 
3906  80 

14236  81 
finalconsts 
82 
False All Ex 

83 
"op =" 

84 
"op &" 

85 
"op " 

86 
"op >" 

87 

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

88 
axioms 
0  89 

79  90 
(* Equality *) 
0  91 

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

92 
refl: "a=a" 
0  93 

79  94 
(* Propositional logic *) 
0  95 

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

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

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

98 
conjunct2: "P&Q ==> Q" 
0  99 

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

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

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

102 
disjE: "[ PQ; P ==> R; Q ==> R ] ==> R" 
0  103 

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

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

105 
mp: "[ P>Q; P ] ==> Q" 
0  106 

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

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

108 

79  109 
(* Quantifiers *) 
0  110 

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

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

112 
spec: "(ALL x. P(x)) ==> P(x)" 
0  113 

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

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

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

117 
(* Reflection *) 

118 

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

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

120 
iff_reflection: "(P<>Q) ==> (P==Q)" 
0  121 

4092  122 

15377  123 
text{*Thanks to Stephan Merz*} 
124 
theorem subst: 

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

126 
shows "P(b)" 

127 
proof  

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

129 
by (rule eq_reflection) 

130 
from p show ?thesis 

131 
by (unfold meta) 

132 
qed 

133 

134 

14236  135 
defs 
136 
(* Definitions *) 

137 

138 
True_def: "True == False>False" 

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

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

141 

142 
(* Unique existence *) 

143 

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

145 

13779  146 

11677  147 
subsection {* Lemmas and proof tools *} 
148 

9886  149 
use "IFOL_lemmas.ML" 
11734  150 

18481  151 
ML {* 
152 
structure ProjectRule = ProjectRuleFun 

153 
(struct 

154 
val conjunct1 = thm "conjunct1"; 

155 
val conjunct2 = thm "conjunct2"; 

156 
val mp = thm "mp"; 

157 
end) 

158 
*} 

159 

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

160 
use "fologic.ML" 
9886  161 
use "hypsubstdata.ML" 
162 
setup hypsubst_setup 

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

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

164 

4092  165 

12875  166 
subsection {* Intuitionistic Reasoning *} 
12368  167 

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

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

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

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

172 
shows R 
12349  173 
proof  
174 
from 3 and 1 have P . 

12368  175 
with 1 have Q by (rule impE) 
12349  176 
with 2 show R . 
177 
qed 

178 

179 
lemma allE': 

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

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

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

182 
shows Q 
12349  183 
proof  
184 
from 1 have "P(x)" by (rule spec) 

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

186 
qed 

187 

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

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

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

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

191 
shows R 
12349  192 
proof  
193 
from 2 and 1 have P . 

194 
with 1 show R by (rule notE) 

195 
qed 

196 

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

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

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

200 
and [Pure.intro] = exI disjI2 disjI1 

201 

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

204 

12368  205 
lemma iff_not_sym: "~ (Q <> P) ==> ~ (P <> Q)" 
17591  206 
by iprover 
12368  207 

208 
lemmas [sym] = sym iff_sym not_sym iff_not_sym 

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

210 

211 

13435  212 
lemma eq_commute: "a=b <> b=a" 
213 
apply (rule iffI) 

214 
apply (erule sym)+ 

215 
done 

216 

217 

11677  218 
subsection {* Atomizing metalevel rules *} 
219 

11747  220 
lemma atomize_all [atomize]: "(!!x. P(x)) == Trueprop (ALL x. P(x))" 
11976  221 
proof 
11677  222 
assume "!!x. P(x)" 
12368  223 
show "ALL x. P(x)" .. 
11677  224 
next 
225 
assume "ALL x. P(x)" 

12368  226 
thus "!!x. P(x)" .. 
11677  227 
qed 
228 

11747  229 
lemma atomize_imp [atomize]: "(A ==> B) == Trueprop (A > B)" 
11976  230 
proof 
12368  231 
assume "A ==> B" 
232 
thus "A > B" .. 

11677  233 
next 
234 
assume "A > B" and A 

235 
thus B by (rule mp) 

236 
qed 

237 

11747  238 
lemma atomize_eq [atomize]: "(x == y) == Trueprop (x = y)" 
11976  239 
proof 
11677  240 
assume "x == y" 
241 
show "x = y" by (unfold prems) (rule refl) 

242 
next 

243 
assume "x = y" 

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

245 
qed 

246 

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

249 
assume "A == B" 

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

251 
next 

252 
assume "A <> B" 

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

254 
qed 

255 

12875  256 
lemma atomize_conj [atomize]: 
19120
353d349740de
not_equal: replaced syntax translation by abbreviation;
wenzelm
parents:
18861
diff
changeset

257 
includes meta_conjunction_syntax 
353d349740de
not_equal: replaced syntax translation by abbreviation;
wenzelm
parents:
18861
diff
changeset

258 
shows "(A && B) == Trueprop (A & B)" 
11976  259 
proof 
19120
353d349740de
not_equal: replaced syntax translation by abbreviation;
wenzelm
parents:
18861
diff
changeset

260 
assume conj: "A && B" 
353d349740de
not_equal: replaced syntax translation by abbreviation;
wenzelm
parents:
18861
diff
changeset

261 
show "A & B" 
353d349740de
not_equal: replaced syntax translation by abbreviation;
wenzelm
parents:
18861
diff
changeset

262 
proof (rule conjI) 
353d349740de
not_equal: replaced syntax translation by abbreviation;
wenzelm
parents:
18861
diff
changeset

263 
from conj show A by (rule conjunctionD1) 
353d349740de
not_equal: replaced syntax translation by abbreviation;
wenzelm
parents:
18861
diff
changeset

264 
from conj show B by (rule conjunctionD2) 
353d349740de
not_equal: replaced syntax translation by abbreviation;
wenzelm
parents:
18861
diff
changeset

265 
qed 
11953  266 
next 
19120
353d349740de
not_equal: replaced syntax translation by abbreviation;
wenzelm
parents:
18861
diff
changeset

267 
assume conj: "A & B" 
353d349740de
not_equal: replaced syntax translation by abbreviation;
wenzelm
parents:
18861
diff
changeset

268 
show "A && B" 
353d349740de
not_equal: replaced syntax translation by abbreviation;
wenzelm
parents:
18861
diff
changeset

269 
proof  
353d349740de
not_equal: replaced syntax translation by abbreviation;
wenzelm
parents:
18861
diff
changeset

270 
from conj show A .. 
353d349740de
not_equal: replaced syntax translation by abbreviation;
wenzelm
parents:
18861
diff
changeset

271 
from conj show B .. 
11953  272 
qed 
273 
qed 

274 

12368  275 
lemmas [symmetric, rulify] = atomize_all atomize_imp 
18861  276 
and [symmetric, defn] = atomize_all atomize_imp atomize_eq atomize_iff 
11771  277 

11848  278 

279 
subsection {* Calculational rules *} 

280 

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

282 
by (rule ssubst) 

283 

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

285 
by (rule subst) 

286 

287 
text {* 

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

289 
*} 

290 

12019  291 
lemmas basic_trans_rules [trans] = 
11848  292 
forw_subst 
293 
back_subst 

294 
rev_mp 

295 
mp 

296 
trans 

297 

13779  298 
subsection {* ``Let'' declarations *} 
299 

300 
nonterminals letbinds letbind 

301 

302 
constdefs 

14854  303 
Let :: "['a::{}, 'a => 'b] => ('b::{})" 
13779  304 
"Let(s, f) == f(s)" 
305 

306 
syntax 

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

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

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

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

311 

312 
translations 

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

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

315 

316 

317 
lemma LetI: 

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

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

320 
apply (unfold Let_def) 

321 
apply (rule refl [THEN prem]) 

322 
done 

323 

324 
ML 

325 
{* 

326 
val Let_def = thm "Let_def"; 

327 
val LetI = thm "LetI"; 

328 
*} 

329 

4854  330 
end 