author  wenzelm 
Sun, 26 Nov 2006 18:07:16 +0100  
changeset 21524  7843e2fd14a9 
parent 21404  eb85850d3eb7 
child 21539  c5cf9243ad62 
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" 
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset

19 
defaultsort "term" 
0  20 

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

21 
typedecl o 
79  22 

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

0  25 

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

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

28 
False :: o 
79  29 

30 
(* Connectives *) 

31 

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

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

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

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

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

79  39 

40 
(* Quantifiers *) 

41 

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

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

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

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

0  46 

19363  47 
abbreviation 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

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

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

21210  51 
notation (xsymbols) 
19656
09be06943252
tuned concrete syntax  abbreviation/const_syntax;
wenzelm
parents:
19380
diff
changeset

52 
not_equal (infixl "\<noteq>" 50) 
19363  53 

21210  54 
notation (HTML output) 
19656
09be06943252
tuned concrete syntax  abbreviation/const_syntax;
wenzelm
parents:
19380
diff
changeset

55 
not_equal (infixl "\<noteq>" 50) 
19363  56 

21524  57 
notation (xsymbols) 
58 
Not ("\<not> _" [40] 40) and 

59 
"op &" (infixr "\<and>" 35) and 

60 
"op " (infixr "\<or>" 30) and 

61 
All (binder "\<forall>" 10) and 

62 
Ex (binder "\<exists>" 10) and 

63 
Ex1 (binder "\<exists>!" 10) and 

64 
"op >" (infixr "\<longrightarrow>" 25) and 

65 
"op <>" (infixr "\<longleftrightarrow>" 25) 

35  66 

21524  67 
notation (HTML output) 
68 
Not ("\<not> _" [40] 40) and 

69 
"op &" (infixr "\<and>" 35) and 

70 
"op " (infixr "\<or>" 30) and 

71 
All (binder "\<forall>" 10) and 

72 
Ex (binder "\<exists>" 10) and 

73 
Ex1 (binder "\<exists>!" 10) 

6340  74 

3932  75 
local 
3906  76 

14236  77 
finalconsts 
78 
False All Ex 

79 
"op =" 

80 
"op &" 

81 
"op " 

82 
"op >" 

83 

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

84 
axioms 
0  85 

79  86 
(* Equality *) 
0  87 

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

88 
refl: "a=a" 
0  89 

79  90 
(* Propositional logic *) 
0  91 

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

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

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

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

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

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

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

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

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

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

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

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

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

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 

19756  119 
lemmas strip = impI allI 
120 

121 

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

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

125 
shows "P(b)" 

126 
proof  

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

128 
by (rule eq_reflection) 

129 
from p show ?thesis 

130 
by (unfold meta) 

131 
qed 

132 

133 

14236  134 
defs 
135 
(* Definitions *) 

136 

137 
True_def: "True == False>False" 

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

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

140 

141 
(* Unique existence *) 

142 

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

144 

13779  145 

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

9886  148 
use "IFOL_lemmas.ML" 
11734  149 

18481  150 
ML {* 
151 
structure ProjectRule = ProjectRuleFun 

152 
(struct 

153 
val conjunct1 = thm "conjunct1"; 

154 
val conjunct2 = thm "conjunct2"; 

155 
val mp = thm "mp"; 

156 
end) 

157 
*} 

158 

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

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

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

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

163 

4092  164 

12875  165 
subsection {* Intuitionistic Reasoning *} 
12368  166 

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

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

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

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

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

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

177 

178 
lemma allE': 

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

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

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

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

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

185 
qed 

186 

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

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

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

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

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

193 
with 1 show R by (rule notE) 

194 
qed 

195 

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

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

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

199 
and [Pure.intro] = exI disjI2 disjI1 

200 

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

203 

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

207 
lemmas [sym] = sym iff_sym not_sym iff_not_sym 

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

209 

210 

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

213 
apply (erule sym)+ 

214 
done 

215 

216 

11677  217 
subsection {* Atomizing metalevel rules *} 
218 

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

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

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

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

234 
thus B by (rule mp) 

235 
qed 

236 

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

241 
next 

242 
assume "x = y" 

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

244 
qed 

245 

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

248 
assume "A == B" 

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

250 
next 

251 
assume "A <> B" 

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

253 
qed 

254 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

273 

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

11848  277 

278 
subsection {* Calculational rules *} 

279 

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

281 
by (rule ssubst) 

282 

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

284 
by (rule subst) 

285 

286 
text {* 

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

288 
*} 

289 

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

293 
rev_mp 

294 
mp 

295 
trans 

296 

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

299 
nonterminals letbinds letbind 

300 

301 
constdefs 

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

305 
syntax 

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

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

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

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

310 

311 
translations 

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

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

314 

315 

316 
lemma LetI: 

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

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

319 
apply (unfold Let_def) 

320 
apply (rule refl [THEN prem]) 

321 
done 

322 

323 
ML 

324 
{* 

325 
val Let_def = thm "Let_def"; 

326 
val LetI = thm "LetI"; 

327 
*} 

328 

4854  329 
end 