[STATEMENT]
lemma symmetric_sym_mpoly [intro]:
  assumes "A \<subseteq> B"
  shows   "symmetric_mpoly A (sym_mpoly B k :: 'a :: zero_neq_one mpoly)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. symmetric_mpoly A (sym_mpoly B k)
[PROOF STEP]
unfolding symmetric_mpoly_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<pi>. \<pi> permutes A \<longrightarrow> mpoly_map_vars \<pi> (sym_mpoly B k) = sym_mpoly B k
[PROOF STEP]
proof (safe intro!: mpoly_eqI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<pi> mon. \<pi> permutes A \<Longrightarrow> MPoly_Type.coeff (mpoly_map_vars \<pi> (sym_mpoly B k)) mon = MPoly_Type.coeff (sym_mpoly B k) mon
[PROOF STEP]
fix \<pi> and mon :: "nat \<Rightarrow>\<^sub>0 nat"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<pi> mon. \<pi> permutes A \<Longrightarrow> MPoly_Type.coeff (mpoly_map_vars \<pi> (sym_mpoly B k)) mon = MPoly_Type.coeff (sym_mpoly B k) mon
[PROOF STEP]
assume \<pi>: "\<pi> permutes A"
[PROOF STATE]
proof (state)
this:
\<pi> permutes A

goal (1 subgoal):
 1. \<And>\<pi> mon. \<pi> permutes A \<Longrightarrow> MPoly_Type.coeff (mpoly_map_vars \<pi> (sym_mpoly B k)) mon = MPoly_Type.coeff (sym_mpoly B k) mon
[PROOF STEP]
from \<pi>
[PROOF STATE]
proof (chain)
picking this:
\<pi> permutes A
[PROOF STEP]
have \<pi>': "\<pi> permutes B"
[PROOF STATE]
proof (prove)
using this:
\<pi> permutes A

goal (1 subgoal):
 1. \<pi> permutes B
[PROOF STEP]
by (rule permutes_subset) fact
[PROOF STATE]
proof (state)
this:
\<pi> permutes B

goal (1 subgoal):
 1. \<And>\<pi> mon. \<pi> permutes A \<Longrightarrow> MPoly_Type.coeff (mpoly_map_vars \<pi> (sym_mpoly B k)) mon = MPoly_Type.coeff (sym_mpoly B k) mon
[PROOF STEP]
from \<pi>
[PROOF STATE]
proof (chain)
picking this:
\<pi> permutes A
[PROOF STEP]
have "MPoly_Type.coeff (mpoly_map_vars \<pi> (sym_mpoly B k :: 'a mpoly)) mon =
                 MPoly_Type.coeff (sym_mpoly B k :: 'a mpoly) (permutep \<pi> mon)"
[PROOF STATE]
proof (prove)
using this:
\<pi> permutes A

goal (1 subgoal):
 1. MPoly_Type.coeff (mpoly_map_vars \<pi> (sym_mpoly B k)) mon = MPoly_Type.coeff (sym_mpoly B k) (permutep \<pi> mon)
[PROOF STEP]
by (simp add: coeff_mpoly_map_vars permutes_bij)
[PROOF STATE]
proof (state)
this:
MPoly_Type.coeff (mpoly_map_vars \<pi> (sym_mpoly B k)) mon = MPoly_Type.coeff (sym_mpoly B k) (permutep \<pi> mon)

goal (1 subgoal):
 1. \<And>\<pi> mon. \<pi> permutes A \<Longrightarrow> MPoly_Type.coeff (mpoly_map_vars \<pi> (sym_mpoly B k)) mon = MPoly_Type.coeff (sym_mpoly B k) mon
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
MPoly_Type.coeff (mpoly_map_vars \<pi> (sym_mpoly B k)) mon = MPoly_Type.coeff (sym_mpoly B k) (permutep \<pi> mon)

goal (1 subgoal):
 1. \<And>\<pi> mon. \<pi> permutes A \<Longrightarrow> MPoly_Type.coeff (mpoly_map_vars \<pi> (sym_mpoly B k)) mon = MPoly_Type.coeff (sym_mpoly B k) mon
[PROOF STEP]
have "\<dots> = 1 \<longleftrightarrow> MPoly_Type.coeff (sym_mpoly B k :: 'a mpoly) mon = 1"
    (is "?lhs = 1 \<longleftrightarrow> ?rhs = 1")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (MPoly_Type.coeff (sym_mpoly B k) (permutep \<pi> mon) = (1::'a)) = (MPoly_Type.coeff (sym_mpoly B k) mon = (1::'a))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. MPoly_Type.coeff (sym_mpoly B k) (permutep \<pi> mon) = (1::'a) \<Longrightarrow> MPoly_Type.coeff (sym_mpoly B k) mon = (1::'a)
 2. MPoly_Type.coeff (sym_mpoly B k) mon = (1::'a) \<Longrightarrow> MPoly_Type.coeff (sym_mpoly B k) (permutep \<pi> mon) = (1::'a)
[PROOF STEP]
assume "?rhs = 1"
[PROOF STATE]
proof (state)
this:
MPoly_Type.coeff (sym_mpoly B k) mon = (1::'a)

goal (2 subgoals):
 1. MPoly_Type.coeff (sym_mpoly B k) (permutep \<pi> mon) = (1::'a) \<Longrightarrow> MPoly_Type.coeff (sym_mpoly B k) mon = (1::'a)
 2. MPoly_Type.coeff (sym_mpoly B k) mon = (1::'a) \<Longrightarrow> MPoly_Type.coeff (sym_mpoly B k) (permutep \<pi> mon) = (1::'a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
MPoly_Type.coeff (sym_mpoly B k) mon = (1::'a)
[PROOF STEP]
obtain Y where "finite B" and Y: "Y \<subseteq> B" "card Y = k" "mon = monom_of_set Y"
[PROOF STATE]
proof (prove)
using this:
MPoly_Type.coeff (sym_mpoly B k) mon = (1::'a)

goal (1 subgoal):
 1. (\<And>Y. \<lbrakk>finite B; Y \<subseteq> B; card Y = k; mon = monom_of_set Y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: coeff_sym_mpoly split: if_splits)
[PROOF STATE]
proof (state)
this:
finite B
Y \<subseteq> B
card Y = k
mon = monom_of_set Y

goal (2 subgoals):
 1. MPoly_Type.coeff (sym_mpoly B k) (permutep \<pi> mon) = (1::'a) \<Longrightarrow> MPoly_Type.coeff (sym_mpoly B k) mon = (1::'a)
 2. MPoly_Type.coeff (sym_mpoly B k) mon = (1::'a) \<Longrightarrow> MPoly_Type.coeff (sym_mpoly B k) (permutep \<pi> mon) = (1::'a)
[PROOF STEP]
with \<pi>'
[PROOF STATE]
proof (chain)
picking this:
\<pi> permutes B
finite B
Y \<subseteq> B
card Y = k
mon = monom_of_set Y
[PROOF STEP]
have "\<pi> -` Y \<subseteq> B" "card (\<pi> -` Y) = k" "permutep \<pi> mon = monom_of_set (\<pi> -` Y)"
[PROOF STATE]
proof (prove)
using this:
\<pi> permutes B
finite B
Y \<subseteq> B
card Y = k
mon = monom_of_set Y

goal (1 subgoal):
 1. \<pi> -` Y \<subseteq> B &&& card (\<pi> -` Y) = k &&& permutep \<pi> mon = monom_of_set (\<pi> -` Y)
[PROOF STEP]
by (auto simp: permutes_in_image card_vimage_inj permutep_monom_of_set
                     permutes_bij permutes_inj permutes_surj)
[PROOF STATE]
proof (state)
this:
\<pi> -` Y \<subseteq> B
card (\<pi> -` Y) = k
permutep \<pi> mon = monom_of_set (\<pi> -` Y)

goal (2 subgoals):
 1. MPoly_Type.coeff (sym_mpoly B k) (permutep \<pi> mon) = (1::'a) \<Longrightarrow> MPoly_Type.coeff (sym_mpoly B k) mon = (1::'a)
 2. MPoly_Type.coeff (sym_mpoly B k) mon = (1::'a) \<Longrightarrow> MPoly_Type.coeff (sym_mpoly B k) (permutep \<pi> mon) = (1::'a)
[PROOF STEP]
thus "?lhs = 1"
[PROOF STATE]
proof (prove)
using this:
\<pi> -` Y \<subseteq> B
card (\<pi> -` Y) = k
permutep \<pi> mon = monom_of_set (\<pi> -` Y)

goal (1 subgoal):
 1. MPoly_Type.coeff (sym_mpoly B k) (permutep \<pi> mon) = (1::'a)
[PROOF STEP]
using \<open>finite B\<close>
[PROOF STATE]
proof (prove)
using this:
\<pi> -` Y \<subseteq> B
card (\<pi> -` Y) = k
permutep \<pi> mon = monom_of_set (\<pi> -` Y)
finite B

goal (1 subgoal):
 1. MPoly_Type.coeff (sym_mpoly B k) (permutep \<pi> mon) = (1::'a)
[PROOF STEP]
by (auto simp: coeff_sym_mpoly)
[PROOF STATE]
proof (state)
this:
MPoly_Type.coeff (sym_mpoly B k) (permutep \<pi> mon) = (1::'a)

goal (1 subgoal):
 1. MPoly_Type.coeff (sym_mpoly B k) (permutep \<pi> mon) = (1::'a) \<Longrightarrow> MPoly_Type.coeff (sym_mpoly B k) mon = (1::'a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. MPoly_Type.coeff (sym_mpoly B k) (permutep \<pi> mon) = (1::'a) \<Longrightarrow> MPoly_Type.coeff (sym_mpoly B k) mon = (1::'a)
[PROOF STEP]
assume "?lhs = 1"
[PROOF STATE]
proof (state)
this:
MPoly_Type.coeff (sym_mpoly B k) (permutep \<pi> mon) = (1::'a)

goal (1 subgoal):
 1. MPoly_Type.coeff (sym_mpoly B k) (permutep \<pi> mon) = (1::'a) \<Longrightarrow> MPoly_Type.coeff (sym_mpoly B k) mon = (1::'a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
MPoly_Type.coeff (sym_mpoly B k) (permutep \<pi> mon) = (1::'a)
[PROOF STEP]
obtain Y where "finite B" and Y: "Y \<subseteq> B" "card Y = k" "permutep \<pi> mon = monom_of_set Y"
[PROOF STATE]
proof (prove)
using this:
MPoly_Type.coeff (sym_mpoly B k) (permutep \<pi> mon) = (1::'a)

goal (1 subgoal):
 1. (\<And>Y. \<lbrakk>finite B; Y \<subseteq> B; card Y = k; permutep \<pi> mon = monom_of_set Y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: coeff_sym_mpoly split: if_splits)
[PROOF STATE]
proof (state)
this:
finite B
Y \<subseteq> B
card Y = k
permutep \<pi> mon = monom_of_set Y

goal (1 subgoal):
 1. MPoly_Type.coeff (sym_mpoly B k) (permutep \<pi> mon) = (1::'a) \<Longrightarrow> MPoly_Type.coeff (sym_mpoly B k) mon = (1::'a)
[PROOF STEP]
from Y(1)
[PROOF STATE]
proof (chain)
picking this:
Y \<subseteq> B
[PROOF STEP]
have "inj_on \<pi> Y"
[PROOF STATE]
proof (prove)
using this:
Y \<subseteq> B

goal (1 subgoal):
 1. inj_on \<pi> Y
[PROOF STEP]
using inj_on_subset[of \<pi> UNIV Y] \<pi>'
[PROOF STATE]
proof (prove)
using this:
Y \<subseteq> B
\<lbrakk>inj \<pi>; Y \<subseteq> UNIV\<rbrakk> \<Longrightarrow> inj_on \<pi> Y
\<pi> permutes B

goal (1 subgoal):
 1. inj_on \<pi> Y
[PROOF STEP]
by (auto simp: permutes_inj)
[PROOF STATE]
proof (state)
this:
inj_on \<pi> Y

goal (1 subgoal):
 1. MPoly_Type.coeff (sym_mpoly B k) (permutep \<pi> mon) = (1::'a) \<Longrightarrow> MPoly_Type.coeff (sym_mpoly B k) mon = (1::'a)
[PROOF STEP]
with Y \<pi>'
[PROOF STATE]
proof (chain)
picking this:
Y \<subseteq> B
card Y = k
permutep \<pi> mon = monom_of_set Y
\<pi> permutes B
inj_on \<pi> Y
[PROOF STEP]
have "\<pi> ` Y \<subseteq> B" "card (\<pi> ` Y) = k" "mon = monom_of_set (\<pi> ` Y)"
[PROOF STATE]
proof (prove)
using this:
Y \<subseteq> B
card Y = k
permutep \<pi> mon = monom_of_set Y
\<pi> permutes B
inj_on \<pi> Y

goal (1 subgoal):
 1. \<pi> ` Y \<subseteq> B &&& card (\<pi> ` Y) = k &&& mon = monom_of_set (\<pi> ` Y)
[PROOF STEP]
by (auto simp: permutes_in_image card_image permutep_monom_of_set
               permutes_bij permutes_inj permutes_surj)
[PROOF STATE]
proof (state)
this:
\<pi> ` Y \<subseteq> B
card (\<pi> ` Y) = k
mon = monom_of_set (\<pi> ` Y)

goal (1 subgoal):
 1. MPoly_Type.coeff (sym_mpoly B k) (permutep \<pi> mon) = (1::'a) \<Longrightarrow> MPoly_Type.coeff (sym_mpoly B k) mon = (1::'a)
[PROOF STEP]
thus "?rhs = 1"
[PROOF STATE]
proof (prove)
using this:
\<pi> ` Y \<subseteq> B
card (\<pi> ` Y) = k
mon = monom_of_set (\<pi> ` Y)

goal (1 subgoal):
 1. MPoly_Type.coeff (sym_mpoly B k) mon = (1::'a)
[PROOF STEP]
using \<open>finite B\<close>
[PROOF STATE]
proof (prove)
using this:
\<pi> ` Y \<subseteq> B
card (\<pi> ` Y) = k
mon = monom_of_set (\<pi> ` Y)
finite B

goal (1 subgoal):
 1. MPoly_Type.coeff (sym_mpoly B k) mon = (1::'a)
[PROOF STEP]
by (auto simp: coeff_sym_mpoly)
[PROOF STATE]
proof (state)
this:
MPoly_Type.coeff (sym_mpoly B k) mon = (1::'a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(MPoly_Type.coeff (sym_mpoly B k) (permutep \<pi> mon) = (1::'a)) = (MPoly_Type.coeff (sym_mpoly B k) mon = (1::'a))

goal (1 subgoal):
 1. \<And>\<pi> mon. \<pi> permutes A \<Longrightarrow> MPoly_Type.coeff (mpoly_map_vars \<pi> (sym_mpoly B k)) mon = MPoly_Type.coeff (sym_mpoly B k) mon
[PROOF STEP]
hence "?lhs = ?rhs"
[PROOF STATE]
proof (prove)
using this:
(MPoly_Type.coeff (sym_mpoly B k) (permutep \<pi> mon) = (1::'a)) = (MPoly_Type.coeff (sym_mpoly B k) mon = (1::'a))

goal (1 subgoal):
 1. MPoly_Type.coeff (sym_mpoly B k) (permutep \<pi> mon) = MPoly_Type.coeff (sym_mpoly B k) mon
[PROOF STEP]
by (auto simp: coeff_sym_mpoly split: if_splits)
[PROOF STATE]
proof (state)
this:
MPoly_Type.coeff (sym_mpoly B k) (permutep \<pi> mon) = MPoly_Type.coeff (sym_mpoly B k) mon

goal (1 subgoal):
 1. \<And>\<pi> mon. \<pi> permutes A \<Longrightarrow> MPoly_Type.coeff (mpoly_map_vars \<pi> (sym_mpoly B k)) mon = MPoly_Type.coeff (sym_mpoly B k) mon
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
MPoly_Type.coeff (mpoly_map_vars \<pi> (sym_mpoly B k)) mon = MPoly_Type.coeff (sym_mpoly B k) mon
[PROOF STEP]
show "MPoly_Type.coeff (mpoly_map_vars \<pi> (sym_mpoly B k :: 'a mpoly)) mon =
                  MPoly_Type.coeff (sym_mpoly B k :: 'a mpoly) mon"
[PROOF STATE]
proof (prove)
using this:
MPoly_Type.coeff (mpoly_map_vars \<pi> (sym_mpoly B k)) mon = MPoly_Type.coeff (sym_mpoly B k) mon

goal (1 subgoal):
 1. MPoly_Type.coeff (mpoly_map_vars \<pi> (sym_mpoly B k)) mon = MPoly_Type.coeff (sym_mpoly B k) mon
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
MPoly_Type.coeff (mpoly_map_vars \<pi> (sym_mpoly B k)) mon = MPoly_Type.coeff (sym_mpoly B k) mon

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma insertion_sym_mpoly:
  assumes "finite X"
  shows   "insertion f (sym_mpoly X k) = (\<Sum>Y | Y \<subseteq> X \<and> card Y = k. prod f Y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion f (sym_mpoly X k) = (\<Sum>Y | Y \<subseteq> X \<and> card Y = k. prod f Y)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite X

goal (1 subgoal):
 1. insertion f (sym_mpoly X k) = (\<Sum>Y | Y \<subseteq> X \<and> card Y = k. prod f Y)
[PROOF STEP]
proof (transfer, transfer)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>X f k Xa. \<lbrakk>finite X; finite Xa\<rbrakk> \<Longrightarrow> insertion_fun f (\<lambda>mon. if finite X \<and> (\<exists>Y\<subseteq>X. card Y = k \<and> mon = monom_of_set Y) then 1::'a else (0::'a)) = sum (prod f) {Y. Y \<subseteq> X \<and> card Y = k}
[PROOF STEP]
fix f :: "nat \<Rightarrow> 'a" and k :: nat and X :: "nat set"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>X f k Xa. \<lbrakk>finite X; finite Xa\<rbrakk> \<Longrightarrow> insertion_fun f (\<lambda>mon. if finite X \<and> (\<exists>Y\<subseteq>X. card Y = k \<and> mon = monom_of_set Y) then 1::'a else (0::'a)) = sum (prod f) {Y. Y \<subseteq> X \<and> card Y = k}
[PROOF STEP]
assume X: "finite X"
[PROOF STATE]
proof (state)
this:
finite X

goal (1 subgoal):
 1. \<And>X f k Xa. \<lbrakk>finite X; finite Xa\<rbrakk> \<Longrightarrow> insertion_fun f (\<lambda>mon. if finite X \<and> (\<exists>Y\<subseteq>X. card Y = k \<and> mon = monom_of_set Y) then 1::'a else (0::'a)) = sum (prod f) {Y. Y \<subseteq> X \<and> card Y = k}
[PROOF STEP]
have "insertion_fun f (\<lambda>mon.
            if finite X \<and> (\<exists>Y\<subseteq>X. card Y = k \<and> mon = monom_of_set Y) then 1 else 0) =
        (\<Sum>m. (\<Prod>v. f v ^ poly_mapping.lookup m v) when (\<exists>Y\<subseteq>X. card Y = k \<and> m = monom_of_set Y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion_fun f (\<lambda>mon. if finite X \<and> (\<exists>Y\<subseteq>X. card Y = k \<and> mon = monom_of_set Y) then 1::'a else (0::'a)) = (\<Sum>m. (\<Prod>v. f v ^ lookup m v) when (\<exists>Y\<subseteq>X. card Y = k \<and> m = monom_of_set Y))
[PROOF STEP]
by (auto simp add: insertion_fun_def X when_def intro!: Sum_any.cong)
[PROOF STATE]
proof (state)
this:
insertion_fun f (\<lambda>mon. if finite X \<and> (\<exists>Y\<subseteq>X. card Y = k \<and> mon = monom_of_set Y) then 1::'a else (0::'a)) = (\<Sum>m. (\<Prod>v. f v ^ lookup m v) when (\<exists>Y\<subseteq>X. card Y = k \<and> m = monom_of_set Y))

goal (1 subgoal):
 1. \<And>X f k Xa. \<lbrakk>finite X; finite Xa\<rbrakk> \<Longrightarrow> insertion_fun f (\<lambda>mon. if finite X \<and> (\<exists>Y\<subseteq>X. card Y = k \<and> mon = monom_of_set Y) then 1::'a else (0::'a)) = sum (prod f) {Y. Y \<subseteq> X \<and> card Y = k}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
insertion_fun f (\<lambda>mon. if finite X \<and> (\<exists>Y\<subseteq>X. card Y = k \<and> mon = monom_of_set Y) then 1::'a else (0::'a)) = (\<Sum>m. (\<Prod>v. f v ^ lookup m v) when (\<exists>Y\<subseteq>X. card Y = k \<and> m = monom_of_set Y))

goal (1 subgoal):
 1. \<And>X f k Xa. \<lbrakk>finite X; finite Xa\<rbrakk> \<Longrightarrow> insertion_fun f (\<lambda>mon. if finite X \<and> (\<exists>Y\<subseteq>X. card Y = k \<and> mon = monom_of_set Y) then 1::'a else (0::'a)) = sum (prod f) {Y. Y \<subseteq> X \<and> card Y = k}
[PROOF STEP]
have "\<dots> = (\<Sum>m | \<exists>Y\<in>Pow X. card Y = k \<and> m = monom_of_set Y. (\<Prod>v. f v ^ poly_mapping.lookup m v) when (\<exists>Y\<subseteq>X. card Y = k \<and> m = monom_of_set Y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>m. (\<Prod>v. f v ^ lookup m v) when (\<exists>Y\<subseteq>X. card Y = k \<and> m = monom_of_set Y)) = (\<Sum>m | \<exists>Y\<in>Pow X. card Y = k \<and> m = monom_of_set Y. (\<Prod>v. f v ^ lookup m v) when (\<exists>Y\<subseteq>X. card Y = k \<and> m = monom_of_set Y))
[PROOF STEP]
by (rule Sum_any.expand_superset) (use X in auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>m. (\<Prod>v. f v ^ lookup m v) when (\<exists>Y\<subseteq>X. card Y = k \<and> m = monom_of_set Y)) = (\<Sum>m | \<exists>Y\<in>Pow X. card Y = k \<and> m = monom_of_set Y. (\<Prod>v. f v ^ lookup m v) when (\<exists>Y\<subseteq>X. card Y = k \<and> m = monom_of_set Y))

goal (1 subgoal):
 1. \<And>X f k Xa. \<lbrakk>finite X; finite Xa\<rbrakk> \<Longrightarrow> insertion_fun f (\<lambda>mon. if finite X \<and> (\<exists>Y\<subseteq>X. card Y = k \<and> mon = monom_of_set Y) then 1::'a else (0::'a)) = sum (prod f) {Y. Y \<subseteq> X \<and> card Y = k}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>m. (\<Prod>v. f v ^ lookup m v) when (\<exists>Y\<subseteq>X. card Y = k \<and> m = monom_of_set Y)) = (\<Sum>m | \<exists>Y\<in>Pow X. card Y = k \<and> m = monom_of_set Y. (\<Prod>v. f v ^ lookup m v) when (\<exists>Y\<subseteq>X. card Y = k \<and> m = monom_of_set Y))

goal (1 subgoal):
 1. \<And>X f k Xa. \<lbrakk>finite X; finite Xa\<rbrakk> \<Longrightarrow> insertion_fun f (\<lambda>mon. if finite X \<and> (\<exists>Y\<subseteq>X. card Y = k \<and> mon = monom_of_set Y) then 1::'a else (0::'a)) = sum (prod f) {Y. Y \<subseteq> X \<and> card Y = k}
[PROOF STEP]
have "\<dots> = (\<Sum>m | \<exists>Y\<in>Pow X. card Y = k \<and> m = monom_of_set Y. (\<Prod>v. f v ^ poly_mapping.lookup m v))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>m | \<exists>Y\<in>Pow X. card Y = k \<and> m = monom_of_set Y. (\<Prod>v. f v ^ lookup m v) when (\<exists>Y\<subseteq>X. card Y = k \<and> m = monom_of_set Y)) = (\<Sum>m | \<exists>Y\<in>Pow X. card Y = k \<and> m = monom_of_set Y. \<Prod>v. f v ^ lookup m v)
[PROOF STEP]
by (intro sum.cong) (auto simp: when_def)
[PROOF STATE]
proof (state)
this:
(\<Sum>m | \<exists>Y\<in>Pow X. card Y = k \<and> m = monom_of_set Y. (\<Prod>v. f v ^ lookup m v) when (\<exists>Y\<subseteq>X. card Y = k \<and> m = monom_of_set Y)) = (\<Sum>m | \<exists>Y\<in>Pow X. card Y = k \<and> m = monom_of_set Y. \<Prod>v. f v ^ lookup m v)

goal (1 subgoal):
 1. \<And>X f k Xa. \<lbrakk>finite X; finite Xa\<rbrakk> \<Longrightarrow> insertion_fun f (\<lambda>mon. if finite X \<and> (\<exists>Y\<subseteq>X. card Y = k \<and> mon = monom_of_set Y) then 1::'a else (0::'a)) = sum (prod f) {Y. Y \<subseteq> X \<and> card Y = k}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>m | \<exists>Y\<in>Pow X. card Y = k \<and> m = monom_of_set Y. (\<Prod>v. f v ^ lookup m v) when (\<exists>Y\<subseteq>X. card Y = k \<and> m = monom_of_set Y)) = (\<Sum>m | \<exists>Y\<in>Pow X. card Y = k \<and> m = monom_of_set Y. \<Prod>v. f v ^ lookup m v)

goal (1 subgoal):
 1. \<And>X f k Xa. \<lbrakk>finite X; finite Xa\<rbrakk> \<Longrightarrow> insertion_fun f (\<lambda>mon. if finite X \<and> (\<exists>Y\<subseteq>X. card Y = k \<and> mon = monom_of_set Y) then 1::'a else (0::'a)) = sum (prod f) {Y. Y \<subseteq> X \<and> card Y = k}
[PROOF STEP]
have "\<dots> = (\<Sum>Y | Y \<subseteq> X \<and> card Y = k. (\<Prod>v. f v ^ poly_mapping.lookup (monom_of_set Y) v))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>m | \<exists>Y\<in>Pow X. card Y = k \<and> m = monom_of_set Y. \<Prod>v. f v ^ lookup m v) = (\<Sum>Y | Y \<subseteq> X \<and> card Y = k. \<Prod>v. f v ^ lookup (monom_of_set Y) v)
[PROOF STEP]
by (rule sum.reindex_bij_witness[of _ monom_of_set keys]) (auto simp: finite_subset[OF _ X])
[PROOF STATE]
proof (state)
this:
(\<Sum>m | \<exists>Y\<in>Pow X. card Y = k \<and> m = monom_of_set Y. \<Prod>v. f v ^ lookup m v) = (\<Sum>Y | Y \<subseteq> X \<and> card Y = k. \<Prod>v. f v ^ lookup (monom_of_set Y) v)

goal (1 subgoal):
 1. \<And>X f k Xa. \<lbrakk>finite X; finite Xa\<rbrakk> \<Longrightarrow> insertion_fun f (\<lambda>mon. if finite X \<and> (\<exists>Y\<subseteq>X. card Y = k \<and> mon = monom_of_set Y) then 1::'a else (0::'a)) = sum (prod f) {Y. Y \<subseteq> X \<and> card Y = k}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>m | \<exists>Y\<in>Pow X. card Y = k \<and> m = monom_of_set Y. \<Prod>v. f v ^ lookup m v) = (\<Sum>Y | Y \<subseteq> X \<and> card Y = k. \<Prod>v. f v ^ lookup (monom_of_set Y) v)

goal (1 subgoal):
 1. \<And>X f k Xa. \<lbrakk>finite X; finite Xa\<rbrakk> \<Longrightarrow> insertion_fun f (\<lambda>mon. if finite X \<and> (\<exists>Y\<subseteq>X. card Y = k \<and> mon = monom_of_set Y) then 1::'a else (0::'a)) = sum (prod f) {Y. Y \<subseteq> X \<and> card Y = k}
