summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Decision_Procs/Commutative_Ring_Complete.thy

author | wenzelm |

Wed Sep 07 16:37:50 2011 +0200 (2011-09-07) | |

changeset 44779 | 98d597c4193d |

parent 41807 | ab5d2d81f9fb |

child 53374 | a14d2a854c02 |

permissions | -rw-r--r-- |

tuned proofs;

1 (* Author: Bernhard Haeupler

3 This theory is about of the relative completeness of method comm-ring

4 method. As long as the reified atomic polynomials of type 'a pol are

5 in normal form, the cring method is complete.

6 *)

8 header {* Proof of the relative completeness of method comm-ring *}

10 theory Commutative_Ring_Complete

11 imports Commutative_Ring

12 begin

14 text {* Formalization of normal form *}

15 fun isnorm :: "'a::comm_ring pol \<Rightarrow> bool"

16 where

17 "isnorm (Pc c) \<longleftrightarrow> True"

18 | "isnorm (Pinj i (Pc c)) \<longleftrightarrow> False"

19 | "isnorm (Pinj i (Pinj j Q)) \<longleftrightarrow> False"

20 | "isnorm (Pinj 0 P) \<longleftrightarrow> False"

21 | "isnorm (Pinj i (PX Q1 j Q2)) \<longleftrightarrow> isnorm (PX Q1 j Q2)"

22 | "isnorm (PX P 0 Q) \<longleftrightarrow> False"

23 | "isnorm (PX (Pc c) i Q) \<longleftrightarrow> c \<noteq> 0 \<and> isnorm Q"

24 | "isnorm (PX (PX P1 j (Pc c)) i Q) \<longleftrightarrow> c \<noteq> 0 \<and> isnorm (PX P1 j (Pc c)) \<and> isnorm Q"

25 | "isnorm (PX P i Q) \<longleftrightarrow> isnorm P \<and> isnorm Q"

27 (* Some helpful lemmas *)

28 lemma norm_Pinj_0_False: "isnorm (Pinj 0 P) = False"

29 by (cases P) auto

31 lemma norm_PX_0_False: "isnorm (PX (Pc 0) i Q) = False"

32 by (cases i) auto

34 lemma norm_Pinj: "isnorm (Pinj i Q) \<Longrightarrow> isnorm Q"

35 by (cases i) (simp add: norm_Pinj_0_False norm_PX_0_False, cases Q, auto)

37 lemma norm_PX2: "isnorm (PX P i Q) \<Longrightarrow> isnorm Q"

38 by (cases i) (auto, cases P, auto, case_tac pol2, auto)

40 lemma norm_PX1: "isnorm (PX P i Q) \<Longrightarrow> isnorm P"

41 by (cases i) (auto, cases P, auto, case_tac pol2, auto)

43 lemma mkPinj_cn: "y ~= 0 \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (mkPinj y Q)"

44 apply (auto simp add: mkPinj_def norm_Pinj_0_False split: pol.split)

45 apply (case_tac nat, auto simp add: norm_Pinj_0_False)

46 apply (case_tac pol, auto)

47 apply (case_tac y, auto)

48 done

50 lemma norm_PXtrans:

51 assumes A: "isnorm (PX P x Q)" and "isnorm Q2"

52 shows "isnorm (PX P x Q2)"

53 proof (cases P)

54 case (PX p1 y p2)

55 with assms show ?thesis by (cases x) (auto, cases p2, auto)

56 next

57 case Pc

58 with assms show ?thesis by (cases x) auto

59 next

60 case Pinj

61 with assms show ?thesis by (cases x) auto

62 qed

64 lemma norm_PXtrans2:

65 assumes "isnorm (PX P x Q)" and "isnorm Q2"

66 shows "isnorm (PX P (Suc (n+x)) Q2)"

67 proof (cases P)

68 case (PX p1 y p2)

69 with assms show ?thesis by (cases x) (auto, cases p2, auto)

70 next

71 case Pc

72 with assms show ?thesis by (cases x) auto

73 next

74 case Pinj

75 with assms show ?thesis by (cases x) auto

76 qed

78 text {* mkPX conserves normalizedness (@{text "_cn"}) *}

79 lemma mkPX_cn:

80 assumes "x \<noteq> 0" and "isnorm P" and "isnorm Q"

81 shows "isnorm (mkPX P x Q)"

82 proof(cases P)

83 case (Pc c)

