1477

1 
(* Title: FOLP/FOLP.thy

1142

2 
ID: $Id$

1477

3 
Author: Martin D Coen, Cambridge University Computer Laboratory

1142

4 
Copyright 1992 University of Cambridge


5 
*)


6 

17480

7 
header {* Classical FirstOrder Logic with Proofs *}


8 


9 
theory FOLP


10 
imports IFOLP


11 
uses


12 
("FOLP_lemmas.ML") ("hypsubst.ML") ("classical.ML")


13 
("simp.ML") ("intprover.ML") ("simpdata.ML")


14 
begin


15 

0

16 
consts


17 
cla :: "[p=>p]=>p"

17480

18 
axioms


19 
classical: "(!!x. x:~P ==> f(x):P) ==> cla(f):P"


20 


21 
ML {* use_legacy_bindings (the_context ()) *}


22 


23 
use "FOLP_lemmas.ML"


24 


25 
use "hypsubst.ML"


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


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


28 


29 
ML {*


30 


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


32 


33 
structure Hypsubst_Data =


34 
struct


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


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


37 


38 
val imp_intr = impI


39 


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


41 
val rev_cut_eq = prove_goal (the_context ())


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


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


44 


45 
val rev_mp = rev_mp


46 
val subst = subst


47 
val sym = sym


48 
val thin_refl = prove_goal (the_context ())


49 
"!!X. [p:x=x; PROP W] ==> PROP W" (K [atac 1]);


50 
end;


51 


52 
structure Hypsubst = HypsubstFun(Hypsubst_Data);


53 
open Hypsubst;


54 
*}


55 


56 
use "intprover.ML"


57 


58 
ML {*


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


60 
structure Classical_Data =


61 
struct


62 
val sizef = size_of_thm


63 
val mp = mp


64 
val not_elim = notE


65 
val swap = swap


66 
val hyp_subst_tacs=[hyp_subst_tac]


67 
end;


68 


69 
structure Cla = ClassicalFun(Classical_Data);


70 
open Cla;


71 


72 
(*Propositional rules


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


74 
run about 7% slower than with iffE*)


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


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


77 


78 
(*Quantifier rules*)


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


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


81 


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


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


84 


85 
*}


86 


87 
use "simpdata.ML"


88 

0

89 
end
