1477

1 
(* Title: FOLP/FOLP.thy


2 
Author: Martin D Coen, Cambridge University Computer Laboratory

1142

3 
Copyright 1992 University of Cambridge


4 
*)


5 

60770

6 
section \<open>Classical FirstOrder Logic with Proofs\<close>

17480

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 

61337

18 
schematic_goal 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*)

61337

27 
schematic_goal 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~ *)

61337

35 
schematic_goal 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 

61337

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

61337

53 
schematic_goal 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])

69593

59 
apply (tactic \<open>DEPTH_SOLVE (assume_tac \<^context> 1 ORELSE


60 
resolve_tac \<^context> [@{thm r1}, @{thm r2}, @{thm major} RS @{thm mp}] 1)\<close>)

26322

61 
done


62 


63 
(*Double negation law*)

61337

64 
schematic_goal 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 *)

61337

75 
schematic_goal 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)

69593

83 
apply (tactic \<open>DEPTH_SOLVE_1 (eresolve_tac \<^context> @{thms impCE} 1 ORELSE


84 
eresolve_tac \<^context> [@{thm notE}, @{thm impE}] 1 THEN assume_tac \<^context> 1 ORELSE


85 
assume_tac \<^context> 1 ORELSE


86 
resolve_tac \<^context> [@{thm r1}, @{thm r2}] 1)\<close>)+

26322

87 
done


88 


89 


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

61337

91 
schematic_goal swap:

26322

92 
assumes major: "p:~P"


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


94 
shows "?p : Q"


95 
apply (rule classical)


96 
apply (rule major [THEN notE])


97 
apply (rule r)


98 
apply assumption


99 
done


100 

48891

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


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

17480

103 

60770

104 
ML \<open>

42799

105 
structure Cla = Classical


106 
(

17480

107 
val sizef = size_of_thm

26322

108 
val mp = @{thm mp}


109 
val not_elim = @{thm notE}


110 
val swap = @{thm swap}

60754

111 
fun hyp_subst_tacs ctxt = [hyp_subst_tac ctxt]

42799

112 
);

17480

113 
open Cla;


114 


115 
(*Propositional rules


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


117 
run about 7% slower than with iffE*)

26322

118 
val prop_cs =


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


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


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

17480

122 


123 
(*Quantifier rules*)

26322

124 
val FOLP_cs =


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


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

17480

127 

26322

128 
val FOLP_dup_cs =


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


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

60770

131 
\<close>

17480

132 

61337

133 
schematic_goal cla_rews:

26322

134 
"?p1 : P  ~P"


135 
"?p2 : ~P  P"


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


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

69593

138 
apply (tactic \<open>ALLGOALS (Cla.fast_tac \<^context> FOLP_cs)\<close>)

26322

139 
done

17480

140 

48891

141 
ML_file "simpdata.ML"

17480

142 

0

143 
end
