[STATEMENT]
lemma graeffe_recursion: assumes "graeffe_poly c as m = f"
  shows "graeffe_poly c as (Suc m) = smult ((-1)^(degree f)) (poly_square_subst (f * f \<circ>\<^sub>p [:0,-1:]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. graeffe_poly c as (Suc m) = Polynomial.smult ((- (1::'a)) ^ degree f) (poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. graeffe_poly c as (Suc m) = Polynomial.smult ((- (1::'a)) ^ degree f) (poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]))
[PROOF STEP]
let ?g = "graeffe_poly c as m"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. graeffe_poly c as (Suc m) = Polynomial.smult ((- (1::'a)) ^ degree f) (poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]))
[PROOF STEP]
have "f * f \<circ>\<^sub>p [:0,-1:] = ?g * ?g \<circ>\<^sub>p [:0,-1:]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f * f \<circ>\<^sub>p [:0::'a, - (1::'a):] = graeffe_poly c as m * graeffe_poly c as m \<circ>\<^sub>p [:0::'a, - (1::'a):]
[PROOF STEP]
unfolding assms
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f * f \<circ>\<^sub>p [:0::'a, - (1::'a):] = f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f * f \<circ>\<^sub>p [:0::'a, - (1::'a):] = graeffe_poly c as m * graeffe_poly c as m \<circ>\<^sub>p [:0::'a, - (1::'a):]

goal (1 subgoal):
 1. graeffe_poly c as (Suc m) = Polynomial.smult ((- (1::'a)) ^ degree f) (poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f * f \<circ>\<^sub>p [:0::'a, - (1::'a):] = graeffe_poly c as m * graeffe_poly c as m \<circ>\<^sub>p [:0::'a, - (1::'a):]

goal (1 subgoal):
 1. graeffe_poly c as (Suc m) = Polynomial.smult ((- (1::'a)) ^ degree f) (poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]))
[PROOF STEP]
have "?g \<circ>\<^sub>p [:0,-1:] = smult ((- 1) ^ length as) (smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1:]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. graeffe_poly c as m \<circ>\<^sub>p [:0::'a, - (1::'a):] = Polynomial.smult ((- (1::'a)) ^ length as) (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:]))
[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::'a:]) \<circ>\<^sub>p [:0::'a, - (1::'a):] = Polynomial.smult ((- (1::'a)) ^ length as) (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:]))
[PROOF STEP]
proof (induct as)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>[]. [:- (a ^ 2 ^ m), 1::'a:]) \<circ>\<^sub>p [:0::'a, - (1::'a):] = Polynomial.smult ((- (1::'a)) ^ length []) (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>[]. [:a ^ 2 ^ m, 1::'a:]))
 2. \<And>a as. Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:]) \<circ>\<^sub>p [:0::'a, - (1::'a):] = Polynomial.smult ((- (1::'a)) ^ length as) (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:])) \<Longrightarrow> Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>a # as. [:- (a ^ 2 ^ m), 1::'a:]) \<circ>\<^sub>p [:0::'a, - (1::'a):] = Polynomial.smult ((- (1::'a)) ^ length (a # as)) (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>a # as. [:a ^ 2 ^ m, 1::'a:]))
[PROOF STEP]
case (Cons a as)
[PROOF STATE]
proof (state)
this:
Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:]) \<circ>\<^sub>p [:0::'a, - (1::'a):] = Polynomial.smult ((- (1::'a)) ^ length as) (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:]))

goal (2 subgoals):
 1. Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>[]. [:- (a ^ 2 ^ m), 1::'a:]) \<circ>\<^sub>p [:0::'a, - (1::'a):] = Polynomial.smult ((- (1::'a)) ^ length []) (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>[]. [:a ^ 2 ^ m, 1::'a:]))
 2. \<And>a as. Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:]) \<circ>\<^sub>p [:0::'a, - (1::'a):] = Polynomial.smult ((- (1::'a)) ^ length as) (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:])) \<Longrightarrow> Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>a # as. [:- (a ^ 2 ^ m), 1::'a:]) \<circ>\<^sub>p [:0::'a, - (1::'a):] = Polynomial.smult ((- (1::'a)) ^ length (a # as)) (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>a # as. [:a ^ 2 ^ m, 1::'a:]))
[PROOF STEP]
have "?case = ((smult (c ^ 2 ^ m) ([:- (a ^ 2 ^ m), 1:] \<circ>\<^sub>p [:0, - 1:] * (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1:]) \<circ>\<^sub>p [:0, - 1:]) =
     smult (-1 * (- 1) ^ length as)
      (smult (c ^ 2 ^ m) ([: a ^ 2 ^ m, 1:] * (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1:])))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>a # as. [:- (a ^ 2 ^ m), 1::'a:]) \<circ>\<^sub>p [:0::'a, - (1::'a):] = Polynomial.smult ((- (1::'a)) ^ length (a # as)) (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>a # as. [:a ^ 2 ^ m, 1::'a:]))) = (Polynomial.smult (c ^ 2 ^ m) ([:- (a ^ 2 ^ m), 1::'a:] \<circ>\<^sub>p [:0::'a, - (1::'a):] * (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:]) \<circ>\<^sub>p [:0::'a, - (1::'a):]) = Polynomial.smult (- (1::'a) * (- (1::'a)) ^ length as) (Polynomial.smult (c ^ 2 ^ m) ([:a ^ 2 ^ m, 1::'a:] * (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:]))))
[PROOF STEP]
unfolding list.simps prod_list.Cons pcompose_smult pcompose_mult
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Polynomial.smult (c ^ 2 ^ m) ([:- (a ^ 2 ^ m), 1::'a:] \<circ>\<^sub>p [:0::'a, - (1::'a):] * (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:]) \<circ>\<^sub>p [:0::'a, - (1::'a):]) = Polynomial.smult ((- (1::'a)) ^ length (a # as)) (Polynomial.smult (c ^ 2 ^ m) ([:a ^ 2 ^ m, 1::'a:] * (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:])))) = (Polynomial.smult (c ^ 2 ^ m) ([:- (a ^ 2 ^ m), 1::'a:] \<circ>\<^sub>p [:0::'a, - (1::'a):] * (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:]) \<circ>\<^sub>p [:0::'a, - (1::'a):]) = Polynomial.smult (- (1::'a) * (- (1::'a)) ^ length as) (Polynomial.smult (c ^ 2 ^ m) ([:a ^ 2 ^ m, 1::'a:] * (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:]))))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>a # as. [:- (a ^ 2 ^ m), 1::'a:]) \<circ>\<^sub>p [:0::'a, - (1::'a):] = Polynomial.smult ((- (1::'a)) ^ length (a # as)) (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>a # as. [:a ^ 2 ^ m, 1::'a:]))) = (Polynomial.smult (c ^ 2 ^ m) ([:- (a ^ 2 ^ m), 1::'a:] \<circ>\<^sub>p [:0::'a, - (1::'a):] * (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:]) \<circ>\<^sub>p [:0::'a, - (1::'a):]) = Polynomial.smult (- (1::'a) * (- (1::'a)) ^ length as) (Polynomial.smult (c ^ 2 ^ m) ([:a ^ 2 ^ m, 1::'a:] * (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:]))))

goal (2 subgoals):
 1. Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>[]. [:- (a ^ 2 ^ m), 1::'a:]) \<circ>\<^sub>p [:0::'a, - (1::'a):] = Polynomial.smult ((- (1::'a)) ^ length []) (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>[]. [:a ^ 2 ^ m, 1::'a:]))
 2. \<And>a as. Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:]) \<circ>\<^sub>p [:0::'a, - (1::'a):] = Polynomial.smult ((- (1::'a)) ^ length as) (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:])) \<Longrightarrow> Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>a # as. [:- (a ^ 2 ^ m), 1::'a:]) \<circ>\<^sub>p [:0::'a, - (1::'a):] = Polynomial.smult ((- (1::'a)) ^ length (a # as)) (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>a # as. [:a ^ 2 ^ m, 1::'a:]))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>a # as. [:- (a ^ 2 ^ m), 1::'a:]) \<circ>\<^sub>p [:0::'a, - (1::'a):] = Polynomial.smult ((- (1::'a)) ^ length (a # as)) (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>a # as. [:a ^ 2 ^ m, 1::'a:]))) = (Polynomial.smult (c ^ 2 ^ m) ([:- (a ^ 2 ^ m), 1::'a:] \<circ>\<^sub>p [:0::'a, - (1::'a):] * (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:]) \<circ>\<^sub>p [:0::'a, - (1::'a):]) = Polynomial.smult (- (1::'a) * (- (1::'a)) ^ length as) (Polynomial.smult (c ^ 2 ^ m) ([:a ^ 2 ^ m, 1::'a:] * (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:]))))

goal (2 subgoals):
 1. Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>[]. [:- (a ^ 2 ^ m), 1::'a:]) \<circ>\<^sub>p [:0::'a, - (1::'a):] = Polynomial.smult ((- (1::'a)) ^ length []) (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>[]. [:a ^ 2 ^ m, 1::'a:]))
 2. \<And>a as. Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:]) \<circ>\<^sub>p [:0::'a, - (1::'a):] = Polynomial.smult ((- (1::'a)) ^ length as) (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:])) \<Longrightarrow> Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>a # as. [:- (a ^ 2 ^ m), 1::'a:]) \<circ>\<^sub>p [:0::'a, - (1::'a):] = Polynomial.smult ((- (1::'a)) ^ length (a # as)) (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>a # as. [:a ^ 2 ^ m, 1::'a:]))
