Theory HOL-Decision_Procs.Commutative_Ring

(*  Title:      HOL/Decision_Procs/Commutative_Ring.thy
    Author:     Bernhard Haeupler, Stefan Berghofer, and Amine Chaieb

Proving equalities in commutative rings done "right" in Isabelle/HOL.
*)

section ‹Proving equalities in commutative rings›

theory Commutative_Ring
  imports
    Conversions
    Algebra_Aux
    "HOL-Library.Code_Target_Numeral"
begin

text ‹Syntax of multivariate polynomials (pol) and polynomial expressions.›

datatype pol =
    Pc int
  | Pinj nat pol
  | PX pol nat pol

datatype polex =
    Var nat
  | Const int
  | Add polex polex
  | Sub polex polex
  | Mul polex polex
  | Pow polex nat
  | Neg polex

text ‹Interpretation functions for the shadow syntax.›

context cring
begin

definition in_carrier :: "'a list ⇒ bool"
  where "in_carrier xs ⟷ (∀x∈set xs. x ∈ carrier R)"

lemma in_carrier_Nil: "in_carrier []"
  by (simp add: in_carrier_def)

lemma in_carrier_Cons: "x ∈ carrier R ⟹ in_carrier xs ⟹ in_carrier (x # xs)"
  by (simp add: in_carrier_def)

lemma drop_in_carrier [simp]: "in_carrier xs ⟹ in_carrier (drop n xs)"
  using set_drop_subset [of n xs] by (auto simp add: in_carrier_def)

primrec head :: "'a list ⇒ 'a"
  where
    "head [] = 𝟬"
  | "head (x # xs) = x"

lemma head_closed [simp]: "in_carrier xs ⟹ head xs ∈ carrier R"
  by (cases xs) (simp_all add: in_carrier_def)

primrec Ipol :: "'a list ⇒ pol ⇒ 'a"
  where
    "Ipol l (Pc c) = «c»"
  | "Ipol l (Pinj i P) = Ipol (drop i l) P"
  | "Ipol l (PX P x Q) = Ipol l P ⊗ head l [^] x ⊕ Ipol (drop 1 l) Q"

lemma Ipol_Pc:
  "Ipol l (Pc 0) = 𝟬"
  "Ipol l (Pc 1) = 𝟭"
  "Ipol l (Pc (numeral n)) = «numeral n»"
  "Ipol l (Pc (- numeral n)) = ⊖ «numeral n»"
  by simp_all

lemma Ipol_closed [simp]: "in_carrier l ⟹ Ipol l p ∈ carrier R"
  by (induct p arbitrary: l) simp_all

primrec Ipolex :: "'a list ⇒ polex ⇒ 'a"
  where
    "Ipolex l (Var n) = head (drop n l)"
  | "Ipolex l (Const i) = «i»"
  | "Ipolex l (Add P Q) = Ipolex l P ⊕ Ipolex l Q"
  | "Ipolex l (Sub P Q) = Ipolex l P ⊖ Ipolex l Q"
  | "Ipolex l (Mul P Q) = Ipolex l P ⊗ Ipolex l Q"
  | "Ipolex l (Pow p n) = Ipolex l p [^] n"
  | "Ipolex l (Neg P) = ⊖ Ipolex l P"

lemma Ipolex_Const:
  "Ipolex l (Const 0) = 𝟬"
  "Ipolex l (Const 1) = 𝟭"
  "Ipolex l (Const (numeral n)) = «numeral n»"
  by simp_all

end

text ‹Create polynomial normalized polynomials given normalized inputs.›

definition mkPinj :: "nat ⇒ pol ⇒ pol"
  where "mkPinj x P =
    (case P of
      Pc c ⇒ Pc c
    | Pinj y P ⇒ Pinj (x + y) P
    | PX p1 y p2 ⇒ Pinj x P)"

definition mkPX :: "pol ⇒ nat ⇒ pol ⇒ pol"
  where "mkPX P i Q =
    (case P of
      Pc c ⇒ if c = 0 then mkPinj 1 Q else PX P i Q
    | Pinj j R ⇒ PX P i Q
    | PX P2 i2 Q2 ⇒ if Q2 = Pc 0 then PX P2 (i + i2) Q else PX P i Q)"

text ‹Defining the basic ring operations on normalized polynomials›

function add :: "pol ⇒ pol ⇒ pol"  (infixl ‹⟨+⟩› 65)
  where
    "Pc a ⟨+⟩ Pc b = Pc (a + b)"
  | "Pc c ⟨+⟩ Pinj i P = Pinj i (P ⟨+⟩ Pc c)"
  | "Pinj i P ⟨+⟩ Pc c = Pinj i (P ⟨+⟩ Pc c)"
  | "Pc c ⟨+⟩ PX P i Q = PX P i (Q ⟨+⟩ Pc c)"
  | "PX P i Q ⟨+⟩ Pc c = PX P i (Q ⟨+⟩ Pc c)"
  | "Pinj x P ⟨+⟩ Pinj y Q =
      (if x = y then mkPinj x (P ⟨+⟩ Q)
       else (if x > y then mkPinj y (Pinj (x - y) P ⟨+⟩ Q)
         else mkPinj x (Pinj (y - x) Q ⟨+⟩ P)))"
  | "Pinj x P ⟨+⟩ PX Q y R =
      (if x = 0 then P ⟨+⟩ PX Q y R
       else (if x = 1 then PX Q y (R ⟨+⟩ P)
         else PX Q y (R ⟨+⟩ Pinj (x - 1) P)))"
  | "PX P x R ⟨+⟩ Pinj y Q =
      (if y = 0 then PX P x R ⟨+⟩ Q
       else (if y = 1 then PX P x (R ⟨+⟩ Q)
         else PX P x (R ⟨+⟩ Pinj (y - 1) Q)))"
  | "PX P1 x P2 ⟨+⟩ PX Q1 y Q2 =
      (if x = y then mkPX (P1 ⟨+⟩ Q1) x (P2 ⟨+⟩ Q2)
       else (if x > y then mkPX (PX P1 (x - y) (Pc 0) ⟨+⟩ Q1) y (P2 ⟨+⟩ Q2)
         else mkPX (PX Q1 (y - x) (Pc 0) ⟨+⟩ P1) x (P2 ⟨+⟩ Q2)))"
  by pat_completeness auto
