[STATEMENT]
lemma sym_mpoly_representation_unique_aux:
  fixes p :: "'a mpoly mpoly"
  assumes "finite A" "insertion (sym_mpoly A) p = 0"
          "\<And>m. vars (coeff p m) \<inter> A = {}" "vars p \<subseteq> {1..n}"
  shows   "p = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p = 0
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
assume p: "p \<noteq> 0"
[PROOF STATE]
proof (state)
this:
p \<noteq> 0

goal (1 subgoal):
 1. p \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
have xs: "set xs = A" "distinct xs" "sorted xs" and [simp]: "length xs = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (set xs = A &&& distinct xs &&& sorted xs) &&& length xs = n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite A
insertion (sym_mpoly A) p = 0
vars (MPoly_Type.coeff p ?m) \<inter> A = {}
vars p \<subseteq> {1..n}

goal (1 subgoal):
 1. (set xs = A &&& distinct xs &&& sorted xs) &&& length xs = n
[PROOF STEP]
by (auto simp: xs_def n_def)
[PROOF STATE]
proof (state)
this:
set xs = A
distinct xs
sorted xs
length xs = n

goal (1 subgoal):
 1. p \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
define h where "h = (\<lambda>m. coeff p m * (\<Prod>i. sym_mpoly A i ^ lookup m i))"
[PROOF STATE]
proof (state)
this:
h = (\<lambda>m. MPoly_Type.coeff p m * (\<Prod>i. sym_mpoly A i ^ lookup m i))

goal (1 subgoal):
 1. p \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
define M where "M = {m. coeff p m \<noteq> 0}"
[PROOF STATE]
proof (state)
this:
M = {m. MPoly_Type.coeff p m \<noteq> 0}

goal (1 subgoal):
 1. p \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
define maxm where "maxm = Max ((lead_monom \<circ> h) ` M)"
[PROOF STATE]
proof (state)
this:
maxm = Max ((lead_monom \<circ> h) ` M)

goal (1 subgoal):
 1. p \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
have "finite M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite M
[PROOF STEP]
by (auto intro!: finite_subset[OF _ finite_coeff_support[of p]] simp: h_def M_def)
[PROOF STATE]
proof (state)
this:
finite M

goal (1 subgoal):
 1. p \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
have keys_subset: "keys m \<subseteq> {1..n}" if "coeff p m \<noteq> 0" for m
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. keys m \<subseteq> {1..n}
[PROOF STEP]
using that assms coeff_notin_vars[of m p]
[PROOF STATE]
proof (prove)
using this:
MPoly_Type.coeff p m \<noteq> 0
finite A
insertion (sym_mpoly A) p = 0
vars (MPoly_Type.coeff p ?m) \<inter> A = {}
vars p \<subseteq> {1..n}
\<not> keys m \<subseteq> vars p \<Longrightarrow> MPoly_Type.coeff p m = 0

goal (1 subgoal):
 1. keys m \<subseteq> {1..n}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
MPoly_Type.coeff p ?m \<noteq> 0 \<Longrightarrow> keys ?m \<subseteq> {1..n}

goal (1 subgoal):
 1. p \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
have lead_coeff: "lead_coeff (h m) = lead_coeff (coeff p m)" (is ?th1)
   and lead_monom: "lead_monom (h m) = lead_monom (coeff p m) +
                      lead_monom (\<Prod>i. sym_mpoly A i ^ lookup m i :: 'a mpoly)" (is ?th2)
   if [simp]: "coeff p m \<noteq> 0" for m
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Symmetric_Polynomials.lead_coeff (h m) = Symmetric_Polynomials.lead_coeff (MPoly_Type.coeff p m) &&& lead_monom (h m) = lead_monom (MPoly_Type.coeff p m) + lead_monom (\<Prod>i. sym_mpoly A i ^ lookup m i)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Symmetric_Polynomials.lead_coeff (h m) = Symmetric_Polynomials.lead_coeff (MPoly_Type.coeff p m)
 2. lead_monom (h m) = lead_monom (MPoly_Type.coeff p m) + lead_monom (\<Prod>i. sym_mpoly A i ^ lookup m i)
[PROOF STEP]
have "(\<Prod>i. sym_mpoly A i ^ lookup m i :: 'a mpoly) =
            (\<Prod>i | lookup m i \<noteq> 0. sym_mpoly A i ^ lookup m i :: 'a mpoly)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>i. sym_mpoly A i ^ lookup m i) = (\<Prod>i\<in>{i. lookup m i \<noteq> 0}. sym_mpoly A i ^ lookup m i)
[PROOF STEP]
by (intro Prod_any.expand_superset) (auto intro!: Nat.gr0I)
[PROOF STATE]
proof (state)
this:
(\<Prod>i. sym_mpoly A i ^ lookup m i) = (\<Prod>i\<in>{i. lookup m i \<noteq> 0}. sym_mpoly A i ^ lookup m i)

goal (2 subgoals):
 1. Symmetric_Polynomials.lead_coeff (h m) = Symmetric_Polynomials.lead_coeff (MPoly_Type.coeff p m)
 2. lead_monom (h m) = lead_monom (MPoly_Type.coeff p m) + lead_monom (\<Prod>i. sym_mpoly A i ^ lookup m i)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Prod>i. sym_mpoly A i ^ lookup m i) = (\<Prod>i\<in>{i. lookup m i \<noteq> 0}. sym_mpoly A i ^ lookup m i)

goal (2 subgoals):
 1. Symmetric_Polynomials.lead_coeff (h m) = Symmetric_Polynomials.lead_coeff (MPoly_Type.coeff p m)
 2. lead_monom (h m) = lead_monom (MPoly_Type.coeff p m) + lead_monom (\<Prod>i. sym_mpoly A i ^ lookup m i)
[PROOF STEP]
have "lead_coeff \<dots> = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Symmetric_Polynomials.lead_coeff (\<Prod>i\<in>{i. lookup m i \<noteq> 0}. sym_mpoly A i ^ lookup m i) = (1::'a)
[PROOF STEP]
using assms keys_subset[of m]
[PROOF STATE]
proof (prove)
using this:
finite A
insertion (sym_mpoly A) p = 0
vars (MPoly_Type.coeff p ?m) \<inter> A = {}
vars p \<subseteq> {1..n}
MPoly_Type.coeff p m \<noteq> 0 \<Longrightarrow> keys m \<subseteq> {1..n}

goal (1 subgoal):
 1. Symmetric_Polynomials.lead_coeff (\<Prod>i\<in>{i. lookup m i \<noteq> 0}. sym_mpoly A i ^ lookup m i) = (1::'a)
[PROOF STEP]
by (intro lead_coeff_sym_mpoly_powerprod) (auto simp: in_keys_iff subset_iff n_def)
[PROOF STATE]
proof (state)
this:
Symmetric_Polynomials.lead_coeff (\<Prod>i\<in>{i. lookup m i \<noteq> 0}. sym_mpoly A i ^ lookup m i) = (1::'a)

goal (2 subgoals):
 1. Symmetric_Polynomials.lead_coeff (h m) = Symmetric_Polynomials.lead_coeff (MPoly_Type.coeff p m)
 2. lead_monom (h m) = lead_monom (MPoly_Type.coeff p m) + lead_monom (\<Prod>i. sym_mpoly A i ^ lookup m i)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
Symmetric_Polynomials.lead_coeff (\<Prod>i. sym_mpoly A i ^ lookup m i) = (1::'a)
[PROOF STEP]
have eq: "lead_coeff (\<Prod>i. sym_mpoly A i ^ lookup m i :: 'a mpoly) = 1"
[PROOF STATE]
proof (prove)
using this:
Symmetric_Polynomials.lead_coeff (\<Prod>i. sym_mpoly A i ^ lookup m i) = (1::'a)

goal (1 subgoal):
 1. Symmetric_Polynomials.lead_coeff (\<Prod>i. sym_mpoly A i ^ lookup m i) = (1::'a)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
Symmetric_Polynomials.lead_coeff (\<Prod>i. sym_mpoly A i ^ lookup m i) = (1::'a)

goal (2 subgoals):
 1. Symmetric_Polynomials.lead_coeff (h m) = Symmetric_Polynomials.lead_coeff (MPoly_Type.coeff p m)
 2. lead_monom (h m) = lead_monom (MPoly_Type.coeff p m) + lead_monom (\<Prod>i. sym_mpoly A i ^ lookup m i)
[PROOF STEP]
thus ?th1
[PROOF STATE]
proof (prove)
using this:
Symmetric_Polynomials.lead_coeff (\<Prod>i. sym_mpoly A i ^ lookup m i) = (1::'a)

goal (1 subgoal):
 1. Symmetric_Polynomials.lead_coeff (h m) = Symmetric_Polynomials.lead_coeff (MPoly_Type.coeff p m)
[PROOF STEP]
unfolding h_def
[PROOF STATE]
proof (prove)
using this:
Symmetric_Polynomials.lead_coeff (\<Prod>i. sym_mpoly A i ^ lookup m i) = (1::'a)

goal (1 subgoal):
 1. Symmetric_Polynomials.lead_coeff (MPoly_Type.coeff p m * (\<Prod>i. sym_mpoly A i ^ lookup m i)) = Symmetric_Polynomials.lead_coeff (MPoly_Type.coeff p m)
[PROOF STEP]
using \<open>coeff p m \<noteq> 0\<close>
[PROOF STATE]
proof (prove)
using this:
Symmetric_Polynomials.lead_coeff (\<Prod>i. sym_mpoly A i ^ lookup m i) = (1::'a)
MPoly_Type.coeff p m \<noteq> 0

goal (1 subgoal):
 1. Symmetric_Polynomials.lead_coeff (MPoly_Type.coeff p m * (\<Prod>i. sym_mpoly A i ^ lookup m i)) = Symmetric_Polynomials.lead_coeff (MPoly_Type.coeff p m)
[PROOF STEP]
by (subst lead_coeff_mult) auto
[PROOF STATE]
proof (state)
this:
Symmetric_Polynomials.lead_coeff (h m) = Symmetric_Polynomials.lead_coeff (MPoly_Type.coeff p m)

goal (1 subgoal):
 1. lead_monom (h m) = lead_monom (MPoly_Type.coeff p m) + lead_monom (\<Prod>i. sym_mpoly A i ^ lookup m i)
[PROOF STEP]
show ?th2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lead_monom (h m) = lead_monom (MPoly_Type.coeff p m) + lead_monom (\<Prod>i. sym_mpoly A i ^ lookup m i)
[PROOF STEP]
unfolding h_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lead_monom (MPoly_Type.coeff p m * (\<Prod>i. sym_mpoly A i ^ lookup m i)) = lead_monom (MPoly_Type.coeff p m) + lead_monom (\<Prod>i. sym_mpoly A i ^ lookup m i)
[PROOF STEP]
by (subst lead_monom_mult) (auto simp: eq)
[PROOF STATE]
proof (state)
this:
lead_monom (h m) = lead_monom (MPoly_Type.coeff p m) + lead_monom (\<Prod>i. sym_mpoly A i ^ lookup m i)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
MPoly_Type.coeff p ?m \<noteq> 0 \<Longrightarrow> Symmetric_Polynomials.lead_coeff (h ?m) = Symmetric_Polynomials.lead_coeff (MPoly_Type.coeff p ?m)
MPoly_Type.coeff p ?m \<noteq> 0 \<Longrightarrow> lead_monom (h ?m) = lead_monom (MPoly_Type.coeff p ?m) + lead_monom (\<Prod>i. sym_mpoly A i ^ lookup ?m i)

goal (1 subgoal):
 1. p \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
have "insertion (sym_mpoly A) p = (\<Sum>m\<in>M. h m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion (sym_mpoly A) p = sum h M
[PROOF STEP]
unfolding insertion_altdef h_def M_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>m. MPoly_Type.coeff p m * (\<Prod>i. sym_mpoly A i ^ lookup m i)) = (\<Sum>m | MPoly_Type.coeff p m \<noteq> 0. MPoly_Type.coeff p m * (\<Prod>i. sym_mpoly A i ^ lookup m i))
[PROOF STEP]
by (intro Sum_any.expand_superset) auto
[PROOF STATE]
proof (state)
this:
insertion (sym_mpoly A) p = sum h M

goal (1 subgoal):
 1. p \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
insertion (sym_mpoly A) p = sum h M

goal (1 subgoal):
 1. p \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
have "lead_monom \<dots> = maxm"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lead_monom (sum h M) = maxm
[PROOF STEP]
unfolding maxm_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lead_monom (sum h M) = Max ((lead_monom \<circ> h) ` M)
[PROOF STEP]
proof (rule lead_monom_sum)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. inj_on (lead_monom \<circ> h) M
 2. finite M
 3. M \<noteq> {}
 4. \<And>m. m \<in> M \<Longrightarrow> h m \<noteq> 0
[PROOF STEP]
from p
[PROOF STATE]
proof (chain)
picking this:
p \<noteq> 0
[PROOF STEP]
obtain m where "coeff p m \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
p \<noteq> 0

