author | wenzelm |
Tue, 16 May 2006 21:33:01 +0200 | |
changeset 19656 | 09be06943252 |
parent 19380 | b808efaa5828 |
child 19683 | 3620e494cef2 |
permissions | -rw-r--r-- |
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 first-order 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 |
|
19656
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19380
diff
changeset
|
52 |
const_syntax (xsymbols) |
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19380
diff
changeset
|
53 |
not_equal (infixl "\<noteq>" 50) |
19363 | 54 |
|
19656
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19380
diff
changeset
|
55 |
const_syntax (HTML output) |
09be06943252
tuned concrete syntax -- abbreviation/const_syntax;
wenzelm
parents:
19380
diff
changeset
|
56 |
not_equal (infixl "\<noteq>" 50) |
19363 | 57 |
|
12114
a8e860c86252
eliminated old "symbols" syntax, use "xsymbols" instead;
wenzelm
parents:
12019
diff
changeset
|
58 |
syntax (xsymbols) |
11677 | 59 |
Not :: "o => o" ("\<not> _" [40] 40) |
60 |
"op &" :: "[o, o] => o" (infixr "\<and>" 35) |
|
61 |
"op |" :: "[o, o] => o" (infixr "\<or>" 30) |
|
62 |
"ALL " :: "[idts, o] => o" ("(3\<forall>_./ _)" [0, 10] 10) |
|
63 |
"EX " :: "[idts, o] => o" ("(3\<exists>_./ _)" [0, 10] 10) |
|
64 |
"EX! " :: "[idts, o] => o" ("(3\<exists>!_./ _)" [0, 10] 10) |
|
65 |
"op -->" :: "[o, o] => o" (infixr "\<longrightarrow>" 25) |
|
66 |
"op <->" :: "[o, o] => o" (infixr "\<longleftrightarrow>" 25) |
|
35 | 67 |
|
6340 | 68 |
syntax (HTML output) |
11677 | 69 |
Not :: "o => o" ("\<not> _" [40] 40) |
14565 | 70 |
"op &" :: "[o, o] => o" (infixr "\<and>" 35) |
71 |
"op |" :: "[o, o] => o" (infixr "\<or>" 30) |
|
72 |
"ALL " :: "[idts, o] => o" ("(3\<forall>_./ _)" [0, 10] 10) |
|
73 |
"EX " :: "[idts, o] => o" ("(3\<exists>_./ _)" [0, 10] 10) |
|
74 |
"EX! " :: "[idts, o] => o" ("(3\<exists>!_./ _)" [0, 10] 10) |
|
6340 | 75 |
|
76 |
||
3932 | 77 |
local |
3906 | 78 |
|
14236 | 79 |
finalconsts |
80 |
False All Ex |
|
81 |
"op =" |
|
82 |
"op &" |
|
83 |
"op |" |
|
84 |
"op -->" |
|
85 |
||
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
86 |
axioms |
0 | 87 |
|
79 | 88 |
(* Equality *) |
0 | 89 |
|
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
90 |
refl: "a=a" |
0 | 91 |
|
79 | 92 |
(* Propositional logic *) |
0 | 93 |
|
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
94 |
conjI: "[| P; Q |] ==> P&Q" |
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
95 |
conjunct1: "P&Q ==> P" |
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
96 |
conjunct2: "P&Q ==> Q" |
0 | 97 |
|
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
98 |
disjI1: "P ==> P|Q" |
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
99 |
disjI2: "Q ==> P|Q" |
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
100 |
disjE: "[| P|Q; P ==> R; Q ==> R |] ==> R" |
0 | 101 |
|
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
102 |
impI: "(P ==> Q) ==> P-->Q" |
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
103 |
mp: "[| P-->Q; P |] ==> Q" |
0 | 104 |
|
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
105 |
FalseE: "False ==> P" |
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
106 |
|
79 | 107 |
(* Quantifiers *) |
0 | 108 |
|
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
109 |
allI: "(!!x. P(x)) ==> (ALL x. P(x))" |
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
110 |
spec: "(ALL x. P(x)) ==> P(x)" |
0 | 111 |
|
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
112 |
exI: "P(x) ==> (EX x. P(x))" |
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
113 |
exE: "[| EX x. P(x); !!x. P(x) ==> R |] ==> R" |
0 | 114 |
|
115 |
(* Reflection *) |
|
116 |
||
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
117 |
eq_reflection: "(x=y) ==> (x==y)" |
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
118 |
iff_reflection: "(P<->Q) ==> (P==Q)" |
0 | 119 |
|
4092 | 120 |
|
15377 | 121 |
text{*Thanks to Stephan Merz*} |
122 |
theorem subst: |
|
123 |
assumes eq: "a = b" and p: "P(a)" |
|
124 |
shows "P(b)" |
|
125 |
proof - |
|
126 |
from eq have meta: "a \<equiv> b" |
|
127 |
by (rule eq_reflection) |
|
128 |
from p show ?thesis |
|
129 |
by (unfold meta) |
|
130 |
qed |
|
131 |
||
132 |
||
14236 | 133 |
defs |
134 |
(* Definitions *) |
|
135 |
||
136 |
True_def: "True == False-->False" |
|
137 |
not_def: "~P == P-->False" |
|
138 |
iff_def: "P<->Q == (P-->Q) & (Q-->P)" |
|
139 |
||
140 |
(* Unique existence *) |
|
141 |
||
142 |
ex1_def: "Ex1(P) == EX x. P(x) & (ALL y. P(y) --> y=x)" |
|
143 |
||
13779 | 144 |
|
11677 | 145 |
subsection {* Lemmas and proof tools *} |
146 |
||
9886 | 147 |
use "IFOL_lemmas.ML" |
11734 | 148 |
|
18481 | 149 |
ML {* |
150 |
structure ProjectRule = ProjectRuleFun |
|
151 |
(struct |
|
152 |
val conjunct1 = thm "conjunct1"; |
|
153 |
val conjunct2 = thm "conjunct2"; |
|
154 |
val mp = thm "mp"; |
|
155 |
end) |
|
156 |
*} |
|
157 |
||
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
158 |
use "fologic.ML" |
9886 | 159 |
use "hypsubstdata.ML" |
160 |
setup hypsubst_setup |
|
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
161 |
use "intprover.ML" |
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
6340
diff
changeset
|
162 |
|
4092 | 163 |
|
12875 | 164 |
subsection {* Intuitionistic Reasoning *} |
12368 | 165 |
|
12349 | 166 |
lemma impE': |
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12875
diff
changeset
|
167 |
assumes 1: "P --> Q" |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12875
diff
changeset
|
168 |
and 2: "Q ==> R" |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12875
diff
changeset
|
169 |
and 3: "P --> Q ==> P" |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12875
diff
changeset
|
170 |
shows R |
12349 | 171 |
proof - |
172 |
from 3 and 1 have P . |
|
12368 | 173 |
with 1 have Q by (rule impE) |
12349 | 174 |
with 2 show R . |
175 |
qed |
|
176 |
||
177 |
lemma allE': |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12875
diff
changeset
|
178 |
assumes 1: "ALL x. P(x)" |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12875
diff
changeset
|
179 |
and 2: "P(x) ==> ALL x. P(x) ==> Q" |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12875
diff
changeset
|
180 |
shows Q |
12349 | 181 |
proof - |
182 |
from 1 have "P(x)" by (rule spec) |
|
183 |
from this and 1 show Q by (rule 2) |
|
184 |
qed |
|
185 |
||
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12875
diff
changeset
|
186 |
lemma notE': |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12875
diff
changeset
|
187 |
assumes 1: "~ P" |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12875
diff
changeset
|
188 |
and 2: "~ P ==> P" |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12875
diff
changeset
|
189 |
shows R |
12349 | 190 |
proof - |
191 |
from 2 and 1 have P . |
|
192 |
with 1 show R by (rule notE) |
|
193 |
qed |
|
194 |
||
195 |
lemmas [Pure.elim!] = disjE iffE FalseE conjE exE |
|
196 |
and [Pure.intro!] = iffI conjI impI TrueI notI allI refl |
|
197 |
and [Pure.elim 2] = allE notE' impE' |
|
198 |
and [Pure.intro] = exI disjI2 disjI1 |
|
199 |
||
18708 | 200 |
setup {* ContextRules.addSWrapper (fn tac => hyp_subst_tac ORELSE' tac) *} |
12349 | 201 |
|
202 |
||
12368 | 203 |
lemma iff_not_sym: "~ (Q <-> P) ==> ~ (P <-> Q)" |
17591 | 204 |
by iprover |
12368 | 205 |
|
206 |
lemmas [sym] = sym iff_sym not_sym iff_not_sym |
|
207 |
and [Pure.elim?] = iffD1 iffD2 impE |
|
208 |
||
209 |
||
13435 | 210 |
lemma eq_commute: "a=b <-> b=a" |
211 |
apply (rule iffI) |
|
212 |
apply (erule sym)+ |
|
213 |
done |
|
214 |
||
215 |
||
11677 | 216 |
subsection {* Atomizing meta-level rules *} |
217 |
||
11747 | 218 |
lemma atomize_all [atomize]: "(!!x. P(x)) == Trueprop (ALL x. P(x))" |
11976 | 219 |
proof |
11677 | 220 |
assume "!!x. P(x)" |
12368 | 221 |
show "ALL x. P(x)" .. |
11677 | 222 |
next |
223 |
assume "ALL x. P(x)" |
|
12368 | 224 |
thus "!!x. P(x)" .. |
11677 | 225 |
qed |
226 |
||
11747 | 227 |
lemma atomize_imp [atomize]: "(A ==> B) == Trueprop (A --> B)" |
11976 | 228 |
proof |
12368 | 229 |
assume "A ==> B" |
230 |
thus "A --> B" .. |
|
11677 | 231 |
next |
232 |
assume "A --> B" and A |
|
233 |
thus B by (rule mp) |
|
234 |
qed |
|
235 |
||
11747 | 236 |
lemma atomize_eq [atomize]: "(x == y) == Trueprop (x = y)" |
11976 | 237 |
proof |
11677 | 238 |
assume "x == y" |
239 |
show "x = y" by (unfold prems) (rule refl) |
|
240 |
next |
|
241 |
assume "x = y" |
|
242 |
thus "x == y" by (rule eq_reflection) |
|
243 |
qed |
|
244 |
||
18813 | 245 |
lemma atomize_iff [atomize]: "(A == B) == Trueprop (A <-> B)" |
246 |
proof |
|
247 |
assume "A == B" |
|
248 |
show "A <-> B" by (unfold prems) (rule iff_refl) |
|
249 |
next |
|
250 |
assume "A <-> B" |
|
251 |
thus "A == B" by (rule iff_reflection) |
|
252 |
qed |
|
253 |
||
12875 | 254 |
lemma atomize_conj [atomize]: |
19120
353d349740de
not_equal: replaced syntax translation by abbreviation;
wenzelm
parents:
18861
diff
changeset
|
255 |
includes meta_conjunction_syntax |
353d349740de
not_equal: replaced syntax translation by abbreviation;
wenzelm
parents:
18861
diff
changeset
|
256 |
shows "(A && B) == Trueprop (A & B)" |
11976 | 257 |
proof |
19120
353d349740de
not_equal: replaced syntax translation by abbreviation;
wenzelm
parents:
18861
diff
changeset
|
258 |
assume conj: "A && B" |
353d349740de
not_equal: replaced syntax translation by abbreviation;
wenzelm
parents:
18861
diff
changeset
|
259 |
show "A & B" |
353d349740de
not_equal: replaced syntax translation by abbreviation;
wenzelm
parents:
18861
diff
changeset
|
260 |
proof (rule conjI) |
353d349740de
not_equal: replaced syntax translation by abbreviation;
wenzelm
parents:
18861
diff
changeset
|
261 |
from conj show A by (rule conjunctionD1) |
353d349740de
not_equal: replaced syntax translation by abbreviation;
wenzelm
parents:
18861
diff
changeset
|
262 |
from conj show B by (rule conjunctionD2) |
353d349740de
not_equal: replaced syntax translation by abbreviation;
wenzelm
parents:
18861
diff
changeset
|
263 |
qed |
11953 | 264 |
next |
19120
353d349740de
not_equal: replaced syntax translation by abbreviation;
wenzelm
parents:
18861
diff
changeset
|
265 |
assume conj: "A & B" |
353d349740de
not_equal: replaced syntax translation by abbreviation;
wenzelm
parents:
18861
diff
changeset
|
266 |
show "A && B" |
353d349740de
not_equal: replaced syntax translation by abbreviation;
wenzelm
parents:
18861
diff
changeset
|
267 |
proof - |
353d349740de
not_equal: replaced syntax translation by abbreviation;
wenzelm
parents:
18861
diff
changeset
|
268 |
from conj show A .. |
353d349740de
not_equal: replaced syntax translation by abbreviation;
wenzelm
parents:
18861
diff
changeset
|
269 |
from conj show B .. |
11953 | 270 |
qed |
271 |
qed |
|
272 |
||
12368 | 273 |
lemmas [symmetric, rulify] = atomize_all atomize_imp |
18861 | 274 |
and [symmetric, defn] = atomize_all atomize_imp atomize_eq atomize_iff |
11771 | 275 |
|
11848 | 276 |
|
277 |
subsection {* Calculational rules *} |
|
278 |
||
279 |
lemma forw_subst: "a = b ==> P(b) ==> P(a)" |
|
280 |
by (rule ssubst) |
|
281 |
||
282 |
lemma back_subst: "P(a) ==> a = b ==> P(b)" |
|
283 |
by (rule subst) |
|
284 |
||
285 |
text {* |
|
286 |
Note that this list of rules is in reverse order of priorities. |
|
287 |
*} |
|
288 |
||
12019 | 289 |
lemmas basic_trans_rules [trans] = |
11848 | 290 |
forw_subst |
291 |
back_subst |
|
292 |
rev_mp |
|
293 |
mp |
|
294 |
trans |
|
295 |
||
13779 | 296 |
subsection {* ``Let'' declarations *} |
297 |
||
298 |
nonterminals letbinds letbind |
|
299 |
||
300 |
constdefs |
|
14854 | 301 |
Let :: "['a::{}, 'a => 'b] => ('b::{})" |
13779 | 302 |
"Let(s, f) == f(s)" |
303 |
||
304 |
syntax |
|
305 |
"_bind" :: "[pttrn, 'a] => letbind" ("(2_ =/ _)" 10) |
|
306 |
"" :: "letbind => letbinds" ("_") |
|
307 |
"_binds" :: "[letbind, letbinds] => letbinds" ("_;/ _") |
|
308 |
"_Let" :: "[letbinds, 'a] => 'a" ("(let (_)/ in (_))" 10) |
|
309 |
||
310 |
translations |
|
311 |
"_Let(_binds(b, bs), e)" == "_Let(b, _Let(bs, e))" |
|
312 |
"let x = a in e" == "Let(a, %x. e)" |
|
313 |
||
314 |
||
315 |
lemma LetI: |
|
316 |
assumes prem: "(!!x. x=t ==> P(u(x)))" |
|
317 |
shows "P(let x=t in u(x))" |
|
318 |
apply (unfold Let_def) |
|
319 |
apply (rule refl [THEN prem]) |
|
320 |
done |
|
321 |
||
322 |
ML |
|
323 |
{* |
|
324 |
val Let_def = thm "Let_def"; |
|
325 |
val LetI = thm "LetI"; |
|
326 |
*} |
|
327 |
||
4854 | 328 |
end |