src/FOL/ROOT.ML
 author clasohm Thu Sep 16 12:20:38 1993 +0200 (1993-09-16) changeset 0 a5a9c433f639 child 72 099d949fe467 permissions -rw-r--r--
Initial revision
1 (*  Title: 	FOL/ROOT
2     ID:         \$Id\$
3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
4     Copyright   1993  University of Cambridge
6 Adds First-Order Logic to a database containing pure Isabelle.
7 Should be executed in the subdirectory FOL.
8 *)
10 val banner = "First-Order Logic with Natural Deduction";
12 writeln banner;
14 print_depth 1;
15 use_thy "ifol";
16 use_thy "fol";
18 use "../Provers/hypsubst.ML";
19 use "../Provers/classical.ML";
20 use "../Provers/simplifier.ML";
21 use "../Provers/splitter.ML";
22 use "../Provers/ind.ML";
24 (*** Applying HypsubstFun to generate hyp_subst_tac ***)
26 structure Hypsubst_Data =
27   struct
28   (*Take apart an equality judgement; otherwise raise Match!*)
29   fun dest_eq (Const("Trueprop",_) \$ (Const("op =",_)  \$ t \$ u)) = (t,u);
31   val imp_intr = impI
33   (*etac rev_cut_eq moves an equality to be the last premise. *)
34   val rev_cut_eq = prove_goal IFOL.thy "[| a=b;  a=b ==> R |] ==> R"
35    (fn prems => [ REPEAT(resolve_tac prems 1) ]);
37   val rev_mp = rev_mp
38   val subst = subst
39   val sym = sym
40   end;
42 structure Hypsubst = HypsubstFun(Hypsubst_Data);
43 open Hypsubst;
45 use "int-prover.ML";
47 (*** Applying ClassicalFun to create a classical prover ***)
48 structure Classical_Data =
49   struct
50   val sizef = size_of_thm
51   val mp = mp
52   val not_elim = notE
53   val swap = swap
54   val hyp_subst_tacs=[hyp_subst_tac]
55   end;
57 structure Cla = ClassicalFun(Classical_Data);
58 open Cla;
60 (*Propositional rules
61   -- iffCE might seem better, but in the examples in ex/cla
62      run about 7% slower than with iffE*)
63 val prop_cs = empty_cs addSIs [refl,TrueI,conjI,disjCI,impI,notI,iffI]