author | wenzelm |
Fri, 30 Dec 2005 16:56:56 +0100 | |
changeset 18522 | 9bdfb6eaf8ab |
parent 18511 | beed2bc052a3 |
child 18531 | ce7b80b7c84e |
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 |
|
18456 | 8 |
theory FOL |
15481 | 9 |
imports IFOL |
16417 | 10 |
uses ("FOL_lemmas1.ML") ("cladata.ML") ("blastdata.ML") ("simpdata.ML") |
15481 | 11 |
("eqrule_FOL_data.ML") |
12 |
("~~/src/Provers/eqsubst.ML") |
|
18456 | 13 |
begin |
9487 | 14 |
|
15 |
||
16 |
subsection {* The classical axiom *} |
|
4093 | 17 |
|
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
5887
diff
changeset
|
18 |
axioms |
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
5887
diff
changeset
|
19 |
classical: "(~P ==> P) ==> P" |
4093 | 20 |
|
9487 | 21 |
|
11678 | 22 |
subsection {* Lemmas and proof tools *} |
9487 | 23 |
|
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
5887
diff
changeset
|
24 |
use "FOL_lemmas1.ML" |
12127
219e543496a3
theorems case_split = case_split_thm [case_names True False, cases type: o];
wenzelm
parents:
11988
diff
changeset
|
25 |
theorems case_split = case_split_thm [case_names True False, cases type: o] |
9525 | 26 |
|
18522 | 27 |
lemma cla_dist_concl: |
28 |
assumes x: "~Z_Z ==> PROP X_X" |
|
29 |
and z: "PROP Y_Y ==> Z_Z" |
|
30 |
and y: "PROP X_X ==> PROP Y_Y" |
|
31 |
shows Z_Z |
|
32 |
apply (rule classical) |
|
33 |
apply (erule x [THEN y, THEN z]) |
|
34 |
done |
|
35 |
||
10383 | 36 |
use "cladata.ML" |
37 |
setup Cla.setup |
|
14156 | 38 |
setup cla_setup |
39 |
setup case_setup |
|
10383 | 40 |
|
9487 | 41 |
use "blastdata.ML" |
42 |
setup Blast.setup |
|
13550 | 43 |
|
44 |
||
45 |
lemma ex1_functional: "[| EX! z. P(a,z); P(a,b); P(a,c) |] ==> b = c" |
|
46 |
by blast |
|
47 |
||
48 |
ML {* |
|
49 |
val ex1_functional = thm "ex1_functional"; |
|
50 |
*} |
|
9487 | 51 |
|
52 |
use "simpdata.ML" |
|
53 |
setup simpsetup |
|
54 |
setup "Simplifier.method_setup Splitter.split_modifiers" |
|
55 |
setup Splitter.setup |
|
56 |
setup Clasimp.setup |
|
57 |
||
15481 | 58 |
|
59 |
subsection {* Lucas Dixon's eqstep tactic *} |
|
60 |
||
61 |
use "~~/src/Provers/eqsubst.ML"; |
|
62 |
use "eqrule_FOL_data.ML"; |
|
63 |
||
64 |
setup EQSubstTac.setup |
|
65 |
||
66 |
||
14085 | 67 |
subsection {* Other simple lemmas *} |
68 |
||
69 |
lemma [simp]: "((P-->R) <-> (Q-->R)) <-> ((P<->Q) | R)" |
|
70 |
by blast |
|
71 |
||
72 |
lemma [simp]: "((P-->Q) <-> (P-->R)) <-> (P --> (Q<->R))" |
|
73 |
by blast |
|
74 |
||
75 |
lemma not_disj_iff_imp: "~P | Q <-> (P-->Q)" |
|
76 |
by blast |
|
77 |
||
78 |
(** Monotonicity of implications **) |
|
79 |
||
80 |
lemma conj_mono: "[| P1-->Q1; P2-->Q2 |] ==> (P1&P2) --> (Q1&Q2)" |
|
81 |
by fast (*or (IntPr.fast_tac 1)*) |
|
82 |
||
83 |
lemma disj_mono: "[| P1-->Q1; P2-->Q2 |] ==> (P1|P2) --> (Q1|Q2)" |
|
84 |
by fast (*or (IntPr.fast_tac 1)*) |
|
85 |
||
86 |
lemma imp_mono: "[| Q1-->P1; P2-->Q2 |] ==> (P1-->P2)-->(Q1-->Q2)" |
|
87 |
by fast (*or (IntPr.fast_tac 1)*) |
|
88 |
||
89 |
lemma imp_refl: "P-->P" |
|
90 |
by (rule impI, assumption) |
|
91 |
||
92 |
(*The quantifier monotonicity rules are also intuitionistically valid*) |
|
93 |
lemma ex_mono: "(!!x. P(x) --> Q(x)) ==> (EX x. P(x)) --> (EX x. Q(x))" |
|
94 |
by blast |
|
95 |
||
96 |
lemma all_mono: "(!!x. P(x) --> Q(x)) ==> (ALL x. P(x)) --> (ALL x. Q(x))" |
|
97 |
by blast |
|
98 |
||
11678 | 99 |
|
100 |
subsection {* Proof by cases and induction *} |
|
101 |
||
102 |
text {* Proper handling of non-atomic rule statements. *} |
|
103 |
||
104 |
constdefs |
|
18456 | 105 |
induct_forall where "induct_forall(P) == \<forall>x. P(x)" |
106 |
induct_implies where "induct_implies(A, B) == A \<longrightarrow> B" |
|
107 |
induct_equal where "induct_equal(x, y) == x = y" |
|
108 |
induct_conj where "induct_conj(A, B) == A \<and> B" |
|
11678 | 109 |
|
110 |
lemma induct_forall_eq: "(!!x. P(x)) == Trueprop(induct_forall(\<lambda>x. P(x)))" |
|
18456 | 111 |
by (unfold atomize_all induct_forall_def) |
11678 | 112 |
|
113 |
lemma induct_implies_eq: "(A ==> B) == Trueprop(induct_implies(A, B))" |
|
18456 | 114 |
by (unfold atomize_imp induct_implies_def) |
11678 | 115 |
|
116 |
lemma induct_equal_eq: "(x == y) == Trueprop(induct_equal(x, y))" |
|
18456 | 117 |
by (unfold atomize_eq induct_equal_def) |
11678 | 118 |
|
18456 | 119 |
lemma induct_conj_eq: |
120 |
includes meta_conjunction_syntax |
|
121 |
shows "(A && B) == Trueprop(induct_conj(A, B))" |
|
122 |
by (unfold atomize_conj induct_conj_def) |
|
11988 | 123 |
|
18456 | 124 |
lemmas induct_atomize = induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq |
125 |
lemmas induct_rulify [symmetric, standard] = induct_atomize |
|
126 |
lemmas induct_rulify_fallback = |
|
127 |
induct_forall_def induct_implies_def induct_equal_def induct_conj_def |
|
11678 | 128 |
|
18456 | 129 |
hide const induct_forall induct_implies induct_equal induct_conj |
11678 | 130 |
|
131 |
||
132 |
text {* Method setup. *} |
|
133 |
||
134 |
ML {* |
|
135 |
structure InductMethod = InductMethodFun |
|
136 |
(struct |
|
137 |
val cases_default = thm "case_split"; |
|
138 |
val atomize = thms "induct_atomize"; |
|
18456 | 139 |
val rulify = thms "induct_rulify"; |
140 |
val rulify_fallback = thms "induct_rulify_fallback"; |
|
11678 | 141 |
end); |
142 |
*} |
|
143 |
||
144 |
setup InductMethod.setup |
|
145 |
||
4854 | 146 |
end |