[STATEMENT]
lemma dupe_monic:
  fixes D :: "'a :: prime_card mod_ring poly"
  assumes 1: "D*S + H*T = 1"
  and mon: "monic D"
  and dupe: "dupe_monic D H S T U = (A,B)"
  shows "A * D + B * H = U" "B = 0 \<or> degree B < degree D"
    "coprime D H \<Longrightarrow> A' * D + B' * H = U \<Longrightarrow> B' = 0 \<or> degree B' < degree D \<Longrightarrow> A' = A \<and> B' = B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A * D + B * H = U &&& B = 0 \<or> degree B < degree D &&& (\<lbrakk>comm_monoid_mult_class.coprime D H; A' * D + B' * H = U; B' = 0 \<or> degree B' < degree D\<rbrakk> \<Longrightarrow> A' = A \<and> B' = B)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. A * D + B * H = U
 2. B = 0 \<or> degree B < degree D
 3. \<lbrakk>comm_monoid_mult_class.coprime D H; A' * D + B' * H = U; B' = 0 \<or> degree B' < degree D\<rbrakk> \<Longrightarrow> A' = A \<and> B' = B
[PROOF STEP]
obtain q r where div: "pdivmod_monic (T * U) D = (q,r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>q r. pdivmod_monic (T * U) D = (q, r) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
pdivmod_monic (T * U) D = (q, r)

goal (3 subgoals):
 1. A * D + B * H = U
 2. B = 0 \<or> degree B < degree D
 3. \<lbrakk>comm_monoid_mult_class.coprime D H; A' * D + B' * H = U; B' = 0 \<or> degree B' < degree D\<rbrakk> \<Longrightarrow> A' = A \<and> B' = B
[PROOF STEP]
from dupe[unfolded dupe_monic_def div split]
[PROOF STATE]
proof (chain)
picking this:
(S * U + H * q, r) = (A, B)
[PROOF STEP]
have A: "A = (S * U + H * q)" and B: "B = r"
[PROOF STATE]
proof (prove)
using this:
(S * U + H * q, r) = (A, B)

goal (1 subgoal):
 1. A = S * U + H * q &&& B = r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A = S * U + H * q
B = r

goal (3 subgoals):
 1. A * D + B * H = U
 2. B = 0 \<or> degree B < degree D
 3. \<lbrakk>comm_monoid_mult_class.coprime D H; A' * D + B' * H = U; B' = 0 \<or> degree B' < degree D\<rbrakk> \<Longrightarrow> A' = A \<and> B' = B
[PROOF STEP]
from pdivmod_monic[OF mon div]
[PROOF STATE]
proof (chain)
picking this:
T * U = D * q + r
r = 0 \<or> degree r < degree D
[PROOF STEP]
have TU: "T * U = D * q + r" and
    deg: "r = 0 \<or> degree r < degree D"
[PROOF STATE]
proof (prove)
using this:
T * U = D * q + r
r = 0 \<or> degree r < degree D

goal (1 subgoal):
 1. T * U = D * q + r &&& r = 0 \<or> degree r < degree D
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
T * U = D * q + r
r = 0 \<or> degree r < degree D

goal (3 subgoals):
 1. A * D + B * H = U
 2. B = 0 \<or> degree B < degree D
 3. \<lbrakk>comm_monoid_mult_class.coprime D H; A' * D + B' * H = U; B' = 0 \<or> degree B' < degree D\<rbrakk> \<Longrightarrow> A' = A \<and> B' = B
[PROOF STEP]
hence r: "r = T * U - D * q"
[PROOF STATE]
proof (prove)
using this:
T * U = D * q + r
r = 0 \<or> degree r < degree D

goal (1 subgoal):
 1. r = T * U - D * q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
r = T * U - D * q

goal (3 subgoals):
 1. A * D + B * H = U
 2. B = 0 \<or> degree B < degree D
 3. \<lbrakk>comm_monoid_mult_class.coprime D H; A' * D + B' * H = U; B' = 0 \<or> degree B' < degree D\<rbrakk> \<Longrightarrow> A' = A \<and> B' = B
[PROOF STEP]
have "A * D + B * H = (S * U + H * q) * D + (T * U - D * q) * H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A * D + B * H = (S * U + H * q) * D + (T * U - D * q) * H
[PROOF STEP]
unfolding A B r
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (S * U + H * q) * D + (T * U - D * q) * H = (S * U + H * q) * D + (T * U - D * q) * H
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
A * D + B * H = (S * U + H * q) * D + (T * U - D * q) * H

goal (3 subgoals):
 1. A * D + B * H = U
 2. B = 0 \<or> degree B < degree D
 3. \<lbrakk>comm_monoid_mult_class.coprime D H; A' * D + B' * H = U; B' = 0 \<or> degree B' < degree D\<rbrakk> \<Longrightarrow> A' = A \<and> B' = B
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
A * D + B * H = (S * U + H * q) * D + (T * U - D * q) * H

goal (3 subgoals):
 1. A * D + B * H = U
 2. B = 0 \<or> degree B < degree D
 3. \<lbrakk>comm_monoid_mult_class.coprime D H; A' * D + B' * H = U; B' = 0 \<or> degree B' < degree D\<rbrakk> \<Longrightarrow> A' = A \<and> B' = B
[PROOF STEP]
have "... = (D * S + H * T) * U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (S * U + H * q) * D + (T * U - D * q) * H = (D * S + H * T) * U
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
(S * U + H * q) * D + (T * U - D * q) * H = (D * S + H * T) * U

goal (3 subgoals):
 1. A * D + B * H = U
 2. B = 0 \<or> degree B < degree D
 3. \<lbrakk>comm_monoid_mult_class.coprime D H; A' * D + B' * H = U; B' = 0 \<or> degree B' < degree D\<rbrakk> \<Longrightarrow> A' = A \<and> B' = B
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(S * U + H * q) * D + (T * U - D * q) * H = (D * S + H * T) * U

goal (3 subgoals):
 1. A * D + B * H = U
 2. B = 0 \<or> degree B < degree D
 3. \<lbrakk>comm_monoid_mult_class.coprime D H; A' * D + B' * H = U; B' = 0 \<or> degree B' < degree D\<rbrakk> \<Longrightarrow> A' = A \<and> B' = B
[PROOF STEP]
have "D * S + H * T = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. D * S + H * T = 1
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
D * S + H * T = 1

goal (1 subgoal):
 1. D * S + H * T = 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
D * S + H * T = 1

goal (3 subgoals):
 1. A * D + B * H = U
 2. B = 0 \<or> degree B < degree D
 3. \<lbrakk>comm_monoid_mult_class.coprime D H; A' * D + B' * H = U; B' = 0 \<or> degree B' < degree D\<rbrakk> \<Longrightarrow> A' = A \<and> B' = B
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
A * D + B * H = 1 * U
[PROOF STEP]
show eq: "A * D + B * H = U"
[PROOF STATE]
proof (prove)
using this:
A * D + B * H = 1 * U

goal (1 subgoal):
 1. A * D + B * H = U
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
A * D + B * H = U

goal (2 subgoals):
 1. B = 0 \<or> degree B < degree D
 2. \<lbrakk>comm_monoid_mult_class.coprime D H; A' * D + B' * H = U; B' = 0 \<or> degree B' < degree D\<rbrakk> \<Longrightarrow> A' = A \<and> B' = B
[PROOF STEP]
show degB: "B = 0 \<or> degree B < degree D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B = 0 \<or> degree B < degree D
[PROOF STEP]
using deg
[PROOF STATE]
proof (prove)
using this:
r = 0 \<or> degree r < degree D

goal (1 subgoal):
 1. B = 0 \<or> degree B < degree D
[PROOF STEP]
unfolding B
[PROOF STATE]
proof (prove)
using this:
r = 0 \<or> degree r < degree D

goal (1 subgoal):
 1. r = 0 \<or> degree r < degree D
[PROOF STEP]
by (cases "r = 0", auto)
[PROOF STATE]
proof (state)
this:
B = 0 \<or> degree B < degree D

goal (1 subgoal):
 1. \<lbrakk>comm_monoid_mult_class.coprime D H; A' * D + B' * H = U; B' = 0 \<or> degree B' < degree D\<rbrakk> \<Longrightarrow> A' = A \<and> B' = B
[PROOF STEP]
assume another: "A' * D + B' * H = U" and degB': "B' = 0 \<or> degree B' < degree D"
    and cop: "coprime D H"
[PROOF STATE]
proof (state)
this:
A' * D + B' * H = U
B' = 0 \<or> degree B' < degree D
comm_monoid_mult_class.coprime D H

goal (1 subgoal):
 1. \<lbrakk>comm_monoid_mult_class.coprime D H; A' * D + B' * H = U; B' = 0 \<or> degree B' < degree D\<rbrakk> \<Longrightarrow> A' = A \<and> B' = B
[PROOF STEP]
from degB
[PROOF STATE]
proof (chain)
picking this:
B = 0 \<or> degree B < degree D
[PROOF STEP]
have degB: "B = 0 \<or> degree B < degree D"
[PROOF STATE]
proof (prove)
using this:
B = 0 \<or> degree B < degree D

goal (1 subgoal):
 1. B = 0 \<or> degree B < degree D
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
B = 0 \<or> degree B < degree D

goal (1 subgoal):
 1. \<lbrakk>comm_monoid_mult_class.coprime D H; A' * D + B' * H = U; B' = 0 \<or> degree B' < degree D\<rbrakk> \<Longrightarrow> A' = A \<and> B' = B
[PROOF STEP]
from degB'
[PROOF STATE]
proof (chain)
picking this:
B' = 0 \<or> degree B' < degree D
[PROOF STEP]
have degB': "B' = 0 \<or> degree B' < degree D"
[PROOF STATE]
proof (prove)
using this:
B' = 0 \<or> degree B' < degree D