termination by (relation "measure (λ(x, y). size x + size y)") auto

function mul :: "pol ⇒ pol ⇒ pol"  (infixl ‹⟨*⟩› 70)
  where
    "Pc a ⟨*⟩ Pc b = Pc (a * b)"
  | "Pc c ⟨*⟩ Pinj i P =
      (if c = 0 then Pc 0 else mkPinj i (P ⟨*⟩ Pc c))"
  | "Pinj i P ⟨*⟩ Pc c =
      (if c = 0 then Pc 0 else mkPinj i (P ⟨*⟩ Pc c))"
  | "Pc c ⟨*⟩ PX P i Q =
      (if c = 0 then Pc 0 else mkPX (P ⟨*⟩ Pc c) i (Q ⟨*⟩ Pc c))"
  | "PX P i Q ⟨*⟩ Pc c =
      (if c = 0 then Pc 0 else mkPX (P ⟨*⟩ Pc c) i (Q ⟨*⟩ Pc c))"
  | "Pinj x P ⟨*⟩ Pinj y Q =
      (if x = y then mkPinj x (P ⟨*⟩ Q)
       else
         (if x > y then mkPinj y (Pinj (x - y) P ⟨*⟩ Q)
          else mkPinj x (Pinj (y - x) Q ⟨*⟩ P)))"
  | "Pinj x P ⟨*⟩ PX Q y R =
      (if x = 0 then P ⟨*⟩ PX Q y R
       else
         (if x = 1 then mkPX (Pinj x P ⟨*⟩ Q) y (R ⟨*⟩ P)
          else mkPX (Pinj x P ⟨*⟩ Q) y (R ⟨*⟩ Pinj (x - 1) P)))"
  | "PX P x R ⟨*⟩ Pinj y Q =
      (if y = 0 then PX P x R ⟨*⟩ Q
       else
         (if y = 1 then mkPX (Pinj y Q ⟨*⟩ P) x (R ⟨*⟩ Q)
          else mkPX (Pinj y Q ⟨*⟩ P) x (R ⟨*⟩ Pinj (y - 1) Q)))"
  | "PX P1 x P2 ⟨*⟩ PX Q1 y Q2 =
      mkPX (P1 ⟨*⟩ Q1) (x + y) (P2 ⟨*⟩ Q2) ⟨+⟩
        (mkPX (P1 ⟨*⟩ mkPinj 1 Q2) x (Pc 0) ⟨+⟩
          (mkPX (Q1 ⟨*⟩ mkPinj 1 P2) y (Pc 0)))"
  by pat_completeness auto
termination by (relation "measure (λ(x, y). size x + size y)")
  (auto simp add: mkPinj_def split: pol.split)

text ‹Negation›
primrec neg :: "pol ⇒ pol"
  where
    "neg (Pc c) = Pc (- c)"
  | "neg (Pinj i P) = Pinj i (neg P)"
  | "neg (PX P x Q) = PX (neg P) x (neg Q)"

text ‹Subtraction›
definition sub :: "pol ⇒ pol ⇒ pol"  (infixl ‹⟨-⟩› 65)
  where "sub P Q = P ⟨+⟩ neg Q"

text ‹Square for Fast Exponentiation›
primrec sqr :: "pol ⇒ pol"
  where
    "sqr (Pc c) = Pc (c * c)"
  | "sqr (Pinj i P) = mkPinj i (sqr P)"
  | "sqr (PX A x B) = mkPX (sqr A) (x + x) (sqr B) ⟨+⟩ mkPX (Pc 2 ⟨*⟩ A ⟨*⟩ mkPinj 1 B) x (Pc 0)"

text ‹Fast Exponentiation›

fun pow :: "nat ⇒ pol ⇒ pol"
  where pow_if [simp del]: "pow n P =
   (if n = 0 then Pc 1
    else if even n then pow (n div 2) (sqr P)
    else P ⟨*⟩ pow (n div 2) (sqr P))"

lemma pow_simps [simp]:
  "pow 0 P = Pc 1"
  "pow (2 * n) P = pow n (sqr P)"
  "pow (Suc (2 * n)) P = P ⟨*⟩ pow n (sqr P)"
  by (simp_all add: pow_if)

lemma even_pow: "even n ⟹ pow n P = pow (n div 2) (sqr P)"
  by (erule evenE) simp

lemma odd_pow: "odd n ⟹ pow n P = P ⟨*⟩ pow (n div 2) (sqr P)"
  by (erule oddE) simp


text ‹Normalization of polynomial expressions›

primrec norm :: "polex ⇒ pol"
  where
    "norm (Var n) =
       (if n = 0 then PX (Pc 1) 1 (Pc 0)
        else Pinj n (PX (Pc 1) 1 (Pc 0)))"
  | "norm (Const i) = Pc i"
  | "norm (Add P Q) = norm P ⟨+⟩ norm Q"
  | "norm (Sub P Q) = norm P ⟨-⟩ norm Q"
  | "norm (Mul P Q) = norm P ⟨*⟩ norm Q"
  | "norm (Pow P n) = pow n (norm P)"
  | "norm (Neg P) = neg (norm P)"

context cring
begin

text ‹mkPinj preserve semantics›
lemma mkPinj_ci: "Ipol l (mkPinj a B) = Ipol l (Pinj a B)"
  by (induct B) (auto simp add: mkPinj_def algebra_simps)

text ‹mkPX preserves semantics›
lemma mkPX_ci: "in_carrier l ⟹ Ipol l (mkPX A b C) = Ipol l (PX A b C)"
  by (cases A) (auto simp add: mkPX_def mkPinj_ci nat_pow_mult [symmetric] m_ac)

text ‹Correctness theorems for the implemented operations›

text ‹Negation›
lemma neg_ci: "in_carrier l ⟹ Ipol l (neg P) = ⊖ (Ipol l P)"
  by (induct P arbitrary: l) (auto simp add: minus_add l_minus)

