author | wenzelm |
Tue, 31 Jan 2023 19:27:02 +0100 | |
changeset 77157 | c0633a0da53e |
parent 74563 | 042041c0ebeb |
child 80701 | 39cd50407f79 |
permissions | -rw-r--r-- |
9487 | 1 |
(* Title: FOL/FOL.thy |
2 |
Author: Lawrence C Paulson and Markus Wenzel |
|
11678 | 3 |
*) |
9487 | 4 |
|
60770 | 5 |
section \<open>Classical first-order logic\<close> |
4093 | 6 |
|
18456 | 7 |
theory FOL |
73015 | 8 |
imports IFOL |
9 |
keywords "print_claset" "print_induct_rules" :: diag |
|
18456 | 10 |
begin |
9487 | 11 |
|
69605 | 12 |
ML_file \<open>~~/src/Provers/classical.ML\<close> |
13 |
ML_file \<open>~~/src/Provers/blast.ML\<close> |
|
14 |
ML_file \<open>~~/src/Provers/clasimp.ML\<close> |
|
48891 | 15 |
|
9487 | 16 |
|
60770 | 17 |
subsection \<open>The classical axiom\<close> |
4093 | 18 |
|
41779 | 19 |
axiomatization where |
69590 | 20 |
classical: \<open>(\<not> P \<Longrightarrow> P) \<Longrightarrow> P\<close> |
4093 | 21 |
|
9487 | 22 |
|
60770 | 23 |
subsection \<open>Lemmas and proof tools\<close> |
9487 | 24 |
|
69590 | 25 |
lemma ccontr: \<open>(\<not> P \<Longrightarrow> False) \<Longrightarrow> P\<close> |
21539 | 26 |
by (erule FalseE [THEN classical]) |
27 |
||
28 |
||
62020 | 29 |
subsubsection \<open>Classical introduction rules for \<open>\<or>\<close> and \<open>\<exists>\<close>\<close> |
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
60770
diff
changeset
|
30 |
|
69590 | 31 |
lemma disjCI: \<open>(\<not> Q \<Longrightarrow> P) \<Longrightarrow> P \<or> Q\<close> |
21539 | 32 |
apply (rule classical) |
33 |
apply (assumption | erule meta_mp | rule disjI1 notI)+ |
|
34 |
apply (erule notE disjI2)+ |
|
35 |
done |
|
36 |
||
62020 | 37 |
text \<open>Introduction rule involving only \<open>\<exists>\<close>\<close> |
21539 | 38 |
lemma ex_classical: |
69590 | 39 |
assumes r: \<open>\<not> (\<exists>x. P(x)) \<Longrightarrow> P(a)\<close> |
40 |
shows \<open>\<exists>x. P(x)\<close> |
|
21539 | 41 |
apply (rule classical) |
42 |
apply (rule exI, erule r) |
|
43 |
done |
|
44 |
||
62020 | 45 |
text \<open>Version of above, simplifying \<open>\<not>\<exists>\<close> to \<open>\<forall>\<not>\<close>.\<close> |
21539 | 46 |
lemma exCI: |
69590 | 47 |
assumes r: \<open>\<forall>x. \<not> P(x) \<Longrightarrow> P(a)\<close> |
48 |
shows \<open>\<exists>x. P(x)\<close> |
|
21539 | 49 |
apply (rule ex_classical) |
50 |
apply (rule notI [THEN allI, THEN r]) |
|
51 |
apply (erule notE) |
|
52 |
apply (erule exI) |
|
53 |
done |
|
54 |
||
69590 | 55 |
lemma excluded_middle: \<open>\<not> P \<or> P\<close> |
21539 | 56 |
apply (rule disjCI) |
57 |
apply assumption |
|
58 |
done |
|
59 |
||
27115
0dcafa5c9e3f
eliminated obsolete case_split_thm -- use case_split;
wenzelm
parents:
26496
diff
changeset
|
60 |
lemma case_split [case_names True False]: |
69590 | 61 |
assumes r1: \<open>P \<Longrightarrow> Q\<close> |
62 |
and r2: \<open>\<not> P \<Longrightarrow> Q\<close> |
|
63 |
shows \<open>Q\<close> |
|
21539 | 64 |
apply (rule excluded_middle [THEN disjE]) |
65 |
apply (erule r2) |
|
66 |
apply (erule r1) |
|
67 |
done |
|
68 |
||
60770 | 69 |
ML \<open> |
59780 | 70 |
fun case_tac ctxt a fixes = |
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
60770
diff
changeset
|
71 |
Rule_Insts.res_inst_tac ctxt [((("P", 0), Position.none), a)] fixes @{thm case_split}; |
60770 | 72 |
\<close> |
21539 | 73 |
|
60770 | 74 |
method_setup case_tac = \<open> |
74563 | 75 |
Args.goal_spec -- Scan.lift (Parse.embedded_inner_syntax -- Parse.for_fixes) >> |
59780 | 76 |
(fn (quant, (s, fixes)) => fn ctxt => SIMPLE_METHOD'' quant (case_tac ctxt s fixes)) |
60770 | 77 |
\<close> "case_tac emulation (dynamic instantiation!)" |
27211 | 78 |
|
21539 | 79 |
|
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
60770
diff
changeset
|
80 |
subsection \<open>Special elimination rules\<close> |
21539 | 81 |
|
62020 | 82 |
text \<open>Classical implies (\<open>\<longrightarrow>\<close>) elimination.\<close> |
21539 | 83 |
lemma impCE: |
69590 | 84 |
assumes major: \<open>P \<longrightarrow> Q\<close> |
85 |
and r1: \<open>\<not> P \<Longrightarrow> R\<close> |
|
86 |
and r2: \<open>Q \<Longrightarrow> R\<close> |
|
87 |
shows \<open>R\<close> |
|
21539 | 88 |
apply (rule excluded_middle [THEN disjE]) |
89 |
apply (erule r1) |
|
90 |
apply (rule r2) |
|
91 |
apply (erule major [THEN mp]) |
|
92 |
done |
|
93 |
||
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
60770
diff
changeset
|
94 |
text \<open> |
62020 | 95 |
This version of \<open>\<longrightarrow>\<close> elimination works on \<open>Q\<close> before \<open>P\<close>. It works best for those cases in which P holds ``almost everywhere''. |
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
60770
diff
changeset
|
96 |
Can't install as default: would break old proofs. |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
60770
diff
changeset
|
97 |
\<close> |
21539 | 98 |
lemma impCE': |
69590 | 99 |
assumes major: \<open>P \<longrightarrow> Q\<close> |
100 |
and r1: \<open>Q \<Longrightarrow> R\<close> |
|
101 |
and r2: \<open>\<not> P \<Longrightarrow> R\<close> |
|
102 |
shows \<open>R\<close> |
|
21539 | 103 |
apply (rule excluded_middle [THEN disjE]) |
104 |
apply (erule r2) |
|
105 |
apply (rule r1) |
|
106 |
apply (erule major [THEN mp]) |
|
107 |
done |
|
108 |
||
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
60770
diff
changeset
|
109 |
text \<open>Double negation law.\<close> |
69590 | 110 |
lemma notnotD: \<open>\<not> \<not> P \<Longrightarrow> P\<close> |
21539 | 111 |
apply (rule classical) |
112 |
apply (erule notE) |
|
113 |
apply assumption |
|
114 |
done |
|
115 |
||
69590 | 116 |
lemma contrapos2: \<open>\<lbrakk>Q; \<not> P \<Longrightarrow> \<not> Q\<rbrakk> \<Longrightarrow> P\<close> |
21539 | 117 |
apply (rule classical) |
118 |
apply (drule (1) meta_mp) |
|
119 |
apply (erule (1) notE) |
|
120 |
done |
|
121 |
||
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
60770
diff
changeset
|
122 |
|
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
60770
diff
changeset
|
123 |
subsubsection \<open>Tactics for implication and contradiction\<close> |
21539 | 124 |
|
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
60770
diff
changeset
|
125 |
text \<open> |
62020 | 126 |
Classical \<open>\<longleftrightarrow>\<close> elimination. Proof substitutes \<open>P = Q\<close> in |
127 |
\<open>\<not> P \<Longrightarrow> \<not> Q\<close> and \<open>P \<Longrightarrow> Q\<close>. |
|
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
60770
diff
changeset
|
128 |
\<close> |
21539 | 129 |
lemma iffCE: |
69590 | 130 |
assumes major: \<open>P \<longleftrightarrow> Q\<close> |
131 |
and r1: \<open>\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> R\<close> |
|
132 |
and r2: \<open>\<lbrakk>\<not> P; \<not> Q\<rbrakk> \<Longrightarrow> R\<close> |
|
133 |
shows \<open>R\<close> |
|
21539 | 134 |
apply (rule major [unfolded iff_def, THEN conjE]) |
135 |
apply (elim impCE) |
|
136 |
apply (erule (1) r2) |
|
137 |
apply (erule (1) notE)+ |
|
138 |
apply (erule (1) r1) |
|
139 |
done |
|
140 |
||
141 |
||
142 |
(*Better for fast_tac: needs no quantifier duplication!*) |
|
143 |
lemma alt_ex1E: |
|
69590 | 144 |
assumes major: \<open>\<exists>! x. P(x)\<close> |
145 |
and r: \<open>\<And>x. \<lbrakk>P(x); \<forall>y y'. P(y) \<and> P(y') \<longrightarrow> y = y'\<rbrakk> \<Longrightarrow> R\<close> |
|
146 |
shows \<open>R\<close> |
|
21539 | 147 |
using major |
148 |
proof (rule ex1E) |
|
149 |
fix x |
|
69590 | 150 |
assume * : \<open>\<forall>y. P(y) \<longrightarrow> y = x\<close> |
151 |
assume \<open>P(x)\<close> |
|
152 |
then show \<open>R\<close> |
|
21539 | 153 |
proof (rule r) |
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
60770
diff
changeset
|
154 |
{ |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
60770
diff
changeset
|
155 |
fix y y' |
69590 | 156 |
assume \<open>P(y)\<close> and \<open>P(y')\<close> |
157 |
with * have \<open>x = y\<close> and \<open>x = y'\<close> |
|
69593 | 158 |
by - (tactic "IntPr.fast_tac \<^context> 1")+ |
69590 | 159 |
then have \<open>y = y'\<close> by (rule subst) |
21539 | 160 |
} note r' = this |
69590 | 161 |
show \<open>\<forall>y y'. P(y) \<and> P(y') \<longrightarrow> y = y'\<close> |
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
60770
diff
changeset
|
162 |
by (intro strip, elim conjE) (rule r') |
21539 | 163 |
qed |
164 |
qed |
|
9525 | 165 |
|
69590 | 166 |
lemma imp_elim: \<open>P \<longrightarrow> Q \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R\<close> |
26411 | 167 |
by (rule classical) iprover |
168 |
||
69590 | 169 |
lemma swap: \<open>\<not> P \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> R\<close> |
26411 | 170 |
by (rule classical) iprover |
171 |
||
27849 | 172 |
|
60770 | 173 |
section \<open>Classical Reasoner\<close> |
27849 | 174 |
|
60770 | 175 |
ML \<open> |
42799 | 176 |
structure Cla = Classical |
42793 | 177 |
( |
178 |
val imp_elim = @{thm imp_elim} |
|
179 |
val not_elim = @{thm notE} |
|
180 |
val swap = @{thm swap} |
|
181 |
val classical = @{thm classical} |
|
182 |
val sizef = size_of_thm |
|
183 |
val hyp_subst_tacs = [hyp_subst_tac] |
|
184 |
); |
|
185 |
||
186 |
structure Basic_Classical: BASIC_CLASSICAL = Cla; |
|
187 |
open Basic_Classical; |
|
60770 | 188 |
\<close> |
42793 | 189 |
|
190 |
(*Propositional rules*) |
|
191 |
lemmas [intro!] = refl TrueI conjI disjCI impI notI iffI |
|
192 |
and [elim!] = conjE disjE impCE FalseE iffCE |
|
69593 | 193 |
ML \<open>val prop_cs = claset_of \<^context>\<close> |
42793 | 194 |
|
195 |
(*Quantifier rules*) |
|
196 |
lemmas [intro!] = allI ex_ex1I |
|
197 |
and [intro] = exI |
|
198 |
and [elim!] = exE alt_ex1E |
|
199 |
and [elim] = allE |
|
69593 | 200 |
ML \<open>val FOL_cs = claset_of \<^context>\<close> |
10383 | 201 |
|
60770 | 202 |
ML \<open> |
32176
893614e2c35c
renamed functor BlastFun to Blast, require explicit theory;
wenzelm
parents:
32171
diff
changeset
|
203 |
structure Blast = Blast |
893614e2c35c
renamed functor BlastFun to Blast, require explicit theory;
wenzelm
parents:
32171
diff
changeset
|
204 |
( |
42477 | 205 |
structure Classical = Cla |
74300 | 206 |
val Trueprop_const = dest_Const \<^Const>\<open>Trueprop\<close> |
69593 | 207 |
val equality_name = \<^const_name>\<open>eq\<close> |
208 |
val not_name = \<^const_name>\<open>Not\<close> |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32261
diff
changeset
|
209 |
val notE = @{thm notE} |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32261
diff
changeset
|
210 |
val ccontr = @{thm ccontr} |
32176
893614e2c35c
renamed functor BlastFun to Blast, require explicit theory;
wenzelm
parents:
32171
diff
changeset
|
211 |
val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac |
893614e2c35c
renamed functor BlastFun to Blast, require explicit theory;
wenzelm
parents:
32171
diff
changeset
|
212 |
); |
893614e2c35c
renamed functor BlastFun to Blast, require explicit theory;
wenzelm
parents:
32171
diff
changeset
|
213 |
val blast_tac = Blast.blast_tac; |
60770 | 214 |
\<close> |
32176
893614e2c35c
renamed functor BlastFun to Blast, require explicit theory;
wenzelm
parents:
32171
diff
changeset
|
215 |
|
13550 | 216 |
|
69590 | 217 |
lemma ex1_functional: \<open>\<lbrakk>\<exists>! z. P(a,z); P(a,b); P(a,c)\<rbrakk> \<Longrightarrow> b = c\<close> |
21539 | 218 |
by blast |
20223 | 219 |
|
62020 | 220 |
text \<open>Elimination of \<open>True\<close> from assumptions:\<close> |
69590 | 221 |
lemma True_implies_equals: \<open>(True \<Longrightarrow> PROP P) \<equiv> PROP P\<close> |
20223 | 222 |
proof |
69590 | 223 |
assume \<open>True \<Longrightarrow> PROP P\<close> |
224 |
from this and TrueI show \<open>PROP P\<close> . |
|
20223 | 225 |
next |
69590 | 226 |
assume \<open>PROP P\<close> |
227 |
then show \<open>PROP P\<close> . |
|
20223 | 228 |
qed |
9487 | 229 |
|
69590 | 230 |
lemma uncurry: \<open>P \<longrightarrow> Q \<longrightarrow> R \<Longrightarrow> P \<and> Q \<longrightarrow> R\<close> |
21539 | 231 |
by blast |
232 |
||
69590 | 233 |
lemma iff_allI: \<open>(\<And>x. P(x) \<longleftrightarrow> Q(x)) \<Longrightarrow> (\<forall>x. P(x)) \<longleftrightarrow> (\<forall>x. Q(x))\<close> |
21539 | 234 |
by blast |
235 |
||
69590 | 236 |
lemma iff_exI: \<open>(\<And>x. P(x) \<longleftrightarrow> Q(x)) \<Longrightarrow> (\<exists>x. P(x)) \<longleftrightarrow> (\<exists>x. Q(x))\<close> |
21539 | 237 |
by blast |
238 |
||
69590 | 239 |
lemma all_comm: \<open>(\<forall>x y. P(x,y)) \<longleftrightarrow> (\<forall>y x. P(x,y))\<close> |
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
60770
diff
changeset
|
240 |
by blast |
21539 | 241 |
|
69590 | 242 |
lemma ex_comm: \<open>(\<exists>x y. P(x,y)) \<longleftrightarrow> (\<exists>y x. P(x,y))\<close> |
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
60770
diff
changeset
|
243 |
by blast |
21539 | 244 |
|
26286 | 245 |
|
246 |
||
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
60770
diff
changeset
|
247 |
subsection \<open>Classical simplification rules\<close> |
26286 | 248 |
|
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
60770
diff
changeset
|
249 |
text \<open> |
62020 | 250 |
Avoids duplication of subgoals after \<open>expand_if\<close>, when the true and |
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
60770
diff
changeset
|
251 |
false cases boil down to the same thing. |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
60770
diff
changeset
|
252 |
\<close> |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
60770
diff
changeset
|
253 |
|
69590 | 254 |
lemma cases_simp: \<open>(P \<longrightarrow> Q) \<and> (\<not> P \<longrightarrow> Q) \<longleftrightarrow> Q\<close> |
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
60770
diff
changeset
|
255 |
by blast |
26286 | 256 |
|
257 |
||
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
60770
diff
changeset
|
258 |
subsubsection \<open>Miniscoping: pushing quantifiers in\<close> |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
60770
diff
changeset
|
259 |
|
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
60770
diff
changeset
|
260 |
text \<open> |
62020 | 261 |
We do NOT distribute of \<open>\<forall>\<close> over \<open>\<and>\<close>, or dually that of |
262 |
\<open>\<exists>\<close> over \<open>\<or>\<close>. |
|
26286 | 263 |
|
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
60770
diff
changeset
|
264 |
Baaz and Leitsch, On Skolemization and Proof Complexity (1994) show that |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
60770
diff
changeset
|
265 |
this step can increase proof length! |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
60770
diff
changeset
|
266 |
\<close> |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
60770
diff
changeset
|
267 |
|
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
60770
diff
changeset
|
268 |
text \<open>Existential miniscoping.\<close> |
26286 | 269 |
lemma int_ex_simps: |
69590 | 270 |
\<open>\<And>P Q. (\<exists>x. P(x) \<and> Q) \<longleftrightarrow> (\<exists>x. P(x)) \<and> Q\<close> |
271 |
\<open>\<And>P Q. (\<exists>x. P \<and> Q(x)) \<longleftrightarrow> P \<and> (\<exists>x. Q(x))\<close> |
|
272 |
\<open>\<And>P Q. (\<exists>x. P(x) \<or> Q) \<longleftrightarrow> (\<exists>x. P(x)) \<or> Q\<close> |
|
273 |
\<open>\<And>P Q. (\<exists>x. P \<or> Q(x)) \<longleftrightarrow> P \<or> (\<exists>x. Q(x))\<close> |
|
26286 | 274 |
by iprover+ |
275 |
||
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
60770
diff
changeset
|
276 |
text \<open>Classical rules.\<close> |
26286 | 277 |
lemma cla_ex_simps: |
69590 | 278 |
\<open>\<And>P Q. (\<exists>x. P(x) \<longrightarrow> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<longrightarrow> Q\<close> |
279 |
\<open>\<And>P Q. (\<exists>x. P \<longrightarrow> Q(x)) \<longleftrightarrow> P \<longrightarrow> (\<exists>x. Q(x))\<close> |
|
26286 | 280 |
by blast+ |
281 |
||
282 |
lemmas ex_simps = int_ex_simps cla_ex_simps |
|
283 |
||
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
60770
diff
changeset
|
284 |
text \<open>Universal miniscoping.\<close> |
26286 | 285 |
lemma int_all_simps: |
69590 | 286 |
\<open>\<And>P Q. (\<forall>x. P(x) \<and> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<and> Q\<close> |
287 |
\<open>\<And>P Q. (\<forall>x. P \<and> Q(x)) \<longleftrightarrow> P \<and> (\<forall>x. Q(x))\<close> |
|
288 |
\<open>\<And>P Q. (\<forall>x. P(x) \<longrightarrow> Q) \<longleftrightarrow> (\<exists> x. P(x)) \<longrightarrow> Q\<close> |
|
289 |
\<open>\<And>P Q. (\<forall>x. P \<longrightarrow> Q(x)) \<longleftrightarrow> P \<longrightarrow> (\<forall>x. Q(x))\<close> |
|
26286 | 290 |
by iprover+ |
291 |
||
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
60770
diff
changeset
|
292 |
text \<open>Classical rules.\<close> |
26286 | 293 |
lemma cla_all_simps: |
69590 | 294 |
\<open>\<And>P Q. (\<forall>x. P(x) \<or> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<or> Q\<close> |
295 |
\<open>\<And>P Q. (\<forall>x. P \<or> Q(x)) \<longleftrightarrow> P \<or> (\<forall>x. Q(x))\<close> |
|
26286 | 296 |
by blast+ |
297 |
||
298 |
lemmas all_simps = int_all_simps cla_all_simps |
|
299 |
||
300 |
||
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
60770
diff
changeset
|
301 |
subsubsection \<open>Named rewrite rules proved for IFOL\<close> |
26286 | 302 |
|
69590 | 303 |
lemma imp_disj1: \<open>(P \<longrightarrow> Q) \<or> R \<longleftrightarrow> (P \<longrightarrow> Q \<or> R)\<close> by blast |
304 |
lemma imp_disj2: \<open>Q \<or> (P \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> Q \<or> R)\<close> by blast |
|
26286 | 305 |
|
69590 | 306 |
lemma de_Morgan_conj: \<open>(\<not> (P \<and> Q)) \<longleftrightarrow> (\<not> P \<or> \<not> Q)\<close> by blast |
26286 | 307 |
|
69590 | 308 |
lemma not_imp: \<open>\<not> (P \<longrightarrow> Q) \<longleftrightarrow> (P \<and> \<not> Q)\<close> by blast |
309 |
lemma not_iff: \<open>\<not> (P \<longleftrightarrow> Q) \<longleftrightarrow> (P \<longleftrightarrow> \<not> Q)\<close> by blast |
|
26286 | 310 |
|
69590 | 311 |
lemma not_all: \<open>(\<not> (\<forall>x. P(x))) \<longleftrightarrow> (\<exists>x. \<not> P(x))\<close> by blast |
312 |
lemma imp_all: \<open>((\<forall>x. P(x)) \<longrightarrow> Q) \<longleftrightarrow> (\<exists>x. P(x) \<longrightarrow> Q)\<close> by blast |
|
26286 | 313 |
|
314 |
||
315 |
lemmas meta_simps = |
|
62020 | 316 |
triv_forall_equality \<comment> \<open>prunes params\<close> |
317 |
True_implies_equals \<comment> \<open>prune asms \<open>True\<close>\<close> |
|
26286 | 318 |
|
319 |
lemmas IFOL_simps = |
|
320 |
refl [THEN P_iff_T] conj_simps disj_simps not_simps |
|
321 |
imp_simps iff_simps quant_simps |
|
322 |
||
69590 | 323 |
lemma notFalseI: \<open>\<not> False\<close> by iprover |
26286 | 324 |
|
325 |
lemma cla_simps_misc: |
|
69590 | 326 |
\<open>\<not> (P \<and> Q) \<longleftrightarrow> \<not> P \<or> \<not> Q\<close> |
327 |
\<open>P \<or> \<not> P\<close> |
|
328 |
\<open>\<not> P \<or> P\<close> |
|
329 |
\<open>\<not> \<not> P \<longleftrightarrow> P\<close> |
|
330 |
\<open>(\<not> P \<longrightarrow> P) \<longleftrightarrow> P\<close> |
|
331 |
\<open>(\<not> P \<longleftrightarrow> \<not> Q) \<longleftrightarrow> (P \<longleftrightarrow> Q)\<close> by blast+ |
|
26286 | 332 |
|
333 |
lemmas cla_simps = |
|
334 |
de_Morgan_conj de_Morgan_disj imp_disj1 imp_disj2 |
|
335 |
not_imp not_all not_ex cases_simp cla_simps_misc |
|
336 |
||
337 |
||
69605 | 338 |
ML_file \<open>simpdata.ML\<close> |
42455 | 339 |
|
71920 | 340 |
simproc_setup defined_Ex (\<open>\<exists>x. P(x)\<close>) = \<open>K Quantifier1.rearrange_Ex\<close> |
341 |
simproc_setup defined_All (\<open>\<forall>x. P(x)\<close>) = \<open>K Quantifier1.rearrange_All\<close> |
|
342 |
simproc_setup defined_all("\<And>x. PROP P(x)") = \<open>K Quantifier1.rearrange_all\<close> |
|
42455 | 343 |
|
60770 | 344 |
ML \<open> |
42453 | 345 |
(*intuitionistic simprules only*) |
346 |
val IFOL_ss = |
|
69593 | 347 |
put_simpset FOL_basic_ss \<^context> |
71959 | 348 |
addsimps @{thms meta_simps IFOL_simps int_ex_simps int_all_simps subst_all} |
69593 | 349 |
addsimprocs [\<^simproc>\<open>defined_All\<close>, \<^simproc>\<open>defined_Ex\<close>] |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51687
diff
changeset
|
350 |
|> Simplifier.add_cong @{thm imp_cong} |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51687
diff
changeset
|
351 |
|> simpset_of; |
42453 | 352 |
|
353 |
(*classical simprules too*) |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51687
diff
changeset
|
354 |
val FOL_ss = |
69593 | 355 |
put_simpset IFOL_ss \<^context> |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51687
diff
changeset
|
356 |
addsimps @{thms cla_simps cla_ex_simps cla_all_simps} |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51687
diff
changeset
|
357 |
|> simpset_of; |
60770 | 358 |
\<close> |
42453 | 359 |
|
60770 | 360 |
setup \<open> |
58826 | 361 |
map_theory_simpset (put_simpset FOL_ss) #> |
362 |
Simplifier.method_setup Splitter.split_modifiers |
|
60770 | 363 |
\<close> |
52241 | 364 |
|
69605 | 365 |
ML_file \<open>~~/src/Tools/eqsubst.ML\<close> |
15481 | 366 |
|
367 |
||
60770 | 368 |
subsection \<open>Other simple lemmas\<close> |
14085 | 369 |
|
69590 | 370 |
lemma [simp]: \<open>((P \<longrightarrow> R) \<longleftrightarrow> (Q \<longrightarrow> R)) \<longleftrightarrow> ((P \<longleftrightarrow> Q) \<or> R)\<close> |
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
60770
diff
changeset
|
371 |
by blast |
14085 | 372 |
|
69590 | 373 |
lemma [simp]: \<open>((P \<longrightarrow> Q) \<longleftrightarrow> (P \<longrightarrow> R)) \<longleftrightarrow> (P \<longrightarrow> (Q \<longleftrightarrow> R))\<close> |
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
60770
diff
changeset
|
374 |
by blast |
14085 | 375 |
|
69590 | 376 |
lemma not_disj_iff_imp: \<open>\<not> P \<or> Q \<longleftrightarrow> (P \<longrightarrow> Q)\<close> |
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
60770
diff
changeset
|
377 |
by blast |
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
60770
diff
changeset
|
378 |
|
14085 | 379 |
|
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
60770
diff
changeset
|
380 |
subsubsection \<open>Monotonicity of implications\<close> |
14085 | 381 |
|
69590 | 382 |
lemma conj_mono: \<open>\<lbrakk>P1 \<longrightarrow> Q1; P2 \<longrightarrow> Q2\<rbrakk> \<Longrightarrow> (P1 \<and> P2) \<longrightarrow> (Q1 \<and> Q2)\<close> |
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
60770
diff
changeset
|
383 |
by fast (*or (IntPr.fast_tac 1)*) |
14085 | 384 |
|
69590 | 385 |
lemma disj_mono: \<open>\<lbrakk>P1 \<longrightarrow> Q1; P2 \<longrightarrow> Q2\<rbrakk> \<Longrightarrow> (P1 \<or> P2) \<longrightarrow> (Q1 \<or> Q2)\<close> |
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
60770
diff
changeset
|
386 |
by fast (*or (IntPr.fast_tac 1)*) |
14085 | 387 |
|
69590 | 388 |
lemma imp_mono: \<open>\<lbrakk>Q1 \<longrightarrow> P1; P2 \<longrightarrow> Q2\<rbrakk> \<Longrightarrow> (P1 \<longrightarrow> P2) \<longrightarrow> (Q1 \<longrightarrow> Q2)\<close> |
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
60770
diff
changeset
|
389 |
by fast (*or (IntPr.fast_tac 1)*) |
14085 | 390 |
|
69590 | 391 |
lemma imp_refl: \<open>P \<longrightarrow> P\<close> |
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
60770
diff
changeset
|
392 |
by (rule impI) |
14085 | 393 |
|
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
60770
diff
changeset
|
394 |
text \<open>The quantifier monotonicity rules are also intuitionistically valid.\<close> |
69590 | 395 |
lemma ex_mono: \<open>(\<And>x. P(x) \<longrightarrow> Q(x)) \<Longrightarrow> (\<exists>x. P(x)) \<longrightarrow> (\<exists>x. Q(x))\<close> |
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
60770
diff
changeset
|
396 |
by blast |
14085 | 397 |
|
69590 | 398 |
lemma all_mono: \<open>(\<And>x. P(x) \<longrightarrow> Q(x)) \<Longrightarrow> (\<forall>x. P(x)) \<longrightarrow> (\<forall>x. Q(x))\<close> |
61487
f8cb97e0fd0b
more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;
wenzelm
parents:
60770
diff
changeset
|
399 |
by blast |
14085 | 400 |
|
11678 | 401 |
|
60770 | 402 |
subsection \<open>Proof by cases and induction\<close> |
11678 | 403 |
|
60770 | 404 |
text \<open>Proper handling of non-atomic rule statements.\<close> |
11678 | 405 |
|
59940
087d81f5213e
local setup of induction tools, with restricted access to auxiliary consts;
wenzelm
parents:
59780
diff
changeset
|
406 |
context |
087d81f5213e
local setup of induction tools, with restricted access to auxiliary consts;
wenzelm
parents:
59780
diff
changeset
|
407 |
begin |
087d81f5213e
local setup of induction tools, with restricted access to auxiliary consts;
wenzelm
parents:
59780
diff
changeset
|
408 |
|
69590 | 409 |
qualified definition \<open>induct_forall(P) \<equiv> \<forall>x. P(x)\<close> |
410 |
qualified definition \<open>induct_implies(A, B) \<equiv> A \<longrightarrow> B\<close> |
|
411 |
qualified definition \<open>induct_equal(x, y) \<equiv> x = y\<close> |
|
412 |
qualified definition \<open>induct_conj(A, B) \<equiv> A \<and> B\<close> |
|
11678 | 413 |
|
69590 | 414 |
lemma induct_forall_eq: \<open>(\<And>x. P(x)) \<equiv> Trueprop(induct_forall(\<lambda>x. P(x)))\<close> |
18816 | 415 |
unfolding atomize_all induct_forall_def . |
11678 | 416 |
|
69590 | 417 |
lemma induct_implies_eq: \<open>(A \<Longrightarrow> B) \<equiv> Trueprop(induct_implies(A, B))\<close> |
18816 | 418 |
unfolding atomize_imp induct_implies_def . |
11678 | 419 |
|
69590 | 420 |
lemma induct_equal_eq: \<open>(x \<equiv> y) \<equiv> Trueprop(induct_equal(x, y))\<close> |
18816 | 421 |
unfolding atomize_eq induct_equal_def . |
11678 | 422 |
|
69590 | 423 |
lemma induct_conj_eq: \<open>(A &&& B) \<equiv> Trueprop(induct_conj(A, B))\<close> |
18816 | 424 |
unfolding atomize_conj induct_conj_def . |
11988 | 425 |
|
18456 | 426 |
lemmas induct_atomize = induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq |
45594 | 427 |
lemmas induct_rulify [symmetric] = induct_atomize |
18456 | 428 |
lemmas induct_rulify_fallback = |
429 |
induct_forall_def induct_implies_def induct_equal_def induct_conj_def |
|
11678 | 430 |
|
60770 | 431 |
text \<open>Method setup.\<close> |
11678 | 432 |
|
69605 | 433 |
ML_file \<open>~~/src/Tools/induct.ML\<close> |
60770 | 434 |
ML \<open> |
32171 | 435 |
structure Induct = Induct |
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
24097
diff
changeset
|
436 |
( |
22139 | 437 |
val cases_default = @{thm case_split} |
438 |
val atomize = @{thms induct_atomize} |
|
439 |
val rulify = @{thms induct_rulify} |
|
440 |
val rulify_fallback = @{thms induct_rulify_fallback} |
|
34989 | 441 |
val equal_def = @{thm induct_equal_def} |
34914 | 442 |
fun dest_def _ = NONE |
58957 | 443 |
fun trivial_tac _ _ = no_tac |
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
24097
diff
changeset
|
444 |
); |
60770 | 445 |
\<close> |
11678 | 446 |
|
24830
a7b3ab44d993
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
wenzelm
parents:
24097
diff
changeset
|
447 |
declare case_split [cases type: o] |
11678 | 448 |
|
59940
087d81f5213e
local setup of induction tools, with restricted access to auxiliary consts;
wenzelm
parents:
59780
diff
changeset
|
449 |
end |
087d81f5213e
local setup of induction tools, with restricted access to auxiliary consts;
wenzelm
parents:
59780
diff
changeset
|
450 |
|
69605 | 451 |
ML_file \<open>~~/src/Tools/case_product.ML\<close> |
41827 | 452 |
|
41310 | 453 |
|
454 |
hide_const (open) eq |
|
455 |
||
4854 | 456 |
end |