goal (1 subgoal):
 1. B' = 0 \<or> degree B' < degree D
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
B' = 0 \<or> degree B' < degree D

goal (1 subgoal):
 1. \<lbrakk>comm_monoid_mult_class.coprime D H; A' * D + B' * H = U; B' = 0 \<or> degree B' < degree D\<rbrakk> \<Longrightarrow> A' = A \<and> B' = B
[PROOF STEP]
from mon
[PROOF STATE]
proof (chain)
picking this:
monic D
[PROOF STEP]
have D0: "D \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
monic D

goal (1 subgoal):
 1. D \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
D \<noteq> 0

goal (1 subgoal):
 1. \<lbrakk>comm_monoid_mult_class.coprime D H; A' * D + B' * H = U; B' = 0 \<or> degree B' < degree D\<rbrakk> \<Longrightarrow> A' = A \<and> B' = B
[PROOF STEP]
from another eq
[PROOF STATE]
proof (chain)
picking this:
A' * D + B' * H = U
A * D + B * H = U
[PROOF STEP]
have "A' * D + B' * H = A * D + B * H"
[PROOF STATE]
proof (prove)
using this:
A' * D + B' * H = U
A * D + B * H = U

goal (1 subgoal):
 1. A' * D + B' * H = A * D + B * H
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
A' * D + B' * H = A * D + B * H

goal (1 subgoal):
 1. \<lbrakk>comm_monoid_mult_class.coprime D H; A' * D + B' * H = U; B' = 0 \<or> degree B' < degree D\<rbrakk> \<Longrightarrow> A' = A \<and> B' = B