84 with assms show ?thesis by (cases x) (auto simp add: mkPinj_cn mkPX_def)

85 next

86 case (Pinj i Q)

87 with assms show ?thesis by (cases x) (auto simp add: mkPinj_cn mkPX_def)

88 next

89 case (PX P1 y P2)

90 with assms have Y0: "y > 0" by (cases y) auto

91 from assms PX have "isnorm P1" "isnorm P2"

92 by (auto simp add: norm_PX1[of P1 y P2] norm_PX2[of P1 y P2])

93 from assms PX Y0 show ?thesis

94 by (cases x) (auto simp add: mkPX_def norm_PXtrans2[of P1 y _ Q _], cases P2, auto)

95 qed

97 text {* add conserves normalizedness *}

98 lemma add_cn: "isnorm P \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (P \<oplus> Q)"

99 proof (induct P Q rule: add.induct)

100 case (2 c i P2)

101 thus ?case by (cases P2) (simp_all, cases i, simp_all)

102 next

103 case (3 i P2 c)

104 thus ?case by (cases P2) (simp_all, cases i, simp_all)

105 next

106 case (4 c P2 i Q2)

107 then have "isnorm P2" "isnorm Q2"

108 by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])

109 with 4 show ?case

110 by (cases i) (simp, cases P2, auto, case_tac pol2, auto)

111 next

112 case (5 P2 i Q2 c)

113 then have "isnorm P2" "isnorm Q2"

114 by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])

115 with 5 show ?case

116 by (cases i) (simp, cases P2, auto, case_tac pol2, auto)

117 next

118 case (6 x P2 y Q2)

119 then have Y0: "y>0" by (cases y) (auto simp add: norm_Pinj_0_False)

120 with 6 have X0: "x>0" by (cases x) (auto simp add: norm_Pinj_0_False)

121 have "x < y \<or> x = y \<or> x > y" by arith

122 moreover

123 { assume "x<y" hence "EX d. y =d + x" by arith

124 then obtain d where y: "y = d + x" ..

125 moreover

126 note 6 X0

127 moreover

128 from 6 have "isnorm P2" "isnorm Q2"

129 by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])

130 moreover

131 from 6 `x < y` y have "isnorm (Pinj d Q2)"

132 by (cases d, simp, cases Q2, auto)

133 ultimately have ?case by (simp add: mkPinj_cn) }

134 moreover

135 { assume "x=y"

136 moreover

137 from 6 have "isnorm P2" "isnorm Q2"

138 by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])

139 moreover

140 note 6 Y0

141 moreover

142 ultimately have ?case by (simp add: mkPinj_cn) }

143 moreover

144 { assume "x>y" hence "EX d. x = d + y" by arith

145 then obtain d where x: "x = d + y"..

146 moreover

147 note 6 Y0

148 moreover

149 from 6 have "isnorm P2" "isnorm Q2"

150 by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])

151 moreover

152 from 6 `x > y` x have "isnorm (Pinj d P2)"

153 by (cases d) (simp, cases P2, auto)

154 ultimately have ?case by (simp add: mkPinj_cn) }

155 ultimately show ?case by blast

156 next

157 case (7 x P2 Q2 y R)

158 have "x = 0 \<or> x = 1 \<or> x > 1" by arith

159 moreover

160 { assume "x = 0"

161 with 7 have ?case by (auto simp add: norm_Pinj_0_False) }

162 moreover

163 { assume "x = 1"

164 from 7 have "isnorm R" "isnorm P2"

165 by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])

166 with 7 `x = 1` have "isnorm (R \<oplus> P2)" by simp

167 with 7 `x = 1` have ?case

168 by (simp add: norm_PXtrans[of Q2 y _]) }

169 moreover

170 { assume "x > 1" hence "EX d. x=Suc (Suc d)" by arith

171 then obtain d where X: "x=Suc (Suc d)" ..

172 with 7 have NR: "isnorm R" "isnorm P2"

173 by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])

174 with 7 X have "isnorm (Pinj (x - 1) P2)" by (cases P2) auto

175 with 7 X NR have "isnorm (R \<oplus> Pinj (x - 1) P2)" by simp

176 with `isnorm (PX Q2 y R)` X have ?case

177 by (simp add: norm_PXtrans[of Q2 y _]) }

178 ultimately show ?case by blast

179 next

180 case (8 Q2 y R x P2)

181 have "x = 0 \<or> x = 1 \<or> x > 1" by arith

182 moreover

