|
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 (** Applying HypsubstFun to generate hyp_subst_tac **) |
|
11 section "Classical Reasoner"; |
|
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 (*Propositional rules |
|
27 -- iffCE might seem better, but in the examples in ex/cla |
|
28 run about 7% slower than with iffE*) |
|
29 val prop_cs = empty_cs addSIs [refl,TrueI,conjI,disjCI,impI,notI,iffI] |
|
30 addSEs [conjE,disjE,impCE,FalseE,iffE]; |
|
31 |
|
32 (*Quantifier rules*) |
|
33 val FOL_cs = prop_cs addSIs [allI] addIs [exI,ex1I] |
|
34 addSEs [exE,ex1E] addEs [allE]; |
|
35 |
|
36 |
|
37 exception CS_DATA of claset; |
|
38 |
|
39 let fun merge [] = CS_DATA empty_cs |
|
40 | merge cs = let val cs = map (fn CS_DATA x => x) cs; |
|
41 in CS_DATA (foldl merge_cs (hd cs, tl cs)) end; |
|
42 |
|
43 fun put (CS_DATA cs) = claset := cs; |
|
44 |
|
45 fun get () = CS_DATA (!claset); |
|
46 in add_thydata "FOL" |
|
47 ("claset", ThyMethods {merge = merge, put = put, get = get}) |
|
48 end; |
|
49 |
|
50 claset := FOL_cs; |
|
51 |