author  haftmann 
Thu, 18 Nov 2010 17:01:15 +0100  
changeset 40602  91e583511113 
parent 30607  c3d1590debd8 
child 41959  b460124855b8 
permissions  rwrr 
17481  1 
(* Title: LK/LK.ML 
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

3 
Copyright 1993 University of Cambridge 
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

4 

7094
6f18ae72a90e
a new theory containing just an axiom needed to derive imp_cong
paulson
parents:
6456
diff
changeset

5 
Axiom to express monotonicity (a variant of the deduction theorem). Makes the 
6f18ae72a90e
a new theory containing just an axiom needed to derive imp_cong
paulson
parents:
6456
diff
changeset

6 
link between  and ==>, needed for instance to prove imp_cong. 
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

7 

7117  8 
Axiom left_cong allows the simplifier to use leftside formulas. Ideally it 
9 
should be derived from lowerlevel axioms. 

10 

7094
6f18ae72a90e
a new theory containing just an axiom needed to derive imp_cong
paulson
parents:
6456
diff
changeset

11 
CANNOT be added to LK0.thy because modal logic is built upon it, and 
6f18ae72a90e
a new theory containing just an axiom needed to derive imp_cong
paulson
parents:
6456
diff
changeset

12 
various modal rules would become inconsistent. 
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

13 
*) 
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

14 

17481  15 
theory LK 
16 
imports LK0 

17 
uses ("simpdata.ML") 

18 
begin 

2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

19 

27149  20 
axiomatization where 
21 
monotonic: "($H  P ==> $H  Q) ==> $H, P  Q" and 

2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

22 

17481  23 
left_cong: "[ P == P';  P' ==> ($H  $F) == ($H'  $F') ] 
24 
==> (P, $H  $F) == (P', $H'  $F')" 

2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

25 

27149  26 

27 
subsection {* Rewrite rules *} 

28 

29 
lemma conj_simps: 

30 
" P & True <> P" 

31 
" True & P <> P" 

32 
" P & False <> False" 

33 
" False & P <> False" 

34 
" P & P <> P" 

35 
" P & P & Q <> P & Q" 

36 
" P & ~P <> False" 

37 
" ~P & P <> False" 

38 
" (P & Q) & R <> P & (Q & R)" 

39 
apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *}) 

40 
done 

41 

42 
lemma disj_simps: 

43 
" P  True <> True" 

44 
" True  P <> True" 

45 
" P  False <> P" 

46 
" False  P <> P" 

47 
" P  P <> P" 

48 
" P  P  Q <> P  Q" 

49 
" (P  Q)  R <> P  (Q  R)" 

50 
apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *}) 

51 
done 

52 

53 
lemma not_simps: 

54 
" ~ False <> True" 

55 
" ~ True <> False" 

56 
apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *}) 

57 
done 

58 

59 
lemma imp_simps: 

60 
" (P > False) <> ~P" 

61 
" (P > True) <> True" 

62 
" (False > P) <> True" 

63 
" (True > P) <> P" 

64 
" (P > P) <> True" 

65 
" (P > ~P) <> ~P" 

66 
apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *}) 

67 
done 

68 

69 
lemma iff_simps: 

70 
" (True <> P) <> P" 

71 
" (P <> True) <> P" 

72 
" (P <> P) <> True" 

73 
" (False <> P) <> ~P" 

74 
" (P <> False) <> ~P" 

75 
apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *}) 

76 
done 

77 

78 
lemma quant_simps: 

79 
"!!P.  (ALL x. P) <> P" 

80 
"!!P.  (ALL x. x=t > P(x)) <> P(t)" 

81 
"!!P.  (ALL x. t=x > P(x)) <> P(t)" 

82 
"!!P.  (EX x. P) <> P" 

83 
"!!P.  (EX x. x=t & P(x)) <> P(t)" 

84 
"!!P.  (EX x. t=x & P(x)) <> P(t)" 

85 
apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *}) 

86 
done 

87 

88 

89 
subsection {* Miniscoping: pushing quantifiers in *} 

90 

