[STATEMENT]
lemma prod_list_ge1:
  assumes "Ball (set x) (\<lambda> (a::real). a \<ge> 1)"
  shows "prod_list x \<ge> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<le> prod_list x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>a\<in>set x. 1 \<le> a

goal (1 subgoal):
 1. 1 \<le> prod_list x
[PROOF STEP]
proof(induct x)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Ball (set []) ((\<le>) 1) \<Longrightarrow> 1 \<le> prod_list []
 2. \<And>a x. \<lbrakk>Ball (set x) ((\<le>) 1) \<Longrightarrow> 1 \<le> prod_list x; Ball (set (a # x)) ((\<le>) 1)\<rbrakk> \<Longrightarrow> 1 \<le> prod_list (a # x)
[PROOF STEP]
case (Cons a as)
[PROOF STATE]
proof (state)
this:
\<forall>a\<in>set as. 1 \<le> a \<Longrightarrow> 1 \<le> prod_list as
\<forall>a\<in>set (a # as). 1 \<le> a

goal (2 subgoals):
 1. Ball (set []) ((\<le>) 1) \<Longrightarrow> 1 \<le> prod_list []
 2. \<And>a x. \<lbrakk>Ball (set x) ((\<le>) 1) \<Longrightarrow> 1 \<le> prod_list x; Ball (set (a # x)) ((\<le>) 1)\<rbrakk> \<Longrightarrow> 1 \<le> prod_list (a # x)
[PROOF STEP]
have "\<forall>a\<in>set as. 1 \<le> a" "1 \<le> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a\<in>set as. 1 \<le> a &&& 1 \<le> a
[PROOF STEP]
using Cons(2)
[PROOF STATE]
proof (prove)
using this:
\<forall>a\<in>set (a # as). 1 \<le> a

goal (1 subgoal):
 1. \<forall>a\<in>set as. 1 \<le> a &&& 1 \<le> a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>a\<in>set as. 1 \<le> a
1 \<le> a

goal (2 subgoals):
 1. Ball (set []) ((\<le>) 1) \<Longrightarrow> 1 \<le> prod_list []
 2. \<And>a x. \<lbrakk>Ball (set x) ((\<le>) 1) \<Longrightarrow> 1 \<le> prod_list x; Ball (set (a # x)) ((\<le>) 1)\<rbrakk> \<Longrightarrow> 1 \<le> prod_list (a # x)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>a\<in>set as. 1 \<le> a
1 \<le> a

goal (1 subgoal):
 1. 1 \<le> prod_list (a # as)
[PROOF STEP]
using Cons.hyps mult_mono'
[PROOF STATE]
proof (prove)
using this:
\<forall>a\<in>set as. 1 \<le> a
1 \<le> a
\<forall>a\<in>set as. 1 \<le> a \<Longrightarrow> 1 \<le> prod_list as
\<lbrakk>?a \<le> ?b; ?c \<le> ?d; (0::?'a) \<le> ?a; (0::?'a) \<le> ?c\<rbrakk> \<Longrightarrow> ?a * ?c \<le> ?b * ?d

goal (1 subgoal):
 1. 1 \<le> prod_list (a # as)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
1 \<le> prod_list (a # as)

goal (1 subgoal):
 1. Ball (set []) ((\<le>) 1) \<Longrightarrow> 1 \<le> prod_list []
[PROOF STEP]
qed auto


[STATEMENT]
lemma mahler_measure_monic_ge_1: "mahler_measure_monic p \<ge> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<le> mahler_measure_monic p
[PROOF STEP]
unfolding mahler_measure_monic_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<le> (\<Prod>a\<leftarrow>complex_roots_complex p. max 1 (cmod a))
[PROOF STEP]
by(rule prod_list_ge1,simp)


[STATEMENT]
lemma mahler_measure_monic_ge_0: "mahler_measure_monic p \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> mahler_measure_monic p
[PROOF STEP]
using mahler_measure_monic_ge_1 le_numeral_extra(1) order_trans
[PROOF STATE]
proof (prove)
using this:
1 \<le> mahler_measure_monic ?p
(0::?'a) \<le> (1::?'a)
\<lbrakk>?x \<le> ?y; ?y \<le> ?z\<rbrakk> \<Longrightarrow> ?x \<le> ?z

goal (1 subgoal):
 1. 0 \<le> mahler_measure_monic p
[PROOF STEP]
by blast


[STATEMENT]
lemma mahler_measure_ge_0: "0 \<le> mahler_measure h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> mahler_measure h
[PROOF STEP]
unfolding mahler_measure_def mahler_measure_poly_via_monic
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> cmod (lead_coeff (of_int_poly h)) * mahler_measure_monic (of_int_poly h)
[PROOF STEP]
by (simp add: mahler_measure_monic_ge_0)


[STATEMENT]
lemma mahler_measure_constant[simp]: "mahler_measure_poly [:c:] = cmod c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mahler_measure_poly [:c:] = cmod c
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mahler_measure_poly [:c:] = cmod c
[PROOF STEP]
have main: "complex_roots_complex [:c:] = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. complex_roots_complex [:c:] = []
[PROOF STEP]
unfolding complex_roots_complex_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SOME as. Polynomial.smult (lead_coeff [:c:]) (\<Prod>a\<leftarrow>as. [:- a, 1:]) = [:c:] \<and> length as = degree [:c:]) = []
[PROOF STEP]
by (rule some_equality, auto)
[PROOF STATE]
proof (state)
this:
complex_roots_complex [:c:] = []

goal (1 subgoal):
 1. mahler_measure_poly [:c:] = cmod c
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mahler_measure_poly [:c:] = cmod c
[PROOF STEP]
unfolding mahler_measure_poly_def main
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod (lead_coeff [:c:]) * (\<Prod>a\<leftarrow>[]. max 1 (cmod a)) = cmod c
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mahler_measure_poly [:c:] = cmod c

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mahler_measure_factor[simplified,simp]: "mahler_measure_poly [:- a, 1:] = max 1 (cmod a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mahler_measure_poly [:- a, 1:] = max 1 (cmod a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mahler_measure_poly [:- a, 1:] = max 1 (cmod a)
[PROOF STEP]
have main: "complex_roots_complex [:- a, 1:] = [a]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. complex_roots_complex [:- a, 1:] = [a]
[PROOF STEP]
unfolding complex_roots_complex_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SOME as. Polynomial.smult (lead_coeff [:- a, 1:]) (\<Prod>a\<leftarrow>as. [:- a, 1:]) = [:- a, 1:] \<and> length as = degree [:- a, 1:]) = [a]
[PROOF STEP]
proof (rule some_equality, auto, goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>as. \<lbrakk>(\<Prod>a\<leftarrow>as. pCons (- a) 1) = pCons (- a) 1; length as = Suc 0\<rbrakk> \<Longrightarrow> as = [a]
[PROOF STEP]
case (1 as)
[PROOF STATE]
proof (state)
this:
(\<Prod>a\<leftarrow>as. pCons (- a) 1) = pCons (- a) 1
length as = Suc 0

goal (1 subgoal):
 1. \<And>as. \<lbrakk>(\<Prod>a\<leftarrow>as. pCons (- a) 1) = pCons (- a) 1; length as = Suc 0\<rbrakk> \<Longrightarrow> as = [a]
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
(\<Prod>a\<leftarrow>as. pCons (- a) 1) = pCons (- a) 1
length as = Suc 0

goal (1 subgoal):
 1. as = [a]
[PROOF STEP]
by (cases as, auto)
[PROOF STATE]
proof (state)
this:
as = [a]

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
complex_roots_complex [:- a, 1:] = [a]

goal (1 subgoal):
 1. mahler_measure_poly [:- a, 1:] = max 1 (cmod a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mahler_measure_poly [:- a, 1:] = max 1 (cmod a)
[PROOF STEP]
unfolding mahler_measure_poly_def main
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod (lead_coeff [:- a, 1:]) * (\<Prod>a\<leftarrow>[a]. max 1 (cmod a)) = max 1 (cmod a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mahler_measure_poly [:- a, 1:] = max 1 (cmod a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mahler_measure_poly_explicit: "mahler_measure_poly (smult c (\<Prod>a\<leftarrow>as. [:- a, 1:]))
  = cmod c * (\<Prod>a\<leftarrow>as. (max 1 (cmod a)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>as. [:- a, 1:])) = cmod c * (\<Prod>a\<leftarrow>as. max 1 (cmod a))
[PROOF STEP]
proof (cases "c = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. c = 0 \<Longrightarrow> mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>as. [:- a, 1:])) = cmod c * (\<Prod>a\<leftarrow>as. max 1 (cmod a))
 2. c \<noteq> 0 \<Longrightarrow> mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>as. [:- a, 1:])) = cmod c * (\<Prod>a\<leftarrow>as. max 1 (cmod a))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
c = 0

goal (2 subgoals):
 1. c = 0 \<Longrightarrow> mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>as. [:- a, 1:])) = cmod c * (\<Prod>a\<leftarrow>as. max 1 (cmod a))
 2. c \<noteq> 0 \<Longrightarrow> mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>as. [:- a, 1:])) = cmod c * (\<Prod>a\<leftarrow>as. max 1 (cmod a))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
c = 0

goal (1 subgoal):
 1. mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>as. [:- a, 1:])) = cmod c * (\<Prod>a\<leftarrow>as. max 1 (cmod a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>as. [:- a, 1:])) = cmod c * (\<Prod>a\<leftarrow>as. max 1 (cmod a))

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>as. [:- a, 1:])) = cmod c * (\<Prod>a\<leftarrow>as. max 1 (cmod a))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>as. [:- a, 1:])) = cmod c * (\<Prod>a\<leftarrow>as. max 1 (cmod a))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
c \<noteq> 0

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>as. [:- a, 1:])) = cmod c * (\<Prod>a\<leftarrow>as. max 1 (cmod a))
[PROOF STEP]
note c = this
[PROOF STATE]
proof (state)
this:
c \<noteq> 0

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>as. [:- a, 1:])) = cmod c * (\<Prod>a\<leftarrow>as. max 1 (cmod a))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>as. [:- a, 1:])) = cmod c * (\<Prod>a\<leftarrow>as. max 1 (cmod a))
[PROOF STEP]
proof (induct as)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>[]. [:- a, 1:])) = cmod c * (\<Prod>a\<leftarrow>[]. max 1 (cmod a))
 2. \<And>a as. mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>as. [:- a, 1:])) = cmod c * (\<Prod>a\<leftarrow>as. max 1 (cmod a)) \<Longrightarrow> mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>a # as. [:- a, 1:])) = cmod c * (\<Prod>a\<leftarrow>a # as. max 1 (cmod a))
