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 


14 
print_depth 1;


15 
use_thy "ifol";


16 
use_thy "fol";


17 


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";


23 


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


25 


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);


30 


31 
val imp_intr = impI


32 


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) ]);


36 


37 
val rev_mp = rev_mp


38 
val subst = subst


39 
val sym = sym


40 
end;


41 


42 
structure Hypsubst = HypsubstFun(Hypsubst_Data);


43 
open Hypsubst;


44 


45 
use "intprover.ML";


46 


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;


56 


57 
structure Cla = ClassicalFun(Classical_Data);


58 
open Cla;


59 


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]


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


65 


66 
(*Quantifier rules*)


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


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


69 


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


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


72 


73 
use "simpdata.ML";


74 


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


76 
print_depth 8;


77 


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


79 
