Theory Poly_Expansions

theory Poly_Expansions
  imports Total_Degree
begin

subsection ‹Explicit expansions›

lemma mpoly_keys_subset: "keys (mapping_of P) ⊆ Abs_poly_mapping ` (!⇩0) ` 
  {i. length i = max_vars P + 1 ∧ sum_list i ≤ total_degree P}"
proof 
  fix k assume assm: "k ∈ keys (mapping_of P)"
  define l::"nat list" where "l ≡ map (lookup k ∘ nat) [0..max_vars P]"

  have 0: "lookup k i = l!⇩0i" for i
  proof (cases "i ≤ max_vars P")
    case True
    have "l!⇩0i = (lookup k ∘ nat) ([0..max_vars P]!i)"
      by (smt (verit, best) Suc_as_int True l_def le_imp_less_Suc length_map length_upto nth0_nth
          nth_map)
    also have "... = lookup k i"
      by (simp add: True)
    finally show ?thesis 
      by simp
  next
    case False    
    hence "lookup k i = 0"
      unfolding max_vars_def vars_def
      by (metis Suc_eq_plus1 after_max_vars assm in_keys_iff max_vars_def not_less_eq_eq vars_def)
    thus ?thesis 
      using False by (simp add: l_def nth0_0)
  qed

  have 1: "k = Abs_poly_mapping ((!⇩0) l)"
    by (simp add: 0 poly_mapping_eqI)

  have "sum_list l = (∑i=0..<length l. l!⇩0i)"
    using sum_list_sum_nth by (metis nth0_nth sum.ivl_cong)
  also have "... = sum (lookup k) (keys k)"
    by (metis "1" calculation keys.rep_eq lookup_Abs_poly_mapping_nth0 nth0_sum_list)
  also have "... ≤ total_degree P"
    unfolding total_degree_def using assm by simp
  finally have 2: "sum_list l ≤ total_degree P" .

  show "k ∈ Abs_poly_mapping ` (!⇩0) ` {i. length i = max_vars P + 1 ∧ sum_list i ≤ total_degree P}"
    using 1 2 l_def by simp
qed

lemma monom_single: "monom (Poly_Mapping.single v p) a = Const a * (Var v) ^ p"
proof (induction p)
  case 0
  show ?case by (simp add: Const.abs_eq Const⇩0_def monom.abs_eq)
next
  case (Suc p)
  show ?case
    unfolding power_Suc2 semigroup_mult_class.mult.assoc[symmetric] Suc[symmetric]
    by (metis Suc_eq_plus1 Var.abs_eq Var⇩0_def monom.abs_eq mult.right_neutral mult_monom single_add)
qed

lemma coeff_monom :
"coeff (monom m a) m' = (if m=m' then a else 0)"
  unfolding coeff_def monom_def using lookup_single_eq lookup_single_not_eq
  by (metis monom.rep_eq monom_def)

lemma monom_eq_var:
"monom (Abs_poly_mapping (λv'. (Suc 0) when v=v')) 1 = MPoly (Var⇩0 v)"
proof -
  have 0: "Poly_Mapping.single (Abs_poly_mapping (λv'. Suc 0 when v=v')) 1 = Var⇩0 v"
    unfolding Var⇩0_def single_def by simp
  hence "MPoly (Poly_Mapping.single (Abs_poly_mapping (λv'. Suc 0 when v=v')) 1) = MPoly (Var⇩0 v)"
    by metis
  thus ?thesis unfolding monom_def by simp
qed

lemma monom_eq_power_var:
  "monom (Abs_poly_mapping (λv'. n when v = v')) 1 = MPoly (Var⇩0 v)^n"
proof (induction n)
  case 0
  then show ?case by simp
next
  case (Suc n)
  note t=this
  have 0: "lookup (Abs_poly_mapping (λv'. n when v = v')) = (λv'. n when v = v')
      ∧ lookup (Abs_poly_mapping (λv'. Suc 0 when v = v')) = (λv'. Suc 0 when v = v')"
    using lookup_Abs_poly_mapping by (simp add: when_def)
  hence "(λk. lookup (Abs_poly_mapping (λv'. n when v = v')) k
         + lookup (Abs_poly_mapping (λv'. Suc 0 when v = v')) k)
      = (λk. (λv'. n when v = v') k + (λv'. Suc 0 when v = v') k)"
    by simp
  also have "... = (λk. Suc n when v = k)"
    by (metis "when"(1) "when"(2) add_0_iff add_Suc_right)
  finally have 0: "(λk. lookup (Abs_poly_mapping (λv'. n when v = v')) k
         + lookup (Abs_poly_mapping (λv'. Suc 0 when v = v')) k)
      = (λk. Suc n when v = k)" by blast
  have "Abs_poly_mapping (λv'. n when v = v') + Abs_poly_mapping (λv'. Suc 0 when v = v')
      = Abs_poly_mapping (λv'. Suc n when v = v')"
    unfolding plus_poly_mapping_def apply simp using 0 by simp
  then show ?case using monom_eq_var[of v] mult_monom[of "Abs_poly_mapping (λv'. n when v = v')" 1
        "Abs_poly_mapping (λv'. Suc 0 when v = v')" 1] power_Suc2 lambda_one t by metis
