src/FOL/cladata.ML
author oheimb
Thu May 15 15:51:09 1997 +0200 (1997-05-15 ago)
changeset 3206 a3de7f32728c
parent 2867 0aa5a3cd4550
child 3610 7e5300420b03
permissions -rw-r--r--
renamed addss to addSss, unsafe_addss to addss, extended auto_tac
     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   -- iffCE might seem better, but in the examples in ex/cla
    40      run about 7% slower than with iffE*)
    41 val prop_cs = empty_cs addSIs [refl,TrueI,conjI,disjCI,impI,notI,iffI] 
    42                        addSEs [conjE,disjE,impCE,FalseE,iffE];
    43 
    44 (*Quantifier rules*)
    45 val FOL_cs = prop_cs addSIs [allI,ex_ex1I] addIs [exI] 
    46                      addSEs [exE,alt_ex1E] addEs [allE];
    47 
    48 
    49 exception CS_DATA of claset;
    50 
    51 let fun merge [] = CS_DATA empty_cs
    52       | merge cs = let val cs = map (fn CS_DATA x => x) cs;
    53                    in CS_DATA (foldl merge_cs (hd cs, tl cs)) end;
    54 
    55     fun put (CS_DATA cs) = claset := cs;
    56 
    57     fun get () = CS_DATA (!claset);
    58 in add_thydata "FOL"
    59      ("claset", ThyMethods {merge = merge, put = put, get = get})
    60 end;
    61 
    62 claset := FOL_cs;
    63 
    64 (*** Applying BlastFun to create Blast_tac ***)
    65 structure Blast_Data = 
    66   struct
    67   type claset	= Cla.claset
    68   val notE	= notE
    69   val ccontr	= ccontr
    70   val contr_tac = Cla.contr_tac
    71   val dup_intr	= Cla.dup_intr
    72   val vars_gen_hyp_subst_tac = Hypsubst.vars_gen_hyp_subst_tac
    73   val claset	= Cla.claset
    74   val rep_claset = Cla.rep_claset
    75   end;
    76 
    77 structure Blast = BlastFun(Blast_Data);
    78 
    79 val Blast_tac = Blast.Blast_tac
    80 and blast_tac = Blast.blast_tac;
    81 
    82