author wenzelm Mon, 02 Aug 1999 18:10:26 +0200 changeset 7156 3e84e73a3b6a parent 5929 890f2f9b926d child 7355 4c43090659ca permissions -rw-r--r--
fixed Blast_Data;
```
ID:         \$Id\$
Author:     Tobias Nipkow

Setting up the classical reasoner
*)

section "Classical Reasoner";

(*** Applying ClassicalFun to create a classical prover ***)
structure Classical_Data =
struct
val sizef     = size_of_thm
val mp        = mp
val not_elim  = notE
val classical = classical
val hyp_subst_tacs=[hyp_subst_tac]
end;

structure Cla = ClassicalFun(Classical_Data);
structure BasicClassical: BASIC_CLASSICAL = Cla;
open BasicClassical;

(*Better for fast_tac: needs no quantifier duplication!*)
qed_goal "alt_ex1E" IFOL.thy
"[| EX! x. P(x);                                              \
\       !!x. [| P(x);  ALL y y'. P(y) & P(y') --> y=y' |] ==> R  \
\    |] ==> R"
(fn major::prems =>
[ (rtac (major RS ex1E) 1),
(REPEAT (ares_tac (allI::prems) 1)),
(etac (dup_elim allE) 1),
(IntPr.fast_tac 1)]);

(*Propositional rules*)
val prop_cs = empty_cs addSIs [refl,TrueI,conjI,disjCI,impI,notI,iffI]

(*Quantifier rules*)

claset_ref() := FOL_cs;

(*** Applying BlastFun to create Blast_tac ***)
structure Blast_Data =
struct
type claset	= Cla.claset
val notE	= notE
val ccontr	= ccontr
val contr_tac = Cla.contr_tac
val dup_intr	= Cla.dup_intr
val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
val claset	= Cla.claset
val rep_cs    = Cla.rep_cs
val cla_modifiers = Cla.cla_modifiers;
val cla_meth' = Cla.cla_meth'
end;

structure Blast = BlastFun(Blast_Data);

val Blast_tac = Blast.Blast_tac
and blast_tac = Blast.blast_tac;
```