src/FOL/cladata.ML
changeset 2844 05d78159812d
parent 2469 b50b8c0eec01
child 2867 0aa5a3cd4550
equal deleted inserted replaced
2843:ea49c12f677f 2844:05d78159812d
     7 *)
     7 *)
     8 
     8 
     9 
     9 
    10 (** Applying HypsubstFun to generate hyp_subst_tac **)
    10 (** Applying HypsubstFun to generate hyp_subst_tac **)
    11 section "Classical Reasoner";
    11 section "Classical Reasoner";
       
    12 
    12 
    13 
    13 (*** Applying ClassicalFun to create a classical prover ***)
    14 (*** Applying ClassicalFun to create a classical prover ***)
    14 structure Classical_Data = 
    15 structure Classical_Data = 
    15   struct
    16   struct
    16   val sizef     = size_of_thm
    17   val sizef     = size_of_thm
    21   end;
    22   end;
    22 
    23 
    23 structure Cla = ClassicalFun(Classical_Data);
    24 structure Cla = ClassicalFun(Classical_Data);
    24 open Cla;
    25 open Cla;
    25 
    26 
       
    27 (*Better for fast_tac: needs no quantifier duplication!*)
       
    28 qed_goal "alt_ex1E" IFOL.thy
       
    29     "[| EX! x.P(x);                                              \
       
    30 \       !!x. [| P(x);  ALL y y'. P(y) & P(y') --> y=y' |] ==> R  \
       
    31 \    |] ==> R"
       
    32  (fn major::prems =>
       
    33   [ (rtac (major RS ex1E) 1),
       
    34     (REPEAT (ares_tac (allI::prems) 1)),
       
    35     (etac (dup_elim allE) 1),
       
    36     (IntPr.fast_tac 1)]);
       
    37 
       
    38 
    26 (*Propositional rules 
    39 (*Propositional rules 
    27   -- iffCE might seem better, but in the examples in ex/cla
    40   -- iffCE might seem better, but in the examples in ex/cla
    28      run about 7% slower than with iffE*)
    41      run about 7% slower than with iffE*)
    29 val prop_cs = empty_cs addSIs [refl,TrueI,conjI,disjCI,impI,notI,iffI] 
    42 val prop_cs = empty_cs addSIs [refl,TrueI,conjI,disjCI,impI,notI,iffI] 
    30                        addSEs [conjE,disjE,impCE,FalseE,iffE];
    43                        addSEs [conjE,disjE,impCE,FalseE,iffE];
    31 
    44 
    32 (*Quantifier rules*)
    45 (*Quantifier rules*)
    33 val FOL_cs = prop_cs addSIs [allI] addIs [exI,ex1I] 
    46 val FOL_cs = prop_cs addSIs [allI,ex_ex1I] addIs [exI] 
    34                      addSEs [exE,ex1E] addEs [allE];
    47                      addSEs [exE,alt_ex1E] addEs [allE];
    35 
    48 
    36 
    49 
    37 exception CS_DATA of claset;
    50 exception CS_DATA of claset;
    38 
    51 
    39 let fun merge [] = CS_DATA empty_cs
    52 let fun merge [] = CS_DATA empty_cs