[STATEMENT]
lemma finite_dec_above_ne: "finite {x. f x \<noteq> c} \<Longrightarrow> finite {x. f (dec_above b i x) \<noteq> c}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {x. f x \<noteq> c} \<Longrightarrow> finite {x. f (dec_above b i x) \<noteq> c}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite {x. f x \<noteq> c} \<Longrightarrow> finite {x. f (dec_above b i x) \<noteq> c}
[PROOF STEP]
fix b and f::"nat\<Rightarrow>'a"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite {x. f x \<noteq> c} \<Longrightarrow> finite {x. f (dec_above b i x) \<noteq> c}
[PROOF STEP]
assume f: "finite {x. f x \<noteq> c}"
[PROOF STATE]
proof (state)
this:
finite {x. f x \<noteq> c}

goal (1 subgoal):
 1. finite {x. f x \<noteq> c} \<Longrightarrow> finite {x. f (dec_above b i x) \<noteq> c}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite {x. f x \<noteq> c}

goal (1 subgoal):
 1. finite {x. f x \<noteq> c} \<Longrightarrow> finite {x. f (dec_above b i x) \<noteq> c}
[PROOF STEP]
have "finite {x. f (x - i) \<noteq> c}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {x. f (x - i) \<noteq> c}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite {x. f (x - i) \<noteq> c}
[PROOF STEP]
have "{x. f (x - i) \<noteq> c} \<subseteq> {0..i} \<union> ((\<lambda>x. x - i) -` {x. f x \<noteq> c} \<inter> {i<..})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x. f (x - i) \<noteq> c} \<subseteq> {0..i} \<union> (\<lambda>x. x - i) -` {x. f x \<noteq> c} \<inter> {i<..}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{x. f (x - i) \<noteq> c} \<subseteq> {0..i} \<union> (\<lambda>x. x - i) -` {x. f x \<noteq> c} \<inter> {i<..}

goal (1 subgoal):
 1. finite {x. f (x - i) \<noteq> c}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
{x. f (x - i) \<noteq> c} \<subseteq> {0..i} \<union> (\<lambda>x. x - i) -` {x. f x \<noteq> c} \<inter> {i<..}

goal (1 subgoal):
 1. finite {x. f (x - i) \<noteq> c}
[PROOF STEP]
have "finite \<dots>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite ({0..i} \<union> (\<lambda>x. x - i) -` {x. f x \<noteq> c} \<inter> {i<..})
[PROOF STEP]
apply (rule finite_UnI[OF finite_atLeastAtMost])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite ((\<lambda>x. x - i) -` {x. f x \<noteq> c} \<inter> {i<..})
[PROOF STEP]
by (rule finite_vimage_IntI) (use f in \<open>auto simp: inj_on_def\<close>)
[PROOF STATE]
proof (state)
this:
finite ({0..i} \<union> (\<lambda>x. x - i) -` {x. f x \<noteq> c} \<inter> {i<..})

goal (1 subgoal):
 1. finite {x. f (x - i) \<noteq> c}
[PROOF STEP]
finally (finite_subset)
[PROOF STATE]
proof (chain)
picking this:
finite {x. f (x - i) \<noteq> c}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite {x. f (x - i) \<noteq> c}

goal (1 subgoal):
 1. finite {x. f (x - i) \<noteq> c}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
finite {x. f (x - i) \<noteq> c}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
finite {x. f (x - i) \<noteq> c}

goal (1 subgoal):
 1. finite {x. f x \<noteq> c} \<Longrightarrow> finite {x. f (dec_above b i x) \<noteq> c}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
finite {x. f x \<noteq> c}
finite {x. f (x - i) \<noteq> c}
[PROOF STEP]
have "finite ({x. f x \<noteq> c} \<union> {x. f (x - i) \<noteq> c} \<union> {b})"
[PROOF STATE]
proof (prove)
using this:
finite {x. f x \<noteq> c}
finite {x. f (x - i) \<noteq> c}

goal (1 subgoal):
 1. finite ({x. f x \<noteq> c} \<union> {x. f (x - i) \<noteq> c} \<union> {b})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite ({x. f x \<noteq> c} \<union> {x. f (x - i) \<noteq> c} \<union> {b})

goal (1 subgoal):
 1. finite {x. f x \<noteq> c} \<Longrightarrow> finite {x. f (dec_above b i x) \<noteq> c}
[PROOF STEP]
from _ this
[PROOF STATE]
proof (chain)
picking this:
PROP ?psi \<Longrightarrow> PROP ?psi
finite ({x. f x \<noteq> c} \<union> {x. f (x - i) \<noteq> c} \<union> {b})
[PROOF STEP]
show "finite {x. f (dec_above b i x) \<noteq> c}"
[PROOF STATE]
proof (prove)
using this:
PROP ?psi \<Longrightarrow> PROP ?psi
finite ({x. f x \<noteq> c} \<union> {x. f (x - i) \<noteq> c} \<union> {b})

goal (1 subgoal):
 1. finite {x. f (dec_above b i x) \<noteq> c}
[PROOF STEP]
by (rule finite_subset) (auto simp: dec_above_def)
[PROOF STATE]
proof (state)
this:
finite {x. f (dec_above b i x) \<noteq> c}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma higherPowers_lowerPowers: "higherPowers n i (lowerPowers n i x) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higherPowers n i (lowerPowers n i x) = x
[PROOF STEP]
by transfer (force simp: dec_above_def inc_above_def antisym_conv2)


[STATEMENT]
lemma inj_lowerPowers: "inj (lowerPowers b i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj (lowerPowers b i)
[PROOF STEP]
using higherPowers_lowerPowers
[PROOF STATE]
proof (prove)
using this:
higherPowers ?n ?i (lowerPowers ?n ?i ?x) = ?x

goal (1 subgoal):
 1. inj (lowerPowers b i)
[PROOF STEP]
by (rule inj_on_inverseI)


[STATEMENT]
lemma lowerPowers_higherPowers:
  "(\<And>j. n \<le> j \<Longrightarrow> j < n + i \<Longrightarrow> lookup x j = 0) \<Longrightarrow> lowerPowers n i (higherPowers n i x) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>j. \<lbrakk>n \<le> j; j < n + i\<rbrakk> \<Longrightarrow> lookup x j = (0::'a)) \<Longrightarrow> lowerPowers n i (higherPowers n i x) = x
[PROOF STEP]
by (transfer fixing: n i) (force simp: inc_above_dec_above)