91 
text {* 

92 
We do NOT distribute of ALL over &, or dually that of EX over  

93 
Baaz and Leitsch, On Skolemization and Proof Complexity (1994) 

94 
show that this step can increase proof length! 

95 
*} 

96 

97 
text {*existential miniscoping*} 

98 
lemma ex_simps: 

99 
"!!P Q.  (EX x. P(x) & Q) <> (EX x. P(x)) & Q" 

100 
"!!P Q.  (EX x. P & Q(x)) <> P & (EX x. Q(x))" 

101 
"!!P Q.  (EX x. P(x)  Q) <> (EX x. P(x))  Q" 

102 
"!!P Q.  (EX x. P  Q(x)) <> P  (EX x. Q(x))" 

103 
"!!P Q.  (EX x. P(x) > Q) <> (ALL x. P(x)) > Q" 

104 
"!!P Q.  (EX x. P > Q(x)) <> P > (EX x. Q(x))" 

105 
apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *}) 

106 
done 

107 

108 
text {*universal miniscoping*} 

109 
lemma all_simps: 

110 
"!!P Q.  (ALL x. P(x) & Q) <> (ALL x. P(x)) & Q" 

111 
"!!P Q.  (ALL x. P & Q(x)) <> P & (ALL x. Q(x))" 

112 
"!!P Q.  (ALL x. P(x) > Q) <> (EX x. P(x)) > Q" 

113 
"!!P Q.  (ALL x. P > Q(x)) <> P > (ALL x. Q(x))" 

114 
"!!P Q.  (ALL x. P(x)  Q) <> (ALL x. P(x))  Q" 

115 
"!!P Q.  (ALL x. P  Q(x)) <> P  (ALL x. Q(x))" 

116 
apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *}) 

117 
done 

118 

119 
text {*These are NOT supplied by default!*} 

120 
lemma distrib_simps: 

121 
" P & (Q  R) <> P&Q  P&R" 

122 
" (Q  R) & P <> Q&P  R&P" 

123 
" (P  Q > R) <> (P > R) & (Q > R)" 

124 
apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *}) 

125 
done 

126 

127 
lemma P_iff_F: " ~P ==>  (P <> False)" 

128 
apply (erule thinR [THEN cut]) 

129 
apply (tactic {* fast_tac LK_pack 1 *}) 

130 
done 

131 

132 
lemmas iff_reflection_F = P_iff_F [THEN iff_reflection, standard] 

133 

134 
lemma P_iff_T: " P ==>  (P <> True)" 

135 
apply (erule thinR [THEN cut]) 

136 
apply (tactic {* fast_tac LK_pack 1 *}) 

137 
done 

138 

139 
lemmas iff_reflection_T = P_iff_T [THEN iff_reflection, standard] 

140 

141 

142 
lemma LK_extra_simps: 

143 
" P  ~P" 

144 
" ~P  P" 

145 
" ~ ~ P <> P" 

146 
" (~P > P) <> P" 

147 
" (~P <> ~Q) <> (P<>Q)" 

148 
apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *}) 

149 
done 

150 

151 

152 
subsection {* Named rewrite rules *} 

153 

154 
lemma conj_commute: " P&Q <> Q&P" 

155 
and conj_left_commute: " P&(Q&R) <> Q&(P&R)" 

156 
apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *}) 

157 
done 

158 

159 
lemmas conj_comms = conj_commute conj_left_commute 

160 

161 
lemma disj_commute: " PQ <> QP" 

162 
and disj_left_commute: " P(QR) <> Q(PR)" 

163 
apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *}) 

164 
done 

165 

166 
lemmas disj_comms = disj_commute disj_left_commute 

167 

168 
lemma conj_disj_distribL: " P&(QR) <> (P&Q  P&R)" 

169 
and conj_disj_distribR: " (PQ)&R <> (P&R  Q&R)" 

170 

171 
and disj_conj_distribL: " P(Q&R) <> (PQ) & (PR)" 

172 
and disj_conj_distribR: " (P&Q)R <> (PR) & (QR)" 

173 

174 
and imp_conj_distrib: " (P > (Q&R)) <> (P>Q) & (P>R)" 

175 
and imp_conj: " ((P&Q)>R) <> (P > (Q > R))" 

