0

1 
(* Title: FOL/ROOT


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1993 University of Cambridge


5 


6 
Adds FirstOrder Logic to a database containing pure Isabelle.


7 
Should be executed in the subdirectory FOL.


8 
*)


9 


10 
val banner = "FirstOrder Logic with Natural Deduction";


11 


12 
writeln banner;


13 

72

14 
structure Readthy = ReadthyFUN (structure ThySyn = ThySyn);


15 
open Readthy;


16 

0

17 
print_depth 1;

97

18 
use_thy "FOL";

0

19 


20 
use "../Provers/hypsubst.ML";


21 
use "../Provers/classical.ML";


22 
use "../Provers/simplifier.ML";


23 
use "../Provers/splitter.ML";


24 
use "../Provers/ind.ML";


25 


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


27 


28 
structure Hypsubst_Data =


29 
struct


30 
(*Take apart an equality judgement; otherwise raise Match!*)


31 
fun dest_eq (Const("Trueprop",_) $ (Const("op =",_) $ t $ u)) = (t,u);


32 


33 
val imp_intr = impI


34 


35 
(*etac rev_cut_eq moves an equality to be the last premise. *)


36 
val rev_cut_eq = prove_goal IFOL.thy "[ a=b; a=b ==> R ] ==> R"


37 
(fn prems => [ REPEAT(resolve_tac prems 1) ]);


38 


39 
val rev_mp = rev_mp


40 
val subst = subst


41 
val sym = sym


42 
end;


43 


44 
structure Hypsubst = HypsubstFun(Hypsubst_Data);


45 
open Hypsubst;


46 

97

47 
use "intprover.ML";

0

48 


49 
(*** Applying ClassicalFun to create a classical prover ***)


50 
structure Classical_Data =


51 
struct


52 
val sizef = size_of_thm


53 
val mp = mp


54 
val not_elim = notE


55 
val swap = swap


56 
val hyp_subst_tacs=[hyp_subst_tac]


57 
end;


58 


59 
structure Cla = ClassicalFun(Classical_Data);


60 
open Cla;


61 


62 
(*Propositional rules


63 
 iffCE might seem better, but in the examples in ex/cla


64 
run about 7% slower than with iffE*)


65 
val prop_cs = empty_cs addSIs [refl,TrueI,conjI,disjCI,impI,notI,iffI]


66 
addSEs [conjE,disjE,impCE,FalseE,iffE];


67 


68 
(*Quantifier rules*)


69 
val FOL_cs = prop_cs addSIs [allI] addIs [exI,ex1I]


70 
addSEs [exE,ex1E] addEs [allE];


71 


72 
val FOL_dup_cs = prop_cs addSIs [allI] addIs [exCI,ex1I]


73 
addSEs [exE,ex1E] addEs [all_dupE];


74 


75 
use "simpdata.ML";


76 


77 
use "../Pure/install_pp.ML";


78 
print_depth 8;


79 


80 
val FOL_build_completed = (); (*indicate successful build*)


81 