[PROOF STEP]
have "smult (c ^ 2 ^ m) ([:- (a ^ 2 ^ m), 1:] \<circ>\<^sub>p [:0, - 1:] * (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1:]) \<circ>\<^sub>p [:0, - 1:])
      = smult (c ^ 2 ^ m) ((\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1:]) \<circ>\<^sub>p [:0, - 1:]) * [:- (a ^ 2 ^ m), 1:] \<circ>\<^sub>p [:0, - 1:]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Polynomial.smult (c ^ 2 ^ m) ([:- (a ^ 2 ^ m), 1::'a:] \<circ>\<^sub>p [:0::'a, - (1::'a):] * (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:]) \<circ>\<^sub>p [:0::'a, - (1::'a):]) = Polynomial.smult (c ^ 2 ^ m) ((\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:]) \<circ>\<^sub>p [:0::'a, - (1::'a):]) * [:- (a ^ 2 ^ m), 1::'a:] \<circ>\<^sub>p [:0::'a, - (1::'a):]
[PROOF STEP]
unfolding mult_smult_left
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Polynomial.smult (c ^ 2 ^ m) ([:- (a ^ 2 ^ m), 1::'a:] \<circ>\<^sub>p [:0::'a, - (1::'a):] * (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:]) \<circ>\<^sub>p [:0::'a, - (1::'a):]) = Polynomial.smult (c ^ 2 ^ m) ((\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:]) \<circ>\<^sub>p [:0::'a, - (1::'a):] * [:- (a ^ 2 ^ m), 1::'a:] \<circ>\<^sub>p [:0::'a, - (1::'a):])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Polynomial.smult (c ^ 2 ^ m) ([:- (a ^ 2 ^ m), 1::'a:] \<circ>\<^sub>p [:0::'a, - (1::'a):] * (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:]) \<circ>\<^sub>p [:0::'a, - (1::'a):]) = Polynomial.smult (c ^ 2 ^ m) ((\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:]) \<circ>\<^sub>p [:0::'a, - (1::'a):]) * [:- (a ^ 2 ^ m), 1::'a:] \<circ>\<^sub>p [:0::'a, - (1::'a):]

goal (2 subgoals):
 1. Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>[]. [:- (a ^ 2 ^ m), 1::'a:]) \<circ>\<^sub>p [:0::'a, - (1::'a):] = Polynomial.smult ((- (1::'a)) ^ length []) (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>[]. [:a ^ 2 ^ m, 1::'a:]))
 2. \<And>a as. Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:]) \<circ>\<^sub>p [:0::'a, - (1::'a):] = Polynomial.smult ((- (1::'a)) ^ length as) (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:])) \<Longrightarrow> Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>a # as. [:- (a ^ 2 ^ m), 1::'a:]) \<circ>\<^sub>p [:0::'a, - (1::'a):] = Polynomial.smult ((- (1::'a)) ^ length (a # as)) (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>a # as. [:a ^ 2 ^ m, 1::'a:]))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Polynomial.smult (c ^ 2 ^ m) ([:- (a ^ 2 ^ m), 1::'a:] \<circ>\<^sub>p [:0::'a, - (1::'a):] * (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:]) \<circ>\<^sub>p [:0::'a, - (1::'a):]) = Polynomial.smult (c ^ 2 ^ m) ((\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:]) \<circ>\<^sub>p [:0::'a, - (1::'a):]) * [:- (a ^ 2 ^ m), 1::'a:] \<circ>\<^sub>p [:0::'a, - (1::'a):]

goal (2 subgoals):
 1. Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>[]. [:- (a ^ 2 ^ m), 1::'a:]) \<circ>\<^sub>p [:0::'a, - (1::'a):] = Polynomial.smult ((- (1::'a)) ^ length []) (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>[]. [:a ^ 2 ^ m, 1::'a:]))
 2. \<And>a as. Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:]) \<circ>\<^sub>p [:0::'a, - (1::'a):] = Polynomial.smult ((- (1::'a)) ^ length as) (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:])) \<Longrightarrow> Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>a # as. [:- (a ^ 2 ^ m), 1::'a:]) \<circ>\<^sub>p [:0::'a, - (1::'a):] = Polynomial.smult ((- (1::'a)) ^ length (a # as)) (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>a # as. [:a ^ 2 ^ m, 1::'a:]))
[PROOF STEP]
have "smult (c ^ 2 ^ m) ((\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1:]) \<circ>\<^sub>p [:0, - 1:]) =
      smult ((- 1) ^ length as) (smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1:]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Polynomial.smult (c ^ 2 ^ m) ((\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:]) \<circ>\<^sub>p [:0::'a, - (1::'a):]) = Polynomial.smult ((- (1::'a)) ^ length as) (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:]))
[PROOF STEP]
unfolding pcompose_smult[symmetric] Cons
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Polynomial.smult ((- (1::'a)) ^ length as) (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:])) = Polynomial.smult ((- (1::'a)) ^ length as) (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:]))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
Polynomial.smult (c ^ 2 ^ m) ((\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:]) \<circ>\<^sub>p [:0::'a, - (1::'a):]) = Polynomial.smult ((- (1::'a)) ^ length as) (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:]))

goal (2 subgoals):
 1. Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>[]. [:- (a ^ 2 ^ m), 1::'a:]) \<circ>\<^sub>p [:0::'a, - (1::'a):] = Polynomial.smult ((- (1::'a)) ^ length []) (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>[]. [:a ^ 2 ^ m, 1::'a:]))
 2. \<And>a as. Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:]) \<circ>\<^sub>p [:0::'a, - (1::'a):] = Polynomial.smult ((- (1::'a)) ^ length as) (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:])) \<Longrightarrow> Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>a # as. [:- (a ^ 2 ^ m), 1::'a:]) \<circ>\<^sub>p [:0::'a, - (1::'a):] = Polynomial.smult ((- (1::'a)) ^ length (a # as)) (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>a # as. [:a ^ 2 ^ m, 1::'a:]))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Polynomial.smult (c ^ 2 ^ m) ((\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:]) \<circ>\<^sub>p [:0::'a, - (1::'a):]) = Polynomial.smult ((- (1::'a)) ^ length as) (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:]))

goal (2 subgoals):
 1. Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>[]. [:- (a ^ 2 ^ m), 1::'a:]) \<circ>\<^sub>p [:0::'a, - (1::'a):] = Polynomial.smult ((- (1::'a)) ^ length []) (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>[]. [:a ^ 2 ^ m, 1::'a:]))
 2. \<And>a as. Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:]) \<circ>\<^sub>p [:0::'a, - (1::'a):] = Polynomial.smult ((- (1::'a)) ^ length as) (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:])) \<Longrightarrow> Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>a # as. [:- (a ^ 2 ^ m), 1::'a:]) \<circ>\<^sub>p [:0::'a, - (1::'a):] = Polynomial.smult ((- (1::'a)) ^ length (a # as)) (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>a # as. [:a ^ 2 ^ m, 1::'a:]))
[PROOF STEP]
have "[:- (a ^ 2 ^ m), 1:] \<circ>\<^sub>p [:0, - 1:] = smult (-1) [: a^2^m, 1:]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [:- (a ^ 2 ^ m), 1::'a:] \<circ>\<^sub>p [:0::'a, - (1::'a):] = Polynomial.smult (- (1::'a)) [:a ^ 2 ^ m, 1::'a:]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[:- (a ^ 2 ^ m), 1::'a:] \<circ>\<^sub>p [:0::'a, - (1::'a):] = Polynomial.smult (- (1::'a)) [:a ^ 2 ^ m, 1::'a:]

goal (2 subgoals):
 1. Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>[]. [:- (a ^ 2 ^ m), 1::'a:]) \<circ>\<^sub>p [:0::'a, - (1::'a):] = Polynomial.smult ((- (1::'a)) ^ length []) (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>[]. [:a ^ 2 ^ m, 1::'a:]))
 2. \<And>a as. Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:]) \<circ>\<^sub>p [:0::'a, - (1::'a):] = Polynomial.smult ((- (1::'a)) ^ length as) (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:])) \<Longrightarrow> Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>a # as. [:- (a ^ 2 ^ m), 1::'a:]) \<circ>\<^sub>p [:0::'a, - (1::'a):] = Polynomial.smult ((- (1::'a)) ^ length (a # as)) (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>a # as. [:a ^ 2 ^ m, 1::'a:]))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>a # as. [:- (a ^ 2 ^ m), 1::'a:]) \<circ>\<^sub>p [:0::'a, - (1::'a):] = Polynomial.smult ((- (1::'a)) ^ length (a # as)) (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>a # as. [:a ^ 2 ^ m, 1::'a:]))) = (Polynomial.smult ((- (1::'a)) ^ length as) (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:])) * Polynomial.smult (- (1::'a)) [:a ^ 2 ^ m, 1::'a:] = Polynomial.smult (- (1::'a) * (- (1::'a)) ^ length as) (Polynomial.smult (c ^ 2 ^ m) ([:a ^ 2 ^ m, 1::'a:] * (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:]))))
[PROOF STEP]
have id: "?case = (smult ((- 1) ^ length as) (smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1:])) * smult (- 1) [:a ^ 2 ^ m, 1:] =
      smult (- 1 * (- 1) ^ length as) (smult (c ^ 2 ^ m) ([:a ^ 2 ^ m, 1:] * (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1:]))))"
[PROOF STATE]
proof (prove)
using this:
(Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>a # as. [:- (a ^ 2 ^ m), 1::'a:]) \<circ>\<^sub>p [:0::'a, - (1::'a):] = Polynomial.smult ((- (1::'a)) ^ length (a # as)) (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>a # as. [:a ^ 2 ^ m, 1::'a:]))) = (Polynomial.smult ((- (1::'a)) ^ length as) (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:])) * Polynomial.smult (- (1::'a)) [:a ^ 2 ^ m, 1::'a:] = Polynomial.smult (- (1::'a) * (- (1::'a)) ^ length as) (Polynomial.smult (c ^ 2 ^ m) ([:a ^ 2 ^ m, 1::'a:] * (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:]))))

goal (1 subgoal):
 1. (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>a # as. [:- (a ^ 2 ^ m), 1::'a:]) \<circ>\<^sub>p [:0::'a, - (1::'a):] = Polynomial.smult ((- (1::'a)) ^ length (a # as)) (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>a # as. [:a ^ 2 ^ m, 1::'a:]))) = (Polynomial.smult ((- (1::'a)) ^ length as) (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:])) * Polynomial.smult (- (1::'a)) [:a ^ 2 ^ m, 1::'a:] = Polynomial.smult (- (1::'a) * (- (1::'a)) ^ length as) (Polynomial.smult (c ^ 2 ^ m) ([:a ^ 2 ^ m, 1::'a:] * (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:]))))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>a # as. [:- (a ^ 2 ^ m), 1::'a:]) \<circ>\<^sub>p [:0::'a, - (1::'a):] = Polynomial.smult ((- (1::'a)) ^ length (a # as)) (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>a # as. [:a ^ 2 ^ m, 1::'a:]))) = (Polynomial.smult ((- (1::'a)) ^ length as) (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:])) * Polynomial.smult (- (1::'a)) [:a ^ 2 ^ m, 1::'a:] = Polynomial.smult (- (1::'a) * (- (1::'a)) ^ length as) (Polynomial.smult (c ^ 2 ^ m) ([:a ^ 2 ^ m, 1::'a:] * (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:]))))

goal (2 subgoals):
 1. Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>[]. [:- (a ^ 2 ^ m), 1::'a:]) \<circ>\<^sub>p [:0::'a, - (1::'a):] = Polynomial.smult ((- (1::'a)) ^ length []) (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>[]. [:a ^ 2 ^ m, 1::'a:]))
 2. \<And>a as. Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:]) \<circ>\<^sub>p [:0::'a, - (1::'a):] = Polynomial.smult ((- (1::'a)) ^ length as) (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:])) \<Longrightarrow> Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>a # as. [:- (a ^ 2 ^ m), 1::'a:]) \<circ>\<^sub>p [:0::'a, - (1::'a):] = Polynomial.smult ((- (1::'a)) ^ length (a # as)) (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>a # as. [:a ^ 2 ^ m, 1::'a:]))
[PROOF STEP]
obtain c d where id': "(\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1:]) = c" "[:a ^ 2 ^ m, 1:] = d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>c d. \<lbrakk>(\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:]) = c; [:a ^ 2 ^ m, 1::'a:] = d\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:]) = c
[:a ^ 2 ^ m, 1::'a:] = d

goal (2 subgoals):
 1. Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>[]. [:- (a ^ 2 ^ m), 1::'a:]) \<circ>\<^sub>p [:0::'a, - (1::'a):] = Polynomial.smult ((- (1::'a)) ^ length []) (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>[]. [:a ^ 2 ^ m, 1::'a:]))
 2. \<And>a as. Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:]) \<circ>\<^sub>p [:0::'a, - (1::'a):] = Polynomial.smult ((- (1::'a)) ^ length as) (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:])) \<Longrightarrow> Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>a # as. [:- (a ^ 2 ^ m), 1::'a:]) \<circ>\<^sub>p [:0::'a, - (1::'a):] = Polynomial.smult ((- (1::'a)) ^ length (a # as)) (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>a # as. [:a ^ 2 ^ m, 1::'a:]))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>a # as. [:- (a ^ 2 ^ m), 1::'a:]) \<circ>\<^sub>p [:0::'a, - (1::'a):] = Polynomial.smult ((- (1::'a)) ^ length (a # as)) (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>a # as. [:a ^ 2 ^ m, 1::'a:]))