text ‹Addition›
lemma add_ci: "in_carrier l ⟹ Ipol l (P ⟨+⟩ Q) = Ipol l P ⊕ Ipol l Q"
proof (induct P Q arbitrary: l rule: add.induct)
  case (6 x P y Q)
  consider "x < y" | "x = y" | "x > y" by arith
  then show ?case
  proof cases
    case 1
    with 6 show ?thesis by (simp add: mkPinj_ci a_ac)
  next
    case 2
    with 6 show ?thesis by (simp add: mkPinj_ci)
  next
    case 3
    with 6 show ?thesis by (simp add: mkPinj_ci)
  qed
next
  case (7 x P Q y R)
  consider "x = 0" | "x = 1" | "x > 1" by arith
  then show ?case
  proof cases
    case 1
    with 7 show ?thesis by simp
  next
    case 2
    with 7 show ?thesis by (simp add: a_ac)
  next
    case 3
    with 7 show ?thesis by (cases x) (simp_all add: a_ac)
  qed
next
  case (8 P x R y Q)
  then show ?case by (simp add: a_ac)
next
  case (9 P1 x P2 Q1 y Q2)
  consider "x = y" | d where "d + x = y" | d where "d + y = x"
    by atomize_elim arith
  then show ?case
  proof cases
    case 1
    with 9 show ?thesis by (simp add: mkPX_ci r_distr a_ac m_ac)
  next
    case 2
    with 9 show ?thesis by (auto simp add: mkPX_ci nat_pow_mult [symmetric] r_distr a_ac m_ac)
  next
    case 3
    with 9 show ?thesis by (auto simp add: nat_pow_mult [symmetric] mkPX_ci r_distr a_ac m_ac)
  qed
qed (auto simp add: a_ac m_ac)

text ‹Multiplication›
lemma mul_ci: "in_carrier l ⟹ Ipol l (P ⟨*⟩ Q) = Ipol l P ⊗ Ipol l Q"
  by (induct P Q arbitrary: l rule: mul.induct)
    (simp_all add: mkPX_ci mkPinj_ci a_ac m_ac r_distr add_ci nat_pow_mult [symmetric])

text ‹Subtraction›
lemma sub_ci: "in_carrier l ⟹ Ipol l (P ⟨-⟩ Q) = Ipol l P ⊖ Ipol l Q"
  by (simp add: add_ci neg_ci sub_def minus_eq)

text ‹Square›
lemma sqr_ci: "in_carrier ls ⟹ Ipol ls (sqr P) = Ipol ls P ⊗ Ipol ls P"
  by (induct P arbitrary: ls)
    (simp_all add: add_ci mkPinj_ci mkPX_ci mul_ci l_distr r_distr
       a_ac m_ac nat_pow_mult [symmetric] of_int_2)

text ‹Power›
lemma pow_ci: "in_carrier ls ⟹ Ipol ls (pow n P) = Ipol ls P [^] n"
proof (induct n arbitrary: P rule: less_induct)
  case (less k)
  consider "k = 0" | "k > 0" by arith
  then show ?case
  proof cases
    case 1
    then show ?thesis by simp
  next
    case 2
    then have "k div 2 < k" by arith
    with less have *: "Ipol ls (pow (k div 2) (sqr P)) = Ipol ls (sqr P) [^] (k div 2)"
      by simp
    show ?thesis
    proof (cases "even k")
      case True
      with * ‹in_carrier ls› show ?thesis
        by (simp add: even_pow sqr_ci nat_pow_distrib nat_pow_mult
          mult_2 [symmetric] even_two_times_div_two)
    next
      case False
      with * ‹in_carrier ls› show ?thesis
        by (simp add: odd_pow mul_ci sqr_ci nat_pow_distrib nat_pow_mult
          mult_2 [symmetric] trans [OF nat_pow_Suc m_comm, symmetric])
    qed
  qed
qed

text ‹Normalization preserves semantics›
lemma norm_ci: "in_carrier l ⟹ Ipolex l Pe = Ipol l (norm Pe)"
  by (induct Pe) (simp_all add: add_ci sub_ci mul_ci neg_ci pow_ci)

text ‹Reflection lemma: Key to the (incomplete) decision procedure›
lemma norm_eq:
  assumes "in_carrier l"
  and "norm P1 = norm P2"
  shows "Ipolex l P1 = Ipolex l P2"
proof -
  from assms have "Ipol l (norm P1) = Ipol l (norm P2)" by simp
  with assms show ?thesis by (simp only: norm_ci)
qed

end


text ‹Monomials›

datatype mon =
    Mc int
  | Minj nat mon
  | MX nat mon

primrec (in cring) Imon :: "'a list ⇒ mon ⇒ 'a"
  where
    "Imon l (Mc c) = «c»"
  | "Imon l (Minj i M) = Imon (drop i l) M"
  | "Imon l (MX x M) = Imon (drop 1 l) M ⊗ head l [^] x"

lemma (in cring) Imon_closed [simp]: "in_carrier l ⟹ Imon l m ∈ carrier R"
  by (induct m arbitrary: l) simp_all

definition mkMinj :: "nat ⇒ mon ⇒ mon"
  where "mkMinj i M =
    (case M of
      Mc c ⇒ Mc c
    | Minj j M ⇒ Minj (i + j) M
    | _ ⇒ Minj i M)"

definition Minj_pred :: "nat ⇒ mon ⇒ mon"
  where "Minj_pred i M = (if i = 1 then M else mkMinj (i - 1) M)"

primrec mkMX :: "nat ⇒ mon ⇒ mon"
  where
    "mkMX i (Mc c) = MX i (Mc c)"
  | "mkMX i (Minj j M) = (if j = 0 then mkMX i M else MX i (Minj_pred j M))"
  | "mkMX i (MX j M) = MX (i + j) M"

lemma (in cring) mkMinj_correct: "Imon l (mkMinj i M) = Imon l (Minj i M)"
  by (simp add: mkMinj_def add.commute split: mon.split)

