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