# Theory Commutative_Ring_Complete

```(*  Author:     Bernhard Haeupler

This theory is about of the relative completeness of the ring
method.  As long as the reified atomic polynomials of type pol are
in normal form, the ring method is complete.
*)

section ‹Proof of the relative completeness of method comm-ring›

theory Commutative_Ring_Complete
imports Commutative_Ring
begin

text ‹Formalization of normal form›
fun isnorm :: "pol ⇒ bool"
where
"isnorm (Pc c) ⟷ True"
| "isnorm (Pinj i (Pc c)) ⟷ False"
| "isnorm (Pinj i (Pinj j Q)) ⟷ False"
| "isnorm (Pinj 0 P) ⟷ False"
| "isnorm (Pinj i (PX Q1 j Q2)) ⟷ isnorm (PX Q1 j Q2)"
| "isnorm (PX P 0 Q) ⟷ False"
| "isnorm (PX (Pc c) i Q) ⟷ c ≠ 0 ∧ isnorm Q"
| "isnorm (PX (PX P1 j (Pc c)) i Q) ⟷ c ≠ 0 ∧ isnorm (PX P1 j (Pc c)) ∧ isnorm Q"
| "isnorm (PX P i Q) ⟷ isnorm P ∧ isnorm Q"

lemma norm_Pinj_0_False: "isnorm (Pinj 0 P) = False"
by (cases P) auto

lemma norm_PX_0_False: "isnorm (PX (Pc 0) i Q) = False"
by (cases i) auto

lemma norm_Pinj: "isnorm (Pinj i Q) ⟹ isnorm Q"
using isnorm.elims(2) by fastforce

lemma norm_PX2: "isnorm (PX P i Q) ⟹ isnorm Q"
using isnorm.elims(1) by auto

lemma norm_PX1: assumes "isnorm (PX P i Q)" shows "isnorm P"
proof (cases P)
case (Pc x1)
then show ?thesis
by auto
qed (use assms isnorm.elims(1) in auto)

lemma mkPinj_cn:
assumes "y ≠ 0" and "isnorm Q"
shows "isnorm (mkPinj y Q)"
proof (cases Q)
case Pc
with assms show ?thesis
next
case Pinj
with assms show ?thesis
using isnorm.elims(2) isnorm.simps(5) mkPinj_def by fastforce
next
case PX
with assms show ?thesis
using isnorm.elims(1) mkPinj_def by auto
qed

lemma norm_PXtrans:
assumes "isnorm (PX P x Q)" and "isnorm Q2"
shows "isnorm (PX P x Q2)"
using assms isnorm.elims(3) by fastforce

lemma norm_PXtrans2:
assumes "isnorm (PX P x Q)"
and "isnorm Q2"
shows "isnorm (PX P (Suc (n + x)) Q2)"
proof (cases P)
case (PX p1 y p2)
with assms show ?thesis
using isnorm.elims(2) by fastforce
next
case Pc
with assms show ?thesis
by (cases x) auto
next
case Pinj
with assms show ?thesis
by (cases x) auto
qed

text ‹‹mkPX› preserves the normal property (‹_cn›)›
lemma mkPX_cn:
assumes "x ≠ 0"
and "isnorm P"
and "isnorm Q"
shows "isnorm (mkPX P x Q)"
proof (cases P)
case (Pc c)
with assms show ?thesis
by (cases x) (auto simp add: mkPinj_cn mkPX_def)
next
case (Pinj i Q)
with assms show ?thesis
by (cases x) (auto simp add: mkPinj_cn mkPX_def)
next
case (PX P1 y P2)
with assms have Y0: "y > 0"
by (cases y) auto
from assms PX have "isnorm P1" "isnorm P2"
by (auto simp add: norm_PX1[of P1 y P2] norm_PX2[of P1 y P2])
from assms PX Y0 show ?thesis
proof (cases P2)
case (Pc x1)
then show ?thesis
using assms gr0_conv_Suc PX by (auto simp add: mkPX_def norm_PXtrans2)
next
case (Pinj x21 x22)
with assms gr0_conv_Suc PX show ?thesis
by (auto simp: mkPX_def)
next
case (PX x31 x32 x33)
with assms gr0_conv_Suc ‹P = PX P1 y P2›
show ?thesis
using assms PX by (auto simp add: mkPX_def norm_PXtrans2)
qed
qed

text ‹‹add› preserves the normal property›
lemma add_cn: "isnorm P ⟹ isnorm Q ⟹ isnorm (P ⟨+⟩ Q)"
proof (induct P Q rule: add.induct)
case 1
then show ?case by simp
next
case (2 c i P2)
then show ?case
using isnorm.elims(2) by fastforce
next
case (3 i P2 c)
then show ?case
using isnorm.elims(2) by fastforce
next
case (4 c P2 i Q2)
then have "isnorm P2" "isnorm Q2"
by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
with 4 show ?case
using isnorm.elims(2) by fastforce
next
case (5 P2 i Q2 c)
then have "isnorm P2" "isnorm Q2"
by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
with 5 show ?case
using isnorm.elims(2) by fastforce
next
case (6 x P2 y Q2)
then have Y0: "y > 0"
by (cases y) (auto simp add: norm_Pinj_0_False)
with 6 have X0: "x > 0"
by (cases x) (auto simp add: norm_Pinj_0_False)
consider "x < y" | "x = y" | "x > y" by arith
then show ?case
proof cases
case xy: 1
then obtain d where y: "y = d + x"
by atomize_elim arith
from 6 have *: "isnorm P2" "isnorm Q2"
by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
from 6 xy y have "isnorm (Pinj d Q2)"
by (cases d, simp, cases Q2, auto)
with 6 X0 y * show ?thesis
next
case xy: 2
from 6 have "isnorm P2" "isnorm Q2"
by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
with xy 6 Y0 show ?thesis
next
case xy: 3
then obtain d where x: "x = d + y"
by atomize_elim arith
from 6 have *: "isnorm P2" "isnorm Q2"
by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
from 6 xy x have "isnorm (Pinj d P2)"
by (cases d) (simp, cases P2, auto)
with xy 6 Y0 * x show ?thesis by (simp add: mkPinj_cn)
qed
next
case (7 x P2 Q2 y R)
consider "x = 0" | "x = 1" | d where "x = Suc (Suc d)"
by atomize_elim arith
then show ?case
proof cases
case 1
with 7 show ?thesis
next
case x: 2
from 7 have "isnorm R" "isnorm P2"
by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
with 7 x have "isnorm (R ⟨+⟩ P2)"
by simp
with 7 x show ?thesis
by (simp add: norm_PXtrans[of Q2 y _])
next
case x: 3
with 7 have NR: "isnorm R" "isnorm P2"
by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
with 7 x have "isnorm (Pinj (x - 1) P2)"
by (cases P2) auto
with 7 x NR have "isnorm (R ⟨+⟩ Pinj (x - 1) P2)"
by simp
with ‹isnorm (PX Q2 y R)› x show ?thesis
by (simp add: norm_PXtrans[of Q2 y _])
qed
next
case (8 Q2 y R x P2)
consider "x = 0" | "x = 1" | "x > 1"
by arith
then show ?case
proof cases
case 1
with 8 show ?thesis
next
case x: 2
with 8 have "isnorm R" "isnorm P2"
by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
with 8 x have "isnorm (R ⟨+⟩ P2)"
by simp
with 8 x show ?thesis
by (simp add: norm_PXtrans[of Q2 y _])
next
case x: 3
then obtain d where x: "x = Suc (Suc d)" by atomize_elim arith
with 8 have NR: "isnorm R" "isnorm P2"
by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
with 8 x have "isnorm (Pinj (x - 1) P2)"
by (cases P2) auto
with 8 x NR have "isnorm (R ⟨+⟩ Pinj (x - 1) P2)"
by simp
with ‹isnorm (PX Q2 y R)› x show ?thesis
by (simp add: norm_PXtrans[of Q2 y _])
qed
next
case (9 P1 x P2 Q1 y Q2)
then have Y0: "y > 0" by (cases y) auto
with 9 have X0: "x > 0" by (cases x) auto
with 9 have NP1: "isnorm P1" and NP2: "isnorm P2"
by (auto simp add: norm_PX1[of P1 _ P2] norm_PX2[of P1 _ P2])
with 9 have NQ1: "isnorm Q1" and NQ2: "isnorm Q2"
by (auto simp add: norm_PX1[of Q1 _ Q2] norm_PX2[of Q1 _ Q2])
consider "y < x" | "x = y" | "x < y" by arith
then show ?case
proof cases
case xy: 1
then obtain d where x: "x = d + y"
by atomize_elim arith
have "isnorm (PX P1 d (Pc 0))"
proof (cases P1)
case (PX p1 y p2)
with 9 xy x show ?thesis
by (cases d) (simp, cases p2, auto)
next
case Pc
with 9 xy x show ?thesis
by (cases d) auto
next
case Pinj
with 9 xy x show ?thesis
by (cases d) auto
qed
with 9 NQ1 NP1 NP2 NQ2 xy x have "isnorm (P2 ⟨+⟩ Q2)" "isnorm (PX P1 (x - y) (Pc 0) ⟨+⟩ Q1)"
by auto
with Y0 xy x show ?thesis
next
case xy: 2
with 9 NP1 NP2 NQ1 NQ2 have "isnorm (P2 ⟨+⟩ Q2)" "isnorm (P1 ⟨+⟩ Q1)"
by auto
with xy Y0 show ?thesis
next
case xy: 3
then obtain d where y: "y = d + x"
by atomize_elim arith
have "isnorm (PX Q1 d (Pc 0))"
proof (cases Q1)
case (PX p1 y p2)
with 9 xy y show ?thesis
by (cases d) (simp, cases p2, auto)
next
case Pc
with 9 xy y show ?thesis
by (cases d) auto
next
case Pinj
with 9 xy y show ?thesis
by (cases d) auto
qed
with 9 NQ1 NP1 NP2 NQ2 xy y have "isnorm (P2 ⟨+⟩ Q2)" "isnorm (PX Q1 (y - x) (Pc 0) ⟨+⟩ P1)"
by auto
with X0 xy y show ?thesis
qed
qed

text ‹‹mul› concerves normalizedness›
lemma mul_cn: "isnorm P ⟹ isnorm Q ⟹ isnorm (P ⟨*⟩ Q)"
proof (induct P Q rule: mul.induct)
case 1
then show ?case by simp
next
case (2 c i P2)
then show ?case
by (metis mkPinj_cn mul.simps(2) norm_Pinj norm_Pinj_0_False)
next
case (3 i P2 c)
then show ?case
by (metis mkPinj_cn mul.simps(3) norm_Pinj norm_Pinj_0_False)
next
case (4 c P2 i Q2)
then show ?case
by (metis isnorm.simps(6) mkPX_cn mul.simps(4) norm_PX1 norm_PX2)
next
case (5 P2 i Q2 c)
then show ?case
by (metis isnorm.simps(6) mkPX_cn mul.simps(5) norm_PX1 norm_PX2)
next
case (6 x P2 y Q2)
consider "x < y" | "x = y" | "x > y" by arith
then show ?case
proof cases
case xy: 1
then obtain d where y: "y = d + x"
by atomize_elim arith
from 6 have *: "x > 0"
by (cases x) (auto simp add: norm_Pinj_0_False)
from 6 have **: "isnorm P2" "isnorm Q2"
by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
from 6 xy y have "isnorm (Pinj d Q2)"
apply simp
by (smt (verit, ccfv_SIG) "**"(2) Suc_pred isnorm.elims(1) isnorm.simps(2) isnorm.simps(3) isnorm.simps(5))
with 6 * ** y show ?thesis
next
case xy: 2
from 6 have *: "isnorm P2" "isnorm Q2"
by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
from 6 have **: "y > 0"
by (cases y) (auto simp add: norm_Pinj_0_False)
with 6 xy * ** show ?thesis
next
case xy: 3
then obtain d where x: "x = d + y"
by atomize_elim arith
from 6 have *: "y > 0"
by (cases y) (auto simp add: norm_Pinj_0_False)
from 6 have **: "isnorm P2" "isnorm Q2"
by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
with 6 xy x have "isnorm (Pinj d P2)"
apply simp
by (smt (verit, ccfv_SIG) Suc_pred isnorm.elims(1) isnorm.simps(2) isnorm.simps(3) isnorm.simps(5))
with 6 xy * ** x show ?thesis
qed
next
case (7 x P2 Q2 y R)
then have Y0: "y > 0" by (cases y) auto
consider "x = 0" | "x = 1" | d where "x = Suc (Suc d)"
by atomize_elim arith
then show ?case
proof cases
case 1
with 7 show ?thesis
next
case x: 2
from 7 have "isnorm R" "isnorm P2"
by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
with 7 x have "isnorm (R ⟨*⟩ P2)" "isnorm Q2"
by (auto simp add: norm_PX1[of Q2 y R])
with 7 x Y0 show ?thesis
next
case x: 3
from 7 have *: "isnorm R" "isnorm Q2"
by (auto simp add: norm_PX2[of Q2 y R] norm_PX1[of Q2 y R])
from 7 x have "isnorm (Pinj (x - 1) P2)"
by (cases P2) auto
with 7 x * have "isnorm (R ⟨*⟩ Pinj (x - 1) P2)" "isnorm (Pinj x P2 ⟨*⟩ Q2)"
by auto
with Y0 x show ?thesis
qed
next
case (8 Q2 y R x P2)
then have Y0: "y > 0"
by (cases y) auto
consider "x = 0" | "x = 1" | d where "x = Suc (Suc d)"
by atomize_elim arith
then show ?case
proof cases
case 1
with 8 show ?thesis
next
case x: 2
from 8 have "isnorm R" "isnorm P2"
by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
with 8 x have "isnorm (R ⟨*⟩ P2)" "isnorm Q2"
by (auto simp add: norm_PX1[of Q2 y R])
with 8 x Y0 show ?thesis
next
case x: 3
from 8 have *: "isnorm R" "isnorm Q2"
by (auto simp add: norm_PX2[of Q2 y R] norm_PX1[of Q2 y R])
from 8 x have "isnorm (Pinj (x - 1) P2)"
by (cases P2) auto
with 8 x * have "isnorm (R ⟨*⟩ Pinj (x - 1) P2)" "isnorm (Pinj x P2 ⟨*⟩ Q2)"
by auto
with Y0 x show ?thesis
qed
next
case (9 P1 x P2 Q1 y Q2)
from 9 have X0: "x > 0" by (cases x) auto
from 9 have Y0: "y > 0" by (cases y) auto
from 9 have *: "isnorm P1" "isnorm P2"
by (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2])
from 9 have "isnorm Q1" "isnorm Q2"
by (auto simp add: norm_PX1[of Q1 y Q2] norm_PX2[of Q1 y Q2])
with 9 * have "isnorm (P1 ⟨*⟩ Q1)" "isnorm (P2 ⟨*⟩ Q2)"
"isnorm (P1 ⟨*⟩ mkPinj 1 Q2)" "isnorm (Q1 ⟨*⟩ mkPinj 1 P2)"
with 9 X0 Y0 have
"isnorm (mkPX (P1 ⟨*⟩ Q1) (x + y) (P2 ⟨*⟩ Q2))"
"isnorm (mkPX (P1 ⟨*⟩ mkPinj (Suc 0) Q2) x (Pc 0))"
"isnorm (mkPX (Q1 ⟨*⟩ mkPinj (Suc 0) P2) y (Pc 0))"
then show ?case
qed

text ‹neg preserves the normal property›
lemma neg_cn: "isnorm P ⟹ isnorm (neg P)"
proof (induct P)
case Pc
then show ?case by simp
next
case (Pinj i P2)
then have "isnorm P2"
by (simp add: norm_Pinj[of i P2])
with Pinj show ?case
by (cases P2) (auto, cases i, auto)
next
case (PX P1 x P2) note PX1 = this
from PX have "isnorm P2" "isnorm P1"
by (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2])
with PX show ?case
proof (cases P1)
case (PX p1 y p2)
with PX1 show ?thesis
by (cases x) (auto, cases p2, auto)
next
case Pinj
with PX1 show ?thesis
by (cases x) auto
qed (cases x, auto)
qed

text ‹sub preserves the normal property›
lemma sub_cn: "isnorm p ⟹ isnorm q ⟹ isnorm (p ⟨-⟩ q)"

text ‹sqr conserves normalizizedness›
lemma sqr_cn: "isnorm P ⟹ isnorm (sqr P)"
proof (induct P)
case Pc
then show ?case by simp
next
case (Pinj i Q)
then show ?case
by (metis Commutative_Ring.sqr.simps(2) mkPinj_cn norm_Pinj norm_Pinj_0_False)
next
case (PX P1 x P2)
then have "x + x ≠ 0" "isnorm P2" "isnorm P1"
by (cases x) (use PX in ‹auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2]›)
with PX have "isnorm (mkPX (Pc (1 + 1) ⟨*⟩ P1 ⟨*⟩ mkPinj (Suc 0) P2) x (Pc 0))"
and "isnorm (mkPX (sqr P1) (x + x) (sqr P2))"
then show ?case
qed

text ‹‹pow› preserves the normal property›
lemma pow_cn: "isnorm P ⟹ isnorm (pow n P)"
proof (induct n arbitrary: P rule: less_induct)
case (less k)
show ?case
proof (cases "k = 0")
case True
then show ?thesis by simp
next
case False
then have K2: "k div 2 < k"
by (cases k) auto
from less have "isnorm (sqr P)"
with less False K2 show ?thesis
by (cases "even k") (auto simp add: mul_cn elim: evenE oddE)
qed
qed

end
```