[STATEMENT]
lemma insertion_Var [simp]: "insertion f (Var i) = f i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion f (Var i) = f i
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. insertion f (Var i) = f i
[PROOF STEP]
have "insertion f (Var i) = (\<Sum>m. (1 when m = Poly_Mapping.single i 1) *
                                       (\<Prod>i. f i ^ lookup m i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion f (Var i) = (\<Sum>m. ((1::'a) when m = Poly_Mapping.single i 1) * (\<Prod>i. f i ^ lookup m i))
[PROOF STEP]
by (simp add: insertion_altdef coeff_Var)
[PROOF STATE]
proof (state)
this:
insertion f (Var i) = (\<Sum>m. ((1::'a) when m = Poly_Mapping.single i 1) * (\<Prod>i. f i ^ lookup m i))

goal (1 subgoal):
 1. insertion f (Var i) = f i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
insertion f (Var i) = (\<Sum>m. ((1::'a) when m = Poly_Mapping.single i 1) * (\<Prod>i. f i ^ lookup m i))

goal (1 subgoal):
 1. insertion f (Var i) = f i
[PROOF STEP]
have "\<dots> = (\<Prod>j. f j ^ lookup (Poly_Mapping.single i 1) j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>m. ((1::'a) when m = Poly_Mapping.single i 1) * (\<Prod>i. f i ^ lookup m i)) = (\<Prod>j. f j ^ lookup (Poly_Mapping.single i 1) j)
[PROOF STEP]
by (subst Sum_any.expand_superset[of "{Poly_Mapping.single i 1}"]) (auto simp: when_def)
[PROOF STATE]
proof (state)
this:
(\<Sum>m. ((1::'a) when m = Poly_Mapping.single i 1) * (\<Prod>i. f i ^ lookup m i)) = (\<Prod>j. f j ^ lookup (Poly_Mapping.single i 1) j)

goal (1 subgoal):
 1. insertion f (Var i) = f i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>m. ((1::'a) when m = Poly_Mapping.single i 1) * (\<Prod>i. f i ^ lookup m i)) = (\<Prod>j. f j ^ lookup (Poly_Mapping.single i 1) j)

goal (1 subgoal):
 1. insertion f (Var i) = f i
[PROOF STEP]
have "\<dots> = f i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>j. f j ^ lookup (Poly_Mapping.single i 1) j) = f i
[PROOF STEP]
by (subst Prod_any.expand_superset[of "{i}"]) (auto simp: when_def lookup_single)
[PROOF STATE]
proof (state)
this:
(\<Prod>j. f j ^ lookup (Poly_Mapping.single i 1) j) = f i

goal (1 subgoal):
 1. insertion f (Var i) = f i
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
insertion f (Var i) = f i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
insertion f (Var i) = f i

goal (1 subgoal):
 1. insertion f (Var i) = f i
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
insertion f (Var i) = f i

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma insertion_Sum_any:
  assumes "finite {x. g x \<noteq> 0}"
  shows   "insertion f (Sum_any g) = Sum_any (\<lambda>x. insertion f (g x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion f (Sum_any g) = (\<Sum>x. insertion f (g x))
[PROOF STEP]
unfolding Sum_any.expand_set insertion_sum
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>{a. g a \<noteq> 0}. insertion f (g x)) = (\<Sum>x\<in>{a. insertion f (g a) \<noteq> (0::'b)}. insertion f (g x))
[PROOF STEP]
by (intro sum.mono_neutral_right) (auto intro!: finite_subset[OF _ assms])


[STATEMENT]
lemma keys_diff_subset:
  "keys (f - g) \<subseteq> keys f \<union> keys g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. keys (f - g) \<subseteq> keys f \<union> keys g
[PROOF STEP]
by transfer auto


[STATEMENT]
lemma keys_empty_iff [simp]: "keys p = {} \<longleftrightarrow> p = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (keys p = {}) = (p = 0)
[PROOF STEP]
by transfer auto


[STATEMENT]
lemma mpoly_coeff_0 [simp]: "MPoly_Type.coeff 0 m = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MPoly_Type.coeff 0 m = (0::'a)
[PROOF STEP]
by transfer auto


[STATEMENT]
lemma lookup_1: "lookup 1 m = (if m = 0 then 1 else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup 1 m = (if m = (0::'b) then 1::'a else (0::'a))
[PROOF STEP]
by transfer (simp add: when_def)


[STATEMENT]
lemma mpoly_coeff_1: "MPoly_Type.coeff 1 m = (if m = 0 then 1 else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MPoly_Type.coeff 1 m = (if m = 0 then 1::'a else (0::'a))
[PROOF STEP]
by (simp add: MPoly_Type.coeff_def one_mpoly.rep_eq lookup_1)


[STATEMENT]
lemma lookup_Const\<^sub>0: "lookup (Const\<^sub>0 c) m = (if m = 0 then c else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup (Const\<^sub>0 c) m = (if m = 0 then c else (0::'a))
[PROOF STEP]
unfolding Const\<^sub>0_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup (Poly_Mapping.single 0 c) m = (if m = 0 then c else (0::'a))
[PROOF STEP]
by (simp add: lookup_single when_def)


[STATEMENT]
lemma mpoly_coeff_Const: "MPoly_Type.coeff (Const c) m = (if m = 0 then c else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MPoly_Type.coeff (Const c) m = (if m = 0 then c else (0::'a))
[PROOF STEP]
by (simp add: MPoly_Type.coeff_def Const.rep_eq lookup_Const\<^sub>0)


[STATEMENT]
lemma coeff_smult [simp]: "coeff (smult c p) m = (c :: 'a :: mult_zero) * coeff p m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MPoly_Type.coeff (MPoly_Type.smult c p) m = c * MPoly_Type.coeff p m
[PROOF STEP]
by transfer (auto simp: map_lookup)


[STATEMENT]
lemma in_keys_mapI: "x \<in> keys m \<Longrightarrow> f (lookup m x) \<noteq> 0 \<Longrightarrow> x \<in> keys (Poly_Mapping.map f m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> keys m; f (lookup m x) \<noteq> (0::'c)\<rbrakk> \<Longrightarrow> x \<in> keys (Poly_Mapping.map f m)
[PROOF STEP]
by transfer auto


[STATEMENT]
lemma vars_uminus [simp]: "vars (-p) = vars p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars (- p) = vars p
[PROOF STEP]
unfolding vars_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (keys ` keys (mapping_of (- p))) = \<Union> (keys ` keys (mapping_of p))
[PROOF STEP]
by transfer' auto


[STATEMENT]
lemma vars_smult: "vars (smult c p) \<subseteq> vars p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars (MPoly_Type.smult c p) \<subseteq> vars p
[PROOF STEP]
unfolding vars_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (keys ` keys (mapping_of (MPoly_Type.smult c p))) \<subseteq> \<Union> (keys ` keys (mapping_of p))
[PROOF STEP]
by (transfer', transfer') auto


[STATEMENT]
lemma vars_sum: "vars (sum f A) \<subseteq> (\<Union>x\<in>A. vars (f x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars (sum f A) \<subseteq> (\<Union>x\<in>A. vars (f x))
[PROOF STEP]
using vars_add
[PROOF STATE]
proof (prove)
using this:
vars (?p1.0 + ?p2.0) \<subseteq> vars ?p1.0 \<union> vars ?p2.0

goal (1 subgoal):
 1. vars (sum f A) \<subseteq> (\<Union>x\<in>A. vars (f x))
[PROOF STEP]
by (induction A rule: infinite_finite_induct) auto


[STATEMENT]
lemma vars_prod: "vars (prod f A) \<subseteq> (\<Union>x\<in>A. vars (f x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars (prod f A) \<subseteq> (\<Union>x\<in>A. vars (f x))
[PROOF STEP]
using vars_mult
[PROOF STATE]
proof (prove)
using this:
vars (?p * ?q) \<subseteq> vars ?p \<union> vars ?q

goal (1 subgoal):
 1. vars (prod f A) \<subseteq> (\<Union>x\<in>A. vars (f x))
[PROOF STEP]
by (induction A rule: infinite_finite_induct) auto


[STATEMENT]
lemma vars_Sum_any: "vars (Sum_any h) \<subseteq> (\<Union>i. vars (h i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars (Sum_any h) \<subseteq> (\<Union>i. vars (h i))
[PROOF STEP]
unfolding Sum_any.expand_set
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars (sum h {a. h a \<noteq> 0}) \<subseteq> (\<Union>i. vars (h i))
[PROOF STEP]
by (intro order.trans[OF vars_sum]) auto


[STATEMENT]
lemma vars_Prod_any: "vars (Prod_any h) \<subseteq> (\<Union>i. vars (h i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars (Prod_any h) \<subseteq> (\<Union>i. vars (h i))
[PROOF STEP]
unfolding Prod_any.expand_set
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars (prod h {a. h a \<noteq> 1}) \<subseteq> (\<Union>i. vars (h i))
[PROOF STEP]
by (intro order.trans[OF vars_prod]) auto


[STATEMENT]
lemma vars_power: "vars (p ^ n) \<subseteq> vars p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars (p ^ n) \<subseteq> vars p
[PROOF STEP]
using vars_mult
[PROOF STATE]
proof (prove)
using this:
vars (?p * ?q) \<subseteq> vars ?p \<union> vars ?q

goal (1 subgoal):
 1. vars (p ^ n) \<subseteq> vars p
[PROOF STEP]
by (induction n) auto


[STATEMENT]
lemma vars_diff: "vars (p1 - p2) \<subseteq> vars p1 \<union> vars p2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars (p1 - p2) \<subseteq> vars p1 \<union> vars p2
[PROOF STEP]
unfolding vars_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (keys ` keys (mapping_of (p1 - p2))) \<subseteq> \<Union> (keys ` keys (mapping_of p1)) \<union> \<Union> (keys ` keys (mapping_of p2))
[PROOF STEP]
proof transfer'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p1 p2. \<Union> (keys ` keys (p1 - p2)) \<subseteq> \<Union> (keys ` keys p1) \<union> \<Union> (keys ` keys p2)
[PROOF STEP]
fix p1 p2 :: "(nat \<Rightarrow>\<^sub>0 nat) \<Rightarrow>\<^sub>0 'a"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p1 p2. \<Union> (keys ` keys (p1 - p2)) \<subseteq> \<Union> (keys ` keys p1) \<union> \<Union> (keys ` keys p2)
[PROOF STEP]
show "\<Union> (keys ` keys (p1 - p2)) \<subseteq> \<Union>(keys ` (keys p1)) \<union> \<Union>(keys ` (keys p2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (keys ` keys (p1 - p2)) \<subseteq> \<Union> (keys ` keys p1) \<union> \<Union> (keys ` keys p2)
[PROOF STEP]
using keys_diff_subset[of p1 p2]
[PROOF STATE]
proof (prove)
using this:
keys (p1 - p2) \<subseteq> keys p1 \<union> keys p2

goal (1 subgoal):
 1. \<Union> (keys ` keys (p1 - p2)) \<subseteq> \<Union> (keys ` keys p1) \<union> \<Union> (keys ` keys p2)
[PROOF STEP]
by (auto simp flip: not_in_keys_iff_lookup_eq_zero)
[PROOF STATE]
proof (state)
this:
\<Union> (keys ` keys (p1 - p2)) \<subseteq> \<Union> (keys ` keys p1) \<union> \<Union> (keys ` keys p2)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma insertion_smult [simp]: "insertion f (smult c p) = c * insertion f p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion f (MPoly_Type.smult c p) = c * insertion f p
[PROOF STEP]
unfolding insertion_altdef
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>m. MPoly_Type.coeff (MPoly_Type.smult c p) m * (\<Prod>i. f i ^ lookup m i)) = c * (\<Sum>m. MPoly_Type.coeff p m * (\<Prod>i. f i ^ lookup m i))
[PROOF STEP]
by (subst Sum_any_right_distrib)
     (auto intro: finite_subset[OF _ finite_coeff_support[of p]] simp: mult.assoc)


[STATEMENT]
lemma coeff_add [simp]: "coeff (p + q) m = coeff p m + coeff q m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MPoly_Type.coeff (p + q) m = MPoly_Type.coeff p m + MPoly_Type.coeff q m
[PROOF STEP]
by transfer' (simp add: lookup_add)


[STATEMENT]
lemma coeff_diff [simp]: "coeff (p - q) m = coeff p m - coeff q m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MPoly_Type.coeff (p - q) m = MPoly_Type.coeff p m - MPoly_Type.coeff q m
[PROOF STEP]
by transfer' (simp add: lookup_minus)


[STATEMENT]
lemma insertion_monom [simp]:
  "insertion f (monom m c) = c * Prod_any (\<lambda>x. f x ^ lookup m x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion f (MPoly_Type.monom m c) = c * (\<Prod>x. f x ^ lookup m x)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. insertion f (MPoly_Type.monom m c) = c * (\<Prod>x. f x ^ lookup m x)
[PROOF STEP]
have "insertion f (monom m c) =
          (\<Sum>m'. (c when m = m') * (\<Prod>v. f v ^ lookup m' v))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion f (MPoly_Type.monom m c) = (\<Sum>m'. (c when m = m') * (\<Prod>v. f v ^ lookup m' v))
[PROOF STEP]
by (simp add: insertion_def insertion_aux_def insertion_fun_def lookup_single)
[PROOF STATE]
proof (state)
this:
insertion f (MPoly_Type.monom m c) = (\<Sum>m'. (c when m = m') * (\<Prod>v. f v ^ lookup m' v))

goal (1 subgoal):
 1. insertion f (MPoly_Type.monom m c) = c * (\<Prod>x. f x ^ lookup m x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
insertion f (MPoly_Type.monom m c) = (\<Sum>m'. (c when m = m') * (\<Prod>v. f v ^ lookup m' v))

goal (1 subgoal):
 1. insertion f (MPoly_Type.monom m c) = c * (\<Prod>x. f x ^ lookup m x)
[PROOF STEP]
have "\<dots> = c * (\<Prod>v. f v ^ lookup m v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>m'. (c when m = m') * (\<Prod>v. f v ^ lookup m' v)) = c * (\<Prod>v. f v ^ lookup m v)
[PROOF STEP]
by (subst Sum_any.expand_superset[of "{m}"]) (auto simp: when_def)
[PROOF STATE]
proof (state)
this:
(\<Sum>m'. (c when m = m') * (\<Prod>v. f v ^ lookup m' v)) = c * (\<Prod>v. f v ^ lookup m v)

goal (1 subgoal):
 1. insertion f (MPoly_Type.monom m c) = c * (\<Prod>x. f x ^ lookup m x)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
insertion f (MPoly_Type.monom m c) = c * (\<Prod>v. f v ^ lookup m v)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
insertion f (MPoly_Type.monom m c) = c * (\<Prod>v. f v ^ lookup m v)

goal (1 subgoal):
 1. insertion f (MPoly_Type.monom m c) = c * (\<Prod>x. f x ^ lookup m x)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
insertion f (MPoly_Type.monom m c) = c * (\<Prod>x. f x ^ lookup m x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma insertion_aux_Const\<^sub>0 [simp]: "insertion_aux f (Const\<^sub>0 c) = c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion_aux f (Const\<^sub>0 c) = c
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. insertion_aux f (Const\<^sub>0 c) = c
[PROOF STEP]
have "insertion_aux f (Const\<^sub>0 c) = (\<Sum>m. (c when m = 0) * (\<Prod>v. f v ^ lookup m v))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion_aux f (Const\<^sub>0 c) = (\<Sum>m. (c when m = 0) * (\<Prod>v. f v ^ lookup m v))
[PROOF STEP]
by (simp add: Const\<^sub>0_def insertion_aux_def insertion_fun_def lookup_single)
[PROOF STATE]
proof (state)
this:
insertion_aux f (Const\<^sub>0 c) = (\<Sum>m. (c when m = 0) * (\<Prod>v. f v ^ lookup m v))

goal (1 subgoal):
 1. insertion_aux f (Const\<^sub>0 c) = c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
insertion_aux f (Const\<^sub>0 c) = (\<Sum>m. (c when m = 0) * (\<Prod>v. f v ^ lookup m v))

goal (1 subgoal):
 1. insertion_aux f (Const\<^sub>0 c) = c
[PROOF STEP]
have "\<dots> = (\<Sum>m\<in>{0}. (c when m = 0) * (\<Prod>v. f v ^ lookup m v))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>m. (c when m = 0) * (\<Prod>v. f v ^ lookup m v)) = (\<Sum>m\<in>{0}. (c when m = 0) * (\<Prod>v. f v ^ lookup m v))
[PROOF STEP]
by (intro Sum_any.expand_superset) (auto simp: when_def)
[PROOF STATE]
proof (state)
this:
(\<Sum>m. (c when m = 0) * (\<Prod>v. f v ^ lookup m v)) = (\<Sum>m\<in>{0}. (c when m = 0) * (\<Prod>v. f v ^ lookup m v))

goal (1 subgoal):
 1. insertion_aux f (Const\<^sub>0 c) = c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>m. (c when m = 0) * (\<Prod>v. f v ^ lookup m v)) = (\<Sum>m\<in>{0}. (c when m = 0) * (\<Prod>v. f v ^ lookup m v))

goal (1 subgoal):
 1. insertion_aux f (Const\<^sub>0 c) = c
[PROOF STEP]
have "\<dots> = c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>m\<in>{0}. (c when m = 0) * (\<Prod>v. f v ^ lookup m v)) = c
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>m\<in>{0}. (c when m = 0) * (\<Prod>v. f v ^ lookup m v)) = c

goal (1 subgoal):
 1. insertion_aux f (Const\<^sub>0 c) = c
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
insertion_aux f (Const\<^sub>0 c) = c
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
insertion_aux f (Const\<^sub>0 c) = c

goal (1 subgoal):
 1. insertion_aux f (Const\<^sub>0 c) = c
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
insertion_aux f (Const\<^sub>0 c) = c

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma insertion_Const [simp]: "insertion f (Const c) = c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion f (Const c) = c
[PROOF STEP]
by (simp add: insertion_def Const.rep_eq)


[STATEMENT]
lemma coeffs_0 [simp]: "coeffs 0 = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MPoly_Type.coeffs 0 = {}
[PROOF STEP]
by transfer auto


[STATEMENT]
lemma coeffs_1 [simp]: "coeffs 1 = {1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MPoly_Type.coeffs 1 = {1::'a}
[PROOF STEP]
by transfer auto


[STATEMENT]
lemma coeffs_Const: "coeffs (Const c) = (if c = 0 then {} else {c})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MPoly_Type.coeffs (Const c) = (if c = (0::'a) then {} else {c})
[PROOF STEP]
unfolding Const_def Const\<^sub>0_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MPoly_Type.coeffs (map_fun id MPoly (Poly_Mapping.single 0) c) = (if c = (0::'a) then {} else {c})
[PROOF STEP]
by transfer' auto


[STATEMENT]
lemma coeffs_subset: "coeffs (Const c) \<subseteq> {c}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MPoly_Type.coeffs (Const c) \<subseteq> {c}
[PROOF STEP]
by (auto simp: coeffs_Const)


[STATEMENT]
lemma keys_Const\<^sub>0: "keys (Const\<^sub>0 c) = (if c = 0 then {} else {0})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. keys (Const\<^sub>0 c) = (if c = (0::'b) then {} else {0})
[PROOF STEP]
unfolding Const\<^sub>0_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. keys (Poly_Mapping.single 0 c) = (if c = (0::'b) then {} else {0})
[PROOF STEP]
by transfer' auto


[STATEMENT]
lemma prod_fun_compose_bij:
  assumes "bij f" and f: "\<And>x y. f (x + y) = f x + f y"
  shows   "prod_fun m1 m2 (f x) = prod_fun (m1 \<circ> f) (m2 \<circ> f) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prod_fun m1 m2 (f x) = prod_fun (m1 \<circ> f) (m2 \<circ> f) x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prod_fun m1 m2 (f x) = prod_fun (m1 \<circ> f) (m2 \<circ> f) x
[PROOF STEP]
have [simp]: "f x = f y \<longleftrightarrow> x = y" for x y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f x = f y) = (x = y)
[PROOF STEP]
using \<open>bij f\<close>
[PROOF STATE]
proof (prove)
using this:
bij f

goal (1 subgoal):
 1. (f x = f y) = (x = y)
[PROOF STEP]
by (auto dest!: bij_is_inj inj_onD)
[PROOF STATE]
proof (state)
this:
(f ?x = f ?y) = (?x = ?y)

goal (1 subgoal):
 1. prod_fun m1 m2 (f x) = prod_fun (m1 \<circ> f) (m2 \<circ> f) x
[PROOF STEP]
have "prod_fun (m1 \<circ> f) (m2 \<circ> f) x =
          Sum_any ((\<lambda>l. m1 l * Sum_any ((\<lambda>q. m2 q when f x = l + q) \<circ> f)) \<circ> f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prod_fun (m1 \<circ> f) (m2 \<circ> f) x = Sum_any ((\<lambda>l. m1 l * Sum_any ((\<lambda>q. m2 q when f x = l + q) \<circ> f)) \<circ> f)
[PROOF STEP]
by (simp add: prod_fun_def f(1) [symmetric] o_def)
[PROOF STATE]
proof (state)
this:
prod_fun (m1 \<circ> f) (m2 \<circ> f) x = Sum_any ((\<lambda>l. m1 l * Sum_any ((\<lambda>q. m2 q when f x = l + q) \<circ> f)) \<circ> f)

goal (1 subgoal):
 1. prod_fun m1 m2 (f x) = prod_fun (m1 \<circ> f) (m2 \<circ> f) x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
prod_fun (m1 \<circ> f) (m2 \<circ> f) x = Sum_any ((\<lambda>l. m1 l * Sum_any ((\<lambda>q. m2 q when f x = l + q) \<circ> f)) \<circ> f)

goal (1 subgoal):
 1. prod_fun m1 m2 (f x) = prod_fun (m1 \<circ> f) (m2 \<circ> f) x
[PROOF STEP]
have "\<dots> = Sum_any ((\<lambda>l. m1 l * Sum_any ((\<lambda>q. m2 q when f x = l + q))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sum_any ((\<lambda>l. m1 l * Sum_any ((\<lambda>q. m2 q when f x = l + q) \<circ> f)) \<circ> f) = (\<Sum>l. m1 l * (\<Sum>q. m2 q when f x = l + q))
[PROOF STEP]
by (simp only: Sum_any.reindex_cong[OF assms(1) refl, symmetric])
[PROOF STATE]
proof (state)
this:
Sum_any ((\<lambda>l. m1 l * Sum_any ((\<lambda>q. m2 q when f x = l + q) \<circ> f)) \<circ> f) = (\<Sum>l. m1 l * (\<Sum>q. m2 q when f x = l + q))

goal (1 subgoal):
 1. prod_fun m1 m2 (f x) = prod_fun (m1 \<circ> f) (m2 \<circ> f) x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Sum_any ((\<lambda>l. m1 l * Sum_any ((\<lambda>q. m2 q when f x = l + q) \<circ> f)) \<circ> f) = (\<Sum>l. m1 l * (\<Sum>q. m2 q when f x = l + q))

goal (1 subgoal):
 1. prod_fun m1 m2 (f x) = prod_fun (m1 \<circ> f) (m2 \<circ> f) x
[PROOF STEP]
have "\<dots> = prod_fun m1 m2 (f x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>l. m1 l * (\<Sum>q. m2 q when f x = l + q)) = prod_fun m1 m2 (f x)
[PROOF STEP]
by (simp add: prod_fun_def)
[PROOF STATE]
proof (state)
this:
(\<Sum>l. m1 l * (\<Sum>q. m2 q when f x = l + q)) = prod_fun m1 m2 (f x)

goal (1 subgoal):
 1. prod_fun m1 m2 (f x) = prod_fun (m1 \<circ> f) (m2 \<circ> f) x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
prod_fun (m1 \<circ> f) (m2 \<circ> f) x = prod_fun m1 m2 (f x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
prod_fun (m1 \<circ> f) (m2 \<circ> f) x = prod_fun m1 m2 (f x)

goal (1 subgoal):
 1. prod_fun m1 m2 (f x) = prod_fun (m1 \<circ> f) (m2 \<circ> f) x
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
prod_fun m1 m2 (f x) = prod_fun (m1 \<circ> f) (m2 \<circ> f) x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma add_nat_poly_mapping_zero_iff [simp]:
  "(a + b :: 'a \<Rightarrow>\<^sub>0 nat) = 0 \<longleftrightarrow> a = 0 \<and> b = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a + b = 0) = (a = 0 \<and> b = 0)
[PROOF STEP]
by transfer (auto simp: fun_eq_iff)


[STATEMENT]
lemma prod_fun_nat_0:
  fixes f g :: "('a \<Rightarrow>\<^sub>0 nat) \<Rightarrow> 'b::semiring_0"
  shows   "prod_fun f g 0 = f 0 * g 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prod_fun f g 0 = f 0 * g 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prod_fun f g 0 = f 0 * g 0
[PROOF STEP]
have "prod_fun f g 0 = (\<Sum>l. f l * (\<Sum>q. g q when 0 = l + q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prod_fun f g 0 = (\<Sum>l. f l * (\<Sum>q. g q when 0 = l + q))
[PROOF STEP]
unfolding prod_fun_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>l. f l * (\<Sum>q. g q when 0 = l + q)) = (\<Sum>l. f l * (\<Sum>q. g q when 0 = l + q))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
prod_fun f g 0 = (\<Sum>l. f l * (\<Sum>q. g q when 0 = l + q))

goal (1 subgoal):
 1. prod_fun f g 0 = f 0 * g 0
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
prod_fun f g 0 = (\<Sum>l. f l * (\<Sum>q. g q when 0 = l + q))

goal (1 subgoal):
 1. prod_fun f g 0 = f 0 * g 0
[PROOF STEP]
have "(\<lambda>l. \<Sum>q. g q when 0 = l + q) = (\<lambda>l. \<Sum>q\<in>{0}. g q when 0 = l + q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>l. \<Sum>q. g q when 0 = l + q) = (\<lambda>l. \<Sum>q\<in>{0}. g q when 0 = l + q)
[PROOF STEP]
by (intro ext Sum_any.expand_superset) (auto simp: when_def)
[PROOF STATE]
proof (state)
this:
(\<lambda>l. \<Sum>q. g q when 0 = l + q) = (\<lambda>l. \<Sum>q\<in>{0}. g q when 0 = l + q)

goal (1 subgoal):
 1. prod_fun f g 0 = f 0 * g 0
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<lambda>l. \<Sum>q. g q when 0 = l + q) = (\<lambda>l. \<Sum>q\<in>{0}. g q when 0 = l + q)

goal (1 subgoal):
 1. prod_fun f g 0 = f 0 * g 0
[PROOF STEP]
have "(\<Sum>l. f l * \<dots> l) = (\<Sum>l\<in>{0}. f l * \<dots> l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>l. f l * (\<Sum>q\<in>{0}. g q when 0 = l + q)) = (\<Sum>l\<in>{0}. f l * (\<Sum>q\<in>{0}. g q when 0 = l + q))
[PROOF STEP]
by (intro ext Sum_any.expand_superset) (auto simp: when_def)
[PROOF STATE]
proof (state)
this:
(\<Sum>l. f l * (\<Sum>q\<in>{0}. g q when 0 = l + q)) = (\<Sum>l\<in>{0}. f l * (\<Sum>q\<in>{0}. g q when 0 = l + q))

goal (1 subgoal):
 1. prod_fun f g 0 = f 0 * g 0
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
prod_fun f g 0 = (\<Sum>l\<in>{0}. f l * (\<Sum>q\<in>{0}. g q when 0 = l + q))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
prod_fun f g 0 = (\<Sum>l\<in>{0}. f l * (\<Sum>q\<in>{0}. g q when 0 = l + q))

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mpoly_coeff_prod_0: "coeff (\<Prod>x\<in>A. f x) 0 = (\<Prod>x\<in>A. coeff (f x) 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MPoly_Type.coeff (prod f A) 0 = (\<Prod>x\<in>A. MPoly_Type.coeff (f x) 0)
[PROOF STEP]
by (induction A rule: infinite_finite_induct) (auto simp: mpoly_coeff_times_0 mpoly_coeff_1)


[STATEMENT]
lemma mpoly_coeff_power_0: "coeff (p ^ n) 0 = coeff p 0 ^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MPoly_Type.coeff (p ^ n) 0 = MPoly_Type.coeff p 0 ^ n
[PROOF STEP]
by (induction n) (auto simp: mpoly_coeff_times_0 mpoly_coeff_1)


[STATEMENT]
lemma prod_fun_gt_max_eq_zero:
  fixes f g :: "'a::{linorder, ordered_cancel_comm_monoid_add} \<Rightarrow> 'b::semiring_0"
  assumes "m > a + b"
  assumes zero: "\<And>m. m > a \<Longrightarrow> f m = 0" "\<And>m. m > b \<Longrightarrow> g m = 0"
  assumes fin: "finite {m. f m \<noteq> 0}" "finite {m. g m \<noteq> 0}"
  shows   "prod_fun f g m = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prod_fun f g m = (0::'b)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prod_fun f g m = (0::'b)
[PROOF STEP]
note fin' = finite_subset[OF _ fin(1)] finite_subset[OF _ fin(2)]
[PROOF STATE]
proof (state)
this:
?A \<subseteq> {m. f m \<noteq> (0::'b)} \<Longrightarrow> finite ?A
?A \<subseteq> {m. g m \<noteq> (0::'b)} \<Longrightarrow> finite ?A

goal (1 subgoal):
 1. prod_fun f g m = (0::'b)
[PROOF STEP]
have "prod_fun f g m = (\<Sum>l. f l * (\<Sum>q. g q when m = l + q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prod_fun f g m = (\<Sum>l. f l * (\<Sum>q. g q when m = l + q))
[PROOF STEP]
by (simp add: prod_fun_def Sum_any_right_distrib)
[PROOF STATE]
proof (state)
this:
prod_fun f g m = (\<Sum>l. f l * (\<Sum>q. g q when m = l + q))

goal (1 subgoal):
 1. prod_fun f g m = (0::'b)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
prod_fun f g m = (\<Sum>l. f l * (\<Sum>q. g q when m = l + q))

goal (1 subgoal):
 1. prod_fun f g m = (0::'b)
[PROOF STEP]
have "\<dots> = (\<Sum>l. \<Sum>q. f l * g q when m = l + q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>l. f l * (\<Sum>q. g q when m = l + q)) = (\<Sum>l. \<Sum>q. f l * g q when m = l + q)
[PROOF STEP]
by (subst Sum_any_right_distrib) (auto intro!: Sum_any.cong fin'(2) simp: when_def)
[PROOF STATE]
proof (state)
this:
(\<Sum>l. f l * (\<Sum>q. g q when m = l + q)) = (\<Sum>l. \<Sum>q. f l * g q when m = l + q)

goal (1 subgoal):
 1. prod_fun f g m = (0::'b)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>l. f l * (\<Sum>q. g q when m = l + q)) = (\<Sum>l. \<Sum>q. f l * g q when m = l + q)

goal (1 subgoal):
 1. prod_fun f g m = (0::'b)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
(\<Sum>l. f l * (\<Sum>q. g q when m = l + q)) = (\<Sum>l. \<Sum>q. f l * g q when m = l + q)

goal (1 subgoal):
 1. prod_fun f g m = (0::'b)
[PROOF STEP]
fix l q
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prod_fun f g m = (0::'b)
[PROOF STEP]
assume lq: "m = l + q" and nz: "f l * g q \<noteq> 0"
[PROOF STATE]
proof (state)
this:
m = l + q
f l * g q \<noteq> (0::'b)

goal (1 subgoal):
 1. prod_fun f g m = (0::'b)
[PROOF STEP]
from nz and zero
[PROOF STATE]
proof (chain)
picking this:
f l * g q \<noteq> (0::'b)
a < ?m \<Longrightarrow> f ?m = (0::'b)
b < ?m \<Longrightarrow> g ?m = (0::'b)
[PROOF STEP]
have "l \<le> a" "q \<le> b"
[PROOF STATE]
proof (prove)
using this:
f l * g q \<noteq> (0::'b)
a < ?m \<Longrightarrow> f ?m = (0::'b)
b < ?m \<Longrightarrow> g ?m = (0::'b)

goal (1 subgoal):
 1. l \<le> a &&& q \<le> b
[PROOF STEP]
by (auto intro: leI)
[PROOF STATE]
proof (state)
this:
l \<le> a
q \<le> b

goal (1 subgoal):
 1. prod_fun f g m = (0::'b)
[PROOF STEP]
hence "l + q \<le> a + b"
[PROOF STATE]
proof (prove)
using this:
l \<le> a
q \<le> b

goal (1 subgoal):
 1. l + q \<le> a + b
[PROOF STEP]
by (intro add_mono)
[PROOF STATE]
proof (state)
this:
l + q \<le> a + b

goal (1 subgoal):
 1. prod_fun f g m = (0::'b)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
l + q \<le> a + b

goal (1 subgoal):
 1. prod_fun f g m = (0::'b)
[PROOF STEP]
have "\<dots> < m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a + b < m
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
a + b < m

goal (1 subgoal):
 1. prod_fun f g m = (0::'b)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
l + q < m
[PROOF STEP]
have "l + q < m"
[PROOF STATE]
proof (prove)
using this:
l + q < m

goal (1 subgoal):
 1. l + q < m
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
l + q < m

goal (1 subgoal):
 1. prod_fun f g m = (0::'b)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>m = ?l2 + ?q2; f ?l2 * g ?q2 \<noteq> (0::'b)\<rbrakk> \<Longrightarrow> ?l2 + ?q2 < m

goal (1 subgoal):
 1. prod_fun f g m = (0::'b)
[PROOF STEP]
hence "(\<Sum>l. \<Sum>q. f l * g q when m = l + q) = (\<Sum>l. \<Sum>q. f l * g q when False)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>m = ?l2 + ?q2; f ?l2 * g ?q2 \<noteq> (0::'b)\<rbrakk> \<Longrightarrow> ?l2 + ?q2 < m

goal (1 subgoal):
 1. (\<Sum>l. \<Sum>q. f l * g q when m = l + q) = (\<Sum>l. \<Sum>q. f l * g q when False)
[PROOF STEP]
by (intro Sum_any.cong refl) (auto simp: when_def)
[PROOF STATE]
proof (state)
this:
(\<Sum>l. \<Sum>q. f l * g q when m = l + q) = (\<Sum>l. \<Sum>q. f l * g q when False)

goal (1 subgoal):
 1. prod_fun f g m = (0::'b)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>l. \<Sum>q. f l * g q when m = l + q) = (\<Sum>l. \<Sum>q. f l * g q when False)

goal (1 subgoal):
 1. prod_fun f g m = (0::'b)
[PROOF STEP]
have "\<dots> = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>l. \<Sum>q. f l * g q when False) = (0::'b)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>l. \<Sum>q. f l * g q when False) = (0::'b)

goal (1 subgoal):
 1. prod_fun f g m = (0::'b)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
prod_fun f g m = (0::'b)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
prod_fun f g m = (0::'b)

goal (1 subgoal):
 1. prod_fun f g m = (0::'b)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
prod_fun f g m = (0::'b)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lookup_restrictpm: "lookup (restrictpm A m) x = (if x \<in> A then lookup m x else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup (restrictpm A m) x = (if x \<in> A then lookup m x else (0::'a))
[PROOF STEP]
by transfer auto


[STATEMENT]
lemma lookup_restrictpm_in [simp]: "x \<in> A \<Longrightarrow> lookup (restrictpm A m) x = lookup m x"
  and lookup_restrict_pm_not_in [simp]: "x \<notin> A \<Longrightarrow> lookup (restrictpm A m) x = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<in> A \<Longrightarrow> lookup (restrictpm A m) x = lookup m x) &&& (x \<notin> A \<Longrightarrow> lookup (restrictpm A m) x = (0::'b))
[PROOF STEP]
by (simp_all add: lookup_restrictpm)


[STATEMENT]
lemma keys_restrictpm [simp]: "keys (restrictpm A m) = keys m \<inter> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. keys (restrictpm A m) = keys m \<inter> A
[PROOF STEP]
by transfer auto


[STATEMENT]
lemma restrictpm_add: "restrictpm X (m1 + m2) = restrictpm X m1 + restrictpm X m2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. restrictpm X (m1 + m2) = restrictpm X m1 + restrictpm X m2
[PROOF STEP]
by transfer auto


[STATEMENT]
lemma restrictpm_id [simp]: "keys m \<subseteq> X \<Longrightarrow> restrictpm X m = m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. keys m \<subseteq> X \<Longrightarrow> restrictpm X m = m
[PROOF STEP]
by transfer (auto simp: fun_eq_iff)


[STATEMENT]
lemma restrictpm_orthogonal [simp]: "keys m \<subseteq> -X \<Longrightarrow> restrictpm X m = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. keys m \<subseteq> - X \<Longrightarrow> restrictpm X m = 0
[PROOF STEP]
by transfer (auto simp: fun_eq_iff)


[STATEMENT]
lemma restrictpm_add_disjoint:
  "X \<inter> Y = {} \<Longrightarrow> restrictpm X m + restrictpm Y m = restrictpm (X \<union> Y) m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X \<inter> Y = {} \<Longrightarrow> restrictpm X m + restrictpm Y m = restrictpm (X \<union> Y) m
[PROOF STEP]
by transfer (auto simp: fun_eq_iff)


[STATEMENT]
lemma restrictpm_add_complements:
  "restrictpm X m + restrictpm (-X) m = m" "restrictpm (-X) m + restrictpm X m = m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. restrictpm X m + restrictpm (- X) m = m &&& restrictpm (- X) m + restrictpm X m = m
[PROOF STEP]
by (subst restrictpm_add_disjoint; force)+


[STATEMENT]
lemma map_mpoly_conv_mapm_mpoly: "map_mpoly f = mapm_mpoly (\<lambda>_. f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_mpoly f = mapm_mpoly (\<lambda>_. f)
[PROOF STEP]
by transfer' (auto simp: poly_mapping_map_conv_mapp)


[STATEMENT]
lemma map_mpoly_comp: "f 0 = 0 \<Longrightarrow> map_mpoly f (map_mpoly g p) = map_mpoly (f \<circ> g) p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (0::'b) = (0::'a) \<Longrightarrow> map_mpoly f (map_mpoly g p) = map_mpoly (f \<circ> g) p
[PROOF STEP]
by (transfer', transfer') (auto simp: when_def fun_eq_iff)


[STATEMENT]
lemma mapp_mapp:
  "(\<And>x. f x 0 = 0) \<Longrightarrow> Poly_Mapping.mapp f (Poly_Mapping.mapp g m) =
                          Poly_Mapping.mapp (\<lambda>x y. f x (g x y)) m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. f x (0::'c) = (0::'b)) \<Longrightarrow> Poly_Mapping.mapp f (Poly_Mapping.mapp g m) = Poly_Mapping.mapp (\<lambda>x y. f x (g x y)) m
[PROOF STEP]
by transfer' (auto simp: fun_eq_iff lookup_mapp in_keys_iff)


[STATEMENT]
lemma mapm_mpoly_comp:
  "(\<And>x. f x 0 = 0) \<Longrightarrow> mapm_mpoly f (mapm_mpoly g p) = mapm_mpoly (\<lambda>m c. f m (g m c)) p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. f x (0::'b) = (0::'a)) \<Longrightarrow> mapm_mpoly f (mapm_mpoly g p) = mapm_mpoly (\<lambda>m c. f m (g m c)) p
[PROOF STEP]
by transfer' (simp add: mapp_mapp)


[STATEMENT]
lemma coeff_map_mpoly:
  "coeff (map_mpoly f p) m = (if coeff p m = 0 then 0 else f (coeff p m))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MPoly_Type.coeff (map_mpoly f p) m = (if MPoly_Type.coeff p m = (0::'b) then 0::'a else f (MPoly_Type.coeff p m))
[PROOF STEP]
by (transfer, transfer) auto


[STATEMENT]
lemma coeff_map_mpoly' [simp]: "f 0 = 0 \<Longrightarrow> coeff (map_mpoly f p) m = f (coeff p m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (0::'b) = (0::'a) \<Longrightarrow> MPoly_Type.coeff (map_mpoly f p) m = f (MPoly_Type.coeff p m)
[PROOF STEP]
by (subst coeff_map_mpoly) auto


[STATEMENT]
lemma coeff_mapm_mpoly' [simp]: "(\<And>m. f m 0 = 0) \<Longrightarrow> coeff (mapm_mpoly f p) m = f m (coeff p m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>m. f m (0::'b) = (0::'a)) \<Longrightarrow> MPoly_Type.coeff (mapm_mpoly f p) m = f m (MPoly_Type.coeff p m)
[PROOF STEP]
by (subst coeff_mapm_mpoly) auto


[STATEMENT]
lemma vars_map_mpoly_subset: "vars (map_mpoly f p) \<subseteq> vars p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars (map_mpoly f p) \<subseteq> vars p
[PROOF STEP]
unfolding vars_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (keys ` keys (mapping_of (map_mpoly f p))) \<subseteq> \<Union> (keys ` keys (mapping_of p))
[PROOF STEP]
by (transfer', transfer') (auto simp: map_mpoly.rep_eq)


[STATEMENT]
lemma coeff_sum [simp]: "coeff (sum f A) m = (\<Sum>x\<in>A. coeff (f x) m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MPoly_Type.coeff (sum f A) m = (\<Sum>x\<in>A. MPoly_Type.coeff (f x) m)
[PROOF STEP]
by (induction A rule: infinite_finite_induct) auto


[STATEMENT]
lemma coeff_Sum_any: "finite {x. f x \<noteq> 0} \<Longrightarrow> coeff (Sum_any f) m = Sum_any (\<lambda>x. coeff (f x) m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {x. f x \<noteq> 0} \<Longrightarrow> MPoly_Type.coeff (Sum_any f) m = (\<Sum>x. MPoly_Type.coeff (f x) m)
[PROOF STEP]
by (auto simp add: Sum_any.expand_set intro!: sum.mono_neutral_right)


[STATEMENT]
lemma Sum_any_zeroI: "(\<And>x. f x = 0) \<Longrightarrow> Sum_any f = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. f x = (0::'b)) \<Longrightarrow> Sum_any f = (0::'b)
[PROOF STEP]
by (auto simp: Sum_any.expand_set)


[STATEMENT]
lemma insertion_Prod_any:
  "finite {x. g x \<noteq> 1} \<Longrightarrow> insertion f (Prod_any g) = Prod_any (\<lambda>x. insertion f (g x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {x. g x \<noteq> 1} \<Longrightarrow> insertion f (Prod_any g) = (\<Prod>x. insertion f (g x))
[PROOF STEP]
by (auto simp: Prod_any.expand_set insertion_prod intro!: prod.mono_neutral_right)


[STATEMENT]
lemma insertion_insertion:
  "insertion g (insertion k p) =
     insertion (\<lambda>x. insertion g (k x)) (map_mpoly (insertion g) p)" (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion g (insertion k p) = insertion (\<lambda>x. insertion g (k x)) (map_mpoly (insertion g) p)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. insertion g (insertion k p) = insertion (\<lambda>x. insertion g (k x)) (map_mpoly (insertion g) p)
[PROOF STEP]
have "insertion g (insertion k p) =
          (\<Sum>x. insertion g (coeff p x) * insertion g (\<Prod>i. k i ^ lookup x i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion g (insertion k p) = (\<Sum>x. insertion g (MPoly_Type.coeff p x) * insertion g (\<Prod>i. k i ^ lookup x i))
[PROOF STEP]
unfolding insertion_altdef[of k p]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion g (\<Sum>m. MPoly_Type.coeff p m * (\<Prod>i. k i ^ lookup m i)) = (\<Sum>x. insertion g (MPoly_Type.coeff p x) * insertion g (\<Prod>i. k i ^ lookup x i))
[PROOF STEP]
by (subst insertion_Sum_any)
       (auto intro: finite_subset[OF _ finite_coeff_support[of p]] simp: insertion_mult)
[PROOF STATE]
proof (state)
this:
insertion g (insertion k p) = (\<Sum>x. insertion g (MPoly_Type.coeff p x) * insertion g (\<Prod>i. k i ^ lookup x i))

goal (1 subgoal):
 1. insertion g (insertion k p) = insertion (\<lambda>x. insertion g (k x)) (map_mpoly (insertion g) p)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
insertion g (insertion k p) = (\<Sum>x. insertion g (MPoly_Type.coeff p x) * insertion g (\<Prod>i. k i ^ lookup x i))

goal (1 subgoal):
 1. insertion g (insertion k p) = insertion (\<lambda>x. insertion g (k x)) (map_mpoly (insertion g) p)
[PROOF STEP]
have "\<dots> = (\<Sum>x. insertion g (coeff p x) * (\<Prod>i. insertion g (k i) ^ lookup x i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x. insertion g (MPoly_Type.coeff p x) * insertion g (\<Prod>i. k i ^ lookup x i)) = (\<Sum>x. insertion g (MPoly_Type.coeff p x) * (\<Prod>i. insertion g (k i) ^ lookup x i))
[PROOF STEP]
proof (intro Sum_any.cong)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. insertion g (MPoly_Type.coeff p a) * insertion g (\<Prod>i. k i ^ lookup a i) = insertion g (MPoly_Type.coeff p a) * (\<Prod>i. insertion g (k i) ^ lookup a i)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. insertion g (MPoly_Type.coeff p a) * insertion g (\<Prod>i. k i ^ lookup a i) = insertion g (MPoly_Type.coeff p a) * (\<Prod>i. insertion g (k i) ^ lookup a i)
[PROOF STEP]
show "insertion g (coeff p x) * insertion g (\<Prod>i. k i ^ lookup x i) =
                  insertion g (coeff p x) * (\<Prod>i. insertion g (k i) ^ lookup x i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion g (MPoly_Type.coeff p x) * insertion g (\<Prod>i. k i ^ lookup x i) = insertion g (MPoly_Type.coeff p x) * (\<Prod>i. insertion g (k i) ^ lookup x i)
[PROOF STEP]
by (subst insertion_Prod_any)
         (auto simp: insertion_power intro!: finite_subset[OF _ finite_lookup[of x]] Nat.gr0I)
[PROOF STATE]
proof (state)
this:
insertion g (MPoly_Type.coeff p x) * insertion g (\<Prod>i. k i ^ lookup x i) = insertion g (MPoly_Type.coeff p x) * (\<Prod>i. insertion g (k i) ^ lookup x i)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>x. insertion g (MPoly_Type.coeff p x) * insertion g (\<Prod>i. k i ^ lookup x i)) = (\<Sum>x. insertion g (MPoly_Type.coeff p x) * (\<Prod>i. insertion g (k i) ^ lookup x i))

goal (1 subgoal):
 1. insertion g (insertion k p) = insertion (\<lambda>x. insertion g (k x)) (map_mpoly (insertion g) p)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>x. insertion g (MPoly_Type.coeff p x) * insertion g (\<Prod>i. k i ^ lookup x i)) = (\<Sum>x. insertion g (MPoly_Type.coeff p x) * (\<Prod>i. insertion g (k i) ^ lookup x i))

goal (1 subgoal):
 1. insertion g (insertion k p) = insertion (\<lambda>x. insertion g (k x)) (map_mpoly (insertion g) p)
[PROOF STEP]
have "\<dots> = insertion (\<lambda>x. insertion g (k x)) (map_mpoly (insertion g) p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x. insertion g (MPoly_Type.coeff p x) * (\<Prod>i. insertion g (k i) ^ lookup x i)) = insertion (\<lambda>x. insertion g (k x)) (map_mpoly (insertion g) p)
[PROOF STEP]
unfolding insertion_altdef[of _ "map_mpoly f p" for f]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x. insertion g (MPoly_Type.coeff p x) * (\<Prod>i. insertion g (k i) ^ lookup x i)) = (\<Sum>m. MPoly_Type.coeff (map_mpoly (insertion g) p) m * (\<Prod>i. insertion g (k i) ^ lookup m i))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>x. insertion g (MPoly_Type.coeff p x) * (\<Prod>i. insertion g (k i) ^ lookup x i)) = insertion (\<lambda>x. insertion g (k x)) (map_mpoly (insertion g) p)

goal (1 subgoal):
 1. insertion g (insertion k p) = insertion (\<lambda>x. insertion g (k x)) (map_mpoly (insertion g) p)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
insertion g (insertion k p) = insertion (\<lambda>x. insertion g (k x)) (map_mpoly (insertion g) p)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
insertion g (insertion k p) = insertion (\<lambda>x. insertion g (k x)) (map_mpoly (insertion g) p)

goal (1 subgoal):
 1. insertion g (insertion k p) = insertion (\<lambda>x. insertion g (k x)) (map_mpoly (insertion g) p)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
insertion g (insertion k p) = insertion (\<lambda>x. insertion g (k x)) (map_mpoly (insertion g) p)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma insertion_substitute_linear:
  "insertion (\<lambda>i. c i * f i) p =
     insertion f (mapm_mpoly (\<lambda>m d. Prod_any (\<lambda>i. c i ^ lookup m i) * d) p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion (\<lambda>i. c i * f i) p = insertion f (mapm_mpoly (\<lambda>m. (*) (\<Prod>i. c i ^ lookup m i)) p)
[PROOF STEP]
unfolding insertion_altdef
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>m. MPoly_Type.coeff p m * (\<Prod>i. (c i * f i) ^ lookup m i)) = (\<Sum>m. MPoly_Type.coeff (mapm_mpoly (\<lambda>m. (*) (\<Prod>i. c i ^ lookup m i)) p) m * (\<Prod>i. f i ^ lookup m i))
[PROOF STEP]
proof (intro Sum_any.cong, goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. MPoly_Type.coeff p a * (\<Prod>i. (c i * f i) ^ lookup a i) = MPoly_Type.coeff (mapm_mpoly (\<lambda>m. (*) (\<Prod>i. c i ^ lookup m i)) p) a * (\<Prod>i. f i ^ lookup a i)
[PROOF STEP]
case (1 m)
[PROOF STATE]
proof (state)
this:

goal (1 subgoal):
 1. \<And>a. MPoly_Type.coeff p a * (\<Prod>i. (c i * f i) ^ lookup a i) = MPoly_Type.coeff (mapm_mpoly (\<lambda>m. (*) (\<Prod>i. c i ^ lookup m i)) p) a * (\<Prod>i. f i ^ lookup a i)
[PROOF STEP]
have "coeff (mapm_mpoly (\<lambda>m. (*) (\<Prod>i. c i ^ lookup m i)) p) m * (\<Prod>i. f i ^ lookup m i) =
          MPoly_Type.coeff p m * ((\<Prod>i. c i ^ lookup m i) * (\<Prod>i. f i ^ lookup m i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MPoly_Type.coeff (mapm_mpoly (\<lambda>m. (*) (\<Prod>i. c i ^ lookup m i)) p) m * (\<Prod>i. f i ^ lookup m i) = MPoly_Type.coeff p m * ((\<Prod>i. c i ^ lookup m i) * (\<Prod>i. f i ^ lookup m i))
[PROOF STEP]
by (simp add: mult_ac)
[PROOF STATE]
proof (state)
this:
MPoly_Type.coeff (mapm_mpoly (\<lambda>m. (*) (\<Prod>i. c i ^ lookup m i)) p) m * (\<Prod>i. f i ^ lookup m i) = MPoly_Type.coeff p m * ((\<Prod>i. c i ^ lookup m i) * (\<Prod>i. f i ^ lookup m i))

goal (1 subgoal):
 1. \<And>a. MPoly_Type.coeff p a * (\<Prod>i. (c i * f i) ^ lookup a i) = MPoly_Type.coeff (mapm_mpoly (\<lambda>m. (*) (\<Prod>i. c i ^ lookup m i)) p) a * (\<Prod>i. f i ^ lookup a i)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
MPoly_Type.coeff (mapm_mpoly (\<lambda>m. (*) (\<Prod>i. c i ^ lookup m i)) p) m * (\<Prod>i. f i ^ lookup m i) = MPoly_Type.coeff p m * ((\<Prod>i. c i ^ lookup m i) * (\<Prod>i. f i ^ lookup m i))

goal (1 subgoal):
 1. \<And>a. MPoly_Type.coeff p a * (\<Prod>i. (c i * f i) ^ lookup a i) = MPoly_Type.coeff (mapm_mpoly (\<lambda>m. (*) (\<Prod>i. c i ^ lookup m i)) p) a * (\<Prod>i. f i ^ lookup a i)
[PROOF STEP]
have "(\<Prod>i. c i ^ lookup m i) * (\<Prod>i. f i ^ lookup m i) =
               (\<Prod>i. (c i * f i) ^ lookup m i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>i. c i ^ lookup m i) * (\<Prod>i. f i ^ lookup m i) = (\<Prod>i. (c i * f i) ^ lookup m i)
[PROOF STEP]
by (subst Prod_any.distrib [symmetric])
       (auto simp: power_mult_distrib intro!: finite_subset[OF _ finite_lookup[of m]] Nat.gr0I)
[PROOF STATE]
proof (state)
this:
(\<Prod>i. c i ^ lookup m i) * (\<Prod>i. f i ^ lookup m i) = (\<Prod>i. (c i * f i) ^ lookup m i)

goal (1 subgoal):
 1. \<And>a. MPoly_Type.coeff p a * (\<Prod>i. (c i * f i) ^ lookup a i) = MPoly_Type.coeff (mapm_mpoly (\<lambda>m. (*) (\<Prod>i. c i ^ lookup m i)) p) a * (\<Prod>i. f i ^ lookup a i)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
MPoly_Type.coeff (mapm_mpoly (\<lambda>m. (*) (\<Prod>i. c i ^ lookup m i)) p) m * (\<Prod>i. f i ^ lookup m i) = MPoly_Type.coeff p m * (\<Prod>i. (c i * f i) ^ lookup m i)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
MPoly_Type.coeff (mapm_mpoly (\<lambda>m. (*) (\<Prod>i. c i ^ lookup m i)) p) m * (\<Prod>i. f i ^ lookup m i) = MPoly_Type.coeff p m * (\<Prod>i. (c i * f i) ^ lookup m i)

goal (1 subgoal):
 1. MPoly_Type.coeff p m * (\<Prod>i. (c i * f i) ^ lookup m i) = MPoly_Type.coeff (mapm_mpoly (\<lambda>m. (*) (\<Prod>i. c i ^ lookup m i)) p) m * (\<Prod>i. f i ^ lookup m i)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
MPoly_Type.coeff p m * (\<Prod>i. (c i * f i) ^ lookup m i) = MPoly_Type.coeff (mapm_mpoly (\<lambda>m. (*) (\<Prod>i. c i ^ lookup m i)) p) m * (\<Prod>i. f i ^ lookup m i)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vars_mapm_mpoly_subset: "vars (mapm_mpoly f p) \<subseteq> vars p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars (mapm_mpoly f p) \<subseteq> vars p
[PROOF STEP]
unfolding vars_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (keys ` keys (mapping_of (mapm_mpoly f p))) \<subseteq> \<Union> (keys ` keys (mapping_of p))
[PROOF STEP]
using keys_mapp_subset[of f]
[PROOF STATE]
proof (prove)
using this:
keys (Poly_Mapping.mapp f ?p) \<subseteq> keys ?p

goal (1 subgoal):
 1. \<Union> (keys ` keys (mapping_of (mapm_mpoly f p))) \<subseteq> \<Union> (keys ` keys (mapping_of p))
[PROOF STEP]
by (auto simp: mapm_mpoly.rep_eq)


[STATEMENT]
lemma map_mpoly_cong:
  assumes "\<And>m. f (coeff p m) = g (coeff p m)" "p = q"
  shows   "map_mpoly f p = map_mpoly g q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_mpoly f p = map_mpoly g q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
f (MPoly_Type.coeff p ?m) = g (MPoly_Type.coeff p ?m)
p = q

goal (1 subgoal):
 1. map_mpoly f p = map_mpoly g q
[PROOF STEP]
by (intro mpoly_eqI) (auto simp: coeff_map_mpoly)


[STATEMENT]
lemma lead_monom_geI [intro]:
  assumes "coeff p m \<noteq> 0"
  shows   "m \<le> lead_monom p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m \<le> lead_monom p
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
MPoly_Type.coeff p m \<noteq> (0::'a)

goal (1 subgoal):
 1. m \<le> lead_monom p
[PROOF STEP]
by (auto simp: lead_monom_def coeff_def in_keys_iff)


[STATEMENT]
lemma coeff_gt_lead_monom_zero [simp]:
  assumes "m > lead_monom p"
  shows   "coeff p m = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MPoly_Type.coeff p m = (0::'a)
[PROOF STEP]
using lead_monom_geI[of p m] assms
[PROOF STATE]
proof (prove)
using this:
MPoly_Type.coeff p m \<noteq> (0::'a) \<Longrightarrow> m \<le> lead_monom p
lead_monom p < m

goal (1 subgoal):
 1. MPoly_Type.coeff p m = (0::'a)
[PROOF STEP]
by force


[STATEMENT]
lemma lead_monom_nonzero_eq:
  assumes "p \<noteq> 0"
  shows   "lead_monom p = Max (keys (mapping_of p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lead_monom p = Max (keys (mapping_of p))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
p \<noteq> 0

goal (1 subgoal):
 1. lead_monom p = Max (keys (mapping_of p))
[PROOF STEP]
by transfer (simp add: max_def)


[STATEMENT]
lemma lead_monom_0 [simp]: "lead_monom 0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lead_monom 0 = 0
[PROOF STEP]
by (simp add: lead_monom_def zero_mpoly.rep_eq)


[STATEMENT]
lemma lead_monom_1 [simp]: "lead_monom 1 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lead_monom 1 = 0
[PROOF STEP]
by (simp add: lead_monom_def one_mpoly.rep_eq)


[STATEMENT]
lemma lead_monom_Const [simp]: "lead_monom (Const c) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lead_monom (Const c) = 0
[PROOF STEP]
by (simp add: lead_monom_def Const.rep_eq Const\<^sub>0_def)


[STATEMENT]
lemma keys_mult_const [simp]:
  fixes c :: "'a :: {semiring_0, semiring_no_zero_divisors}"
  assumes "c \<noteq> 0"
  shows "keys (Poly_Mapping.map ((*) c) p) = keys p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. keys (Poly_Mapping.map ((*) c) p) = keys p
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
c \<noteq> (0::'a)

goal (1 subgoal):
 1. keys (Poly_Mapping.map ((*) c) p) = keys p
[PROOF STEP]
by transfer auto


[STATEMENT]
lemma lead_monom_eq_0_iff: "lead_monom p = 0 \<longleftrightarrow> vars p = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (lead_monom p = 0) = (vars p = {})
[PROOF STEP]
unfolding vars_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (lead_monom p = 0) = (\<Union> (keys ` keys (mapping_of p)) = {})
[PROOF STEP]
by transfer' (auto simp: Max_eq_iff)


[STATEMENT]
lemma lead_monom_monom: "lead_monom (monom m c) = (if c = 0 then 0 else m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lead_monom (MPoly_Type.monom m c) = (if c = (0::'a) then 0 else m)
[PROOF STEP]
by (auto simp add: lead_monom_def monom.rep_eq Const\<^sub>0_def max_def )


[STATEMENT]
lemma lead_monom_monom' [simp]: "c \<noteq> 0 \<Longrightarrow> lead_monom (monom m c) = m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c \<noteq> (0::'a) \<Longrightarrow> lead_monom (MPoly_Type.monom m c) = m
[PROOF STEP]
by (simp add: lead_monom_monom)


[STATEMENT]
lemma lead_monom_numeral [simp]: "lead_monom (numeral n) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lead_monom (numeral n) = 0
[PROOF STEP]
unfolding monom_numeral[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lead_monom (MPoly_Type.monom 0 (numeral n)) = 0
[PROOF STEP]
by (subst lead_monom_monom) auto


[STATEMENT]
lemma lead_monom_add: "lead_monom (p + q) \<le> max (lead_monom p) (lead_monom q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lead_monom (p + q) \<le> max (lead_monom p) (lead_monom q)
[PROOF STEP]
proof transfer
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p q. Max (insert 0 (keys (p + q))) \<le> max (Max (insert 0 (keys p))) (Max (insert 0 (keys q)))
[PROOF STEP]
fix p q :: "(nat \<Rightarrow>\<^sub>0 nat) \<Rightarrow>\<^sub>0 'a"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p q. Max (insert 0 (keys (p + q))) \<le> max (Max (insert 0 (keys p))) (Max (insert 0 (keys q)))
[PROOF STEP]
show "Max (insert 0 (keys (p + q))) \<le> max (Max (insert 0 (keys p))) (Max (insert 0 (keys q)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Max (insert 0 (keys (p + q))) \<le> max (Max (insert 0 (keys p))) (Max (insert 0 (keys q)))
[PROOF STEP]
proof (rule Max.boundedI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. finite (insert 0 (keys (p + q)))
 2. insert 0 (keys (p + q)) \<noteq> {}
 3. \<And>a. a \<in> insert 0 (keys (p + q)) \<Longrightarrow> a \<le> max (Max (insert 0 (keys p))) (Max (insert 0 (keys q)))
[PROOF STEP]
fix m
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. finite (insert 0 (keys (p + q)))
 2. insert 0 (keys (p + q)) \<noteq> {}
 3. \<And>a. a \<in> insert 0 (keys (p + q)) \<Longrightarrow> a \<le> max (Max (insert 0 (keys p))) (Max (insert 0 (keys q)))
[PROOF STEP]
assume m: "m \<in> insert 0 (keys (p + q))"
[PROOF STATE]
proof (state)
this:
m \<in> insert 0 (keys (p + q))

goal (3 subgoals):
 1. finite (insert 0 (keys (p + q)))
 2. insert 0 (keys (p + q)) \<noteq> {}
 3. \<And>a. a \<in> insert 0 (keys (p + q)) \<Longrightarrow> a \<le> max (Max (insert 0 (keys p))) (Max (insert 0 (keys q)))
[PROOF STEP]
thus "m \<le> max (Max (insert 0 (keys p))) (Max (insert 0 (keys q)))"
[PROOF STATE]
proof (prove)
using this:
m \<in> insert 0 (keys (p + q))

goal (1 subgoal):
 1. m \<le> max (Max (insert 0 (keys p))) (Max (insert 0 (keys q)))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. m = 0 \<Longrightarrow> m \<le> max (Max (insert 0 (keys p))) (Max (insert 0 (keys q)))
 2. m \<in> keys (p + q) \<Longrightarrow> m \<le> max (Max (insert 0 (keys p))) (Max (insert 0 (keys q)))
[PROOF STEP]
assume "m \<in> keys (p + q)"
[PROOF STATE]
proof (state)
this:
m \<in> keys (p + q)

goal (2 subgoals):
 1. m = 0 \<Longrightarrow> m \<le> max (Max (insert 0 (keys p))) (Max (insert 0 (keys q)))
 2. m \<in> keys (p + q) \<Longrightarrow> m \<le> max (Max (insert 0 (keys p))) (Max (insert 0 (keys q)))
[PROOF STEP]
with keys_add[of p q]
[PROOF STATE]
proof (chain)
picking this:
keys p \<inter> keys q = {} \<Longrightarrow> keys p \<union> keys q = keys (p + q)
m \<in> keys (p + q)
[PROOF STEP]
have "m \<in> keys p \<or> m \<in> keys q"
[PROOF STATE]
proof (prove)
using this:
keys p \<inter> keys q = {} \<Longrightarrow> keys p \<union> keys q = keys (p + q)
m \<in> keys (p + q)

goal (1 subgoal):
 1. m \<in> keys p \<or> m \<in> keys q
[PROOF STEP]
by (auto simp: in_keys_iff plus_poly_mapping.rep_eq)
[PROOF STATE]
proof (state)
this:
m \<in> keys p \<or> m \<in> keys q

goal (2 subgoals):
 1. m = 0 \<Longrightarrow> m \<le> max (Max (insert 0 (keys p))) (Max (insert 0 (keys q)))
 2. m \<in> keys (p + q) \<Longrightarrow> m \<le> max (Max (insert 0 (keys p))) (Max (insert 0 (keys q)))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
m \<in> keys p \<or> m \<in> keys q

goal (1 subgoal):
 1. m \<le> max (Max (insert 0 (keys p))) (Max (insert 0 (keys q)))
[PROOF STEP]
by (auto simp: le_max_iff_disj)
[PROOF STATE]
proof (state)
this:
m \<le> max (Max (insert 0 (keys p))) (Max (insert 0 (keys q)))

goal (1 subgoal):
 1. m = 0 \<Longrightarrow> m \<le> max (Max (insert 0 (keys p))) (Max (insert 0 (keys q)))
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
m \<le> max (Max (insert 0 (keys p))) (Max (insert 0 (keys q)))

goal (2 subgoals):
 1. finite (insert 0 (keys (p + q)))
 2. insert 0 (keys (p + q)) \<noteq> {}
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
Max (insert 0 (keys (p + q))) \<le> max (Max (insert 0 (keys p))) (Max (insert 0 (keys q)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vars_empty_iff: "vars p = {} \<longleftrightarrow> p = Const (lead_coeff p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (vars p = {}) = (p = Const (Symmetric_Polynomials.lead_coeff p))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. vars p = {} \<Longrightarrow> p = Const (Symmetric_Polynomials.lead_coeff p)
 2. p = Const (Symmetric_Polynomials.lead_coeff p) \<Longrightarrow> vars p = {}
[PROOF STEP]
assume "vars p = {}"
[PROOF STATE]
proof (state)
this:
vars p = {}

goal (2 subgoals):
 1. vars p = {} \<Longrightarrow> p = Const (Symmetric_Polynomials.lead_coeff p)
 2. p = Const (Symmetric_Polynomials.lead_coeff p) \<Longrightarrow> vars p = {}
[PROOF STEP]
hence [simp]: "lead_monom p = 0"
[PROOF STATE]
proof (prove)
using this:
vars p = {}

goal (1 subgoal):
 1. lead_monom p = 0
[PROOF STEP]
by (simp add: lead_monom_eq_0_iff)
[PROOF STATE]
proof (state)
this:
lead_monom p = 0

goal (2 subgoals):
 1. vars p = {} \<Longrightarrow> p = Const (Symmetric_Polynomials.lead_coeff p)
 2. p = Const (Symmetric_Polynomials.lead_coeff p) \<Longrightarrow> vars p = {}
[PROOF STEP]
have [simp]: "mon \<noteq> 0 \<longleftrightarrow> (mon > (0 :: nat \<Rightarrow>\<^sub>0 nat))" for mon
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (mon \<noteq> 0) = (0 < mon)
[PROOF STEP]
by (auto simp: order.strict_iff_order)
[PROOF STATE]
proof (state)
this:
(?mon \<noteq> 0) = (0 < ?mon)

goal (2 subgoals):
 1. vars p = {} \<Longrightarrow> p = Const (Symmetric_Polynomials.lead_coeff p)
 2. p = Const (Symmetric_Polynomials.lead_coeff p) \<Longrightarrow> vars p = {}
[PROOF STEP]
thus "p = Const (lead_coeff p)"
[PROOF STATE]
proof (prove)
using this:
(?mon \<noteq> 0) = (0 < ?mon)

goal (1 subgoal):
 1. p = Const (Symmetric_Polynomials.lead_coeff p)
[PROOF STEP]
by (intro mpoly_eqI) (auto simp: mpoly_coeff_Const lead_coeff_def)
[PROOF STATE]
proof (state)
this:
p = Const (Symmetric_Polynomials.lead_coeff p)

goal (1 subgoal):
 1. p = Const (Symmetric_Polynomials.lead_coeff p) \<Longrightarrow> vars p = {}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p = Const (Symmetric_Polynomials.lead_coeff p) \<Longrightarrow> vars p = {}
[PROOF STEP]
assume "p = Const (lead_coeff p)"
[PROOF STATE]
proof (state)
this:
p = Const (Symmetric_Polynomials.lead_coeff p)

goal (1 subgoal):
 1. p = Const (Symmetric_Polynomials.lead_coeff p) \<Longrightarrow> vars p = {}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
p = Const (Symmetric_Polynomials.lead_coeff p)

goal (1 subgoal):
 1. p = Const (Symmetric_Polynomials.lead_coeff p) \<Longrightarrow> vars p = {}
[PROOF STEP]
have "vars \<dots> = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars (Const (Symmetric_Polynomials.lead_coeff p)) = {}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vars (Const (Symmetric_Polynomials.lead_coeff p)) = {}

goal (1 subgoal):
 1. p = Const (Symmetric_Polynomials.lead_coeff p) \<Longrightarrow> vars p = {}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
vars p = {}
[PROOF STEP]
show "vars p = {}"
[PROOF STATE]
proof (prove)
using this:
vars p = {}

goal (1 subgoal):
 1. vars p = {}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
vars p = {}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lead_coeff_0 [simp]: "lead_coeff 0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Symmetric_Polynomials.lead_coeff 0 = (0::'a)
[PROOF STEP]
by (simp add: lead_coeff_def)


[STATEMENT]
lemma lead_coeff_1 [simp]: "lead_coeff 1 = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Symmetric_Polynomials.lead_coeff 1 = (1::'a)
[PROOF STEP]
by (simp add: lead_coeff_def mpoly_coeff_1)


[STATEMENT]
lemma lead_coeff_Const [simp]: "lead_coeff (Const c) = c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Symmetric_Polynomials.lead_coeff (Const c) = c
[PROOF STEP]
by (simp add: lead_coeff_def mpoly_coeff_Const)


[STATEMENT]
lemma lead_coeff_monom [simp]: "lead_coeff (monom p c) = c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Symmetric_Polynomials.lead_coeff (MPoly_Type.monom p c) = c
[PROOF STEP]
by (simp add: lead_coeff_def coeff_monom when_def lead_monom_monom)


[STATEMENT]
lemma lead_coeff_nonzero [simp]: "p \<noteq> 0 \<Longrightarrow> lead_coeff p \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<noteq> 0 \<Longrightarrow> Symmetric_Polynomials.lead_coeff p \<noteq> (0::'a)
[PROOF STEP]
unfolding lead_coeff_def lead_monom_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<noteq> 0 \<Longrightarrow> MPoly_Type.coeff p (map_fun mapping_of id (\<lambda>f. Max (insert 0 (keys f))) p) \<noteq> (0::'a)
[PROOF STEP]
by (cases "keys (mapping_of p) = {}") (auto simp: coeff_def max_def)


[STATEMENT]
lemma lead_coeff_mult_aux:
  "coeff (p * q) (lead_monom p + lead_monom q) = lead_coeff p * lead_coeff q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MPoly_Type.coeff (p * q) (lead_monom p + lead_monom q) = Symmetric_Polynomials.lead_coeff p * Symmetric_Polynomials.lead_coeff q
[PROOF STEP]
proof (cases "p = 0 \<or> q = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p = 0 \<or> q = 0 \<Longrightarrow> MPoly_Type.coeff (p * q) (lead_monom p + lead_monom q) = Symmetric_Polynomials.lead_coeff p * Symmetric_Polynomials.lead_coeff q
 2. \<not> (p = 0 \<or> q = 0) \<Longrightarrow> MPoly_Type.coeff (p * q) (lead_monom p + lead_monom q) = Symmetric_Polynomials.lead_coeff p * Symmetric_Polynomials.lead_coeff q
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (p = 0 \<or> q = 0)

goal (2 subgoals):
 1. p = 0 \<or> q = 0 \<Longrightarrow> MPoly_Type.coeff (p * q) (lead_monom p + lead_monom q) = Symmetric_Polynomials.lead_coeff p * Symmetric_Polynomials.lead_coeff q
 2. \<not> (p = 0 \<or> q = 0) \<Longrightarrow> MPoly_Type.coeff (p * q) (lead_monom p + lead_monom q) = Symmetric_Polynomials.lead_coeff p * Symmetric_Polynomials.lead_coeff q
[PROOF STEP]
define a b where "a = lead_monom p" and "b = lead_monom q"
[PROOF STATE]
proof (state)
this:
a = lead_monom p
b = lead_monom q

goal (2 subgoals):
 1. p = 0 \<or> q = 0 \<Longrightarrow> MPoly_Type.coeff (p * q) (lead_monom p + lead_monom q) = Symmetric_Polynomials.lead_coeff p * Symmetric_Polynomials.lead_coeff q
 2. \<not> (p = 0 \<or> q = 0) \<Longrightarrow> MPoly_Type.coeff (p * q) (lead_monom p + lead_monom q) = Symmetric_Polynomials.lead_coeff p * Symmetric_Polynomials.lead_coeff q
[PROOF STEP]
have "coeff (p * q) (a + b) = coeff p a * coeff q b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MPoly_Type.coeff (p * q) (a + b) = MPoly_Type.coeff p a * MPoly_Type.coeff q b
[PROOF STEP]
unfolding coeff_mpoly_times
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prod_fun (MPoly_Type.coeff p) (MPoly_Type.coeff q) (a + b) = MPoly_Type.coeff p a * MPoly_Type.coeff q b
[PROOF STEP]
by (rule prod_fun_max) (insert False, auto simp: a_def b_def)
[PROOF STATE]
proof (state)
this:
MPoly_Type.coeff (p * q) (a + b) = MPoly_Type.coeff p a * MPoly_Type.coeff q b

goal (2 subgoals):
 1. p = 0 \<or> q = 0 \<Longrightarrow> MPoly_Type.coeff (p * q) (lead_monom p + lead_monom q) = Symmetric_Polynomials.lead_coeff p * Symmetric_Polynomials.lead_coeff q
 2. \<not> (p = 0 \<or> q = 0) \<Longrightarrow> MPoly_Type.coeff (p * q) (lead_monom p + lead_monom q) = Symmetric_Polynomials.lead_coeff p * Symmetric_Polynomials.lead_coeff q
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
MPoly_Type.coeff (p * q) (a + b) = MPoly_Type.coeff p a * MPoly_Type.coeff q b

goal (1 subgoal):
 1. MPoly_Type.coeff (p * q) (lead_monom p + lead_monom q) = Symmetric_Polynomials.lead_coeff p * Symmetric_Polynomials.lead_coeff q
[PROOF STEP]
by (simp add: a_def b_def lead_coeff_def)
[PROOF STATE]
proof (state)
this:
MPoly_Type.coeff (p * q) (lead_monom p + lead_monom q) = Symmetric_Polynomials.lead_coeff p * Symmetric_Polynomials.lead_coeff q

goal (1 subgoal):
 1. p = 0 \<or> q = 0 \<Longrightarrow> MPoly_Type.coeff (p * q) (lead_monom p + lead_monom q) = Symmetric_Polynomials.lead_coeff p * Symmetric_Polynomials.lead_coeff q
[PROOF STEP]
qed auto


[STATEMENT]
lemma lead_monom_mult_le: "lead_monom (p * q) \<le> lead_monom p + lead_monom q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lead_monom (p * q) \<le> lead_monom p + lead_monom q
[PROOF STEP]
proof (cases "p * q = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p * q = 0 \<Longrightarrow> lead_monom (p * q) \<le> lead_monom p + lead_monom q
 2. p * q \<noteq> 0 \<Longrightarrow> lead_monom (p * q) \<le> lead_monom p + lead_monom q
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
p * q \<noteq> 0

goal (2 subgoals):
 1. p * q = 0 \<Longrightarrow> lead_monom (p * q) \<le> lead_monom p + lead_monom q
 2. p * q \<noteq> 0 \<Longrightarrow> lead_monom (p * q) \<le> lead_monom p + lead_monom q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lead_monom (p * q) \<le> lead_monom p + lead_monom q
[PROOF STEP]
proof (intro leI notI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lead_monom p + lead_monom q < lead_monom (p * q) \<Longrightarrow> False
[PROOF STEP]
assume "lead_monom p + lead_monom q < lead_monom (p * q)"
[PROOF STATE]
proof (state)
this:
lead_monom p + lead_monom q < lead_monom (p * q)

goal (1 subgoal):
 1. lead_monom p + lead_monom q < lead_monom (p * q) \<Longrightarrow> False
[PROOF STEP]
hence "lead_coeff (p * q) = 0"
[PROOF STATE]
proof (prove)
using this:
lead_monom p + lead_monom q < lead_monom (p * q)

goal (1 subgoal):
 1. Symmetric_Polynomials.lead_coeff (p * q) = (0::'a)
[PROOF STEP]
unfolding lead_coeff_def coeff_mpoly_times
[PROOF STATE]
proof (prove)
using this:
lead_monom p + lead_monom q < lead_monom (p * q)

goal (1 subgoal):
 1. prod_fun (MPoly_Type.coeff p) (MPoly_Type.coeff q) (lead_monom (p * q)) = (0::'a)
[PROOF STEP]
by (rule prod_fun_gt_max_eq_zero) auto
[PROOF STATE]
proof (state)
this:
Symmetric_Polynomials.lead_coeff (p * q) = (0::'a)

goal (1 subgoal):
 1. lead_monom p + lead_monom q < lead_monom (p * q) \<Longrightarrow> False
[PROOF STEP]
with False
[PROOF STATE]
proof (chain)
picking this:
p * q \<noteq> 0
Symmetric_Polynomials.lead_coeff (p * q) = (0::'a)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
p * q \<noteq> 0
Symmetric_Polynomials.lead_coeff (p * q) = (0::'a)

goal (1 subgoal):
 1. False
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
lead_monom (p * q) \<le> lead_monom p + lead_monom q

goal (1 subgoal):
 1. p * q = 0 \<Longrightarrow> lead_monom (p * q) \<le> lead_monom p + lead_monom q
[PROOF STEP]
qed auto


[STATEMENT]
lemma lead_monom_mult:
  assumes "lead_coeff p * lead_coeff q \<noteq> 0"
  shows   "lead_monom (p * q) = lead_monom p + lead_monom q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lead_monom (p * q) = lead_monom p + lead_monom q
[PROOF STEP]
by (intro antisym lead_monom_mult_le lead_monom_geI)
     (insert assms, auto simp: lead_coeff_mult_aux)


[STATEMENT]
lemma lead_coeff_mult:
  assumes "lead_coeff p * lead_coeff q \<noteq> 0"
  shows   "lead_coeff (p * q) = lead_coeff p * lead_coeff q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Symmetric_Polynomials.lead_coeff (p * q) = Symmetric_Polynomials.lead_coeff p * Symmetric_Polynomials.lead_coeff q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Symmetric_Polynomials.lead_coeff p * Symmetric_Polynomials.lead_coeff q \<noteq> (0::'a)

goal (1 subgoal):
 1. Symmetric_Polynomials.lead_coeff (p * q) = Symmetric_Polynomials.lead_coeff p * Symmetric_Polynomials.lead_coeff q
[PROOF STEP]
by (simp add: lead_monom_mult lead_coeff_mult_aux lead_coeff_def)


[STATEMENT]
lemma keys_lead_monom_subset: "keys (lead_monom p) \<subseteq> vars p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. keys (lead_monom p) \<subseteq> vars p
[PROOF STEP]
proof (cases "p = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p = 0 \<Longrightarrow> keys (lead_monom p) \<subseteq> vars p
 2. p \<noteq> 0 \<Longrightarrow> keys (lead_monom p) \<subseteq> vars p
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
p \<noteq> 0

goal (2 subgoals):
 1. p = 0 \<Longrightarrow> keys (lead_monom p) \<subseteq> vars p
 2. p \<noteq> 0 \<Longrightarrow> keys (lead_monom p) \<subseteq> vars p
[PROOF STEP]
hence "lead_coeff p \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
p \<noteq> 0

goal (1 subgoal):
 1. Symmetric_Polynomials.lead_coeff p \<noteq> (0::'a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Symmetric_Polynomials.lead_coeff p \<noteq> (0::'a)

goal (2 subgoals):
 1. p = 0 \<Longrightarrow> keys (lead_monom p) \<subseteq> vars p
 2. p \<noteq> 0 \<Longrightarrow> keys (lead_monom p) \<subseteq> vars p
[PROOF STEP]
hence "coeff p (lead_monom p) \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
Symmetric_Polynomials.lead_coeff p \<noteq> (0::'a)

goal (1 subgoal):
 1. MPoly_Type.coeff p (lead_monom p) \<noteq> (0::'a)
[PROOF STEP]
unfolding lead_coeff_def
[PROOF STATE]
proof (prove)
using this:
MPoly_Type.coeff p (lead_monom p) \<noteq> (0::'a)

goal (1 subgoal):
 1. MPoly_Type.coeff p (lead_monom p) \<noteq> (0::'a)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
MPoly_Type.coeff p (lead_monom p) \<noteq> (0::'a)

goal (2 subgoals):
 1. p = 0 \<Longrightarrow> keys (lead_monom p) \<subseteq> vars p
 2. p \<noteq> 0 \<Longrightarrow> keys (lead_monom p) \<subseteq> vars p
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
MPoly_Type.coeff p (lead_monom p) \<noteq> (0::'a)

goal (1 subgoal):
 1. keys (lead_monom p) \<subseteq> vars p
[PROOF STEP]
unfolding vars_def
[PROOF STATE]
proof (prove)
using this:
MPoly_Type.coeff p (lead_monom p) \<noteq> (0::'a)

goal (1 subgoal):
 1. keys (lead_monom p) \<subseteq> \<Union> (keys ` keys (mapping_of p))
[PROOF STEP]
by transfer' (auto simp: max_def in_keys_iff)
[PROOF STATE]
proof (state)
this:
keys (lead_monom p) \<subseteq> vars p

goal (1 subgoal):
 1. p = 0 \<Longrightarrow> keys (lead_monom p) \<subseteq> vars p
[PROOF STEP]
qed auto


[STATEMENT]
lemma lead_monom_sum_le: "(\<And>x. x \<in> X \<Longrightarrow> lead_monom (h x) \<le> ub) \<Longrightarrow> lead_monom (sum h X) \<le> ub"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. x \<in> X \<Longrightarrow> lead_monom (h x) \<le> ub) \<Longrightarrow> lead_monom (sum h X) \<le> ub
[PROOF STEP]
by (induction X rule: infinite_finite_induct) (auto intro!: order.trans[OF lead_monom_add])


[STATEMENT]
lemma lead_monom_sum:
  assumes "inj_on (lead_monom \<circ> h) X" and "finite X" and "X \<noteq> {}" and "\<And>x. x \<in> X \<Longrightarrow> h x \<noteq> 0"
  defines "m \<equiv> Max ((lead_monom \<circ> h) ` X)"
  shows   "lead_monom (\<Sum>x\<in>X. h x) = m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lead_monom (sum h X) = m
[PROOF STEP]
proof (rule antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. lead_monom (sum h X) \<le> m
 2. m \<le> lead_monom (sum h X)
[PROOF STEP]
show "lead_monom (sum h X) \<le> m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lead_monom (sum h X) \<le> m
[PROOF STEP]
unfolding m_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lead_monom (sum h X) \<le> Max ((lead_monom \<circ> h) ` X)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
inj_on (lead_monom \<circ> h) X
finite X
X \<noteq> {}
?x \<in> X \<Longrightarrow> h ?x \<noteq> 0
m \<equiv> Max ((lead_monom \<circ> h) ` X)

goal (1 subgoal):
 1. lead_monom (sum h X) \<le> Max ((lead_monom \<circ> h) ` X)
[PROOF STEP]
by (intro lead_monom_sum_le Max_ge finite_imageI) auto
[PROOF STATE]
proof (state)
this:
lead_monom (sum h X) \<le> m

goal (1 subgoal):
 1. m \<le> lead_monom (sum h X)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. m \<le> lead_monom (sum h X)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
inj_on (lead_monom \<circ> h) X
finite X
X \<noteq> {}
?x \<in> X \<Longrightarrow> h ?x \<noteq> 0
m \<equiv> Max ((lead_monom \<circ> h) ` X)
[PROOF STEP]
have "m \<in> (lead_monom \<circ> h) ` X"
[PROOF STATE]
proof (prove)
using this:
inj_on (lead_monom \<circ> h) X
finite X
X \<noteq> {}
?x \<in> X \<Longrightarrow> h ?x \<noteq> 0
m \<equiv> Max ((lead_monom \<circ> h) ` X)

goal (1 subgoal):
 1. m \<in> (lead_monom \<circ> h) ` X
[PROOF STEP]
unfolding m_def
[PROOF STATE]
proof (prove)
using this:
inj_on (lead_monom \<circ> h) X
finite X
X \<noteq> {}
?x \<in> X \<Longrightarrow> h ?x \<noteq> 0
Max ((lead_monom \<circ> h) ` X) \<equiv> Max ((lead_monom \<circ> h) ` X)

goal (1 subgoal):
 1. Max ((lead_monom \<circ> h) ` X) \<in> (lead_monom \<circ> h) ` X
[PROOF STEP]
by (intro Max_in finite_imageI) auto
[PROOF STATE]
proof (state)
this:
m \<in> (lead_monom \<circ> h) ` X

goal (1 subgoal):
 1. m \<le> lead_monom (sum h X)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
m \<in> (lead_monom \<circ> h) ` X
[PROOF STEP]
obtain x where x: "x \<in> X" "m = lead_monom (h x)"
[PROOF STATE]
proof (prove)
using this:
m \<in> (lead_monom \<circ> h) ` X

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> X; m = lead_monom (h x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> X
m = lead_monom (h x)

goal (1 subgoal):
 1. m \<le> lead_monom (sum h X)
[PROOF STEP]
have "coeff (\<Sum>x\<in>X. h x) m = (\<Sum>x\<in>X. coeff (h x) m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MPoly_Type.coeff (sum h X) m = (\<Sum>x\<in>X. MPoly_Type.coeff (h x) m)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
MPoly_Type.coeff (sum h X) m = (\<Sum>x\<in>X. MPoly_Type.coeff (h x) m)

goal (1 subgoal):
 1. m \<le> lead_monom (sum h X)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
MPoly_Type.coeff (sum h X) m = (\<Sum>x\<in>X. MPoly_Type.coeff (h x) m)

goal (1 subgoal):
 1. m \<le> lead_monom (sum h X)
[PROOF STEP]
have "\<dots> = (\<Sum>x\<in>{x}. coeff (h x) m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>X. MPoly_Type.coeff (h x) m) = (\<Sum>x\<in>{x}. MPoly_Type.coeff (h x) m)
[PROOF STEP]
proof (intro sum.mono_neutral_right ballI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. finite X
 2. {x} \<subseteq> X
 3. \<And>i. i \<in> X - {x} \<Longrightarrow> MPoly_Type.coeff (h i) m = (0::'b)
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. finite X
 2. {x} \<subseteq> X
 3. \<And>i. i \<in> X - {x} \<Longrightarrow> MPoly_Type.coeff (h i) m = (0::'b)
[PROOF STEP]
assume y: "y \<in> X - {x}"
[PROOF STATE]
proof (state)
this:
y \<in> X - {x}

goal (3 subgoals):
 1. finite X
 2. {x} \<subseteq> X
 3. \<And>i. i \<in> X - {x} \<Longrightarrow> MPoly_Type.coeff (h i) m = (0::'b)
[PROOF STEP]
hence "(lead_monom \<circ> h) y \<le> m"
[PROOF STATE]
proof (prove)
using this:
y \<in> X - {x}

goal (1 subgoal):
 1. (lead_monom \<circ> h) y \<le> m
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
y \<in> X - {x}
inj_on (lead_monom \<circ> h) X
finite X
X \<noteq> {}
?x \<in> X \<Longrightarrow> h ?x \<noteq> 0
m \<equiv> Max ((lead_monom \<circ> h) ` X)

goal (1 subgoal):
 1. (lead_monom \<circ> h) y \<le> m
[PROOF STEP]
unfolding m_def
[PROOF STATE]
proof (prove)
using this:
y \<in> X - {x}
inj_on (lead_monom \<circ> h) X
finite X
X \<noteq> {}
?x \<in> X \<Longrightarrow> h ?x \<noteq> 0
Max ((lead_monom \<circ> h) ` X) \<equiv> Max ((lead_monom \<circ> h) ` X)

goal (1 subgoal):
 1. (lead_monom \<circ> h) y \<le> Max ((lead_monom \<circ> h) ` X)
[PROOF STEP]
by (intro Max_ge finite_imageI) auto
[PROOF STATE]
proof (state)
this:
(lead_monom \<circ> h) y \<le> m

goal (3 subgoals):
 1. finite X
 2. {x} \<subseteq> X
 3. \<And>i. i \<in> X - {x} \<Longrightarrow> MPoly_Type.coeff (h i) m = (0::'b)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(lead_monom \<circ> h) y \<le> m

goal (3 subgoals):
 1. finite X
 2. {x} \<subseteq> X
 3. \<And>i. i \<in> X - {x} \<Longrightarrow> MPoly_Type.coeff (h i) m = (0::'b)
[PROOF STEP]
have "(lead_monom \<circ> h) y \<noteq> (lead_monom \<circ> h) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (lead_monom \<circ> h) y \<noteq> (lead_monom \<circ> h) x
[PROOF STEP]
using \<open>x \<in> X\<close> y inj_onD[OF assms(1), of x y]
[PROOF STATE]
proof (prove)
using this:
x \<in> X
y \<in> X - {x}
\<lbrakk>(lead_monom \<circ> h) x = (lead_monom \<circ> h) y; x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> x = y

goal (1 subgoal):
 1. (lead_monom \<circ> h) y \<noteq> (lead_monom \<circ> h) x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(lead_monom \<circ> h) y \<noteq> (lead_monom \<circ> h) x

goal (3 subgoals):
 1. finite X
 2. {x} \<subseteq> X
 3. \<And>i. i \<in> X - {x} \<Longrightarrow> MPoly_Type.coeff (h i) m = (0::'b)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(lead_monom \<circ> h) y \<le> m
(lead_monom \<circ> h) y \<noteq> (lead_monom \<circ> h) x
[PROOF STEP]
have "lead_monom (h y) < m"
[PROOF STATE]
proof (prove)
using this:
(lead_monom \<circ> h) y \<le> m
(lead_monom \<circ> h) y \<noteq> (lead_monom \<circ> h) x

goal (1 subgoal):
 1. lead_monom (h y) < m
[PROOF STEP]
using x
[PROOF STATE]
proof (prove)
using this:
(lead_monom \<circ> h) y \<le> m
(lead_monom \<circ> h) y \<noteq> (lead_monom \<circ> h) x
x \<in> X
m = lead_monom (h x)

goal (1 subgoal):
 1. lead_monom (h y) < m
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lead_monom (h y) < m

goal (3 subgoals):
 1. finite X
 2. {x} \<subseteq> X
 3. \<And>i. i \<in> X - {x} \<Longrightarrow> MPoly_Type.coeff (h i) m = (0::'b)
[PROOF STEP]
thus "coeff (h y) m = 0"
[PROOF STATE]
proof (prove)
using this:
lead_monom (h y) < m

goal (1 subgoal):
 1. MPoly_Type.coeff (h y) m = (0::'b)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
MPoly_Type.coeff (h y) m = (0::'b)

goal (2 subgoals):
 1. finite X
 2. {x} \<subseteq> X
[PROOF STEP]
qed (insert x assms, auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>X. MPoly_Type.coeff (h x) m) = (\<Sum>x\<in>{x}. MPoly_Type.coeff (h x) m)

goal (1 subgoal):
 1. m \<le> lead_monom (sum h X)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>X. MPoly_Type.coeff (h x) m) = (\<Sum>x\<in>{x}. MPoly_Type.coeff (h x) m)

goal (1 subgoal):
 1. m \<le> lead_monom (sum h X)
[PROOF STEP]
have "\<dots> = coeff (h x) m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>{x}. MPoly_Type.coeff (h x) m) = MPoly_Type.coeff (h x) m
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>{x}. MPoly_Type.coeff (h x) m) = MPoly_Type.coeff (h x) m

goal (1 subgoal):
 1. m \<le> lead_monom (sum h X)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>{x}. MPoly_Type.coeff (h x) m) = MPoly_Type.coeff (h x) m

goal (1 subgoal):
 1. m \<le> lead_monom (sum h X)
[PROOF STEP]
have "\<dots> = lead_coeff (h x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MPoly_Type.coeff (h x) m = Symmetric_Polynomials.lead_coeff (h x)
[PROOF STEP]
using x
[PROOF STATE]
proof (prove)
using this:
x \<in> X
m = lead_monom (h x)

goal (1 subgoal):
 1. MPoly_Type.coeff (h x) m = Symmetric_Polynomials.lead_coeff (h x)
[PROOF STEP]
by (simp add: lead_coeff_def)
[PROOF STATE]
proof (state)
this:
MPoly_Type.coeff (h x) m = Symmetric_Polynomials.lead_coeff (h x)

goal (1 subgoal):
 1. m \<le> lead_monom (sum h X)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
MPoly_Type.coeff (h x) m = Symmetric_Polynomials.lead_coeff (h x)

goal (1 subgoal):
 1. m \<le> lead_monom (sum h X)
[PROOF STEP]
have "\<dots> \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Symmetric_Polynomials.lead_coeff (h x) \<noteq> (0::'b)
[PROOF STEP]
using assms x
[PROOF STATE]
proof (prove)
using this:
inj_on (lead_monom \<circ> h) X
finite X
X \<noteq> {}
?x \<in> X \<Longrightarrow> h ?x \<noteq> 0
m \<equiv> Max ((lead_monom \<circ> h) ` X)
x \<in> X
m = lead_monom (h x)

goal (1 subgoal):
 1. Symmetric_Polynomials.lead_coeff (h x) \<noteq> (0::'b)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Symmetric_Polynomials.lead_coeff (h x) \<noteq> (0::'b)

goal (1 subgoal):
 1. m \<le> lead_monom (sum h X)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
MPoly_Type.coeff (sum h X) m \<noteq> (0::'b)
[PROOF STEP]
show "lead_monom (sum h X) \<ge> m"
[PROOF STATE]
proof (prove)
using this:
MPoly_Type.coeff (sum h X) m \<noteq> (0::'b)

goal (1 subgoal):
 1. m \<le> lead_monom (sum h X)
[PROOF STEP]
by (intro lead_monom_geI)
[PROOF STATE]
proof (state)
this:
m \<le> lead_monom (sum h X)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lead_coeff_eq_0_iff [simp]: "lead_coeff p = 0 \<longleftrightarrow> p = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Symmetric_Polynomials.lead_coeff p = (0::'a)) = (p = 0)
[PROOF STEP]
by (cases "p = 0") auto


[STATEMENT]
lemma lookup_monom_of_set:
  "Poly_Mapping.lookup (monom_of_set X) i = (if finite X \<and> i \<in> X then 1 else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup (monom_of_set X) i = (if finite X \<and> i \<in> X then 1 else 0)
[PROOF STEP]
by transfer auto


[STATEMENT]
lemma lookup_monom_of_set_1 [simp]:
        "finite X \<Longrightarrow> i \<in> X \<Longrightarrow> Poly_Mapping.lookup (monom_of_set X) i = 1"
  and lookup_monom_of_set_0 [simp]:
        "i \<notin> X \<Longrightarrow> Poly_Mapping.lookup (monom_of_set X) i = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>finite X; i \<in> X\<rbrakk> \<Longrightarrow> lookup (monom_of_set X) i = 1) &&& (i \<notin> X \<Longrightarrow> lookup (monom_of_set X) i = 0)
[PROOF STEP]
by (simp_all add: lookup_monom_of_set)


[STATEMENT]
lemma keys_monom_of_set: "keys (monom_of_set X) = (if finite X then X else {})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. keys (monom_of_set X) = (if finite X then X else {})
[PROOF STEP]
by transfer auto


[STATEMENT]
lemma keys_monom_of_set_finite [simp]: "finite X \<Longrightarrow> keys (monom_of_set X) = X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite X \<Longrightarrow> keys (monom_of_set X) = X
[PROOF STEP]
by (simp add: keys_monom_of_set)


[STATEMENT]
lemma monom_of_set_eq_iff [simp]: "finite X \<Longrightarrow> finite Y \<Longrightarrow> monom_of_set X = monom_of_set Y \<longleftrightarrow> X = Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite X; finite Y\<rbrakk> \<Longrightarrow> (monom_of_set X = monom_of_set Y) = (X = Y)
[PROOF STEP]
by transfer (auto simp: fun_eq_iff)


[STATEMENT]
lemma monom_of_set_empty [simp]: "monom_of_set {} = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monom_of_set {} = 0
[PROOF STEP]
by transfer auto


[STATEMENT]
lemma monom_of_set_eq_zero_iff [simp]: "monom_of_set X = 0 \<longleftrightarrow> infinite X \<or> X = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (monom_of_set X = 0) = (infinite X \<or> X = {})
[PROOF STEP]
by transfer (auto simp: fun_eq_iff)


[STATEMENT]
lemma zero_eq_monom_of_set_iff [simp]: "0 = monom_of_set X \<longleftrightarrow> infinite X \<or> X = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0 = monom_of_set X) = (infinite X \<or> X = {})
[PROOF STEP]
by transfer (auto simp: fun_eq_iff)


[STATEMENT]
lemma keys_permutep: "bij f \<Longrightarrow> keys (permutep f m) = f -` keys m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij f \<Longrightarrow> keys (permutep f m) = f -` keys m
[PROOF STEP]
by transfer auto


[STATEMENT]
lemma permutep_id'' [simp]: "permutep id = id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. permutep id = id
[PROOF STEP]
by transfer' (auto simp: fun_eq_iff)


[STATEMENT]
lemma permutep_id''' [simp]: "permutep (\<lambda>x. x) = id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. permutep (\<lambda>x. x) = id
[PROOF STEP]
by transfer' (auto simp: fun_eq_iff)


[STATEMENT]
lemma permutep_0 [simp]: "permutep f 0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. permutep f 0 = 0
[PROOF STEP]
by transfer auto


[STATEMENT]
lemma permutep_single:
  "bij f \<Longrightarrow> permutep f (Poly_Mapping.single a b) = Poly_Mapping.single (inv_into UNIV f a) b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij f \<Longrightarrow> permutep f (Poly_Mapping.single a b) = Poly_Mapping.single (inv f a) b
[PROOF STEP]
by transfer (auto simp: fun_eq_iff when_def inv_f_f surj_f_inv_f bij_is_inj bij_is_surj)


[STATEMENT]
lemma mpoly_map_vars_id [simp]: "mpoly_map_vars id = id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mpoly_map_vars id = id
[PROOF STEP]
by transfer auto


[STATEMENT]
lemma mpoly_map_vars_id' [simp]: "mpoly_map_vars (\<lambda>x. x) = id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mpoly_map_vars (\<lambda>x. x) = id
[PROOF STEP]
by transfer auto


[STATEMENT]
lemma lookup_permutep:
  "Poly_Mapping.lookup (permutep f m) x = (if bij f then Poly_Mapping.lookup m (f x) else Poly_Mapping.lookup m x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup (permutep f m) x = (if bij f then lookup m (f x) else lookup m x)
[PROOF STEP]
by transfer auto


[STATEMENT]
lemma inj_permutep [intro]: "inj (permutep (f :: 'a \<Rightarrow> 'a) :: _ \<Rightarrow> 'a \<Rightarrow>\<^sub>0 'b :: zero)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj (permutep f)
[PROOF STEP]
unfolding inj_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x y. permutep f x = permutep f y \<longrightarrow> x = y
[PROOF STEP]
proof (transfer, safe)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f x y. \<lbrakk>finite {xa. x xa \<noteq> (0::'b)}; finite {x. y x \<noteq> (0::'b)}; (if bij f then x \<circ> f else x) = (if bij f then y \<circ> f else y)\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
fix f :: "'a \<Rightarrow> 'a" and x y :: "'a \<Rightarrow> 'b"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f x y. \<lbrakk>finite {xa. x xa \<noteq> (0::'b)}; finite {x. y x \<noteq> (0::'b)}; (if bij f then x \<circ> f else x) = (if bij f then y \<circ> f else y)\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
assume eq: "(if bij f then x \<circ> f else x) = (if bij f then y \<circ> f else y)"
[PROOF STATE]
proof (state)
this:
(if bij f then x \<circ> f else x) = (if bij f then y \<circ> f else y)

goal (1 subgoal):
 1. \<And>f x y. \<lbrakk>finite {xa. x xa \<noteq> (0::'b)}; finite {x. y x \<noteq> (0::'b)}; (if bij f then x \<circ> f else x) = (if bij f then y \<circ> f else y)\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
show "x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = y
[PROOF STEP]
proof (cases "bij f")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. bij f \<Longrightarrow> x = y
 2. \<not> bij f \<Longrightarrow> x = y
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
bij f

goal (2 subgoals):
 1. bij f \<Longrightarrow> x = y
 2. \<not> bij f \<Longrightarrow> x = y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = y
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. x xa = y xa
[PROOF STEP]
fix t :: 'a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. x xa = y xa
[PROOF STEP]
from \<open>bij f\<close>
[PROOF STATE]
proof (chain)
picking this:
bij f
[PROOF STEP]
obtain s where "t = f s"
[PROOF STATE]
proof (prove)
using this:
bij f

goal (1 subgoal):
 1. (\<And>s. t = f s \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto dest!: bij_is_surj)
[PROOF STATE]
proof (state)
this:
t = f s

goal (1 subgoal):
 1. \<And>xa. x xa = y xa
[PROOF STEP]
with eq and True
[PROOF STATE]
proof (chain)
picking this:
(if bij f then x \<circ> f else x) = (if bij f then y \<circ> f else y)
bij f
t = f s
[PROOF STEP]
show "x t = y t"
[PROOF STATE]
proof (prove)
using this:
(if bij f then x \<circ> f else x) = (if bij f then y \<circ> f else y)
bij f
t = f s

goal (1 subgoal):
 1. x t = y t
[PROOF STEP]
by (auto simp: fun_eq_iff)
[PROOF STATE]
proof (state)
this:
x t = y t

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x = y

goal (1 subgoal):
 1. \<not> bij f \<Longrightarrow> x = y
[PROOF STEP]
qed (use eq in auto)
[PROOF STATE]
proof (state)
this:
x = y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma surj_permutep [intro]: "surj (permutep (f :: 'a \<Rightarrow> 'a) :: _ \<Rightarrow> 'a \<Rightarrow>\<^sub>0 'b :: zero)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. surj (permutep f)
[PROOF STEP]
unfolding surj_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>y. \<exists>x. y = permutep f x
[PROOF STEP]
proof (transfer, safe)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f y. finite {x. y x \<noteq> (0::'b)} \<Longrightarrow> \<exists>x\<in>{f. finite {x. f x \<noteq> (0::'b)}}. y = (if bij f then x \<circ> f else x)
[PROOF STEP]
fix f :: "'a \<Rightarrow> 'a" and y :: "'a \<Rightarrow> 'b"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f y. finite {x. y x \<noteq> (0::'b)} \<Longrightarrow> \<exists>x\<in>{f. finite {x. f x \<noteq> (0::'b)}}. y = (if bij f then x \<circ> f else x)
[PROOF STEP]
assume fin: "finite {t. y t \<noteq> 0}"
[PROOF STATE]
proof (state)
this:
finite {t. y t \<noteq> (0::'b)}

goal (1 subgoal):
 1. \<And>f y. finite {x. y x \<noteq> (0::'b)} \<Longrightarrow> \<exists>x\<in>{f. finite {x. f x \<noteq> (0::'b)}}. y = (if bij f then x \<circ> f else x)
[PROOF STEP]
show "\<exists>x\<in>{f. finite {x. f x \<noteq> 0}}. y = (if bij f then x \<circ> f else x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x\<in>{f. finite {x. f x \<noteq> (0::'b)}}. y = (if bij f then x \<circ> f else x)
[PROOF STEP]
proof (cases "bij f")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. bij f \<Longrightarrow> \<exists>x\<in>{f. finite {x. f x \<noteq> (0::'b)}}. y = (if bij f then x \<circ> f else x)
 2. \<not> bij f \<Longrightarrow> \<exists>x\<in>{f. finite {x. f x \<noteq> (0::'b)}}. y = (if bij f then x \<circ> f else x)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
bij f

goal (2 subgoals):
 1. bij f \<Longrightarrow> \<exists>x\<in>{f. finite {x. f x \<noteq> (0::'b)}}. y = (if bij f then x \<circ> f else x)
 2. \<not> bij f \<Longrightarrow> \<exists>x\<in>{f. finite {x. f x \<noteq> (0::'b)}}. y = (if bij f then x \<circ> f else x)
[PROOF STEP]
with fin
[PROOF STATE]
proof (chain)
picking this:
finite {t. y t \<noteq> (0::'b)}
bij f
[PROOF STEP]
have "finite (the_inv f -` {t. y t \<noteq> 0})"
[PROOF STATE]
proof (prove)
using this:
finite {t. y t \<noteq> (0::'b)}
bij f

goal (1 subgoal):
 1. finite (the_inv f -` {t. y t \<noteq> (0::'b)})
[PROOF STEP]
by (intro finite_vimageI) (auto simp: bij_is_inj bij_betw_the_inv_into)
[PROOF STATE]
proof (state)
this:
finite (the_inv f -` {t. y t \<noteq> (0::'b)})

goal (2 subgoals):
 1. bij f \<Longrightarrow> \<exists>x\<in>{f. finite {x. f x \<noteq> (0::'b)}}. y = (if bij f then x \<circ> f else x)
 2. \<not> bij f \<Longrightarrow> \<exists>x\<in>{f. finite {x. f x \<noteq> (0::'b)}}. y = (if bij f then x \<circ> f else x)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite (the_inv f -` {t. y t \<noteq> (0::'b)})

goal (2 subgoals):
 1. bij f \<Longrightarrow> \<exists>x\<in>{f. finite {x. f x \<noteq> (0::'b)}}. y = (if bij f then x \<circ> f else x)
 2. \<not> bij f \<Longrightarrow> \<exists>x\<in>{f. finite {x. f x \<noteq> (0::'b)}}. y = (if bij f then x \<circ> f else x)
[PROOF STEP]
have "y \<circ> the_inv f \<circ> f = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<circ> the_inv f \<circ> f = y
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
bij f

goal (1 subgoal):
 1. y \<circ> the_inv f \<circ> f = y
[PROOF STEP]
by (simp add: fun_eq_iff the_inv_f_f bij_is_inj)
[PROOF STATE]
proof (state)
this:
y \<circ> the_inv f \<circ> f = y

goal (2 subgoals):
 1. bij f \<Longrightarrow> \<exists>x\<in>{f. finite {x. f x \<noteq> (0::'b)}}. y = (if bij f then x \<circ> f else x)
 2. \<not> bij f \<Longrightarrow> \<exists>x\<in>{f. finite {x. f x \<noteq> (0::'b)}}. y = (if bij f then x \<circ> f else x)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
finite (the_inv f -` {t. y t \<noteq> (0::'b)})
y \<circ> the_inv f \<circ> f = y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite (the_inv f -` {t. y t \<noteq> (0::'b)})
y \<circ> the_inv f \<circ> f = y

goal (1 subgoal):
 1. \<exists>x\<in>{f. finite {x. f x \<noteq> (0::'b)}}. y = (if bij f then x \<circ> f else x)
[PROOF STEP]
by (intro bexI[of _ "y \<circ> the_inv f"]) (auto simp: True)
[PROOF STATE]
proof (state)
this:
\<exists>x\<in>{f. finite {x. f x \<noteq> (0::'b)}}. y = (if bij f then x \<circ> f else x)

goal (1 subgoal):
 1. \<not> bij f \<Longrightarrow> \<exists>x\<in>{f. finite {x. f x \<noteq> (0::'b)}}. y = (if bij f then x \<circ> f else x)
[PROOF STEP]
qed (use fin in auto)
[PROOF STATE]
proof (state)
this:
\<exists>x\<in>{f. finite {x. f x \<noteq> (0::'b)}}. y = (if bij f then x \<circ> f else x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bij_permutep [intro]: "bij (permutep f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij (permutep f)
[PROOF STEP]
using inj_permutep[of f] surj_permutep[of f]
[PROOF STATE]
proof (prove)
using this:
inj (permutep f)
surj (permutep f)

goal (1 subgoal):
 1. bij (permutep f)
[PROOF STEP]
by (simp add: bij_def)


[STATEMENT]
lemma mpoly_map_vars_map_mpoly:
  "mpoly_map_vars f (map_mpoly g p) = map_mpoly g (mpoly_map_vars f p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mpoly_map_vars f (map_mpoly g p) = map_mpoly g (mpoly_map_vars f p)
[PROOF STEP]
by (transfer', transfer') (auto simp: fun_eq_iff)


[STATEMENT]
lemma coeff_mpoly_map_vars:
  fixes f :: "nat \<Rightarrow> nat" and p :: "'a :: zero mpoly"
  assumes "bij f"
  shows   "MPoly_Type.coeff (mpoly_map_vars f p) mon =
             MPoly_Type.coeff p (permutep f mon)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MPoly_Type.coeff (mpoly_map_vars f p) mon = MPoly_Type.coeff p (permutep f mon)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
bij f

goal (1 subgoal):
 1. MPoly_Type.coeff (mpoly_map_vars f p) mon = MPoly_Type.coeff p (permutep f mon)
[PROOF STEP]
by transfer' (simp add: lookup_permutep bij_permutep)


[STATEMENT]
lemma permutep_monom_of_set:
  assumes "bij f"
  shows   "permutep f (monom_of_set A) = monom_of_set (f -` A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. permutep f (monom_of_set A) = monom_of_set (f -` A)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
bij f

goal (1 subgoal):
 1. permutep f (monom_of_set A) = monom_of_set (f -` A)
[PROOF STEP]
by transfer (auto simp: fun_eq_iff bij_is_inj finite_vimage_iff)


[STATEMENT]
lemma permutep_comp: "bij f \<Longrightarrow> bij g \<Longrightarrow> permutep (f \<circ> g) = permutep g \<circ> permutep f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bij f; bij g\<rbrakk> \<Longrightarrow> permutep (f \<circ> g) = permutep g \<circ> permutep f
[PROOF STEP]
by transfer' (auto simp: fun_eq_iff bij_comp)


[STATEMENT]
lemma permutep_comp': "bij f \<Longrightarrow> bij g \<Longrightarrow> permutep (f \<circ> g) mon = permutep g (permutep f mon)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bij f; bij g\<rbrakk> \<Longrightarrow> permutep (f \<circ> g) mon = permutep g (permutep f mon)
[PROOF STEP]
by transfer (auto simp: fun_eq_iff bij_comp)


[STATEMENT]
lemma mpoly_map_vars_comp:
  "bij f \<Longrightarrow> bij g \<Longrightarrow> mpoly_map_vars f (mpoly_map_vars g p) = mpoly_map_vars (f \<circ> g) p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bij f; bij g\<rbrakk> \<Longrightarrow> mpoly_map_vars f (mpoly_map_vars g p) = mpoly_map_vars (f \<circ> g) p
[PROOF STEP]
by transfer (auto simp: bij_permutep permutep_comp)


[STATEMENT]
lemma permutep_id [simp]: "permutep id mon = mon"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. permutep id mon = mon
[PROOF STEP]
by transfer auto


[STATEMENT]
lemma permutep_id' [simp]: "permutep (\<lambda>x. x) mon = mon"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. permutep (\<lambda>x. x) mon = mon
[PROOF STEP]
by transfer auto


[STATEMENT]
lemma inv_permutep [simp]:
  fixes f :: "'a \<Rightarrow> 'a"
  assumes "bij f"
  shows   "inv_into UNIV (permutep f) = permutep (inv_into UNIV f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv (permutep f) = permutep (inv f)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. inv (permutep f) x = permutep (inv f) x
[PROOF STEP]
fix m :: "'a \<Rightarrow>\<^sub>0 'b"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. inv (permutep f) x = permutep (inv f) x
[PROOF STEP]
show "inv_into UNIV (permutep f) m = permutep (inv_into UNIV f) m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv (permutep f) m = permutep (inv f) m
[PROOF STEP]
using permutep_comp'[of "inv_into UNIV f" f m] assms inj_iff[of f]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>bij (inv f); bij f\<rbrakk> \<Longrightarrow> permutep (inv f \<circ> f) m = permutep f (permutep (inv f) m)
bij f
inj f = (inv f \<circ> f = id)

goal (1 subgoal):
 1. inv (permutep f) m = permutep (inv f) m
[PROOF STEP]
by (intro inv_f_eq) (auto simp: bij_imp_bij_inv bij_is_inj)
[PROOF STATE]
proof (state)
this:
inv (permutep f) m = permutep (inv f) m

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mpoly_map_vars_monom:
  "bij f \<Longrightarrow> mpoly_map_vars f (monom m c) = monom (permutep (inv_into UNIV f) m) c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij f \<Longrightarrow> mpoly_map_vars f (MPoly_Type.monom m c) = MPoly_Type.monom (permutep (inv f) m) c
[PROOF STEP]
by transfer' (simp add: permutep_single bij_permutep)