qed

lemma coeff_prod_monom_not_enough:
  fixes m m' a
  assumes "∃k. lookup m k < lookup m' k"
  shows "coeff (monom m' a * Q) m = 0"
proof -
  from assms obtain k where "lookup m k < lookup m' k" by auto
  hence 0: "lookup m k ≠ lookup m' k + v" for v
    by simp
  have "m ≠ m' + m''" for m''
    unfolding lookup_inject[symmetric]
    using 0[of "lookup m'' k"]
    by (auto simp: lookup_add)
  thus ?thesis
    unfolding coeff_def times_mpoly.rep_eq times_poly_mapping.rep_eq prod_fun_def
    unfolding coeff_def[symmetric] coeff_monom
    unfolding when_def[symmetric] when_mult Sum_any_when_equal'
    apply (subst zero_class.when(2))
    by auto
qed

lemma finite_sum_mpoly_commute:
  "finite S ⟹ (∑m∈S. MPoly (f m)) = MPoly (∑m∈S. f m)"
  by (simp add: add_to_finite_sum plus_mpoly.abs_eq zero_mpoly_def)

lemma finite_prod_mpoly_commute:
  "finite S ⟹ (∏m∈S. MPoly (f m)) = MPoly (∏m∈S. f m)"
  by (simp add: mult_to_finite_prod one_mpoly_def times_mpoly.abs_eq)

lemma power_mpoly_commute: "MPoly a ^ p = MPoly (a ^ p)"
  by (transfer; auto)

lemma finite_sum_poly_mapping_commute :
"finite S ⟹ (⋀m. finite {x. f m x≠0}) ⟹
(∑m∈S. Abs_poly_mapping (f m)) = Abs_poly_mapping (λx. ∑m∈S. f m x)"
proof (induction "card S" arbitrary:S)
  case 0
  then show ?case by force