[PROOF STEP]
have "\<dots> = (\<Sum>Y | Y \<subseteq> X \<and> card Y = k. \<Prod>v\<in>Y. f v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>Y | Y \<subseteq> X \<and> card Y = k. \<Prod>v. f v ^ lookup (monom_of_set Y) v) = (\<Sum>Y | Y \<subseteq> X \<and> card Y = k. prod f Y)
[PROOF STEP]
proof (intro sum.cong when_cong refl, goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {Y. Y \<subseteq> X \<and> card Y = k} \<Longrightarrow> (\<Prod>v. f v ^ lookup (monom_of_set x) v) = prod f x
[PROOF STEP]
case (1 Y)
[PROOF STATE]
proof (state)
this:
Y \<in> {Y. Y \<subseteq> X \<and> card Y = k}

goal (1 subgoal):
 1. \<And>x. x \<in> {Y. Y \<subseteq> X \<and> card Y = k} \<Longrightarrow> (\<Prod>v. f v ^ lookup (monom_of_set x) v) = prod f x
[PROOF STEP]
hence "finite Y"
[PROOF STATE]
proof (prove)
using this:
Y \<in> {Y. Y \<subseteq> X \<and> card Y = k}

goal (1 subgoal):
 1. finite Y
[PROOF STEP]
by (auto dest: finite_subset[OF _ X])
[PROOF STATE]
proof (state)
this:
finite Y

goal (1 subgoal):
 1. \<And>x. x \<in> {Y. Y \<subseteq> X \<and> card Y = k} \<Longrightarrow> (\<Prod>v. f v ^ lookup (monom_of_set x) v) = prod f x
[PROOF STEP]
with 1
[PROOF STATE]
proof (chain)
picking this:
Y \<in> {Y. Y \<subseteq> X \<and> card Y = k}
finite Y
[PROOF STEP]
have "(\<Prod>v. f v ^ poly_mapping.lookup (monom_of_set Y) v) =
                   (\<Prod>v::nat. if v \<in> Y then f v else 1)"
[PROOF STATE]
proof (prove)
using this:
Y \<in> {Y. Y \<subseteq> X \<and> card Y = k}
finite Y

goal (1 subgoal):
 1. (\<Prod>v. f v ^ lookup (monom_of_set Y) v) = (\<Prod>v. if v \<in> Y then f v else (1::'a))
[PROOF STEP]
by (intro Prod_any.cong) (auto simp: lookup_monom_of_set)
[PROOF STATE]
proof (state)
this:
(\<Prod>v. f v ^ lookup (monom_of_set Y) v) = (\<Prod>v. if v \<in> Y then f v else (1::'a))

goal (1 subgoal):
 1. \<And>x. x \<in> {Y. Y \<subseteq> X \<and> card Y = k} \<Longrightarrow> (\<Prod>v. f v ^ lookup (monom_of_set x) v) = prod f x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Prod>v. f v ^ lookup (monom_of_set Y) v) = (\<Prod>v. if v \<in> Y then f v else (1::'a))

goal (1 subgoal):
 1. \<And>x. x \<in> {Y. Y \<subseteq> X \<and> card Y = k} \<Longrightarrow> (\<Prod>v. f v ^ lookup (monom_of_set x) v) = prod f x
[PROOF STEP]
have "\<dots> = (\<Prod>v\<in>Y. f v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>v. if v \<in> Y then f v else (1::'a)) = prod f Y
[PROOF STEP]
by (rule Prod_any.conditionalize [symmetric]) fact+
[PROOF STATE]
proof (state)
this:
(\<Prod>v. if v \<in> Y then f v else (1::'a)) = prod f Y

goal (1 subgoal):
 1. \<And>x. x \<in> {Y. Y \<subseteq> X \<and> card Y = k} \<Longrightarrow> (\<Prod>v. f v ^ lookup (monom_of_set x) v) = prod f x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Prod>v. f v ^ lookup (monom_of_set Y) v) = prod f Y
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(\<Prod>v. f v ^ lookup (monom_of_set Y) v) = prod f Y

goal (1 subgoal):
 1. (\<Prod>v. f v ^ lookup (monom_of_set Y) v) = prod f Y
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<Prod>v. f v ^ lookup (monom_of_set Y) v) = prod f Y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>Y | Y \<subseteq> X \<and> card Y = k. \<Prod>v. f v ^ lookup (monom_of_set Y) v) = (\<Sum>Y | Y \<subseteq> X \<and> card Y = k. prod f Y)

goal (1 subgoal):
 1. \<And>X f k Xa. \<lbrakk>finite X; finite Xa\<rbrakk> \<Longrightarrow> insertion_fun f (\<lambda>mon. if finite X \<and> (\<exists>Y\<subseteq>X. card Y = k \<and> mon = monom_of_set Y) then 1::'a else (0::'a)) = sum (prod f) {Y. Y \<subseteq> X \<and> card Y = k}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
insertion_fun f (\<lambda>mon. if finite X \<and> (\<exists>Y\<subseteq>X. card Y = k \<and> mon = monom_of_set Y) then 1::'a else (0::'a)) = (\<Sum>Y | Y \<subseteq> X \<and> card Y = k. prod f Y)
[PROOF STEP]
show "insertion_fun f
                   (\<lambda>mon. if finite X \<and> (\<exists>Y\<subseteq>X. card Y = k \<and> mon = monom_of_set Y) then 1 else 0) =
                 (\<Sum>Y | Y \<subseteq> X \<and> card Y = k. prod f Y)"
[PROOF STATE]
proof (prove)
using this:
insertion_fun f (\<lambda>mon. if finite X \<and> (\<exists>Y\<subseteq>X. card Y = k \<and> mon = monom_of_set Y) then 1::'a else (0::'a)) = (\<Sum>Y | Y \<subseteq> X \<and> card Y = k. prod f Y)

goal (1 subgoal):
 1. insertion_fun f (\<lambda>mon. if finite X \<and> (\<exists>Y\<subseteq>X. card Y = k \<and> mon = monom_of_set Y) then 1::'a else (0::'a)) = (\<Sum>Y | Y \<subseteq> X \<and> card Y = k. prod f Y)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
insertion_fun f (\<lambda>mon. if finite X \<and> (\<exists>Y\<subseteq>X. card Y = k \<and> mon = monom_of_set Y) then 1::'a else (0::'a)) = (\<Sum>Y | Y \<subseteq> X \<and> card Y = k. prod f Y)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sym_mpoly_nz [simp]:
  assumes "finite A" "k \<le> card A"
  shows   "sym_mpoly A k \<noteq> (0 :: 'a :: zero_neq_one mpoly)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sym_mpoly A k \<noteq> 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sym_mpoly A k \<noteq> 0
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
finite A
k \<le> card A
[PROOF STEP]
obtain B where B: "B \<subseteq> A" "card B = k"
[PROOF STATE]
proof (prove)
using this:
finite A
k \<le> card A

