src/HOL/blastdata.ML
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 10429 8820f787e61e
child 10906 de95ba2760fe
permissions -rw-r--r--
hide many names from Datatype_Universe.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
7357
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents:
diff changeset
     1
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents:
diff changeset
     2
(*Better then ex1E for classical reasoner: needs no quantifier duplication!*)
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents:
diff changeset
     3
val major::prems = goal (the_context ())
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents:
diff changeset
     4
    "[| ?! x. P(x);                                              \
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents:
diff changeset
     5
\       !!x. [| P(x);  ALL y y'. P(y) & P(y') --> y=y' |] ==> R  \
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents:
diff changeset
     6
\    |] ==> R";
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents:
diff changeset
     7
by (rtac (major RS ex1E) 1);
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents:
diff changeset
     8
by (REPEAT (ares_tac (allI::prems) 1));
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents:
diff changeset
     9
by (etac (dup_elim allE) 1);
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents:
diff changeset
    10
by (Fast_tac 1);
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents:
diff changeset
    11
qed "alt_ex1E";
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents:
diff changeset
    12
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents:
diff changeset
    13
AddSEs [alt_ex1E];
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents:
diff changeset
    14
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents:
diff changeset
    15
(*** Applying BlastFun to create Blast_tac ***)
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents:
diff changeset
    16
structure Blast_Data = 
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents:
diff changeset
    17
  struct
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents:
diff changeset
    18
  type claset	= Classical.claset
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents:
diff changeset
    19
  val notE	= notE
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents:
diff changeset
    20
  val ccontr	= ccontr
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents:
diff changeset
    21
  val contr_tac = Classical.contr_tac
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents:
diff changeset
    22
  val dup_intr	= Classical.dup_intr
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents:
diff changeset
    23
  val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents:
diff changeset
    24
  val claset	= Classical.claset
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents:
diff changeset
    25
  val rep_cs    = Classical.rep_cs
10429
8820f787e61e val atomize = thms "atomize'";
wenzelm
parents: 9530
diff changeset
    26
  val atomize	= thms "atomize'"
7357
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents:
diff changeset
    27
  val cla_modifiers = Classical.cla_modifiers;
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents:
diff changeset
    28
  val cla_meth' = Classical.cla_meth'
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents:
diff changeset
    29
  end;
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents:
diff changeset
    30
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents:
diff changeset
    31
structure Blast = BlastFun(Blast_Data);
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents:
diff changeset
    32
Blast.overloaded ("op =", domain_type);	(*overloading of equality as iff*)
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents:
diff changeset
    33
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents:
diff changeset
    34
val Blast_tac = Blast.Blast_tac
d0e16da40ea2 proper bootstrap of HOL theory and packages;
wenzelm
parents:
diff changeset
    35
and blast_tac = Blast.blast_tac;