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 
begin


11 

41779

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


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

17480

14 

26322

15 


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


17 

36319

18 
schematic_lemma disjCI:

26322

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


20 
shows "?p : PQ"


21 
apply (rule classical)


22 
apply (assumption  rule assms disjI1 notI)+


23 
apply (assumption  rule disjI2 notE)+


24 
done


25 


26 
(*introduction rule involving only EX*)

36319

27 
schematic_lemma ex_classical:

26322

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


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


30 
apply (rule classical)


31 
apply (rule exI, rule assms, assumption)


32 
done


33 


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

36319

35 
schematic_lemma exCI:

26322

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


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


38 
apply (rule ex_classical)


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


40 
apply (erule notE)


41 
apply (erule exI)


42 
done


43 

36319

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

26322

45 
apply (rule disjCI)


46 
apply assumption


47 
done


48 


49 


50 
(*** Special elimination rules *)

17480

51 

26322

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

36319

53 
schematic_lemma impCE:

26322

54 
assumes major: "p:P>Q"


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


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


57 
shows "?p : R"


58 
apply (rule excluded_middle [THEN disjE])


59 
apply (tactic {* DEPTH_SOLVE (atac 1 ORELSE


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


61 
done


62 


63 
(*Double negation law*)

36319

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

26322

65 
apply (rule classical)


66 
apply (erule notE)


67 
apply assumption


68 
done


69 


70 


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

17480

72 

26322

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


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

36319

75 
schematic_lemma iffCE:

26322

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


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


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


79 
shows "?p : R"


80 
apply (insert major)


81 
apply (unfold iff_def)


82 
apply (rule conjE)


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


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


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


86 
done


87 


88 


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

36319

90 
schematic_lemma swap:

26322

91 
assumes major: "p:~P"


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


93 
shows "?p : Q"


94 
apply (rule classical)


95 
apply (rule major [THEN notE])


96 
apply (rule r)


97 
apply assumption


98 
done


99 

48891

100 
ML_file "classical.ML" (* Patched because matching won't instantiate proof *)


101 
ML_file "simp.ML" (* Patched because matching won't instantiate proof *)

17480

102 


103 
ML {*

42799

104 
structure Cla = Classical


105 
(

17480

106 
val sizef = size_of_thm

26322

107 
val mp = @{thm mp}


108 
val not_elim = @{thm notE}


109 
val swap = @{thm swap}


110 
val hyp_subst_tacs = [hyp_subst_tac]

42799

111 
);

17480

112 
open Cla;


113 


114 
(*Propositional rules


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


116 
run about 7% slower than with iffE*)

26322

117 
val prop_cs =


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


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


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

17480

121 


122 
(*Quantifier rules*)

26322

123 
val FOLP_cs =


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


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

17480

126 

26322

127 
val FOLP_dup_cs =


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


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


130 
*}

17480

131 

36319

132 
schematic_lemma cla_rews:

26322

133 
"?p1 : P  ~P"


134 
"?p2 : ~P  P"


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


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


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


138 
done

17480

139 

48891

140 
ML_file "simpdata.ML"

17480

141 

0

142 
end