[STATEMENT]
lemma inj_on_higherPowers: "inj_on (higherPowers n i) {x. \<forall>j. n \<le> j \<and> j < n + i \<longrightarrow> lookup x j = 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (higherPowers n i) {x. \<forall>j. n \<le> j \<and> j < n + i \<longrightarrow> lookup x j = (0::'a)}
[PROOF STEP]
using lowerPowers_higherPowers
[PROOF STATE]
proof (prove)
using this:
(\<And>j. \<lbrakk>?n \<le> j; j < ?n + ?i\<rbrakk> \<Longrightarrow> lookup ?x j = (0::?'a)) \<Longrightarrow> lowerPowers ?n ?i (higherPowers ?n ?i ?x) = ?x

goal (1 subgoal):
 1. inj_on (higherPowers n i) {x. \<forall>j. n \<le> j \<and> j < n + i \<longrightarrow> lookup x j = (0::'a)}
[PROOF STEP]
by (rule inj_on_inverseI) auto


[STATEMENT]
lemma higherPowers_eq: "lookup (higherPowers b i p) x = lookup p (inc_above b i x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup (higherPowers b i p) x = lookup p (inc_above b i x)
[PROOF STEP]
by (simp_all add: higherPowers.rep_eq)


[STATEMENT]
lemma lowerPowers_eq: "lookup (lowerPowers b i p) x = (if b \<le> x \<and> x < b + i then 0 else lookup p (dec_above b i x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup (lowerPowers b i p) x = (if b \<le> x \<and> x < b + i then 0::'a else lookup p (dec_above b i x))
[PROOF STEP]
by (auto simp add: lowerPowers.rep_eq)


[STATEMENT]
lemma keys_higherPowers: "keys (higherPowers b i m) = dec_above b i ` (keys m \<inter> {x. x \<notin> {b..<b+i}})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. keys (higherPowers b i m) = dec_above b i ` (keys m \<inter> {x. x \<notin> {b..<b + i}})
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> keys (higherPowers b i m) \<Longrightarrow> x \<in> dec_above b i ` (keys m \<inter> {x. x \<notin> {b..<b + i}})
 2. \<And>x xa. \<lbrakk>xa \<in> keys m; xa \<notin> {b..<b + i}\<rbrakk> \<Longrightarrow> dec_above b i xa \<in> keys (higherPowers b i m)
[PROOF STEP]
subgoal for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> keys (higherPowers b i m) \<Longrightarrow> x \<in> dec_above b i ` (keys m \<inter> {x. x \<notin> {b..<b + i}})
[PROOF STEP]
apply (rule image_eqI[where x="inc_above b i x"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. x \<in> keys (higherPowers b i m) \<Longrightarrow> x = dec_above b i (inc_above b i x)
 2. x \<in> keys (higherPowers b i m) \<Longrightarrow> inc_above b i x \<in> keys m \<inter> {x. x \<notin> {b..<b + i}}
[PROOF STEP]
apply (auto simp: dec_above_inc_above in_keys_iff higherPowers.rep_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>lookup m (inc_above b i x) \<noteq> (0::'a); b \<le> inc_above b i x; inc_above b i x < b + i\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by (metis add_less_cancel_right inc_above_def leD)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>xa \<in> keys m; xa \<notin> {b..<b + i}\<rbrakk> \<Longrightarrow> dec_above b i xa \<in> keys (higherPowers b i m)
[PROOF STEP]
subgoal for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xa_ \<in> keys m; xa_ \<notin> {b..<b + i}\<rbrakk> \<Longrightarrow> dec_above b i xa_ \<in> keys (higherPowers b i m)
[PROOF STEP]
by (auto simp: inc_above_dec_above in_keys_iff higherPowers.rep_eq)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma map_of_map_key_inverse_fun_eq:
  "map_of (map (\<lambda>(k, y). (f k, y)) xs) x = map_of xs (g x)"
  if "\<And>x. x \<in> set xs \<Longrightarrow> g (f (fst x)) = fst x" "f (g x) = x"
  for f::"'a \<Rightarrow> 'b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_of (map (\<lambda>(k, y). (f k, y)) xs) x = map_of xs (g x)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
?x \<in> set xs \<Longrightarrow> g (f (fst ?x)) = fst ?x
f (g x) = x

goal (1 subgoal):
 1. map_of (map (\<lambda>(k, y). (f k, y)) xs) x = map_of xs (g x)
[PROOF STEP]
proof (induction xs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>x. x \<in> set [] \<Longrightarrow> g (f (fst x)) = fst x; f (g x) = x\<rbrakk> \<Longrightarrow> map_of (map (\<lambda>(k, y). (f k, y)) []) x = map_of [] (g x)
 2. \<And>a xs. \<lbrakk>\<lbrakk>\<And>x. x \<in> set xs \<Longrightarrow> g (f (fst x)) = fst x; f (g x) = x\<rbrakk> \<Longrightarrow> map_of (map (\<lambda>(k, y). (f k, y)) xs) x = map_of xs (g x); \<And>x. x \<in> set (a # xs) \<Longrightarrow> g (f (fst x)) = fst x; f (g x) = x\<rbrakk> \<Longrightarrow> map_of (map (\<lambda>(k, y). (f k, y)) (a # xs)) x = map_of (a # xs) (g x)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
?x \<in> set [] \<Longrightarrow> g (f (fst ?x)) = fst ?x
f (g x) = x

goal (2 subgoals):
 1. \<lbrakk>\<And>x. x \<in> set [] \<Longrightarrow> g (f (fst x)) = fst x; f (g x) = x\<rbrakk> \<Longrightarrow> map_of (map (\<lambda>(k, y). (f k, y)) []) x = map_of [] (g x)
 2. \<And>a xs. \<lbrakk>\<lbrakk>\<And>x. x \<in> set xs \<Longrightarrow> g (f (fst x)) = fst x; f (g x) = x\<rbrakk> \<Longrightarrow> map_of (map (\<lambda>(k, y). (f k, y)) xs) x = map_of xs (g x); \<And>x. x \<in> set (a # xs) \<Longrightarrow> g (f (fst x)) = fst x; f (g x) = x\<rbrakk> \<Longrightarrow> map_of (map (\<lambda>(k, y). (f k, y)) (a # xs)) x = map_of (a # xs) (g x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?x \<in> set [] \<Longrightarrow> g (f (fst ?x)) = fst ?x
f (g x) = x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
?x \<in> set [] \<Longrightarrow> g (f (fst ?x)) = fst ?x
f (g x) = x

goal (1 subgoal):
 1. map_of (map (\<lambda>a. case a of (k, a) \<Rightarrow> (f k, a)) []) x = map_of [] (g x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
map_of (map (\<lambda>a. case a of (k, a) \<Rightarrow> (f k, a)) []) x = map_of [] (g x)

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>\<lbrakk>\<And>x. x \<in> set xs \<Longrightarrow> g (f (fst x)) = fst x; f (g x) = x\<rbrakk> \<Longrightarrow> map_of (map (\<lambda>(k, y). (f k, y)) xs) x = map_of xs (g x); \<And>x. x \<in> set (a # xs) \<Longrightarrow> g (f (fst x)) = fst x; f (g x) = x\<rbrakk> \<Longrightarrow> map_of (map (\<lambda>(k, y). (f k, y)) (a # xs)) x = map_of (a # xs) (g x)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>\<lbrakk>\<And>x. x \<in> set xs \<Longrightarrow> g (f (fst x)) = fst x; f (g x) = x\<rbrakk> \<Longrightarrow> map_of (map (\<lambda>(k, y). (f k, y)) xs) x = map_of xs (g x); \<And>x. x \<in> set (a # xs) \<Longrightarrow> g (f (fst x)) = fst x; f (g x) = x\<rbrakk> \<Longrightarrow> map_of (map (\<lambda>(k, y). (f k, y)) (a # xs)) x = map_of (a # xs) (g x)
[PROOF STEP]
case (Cons a xs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<And>x. x \<in> set xs \<Longrightarrow> g (f (fst x)) = fst x; f (g x) = x\<rbrakk> \<Longrightarrow> map_of (map (\<lambda>a. case a of (k, a) \<Rightarrow> (f k, a)) xs) x = map_of xs (g x)
?x \<in> set (a # xs) \<Longrightarrow> g (f (fst ?x)) = fst ?x
f (g x) = x

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>\<lbrakk>\<And>x. x \<in> set xs \<Longrightarrow> g (f (fst x)) = fst x; f (g x) = x\<rbrakk> \<Longrightarrow> map_of (map (\<lambda>(k, y). (f k, y)) xs) x = map_of xs (g x); \<And>x. x \<in> set (a # xs) \<Longrightarrow> g (f (fst x)) = fst x; f (g x) = x\<rbrakk> \<Longrightarrow> map_of (map (\<lambda>(k, y). (f k, y)) (a # xs)) x = map_of (a # xs) (g x)
[PROOF STEP]
from Cons
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<And>x. x \<in> set xs \<Longrightarrow> g (f (fst x)) = fst x; f (g x) = x\<rbrakk> \<Longrightarrow> map_of (map (\<lambda>a. case a of (k, a) \<Rightarrow> (f k, a)) xs) x = map_of xs (g x)
?x \<in> set (a # xs) \<Longrightarrow> g (f (fst ?x)) = fst ?x
f (g x) = x
[PROOF STEP]
have IH: "map_of (map (\<lambda>a. (f (fst a), snd a)) xs) x = map_of xs (g x)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>x. x \<in> set xs \<Longrightarrow> g (f (fst x)) = fst x; f (g x) = x\<rbrakk> \<Longrightarrow> map_of (map (\<lambda>a. case a of (k, a) \<Rightarrow> (f k, a)) xs) x = map_of xs (g x)
?x \<in> set (a # xs) \<Longrightarrow> g (f (fst ?x)) = fst ?x
f (g x) = x

goal (1 subgoal):
 1. map_of (map (\<lambda>a. (f (fst a), snd a)) xs) x = map_of xs (g x)
[PROOF STEP]
by (auto simp: split_beta')
[PROOF STATE]
proof (state)
this:
map_of (map (\<lambda>a. (f (fst a), snd a)) xs) x = map_of xs (g x)

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>\<lbrakk>\<And>x. x \<in> set xs \<Longrightarrow> g (f (fst x)) = fst x; f (g x) = x\<rbrakk> \<Longrightarrow> map_of (map (\<lambda>(k, y). (f k, y)) xs) x = map_of xs (g x); \<And>x. x \<in> set (a # xs) \<Longrightarrow> g (f (fst x)) = fst x; f (g x) = x\<rbrakk> \<Longrightarrow> map_of (map (\<lambda>(k, y). (f k, y)) (a # xs)) x = map_of (a # xs) (g x)
[PROOF STEP]
have inv_into: "g (f (fst a)) = fst a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g (f (fst a)) = fst a
[PROOF STEP]
by (rule Cons) simp
[PROOF STATE]
proof (state)
this:
g (f (fst a)) = fst a

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>\<lbrakk>\<And>x. x \<in> set xs \<Longrightarrow> g (f (fst x)) = fst x; f (g x) = x\<rbrakk> \<Longrightarrow> map_of (map (\<lambda>(k, y). (f k, y)) xs) x = map_of xs (g x); \<And>x. x \<in> set (a # xs) \<Longrightarrow> g (f (fst x)) = fst x; f (g x) = x\<rbrakk> \<Longrightarrow> map_of (map (\<lambda>(k, y). (f k, y)) (a # xs)) x = map_of (a # xs) (g x)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_of (map (\<lambda>a. case a of (k, a) \<Rightarrow> (f k, a)) (a # xs)) x = map_of (a # xs) (g x)
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>x. x \<in> set xs \<Longrightarrow> g (f (fst x)) = fst x; f (g x) = x\<rbrakk> \<Longrightarrow> map_of (map (\<lambda>a. case a of (k, a) \<Rightarrow> (f k, a)) xs) x = map_of xs (g x)
?x \<in> set (a # xs) \<Longrightarrow> g (f (fst ?x)) = fst ?x
f (g x) = x

goal (1 subgoal):
 1. map_of (map (\<lambda>a. case a of (k, a) \<Rightarrow> (f k, a)) (a # xs)) x = map_of (a # xs) (g x)
[PROOF STEP]
by (auto simp add: split_beta' inv_into IH)
[PROOF STATE]
proof (state)
this:
map_of (map (\<lambda>a. case a of (k, a) \<Rightarrow> (f k, a)) (a # xs)) x = map_of (a # xs) (g x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma map_of_filter_key_in: "P x \<Longrightarrow> map_of (filter (\<lambda>(k, v). P k) xs) x = map_of xs x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P x \<Longrightarrow> map_of (filter (\<lambda>(k, v). P k) xs) x = map_of xs x
[PROOF STEP]
by (induction xs) auto


[STATEMENT]
lemma map_of_eq_NoneI: "x\<notin>fst`set xs \<Longrightarrow> map_of xs x = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<notin> fst ` set xs \<Longrightarrow> map_of xs x = None
[PROOF STEP]
by (induction xs) auto


[STATEMENT]
lemma compute_higherPowers\<^sub>f[code]: "higherPowers\<^sub>f b i (fmap_of_list xs) =
  fmap_of_list (map (\<lambda>(k, v). (if k < b then k else k - i, v)) (filter (\<lambda>(k, v). k \<notin> {b..<b+i}) xs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higherPowers\<^sub>f b i (fmap_of_list xs) = fmap_of_list (map (\<lambda>(k, v). (if k < b then k else k - i, v)) (filter (\<lambda>(k, v). k \<notin> {b..<b + i}) xs))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. higherPowers\<^sub>f b i (fmap_of_list xs) = fmap_of_list (map (\<lambda>(k, v). (if k < b then k else k - i, v)) (filter (\<lambda>(k, v). k \<notin> {b..<b + i}) xs))
[PROOF STEP]
have *: "map_of (map (\<lambda>(k, y). (if k < b then k else k - i, y)) (filter (\<lambda>(k, v).  b \<le> k \<longrightarrow> \<not> k < b + i) xs)) x =
    map_of (filter (\<lambda>(k, v).  b \<le> k \<longrightarrow> \<not> k < b + i) xs) (if x < b then x else x + i)"
    for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_of (map (\<lambda>(k, y). (if k < b then k else k - i, y)) (filter (\<lambda>(k, v). b \<le> k \<longrightarrow> \<not> k < b + i) xs)) x = map_of (filter (\<lambda>(k, v). b \<le> k \<longrightarrow> \<not> k < b + i) xs) (if x < b then x else x + i)
[PROOF STEP]
by (rule map_of_map_key_inverse_fun_eq[where g="\<lambda>k. if k < b then k else k + i"
          and f = "\<lambda>k. if k < b then k else k - i"]) auto
[PROOF STATE]
proof (state)
this:
map_of (map (\<lambda>(k, y). (if k < b then k else k - i, y)) (filter (\<lambda>(k, v). b \<le> k \<longrightarrow> \<not> k < b + i) xs)) ?x = map_of (filter (\<lambda>(k, v). b \<le> k \<longrightarrow> \<not> k < b + i) xs) (if ?x < b then ?x else ?x + i)

goal (1 subgoal):
 1. higherPowers\<^sub>f b i (fmap_of_list xs) = fmap_of_list (map (\<lambda>(k, v). (if k < b then k else k - i, v)) (filter (\<lambda>(k, v). k \<notin> {b..<b + i}) xs))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higherPowers\<^sub>f b i (fmap_of_list xs) = fmap_of_list (map (\<lambda>(k, v). (if k < b then k else k - i, v)) (filter (\<lambda>(k, v). k \<notin> {b..<b + i}) xs))
[PROOF STEP]
by (auto
        simp add: * higherPowers\<^sub>f.rep_eq lowerPowers\<^sub>f.rep_eq fmlookup_of_list fmlookup_default_def
        inc_above_def
        map_of_filter_key_in
        split: option.splits
        intro!: fmap_ext)
[PROOF STATE]
proof (state)
this:
higherPowers\<^sub>f b i (fmap_of_list xs) = fmap_of_list (map (\<lambda>(k, v). (if k < b then k else k - i, v)) (filter (\<lambda>(k, v). k \<notin> {b..<b + i}) xs))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma compute_lowerPowers\<^sub>f[code]: "lowerPowers\<^sub>f b i (fmap_of_list xs) =
  fmap_of_list (map (\<lambda>(k, v). (if k < b then k else k + i, v)) xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lowerPowers\<^sub>f b i (fmap_of_list xs) = fmap_of_list (map (\<lambda>(k, v). (if k < b then k else k + i, v)) xs)
[PROOF STEP]
apply (auto
      simp add: lowerPowers\<^sub>f.rep_eq fmlookup_of_list fmlookup_default_def
      dec_above_def
      map_of_filter_key_in
      split: option.splits
      intro!: fmap_ext)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. 0 < i \<Longrightarrow> None = map_of (map (\<lambda>(k, y). (if k < b then k else k + i, y)) xs) b
 2. \<And>x. \<lbrakk>x \<le> b; b \<noteq> x\<rbrakk> \<Longrightarrow> map_of xs x = map_of (map (\<lambda>(k, y). (if k < b then k else k + i, y)) xs) x
 3. \<And>x. \<lbrakk>x \<le> b; i = 0\<rbrakk> \<Longrightarrow> map_of xs x = map_of (map (\<lambda>(k, y). (if k < b then k else k + 0, y)) xs) x
 4. \<And>x. \<lbrakk>\<not> x \<le> b; x < b + i\<rbrakk> \<Longrightarrow> None = map_of (map (\<lambda>(k, y). (if k < b then k else k + i, y)) xs) x
 5. \<And>x. \<lbrakk>\<not> x \<le> b; \<not> x < b + i\<rbrakk> \<Longrightarrow> map_of xs (x - i) = map_of (map (\<lambda>(k, y). (if k < b then k else k + i, y)) xs) x
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < i \<Longrightarrow> None = map_of (map (\<lambda>(k, y). (if k < b then k else k + i, y)) xs) b
[PROOF STEP]
by (rule map_of_eq_NoneI[symmetric]) (auto split: if_splits)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>x \<le> b; b \<noteq> x\<rbrakk> \<Longrightarrow> map_of xs x = map_of (map (\<lambda>(k, y). (if k < b then k else k + i, y)) xs) x
 2. \<And>x. \<lbrakk>x \<le> b; i = 0\<rbrakk> \<Longrightarrow> map_of xs x = map_of (map (\<lambda>(k, y). (if k < b then k else k + 0, y)) xs) x
 3. \<And>x. \<lbrakk>\<not> x \<le> b; x < b + i\<rbrakk> \<Longrightarrow> None = map_of (map (\<lambda>(k, y). (if k < b then k else k + i, y)) xs) x
 4. \<And>x. \<lbrakk>\<not> x \<le> b; \<not> x < b + i\<rbrakk> \<Longrightarrow> map_of xs (x - i) = map_of (map (\<lambda>(k, y). (if k < b then k else k + i, y)) xs) x
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x_ \<le> b; b \<noteq> x_\<rbrakk> \<Longrightarrow> map_of xs x_ = map_of (map (\<lambda>(k, y). (if k < b then k else k + i, y)) xs) x_
[PROOF STEP]
by (subst map_of_map_key_inverse_fun_eq[where g="\<lambda>k. if k < b then k else k - i"]) auto
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>x \<le> b; i = 0\<rbrakk> \<Longrightarrow> map_of xs x = map_of (map (\<lambda>(k, y). (if k < b then k else k + 0, y)) xs) x
 2. \<And>x. \<lbrakk>\<not> x \<le> b; x < b + i\<rbrakk> \<Longrightarrow> None = map_of (map (\<lambda>(k, y). (if k < b then k else k + i, y)) xs) x
 3. \<And>x. \<lbrakk>\<not> x \<le> b; \<not> x < b + i\<rbrakk> \<Longrightarrow> map_of xs (x - i) = map_of (map (\<lambda>(k, y). (if k < b then k else k + i, y)) xs) x
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x_ \<le> b; i = 0\<rbrakk> \<Longrightarrow> map_of xs x_ = map_of (map (\<lambda>(k, y). (if k < b then k else k + 0, y)) xs) x_
[PROOF STEP]
by (subst map_of_map_key_inverse_fun_eq[where g="\<lambda>k. if k < b then k else k - i"]) auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<not> x \<le> b; x < b + i\<rbrakk> \<Longrightarrow> None = map_of (map (\<lambda>(k, y). (if k < b then k else k + i, y)) xs) x
 2. \<And>x. \<lbrakk>\<not> x \<le> b; \<not> x < b + i\<rbrakk> \<Longrightarrow> map_of xs (x - i) = map_of (map (\<lambda>(k, y). (if k < b then k else k + i, y)) xs) x
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> x_ \<le> b; x_ < b + i\<rbrakk> \<Longrightarrow> None = map_of (map (\<lambda>(k, y). (if k < b then k else k + i, y)) xs) x_
[PROOF STEP]
by (rule map_of_eq_NoneI[symmetric]) (auto split: if_splits)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<not> x \<le> b; \<not> x < b + i\<rbrakk> \<Longrightarrow> map_of xs (x - i) = map_of (map (\<lambda>(k, y). (if k < b then k else k + i, y)) xs) x
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> x_ \<le> b; \<not> x_ < b + i\<rbrakk> \<Longrightarrow> map_of xs (x_ - i) = map_of (map (\<lambda>(k, y). (if k < b then k else k + i, y)) xs) x_
[PROOF STEP]
by (subst map_of_map_key_inverse_fun_eq[where g="\<lambda>k. if k < b then k else k - i"]) auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma compute_higherPowers[code]: "higherPowers n i (Pm_fmap xs) = Pm_fmap (higherPowers\<^sub>f n i xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higherPowers n i (Pm_fmap xs) = Pm_fmap (higherPowers\<^sub>f n i xs)
[PROOF STEP]
by (rule poly_mapping_eqI)
    (auto simp: higherPowers\<^sub>f.rep_eq higherPowers.rep_eq fmlookup_default_def dec_above_def
      split: option.splits)


[STATEMENT]
lemma compute_lowerPowers[code]: "lowerPowers n i (Pm_fmap xs) = Pm_fmap (lowerPowers\<^sub>f n i xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lowerPowers n i (Pm_fmap xs) = Pm_fmap (lowerPowers\<^sub>f n i xs)
[PROOF STEP]
by (rule poly_mapping_eqI)
    (auto simp: lowerPowers\<^sub>f.rep_eq lowerPowers.rep_eq fmlookup_default_def dec_above_def
      split: option.splits)


[STATEMENT]
lemma finite_nonzero_coeff: "finite {x. MPoly_Type.coeff mpoly x \<noteq> 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {x. MPoly_Type.coeff mpoly x \<noteq> (0::'a)}
[PROOF STEP]
by transfer auto


[STATEMENT]
lemma higherPowers_zero[simp]: "higherPowers b i 0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higherPowers b i 0 = 0
[PROOF STEP]
by transfer auto


[STATEMENT]
lemma keys_lowerPoly\<^sub>0: "keys (lowerPoly\<^sub>0 b i mp) = higherPowers b i ` (keys mp \<inter> {x. \<forall>j\<in>{b..<b+i}. lookup x j = 0})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. keys (lowerPoly\<^sub>0 b i mp) = higherPowers b i ` (keys mp \<inter> {x. \<forall>j\<in>{b..<b + i}. lookup x j = 0})
[PROOF STEP]
apply (auto )
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> keys (lowerPoly\<^sub>0 b i mp) \<Longrightarrow> x \<in> higherPowers b i ` (keys mp \<inter> {x. \<forall>j\<in>{b..<b + i}. lookup x j = 0})
 2. \<And>xa. \<lbrakk>xa \<in> keys mp; \<forall>j\<in>{b..<b + i}. lookup xa j = 0\<rbrakk> \<Longrightarrow> higherPowers b i xa \<in> keys (lowerPoly\<^sub>0 b i mp)
[PROOF STEP]
subgoal for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> keys (lowerPoly\<^sub>0 b i mp) \<Longrightarrow> x \<in> higherPowers b i ` (keys mp \<inter> {x. \<forall>j\<in>{b..<b + i}. lookup x j = 0})
[PROOF STEP]
apply (rule image_eqI[where x="lowerPowers b i x"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. x \<in> keys (lowerPoly\<^sub>0 b i mp) \<Longrightarrow> x = higherPowers b i (lowerPowers b i x)
 2. x \<in> keys (lowerPoly\<^sub>0 b i mp) \<Longrightarrow> lowerPowers b i x \<in> keys mp \<inter> {x. \<forall>j\<in>{b..<b + i}. lookup x j = 0}
[PROOF STEP]
apply (auto simp: higherPowers_lowerPowers in_keys_iff lowerPoly\<^sub>0.rep_eq lowerPowers.rep_eq)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>xa \<in> keys mp; \<forall>j\<in>{b..<b + i}. lookup xa j = 0\<rbrakk> \<Longrightarrow> higherPowers b i xa \<in> keys (lowerPoly\<^sub>0 b i mp)
[PROOF STEP]
subgoal for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> keys mp; \<forall>j\<in>{b..<b + i}. lookup x j = 0\<rbrakk> \<Longrightarrow> higherPowers b i x \<in> keys (lowerPoly\<^sub>0 b i mp)
[PROOF STEP]
apply (auto simp: in_keys_iff lowerPoly\<^sub>0.rep_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>lookup mp x \<noteq> (0::'a); \<forall>j\<in>{b..<b + i}. lookup x j = 0; lookup mp (lowerPowers b i (higherPowers b i x)) = (0::'a)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (subst (asm) lowerPowers_higherPowers)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>j. \<lbrakk>lookup mp x \<noteq> (0::'a); \<forall>j\<in>{b..<b + i}. lookup x j = 0; b \<le> j; j < b + i\<rbrakk> \<Longrightarrow> lookup x j = 0
 2. \<lbrakk>lookup mp x \<noteq> (0::'a); \<forall>j\<in>{b..<b + i}. lookup x j = 0; lookup mp x = (0::'a)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma keys_lowerPowers: "keys (lowerPowers b i m) = inc_above b i ` (keys m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. keys (lowerPowers b i m) = inc_above b i ` keys m
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> keys (lowerPowers b i m) \<Longrightarrow> x \<in> inc_above b i ` keys m
 2. \<And>x xa. xa \<in> keys m \<Longrightarrow> inc_above b i xa \<in> keys (lowerPowers b i m)
[PROOF STEP]
subgoal for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> keys (lowerPowers b i m) \<Longrightarrow> x \<in> inc_above b i ` keys m
[PROOF STEP]
apply (rule image_eqI[where x="dec_above b i x"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. x \<in> keys (lowerPowers b i m) \<Longrightarrow> x = inc_above b i (dec_above b i x)
 2. x \<in> keys (lowerPowers b i m) \<Longrightarrow> dec_above b i x \<in> keys m
[PROOF STEP]
apply (auto simp: inc_above_dec_above in_keys_iff lowerPowers.rep_eq)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (if b \<le> x \<and> x < b + i then 0::'a else lookup m (dec_above b i x)) \<noteq> (0::'a) \<Longrightarrow> x = inc_above b i (dec_above b i x)
 2. \<lbrakk>(if b \<le> x \<and> x < b + i then 0::'a else lookup m (dec_above b i x)) \<noteq> (0::'a); lookup m (dec_above b i x) = (0::'a)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (metis inc_above_dec_above not_less)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(if b \<le> x \<and> x < b + i then 0::'a else lookup m (dec_above b i x)) \<noteq> (0::'a); lookup m (dec_above b i x) = (0::'a)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by meson
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. xa \<in> keys m \<Longrightarrow> inc_above b i xa \<in> keys (lowerPowers b i m)
[PROOF STEP]
by (metis higherPowers.rep_eq higherPowers_lowerPowers in_keys_iff)


[STATEMENT]
lemma keys_higherPoly\<^sub>0: "keys (higherPoly\<^sub>0 b i mp) = lowerPowers b i ` (keys mp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. keys (higherPoly\<^sub>0 b i mp) = lowerPowers b i ` keys mp
[PROOF STEP]
apply (auto )
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> keys (higherPoly\<^sub>0 b i mp) \<Longrightarrow> x \<in> lowerPowers b i ` keys mp
 2. \<And>xa. xa \<in> keys mp \<Longrightarrow> lowerPowers b i xa \<in> keys (higherPoly\<^sub>0 b i mp)
[PROOF STEP]
subgoal for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> keys (higherPoly\<^sub>0 b i mp) \<Longrightarrow> x \<in> lowerPowers b i ` keys mp
[PROOF STEP]
apply (rule image_eqI[where x="higherPowers b i x"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. x \<in> keys (higherPoly\<^sub>0 b i mp) \<Longrightarrow> x = lowerPowers b i (higherPowers b i x)
 2. x \<in> keys (higherPoly\<^sub>0 b i mp) \<Longrightarrow> higherPowers b i x \<in> keys mp
[PROOF STEP]
apply (auto simp: lowerPowers_higherPowers in_keys_iff higherPoly\<^sub>0.rep_eq higherPowers.rep_eq)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (if \<exists>j\<in>{b..<b + i}. 0 < lookup x j then 0::'a else lookup mp (higherPowers b i x)) \<noteq> (0::'a) \<Longrightarrow> x = lowerPowers b i (higherPowers b i x)
 2. \<lbrakk>(if \<exists>j\<in>{b..<b + i}. 0 < lookup x j then 0::'a else lookup mp (higherPowers b i x)) \<noteq> (0::'a); lookup mp (higherPowers b i x) = (0::'a)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (metis atLeastLessThan_iff lowerPowers_higherPowers neq0_conv)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(if \<exists>j\<in>{b..<b + i}. 0 < lookup x j then 0::'a else lookup mp (higherPowers b i x)) \<noteq> (0::'a); lookup mp (higherPowers b i x) = (0::'a)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by meson
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. xa \<in> keys mp \<Longrightarrow> lowerPowers b i xa \<in> keys (higherPoly\<^sub>0 b i mp)
[PROOF STEP]
subgoal for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> keys mp \<Longrightarrow> lowerPowers b i x \<in> keys (higherPoly\<^sub>0 b i mp)
[PROOF STEP]
apply (auto simp: in_keys_iff higherPoly\<^sub>0.rep_eq)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>j. \<lbrakk>lookup mp x \<noteq> (0::'a); b \<le> j; j < b + i\<rbrakk> \<Longrightarrow> lookup (lowerPowers b i x) j = 0
 2. \<lbrakk>lookup mp x \<noteq> (0::'a); \<forall>j\<in>{b..<b + i}. lookup (lowerPowers b i x) j = 0; lookup mp (higherPowers b i (lowerPowers b i x)) = (0::'a)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (simp add: lowerPowers_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>lookup mp x \<noteq> (0::'a); \<forall>j\<in>{b..<b + i}. lookup (lowerPowers b i x) j = 0; lookup mp (higherPowers b i (lowerPowers b i x)) = (0::'a)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by (simp add: higherPowers_lowerPowers)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma inc_above_id[simp]: "n < m \<Longrightarrow> inc_above m i n = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < m \<Longrightarrow> inc_above m i n = n
[PROOF STEP]
by (auto simp: inc_above_def)


[STATEMENT]
lemma inc_above_Suc[simp]: "n \<ge> m \<Longrightarrow> inc_above m i n = n + i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m \<le> n \<Longrightarrow> inc_above m i n = n + i
[PROOF STEP]
by (auto simp: inc_above_def)


[STATEMENT]
lemma compute_lowerPoly\<^sub>0[code]: "lowerPoly\<^sub>0 n i (Pm_fmap m) = Pm_fmap (lowerPoly\<^sub>f n i m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lowerPoly\<^sub>0 n i (Pm_fmap m) = Pm_fmap (lowerPoly\<^sub>f n i m)
[PROOF STEP]
by (auto simp: lowerPoly\<^sub>0.rep_eq fmlookup_default_def lowerPoly\<^sub>f.rep_eq
      split: option.splits
      intro!: poly_mapping_eqI)


[STATEMENT]
lemma compute_higherPoly\<^sub>0[code]: "higherPoly\<^sub>0 n i (Pm_fmap m) = Pm_fmap (higherPoly\<^sub>f n i m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higherPoly\<^sub>0 n i (Pm_fmap m) = Pm_fmap (higherPoly\<^sub>f n i m)
[PROOF STEP]
by (auto simp: higherPoly\<^sub>0.rep_eq fmlookup_default_def higherPoly\<^sub>f.rep_eq
      split: option.splits
      intro!: poly_mapping_eqI)


[STATEMENT]
lemma compute_lowerPoly\<^sub>f[code]: "lowerPoly\<^sub>f n i (fmap_of_list xs) =
  (fmap_of_list (map (\<lambda>(mon, c). (higherPowers n i mon, c))
    (filter (\<lambda>(mon, v). \<forall>j\<in>{n..<n+i}. lookup mon j = 0) xs)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lowerPoly\<^sub>f n i (fmap_of_list xs) = fmap_of_list (map (\<lambda>(mon, c). (higherPowers n i mon, c)) (filter (\<lambda>(mon, v). \<forall>j\<in>{n..<n + i}. lookup mon j = 0) xs))
[PROOF STEP]
apply (rule sym)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fmap_of_list (map (\<lambda>(mon, c). (higherPowers n i mon, c)) (filter (\<lambda>(mon, v). \<forall>j\<in>{n..<n + i}. lookup mon j = 0) xs)) = lowerPoly\<^sub>f n i (fmap_of_list xs)
[PROOF STEP]
apply (rule fmap_ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. fmlookup (fmap_of_list (map (\<lambda>(mon, c). (higherPowers n i mon, c)) (filter (\<lambda>(mon, v). \<forall>j\<in>{n..<n + i}. lookup mon j = 0) xs))) x = fmlookup (lowerPoly\<^sub>f n i (fmap_of_list xs)) x
[PROOF STEP]
unfolding lowerPoly\<^sub>f.rep_eq fmlookup_of_list
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. map_of (map (\<lambda>(mon, y). (higherPowers n i mon, y)) (filter (\<lambda>(mon, v). \<forall>j\<in>{n..<n + i}. lookup mon j = 0) xs)) x = map_of xs (lowerPowers n i x)
[PROOF STEP]
apply (subst map_of_map_key_inverse_fun_eq[where g="lowerPowers n i"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x xa. xa \<in> set (filter (\<lambda>(mon, v). \<forall>j\<in>{n..<n + i}. lookup mon j = 0) xs) \<Longrightarrow> lowerPowers n i (higherPowers n i (fst xa)) = fst xa
 2. \<And>x. higherPowers n i (lowerPowers n i x) = x
 3. \<And>x. map_of (filter (\<lambda>(mon, v). \<forall>j\<in>{n..<n + i}. lookup mon j = 0) xs) (lowerPowers n i x) = map_of xs (lowerPowers n i x)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xa_ \<in> set (filter (\<lambda>(mon, v). \<forall>j\<in>{n..<n + i}. lookup mon j = 0) xs) \<Longrightarrow> lowerPowers n i (higherPowers n i (fst xa_)) = fst xa_
[PROOF STEP]
by (auto simp add: lowerPowers_higherPowers)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. higherPowers n i (lowerPowers n i x) = x
 2. \<And>x. map_of (filter (\<lambda>(mon, v). \<forall>j\<in>{n..<n + i}. lookup mon j = 0) xs) (lowerPowers n i x) = map_of xs (lowerPowers n i x)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higherPowers n i (lowerPowers n i x_) = x_
[PROOF STEP]
by (auto simp add: higherPowers_lowerPowers)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. map_of (filter (\<lambda>(mon, v). \<forall>j\<in>{n..<n + i}. lookup mon j = 0) xs) (lowerPowers n i x) = map_of xs (lowerPowers n i x)
[PROOF STEP]
apply (auto simp: fmlookup_of_list lowerPoly\<^sub>f.rep_eq map_of_eq_None_iff map_of_filter_key_in
      fmdom'_fmap_of_list higherPowers.rep_eq lowerPowers.rep_eq dec_above_def
      intro!: fmap_ext)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma compute_higherPoly\<^sub>f[code]: "higherPoly\<^sub>f n i (fmap_of_list xs) =
  fmap_of_list (filter (\<lambda>(mon, v). \<forall>j\<in>{n..<n+i}. lookup mon j = 0)
    (map (\<lambda>(mon, c). (lowerPowers n i mon, c)) xs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higherPoly\<^sub>f n i (fmap_of_list xs) = fmap_of_list (filter (\<lambda>(mon, v). \<forall>j\<in>{n..<n + i}. lookup mon j = 0) (map (\<lambda>(mon, c). (lowerPowers n i mon, c)) xs))
[PROOF STEP]
apply (rule sym)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fmap_of_list (filter (\<lambda>(mon, v). \<forall>j\<in>{n..<n + i}. lookup mon j = 0) (map (\<lambda>(mon, c). (lowerPowers n i mon, c)) xs)) = higherPoly\<^sub>f n i (fmap_of_list xs)
[PROOF STEP]
apply (rule fmap_ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. fmlookup (fmap_of_list (filter (\<lambda>(mon, v). \<forall>j\<in>{n..<n + i}. lookup mon j = 0) (map (\<lambda>(mon, c). (lowerPowers n i mon, c)) xs))) x = fmlookup (higherPoly\<^sub>f n i (fmap_of_list xs)) x
[PROOF STEP]
unfolding higherPoly\<^sub>f.rep_eq fmlookup_of_list
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. map_of (filter (\<lambda>(mon, v). \<forall>j\<in>{n..<n + i}. lookup mon j = 0) (map (\<lambda>(mon, y). (lowerPowers n i mon, y)) xs)) x = (if \<exists>j\<in>{n..<n + i}. 0 < lookup x j then None else map_of xs (higherPowers n i x))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x j. \<lbrakk>0 < lookup x j; n \<le> j; j < n + i\<rbrakk> \<Longrightarrow> map_of (filter (\<lambda>(mon, v). \<forall>j\<in>{n..<n + i}. lookup mon j = 0) (map (\<lambda>(mon, y). (lowerPowers n i mon, y)) xs)) x = None
 2. \<And>x. \<forall>j\<in>{n..<n + i}. lookup x j = 0 \<Longrightarrow> map_of (filter (\<lambda>(mon, v). \<forall>j\<in>{n..<n + i}. lookup mon j = 0) (map (\<lambda>(mon, y). (lowerPowers n i mon, y)) xs)) x = map_of xs (higherPowers n i x)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < lookup x_ j_; n \<le> j_; j_ < n + i\<rbrakk> \<Longrightarrow> map_of (filter (\<lambda>(mon, v). \<forall>j\<in>{n..<n + i}. lookup mon j = 0) (map (\<lambda>(mon, y). (lowerPowers n i mon, y)) xs)) x_ = None
[PROOF STEP]
by (rule map_of_eq_NoneI) auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<forall>j\<in>{n..<n + i}. lookup x j = 0 \<Longrightarrow> map_of (filter (\<lambda>(mon, v). \<forall>j\<in>{n..<n + i}. lookup mon j = 0) (map (\<lambda>(mon, y). (lowerPowers n i mon, y)) xs)) x = map_of xs (higherPowers n i x)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>j\<in>{n..<n + i}. lookup x_ j = 0 \<Longrightarrow> map_of (filter (\<lambda>(mon, v). \<forall>j\<in>{n..<n + i}. lookup mon j = 0) (map (\<lambda>(mon, y). (lowerPowers n i mon, y)) xs)) x_ = map_of xs (higherPowers n i x_)
[PROOF STEP]
apply (subst map_of_filter_key_in)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>j\<in>{n..<n + i}. lookup x_ j = 0 \<Longrightarrow> \<forall>j\<in>{n..<n + i}. lookup x_ j = 0
 2. \<forall>j\<in>{n..<n + i}. lookup x_ j = 0 \<Longrightarrow> map_of (map (\<lambda>(mon, y). (lowerPowers n i mon, y)) xs) x_ = map_of xs (higherPowers n i x_)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>j\<in>{n..<n + i}. lookup x_ j = 0 \<Longrightarrow> map_of (map (\<lambda>(mon, y). (lowerPowers n i mon, y)) xs) x_ = map_of xs (higherPowers n i x_)
[PROOF STEP]
apply (subst map_of_map_key_inverse_fun_eq[where g="higherPowers n i"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>\<forall>j\<in>{n..<n + i}. lookup x_ j = 0; xa \<in> set xs\<rbrakk> \<Longrightarrow> higherPowers n i (lowerPowers n i (fst xa)) = fst xa
 2. \<forall>j\<in>{n..<n + i}. lookup x_ j = 0 \<Longrightarrow> lowerPowers n i (higherPowers n i x_) = x_
 3. \<forall>j\<in>{n..<n + i}. lookup x_ j = 0 \<Longrightarrow> map_of xs (higherPowers n i x_) = map_of xs (higherPowers n i x_)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>j\<in>{n..<n + i}. lookup x_ j = 0; xa_ \<in> set xs\<rbrakk> \<Longrightarrow> higherPowers n i (lowerPowers n i (fst xa_)) = fst xa_
[PROOF STEP]
by (auto simp add: higherPowers_lowerPowers)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>j\<in>{n..<n + i}. lookup x_ j = 0 \<Longrightarrow> lowerPowers n i (higherPowers n i x_) = x_
 2. \<forall>j\<in>{n..<n + i}. lookup x_ j = 0 \<Longrightarrow> map_of xs (higherPowers n i x_) = map_of xs (higherPowers n i x_)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>j\<in>{n..<n + i}. lookup x_ j = 0 \<Longrightarrow> lowerPowers n i (higherPowers n i x_) = x_
[PROOF STEP]
by (auto simp add: lowerPowers_higherPowers)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>j\<in>{n..<n + i}. lookup x_ j = 0 \<Longrightarrow> map_of xs (higherPowers n i x_) = map_of xs (higherPowers n i x_)
[PROOF STEP]
apply (auto simp: fmlookup_of_list lowerPoly\<^sub>f.rep_eq map_of_eq_None_iff map_of_filter_key_in
        fmdom'_fmap_of_list higherPowers.rep_eq lowerPowers.rep_eq dec_above_def
        intro!: fmap_ext)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma coeff_lowerPoly: "MPoly_Type.coeff (lowerPoly b i mp) x = MPoly_Type.coeff mp (lowerPowers b i x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MPoly_Type.coeff (lowerPoly b i mp) x = MPoly_Type.coeff mp (lowerPowers b i x)
[PROOF STEP]
by (transfer') (simp add: lowerPoly\<^sub>0.rep_eq lowerPowers.rep_eq)


[STATEMENT]
lemma coeff_liftPoly: "MPoly_Type.coeff (liftPoly b i mp) x = (if (\<exists>j\<in>{b..<b+i}. lookup x j > 0)
    then 0
    else MPoly_Type.coeff mp (higherPowers b i x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MPoly_Type.coeff (liftPoly b i mp) x = (if \<exists>j\<in>{b..<b + i}. 0 < lookup x j then 0::'a else MPoly_Type.coeff mp (higherPowers b i x))
[PROOF STEP]
by (transfer') (simp add: higherPowers.rep_eq higherPoly\<^sub>0.rep_eq )


[STATEMENT]
lemma monomials_lowerPoly: "monomials (lowerPoly b i mp) = higherPowers b i ` (monomials mp \<inter> {x. \<forall>j\<in>{b..<b + i}. lookup x j = 0}) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monomials (lowerPoly b i mp) = higherPowers b i ` (monomials mp \<inter> {x. \<forall>j\<in>{b..<b + i}. lookup x j = 0})
[PROOF STEP]
by transfer' (simp add: keys_lowerPoly\<^sub>0)


[STATEMENT]
lemma monomials_liftPoly: "monomials (liftPoly b i mp) = lowerPowers b i ` (monomials mp) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monomials (liftPoly b i mp) = lowerPowers b i ` monomials mp
[PROOF STEP]
using keys_higherPoly\<^sub>0
[PROOF STATE]
proof (prove)
using this:
keys (higherPoly\<^sub>0 ?b ?i ?mp) = lowerPowers ?b ?i ` keys ?mp

goal (1 subgoal):
 1. monomials (liftPoly b i mp) = lowerPowers b i ` monomials mp
[PROOF STEP]
by (simp add: keys_higherPoly\<^sub>0 liftPoly.rep_eq monomials.rep_eq)


[STATEMENT]
lemma lookup_not_in_vars_eq_zero: "x \<in> monomials p \<Longrightarrow> i \<notin> vars p \<Longrightarrow> lookup x i = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> monomials p; i \<notin> vars p\<rbrakk> \<Longrightarrow> lookup x i = 0
[PROOF STEP]
by (meson degree_eq_iff varNotIn_degree)


[STATEMENT]
lemma nth_dec_above:
  assumes "length xs = i" "length ys = j" "k \<notin> {i..<i+j}"
  shows "nth_default 0 (xs @ zs) (dec_above i j k) = (nth_default 0 (xs @ ys @ zs)) k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nth_default (0::'a) (xs @ zs) (dec_above i j k) = nth_default (0::'a) (xs @ ys @ zs) k
[PROOF STEP]
using assms dec_above_def nth_append add.commute
[PROOF STATE]
proof (prove)
using this:
length xs = i
length ys = j
k \<notin> {i..<i + j}
dec_above ?b ?i ?x = (if ?x \<le> ?b then ?x else ?x - ?i)
(?xs @ ?ys) ! ?n = (if ?n < length ?xs then ?xs ! ?n else ?ys ! (?n - length ?xs))
?a + ?b = ?b + ?a

goal (1 subgoal):
 1. nth_default (0::'a) (xs @ zs) (dec_above i j k) = nth_default (0::'a) (xs @ ys @ zs) k
[PROOF STEP]
by (smt add_diff_cancel_left add_le_cancel_left add_strict_increasing append_Nil2 atLeastLessThan_iff le_add_diff_inverse length_append length_greater_0_conv less_imp_le_nat not_less nth_default_append)


[STATEMENT]
lemma insertion_lowerPoly:
  assumes i_notin: "vars p \<inter> {i..<i+j} = {}"
    and lprfx: "length prfx = i"
    and lxs: "length xs = j"
  shows "insertion (nth_default 0 (prfx@L)) (lowerPoly i j p) = insertion (nth_default 0 (prfx@xs@L)) p" (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion (nth_default (0::'a) (prfx @ L)) (lowerPoly i j p) = insertion (nth_default (0::'a) (prfx @ xs @ L)) p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. insertion (nth_default (0::'a) (prfx @ L)) (lowerPoly i j p) = insertion (nth_default (0::'a) (prfx @ xs @ L)) p
[PROOF STEP]
have *: "monomials p \<inter> {x. \<forall>j\<in>{i..<i + j}. lookup x j = 0} = monomials p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monomials p \<inter> {x. \<forall>j\<in>{i..<i + j}. lookup x j = 0} = monomials p
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
vars p \<inter> {i..<i + j} = {}

goal (1 subgoal):
 1. monomials p \<inter> {x. \<forall>j\<in>{i..<i + j}. lookup x j = 0} = monomials p
[PROOF STEP]
by (auto intro: lookup_not_in_vars_eq_zero)
[PROOF STATE]
proof (state)
this:
monomials p \<inter> {x. \<forall>j\<in>{i..<i + j}. lookup x j = 0} = monomials p

goal (1 subgoal):
 1. insertion (nth_default (0::'a) (prfx @ L)) (lowerPoly i j p) = insertion (nth_default (0::'a) (prfx @ xs @ L)) p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
monomials p \<inter> {x. \<forall>j\<in>{i..<i + j}. lookup x j = 0} = monomials p
[PROOF STEP]
have "monomials p \<subseteq> {x. \<forall>k. i \<le> k \<and> k < i + j \<longrightarrow> lookup x k = 0}"
[PROOF STATE]
proof (prove)
using this:
monomials p \<inter> {x. \<forall>j\<in>{i..<i + j}. lookup x j = 0} = monomials p

goal (1 subgoal):
 1. monomials p \<subseteq> {x. \<forall>k. i \<le> k \<and> k < i + j \<longrightarrow> lookup x k = 0}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
monomials p \<subseteq> {x. \<forall>k. i \<le> k \<and> k < i + j \<longrightarrow> lookup x k = 0}

goal (1 subgoal):
 1. insertion (nth_default (0::'a) (prfx @ L)) (lowerPoly i j p) = insertion (nth_default (0::'a) (prfx @ xs @ L)) p
[PROOF STEP]
have "?lhs = (\<Sum>m\<in>monomials (lowerPoly i j p). MPoly_Type.coeff (lowerPoly i j p) m * (\<Prod>k\<in>keys m. (nth_default 0 (prfx @ L)) k ^ lookup m k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion (nth_default (0::'a) (prfx @ L)) (lowerPoly i j p) = (\<Sum>m\<in>monomials (lowerPoly i j p). MPoly_Type.coeff (lowerPoly i j p) m * (\<Prod>k\<in>keys m. nth_default (0::'a) (prfx @ L) k ^ lookup m k))
[PROOF STEP]
unfolding insertion_code
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>m\<in>monomials (lowerPoly i j p). MPoly_Type.coeff (lowerPoly i j p) m * (\<Prod>k\<in>keys m. nth_default (0::'a) (prfx @ L) k ^ lookup m k)) = (\<Sum>m\<in>monomials (lowerPoly i j p). MPoly_Type.coeff (lowerPoly i j p) m * (\<Prod>k\<in>keys m. nth_default (0::'a) (prfx @ L) k ^ lookup m k))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
insertion (nth_default (0::'a) (prfx @ L)) (lowerPoly i j p) = (\<Sum>m\<in>monomials (lowerPoly i j p). MPoly_Type.coeff (lowerPoly i j p) m * (\<Prod>k\<in>keys m. nth_default (0::'a) (prfx @ L) k ^ lookup m k))

goal (1 subgoal):
 1. insertion (nth_default (0::'a) (prfx @ L)) (lowerPoly i j p) = insertion (nth_default (0::'a) (prfx @ xs @ L)) p
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
insertion (nth_default (0::'a) (prfx @ L)) (lowerPoly i j p) = (\<Sum>m\<in>monomials (lowerPoly i j p). MPoly_Type.coeff (lowerPoly i j p) m * (\<Prod>k\<in>keys m. nth_default (0::'a) (prfx @ L) k ^ lookup m k))

goal (1 subgoal):
 1. insertion (nth_default (0::'a) (prfx @ L)) (lowerPoly i j p) = insertion (nth_default (0::'a) (prfx @ xs @ L)) p
[PROOF STEP]
have "\<dots> = (\<Sum>m\<in>monomials p.
       MPoly_Type.coeff p m * (\<Prod>k\<in>keys m. (nth_default 0 (prfx @ xs @ L) k) ^ lookup m k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>m\<in>monomials (lowerPoly i j p). MPoly_Type.coeff (lowerPoly i j p) m * (\<Prod>k\<in>keys m. nth_default (0::'a) (prfx @ L) k ^ lookup m k)) = (\<Sum>m\<in>monomials p. MPoly_Type.coeff p m * (\<Prod>k\<in>keys m. nth_default (0::'a) (prfx @ xs @ L) k ^ lookup m k))
[PROOF STEP]
proof (rule sum.reindex_cong)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. inj_on ?l (monomials p)
 2. monomials (lowerPoly i j p) = ?l ` monomials p
 3. \<And>x. x \<in> monomials p \<Longrightarrow> MPoly_Type.coeff (lowerPoly i j p) (?l x) * (\<Prod>k\<in>keys (?l x). nth_default (0::'a) (prfx @ L) k ^ lookup (?l x) k) = MPoly_Type.coeff p x * (\<Prod>k\<in>keys x. nth_default (0::'a) (prfx @ xs @ L) k ^ lookup x k)
[PROOF STEP]
note inj_on_higherPowers[of i j]
[PROOF STATE]
proof (state)
this:
inj_on (higherPowers i j) {x. \<forall>ja. i \<le> ja \<and> ja < i + j \<longrightarrow> lookup x ja = (0::?'a)}

goal (3 subgoals):
 1. inj_on ?l (monomials p)
 2. monomials (lowerPoly i j p) = ?l ` monomials p
 3. \<And>x. x \<in> monomials p \<Longrightarrow> MPoly_Type.coeff (lowerPoly i j p) (?l x) * (\<Prod>k\<in>keys (?l x). nth_default (0::'a) (prfx @ L) k ^ lookup (?l x) k) = MPoly_Type.coeff p x * (\<Prod>k\<in>keys x. nth_default (0::'a) (prfx @ xs @ L) k ^ lookup x k)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
inj_on (higherPowers i j) {x. \<forall>ja. i \<le> ja \<and> ja < i + j \<longrightarrow> lookup x ja = (0::?'a)}

goal (3 subgoals):
 1. inj_on ?l (monomials p)
 2. monomials (lowerPoly i j p) = ?l ` monomials p
 3. \<And>x. x \<in> monomials p \<Longrightarrow> MPoly_Type.coeff (lowerPoly i j p) (?l x) * (\<Prod>k\<in>keys (?l x). nth_default (0::'a) (prfx @ L) k ^ lookup (?l x) k) = MPoly_Type.coeff p x * (\<Prod>k\<in>keys x. nth_default (0::'a) (prfx @ xs @ L) k ^ lookup x k)
[PROOF STEP]
note \<open>monomials p \<subseteq> _\<close>
[PROOF STATE]
proof (state)
this:
monomials p \<subseteq> {x. \<forall>k. i \<le> k \<and> k < i + j \<longrightarrow> lookup x k = 0}

goal (3 subgoals):
 1. inj_on ?l (monomials p)
 2. monomials (lowerPoly i j p) = ?l ` monomials p
 3. \<And>x. x \<in> monomials p \<Longrightarrow> MPoly_Type.coeff (lowerPoly i j p) (?l x) * (\<Prod>k\<in>keys (?l x). nth_default (0::'a) (prfx @ L) k ^ lookup (?l x) k) = MPoly_Type.coeff p x * (\<Prod>k\<in>keys x. nth_default (0::'a) (prfx @ xs @ L) k ^ lookup x k)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
inj_on (higherPowers i j) {x. \<forall>ja. i \<le> ja \<and> ja < i + j \<longrightarrow> lookup x ja = (0::?'a)}
monomials p \<subseteq> {x. \<forall>k. i \<le> k \<and> k < i + j \<longrightarrow> lookup x k = 0}
[PROOF STEP]
show "inj_on (higherPowers i j) (monomials p)"
[PROOF STATE]
proof (prove)
using this:
inj_on (higherPowers i j) {x. \<forall>ja. i \<le> ja \<and> ja < i + j \<longrightarrow> lookup x ja = (0::?'a)}
monomials p \<subseteq> {x. \<forall>k. i \<le> k \<and> k < i + j \<longrightarrow> lookup x k = 0}

goal (1 subgoal):
 1. inj_on (higherPowers i j) (monomials p)
[PROOF STEP]
by (rule inj_on_subset)
[PROOF STATE]
proof (state)
this:
inj_on (higherPowers i j) (monomials p)

goal (2 subgoals):
 1. monomials (lowerPoly i j p) = higherPowers i j ` monomials p
 2. \<And>x. x \<in> monomials p \<Longrightarrow> MPoly_Type.coeff (lowerPoly i j p) (higherPowers i j x) * (\<Prod>k\<in>keys (higherPowers i j x). nth_default (0::'a) (prfx @ L) k ^ lookup (higherPowers i j x) k) = MPoly_Type.coeff p x * (\<Prod>k\<in>keys x. nth_default (0::'a) (prfx @ xs @ L) k ^ lookup x k)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. monomials (lowerPoly i j p) = higherPowers i j ` monomials p
 2. \<And>x. x \<in> monomials p \<Longrightarrow> MPoly_Type.coeff (lowerPoly i j p) (higherPowers i j x) * (\<Prod>k\<in>keys (higherPowers i j x). nth_default (0::'a) (prfx @ L) k ^ lookup (higherPowers i j x) k) = MPoly_Type.coeff p x * (\<Prod>k\<in>keys x. nth_default (0::'a) (prfx @ xs @ L) k ^ lookup x k)
[PROOF STEP]
show "monomials (lowerPoly i j p) = higherPowers i j ` monomials p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monomials (lowerPoly i j p) = higherPowers i j ` monomials p
[PROOF STEP]
unfolding monomials_lowerPoly *
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higherPowers i j ` monomials p = higherPowers i j ` monomials p
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
monomials (lowerPoly i j p) = higherPowers i j ` monomials p

goal (1 subgoal):
 1. \<And>x. x \<in> monomials p \<Longrightarrow> MPoly_Type.coeff (lowerPoly i j p) (higherPowers i j x) * (\<Prod>k\<in>keys (higherPowers i j x). nth_default (0::'a) (prfx @ L) k ^ lookup (higherPowers i j x) k) = MPoly_Type.coeff p x * (\<Prod>k\<in>keys x. nth_default (0::'a) (prfx @ xs @ L) k ^ lookup x k)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> monomials p \<Longrightarrow> MPoly_Type.coeff (lowerPoly i j p) (higherPowers i j x) * (\<Prod>k\<in>keys (higherPowers i j x). nth_default (0::'a) (prfx @ L) k ^ lookup (higherPowers i j x) k) = MPoly_Type.coeff p x * (\<Prod>k\<in>keys x. nth_default (0::'a) (prfx @ xs @ L) k ^ lookup x k)
[PROOF STEP]
fix m
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> monomials p \<Longrightarrow> MPoly_Type.coeff (lowerPoly i j p) (higherPowers i j x) * (\<Prod>k\<in>keys (higherPowers i j x). nth_default (0::'a) (prfx @ L) k ^ lookup (higherPowers i j x) k) = MPoly_Type.coeff p x * (\<Prod>k\<in>keys x. nth_default (0::'a) (prfx @ xs @ L) k ^ lookup x k)
[PROOF STEP]
assume m: "m \<in> monomials p"
[PROOF STATE]
proof (state)
this:
m \<in> monomials p

goal (1 subgoal):
 1. \<And>x. x \<in> monomials p \<Longrightarrow> MPoly_Type.coeff (lowerPoly i j p) (higherPowers i j x) * (\<Prod>k\<in>keys (higherPowers i j x). nth_default (0::'a) (prfx @ L) k ^ lookup (higherPowers i j x) k) = MPoly_Type.coeff p x * (\<Prod>k\<in>keys x. nth_default (0::'a) (prfx @ xs @ L) k ^ lookup x k)
[PROOF STEP]
from m \<open>monomials p \<subseteq> _\<close>
[PROOF STATE]
proof (chain)
picking this:
m \<in> monomials p
monomials p \<subseteq> {x. \<forall>k. i \<le> k \<and> k < i + j \<longrightarrow> lookup x k = 0}
[PROOF STEP]
have "keys m \<subseteq> {x. x \<notin> {i..<i + j}}"
[PROOF STATE]
proof (prove)
using this:
m \<in> monomials p
monomials p \<subseteq> {x. \<forall>k. i \<le> k \<and> k < i + j \<longrightarrow> lookup x k = 0}

goal (1 subgoal):
 1. keys m \<subseteq> {x. x \<notin> {i..<i + j}}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
keys m \<subseteq> {x. x \<notin> {i..<i + j}}

goal (1 subgoal):
 1. \<And>x. x \<in> monomials p \<Longrightarrow> MPoly_Type.coeff (lowerPoly i j p) (higherPowers i j x) * (\<Prod>k\<in>keys (higherPowers i j x). nth_default (0::'a) (prfx @ L) k ^ lookup (higherPowers i j x) k) = MPoly_Type.coeff p x * (\<Prod>k\<in>keys x. nth_default (0::'a) (prfx @ xs @ L) k ^ lookup x k)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
keys m \<subseteq> {x. x \<notin> {i..<i + j}}
[PROOF STEP]
have "lookup m k = 0" if "i \<le> k" "k < i + j" for k
[PROOF STATE]
proof (prove)
using this:
keys m \<subseteq> {x. x \<notin> {i..<i + j}}

goal (1 subgoal):
 1. lookup m k = 0
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
keys m \<subseteq> {x. x \<notin> {i..<i + j}}
i \<le> k
k < i + j

goal (1 subgoal):
 1. lookup m k = 0
[PROOF STEP]
by (auto simp: in_keys_iff)
[PROOF STATE]
proof (state)
this:
\<lbrakk>i \<le> ?k; ?k < i + j\<rbrakk> \<Longrightarrow> lookup m ?k = 0

goal (1 subgoal):
 1. \<And>x. x \<in> monomials p \<Longrightarrow> MPoly_Type.coeff (lowerPoly i j p) (higherPowers i j x) * (\<Prod>k\<in>keys (higherPowers i j x). nth_default (0::'a) (prfx @ L) k ^ lookup (higherPowers i j x) k) = MPoly_Type.coeff p x * (\<Prod>k\<in>keys x. nth_default (0::'a) (prfx @ xs @ L) k ^ lookup x k)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>i \<le> ?k; ?k < i + j\<rbrakk> \<Longrightarrow> lookup m ?k = 0
[PROOF STEP]
have "lowerPowers i j (higherPowers i j m) = m"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i \<le> ?k; ?k < i + j\<rbrakk> \<Longrightarrow> lookup m ?k = 0

goal (1 subgoal):
 1. lowerPowers i j (higherPowers i j m) = m
[PROOF STEP]
by (rule lowerPowers_higherPowers)
[PROOF STATE]
proof (state)
this:
lowerPowers i j (higherPowers i j m) = m

goal (1 subgoal):
 1. \<And>x. x \<in> monomials p \<Longrightarrow> MPoly_Type.coeff (lowerPoly i j p) (higherPowers i j x) * (\<Prod>k\<in>keys (higherPowers i j x). nth_default (0::'a) (prfx @ L) k ^ lookup (higherPowers i j x) k) = MPoly_Type.coeff p x * (\<Prod>k\<in>keys x. nth_default (0::'a) (prfx @ xs @ L) k ^ lookup x k)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
lowerPowers i j (higherPowers i j m) = m
[PROOF STEP]
have "MPoly_Type.coeff (lowerPoly i j p) (higherPowers i j m) = MPoly_Type.coeff p m"
[PROOF STATE]
proof (prove)
using this:
lowerPowers i j (higherPowers i j m) = m

goal (1 subgoal):
 1. MPoly_Type.coeff (lowerPoly i j p) (higherPowers i j m) = MPoly_Type.coeff p m
[PROOF STEP]
unfolding coeff_lowerPoly
[PROOF STATE]
proof (prove)
using this:
lowerPowers i j (higherPowers i j m) = m

goal (1 subgoal):
 1. MPoly_Type.coeff p (lowerPowers i j (higherPowers i j m)) = MPoly_Type.coeff p m
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
MPoly_Type.coeff (lowerPoly i j p) (higherPowers i j m) = MPoly_Type.coeff p m

goal (1 subgoal):
 1. \<And>x. x \<in> monomials p \<Longrightarrow> MPoly_Type.coeff (lowerPoly i j p) (higherPowers i j x) * (\<Prod>k\<in>keys (higherPowers i j x). nth_default (0::'a) (prfx @ L) k ^ lookup (higherPowers i j x) k) = MPoly_Type.coeff p x * (\<Prod>k\<in>keys x. nth_default (0::'a) (prfx @ xs @ L) k ^ lookup x k)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
MPoly_Type.coeff (lowerPoly i j p) (higherPowers i j m) = MPoly_Type.coeff p m

goal (1 subgoal):
 1. \<And>x. x \<in> monomials p \<Longrightarrow> MPoly_Type.coeff (lowerPoly i j p) (higherPowers i j x) * (\<Prod>k\<in>keys (higherPowers i j x). nth_default (0::'a) (prfx @ L) k ^ lookup (higherPowers i j x) k) = MPoly_Type.coeff p x * (\<Prod>k\<in>keys x. nth_default (0::'a) (prfx @ xs @ L) k ^ lookup x k)
[PROOF STEP]
have "(\<Prod>k\<in>keys (higherPowers i j m). (nth_default 0 (prfx @ L)) k ^ lookup (higherPowers i j m) k) =
      (\<Prod>k\<in>keys m. (nth_default 0 (prfx @ xs @ L)) k ^ lookup m k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>k\<in>keys (higherPowers i j m). nth_default (0::'a) (prfx @ L) k ^ lookup (higherPowers i j m) k) = (\<Prod>k\<in>keys m. nth_default (0::'a) (prfx @ xs @ L) k ^ lookup m k)
[PROOF STEP]
proof (rule prod.reindex_cong)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. inj_on ?l (keys m)
 2. keys (higherPowers i j m) = ?l ` keys m
 3. \<And>x. x \<in> keys m \<Longrightarrow> nth_default (0::'a) (prfx @ L) (?l x) ^ lookup (higherPowers i j m) (?l x) = nth_default (0::'a) (prfx @ xs @ L) x ^ lookup m x
[PROOF STEP]
show "keys (higherPowers i j m) = dec_above i j ` keys m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. keys (higherPowers i j m) = dec_above i j ` keys m
[PROOF STEP]
unfolding keys_higherPowers
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dec_above i j ` (keys m \<inter> {x. x \<notin> {i..<i + j}}) = dec_above i j ` keys m
[PROOF STEP]
using \<open>keys m \<subseteq> _\<close>
[PROOF STATE]
proof (prove)
using this:
keys m \<subseteq> {x. x \<notin> {i..<i + j}}

goal (1 subgoal):
 1. dec_above i j ` (keys m \<inter> {x. x \<notin> {i..<i + j}}) = dec_above i j ` keys m
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
keys (higherPowers i j m) = dec_above i j ` keys m

goal (2 subgoals):
 1. inj_on (dec_above i j) (keys m)
 2. \<And>x. x \<in> keys m \<Longrightarrow> nth_default (0::'a) (prfx @ L) (dec_above i j x) ^ lookup (higherPowers i j m) (dec_above i j x) = nth_default (0::'a) (prfx @ xs @ L) x ^ lookup m x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. inj_on (dec_above i j) (keys m)
 2. \<And>x. x \<in> keys m \<Longrightarrow> nth_default (0::'a) (prfx @ L) (dec_above i j x) ^ lookup (higherPowers i j m) (dec_above i j x) = nth_default (0::'a) (prfx @ xs @ L) x ^ lookup m x
[PROOF STEP]
from inj_on_dec_above[of i j]
[PROOF STATE]
proof (chain)
picking this:
inj_on (dec_above i j) {x. x < i \<or> i + j \<le> x}
[PROOF STEP]
show "inj_on (dec_above i j) (keys m)"
[PROOF STATE]
proof (prove)
using this:
inj_on (dec_above i j) {x. x < i \<or> i + j \<le> x}

goal (1 subgoal):
 1. inj_on (dec_above i j) (keys m)
[PROOF STEP]
by (rule inj_on_subset) (use \<open>keys m \<subseteq> _\<close> in auto)
[PROOF STATE]
proof (state)
this:
inj_on (dec_above i j) (keys m)

goal (1 subgoal):
 1. \<And>x. x \<in> keys m \<Longrightarrow> nth_default (0::'a) (prfx @ L) (dec_above i j x) ^ lookup (higherPowers i j m) (dec_above i j x) = nth_default (0::'a) (prfx @ xs @ L) x ^ lookup m x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> keys m \<Longrightarrow> nth_default (0::'a) (prfx @ L) (dec_above i j x) ^ lookup (higherPowers i j m) (dec_above i j x) = nth_default (0::'a) (prfx @ xs @ L) x ^ lookup m x
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> keys m \<Longrightarrow> nth_default (0::'a) (prfx @ L) (dec_above i j x) ^ lookup (higherPowers i j m) (dec_above i j x) = nth_default (0::'a) (prfx @ xs @ L) x ^ lookup m x
[PROOF STEP]
assume k: "k \<in> keys m"
[PROOF STATE]
proof (state)
this:
k \<in> keys m

goal (1 subgoal):
 1. \<And>x. x \<in> keys m \<Longrightarrow> nth_default (0::'a) (prfx @ L) (dec_above i j x) ^ lookup (higherPowers i j m) (dec_above i j x) = nth_default (0::'a) (prfx @ xs @ L) x ^ lookup m x
[PROOF STEP]
from k \<open>keys m \<subseteq> _\<close>
[PROOF STATE]
proof (chain)
picking this:
k \<in> keys m
keys m \<subseteq> {x. x \<notin> {i..<i + j}}
[PROOF STEP]
have "k \<notin> {i..<i+j}"
[PROOF STATE]
proof (prove)
using this:
k \<in> keys m
keys m \<subseteq> {x. x \<notin> {i..<i + j}}

goal (1 subgoal):
 1. k \<notin> {i..<i + j}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k \<notin> {i..<i + j}

goal (1 subgoal):
 1. \<And>x. x \<in> keys m \<Longrightarrow> nth_default (0::'a) (prfx @ L) (dec_above i j x) ^ lookup (higherPowers i j m) (dec_above i j x) = nth_default (0::'a) (prfx @ xs @ L) x ^ lookup m x
[PROOF STEP]
from k \<open>keys m \<subseteq> _\<close>
[PROOF STATE]
proof (chain)
picking this:
k \<in> keys m
keys m \<subseteq> {x. x \<notin> {i..<i + j}}
[PROOF STEP]
have "inc_above i j (dec_above i j k) = k"
[PROOF STATE]
proof (prove)
using this:
k \<in> keys m
keys m \<subseteq> {x. x \<notin> {i..<i + j}}

goal (1 subgoal):
 1. inc_above i j (dec_above i j k) = k
[PROOF STEP]
by (subst inc_above_dec_above) auto
[PROOF STATE]
proof (state)
this:
inc_above i j (dec_above i j k) = k

goal (1 subgoal):
 1. \<And>x. x \<in> keys m \<Longrightarrow> nth_default (0::'a) (prfx @ L) (dec_above i j x) ^ lookup (higherPowers i j m) (dec_above i j x) = nth_default (0::'a) (prfx @ xs @ L) x ^ lookup m x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
inc_above i j (dec_above i j k) = k
[PROOF STEP]
have "lookup (higherPowers i j m) (dec_above i j k) = lookup m k"
[PROOF STATE]
proof (prove)
using this:
inc_above i j (dec_above i j k) = k

goal (1 subgoal):
 1. lookup (higherPowers i j m) (dec_above i j k) = lookup m k
[PROOF STEP]
unfolding higherPowers.rep_eq
[PROOF STATE]
proof (prove)
using this:
inc_above i j (dec_above i j k) = k

goal (1 subgoal):
 1. lookup m (inc_above i j (dec_above i j k)) = lookup m k
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lookup (higherPowers i j m) (dec_above i j k) = lookup m k

goal (1 subgoal):
 1. \<And>x. x \<in> keys m \<Longrightarrow> nth_default (0::'a) (prfx @ L) (dec_above i j x) ^ lookup (higherPowers i j m) (dec_above i j x) = nth_default (0::'a) (prfx @ xs @ L) x ^ lookup m x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
lookup (higherPowers i j m) (dec_above i j k) = lookup m k

goal (1 subgoal):
 1. \<And>x. x \<in> keys m \<Longrightarrow> nth_default (0::'a) (prfx @ L) (dec_above i j x) ^ lookup (higherPowers i j m) (dec_above i j x) = nth_default (0::'a) (prfx @ xs @ L) x ^ lookup m x
[PROOF STEP]
have "nth_default 0 (prfx @ L) (dec_above i j k) = (nth_default 0 (prfx @ xs @ L)) k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nth_default (0::'a) (prfx @ L) (dec_above i j k) = nth_default (0::'a) (prfx @ xs @ L) k
[PROOF STEP]
apply (rule nth_dec_above)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. length prfx = i
 2. length xs = j
 3. k \<notin> {i..<i + j}
[PROOF STEP]
using assms \<open>k \<notin> _\<close>
[PROOF STATE]
proof (prove)
using this:
vars p \<inter> {i..<i + j} = {}
length prfx = i
length xs = j
k \<notin> {i..<i + j}

goal (3 subgoals):
 1. length prfx = i
 2. length xs = j
 3. k \<notin> {i..<i + j}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nth_default (0::'a) (prfx @ L) (dec_above i j k) = nth_default (0::'a) (prfx @ xs @ L) k

goal (1 subgoal):
 1. \<And>x. x \<in> keys m \<Longrightarrow> nth_default (0::'a) (prfx @ L) (dec_above i j x) ^ lookup (higherPowers i j m) (dec_above i j x) = nth_default (0::'a) (prfx @ xs @ L) x ^ lookup m x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
lookup (higherPowers i j m) (dec_above i j k) = lookup m k
nth_default (0::'a) (prfx @ L) (dec_above i j k) = nth_default (0::'a) (prfx @ xs @ L) k
[PROOF STEP]
show "((nth_default 0 (prfx @ L)) (dec_above i j k)) ^ lookup (higherPowers i j m) (dec_above i j k) = ((nth_default 0 (prfx @ xs @ L)) k) ^ lookup m k"
[PROOF STATE]
proof (prove)
using this:
lookup (higherPowers i j m) (dec_above i j k) = lookup m k
nth_default (0::'a) (prfx @ L) (dec_above i j k) = nth_default (0::'a) (prfx @ xs @ L) k

goal (1 subgoal):
 1. nth_default (0::'a) (prfx @ L) (dec_above i j k) ^ lookup (higherPowers i j m) (dec_above i j k) = nth_default (0::'a) (prfx @ xs @ L) k ^ lookup m k
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
nth_default (0::'a) (prfx @ L) (dec_above i j k) ^ lookup (higherPowers i j m) (dec_above i j k) = nth_default (0::'a) (prfx @ xs @ L) k ^ lookup m k

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Prod>k\<in>keys (higherPowers i j m). nth_default (0::'a) (prfx @ L) k ^ lookup (higherPowers i j m) k) = (\<Prod>k\<in>keys m. nth_default (0::'a) (prfx @ xs @ L) k ^ lookup m k)

goal (1 subgoal):
 1. \<And>x. x \<in> monomials p \<Longrightarrow> MPoly_Type.coeff (lowerPoly i j p) (higherPowers i j x) * (\<Prod>k\<in>keys (higherPowers i j x). nth_default (0::'a) (prfx @ L) k ^ lookup (higherPowers i j x) k) = MPoly_Type.coeff p x * (\<Prod>k\<in>keys x. nth_default (0::'a) (prfx @ xs @ L) k ^ lookup x k)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
MPoly_Type.coeff (lowerPoly i j p) (higherPowers i j m) = MPoly_Type.coeff p m
(\<Prod>k\<in>keys (higherPowers i j m). nth_default (0::'a) (prfx @ L) k ^ lookup (higherPowers i j m) k) = (\<Prod>k\<in>keys m. nth_default (0::'a) (prfx @ xs @ L) k ^ lookup m k)
[PROOF STEP]
show "MPoly_Type.coeff (lowerPoly i j p) (higherPowers i j m) * (\<Prod>k\<in>keys (higherPowers i j m). (nth_default 0(prfx @ L)) k ^ lookup (higherPowers i j m) k) =
          MPoly_Type.coeff p m * (\<Prod>k\<in>keys m. (nth_default 0 (prfx @ xs @ L)) k ^ lookup m k)"
[PROOF STATE]
proof (prove)
using this:
MPoly_Type.coeff (lowerPoly i j p) (higherPowers i j m) = MPoly_Type.coeff p m
(\<Prod>k\<in>keys (higherPowers i j m). nth_default (0::'a) (prfx @ L) k ^ lookup (higherPowers i j m) k) = (\<Prod>k\<in>keys m. nth_default (0::'a) (prfx @ xs @ L) k ^ lookup m k)

goal (1 subgoal):
 1. MPoly_Type.coeff (lowerPoly i j p) (higherPowers i j m) * (\<Prod>k\<in>keys (higherPowers i j m). nth_default (0::'a) (prfx @ L) k ^ lookup (higherPowers i j m) k) = MPoly_Type.coeff p m * (\<Prod>k\<in>keys m. nth_default (0::'a) (prfx @ xs @ L) k ^ lookup m k)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
MPoly_Type.coeff (lowerPoly i j p) (higherPowers i j m) * (\<Prod>k\<in>keys (higherPowers i j m). nth_default (0::'a) (prfx @ L) k ^ lookup (higherPowers i j m) k) = MPoly_Type.coeff p m * (\<Prod>k\<in>keys m. nth_default (0::'a) (prfx @ xs @ L) k ^ lookup m k)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>m\<in>monomials (lowerPoly i j p). MPoly_Type.coeff (lowerPoly i j p) m * (\<Prod>k\<in>keys m. nth_default (0::'a) (prfx @ L) k ^ lookup m k)) = (\<Sum>m\<in>monomials p. MPoly_Type.coeff p m * (\<Prod>k\<in>keys m. nth_default (0::'a) (prfx @ xs @ L) k ^ lookup m k))

goal (1 subgoal):
 1. insertion (nth_default (0::'a) (prfx @ L)) (lowerPoly i j p) = insertion (nth_default (0::'a) (prfx @ xs @ L)) p
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
insertion (nth_default (0::'a) (prfx @ L)) (lowerPoly i j p) = (\<Sum>m\<in>monomials p. MPoly_Type.coeff p m * (\<Prod>k\<in>keys m. nth_default (0::'a) (prfx @ xs @ L) k ^ lookup m k))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
insertion (nth_default (0::'a) (prfx @ L)) (lowerPoly i j p) = (\<Sum>m\<in>monomials p. MPoly_Type.coeff p m * (\<Prod>k\<in>keys m. nth_default (0::'a) (prfx @ xs @ L) k ^ lookup m k))

goal (1 subgoal):
 1. insertion (nth_default (0::'a) (prfx @ L)) (lowerPoly i j p) = insertion (nth_default (0::'a) (prfx @ xs @ L)) p
[PROOF STEP]
unfolding insertion_code
[PROOF STATE]
proof (prove)
using this:
(\<Sum>m\<in>monomials (lowerPoly i j p). MPoly_Type.coeff (lowerPoly i j p) m * (\<Prod>k\<in>keys m. nth_default (0::'a) (prfx @ L) k ^ lookup m k)) = (\<Sum>m\<in>monomials p. MPoly_Type.coeff p m * (\<Prod>k\<in>keys m. nth_default (0::'a) (prfx @ xs @ L) k ^ lookup m k))

goal (1 subgoal):
 1. (\<Sum>m\<in>monomials (lowerPoly i j p). MPoly_Type.coeff (lowerPoly i j p) m * (\<Prod>k\<in>keys m. nth_default (0::'a) (prfx @ L) k ^ lookup m k)) = (\<Sum>m\<in>monomials p. MPoly_Type.coeff p m * (\<Prod>k\<in>keys m. nth_default (0::'a) (prfx @ xs @ L) k ^ lookup m k))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
insertion (nth_default (0::'a) (prfx @ L)) (lowerPoly i j p) = insertion (nth_default (0::'a) (prfx @ xs @ L)) p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma insertion_lowerPoly1:
  assumes i_notin: "i \<notin> vars p"
    and lprfx: "length prfx = i"
  shows "insertion (nth_default 0 (prfx@x#L)) p = insertion (nth_default 0 (prfx@L)) (lowerPoly i 1 p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion (nth_default (0::'a) (prfx @ x # L)) p = insertion (nth_default (0::'a) (prfx @ L)) (lowerPoly i 1 p)
[PROOF STEP]
using assms nth_default_def
[PROOF STATE]
proof (prove)
using this:
i \<notin> vars p
length prfx = i
nth_default ?dflt ?xs ?n = (if ?n < length ?xs then ?xs ! ?n else ?dflt)

goal (1 subgoal):
 1. insertion (nth_default (0::'a) (prfx @ x # L)) p = insertion (nth_default (0::'a) (prfx @ L)) (lowerPoly i 1 p)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i \<notin> vars p; length prfx = i; \<And>dflt xs n. nth_default dflt xs n = (if n < length xs then xs ! n else dflt)\<rbrakk> \<Longrightarrow> insertion (nth_default (0::'a) (prfx @ x # L)) p = insertion (nth_default (0::'a) (prfx @ L)) (lowerPoly i (Suc 0) p)
[PROOF STEP]
by (subst insertion_lowerPoly[where xs="[x]"]) auto


[STATEMENT]
lemma insertion_lowerPoly01:
  assumes i_notin: "0 \<notin> vars p"
  shows "insertion (nth_default 0 (x#L)) p = insertion (nth_default 0 L) (lowerPoly 0 1 p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion (nth_default (0::'a) (x # L)) p = insertion (nth_default (0::'a) L) (lowerPoly 0 1 p)
[PROOF STEP]
using insertion_lowerPoly1[OF assms, of Nil x L]
[PROOF STATE]
proof (prove)
using this:
length [] = 0 \<Longrightarrow> insertion (nth_default (0::'a) ([] @ x # L)) p = insertion (nth_default (0::'a) ([] @ L)) (lowerPoly 0 1 p)

goal (1 subgoal):
 1. insertion (nth_default (0::'a) (x # L)) p = insertion (nth_default (0::'a) L) (lowerPoly 0 1 p)
[PROOF STEP]
by simp


[STATEMENT]
lemma aEval_lowerAtom : "(freeIn 0 (Atom A)) \<Longrightarrow> (aEval A (x#L) = aEval (lowerAtom 0 1 A) L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. freeIn 0 (fm.Atom A) \<Longrightarrow> aEval A (x # L) = aEval (lowerAtom 0 1 A) L
[PROOF STEP]
by (cases A) (simp_all add:insertion_lowerPoly01)