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--
```     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
```