|
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 *) |
1 |
11 |
2 theory FOL = IFOL |
12 theory FOL = IFOL |
3 files ("FOL_lemmas1.ML") ("cladata.ML") ("blastdata.ML") ("simpdata.ML") ("FOL_lemmas2.ML"): |
13 files |
|
14 ("FOL_lemmas1.ML") ("cladata.ML") ("blastdata.ML") |
|
15 ("simpdata.ML") ("FOL_lemmas2.ML"): |
|
16 |
|
17 |
|
18 subsection {* The classical axiom *} |
4 |
19 |
5 axioms |
20 axioms |
6 classical: "(~P ==> P) ==> P" |
21 classical: "(~P ==> P) ==> P" |
7 |
22 |
|
23 |
|
24 subsection {* Setup of several proof tools *} |
|
25 |
8 use "FOL_lemmas1.ML" |
26 use "FOL_lemmas1.ML" |
9 use "cladata.ML" setup Cla.setup setup clasetup |
27 use "cladata.ML" |
10 use "blastdata.ML" setup Blast.setup |
28 setup Cla.setup |
|
29 setup clasetup |
|
30 |
|
31 lemma all_eq: "(!!x. P(x)) == Trueprop (ALL x. P(x))" |
|
32 proof (rule equal_intr_rule) |
|
33 assume "!!x. P(x)" |
|
34 show "ALL x. P(x)" .. |
|
35 next |
|
36 assume "ALL x. P(x)" |
|
37 thus "!!x. P(x)" .. |
|
38 qed |
|
39 |
|
40 lemma imp_eq: "(A ==> B) == Trueprop (A --> B)" |
|
41 proof (rule equal_intr_rule) |
|
42 assume r: "A ==> B" |
|
43 show "A --> B" |
|
44 by (rule) (rule r) |
|
45 next |
|
46 assume "A --> B" and A |
|
47 thus B .. |
|
48 qed |
|
49 |
|
50 use "blastdata.ML" |
|
51 setup Blast.setup |
11 use "FOL_lemmas2.ML" |
52 use "FOL_lemmas2.ML" |
12 use "simpdata.ML" setup simpsetup setup cong_attrib_setup |
53 |
13 setup "Simplifier.method_setup Splitter.split_modifiers" |
54 use "simpdata.ML" |
14 setup Splitter.setup setup Clasimp.setup |
55 setup simpsetup |
|
56 setup cong_attrib_setup |
|
57 setup "Simplifier.method_setup Splitter.split_modifiers" |
|
58 setup Splitter.setup |
|
59 setup Clasimp.setup |
|
60 |
|
61 |
|
62 subsection {* Calculational rules *} |
|
63 |
|
64 lemma forw_subst: "a = b ==> P(b) ==> P(a)" |
|
65 by (rule ssubst) |
|
66 |
|
67 lemma back_subst: "P(a) ==> a = b ==> P(b)" |
|
68 by (rule subst) |
|
69 |
|
70 text {* |
|
71 Note that this list of rules is in reverse order of priorities. |
|
72 *} |
|
73 |
|
74 lemmas trans_rules [trans] = |
|
75 forw_subst |
|
76 back_subst |
|
77 rev_mp |
|
78 mp |
|
79 trans |
|
80 |
|
81 lemmas [elim?] = sym |
15 |
82 |
16 end |
83 end |