[PROOF STEP]
from uniqueness_poly_equality[OF cop degB' degB D0 this]
[PROOF STATE]
proof (chain)
picking this:
A' = A
B' = B
[PROOF STEP]
show "A' = A \<and> B' = B"
[PROOF STATE]
proof (prove)
using this:
A' = A
B' = B

goal (1 subgoal):
 1. A' = A \<and> B' = B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A' = A \<and> B' = B

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma deg_v: "degree (#v :: 'p mod_ring poly) = degree v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (#v) = degree v
[PROOF STEP]
using monic_v
[PROOF STATE]
proof (prove)
using this:
monic v

goal (1 subgoal):
 1. degree (#v) = degree v
[PROOF STEP]
by (simp add: of_int_hom.monic_degree_map_poly_hom)


[STATEMENT]
lemma u0: "u \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<noteq> 0
[PROOF STEP]
using degu bv
[PROOF STATE]
proof (prove)
using this:
degree u = degree v + degree w
degree b < degree v

goal (1 subgoal):
 1. u \<noteq> 0
[PROOF STEP]
by auto


[STATEMENT]
lemma ex_f: "\<exists>f :: 'p mod_ring poly. u = #v * #w + smult (of_nat q) (#f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>f. u = #v * #w + Polynomial.smult (of_nat q) (#f)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>f. u = #v * #w + Polynomial.smult (of_nat q) (#f)
[PROOF STEP]
from uvw
[PROOF STATE]
proof (chain)
picking this:
#u = v * w
[PROOF STEP]
have "(#(u - #v * #w) :: 'q mod_ring poly) = 0"
[PROOF STATE]
proof (prove)
using this:
#u = v * w

goal (1 subgoal):
 1. #(u - #v * #w) = 0
[PROOF STEP]
by (auto simp:hom_distribs)
[PROOF STATE]
proof (state)
this:
#(u - #v * #w) = 0

goal (1 subgoal):
 1. \<exists>f. u = #v * #w + Polynomial.smult (of_nat q) (#f)
[PROOF STEP]
from rebase_pq_to_q.rebase_poly_eq_0_imp_ex_smult[OF this]
[PROOF STATE]
proof (chain)
picking this:
\<exists>p'. (u - #v * #w = 0) = (p' = 0) \<and> degree p' \<le> degree (u - #v * #w) \<and> u - #v * #w = Polynomial.smult (of_nat CARD('q)) (#p')
[PROOF STEP]
obtain f :: "'p mod_ring poly" where "u - #v * #w = smult (of_nat q) (#f)"
[PROOF STATE]
proof (prove)
using this:
\<exists>p'. (u - #v * #w = 0) = (p' = 0) \<and> degree p' \<le> degree (u - #v * #w) \<and> u - #v * #w = Polynomial.smult (of_nat CARD('q)) (#p')

goal (1 subgoal):
 1. (\<And>f. u - #v * #w = Polynomial.smult (of_nat q) (#f) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
u - #v * #w = Polynomial.smult (of_nat q) (#f)

goal (1 subgoal):
 1. \<exists>f. u = #v * #w + Polynomial.smult (of_nat q) (#f)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
u - #v * #w = Polynomial.smult (of_nat q) (#f)
[PROOF STEP]
have "u = #v * #w + smult (of_nat q) (#f)"
[PROOF STATE]
proof (prove)
using this:
u - #v * #w = Polynomial.smult (of_nat q) (#f)

goal (1 subgoal):
 1. u = #v * #w + Polynomial.smult (of_nat q) (#f)
[PROOF STEP]
by (metis add_diff_cancel_left' add_diff_eq)
[PROOF STATE]
proof (state)
this:
u = #v * #w + Polynomial.smult (of_nat q) (#f)

goal (1 subgoal):
 1. \<exists>f. u = #v * #w + Polynomial.smult (of_nat q) (#f)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
u = #v * #w + Polynomial.smult (of_nat q) (#f)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
u = #v * #w + Polynomial.smult (of_nat q) (#f)

goal (1 subgoal):
 1. \<exists>f. u = #v * #w + Polynomial.smult (of_nat q) (#f)
[PROOF STEP]
by (intro exI[of _ f], auto)
[PROOF STATE]
proof (state)
this:
\<exists>f. u = #v * #w + Polynomial.smult (of_nat q) (#f)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma u: "u = #v * #w + smult (of_nat q) (#f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u = #v * #w + Polynomial.smult (of_nat q) (#f)
[PROOF STEP]
using ex_f[folded some_eq_ex] f_def
[PROOF STATE]
proof (prove)
using this:
u = #v * #w + Polynomial.smult (of_nat q) (#(SOME f. u = #v * #w + Polynomial.smult (of_nat q) (#f)))
f \<equiv> SOME f. u = #v * #w + Polynomial.smult (of_nat q) (#f)

goal (1 subgoal):
 1. u = #v * #w + Polynomial.smult (of_nat q) (#f)
[PROOF STEP]
by auto


[STATEMENT]
lemma t_ex: "\<exists>t :: 'p mod_ring poly. degree (b * f - t * #v) < degree v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>t. degree (b * f - t * #v) < degree v
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>t. degree (b * f - t * #v) < degree v
[PROOF STEP]
define v' where "v' \<equiv> #v :: 'p mod_ring poly"
[PROOF STATE]
proof (state)
this:
v' \<equiv> #v

goal (1 subgoal):
 1. \<exists>t. degree (b * f - t * #v) < degree v
[PROOF STEP]
from monic_v
[PROOF STATE]
proof (chain)
picking this:
monic v
[PROOF STEP]
have 1: "lead_coeff v' = 1"
[PROOF STATE]
proof (prove)
using this:
monic v

goal (1 subgoal):
 1. monic v'
[PROOF STEP]
by (simp add: v'_def deg_v)
[PROOF STATE]
proof (state)
this:
monic v'

goal (1 subgoal):
 1. \<exists>t. degree (b * f - t * #v) < degree v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
monic v'
[PROOF STEP]
have 4: "v' \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
monic v'

goal (1 subgoal):
 1. v' \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v' \<noteq> 0

goal (1 subgoal):
 1. \<exists>t. degree (b * f - t * #v) < degree v
[PROOF STEP]
obtain t rem :: "'p mod_ring poly"
  where "pseudo_divmod (b * f) v' = (t,rem)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>t rem. pseudo_divmod (b * f) v' = (t, rem) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
pseudo_divmod (b * f) v' = (t, rem)

goal (1 subgoal):
 1. \<exists>t. degree (b * f - t * #v) < degree v
[PROOF STEP]
from pseudo_divmod[OF 4 this, folded, unfolded 1]
[PROOF STATE]
proof (chain)
picking this:
Polynomial.smult (1 ^ (Suc (degree (b * f)) - degree v')) (b * f) = v' * t + rem
rem = 0 \<or> degree rem < degree v'
[PROOF STEP]
have "b * f = v' * t + rem" and deg: "rem = 0 \<or> degree rem < degree v'"
[PROOF STATE]
proof (prove)
using this:
Polynomial.smult (1 ^ (Suc (degree (b * f)) - degree v')) (b * f) = v' * t + rem
rem = 0 \<or> degree rem < degree v'

goal (1 subgoal):
 1. b * f = v' * t + rem &&& rem = 0 \<or> degree rem < degree v'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
b * f = v' * t + rem
rem = 0 \<or> degree rem < degree v'

goal (1 subgoal):
 1. \<exists>t. degree (b * f - t * #v) < degree v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b * f = v' * t + rem
rem = 0 \<or> degree rem < degree v'
[PROOF STEP]
have "rem = b * f - t * v'"
[PROOF STATE]
proof (prove)
using this:
b * f = v' * t + rem
rem = 0 \<or> degree rem < degree v'

goal (1 subgoal):
 1. rem = b * f - t * v'
[PROOF STEP]
by(auto simp: ac_simps)
[PROOF STATE]
proof (state)
this:
rem = b * f - t * v'

goal (1 subgoal):
 1. \<exists>t. degree (b * f - t * #v) < degree v
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
rem = b * f - t * v'

goal (1 subgoal):
 1. \<exists>t. degree (b * f - t * #v) < degree v
[PROOF STEP]
have "... = b * f - #(#t :: 'p mod_ring poly) * v'" (is "_ = _ - ?t * v'")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b * f - t * v' = b * f - ##t * v'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
b * f - t * v' = b * f - ##t * v'

goal (1 subgoal):
 1. \<exists>t. degree (b * f - t * #v) < degree v
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
b * f - t * v' = b * f - ##t * v'

goal (1 subgoal):
 1. \<exists>t. degree (b * f - t * #v) < degree v
[PROOF STEP]
have "... = b * f - ?t * #v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b * f - ##t * v' = b * f - ##t * #v
[PROOF STEP]
by (unfold v'_def, rule)
[PROOF STATE]
proof (state)
this:
b * f - ##t * v' = b * f - ##t * #v

goal (1 subgoal):
 1. \<exists>t. degree (b * f - t * #v) < degree v
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
rem = b * f - ##t * #v
[PROOF STEP]
have "degree rem = degree ..."
[PROOF STATE]
proof (prove)
using this:
rem = b * f - ##t * #v

goal (1 subgoal):
 1. degree rem = degree (b * f - ##t * #v)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
degree rem = degree (b * f - ##t * #v)

goal (1 subgoal):
 1. \<exists>t. degree (b * f - t * #v) < degree v
[PROOF STEP]
with deg bv
[PROOF STATE]
proof (chain)
picking this:
rem = 0 \<or> degree rem < degree v'
degree b < degree v
degree rem = degree (b * f - ##t * #v)
[PROOF STEP]
have "degree (b * f - ?t * #v :: 'p mod_ring poly) < degree v"
[PROOF STATE]
proof (prove)
using this:
rem = 0 \<or> degree rem < degree v'
degree b < degree v
degree rem = degree (b * f - ##t * #v)

goal (1 subgoal):
 1. degree (b * f - ##t * #v) < degree v
[PROOF STEP]
by (auto simp: v'_def deg_v)
[PROOF STATE]
proof (state)
this:
degree (b * f - ##t * #v) < degree v

goal (1 subgoal):
 1. \<exists>t. degree (b * f - t * #v) < degree v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
degree (b * f - ##t * #v) < degree v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
degree (b * f - ##t * #v) < degree v

goal (1 subgoal):
 1. \<exists>t. degree (b * f - t * #v) < degree v
[PROOF STEP]
by (rule exI)
[PROOF STATE]
proof (state)
this:
\<exists>t. degree (b * f - t * #v) < degree v

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma f: "w' * #v + v' * #w = f" (is "?l = _")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w' * #v + v' * #w = f
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. w' * #v + v' * #w = f
[PROOF STEP]
have "?l = f * (a * #v + b * #w :: 'p mod_ring poly)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w' * #v + v' * #w = f * (a * #v + b * #w)
[PROOF STEP]
by (simp add: v'_def w'_def ring_distribs ac_simps)
[PROOF STATE]
proof (state)
this:
w' * #v + v' * #w = f * (a * #v + b * #w)

goal (1 subgoal):
 1. w' * #v + v' * #w = f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
w' * #v + v' * #w = f * (a * #v + b * #w)

goal (1 subgoal):
 1. w' * #v + v' * #w = f
[PROOF STEP]
from avbw
[PROOF STATE]
proof (chain)
picking this:
a * #v + b * #w = 1
[PROOF STEP]
have "(#(a * #v + b * #w) :: 'p mod_ring poly) = 1"
[PROOF STATE]
proof (prove)
using this:
a * #v + b * #w = 1

goal (1 subgoal):
 1. #(a * #v + b * #w) = 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
#(a * #v + b * #w) = 1

goal (1 subgoal):
 1. w' * #v + v' * #w = f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
#(a * #v + b * #w) = 1
[PROOF STEP]
have "(a * #v + b * #w :: 'p mod_ring poly) = 1"
[PROOF STATE]
proof (prove)
using this:
#(a * #v + b * #w) = 1

goal (1 subgoal):
 1. a * #v + b * #w = 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a * #v + b * #w = 1

goal (1 subgoal):
 1. w' * #v + v' * #w = f
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
w' * #v + v' * #w = f * 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
w' * #v + v' * #w = f * 1

goal (1 subgoal):
 1. w' * #v + v' * #w = f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
w' * #v + v' * #w = f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma degv': "degree v' < degree v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree v' < degree v
[PROOF STEP]
by (unfold v'_def t_def, rule someI_ex, rule t_ex)


[STATEMENT]
lemma degqf[simp]: "degree (smult (of_nat CARD('q)) (#f :: 'pq mod_ring poly)) = degree (#f :: 'pq mod_ring poly)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (Polynomial.smult (of_nat CARD('q)) (#f)) = degree (#f)
[PROOF STEP]
proof (intro degree_smult_eqI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. degree (#f) \<noteq> 0 \<Longrightarrow> of_nat CARD('q) * lead_coeff (#f) \<noteq> 0
[PROOF STEP]
assume "degree (#f :: 'pq mod_ring poly) \<noteq> 0"
[PROOF STATE]
proof (state)
this:
degree (#f) \<noteq> 0

goal (1 subgoal):
 1. degree (#f) \<noteq> 0 \<Longrightarrow> of_nat CARD('q) * lead_coeff (#f) \<noteq> 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
degree (#f) \<noteq> 0
[PROOF STEP]
have f0: "degree f \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
degree (#f) \<noteq> 0

goal (1 subgoal):
 1. degree f \<noteq> 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
degree f \<noteq> 0

goal (1 subgoal):
 1. degree (#f) \<noteq> 0 \<Longrightarrow> of_nat CARD('q) * lead_coeff (#f) \<noteq> 0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
degree f \<noteq> 0

goal (1 subgoal):
 1. degree (#f) \<noteq> 0 \<Longrightarrow> of_nat CARD('q) * lead_coeff (#f) \<noteq> 0
[PROOF STEP]
define l where "l \<equiv> lead_coeff f"
[PROOF STATE]
proof (state)
this:
l \<equiv> lead_coeff f

goal (1 subgoal):
 1. degree (#f) \<noteq> 0 \<Longrightarrow> of_nat CARD('q) * lead_coeff (#f) \<noteq> 0
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
degree f \<noteq> 0
l \<equiv> lead_coeff f
[PROOF STEP]
have l0: "l \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
degree f \<noteq> 0
l \<equiv> lead_coeff f

goal (1 subgoal):
 1. l \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l \<noteq> 0

goal (1 subgoal):
 1. degree (#f) \<noteq> 0 \<Longrightarrow> of_nat CARD('q) * lead_coeff (#f) \<noteq> 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l \<noteq> 0
[PROOF STEP]
show "of_nat CARD('q) * lead_coeff (#f::'pq mod_ring poly) \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
l \<noteq> 0

goal (1 subgoal):
 1. of_nat CARD('q) * lead_coeff (#f) \<noteq> 0
[PROOF STEP]
apply (unfold rebase_p_to_pq.lead_coeff_rebase_poly, fold l_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>l \<noteq> 0; l \<noteq> 0\<rbrakk> \<Longrightarrow> of_nat CARD('q) * @l \<noteq> 0
[PROOF STEP]
apply (transfer)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>l \<in> {0..<int CARD('p)}; l \<noteq> 0; l \<noteq> 0\<rbrakk> \<Longrightarrow> int CARD('q) mod int CARD('pq) * (l mod int CARD('pq)) mod int CARD('pq) \<noteq> 0
[PROOF STEP]
using q1
[PROOF STATE]
proof (prove)
using this:
1 < int q

goal (1 subgoal):
 1. \<And>l. \<lbrakk>l \<in> {0..<int CARD('p)}; l \<noteq> 0; l \<noteq> 0\<rbrakk> \<Longrightarrow> int CARD('q) mod int CARD('pq) * (l mod int CARD('pq)) mod int CARD('pq) \<noteq> 0
[PROOF STEP]
by (simp add: pq mod_mod_cancel)
[PROOF STATE]
proof (state)
this:
of_nat CARD('q) * lead_coeff (#f) \<noteq> 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma degw': "degree w' \<le> degree w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree w' \<le> degree w
[PROOF STEP]
proof(rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> degree w' \<le> degree w \<Longrightarrow> False
[PROOF STEP]
let ?f = "#f :: 'pq mod_ring poly"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> degree w' \<le> degree w \<Longrightarrow> False
[PROOF STEP]
let ?qf = "smult (of_nat q) (#f) :: 'pq mod_ring poly"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> degree w' \<le> degree w \<Longrightarrow> False
[PROOF STEP]
have "degree (#w::'p mod_ring poly) \<le> degree w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (#w) \<le> degree w
[PROOF STEP]
by (rule degree_rebase_poly_le)
[PROOF STATE]
proof (state)
this:
degree (#w) \<le> degree w

goal (1 subgoal):
 1. \<not> degree w' \<le> degree w \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
degree (#w) \<le> degree w

goal (1 subgoal):
 1. \<not> degree w' \<le> degree w \<Longrightarrow> False
[PROOF STEP]
assume "\<not> degree w' \<le> degree w"
[PROOF STATE]
proof (state)
this:
\<not> degree w' \<le> degree w

goal (1 subgoal):
 1. \<not> degree w' \<le> degree w \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> degree w' \<le> degree w
[PROOF STEP]
have 1: "degree w < degree w'"
[PROOF STATE]
proof (prove)
using this:
\<not> degree w' \<le> degree w

goal (1 subgoal):
 1. degree w < degree w'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
degree w < degree w'

goal (1 subgoal):
 1. \<not> degree w' \<le> degree w \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
degree (#w) < degree w'
[PROOF STEP]
have 2: "degree (#w :: 'p mod_ring poly) < degree w'"
[PROOF STATE]
proof (prove)
using this:
degree (#w) < degree w'

goal (1 subgoal):
 1. degree (#w) < degree w'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
degree (#w) < degree w'

goal (1 subgoal):
 1. \<not> degree w' \<le> degree w \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
degree (#w) < degree w'
[PROOF STEP]
have w'0: "w' \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
degree (#w) < degree w'

goal (1 subgoal):
 1. w' \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
w' \<noteq> 0

goal (1 subgoal):
 1. \<not> degree w' \<le> degree w \<Longrightarrow> False
[PROOF STEP]
have 3: "degree (#v * w') = degree (#v :: 'p mod_ring poly) + degree w'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (#v * w') = degree (#v) + degree w'
[PROOF STEP]
using monic_v[unfolded]
[PROOF STATE]
proof (prove)
using this:
monic v

goal (1 subgoal):
 1. degree (#v * w') = degree (#v) + degree w'
[PROOF STEP]
by (intro degree_monic_mult[OF _ w'0], auto simp: deg_v)
[PROOF STATE]
proof (state)
this:
degree (#v * w') = degree (#v) + degree w'

goal (1 subgoal):
 1. \<not> degree w' \<le> degree w \<Longrightarrow> False
[PROOF STEP]
have "degree f \<le> degree u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree f \<le> degree u
[PROOF STEP]
proof(rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> degree f \<le> degree u \<Longrightarrow> False
[PROOF STEP]
assume "\<not>?thesis"
[PROOF STATE]
proof (state)
this:
\<not> degree f \<le> degree u

goal (1 subgoal):
 1. \<not> degree f \<le> degree u \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> degree f \<le> degree u
[PROOF STEP]
have *: "degree u < degree f"
[PROOF STATE]
proof (prove)
using this:
\<not> degree f \<le> degree u

goal (1 subgoal):
 1. degree u < degree f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
degree u < degree f

goal (1 subgoal):
 1. \<not> degree f \<le> degree u \<Longrightarrow> False
[PROOF STEP]
with degu
[PROOF STATE]
proof (chain)
picking this:
degree u = degree v + degree w
degree u < degree f
[PROOF STEP]
have 1: "degree v + degree w < degree f"
[PROOF STATE]
proof (prove)
using this:
degree u = degree v + degree w
degree u < degree f

goal (1 subgoal):
 1. degree v + degree w < degree f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
degree v + degree w < degree f

goal (1 subgoal):
 1. \<not> degree f \<le> degree u \<Longrightarrow> False
[PROOF STEP]
define lcf where "lcf \<equiv> lead_coeff f"
[PROOF STATE]
proof (state)
this:
lcf \<equiv> lead_coeff f

goal (1 subgoal):
 1. \<not> degree f \<le> degree u \<Longrightarrow> False
[PROOF STEP]
with 1
[PROOF STATE]
proof (chain)
picking this:
degree v + degree w < degree f
lcf \<equiv> lead_coeff f
[PROOF STEP]
have lcf0: "lcf \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
degree v + degree w < degree f
lcf \<equiv> lead_coeff f

goal (1 subgoal):
 1. lcf \<noteq> 0
[PROOF STEP]
by (unfold, auto)
[PROOF STATE]
proof (state)
this:
lcf \<noteq> 0

goal (1 subgoal):
 1. \<not> degree f \<le> degree u \<Longrightarrow> False
[PROOF STEP]
have "degree f = degree ?qf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree f = degree (Polynomial.smult (of_nat q) (#f))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
degree f = degree (Polynomial.smult (of_nat q) (#f))

goal (1 subgoal):
 1. \<not> degree f \<le> degree u \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
degree f = degree (Polynomial.smult (of_nat q) (#f))

goal (1 subgoal):
 1. \<not> degree f \<le> degree u \<Longrightarrow> False
[PROOF STEP]
have "... = degree (#v * #w + ?qf)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (Polynomial.smult (of_nat q) (#f)) = degree (#v * #w + Polynomial.smult (of_nat q) (#f))
[PROOF STEP]
proof(rule sym, rule degree_add_eq_right)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. degree (#v * #w) < degree (Polynomial.smult (of_nat q) (#f))
[PROOF STEP]
from 1 degree_mult_le[of "#v::'pq mod_ring poly" "#w"]
[PROOF STATE]
proof (chain)
picking this:
degree v + degree w < degree f
degree (#v * #w) \<le> degree (#v) + degree (#w)
[PROOF STEP]
show "degree (#v * #w :: 'pq mod_ring poly) < degree ?qf"
[PROOF STATE]
proof (prove)
using this:
degree v + degree w < degree f
degree (#v * #w) \<le> degree (#v) + degree (#w)

goal (1 subgoal):
 1. degree (#v * #w) < degree (Polynomial.smult (of_nat q) (#f))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
degree (#v * #w) < degree (Polynomial.smult (of_nat q) (#f))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
degree (Polynomial.smult (of_nat q) (#f)) = degree (#v * #w + Polynomial.smult (of_nat q) (#f))

goal (1 subgoal):
 1. \<not> degree f \<le> degree u \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
degree (Polynomial.smult (of_nat q) (#f)) = degree (#v * #w + Polynomial.smult (of_nat q) (#f))

goal (1 subgoal):
 1. \<not> degree f \<le> degree u \<Longrightarrow> False
[PROOF STEP]
have "... < degree f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (#v * #w + Polynomial.smult (of_nat q) (#f)) < degree f
[PROOF STEP]
using * u
[PROOF STATE]
proof (prove)
using this:
degree u < degree f
u = #v * #w + Polynomial.smult (of_nat q) (#f)

goal (1 subgoal):
 1. degree (#v * #w + Polynomial.smult (of_nat q) (#f)) < degree f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
degree (#v * #w + Polynomial.smult (of_nat q) (#f)) < degree f

goal (1 subgoal):
 1. \<not> degree f \<le> degree u \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
degree f < degree f
[PROOF STEP]
show "False"
[PROOF STATE]
proof (prove)
using this:
degree f < degree f

goal (1 subgoal):
 1. False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
degree f \<le> degree u

goal (1 subgoal):
 1. \<not> degree w' \<le> degree w \<Longrightarrow> False
[PROOF STEP]
with degu
[PROOF STATE]
proof (chain)
picking this:
degree u = degree v + degree w
degree f \<le> degree u
[PROOF STEP]
have "degree f \<le> degree v + degree w"
[PROOF STATE]
proof (prove)
using this:
degree u = degree v + degree w
degree f \<le> degree u

goal (1 subgoal):
 1. degree f \<le> degree v + degree w
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
degree f \<le> degree v + degree w

goal (1 subgoal):
 1. \<not> degree w' \<le> degree w \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
degree f \<le> degree v + degree w

goal (1 subgoal):
 1. \<not> degree w' \<le> degree w \<Longrightarrow> False
[PROOF STEP]
note f[symmetric]
[PROOF STATE]
proof (state)
this:
f = w' * #v + v' * #w

goal (1 subgoal):
 1. \<not> degree w' \<le> degree w \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
degree (w' * #v + v' * #w) \<le> degree v + degree w
[PROOF STEP]
have "degree (w' * #v + v' * #w) \<le> degree v + degree w"
[PROOF STATE]
proof (prove)
using this:
degree (w' * #v + v' * #w) \<le> degree v + degree w

goal (1 subgoal):
 1. degree (w' * #v + v' * #w) \<le> degree v + degree w
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
degree (w' * #v + v' * #w) \<le> degree v + degree w

goal (1 subgoal):
 1. \<not> degree w' \<le> degree w \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
degree (w' * #v + v' * #w) \<le> degree v + degree w

goal (1 subgoal):
 1. \<not> degree w' \<le> degree w \<Longrightarrow> False
[PROOF STEP]
have "degree (w' * #v + v' * #w) = degree (w' * #v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (w' * #v + v' * #w) = degree (w' * #v)
[PROOF STEP]
proof(rule degree_add_eq_left)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. degree (v' * #w) < degree (w' * #v)
[PROOF STEP]
have "degree (v' * #w) \<le> degree v' + degree (#w :: 'p mod_ring poly)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (v' * #w) \<le> degree v' + degree (#w)
[PROOF STEP]
by(rule degree_mult_le)
[PROOF STATE]
proof (state)
this:
degree (v' * #w) \<le> degree v' + degree (#w)

goal (1 subgoal):
 1. degree (v' * #w) < degree (w' * #v)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
degree (v' * #w) \<le> degree v' + degree (#w)

goal (1 subgoal):
 1. degree (v' * #w) < degree (w' * #v)
[PROOF STEP]
have "... < degree v + degree (#w :: 'p mod_ring poly)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree v' + degree (#w) < degree v + degree (#w)
[PROOF STEP]
using degv'
[PROOF STATE]
proof (prove)
using this:
degree v' < degree v

goal (1 subgoal):
 1. degree v' + degree (#w) < degree v + degree (#w)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
degree v' + degree (#w) < degree v + degree (#w)

goal (1 subgoal):
 1. degree (v' * #w) < degree (w' * #v)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
degree v' + degree (#w) < degree v + degree (#w)

goal (1 subgoal):
 1. degree (v' * #w) < degree (w' * #v)
[PROOF STEP]
have "... < degree (#v :: 'p mod_ring poly) + degree w'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree v + degree (#w) < degree (#v) + degree w'
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
degree (#w) < degree w'

goal (1 subgoal):
 1. degree v + degree (#w) < degree (#v) + degree w'
[PROOF STEP]
by (auto simp: deg_v)
[PROOF STATE]
proof (state)
this:
degree v + degree (#w) < degree (#v) + degree w'

goal (1 subgoal):
 1. degree (v' * #w) < degree (w' * #v)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
degree v + degree (#w) < degree (#v) + degree w'

goal (1 subgoal):
 1. degree (v' * #w) < degree (w' * #v)
[PROOF STEP]
have "... = degree (#v * w')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (#v) + degree w' = degree (#v * w')
[PROOF STEP]
using 3
[PROOF STATE]
proof (prove)
using this:
degree (#v * w') = degree (#v) + degree w'

goal (1 subgoal):
 1. degree (#v) + degree w' = degree (#v * w')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
degree (#v) + degree w' = degree (#v * w')

goal (1 subgoal):
 1. degree (v' * #w) < degree (w' * #v)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
degree (v' * #w) < degree (#v * w')
[PROOF STEP]
show "degree (v' * #w) < degree (w' * #v)"
[PROOF STATE]
proof (prove)
using this:
degree (v' * #w) < degree (#v * w')

goal (1 subgoal):
 1. degree (v' * #w) < degree (w' * #v)
[PROOF STEP]
by (auto simp: ac_simps)
[PROOF STATE]
proof (state)
this:
degree (v' * #w) < degree (w' * #v)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
degree (w' * #v + v' * #w) = degree (w' * #v)

goal (1 subgoal):
 1. \<not> degree w' \<le> degree w \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
degree (w' * #v + v' * #w) \<le> degree v + degree w
degree (w' * #v + v' * #w) = degree (w' * #v)
[PROOF STEP]
have "degree (w' * #v) \<le> degree v + degree w"
[PROOF STATE]
proof (prove)
using this:
degree (w' * #v + v' * #w) \<le> degree v + degree w
degree (w' * #v + v' * #w) = degree (w' * #v)

goal (1 subgoal):
 1. degree (w' * #v) \<le> degree v + degree w
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
degree (w' * #v) \<le> degree v + degree w

goal (1 subgoal):
 1. \<not> degree w' \<le> degree w \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
degree (w' * #v) \<le> degree v + degree w

goal (1 subgoal):
 1. \<not> degree w' \<le> degree w \<Longrightarrow> False
[PROOF STEP]
from 3
[PROOF STATE]
proof (chain)
picking this:
degree (#v * w') = degree (#v) + degree w'
[PROOF STEP]
have "degree (w' * #v) = degree w' + degree v"
[PROOF STATE]
proof (prove)
using this:
degree (#v * w') = degree (#v) + degree w'

goal (1 subgoal):
 1. degree (w' * #v) = degree w' + degree v
[PROOF STEP]
by (auto simp: ac_simps deg_v)
[PROOF STATE]
proof (state)
this:
degree (w' * #v) = degree w' + degree v

goal (1 subgoal):
 1. \<not> degree w' \<le> degree w \<Longrightarrow> False
[PROOF STEP]
with 1
[PROOF STATE]
proof (chain)
picking this:
degree w < degree w'
degree (w' * #v) = degree w' + degree v
[PROOF STEP]
have "degree w + degree v < degree (w' * #v)"
[PROOF STATE]
proof (prove)
using this:
degree w < degree w'
degree (w' * #v) = degree w' + degree v

goal (1 subgoal):
 1. degree w + degree v < degree (w' * #v)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
degree w + degree v < degree (w' * #v)

goal (1 subgoal):
 1. \<not> degree w' \<le> degree w \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
degree (w' * #v) \<le> degree v + degree w
degree w + degree v < degree (w' * #v)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
degree (w' * #v) \<le> degree v + degree w
degree w + degree v < degree (w' * #v)

goal (1 subgoal):
 1. False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vV: "v = #V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v = #(#v + Polynomial.smult (of_nat q) (#v'))
[PROOF STEP]
by (auto simp: v'_def hom_distribs)


[STATEMENT]
lemma wW: "w = #W"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w = #(#w + Polynomial.smult (of_nat q) (#w'))
[PROOF STEP]
by (auto simp: w'_def hom_distribs)


[STATEMENT]
lemma uVW: "u = V * W"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u = (#v + Polynomial.smult (of_nat q) (#v')) * (#w + Polynomial.smult (of_nat q) (#w'))
[PROOF STEP]
by (subst u, fold f, simp add: ring_distribs add.left_cancel smult_add_right[symmetric] hom_distribs)


[STATEMENT]
lemma degV: "degree V = degree v"
  and lcV: "lead_coeff V = @lead_coeff v"
  and degW: "degree W = degree w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (#v + Polynomial.smult (of_nat q) (#v')) = degree v &&& lead_coeff (#v + Polynomial.smult (of_nat q) (#v')) = @lead_coeff v &&& degree (#w + Polynomial.smult (of_nat q) (#w')) = degree w
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. degree (#v + Polynomial.smult (of_nat q) (#v')) = degree v
 2. lead_coeff (#v + Polynomial.smult (of_nat q) (#v')) = @lead_coeff v
 3. degree (#w + Polynomial.smult (of_nat q) (#w')) = degree w
[PROOF STEP]
from p1 q1
[PROOF STATE]
proof (chain)
picking this:
1 < int p
1 < int q
[PROOF STEP]
have "int p < int p * int q"
[PROOF STATE]
proof (prove)
using this:
1 < int p
1 < int q

goal (1 subgoal):
 1. int p < int p * int q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
int p < int p * int q

goal (3 subgoals):
 1. degree (#v + Polynomial.smult (of_nat q) (#v')) = degree v
 2. lead_coeff (#v + Polynomial.smult (of_nat q) (#v')) = @lead_coeff v
 3. degree (#w + Polynomial.smult (of_nat q) (#w')) = degree w
[PROOF STEP]
from less_trans[OF _ this]
[PROOF STATE]
proof (chain)
picking this:
?x < int p \<Longrightarrow> ?x < int p * int q
[PROOF STEP]
have 1: "l < int p \<Longrightarrow> l < int p * int q" for l
[PROOF STATE]
proof (prove)
using this:
?x < int p \<Longrightarrow> ?x < int p * int q

goal (1 subgoal):
 1. l < int p \<Longrightarrow> l < int p * int q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?l < int p \<Longrightarrow> ?l < int p * int q

goal (3 subgoals):
 1. degree (#v + Polynomial.smult (of_nat q) (#v')) = degree v
 2. lead_coeff (#v + Polynomial.smult (of_nat q) (#v')) = @lead_coeff v
 3. degree (#w + Polynomial.smult (of_nat q) (#w')) = degree w
[PROOF STEP]
have "degree qv' = degree (#v' :: 'pq mod_ring poly)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (Polynomial.smult (of_nat q) (#v')) = degree (#v')
[PROOF STEP]
proof (rule degree_smult_eqI, safe, unfold rebase_p_to_pq.degree_rebase_poly_eq)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>0 < degree v'; of_nat q * poly.coeff (#v') (degree v') = 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
define l where "l \<equiv> lead_coeff v'"
[PROOF STATE]
proof (state)
this:
l \<equiv> lead_coeff v'

goal (1 subgoal):
 1. \<lbrakk>0 < degree v'; of_nat q * poly.coeff (#v') (degree v') = 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "degree v' > 0"
[PROOF STATE]
proof (state)
this:
0 < degree v'

goal (1 subgoal):
 1. \<lbrakk>0 < degree v'; of_nat q * poly.coeff (#v') (degree v') = 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < degree v'
[PROOF STEP]
have "lead_coeff v' \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
0 < degree v'

goal (1 subgoal):
 1. lead_coeff v' \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lead_coeff v' \<noteq> 0

goal (1 subgoal):
 1. \<lbrakk>0 < degree v'; of_nat q * poly.coeff (#v') (degree v') = 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
lead_coeff v' \<noteq> 0
[PROOF STEP]
have "(@l :: 'pq mod_ring) \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
lead_coeff v' \<noteq> 0

goal (1 subgoal):
 1. @l \<noteq> 0
[PROOF STEP]
by (simp add: l_def)
[PROOF STATE]
proof (state)
this:
@l \<noteq> 0

goal (1 subgoal):
 1. \<lbrakk>0 < degree v'; of_nat q * poly.coeff (#v') (degree v') = 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
@l \<noteq> 0
[PROOF STEP]
have "(of_nat q * @l :: 'pq mod_ring) \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
@l \<noteq> 0

goal (1 subgoal):
 1. of_nat q * @l \<noteq> 0
[PROOF STEP]
apply (transfer fixing:q_ty)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>l \<in> {0..<int CARD('p)}; l mod int CARD('pq) \<noteq> 0\<rbrakk> \<Longrightarrow> int q mod int CARD('pq) * (l mod int CARD('pq)) mod int CARD('pq) \<noteq> 0
[PROOF STEP]
using p_dvd_q p1 q1 1
[PROOF STATE]
proof (prove)
using this:
CARD('p) dvd CARD('q)
1 < int p
1 < int q
?l < int p \<Longrightarrow> ?l < int p * int q

goal (1 subgoal):
 1. \<And>l. \<lbrakk>l \<in> {0..<int CARD('p)}; l mod int CARD('pq) \<noteq> 0\<rbrakk> \<Longrightarrow> int q mod int CARD('pq) * (l mod int CARD('pq)) mod int CARD('pq) \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
of_nat q * @l \<noteq> 0

goal (1 subgoal):
 1. \<lbrakk>0 < degree v'; of_nat q * poly.coeff (#v') (degree v') = 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
of_nat q * @l \<noteq> 0

goal (1 subgoal):
 1. \<lbrakk>0 < degree v'; of_nat q * poly.coeff (#v') (degree v') = 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume " of_nat q * coeff (#v') (degree v') = (0 :: 'pq mod_ring)"
[PROOF STATE]
proof (state)
this:
of_nat q * poly.coeff (#v') (degree v') = 0

goal (1 subgoal):
 1. \<lbrakk>0 < degree v'; of_nat q * poly.coeff (#v') (degree v') = 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
of_nat q * @l \<noteq> 0
of_nat q * poly.coeff (#v') (degree v') = 0
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
of_nat q * @l \<noteq> 0
of_nat q * poly.coeff (#v') (degree v') = 0

goal (1 subgoal):
 1. False
[PROOF STEP]
by (auto simp: l_def)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
degree (Polynomial.smult (of_nat q) (#v')) = degree (#v')

goal (3 subgoals):
 1. degree (#v + Polynomial.smult (of_nat q) (#v')) = degree v
 2. lead_coeff (#v + Polynomial.smult (of_nat q) (#v')) = @lead_coeff v
 3. degree (#w + Polynomial.smult (of_nat q) (#w')) = degree w
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
degree (Polynomial.smult (of_nat q) (#v')) = degree (#v')

goal (3 subgoals):
 1. degree (#v + Polynomial.smult (of_nat q) (#v')) = degree v
 2. lead_coeff (#v + Polynomial.smult (of_nat q) (#v')) = @lead_coeff v
 3. degree (#w + Polynomial.smult (of_nat q) (#w')) = degree w
[PROOF STEP]
from degv'
[PROOF STATE]
proof (chain)
picking this:
degree v' < degree v
[PROOF STEP]
have "... < degree (#v::'pq mod_ring poly)"
[PROOF STATE]
proof (prove)
using this:
degree v' < degree v

goal (1 subgoal):
 1. degree (#v') < degree (#v)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
degree (#v') < degree (#v)

goal (3 subgoals):
 1. degree (#v + Polynomial.smult (of_nat q) (#v')) = degree v
 2. lead_coeff (#v + Polynomial.smult (of_nat q) (#v')) = @lead_coeff v
 3. degree (#w + Polynomial.smult (of_nat q) (#w')) = degree w
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
degree (Polynomial.smult (of_nat q) (#v')) < degree (#v)
[PROOF STEP]
have *: "degree qv' < degree (#v :: 'pq mod_ring poly)"
[PROOF STATE]
proof (prove)
using this:
degree (Polynomial.smult (of_nat q) (#v')) < degree (#v)

goal (1 subgoal):
 1. degree (Polynomial.smult (of_nat q) (#v')) < degree (#v)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
degree (Polynomial.smult (of_nat q) (#v')) < degree (#v)

goal (3 subgoals):
 1. degree (#v + Polynomial.smult (of_nat q) (#v')) = degree v
 2. lead_coeff (#v + Polynomial.smult (of_nat q) (#v')) = @lead_coeff v
 3. degree (#w + Polynomial.smult (of_nat q) (#w')) = degree w
[PROOF STEP]
from degree_add_eq_left[OF *]
[PROOF STATE]
proof (chain)
picking this:
degree (#v + Polynomial.smult (of_nat q) (#v')) = degree (#v)
[PROOF STEP]
show **: "degree V = degree v"
[PROOF STATE]
proof (prove)
using this:
degree (#v + Polynomial.smult (of_nat q) (#v')) = degree (#v)

goal (1 subgoal):
 1. degree (#v + Polynomial.smult (of_nat q) (#v')) = degree v
[PROOF STEP]
by (simp add: v'_def)
[PROOF STATE]
proof (state)
this:
degree (#v + Polynomial.smult (of_nat q) (#v')) = degree v

goal (2 subgoals):
 1. lead_coeff (#v + Polynomial.smult (of_nat q) (#v')) = @lead_coeff v
 2. degree (#w + Polynomial.smult (of_nat q) (#w')) = degree w
[PROOF STEP]
from *
[PROOF STATE]
proof (chain)
picking this:
degree (Polynomial.smult (of_nat q) (#v')) < degree (#v)
[PROOF STEP]
have "coeff qv' (degree v) = 0"
[PROOF STATE]
proof (prove)
using this:
degree (Polynomial.smult (of_nat q) (#v')) < degree (#v)

goal (1 subgoal):
 1. poly.coeff (Polynomial.smult (of_nat q) (#v')) (degree v) = 0
[PROOF STEP]
by (intro coeff_eq_0, auto)
[PROOF STATE]
proof (state)
this:
poly.coeff (Polynomial.smult (of_nat q) (#v')) (degree v) = 0

goal (2 subgoals):
 1. lead_coeff (#v + Polynomial.smult (of_nat q) (#v')) = @lead_coeff v
 2. degree (#w + Polynomial.smult (of_nat q) (#w')) = degree w
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
poly.coeff (Polynomial.smult (of_nat q) (#v')) (degree v) = 0
[PROOF STEP]
show "lead_coeff V = @lead_coeff v"
[PROOF STATE]
proof (prove)
using this:
poly.coeff (Polynomial.smult (of_nat q) (#v')) (degree v) = 0

goal (1 subgoal):
 1. lead_coeff (#v + Polynomial.smult (of_nat q) (#v')) = @lead_coeff v
[PROOF STEP]
by (unfold **, auto simp: v'_def)
[PROOF STATE]
proof (state)
this:
lead_coeff (#v + Polynomial.smult (of_nat q) (#v')) = @lead_coeff v

goal (1 subgoal):
 1. degree (#w + Polynomial.smult (of_nat q) (#w')) = degree w
[PROOF STEP]
with u0 uVW
[PROOF STATE]
proof (chain)
picking this:
u \<noteq> 0
u = (#v + Polynomial.smult (of_nat q) (#v')) * (#w + Polynomial.smult (of_nat q) (#w'))
lead_coeff (#v + Polynomial.smult (of_nat q) (#v')) = @lead_coeff v
[PROOF STEP]
have "degree (V * W) = degree V + degree W"
[PROOF STATE]
proof (prove)
using this:
u \<noteq> 0
u = (#v + Polynomial.smult (of_nat q) (#v')) * (#w + Polynomial.smult (of_nat q) (#w'))
lead_coeff (#v + Polynomial.smult (of_nat q) (#v')) = @lead_coeff v

goal (1 subgoal):
 1. degree ((#v + Polynomial.smult (of_nat q) (#v')) * (#w + Polynomial.smult (of_nat q) (#w'))) = degree (#v + Polynomial.smult (of_nat q) (#v')) + degree (#w + Polynomial.smult (of_nat q) (#w'))
[PROOF STEP]
by (intro degree_mult_eq_left_unit, auto simp: monic_v)
[PROOF STATE]
proof (state)
this:
degree ((#v + Polynomial.smult (of_nat q) (#v')) * (#w + Polynomial.smult (of_nat q) (#w'))) = degree (#v + Polynomial.smult (of_nat q) (#v')) + degree (#w + Polynomial.smult (of_nat q) (#w'))

goal (1 subgoal):
 1. degree (#w + Polynomial.smult (of_nat q) (#w')) = degree w
[PROOF STEP]
from this[folded uVW, unfolded degu **]
[PROOF STATE]
proof (chain)
picking this:
degree v + degree w = degree v + degree (#w + Polynomial.smult (of_nat q) (#w'))
[PROOF STEP]
show "degree W = degree w"
[PROOF STATE]
proof (prove)
using this:
degree v + degree w = degree v + degree (#w + Polynomial.smult (of_nat q) (#w'))

goal (1 subgoal):
 1. degree (#w + Polynomial.smult (of_nat q) (#w')) = degree w
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
degree (#w + Polynomial.smult (of_nat q) (#w')) = degree w

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma coprime_preserves: "coprime (#V :: 'p mod_ring poly) (#W)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. comm_monoid_mult_class.coprime (#(#v + Polynomial.smult (of_nat q) (#v'))) (#(#w + Polynomial.smult (of_nat q) (#w')))
[PROOF STEP]
apply (intro coprimeI,simp add: rebase_q_to_p.of_nat_CARD_eq_0[simplified] hom_distribs)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r. \<lbrakk>r dvd #v; r dvd #w\<rbrakk> \<Longrightarrow> r \<noteq> 0 \<and> degree r = 0
[PROOF STEP]
using coprime
[PROOF STATE]
proof (prove)
using this:
comm_monoid_mult_class.coprime (#v) (#w)

goal (1 subgoal):
 1. \<And>r. \<lbrakk>r dvd #v; r dvd #w\<rbrakk> \<Longrightarrow> r \<noteq> 0 \<and> degree r = 0
[PROOF STEP]
by (elim coprimeE, auto)


[STATEMENT]
lemma pre_unique:
  assumes f2: "w'' * #v + v'' * #w = f"
      and degv'': "degree v'' < degree v"
  shows "v'' = v' \<and> w'' = w'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v'' = v' \<and> w'' = w'
[PROOF STEP]
proof(intro conjI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. v'' = v'
 2. w'' = w'
[PROOF STEP]
from f f2
[PROOF STATE]
proof (chain)
picking this:
w' * #v + v' * #w = f
w'' * #v + v'' * #w = f
[PROOF STEP]
have "w' * #v + v' * #w = w'' * #v + v'' * #w"
[PROOF STATE]
proof (prove)
using this:
w' * #v + v' * #w = f
w'' * #v + v'' * #w = f

goal (1 subgoal):
 1. w' * #v + v' * #w = w'' * #v + v'' * #w
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
w' * #v + v' * #w = w'' * #v + v'' * #w

goal (2 subgoals):
 1. v'' = v'
 2. w'' = w'
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
w' * #v + v' * #w = w'' * #v + v'' * #w

goal (2 subgoals):
 1. v'' = v'
 2. w'' = w'
[PROOF STEP]
have "... - w'' * #v = v'' * #w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w'' * #v + v'' * #w - w'' * #v = v'' * #w
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
w'' * #v + v'' * #w - w'' * #v = v'' * #w

goal (2 subgoals):
 1. v'' = v'
 2. w'' = w'
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
w'' * #v + v'' * #w - w'' * #v = v'' * #w

goal (2 subgoals):
 1. v'' = v'
 2. w'' = w'
[PROOF STEP]
have "... - v' * #w = (v''- v') * #w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v'' * #w - v' * #w = (v'' - v') * #w
[PROOF STEP]
by (auto simp: left_diff_distrib)
[PROOF STATE]
proof (state)
this:
v'' * #w - v' * #w = (v'' - v') * #w

goal (2 subgoals):
 1. v'' = v'
 2. w'' = w'
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
w' * #v + v' * #w - w'' * #v - v' * #w = (v'' - v') * #w
[PROOF STEP]
have *: "(w' - w'') * #v = (v''- v') * #w"
[PROOF STATE]
proof (prove)
using this:
w' * #v + v' * #w - w'' * #v - v' * #w = (v'' - v') * #w

goal (1 subgoal):
 1. (w' - w'') * #v = (v'' - v') * #w
[PROOF STEP]
by (auto simp: left_diff_distrib)
[PROOF STATE]
proof (state)
this:
(w' - w'') * #v = (v'' - v') * #w

goal (2 subgoals):
 1. v'' = v'
 2. w'' = w'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(w' - w'') * #v = (v'' - v') * #w
[PROOF STEP]
have "#v dvd (v'' - v') * #w"
[PROOF STATE]
proof (prove)
using this:
(w' - w'') * #v = (v'' - v') * #w

goal (1 subgoal):
 1. #v dvd (v'' - v') * #w
[PROOF STEP]
by (auto intro: dvdI[of _ _ "w' - w''"] simp: ac_simps)
[PROOF STATE]
proof (state)
this:
#v dvd (v'' - v') * #w

goal (2 subgoals):
 1. v'' = v'
 2. w'' = w'
[PROOF STEP]
with coprime
[PROOF STATE]
proof (chain)
picking this:
comm_monoid_mult_class.coprime (#v) (#w)
#v dvd (v'' - v') * #w
[PROOF STEP]
have "#v dvd v'' - v'"
[PROOF STATE]
proof (prove)
using this:
comm_monoid_mult_class.coprime (#v) (#w)
#v dvd (v'' - v') * #w

goal (1 subgoal):
 1. #v dvd v'' - v'
[PROOF STEP]
by (simp add: coprime_dvd_mult_left_iff)
[PROOF STATE]
proof (state)
this:
#v dvd v'' - v'

goal (2 subgoals):
 1. v'' = v'
 2. w'' = w'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
#v dvd v'' - v'

goal (2 subgoals):
 1. v'' = v'
 2. w'' = w'
[PROOF STEP]
have "degree (v'' - v') < degree v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (v'' - v') < degree v
[PROOF STEP]
by (rule degree_diff_less[OF degv'' degv'])
[PROOF STATE]
proof (state)
this:
degree (v'' - v') < degree v

goal (2 subgoals):
 1. v'' = v'
 2. w'' = w'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
#v dvd v'' - v'
degree (v'' - v') < degree v
[PROOF STEP]
have "v'' - v' = 0"
[PROOF STATE]
proof (prove)
using this:
#v dvd v'' - v'
degree (v'' - v') < degree v

goal (1 subgoal):
 1. v'' - v' = 0
[PROOF STEP]
by (metis deg_v degree_0 gr_implies_not_zero poly_divides_conv0)
[PROOF STATE]
proof (state)
this:
v'' - v' = 0

goal (2 subgoals):
 1. v'' = v'
 2. w'' = w'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v'' - v' = 0
[PROOF STEP]
show "v'' = v'"
[PROOF STATE]
proof (prove)
using this:
v'' - v' = 0

goal (1 subgoal):
 1. v'' = v'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v'' = v'

goal (1 subgoal):
 1. w'' = w'
[PROOF STEP]
with *
[PROOF STATE]
proof (chain)
picking this:
(w' - w'') * #v = (v'' - v') * #w
v'' = v'
[PROOF STEP]
have "(w' - w'') * #v = 0"
[PROOF STATE]
proof (prove)
using this:
(w' - w'') * #v = (v'' - v') * #w
v'' = v'

goal (1 subgoal):
 1. (w' - w'') * #v = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(w' - w'') * #v = 0

goal (1 subgoal):
 1. w'' = w'
[PROOF STEP]
with bv
[PROOF STATE]
proof (chain)
picking this:
degree b < degree v
(w' - w'') * #v = 0
[PROOF STEP]
have "w' - w'' = 0"
[PROOF STATE]
proof (prove)
using this:
degree b < degree v
(w' - w'') * #v = 0

goal (1 subgoal):
 1. w' - w'' = 0
[PROOF STEP]
by (metis deg_v degree_0 gr_implies_not_zero mult_eq_0_iff)
[PROOF STATE]
proof (state)
this:
w' - w'' = 0

goal (1 subgoal):
 1. w'' = w'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
w' - w'' = 0
[PROOF STEP]
show "w'' = w'"
[PROOF STATE]
proof (prove)
using this:
w' - w'' = 0

goal (1 subgoal):
 1. w'' = w'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
w'' = w'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma unique:
  assumes vV2: "v = #V2" and wW2: "w = #W2" and uVW2: "u = V2 * W2"
      and degV2: "degree V2 = degree v" and degW2: "degree W2 = degree w"
      and lc: "lead_coeff V2 = @lead_coeff v"
  shows "V2 = V" "W2 = W"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V2 = #v + Polynomial.smult (of_nat q) (#v') &&& W2 = #w + Polynomial.smult (of_nat q) (#w')
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. V2 = #v + Polynomial.smult (of_nat q) (#v')
 2. W2 = #w + Polynomial.smult (of_nat q) (#w')
[PROOF STEP]
from vV2
[PROOF STATE]
proof (chain)
picking this:
v = #V2
[PROOF STEP]
have "(#(V2 - #v) :: 'q mod_ring poly) = 0"
[PROOF STATE]
proof (prove)
using this:
v = #V2

goal (1 subgoal):
 1. #(V2 - #v) = 0
[PROOF STEP]
by (auto simp: hom_distribs)
[PROOF STATE]
proof (state)
this:
#(V2 - #v) = 0

goal (2 subgoals):
 1. V2 = #v + Polynomial.smult (of_nat q) (#v')
 2. W2 = #w + Polynomial.smult (of_nat q) (#w')
[PROOF STEP]
from rebase_pq_to_q.rebase_poly_eq_0_imp_ex_smult[OF this]
[PROOF STATE]
proof (chain)
picking this:
\<exists>p'. (V2 - #v = 0) = (p' = 0) \<and> degree p' \<le> degree (V2 - #v) \<and> V2 - #v = Polynomial.smult (of_nat CARD('q)) (#p')
[PROOF STEP]
obtain v'' :: "'p mod_ring poly"
  where deg: "degree v'' \<le> degree (V2 - #v)"
    and v'': "V2 - #v = smult (of_nat CARD('q)) (#v'')"
[PROOF STATE]
proof (prove)
using this:
\<exists>p'. (V2 - #v = 0) = (p' = 0) \<and> degree p' \<le> degree (V2 - #v) \<and> V2 - #v = Polynomial.smult (of_nat CARD('q)) (#p')

goal (1 subgoal):
 1. (\<And>v''. \<lbrakk>degree v'' \<le> degree (V2 - #v); V2 - #v = Polynomial.smult (of_nat CARD('q)) (#v'')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (elim exE conjE)
[PROOF STATE]
proof (state)
this:
degree v'' \<le> degree (V2 - #v)
V2 - #v = Polynomial.smult (of_nat CARD('q)) (#v'')

goal (2 subgoals):
 1. V2 = #v + Polynomial.smult (of_nat q) (#v')
 2. W2 = #w + Polynomial.smult (of_nat q) (#w')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
degree v'' \<le> degree (V2 - #v)
V2 - #v = Polynomial.smult (of_nat CARD('q)) (#v'')
[PROOF STEP]
have V2: "V2 = #v + ..."
[PROOF STATE]
proof (prove)
using this:
degree v'' \<le> degree (V2 - #v)
V2 - #v = Polynomial.smult (of_nat CARD('q)) (#v'')

goal (1 subgoal):
 1. V2 = #v + Polynomial.smult (of_nat CARD('q)) (#v'')
[PROOF STEP]
by (metis add_diff_cancel_left' diff_add_cancel)
[PROOF STATE]
proof (state)
this:
V2 = #v + Polynomial.smult (of_nat CARD('q)) (#v'')

goal (2 subgoals):
 1. V2 = #v + Polynomial.smult (of_nat q) (#v')
 2. W2 = #w + Polynomial.smult (of_nat q) (#w')
[PROOF STEP]
from lc[unfolded degV2, unfolded V2]
[PROOF STATE]
proof (chain)
picking this:
poly.coeff (#v + Polynomial.smult (of_nat CARD('q)) (#v'')) (degree v) = @lead_coeff v
[PROOF STEP]
have "of_nat q * (@coeff v'' (degree v) :: 'pq mod_ring) = of_nat q * 0"
[PROOF STATE]
proof (prove)
using this:
poly.coeff (#v + Polynomial.smult (of_nat CARD('q)) (#v'')) (degree v) = @lead_coeff v

goal (1 subgoal):
 1. of_nat q * @poly.coeff v'' (degree v) = of_nat q * 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
of_nat q * @poly.coeff v'' (degree v) = of_nat q * 0

goal (2 subgoals):
 1. V2 = #v + Polynomial.smult (of_nat q) (#v')
 2. W2 = #w + Polynomial.smult (of_nat q) (#w')
[PROOF STEP]
from this[unfolded q rebase_pq_to_p.rebase_mult_eq]
[PROOF STATE]
proof (chain)
picking this:
@@poly.coeff v'' (degree v) = @0
[PROOF STEP]
have "coeff v'' (degree v) = 0"
[PROOF STATE]
proof (prove)
using this:
@@poly.coeff v'' (degree v) = @0

goal (1 subgoal):
 1. poly.coeff v'' (degree v) = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
poly.coeff v'' (degree v) = 0

goal (2 subgoals):
 1. V2 = #v + Polynomial.smult (of_nat q) (#v')
 2. W2 = #w + Polynomial.smult (of_nat q) (#w')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
poly.coeff v'' (degree v) = 0

goal (2 subgoals):
 1. V2 = #v + Polynomial.smult (of_nat q) (#v')
 2. W2 = #w + Polynomial.smult (of_nat q) (#w')
[PROOF STEP]
have "degree v'' \<le>  degree v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree v'' \<le> degree v
[PROOF STEP]
using deg degV2
[PROOF STATE]
proof (prove)
using this:
degree v'' \<le> degree (V2 - #v)
degree V2 = degree v

goal (1 subgoal):
 1. degree v'' \<le> degree v
[PROOF STEP]
by (metis degree_diff_le le_antisym nat_le_linear rebase_q_to_pq.degree_rebase_poly_eq)
[PROOF STATE]
proof (state)
this:
degree v'' \<le> degree v

goal (2 subgoals):
 1. V2 = #v + Polynomial.smult (of_nat q) (#v')
 2. W2 = #w + Polynomial.smult (of_nat q) (#w')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
poly.coeff v'' (degree v) = 0
degree v'' \<le> degree v
[PROOF STEP]
have degv'': "degree v'' < degree v"
[PROOF STATE]
proof (prove)
using this:
poly.coeff v'' (degree v) = 0
degree v'' \<le> degree v

goal (1 subgoal):
 1. degree v'' < degree v
[PROOF STEP]
using bv eq_zero_or_degree_less
[PROOF STATE]
proof (prove)
using this:
poly.coeff v'' (degree v) = 0
degree v'' \<le> degree v
degree b < degree v
\<lbrakk>degree ?p \<le> ?n; poly.coeff ?p ?n = (0::?'a)\<rbrakk> \<Longrightarrow> ?p = 0 \<or> degree ?p < ?n

goal (1 subgoal):
 1. degree v'' < degree v
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
degree v'' < degree v

goal (2 subgoals):
 1. V2 = #v + Polynomial.smult (of_nat q) (#v')
 2. W2 = #w + Polynomial.smult (of_nat q) (#w')
[PROOF STEP]
from wW2
[PROOF STATE]
proof (chain)
picking this:
w = #W2
[PROOF STEP]
have "(#(W2 - #w) :: 'q mod_ring poly) = 0"
[PROOF STATE]
proof (prove)
using this:
w = #W2

goal (1 subgoal):
 1. #(W2 - #w) = 0
[PROOF STEP]
by (auto simp: hom_distribs)
[PROOF STATE]
proof (state)
this:
#(W2 - #w) = 0

goal (2 subgoals):
 1. V2 = #v + Polynomial.smult (of_nat q) (#v')
 2. W2 = #w + Polynomial.smult (of_nat q) (#w')
[PROOF STEP]
from rebase_pq_to_q.rebase_poly_eq_0_imp_ex_smult[OF this] pq
[PROOF STATE]
proof (chain)
picking this:
\<exists>p'. (W2 - #w = 0) = (p' = 0) \<and> degree p' \<le> degree (W2 - #w) \<and> W2 - #w = Polynomial.smult (of_nat CARD('q)) (#p')
CARD('pq) = CARD('p) * CARD('q)
[PROOF STEP]
obtain w'' :: "'p mod_ring poly" where w'': "W2 - #w = smult (of_nat q) (#w'')"
[PROOF STATE]
proof (prove)
using this:
\<exists>p'. (W2 - #w = 0) = (p' = 0) \<and> degree p' \<le> degree (W2 - #w) \<and> W2 - #w = Polynomial.smult (of_nat CARD('q)) (#p')
CARD('pq) = CARD('p) * CARD('q)

goal (1 subgoal):
 1. (\<And>w''. W2 - #w = Polynomial.smult (of_nat q) (#w'') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
W2 - #w = Polynomial.smult (of_nat q) (#w'')

goal (2 subgoals):
 1. V2 = #v + Polynomial.smult (of_nat q) (#v')
 2. W2 = #w + Polynomial.smult (of_nat q) (#w')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
W2 - #w = Polynomial.smult (of_nat q) (#w'')
[PROOF STEP]
have W2: "W2 = #w + ..."
[PROOF STATE]
proof (prove)
using this:
W2 - #w = Polynomial.smult (of_nat q) (#w'')

goal (1 subgoal):
 1. W2 = #w + Polynomial.smult (of_nat q) (#w'')
[PROOF STEP]
by (metis add_diff_cancel_left' diff_add_cancel)
[PROOF STATE]
proof (state)
this:
W2 = #w + Polynomial.smult (of_nat q) (#w'')

goal (2 subgoals):
 1. V2 = #v + Polynomial.smult (of_nat q) (#v')
 2. W2 = #w + Polynomial.smult (of_nat q) (#w')
[PROOF STEP]
have "u = #v * #w + smult (of_nat q) (#w'' * #v + #v'' * #w) + smult (of_nat (q * q)) (#v'' * #w'')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u = #v * #w + Polynomial.smult (of_nat q) (#w'' * #v + #v'' * #w) + Polynomial.smult (of_nat (q * q)) (#v'' * #w'')
[PROOF STEP]
by(simp add: uVW2 V2 W2 ring_distribs smult_add_right ac_simps)
[PROOF STATE]
proof (state)
this:
u = #v * #w + Polynomial.smult (of_nat q) (#w'' * #v + #v'' * #w) + Polynomial.smult (of_nat (q * q)) (#v'' * #w'')

goal (2 subgoals):
 1. V2 = #v + Polynomial.smult (of_nat q) (#v')
 2. W2 = #w + Polynomial.smult (of_nat q) (#w')
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
u = #v * #w + Polynomial.smult (of_nat q) (#w'' * #v + #v'' * #w) + Polynomial.smult (of_nat (q * q)) (#v'' * #w'')

goal (2 subgoals):
 1. V2 = #v + Polynomial.smult (of_nat q) (#v')
 2. W2 = #w + Polynomial.smult (of_nat q) (#w')
[PROOF STEP]
have "smult (of_nat (q * q)) (#v'' * #w'' :: 'pq mod_ring poly) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Polynomial.smult (of_nat (q * q)) (#v'' * #w'') = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Polynomial.smult (of_nat (q * q)) (#v'' * #w'') = 0

goal (2 subgoals):
 1. V2 = #v + Polynomial.smult (of_nat q) (#v')
 2. W2 = #w + Polynomial.smult (of_nat q) (#w')
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
u = #v * #w + Polynomial.smult (of_nat q) (#w'' * #v + #v'' * #w) + 0
[PROOF STEP]
have "u - #v * #w = smult (of_nat q) (#w'' * #v + #v'' * #w)"
[PROOF STATE]
proof (prove)
using this:
u = #v * #w + Polynomial.smult (of_nat q) (#w'' * #v + #v'' * #w) + 0

goal (1 subgoal):
 1. u - #v * #w = Polynomial.smult (of_nat q) (#w'' * #v + #v'' * #w)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u - #v * #w = Polynomial.smult (of_nat q) (#w'' * #v + #v'' * #w)

goal (2 subgoals):
 1. V2 = #v + Polynomial.smult (of_nat q) (#v')
 2. W2 = #w + Polynomial.smult (of_nat q) (#w')
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
u - #v * #w = Polynomial.smult (of_nat q) (#w'' * #v + #v'' * #w)

goal (2 subgoals):
 1. V2 = #v + Polynomial.smult (of_nat q) (#v')
 2. W2 = #w + Polynomial.smult (of_nat q) (#w')
[PROOF STEP]
have "u - #v * #w = smult (of_nat q) (#f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u - #v * #w = Polynomial.smult (of_nat q) (#f)
[PROOF STEP]
by (subst u, simp)
[PROOF STATE]
proof (state)
this:
u - #v * #w = Polynomial.smult (of_nat q) (#f)

goal (2 subgoals):
 1. V2 = #v + Polynomial.smult (of_nat q) (#v')
 2. W2 = #w + Polynomial.smult (of_nat q) (#w')
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
Polynomial.smult (of_nat q) (#f) = Polynomial.smult (of_nat q) (#w'' * #v + #v'' * #w)
[PROOF STEP]
have "w'' * #v + v'' * #w = f"
[PROOF STATE]
proof (prove)
using this:
Polynomial.smult (of_nat q) (#f) = Polynomial.smult (of_nat q) (#w'' * #v + #v'' * #w)

goal (1 subgoal):
 1. w'' * #v + v'' * #w = f
[PROOF STEP]
by (simp add: hom_distribs)
[PROOF STATE]
proof (state)
this:
w'' * #v + v'' * #w = f

goal (2 subgoals):
 1. V2 = #v + Polynomial.smult (of_nat q) (#v')
 2. W2 = #w + Polynomial.smult (of_nat q) (#w')
[PROOF STEP]
from pre_unique[OF this degv'']
[PROOF STATE]
proof (chain)
picking this:
v'' = v' \<and> w'' = w'
[PROOF STEP]
have pre: "v'' = v'" "w'' = w'"
[PROOF STATE]
proof (prove)
using this:
v'' = v' \<and> w'' = w'

goal (1 subgoal):
 1. v'' = v' &&& w'' = w'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v'' = v'
w'' = w'

goal (2 subgoals):
 1. V2 = #v + Polynomial.smult (of_nat q) (#v')
 2. W2 = #w + Polynomial.smult (of_nat q) (#w')
[PROOF STEP]
with V2 W2
[PROOF STATE]
proof (chain)
picking this:
V2 = #v + Polynomial.smult (of_nat CARD('q)) (#v'')
W2 = #w + Polynomial.smult (of_nat q) (#w'')
v'' = v'
w'' = w'
[PROOF STEP]
show "V2 = V" "W2 = W"
[PROOF STATE]
proof (prove)
using this:
V2 = #v + Polynomial.smult (of_nat CARD('q)) (#v'')
W2 = #w + Polynomial.smult (of_nat q) (#w'')
v'' = v'
w'' = w'

goal (1 subgoal):
 1. V2 = #v + Polynomial.smult (of_nat q) (#v') &&& W2 = #w + Polynomial.smult (of_nat q) (#w')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
V2 = #v + Polynomial.smult (of_nat q) (#v')
W2 = #w + Polynomial.smult (of_nat q) (#w')

goal:
No subgoals!
[PROOF STEP]
qed