[STATEMENT]
lemma dvd_monic:
  fixes p q:: "'a :: idom poly"
  assumes monic:"lead_coeff p=1" and "p dvd (smult c q)" and "c\<noteq>0"
  shows "p dvd q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p dvd q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
lead_coeff p = (1::'a)
p dvd smult c q
c \<noteq> (0::'a)

goal (1 subgoal):
 1. p dvd q
[PROOF STEP]
proof (cases "q=0 \<or> degree p=0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>lead_coeff p = (1::'a); p dvd smult c q; c \<noteq> (0::'a); q = 0 \<or> degree p = 0\<rbrakk> \<Longrightarrow> p dvd q
 2. \<lbrakk>lead_coeff p = (1::'a); p dvd smult c q; c \<noteq> (0::'a); \<not> (q = 0 \<or> degree p = 0)\<rbrakk> \<Longrightarrow> p dvd q
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
q = 0 \<or> degree p = 0

goal (2 subgoals):
 1. \<lbrakk>lead_coeff p = (1::'a); p dvd smult c q; c \<noteq> (0::'a); q = 0 \<or> degree p = 0\<rbrakk> \<Longrightarrow> p dvd q
 2. \<lbrakk>lead_coeff p = (1::'a); p dvd smult c q; c \<noteq> (0::'a); \<not> (q = 0 \<or> degree p = 0)\<rbrakk> \<Longrightarrow> p dvd q
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
q = 0 \<or> degree p = 0

goal (1 subgoal):
 1. p dvd q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
q = 0 \<or> degree p = 0
lead_coeff p = (1::'a)
p dvd smult c q
c \<noteq> (0::'a)

goal (1 subgoal):
 1. p dvd q
[PROOF STEP]
by (auto elim!: degree_eq_zeroE simp add: const_poly_dvd_iff)
[PROOF STATE]
proof (state)
this:
p dvd q

goal (1 subgoal):
 1. \<lbrakk>lead_coeff p = (1::'a); p dvd smult c q; c \<noteq> (0::'a); \<not> (q = 0 \<or> degree p = 0)\<rbrakk> \<Longrightarrow> p dvd q
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>lead_coeff p = (1::'a); p dvd smult c q; c \<noteq> (0::'a); \<not> (q = 0 \<or> degree p = 0)\<rbrakk> \<Longrightarrow> p dvd q
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (q = 0 \<or> degree p = 0)

goal (1 subgoal):
 1. \<lbrakk>lead_coeff p = (1::'a); p dvd smult c q; c \<noteq> (0::'a); \<not> (q = 0 \<or> degree p = 0)\<rbrakk> \<Longrightarrow> p dvd q
[PROOF STEP]
hence "q\<noteq>0" and "degree p\<noteq>0"
[PROOF STATE]
proof (prove)
using this:
\<not> (q = 0 \<or> degree p = 0)

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

goal (1 subgoal):
 1. \<lbrakk>lead_coeff p = (1::'a); p dvd smult c q; c \<noteq> (0::'a); \<not> (q = 0 \<or> degree p = 0)\<rbrakk> \<Longrightarrow> p dvd q
[PROOF STEP]
obtain k where k:"smult c q = p*k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k. smult c q = p * k \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms dvd_def
[PROOF STATE]
proof (prove)
using this:
lead_coeff p = (1::'a)
p dvd smult c q
c \<noteq> (0::'a)
(?b dvd ?a) = (\<exists>k. ?a = ?b * k)

goal (1 subgoal):
 1. (\<And>k. smult c q = p * k \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
smult c q = p * k

goal (1 subgoal):
 1. \<lbrakk>lead_coeff p = (1::'a); p dvd smult c q; c \<noteq> (0::'a); \<not> (q = 0 \<or> degree p = 0)\<rbrakk> \<Longrightarrow> p dvd q
[PROOF STEP]
hence "k\<noteq>0"
[PROOF STATE]
proof (prove)
using this:
smult c q = p * k

goal (1 subgoal):
 1. k \<noteq> 0
[PROOF STEP]
by (metis False assms(3) mult_zero_right smult_eq_0_iff)
[PROOF STATE]
proof (state)
this:
k \<noteq> 0

goal (1 subgoal):
 1. \<lbrakk>lead_coeff p = (1::'a); p dvd smult c q; c \<noteq> (0::'a); \<not> (q = 0 \<or> degree p = 0)\<rbrakk> \<Longrightarrow> p dvd q
[PROOF STEP]
hence deg_eq:"degree q=degree p + degree k"
[PROOF STATE]
proof (prove)
using this:
k \<noteq> 0

goal (1 subgoal):
 1. degree q = degree p + degree k
[PROOF STEP]
by (metis False assms(3) degree_0 degree_mult_eq degree_smult_eq k)
[PROOF STATE]
proof (state)
this:
degree q = degree p + degree k

goal (1 subgoal):
 1. \<lbrakk>lead_coeff p = (1::'a); p dvd smult c q; c \<noteq> (0::'a); \<not> (q = 0 \<or> degree p = 0)\<rbrakk> \<Longrightarrow> p dvd q
[PROOF STEP]
have c_dvd:"\<forall>n\<le>degree k. c dvd coeff k (degree k - n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n\<le>degree k. c dvd coeff k (degree k - n)
[PROOF STEP]
proof (rule,rule)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. n \<le> degree k \<Longrightarrow> c dvd coeff k (degree k - n)
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. n \<le> degree k \<Longrightarrow> c dvd coeff k (degree k - n)
[PROOF STEP]
assume "n \<le> degree k "
[PROOF STATE]
proof (state)
this:
n \<le> degree k

goal (1 subgoal):
 1. \<And>n. n \<le> degree k \<Longrightarrow> c dvd coeff k (degree k - n)
[PROOF STEP]
thus "c dvd coeff k (degree k - n)"
[PROOF STATE]
proof (prove)
using this:
n \<le> degree k

goal (1 subgoal):
 1. c dvd coeff k (degree k - n)
[PROOF STEP]
proof (induct n rule:nat_less_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>m<n. m \<le> degree k \<longrightarrow> c dvd coeff k (degree k - m); n \<le> degree k\<rbrakk> \<Longrightarrow> c dvd coeff k (degree k - n)
[PROOF STEP]
case (1 n)
[PROOF STATE]
proof (state)
this:
\<forall>m<n. m \<le> degree k \<longrightarrow> c dvd coeff k (degree k - m)
n \<le> degree k

goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>m<n. m \<le> degree k \<longrightarrow> c dvd coeff k (degree k - m); n \<le> degree k\<rbrakk> \<Longrightarrow> c dvd coeff k (degree k - n)
[PROOF STEP]
define T where "T\<equiv>(\<lambda>i. coeff p i * coeff k (degree p+degree k - n - i))"
[PROOF STATE]
proof (state)
this:
T \<equiv> \<lambda>i. coeff p i * coeff k (degree p + degree k - n - i)

goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>m<n. m \<le> degree k \<longrightarrow> c dvd coeff k (degree k - m); n \<le> degree k\<rbrakk> \<Longrightarrow> c dvd coeff k (degree k - n)
[PROOF STEP]
have "c * coeff q (degree q - n) = (\<Sum>i\<le>degree q - n. coeff p i * coeff k (degree q - n - i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c * coeff q (degree q - n) = (\<Sum>i\<le>degree q - n. coeff p i * coeff k (degree q - n - i))
[PROOF STEP]
using coeff_mult[of p k "degree q - n"] k coeff_smult[of c q "degree q -n"]
[PROOF STATE]
proof (prove)
using this:
coeff (p * k) (degree q - n) = (\<Sum>i\<le>degree q - n. coeff p i * coeff k (degree q - n - i))
smult c q = p * k
coeff (smult c q) (degree q - n) = c * coeff q (degree q - n)

goal (1 subgoal):
 1. c * coeff q (degree q - n) = (\<Sum>i\<le>degree q - n. coeff p i * coeff k (degree q - n - i))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c * coeff q (degree q - n) = (\<Sum>i\<le>degree q - n. coeff p i * coeff k (degree q - n - i))

goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>m<n. m \<le> degree k \<longrightarrow> c dvd coeff k (degree k - m); n \<le> degree k\<rbrakk> \<Longrightarrow> c dvd coeff k (degree k - n)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
c * coeff q (degree q - n) = (\<Sum>i\<le>degree q - n. coeff p i * coeff k (degree q - n - i))

goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>m<n. m \<le> degree k \<longrightarrow> c dvd coeff k (degree k - m); n \<le> degree k\<rbrakk> \<Longrightarrow> c dvd coeff k (degree k - n)
[PROOF STEP]
have "...=(\<Sum>i\<le>degree p+degree k - n. T i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<le>degree q - n. coeff p i * coeff k (degree q - n - i)) = sum T {..degree p + degree k - n}
[PROOF STEP]
using deg_eq
[PROOF STATE]
proof (prove)
using this:
degree q = degree p + degree k

goal (1 subgoal):
 1. (\<Sum>i\<le>degree q - n. coeff p i * coeff k (degree q - n - i)) = sum T {..degree p + degree k - n}
[PROOF STEP]
unfolding T_def
[PROOF STATE]
proof (prove)
using this:
degree q = degree p + degree k

goal (1 subgoal):
 1. (\<Sum>i\<le>degree q - n. coeff p i * coeff k (degree q - n - i)) = (\<Sum>i\<le>degree p + degree k - n. coeff p i * coeff k (degree p + degree k - n - i))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<le>degree q - n. coeff p i * coeff k (degree q - n - i)) = sum T {..degree p + degree k - n}

goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>m<n. m \<le> degree k \<longrightarrow> c dvd coeff k (degree k - m); n \<le> degree k\<rbrakk> \<Longrightarrow> c dvd coeff k (degree k - n)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<le>degree q - n. coeff p i * coeff k (degree q - n - i)) = sum T {..degree p + degree k - n}

goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>m<n. m \<le> degree k \<longrightarrow> c dvd coeff k (degree k - m); n \<le> degree k\<rbrakk> \<Longrightarrow> c dvd coeff k (degree k - n)
[PROOF STEP]
have "...=(\<Sum>i\<in>{0..<degree p}. T i) + sum T {(degree p)}+
                  sum T {degree p + 1..degree p + degree k - n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum T {..degree p + degree k - n} = sum T {0..<degree p} + sum T {degree p} + sum T {degree p + 1..degree p + degree k - n}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sum T {..degree p + degree k - n} = sum T {0..<degree p} + sum T {degree p} + sum T {degree p + 1..degree p + degree k - n}
[PROOF STEP]
define C where "C\<equiv>{{0..<degree p}, {degree p},{degree p+1..degree p+degree k-n}}"
[PROOF STATE]
proof (state)
this:
C \<equiv> {{0..<degree p}, {degree p}, {degree p + 1..degree p + degree k - n}}

goal (1 subgoal):
 1. sum T {..degree p + degree k - n} = sum T {0..<degree p} + sum T {degree p} + sum T {degree p + 1..degree p + degree k - n}
[PROOF STEP]
have "\<forall>A\<in>C. finite A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>A\<in>C. finite A
[PROOF STEP]
unfolding C_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>A\<in>{{0..<degree p}, {degree p}, {degree p + 1..degree p + degree k - n}}. finite A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>A\<in>C. finite A

goal (1 subgoal):
 1. sum T {..degree p + degree k - n} = sum T {0..<degree p} + sum T {degree p} + sum T {degree p + 1..degree p + degree k - n}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>A\<in>C. finite A

goal (1 subgoal):
 1. sum T {..degree p + degree k - n} = sum T {0..<degree p} + sum T {degree p} + sum T {degree p + 1..degree p + degree k - n}
[PROOF STEP]
have "\<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> A \<inter> B = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> A \<inter> B = {}
[PROOF STEP]
unfolding C_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>A\<in>{{0..<degree p}, {degree p}, {degree p + 1..degree p + degree k - n}}. \<forall>B\<in>{{0..<degree p}, {degree p}, {degree p + 1..degree p + degree k - n}}. A \<noteq> B \<longrightarrow> A \<inter> B = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> A \<inter> B = {}

goal (1 subgoal):
 1. sum T {..degree p + degree k - n} = sum T {0..<degree p} + sum T {degree p} + sum T {degree p + 1..degree p + degree k - n}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>A\<in>C. finite A
\<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> A \<inter> B = {}
[PROOF STEP]
have "sum T (\<Union>C) = sum (sum T) C"
[PROOF STATE]
proof (prove)
using this:
\<forall>A\<in>C. finite A
\<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> A \<inter> B = {}

goal (1 subgoal):
 1. sum T (\<Union> C) = sum (sum T) C
[PROOF STEP]
using sum.Union_disjoint
[PROOF STATE]
proof (prove)
using this:
\<forall>A\<in>C. finite A
\<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> A \<inter> B = {}
\<lbrakk>\<forall>A\<in>?C. finite A; \<forall>A\<in>?C. \<forall>B\<in>?C. A \<noteq> B \<longrightarrow> A \<inter> B = {}\<rbrakk> \<Longrightarrow> sum ?g (\<Union> ?C) = (sum \<circ> sum) ?g ?C

goal (1 subgoal):
 1. sum T (\<Union> C) = sum (sum T) C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sum T (\<Union> C) = sum (sum T) C

goal (1 subgoal):
 1. sum T {..degree p + degree k - n} = sum T {0..<degree p} + sum T {degree p} + sum T {degree p + 1..degree p + degree k - n}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sum T (\<Union> C) = sum (sum T) C

goal (1 subgoal):
 1. sum T {..degree p + degree k - n} = sum T {0..<degree p} + sum T {degree p} + sum T {degree p + 1..degree p + degree k - n}
[PROOF STEP]
have "\<Union>C={..degree p + degree k - n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> C = {..degree p + degree k - n}
[PROOF STEP]
using \<open>n \<le> degree k\<close>
[PROOF STATE]
proof (prove)
using this:
n \<le> degree k

goal (1 subgoal):
 1. \<Union> C = {..degree p + degree k - n}
[PROOF STEP]
unfolding C_def
[PROOF STATE]
proof (prove)
using this:
n \<le> degree k

goal (1 subgoal):
 1. \<Union> {{0..<degree p}, {degree p}, {degree p + 1..degree p + degree k - n}} = {..degree p + degree k - n}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Union> C = {..degree p + degree k - n}

goal (1 subgoal):
 1. sum T {..degree p + degree k - n} = sum T {0..<degree p} + sum T {degree p} + sum T {degree p + 1..degree p + degree k - n}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Union> C = {..degree p + degree k - n}

goal (1 subgoal):
 1. sum T {..degree p + degree k - n} = sum T {0..<degree p} + sum T {degree p} + sum T {degree p + 1..degree p + degree k - n}
[PROOF STEP]
have  "sum (sum T) C= sum T {0..<degree p} + sum T {(degree p)} +
                  sum T {degree p + 1..degree p + degree k - n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum (sum T) C = sum T {0..<degree p} + sum T {degree p} + sum T {degree p + 1..degree p + degree k - n}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sum (sum T) C = sum T {0..<degree p} + sum T {degree p} + sum T {degree p + 1..degree p + degree k - n}
[PROOF STEP]
have "{0..<degree p}\<noteq>{degree p}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {0..<degree p} \<noteq> {degree p}
[PROOF STEP]
by (metis atLeast0LessThan insertI1 lessThan_iff less_imp_not_eq)
[PROOF STATE]
proof (state)
this:
{0..<degree p} \<noteq> {degree p}

goal (1 subgoal):
 1. sum (sum T) C = sum T {0..<degree p} + sum T {degree p} + sum T {degree p + 1..degree p + degree k - n}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{0..<degree p} \<noteq> {degree p}

goal (1 subgoal):
 1. sum (sum T) C = sum T {0..<degree p} + sum T {degree p} + sum T {degree p + 1..degree p + degree k - n}
[PROOF STEP]
have "{degree p}\<noteq>{degree p + 1..degree p + degree k - n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {degree p} \<noteq> {degree p + 1..degree p + degree k - n}
[PROOF STEP]
by (metis add.commute add_diff_cancel_right' atLeastAtMost_singleton_iff
                  diff_self_eq_0 eq_imp_le not_one_le_zero)
[PROOF STATE]
proof (state)
this:
{degree p} \<noteq> {degree p + 1..degree p + degree k - n}

goal (1 subgoal):
 1. sum (sum T) C = sum T {0..<degree p} + sum T {degree p} + sum T {degree p + 1..degree p + degree k - n}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{degree p} \<noteq> {degree p + 1..degree p + degree k - n}

goal (1 subgoal):
 1. sum (sum T) C = sum T {0..<degree p} + sum T {degree p} + sum T {degree p + 1..degree p + degree k - n}
[PROOF STEP]
have "{0..<degree p}\<noteq>{degree p + 1..degree p + degree k - n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {0..<degree p} \<noteq> {degree p + 1..degree p + degree k - n}
[PROOF STEP]
using \<open>degree k\<ge>n\<close> \<open>degree p\<noteq>0\<close>
[PROOF STATE]
proof (prove)
using this:
n \<le> degree k
degree p \<noteq> 0

goal (1 subgoal):
 1. {0..<degree p} \<noteq> {degree p + 1..degree p + degree k - n}
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
{0..<degree p} \<noteq> {degree p + 1..degree p + degree k - n}

goal (1 subgoal):
 1. sum (sum T) C = sum T {0..<degree p} + sum T {degree p} + sum T {degree p + 1..degree p + degree k - n}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
{0..<degree p} \<noteq> {degree p}
{degree p} \<noteq> {degree p + 1..degree p + degree k - n}
{0..<degree p} \<noteq> {degree p + 1..degree p + degree k - n}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
{0..<degree p} \<noteq> {degree p}
{degree p} \<noteq> {degree p + 1..degree p + degree k - n}
{0..<degree p} \<noteq> {degree p + 1..degree p + degree k - n}

goal (1 subgoal):
 1. sum (sum T) C = sum T {0..<degree p} + sum T {degree p} + sum T {degree p + 1..degree p + degree k - n}
[PROOF STEP]
unfolding C_def
[PROOF STATE]
proof (prove)
using this:
{0..<degree p} \<noteq> {degree p}
{degree p} \<noteq> {degree p + 1..degree p + degree k - n}
{0..<degree p} \<noteq> {degree p + 1..degree p + degree k - n}

goal (1 subgoal):
 1. sum (sum T) {{0..<degree p}, {degree p}, {degree p + 1..degree p + degree k - n}} = sum T {0..<degree p} + sum T {degree p} + sum T {degree p + 1..degree p + degree k - n}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sum (sum T) C = sum T {0..<degree p} + sum T {degree p} + sum T {degree p + 1..degree p + degree k - n}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sum (sum T) C = sum T {0..<degree p} + sum T {degree p} + sum T {degree p + 1..degree p + degree k - n}

goal (1 subgoal):
 1. sum T {..degree p + degree k - n} = sum T {0..<degree p} + sum T {degree p} + sum T {degree p + 1..degree p + degree k - n}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
sum T (\<Union> C) = sum (sum T) C
\<Union> C = {..degree p + degree k - n}
sum (sum T) C = sum T {0..<degree p} + sum T {degree p} + sum T {degree p + 1..degree p + degree k - n}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sum T (\<Union> C) = sum (sum T) C
\<Union> C = {..degree p + degree k - n}
sum (sum T) C = sum T {0..<degree p} + sum T {degree p} + sum T {degree p + 1..degree p + degree k - n}

goal (1 subgoal):
 1. sum T {..degree p + degree k - n} = sum T {0..<degree p} + sum T {degree p} + sum T {degree p + 1..degree p + degree k - n}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sum T {..degree p + degree k - n} = sum T {0..<degree p} + sum T {degree p} + sum T {degree p + 1..degree p + degree k - n}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sum T {..degree p + degree k - n} = sum T {0..<degree p} + sum T {degree p} + sum T {degree p + 1..degree p + degree k - n}

goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>m<n. m \<le> degree k \<longrightarrow> c dvd coeff k (degree k - m); n \<le> degree k\<rbrakk> \<Longrightarrow> c dvd coeff k (degree k - n)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum T {..degree p + degree k - n} = sum T {0..<degree p} + sum T {degree p} + sum T {degree p + 1..degree p + degree k - n}

goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>m<n. m \<le> degree k \<longrightarrow> c dvd coeff k (degree k - m); n \<le> degree k\<rbrakk> \<Longrightarrow> c dvd coeff k (degree k - n)
[PROOF STEP]
have "...=(\<Sum>i\<in>{0..<degree p}. T i) +  coeff k (degree k - n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum T {0..<degree p} + sum T {degree p} + sum T {degree p + 1..degree p + degree k - n} = sum T {0..<degree p} + coeff k (degree k - n)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sum T {0..<degree p} + sum T {degree p} + sum T {degree p + 1..degree p + degree k - n} = sum T {0..<degree p} + coeff k (degree k - n)
[PROOF STEP]
have "\<forall>x\<in>{degree p + 1..degree p + degree k - n}. T x=0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>{degree p + 1..degree p + degree k - n}. T x = (0::'a)
[PROOF STEP]
using coeff_eq_0[of p]
[PROOF STATE]
proof (prove)
using this:
degree p < ?n \<Longrightarrow> coeff p ?n = (0::'a)

goal (1 subgoal):
 1. \<forall>x\<in>{degree p + 1..degree p + degree k - n}. T x = (0::'a)
[PROOF STEP]
unfolding T_def
[PROOF STATE]
proof (prove)
using this:
degree p < ?n \<Longrightarrow> coeff p ?n = (0::'a)

goal (1 subgoal):
 1. \<forall>x\<in>{degree p + 1..degree p + degree k - n}. coeff p x * coeff k (degree p + degree k - n - x) = (0::'a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>{degree p + 1..degree p + degree k - n}. T x = (0::'a)

goal (1 subgoal):
 1. sum T {0..<degree p} + sum T {degree p} + sum T {degree p + 1..degree p + degree k - n} = sum T {0..<degree p} + coeff k (degree k - n)
[PROOF STEP]
hence "sum T {degree p + 1..degree p + degree k - n}=0"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>{degree p + 1..degree p + degree k - n}. T x = (0::'a)

goal (1 subgoal):
 1. sum T {degree p + 1..degree p + degree k - n} = (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sum T {degree p + 1..degree p + degree k - n} = (0::'a)

goal (1 subgoal):
 1. sum T {0..<degree p} + sum T {degree p} + sum T {degree p + 1..degree p + degree k - n} = sum T {0..<degree p} + coeff k (degree k - n)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sum T {degree p + 1..degree p + degree k - n} = (0::'a)

goal (1 subgoal):
 1. sum T {0..<degree p} + sum T {degree p} + sum T {degree p + 1..degree p + degree k - n} = sum T {0..<degree p} + coeff k (degree k - n)
[PROOF STEP]
have "T (degree p)=coeff k (degree k - n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T (degree p) = coeff k (degree k - n)
[PROOF STEP]
using monic
[PROOF STATE]
proof (prove)
using this:
lead_coeff p = (1::'a)

goal (1 subgoal):
 1. T (degree p) = coeff k (degree k - n)
[PROOF STEP]
by (simp add: T_def)
[PROOF STATE]
proof (state)
this:
T (degree p) = coeff k (degree k - n)

goal (1 subgoal):
 1. sum T {0..<degree p} + sum T {degree p} + sum T {degree p + 1..degree p + degree k - n} = sum T {0..<degree p} + coeff k (degree k - n)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
sum T {degree p + 1..degree p + degree k - n} = (0::'a)
T (degree p) = coeff k (degree k - n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sum T {degree p + 1..degree p + degree k - n} = (0::'a)
T (degree p) = coeff k (degree k - n)

goal (1 subgoal):
 1. sum T {0..<degree p} + sum T {degree p} + sum T {degree p + 1..degree p + degree k - n} = sum T {0..<degree p} + coeff k (degree k - n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sum T {0..<degree p} + sum T {degree p} + sum T {degree p + 1..degree p + degree k - n} = sum T {0..<degree p} + coeff k (degree k - n)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sum T {0..<degree p} + sum T {degree p} + sum T {degree p + 1..degree p + degree k - n} = sum T {0..<degree p} + coeff k (degree k - n)

goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>m<n. m \<le> degree k \<longrightarrow> c dvd coeff k (degree k - m); n \<le> degree k\<rbrakk> \<Longrightarrow> c dvd coeff k (degree k - n)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
c * coeff q (degree q - n) = sum T {0..<degree p} + coeff k (degree k - n)
[PROOF STEP]
have c_coeff: "c * coeff q (degree q - n) = sum T {0..<degree p}
              + coeff k (degree k - n)"
[PROOF STATE]
proof (prove)
using this:
c * coeff q (degree q - n) = sum T {0..<degree p} + coeff k (degree k - n)

goal (1 subgoal):
 1. c * coeff q (degree q - n) = sum T {0..<degree p} + coeff k (degree k - n)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
c * coeff q (degree q - n) = sum T {0..<degree p} + coeff k (degree k - n)

goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>m<n. m \<le> degree k \<longrightarrow> c dvd coeff k (degree k - m); n \<le> degree k\<rbrakk> \<Longrightarrow> c dvd coeff k (degree k - n)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
c * coeff q (degree q - n) = sum T {0..<degree p} + coeff k (degree k - n)

goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>m<n. m \<le> degree k \<longrightarrow> c dvd coeff k (degree k - m); n \<le> degree k\<rbrakk> \<Longrightarrow> c dvd coeff k (degree k - n)
[PROOF STEP]
have "n\<noteq>0\<Longrightarrow>c dvd sum T {0..<degree p}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> c dvd sum T {0..<degree p}
[PROOF STEP]
proof (rule dvd_sum)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>n \<noteq> 0; a \<in> {0..<degree p}\<rbrakk> \<Longrightarrow> c dvd T a
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>n \<noteq> 0; a \<in> {0..<degree p}\<rbrakk> \<Longrightarrow> c dvd T a
[PROOF STEP]
assume i:"i \<in> {0..<degree p}" and "n\<noteq>0"
[PROOF STATE]
proof (state)
this:
i \<in> {0..<degree p}
n \<noteq> 0

goal (1 subgoal):
 1. \<And>a. \<lbrakk>n \<noteq> 0; a \<in> {0..<degree p}\<rbrakk> \<Longrightarrow> c dvd T a
[PROOF STEP]
hence "(n+i-degree p)\<le>degree k"
[PROOF STATE]
proof (prove)
using this:
i \<in> {0..<degree p}
n \<noteq> 0

goal (1 subgoal):
 1. n + i - degree p \<le> degree k
[PROOF STEP]
using \<open>n \<le> degree k\<close>
[PROOF STATE]
proof (prove)
using this:
i \<in> {0..<degree p}
n \<noteq> 0
n \<le> degree k

goal (1 subgoal):
 1. n + i - degree p \<le> degree k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n + i - degree p \<le> degree k

goal (1 subgoal):
 1. \<And>a. \<lbrakk>n \<noteq> 0; a \<in> {0..<degree p}\<rbrakk> \<Longrightarrow> c dvd T a
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
n + i - degree p \<le> degree k

goal (1 subgoal):
 1. \<And>a. \<lbrakk>n \<noteq> 0; a \<in> {0..<degree p}\<rbrakk> \<Longrightarrow> c dvd T a
[PROOF STEP]
have "n + i - degree p <n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n + i - degree p < n
[PROOF STEP]
using i \<open>n\<noteq>0\<close>
[PROOF STATE]
proof (prove)
using this:
i \<in> {0..<degree p}
n \<noteq> 0

goal (1 subgoal):
 1. n + i - degree p < n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n + i - degree p < n

goal (1 subgoal):
 1. \<And>a. \<lbrakk>n \<noteq> 0; a \<in> {0..<degree p}\<rbrakk> \<Longrightarrow> c dvd T a
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
n + i - degree p \<le> degree k
n + i - degree p < n
[PROOF STEP]
have "c dvd coeff k (degree k - (n+i-degree p))"
[PROOF STATE]
proof (prove)
using this:
n + i - degree p \<le> degree k
n + i - degree p < n

goal (1 subgoal):
 1. c dvd coeff k (degree k - (n + i - degree p))
[PROOF STEP]
using 1(1)
[PROOF STATE]
proof (prove)
using this:
n + i - degree p \<le> degree k
n + i - degree p < n
\<forall>m<n. m \<le> degree k \<longrightarrow> c dvd coeff k (degree k - m)

goal (1 subgoal):
 1. c dvd coeff k (degree k - (n + i - degree p))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c dvd coeff k (degree k - (n + i - degree p))

goal (1 subgoal):
 1. \<And>a. \<lbrakk>n \<noteq> 0; a \<in> {0..<degree p}\<rbrakk> \<Longrightarrow> c dvd T a
[PROOF STEP]
hence "c dvd coeff k (degree p + degree k - n - i)"
[PROOF STATE]
proof (prove)
using this:
c dvd coeff k (degree k - (n + i - degree p))

goal (1 subgoal):
 1. c dvd coeff k (degree p + degree k - n - i)
[PROOF STEP]
by (metis add_diff_cancel_left' deg_eq diff_diff_left dvd_0_right le_degree
                  le_diff_conv add.commute ordered_cancel_comm_monoid_diff_class.diff_diff_right)
[PROOF STATE]
proof (state)
this:
c dvd coeff k (degree p + degree k - n - i)

goal (1 subgoal):
 1. \<And>a. \<lbrakk>n \<noteq> 0; a \<in> {0..<degree p}\<rbrakk> \<Longrightarrow> c dvd T a
[PROOF STEP]
thus "c dvd T i"
[PROOF STATE]
proof (prove)
using this:
c dvd coeff k (degree p + degree k - n - i)

goal (1 subgoal):
 1. c dvd T i
[PROOF STEP]
unfolding T_def
[PROOF STATE]
proof (prove)
using this:
c dvd coeff k (degree p + degree k - n - i)

goal (1 subgoal):
 1. c dvd coeff p i * coeff k (degree p + degree k - n - i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c dvd T i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
n \<noteq> 0 \<Longrightarrow> c dvd sum T {0..<degree p}

goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>m<n. m \<le> degree k \<longrightarrow> c dvd coeff k (degree k - m); n \<le> degree k\<rbrakk> \<Longrightarrow> c dvd coeff k (degree k - n)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
n \<noteq> 0 \<Longrightarrow> c dvd sum T {0..<degree p}

goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>m<n. m \<le> degree k \<longrightarrow> c dvd coeff k (degree k - m); n \<le> degree k\<rbrakk> \<Longrightarrow> c dvd coeff k (degree k - n)
[PROOF STEP]
have "n=0 \<Longrightarrow>?case"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n = 0 \<Longrightarrow> c dvd coeff k (degree k - n)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n = 0 \<Longrightarrow> c dvd coeff k (degree k - n)
[PROOF STEP]
assume "n=0"
[PROOF STATE]
proof (state)
this:
n = 0

goal (1 subgoal):
 1. n = 0 \<Longrightarrow> c dvd coeff k (degree k - n)
[PROOF STEP]
hence "\<forall>i\<in>{0..<degree p}. coeff k (degree p + degree k - n - i) =0"
[PROOF STATE]
proof (prove)
using this:
n = 0

goal (1 subgoal):
 1. \<forall>i\<in>{0..<degree p}. coeff k (degree p + degree k - n - i) = (0::'a)
[PROOF STEP]
using coeff_eq_0[of k]
[PROOF STATE]
proof (prove)
using this:
n = 0
degree k < ?n \<Longrightarrow> coeff k ?n = (0::'a)

goal (1 subgoal):
 1. \<forall>i\<in>{0..<degree p}. coeff k (degree p + degree k - n - i) = (0::'a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>i\<in>{0..<degree p}. coeff k (degree p + degree k - n - i) = (0::'a)

goal (1 subgoal):
 1. n = 0 \<Longrightarrow> c dvd coeff k (degree k - n)
[PROOF STEP]
hence "c * coeff q (degree q - n) = coeff k (degree k - n)"
[PROOF STATE]
proof (prove)
using this:
\<forall>i\<in>{0..<degree p}. coeff k (degree p + degree k - n - i) = (0::'a)

goal (1 subgoal):
 1. c * coeff q (degree q - n) = coeff k (degree k - n)
[PROOF STEP]
using c_coeff
[PROOF STATE]
proof (prove)
using this:
\<forall>i\<in>{0..<degree p}. coeff k (degree p + degree k - n - i) = (0::'a)
c * coeff q (degree q - n) = sum T {0..<degree p} + coeff k (degree k - n)

goal (1 subgoal):
 1. c * coeff q (degree q - n) = coeff k (degree k - n)
[PROOF STEP]
unfolding T_def
[PROOF STATE]
proof (prove)
using this:
\<forall>i\<in>{0..<degree p}. coeff k (degree p + degree k - n - i) = (0::'a)
c * coeff q (degree q - n) = (\<Sum>i = 0..<degree p. coeff p i * coeff k (degree p + degree k - n - i)) + coeff k (degree k - n)

goal (1 subgoal):
 1. c * coeff q (degree q - n) = coeff k (degree k - n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c * coeff q (degree q - n) = coeff k (degree k - n)

goal (1 subgoal):
 1. n = 0 \<Longrightarrow> c dvd coeff k (degree k - n)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
c * coeff q (degree q - n) = coeff k (degree k - n)

goal (1 subgoal):
 1. c dvd coeff k (degree k - n)
[PROOF STEP]
by (metis dvdI)
[PROOF STATE]
proof (state)
this:
c dvd coeff k (degree k - n)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
n = 0 \<Longrightarrow> c dvd coeff k (degree k - n)

goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>m<n. m \<le> degree k \<longrightarrow> c dvd coeff k (degree k - m); n \<le> degree k\<rbrakk> \<Longrightarrow> c dvd coeff k (degree k - n)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
c * coeff q (degree q - n) = sum T {0..<degree p} + coeff k (degree k - n)
n \<noteq> 0 \<Longrightarrow> c dvd sum T {0..<degree p}
n = 0 \<Longrightarrow> c dvd coeff k (degree k - n)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
c * coeff q (degree q - n) = sum T {0..<degree p} + coeff k (degree k - n)
n \<noteq> 0 \<Longrightarrow> c dvd sum T {0..<degree p}
n = 0 \<Longrightarrow> c dvd coeff k (degree k - n)

goal (1 subgoal):
 1. c dvd coeff k (degree k - n)
[PROOF STEP]
by (metis dvd_add_right_iff dvd_triv_left)
[PROOF STATE]
proof (state)
this:
c dvd coeff k (degree k - n)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
c dvd coeff k (degree k - n)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>n\<le>degree k. c dvd coeff k (degree k - n)

goal (1 subgoal):
 1. \<lbrakk>lead_coeff p = (1::'a); p dvd smult c q; c \<noteq> (0::'a); \<not> (q = 0 \<or> degree p = 0)\<rbrakk> \<Longrightarrow> p dvd q
[PROOF STEP]
hence "\<forall>n. c dvd coeff k n"
[PROOF STATE]
proof (prove)
using this:
\<forall>n\<le>degree k. c dvd coeff k (degree k - n)

goal (1 subgoal):
 1. \<forall>n. c dvd coeff k n
[PROOF STEP]
by (metis diff_diff_cancel dvd_0_right le_add2 le_add_diff_inverse le_degree)
[PROOF STATE]
proof (state)
this:
\<forall>n. c dvd coeff k n

goal (1 subgoal):
 1. \<lbrakk>lead_coeff p = (1::'a); p dvd smult c q; c \<noteq> (0::'a); \<not> (q = 0 \<or> degree p = 0)\<rbrakk> \<Longrightarrow> p dvd q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>n. c dvd coeff k n
[PROOF STEP]
obtain f where f:"\<forall>n. c * f n=coeff k n"
[PROOF STATE]
proof (prove)
using this:
\<forall>n. c dvd coeff k n

goal (1 subgoal):
 1. (\<And>f. \<forall>n. c * f n = coeff k n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding dvd_def
[PROOF STATE]
proof (prove)
using this:
\<forall>n. \<exists>ka. coeff k n = c * ka

goal (1 subgoal):
 1. (\<And>f. \<forall>n. c * f n = coeff k n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<forall>n. c * f n = coeff k n

goal (1 subgoal):
 1. \<lbrakk>lead_coeff p = (1::'a); p dvd smult c q; c \<noteq> (0::'a); \<not> (q = 0 \<or> degree p = 0)\<rbrakk> \<Longrightarrow> p dvd q
[PROOF STEP]
have " \<forall>\<^sub>\<infinity> n. f n = 0 "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>\<infinity>n. f n = (0::'a)
[PROOF STEP]
by (metis (mono_tags, lifting) MOST_coeff_eq_0 MOST_mono assms(3) f mult_eq_0_iff)
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>\<infinity>n. f n = (0::'a)

goal (1 subgoal):
 1. \<lbrakk>lead_coeff p = (1::'a); p dvd smult c q; c \<noteq> (0::'a); \<not> (q = 0 \<or> degree p = 0)\<rbrakk> \<Longrightarrow> p dvd q
[PROOF STEP]
hence "smult c (Abs_poly f)=k"
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>\<infinity>n. f n = (0::'a)

goal (1 subgoal):
 1. smult c (Abs_poly f) = k
[PROOF STEP]
using f smult.abs_eq[of c "Abs_poly f"] Abs_poly_inverse[of f] coeff_inverse[of k]
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>\<infinity>n. f n = (0::'a)
\<forall>n. c * f n = coeff k n
smult c (Abs_poly f) = Abs_poly (\<lambda>n. c * coeff (Abs_poly f) n)
f \<in> {f. \<forall>\<^sub>\<infinity>n. f n = (0::'a)} \<Longrightarrow> coeff (Abs_poly f) = f
Abs_poly (coeff k) = k

goal (1 subgoal):
 1. smult c (Abs_poly f) = k
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
smult c (Abs_poly f) = k

goal (1 subgoal):
 1. \<lbrakk>lead_coeff p = (1::'a); p dvd smult c q; c \<noteq> (0::'a); \<not> (q = 0 \<or> degree p = 0)\<rbrakk> \<Longrightarrow> p dvd q
[PROOF STEP]
hence "q=p* Abs_poly f"
[PROOF STATE]
proof (prove)
using this:
smult c (Abs_poly f) = k

goal (1 subgoal):
 1. q = p * Abs_poly f
[PROOF STEP]
using k \<open>c\<noteq>0\<close> smult_cancel
[PROOF STATE]
proof (prove)
using this:
smult c (Abs_poly f) = k
smult c q = p * k
c \<noteq> (0::'a)
\<lbrakk>?c \<noteq> (0::?'a); smult ?c ?p = smult ?c ?q\<rbrakk> \<Longrightarrow> ?p = ?q

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

goal (1 subgoal):
 1. \<lbrakk>lead_coeff p = (1::'a); p dvd smult c q; c \<noteq> (0::'a); \<not> (q = 0 \<or> degree p = 0)\<rbrakk> \<Longrightarrow> p dvd q
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
q = p * Abs_poly f

goal (1 subgoal):
 1. p dvd q
[PROOF STEP]
unfolding dvd_def
[PROOF STATE]
proof (prove)
using this:
q = p * Abs_poly f

goal (1 subgoal):
 1. \<exists>k. q = p * k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p dvd q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma poly_power_n_eq:
  fixes x::"'a :: idom"
  assumes "n\<noteq>0"
  shows "poly ([:-a,1:]^n) x=0 \<longleftrightarrow> (x=a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (poly ([:- a, 1::'a:] ^ n) x = (0::'a)) = (x = a)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
n \<noteq> 0

goal (1 subgoal):
 1. (poly ([:- a, 1::'a:] ^ n) x = (0::'a)) = (x = a)
[PROOF STEP]
by (induct n,auto)


[STATEMENT]
lemma poly_power_n_odd:
  fixes x a:: real
  assumes "odd n"
  shows "poly ([:-a,1:]^n) x>0 \<longleftrightarrow> (x>a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0 < poly ([:- a, 1:] ^ n) x) = (a < x)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
odd n

goal (1 subgoal):
 1. (0 < poly ([:- a, 1:] ^ n) x) = (a < x)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. odd n \<Longrightarrow> (0 < poly ([:- a, 1:] ^ n) x) = (a < x)
[PROOF STEP]
have "poly ([:-a,1:]^n) x\<ge>0 = (poly [:- a, 1:] x \<ge>0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0 \<le> poly ([:- a, 1:] ^ n) x) = (0 \<le> poly [:- a, 1:] x)
[PROOF STEP]
unfolding poly_power
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0 \<le> poly [:- a, 1:] x ^ n) = (0 \<le> poly [:- a, 1:] x)
[PROOF STEP]
using zero_le_odd_power[OF \<open>odd n\<close>]
[PROOF STATE]
proof (prove)
using this:
((0::?'a) \<le> ?a ^ n) = ((0::?'a) \<le> ?a)

goal (1 subgoal):
 1. (0 \<le> poly [:- a, 1:] x ^ n) = (0 \<le> poly [:- a, 1:] x)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(0 \<le> poly ([:- a, 1:] ^ n) x) = (0 \<le> poly [:- a, 1:] x)

goal (1 subgoal):
 1. odd n \<Longrightarrow> (0 < poly ([:- a, 1:] ^ n) x) = (a < x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(0 \<le> poly ([:- a, 1:] ^ n) x) = (0 \<le> poly [:- a, 1:] x)

goal (1 subgoal):
 1. odd n \<Longrightarrow> (0 < poly ([:- a, 1:] ^ n) x) = (a < x)
[PROOF STEP]
have "(poly [:- a, 1:] x \<ge>0) = (x\<ge>a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0 \<le> poly [:- a, 1:] x) = (a \<le> x)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(0 \<le> poly [:- a, 1:] x) = (a \<le> x)

goal (1 subgoal):
 1. odd n \<Longrightarrow> (0 < poly ([:- a, 1:] ^ n) x) = (a < x)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(0 \<le> poly ([:- a, 1:] ^ n) x) = (a \<le> x)
[PROOF STEP]
have "poly ([:-a,1:]^n) x\<ge>0 = (x\<ge>a)"
[PROOF STATE]
proof (prove)
using this:
(0 \<le> poly ([:- a, 1:] ^ n) x) = (a \<le> x)

goal (1 subgoal):
 1. (0 \<le> poly ([:- a, 1:] ^ n) x) = (a \<le> x)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(0 \<le> poly ([:- a, 1:] ^ n) x) = (a \<le> x)

goal (1 subgoal):
 1. odd n \<Longrightarrow> (0 < poly ([:- a, 1:] ^ n) x) = (a < x)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(0 \<le> poly ([:- a, 1:] ^ n) x) = (a \<le> x)

goal (1 subgoal):
 1. odd n \<Longrightarrow> (0 < poly ([:- a, 1:] ^ n) x) = (a < x)
[PROOF STEP]
have "poly ([:-a,1:]^n) x=0 = (x=a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (poly ([:- a, 1:] ^ n) x = 0) = (x = a)
[PROOF STEP]
by(rule poly_power_n_eq, metis assms even_zero)
[PROOF STATE]
proof (state)
this:
(poly ([:- a, 1:] ^ n) x = 0) = (x = a)

goal (1 subgoal):
 1. odd n \<Longrightarrow> (0 < poly ([:- a, 1:] ^ n) x) = (a < x)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(0 \<le> poly ([:- a, 1:] ^ n) x) = (a \<le> x)
(poly ([:- a, 1:] ^ n) x = 0) = (x = a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(0 \<le> poly ([:- a, 1:] ^ n) x) = (a \<le> x)
(poly ([:- a, 1:] ^ n) x = 0) = (x = a)

goal (1 subgoal):
 1. (0 < poly ([:- a, 1:] ^ n) x) = (a < x)
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
(0 < poly ([:- a, 1:] ^ n) x) = (a < x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma gcd_coprime_poly:
  fixes p q::"'a::{factorial_ring_gcd,semiring_gcd_mult_normalize} poly"
  assumes nz: "p \<noteq> 0 \<or> q \<noteq> 0" and p': "p = p' * gcd p q" and
    q': "q = q' * gcd p q"
  shows "coprime p' q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coprime p' q'
[PROOF STEP]
using gcd_coprime nz p' q'
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>gcd ?a ?b \<noteq> (0::?'a); ?a = ?a' * gcd ?a ?b; ?b = ?b' * gcd ?a ?b\<rbrakk> \<Longrightarrow> coprime ?a' ?b'
p \<noteq> 0 \<or> q \<noteq> 0
p = p' * gcd p q
q = q' * gcd p q

goal (1 subgoal):
 1. coprime p' q'
[PROOF STEP]
by auto


[STATEMENT]
lemma poly_mod:
  "poly (p mod q) x = poly p x" if "poly q x = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly (p mod q) x = poly p x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. poly (p mod q) x = poly p x
[PROOF STEP]
from that
[PROOF STATE]
proof (chain)
picking this:
poly q x = (0::'a)
[PROOF STEP]
have "poly (p mod q) x = poly (p div q * q) x + poly (p mod q) x"
[PROOF STATE]
proof (prove)
using this:
poly q x = (0::'a)

goal (1 subgoal):
 1. poly (p mod q) x = poly (p div q * q) x + poly (p mod q) x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
poly (p mod q) x = poly (p div q * q) x + poly (p mod q) x

goal (1 subgoal):
 1. poly (p mod q) x = poly p x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
poly (p mod q) x = poly (p div q * q) x + poly (p mod q) x

goal (1 subgoal):
 1. poly (p mod q) x = poly p x
[PROOF STEP]
have "\<dots> = poly p x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly (p div q * q) x + poly (p mod q) x = poly p x
[PROOF STEP]
by (simp only: poly_add [symmetric]) simp
[PROOF STATE]
proof (state)
this:
poly (p div q * q) x + poly (p mod q) x = poly p x

goal (1 subgoal):
 1. poly (p mod q) x = poly p x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
poly (p mod q) x = poly p x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
poly (p mod q) x = poly p x

goal (1 subgoal):
 1. poly (p mod q) x = poly p x
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
poly (p mod q) x = poly p x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pseudo_divmod_0[simp]: "pseudo_divmod f 0 = (0,f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pseudo_divmod f 0 = (0, f)
[PROOF STEP]
unfolding pseudo_divmod_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if 0 = 0 then (0, f) else pseudo_divmod_main (lead_coeff 0) 0 f 0 (degree f) (1 + length (coeffs f) - length (coeffs 0))) = (0, f)
[PROOF STEP]
by auto


[STATEMENT]
lemma map_poly_eq_iff:
  assumes "f 0=0" "inj f"
  shows "map_poly f x =map_poly f y \<longleftrightarrow> x=y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (map_poly f x = map_poly f y) = (x = y)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
f (0::'b) = (0::'a)
inj f

goal (1 subgoal):
 1. (map_poly f x = map_poly f y) = (x = y)
[PROOF STEP]
by (auto simp: poly_eq_iff coeff_map_poly dest:injD)


[STATEMENT]
lemma pseudo_mod_0[simp]:
  shows "pseudo_mod p 0= p" "pseudo_mod 0 q = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pseudo_mod p 0 = p &&& pseudo_mod 0 q = 0
[PROOF STEP]
unfolding pseudo_mod_def pseudo_divmod_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (if 0 = 0 then (0, p) else pseudo_divmod_main (lead_coeff 0) 0 p 0 (degree p) (1 + length (coeffs p) - length (coeffs 0))) = p &&& snd (if q = 0 then (0, 0) else pseudo_divmod_main (lead_coeff q) 0 0 q (degree 0) (1 + length (coeffs 0) - length (coeffs q))) = 0
[PROOF STEP]
by (auto simp add: length_coeffs_degree)


[STATEMENT]
lemma pseudo_mod_mod:
  assumes "g\<noteq>0"
  shows "smult (lead_coeff g ^ (Suc (degree f) - degree g)) (f mod g) = pseudo_mod f g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. smult (lead_coeff g ^ (Suc (degree f) - degree g)) (f mod g) = pseudo_mod f g
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. smult (lead_coeff g ^ (Suc (degree f) - degree g)) (f mod g) = pseudo_mod f g
[PROOF STEP]
define a where "a=lead_coeff g ^ (Suc (degree f) - degree g)"
[PROOF STATE]
proof (state)
this:
a = lead_coeff g ^ (Suc (degree f) - degree g)

goal (1 subgoal):
 1. smult (lead_coeff g ^ (Suc (degree f) - degree g)) (f mod g) = pseudo_mod f g
[PROOF STEP]
have "a\<noteq>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<noteq> (0::'a)
[PROOF STEP]
unfolding a_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lead_coeff g ^ (Suc (degree f) - degree g) \<noteq> (0::'a)
[PROOF STEP]
by (simp add: assms)
[PROOF STATE]
proof (state)
this:
a \<noteq> (0::'a)

goal (1 subgoal):
 1. smult (lead_coeff g ^ (Suc (degree f) - degree g)) (f mod g) = pseudo_mod f g
[PROOF STEP]
define r where "r = pseudo_mod f g"
[PROOF STATE]
proof (state)
this:
r = pseudo_mod f g

goal (1 subgoal):
 1. smult (lead_coeff g ^ (Suc (degree f) - degree g)) (f mod g) = pseudo_mod f g
[PROOF STEP]
define r' where "r' = pseudo_mod (smult (1/a) f) g"
[PROOF STATE]
proof (state)
this:
r' = pseudo_mod (smult ((1::'a) / a) f) g

goal (1 subgoal):
 1. smult (lead_coeff g ^ (Suc (degree f) - degree g)) (f mod g) = pseudo_mod f g
[PROOF STEP]
obtain q where pdm: "pseudo_divmod f g = (q,r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>q. pseudo_divmod f g = (q, r) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using r_def[unfolded pseudo_mod_def]
[PROOF STATE]
proof (prove)
using this:
r = snd (pseudo_divmod f g)

goal (1 subgoal):
 1. (\<And>q. pseudo_divmod f g = (q, r) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply (cases "pseudo_divmod f g")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<And>q. pseudo_divmod f g = (q, r) \<Longrightarrow> thesis; r = snd (pseudo_divmod f g); pseudo_divmod f g = (a, b)\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pseudo_divmod f g = (q, r)

goal (1 subgoal):
 1. smult (lead_coeff g ^ (Suc (degree f) - degree g)) (f mod g) = pseudo_mod f g
[PROOF STEP]
obtain q' where pdm': "pseudo_divmod (smult (1/a) f) g = (q',r')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>q'. pseudo_divmod (smult ((1::'a) / a) f) g = (q', r') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using r'_def[unfolded pseudo_mod_def]
[PROOF STATE]
proof (prove)
using this:
r' = snd (pseudo_divmod (smult ((1::'a) / a) f) g)

goal (1 subgoal):
 1. (\<And>q'. pseudo_divmod (smult ((1::'a) / a) f) g = (q', r') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply (cases "pseudo_divmod (smult (1/a) f) g")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa b. \<lbrakk>\<And>q'. pseudo_divmod (smult ((1::'a) / a) f) g = (q', r') \<Longrightarrow> thesis; r' = snd (pseudo_divmod (smult ((1::'a) / a) f) g); pseudo_divmod (smult ((1::'a) / a) f) g = (aa, b)\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pseudo_divmod (smult ((1::'a) / a) f) g = (q', r')

goal (1 subgoal):
 1. smult (lead_coeff g ^ (Suc (degree f) - degree g)) (f mod g) = pseudo_mod f g
[PROOF STEP]
have "smult a f = q * g + r" and deg_r:"r = 0 \<or> degree r < degree g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. smult a f = q * g + r &&& r = 0 \<or> degree r < degree g
[PROOF STEP]
using pseudo_divmod[OF assms pdm]
[PROOF STATE]
proof (prove)
using this:
smult (lead_coeff g ^ (Suc (degree f) - degree g)) f = g * q + r
r = 0 \<or> degree r < degree g

goal (1 subgoal):
 1. smult a f = q * g + r &&& r = 0 \<or> degree r < degree g
[PROOF STEP]
unfolding a_def
[PROOF STATE]
proof (prove)
using this:
smult (lead_coeff g ^ (Suc (degree f) - degree g)) f = g * q + r
r = 0 \<or> degree r < degree g

goal (1 subgoal):
 1. smult (lead_coeff g ^ (Suc (degree f) - degree g)) f = q * g + r &&& r = 0 \<or> degree r < degree g
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
smult a f = q * g + r
r = 0 \<or> degree r < degree g

goal (1 subgoal):
 1. smult (lead_coeff g ^ (Suc (degree f) - degree g)) (f mod g) = pseudo_mod f g
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
smult a f = q * g + r
r = 0 \<or> degree r < degree g

goal (1 subgoal):
 1. smult (lead_coeff g ^ (Suc (degree f) - degree g)) (f mod g) = pseudo_mod f g
[PROOF STEP]
have "f = q' * g + r'" and deg_r':"r' = 0 \<or> degree r' < degree g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f = q' * g + r' &&& r' = 0 \<or> degree r' < degree g
[PROOF STEP]
using \<open>a\<noteq>0\<close>  pseudo_divmod[OF assms pdm']
[PROOF STATE]
proof (prove)
using this:
a \<noteq> (0::'a)
smult (lead_coeff g ^ (Suc (degree (smult ((1::'a) / a) f)) - degree g)) (smult ((1::'a) / a) f) = g * q' + r'
r' = 0 \<or> degree r' < degree g

goal (1 subgoal):
 1. f = q' * g + r' &&& r' = 0 \<or> degree r' < degree g
[PROOF STEP]
unfolding a_def degree_smult_eq
[PROOF STATE]
proof (prove)
using this:
lead_coeff g ^ (Suc (degree f) - degree g) \<noteq> (0::'a)
smult (lead_coeff g ^ (Suc (if (1::'a) / lead_coeff g ^ (Suc (degree f) - degree g) = (0::'a) then 0 else degree f) - degree g)) (smult ((1::'a) / lead_coeff g ^ (Suc (degree f) - degree g)) f) = g * q' + r'
r' = 0 \<or> degree r' < degree g

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

goal (1 subgoal):
 1. smult (lead_coeff g ^ (Suc (degree f) - degree g)) (f mod g) = pseudo_mod f g
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
smult a f = q * g + r
r = 0 \<or> degree r < degree g
f = q' * g + r'
r' = 0 \<or> degree r' < degree g
[PROOF STEP]
have gr:"(smult a q' - q) * g =  r - smult a r'"
[PROOF STATE]
proof (prove)
using this:
smult a f = q * g + r
r = 0 \<or> degree r < degree g
f = q' * g + r'
r' = 0 \<or> degree r' < degree g

goal (1 subgoal):
 1. (smult a q' - q) * g = r - smult a r'
[PROOF STEP]
by (auto simp add:smult_add_right algebra_simps)
[PROOF STATE]
proof (state)
this:
(smult a q' - q) * g = r - smult a r'

goal (1 subgoal):
 1. smult (lead_coeff g ^ (Suc (degree f) - degree g)) (f mod g) = pseudo_mod f g
[PROOF STEP]
have "smult a r' = r" when "r=0" "r'=0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. smult a r' = r
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
r = 0
r' = 0

goal (1 subgoal):
 1. smult a r' = r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>r = 0; r' = 0\<rbrakk> \<Longrightarrow> smult a r' = r

goal (1 subgoal):
 1. smult (lead_coeff g ^ (Suc (degree f) - degree g)) (f mod g) = pseudo_mod f g
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>r = 0; r' = 0\<rbrakk> \<Longrightarrow> smult a r' = r

goal (1 subgoal):
 1. smult (lead_coeff g ^ (Suc (degree f) - degree g)) (f mod g) = pseudo_mod f g
[PROOF STEP]
have "smult a r' = r" when "r\<noteq>0 \<or> r'\<noteq>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. smult a r' = r
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. smult a r' = r
[PROOF STEP]
have "smult a q' - q =0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. smult a q' - q = 0
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. smult a q' - q \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
assume asm:"smult a q' - q \<noteq> 0 "
[PROOF STATE]
proof (state)
this:
smult a q' - q \<noteq> 0

goal (1 subgoal):
 1. smult a q' - q \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
have "degree (r - smult a r') < degree g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (r - smult a r') < degree g
[PROOF STEP]
using deg_r deg_r' degree_diff_less that
[PROOF STATE]
proof (prove)
using this:
r = 0 \<or> degree r < degree g
r' = 0 \<or> degree r' < degree g
\<lbrakk>degree ?p < ?n; degree ?q < ?n\<rbrakk> \<Longrightarrow> degree (?p - ?q) < ?n
r \<noteq> 0 \<or> r' \<noteq> 0

goal (1 subgoal):
 1. degree (r - smult a r') < degree g
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
degree (r - smult a r') < degree g

goal (1 subgoal):
 1. smult a q' - q \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
degree (r - smult a r') < degree g

goal (1 subgoal):
 1. smult a q' - q \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
have "... \<le> degree (( smult a q' - q)*g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree g \<le> degree ((smult a q' - q) * g)
[PROOF STEP]
using degree_mult_right_le[OF asm,of g]
[PROOF STATE]
proof (prove)
using this:
degree g \<le> degree (g * (smult a q' - q))

goal (1 subgoal):
 1. degree g \<le> degree ((smult a q' - q) * g)
[PROOF STEP]
by (simp add: mult.commute)
[PROOF STATE]
proof (state)
this:
degree g \<le> degree ((smult a q' - q) * g)

goal (1 subgoal):
 1. smult a q' - q \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
degree g \<le> degree ((smult a q' - q) * g)

goal (1 subgoal):
 1. smult a q' - q \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
have "... = degree (r - smult a r')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree ((smult a q' - q) * g) = degree (r - smult a r')
[PROOF STEP]
using gr
[PROOF STATE]
proof (prove)
using this:
(smult a q' - q) * g = r - smult a r'

goal (1 subgoal):
 1. degree ((smult a q' - q) * g) = degree (r - smult a r')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
degree ((smult a q' - q) * g) = degree (r - smult a r')

goal (1 subgoal):
 1. smult a q' - q \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
degree (r - smult a r') < degree (r - smult a r')
[PROOF STEP]
have "degree (r - smult a r') < degree (r - smult a r')"
[PROOF STATE]
proof (prove)
using this:
degree (r - smult a r') < degree (r - smult a r')

goal (1 subgoal):
 1. degree (r - smult a r') < degree (r - smult a r')
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
degree (r - smult a r') < degree (r - smult a r')

goal (1 subgoal):
 1. smult a q' - q \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
degree (r - smult a r') < degree (r - smult a r')
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
degree (r - smult a r') < degree (r - smult a r')

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
smult a q' - q = 0

goal (1 subgoal):
 1. smult a r' = r
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
smult a q' - q = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
smult a q' - q = 0

goal (1 subgoal):
 1. smult a r' = r
[PROOF STEP]
using gr
[PROOF STATE]
proof (prove)
using this:
smult a q' - q = 0
(smult a q' - q) * g = r - smult a r'

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
r \<noteq> 0 \<or> r' \<noteq> 0 \<Longrightarrow> smult a r' = r

goal (1 subgoal):
 1. smult (lead_coeff g ^ (Suc (degree f) - degree g)) (f mod g) = pseudo_mod f g
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>r = 0; r' = 0\<rbrakk> \<Longrightarrow> smult a r' = r
r \<noteq> 0 \<or> r' \<noteq> 0 \<Longrightarrow> smult a r' = r
[PROOF STEP]
have "smult a r' = r"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>r = 0; r' = 0\<rbrakk> \<Longrightarrow> smult a r' = r
r \<noteq> 0 \<or> r' \<noteq> 0 \<Longrightarrow> smult a r' = r

goal (1 subgoal):
 1. smult a r' = r
[PROOF STEP]
by argo
[PROOF STATE]
proof (state)
this:
smult a r' = r

goal (1 subgoal):
 1. smult (lead_coeff g ^ (Suc (degree f) - degree g)) (f mod g) = pseudo_mod f g
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
smult a r' = r
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
smult a r' = r

goal (1 subgoal):
 1. smult (lead_coeff g ^ (Suc (degree f) - degree g)) (f mod g) = pseudo_mod f g
[PROOF STEP]
unfolding r_def r'_def a_def mod_poly_def
[PROOF STATE]
proof (prove)
using this:
smult (lead_coeff g ^ (Suc (degree f) - degree g)) (pseudo_mod (smult ((1::'a) / lead_coeff g ^ (Suc (degree f) - degree g)) f) g) = pseudo_mod f g

goal (1 subgoal):
 1. smult (lead_coeff g ^ (Suc (degree f) - degree g)) (if g = 0 then f else pseudo_mod (smult (((1::'a) / lead_coeff g) ^ (Suc (degree f) - degree g)) f) g) = pseudo_mod f g
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
smult (lead_coeff g ^ (Suc (degree f) - degree g)) (pseudo_mod (smult ((1::'a) / lead_coeff g ^ (Suc (degree f) - degree g)) f) g) = pseudo_mod f g
g \<noteq> 0

goal (1 subgoal):
 1. smult (lead_coeff g ^ (Suc (degree f) - degree g)) (if g = 0 then f else pseudo_mod (smult (((1::'a) / lead_coeff g) ^ (Suc (degree f) - degree g)) f) g) = pseudo_mod f g
[PROOF STEP]
by (auto simp add:field_simps)
[PROOF STATE]
proof (state)
this:
smult (lead_coeff g ^ (Suc (degree f) - degree g)) (f mod g) = pseudo_mod f g

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma poly_pseudo_mod:
  assumes "poly q x=0" "q\<noteq>0"
  shows "poly (pseudo_mod p q) x = (lead_coeff q ^ (Suc (degree p) - degree q)) * poly p x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly (pseudo_mod p q) x = lead_coeff q ^ (Suc (degree p) - degree q) * poly p x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. poly (pseudo_mod p q) x = lead_coeff q ^ (Suc (degree p) - degree q) * poly p x
[PROOF STEP]
define a where "a=coeff q (degree q) ^ (Suc (degree p) - degree q)"
[PROOF STATE]
proof (state)
this:
a = lead_coeff q ^ (Suc (degree p) - degree q)

goal (1 subgoal):
 1. poly (pseudo_mod p q) x = lead_coeff q ^ (Suc (degree p) - degree q) * poly p x
[PROOF STEP]
obtain f r where fr:"pseudo_divmod p q = (f, r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>f r. pseudo_divmod p q = (f, r) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
pseudo_divmod p q = (f, r)

goal (1 subgoal):
 1. poly (pseudo_mod p q) x = lead_coeff q ^ (Suc (degree p) - degree q) * poly p x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pseudo_divmod p q = (f, r)
[PROOF STEP]
have "smult a p = q * f + r" "r = 0 \<or> degree r < degree q"
[PROOF STATE]
proof (prove)
using this:
pseudo_divmod p q = (f, r)

goal (1 subgoal):
 1. smult a p = q * f + r &&& r = 0 \<or> degree r < degree q
[PROOF STEP]
using pseudo_divmod[OF \<open>q\<noteq>0\<close>]
[PROOF STATE]
proof (prove)
using this:
pseudo_divmod p q = (f, r)
pseudo_divmod ?f q = (?q, ?r) \<Longrightarrow> smult (lead_coeff q ^ (Suc (degree ?f) - degree q)) ?f = q * ?q + ?r
pseudo_divmod ?f q = (?q, ?r) \<Longrightarrow> ?r = 0 \<or> degree ?r < degree q

goal (1 subgoal):
 1. smult a p = q * f + r &&& r = 0 \<or> degree r < degree q
[PROOF STEP]
unfolding a_def
[PROOF STATE]
proof (prove)
using this:
pseudo_divmod p q = (f, r)
pseudo_divmod ?f q = (?q, ?r) \<Longrightarrow> smult (lead_coeff q ^ (Suc (degree ?f) - degree q)) ?f = q * ?q + ?r
pseudo_divmod ?f q = (?q, ?r) \<Longrightarrow> ?r = 0 \<or> degree ?r < degree q

goal (1 subgoal):
 1. smult (lead_coeff q ^ (Suc (degree p) - degree q)) p = q * f + r &&& r = 0 \<or> degree r < degree q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
smult a p = q * f + r
r = 0 \<or> degree r < degree q

goal (1 subgoal):
 1. poly (pseudo_mod p q) x = lead_coeff q ^ (Suc (degree p) - degree q) * poly p x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
smult a p = q * f + r
r = 0 \<or> degree r < degree q
[PROOF STEP]
have "poly (q*f+r) x = poly (smult a p) x"
[PROOF STATE]
proof (prove)
using this:
smult a p = q * f + r
r = 0 \<or> degree r < degree q

goal (1 subgoal):
 1. poly (q * f + r) x = poly (smult a p) x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
poly (q * f + r) x = poly (smult a p) x

goal (1 subgoal):
 1. poly (pseudo_mod p q) x = lead_coeff q ^ (Suc (degree p) - degree q) * poly p x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
poly (q * f + r) x = poly (smult a p) x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
poly (q * f + r) x = poly (smult a p) x

goal (1 subgoal):
 1. poly (pseudo_mod p q) x = lead_coeff q ^ (Suc (degree p) - degree q) * poly p x
[PROOF STEP]
using assms(1) fr
[PROOF STATE]
proof (prove)
using this:
poly (q * f + r) x = poly (smult a p) x
poly q x = (0::'a)
pseudo_divmod p q = (f, r)

goal (1 subgoal):
 1. poly (pseudo_mod p q) x = lead_coeff q ^ (Suc (degree p) - degree q) * poly p x
[PROOF STEP]
unfolding pseudo_mod_def a_def
[PROOF STATE]
proof (prove)
using this:
poly (q * f + r) x = poly (smult (lead_coeff q ^ (Suc (degree p) - degree q)) p) x
poly q x = (0::'a)
pseudo_divmod p q = (f, r)

goal (1 subgoal):
 1. poly (snd (pseudo_divmod p q)) x = lead_coeff q ^ (Suc (degree p) - degree q) * poly p x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
poly (pseudo_mod p q) x = lead_coeff q ^ (Suc (degree p) - degree q) * poly p x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma degree_less_timesD:
  fixes q::"'a::idom poly"
  assumes "q*g=r" and deg:"r=0 \<or> degree g>degree r" and "g\<noteq>0"
  shows "q=0 \<and> r=0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q = 0 \<and> r = 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. q = 0 \<and> r = 0
[PROOF STEP]
have ?thesis when "r=0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q = 0 \<and> r = 0
[PROOF STEP]
using assms(1) assms(3) no_zero_divisors that
[PROOF STATE]
proof (prove)
using this:
q * g = r
g \<noteq> 0
\<lbrakk>?a \<noteq> (0::?'a); ?b \<noteq> (0::?'a)\<rbrakk> \<Longrightarrow> ?a * ?b \<noteq> (0::?'a)
r = 0

goal (1 subgoal):
 1. q = 0 \<and> r = 0
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
r = 0 \<Longrightarrow> q = 0 \<and> r = 0

goal (1 subgoal):
 1. q = 0 \<and> r = 0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
r = 0 \<Longrightarrow> q = 0 \<and> r = 0

goal (1 subgoal):
 1. q = 0 \<and> r = 0
[PROOF STEP]
have False when "r\<noteq>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. False
[PROOF STEP]
have "degree r < degree g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree r < degree g
[PROOF STEP]
using deg that
[PROOF STATE]
proof (prove)
using this:
r = 0 \<or> degree r < degree g
r \<noteq> 0

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

goal (1 subgoal):
 1. False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
degree r < degree g

goal (1 subgoal):
 1. False
[PROOF STEP]
have "... \<le> degree (q*g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree g \<le> degree (q * g)
[PROOF STEP]
by (metis assms(1) degree_mult_right_le mult.commute mult_not_zero that)
[PROOF STATE]
proof (state)
this:
degree g \<le> degree (q * g)

goal (1 subgoal):
 1. False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
degree g \<le> degree (q * g)

goal (1 subgoal):
 1. False
[PROOF STEP]
have "... = degree r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (q * g) = degree r
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
q * g = r

goal (1 subgoal):
 1. degree (q * g) = degree r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
degree (q * g) = degree r

goal (1 subgoal):
 1. False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
degree r < degree r
[PROOF STEP]
have "degree r<degree r"
[PROOF STATE]
proof (prove)
using this:
degree r < degree r

goal (1 subgoal):
 1. degree r < degree r
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
degree r < degree r

goal (1 subgoal):
 1. False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
degree r < degree r
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
degree r < degree r

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:
r \<noteq> 0 \<Longrightarrow> False

goal (1 subgoal):
 1. q = 0 \<and> r = 0
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
r = 0 \<Longrightarrow> q = 0 \<and> r = 0
r \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
r = 0 \<Longrightarrow> q = 0 \<and> r = 0
r \<noteq> 0 \<Longrightarrow> False

goal (1 subgoal):
 1. q = 0 \<and> r = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
q = 0 \<and> r = 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_element_ptr_ref [simp]: "is_element_ptr (element_ptr.Ref n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_element_ptr (Ref n)
[PROOF STEP]
by(simp add: is_element_ptr\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def)


[STATEMENT]
lemma element_ptr_casts_commute [simp]:
  "cast\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r node_ptr = Some element_ptr \<longleftrightarrow> cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r element_ptr = node_ptr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cast node_ptr = Some element_ptr) = (cast element_ptr = node_ptr)
[PROOF STEP]
unfolding cast\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((case node_ptr of node_ptr.Ext (Inl xa) \<Rightarrow> Some xa | node_ptr.Ext (Inr xa) \<Rightarrow> Map.empty xa) = Some element_ptr) = (node_ptr.Ext (Inl element_ptr) = node_ptr)
[PROOF STEP]
by(auto split: node_ptr.splits sum.splits)


[STATEMENT]
lemma element_ptr_casts_commute2 [simp]:
  "(cast\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r (cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r element_ptr) = Some element_ptr)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cast (cast element_ptr) = Some element_ptr
[PROOF STEP]
by simp


[STATEMENT]
lemma element_ptr_casts_commute3 [simp]:
  assumes "is_element_ptr_kind\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r node_ptr"
  shows "cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r (the (cast\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r node_ptr)) = node_ptr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cast (the (cast node_ptr)) = node_ptr
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_element_ptr_kind node_ptr

goal (1 subgoal):
 1. cast (the (cast node_ptr)) = node_ptr
[PROOF STEP]
by(auto simp add: is_element_ptr_kind_def cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def cast\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def
      split: node_ptr.splits sum.splits)


[STATEMENT]
lemma is_element_ptr_kind_obtains:
  assumes "is_element_ptr_kind node_ptr"
  obtains element_ptr where "node_ptr = cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r element_ptr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>element_ptr. node_ptr = cast element_ptr \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis assms is_element_ptr_kind_def case_optionE element_ptr_casts_commute)


[STATEMENT]
lemma is_element_ptr_kind_none:
  assumes "\<not>is_element_ptr_kind node_ptr"
  shows "cast\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r node_ptr = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cast node_ptr = None
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<not> is_element_ptr_kind node_ptr

goal (1 subgoal):
 1. cast node_ptr = None
[PROOF STEP]
unfolding is_element_ptr_kind_def cast\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def
[PROOF STATE]
proof (prove)
using this:
\<not> (case case node_ptr of node_ptr.Ext (Inl xa) \<Rightarrow> Some xa | node_ptr.Ext (Inr xa) \<Rightarrow> Map.empty xa of None \<Rightarrow> False | Some x \<Rightarrow> True)

goal (1 subgoal):
 1. (case node_ptr of node_ptr.Ext (Inl xa) \<Rightarrow> Some xa | node_ptr.Ext (Inr xa) \<Rightarrow> Map.empty xa) = None
[PROOF STEP]
by(auto split: node_ptr.splits sum.splits)


[STATEMENT]
lemma is_element_ptr_kind_cast [simp]:
  "is_element_ptr_kind (cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r element_ptr)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_element_ptr_kind (cast element_ptr)
[PROOF STEP]
by (metis element_ptr_casts_commute is_element_ptr_kind_none option.distinct(1))


[STATEMENT]
lemma cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r_inject [simp]:
  "cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r x = cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r y \<longleftrightarrow> x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cast x = cast y) = (x = y)
[PROOF STEP]
by(simp add: cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def)


[STATEMENT]
lemma cast\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_ext_none [simp]:
  "cast\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r (node_ptr.Ext (Inr (Inr node_ext_ptr))) = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cast (node_ptr.Ext (Inr (Inr node_ext_ptr))) = None
[PROOF STEP]
by(simp add: cast\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def)


[STATEMENT]
lemma is_element_ptr_implies_kind [dest]: "is_element_ptr\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r ptr \<Longrightarrow> is_element_ptr_kind\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r ptr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. case cast ptr of None \<Rightarrow> False | Some element_ptr \<Rightarrow> is_element_ptr element_ptr \<Longrightarrow> is_element_ptr_kind ptr
[PROOF STEP]
by(auto split: option.splits)


[STATEMENT]
lemma DynPDG_empty_path_eq_nodes:"n -[]\<rightarrow>\<^sub>d* n' \<Longrightarrow> n = n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n -[]\<rightarrow>\<^sub>d* n' \<Longrightarrow> n = n'
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n -[]\<rightarrow>\<^sub>d* n' \<Longrightarrow> n = n'
[PROOF STEP]
apply(erule DynPDG_path.cases)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>na. \<lbrakk>n = na; [] = []; n' = na; valid_node na\<rbrakk> \<Longrightarrow> n = n'
 2. \<And>na as n'' as' n'a. \<lbrakk>n = na; [] = as @ as'; n' = n'a; na -as\<rightarrow>\<^sub>d* n''; n'' -as'\<rightarrow>\<^sub>c\<^sub>d n'a\<rbrakk> \<Longrightarrow> n = n'
 3. \<And>na as n'' V as' n'a. \<lbrakk>n = na; [] = as @ as'; n' = n'a; na -as\<rightarrow>\<^sub>d* n''; n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'a\<rbrakk> \<Longrightarrow> n = n'
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>na as n'' as' n'a. \<lbrakk>n = na; [] = as @ as'; n' = n'a; na -as\<rightarrow>\<^sub>d* n''; n'' -as'\<rightarrow>\<^sub>c\<^sub>d n'a\<rbrakk> \<Longrightarrow> n = n'
 2. \<And>na as n'' V as' n'a. \<lbrakk>n = na; [] = as @ as'; n' = n'a; na -as\<rightarrow>\<^sub>d* n''; n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'a\<rbrakk> \<Longrightarrow> n = n'
[PROOF STEP]
apply(auto elim:DynPDG_edge.cases dest:dyn_control_dependence_path)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n'' V. \<lbrakk>n -[]\<rightarrow>\<^sub>d* n''; n'' -{V}[]\<rightarrow>\<^sub>d\<^sub>d n'\<rbrakk> \<Longrightarrow> n = n'
[PROOF STEP]
by(auto elim:DynPDG_edge.cases simp:dyn_data_dependence_def)


[STATEMENT]
lemma DynPDG_path_cdep:"n -as\<rightarrow>\<^sub>c\<^sub>d n' \<Longrightarrow> n -as\<rightarrow>\<^sub>d* n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n -as\<rightarrow>\<^sub>c\<^sub>d n' \<Longrightarrow> n -as\<rightarrow>\<^sub>d* n'
[PROOF STEP]
apply(subgoal_tac "n -[]@as\<rightarrow>\<^sub>d* n'")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n -as\<rightarrow>\<^sub>c\<^sub>d n'; n -[] @ as\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> n -as\<rightarrow>\<^sub>d* n'
 2. n -as\<rightarrow>\<^sub>c\<^sub>d n' \<Longrightarrow> n -[] @ as\<rightarrow>\<^sub>d* n'
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n -as\<rightarrow>\<^sub>c\<^sub>d n' \<Longrightarrow> n -[] @ as\<rightarrow>\<^sub>d* n'
[PROOF STEP]
apply(rule DynPDG_path_Append_cdep, rule DynPDG_path_Nil)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. n -as\<rightarrow>\<^sub>c\<^sub>d n' \<Longrightarrow> valid_node n
 2. n -as\<rightarrow>\<^sub>c\<^sub>d n' \<Longrightarrow> n -as\<rightarrow>\<^sub>c\<^sub>d n'
[PROOF STEP]
by(auto elim!:DynPDG_edge.cases dest:dyn_control_dependence_path path_valid_node)


[STATEMENT]
lemma DynPDG_path_ddep:"n -{V}as\<rightarrow>\<^sub>d\<^sub>d n' \<Longrightarrow> n -as\<rightarrow>\<^sub>d* n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n -{V}as\<rightarrow>\<^sub>d\<^sub>d n' \<Longrightarrow> n -as\<rightarrow>\<^sub>d* n'
[PROOF STEP]
apply(subgoal_tac "n -[]@as\<rightarrow>\<^sub>d* n'")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n -{V}as\<rightarrow>\<^sub>d\<^sub>d n'; n -[] @ as\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> n -as\<rightarrow>\<^sub>d* n'
 2. n -{V}as\<rightarrow>\<^sub>d\<^sub>d n' \<Longrightarrow> n -[] @ as\<rightarrow>\<^sub>d* n'
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n -{V}as\<rightarrow>\<^sub>d\<^sub>d n' \<Longrightarrow> n -[] @ as\<rightarrow>\<^sub>d* n'
[PROOF STEP]
apply(rule DynPDG_path_Append_ddep, rule DynPDG_path_Nil)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. n -{V}as\<rightarrow>\<^sub>d\<^sub>d n' \<Longrightarrow> valid_node n
 2. n -{V}as\<rightarrow>\<^sub>d\<^sub>d n' \<Longrightarrow> n -{?V1}as\<rightarrow>\<^sub>d\<^sub>d n'
[PROOF STEP]
by(auto elim!:DynPDG_edge.cases dest:path_valid_node simp:dyn_data_dependence_def)


[STATEMENT]
lemma DynPDG_path_Append:
  "\<lbrakk>n'' -as'\<rightarrow>\<^sub>d* n'; n -as\<rightarrow>\<^sub>d* n''\<rbrakk> \<Longrightarrow> n -as@as'\<rightarrow>\<^sub>d* n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n'' -as'\<rightarrow>\<^sub>d* n'; n -as\<rightarrow>\<^sub>d* n''\<rbrakk> \<Longrightarrow> n -as @ as'\<rightarrow>\<^sub>d* n'
[PROOF STEP]
apply(induct rule:DynPDG_path.induct)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>na. \<lbrakk>valid_node na; n -as\<rightarrow>\<^sub>d* na\<rbrakk> \<Longrightarrow> n -as @ []\<rightarrow>\<^sub>d* na
 2. \<And>na asa n'' as' n'. \<lbrakk>na -asa\<rightarrow>\<^sub>d* n''; n -as\<rightarrow>\<^sub>d* na \<Longrightarrow> n -as @ asa\<rightarrow>\<^sub>d* n''; n'' -as'\<rightarrow>\<^sub>c\<^sub>d n'; n -as\<rightarrow>\<^sub>d* na\<rbrakk> \<Longrightarrow> n -as @ asa @ as'\<rightarrow>\<^sub>d* n'
 3. \<And>na asa n'' V as' n'. \<lbrakk>na -asa\<rightarrow>\<^sub>d* n''; n -as\<rightarrow>\<^sub>d* na \<Longrightarrow> n -as @ asa\<rightarrow>\<^sub>d* n''; n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'; n -as\<rightarrow>\<^sub>d* na\<rbrakk> \<Longrightarrow> n -as @ asa @ as'\<rightarrow>\<^sub>d* n'
[PROOF STEP]
apply(auto intro:DynPDG_path.intros)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>na asa n'' as' n'. \<lbrakk>na -asa\<rightarrow>\<^sub>d* n''; n -as @ asa\<rightarrow>\<^sub>d* n''; n'' -as'\<rightarrow>\<^sub>c\<^sub>d n'; n -as\<rightarrow>\<^sub>d* na\<rbrakk> \<Longrightarrow> n -as @ asa @ as'\<rightarrow>\<^sub>d* n'
 2. \<And>na asa n'' V as' n'. \<lbrakk>na -asa\<rightarrow>\<^sub>d* n''; n -as @ asa\<rightarrow>\<^sub>d* n''; n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'; n -as\<rightarrow>\<^sub>d* na\<rbrakk> \<Longrightarrow> n -as @ asa @ as'\<rightarrow>\<^sub>d* n'
[PROOF STEP]
apply(rotate_tac 1,drule DynPDG_path_Append_cdep,simp+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>na asa n'' V as' n'. \<lbrakk>na -asa\<rightarrow>\<^sub>d* n''; n -as @ asa\<rightarrow>\<^sub>d* n''; n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'; n -as\<rightarrow>\<^sub>d* na\<rbrakk> \<Longrightarrow> n -as @ asa @ as'\<rightarrow>\<^sub>d* n'
[PROOF STEP]
apply(rotate_tac 1,drule DynPDG_path_Append_ddep,simp+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma DynPDG_path_Exit:"\<lbrakk>n -as\<rightarrow>\<^sub>d* n'; n' = (_Exit_)\<rbrakk> \<Longrightarrow> n = (_Exit_)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n -as\<rightarrow>\<^sub>d* n'; n' = (_Exit_)\<rbrakk> \<Longrightarrow> n = (_Exit_)
[PROOF STEP]
apply(induct rule:DynPDG_path.induct)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n. \<lbrakk>valid_node n; n = (_Exit_)\<rbrakk> \<Longrightarrow> n = (_Exit_)
 2. \<And>n as n'' as' n'. \<lbrakk>n -as\<rightarrow>\<^sub>d* n''; n'' = (_Exit_) \<Longrightarrow> n = (_Exit_); n'' -as'\<rightarrow>\<^sub>c\<^sub>d n'; n' = (_Exit_)\<rbrakk> \<Longrightarrow> n = (_Exit_)
 3. \<And>n as n'' V as' n'. \<lbrakk>n -as\<rightarrow>\<^sub>d* n''; n'' = (_Exit_) \<Longrightarrow> n = (_Exit_); n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'; n' = (_Exit_)\<rbrakk> \<Longrightarrow> n = (_Exit_)
[PROOF STEP]
by(auto elim:DynPDG_edge.cases dest:Exit_not_dyn_control_dependent
        simp:dyn_data_dependence_def)


[STATEMENT]
lemma DynPDG_path_not_inner:
  "\<lbrakk>n -as\<rightarrow>\<^sub>d* n'; \<not> inner_node n'\<rbrakk> \<Longrightarrow> n = n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n -as\<rightarrow>\<^sub>d* n'; \<not> inner_node n'\<rbrakk> \<Longrightarrow> n = n'
[PROOF STEP]
proof(induct rule:DynPDG_path.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>n. \<lbrakk>valid_node n; \<not> inner_node n\<rbrakk> \<Longrightarrow> n = n
 2. \<And>n as n'' as' n'. \<lbrakk>n -as\<rightarrow>\<^sub>d* n''; \<not> inner_node n'' \<Longrightarrow> n = n''; n'' -as'\<rightarrow>\<^sub>c\<^sub>d n'; \<not> inner_node n'\<rbrakk> \<Longrightarrow> n = n'
 3. \<And>n as n'' V as' n'. \<lbrakk>n -as\<rightarrow>\<^sub>d* n''; \<not> inner_node n'' \<Longrightarrow> n = n''; n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'; \<not> inner_node n'\<rbrakk> \<Longrightarrow> n = n'
[PROOF STEP]
case (DynPDG_path_Nil n)
[PROOF STATE]
proof (state)
this:
valid_node n
\<not> inner_node n

goal (3 subgoals):
 1. \<And>n. \<lbrakk>valid_node n; \<not> inner_node n\<rbrakk> \<Longrightarrow> n = n
 2. \<And>n as n'' as' n'. \<lbrakk>n -as\<rightarrow>\<^sub>d* n''; \<not> inner_node n'' \<Longrightarrow> n = n''; n'' -as'\<rightarrow>\<^sub>c\<^sub>d n'; \<not> inner_node n'\<rbrakk> \<Longrightarrow> n = n'
 3. \<And>n as n'' V as' n'. \<lbrakk>n -as\<rightarrow>\<^sub>d* n''; \<not> inner_node n'' \<Longrightarrow> n = n''; n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'; \<not> inner_node n'\<rbrakk> \<Longrightarrow> n = n'
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
valid_node n
\<not> inner_node n

goal (1 subgoal):
 1. n = n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n = n

goal (2 subgoals):
 1. \<And>n as n'' as' n'. \<lbrakk>n -as\<rightarrow>\<^sub>d* n''; \<not> inner_node n'' \<Longrightarrow> n = n''; n'' -as'\<rightarrow>\<^sub>c\<^sub>d n'; \<not> inner_node n'\<rbrakk> \<Longrightarrow> n = n'
 2. \<And>n as n'' V as' n'. \<lbrakk>n -as\<rightarrow>\<^sub>d* n''; \<not> inner_node n'' \<Longrightarrow> n = n''; n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'; \<not> inner_node n'\<rbrakk> \<Longrightarrow> n = n'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n as n'' as' n'. \<lbrakk>n -as\<rightarrow>\<^sub>d* n''; \<not> inner_node n'' \<Longrightarrow> n = n''; n'' -as'\<rightarrow>\<^sub>c\<^sub>d n'; \<not> inner_node n'\<rbrakk> \<Longrightarrow> n = n'
 2. \<And>n as n'' V as' n'. \<lbrakk>n -as\<rightarrow>\<^sub>d* n''; \<not> inner_node n'' \<Longrightarrow> n = n''; n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'; \<not> inner_node n'\<rbrakk> \<Longrightarrow> n = n'
[PROOF STEP]
case (DynPDG_path_Append_cdep n as n'' as' n')
[PROOF STATE]
proof (state)
this:
n -as\<rightarrow>\<^sub>d* n''
\<not> inner_node n'' \<Longrightarrow> n = n''
n'' -as'\<rightarrow>\<^sub>c\<^sub>d n'
\<not> inner_node n'

goal (2 subgoals):
 1. \<And>n as n'' as' n'. \<lbrakk>n -as\<rightarrow>\<^sub>d* n''; \<not> inner_node n'' \<Longrightarrow> n = n''; n'' -as'\<rightarrow>\<^sub>c\<^sub>d n'; \<not> inner_node n'\<rbrakk> \<Longrightarrow> n = n'
 2. \<And>n as n'' V as' n'. \<lbrakk>n -as\<rightarrow>\<^sub>d* n''; \<not> inner_node n'' \<Longrightarrow> n = n''; n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'; \<not> inner_node n'\<rbrakk> \<Longrightarrow> n = n'
[PROOF STEP]
from \<open>n'' -as'\<rightarrow>\<^sub>c\<^sub>d n'\<close> \<open>\<not> inner_node n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n'' -as'\<rightarrow>\<^sub>c\<^sub>d n'
\<not> inner_node n'
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
n'' -as'\<rightarrow>\<^sub>c\<^sub>d n'
\<not> inner_node n'

goal (1 subgoal):
 1. False
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n'' -as'\<rightarrow>\<^sub>c\<^sub>d n'; \<not> inner_node n'\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(erule DynPDG_edge.cases)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n n' as. \<lbrakk>\<not> inner_node n'; n'' = n; None = None; as' = as; n' = n'; n controls n' via as\<rbrakk> \<Longrightarrow> False
 2. \<And>n V n' as. \<lbrakk>\<not> inner_node n'; n'' = n; None = Some V; as' = as; n' = n'; n influences V in n' via as\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(auto simp:inner_node_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>n'' controls n' via as'; \<not> valid_node n'\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>n'' controls (_Entry_) via as'; n' = (_Entry_)\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>n'' controls (_Exit_) via as'; n' = (_Exit_)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(fastforce dest:dyn_control_dependence_path path_valid_node)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n'' controls (_Entry_) via as'; n' = (_Entry_)\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>n'' controls (_Exit_) via as'; n' = (_Exit_)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(fastforce dest:dyn_control_dependence_path path_valid_node)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n'' controls (_Exit_) via as'; n' = (_Exit_)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by(fastforce dest:Exit_not_dyn_control_dependent)
[PROOF STATE]
proof (state)
this:
False

goal (2 subgoals):
 1. \<And>n as n'' as' n'. \<lbrakk>n -as\<rightarrow>\<^sub>d* n''; \<not> inner_node n'' \<Longrightarrow> n = n''; n'' -as'\<rightarrow>\<^sub>c\<^sub>d n'; \<not> inner_node n'\<rbrakk> \<Longrightarrow> n = n'
 2. \<And>n as n'' V as' n'. \<lbrakk>n -as\<rightarrow>\<^sub>d* n''; \<not> inner_node n'' \<Longrightarrow> n = n''; n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'; \<not> inner_node n'\<rbrakk> \<Longrightarrow> n = n'
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
False

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

goal (1 subgoal):
 1. \<And>n as n'' V as' n'. \<lbrakk>n -as\<rightarrow>\<^sub>d* n''; \<not> inner_node n'' \<Longrightarrow> n = n''; n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'; \<not> inner_node n'\<rbrakk> \<Longrightarrow> n = n'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n as n'' V as' n'. \<lbrakk>n -as\<rightarrow>\<^sub>d* n''; \<not> inner_node n'' \<Longrightarrow> n = n''; n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'; \<not> inner_node n'\<rbrakk> \<Longrightarrow> n = n'
[PROOF STEP]
case (DynPDG_path_Append_ddep n as n'' V as' n')
[PROOF STATE]
proof (state)
this:
n -as\<rightarrow>\<^sub>d* n''
\<not> inner_node n'' \<Longrightarrow> n = n''
n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'
\<not> inner_node n'

goal (1 subgoal):
 1. \<And>n as n'' V as' n'. \<lbrakk>n -as\<rightarrow>\<^sub>d* n''; \<not> inner_node n'' \<Longrightarrow> n = n''; n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'; \<not> inner_node n'\<rbrakk> \<Longrightarrow> n = n'
[PROOF STEP]
from \<open>n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'\<close> \<open>\<not> inner_node n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'
\<not> inner_node n'
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'
\<not> inner_node n'

goal (1 subgoal):
 1. False
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'; \<not> inner_node n'\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(erule DynPDG_edge.cases)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n n' as. \<lbrakk>\<not> inner_node n'; n'' = n; Some V = None; as' = as; n' = n'; n controls n' via as\<rbrakk> \<Longrightarrow> False
 2. \<And>n Va n' as. \<lbrakk>\<not> inner_node n'; n'' = n; Some V = Some Va; as' = as; n' = n'; n influences Va in n' via as\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by(auto dest:path_valid_node simp:inner_node_def dyn_data_dependence_def)
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. \<And>n as n'' V as' n'. \<lbrakk>n -as\<rightarrow>\<^sub>d* n''; \<not> inner_node n'' \<Longrightarrow> n = n''; n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'; \<not> inner_node n'\<rbrakk> \<Longrightarrow> n = n'
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
False

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma DynPDG_cdep_edge_CFG_path:
  assumes "n -as\<rightarrow>\<^sub>c\<^sub>d n'" shows "n -as\<rightarrow>* n'" and "as \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n -as\<rightarrow>* n' &&& as \<noteq> []
[PROOF STEP]
using \<open>n -as\<rightarrow>\<^sub>c\<^sub>d n'\<close>
[PROOF STATE]
proof (prove)
using this:
n -as\<rightarrow>\<^sub>c\<^sub>d n'

goal (1 subgoal):
 1. n -as\<rightarrow>* n' &&& as \<noteq> []
[PROOF STEP]
by(auto elim:DynPDG_edge.cases dest:dyn_control_dependence_path)


[STATEMENT]
lemma DynPDG_ddep_edge_CFG_path:
  assumes "n -{V}as\<rightarrow>\<^sub>d\<^sub>d n'" shows "n -as\<rightarrow>* n'" and "as \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n -as\<rightarrow>* n' &&& as \<noteq> []
[PROOF STEP]
using \<open>n -{V}as\<rightarrow>\<^sub>d\<^sub>d n'\<close>
[PROOF STATE]
proof (prove)
using this:
n -{V}as\<rightarrow>\<^sub>d\<^sub>d n'

goal (1 subgoal):
 1. n -as\<rightarrow>* n' &&& as \<noteq> []
[PROOF STEP]
by(auto elim:DynPDG_edge.cases simp:dyn_data_dependence_def)


[STATEMENT]
lemma DynPDG_path_CFG_path:
  "n -as\<rightarrow>\<^sub>d* n' \<Longrightarrow> n -as\<rightarrow>* n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n -as\<rightarrow>\<^sub>d* n' \<Longrightarrow> n -as\<rightarrow>* n'
[PROOF STEP]
proof(induct rule:DynPDG_path.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>n. valid_node n \<Longrightarrow> n -[]\<rightarrow>* n
 2. \<And>n as n'' as' n'. \<lbrakk>n -as\<rightarrow>\<^sub>d* n''; n -as\<rightarrow>* n''; n'' -as'\<rightarrow>\<^sub>c\<^sub>d n'\<rbrakk> \<Longrightarrow> n -as @ as'\<rightarrow>* n'
 3. \<And>n as n'' V as' n'. \<lbrakk>n -as\<rightarrow>\<^sub>d* n''; n -as\<rightarrow>* n''; n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'\<rbrakk> \<Longrightarrow> n -as @ as'\<rightarrow>* n'
[PROOF STEP]
case DynPDG_path_Nil
[PROOF STATE]
proof (state)
this:
valid_node n_

goal (3 subgoals):
 1. \<And>n. valid_node n \<Longrightarrow> n -[]\<rightarrow>* n
 2. \<And>n as n'' as' n'. \<lbrakk>n -as\<rightarrow>\<^sub>d* n''; n -as\<rightarrow>* n''; n'' -as'\<rightarrow>\<^sub>c\<^sub>d n'\<rbrakk> \<Longrightarrow> n -as @ as'\<rightarrow>* n'
 3. \<And>n as n'' V as' n'. \<lbrakk>n -as\<rightarrow>\<^sub>d* n''; n -as\<rightarrow>* n''; n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'\<rbrakk> \<Longrightarrow> n -as @ as'\<rightarrow>* n'
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
valid_node n_

goal (1 subgoal):
 1. n_ -[]\<rightarrow>* n_
[PROOF STEP]
by(rule empty_path)
[PROOF STATE]
proof (state)
this:
n_ -[]\<rightarrow>* n_

goal (2 subgoals):
 1. \<And>n as n'' as' n'. \<lbrakk>n -as\<rightarrow>\<^sub>d* n''; n -as\<rightarrow>* n''; n'' -as'\<rightarrow>\<^sub>c\<^sub>d n'\<rbrakk> \<Longrightarrow> n -as @ as'\<rightarrow>* n'
 2. \<And>n as n'' V as' n'. \<lbrakk>n -as\<rightarrow>\<^sub>d* n''; n -as\<rightarrow>* n''; n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'\<rbrakk> \<Longrightarrow> n -as @ as'\<rightarrow>* n'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n as n'' as' n'. \<lbrakk>n -as\<rightarrow>\<^sub>d* n''; n -as\<rightarrow>* n''; n'' -as'\<rightarrow>\<^sub>c\<^sub>d n'\<rbrakk> \<Longrightarrow> n -as @ as'\<rightarrow>* n'
 2. \<And>n as n'' V as' n'. \<lbrakk>n -as\<rightarrow>\<^sub>d* n''; n -as\<rightarrow>* n''; n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'\<rbrakk> \<Longrightarrow> n -as @ as'\<rightarrow>* n'
[PROOF STEP]
case (DynPDG_path_Append_cdep n as n'' as' n')
[PROOF STATE]
proof (state)
this:
n -as\<rightarrow>\<^sub>d* n''
n -as\<rightarrow>* n''
n'' -as'\<rightarrow>\<^sub>c\<^sub>d n'

goal (2 subgoals):
 1. \<And>n as n'' as' n'. \<lbrakk>n -as\<rightarrow>\<^sub>d* n''; n -as\<rightarrow>* n''; n'' -as'\<rightarrow>\<^sub>c\<^sub>d n'\<rbrakk> \<Longrightarrow> n -as @ as'\<rightarrow>* n'
 2. \<And>n as n'' V as' n'. \<lbrakk>n -as\<rightarrow>\<^sub>d* n''; n -as\<rightarrow>* n''; n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'\<rbrakk> \<Longrightarrow> n -as @ as'\<rightarrow>* n'
[PROOF STEP]
from \<open>n'' -as'\<rightarrow>\<^sub>c\<^sub>d n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n'' -as'\<rightarrow>\<^sub>c\<^sub>d n'
[PROOF STEP]
have "n'' -as'\<rightarrow>* n'"
[PROOF STATE]
proof (prove)
using this:
n'' -as'\<rightarrow>\<^sub>c\<^sub>d n'

goal (1 subgoal):
 1. n'' -as'\<rightarrow>* n'
[PROOF STEP]
by(rule DynPDG_cdep_edge_CFG_path(1))
[PROOF STATE]
proof (state)
this:
n'' -as'\<rightarrow>* n'

goal (2 subgoals):
 1. \<And>n as n'' as' n'. \<lbrakk>n -as\<rightarrow>\<^sub>d* n''; n -as\<rightarrow>* n''; n'' -as'\<rightarrow>\<^sub>c\<^sub>d n'\<rbrakk> \<Longrightarrow> n -as @ as'\<rightarrow>* n'
 2. \<And>n as n'' V as' n'. \<lbrakk>n -as\<rightarrow>\<^sub>d* n''; n -as\<rightarrow>* n''; n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'\<rbrakk> \<Longrightarrow> n -as @ as'\<rightarrow>* n'
[PROOF STEP]
with \<open>n -as\<rightarrow>* n''\<close>
[PROOF STATE]
proof (chain)
picking this:
n -as\<rightarrow>* n''
n'' -as'\<rightarrow>* n'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
n -as\<rightarrow>* n''
n'' -as'\<rightarrow>* n'

goal (1 subgoal):
 1. n -as @ as'\<rightarrow>* n'
[PROOF STEP]
by(rule path_Append)
[PROOF STATE]
proof (state)
this:
n -as @ as'\<rightarrow>* n'

goal (1 subgoal):
 1. \<And>n as n'' V as' n'. \<lbrakk>n -as\<rightarrow>\<^sub>d* n''; n -as\<rightarrow>* n''; n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'\<rbrakk> \<Longrightarrow> n -as @ as'\<rightarrow>* n'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n as n'' V as' n'. \<lbrakk>n -as\<rightarrow>\<^sub>d* n''; n -as\<rightarrow>* n''; n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'\<rbrakk> \<Longrightarrow> n -as @ as'\<rightarrow>* n'
[PROOF STEP]
case (DynPDG_path_Append_ddep n as n'' V as' n')
[PROOF STATE]
proof (state)
this:
n -as\<rightarrow>\<^sub>d* n''
n -as\<rightarrow>* n''
n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'

goal (1 subgoal):
 1. \<And>n as n'' V as' n'. \<lbrakk>n -as\<rightarrow>\<^sub>d* n''; n -as\<rightarrow>* n''; n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'\<rbrakk> \<Longrightarrow> n -as @ as'\<rightarrow>* n'
[PROOF STEP]
from \<open>n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'
[PROOF STEP]
have "n'' -as'\<rightarrow>* n'"
[PROOF STATE]
proof (prove)
using this:
n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'

goal (1 subgoal):
 1. n'' -as'\<rightarrow>* n'
[PROOF STEP]
by(rule DynPDG_ddep_edge_CFG_path(1))
[PROOF STATE]
proof (state)
this:
n'' -as'\<rightarrow>* n'

goal (1 subgoal):
 1. \<And>n as n'' V as' n'. \<lbrakk>n -as\<rightarrow>\<^sub>d* n''; n -as\<rightarrow>* n''; n'' -{V}as'\<rightarrow>\<^sub>d\<^sub>d n'\<rbrakk> \<Longrightarrow> n -as @ as'\<rightarrow>* n'
[PROOF STEP]
with \<open>n -as\<rightarrow>* n''\<close>
[PROOF STATE]
proof (chain)
picking this:
n -as\<rightarrow>* n''
n'' -as'\<rightarrow>* n'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
n -as\<rightarrow>* n''
n'' -as'\<rightarrow>* n'

goal (1 subgoal):
 1. n -as @ as'\<rightarrow>* n'
[PROOF STEP]
by(rule path_Append)
[PROOF STATE]
proof (state)
this:
n -as @ as'\<rightarrow>* n'

goal:
No subgoals!
[PROOF STEP]
qed