183 { assume "x = 0" with 8 have ?case by (auto simp add: norm_Pinj_0_False) }

184 moreover

185 { assume "x = 1"

186 with 8 have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])

187 with 8 `x = 1` have "isnorm (R \<oplus> P2)" by simp

188 with 8 `x = 1` have ?case by (simp add: norm_PXtrans[of Q2 y _]) }

189 moreover

190 { assume "x > 1" hence "EX d. x=Suc (Suc d)" by arith

191 then obtain d where X: "x = Suc (Suc d)" ..

192 with 8 have NR: "isnorm R" "isnorm P2"

193 by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])

194 with 8 X have "isnorm (Pinj (x - 1) P2)" by (cases P2) auto

195 with 8 `x > 1` NR have "isnorm (R \<oplus> Pinj (x - 1) P2)" by simp

196 with `isnorm (PX Q2 y R)` X have ?case by (simp add: norm_PXtrans[of Q2 y _]) }

197 ultimately show ?case by blast

198 next

199 case (9 P1 x P2 Q1 y Q2)

200 then have Y0: "y>0" by (cases y) auto

201 with 9 have X0: "x>0" by (cases x) auto

202 with 9 have NP1: "isnorm P1" and NP2: "isnorm P2"

203 by (auto simp add: norm_PX1[of P1 _ P2] norm_PX2[of P1 _ P2])

204 with 9 have NQ1: "isnorm Q1" and NQ2: "isnorm Q2"

205 by (auto simp add: norm_PX1[of Q1 _ Q2] norm_PX2[of Q1 _ Q2])

206 have "y < x \<or> x = y \<or> x < y" by arith

207 moreover

208 { assume sm1: "y < x" hence "EX d. x = d + y" by arith

209 then obtain d where sm2: "x = d + y" ..

210 note 9 NQ1 NP1 NP2 NQ2 sm1 sm2

211 moreover

212 have "isnorm (PX P1 d (Pc 0))"

213 proof (cases P1)

214 case (PX p1 y p2)

215 with 9 sm1 sm2 show ?thesis by (cases d) (simp, cases p2, auto)

216 next

217 case Pc with 9 sm1 sm2 show ?thesis by (cases d) auto

218 next

219 case Pinj with 9 sm1 sm2 show ?thesis by (cases d) auto

220 qed

221 ultimately have "isnorm (P2 \<oplus> Q2)" "isnorm (PX P1 (x - y) (Pc 0) \<oplus> Q1)" by auto

222 with Y0 sm1 sm2 have ?case by (simp add: mkPX_cn) }

223 moreover

224 { assume "x = y"

225 with 9 NP1 NP2 NQ1 NQ2 have "isnorm (P2 \<oplus> Q2)" "isnorm (P1 \<oplus> Q1)" by auto

226 with `x = y` Y0 have ?case by (simp add: mkPX_cn) }

227 moreover

228 { assume sm1: "x < y" hence "EX d. y = d + x" by arith

229 then obtain d where sm2: "y = d + x" ..

230 note 9 NQ1 NP1 NP2 NQ2 sm1 sm2

231 moreover

232 have "isnorm (PX Q1 d (Pc 0))"

233 proof (cases Q1)

234 case (PX p1 y p2)

235 with 9 sm1 sm2 show ?thesis by (cases d) (simp, cases p2, auto)

236 next

237 case Pc with 9 sm1 sm2 show ?thesis by (cases d) auto

238 next

239 case Pinj with 9 sm1 sm2 show ?thesis by (cases d) auto

240 qed

241 ultimately have "isnorm (P2 \<oplus> Q2)" "isnorm (PX Q1 (y - x) (Pc 0) \<oplus> P1)" by auto

242 with X0 sm1 sm2 have ?case by (simp add: mkPX_cn) }

243 ultimately show ?case by blast

244 qed simp

246 text {* mul concerves normalizedness *}

247 lemma mul_cn: "isnorm P \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (P \<otimes> Q)"

248 proof (induct P Q rule: mul.induct)

249 case (2 c i P2) thus ?case

250 by (cases P2) (simp_all, cases i, simp_all add: mkPinj_cn)

251 next

252 case (3 i P2 c) thus ?case

253 by (cases P2) (simp_all, cases i, simp_all add: mkPinj_cn)

254 next

255 case (4 c P2 i Q2)

256 then have "isnorm P2" "isnorm Q2"

257 by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])

258 with 4 show ?case

