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

goal (1 subgoal):
 1. vars (mpoly_map_vars f p) = f ` vars p
[PROOF STEP]
unfolding vars_def
[PROOF STATE]
proof (prove)
using this:
bij f

goal (1 subgoal):
 1. \<Union> (keys ` keys (mapping_of (mpoly_map_vars f p))) = f ` \<Union> (keys ` keys (mapping_of p))
[PROOF STEP]
proof transfer'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f p. bij f \<Longrightarrow> \<Union> (keys ` keys (permutep (permutep f) p)) = f ` \<Union> (keys ` keys p)
[PROOF STEP]
fix f :: "nat \<Rightarrow> nat" and p :: "(nat \<Rightarrow>\<^sub>0 nat) \<Rightarrow>\<^sub>0 'a"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f p. bij f \<Longrightarrow> \<Union> (keys ` keys (permutep (permutep f) p)) = f ` \<Union> (keys ` keys p)
[PROOF STEP]
assume f: "bij f"
[PROOF STATE]
proof (state)
this:
bij f

goal (1 subgoal):
 1. \<And>f p. bij f \<Longrightarrow> \<Union> (keys ` keys (permutep (permutep f) p)) = f ` \<Union> (keys ` keys p)
[PROOF STEP]
have eq: "f (inv_into UNIV f x) = x" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (inv f x) = x
[PROOF STEP]
using f
[PROOF STATE]
proof (prove)
using this:
bij f

goal (1 subgoal):
 1. f (inv f x) = x
[PROOF STEP]
by (subst surj_f_inv_f[of f]) (auto simp: bij_is_surj)
[PROOF STATE]
proof (state)
this:
f (inv f ?x) = ?x

goal (1 subgoal):
 1. \<And>f p. bij f \<Longrightarrow> \<Union> (keys ` keys (permutep (permutep f) p)) = f ` \<Union> (keys ` keys p)
[PROOF STEP]
show "\<Union> (keys ` keys (permutep (permutep f) p)) = f ` \<Union> (keys ` keys p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (keys ` keys (permutep (permutep f) p)) = f ` \<Union> (keys ` keys p)
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>xa \<in> keys (permutep (permutep f) p); x \<in> keys xa\<rbrakk> \<Longrightarrow> x \<in> f ` \<Union> (keys ` keys p)
 2. \<And>x xa xb. \<lbrakk>xb \<in> keys p; xa \<in> keys xb\<rbrakk> \<Longrightarrow> f xa \<in> \<Union> (keys ` keys (permutep (permutep f) p))
[PROOF STEP]
fix m x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>xa \<in> keys (permutep (permutep f) p); x \<in> keys xa\<rbrakk> \<Longrightarrow> x \<in> f ` \<Union> (keys ` keys p)
 2. \<And>x xa xb. \<lbrakk>xb \<in> keys p; xa \<in> keys xb\<rbrakk> \<Longrightarrow> f xa \<in> \<Union> (keys ` keys (permutep (permutep f) p))
[PROOF STEP]
assume mx: "m \<in> keys (permutep (permutep f) p)" "x \<in> keys m"
[PROOF STATE]
proof (state)
this:
m \<in> keys (permutep (permutep f) p)
x \<in> keys m

goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>xa \<in> keys (permutep (permutep f) p); x \<in> keys xa\<rbrakk> \<Longrightarrow> x \<in> f ` \<Union> (keys ` keys p)
 2. \<And>x xa xb. \<lbrakk>xb \<in> keys p; xa \<in> keys xb\<rbrakk> \<Longrightarrow> f xa \<in> \<Union> (keys ` keys (permutep (permutep f) p))
[PROOF STEP]
from mx
[PROOF STATE]
proof (chain)
picking this:
m \<in> keys (permutep (permutep f) p)
x \<in> keys m
[PROOF STEP]
have "permutep f m \<in> keys p"
[PROOF STATE]
proof (prove)
using this:
m \<in> keys (permutep (permutep f) p)
x \<in> keys m

goal (1 subgoal):
 1. permutep f m \<in> keys p
[PROOF STEP]
by (auto simp: keys_permutep bij_permutep f)
[PROOF STATE]
proof (state)
this:
permutep f m \<in> keys p

goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>xa \<in> keys (permutep (permutep f) p); x \<in> keys xa\<rbrakk> \<Longrightarrow> x \<in> f ` \<Union> (keys ` keys p)
 2. \<And>x xa xb. \<lbrakk>xb \<in> keys p; xa \<in> keys xb\<rbrakk> \<Longrightarrow> f xa \<in> \<Union> (keys ` keys (permutep (permutep f) p))
[PROOF STEP]
with mx
[PROOF STATE]
proof (chain)
picking this:
m \<in> keys (permutep (permutep f) p)
x \<in> keys m
permutep f m \<in> keys p
[PROOF STEP]
have "f (inv_into UNIV f x) \<in> f ` (\<Union>m\<in>keys p. keys m)"
[PROOF STATE]
proof (prove)
using this:
m \<in> keys (permutep (permutep f) p)
x \<in> keys m
permutep f m \<in> keys p

goal (1 subgoal):
 1. f (inv f x) \<in> f ` \<Union> (keys ` keys p)
[PROOF STEP]
by (intro imageI) (auto intro!: bexI[of _ "permutep f m"] simp: keys_permutep f eq)
[PROOF STATE]
proof (state)
this:
f (inv f x) \<in> f ` \<Union> (keys ` keys p)

goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>xa \<in> keys (permutep (permutep f) p); x \<in> keys xa\<rbrakk> \<Longrightarrow> x \<in> f ` \<Union> (keys ` keys p)
 2. \<And>x xa xb. \<lbrakk>xb \<in> keys p; xa \<in> keys xb\<rbrakk> \<Longrightarrow> f xa \<in> \<Union> (keys ` keys (permutep (permutep f) p))
[PROOF STEP]
with eq
[PROOF STATE]
proof (chain)
picking this:
f (inv f ?x) = ?x
f (inv f x) \<in> f ` \<Union> (keys ` keys p)
[PROOF STEP]
show "x \<in> f ` (\<Union>m\<in>keys p. keys m)"
[PROOF STATE]
proof (prove)
using this:
f (inv f ?x) = ?x
f (inv f x) \<in> f ` \<Union> (keys ` keys p)

goal (1 subgoal):
 1. x \<in> f ` \<Union> (keys ` keys p)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<in> f ` \<Union> (keys ` keys p)

goal (1 subgoal):
 1. \<And>x xa xb. \<lbrakk>xb \<in> keys p; xa \<in> keys xb\<rbrakk> \<Longrightarrow> f xa \<in> \<Union> (keys ` keys (permutep (permutep f) p))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa xb. \<lbrakk>xb \<in> keys p; xa \<in> keys xb\<rbrakk> \<Longrightarrow> f xa \<in> \<Union> (keys ` keys (permutep (permutep f) p))
[PROOF STEP]
fix m x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa xb. \<lbrakk>xb \<in> keys p; xa \<in> keys xb\<rbrakk> \<Longrightarrow> f xa \<in> \<Union> (keys ` keys (permutep (permutep f) p))
[PROOF STEP]
assume mx: "m \<in> keys p" "x \<in> keys m"
[PROOF STATE]
proof (state)
this:
m \<in> keys p
x \<in> keys m

goal (1 subgoal):
 1. \<And>x xa xb. \<lbrakk>xb \<in> keys p; xa \<in> keys xb\<rbrakk> \<Longrightarrow> f xa \<in> \<Union> (keys ` keys (permutep (permutep f) p))
[PROOF STEP]
from mx
[PROOF STATE]
proof (chain)
picking this:
m \<in> keys p
x \<in> keys m
[PROOF STEP]
have "permutep id m \<in> keys p"
[PROOF STATE]
proof (prove)
using this:
m \<in> keys p
x \<in> keys m

goal (1 subgoal):
 1. permutep id m \<in> keys p
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
permutep id m \<in> keys p

goal (1 subgoal):
 1. \<And>x xa xb. \<lbrakk>xb \<in> keys p; xa \<in> keys xb\<rbrakk> \<Longrightarrow> f xa \<in> \<Union> (keys ` keys (permutep (permutep f) p))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
permutep id m \<in> keys p

goal (1 subgoal):
 1. \<And>x xa xb. \<lbrakk>xb \<in> keys p; xa \<in> keys xb\<rbrakk> \<Longrightarrow> f xa \<in> \<Union> (keys ` keys (permutep (permutep f) p))
[PROOF STEP]
have "id = inv_into UNIV f \<circ> f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. id = inv f \<circ> f
[PROOF STEP]
using f
[PROOF STATE]
proof (prove)
using this:
bij f

goal (1 subgoal):
 1. id = inv f \<circ> f
[PROOF STEP]
by (intro ext) (auto simp: bij_is_inj inv_f_f)
[PROOF STATE]
proof (state)
this:
id = inv f \<circ> f

goal (1 subgoal):
 1. \<And>x xa xb. \<lbrakk>xb \<in> keys p; xa \<in> keys xb\<rbrakk> \<Longrightarrow> f xa \<in> \<Union> (keys ` keys (permutep (permutep f) p))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
id = inv f \<circ> f

goal (1 subgoal):
 1. \<And>x xa xb. \<lbrakk>xb \<in> keys p; xa \<in> keys xb\<rbrakk> \<Longrightarrow> f xa \<in> \<Union> (keys ` keys (permutep (permutep f) p))
[PROOF STEP]
have "permutep \<dots> m = permutep f (permutep (inv_into UNIV f) m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. permutep (inv f \<circ> f) m = permutep f (permutep (inv f) m)
[PROOF STEP]
by (simp add: permutep_comp f bij_imp_bij_inv)
[PROOF STATE]
proof (state)
this:
permutep (inv f \<circ> f) m = permutep f (permutep (inv f) m)

goal (1 subgoal):
 1. \<And>x xa xb. \<lbrakk>xb \<in> keys p; xa \<in> keys xb\<rbrakk> \<Longrightarrow> f xa \<in> \<Union> (keys ` keys (permutep (permutep f) p))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
permutep f (permutep (inv f) m) \<in> keys p
[PROOF STEP]
have **: "permutep f (permutep (inv_into UNIV f) m) \<in> keys p"
[PROOF STATE]
proof (prove)
using this:
permutep f (permutep (inv f) m) \<in> keys p

goal (1 subgoal):
 1. permutep f (permutep (inv f) m) \<in> keys p
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
permutep f (permutep (inv f) m) \<in> keys p

goal (1 subgoal):
 1. \<And>x xa xb. \<lbrakk>xb \<in> keys p; xa \<in> keys xb\<rbrakk> \<Longrightarrow> f xa \<in> \<Union> (keys ` keys (permutep (permutep f) p))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
permutep f (permutep (inv f) m) \<in> keys p

goal (1 subgoal):
 1. \<And>x xa xb. \<lbrakk>xb \<in> keys p; xa \<in> keys xb\<rbrakk> \<Longrightarrow> f xa \<in> \<Union> (keys ` keys (permutep (permutep f) p))
[PROOF STEP]
from f mx
[PROOF STATE]
proof (chain)
picking this:
bij f
m \<in> keys p
x \<in> keys m
[PROOF STEP]
have "f x \<in> keys (permutep (inv_into UNIV f) m)"
[PROOF STATE]
proof (prove)
using this:
bij f
m \<in> keys p
x \<in> keys m

goal (1 subgoal):
 1. f x \<in> keys (permutep (inv f) m)
[PROOF STEP]
by (auto simp: keys_permutep bij_imp_bij_inv inv_f_f bij_is_inj)
[PROOF STATE]
proof (state)
this:
f x \<in> keys (permutep (inv f) m)

goal (1 subgoal):
 1. \<And>x xa xb. \<lbrakk>xb \<in> keys p; xa \<in> keys xb\<rbrakk> \<Longrightarrow> f xa \<in> \<Union> (keys ` keys (permutep (permutep f) p))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
permutep f (permutep (inv f) m) \<in> keys p
f x \<in> keys (permutep (inv f) m)
[PROOF STEP]
show "f x \<in> \<Union> (keys ` keys (permutep (permutep f) p))"
[PROOF STATE]
proof (prove)
using this:
permutep f (permutep (inv f) m) \<in> keys p
f x \<in> keys (permutep (inv f) m)

goal (1 subgoal):
 1. f x \<in> \<Union> (keys ` keys (permutep (permutep f) p))
[PROOF STEP]
using f
[PROOF STATE]
proof (prove)
using this:
permutep f (permutep (inv f) m) \<in> keys p
f x \<in> keys (permutep (inv f) m)
bij f

goal (1 subgoal):
 1. f x \<in> \<Union> (keys ` keys (permutep (permutep f) p))
