src/FOL/ROOT.ML
 author paulson Wed, 28 Feb 1996 11:46:08 +0100 changeset 1523 7513fbe502fb parent 1459 d12da312eff4 child 2237 f01ac387e82b permissions -rw-r--r--
changed prove_goal to qed_goal
```
(*  Title:      FOL/ROOT
ID:         \$Id\$
Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

Adds First-Order Logic to a database containing pure Isabelle.
Should be executed in the subdirectory FOL.
*)

val banner = "First-Order Logic with Natural Deduction";

writeln banner;

print_depth 1;
use_thy "FOL";

use "../Provers/splitter.ML";
use "../Provers/ind.ML";
use "../Provers/hypsubst.ML";
use "../Provers/classical.ML";

(*** Applying HypsubstFun to generate hyp_subst_tac ***)

structure Hypsubst_Data =
struct
structure Simplifier = Simplifier
(*Take apart an equality judgement; otherwise raise Match!*)
fun dest_eq (Const("Trueprop",_) \$ (Const("op =",_)  \$ t \$ u)) = (t,u)
val eq_reflection = eq_reflection
val imp_intr = impI
val rev_mp = rev_mp
val subst = subst
val sym = sym
end;

structure Hypsubst = HypsubstFun(Hypsubst_Data);
open Hypsubst;

use "intprover.ML";

(*** Applying ClassicalFun to create a classical prover ***)
structure Classical_Data =
struct
val sizef     = size_of_thm
val mp        = mp
val not_elim  = notE
val classical = classical
val hyp_subst_tacs=[hyp_subst_tac]
end;

structure Cla = ClassicalFun(Classical_Data);
open Cla;

(*Propositional rules
-- iffCE might seem better, but in the examples in ex/cla
run about 7% slower than with iffE*)
val prop_cs = empty_cs addSIs [refl,TrueI,conjI,disjCI,impI,notI,iffI]

(*Quantifier rules*)