[STATEMENT]
lemma bisim_J0_J1_start:
  assumes wf: "wf_J_prog P"
  and start: "wf_start_state P C M vs"
  shows "red0_Red1'.mbisim (J0_start_state P C M vs) (J1_start_state (compP1 P) C M vs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. red0_Red1'.mbisim (J0_start_state P C M vs) (J1_start_state (compP1 P) C M vs)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. red0_Red1'.mbisim (J0_start_state P C M vs) (J1_start_state (compP1 P) C M vs)
[PROOF STEP]
from start
[PROOF STATE]
proof (chain)
picking this:
wf_start_state P C M vs
[PROOF STEP]
obtain Ts T pns body D
    where sees: "P \<turnstile> C sees M:Ts\<rightarrow>T=\<lfloor>(pns,body)\<rfloor> in D"
    and conf: "P,start_heap \<turnstile> vs [:\<le>] Ts"
[PROOF STATE]
proof (prove)
using this:
wf_start_state P C M vs

goal (1 subgoal):
 1. (\<And>Ts T pns body D. \<lbrakk>P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>(pns, body)\<rfloor> in D; P,start_heap \<turnstile> vs [:\<le>] Ts\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by cases auto
[PROOF STATE]
proof (state)
this:
P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>(pns, body)\<rfloor> in D
P,start_heap \<turnstile> vs [:\<le>] Ts

goal (1 subgoal):
 1. red0_Red1'.mbisim (J0_start_state P C M vs) (J1_start_state (compP1 P) C M vs)
[PROOF STEP]
from conf
[PROOF STATE]
proof (chain)
picking this:
P,start_heap \<turnstile> vs [:\<le>] Ts
[PROOF STEP]
have vs: "length vs = length Ts"
[PROOF STATE]
proof (prove)
using this:
P,start_heap \<turnstile> vs [:\<le>] Ts

goal (1 subgoal):
 1. length vs = length Ts
[PROOF STEP]
by(rule list_all2_lengthD)
[PROOF STATE]
proof (state)
this:
length vs = length Ts

goal (1 subgoal):
 1. red0_Red1'.mbisim (J0_start_state P C M vs) (J1_start_state (compP1 P) C M vs)
[PROOF STEP]
from sees_wf_mdecl[OF wf_prog_wwf_prog[OF wf] sees]
[PROOF STATE]
proof (chain)
picking this:
wf_mdecl wwf_J_mdecl P D (M, Ts, T, \<lfloor>(pns, body)\<rfloor>)
[PROOF STEP]
have fvbody: "fv body \<subseteq> {this} \<union> set pns" and len: "length pns = length Ts"
[PROOF STATE]
proof (prove)
using this:
wf_mdecl wwf_J_mdecl P D (M, Ts, T, \<lfloor>(pns, body)\<rfloor>)

goal (1 subgoal):
 1. fv body \<subseteq> {this} \<union> set pns &&& length pns = length Ts
[PROOF STEP]
by(auto simp add: wf_mdecl_def)
[PROOF STATE]
proof (state)
this:
fv body \<subseteq> {this} \<union> set pns
length pns = length Ts

goal (1 subgoal):
 1. red0_Red1'.mbisim (J0_start_state P C M vs) (J1_start_state (compP1 P) C M vs)
[PROOF STEP]
with vs
[PROOF STATE]
proof (chain)
picking this:
length vs = length Ts
fv body \<subseteq> {this} \<union> set pns
length pns = length Ts
[PROOF STEP]
have fv: "fv (blocks pns Ts vs body) \<subseteq> {this}"
[PROOF STATE]
proof (prove)
using this:
length vs = length Ts
fv body \<subseteq> {this} \<union> set pns
length pns = length Ts

goal (1 subgoal):
 1. fv (blocks pns Ts vs body) \<subseteq> {this}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fv (blocks pns Ts vs body) \<subseteq> {this}

goal (1 subgoal):
 1. red0_Red1'.mbisim (J0_start_state P C M vs) (J1_start_state (compP1 P) C M vs)
[PROOF STEP]
have wfCM: "wf_J_mdecl P D (M, Ts, T, pns, body)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_J_mdecl P D (M, Ts, T, pns, body)
[PROOF STEP]
using sees_wf_mdecl[OF wf sees]
[PROOF STATE]
proof (prove)
using this:
wf_mdecl wf_J_mdecl P D (M, Ts, T, \<lfloor>(pns, body)\<rfloor>)

goal (1 subgoal):
 1. wf_J_mdecl P D (M, Ts, T, pns, body)
[PROOF STEP]
by(auto simp add: wf_mdecl_def)
[PROOF STATE]
proof (state)
this:
wf_J_mdecl P D (M, Ts, T, pns, body)

goal (1 subgoal):
 1. red0_Red1'.mbisim (J0_start_state P C M vs) (J1_start_state (compP1 P) C M vs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
wf_J_mdecl P D (M, Ts, T, pns, body)
[PROOF STEP]
obtain T' where wtbody: "P,[this # pns [\<mapsto>] Class D # Ts] \<turnstile> body :: T'"
[PROOF STATE]
proof (prove)
using this:
wf_J_mdecl P D (M, Ts, T, pns, body)

goal (1 subgoal):
 1. (\<And>T'. P,[this # pns [\<mapsto>] Class D # Ts] \<turnstile> body :: T' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P,[this # pns [\<mapsto>] Class D # Ts] \<turnstile> body :: T'

goal (1 subgoal):
 1. red0_Red1'.mbisim (J0_start_state P C M vs) (J1_start_state (compP1 P) C M vs)
[PROOF STEP]
hence elbody: "expr_locks body = (\<lambda>l. 0)"
[PROOF STATE]
proof (prove)
using this:
P,[this # pns [\<mapsto>] Class D # Ts] \<turnstile> body :: T'

goal (1 subgoal):
 1. expr_locks body = (\<lambda>l. 0)
[PROOF STEP]
by(rule WT_expr_locks)
[PROOF STATE]
proof (state)
this:
expr_locks body = (\<lambda>l. 0)

goal (1 subgoal):
 1. red0_Red1'.mbisim (J0_start_state P C M vs) (J1_start_state (compP1 P) C M vs)
[PROOF STEP]
hence cisbody: "\<not> contains_insync body"
[PROOF STATE]
proof (prove)
using this:
expr_locks body = (\<lambda>l. 0)

goal (1 subgoal):
 1. \<not> contains_insync body
[PROOF STEP]
by(auto simp add: contains_insync_conv)
[PROOF STATE]
proof (state)
this:
\<not> contains_insync body

goal (1 subgoal):
 1. red0_Red1'.mbisim (J0_start_state P C M vs) (J1_start_state (compP1 P) C M vs)
[PROOF STEP]
from wfCM len vs
[PROOF STATE]
proof (chain)
picking this:
wf_J_mdecl P D (M, Ts, T, pns, body)
length pns = length Ts
length vs = length Ts
[PROOF STEP]
have dabody: "\<D> (blocks pns Ts vs body) \<lfloor>{this}\<rfloor>"
[PROOF STATE]
proof (prove)
using this:
wf_J_mdecl P D (M, Ts, T, pns, body)
length pns = length Ts
length vs = length Ts

goal (1 subgoal):
 1. \<D> (blocks pns Ts vs body) \<lfloor>{this}\<rfloor>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<D> (blocks pns Ts vs body) \<lfloor>{this}\<rfloor>

goal (1 subgoal):
 1. red0_Red1'.mbisim (J0_start_state P C M vs) (J1_start_state (compP1 P) C M vs)
[PROOF STEP]
from sees
[PROOF STATE]
proof (chain)
picking this:
P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>(pns, body)\<rfloor> in D
[PROOF STEP]
have sees1: "compP1 P \<turnstile> C sees M:Ts\<rightarrow>T = \<lfloor>compE1 (this # pns) body\<rfloor> in D"
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>(pns, body)\<rfloor> in D

goal (1 subgoal):
 1. compP1 P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>compE1 (this # pns) body\<rfloor> in D
[PROOF STEP]
by(auto dest: sees_method_compP[where f="(\<lambda>C M Ts T (pns, body). compE1 (this # pns) body)"])
[PROOF STATE]
proof (state)
this:
compP1 P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>compE1 (this # pns) body\<rfloor> in D

goal (1 subgoal):
 1. red0_Red1'.mbisim (J0_start_state P C M vs) (J1_start_state (compP1 P) C M vs)
[PROOF STEP]
let ?e = "blocks1 0 (Class C#Ts) (compE1 (this # pns) body)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. red0_Red1'.mbisim (J0_start_state P C M vs) (J1_start_state (compP1 P) C M vs)
[PROOF STEP]
let ?xs = "Null # vs @ replicate (max_vars body) undefined_value"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. red0_Red1'.mbisim (J0_start_state P C M vs) (J1_start_state (compP1 P) C M vs)
[PROOF STEP]
from fvbody cisbody len vs
[PROOF STATE]
proof (chain)
picking this:
fv body \<subseteq> {this} \<union> set pns
\<not> contains_insync body
length pns = length Ts
length vs = length Ts
[PROOF STEP]
have "bisim [] (blocks (this # pns) (Class D # Ts) (Null # vs) body) (blocks1 (length ([] :: vname list)) (Class D # Ts) (compE1 (this # pns) body)) ?xs"
[PROOF STATE]
proof (prove)
using this:
fv body \<subseteq> {this} \<union> set pns
\<not> contains_insync body
length pns = length Ts
length vs = length Ts

goal (1 subgoal):
 1. bisim [] (blocks (this # pns) (Class D # Ts) (Null # vs) body) (blocks1 (length []) (Class D # Ts) (compE1 (this # pns) body)) (Null # vs @ replicate (max_vars body) undefined_value)
[PROOF STEP]
by-(rule blocks_bisim,(fastforce simp add: nth_Cons' nth_append)+)
[PROOF STATE]
proof (state)
this:
bisim [] (blocks (this # pns) (Class D # Ts) (Null # vs) body) (blocks1 (length []) (Class D # Ts) (compE1 (this # pns) body)) (Null # vs @ replicate (max_vars body) undefined_value)

goal (1 subgoal):
 1. red0_Red1'.mbisim (J0_start_state P C M vs) (J1_start_state (compP1 P) C M vs)
[PROOF STEP]
with fv dabody len vs elbody sees sees1
[PROOF STATE]
proof (chain)
picking this:
fv (blocks pns Ts vs body) \<subseteq> {this}
\<D> (blocks pns Ts vs body) \<lfloor>{this}\<rfloor>
length pns = length Ts
length vs = length Ts
expr_locks body = (\<lambda>l. 0)
P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>(pns, body)\<rfloor> in D
compP1 P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>compE1 (this # pns) body\<rfloor> in D
bisim [] (blocks (this # pns) (Class D # Ts) (Null # vs) body) (blocks1 (length []) (Class D # Ts) (compE1 (this # pns) body)) (Null # vs @ replicate (max_vars body) undefined_value)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
fv (blocks pns Ts vs body) \<subseteq> {this}
\<D> (blocks pns Ts vs body) \<lfloor>{this}\<rfloor>
length pns = length Ts
length vs = length Ts
expr_locks body = (\<lambda>l. 0)
P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>(pns, body)\<rfloor> in D
compP1 P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>compE1 (this # pns) body\<rfloor> in D
bisim [] (blocks (this # pns) (Class D # Ts) (Null # vs) body) (blocks1 (length []) (Class D # Ts) (compE1 (this # pns) body)) (Null # vs @ replicate (max_vars body) undefined_value)

goal (1 subgoal):
 1. red0_Red1'.mbisim (J0_start_state P C M vs) (J1_start_state (compP1 P) C M vs)
[PROOF STEP]
unfolding start_state_def
[PROOF STATE]
proof (prove)
using this:
fv (blocks pns Ts vs body) \<subseteq> {this}
\<D> (blocks pns Ts vs body) \<lfloor>{this}\<rfloor>
length pns = length Ts
length vs = length Ts
expr_locks body = (\<lambda>l. 0)
P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>(pns, body)\<rfloor> in D
compP1 P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>compE1 (this # pns) body\<rfloor> in D
bisim [] (blocks (this # pns) (Class D # Ts) (Null # vs) body) (blocks1 (length []) (Class D # Ts) (compE1 (this # pns) body)) (Null # vs @ replicate (max_vars body) undefined_value)

goal (1 subgoal):
 1. red0_Red1'.mbisim (let (D, Ts, T, m) = method P C M in (K$ None, ([start_tid \<mapsto> ((case the m of (pns, body) \<Rightarrow> \<lambda>vs. (blocks (this # pns) (Class D # Ts) (Null # vs) body, [])) vs, no_wait_locks)], start_heap), Map.empty, {})) (let (D, Ts, T, m) = method (compP1 P) C M in (K$ None, ([start_tid \<mapsto> (((blocks1 0 (Class D # Ts) (the m), Null # vs @ replicate (max_vars (the m)) undefined_value), []), no_wait_locks)], start_heap), Map.empty, {}))
[PROOF STEP]
by(auto intro!: red0_Red1'.mbisimI split: if_split_asm)(auto simp add: bisim_red0_Red1_def blocks1_max_vars intro!: bisim_list.intros bisim_list1I wset_thread_okI)
[PROOF STATE]
proof (state)
this:
red0_Red1'.mbisim (J0_start_state P C M vs) (J1_start_state (compP1 P) C M vs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma induct_gen_abs:
    assumes "\<And> a r. a\<in>set lst \<Longrightarrow> P (f (h a) r) (f (g a) r)"
            "\<And> x y z. P x y \<Longrightarrow> P y z \<Longrightarrow> P x z"
            "P (F (map g lst)) (F (map g lst))"
    shows "P (F (map h lst)) (F (map g lst)) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (F (map h lst)) (F (map g lst))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?a \<in> set lst \<Longrightarrow> P (h ?a \<^bold>* ?r) (g ?a \<^bold>* ?r)
\<lbrakk>P ?x ?y; P ?y ?z\<rbrakk> \<Longrightarrow> P ?x ?z
P (F (map g lst)) (F (map g lst))

goal (1 subgoal):
 1. P (F (map h lst)) (F (map g lst))
[PROOF STEP]
proof(induct lst arbitrary:P)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>P. \<lbrakk>\<And>a r. a \<in> set [] \<Longrightarrow> P (h a \<^bold>* r) (g a \<^bold>* r); \<And>x y z. \<lbrakk>P x y; P y z\<rbrakk> \<Longrightarrow> P x z; P (F (map g [])) (F (map g []))\<rbrakk> \<Longrightarrow> P (F (map h [])) (F (map g []))
 2. \<And>a lst P. \<lbrakk>\<And>P. \<lbrakk>\<And>a r. a \<in> set lst \<Longrightarrow> P (h a \<^bold>* r) (g a \<^bold>* r); \<And>x y z. \<lbrakk>P x y; P y z\<rbrakk> \<Longrightarrow> P x z; P (F (map g lst)) (F (map g lst))\<rbrakk> \<Longrightarrow> P (F (map h lst)) (F (map g lst)); \<And>aa r. aa \<in> set (a # lst) \<Longrightarrow> P (h aa \<^bold>* r) (g aa \<^bold>* r); \<And>x y z. \<lbrakk>P x y; P y z\<rbrakk> \<Longrightarrow> P x z; P (F (map g (a # lst))) (F (map g (a # lst)))\<rbrakk> \<Longrightarrow> P (F (map h (a # lst))) (F (map g (a # lst)))
[PROOF STEP]
case (Cons a as P)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<And>a r. a \<in> set as \<Longrightarrow> ?P (h a \<^bold>* r) (g a \<^bold>* r); \<And>x y z. \<lbrakk>?P x y; ?P y z\<rbrakk> \<Longrightarrow> ?P x z; ?P (F (map g as)) (F (map g as))\<rbrakk> \<Longrightarrow> ?P (F (map h as)) (F (map g as))
?a \<in> set (a # as) \<Longrightarrow> P (h ?a \<^bold>* ?r) (g ?a \<^bold>* ?r)
\<lbrakk>P ?x ?y; P ?y ?z\<rbrakk> \<Longrightarrow> P ?x ?z
P (F (map g (a # as))) (F (map g (a # as)))

goal (2 subgoals):
 1. \<And>P. \<lbrakk>\<And>a r. a \<in> set [] \<Longrightarrow> P (h a \<^bold>* r) (g a \<^bold>* r); \<And>x y z. \<lbrakk>P x y; P y z\<rbrakk> \<Longrightarrow> P x z; P (F (map g [])) (F (map g []))\<rbrakk> \<Longrightarrow> P (F (map h [])) (F (map g []))
 2. \<And>a lst P. \<lbrakk>\<And>P. \<lbrakk>\<And>a r. a \<in> set lst \<Longrightarrow> P (h a \<^bold>* r) (g a \<^bold>* r); \<And>x y z. \<lbrakk>P x y; P y z\<rbrakk> \<Longrightarrow> P x z; P (F (map g lst)) (F (map g lst))\<rbrakk> \<Longrightarrow> P (F (map h lst)) (F (map g lst)); \<And>aa r. aa \<in> set (a # lst) \<Longrightarrow> P (h aa \<^bold>* r) (g aa \<^bold>* r); \<And>x y z. \<lbrakk>P x y; P y z\<rbrakk> \<Longrightarrow> P x z; P (F (map g (a # lst))) (F (map g (a # lst)))\<rbrakk> \<Longrightarrow> P (F (map h (a # lst))) (F (map g (a # lst)))
[PROOF STEP]
have inl:"a\<in>set (a#as)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in> set (a # as)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<in> set (a # as)

goal (2 subgoals):
 1. \<And>P. \<lbrakk>\<And>a r. a \<in> set [] \<Longrightarrow> P (h a \<^bold>* r) (g a \<^bold>* r); \<And>x y z. \<lbrakk>P x y; P y z\<rbrakk> \<Longrightarrow> P x z; P (F (map g [])) (F (map g []))\<rbrakk> \<Longrightarrow> P (F (map h [])) (F (map g []))
 2. \<And>a lst P. \<lbrakk>\<And>P. \<lbrakk>\<And>a r. a \<in> set lst \<Longrightarrow> P (h a \<^bold>* r) (g a \<^bold>* r); \<And>x y z. \<lbrakk>P x y; P y z\<rbrakk> \<Longrightarrow> P x z; P (F (map g lst)) (F (map g lst))\<rbrakk> \<Longrightarrow> P (F (map h lst)) (F (map g lst)); \<And>aa r. aa \<in> set (a # lst) \<Longrightarrow> P (h aa \<^bold>* r) (g aa \<^bold>* r); \<And>x y z. \<lbrakk>P x y; P y z\<rbrakk> \<Longrightarrow> P x z; P (F (map g (a # lst))) (F (map g (a # lst)))\<rbrakk> \<Longrightarrow> P (F (map h (a # lst))) (F (map g (a # lst)))
[PROOF STEP]
let ?uf = "\<lambda> v w. P (f (g a) v) (f (g a) w)"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>P. \<lbrakk>\<And>a r. a \<in> set [] \<Longrightarrow> P (h a \<^bold>* r) (g a \<^bold>* r); \<And>x y z. \<lbrakk>P x y; P y z\<rbrakk> \<Longrightarrow> P x z; P (F (map g [])) (F (map g []))\<rbrakk> \<Longrightarrow> P (F (map h [])) (F (map g []))
 2. \<And>a lst P. \<lbrakk>\<And>P. \<lbrakk>\<And>a r. a \<in> set lst \<Longrightarrow> P (h a \<^bold>* r) (g a \<^bold>* r); \<And>x y z. \<lbrakk>P x y; P y z\<rbrakk> \<Longrightarrow> P x z; P (F (map g lst)) (F (map g lst))\<rbrakk> \<Longrightarrow> P (F (map h lst)) (F (map g lst)); \<And>aa r. aa \<in> set (a # lst) \<Longrightarrow> P (h aa \<^bold>* r) (g aa \<^bold>* r); \<And>x y z. \<lbrakk>P x y; P y z\<rbrakk> \<Longrightarrow> P x z; P (F (map g (a # lst))) (F (map g (a # lst)))\<rbrakk> \<Longrightarrow> P (F (map h (a # lst))) (F (map g (a # lst)))
[PROOF STEP]
have p_suc:"?uf (F (map g as)) (F (map g as))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (g a \<^bold>* F (map g as)) (g a \<^bold>* F (map g as))
[PROOF STEP]
using Cons.prems(3)
[PROOF STATE]
proof (prove)
using this:
P (F (map g (a # as))) (F (map g (a # as)))

goal (1 subgoal):
 1. P (g a \<^bold>* F (map g as)) (g a \<^bold>* F (map g as))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P (g a \<^bold>* F (map g as)) (g a \<^bold>* F (map g as))

goal (2 subgoals):
 1. \<And>P. \<lbrakk>\<And>a r. a \<in> set [] \<Longrightarrow> P (h a \<^bold>* r) (g a \<^bold>* r); \<And>x y z. \<lbrakk>P x y; P y z\<rbrakk> \<Longrightarrow> P x z; P (F (map g [])) (F (map g []))\<rbrakk> \<Longrightarrow> P (F (map h [])) (F (map g []))
 2. \<And>a lst P. \<lbrakk>\<And>P. \<lbrakk>\<And>a r. a \<in> set lst \<Longrightarrow> P (h a \<^bold>* r) (g a \<^bold>* r); \<And>x y z. \<lbrakk>P x y; P y z\<rbrakk> \<Longrightarrow> P x z; P (F (map g lst)) (F (map g lst))\<rbrakk> \<Longrightarrow> P (F (map h lst)) (F (map g lst)); \<And>aa r. aa \<in> set (a # lst) \<Longrightarrow> P (h aa \<^bold>* r) (g aa \<^bold>* r); \<And>x y z. \<lbrakk>P x y; P y z\<rbrakk> \<Longrightarrow> P x z; P (F (map g (a # lst))) (F (map g (a # lst)))\<rbrakk> \<Longrightarrow> P (F (map h (a # lst))) (F (map g (a # lst)))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
P (g a \<^bold>* F (map g as)) (g a \<^bold>* F (map g as))

goal (2 subgoals):
 1. \<And>P. \<lbrakk>\<And>a r. a \<in> set [] \<Longrightarrow> P (h a \<^bold>* r) (g a \<^bold>* r); \<And>x y z. \<lbrakk>P x y; P y z\<rbrakk> \<Longrightarrow> P x z; P (F (map g [])) (F (map g []))\<rbrakk> \<Longrightarrow> P (F (map h [])) (F (map g []))
 2. \<And>a lst P. \<lbrakk>\<And>P. \<lbrakk>\<And>a r. a \<in> set lst \<Longrightarrow> P (h a \<^bold>* r) (g a \<^bold>* r); \<And>x y z. \<lbrakk>P x y; P y z\<rbrakk> \<Longrightarrow> P x z; P (F (map g lst)) (F (map g lst))\<rbrakk> \<Longrightarrow> P (F (map h lst)) (F (map g lst)); \<And>aa r. aa \<in> set (a # lst) \<Longrightarrow> P (h aa \<^bold>* r) (g aa \<^bold>* r); \<And>x y z. \<lbrakk>P x y; P y z\<rbrakk> \<Longrightarrow> P x z; P (F (map g (a # lst))) (F (map g (a # lst)))\<rbrakk> \<Longrightarrow> P (F (map h (a # lst))) (F (map g (a # lst)))
[PROOF STEP]
fix r aa
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>P. \<lbrakk>\<And>a r. a \<in> set [] \<Longrightarrow> P (h a \<^bold>* r) (g a \<^bold>* r); \<And>x y z. \<lbrakk>P x y; P y z\<rbrakk> \<Longrightarrow> P x z; P (F (map g [])) (F (map g []))\<rbrakk> \<Longrightarrow> P (F (map h [])) (F (map g []))
 2. \<And>a lst P. \<lbrakk>\<And>P. \<lbrakk>\<And>a r. a \<in> set lst \<Longrightarrow> P (h a \<^bold>* r) (g a \<^bold>* r); \<And>x y z. \<lbrakk>P x y; P y z\<rbrakk> \<Longrightarrow> P x z; P (F (map g lst)) (F (map g lst))\<rbrakk> \<Longrightarrow> P (F (map h lst)) (F (map g lst)); \<And>aa r. aa \<in> set (a # lst) \<Longrightarrow> P (h aa \<^bold>* r) (g aa \<^bold>* r); \<And>x y z. \<lbrakk>P x y; P y z\<rbrakk> \<Longrightarrow> P x z; P (F (map g (a # lst))) (F (map g (a # lst)))\<rbrakk> \<Longrightarrow> P (F (map h (a # lst))) (F (map g (a # lst)))
[PROOF STEP]
assume "aa \<in> set as"
[PROOF STATE]
proof (state)
this:
aa \<in> set as

goal (2 subgoals):
 1. \<And>P. \<lbrakk>\<And>a r. a \<in> set [] \<Longrightarrow> P (h a \<^bold>* r) (g a \<^bold>* r); \<And>x y z. \<lbrakk>P x y; P y z\<rbrakk> \<Longrightarrow> P x z; P (F (map g [])) (F (map g []))\<rbrakk> \<Longrightarrow> P (F (map h [])) (F (map g []))
 2. \<And>a lst P. \<lbrakk>\<And>P. \<lbrakk>\<And>a r. a \<in> set lst \<Longrightarrow> P (h a \<^bold>* r) (g a \<^bold>* r); \<And>x y z. \<lbrakk>P x y; P y z\<rbrakk> \<Longrightarrow> P x z; P (F (map g lst)) (F (map g lst))\<rbrakk> \<Longrightarrow> P (F (map h lst)) (F (map g lst)); \<And>aa r. aa \<in> set (a # lst) \<Longrightarrow> P (h aa \<^bold>* r) (g aa \<^bold>* r); \<And>x y z. \<lbrakk>P x y; P y z\<rbrakk> \<Longrightarrow> P x z; P (F (map g (a # lst))) (F (map g (a # lst)))\<rbrakk> \<Longrightarrow> P (F (map h (a # lst))) (F (map g (a # lst)))
[PROOF STEP]
hence ins:"aa \<in> set (a#as)"
[PROOF STATE]
proof (prove)
using this:
aa \<in> set as

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

goal (2 subgoals):
 1. \<And>P. \<lbrakk>\<And>a r. a \<in> set [] \<Longrightarrow> P (h a \<^bold>* r) (g a \<^bold>* r); \<And>x y z. \<lbrakk>P x y; P y z\<rbrakk> \<Longrightarrow> P x z; P (F (map g [])) (F (map g []))\<rbrakk> \<Longrightarrow> P (F (map h [])) (F (map g []))
 2. \<And>a lst P. \<lbrakk>\<And>P. \<lbrakk>\<And>a r. a \<in> set lst \<Longrightarrow> P (h a \<^bold>* r) (g a \<^bold>* r); \<And>x y z. \<lbrakk>P x y; P y z\<rbrakk> \<Longrightarrow> P x z; P (F (map g lst)) (F (map g lst))\<rbrakk> \<Longrightarrow> P (F (map h lst)) (F (map g lst)); \<And>aa r. aa \<in> set (a # lst) \<Longrightarrow> P (h aa \<^bold>* r) (g aa \<^bold>* r); \<And>x y z. \<lbrakk>P x y; P y z\<rbrakk> \<Longrightarrow> P x z; P (F (map g (a # lst))) (F (map g (a # lst)))\<rbrakk> \<Longrightarrow> P (F (map h (a # lst))) (F (map g (a # lst)))
[PROOF STEP]
have "P (f (g a) (f (h aa) r)) (f (g a) (f (g aa) r))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (g a \<^bold>* (h aa \<^bold>* r)) (g a \<^bold>* (g aa \<^bold>* r))
[PROOF STEP]
using Cons.prems(1)[of aa "f r (g a)",OF ins]
[PROOF STATE]
proof (prove)
using this:
P (h aa \<^bold>* (r \<^bold>* g a)) (g aa \<^bold>* (r \<^bold>* g a))

goal (1 subgoal):
 1. P (g a \<^bold>* (h aa \<^bold>* r)) (g a \<^bold>* (g aa \<^bold>* r))
[PROOF STEP]
by (auto simp: assoc commute left_commute)
[PROOF STATE]
proof (state)
this:
P (g a \<^bold>* (h aa \<^bold>* r)) (g a \<^bold>* (g aa \<^bold>* r))

goal (2 subgoals):
 1. \<And>P. \<lbrakk>\<And>a r. a \<in> set [] \<Longrightarrow> P (h a \<^bold>* r) (g a \<^bold>* r); \<And>x y z. \<lbrakk>P x y; P y z\<rbrakk> \<Longrightarrow> P x z; P (F (map g [])) (F (map g []))\<rbrakk> \<Longrightarrow> P (F (map h [])) (F (map g []))
 2. \<And>a lst P. \<lbrakk>\<And>P. \<lbrakk>\<And>a r. a \<in> set lst \<Longrightarrow> P (h a \<^bold>* r) (g a \<^bold>* r); \<And>x y z. \<lbrakk>P x y; P y z\<rbrakk> \<Longrightarrow> P x z; P (F (map g lst)) (F (map g lst))\<rbrakk> \<Longrightarrow> P (F (map h lst)) (F (map g lst)); \<And>aa r. aa \<in> set (a # lst) \<Longrightarrow> P (h aa \<^bold>* r) (g aa \<^bold>* r); \<And>x y z. \<lbrakk>P x y; P y z\<rbrakk> \<Longrightarrow> P x z; P (F (map g (a # lst))) (F (map g (a # lst)))\<rbrakk> \<Longrightarrow> P (F (map h (a # lst))) (F (map g (a # lst)))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?aa2 \<in> set as \<Longrightarrow> P (g a \<^bold>* (h ?aa2 \<^bold>* ?r2)) (g a \<^bold>* (g ?aa2 \<^bold>* ?r2))

goal (2 subgoals):
 1. \<And>P. \<lbrakk>\<And>a r. a \<in> set [] \<Longrightarrow> P (h a \<^bold>* r) (g a \<^bold>* r); \<And>x y z. \<lbrakk>P x y; P y z\<rbrakk> \<Longrightarrow> P x z; P (F (map g [])) (F (map g []))\<rbrakk> \<Longrightarrow> P (F (map h [])) (F (map g []))
 2. \<And>a lst P. \<lbrakk>\<And>P. \<lbrakk>\<And>a r. a \<in> set lst \<Longrightarrow> P (h a \<^bold>* r) (g a \<^bold>* r); \<And>x y z. \<lbrakk>P x y; P y z\<rbrakk> \<Longrightarrow> P x z; P (F (map g lst)) (F (map g lst))\<rbrakk> \<Longrightarrow> P (F (map h lst)) (F (map g lst)); \<And>aa r. aa \<in> set (a # lst) \<Longrightarrow> P (h aa \<^bold>* r) (g aa \<^bold>* r); \<And>x y z. \<lbrakk>P x y; P y z\<rbrakk> \<Longrightarrow> P x z; P (F (map g (a # lst))) (F (map g (a # lst)))\<rbrakk> \<Longrightarrow> P (F (map h (a # lst))) (F (map g (a # lst)))
[PROOF STEP]
note h = this
[PROOF STATE]
proof (state)
this:
?aa2 \<in> set as \<Longrightarrow> P (g a \<^bold>* (h ?aa2 \<^bold>* ?r2)) (g a \<^bold>* (g ?aa2 \<^bold>* ?r2))

goal (2 subgoals):
 1. \<And>P. \<lbrakk>\<And>a r. a \<in> set [] \<Longrightarrow> P (h a \<^bold>* r) (g a \<^bold>* r); \<And>x y z. \<lbrakk>P x y; P y z\<rbrakk> \<Longrightarrow> P x z; P (F (map g [])) (F (map g []))\<rbrakk> \<Longrightarrow> P (F (map h [])) (F (map g []))
 2. \<And>a lst P. \<lbrakk>\<And>P. \<lbrakk>\<And>a r. a \<in> set lst \<Longrightarrow> P (h a \<^bold>* r) (g a \<^bold>* r); \<And>x y z. \<lbrakk>P x y; P y z\<rbrakk> \<Longrightarrow> P x z; P (F (map g lst)) (F (map g lst))\<rbrakk> \<Longrightarrow> P (F (map h lst)) (F (map g lst)); \<And>aa r. aa \<in> set (a # lst) \<Longrightarrow> P (h aa \<^bold>* r) (g aa \<^bold>* r); \<And>x y z. \<lbrakk>P x y; P y z\<rbrakk> \<Longrightarrow> P x z; P (F (map g (a # lst))) (F (map g (a # lst)))\<rbrakk> \<Longrightarrow> P (F (map h (a # lst))) (F (map g (a # lst)))
[PROOF STEP]
from Cons.hyps(1)[of ?uf, OF h Cons.prems(2)[simplified] p_suc]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<And>a r. a \<in> set as \<Longrightarrow> a \<in> set as; \<And>x y z. \<lbrakk>P (g a \<^bold>* x) (g a \<^bold>* y); P (g a \<^bold>* y) (g a \<^bold>* z)\<rbrakk> \<Longrightarrow> P (g a \<^bold>* x) (?y x y z); \<And>x y z. \<lbrakk>P (g a \<^bold>* x) (g a \<^bold>* y); P (g a \<^bold>* y) (g a \<^bold>* z)\<rbrakk> \<Longrightarrow> P (?y x y z) (g a \<^bold>* z)\<rbrakk> \<Longrightarrow> P (g a \<^bold>* F (map h as)) (g a \<^bold>* F (map g as))
[PROOF STEP]
have e1:"P (f (g a) (F (map h as))) (f (g a) (F (map g as)))"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>a r. a \<in> set as \<Longrightarrow> a \<in> set as; \<And>x y z. \<lbrakk>P (g a \<^bold>* x) (g a \<^bold>* y); P (g a \<^bold>* y) (g a \<^bold>* z)\<rbrakk> \<Longrightarrow> P (g a \<^bold>* x) (?y x y z); \<And>x y z. \<lbrakk>P (g a \<^bold>* x) (g a \<^bold>* y); P (g a \<^bold>* y) (g a \<^bold>* z)\<rbrakk> \<Longrightarrow> P (?y x y z) (g a \<^bold>* z)\<rbrakk> \<Longrightarrow> P (g a \<^bold>* F (map h as)) (g a \<^bold>* F (map g as))

goal (1 subgoal):
 1. P (g a \<^bold>* F (map h as)) (g a \<^bold>* F (map g as))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P (g a \<^bold>* F (map h as)) (g a \<^bold>* F (map g as))

goal (2 subgoals):
 1. \<And>P. \<lbrakk>\<And>a r. a \<in> set [] \<Longrightarrow> P (h a \<^bold>* r) (g a \<^bold>* r); \<And>x y z. \<lbrakk>P x y; P y z\<rbrakk> \<Longrightarrow> P x z; P (F (map g [])) (F (map g []))\<rbrakk> \<Longrightarrow> P (F (map h [])) (F (map g []))
 2. \<And>a lst P. \<lbrakk>\<And>P. \<lbrakk>\<And>a r. a \<in> set lst \<Longrightarrow> P (h a \<^bold>* r) (g a \<^bold>* r); \<And>x y z. \<lbrakk>P x y; P y z\<rbrakk> \<Longrightarrow> P x z; P (F (map g lst)) (F (map g lst))\<rbrakk> \<Longrightarrow> P (F (map h lst)) (F (map g lst)); \<And>aa r. aa \<in> set (a # lst) \<Longrightarrow> P (h aa \<^bold>* r) (g aa \<^bold>* r); \<And>x y z. \<lbrakk>P x y; P y z\<rbrakk> \<Longrightarrow> P x z; P (F (map g (a # lst))) (F (map g (a # lst)))\<rbrakk> \<Longrightarrow> P (F (map h (a # lst))) (F (map g (a # lst)))
[PROOF STEP]
have e2:"P (f (h a) (F (map h as))) (f (g a) (F (map h as)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (h a \<^bold>* F (map h as)) (g a \<^bold>* F (map h as))
[PROOF STEP]
using Cons.prems(1)[OF inl]
[PROOF STATE]
proof (prove)
using this:
P (h a \<^bold>* ?r) (g a \<^bold>* ?r)

goal (1 subgoal):
 1. P (h a \<^bold>* F (map h as)) (g a \<^bold>* F (map h as))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
P (h a \<^bold>* F (map h as)) (g a \<^bold>* F (map h as))

goal (2 subgoals):
 1. \<And>P. \<lbrakk>\<And>a r. a \<in> set [] \<Longrightarrow> P (h a \<^bold>* r) (g a \<^bold>* r); \<And>x y z. \<lbrakk>P x y; P y z\<rbrakk> \<Longrightarrow> P x z; P (F (map g [])) (F (map g []))\<rbrakk> \<Longrightarrow> P (F (map h [])) (F (map g []))
 2. \<And>a lst P. \<lbrakk>\<And>P. \<lbrakk>\<And>a r. a \<in> set lst \<Longrightarrow> P (h a \<^bold>* r) (g a \<^bold>* r); \<And>x y z. \<lbrakk>P x y; P y z\<rbrakk> \<Longrightarrow> P x z; P (F (map g lst)) (F (map g lst))\<rbrakk> \<Longrightarrow> P (F (map h lst)) (F (map g lst)); \<And>aa r. aa \<in> set (a # lst) \<Longrightarrow> P (h aa \<^bold>* r) (g aa \<^bold>* r); \<And>x y z. \<lbrakk>P x y; P y z\<rbrakk> \<Longrightarrow> P x z; P (F (map g (a # lst))) (F (map g (a # lst)))\<rbrakk> \<Longrightarrow> P (F (map h (a # lst))) (F (map g (a # lst)))
[PROOF STEP]
from Cons(3)[OF e2 e1]
[PROOF STATE]
proof (chain)
picking this:
P (h a \<^bold>* F (map h as)) (g a \<^bold>* F (map g as))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
P (h a \<^bold>* F (map h as)) (g a \<^bold>* F (map g as))

goal (1 subgoal):
 1. P (F (map h (a # as))) (F (map g (a # as)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P (F (map h (a # as))) (F (map g (a # as)))

goal (1 subgoal):
 1. \<And>P. \<lbrakk>\<And>a r. a \<in> set [] \<Longrightarrow> P (h a \<^bold>* r) (g a \<^bold>* r); \<And>x y z. \<lbrakk>P x y; P y z\<rbrakk> \<Longrightarrow> P x z; P (F (map g [])) (F (map g []))\<rbrakk> \<Longrightarrow> P (F (map h [])) (F (map g []))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P. \<lbrakk>\<And>a r. a \<in> set [] \<Longrightarrow> P (h a \<^bold>* r) (g a \<^bold>* r); \<And>x y z. \<lbrakk>P x y; P y z\<rbrakk> \<Longrightarrow> P x z; P (F (map g [])) (F (map g []))\<rbrakk> \<Longrightarrow> P (F (map h [])) (F (map g []))
[PROOF STEP]
qed auto


[STATEMENT]
lemma complex_roots:
  "smult (lead_coeff p) (\<Prod>a\<leftarrow>complex_roots_complex p. [:- a, 1:]) = p"
  "length (complex_roots_complex p) = degree p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Polynomial.smult (lead_coeff p) (\<Prod>a\<leftarrow>complex_roots_complex p. [:- a, 1:]) = p &&& length (complex_roots_complex p) = degree p
[PROOF STEP]
using someI_ex[OF fundamental_theorem_algebra_factorized]
[PROOF STATE]
proof (prove)
using this:
Polynomial.smult (lead_coeff ?p1) (\<Prod>a\<leftarrow>(SOME x. Polynomial.smult (lead_coeff ?p1) (\<Prod>a\<leftarrow>x. [:- a, 1:]) = ?p1 \<and> length x = degree ?p1). [:- a, 1:]) = ?p1 \<and> length (SOME x. Polynomial.smult (lead_coeff ?p1) (\<Prod>a\<leftarrow>x. [:- a, 1:]) = ?p1 \<and> length x = degree ?p1) = degree ?p1

goal (1 subgoal):
 1. Polynomial.smult (lead_coeff p) (\<Prod>a\<leftarrow>complex_roots_complex p. [:- a, 1:]) = p &&& length (complex_roots_complex p) = degree p
[PROOF STEP]
unfolding complex_roots_complex_def
[PROOF STATE]
proof (prove)
using this:
Polynomial.smult (lead_coeff ?p1) (\<Prod>a\<leftarrow>(SOME x. Polynomial.smult (lead_coeff ?p1) (\<Prod>a\<leftarrow>x. [:- a, 1:]) = ?p1 \<and> length x = degree ?p1). [:- a, 1:]) = ?p1 \<and> length (SOME x. Polynomial.smult (lead_coeff ?p1) (\<Prod>a\<leftarrow>x. [:- a, 1:]) = ?p1 \<and> length x = degree ?p1) = degree ?p1

goal (1 subgoal):
 1. Polynomial.smult (lead_coeff p) (\<Prod>a\<leftarrow>(SOME as. Polynomial.smult (lead_coeff p) (\<Prod>a\<leftarrow>as. [:- a, 1:]) = p \<and> length as = degree p). [:- a, 1:]) = p &&& length (SOME as. Polynomial.smult (lead_coeff p) (\<Prod>a\<leftarrow>as. [:- a, 1:]) = p \<and> length as = degree p) = degree p
[PROOF STEP]
by simp_all


[STATEMENT]
lemma complex_roots_c [simp]:
  "complex_roots_complex [:c:] = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. complex_roots_complex [:c:] = []
[PROOF STEP]
using complex_roots(2) [of "[:c:]"]
[PROOF STATE]
proof (prove)
using this:
length (complex_roots_complex [:c:]) = degree [:c:]

goal (1 subgoal):
 1. complex_roots_complex [:c:] = []
[PROOF STEP]
by simp


[STATEMENT]
lemma complex_roots_1 [simp]:
  "complex_roots_complex 1 = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. complex_roots_complex 1 = []
[PROOF STEP]
using complex_roots_c [of 1]
[PROOF STATE]
proof (prove)
using this:
complex_roots_complex [:1:] = []

goal (1 subgoal):
 1. complex_roots_complex 1 = []
[PROOF STEP]
by (simp add: pCons_one)


[STATEMENT]
lemma linear_term_irreducible\<^sub>d[simp]: "irreducible\<^sub>d [: a, 1:]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. irreducible\<^sub>d [:a, 1::'a:]
[PROOF STEP]
by (rule linear_irreducible\<^sub>d, simp)


[STATEMENT]
lemma complex_roots_int:
  "smult (lead_coeff p) (\<Prod>a\<leftarrow>complex_roots_int p. [:- a, 1:]) = map_poly of_int p"
  "length (complex_roots_int p) = degree p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Polynomial.smult (complex_of_int (lead_coeff p)) (\<Prod>a\<leftarrow>complex_roots_int p. [:- a, 1:]) = of_int_poly p &&& length (complex_roots_int p) = degree p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Polynomial.smult (complex_of_int (lead_coeff p)) (\<Prod>a\<leftarrow>complex_roots_int p. [:- a, 1:]) = of_int_poly p
 2. length (complex_roots_int p) = degree p
[PROOF STEP]
show "smult (lead_coeff p) (\<Prod>a\<leftarrow>complex_roots_int p. [:- a, 1:]) = map_poly of_int p"
  "length (complex_roots_int p) = degree p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Polynomial.smult (complex_of_int (lead_coeff p)) (\<Prod>a\<leftarrow>complex_roots_int p. [:- a, 1:]) = of_int_poly p &&& length (complex_roots_int p) = degree p
[PROOF STEP]
using complex_roots[of "map_poly of_int p"]
[PROOF STATE]
proof (prove)
using this:
Polynomial.smult (lead_coeff (of_int_poly p)) (\<Prod>a\<leftarrow>complex_roots_complex (of_int_poly p). [:- a, 1:]) = of_int_poly p
length (complex_roots_complex (of_int_poly p)) = degree (of_int_poly p)

goal (1 subgoal):
 1. Polynomial.smult (complex_of_int (lead_coeff p)) (\<Prod>a\<leftarrow>complex_roots_int p. [:- a, 1:]) = of_int_poly p &&& length (complex_roots_int p) = degree p
[PROOF STEP]
unfolding complex_roots_int_def
[PROOF STATE]
proof (prove)
using this:
Polynomial.smult (lead_coeff (of_int_poly p)) (\<Prod>a\<leftarrow>complex_roots_complex (of_int_poly p). [:- a, 1:]) = of_int_poly p
length (complex_roots_complex (of_int_poly p)) = degree (of_int_poly p)

goal (1 subgoal):
 1. Polynomial.smult (complex_of_int (lead_coeff p)) (\<Prod>a\<leftarrow>complex_roots_complex (of_int_poly p). [:- a, 1:]) = of_int_poly p &&& length (complex_roots_complex (of_int_poly p)) = degree p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Polynomial.smult (complex_of_int (lead_coeff p)) (\<Prod>a\<leftarrow>complex_roots_int p. [:- a, 1:]) = of_int_poly p
length (complex_roots_int p) = degree p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mahler_measure_poly_via_monic :
  "mahler_measure_poly p = cmod (lead_coeff p) * mahler_measure_monic p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mahler_measure_poly p = cmod (lead_coeff p) * mahler_measure_monic p
[PROOF STEP]
unfolding mahler_measure_poly_def mahler_measure_monic_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod (lead_coeff p) * (\<Prod>a\<leftarrow>complex_roots_complex p. max 1 (cmod a)) = cmod (lead_coeff p) * (\<Prod>a\<leftarrow>complex_roots_complex p. max 1 (cmod a))
[PROOF STEP]
by simp


[STATEMENT]
lemma smult_inj[simp]: assumes "(a::'a::idom) \<noteq> 0" shows "inj (smult a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj (Polynomial.smult a)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inj (Polynomial.smult a)
[PROOF STEP]
interpret map_poly_inj_zero_hom "(*) a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_poly_inj_zero_hom ((*) a)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a \<noteq> (0::'a)

goal (1 subgoal):
 1. map_poly_inj_zero_hom ((*) a)
[PROOF STEP]
by (unfold_locales, auto)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inj (Polynomial.smult a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj (Polynomial.smult a)
[PROOF STEP]
unfolding smult_as_map_poly
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj (map_poly ((*) a))
[PROOF STEP]
by (rule inj_f)
[PROOF STATE]
proof (state)
this:
inj (Polynomial.smult a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma reconstruct_is_original_poly:
  "reconstruct_poly (lead_coeff p) (complex_roots_complex p) = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reconstruct_poly (lead_coeff p) (complex_roots_complex p) = p
[PROOF STEP]
using complex_roots(1)
[PROOF STATE]
proof (prove)
using this:
Polynomial.smult (lead_coeff ?p) (\<Prod>a\<leftarrow>complex_roots_complex ?p. [:- a, 1:]) = ?p

goal (1 subgoal):
 1. reconstruct_poly (lead_coeff p) (complex_roots_complex p) = p
[PROOF STEP]
by (simp add: reconstruct_poly_def)


[STATEMENT]
lemma reconstruct_with_type_conversion:
  "smult (lead_coeff (map_poly of_int f)) (prod_list (map (\<lambda> a. [:- a, 1:]) (complex_roots_int f)))
   = map_poly of_int f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Polynomial.smult (lead_coeff (of_int_poly f)) (\<Prod>a\<leftarrow>complex_roots_int f. [:- a, 1:]) = of_int_poly f
[PROOF STEP]
unfolding complex_roots_int_def complex_roots(1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int_poly f = of_int_poly f
[PROOF STEP]
by simp


[STATEMENT]
lemma reconstruct_prod:
  shows "reconstruct_poly (a::complex) as * reconstruct_poly b bs
        = reconstruct_poly (a * b) (as @ bs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reconstruct_poly a as * reconstruct_poly b bs = reconstruct_poly (a * b) (as @ bs)
[PROOF STEP]
unfolding reconstruct_poly_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Polynomial.smult a (\<Prod>a\<leftarrow>as. [:- a, 1:]) * Polynomial.smult b (\<Prod>a\<leftarrow>bs. [:- a, 1:]) = Polynomial.smult (a * b) (\<Prod>a\<leftarrow>as @ bs. [:- a, 1:])
[PROOF STEP]
by auto


[STATEMENT]
lemma linear_term_inj[simplified,simp]: "inj (\<lambda> a. [:- a, 1::'a::idom:])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj (\<lambda>a. [:- a, 1::'a:])
[PROOF STEP]
unfolding inj_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>UNIV. \<forall>y\<in>UNIV. [:- x, 1::'a:] = [:- y, 1::'a:] \<longrightarrow> x = y
[PROOF STEP]
by simp


[STATEMENT]
lemma reconstruct_poly_monic_defines_mset:
  assumes "(\<Prod>a\<leftarrow>as. [:- a, 1:]) = (\<Prod>a\<leftarrow>bs. [:- a, 1::'a::field:])"
  shows "mset as = mset bs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset as = mset bs
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mset as = mset bs
[PROOF STEP]
let ?as = "mset (map (\<lambda> a. [:- a, 1:]) as)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mset as = mset bs
[PROOF STEP]
let ?bs = "mset (map (\<lambda> a. [:- a, 1:]) bs)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mset as = mset bs
[PROOF STEP]
have eq_smult:"prod_mset ?as = prod_mset ?bs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Prod>\<^sub># (mset (map (\<lambda>a. [:- a, 1::'a:]) as)) = \<Prod>\<^sub># (mset (map (\<lambda>a. [:- a, 1::'a:]) bs))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(\<Prod>a\<leftarrow>as. [:- a, 1::'a:]) = (\<Prod>a\<leftarrow>bs. [:- a, 1::'a:])

goal (1 subgoal):
 1. \<Prod>\<^sub># (mset (map (\<lambda>a. [:- a, 1::'a:]) as)) = \<Prod>\<^sub># (mset (map (\<lambda>a. [:- a, 1::'a:]) bs))
[PROOF STEP]
by (metis prod_mset_prod_list)
[PROOF STATE]
proof (state)
this:
\<Prod>\<^sub># (mset (map (\<lambda>a. [:- a, 1::'a:]) as)) = \<Prod>\<^sub># (mset (map (\<lambda>a. [:- a, 1::'a:]) bs))

goal (1 subgoal):
 1. mset as = mset bs
[PROOF STEP]
have irr:"\<And> as::'a list. set_mset (mset (map (\<lambda> a. [:- a, 1:]) as)) \<subseteq> {q. irreducible q \<and> monic q}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>as. set_mset (mset (map (\<lambda>a. [:- a, 1::'a:]) as)) \<subseteq> {q. irreducible q \<and> monic q}
[PROOF STEP]
by (auto intro!: linear_term_irreducible\<^sub>d[of "-_::'a", simplified])
[PROOF STATE]
proof (state)
this:
set_mset (mset (map (\<lambda>a. [:- a, 1::'a:]) ?as)) \<subseteq> {q. irreducible q \<and> monic q}

goal (1 subgoal):
 1. mset as = mset bs
[PROOF STEP]
from monic_factorization_unique_mset[OF eq_smult irr irr]
[PROOF STATE]
proof (chain)
picking this:
mset (map (\<lambda>a. [:- a, 1::'a:]) as) = mset (map (\<lambda>a. [:- a, 1::'a:]) bs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
mset (map (\<lambda>a. [:- a, 1::'a:]) as) = mset (map (\<lambda>a. [:- a, 1::'a:]) bs)

goal (1 subgoal):
 1. mset as = mset bs
[PROOF STEP]
apply (subst inj_eq[OF multiset.inj_map,symmetric])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. mset (map (\<lambda>a. [:- a, 1::'a:]) as) = mset (map (\<lambda>a. [:- a, 1::'a:]) bs) \<Longrightarrow> inj ?f4
 2. mset (map (\<lambda>a. [:- a, 1::'a:]) as) = mset (map (\<lambda>a. [:- a, 1::'a:]) bs) \<Longrightarrow> image_mset ?f4 (mset as) = image_mset ?f4 (mset bs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mset as = mset bs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma reconstruct_poly_defines_mset_of_argument:
  assumes "(a::'a::field) \<noteq> 0"
          "reconstruct_poly a as = reconstruct_poly a bs"
  shows "mset as = mset bs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset as = mset bs
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mset as = mset bs
[PROOF STEP]
have eq_smult:"smult a (\<Prod>a\<leftarrow>as. [:- a, 1:]) = smult a (\<Prod>a\<leftarrow>bs. [:- a, 1:])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Polynomial.smult a (\<Prod>a\<leftarrow>as. [:- a, 1::'a:]) = Polynomial.smult a (\<Prod>a\<leftarrow>bs. [:- a, 1::'a:])
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
reconstruct_poly a as = reconstruct_poly a bs

goal (1 subgoal):
 1. Polynomial.smult a (\<Prod>a\<leftarrow>as. [:- a, 1::'a:]) = Polynomial.smult a (\<Prod>a\<leftarrow>bs. [:- a, 1::'a:])
[PROOF STEP]
by (auto simp:reconstruct_poly_def)
[PROOF STATE]
proof (state)
this:
Polynomial.smult a (\<Prod>a\<leftarrow>as. [:- a, 1::'a:]) = Polynomial.smult a (\<Prod>a\<leftarrow>bs. [:- a, 1::'a:])

goal (1 subgoal):
 1. mset as = mset bs
[PROOF STEP]
from reconstruct_poly_monic_defines_mset[OF Fun.injD[OF smult_inj[OF assms(1)] eq_smult]]
[PROOF STATE]
proof (chain)
picking this:
mset as = mset bs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
mset as = mset bs

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma complex_roots_complex_prod [simp]:
  assumes "f \<noteq> 0" "g \<noteq> 0"
  shows  "mset (complex_roots_complex (f * g))
        = mset (complex_roots_complex f) + mset (complex_roots_complex g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset (complex_roots_complex (f * g)) = mset (complex_roots_complex f) + mset (complex_roots_complex g)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mset (complex_roots_complex (f * g)) = mset (complex_roots_complex f) + mset (complex_roots_complex g)
[PROOF STEP]
let ?p = "f * g"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mset (complex_roots_complex (f * g)) = mset (complex_roots_complex f) + mset (complex_roots_complex g)
[PROOF STEP]
let "?lc v" = "(lead_coeff (v:: complex poly))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mset (complex_roots_complex (f * g)) = mset (complex_roots_complex f) + mset (complex_roots_complex g)
[PROOF STEP]
have nonzero_prod:"?lc ?p \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lead_coeff (f * g) \<noteq> 0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
f \<noteq> 0
g \<noteq> 0

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

goal (1 subgoal):
 1. mset (complex_roots_complex (f * g)) = mset (complex_roots_complex f) + mset (complex_roots_complex g)
[PROOF STEP]
from reconstruct_prod[of "?lc f" "complex_roots_complex f" "?lc g" "complex_roots_complex g"]
[PROOF STATE]
proof (chain)
picking this:
reconstruct_poly (lead_coeff f) (complex_roots_complex f) * reconstruct_poly (lead_coeff g) (complex_roots_complex g) = reconstruct_poly (lead_coeff f * lead_coeff g) (complex_roots_complex f @ complex_roots_complex g)
[PROOF STEP]
have "reconstruct_poly (?lc ?p) (complex_roots_complex ?p)
       = reconstruct_poly (?lc ?p) (complex_roots_complex f @ complex_roots_complex g)"
[PROOF STATE]
proof (prove)
using this:
reconstruct_poly (lead_coeff f) (complex_roots_complex f) * reconstruct_poly (lead_coeff g) (complex_roots_complex g) = reconstruct_poly (lead_coeff f * lead_coeff g) (complex_roots_complex f @ complex_roots_complex g)

goal (1 subgoal):
 1. reconstruct_poly (lead_coeff (f * g)) (complex_roots_complex (f * g)) = reconstruct_poly (lead_coeff (f * g)) (complex_roots_complex f @ complex_roots_complex g)
[PROOF STEP]
unfolding lead_coeff_mult[symmetric] reconstruct_is_original_poly
[PROOF STATE]
proof (prove)
using this:
f * g = reconstruct_poly (lead_coeff (f * g)) (complex_roots_complex f @ complex_roots_complex g)

goal (1 subgoal):
 1. f * g = reconstruct_poly (lead_coeff (f * g)) (complex_roots_complex f @ complex_roots_complex g)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
reconstruct_poly (lead_coeff (f * g)) (complex_roots_complex (f * g)) = reconstruct_poly (lead_coeff (f * g)) (complex_roots_complex f @ complex_roots_complex g)

goal (1 subgoal):
 1. mset (complex_roots_complex (f * g)) = mset (complex_roots_complex f) + mset (complex_roots_complex g)
[PROOF STEP]
from reconstruct_poly_defines_mset_of_argument[OF nonzero_prod this]
[PROOF STATE]
proof (chain)
picking this:
mset (complex_roots_complex (f * g)) = mset (complex_roots_complex f @ complex_roots_complex g)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
mset (complex_roots_complex (f * g)) = mset (complex_roots_complex f @ complex_roots_complex g)

goal (1 subgoal):
 1. mset (complex_roots_complex (f * g)) = mset (complex_roots_complex f) + mset (complex_roots_complex g)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
mset (complex_roots_complex (f * g)) = mset (complex_roots_complex f) + mset (complex_roots_complex g)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mset_mult_add:
  assumes "mset (a::'a::field list) = mset b + mset c"
  shows "prod_list a = prod_list b * prod_list c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prod_list a = prod_list b * prod_list c
[PROOF STEP]
unfolding prod_mset_prod_list[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Prod>\<^sub># (mset a) = \<Prod>\<^sub># (mset b) * \<Prod>\<^sub># (mset c)
[PROOF STEP]
using prod_mset_Un[of "mset b" "mset c",unfolded assms[symmetric]]
[PROOF STATE]
proof (prove)
using this:
\<Prod>\<^sub># (mset a) = \<Prod>\<^sub># (mset b) * \<Prod>\<^sub># (mset c)

goal (1 subgoal):
 1. \<Prod>\<^sub># (mset a) = \<Prod>\<^sub># (mset b) * \<Prod>\<^sub># (mset c)
[PROOF STEP]
.


[STATEMENT]
lemma mset_mult_add_2:
  assumes "mset a = mset b + mset c"
  shows "prod_list (map i a::'b::field list) = prod_list (map i b) * prod_list (map i c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prod_list (map i a) = prod_list (map i b) * prod_list (map i c)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prod_list (map i a) = prod_list (map i b) * prod_list (map i c)
[PROOF STEP]
have r:"mset (map i a) = mset (map i b) + mset (map i c) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mset (map i a) = mset (map i b) + mset (map i c)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
mset a = mset b + mset c

goal (1 subgoal):
 1. mset (map i a) = mset (map i b) + mset (map i c)
[PROOF STEP]
by (metis map_append mset_append mset_map)
[PROOF STATE]
proof (state)
this:
mset (map i a) = mset (map i b) + mset (map i c)

goal (1 subgoal):
 1. prod_list (map i a) = prod_list (map i b) * prod_list (map i c)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prod_list (map i a) = prod_list (map i b) * prod_list (map i c)
[PROOF STEP]
using mset_mult_add[OF r]
[PROOF STATE]
proof (prove)
using this:
prod_list (map i a) = prod_list (map i b) * prod_list (map i c)

goal (1 subgoal):
 1. prod_list (map i a) = prod_list (map i b) * prod_list (map i c)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
prod_list (map i a) = prod_list (map i b) * prod_list (map i c)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma measure_mono_eq_prod:
  assumes "f \<noteq> 0" "g \<noteq> 0"
  shows "mahler_measure_monic (f * g) = mahler_measure_monic f * mahler_measure_monic g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mahler_measure_monic (f * g) = mahler_measure_monic f * mahler_measure_monic g
[PROOF STEP]
unfolding mahler_measure_monic_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>a\<leftarrow>complex_roots_complex (f * g). max 1 (cmod a)) = (\<Prod>a\<leftarrow>complex_roots_complex f. max 1 (cmod a)) * (\<Prod>a\<leftarrow>complex_roots_complex g. max 1 (cmod a))
[PROOF STEP]
using mset_mult_add_2[OF complex_roots_complex_prod[OF assms],of "\<lambda> a. max 1 (cmod a)"]
[PROOF STATE]
proof (prove)
using this:
(\<Prod>a\<leftarrow>complex_roots_complex (f * g). max 1 (cmod a)) = (\<Prod>a\<leftarrow>complex_roots_complex f. max 1 (cmod a)) * (\<Prod>a\<leftarrow>complex_roots_complex g. max 1 (cmod a))

goal (1 subgoal):
 1. (\<Prod>a\<leftarrow>complex_roots_complex (f * g). max 1 (cmod a)) = (\<Prod>a\<leftarrow>complex_roots_complex f. max 1 (cmod a)) * (\<Prod>a\<leftarrow>complex_roots_complex g. max 1 (cmod a))
[PROOF STEP]
by simp


[STATEMENT]
lemma mahler_measure_poly_0[simp]: "mahler_measure_poly 0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mahler_measure_poly 0 = 0
[PROOF STEP]
unfolding mahler_measure_poly_via_monic
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod (lead_coeff 0) * mahler_measure_monic 0 = 0
[PROOF STEP]
by auto


[STATEMENT]
lemma measure_eq_prod: (* Remark 10.2 *)
  "mahler_measure_poly (f * g) = mahler_measure_poly f * mahler_measure_poly g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mahler_measure_poly (f * g) = mahler_measure_poly f * mahler_measure_poly g
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mahler_measure_poly (f * g) = mahler_measure_poly f * mahler_measure_poly g
[PROOF STEP]
consider "f = 0" | "g = 0" | (both) "f \<noteq> 0" "g \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f = 0 \<Longrightarrow> thesis; g = 0 \<Longrightarrow> thesis; \<lbrakk>f \<noteq> 0; g \<noteq> 0\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>f = 0 \<Longrightarrow> ?thesis; g = 0 \<Longrightarrow> ?thesis; \<lbrakk>f \<noteq> 0; g \<noteq> 0\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. mahler_measure_poly (f * g) = mahler_measure_poly f * mahler_measure_poly g
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>f = 0 \<Longrightarrow> ?thesis; g = 0 \<Longrightarrow> ?thesis; \<lbrakk>f \<noteq> 0; g \<noteq> 0\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. mahler_measure_poly (f * g) = mahler_measure_poly f * mahler_measure_poly g
[PROOF STEP]
proof(cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. f = 0 \<Longrightarrow> mahler_measure_poly (f * g) = mahler_measure_poly f * mahler_measure_poly g
 2. g = 0 \<Longrightarrow> mahler_measure_poly (f * g) = mahler_measure_poly f * mahler_measure_poly g
 3. \<lbrakk>f \<noteq> 0; g \<noteq> 0\<rbrakk> \<Longrightarrow> mahler_measure_poly (f * g) = mahler_measure_poly f * mahler_measure_poly g
[PROOF STEP]
case both
[PROOF STATE]
proof (state)
this:
f \<noteq> 0
g \<noteq> 0

goal (3 subgoals):
 1. f = 0 \<Longrightarrow> mahler_measure_poly (f * g) = mahler_measure_poly f * mahler_measure_poly g
 2. g = 0 \<Longrightarrow> mahler_measure_poly (f * g) = mahler_measure_poly f * mahler_measure_poly g
 3. \<lbrakk>f \<noteq> 0; g \<noteq> 0\<rbrakk> \<Longrightarrow> mahler_measure_poly (f * g) = mahler_measure_poly f * mahler_measure_poly g
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mahler_measure_poly (f * g) = mahler_measure_poly f * mahler_measure_poly g
[PROOF STEP]
unfolding mahler_measure_poly_via_monic norm_mult lead_coeff_mult
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod (lead_coeff f) * cmod (lead_coeff g) * mahler_measure_monic (f * g) = cmod (lead_coeff f) * mahler_measure_monic f * (cmod (lead_coeff g) * mahler_measure_monic g)
[PROOF STEP]
by (auto simp: measure_mono_eq_prod[OF both])
[PROOF STATE]
proof (state)
this:
mahler_measure_poly (f * g) = mahler_measure_poly f * mahler_measure_poly g

goal (2 subgoals):
 1. f = 0 \<Longrightarrow> mahler_measure_poly (f * g) = mahler_measure_poly f * mahler_measure_poly g
 2. g = 0 \<Longrightarrow> mahler_measure_poly (f * g) = mahler_measure_poly f * mahler_measure_poly g
[PROOF STEP]
qed (simp_all)
[PROOF STATE]
proof (state)
this:
mahler_measure_poly (f * g) = mahler_measure_poly f * mahler_measure_poly g

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prod_cmod[simp]:
  "cmod (\<Prod>a\<leftarrow>lst. f a) = (\<Prod>a\<leftarrow>lst. cmod (f a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod (prod_list (map f lst)) = (\<Prod>a\<leftarrow>lst. cmod (f a))
[PROOF STEP]
by(induct lst,auto simp:real_normed_div_algebra_class.norm_mult)


[STATEMENT]
lemma lead_coeff_of_prod[simp]:
  "lead_coeff (\<Prod>a\<leftarrow>lst. f a::'a::idom poly) = (\<Prod>a\<leftarrow>lst. lead_coeff (f a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lead_coeff (prod_list (map f lst)) = (\<Prod>a\<leftarrow>lst. lead_coeff (f a))
[PROOF STEP]
by(induct lst,auto simp:lead_coeff_mult)


[STATEMENT]
lemma ineq_about_squares:assumes "x \<le> (y::real)" shows "x \<le> c^2 + y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> c\<^sup>2 + y
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<le> y

goal (1 subgoal):
 1. x \<le> c\<^sup>2 + y
[PROOF STEP]
by (simp add: add.commute add_increasing2)


[STATEMENT]
lemma first_coeff_le_tail:"(cmod (lead_coeff g))^2 \<le> (\<Sum>a\<leftarrow>coeffs g. (cmod a)^2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cmod (lead_coeff g))\<^sup>2 \<le> norm2 g
[PROOF STEP]
proof(induct g)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (cmod (lead_coeff 0))\<^sup>2 \<le> norm2 0
 2. \<And>a g. \<lbrakk>a \<noteq> 0 \<or> g \<noteq> 0; (cmod (lead_coeff g))\<^sup>2 \<le> norm2 g\<rbrakk> \<Longrightarrow> (cmod (lead_coeff (pCons a g)))\<^sup>2 \<le> norm2 (pCons a g)
[PROOF STEP]
case (pCons a p)
[PROOF STATE]
proof (state)
this:
a \<noteq> 0 \<or> p \<noteq> 0
(cmod (lead_coeff p))\<^sup>2 \<le> norm2 p

goal (2 subgoals):
 1. (cmod (lead_coeff 0))\<^sup>2 \<le> norm2 0
 2. \<And>a g. \<lbrakk>a \<noteq> 0 \<or> g \<noteq> 0; (cmod (lead_coeff g))\<^sup>2 \<le> norm2 g\<rbrakk> \<Longrightarrow> (cmod (lead_coeff (pCons a g)))\<^sup>2 \<le> norm2 (pCons a g)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
a \<noteq> 0 \<or> p \<noteq> 0
(cmod (lead_coeff p))\<^sup>2 \<le> norm2 p

goal (1 subgoal):
 1. (cmod (lead_coeff (pCons a p)))\<^sup>2 \<le> norm2 (pCons a p)
[PROOF STEP]
proof(cases "p = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>a \<noteq> 0 \<or> p \<noteq> 0; (cmod (lead_coeff p))\<^sup>2 \<le> norm2 p; p = 0\<rbrakk> \<Longrightarrow> (cmod (lead_coeff (pCons a p)))\<^sup>2 \<le> norm2 (pCons a p)
 2. \<lbrakk>a \<noteq> 0 \<or> p \<noteq> 0; (cmod (lead_coeff p))\<^sup>2 \<le> norm2 p; p \<noteq> 0\<rbrakk> \<Longrightarrow> (cmod (lead_coeff (pCons a p)))\<^sup>2 \<le> norm2 (pCons a p)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
p \<noteq> 0

goal (2 subgoals):
 1. \<lbrakk>a \<noteq> 0 \<or> p \<noteq> 0; (cmod (lead_coeff p))\<^sup>2 \<le> norm2 p; p = 0\<rbrakk> \<Longrightarrow> (cmod (lead_coeff (pCons a p)))\<^sup>2 \<le> norm2 (pCons a p)
 2. \<lbrakk>a \<noteq> 0 \<or> p \<noteq> 0; (cmod (lead_coeff p))\<^sup>2 \<le> norm2 p; p \<noteq> 0\<rbrakk> \<Longrightarrow> (cmod (lead_coeff (pCons a p)))\<^sup>2 \<le> norm2 (pCons a p)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cmod (lead_coeff (pCons a p)))\<^sup>2 \<le> norm2 (pCons a p)
[PROOF STEP]
using pCons
[PROOF STATE]
proof (prove)
using this:
a \<noteq> 0 \<or> p \<noteq> 0
(cmod (lead_coeff p))\<^sup>2 \<le> norm2 p

goal (1 subgoal):
 1. (cmod (lead_coeff (pCons a p)))\<^sup>2 \<le> norm2 (pCons a p)
[PROOF STEP]
unfolding lead_coeff_pCons(1)[OF False]
[PROOF STATE]
proof (prove)
using this:
a \<noteq> 0 \<or> p \<noteq> 0
(cmod (lead_coeff p))\<^sup>2 \<le> norm2 p

goal (1 subgoal):
 1. (cmod (lead_coeff p))\<^sup>2 \<le> norm2 (pCons a p)
[PROOF STEP]
by(cases "a = 0",simp_all add:ineq_about_squares)
[PROOF STATE]
proof (state)
this:
(cmod (lead_coeff (pCons a p)))\<^sup>2 \<le> norm2 (pCons a p)

goal (1 subgoal):
 1. \<lbrakk>a \<noteq> 0 \<or> p \<noteq> 0; (cmod (lead_coeff p))\<^sup>2 \<le> norm2 p; p = 0\<rbrakk> \<Longrightarrow> (cmod (lead_coeff (pCons a p)))\<^sup>2 \<le> norm2 (pCons a p)
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
(cmod (lead_coeff (pCons a p)))\<^sup>2 \<le> norm2 (pCons a p)

goal (1 subgoal):
 1. (cmod (lead_coeff 0))\<^sup>2 \<le> norm2 0
[PROOF STEP]
qed simp


[STATEMENT]
lemma square_prod_cmod[simp]:
  "(cmod (a * b))^2 = cmod a ^ 2 * cmod b ^ 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cmod (a * b))\<^sup>2 = (cmod a)\<^sup>2 * (cmod b)\<^sup>2
[PROOF STEP]
by (simp add: norm_mult power_mult_distrib)


[STATEMENT]
lemma sum_coeffs_smult_cmod:
  "(\<Sum>a\<leftarrow>coeffs (smult v p). (cmod a)^2) = (cmod v)^2 * (\<Sum>a\<leftarrow>coeffs p. (cmod a)^2)"
  (is "?l = ?r")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm2 (Polynomial.smult v p) = (cmod v)\<^sup>2 * norm2 p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. norm2 (Polynomial.smult v p) = (cmod v)\<^sup>2 * norm2 p
[PROOF STEP]
have "?l = (\<Sum>a\<leftarrow>coeffs p. (cmod v)^2 * (cmod a)^2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm2 (Polynomial.smult v p) = (\<Sum>a\<leftarrow>coeffs p. (cmod v)\<^sup>2 * (cmod a)\<^sup>2)
[PROOF STEP]
by(cases "v=0";induct p,auto)
[PROOF STATE]
proof (state)
this:
norm2 (Polynomial.smult v p) = (\<Sum>a\<leftarrow>coeffs p. (cmod v)\<^sup>2 * (cmod a)\<^sup>2)

goal (1 subgoal):
 1. norm2 (Polynomial.smult v p) = (cmod v)\<^sup>2 * norm2 p
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
norm2 (Polynomial.smult v p) = (\<Sum>a\<leftarrow>coeffs p. (cmod v)\<^sup>2 * (cmod a)\<^sup>2)

goal (1 subgoal):
 1. norm2 (Polynomial.smult v p) = (cmod v)\<^sup>2 * norm2 p
[PROOF STEP]
by (auto simp:sum_list_const_mult)
[PROOF STATE]
proof (state)
this:
norm2 (Polynomial.smult v p) = (cmod v)\<^sup>2 * norm2 p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma coeffs_cong_1[simp]: "cCons a v = cCons b v \<longleftrightarrow> a = b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cCons a v = cCons b v) = (a = b)
[PROOF STEP]
unfolding cCons_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((if v = [] \<and> a = (0::'a) then [] else a # v) = (if v = [] \<and> b = (0::'a) then [] else b # v)) = (a = b)
[PROOF STEP]
by auto


[STATEMENT]
lemma strip_while_singleton[simp]:
  "strip_while ((=) 0) [v * a] = cCons (v * a) []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strip_while ((=) (0::'a)) [v * a] = cCons (v * a) []
[PROOF STEP]
unfolding cCons_def strip_while_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rev \<circ> dropWhile ((=) (0::'a)) \<circ> rev) [v * a] = (if [] = [] \<and> v * a = (0::'a) then [] else [v * a])
[PROOF STEP]
by auto


[STATEMENT]
lemma coeffs_times_linterm:
  shows "coeffs (pCons 0 (smult a p) + smult b p) = strip_while (HOL.eq (0::'a::{comm_ring_1}))
     (map (\<lambda>(c,d).b*d+c*a) (zip (0 # coeffs p) (coeffs p @ [0])))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coeffs (pCons (0::'a) (Polynomial.smult a p) + Polynomial.smult b p) = strip_while ((=) (0::'a)) (map2 (\<lambda>c d. b * d + c * a) ((0::'a) # coeffs p) (coeffs p @ [0::'a]))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. coeffs (pCons (0::'a) (Polynomial.smult a p) + Polynomial.smult b p) = strip_while ((=) (0::'a)) (map2 (\<lambda>c d. b * d + c * a) ((0::'a) # coeffs p) (coeffs p @ [0::'a]))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. coeffs (pCons (0::'a) (Polynomial.smult a p) + Polynomial.smult b p) = strip_while ((=) (0::'a)) (map2 (\<lambda>c d. b * d + c * a) ((0::'a) # coeffs p) (coeffs p @ [0::'a]))
[PROOF STEP]
fix v
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. coeffs (pCons (0::'a) (Polynomial.smult a p) + Polynomial.smult b p) = strip_while ((=) (0::'a)) (map2 (\<lambda>c d. b * d + c * a) ((0::'a) # coeffs p) (coeffs p @ [0::'a]))
[PROOF STEP]
have "coeffs (smult b p + pCons (a* v) (smult a p)) = strip_while (HOL.eq 0) (map (\<lambda>(c,d).b*d+c*a) (zip ([v] @ coeffs p) (coeffs p @ [0])))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coeffs (Polynomial.smult b p + pCons (a * v) (Polynomial.smult a p)) = strip_while ((=) (0::'a)) (map2 (\<lambda>c d. b * d + c * a) ([v] @ coeffs p) (coeffs p @ [0::'a]))
[PROOF STEP]
proof(induct p arbitrary:v)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>v. coeffs (Polynomial.smult b 0 + pCons (a * v) (Polynomial.smult a 0)) = strip_while ((=) (0::'a)) (map2 (\<lambda>c d. b * d + c * a) ([v] @ coeffs 0) (coeffs 0 @ [0::'a]))
 2. \<And>aa p v. \<lbrakk>aa \<noteq> (0::'a) \<or> p \<noteq> 0; \<And>v. coeffs (Polynomial.smult b p + pCons (a * v) (Polynomial.smult a p)) = strip_while ((=) (0::'a)) (map2 (\<lambda>c d. b * d + c * a) ([v] @ coeffs p) (coeffs p @ [0::'a]))\<rbrakk> \<Longrightarrow> coeffs (Polynomial.smult b (pCons aa p) + pCons (a * v) (Polynomial.smult a (pCons aa p))) = strip_while ((=) (0::'a)) (map2 (\<lambda>c d. b * d + c * a) ([v] @ coeffs (pCons aa p)) (coeffs (pCons aa p) @ [0::'a]))
[PROOF STEP]
case (pCons pa ps)
[PROOF STATE]
proof (state)
this:
pa \<noteq> (0::'a) \<or> ps \<noteq> 0
coeffs (Polynomial.smult b ps + pCons (a * ?v) (Polynomial.smult a ps)) = strip_while ((=) (0::'a)) (map2 (\<lambda>c d. b * d + c * a) ([?v] @ coeffs ps) (coeffs ps @ [0::'a]))

goal (2 subgoals):
 1. \<And>v. coeffs (Polynomial.smult b 0 + pCons (a * v) (Polynomial.smult a 0)) = strip_while ((=) (0::'a)) (map2 (\<lambda>c d. b * d + c * a) ([v] @ coeffs 0) (coeffs 0 @ [0::'a]))
 2. \<And>aa p v. \<lbrakk>aa \<noteq> (0::'a) \<or> p \<noteq> 0; \<And>v. coeffs (Polynomial.smult b p + pCons (a * v) (Polynomial.smult a p)) = strip_while ((=) (0::'a)) (map2 (\<lambda>c d. b * d + c * a) ([v] @ coeffs p) (coeffs p @ [0::'a]))\<rbrakk> \<Longrightarrow> coeffs (Polynomial.smult b (pCons aa p) + pCons (a * v) (Polynomial.smult a (pCons aa p))) = strip_while ((=) (0::'a)) (map2 (\<lambda>c d. b * d + c * a) ([v] @ coeffs (pCons aa p)) (coeffs (pCons aa p) @ [0::'a]))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
pa \<noteq> (0::'a) \<or> ps \<noteq> 0
coeffs (Polynomial.smult b ps + pCons (a * ?v) (Polynomial.smult a ps)) = strip_while ((=) (0::'a)) (map2 (\<lambda>c d. b * d + c * a) ([?v] @ coeffs ps) (coeffs ps @ [0::'a]))

goal (1 subgoal):
 1. coeffs (Polynomial.smult b (pCons pa ps) + pCons (a * v) (Polynomial.smult a (pCons pa ps))) = strip_while ((=) (0::'a)) (map2 (\<lambda>c d. b * d + c * a) ([v] @ coeffs (pCons pa ps)) (coeffs (pCons pa ps) @ [0::'a]))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
coeffs (Polynomial.smult b (pCons pa ps) + pCons (a * v) (Polynomial.smult a (pCons pa ps))) = strip_while ((=) (0::'a)) (map2 (\<lambda>c d. b * d + c * a) ([v] @ coeffs (pCons pa ps)) (coeffs (pCons pa ps) @ [0::'a]))

goal (1 subgoal):
 1. \<And>v. coeffs (Polynomial.smult b 0 + pCons (a * v) (Polynomial.smult a 0)) = strip_while ((=) (0::'a)) (map2 (\<lambda>c d. b * d + c * a) ([v] @ coeffs 0) (coeffs 0 @ [0::'a]))
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
coeffs (Polynomial.smult b p + pCons (a * v) (Polynomial.smult a p)) = strip_while ((=) (0::'a)) (map2 (\<lambda>c d. b * d + c * a) ([v] @ coeffs p) (coeffs p @ [0::'a]))

goal (1 subgoal):
 1. coeffs (pCons (0::'a) (Polynomial.smult a p) + Polynomial.smult b p) = strip_while ((=) (0::'a)) (map2 (\<lambda>c d. b * d + c * a) ((0::'a) # coeffs p) (coeffs p @ [0::'a]))
[PROOF STEP]
(* just putting ;auto does not work *)
[PROOF STATE]
proof (state)
this:
coeffs (Polynomial.smult b p + pCons (a * v) (Polynomial.smult a p)) = strip_while ((=) (0::'a)) (map2 (\<lambda>c d. b * d + c * a) ([v] @ coeffs p) (coeffs p @ [0::'a]))

goal (1 subgoal):
 1. coeffs (pCons (0::'a) (Polynomial.smult a p) + Polynomial.smult b p) = strip_while ((=) (0::'a)) (map2 (\<lambda>c d. b * d + c * a) ((0::'a) # coeffs p) (coeffs p @ [0::'a]))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
coeffs (Polynomial.smult b p + pCons (a * ?v2) (Polynomial.smult a p)) = strip_while ((=) (0::'a)) (map2 (\<lambda>c d. b * d + c * a) ([?v2] @ coeffs p) (coeffs p @ [0::'a]))

goal (1 subgoal):
 1. coeffs (pCons (0::'a) (Polynomial.smult a p) + Polynomial.smult b p) = strip_while ((=) (0::'a)) (map2 (\<lambda>c d. b * d + c * a) ((0::'a) # coeffs p) (coeffs p @ [0::'a]))
[PROOF STEP]
from this[of 0]
[PROOF STATE]
proof (chain)
picking this:
coeffs (Polynomial.smult b p + pCons (a * (0::'a)) (Polynomial.smult a p)) = strip_while ((=) (0::'a)) (map2 (\<lambda>c d. b * d + c * a) ([0::'a] @ coeffs p) (coeffs p @ [0::'a]))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
coeffs (Polynomial.smult b p + pCons (a * (0::'a)) (Polynomial.smult a p)) = strip_while ((=) (0::'a)) (map2 (\<lambda>c d. b * d + c * a) ([0::'a] @ coeffs p) (coeffs p @ [0::'a]))

goal (1 subgoal):
 1. coeffs (pCons (0::'a) (Polynomial.smult a p) + Polynomial.smult b p) = strip_while ((=) (0::'a)) (map2 (\<lambda>c d. b * d + c * a) ((0::'a) # coeffs p) (coeffs p @ [0::'a]))
[PROOF STEP]
by (simp add: add.commute)
[PROOF STATE]
proof (state)
this:
coeffs (pCons (0::'a) (Polynomial.smult a p) + Polynomial.smult b p) = strip_while ((=) (0::'a)) (map2 (\<lambda>c d. b * d + c * a) ((0::'a) # coeffs p) (coeffs p @ [0::'a]))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma filter_distr_rev[simp]:
  shows "filter f (rev lst) = rev (filter f lst)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filter f (rev lst) = rev (filter f lst)
[PROOF STEP]
by(induct lst;auto)


[STATEMENT]
lemma strip_while_filter:
  shows "filter ((\<noteq>) 0) (strip_while ((=) 0) (lst::'a::zero list)) = filter ((\<noteq>) 0) lst"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filter ((\<noteq>) (0::'a)) (strip_while ((=) (0::'a)) lst) = filter ((\<noteq>) (0::'a)) lst
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. filter ((\<noteq>) (0::'a)) (strip_while ((=) (0::'a)) lst) = filter ((\<noteq>) (0::'a)) lst
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. filter ((\<noteq>) (0::'a)) (strip_while ((=) (0::'a)) lst) = filter ((\<noteq>) (0::'a)) lst
[PROOF STEP]
fix lst::"'a list"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. filter ((\<noteq>) (0::'a)) (strip_while ((=) (0::'a)) lst) = filter ((\<noteq>) (0::'a)) lst
[PROOF STEP]
have "filter ((\<noteq>) 0) (dropWhile ((=) 0) lst) = filter ((\<noteq>) 0) lst"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filter ((\<noteq>) (0::'a)) (dropWhile ((=) (0::'a)) lst) = filter ((\<noteq>) (0::'a)) lst
[PROOF STEP]
by (induct lst;auto)
[PROOF STATE]
proof (state)
this:
filter ((\<noteq>) (0::'a)) (dropWhile ((=) (0::'a)) lst) = filter ((\<noteq>) (0::'a)) lst

goal (1 subgoal):
 1. filter ((\<noteq>) (0::'a)) (strip_while ((=) (0::'a)) lst) = filter ((\<noteq>) (0::'a)) lst
[PROOF STEP]
hence "(filter ((\<noteq>) 0) (strip_while ((=) 0) (rev lst))) = filter ((\<noteq>) 0) (rev lst)"
[PROOF STATE]
proof (prove)
using this:
filter ((\<noteq>) (0::'a)) (dropWhile ((=) (0::'a)) lst) = filter ((\<noteq>) (0::'a)) lst

goal (1 subgoal):
 1. filter ((\<noteq>) (0::'a)) (strip_while ((=) (0::'a)) (rev lst)) = filter ((\<noteq>) (0::'a)) (rev lst)
[PROOF STEP]
unfolding strip_while_def
[PROOF STATE]
proof (prove)
using this:
filter ((\<noteq>) (0::'a)) (dropWhile ((=) (0::'a)) lst) = filter ((\<noteq>) (0::'a)) lst

goal (1 subgoal):
 1. filter ((\<noteq>) (0::'a)) ((rev \<circ> dropWhile ((=) (0::'a)) \<circ> rev) (rev lst)) = filter ((\<noteq>) (0::'a)) (rev lst)
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
filter ((\<noteq>) (0::'a)) (strip_while ((=) (0::'a)) (rev lst)) = filter ((\<noteq>) (0::'a)) (rev lst)

goal (1 subgoal):
 1. filter ((\<noteq>) (0::'a)) (strip_while ((=) (0::'a)) lst) = filter ((\<noteq>) (0::'a)) lst
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
filter ((\<noteq>) (0::'a)) (strip_while ((=) (0::'a)) (rev ?lsta2)) = filter ((\<noteq>) (0::'a)) (rev ?lsta2)

goal (1 subgoal):
 1. filter ((\<noteq>) (0::'a)) (strip_while ((=) (0::'a)) lst) = filter ((\<noteq>) (0::'a)) lst
[PROOF STEP]
from this[of "rev lst"]
[PROOF STATE]
proof (chain)
picking this:
filter ((\<noteq>) (0::'a)) (strip_while ((=) (0::'a)) (rev (rev lst))) = filter ((\<noteq>) (0::'a)) (rev (rev lst))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
filter ((\<noteq>) (0::'a)) (strip_while ((=) (0::'a)) (rev (rev lst))) = filter ((\<noteq>) (0::'a)) (rev (rev lst))

goal (1 subgoal):
 1. filter ((\<noteq>) (0::'a)) (strip_while ((=) (0::'a)) lst) = filter ((\<noteq>) (0::'a)) lst
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
filter ((\<noteq>) (0::'a)) (strip_while ((=) (0::'a)) lst) = filter ((\<noteq>) (0::'a)) lst

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sum_stripwhile[simp]:
  assumes "f 0 = 0"
  shows "(\<Sum>a\<leftarrow>strip_while ((=) 0) lst. f a) = (\<Sum>a\<leftarrow>lst. f a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_list (map f (strip_while ((=) (0::'b)) lst)) = sum_list (map f lst)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sum_list (map f (strip_while ((=) (0::'b)) lst)) = sum_list (map f lst)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sum_list (map f (strip_while ((=) (0::'b)) lst)) = sum_list (map f lst)
[PROOF STEP]
fix lst
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sum_list (map f (strip_while ((=) (0::'b)) lst)) = sum_list (map f lst)
[PROOF STEP]
have "(\<Sum>a\<leftarrow>filter ((\<noteq>) 0) lst. f a) = (\<Sum>a\<leftarrow>lst. f a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_list (map f (filter ((\<noteq>) (0::'b)) lst)) = sum_list (map f lst)
[PROOF STEP]
by(induct lst,auto simp:assms)
[PROOF STATE]
proof (state)
this:
sum_list (map f (filter ((\<noteq>) (0::'b)) lst)) = sum_list (map f lst)

goal (1 subgoal):
 1. sum_list (map f (strip_while ((=) (0::'b)) lst)) = sum_list (map f lst)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
sum_list (map f (filter ((\<noteq>) (0::'b)) ?lsta2)) = sum_list (map f ?lsta2)

goal (1 subgoal):
 1. sum_list (map f (strip_while ((=) (0::'b)) lst)) = sum_list (map f lst)
[PROOF STEP]
note f=this
[PROOF STATE]
proof (state)
this:
sum_list (map f (filter ((\<noteq>) (0::'b)) ?lsta2)) = sum_list (map f ?lsta2)

goal (1 subgoal):
 1. sum_list (map f (strip_while ((=) (0::'b)) lst)) = sum_list (map f lst)
[PROOF STEP]
have "sum_list (map f (filter ((\<noteq>) 0) (strip_while ((=) 0) lst)))
       = sum_list (map f (filter ((\<noteq>) 0) lst))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_list (map f (filter ((\<noteq>) (0::'b)) (strip_while ((=) (0::'b)) lst))) = sum_list (map f (filter ((\<noteq>) (0::'b)) lst))
[PROOF STEP]
using strip_while_filter[of lst]
[PROOF STATE]
proof (prove)
using this:
filter ((\<noteq>) (0::'b)) (strip_while ((=) (0::'b)) lst) = filter ((\<noteq>) (0::'b)) lst

goal (1 subgoal):
 1. sum_list (map f (filter ((\<noteq>) (0::'b)) (strip_while ((=) (0::'b)) lst))) = sum_list (map f (filter ((\<noteq>) (0::'b)) lst))
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
sum_list (map f (filter ((\<noteq>) (0::'b)) (strip_while ((=) (0::'b)) lst))) = sum_list (map f (filter ((\<noteq>) (0::'b)) lst))

goal (1 subgoal):
 1. sum_list (map f (strip_while ((=) (0::'b)) lst)) = sum_list (map f lst)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
sum_list (map f (filter ((\<noteq>) (0::'b)) (strip_while ((=) (0::'b)) lst))) = sum_list (map f (filter ((\<noteq>) (0::'b)) lst))

goal (1 subgoal):
 1. sum_list (map f (strip_while ((=) (0::'b)) lst)) = sum_list (map f lst)
[PROOF STEP]
unfolding f
[PROOF STATE]
proof (prove)
using this:
sum_list (map f (strip_while ((=) (0::'b)) lst)) = sum_list (map f lst)

goal (1 subgoal):
 1. sum_list (map f (strip_while ((=) (0::'b)) lst)) = sum_list (map f lst)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
sum_list (map f (strip_while ((=) (0::'b)) lst)) = sum_list (map f lst)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma complex_split : "Complex a b = c \<longleftrightarrow> (a = Re c \<and> b = Im c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Complex a b = c) = (a = Re c \<and> b = Im c)
[PROOF STEP]
using complex_surj
[PROOF STATE]
proof (prove)
using this:
Complex (Re ?z) (Im ?z) = ?z

goal (1 subgoal):
 1. (Complex a b = c) = (a = Re c \<and> b = Im c)
[PROOF STEP]
by auto


[STATEMENT]
lemma norm_times_const:"(\<Sum>y\<leftarrow>lst. (cmod (a * y))\<^sup>2) = (cmod a)\<^sup>2 * (\<Sum>y\<leftarrow>lst. (cmod y)\<^sup>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>y\<leftarrow>lst. (cmod (a * y))\<^sup>2) = (cmod a)\<^sup>2 * (\<Sum>y\<leftarrow>lst. (cmod y)\<^sup>2)
[PROOF STEP]
by(induct lst,auto simp:ring_distribs)


[STATEMENT]
lemma bisumTail_is_map_zip:
  "(\<Sum>x\<leftarrow>zip (v # l1) (l1 @ [0]). f x) = bisumTail (\<lambda>x y .f (x,y))  (v#l1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_list (map f (zip (v # l1) (l1 @ [0::'b]))) = bisumTail (\<lambda>x y. f (x, y)) (v # l1)
[PROOF STEP]
by(induct l1 arbitrary:v,auto)


[STATEMENT]
lemma bisum_is_map_zip:
  "(\<Sum>x\<leftarrow>zip (0 # l1) (l1 @ [0]). f x) = bisum (\<lambda>x y. f (x,y)) l1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_list (map f (zip ((0::'b) # l1) (l1 @ [0::'b]))) = bisum (\<lambda>x y. f (x, y)) l1
[PROOF STEP]
using bisumTail_is_map_zip[of f "hd l1" "tl l1"]
[PROOF STATE]
proof (prove)
using this:
sum_list (map f (zip (hd l1 # tl l1) (tl l1 @ [0::'b]))) = bisumTail (\<lambda>x y. f (x, y)) (hd l1 # tl l1)

goal (1 subgoal):
 1. sum_list (map f (zip ((0::'b) # l1) (l1 @ [0::'b]))) = bisum (\<lambda>x y. f (x, y)) l1
[PROOF STEP]
by(cases l1,auto)


[STATEMENT]
lemma map_zip_is_bisum:
  "bisum f l1 = (\<Sum>(x,y)\<leftarrow>zip (0 # l1) (l1 @ [0]). f x y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bisum f l1 = sum_list (map2 f ((0::'b) # l1) (l1 @ [0::'b]))
[PROOF STEP]
using bisum_is_map_zip[of "\<lambda>(x,y). f x y"]
[PROOF STATE]
proof (prove)
using this:
sum_list (map2 f ((0::'b) # ?l1.0) (?l1.0 @ [0::'b])) = bisum (\<lambda>x y. case (x, y) of (x, y) \<Rightarrow> f x y) ?l1.0

goal (1 subgoal):
 1. bisum f l1 = sum_list (map2 f ((0::'b) # l1) (l1 @ [0::'b]))
[PROOF STEP]
by auto


[STATEMENT]
lemma bisum_outside :
  "(bisum (\<lambda> x y. f1 x - f2 x y + f3 y) lst :: 'a :: field)
  = sum_list (map f1 lst) + f1 0 - bisum f2 lst + sum_list (map f3 lst) + f3 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bisum (\<lambda>x y. f1 x - f2 x y + f3 y) lst = sum_list (map f1 lst) + f1 (0::'b) - bisum f2 lst + sum_list (map f3 lst) + f3 (0::'b)
[PROOF STEP]
proof(cases lst)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. lst = [] \<Longrightarrow> bisum (\<lambda>x y. f1 x - f2 x y + f3 y) lst = sum_list (map f1 lst) + f1 (0::'b) - bisum f2 lst + sum_list (map f3 lst) + f3 (0::'b)
 2. \<And>a list. lst = a # list \<Longrightarrow> bisum (\<lambda>x y. f1 x - f2 x y + f3 y) lst = sum_list (map f1 lst) + f1 (0::'b) - bisum f2 lst + sum_list (map f3 lst) + f3 (0::'b)
[PROOF STEP]
case (Cons a lst)
[PROOF STATE]
proof (state)
this:
lst = a # lst

goal (2 subgoals):
 1. lst = [] \<Longrightarrow> bisum (\<lambda>x y. f1 x - f2 x y + f3 y) lst = sum_list (map f1 lst) + f1 (0::'b) - bisum f2 lst + sum_list (map f3 lst) + f3 (0::'b)
 2. \<And>a list. lst = a # list \<Longrightarrow> bisum (\<lambda>x y. f1 x - f2 x y + f3 y) lst = sum_list (map f1 lst) + f1 (0::'b) - bisum f2 lst + sum_list (map f3 lst) + f3 (0::'b)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bisum (\<lambda>x y. f1 x - f2 x y + f3 y) lst = sum_list (map f1 lst) + f1 (0::'b) - bisum f2 lst + sum_list (map f3 lst) + f3 (0::'b)
[PROOF STEP]
unfolding map_zip_is_bisum Cons
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_list (map2 (\<lambda>x y. f1 x - f2 x y + f3 y) ((0::'b) # a # lst) ((a # lst) @ [0::'b])) = sum_list (map f1 (a # lst)) + f1 (0::'b) - sum_list (map2 f2 ((0::'b) # a # lst) ((a # lst) @ [0::'b])) + sum_list (map f3 (a # lst)) + f3 (0::'b)
[PROOF STEP]
by(induct lst arbitrary:a,auto)
[PROOF STATE]
proof (state)
this:
bisum (\<lambda>x y. f1 x - f2 x y + f3 y) lst = sum_list (map f1 lst) + f1 (0::'b) - bisum f2 lst + sum_list (map f3 lst) + f3 (0::'b)

goal (1 subgoal):
 1. lst = [] \<Longrightarrow> bisum (\<lambda>x y. f1 x - f2 x y + f3 y) lst = sum_list (map f1 lst) + f1 (0::'b) - bisum f2 lst + sum_list (map f3 lst) + f3 (0::'b)
[PROOF STEP]
qed auto


[STATEMENT]
lemma Landau_lemma:
  "(\<Sum>a\<leftarrow>coeffs (\<Prod>a\<leftarrow>lst. [:- a, 1:]). (cmod a)\<^sup>2) = (\<Sum>a\<leftarrow>coeffs (\<Prod>a\<leftarrow>lst. linH a). (cmod a)\<^sup>2)"
  (is "norm2 ?l = norm2 ?r")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm2 (\<Prod>a\<leftarrow>lst. [:- a, 1:]) = norm2 (\<Prod>a\<leftarrow>lst. if 1 < cmod a then [:- 1, cnj a:] else [:- a, 1:])
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. norm2 (\<Prod>a\<leftarrow>lst. [:- a, 1:]) = norm2 (\<Prod>a\<leftarrow>lst. if 1 < cmod a then [:- 1, cnj a:] else [:- a, 1:])
[PROOF STEP]
have a:"\<And> a. (cmod a)\<^sup>2 = Re (a * cnj a) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. (cmod a)\<^sup>2 = Re (a * cnj a)
[PROOF STEP]
using complex_norm_square
[PROOF STATE]
proof (prove)
using this:
complex_of_real ((cmod ?z)\<^sup>2) = ?z * cnj ?z

goal (1 subgoal):
 1. \<And>a. (cmod a)\<^sup>2 = Re (a * cnj a)
[PROOF STEP]
unfolding complex_split complex_of_real_def
[PROOF STATE]
proof (prove)
using this:
(cmod ?z)\<^sup>2 = Re (?z * cnj ?z) \<and> 0 = Im (?z * cnj ?z)

goal (1 subgoal):
 1. \<And>a. (cmod a)\<^sup>2 = Re (a * cnj a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(cmod ?a)\<^sup>2 = Re (?a * cnj ?a)

goal (1 subgoal):
 1. norm2 (\<Prod>a\<leftarrow>lst. [:- a, 1:]) = norm2 (\<Prod>a\<leftarrow>lst. if 1 < cmod a then [:- 1, cnj a:] else [:- a, 1:])
[PROOF STEP]
have b:"\<And> x a y. (cmod (x - a * y))^2
               = (cmod x)\<^sup>2 - Re (a * y * cnj x + x * cnj (a * y)) + (cmod (a * y))^2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x a y. (cmod (x - a * y))\<^sup>2 = (cmod x)\<^sup>2 - Re (a * y * cnj x + x * cnj (a * y)) + (cmod (a * y))\<^sup>2
[PROOF STEP]
unfolding left_diff_distrib right_diff_distrib a complex_cnj_diff
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x a y. Re (x * cnj x - a * y * cnj x - (x * cnj (a * y) - a * y * cnj (a * y))) = Re (x * cnj x) - Re (a * y * cnj x + x * cnj (a * y)) + Re (a * y * cnj (a * y))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(cmod (?x - ?a * ?y))\<^sup>2 = (cmod ?x)\<^sup>2 - Re (?a * ?y * cnj ?x + ?x * cnj (?a * ?y)) + (cmod (?a * ?y))\<^sup>2

goal (1 subgoal):
 1. norm2 (\<Prod>a\<leftarrow>lst. [:- a, 1:]) = norm2 (\<Prod>a\<leftarrow>lst. if 1 < cmod a then [:- 1, cnj a:] else [:- a, 1:])
[PROOF STEP]
have c:"\<And> y a x. (cmod (cnj a * x - y))\<^sup>2
               = (cmod (a * x))\<^sup>2 - Re (a * y * cnj x + x * cnj (a * y)) + (cmod y)^2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y a x. (cmod (cnj a * x - y))\<^sup>2 = (cmod (a * x))\<^sup>2 - Re (a * y * cnj x + x * cnj (a * y)) + (cmod y)\<^sup>2
[PROOF STEP]
unfolding left_diff_distrib right_diff_distrib a complex_cnj_diff
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y a x. Re (cnj a * x * cnj (cnj a * x) - y * cnj (cnj a * x) - (cnj a * x * cnj y - y * cnj y)) = Re (a * x * cnj (a * x)) - Re (a * y * cnj x + x * cnj (a * y)) + Re (y * cnj y)
[PROOF STEP]
by (simp add: mult.assoc mult.left_commute)
[PROOF STATE]
proof (state)
this:
(cmod (cnj ?a * ?x - ?y))\<^sup>2 = (cmod (?a * ?x))\<^sup>2 - Re (?a * ?y * cnj ?x + ?x * cnj (?a * ?y)) + (cmod ?y)\<^sup>2

goal (1 subgoal):
 1. norm2 (\<Prod>a\<leftarrow>lst. [:- a, 1:]) = norm2 (\<Prod>a\<leftarrow>lst. if 1 < cmod a then [:- 1, cnj a:] else [:- a, 1:])
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
(cmod (cnj ?a * ?x - ?y))\<^sup>2 = (cmod (?a * ?x))\<^sup>2 - Re (?a * ?y * cnj ?x + ?x * cnj (?a * ?y)) + (cmod ?y)\<^sup>2

goal (1 subgoal):
 1. norm2 (\<Prod>a\<leftarrow>lst. [:- a, 1:]) = norm2 (\<Prod>a\<leftarrow>lst. if 1 < cmod a then [:- 1, cnj a:] else [:- a, 1:])
[PROOF STEP]
fix f1 a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. norm2 (\<Prod>a\<leftarrow>lst. [:- a, 1:]) = norm2 (\<Prod>a\<leftarrow>lst. if 1 < cmod a then [:- 1, cnj a:] else [:- a, 1:])
[PROOF STEP]
have "norm2 ([:- a, 1 :] * f1) = bisum (\<lambda>x y. cmod (x - a * y)^2) (coeffs f1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm2 ([:- a, 1:] * f1) = bisum (\<lambda>x y. (cmod (x - a * y))\<^sup>2) (coeffs f1)
[PROOF STEP]
by(simp add: bisum_is_map_zip[of _ "coeffs f1"] coeffs_times_linterm[of 1 _ "-a",simplified])
[PROOF STATE]
proof (state)
this:
norm2 ([:- a, 1:] * f1) = bisum (\<lambda>x y. (cmod (x - a * y))\<^sup>2) (coeffs f1)

goal (1 subgoal):
 1. norm2 (\<Prod>a\<leftarrow>lst. [:- a, 1:]) = norm2 (\<Prod>a\<leftarrow>lst. if 1 < cmod a then [:- 1, cnj a:] else [:- a, 1:])
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
norm2 ([:- a, 1:] * f1) = bisum (\<lambda>x y. (cmod (x - a * y))\<^sup>2) (coeffs f1)

goal (1 subgoal):
 1. norm2 (\<Prod>a\<leftarrow>lst. [:- a, 1:]) = norm2 (\<Prod>a\<leftarrow>lst. if 1 < cmod a then [:- 1, cnj a:] else [:- a, 1:])
[PROOF STEP]
have "\<dots> = norm2 f1 + cmod a^2*norm2 f1
                  - bisum (\<lambda>x y. Re (a * y * cnj x + x * cnj (a * y))) (coeffs f1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bisum (\<lambda>x y. (cmod (x - a * y))\<^sup>2) (coeffs f1) = norm2 f1 + (cmod a)\<^sup>2 * norm2 f1 - bisum (\<lambda>x y. Re (a * y * cnj x + x * cnj (a * y))) (coeffs f1)
[PROOF STEP]
unfolding b bisum_outside norm_times_const
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm2 f1 + (cmod 0)\<^sup>2 - bisum (\<lambda>x y. Re (a * y * cnj x + x * cnj (a * y))) (coeffs f1) + (cmod a)\<^sup>2 * norm2 f1 + (cmod (a * 0))\<^sup>2 = norm2 f1 + (cmod a)\<^sup>2 * norm2 f1 - bisum (\<lambda>x y. Re (a * y * cnj x + x * cnj (a * y))) (coeffs f1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
bisum (\<lambda>x y. (cmod (x - a * y))\<^sup>2) (coeffs f1) = norm2 f1 + (cmod a)\<^sup>2 * norm2 f1 - bisum (\<lambda>x y. Re (a * y * cnj x + x * cnj (a * y))) (coeffs f1)

goal (1 subgoal):
 1. norm2 (\<Prod>a\<leftarrow>lst. [:- a, 1:]) = norm2 (\<Prod>a\<leftarrow>lst. if 1 < cmod a then [:- 1, cnj a:] else [:- a, 1:])
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
bisum (\<lambda>x y. (cmod (x - a * y))\<^sup>2) (coeffs f1) = norm2 f1 + (cmod a)\<^sup>2 * norm2 f1 - bisum (\<lambda>x y. Re (a * y * cnj x + x * cnj (a * y))) (coeffs f1)

goal (1 subgoal):
 1. norm2 (\<Prod>a\<leftarrow>lst. [:- a, 1:]) = norm2 (\<Prod>a\<leftarrow>lst. if 1 < cmod a then [:- 1, cnj a:] else [:- a, 1:])
[PROOF STEP]
have "\<dots> = bisum (\<lambda>x y. cmod (cnj a * x - y)^2) (coeffs f1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm2 f1 + (cmod a)\<^sup>2 * norm2 f1 - bisum (\<lambda>x y. Re (a * y * cnj x + x * cnj (a * y))) (coeffs f1) = bisum (\<lambda>x y. (cmod (cnj a * x - y))\<^sup>2) (coeffs f1)
[PROOF STEP]
unfolding c bisum_outside norm_times_const
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm2 f1 + (cmod a)\<^sup>2 * norm2 f1 - bisum (\<lambda>x y. Re (a * y * cnj x + x * cnj (a * y))) (coeffs f1) = (cmod a)\<^sup>2 * norm2 f1 + (cmod (a * 0))\<^sup>2 - bisum (\<lambda>x y. Re (a * y * cnj x + x * cnj (a * y))) (coeffs f1) + norm2 f1 + (cmod 0)\<^sup>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
norm2 f1 + (cmod a)\<^sup>2 * norm2 f1 - bisum (\<lambda>x y. Re (a * y * cnj x + x * cnj (a * y))) (coeffs f1) = bisum (\<lambda>x y. (cmod (cnj a * x - y))\<^sup>2) (coeffs f1)

goal (1 subgoal):
 1. norm2 (\<Prod>a\<leftarrow>lst. [:- a, 1:]) = norm2 (\<Prod>a\<leftarrow>lst. if 1 < cmod a then [:- 1, cnj a:] else [:- a, 1:])
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
norm2 f1 + (cmod a)\<^sup>2 * norm2 f1 - bisum (\<lambda>x y. Re (a * y * cnj x + x * cnj (a * y))) (coeffs f1) = bisum (\<lambda>x y. (cmod (cnj a * x - y))\<^sup>2) (coeffs f1)

goal (1 subgoal):
 1. norm2 (\<Prod>a\<leftarrow>lst. [:- a, 1:]) = norm2 (\<Prod>a\<leftarrow>lst. if 1 < cmod a then [:- 1, cnj a:] else [:- a, 1:])
[PROOF STEP]
have "\<dots> = norm2 ([:- 1, cnj a :] * f1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bisum (\<lambda>x y. (cmod (cnj a * x - y))\<^sup>2) (coeffs f1) = norm2 ([:- 1, cnj a:] * f1)
[PROOF STEP]
using coeffs_times_linterm[of "cnj a" _ "-1"]
[PROOF STATE]
proof (prove)
using this:
coeffs (pCons 0 (Polynomial.smult (cnj a) ?p) + Polynomial.smult (- 1) ?p) = strip_while ((=) 0) (map2 (\<lambda>c d. - 1 * d + c * cnj a) (0 # coeffs ?p) (coeffs ?p @ [0]))

goal (1 subgoal):
 1. bisum (\<lambda>x y. (cmod (cnj a * x - y))\<^sup>2) (coeffs f1) = norm2 ([:- 1, cnj a:] * f1)
[PROOF STEP]
by(simp add: bisum_is_map_zip[of _ "coeffs f1"] mult.commute)
[PROOF STATE]
proof (state)
this:
bisum (\<lambda>x y. (cmod (cnj a * x - y))\<^sup>2) (coeffs f1) = norm2 ([:- 1, cnj a:] * f1)

goal (1 subgoal):
 1. norm2 (\<Prod>a\<leftarrow>lst. [:- a, 1:]) = norm2 (\<Prod>a\<leftarrow>lst. if 1 < cmod a then [:- 1, cnj a:] else [:- a, 1:])
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
norm2 ([:- a, 1:] * f1) = norm2 ([:- 1, cnj a:] * f1)
[PROOF STEP]
have "norm2 ([:- a, 1 :] * f1) = \<dots>"
[PROOF STATE]
proof (prove)
using this:
norm2 ([:- a, 1:] * f1) = norm2 ([:- 1, cnj a:] * f1)

goal (1 subgoal):
 1. norm2 ([:- a, 1:] * f1) = norm2 ([:- 1, cnj a:] * f1)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
norm2 ([:- a, 1:] * f1) = norm2 ([:- 1, cnj a:] * f1)

goal (1 subgoal):
 1. norm2 (\<Prod>a\<leftarrow>lst. [:- a, 1:]) = norm2 (\<Prod>a\<leftarrow>lst. if 1 < cmod a then [:- 1, cnj a:] else [:- a, 1:])
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
norm2 ([:- ?a2, 1:] * ?f1.2) = norm2 ([:- 1, cnj ?a2:] * ?f1.2)

goal (1 subgoal):
 1. norm2 (\<Prod>a\<leftarrow>lst. [:- a, 1:]) = norm2 (\<Prod>a\<leftarrow>lst. if 1 < cmod a then [:- 1, cnj a:] else [:- a, 1:])
[PROOF STEP]
hence h:"\<And> a f1. norm2 ([:- a, 1 :] * f1) = norm2 (linH a * f1)"
[PROOF STATE]
proof (prove)
using this:
norm2 ([:- ?a2, 1:] * ?f1.2) = norm2 ([:- 1, cnj ?a2:] * ?f1.2)

goal (1 subgoal):
 1. \<And>a f1. norm2 ([:- a, 1:] * f1) = norm2 ((if 1 < cmod a then [:- 1, cnj a:] else [:- a, 1:]) * f1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
norm2 ([:- ?a, 1:] * ?f1.0) = norm2 ((if 1 < cmod ?a then [:- 1, cnj ?a:] else [:- ?a, 1:]) * ?f1.0)

goal (1 subgoal):
 1. norm2 (\<Prod>a\<leftarrow>lst. [:- a, 1:]) = norm2 (\<Prod>a\<leftarrow>lst. if 1 < cmod a then [:- 1, cnj a:] else [:- a, 1:])
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm2 (\<Prod>a\<leftarrow>lst. [:- a, 1:]) = norm2 (\<Prod>a\<leftarrow>lst. if 1 < cmod a then [:- 1, cnj a:] else [:- a, 1:])
[PROOF STEP]
by(rule prod_induct_gen[OF h])
[PROOF STATE]
proof (state)
this:
norm2 (\<Prod>a\<leftarrow>lst. [:- a, 1:]) = norm2 (\<Prod>a\<leftarrow>lst. if 1 < cmod a then [:- 1, cnj a:] else [:- a, 1:])

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Landau_inequality:
  "mahler_measure_poly f \<le> l2norm_complex f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mahler_measure_poly f \<le> l2norm_complex f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mahler_measure_poly f \<le> l2norm_complex f
[PROOF STEP]
let ?f = "reconstruct_poly (lead_coeff f) (complex_roots_complex f)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mahler_measure_poly f \<le> l2norm_complex f
[PROOF STEP]
let ?roots = "(complex_roots_complex f)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mahler_measure_poly f \<le> l2norm_complex f
[PROOF STEP]
let ?g = "\<Prod>a\<leftarrow>?roots. linH a"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mahler_measure_poly f \<le> l2norm_complex f
[PROOF STEP]
(* g is chosen such that lead_coeff_g holds, and its l2 norm is equal to f's l2 norm *)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mahler_measure_poly f \<le> l2norm_complex f
[PROOF STEP]
have max:"\<And>a. cmod (if 1 < cmod a then cnj a else 1) = max 1 (cmod a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. cmod (if 1 < cmod a then cnj a else 1) = max 1 (cmod a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cmod (if 1 < cmod ?a then cnj ?a else 1) = max 1 (cmod ?a)

goal (1 subgoal):
 1. mahler_measure_poly f \<le> l2norm_complex f
[PROOF STEP]
have "\<And>a. 1 < cmod a \<Longrightarrow> a \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. 1 < cmod a \<Longrightarrow> a \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
1 < cmod ?a \<Longrightarrow> ?a \<noteq> 0

goal (1 subgoal):
 1. mahler_measure_poly f \<le> l2norm_complex f
[PROOF STEP]
hence "\<And>a. lead_coeff (linH a) = (if (cmod a > 1) then cnj a else 1)"
[PROOF STATE]
proof (prove)
using this:
1 < cmod ?a \<Longrightarrow> ?a \<noteq> 0

goal (1 subgoal):
 1. \<And>a. lead_coeff (if 1 < cmod a then [:- 1, cnj a:] else [:- a, 1:]) = (if 1 < cmod a then cnj a else 1)
[PROOF STEP]
by(auto simp:if_split)
[PROOF STATE]
proof (state)
this:
lead_coeff (if 1 < cmod ?a then [:- 1, cnj ?a:] else [:- ?a, 1:]) = (if 1 < cmod ?a then cnj ?a else 1)

goal (1 subgoal):
 1. mahler_measure_poly f \<le> l2norm_complex f
[PROOF STEP]
hence lead_coeff_g:"cmod (lead_coeff ?g) = (\<Prod>a\<leftarrow>?roots. max 1 (cmod a))"
[PROOF STATE]
proof (prove)
using this:
lead_coeff (if 1 < cmod ?a then [:- 1, cnj ?a:] else [:- ?a, 1:]) = (if 1 < cmod ?a then cnj ?a else 1)

goal (1 subgoal):
 1. cmod (lead_coeff (\<Prod>a\<leftarrow>complex_roots_complex f. if 1 < cmod a then [:- 1, cnj a:] else [:- a, 1:])) = (\<Prod>a\<leftarrow>complex_roots_complex f. max 1 (cmod a))
[PROOF STEP]
by(auto simp:max)
[PROOF STATE]
proof (state)
this:
cmod (lead_coeff (\<Prod>a\<leftarrow>complex_roots_complex f. if 1 < cmod a then [:- 1, cnj a:] else [:- a, 1:])) = (\<Prod>a\<leftarrow>complex_roots_complex f. max 1 (cmod a))

goal (1 subgoal):
 1. mahler_measure_poly f \<le> l2norm_complex f
[PROOF STEP]
have "norm2 f = (\<Sum>a\<leftarrow>coeffs ?f. (cmod a)^2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm2 f = norm2 (reconstruct_poly (lead_coeff f) (complex_roots_complex f))
[PROOF STEP]
unfolding reconstruct_is_original_poly
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm2 f = norm2 f
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
norm2 f = norm2 (reconstruct_poly (lead_coeff f) (complex_roots_complex f))

goal (1 subgoal):
 1. mahler_measure_poly f \<le> l2norm_complex f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
norm2 f = norm2 (reconstruct_poly (lead_coeff f) (complex_roots_complex f))

goal (1 subgoal):
 1. mahler_measure_poly f \<le> l2norm_complex f
[PROOF STEP]
have "\<dots> = cmod (lead_coeff f)^2 * (\<Sum>a\<leftarrow>coeffs (\<Prod>a\<leftarrow>?roots. [:- a, 1:]). (cmod a)\<^sup>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm2 (reconstruct_poly (lead_coeff f) (complex_roots_complex f)) = (cmod (lead_coeff f))\<^sup>2 * norm2 (\<Prod>a\<leftarrow>complex_roots_complex f. [:- a, 1:])
[PROOF STEP]
unfolding reconstruct_poly_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm2 (Polynomial.smult (lead_coeff f) (\<Prod>a\<leftarrow>complex_roots_complex f. [:- a, 1:])) = (cmod (lead_coeff f))\<^sup>2 * norm2 (\<Prod>a\<leftarrow>complex_roots_complex f. [:- a, 1:])
[PROOF STEP]
using sum_coeffs_smult_cmod
[PROOF STATE]
proof (prove)
using this:
norm2 (Polynomial.smult ?v ?p) = (cmod ?v)\<^sup>2 * norm2 ?p

goal (1 subgoal):
 1. norm2 (Polynomial.smult (lead_coeff f) (\<Prod>a\<leftarrow>complex_roots_complex f. [:- a, 1:])) = (cmod (lead_coeff f))\<^sup>2 * norm2 (\<Prod>a\<leftarrow>complex_roots_complex f. [:- a, 1:])
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
norm2 (reconstruct_poly (lead_coeff f) (complex_roots_complex f)) = (cmod (lead_coeff f))\<^sup>2 * norm2 (\<Prod>a\<leftarrow>complex_roots_complex f. [:- a, 1:])

goal (1 subgoal):
 1. mahler_measure_poly f \<le> l2norm_complex f
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
norm2 f = (cmod (lead_coeff f))\<^sup>2 * norm2 (\<Prod>a\<leftarrow>complex_roots_complex f. [:- a, 1:])
[PROOF STEP]
have fg_norm:"norm2 f = cmod (lead_coeff f)^2 * (\<Sum>a\<leftarrow>coeffs ?g. (cmod a)^2)"
[PROOF STATE]
proof (prove)
using this:
norm2 f = (cmod (lead_coeff f))\<^sup>2 * norm2 (\<Prod>a\<leftarrow>complex_roots_complex f. [:- a, 1:])

goal (1 subgoal):
 1. norm2 f = (cmod (lead_coeff f))\<^sup>2 * norm2 (\<Prod>a\<leftarrow>complex_roots_complex f. if 1 < cmod a then [:- 1, cnj a:] else [:- a, 1:])
[PROOF STEP]
unfolding Landau_lemma
[PROOF STATE]
proof (prove)
using this:
norm2 f = (cmod (lead_coeff f))\<^sup>2 * norm2 (\<Prod>a\<leftarrow>complex_roots_complex f. if 1 < cmod a then [:- 1, cnj a:] else [:- a, 1:])

goal (1 subgoal):
 1. norm2 f = (cmod (lead_coeff f))\<^sup>2 * norm2 (\<Prod>a\<leftarrow>complex_roots_complex f. if 1 < cmod a then [:- 1, cnj a:] else [:- a, 1:])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
norm2 f = (cmod (lead_coeff f))\<^sup>2 * norm2 (\<Prod>a\<leftarrow>complex_roots_complex f. if 1 < cmod a then [:- 1, cnj a:] else [:- a, 1:])

goal (1 subgoal):
 1. mahler_measure_poly f \<le> l2norm_complex f
[PROOF STEP]
have "(cmod (lead_coeff ?g))^2 \<le> (\<Sum>a\<leftarrow>coeffs ?g. (cmod a)^2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cmod (lead_coeff (\<Prod>a\<leftarrow>complex_roots_complex f. if 1 < cmod a then [:- 1, cnj a:] else [:- a, 1:])))\<^sup>2 \<le> norm2 (\<Prod>a\<leftarrow>complex_roots_complex f. if 1 < cmod a then [:- 1, cnj a:] else [:- a, 1:])
[PROOF STEP]
using first_coeff_le_tail
[PROOF STATE]
proof (prove)
using this:
(cmod (lead_coeff ?g))\<^sup>2 \<le> norm2 ?g

goal (1 subgoal):
 1. (cmod (lead_coeff (\<Prod>a\<leftarrow>complex_roots_complex f. if 1 < cmod a then [:- 1, cnj a:] else [:- a, 1:])))\<^sup>2 \<le> norm2 (\<Prod>a\<leftarrow>complex_roots_complex f. if 1 < cmod a then [:- 1, cnj a:] else [:- a, 1:])
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(cmod (lead_coeff (\<Prod>a\<leftarrow>complex_roots_complex f. if 1 < cmod a then [:- 1, cnj a:] else [:- a, 1:])))\<^sup>2 \<le> norm2 (\<Prod>a\<leftarrow>complex_roots_complex f. if 1 < cmod a then [:- 1, cnj a:] else [:- a, 1:])

goal (1 subgoal):
 1. mahler_measure_poly f \<le> l2norm_complex f
[PROOF STEP]
from ordered_comm_semiring_class.comm_mult_left_mono[OF this]
[PROOF STATE]
proof (chain)
picking this:
0 \<le> ?c \<Longrightarrow> ?c * (cmod (lead_coeff (\<Prod>a\<leftarrow>complex_roots_complex f. if 1 < cmod a then [:- 1, cnj a:] else [:- a, 1:])))\<^sup>2 \<le> ?c * norm2 (\<Prod>a\<leftarrow>complex_roots_complex f. if 1 < cmod a then [:- 1, cnj a:] else [:- a, 1:])
[PROOF STEP]
have "(cmod (lead_coeff f) * cmod (lead_coeff ?g))^2 \<le> (\<Sum>a\<leftarrow>coeffs f. (cmod a)^2)"
[PROOF STATE]
proof (prove)
using this:
0 \<le> ?c \<Longrightarrow> ?c * (cmod (lead_coeff (\<Prod>a\<leftarrow>complex_roots_complex f. if 1 < cmod a then [:- 1, cnj a:] else [:- a, 1:])))\<^sup>2 \<le> ?c * norm2 (\<Prod>a\<leftarrow>complex_roots_complex f. if 1 < cmod a then [:- 1, cnj a:] else [:- a, 1:])

goal (1 subgoal):
 1. (cmod (lead_coeff f) * cmod (lead_coeff (\<Prod>a\<leftarrow>complex_roots_complex f. if 1 < cmod a then [:- 1, cnj a:] else [:- a, 1:])))\<^sup>2 \<le> norm2 f
[PROOF STEP]
unfolding fg_norm
[PROOF STATE]
proof (prove)
using this:
0 \<le> ?c \<Longrightarrow> ?c * (cmod (lead_coeff (\<Prod>a\<leftarrow>complex_roots_complex f. if 1 < cmod a then [:- 1, cnj a:] else [:- a, 1:])))\<^sup>2 \<le> ?c * norm2 (\<Prod>a\<leftarrow>complex_roots_complex f. if 1 < cmod a then [:- 1, cnj a:] else [:- a, 1:])

goal (1 subgoal):
 1. (cmod (lead_coeff f) * cmod (lead_coeff (\<Prod>a\<leftarrow>complex_roots_complex f. if 1 < cmod a then [:- 1, cnj a:] else [:- a, 1:])))\<^sup>2 \<le> (cmod (lead_coeff f))\<^sup>2 * norm2 (\<Prod>a\<leftarrow>complex_roots_complex f. if 1 < cmod a then [:- 1, cnj a:] else [:- a, 1:])
[PROOF STEP]
by (simp add:power_mult_distrib)
[PROOF STATE]
proof (state)
this:
(cmod (lead_coeff f) * cmod (lead_coeff (\<Prod>a\<leftarrow>complex_roots_complex f. if 1 < cmod a then [:- 1, cnj a:] else [:- a, 1:])))\<^sup>2 \<le> norm2 f

goal (1 subgoal):
 1. mahler_measure_poly f \<le> l2norm_complex f
[PROOF STEP]
hence "cmod (lead_coeff f) * (\<Prod>a\<leftarrow>?roots. max 1 (cmod a)) \<le> sqrt (norm2 f)"
[PROOF STATE]
proof (prove)
using this:
(cmod (lead_coeff f) * cmod (lead_coeff (\<Prod>a\<leftarrow>complex_roots_complex f. if 1 < cmod a then [:- 1, cnj a:] else [:- a, 1:])))\<^sup>2 \<le> norm2 f

goal (1 subgoal):
 1. cmod (lead_coeff f) * (\<Prod>a\<leftarrow>complex_roots_complex f. max 1 (cmod a)) \<le> l2norm_complex f
[PROOF STEP]
using NthRoot.real_le_rsqrt lead_coeff_g
[PROOF STATE]
proof (prove)
using this:
(cmod (lead_coeff f) * cmod (lead_coeff (\<Prod>a\<leftarrow>complex_roots_complex f. if 1 < cmod a then [:- 1, cnj a:] else [:- a, 1:])))\<^sup>2 \<le> norm2 f
?x\<^sup>2 \<le> ?y \<Longrightarrow> ?x \<le> sqrt ?y
cmod (lead_coeff (\<Prod>a\<leftarrow>complex_roots_complex f. if 1 < cmod a then [:- 1, cnj a:] else [:- a, 1:])) = (\<Prod>a\<leftarrow>complex_roots_complex f. max 1 (cmod a))

goal (1 subgoal):
 1. cmod (lead_coeff f) * (\<Prod>a\<leftarrow>complex_roots_complex f. max 1 (cmod a)) \<le> l2norm_complex f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cmod (lead_coeff f) * (\<Prod>a\<leftarrow>complex_roots_complex f. max 1 (cmod a)) \<le> l2norm_complex f

goal (1 subgoal):
 1. mahler_measure_poly f \<le> l2norm_complex f
[PROOF STEP]
thus "mahler_measure_poly f \<le> sqrt (norm2 f)"
[PROOF STATE]
proof (prove)
using this:
cmod (lead_coeff f) * (\<Prod>a\<leftarrow>complex_roots_complex f. max 1 (cmod a)) \<le> l2norm_complex f

goal (1 subgoal):
 1. mahler_measure_poly f \<le> l2norm_complex f
[PROOF STEP]
using reconstruct_with_type_conversion[unfolded complex_roots_int_def]
[PROOF STATE]
proof (prove)
using this:
cmod (lead_coeff f) * (\<Prod>a\<leftarrow>complex_roots_complex f. max 1 (cmod a)) \<le> l2norm_complex f
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_poly f \<le> l2norm_complex f
[PROOF STEP]
by (simp add: mahler_measure_poly_via_monic mahler_measure_monic_def complex_roots_int_def)
[PROOF STATE]
proof (state)
this:
mahler_measure_poly f \<le> l2norm_complex f

goal:
No subgoals!
[PROOF STEP]
qed