author paulson Wed, 20 Aug 2003 11:04:17 +0200 changeset 14156 2072802ab0e3 parent 13034 d7bb6e4f5f82 child 17876 b9c92f384109 permissions -rw-r--r--
new case_tac method
```
ID:         \$Id\$
Author:     Tobias Nipkow

Setting up the classical reasoner.
*)

section "Classical Reasoner";

(*** Applying Make_Elim_Fun to create a classical "make_elim" rule ***)
structure Make_Elim = Make_Elim_Fun(val classical = classical);

(*we don't redeclare the original make_elim (Tactic.make_elim) for
compatibility with strange things done in many existing proofs *)
val cla_make_elim = Make_Elim.make_elim;

(*** Applying ClassicalFun to create a classical prover ***)
structure Classical_Data =
struct
val make_elim = cla_make_elim
val mp        = mp
val not_elim  = notE
val classical = classical
val sizef     = size_of_thm
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]