176 
and imp_disj: " (PQ > R) <> (P>R) & (Q>R)" 

177 

178 
and imp_disj1: " (P>Q)  R <> (P>Q  R)" 

179 
and imp_disj2: " Q  (P>R) <> (P>Q  R)" 

180 

181 
and de_Morgan_disj: " (~(P  Q)) <> (~P & ~Q)" 

182 
and de_Morgan_conj: " (~(P & Q)) <> (~P  ~Q)" 

183 

184 
and not_iff: " ~(P <> Q) <> (P <> ~Q)" 

185 
apply (tactic {* ALLGOALS (fast_tac (LK_pack add_safes @{thms subst})) *}) 

186 
done 

187 

188 
lemma imp_cong: 

189 
assumes p1: " P <> P'" 

190 
and p2: " P' ==>  Q <> Q'" 

191 
shows " (P>Q) <> (P'>Q')" 

192 
apply (tactic {* lemma_tac @{thm p1} 1 *}) 

193 
apply (tactic {* safe_tac LK_pack 1 *}) 

194 
apply (tactic {* 

195 
REPEAT (rtac @{thm cut} 1 THEN 

196 
DEPTH_SOLVE_1 

197 
(resolve_tac [@{thm thinL}, @{thm thinR}, @{thm p2} COMP @{thm monotonic}] 1) THEN 

198 
safe_tac LK_pack 1) *}) 

199 
done 

200 

201 
lemma conj_cong: 

202 
assumes p1: " P <> P'" 

203 
and p2: " P' ==>  Q <> Q'" 

204 
shows " (P&Q) <> (P'&Q')" 

205 
apply (tactic {* lemma_tac @{thm p1} 1 *}) 

206 
apply (tactic {* safe_tac LK_pack 1 *}) 

207 
apply (tactic {* 

208 
REPEAT (rtac @{thm cut} 1 THEN 

209 
DEPTH_SOLVE_1 

210 
(resolve_tac [@{thm thinL}, @{thm thinR}, @{thm p2} COMP @{thm monotonic}] 1) THEN 

211 
safe_tac LK_pack 1) *}) 

212 
done 

213 

214 
lemma eq_sym_conv: " (x=y) <> (y=x)" 

215 
apply (tactic {* fast_tac (LK_pack add_safes @{thms subst}) 1 *}) 

216 
done 

217 

17481  218 
use "simpdata.ML" 
219 

27149  220 

221 
text {* To create substition rules *} 

222 

223 
lemma eq_imp_subst: " a=b ==> $H, A(a), $G  $E, A(b), $F" 

224 
apply (tactic {* asm_simp_tac LK_basic_ss 1 *}) 

225 
done 

226 

227 
lemma split_if: " P(if Q then x else y) <> ((Q > P(x)) & (~Q > P(y)))" 

228 
apply (rule_tac P = Q in cut) 

30607
c3d1590debd8
eliminated global SIMPSET, CLASET etc.  refer to explicit context;
wenzelm
parents:
28952
diff
changeset

229 
apply (tactic {* simp_tac (@{simpset} addsimps @{thms if_P}) 2 *}) 
27149  230 
apply (rule_tac P = "~Q" in cut) 
30607
c3d1590debd8
eliminated global SIMPSET, CLASET etc.  refer to explicit context;
wenzelm
parents:
28952
diff
changeset

231 
apply (tactic {* simp_tac (@{simpset} addsimps @{thms if_not_P}) 2 *}) 
27149  232 
apply (tactic {* fast_tac LK_pack 1 *}) 
233 
done 

234 

235 
lemma if_cancel: " (if P then x else x) = x" 

236 
apply (tactic {* lemma_tac @{thm split_if} 1 *}) 

237 
apply (tactic {* fast_tac LK_pack 1 *}) 

238 
done 

239 

240 
lemma if_eq_cancel: " (if x=y then y else x) = x" 

241 
apply (tactic {* lemma_tac @{thm split_if} 1 *}) 

242 
apply (tactic {* safe_tac LK_pack 1 *}) 

243 
apply (rule symL) 

244 
apply (rule basic) 

245 
done 

246 

2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

247 
end 