[PROOF STEP]
case (Cons a as)
[PROOF STATE]
proof (state)
this:
mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>as. [:- a, 1:])) = cmod c * (\<Prod>a\<leftarrow>as. max 1 (cmod a))

goal (2 subgoals):
 1. mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>[]. [:- a, 1:])) = cmod c * (\<Prod>a\<leftarrow>[]. max 1 (cmod a))
 2. \<And>a as. mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>as. [:- a, 1:])) = cmod c * (\<Prod>a\<leftarrow>as. max 1 (cmod a)) \<Longrightarrow> mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>a # as. [:- a, 1:])) = cmod c * (\<Prod>a\<leftarrow>a # as. max 1 (cmod a))
[PROOF STEP]
have "mahler_measure_poly (smult c (\<Prod>a\<leftarrow>a # as. [:- a, 1:]))
      = mahler_measure_poly (smult c (\<Prod>a\<leftarrow>as. [:- a, 1:]) * [: -a, 1 :])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>a # as. [:- a, 1:])) = mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>as. [:- a, 1:]) * [:- a, 1:])
[PROOF STEP]
by (rule arg_cong[of _ _ mahler_measure_poly], unfold list.simps prod_list.Cons mult_smult_left, simp)
[PROOF STATE]
proof (state)
this:
mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>a # as. [:- a, 1:])) = mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>as. [:- a, 1:]) * [:- a, 1:])

goal (2 subgoals):
 1. mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>[]. [:- a, 1:])) = cmod c * (\<Prod>a\<leftarrow>[]. max 1 (cmod a))
 2. \<And>a as. mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>as. [:- a, 1:])) = cmod c * (\<Prod>a\<leftarrow>as. max 1 (cmod a)) \<Longrightarrow> mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>a # as. [:- a, 1:])) = cmod c * (\<Prod>a\<leftarrow>a # as. max 1 (cmod a))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>a # as. [:- a, 1:])) = mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>as. [:- a, 1:]) * [:- a, 1:])

goal (2 subgoals):
 1. mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>[]. [:- a, 1:])) = cmod c * (\<Prod>a\<leftarrow>[]. max 1 (cmod a))
 2. \<And>a as. mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>as. [:- a, 1:])) = cmod c * (\<Prod>a\<leftarrow>as. max 1 (cmod a)) \<Longrightarrow> mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>a # as. [:- a, 1:])) = cmod c * (\<Prod>a\<leftarrow>a # as. max 1 (cmod a))
[PROOF STEP]
have "\<dots> = mahler_measure_poly (smult c (\<Prod>a\<leftarrow>as. [:- a, 1:])) * mahler_measure_poly ([:- a, 1:])"
      (is "_ = ?l * ?r")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>as. [:- a, 1:]) * [:- a, 1:]) = mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>as. [:- a, 1:])) * mahler_measure_poly [:- a, 1:]
[PROOF STEP]
by (rule measure_eq_prod)
[PROOF STATE]
proof (state)
this:
mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>as. [:- a, 1:]) * [:- a, 1:]) = mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>as. [:- a, 1:])) * mahler_measure_poly [:- a, 1:]

goal (2 subgoals):
 1. mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>[]. [:- a, 1:])) = cmod c * (\<Prod>a\<leftarrow>[]. max 1 (cmod a))
 2. \<And>a as. mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>as. [:- a, 1:])) = cmod c * (\<Prod>a\<leftarrow>as. max 1 (cmod a)) \<Longrightarrow> mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>a # as. [:- a, 1:])) = cmod c * (\<Prod>a\<leftarrow>a # as. max 1 (cmod a))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>as. [:- a, 1:]) * [:- a, 1:]) = mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>as. [:- a, 1:])) * mahler_measure_poly [:- a, 1:]

goal (2 subgoals):
 1. mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>[]. [:- a, 1:])) = cmod c * (\<Prod>a\<leftarrow>[]. max 1 (cmod a))
 2. \<And>a as. mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>as. [:- a, 1:])) = cmod c * (\<Prod>a\<leftarrow>as. max 1 (cmod a)) \<Longrightarrow> mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>a # as. [:- a, 1:])) = cmod c * (\<Prod>a\<leftarrow>a # as. max 1 (cmod a))
[PROOF STEP]
have "?l = cmod c * (\<Prod>a\<leftarrow>as. max 1 (cmod a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>as. [:- a, 1:])) = cmod c * (\<Prod>a\<leftarrow>as. max 1 (cmod a))
[PROOF STEP]
unfolding Cons
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod c * (\<Prod>a\<leftarrow>as. max 1 (cmod a)) = cmod c * (\<Prod>a\<leftarrow>as. max 1 (cmod a))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>as. [:- a, 1:])) = cmod c * (\<Prod>a\<leftarrow>as. max 1 (cmod a))

goal (2 subgoals):
 1. mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>[]. [:- a, 1:])) = cmod c * (\<Prod>a\<leftarrow>[]. max 1 (cmod a))
 2. \<And>a as. mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>as. [:- a, 1:])) = cmod c * (\<Prod>a\<leftarrow>as. max 1 (cmod a)) \<Longrightarrow> mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>a # as. [:- a, 1:])) = cmod c * (\<Prod>a\<leftarrow>a # as. max 1 (cmod a))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>as. [:- a, 1:])) = cmod c * (\<Prod>a\<leftarrow>as. max 1 (cmod a))

