(*
  File:         PAC_More_Poly.thy
  Author:       Mathias Fleury, Daniela Kaufmann, JKU
  Maintainer:   Mathias Fleury, JKU
*)
theory PAC_More_Poly
  imports "HOL-Library.Poly_Mapping" "HOL-Algebra.Polynomials" "Polynomials.MPoly_Type_Class"
  "HOL-Algebra.Module" "HOL-Library.Countable_Set"
begin


section ‹Overview›

text ‹

One solution to check circuit of multipliers is to use algebraic method, like producing proofs on
polynomials.  We are here interested in checking PAC proofs on the Boolean ring. The idea is the
following: each variable represents an input or the output of a gate and we want to prove the
bitwise multiplication of the input bits yields the output, namely the bitwise representation of the
multiplication of the input (modulo \<^term>‹(2::nat)^n› where \<^term>‹n::nat› is the number of bits of the
circuit).

Algebraic proof systems typically reason over polynomials in a ring $\set K[X]$,
where the variables $X$ represent Boolean values.
The aim of an algebraic proof is to derive whether a polynomial $f$ can be derived from a given set of polynomials
$G = \{g_1,\dots,g_l\} \subseteq \set K[X]$ together with the Boolean value constraints
$B(X) = \{x^2_i-x_i \mid x_i \in X\}$. In algebraic terms this means to show that the polynomial \<^latex>‹\(f \in \langle G \cup B(X)\rangle\)›.

In our setting we set $\set K = \set Z$ and we treat the Boolean value constraints implicitly, i.e.,
we consider proofs in the ring \<^latex>‹\(\set Z[X]/\langle B(X)\rangle\)› to admit shorter proofs



The checker takes as input 3 files:
  ▸ an input file containing all polynomials that are initially present;
  ▸ a target (or specification) polynomial ;
  ▸ a ``proof'' file to check that contains the proof in PAC format that shows that the specification
  is in the ideal generated by the polynomials present initially.


Each step of the proof is either an addition of two polynomials previously derived, a multiplication
from a previously derived polynomial and an arbitrary polynomial, and the deletion a derived
polynomial.

One restriction on the proofs compared to generic PAC proofs is that \<^term>‹(x::nat)^2 = x› in the
Boolean ring we are considering.

The checker can produce two outputs: valid (meaning that each derived polynomial in the proof has
been correctly derived and the specification polynomial was also derived at some point [either in
the proof or as input]) or invalid (without proven information what went wrong).


The development is organised as follows:
  ▪ 🗏‹PAC_Specification.thy› (this file) contains the specification as described above on ideals
  without any peculiarities on the PAC proof format
  ▪ 🗏‹PAC_Checker_Specification.thy› specialises to the PAC format and enters the nondeterminism
  monad to prepare the subsequent refinements.
  ▪ 🗏‹PAC_Checker.thy› contains the refined version where polynomials are represented as lists.
  ▪ 🗏‹PAC_Checker_Synthesis.thy› contains the efficient implementation with imperative data
  structure like a hash set.
  ▪ 🗏‹PAC_Checker_MLton.thy› contains the code generation and the command to compile the file with
  the ML compiler MLton.


