[STATEMENT]
lemma \<Delta>\<Phi>_pass2: "hs \<noteq> [] \<Longrightarrow> no_Emptys hs \<Longrightarrow>
  \<Phi> (pass\<^sub>2 hs) - \<Phi>_hps hs \<le> log 2 (size_hps hs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>hs \<noteq> []; no_Emptys hs\<rbrakk> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs) - \<Phi>_hps hs \<le> log 2 (real (size_hps hs))
[PROOF STEP]
proof (induction hs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>[] \<noteq> []; no_Emptys []\<rbrakk> \<Longrightarrow> \<Phi> (pass\<^sub>2 []) - \<Phi>_hps [] \<le> log 2 (real (size_hps []))
 2. \<And>a hs. \<lbrakk>\<lbrakk>hs \<noteq> []; no_Emptys hs\<rbrakk> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs) - \<Phi>_hps hs \<le> log 2 (real (size_hps hs)); a # hs \<noteq> []; no_Emptys (a # hs)\<rbrakk> \<Longrightarrow> \<Phi> (pass\<^sub>2 (a # hs)) - \<Phi>_hps (a # hs) \<le> log 2 (real (size_hps (a # hs)))
[PROOF STEP]
case (Cons h hs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>hs \<noteq> []; no_Emptys hs\<rbrakk> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs) - \<Phi>_hps hs \<le> log 2 (real (size_hps hs))
h # hs \<noteq> []
no_Emptys (h # hs)

goal (2 subgoals):
 1. \<lbrakk>[] \<noteq> []; no_Emptys []\<rbrakk> \<Longrightarrow> \<Phi> (pass\<^sub>2 []) - \<Phi>_hps [] \<le> log 2 (real (size_hps []))
 2. \<And>a hs. \<lbrakk>\<lbrakk>hs \<noteq> []; no_Emptys hs\<rbrakk> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs) - \<Phi>_hps hs \<le> log 2 (real (size_hps hs)); a # hs \<noteq> []; no_Emptys (a # hs)\<rbrakk> \<Longrightarrow> \<Phi> (pass\<^sub>2 (a # hs)) - \<Phi>_hps (a # hs) \<le> log 2 (real (size_hps (a # hs)))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>hs \<noteq> []; no_Emptys hs\<rbrakk> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs) - \<Phi>_hps hs \<le> log 2 (real (size_hps hs))
h # hs \<noteq> []
no_Emptys (h # hs)

goal (1 subgoal):
 1. \<Phi> (pass\<^sub>2 (h # hs)) - \<Phi>_hps (h # hs) \<le> log 2 (real (size_hps (h # hs)))
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>hs \<noteq> []; no_Emptys hs\<rbrakk> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs) - \<Phi>_hps hs \<le> log 2 (real (size_hps hs)); h # hs \<noteq> []; no_Emptys (h # hs); ?P3\<rbrakk> \<Longrightarrow> \<Phi> (pass\<^sub>2 (h # hs)) - \<Phi>_hps (h # hs) \<le> log 2 (real (size_hps (h # hs)))
 2. \<lbrakk>\<lbrakk>hs \<noteq> []; no_Emptys hs\<rbrakk> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs) - \<Phi>_hps hs \<le> log 2 (real (size_hps hs)); h # hs \<noteq> []; no_Emptys (h # hs); \<not> ?P3\<rbrakk> \<Longrightarrow> \<Phi> (pass\<^sub>2 (h # hs)) - \<Phi>_hps (h # hs) \<le> log 2 (real (size_hps (h # hs)))
[PROOF STEP]
assume "hs = []"
[PROOF STATE]
proof (state)
this:
hs = []

goal (2 subgoals):
 1. \<lbrakk>\<lbrakk>hs \<noteq> []; no_Emptys hs\<rbrakk> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs) - \<Phi>_hps hs \<le> log 2 (real (size_hps hs)); h # hs \<noteq> []; no_Emptys (h # hs); ?P3\<rbrakk> \<Longrightarrow> \<Phi> (pass\<^sub>2 (h # hs)) - \<Phi>_hps (h # hs) \<le> log 2 (real (size_hps (h # hs)))
 2. \<lbrakk>\<lbrakk>hs \<noteq> []; no_Emptys hs\<rbrakk> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs) - \<Phi>_hps hs \<le> log 2 (real (size_hps hs)); h # hs \<noteq> []; no_Emptys (h # hs); \<not> ?P3\<rbrakk> \<Longrightarrow> \<Phi> (pass\<^sub>2 (h # hs)) - \<Phi>_hps (h # hs) \<le> log 2 (real (size_hps (h # hs)))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
hs = []

