src/HOL/blastdata.ML
author nipkow
Wed Aug 18 11:09:40 2004 +0200 (2004-08-18)
changeset 15140 322485b816ac
parent 13550 5a176b8dda84
child 16774 515b6020cf5d
permissions -rw-r--r--
import -> imports
wenzelm@7357
     1
wenzelm@7357
     2
(*Better then ex1E for classical reasoner: needs no quantifier duplication!*)
wenzelm@7357
     3
val major::prems = goal (the_context ())
wenzelm@7357
     4
    "[| ?! x. P(x);                                              \
wenzelm@7357
     5
\       !!x. [| P(x);  ALL y y'. P(y) & P(y') --> y=y' |] ==> R  \
wenzelm@7357
     6
\    |] ==> R";
wenzelm@7357
     7
by (rtac (major RS ex1E) 1);
wenzelm@7357
     8
by (REPEAT (ares_tac (allI::prems) 1));
wenzelm@7357
     9
by (etac (dup_elim allE) 1);
wenzelm@7357
    10
by (Fast_tac 1);
wenzelm@7357
    11
qed "alt_ex1E";
wenzelm@7357
    12
wenzelm@7357
    13
AddSEs [alt_ex1E];
wenzelm@7357
    14
wenzelm@7357
    15
(*** Applying BlastFun to create Blast_tac ***)
wenzelm@7357
    16
structure Blast_Data = 
wenzelm@7357
    17
  struct
wenzelm@7357
    18
  type claset	= Classical.claset
wenzelm@7357
    19
  val notE	= notE
wenzelm@7357
    20
  val ccontr	= ccontr
wenzelm@7357
    21
  val contr_tac = Classical.contr_tac
wenzelm@7357
    22
  val dup_intr	= Classical.dup_intr
wenzelm@7357
    23
  val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
wenzelm@7357
    24
  val claset	= Classical.claset
wenzelm@7357
    25
  val rep_cs    = Classical.rep_cs
wenzelm@7357
    26
  val cla_modifiers = Classical.cla_modifiers;
wenzelm@7357
    27
  val cla_meth' = Classical.cla_meth'
wenzelm@7357
    28
  end;
wenzelm@7357
    29
wenzelm@7357
    30
structure Blast = BlastFun(Blast_Data);
wenzelm@7357
    31
wenzelm@7357
    32
val Blast_tac = Blast.Blast_tac
wenzelm@7357
    33
and blast_tac = Blast.blast_tac;