author | wenzelm |
Sun, 14 Oct 2001 22:15:07 +0200 | |
changeset 11771 | b7b100a2de1d |
parent 11678 | 6aa3e2d26683 |
child 11848 | 6e3017adb8c0 |
permissions | -rw-r--r-- |
9487 | 1 |
(* Title: FOL/FOL.thy |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson and Markus Wenzel |
|
11678 | 4 |
*) |
9487 | 5 |
|
11678 | 6 |
header {* Classical first-order logic *} |
4093 | 7 |
|
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
5887
diff
changeset
|
8 |
theory FOL = IFOL |
9487 | 9 |
files |
10 |
("FOL_lemmas1.ML") ("cladata.ML") ("blastdata.ML") |
|
11 |
("simpdata.ML") ("FOL_lemmas2.ML"): |
|
12 |
||
13 |
||
14 |
subsection {* The classical axiom *} |
|
4093 | 15 |
|
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
5887
diff
changeset
|
16 |
axioms |
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
5887
diff
changeset
|
17 |
classical: "(~P ==> P) ==> P" |
4093 | 18 |
|
9487 | 19 |
|
11678 | 20 |
subsection {* Lemmas and proof tools *} |
9487 | 21 |
|
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
5887
diff
changeset
|
22 |
use "FOL_lemmas1.ML" |
11678 | 23 |
theorems case_split = case_split_thm [case_names True False] |
9525 | 24 |
|
10383 | 25 |
use "cladata.ML" |
26 |
setup Cla.setup |
|
27 |
setup clasetup |
|
28 |
||
9487 | 29 |
use "blastdata.ML" |
30 |
setup Blast.setup |
|
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
5887
diff
changeset
|
31 |
use "FOL_lemmas2.ML" |
9487 | 32 |
|
33 |
use "simpdata.ML" |
|
34 |
setup simpsetup |
|
35 |
setup "Simplifier.method_setup Splitter.split_modifiers" |
|
36 |
setup Splitter.setup |
|
37 |
setup Clasimp.setup |
|
38 |
||
11678 | 39 |
|
40 |
subsection {* Proof by cases and induction *} |
|
41 |
||
42 |
text {* Proper handling of non-atomic rule statements. *} |
|
43 |
||
44 |
constdefs |
|
45 |
induct_forall :: "('a => o) => o" |
|
46 |
"induct_forall(P) == \<forall>x. P(x)" |
|
47 |
induct_implies :: "o => o => o" |
|
48 |
"induct_implies(A, B) == A --> B" |
|
49 |
induct_equal :: "'a => 'a => o" |
|
50 |
"induct_equal(x, y) == x = y" |
|
51 |
||
52 |
lemma induct_forall_eq: "(!!x. P(x)) == Trueprop(induct_forall(\<lambda>x. P(x)))" |
|
53 |
by (simp only: atomize_all induct_forall_def) |
|
54 |
||
55 |
lemma induct_implies_eq: "(A ==> B) == Trueprop(induct_implies(A, B))" |
|
56 |
by (simp only: atomize_imp induct_implies_def) |
|
57 |
||
58 |
lemma induct_equal_eq: "(x == y) == Trueprop(induct_equal(x, y))" |
|
59 |
by (simp only: atomize_eq induct_equal_def) |
|
60 |
||
61 |
lemmas induct_atomize = induct_forall_eq induct_implies_eq induct_equal_eq |
|
62 |
lemmas induct_rulify1 = induct_atomize [symmetric, standard] |
|
63 |
lemmas induct_rulify2 = induct_forall_def induct_implies_def induct_equal_def |
|
64 |
||
65 |
hide const induct_forall induct_implies induct_equal |
|
66 |
||
67 |
||
68 |
text {* Method setup. *} |
|
69 |
||
70 |
ML {* |
|
71 |
structure InductMethod = InductMethodFun |
|
72 |
(struct |
|
73 |
val dest_concls = FOLogic.dest_concls; |
|
74 |
val cases_default = thm "case_split"; |
|
75 |
val conjI = thm "conjI"; |
|
76 |
val atomize = thms "induct_atomize"; |
|
77 |
val rulify1 = thms "induct_rulify1"; |
|
78 |
val rulify2 = thms "induct_rulify2"; |
|
79 |
end); |
|
80 |
*} |
|
81 |
||
82 |
setup InductMethod.setup |
|
83 |
||
84 |
||
9487 | 85 |
subsection {* Calculational rules *} |
86 |
||
87 |
lemma forw_subst: "a = b ==> P(b) ==> P(a)" |
|
88 |
by (rule ssubst) |
|
89 |
||
90 |
lemma back_subst: "P(a) ==> a = b ==> P(b)" |
|
91 |
by (rule subst) |
|
92 |
||
93 |
text {* |
|
94 |
Note that this list of rules is in reverse order of priorities. |
|
95 |
*} |
|
96 |
||
97 |
lemmas trans_rules [trans] = |
|
98 |
forw_subst |
|
99 |
back_subst |
|
100 |
rev_mp |
|
101 |
mp |
|
11096 | 102 |
transitive |
9487 | 103 |
trans |
104 |
||
105 |
lemmas [elim?] = sym |
|
4093 | 106 |
|
4854 | 107 |
end |