[PROOF STEP]
by (auto simp: keys_permutep bij_permutep)
[PROOF STATE]
proof (state)
this:
f x \<in> \<Union> (keys ` keys (permutep (permutep f) p))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Union> (keys ` keys (permutep (permutep f) p)) = f ` \<Union> (keys ` keys p)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma permutep_eq_monom_of_set_iff [simp]:
  assumes "bij f"
  shows   "permutep f mon = monom_of_set A \<longleftrightarrow> mon = monom_of_set (f ` A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (permutep f mon = monom_of_set A) = (mon = monom_of_set (f ` A))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. permutep f mon = monom_of_set A \<Longrightarrow> mon = monom_of_set (f ` A)
 2. mon = monom_of_set (f ` A) \<Longrightarrow> permutep f mon = monom_of_set A
[PROOF STEP]
assume eq: "permutep f mon = monom_of_set A"
[PROOF STATE]
proof (state)
this:
permutep f mon = monom_of_set A

goal (2 subgoals):
 1. permutep f mon = monom_of_set A \<Longrightarrow> mon = monom_of_set (f ` A)
 2. mon = monom_of_set (f ` A) \<Longrightarrow> permutep f mon = monom_of_set A
[PROOF STEP]
have "permutep (inv_into UNIV f) (permutep f mon) = monom_of_set (inv_into UNIV f -` A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. permutep (inv f) (permutep f mon) = monom_of_set (inv f -` A)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
bij f

goal (1 subgoal):
 1. permutep (inv f) (permutep f mon) = monom_of_set (inv f -` A)
[PROOF STEP]
by (simp add: eq bij_imp_bij_inv assms permutep_monom_of_set)
[PROOF STATE]
proof (state)
this:
permutep (inv f) (permutep f mon) = monom_of_set (inv f -` A)

goal (2 subgoals):
 1. permutep f mon = monom_of_set A \<Longrightarrow> mon = monom_of_set (f ` A)
 2. mon = monom_of_set (f ` A) \<Longrightarrow> permutep f mon = monom_of_set A
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
permutep (inv f) (permutep f mon) = monom_of_set (inv f -` A)

goal (2 subgoals):
 1. permutep f mon = monom_of_set A \<Longrightarrow> mon = monom_of_set (f ` A)
 2. mon = monom_of_set (f ` A) \<Longrightarrow> permutep f mon = monom_of_set A
[PROOF STEP]
have "inv_into UNIV f -` A = f ` A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv f -` A = f ` A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
bij f

goal (1 subgoal):
 1. inv f -` A = f ` A
[PROOF STEP]
by (force simp: bij_is_surj image_iff inv_f_f bij_is_inj surj_f_inv_f)
[PROOF STATE]
proof (state)
this:
inv f -` A = f ` A

goal (2 subgoals):
 1. permutep f mon = monom_of_set A \<Longrightarrow> mon = monom_of_set (f ` A)
 2. mon = monom_of_set (f ` A) \<Longrightarrow> permutep f mon = monom_of_set A
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
inv f -` A = f ` A

goal (2 subgoals):
 1. permutep f mon = monom_of_set A \<Longrightarrow> mon = monom_of_set (f ` A)
 2. mon = monom_of_set (f ` A) \<Longrightarrow> permutep f mon = monom_of_set A
[PROOF STEP]
have "permutep (inv_into UNIV f) (permutep f mon) = permutep (f \<circ> inv_into UNIV f) mon"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. permutep (inv f) (permutep f mon) = permutep (f \<circ> inv f) mon
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
bij f

goal (1 subgoal):
 1. permutep (inv f) (permutep f mon) = permutep (f \<circ> inv f) mon
[PROOF STEP]
by (simp add: permutep_comp bij_imp_bij_inv)
[PROOF STATE]
proof (state)
this:
permutep (inv f) (permutep f mon) = permutep (f \<circ> inv f) mon

goal (2 subgoals):
 1. permutep f mon = monom_of_set A \<Longrightarrow> mon = monom_of_set (f ` A)
 2. mon = monom_of_set (f ` A) \<Longrightarrow> permutep f mon = monom_of_set A
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
permutep (inv f) (permutep f mon) = permutep (f \<circ> inv f) mon

goal (2 subgoals):
 1. permutep f mon = monom_of_set A \<Longrightarrow> mon = monom_of_set (f ` A)
 2. mon = monom_of_set (f ` A) \<Longrightarrow> permutep f mon = monom_of_set A
[PROOF STEP]
have "f \<circ> inv_into UNIV f = id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<circ> inv f = id
[PROOF STEP]
by (subst surj_iff [symmetric]) (insert assms, auto simp: bij_is_surj)
[PROOF STATE]
proof (state)
this:
f \<circ> inv f = id

goal (2 subgoals):
 1. permutep f mon = monom_of_set A \<Longrightarrow> mon = monom_of_set (f ` A)
 2. mon = monom_of_set (f ` A) \<Longrightarrow> permutep f mon = monom_of_set A
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
permutep id mon = monom_of_set (f ` A)
[PROOF STEP]
show "mon = monom_of_set (f ` A)"
[PROOF STATE]
proof (prove)
using this:
permutep id mon = monom_of_set (f ` A)

goal (1 subgoal):
 1. mon = monom_of_set (f ` A)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
mon = monom_of_set (f ` A)

goal (1 subgoal):
 1. mon = monom_of_set (f ` A) \<Longrightarrow> permutep f mon = monom_of_set A
[PROOF STEP]
qed (insert assms, auto simp: permutep_monom_of_set inj_vimage_image_eq bij_is_inj)


[STATEMENT]
lemma permutep_monom_of_set_permutes [simp]:
  assumes "\<pi> permutes A"
  shows   "permutep \<pi> (monom_of_set A) = monom_of_set A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. permutep \<pi> (monom_of_set A) = monom_of_set A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<pi> permutes A

goal (1 subgoal):
 1. permutep \<pi> (monom_of_set A) = monom_of_set A
[PROOF STEP]
by transfer (auto simp: if_splits fun_eq_iff permutes_in_image)


[STATEMENT]
lemma mpoly_map_vars_0 [simp]: "mpoly_map_vars f 0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mpoly_map_vars f 0 = 0
[PROOF STEP]
by (transfer, transfer') (simp add: o_def)


[STATEMENT]
lemma permutep_eq_0_iff [simp]: "permutep f m = 0 \<longleftrightarrow> m = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (permutep f m = 0) = (m = 0)
[PROOF STEP]
proof transfer
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f m. finite {x. m x \<noteq> (0::'b)} \<Longrightarrow> ((if bij f then m \<circ> f else m) = (\<lambda>k. 0::'b)) = (m = (\<lambda>k. 0::'b))
[PROOF STEP]
fix f :: "'a \<Rightarrow> 'a" and m :: "'a \<Rightarrow> 'b"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f m. finite {x. m x \<noteq> (0::'b)} \<Longrightarrow> ((if bij f then m \<circ> f else m) = (\<lambda>k. 0::'b)) = (m = (\<lambda>k. 0::'b))
[PROOF STEP]
assume "finite {x. m x \<noteq> 0}"
[PROOF STATE]
proof (state)
this:
finite {x. m x \<noteq> (0::'b)}

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

goal (2 subgoals):
 1. bij f \<Longrightarrow> ((if bij f then m \<circ> f else m) = (\<lambda>k. 0::'b)) = (m = (\<lambda>k. 0::'b))
 2. \<not> bij f \<Longrightarrow> ((if bij f then m \<circ> f else m) = (\<lambda>k. 0::'b)) = (m = (\<lambda>k. 0::'b))
[PROOF STEP]
hence "(\<forall>x. m (f x) = 0) \<longleftrightarrow> (\<forall>x. m x = 0)"
[PROOF STATE]
proof (prove)
using this:
bij f

goal (1 subgoal):
 1. (\<forall>x. m (f x) = (0::'b)) = (\<forall>x. m x = (0::'b))
[PROOF STEP]
using bij_iff[of f]
[PROOF STATE]
proof (prove)
using this:
bij f
bij f = (\<forall>x. \<exists>!y. f y = x)

goal (1 subgoal):
 1. (\<forall>x. m (f x) = (0::'b)) = (\<forall>x. m x = (0::'b))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(\<forall>x. m (f x) = (0::'b)) = (\<forall>x. m x = (0::'b))

goal (2 subgoals):
 1. bij f \<Longrightarrow> ((if bij f then m \<circ> f else m) = (\<lambda>k. 0::'b)) = (m = (\<lambda>k. 0::'b))
 2. \<not> bij f \<Longrightarrow> ((if bij f then m \<circ> f else m) = (\<lambda>k. 0::'b)) = (m = (\<lambda>k. 0::'b))
[PROOF STEP]
with True
[PROOF STATE]
proof (chain)
picking this:
bij f
(\<forall>x. m (f x) = (0::'b)) = (\<forall>x. m x = (0::'b))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
bij f
(\<forall>x. m (f x) = (0::'b)) = (\<forall>x. m x = (0::'b))

goal (1 subgoal):
 1. ((if bij f then m \<circ> f else m) = (\<lambda>k. 0::'b)) = (m = (\<lambda>k. 0::'b))
[PROOF STEP]
by (auto simp: fun_eq_iff)
[PROOF STATE]
proof (state)
this:
((if bij f then m \<circ> f else m) = (\<lambda>k. 0::'b)) = (m = (\<lambda>k. 0::'b))

goal (1 subgoal):
 1. \<not> bij f \<Longrightarrow> ((if bij f then m \<circ> f else m) = (\<lambda>k. 0::'b)) = (m = (\<lambda>k. 0::'b))
[PROOF STEP]
qed (auto simp: fun_eq_iff)
[PROOF STATE]
proof (state)
this:
((if bij f then m \<circ> f else m) = (\<lambda>k. 0::'b)) = (m = (\<lambda>k. 0::'b))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mpoly_map_vars_1 [simp]: "mpoly_map_vars f 1 = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mpoly_map_vars f 1 = 1
[PROOF STEP]
by (transfer, transfer') (auto simp: o_def fun_eq_iff when_def)


[STATEMENT]
lemma permutep_Const\<^sub>0 [simp]: "(\<And>x. f x = 0 \<longleftrightarrow> x = 0) \<Longrightarrow> permutep f (Const\<^sub>0 c) = Const\<^sub>0 c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. (f x = 0) = (x = 0)) \<Longrightarrow> permutep f (Const\<^sub>0 c) = Const\<^sub>0 c
[PROOF STEP]
unfolding Const\<^sub>0_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. (f x = 0) = (x = 0)) \<Longrightarrow> permutep f (Poly_Mapping.single 0 c) = Poly_Mapping.single 0 c
[PROOF STEP]
by transfer' (auto simp: when_def fun_eq_iff)


[STATEMENT]
lemma permutep_add [simp]: "permutep f (m1 + m2) = permutep f m1 + permutep f m2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. permutep f (m1 + m2) = permutep f m1 + permutep f m2
[PROOF STEP]
unfolding Const\<^sub>0_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. permutep f (m1 + m2) = permutep f m1 + permutep f m2
[PROOF STEP]
by transfer' (auto simp: when_def fun_eq_iff)


[STATEMENT]
lemma permutep_diff [simp]: "permutep f (m1 - m2) = permutep f m1 - permutep f m2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. permutep f (m1 - m2) = permutep f m1 - permutep f m2
[PROOF STEP]
unfolding Const\<^sub>0_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. permutep f (m1 - m2) = permutep f m1 - permutep f m2
[PROOF STEP]
by transfer' (auto simp: when_def fun_eq_iff)


[STATEMENT]
lemma permutep_uminus [simp]: "permutep f (-m) = -permutep f m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. permutep f (- m) = - permutep f m
[PROOF STEP]
unfolding Const\<^sub>0_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. permutep f (- m) = - permutep f m
[PROOF STEP]
by transfer' (auto simp: when_def fun_eq_iff)


[STATEMENT]
lemma permutep_mult [simp]:
  "(\<And>x y. f (x + y) = f x + f y) \<Longrightarrow> permutep f (m1 * m2) = permutep f m1 * permutep f m2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x y. f (x + y) = f x + f y) \<Longrightarrow> permutep f (m1 * m2) = permutep f m1 * permutep f m2
[PROOF STEP]
unfolding Const\<^sub>0_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x y. f (x + y) = f x + f y) \<Longrightarrow> permutep f (m1 * m2) = permutep f m1 * permutep f m2
[PROOF STEP]
by transfer' (auto simp: when_def fun_eq_iff prod_fun_compose_bij)


[STATEMENT]
lemma mpoly_map_vars_Const [simp]: "mpoly_map_vars f (Const c) = Const c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mpoly_map_vars f (Const c) = Const c
[PROOF STEP]
by transfer (auto simp: o_def fun_eq_iff when_def)


[STATEMENT]
lemma mpoly_map_vars_add [simp]: "mpoly_map_vars f (p + q) = mpoly_map_vars f p + mpoly_map_vars f q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mpoly_map_vars f (p + q) = mpoly_map_vars f p + mpoly_map_vars f q
[PROOF STEP]
by transfer simp


[STATEMENT]
lemma mpoly_map_vars_diff [simp]: "mpoly_map_vars f (p - q) = mpoly_map_vars f p - mpoly_map_vars f q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mpoly_map_vars f (p - q) = mpoly_map_vars f p - mpoly_map_vars f q
[PROOF STEP]
by transfer simp


[STATEMENT]
lemma mpoly_map_vars_uminus [simp]: "mpoly_map_vars f (-p) = -mpoly_map_vars f p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mpoly_map_vars f (- p) = - mpoly_map_vars f p
[PROOF STEP]
by transfer simp


[STATEMENT]
lemma permutep_smult:
  "permutep (permutep f) (Poly_Mapping.map ((*) c) p) =
     Poly_Mapping.map ((*) c) (permutep (permutep f) p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. permutep (permutep f) (Poly_Mapping.map ((*) c) p) = Poly_Mapping.map ((*) c) (permutep (permutep f) p)
[PROOF STEP]
by transfer' (auto split: if_splits simp: fun_eq_iff)


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


[STATEMENT]
lemma mpoly_map_vars_prod [simp]: "mpoly_map_vars f (prod g A) = (\<Prod>x\<in>A. mpoly_map_vars f (g x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mpoly_map_vars f (prod g A) = (\<Prod>x\<in>A. mpoly_map_vars f (g x))
[PROOF STEP]
by (induction A rule: infinite_finite_induct) auto


[STATEMENT]
lemma permutep_eq_iff [simp]: "permutep f p = permutep f q \<longleftrightarrow> p = q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (permutep f p = permutep f q) = (p = q)
[PROOF STEP]
by transfer (auto simp: comp_bij_eq_iff)


[STATEMENT]
lemma mpoly_map_vars_Sum_any [simp]:
  "mpoly_map_vars f (Sum_any g) = Sum_any (\<lambda>x. mpoly_map_vars f (g x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mpoly_map_vars f (Sum_any g) = (\<Sum>x. mpoly_map_vars f (g x))
[PROOF STEP]
by (simp add: Sum_any.expand_set)


[STATEMENT]
lemma mpoly_map_vars_power [simp]: "mpoly_map_vars f (p ^ n) = mpoly_map_vars f p ^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mpoly_map_vars f (p ^ n) = mpoly_map_vars f p ^ n
[PROOF STEP]
by (induction n) auto


[STATEMENT]
lemma mpoly_map_vars_monom_single [simp]:
  assumes "bij f"
  shows   "mpoly_map_vars f (monom (Poly_Mapping.single i n) c) =
             monom (Poly_Mapping.single (f i) n) c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mpoly_map_vars f (MPoly_Type.monom (Poly_Mapping.single i n) c) = MPoly_Type.monom (Poly_Mapping.single (f i) n) c
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
bij f

goal (1 subgoal):
 1. mpoly_map_vars f (MPoly_Type.monom (Poly_Mapping.single i n) c) = MPoly_Type.monom (Poly_Mapping.single (f i) n) c
[PROOF STEP]
by (simp add: mpoly_map_vars_monom permutep_single bij_imp_bij_inv inv_inv_eq)


[STATEMENT]
lemma insertion_mpoly_map_vars:
  assumes "bij f"
  shows   "insertion g (mpoly_map_vars f p) = insertion (g \<circ> f) p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion g (mpoly_map_vars f p) = insertion (g \<circ> f) p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. insertion g (mpoly_map_vars f p) = insertion (g \<circ> f) p
[PROOF STEP]
have "insertion g (mpoly_map_vars f p) =
          (\<Sum>m. coeff p (permutep f m) * (\<Prod>i. g i ^ lookup m i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion g (mpoly_map_vars f p) = (\<Sum>m. MPoly_Type.coeff p (permutep f m) * (\<Prod>i. g i ^ lookup m i))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
bij f

goal (1 subgoal):
 1. insertion g (mpoly_map_vars f p) = (\<Sum>m. MPoly_Type.coeff p (permutep f m) * (\<Prod>i. g i ^ lookup m i))
[PROOF STEP]
by (simp add: insertion_altdef coeff_mpoly_map_vars)
[PROOF STATE]
proof (state)
this:
insertion g (mpoly_map_vars f p) = (\<Sum>m. MPoly_Type.coeff p (permutep f m) * (\<Prod>i. g i ^ lookup m i))

goal (1 subgoal):
 1. insertion g (mpoly_map_vars f p) = insertion (g \<circ> f) p
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
insertion g (mpoly_map_vars f p) = (\<Sum>m. MPoly_Type.coeff p (permutep f m) * (\<Prod>i. g i ^ lookup m i))

goal (1 subgoal):
 1. insertion g (mpoly_map_vars f p) = insertion (g \<circ> f) p
[PROOF STEP]
have "\<dots> = Sum_any (\<lambda>m. coeff p (permutep f m) *
                    Prod_any (\<lambda>i. g (f i) ^ lookup m (f i)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>m. MPoly_Type.coeff p (permutep f m) * (\<Prod>i. g i ^ lookup m i)) = (\<Sum>m. MPoly_Type.coeff p (permutep f m) * (\<Prod>i. g (f i) ^ lookup m (f i)))
[PROOF STEP]
by (intro Sum_any.cong arg_cong[where ?f = "\<lambda>y. x * y" for x]
          Prod_any.reindex_cong[OF assms]) (auto simp: o_def)
[PROOF STATE]
proof (state)
this:
(\<Sum>m. MPoly_Type.coeff p (permutep f m) * (\<Prod>i. g i ^ lookup m i)) = (\<Sum>m. MPoly_Type.coeff p (permutep f m) * (\<Prod>i. g (f i) ^ lookup m (f i)))

goal (1 subgoal):
 1. insertion g (mpoly_map_vars f p) = insertion (g \<circ> f) p
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>m. MPoly_Type.coeff p (permutep f m) * (\<Prod>i. g i ^ lookup m i)) = (\<Sum>m. MPoly_Type.coeff p (permutep f m) * (\<Prod>i. g (f i) ^ lookup m (f i)))

goal (1 subgoal):
 1. insertion g (mpoly_map_vars f p) = insertion (g \<circ> f) p
[PROOF STEP]
have "\<dots> = Sum_any (\<lambda>m. coeff p m * (\<Prod>i. g (f i) ^ lookup m i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>m. MPoly_Type.coeff p (permutep f m) * (\<Prod>i. g (f i) ^ lookup m (f i))) = (\<Sum>m. MPoly_Type.coeff p m * (\<Prod>i. g (f i) ^ lookup m i))
[PROOF STEP]
by (intro Sum_any.reindex_cong [OF bij_permutep[of f], symmetric])
       (auto simp: o_def lookup_permutep assms)
[PROOF STATE]
proof (state)
this:
(\<Sum>m. MPoly_Type.coeff p (permutep f m) * (\<Prod>i. g (f i) ^ lookup m (f i))) = (\<Sum>m. MPoly_Type.coeff p m * (\<Prod>i. g (f i) ^ lookup m i))

goal (1 subgoal):
 1. insertion g (mpoly_map_vars f p) = insertion (g \<circ> f) p
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>m. MPoly_Type.coeff p (permutep f m) * (\<Prod>i. g (f i) ^ lookup m (f i))) = (\<Sum>m. MPoly_Type.coeff p m * (\<Prod>i. g (f i) ^ lookup m i))

goal (1 subgoal):
 1. insertion g (mpoly_map_vars f p) = insertion (g \<circ> f) p
[PROOF STEP]
have "\<dots> = insertion (g \<circ> f) p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>m. MPoly_Type.coeff p m * (\<Prod>i. g (f i) ^ lookup m i)) = insertion (g \<circ> f) p
[PROOF STEP]
by (simp add: insertion_altdef)
[PROOF STATE]
proof (state)
this:
(\<Sum>m. MPoly_Type.coeff p m * (\<Prod>i. g (f i) ^ lookup m i)) = insertion (g \<circ> f) p

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

goal (1 subgoal):
 1. insertion g (mpoly_map_vars f p) = insertion (g \<circ> f) p
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
insertion g (mpoly_map_vars f p) = insertion (g \<circ> f) p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma permutep_cong:
  assumes "f permutes (-keys p)" "g permutes (-keys p)" "p = q"
  shows   "permutep f p = permutep g q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. permutep f p = permutep g q
[PROOF STEP]
proof (intro poly_mapping_eqI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. lookup (permutep f p) k = lookup (permutep g q) k
[PROOF STEP]
fix k :: 'a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. lookup (permutep f p) k = lookup (permutep g q) k
[PROOF STEP]
show "lookup (permutep f p) k = lookup (permutep g q) k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup (permutep f p) k = lookup (permutep g q) k
[PROOF STEP]
proof (cases "k \<in> keys p")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. k \<in> keys p \<Longrightarrow> lookup (permutep f p) k = lookup (permutep g q) k
 2. k \<notin> keys p \<Longrightarrow> lookup (permutep f p) k = lookup (permutep g q) k
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
k \<notin> keys p

goal (2 subgoals):
 1. k \<in> keys p \<Longrightarrow> lookup (permutep f p) k = lookup (permutep g q) k
 2. k \<notin> keys p \<Longrightarrow> lookup (permutep f p) k = lookup (permutep g q) k
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
f permutes - keys p
g permutes - keys p
p = q
k \<notin> keys p
[PROOF STEP]
have "f k \<notin> keys p" "g k \<notin> keys p"
[PROOF STATE]
proof (prove)
using this:
f permutes - keys p
g permutes - keys p
p = q
k \<notin> keys p

goal (1 subgoal):
 1. f k \<notin> keys p &&& g k \<notin> keys p
[PROOF STEP]
using permutes_in_image[of _ "-keys p" k]
[PROOF STATE]
proof (prove)
using this:
f permutes - keys p
g permutes - keys p
p = q
k \<notin> keys p
?p permutes - keys p \<Longrightarrow> (?p k \<in> - keys p) = (k \<in> - keys p)

goal (1 subgoal):
 1. f k \<notin> keys p &&& g k \<notin> keys p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f k \<notin> keys p
g k \<notin> keys p

goal (2 subgoals):
 1. k \<in> keys p \<Longrightarrow> lookup (permutep f p) k = lookup (permutep g q) k
 2. k \<notin> keys p \<Longrightarrow> lookup (permutep f p) k = lookup (permutep g q) k
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
f k \<notin> keys p
g k \<notin> keys p

goal (1 subgoal):
 1. lookup (permutep f p) k = lookup (permutep g q) k
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
f k \<notin> keys p
g k \<notin> keys p
f permutes - keys p
g permutes - keys p
p = q

goal (1 subgoal):
 1. lookup (permutep f p) k = lookup (permutep g q) k
[PROOF STEP]
by (auto simp: lookup_permutep permutes_bij in_keys_iff)
[PROOF STATE]
proof (state)
this:
lookup (permutep f p) k = lookup (permutep g q) k

goal (1 subgoal):
 1. k \<in> keys p \<Longrightarrow> lookup (permutep f p) k = lookup (permutep g q) k
[PROOF STEP]
qed (insert assms, auto simp: lookup_permutep permutes_bij permutes_not_in)
[PROOF STATE]
proof (state)
this:
lookup (permutep f p) k = lookup (permutep g q) k

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mpoly_map_vars_cong:
  assumes "f permutes (-vars p)" "g permutes (-vars q)" "p = q"
  shows   "mpoly_map_vars f p = mpoly_map_vars g (q :: 'a :: zero mpoly)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mpoly_map_vars f p = mpoly_map_vars g q
[PROOF STEP]
proof (intro mpoly_eqI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>mon. MPoly_Type.coeff (mpoly_map_vars f p) mon = MPoly_Type.coeff (mpoly_map_vars g q) mon
[PROOF STEP]
fix mon :: "nat \<Rightarrow>\<^sub>0 nat"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>mon. MPoly_Type.coeff (mpoly_map_vars f p) mon = MPoly_Type.coeff (mpoly_map_vars g q) mon
[PROOF STEP]
show "coeff (mpoly_map_vars f p) mon = coeff (mpoly_map_vars g q) mon"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MPoly_Type.coeff (mpoly_map_vars f p) mon = MPoly_Type.coeff (mpoly_map_vars g q) mon
[PROOF STEP]
proof (cases "keys mon \<subseteq> vars p")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. keys mon \<subseteq> vars p \<Longrightarrow> MPoly_Type.coeff (mpoly_map_vars f p) mon = MPoly_Type.coeff (mpoly_map_vars g q) mon
 2. \<not> keys mon \<subseteq> vars p \<Longrightarrow> MPoly_Type.coeff (mpoly_map_vars f p) mon = MPoly_Type.coeff (mpoly_map_vars g q) mon
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
keys mon \<subseteq> vars p

goal (2 subgoals):
 1. keys mon \<subseteq> vars p \<Longrightarrow> MPoly_Type.coeff (mpoly_map_vars f p) mon = MPoly_Type.coeff (mpoly_map_vars g q) mon
 2. \<not> keys mon \<subseteq> vars p \<Longrightarrow> MPoly_Type.coeff (mpoly_map_vars f p) mon = MPoly_Type.coeff (mpoly_map_vars g q) mon
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
f permutes - vars p
g permutes - vars q
p = q
keys mon \<subseteq> vars p
[PROOF STEP]
have "permutep f mon = permutep g mon"
[PROOF STATE]
proof (prove)
using this:
f permutes - vars p
g permutes - vars q
p = q
keys mon \<subseteq> vars p

goal (1 subgoal):
 1. permutep f mon = permutep g mon
[PROOF STEP]
by (intro permutep_cong assms(1,2)[THEN permutes_subset]) auto
[PROOF STATE]
proof (state)
this:
permutep f mon = permutep g mon

goal (2 subgoals):
 1. keys mon \<subseteq> vars p \<Longrightarrow> MPoly_Type.coeff (mpoly_map_vars f p) mon = MPoly_Type.coeff (mpoly_map_vars g q) mon
 2. \<not> keys mon \<subseteq> vars p \<Longrightarrow> MPoly_Type.coeff (mpoly_map_vars f p) mon = MPoly_Type.coeff (mpoly_map_vars g q) mon
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
permutep f mon = permutep g mon

goal (1 subgoal):
 1. MPoly_Type.coeff (mpoly_map_vars f p) mon = MPoly_Type.coeff (mpoly_map_vars g q) mon
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
permutep f mon = permutep g mon
f permutes - vars p
g permutes - vars q
p = q

goal (1 subgoal):
 1. MPoly_Type.coeff (mpoly_map_vars f p) mon = MPoly_Type.coeff (mpoly_map_vars g q) mon
[PROOF STEP]
by (simp add: coeff_mpoly_map_vars permutes_bij)
[PROOF STATE]
proof (state)
this:
MPoly_Type.coeff (mpoly_map_vars f p) mon = MPoly_Type.coeff (mpoly_map_vars g q) mon

goal (1 subgoal):
 1. \<not> keys mon \<subseteq> vars p \<Longrightarrow> MPoly_Type.coeff (mpoly_map_vars f p) mon = MPoly_Type.coeff (mpoly_map_vars g q) mon
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> keys mon \<subseteq> vars p \<Longrightarrow> MPoly_Type.coeff (mpoly_map_vars f p) mon = MPoly_Type.coeff (mpoly_map_vars g q) mon
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> keys mon \<subseteq> vars p

goal (1 subgoal):
 1. \<not> keys mon \<subseteq> vars p \<Longrightarrow> MPoly_Type.coeff (mpoly_map_vars f p) mon = MPoly_Type.coeff (mpoly_map_vars g q) mon
[PROOF STEP]
hence "\<not>(keys mon \<subseteq> f ` vars q)" "\<not>(keys mon \<subseteq> g ` vars q)"
[PROOF STATE]
proof (prove)
using this:
\<not> keys mon \<subseteq> vars p

goal (1 subgoal):
 1. \<not> keys mon \<subseteq> f ` vars q &&& \<not> keys mon \<subseteq> g ` vars q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<not> keys mon \<subseteq> vars p
f permutes - vars p
g permutes - vars q
p = q

goal (1 subgoal):
 1. \<not> keys mon \<subseteq> f ` vars q &&& \<not> keys mon \<subseteq> g ` vars q
[PROOF STEP]
by (auto simp: subset_iff permutes_not_in)
[PROOF STATE]
proof (state)
this:
\<not> keys mon \<subseteq> f ` vars q
\<not> keys mon \<subseteq> g ` vars q

goal (1 subgoal):
 1. \<not> keys mon \<subseteq> vars p \<Longrightarrow> MPoly_Type.coeff (mpoly_map_vars f p) mon = MPoly_Type.coeff (mpoly_map_vars g q) mon
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> keys mon \<subseteq> f ` vars q
\<not> keys mon \<subseteq> g ` vars q

goal (1 subgoal):
 1. MPoly_Type.coeff (mpoly_map_vars f p) mon = MPoly_Type.coeff (mpoly_map_vars g q) mon
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<not> keys mon \<subseteq> f ` vars q
\<not> keys mon \<subseteq> g ` vars q
f permutes - vars p
g permutes - vars q
p = q

goal (1 subgoal):
 1. MPoly_Type.coeff (mpoly_map_vars f p) mon = MPoly_Type.coeff (mpoly_map_vars g q) mon
[PROOF STEP]
by (subst (1 2) coeff_notin_vars)
         (auto simp: coeff_notin_vars vars_mpoly_map_vars permutes_bij)
[PROOF STATE]
proof (state)
this:
MPoly_Type.coeff (mpoly_map_vars f p) mon = MPoly_Type.coeff (mpoly_map_vars g q) mon

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
MPoly_Type.coeff (mpoly_map_vars f p) mon = MPoly_Type.coeff (mpoly_map_vars g q) mon

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma symmetric_mpoly_empty [simp, intro]: "symmetric_mpoly {} p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. symmetric_mpoly {} p
[PROOF STEP]
by (simp add: symmetric_mpoly_def)


[STATEMENT]
lemma symmetric_mpoly_orthogonal:
  assumes "vars p \<inter> A = {}"
  shows   "symmetric_mpoly A p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. symmetric_mpoly A p
[PROOF STEP]
unfolding symmetric_mpoly_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<pi>. \<pi> permutes A \<longrightarrow> mpoly_map_vars \<pi> p = p
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<pi>. \<pi> permutes A \<Longrightarrow> mpoly_map_vars \<pi> p = p
[PROOF STEP]
fix \<pi>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<pi>. \<pi> permutes A \<Longrightarrow> mpoly_map_vars \<pi> p = p
[PROOF STEP]
assume \<pi>: "\<pi> permutes A"
[PROOF STATE]
proof (state)
this:
\<pi> permutes A

goal (1 subgoal):
 1. \<And>\<pi>. \<pi> permutes A \<Longrightarrow> mpoly_map_vars \<pi> p = p
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
vars p \<inter> A = {}
\<pi> permutes A
[PROOF STEP]
have "\<pi> x = x" if "x \<in> vars p" for x
[PROOF STATE]
proof (prove)
using this:
vars p \<inter> A = {}
\<pi> permutes A

goal (1 subgoal):
 1. \<pi> x = x
[PROOF STEP]
using that permutes_not_in[of \<pi> A x]
[PROOF STATE]
proof (prove)
using this:
vars p \<inter> A = {}
\<pi> permutes A
x \<in> vars p
\<lbrakk>\<pi> permutes A; x \<notin> A\<rbrakk> \<Longrightarrow> \<pi> x = x

goal (1 subgoal):
 1. \<pi> x = x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?x \<in> vars p \<Longrightarrow> \<pi> ?x = ?x

goal (1 subgoal):
 1. \<And>\<pi>. \<pi> permutes A \<Longrightarrow> mpoly_map_vars \<pi> p = p
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
vars p \<inter> A = {}
[PROOF STEP]
have "mpoly_map_vars \<pi> p = mpoly_map_vars id p"
[PROOF STATE]
proof (prove)
using this:
vars p \<inter> A = {}

goal (1 subgoal):
 1. mpoly_map_vars \<pi> p = mpoly_map_vars id p
[PROOF STEP]
by (intro mpoly_map_vars_cong permutes_subset[OF \<pi>] permutes_id) auto
[PROOF STATE]
proof (state)
this:
mpoly_map_vars \<pi> p = mpoly_map_vars id p

goal (1 subgoal):
 1. \<And>\<pi>. \<pi> permutes A \<Longrightarrow> mpoly_map_vars \<pi> p = p
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
mpoly_map_vars \<pi> p = mpoly_map_vars id p

goal (1 subgoal):
 1. \<And>\<pi>. \<pi> permutes A \<Longrightarrow> mpoly_map_vars \<pi> p = p
[PROOF STEP]
have "\<dots> = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mpoly_map_vars id p = p
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
mpoly_map_vars id p = p

goal (1 subgoal):
 1. \<And>\<pi>. \<pi> permutes A \<Longrightarrow> mpoly_map_vars \<pi> p = p
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
mpoly_map_vars \<pi> p = p
[PROOF STEP]
show "mpoly_map_vars \<pi> p = p"
[PROOF STATE]
proof (prove)
using this:
mpoly_map_vars \<pi> p = p

goal (1 subgoal):
 1. mpoly_map_vars \<pi> p = p
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
mpoly_map_vars \<pi> p = p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma symmetric_mpoly_monom [intro]:
  assumes "keys m \<inter> A = {}"
  shows   "symmetric_mpoly A (monom m c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. symmetric_mpoly A (MPoly_Type.monom m c)
[PROOF STEP]
using assms vars_monom_subset[of m c]
[PROOF STATE]
proof (prove)
using this:
keys m \<inter> A = {}
vars (MPoly_Type.monom m c) \<subseteq> keys m

goal (1 subgoal):
 1. symmetric_mpoly A (MPoly_Type.monom m c)
[PROOF STEP]
by (intro symmetric_mpoly_orthogonal) auto


[STATEMENT]
lemma symmetric_mpoly_subset:
  assumes "symmetric_mpoly A p" "B \<subseteq> A"
  shows   "symmetric_mpoly B p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. symmetric_mpoly B p
[PROOF STEP]
unfolding symmetric_mpoly_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<pi>. \<pi> permutes B \<longrightarrow> mpoly_map_vars \<pi> p = p
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<pi>. \<pi> permutes B \<Longrightarrow> mpoly_map_vars \<pi> p = p
[PROOF STEP]
fix \<pi>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<pi>. \<pi> permutes B \<Longrightarrow> mpoly_map_vars \<pi> p = p
[PROOF STEP]
assume "\<pi> permutes B"
[PROOF STATE]
proof (state)
this:
\<pi> permutes B

goal (1 subgoal):
 1. \<And>\<pi>. \<pi> permutes B \<Longrightarrow> mpoly_map_vars \<pi> p = p
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
symmetric_mpoly A p
B \<subseteq> A
\<pi> permutes B
[PROOF STEP]
have "\<pi> permutes A"
[PROOF STATE]
proof (prove)
using this:
symmetric_mpoly A p
B \<subseteq> A
\<pi> permutes B

goal (1 subgoal):
 1. \<pi> permutes A
[PROOF STEP]
using permutes_subset
[PROOF STATE]
proof (prove)
using this:
symmetric_mpoly A p
B \<subseteq> A
\<pi> permutes B
\<lbrakk>?p permutes ?S; ?S \<subseteq> ?T\<rbrakk> \<Longrightarrow> ?p permutes ?T

goal (1 subgoal):
 1. \<pi> permutes A
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<pi> permutes A

goal (1 subgoal):
 1. \<And>\<pi>. \<pi> permutes B \<Longrightarrow> mpoly_map_vars \<pi> p = p
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
symmetric_mpoly A p
B \<subseteq> A
\<pi> permutes A
[PROOF STEP]
show "mpoly_map_vars \<pi> p = p"
[PROOF STATE]
proof (prove)
using this:
symmetric_mpoly A p
B \<subseteq> A
\<pi> permutes A

goal (1 subgoal):
 1. mpoly_map_vars \<pi> p = p
[PROOF STEP]
by (auto simp: symmetric_mpoly_def)
[PROOF STATE]
proof (state)
this:
mpoly_map_vars \<pi> p = p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma symmetric_mpoly_imp_orthogonal_or_subset:
  assumes "symmetric_mpoly A p"
  shows   "vars p \<inter> A = {} \<or> A \<subseteq> vars p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars p \<inter> A = {} \<or> A \<subseteq> vars p
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (vars p \<inter> A = {} \<or> A \<subseteq> vars p) \<Longrightarrow> False
[PROOF STEP]
assume "\<not>(vars p \<inter> A = {} \<or> A \<subseteq> vars p)"
[PROOF STATE]
proof (state)
this:
\<not> (vars p \<inter> A = {} \<or> A \<subseteq> vars p)

goal (1 subgoal):
 1. \<not> (vars p \<inter> A = {} \<or> A \<subseteq> vars p) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (vars p \<inter> A = {} \<or> A \<subseteq> vars p)
[PROOF STEP]
obtain x y where xy: "x \<in> vars p \<inter> A" "y \<in> A - vars p"
[PROOF STATE]
proof (prove)
using this:
\<not> (vars p \<inter> A = {} \<or> A \<subseteq> vars p)

goal (1 subgoal):
 1. (\<And>x y. \<lbrakk>x \<in> vars p \<inter> A; y \<in> A - vars p\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> vars p \<inter> A
y \<in> A - vars p

goal (1 subgoal):
 1. \<not> (vars p \<inter> A = {} \<or> A \<subseteq> vars p) \<Longrightarrow> False
[PROOF STEP]
define \<pi> where "\<pi> = transpose x y"
[PROOF STATE]
proof (state)
this:
\<pi> = Transposition.transpose x y

goal (1 subgoal):
 1. \<not> (vars p \<inter> A = {} \<or> A \<subseteq> vars p) \<Longrightarrow> False
[PROOF STEP]
from xy
[PROOF STATE]
proof (chain)
picking this:
x \<in> vars p \<inter> A
y \<in> A - vars p
[PROOF STEP]
have \<pi>: "\<pi> permutes A"
[PROOF STATE]
proof (prove)
using this:
x \<in> vars p \<inter> A
y \<in> A - vars p

goal (1 subgoal):
 1. \<pi> permutes A
[PROOF STEP]
unfolding \<pi>_def
[PROOF STATE]
proof (prove)
using this:
x \<in> vars p \<inter> A
y \<in> A - vars p

goal (1 subgoal):
 1. Transposition.transpose x y permutes A
[PROOF STEP]
by (intro permutes_swap_id) auto
[PROOF STATE]
proof (state)
this:
\<pi> permutes A

goal (1 subgoal):
 1. \<not> (vars p \<inter> A = {} \<or> A \<subseteq> vars p) \<Longrightarrow> False
[PROOF STEP]
from xy
[PROOF STATE]
proof (chain)
picking this:
x \<in> vars p \<inter> A
y \<in> A - vars p
[PROOF STEP]
have "y \<in> \<pi> ` vars p"
[PROOF STATE]
proof (prove)
using this:
x \<in> vars p \<inter> A
y \<in> A - vars p

goal (1 subgoal):
 1. y \<in> \<pi> ` vars p
[PROOF STEP]
by (auto simp: \<pi>_def transpose_def)
[PROOF STATE]
proof (state)
this:
y \<in> \<pi> ` vars p

goal (1 subgoal):
 1. \<not> (vars p \<inter> A = {} \<or> A \<subseteq> vars p) \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
y \<in> \<pi> ` vars p

goal (1 subgoal):
 1. \<not> (vars p \<inter> A = {} \<or> A \<subseteq> vars p) \<Longrightarrow> False
[PROOF STEP]
from \<pi>
[PROOF STATE]
proof (chain)
picking this:
\<pi> permutes A
[PROOF STEP]
have "\<pi> ` vars p = vars (mpoly_map_vars \<pi> p)"
[PROOF STATE]
proof (prove)
using this:
\<pi> permutes A

goal (1 subgoal):
 1. \<pi> ` vars p = vars (mpoly_map_vars \<pi> p)
[PROOF STEP]
by (auto simp: vars_mpoly_map_vars permutes_bij)
[PROOF STATE]
proof (state)
this:
\<pi> ` vars p = vars (mpoly_map_vars \<pi> p)

goal (1 subgoal):
 1. \<not> (vars p \<inter> A = {} \<or> A \<subseteq> vars p) \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<pi> ` vars p = vars (mpoly_map_vars \<pi> p)

goal (1 subgoal):
 1. \<not> (vars p \<inter> A = {} \<or> A \<subseteq> vars p) \<Longrightarrow> False
[PROOF STEP]
have "mpoly_map_vars \<pi> p = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mpoly_map_vars \<pi> p = p
[PROOF STEP]
using assms \<pi>
[PROOF STATE]
proof (prove)
using this:
symmetric_mpoly A p
\<pi> permutes A

goal (1 subgoal):
 1. mpoly_map_vars \<pi> p = p
[PROOF STEP]
by (simp add: symmetric_mpoly_def)
[PROOF STATE]
proof (state)
this:
mpoly_map_vars \<pi> p = p

goal (1 subgoal):
 1. \<not> (vars p \<inter> A = {} \<or> A \<subseteq> vars p) \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
y \<in> vars p
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
y \<in> vars p

goal (1 subgoal):
 1. False
[PROOF STEP]
using xy
[PROOF STATE]
proof (prove)
using this:
y \<in> vars p
x \<in> vars p \<inter> A
y \<in> A - vars p

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma symmetric_mpoly_add [intro]:
  "symmetric_mpoly A p \<Longrightarrow> symmetric_mpoly A q \<Longrightarrow> symmetric_mpoly A (p + q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>symmetric_mpoly A p; symmetric_mpoly A q\<rbrakk> \<Longrightarrow> symmetric_mpoly A (p + q)
[PROOF STEP]
unfolding symmetric_mpoly_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>\<pi>. \<pi> permutes A \<longrightarrow> mpoly_map_vars \<pi> p = p; \<forall>\<pi>. \<pi> permutes A \<longrightarrow> mpoly_map_vars \<pi> q = q\<rbrakk> \<Longrightarrow> \<forall>\<pi>. \<pi> permutes A \<longrightarrow> mpoly_map_vars \<pi> (p + q) = p + q
[PROOF STEP]
by simp


[STATEMENT]
lemma symmetric_mpoly_diff [intro]:
  "symmetric_mpoly A p \<Longrightarrow> symmetric_mpoly A q \<Longrightarrow> symmetric_mpoly A (p - q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>symmetric_mpoly A p; symmetric_mpoly A q\<rbrakk> \<Longrightarrow> symmetric_mpoly A (p - q)
[PROOF STEP]
unfolding symmetric_mpoly_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>\<pi>. \<pi> permutes A \<longrightarrow> mpoly_map_vars \<pi> p = p; \<forall>\<pi>. \<pi> permutes A \<longrightarrow> mpoly_map_vars \<pi> q = q\<rbrakk> \<Longrightarrow> \<forall>\<pi>. \<pi> permutes A \<longrightarrow> mpoly_map_vars \<pi> (p - q) = p - q
[PROOF STEP]
by simp


[STATEMENT]
lemma symmetric_mpoly_uminus [intro]: "symmetric_mpoly A p \<Longrightarrow> symmetric_mpoly A (-p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. symmetric_mpoly A p \<Longrightarrow> symmetric_mpoly A (- p)
[PROOF STEP]
unfolding symmetric_mpoly_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<pi>. \<pi> permutes A \<longrightarrow> mpoly_map_vars \<pi> p = p \<Longrightarrow> \<forall>\<pi>. \<pi> permutes A \<longrightarrow> mpoly_map_vars \<pi> (- p) = - p
[PROOF STEP]
by simp


[STATEMENT]
lemma symmetric_mpoly_uminus_iff [simp]: "symmetric_mpoly A (-p) \<longleftrightarrow> symmetric_mpoly A p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. symmetric_mpoly A (- p) = symmetric_mpoly A p
[PROOF STEP]
unfolding symmetric_mpoly_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>\<pi>. \<pi> permutes A \<longrightarrow> mpoly_map_vars \<pi> (- p) = - p) = (\<forall>\<pi>. \<pi> permutes A \<longrightarrow> mpoly_map_vars \<pi> p = p)
[PROOF STEP]
by simp


[STATEMENT]
lemma symmetric_mpoly_smult [intro]: "symmetric_mpoly A p \<Longrightarrow> symmetric_mpoly A (smult c p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. symmetric_mpoly A p \<Longrightarrow> symmetric_mpoly A (MPoly_Type.smult c p)
[PROOF STEP]
unfolding symmetric_mpoly_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<pi>. \<pi> permutes A \<longrightarrow> mpoly_map_vars \<pi> p = p \<Longrightarrow> \<forall>\<pi>. \<pi> permutes A \<longrightarrow> mpoly_map_vars \<pi> (MPoly_Type.smult c p) = MPoly_Type.smult c p
[PROOF STEP]
by simp


[STATEMENT]
lemma symmetric_mpoly_mult [intro]:
  "symmetric_mpoly A p \<Longrightarrow> symmetric_mpoly A q \<Longrightarrow> symmetric_mpoly A (p * q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>symmetric_mpoly A p; symmetric_mpoly A q\<rbrakk> \<Longrightarrow> symmetric_mpoly A (p * q)
[PROOF STEP]
unfolding symmetric_mpoly_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>\<pi>. \<pi> permutes A \<longrightarrow> mpoly_map_vars \<pi> p = p; \<forall>\<pi>. \<pi> permutes A \<longrightarrow> mpoly_map_vars \<pi> q = q\<rbrakk> \<Longrightarrow> \<forall>\<pi>. \<pi> permutes A \<longrightarrow> mpoly_map_vars \<pi> (p * q) = p * q
[PROOF STEP]
by simp


[STATEMENT]
lemma symmetric_mpoly_0 [simp, intro]: "symmetric_mpoly A 0"
  and symmetric_mpoly_1 [simp, intro]: "symmetric_mpoly A 1"
  and symmetric_mpoly_Const [simp, intro]: "symmetric_mpoly A (Const c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. symmetric_mpoly A 0 &&& symmetric_mpoly A 1 &&& symmetric_mpoly A (Const c)
[PROOF STEP]
by (simp_all add: symmetric_mpoly_def)


[STATEMENT]
lemma symmetric_mpoly_power [intro]:
  "symmetric_mpoly A p \<Longrightarrow> symmetric_mpoly A (p ^ n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. symmetric_mpoly A p \<Longrightarrow> symmetric_mpoly A (p ^ n)
[PROOF STEP]
by (induction n) (auto intro!: symmetric_mpoly_mult)


[STATEMENT]
lemma symmetric_mpoly_sum [intro]:
  "(\<And>i. i \<in> B \<Longrightarrow> symmetric_mpoly A (f i)) \<Longrightarrow> symmetric_mpoly A (sum f B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i. i \<in> B \<Longrightarrow> symmetric_mpoly A (f i)) \<Longrightarrow> symmetric_mpoly A (sum f B)
[PROOF STEP]
by (induction B rule: infinite_finite_induct) (auto intro!: symmetric_mpoly_add)


[STATEMENT]
lemma symmetric_mpoly_prod [intro]:
  "(\<And>i. i \<in> B \<Longrightarrow> symmetric_mpoly A (f i)) \<Longrightarrow> symmetric_mpoly A (prod f B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i. i \<in> B \<Longrightarrow> symmetric_mpoly A (f i)) \<Longrightarrow> symmetric_mpoly A (prod f B)
[PROOF STEP]
by (induction B rule: infinite_finite_induct) (auto intro!: symmetric_mpoly_mult)


[STATEMENT]
lemma symmetric_mpoly_symmetric_sum:
  assumes "g permutes X"
  assumes "\<And>x \<pi>. x \<in> X \<Longrightarrow> \<pi> permutes A \<Longrightarrow> mpoly_map_vars \<pi> (f x) = f (g x)"
  shows "symmetric_mpoly A (\<Sum>x\<in>X. f x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. symmetric_mpoly A (sum f X)
[PROOF STEP]
unfolding symmetric_mpoly_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<pi>. \<pi> permutes A \<longrightarrow> mpoly_map_vars \<pi> (sum f X) = sum f X
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<pi>. \<pi> permutes A \<Longrightarrow> mpoly_map_vars \<pi> (sum f X) = sum f X
[PROOF STEP]
fix \<pi>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<pi>. \<pi> permutes A \<Longrightarrow> mpoly_map_vars \<pi> (sum f X) = sum f X
[PROOF STEP]
assume \<pi>: "\<pi> permutes A"
[PROOF STATE]
proof (state)
this:
\<pi> permutes A

goal (1 subgoal):
 1. \<And>\<pi>. \<pi> permutes A \<Longrightarrow> mpoly_map_vars \<pi> (sum f X) = sum f X
[PROOF STEP]
have "mpoly_map_vars \<pi> (sum f X) = (\<Sum>x\<in>X. mpoly_map_vars \<pi> (f x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mpoly_map_vars \<pi> (sum f X) = (\<Sum>x\<in>X. mpoly_map_vars \<pi> (f x))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
mpoly_map_vars \<pi> (sum f X) = (\<Sum>x\<in>X. mpoly_map_vars \<pi> (f x))

goal (1 subgoal):
 1. \<And>\<pi>. \<pi> permutes A \<Longrightarrow> mpoly_map_vars \<pi> (sum f X) = sum f X
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
mpoly_map_vars \<pi> (sum f X) = (\<Sum>x\<in>X. mpoly_map_vars \<pi> (f x))

goal (1 subgoal):
 1. \<And>\<pi>. \<pi> permutes A \<Longrightarrow> mpoly_map_vars \<pi> (sum f X) = sum f X
[PROOF STEP]
have "\<dots> = (\<Sum>x\<in>X. f (g x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>X. mpoly_map_vars \<pi> (f x)) = (\<Sum>x\<in>X. f (g x))
[PROOF STEP]
by (intro sum.cong assms \<pi> refl)
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>X. mpoly_map_vars \<pi> (f x)) = (\<Sum>x\<in>X. f (g x))

goal (1 subgoal):
 1. \<And>\<pi>. \<pi> permutes A \<Longrightarrow> mpoly_map_vars \<pi> (sum f X) = sum f X
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>X. mpoly_map_vars \<pi> (f x)) = (\<Sum>x\<in>X. f (g x))

goal (1 subgoal):
 1. \<And>\<pi>. \<pi> permutes A \<Longrightarrow> mpoly_map_vars \<pi> (sum f X) = sum f X
[PROOF STEP]
have "\<dots> = (\<Sum>x\<in>g`X. f x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>X. f (g x)) = sum f (g ` X)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
g permutes X
\<lbrakk>?x \<in> X; ?\<pi> permutes A\<rbrakk> \<Longrightarrow> mpoly_map_vars ?\<pi> (f ?x) = f (g ?x)

goal (1 subgoal):
 1. (\<Sum>x\<in>X. f (g x)) = sum f (g ` X)
[PROOF STEP]
by (subst sum.reindex) (auto simp: permutes_inj_on)
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>X. f (g x)) = sum f (g ` X)

goal (1 subgoal):
 1. \<And>\<pi>. \<pi> permutes A \<Longrightarrow> mpoly_map_vars \<pi> (sum f X) = sum f X
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>X. f (g x)) = sum f (g ` X)

goal (1 subgoal):
 1. \<And>\<pi>. \<pi> permutes A \<Longrightarrow> mpoly_map_vars \<pi> (sum f X) = sum f X
[PROOF STEP]
have "g ` X = X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g ` X = X
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
g permutes X
\<lbrakk>?x \<in> X; ?\<pi> permutes A\<rbrakk> \<Longrightarrow> mpoly_map_vars ?\<pi> (f ?x) = f (g ?x)

goal (1 subgoal):
 1. g ` X = X
[PROOF STEP]
by (simp add: permutes_image)
[PROOF STATE]
proof (state)
this:
g ` X = X

goal (1 subgoal):
 1. \<And>\<pi>. \<pi> permutes A \<Longrightarrow> mpoly_map_vars \<pi> (sum f X) = sum f X
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
mpoly_map_vars \<pi> (sum f X) = sum f X
[PROOF STEP]
show "mpoly_map_vars \<pi> (sum f X) = sum f X"
[PROOF STATE]
proof (prove)
using this:
mpoly_map_vars \<pi> (sum f X) = sum f X

goal (1 subgoal):
 1. mpoly_map_vars \<pi> (sum f X) = sum f X
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
mpoly_map_vars \<pi> (sum f X) = sum f X

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma symmetric_mpoly_symmetric_prod:
  assumes "g permutes X"
  assumes "\<And>x \<pi>. x \<in> X \<Longrightarrow> \<pi> permutes A \<Longrightarrow> mpoly_map_vars \<pi> (f x) = f (g x)"
  shows "symmetric_mpoly A (\<Prod>x\<in>X. f x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. symmetric_mpoly A (prod f X)
[PROOF STEP]
unfolding symmetric_mpoly_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<pi>. \<pi> permutes A \<longrightarrow> mpoly_map_vars \<pi> (prod f X) = prod f X
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<pi>. \<pi> permutes A \<Longrightarrow> mpoly_map_vars \<pi> (prod f X) = prod f X
[PROOF STEP]
fix \<pi>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<pi>. \<pi> permutes A \<Longrightarrow> mpoly_map_vars \<pi> (prod f X) = prod f X
[PROOF STEP]
assume \<pi>: "\<pi> permutes A"
[PROOF STATE]
proof (state)
this:
\<pi> permutes A

goal (1 subgoal):
 1. \<And>\<pi>. \<pi> permutes A \<Longrightarrow> mpoly_map_vars \<pi> (prod f X) = prod f X
[PROOF STEP]
have "mpoly_map_vars \<pi> (prod f X) = (\<Prod>x\<in>X. mpoly_map_vars \<pi> (f x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mpoly_map_vars \<pi> (prod f X) = (\<Prod>x\<in>X. mpoly_map_vars \<pi> (f x))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
mpoly_map_vars \<pi> (prod f X) = (\<Prod>x\<in>X. mpoly_map_vars \<pi> (f x))

goal (1 subgoal):
 1. \<And>\<pi>. \<pi> permutes A \<Longrightarrow> mpoly_map_vars \<pi> (prod f X) = prod f X
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
mpoly_map_vars \<pi> (prod f X) = (\<Prod>x\<in>X. mpoly_map_vars \<pi> (f x))

goal (1 subgoal):
 1. \<And>\<pi>. \<pi> permutes A \<Longrightarrow> mpoly_map_vars \<pi> (prod f X) = prod f X
[PROOF STEP]
have "\<dots> = (\<Prod>x\<in>X. f (g x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>x\<in>X. mpoly_map_vars \<pi> (f x)) = (\<Prod>x\<in>X. f (g x))
[PROOF STEP]
by (intro prod.cong assms \<pi> refl)
[PROOF STATE]
proof (state)
this:
(\<Prod>x\<in>X. mpoly_map_vars \<pi> (f x)) = (\<Prod>x\<in>X. f (g x))

goal (1 subgoal):
 1. \<And>\<pi>. \<pi> permutes A \<Longrightarrow> mpoly_map_vars \<pi> (prod f X) = prod f X
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Prod>x\<in>X. mpoly_map_vars \<pi> (f x)) = (\<Prod>x\<in>X. f (g x))

goal (1 subgoal):
 1. \<And>\<pi>. \<pi> permutes A \<Longrightarrow> mpoly_map_vars \<pi> (prod f X) = prod f X
[PROOF STEP]
have "\<dots> = (\<Prod>x\<in>g`X. f x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>x\<in>X. f (g x)) = prod f (g ` X)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
g permutes X
\<lbrakk>?x \<in> X; ?\<pi> permutes A\<rbrakk> \<Longrightarrow> mpoly_map_vars ?\<pi> (f ?x) = f (g ?x)

goal (1 subgoal):
 1. (\<Prod>x\<in>X. f (g x)) = prod f (g ` X)
[PROOF STEP]
by (subst prod.reindex) (auto simp: permutes_inj_on)
[PROOF STATE]
proof (state)
this:
(\<Prod>x\<in>X. f (g x)) = prod f (g ` X)

goal (1 subgoal):
 1. \<And>\<pi>. \<pi> permutes A \<Longrightarrow> mpoly_map_vars \<pi> (prod f X) = prod f X
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Prod>x\<in>X. f (g x)) = prod f (g ` X)

goal (1 subgoal):
 1. \<And>\<pi>. \<pi> permutes A \<Longrightarrow> mpoly_map_vars \<pi> (prod f X) = prod f X
[PROOF STEP]
have "g ` X = X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g ` X = X
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
g permutes X
\<lbrakk>?x \<in> X; ?\<pi> permutes A\<rbrakk> \<Longrightarrow> mpoly_map_vars ?\<pi> (f ?x) = f (g ?x)

goal (1 subgoal):
 1. g ` X = X
[PROOF STEP]
by (simp add: permutes_image)
[PROOF STATE]
proof (state)
this:
g ` X = X

goal (1 subgoal):
 1. \<And>\<pi>. \<pi> permutes A \<Longrightarrow> mpoly_map_vars \<pi> (prod f X) = prod f X
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
mpoly_map_vars \<pi> (prod f X) = prod f X
[PROOF STEP]
show "mpoly_map_vars \<pi> (prod f X) = prod f X"
[PROOF STATE]
proof (prove)
using this:
mpoly_map_vars \<pi> (prod f X) = prod f X

goal (1 subgoal):
 1. mpoly_map_vars \<pi> (prod f X) = prod f X
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
mpoly_map_vars \<pi> (prod f X) = prod f X

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem lookup_lead_monom_decreasing:
  assumes "symmetric_mpoly A p"
  defines "m \<equiv> lead_monom p"
  assumes "i \<in> A" "j \<in> A" "i \<le> j"
  shows   "lookup m i \<ge> lookup m j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup m j \<le> lookup m i
[PROOF STEP]
proof (cases "p = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p = 0 \<Longrightarrow> lookup m j \<le> lookup m i
 2. p \<noteq> 0 \<Longrightarrow> lookup m j \<le> lookup m i
[PROOF STEP]
case [simp]: False
[PROOF STATE]
proof (state)
this:
p \<noteq> 0

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

goal (1 subgoal):
 1. lookup m i < lookup m j \<Longrightarrow> False
[PROOF STEP]
define \<pi> where "\<pi> = transpose i j"
[PROOF STATE]
proof (state)
this:
\<pi> = Transposition.transpose i j

goal (1 subgoal):
 1. lookup m i < lookup m j \<Longrightarrow> False
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
symmetric_mpoly A p
m \<equiv> lead_monom p
i \<in> A
j \<in> A
i \<le> j
[PROOF STEP]
have \<pi>: "\<pi> permutes A"
[PROOF STATE]
proof (prove)
using this:
symmetric_mpoly A p
m \<equiv> lead_monom p
i \<in> A
j \<in> A
i \<le> j

goal (1 subgoal):
 1. \<pi> permutes A
[PROOF STEP]
unfolding \<pi>_def
[PROOF STATE]
proof (prove)
using this:
symmetric_mpoly A p
m \<equiv> lead_monom p
i \<in> A
j \<in> A
i \<le> j

goal (1 subgoal):
 1. Transposition.transpose i j permutes A
[PROOF STEP]
by (intro permutes_swap_id) auto
[PROOF STATE]
proof (state)
this:
\<pi> permutes A

goal (1 subgoal):
 1. lookup m i < lookup m j \<Longrightarrow> False
[PROOF STEP]
have [simp]: "\<pi> \<circ> \<pi> = id" "\<pi> i = j" "\<pi> j = i" "\<And>k. k \<noteq> i \<Longrightarrow> k \<noteq> j \<Longrightarrow> \<pi> k = k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<pi> \<circ> \<pi> = id &&& \<pi> i = j) &&& \<pi> j = i &&& (\<And>k. \<lbrakk>k \<noteq> i; k \<noteq> j\<rbrakk> \<Longrightarrow> \<pi> k = k)
[PROOF STEP]
by (auto simp: \<pi>_def Fun.swap_def fun_eq_iff)
[PROOF STATE]
proof (state)
this:
\<pi> \<circ> \<pi> = id
\<pi> i = j
\<pi> j = i
\<lbrakk>?k \<noteq> i; ?k \<noteq> j\<rbrakk> \<Longrightarrow> \<pi> ?k = ?k

goal (1 subgoal):
 1. lookup m i < lookup m j \<Longrightarrow> False
[PROOF STEP]
have "0 \<noteq> lead_coeff p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<noteq> Symmetric_Polynomials.lead_coeff p
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(0::'a) \<noteq> Symmetric_Polynomials.lead_coeff p

goal (1 subgoal):
 1. lookup m i < lookup m j \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(0::'a) \<noteq> Symmetric_Polynomials.lead_coeff p

goal (1 subgoal):
 1. lookup m i < lookup m j \<Longrightarrow> False
[PROOF STEP]
have "lead_coeff p = MPoly_Type.coeff (mpoly_map_vars \<pi> p) (permutep \<pi> m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Symmetric_Polynomials.lead_coeff p = MPoly_Type.coeff (mpoly_map_vars \<pi> p) (permutep \<pi> m)
[PROOF STEP]
using \<pi>
[PROOF STATE]
proof (prove)
using this:
\<pi> permutes A

goal (1 subgoal):
 1. Symmetric_Polynomials.lead_coeff p = MPoly_Type.coeff (mpoly_map_vars \<pi> p) (permutep \<pi> m)
[PROOF STEP]
by (simp add: lead_coeff_def m_def coeff_mpoly_map_vars
                            permutes_bij permutep_comp' [symmetric])
[PROOF STATE]
proof (state)
this:
Symmetric_Polynomials.lead_coeff p = MPoly_Type.coeff (mpoly_map_vars \<pi> p) (permutep \<pi> m)

goal (1 subgoal):
 1. lookup m i < lookup m j \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Symmetric_Polynomials.lead_coeff p = MPoly_Type.coeff (mpoly_map_vars \<pi> p) (permutep \<pi> m)

goal (1 subgoal):
 1. lookup m i < lookup m j \<Longrightarrow> False
[PROOF STEP]
have "mpoly_map_vars \<pi> p = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mpoly_map_vars \<pi> p = p
[PROOF STEP]
using \<pi> assms
[PROOF STATE]
proof (prove)
using this:
\<pi> permutes A
symmetric_mpoly A p
m \<equiv> lead_monom p
i \<in> A
j \<in> A
i \<le> j

goal (1 subgoal):
 1. mpoly_map_vars \<pi> p = p
[PROOF STEP]
by (simp add: symmetric_mpoly_def)
[PROOF STATE]
proof (state)
this:
mpoly_map_vars \<pi> p = p

goal (1 subgoal):
 1. lookup m i < lookup m j \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(0::'a) \<noteq> MPoly_Type.coeff p (permutep \<pi> m)
[PROOF STEP]
have "permutep \<pi> m \<le> m"
[PROOF STATE]
proof (prove)
using this:
(0::'a) \<noteq> MPoly_Type.coeff p (permutep \<pi> m)

goal (1 subgoal):
 1. permutep \<pi> m \<le> m
[PROOF STEP]
by (auto simp: m_def)
[PROOF STATE]
proof (state)
this:
permutep \<pi> m \<le> m

goal (1 subgoal):
 1. lookup m i < lookup m j \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
permutep \<pi> m \<le> m

goal (1 subgoal):
 1. lookup m i < lookup m j \<Longrightarrow> False
[PROOF STEP]
have "lookup m i < lookup (permutep \<pi> m) i"
              and "(\<forall>k<i. lookup m k = lookup (permutep \<pi> m) k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup m i < lookup (permutep \<pi> m) i &&& \<forall>k<i. lookup m k = lookup (permutep \<pi> m) k
[PROOF STEP]
using assms \<pi> less
[PROOF STATE]
proof (prove)
using this:
symmetric_mpoly A p
m \<equiv> lead_monom p
i \<in> A
j \<in> A
i \<le> j
\<pi> permutes A
lookup m i < lookup m j

goal (1 subgoal):
 1. lookup m i < lookup (permutep \<pi> m) i &&& \<forall>k<i. lookup m k = lookup (permutep \<pi> m) k
[PROOF STEP]
by (auto simp: lookup_permutep permutes_bij)
[PROOF STATE]
proof (state)
this:
lookup m i < lookup (permutep \<pi> m) i
\<forall>k<i. lookup m k = lookup (permutep \<pi> m) k

goal (1 subgoal):
 1. lookup m i < lookup m j \<Longrightarrow> False
[PROOF STEP]
hence "m < permutep \<pi> m"
[PROOF STATE]
proof (prove)
using this:
lookup m i < lookup (permutep \<pi> m) i
\<forall>k<i. lookup m k = lookup (permutep \<pi> m) k

goal (1 subgoal):
 1. m < permutep \<pi> m
[PROOF STEP]
by (auto simp: less_poly_mapping_def less_fun_def)
[PROOF STATE]
proof (state)
this:
m < permutep \<pi> m

goal (1 subgoal):
 1. lookup m i < lookup m j \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
permutep \<pi> m \<le> m
m < permutep \<pi> m
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
permutep \<pi> m \<le> m
m < permutep \<pi> m

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:
lookup m j \<le> lookup m i

goal (1 subgoal):
 1. p = 0 \<Longrightarrow> lookup m j \<le> lookup m i
[PROOF STEP]
qed (auto simp: m_def)


[STATEMENT]
lemma lookup_sym_mpoly_aux_monom_of_set [simp]:
  assumes "finite X" "Y \<subseteq> X" "card Y = k"
  shows   "Poly_Mapping.lookup (sym_mpoly_aux X k) (monom_of_set Y) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup (sym_mpoly_aux X k) (monom_of_set Y) = (1::'a)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite X
Y \<subseteq> X
card Y = k

goal (1 subgoal):
 1. lookup (sym_mpoly_aux X k) (monom_of_set Y) = (1::'a)
[PROOF STEP]
by (auto simp: lookup_sym_mpoly_aux)


[STATEMENT]
lemma keys_sym_mpoly_aux: "m \<in> keys (sym_mpoly_aux A k) \<Longrightarrow> keys m \<subseteq> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m \<in> keys (sym_mpoly_aux A k) \<Longrightarrow> keys m \<subseteq> A
[PROOF STEP]
by transfer' (auto split: if_splits simp: keys_monom_of_set)


[STATEMENT]
lemma vars_sym_mpoly_subset: "vars (sym_mpoly A k) \<subseteq> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars (sym_mpoly A k) \<subseteq> A
[PROOF STEP]
using keys_sym_mpoly_aux
[PROOF STATE]
proof (prove)
using this:
?m \<in> keys (sym_mpoly_aux ?A ?k) \<Longrightarrow> keys ?m \<subseteq> ?A

goal (1 subgoal):
 1. vars (sym_mpoly A k) \<subseteq> A
[PROOF STEP]
by (auto simp: vars_def sym_mpoly.rep_eq)


[STATEMENT]
lemma coeff_sym_mpoly:
  "MPoly_Type.coeff (sym_mpoly X k) mon =
     (if finite X \<and> (\<exists>Y. Y \<subseteq> X \<and> card Y = k \<and> mon = monom_of_set Y) then 1 else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MPoly_Type.coeff (sym_mpoly X k) mon = (if finite X \<and> (\<exists>Y\<subseteq>X. card Y = k \<and> mon = monom_of_set Y) then 1::'a else (0::'a))
[PROOF STEP]
by transfer' (simp add: lookup_sym_mpoly_aux)


[STATEMENT]
lemma sym_mpoly_infinite: "\<not>finite A \<Longrightarrow> sym_mpoly A k = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite A \<Longrightarrow> sym_mpoly A k = 0
[PROOF STEP]
by (transfer, transfer) auto


[STATEMENT]
lemma sym_mpoly_altdef: "sym_mpoly A k = (\<Sum>X | X \<subseteq> A \<and> card X = k. monom (monom_of_set X) 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sym_mpoly A k = (\<Sum>X | X \<subseteq> A \<and> card X = k. MPoly_Type.monom (monom_of_set X) (1::'a))
[PROOF STEP]
proof (cases "finite A")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. finite A \<Longrightarrow> sym_mpoly A k = (\<Sum>X | X \<subseteq> A \<and> card X = k. MPoly_Type.monom (monom_of_set X) (1::'a))
 2. infinite A \<Longrightarrow> sym_mpoly A k = (\<Sum>X | X \<subseteq> A \<and> card X = k. MPoly_Type.monom (monom_of_set X) (1::'a))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
infinite A

goal (2 subgoals):
 1. finite A \<Longrightarrow> sym_mpoly A k = (\<Sum>X | X \<subseteq> A \<and> card X = k. MPoly_Type.monom (monom_of_set X) (1::'a))
 2. infinite A \<Longrightarrow> sym_mpoly A k = (\<Sum>X | X \<subseteq> A \<and> card X = k. MPoly_Type.monom (monom_of_set X) (1::'a))
[PROOF STEP]
hence *: "infinite {X. X \<subseteq> A \<and> infinite X}"
[PROOF STATE]
proof (prove)
using this:
infinite A

goal (1 subgoal):
 1. infinite {X. X \<subseteq> A \<and> infinite X}
[PROOF STEP]
by (rule infinite_infinite_subsets)
[PROOF STATE]
proof (state)
this:
infinite {X. X \<subseteq> A \<and> infinite X}

goal (2 subgoals):
 1. finite A \<Longrightarrow> sym_mpoly A k = (\<Sum>X | X \<subseteq> A \<and> card X = k. MPoly_Type.monom (monom_of_set X) (1::'a))
 2. infinite A \<Longrightarrow> sym_mpoly A k = (\<Sum>X | X \<subseteq> A \<and> card X = k. MPoly_Type.monom (monom_of_set X) (1::'a))
[PROOF STEP]
have "infinite {X. X \<subseteq> A \<and> card X = 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite {X. X \<subseteq> A \<and> card X = 0}
[PROOF STEP]
by (rule infinite_super[OF _ *]) auto
[PROOF STATE]
proof (state)
this:
infinite {X. X \<subseteq> A \<and> card X = 0}

goal (2 subgoals):
 1. finite A \<Longrightarrow> sym_mpoly A k = (\<Sum>X | X \<subseteq> A \<and> card X = k. MPoly_Type.monom (monom_of_set X) (1::'a))
 2. infinite A \<Longrightarrow> sym_mpoly A k = (\<Sum>X | X \<subseteq> A \<and> card X = k. MPoly_Type.monom (monom_of_set X) (1::'a))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
infinite {X. X \<subseteq> A \<and> card X = 0}

goal (2 subgoals):
 1. finite A \<Longrightarrow> sym_mpoly A k = (\<Sum>X | X \<subseteq> A \<and> card X = k. MPoly_Type.monom (monom_of_set X) (1::'a))
 2. infinite A \<Longrightarrow> sym_mpoly A k = (\<Sum>X | X \<subseteq> A \<and> card X = k. MPoly_Type.monom (monom_of_set X) (1::'a))
[PROOF STEP]
have **: "infinite {X. X \<subseteq> A \<and> finite X \<and> card X = k}" if "k \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite {X. X \<subseteq> A \<and> finite X \<and> card X = k}
[PROOF STEP]
using that infinite_card_subsets[of A k] False
[PROOF STATE]
proof (prove)
using this:
k \<noteq> 0
\<lbrakk>infinite A; 0 < k\<rbrakk> \<Longrightarrow> infinite {X. X \<subseteq> A \<and> finite X \<and> card X = k}
infinite A

goal (1 subgoal):
 1. infinite {X. X \<subseteq> A \<and> finite X \<and> card X = k}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k \<noteq> 0 \<Longrightarrow> infinite {X. X \<subseteq> A \<and> finite X \<and> card X = k}

goal (2 subgoals):
 1. finite A \<Longrightarrow> sym_mpoly A k = (\<Sum>X | X \<subseteq> A \<and> card X = k. MPoly_Type.monom (monom_of_set X) (1::'a))
 2. infinite A \<Longrightarrow> sym_mpoly A k = (\<Sum>X | X \<subseteq> A \<and> card X = k. MPoly_Type.monom (monom_of_set X) (1::'a))
[PROOF STEP]
have "infinite {X. X \<subseteq> A \<and> card X = k}" if "k \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite {X. X \<subseteq> A \<and> card X = k}
[PROOF STEP]
by (rule infinite_super[OF _ **[OF that]]) auto
[PROOF STATE]
proof (state)
this:
k \<noteq> 0 \<Longrightarrow> infinite {X. X \<subseteq> A \<and> card X = k}

goal (2 subgoals):
 1. finite A \<Longrightarrow> sym_mpoly A k = (\<Sum>X | X \<subseteq> A \<and> card X = k. MPoly_Type.monom (monom_of_set X) (1::'a))
 2. infinite A \<Longrightarrow> sym_mpoly A k = (\<Sum>X | X \<subseteq> A \<and> card X = k. MPoly_Type.monom (monom_of_set X) (1::'a))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
infinite {X. X \<subseteq> A \<and> card X = 0}
k \<noteq> 0 \<Longrightarrow> infinite {X. X \<subseteq> A \<and> card X = k}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
infinite {X. X \<subseteq> A \<and> card X = 0}
k \<noteq> 0 \<Longrightarrow> infinite {X. X \<subseteq> A \<and> card X = k}

goal (1 subgoal):
 1. sym_mpoly A k = (\<Sum>X | X \<subseteq> A \<and> card X = k. MPoly_Type.monom (monom_of_set X) (1::'a))
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
infinite {X. X \<subseteq> A \<and> card X = 0}
k \<noteq> 0 \<Longrightarrow> infinite {X. X \<subseteq> A \<and> card X = k}
infinite A

goal (1 subgoal):
 1. sym_mpoly A k = (\<Sum>X | X \<subseteq> A \<and> card X = k. MPoly_Type.monom (monom_of_set X) (1::'a))
[PROOF STEP]
by (cases "k = 0") (simp_all add: sym_mpoly_infinite)
[PROOF STATE]
proof (state)
this:
sym_mpoly A k = (\<Sum>X | X \<subseteq> A \<and> card X = k. MPoly_Type.monom (monom_of_set X) (1::'a))

goal (1 subgoal):
 1. finite A \<Longrightarrow> sym_mpoly A k = (\<Sum>X | X \<subseteq> A \<and> card X = k. MPoly_Type.monom (monom_of_set X) (1::'a))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite A \<Longrightarrow> sym_mpoly A k = (\<Sum>X | X \<subseteq> A \<and> card X = k. MPoly_Type.monom (monom_of_set X) (1::'a))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
finite A

goal (1 subgoal):
 1. finite A \<Longrightarrow> sym_mpoly A k = (\<Sum>X | X \<subseteq> A \<and> card X = k. MPoly_Type.monom (monom_of_set X) (1::'a))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sym_mpoly A k = (\<Sum>X | X \<subseteq> A \<and> card X = k. MPoly_Type.monom (monom_of_set X) (1::'a))
[PROOF STEP]
proof (intro mpoly_eqI, goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>mon. MPoly_Type.coeff (sym_mpoly A k) mon = MPoly_Type.coeff (\<Sum>X | X \<subseteq> A \<and> card X = k. MPoly_Type.monom (monom_of_set X) (1::'a)) mon
[PROOF STEP]
case (1 m)
[PROOF STATE]
proof (state)
this:

goal (1 subgoal):
 1. \<And>mon. MPoly_Type.coeff (sym_mpoly A k) mon = MPoly_Type.coeff (\<Sum>X | X \<subseteq> A \<and> card X = k. MPoly_Type.monom (monom_of_set X) (1::'a)) mon
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MPoly_Type.coeff (sym_mpoly A k) m = MPoly_Type.coeff (\<Sum>X | X \<subseteq> A \<and> card X = k. MPoly_Type.monom (monom_of_set X) (1::'a)) m
[PROOF STEP]
proof (cases "\<exists>X. X \<subseteq> A \<and> card X = k \<and> m = monom_of_set X")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>X\<subseteq>A. card X = k \<and> m = monom_of_set X \<Longrightarrow> MPoly_Type.coeff (sym_mpoly A k) m = MPoly_Type.coeff (\<Sum>X | X \<subseteq> A \<and> card X = k. MPoly_Type.monom (monom_of_set X) (1::'a)) m
 2. \<not> (\<exists>X\<subseteq>A. card X = k \<and> m = monom_of_set X) \<Longrightarrow> MPoly_Type.coeff (sym_mpoly A k) m = MPoly_Type.coeff (\<Sum>X | X \<subseteq> A \<and> card X = k. MPoly_Type.monom (monom_of_set X) (1::'a)) m
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (\<exists>X\<subseteq>A. card X = k \<and> m = monom_of_set X)

goal (2 subgoals):
 1. \<exists>X\<subseteq>A. card X = k \<and> m = monom_of_set X \<Longrightarrow> MPoly_Type.coeff (sym_mpoly A k) m = MPoly_Type.coeff (\<Sum>X | X \<subseteq> A \<and> card X = k. MPoly_Type.monom (monom_of_set X) (1::'a)) m
 2. \<not> (\<exists>X\<subseteq>A. card X = k \<and> m = monom_of_set X) \<Longrightarrow> MPoly_Type.coeff (sym_mpoly A k) m = MPoly_Type.coeff (\<Sum>X | X \<subseteq> A \<and> card X = k. MPoly_Type.monom (monom_of_set X) (1::'a)) m
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>X\<subseteq>A. card X = k \<and> m = monom_of_set X)

goal (1 subgoal):
 1. MPoly_Type.coeff (sym_mpoly A k) m = MPoly_Type.coeff (\<Sum>X | X \<subseteq> A \<and> card X = k. MPoly_Type.monom (monom_of_set X) (1::'a)) m
[PROOF STEP]
by (auto simp: coeff_sym_mpoly coeff_sum coeff_monom)
[PROOF STATE]
proof (state)
this:
MPoly_Type.coeff (sym_mpoly A k) m = MPoly_Type.coeff (\<Sum>X | X \<subseteq> A \<and> card X = k. MPoly_Type.monom (monom_of_set X) (1::'a)) m

goal (1 subgoal):
 1. \<exists>X\<subseteq>A. card X = k \<and> m = monom_of_set X \<Longrightarrow> MPoly_Type.coeff (sym_mpoly A k) m = MPoly_Type.coeff (\<Sum>X | X \<subseteq> A \<and> card X = k. MPoly_Type.monom (monom_of_set X) (1::'a)) m
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>X\<subseteq>A. card X = k \<and> m = monom_of_set X \<Longrightarrow> MPoly_Type.coeff (sym_mpoly A k) m = MPoly_Type.coeff (\<Sum>X | X \<subseteq> A \<and> card X = k. MPoly_Type.monom (monom_of_set X) (1::'a)) m
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<exists>X\<subseteq>A. card X = k \<and> m = monom_of_set X

goal (1 subgoal):
 1. \<exists>X\<subseteq>A. card X = k \<and> m = monom_of_set X \<Longrightarrow> MPoly_Type.coeff (sym_mpoly A k) m = MPoly_Type.coeff (\<Sum>X | X \<subseteq> A \<and> card X = k. MPoly_Type.monom (monom_of_set X) (1::'a)) m
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>X\<subseteq>A. card X = k \<and> m = monom_of_set X
[PROOF STEP]
obtain X where X: "X \<subseteq> A" "card X = k" "m = monom_of_set X"
[PROOF STATE]
proof (prove)
using this:
\<exists>X\<subseteq>A. card X = k \<and> m = monom_of_set X

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

goal (1 subgoal):
 1. \<exists>X\<subseteq>A. card X = k \<and> m = monom_of_set X \<Longrightarrow> MPoly_Type.coeff (sym_mpoly A k) m = MPoly_Type.coeff (\<Sum>X | X \<subseteq> A \<and> card X = k. MPoly_Type.monom (monom_of_set X) (1::'a)) m
[PROOF STEP]
have "coeff (\<Sum>X | X \<subseteq> A \<and> card X = k.
               monom (monom_of_set X) 1) m = (\<Sum>X\<in>{X}. 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MPoly_Type.coeff (\<Sum>X | X \<subseteq> A \<and> card X = k. MPoly_Type.monom (monom_of_set X) (1::'b)) m = (\<Sum>X\<in>{X}. (1::'b))
[PROOF STEP]
unfolding coeff_sum
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>{X. X \<subseteq> A \<and> card X = k}. MPoly_Type.coeff (MPoly_Type.monom (monom_of_set x) (1::'b)) m) = (\<Sum>X\<in>{X}. (1::'b))
[PROOF STEP]
proof (intro sum.mono_neutral_cong_right ballI)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. finite {X. X \<subseteq> A \<and> card X = k}
 2. {X} \<subseteq> {X. X \<subseteq> A \<and> card X = k}
 3. \<And>i. i \<in> {X. X \<subseteq> A \<and> card X = k} - {X} \<Longrightarrow> MPoly_Type.coeff (MPoly_Type.monom (monom_of_set i) (1::'b)) m = (0::'b)
 4. \<And>x. x \<in> {X} \<Longrightarrow> MPoly_Type.coeff (MPoly_Type.monom (monom_of_set x) (1::'b)) m = (1::'b)
[PROOF STEP]
fix Y
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. finite {X. X \<subseteq> A \<and> card X = k}
 2. {X} \<subseteq> {X. X \<subseteq> A \<and> card X = k}
 3. \<And>i. i \<in> {X. X \<subseteq> A \<and> card X = k} - {X} \<Longrightarrow> MPoly_Type.coeff (MPoly_Type.monom (monom_of_set i) (1::'b)) m = (0::'b)
 4. \<And>x. x \<in> {X} \<Longrightarrow> MPoly_Type.coeff (MPoly_Type.monom (monom_of_set x) (1::'b)) m = (1::'b)
[PROOF STEP]
assume Y: "Y \<in> {X. X \<subseteq> A \<and> card X = k} - {X}"
[PROOF STATE]
proof (state)
this:
Y \<in> {X. X \<subseteq> A \<and> card X = k} - {X}

goal (4 subgoals):
 1. finite {X. X \<subseteq> A \<and> card X = k}
 2. {X} \<subseteq> {X. X \<subseteq> A \<and> card X = k}
 3. \<And>i. i \<in> {X. X \<subseteq> A \<and> card X = k} - {X} \<Longrightarrow> MPoly_Type.coeff (MPoly_Type.monom (monom_of_set i) (1::'b)) m = (0::'b)
 4. \<And>x. x \<in> {X} \<Longrightarrow> MPoly_Type.coeff (MPoly_Type.monom (monom_of_set x) (1::'b)) m = (1::'b)
[PROOF STEP]
hence "X = Y" if "monom_of_set X = monom_of_set Y"
[PROOF STATE]
proof (prove)
using this:
Y \<in> {X. X \<subseteq> A \<and> card X = k} - {X}

goal (1 subgoal):
 1. X = Y
[PROOF STEP]
using that finite_subset[OF X(1)] finite_subset[of Y A] \<open>finite A\<close>
[PROOF STATE]
proof (prove)
using this:
Y \<in> {X. X \<subseteq> A \<and> card X = k} - {X}
monom_of_set X = monom_of_set Y
finite A \<Longrightarrow> finite X
\<lbrakk>Y \<subseteq> A; finite A\<rbrakk> \<Longrightarrow> finite Y
finite A

goal (1 subgoal):
 1. X = Y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
monom_of_set X = monom_of_set Y \<Longrightarrow> X = Y

goal (4 subgoals):
 1. finite {X. X \<subseteq> A \<and> card X = k}
 2. {X} \<subseteq> {X. X \<subseteq> A \<and> card X = k}
 3. \<And>i. i \<in> {X. X \<subseteq> A \<and> card X = k} - {X} \<Longrightarrow> MPoly_Type.coeff (MPoly_Type.monom (monom_of_set i) (1::'b)) m = (0::'b)
 4. \<And>x. x \<in> {X} \<Longrightarrow> MPoly_Type.coeff (MPoly_Type.monom (monom_of_set x) (1::'b)) m = (1::'b)
[PROOF STEP]
thus "coeff (monom (monom_of_set Y) 1) m = 0"
[PROOF STATE]
proof (prove)
using this:
monom_of_set X = monom_of_set Y \<Longrightarrow> X = Y

goal (1 subgoal):
 1. MPoly_Type.coeff (MPoly_Type.monom (monom_of_set Y) (1::'c)) m = (0::'c)
[PROOF STEP]
using X Y
[PROOF STATE]
proof (prove)
using this:
monom_of_set X = monom_of_set Y \<Longrightarrow> X = Y
X \<subseteq> A
card X = k
m = monom_of_set X
Y \<in> {X. X \<subseteq> A \<and> card X = k} - {X}

goal (1 subgoal):
 1. MPoly_Type.coeff (MPoly_Type.monom (monom_of_set Y) (1::'c)) m = (0::'c)
[PROOF STEP]
by (auto simp: coeff_monom when_def )
[PROOF STATE]
proof (state)
this:
MPoly_Type.coeff (MPoly_Type.monom (monom_of_set Y) (1::?'c1)) m = (0::?'c1)

goal (3 subgoals):
 1. finite {X. X \<subseteq> A \<and> card X = k}
 2. {X} \<subseteq> {X. X \<subseteq> A \<and> card X = k}
 3. \<And>x. x \<in> {X} \<Longrightarrow> MPoly_Type.coeff (MPoly_Type.monom (monom_of_set x) (1::'b)) m = (1::'b)
[PROOF STEP]
qed (insert X \<open>finite A\<close>, auto simp: coeff_monom)
[PROOF STATE]
proof (state)
this:
MPoly_Type.coeff (\<Sum>X | X \<subseteq> A \<and> card X = k. MPoly_Type.monom (monom_of_set X) (1::?'b1)) m = (\<Sum>X\<in>{X}. (1::?'b1))

goal (1 subgoal):
 1. \<exists>X\<subseteq>A. card X = k \<and> m = monom_of_set X \<Longrightarrow> MPoly_Type.coeff (sym_mpoly A k) m = MPoly_Type.coeff (\<Sum>X | X \<subseteq> A \<and> card X = k. MPoly_Type.monom (monom_of_set X) (1::'a)) m
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
MPoly_Type.coeff (\<Sum>X | X \<subseteq> A \<and> card X = k. MPoly_Type.monom (monom_of_set X) (1::?'b1)) m = (\<Sum>X\<in>{X}. (1::?'b1))

goal (1 subgoal):
 1. MPoly_Type.coeff (sym_mpoly A k) m = MPoly_Type.coeff (\<Sum>X | X \<subseteq> A \<and> card X = k. MPoly_Type.monom (monom_of_set X) (1::'a)) m
[PROOF STEP]
using \<open>finite A\<close>
[PROOF STATE]
proof (prove)
using this:
MPoly_Type.coeff (\<Sum>X | X \<subseteq> A \<and> card X = k. MPoly_Type.monom (monom_of_set X) (1::?'b1)) m = (\<Sum>X\<in>{X}. (1::?'b1))
finite A

goal (1 subgoal):
 1. MPoly_Type.coeff (sym_mpoly A k) m = MPoly_Type.coeff (\<Sum>X | X \<subseteq> A \<and> card X = k. MPoly_Type.monom (monom_of_set X) (1::'a)) m
[PROOF STEP]
by (auto simp: coeff_sym_mpoly coeff_sum coeff_monom)
[PROOF STATE]
proof (state)
this:
MPoly_Type.coeff (sym_mpoly A k) m = MPoly_Type.coeff (\<Sum>X | X \<subseteq> A \<and> card X = k. MPoly_Type.monom (monom_of_set X) (1::'a)) m

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
MPoly_Type.coeff (sym_mpoly A k) m = MPoly_Type.coeff (\<Sum>X | X \<subseteq> A \<and> card X = k. MPoly_Type.monom (monom_of_set X) (1::'a)) m

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sym_mpoly A k = (\<Sum>X | X \<subseteq> A \<and> card X = k. MPoly_Type.monom (monom_of_set X) (1::'a))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma coeff_sym_mpoly_monom_of_set [simp]:
  assumes "finite X" "Y \<subseteq> X" "card Y = k"
  shows   "MPoly_Type.coeff (sym_mpoly X k) (monom_of_set Y) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MPoly_Type.coeff (sym_mpoly X k) (monom_of_set Y) = (1::'a)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite X
Y \<subseteq> X
card Y = k

goal (1 subgoal):
 1. MPoly_Type.coeff (sym_mpoly X k) (monom_of_set Y) = (1::'a)
[PROOF STEP]
by (auto simp: coeff_sym_mpoly)


[STATEMENT]
lemma coeff_sym_mpoly_0: "coeff (sym_mpoly X k) 0 = (if finite X \<and> k = 0 then 1 else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MPoly_Type.coeff (sym_mpoly X k) 0 = (if finite X \<and> k = 0 then 1::'a else (0::'a))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. MPoly_Type.coeff (sym_mpoly X k) 0 = (if finite X \<and> k = 0 then 1::'a else (0::'a))
[PROOF STEP]
consider "finite X" "k = 0" | "finite X" "k \<noteq> 0" | "infinite X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>finite X; k = 0\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>finite X; k \<noteq> 0\<rbrakk> \<Longrightarrow> thesis; infinite X \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<lbrakk>finite X; k = 0\<rbrakk> \<Longrightarrow> ?thesis; \<lbrakk>finite X; k \<noteq> 0\<rbrakk> \<Longrightarrow> ?thesis; infinite X \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. MPoly_Type.coeff (sym_mpoly X k) 0 = (if finite X \<and> k = 0 then 1::'a else (0::'a))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<lbrakk>finite X; k = 0\<rbrakk> \<Longrightarrow> ?thesis; \<lbrakk>finite X; k \<noteq> 0\<rbrakk> \<Longrightarrow> ?thesis; infinite X \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. MPoly_Type.coeff (sym_mpoly X k) 0 = (if finite X \<and> k = 0 then 1::'a else (0::'a))
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<lbrakk>finite X; k = 0\<rbrakk> \<Longrightarrow> MPoly_Type.coeff (sym_mpoly X k) 0 = (if finite X \<and> k = 0 then 1::'a else (0::'a))
 2. \<lbrakk>finite X; k \<noteq> 0\<rbrakk> \<Longrightarrow> MPoly_Type.coeff (sym_mpoly X k) 0 = (if finite X \<and> k = 0 then 1::'a else (0::'a))
 3. infinite X \<Longrightarrow> MPoly_Type.coeff (sym_mpoly X k) 0 = (if finite X \<and> k = 0 then 1::'a else (0::'a))
[PROOF STEP]
assume "finite X" "k = 0"
[PROOF STATE]
proof (state)
this:
finite X
k = 0

goal (3 subgoals):
 1. \<lbrakk>finite X; k = 0\<rbrakk> \<Longrightarrow> MPoly_Type.coeff (sym_mpoly X k) 0 = (if finite X \<and> k = 0 then 1::'a else (0::'a))
 2. \<lbrakk>finite X; k \<noteq> 0\<rbrakk> \<Longrightarrow> MPoly_Type.coeff (sym_mpoly X k) 0 = (if finite X \<and> k = 0 then 1::'a else (0::'a))
 3. infinite X \<Longrightarrow> MPoly_Type.coeff (sym_mpoly X k) 0 = (if finite X \<and> k = 0 then 1::'a else (0::'a))
[PROOF STEP]
hence "coeff (sym_mpoly X k) (monom_of_set {}) = 1"
[PROOF STATE]
proof (prove)
using this:
finite X
k = 0

goal (1 subgoal):
 1. MPoly_Type.coeff (sym_mpoly X k) (monom_of_set {}) = (1::'b)
[PROOF STEP]
by (subst coeff_sym_mpoly_monom_of_set) auto
[PROOF STATE]
proof (state)
this:
MPoly_Type.coeff (sym_mpoly X k) (monom_of_set {}) = (1::?'b1)

goal (3 subgoals):
 1. \<lbrakk>finite X; k = 0\<rbrakk> \<Longrightarrow> MPoly_Type.coeff (sym_mpoly X k) 0 = (if finite X \<and> k = 0 then 1::'a else (0::'a))
 2. \<lbrakk>finite X; k \<noteq> 0\<rbrakk> \<Longrightarrow> MPoly_Type.coeff (sym_mpoly X k) 0 = (if finite X \<and> k = 0 then 1::'a else (0::'a))
 3. infinite X \<Longrightarrow> MPoly_Type.coeff (sym_mpoly X k) 0 = (if finite X \<and> k = 0 then 1::'a else (0::'a))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
MPoly_Type.coeff (sym_mpoly X k) (monom_of_set {}) = (1::?'b1)

goal (1 subgoal):
 1. MPoly_Type.coeff (sym_mpoly X k) 0 = (if finite X \<and> k = 0 then 1::'a else (0::'a))
[PROOF STEP]
unfolding monom_of_set_empty
[PROOF STATE]
proof (prove)
using this:
MPoly_Type.coeff (sym_mpoly X k) 0 = (1::?'b1)

goal (1 subgoal):
 1. MPoly_Type.coeff (sym_mpoly X k) 0 = (if finite X \<and> k = 0 then 1::'a else (0::'a))
[PROOF STEP]
using \<open>finite X\<close> \<open>k = 0\<close>
[PROOF STATE]
proof (prove)
using this:
MPoly_Type.coeff (sym_mpoly X k) 0 = (1::?'b1)
finite X
k = 0

goal (1 subgoal):
 1. MPoly_Type.coeff (sym_mpoly X k) 0 = (if finite X \<and> k = 0 then 1::'a else (0::'a))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
MPoly_Type.coeff (sym_mpoly X k) 0 = (if finite X \<and> k = 0 then 1::'a else (0::'a))

goal (2 subgoals):
 1. \<lbrakk>finite X; k \<noteq> 0\<rbrakk> \<Longrightarrow> MPoly_Type.coeff (sym_mpoly X k) 0 = (if finite X \<and> k = 0 then 1::'a else (0::'a))
 2. infinite X \<Longrightarrow> MPoly_Type.coeff (sym_mpoly X k) 0 = (if finite X \<and> k = 0 then 1::'a else (0::'a))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>finite X; k \<noteq> 0\<rbrakk> \<Longrightarrow> MPoly_Type.coeff (sym_mpoly X k) 0 = (if finite X \<and> k = 0 then 1::'a else (0::'a))
 2. infinite X \<Longrightarrow> MPoly_Type.coeff (sym_mpoly X k) 0 = (if finite X \<and> k = 0 then 1::'a else (0::'a))
[PROOF STEP]
assume "finite X" "k \<noteq> 0"
[PROOF STATE]
proof (state)
this:
finite X
k \<noteq> 0

goal (2 subgoals):
 1. \<lbrakk>finite X; k \<noteq> 0\<rbrakk> \<Longrightarrow> MPoly_Type.coeff (sym_mpoly X k) 0 = (if finite X \<and> k = 0 then 1::'a else (0::'a))
 2. infinite X \<Longrightarrow> MPoly_Type.coeff (sym_mpoly X k) 0 = (if finite X \<and> k = 0 then 1::'a else (0::'a))
[PROOF STEP]
hence "\<not>(\<exists>Y. finite Y \<and> Y \<subseteq> X \<and> card Y = k \<and> monom_of_set Y = 0)"
[PROOF STATE]
proof (prove)
using this:
finite X
k \<noteq> 0

goal (1 subgoal):
 1. \<nexists>Y. finite Y \<and> Y \<subseteq> X \<and> card Y = k \<and> monom_of_set Y = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<nexists>Y. finite Y \<and> Y \<subseteq> X \<and> card Y = k \<and> monom_of_set Y = 0

goal (2 subgoals):
 1. \<lbrakk>finite X; k \<noteq> 0\<rbrakk> \<Longrightarrow> MPoly_Type.coeff (sym_mpoly X k) 0 = (if finite X \<and> k = 0 then 1::'a else (0::'a))
 2. infinite X \<Longrightarrow> MPoly_Type.coeff (sym_mpoly X k) 0 = (if finite X \<and> k = 0 then 1::'a else (0::'a))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<nexists>Y. finite Y \<and> Y \<subseteq> X \<and> card Y = k \<and> monom_of_set Y = 0

goal (1 subgoal):
 1. MPoly_Type.coeff (sym_mpoly X k) 0 = (if finite X \<and> k = 0 then 1::'a else (0::'a))
[PROOF STEP]
using \<open>k \<noteq> 0\<close>
[PROOF STATE]
proof (prove)
using this:
\<nexists>Y. finite Y \<and> Y \<subseteq> X \<and> card Y = k \<and> monom_of_set Y = 0
k \<noteq> 0

goal (1 subgoal):
 1. MPoly_Type.coeff (sym_mpoly X k) 0 = (if finite X \<and> k = 0 then 1::'a else (0::'a))
[PROOF STEP]
by (auto simp: coeff_sym_mpoly)
[PROOF STATE]
proof (state)
this:
MPoly_Type.coeff (sym_mpoly X k) 0 = (if finite X \<and> k = 0 then 1::'a else (0::'a))

goal (1 subgoal):
 1. infinite X \<Longrightarrow> MPoly_Type.coeff (sym_mpoly X k) 0 = (if finite X \<and> k = 0 then 1::'a else (0::'a))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. infinite X \<Longrightarrow> MPoly_Type.coeff (sym_mpoly X k) 0 = (if finite X \<and> k = 0 then 1::'a else (0::'a))
[PROOF STEP]
assume "infinite X"
[PROOF STATE]
proof (state)
this:
infinite X

goal (1 subgoal):
 1. infinite X \<Longrightarrow> MPoly_Type.coeff (sym_mpoly X k) 0 = (if finite X \<and> k = 0 then 1::'a else (0::'a))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
infinite X

goal (1 subgoal):
 1. MPoly_Type.coeff (sym_mpoly X k) 0 = (if finite X \<and> k = 0 then 1::'a else (0::'a))
[PROOF STEP]
by (simp add: coeff_sym_mpoly)
[PROOF STATE]
proof (state)
this:
MPoly_Type.coeff (sym_mpoly X k) 0 = (if finite X \<and> k = 0 then 1::'a else (0::'a))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
MPoly_Type.coeff (sym_mpoly X k) 0 = (if finite X \<and> k = 0 then 1::'a else (0::'a))

goal:
No subgoals!
[PROOF STEP]
qed