1477

1 
(* Title: FOLP/FOLP.thy


2 
Author: Martin D Coen, Cambridge University Computer Laboratory

1142

3 
Copyright 1992 University of Cambridge


4 
*)


5 

17480

6 
header {* Classical FirstOrder Logic with Proofs *}


7 


8 
theory FOLP


9 
imports IFOLP


10 
uses

26322

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

17480

12 
begin


13 

41779

14 
axiomatization cla :: "[p=>p]=>p"


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

17480

16 

26322

17 


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


19 

36319

20 
schematic_lemma disjCI:

26322

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


22 
shows "?p : PQ"


23 
apply (rule classical)


24 
apply (assumption  rule assms disjI1 notI)+


25 
apply (assumption  rule disjI2 notE)+


26 
done


27 


28 
(*introduction rule involving only EX*)

36319

29 
schematic_lemma ex_classical:

26322

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


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


32 
apply (rule classical)


33 
apply (rule exI, rule assms, assumption)


34 
done


35 


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

36319

37 
schematic_lemma exCI:

26322

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


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


40 
apply (rule ex_classical)


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


42 
apply (erule notE)


43 
apply (erule exI)


44 
done


45 

36319

46 
schematic_lemma excluded_middle: "?p : ~P  P"

26322

47 
apply (rule disjCI)


48 
apply assumption


49 
done


50 


51 


52 
(*** Special elimination rules *)

17480

53 

26322

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

36319

55 
schematic_lemma impCE:

26322

56 
assumes major: "p:P>Q"


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


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


59 
shows "?p : R"


60 
apply (rule excluded_middle [THEN disjE])


61 
apply (tactic {* DEPTH_SOLVE (atac 1 ORELSE


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


63 
done


64 


65 
(*Double negation law*)

36319

66 
schematic_lemma notnotD: "p:~~P ==> ?p : P"

26322

67 
apply (rule classical)


68 
apply (erule notE)


69 
apply assumption


70 
done


71 


72 


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

17480

74 

26322

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


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

36319

77 
schematic_lemma iffCE:

26322

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


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


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


81 
shows "?p : R"


82 
apply (insert major)


83 
apply (unfold iff_def)


84 
apply (rule conjE)


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


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


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


88 
done


89 


90 


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

36319

92 
schematic_lemma swap:

26322

93 
assumes major: "p:~P"


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


95 
shows "?p : Q"


96 
apply (rule classical)


97 
apply (rule major [THEN notE])


98 
apply (rule r)


99 
apply assumption


100 
done


101 

17480

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


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


104 


105 
ML {*


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


107 
structure Classical_Data =

26322

108 
struct

17480

109 
val sizef = size_of_thm

26322

110 
val mp = @{thm mp}


111 
val not_elim = @{thm notE}


112 
val swap = @{thm swap}


113 
val hyp_subst_tacs = [hyp_subst_tac]


114 
end;

17480

115 


116 
structure Cla = ClassicalFun(Classical_Data);


117 
open Cla;


118 


119 
(*Propositional rules


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


121 
run about 7% slower than with iffE*)

26322

122 
val prop_cs =


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


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


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

17480

126 


127 
(*Quantifier rules*)

26322

128 
val FOLP_cs =


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


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

17480

131 

26322

132 
val FOLP_dup_cs =


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


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


135 
*}

17480

136 

36319

137 
schematic_lemma cla_rews:

26322

138 
"?p1 : P  ~P"


139 
"?p2 : ~P  P"


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


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


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


143 
done

17480

144 


145 
use "simpdata.ML"


146 

0

147 
end
