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

src/HOL/Decision_Procs/Commutative_Ring_Complete.thy

author | blanchet |

Thu Sep 11 18:54:36 2014 +0200 (2014-09-11) | |

changeset 58306 | 117ba6cbe414 |

parent 58259 | 52c35a59bbf5 |

child 58710 | 7216a10d69ba |

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

renamed 'rep_datatype' to 'old_rep_datatype' (HOL)

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 apply (cases i)

39 apply auto

40 apply (cases P)

41 apply auto

42 apply (rename_tac pol2, case_tac pol2)

43 apply auto

44 done

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

47 apply (cases i)

48 apply auto

49 apply (cases P)

50 apply auto

51 apply (rename_tac pol2, case_tac pol2)

52 apply auto

53 done

55 lemma mkPinj_cn: "y \<noteq> 0 \<Longrightarrow> isnorm Q \<Longrightarrow> isnorm (mkPinj y Q)"

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

57 apply (rename_tac nat a, case_tac nat, auto simp add: norm_Pinj_0_False)

58 apply (rename_tac pol a, case_tac pol, auto)

59 apply (case_tac y, auto)

60 done

62 lemma norm_PXtrans:

63 assumes A: "isnorm (PX P x Q)"

64 and "isnorm Q2"

65 shows "isnorm (PX P x Q2)"

66 proof (cases P)

67 case (PX p1 y p2)

68 with assms show ?thesis

69 apply (cases x)

70 apply auto

71 apply (cases p2)

72 apply auto

73 done

74 next

75 case Pc

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

77 next

78 case Pinj

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

80 qed

82 lemma norm_PXtrans2:

83 assumes "isnorm (PX P x Q)"

84 and "isnorm Q2"

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

86 proof (cases P)

87 case (PX p1 y p2)

88 with assms show ?thesis

89 apply (cases x)

90 apply auto

91 apply (cases p2)

92 apply auto

93 done

94 next

95 case Pc

96 with assms show ?thesis

97 by (cases x) auto

98 next

99 case Pinj

100 with assms show ?thesis

101 by (cases x) auto

102 qed

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

105 lemma mkPX_cn:

106 assumes "x \<noteq> 0"

107 and "isnorm P"

108 and "isnorm Q"

109 shows "isnorm (mkPX P x Q)"

110 proof (cases P)

111 case (Pc c)

112 with assms show ?thesis

113 by (cases x) (auto simp add: mkPinj_cn mkPX_def)

114 next

115 case (Pinj i Q)

116 with assms show ?thesis

117 by (cases x) (auto simp add: mkPinj_cn mkPX_def)

118 next

119 case (PX P1 y P2)

120 with assms have Y0: "y > 0"

121 by (cases y) auto

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

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

124 from assms PX Y0 show ?thesis

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

126 qed

128 text {* add conserves normalizedness *}

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

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

131 case (2 c i P2)

132 then show ?case

133 by (cases P2) (simp_all, cases i, simp_all)

134 next

135 case (3 i P2 c)

136 then show ?case

137 by (cases P2) (simp_all, cases i, simp_all)

138 next

139 case (4 c P2 i Q2)

140 then have "isnorm P2" "isnorm Q2"

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

142 with 4 show ?case

143 by (cases i) (simp, cases P2, auto, rename_tac pol2, case_tac pol2, auto)

144 next

145 case (5 P2 i Q2 c)

146 then have "isnorm P2" "isnorm Q2"

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

148 with 5 show ?case

149 by (cases i) (simp, cases P2, auto, rename_tac pol2, case_tac pol2, auto)

150 next

151 case (6 x P2 y Q2)

152 then have Y0: "y > 0"

153 by (cases y) (auto simp add: norm_Pinj_0_False)

154 with 6 have X0: "x > 0"

155 by (cases x) (auto simp add: norm_Pinj_0_False)

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

157 moreover {

158 assume "x < y"

159 then have "\<exists>d. y = d + x" by arith

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

161 moreover

162 note 6 X0

163 moreover

164 from 6 have "isnorm P2" "isnorm Q2"

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

166 moreover

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

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

169 ultimately have ?case by (simp add: mkPinj_cn)

170 }

171 moreover {

172 assume "x = y"

173 moreover

174 from 6 have "isnorm P2" "isnorm Q2"

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

176 moreover

177 note 6 Y0

178 ultimately have ?case by (simp add: mkPinj_cn)

179 }