goal (1 subgoal):
 1. \<Phi> (pass\<^sub>2 (h # hs)) - \<Phi>_hps (h # hs) \<le> log 2 (real (size_hps (h # hs)))
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
hs = []
\<lbrakk>hs \<noteq> []; no_Emptys hs\<rbrakk> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs) - \<Phi>_hps hs \<le> log 2 (real (size_hps hs))
h # hs \<noteq> []
no_Emptys (h # hs)

goal (1 subgoal):
 1. \<Phi> (pass\<^sub>2 (h # hs)) - \<Phi>_hps (h # hs) \<le> log 2 (real (size_hps (h # hs)))
[PROOF STEP]
by (auto simp add: \<Phi>_hps1 dest: no_Empty_ge0)
[PROOF STATE]
proof (state)
this:
\<Phi> (pass\<^sub>2 (h # hs)) - \<Phi>_hps (h # hs) \<le> log 2 (real (size_hps (h # hs)))

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>hs \<noteq> []; no_Emptys hs\<rbrakk> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs) - \<Phi>_hps hs \<le> log 2 (real (size_hps hs)); h # hs \<noteq> []; no_Emptys (h # hs); hs \<noteq> []\<rbrakk> \<Longrightarrow> \<Phi> (pass\<^sub>2 (h # hs)) - \<Phi>_hps (h # hs) \<le> log 2 (real (size_hps (h # hs)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>hs \<noteq> []; no_Emptys hs\<rbrakk> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs) - \<Phi>_hps hs \<le> log 2 (real (size_hps hs)); h # hs \<noteq> []; no_Emptys (h # hs); hs \<noteq> []\<rbrakk> \<Longrightarrow> \<Phi> (pass\<^sub>2 (h # hs)) - \<Phi>_hps (h # hs) \<le> log 2 (real (size_hps (h # hs)))
[PROOF STEP]
assume *: "hs \<noteq> []"
[PROOF STATE]
proof (state)
this:
hs \<noteq> []

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>hs \<noteq> []; no_Emptys hs\<rbrakk> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs) - \<Phi>_hps hs \<le> log 2 (real (size_hps hs)); h # hs \<noteq> []; no_Emptys (h # hs); hs \<noteq> []\<rbrakk> \<Longrightarrow> \<Phi> (pass\<^sub>2 (h # hs)) - \<Phi>_hps (h # hs) \<le> log 2 (real (size_hps (h # hs)))
[PROOF STEP]
obtain x hs2 where [simp]: "h = Hp x hs2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x hs2. h = Hp x hs2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using Cons.prems(2)
[PROOF STATE]
proof (prove)
using this:
no_Emptys (h # hs)

goal (1 subgoal):
 1. (\<And>x hs2. h = Hp x hs2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by simp (meson no_Empty.elims(2))
[PROOF STATE]
proof (state)
this:
h = Hp x hs2

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>hs \<noteq> []; no_Emptys hs\<rbrakk> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs) - \<Phi>_hps hs \<le> log 2 (real (size_hps hs)); h # hs \<noteq> []; no_Emptys (h # hs); hs \<noteq> []\<rbrakk> \<Longrightarrow> \<Phi> (pass\<^sub>2 (h # hs)) - \<Phi>_hps (h # hs) \<le> log 2 (real (size_hps (h # hs)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Phi> (pass\<^sub>2 (h # hs)) - \<Phi>_hps (h # hs) \<le> log 2 (real (size_hps (h # hs)))
[PROOF STEP]
proof (cases "pass\<^sub>2 hs")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. pass\<^sub>2 hs = heap.Empty \<Longrightarrow> \<Phi> (pass\<^sub>2 (h # hs)) - \<Phi>_hps (h # hs) \<le> log 2 (real (size_hps (h # hs)))
 2. \<And>x21 x22. pass\<^sub>2 hs = Hp x21 x22 \<Longrightarrow> \<Phi> (pass\<^sub>2 (h # hs)) - \<Phi>_hps (h # hs) \<le> log 2 (real (size_hps (h # hs)))
[PROOF STEP]
case Empty
[PROOF STATE]
proof (state)
this:
pass\<^sub>2 hs = heap.Empty

goal (2 subgoals):
 1. pass\<^sub>2 hs = heap.Empty \<Longrightarrow> \<Phi> (pass\<^sub>2 (h # hs)) - \<Phi>_hps (h # hs) \<le> log 2 (real (size_hps (h # hs)))
 2. \<And>x21 x22. pass\<^sub>2 hs = Hp x21 x22 \<Longrightarrow> \<Phi> (pass\<^sub>2 (h # hs)) - \<Phi>_hps (h # hs) \<le> log 2 (real (size_hps (h # hs)))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
pass\<^sub>2 hs = heap.Empty

goal (1 subgoal):
 1. \<Phi> (pass\<^sub>2 (h # hs)) - \<Phi>_hps (h # hs) \<le> log 2 (real (size_hps (h # hs)))
[PROOF STEP]
using \<Phi>_hps_ge0[of hs]
[PROOF STATE]
proof (prove)
using this:
pass\<^sub>2 hs = heap.Empty
0 \<le> \<Phi>_hps hs

goal (1 subgoal):
 1. \<Phi> (pass\<^sub>2 (h # hs)) - \<Phi>_hps (h # hs) \<le> log 2 (real (size_hps (h # hs)))
[PROOF STEP]
by(simp add: add_increasing xt1(3)[OF mult_2, OF add_increasing])
[PROOF STATE]
proof (state)
this:
\<Phi> (pass\<^sub>2 (h # hs)) - \<Phi>_hps (h # hs) \<le> log 2 (real (size_hps (h # hs)))

goal (1 subgoal):
 1. \<And>x21 x22. pass\<^sub>2 hs = Hp x21 x22 \<Longrightarrow> \<Phi> (pass\<^sub>2 (h # hs)) - \<Phi>_hps (h # hs) \<le> log 2 (real (size_hps (h # hs)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x21 x22. pass\<^sub>2 hs = Hp x21 x22 \<Longrightarrow> \<Phi> (pass\<^sub>2 (h # hs)) - \<Phi>_hps (h # hs) \<le> log 2 (real (size_hps (h # hs)))
[PROOF STEP]
case (Hp y hs3)
[PROOF STATE]
proof (state)
this:
pass\<^sub>2 hs = Hp y hs3

goal (1 subgoal):
 1. \<And>x21 x22. pass\<^sub>2 hs = Hp x21 x22 \<Longrightarrow> \<Phi> (pass\<^sub>2 (h # hs)) - \<Phi>_hps (h # hs) \<le> log 2 (real (size_hps (h # hs)))
[PROOF STEP]
with Cons * size_hps_pass2[of hs]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>hs \<noteq> []; no_Emptys hs\<rbrakk> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs) - \<Phi>_hps hs \<le> log 2 (real (size_hps hs))
h # hs \<noteq> []
no_Emptys (h # hs)
hs \<noteq> []
\<lbrakk>hs \<noteq> []; no_Emptys hs\<rbrakk> \<Longrightarrow> no_Empty (pass\<^sub>2 hs) \<and> size_hps hs = size_hps (hps (pass\<^sub>2 hs)) + 1
pass\<^sub>2 hs = Hp y hs3
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>hs \<noteq> []; no_Emptys hs\<rbrakk> \<Longrightarrow> \<Phi> (pass\<^sub>2 hs) - \<Phi>_hps hs \<le> log 2 (real (size_hps hs))
h # hs \<noteq> []
no_Emptys (h # hs)
hs \<noteq> []
\<lbrakk>hs \<noteq> []; no_Emptys hs\<rbrakk> \<Longrightarrow> no_Empty (pass\<^sub>2 hs) \<and> size_hps hs = size_hps (hps (pass\<^sub>2 hs)) + 1
pass\<^sub>2 hs = Hp y hs3

goal (1 subgoal):
 1. \<Phi> (pass\<^sub>2 (h # hs)) - \<Phi>_hps (h # hs) \<le> log 2 (real (size_hps (h # hs)))
[PROOF STEP]
by(auto simp: add_mono)
[PROOF STATE]
proof (state)
this:
\<Phi> (pass\<^sub>2 (h # hs)) - \<Phi>_hps (h # hs) \<le> log 2 (real (size_hps (h # hs)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Phi> (pass\<^sub>2 (h # hs)) - \<Phi>_hps (h # hs) \<le> log 2 (real (size_hps (h # hs)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Phi> (pass\<^sub>2 (h # hs)) - \<Phi>_hps (h # hs) \<le> log 2 (real (size_hps (h # hs)))

goal (1 subgoal):
 1. \<lbrakk>[] \<noteq> []; no_Emptys []\<rbrakk> \<Longrightarrow> \<Phi> (pass\<^sub>2 []) - \<Phi>_hps [] \<le> log 2 (real (size_hps []))
[PROOF STEP]
qed simp


[STATEMENT]
lemma \<Delta>\<Phi>_del_min: assumes "hps h \<noteq> []" "no_Empty h"
  shows "\<Phi> (del_min h) - \<Phi> h
  \<le> 3 * log 2 (size_hps(hps h)) - length(hps h) + 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Phi> (del_min h) - \<Phi> h \<le> 3 * log 2 (real (size_hps (hps h))) - real (length (hps h)) + 2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Phi> (del_min h) - \<Phi> h \<le> 3 * log 2 (real (size_hps (hps h))) - real (length (hps h)) + 2
[PROOF STEP]
obtain x hs where [simp]: "h = Hp x hs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x hs. h = Hp x hs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
no_Empty h

goal (1 subgoal):
 1. (\<And>x hs. h = Hp x hs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases h) auto
[PROOF STATE]
proof (state)
this:
h = Hp x hs

goal (1 subgoal):
 1. \<Phi> (del_min h) - \<Phi> h \<le> 3 * log 2 (real (size_hps (hps h))) - real (length (hps h)) + 2
[PROOF STEP]
let ?\<Delta>\<Phi>\<^sub>1 = "\<Phi>_hps(hps h) - \<Phi> h"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Phi> (del_min h) - \<Phi> h \<le> 3 * log 2 (real (size_hps (hps h))) - real (length (hps h)) + 2
[PROOF STEP]
let ?\<Delta>\<Phi>\<^sub>2 = "\<Phi>(pass\<^sub>2(pass\<^sub>1 (hps h))) - \<Phi>_hps (hps h)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Phi> (del_min h) - \<Phi> h \<le> 3 * log 2 (real (size_hps (hps h))) - real (length (hps h)) + 2
[PROOF STEP]
let ?\<Delta>\<Phi> = "\<Phi> (del_min h) - \<Phi> h"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Phi> (del_min h) - \<Phi> h \<le> 3 * log 2 (real (size_hps (hps h))) - real (length (hps h)) + 2
[PROOF STEP]
have "\<Phi>(pass\<^sub>2(pass\<^sub>1(hps h))) - \<Phi>_hps (pass\<^sub>1(hps h)) \<le> log 2 (size_hps(hps h))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Phi> (pass\<^sub>2 (pass\<^sub>1 (hps h))) - \<Phi>_hps (pass\<^sub>1 (hps h)) \<le> log 2 (real (size_hps (hps h)))
[PROOF STEP]
using \<Delta>\<Phi>_pass2[of "pass\<^sub>1(hps h)"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>pass\<^sub>1 (hps h) \<noteq> []; no_Emptys (pass\<^sub>1 (hps h))\<rbrakk> \<Longrightarrow> \<Phi> (pass\<^sub>2 (pass\<^sub>1 (hps h))) - \<Phi>_hps (pass\<^sub>1 (hps h)) \<le> log 2 (real (size_hps (pass\<^sub>1 (hps h))))

goal (1 subgoal):
 1. \<Phi> (pass\<^sub>2 (pass\<^sub>1 (hps h))) - \<Phi>_hps (pass\<^sub>1 (hps h)) \<le> log 2 (real (size_hps (hps h)))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>pass\<^sub>1 (hps h) \<noteq> []; no_Emptys (pass\<^sub>1 (hps h))\<rbrakk> \<Longrightarrow> \<Phi> (pass\<^sub>2 (pass\<^sub>1 (hps h))) - \<Phi>_hps (pass\<^sub>1 (hps h)) \<le> log 2 (real (size_hps (pass\<^sub>1 (hps h))))
hps h \<noteq> []
no_Empty h

goal (1 subgoal):
 1. \<Phi> (pass\<^sub>2 (pass\<^sub>1 (hps h))) - \<Phi>_hps (pass\<^sub>1 (hps h)) \<le> log 2 (real (size_hps (hps h)))
[PROOF STEP]
by (auto simp: pass1_Nil_iff no_Emptys_pass1 dest: no_Emptys_hps)
[PROOF STATE]
proof (state)
this:
\<Phi> (pass\<^sub>2 (pass\<^sub>1 (hps h))) - \<Phi>_hps (pass\<^sub>1 (hps h)) \<le> log 2 (real (size_hps (hps h)))

goal (1 subgoal):
 1. \<Phi> (del_min h) - \<Phi> h \<le> 3 * log 2 (real (size_hps (hps h))) - real (length (hps h)) + 2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Phi> (pass\<^sub>2 (pass\<^sub>1 (hps h))) - \<Phi>_hps (pass\<^sub>1 (hps h)) \<le> log 2 (real (size_hps (hps h)))

goal (1 subgoal):
 1. \<Phi> (del_min h) - \<Phi> h \<le> 3 * log 2 (real (size_hps (hps h))) - real (length (hps h)) + 2
[PROOF STEP]
have "\<Phi>_hps (pass\<^sub>1 (hps h)) - \<Phi>_hps (hps h) \<le>  2*\<dots> - length (hps h) + 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Phi>_hps (pass\<^sub>1 (hps h)) - \<Phi>_hps (hps h) \<le> 2 * log 2 (real (size_hps (hps h))) - real (length (hps h)) + 2
[PROOF STEP]
using \<Delta>\<Phi>_pass1[OF assms(1) no_Emptys_hps[OF assms(2)]]
[PROOF STATE]
proof (prove)
using this:
\<Phi>_hps (pass\<^sub>1 (hps h)) - \<Phi>_hps (hps h) \<le> 2 * log 2 (real (size_hps (hps h))) - real (length (hps h)) + 2

goal (1 subgoal):
 1. \<Phi>_hps (pass\<^sub>1 (hps h)) - \<Phi>_hps (hps h) \<le> 2 * log 2 (real (size_hps (hps h))) - real (length (hps h)) + 2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<Phi>_hps (pass\<^sub>1 (hps h)) - \<Phi>_hps (hps h) \<le> 2 * log 2 (real (size_hps (hps h))) - real (length (hps h)) + 2

goal (1 subgoal):
 1. \<Phi> (del_min h) - \<Phi> h \<le> 3 * log 2 (real (size_hps (hps h))) - real (length (hps h)) + 2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Phi>_hps (pass\<^sub>1 (hps h)) - \<Phi>_hps (hps h) \<le> 2 * log 2 (real (size_hps (hps h))) - real (length (hps h)) + 2

goal (1 subgoal):
 1. \<Phi> (del_min h) - \<Phi> h \<le> 3 * log 2 (real (size_hps (hps h))) - real (length (hps h)) + 2
[PROOF STEP]
have "?\<Delta>\<Phi>\<^sub>1 \<le> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Phi>_hps (hps h) - \<Phi> h \<le> 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Phi>_hps (hps h) - \<Phi> h \<le> 0

goal (1 subgoal):
 1. \<Phi> (del_min h) - \<Phi> h \<le> 3 * log 2 (real (size_hps (hps h))) - real (length (hps h)) + 2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Phi>_hps (hps h) - \<Phi> h \<le> 0

goal (1 subgoal):
 1. \<Phi> (del_min h) - \<Phi> h \<le> 3 * log 2 (real (size_hps (hps h))) - real (length (hps h)) + 2
[PROOF STEP]
have "?\<Delta>\<Phi> = ?\<Delta>\<Phi>\<^sub>1 + ?\<Delta>\<Phi>\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Phi> (del_min h) - \<Phi> h = \<Phi>_hps (hps h) - \<Phi> h + (\<Phi> (pass\<^sub>2 (pass\<^sub>1 (hps h))) - \<Phi>_hps (hps h))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Phi> (del_min h) - \<Phi> h = \<Phi>_hps (hps h) - \<Phi> h + (\<Phi> (pass\<^sub>2 (pass\<^sub>1 (hps h))) - \<Phi>_hps (hps h))

goal (1 subgoal):
 1. \<Phi> (del_min h) - \<Phi> h \<le> 3 * log 2 (real (size_hps (hps h))) - real (length (hps h)) + 2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Phi> (pass\<^sub>2 (pass\<^sub>1 (hps h))) - \<Phi>_hps (pass\<^sub>1 (hps h)) \<le> log 2 (real (size_hps (hps h)))
\<Phi>_hps (pass\<^sub>1 (hps h)) - \<Phi>_hps (hps h) \<le> 2 * log 2 (real (size_hps (hps h))) - real (length (hps h)) + 2
\<Phi>_hps (hps h) - \<Phi> h \<le> 0
\<Phi> (del_min h) - \<Phi> h = \<Phi>_hps (hps h) - \<Phi> h + (\<Phi> (pass\<^sub>2 (pass\<^sub>1 (hps h))) - \<Phi>_hps (hps h))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Phi> (pass\<^sub>2 (pass\<^sub>1 (hps h))) - \<Phi>_hps (pass\<^sub>1 (hps h)) \<le> log 2 (real (size_hps (hps h)))
\<Phi>_hps (pass\<^sub>1 (hps h)) - \<Phi>_hps (hps h) \<le> 2 * log 2 (real (size_hps (hps h))) - real (length (hps h)) + 2
\<Phi>_hps (hps h) - \<Phi> h \<le> 0
\<Phi> (del_min h) - \<Phi> h = \<Phi>_hps (hps h) - \<Phi> h + (\<Phi> (pass\<^sub>2 (pass\<^sub>1 (hps h))) - \<Phi>_hps (hps h))

goal (1 subgoal):
 1. \<Phi> (del_min h) - \<Phi> h \<le> 3 * log 2 (real (size_hps (hps h))) - real (length (hps h)) + 2
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
\<Phi> (del_min h) - \<Phi> h \<le> 3 * log 2 (real (size_hps (hps h))) - real (length (hps h)) + 2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma PPc_nonempt: "PPc c \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. PPc c \<noteq> []
[PROOF STEP]
by (induct c) auto


[STATEMENT]
lemma unique_c_uneq: "set (PPc c) \<inter> set (PPc c') = {} \<Longrightarrow> c \<noteq> c'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (PPc c) \<inter> set (PPc c') = {} \<Longrightarrow> c \<noteq> c'
[PROOF STEP]
by (insert PPc_nonempt, force)


[STATEMENT]
lemma V_nonempt_PPV_nonempt: "V \<noteq> [] \<Longrightarrow> PPV V \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V \<noteq> [] \<Longrightarrow> PPV V \<noteq> []
[PROOF STEP]
by (auto, induct V, simp_all, insert PPc_nonempt, force)


[STATEMENT]
lemma unique_V_uneq:
"\<lbrakk>V \<noteq> []; V' \<noteq> []; set (PPV V) \<inter> set (PPV V') = {}\<rbrakk> \<Longrightarrow> V \<noteq> V'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>V \<noteq> []; V' \<noteq> []; set (PPV V) \<inter> set (PPV V') = {}\<rbrakk> \<Longrightarrow> V \<noteq> V'
[PROOF STEP]
by (auto, induct V, simp_all, insert V_nonempt_PPV_nonempt, auto)


[STATEMENT]
lemma PPc_in_PPV: "c \<in> set V \<Longrightarrow> set (PPc c) \<subseteq> set (PPV V)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c \<in> set V \<Longrightarrow> set (PPc c) \<subseteq> set (PPV V)
[PROOF STEP]
by (induct V, auto)


[STATEMENT]
lemma listindices_aux: "i < length V \<Longrightarrow> (V!i) \<in> set V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < length V \<Longrightarrow> V ! i \<in> set V
[PROOF STEP]
by (metis nth_mem)


[STATEMENT]
lemma PPc_in_PPV_version:
  "i < length V \<Longrightarrow> set (PPc (V!i)) \<subseteq> set (PPV V)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < length V \<Longrightarrow> set (PPc (V ! i)) \<subseteq> set (PPV V)
[PROOF STEP]
by (rule PPc_in_PPV, erule listindices_aux)


[STATEMENT]
lemma uniPPV_uniPPc: "unique_PPV V \<Longrightarrow> (\<forall>i < length V. unique_PPc (V!i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unique_PPV V \<Longrightarrow> \<forall>i<length V. unique_PPc (V ! i)
[PROOF STEP]
by (auto, simp add: unique_PPV_def, induct V,
    auto simp add: unique_PPc_def,
    metis in_set_conv_nth length_Suc_conv set_ConsD)

\<comment> \<open>SEMANTICS\<close>


[STATEMENT]
lemma nextmem_exists_and_unique:
"\<exists>m' p \<alpha>. \<langle>c,m\<rangle> \<rightarrow>\<lhd>\<alpha>\<rhd> \<langle>p,m'\<rangle>
  \<and> (\<forall>m''. (\<exists>p \<alpha>. \<langle>c,m\<rangle> \<rightarrow>\<lhd>\<alpha>\<rhd> \<langle>p,m''\<rangle>) \<longrightarrow> m'' = m')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>m' p \<alpha>. \<langle>c,m\<rangle> \<rightarrow>\<lhd>\<alpha>\<rhd> \<langle>p,m'\<rangle> \<and> (\<forall>m''. (\<exists>p \<alpha>. \<langle>c,m\<rangle> \<rightarrow>\<lhd>\<alpha>\<rhd> \<langle>p,m''\<rangle>) \<longrightarrow> m'' = m')
[PROOF STEP]
by (induct c, auto, metis MWLsSteps_det.skip MWLsSteps_det_cases(1),
    metis MWLsSteps_det_cases(2) MWLsSteps_det.assign,
    metis (no_types) MWLsSteps_det.seq1 MWLsSteps_det.seq2
    MWLsSteps_det_cases(3) not_Some_eq,
    metis MWLsSteps_det.iffalse MWLsSteps_det.iftrue
    MWLsSteps_det_cases(4),
    metis MWLsSteps_det.whilefalse MWLsSteps_det.whiletrue
    MWLsSteps_det_cases(5),
    metis MWLsSteps_det.spawn MWLsSteps_det_cases(6))


[STATEMENT]
lemma PPsc_of_step:
"\<lbrakk> \<langle>c,m\<rangle> \<rightarrow>\<lhd>\<alpha>\<rhd> \<langle>p,m'\<rangle>; \<exists>c'. p = Some c' \<rbrakk>
  \<Longrightarrow> set (PPc (the p)) \<subseteq> set (PPc c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<langle>c,m\<rangle> \<rightarrow>\<lhd>\<alpha>\<rhd> \<langle>p,m'\<rangle>; \<exists>c'. p = Some c'\<rbrakk> \<Longrightarrow> set (PPc (the p)) \<subseteq> set (PPc c)
[PROOF STEP]
by (induct rule: MWLsSteps_det.induct, auto)


[STATEMENT]
lemma PPs\<alpha>_of_step:
"\<langle>c,m\<rangle> \<rightarrow>\<lhd>\<alpha>\<rhd> \<langle>p,m'\<rangle>
  \<Longrightarrow> set (PPV \<alpha>) \<subseteq> set (PPc c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>c,m\<rangle> \<rightarrow>\<lhd>\<alpha>\<rhd> \<langle>p,m'\<rangle> \<Longrightarrow> set (PPV \<alpha>) \<subseteq> set (PPc c)
[PROOF STEP]
by (induct rule: MWLsSteps_det.induct, auto)


[STATEMENT]
lemma (in domain) finprod_zero_iff:
  assumes "finite A"
  assumes "\<And>a. a \<in> A \<Longrightarrow> f a \<in> carrier R"
  shows "finprod R f A = \<zero> \<longleftrightarrow> (\<exists>x \<in> A. f x = \<zero>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (finprod R f A = \<zero>) = (\<exists>x\<in>A. f x = \<zero>)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite A
?a \<in> A \<Longrightarrow> f ?a \<in> carrier R

goal (1 subgoal):
 1. (finprod R f A = \<zero>) = (\<exists>x\<in>A. f x = \<zero>)
[PROOF STEP]
proof (induct A rule: finite_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<And>a. a \<in> {} \<Longrightarrow> f a \<in> carrier R) \<Longrightarrow> (finprod R f {} = \<zero>) = (\<exists>x\<in>{}. f x = \<zero>)
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; (\<And>a. a \<in> F \<Longrightarrow> f a \<in> carrier R) \<Longrightarrow> (finprod R f F = \<zero>) = (\<exists>x\<in>F. f x = \<zero>); \<And>a. a \<in> insert x F \<Longrightarrow> f a \<in> carrier R\<rbrakk> \<Longrightarrow> (finprod R f (insert x F) = \<zero>) = (\<exists>x\<in>insert x F. f x = \<zero>)
[PROOF STEP]
case empty
[PROOF STATE]
proof (state)
this:
?a \<in> {} \<Longrightarrow> f ?a \<in> carrier R

goal (2 subgoals):
 1. (\<And>a. a \<in> {} \<Longrightarrow> f a \<in> carrier R) \<Longrightarrow> (finprod R f {} = \<zero>) = (\<exists>x\<in>{}. f x = \<zero>)
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; (\<And>a. a \<in> F \<Longrightarrow> f a \<in> carrier R) \<Longrightarrow> (finprod R f F = \<zero>) = (\<exists>x\<in>F. f x = \<zero>); \<And>a. a \<in> insert x F \<Longrightarrow> f a \<in> carrier R\<rbrakk> \<Longrightarrow> (finprod R f (insert x F) = \<zero>) = (\<exists>x\<in>insert x F. f x = \<zero>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?a \<in> {} \<Longrightarrow> f ?a \<in> carrier R
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
?a \<in> {} \<Longrightarrow> f ?a \<in> carrier R

goal (1 subgoal):
 1. (finprod R f {} = \<zero>) = (\<exists>x\<in>{}. f x = \<zero>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(finprod R f {} = \<zero>) = (\<exists>x\<in>{}. f x = \<zero>)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; (\<And>a. a \<in> F \<Longrightarrow> f a \<in> carrier R) \<Longrightarrow> (finprod R f F = \<zero>) = (\<exists>x\<in>F. f x = \<zero>); \<And>a. a \<in> insert x F \<Longrightarrow> f a \<in> carrier R\<rbrakk> \<Longrightarrow> (finprod R f (insert x F) = \<zero>) = (\<exists>x\<in>insert x F. f x = \<zero>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; (\<And>a. a \<in> F \<Longrightarrow> f a \<in> carrier R) \<Longrightarrow> (finprod R f F = \<zero>) = (\<exists>x\<in>F. f x = \<zero>); \<And>a. a \<in> insert x F \<Longrightarrow> f a \<in> carrier R\<rbrakk> \<Longrightarrow> (finprod R f (insert x F) = \<zero>) = (\<exists>x\<in>insert x F. f x = \<zero>)
[PROOF STEP]
case (insert y F)
[PROOF STATE]
proof (state)
this:
finite F
y \<notin> F
(\<And>a. a \<in> F \<Longrightarrow> f a \<in> carrier R) \<Longrightarrow> (finprod R f F = \<zero>) = (\<exists>x\<in>F. f x = \<zero>)
?a \<in> insert y F \<Longrightarrow> f ?a \<in> carrier R

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; (\<And>a. a \<in> F \<Longrightarrow> f a \<in> carrier R) \<Longrightarrow> (finprod R f F = \<zero>) = (\<exists>x\<in>F. f x = \<zero>); \<And>a. a \<in> insert x F \<Longrightarrow> f a \<in> carrier R\<rbrakk> \<Longrightarrow> (finprod R f (insert x F) = \<zero>) = (\<exists>x\<in>insert x F. f x = \<zero>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite F
y \<notin> F
(\<And>a. a \<in> F \<Longrightarrow> f a \<in> carrier R) \<Longrightarrow> (finprod R f F = \<zero>) = (\<exists>x\<in>F. f x = \<zero>)
?a \<in> insert y F \<Longrightarrow> f ?a \<in> carrier R

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; (\<And>a. a \<in> F \<Longrightarrow> f a \<in> carrier R) \<Longrightarrow> (finprod R f F = \<zero>) = (\<exists>x\<in>F. f x = \<zero>); \<And>a. a \<in> insert x F \<Longrightarrow> f a \<in> carrier R\<rbrakk> \<Longrightarrow> (finprod R f (insert x F) = \<zero>) = (\<exists>x\<in>insert x F. f x = \<zero>)
[PROOF STEP]
have "f \<in> F \<rightarrow> carrier R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> F \<rightarrow> carrier R
[PROOF STEP]
using insert
[PROOF STATE]
proof (prove)
using this:
finite F
y \<notin> F
(\<And>a. a \<in> F \<Longrightarrow> f a \<in> carrier R) \<Longrightarrow> (finprod R f F = \<zero>) = (\<exists>x\<in>F. f x = \<zero>)
?a \<in> insert y F \<Longrightarrow> f ?a \<in> carrier R

goal (1 subgoal):
 1. f \<in> F \<rightarrow> carrier R
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f \<in> F \<rightarrow> carrier R

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; (\<And>a. a \<in> F \<Longrightarrow> f a \<in> carrier R) \<Longrightarrow> (finprod R f F = \<zero>) = (\<exists>x\<in>F. f x = \<zero>); \<And>a. a \<in> insert x F \<Longrightarrow> f a \<in> carrier R\<rbrakk> \<Longrightarrow> (finprod R f (insert x F) = \<zero>) = (\<exists>x\<in>insert x F. f x = \<zero>)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
finite F
y \<notin> F
(\<And>a. a \<in> F \<Longrightarrow> f a \<in> carrier R) \<Longrightarrow> (finprod R f F = \<zero>) = (\<exists>x\<in>F. f x = \<zero>)
?a \<in> insert y F \<Longrightarrow> f ?a \<in> carrier R
f \<in> F \<rightarrow> carrier R
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
finite F
y \<notin> F
(\<And>a. a \<in> F \<Longrightarrow> f a \<in> carrier R) \<Longrightarrow> (finprod R f F = \<zero>) = (\<exists>x\<in>F. f x = \<zero>)
?a \<in> insert y F \<Longrightarrow> f ?a \<in> carrier R
f \<in> F \<rightarrow> carrier R

goal (1 subgoal):
 1. (finprod R f (insert y F) = \<zero>) = (\<exists>x\<in>insert y F. f x = \<zero>)
[PROOF STEP]
by (simp add:integral_iff)
[PROOF STATE]
proof (state)
this:
(finprod R f (insert y F) = \<zero>) = (\<exists>x\<in>insert y F. f x = \<zero>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in ring) poly_of_const_in_carrier:
  assumes "s \<in> carrier R"
  shows "poly_of_const s \<in> carrier (poly_ring R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly_of_const s \<in> carrier (poly_ring R)
[PROOF STEP]
using poly_of_const_def assms
[PROOF STATE]
proof (prove)
using this:
poly_of_const = (\<lambda>k. local.normalize [k])
s \<in> carrier R

goal (1 subgoal):
 1. poly_of_const s \<in> carrier (poly_ring R)
[PROOF STEP]
by (simp add:univ_poly_carrier[symmetric] polynomial_def)


[STATEMENT]
lemma (in ring) eval_poly_of_const:
  assumes "x \<in> carrier R"
  shows "eval (poly_of_const x) y = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.eval (poly_of_const x) y = x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in> carrier R

goal (1 subgoal):
 1. local.eval (poly_of_const x) y = x
[PROOF STEP]
by (simp add:poly_of_const_def)


[STATEMENT]
lemma (in ring) eval_in_carrier_2:
  assumes "x \<in> carrier (poly_ring R)"
  assumes "y \<in> carrier R"
  shows "eval x y \<in> carrier R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.eval x y \<in> carrier R
[PROOF STEP]
using eval_in_carrier univ_poly_carrier polynomial_incl assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>set ?p \<subseteq> carrier R; ?x \<in> carrier R\<rbrakk> \<Longrightarrow> local.eval ?p ?x \<in> carrier R
polynomial\<^bsub>?R\<^esub> ?K ?p = (?p \<in> carrier (?K [X]\<^bsub>?R\<^esub>))
polynomial ?K ?p \<Longrightarrow> set ?p \<subseteq> ?K
x \<in> carrier (poly_ring R)
y \<in> carrier R

goal (1 subgoal):
 1. local.eval x y \<in> carrier R
[PROOF STEP]
by blast


[STATEMENT]
lemma (in domain) poly_mult_degree_le_1:
  assumes "x \<in> carrier (poly_ring R)"
  assumes "y \<in> carrier (poly_ring R)"
  shows "degree (x \<otimes>\<^bsub>poly_ring R\<^esub> y) \<le> degree x + degree y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (x \<otimes>\<^bsub>poly_ring R\<^esub> y) \<le> degree x + degree y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. degree (x \<otimes>\<^bsub>poly_ring R\<^esub> y) \<le> degree x + degree y
[PROOF STEP]
have "degree (x \<otimes>\<^bsub>poly_ring R\<^esub> y) = (if x = [] \<or> y = [] then 0 else degree x + degree y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (x \<otimes>\<^bsub>poly_ring R\<^esub> y) = (if x = [] \<or> y = [] then 0 else degree x + degree y)
[PROOF STEP]
unfolding univ_poly_mult
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (poly_mult x y) = (if x = [] \<or> y = [] then 0 else degree x + degree y)
[PROOF STEP]
by (metis univ_poly_carrier assms(1,2) carrier_is_subring poly_mult_degree_eq)
[PROOF STATE]
proof (state)
this:
degree (x \<otimes>\<^bsub>poly_ring R\<^esub> y) = (if x = [] \<or> y = [] then 0 else degree x + degree y)

goal (1 subgoal):
 1. degree (x \<otimes>\<^bsub>poly_ring R\<^esub> y) \<le> degree x + degree y
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
degree (x \<otimes>\<^bsub>poly_ring R\<^esub> y) = (if x = [] \<or> y = [] then 0 else degree x + degree y)

goal (1 subgoal):
 1. degree (x \<otimes>\<^bsub>poly_ring R\<^esub> y) \<le> degree x + degree y
[PROOF STEP]
by (metis nat_le_linear zero_le)
[PROOF STATE]
proof (state)
this:
degree (x \<otimes>\<^bsub>poly_ring R\<^esub> y) \<le> degree x + degree y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in domain) poly_mult_degree_le:
  assumes "x \<in> carrier (poly_ring R)"
  assumes "y \<in> carrier (poly_ring R)"
  assumes "degree x \<le> n"
  assumes "degree y \<le> m"
  shows "degree (x \<otimes>\<^bsub>poly_ring R\<^esub> y) \<le> n + m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (x \<otimes>\<^bsub>poly_ring R\<^esub> y) \<le> n + m
[PROOF STEP]
using poly_mult_degree_le_1 assms add_mono
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> carrier (poly_ring R); ?y \<in> carrier (poly_ring R)\<rbrakk> \<Longrightarrow> degree (?x \<otimes>\<^bsub>poly_ring R\<^esub> ?y) \<le> degree ?x + degree ?y
x \<in> carrier (poly_ring R)
y \<in> carrier (poly_ring R)
degree x \<le> n
degree y \<le> m
\<lbrakk>?a \<le> ?b; ?c \<le> ?d\<rbrakk> \<Longrightarrow> ?a + ?c \<le> ?b + ?d

goal (1 subgoal):
 1. degree (x \<otimes>\<^bsub>poly_ring R\<^esub> y) \<le> n + m
[PROOF STEP]
by force


[STATEMENT]
lemma (in domain) poly_add_degree_le:
  assumes "x \<in> carrier (poly_ring R)" "degree x \<le> n"
  assumes "y \<in> carrier (poly_ring R)" "degree y \<le> n"
  shows "degree (x \<oplus>\<^bsub>poly_ring R\<^esub> y) \<le> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (x \<oplus>\<^bsub>poly_ring R\<^esub> y) \<le> n
[PROOF STEP]
using assms poly_add_degree
[PROOF STATE]
proof (prove)
using this:
x \<in> carrier (poly_ring R)
degree x \<le> n
y \<in> carrier (poly_ring R)
degree y \<le> n
degree (poly_add ?p1.0 ?p2.0) \<le> max (degree ?p1.0) (degree ?p2.0)

goal (1 subgoal):
 1. degree (x \<oplus>\<^bsub>poly_ring R\<^esub> y) \<le> n
[PROOF STEP]
by (metis dual_order.trans max.bounded_iff univ_poly_add)


[STATEMENT]
lemma (in domain) poly_sub_degree_le:
  assumes "x \<in> carrier (poly_ring R)" "degree x \<le> n"
  assumes "y \<in> carrier (poly_ring R)" "degree y \<le> n"
  shows "degree (x \<ominus>\<^bsub>poly_ring R\<^esub> y) \<le> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (x \<ominus>\<^bsub>poly_ring R\<^esub> y) \<le> n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. degree (x \<ominus>\<^bsub>poly_ring R\<^esub> y) \<le> n
[PROOF STEP]
interpret x:cring "poly_ring R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cring (poly_ring R)
[PROOF STEP]
using carrier_is_subring domain.univ_poly_is_cring domain_axioms
[PROOF STATE]
proof (prove)
using this:
subring (carrier R) R
\<lbrakk>domain ?R; subring ?K ?R\<rbrakk> \<Longrightarrow> cring (?K [X]\<^bsub>?R\<^esub>)
domain R

goal (1 subgoal):
 1. cring (poly_ring R)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. degree (x \<ominus>\<^bsub>poly_ring R\<^esub> y) \<le> n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (x \<ominus>\<^bsub>poly_ring R\<^esub> y) \<le> n
[PROOF STEP]
unfolding a_minus_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (x \<oplus>\<^bsub>poly_ring R\<^esub> \<ominus>\<^bsub>poly_ring R\<^esub> y) \<le> n
[PROOF STEP]
using assms univ_poly_a_inv_degree carrier_is_subring poly_add_degree_le x.a_inv_closed
[PROOF STATE]
proof (prove)
using this:
x \<in> carrier (poly_ring R)
degree x \<le> n
y \<in> carrier (poly_ring R)
degree y \<le> n
\<lbrakk>subring ?K R; ?p \<in> carrier (?K [X])\<rbrakk> \<Longrightarrow> degree (\<ominus>\<^bsub>?K [X]\<^esub> ?p) = degree ?p
subring (carrier R) R
\<lbrakk>?x \<in> carrier (poly_ring R); degree ?x \<le> ?n; ?y \<in> carrier (poly_ring R); degree ?y \<le> ?n\<rbrakk> \<Longrightarrow> degree (?x \<oplus>\<^bsub>poly_ring R\<^esub> ?y) \<le> ?n
?x \<in> carrier (poly_ring R) \<Longrightarrow> \<ominus>\<^bsub>poly_ring R\<^esub> ?x \<in> carrier (poly_ring R)

goal (1 subgoal):
 1. degree (x \<oplus>\<^bsub>poly_ring R\<^esub> \<ominus>\<^bsub>poly_ring R\<^esub> y) \<le> n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
degree (x \<ominus>\<^bsub>poly_ring R\<^esub> y) \<le> n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in domain) poly_sum_degree_le:
  assumes "finite A"
  assumes "\<And>x. x \<in> A \<Longrightarrow> degree (f x) \<le> n"
  assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<in> carrier (poly_ring R)"
  shows "degree (finsum (poly_ring R) f A) \<le> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (finsum (poly_ring R) f A) \<le> n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite A
?x \<in> A \<Longrightarrow> degree (f ?x) \<le> n
?x \<in> A \<Longrightarrow> f ?x \<in> carrier (poly_ring R)

goal (1 subgoal):
 1. degree (finsum (poly_ring R) f A) \<le> n
[PROOF STEP]
proof (induct A rule:finite_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>x. x \<in> {} \<Longrightarrow> degree (f x) \<le> n; \<And>x. x \<in> {} \<Longrightarrow> f x \<in> carrier (poly_ring R)\<rbrakk> \<Longrightarrow> degree (finsum (poly_ring R) f {}) \<le> n
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>\<And>x. x \<in> F \<Longrightarrow> degree (f x) \<le> n; \<And>x. x \<in> F \<Longrightarrow> f x \<in> carrier (poly_ring R)\<rbrakk> \<Longrightarrow> degree (finsum (poly_ring R) f F) \<le> n; \<And>xa. xa \<in> insert x F \<Longrightarrow> degree (f xa) \<le> n; \<And>xa. xa \<in> insert x F \<Longrightarrow> f xa \<in> carrier (poly_ring R)\<rbrakk> \<Longrightarrow> degree (finsum (poly_ring R) f (insert x F)) \<le> n
[PROOF STEP]
case empty
[PROOF STATE]
proof (state)
this:
?x \<in> {} \<Longrightarrow> degree (f ?x) \<le> n
?x \<in> {} \<Longrightarrow> f ?x \<in> carrier (poly_ring R)

goal (2 subgoals):
 1. \<lbrakk>\<And>x. x \<in> {} \<Longrightarrow> degree (f x) \<le> n; \<And>x. x \<in> {} \<Longrightarrow> f x \<in> carrier (poly_ring R)\<rbrakk> \<Longrightarrow> degree (finsum (poly_ring R) f {}) \<le> n
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>\<And>x. x \<in> F \<Longrightarrow> degree (f x) \<le> n; \<And>x. x \<in> F \<Longrightarrow> f x \<in> carrier (poly_ring R)\<rbrakk> \<Longrightarrow> degree (finsum (poly_ring R) f F) \<le> n; \<And>xa. xa \<in> insert x F \<Longrightarrow> degree (f xa) \<le> n; \<And>xa. xa \<in> insert x F \<Longrightarrow> f xa \<in> carrier (poly_ring R)\<rbrakk> \<Longrightarrow> degree (finsum (poly_ring R) f (insert x F)) \<le> n
[PROOF STEP]
interpret x:cring "poly_ring R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cring (poly_ring R)
[PROOF STEP]
using carrier_is_subring domain.univ_poly_is_cring domain_axioms
[PROOF STATE]
proof (prove)
using this:
subring (carrier R) R
\<lbrakk>domain ?R; subring ?K ?R\<rbrakk> \<Longrightarrow> cring (?K [X]\<^bsub>?R\<^esub>)
domain R

goal (1 subgoal):
 1. cring (poly_ring R)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>x. x \<in> {} \<Longrightarrow> degree (f x) \<le> n; \<And>x. x \<in> {} \<Longrightarrow> f x \<in> carrier (poly_ring R)\<rbrakk> \<Longrightarrow> degree (finsum (poly_ring R) f {}) \<le> n
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>\<And>x. x \<in> F \<Longrightarrow> degree (f x) \<le> n; \<And>x. x \<in> F \<Longrightarrow> f x \<in> carrier (poly_ring R)\<rbrakk> \<Longrightarrow> degree (finsum (poly_ring R) f F) \<le> n; \<And>xa. xa \<in> insert x F \<Longrightarrow> degree (f xa) \<le> n; \<And>xa. xa \<in> insert x F \<Longrightarrow> f xa \<in> carrier (poly_ring R)\<rbrakk> \<Longrightarrow> degree (finsum (poly_ring R) f (insert x F)) \<le> n
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (finsum (poly_ring R) f {}) \<le> n
[PROOF STEP]
using empty
[PROOF STATE]
proof (prove)
using this:
?x \<in> {} \<Longrightarrow> degree (f ?x) \<le> n
?x \<in> {} \<Longrightarrow> f ?x \<in> carrier (poly_ring R)

goal (1 subgoal):
 1. degree (finsum (poly_ring R) f {}) \<le> n
[PROOF STEP]
by (simp add:univ_poly_zero)
[PROOF STATE]
proof (state)
this:
degree (finsum (poly_ring R) f {}) \<le> n

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>\<And>x. x \<in> F \<Longrightarrow> degree (f x) \<le> n; \<And>x. x \<in> F \<Longrightarrow> f x \<in> carrier (poly_ring R)\<rbrakk> \<Longrightarrow> degree (finsum (poly_ring R) f F) \<le> n; \<And>xa. xa \<in> insert x F \<Longrightarrow> degree (f xa) \<le> n; \<And>xa. xa \<in> insert x F \<Longrightarrow> f xa \<in> carrier (poly_ring R)\<rbrakk> \<Longrightarrow> degree (finsum (poly_ring R) f (insert x F)) \<le> n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>\<And>x. x \<in> F \<Longrightarrow> degree (f x) \<le> n; \<And>x. x \<in> F \<Longrightarrow> f x \<in> carrier (poly_ring R)\<rbrakk> \<Longrightarrow> degree (finsum (poly_ring R) f F) \<le> n; \<And>xa. xa \<in> insert x F \<Longrightarrow> degree (f xa) \<le> n; \<And>xa. xa \<in> insert x F \<Longrightarrow> f xa \<in> carrier (poly_ring R)\<rbrakk> \<Longrightarrow> degree (finsum (poly_ring R) f (insert x F)) \<le> n
[PROOF STEP]
case (insert x F)
[PROOF STATE]
proof (state)
this:
finite F
x \<notin> F
\<lbrakk>\<And>x. x \<in> F \<Longrightarrow> degree (f x) \<le> n; \<And>x. x \<in> F \<Longrightarrow> f x \<in> carrier (poly_ring R)\<rbrakk> \<Longrightarrow> degree (finsum (poly_ring R) f F) \<le> n
?x \<in> insert x F \<Longrightarrow> degree (f ?x) \<le> n
?x \<in> insert x F \<Longrightarrow> f ?x \<in> carrier (poly_ring R)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>\<And>x. x \<in> F \<Longrightarrow> degree (f x) \<le> n; \<And>x. x \<in> F \<Longrightarrow> f x \<in> carrier (poly_ring R)\<rbrakk> \<Longrightarrow> degree (finsum (poly_ring R) f F) \<le> n; \<And>xa. xa \<in> insert x F \<Longrightarrow> degree (f xa) \<le> n; \<And>xa. xa \<in> insert x F \<Longrightarrow> f xa \<in> carrier (poly_ring R)\<rbrakk> \<Longrightarrow> degree (finsum (poly_ring R) f (insert x F)) \<le> n
[PROOF STEP]
interpret x:cring "poly_ring R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cring (poly_ring R)
[PROOF STEP]
using carrier_is_subring domain.univ_poly_is_cring domain_axioms
[PROOF STATE]
proof (prove)
using this:
subring (carrier R) R
\<lbrakk>domain ?R; subring ?K ?R\<rbrakk> \<Longrightarrow> cring (?K [X]\<^bsub>?R\<^esub>)
domain R

goal (1 subgoal):
 1. cring (poly_ring R)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>\<And>x. x \<in> F \<Longrightarrow> degree (f x) \<le> n; \<And>x. x \<in> F \<Longrightarrow> f x \<in> carrier (poly_ring R)\<rbrakk> \<Longrightarrow> degree (finsum (poly_ring R) f F) \<le> n; \<And>xa. xa \<in> insert x F \<Longrightarrow> degree (f xa) \<le> n; \<And>xa. xa \<in> insert x F \<Longrightarrow> f xa \<in> carrier (poly_ring R)\<rbrakk> \<Longrightarrow> degree (finsum (poly_ring R) f (insert x F)) \<le> n
[PROOF STEP]
have a: "degree (f x \<oplus>\<^bsub>poly_ring R\<^esub> finsum (poly_ring R) f F) \<le> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (f x \<oplus>\<^bsub>poly_ring R\<^esub> finsum (poly_ring R) f F) \<le> n
[PROOF STEP]
using insert poly_add_degree_le x.finsum_closed
[PROOF STATE]
proof (prove)
using this:
finite F
x \<notin> F
\<lbrakk>\<And>x. x \<in> F \<Longrightarrow> degree (f x) \<le> n; \<And>x. x \<in> F \<Longrightarrow> f x \<in> carrier (poly_ring R)\<rbrakk> \<Longrightarrow> degree (finsum (poly_ring R) f F) \<le> n
?x \<in> insert x F \<Longrightarrow> degree (f ?x) \<le> n
?x \<in> insert x F \<Longrightarrow> f ?x \<in> carrier (poly_ring R)
\<lbrakk>?x \<in> carrier (poly_ring R); degree ?x \<le> ?n; ?y \<in> carrier (poly_ring R); degree ?y \<le> ?n\<rbrakk> \<Longrightarrow> degree (?x \<oplus>\<^bsub>poly_ring R\<^esub> ?y) \<le> ?n
?f \<in> ?A \<rightarrow> carrier (poly_ring R) \<Longrightarrow> finsum (poly_ring R) ?f ?A \<in> carrier (poly_ring R)

goal (1 subgoal):
 1. degree (f x \<oplus>\<^bsub>poly_ring R\<^esub> finsum (poly_ring R) f F) \<le> n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
degree (f x \<oplus>\<^bsub>poly_ring R\<^esub> finsum (poly_ring R) f F) \<le> n

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>\<And>x. x \<in> F \<Longrightarrow> degree (f x) \<le> n; \<And>x. x \<in> F \<Longrightarrow> f x \<in> carrier (poly_ring R)\<rbrakk> \<Longrightarrow> degree (finsum (poly_ring R) f F) \<le> n; \<And>xa. xa \<in> insert x F \<Longrightarrow> degree (f xa) \<le> n; \<And>xa. xa \<in> insert x F \<Longrightarrow> f xa \<in> carrier (poly_ring R)\<rbrakk> \<Longrightarrow> degree (finsum (poly_ring R) f (insert x F)) \<le> n
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (finsum (poly_ring R) f (insert x F)) \<le> n
[PROOF STEP]
using insert a
[PROOF STATE]
proof (prove)
using this:
finite F
x \<notin> F
\<lbrakk>\<And>x. x \<in> F \<Longrightarrow> degree (f x) \<le> n; \<And>x. x \<in> F \<Longrightarrow> f x \<in> carrier (poly_ring R)\<rbrakk> \<Longrightarrow> degree (finsum (poly_ring R) f F) \<le> n
?x \<in> insert x F \<Longrightarrow> degree (f ?x) \<le> n
?x \<in> insert x F \<Longrightarrow> f ?x \<in> carrier (poly_ring R)
degree (f x \<oplus>\<^bsub>poly_ring R\<^esub> finsum (poly_ring R) f F) \<le> n

goal (1 subgoal):
 1. degree (finsum (poly_ring R) f (insert x F)) \<le> n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
degree (finsum (poly_ring R) f (insert x F)) \<le> n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in domain) lagrange_aux_eval:
  assumes "finite S"
  assumes "S \<subseteq> carrier R"
  assumes "x \<in> carrier R"
  shows "(eval (lagrange_basis_polynomial_aux S) x) = (\<Otimes>s \<in> S. x \<ominus> s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.eval (lagrange_basis_polynomial_aux S) x = finprod R (a_minus R x) S
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local.eval (lagrange_basis_polynomial_aux S) x = finprod R (a_minus R x) S
[PROOF STEP]
interpret x:ring_hom_cring "poly_ring R" "R" "(\<lambda>p. eval p x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring_hom_cring (poly_ring R) R (\<lambda>p. local.eval p x)
[PROOF STEP]
by (rule eval_cring_hom[OF carrier_is_subring assms(3)])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local.eval (lagrange_basis_polynomial_aux S) x = finprod R (a_minus R x) S
[PROOF STEP]
have "\<And>a. a \<in> S \<Longrightarrow> X \<ominus>\<^bsub>poly_ring R\<^esub> poly_of_const a \<in> carrier (poly_ring R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. a \<in> S \<Longrightarrow> X \<ominus>\<^bsub>poly_ring R\<^esub> poly_of_const a \<in> carrier (poly_ring R)
[PROOF STEP]
by (meson poly_of_const_in_carrier carrier_is_subring assms(2) cring.cring_simprules(4)
        domain_def subsetD univ_poly_is_domain var_closed(1))
[PROOF STATE]
proof (state)
this:
?a \<in> S \<Longrightarrow> X \<ominus>\<^bsub>poly_ring R\<^esub> poly_of_const ?a \<in> carrier (poly_ring R)

goal (1 subgoal):
 1. local.eval (lagrange_basis_polynomial_aux S) x = finprod R (a_minus R x) S
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?a \<in> S \<Longrightarrow> X \<ominus>\<^bsub>poly_ring R\<^esub> poly_of_const ?a \<in> carrier (poly_ring R)

goal (1 subgoal):
 1. local.eval (lagrange_basis_polynomial_aux S) x = finprod R (a_minus R x) S
[PROOF STEP]
have "\<And>s. s \<in> S \<Longrightarrow> eval (X \<ominus>\<^bsub>poly_ring R\<^esub> poly_of_const s) x = x \<ominus> s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. s \<in> S \<Longrightarrow> local.eval (X \<ominus>\<^bsub>poly_ring R\<^esub> poly_of_const s) x = x \<ominus> s
[PROOF STEP]
using assms var_closed carrier_is_subring poly_of_const_in_carrier subsetD[OF assms(2)]
[PROOF STATE]
proof (prove)
using this:
finite S
S \<subseteq> carrier R
x \<in> carrier R
subring ?K R \<Longrightarrow> X \<in> carrier (?K [X])
subring ?K R \<Longrightarrow> polynomial ?K X
subring (carrier R) R
?s \<in> carrier R \<Longrightarrow> poly_of_const ?s \<in> carrier (poly_ring R)
?c \<in> S \<Longrightarrow> ?c \<in> carrier R

goal (1 subgoal):
 1. \<And>s. s \<in> S \<Longrightarrow> local.eval (X \<ominus>\<^bsub>poly_ring R\<^esub> poly_of_const s) x = x \<ominus> s
[PROOF STEP]
by (simp add:eval_var eval_poly_of_const)
[PROOF STATE]
proof (state)
this:
?s \<in> S \<Longrightarrow> local.eval (X \<ominus>\<^bsub>poly_ring R\<^esub> poly_of_const ?s) x = x \<ominus> ?s

goal (1 subgoal):
 1. local.eval (lagrange_basis_polynomial_aux S) x = finprod R (a_minus R x) S
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?s \<in> S \<Longrightarrow> local.eval (X \<ominus>\<^bsub>poly_ring R\<^esub> poly_of_const ?s) x = x \<ominus> ?s

goal (1 subgoal):
 1. local.eval (lagrange_basis_polynomial_aux S) x = finprod R (a_minus R x) S
[PROOF STEP]
have "a_minus R x \<in> S \<rightarrow> carrier R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a_minus R x \<in> S \<rightarrow> carrier R
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite S
S \<subseteq> carrier R
x \<in> carrier R

goal (1 subgoal):
 1. a_minus R x \<in> S \<rightarrow> carrier R
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
a_minus R x \<in> S \<rightarrow> carrier R

goal (1 subgoal):
 1. local.eval (lagrange_basis_polynomial_aux S) x = finprod R (a_minus R x) S
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?a \<in> S \<Longrightarrow> X \<ominus>\<^bsub>poly_ring R\<^esub> poly_of_const ?a \<in> carrier (poly_ring R)
?s \<in> S \<Longrightarrow> local.eval (X \<ominus>\<^bsub>poly_ring R\<^esub> poly_of_const ?s) x = x \<ominus> ?s
a_minus R x \<in> S \<rightarrow> carrier R
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?a \<in> S \<Longrightarrow> X \<ominus>\<^bsub>poly_ring R\<^esub> poly_of_const ?a \<in> carrier (poly_ring R)
?s \<in> S \<Longrightarrow> local.eval (X \<ominus>\<^bsub>poly_ring R\<^esub> poly_of_const ?s) x = x \<ominus> ?s
a_minus R x \<in> S \<rightarrow> carrier R

goal (1 subgoal):
 1. local.eval (lagrange_basis_polynomial_aux S) x = finprod R (a_minus R x) S
[PROOF STEP]
by (simp add:lagrange_basis_polynomial_aux_def x.hom_finprod cong:finprod_cong')
[PROOF STATE]
proof (state)
this:
local.eval (lagrange_basis_polynomial_aux S) x = finprod R (a_minus R x) S

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in domain) lagrange_aux_poly:
  assumes "finite S"
  assumes "S \<subseteq> carrier R"
  shows "lagrange_basis_polynomial_aux S \<in> carrier (poly_ring R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lagrange_basis_polynomial_aux S \<in> carrier (poly_ring R)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lagrange_basis_polynomial_aux S \<in> carrier (poly_ring R)
[PROOF STEP]
have a:"subring (carrier R) R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subring (carrier R) R
[PROOF STEP]
using carrier_is_subring assms
[PROOF STATE]
proof (prove)
using this:
subring (carrier R) R
finite S
S \<subseteq> carrier R

goal (1 subgoal):
 1. subring (carrier R) R
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
subring (carrier R) R

goal (1 subgoal):
 1. lagrange_basis_polynomial_aux S \<in> carrier (poly_ring R)
[PROOF STEP]
have b: "\<And>a. a \<in> S \<Longrightarrow> X \<ominus>\<^bsub>poly_ring R\<^esub> poly_of_const a \<in> carrier (poly_ring R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. a \<in> S \<Longrightarrow> X \<ominus>\<^bsub>poly_ring R\<^esub> poly_of_const a \<in> carrier (poly_ring R)
[PROOF STEP]
by (meson poly_of_const_in_carrier a assms(2) cring.cring_simprules(4) domain_def subsetD
        univ_poly_is_domain var_closed(1))
[PROOF STATE]
proof (state)
this:
?a \<in> S \<Longrightarrow> X \<ominus>\<^bsub>poly_ring R\<^esub> poly_of_const ?a \<in> carrier (poly_ring R)

goal (1 subgoal):
 1. lagrange_basis_polynomial_aux S \<in> carrier (poly_ring R)
[PROOF STEP]
interpret x:cring "poly_ring R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cring (poly_ring R)
[PROOF STEP]
using carrier_is_subring domain.univ_poly_is_cring domain_axioms
[PROOF STATE]
proof (prove)
using this:
subring (carrier R) R
\<lbrakk>domain ?R; subring ?K ?R\<rbrakk> \<Longrightarrow> cring (?K [X]\<^bsub>?R\<^esub>)
domain R

goal (1 subgoal):
 1. cring (poly_ring R)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lagrange_basis_polynomial_aux S \<in> carrier (poly_ring R)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lagrange_basis_polynomial_aux S \<in> carrier (poly_ring R)
[PROOF STEP]
using lagrange_basis_polynomial_aux_def b x.finprod_closed[OF Pi_I]
[PROOF STATE]
proof (prove)
using this:
lagrange_basis_polynomial_aux ?S = (\<Otimes>\<^bsub>poly_ring R\<^esub>s\<in>?S. X \<ominus>\<^bsub>poly_ring R\<^esub> poly_of_const s)
?a \<in> S \<Longrightarrow> X \<ominus>\<^bsub>poly_ring R\<^esub> poly_of_const ?a \<in> carrier (poly_ring R)
(\<And>x. x \<in> ?A \<Longrightarrow> ?f x \<in> carrier (poly_ring R)) \<Longrightarrow> finprod (poly_ring R) ?f ?A \<in> carrier (poly_ring R)

goal (1 subgoal):
 1. lagrange_basis_polynomial_aux S \<in> carrier (poly_ring R)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lagrange_basis_polynomial_aux S \<in> carrier (poly_ring R)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in domain) poly_prod_degree_le:
  assumes "finite A"
  assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<in> carrier (poly_ring R)"
  shows "degree (finprod (poly_ring R) f A) \<le> (\<Sum>x \<in> A. degree (f x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (finprod (poly_ring R) f A) \<le> (\<Sum>x\<in>A. degree (f x))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite A
?x \<in> A \<Longrightarrow> f ?x \<in> carrier (poly_ring R)

goal (1 subgoal):
 1. degree (finprod (poly_ring R) f A) \<le> (\<Sum>x\<in>A. degree (f x))
[PROOF STEP]
proof (induct A rule:finite_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<And>x. x \<in> {} \<Longrightarrow> f x \<in> carrier (poly_ring R)) \<Longrightarrow> degree (finprod (poly_ring R) f {}) \<le> (\<Sum>x\<in>{}. degree (f x))
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; (\<And>x. x \<in> F \<Longrightarrow> f x \<in> carrier (poly_ring R)) \<Longrightarrow> degree (finprod (poly_ring R) f F) \<le> (\<Sum>x\<in>F. degree (f x)); \<And>xa. xa \<in> insert x F \<Longrightarrow> f xa \<in> carrier (poly_ring R)\<rbrakk> \<Longrightarrow> degree (finprod (poly_ring R) f (insert x F)) \<le> (\<Sum>x\<in>insert x F. degree (f x))
[PROOF STEP]
case empty
[PROOF STATE]
proof (state)
this:
?x \<in> {} \<Longrightarrow> f ?x \<in> carrier (poly_ring R)

goal (2 subgoals):
 1. (\<And>x. x \<in> {} \<Longrightarrow> f x \<in> carrier (poly_ring R)) \<Longrightarrow> degree (finprod (poly_ring R) f {}) \<le> (\<Sum>x\<in>{}. degree (f x))
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; (\<And>x. x \<in> F \<Longrightarrow> f x \<in> carrier (poly_ring R)) \<Longrightarrow> degree (finprod (poly_ring R) f F) \<le> (\<Sum>x\<in>F. degree (f x)); \<And>xa. xa \<in> insert x F \<Longrightarrow> f xa \<in> carrier (poly_ring R)\<rbrakk> \<Longrightarrow> degree (finprod (poly_ring R) f (insert x F)) \<le> (\<Sum>x\<in>insert x F. degree (f x))
[PROOF STEP]
interpret x:cring "poly_ring R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cring (poly_ring R)
[PROOF STEP]
using carrier_is_subring domain.univ_poly_is_cring domain_axioms
[PROOF STATE]
proof (prove)
using this:
subring (carrier R) R
\<lbrakk>domain ?R; subring ?K ?R\<rbrakk> \<Longrightarrow> cring (?K [X]\<^bsub>?R\<^esub>)
domain R

goal (1 subgoal):
 1. cring (poly_ring R)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<And>x. x \<in> {} \<Longrightarrow> f x \<in> carrier (poly_ring R)) \<Longrightarrow> degree (finprod (poly_ring R) f {}) \<le> (\<Sum>x\<in>{}. degree (f x))
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; (\<And>x. x \<in> F \<Longrightarrow> f x \<in> carrier (poly_ring R)) \<Longrightarrow> degree (finprod (poly_ring R) f F) \<le> (\<Sum>x\<in>F. degree (f x)); \<And>xa. xa \<in> insert x F \<Longrightarrow> f xa \<in> carrier (poly_ring R)\<rbrakk> \<Longrightarrow> degree (finprod (poly_ring R) f (insert x F)) \<le> (\<Sum>x\<in>insert x F. degree (f x))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (finprod (poly_ring R) f {}) \<le> (\<Sum>x\<in>{}. degree (f x))
[PROOF STEP]
by (simp add:univ_poly_one)
[PROOF STATE]
proof (state)
this:
degree (finprod (poly_ring R) f {}) \<le> (\<Sum>x\<in>{}. degree (f x))

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; (\<And>x. x \<in> F \<Longrightarrow> f x \<in> carrier (poly_ring R)) \<Longrightarrow> degree (finprod (poly_ring R) f F) \<le> (\<Sum>x\<in>F. degree (f x)); \<And>xa. xa \<in> insert x F \<Longrightarrow> f xa \<in> carrier (poly_ring R)\<rbrakk> \<Longrightarrow> degree (finprod (poly_ring R) f (insert x F)) \<le> (\<Sum>x\<in>insert x F. degree (f x))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; (\<And>x. x \<in> F \<Longrightarrow> f x \<in> carrier (poly_ring R)) \<Longrightarrow> degree (finprod (poly_ring R) f F) \<le> (\<Sum>x\<in>F. degree (f x)); \<And>xa. xa \<in> insert x F \<Longrightarrow> f xa \<in> carrier (poly_ring R)\<rbrakk> \<Longrightarrow> degree (finprod (poly_ring R) f (insert x F)) \<le> (\<Sum>x\<in>insert x F. degree (f x))
[PROOF STEP]
case (insert x F)
[PROOF STATE]
proof (state)
this:
finite F
x \<notin> F
(\<And>x. x \<in> F \<Longrightarrow> f x \<in> carrier (poly_ring R)) \<Longrightarrow> degree (finprod (poly_ring R) f F) \<le> (\<Sum>x\<in>F. degree (f x))
?x \<in> insert x F \<Longrightarrow> f ?x \<in> carrier (poly_ring R)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; (\<And>x. x \<in> F \<Longrightarrow> f x \<in> carrier (poly_ring R)) \<Longrightarrow> degree (finprod (poly_ring R) f F) \<le> (\<Sum>x\<in>F. degree (f x)); \<And>xa. xa \<in> insert x F \<Longrightarrow> f xa \<in> carrier (poly_ring R)\<rbrakk> \<Longrightarrow> degree (finprod (poly_ring R) f (insert x F)) \<le> (\<Sum>x\<in>insert x F. degree (f x))
[PROOF STEP]
interpret x:cring "poly_ring R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cring (poly_ring R)
[PROOF STEP]
using carrier_is_subring domain.univ_poly_is_cring domain_axioms
[PROOF STATE]
proof (prove)
using this:
subring (carrier R) R
\<lbrakk>domain ?R; subring ?K ?R\<rbrakk> \<Longrightarrow> cring (?K [X]\<^bsub>?R\<^esub>)
domain R

goal (1 subgoal):
 1. cring (poly_ring R)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; (\<And>x. x \<in> F \<Longrightarrow> f x \<in> carrier (poly_ring R)) \<Longrightarrow> degree (finprod (poly_ring R) f F) \<le> (\<Sum>x\<in>F. degree (f x)); \<And>xa. xa \<in> insert x F \<Longrightarrow> f xa \<in> carrier (poly_ring R)\<rbrakk> \<Longrightarrow> degree (finprod (poly_ring R) f (insert x F)) \<le> (\<Sum>x\<in>insert x F. degree (f x))
[PROOF STEP]
have a:"f \<in> F \<rightarrow> carrier (poly_ring R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> F \<rightarrow> carrier (poly_ring R)
[PROOF STEP]
using insert
[PROOF STATE]
proof (prove)
using this:
finite F
x \<notin> F
(\<And>x. x \<in> F \<Longrightarrow> f x \<in> carrier (poly_ring R)) \<Longrightarrow> degree (finprod (poly_ring R) f F) \<le> (\<Sum>x\<in>F. degree (f x))
?x \<in> insert x F \<Longrightarrow> f ?x \<in> carrier (poly_ring R)

goal (1 subgoal):
 1. f \<in> F \<rightarrow> carrier (poly_ring R)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f \<in> F \<rightarrow> carrier (poly_ring R)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; (\<And>x. x \<in> F \<Longrightarrow> f x \<in> carrier (poly_ring R)) \<Longrightarrow> degree (finprod (poly_ring R) f F) \<le> (\<Sum>x\<in>F. degree (f x)); \<And>xa. xa \<in> insert x F \<Longrightarrow> f xa \<in> carrier (poly_ring R)\<rbrakk> \<Longrightarrow> degree (finprod (poly_ring R) f (insert x F)) \<le> (\<Sum>x\<in>insert x F. degree (f x))
[PROOF STEP]
have b:"f x \<in> carrier (poly_ring R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f x \<in> carrier (poly_ring R)
[PROOF STEP]
using insert
[PROOF STATE]
proof (prove)
using this:
finite F
x \<notin> F
(\<And>x. x \<in> F \<Longrightarrow> f x \<in> carrier (poly_ring R)) \<Longrightarrow> degree (finprod (poly_ring R) f F) \<le> (\<Sum>x\<in>F. degree (f x))
?x \<in> insert x F \<Longrightarrow> f ?x \<in> carrier (poly_ring R)

goal (1 subgoal):
 1. f x \<in> carrier (poly_ring R)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f x \<in> carrier (poly_ring R)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; (\<And>x. x \<in> F \<Longrightarrow> f x \<in> carrier (poly_ring R)) \<Longrightarrow> degree (finprod (poly_ring R) f F) \<le> (\<Sum>x\<in>F. degree (f x)); \<And>xa. xa \<in> insert x F \<Longrightarrow> f xa \<in> carrier (poly_ring R)\<rbrakk> \<Longrightarrow> degree (finprod (poly_ring R) f (insert x F)) \<le> (\<Sum>x\<in>insert x F. degree (f x))
[PROOF STEP]
have "degree (finprod (poly_ring R) f (insert x F)) = degree (f x \<otimes>\<^bsub>poly_ring R\<^esub> finprod (poly_ring R) f F)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (finprod (poly_ring R) f (insert x F)) = degree (f x \<otimes>\<^bsub>poly_ring R\<^esub> finprod (poly_ring R) f F)
[PROOF STEP]
using a b insert
[PROOF STATE]
proof (prove)
using this:
f \<in> F \<rightarrow> carrier (poly_ring R)
f x \<in> carrier (poly_ring R)
finite F
x \<notin> F
(\<And>x. x \<in> F \<Longrightarrow> f x \<in> carrier (poly_ring R)) \<Longrightarrow> degree (finprod (poly_ring R) f F) \<le> (\<Sum>x\<in>F. degree (f x))
?x \<in> insert x F \<Longrightarrow> f ?x \<in> carrier (poly_ring R)

goal (1 subgoal):
 1. degree (finprod (poly_ring R) f (insert x F)) = degree (f x \<otimes>\<^bsub>poly_ring R\<^esub> finprod (poly_ring R) f F)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
degree (finprod (poly_ring R) f (insert x F)) = degree (f x \<otimes>\<^bsub>poly_ring R\<^esub> finprod (poly_ring R) f F)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; (\<And>x. x \<in> F \<Longrightarrow> f x \<in> carrier (poly_ring R)) \<Longrightarrow> degree (finprod (poly_ring R) f F) \<le> (\<Sum>x\<in>F. degree (f x)); \<And>xa. xa \<in> insert x F \<Longrightarrow> f xa \<in> carrier (poly_ring R)\<rbrakk> \<Longrightarrow> degree (finprod (poly_ring R) f (insert x F)) \<le> (\<Sum>x\<in>insert x F. degree (f x))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
degree (finprod (poly_ring R) f (insert x F)) = degree (f x \<otimes>\<^bsub>poly_ring R\<^esub> finprod (poly_ring R) f F)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; (\<And>x. x \<in> F \<Longrightarrow> f x \<in> carrier (poly_ring R)) \<Longrightarrow> degree (finprod (poly_ring R) f F) \<le> (\<Sum>x\<in>F. degree (f x)); \<And>xa. xa \<in> insert x F \<Longrightarrow> f xa \<in> carrier (poly_ring R)\<rbrakk> \<Longrightarrow> degree (finprod (poly_ring R) f (insert x F)) \<le> (\<Sum>x\<in>insert x F. degree (f x))
[PROOF STEP]
have "... \<le> degree (f x) + degree (finprod (poly_ring R) f F)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (f x \<otimes>\<^bsub>poly_ring R\<^esub> finprod (poly_ring R) f F) \<le> degree (f x) + degree (finprod (poly_ring R) f F)
[PROOF STEP]
using poly_mult_degree_le x.finprod_closed[OF a] b
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> carrier (poly_ring R); ?y \<in> carrier (poly_ring R); degree ?x \<le> ?n; degree ?y \<le> ?m\<rbrakk> \<Longrightarrow> degree (?x \<otimes>\<^bsub>poly_ring R\<^esub> ?y) \<le> ?n + ?m
finprod (poly_ring R) f F \<in> carrier (poly_ring R)
f x \<in> carrier (poly_ring R)

goal (1 subgoal):
 1. degree (f x \<otimes>\<^bsub>poly_ring R\<^esub> finprod (poly_ring R) f F) \<le> degree (f x) + degree (finprod (poly_ring R) f F)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
degree (f x \<otimes>\<^bsub>poly_ring R\<^esub> finprod (poly_ring R) f F) \<le> degree (f x) + degree (finprod (poly_ring R) f F)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; (\<And>x. x \<in> F \<Longrightarrow> f x \<in> carrier (poly_ring R)) \<Longrightarrow> degree (finprod (poly_ring R) f F) \<le> (\<Sum>x\<in>F. degree (f x)); \<And>xa. xa \<in> insert x F \<Longrightarrow> f xa \<in> carrier (poly_ring R)\<rbrakk> \<Longrightarrow> degree (finprod (poly_ring R) f (insert x F)) \<le> (\<Sum>x\<in>insert x F. degree (f x))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
degree (f x \<otimes>\<^bsub>poly_ring R\<^esub> finprod (poly_ring R) f F) \<le> degree (f x) + degree (finprod (poly_ring R) f F)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; (\<And>x. x \<in> F \<Longrightarrow> f x \<in> carrier (poly_ring R)) \<Longrightarrow> degree (finprod (poly_ring R) f F) \<le> (\<Sum>x\<in>F. degree (f x)); \<And>xa. xa \<in> insert x F \<Longrightarrow> f xa \<in> carrier (poly_ring R)\<rbrakk> \<Longrightarrow> degree (finprod (poly_ring R) f (insert x F)) \<le> (\<Sum>x\<in>insert x F. degree (f x))
[PROOF STEP]
have "... \<le> degree (f x) + (\<Sum>y \<in> F. degree (f y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (f x) + degree (finprod (poly_ring R) f F) \<le> degree (f x) + (\<Sum>y\<in>F. degree (f y))
[PROOF STEP]
using insert(3) a add_mono
[PROOF STATE]
proof (prove)
using this:
(\<And>x. x \<in> F \<Longrightarrow> f x \<in> carrier (poly_ring R)) \<Longrightarrow> degree (finprod (poly_ring R) f F) \<le> (\<Sum>x\<in>F. degree (f x))
f \<in> F \<rightarrow> carrier (poly_ring R)
\<lbrakk>?a \<le> ?b; ?c \<le> ?d\<rbrakk> \<Longrightarrow> ?a + ?c \<le> ?b + ?d

goal (1 subgoal):
 1. degree (f x) + degree (finprod (poly_ring R) f F) \<le> degree (f x) + (\<Sum>y\<in>F. degree (f y))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
degree (f x) + degree (finprod (poly_ring R) f F) \<le> degree (f x) + (\<Sum>y\<in>F. degree (f y))

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; (\<And>x. x \<in> F \<Longrightarrow> f x \<in> carrier (poly_ring R)) \<Longrightarrow> degree (finprod (poly_ring R) f F) \<le> (\<Sum>x\<in>F. degree (f x)); \<And>xa. xa \<in> insert x F \<Longrightarrow> f xa \<in> carrier (poly_ring R)\<rbrakk> \<Longrightarrow> degree (finprod (poly_ring R) f (insert x F)) \<le> (\<Sum>x\<in>insert x F. degree (f x))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
degree (f x) + degree (finprod (poly_ring R) f F) \<le> degree (f x) + (\<Sum>y\<in>F. degree (f y))

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; (\<And>x. x \<in> F \<Longrightarrow> f x \<in> carrier (poly_ring R)) \<Longrightarrow> degree (finprod (poly_ring R) f F) \<le> (\<Sum>x\<in>F. degree (f x)); \<And>xa. xa \<in> insert x F \<Longrightarrow> f xa \<in> carrier (poly_ring R)\<rbrakk> \<Longrightarrow> degree (finprod (poly_ring R) f (insert x F)) \<le> (\<Sum>x\<in>insert x F. degree (f x))
[PROOF STEP]
have "... = (\<Sum>y \<in> (insert x F). degree (f y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (f x) + (\<Sum>y\<in>F. degree (f y)) = (\<Sum>y\<in>insert x F. degree (f y))
[PROOF STEP]
using insert
[PROOF STATE]
proof (prove)
using this:
finite F
x \<notin> F
(\<And>x. x \<in> F \<Longrightarrow> f x \<in> carrier (poly_ring R)) \<Longrightarrow> degree (finprod (poly_ring R) f F) \<le> (\<Sum>x\<in>F. degree (f x))
?x \<in> insert x F \<Longrightarrow> f ?x \<in> carrier (poly_ring R)

goal (1 subgoal):
 1. degree (f x) + (\<Sum>y\<in>F. degree (f y)) = (\<Sum>y\<in>insert x F. degree (f y))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
degree (f x) + (\<Sum>y\<in>F. degree (f y)) = (\<Sum>y\<in>insert x F. degree (f y))

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; (\<And>x. x \<in> F \<Longrightarrow> f x \<in> carrier (poly_ring R)) \<Longrightarrow> degree (finprod (poly_ring R) f F) \<le> (\<Sum>x\<in>F. degree (f x)); \<And>xa. xa \<in> insert x F \<Longrightarrow> f xa \<in> carrier (poly_ring R)\<rbrakk> \<Longrightarrow> degree (finprod (poly_ring R) f (insert x F)) \<le> (\<Sum>x\<in>insert x F. degree (f x))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
degree (finprod (poly_ring R) f (insert x F)) \<le> (\<Sum>y\<in>insert x F. degree (f y))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
degree (finprod (poly_ring R) f (insert x F)) \<le> (\<Sum>y\<in>insert x F. degree (f y))

goal (1 subgoal):
 1. degree (finprod (poly_ring R) f (insert x F)) \<le> (\<Sum>x\<in>insert x F. degree (f x))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
degree (finprod (poly_ring R) f (insert x F)) \<le> (\<Sum>x\<in>insert x F. degree (f x))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in domain) lagrange_aux_degree:
  assumes "finite S"
  assumes "S \<subseteq> carrier R"
  shows "degree (lagrange_basis_polynomial_aux S) \<le> card S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (lagrange_basis_polynomial_aux S) \<le> card S
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. degree (lagrange_basis_polynomial_aux S) \<le> card S
[PROOF STEP]
interpret x:cring "poly_ring R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cring (poly_ring R)
[PROOF STEP]
using carrier_is_subring domain.univ_poly_is_cring domain_axioms
[PROOF STATE]
proof (prove)
using this:
subring (carrier R) R
\<lbrakk>domain ?R; subring ?K ?R\<rbrakk> \<Longrightarrow> cring (?K [X]\<^bsub>?R\<^esub>)
domain R

goal (1 subgoal):
 1. cring (poly_ring R)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. degree (lagrange_basis_polynomial_aux S) \<le> card S
[PROOF STEP]
have "degree X \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree X \<le> 1
[PROOF STEP]
by (simp add:var_def)
[PROOF STATE]
proof (state)
this:
degree X \<le> 1

goal (1 subgoal):
 1. degree (lagrange_basis_polynomial_aux S) \<le> card S
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
degree X \<le> 1

goal (1 subgoal):
 1. degree (lagrange_basis_polynomial_aux S) \<le> card S
[PROOF STEP]
have "\<And>y. y\<in> S \<Longrightarrow> degree (poly_of_const y) \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. y \<in> S \<Longrightarrow> degree (poly_of_const y) \<le> 1
[PROOF STEP]
by (simp add:poly_of_const_def)
[PROOF STATE]
proof (state)
this:
?y \<in> S \<Longrightarrow> degree (poly_of_const ?y) \<le> 1

goal (1 subgoal):
 1. degree (lagrange_basis_polynomial_aux S) \<le> card S
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
degree X \<le> 1
?y \<in> S \<Longrightarrow> degree (poly_of_const ?y) \<le> 1
[PROOF STEP]
have a: "\<And>y. y\<in> S \<Longrightarrow> degree (X \<ominus>\<^bsub>poly_ring R\<^esub> poly_of_const y) \<le> 1"
[PROOF STATE]
proof (prove)
using this:
degree X \<le> 1
?y \<in> S \<Longrightarrow> degree (poly_of_const ?y) \<le> 1

goal (1 subgoal):
 1. \<And>y. y \<in> S \<Longrightarrow> degree (X \<ominus>\<^bsub>poly_ring R\<^esub> poly_of_const y) \<le> 1
[PROOF STEP]
by (meson assms(2) in_mono poly_of_const_in_carrier poly_sub_degree_le var_closed[OF carrier_is_subring])
[PROOF STATE]
proof (state)
this:
?y \<in> S \<Longrightarrow> degree (X \<ominus>\<^bsub>poly_ring R\<^esub> poly_of_const ?y) \<le> 1

goal (1 subgoal):
 1. degree (lagrange_basis_polynomial_aux S) \<le> card S
[PROOF STEP]
have b:"\<And>y. y \<in> S \<Longrightarrow> (X \<ominus>\<^bsub>poly_ring R\<^esub> poly_of_const y) \<in> carrier (poly_ring R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. y \<in> S \<Longrightarrow> X \<ominus>\<^bsub>poly_ring R\<^esub> poly_of_const y \<in> carrier (poly_ring R)
[PROOF STEP]
by (meson subsetD x.minus_closed var_closed(1)[OF carrier_is_subring] poly_of_const_in_carrier assms(2))
[PROOF STATE]
proof (state)
this:
?y \<in> S \<Longrightarrow> X \<ominus>\<^bsub>poly_ring R\<^esub> poly_of_const ?y \<in> carrier (poly_ring R)

goal (1 subgoal):
 1. degree (lagrange_basis_polynomial_aux S) \<le> card S
[PROOF STEP]
have "degree (lagrange_basis_polynomial_aux S) \<le> (\<Sum>y \<in> S. degree (X \<ominus>\<^bsub>poly_ring R\<^esub> poly_of_const y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (lagrange_basis_polynomial_aux S) \<le> (\<Sum>y\<in>S. degree (X \<ominus>\<^bsub>poly_ring R\<^esub> poly_of_const y))
[PROOF STEP]
using lagrange_basis_polynomial_aux_def b poly_prod_degree_le[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
lagrange_basis_polynomial_aux ?S = (\<Otimes>\<^bsub>poly_ring R\<^esub>s\<in>?S. X \<ominus>\<^bsub>poly_ring R\<^esub> poly_of_const s)
?y \<in> S \<Longrightarrow> X \<ominus>\<^bsub>poly_ring R\<^esub> poly_of_const ?y \<in> carrier (poly_ring R)
(\<And>x. x \<in> S \<Longrightarrow> ?f x \<in> carrier (poly_ring R)) \<Longrightarrow> degree (finprod (poly_ring R) ?f S) \<le> (\<Sum>x\<in>S. degree (?f x))

goal (1 subgoal):
 1. degree (lagrange_basis_polynomial_aux S) \<le> (\<Sum>y\<in>S. degree (X \<ominus>\<^bsub>poly_ring R\<^esub> poly_of_const y))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
degree (lagrange_basis_polynomial_aux S) \<le> (\<Sum>y\<in>S. degree (X \<ominus>\<^bsub>poly_ring R\<^esub> poly_of_const y))

goal (1 subgoal):
 1. degree (lagrange_basis_polynomial_aux S) \<le> card S
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
degree (lagrange_basis_polynomial_aux S) \<le> (\<Sum>y\<in>S. degree (X \<ominus>\<^bsub>poly_ring R\<^esub> poly_of_const y))

goal (1 subgoal):
 1. degree (lagrange_basis_polynomial_aux S) \<le> card S
[PROOF STEP]
have "... \<le> (\<Sum>y \<in> S. 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>y\<in>S. degree (X \<ominus>\<^bsub>poly_ring R\<^esub> poly_of_const y)) \<le> (\<Sum>y\<in>S. 1)
[PROOF STEP]
using sum_mono a
[PROOF STATE]
proof (prove)
using this:
(\<And>i. i \<in> ?K \<Longrightarrow> ?f i \<le> ?g i) \<Longrightarrow> sum ?f ?K \<le> sum ?g ?K
?y \<in> S \<Longrightarrow> degree (X \<ominus>\<^bsub>poly_ring R\<^esub> poly_of_const ?y) \<le> 1

goal (1 subgoal):
 1. (\<Sum>y\<in>S. degree (X \<ominus>\<^bsub>poly_ring R\<^esub> poly_of_const y)) \<le> (\<Sum>y\<in>S. 1)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(\<Sum>y\<in>S. degree (X \<ominus>\<^bsub>poly_ring R\<^esub> poly_of_const y)) \<le> (\<Sum>y\<in>S. 1)

goal (1 subgoal):
 1. degree (lagrange_basis_polynomial_aux S) \<le> card S
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>y\<in>S. degree (X \<ominus>\<^bsub>poly_ring R\<^esub> poly_of_const y)) \<le> (\<Sum>y\<in>S. 1)

goal (1 subgoal):
 1. degree (lagrange_basis_polynomial_aux S) \<le> card S
[PROOF STEP]
have "... = card S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>y\<in>S. 1) = card S
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>y\<in>S. 1) = card S

goal (1 subgoal):
 1. degree (lagrange_basis_polynomial_aux S) \<le> card S
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
degree (lagrange_basis_polynomial_aux S) \<le> card S
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
degree (lagrange_basis_polynomial_aux S) \<le> card S

goal (1 subgoal):
 1. degree (lagrange_basis_polynomial_aux S) \<le> card S
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
degree (lagrange_basis_polynomial_aux S) \<le> card S

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in field)
  assumes "finite S"
  assumes "S \<subseteq> carrier R"
  assumes "x \<in> carrier R - S"
  shows
    lagrange_one: "eval (lagrange_basis_polynomial S x) x = \<one>" and
    lagrange_degree: "degree (lagrange_basis_polynomial S x) \<le> card S" and
    lagrange_zero: "\<And>s. s \<in> S \<Longrightarrow> eval (lagrange_basis_polynomial S x) s = \<zero>" and
    lagrange_poly: "lagrange_basis_polynomial S x \<in> carrier (poly_ring R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (local.eval (lagrange_basis_polynomial S x) x = \<one> &&& degree (lagrange_basis_polynomial S x) \<le> card S) &&& (\<And>s. s \<in> S \<Longrightarrow> local.eval (lagrange_basis_polynomial S x) s = \<zero>) &&& lagrange_basis_polynomial S x \<in> carrier (poly_ring R)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. local.eval (lagrange_basis_polynomial S x) x = \<one>
 2. degree (lagrange_basis_polynomial S x) \<le> card S
 3. \<And>s. s \<in> S \<Longrightarrow> local.eval (lagrange_basis_polynomial S x) s = \<zero>
 4. lagrange_basis_polynomial S x \<in> carrier (poly_ring R)
[PROOF STEP]
interpret x:ring_hom_cring "poly_ring R" "R" "(\<lambda>p. eval p x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring_hom_cring (poly_ring R) R (\<lambda>p. local.eval p x)
[PROOF STEP]
using assms carrier_is_subring eval_cring_hom
[PROOF STATE]
proof (prove)
using this:
finite S
S \<subseteq> carrier R
x \<in> carrier R - S
subring (carrier R) R
\<lbrakk>subring ?K R; ?a \<in> carrier R\<rbrakk> \<Longrightarrow> ring_hom_cring (?K [X]) R (\<lambda>p. local.eval p ?a)

goal (1 subgoal):
 1. ring_hom_cring (poly_ring R) R (\<lambda>p. local.eval p x)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. local.eval (lagrange_basis_polynomial S x) x = \<one>
 2. degree (lagrange_basis_polynomial S x) \<le> card S
 3. \<And>s. s \<in> S \<Longrightarrow> local.eval (lagrange_basis_polynomial S x) s = \<zero>
 4. lagrange_basis_polynomial S x \<in> carrier (poly_ring R)
[PROOF STEP]
define p where "p = lagrange_basis_polynomial_aux S"
[PROOF STATE]
proof (state)
this:
p = lagrange_basis_polynomial_aux S

goal (4 subgoals):
 1. local.eval (lagrange_basis_polynomial S x) x = \<one>
 2. degree (lagrange_basis_polynomial S x) \<le> card S
 3. \<And>s. s \<in> S \<Longrightarrow> local.eval (lagrange_basis_polynomial S x) s = \<zero>
 4. lagrange_basis_polynomial S x \<in> carrier (poly_ring R)
[PROOF STEP]
have a:"eval p x = (\<Otimes>s \<in> S. x \<ominus> s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.eval p x = finprod R (a_minus R x) S
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite S
S \<subseteq> carrier R
x \<in> carrier R - S

goal (1 subgoal):
 1. local.eval p x = finprod R (a_minus R x) S
[PROOF STEP]
by (simp add:p_def lagrange_aux_eval)
[PROOF STATE]
proof (state)
this:
local.eval p x = finprod R (a_minus R x) S

goal (4 subgoals):
 1. local.eval (lagrange_basis_polynomial S x) x = \<one>
 2. degree (lagrange_basis_polynomial S x) \<le> card S
 3. \<And>s. s \<in> S \<Longrightarrow> local.eval (lagrange_basis_polynomial S x) s = \<zero>
 4. lagrange_basis_polynomial S x \<in> carrier (poly_ring R)
[PROOF STEP]
have b:"p \<in> carrier (poly_ring R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<in> carrier (poly_ring R)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite S
S \<subseteq> carrier R
x \<in> carrier R - S

goal (1 subgoal):
 1. p \<in> carrier (poly_ring R)
[PROOF STEP]
by (simp add:p_def lagrange_aux_poly)
[PROOF STATE]
proof (state)
this:
p \<in> carrier (poly_ring R)

goal (4 subgoals):
 1. local.eval (lagrange_basis_polynomial S x) x = \<one>
 2. degree (lagrange_basis_polynomial S x) \<le> card S
 3. \<And>s. s \<in> S \<Longrightarrow> local.eval (lagrange_basis_polynomial S x) s = \<zero>
 4. lagrange_basis_polynomial S x \<in> carrier (poly_ring R)
[PROOF STEP]
have "\<And>y. y \<in> S \<Longrightarrow> a_minus R x y \<in> carrier R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. y \<in> S \<Longrightarrow> x \<ominus> y \<in> carrier R
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite S
S \<subseteq> carrier R
x \<in> carrier R - S

goal (1 subgoal):
 1. \<And>y. y \<in> S \<Longrightarrow> x \<ominus> y \<in> carrier R
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
?y \<in> S \<Longrightarrow> x \<ominus> ?y \<in> carrier R

goal (4 subgoals):
 1. local.eval (lagrange_basis_polynomial S x) x = \<one>
 2. degree (lagrange_basis_polynomial S x) \<le> card S
 3. \<And>s. s \<in> S \<Longrightarrow> local.eval (lagrange_basis_polynomial S x) s = \<zero>
 4. lagrange_basis_polynomial S x \<in> carrier (poly_ring R)
[PROOF STEP]
hence c:"finprod R (a_minus R x) S \<in> Units R"
[PROOF STATE]
proof (prove)
using this:
?y \<in> S \<Longrightarrow> x \<ominus> ?y \<in> carrier R

goal (1 subgoal):
 1. finprod R (a_minus R x) S \<in> Units R
[PROOF STEP]
using finprod_closed[OF Pi_I] assms
[PROOF STATE]
proof (prove)
using this:
?y \<in> S \<Longrightarrow> x \<ominus> ?y \<in> carrier R
(\<And>x. x \<in> ?A \<Longrightarrow> ?f x \<in> carrier R) \<Longrightarrow> finprod R ?f ?A \<in> carrier R
finite S
S \<subseteq> carrier R
x \<in> carrier R - S

goal (1 subgoal):
 1. finprod R (a_minus R x) S \<in> Units R
[PROOF STEP]
by (auto simp add:field_Units finprod_zero_iff)
[PROOF STATE]
proof (state)
this:
finprod R (a_minus R x) S \<in> Units R

goal (4 subgoals):
 1. local.eval (lagrange_basis_polynomial S x) x = \<one>
 2. degree (lagrange_basis_polynomial S x) \<le> card S
 3. \<And>s. s \<in> S \<Longrightarrow> local.eval (lagrange_basis_polynomial S x) s = \<zero>
 4. lagrange_basis_polynomial S x \<in> carrier (poly_ring R)
[PROOF STEP]
have "eval (lagrange_basis_polynomial S x) x =
    (\<Otimes>s \<in> S. x \<ominus> s) \<otimes> eval (poly_of_const (inv finprod R (a_minus R x) S)) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.eval (lagrange_basis_polynomial S x) x = finprod R (a_minus R x) S \<otimes> local.eval (poly_of_const (inv finprod R (a_minus R x) S)) x
[PROOF STEP]
using poly_of_const_in_carrier Units_inv_closed c p_def[symmetric]
[PROOF STATE]
proof (prove)
using this:
?s \<in> carrier R \<Longrightarrow> poly_of_const ?s \<in> carrier (poly_ring R)
?x \<in> Units R \<Longrightarrow> inv ?x \<in> carrier R
finprod R (a_minus R x) S \<in> Units R
lagrange_basis_polynomial_aux S = p

goal (1 subgoal):
 1. local.eval (lagrange_basis_polynomial S x) x = finprod R (a_minus R x) S \<otimes> local.eval (poly_of_const (inv finprod R (a_minus R x) S)) x
[PROOF STEP]
by (simp add: lagrange_basis_polynomial_def x.hom_mult[OF b] a)
[PROOF STATE]
proof (state)
this:
local.eval (lagrange_basis_polynomial S x) x = finprod R (a_minus R x) S \<otimes> local.eval (poly_of_const (inv finprod R (a_minus R x) S)) x

goal (4 subgoals):
 1. local.eval (lagrange_basis_polynomial S x) x = \<one>
 2. degree (lagrange_basis_polynomial S x) \<le> card S
 3. \<And>s. s \<in> S \<Longrightarrow> local.eval (lagrange_basis_polynomial S x) s = \<zero>
 4. lagrange_basis_polynomial S x \<in> carrier (poly_ring R)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
local.eval (lagrange_basis_polynomial S x) x = finprod R (a_minus R x) S \<otimes> local.eval (poly_of_const (inv finprod R (a_minus R x) S)) x

goal (4 subgoals):
 1. local.eval (lagrange_basis_polynomial S x) x = \<one>
 2. degree (lagrange_basis_polynomial S x) \<le> card S
 3. \<And>s. s \<in> S \<Longrightarrow> local.eval (lagrange_basis_polynomial S x) s = \<zero>
 4. lagrange_basis_polynomial S x \<in> carrier (poly_ring R)
[PROOF STEP]
have "... =  \<one>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finprod R (a_minus R x) S \<otimes> local.eval (poly_of_const (inv finprod R (a_minus R x) S)) x = \<one>
[PROOF STEP]
using poly_of_const_in_carrier Units_inv_closed c eval_poly_of_const
[PROOF STATE]
proof (prove)
using this:
?s \<in> carrier R \<Longrightarrow> poly_of_const ?s \<in> carrier (poly_ring R)
?x \<in> Units R \<Longrightarrow> inv ?x \<in> carrier R
finprod R (a_minus R x) S \<in> Units R
?x \<in> carrier R \<Longrightarrow> local.eval (poly_of_const ?x) ?y = ?x

goal (1 subgoal):
 1. finprod R (a_minus R x) S \<otimes> local.eval (poly_of_const (inv finprod R (a_minus R x) S)) x = \<one>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finprod R (a_minus R x) S \<otimes> local.eval (poly_of_const (inv finprod R (a_minus R x) S)) x = \<one>

goal (4 subgoals):
 1. local.eval (lagrange_basis_polynomial S x) x = \<one>
 2. degree (lagrange_basis_polynomial S x) \<le> card S
 3. \<And>s. s \<in> S \<Longrightarrow> local.eval (lagrange_basis_polynomial S x) s = \<zero>
 4. lagrange_basis_polynomial S x \<in> carrier (poly_ring R)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
local.eval (lagrange_basis_polynomial S x) x = \<one>
[PROOF STEP]
show "eval (lagrange_basis_polynomial S x) x = \<one>"
[PROOF STATE]
proof (prove)
using this:
local.eval (lagrange_basis_polynomial S x) x = \<one>

goal (1 subgoal):
 1. local.eval (lagrange_basis_polynomial S x) x = \<one>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
local.eval (lagrange_basis_polynomial S x) x = \<one>

goal (3 subgoals):
 1. degree (lagrange_basis_polynomial S x) \<le> card S
 2. \<And>s. s \<in> S \<Longrightarrow> local.eval (lagrange_basis_polynomial S x) s = \<zero>
 3. lagrange_basis_polynomial S x \<in> carrier (poly_ring R)
[PROOF STEP]
have "degree (lagrange_basis_polynomial S x) \<le> degree p + degree (poly_of_const (inv finprod R (a_minus R x) S))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (lagrange_basis_polynomial S x) \<le> degree p + degree (poly_of_const (inv finprod R (a_minus R x) S))
[PROOF STEP]
unfolding lagrange_basis_polynomial_def p_def[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (p \<otimes>\<^bsub>poly_ring R\<^esub> poly_of_const (inv finprod R (a_minus R x) S)) \<le> degree p + degree (poly_of_const (inv finprod R (a_minus R x) S))
[PROOF STEP]
using poly_mult_degree_le[OF b] poly_of_const_in_carrier Units_inv_closed c
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?y \<in> carrier (poly_ring R); degree p \<le> ?n; degree ?y \<le> ?m\<rbrakk> \<Longrightarrow> degree (p \<otimes>\<^bsub>poly_ring R\<^esub> ?y) \<le> ?n + ?m
?s \<in> carrier R \<Longrightarrow> poly_of_const ?s \<in> carrier (poly_ring R)
?x \<in> Units R \<Longrightarrow> inv ?x \<in> carrier R
finprod R (a_minus R x) S \<in> Units R

goal (1 subgoal):
 1. degree (p \<otimes>\<^bsub>poly_ring R\<^esub> poly_of_const (inv finprod R (a_minus R x) S)) \<le> degree p + degree (poly_of_const (inv finprod R (a_minus R x) S))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
degree (lagrange_basis_polynomial S x) \<le> degree p + degree (poly_of_const (inv finprod R (a_minus R x) S))

goal (3 subgoals):
 1. degree (lagrange_basis_polynomial S x) \<le> card S
 2. \<And>s. s \<in> S \<Longrightarrow> local.eval (lagrange_basis_polynomial S x) s = \<zero>
 3. lagrange_basis_polynomial S x \<in> carrier (poly_ring R)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
degree (lagrange_basis_polynomial S x) \<le> degree p + degree (poly_of_const (inv finprod R (a_minus R x) S))

goal (3 subgoals):
 1. degree (lagrange_basis_polynomial S x) \<le> card S
 2. \<And>s. s \<in> S \<Longrightarrow> local.eval (lagrange_basis_polynomial S x) s = \<zero>
 3. lagrange_basis_polynomial S x \<in> carrier (poly_ring R)
[PROOF STEP]
have "... \<le> card S + 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree p + degree (poly_of_const (inv finprod R (a_minus R x) S)) \<le> card S + 0
[PROOF STEP]
using add_mono lagrange_aux_degree[OF assms(1) assms(2)] p_def poly_of_const_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?a \<le> ?b; ?c \<le> ?d\<rbrakk> \<Longrightarrow> ?a + ?c \<le> ?b + ?d
degree (lagrange_basis_polynomial_aux S) \<le> card S
p = lagrange_basis_polynomial_aux S
poly_of_const = (\<lambda>k. local.normalize [k])

goal (1 subgoal):
 1. degree p + degree (poly_of_const (inv finprod R (a_minus R x) S)) \<le> card S + 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
degree p + degree (poly_of_const (inv finprod R (a_minus R x) S)) \<le> card S + 0

goal (3 subgoals):
 1. degree (lagrange_basis_polynomial S x) \<le> card S
 2. \<And>s. s \<in> S \<Longrightarrow> local.eval (lagrange_basis_polynomial S x) s = \<zero>
 3. lagrange_basis_polynomial S x \<in> carrier (poly_ring R)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
degree (lagrange_basis_polynomial S x) \<le> card S + 0
[PROOF STEP]
show "degree (lagrange_basis_polynomial S x) \<le> card S"
[PROOF STATE]
proof (prove)
using this:
degree (lagrange_basis_polynomial S x) \<le> card S + 0

goal (1 subgoal):
 1. degree (lagrange_basis_polynomial S x) \<le> card S
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
degree (lagrange_basis_polynomial S x) \<le> card S

goal (2 subgoals):
 1. \<And>s. s \<in> S \<Longrightarrow> local.eval (lagrange_basis_polynomial S x) s = \<zero>
 2. lagrange_basis_polynomial S x \<in> carrier (poly_ring R)
[PROOF STEP]
show "\<And>s. s \<in> S \<Longrightarrow> eval (lagrange_basis_polynomial S x) s = \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. s \<in> S \<Longrightarrow> local.eval (lagrange_basis_polynomial S x) s = \<zero>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s. s \<in> S \<Longrightarrow> local.eval (lagrange_basis_polynomial S x) s = \<zero>
[PROOF STEP]
fix s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s. s \<in> S \<Longrightarrow> local.eval (lagrange_basis_polynomial S x) s = \<zero>
[PROOF STEP]
assume d:"s \<in> S"
[PROOF STATE]
proof (state)
this:
s \<in> S

goal (1 subgoal):
 1. \<And>s. s \<in> S \<Longrightarrow> local.eval (lagrange_basis_polynomial S x) s = \<zero>
[PROOF STEP]
interpret s:ring_hom_cring "poly_ring R" "R" "(\<lambda>p. eval p s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring_hom_cring (poly_ring R) R (\<lambda>p. local.eval p s)
[PROOF STEP]
using eval_cring_hom carrier_is_subring assms d
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>subring ?K R; ?a \<in> carrier R\<rbrakk> \<Longrightarrow> ring_hom_cring (?K [X]) R (\<lambda>p. local.eval p ?a)
subring (carrier R) R
finite S
S \<subseteq> carrier R
x \<in> carrier R - S
s \<in> S

goal (1 subgoal):
 1. ring_hom_cring (poly_ring R) R (\<lambda>p. local.eval p s)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s. s \<in> S \<Longrightarrow> local.eval (lagrange_basis_polynomial S x) s = \<zero>
[PROOF STEP]
have "eval p s = finprod R (a_minus R s) S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.eval p s = finprod R (a_minus R s) S
[PROOF STEP]
using subsetD[OF assms(2) d] assms
[PROOF STATE]
proof (prove)
using this:
s \<in> carrier R
finite S
S \<subseteq> carrier R
x \<in> carrier R - S

goal (1 subgoal):
 1. local.eval p s = finprod R (a_minus R s) S
[PROOF STEP]
by (simp add:p_def lagrange_aux_eval)
[PROOF STATE]
proof (state)
this:
local.eval p s = finprod R (a_minus R s) S

goal (1 subgoal):
 1. \<And>s. s \<in> S \<Longrightarrow> local.eval (lagrange_basis_polynomial S x) s = \<zero>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
local.eval p s = finprod R (a_minus R s) S

goal (1 subgoal):
 1. \<And>s. s \<in> S \<Longrightarrow> local.eval (lagrange_basis_polynomial S x) s = \<zero>
[PROOF STEP]
have "... = \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finprod R (a_minus R s) S = \<zero>
[PROOF STEP]
using subsetD[OF assms(2)] d assms
[PROOF STATE]
proof (prove)
using this:
?c \<in> S \<Longrightarrow> ?c \<in> carrier R
s \<in> S
finite S
S \<subseteq> carrier R
x \<in> carrier R - S

goal (1 subgoal):
 1. finprod R (a_minus R s) S = \<zero>
[PROOF STEP]
by (simp add: finprod_zero_iff)
[PROOF STATE]
proof (state)
this:
finprod R (a_minus R s) S = \<zero>

goal (1 subgoal):
 1. \<And>s. s \<in> S \<Longrightarrow> local.eval (lagrange_basis_polynomial S x) s = \<zero>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
local.eval p s = \<zero>
[PROOF STEP]
have "eval p s = \<zero>\<^bsub>R\<^esub>"
[PROOF STATE]
proof (prove)
using this:
local.eval p s = \<zero>

goal (1 subgoal):
 1. local.eval p s = \<zero>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
local.eval p s = \<zero>

goal (1 subgoal):
 1. \<And>s. s \<in> S \<Longrightarrow> local.eval (lagrange_basis_polynomial S x) s = \<zero>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
local.eval p s = \<zero>

goal (1 subgoal):
 1. \<And>s. s \<in> S \<Longrightarrow> local.eval (lagrange_basis_polynomial S x) s = \<zero>
[PROOF STEP]
have "eval (poly_of_const (inv finprod R (a_minus R x) S)) s \<in> carrier R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.eval (poly_of_const (inv finprod R (a_minus R x) S)) s \<in> carrier R
[PROOF STEP]
using s.hom_closed poly_of_const_in_carrier  Units_inv_closed c
[PROOF STATE]
proof (prove)
using this:
?x \<in> carrier (poly_ring R) \<Longrightarrow> local.eval ?x s \<in> carrier R
?s \<in> carrier R \<Longrightarrow> poly_of_const ?s \<in> carrier (poly_ring R)
?x \<in> Units R \<Longrightarrow> inv ?x \<in> carrier R
finprod R (a_minus R x) S \<in> Units R

goal (1 subgoal):
 1. local.eval (poly_of_const (inv finprod R (a_minus R x) S)) s \<in> carrier R
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
local.eval (poly_of_const (inv finprod R (a_minus R x) S)) s \<in> carrier R

goal (1 subgoal):
 1. \<And>s. s \<in> S \<Longrightarrow> local.eval (lagrange_basis_polynomial S x) s = \<zero>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
local.eval p s = \<zero>
local.eval (poly_of_const (inv finprod R (a_minus R x) S)) s \<in> carrier R
[PROOF STEP]
show "eval (lagrange_basis_polynomial S x) s = \<zero>"
[PROOF STATE]
proof (prove)
using this:
local.eval p s = \<zero>
local.eval (poly_of_const (inv finprod R (a_minus R x) S)) s \<in> carrier R

goal (1 subgoal):
 1. local.eval (lagrange_basis_polynomial S x) s = \<zero>
[PROOF STEP]
using poly_of_const_in_carrier Units_inv_closed c
[PROOF STATE]
proof (prove)
using this:
local.eval p s = \<zero>
local.eval (poly_of_const (inv finprod R (a_minus R x) S)) s \<in> carrier R
?s \<in> carrier R \<Longrightarrow> poly_of_const ?s \<in> carrier (poly_ring R)
?x \<in> Units R \<Longrightarrow> inv ?x \<in> carrier R
finprod R (a_minus R x) S \<in> Units R

goal (1 subgoal):
 1. local.eval (lagrange_basis_polynomial S x) s = \<zero>
[PROOF STEP]
by (simp add:lagrange_basis_polynomial_def Let_def p_def[symmetric] s.hom_mult[OF b])
[PROOF STATE]
proof (state)
this:
local.eval (lagrange_basis_polynomial S x) s = \<zero>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?s \<in> S \<Longrightarrow> local.eval (lagrange_basis_polynomial S x) ?s = \<zero>

goal (1 subgoal):
 1. lagrange_basis_polynomial S x \<in> carrier (poly_ring R)
[PROOF STEP]
interpret r:cring "poly_ring R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cring (poly_ring R)
[PROOF STEP]
using carrier_is_subring domain.univ_poly_is_cring domain_axioms
[PROOF STATE]
proof (prove)
using this:
subring (carrier R) R
\<lbrakk>domain ?R; subring ?K ?R\<rbrakk> \<Longrightarrow> cring (?K [X]\<^bsub>?R\<^esub>)
domain R

goal (1 subgoal):
 1. cring (poly_ring R)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lagrange_basis_polynomial S x \<in> carrier (poly_ring R)
[PROOF STEP]
show "lagrange_basis_polynomial S x \<in> carrier (poly_ring R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lagrange_basis_polynomial S x \<in> carrier (poly_ring R)
[PROOF STEP]
using lagrange_basis_polynomial_def p_def[symmetric] poly_of_const_in_carrier Units_inv_closed
      a b c
[PROOF STATE]
proof (prove)
using this:
lagrange_basis_polynomial ?S ?x = lagrange_basis_polynomial_aux ?S \<otimes>\<^bsub>poly_ring R\<^esub> poly_of_const (inv finprod R (a_minus R ?x) ?S)
lagrange_basis_polynomial_aux S = p
?s \<in> carrier R \<Longrightarrow> poly_of_const ?s \<in> carrier (poly_ring R)
?x \<in> Units R \<Longrightarrow> inv ?x \<in> carrier R
local.eval p x = finprod R (a_minus R x) S
p \<in> carrier (poly_ring R)
finprod R (a_minus R x) S \<in> Units R

goal (1 subgoal):
 1. lagrange_basis_polynomial S x \<in> carrier (poly_ring R)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lagrange_basis_polynomial S x \<in> carrier (poly_ring R)

goal:
No subgoals!
[PROOF STEP]
qed