[PROOF STEP]
unfolding id
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Polynomial.smult ((- (1::'a)) ^ length as) (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:])) * Polynomial.smult (- (1::'a)) [:a ^ 2 ^ m, 1::'a:] = Polynomial.smult (- (1::'a) * (- (1::'a)) ^ length as) (Polynomial.smult (c ^ 2 ^ m) ([:a ^ 2 ^ m, 1::'a:] * (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:])))
[PROOF STEP]
unfolding id'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Polynomial.smult ((- (1::'a)) ^ length as) (Polynomial.smult (c ^ 2 ^ m) c) * Polynomial.smult (- (1::'a)) d = Polynomial.smult (- (1::'a) * (- (1::'a)) ^ length as) (Polynomial.smult (c ^ 2 ^ m) (d * c))
[PROOF STEP]
by (simp add: ac_simps)
[PROOF STATE]
proof (state)
this:
Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>a # as. [:- (a ^ 2 ^ m), 1::'a:]) \<circ>\<^sub>p [:0::'a, - (1::'a):] = Polynomial.smult ((- (1::'a)) ^ length (a # as)) (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>a # as. [:a ^ 2 ^ m, 1::'a:]))

goal (1 subgoal):
 1. Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>[]. [:- (a ^ 2 ^ m), 1::'a:]) \<circ>\<^sub>p [:0::'a, - (1::'a):] = Polynomial.smult ((- (1::'a)) ^ length []) (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>[]. [:a ^ 2 ^ m, 1::'a:]))
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
graeffe_poly c as m \<circ>\<^sub>p [:0::'a, - (1::'a):] = Polynomial.smult ((- (1::'a)) ^ length as) (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:]))

goal (1 subgoal):
 1. graeffe_poly c as (Suc m) = Polynomial.smult ((- (1::'a)) ^ degree f) (poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
f * f \<circ>\<^sub>p [:0::'a, - (1::'a):] = graeffe_poly c as m * Polynomial.smult ((- (1::'a)) ^ length as) (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:]))
[PROOF STEP]
have "f * f \<circ>\<^sub>p [:0, - 1:] =
    smult ((- 1) ^ length as * (c ^ 2 ^ m * c ^ 2 ^ m))
    ((\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1:]) * (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1:]))"
[PROOF STATE]
proof (prove)
using this:
f * f \<circ>\<^sub>p [:0::'a, - (1::'a):] = graeffe_poly c as m * Polynomial.smult ((- (1::'a)) ^ length as) (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:]))

goal (1 subgoal):
 1. f * f \<circ>\<^sub>p [:0::'a, - (1::'a):] = Polynomial.smult ((- (1::'a)) ^ length as * (c ^ 2 ^ m * c ^ 2 ^ m)) ((\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:]) * (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:]))
[PROOF STEP]
unfolding graeffe_poly_def
[PROOF STATE]
proof (prove)
using this:
f * f \<circ>\<^sub>p [:0::'a, - (1::'a):] = Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:]) * Polynomial.smult ((- (1::'a)) ^ length as) (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:]))

goal (1 subgoal):
 1. f * f \<circ>\<^sub>p [:0::'a, - (1::'a):] = Polynomial.smult ((- (1::'a)) ^ length as * (c ^ 2 ^ m * c ^ 2 ^ m)) ((\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:]) * (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:]))
[PROOF STEP]
by (simp add: ac_simps)
[PROOF STATE]
proof (state)
this:
f * f \<circ>\<^sub>p [:0::'a, - (1::'a):] = Polynomial.smult ((- (1::'a)) ^ length as * (c ^ 2 ^ m * c ^ 2 ^ m)) ((\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:]) * (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:]))

goal (1 subgoal):
 1. graeffe_poly c as (Suc m) = Polynomial.smult ((- (1::'a)) ^ degree f) (poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f * f \<circ>\<^sub>p [:0::'a, - (1::'a):] = Polynomial.smult ((- (1::'a)) ^ length as * (c ^ 2 ^ m * c ^ 2 ^ m)) ((\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:]) * (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:]))

goal (1 subgoal):
 1. graeffe_poly c as (Suc m) = Polynomial.smult ((- (1::'a)) ^ degree f) (poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]))
[PROOF STEP]
have "c ^ 2 ^ m * c ^ 2 ^ m = c ^ 2 ^ (Suc m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c ^ 2 ^ m * c ^ 2 ^ m = c ^ 2 ^ Suc m
[PROOF STEP]
by (simp add: semiring_normalization_rules(36))
[PROOF STATE]
proof (state)
this:
c ^ 2 ^ m * c ^ 2 ^ m = c ^ 2 ^ Suc m

goal (1 subgoal):
 1. graeffe_poly c as (Suc m) = Polynomial.smult ((- (1::'a)) ^ degree f) (poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
c ^ 2 ^ m * c ^ 2 ^ m = c ^ 2 ^ Suc m

goal (1 subgoal):
 1. graeffe_poly c as (Suc m) = Polynomial.smult ((- (1::'a)) ^ degree f) (poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]))
[PROOF STEP]
have "(\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1:]) * (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1:]) =
    (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ (Suc m)), 1:]) \<circ>\<^sub>p monom 1 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:]) * (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:]) = (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ Suc m), 1::'a:]) \<circ>\<^sub>p Polynomial.monom (1::'a) 2
[PROOF STEP]
proof (induct as)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<Prod>a\<leftarrow>[]. [:- (a ^ 2 ^ m), 1::'a:]) * (\<Prod>a\<leftarrow>[]. [:a ^ 2 ^ m, 1::'a:]) = (\<Prod>a\<leftarrow>[]. [:- (a ^ 2 ^ Suc m), 1::'a:]) \<circ>\<^sub>p Polynomial.monom (1::'a) 2
 2. \<And>a as. (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:]) * (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:]) = (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ Suc m), 1::'a:]) \<circ>\<^sub>p Polynomial.monom (1::'a) 2 \<Longrightarrow> (\<Prod>a\<leftarrow>a # as. [:- (a ^ 2 ^ m), 1::'a:]) * (\<Prod>a\<leftarrow>a # as. [:a ^ 2 ^ m, 1::'a:]) = (\<Prod>a\<leftarrow>a # as. [:- (a ^ 2 ^ Suc m), 1::'a:]) \<circ>\<^sub>p Polynomial.monom (1::'a) 2
[PROOF STEP]
case (Cons a as)
[PROOF STATE]
proof (state)
this:
(\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:]) * (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:]) = (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ Suc m), 1::'a:]) \<circ>\<^sub>p Polynomial.monom (1::'a) 2

goal (2 subgoals):
 1. (\<Prod>a\<leftarrow>[]. [:- (a ^ 2 ^ m), 1::'a:]) * (\<Prod>a\<leftarrow>[]. [:a ^ 2 ^ m, 1::'a:]) = (\<Prod>a\<leftarrow>[]. [:- (a ^ 2 ^ Suc m), 1::'a:]) \<circ>\<^sub>p Polynomial.monom (1::'a) 2
 2. \<And>a as. (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:]) * (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:]) = (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ Suc m), 1::'a:]) \<circ>\<^sub>p Polynomial.monom (1::'a) 2 \<Longrightarrow> (\<Prod>a\<leftarrow>a # as. [:- (a ^ 2 ^ m), 1::'a:]) * (\<Prod>a\<leftarrow>a # as. [:a ^ 2 ^ m, 1::'a:]) = (\<Prod>a\<leftarrow>a # as. [:- (a ^ 2 ^ Suc m), 1::'a:]) \<circ>\<^sub>p Polynomial.monom (1::'a) 2
[PROOF STEP]
have id: "(monom 1 2 :: 'a poly) = [:0,0,1:]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Polynomial.monom (1::'a) 2 = [:0::'a, 0::'a, 1::'a:]
[PROOF STEP]
by (metis monom_altdef pCons_0_as_mult power2_eq_square smult_1_left)
[PROOF STATE]
proof (state)
this:
Polynomial.monom (1::'a) 2 = [:0::'a, 0::'a, 1::'a:]

goal (2 subgoals):
 1. (\<Prod>a\<leftarrow>[]. [:- (a ^ 2 ^ m), 1::'a:]) * (\<Prod>a\<leftarrow>[]. [:a ^ 2 ^ m, 1::'a:]) = (\<Prod>a\<leftarrow>[]. [:- (a ^ 2 ^ Suc m), 1::'a:]) \<circ>\<^sub>p Polynomial.monom (1::'a) 2
 2. \<And>a as. (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:]) * (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:]) = (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ Suc m), 1::'a:]) \<circ>\<^sub>p Polynomial.monom (1::'a) 2 \<Longrightarrow> (\<Prod>a\<leftarrow>a # as. [:- (a ^ 2 ^ m), 1::'a:]) * (\<Prod>a\<leftarrow>a # as. [:a ^ 2 ^ m, 1::'a:]) = (\<Prod>a\<leftarrow>a # as. [:- (a ^ 2 ^ Suc m), 1::'a:]) \<circ>\<^sub>p Polynomial.monom (1::'a) 2
[PROOF STEP]
have "(\<Prod>a\<leftarrow>a # as. [:- (a ^ 2 ^ m), 1:]) * (\<Prod>a\<leftarrow>a # as. [:a ^ 2 ^ m, 1:])
      = ([:- (a ^ 2 ^ m), 1:] * [: a ^ 2 ^ m, 1:]) * ((\<Prod>a\<leftarrow> as. [:- (a ^ 2 ^ m), 1:]) * (\<Prod>a\<leftarrow> as. [:a ^ 2 ^ m, 1:]))"
        (is "_ = ?a * ?b")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>a\<leftarrow>a # as. [:- (a ^ 2 ^ m), 1::'a:]) * (\<Prod>a\<leftarrow>a # as. [:a ^ 2 ^ m, 1::'a:]) = [:- (a ^ 2 ^ m), 1::'a:] * [:a ^ 2 ^ m, 1::'a:] * ((\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:]) * (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:]))
[PROOF STEP]
unfolding list.simps prod_list.Cons
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [:- (a ^ 2 ^ m), 1::'a:] * (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:]) * ([:a ^ 2 ^ m, 1::'a:] * (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:])) = [:- (a ^ 2 ^ m), 1::'a:] * [:a ^ 2 ^ m, 1::'a:] * ((\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:]) * (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:]))
[PROOF STEP]
by (simp only: ac_simps)
[PROOF STATE]
proof (state)
this:
(\<Prod>a\<leftarrow>a # as. [:- (a ^ 2 ^ m), 1::'a:]) * (\<Prod>a\<leftarrow>a # as. [:a ^ 2 ^ m, 1::'a:]) = [:- (a ^ 2 ^ m), 1::'a:] * [:a ^ 2 ^ m, 1::'a:] * ((\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:]) * (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:]))

goal (2 subgoals):
 1. (\<Prod>a\<leftarrow>[]. [:- (a ^ 2 ^ m), 1::'a:]) * (\<Prod>a\<leftarrow>[]. [:a ^ 2 ^ m, 1::'a:]) = (\<Prod>a\<leftarrow>[]. [:- (a ^ 2 ^ Suc m), 1::'a:]) \<circ>\<^sub>p Polynomial.monom (1::'a) 2
 2. \<And>a as. (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:]) * (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:]) = (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ Suc m), 1::'a:]) \<circ>\<^sub>p Polynomial.monom (1::'a) 2 \<Longrightarrow> (\<Prod>a\<leftarrow>a # as. [:- (a ^ 2 ^ m), 1::'a:]) * (\<Prod>a\<leftarrow>a # as. [:a ^ 2 ^ m, 1::'a:]) = (\<Prod>a\<leftarrow>a # as. [:- (a ^ 2 ^ Suc m), 1::'a:]) \<circ>\<^sub>p Polynomial.monom (1::'a) 2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Prod>a\<leftarrow>a # as. [:- (a ^ 2 ^ m), 1::'a:]) * (\<Prod>a\<leftarrow>a # as. [:a ^ 2 ^ m, 1::'a:]) = [:- (a ^ 2 ^ m), 1::'a:] * [:a ^ 2 ^ m, 1::'a:] * ((\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:]) * (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:]))

goal (2 subgoals):
 1. (\<Prod>a\<leftarrow>[]. [:- (a ^ 2 ^ m), 1::'a:]) * (\<Prod>a\<leftarrow>[]. [:a ^ 2 ^ m, 1::'a:]) = (\<Prod>a\<leftarrow>[]. [:- (a ^ 2 ^ Suc m), 1::'a:]) \<circ>\<^sub>p Polynomial.monom (1::'a) 2
 2. \<And>a as. (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:]) * (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:]) = (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ Suc m), 1::'a:]) \<circ>\<^sub>p Polynomial.monom (1::'a) 2 \<Longrightarrow> (\<Prod>a\<leftarrow>a # as. [:- (a ^ 2 ^ m), 1::'a:]) * (\<Prod>a\<leftarrow>a # as. [:a ^ 2 ^ m, 1::'a:]) = (\<Prod>a\<leftarrow>a # as. [:- (a ^ 2 ^ Suc m), 1::'a:]) \<circ>\<^sub>p Polynomial.monom (1::'a) 2
[PROOF STEP]
have "?b = (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ Suc m), 1:]) \<circ>\<^sub>p monom 1 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:]) * (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:]) = (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ Suc m), 1::'a:]) \<circ>\<^sub>p Polynomial.monom (1::'a) 2
[PROOF STEP]
unfolding Cons
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ Suc m), 1::'a:]) \<circ>\<^sub>p Polynomial.monom (1::'a) 2 = (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ Suc m), 1::'a:]) \<circ>\<^sub>p Polynomial.monom (1::'a) 2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:]) * (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:]) = (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ Suc m), 1::'a:]) \<circ>\<^sub>p Polynomial.monom (1::'a) 2