259 by (cases "c = 0") (simp_all, cases "i = 0", simp_all add: mkPX_cn)

260 next

261 case (5 P2 i Q2 c)

262 then have "isnorm P2" "isnorm Q2"

263 by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])

264 with 5 show ?case

265 by (cases "c = 0") (simp_all, cases "i = 0", simp_all add: mkPX_cn)

266 next

267 case (6 x P2 y Q2)

268 have "x < y \<or> x = y \<or> x > y" by arith

269 moreover

270 { assume "x < y" hence "EX d. y = d + x" by arith

271 then obtain d where y: "y = d + x" ..

272 moreover

273 note 6

274 moreover

275 from 6 have "x > 0" by (cases x) (auto simp add: norm_Pinj_0_False)

276 moreover

277 from 6 have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])

278 moreover

279 from 6 `x < y` y have "isnorm (Pinj d Q2)" by (cases d) (simp, cases Q2, auto)

280 ultimately have ?case by (simp add: mkPinj_cn) }

281 moreover

282 { assume "x = y"

283 moreover

284 from 6 have "isnorm P2" "isnorm Q2" by(auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])

285 moreover

286 from 6 have "y>0" by (cases y) (auto simp add: norm_Pinj_0_False)

287 moreover

288 note 6

289 moreover

290 ultimately have ?case by (simp add: mkPinj_cn) }

291 moreover

292 { assume "x > y" hence "EX d. x = d + y" by arith

293 then obtain d where x: "x = d + y" ..

294 moreover

295 note 6

296 moreover

297 from 6 have "y > 0" by (cases y) (auto simp add: norm_Pinj_0_False)

298 moreover

299 from 6 have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])

300 moreover

301 from 6 `x > y` x have "isnorm (Pinj d P2)" by (cases d) (simp, cases P2, auto)

302 ultimately have ?case by (simp add: mkPinj_cn) }

303 ultimately show ?case by blast

304 next

305 case (7 x P2 Q2 y R)

306 then have Y0: "y > 0" by (cases y) auto

307 have "x = 0 \<or> x = 1 \<or> x > 1" by arith

308 moreover

309 { assume "x = 0" with 7 have ?case by (auto simp add: norm_Pinj_0_False) }

310 moreover

311 { assume "x = 1"

312 from 7 have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])

313 with 7 `x = 1` have "isnorm (R \<otimes> P2)" "isnorm Q2" by (auto simp add: norm_PX1[of Q2 y R])

314 with 7 `x = 1` Y0 have ?case by (simp add: mkPX_cn) }

315 moreover

316 { assume "x > 1" hence "EX d. x = Suc (Suc d)" by arith

317 then obtain d where X: "x = Suc (Suc d)" ..

318 from 7 have NR: "isnorm R" "isnorm Q2"

319 by (auto simp add: norm_PX2[of Q2 y R] norm_PX1[of Q2 y R])

320 moreover

321 from 7 X have "isnorm (Pinj (x - 1) P2)" by (cases P2) auto

322 moreover

323 from 7 have "isnorm (Pinj x P2)" by (cases P2) auto

324 moreover

325 note 7 X

326 ultimately have "isnorm (R \<otimes> Pinj (x - 1) P2)" "isnorm (Pinj x P2 \<otimes> Q2)" by auto

327 with Y0 X have ?case by (simp add: mkPX_cn) }

328 ultimately show ?case by blast

329 next

330 case (8 Q2 y R x P2)

331 then have Y0: "y>0" by (cases y) auto

332 have "x = 0 \<or> x = 1 \<or> x > 1" by arith

333 moreover

334 { assume "x = 0" with 8 have ?case by (auto simp add: norm_Pinj_0_False) }

335 moreover

336 { assume "x = 1"

337 from 8 have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])

338 with 8 `x = 1` have "isnorm (R \<otimes> P2)" "isnorm Q2" by (auto simp add: norm_PX1[of Q2 y R])

339 with 8 `x = 1` Y0 have ?case by (simp add: mkPX_cn) }

340 moreover

