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 


15 
print_depth 1;


16 
use_thy "ifolp";


17 
use_thy "folp";


18 


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


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


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


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


23 


24 


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


26 


27 
structure Hypsubst_Data =


28 
struct


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


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


31 


32 
val imp_intr = impI


33 


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


35 
val rev_cut_eq = prove_goal IFOLP.thy


36 
"[ p:a=b; !!x.x:a=b ==> f(x):R ] ==> ?p: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 


47 
use "intprover.ML";


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 FOLP_cs = prop_cs addSIs [allI] addIs [exI,ex1I]


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


71 


72 
val FOLP_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;
