src/FOL/cladata.ML
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 4653 d60f76680bf4
child 5929 890f2f9b926d
permissions -rw-r--r--
made tutorial first;
     1 (*  Title:      FOL/cladata.ML
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   1996  University of Cambridge
     5 
     6 Setting up the classical reasoner 
     7 *)
     8 
     9 
    10 section "Classical Reasoner";
    11 
    12 
    13 (*** Applying ClassicalFun to create a classical prover ***)
    14 structure Classical_Data = 
    15   struct
    16   val sizef     = size_of_thm
    17   val mp        = mp
    18   val not_elim  = notE
    19   val classical = classical
    20   val hyp_subst_tacs=[hyp_subst_tac]
    21   end;
    22 
    23 structure Cla = ClassicalFun(Classical_Data);
    24 open Cla;
    25 
    26 (*Better for fast_tac: needs no quantifier duplication!*)
    27 qed_goal "alt_ex1E" IFOL.thy
    28     "[| EX! x. P(x);                                              \
    29 \       !!x. [| P(x);  ALL y y'. P(y) & P(y') --> y=y' |] ==> R  \
    30 \    |] ==> R"
    31  (fn major::prems =>
    32   [ (rtac (major RS ex1E) 1),
    33     (REPEAT (ares_tac (allI::prems) 1)),
    34     (etac (dup_elim allE) 1),
    35     (IntPr.fast_tac 1)]);
    36 
    37 
    38 (*Propositional rules*)
    39 val prop_cs = empty_cs addSIs [refl,TrueI,conjI,disjCI,impI,notI,iffI] 
    40                        addSEs [conjE,disjE,impCE,FalseE,iffCE];
    41 
    42 (*Quantifier rules*)
    43 val FOL_cs = prop_cs addSIs [allI,ex_ex1I] addIs [exI] 
    44                      addSEs [exE,alt_ex1E] addEs [allE];
    45 
    46 claset_ref() := FOL_cs;
    47 
    48 
    49 (*** Applying BlastFun to create Blast_tac ***)
    50 structure Blast_Data = 
    51   struct
    52   type claset	= Cla.claset
    53   val notE	= notE
    54   val ccontr	= ccontr
    55   val contr_tac = Cla.contr_tac
    56   val dup_intr	= Cla.dup_intr
    57   val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
    58   val claset	= Cla.claset
    59   val rep_cs    = Cla.rep_cs
    60   end;
    61 
    62 structure Blast = BlastFun(Blast_Data);
    63 
    64 val Blast_tac = Blast.Blast_tac
    65 and blast_tac = Blast.blast_tac;
    66 
    67