Here is an example of a proof and an input file (taken from the appendix of our FMCAD
paper~\cite{KaufmannFleuryBiere-FMCAD20}, available at 🌐‹http://fmv.jku.at/pacheck_pasteque›):
▩‹
<res.input>      <res.proof>
 1 x*y;           3  = fz, -z+1;
 2 y*z-y-z+1;     4  *  3,  y-1, -fz*y+fz-y*z+y+z-1;
                  5  +  2,    4, -fz*y+fz;
                  2  d;
                  4  d;
<res.target>      6  *  1,   fz, fz*x*y;
 -x*z+x;          1  d;
                  7  *  5,    x, -fz*x*y+fz*x;
                  8  +  6,    7, fz*x;
                  9  *  3,    x, -fz*x-x*z+x;
                 10  +  8,    9, -x*z+x;
›

Each line starts with a number that is used to index the (conclusion) polynomial. In the proof,
there are four kind of steps:
  ▸ ▩‹3 = fz, -z+1;› is an extension that introduces a new variable (in this case ▩‹fz›);
  ▸ ▩‹4  *  3,  y-1, -fz*y+fz-y*z+y+z-1;› is a multiplication of the existing polynomial with
  index 3 by the arbitrary polynomial ▩‹y-1› and generates the new polynomial
  ▩‹-fz*y+fz-y*z+y+z-1› with index 4;
  ▸ ▩‹5  +  2,    4, -fz*y+fz;› is an addition of the existing polynomials with
  index 2 and 4 and generates the new polynomial ▩‹-fz*y+fz› with index 5;
  ▸ ▩‹1  d;› deletes the polynomial with index 1 and it cannot be reused in subsequent steps.



Remark that unlike DRAT checker, we do forward checking and check every derived polynomial. The
target polynomial can also be part of the input file.
›

section ‹Libraries›

subsection ‹More Polynomials›

text ‹

  Here are more theorems on polynomials. Most of these facts are
  extremely trivial and should probably be generalised and moved to
  the Isabelle distribution.
›

lemma Const⇩0_add:
  ‹Const⇩0 (a + b) = Const⇩0 a + Const⇩0 b›
  by transfer
   (simp add: Const⇩0_def single_add)

lemma Const_mult:
  ‹Const (a * b) = Const a * Const b›
  by transfer (simp add: Const⇩0_def times_monomial_monomial)

lemma Const⇩0_mult:
  ‹Const⇩0 (a * b) = Const⇩0 a * Const⇩0 b›
  by transfer (simp add: Const⇩0_def times_monomial_monomial)

lemma Const0[simp]:
  ‹Const 0 = 0›
  by transfer (simp add: Const⇩0_def)

lemma (in -) Const_uminus[simp]:
  ‹Const (-n) = - Const n›
  by transfer (auto simp: Const⇩0_def monomial_uminus)

lemma [simp]: ‹Const⇩0 0 = 0›
  ‹MPoly 0 = 0›
  by (auto simp: Const⇩0_def zero_mpoly_def)

lemma Const_add:
  ‹Const (a + b) = Const a + Const b›
  by transfer (simp add: Const⇩0_def single_add)

instance mpoly :: (comm_semiring_1) comm_semiring_1
  by standard

lemma degree_uminus[simp]:
  ‹degree (-A) x' = degree A x'›
  by (auto simp: degree_def uminus_mpoly.rep_eq)

lemma degree_sum_notin:
  ‹x' ∉ vars B ⟹ degree (A + B) x' = degree A x'›
  apply (auto simp: degree_def)
  apply (rule arg_cong[of _ _ Max])
  apply standard+
  apply (auto simp: plus_mpoly.rep_eq UN_I UnE image_iff in_keys_iff subsetD vars_def lookup_add
    dest: keys_add intro: in_keys_plusI1 cong: ball_cong_simp)
  done

lemma degree_notin_vars:
  ‹x ∉ (vars B) ⟹ degree (B :: 'a :: {monoid_add} mpoly) x = 0›
  using degree_sum_notin[of x B 0]
  by auto

lemma not_in_vars_coeff0:
  ‹x ∉ vars p ⟹ MPoly_Type.coeff p (monomial (Suc 0) x) = 0›
  by (subst not_not[symmetric], subst coeff_keys[symmetric])
    (auto simp: vars_def)

lemma keys_add':
  "p ∈ keys (f + g) ⟹ p ∈ keys f ∪ keys g"
  by transfer auto

lemma keys_mapping_sum_add:
  ‹finite A ⟹ keys (mapping_of (∑v ∈ A. f v)) ⊆ ⋃(keys ` mapping_of ` f ` UNIV)›
  by (induction A rule: finite_induct)
   (auto simp add: zero_mpoly.rep_eq plus_mpoly.rep_eq
     keys_plus_ninv_comm_monoid_add dest: keys_add')

lemma vars_sum_vars_union:
  fixes f :: ‹int mpoly ⇒ int mpoly›
  assumes ‹finite {v. f v ≠ 0}›
  shows ‹vars (∑v | f v ≠ 0. f v * v) ⊆ ⋃(vars ` {v. f v ≠ 0}) ∪ ⋃(vars ` f ` {v. f v ≠ 0})›
    (is ‹?A ⊆ ?B›)
proof
  fix p
  assume ‹p ∈ vars (∑v | f v ≠ 0. f v * v)›
  then obtain x where ‹x ∈ keys (mapping_of (∑v | f v ≠ 0. f v * v))› and
    p: ‹p ∈ keys x›
    by (auto simp: vars_def times_mpoly.rep_eq simp del: keys_mult)
  then have ‹x ∈ (⋃x. keys (mapping_of (f x) * mapping_of x))›
    using keys_mapping_sum_add[of ‹{v. f v ≠ 0}› ‹λx. f x * x›] assms
    by (auto simp: vars_def times_mpoly.rep_eq)
  then have ‹x ∈ (⋃x. {a+b| a b. a ∈ keys (mapping_of (f x)) ∧ b ∈ keys (mapping_of x)})›
    using Union_mono[OF ] keys_mult by fast
  then show ‹p ∈ ?B›
    using p by (force simp: vars_def zero_mpoly.rep_eq dest!: keys_add')
qed


lemma vars_in_right_only:
  "x ∈ vars q ⟹ x ∉ vars p ⟹ x ∈ vars (p+q)"
  unfolding  vars_def keys_def plus_mpoly.rep_eq lookup_plus_fun
  apply clarify
  subgoal for xa
    by (auto simp: vars_def keys_def plus_mpoly.rep_eq
      lookup_plus_fun intro!: exI[of _ xa] dest!: spec[of _ xa])
  done

lemma [simp]:
  ‹vars 0 = {}›
  by (simp add: vars_def zero_mpoly.rep_eq)


lemma vars_Un_nointer:
  ‹keys (mapping_of p) ∩  keys (mapping_of q) = {} ⟹ vars (p + q) = vars p ∪ vars q›
  by (auto simp: vars_def plus_mpoly.rep_eq simp flip: More_MPoly_Type.keys_add dest!: keys_add')

lemmas [simp] = zero_mpoly.rep_eq

lemma polynomial_sum_monoms:
  fixes p :: ‹'a :: {comm_monoid_add,cancel_comm_monoid_add} mpoly›
  shows
     ‹p = (∑x∈keys (mapping_of p). MPoly_Type.monom x (MPoly_Type.coeff p x))›
     ‹keys (mapping_of p) ⊆ I ⟹ finite I ⟹ p = (∑x∈I. MPoly_Type.monom x (MPoly_Type.coeff p x))›
proof -
  define J where ‹J ≡ keys (mapping_of p)›
  define a where ‹a x ≡ coeff p x› for x
  have ‹finite (keys (mapping_of p))›
    by auto
  have ‹p = (∑x∈I. MPoly_Type.monom x (MPoly_Type.coeff p x))›
    if ‹finite I› and ‹keys (mapping_of p) ⊆ I›
    for I
    using that
    unfolding a_def
   proof (induction I arbitrary: p rule: finite_induct)
      case empty
      then have ‹p = 0›
        using empty coeff_all_0 coeff_keys by blast
      then show ?case using empty by (auto simp: zero_mpoly.rep_eq)
    next
      case (insert x F) note fin = this(1) and xF = this(2) and IH = this(3) and
        incl = this(4)
      let ?p = ‹p - MPoly_Type.monom x (MPoly_Type.coeff p x)›
      have H: ‹⋀xa. x ∉ F ⟹ xa ∈ F ⟹
        MPoly_Type.monom xa (MPoly_Type.coeff (p - MPoly_Type.monom x (MPoly_Type.coeff p x)) xa) =
         MPoly_Type.monom xa (MPoly_Type.coeff p xa)›
        by (metis (mono_tags, hide_lams) add_diff_cancel_right' remove_term_coeff
          remove_term_sum when_def)
      have ‹?p = (∑xa∈F. MPoly_Type.monom xa (MPoly_Type.coeff ?p xa))›
        apply (rule IH)
        using incl apply -
        by standard (smt Diff_iff Diff_insert_absorb add_diff_cancel_right'
          remove_term_keys remove_term_sum subsetD xF)
      also have ‹... = (∑xa∈F. MPoly_Type.monom xa (MPoly_Type.coeff p xa))›
        by (use xF in ‹auto intro!: sum.cong simp: H›)
      finally show ?case
        apply (subst (asm) remove_term_sum[of x p, symmetric])
        apply (subst remove_term_sum[of x p, symmetric])
        using xF fin by (auto simp: ac_simps)
    qed
    from this[of I] this[of J] show
     ‹p = (∑x∈keys (mapping_of p). MPoly_Type.monom x (MPoly_Type.coeff p x))›
     ‹keys (mapping_of p) ⊆ I ⟹ finite I ⟹ p = (∑x∈I. MPoly_Type.monom x (MPoly_Type.coeff p x))›
     by (auto simp: J_def)
qed


lemma vars_mult_monom:
  fixes p :: ‹int mpoly›
  shows ‹vars (p * (monom (monomial (Suc 0) x') 1)) = (if p = 0 then {} else insert x' (vars p))›
proof -

  let ?v = ‹monom (monomial (Suc 0) x') 1›
  have
    p: ‹p = (∑x∈keys (mapping_of p). MPoly_Type.monom x (MPoly_Type.coeff p x))› (is ‹_ = (∑x ∈ ?I. ?f x)›)
    using polynomial_sum_monoms(1)[of p] .
  have pv: ‹p * ?v = (∑x ∈ ?I. ?f x * ?v)›
    by (subst p) (auto simp:  field_simps sum_distrib_left)
  define I where ‹I ≡ ?I›
  have in_keysD: ‹x ∈ keys (mapping_of (∑x∈I. MPoly_Type.monom x (h x)))  ⟹ x ∈ I›
   if ‹finite I› for I and h :: ‹_ ⇒ int› and x
   using that by (induction rule: finite_induct)
    (force simp: monom.rep_eq empty_iff insert_iff keys_single coeff_monom
     simp: coeff_keys simp flip: coeff_add
     simp del: coeff_add)+
  have in_keys: ‹keys (mapping_of (∑x∈I. MPoly_Type.monom x (h x))) = (⋃x ∈ I. (if h x  = 0 then {} else {x}))›
   if ‹finite I› for I and h :: ‹_ ⇒ int› and x
   supply in_keysD[dest]
   using that by (induction rule: finite_induct)
     (auto simp: plus_mpoly.rep_eq MPoly_Type_Class.keys_plus_eqI)

  have H[simp]: ‹vars ((∑x∈I. MPoly_Type.monom x (h x))) = (⋃x∈I. (if h x  = 0 then {} else keys x))›
   if ‹finite I› for I and h :: ‹_ ⇒ int›
   using that by (auto simp: vars_def in_keys)

  have sums: ‹(∑x∈I.
        MPoly_Type.monom (x + a') (c x)) =
       (∑x∈ (λx. x + a') ` I.
        MPoly_Type.monom x (c (x - a')))›
    if ‹finite I› for I a' c q
    using that apply (induction rule: finite_induct)
    subgoal by auto
    subgoal
      unfolding image_insert by (subst sum.insert) auto
    done
  have non_zero_keysEx: ‹p ≠ 0 ⟹ ∃a. a ∈ keys (mapping_of p)› for p :: ‹int mpoly›
     using mapping_of_inject by (fastforce simp add: ex_in_conv)
  have ‹finite I› ‹keys (mapping_of p) ⊆ I›
    unfolding I_def by auto
  then show
    ‹vars (p * (monom (monomial (Suc 0) x') 1)) = (if p = 0 then {} else insert x' (vars p))›
    apply (subst pv, subst I_def[symmetric], subst mult_monom)
    apply (auto simp: mult_monom sums I_def)
    using Poly_Mapping.keys_add vars_def apply fastforce
     apply (auto dest!: non_zero_keysEx)
     apply (rule_tac x= ‹a + monomial (Suc 0) x'› in bexI)
      apply (auto simp: coeff_keys)
     apply (simp add: in_keys_iff lookup_add)
    apply (auto simp: vars_def)
    apply (rule_tac x= ‹xa + monomial (Suc 0) x'› in bexI)
     apply (auto simp: coeff_keys)
    apply (simp add: in_keys_iff lookup_add)
    done
qed


  term ‹(x', u, lookup u x', A)›
lemma in_mapping_mult_single:
  ‹x ∈ (λx. lookup x x') ` keys (A * (Var⇩0 x' :: (nat ⇒⇩0 nat) ⇒⇩0 'b :: {monoid_mult,zero_neq_one,semiring_0})) ⟷
  x > 0 ∧ x - 1 ∈ (λx. lookup x x') ` keys (A)›
  apply (standard+; clarify)
  subgoal
    apply (auto  elim!: in_keys_timesE simp: lookup_add)
    apply (auto simp: keys_def lookup_times_monomial_right Var⇩0_def lookup_single image_iff)
    done
  subgoal
    apply (auto  elim!: in_keys_timesE simp: lookup_add)
    apply (auto simp: keys_def lookup_times_monomial_right Var⇩0_def lookup_single image_iff)
    done
  subgoal for  xa
    apply (auto  elim!: in_keys_timesE simp: lookup_add)
    apply (auto simp: keys_def lookup_times_monomial_right Var⇩0_def lookup_single image_iff lookup_add
      intro!: exI[of _ ‹xa + Poly_Mapping.single x' 1›])
    done
  done

lemma Max_Suc_Suc_Max:
  ‹finite A ⟹ A ≠ {} ⟹ Max (insert 0 (Suc ` A)) =
    Suc (Max (insert 0 A))›
  by (induction rule: finite_induct)
   (auto simp: hom_Max_commute)

lemma [simp]:
  ‹keys (Var⇩0 x' :: ('a ⇒⇩0 nat) ⇒⇩0 'b :: {zero_neq_one}) = {Poly_Mapping.single x' 1}›
  by (auto simp: Var⇩0_def)


lemma degree_mult_Var:
  ‹degree (A * Var x') x' = (if A = 0 then 0 else Suc (degree A x'))› for A :: ‹int mpoly›
proof -
  have [simp]: ‹A ≠ 0 ⟹
    Max (insert 0 ((λx. Suc (lookup x x')) ` keys (mapping_of A))) =
    Max (insert (Suc 0) ((λx. Suc (lookup x x')) ` keys (mapping_of A)))›
    unfolding image_image[of Suc ‹λx. lookup x x'›, symmetric] image_insert[symmetric]
    by (subst Max_Suc_Suc_Max, use mapping_of_inject in fastforce, use mapping_of_inject in fastforce)+
      (simp add: Max.hom_commute)
  have ‹A ≠ 0 ⟹
    Max (insert 0
    ((λx. lookup x x') `
    keys (mapping_of A * mapping_of (Var x')))) =
    Suc (Max (insert 0 ((λm. lookup m x') ` keys (mapping_of A))))›
    by (subst arg_cong[of _ ‹insert 0
      (Suc ` ((λx. lookup x x') ` keys (mapping_of A)))› Max])
     (auto simp: image_image Var.rep_eq lookup_plus_fun in_mapping_mult_single
      hom_Max_commute Max_Suc_Suc_Max
      elim!: in_keys_timesE  split: if_splits)
  then show ?thesis
    by (auto simp: degree_def times_mpoly.rep_eq
      intro!: arg_cong[of _ ‹insert 0
      (Suc ` ((λx. lookup x x') ` keys (mapping_of A)))› Max])
qed

lemma degree_mult_Var':
  ‹degree (Var x' * A) x' = (if A = 0 then 0 else Suc (degree A x'))› for A :: ‹int mpoly›
 by (simp add: degree_mult_Var semiring_normalization_rules(7))

lemma degree_times_le:
  ‹degree (A * B) x ≤ degree A x + degree B x›
  by (auto simp: degree_def times_mpoly.rep_eq
       max_def lookup_add add_mono
    dest!: set_rev_mp[OF _ Poly_Mapping.keys_add]
    elim!: in_keys_timesE)

lemma monomial_inj:
  "monomial c s = monomial (d::'b::zero_neq_one) t ⟷ (c = 0 ∧ d = 0) ∨ (c = d ∧ s = t)"
  by (fastforce simp add: monomial_inj Poly_Mapping.single_def
    poly_mapping.Abs_poly_mapping_inject when_def fun_eq_iff
    cong: if_cong
    split: if_splits)

lemma MPoly_monomial_power':
  ‹MPoly (monomial 1 x') ^ (n+1) =  MPoly (monomial (1) (((λx. x + x') ^^ n) x'))›
  by (induction n)
   (auto simp: times_mpoly.abs_eq mult_single ac_simps)

lemma MPoly_monomial_power:
  ‹n > 0 ⟹ MPoly (monomial 1 x') ^ (n) =  MPoly (monomial (1) (((λx. x + x') ^^ (n - 1)) x'))›
  using MPoly_monomial_power'[of _ ‹n-1›]
  by auto


lemma vars_uminus[simp]:
  ‹vars (-p) = vars p›
  by (auto simp: vars_def uminus_mpoly.rep_eq)

lemma coeff_uminus[simp]:
  ‹MPoly_Type.coeff (-p) x = -MPoly_Type.coeff p x›
  by (auto simp: coeff_def uminus_mpoly.rep_eq)

definition decrease_key::"'a ⇒ ('a ⇒⇩0 'b::{monoid_add, minus,one}) ⇒ ('a ⇒⇩0 'b)" where
  "decrease_key k0 f = Abs_poly_mapping (λk. if k = k0 ∧ lookup f k ≠ 0 then lookup f k - 1 else lookup f k)"

lemma remove_key_lookup:
  "lookup (decrease_key k0 f) k = (if k = k0 ∧ lookup f k ≠ 0 then lookup f k - 1 else lookup f k)"
  unfolding decrease_key_def using finite_subset apply (simp add: )
  apply (subst lookup_Abs_poly_mapping)
  apply (auto intro: finite_subset[of _ ‹{x. lookup f x ≠ 0}›])
  apply (subst lookup_Abs_poly_mapping)
  apply (auto intro: finite_subset[of _ ‹{x. lookup f x ≠ 0}›])
  done

lemma polynomial_split_on_var:
  fixes p :: ‹'a :: {comm_monoid_add,cancel_comm_monoid_add,semiring_0,comm_semiring_1} mpoly›
  obtains q r where
    ‹p = monom (monomial (Suc 0) x') 1 * q + r› and
    ‹x' ∉ vars r›
proof -
  have [simp]: ‹{x ∈ keys (mapping_of p). x' ∈ keys x} ∪
        {x ∈ keys (mapping_of p). x' ∉ keys x} = keys (mapping_of p)›
    by auto
  have
    ‹p = (∑x∈keys (mapping_of p). MPoly_Type.monom x (MPoly_Type.coeff p x))› (is ‹_ = (∑x ∈ ?I. ?f x)›)
    using polynomial_sum_monoms(1)[of p] .
  also have ‹... = (∑x∈ {x ∈ ?I. x' ∈ keys x}. ?f x) + (∑x∈ {x ∈ ?I. x' ∉ keys x}. ?f x)› (is ‹_ = ?pX + ?qX›)
    by (subst comm_monoid_add_class.sum.union_disjoint[symmetric]) auto
  finally have 1: ‹p = ?pX + ?qX› .
  have H: ‹0 < lookup x x' ⟹ (λk. (if x' = k then Suc 0 else 0) +
          (if k = x' ∧ 0 < lookup x k then lookup x k - 1
           else lookup x k)) = lookup x› for x x'
    by auto
  have [simp]: ‹finite {x. 0 < (Suc 0 when x' = x)}› for x' :: nat and x
    by (smt bounded_nat_set_is_finite lessI mem_Collect_eq neq0_conv when_cong when_neq_zero)
  have H: ‹x' ∈ keys x ⟹ monomial (Suc 0) x' + Abs_poly_mapping (λk. if k = x' ∧ 0 < lookup x k then lookup x k - 1 else lookup x k) = x›
    for x and x' :: nat
    apply (simp only: keys_def single.abs_eq)
    apply (subst plus_poly_mapping.abs_eq)
    by (auto simp: eq_onp_def when_def H
        intro!: finite_subset[of ‹{xa. (xa = x' ∧ 0 < lookup x xa ⟶ Suc 0 < lookup x x') ∧
           (xa ≠ x' ⟶ 0 < lookup x xa)}› ‹{xa. 0 < lookup x xa}›])

  have [simp]: ‹x' ∈ keys x ⟹
        MPoly_Type.monom (monomial (Suc 0) x' + decrease_key x' x) n =
        MPoly_Type.monom x n› for x n and x'
    apply (subst mpoly.mapping_of_inject[symmetric], subst poly_mapping.lookup_inject[symmetric])
    unfolding mapping_of_monom lookup_single
    apply (auto intro!: ext simp: decrease_key_def when_def H)
    done
  have pX: ‹?pX = monom (monomial (Suc 0) x') 1 * (∑x∈ {x ∈ ?I. x' ∈ keys x}. MPoly_Type.monom (decrease_key x' x) (MPoly_Type.coeff p x))›
    (is ‹_ = _ * ?pX'›)
    by (subst sum_distrib_left, subst mult_monom)
     (auto intro!: sum.cong)
  have ‹x' ∉ vars ?qX›
    using vars_setsum[of ‹{x. x ∈ keys (mapping_of p) ∧ x' ∉ keys x}› ‹?f›]
    by (auto dest!: vars_monom_subset[unfolded subset_eq Ball_def, rule_format])
  then show ?thesis
    using that[of ?pX' ?qX]
    unfolding pX[symmetric] 1[symmetric]
    by blast
qed


lemma polynomial_split_on_var2:
  fixes p :: ‹int mpoly›
  assumes ‹x' ∉ vars s›
  obtains q r where
    ‹p = (monom (monomial (Suc 0) x') 1 - s) * q + r› and
    ‹x' ∉ vars r›
proof -
  have eq[simp]: ‹monom (monomial (Suc 0) x') 1 = Var x'›
    by (simp add: Var.abs_eq Var⇩0_def monom.abs_eq)
  have ‹∀m ≤ n. ∀P::int mpoly. degree P x' < m ⟶ (∃A B. P = (Var x' - s) * A + B ∧ x' ∉ vars B)› for n
  proof (induction n)
    case 0
    then show ?case by auto
  next
    case (Suc n)
    then have IH: ‹m≤n ⟹ MPoly_Type.degree P x' < m ⟹
              (∃A B. P = (Var x' - s) * A + B ∧ x' ∉ vars B)› for m P
      by fast
    show ?case
    proof (intro allI impI)
     fix m and P :: ‹int mpoly›
     assume ‹m ≤ Suc n› and deg: ‹MPoly_Type.degree P x' < m›
     consider
       ‹m ≤ n› |
       ‹m = Suc n›
       using ‹m ≤ Suc n› by linarith
     then show ‹∃A B. P = (Var x' - s) * A + B ∧ x' ∉ vars B›
     proof cases
       case 1
       then show ‹?thesis›
         using Suc deg by blast
     next
       case [simp]: 2
       obtain A B where
         P: ‹P = Var x' * A + B› and
         ‹x' ∉ vars B›
         using polynomial_split_on_var[of P x'] unfolding eq by blast
       have P': ‹P = (Var x' - s) * A + (s * A + B)›
         by (auto simp: field_simps P)
       have ‹A = 0 ∨ degree (s * A) x' < degree P x'›
         using deg ‹x' ∉ vars B› ‹x' ∉ vars s› degree_times_le[of s A x'] deg
         unfolding P
         by (auto simp: degree_sum_notin degree_mult_Var' degree_mult_Var degree_notin_vars
           split: if_splits)
       then obtain A' B' where
         sA: ‹s*A = (Var x' - s) * A' + B'› and
         ‹x' ∉ vars B'›
         using IH[of ‹m-1› ‹s*A›] deg ‹x' ∉ vars B› that[of 0 0]
         by (cases ‹0 < n›) (auto dest!: vars_in_right_only)
       have ‹P = (Var x' - s) * (A + A') + (B' + B)›
         unfolding P' sA by (auto simp: field_simps)
       moreover have ‹x' ∉ vars (B' + B)›
         using ‹x' ∉ vars B'›  ‹x' ∉ vars B›
         by (meson UnE subset_iff vars_add)
       ultimately show ?thesis
         by fast
     qed
   qed
  qed
  then show ?thesis
    using that unfolding eq
    by blast
qed

lemma finit_whenI[intro]:
  ‹finite  {x. (0 :: nat) < (y x)} ⟹ finite {x. 0 < (y x when x ≠ x')}›
  apply (rule finite_subset)
    defer apply assumption
  apply (auto simp: when_def)
  done

lemma polynomial_split_on_var_diff_sq2:
 fixes p :: ‹int mpoly›
  obtains q r s where
    ‹p = monom (monomial (Suc 0) x') 1 * q + r + s * (monom (monomial (Suc 0) x') 1^2 - monom (monomial (Suc 0) x') 1)› and
    ‹x' ∉ vars r› and
    ‹x' ∉ vars q›
proof -
  let ?v = ‹monom (monomial (Suc 0) x') 1 :: int mpoly›
  have H: ‹n < m ⟹ n > 0 ⟹ ∃q. ?v^n = ?v + q * (?v^2 - ?v)› for n m :: nat
  proof (induction m arbitrary: n)
    case 0
    then show ?case by auto
  next
    case (Suc m n) note IH = this(1-)
    consider
      ‹n < m› |
      ‹m = n› ‹n > 1› |
      ‹n = 1›
      using IH
      by (cases ‹n < m›; cases n) auto
    then show ?case
    proof cases
      case 1
      then show ?thesis using IH by auto
    next
      case 2
      have eq: ‹?v^(n) = ((?v :: int mpoly) ^ (n-2)) * (?v^2-?v) + ?v^(n-1)›
        using 2 by (auto simp: field_simps power_eq_if
          ideal.scale_right_diff_distrib)
      obtain q where
        q: ‹?v^(n-1) = ?v + q * (?v^2 - ?v)›
        using IH(1)[of ‹n-1›] 2
        by auto
      show ?thesis
        using q unfolding eq
        by (auto intro!: exI[of _ ‹?v ^ (n - 2) + q›] simp: distrib_right)
    next
      case 3
      then show ‹?thesis›
        by auto
    qed
  qed
  have H: ‹n>0 ⟹ ∃q. ?v^n = ?v + q * (?v^2-?v)› for n
    using H[of n ‹n+1›]
    by auto
  obtain qr :: ‹nat ⇒ int mpoly› where
     qr: ‹n > 0 ⟹ ?v^n = ?v + qr n * (?v^2-?v)› for n
   using H by metis
  have vn: ‹(if lookup x x' = 0 then 1 else Var x' ^ lookup x x') =
    (if lookup x x' = 0 then 1 else ?v) + (if lookup x x' = 0 then 0 else 1) * qr (lookup x x') * (?v^2-?v)› for x
    by (simp add: qr[symmetric] Var_def Var⇩0_def monom.abs_eq[symmetric] cong: if_cong)

  have q: ‹p = (∑x∈keys (mapping_of p). MPoly_Type.monom x (MPoly_Type.coeff p x))›
    by (rule polynomial_sum_monoms(1)[of p])
  have [simp]:
    ‹lookup x x' = 0 ⟹
    Abs_poly_mapping (λk. lookup x k when k ≠ x') = x› for x
    by (cases x, auto simp: poly_mapping.Abs_poly_mapping_inject)
      (auto intro!: ext simp: when_def)
  have [simp]: ‹finite {x. 0 < (a when x' = x)}› for a :: nat
    by (metis (no_types, lifting) infinite_nat_iff_unbounded less_not_refl lookup_single lookup_single_not_eq mem_Collect_eq)

  have [simp]: ‹((λx. x + monomial (Suc 0) x') ^^ (n))
     (monomial (Suc 0) x') = Abs_poly_mapping (λk. (if k = x' then n+1 else 0))› for n
    by (induction n)
     (auto simp: single_def Abs_poly_mapping_inject plus_poly_mapping.abs_eq eq_onp_def cong:if_cong)
  have [simp]: ‹0 < lookup x x' ⟹
    Abs_poly_mapping (λk. lookup x k when k ≠ x') +
    Abs_poly_mapping (λk. if k = x' then lookup x x' - Suc 0 + 1 else 0) =
    x› for x
    apply (cases x, auto simp: poly_mapping.Abs_poly_mapping_inject plus_poly_mapping.abs_eq eq_onp_def)
    apply (subst plus_poly_mapping.abs_eq)
    apply (auto simp: poly_mapping.Abs_poly_mapping_inject plus_poly_mapping.abs_eq eq_onp_def)
    apply (subst Abs_poly_mapping_inject)
    apply auto
    done
  define f where
    ‹f x = (MPoly_Type.monom (remove_key x' x) (MPoly_Type.coeff p x)) *
      (if lookup x x' = 0 then 1 else Var x' ^ (lookup x x'))› for x
  have f_alt_def: ‹f x = MPoly_Type.monom x (MPoly_Type.coeff p x)› for x
    by (auto simp: f_def monom_def remove_key_def Var_def MPoly_monomial_power Var⇩0_def
      mpoly.MPoly_inject monomial_inj times_mpoly.abs_eq
      times_mpoly.abs_eq mult_single)
  have p: ‹p = (∑x∈keys (mapping_of p).
       MPoly_Type.monom (remove_key x' x) (MPoly_Type.coeff p x) *
       (if lookup x x' = 0 then 1 else ?v)) +
          (∑x∈keys (mapping_of p).
       MPoly_Type.monom (remove_key x' x) (MPoly_Type.coeff p x) *
       (if lookup x x' = 0 then 0
        else 1) * qr (lookup x x')) *
             (?v⇧2 - ?v)›
    (is ‹_ = ?a + ?v2v›)
    apply (subst q)
    unfolding f_alt_def[symmetric, abs_def] f_def vn semiring_class.distrib_left
      comm_semiring_1_class.semiring_normalization_rules(18) semiring_0_class.sum_distrib_right
    by (simp add: semiring_class.distrib_left
      sum.distrib)

  have I: ‹keys (mapping_of p) = {x ∈ keys (mapping_of p). lookup x x' = 0} ∪ {x ∈ keys (mapping_of p). lookup x x' ≠ 0}›
    by auto

  have ‹p = (∑x | x ∈ keys (mapping_of p) ∧ lookup x x' = 0.
       MPoly_Type.monom x (MPoly_Type.coeff p x)) +
    (∑x | x ∈ keys (mapping_of p) ∧ lookup x x' ≠ 0.
       MPoly_Type.monom (remove_key x' x) (MPoly_Type.coeff p x)) *
       (MPoly_Type.monom (monomial (Suc 0) x') 1) +
     (∑x | x ∈ keys (mapping_of p) ∧ lookup x x' ≠ 0.
        MPoly_Type.monom (remove_key x' x) (MPoly_Type.coeff p x) *
        qr (lookup x x')) *
             (?v⇧2 - ?v)›
    (is ‹p = ?A + ?B * _ + ?C * _›)
    unfolding semiring_0_class.sum_distrib_right[of _ _ ‹(MPoly_Type.monom (monomial (Suc 0) x') 1)›]
    apply (subst p)
    apply (subst (2)I)
    apply (subst I)
    apply (subst comm_monoid_add_class.sum.union_disjoint)
    apply auto[3]
    apply (subst comm_monoid_add_class.sum.union_disjoint)
    apply auto[3]
    apply (subst (4) sum.cong[OF refl, of _ _ ‹λx. MPoly_Type.monom (remove_key x' x) (MPoly_Type.coeff p x) *
        qr (lookup x x')›])
    apply (auto; fail)
    apply (subst (3) sum.cong[OF refl, of _ _ ‹λx. 0›])
    apply (auto; fail)
    apply (subst (2) sum.cong[OF refl, of _ _ ‹λx. MPoly_Type.monom (remove_key x' x) (MPoly_Type.coeff p x) *
       (MPoly_Type.monom (monomial (Suc 0) x') 1)›])
    apply (auto; fail)
    apply (subst (1) sum.cong[OF refl, of _ _ ‹λx. MPoly_Type.monom x (MPoly_Type.coeff p x)›])
    by (auto simp: f_def simp flip: f_alt_def)

  moreover have ‹x' ∉ vars ?A›
    using vars_setsum[of ‹{x ∈ keys (mapping_of p). lookup x x' = 0}›
      ‹λx. MPoly_Type.monom x (MPoly_Type.coeff p x)›]
    apply auto
    apply (drule set_rev_mp, assumption)
    apply (auto dest!: lookup_eq_zero_in_keys_contradict)
    by (meson lookup_eq_zero_in_keys_contradict subsetD vars_monom_subset)
  moreover have ‹x' ∉ vars ?B›
    using vars_setsum[of ‹{x ∈ keys (mapping_of p). lookup x x' ≠ 0}›
      ‹λx. MPoly_Type.monom (remove_key x' x) (MPoly_Type.coeff p x)›]
    apply auto
    apply (drule set_rev_mp, assumption)
    apply (auto dest!: lookup_eq_zero_in_keys_contradict)
    apply (drule subsetD[OF vars_monom_subset])
    apply (auto simp: remove_key_keys[symmetric])
    done
  ultimately show ?thesis apply -
    apply (rule that[of ?B ?A ?C])
    apply (auto simp: ac_simps)
    done
qed


lemma polynomial_decomp_alien_var:
  fixes q A b :: ‹int mpoly›
  assumes
    q: ‹q = A * (monom (monomial (Suc 0) x') 1) + b› and
    x: ‹x' ∉ vars q› ‹x' ∉ vars b›
  shows
    ‹A = 0› and
    ‹q = b›
proof -
  let ?A = ‹A * (monom (monomial (Suc 0) x') 1)›
  have ‹?A = q - b›
    using arg_cong[OF q, of ‹λa. a - b›]
    by auto
  moreover have ‹x' ∉ vars (q - b)›
    using x vars_in_right_only
    by fastforce
  ultimately have ‹x' ∉ vars (?A)›
    by simp
  then have ‹?A = 0›
    by (auto simp: vars_mult_monom split: if_splits)
  moreover have ‹?A = 0 ⟹ A = 0›
    by (metis empty_not_insert mult_zero_left vars_mult_monom)
  ultimately show ‹A = 0›
    by blast
  then show ‹q = b›
    using q by auto
qed

lemma polynomial_decomp_alien_var2:
  fixes q A b :: ‹int mpoly›
  assumes
    q: ‹q = A * (monom (monomial (Suc 0) x') 1 + p) + b› and
    x: ‹x' ∉ vars q› ‹x' ∉ vars b› ‹x' ∉ vars p›
  shows
    ‹A = 0› and
    ‹q = b›
proof -
  let ?x = ‹monom (monomial (Suc 0) x') 1›
  have x'[simp]: ‹?x = Var x'›
    by (simp add: Var.abs_eq Var⇩0_def monom.abs_eq)
  have ‹∃n Ax A'. A = ?x * Ax + A' ∧ x' ∉ vars A' ∧ degree Ax x' = n›
    using polynomial_split_on_var[of A x'] by metis
  from wellorder_class.exists_least_iff[THEN iffD1, OF this] obtain Ax A' n where
    A: ‹A = Ax * ?x + A'› and
    ‹x' ∉ vars A'› and
    n: ‹MPoly_Type.degree Ax x' = n› and
    H: ‹⋀m Ax A'. m < n ⟶
                   A ≠ Ax * MPoly_Type.monom (monomial (Suc 0) x') 1 + A' ∨
                   x' ∈ vars A' ∨ MPoly_Type.degree Ax x' ≠ m›
    unfolding wellorder_class.exists_least_iff[of ‹λn. ∃Ax A'. A = Ax * ?x + A' ∧ x' ∉ vars A' ∧
      degree Ax x' = n›]
    by (auto simp: field_simps)

  have ‹q = (A + Ax * p) * monom (monomial (Suc 0) x') 1 + (p * A' + b)›
    unfolding q A by (auto simp: field_simps)
  moreover have ‹x' ∉ vars q› ‹x' ∉ vars (p * A' + b)›
    using x ‹x' ∉ vars A'›
    by (smt UnE add.assoc add.commute calculation subset_iff vars_in_right_only vars_mult)+
  ultimately have ‹A + Ax * p = 0› ‹q = p * A' + b›
    by (rule polynomial_decomp_alien_var)+

  have A': ‹A' = -Ax * ?x - Ax * p›
    using ‹A + Ax * p = 0› unfolding A
    by (metis (no_types, lifting) add_uminus_conv_diff eq_neg_iff_add_eq_0 minus_add_cancel
        mult_minus_left)

  have ‹A = - (Ax * p)›
    using A unfolding A'
    apply auto
    done

  obtain Axx Ax' where
    Ax: ‹Ax = ?x * Axx + Ax'› and
    ‹x' ∉ vars Ax'›
    using polynomial_split_on_var[of Ax x'] by metis

  have ‹A = ?x * (- Axx * p) + (- Ax' * p)›
    unfolding ‹A = - (Ax * p)› Ax
    by (auto simp: field_simps)

  moreover have ‹x' ∉ vars (-Ax' * p)›
    using ‹x' ∉ vars Ax'› by (metis (no_types, hide_lams) UnE add.right_neutral
      add_minus_cancel assms(4) subsetD vars_in_right_only vars_mult)
   moreover have ‹Axx ≠ 0 ⟹ MPoly_Type.degree (- Axx * p) x' < degree Ax x'›
     using degree_times_le[of Axx p x'] x
     by (auto simp: Ax degree_sum_notin ‹x' ∉ vars Ax'› degree_mult_Var'
       degree_notin_vars)
   ultimately have [simp]: ‹Axx = 0›
     using H[of ‹MPoly_Type.degree (- Axx * p) x'› ‹- Axx * p› ‹- Ax' * p›]
     by (auto simp: n)
  then have [simp]: ‹Ax' = Ax›
    using Ax by auto

  show ‹A = 0›
    using A ‹A = - (Ax * p)› ‹x' ∉ vars (- Ax' * p)› ‹x' ∉ vars A'› polynomial_decomp_alien_var(1) by force
  then show ‹q = b›
    using q by auto
qed

lemma vars_unE: ‹x ∈ vars (a * b) ⟹ (x ∈ vars a ⟹ thesis) ⟹ (x ∈ vars b ⟹ thesis) ⟹ thesis›
   using vars_mult[of a b] by auto


lemma in_keys_minusI1:
  assumes "t ∈ keys p" and "t ∉ keys q"
  shows "t ∈ keys (p - q)"
  using assms unfolding in_keys_iff lookup_minus by simp

lemma in_keys_minusI2:
  fixes t :: ‹'a› and q :: ‹'a ⇒⇩0 'b :: {cancel_comm_monoid_add,group_add}›
  assumes "t ∈ keys q" and "t ∉ keys p"
  shows "t ∈ keys (p - q)"
  using assms unfolding in_keys_iff lookup_minus by simp


lemma in_vars_addE:
  ‹x ∈ vars (p + q) ⟹ (x ∈ vars p ⟹ thesis) ⟹ (x ∈ vars q ⟹ thesis) ⟹ thesis›
  by (meson UnE in_mono vars_add)

lemma lookup_monomial_If:
  ‹lookup (monomial v k) = (λk'. if k = k' then v else 0)›
  by (intro ext) (auto simp: lookup_single_not_eq)

lemma vars_mult_Var:
  ‹vars (Var x * p) = (if p = 0 then {} else insert x (vars p))› for p :: ‹int mpoly›
proof -
  have ‹p ≠ 0 ⟹
    ∃xa. (∃k. xa = monomial (Suc 0) x + k) ∧
         lookup (mapping_of p) (xa - monomial (Suc 0) x) ≠ 0 ∧
         0 < lookup xa x›
   by (metis (no_types, hide_lams) One_nat_def ab_semigroup_add_class.add.commute
     add_diff_cancel_right' aux lookup_add lookup_single_eq mapping_of_inject
     neq0_conv one_neq_zero plus_eq_zero_2 zero_mpoly.rep_eq)
  then show ?thesis
    apply (auto simp: vars_def times_mpoly.rep_eq Var.rep_eq
    elim!: in_keys_timesE dest: keys_add')
    apply (auto simp: keys_def lookup_times_monomial_left Var.rep_eq Var⇩0_def adds_def
      lookup_add eq_diff_eq'[symmetric])
    done
qed

lemma keys_mult_monomial:
  ‹keys (monomial (n :: int) k * mapping_of a) = (if n = 0 then {} else ((+) k) ` keys (mapping_of a))›
proof -
  have [simp]: ‹(∑aa. (if k = aa then n else 0) *
               (∑q. lookup (mapping_of a) q when k + xa = aa + q)) =
        (∑aa. (if k = aa then n * (∑q. lookup (mapping_of a) q when k + xa = aa + q) else 0))›
      for xa
    by (smt Sum_any.cong mult_not_zero)
  show ?thesis
    apply (auto simp: vars_def times_mpoly.rep_eq Const.rep_eq times_poly_mapping.rep_eq
      Const⇩0_def elim!: in_keys_timesE split: if_splits)
    apply (auto simp: lookup_monomial_If prod_fun_def
      keys_def times_poly_mapping.rep_eq)
    done
qed

lemma vars_mult_Const:
  ‹vars (Const n * a) = (if n = 0 then {} else vars a)› for a :: ‹int mpoly›
  by (auto simp: vars_def times_mpoly.rep_eq Const.rep_eq keys_mult_monomial
    Const⇩0_def elim!: in_keys_timesE split: if_splits)

lemma coeff_minus: "coeff p m - coeff q m = coeff (p-q) m"
  by (simp add: coeff_def lookup_minus minus_mpoly.rep_eq)

lemma Const_1_eq_1: ‹Const (1 :: int) = (1 :: int mpoly)›
  by (simp add: Const.abs_eq Const⇩0_one one_mpoly.abs_eq)

lemma [simp]:
  ‹vars (1 :: int mpoly) = {}›
  by (auto simp: vars_def one_mpoly.rep_eq Const_1_eq_1)


subsection ‹More Ideals›

lemma
  fixes A :: ‹(('x ⇒⇩0 nat) ⇒⇩0 'a::comm_ring_1) set›
  assumes ‹p ∈ ideal A›
  shows ‹p * q ∈ ideal A›
  by (metis assms ideal.span_scale semiring_normalization_rules(7))


text ‹The following theorem is very close to @{thm ideal.span_insert}, except that it
is more useful if we need to take an element of \<^term>‹More_Modules.ideal (insert a S)›.›
lemma ideal_insert':
  ‹More_Modules.ideal (insert a S) = {y. ∃x k. y = x + k * a ∧ x ∈ More_Modules.ideal S}›
    apply (auto simp: ideal.span_insert
      intro: exI[of _ ‹_ - k * a›])
   apply (rule_tac x = ‹x - k * a› in exI)
   apply auto
   apply (rule_tac x = ‹k› in exI)
   apply auto
   done

lemma ideal_mult_right_in:
  ‹a ∈ ideal A ⟹ a * b ∈ More_Modules.ideal A›
  by (metis ideal.span_scale mult.commute)

lemma ideal_mult_right_in2:
  ‹a ∈ ideal A ⟹ b * a ∈ More_Modules.ideal A›
  by (metis ideal.span_scale)


lemma [simp]: ‹vars (Var x :: 'a :: {zero_neq_one} mpoly) = {x}›
  by (auto simp: vars_def Var.rep_eq  Var⇩0_def)

lemma vars_minus_Var_subset:
  ‹vars (p' - Var x :: 'a :: {ab_group_add,one,zero_neq_one} mpoly) ⊆  𝒱 ⟹ vars p' ⊆ insert x 𝒱›
  using vars_add[of ‹p' - Var x› ‹Var x›]
  by auto

lemma vars_add_Var_subset:
  ‹vars (p' + Var x :: 'a :: {ab_group_add,one,zero_neq_one} mpoly) ⊆  𝒱 ⟹ vars p' ⊆ insert x 𝒱›
  using vars_add[of ‹p' + Var x› ‹-Var x›]
  by auto

lemma coeff_monomila_in_varsD:
  ‹coeff p (monomial (Suc 0) x) ≠ 0 ⟹ x ∈ vars (p :: int mpoly)›
  by (auto simp: coeff_def vars_def keys_def
    intro!: exI[of _ ‹monomial (Suc 0) x›])

lemma coeff_MPoly_monomial[simp]:
  ‹(MPoly_Type.coeff (MPoly (monomial a m)) m) = a›
  by (metis MPoly_Type.coeff_def lookup_single_eq monom.abs_eq monom.rep_eq)

end