341 { assume "x > 1" hence "EX d. x = Suc (Suc d)" by arith

342 then obtain d where X: "x = Suc (Suc d)" ..

343 from 8 have NR: "isnorm R" "isnorm Q2"

344 by (auto simp add: norm_PX2[of Q2 y R] norm_PX1[of Q2 y R])

345 moreover

346 from 8 X have "isnorm (Pinj (x - 1) P2)" by (cases P2) auto

347 moreover

348 from 8 X have "isnorm (Pinj x P2)" by (cases P2) auto

349 moreover

350 note 8 X

351 ultimately have "isnorm (R \<otimes> Pinj (x - 1) P2)" "isnorm (Pinj x P2 \<otimes> Q2)" by auto

352 with Y0 X have ?case by (simp add: mkPX_cn) }

353 ultimately show ?case by blast

354 next

355 case (9 P1 x P2 Q1 y Q2)

356 from 9 have X0: "x > 0" by (cases x) auto

357 from 9 have Y0: "y > 0" by (cases y) auto

358 note 9

359 moreover

360 from 9 have "isnorm P1" "isnorm P2" by (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2])

361 moreover

362 from 9 have "isnorm Q1" "isnorm Q2" by (auto simp add: norm_PX1[of Q1 y Q2] norm_PX2[of Q1 y Q2])

363 ultimately have "isnorm (P1 \<otimes> Q1)" "isnorm (P2 \<otimes> Q2)"

364 "isnorm (P1 \<otimes> mkPinj 1 Q2)" "isnorm (Q1 \<otimes> mkPinj 1 P2)"

365 by (auto simp add: mkPinj_cn)

366 with 9 X0 Y0 have

367 "isnorm (mkPX (P1 \<otimes> Q1) (x + y) (P2 \<otimes> Q2))"

368 "isnorm (mkPX (P1 \<otimes> mkPinj (Suc 0) Q2) x (Pc 0))"

369 "isnorm (mkPX (Q1 \<otimes> mkPinj (Suc 0) P2) y (Pc 0))"

370 by (auto simp add: mkPX_cn)

371 thus ?case by (simp add: add_cn)

372 qed simp

374 text {* neg conserves normalizedness *}

375 lemma neg_cn: "isnorm P \<Longrightarrow> isnorm (neg P)"

376 proof (induct P)

377 case (Pinj i P2)

378 then have "isnorm P2" by (simp add: norm_Pinj[of i P2])

379 with Pinj show ?case by (cases P2) (auto, cases i, auto)

380 next

381 case (PX P1 x P2) note PX1 = this

382 from PX have "isnorm P2" "isnorm P1"

383 by (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2])

384 with PX show ?case

385 proof (cases P1)

386 case (PX p1 y p2)

387 with PX1 show ?thesis by (cases x) (auto, cases p2, auto)

388 next

389 case Pinj

390 with PX1 show ?thesis by (cases x) auto

391 qed (cases x, auto)

392 qed simp

394 text {* sub conserves normalizedness *}

395 lemma sub_cn: "isnorm p \<Longrightarrow> isnorm q \<Longrightarrow> isnorm (p \<ominus> q)"

396 by (simp add: sub_def add_cn neg_cn)

398 text {* sqr conserves normalizizedness *}

399 lemma sqr_cn: "isnorm P \<Longrightarrow> isnorm (sqr P)"

400 proof (induct P)

401 case Pc

402 then show ?case by simp

403 next

404 case (Pinj i Q)

405 then show ?case

406 by (cases Q) (auto simp add: mkPX_cn mkPinj_cn, cases i, auto simp add: mkPX_cn mkPinj_cn)

407 next

408 case (PX P1 x P2)

409 then have "x + x ~= 0" "isnorm P2" "isnorm P1"

410 by (cases x, auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2])

411 with PX have "isnorm (mkPX (Pc (1 + 1) \<otimes> P1 \<otimes> mkPinj (Suc 0) P2) x (Pc 0))"

412 and "isnorm (mkPX (sqr P1) (x + x) (sqr P2))"

413 by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn)

414 then show ?case by (auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn)

415 qed

417 text {* pow conserves normalizedness *}

418 lemma pow_cn: "isnorm P \<Longrightarrow> isnorm (pow n P)"

419 proof (induct n arbitrary: P rule: less_induct)

420 case (less k)

421 show ?case

422 proof (cases "k = 0")

423 case True

424 then show ?thesis by simp

425 next

426 case False

427 then have K2: "k div 2 < k" by (cases k) auto

428 from less have "isnorm (sqr P)" by (simp add: sqr_cn)

429 with less False K2 show ?thesis

430 by (simp add: allE[of _ "(k div 2)" _] allE[of _ "(sqr P)" _], cases k, auto simp add: mul_cn)

431 qed

432 qed

434 end