src/HOL/blastdata.ML
author obua
Mon Apr 10 16:00:34 2006 +0200 (2006-04-10)
changeset 19404 9bf2cdc9e8e8
parent 18524 57b489b54914
child 20944 34b2c1bb7178
permissions -rw-r--r--
Moved stuff from Ring_and_Field to Matrix
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@18524
    19
  val equality_name = "op ="
wenzelm@18524
    20
  val not_name = "Not"
wenzelm@7357
    21
  val notE	= notE
wenzelm@7357
    22
  val ccontr	= ccontr
wenzelm@7357
    23
  val contr_tac = Classical.contr_tac
wenzelm@7357
    24
  val dup_intr	= Classical.dup_intr
wenzelm@7357
    25
  val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
wenzelm@7357
    26
  val claset	= Classical.claset
wenzelm@7357
    27
  val rep_cs    = Classical.rep_cs
wenzelm@7357
    28
  val cla_modifiers = Classical.cla_modifiers;
wenzelm@7357
    29
  val cla_meth' = Classical.cla_meth'
wenzelm@7357
    30
  end;
wenzelm@7357
    31
wenzelm@7357
    32
structure Blast = BlastFun(Blast_Data);
wenzelm@7357
    33
wenzelm@7357
    34
val Blast_tac = Blast.Blast_tac
wenzelm@7357
    35
and blast_tac = Blast.blast_tac;