author | wenzelm |
Tue, 01 Aug 2000 11:57:09 +0200 | |
changeset 9486 | 2df511ebb956 |
parent 7357 | d0e16da40ea2 |
child 9530 | f0ffd29fd4e4 |
permissions | -rw-r--r-- |
7357 | 1 |
|
2 |
(*Better then ex1E for classical reasoner: needs no quantifier duplication!*) |
|
3 |
val major::prems = goal (the_context ()) |
|
4 |
"[| ?! x. P(x); \ |
|
5 |
\ !!x. [| P(x); ALL y y'. P(y) & P(y') --> y=y' |] ==> R \ |
|
6 |
\ |] ==> R"; |
|
7 |
by (rtac (major RS ex1E) 1); |
|
8 |
by (REPEAT (ares_tac (allI::prems) 1)); |
|
9 |
by (etac (dup_elim allE) 1); |
|
10 |
by (Fast_tac 1); |
|
11 |
qed "alt_ex1E"; |
|
12 |
||
13 |
AddSEs [alt_ex1E]; |
|
14 |
||
15 |
(*** Applying BlastFun to create Blast_tac ***) |
|
16 |
structure Blast_Data = |
|
17 |
struct |
|
18 |
type claset = Classical.claset |
|
19 |
val notE = notE |
|
20 |
val ccontr = ccontr |
|
21 |
val contr_tac = Classical.contr_tac |
|
22 |
val dup_intr = Classical.dup_intr |
|
23 |
val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac |
|
24 |
val claset = Classical.claset |
|
25 |
val rep_cs = Classical.rep_cs |
|
9486
2df511ebb956
handle actual object-logic rules by atomizing the goal;
wenzelm
parents:
7357
diff
changeset
|
26 |
val atomize = [thm "all_eq", thm "imp_eq"] |
7357 | 27 |
val cla_modifiers = Classical.cla_modifiers; |
28 |
val cla_meth' = Classical.cla_meth' |
|
29 |
end; |
|
30 |
||
31 |
structure Blast = BlastFun(Blast_Data); |
|
32 |
Blast.overloaded ("op =", domain_type); (*overloading of equality as iff*) |
|
33 |
||
34 |
val Blast_tac = Blast.Blast_tac |
|
35 |
and blast_tac = Blast.blast_tac; |