[STATEMENT]
lemma coeff_lift_add : "MPoly_Type.coeff (liftPoly x y (a + b)) m = MPoly_Type.coeff (liftPoly x y a) m + MPoly_Type.coeff (liftPoly x y b) m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MPoly_Type.coeff (liftPoly x y (a + b)) m = MPoly_Type.coeff (liftPoly x y a) m + MPoly_Type.coeff (liftPoly x y b) m
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. MPoly_Type.coeff (liftPoly x y (a + b)) m = MPoly_Type.coeff (liftPoly x y a) m + MPoly_Type.coeff (liftPoly x y b) m
[PROOF STEP]
have "MPoly_Type.coeff (liftPoly x y (a + b)) m = MPoly_Type.coeff (liftPoly x y a + liftPoly x y b) m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MPoly_Type.coeff (liftPoly x y (a + b)) m = MPoly_Type.coeff (liftPoly x y a + liftPoly x y b) m
[PROOF STEP]
apply( simp add : mapping_of_lift_add coeff_def  )
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup (mapping_of (liftPoly x y a) + mapping_of (liftPoly x y b)) m = lookup (mapping_of (liftPoly x y a + liftPoly x y b)) m
[PROOF STEP]
using lookup_add
[PROOF STATE]
proof (prove)
using this:
lookup (?f + ?g) ?k = lookup ?f ?k + lookup ?g ?k

goal (1 subgoal):
 1. lookup (mapping_of (liftPoly x y a) + mapping_of (liftPoly x y b)) m = lookup (mapping_of (liftPoly x y a + liftPoly x y b)) m
[PROOF STEP]
by (simp add: plus_mpoly.rep_eq)
[PROOF STATE]
proof (state)
this:
MPoly_Type.coeff (liftPoly x y (a + b)) m = MPoly_Type.coeff (liftPoly x y a + liftPoly x y b) m

goal (1 subgoal):
 1. MPoly_Type.coeff (liftPoly x y (a + b)) m = MPoly_Type.coeff (liftPoly x y a) m + MPoly_Type.coeff (liftPoly x y b) m
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
MPoly_Type.coeff (liftPoly x y (a + b)) m = MPoly_Type.coeff (liftPoly x y a + liftPoly x y b) m

goal (1 subgoal):
 1. MPoly_Type.coeff (liftPoly x y (a + b)) m = MPoly_Type.coeff (liftPoly x y a) m + MPoly_Type.coeff (liftPoly x y b) m
[PROOF STEP]
have "... = MPoly_Type.coeff (liftPoly x y a) m + MPoly_Type.coeff (liftPoly x y b) m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MPoly_Type.coeff (liftPoly x y a + liftPoly x y b) m = MPoly_Type.coeff (liftPoly x y a) m + MPoly_Type.coeff (liftPoly x y b) m
[PROOF STEP]
using MPolyExtension.coeff_add[of "liftPoly x y a" "liftPoly x y b" m]
[PROOF STATE]
proof (prove)
using this:
MPoly_Type.coeff (liftPoly x y a + liftPoly x y b) m = MPoly_Type.coeff (liftPoly x y a) m + MPoly_Type.coeff (liftPoly x y b) m

goal (1 subgoal):
 1. MPoly_Type.coeff (liftPoly x y a + liftPoly x y b) m = MPoly_Type.coeff (liftPoly x y a) m + MPoly_Type.coeff (liftPoly x y b) m
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
MPoly_Type.coeff (liftPoly x y a + liftPoly x y b) m = MPoly_Type.coeff (liftPoly x y a) m + MPoly_Type.coeff (liftPoly x y b) m

goal (1 subgoal):
 1. MPoly_Type.coeff (liftPoly x y (a + b)) m = MPoly_Type.coeff (liftPoly x y a) m + MPoly_Type.coeff (liftPoly x y b) m
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
MPoly_Type.coeff (liftPoly x y (a + b)) m = MPoly_Type.coeff (liftPoly x y a) m + MPoly_Type.coeff (liftPoly x y b) m
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
MPoly_Type.coeff (liftPoly x y (a + b)) m = MPoly_Type.coeff (liftPoly x y a) m + MPoly_Type.coeff (liftPoly x y b) m

goal (1 subgoal):
 1. MPoly_Type.coeff (liftPoly x y (a + b)) m = MPoly_Type.coeff (liftPoly x y a) m + MPoly_Type.coeff (liftPoly x y b) m
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
MPoly_Type.coeff (liftPoly x y (a + b)) m = MPoly_Type.coeff (liftPoly x y a) m + MPoly_Type.coeff (liftPoly x y b) m

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lift_add : "insertion (f::nat\<Rightarrow>real)  (liftPoly 0 z (a + b)) = insertion f (liftPoly 0 z a + liftPoly 0 z b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion f (liftPoly 0 z (a + b)) = insertion f (liftPoly 0 z a + liftPoly 0 z b)
[PROOF STEP]
using liftPoly_add[of 0 z a b]
[PROOF STATE]
proof (prove)
using this:
liftPoly 0 z (a + b) = liftPoly 0 z a + liftPoly 0 z b

goal (1 subgoal):
 1. insertion f (liftPoly 0 z (a + b)) = insertion f (liftPoly 0 z a + liftPoly 0 z b)
[PROOF STEP]
by simp