next
  case (Suc n)
  then obtain y where y_prop: "y∈S" by fastforce
  define S' where "S' = S - {y}"
  hence card_S':"card S' = n" using Suc by (simp add: y_prop)
  hence IH: "(∑m∈S'. Abs_poly_mapping (f m)) = Abs_poly_mapping (λx. ∑m∈S'. f m x)"
    using Suc by force
  have sum_disj: "(∑m∈S'. f m x) + f y x = (∑m∈S. f m x)" for x using S'_def
    by (metis Suc.prems(1) add.commute sum.remove y_prop)
  have "finite S'" by (simp add: S'_def Suc.prems(1))
  hence "(∀m∈S'. f m x = 0) ⟹ (∑m∈S'. f m x) = 0" for x by simp
  hence "{x. (∑m∈S'. f m x) ≠ 0} ⊆ (⋃m∈S'. {x. f m x ≠ 0})"
    by (smt (verit, best) UN_I mem_Collect_eq subsetI)
  hence fin_sum: "finite {x. (∑m∈S'. f m x) ≠ 0}" using Suc(4) ‹finite S'› finite_subset by blast
  have "(∑m∈S. Abs_poly_mapping (f m)) = (∑m∈S'. Abs_poly_mapping (f m)) + Abs_poly_mapping (f y)"
    using S'_def by (metis Suc.prems(1) add.commute sum.remove y_prop)
  also have "... = Abs_poly_mapping (λx. ∑m∈S'. f m x) + Abs_poly_mapping (f y)" using IH by argo
  also have "... = Abs_poly_mapping (λx. (∑m∈S'. f m x) + f y x)"
    unfolding plus_poly_mapping_def apply simp
    using lookup_Abs_poly_mapping fin_sum Suc(4)[of y] by force
  also have "... = Abs_poly_mapping (λx. (∑m∈S. f m x))" using sum_disj by presburger
  finally show ?case by blast
qed

lemma coeff_sum_monom:
  assumes "finite {m. f m≠0}"
  shows "coeff (Sum_any (λm. monom m (f m))) = f"
proof -
  define S where "S = {m. f m≠0}"
  have fin_S: "finite S" unfolding S_def using assms by simp
  have "Sum_any (λm. monom m (f m)) = Sum_any (λm. MPoly (Poly_Mapping.single m (f m)))"
    unfolding monom_def by simp
  also have "... = (∑m∈S. MPoly (Poly_Mapping.single m (f m)))"
    unfolding S_def                   
    by (metis (mono_tags, lifting) Collect_mono Sum_any.expand_superset assms single_zero zero_mpoly_def)
  also have "... = MPoly (∑m∈S. (Poly_Mapping.single m (f m)))"
    using finite_sum_mpoly_commute fin_S by fastforce
  finally have 0: "Sum_any (λm. monom m (f m)) = (MPoly (∑a∈S. (Poly_Mapping.single a (f a))))"
    by simp

  have 1:"(∑a∈S. (Poly_Mapping.single a (f a))) = Abs_poly_mapping (λm. ∑a∈S. f a when a = m)"
    unfolding single_def apply simp
    using finite_sum_poly_mapping_commute[of S "(λa. (λk'. f a when a = k'))"] fin_S by fastforce
  have "(∑a∈S. f a when a = m) = f m" for m
  proof (cases "m∈S")
    case True
    hence "finite S ∧ S = (S-{m})∪{m} ∧ (S-{m})∩{m}={}" using fin_S by blast
    hence "(∑a∈S. f a when a = m) = (∑a∈(S-{m}). f a when a = m) + (∑a∈{m}. f a when a = m)"
      by (meson True bot.extremum insert_subset sum.subset_diff)
    also have "... = f m" by auto
    finally show ?thesis using ‹m∈S› by presburger
  next
    case False
    hence "a∈S ⟹ (f a when a = m) = 0" for a unfolding when_def by force
    hence "(∑a∈S. f a when a = m) = 0" by simp
    then show ?thesis using ‹m∉S› S_def by force
  qed
  hence "(∑a∈S. (Poly_Mapping.single a (f a))) = Abs_poly_mapping f"
    using 1 by force
  hence "coeff (Sum_any (λm. monom m (f m))) = lookup (mapping_of (MPoly (Abs_poly_mapping f)))"
    using 0 coeff_def by force
  thus ?thesis using MPoly_inverse UNIV_I lookup_Abs_poly_mapping[of f] assms by metis
qed

lemma coeff_sum_monom_bis:
  assumes "finite {m. f m≠0}" and "finite S"
  shows "coeff (∑m∈S. monom m (f m)) m'= (if m'∈ S then f m' else 0)"
proof -
  define g where "g = (λm. if m∈S then f m else 0)"
  hence "{m. g m ≠ 0} ⊆ {m. f m ≠ 0}" by auto
  hence fin_g: "finite {m. g m ≠ 0}" using assms finite_subset by blast
  hence "(∑m∈S. monom m (f m)) = Sum_any (λm. monom m (g m))" using assms(2)
    by (smt (verit, best) Sum_any.conditionalize Sum_any.cong g_def monom.abs_eq monom_zero 
        single_zero)
  hence "coeff (∑m∈S. monom m (f m)) m' = coeff (Sum_any (λm. monom m (g m))) m'" by simp
  also have "... = g m'" using fin_g coeff_sum_monom by fastforce
  finally show ?thesis unfolding g_def by blast
qed


lemma cst_poly_times_monom: "MPoly (Const⇩0 (a::('a::semiring_1))) * monom m b = monom m (a*b)"
proof -
  have "MPoly (Const⇩0 a) * monom m b = monom 0 a * monom m b"
    using Const⇩0_def by (metis monom.abs_eq)
  also have "... = monom m (a*b)"
    using mult_monom[of 0 a m b] by simp
  finally show ?thesis by simp
qed

lemma cst_poly_times_monom_one: "MPoly (Const⇩0 (a::('a::semiring_1))) * monom m 1 = monom m a"
  using cst_poly_times_monom[of a m 1] by simp

lemma poly_eq_sum_monom: "P = Sum_any (λm. monom m (coeff P m))"
proof -
  have "⋀m'. coeff P m' = coeff (Sum_any (λm. monom m (coeff P m))) m'"
    using coeff_sum_monom coeff_def
    by (metis (full_types) finite_lookup)
  thus ?thesis using coeff_eq by blast
qed

lemma poly_eq_sum_monom_alt: "P = (∑m∈(keys (mapping_of P)). monom m (coeff P m))"
  using poly_eq_sum_monom[of P]
  by (smt (verit) Sum_any.conditionalize Sum_any.cong coeff_keys finite_keys monom.abs_eq monom_zero single_zero)

lemma coeff_sum:
  fixes P::"_ ⇒ 'a::comm_monoid_add mpoly"
  assumes S_fin: "finite S"
  shows "coeff (sum P S) m = (∑i∈S. coeff (P i) m)"
proof (induct rule: finite_induct[OF S_fin])
  case 1 thus ?case by (simp add: coeff_def zero_mpoly.rep_eq)
next
  case (2 x S)
  have "coeff (sum P (insert x S)) m = coeff (sum P S + P x) m"
    by (simp add: "2.hyps"(1) "2.hyps"(2) add.commute)
  also have "... = coeff (sum P S) m + coeff (P x) m"
    by (simp add: coeff_add)
  also have "... = (∑i∈S. coeff (P i) m) + coeff (P x) m"
    by (simp add: "2")
  finally show ?case
    by (simp add: "2.hyps"(1) "2.hyps"(2) add.commute)
qed

lemma coeff_var_power_le:
  "j ≤ i ⟹ MPoly_Type.coeff (Var v ^ j * P) (Poly_Mapping.single v i)
             = MPoly_Type.coeff P (Poly_Mapping.single v (i - j))"
proof -
  assume "j ≤ i"
  then have eqi: "i = j + (i - j)"
    by auto

  show ?thesis
    apply (subst eqi)
    unfolding Var.abs_eq monom_eq_power_var[symmetric] Poly_Mapping.single_add
      Poly_Mapping.single.abs_eq[symmetric]
    apply (subst More_MPoly_Type.coeff_monom_mult)
    by simp
qed

lemma coeff_var_power_eq: "MPoly_Type.coeff (Var v ^ i) (Poly_Mapping.single v i) = 1"
  using coeff_var_power_le[of i i v 1]
  unfolding insertion_trivial[symmetric] MPoly_Type.coeff_def one_mpoly.rep_eq
  by auto

lemma coeff_const: "i > 0 ⟹ MPoly_Type.coeff (Const c) (Poly_Mapping.single v i) = 0"
  unfolding MPoly_Type.coeff_def Const.rep_eq Const⇩0_def lookup_single
  unfolding single_zero[of v, symmetric]
  apply (rule "when"(2))
  by (metis lookup_single_eq nat_less_le)

lemma mpoly_univariate_expansion:
  fixes P::"'a::comm_semiring_1 mpoly" and v::nat
  assumes univariate: "vars P ⊆ {v}"
  shows "P = Sum_any (λi. monom (Poly_Mapping.single v i) (coeff P (Poly_Mapping.single v i)))"
proof -
  define K where "K = keys (mapping_of P)"
  define f where "f = (λm::nat⇒⇩0nat. lookup m v)"

  have rewrite_monom: "m∈K ⟹ m = Poly_Mapping.single v (f m)" for m
  proof -
    assume "m∈K" 
    hence "keys m ⊆ vars P" 
      unfolding vars_def K_def by auto
    hence "keys m ⊆ {v}" 
      using univariate by auto
    thus ?thesis 
      unfolding f_def
      by (metis diff_shunt_var keys_eq_empty lookup_single_eq remove_key_keys 
          remove_key_single remove_key_sum)
  qed

  have f_inj: "inj_on f K" 
    using rewrite_monom by (metis inj_onI) 

  have coeff_null: "i ∉ f ` K ⟹ 
    monom (Poly_Mapping.single v i) (coeff P (Poly_Mapping.single v i)) = 0" for i
  proof -
    assume "i ∉ f ` K"
    hence "Poly_Mapping.single v i ∉ K" 
      unfolding f_def by force
    hence "coeff P (Poly_Mapping.single v i) = 0" 
      unfolding K_def coeff_def by (simp add: in_keys_iff)
    thus ?thesis by (metis mult_zero_left smult_0 smult_monom)
  qed

  have "P = (∑m∈K. monom m (coeff P m))"
    by (simp add: K_def poly_eq_sum_monom_alt)
  also have "... = (∑m∈K. monom (Poly_Mapping.single v (f m)) (coeff P (Poly_Mapping.single v (f m))))"
    using rewrite_monom by simp
  also have "... = (∑i∈f ` K. monom (Poly_Mapping.single v i) (coeff P (Poly_Mapping.single v i)))"
    by (metis (mono_tags, lifting) f_inj sum.reindex_cong)
  also have "... = Sum_any (λi. monom (Poly_Mapping.single v i) (coeff P (Poly_Mapping.single v i)))"
    using coeff_null
    by (smt (verit) K_def Sum_any.conditionalize Sum_any.cong finite_imageI finite_keys)
  finally show ?thesis .
qed


lemma term_expansion_lemma_1: "i ≠ [] ⟹
  Poly_Mapping.single (Abs_poly_mapping ((!⇩0) i)) (1 :: 'a::comm_semiring_1) =
  (∏s = 0..(length i - 1). Var⇩0 s ^ (i ! s))"
proof (induction i rule: length_induct)
  case (1 i)
  show ?case proof (cases i rule: rev_exhaust)
    case Nil
    thus ?thesis using 1 by auto
  next
    case (snoc i' x)
    show ?thesis proof cases
      assume i'_def: "i' = []"
      have "Poly_Mapping.single (Abs_poly_mapping ((!⇩0) [x])) 1 = Var⇩0 0 ^ x"
        unfolding MPoly_Type.Var⇩0_power by auto
      thus ?thesis unfolding snoc i'_def by auto
    next
      assume i'_non_empty: "i' ≠ []"
      have "(∏s = 0..length i'. Var⇩0 s ^ ((i' @ [x]) ! s)) =
        Poly_Mapping.single (Abs_poly_mapping ((!⇩0) (i' @ [x]))) (1 :: 'a)" proof -
        have "(∏s = 0..length i'. Var⇩0 s ^ ((i' @ [x]) ! s)) =
          (∏s = 0..Suc (length i' - 1). Var⇩0 s ^ ((i' @ [x]) ! s))"
          using i'_non_empty by auto
        also have "... = (∏s = 0..length i' - 1. Var⇩0 s ^ ((i' @ [x]) ! s)) *
          Var⇩0 (Suc (length i' - 1)) ^ ((i' @ [x]) ! (Suc (length i' - 1)))"
          using prod.atLeast0_atMost_Suc by auto
        also have "... = (∏s = 0..length i' - 1. Var⇩0 s ^ ((i' @ [x]) ! s)) *
          Var⇩0 (length i') ^ ((i' @ [x]) ! (length i'))"
          using i'_non_empty by auto
        also have "... = (∏s = 0..length i' - 1. Var⇩0 s ^ ((i' @ [x]) ! s)) *
          Var⇩0 (length i') ^ x" by auto
        also have "... = (∏s = 0..length i' - 1. Var⇩0 s ^ (i' ! s)) *
          Var⇩0 (length i') ^ x"
          by (auto simp add: List.nth_append i'_non_empty order_le_less_trans)
        also have "... = Poly_Mapping.single (Abs_poly_mapping ((!⇩0) i'))
          (1 :: 'a) * Var⇩0 (length i') ^ x" using 1 snoc i'_non_empty by auto
        also have "... = Poly_Mapping.single (Abs_poly_mapping ((!⇩0) i')) 1 *
          Poly_Mapping.single (Poly_Mapping.single (length i') x) 1"
          unfolding MPoly_Type.Var⇩0_power by simp
        also have "... = Poly_Mapping.single (Abs_poly_mapping ((!⇩0) i))
          (1 :: 'a)" proof -
          have "Abs_poly_mapping ((!⇩0) i') + Poly_Mapping.single (length i') x =
            Abs_poly_mapping ((!⇩0) i)" unfolding snoc by auto
          thus ?thesis by (simp add: Poly_Mapping.mult_single)
        qed
        finally show ?thesis unfolding snoc .
      qed
      thus ?thesis unfolding snoc by auto
    qed
  qed
qed

lemma term_expansion_lemma_2: "i ≠ [] ⟹
  monom (Abs_poly_mapping ((!⇩0) i)) c =
  MPoly (Const⇩0 c) * MPoly (∏s = 0..length i - 1. Var⇩0 s ^ (i ! s))"
  unfolding term_expansion_lemma_1[symmetric] monom.abs_eq[symmetric]
    cst_poly_times_monom_one by simp

lemma term_expansion: "i ≠ [] ⟹
  monom (Abs_poly_mapping ((!⇩0) i)) c =
  Const c * (∏s = 0..length i - 1. Var s ^ (i ! s))"
  unfolding MPoly_Type.Const.abs_eq MPoly_Type.Var.abs_eq term_expansion_lemma_2
  by (simp add: finite_prod_mpoly_commute power_mpoly_commute)

fun sample_prefix :: "nat ⇒ (nat ⇒ 'a) ⇒ 'a list" where
  "sample_prefix 0 f = []" |
  "sample_prefix (Suc l) f = sample_prefix l f @ [f l]"

lemma sample_prefix_length[simp]: "length (sample_prefix l f) = l"
  by (induction l; auto)

lemma sample_prefix_cong:
  "(∀x<n. f x = g x) ⟹ sample_prefix n f = sample_prefix n g"
proof -
  assume "∀x<n. f x = g x"
  hence "l ≤ n ⟹ sample_prefix l f = sample_prefix l g" for l
    by (induction l; auto)
  thus ?thesis by auto
qed

lemma sample_prefix_inv_nth0: "(∀i≥n. f i = 0) ⟹ f = (!⇩0) (sample_prefix n f)"
proof (induction n arbitrary: f)
  case 0
  thus ?case unfolding nth0_def by simp
next
  case (Suc n)
  let ?g = "λx. f x when x < n"
  have "?g = (!⇩0) (sample_prefix n ?g)" using Suc by auto
  also have "... = (!⇩0) (sample_prefix n f)"
    using sample_prefix_cong[of n f ?g] by auto
  finally have 0: "?g = (!⇩0) (sample_prefix n f)" .
  have "f = (λx. if x = n then f n else ?g x)" unfolding when_def using Suc by auto
  also have "... = (λx. if x = n then f n else (!⇩0) (sample_prefix n f) x)"
    unfolding 0[symmetric] by simp
  also have "... = (!⇩0) (sample_prefix (Suc n) f)"
    apply (rule ext)
    subgoal for x
      apply (cases "x = n")
      unfolding nth0_def apply simp_all
      unfolding List.nth_append apply simp_all
      done
    done
  finally show ?case .
qed

lemma sample_prefix_inj:
  "inj_on (λf. sample_prefix n f) {f. ∀i≥n. (f i :: 'a::zero) = 0}"
proof
  fix g h
  assume "g ∈ {f. ∀i≥n. (f i :: 'a::zero) = 0}"
  hence 0: "∀i≥n. g i = 0" by auto
  assume "h ∈ {f. ∀i≥n. (f i :: 'a::zero) = 0}"
  hence 1: "∀i≥n. h i = 0" by auto
  assume "sample_prefix n g = sample_prefix n h"
  hence "(!⇩0) (sample_prefix n g) = (!⇩0) (sample_prefix n h)" by auto
  thus "g = h" using 0 1 by (simp add: sample_prefix_inv_nth0[symmetric])
qed

lemma lookup_nth0_total_degree:
  "lookup (mapping_of P) (Abs_poly_mapping ((!⇩0) i)) ≠ 0 ⟹
  sum_list i ≤ total_degree P"
  apply transfer
  apply (rule Max_ge)
  subgoal for P i
    apply simp
    done
  subgoal for P i
    unfolding image_def keys_def apply simp
    using nth0_sum_list[of i] apply auto
    done
  done

lemma prod_monom: "finite S ⟹ prod (λs. monom (x s) (a s)) S = monom (sum x S) (prod a S)"
proof (induction "card S" arbitrary:S)
  case 0
  then show ?case by auto
next
  case (Suc n)
  then obtain y where y_prop: "y∈S" by fastforce
  define S' where "S' = S - {y}"
  with Suc(3) have "finite S'" by auto
  from S'_def have card_S': "card S' = n" using Suc by (simp add: y_prop)
  have disj_un_S: "S = S'∪{y} ∧ S'∩{y}={}∧finite S" using y_prop S'_def Suc by force
  hence "(∏s∈S. monom (x s) (a s)) = (∏s∈S'. monom (x s) (a s)) * (∏s∈{y}. monom (x s) (a s))"
    by (meson finite_Un prod.union_disjoint)
  also have "... = monom (sum x S') (prod a S') * monom (x y) (a y)"
    using Suc(1)[of "S'"] card_S' ‹finite S'› by auto
  also have "... = monom (sum x S' + x y) (prod a S' * a y)"
    using mult_monom by auto
  finally show "(∏s∈S. monom (x s) (a s)) = monom (sum x S) (prod a S)"
    using S'_def Suc
    by (smt (verit, ccfv_threshold) add.commute mult.commute prod.remove sum.remove y_prop)
qed

lemma poly_mapping_expansion: "x = (∑s∈keys x. Abs_poly_mapping (λv'. lookup x s when s = v'))"
proof - 
  have h0: "(∑xa∈keys x. lookup (Abs_poly_mapping (λv'. lookup x xa when xa = v')) i)
         = (∑xa∈keys x. (λv'. lookup x xa when xa = v') i)" for i
    by (rule sum.cong, auto)
  define x_fun where "x_fun ≡ lookup x"
  have h1: "lookup x i = (∑xa∈keys x. lookup x xa when xa = i)" for i
    apply (cases "i ∈ keys x", simp add: sum.remove[OF finite_keys])
    unfolding keys.rep_eq x_fun_def[symmetric]
    by (smt (verit, ccfv_SIG) mem_Collect_eq sum.neutral when_simps(2))

  thus ?thesis
    unfolding lookup_inject[symmetric] lookup_sum h0 by blast
qed

lemma monom_expansion:
  shows "monom x c = Const c * (∏s∈keys x. Var s ^ (lookup x s))"
  unfolding Var.abs_eq monom_eq_power_var[symmetric]
  apply (subst prod_monom[OF finite_keys, where ?a = "λ_. 1"])
  apply (simp add: Const.abs_eq cst_poly_times_monom)
  by (subst poly_mapping_expansion) simp

lemma monom_expansion':
  fixes P :: "'a::{ring_no_zero_divisors,comm_semiring_1} mpoly"
  assumes "x ∈ keys (mapping_of P)"
  shows "monom x (coeff P x) = Const (coeff P x) * (∏s = 0..max_vars P. Var s ^ (lookup x s))"
proof (cases "vars P = {}")
  case True
  then show ?thesis 
    by (metis (no_types, lifting) Poly_Expansions.coeff_monom assms
        atLeastAtMost_singleton coeff_keys empty_iff finite.emptyI keys_zero
        lookup_zero max_vars_Const monom_expansion mult.commute mult_1 power_0
        prod.empty prod.insert vars_empty)
next
  case False
  then show ?thesis 
  unfolding max_vars_of_nonempty[OF False]
  apply (subst monom_expansion)
  apply (subst mult_cancel_left, rule disjI2)
  apply (rule prod.mono_neutral_cong_left)
  using assms apply simp_all
  subgoal 
    by (metis Max_ge UN_I atLeastAtMost_iff le0 subsetI vars_def
        vars_finite)
  subgoal
    by (simp add: in_keys_iff)
  done
qed

lemma mpoly_multivariate_expansion':
  fixes P::"'a::{ring_no_zero_divisors,comm_semiring_1} mpoly"
  shows "P = (∑m∈keys (mapping_of P). 
                  Const (coeff P m) * (∏s = 0..max_vars P. (Var s) ^ (lookup m s)))"
  apply (subst poly_eq_sum_monom_alt)
  by (rule sum.cong, simp_all add: monom_expansion')

lemma mpoly_multivariate_expansion:
  fixes P::"'a::comm_semiring_1 mpoly"
  shows "P = (∑i | length i = max_vars P + 1 ∧ sum_list i ≤ total_degree P. 
    Const (coeff P (Abs_poly_mapping ((!⇩0) i))) *
    (∏s = 0..max_vars P. (Var s) ^ (i ! s)))"
proof -
  let ?t = "λm. (sample_prefix (max_vars P + 1) (lookup m))"
  have "P = (∑m∈keys (mapping_of P). monom m (coeff P m))"
    by (rule poly_eq_sum_monom_alt)
  also have "... = (∑m | lookup (mapping_of P) m ≠ 0. monom m (coeff P m))"
    unfolding Poly_Mapping.in_keys_iff[symmetric] by auto
  also have "... = (∑m | lookup (mapping_of P) m ≠ 0.
    monom (Abs_poly_mapping (lookup m)) (coeff P (Abs_poly_mapping (lookup m))))"
    by auto
  also have "... = (∑i | length i = max_vars P + 1 ∧
    lookup (mapping_of P) (Abs_poly_mapping ((!⇩0) i)) ≠ 0.
    monom (Abs_poly_mapping ((!⇩0) i)) (coeff P (Abs_poly_mapping ((!⇩0) i))))"
  proof (rule sum.reindex_cong[symmetric, of ?t])
    let ?S = "{m. lookup (mapping_of P) m ≠ 0}"
    let ?T = "{i. length i = max_vars P + 1 ∧
      lookup (mapping_of P) (Abs_poly_mapping ((!⇩0) i)) ≠ 0}"
    show "inj_on ?t ?S" 
      proof
        fix m1 m2
        assume "m1 ∈ {m. lookup (mapping_of P) m ≠ 0}"
        hence 1: "∀v≥(max_vars P + 1). lookup m1 v = 0" using after_max_vars by auto
        assume "m2 ∈ {m. lookup (mapping_of P) m ≠ 0}"
        hence 2: "∀v≥(max_vars P + 1). lookup m2 v = 0" using after_max_vars by auto
        assume "sample_prefix (max_vars P + 1) (lookup m1) =
          sample_prefix (max_vars P + 1) (lookup m2)"
        hence "lookup m1 = lookup m2"
          using sample_prefix_inj[of "max_vars P + 1"] 1 2
          unfolding inj_on_def by blast
        thus "m1 = m2" by auto
      qed
    show "?T = ?t ` ?S" 
    proof (rule set_eqI; rule iffI)
      fix i
      assume 3: "i ∈ ?T"
      let ?m = "Abs_poly_mapping ((!⇩0) i)"
      from 3 have 4: "lookup (mapping_of P) ?m ≠ 0" by auto
      have "lookup ?m = (!⇩0) (sample_prefix (max_vars P + 1) (lookup ?m))"
        apply (rule sample_prefix_inv_nth0)
        using after_max_vars[of P ?m] 4 by auto
      hence "(!⇩0) i = (!⇩0) (sample_prefix (max_vars P + 1) (lookup ?m))" by auto
      hence 5: "i = (sample_prefix (max_vars P + 1) (lookup ?m))"
        using nth0_inj[of i] 3 by auto
      from 4 5 have "∃m. lookup (mapping_of P) m ≠ 0 ∧
        i = sample_prefix (max_vars P + 1) (lookup m)" by blast
      thus "i ∈ ?t ` ?S" unfolding image_def by auto
    next
      fix i
      assume "i ∈ ?t ` ?S"
      then obtain m where 6: "lookup (mapping_of P) m ≠ 0"
        "i = sample_prefix (max_vars P + 1) (lookup m)" by blast
      have 7: "length i = max_vars P + 1" using 6 by auto
      have "lookup m = (!⇩0) (sample_prefix (max_vars P + 1) (lookup m))"
        apply (rule sample_prefix_inv_nth0)
        using after_max_vars[of P m] 6 apply auto
        done
      hence 8: "lookup (mapping_of P) (Abs_poly_mapping ((!⇩0) i)) ≠ 0"
        using 6 by auto
      from 7 8 show "i ∈ ?T" by blast
    qed
    show "m ∈ ?S ⟹
      monom (Abs_poly_mapping ((!⇩0) (?t m)))
        (coeff P (Abs_poly_mapping ((!⇩0) (?t m)))) =
      monom (Abs_poly_mapping (lookup m))
        (coeff P (Abs_poly_mapping (lookup m)))" for m
    proof -
      assume 9: "m ∈ ?S"
      have "lookup m = (!⇩0) (sample_prefix (max_vars P + 1) (lookup m))"
        apply (rule sample_prefix_inv_nth0)
        using after_max_vars[of P m] 9 apply auto
        done
      thus ?thesis by auto
    qed
  qed
  also have "... = (∑i | length i = max_vars P + 1 ∧ sum_list i ≤ total_degree P.
    monom (Abs_poly_mapping ((!⇩0) i)) (coeff P (Abs_poly_mapping ((!⇩0) i))))"
  proof (rule sum.mono_neutral_left)
    let ?A = "{i. length i = max_vars P + 1 ∧
     lookup (mapping_of P) (Abs_poly_mapping ((!⇩0) i)) ≠ 0}"
    let ?B = "{i. length i = max_vars P + 1 ∧ sum_list i ≤ total_degree P}"
    have "?B ⊆ {i. set i ⊆ {0..total_degree P} ∧ length i = max_vars P + 1}"
      using member_le_sum_list by fastforce
    also have "finite ..."  using List.finite_lists_length_eq by auto
    ultimately show "finite ?B" using Finite_Set.finite_subset by auto
    show "?A ⊆ ?B" using lookup_nth0_total_degree by auto
    show "∀i∈?B - ?A. monom (Abs_poly_mapping ((!⇩0) i))
      (coeff P (Abs_poly_mapping ((!⇩0) i))) = 0"
      by (simp add: coeff_all_0 coeff_def)
  qed
  also have "... = (∑i | length i = max_vars P + 1 ∧ sum_list i ≤ total_degree P.
    Const (coeff P (Abs_poly_mapping ((!⇩0) i))) *
    (∏s = 0..max_vars P. (Var s) ^ (i ! s)))"
  proof (rule sum.cong[OF refl])
    fix i
    assume i_porp:
      "i ∈ {i. length i = max_vars P + 1 ∧ sum_list i ≤ total_degree P}"
    hence "i ≠ []" "length i - 1 = max_vars P" by auto
    thus "monom (Abs_poly_mapping ((!⇩0) i)) (coeff P (Abs_poly_mapping ((!⇩0) i))) =
      Const (coeff P (Abs_poly_mapping ((!⇩0) i))) *
      (∏s = 0..max_vars P. Var s ^ i ! s)"
      by (simp add: term_expansion)
  qed
  finally show ?thesis .
qed


lemma mpoly_univariate_expansion_sum:
  fixes P :: "('a::comm_ring_1) mpoly"
  assumes "vars P ⊆ {v}"
  defines "q ≡ MPoly_Type.degree P v"
  defines "coeff_P ≡ (λd. coeff P (Poly_Mapping.single v d))"
  shows "P = (∑d = 0..q. Const (coeff_P d) * (Var v) ^ d)"
  unfolding coeff_P_def
  apply (subst mpoly_univariate_expansion[of P v, OF assms(1)])
  unfolding monom_single
  unfolding Sum_any.expand_set
  apply (rule sum.mono_neutral_cong_left)
  subgoal by auto
  subgoal unfolding q_def degree.rep_eq
  proof -
    have "Const (coeff P (Poly_Mapping.single v p)) * Var v ^ p ≠ 0 ⟹
      p ∈ {0..Max (insert 0 ((λm. lookup m v) ` keys (mapping_of P)))}" for p
    proof -
      assume "Const (coeff P (Poly_Mapping.single v p)) * Var v ^ p ≠ 0"
      hence "coeff P (Poly_Mapping.single v p) ≠ 0"
        by (metis Const_zero lambda_zero)
      hence "p ∈ (λm. lookup m v) ` keys (mapping_of P)"
        by (metis coeff_def imageI in_keys_iff lookup_single_eq)
      thus "p ∈ {0..Max (insert 0 ((λm. lookup m v) ` keys (mapping_of P)))}"
        by simp
    qed
    thus "{a. Const (coeff P (Poly_Mapping.single v a)) * Var v ^ a ≠ 0}
      ⊆ {0..Max (insert 0 ((λm. lookup m v) ` keys (mapping_of P)))}"
      by blast
  qed
  subgoal by auto
  subgoal by auto
  done

end