lemma (in cring) Minj_pred_correct: "0 < i ⟹ Imon (drop 1 l) (Minj_pred i M) = Imon l (Minj i M)"
  by (simp add: Minj_pred_def mkMinj_correct)

lemma (in cring) mkMX_correct: "in_carrier l ⟹ Imon l (mkMX i M) = Imon l M ⊗ head l [^] i"
  by (induct M)
    (simp_all add: Minj_pred_correct [simplified] nat_pow_mult [symmetric] m_ac split: mon.split)

fun cfactor :: "pol ⇒ int ⇒ pol × pol"
  where
    "cfactor (Pc c') c = (Pc (c' mod c), Pc (c' div c))"
  | "cfactor (Pinj i P) c =
       (let (R, S) = cfactor P c
        in (mkPinj i R, mkPinj i S))"
  | "cfactor (PX P i Q) c =
       (let
          (R1, S1) = cfactor P c;
          (R2, S2) = cfactor Q c
        in (mkPX R1 i R2, mkPX S1 i S2))"

lemma (in cring) cfactor_correct:
  "in_carrier l ⟹ Ipol l P = Ipol l (fst (cfactor P c)) ⊕ «c» ⊗ Ipol l (snd (cfactor P c))"
proof (induct P c arbitrary: l rule: cfactor.induct)
  case (1 c' c)
  show ?case
    by (simp add: of_int_mult [symmetric] of_int_add [symmetric] del: of_int_mult)
next
  case (2 i P c)
  then show ?case
    by (simp add: mkPinj_ci split_beta)
next
  case (3 P i Q c)
  from 3(1) 3(2) [OF refl prod.collapse] 3(3)
  show ?case
    by (simp add: mkPX_ci r_distr a_ac m_ac split_beta)
qed

fun mfactor :: "pol ⇒ mon ⇒ pol × pol"
  where
    "mfactor P (Mc c) = (if c = 1 then (Pc 0, P) else cfactor P c)"
  | "mfactor (Pc d) M = (Pc d, Pc 0)"
  | "mfactor (Pinj i P) (Minj j M) =
       (if i = j then
          let (R, S) = mfactor P M
          in (mkPinj i R, mkPinj i S)
        else if i < j then
          let (R, S) = mfactor P (Minj (j - i) M)
          in (mkPinj i R, mkPinj i S)
        else (Pinj i P, Pc 0))"
  | "mfactor (Pinj i P) (MX j M) = (Pinj i P, Pc 0)"
  | "mfactor (PX P i Q) (Minj j M) =
       (if j = 0 then mfactor (PX P i Q) M
        else
          let
            (R1, S1) = mfactor P (Minj j M);
            (R2, S2) = mfactor Q (Minj_pred j M)
          in (mkPX R1 i R2, mkPX S1 i S2))"
  | "mfactor (PX P i Q) (MX j M) =
       (if i = j then
          let (R, S) = mfactor P (mkMinj 1 M)
          in (mkPX R i Q, S)
        else if i < j then
          let (R, S) = mfactor P (MX (j - i) M)
          in (mkPX R i Q, S)
        else
          let (R, S) = mfactor P (mkMinj 1 M)
          in (mkPX R i Q, mkPX S (i - j) (Pc 0)))"

lemmas mfactor_induct = mfactor.induct
  [case_names Mc Pc_Minj Pc_MX Pinj_Minj Pinj_MX PX_Minj PX_MX]

lemma (in cring) mfactor_correct:
  "in_carrier l ⟹
   Ipol l P =
   Ipol l (fst (mfactor P M)) ⊕
   Imon l M ⊗ Ipol l (snd (mfactor P M))"
proof (induct P M arbitrary: l rule: mfactor_induct)
  case (Mc P c)
  then show ?case
    by (simp add: cfactor_correct)
next
  case (Pc_Minj d i M)
  then show ?case
    by simp
next
  case (Pc_MX d i M)
  then show ?case
    by simp
next
  case (Pinj_Minj i P j M)
  then show ?case
    by (simp add: mkPinj_ci split_beta)
next
  case (Pinj_MX i P j M)
  then show ?case
    by simp
next
  case (PX_Minj P i Q j M)
  from PX_Minj(1,2) PX_Minj(3) [OF _ refl prod.collapse] PX_Minj(4)
  show ?case
    by (simp add: mkPX_ci Minj_pred_correct [simplified] r_distr a_ac m_ac split_beta)
next
  case (PX_MX P i Q j M)
  from ‹in_carrier l›
  have eq1: "(Imon (drop (Suc 0) l) M ⊗ head l [^] (j - i)) ⊗
    Ipol l (snd (mfactor P (MX (j - i) M))) ⊗ head l [^] i =
    Imon (drop (Suc 0) l) M ⊗
    Ipol l (snd (mfactor P (MX (j - i) M))) ⊗
    (head l [^] (j - i) ⊗ head l [^] i)"
    by (simp add: m_ac)
  from ‹in_carrier l›
  have eq2: "(Imon (drop (Suc 0) l) M ⊗ head l [^] j) ⊗
    (Ipol l (snd (mfactor P (mkMinj (Suc 0) M))) ⊗ head l [^] (i - j)) =
    Imon (drop (Suc 0) l) M ⊗
    Ipol l (snd (mfactor P (mkMinj (Suc 0) M))) ⊗
    (head l [^] (i - j) ⊗ head l [^] j)"
    by (simp add: m_ac)
  from PX_MX ‹in_carrier l› show ?case
    by (simp add: mkPX_ci mkMinj_correct l_distr eq1 eq2 split_beta nat_pow_mult)
      (simp add: a_ac m_ac)
qed

primrec mon_of_pol :: "pol ⇒ mon option"
  where
    "mon_of_pol (Pc c) = Some (Mc c)"
  | "mon_of_pol (Pinj i P) = (case mon_of_pol P of
         None ⇒ None
       | Some M ⇒ Some (mkMinj i M))"
  | "mon_of_pol (PX P i Q) =
       (if Q = Pc 0 then (case mon_of_pol P of
            None ⇒ None
          | Some M ⇒ Some (mkMX i M))
        else None)"