goal (2 subgoals):
 1. (\<Prod>a\<leftarrow>[]. [:- (a ^ 2 ^ m), 1::'a:]) * (\<Prod>a\<leftarrow>[]. [:a ^ 2 ^ m, 1::'a:]) = (\<Prod>a\<leftarrow>[]. [:- (a ^ 2 ^ Suc m), 1::'a:]) \<circ>\<^sub>p Polynomial.monom (1::'a) 2
 2. \<And>a as. (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:]) * (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:]) = (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ Suc m), 1::'a:]) \<circ>\<^sub>p Polynomial.monom (1::'a) 2 \<Longrightarrow> (\<Prod>a\<leftarrow>a # as. [:- (a ^ 2 ^ m), 1::'a:]) * (\<Prod>a\<leftarrow>a # as. [:a ^ 2 ^ m, 1::'a:]) = (\<Prod>a\<leftarrow>a # as. [:- (a ^ 2 ^ Suc m), 1::'a:]) \<circ>\<^sub>p Polynomial.monom (1::'a) 2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:]) * (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:]) = (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ Suc m), 1::'a:]) \<circ>\<^sub>p Polynomial.monom (1::'a) 2

goal (2 subgoals):
 1. (\<Prod>a\<leftarrow>[]. [:- (a ^ 2 ^ m), 1::'a:]) * (\<Prod>a\<leftarrow>[]. [:a ^ 2 ^ m, 1::'a:]) = (\<Prod>a\<leftarrow>[]. [:- (a ^ 2 ^ Suc m), 1::'a:]) \<circ>\<^sub>p Polynomial.monom (1::'a) 2
 2. \<And>a as. (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:]) * (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:]) = (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ Suc m), 1::'a:]) \<circ>\<^sub>p Polynomial.monom (1::'a) 2 \<Longrightarrow> (\<Prod>a\<leftarrow>a # as. [:- (a ^ 2 ^ m), 1::'a:]) * (\<Prod>a\<leftarrow>a # as. [:a ^ 2 ^ m, 1::'a:]) = (\<Prod>a\<leftarrow>a # as. [:- (a ^ 2 ^ Suc m), 1::'a:]) \<circ>\<^sub>p Polynomial.monom (1::'a) 2
[PROOF STEP]
have "?a = [: - (a ^ 2 ^ (Suc m)), 0 , 1:]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [:- (a ^ 2 ^ m), 1::'a:] * [:a ^ 2 ^ m, 1::'a:] = [:- (a ^ 2 ^ Suc m), 0::'a, 1::'a:]
[PROOF STEP]
by (simp add: semiring_normalization_rules(36))
[PROOF STATE]
proof (state)
this:
[:- (a ^ 2 ^ m), 1::'a:] * [:a ^ 2 ^ m, 1::'a:] = [:- (a ^ 2 ^ Suc m), 0::'a, 1::'a:]

goal (2 subgoals):
 1. (\<Prod>a\<leftarrow>[]. [:- (a ^ 2 ^ m), 1::'a:]) * (\<Prod>a\<leftarrow>[]. [:a ^ 2 ^ m, 1::'a:]) = (\<Prod>a\<leftarrow>[]. [:- (a ^ 2 ^ Suc m), 1::'a:]) \<circ>\<^sub>p Polynomial.monom (1::'a) 2
 2. \<And>a as. (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:]) * (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:]) = (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ Suc m), 1::'a:]) \<circ>\<^sub>p Polynomial.monom (1::'a) 2 \<Longrightarrow> (\<Prod>a\<leftarrow>a # as. [:- (a ^ 2 ^ m), 1::'a:]) * (\<Prod>a\<leftarrow>a # as. [:a ^ 2 ^ m, 1::'a:]) = (\<Prod>a\<leftarrow>a # as. [:- (a ^ 2 ^ Suc m), 1::'a:]) \<circ>\<^sub>p Polynomial.monom (1::'a) 2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
[:- (a ^ 2 ^ m), 1::'a:] * [:a ^ 2 ^ m, 1::'a:] = [:- (a ^ 2 ^ Suc m), 0::'a, 1::'a:]

goal (2 subgoals):
 1. (\<Prod>a\<leftarrow>[]. [:- (a ^ 2 ^ m), 1::'a:]) * (\<Prod>a\<leftarrow>[]. [:a ^ 2 ^ m, 1::'a:]) = (\<Prod>a\<leftarrow>[]. [:- (a ^ 2 ^ Suc m), 1::'a:]) \<circ>\<^sub>p Polynomial.monom (1::'a) 2
 2. \<And>a as. (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:]) * (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:]) = (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ Suc m), 1::'a:]) \<circ>\<^sub>p Polynomial.monom (1::'a) 2 \<Longrightarrow> (\<Prod>a\<leftarrow>a # as. [:- (a ^ 2 ^ m), 1::'a:]) * (\<Prod>a\<leftarrow>a # as. [:a ^ 2 ^ m, 1::'a:]) = (\<Prod>a\<leftarrow>a # as. [:- (a ^ 2 ^ Suc m), 1::'a:]) \<circ>\<^sub>p Polynomial.monom (1::'a) 2
[PROOF STEP]
have "\<dots> = [: - (a ^ 2 ^ (Suc m)), 1:] \<circ>\<^sub>p monom 1 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [:- (a ^ 2 ^ Suc m), 0::'a, 1::'a:] = [:- (a ^ 2 ^ Suc m), 1::'a:] \<circ>\<^sub>p Polynomial.monom (1::'a) 2
[PROOF STEP]
by (simp add: id)
[PROOF STATE]
proof (state)
this:
[:- (a ^ 2 ^ Suc m), 0::'a, 1::'a:] = [:- (a ^ 2 ^ Suc m), 1::'a:] \<circ>\<^sub>p Polynomial.monom (1::'a) 2

goal (2 subgoals):
 1. (\<Prod>a\<leftarrow>[]. [:- (a ^ 2 ^ m), 1::'a:]) * (\<Prod>a\<leftarrow>[]. [:a ^ 2 ^ m, 1::'a:]) = (\<Prod>a\<leftarrow>[]. [:- (a ^ 2 ^ Suc m), 1::'a:]) \<circ>\<^sub>p Polynomial.monom (1::'a) 2
 2. \<And>a as. (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:]) * (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:]) = (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ Suc m), 1::'a:]) \<circ>\<^sub>p Polynomial.monom (1::'a) 2 \<Longrightarrow> (\<Prod>a\<leftarrow>a # as. [:- (a ^ 2 ^ m), 1::'a:]) * (\<Prod>a\<leftarrow>a # as. [:a ^ 2 ^ m, 1::'a:]) = (\<Prod>a\<leftarrow>a # as. [:- (a ^ 2 ^ Suc m), 1::'a:]) \<circ>\<^sub>p Polynomial.monom (1::'a) 2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
[:- (a ^ 2 ^ Suc m), 0::'a, 1::'a:] = [:- (a ^ 2 ^ Suc m), 1::'a:] \<circ>\<^sub>p Polynomial.monom (1::'a) 2

goal (2 subgoals):
 1. (\<Prod>a\<leftarrow>[]. [:- (a ^ 2 ^ m), 1::'a:]) * (\<Prod>a\<leftarrow>[]. [:a ^ 2 ^ m, 1::'a:]) = (\<Prod>a\<leftarrow>[]. [:- (a ^ 2 ^ Suc m), 1::'a:]) \<circ>\<^sub>p Polynomial.monom (1::'a) 2
 2. \<And>a as. (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:]) * (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:]) = (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ Suc m), 1::'a:]) \<circ>\<^sub>p Polynomial.monom (1::'a) 2 \<Longrightarrow> (\<Prod>a\<leftarrow>a # as. [:- (a ^ 2 ^ m), 1::'a:]) * (\<Prod>a\<leftarrow>a # as. [:a ^ 2 ^ m, 1::'a:]) = (\<Prod>a\<leftarrow>a # as. [:- (a ^ 2 ^ Suc m), 1::'a:]) \<circ>\<^sub>p Polynomial.monom (1::'a) 2
[PROOF STEP]
have "[: - (a ^ 2 ^ (Suc m)), 1:] \<circ>\<^sub>p monom 1 2 * (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ Suc m), 1:]) \<circ>\<^sub>p monom 1 2 =
      (\<Prod>a\<leftarrow>a # as. [:- (a ^ 2 ^ Suc m), 1:]) \<circ>\<^sub>p monom 1 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [:- (a ^ 2 ^ Suc m), 1::'a:] \<circ>\<^sub>p Polynomial.monom (1::'a) 2 * (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ Suc m), 1::'a:]) \<circ>\<^sub>p Polynomial.monom (1::'a) 2 = (\<Prod>a\<leftarrow>a # as. [:- (a ^ 2 ^ Suc m), 1::'a:]) \<circ>\<^sub>p Polynomial.monom (1::'a) 2
[PROOF STEP]
unfolding pcompose_mult[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([:- (a ^ 2 ^ Suc m), 1::'a:] * (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ Suc m), 1::'a:])) \<circ>\<^sub>p Polynomial.monom (1::'a) 2 = (\<Prod>a\<leftarrow>a # as. [:- (a ^ 2 ^ Suc m), 1::'a:]) \<circ>\<^sub>p Polynomial.monom (1::'a) 2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[:- (a ^ 2 ^ Suc m), 1::'a:] \<circ>\<^sub>p Polynomial.monom (1::'a) 2 * (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ Suc m), 1::'a:]) \<circ>\<^sub>p Polynomial.monom (1::'a) 2 = (\<Prod>a\<leftarrow>a # as. [:- (a ^ 2 ^ Suc m), 1::'a:]) \<circ>\<^sub>p Polynomial.monom (1::'a) 2

goal (2 subgoals):
 1. (\<Prod>a\<leftarrow>[]. [:- (a ^ 2 ^ m), 1::'a:]) * (\<Prod>a\<leftarrow>[]. [:a ^ 2 ^ m, 1::'a:]) = (\<Prod>a\<leftarrow>[]. [:- (a ^ 2 ^ Suc m), 1::'a:]) \<circ>\<^sub>p Polynomial.monom (1::'a) 2
 2. \<And>a as. (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:]) * (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:]) = (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ Suc m), 1::'a:]) \<circ>\<^sub>p Polynomial.monom (1::'a) 2 \<Longrightarrow> (\<Prod>a\<leftarrow>a # as. [:- (a ^ 2 ^ m), 1::'a:]) * (\<Prod>a\<leftarrow>a # as. [:a ^ 2 ^ m, 1::'a:]) = (\<Prod>a\<leftarrow>a # as. [:- (a ^ 2 ^ Suc m), 1::'a:]) \<circ>\<^sub>p Polynomial.monom (1::'a) 2
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Prod>a\<leftarrow>a # as. [:- (a ^ 2 ^ m), 1::'a:]) * (\<Prod>a\<leftarrow>a # as. [:a ^ 2 ^ m, 1::'a:]) = (\<Prod>a\<leftarrow>a # as. [:- (a ^ 2 ^ Suc m), 1::'a:]) \<circ>\<^sub>p Polynomial.monom (1::'a) 2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(\<Prod>a\<leftarrow>a # as. [:- (a ^ 2 ^ m), 1::'a:]) * (\<Prod>a\<leftarrow>a # as. [:a ^ 2 ^ m, 1::'a:]) = (\<Prod>a\<leftarrow>a # as. [:- (a ^ 2 ^ Suc m), 1::'a:]) \<circ>\<^sub>p Polynomial.monom (1::'a) 2

goal (1 subgoal):
 1. (\<Prod>a\<leftarrow>a # as. [:- (a ^ 2 ^ m), 1::'a:]) * (\<Prod>a\<leftarrow>a # as. [:a ^ 2 ^ m, 1::'a:]) = (\<Prod>a\<leftarrow>a # as. [:- (a ^ 2 ^ Suc m), 1::'a:]) \<circ>\<^sub>p Polynomial.monom (1::'a) 2
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<Prod>a\<leftarrow>a # as. [:- (a ^ 2 ^ m), 1::'a:]) * (\<Prod>a\<leftarrow>a # as. [:a ^ 2 ^ m, 1::'a:]) = (\<Prod>a\<leftarrow>a # as. [:- (a ^ 2 ^ Suc m), 1::'a:]) \<circ>\<^sub>p Polynomial.monom (1::'a) 2

goal (1 subgoal):
 1. (\<Prod>a\<leftarrow>[]. [:- (a ^ 2 ^ m), 1::'a:]) * (\<Prod>a\<leftarrow>[]. [:a ^ 2 ^ m, 1::'a:]) = (\<Prod>a\<leftarrow>[]. [:- (a ^ 2 ^ Suc m), 1::'a:]) \<circ>\<^sub>p Polynomial.monom (1::'a) 2
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
(\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:]) * (\<Prod>a\<leftarrow>as. [:a ^ 2 ^ m, 1::'a:]) = (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ Suc m), 1::'a:]) \<circ>\<^sub>p Polynomial.monom (1::'a) 2

goal (1 subgoal):
 1. graeffe_poly c as (Suc m) = Polynomial.smult ((- (1::'a)) ^ degree f) (poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
f * f \<circ>\<^sub>p [:0::'a, - (1::'a):] = Polynomial.smult ((- (1::'a)) ^ length as * c ^ 2 ^ Suc m) ((\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ Suc m), 1::'a:]) \<circ>\<^sub>p Polynomial.monom (1::'a) 2)
[PROOF STEP]
have "f * f \<circ>\<^sub>p [:0, - 1:] = (smult ((- 1) ^ length as) (graeffe_poly c as (Suc m)) \<circ>\<^sub>p monom 1 2)"
[PROOF STATE]
proof (prove)
using this:
f * f \<circ>\<^sub>p [:0::'a, - (1::'a):] = Polynomial.smult ((- (1::'a)) ^ length as * c ^ 2 ^ Suc m) ((\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ Suc m), 1::'a:]) \<circ>\<^sub>p Polynomial.monom (1::'a) 2)

goal (1 subgoal):
 1. f * f \<circ>\<^sub>p [:0::'a, - (1::'a):] = Polynomial.smult ((- (1::'a)) ^ length as) (graeffe_poly c as (Suc m)) \<circ>\<^sub>p Polynomial.monom (1::'a) 2
[PROOF STEP]
unfolding graeffe_poly_def pcompose_smult
[PROOF STATE]
proof (prove)
using this:
f * f \<circ>\<^sub>p [:0::'a, - (1::'a):] = Polynomial.smult ((- (1::'a)) ^ length as * c ^ 2 ^ Suc m) ((\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ Suc m), 1::'a:]) \<circ>\<^sub>p Polynomial.monom (1::'a) 2)

goal (1 subgoal):
 1. f * f \<circ>\<^sub>p [:0::'a, - (1::'a):] = Polynomial.smult ((- (1::'a)) ^ length as) (Polynomial.smult (c ^ 2 ^ Suc m) ((\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ Suc m), 1::'a:]) \<circ>\<^sub>p Polynomial.monom (1::'a) 2))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f * f \<circ>\<^sub>p [:0::'a, - (1::'a):] = Polynomial.smult ((- (1::'a)) ^ length as) (graeffe_poly c as (Suc m)) \<circ>\<^sub>p Polynomial.monom (1::'a) 2

goal (1 subgoal):
 1. graeffe_poly c as (Suc m) = Polynomial.smult ((- (1::'a)) ^ degree f) (poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]))
[PROOF STEP]
from arg_cong[OF this, of "\<lambda> f. smult ((- 1) ^ length as) (poly_square_subst f)", unfolded poly_square_subst]
[PROOF STATE]
proof (chain)
picking this:
Polynomial.smult ((- (1::'a)) ^ length as) (poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):])) = Polynomial.smult ((- (1::'a)) ^ length as) (Polynomial.smult ((- (1::'a)) ^ length as) (graeffe_poly c as (Suc m)))
[PROOF STEP]
have "graeffe_poly c as (Suc m) = smult ((- 1) ^ length as) (poly_square_subst (f * f \<circ>\<^sub>p [:0, - 1:]))"
[PROOF STATE]
proof (prove)
using this:
Polynomial.smult ((- (1::'a)) ^ length as) (poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):])) = Polynomial.smult ((- (1::'a)) ^ length as) (Polynomial.smult ((- (1::'a)) ^ length as) (graeffe_poly c as (Suc m)))

goal (1 subgoal):
 1. graeffe_poly c as (Suc m) = Polynomial.smult ((- (1::'a)) ^ length as) (poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
graeffe_poly c as (Suc m) = Polynomial.smult ((- (1::'a)) ^ length as) (poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]))

goal (1 subgoal):
 1. graeffe_poly c as (Suc m) = Polynomial.smult ((- (1::'a)) ^ degree f) (poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
graeffe_poly c as (Suc m) = Polynomial.smult ((- (1::'a)) ^ length as) (poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]))

goal (1 subgoal):
 1. graeffe_poly c as (Suc m) = Polynomial.smult ((- (1::'a)) ^ degree f) (poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]))
[PROOF STEP]
have "\<dots> = smult ((- 1) ^ degree f) (poly_square_subst (f * f \<circ>\<^sub>p [:0, - 1:]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Polynomial.smult ((- (1::'a)) ^ length as) (poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):])) = Polynomial.smult ((- (1::'a)) ^ degree f) (poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]))
[PROOF STEP]
proof (cases "f = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. f = 0 \<Longrightarrow> Polynomial.smult ((- (1::'a)) ^ length as) (poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):])) = Polynomial.smult ((- (1::'a)) ^ degree f) (poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]))
 2. f \<noteq> 0 \<Longrightarrow> Polynomial.smult ((- (1::'a)) ^ length as) (poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):])) = Polynomial.smult ((- (1::'a)) ^ degree f) (poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
f = 0

goal (2 subgoals):
 1. f = 0 \<Longrightarrow> Polynomial.smult ((- (1::'a)) ^ length as) (poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):])) = Polynomial.smult ((- (1::'a)) ^ degree f) (poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]))
 2. f \<noteq> 0 \<Longrightarrow> Polynomial.smult ((- (1::'a)) ^ length as) (poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):])) = Polynomial.smult ((- (1::'a)) ^ degree f) (poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
f = 0

goal (1 subgoal):
 1. Polynomial.smult ((- (1::'a)) ^ length as) (poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):])) = Polynomial.smult ((- (1::'a)) ^ degree f) (poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]))
[PROOF STEP]
by (auto simp: poly_square_subst_def)
[PROOF STATE]
proof (state)
this:
Polynomial.smult ((- (1::'a)) ^ length as) (poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):])) = Polynomial.smult ((- (1::'a)) ^ degree f) (poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]))

goal (1 subgoal):
 1. f \<noteq> 0 \<Longrightarrow> Polynomial.smult ((- (1::'a)) ^ length as) (poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):])) = Polynomial.smult ((- (1::'a)) ^ degree f) (poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f \<noteq> 0 \<Longrightarrow> Polynomial.smult ((- (1::'a)) ^ length as) (poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):])) = Polynomial.smult ((- (1::'a)) ^ degree f) (poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
f \<noteq> 0

goal (1 subgoal):
 1. f \<noteq> 0 \<Longrightarrow> Polynomial.smult ((- (1::'a)) ^ length as) (poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):])) = Polynomial.smult ((- (1::'a)) ^ degree f) (poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]))
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
graeffe_poly c as m = f
f \<noteq> 0
[PROOF STEP]
have c0: "c \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
graeffe_poly c as m = f
f \<noteq> 0

goal (1 subgoal):
 1. c \<noteq> (0::'a)
[PROOF STEP]
unfolding graeffe_poly_def
[PROOF STATE]
proof (prove)
using this:
Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:]) = f
f \<noteq> 0

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

goal (1 subgoal):
 1. f \<noteq> 0 \<Longrightarrow> Polynomial.smult ((- (1::'a)) ^ length as) (poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):])) = Polynomial.smult ((- (1::'a)) ^ degree f) (poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]))
[PROOF STEP]
from arg_cong[OF assms, of degree]
[PROOF STATE]
proof (chain)
picking this:
degree (graeffe_poly c as m) = degree f
[PROOF STEP]
have "degree f = degree (smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1:]))"
[PROOF STATE]
proof (prove)
using this:
degree (graeffe_poly c as m) = degree f

goal (1 subgoal):
 1. degree f = degree (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:]))
[PROOF STEP]
unfolding graeffe_poly_def
[PROOF STATE]
proof (prove)
using this:
degree (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:])) = degree f

goal (1 subgoal):
 1. degree f = degree (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:]))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
degree f = degree (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:]))

goal (1 subgoal):
 1. f \<noteq> 0 \<Longrightarrow> Polynomial.smult ((- (1::'a)) ^ length as) (poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):])) = Polynomial.smult ((- (1::'a)) ^ degree f) (poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
degree f = degree (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:]))

goal (1 subgoal):
 1. f \<noteq> 0 \<Longrightarrow> Polynomial.smult ((- (1::'a)) ^ length as) (poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):])) = Polynomial.smult ((- (1::'a)) ^ degree f) (poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]))
[PROOF STEP]
have "\<dots> = degree (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1:])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:])) = degree (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:])
[PROOF STEP]
unfolding degree_smult_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if c ^ 2 ^ m = (0::'a) then 0 else degree (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:])) = degree (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:])
[PROOF STEP]
using c0
[PROOF STATE]
proof (prove)
using this:
c \<noteq> (0::'a)

goal (1 subgoal):
 1. (if c ^ 2 ^ m = (0::'a) then 0 else degree (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:])) = degree (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
degree (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:])) = degree (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:])

goal (1 subgoal):
 1. f \<noteq> 0 \<Longrightarrow> Polynomial.smult ((- (1::'a)) ^ length as) (poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):])) = Polynomial.smult ((- (1::'a)) ^ degree f) (poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
degree (Polynomial.smult (c ^ 2 ^ m) (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:])) = degree (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:])

goal (1 subgoal):
 1. f \<noteq> 0 \<Longrightarrow> Polynomial.smult ((- (1::'a)) ^ length as) (poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):])) = Polynomial.smult ((- (1::'a)) ^ degree f) (poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]))
[PROOF STEP]
have "\<dots> = length as"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:]) = length as
[PROOF STEP]
unfolding degree_linear_factors
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length as = length as
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
degree (\<Prod>a\<leftarrow>as. [:- (a ^ 2 ^ m), 1::'a:]) = length as

goal (1 subgoal):
 1. f \<noteq> 0 \<Longrightarrow> Polynomial.smult ((- (1::'a)) ^ length as) (poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):])) = Polynomial.smult ((- (1::'a)) ^ degree f) (poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
degree f = length as
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
degree f = length as

goal (1 subgoal):
 1. Polynomial.smult ((- (1::'a)) ^ length as) (poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):])) = Polynomial.smult ((- (1::'a)) ^ degree f) (poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Polynomial.smult ((- (1::'a)) ^ length as) (poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):])) = Polynomial.smult ((- (1::'a)) ^ degree f) (poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Polynomial.smult ((- (1::'a)) ^ length as) (poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):])) = Polynomial.smult ((- (1::'a)) ^ degree f) (poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]))

goal (1 subgoal):
 1. graeffe_poly c as (Suc m) = Polynomial.smult ((- (1::'a)) ^ degree f) (poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
graeffe_poly c as (Suc m) = Polynomial.smult ((- (1::'a)) ^ degree f) (poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
graeffe_poly c as (Suc m) = Polynomial.smult ((- (1::'a)) ^ degree f) (poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]))

goal (1 subgoal):
 1. graeffe_poly c as (Suc m) = Polynomial.smult ((- (1::'a)) ^ degree f) (poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
graeffe_poly c as (Suc m) = Polynomial.smult ((- (1::'a)) ^ degree f) (poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma graeffe_one_step_code[code]: fixes c :: "'a :: idom"
  shows "graeffe_one_step c f = (case poly_even_odd f of (g,h)
  \<Rightarrow> smult c (g * g - monom 1 1 * h * h))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. graeffe_one_step c f = (case poly_even_odd f of (g, h) \<Rightarrow> Polynomial.smult c (g * g - Polynomial.monom (1::'a) 1 * h * h))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. graeffe_one_step c f = (case poly_even_odd f of (g, h) \<Rightarrow> Polynomial.smult c (g * g - Polynomial.monom (1::'a) 1 * h * h))
[PROOF STEP]
obtain g h where eo: "poly_even_odd f = (g,h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>g h. poly_even_odd f = (g, h) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
poly_even_odd f = (g, h)

goal (1 subgoal):
 1. graeffe_one_step c f = (case poly_even_odd f of (g, h) \<Rightarrow> Polynomial.smult c (g * g - Polynomial.monom (1::'a) 1 * h * h))
[PROOF STEP]
from poly_even_odd[OF eo]
[PROOF STATE]
proof (chain)
picking 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
[PROOF STEP]
have fgh: "f = g \<circ>\<^sub>p monom 1 2 + monom 1 1 * h \<circ>\<^sub>p monom 1 2 "
[PROOF STATE]
proof (prove)
using 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 (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]
by auto
[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 (1 subgoal):
 1. graeffe_one_step c f = (case poly_even_odd f of (g, h) \<Rightarrow> Polynomial.smult c (g * g - Polynomial.monom (1::'a) 1 * h * h))
[PROOF STEP]
have m2: "monom (1 :: 'a) 2 = [:0,0,1:]" "monom (1 :: 'a) 1 = [:0,1:]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Polynomial.monom (1::'a) 2 = [:0::'a, 0::'a, 1::'a:] &&& Polynomial.monom (1::'a) 1 = [:0::'a, 1::'a:]
[PROOF STEP]
unfolding coeffs_eq_iff coeffs_monom
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if (1::'a) = (0::'a) then [] else replicate 2 (0::'a) @ [1::'a]) = coeffs [:0::'a, 0::'a, 1::'a:] &&& (if (1::'a) = (0::'a) then [] else replicate 1 (0::'a) @ [1::'a]) = coeffs [:0::'a, 1::'a:]
[PROOF STEP]
by (auto simp add: numeral_2_eq_2)
[PROOF STATE]
proof (state)
this:
Polynomial.monom (1::'a) 2 = [:0::'a, 0::'a, 1::'a:]
Polynomial.monom (1::'a) 1 = [:0::'a, 1::'a:]

goal (1 subgoal):
 1. graeffe_one_step c f = (case poly_even_odd f of (g, h) \<Rightarrow> Polynomial.smult c (g * g - Polynomial.monom (1::'a) 1 * h * h))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. graeffe_one_step c f = (case poly_even_odd f of (g, h) \<Rightarrow> Polynomial.smult c (g * g - Polynomial.monom (1::'a) 1 * h * h))
[PROOF STEP]
unfolding eo split graeffe_one_step_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Polynomial.smult c (poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):])) = Polynomial.smult c (g * g - Polynomial.monom (1::'a) 1 * h * h)
[PROOF STEP]
proof (rule arg_cong[of _ _ "smult c"])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]) = g * g - Polynomial.monom (1::'a) 1 * h * h
[PROOF STEP]
let ?g = "g \<circ>\<^sub>p monom 1 2"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]) = g * g - Polynomial.monom (1::'a) 1 * h * h
[PROOF STEP]
let ?h = "h \<circ>\<^sub>p monom 1 2"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]) = g * g - Polynomial.monom (1::'a) 1 * h * h
[PROOF STEP]
let ?x = "monom (1 :: 'a) 1"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]) = g * g - Polynomial.monom (1::'a) 1 * h * h
[PROOF STEP]
have 2: "2 = Suc (Suc 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 = Suc (Suc 0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
2 = Suc (Suc 0)

goal (1 subgoal):
 1. poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]) = g * g - Polynomial.monom (1::'a) 1 * h * h
[PROOF STEP]
have "f * f \<circ>\<^sub>p [:0, - 1:] = (g \<circ>\<^sub>p monom 1 2 + monom 1 1 * h \<circ>\<^sub>p monom 1 2) *
      (g \<circ>\<^sub>p monom 1 2 + monom 1 1 * h \<circ>\<^sub>p monom 1 2) \<circ>\<^sub>p [:0, - 1:]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f * f \<circ>\<^sub>p [:0::'a, - (1::'a):] = (g \<circ>\<^sub>p Polynomial.monom (1::'a) 2 + Polynomial.monom (1::'a) 1 * h \<circ>\<^sub>p Polynomial.monom (1::'a) 2) * (g \<circ>\<^sub>p Polynomial.monom (1::'a) 2 + Polynomial.monom (1::'a) 1 * h \<circ>\<^sub>p Polynomial.monom (1::'a) 2) \<circ>\<^sub>p [:0::'a, - (1::'a):]
[PROOF STEP]
unfolding fgh
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (g \<circ>\<^sub>p Polynomial.monom (1::'a) 2 + Polynomial.monom (1::'a) 1 * h \<circ>\<^sub>p Polynomial.monom (1::'a) 2) * (g \<circ>\<^sub>p Polynomial.monom (1::'a) 2 + Polynomial.monom (1::'a) 1 * h \<circ>\<^sub>p Polynomial.monom (1::'a) 2) \<circ>\<^sub>p [:0::'a, - (1::'a):] = (g \<circ>\<^sub>p Polynomial.monom (1::'a) 2 + Polynomial.monom (1::'a) 1 * h \<circ>\<^sub>p Polynomial.monom (1::'a) 2) * (g \<circ>\<^sub>p Polynomial.monom (1::'a) 2 + Polynomial.monom (1::'a) 1 * h \<circ>\<^sub>p Polynomial.monom (1::'a) 2) \<circ>\<^sub>p [:0::'a, - (1::'a):]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f * f \<circ>\<^sub>p [:0::'a, - (1::'a):] = (g \<circ>\<^sub>p Polynomial.monom (1::'a) 2 + Polynomial.monom (1::'a) 1 * h \<circ>\<^sub>p Polynomial.monom (1::'a) 2) * (g \<circ>\<^sub>p Polynomial.monom (1::'a) 2 + Polynomial.monom (1::'a) 1 * h \<circ>\<^sub>p Polynomial.monom (1::'a) 2) \<circ>\<^sub>p [:0::'a, - (1::'a):]

goal (1 subgoal):
 1. poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]) = g * g - Polynomial.monom (1::'a) 1 * h * h
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f * f \<circ>\<^sub>p [:0::'a, - (1::'a):] = (g \<circ>\<^sub>p Polynomial.monom (1::'a) 2 + Polynomial.monom (1::'a) 1 * h \<circ>\<^sub>p Polynomial.monom (1::'a) 2) * (g \<circ>\<^sub>p Polynomial.monom (1::'a) 2 + Polynomial.monom (1::'a) 1 * h \<circ>\<^sub>p Polynomial.monom (1::'a) 2) \<circ>\<^sub>p [:0::'a, - (1::'a):]

goal (1 subgoal):
 1. poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]) = g * g - Polynomial.monom (1::'a) 1 * h * h
[PROOF STEP]
have "(g \<circ>\<^sub>p monom 1 2 + monom 1 1 * h \<circ>\<^sub>p monom 1 2) \<circ>\<^sub>p [:0, - 1:]
      = g \<circ>\<^sub>p (monom 1 2 \<circ>\<^sub>p [:0, - 1:]) + monom 1 1 \<circ>\<^sub>p [:0, - 1:] * h \<circ>\<^sub>p (monom 1 2 \<circ>\<^sub>p [:0, - 1:])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (g \<circ>\<^sub>p Polynomial.monom (1::'a) 2 + Polynomial.monom (1::'a) 1 * h \<circ>\<^sub>p Polynomial.monom (1::'a) 2) \<circ>\<^sub>p [:0::'a, - (1::'a):] = g \<circ>\<^sub>p (Polynomial.monom (1::'a) 2 \<circ>\<^sub>p [:0::'a, - (1::'a):]) + Polynomial.monom (1::'a) 1 \<circ>\<^sub>p [:0::'a, - (1::'a):] * h \<circ>\<^sub>p (Polynomial.monom (1::'a) 2 \<circ>\<^sub>p [:0::'a, - (1::'a):])
[PROOF STEP]
unfolding pcompose_add pcompose_mult pcompose_assoc
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g \<circ>\<^sub>p Polynomial.monom (1::'a) 2 \<circ>\<^sub>p [:0::'a, - (1::'a):] + Polynomial.monom (1::'a) 1 \<circ>\<^sub>p [:0::'a, - (1::'a):] * h \<circ>\<^sub>p Polynomial.monom (1::'a) 2 \<circ>\<^sub>p [:0::'a, - (1::'a):] = g \<circ>\<^sub>p Polynomial.monom (1::'a) 2 \<circ>\<^sub>p [:0::'a, - (1::'a):] + Polynomial.monom (1::'a) 1 \<circ>\<^sub>p [:0::'a, - (1::'a):] * h \<circ>\<^sub>p Polynomial.monom (1::'a) 2 \<circ>\<^sub>p [:0::'a, - (1::'a):]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(g \<circ>\<^sub>p Polynomial.monom (1::'a) 2 + Polynomial.monom (1::'a) 1 * h \<circ>\<^sub>p Polynomial.monom (1::'a) 2) \<circ>\<^sub>p [:0::'a, - (1::'a):] = g \<circ>\<^sub>p (Polynomial.monom (1::'a) 2 \<circ>\<^sub>p [:0::'a, - (1::'a):]) + Polynomial.monom (1::'a) 1 \<circ>\<^sub>p [:0::'a, - (1::'a):] * h \<circ>\<^sub>p (Polynomial.monom (1::'a) 2 \<circ>\<^sub>p [:0::'a, - (1::'a):])

goal (1 subgoal):
 1. poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]) = g * g - Polynomial.monom (1::'a) 1 * h * h
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(g \<circ>\<^sub>p Polynomial.monom (1::'a) 2 + Polynomial.monom (1::'a) 1 * h \<circ>\<^sub>p Polynomial.monom (1::'a) 2) \<circ>\<^sub>p [:0::'a, - (1::'a):] = g \<circ>\<^sub>p (Polynomial.monom (1::'a) 2 \<circ>\<^sub>p [:0::'a, - (1::'a):]) + Polynomial.monom (1::'a) 1 \<circ>\<^sub>p [:0::'a, - (1::'a):] * h \<circ>\<^sub>p (Polynomial.monom (1::'a) 2 \<circ>\<^sub>p [:0::'a, - (1::'a):])

goal (1 subgoal):
 1. poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]) = g * g - Polynomial.monom (1::'a) 1 * h * h
[PROOF STEP]
have "monom (1 :: 'a) 2 \<circ>\<^sub>p [:0, - 1:] = monom 1 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Polynomial.monom (1::'a) 2 \<circ>\<^sub>p [:0::'a, - (1::'a):] = Polynomial.monom (1::'a) 2
[PROOF STEP]
unfolding m2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [:0::'a, 0::'a, 1::'a:] \<circ>\<^sub>p [:0::'a, - (1::'a):] = [:0::'a, 0::'a, 1::'a:]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Polynomial.monom (1::'a) 2 \<circ>\<^sub>p [:0::'a, - (1::'a):] = Polynomial.monom (1::'a) 2

goal (1 subgoal):
 1. poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]) = g * g - Polynomial.monom (1::'a) 1 * h * h
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Polynomial.monom (1::'a) 2 \<circ>\<^sub>p [:0::'a, - (1::'a):] = Polynomial.monom (1::'a) 2

goal (1 subgoal):
 1. poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]) = g * g - Polynomial.monom (1::'a) 1 * h * h
[PROOF STEP]
have "?x \<circ>\<^sub>p [:0, - 1:] = [:0, -1:]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Polynomial.monom (1::'a) 1 \<circ>\<^sub>p [:0::'a, - (1::'a):] = [:0::'a, - (1::'a):]
[PROOF STEP]
unfolding m2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [:0::'a, 1::'a:] \<circ>\<^sub>p [:0::'a, - (1::'a):] = [:0::'a, - (1::'a):]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Polynomial.monom (1::'a) 1 \<circ>\<^sub>p [:0::'a, - (1::'a):] = [:0::'a, - (1::'a):]

goal (1 subgoal):
 1. poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]) = g * g - Polynomial.monom (1::'a) 1 * h * h
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Polynomial.monom (1::'a) 1 \<circ>\<^sub>p [:0::'a, - (1::'a):] = [:0::'a, - (1::'a):]

goal (1 subgoal):
 1. poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]) = g * g - Polynomial.monom (1::'a) 1 * h * h
[PROOF STEP]
have "[:0, - 1:] * h \<circ>\<^sub>p monom 1 2 = (-?x) * ?h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [:0::'a, - (1::'a):] * h \<circ>\<^sub>p Polynomial.monom (1::'a) 2 = - Polynomial.monom (1::'a) 1 * h \<circ>\<^sub>p Polynomial.monom (1::'a) 2
[PROOF STEP]
unfolding m2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [:0::'a, - (1::'a):] * h \<circ>\<^sub>p [:0::'a, 0::'a, 1::'a:] = - [:0::'a, 1::'a:] * h \<circ>\<^sub>p [:0::'a, 0::'a, 1::'a:]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[:0::'a, - (1::'a):] * h \<circ>\<^sub>p Polynomial.monom (1::'a) 2 = - Polynomial.monom (1::'a) 1 * h \<circ>\<^sub>p Polynomial.monom (1::'a) 2

goal (1 subgoal):
 1. poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]) = g * g - Polynomial.monom (1::'a) 1 * h * h
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
[:0::'a, - (1::'a):] * h \<circ>\<^sub>p Polynomial.monom (1::'a) 2 = - Polynomial.monom (1::'a) 1 * h \<circ>\<^sub>p Polynomial.monom (1::'a) 2

goal (1 subgoal):
 1. poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]) = g * g - Polynomial.monom (1::'a) 1 * h * h
[PROOF STEP]
have "(?g + ?x * ?h) * (?g + (- ?x) * ?h) = (?g * ?g - (?x * ?x) * ?h * ?h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (g \<circ>\<^sub>p Polynomial.monom (1::'a) 2 + Polynomial.monom (1::'a) 1 * h \<circ>\<^sub>p Polynomial.monom (1::'a) 2) * (g \<circ>\<^sub>p Polynomial.monom (1::'a) 2 + - Polynomial.monom (1::'a) 1 * h \<circ>\<^sub>p Polynomial.monom (1::'a) 2) = g \<circ>\<^sub>p Polynomial.monom (1::'a) 2 * g \<circ>\<^sub>p Polynomial.monom (1::'a) 2 - Polynomial.monom (1::'a) 1 * Polynomial.monom (1::'a) 1 * h \<circ>\<^sub>p Polynomial.monom (1::'a) 2 * h \<circ>\<^sub>p Polynomial.monom (1::'a) 2
[PROOF STEP]
by (auto simp: field_simps)
[PROOF STATE]
proof (state)
this:
(g \<circ>\<^sub>p Polynomial.monom (1::'a) 2 + Polynomial.monom (1::'a) 1 * h \<circ>\<^sub>p Polynomial.monom (1::'a) 2) * (g \<circ>\<^sub>p Polynomial.monom (1::'a) 2 + - Polynomial.monom (1::'a) 1 * h \<circ>\<^sub>p Polynomial.monom (1::'a) 2) = g \<circ>\<^sub>p Polynomial.monom (1::'a) 2 * g \<circ>\<^sub>p Polynomial.monom (1::'a) 2 - Polynomial.monom (1::'a) 1 * Polynomial.monom (1::'a) 1 * h \<circ>\<^sub>p Polynomial.monom (1::'a) 2 * h \<circ>\<^sub>p Polynomial.monom (1::'a) 2

goal (1 subgoal):
 1. poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]) = g * g - Polynomial.monom (1::'a) 1 * h * h
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(g \<circ>\<^sub>p Polynomial.monom (1::'a) 2 + Polynomial.monom (1::'a) 1 * h \<circ>\<^sub>p Polynomial.monom (1::'a) 2) * (g \<circ>\<^sub>p Polynomial.monom (1::'a) 2 + - Polynomial.monom (1::'a) 1 * h \<circ>\<^sub>p Polynomial.monom (1::'a) 2) = g \<circ>\<^sub>p Polynomial.monom (1::'a) 2 * g \<circ>\<^sub>p Polynomial.monom (1::'a) 2 - Polynomial.monom (1::'a) 1 * Polynomial.monom (1::'a) 1 * h \<circ>\<^sub>p Polynomial.monom (1::'a) 2 * h \<circ>\<^sub>p Polynomial.monom (1::'a) 2

goal (1 subgoal):
 1. poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]) = g * g - Polynomial.monom (1::'a) 1 * h * h
[PROOF STEP]
have "?x * ?x = ?x \<circ>\<^sub>p monom 1 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Polynomial.monom (1::'a) 1 * Polynomial.monom (1::'a) 1 = Polynomial.monom (1::'a) 1 \<circ>\<^sub>p Polynomial.monom (1::'a) 2
[PROOF STEP]
unfolding mult_monom
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Polynomial.monom ((1::'a) * (1::'a)) (1 + 1) = Polynomial.monom (1::'a) 1 \<circ>\<^sub>p Polynomial.monom (1::'a) 2
[PROOF STEP]
by (insert m2, simp add: 2)
[PROOF STATE]
proof (state)
this:
Polynomial.monom (1::'a) 1 * Polynomial.monom (1::'a) 1 = Polynomial.monom (1::'a) 1 \<circ>\<^sub>p Polynomial.monom (1::'a) 2

goal (1 subgoal):
 1. poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]) = g * g - Polynomial.monom (1::'a) 1 * h * h
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Polynomial.monom (1::'a) 1 * Polynomial.monom (1::'a) 1 = Polynomial.monom (1::'a) 1 \<circ>\<^sub>p Polynomial.monom (1::'a) 2

goal (1 subgoal):
 1. poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]) = g * g - Polynomial.monom (1::'a) 1 * h * h
[PROOF STEP]
have "(?g * ?g - \<dots> * ?h * ?h) = (g * g - ?x * h * h) \<circ>\<^sub>p monom 1 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g \<circ>\<^sub>p Polynomial.monom (1::'a) 2 * g \<circ>\<^sub>p Polynomial.monom (1::'a) 2 - Polynomial.monom (1::'a) 1 \<circ>\<^sub>p Polynomial.monom (1::'a) 2 * h \<circ>\<^sub>p Polynomial.monom (1::'a) 2 * h \<circ>\<^sub>p Polynomial.monom (1::'a) 2 = (g * g - Polynomial.monom (1::'a) 1 * h * h) \<circ>\<^sub>p Polynomial.monom (1::'a) 2
[PROOF STEP]
unfolding pcompose_diff pcompose_mult
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g \<circ>\<^sub>p Polynomial.monom (1::'a) 2 * g \<circ>\<^sub>p Polynomial.monom (1::'a) 2 - Polynomial.monom (1::'a) 1 \<circ>\<^sub>p Polynomial.monom (1::'a) 2 * h \<circ>\<^sub>p Polynomial.monom (1::'a) 2 * h \<circ>\<^sub>p Polynomial.monom (1::'a) 2 = g \<circ>\<^sub>p Polynomial.monom (1::'a) 2 * g \<circ>\<^sub>p Polynomial.monom (1::'a) 2 - Polynomial.monom (1::'a) 1 \<circ>\<^sub>p Polynomial.monom (1::'a) 2 * h \<circ>\<^sub>p Polynomial.monom (1::'a) 2 * h \<circ>\<^sub>p Polynomial.monom (1::'a) 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
g \<circ>\<^sub>p Polynomial.monom (1::'a) 2 * g \<circ>\<^sub>p Polynomial.monom (1::'a) 2 - Polynomial.monom (1::'a) 1 \<circ>\<^sub>p Polynomial.monom (1::'a) 2 * h \<circ>\<^sub>p Polynomial.monom (1::'a) 2 * h \<circ>\<^sub>p Polynomial.monom (1::'a) 2 = (g * g - Polynomial.monom (1::'a) 1 * h * h) \<circ>\<^sub>p Polynomial.monom (1::'a) 2

goal (1 subgoal):
 1. poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]) = g * g - Polynomial.monom (1::'a) 1 * h * h
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
f * f \<circ>\<^sub>p [:0::'a, - (1::'a):] = (g * g - Polynomial.monom (1::'a) 1 * h * h) \<circ>\<^sub>p Polynomial.monom (1::'a) 2
[PROOF STEP]
have "poly_square_subst (f * f \<circ>\<^sub>p [:0, - 1:])
      = poly_square_subst ((g * g - ?x * h * h) \<circ>\<^sub>p monom 1 2)"
[PROOF STATE]
proof (prove)
using this:
f * f \<circ>\<^sub>p [:0::'a, - (1::'a):] = (g * g - Polynomial.monom (1::'a) 1 * h * h) \<circ>\<^sub>p Polynomial.monom (1::'a) 2

goal (1 subgoal):
 1. poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]) = poly_square_subst ((g * g - Polynomial.monom (1::'a) 1 * h * h) \<circ>\<^sub>p Polynomial.monom (1::'a) 2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]) = poly_square_subst ((g * g - Polynomial.monom (1::'a) 1 * h * h) \<circ>\<^sub>p Polynomial.monom (1::'a) 2)

goal (1 subgoal):
 1. poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]) = g * g - Polynomial.monom (1::'a) 1 * h * h
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]) = poly_square_subst ((g * g - Polynomial.monom (1::'a) 1 * h * h) \<circ>\<^sub>p Polynomial.monom (1::'a) 2)

goal (1 subgoal):
 1. poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]) = g * g - Polynomial.monom (1::'a) 1 * h * h
[PROOF STEP]
have "\<dots> = g * g - ?x * h * h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly_square_subst ((g * g - Polynomial.monom (1::'a) 1 * h * h) \<circ>\<^sub>p Polynomial.monom (1::'a) 2) = g * g - Polynomial.monom (1::'a) 1 * h * h
[PROOF STEP]
unfolding poly_square_subst
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g * g - Polynomial.monom (1::'a) 1 * h * h = g * g - Polynomial.monom (1::'a) 1 * h * h
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
poly_square_subst ((g * g - Polynomial.monom (1::'a) 1 * h * h) \<circ>\<^sub>p Polynomial.monom (1::'a) 2) = g * g - Polynomial.monom (1::'a) 1 * h * h

goal (1 subgoal):
 1. poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]) = g * g - Polynomial.monom (1::'a) 1 * h * h
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]) = g * g - Polynomial.monom (1::'a) 1 * h * h
[PROOF STEP]
show "poly_square_subst (f * f \<circ>\<^sub>p [:0, - 1:]) = g * g - ?x * h * h"
[PROOF STATE]
proof (prove)
using this:
poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]) = g * g - Polynomial.monom (1::'a) 1 * h * h

goal (1 subgoal):
 1. poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]) = g * g - Polynomial.monom (1::'a) 1 * h * h
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
poly_square_subst (f * f \<circ>\<^sub>p [:0::'a, - (1::'a):]) = g * g - Polynomial.monom (1::'a) 1 * h * h

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
graeffe_one_step c f = (case poly_even_odd f of (g, h) \<Rightarrow> Polynomial.smult c (g * g - Polynomial.monom (1::'a) 1 * h * h))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma graeffe_poly_impl_main: assumes "f = smult c (\<Prod>a\<leftarrow>as. [:- a, 1:])"
  shows "graeffe_poly_impl_main ((-1)^degree f) f m = graeffe_poly c as m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. graeffe_poly_impl_main ((- (1::'a)) ^ degree f) f m = graeffe_poly c as m
[PROOF STEP]
proof (induct m)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. graeffe_poly_impl_main ((- (1::'a)) ^ degree f) f 0 = graeffe_poly c as 0
 2. \<And>m. graeffe_poly_impl_main ((- (1::'a)) ^ degree f) f m = graeffe_poly c as m \<Longrightarrow> graeffe_poly_impl_main ((- (1::'a)) ^ degree f) f (Suc m) = graeffe_poly c as (Suc m)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. graeffe_poly_impl_main ((- (1::'a)) ^ degree f) f 0 = graeffe_poly c as 0
 2. \<And>m. graeffe_poly_impl_main ((- (1::'a)) ^ degree f) f m = graeffe_poly c as m \<Longrightarrow> graeffe_poly_impl_main ((- (1::'a)) ^ degree f) f (Suc m) = graeffe_poly c as (Suc m)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. graeffe_poly_impl_main ((- (1::'a)) ^ degree f) f 0 = graeffe_poly c as 0
[PROOF STEP]
using graeffe_0[OF assms]
[PROOF STATE]
proof (prove)
using this:
graeffe_poly c as 0 = f

goal (1 subgoal):
 1. graeffe_poly_impl_main ((- (1::'a)) ^ degree f) f 0 = graeffe_poly c as 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
graeffe_poly_impl_main ((- (1::'a)) ^ degree f) f 0 = graeffe_poly c as 0

goal (1 subgoal):
 1. \<And>m. graeffe_poly_impl_main ((- (1::'a)) ^ degree f) f m = graeffe_poly c as m \<Longrightarrow> graeffe_poly_impl_main ((- (1::'a)) ^ degree f) f (Suc m) = graeffe_poly c as (Suc m)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m. graeffe_poly_impl_main ((- (1::'a)) ^ degree f) f m = graeffe_poly c as m \<Longrightarrow> graeffe_poly_impl_main ((- (1::'a)) ^ degree f) f (Suc m) = graeffe_poly c as (Suc m)
[PROOF STEP]
case (Suc m)
[PROOF STATE]
proof (state)
this:
graeffe_poly_impl_main ((- (1::'a)) ^ degree f) f m = graeffe_poly c as m

goal (1 subgoal):
 1. \<And>m. graeffe_poly_impl_main ((- (1::'a)) ^ degree f) f m = graeffe_poly c as m \<Longrightarrow> graeffe_poly_impl_main ((- (1::'a)) ^ degree f) f (Suc m) = graeffe_poly c as (Suc m)
[PROOF STEP]
have [simp]: "degree (graeffe_poly c as m) = degree f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (graeffe_poly c as m) = degree f
[PROOF STEP]
unfolding graeffe_poly_def degree_smult_eq assms
    degree_linear_factors
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if c ^ 2 ^ m = (0::'a) then 0 else length as) = (if c = (0::'a) then 0 else length as)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
degree (graeffe_poly c as m) = degree f

goal (1 subgoal):
 1. \<And>m. graeffe_poly_impl_main ((- (1::'a)) ^ degree f) f m = graeffe_poly c as m \<Longrightarrow> graeffe_poly_impl_main ((- (1::'a)) ^ degree f) f (Suc m) = graeffe_poly c as (Suc m)
[PROOF STEP]
from arg_cong[OF Suc, of degree]
[PROOF STATE]
proof (chain)
picking this:
degree (graeffe_poly_impl_main ((- (1::'a)) ^ degree f) f m) = degree (graeffe_poly c as m)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
degree (graeffe_poly_impl_main ((- (1::'a)) ^ degree f) f m) = degree (graeffe_poly c as m)

goal (1 subgoal):
 1. graeffe_poly_impl_main ((- (1::'a)) ^ degree f) f (Suc m) = graeffe_poly c as (Suc m)
[PROOF STEP]
unfolding graeffe_recursion[OF Suc[symmetric]]
[PROOF STATE]
proof (prove)
using this:
degree (graeffe_poly_impl_main ((- (1::'a)) ^ degree f) f m) = degree (graeffe_poly c as m)

goal (1 subgoal):
 1. graeffe_poly_impl_main ((- (1::'a)) ^ degree f) f (Suc m) = Polynomial.smult ((- (1::'a)) ^ degree (graeffe_poly_impl_main ((- (1::'a)) ^ degree f) f m)) (poly_square_subst (graeffe_poly_impl_main ((- (1::'a)) ^ degree f) f m * graeffe_poly_impl_main ((- (1::'a)) ^ degree f) f m \<circ>\<^sub>p [:0::'a, - (1::'a):]))
[PROOF STEP]
by (simp add: graeffe_one_step_def)
[PROOF STATE]
proof (state)
this:
graeffe_poly_impl_main ((- (1::'a)) ^ degree f) f (Suc m) = graeffe_poly c as (Suc m)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma graeffe_poly_impl: assumes "f = smult c (\<Prod>a\<leftarrow>as. [:- a, 1:])"
  shows "graeffe_poly_impl f m = graeffe_poly c as m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. graeffe_poly_impl f m = graeffe_poly c as m
[PROOF STEP]
using graeffe_poly_impl_main[OF assms]
[PROOF STATE]
proof (prove)
using this:
graeffe_poly_impl_main ((- (1::'a)) ^ degree f) f ?m = graeffe_poly c as ?m

goal (1 subgoal):
 1. graeffe_poly_impl f m = graeffe_poly c as m
[PROOF STEP]
unfolding graeffe_poly_impl_def
[PROOF STATE]
proof (prove)
using this:
graeffe_poly_impl_main ((- (1::'a)) ^ degree f) f ?m = graeffe_poly c as ?m

goal (1 subgoal):
 1. graeffe_poly_impl_main ((- (1::'a)) ^ degree f) f m = graeffe_poly c as m
[PROOF STEP]
.


[STATEMENT]
lemma drop_half_map: "drop_half (map f xs) = map f (drop_half xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. drop_half (map f xs) = map f (drop_half xs)
[PROOF STEP]
by (induct xs rule: drop_half.induct, auto)


[STATEMENT]
lemma (in inj_comm_ring_hom) map_poly_poly_square_subst:
  "map_poly hom (poly_square_subst f) = poly_square_subst (map_poly hom f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_poly hom (poly_square_subst f) = poly_square_subst (map_poly hom f)
[PROOF STEP]
unfolding poly_square_subst_def coeffs_map_poly_hom drop_half_map poly_of_list_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_poly hom (Poly (drop_half (coeffs f))) = Poly (map hom (drop_half (coeffs f)))
[PROOF STEP]
by (rule poly_eqI, auto simp: nth_default_map_eq)


[STATEMENT]
lemma graeffe_poly_impl_hom:
  "map_poly hom (graeffe_poly_impl f m) = graeffe_poly_impl (map_poly hom f) m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_poly hom (graeffe_poly_impl f m) = graeffe_poly_impl (map_poly hom f) m
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. map_poly hom (graeffe_poly_impl f m) = graeffe_poly_impl (map_poly hom f) m
[PROOF STEP]
interpret mh: map_poly_inj_idom_hom
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_poly_inj_idom_hom hom
[PROOF STEP]
..
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. map_poly hom (graeffe_poly_impl f m) = graeffe_poly_impl (map_poly hom f) m
[PROOF STEP]
obtain c where c: "(((- 1) ^ degree f) :: 'a) = c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>c. (- (1::'a)) ^ degree f = c \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(- (1::'a)) ^ degree f = c

goal (1 subgoal):
 1. map_poly hom (graeffe_poly_impl f m) = graeffe_poly_impl (map_poly hom f) m
[PROOF STEP]
have c': "(((- 1) ^ degree f) :: 'b) = hom c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (- (1::'b)) ^ degree f = hom c
[PROOF STEP]
unfolding c[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (- (1::'b)) ^ degree f = hom ((- (1::'a)) ^ degree f)
[PROOF STEP]
by (simp add:hom_distribs)
[PROOF STATE]
proof (state)
this:
(- (1::'b)) ^ degree f = hom c

goal (1 subgoal):
 1. map_poly hom (graeffe_poly_impl f m) = graeffe_poly_impl (map_poly hom f) m
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_poly hom (graeffe_poly_impl f m) = graeffe_poly_impl (map_poly hom f) m
[PROOF STEP]
unfolding graeffe_poly_impl_def degree_map_poly_hom c c'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_poly hom (graeffe_poly_impl_main c f m) = graeffe_poly_impl_main (hom c) (map_poly hom f) m
[PROOF STEP]
apply (induct m arbitrary: f; simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m f. (\<And>f. map_poly hom (graeffe_poly_impl_main c f m) = graeffe_poly_impl_main (hom c) (map_poly hom f) m) \<Longrightarrow> map_poly hom (graeffe_one_step c (graeffe_poly_impl_main c f m)) = graeffe_one_step (hom c) (graeffe_poly_impl_main (hom c) (map_poly hom f) m)
[PROOF STEP]
by (unfold graeffe_one_step_def hom_distribs map_poly_poly_square_subst map_poly_pcompose,simp)
[PROOF STATE]
proof (state)
this:
map_poly hom (graeffe_poly_impl f m) = graeffe_poly_impl (map_poly hom f) m

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma graeffe_poly_impl_mahler: "mahler_measure (graeffe_poly_impl f m) = mahler_measure f ^ 2 ^ m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mahler_measure (graeffe_poly_impl f m) = mahler_measure f ^ 2 ^ m
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mahler_measure (graeffe_poly_impl f m) = mahler_measure f ^ 2 ^ m
[PROOF STEP]
let ?c = "complex_of_int"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mahler_measure (graeffe_poly_impl f m) = mahler_measure f ^ 2 ^ m
[PROOF STEP]
let ?cc = "map_poly ?c"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mahler_measure (graeffe_poly_impl f m) = mahler_measure f ^ 2 ^ m
[PROOF STEP]
let ?f = "?cc f"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mahler_measure (graeffe_poly_impl f m) = mahler_measure f ^ 2 ^ m
[PROOF STEP]
note eq = complex_roots(1)[of ?f]
[PROOF STATE]
proof (state)
this:
Polynomial.smult (lead_coeff (of_int_poly f)) (\<Prod>a\<leftarrow>complex_roots_complex (of_int_poly f). [:- a, 1:]) = of_int_poly f

goal (1 subgoal):
 1. mahler_measure (graeffe_poly_impl f m) = mahler_measure f ^ 2 ^ m
[PROOF STEP]
interpret inj_idom_hom complex_of_int
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_idom_hom complex_of_int
[PROOF STEP]
by (standard, auto)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mahler_measure (graeffe_poly_impl f m) = mahler_measure f ^ 2 ^ m
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mahler_measure (graeffe_poly_impl f m) = mahler_measure f ^ 2 ^ m
[PROOF STEP]
unfolding mahler_measure_def mahler_graeffe[OF eq[symmetric], symmetric]
     graeffe_poly_impl[OF eq[symmetric], symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mahler_measure_poly (of_int_poly (graeffe_poly_impl f m)) = mahler_measure_poly (graeffe_poly_impl (of_int_poly f) m)
[PROOF STEP]
by (simp add: of_int_hom.graeffe_poly_impl_hom)
[PROOF STATE]
proof (state)
this:
mahler_measure (graeffe_poly_impl f m) = mahler_measure f ^ 2 ^ m

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mahler_landau_graeffe_approximation_core:
  assumes g: "g = graeffe_poly_impl f k"
  shows "mahler_measure f \<le> root (2 ^ Suc k) (real_of_int (\<Sum>a\<leftarrow>coeffs g. a * a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mahler_measure f \<le> root (2 ^ Suc k) (real_of_int (\<Sum>a\<leftarrow>coeffs g. a * a))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mahler_measure f \<le> root (2 ^ Suc k) (real_of_int (\<Sum>a\<leftarrow>coeffs g. a * a))
[PROOF STEP]
have "mahler_measure f = root (2^k) (mahler_measure f ^ (2^k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mahler_measure f = root (2 ^ k) (mahler_measure f ^ 2 ^ k)
[PROOF STEP]
by (simp add: real_root_power_cancel mahler_measure_ge_0)
[PROOF STATE]
proof (state)
this:
mahler_measure f = root (2 ^ k) (mahler_measure f ^ 2 ^ k)

goal (1 subgoal):
 1. mahler_measure f \<le> root (2 ^ Suc k) (real_of_int (\<Sum>a\<leftarrow>coeffs g. a * a))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
mahler_measure f = root (2 ^ k) (mahler_measure f ^ 2 ^ k)

goal (1 subgoal):
 1. mahler_measure f \<le> root (2 ^ Suc k) (real_of_int (\<Sum>a\<leftarrow>coeffs g. a * a))
[PROOF STEP]
have "\<dots> = root (2^k) (mahler_measure g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. root (2 ^ k) (mahler_measure f ^ 2 ^ k) = root (2 ^ k) (mahler_measure g)
[PROOF STEP]
unfolding graeffe_poly_impl_mahler g
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. root (2 ^ k) (mahler_measure f ^ 2 ^ k) = root (2 ^ k) (mahler_measure f ^ 2 ^ k)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
root (2 ^ k) (mahler_measure f ^ 2 ^ k) = root (2 ^ k) (mahler_measure g)

goal (1 subgoal):
 1. mahler_measure f \<le> root (2 ^ Suc k) (real_of_int (\<Sum>a\<leftarrow>coeffs g. a * a))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
root (2 ^ k) (mahler_measure f ^ 2 ^ k) = root (2 ^ k) (mahler_measure g)

goal (1 subgoal):
 1. mahler_measure f \<le> root (2 ^ Suc k) (real_of_int (\<Sum>a\<leftarrow>coeffs g. a * a))
[PROOF STEP]
have "\<dots> = root (2^k) (root 2 (((mahler_measure g)^2)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. root (2 ^ k) (mahler_measure g) = root (2 ^ k) (root 2 ((mahler_measure g)\<^sup>2))
[PROOF STEP]
by (simp add: real_root_power_cancel mahler_measure_ge_0)
[PROOF STATE]
proof (state)
this:
root (2 ^ k) (mahler_measure g) = root (2 ^ k) (root 2 ((mahler_measure g)\<^sup>2))

goal (1 subgoal):
 1. mahler_measure f \<le> root (2 ^ Suc k) (real_of_int (\<Sum>a\<leftarrow>coeffs g. a * a))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
root (2 ^ k) (mahler_measure g) = root (2 ^ k) (root 2 ((mahler_measure g)\<^sup>2))

goal (1 subgoal):
 1. mahler_measure f \<le> root (2 ^ Suc k) (real_of_int (\<Sum>a\<leftarrow>coeffs g. a * a))
[PROOF STEP]
have "\<dots> = root (2^Suc k) (((mahler_measure g)^2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. root (2 ^ k) (root 2 ((mahler_measure g)\<^sup>2)) = root (2 ^ Suc k) ((mahler_measure g)\<^sup>2)
[PROOF STEP]
by (metis power_Suc2 real_root_mult_exp)
[PROOF STATE]
proof (state)
this:
root (2 ^ k) (root 2 ((mahler_measure g)\<^sup>2)) = root (2 ^ Suc k) ((mahler_measure g)\<^sup>2)

goal (1 subgoal):
 1. mahler_measure f \<le> root (2 ^ Suc k) (real_of_int (\<Sum>a\<leftarrow>coeffs g. a * a))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
root (2 ^ k) (root 2 ((mahler_measure g)\<^sup>2)) = root (2 ^ Suc k) ((mahler_measure g)\<^sup>2)

goal (1 subgoal):
 1. mahler_measure f \<le> root (2 ^ Suc k) (real_of_int (\<Sum>a\<leftarrow>coeffs g. a * a))
[PROOF STEP]
have "\<dots> \<le> root (2 ^ Suc k) (real_of_int (\<Sum>a\<leftarrow>coeffs g. a * a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. root (2 ^ Suc k) ((mahler_measure g)\<^sup>2) \<le> root (2 ^ Suc k) (real_of_int (\<Sum>a\<leftarrow>coeffs g. a * a))
[PROOF STEP]
proof (rule real_root_le_mono, force)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (mahler_measure g)\<^sup>2 \<le> real_of_int (\<Sum>a\<leftarrow>coeffs g. a * a)
[PROOF STEP]
have square_mono: "0 \<le> (x :: real) \<Longrightarrow> x \<le> y \<Longrightarrow> x * x \<le> y * y" for x y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 \<le> x; x \<le> y\<rbrakk> \<Longrightarrow> x * x \<le> y * y
[PROOF STEP]
by (simp add: mult_mono')
[PROOF STATE]
proof (state)
this:
\<lbrakk>0 \<le> ?x; ?x \<le> ?y\<rbrakk> \<Longrightarrow> ?x * ?x \<le> ?y * ?y

goal (1 subgoal):
 1. (mahler_measure g)\<^sup>2 \<le> real_of_int (\<Sum>a\<leftarrow>coeffs g. a * a)
[PROOF STEP]
obtain gs where gs: "coeffs g = gs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>gs. coeffs g = gs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
coeffs g = gs

goal (1 subgoal):
 1. (mahler_measure g)\<^sup>2 \<le> real_of_int (\<Sum>a\<leftarrow>coeffs g. a * a)
[PROOF STEP]
have "(mahler_measure g)\<^sup>2 \<le> real_of_int \<bar>\<Sum>a\<leftarrow>coeffs g. a * a\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (mahler_measure g)\<^sup>2 \<le> real_of_int \<bar>\<Sum>a\<leftarrow>coeffs g. a * a\<bar>
[PROOF STEP]
using square_mono[OF mahler_measure_ge_0 Landau_inequality[of "of_int_poly g", folded mahler_measure_def]]
[PROOF STATE]
proof (prove)
using this:
mahler_measure g * mahler_measure g \<le> l2norm_complex (of_int_poly g) * l2norm_complex (of_int_poly g)

goal (1 subgoal):
 1. (mahler_measure g)\<^sup>2 \<le> real_of_int \<bar>\<Sum>a\<leftarrow>coeffs g. a * a\<bar>
[PROOF STEP]
by (auto simp: power2_eq_square coeffs_map_poly o_def of_int_hom.hom_sum_list)
[PROOF STATE]
proof (state)
this:
(mahler_measure g)\<^sup>2 \<le> real_of_int \<bar>\<Sum>a\<leftarrow>coeffs g. a * a\<bar>

goal (1 subgoal):
 1. (mahler_measure g)\<^sup>2 \<le> real_of_int (\<Sum>a\<leftarrow>coeffs g. a * a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(mahler_measure g)\<^sup>2 \<le> real_of_int \<bar>\<Sum>a\<leftarrow>coeffs g. a * a\<bar>

goal (1 subgoal):
 1. (mahler_measure g)\<^sup>2 \<le> real_of_int (\<Sum>a\<leftarrow>coeffs g. a * a)
[PROOF STEP]
have "\<bar>\<Sum>a\<leftarrow>coeffs g. a * a\<bar> = (\<Sum>a\<leftarrow>coeffs g. a * a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>\<Sum>a\<leftarrow>coeffs g. a * a\<bar> = (\<Sum>a\<leftarrow>coeffs g. a * a)
[PROOF STEP]
unfolding gs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>\<Sum>a\<leftarrow>gs. a * a\<bar> = (\<Sum>a\<leftarrow>gs. a * a)
[PROOF STEP]
by (induct gs, auto)
[PROOF STATE]
proof (state)
this:
\<bar>\<Sum>a\<leftarrow>coeffs g. a * a\<bar> = (\<Sum>a\<leftarrow>coeffs g. a * a)

goal (1 subgoal):
 1. (mahler_measure g)\<^sup>2 \<le> real_of_int (\<Sum>a\<leftarrow>coeffs g. a * a)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(mahler_measure g)\<^sup>2 \<le> real_of_int (\<Sum>a\<leftarrow>coeffs g. a * a)
[PROOF STEP]
show "(mahler_measure g)\<^sup>2 \<le> real_of_int (\<Sum>a\<leftarrow>coeffs g. a * a)"
[PROOF STATE]
proof (prove)
using this:
(mahler_measure g)\<^sup>2 \<le> real_of_int (\<Sum>a\<leftarrow>coeffs g. a * a)

goal (1 subgoal):
 1. (mahler_measure g)\<^sup>2 \<le> real_of_int (\<Sum>a\<leftarrow>coeffs g. a * a)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(mahler_measure g)\<^sup>2 \<le> real_of_int (\<Sum>a\<leftarrow>coeffs g. a * a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
root (2 ^ Suc k) ((mahler_measure g)\<^sup>2) \<le> root (2 ^ Suc k) (real_of_int (\<Sum>a\<leftarrow>coeffs g. a * a))

goal (1 subgoal):
 1. mahler_measure f \<le> root (2 ^ Suc k) (real_of_int (\<Sum>a\<leftarrow>coeffs g. a * a))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
mahler_measure f \<le> root (2 ^ Suc k) (real_of_int (\<Sum>a\<leftarrow>coeffs g. a * a))
[PROOF STEP]
show "mahler_measure f \<le> root (2 ^ Suc k) (real_of_int (\<Sum>a\<leftarrow>coeffs g. a * a))"
[PROOF STATE]
proof (prove)
using this:
mahler_measure f \<le> root (2 ^ Suc k) (real_of_int (\<Sum>a\<leftarrow>coeffs g. a * a))

goal (1 subgoal):
 1. mahler_measure f \<le> root (2 ^ Suc k) (real_of_int (\<Sum>a\<leftarrow>coeffs g. a * a))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
mahler_measure f \<le> root (2 ^ Suc k) (real_of_int (\<Sum>a\<leftarrow>coeffs g. a * a))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Landau_inequality_mahler_measure: "mahler_measure f \<le> sqrt (real_of_int (\<Sum>a\<leftarrow>coeffs f. a * a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mahler_measure f \<le> sqrt (real_of_int (\<Sum>a\<leftarrow>coeffs f. a * a))
[PROOF STEP]
by (rule order.trans[OF mahler_landau_graeffe_approximation_core[OF refl, of _ 0]],
  auto simp: graeffe_poly_impl_def sqrt_def)


[STATEMENT]
lemma mahler_landau_graeffe_approximation:
  assumes g: "g = graeffe_poly_impl f k" "dd = d^(2^(Suc k))" "kk = 2^(Suc k)"
  shows "\<lfloor>real d * mahler_measure f\<rfloor> \<le> mahler_landau_graeffe_approximation kk dd g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>real d * mahler_measure f\<rfloor> \<le> mahler_landau_graeffe_approximation kk dd g
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lfloor>real d * mahler_measure f\<rfloor> \<le> mahler_landau_graeffe_approximation kk dd g
[PROOF STEP]
have id1: "real_of_int (int (d ^ 2 ^ Suc k)) = (real d) ^ 2 ^ Suc k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int (int (d ^ 2 ^ Suc k)) = real d ^ 2 ^ Suc k
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
real_of_int (int (d ^ 2 ^ Suc k)) = real d ^ 2 ^ Suc k

goal (1 subgoal):
 1. \<lfloor>real d * mahler_measure f\<rfloor> \<le> mahler_landau_graeffe_approximation kk dd g
[PROOF STEP]
have id2: "root (2 ^ Suc k) (real d ^ 2 ^ Suc k) = real d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. root (2 ^ Suc k) (real d ^ 2 ^ Suc k) = real d
[PROOF STEP]
by (simp add: real_root_power_cancel)
[PROOF STATE]
proof (state)
this:
root (2 ^ Suc k) (real d ^ 2 ^ Suc k) = real d

goal (1 subgoal):
 1. \<lfloor>real d * mahler_measure f\<rfloor> \<le> mahler_landau_graeffe_approximation kk dd g
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>real d * mahler_measure f\<rfloor> \<le> mahler_landau_graeffe_approximation kk dd g
[PROOF STEP]
unfolding mahler_landau_graeffe_approximation_def Let_def root_int_floor of_int_mult g(2-3)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>real d * mahler_measure f\<rfloor> \<le> \<lfloor>root (2 ^ Suc k) (real_of_int (int (d ^ 2 ^ Suc k)) * real_of_int (\<Sum>a\<leftarrow>coeffs g. a * a))\<rfloor>
[PROOF STEP]
by (rule floor_mono, unfold real_root_mult id1 id2, rule mult_left_mono,
    rule mahler_landau_graeffe_approximation_core[OF g(1)], auto)
[PROOF STATE]
proof (state)
this:
\<lfloor>real d * mahler_measure f\<rfloor> \<le> mahler_landau_graeffe_approximation kk dd g

goal:
No subgoals!
[PROOF STEP]
qed