goal (2 subgoals):
 1. mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>[]. [:- a, 1:])) = cmod c * (\<Prod>a\<leftarrow>[]. max 1 (cmod a))
 2. \<And>a as. mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>as. [:- a, 1:])) = cmod c * (\<Prod>a\<leftarrow>as. max 1 (cmod a)) \<Longrightarrow> mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>a # as. [:- a, 1:])) = cmod c * (\<Prod>a\<leftarrow>a # as. max 1 (cmod a))
[PROOF STEP]
have "?r = max 1 (cmod a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mahler_measure_poly [:- a, 1:] = max 1 (cmod a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
mahler_measure_poly [:- a, 1:] = max 1 (cmod a)

goal (2 subgoals):
 1. mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>[]. [:- a, 1:])) = cmod c * (\<Prod>a\<leftarrow>[]. max 1 (cmod a))
 2. \<And>a as. mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>as. [:- a, 1:])) = cmod c * (\<Prod>a\<leftarrow>as. max 1 (cmod a)) \<Longrightarrow> mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>a # as. [:- a, 1:])) = cmod c * (\<Prod>a\<leftarrow>a # as. max 1 (cmod a))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>a # as. [:- a, 1:])) = cmod c * (\<Prod>a\<leftarrow>as. max 1 (cmod a)) * max 1 (cmod a)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>a # as. [:- a, 1:])) = cmod c * (\<Prod>a\<leftarrow>as. max 1 (cmod a)) * max 1 (cmod a)

goal (1 subgoal):
 1. mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>a # as. [:- a, 1:])) = cmod c * (\<Prod>a\<leftarrow>a # as. max 1 (cmod a))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>a # as. [:- a, 1:])) = cmod c * (\<Prod>a\<leftarrow>a # as. max 1 (cmod a))

goal (1 subgoal):
 1. mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>[]. [:- a, 1:])) = cmod c * (\<Prod>a\<leftarrow>[]. max 1 (cmod a))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>[]. [:- a, 1:])) = cmod c * (\<Prod>a\<leftarrow>[]. max 1 (cmod a))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (1 subgoal):
 1. mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>[]. [:- a, 1:])) = cmod c * (\<Prod>a\<leftarrow>[]. max 1 (cmod a))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>[]. [:- a, 1:])) = cmod c * (\<Prod>a\<leftarrow>[]. max 1 (cmod a))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>[]. [:- a, 1:])) = cmod c * (\<Prod>a\<leftarrow>[]. max 1 (cmod a))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
mahler_measure_poly (Polynomial.smult c (\<Prod>a\<leftarrow>as. [:- a, 1:])) = cmod c * (\<Prod>a\<leftarrow>as. max 1 (cmod a))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mahler_measure_poly_ge_1:
  assumes "h \<noteq> 0"
  shows "(1::real) \<le> mahler_measure h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<le> mahler_measure h
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 1 \<le> mahler_measure h
[PROOF STEP]
have rc: "\<bar>real_of_int i\<bar> = of_int \<bar>i\<bar>" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>real_of_int i\<bar> = real_of_int \<bar>i\<bar>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<bar>real_of_int ?i\<bar> = real_of_int \<bar>?i\<bar>

goal (1 subgoal):
 1. 1 \<le> mahler_measure h
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
h \<noteq> 0
[PROOF STEP]
have "cmod (lead_coeff (map_poly complex_of_int h)) > 0"
[PROOF STATE]
proof (prove)
using this:
h \<noteq> 0

goal (1 subgoal):
 1. 0 < cmod (lead_coeff (of_int_poly h))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < cmod (lead_coeff (of_int_poly h))

goal (1 subgoal):
 1. 1 \<le> mahler_measure h
[PROOF STEP]
hence "cmod (lead_coeff (map_poly complex_of_int h)) \<ge> 1"
[PROOF STATE]
proof (prove)
using this:
0 < cmod (lead_coeff (of_int_poly h))

goal (1 subgoal):
 1. 1 \<le> cmod (lead_coeff (of_int_poly h))
[PROOF STEP]
by(cases "lead_coeff h = 0", auto simp del: leading_coeff_0_iff)
[PROOF STATE]
proof (state)
this:
1 \<le> cmod (lead_coeff (of_int_poly h))

goal (1 subgoal):
 1. 1 \<le> mahler_measure h
[PROOF STEP]
from mult_mono[OF this mahler_measure_monic_ge_1 norm_ge_zero]
[PROOF STATE]
proof (chain)
picking this:
0 \<le> 1 \<Longrightarrow> 1 * 1 \<le> cmod (lead_coeff (of_int_poly h)) * mahler_measure_monic ?p2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 \<le> 1 \<Longrightarrow> 1 * 1 \<le> cmod (lead_coeff (of_int_poly h)) * mahler_measure_monic ?p2

goal (1 subgoal):
 1. 1 \<le> mahler_measure h
[PROOF STEP]
unfolding mahler_measure_def mahler_measure_poly_via_monic
[PROOF STATE]
proof (prove)
using this:
0 \<le> 1 \<Longrightarrow> 1 * 1 \<le> cmod (lead_coeff (of_int_poly h)) * mahler_measure_monic ?p2

goal (1 subgoal):
 1. 1 \<le> cmod (lead_coeff (of_int_poly h)) * mahler_measure_monic (of_int_poly h)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
1 \<le> mahler_measure h

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mahler_measure_dvd: assumes "f \<noteq> 0" and "h dvd f"
  shows "mahler_measure h \<le> mahler_measure f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mahler_measure h \<le> mahler_measure f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mahler_measure h \<le> mahler_measure f
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
f \<noteq> 0
h dvd f
[PROOF STEP]
obtain g where f: "f = g * h"
[PROOF STATE]
proof (prove)
using this:
f \<noteq> 0
h dvd f

goal (1 subgoal):
 1. (\<And>g. f = g * h \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding dvd_def
[PROOF STATE]
proof (prove)
using this:
f \<noteq> 0
\<exists>k. f = h * k

goal (1 subgoal):
 1. (\<And>g. f = g * h \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f = g * h

goal (1 subgoal):
 1. mahler_measure h \<le> mahler_measure f
[PROOF STEP]
from f assms
[PROOF STATE]
proof (chain)
picking this:
f = g * h
f \<noteq> 0
h dvd f
[PROOF STEP]
have g0: "g \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
f = g * h
f \<noteq> 0
h dvd f

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

goal (1 subgoal):
 1. mahler_measure h \<le> mahler_measure f
[PROOF STEP]
hence mg: "mahler_measure g \<ge> 1"
[PROOF STATE]
proof (prove)
using this:
g \<noteq> 0

goal (1 subgoal):
 1. 1 \<le> mahler_measure g
[PROOF STEP]
by (rule mahler_measure_poly_ge_1)
[PROOF STATE]
proof (state)
this:
1 \<le> mahler_measure g

goal (1 subgoal):
 1. mahler_measure h \<le> mahler_measure f
[PROOF STEP]
have "1 * mahler_measure h \<le> mahler_measure f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 * mahler_measure h \<le> mahler_measure f
[PROOF STEP]
unfolding mahler_measure_def f measure_eq_prod
      of_int_poly_hom.hom_mult
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 * mahler_measure_poly (of_int_poly h) \<le> mahler_measure_poly (of_int_poly g) * mahler_measure_poly (of_int_poly h)
[PROOF STEP]
unfolding mahler_measure_def[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 * mahler_measure h \<le> mahler_measure g * mahler_measure h
[PROOF STEP]
by (rule mult_right_mono[OF mg mahler_measure_ge_0])
[PROOF STATE]
proof (state)
this:
1 * mahler_measure h \<le> mahler_measure f

goal (1 subgoal):
 1. mahler_measure h \<le> mahler_measure f
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
1 * mahler_measure h \<le> mahler_measure f

goal (1 subgoal):
 1. mahler_measure h \<le> mahler_measure f
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
mahler_measure h \<le> mahler_measure f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mahler_graeffe: "mahler_measure_poly (graeffe_poly c as m) = (mahler_measure_poly f)^(2^m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mahler_measure_poly (graeffe_poly c as m) = mahler_measure_poly f ^ 2 ^ m
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mahler_measure_poly (graeffe_poly c as m) = mahler_measure_poly f ^ 2 ^ m
[PROOF STEP]
have graeffe: "graeffe_poly c as m = smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>(map (\<lambda> a. a ^ 2 ^ m) as). [:- a, 1:])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. graeffe_poly c as m = Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>map (\<lambda>a. a ^ 2 ^ m) as. [:- a, 1:])
[PROOF STEP]
unfolding graeffe_poly_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1:]) = Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>map (\<lambda>a. a ^ 2 ^ m) as. [:- a, 1:])
[PROOF STEP]
by (rule arg_cong[of _ _ "smult (c ^ 2 ^ m)"], induct as, auto)
[PROOF STATE]
proof (state)
this:
graeffe_poly c as m = Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>map (\<lambda>a. a ^ 2 ^ m) as. [:- a, 1:])