goal (1 subgoal):
 1. (\<And>B. \<lbrakk>B \<subseteq> A; card B = k\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using ex_subset_of_card
[PROOF STATE]
proof (prove)
using this:
finite A
k \<le> card A
\<lbrakk>finite ?A; ?k \<le> card ?A\<rbrakk> \<Longrightarrow> \<exists>B\<subseteq>?A. card B = ?k

goal (1 subgoal):
 1. (\<And>B. \<lbrakk>B \<subseteq> A; card B = k\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
B \<subseteq> A
card B = k

goal (1 subgoal):
 1. sym_mpoly A k \<noteq> 0
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
finite A
k \<le> card A
B \<subseteq> A
card B = k
[PROOF STEP]
have "coeff (sym_mpoly A k :: 'a mpoly) (monom_of_set B) = 1"
[PROOF STATE]
proof (prove)
using this:
finite A
k \<le> card A
B \<subseteq> A
card B = k

goal (1 subgoal):
 1. MPoly_Type.coeff (sym_mpoly A k) (monom_of_set B) = (1::'a)
[PROOF STEP]
by (intro coeff_sym_mpoly_monom_of_set)
[PROOF STATE]
proof (state)
this:
MPoly_Type.coeff (sym_mpoly A k) (monom_of_set B) = (1::'a)

goal (1 subgoal):
 1. sym_mpoly A k \<noteq> 0
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
MPoly_Type.coeff (sym_mpoly A k) (monom_of_set B) = (1::'a)

goal (1 subgoal):
 1. sym_mpoly A k \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sym_mpoly A k \<noteq> 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma coeff_sym_mpoly_0_or_1: "coeff (sym_mpoly A k) m \<in> {0, 1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MPoly_Type.coeff (sym_mpoly A k) m \<in> {0::'a, 1::'a}
[PROOF STEP]
by (transfer, transfer) auto


[STATEMENT]
lemma lead_coeff_sym_mpoly [simp]:
  assumes "finite A" "k \<le> card A"
  shows   "lead_coeff (sym_mpoly A k) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Symmetric_Polynomials.lead_coeff (sym_mpoly A k) = (1::'a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Symmetric_Polynomials.lead_coeff (sym_mpoly A k) = (1::'a)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
finite A
k \<le> card A
[PROOF STEP]
have "lead_coeff (sym_mpoly A k) \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
finite A
k \<le> card A

goal (1 subgoal):
 1. Symmetric_Polynomials.lead_coeff (sym_mpoly A k) \<noteq> (0::'b)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Symmetric_Polynomials.lead_coeff (sym_mpoly A k) \<noteq> (0::?'b1)

goal (1 subgoal):
 1. Symmetric_Polynomials.lead_coeff (sym_mpoly A k) = (1::'a)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
Symmetric_Polynomials.lead_coeff (sym_mpoly A k) \<noteq> (0::?'b1)

goal (1 subgoal):
 1. Symmetric_Polynomials.lead_coeff (sym_mpoly A k) = (1::'a)
[PROOF STEP]
using coeff_sym_mpoly_0_or_1[of A k "lead_monom (sym_mpoly A k)"]
[PROOF STATE]
proof (prove)
using this:
Symmetric_Polynomials.lead_coeff (sym_mpoly A k) \<noteq> (0::?'b1)
MPoly_Type.coeff (sym_mpoly A k) (lead_monom (sym_mpoly A k)) \<in> {0::?'a, 1::?'a}

goal (1 subgoal):
 1. Symmetric_Polynomials.lead_coeff (sym_mpoly A k) = (1::'a)
[PROOF STEP]
unfolding lead_coeff_def
[PROOF STATE]
proof (prove)
using this:
MPoly_Type.coeff (sym_mpoly A k) (lead_monom (sym_mpoly A k)) \<noteq> (0::?'b1)
MPoly_Type.coeff (sym_mpoly A k) (lead_monom (sym_mpoly A k)) \<in> {0::?'a, 1::?'a}

goal (1 subgoal):
 1. MPoly_Type.coeff (sym_mpoly A k) (lead_monom (sym_mpoly A k)) = (1::'a)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Symmetric_Polynomials.lead_coeff (sym_mpoly A k) = (1::'a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lead_monom_sym_mpoly:
  assumes "sorted xs" "distinct xs" "k \<le> length xs"
  shows   "lead_monom (sym_mpoly (set xs) k :: 'a :: zero_neq_one mpoly) =
             monom_of_set (set (take k xs))" (is "lead_monom ?p = _")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lead_monom (sym_mpoly (set xs) k) = monom_of_set (set (take k xs))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lead_monom (sym_mpoly (set xs) k) = monom_of_set (set (take k xs))
[PROOF STEP]
let ?m = "lead_monom ?p"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lead_monom (sym_mpoly (set xs) k) = monom_of_set (set (take k xs))
[PROOF STEP]
have sym: "symmetric_mpoly (set xs) (sym_mpoly (set xs) k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. symmetric_mpoly (set xs) (sym_mpoly (set xs) k)
[PROOF STEP]
by (intro symmetric_sym_mpoly) auto
[PROOF STATE]
proof (state)
this:
symmetric_mpoly (set xs) (sym_mpoly (set xs) k)

goal (1 subgoal):
 1. lead_monom (sym_mpoly (set xs) k) = monom_of_set (set (take k xs))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
sorted xs
distinct xs
k \<le> length xs
[PROOF STEP]
have [simp]: "card (set xs) = length xs"
[PROOF STATE]
proof (prove)
using this:
sorted xs
distinct xs
k \<le> length xs

goal (1 subgoal):
 1. card (set xs) = length xs
[PROOF STEP]
by (subst distinct_card) auto
[PROOF STATE]
proof (state)
this:
card (set xs) = length xs

goal (1 subgoal):
 1. lead_monom (sym_mpoly (set xs) k) = monom_of_set (set (take k xs))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
sorted xs
distinct xs
k \<le> length xs
[PROOF STEP]
have "lead_coeff ?p = 1"
[PROOF STATE]
proof (prove)
using this:
sorted xs
distinct xs
k \<le> length xs

goal (1 subgoal):
 1. Symmetric_Polynomials.lead_coeff (sym_mpoly (set xs) k) = (1::'a)
[PROOF STEP]
by (subst lead_coeff_sym_mpoly) auto
[PROOF STATE]
proof (state)
this:
Symmetric_Polynomials.lead_coeff (sym_mpoly (set xs) k) = (1::'a)

goal (1 subgoal):
 1. lead_monom (sym_mpoly (set xs) k) = monom_of_set (set (take k xs))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Symmetric_Polynomials.lead_coeff (sym_mpoly (set xs) k) = (1::'a)
[PROOF STEP]
obtain X where X: "X \<subseteq> set xs" "card X = k" "?m = monom_of_set X"
[PROOF STATE]
proof (prove)
using this:
Symmetric_Polynomials.lead_coeff (sym_mpoly (set xs) k) = (1::'a)

goal (1 subgoal):
 1. (\<And>X. \<lbrakk>X \<subseteq> set xs; card X = k; lead_monom (sym_mpoly (set xs) k) = monom_of_set X\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding lead_coeff_def
[PROOF STATE]
proof (prove)
using this:
MPoly_Type.coeff (sym_mpoly (set xs) k) (lead_monom (sym_mpoly (set xs) k)) = (1::'a)

goal (1 subgoal):
 1. (\<And>X. \<lbrakk>X \<subseteq> set xs; card X = k; lead_monom (sym_mpoly (set xs) k) = monom_of_set X\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (subst (asm) coeff_sym_mpoly) (auto split: if_splits)
[PROOF STATE]
proof (state)
this:
X \<subseteq> set xs
card X = k
lead_monom (sym_mpoly (set xs) k) = monom_of_set X

goal (1 subgoal):
 1. lead_monom (sym_mpoly (set xs) k) = monom_of_set (set (take k xs))
[PROOF STEP]
define ys where "ys = map (\<lambda>x. if x \<in> X then 1 else 0 :: nat) xs"
[PROOF STATE]
proof (state)
this:
ys = map (\<lambda>x. if x \<in> X then 1 else 0) xs

goal (1 subgoal):
 1. lead_monom (sym_mpoly (set xs) k) = monom_of_set (set (take k xs))
[PROOF STEP]
have [simp]: "length ys = length xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length ys = length xs
[PROOF STEP]
by (simp add: ys_def)
[PROOF STATE]
proof (state)
this:
length ys = length xs

goal (1 subgoal):
 1. lead_monom (sym_mpoly (set xs) k) = monom_of_set (set (take k xs))
[PROOF STEP]
have ys_altdef: "ys = map (lookup ?m) xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ys = map (lookup (lead_monom (sym_mpoly (set xs) k))) xs
[PROOF STEP]
unfolding ys_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (\<lambda>x. if x \<in> X then 1 else 0) xs = map (lookup (lead_monom (sym_mpoly (set xs) k))) xs
[PROOF STEP]
using X finite_subset[OF X(1)]
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> set xs
card X = k
lead_monom (sym_mpoly (set xs) k) = monom_of_set X
finite (set xs) \<Longrightarrow> finite X

goal (1 subgoal):
 1. map (\<lambda>x. if x \<in> X then 1 else 0) xs = map (lookup (lead_monom (sym_mpoly (set xs) k))) xs
[PROOF STEP]
by (intro map_cong) (auto simp: lookup_monom_of_set)
[PROOF STATE]
proof (state)
this:
ys = map (lookup (lead_monom (sym_mpoly (set xs) k))) xs

goal (1 subgoal):
 1. lead_monom (sym_mpoly (set xs) k) = monom_of_set (set (take k xs))
[PROOF STEP]
define i where "i = Min (insert (length xs) {i. i < length xs \<and> ys ! i = 0})"
[PROOF STATE]
proof (state)
this:
i = Min (insert (length xs) {i. i < length xs \<and> ys ! i = 0})

goal (1 subgoal):
 1. lead_monom (sym_mpoly (set xs) k) = monom_of_set (set (take k xs))
[PROOF STEP]
have "i \<le> length xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<le> length xs
[PROOF STEP]
by (auto simp: i_def)
[PROOF STATE]
proof (state)
this:
i \<le> length xs

goal (1 subgoal):
 1. lead_monom (sym_mpoly (set xs) k) = monom_of_set (set (take k xs))
[PROOF STEP]
have in_X: "xs ! j \<in> X" if "j < i" for j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs ! j \<in> X
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
j < i

goal (1 subgoal):
 1. xs ! j \<in> X
[PROOF STEP]
unfolding i_def
[PROOF STATE]
proof (prove)
using this:
j < Min (insert (length xs) {i. i < length xs \<and> ys ! i = 0})

goal (1 subgoal):
 1. xs ! j \<in> X
[PROOF STEP]
by (auto simp: ys_def)
[PROOF STATE]
proof (state)
this:
?j1 < i \<Longrightarrow> xs ! ?j1 \<in> X

goal (1 subgoal):
 1. lead_monom (sym_mpoly (set xs) k) = monom_of_set (set (take k xs))
[PROOF STEP]
have not_in_X: "xs ! j \<notin> X" if "i \<le> j" "j < length xs" for j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs ! j \<notin> X
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. xs ! j \<notin> X
[PROOF STEP]
have ne: "{i. i < length xs \<and> ys ! i = 0} \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {i. i < length xs \<and> ys ! i = 0} \<noteq> {}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {i. i < length xs \<and> ys ! i = 0} = {} \<Longrightarrow> False
[PROOF STEP]
assume [simp]: "{i. i < length xs \<and> ys ! i = 0} = {}"
[PROOF STATE]
proof (state)
this:
{i. i < length xs \<and> ys ! i = 0} = {}

goal (1 subgoal):
 1. {i. i < length xs \<and> ys ! i = 0} = {} \<Longrightarrow> False
[PROOF STEP]
from that
[PROOF STATE]
proof (chain)
picking this:
i \<le> j
j < length xs
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
i \<le> j
j < length xs

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{i. i < length xs \<and> ys ! i = 0} \<noteq> {}

goal (1 subgoal):
 1. xs ! j \<notin> X
[PROOF STEP]
hence "Min {i. i < length xs \<and> ys ! i = 0} \<in> {i. i < length xs \<and> ys ! i = 0}"
[PROOF STATE]
proof (prove)
using this:
{i. i < length xs \<and> ys ! i = 0} \<noteq> {}

goal (1 subgoal):
 1. Min {i. i < length xs \<and> ys ! i = 0} \<in> {i. i < length xs \<and> ys ! i = 0}
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
{i. i < length xs \<and> ys ! i = 0} \<noteq> {}
i \<le> j
j < length xs

goal (1 subgoal):
 1. Min {i. i < length xs \<and> ys ! i = 0} \<in> {i. i < length xs \<and> ys ! i = 0}
[PROOF STEP]
by (intro Min_in) auto
[PROOF STATE]
proof (state)
this:
Min {i. i < length xs \<and> ys ! i = 0} \<in> {i. i < length xs \<and> ys ! i = 0}

goal (1 subgoal):
 1. xs ! j \<notin> X
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Min {i. i < length xs \<and> ys ! i = 0} \<in> {i. i < length xs \<and> ys ! i = 0}

goal (1 subgoal):
 1. xs ! j \<notin> X
[PROOF STEP]
have "Min {i. i < length xs \<and> ys ! i = 0} = i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Min {i. i < length xs \<and> ys ! i = 0} = i
[PROOF STEP]
unfolding i_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Min {i. i < length xs \<and> ys ! i = 0} = Min (insert (length xs) {i. i < length xs \<and> ys ! i = 0})
[PROOF STEP]
using ne
[PROOF STATE]
proof (prove)
using this:
{i. i < length xs \<and> ys ! i = 0} \<noteq> {}

goal (1 subgoal):
 1. Min {i. i < length xs \<and> ys ! i = 0} = Min (insert (length xs) {i. i < length xs \<and> ys ! i = 0})
[PROOF STEP]
by (subst Min_insert) (auto simp: min_def)
[PROOF STATE]
proof (state)
this:
Min {i. i < length xs \<and> ys ! i = 0} = i

goal (1 subgoal):
 1. xs ! j \<notin> X
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
i \<in> {i. i < length xs \<and> ys ! i = 0}
[PROOF STEP]
have i: "ys ! i = 0" "i < length xs"
[PROOF STATE]
proof (prove)
using this:
i \<in> {i. i < length xs \<and> ys ! i = 0}

goal (1 subgoal):
 1. ys ! i = 0 &&& i < length xs
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
ys ! i = 0
i < length xs

goal (1 subgoal):
 1. xs ! j \<notin> X
[PROOF STEP]
have "lookup ?m (xs ! j) \<le> lookup ?m (xs ! i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup (lead_monom (sym_mpoly (set xs) k)) (xs ! j) \<le> lookup (lead_monom (sym_mpoly (set xs) k)) (xs ! i)
[PROOF STEP]
using that assms
[PROOF STATE]
proof (prove)
using this:
i \<le> j
j < length xs
sorted xs
distinct xs
k \<le> length xs

goal (1 subgoal):
 1. lookup (lead_monom (sym_mpoly (set xs) k)) (xs ! j) \<le> lookup (lead_monom (sym_mpoly (set xs) k)) (xs ! i)
[PROOF STEP]
by (intro lookup_lead_monom_decreasing[OF sym])
         (auto intro!: sorted_nth_mono simp: set_conv_nth)
[PROOF STATE]
proof (state)
this:
lookup (lead_monom (sym_mpoly (set xs) k)) (xs ! j) \<le> lookup (lead_monom (sym_mpoly (set xs) k)) (xs ! i)

goal (1 subgoal):
 1. xs ! j \<notin> X
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lookup (lead_monom (sym_mpoly (set xs) k)) (xs ! j) \<le> lookup (lead_monom (sym_mpoly (set xs) k)) (xs ! i)

goal (1 subgoal):
 1. xs ! j \<notin> X
[PROOF STEP]
have "\<dots> = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup (lead_monom (sym_mpoly (set xs) k)) (xs ! i) = 0
[PROOF STEP]
using i
[PROOF STATE]
proof (prove)
using this:
ys ! i = 0
i < length xs

goal (1 subgoal):
 1. lookup (lead_monom (sym_mpoly (set xs) k)) (xs ! i) = 0
[PROOF STEP]
by (simp add: ys_altdef)
[PROOF STATE]
proof (state)
this:
lookup (lead_monom (sym_mpoly (set xs) k)) (xs ! i) = 0

goal (1 subgoal):
 1. xs ! j \<notin> X
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
lookup (lead_monom (sym_mpoly (set xs) k)) (xs ! j) \<le> 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
lookup (lead_monom (sym_mpoly (set xs) k)) (xs ! j) \<le> 0

goal (1 subgoal):
 1. xs ! j \<notin> X
[PROOF STEP]
using that X finite_subset[OF X(1)]
[PROOF STATE]
proof (prove)
using this:
lookup (lead_monom (sym_mpoly (set xs) k)) (xs ! j) \<le> 0
i \<le> j
j < length xs
X \<subseteq> set xs
card X = k
lead_monom (sym_mpoly (set xs) k) = monom_of_set X
finite (set xs) \<Longrightarrow> finite X

goal (1 subgoal):
 1. xs ! j \<notin> X
[PROOF STEP]
by (auto simp: lookup_monom_of_set)
[PROOF STATE]
proof (state)
this:
xs ! j \<notin> X

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>i \<le> ?j1; ?j1 < length xs\<rbrakk> \<Longrightarrow> xs ! ?j1 \<notin> X

goal (1 subgoal):
 1. lead_monom (sym_mpoly (set xs) k) = monom_of_set (set (take k xs))
[PROOF STEP]
from X
[PROOF STATE]
proof (chain)
picking this:
X \<subseteq> set xs
card X = k
lead_monom (sym_mpoly (set xs) k) = monom_of_set X
[PROOF STEP]
have "k = card X"
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> set xs
card X = k
lead_monom (sym_mpoly (set xs) k) = monom_of_set X

goal (1 subgoal):
 1. k = card X
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
k = card X

goal (1 subgoal):
 1. lead_monom (sym_mpoly (set xs) k) = monom_of_set (set (take k xs))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
k = card X

goal (1 subgoal):
 1. lead_monom (sym_mpoly (set xs) k) = monom_of_set (set (take k xs))
[PROOF STEP]
have "X = (\<lambda>i. xs ! i) ` {i. i < length xs \<and> xs ! i \<in> X}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X = (!) xs ` {i. i < length xs \<and> xs ! i \<in> X}
[PROOF STEP]
using X
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> set xs
card X = k
lead_monom (sym_mpoly (set xs) k) = monom_of_set X

goal (1 subgoal):
 1. X = (!) xs ` {i. i < length xs \<and> xs ! i \<in> X}
[PROOF STEP]
by (auto simp: set_conv_nth)
[PROOF STATE]
proof (state)
this:
X = (!) xs ` {i. i < length xs \<and> xs ! i \<in> X}

goal (1 subgoal):
 1. lead_monom (sym_mpoly (set xs) k) = monom_of_set (set (take k xs))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
X = (!) xs ` {i. i < length xs \<and> xs ! i \<in> X}

goal (1 subgoal):
 1. lead_monom (sym_mpoly (set xs) k) = monom_of_set (set (take k xs))
[PROOF STEP]
have "card \<dots> = (\<Sum>i | i < length xs \<and> xs ! i \<in> X. 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card ((!) xs ` {i. i < length xs \<and> xs ! i \<in> X}) = (\<Sum>i | i < length xs \<and> xs ! i \<in> X. 1)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
sorted xs
distinct xs
k \<le> length xs

goal (1 subgoal):
 1. card ((!) xs ` {i. i < length xs \<and> xs ! i \<in> X}) = (\<Sum>i | i < length xs \<and> xs ! i \<in> X. 1)
[PROOF STEP]
by (subst card_image) (auto intro!: inj_on_nth)
[PROOF STATE]
proof (state)
this:
card ((!) xs ` {i. i < length xs \<and> xs ! i \<in> X}) = (\<Sum>i | i < length xs \<and> xs ! i \<in> X. 1)

goal (1 subgoal):
 1. lead_monom (sym_mpoly (set xs) k) = monom_of_set (set (take k xs))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card ((!) xs ` {i. i < length xs \<and> xs ! i \<in> X}) = (\<Sum>i | i < length xs \<and> xs ! i \<in> X. 1)

goal (1 subgoal):
 1. lead_monom (sym_mpoly (set xs) k) = monom_of_set (set (take k xs))
[PROOF STEP]
have "\<dots> = (\<Sum>i | i < length xs. if xs ! i \<in> X then 1 else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i | i < length xs \<and> xs ! i \<in> X. 1) = (\<Sum>i | i < length xs. if xs ! i \<in> X then 1 else 0)
[PROOF STEP]
by (intro sum.mono_neutral_cong_left) auto
[PROOF STATE]
proof (state)
this:
(\<Sum>i | i < length xs \<and> xs ! i \<in> X. 1) = (\<Sum>i | i < length xs. if xs ! i \<in> X then 1 else 0)

goal (1 subgoal):
 1. lead_monom (sym_mpoly (set xs) k) = monom_of_set (set (take k xs))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i | i < length xs \<and> xs ! i \<in> X. 1) = (\<Sum>i | i < length xs. if xs ! i \<in> X then 1 else 0)

goal (1 subgoal):
 1. lead_monom (sym_mpoly (set xs) k) = monom_of_set (set (take k xs))
[PROOF STEP]
have "\<dots> = sum_list ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i | i < length xs. if xs ! i \<in> X then 1 else 0) = sum_list ys
[PROOF STEP]
by (auto simp: sum_list_sum_nth ys_def intro!: sum.cong)
[PROOF STATE]
proof (state)
this:
(\<Sum>i | i < length xs. if xs ! i \<in> X then 1 else 0) = sum_list ys

goal (1 subgoal):
 1. lead_monom (sym_mpoly (set xs) k) = monom_of_set (set (take k xs))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i | i < length xs. if xs ! i \<in> X then 1 else 0) = sum_list ys

goal (1 subgoal):
 1. lead_monom (sym_mpoly (set xs) k) = monom_of_set (set (take k xs))
[PROOF STEP]
have "ys = take i ys @ drop i ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ys = take i ys @ drop i ys
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ys = take i ys @ drop i ys

goal (1 subgoal):
 1. lead_monom (sym_mpoly (set xs) k) = monom_of_set (set (take k xs))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ys = take i ys @ drop i ys

goal (1 subgoal):
 1. lead_monom (sym_mpoly (set xs) k) = monom_of_set (set (take k xs))
[PROOF STEP]
have "sum_list \<dots> = sum_list (take i ys) + sum_list (drop i ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_list (take i ys @ drop i ys) = sum_list (take i ys) + sum_list (drop i ys)
[PROOF STEP]
by (subst sum_list_append) auto
[PROOF STATE]
proof (state)
this:
sum_list (take i ys @ drop i ys) = sum_list (take i ys) + sum_list (drop i ys)

goal (1 subgoal):
 1. lead_monom (sym_mpoly (set xs) k) = monom_of_set (set (take k xs))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum_list (take i ys @ drop i ys) = sum_list (take i ys) + sum_list (drop i ys)

goal (1 subgoal):
 1. lead_monom (sym_mpoly (set xs) k) = monom_of_set (set (take k xs))
[PROOF STEP]
have "take i ys = replicate i 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. take i ys = replicate i 1
[PROOF STEP]
using \<open>i \<le> length xs\<close> in_X
[PROOF STATE]
proof (prove)
using this:
i \<le> length xs
?j1 < i \<Longrightarrow> xs ! ?j1 \<in> X

goal (1 subgoal):
 1. take i ys = replicate i 1
[PROOF STEP]
by (intro replicate_eqI) (auto simp: ys_def set_conv_nth)
[PROOF STATE]
proof (state)
this:
take i ys = replicate i 1

goal (1 subgoal):
 1. lead_monom (sym_mpoly (set xs) k) = monom_of_set (set (take k xs))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
take i ys = replicate i 1

goal (1 subgoal):
 1. lead_monom (sym_mpoly (set xs) k) = monom_of_set (set (take k xs))
[PROOF STEP]
have "sum_list \<dots> = i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_list (replicate i 1) = i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sum_list (replicate i 1) = i

goal (1 subgoal):
 1. lead_monom (sym_mpoly (set xs) k) = monom_of_set (set (take k xs))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum_list (replicate i 1) = i

goal (1 subgoal):
 1. lead_monom (sym_mpoly (set xs) k) = monom_of_set (set (take k xs))
[PROOF STEP]
have "drop i ys = replicate (length ys - i) 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. drop i ys = replicate (length ys - i) 0
[PROOF STEP]
using \<open>i \<le> length xs\<close> not_in_X
[PROOF STATE]
proof (prove)
using this:
i \<le> length xs
\<lbrakk>i \<le> ?j1; ?j1 < length xs\<rbrakk> \<Longrightarrow> xs ! ?j1 \<notin> X

goal (1 subgoal):
 1. drop i ys = replicate (length ys - i) 0
[PROOF STEP]
by (intro replicate_eqI) (auto simp: ys_def set_conv_nth)
[PROOF STATE]
proof (state)
this:
drop i ys = replicate (length ys - i) 0

goal (1 subgoal):
 1. lead_monom (sym_mpoly (set xs) k) = monom_of_set (set (take k xs))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
drop i ys = replicate (length ys - i) 0

goal (1 subgoal):
 1. lead_monom (sym_mpoly (set xs) k) = monom_of_set (set (take k xs))
[PROOF STEP]
have "sum_list \<dots> = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_list (replicate (length ys - i) 0) = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sum_list (replicate (length ys - i) 0) = 0

goal (1 subgoal):
 1. lead_monom (sym_mpoly (set xs) k) = monom_of_set (set (take k xs))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
k = i + 0
[PROOF STEP]
have "i = k"
[PROOF STATE]
proof (prove)
using this:
k = i + 0

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

goal (1 subgoal):
 1. lead_monom (sym_mpoly (set xs) k) = monom_of_set (set (take k xs))
[PROOF STEP]
have "X = set (filter (\<lambda>x. x \<in> X) xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X = set (filter (\<lambda>x. x \<in> X) xs)
[PROOF STEP]
using X
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> set xs
card X = k
lead_monom (sym_mpoly (set xs) k) = monom_of_set X

goal (1 subgoal):
 1. X = set (filter (\<lambda>x. x \<in> X) xs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
X = set (filter (\<lambda>x. x \<in> X) xs)

goal (1 subgoal):
 1. lead_monom (sym_mpoly (set xs) k) = monom_of_set (set (take k xs))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
X = set (filter (\<lambda>x. x \<in> X) xs)

goal (1 subgoal):
 1. lead_monom (sym_mpoly (set xs) k) = monom_of_set (set (take k xs))
[PROOF STEP]
have "xs = take i xs @ drop i xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs = take i xs @ drop i xs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
xs = take i xs @ drop i xs

goal (1 subgoal):
 1. lead_monom (sym_mpoly (set xs) k) = monom_of_set (set (take k xs))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
xs = take i xs @ drop i xs

goal (1 subgoal):
 1. lead_monom (sym_mpoly (set xs) k) = monom_of_set (set (take k xs))
[PROOF STEP]
note filter_append
[PROOF STATE]
proof (state)
this:
filter ?P (?xs @ ?ys) = filter ?P ?xs @ filter ?P ?ys

goal (1 subgoal):
 1. lead_monom (sym_mpoly (set xs) k) = monom_of_set (set (take k xs))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
filter ?P (?xs @ ?ys) = filter ?P ?xs @ filter ?P ?ys

goal (1 subgoal):
 1. lead_monom (sym_mpoly (set xs) k) = monom_of_set (set (take k xs))
[PROOF STEP]
have "filter (\<lambda>x. x \<in> X) (take i xs) = take i xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filter (\<lambda>x. x \<in> X) (take i xs) = take i xs
[PROOF STEP]
using in_X
[PROOF STATE]
proof (prove)
using this:
?j1 < i \<Longrightarrow> xs ! ?j1 \<in> X

goal (1 subgoal):
 1. filter (\<lambda>x. x \<in> X) (take i xs) = take i xs
[PROOF STEP]
by (intro filter_True) (auto simp: set_conv_nth)
[PROOF STATE]
proof (state)
this:
filter (\<lambda>x. x \<in> X) (take i xs) = take i xs

goal (1 subgoal):
 1. lead_monom (sym_mpoly (set xs) k) = monom_of_set (set (take k xs))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
filter (\<lambda>x. x \<in> X) (take i xs) = take i xs

goal (1 subgoal):
 1. lead_monom (sym_mpoly (set xs) k) = monom_of_set (set (take k xs))
[PROOF STEP]
have "filter (\<lambda>x. x \<in> X) (drop i xs) = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filter (\<lambda>x. x \<in> X) (drop i xs) = []
[PROOF STEP]
using not_in_X
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i \<le> ?j1; ?j1 < length xs\<rbrakk> \<Longrightarrow> xs ! ?j1 \<notin> X

goal (1 subgoal):
 1. filter (\<lambda>x. x \<in> X) (drop i xs) = []
[PROOF STEP]
by (intro filter_False) (auto simp: set_conv_nth)
[PROOF STATE]
proof (state)
this:
filter (\<lambda>x. x \<in> X) (drop i xs) = []

goal (1 subgoal):
 1. lead_monom (sym_mpoly (set xs) k) = monom_of_set (set (take k xs))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
X = set (take i xs @ [])
[PROOF STEP]
have "X = set (take i xs)"
[PROOF STATE]
proof (prove)
using this:
X = set (take i xs @ [])

goal (1 subgoal):
 1. X = set (take i xs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
X = set (take i xs)

goal (1 subgoal):
 1. lead_monom (sym_mpoly (set xs) k) = monom_of_set (set (take k xs))
[PROOF STEP]
with \<open>i = k\<close> and X
[PROOF STATE]
proof (chain)
picking this:
i = k
X \<subseteq> set xs
card X = k
lead_monom (sym_mpoly (set xs) k) = monom_of_set X
X = set (take i xs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i = k
X \<subseteq> set xs
card X = k
lead_monom (sym_mpoly (set xs) k) = monom_of_set X
X = set (take i xs)

goal (1 subgoal):
 1. lead_monom (sym_mpoly (set xs) k) = monom_of_set (set (take k xs))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lead_monom (sym_mpoly (set xs) k) = monom_of_set (set (take k xs))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wf_monom_less_on:
  assumes "finite A"
  shows   "wf (monom_less_on A :: ((nat \<Rightarrow>\<^sub>0 'b :: {zero, wellorder}) \<times> _) set)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf (monom_less_on A)
[PROOF STEP]
proof (rule wf_subset)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. wf ?r
 2. monom_less_on A \<subseteq> ?r
[PROOF STEP]
define n where "n = Suc (Max (insert 0 A))"
[PROOF STATE]
proof (state)
this:
n = Suc (Max (insert 0 A))

goal (2 subgoals):
 1. wf ?r
 2. monom_less_on A \<subseteq> ?r
[PROOF STEP]
have less_n: "k < n" if "k \<in> A" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k < n
[PROOF STEP]
using that assms
[PROOF STATE]
proof (prove)
using this:
k \<in> A
finite A

goal (1 subgoal):
 1. k < n
[PROOF STEP]
by (auto simp: n_def less_Suc_eq_le Max_ge_iff)
[PROOF STATE]
proof (state)
this:
?k \<in> A \<Longrightarrow> ?k < n

goal (2 subgoals):
 1. wf ?r
 2. monom_less_on A \<subseteq> ?r
[PROOF STEP]
define f :: "(nat \<Rightarrow>\<^sub>0 'b) \<Rightarrow> 'b list" where "f = (\<lambda>m. map (lookup m) [0..<n])"
[PROOF STATE]
proof (state)
this:
f = (\<lambda>m. map (lookup m) [0..<n])

goal (2 subgoals):
 1. wf ?r
 2. monom_less_on A \<subseteq> ?r
[PROOF STEP]
show "wf (inv_image (lexn {(x,y). x < y} n) f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf (inv_image (lexn {(x, y). x < y} n) f)
[PROOF STEP]
by (intro wf_inv_image wf_lexn wellorder_class.wf)
[PROOF STATE]
proof (state)
this:
wf (inv_image (lexn {(x, y). x < y} n) f)

goal (1 subgoal):
 1. monom_less_on A \<subseteq> inv_image (lexn {(x, y). x < y} (Suc (Max (insert 0 A)))) (\<lambda>m. map (lookup m) [0..<Suc (Max (insert 0 A))])
[PROOF STEP]
show "monom_less_on A \<subseteq> inv_image (lexn {(x, y). x < y} n) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monom_less_on A \<subseteq> inv_image (lexn {(x, y). x < y} n) f
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> monom_less_on A \<Longrightarrow> (a, b) \<in> inv_image (lexn {(x, y). x < y} n) f
[PROOF STEP]
fix m1 m2 :: "nat \<Rightarrow>\<^sub>0 'b"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> monom_less_on A \<Longrightarrow> (a, b) \<in> inv_image (lexn {(x, y). x < y} n) f
[PROOF STEP]
assume "(m1, m2) \<in> monom_less_on A"
[PROOF STATE]
proof (state)
this:
(m1, m2) \<in> monom_less_on A

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> monom_less_on A \<Longrightarrow> (a, b) \<in> inv_image (lexn {(x, y). x < y} n) f
[PROOF STEP]
hence m12: "m1 < m2" "keys m1 \<subseteq> A" "keys m2 \<subseteq> A"
[PROOF STATE]
proof (prove)
using this:
(m1, m2) \<in> monom_less_on A

goal (1 subgoal):
 1. m1 < m2 &&& keys m1 \<subseteq> A &&& keys m2 \<subseteq> A
[PROOF STEP]
by (auto simp: monom_less_on_def)
[PROOF STATE]
proof (state)
this:
m1 < m2
keys m1 \<subseteq> A
keys m2 \<subseteq> A

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> monom_less_on A \<Longrightarrow> (a, b) \<in> inv_image (lexn {(x, y). x < y} n) f
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
m1 < m2
keys m1 \<subseteq> A
keys m2 \<subseteq> A
[PROOF STEP]
obtain k where k: "lookup m1 k < lookup m2 k" "\<forall>i<k. lookup m1 i = lookup m2 i"
[PROOF STATE]
proof (prove)
using this:
m1 < m2
keys m1 \<subseteq> A
keys m2 \<subseteq> A

goal (1 subgoal):
 1. (\<And>k. \<lbrakk>lookup m1 k < lookup m2 k; \<forall>i<k. lookup m1 i = lookup m2 i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: less_poly_mapping_def less_fun_def)
[PROOF STATE]
proof (state)
this:
lookup m1 k < lookup m2 k
\<forall>i<k. lookup m1 i = lookup m2 i

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> monom_less_on A \<Longrightarrow> (a, b) \<in> inv_image (lexn {(x, y). x < y} n) f
[PROOF STEP]
have "\<not>(lookup m1 k = 0 \<and> lookup m2 k = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> (lookup m1 k = (0::'b) \<and> lookup m2 k = (0::'b))
[PROOF STEP]
proof (intro notI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lookup m1 k = (0::'b) \<and> lookup m2 k = (0::'b) \<Longrightarrow> False
[PROOF STEP]
assume "lookup m1 k = 0 \<and> lookup m2 k = 0"
[PROOF STATE]
proof (state)
this:
lookup m1 k = (0::'b) \<and> lookup m2 k = (0::'b)

goal (1 subgoal):
 1. lookup m1 k = (0::'b) \<and> lookup m2 k = (0::'b) \<Longrightarrow> False
[PROOF STEP]
hence [simp]: "lookup m1 k = 0" "lookup m2 k = 0"
[PROOF STATE]
proof (prove)
using this:
lookup m1 k = (0::'b) \<and> lookup m2 k = (0::'b)

goal (1 subgoal):
 1. lookup m1 k = (0::'b) &&& lookup m2 k = (0::'b)
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
lookup m1 k = (0::'b)
lookup m2 k = (0::'b)

goal (1 subgoal):
 1. lookup m1 k = (0::'b) \<and> lookup m2 k = (0::'b) \<Longrightarrow> False
[PROOF STEP]
from k(1)
[PROOF STATE]
proof (chain)
picking this:
lookup m1 k < lookup m2 k
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
lookup m1 k < lookup m2 k

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:
\<not> (lookup m1 k = (0::'b) \<and> lookup m2 k = (0::'b))

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> monom_less_on A \<Longrightarrow> (a, b) \<in> inv_image (lexn {(x, y). x < y} n) f
[PROOF STEP]
hence "k \<in> A"
[PROOF STATE]
proof (prove)
using this:
\<not> (lookup m1 k = (0::'b) \<and> lookup m2 k = (0::'b))

goal (1 subgoal):
 1. k \<in> A
[PROOF STEP]
using m12
[PROOF STATE]
proof (prove)
using this:
\<not> (lookup m1 k = (0::'b) \<and> lookup m2 k = (0::'b))
m1 < m2
keys m1 \<subseteq> A
keys m2 \<subseteq> A

goal (1 subgoal):
 1. k \<in> A
[PROOF STEP]
by (auto simp: in_keys_iff)
[PROOF STATE]
proof (state)
this:
k \<in> A

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> monom_less_on A \<Longrightarrow> (a, b) \<in> inv_image (lexn {(x, y). x < y} n) f
[PROOF STEP]
hence "k < n"
[PROOF STATE]
proof (prove)
using this:
k \<in> A

goal (1 subgoal):
 1. k < n
[PROOF STEP]
by (simp add: less_n)
[PROOF STATE]
proof (state)
this:
k < n

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> monom_less_on A \<Longrightarrow> (a, b) \<in> inv_image (lexn {(x, y). x < y} n) f
[PROOF STEP]
define as where "as = map (lookup m1) [0..<k]"
[PROOF STATE]
proof (state)
this:
as = map (lookup m1) [0..<k]

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> monom_less_on A \<Longrightarrow> (a, b) \<in> inv_image (lexn {(x, y). x < y} n) f
[PROOF STEP]
define bs1 where "bs1 = map (lookup m1) [Suc k..<n]"
[PROOF STATE]
proof (state)
this:
bs1 = map (lookup m1) [Suc k..<n]

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> monom_less_on A \<Longrightarrow> (a, b) \<in> inv_image (lexn {(x, y). x < y} n) f
[PROOF STEP]
define bs2 where "bs2 = map (lookup m2) [Suc k..<n]"
[PROOF STATE]
proof (state)
this:
bs2 = map (lookup m2) [Suc k..<n]

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> monom_less_on A \<Longrightarrow> (a, b) \<in> inv_image (lexn {(x, y). x < y} n) f
[PROOF STEP]
have decomp: "[0..<n] = [0..<k] @ [k] @ drop (Suc k) [0..<n]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [0..<n] = [0..<k] @ [k] @ drop (Suc k) [0..<n]
[PROOF STEP]
using \<open>k < n\<close>
[PROOF STATE]
proof (prove)
using this:
k < n

goal (1 subgoal):
 1. [0..<n] = [0..<k] @ [k] @ drop (Suc k) [0..<n]
[PROOF STEP]
by (simp flip: upt_conv_Cons upt_add_eq_append')
[PROOF STATE]
proof (state)
this:
[0..<n] = [0..<k] @ [k] @ drop (Suc k) [0..<n]

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> monom_less_on A \<Longrightarrow> (a, b) \<in> inv_image (lexn {(x, y). x < y} n) f
[PROOF STEP]
have [simp]: "length as = k" "length bs1 = n - Suc k" "length bs2 = n - Suc k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length as = k &&& length bs1 = n - Suc k &&& length bs2 = n - Suc k
[PROOF STEP]
by (simp_all add: as_def bs1_def bs2_def)
[PROOF STATE]
proof (state)
this:
length as = k
length bs1 = n - Suc k
length bs2 = n - Suc k

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> monom_less_on A \<Longrightarrow> (a, b) \<in> inv_image (lexn {(x, y). x < y} n) f
[PROOF STEP]
have "f m1 = as @ [lookup m1 k] @ bs1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f m1 = as @ [lookup m1 k] @ bs1
[PROOF STEP]
unfolding f_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (lookup m1) [0..<n] = as @ [lookup m1 k] @ bs1
[PROOF STEP]
by (subst decomp) (simp add: as_def bs1_def)
[PROOF STATE]
proof (state)
this:
f m1 = as @ [lookup m1 k] @ bs1

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> monom_less_on A \<Longrightarrow> (a, b) \<in> inv_image (lexn {(x, y). x < y} n) f
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f m1 = as @ [lookup m1 k] @ bs1

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> monom_less_on A \<Longrightarrow> (a, b) \<in> inv_image (lexn {(x, y). x < y} n) f
[PROOF STEP]
have "f m2 = as @ [lookup m2 k] @ bs2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f m2 = as @ [lookup m2 k] @ bs2
[PROOF STEP]
unfolding f_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (lookup m2) [0..<n] = as @ [lookup m2 k] @ bs2
[PROOF STEP]
using k
[PROOF STATE]
proof (prove)
using this:
lookup m1 k < lookup m2 k
\<forall>i<k. lookup m1 i = lookup m2 i

goal (1 subgoal):
 1. map (lookup m2) [0..<n] = as @ [lookup m2 k] @ bs2
[PROOF STEP]
by (subst decomp) (simp add: as_def bs2_def)
[PROOF STATE]
proof (state)
this:
f m2 = as @ [lookup m2 k] @ bs2

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> monom_less_on A \<Longrightarrow> (a, b) \<in> inv_image (lexn {(x, y). x < y} n) f
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
f m1 = as @ [lookup m1 k] @ bs1
f m2 = as @ [lookup m2 k] @ bs2
[PROOF STEP]
show "(m1, m2) \<in> inv_image (lexn {(x,y). x < y} n) f"
[PROOF STATE]
proof (prove)
using this:
f m1 = as @ [lookup m1 k] @ bs1
f m2 = as @ [lookup m2 k] @ bs2

goal (1 subgoal):
 1. (m1, m2) \<in> inv_image (lexn {(x, y). x < y} n) f
[PROOF STEP]
using k(1) \<open>k < n\<close>
[PROOF STATE]
proof (prove)
using this:
f m1 = as @ [lookup m1 k] @ bs1
f m2 = as @ [lookup m2 k] @ bs2
lookup m1 k < lookup m2 k
k < n

goal (1 subgoal):
 1. (m1, m2) \<in> inv_image (lexn {(x, y). x < y} n) f
[PROOF STEP]
unfolding lexn_conv
[PROOF STATE]
proof (prove)
using this:
f m1 = as @ [lookup m1 k] @ bs1
f m2 = as @ [lookup m2 k] @ bs2
lookup m1 k < lookup m2 k
k < n

goal (1 subgoal):
 1. (m1, m2) \<in> inv_image {(xs, ys). length xs = n \<and> length ys = n \<and> (\<exists>xys x y xs' ys'. xs = xys @ x # xs' \<and> ys = xys @ y # ys' \<and> (x, y) \<in> {(x, y). x < y})} f
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(m1, m2) \<in> inv_image (lexn {(x, y). x < y} n) f

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
monom_less_on A \<subseteq> inv_image (lexn {(x, y). x < y} n) f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lead_monom_induct [consumes 2, case_names less]:
  fixes p :: "'a :: zero mpoly"
  assumes fin: "finite A" and vars: "vars p \<subseteq> A"
  assumes IH: "\<And>p. vars p \<subseteq> A \<Longrightarrow>
                 (\<And>p'. vars p' \<subseteq> A \<Longrightarrow> lead_monom p' < lead_monom p \<Longrightarrow> P p') \<Longrightarrow> P p"
  shows   "P p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P p
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
vars p \<subseteq> A

goal (1 subgoal):
 1. P p
[PROOF STEP]
proof (induct m \<equiv> "lead_monom p" arbitrary: p rule: wf_induct_rule[OF wf_monom_less_on[OF fin]])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>\<And>pa. \<lbrakk>(lead_monom pa, lead_monom p) \<in> monom_less_on A; vars pa \<subseteq> A\<rbrakk> \<Longrightarrow> P pa; vars p \<subseteq> A\<rbrakk> \<Longrightarrow> P p
[PROOF STEP]
case (1 p)
[PROOF STATE]
proof (state)
this:
\<lbrakk>(lead_monom ?p, lead_monom p) \<in> monom_less_on A; vars ?p \<subseteq> A\<rbrakk> \<Longrightarrow> P ?p
vars p \<subseteq> A

goal (1 subgoal):
 1. \<And>p. \<lbrakk>\<And>pa. \<lbrakk>(lead_monom pa, lead_monom p) \<in> monom_less_on A; vars pa \<subseteq> A\<rbrakk> \<Longrightarrow> P pa; vars p \<subseteq> A\<rbrakk> \<Longrightarrow> P p
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P p
[PROOF STEP]
proof (rule IH)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. vars p \<subseteq> A
 2. \<And>p'. \<lbrakk>vars p' \<subseteq> A; lead_monom p' < lead_monom p\<rbrakk> \<Longrightarrow> P p'
[PROOF STEP]
fix p' :: "'a mpoly"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. vars p \<subseteq> A
 2. \<And>p'. \<lbrakk>vars p' \<subseteq> A; lead_monom p' < lead_monom p\<rbrakk> \<Longrightarrow> P p'
[PROOF STEP]
assume *: "vars p' \<subseteq> A" "lead_monom p' < lead_monom p"
[PROOF STATE]
proof (state)
this:
vars p' \<subseteq> A
lead_monom p' < lead_monom p

goal (2 subgoals):
 1. vars p \<subseteq> A
 2. \<And>p'. \<lbrakk>vars p' \<subseteq> A; lead_monom p' < lead_monom p\<rbrakk> \<Longrightarrow> P p'
[PROOF STEP]
show "P p'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P p'
[PROOF STEP]
by (rule 1) (insert * "1.prems" keys_lead_monom_subset, auto simp: monom_less_on_def)
[PROOF STATE]
proof (state)
this:
P p'

goal (1 subgoal):
 1. vars p \<subseteq> A
[PROOF STEP]
qed (insert 1, auto)
[PROOF STATE]
proof (state)
this:
P p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lead_monom_induct' [case_names less]:
  fixes p :: "'a :: zero mpoly"
  assumes IH: "\<And>p. (\<And>p'. vars p' \<subseteq> vars p \<Longrightarrow> lead_monom p' < lead_monom p \<Longrightarrow> P p') \<Longrightarrow> P p"
  shows   "P p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P p
[PROOF STEP]
have "finite (vars p)" "vars p \<subseteq> vars p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (vars p) &&& vars p \<subseteq> vars p
[PROOF STEP]
by (auto simp: vars_finite)
[PROOF STATE]
proof (state)
this:
finite (vars p)
vars p \<subseteq> vars p

goal (1 subgoal):
 1. P p
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
finite (vars p)
vars p \<subseteq> vars p

goal (1 subgoal):
 1. P p
[PROOF STEP]
by (induction rule: lead_monom_induct) (use IH in blast)
[PROOF STATE]
proof (state)
this:
P p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lead_coeff_sym_mpoly_powerprod:
  assumes "finite A" "\<And>x. x \<in> X \<Longrightarrow> f x \<in> {1..card A}"
  shows   "lead_coeff (\<Prod>x\<in>X. sym_mpoly A (f (x::'a)) ^ g x) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Symmetric_Polynomials.lead_coeff (\<Prod>x\<in>X. sym_mpoly A (f x) ^ g x) = (1::'b)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Symmetric_Polynomials.lead_coeff (\<Prod>x\<in>X. sym_mpoly A (f x) ^ g x) = (1::'b)
[PROOF STEP]
have eq: "lead_coeff (sym_mpoly A (f x) ^ g x :: 'b mpoly) = 1" if "x \<in> X" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Symmetric_Polynomials.lead_coeff (sym_mpoly A (f x) ^ g x) = (1::'b)
[PROOF STEP]
using that assms
[PROOF STATE]
proof (prove)
using this:
x \<in> X
finite A
?x \<in> X \<Longrightarrow> f ?x \<in> {1..card A}

goal (1 subgoal):
 1. Symmetric_Polynomials.lead_coeff (sym_mpoly A (f x) ^ g x) = (1::'b)
[PROOF STEP]
by (subst lead_coeff_power) (auto simp: lead_coeff_sym_mpoly assms)
[PROOF STATE]
proof (state)
this:
?x \<in> X \<Longrightarrow> Symmetric_Polynomials.lead_coeff (sym_mpoly A (f ?x) ^ g ?x) = (1::'b)

goal (1 subgoal):
 1. Symmetric_Polynomials.lead_coeff (\<Prod>x\<in>X. sym_mpoly A (f x) ^ g x) = (1::'b)
[PROOF STEP]
hence "(\<Prod>x\<in>X. lead_coeff (sym_mpoly A (f x) ^ g x :: 'b mpoly)) = (\<Prod>x\<in>X. 1)"
[PROOF STATE]
proof (prove)
using this:
?x \<in> X \<Longrightarrow> Symmetric_Polynomials.lead_coeff (sym_mpoly A (f ?x) ^ g ?x) = (1::'b)

goal (1 subgoal):
 1. (\<Prod>x\<in>X. Symmetric_Polynomials.lead_coeff (sym_mpoly A (f x) ^ g x)) = (\<Prod>x\<in>X. (1::'b))
[PROOF STEP]
by (intro prod.cong eq refl)
[PROOF STATE]
proof (state)
this:
(\<Prod>x\<in>X. Symmetric_Polynomials.lead_coeff (sym_mpoly A (f x) ^ g x)) = (\<Prod>x\<in>X. (1::'b))

goal (1 subgoal):
 1. Symmetric_Polynomials.lead_coeff (\<Prod>x\<in>X. sym_mpoly A (f x) ^ g x) = (1::'b)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Prod>x\<in>X. Symmetric_Polynomials.lead_coeff (sym_mpoly A (f x) ^ g x)) = (\<Prod>x\<in>X. (1::'b))

goal (1 subgoal):
 1. Symmetric_Polynomials.lead_coeff (\<Prod>x\<in>X. sym_mpoly A (f x) ^ g x) = (1::'b)
[PROOF STEP]
have "\<dots> = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>x\<in>X. (1::'b)) = (1::'b)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Prod>x\<in>X. (1::'b)) = (1::'b)

goal (1 subgoal):
 1. Symmetric_Polynomials.lead_coeff (\<Prod>x\<in>X. sym_mpoly A (f x) ^ g x) = (1::'b)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Prod>x\<in>X. Symmetric_Polynomials.lead_coeff (sym_mpoly A (f x) ^ g x)) = (1::'b)
[PROOF STEP]
have eq': "(\<Prod>x\<in>X. lead_coeff (sym_mpoly A (f x) ^ g x :: 'b mpoly)) = 1"
[PROOF STATE]
proof (prove)
using this:
(\<Prod>x\<in>X. Symmetric_Polynomials.lead_coeff (sym_mpoly A (f x) ^ g x)) = (1::'b)

goal (1 subgoal):
 1. (\<Prod>x\<in>X. Symmetric_Polynomials.lead_coeff (sym_mpoly A (f x) ^ g x)) = (1::'b)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<Prod>x\<in>X. Symmetric_Polynomials.lead_coeff (sym_mpoly A (f x) ^ g x)) = (1::'b)

goal (1 subgoal):
 1. Symmetric_Polynomials.lead_coeff (\<Prod>x\<in>X. sym_mpoly A (f x) ^ g x) = (1::'b)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Symmetric_Polynomials.lead_coeff (\<Prod>x\<in>X. sym_mpoly A (f x) ^ g x) = (1::'b)
[PROOF STEP]
by (subst lead_coeff_prod) (auto simp: eq eq')
[PROOF STATE]
proof (state)
this:
Symmetric_Polynomials.lead_coeff (\<Prod>x\<in>X. sym_mpoly A (f x) ^ g x) = (1::'b)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma coeff_fund_sym_step_coeff: "coeff (fund_sym_step_coeff p) m \<in> {lead_coeff p, 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MPoly_Type.coeff (local.fund_sym_step_coeff p) m \<in> {Symmetric_Polynomials.lead_coeff p, 0::'a}
[PROOF STEP]
by (auto simp: fund_sym_step_coeff_def coeff_monom when_def)


[STATEMENT]
lemma vars_fund_sym_step_coeff: "vars (fund_sym_step_coeff p) \<subseteq> vars p - A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars (local.fund_sym_step_coeff p) \<subseteq> vars p - A
[PROOF STEP]
unfolding fund_sym_step_coeff_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars (MPoly_Type.monom (restrictpm (- A) (lead_monom p)) (Symmetric_Polynomials.lead_coeff p)) \<subseteq> vars p - A
[PROOF STEP]
using keys_lead_monom_subset[of p]
[PROOF STATE]
proof (prove)
using this:
keys (lead_monom p) \<subseteq> vars p

goal (1 subgoal):
 1. vars (MPoly_Type.monom (restrictpm (- A) (lead_monom p)) (Symmetric_Polynomials.lead_coeff p)) \<subseteq> vars p - A
[PROOF STEP]
by (intro order.trans[OF vars_monom_subset]) auto


[STATEMENT]
lemma keys_fund_sym_step_monom: "keys (fund_sym_step_monom p) \<subseteq> {1..n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. keys (local.fund_sym_step_monom p) \<subseteq> {1..n}
[PROOF STEP]
unfolding fund_sym_step_monom_def Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. keys (\<Sum>i<n. Poly_Mapping.single (Suc i) ((if i < n then lookup (lead_monom p) (f i) else 0) - (if Suc i < n then lookup (lead_monom p) (f (Suc i)) else 0))) \<subseteq> {1..n}
[PROOF STEP]
by (intro order.trans[OF keys_sum] UN_least, subst keys_single) auto


[STATEMENT]
lemma coeff_fund_sym_step_poly:
  assumes C: "\<forall>m. coeff p m \<in> C" and "ring_closed C"
  shows   "coeff (fund_sym_step_poly p) m \<in> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MPoly_Type.coeff (local.fund_sym_step_poly p) m \<in> C
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. MPoly_Type.coeff (local.fund_sym_step_poly p) m \<in> C
[PROOF STEP]
interpret ring_closed C
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring_closed C
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. MPoly_Type.coeff (local.fund_sym_step_poly p) m \<in> C
[PROOF STEP]
have *: "\<And>m. coeff (p ^ x) m \<in> C" if "\<And>m. coeff p m \<in> C"  for p x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m. MPoly_Type.coeff (p ^ x) m \<in> C
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
MPoly_Type.coeff p ?m \<in> C

goal (1 subgoal):
 1. \<And>m. MPoly_Type.coeff (p ^ x) m \<in> C
[PROOF STEP]
by (induction x)
                  (auto simp: coeff_mpoly_times mpoly_coeff_1 intro!: prod_fun_closed)
[PROOF STATE]
proof (state)
this:
(\<And>m. MPoly_Type.coeff ?p1 m \<in> C) \<Longrightarrow> MPoly_Type.coeff (?p1 ^ ?x1) ?m \<in> C

goal (1 subgoal):
 1. MPoly_Type.coeff (local.fund_sym_step_poly p) m \<in> C
[PROOF STEP]
have **: "\<And>m. coeff (prod f X) m \<in> C" if "\<And>i m. i \<in> X \<Longrightarrow> coeff (f i) m \<in> C"
    for X and f :: "nat \<Rightarrow> _"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m. MPoly_Type.coeff (prod f X) m \<in> C
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
?i \<in> X \<Longrightarrow> MPoly_Type.coeff (f ?i) ?m \<in> C

goal (1 subgoal):
 1. \<And>m. MPoly_Type.coeff (prod f X) m \<in> C
[PROOF STEP]
by (induction X rule: infinite_finite_induct)
                  (auto simp: coeff_mpoly_times mpoly_coeff_1 intro!: prod_fun_closed)
[PROOF STATE]
proof (state)
this:
(\<And>i m. i \<in> ?X1 \<Longrightarrow> MPoly_Type.coeff (?f1 i) m \<in> C) \<Longrightarrow> MPoly_Type.coeff (prod ?f1 ?X1) ?m \<in> C

goal (1 subgoal):
 1. MPoly_Type.coeff (local.fund_sym_step_poly p) m \<in> C
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MPoly_Type.coeff (local.fund_sym_step_poly p) m \<in> C
[PROOF STEP]
using C
[PROOF STATE]
proof (prove)
using this:
\<forall>m. MPoly_Type.coeff p m \<in> C

goal (1 subgoal):
 1. MPoly_Type.coeff (local.fund_sym_step_poly p) m \<in> C
[PROOF STEP]
unfolding fund_sym_step_poly_def Let_def fund_sym_step_coeff_def coeff_mpoly_times
[PROOF STATE]
proof (prove)
using this:
\<forall>m. MPoly_Type.coeff p m \<in> C

goal (1 subgoal):
 1. prod_fun (MPoly_Type.coeff (MPoly_Type.monom (restrictpm (- A) (lead_monom p)) (Symmetric_Polynomials.lead_coeff p))) (MPoly_Type.coeff (\<Prod>i<n. sym_mpoly A (Suc i) ^ ((if i < n then lookup (lead_monom p) (f i) else 0) - (if Suc i < n then lookup (lead_monom p) (f (Suc i)) else 0)))) m \<in> C
[PROOF STEP]
by (intro prod_fun_closed)
       (auto simp: coeff_monom when_def lead_coeff_def coeff_sym_mpoly intro!: * **)
[PROOF STATE]
proof (state)
this:
MPoly_Type.coeff (local.fund_sym_step_poly p) m \<in> C

goal:
No subgoals!
[PROOF STEP]
qed