0

1 
(* Title: FOLP/ROOT


2 
ID: $Id$


3 
Author: martin Coen, Cambridge University Computer Laboratory


4 
Copyright 1993 University of Cambridge


5 


6 
Modifed version of Lawrence Paulson's FOL that contains proof terms.


7 


8 
Presence of unknown proof term means that matching does not behave as expected.


9 
*)


10 


11 
val banner = "FirstOrder Logic with Natural Deduction with Proof Terms";


12 


13 
writeln banner;


14 

393

15 
init_thy_reader();

72

16 

0

17 
print_depth 1;

98

18 
use_thy "IFOLP";


19 
use_thy "FOLP";

0

20 


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


22 
use "classical.ML"; (* Patched 'cos matching won't instantiate proof *)


23 
use "simp.ML"; (* Patched 'cos matching won't instantiate proof *)


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


25 


26 


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


28 


29 
structure Hypsubst_Data =


30 
struct


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


32 
fun dest_eq (Const("Proof",_) $ (Const("op =",_) $ t $ u) $ _) = (t,u);


33 


34 
val imp_intr = impI


35 


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


37 
val rev_cut_eq = prove_goal IFOLP.thy


38 
"[ p:a=b; !!x.x:a=b ==> f(x):R ] ==> ?p:R"


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


40 


41 
val rev_mp = rev_mp


42 
val subst = subst


43 
val sym = sym


44 
end;


45 


46 
structure Hypsubst = HypsubstFun(Hypsubst_Data);


47 
open Hypsubst;


48 

98

49 
use "intprover.ML";

0

50 


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


52 
structure Classical_Data =


53 
struct


54 
val sizef = size_of_thm


55 
val mp = mp


56 
val not_elim = notE


57 
val swap = swap


58 
val hyp_subst_tacs=[hyp_subst_tac]


59 
end;


60 


61 
structure Cla = ClassicalFun(Classical_Data);


62 
open Cla;


63 


64 
(*Propositional rules


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


66 
run about 7% slower than with iffE*)


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


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


69 


70 
(*Quantifier rules*)


71 
val FOLP_cs = prop_cs addSIs [allI] addIs [exI,ex1I]


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


73 


74 
val FOLP_dup_cs = prop_cs addSIs [allI] addIs [exCI,ex1I]


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


76 


77 
use "simpdata.ML";


78 


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


80 
print_depth 8;

176

81 


82 
val FOLP_build_completed = (); (*indicate successful build*)
