# Theory Commutative_Ring_Complete

Up to index of Isabelle/HOL/ex

theory Commutative_Ring_Complete
imports Commutative_Ring
begin

    (*  ID:         $Id: Commutative_Ring_Complete.thy,v 1.4 2005/09/20 12:03:37 wenzelm Exp $
        Author:     Bernhard Haeupler

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

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

    theory Commutative_Ring_Complete
    imports Commutative_Ring
    begin

      (* Fromalization of normal form *)
    consts isnorm :: "('a::{comm_ring,recpower}) pol => bool"
    recdef isnorm "measure size"
      "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)"

    (* Some helpful lemmas *)
    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"
    by(cases i,simp add: norm_Pinj_0_False norm_PX_0_False,cases Q) auto

    lemma norm_PX2:"isnorm (PX P i Q) ==> isnorm Q"
    by(cases i, auto, cases P, auto, case_tac pol2, auto)

    lemma norm_PX1:"isnorm (PX P i Q) ==> isnorm P"
    by(cases i, auto, cases P, auto, case_tac pol2, auto)

    lemma mkPinj_cn:"[|y~=0; isnorm Q|] ==> isnorm (mkPinj y Q)"
    apply(auto simp add: mkPinj_def norm_Pinj_0_False split: pol.split)
    apply(case_tac nat, auto simp add: norm_Pinj_0_False)
    by(case_tac pol, auto) (case_tac y, auto)

    lemma norm_PXtrans:
      assumes A:"isnorm (PX P x Q)" and "isnorm Q2"
      shows "isnorm (PX P x Q2)"
    proof(cases P)
      case (PX p1 y p2) from prems show ?thesis by(cases x, auto, cases p2, auto)
    next
      case Pc from prems show ?thesis by(cases x, auto)
    next
      case Pinj from prems show ?thesis by(cases x, auto)
    qed

    lemma norm_PXtrans2: assumes A:"isnorm (PX P x Q)" and "isnorm Q2" shows "isnorm (PX P (Suc (n+x)) Q2)"
    proof(cases P)
      case (PX p1 y p2)
      from prems show ?thesis by(cases x, auto, cases p2, auto)
    next
      case Pc
      from prems show ?thesis by(cases x, auto)
    next
      case Pinj
      from prems show ?thesis by(cases x, auto)
    qed

        (* mkPX conserves normalizedness (_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)
      from prems show ?thesis by (cases x) (auto simp add: mkPinj_cn mkPX_def)
    next
      case (Pinj i Q)
      from prems show ?thesis by (cases x) (auto simp add: mkPinj_cn mkPX_def)
    next
      case (PX P1 y P2)
      from prems have Y0:"y>0" by(cases y, auto)
      from prems have "isnorm P1" "isnorm P2" by (auto simp add: norm_PX1[of P1 y P2] norm_PX2[of P1 y P2])
      with prems Y0 show ?thesis by (cases x, auto simp add: mkPX_def norm_PXtrans2[of P1 y _ Q _], cases P2, auto)
    qed

        (* add conserves normalizedness *)
    lemma add_cn:"[|isnorm P; (isnorm Q)|] ==> isnorm (add (P, Q))"
    proof(induct P Q rule: add.induct)
      case (2 c i P2) thus ?case by (cases P2, simp_all, cases i, simp_all)
    next
      case (3 i P2 c) thus ?case by (cases P2, simp_all, cases i, simp_all)
    next
      case (4 c P2 i Q2)
      from prems have "isnorm P2" "isnorm Q2" by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
      with prems show ?case by(cases i, simp, cases P2, auto, case_tac pol2, auto)
    next
      case (5 P2 i Q2 c)
      from prems have "isnorm P2" "isnorm Q2" by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
      with prems show ?case by(cases i, simp, cases P2, auto, case_tac pol2, auto)
    next
      case (6 x P2 y Q2)
      from prems have Y0:"y>0" by (cases y, auto simp add: norm_Pinj_0_False)
      from prems have X0:"x>0" by (cases x, auto simp add: norm_Pinj_0_False)
      have "x < y ∨ x = y ∨ x > y" by arith
      moreover
      { assume "x<y" hence "EX d. y=d+x" by arith
        then obtain d where "y=d+x"..
        moreover
        note prems X0
        moreover
        from prems have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
        moreover
        with prems have "isnorm (Pinj d Q2)" by (cases d, simp, cases Q2, auto)
        ultimately have ?case by (simp add: mkPinj_cn)}
      moreover
      { assume "x=y"
        moreover
        from prems have "isnorm P2" "isnorm Q2" by(auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
        moreover
        note prems Y0
        moreover
        ultimately have ?case by (simp add: mkPinj_cn) }
      moreover
      { assume "x>y" hence "EX d. x=d+y" by arith
        then obtain d where "x=d+y"..
        moreover
        note prems Y0
        moreover
        from prems have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
        moreover
        with prems have "isnorm (Pinj d P2)" by (cases d, simp, cases P2, auto)
        ultimately have ?case by (simp add: mkPinj_cn)}
      ultimately show ?case by blast
    next
      case (7 x P2 Q2 y R)
      have "x=0 ∨ (x = 1) ∨ (x > 1)" by arith
      moreover
      { assume "x=0" with prems have ?case by (auto simp add: norm_Pinj_0_False)}
      moreover
      { assume "x=1"
        from prems have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
        with prems have "isnorm (add (R, P2))" by simp
        with prems have ?case by (simp add: norm_PXtrans[of Q2 y _]) }
      moreover
      { assume "x > 1" hence "EX d. x=Suc (Suc d)" by arith
        then obtain d where X:"x=Suc (Suc d)" ..
        from prems have NR:"isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
        with prems have "isnorm (Pinj (x - 1) P2)" by(cases P2, auto)
        with prems NR have "isnorm( add (R, Pinj (x - 1) P2))" "isnorm(PX Q2 y R)" by simp
        with X have ?case by (simp add: norm_PXtrans[of Q2 y _]) }
      ultimately show ?case by blast
    next
      case (8 Q2 y R x P2)
      have "x=0 ∨ (x = 1) ∨ (x > 1)" by arith
      moreover
      { assume "x=0" with prems have ?case by (auto simp add: norm_Pinj_0_False)}
      moreover
      { assume "x=1"
        from prems have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
        with prems have "isnorm (add (R, P2))" by simp
        with prems have ?case by (simp add: norm_PXtrans[of Q2 y _]) }
      moreover
      { assume "x > 1" hence "EX d. x=Suc (Suc d)" by arith
        then obtain d where X:"x=Suc (Suc d)" ..
        from prems have NR:"isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
        with prems have "isnorm (Pinj (x - 1) P2)" by(cases P2, auto)
        with prems NR have "isnorm( add (R, Pinj (x - 1) P2))" "isnorm(PX Q2 y R)" by simp
        with X have ?case by (simp add: norm_PXtrans[of Q2 y _]) }
      ultimately show ?case by blast
    next
      case (9 P1 x P2 Q1 y Q2)
      from prems have Y0:"y>0" by(cases y, auto)
      from prems have X0:"x>0" by(cases x, auto)
      from prems have NP1:"isnorm P1" and NP2:"isnorm P2" by (auto simp add: norm_PX1[of P1 _ P2] norm_PX2[of P1 _ P2])
      from prems have NQ1:"isnorm Q1" and NQ2:"isnorm Q2" by (auto simp add: norm_PX1[of Q1 _ Q2] norm_PX2[of Q1 _ Q2])
      have "y < x ∨ x = y ∨ x < y" by arith
      moreover
      {assume sm1:"y < x" hence "EX d. x=d+y" by arith
        then obtain d where sm2:"x=d+y"..
        note prems NQ1 NP1 NP2 NQ2 sm1 sm2
        moreover
        have "isnorm (PX P1 d (Pc 0))"
        proof(cases P1)
          case (PX p1 y p2)
          with prems show ?thesis by(cases d, simp,cases p2, auto)
        next case Pc   from prems show ?thesis by(cases d, auto)
        next case Pinj from prems show ?thesis by(cases d, auto)
        qed
        ultimately have "isnorm (add (P2, Q2))" "isnorm (add (PX P1 (x - y) (Pc 0), Q1))" by auto
        with Y0 sm1 sm2 have ?case by (simp add: mkPX_cn)}
      moreover
      {assume "x=y"
        from prems NP1 NP2 NQ1 NQ2 have "isnorm (add (P2, Q2))" "isnorm (add (P1, Q1))" by auto
        with Y0 prems have ?case by (simp add: mkPX_cn) }
      moreover
      {assume sm1:"x<y" hence "EX d. y=d+x" by arith
        then obtain d where sm2:"y=d+x"..
        note prems NQ1 NP1 NP2 NQ2 sm1 sm2
        moreover
        have "isnorm (PX Q1 d (Pc 0))"
        proof(cases Q1)
          case (PX p1 y p2)
          with prems show ?thesis by(cases d, simp,cases p2, auto)
        next case Pc   from prems show ?thesis by(cases d, auto)
        next case Pinj from prems show ?thesis by(cases d, auto)
        qed
        ultimately have "isnorm (add (P2, Q2))" "isnorm (add (PX Q1 (y - x) (Pc 0), P1))" by auto
        with X0 sm1 sm2 have ?case by (simp add: mkPX_cn)}
      ultimately show ?case by blast
    qed(simp)

        (* mul concerves normalizedness *)
    lemma mul_cn :"[|isnorm P; (isnorm Q)|] ==> isnorm (mul (P, Q))"
    proof(induct P Q rule: mul.induct)
      case (2 c i P2) thus ?case
        by (cases P2, simp_all) (cases "i",simp_all add: mkPinj_cn)
    next
      case (3 i P2 c) thus ?case
        by (cases P2, simp_all) (cases "i",simp_all add: mkPinj_cn)
    next
      case (4 c P2 i Q2)
      from prems have "isnorm P2" "isnorm Q2" by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
      with prems show ?case
        by - (case_tac "c=0",simp_all,case_tac "i=0",simp_all add: mkPX_cn)
    next
      case (5 P2 i Q2 c)
      from prems have "isnorm P2" "isnorm Q2" by (auto simp only: norm_PX1[of P2 i Q2] norm_PX2[of P2 i Q2])
      with prems show ?case
        by - (case_tac "c=0",simp_all,case_tac "i=0",simp_all add: mkPX_cn)
    next
      case (6 x P2 y Q2)
      have "x < y ∨ x = y ∨ x > y" by arith
      moreover
      { assume "x<y" hence "EX d. y=d+x" by arith
        then obtain d where "y=d+x"..
        moreover
        note prems
        moreover
        from prems have "x>0" by (cases x, auto simp add: norm_Pinj_0_False)
        moreover
        from prems have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
        moreover
        with prems have "isnorm (Pinj d Q2)" by (cases d, simp, cases Q2, auto)
        ultimately have ?case by (simp add: mkPinj_cn)}
      moreover
      { assume "x=y"
        moreover
        from prems have "isnorm P2" "isnorm Q2" by(auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
        moreover
        with prems have "y>0" by (cases y, auto simp add: norm_Pinj_0_False)
        moreover
        note prems
        moreover
        ultimately have ?case by (simp add: mkPinj_cn) }
      moreover
      { assume "x>y" hence "EX d. x=d+y" by arith
        then obtain d where "x=d+y"..
        moreover
        note prems
        moreover
        from prems have "y>0" by (cases y, auto simp add: norm_Pinj_0_False)
        moreover
        from prems have "isnorm P2" "isnorm Q2" by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
        moreover
        with prems have "isnorm (Pinj d P2)"  by (cases d, simp, cases P2, auto)
        ultimately have ?case by (simp add: mkPinj_cn) }
      ultimately show ?case by blast
    next
      case (7 x P2 Q2 y R)
      from prems have Y0:"y>0" by(cases y, auto)
      have "x=0 ∨ (x = 1) ∨ (x > 1)" by arith
      moreover
      { assume "x=0" with prems have ?case by (auto simp add: norm_Pinj_0_False)}
      moreover
      { assume "x=1"
        from prems have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
        with prems have "isnorm (mul (R, P2))" "isnorm Q2" by (auto simp add: norm_PX1[of Q2 y R])
        with Y0 prems have ?case by (simp add: mkPX_cn)}
      moreover
      { assume "x > 1" hence "EX d. x=Suc (Suc d)" by arith
        then obtain d where X:"x=Suc (Suc d)" ..
        from prems have NR:"isnorm R" "isnorm Q2" by (auto simp add: norm_PX2[of Q2 y R] norm_PX1[of Q2 y R])
        moreover
        from prems have "isnorm (Pinj (x - 1) P2)" by(cases P2, auto)
        moreover
        from prems have "isnorm (Pinj x P2)" by(cases P2, auto)
        moreover
        note prems
        ultimately have "isnorm (mul (R, Pinj (x - 1) P2))" "isnorm (mul (Pinj x P2, Q2))" by auto
        with Y0 X have ?case by (simp add: mkPX_cn)}
      ultimately show ?case by blast
    next
      case (8 Q2 y R x P2)
      from prems have Y0:"y>0" by(cases y, auto)
      have "x=0 ∨ (x = 1) ∨ (x > 1)" by arith
      moreover
      { assume "x=0" with prems have ?case by (auto simp add: norm_Pinj_0_False)}
      moreover
      { assume "x=1"
        from prems have "isnorm R" "isnorm P2" by (auto simp add: norm_Pinj[of _ P2] norm_PX2[of Q2 y R])
        with prems have "isnorm (mul (R, P2))" "isnorm Q2" by (auto simp add: norm_PX1[of Q2 y R])
        with Y0 prems have ?case by (simp add: mkPX_cn) }
      moreover
      { assume "x > 1" hence "EX d. x=Suc (Suc d)" by arith
        then obtain d where X:"x=Suc (Suc d)" ..
        from prems have NR:"isnorm R" "isnorm Q2" by (auto simp add: norm_PX2[of Q2 y R] norm_PX1[of Q2 y R])
        moreover
        from prems have "isnorm (Pinj (x - 1) P2)" by(cases P2, auto)
        moreover
        from prems have "isnorm (Pinj x P2)" by(cases P2, auto)
        moreover
        note prems
        ultimately have "isnorm (mul (R, Pinj (x - 1) P2))" "isnorm (mul (Pinj x P2, Q2))" by auto
        with Y0 X have ?case by (simp add: mkPX_cn) }
      ultimately show ?case by blast
    next
      case (9 P1 x P2 Q1 y Q2)
      from prems have X0:"x>0" by(cases x, auto)
      from prems have Y0:"y>0" by(cases y, auto)
      note prems
      moreover
      from prems have "isnorm P1" "isnorm P2" by (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2])
      moreover
      from prems have "isnorm Q1" "isnorm Q2" by (auto simp add: norm_PX1[of Q1 y Q2] norm_PX2[of Q1 y Q2])
      ultimately have "isnorm (mul (P1, Q1))" "isnorm (mul (P2, Q2))" "isnorm (mul (P1, mkPinj 1 Q2))" "isnorm (mul (Q1, mkPinj 1 P2))"
        by (auto simp add: mkPinj_cn)
      with prems X0 Y0 have "isnorm (mkPX (mul (P1, Q1)) (x + y) (mul (P2, Q2)))" "isnorm (mkPX (mul (P1, mkPinj (Suc 0) Q2)) x (Pc 0))"
        "isnorm (mkPX (mul (Q1, mkPinj (Suc 0) P2)) y (Pc 0))"
        by (auto simp add: mkPX_cn)
      thus ?case by (simp add: add_cn)
    qed(simp)

        (* neg conserves normalizedness *)
    lemma neg_cn: "isnorm P ==> isnorm (neg P)"
    proof(induct P rule: neg.induct)
      case (Pinj i P2)
      from prems have "isnorm P2" by (simp add: norm_Pinj[of i P2])
      with prems show ?case by(cases P2, auto, cases i, auto)
    next
      case (PX P1 x P2)
      from prems have "isnorm P2" "isnorm P1" by (auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2])
      with prems show ?case
      proof(cases P1)
        case (PX p1 y p2)
        with prems show ?thesis by(cases x, auto, cases p2, auto)
      next
        case Pinj
        with prems show ?thesis by(cases x, auto)
      qed(cases x, auto)
    qed(simp)

        (* sub conserves normalizedness *)
    lemma sub_cn:"[|isnorm p; isnorm q|] ==> isnorm (sub p q)"
    by (simp add: sub_def add_cn neg_cn)

      (* sqr conserves normalizizedness *)
    lemma sqr_cn:"isnorm P ==> isnorm (sqr P)"
    proof(induct P)
      case (Pinj i Q)
      from prems show ?case by(cases Q, auto simp add: mkPX_cn mkPinj_cn, cases i, auto simp add: mkPX_cn mkPinj_cn)
    next
      case (PX P1 x P2)
      from prems have "x+x~=0" "isnorm P2" "isnorm P1" by (cases x,  auto simp add: norm_PX1[of P1 x P2] norm_PX2[of P1 x P2])
      with prems have "isnorm (mkPX (mul (mul (Pc ((1::'a) + (1::'a)), P1), mkPinj (Suc 0) P2)) x (Pc (0::'a)))"
                  and "isnorm (mkPX (sqr P1) (x + x) (sqr P2))" by( auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn)
      thus ?case by( auto simp add: add_cn mkPX_cn mkPinj_cn mul_cn)
    qed(simp)

        (* pow conserves normalizedness  *)
    lemma pow_cn:"!! P. [|isnorm P|] ==> isnorm (pow (P, n))"
    proof(induct n rule: nat_less_induct)
      case (1 k)
      show ?case
      proof(cases "k=0")
        case False
        hence K2:"k div 2 < k" by (cases k, auto)
        from prems have "isnorm (sqr P)" by (simp add: sqr_cn)
        with prems K2 show ?thesis by(simp add: allE[of _ "(k div 2)" _] allE[of _ "(sqr P)" _], cases k, auto simp add: mul_cn)
      qed(simp)
    qed

    end

lemma norm_Pinj_0_False:

      isnorm (Pinj 0 P) = False

lemma norm_PX_0_False:

      isnorm (PX (Pc (0::'a)) i Q) = False

lemma norm_Pinj:

      isnorm (Pinj i Q) ==> isnorm Q

lemma norm_PX2:

      isnorm (PX P i Q) ==> isnorm Q

lemma norm_PX1:

      isnorm (PX P i Q) ==> isnorm P

lemma mkPinj_cn:

      [| y ≠ 0; isnorm Q |] ==> isnorm (mkPinj y Q)

lemma norm_PXtrans:

      [| isnorm (PX P x Q); isnorm Q2.0 |] ==> isnorm (PX P x Q2.0)

lemma norm_PXtrans2:

      [| isnorm (PX P x Q); isnorm Q2.0 |] ==> isnorm (PX P (Suc (n + x)) Q2.0)

lemma mkPX_cn:

      [| x ≠ 0; isnorm P; isnorm Q |] ==> isnorm (mkPX P x Q)

lemma add_cn:

      [| isnorm P; isnorm Q |] ==> isnorm (add (P, Q))

lemma mul_cn:

      [| isnorm P; isnorm Q |] ==> isnorm (mul (P, Q))

lemma neg_cn:

      isnorm P ==> isnorm (Commutative_Ring.neg P)

lemma sub_cn:

      [| isnorm p; isnorm q |] ==> isnorm (sub p q)

lemma sqr_cn:

      isnorm P ==> isnorm (sqr P)

lemma pow_cn:

      isnorm P ==> isnorm (pow (P, n))