author  wenzelm 
Mon, 07 Oct 2013 21:24:44 +0200  
changeset 54313  da2e6282a4f5 
parent 51717  9e7d1c139569 
child 55228  901a6696cdd8 
permissions  rwrr 
41959  1 
(* Title: Sequents/LK.thy 
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 
begin 

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

18 

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

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

21 

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

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

24 

27149  25 

26 
subsection {* Rewrite rules *} 

27 

28 
lemma conj_simps: 

29 
" P & True <> P" 

30 
" True & P <> P" 

31 
" P & False <> False" 

32 
" False & P <> False" 

33 
" P & P <> P" 

34 
" P & P & Q <> P & Q" 

35 
" P & ~P <> False" 

36 
" ~P & P <> False" 

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

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

39 
done 

40 

41 
lemma disj_simps: 

42 
" P  True <> True" 

43 
" True  P <> True" 

44 
" P  False <> P" 

45 
" False  P <> P" 

46 
" P  P <> P" 

47 
" P  P  Q <> P  Q" 

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

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

50 
done 

51 

52 
lemma not_simps: 

53 
" ~ False <> True" 

54 
" ~ True <> False" 

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

56 
done 

57 

58 
lemma imp_simps: 

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

60 
" (P > True) <> True" 

61 
" (False > P) <> True" 

62 
" (True > P) <> P" 

63 
" (P > P) <> True" 

64 
" (P > ~P) <> ~P" 

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

66 
done 

67 

68 
lemma iff_simps: 

69 
" (True <> P) <> P" 

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

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

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

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

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

75 
done 

76 

77 
lemma quant_simps: 

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

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

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

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

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

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

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

85 
done 

86 

87 

88 
subsection {* Miniscoping: pushing quantifiers in *} 

89 

90 
text {* 

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

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

93 
show that this step can increase proof length! 

94 
*} 

95 

96 
text {*existential miniscoping*} 

97 
lemma ex_simps: 

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

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

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

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

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

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

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

105 
done 

106 

107 
text {*universal miniscoping*} 

108 
lemma all_simps: 

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

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

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

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

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

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

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

116 
done 

117 

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

119 
lemma distrib_simps: 

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

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

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

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

124 
done 

125 

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

127 
apply (erule thinR [THEN cut]) 

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

129 
done 

130 

45602  131 
lemmas iff_reflection_F = P_iff_F [THEN iff_reflection] 
27149  132 

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

134 
apply (erule thinR [THEN cut]) 

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

136 
done 

137 

45602  138 
lemmas iff_reflection_T = P_iff_T [THEN iff_reflection] 
27149  139 

140 

141 
lemma LK_extra_simps: 

142 
" P  ~P" 

143 
" ~P  P" 

144 
" ~ ~ P <> P" 

145 
" (~P > P) <> P" 

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

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

148 
done 

149 

150 

151 
subsection {* Named rewrite rules *} 

152 

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

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

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

156 
done 

157 

158 
lemmas conj_comms = conj_commute conj_left_commute 

159 

160 
lemma disj_commute: " PQ <> QP" 

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

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

163 
done 

164 

165 
lemmas disj_comms = disj_commute disj_left_commute 

166 

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

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

169 

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

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

172 

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

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

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

176 

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

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

179 

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

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

182 

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

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

185 
done 

186 

187 
lemma imp_cong: 

188 
assumes p1: " P <> P'" 

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

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

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

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

193 
apply (tactic {* 

194 
REPEAT (rtac @{thm cut} 1 THEN 

195 
DEPTH_SOLVE_1 

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

197 
safe_tac LK_pack 1) *}) 

198 
done 

199 

200 
lemma conj_cong: 

201 
assumes p1: " P <> P'" 

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

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

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

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

206 
apply (tactic {* 

207 
REPEAT (rtac @{thm cut} 1 THEN 

208 
DEPTH_SOLVE_1 

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

210 
safe_tac LK_pack 1) *}) 

211 
done 

212 

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

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

215 
done 

216 

48891  217 
ML_file "simpdata.ML" 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
48891
diff
changeset

218 
setup {* map_theory_simpset (put_simpset LK_ss) *} 
17481  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" 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
48891
diff
changeset

224 
apply (tactic {* asm_simp_tac (put_simpset LK_basic_ss @{context}) 1 *}) 
27149  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) 

51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
48891
diff
changeset

229 
apply (tactic {* simp_tac (@{context} addsimps @{thms if_P}) 2 *}) 
27149  230 
apply (rule_tac P = "~Q" in cut) 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
48891
diff
changeset

231 
apply (tactic {* simp_tac (@{context} 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 