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

26322

12 
("classical.ML") ("simp.ML") ("simpdata.ML")

17480

13 
begin


14 

0

15 
consts


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

17480

17 
axioms


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


19 

26322

20 


21 
(*** Classical introduction rules for  and EX ***)


22 


23 
lemma disjCI:


24 
assumes "!!x. x:~Q ==> f(x):P"


25 
shows "?p : PQ"


26 
apply (rule classical)


27 
apply (assumption  rule assms disjI1 notI)+


28 
apply (assumption  rule disjI2 notE)+


29 
done


30 


31 
(*introduction rule involving only EX*)


32 
lemma ex_classical:


33 
assumes "!!u. u:~(EX x. P(x)) ==> f(u):P(a)"


34 
shows "?p : EX x. P(x)"


35 
apply (rule classical)


36 
apply (rule exI, rule assms, assumption)


37 
done


38 


39 
(*version of above, simplifying ~EX to ALL~ *)


40 
lemma exCI:


41 
assumes "!!u. u:ALL x. ~P(x) ==> f(u):P(a)"


42 
shows "?p : EX x. P(x)"


43 
apply (rule ex_classical)


44 
apply (rule notI [THEN allI, THEN assms])


45 
apply (erule notE)


46 
apply (erule exI)


47 
done


48 


49 
lemma excluded_middle: "?p : ~P  P"


50 
apply (rule disjCI)


51 
apply assumption


52 
done


53 


54 


55 
(*** Special elimination rules *)

17480

56 

26322

57 
(*Classical implies (>) elimination. *)


58 
lemma impCE:


59 
assumes major: "p:P>Q"


60 
and r1: "!!x. x:~P ==> f(x):R"


61 
and r2: "!!y. y:Q ==> g(y):R"


62 
shows "?p : R"


63 
apply (rule excluded_middle [THEN disjE])


64 
apply (tactic {* DEPTH_SOLVE (atac 1 ORELSE


65 
resolve_tac [@{thm r1}, @{thm r2}, @{thm major} RS @{thm mp}] 1) *})


66 
done


67 


68 
(*Double negation law*)


69 
lemma notnotD: "p:~~P ==> ?p : P"


70 
apply (rule classical)


71 
apply (erule notE)


72 
apply assumption


73 
done


74 


75 


76 
(*** Tactics for implication and contradiction ***)

17480

77 

26322

78 
(*Classical <> elimination. Proof substitutes P=Q in


79 
~P ==> ~Q and P ==> Q *)


80 
lemma iffCE:


81 
assumes major: "p:P<>Q"


82 
and r1: "!!x y.[ x:P; y:Q ] ==> f(x,y):R"


83 
and r2: "!!x y.[ x:~P; y:~Q ] ==> g(x,y):R"


84 
shows "?p : R"


85 
apply (insert major)


86 
apply (unfold iff_def)


87 
apply (rule conjE)


88 
apply (tactic {* DEPTH_SOLVE_1 (etac @{thm impCE} 1 ORELSE


89 
eresolve_tac [@{thm notE}, @{thm impE}] 1 THEN atac 1 ORELSE atac 1 ORELSE


90 
resolve_tac [@{thm r1}, @{thm r2}] 1) *})+


91 
done


92 


93 


94 
(*Should be used as swap since ~P becomes redundant*)


95 
lemma swap:


96 
assumes major: "p:~P"


97 
and r: "!!x. x:~Q ==> f(x):P"


98 
shows "?p : Q"


99 
apply (rule classical)


100 
apply (rule major [THEN notE])


101 
apply (rule r)


102 
apply assumption


103 
done


104 

17480

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


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


107 


108 
ML {*


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


110 
structure Classical_Data =

26322

111 
struct

17480

112 
val sizef = size_of_thm

26322

113 
val mp = @{thm mp}


114 
val not_elim = @{thm notE}


115 
val swap = @{thm swap}


116 
val hyp_subst_tacs = [hyp_subst_tac]


117 
end;

17480

118 


119 
structure Cla = ClassicalFun(Classical_Data);


120 
open Cla;


121 


122 
(*Propositional rules


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


124 
run about 7% slower than with iffE*)

26322

125 
val prop_cs =


126 
empty_cs addSIs [@{thm refl}, @{thm TrueI}, @{thm conjI}, @{thm disjCI},


127 
@{thm impI}, @{thm notI}, @{thm iffI}]


128 
addSEs [@{thm conjE}, @{thm disjE}, @{thm impCE}, @{thm FalseE}, @{thm iffE}];

17480

129 


130 
(*Quantifier rules*)

26322

131 
val FOLP_cs =


132 
prop_cs addSIs [@{thm allI}] addIs [@{thm exI}, @{thm ex1I}]


133 
addSEs [@{thm exE}, @{thm ex1E}] addEs [@{thm allE}];

17480

134 

26322

135 
val FOLP_dup_cs =


136 
prop_cs addSIs [@{thm allI}] addIs [@{thm exCI}, @{thm ex1I}]


137 
addSEs [@{thm exE}, @{thm ex1E}] addEs [@{thm all_dupE}];


138 
*}

17480

139 

26322

140 
lemma cla_rews:


141 
"?p1 : P  ~P"


142 
"?p2 : ~P  P"


143 
"?p3 : ~ ~ P <> P"


144 
"?p4 : (~P > P) <> P"


145 
apply (tactic {* ALLGOALS (Cla.fast_tac FOLP_cs) *})


146 
done

17480

147 


148 
use "simpdata.ML"


149 

0

150 
end