lemma (in cring) mon_of_pol_correct:
  assumes "in_carrier l"
    and "mon_of_pol P = Some M"
  shows "Ipol l P = Imon l M"
  using assms
proof (induct P arbitrary: M l)
  case (PX P1 i P2)
  from PX(1,3,4)
  show ?case
    by (auto simp add: mkMinj_correct mkMX_correct split: if_split_asm option.split_asm)
qed (auto simp add: mkMinj_correct split: option.split_asm)

fun (in cring) Ipolex_polex_list :: "'a list ⇒ (polex × polex) list ⇒ bool"
  where
    "Ipolex_polex_list l [] = True"
  | "Ipolex_polex_list l ((P, Q) # pps) = ((Ipolex l P = Ipolex l Q) ∧ Ipolex_polex_list l pps)"

fun (in cring) Imon_pol_list :: "'a list ⇒ (mon × pol) list ⇒ bool"
  where
    "Imon_pol_list l [] = True"
  | "Imon_pol_list l ((M, P) # mps) = ((Imon l M = Ipol l P) ∧ Imon_pol_list l mps)"

fun mk_monpol_list :: "(polex × polex) list ⇒ (mon × pol) list"
  where
    "mk_monpol_list [] = []"
  | "mk_monpol_list ((P, Q) # pps) =
       (case mon_of_pol (norm P) of
          None ⇒ mk_monpol_list pps
        | Some M ⇒ (M, norm Q) # mk_monpol_list pps)"

lemma (in cring) mk_monpol_list_correct:
  "in_carrier l ⟹ Ipolex_polex_list l pps ⟹ Imon_pol_list l (mk_monpol_list pps)"
  by (induct pps rule: mk_monpol_list.induct)
    (auto split: option.split simp add: norm_ci [symmetric] mon_of_pol_correct [symmetric])

definition ponesubst :: "pol ⇒ mon ⇒ pol ⇒ pol option"
  where "ponesubst P1 M P2 =
   (let (Q, R) = mfactor P1 M in
    (case R of
      Pc c ⇒ if c = 0 then None else Some (add Q (mul P2 R))
    | _ ⇒ Some (add Q (mul P2 R))))"

fun pnsubst1 :: "pol ⇒ mon ⇒ pol ⇒ nat ⇒ pol"
  where "pnsubst1 P1 M P2 n =
    (case ponesubst P1 M P2 of
      None ⇒ P1
    | Some P3 ⇒ if n = 0 then P3 else pnsubst1 P3 M P2 (n - 1))"

lemma pnsubst1_0 [simp]: "pnsubst1 P1 M P2 0 = (case ponesubst P1 M P2 of
  None ⇒ P1 | Some P3 ⇒ P3)"
  by (simp split: option.split)

lemma pnsubst1_Suc [simp]:
  "pnsubst1 P1 M P2 (Suc n) =
    (case ponesubst P1 M P2 of
      None ⇒ P1
    | Some P3 ⇒ pnsubst1 P3 M P2 n)"
  by (simp split: option.split)

declare pnsubst1.simps [simp del]

definition pnsubst :: "pol ⇒ mon ⇒ pol ⇒ nat ⇒ pol option"
  where "pnsubst P1 M P2 n =
    (case ponesubst P1 M P2 of
      None ⇒ None
    | Some P3 ⇒ Some (pnsubst1 P3 M P2 n))"

fun psubstl1 :: "pol ⇒ (mon × pol) list ⇒ nat ⇒ pol"
  where
    "psubstl1 P1 [] n = P1"
  | "psubstl1 P1 ((M, P2) # mps) n = psubstl1 (pnsubst1 P1 M P2 n) mps n"

fun psubstl :: "pol ⇒ (mon × pol) list ⇒ nat ⇒ pol option"
  where
    "psubstl P1 [] n = None"
  | "psubstl P1 ((M, P2) # mps) n =
      (case pnsubst P1 M P2 n of
        None ⇒ psubstl P1 mps n
      | Some P3 ⇒ Some (psubstl1 P3 mps n))"

fun pnsubstl :: "pol ⇒ (mon × pol) list ⇒ nat ⇒ nat ⇒ pol"
  where "pnsubstl P1 mps m n =
    (case psubstl P1 mps n of
      None ⇒ P1
    | Some P3 ⇒ if m = 0 then P3 else pnsubstl P3 mps (m - 1) n)"

lemma pnsubstl_0 [simp]:
  "pnsubstl P1 mps 0 n = (case psubstl P1 mps n of None ⇒ P1 | Some P3 ⇒ P3)"
  by (simp split: option.split)

lemma pnsubstl_Suc [simp]:
  "pnsubstl P1 mps (Suc m) n = (case psubstl P1 mps n of None ⇒ P1 | Some P3 ⇒ pnsubstl P3 mps m n)"
  by (simp split: option.split)

declare pnsubstl.simps [simp del]

lemma (in cring) ponesubst_correct:
  "in_carrier l ⟹ ponesubst P1 M P2 = Some P3 ⟹ Imon l M = Ipol l P2 ⟹ Ipol l P1 = Ipol l P3"
  by (auto simp add: ponesubst_def split_beta mfactor_correct [of l P1 M]
    add_ci mul_ci split: pol.split_asm if_split_asm)

lemma (in cring) pnsubst1_correct:
  "in_carrier l ⟹ Imon l M = Ipol l P2 ⟹ Ipol l (pnsubst1 P1 M P2 n) = Ipol l P1"
  by (induct n arbitrary: P1)
    (simp_all add: ponesubst_correct split: option.split)

lemma (in cring) pnsubst_correct:
  "in_carrier l ⟹ pnsubst P1 M P2 n = Some P3 ⟹ Imon l M = Ipol l P2 ⟹ Ipol l P1 = Ipol l P3"
  by (auto simp add: pnsubst_def
    pnsubst1_correct ponesubst_correct split: option.split_asm)

lemma (in cring) psubstl1_correct:
  "in_carrier l ⟹ Imon_pol_list l mps ⟹ Ipol l (psubstl1 P1 mps n) = Ipol l P1"
  by (induct P1 mps n rule: psubstl1.induct) (simp_all add: pnsubst1_correct)