[STATEMENT]
lemma lower_power_zero : "lowerPowers a b 0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lowerPowers a b 0 = 0
[PROOF STEP]
unfolding lowerPowers_def dec_above_def id_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_fun (\<lambda>x. x) (map_fun (\<lambda>x. x) (map_fun lookup Abs_poly_mapping)) (\<lambda>b i p x. if x \<in> {b..<b + i} then 0::'a else p (if x \<le> b then x else x - i)) a b 0 = 0
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_poly_mapping (\<lambda>x. if a \<le> x \<and> x < a + b then 0::'a else lookup 0 (if x \<le> a then x else x - b)) = 0
[PROOF STEP]
unfolding Poly_Mapping.lookup_zero
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_poly_mapping (\<lambda>x. if a \<le> x \<and> x < a + b then 0::'a else (0::'a)) = 0
[PROOF STEP]
by auto


[STATEMENT]
lemma lift_vars_monom : "vars (liftPoly i j ((MPoly_Type.monom m a)::real mpoly)) = (\<lambda>x. if x\<ge>i then x+j else x) ` vars(MPoly_Type.monom m a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars (liftPoly i j (MPoly_Type.monom m a)) = (\<lambda>x. if i \<le> x then x + j else x) ` vars (MPoly_Type.monom m a)
[PROOF STEP]
proof(cases "a=0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a = 0 \<Longrightarrow> vars (liftPoly i j (MPoly_Type.monom m a)) = (\<lambda>x. if i \<le> x then x + j else x) ` vars (MPoly_Type.monom m a)
 2. a \<noteq> 0 \<Longrightarrow> vars (liftPoly i j (MPoly_Type.monom m a)) = (\<lambda>x. if i \<le> x then x + j else x) ` vars (MPoly_Type.monom m a)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
a = 0

goal (2 subgoals):
 1. a = 0 \<Longrightarrow> vars (liftPoly i j (MPoly_Type.monom m a)) = (\<lambda>x. if i \<le> x then x + j else x) ` vars (MPoly_Type.monom m a)
 2. a \<noteq> 0 \<Longrightarrow> vars (liftPoly i j (MPoly_Type.monom m a)) = (\<lambda>x. if i \<le> x then x + j else x) ` vars (MPoly_Type.monom m a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a = 0

goal (1 subgoal):
 1. vars (liftPoly i j (MPoly_Type.monom m a)) = (\<lambda>x. if i \<le> x then x + j else x) ` vars (MPoly_Type.monom m a)
[PROOF STEP]
by (smt MPolyExtension.monom_zero add.left_neutral add_diff_cancel_right' image_empty liftPoly_add vars_monom_single_cases)
[PROOF STATE]
proof (state)
this:
vars (liftPoly i j (MPoly_Type.monom m a)) = (\<lambda>x. if i \<le> x then x + j else x) ` vars (MPoly_Type.monom m a)

goal (1 subgoal):
 1. a \<noteq> 0 \<Longrightarrow> vars (liftPoly i j (MPoly_Type.monom m a)) = (\<lambda>x. if i \<le> x then x + j else x) ` vars (MPoly_Type.monom m a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<noteq> 0 \<Longrightarrow> vars (liftPoly i j (MPoly_Type.monom m a)) = (\<lambda>x. if i \<le> x then x + j else x) ` vars (MPoly_Type.monom m a)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
a \<noteq> 0

goal (1 subgoal):
 1. a \<noteq> 0 \<Longrightarrow> vars (liftPoly i j (MPoly_Type.monom m a)) = (\<lambda>x. if i \<le> x then x + j else x) ` vars (MPoly_Type.monom m a)
[PROOF STEP]
have h1: "vars (liftPoly i j (MPoly_Type.monom m a)) = keys (lowerPowers i j m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars (liftPoly i j (MPoly_Type.monom m a)) = keys (lowerPowers i j m)
[PROOF STEP]
unfolding liftPoly_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars (map_fun id (map_fun id (map_fun mapping_of MPoly)) higherPoly\<^sub>0 i j (MPoly_Type.monom m a)) = keys (lowerPowers i j m)
[PROOF STEP]
unfolding keys_lowerPowers keys_higherPoly\<^sub>0 vars_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (keys ` keys (mapping_of (map_fun id (map_fun id (map_fun mapping_of MPoly)) higherPoly\<^sub>0 i j (MPoly_Type.monom m a)))) = inc_above i j ` keys m
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>xa \<in> keys (mapping_of (MPoly (higherPoly\<^sub>0 i j (monomial a m)))); x \<in> keys xa\<rbrakk> \<Longrightarrow> x \<in> inc_above i j ` keys m
 2. \<And>xa. xa \<in> keys m \<Longrightarrow> \<exists>x\<in>keys (mapping_of (MPoly (higherPoly\<^sub>0 i j (monomial a m)))). inc_above i j xa \<in> keys x
[PROOF STEP]
apply (smt imageE keys_higherPoly\<^sub>0 keys_lowerPowers lookup_eq_zero_in_keys_contradict lookup_single_not_eq mapping_of_inverse monomials.abs_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. xa \<in> keys m \<Longrightarrow> \<exists>x\<in>keys (mapping_of (MPoly (higherPoly\<^sub>0 i j (monomial a m)))). inc_above i j xa \<in> keys x
[PROOF STEP]
by (metis False higherPowers.rep_eq higherPowers_lowerPowers image_eqI in_keys_iff keys_higherPoly\<^sub>0 lookup_single_eq mapping_of_inverse monomials.abs_eq)
[PROOF STATE]
proof (state)
this:
vars (liftPoly i j (MPoly_Type.monom m a)) = keys (lowerPowers i j m)

goal (1 subgoal):
 1. a \<noteq> 0 \<Longrightarrow> vars (liftPoly i j (MPoly_Type.monom m a)) = (\<lambda>x. if i \<le> x then x + j else x) ` vars (MPoly_Type.monom m a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars (liftPoly i j (MPoly_Type.monom m a)) = (\<lambda>x. if i \<le> x then x + j else x) ` vars (MPoly_Type.monom m a)
[PROOF STEP]
unfolding h1  vars_monom_keys[OF False]
      keys_lowerPowers inc_above_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. if x < i then x else x + j) ` keys m = (\<lambda>x. if i \<le> x then x + j else x) ` keys m
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vars (liftPoly i j (MPoly_Type.monom m a)) = (\<lambda>x. if i \<le> x then x + j else x) ` vars (MPoly_Type.monom m a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lift_clear_vars : "vars (liftPoly i j (p::real mpoly)) \<inter> {i..<i + j} = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars (liftPoly i j p) \<inter> {i..<i + j} = {}
[PROOF STEP]
proof(induction p rule: mpoly_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>m a. vars (liftPoly i j (MPoly_Type.monom m a)) \<inter> {i..<i + j} = {}
 2. \<And>p1 p2 m a. \<lbrakk>vars (liftPoly i j p1) \<inter> {i..<i + j} = {}; vars (liftPoly i j p2) \<inter> {i..<i + j} = {}; p2 = MPoly_Type.monom m a; m \<notin> monomials p1; a \<noteq> 0\<rbrakk> \<Longrightarrow> vars (liftPoly i j (p1 + p2)) \<inter> {i..<i + j} = {}
[PROOF STEP]
case (monom m a)
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>m a. vars (liftPoly i j (MPoly_Type.monom m a)) \<inter> {i..<i + j} = {}
 2. \<And>p1 p2 m a. \<lbrakk>vars (liftPoly i j p1) \<inter> {i..<i + j} = {}; vars (liftPoly i j p2) \<inter> {i..<i + j} = {}; p2 = MPoly_Type.monom m a; m \<notin> monomials p1; a \<noteq> 0\<rbrakk> \<Longrightarrow> vars (liftPoly i j (p1 + p2)) \<inter> {i..<i + j} = {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars (liftPoly i j (MPoly_Type.monom m a)) \<inter> {i..<i + j} = {}
[PROOF STEP]
unfolding lift_vars_monom
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. if i \<le> x then x + j else x) ` vars (MPoly_Type.monom m a) \<inter> {i..<i + j} = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vars (liftPoly i j (MPoly_Type.monom m a)) \<inter> {i..<i + j} = {}

goal (1 subgoal):
 1. \<And>p1 p2 m a. \<lbrakk>vars (liftPoly i j p1) \<inter> {i..<i + j} = {}; vars (liftPoly i j p2) \<inter> {i..<i + j} = {}; p2 = MPoly_Type.monom m a; m \<notin> monomials p1; a \<noteq> 0\<rbrakk> \<Longrightarrow> vars (liftPoly i j (p1 + p2)) \<inter> {i..<i + j} = {}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p1 p2 m a. \<lbrakk>vars (liftPoly i j p1) \<inter> {i..<i + j} = {}; vars (liftPoly i j p2) \<inter> {i..<i + j} = {}; p2 = MPoly_Type.monom m a; m \<notin> monomials p1; a \<noteq> 0\<rbrakk> \<Longrightarrow> vars (liftPoly i j (p1 + p2)) \<inter> {i..<i + j} = {}
[PROOF STEP]
case (sum p1 p2 m a)
[PROOF STATE]
proof (state)
this:
vars (liftPoly i j p1) \<inter> {i..<i + j} = {}
vars (liftPoly i j p2) \<inter> {i..<i + j} = {}
p2 = MPoly_Type.monom m a
m \<notin> monomials p1
a \<noteq> 0

goal (1 subgoal):
 1. \<And>p1 p2 m a. \<lbrakk>vars (liftPoly i j p1) \<inter> {i..<i + j} = {}; vars (liftPoly i j p2) \<inter> {i..<i + j} = {}; p2 = MPoly_Type.monom m a; m \<notin> monomials p1; a \<noteq> 0\<rbrakk> \<Longrightarrow> vars (liftPoly i j (p1 + p2)) \<inter> {i..<i + j} = {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
vars (liftPoly i j p1) \<inter> {i..<i + j} = {}
vars (liftPoly i j p2) \<inter> {i..<i + j} = {}
p2 = MPoly_Type.monom m a
m \<notin> monomials p1
a \<noteq> 0
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
vars (liftPoly i j p1) \<inter> {i..<i + j} = {}
vars (liftPoly i j p2) \<inter> {i..<i + j} = {}
p2 = MPoly_Type.monom m a
m \<notin> monomials p1
a \<noteq> 0

goal (1 subgoal):
 1. vars (liftPoly i j (p1 + p2)) \<inter> {i..<i + j} = {}
[PROOF STEP]
using vars_lift_add[of i j p1 p2]
[PROOF STATE]
proof (prove)
using this:
vars (liftPoly i j p1) \<inter> {i..<i + j} = {}
vars (liftPoly i j p2) \<inter> {i..<i + j} = {}
p2 = MPoly_Type.monom m a
m \<notin> monomials p1
a \<noteq> 0
vars (liftPoly i j (p1 + p2)) \<subseteq> vars (liftPoly i j p1) \<union> vars (liftPoly i j p2)

goal (1 subgoal):
 1. vars (liftPoly i j (p1 + p2)) \<inter> {i..<i + j} = {}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
vars (liftPoly i j (p1 + p2)) \<inter> {i..<i + j} = {}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lift0: "(liftPoly i j 0) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. liftPoly i j 0 = 0
[PROOF STEP]
by (simp add: coeff_liftPoly mpoly_eq_iff)


[STATEMENT]
lemma lower0: "(lowerPoly i j 0) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lowerPoly i j 0 = 0
[PROOF STEP]
by (simp add: coeff_all_0 coeff_lowerPoly)


[STATEMENT]
lemma lower_lift_monom : "insertion f (MPoly_Type.monom m a :: real mpoly) = insertion f (lowerPoly i j (liftPoly i j (MPoly_Type.monom  m a)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion f (MPoly_Type.monom m a) = insertion f (lowerPoly i j (liftPoly i j (MPoly_Type.monom m a)))
[PROOF STEP]
proof (cases "a=0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a = 0 \<Longrightarrow> insertion f (MPoly_Type.monom m a) = insertion f (lowerPoly i j (liftPoly i j (MPoly_Type.monom m a)))
 2. a \<noteq> 0 \<Longrightarrow> insertion f (MPoly_Type.monom m a) = insertion f (lowerPoly i j (liftPoly i j (MPoly_Type.monom m a)))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
a = 0

goal (2 subgoals):
 1. a = 0 \<Longrightarrow> insertion f (MPoly_Type.monom m a) = insertion f (lowerPoly i j (liftPoly i j (MPoly_Type.monom m a)))
 2. a \<noteq> 0 \<Longrightarrow> insertion f (MPoly_Type.monom m a) = insertion f (lowerPoly i j (liftPoly i j (MPoly_Type.monom m a)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion f (MPoly_Type.monom m a) = insertion f (lowerPoly i j (liftPoly i j (MPoly_Type.monom m a)))
[PROOF STEP]
unfolding True lift0 monom_zero lower0
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion f 0 = insertion f 0
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
insertion f (MPoly_Type.monom m a) = insertion f (lowerPoly i j (liftPoly i j (MPoly_Type.monom m a)))

goal (1 subgoal):
 1. a \<noteq> 0 \<Longrightarrow> insertion f (MPoly_Type.monom m a) = insertion f (lowerPoly i j (liftPoly i j (MPoly_Type.monom m a)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<noteq> 0 \<Longrightarrow> insertion f (MPoly_Type.monom m a) = insertion f (lowerPoly i j (liftPoly i j (MPoly_Type.monom m a)))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
a \<noteq> 0

goal (1 subgoal):
 1. a \<noteq> 0 \<Longrightarrow> insertion f (MPoly_Type.monom m a) = insertion f (lowerPoly i j (liftPoly i j (MPoly_Type.monom m a)))
[PROOF STEP]
have h1 :  "higherPowers i j ` ({lowerPowers i j m} \<inter> {x. \<forall>j\<in>{i..<i + j}. lookup x j = 0}) = {m}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higherPowers i j ` ({lowerPowers i j m} \<inter> {x. \<forall>j\<in>{i..<i + j}. lookup x j = 0}) = {m}
[PROOF STEP]
apply (simp add: lowerPowers.rep_eq higherPowers.rep_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higherPowers i j (lowerPowers i j m) = m
[PROOF STEP]
using higherPowers_lowerPowers
[PROOF STATE]
proof (prove)
using this:
higherPowers ?n ?i (lowerPowers ?n ?i ?x) = ?x

goal (1 subgoal):
 1. higherPowers i j (lowerPowers i j m) = m
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
higherPowers i j ` ({lowerPowers i j m} \<inter> {x. \<forall>j\<in>{i..<i + j}. lookup x j = 0}) = {m}

goal (1 subgoal):
 1. a \<noteq> 0 \<Longrightarrow> insertion f (MPoly_Type.monom m a) = insertion f (lowerPoly i j (liftPoly i j (MPoly_Type.monom m a)))
[PROOF STEP]
have higher_lower : "higherPowers i j (lowerPowers i j m) = m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higherPowers i j (lowerPowers i j m) = m
[PROOF STEP]
using higherPowers_lowerPowers
[PROOF STATE]
proof (prove)
using this:
higherPowers ?n ?i (lowerPowers ?n ?i ?x) = ?x

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

goal (1 subgoal):
 1. a \<noteq> 0 \<Longrightarrow> insertion f (MPoly_Type.monom m a) = insertion f (lowerPoly i j (liftPoly i j (MPoly_Type.monom m a)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion f (MPoly_Type.monom m a) = insertion f (lowerPoly i j (liftPoly i j (MPoly_Type.monom m a)))
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
a \<noteq> 0

goal (1 subgoal):
 1. insertion f (MPoly_Type.monom m a) = insertion f (lowerPoly i j (liftPoly i j (MPoly_Type.monom m a)))
[PROOF STEP]
unfolding insertion_code monomials_monom
[PROOF STATE]
proof (prove)
using this:
a \<noteq> 0

goal (1 subgoal):
 1. (\<Sum>ma\<in>(if a = 0 then {} else {m}). MPoly_Type.coeff (MPoly_Type.monom m a) ma * (\<Prod>k\<in>keys ma. f k ^ lookup ma k)) = (\<Sum>ma\<in>monomials (lowerPoly i j (liftPoly i j (MPoly_Type.monom m a))). MPoly_Type.coeff (lowerPoly i j (liftPoly i j (MPoly_Type.monom m a))) ma * (\<Prod>k\<in>keys ma. f k ^ lookup ma k))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<noteq> 0 \<Longrightarrow> a * (\<Prod>k\<in>keys m. f k ^ lookup m k) = (\<Sum>ma\<in>monomials (lowerPoly i j (liftPoly i j (MPoly_Type.monom m a))). MPoly_Type.coeff (lowerPoly i j (liftPoly i j (MPoly_Type.monom m a))) ma * (\<Prod>k\<in>keys ma. f k ^ lookup ma k))
[PROOF STEP]
unfolding monomials_lowerPoly monomials_liftPoly
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<noteq> 0 \<Longrightarrow> a * (\<Prod>k\<in>keys m. f k ^ lookup m k) = (\<Sum>ma\<in>higherPowers i j ` (lowerPowers i j ` monomials (MPoly_Type.monom m a) \<inter> {x. \<forall>j\<in>{i..<i + j}. lookup x j = 0}). MPoly_Type.coeff (lowerPoly i j (liftPoly i j (MPoly_Type.monom m a))) ma * (\<Prod>k\<in>keys ma. f k ^ lookup ma k))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<noteq> 0 \<Longrightarrow> a * (\<Prod>k\<in>keys m. f k ^ lookup m k) = (\<Sum>ma\<in>higherPowers i j ` ({lowerPowers i j m} \<inter> {x. \<forall>j\<in>{i..<i + j}. lookup x j = 0}). MPoly_Type.coeff (lowerPoly i j (liftPoly i j (MPoly_Type.monom m a))) ma * (\<Prod>k\<in>keys ma. f k ^ lookup ma k))
[PROOF STEP]
unfolding More_MPoly_Type.coeff_monom  h1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<noteq> 0 \<Longrightarrow> a * (\<Prod>k\<in>keys m. f k ^ lookup m k) = (\<Sum>ma\<in>{m}. MPoly_Type.coeff (lowerPoly i j (liftPoly i j (MPoly_Type.monom m a))) ma * (\<Prod>k\<in>keys ma. f k ^ lookup ma k))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<noteq> 0; a \<noteq> MPoly_Type.coeff (lowerPoly i j (liftPoly i j (MPoly_Type.monom m a))) m\<rbrakk> \<Longrightarrow> \<exists>a\<in>keys m. f a = 0 \<and> 0 < lookup m a
[PROOF STEP]
unfolding coeff_lowerPoly coeff_liftPoly higherPowers_lowerPowers coeff_monom
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<noteq> 0; a \<noteq> (if \<exists>ja\<in>{i..<i + j}. 0 < lookup (lowerPowers i j m) ja then 0 else a)\<rbrakk> \<Longrightarrow> \<exists>a\<in>keys m. f a = 0 \<and> 0 < lookup m a
[PROOF STEP]
apply(cases "\<exists>ja\<in>{i..<i + j}. 0 < lookup (lowerPowers i j m) ja")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<noteq> 0; a \<noteq> (if \<exists>ja\<in>{i..<i + j}. 0 < lookup (lowerPowers i j m) ja then 0 else a); \<exists>ja\<in>{i..<i + j}. 0 < lookup (lowerPowers i j m) ja\<rbrakk> \<Longrightarrow> \<exists>a\<in>keys m. f a = 0 \<and> 0 < lookup m a
 2. \<lbrakk>a \<noteq> 0; a \<noteq> (if \<exists>ja\<in>{i..<i + j}. 0 < lookup (lowerPowers i j m) ja then 0 else a); \<not> (\<exists>ja\<in>{i..<i + j}. 0 < lookup (lowerPowers i j m) ja)\<rbrakk> \<Longrightarrow> \<exists>a\<in>keys m. f a = 0 \<and> 0 < lookup m a
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ja. \<lbrakk>a \<noteq> 0; 0 < lookup (lowerPowers i j m) ja; i \<le> ja; ja < i + j\<rbrakk> \<Longrightarrow> \<exists>a\<in>keys m. f a = 0 \<and> 0 < lookup m a
[PROOF STEP]
by (simp add: lowerPowers_eq)
[PROOF STATE]
proof (state)
this:
insertion f (MPoly_Type.monom m a) = insertion f (lowerPoly i j (liftPoly i j (MPoly_Type.monom m a)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lower_lift : "insertion f (p::real mpoly) = insertion f (lowerPoly i j (liftPoly i j p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion f p = insertion f (lowerPoly i j (liftPoly i j p))
[PROOF STEP]
unfolding insertion_code
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>m\<in>monomials p. MPoly_Type.coeff p m * (\<Prod>k\<in>keys m. f k ^ lookup m k)) = (\<Sum>m\<in>monomials (lowerPoly i j (liftPoly i j p)). MPoly_Type.coeff (lowerPoly i j (liftPoly i j p)) m * (\<Prod>k\<in>keys m. f k ^ lookup m k))
[PROOF STEP]
proof(induction p rule: mpoly_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>m a. (\<Sum>ma\<in>monomials (MPoly_Type.monom m a). MPoly_Type.coeff (MPoly_Type.monom m a) ma * (\<Prod>k\<in>keys ma. f k ^ lookup ma k)) = (\<Sum>ma\<in>monomials (lowerPoly i j (liftPoly i j (MPoly_Type.monom m a))). MPoly_Type.coeff (lowerPoly i j (liftPoly i j (MPoly_Type.monom m a))) ma * (\<Prod>k\<in>keys ma. f k ^ lookup ma k))
 2. \<And>p1 p2 m a. \<lbrakk>(\<Sum>m\<in>monomials p1. MPoly_Type.coeff p1 m * (\<Prod>k\<in>keys m. f k ^ lookup m k)) = (\<Sum>m\<in>monomials (lowerPoly i j (liftPoly i j p1)). MPoly_Type.coeff (lowerPoly i j (liftPoly i j p1)) m * (\<Prod>k\<in>keys m. f k ^ lookup m k)); (\<Sum>m\<in>monomials p2. MPoly_Type.coeff p2 m * (\<Prod>k\<in>keys m. f k ^ lookup m k)) = (\<Sum>m\<in>monomials (lowerPoly i j (liftPoly i j p2)). MPoly_Type.coeff (lowerPoly i j (liftPoly i j p2)) m * (\<Prod>k\<in>keys m. f k ^ lookup m k)); p2 = MPoly_Type.monom m a; m \<notin> monomials p1; a \<noteq> 0\<rbrakk> \<Longrightarrow> (\<Sum>m\<in>monomials (p1 + p2). MPoly_Type.coeff (p1 + p2) m * (\<Prod>k\<in>keys m. f k ^ lookup m k)) = (\<Sum>m\<in>monomials (lowerPoly i j (liftPoly i j (p1 + p2))). MPoly_Type.coeff (lowerPoly i j (liftPoly i j (p1 + p2))) m * (\<Prod>k\<in>keys m. f k ^ lookup m k))
[PROOF STEP]
case (monom m a)
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>m a. (\<Sum>ma\<in>monomials (MPoly_Type.monom m a). MPoly_Type.coeff (MPoly_Type.monom m a) ma * (\<Prod>k\<in>keys ma. f k ^ lookup ma k)) = (\<Sum>ma\<in>monomials (lowerPoly i j (liftPoly i j (MPoly_Type.monom m a))). MPoly_Type.coeff (lowerPoly i j (liftPoly i j (MPoly_Type.monom m a))) ma * (\<Prod>k\<in>keys ma. f k ^ lookup ma k))
 2. \<And>p1 p2 m a. \<lbrakk>(\<Sum>m\<in>monomials p1. MPoly_Type.coeff p1 m * (\<Prod>k\<in>keys m. f k ^ lookup m k)) = (\<Sum>m\<in>monomials (lowerPoly i j (liftPoly i j p1)). MPoly_Type.coeff (lowerPoly i j (liftPoly i j p1)) m * (\<Prod>k\<in>keys m. f k ^ lookup m k)); (\<Sum>m\<in>monomials p2. MPoly_Type.coeff p2 m * (\<Prod>k\<in>keys m. f k ^ lookup m k)) = (\<Sum>m\<in>monomials (lowerPoly i j (liftPoly i j p2)). MPoly_Type.coeff (lowerPoly i j (liftPoly i j p2)) m * (\<Prod>k\<in>keys m. f k ^ lookup m k)); p2 = MPoly_Type.monom m a; m \<notin> monomials p1; a \<noteq> 0\<rbrakk> \<Longrightarrow> (\<Sum>m\<in>monomials (p1 + p2). MPoly_Type.coeff (p1 + p2) m * (\<Prod>k\<in>keys m. f k ^ lookup m k)) = (\<Sum>m\<in>monomials (lowerPoly i j (liftPoly i j (p1 + p2))). MPoly_Type.coeff (lowerPoly i j (liftPoly i j (p1 + p2))) m * (\<Prod>k\<in>keys m. f k ^ lookup m k))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>ma\<in>monomials (MPoly_Type.monom m a). MPoly_Type.coeff (MPoly_Type.monom m a) ma * (\<Prod>k\<in>keys ma. f k ^ lookup ma k)) = (\<Sum>ma\<in>monomials (lowerPoly i j (liftPoly i j (MPoly_Type.monom m a))). MPoly_Type.coeff (lowerPoly i j (liftPoly i j (MPoly_Type.monom m a))) ma * (\<Prod>k\<in>keys ma. f k ^ lookup ma k))
[PROOF STEP]
using lower_lift_monom
[PROOF STATE]
proof (prove)
using this:
insertion ?f (MPoly_Type.monom ?m ?a) = insertion ?f (lowerPoly ?i ?j (liftPoly ?i ?j (MPoly_Type.monom ?m ?a)))

goal (1 subgoal):
 1. (\<Sum>ma\<in>monomials (MPoly_Type.monom m a). MPoly_Type.coeff (MPoly_Type.monom m a) ma * (\<Prod>k\<in>keys ma. f k ^ lookup ma k)) = (\<Sum>ma\<in>monomials (lowerPoly i j (liftPoly i j (MPoly_Type.monom m a))). MPoly_Type.coeff (lowerPoly i j (liftPoly i j (MPoly_Type.monom m a))) ma * (\<Prod>k\<in>keys ma. f k ^ lookup ma k))
[PROOF STEP]
unfolding insertion_code monomials_lowerPoly monomials_liftPoly coeff_lowerPoly coeff_liftPoly
[PROOF STATE]
proof (prove)
using this:
(\<Sum>m\<in>monomials (MPoly_Type.monom ?m ?a). MPoly_Type.coeff (MPoly_Type.monom ?m ?a) m * (\<Prod>k\<in>keys m. ?f k ^ lookup m k)) = (\<Sum>m\<in>higherPowers ?i ?j ` (lowerPowers ?i ?j ` monomials (MPoly_Type.monom ?m ?a) \<inter> {x. \<forall>j\<in>{?i..<?i + ?j}. lookup x j = 0}). (if \<exists>j\<in>{?i..<?i + ?j}. 0 < lookup (lowerPowers ?i ?j m) j then 0 else MPoly_Type.coeff (MPoly_Type.monom ?m ?a) (higherPowers ?i ?j (lowerPowers ?i ?j m))) * (\<Prod>k\<in>keys m. ?f k ^ lookup m k))

goal (1 subgoal):
 1. (\<Sum>ma\<in>monomials (MPoly_Type.monom m a). MPoly_Type.coeff (MPoly_Type.monom m a) ma * (\<Prod>k\<in>keys ma. f k ^ lookup ma k)) = (\<Sum>ma\<in>higherPowers i j ` (lowerPowers i j ` monomials (MPoly_Type.monom m a) \<inter> {x. \<forall>j\<in>{i..<i + j}. lookup x j = 0}). (if \<exists>ja\<in>{i..<i + j}. 0 < lookup (lowerPowers i j ma) ja then 0 else MPoly_Type.coeff (MPoly_Type.monom m a) (higherPowers i j (lowerPowers i j ma))) * (\<Prod>k\<in>keys ma. f k ^ lookup ma k))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>ma\<in>monomials (MPoly_Type.monom m a). MPoly_Type.coeff (MPoly_Type.monom m a) ma * (\<Prod>k\<in>keys ma. f k ^ lookup ma k)) = (\<Sum>ma\<in>monomials (lowerPoly i j (liftPoly i j (MPoly_Type.monom m a))). MPoly_Type.coeff (lowerPoly i j (liftPoly i j (MPoly_Type.monom m a))) ma * (\<Prod>k\<in>keys ma. f k ^ lookup ma k))

goal (1 subgoal):
 1. \<And>p1 p2 m a. \<lbrakk>(\<Sum>m\<in>monomials p1. MPoly_Type.coeff p1 m * (\<Prod>k\<in>keys m. f k ^ lookup m k)) = (\<Sum>m\<in>monomials (lowerPoly i j (liftPoly i j p1)). MPoly_Type.coeff (lowerPoly i j (liftPoly i j p1)) m * (\<Prod>k\<in>keys m. f k ^ lookup m k)); (\<Sum>m\<in>monomials p2. MPoly_Type.coeff p2 m * (\<Prod>k\<in>keys m. f k ^ lookup m k)) = (\<Sum>m\<in>monomials (lowerPoly i j (liftPoly i j p2)). MPoly_Type.coeff (lowerPoly i j (liftPoly i j p2)) m * (\<Prod>k\<in>keys m. f k ^ lookup m k)); p2 = MPoly_Type.monom m a; m \<notin> monomials p1; a \<noteq> 0\<rbrakk> \<Longrightarrow> (\<Sum>m\<in>monomials (p1 + p2). MPoly_Type.coeff (p1 + p2) m * (\<Prod>k\<in>keys m. f k ^ lookup m k)) = (\<Sum>m\<in>monomials (lowerPoly i j (liftPoly i j (p1 + p2))). MPoly_Type.coeff (lowerPoly i j (liftPoly i j (p1 + p2))) m * (\<Prod>k\<in>keys m. f k ^ lookup m k))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p1 p2 m a. \<lbrakk>(\<Sum>m\<in>monomials p1. MPoly_Type.coeff p1 m * (\<Prod>k\<in>keys m. f k ^ lookup m k)) = (\<Sum>m\<in>monomials (lowerPoly i j (liftPoly i j p1)). MPoly_Type.coeff (lowerPoly i j (liftPoly i j p1)) m * (\<Prod>k\<in>keys m. f k ^ lookup m k)); (\<Sum>m\<in>monomials p2. MPoly_Type.coeff p2 m * (\<Prod>k\<in>keys m. f k ^ lookup m k)) = (\<Sum>m\<in>monomials (lowerPoly i j (liftPoly i j p2)). MPoly_Type.coeff (lowerPoly i j (liftPoly i j p2)) m * (\<Prod>k\<in>keys m. f k ^ lookup m k)); p2 = MPoly_Type.monom m a; m \<notin> monomials p1; a \<noteq> 0\<rbrakk> \<Longrightarrow> (\<Sum>m\<in>monomials (p1 + p2). MPoly_Type.coeff (p1 + p2) m * (\<Prod>k\<in>keys m. f k ^ lookup m k)) = (\<Sum>m\<in>monomials (lowerPoly i j (liftPoly i j (p1 + p2))). MPoly_Type.coeff (lowerPoly i j (liftPoly i j (p1 + p2))) m * (\<Prod>k\<in>keys m. f k ^ lookup m k))
[PROOF STEP]
case (sum p1 p2 m a)
[PROOF STATE]
proof (state)
this:
(\<Sum>m\<in>monomials p1. MPoly_Type.coeff p1 m * (\<Prod>k\<in>keys m. f k ^ lookup m k)) = (\<Sum>m\<in>monomials (lowerPoly i j (liftPoly i j p1)). MPoly_Type.coeff (lowerPoly i j (liftPoly i j p1)) m * (\<Prod>k\<in>keys m. f k ^ lookup m k))
(\<Sum>m\<in>monomials p2. MPoly_Type.coeff p2 m * (\<Prod>k\<in>keys m. f k ^ lookup m k)) = (\<Sum>m\<in>monomials (lowerPoly i j (liftPoly i j p2)). MPoly_Type.coeff (lowerPoly i j (liftPoly i j p2)) m * (\<Prod>k\<in>keys m. f k ^ lookup m k))
p2 = MPoly_Type.monom m a
m \<notin> monomials p1
a \<noteq> 0

goal (1 subgoal):
 1. \<And>p1 p2 m a. \<lbrakk>(\<Sum>m\<in>monomials p1. MPoly_Type.coeff p1 m * (\<Prod>k\<in>keys m. f k ^ lookup m k)) = (\<Sum>m\<in>monomials (lowerPoly i j (liftPoly i j p1)). MPoly_Type.coeff (lowerPoly i j (liftPoly i j p1)) m * (\<Prod>k\<in>keys m. f k ^ lookup m k)); (\<Sum>m\<in>monomials p2. MPoly_Type.coeff p2 m * (\<Prod>k\<in>keys m. f k ^ lookup m k)) = (\<Sum>m\<in>monomials (lowerPoly i j (liftPoly i j p2)). MPoly_Type.coeff (lowerPoly i j (liftPoly i j p2)) m * (\<Prod>k\<in>keys m. f k ^ lookup m k)); p2 = MPoly_Type.monom m a; m \<notin> monomials p1; a \<noteq> 0\<rbrakk> \<Longrightarrow> (\<Sum>m\<in>monomials (p1 + p2). MPoly_Type.coeff (p1 + p2) m * (\<Prod>k\<in>keys m. f k ^ lookup m k)) = (\<Sum>m\<in>monomials (lowerPoly i j (liftPoly i j (p1 + p2))). MPoly_Type.coeff (lowerPoly i j (liftPoly i j (p1 + p2))) m * (\<Prod>k\<in>keys m. f k ^ lookup m k))
[PROOF STEP]
have h1 : "monomials p1 \<inter> monomials p2 = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monomials p1 \<inter> monomials p2 = {}
[PROOF STEP]
using sum
[PROOF STATE]
proof (prove)
using this:
(\<Sum>m\<in>monomials p1. MPoly_Type.coeff p1 m * (\<Prod>k\<in>keys m. f k ^ lookup m k)) = (\<Sum>m\<in>monomials (lowerPoly i j (liftPoly i j p1)). MPoly_Type.coeff (lowerPoly i j (liftPoly i j p1)) m * (\<Prod>k\<in>keys m. f k ^ lookup m k))
(\<Sum>m\<in>monomials p2. MPoly_Type.coeff p2 m * (\<Prod>k\<in>keys m. f k ^ lookup m k)) = (\<Sum>m\<in>monomials (lowerPoly i j (liftPoly i j p2)). MPoly_Type.coeff (lowerPoly i j (liftPoly i j p2)) m * (\<Prod>k\<in>keys m. f k ^ lookup m k))
p2 = MPoly_Type.monom m a
m \<notin> monomials p1
a \<noteq> 0

goal (1 subgoal):
 1. monomials p1 \<inter> monomials p2 = {}
[PROOF STEP]
by (metis Int_insert_right_if0 inf_bot_right monomials_monom)
[PROOF STATE]
proof (state)
this:
monomials p1 \<inter> monomials p2 = {}

goal (1 subgoal):
 1. \<And>p1 p2 m a. \<lbrakk>(\<Sum>m\<in>monomials p1. MPoly_Type.coeff p1 m * (\<Prod>k\<in>keys m. f k ^ lookup m k)) = (\<Sum>m\<in>monomials (lowerPoly i j (liftPoly i j p1)). MPoly_Type.coeff (lowerPoly i j (liftPoly i j p1)) m * (\<Prod>k\<in>keys m. f k ^ lookup m k)); (\<Sum>m\<in>monomials p2. MPoly_Type.coeff p2 m * (\<Prod>k\<in>keys m. f k ^ lookup m k)) = (\<Sum>m\<in>monomials (lowerPoly i j (liftPoly i j p2)). MPoly_Type.coeff (lowerPoly i j (liftPoly i j p2)) m * (\<Prod>k\<in>keys m. f k ^ lookup m k)); p2 = MPoly_Type.monom m a; m \<notin> monomials p1; a \<noteq> 0\<rbrakk> \<Longrightarrow> (\<Sum>m\<in>monomials (p1 + p2). MPoly_Type.coeff (p1 + p2) m * (\<Prod>k\<in>keys m. f k ^ lookup m k)) = (\<Sum>m\<in>monomials (lowerPoly i j (liftPoly i j (p1 + p2))). MPoly_Type.coeff (lowerPoly i j (liftPoly i j (p1 + p2))) m * (\<Prod>k\<in>keys m. f k ^ lookup m k))
[PROOF STEP]
have h4 : "monomials (lowerPoly i j (liftPoly i j (p1 + p2))) = monomials (lowerPoly i j (liftPoly i j (p1))) \<union> monomials (lowerPoly i j (liftPoly i j (p2)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monomials (lowerPoly i j (liftPoly i j (p1 + p2))) = monomials (lowerPoly i j (liftPoly i j p1)) \<union> monomials (lowerPoly i j (liftPoly i j p2))
[PROOF STEP]
using monomials_lowerPoly monomials_liftPoly monomials_add_disjoint[OF h1]
[PROOF STATE]
proof (prove)
using this:
monomials (lowerPoly ?b ?i ?mp) = higherPowers ?b ?i ` (monomials ?mp \<inter> {x. \<forall>j\<in>{?b..<?b + ?i}. lookup x j = 0})
monomials (liftPoly ?b ?i ?mp) = lowerPowers ?b ?i ` monomials ?mp
monomials (p1 + p2) = monomials p1 \<union> monomials p2

goal (1 subgoal):
 1. monomials (lowerPoly i j (liftPoly i j (p1 + p2))) = monomials (lowerPoly i j (liftPoly i j p1)) \<union> monomials (lowerPoly i j (liftPoly i j p2))
[PROOF STEP]
by (simp add: monomials_liftPoly monomials_lowerPoly Int_Un_distrib2 image_Un)
[PROOF STATE]
proof (state)
this:
monomials (lowerPoly i j (liftPoly i j (p1 + p2))) = monomials (lowerPoly i j (liftPoly i j p1)) \<union> monomials (lowerPoly i j (liftPoly i j p2))

goal (1 subgoal):
 1. \<And>p1 p2 m a. \<lbrakk>(\<Sum>m\<in>monomials p1. MPoly_Type.coeff p1 m * (\<Prod>k\<in>keys m. f k ^ lookup m k)) = (\<Sum>m\<in>monomials (lowerPoly i j (liftPoly i j p1)). MPoly_Type.coeff (lowerPoly i j (liftPoly i j p1)) m * (\<Prod>k\<in>keys m. f k ^ lookup m k)); (\<Sum>m\<in>monomials p2. MPoly_Type.coeff p2 m * (\<Prod>k\<in>keys m. f k ^ lookup m k)) = (\<Sum>m\<in>monomials (lowerPoly i j (liftPoly i j p2)). MPoly_Type.coeff (lowerPoly i j (liftPoly i j p2)) m * (\<Prod>k\<in>keys m. f k ^ lookup m k)); p2 = MPoly_Type.monom m a; m \<notin> monomials p1; a \<noteq> 0\<rbrakk> \<Longrightarrow> (\<Sum>m\<in>monomials (p1 + p2). MPoly_Type.coeff (p1 + p2) m * (\<Prod>k\<in>keys m. f k ^ lookup m k)) = (\<Sum>m\<in>monomials (lowerPoly i j (liftPoly i j (p1 + p2))). MPoly_Type.coeff (lowerPoly i j (liftPoly i j (p1 + p2))) m * (\<Prod>k\<in>keys m. f k ^ lookup m k))
[PROOF STEP]
have h5 : "MPoly_Type.coeff (lowerPoly i j (liftPoly i j (p1 + p2))) = MPoly_Type.coeff (lowerPoly i j (liftPoly i j (p1))) + MPoly_Type.coeff (lowerPoly i j (liftPoly i j (p2)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MPoly_Type.coeff (lowerPoly i j (liftPoly i j (p1 + p2))) = MPoly_Type.coeff (lowerPoly i j (liftPoly i j p1)) + MPoly_Type.coeff (lowerPoly i j (liftPoly i j p2))
[PROOF STEP]
unfolding coeff_lowerPoly coeff_liftPoly MPolyExtension.coeff_add
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. if \<exists>ja\<in>{i..<i + j}. 0 < lookup (lowerPowers i j x) ja then 0 else MPoly_Type.coeff p1 (higherPowers i j (lowerPowers i j x)) + MPoly_Type.coeff p2 (higherPowers i j (lowerPowers i j x))) = (\<lambda>x. if \<exists>ja\<in>{i..<i + j}. 0 < lookup (lowerPowers i j x) ja then 0 else MPoly_Type.coeff p1 (higherPowers i j (lowerPowers i j x))) + (\<lambda>x. if \<exists>ja\<in>{i..<i + j}. 0 < lookup (lowerPowers i j x) ja then 0 else MPoly_Type.coeff p2 (higherPowers i j (lowerPowers i j x)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
MPoly_Type.coeff (lowerPoly i j (liftPoly i j (p1 + p2))) = MPoly_Type.coeff (lowerPoly i j (liftPoly i j p1)) + MPoly_Type.coeff (lowerPoly i j (liftPoly i j p2))

goal (1 subgoal):
 1. \<And>p1 p2 m a. \<lbrakk>(\<Sum>m\<in>monomials p1. MPoly_Type.coeff p1 m * (\<Prod>k\<in>keys m. f k ^ lookup m k)) = (\<Sum>m\<in>monomials (lowerPoly i j (liftPoly i j p1)). MPoly_Type.coeff (lowerPoly i j (liftPoly i j p1)) m * (\<Prod>k\<in>keys m. f k ^ lookup m k)); (\<Sum>m\<in>monomials p2. MPoly_Type.coeff p2 m * (\<Prod>k\<in>keys m. f k ^ lookup m k)) = (\<Sum>m\<in>monomials (lowerPoly i j (liftPoly i j p2)). MPoly_Type.coeff (lowerPoly i j (liftPoly i j p2)) m * (\<Prod>k\<in>keys m. f k ^ lookup m k)); p2 = MPoly_Type.monom m a; m \<notin> monomials p1; a \<noteq> 0\<rbrakk> \<Longrightarrow> (\<Sum>m\<in>monomials (p1 + p2). MPoly_Type.coeff (p1 + p2) m * (\<Prod>k\<in>keys m. f k ^ lookup m k)) = (\<Sum>m\<in>monomials (lowerPoly i j (liftPoly i j (p1 + p2))). MPoly_Type.coeff (lowerPoly i j (liftPoly i j (p1 + p2))) m * (\<Prod>k\<in>keys m. f k ^ lookup m k))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>m\<in>monomials (p1 + p2). MPoly_Type.coeff (p1 + p2) m * (\<Prod>k\<in>keys m. f k ^ lookup m k)) = (\<Sum>m\<in>monomials (lowerPoly i j (liftPoly i j (p1 + p2))). MPoly_Type.coeff (lowerPoly i j (liftPoly i j (p1 + p2))) m * (\<Prod>k\<in>keys m. f k ^ lookup m k))
[PROOF STEP]
unfolding MPolyExtension.coeff_add
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>m\<in>monomials (p1 + p2). (MPoly_Type.coeff p1 m + MPoly_Type.coeff p2 m) * (\<Prod>k\<in>keys m. f k ^ lookup m k)) = (\<Sum>m\<in>monomials (lowerPoly i j (liftPoly i j (p1 + p2))). MPoly_Type.coeff (lowerPoly i j (liftPoly i j (p1 + p2))) m * (\<Prod>k\<in>keys m. f k ^ lookup m k))
[PROOF STEP]
unfolding h4 h5
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>m\<in>monomials (p1 + p2). (MPoly_Type.coeff p1 m + MPoly_Type.coeff p2 m) * (\<Prod>k\<in>keys m. f k ^ lookup m k)) = (\<Sum>m\<in>monomials (lowerPoly i j (liftPoly i j p1)) \<union> monomials (lowerPoly i j (liftPoly i j p2)). (MPoly_Type.coeff (lowerPoly i j (liftPoly i j p1)) + MPoly_Type.coeff (lowerPoly i j (liftPoly i j p2))) m * (\<Prod>k\<in>keys m. f k ^ lookup m k))
[PROOF STEP]
unfolding monomials_add_disjoint[OF h1]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>m\<in>monomials p1 \<union> monomials p2. (MPoly_Type.coeff p1 m + MPoly_Type.coeff p2 m) * (\<Prod>k\<in>keys m. f k ^ lookup m k)) = (\<Sum>m\<in>monomials (lowerPoly i j (liftPoly i j p1)) \<union> monomials (lowerPoly i j (liftPoly i j p2)). (MPoly_Type.coeff (lowerPoly i j (liftPoly i j p1)) + MPoly_Type.coeff (lowerPoly i j (liftPoly i j p2))) m * (\<Prod>k\<in>keys m. f k ^ lookup m k))
[PROOF STEP]
by (smt IntE coeff_eq_zero_iff disjoint_iff_not_equal finite_monomials h1 higherPowers_lowerPowers imageE monomials_liftPoly monomials_lowerPoly plus_fun_apply sum.IH(1) sum.IH(2) sum.cong sum.union_disjoint
        )
[PROOF STATE]
proof (state)
this:
(\<Sum>m\<in>monomials (p1 + p2). MPoly_Type.coeff (p1 + p2) m * (\<Prod>k\<in>keys m. f k ^ lookup m k)) = (\<Sum>m\<in>monomials (lowerPoly i j (liftPoly i j (p1 + p2))). MPoly_Type.coeff (lowerPoly i j (liftPoly i j (p1 + p2))) m * (\<Prod>k\<in>keys m. f k ^ lookup m k))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lift_insertion : " \<forall>init.
       length init = (i::nat) \<longrightarrow>
       (\<forall>I xs.
           (insertion (nth_default 0 (init @ xs)) (p::real mpoly)) = (insertion ((nth_default 0) (init @ I @ xs)) (liftPoly i (length I) p)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>init. length init = i \<longrightarrow> (\<forall>I xs. insertion (nth_default 0 (init @ xs)) p = insertion (nth_default 0 (init @ I @ xs)) (liftPoly i (length I) p))
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>init I xs. i = length init \<Longrightarrow> insertion (nth_default 0 (init @ xs)) p = insertion (nth_default 0 (init @ I @ xs)) (liftPoly (length init) (length I) p)
[PROOF STEP]
fix init I xs
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>init I xs. i = length init \<Longrightarrow> insertion (nth_default 0 (init @ xs)) p = insertion (nth_default 0 (init @ I @ xs)) (liftPoly (length init) (length I) p)
[PROOF STEP]
assume "i = length (init::real list)"
[PROOF STATE]
proof (state)
this:
i = length init

goal (1 subgoal):
 1. \<And>init I xs. i = length init \<Longrightarrow> insertion (nth_default 0 (init @ xs)) p = insertion (nth_default 0 (init @ I @ xs)) (liftPoly (length init) (length I) p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i = length init
[PROOF STEP]
have i_len : "length init = i"
[PROOF STATE]
proof (prove)
using this:
i = length init

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

goal (1 subgoal):
 1. \<And>init I xs. i = length init \<Longrightarrow> insertion (nth_default 0 (init @ xs)) p = insertion (nth_default 0 (init @ I @ xs)) (liftPoly (length init) (length I) p)
[PROOF STEP]
have h: "higherPoly\<^sub>0 i (length (I::real list)) (mapping_of p) \<in> UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higherPoly\<^sub>0 i (length I) (mapping_of p) \<in> UNIV
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
higherPoly\<^sub>0 i (length I) (mapping_of p) \<in> UNIV

goal (1 subgoal):
 1. \<And>init I xs. i = length init \<Longrightarrow> insertion (nth_default 0 (init @ xs)) p = insertion (nth_default 0 (init @ I @ xs)) (liftPoly (length init) (length I) p)
[PROOF STEP]
have h2 : "vars (liftPoly i (length I) p) \<inter> {i..<i + length I} = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars (liftPoly i (length I) p) \<inter> {i..<i + length I} = {}
[PROOF STEP]
using lift_clear_vars
[PROOF STATE]
proof (prove)
using this:
vars (liftPoly ?i ?j ?p) \<inter> {?i..<?i + ?j} = {}

goal (1 subgoal):
 1. vars (liftPoly i (length I) p) \<inter> {i..<i + length I} = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vars (liftPoly i (length I) p) \<inter> {i..<i + length I} = {}

goal (1 subgoal):
 1. \<And>init I xs. i = length init \<Longrightarrow> insertion (nth_default 0 (init @ xs)) p = insertion (nth_default 0 (init @ I @ xs)) (liftPoly (length init) (length I) p)
[PROOF STEP]
show "insertion ((nth_default 0) (init @ xs)) p = insertion ((nth_default 0) (init @ I @ xs)) (liftPoly (length init) (length I) p) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion (nth_default 0 (init @ xs)) p = insertion (nth_default 0 (init @ I @ xs)) (liftPoly (length init) (length I) p)
[PROOF STEP]
using lower_lift insertion_lowerPoly[OF h2 i_len refl, of xs] i_len
[PROOF STATE]
proof (prove)
using this:
insertion ?f ?p = insertion ?f (lowerPoly ?i ?j (liftPoly ?i ?j ?p))
insertion (nth_default 0 (init @ xs)) (lowerPoly i (length I) (liftPoly i (length I) p)) = insertion (nth_default 0 (init @ I @ xs)) (liftPoly i (length I) p)
length init = i

goal (1 subgoal):
 1. insertion (nth_default 0 (init @ xs)) p = insertion (nth_default 0 (init @ I @ xs)) (liftPoly (length init) (length I) p)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
insertion (nth_default 0 (init @ xs)) p = insertion (nth_default 0 (init @ I @ xs)) (liftPoly (length init) (length I) p)

goal:
No subgoals!
[PROOF STEP]
qed