180 moreover {

181 assume "x > y"

182 then have "\<exists>d. x = d + y"

183 by arith

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

185 moreover

186 note 6 Y0

187 moreover

188 from 6 have "isnorm P2" "isnorm Q2"

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

190 moreover

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

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

193 ultimately have ?case by (simp add: mkPinj_cn)

194 }

195 ultimately show ?case by blast

196 next

197 case (7 x P2 Q2 y R)

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

199 moreover {

200 assume "x = 0"

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

202 }

203 moreover {

204 assume "x = 1"

205 from 7 have "isnorm R" "isnorm P2"

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

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

208 with 7 `x = 1` have ?case

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

210 }

211 moreover {

212 assume "x > 1" then have "\<exists>d. x=Suc (Suc d)" by arith

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

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

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

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

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

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

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

220 }

221 ultimately show ?case by blast

222 next

223 case (8 Q2 y R x P2)

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

225 moreover {

226 assume "x = 0"

227 with 8 have ?case

228 by (auto simp add: norm_Pinj_0_False)

229 }

230 moreover {

231 assume "x = 1"

232 with 8 have "isnorm R" "isnorm P2"

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

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

235 by simp

236 with 8 `x = 1` have ?case

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

238 }

239 moreover {

240 assume "x > 1"

241 then have "\<exists>d. x = Suc (Suc d)" by arith

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

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

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

245 with 8 X have "isnorm (Pinj (x - 1) P2)"

246 by (cases P2) auto

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

248 by simp

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

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

251 }

252 ultimately show ?case by blast

253 next

254 case (9 P1 x P2 Q1 y Q2)

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

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

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

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

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

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

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

262 moreover {

263 assume sm1: "y < x"

264 then have "\<exists>d. x = d + y" by arith

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

266 note 9 NQ1 NP1 NP2 NQ2 sm1 sm2

267 moreover

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

269 proof (cases P1)

270 case (PX p1 y p2)

271 with 9 sm1 sm2 show ?thesis

272 by (cases d) (simp, cases p2, auto)

273 next

274 case Pc

275 with 9 sm1 sm2 show ?thesis

276 by (cases d) auto

277 next

278 case Pinj

279 with 9 sm1 sm2 show ?thesis

280 by (cases d) auto

281 qed

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

283 by auto

284 with Y0 sm1 sm2 have ?case

285 by (simp add: mkPX_cn)

286 }

287 moreover {

288 assume "x = y"

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

290 by auto

291 with `x = y` Y0 have ?case

292 by (simp add: mkPX_cn)

293 }

294 moreover {

295 assume sm1: "x < y"

296 then have "\<exists>d. y = d + x" by arith

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

298 note 9 NQ1 NP1 NP2 NQ2 sm1 sm2

299 moreover

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

301 proof (cases Q1)

302 case (PX p1 y p2)

303 with 9 sm1 sm2 show ?thesis

304 by (cases d) (simp, cases p2, auto)

305 next

306 case Pc

307 with 9 sm1 sm2 show ?thesis

308 by (cases d) auto

309 next

310 case Pinj

311 with 9 sm1 sm2 show ?thesis

312 by (cases d) auto

313 qed

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

315 by auto

316 with X0 sm1 sm2 have ?case

317 by (simp add: mkPX_cn)

318 }

319 ultimately show ?case by blast

320 qed simp

322 text {* mul concerves normalizedness *}

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

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

325 case (2 c i P2)

326 then show ?case

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

328 next

329 case (3 i P2 c)

330 then show ?case

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

332 next

333 case (4 c P2 i Q2)

334 then have "isnorm P2" "isnorm Q2"

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

336 with 4 show ?case

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

338 next

339 case (5 P2 i Q2 c)

340 then have "isnorm P2" "isnorm Q2"

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

342 with 5 show ?case

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

344 next

345 case (6 x P2 y Q2)

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

347 moreover {

348 assume "x < y"

349 then have "\<exists>d. y = d + x" by arith

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

351 moreover

352 note 6

353 moreover

354 from 6 have "x > 0"

355 by (cases x) (auto simp add: norm_Pinj_0_False)

356 moreover

357 from 6 have "isnorm P2" "isnorm Q2"

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

359 moreover

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

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

362 ultimately have ?case by (simp add: mkPinj_cn)

363 }

364 moreover {

365 assume "x = y"

366 moreover

367 from 6 have "isnorm P2" "isnorm Q2"

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

369 moreover

370 from 6 have "y>0"

371 by (cases y) (auto simp add: norm_Pinj_0_False)

372 moreover

373 note 6

374 ultimately have ?case by (simp add: mkPinj_cn)

375 }

