author | nipkow |
Mon, 06 Aug 2001 13:43:24 +0200 | |
changeset 11464 | ddea204de5bc |
parent 11096 | bedfd42db838 |
child 11678 | 6aa3e2d26683 |
permissions | -rw-r--r-- |
9487 | 1 |
(* Title: FOL/FOL.thy |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson and Markus Wenzel |
|
4 |
||
5 |
Classical first-order logic. |
|
6 |
||
7 |
This may serve as a good example of initializing all the tools and |
|
8 |
packages required for a reasonable working environment. Please go |
|
9 |
elsewhere to see actual applications! |
|
10 |
*) |
|
4093 | 11 |
|
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
5887
diff
changeset
|
12 |
theory FOL = IFOL |
9487 | 13 |
files |
14 |
("FOL_lemmas1.ML") ("cladata.ML") ("blastdata.ML") |
|
15 |
("simpdata.ML") ("FOL_lemmas2.ML"): |
|
16 |
||
17 |
||
18 |
subsection {* The classical axiom *} |
|
4093 | 19 |
|
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
5887
diff
changeset
|
20 |
axioms |
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
5887
diff
changeset
|
21 |
classical: "(~P ==> P) ==> P" |
4093 | 22 |
|
9487 | 23 |
|
24 |
subsection {* Setup of several proof tools *} |
|
25 |
||
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
5887
diff
changeset
|
26 |
use "FOL_lemmas1.ML" |
9487 | 27 |
|
10430 | 28 |
lemma atomize_all: "(!!x. P(x)) == Trueprop (ALL x. P(x))" |
9487 | 29 |
proof (rule equal_intr_rule) |
30 |
assume "!!x. P(x)" |
|
10383 | 31 |
show "ALL x. P(x)" by (rule allI) |
9487 | 32 |
next |
33 |
assume "ALL x. P(x)" |
|
10383 | 34 |
thus "!!x. P(x)" by (rule allE) |
9487 | 35 |
qed |
36 |
||
10430 | 37 |
lemma atomize_imp: "(A ==> B) == Trueprop (A --> B)" |
9487 | 38 |
proof (rule equal_intr_rule) |
39 |
assume r: "A ==> B" |
|
10383 | 40 |
show "A --> B" by (rule impI) (rule r) |
9487 | 41 |
next |
42 |
assume "A --> B" and A |
|
10383 | 43 |
thus B by (rule mp) |
9487 | 44 |
qed |
45 |
||
10430 | 46 |
lemma atomize_eq: "(x == y) == Trueprop (x = y)" |
47 |
proof (rule equal_intr_rule) |
|
48 |
assume "x == y" |
|
49 |
show "x = y" by (unfold prems) (rule refl) |
|
50 |
next |
|
51 |
assume "x = y" |
|
52 |
thus "x == y" by (rule eq_reflection) |
|
53 |
qed |
|
54 |
||
55 |
lemmas atomize = atomize_all atomize_imp |
|
56 |
lemmas atomize' = atomize atomize_eq |
|
9525 | 57 |
|
10383 | 58 |
use "cladata.ML" |
59 |
setup Cla.setup |
|
60 |
setup clasetup |
|
61 |
||
9487 | 62 |
use "blastdata.ML" |
63 |
setup Blast.setup |
|
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
5887
diff
changeset
|
64 |
use "FOL_lemmas2.ML" |
9487 | 65 |
|
66 |
use "simpdata.ML" |
|
67 |
setup simpsetup |
|
68 |
setup "Simplifier.method_setup Splitter.split_modifiers" |
|
69 |
setup Splitter.setup |
|
70 |
setup Clasimp.setup |
|
9885 | 71 |
setup Rulify.setup |
9487 | 72 |
|
73 |
||
74 |
subsection {* Calculational rules *} |
|
75 |
||
76 |
lemma forw_subst: "a = b ==> P(b) ==> P(a)" |
|
77 |
by (rule ssubst) |
|
78 |
||
79 |
lemma back_subst: "P(a) ==> a = b ==> P(b)" |
|
80 |
by (rule subst) |
|
81 |
||
82 |
text {* |
|
83 |
Note that this list of rules is in reverse order of priorities. |
|
84 |
*} |
|
85 |
||
86 |
lemmas trans_rules [trans] = |
|
87 |
forw_subst |
|
88 |
back_subst |
|
89 |
rev_mp |
|
90 |
mp |
|
11096 | 91 |
transitive |
9487 | 92 |
trans |
93 |
||
94 |
lemmas [elim?] = sym |
|
4093 | 95 |
|
4854 | 96 |
end |