goal (1 subgoal):
 1. mahler_measure_poly (graeffe_poly c as m) = mahler_measure_poly f ^ 2 ^ m
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
graeffe_poly c as m = Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>map (\<lambda>a. a ^ 2 ^ m) as. [:- a, 1:])

goal (1 subgoal):
 1. mahler_measure_poly (graeffe_poly c as m) = mahler_measure_poly f ^ 2 ^ m
[PROOF STEP]
fix n :: nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mahler_measure_poly (graeffe_poly c as m) = mahler_measure_poly f ^ 2 ^ m
[PROOF STEP]
assume n: "n > 0"
[PROOF STATE]
proof (state)
this:
0 < n

goal (1 subgoal):
 1. mahler_measure_poly (graeffe_poly c as m) = mahler_measure_poly f ^ 2 ^ m
[PROOF STEP]
have id: "max 1 (cmod a ^ n) = max 1 (cmod a) ^ n" for a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max 1 (cmod a ^ n) = max 1 (cmod a) ^ n
[PROOF STEP]
proof (cases "cmod a \<le> 1")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. cmod a \<le> 1 \<Longrightarrow> max 1 (cmod a ^ n) = max 1 (cmod a) ^ n
 2. \<not> cmod a \<le> 1 \<Longrightarrow> max 1 (cmod a ^ n) = max 1 (cmod a) ^ n
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
cmod a \<le> 1

goal (2 subgoals):
 1. cmod a \<le> 1 \<Longrightarrow> max 1 (cmod a ^ n) = max 1 (cmod a) ^ n
 2. \<not> cmod a \<le> 1 \<Longrightarrow> max 1 (cmod a ^ n) = max 1 (cmod a) ^ n
[PROOF STEP]
hence "cmod a ^ n \<le> 1"
[PROOF STATE]
proof (prove)
using this:
cmod a \<le> 1

goal (1 subgoal):
 1. cmod a ^ n \<le> 1
[PROOF STEP]
by (simp add: power_le_one)
[PROOF STATE]
proof (state)
this:
cmod a ^ n \<le> 1

goal (2 subgoals):
 1. cmod a \<le> 1 \<Longrightarrow> max 1 (cmod a ^ n) = max 1 (cmod a) ^ n
 2. \<not> cmod a \<le> 1 \<Longrightarrow> max 1 (cmod a ^ n) = max 1 (cmod a) ^ n
[PROOF STEP]
with True
[PROOF STATE]
proof (chain)
picking this:
cmod a \<le> 1
cmod a ^ n \<le> 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
cmod a \<le> 1
cmod a ^ n \<le> 1

goal (1 subgoal):
 1. max 1 (cmod a ^ n) = max 1 (cmod a) ^ n
[PROOF STEP]
by (simp add: max_def)
[PROOF STATE]
proof (state)
this:
max 1 (cmod a ^ n) = max 1 (cmod a) ^ n

goal (1 subgoal):
 1. \<not> cmod a \<le> 1 \<Longrightarrow> max 1 (cmod a ^ n) = max 1 (cmod a) ^ n
[PROOF STEP]
qed (auto simp: max_def)
[PROOF STATE]
proof (state)
this:
max 1 (cmod ?a ^ n) = max 1 (cmod ?a) ^ n

goal (1 subgoal):
 1. mahler_measure_poly (graeffe_poly c as m) = mahler_measure_poly f ^ 2 ^ m
[PROOF STEP]
have "(\<Prod>x\<leftarrow>as. max 1 (cmod x ^ n)) = (\<Prod>a\<leftarrow>as. max 1 (cmod a)) ^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>x\<leftarrow>as. max 1 (cmod x ^ n)) = (\<Prod>a\<leftarrow>as. max 1 (cmod a)) ^ n
[PROOF STEP]
by (induct as, auto simp: field_simps n id)
[PROOF STATE]
proof (state)
this:
(\<Prod>x\<leftarrow>as. max 1 (cmod x ^ n)) = (\<Prod>a\<leftarrow>as. max 1 (cmod a)) ^ n

goal (1 subgoal):
 1. mahler_measure_poly (graeffe_poly c as m) = mahler_measure_poly f ^ 2 ^ m
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
0 < ?n2 \<Longrightarrow> (\<Prod>x\<leftarrow>as. max 1 (cmod x ^ ?n2)) = (\<Prod>a\<leftarrow>as. max 1 (cmod a)) ^ ?n2

goal (1 subgoal):
 1. mahler_measure_poly (graeffe_poly c as m) = mahler_measure_poly f ^ 2 ^ m
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < ?n2 \<Longrightarrow> (\<Prod>x\<leftarrow>as. max 1 (cmod x ^ ?n2)) = (\<Prod>a\<leftarrow>as. max 1 (cmod a)) ^ ?n2

goal (1 subgoal):
 1. mahler_measure_poly (graeffe_poly c as m) = mahler_measure_poly f ^ 2 ^ m
[PROOF STEP]
unfolding f mahler_measure_poly_explicit graeffe
[PROOF STATE]
proof (prove)
using this:
0 < ?n2 \<Longrightarrow> (\<Prod>x\<leftarrow>as. max 1 (cmod x ^ ?n2)) = (\<Prod>a\<leftarrow>as. max 1 (cmod a)) ^ ?n2

goal (1 subgoal):
 1. cmod (c ^ 2 ^ m) * (\<Prod>a\<leftarrow>map (\<lambda>a. a ^ 2 ^ m) as. max 1 (cmod a)) = (cmod c * (\<Prod>a\<leftarrow>as. max 1 (cmod a))) ^ 2 ^ m
[PROOF STEP]
by (auto simp: o_def field_simps norm_power)
[PROOF STATE]
proof (state)
this:
mahler_measure_poly (graeffe_poly c as m) = mahler_measure_poly f ^ 2 ^ m

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma poly_square_subst_coeff: "coeff (poly_square_subst f) i = coeff f (2 * i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly.coeff (poly_square_subst f) i = poly.coeff f (2 * i)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. poly.coeff (poly_square_subst f) i = poly.coeff f (2 * i)
[PROOF STEP]
have id: "coeff f (2 * i) = coeff (Poly (coeffs f)) (2 * i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly.coeff f (2 * i) = poly.coeff (Poly (coeffs f)) (2 * i)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
poly.coeff f (2 * i) = poly.coeff (Poly (coeffs f)) (2 * i)

goal (1 subgoal):
 1. poly.coeff (poly_square_subst f) i = poly.coeff f (2 * i)
[PROOF STEP]
obtain xs where xs: "coeffs f = xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>xs. coeffs f = xs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
coeffs f = xs

goal (1 subgoal):
 1. poly.coeff (poly_square_subst f) i = poly.coeff f (2 * i)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly.coeff (poly_square_subst f) i = poly.coeff f (2 * i)