376 moreover {

377 assume "x > y"

378 then have "\<exists>d. x = d + y" by arith

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

380 moreover

381 note 6

382 moreover

383 from 6 have "y > 0"

384 by (cases y) (auto simp add: norm_Pinj_0_False)

385 moreover

386 from 6 have "isnorm P2" "isnorm Q2"

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

388 moreover

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

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

391 ultimately have ?case by (simp add: mkPinj_cn)

392 }

393 ultimately show ?case by blast

394 next

395 case (7 x P2 Q2 y R)

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

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

398 moreover {

399 assume "x = 0"

400 with 7 have ?case

401 by (auto simp add: norm_Pinj_0_False)

402 }

403 moreover {

404 assume "x = 1"

405 from 7 have "isnorm R" "isnorm P2"

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

407 with 7 `x = 1` have "isnorm (R \<otimes> P2)" "isnorm Q2"

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

409 with 7 `x = 1` Y0 have ?case

410 by (simp add: mkPX_cn)

411 }

412 moreover {

413 assume "x > 1"

414 then have "\<exists>d. x = Suc (Suc d)"

415 by arith

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

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

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

419 moreover

420 from 7 X have "isnorm (Pinj (x - 1) P2)"

421 by (cases P2) auto

422 moreover

423 from 7 have "isnorm (Pinj x P2)"

424 by (cases P2) auto

425 moreover

426 note 7 X

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

428 by auto

429 with Y0 X have ?case

430 by (simp add: mkPX_cn)

431 }

432 ultimately show ?case by blast

433 next

434 case (8 Q2 y R x P2)

435 then have Y0: "y > 0"

436 by (cases y) auto

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

438 moreover {

439 assume "x = 0"

440 with 8 have ?case

441 by (auto simp add: norm_Pinj_0_False)

442 }

443 moreover {

444 assume "x = 1"

445 from 8 have "isnorm R" "isnorm P2"

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

447 with 8 `x = 1` have "isnorm (R \<otimes> P2)" "isnorm Q2"

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

449 with 8 `x = 1` Y0 have ?case

450 by (simp add: mkPX_cn)

451 }

452 moreover {

453 assume "x > 1"

454 then have "\<exists>d. x = Suc (Suc d)" by arith

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

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

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

458 moreover

459 from 8 X have "isnorm (Pinj (x - 1) P2)"

460 by (cases P2) auto

461 moreover

462 from 8 X have "isnorm (Pinj x P2)"

463 by (cases P2) auto

464 moreover

465 note 8 X

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

467 by auto

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

469 }

470 ultimately show ?case by blast

471 next

472 case (9 P1 x P2 Q1 y Q2)

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

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

475 note 9

476 moreover

477 from 9 have "isnorm P1" "isnorm P2"

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

479 moreover

480 from 9 have "isnorm Q1" "isnorm Q2"

481 by (auto simp add: norm_PX1[of Q1 y Q2] norm_PX2[of Q1 y Q2])

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

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

484 by (auto simp add: mkPinj_cn)

485 with 9 X0 Y0 have

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

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

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

489 by (auto simp add: mkPX_cn)

490 then show ?case by (simp add: add_cn)

491 qed simp

493 text {* neg conserves normalizedness *}

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

495 proof (induct P)

496 case (Pinj i P2)

497 then have "isnorm P2"

498 by (simp add: norm_Pinj[of i P2])

499 with Pinj show ?case

500 by (cases P2) (auto, cases i, auto)

501 next

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

503 from PX have "isnorm P2" "isnorm P1"

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

505 with PX show ?case

506 proof (cases P1)

507 case (PX p1 y p2)

508 with PX1 show ?thesis

509 by (cases x) (auto, cases p2, auto)

510 next

511 case Pinj

512 with PX1 show ?thesis

513 by (cases x) auto

514 qed (cases x, auto)

515 qed simp

517 text {* sub conserves normalizedness *}

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

519 by (simp add: sub_def add_cn neg_cn)

521 text {* sqr conserves normalizizedness *}

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

523 proof (induct P)

524 case Pc

525 then show ?case by simp

526 next

527 case (Pinj i Q)

528 then show ?case

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

530 next

531 case (PX P1 x P2)

532 then have "x + x \<noteq> 0" "isnorm P2" "isnorm P1"

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

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

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

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

537 then show ?case

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

539 qed

541 text {* pow conserves normalizedness *}

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

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

544 case (less k)

545 show ?case

546 proof (cases "k = 0")

547 case True

548 then show ?thesis by simp

549 next

550 case False

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

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

553 with less False K2 show ?thesis

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

555 qed

556 qed

558 end