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. *)

22577

41 
val rev_cut_eq = prove_goal @{theory}

17480

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

22577

48 
val thin_refl = prove_goal @{theory} "!!X. [p:x=x; PROP W] ==> PROP W" (K [atac 1]);

17480

49 
end;


50 


51 
structure Hypsubst = HypsubstFun(Hypsubst_Data);


52 
open Hypsubst;


53 
*}


54 


55 
use "intprover.ML"


56 


57 
ML {*


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


59 
structure Classical_Data =


60 
struct


61 
val sizef = size_of_thm


62 
val mp = mp


63 
val not_elim = notE


64 
val swap = swap


65 
val hyp_subst_tacs=[hyp_subst_tac]


66 
end;


67 


68 
structure Cla = ClassicalFun(Classical_Data);


69 
open Cla;


70 


71 
(*Propositional rules


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


73 
run about 7% slower than with iffE*)


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


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


76 


77 
(*Quantifier rules*)


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


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


80 


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


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


83 


84 
*}


85 


86 
use "simpdata.ML"


87 

0

88 
end