[PROOF STEP]
unfolding poly_square_subst_def poly_of_list_def coeff_Poly_eq id xs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nth_default (0::'a) (drop_half xs) i = nth_default (0::'a) xs (2 * i)
[PROOF STEP]
proof (induct xs arbitrary: i rule: drop_half.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x y ys i. (\<And>i. nth_default (0::'a) (drop_half ys) i = nth_default (0::'a) ys (2 * i)) \<Longrightarrow> nth_default (0::'a) (drop_half (x # y # ys)) i = nth_default (0::'a) (x # y # ys) (2 * i)
 2. \<And>i. nth_default (0::'a) (drop_half []) i = nth_default (0::'a) [] (2 * i)
 3. \<And>v i. nth_default (0::'a) (drop_half [v]) i = nth_default (0::'a) [v] (2 * i)
[PROOF STEP]
case (1 x y ys i)
[PROOF STATE]
proof (state)
this:
nth_default (0::'a) (drop_half ys) ?i = nth_default (0::'a) ys (2 * ?i)

goal (3 subgoals):
 1. \<And>x y ys i. (\<And>i. nth_default (0::'a) (drop_half ys) i = nth_default (0::'a) ys (2 * i)) \<Longrightarrow> nth_default (0::'a) (drop_half (x # y # ys)) i = nth_default (0::'a) (x # y # ys) (2 * i)
 2. \<And>i. nth_default (0::'a) (drop_half []) i = nth_default (0::'a) [] (2 * i)
 3. \<And>v i. nth_default (0::'a) (drop_half [v]) i = nth_default (0::'a) [v] (2 * i)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
nth_default (0::'a) (drop_half ys) ?i = nth_default (0::'a) ys (2 * ?i)

goal (1 subgoal):
 1. nth_default (0::'a) (drop_half (x # y # ys)) i = nth_default (0::'a) (x # y # ys) (2 * i)
[PROOF STEP]
by (cases i, auto)
[PROOF STATE]
proof (state)
this:
nth_default (0::'a) (drop_half (x # y # ys)) i = nth_default (0::'a) (x # y # ys) (2 * i)

goal (2 subgoals):
 1. \<And>i. nth_default (0::'a) (drop_half []) i = nth_default (0::'a) [] (2 * i)
 2. \<And>v i. nth_default (0::'a) (drop_half [v]) i = nth_default (0::'a) [v] (2 * i)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. nth_default (0::'a) (drop_half []) i = nth_default (0::'a) [] (2 * i)
 2. \<And>v i. nth_default (0::'a) (drop_half [v]) i = nth_default (0::'a) [v] (2 * i)
[PROOF STEP]
case ("2_2" x i)
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>i. nth_default (0::'a) (drop_half []) i = nth_default (0::'a) [] (2 * i)
 2. \<And>v i. nth_default (0::'a) (drop_half [v]) i = nth_default (0::'a) [v] (2 * i)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nth_default (0::'a) (drop_half [x]) i = nth_default (0::'a) [x] (2 * i)
[PROOF STEP]
by (cases i, auto)
[PROOF STATE]
proof (state)
this:
nth_default (0::'a) (drop_half [x]) i = nth_default (0::'a) [x] (2 * i)

goal (1 subgoal):
 1. \<And>i. nth_default (0::'a) (drop_half []) i = nth_default (0::'a) [] (2 * i)
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
poly.coeff (poly_square_subst f) i = poly.coeff f (2 * i)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma poly_even_odd_coeff: assumes "poly_even_odd f = (ev,od)"
  shows "coeff ev i = coeff f (2 * i)" "coeff od i = coeff f (2 * i + 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly.coeff ev i = poly.coeff f (2 * i) &&& poly.coeff od i = poly.coeff f (2 * i + 1)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. poly.coeff ev i = poly.coeff f (2 * i)
 2. poly.coeff od i = poly.coeff f (2 * i + 1)
[PROOF STEP]
have id: "\<And> i. coeff f i = coeff (Poly (coeffs f)) i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. poly.coeff f i = poly.coeff (Poly (coeffs f)) i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
poly.coeff f ?i = poly.coeff (Poly (coeffs f)) ?i

goal (2 subgoals):
 1. poly.coeff ev i = poly.coeff f (2 * i)
 2. poly.coeff od i = poly.coeff f (2 * i + 1)
[PROOF STEP]
obtain xs where xs: "coeffs f = xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>xs. coeffs f = xs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
coeffs f = xs

goal (2 subgoals):
 1. poly.coeff ev i = poly.coeff f (2 * i)
 2. poly.coeff od i = poly.coeff f (2 * i + 1)
[PROOF STEP]
from assms[unfolded poly_even_odd_def]
[PROOF STATE]
proof (chain)
picking this:
(case alternate (coeffs f) of (evn, od) \<Rightarrow> (poly_of_list evn, poly_of_list od)) = (ev, od)
[PROOF STEP]
have ev_od: "ev = Poly (fst (alternate xs))" "od = Poly (snd (alternate xs))"
[PROOF STATE]
proof (prove)
using this:
(case alternate (coeffs f) of (evn, od) \<Rightarrow> (poly_of_list evn, poly_of_list od)) = (ev, od)

goal (1 subgoal):
 1. ev = Poly (fst (alternate xs)) &&& od = Poly (snd (alternate xs))
[PROOF STEP]
by (auto simp: xs split: prod.splits)
[PROOF STATE]
proof (state)
this:
ev = Poly (fst (alternate xs))
od = Poly (snd (alternate xs))

goal (2 subgoals):
 1. poly.coeff ev i = poly.coeff f (2 * i)
 2. poly.coeff od i = poly.coeff f (2 * i + 1)
[PROOF STEP]
have "coeff ev i = coeff f (2 * i) \<and> coeff od i = coeff f (2 * i + 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly.coeff ev i = poly.coeff f (2 * i) \<and> poly.coeff od i = poly.coeff f (2 * i + 1)
[PROOF STEP]
unfolding poly_of_list_def coeff_Poly_eq id xs ev_od
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nth_default (0::'a) (fst (alternate xs)) i = nth_default (0::'a) xs (2 * i) \<and> nth_default (0::'a) (snd (alternate xs)) i = nth_default (0::'a) xs (2 * i + 1)
[PROOF STEP]
proof (induct xs arbitrary: i rule: alternate.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x y ys i. (\<And>i. nth_default (0::'a) (fst (alternate ys)) i = nth_default (0::'a) ys (2 * i) \<and> nth_default (0::'a) (snd (alternate ys)) i = nth_default (0::'a) ys (2 * i + 1)) \<Longrightarrow> nth_default (0::'a) (fst (alternate (x # y # ys))) i = nth_default (0::'a) (x # y # ys) (2 * i) \<and> nth_default (0::'a) (snd (alternate (x # y # ys))) i = nth_default (0::'a) (x # y # ys) (2 * i + 1)
 2. \<And>i. nth_default (0::'a) (fst (alternate [])) i = nth_default (0::'a) [] (2 * i) \<and> nth_default (0::'a) (snd (alternate [])) i = nth_default (0::'a) [] (2 * i + 1)
 3. \<And>v i. nth_default (0::'a) (fst (alternate [v])) i = nth_default (0::'a) [v] (2 * i) \<and> nth_default (0::'a) (snd (alternate [v])) i = nth_default (0::'a) [v] (2 * i + 1)
[PROOF STEP]
case (1 x y ys i)
[PROOF STATE]
proof (state)
this:
nth_default (0::'a) (fst (alternate ys)) ?i = nth_default (0::'a) ys (2 * ?i) \<and> nth_default (0::'a) (snd (alternate ys)) ?i = nth_default (0::'a) ys (2 * ?i + 1)

goal (3 subgoals):
 1. \<And>x y ys i. (\<And>i. nth_default (0::'a) (fst (alternate ys)) i = nth_default (0::'a) ys (2 * i) \<and> nth_default (0::'a) (snd (alternate ys)) i = nth_default (0::'a) ys (2 * i + 1)) \<Longrightarrow> nth_default (0::'a) (fst (alternate (x # y # ys))) i = nth_default (0::'a) (x # y # ys) (2 * i) \<and> nth_default (0::'a) (snd (alternate (x # y # ys))) i = nth_default (0::'a) (x # y # ys) (2 * i + 1)
 2. \<And>i. nth_default (0::'a) (fst (alternate [])) i = nth_default (0::'a) [] (2 * i) \<and> nth_default (0::'a) (snd (alternate [])) i = nth_default (0::'a) [] (2 * i + 1)
 3. \<And>v i. nth_default (0::'a) (fst (alternate [v])) i = nth_default (0::'a) [v] (2 * i) \<and> nth_default (0::'a) (snd (alternate [v])) i = nth_default (0::'a) [v] (2 * i + 1)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
nth_default (0::'a) (fst (alternate ys)) ?i = nth_default (0::'a) ys (2 * ?i) \<and> nth_default (0::'a) (snd (alternate ys)) ?i = nth_default (0::'a) ys (2 * ?i + 1)

goal (1 subgoal):
 1. nth_default (0::'a) (fst (alternate (x # y # ys))) i = nth_default (0::'a) (x # y # ys) (2 * i) \<and> nth_default (0::'a) (snd (alternate (x # y # ys))) i = nth_default (0::'a) (x # y # ys) (2 * i + 1)
[PROOF STEP]
by (cases "alternate ys"; cases i, auto)
[PROOF STATE]
proof (state)
this:
nth_default (0::'a) (fst (alternate (x # y # ys))) i = nth_default (0::'a) (x # y # ys) (2 * i) \<and> nth_default (0::'a) (snd (alternate (x # y # ys))) i = nth_default (0::'a) (x # y # ys) (2 * i + 1)

goal (2 subgoals):
 1. \<And>i. nth_default (0::'a) (fst (alternate [])) i = nth_default (0::'a) [] (2 * i) \<and> nth_default (0::'a) (snd (alternate [])) i = nth_default (0::'a) [] (2 * i + 1)
 2. \<And>v i. nth_default (0::'a) (fst (alternate [v])) i = nth_default (0::'a) [v] (2 * i) \<and> nth_default (0::'a) (snd (alternate [v])) i = nth_default (0::'a) [v] (2 * i + 1)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. nth_default (0::'a) (fst (alternate [])) i = nth_default (0::'a) [] (2 * i) \<and> nth_default (0::'a) (snd (alternate [])) i = nth_default (0::'a) [] (2 * i + 1)
 2. \<And>v i. nth_default (0::'a) (fst (alternate [v])) i = nth_default (0::'a) [v] (2 * i) \<and> nth_default (0::'a) (snd (alternate [v])) i = nth_default (0::'a) [v] (2 * i + 1)
[PROOF STEP]
case ("2_2" x i)
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>i. nth_default (0::'a) (fst (alternate [])) i = nth_default (0::'a) [] (2 * i) \<and> nth_default (0::'a) (snd (alternate [])) i = nth_default (0::'a) [] (2 * i + 1)
 2. \<And>v i. nth_default (0::'a) (fst (alternate [v])) i = nth_default (0::'a) [v] (2 * i) \<and> nth_default (0::'a) (snd (alternate [v])) i = nth_default (0::'a) [v] (2 * i + 1)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nth_default (0::'a) (fst (alternate [x])) i = nth_default (0::'a) [x] (2 * i) \<and> nth_default (0::'a) (snd (alternate [x])) i = nth_default (0::'a) [x] (2 * i + 1)
[PROOF STEP]
by (cases i, auto)
[PROOF STATE]
proof (state)
this:
nth_default (0::'a) (fst (alternate [x])) i = nth_default (0::'a) [x] (2 * i) \<and> nth_default (0::'a) (snd (alternate [x])) i = nth_default (0::'a) [x] (2 * i + 1)

goal (1 subgoal):
 1. \<And>i. nth_default (0::'a) (fst (alternate [])) i = nth_default (0::'a) [] (2 * i) \<and> nth_default (0::'a) (snd (alternate [])) i = nth_default (0::'a) [] (2 * i + 1)
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
poly.coeff ev i = poly.coeff f (2 * i) \<and> poly.coeff od i = poly.coeff f (2 * i + 1)

goal (2 subgoals):
 1. poly.coeff ev i = poly.coeff f (2 * i)
 2. poly.coeff od i = poly.coeff f (2 * i + 1)
[PROOF STEP]
thus "coeff ev i = coeff f (2 * i)" "coeff od i = coeff f (2 * i + 1)"
[PROOF STATE]
proof (prove)
using this:
poly.coeff ev i = poly.coeff f (2 * i) \<and> poly.coeff od i = poly.coeff f (2 * i + 1)

goal (1 subgoal):
 1. poly.coeff ev i = poly.coeff f (2 * i) &&& poly.coeff od i = poly.coeff f (2 * i + 1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
poly.coeff ev i = poly.coeff f (2 * i)
poly.coeff od i = poly.coeff f (2 * i + 1)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma poly_square_subst: "poly_square_subst (f \<circ>\<^sub>p (monom 1 2)) = f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly_square_subst (f \<circ>\<^sub>p Polynomial.monom (1::'a) 2) = f
[PROOF STEP]
by (rule poly_eqI, unfold poly_square_subst_coeff, subst coeff_pcompose_x_pow_n, auto)


[STATEMENT]
lemma poly_even_odd: assumes "poly_even_odd f = (g,h)"
  shows "f = g \<circ>\<^sub>p monom 1 2 + monom 1 1 * (h \<circ>\<^sub>p monom 1 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f = g \<circ>\<^sub>p Polynomial.monom (1::'a) 2 + Polynomial.monom (1::'a) 1 * h \<circ>\<^sub>p Polynomial.monom (1::'a) 2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f = g \<circ>\<^sub>p Polynomial.monom (1::'a) 2 + Polynomial.monom (1::'a) 1 * h \<circ>\<^sub>p Polynomial.monom (1::'a) 2
[PROOF STEP]
note id = poly_even_odd_coeff[OF assms]
[PROOF STATE]
proof (state)
this:
poly.coeff g ?i = poly.coeff f (2 * ?i)
poly.coeff h ?i = poly.coeff f (2 * ?i + 1)

goal (1 subgoal):
 1. f = g \<circ>\<^sub>p Polynomial.monom (1::'a) 2 + Polynomial.monom (1::'a) 1 * h \<circ>\<^sub>p Polynomial.monom (1::'a) 2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f = g \<circ>\<^sub>p Polynomial.monom (1::'a) 2 + Polynomial.monom (1::'a) 1 * h \<circ>\<^sub>p Polynomial.monom (1::'a) 2
[PROOF STEP]
proof (rule poly_eqI, unfold coeff_add coeff_monom_mult)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. poly.coeff f n = poly.coeff (g \<circ>\<^sub>p Polynomial.monom (1::'a) 2) n + (if 1 \<le> n then (1::'a) * poly.coeff (h \<circ>\<^sub>p Polynomial.monom (1::'a) 2) (n - 1) else (0::'a))
[PROOF STEP]
fix n :: nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. poly.coeff f n = poly.coeff (g \<circ>\<^sub>p Polynomial.monom (1::'a) 2) n + (if 1 \<le> n then (1::'a) * poly.coeff (h \<circ>\<^sub>p Polynomial.monom (1::'a) 2) (n - 1) else (0::'a))
[PROOF STEP]
obtain m i where mi: "m = n div 2" "i = n mod 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>m i. \<lbrakk>m = n div 2; i = n mod 2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
m = n div 2
i = n mod 2

goal (1 subgoal):
 1. \<And>n. poly.coeff f n = poly.coeff (g \<circ>\<^sub>p Polynomial.monom (1::'a) 2) n + (if 1 \<le> n then (1::'a) * poly.coeff (h \<circ>\<^sub>p Polynomial.monom (1::'a) 2) (n - 1) else (0::'a))
[PROOF STEP]
have nmi: "n = 2 * m + i" "i < 2" "0 < (2 :: nat)" "1 < (2 :: nat)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (n = 2 * m + i &&& i < 2) &&& 0 < 2 &&& 1 < 2
[PROOF STEP]
unfolding mi
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (n = 2 * (n div 2) + n mod 2 &&& n mod 2 < 2) &&& 0 < 2 &&& 1 < 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n = 2 * m + i
i < 2
0 < 2
1 < 2

goal (1 subgoal):
 1. \<And>n. poly.coeff f n = poly.coeff (g \<circ>\<^sub>p Polynomial.monom (1::'a) 2) n + (if 1 \<le> n then (1::'a) * poly.coeff (h \<circ>\<^sub>p Polynomial.monom (1::'a) 2) (n - 1) else (0::'a))
[PROOF STEP]
have "(2 :: nat) \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
2 \<noteq> 0

goal (1 subgoal):
 1. \<And>n. poly.coeff f n = poly.coeff (g \<circ>\<^sub>p Polynomial.monom (1::'a) 2) n + (if 1 \<le> n then (1::'a) * poly.coeff (h \<circ>\<^sub>p Polynomial.monom (1::'a) 2) (n - 1) else (0::'a))
[PROOF STEP]
show "coeff f n = coeff (g \<circ>\<^sub>p monom 1 2) n + (if 1 \<le> n then 1 * coeff (h \<circ>\<^sub>p monom 1 2) (n - 1) else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly.coeff f n = poly.coeff (g \<circ>\<^sub>p Polynomial.monom (1::'a) 2) n + (if 1 \<le> n then (1::'a) * poly.coeff (h \<circ>\<^sub>p Polynomial.monom (1::'a) 2) (n - 1) else (0::'a))
[PROOF STEP]
proof (cases "i = 1")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i = 1 \<Longrightarrow> poly.coeff f n = poly.coeff (g \<circ>\<^sub>p Polynomial.monom (1::'a) 2) n + (if 1 \<le> n then (1::'a) * poly.coeff (h \<circ>\<^sub>p Polynomial.monom (1::'a) 2) (n - 1) else (0::'a))
 2. i \<noteq> 1 \<Longrightarrow> poly.coeff f n = poly.coeff (g \<circ>\<^sub>p Polynomial.monom (1::'a) 2) n + (if 1 \<le> n then (1::'a) * poly.coeff (h \<circ>\<^sub>p Polynomial.monom (1::'a) 2) (n - 1) else (0::'a))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
i = 1

goal (2 subgoals):
 1. i = 1 \<Longrightarrow> poly.coeff f n = poly.coeff (g \<circ>\<^sub>p Polynomial.monom (1::'a) 2) n + (if 1 \<le> n then (1::'a) * poly.coeff (h \<circ>\<^sub>p Polynomial.monom (1::'a) 2) (n - 1) else (0::'a))
 2. i \<noteq> 1 \<Longrightarrow> poly.coeff f n = poly.coeff (g \<circ>\<^sub>p Polynomial.monom (1::'a) 2) n + (if 1 \<le> n then (1::'a) * poly.coeff (h \<circ>\<^sub>p Polynomial.monom (1::'a) 2) (n - 1) else (0::'a))
[PROOF STEP]
hence id1: "2 * m + i - 1 = 2 * m + 0"
[PROOF STATE]
proof (prove)
using this:
i = 1

goal (1 subgoal):
 1. 2 * m + i - 1 = 2 * m + 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
2 * m + i - 1 = 2 * m + 0

goal (2 subgoals):
 1. i = 1 \<Longrightarrow> poly.coeff f n = poly.coeff (g \<circ>\<^sub>p Polynomial.monom (1::'a) 2) n + (if 1 \<le> n then (1::'a) * poly.coeff (h \<circ>\<^sub>p Polynomial.monom (1::'a) 2) (n - 1) else (0::'a))
 2. i \<noteq> 1 \<Longrightarrow> poly.coeff f n = poly.coeff (g \<circ>\<^sub>p Polynomial.monom (1::'a) 2) n + (if 1 \<le> n then (1::'a) * poly.coeff (h \<circ>\<^sub>p Polynomial.monom (1::'a) 2) (n - 1) else (0::'a))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly.coeff f n = poly.coeff (g \<circ>\<^sub>p Polynomial.monom (1::'a) 2) n + (if 1 \<le> n then (1::'a) * poly.coeff (h \<circ>\<^sub>p Polynomial.monom (1::'a) 2) (n - 1) else (0::'a))
[PROOF STEP]
unfolding nmi id id1 coeff_pcompose_monom[OF nmi(2)] coeff_pcompose_monom[OF nmi(3)]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly.coeff f (2 * m + i) = (if i = 0 then poly.coeff f (2 * m) else (0::'a)) + (if 1 \<le> 2 * m + i then (1::'a) * (if 0 = 0 then poly.coeff f (2 * m + 1) else (0::'a)) else (0::'a))
[PROOF STEP]
unfolding True
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly.coeff f (2 * m + 1) = (if 1 = 0 then poly.coeff f (2 * m) else (0::'a)) + (if 1 \<le> 2 * m + 1 then (1::'a) * (if 0 = 0 then poly.coeff f (2 * m + 1) else (0::'a)) else (0::'a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
poly.coeff f n = poly.coeff (g \<circ>\<^sub>p Polynomial.monom (1::'a) 2) n + (if 1 \<le> n then (1::'a) * poly.coeff (h \<circ>\<^sub>p Polynomial.monom (1::'a) 2) (n - 1) else (0::'a))

goal (1 subgoal):
 1. i \<noteq> 1 \<Longrightarrow> poly.coeff f n = poly.coeff (g \<circ>\<^sub>p Polynomial.monom (1::'a) 2) n + (if 1 \<le> n then (1::'a) * poly.coeff (h \<circ>\<^sub>p Polynomial.monom (1::'a) 2) (n - 1) else (0::'a))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i \<noteq> 1 \<Longrightarrow> poly.coeff f n = poly.coeff (g \<circ>\<^sub>p Polynomial.monom (1::'a) 2) n + (if 1 \<le> n then (1::'a) * poly.coeff (h \<circ>\<^sub>p Polynomial.monom (1::'a) 2) (n - 1) else (0::'a))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
i \<noteq> 1

goal (1 subgoal):
 1. i \<noteq> 1 \<Longrightarrow> poly.coeff f n = poly.coeff (g \<circ>\<^sub>p Polynomial.monom (1::'a) 2) n + (if 1 \<le> n then (1::'a) * poly.coeff (h \<circ>\<^sub>p Polynomial.monom (1::'a) 2) (n - 1) else (0::'a))
[PROOF STEP]
with nmi
[PROOF STATE]
proof (chain)
picking this:
n = 2 * m + i
i < 2
0 < 2
1 < 2
i \<noteq> 1
[PROOF STEP]
have i0: "i = 0"
[PROOF STATE]
proof (prove)
using this:
n = 2 * m + i
i < 2
0 < 2
1 < 2
i \<noteq> 1

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

goal (1 subgoal):
 1. i \<noteq> 1 \<Longrightarrow> poly.coeff f n = poly.coeff (g \<circ>\<^sub>p Polynomial.monom (1::'a) 2) n + (if 1 \<le> n then (1::'a) * poly.coeff (h \<circ>\<^sub>p Polynomial.monom (1::'a) 2) (n - 1) else (0::'a))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly.coeff f n = poly.coeff (g \<circ>\<^sub>p Polynomial.monom (1::'a) 2) n + (if 1 \<le> n then (1::'a) * poly.coeff (h \<circ>\<^sub>p Polynomial.monom (1::'a) 2) (n - 1) else (0::'a))
[PROOF STEP]
proof (cases m)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. m = 0 \<Longrightarrow> poly.coeff f n = poly.coeff (g \<circ>\<^sub>p Polynomial.monom (1::'a) 2) n + (if 1 \<le> n then (1::'a) * poly.coeff (h \<circ>\<^sub>p Polynomial.monom (1::'a) 2) (n - 1) else (0::'a))
 2. \<And>nat. m = Suc nat \<Longrightarrow> poly.coeff f n = poly.coeff (g \<circ>\<^sub>p Polynomial.monom (1::'a) 2) n + (if 1 \<le> n then (1::'a) * poly.coeff (h \<circ>\<^sub>p Polynomial.monom (1::'a) 2) (n - 1) else (0::'a))
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
m = Suc k

goal (2 subgoals):
 1. m = 0 \<Longrightarrow> poly.coeff f n = poly.coeff (g \<circ>\<^sub>p Polynomial.monom (1::'a) 2) n + (if 1 \<le> n then (1::'a) * poly.coeff (h \<circ>\<^sub>p Polynomial.monom (1::'a) 2) (n - 1) else (0::'a))
 2. \<And>nat. m = Suc nat \<Longrightarrow> poly.coeff f n = poly.coeff (g \<circ>\<^sub>p Polynomial.monom (1::'a) 2) n + (if 1 \<le> n then (1::'a) * poly.coeff (h \<circ>\<^sub>p Polynomial.monom (1::'a) 2) (n - 1) else (0::'a))
[PROOF STEP]
hence id1: "2 * m + i - 1 = 2 * k + 1"
[PROOF STATE]
proof (prove)
using this:
m = Suc k

goal (1 subgoal):
 1. 2 * m + i - 1 = 2 * k + 1
[PROOF STEP]
using i0
[PROOF STATE]
proof (prove)
using this:
m = Suc k
i = 0

goal (1 subgoal):
 1. 2 * m + i - 1 = 2 * k + 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
2 * m + i - 1 = 2 * k + 1

goal (2 subgoals):
 1. m = 0 \<Longrightarrow> poly.coeff f n = poly.coeff (g \<circ>\<^sub>p Polynomial.monom (1::'a) 2) n + (if 1 \<le> n then (1::'a) * poly.coeff (h \<circ>\<^sub>p Polynomial.monom (1::'a) 2) (n - 1) else (0::'a))
 2. \<And>nat. m = Suc nat \<Longrightarrow> poly.coeff f n = poly.coeff (g \<circ>\<^sub>p Polynomial.monom (1::'a) 2) n + (if 1 \<le> n then (1::'a) * poly.coeff (h \<circ>\<^sub>p Polynomial.monom (1::'a) 2) (n - 1) else (0::'a))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly.coeff f n = poly.coeff (g \<circ>\<^sub>p Polynomial.monom (1::'a) 2) n + (if 1 \<le> n then (1::'a) * poly.coeff (h \<circ>\<^sub>p Polynomial.monom (1::'a) 2) (n - 1) else (0::'a))
[PROOF STEP]
unfolding nmi id coeff_pcompose_monom[OF nmi(2)]
          coeff_pcompose_monom[OF nmi(4)] id1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly.coeff f (2 * m + i) = (if i = 0 then poly.coeff f (2 * m) else (0::'a)) + (if 1 \<le> 2 * m + i then (1::'a) * (if 1 = 0 then poly.coeff f (2 * k + 1) else (0::'a)) else (0::'a))
[PROOF STEP]
unfolding Suc i0
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly.coeff f (2 * Suc k + 0) = (if 0 = 0 then poly.coeff f (2 * Suc k) else (0::'a)) + (if 1 \<le> 2 * Suc k + 0 then (1::'a) * (if 1 = 0 then poly.coeff f (2 * k + 1) else (0::'a)) else (0::'a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
poly.coeff f n = poly.coeff (g \<circ>\<^sub>p Polynomial.monom (1::'a) 2) n + (if 1 \<le> n then (1::'a) * poly.coeff (h \<circ>\<^sub>p Polynomial.monom (1::'a) 2) (n - 1) else (0::'a))

goal (1 subgoal):
 1. m = 0 \<Longrightarrow> poly.coeff f n = poly.coeff (g \<circ>\<^sub>p Polynomial.monom (1::'a) 2) n + (if 1 \<le> n then (1::'a) * poly.coeff (h \<circ>\<^sub>p Polynomial.monom (1::'a) 2) (n - 1) else (0::'a))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. m = 0 \<Longrightarrow> poly.coeff f n = poly.coeff (g \<circ>\<^sub>p Polynomial.monom (1::'a) 2) n + (if 1 \<le> n then (1::'a) * poly.coeff (h \<circ>\<^sub>p Polynomial.monom (1::'a) 2) (n - 1) else (0::'a))
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
m = 0

goal (1 subgoal):
 1. m = 0 \<Longrightarrow> poly.coeff f n = poly.coeff (g \<circ>\<^sub>p Polynomial.monom (1::'a) 2) n + (if 1 \<le> n then (1::'a) * poly.coeff (h \<circ>\<^sub>p Polynomial.monom (1::'a) 2) (n - 1) else (0::'a))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly.coeff f n = poly.coeff (g \<circ>\<^sub>p Polynomial.monom (1::'a) 2) n + (if 1 \<le> n then (1::'a) * poly.coeff (h \<circ>\<^sub>p Polynomial.monom (1::'a) 2) (n - 1) else (0::'a))
[PROOF STEP]
unfolding nmi id coeff_pcompose_monom[OF nmi(2)]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly.coeff f (2 * m + i) = (if i = 0 then poly.coeff f (2 * m) else (0::'a)) + (if 1 \<le> 2 * m + i then (1::'a) * poly.coeff (h \<circ>\<^sub>p Polynomial.monom (1::'a) 2) (2 * m + i - 1) else (0::'a))
[PROOF STEP]
unfolding i0 0
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly.coeff f (2 * 0 + 0) = (if 0 = 0 then poly.coeff f (2 * 0) else (0::'a)) + (if 1 \<le> 2 * 0 + 0 then (1::'a) * poly.coeff (h \<circ>\<^sub>p Polynomial.monom (1::'a) 2) (2 * 0 + 0 - 1) else (0::'a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
poly.coeff f n = poly.coeff (g \<circ>\<^sub>p Polynomial.monom (1::'a) 2) n + (if 1 \<le> n then (1::'a) * poly.coeff (h \<circ>\<^sub>p Polynomial.monom (1::'a) 2) (n - 1) else (0::'a))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
poly.coeff f n = poly.coeff (g \<circ>\<^sub>p Polynomial.monom (1::'a) 2) n + (if 1 \<le> n then (1::'a) * poly.coeff (h \<circ>\<^sub>p Polynomial.monom (1::'a) 2) (n - 1) else (0::'a))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
poly.coeff f n = poly.coeff (g \<circ>\<^sub>p Polynomial.monom (1::'a) 2) n + (if 1 \<le> n then (1::'a) * poly.coeff (h \<circ>\<^sub>p Polynomial.monom (1::'a) 2) (n - 1) else (0::'a))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f = g \<circ>\<^sub>p Polynomial.monom (1::'a) 2 + Polynomial.monom (1::'a) 1 * h \<circ>\<^sub>p Polynomial.monom (1::'a) 2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma graeffe_0: "f = smult c (\<Prod>a\<leftarrow>as. [:- a, 1:]) \<Longrightarrow> graeffe_poly c as 0 = f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f = Polynomial.smult c (\<Prod>a\<leftarrow>as. [:- a, 1::'a:]) \<Longrightarrow> graeffe_poly c as 0 = f
[PROOF STEP]
unfolding graeffe_poly_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f = Polynomial.smult c (\<Prod>a\<leftarrow>as. [:- a, 1::'a:]) \<Longrightarrow> Polynomial.smult (c ^ 2 ^ 0) (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ 0), 1::'a:]) = f
[PROOF STEP]
by auto