goal (1 subgoal):
 1. (\<And>m. MPoly_Type.coeff p m \<noteq> 0 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using mpoly_eqI[of p 0]
[PROOF STATE]
proof (prove)
using this:
p \<noteq> 0
(\<And>mon. MPoly_Type.coeff p mon = MPoly_Type.coeff 0 mon) \<Longrightarrow> p = 0

goal (1 subgoal):
 1. (\<And>m. MPoly_Type.coeff p m \<noteq> 0 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
MPoly_Type.coeff p m \<noteq> 0

goal (4 subgoals):
 1. inj_on (lead_monom \<circ> h) M
 2. finite M
 3. M \<noteq> {}
 4. \<And>m. m \<in> M \<Longrightarrow> h m \<noteq> 0
[PROOF STEP]
hence "m \<in> M"
[PROOF STATE]
proof (prove)
using this:
MPoly_Type.coeff p m \<noteq> 0

goal (1 subgoal):
 1. m \<in> M
[PROOF STEP]
using \<open>coeff p m \<noteq> 0\<close> lead_coeff[of m]
[PROOF STATE]
proof (prove)
using this:
MPoly_Type.coeff p m \<noteq> 0
MPoly_Type.coeff p m \<noteq> 0
MPoly_Type.coeff p m \<noteq> 0 \<Longrightarrow> Symmetric_Polynomials.lead_coeff (h m) = Symmetric_Polynomials.lead_coeff (MPoly_Type.coeff p m)

goal (1 subgoal):
 1. m \<in> M
[PROOF STEP]
by (auto simp: M_def)
[PROOF STATE]
proof (state)
this:
m \<in> M

goal (4 subgoals):
 1. inj_on (lead_monom \<circ> h) M
 2. finite M
 3. M \<noteq> {}
 4. \<And>m. m \<in> M \<Longrightarrow> h m \<noteq> 0
[PROOF STEP]
thus "M \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
m \<in> M

goal (1 subgoal):
 1. M \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
M \<noteq> {}

goal (3 subgoals):
 1. inj_on (lead_monom \<circ> h) M
 2. finite M
 3. \<And>m. m \<in> M \<Longrightarrow> h m \<noteq> 0
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. inj_on (lead_monom \<circ> h) M
 2. finite M
 3. \<And>m. m \<in> M \<Longrightarrow> h m \<noteq> 0
[PROOF STEP]
have restrict_lead_monom:
           "restrictpm A (lead_monom (h m)) =
             lead_monom (\<Prod>i. sym_mpoly A i ^ lookup m i :: 'a mpoly)"
      if [simp]: "coeff p m \<noteq> 0" for m
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. restrictpm A (lead_monom (h m)) = lead_monom (\<Prod>i. sym_mpoly A i ^ lookup m i)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. restrictpm A (lead_monom (h m)) = lead_monom (\<Prod>i. sym_mpoly A i ^ lookup m i)
[PROOF STEP]
have "restrictpm A (lead_monom (h m)) =
              restrictpm A (lead_monom (coeff p m)) +
              restrictpm A (lead_monom (\<Prod>i. sym_mpoly A i ^ lookup m i :: 'a mpoly))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. restrictpm A (lead_monom (h m)) = restrictpm A (lead_monom (MPoly_Type.coeff p m)) + restrictpm A (lead_monom (\<Prod>i. sym_mpoly A i ^ lookup m i))
[PROOF STEP]
by (auto simp: lead_monom restrictpm_add)
[PROOF STATE]
proof (state)
this:
restrictpm A (lead_monom (h m)) = restrictpm A (lead_monom (MPoly_Type.coeff p m)) + restrictpm A (lead_monom (\<Prod>i. sym_mpoly A i ^ lookup m i))

goal (1 subgoal):
 1. restrictpm A (lead_monom (h m)) = lead_monom (\<Prod>i. sym_mpoly A i ^ lookup m i)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
restrictpm A (lead_monom (h m)) = restrictpm A (lead_monom (MPoly_Type.coeff p m)) + restrictpm A (lead_monom (\<Prod>i. sym_mpoly A i ^ lookup m i))

goal (1 subgoal):
 1. restrictpm A (lead_monom (h m)) = lead_monom (\<Prod>i. sym_mpoly A i ^ lookup m i)
[PROOF STEP]
have "restrictpm A (lead_monom (coeff p m)) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. restrictpm A (lead_monom (MPoly_Type.coeff p m)) = 0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite A
insertion (sym_mpoly A) p = 0
vars (MPoly_Type.coeff p ?m) \<inter> A = {}
vars p \<subseteq> {1..n}

goal (1 subgoal):
 1. restrictpm A (lead_monom (MPoly_Type.coeff p m)) = 0
[PROOF STEP]
by (intro restrictpm_orthogonal order.trans[OF keys_lead_monom_subset]) auto
[PROOF STATE]
proof (state)
this:
restrictpm A (lead_monom (MPoly_Type.coeff p m)) = 0

goal (1 subgoal):
 1. restrictpm A (lead_monom (h m)) = lead_monom (\<Prod>i. sym_mpoly A i ^ lookup m i)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
restrictpm A (lead_monom (MPoly_Type.coeff p m)) = 0

goal (1 subgoal):
 1. restrictpm A (lead_monom (h m)) = lead_monom (\<Prod>i. sym_mpoly A i ^ lookup m i)
[PROOF STEP]
have "restrictpm A (lead_monom (\<Prod>i. sym_mpoly A i ^ lookup m i :: 'a mpoly)) =
                   lead_monom (\<Prod>i. sym_mpoly A i ^ lookup m i :: 'a mpoly)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. restrictpm A (lead_monom (\<Prod>i. sym_mpoly A i ^ lookup m i)) = lead_monom (\<Prod>i. sym_mpoly A i ^ lookup m i)
[PROOF STEP]
by (intro restrictpm_id order.trans[OF keys_lead_monom_subset]
                  order.trans[OF vars_Prod_any] UN_least order.trans[OF vars_power]
                  vars_sym_mpoly_subset)
[PROOF STATE]
proof (state)
this:
restrictpm A (lead_monom (\<Prod>i. sym_mpoly A i ^ lookup m i)) = lead_monom (\<Prod>i. sym_mpoly A i ^ lookup m i)

goal (1 subgoal):
 1. restrictpm A (lead_monom (h m)) = lead_monom (\<Prod>i. sym_mpoly A i ^ lookup m i)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
restrictpm A (lead_monom (h m)) = 0 + lead_monom (\<Prod>i. sym_mpoly A i ^ lookup m i)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
restrictpm A (lead_monom (h m)) = 0 + lead_monom (\<Prod>i. sym_mpoly A i ^ lookup m i)

goal (1 subgoal):
 1. restrictpm A (lead_monom (h m)) = lead_monom (\<Prod>i. sym_mpoly A i ^ lookup m i)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
restrictpm A (lead_monom (h m)) = lead_monom (\<Prod>i. sym_mpoly A i ^ lookup m i)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
MPoly_Type.coeff p ?m \<noteq> 0 \<Longrightarrow> restrictpm A (lead_monom (h ?m)) = lead_monom (\<Prod>i. sym_mpoly A i ^ lookup ?m i)

goal (3 subgoals):
 1. inj_on (lead_monom \<circ> h) M
 2. finite M
 3. \<And>m. m \<in> M \<Longrightarrow> h m \<noteq> 0
[PROOF STEP]
show "inj_on (lead_monom \<circ> h) M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (lead_monom \<circ> h) M
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> M; y \<in> M; (lead_monom \<circ> h) x = (lead_monom \<circ> h) y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
fix m1 m2
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> M; y \<in> M; (lead_monom \<circ> h) x = (lead_monom \<circ> h) y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
assume m12: "m1 \<in> M" "m2 \<in> M" "(lead_monom \<circ> h) m1 = (lead_monom \<circ> h) m2"
[PROOF STATE]
proof (state)
this:
m1 \<in> M
m2 \<in> M
(lead_monom \<circ> h) m1 = (lead_monom \<circ> h) m2

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> M; y \<in> M; (lead_monom \<circ> h) x = (lead_monom \<circ> h) y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
hence [simp]: "coeff p m1 \<noteq> 0" "coeff p m2 \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
m1 \<in> M
m2 \<in> M
(lead_monom \<circ> h) m1 = (lead_monom \<circ> h) m2

goal (1 subgoal):
 1. MPoly_Type.coeff p m1 \<noteq> 0 &&& MPoly_Type.coeff p m2 \<noteq> 0
[PROOF STEP]
by (auto simp: M_def h_def)
[PROOF STATE]
proof (state)
this:
MPoly_Type.coeff p m1 \<noteq> 0
MPoly_Type.coeff p m2 \<noteq> 0

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> M; y \<in> M; (lead_monom \<circ> h) x = (lead_monom \<circ> h) y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
have "restrictpm A (lead_monom (h m1)) = restrictpm A (lead_monom (h m2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. restrictpm A (lead_monom (h m1)) = restrictpm A (lead_monom (h m2))
[PROOF STEP]
using m12
[PROOF STATE]
proof (prove)
using this:
m1 \<in> M
m2 \<in> M
(lead_monom \<circ> h) m1 = (lead_monom \<circ> h) m2

goal (1 subgoal):
 1. restrictpm A (lead_monom (h m1)) = restrictpm A (lead_monom (h m2))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
restrictpm A (lead_monom (h m1)) = restrictpm A (lead_monom (h m2))

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> M; y \<in> M; (lead_monom \<circ> h) x = (lead_monom \<circ> h) y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
hence "lead_monom (\<Prod>i. sym_mpoly A i ^ lookup m1 i :: 'a mpoly) =
               lead_monom (\<Prod>i. sym_mpoly A i ^ lookup m2 i :: 'a mpoly)"
[PROOF STATE]
proof (prove)
using this:
restrictpm A (lead_monom (h m1)) = restrictpm A (lead_monom (h m2))

goal (1 subgoal):
 1. lead_monom (\<Prod>i. sym_mpoly A i ^ lookup m1 i) = lead_monom (\<Prod>i. sym_mpoly A i ^ lookup m2 i)
[PROOF STEP]
by (simp add: restrict_lead_monom)
[PROOF STATE]
proof (state)
this:
lead_monom (\<Prod>i. sym_mpoly A i ^ lookup m1 i) = lead_monom (\<Prod>i. sym_mpoly A i ^ lookup m2 i)

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> M; y \<in> M; (lead_monom \<circ> h) x = (lead_monom \<circ> h) y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
thus "m1 = m2"
[PROOF STATE]
proof (prove)
using this:
lead_monom (\<Prod>i. sym_mpoly A i ^ lookup m1 i) = lead_monom (\<Prod>i. sym_mpoly A i ^ lookup m2 i)

goal (1 subgoal):
 1. m1 = m2
[PROOF STEP]
by (rule lead_monom_sym_poly_powerprod_inj)
           (use \<open>finite A\<close> keys_subset[of m1] keys_subset[of m2] in auto)
[PROOF STATE]
proof (state)
this:
m1 = m2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
inj_on (lead_monom \<circ> h) M

goal (2 subgoals):
 1. finite M
 2. \<And>m. m \<in> M \<Longrightarrow> h m \<noteq> 0
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. finite M
 2. \<And>m. m \<in> M \<Longrightarrow> h m \<noteq> 0
[PROOF STEP]
fix m
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. finite M
 2. \<And>m. m \<in> M \<Longrightarrow> h m \<noteq> 0
[PROOF STEP]
assume "m \<in> M"
[PROOF STATE]
proof (state)
this:
m \<in> M

goal (2 subgoals):
 1. finite M
 2. \<And>m. m \<in> M \<Longrightarrow> h m \<noteq> 0
[PROOF STEP]
hence "lead_coeff (h m) = lead_coeff (coeff p m)"
[PROOF STATE]
proof (prove)
using this:
m \<in> M

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

goal (2 subgoals):
 1. finite M
 2. \<And>m. m \<in> M \<Longrightarrow> h m \<noteq> 0
[PROOF STEP]
with \<open>m \<in> M\<close>
[PROOF STATE]
proof (chain)
picking this:
m \<in> M
Symmetric_Polynomials.lead_coeff (h m) = Symmetric_Polynomials.lead_coeff (MPoly_Type.coeff p m)
[PROOF STEP]
show "h m \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
m \<in> M
Symmetric_Polynomials.lead_coeff (h m) = Symmetric_Polynomials.lead_coeff (MPoly_Type.coeff p m)

goal (1 subgoal):
 1. h m \<noteq> 0
[PROOF STEP]
by (auto simp: M_def)
[PROOF STATE]
proof (state)
this:
h m \<noteq> 0

goal (1 subgoal):
 1. finite M
[PROOF STEP]
qed fact+
[PROOF STATE]
proof (state)
this:
lead_monom (sum h M) = maxm

goal (1 subgoal):
 1. p \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
lead_monom (insertion (sym_mpoly A) p) = maxm
[PROOF STEP]
have "maxm = 0"
[PROOF STATE]
proof (prove)
using this:
lead_monom (insertion (sym_mpoly A) p) = maxm

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

goal (1 subgoal):
 1. p \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
have only_zero: "m = 0" if "m \<in> M" for m
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m = 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. m = 0
[PROOF STEP]
from that
[PROOF STATE]
proof (chain)
picking this:
m \<in> M
[PROOF STEP]
have nz [simp]: "coeff p m \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
m \<in> M

goal (1 subgoal):
 1. MPoly_Type.coeff p m \<noteq> 0
[PROOF STEP]
by (auto simp: M_def h_def)
[PROOF STATE]
proof (state)
this:
MPoly_Type.coeff p m \<noteq> 0

goal (1 subgoal):
 1. m = 0
[PROOF STEP]
from that
[PROOF STATE]
proof (chain)
picking this:
m \<in> M
[PROOF STEP]
have "(lead_monom \<circ> h) m \<le> maxm"
[PROOF STATE]
proof (prove)
using this:
m \<in> M

goal (1 subgoal):
 1. (lead_monom \<circ> h) m \<le> maxm
[PROOF STEP]
using \<open>finite M\<close>
[PROOF STATE]
proof (prove)
using this:
m \<in> M
finite M

goal (1 subgoal):
 1. (lead_monom \<circ> h) m \<le> maxm
[PROOF STEP]
unfolding maxm_def
[PROOF STATE]
proof (prove)
using this:
m \<in> M
finite M

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

goal (1 subgoal):
 1. m = 0
[PROOF STEP]
with \<open>maxm = 0\<close>
[PROOF STATE]
proof (chain)
picking this:
maxm = 0
(lead_monom \<circ> h) m \<le> maxm
[PROOF STEP]
have [simp]: "lead_monom (h m) = 0"
[PROOF STATE]
proof (prove)
using this:
maxm = 0
(lead_monom \<circ> h) m \<le> maxm

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

goal (1 subgoal):
 1. m = 0
[PROOF STEP]
have lookup_nzD: "k \<in> {1..n}" if "lookup m k \<noteq> 0" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k \<in> {1..n}
[PROOF STEP]
using keys_subset[of m] that
[PROOF STATE]
proof (prove)
using this:
MPoly_Type.coeff p m \<noteq> 0 \<Longrightarrow> keys m \<subseteq> {1..n}
lookup m k \<noteq> 0

goal (1 subgoal):
 1. k \<in> {1..n}
[PROOF STEP]
by (auto simp: in_keys_iff subset_iff)
[PROOF STATE]
proof (state)
this:
lookup m ?k \<noteq> 0 \<Longrightarrow> ?k \<in> {1..n}

goal (1 subgoal):
 1. m = 0
[PROOF STEP]
have "lead_monom (coeff p m) + 0 \<le> lead_monom (h m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lead_monom (MPoly_Type.coeff p m) + 0 \<le> lead_monom (h m)
[PROOF STEP]
unfolding lead_monom[OF nz]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lead_monom (MPoly_Type.coeff p m) + 0 \<le> lead_monom (MPoly_Type.coeff p m) + lead_monom (\<Prod>i. sym_mpoly A i ^ lookup m i)
[PROOF STEP]
by (intro add_left_mono) auto
[PROOF STATE]
proof (state)
this:
lead_monom (MPoly_Type.coeff p m) + 0 \<le> lead_monom (h m)

goal (1 subgoal):
 1. m = 0
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lead_monom (MPoly_Type.coeff p m) + 0 \<le> lead_monom (h m)

goal (1 subgoal):
 1. m = 0
[PROOF STEP]
have "\<dots> = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lead_monom (h m) = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lead_monom (h m) = 0

goal (1 subgoal):
 1. m = 0
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
lead_monom (MPoly_Type.coeff p m) + 0 \<le> 0
[PROOF STEP]
have lead_monom_0: "lead_monom (coeff p m) = 0"
[PROOF STATE]
proof (prove)
using this:
lead_monom (MPoly_Type.coeff p m) + 0 \<le> 0

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

goal (1 subgoal):
 1. m = 0
[PROOF STEP]
have "sum (lookup m) {1..n} = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum (lookup m) {1..n} = 0
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sum (lookup m) {1..n} \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
assume "sum (lookup m) {1..n} \<noteq> 0"
[PROOF STATE]
proof (state)
this:
sum (lookup m) {1..n} \<noteq> 0

goal (1 subgoal):
 1. sum (lookup m) {1..n} \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
hence "sum (lookup m) {1..n} > 0"
[PROOF STATE]
proof (prove)
using this:
sum (lookup m) {1..n} \<noteq> 0

goal (1 subgoal):
 1. 0 < sum (lookup m) {1..n}
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
0 < sum (lookup m) {1..n}

goal (1 subgoal):
 1. sum (lookup m) {1..n} \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
have "0 \<noteq> lead_coeff (MPoly_Type.coeff p m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<noteq> Symmetric_Polynomials.lead_coeff (MPoly_Type.coeff p m)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(0::'a) \<noteq> Symmetric_Polynomials.lead_coeff (MPoly_Type.coeff p m)

goal (1 subgoal):
 1. sum (lookup m) {1..n} \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(0::'a) \<noteq> Symmetric_Polynomials.lead_coeff (MPoly_Type.coeff p m)

goal (1 subgoal):
 1. sum (lookup m) {1..n} \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
have "lead_coeff (MPoly_Type.coeff p m) = lead_coeff (h m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Symmetric_Polynomials.lead_coeff (MPoly_Type.coeff p m) = Symmetric_Polynomials.lead_coeff (h m)
[PROOF STEP]
by (simp add: lead_coeff)
[PROOF STATE]
proof (state)
this:
Symmetric_Polynomials.lead_coeff (MPoly_Type.coeff p m) = Symmetric_Polynomials.lead_coeff (h m)

goal (1 subgoal):
 1. sum (lookup m) {1..n} \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Symmetric_Polynomials.lead_coeff (MPoly_Type.coeff p m) = Symmetric_Polynomials.lead_coeff (h m)

goal (1 subgoal):
 1. sum (lookup m) {1..n} \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
have "lead_coeff (h m) = coeff (h m) 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Symmetric_Polynomials.lead_coeff (h m) = MPoly_Type.coeff (h m) 0
[PROOF STEP]
by (simp add: lead_coeff_def)
[PROOF STATE]
proof (state)
this:
Symmetric_Polynomials.lead_coeff (h m) = MPoly_Type.coeff (h m) 0

goal (1 subgoal):
 1. sum (lookup m) {1..n} \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Symmetric_Polynomials.lead_coeff (h m) = MPoly_Type.coeff (h m) 0

goal (1 subgoal):
 1. sum (lookup m) {1..n} \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
have "\<dots> = coeff (coeff p m) 0 * coeff (\<Prod>i. sym_mpoly A i ^ lookup m i) 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MPoly_Type.coeff (h m) 0 = MPoly_Type.coeff (MPoly_Type.coeff p m) 0 * MPoly_Type.coeff (\<Prod>i. sym_mpoly A i ^ lookup m i) 0
[PROOF STEP]
by (simp add: h_def mpoly_coeff_times_0)
[PROOF STATE]
proof (state)
this:
MPoly_Type.coeff (h m) 0 = MPoly_Type.coeff (MPoly_Type.coeff p m) 0 * MPoly_Type.coeff (\<Prod>i. sym_mpoly A i ^ lookup m i) 0

goal (1 subgoal):
 1. sum (lookup m) {1..n} \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
MPoly_Type.coeff (h m) 0 = MPoly_Type.coeff (MPoly_Type.coeff p m) 0 * MPoly_Type.coeff (\<Prod>i. sym_mpoly A i ^ lookup m i) 0

goal (1 subgoal):
 1. sum (lookup m) {1..n} \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
have "(\<Prod>i. sym_mpoly A i ^ lookup m i) = (\<Prod>i=1..n. sym_mpoly A i ^ lookup m i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>i. sym_mpoly A i ^ lookup m i) = (\<Prod>i = 1..n. sym_mpoly A i ^ lookup m i)
[PROOF STEP]
by (intro Prod_any.expand_superset subsetI lookup_nzD) (auto intro!: Nat.gr0I)
[PROOF STATE]
proof (state)
this:
(\<Prod>i. sym_mpoly A i ^ lookup m i) = (\<Prod>i = 1..n. sym_mpoly A i ^ lookup m i)

goal (1 subgoal):
 1. sum (lookup m) {1..n} \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Prod>i. sym_mpoly A i ^ lookup m i) = (\<Prod>i = 1..n. sym_mpoly A i ^ lookup m i)

goal (1 subgoal):
 1. sum (lookup m) {1..n} \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
have "coeff \<dots> 0 = (\<Prod>i=1..n. 0 ^ lookup m i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MPoly_Type.coeff (\<Prod>i = 1..n. sym_mpoly A i ^ lookup m i) 0 = (\<Prod>i = 1..n. (0::'b) ^ lookup m i)
[PROOF STEP]
unfolding mpoly_coeff_prod_0 mpoly_coeff_power_0
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>x = 1..n. MPoly_Type.coeff (sym_mpoly A x) 0 ^ lookup m x) = (\<Prod>i = 1..n. (0::'b) ^ lookup m i)
[PROOF STEP]
by (intro prod.cong) (auto simp: coeff_sym_mpoly_0)
[PROOF STATE]
proof (state)
this:
MPoly_Type.coeff (\<Prod>i = 1..n. sym_mpoly A i ^ lookup m i) 0 = (\<Prod>i = 1..n. (0::?'b2) ^ lookup m i)

goal (1 subgoal):
 1. sum (lookup m) {1..n} \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
MPoly_Type.coeff (\<Prod>i = 1..n. sym_mpoly A i ^ lookup m i) 0 = (\<Prod>i = 1..n. (0::?'b2) ^ lookup m i)

goal (1 subgoal):
 1. sum (lookup m) {1..n} \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
have "\<dots> = 0 ^ (\<Sum>i=1..n. lookup m i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>i = 1..n. (0::'b) ^ lookup m i) = (0::'b) ^ sum (lookup m) {1..n}
[PROOF STEP]
by (simp add: power_sum)
[PROOF STATE]
proof (state)
this:
(\<Prod>i = 1..n. (0::?'b3) ^ lookup m i) = (0::?'b3) ^ sum (lookup m) {1..n}

goal (1 subgoal):
 1. sum (lookup m) {1..n} \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Prod>i = 1..n. (0::?'b3) ^ lookup m i) = (0::?'b3) ^ sum (lookup m) {1..n}

goal (1 subgoal):
 1. sum (lookup m) {1..n} \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
have "\<dots> = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'b) ^ sum (lookup m) {1..n} = (0::'b)
[PROOF STEP]
using zero_power[OF \<open>sum (lookup m) {1..n} > 0\<close>]
[PROOF STATE]
proof (prove)
using this:
(0::?'a) ^ sum (lookup m) {1..n} = (0::?'a)

goal (1 subgoal):
 1. (0::'b) ^ sum (lookup m) {1..n} = (0::'b)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(0::?'b4) ^ sum (lookup m) {1..n} = (0::?'b4)

goal (1 subgoal):
 1. sum (lookup m) {1..n} \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(0::'a) \<noteq> MPoly_Type.coeff (MPoly_Type.coeff p m) 0 * (0::'a)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
(0::'a) \<noteq> MPoly_Type.coeff (MPoly_Type.coeff p m) 0 * (0::'a)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sum (lookup m) {1..n} = 0

goal (1 subgoal):
 1. m = 0
[PROOF STEP]
hence "lookup m k = 0" for k
[PROOF STATE]
proof (prove)
using this:
sum (lookup m) {1..n} = 0

goal (1 subgoal):
 1. lookup m k = 0
[PROOF STEP]
using keys_subset[of m]
[PROOF STATE]
proof (prove)
using this:
sum (lookup m) {1..n} = 0
MPoly_Type.coeff p m \<noteq> 0 \<Longrightarrow> keys m \<subseteq> {1..n}

goal (1 subgoal):
 1. lookup m k = 0
[PROOF STEP]
by (cases "k \<in> {1..n}") (auto simp: in_keys_iff)
[PROOF STATE]
proof (state)
this:
lookup m ?k = 0

goal (1 subgoal):
 1. m = 0
[PROOF STEP]
thus "m = 0"
[PROOF STATE]
proof (prove)
using this:
lookup m ?k = 0

goal (1 subgoal):
 1. m = 0
[PROOF STEP]
by (intro poly_mapping_eqI) auto
[PROOF STATE]
proof (state)
this:
m = 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?m \<in> M \<Longrightarrow> ?m = 0

goal (1 subgoal):
 1. p \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
have "0 = insertion (sym_mpoly A) p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 = insertion (sym_mpoly A) p
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite A
insertion (sym_mpoly A) p = 0
vars (MPoly_Type.coeff p ?m) \<inter> A = {}
vars p \<subseteq> {1..n}

goal (1 subgoal):
 1. 0 = insertion (sym_mpoly A) p
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 = insertion (sym_mpoly A) p

goal (1 subgoal):
 1. p \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
0 = insertion (sym_mpoly A) p

goal (1 subgoal):
 1. p \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
have "insertion (sym_mpoly A) p = (\<Sum>m\<in>M. h m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion (sym_mpoly A) p = sum h M
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
insertion (sym_mpoly A) p = sum h M

goal (1 subgoal):
 1. p \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
insertion (sym_mpoly A) p = sum h M

goal (1 subgoal):
 1. p \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
have "\<dots> = (\<Sum>m\<in>{0}. h m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum h M = sum h {0}
[PROOF STEP]
using only_zero
[PROOF STATE]
proof (prove)
using this:
?m \<in> M \<Longrightarrow> ?m = 0

goal (1 subgoal):
 1. sum h M = sum h {0}
[PROOF STEP]
by (intro sum.mono_neutral_left) (auto simp: h_def M_def)
[PROOF STATE]
proof (state)
this:
sum h M = sum h {0}

goal (1 subgoal):
 1. p \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum h M = sum h {0}

goal (1 subgoal):
 1. p \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
have "\<dots> = coeff p 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum h {0} = MPoly_Type.coeff p 0
[PROOF STEP]
by (simp add: h_def)
[PROOF STATE]
proof (state)
this:
sum h {0} = MPoly_Type.coeff p 0

goal (1 subgoal):
 1. p \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
0 = MPoly_Type.coeff p 0
[PROOF STEP]
have "0 \<notin> M"
[PROOF STATE]
proof (prove)
using this:
0 = MPoly_Type.coeff p 0

goal (1 subgoal):
 1. 0 \<notin> M
[PROOF STEP]
by (auto simp: M_def)
[PROOF STATE]
proof (state)
this:
0 \<notin> M

goal (1 subgoal):
 1. p \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
with only_zero
[PROOF STATE]
proof (chain)
picking this:
?m \<in> M \<Longrightarrow> ?m = 0
0 \<notin> M
[PROOF STEP]
have "M = {}"
[PROOF STATE]
proof (prove)
using this:
?m \<in> M \<Longrightarrow> ?m = 0
0 \<notin> M

goal (1 subgoal):
 1. M = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
M = {}

goal (1 subgoal):
 1. p \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
hence "p = 0"
[PROOF STATE]
proof (prove)
using this:
M = {}

goal (1 subgoal):
 1. p = 0
[PROOF STEP]
by (intro mpoly_eqI) (auto simp: M_def)
[PROOF STATE]
proof (state)
this:
p = 0

goal (1 subgoal):
 1. p \<noteq> 0 \<Longrightarrow> False
[PROOF STEP]
with \<open>p \<noteq> 0\<close>
[PROOF STATE]
proof (chain)
picking this:
p \<noteq> 0
p = 0
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
p \<noteq> 0
p = 0

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem sym_mpoly_representation_unique:
  fixes p :: "'a mpoly mpoly"
  assumes "finite A"
          "insertion (sym_mpoly A) p = insertion (sym_mpoly A) q"
          "\<And>m. vars (coeff p m) \<inter> A = {}" "\<And>m. vars (coeff q m) \<inter> A = {}"
          "vars p \<subseteq> {1..n}" "vars q \<subseteq> {1..n}"
  shows   "p = q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p = q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p = q
[PROOF STEP]
have "p - q = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p - q = 0
[PROOF STEP]
proof (rule sym_mpoly_representation_unique_aux)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. finite A
 2. insertion (sym_mpoly A) (p - q) = 0
 3. \<And>m. vars (MPoly_Type.coeff (p - q) m) \<inter> A = {}
 4. vars (p - q) \<subseteq> {1..n}
[PROOF STEP]
fix m
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. finite A
 2. insertion (sym_mpoly A) (p - q) = 0
 3. \<And>m. vars (MPoly_Type.coeff (p - q) m) \<inter> A = {}
 4. vars (p - q) \<subseteq> {1..n}
[PROOF STEP]
show "vars (coeff (p - q) m) \<inter> A = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars (MPoly_Type.coeff (p - q) m) \<inter> A = {}
[PROOF STEP]
using vars_diff[of "coeff p m" "coeff q m"] assms(3,4)[of m]
[PROOF STATE]
proof (prove)
using this:
vars (MPoly_Type.coeff p m - MPoly_Type.coeff q m) \<subseteq> vars (MPoly_Type.coeff p m) \<union> vars (MPoly_Type.coeff q m)
vars (MPoly_Type.coeff p m) \<inter> A = {}
vars (MPoly_Type.coeff q m) \<inter> A = {}

goal (1 subgoal):
 1. vars (MPoly_Type.coeff (p - q) m) \<inter> A = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vars (MPoly_Type.coeff (p - q) m) \<inter> A = {}

goal (3 subgoals):
 1. finite A
 2. insertion (sym_mpoly A) (p - q) = 0
 3. vars (p - q) \<subseteq> {1..n}
[PROOF STEP]
qed (insert assms vars_diff[of p q], auto simp: insertion_diff)
[PROOF STATE]
proof (state)
this:
p - q = 0

goal (1 subgoal):
 1. p = q
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
p - q = 0

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem eq_fund_sym_poly_witI:
  fixes p :: "'a mpoly" and q :: "'a mpoly mpoly"
  assumes "finite A" "symmetric_mpoly A p"
          "insertion (sym_mpoly A) q = p"
          "\<And>m. vars (coeff q m) \<inter> A = {}"
          "vars q \<subseteq> {1..n}"
  shows   "q = fund_sym_poly_wit p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q = local.fund_sym_poly_wit p
[PROOF STEP]
using fund_sym_poly_wit_insertion[of p] fund_sym_poly_wit_vars[of p]
        fund_sym_poly_wit_coeffs[of p]
[PROOF STATE]
proof (prove)
using this:
symmetric_mpoly A p \<Longrightarrow> insertion (sym_mpoly A) (local.fund_sym_poly_wit p) = p
vars (local.fund_sym_poly_wit p) \<subseteq> {1..n}
symmetric_mpoly A p \<Longrightarrow> vars (MPoly_Type.coeff (local.fund_sym_poly_wit p) ?m) \<subseteq> vars p - A

goal (1 subgoal):
 1. q = local.fund_sym_poly_wit p
[PROOF STEP]
by (intro sym_mpoly_representation_unique)
     (insert assms, auto simp: fund_sym_poly_wit_insertion)


[STATEMENT]
lemma check_symmetric_mpoly_dom_aux:
  assumes "finite B" "vars p \<subseteq> B" "A \<subseteq> B"
  shows   "check_symmetric_mpoly_dom p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.check_symmetric_mpoly_dom p
[PROOF STEP]
using assms(1-3)
[PROOF STATE]
proof (prove)
using this:
finite B
vars p \<subseteq> B
A \<subseteq> B

goal (1 subgoal):
 1. local.check_symmetric_mpoly_dom p
[PROOF STEP]
proof (induction p rule: lead_monom_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>vars p \<subseteq> B; \<And>p'. \<lbrakk>vars p' \<subseteq> B; lead_monom p' < lead_monom p; A \<subseteq> B\<rbrakk> \<Longrightarrow> local.check_symmetric_mpoly_dom p'; A \<subseteq> B\<rbrakk> \<Longrightarrow> local.check_symmetric_mpoly_dom p
[PROOF STEP]
case (less p)
[PROOF STATE]
proof (state)
this:
vars p \<subseteq> B
\<lbrakk>vars ?p' \<subseteq> B; lead_monom ?p' < lead_monom p; A \<subseteq> B\<rbrakk> \<Longrightarrow> local.check_symmetric_mpoly_dom ?p'
A \<subseteq> B

goal (1 subgoal):
 1. \<And>p. \<lbrakk>vars p \<subseteq> B; \<And>p'. \<lbrakk>vars p' \<subseteq> B; lead_monom p' < lead_monom p; A \<subseteq> B\<rbrakk> \<Longrightarrow> local.check_symmetric_mpoly_dom p'; A \<subseteq> B\<rbrakk> \<Longrightarrow> local.check_symmetric_mpoly_dom p
[PROOF STEP]
have [simp]: "finite A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite A
[PROOF STEP]
by (rule finite_subset[of _ B]) fact+
[PROOF STATE]
proof (state)
this:
finite A

goal (1 subgoal):
 1. \<And>p. \<lbrakk>vars p \<subseteq> B; \<And>p'. \<lbrakk>vars p' \<subseteq> B; lead_monom p' < lead_monom p; A \<subseteq> B\<rbrakk> \<Longrightarrow> local.check_symmetric_mpoly_dom p'; A \<subseteq> B\<rbrakk> \<Longrightarrow> local.check_symmetric_mpoly_dom p
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.check_symmetric_mpoly_dom p
[PROOF STEP]
proof (cases "lead_monom p = 0 \<or> \<not>decr p")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. lead_monom p = 0 \<or> \<not> decr p \<Longrightarrow> local.check_symmetric_mpoly_dom p
 2. \<not> (lead_monom p = 0 \<or> \<not> decr p) \<Longrightarrow> local.check_symmetric_mpoly_dom p
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (lead_monom p = 0 \<or> \<not> decr p)

goal (2 subgoals):
 1. lead_monom p = 0 \<or> \<not> decr p \<Longrightarrow> local.check_symmetric_mpoly_dom p
 2. \<not> (lead_monom p = 0 \<or> \<not> decr p) \<Longrightarrow> local.check_symmetric_mpoly_dom p
[PROOF STEP]
hence [simp]: "p \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
\<not> (lead_monom p = 0 \<or> \<not> decr p)

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

goal (2 subgoals):
 1. lead_monom p = 0 \<or> \<not> decr p \<Longrightarrow> local.check_symmetric_mpoly_dom p
 2. \<not> (lead_monom p = 0 \<or> \<not> decr p) \<Longrightarrow> local.check_symmetric_mpoly_dom p
[PROOF STEP]
have "vars (p - fund_sym_step_poly p) \<subseteq> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars (p - local.fund_sym_step_poly p) \<subseteq> B
[PROOF STEP]
using fund_sym_step_poly[of p] False less.prems less.hyps \<open>A \<subseteq> B\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> lead_monom (local.fund_sym_step_poly p) = lead_monom p
\<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> Symmetric_Polynomials.lead_coeff (local.fund_sym_step_poly p) = Symmetric_Polynomials.lead_coeff p
\<lbrakk>finite A; p \<noteq> 0; decr p\<rbrakk> \<Longrightarrow> local.fund_sym_step_poly p = local.fund_sym_step_coeff p * (\<Prod>x. sym_mpoly A x ^ lookup (local.fund_sym_step_monom p) x)
vars (local.fund_sym_step_poly p) \<subseteq> vars p \<union> A
symmetric_mpoly A (local.fund_sym_step_poly p)
\<not> (lead_monom p = 0 \<or> \<not> decr p)
A \<subseteq> B
vars p \<subseteq> B
A \<subseteq> B

goal (1 subgoal):
 1. vars (p - local.fund_sym_step_poly p) \<subseteq> B
[PROOF STEP]
by (intro order.trans[OF vars_diff]) auto
[PROOF STATE]
proof (state)
this:
vars (p - local.fund_sym_step_poly p) \<subseteq> B

goal (2 subgoals):
 1. lead_monom p = 0 \<or> \<not> decr p \<Longrightarrow> local.check_symmetric_mpoly_dom p
 2. \<not> (lead_monom p = 0 \<or> \<not> decr p) \<Longrightarrow> local.check_symmetric_mpoly_dom p
[PROOF STEP]
hence "check_symmetric_mpoly_dom (p - local.fund_sym_step_poly p)"
[PROOF STATE]
proof (prove)
using this:
vars (p - local.fund_sym_step_poly p) \<subseteq> B

goal (1 subgoal):
 1. local.check_symmetric_mpoly_dom (p - local.fund_sym_step_poly p)
[PROOF STEP]
using False less.prems less.hyps
[PROOF STATE]
proof (prove)
using this:
vars (p - local.fund_sym_step_poly p) \<subseteq> B
\<not> (lead_monom p = 0 \<or> \<not> decr p)
A \<subseteq> B
vars p \<subseteq> B

goal (1 subgoal):
 1. local.check_symmetric_mpoly_dom (p - local.fund_sym_step_poly p)
[PROOF STEP]
by (intro less.IH fund_sym_step_poly symmetric_mpoly_diff
                lead_monom_fund_sym_step_poly_less) (auto simp: decr_def)
[PROOF STATE]
proof (state)
this:
local.check_symmetric_mpoly_dom (p - local.fund_sym_step_poly p)

goal (2 subgoals):
 1. lead_monom p = 0 \<or> \<not> decr p \<Longrightarrow> local.check_symmetric_mpoly_dom p
 2. \<not> (lead_monom p = 0 \<or> \<not> decr p) \<Longrightarrow> local.check_symmetric_mpoly_dom p
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
local.check_symmetric_mpoly_dom (p - local.fund_sym_step_poly p)

goal (1 subgoal):
 1. local.check_symmetric_mpoly_dom p
[PROOF STEP]
using check_symmetric_mpoly.domintros
[PROOF STATE]
proof (prove)
using this:
local.check_symmetric_mpoly_dom (p - local.fund_sym_step_poly p)
(\<And>x. \<lbrakk>A \<subseteq> vars ?p; decr ?p; \<not> local.check_symmetric_mpoly_dom (?p - local.fund_sym_step_poly ?p); x \<in> vars ?p; x \<in> A\<rbrakk> \<Longrightarrow> False) \<Longrightarrow> local.check_symmetric_mpoly_dom ?p

goal (1 subgoal):
 1. local.check_symmetric_mpoly_dom p
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
local.check_symmetric_mpoly_dom p

goal (1 subgoal):
 1. lead_monom p = 0 \<or> \<not> decr p \<Longrightarrow> local.check_symmetric_mpoly_dom p
[PROOF STEP]
qed (auto intro: check_symmetric_mpoly.domintros simp: lead_monom_eq_0_iff)
[PROOF STATE]
proof (state)
this:
local.check_symmetric_mpoly_dom p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma check_symmetric_mpoly_dom [intro]: "check_symmetric_mpoly_dom p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.check_symmetric_mpoly_dom p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local.check_symmetric_mpoly_dom p
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.check_symmetric_mpoly_dom p
[PROOF STEP]
proof (cases "A \<subseteq> vars p")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. A \<subseteq> vars p \<Longrightarrow> local.check_symmetric_mpoly_dom p
 2. \<not> A \<subseteq> vars p \<Longrightarrow> local.check_symmetric_mpoly_dom p
[PROOF STEP]
assume "A \<subseteq> vars p"
[PROOF STATE]
proof (state)
this:
A \<subseteq> vars p

goal (2 subgoals):
 1. A \<subseteq> vars p \<Longrightarrow> local.check_symmetric_mpoly_dom p
 2. \<not> A \<subseteq> vars p \<Longrightarrow> local.check_symmetric_mpoly_dom p
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
A \<subseteq> vars p

goal (1 subgoal):
 1. local.check_symmetric_mpoly_dom p
[PROOF STEP]
using check_symmetric_mpoly_dom_aux[of "vars p" p]
[PROOF STATE]
proof (prove)
using this:
A \<subseteq> vars p
\<lbrakk>finite (vars p); vars p \<subseteq> vars p; A \<subseteq> vars p\<rbrakk> \<Longrightarrow> local.check_symmetric_mpoly_dom p

goal (1 subgoal):
 1. local.check_symmetric_mpoly_dom p
[PROOF STEP]
by (auto simp: vars_finite)
[PROOF STATE]
proof (state)
this:
local.check_symmetric_mpoly_dom p

goal (1 subgoal):
 1. \<not> A \<subseteq> vars p \<Longrightarrow> local.check_symmetric_mpoly_dom p
[PROOF STEP]
qed (auto intro: check_symmetric_mpoly.domintros)
[PROOF STATE]
proof (state)
this:
local.check_symmetric_mpoly_dom p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma check_symmetric_mpoly_correct: "check_symmetric_mpoly p \<longleftrightarrow> symmetric_mpoly A p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.check_symmetric_mpoly p = symmetric_mpoly A p
[PROOF STEP]
proof (induction p rule: check_symmetric_mpoly.induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p. (\<lbrakk>vars p \<inter> A \<noteq> {}; A \<subseteq> vars p; decr p\<rbrakk> \<Longrightarrow> local.check_symmetric_mpoly (p - local.fund_sym_step_poly p) = symmetric_mpoly A (p - local.fund_sym_step_poly p)) \<Longrightarrow> local.check_symmetric_mpoly p = symmetric_mpoly A p
[PROOF STEP]
case (1 p)
[PROOF STATE]
proof (state)
this:
\<lbrakk>vars p \<inter> A \<noteq> {}; A \<subseteq> vars p; decr p\<rbrakk> \<Longrightarrow> local.check_symmetric_mpoly (p - local.fund_sym_step_poly p) = symmetric_mpoly A (p - local.fund_sym_step_poly p)

goal (1 subgoal):
 1. \<And>p. (\<lbrakk>vars p \<inter> A \<noteq> {}; A \<subseteq> vars p; decr p\<rbrakk> \<Longrightarrow> local.check_symmetric_mpoly (p - local.fund_sym_step_poly p) = symmetric_mpoly A (p - local.fund_sym_step_poly p)) \<Longrightarrow> local.check_symmetric_mpoly p = symmetric_mpoly A p
[PROOF STEP]
have "symmetric_mpoly A (p - fund_sym_step_poly p) \<longleftrightarrow> symmetric_mpoly A p" (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. symmetric_mpoly A (p - local.fund_sym_step_poly p) = symmetric_mpoly A p
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. symmetric_mpoly A (p - local.fund_sym_step_poly p) \<Longrightarrow> symmetric_mpoly A p
 2. symmetric_mpoly A p \<Longrightarrow> symmetric_mpoly A (p - local.fund_sym_step_poly p)
[PROOF STEP]
assume ?rhs
[PROOF STATE]
proof (state)
this:
symmetric_mpoly A p

goal (2 subgoals):
 1. symmetric_mpoly A (p - local.fund_sym_step_poly p) \<Longrightarrow> symmetric_mpoly A p
 2. symmetric_mpoly A p \<Longrightarrow> symmetric_mpoly A (p - local.fund_sym_step_poly p)
[PROOF STEP]
thus ?lhs
[PROOF STATE]
proof (prove)
using this:
symmetric_mpoly A p

goal (1 subgoal):
 1. symmetric_mpoly A (p - local.fund_sym_step_poly p)
[PROOF STEP]
by (intro symmetric_mpoly_diff fund_sym_step_poly)
[PROOF STATE]
proof (state)
this:
symmetric_mpoly A (p - local.fund_sym_step_poly p)

goal (1 subgoal):
 1. symmetric_mpoly A (p - local.fund_sym_step_poly p) \<Longrightarrow> symmetric_mpoly A p
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. symmetric_mpoly A (p - local.fund_sym_step_poly p) \<Longrightarrow> symmetric_mpoly A p
[PROOF STEP]
assume ?lhs
[PROOF STATE]
proof (state)
this:
symmetric_mpoly A (p - local.fund_sym_step_poly p)

goal (1 subgoal):
 1. symmetric_mpoly A (p - local.fund_sym_step_poly p) \<Longrightarrow> symmetric_mpoly A p
[PROOF STEP]
hence "symmetric_mpoly A (p - fund_sym_step_poly p + fund_sym_step_poly p)"
[PROOF STATE]
proof (prove)
using this:
symmetric_mpoly A (p - local.fund_sym_step_poly p)

goal (1 subgoal):
 1. symmetric_mpoly A (p - local.fund_sym_step_poly p + local.fund_sym_step_poly p)
[PROOF STEP]
by (intro symmetric_mpoly_add fund_sym_step_poly)
[PROOF STATE]
proof (state)
this:
symmetric_mpoly A (p - local.fund_sym_step_poly p + local.fund_sym_step_poly p)

goal (1 subgoal):
 1. symmetric_mpoly A (p - local.fund_sym_step_poly p) \<Longrightarrow> symmetric_mpoly A p
[PROOF STEP]
thus ?rhs
[PROOF STATE]
proof (prove)
using this:
symmetric_mpoly A (p - local.fund_sym_step_poly p + local.fund_sym_step_poly p)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
symmetric_mpoly A (p - local.fund_sym_step_poly p) = symmetric_mpoly A p

goal (1 subgoal):
 1. \<And>p. (\<lbrakk>vars p \<inter> A \<noteq> {}; A \<subseteq> vars p; decr p\<rbrakk> \<Longrightarrow> local.check_symmetric_mpoly (p - local.fund_sym_step_poly p) = symmetric_mpoly A (p - local.fund_sym_step_poly p)) \<Longrightarrow> local.check_symmetric_mpoly p = symmetric_mpoly A p
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
symmetric_mpoly A (p - local.fund_sym_step_poly p) = symmetric_mpoly A p

goal (1 subgoal):
 1. \<And>p. (\<lbrakk>vars p \<inter> A \<noteq> {}; A \<subseteq> vars p; decr p\<rbrakk> \<Longrightarrow> local.check_symmetric_mpoly (p - local.fund_sym_step_poly p) = symmetric_mpoly A (p - local.fund_sym_step_poly p)) \<Longrightarrow> local.check_symmetric_mpoly p = symmetric_mpoly A p
[PROOF STEP]
have "decr p" if "symmetric_mpoly A p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. decr p
[PROOF STEP]
using lookup_lead_monom_decreasing[of A p] that
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>symmetric_mpoly A p; ?i \<in> A; ?j \<in> A; ?i \<le> ?j\<rbrakk> \<Longrightarrow> lookup (lead_monom p) ?j \<le> lookup (lead_monom p) ?i
symmetric_mpoly A p

goal (1 subgoal):
 1. decr p
[PROOF STEP]
by (auto simp: decr_def)
[PROOF STATE]
proof (state)
this:
symmetric_mpoly A p \<Longrightarrow> decr p

goal (1 subgoal):
 1. \<And>p. (\<lbrakk>vars p \<inter> A \<noteq> {}; A \<subseteq> vars p; decr p\<rbrakk> \<Longrightarrow> local.check_symmetric_mpoly (p - local.fund_sym_step_poly p) = symmetric_mpoly A (p - local.fund_sym_step_poly p)) \<Longrightarrow> local.check_symmetric_mpoly p = symmetric_mpoly A p
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
symmetric_mpoly A (p - local.fund_sym_step_poly p) = symmetric_mpoly A p
symmetric_mpoly A p \<Longrightarrow> decr p
[PROOF STEP]
show "check_symmetric_mpoly p \<longleftrightarrow> symmetric_mpoly A p"
[PROOF STATE]
proof (prove)
using this:
symmetric_mpoly A (p - local.fund_sym_step_poly p) = symmetric_mpoly A p
symmetric_mpoly A p \<Longrightarrow> decr p

goal (1 subgoal):
 1. local.check_symmetric_mpoly p = symmetric_mpoly A p
[PROOF STEP]
using 1 symmetric_mpoly_imp_orthogonal_or_subset[of A p]
[PROOF STATE]
proof (prove)
using this:
symmetric_mpoly A (p - local.fund_sym_step_poly p) = symmetric_mpoly A p
symmetric_mpoly A p \<Longrightarrow> decr p
\<lbrakk>vars p \<inter> A \<noteq> {}; A \<subseteq> vars p; decr p\<rbrakk> \<Longrightarrow> local.check_symmetric_mpoly (p - local.fund_sym_step_poly p) = symmetric_mpoly A (p - local.fund_sym_step_poly p)
symmetric_mpoly A p \<Longrightarrow> vars p \<inter> A = {} \<or> A \<subseteq> vars p

goal (1 subgoal):
 1. local.check_symmetric_mpoly p = symmetric_mpoly A p
[PROOF STEP]
by (auto simp: Let_def check_symmetric_mpoly.simps[of p] intro: symmetric_mpoly_orthogonal)
[PROOF STATE]
proof (state)
this:
local.check_symmetric_mpoly p = symmetric_mpoly A p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem symmetric_poly_of_roots_conv_poly_of_coeffs:
  assumes c: "cinv * l c = 1" "cinv \<in> C"
  assumes "p = Polynomial.smult c (\<Prod>i\<in>A. [:-root i, 1:])"
  obtains q' where "vars q' \<subseteq> {0..<n}"
               and "\<And>m. coeff q' m \<in> C"
               and "insertion (l \<circ> poly.coeff p) q' = insertion (l \<circ> root) q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>q'. \<lbrakk>vars q' \<subseteq> {0..<n}; \<And>m. MPoly_Type.coeff q' m \<in> C; insertion (l \<circ> poly.coeff p) q' = insertion (l \<circ> root) q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>q'. \<lbrakk>vars q' \<subseteq> {0..<n}; \<And>m. MPoly_Type.coeff q' m \<in> C; insertion (l \<circ> poly.coeff p) q' = insertion (l \<circ> root) q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define q' where "q' = fund_sym_poly_wit A q"
[PROOF STATE]
proof (state)
this:
q' = fund_sym_poly_wit A q

goal (1 subgoal):
 1. (\<And>q'. \<lbrakk>vars q' \<subseteq> {0..<n}; \<And>m. MPoly_Type.coeff q' m \<in> C; insertion (l \<circ> poly.coeff p) q' = insertion (l \<circ> root) q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define q'' where "q'' =
     mapm_mpoly (\<lambda>m x. (\<Prod>i. (cinv * l (- 1) ^ i) ^ lookup m i) * insertion (\<lambda>_. 0) x) q'"
[PROOF STATE]
proof (state)
this:
q'' = mapm_mpoly (\<lambda>m x. (\<Prod>i. (cinv * l (- (1::'a)) ^ i) ^ lookup m i) * insertion (\<lambda>_. 0::'b) x) q'

goal (1 subgoal):
 1. (\<And>q'. \<lbrakk>vars q' \<subseteq> {0..<n}; \<And>m. MPoly_Type.coeff q' m \<in> C; insertion (l \<circ> poly.coeff p) q' = insertion (l \<circ> root) q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define reindex where "reindex = (\<lambda>i. if i \<le> n then n - i else i)"
[PROOF STATE]
proof (state)
this:
reindex = (\<lambda>i. if i \<le> n then n - i else i)

goal (1 subgoal):
 1. (\<And>q'. \<lbrakk>vars q' \<subseteq> {0..<n}; \<And>m. MPoly_Type.coeff q' m \<in> C; insertion (l \<circ> poly.coeff p) q' = insertion (l \<circ> root) q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "bij reindex"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij reindex
[PROOF STEP]
by (intro bij_betwI[of reindex _ _ reindex]) (auto simp: reindex_def)
[PROOF STATE]
proof (state)
this:
bij reindex

goal (1 subgoal):
 1. (\<And>q'. \<lbrakk>vars q' \<subseteq> {0..<n}; \<And>m. MPoly_Type.coeff q' m \<in> C; insertion (l \<circ> poly.coeff p) q' = insertion (l \<circ> root) q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "vars q' \<subseteq> {1..n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars q' \<subseteq> {1..n}
[PROOF STEP]
unfolding q'_def n_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars (fund_sym_poly_wit A q) \<subseteq> {1..card A}
[PROOF STEP]
by (intro fund_sym_poly_wit_vars)
[PROOF STATE]
proof (state)
this:
vars q' \<subseteq> {1..n}

goal (1 subgoal):
 1. (\<And>q'. \<lbrakk>vars q' \<subseteq> {0..<n}; \<And>m. MPoly_Type.coeff q' m \<in> C; insertion (l \<circ> poly.coeff p) q' = insertion (l \<circ> root) q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
hence "vars q'' \<subseteq> {1..n}"
[PROOF STATE]
proof (prove)
using this:
vars q' \<subseteq> {1..n}

goal (1 subgoal):
 1. vars q'' \<subseteq> {1..n}
[PROOF STEP]
unfolding q''_def
[PROOF STATE]
proof (prove)
using this:
vars q' \<subseteq> {1..n}

goal (1 subgoal):
 1. vars (mapm_mpoly (\<lambda>m x. (\<Prod>i. (cinv * l (- (1::'a)) ^ i) ^ lookup m i) * insertion (\<lambda>_. 0::'b) x) q') \<subseteq> {1..n}
[PROOF STEP]
using vars_mapm_mpoly_subset
[PROOF STATE]
proof (prove)
using this:
vars q' \<subseteq> {1..n}
vars (mapm_mpoly ?f ?p) \<subseteq> vars ?p

goal (1 subgoal):
 1. vars (mapm_mpoly (\<lambda>m x. (\<Prod>i. (cinv * l (- (1::'a)) ^ i) ^ lookup m i) * insertion (\<lambda>_. 0::'b) x) q') \<subseteq> {1..n}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vars q'' \<subseteq> {1..n}

goal (1 subgoal):
 1. (\<And>q'. \<lbrakk>vars q' \<subseteq> {0..<n}; \<And>m. MPoly_Type.coeff q' m \<in> C; insertion (l \<circ> poly.coeff p) q' = insertion (l \<circ> root) q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "insertion (l \<circ> root) (insertion (sym_mpoly A) q') =
          insertion (\<lambda>n. insertion (l \<circ> root) (sym_mpoly A n))
            (map_mpoly (insertion (l \<circ> root)) q')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion (l \<circ> root) (insertion (sym_mpoly A) q') = insertion (\<lambda>n. insertion (l \<circ> root) (sym_mpoly A n)) (map_mpoly (insertion (l \<circ> root)) q')
[PROOF STEP]
by (rule insertion_insertion)
[PROOF STATE]
proof (state)
this:
insertion (l \<circ> root) (insertion (sym_mpoly A) q') = insertion (\<lambda>n. insertion (l \<circ> root) (sym_mpoly A n)) (map_mpoly (insertion (l \<circ> root)) q')

goal (1 subgoal):
 1. (\<And>q'. \<lbrakk>vars q' \<subseteq> {0..<n}; \<And>m. MPoly_Type.coeff q' m \<in> C; insertion (l \<circ> poly.coeff p) q' = insertion (l \<circ> root) q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
insertion (l \<circ> root) (insertion (sym_mpoly A) q') = insertion (\<lambda>n. insertion (l \<circ> root) (sym_mpoly A n)) (map_mpoly (insertion (l \<circ> root)) q')

goal (1 subgoal):
 1. (\<And>q'. \<lbrakk>vars q' \<subseteq> {0..<n}; \<And>m. MPoly_Type.coeff q' m \<in> C; insertion (l \<circ> poly.coeff p) q' = insertion (l \<circ> root) q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "insertion (sym_mpoly A) q' = q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion (sym_mpoly A) q' = q
[PROOF STEP]
unfolding q'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion (sym_mpoly A) (fund_sym_poly_wit A q) = q
[PROOF STEP]
by (intro fund_sym_poly_wit_insertion sym)
[PROOF STATE]
proof (state)
this:
insertion (sym_mpoly A) q' = q

goal (1 subgoal):
 1. (\<And>q'. \<lbrakk>vars q' \<subseteq> {0..<n}; \<And>m. MPoly_Type.coeff q' m \<in> C; insertion (l \<circ> poly.coeff p) q' = insertion (l \<circ> root) q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
insertion (sym_mpoly A) q' = q

goal (1 subgoal):
 1. (\<And>q'. \<lbrakk>vars q' \<subseteq> {0..<n}; \<And>m. MPoly_Type.coeff q' m \<in> C; insertion (l \<circ> poly.coeff p) q' = insertion (l \<circ> root) q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "insertion (\<lambda>i. insertion (l \<circ> root) (sym_mpoly A i))
               (map_mpoly (insertion (l \<circ> root)) q') =
             insertion (\<lambda>i. cinv * l ((- 1) ^ i) * l (poly.coeff p (n - i)))
               (map_mpoly (insertion (l \<circ> root)) q')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion (\<lambda>i. insertion (l \<circ> root) (sym_mpoly A i)) (map_mpoly (insertion (l \<circ> root)) q') = insertion (\<lambda>i. cinv * l ((- (1::'a)) ^ i) * l (poly.coeff p (n - i))) (map_mpoly (insertion (l \<circ> root)) q')
[PROOF STEP]
proof (intro insertion_irrelevant_vars, goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>v. v \<in> vars (map_mpoly (insertion (l \<circ> root)) q') \<Longrightarrow> insertion (l \<circ> root) (sym_mpoly A v) = cinv * l ((- (1::'a)) ^ v) * l (poly.coeff p (n - v))
[PROOF STEP]
case (1 i)
[PROOF STATE]
proof (state)
this:
i \<in> vars (map_mpoly (insertion (l \<circ> root)) q')

goal (1 subgoal):
 1. \<And>v. v \<in> vars (map_mpoly (insertion (l \<circ> root)) q') \<Longrightarrow> insertion (l \<circ> root) (sym_mpoly A v) = cinv * l ((- (1::'a)) ^ v) * l (poly.coeff p (n - v))
[PROOF STEP]
hence "i \<in> vars q'"
[PROOF STATE]
proof (prove)
using this:
i \<in> vars (map_mpoly (insertion (l \<circ> root)) q')

goal (1 subgoal):
 1. i \<in> vars q'
[PROOF STEP]
using vars_map_mpoly_subset
[PROOF STATE]
proof (prove)
using this:
i \<in> vars (map_mpoly (insertion (l \<circ> root)) q')
vars (map_mpoly ?f ?p) \<subseteq> vars ?p

goal (1 subgoal):
 1. i \<in> vars q'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i \<in> vars q'

goal (1 subgoal):
 1. \<And>v. v \<in> vars (map_mpoly (insertion (l \<circ> root)) q') \<Longrightarrow> insertion (l \<circ> root) (sym_mpoly A v) = cinv * l ((- (1::'a)) ^ v) * l (poly.coeff p (n - v))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
i \<in> vars q'

goal (1 subgoal):
 1. \<And>v. v \<in> vars (map_mpoly (insertion (l \<circ> root)) q') \<Longrightarrow> insertion (l \<circ> root) (sym_mpoly A v) = cinv * l ((- (1::'a)) ^ v) * l (poly.coeff p (n - v))
[PROOF STEP]
have "\<dots> \<subseteq> {1..n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars q' \<subseteq> {1..n}
[PROOF STEP]
unfolding q'_def n_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars (fund_sym_poly_wit A q) \<subseteq> {1..card A}
[PROOF STEP]
by (intro fund_sym_poly_wit_vars)
[PROOF STATE]
proof (state)
this:
vars q' \<subseteq> {1..n}

goal (1 subgoal):
 1. \<And>v. v \<in> vars (map_mpoly (insertion (l \<circ> root)) q') \<Longrightarrow> insertion (l \<circ> root) (sym_mpoly A v) = cinv * l ((- (1::'a)) ^ v) * l (poly.coeff p (n - v))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
i \<in> {1..n}
[PROOF STEP]
have i: "i \<in> {1..n}"
[PROOF STATE]
proof (prove)
using this:
i \<in> {1..n}

goal (1 subgoal):
 1. i \<in> {1..n}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
i \<in> {1..n}

goal (1 subgoal):
 1. \<And>v. v \<in> vars (map_mpoly (insertion (l \<circ> root)) q') \<Longrightarrow> insertion (l \<circ> root) (sym_mpoly A v) = cinv * l ((- (1::'a)) ^ v) * l (poly.coeff p (n - v))
[PROOF STEP]
have "insertion (l \<circ> root) (sym_mpoly A i) =
             l (\<Sum>Y | Y \<subseteq> A \<and> card Y = i. prod root Y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion (l \<circ> root) (sym_mpoly A i) = l (\<Sum>Y | Y \<subseteq> A \<and> card Y = i. prod root Y)
[PROOF STEP]
using \<open>finite A\<close>
[PROOF STATE]
proof (prove)
using this:
finite A

goal (1 subgoal):
 1. insertion (l \<circ> root) (sym_mpoly A i) = l (\<Sum>Y | Y \<subseteq> A \<and> card Y = i. prod root Y)
[PROOF STEP]
by (simp add: insertion_sym_mpoly)
[PROOF STATE]
proof (state)
this:
insertion (l \<circ> root) (sym_mpoly A i) = l (\<Sum>Y | Y \<subseteq> A \<and> card Y = i. prod root Y)

goal (1 subgoal):
 1. \<And>v. v \<in> vars (map_mpoly (insertion (l \<circ> root)) q') \<Longrightarrow> insertion (l \<circ> root) (sym_mpoly A v) = cinv * l ((- (1::'a)) ^ v) * l (poly.coeff p (n - v))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
insertion (l \<circ> root) (sym_mpoly A i) = l (\<Sum>Y | Y \<subseteq> A \<and> card Y = i. prod root Y)

goal (1 subgoal):
 1. \<And>v. v \<in> vars (map_mpoly (insertion (l \<circ> root)) q') \<Longrightarrow> insertion (l \<circ> root) (sym_mpoly A v) = cinv * l ((- (1::'a)) ^ v) * l (poly.coeff p (n - v))
[PROOF STEP]
have "\<dots> = cinv * l (c * (\<Sum>Y | Y \<subseteq> A \<and> card Y = i. prod root Y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l (\<Sum>Y | Y \<subseteq> A \<and> card Y = i. prod root Y) = cinv * l (c * (\<Sum>Y | Y \<subseteq> A \<and> card Y = i. prod root Y))
[PROOF STEP]
unfolding mult mult.assoc[symmetric] \<open>cinv * l c = 1\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l (\<Sum>Y | Y \<subseteq> A \<and> card Y = i. prod root Y) = (1::'b) * l (sum (prod root) {Y. Y \<subseteq> A \<and> card Y = i})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
l (\<Sum>Y | Y \<subseteq> A \<and> card Y = i. prod root Y) = cinv * l (c * (\<Sum>Y | Y \<subseteq> A \<and> card Y = i. prod root Y))

goal (1 subgoal):
 1. \<And>v. v \<in> vars (map_mpoly (insertion (l \<circ> root)) q') \<Longrightarrow> insertion (l \<circ> root) (sym_mpoly A v) = cinv * l ((- (1::'a)) ^ v) * l (poly.coeff p (n - v))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
l (\<Sum>Y | Y \<subseteq> A \<and> card Y = i. prod root Y) = cinv * l (c * (\<Sum>Y | Y \<subseteq> A \<and> card Y = i. prod root Y))

goal (1 subgoal):
 1. \<And>v. v \<in> vars (map_mpoly (insertion (l \<circ> root)) q') \<Longrightarrow> insertion (l \<circ> root) (sym_mpoly A v) = cinv * l ((- (1::'a)) ^ v) * l (poly.coeff p (n - v))
[PROOF STEP]
have "c * (\<Sum>Y | Y \<subseteq> A \<and> card Y = i. prod root Y) = ((-1) ^ i * poly.coeff p (n - i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c * (\<Sum>Y | Y \<subseteq> A \<and> card Y = i. prod root Y) = (- (1::'a)) ^ i * poly.coeff p (n - i)
[PROOF STEP]
using coeff_poly_from_roots[of A "n - i" root] i assms finite
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite A; n - i \<le> card A\<rbrakk> \<Longrightarrow> poly.coeff (\<Prod>x\<in>A. [:- root x, 1::'a:]) (n - i) = (- (1::'a)) ^ (card A - (n - i)) * (\<Sum>X | X \<subseteq> A \<and> card X = card A - (n - i). prod root X)
i \<in> {1..n}
cinv * l c = (1::'b)
cinv \<in> C
p = Polynomial.smult c (\<Prod>i\<in>A. [:- root i, 1::'a:])
finite A

goal (1 subgoal):
 1. c * (\<Sum>Y | Y \<subseteq> A \<and> card Y = i. prod root Y) = (- (1::'a)) ^ i * poly.coeff p (n - i)
[PROOF STEP]
by (auto simp: n_def minus_one_power_iff)
[PROOF STATE]
proof (state)
this:
c * (\<Sum>Y | Y \<subseteq> A \<and> card Y = i. prod root Y) = (- (1::'a)) ^ i * poly.coeff p (n - i)

goal (1 subgoal):
 1. \<And>v. v \<in> vars (map_mpoly (insertion (l \<circ> root)) q') \<Longrightarrow> insertion (l \<circ> root) (sym_mpoly A v) = cinv * l ((- (1::'a)) ^ v) * l (poly.coeff p (n - v))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
insertion (l \<circ> root) (sym_mpoly A i) = cinv * l ((- (1::'a)) ^ i * poly.coeff p (n - i))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
insertion (l \<circ> root) (sym_mpoly A i) = cinv * l ((- (1::'a)) ^ i * poly.coeff p (n - i))

goal (1 subgoal):
 1. insertion (l \<circ> root) (sym_mpoly A i) = cinv * l ((- (1::'a)) ^ i) * l (poly.coeff p (n - i))
[PROOF STEP]
by (simp add: o_def)
[PROOF STATE]
proof (state)
this:
insertion (l \<circ> root) (sym_mpoly A i) = cinv * l ((- (1::'a)) ^ i) * l (poly.coeff p (n - i))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
insertion (\<lambda>i. insertion (l \<circ> root) (sym_mpoly A i)) (map_mpoly (insertion (l \<circ> root)) q') = insertion (\<lambda>i. cinv * l ((- (1::'a)) ^ i) * l (poly.coeff p (n - i))) (map_mpoly (insertion (l \<circ> root)) q')

goal (1 subgoal):
 1. (\<And>q'. \<lbrakk>vars q' \<subseteq> {0..<n}; \<And>m. MPoly_Type.coeff q' m \<in> C; insertion (l \<circ> poly.coeff p) q' = insertion (l \<circ> root) q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
insertion (\<lambda>i. insertion (l \<circ> root) (sym_mpoly A i)) (map_mpoly (insertion (l \<circ> root)) q') = insertion (\<lambda>i. cinv * l ((- (1::'a)) ^ i) * l (poly.coeff p (n - i))) (map_mpoly (insertion (l \<circ> root)) q')

goal (1 subgoal):
 1. (\<And>q'. \<lbrakk>vars q' \<subseteq> {0..<n}; \<And>m. MPoly_Type.coeff q' m \<in> C; insertion (l \<circ> poly.coeff p) q' = insertion (l \<circ> root) q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "map_mpoly (insertion (l \<circ> root)) q' = map_mpoly (insertion (\<lambda>_. 0)) q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_mpoly (insertion (l \<circ> root)) q' = map_mpoly (insertion (\<lambda>_. 0::'b)) q'
[PROOF STEP]
using fund_sym_poly_wit_coeffs[OF sym] vars
[PROOF STATE]
proof (prove)
using this:
vars (MPoly_Type.coeff (fund_sym_poly_wit A q) ?m) \<subseteq> vars q - A
vars q \<subseteq> A

goal (1 subgoal):
 1. map_mpoly (insertion (l \<circ> root)) q' = map_mpoly (insertion (\<lambda>_. 0::'b)) q'
[PROOF STEP]
by (intro map_mpoly_cong insertion_irrelevant_vars) (auto simp: q'_def)
[PROOF STATE]
proof (state)
this:
map_mpoly (insertion (l \<circ> root)) q' = map_mpoly (insertion (\<lambda>_. 0::'b)) q'

goal (1 subgoal):
 1. (\<And>q'. \<lbrakk>vars q' \<subseteq> {0..<n}; \<And>m. MPoly_Type.coeff q' m \<in> C; insertion (l \<circ> poly.coeff p) q' = insertion (l \<circ> root) q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
map_mpoly (insertion (l \<circ> root)) q' = map_mpoly (insertion (\<lambda>_. 0::'b)) q'

goal (1 subgoal):
 1. (\<And>q'. \<lbrakk>vars q' \<subseteq> {0..<n}; \<And>m. MPoly_Type.coeff q' m \<in> C; insertion (l \<circ> poly.coeff p) q' = insertion (l \<circ> root) q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "insertion (\<lambda>i. cinv * l ((- 1) ^ i) * l (poly.coeff p (n - i))) \<dots> =
               insertion (\<lambda>i. l (poly.coeff p (n - i))) q''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion (\<lambda>i. cinv * l ((- (1::'a)) ^ i) * l (poly.coeff p (n - i))) (map_mpoly (insertion (\<lambda>_. 0::'b)) q') = insertion (\<lambda>i. l (poly.coeff p (n - i))) q''
[PROOF STEP]
unfolding insertion_substitute_linear map_mpoly_conv_mapm_mpoly q''_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion (\<lambda>i. l (poly.coeff p (n - i))) (mapm_mpoly (\<lambda>m. (*) (\<Prod>i. (cinv * l ((- (1::'a)) ^ i)) ^ lookup m i)) (mapm_mpoly (\<lambda>_. insertion (\<lambda>_. 0::'b)) q')) = insertion (\<lambda>i. l (poly.coeff p (n - i))) (mapm_mpoly (\<lambda>m x. (\<Prod>i. (cinv * l (- (1::'a)) ^ i) ^ lookup m i) * insertion (\<lambda>_. 0::'b) x) q')
[PROOF STEP]
by (subst mapm_mpoly_comp) auto
[PROOF STATE]
proof (state)
this:
insertion (\<lambda>i. cinv * l ((- (1::'a)) ^ i) * l (poly.coeff p (n - i))) (map_mpoly (insertion (\<lambda>_. 0::'b)) q') = insertion (\<lambda>i. l (poly.coeff p (n - i))) q''

goal (1 subgoal):
 1. (\<And>q'. \<lbrakk>vars q' \<subseteq> {0..<n}; \<And>m. MPoly_Type.coeff q' m \<in> C; insertion (l \<circ> poly.coeff p) q' = insertion (l \<circ> root) q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
insertion (\<lambda>i. cinv * l ((- (1::'a)) ^ i) * l (poly.coeff p (n - i))) (map_mpoly (insertion (\<lambda>_. 0::'b)) q') = insertion (\<lambda>i. l (poly.coeff p (n - i))) q''

goal (1 subgoal):
 1. (\<And>q'. \<lbrakk>vars q' \<subseteq> {0..<n}; \<And>m. MPoly_Type.coeff q' m \<in> C; insertion (l \<circ> poly.coeff p) q' = insertion (l \<circ> root) q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "\<dots> = insertion (l \<circ> poly.coeff p) (mpoly_map_vars reindex q'')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion (\<lambda>i. l (poly.coeff p (n - i))) q'' = insertion (l \<circ> poly.coeff p) (mpoly_map_vars reindex q'')
[PROOF STEP]
using \<open>bij reindex\<close> and \<open>vars q'' \<subseteq> {1..n}\<close>
[PROOF STATE]
proof (prove)
using this:
bij reindex
vars q'' \<subseteq> {1..n}

goal (1 subgoal):
 1. insertion (\<lambda>i. l (poly.coeff p (n - i))) q'' = insertion (l \<circ> poly.coeff p) (mpoly_map_vars reindex q'')
[PROOF STEP]
by (subst insertion_mpoly_map_vars)
       (auto simp: o_def reindex_def intro!: insertion_irrelevant_vars)
[PROOF STATE]
proof (state)
this:
insertion (\<lambda>i. l (poly.coeff p (n - i))) q'' = insertion (l \<circ> poly.coeff p) (mpoly_map_vars reindex q'')

goal (1 subgoal):
 1. (\<And>q'. \<lbrakk>vars q' \<subseteq> {0..<n}; \<And>m. MPoly_Type.coeff q' m \<in> C; insertion (l \<circ> poly.coeff p) q' = insertion (l \<circ> root) q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
insertion (l \<circ> root) q = insertion (l \<circ> poly.coeff p) (mpoly_map_vars reindex q'')
[PROOF STEP]
have "insertion (l \<circ> root) q =
                  insertion (l \<circ> poly.coeff p) (mpoly_map_vars reindex q'')"
[PROOF STATE]
proof (prove)
using this:
insertion (l \<circ> root) q = insertion (l \<circ> poly.coeff p) (mpoly_map_vars reindex q'')

goal (1 subgoal):
 1. insertion (l \<circ> root) q = insertion (l \<circ> poly.coeff p) (mpoly_map_vars reindex q'')
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
insertion (l \<circ> root) q = insertion (l \<circ> poly.coeff p) (mpoly_map_vars reindex q'')

goal (1 subgoal):
 1. (\<And>q'. \<lbrakk>vars q' \<subseteq> {0..<n}; \<And>m. MPoly_Type.coeff q' m \<in> C; insertion (l \<circ> poly.coeff p) q' = insertion (l \<circ> root) q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
insertion (l \<circ> root) q = insertion (l \<circ> poly.coeff p) (mpoly_map_vars reindex q'')

goal (1 subgoal):
 1. (\<And>q'. \<lbrakk>vars q' \<subseteq> {0..<n}; \<And>m. MPoly_Type.coeff q' m \<in> C; insertion (l \<circ> poly.coeff p) q' = insertion (l \<circ> root) q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "coeff (mpoly_map_vars reindex q'') m \<in> C" for m
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MPoly_Type.coeff (mpoly_map_vars reindex q'') m \<in> C
[PROOF STEP]
unfolding q''_def q'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MPoly_Type.coeff (mpoly_map_vars reindex (mapm_mpoly (\<lambda>m x. (\<Prod>i. (cinv * l (- (1::'a)) ^ i) ^ lookup m i) * insertion (\<lambda>_. 0::'b) x) (fund_sym_poly_wit A q))) m \<in> C
[PROOF STEP]
using \<open>bij reindex\<close> fund_sym_poly_wit_coeff[of q C A] C \<open>cinv \<in> C\<close>
[PROOF STATE]
proof (prove)
using this:
bij reindex
\<lbrakk>\<forall>m. MPoly_Type.coeff q m \<in> C; ring_closed C\<rbrakk> \<Longrightarrow> \<forall>m m'. MPoly_Type.coeff (MPoly_Type.coeff (fund_sym_poly_wit A q) m) m' \<in> C
ring_closed C
\<forall>m. MPoly_Type.coeff q m \<in> C
cinv \<in> C

goal (1 subgoal):
 1. MPoly_Type.coeff (mpoly_map_vars reindex (mapm_mpoly (\<lambda>m x. (\<Prod>i. (cinv * l (- (1::'a)) ^ i) ^ lookup m i) * insertion (\<lambda>_. 0::'b) x) (fund_sym_poly_wit A q))) m \<in> C
[PROOF STEP]
by (auto simp: coeff_mpoly_map_vars
             intro!: mult_closed Prod_any_closed power_closed Sum_any_closed)
[PROOF STATE]
proof (state)
this:
MPoly_Type.coeff (mpoly_map_vars reindex q'') ?m \<in> C

goal (1 subgoal):
 1. (\<And>q'. \<lbrakk>vars q' \<subseteq> {0..<n}; \<And>m. MPoly_Type.coeff q' m \<in> C; insertion (l \<circ> poly.coeff p) q' = insertion (l \<circ> root) q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
MPoly_Type.coeff (mpoly_map_vars reindex q'') ?m \<in> C

goal (1 subgoal):
 1. (\<And>q'. \<lbrakk>vars q' \<subseteq> {0..<n}; \<And>m. MPoly_Type.coeff q' m \<in> C; insertion (l \<circ> poly.coeff p) q' = insertion (l \<circ> root) q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "vars (mpoly_map_vars reindex q'') \<subseteq> {0..<n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars (mpoly_map_vars reindex q'') \<subseteq> {0..<n}
[PROOF STEP]
using \<open>bij reindex\<close> and \<open>vars q'' \<subseteq> {1..n}\<close>
[PROOF STATE]
proof (prove)
using this:
bij reindex
vars q'' \<subseteq> {1..n}

goal (1 subgoal):
 1. vars (mpoly_map_vars reindex q'') \<subseteq> {0..<n}
[PROOF STEP]
by (subst vars_mpoly_map_vars) (auto simp: reindex_def subset_iff)+
[PROOF STATE]
proof (state)
this:
vars (mpoly_map_vars reindex q'') \<subseteq> {0..<n}

goal (1 subgoal):
 1. (\<And>q'. \<lbrakk>vars q' \<subseteq> {0..<n}; \<And>m. MPoly_Type.coeff q' m \<in> C; insertion (l \<circ> poly.coeff p) q' = insertion (l \<circ> root) q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
insertion (l \<circ> root) q = insertion (l \<circ> poly.coeff p) (mpoly_map_vars reindex q'')
MPoly_Type.coeff (mpoly_map_vars reindex q'') ?m \<in> C
vars (mpoly_map_vars reindex q'') \<subseteq> {0..<n}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
insertion (l \<circ> root) q = insertion (l \<circ> poly.coeff p) (mpoly_map_vars reindex q'')
MPoly_Type.coeff (mpoly_map_vars reindex q'') ?m \<in> C
vars (mpoly_map_vars reindex q'') \<subseteq> {0..<n}

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that[of "mpoly_map_vars reindex q''"]
[PROOF STATE]
proof (prove)
using this:
insertion (l \<circ> root) q = insertion (l \<circ> poly.coeff p) (mpoly_map_vars reindex q'')
MPoly_Type.coeff (mpoly_map_vars reindex q'') ?m \<in> C
vars (mpoly_map_vars reindex q'') \<subseteq> {0..<n}
\<lbrakk>vars (mpoly_map_vars reindex q'') \<subseteq> {0..<n}; \<And>m. MPoly_Type.coeff (mpoly_map_vars reindex q'') m \<in> C; insertion (l \<circ> poly.coeff p) (mpoly_map_vars reindex q'') = insertion (l \<circ> root) q\<rbrakk> \<Longrightarrow> thesis

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma simp_regular [simp]:
  "\<exists>y . Rep_regular x = -y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. in_p_image (Rep_regular x)
[PROOF STEP]
using Rep_regular
[PROOF STATE]
proof (prove)
using this:
Rep_regular ?x \<in> regular_elements

goal (1 subgoal):
 1. in_p_image (Rep_regular x)
[PROOF STEP]
by simp


[STATEMENT]
lemma simp_dense [simp]:
  "-Rep_dense x = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dense (Rep_dense x)
[PROOF STEP]
using Rep_dense
[PROOF STATE]
proof (prove)
using this:
Rep_dense ?x \<in> dense_elements

goal (1 subgoal):
 1. dense (Rep_dense x)
[PROOF STEP]
by simp


[STATEMENT]
lemma up_filter_dense_antitone_dense:
  "dense (x \<squnion> -x \<squnion> y) \<and> dense (x \<squnion> -x \<squnion> y \<squnion> z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dense (x \<squnion> - x \<squnion> y) \<and> dense (x \<squnion> - x \<squnion> y \<squnion> z)
[PROOF STEP]
by simp


[STATEMENT]
lemma up_filter_dense_antitone:
  "up_filter (Abs_dense (x \<squnion> -x \<squnion> y \<squnion> z)) \<le> up_filter (Abs_dense (x \<squnion> -x \<squnion> y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. up_filter (Abs_dense (x \<squnion> - x \<squnion> y \<squnion> z)) \<le> up_filter (Abs_dense (x \<squnion> - x \<squnion> y))
[PROOF STEP]
by (unfold up_filter_antitone[THEN sym]) (simp add: Abs_dense_inverse less_eq_dense.rep_eq)


[STATEMENT]
lemma stone_phi_base_filter:
  "filter (stone_phi_base x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ord_class.filter (stone_phi_base x)
[PROOF STEP]
apply (unfold filter_def, intro conjI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. stone_phi_base x \<noteq> {}
 2. \<forall>xa\<in>stone_phi_base x. \<forall>y\<in>stone_phi_base x. \<exists>z\<in>stone_phi_base x. z \<le> xa \<and> z \<le> y
 3. is_up_set (stone_phi_base x)
[PROOF STEP]
apply (metis Collect_empty_eq top_dense.rep_eq top_greatest)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>xa\<in>stone_phi_base x. \<forall>y\<in>stone_phi_base x. \<exists>z\<in>stone_phi_base x. z \<le> xa \<and> z \<le> y
 2. is_up_set (stone_phi_base x)
[PROOF STEP]
apply (metis inf_dense.rep_eq inf_le2 le_inf_iff mem_Collect_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_up_set (stone_phi_base x)
[PROOF STEP]
using order_trans less_eq_dense.rep_eq
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<le> ?y; ?y \<le> ?z\<rbrakk> \<Longrightarrow> ?x \<le> ?z
(?x \<le> ?xa) = (Rep_dense ?x \<le> Rep_dense ?xa)

goal (1 subgoal):
 1. is_up_set (stone_phi_base x)
[PROOF STEP]
by blast


[STATEMENT]
lemma phi_bot:
  "phi bot = Abs_filter {top}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. phi bot = Filters.filter.Abs_filter {top}
[PROOF STEP]
by (metis hom bot_filter_def)


[STATEMENT]
lemma phi_top:
  "phi top = Abs_filter UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. phi top = Filters.filter.Abs_filter UNIV
[PROOF STEP]
by (metis hom top_filter_def)


[STATEMENT]
lemma pairs_top_in_set:
  "(x,y) \<in> pairs \<Longrightarrow> top \<in> Rep_filter y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x, y) \<in> pairs \<Longrightarrow> top \<in> Filters.filter.Rep_filter y
[PROOF STEP]
by simp


[STATEMENT]
lemma phi_complemented:
  "complement (phi x) (phi (-x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. complement (phi x) (phi (- x))
[PROOF STEP]
by (metis hom inf_compl_bot sup_compl_top)


[STATEMENT]
lemma phi_inf_principal:
  "\<exists>z . up_filter z = phi x \<sqinter> up_filter y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>z. up_filter z = phi x \<sqinter> up_filter y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>z. up_filter z = phi x \<sqinter> up_filter y
[PROOF STEP]
let ?F = "Rep_filter (phi x)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>z. up_filter z = phi x \<sqinter> up_filter y
[PROOF STEP]
let ?G = "Rep_filter (phi (-x))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>z. up_filter z = phi x \<sqinter> up_filter y
[PROOF STEP]
have 1: "eq_onp filter ?F ?F \<and> eq_onp filter (\<up>y) (\<up>y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eq_onp ord_class.filter (Filters.filter.Rep_filter (phi x)) (Filters.filter.Rep_filter (phi x)) \<and> eq_onp ord_class.filter (\<up>y) (\<up>y)
[PROOF STEP]
by (simp add: eq_onp_def)
[PROOF STATE]
proof (state)
this:
eq_onp ord_class.filter (Filters.filter.Rep_filter (phi x)) (Filters.filter.Rep_filter (phi x)) \<and> eq_onp ord_class.filter (\<up>y) (\<up>y)

goal (1 subgoal):
 1. \<exists>z. up_filter z = phi x \<sqinter> up_filter y
[PROOF STEP]
have "filter_complements ?F ?G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filter_complements (Filters.filter.Rep_filter (phi x)) (Filters.filter.Rep_filter (phi (- x)))
[PROOF STEP]
apply (intro conjI)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. ord_class.filter (Filters.filter.Rep_filter (phi x))
 2. ord_class.filter (Filters.filter.Rep_filter (phi (- x)))
 3. filter_sup (Filters.filter.Rep_filter (phi x)) (Filters.filter.Rep_filter (phi (- x))) = UNIV
 4. Filters.filter.Rep_filter (phi x) \<inter> Filters.filter.Rep_filter (phi (- x)) = {top}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. ord_class.filter (Filters.filter.Rep_filter (phi (- x)))
 2. filter_sup (Filters.filter.Rep_filter (phi x)) (Filters.filter.Rep_filter (phi (- x))) = UNIV
 3. Filters.filter.Rep_filter (phi x) \<inter> Filters.filter.Rep_filter (phi (- x)) = {top}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. filter_sup (Filters.filter.Rep_filter (phi x)) (Filters.filter.Rep_filter (phi (- x))) = UNIV
 2. Filters.filter.Rep_filter (phi x) \<inter> Filters.filter.Rep_filter (phi (- x)) = {top}
[PROOF STEP]
apply (metis (no_types) phi_complemented sup_filter.rep_eq top_filter.rep_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Filters.filter.Rep_filter (phi x) \<inter> Filters.filter.Rep_filter (phi (- x)) = {top}
[PROOF STEP]
by (metis (no_types) phi_complemented inf_filter.rep_eq bot_filter.rep_eq)
[PROOF STATE]
proof (state)
this:
filter_complements (Filters.filter.Rep_filter (phi x)) (Filters.filter.Rep_filter (phi (- x)))

goal (1 subgoal):
 1. \<exists>z. up_filter z = phi x \<sqinter> up_filter y
[PROOF STEP]
hence "is_principal_up (?F \<inter> \<up>y)"
[PROOF STATE]
proof (prove)
using this:
filter_complements (Filters.filter.Rep_filter (phi x)) (Filters.filter.Rep_filter (phi (- x)))

goal (1 subgoal):
 1. inf.is_principal_down (Filters.filter.Rep_filter (phi x) \<inter> \<up>y)
[PROOF STEP]
using complemented_filter_inf_principal
[PROOF STATE]
proof (prove)
using this:
filter_complements (Filters.filter.Rep_filter (phi x)) (Filters.filter.Rep_filter (phi (- x)))
filter_complements ?F ?G \<Longrightarrow> inf.is_principal_down (?F \<inter> \<up>?x)

goal (1 subgoal):
 1. inf.is_principal_down (Filters.filter.Rep_filter (phi x) \<inter> \<up>y)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
inf.is_principal_down (Filters.filter.Rep_filter (phi x) \<inter> \<up>y)

goal (1 subgoal):
 1. \<exists>z. up_filter z = phi x \<sqinter> up_filter y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
inf.is_principal_down (Filters.filter.Rep_filter (phi x) \<inter> \<up>y)
[PROOF STEP]
obtain z where "\<up>z = ?F \<inter> \<up>y"
[PROOF STATE]
proof (prove)
using this:
inf.is_principal_down (Filters.filter.Rep_filter (phi x) \<inter> \<up>y)

goal (1 subgoal):
 1. (\<And>z. \<up>z = Filters.filter.Rep_filter (phi x) \<inter> \<up>y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<up>z = Filters.filter.Rep_filter (phi x) \<inter> \<up>y

goal (1 subgoal):
 1. \<exists>z. up_filter z = phi x \<sqinter> up_filter y
[PROOF STEP]
hence "up_filter z = Abs_filter (?F \<inter> \<up>y)"
[PROOF STATE]
proof (prove)
using this:
\<up>z = Filters.filter.Rep_filter (phi x) \<inter> \<up>y

goal (1 subgoal):
 1. up_filter z = Filters.filter.Abs_filter (Filters.filter.Rep_filter (phi x) \<inter> \<up>y)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
up_filter z = Filters.filter.Abs_filter (Filters.filter.Rep_filter (phi x) \<inter> \<up>y)

goal (1 subgoal):
 1. \<exists>z. up_filter z = phi x \<sqinter> up_filter y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
up_filter z = Filters.filter.Abs_filter (Filters.filter.Rep_filter (phi x) \<inter> \<up>y)

goal (1 subgoal):
 1. \<exists>z. up_filter z = phi x \<sqinter> up_filter y
[PROOF STEP]
have "... = Abs_filter ?F \<sqinter> up_filter y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Filters.filter.Abs_filter (Filters.filter.Rep_filter (phi x) \<inter> \<up>y) = Filters.filter.Abs_filter (Filters.filter.Rep_filter (phi x)) \<sqinter> up_filter y
[PROOF STEP]
using 1 inf_filter.abs_eq
[PROOF STATE]
proof (prove)
using this:
eq_onp ord_class.filter (Filters.filter.Rep_filter (phi x)) (Filters.filter.Rep_filter (phi x)) \<and> eq_onp ord_class.filter (\<up>y) (\<up>y)
\<lbrakk>eq_onp ord_class.filter ?xa ?xa; eq_onp ord_class.filter ?x ?x\<rbrakk> \<Longrightarrow> Filters.filter.Abs_filter ?xa \<sqinter> Filters.filter.Abs_filter ?x = Filters.filter.Abs_filter (?xa \<inter> ?x)

goal (1 subgoal):
 1. Filters.filter.Abs_filter (Filters.filter.Rep_filter (phi x) \<inter> \<up>y) = Filters.filter.Abs_filter (Filters.filter.Rep_filter (phi x)) \<sqinter> up_filter y
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
Filters.filter.Abs_filter (Filters.filter.Rep_filter (phi x) \<inter> \<up>y) = Filters.filter.Abs_filter (Filters.filter.Rep_filter (phi x)) \<sqinter> up_filter y

goal (1 subgoal):
 1. \<exists>z. up_filter z = phi x \<sqinter> up_filter y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Filters.filter.Abs_filter (Filters.filter.Rep_filter (phi x) \<inter> \<up>y) = Filters.filter.Abs_filter (Filters.filter.Rep_filter (phi x)) \<sqinter> up_filter y

goal (1 subgoal):
 1. \<exists>z. up_filter z = phi x \<sqinter> up_filter y
[PROOF STEP]
have "... = phi x \<sqinter> up_filter y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Filters.filter.Abs_filter (Filters.filter.Rep_filter (phi x)) \<sqinter> up_filter y = phi x \<sqinter> up_filter y
[PROOF STEP]
by (simp add: Rep_filter_inverse)
[PROOF STATE]
proof (state)
this:
Filters.filter.Abs_filter (Filters.filter.Rep_filter (phi x)) \<sqinter> up_filter y = phi x \<sqinter> up_filter y

goal (1 subgoal):
 1. \<exists>z. up_filter z = phi x \<sqinter> up_filter y
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
up_filter z = phi x \<sqinter> up_filter y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
up_filter z = phi x \<sqinter> up_filter y

goal (1 subgoal):
 1. \<exists>z. up_filter z = phi x \<sqinter> up_filter y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>z. up_filter z = phi x \<sqinter> up_filter y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rho_char:
  "up_filter (rho x y) = phi x \<sqinter> up_filter y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. up_filter (rho x y) = phi x \<sqinter> up_filter y
[PROOF STEP]
by (metis (mono_tags) someI_ex rho.simps phi_inf_principal)