src/FOLP/ROOT.ML
changeset 17480 fd19f77dcf60
parent 6349 f7750d816c21
child 25750 4e796867ccb5
     1.1 --- a/src/FOLP/ROOT.ML	Sat Sep 17 20:49:14 2005 +0200
     1.2 +++ b/src/FOLP/ROOT.ML	Sun Sep 18 14:25:48 2005 +0200
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Title:      FOLP/ROOT
     1.5 +(*  Title:      FOLP/ROOT.ML
     1.6      ID:         $Id$
     1.7      Author:     martin Coen, Cambridge University Computer Laboratory
     1.8      Copyright   1993  University of Cambridge
     1.9 @@ -9,72 +9,6 @@
    1.10  *)
    1.11  
    1.12  val banner = "First-Order Logic with Natural Deduction with Proof Terms";
    1.13 -
    1.14  writeln banner;
    1.15  
    1.16 -print_depth 1;
    1.17 -
    1.18 -use_thy "IFOLP";
    1.19  use_thy "FOLP";
    1.20 -
    1.21 -use "hypsubst.ML";
    1.22 -use "classical.ML";      (* Patched 'cos matching won't instantiate proof *)
    1.23 -use "simp.ML";           (* Patched 'cos matching won't instantiate proof *)
    1.24 -
    1.25 -
    1.26 -(*** Applying HypsubstFun to generate hyp_subst_tac ***)
    1.27 -
    1.28 -structure Hypsubst_Data =
    1.29 -  struct
    1.30 -  (*Take apart an equality judgement; otherwise raise Match!*)
    1.31 -  fun dest_eq (Const("Proof",_) $ (Const("op =",_)  $ t $ u) $ _) = (t,u);
    1.32 -
    1.33 -  val imp_intr = impI
    1.34 -
    1.35 -  (*etac rev_cut_eq moves an equality to be the last premise. *)
    1.36 -  val rev_cut_eq = prove_goal IFOLP.thy 
    1.37 -                "[| p:a=b;  !!x. x:a=b ==> f(x):R |] ==> ?p:R"
    1.38 -   (fn prems => [ REPEAT(resolve_tac prems 1) ]);
    1.39 -
    1.40 -  val rev_mp = rev_mp
    1.41 -  val subst = subst
    1.42 -  val sym = sym
    1.43 -  val thin_refl = prove_goal IFOLP.thy 
    1.44 -		  "!!X. [|p:x=x; PROP W|] ==> PROP W" (K [atac 1]);
    1.45 -  end;
    1.46 -
    1.47 -structure Hypsubst = HypsubstFun(Hypsubst_Data);
    1.48 -open Hypsubst;
    1.49 -
    1.50 -use "intprover.ML";
    1.51 -
    1.52 -(*** Applying ClassicalFun to create a classical prover ***)
    1.53 -structure Classical_Data = 
    1.54 -  struct
    1.55 -  val sizef = size_of_thm
    1.56 -  val mp = mp
    1.57 -  val not_elim = notE
    1.58 -  val swap = swap
    1.59 -  val hyp_subst_tacs=[hyp_subst_tac]
    1.60 -  end;
    1.61 -
    1.62 -structure Cla = ClassicalFun(Classical_Data);
    1.63 -open Cla;
    1.64 -
    1.65 -(*Propositional rules 
    1.66 -  -- iffCE might seem better, but in the examples in ex/cla
    1.67 -     run about 7% slower than with iffE*)
    1.68 -val prop_cs = empty_cs addSIs [refl,TrueI,conjI,disjCI,impI,notI,iffI] 
    1.69 -                       addSEs [conjE,disjE,impCE,FalseE,iffE];
    1.70 -
    1.71 -(*Quantifier rules*)
    1.72 -val FOLP_cs = prop_cs addSIs [allI] addIs [exI,ex1I] 
    1.73 -                      addSEs [exE,ex1E] addEs [allE];
    1.74 -
    1.75 -val FOLP_dup_cs = prop_cs addSIs [allI] addIs [exCI,ex1I] 
    1.76 -                          addSEs [exE,ex1E] addEs [all_dupE];
    1.77 -
    1.78 -use "simpdata.ML";
    1.79 -
    1.80 -
    1.81 -print_depth 8;