lemma (in cring) psubstl_correct:
  "in_carrier l ⟹ psubstl P1 mps n = Some P2 ⟹ Imon_pol_list l mps ⟹ Ipol l P1 = Ipol l P2"
  by (induct P1 mps n rule: psubstl.induct)
    (auto simp add: psubstl1_correct pnsubst_correct split: option.split_asm)

lemma (in cring) pnsubstl_correct:
  "in_carrier l ⟹ Imon_pol_list l mps ⟹ Ipol l (pnsubstl P1 mps m n) = Ipol l P1"
  by (induct m arbitrary: P1)
    (simp_all add: psubstl_correct split: option.split)

lemma (in cring) norm_subst_correct:
  "in_carrier l ⟹ Ipolex_polex_list l pps ⟹
   Ipolex l P = Ipol l (pnsubstl (norm P) (mk_monpol_list pps) m n)"
  by (simp add: pnsubstl_correct mk_monpol_list_correct norm_ci)

lemma in_carrier_trivial: "cring_class.in_carrier l"
  by (induct l) (simp_all add: cring_class.in_carrier_def carrier_class)

ML ‹
val term_of_nat = HOLogic.mk_number \<^Type>‹nat› o @{code integer_of_nat};

val term_of_int = HOLogic.mk_number \<^Type>‹int› o @{code integer_of_int};

fun term_of_pol (@{code Pc} k) = \<^Const>‹Pc› $ term_of_int k
  | term_of_pol (@{code Pinj} (n, p)) = \<^Const>‹Pinj› $ term_of_nat n $ term_of_pol p
  | term_of_pol (@{code PX} (p, n, q)) = \<^Const>‹PX› $ term_of_pol p $ term_of_nat n $ term_of_pol q;

local

fun pol (ctxt, ct, t) =
  \<^instantiate>‹x = ct and y = ‹Thm.cterm_of ctxt t›
    in cterm ‹x ≡ y› for x y :: pol›;

val (_, raw_pol_oracle) = Theory.setup_result (Thm.add_oracle (\<^binding>‹pnsubstl›, pol));

fun pol_oracle ctxt ct t = raw_pol_oracle (ctxt, ct, t);

in

val cv = @{computation_conv pol
  terms: pnsubstl mk_monpol_list norm
    nat_of_integer Code_Target_Nat.natural
      "0::nat" "1::nat" "2::nat" "3::nat"
      "0::int" "1::int" "2::int" "3::int" "-1::int"
  datatypes: polex "(polex * polex) list" int integer num}
  (fn ctxt => fn p => fn ct => pol_oracle ctxt ct (term_of_pol p))

end
›

