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 

72

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


16 
open Readthy;


17 

0

18 
print_depth 1;

98

19 
use_thy "IFOLP";


20 
use_thy "FOLP";

0

21 


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


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


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


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


26 


27 


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


29 


30 
structure Hypsubst_Data =


31 
struct


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


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


34 


35 
val imp_intr = impI


36 


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


38 
val rev_cut_eq = prove_goal IFOLP.thy


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


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


41 


42 
val rev_mp = rev_mp


43 
val subst = subst


44 
val sym = sym


45 
end;


46 


47 
structure Hypsubst = HypsubstFun(Hypsubst_Data);


48 
open Hypsubst;


49 

98

50 
use "intprover.ML";

0

51 


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


53 
structure Classical_Data =


54 
struct


55 
val sizef = size_of_thm


56 
val mp = mp


57 
val not_elim = notE


58 
val swap = swap


59 
val hyp_subst_tacs=[hyp_subst_tac]


60 
end;


61 


62 
structure Cla = ClassicalFun(Classical_Data);


63 
open Cla;


64 


65 
(*Propositional rules


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


67 
run about 7% slower than with iffE*)


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


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


70 


71 
(*Quantifier rules*)


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


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


74 


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


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


77 


78 
use "simpdata.ML";


79 


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


81 
print_depth 8;