ML ‹
signature RING_TAC =
sig
  structure Ring_Simps:
  sig
    type T
    val get: Context.generic -> T
    val put: T -> Context.generic -> Context.generic
    val map: (T -> T) -> Context.generic -> Context.generic
  end
  val insert_rules: ((term * 'a) * (term * 'a) -> bool) -> (term * 'a) ->
    (term * 'a) Net.net -> (term * 'a) Net.net
  val eq_ring_simps:
    (term * (thm list * thm list * thm list * thm list * thm * thm)) *
    (term * (thm list * thm list * thm list * thm list * thm * thm)) -> bool
  val ring_tac: bool -> thm list -> Proof.context -> int -> tactic
  val get_matching_rules: Proof.context -> (term * 'a) Net.net -> term -> 'a option
  val norm: thm -> thm
  val mk_in_carrier: Proof.context -> term -> thm list -> (string * typ) list -> thm
  val mk_ring: typ -> term
end

structure Ring_Tac : RING_TAC =
struct

fun eq_ring_simps
  ((t, (ths1, ths2, ths3, ths4, th5, th)),
   (t', (ths1', ths2', ths3', ths4', th5', th'))) =
    t aconv t' andalso
    eq_list Thm.eq_thm (ths1, ths1') andalso
    eq_list Thm.eq_thm (ths2, ths2') andalso
    eq_list Thm.eq_thm (ths3, ths3') andalso
    eq_list Thm.eq_thm (ths4, ths4') andalso
    Thm.eq_thm (th5, th5') andalso
    Thm.eq_thm (th, th');

structure Ring_Simps = Generic_Data
(struct
  type T = (term * (thm list * thm list * thm list * thm list * thm * thm)) Net.net
  val empty = Net.empty
  val merge = Net.merge eq_ring_simps
end);

fun get_matching_rules ctxt net t = get_first
  (fn (p, x) =>
     if Pattern.matches (Proof_Context.theory_of ctxt) (p, t) then SOME x else NONE)
  (Net.match_term net t);

fun insert_rules eq (t, x) = Net.insert_term eq (t, (t, x));

fun norm thm = thm COMP_INCR asm_rl;

fun get_ring_simps ctxt optcT t =
  (case get_matching_rules ctxt (Ring_Simps.get (Context.Proof ctxt)) t of
     SOME (ths1, ths2, ths3, ths4, th5, th) =>
       let val tr =
         Thm.transfer' ctxt #>
         (case optcT of NONE => I | SOME cT => inst [cT] [] #> norm)
       in (map tr ths1, map tr ths2, map tr ths3, map tr ths4, tr th5, tr th) end
   | NONE => error "get_ring_simps: lookup failed");

fun ring_struct \<^Const_>‹Ring.ring.add _ _ for R _ _› = SOME R
  | ring_struct \<^Const_>‹Ring.a_minus _ _ for R _ _› = SOME R
  | ring_struct \<^Const_>‹Group.monoid.mult _ _ for R _ _› = SOME R
  | ring_struct \<^Const_>‹Ring.a_inv _ _ for R _› = SOME R
  | ring_struct \<^Const_>‹Group.pow _ _ _ for R _ _› = SOME R
  | ring_struct \<^Const_>‹Ring.ring.zero _ _ for R› = SOME R
  | ring_struct \<^Const_>‹Group.monoid.one _ _ for R› = SOME R
  | ring_struct \<^Const_>‹Algebra_Aux.of_integer _ _ for R _› = SOME R
  | ring_struct _ = NONE;

fun reif_polex vs \<^Const_>‹Ring.ring.add _ _ for _ a b› =
      \<^Const>‹Add for ‹reif_polex vs a› ‹reif_polex vs b››
  | reif_polex vs \<^Const_>‹Ring.a_minus _ _ for _ a b› =
      \<^Const>‹Sub for ‹reif_polex vs a› ‹reif_polex vs b››
  | reif_polex vs \<^Const_>‹Group.monoid.mult _ _ for _ a b› =
      \<^Const>‹Mul for ‹reif_polex vs a› ‹reif_polex vs b››
  | reif_polex vs \<^Const_>‹Ring.a_inv _ _ for _ a› =
      \<^Const>‹Neg for ‹reif_polex vs a››
  | reif_polex vs \<^Const_>‹Group.pow _ _ _ for _ a n› =
      \<^Const>‹Pow for ‹reif_polex vs a› n›
  | reif_polex vs (Free x) =
      \<^Const>‹Var for ‹HOLogic.mk_number HOLogic.natT (find_index (equal x) vs)››
  | reif_polex _ \<^Const_>‹Ring.ring.zero _ _ for _› = \<^term>‹Const 0›
  | reif_polex _ \<^Const_>‹Group.monoid.one _ _ for _› = \<^term>‹Const 1›
  | reif_polex _ \<^Const_>‹Algebra_Aux.of_integer _ _ for _ n› = \<^Const>‹Const for n›
  | reif_polex _ _ = error "reif_polex: bad expression";

fun reif_polex' vs \<^Const_>‹plus _ for a b› = \<^Const>‹Add for ‹reif_polex' vs a› ‹reif_polex' vs b››
  | reif_polex' vs \<^Const_>‹minus _ for a b› = \<^Const>‹Sub for ‹reif_polex' vs a› ‹reif_polex' vs b››
  | reif_polex' vs \<^Const_>‹times _ for a b› = \<^Const>‹Mul for ‹reif_polex' vs a› ‹reif_polex' vs b››
  | reif_polex' vs \<^Const_>‹uminus _ for a› = \<^Const>‹Neg for ‹reif_polex' vs a››
  | reif_polex' vs \<^Const_>‹power _ for a n› = \<^Const>‹Pow for ‹reif_polex' vs a› n›
  | reif_polex' vs (Free x) = \<^Const>‹Var for ‹HOLogic.mk_number \<^Type>‹nat› (find_index (equal x) vs)››
  | reif_polex' _ \<^Const_>‹numeral _ for b› = \<^Const>‹Const for \<^Const>‹numeral \<^Type>‹int› for b››
  | reif_polex' _ \<^Const_>‹zero_class.zero _› = \<^term>‹Const 0›
  | reif_polex' _ \<^Const_>‹one_class.one _› = \<^term>‹Const 1›
  | reif_polex' _ t = error "reif_polex: bad expression";

fun head_conv (_, _, _, _, head_simp, _) ys =
  (case strip_app ys of
     (\<^const_name>‹Cons›, [y, xs]) => inst [] [y, xs] head_simp);

fun Ipol_conv (rls as
      ([Ipol_simps_1, Ipol_simps_2, Ipol_simps_3,
        Ipol_simps_4, Ipol_simps_5, Ipol_simps_6,
        Ipol_simps_7], _, _, _, _, _)) =
  let
    val a = type_of_eqn Ipol_simps_1;
    val drop_conv_a = drop_conv a;

    fun conv l p = (case strip_app p of
        (\<^const_name>‹Pc›, [c]) => (case strip_numeral c of
            (\<^const_name>‹zero_class.zero›, _) => inst [] [l] Ipol_simps_4
          | (\<^const_name>‹one_class.one›, _) => inst [] [l] Ipol_simps_5
          | (\<^const_name>‹numeral›, [m]) => inst [] [l, m] Ipol_simps_6
          | (\<^const_name>‹uminus›, [m]) => inst [] [l, m] Ipol_simps_7
          | _ => inst [] [l, c] Ipol_simps_1)
      | (\<^const_name>‹Pinj›, [i, P]) =>
          transitive'
            (inst [] [l, i, P] Ipol_simps_2)
            (cong2' conv (args2 drop_conv_a) Thm.reflexive)
      | (\<^const_name>‹PX›, [P, x, Q]) =>
          transitive'
            (inst [] [l, P, x, Q] Ipol_simps_3)
            (cong2
               (cong2
                  (args2 conv) (cong2 (args1 (head_conv rls)) Thm.reflexive))
               (cong2' conv (args2 drop_conv_a) Thm.reflexive)))
  in conv end;

fun Ipolex_conv (rls as
      (_,
       [Ipolex_Var, Ipolex_Const, Ipolex_Add,
        Ipolex_Sub, Ipolex_Mul, Ipolex_Pow,
        Ipolex_Neg, Ipolex_Const_0, Ipolex_Const_1,
        Ipolex_Const_numeral], _, _, _, _)) =
  let
    val a = type_of_eqn Ipolex_Var;
    val drop_conv_a = drop_conv a;

    fun conv l r = (case strip_app r of
        (\<^const_name>‹Var›, [n]) =>
          transitive'
            (inst [] [l, n] Ipolex_Var)
            (cong1' (head_conv rls) (args2 drop_conv_a))
      | (\<^const_name>‹Const›, [i]) => (case strip_app i of
            (\<^const_name>‹zero_class.zero›, _) => inst [] [l] Ipolex_Const_0
          | (\<^const_name>‹one_class.one›, _) => inst [] [l] Ipolex_Const_1
          | (\<^const_name>‹numeral›, [m]) => inst [] [l, m] Ipolex_Const_numeral
          | _ => inst [] [l, i] Ipolex_Const)
      | (\<^const_name>‹Add›, [P, Q]) =>
          transitive'
            (inst [] [l, P, Q] Ipolex_Add)
            (cong2 (args2 conv) (args2 conv))
      | (\<^const_name>‹Sub›, [P, Q]) =>
          transitive'
            (inst [] [l, P, Q] Ipolex_Sub)
            (cong2 (args2 conv) (args2 conv))
      | (\<^const_name>‹Mul›, [P, Q]) =>
          transitive'
            (inst [] [l, P, Q] Ipolex_Mul)
            (cong2 (args2 conv) (args2 conv))
      | (\<^const_name>‹Pow›, [P, n]) =>
          transitive'
            (inst [] [l, P, n] Ipolex_Pow)
            (cong2 (args2 conv) Thm.reflexive)
      | (\<^const_name>‹Neg›, [P]) =>
          transitive'
            (inst [] [l, P] Ipolex_Neg)
            (cong1 (args2 conv)))
  in conv end;

fun Ipolex_polex_list_conv (rls as
      (_, _,
       [Ipolex_polex_list_Nil, Ipolex_polex_list_Cons], _, _, _)) l pps =
  (case strip_app pps of
     (\<^const_name>‹Nil›, []) => inst [] [l] Ipolex_polex_list_Nil
   | (\<^const_name>‹Cons›, [p, pps']) => (case strip_app p of
       (\<^const_name>‹Pair›, [P, Q]) =>
         transitive'
           (inst [] [l, P, Q, pps'] Ipolex_polex_list_Cons)
           (cong2
              (cong2 (args2 (Ipolex_conv rls)) (args2 (Ipolex_conv rls)))
              (args2 (Ipolex_polex_list_conv rls)))));

fun dest_conj th =
  let
    val th1 = th RS @{thm conjunct1};
    val th2 = th RS @{thm conjunct2}
  in
    dest_conj th1 @ dest_conj th2
  end handle THM _ => [th];

fun mk_in_carrier ctxt R prems xs =
  let
    val (_, _, _, [in_carrier_Nil, in_carrier_Cons], _, _) =
      get_ring_simps ctxt NONE R;
    val props = map fst (Facts.props (Proof_Context.facts_of ctxt)) @ maps dest_conj prems;
    val ths = map (fn p as (x, _) =>
      (case find_first
         ((fn \<^Const_>‹Trueprop
              for \<^Const_>‹Set.member _ for ‹Free (y, _)› \<^Const_>‹carrier _ _ for S››› =>
                x = y andalso R aconv S
            | _ => false) o Thm.prop_of) props of
         SOME th => th
       | NONE => error ("Variable " ^ Syntax.string_of_term ctxt (Free p) ^
           " not in carrier"))) xs
  in
    fold_rev (fn th1 => fn th2 => [th1, th2] MRS in_carrier_Cons)
       ths in_carrier_Nil
  end;

fun mk_ring T = \<^Const>‹cring_class_ops T›;

val iterations = \<^cterm>‹1000::nat›;
val Trueprop_cong = Thm.combination (Thm.reflexive \<^cterm>‹Trueprop›);

fun commutative_ring_conv ctxt prems eqs ct =
  let
    val cT = Thm.ctyp_of_cterm ct;
    val T = Thm.typ_of cT;
    val eqs' = map (HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of) eqs;
    val xs = filter (equal T o snd) (rev (fold Term.add_frees
      (map fst eqs' @ map snd eqs' @ [Thm.term_of ct]) []));
    val (R, optcT, prem', reif) = (case ring_struct (Thm.term_of ct) of
        SOME R => (R, NONE, mk_in_carrier ctxt R prems xs, reif_polex xs)
      | NONE => (mk_ring T, SOME cT, @{thm in_carrier_trivial}, reif_polex' xs));
    val rls as (_, _, _, _, _, norm_subst_correct) = get_ring_simps ctxt optcT R;
    val cxs = Thm.cterm_of ctxt (HOLogic.mk_list T (map Free xs));
    val ceqs = Thm.cterm_of ctxt (HOLogic.mk_list \<^typ>‹polex × polex›
      (map (HOLogic.mk_prod o apply2 reif) eqs'));
    val cp = Thm.cterm_of ctxt (reif (Thm.term_of ct));
    val prem = Thm.equal_elim
      (Trueprop_cong (Thm.symmetric (Ipolex_polex_list_conv rls cxs ceqs)))
      (fold_rev (fn th1 => fn th2 => [th1, th2] MRS @{thm conjI})
         eqs @{thm TrueI});
  in
    Thm.transitive
      (Thm.symmetric (Ipolex_conv rls cxs cp))
      (transitive'
         ([prem', prem] MRS inst [] [cxs, ceqs, cp, iterations, iterations]
            norm_subst_correct)
         (cong2' (Ipol_conv rls)
            Thm.reflexive
            (cv ctxt)))
  end;

fun ring_tac in_prems thms ctxt =
  tactic_of_conv (fn ct =>
    (if in_prems then Conv.prems_conv else Conv.concl_conv)
      (Logic.count_prems (Thm.term_of ct))
      (Conv.arg_conv (Conv.binop_conv (commutative_ring_conv ctxt [] thms))) ct) THEN'
  TRY o (assume_tac ctxt ORELSE' resolve_tac ctxt [@{thm refl}]);

end
›

context cring
begin

declaration ‹fn phi =>
  Ring_Tac.Ring_Simps.map (Ring_Tac.insert_rules Ring_Tac.eq_ring_simps
    (Morphism.term phi \<^term>‹R›,
     (Morphism.fact phi @{thms Ipol.simps [meta] Ipol_Pc [meta]},
      Morphism.fact phi @{thms Ipolex.simps [meta] Ipolex_Const [meta]},
      Morphism.fact phi @{thms Ipolex_polex_list.simps [meta]},
      Morphism.fact phi @{thms in_carrier_Nil in_carrier_Cons},
      singleton (Morphism.fact phi) @{thm head.simps(2) [meta]},
      singleton (Morphism.fact phi) @{thm norm_subst_correct [meta]})))
›

end

method_setup ring = ‹
  Scan.lift (Args.mode "prems") -- Attrib.thms >> (SIMPLE_METHOD' oo uncurry Ring_Tac.ring_tac)
› "simplify equations involving rings"

end