Theory Linear_Diophantine_Solver

section ‹Linear Diophantine Equation Solver›

text ‹We verify Griggio's algorithm to eliminate equations or detect unsatisfiability.›

subsection ‹Abstract Algorithm›

theory Linear_Diophantine_Solver
  imports 
    Diophantine_Eqs_and_Ineqs
    "HOL.Map" 
begin
 
lift_definition normalize_dleq :: "'v dleq ⇒ int × 'v dleq" is 
  "λ c. (Gcd (range c), λ x. c x div Gcd (range c))" 
  apply simp
  subgoal by (rule finite_subset, auto)
  done

lemma normalize_dleq_gcd: assumes "normalize_dleq p = (g,q)" 
  and "p ≠ 0" 
shows "g = Gcd (insert (constant_l p) (coeff_l p ` vars_l p))"
  and "g ≥ 1"
  and "normalize_dleq q = (1,q)"     
  using assms
proof (atomize (full), transfer, goal_cases)
  case (1 p g q)
  let ?G = "insert (p None) ((λx. p (Some x)) ` {x. p (Some x) ≠ 0})" 
  let ?g = "Gcd (range p)" 
  have "Gcd ?G = Gcd (insert 0 ?G)" by auto
  also have "insert 0 ?G = insert 0 (range p)" 
  proof - 
    {
      fix y
      assume *: "y ∈ insert 0 (range p)" "y ∉ insert 0 ?G" 
      then obtain z where "y = p z" by auto
      with * have False by (cases z, auto)
    }
    thus ?thesis by auto
  qed
  also have "Gcd … = Gcd (range p)" by auto
  finally have eq: "Gcd ?G = ?g" .
  
  from 1 obtain x where px: "p x ≠ 0" by auto
  then obtain y where "y ∈ range p" "y ≠ 0" by auto
  hence g0: "?g ≠ 0" by auto
  moreover have "?g ≥ 0" by simp
  ultimately have g1: "?g ≥ 1" by linarith

  from 1 have gg: "g = ?g" by auto

  let ?gq = "Gcd (range q)" 
  from 1 have q: "q = (λx. p x div ?g)" by auto
  have dvd: "?g dvd p x" for x by auto
  define gp where "gp = ?g" 
  define gq where "gq = ?gq" 
  note hide = gp_def[symmetric] gq_def[symmetric]
  have "?gq ≥ 0" by simp
  then consider (0) "?gq = 0" | (1) "?gq = 1" | (large) "?gq ≥ 2" by linarith
  hence gq1: "?gq = 1"
  proof cases
    case 0
    hence "range q ⊆ {0}" by simp
    moreover from px dvd[of x] have "q x ≠ 0" unfolding q
      using dvd_div_eq_0_iff by blast
    ultimately show ?thesis by auto
  next
    case large
    hence gq0: "?gq ≠ 0" by linarith
    define prod where "prod = ?gq * ?g" 
    {
      fix y
      have "?gq dvd q y" by simp
      then obtain fq where qy: "q y = ?gq * fq" by blast
      from dvd[of y] obtain fp where py: "p y = ?g * fp" by blast
      have "prod dvd p y" using fun_cong[OF q, of y] py qy gq0 g0 unfolding hide prod_def by auto
    }
    hence "prod dvd Gcd (range p)"
      by (simp add: dvd_Gcd_iff)
    from this[unfolded prod_def] g0 gq0 have "?gq dvd 1" by force
    hence "abs ?gq = 1" by simp
    with large show ?thesis by simp
  qed simp

  show ?case unfolding gg gq1
    by (intro conjI g1 eq[symmetric], auto)
qed
  
  

lemma vars_l_normalize: "normalize_dleq p = (g,q) ⟹ vars_l q = vars_l p" 
proof (transfer, goal_cases)
  case (1 c g q)
  {
    fix x
    assume "c (Some x) ≠ 0" 
    moreover have "Gcd (range c) dvd c (Some x)" by simp
    ultimately have "c (Some x) div Gcd (range c) ≠ 0" by fastforce
  }
  thus ?case using 1 by auto
qed


lemma eval_normalize_dleq: "normalize_dleq p = (g,q) ⟹ eval_l α p = g * eval_l α q" 
proof (subst (1 2) eval_l_mono[of "vars_l p"], goal_cases)
  case 1 show ?case by force
  case 2 thus ?case using vars_l_normalize by auto
  case 3 thus ?case by force
  case 4 thus ?case
  proof (transfer, goal_cases)
    case (1 c g d α)
    show ?case
    proof (cases "range c ⊆ {0}")
      case True
      hence "c x = 0" for x using 1 by auto
      thus ?thesis using 1 by auto
    next
      case False
      let ?g = "Gcd (range c)" 
      from False have gcd: "?g ≠ 0" by auto
      hence mult: "c x div ?g * ?g = c x" for x by simp
      let ?expr = "c None div ?g + (∑x | c (Some x) ≠ 0. c (Some x) div ?g * α x)" 
      have "?g * ?expr = ?expr * ?g" by simp
      also have "… = c None + (∑x | c (Some x) ≠ 0. c (Some x) * α x)" 
        unfolding distrib_right mult sum_distrib_right
        by (simp add: ac_simps mult)
      finally show ?thesis using 1(3) by auto
    qed
  qed  
qed
 
lemma gcd_unsat_detection: assumes "g = Gcd (coeff_l p ` vars_l p)" 
  and "¬ g dvd constant_l p" 
shows "¬ satisfies_dleq α p" 
proof
  assume "satisfies_dleq α p" 
  from this[unfolded satisfies_dleq_def eval_l_def]
  have "(∑x∈vars_l p. coeff_l p x * α x) = - constant_l p" by auto
  hence "(∑x∈vars_l p. coeff_l p x * α x) dvd constant_l p" by auto
  moreover have "g dvd (∑x∈vars_l p. coeff_l p x * α x)" 
    unfolding assms by (rule dvd_sum, simp)
  ultimately show False using assms by auto
qed


lemma substitute_l_in_equation: assumes "α x = eval_l α p" 
  shows "eval_l α (substitute_l x p q) = eval_l α q" 
    "satisfies_dleq α (substitute_l x p q) ⟷ satisfies_dleq α q" 
proof -
  show "eval_l α (substitute_l x p q) = eval_l α q" 
    unfolding eval_substitute_l unfolding assms(1)[symmetric] by auto
  thus "satisfies_dleq α (substitute_l x p q) ⟷ satisfies_dleq α q" 
    unfolding satisfies_dleq_def by auto
qed

type_synonym 'v dleq_sf = "'v × (int,'v)lpoly" 

fun satisfies_dleq_sf:: "(int,'v) assign ⇒ 'v dleq_sf ⇒ bool" where
  "satisfies_dleq_sf α (x,p) = (α x = eval_l α p)"

type_synonym 'v dleq_system = "'v dleq_sf set × 'v dleq set" 

fun satisfies_system :: "(int,'v) assign ⇒ 'v dleq_system ⇒ bool" where
  "satisfies_system α (S,E) = (Ball S (satisfies_dleq_sf α) ∧ Ball E (satisfies_dleq α))" 

fun invariant_system :: "'v dleq_system ⇒ bool" where
  "invariant_system (S,E) = (Ball (fst ` S) (λ x. x ∉ ⋃ (vars_l ` (snd ` S ∪ E)) ∧ (∃! e. (x,e) ∈ S)))"  

definition reorder_for_var where
  "reorder_for_var x p = (if coeff_l p x = 1 then - (p - var_l x) else p + var_l x)" 

lemma reorder_for_var: assumes "abs (coeff_l p x) = 1" 
  shows "satisfies_dleq α p ⟷ satisfies_dleq_sf α (x, reorder_for_var x p)" (is ?prop1)
    "vars_l (reorder_for_var x p) = vars_l p - {x}" (is ?prop2)
proof -
  from assms have "coeff_l p x = 1 ∨ coeff_l p x = -1" by auto
  hence "?prop1 ∧ ?prop2" 
  proof
    assume 1: "coeff_l p x = 1" 
    hence res: "reorder_for_var x p = - (p - var_l x)" unfolding reorder_for_var_def by auto
    have ?prop2 unfolding res vars_l_uminus using 1 by transfer auto
    moreover have ?prop1 unfolding satisfies_dleq_def res satisfies_dleq_sf.simps by auto
    ultimately show ?thesis by auto
  next
    assume m1: "coeff_l p x = -1" 
    hence res: "reorder_for_var x p = p + var_l x" unfolding reorder_for_var_def by auto
    have ?prop2 unfolding res using m1 by transfer auto
    moreover have ?prop1 unfolding satisfies_dleq_def res satisfies_dleq_sf.simps by auto
    ultimately show ?thesis by auto
  qed
  thus ?prop1 ?prop2 by blast+
qed 

lemma reorder_nontriv_var_sat: "∃ a. satisfies_dleq (α(y := a)) (reorder_nontriv_var x p y)" 
proof -
  define X where "X = insert x (vars_l p) - {y}" 
  have X: "finite X" "y ∉ X" "insert x (insert y (vars_l p)) = insert y X" unfolding X_def by auto
  have sum: "sum f (insert x (insert y (vars_l p))) = f y + sum f X" for f :: "_ ⇒ int" 
    unfolding X using X(1-2) by simp 
  show ?thesis
    unfolding satisfies_dleq_def
    apply (subst eval_l_mono[of "insert x (insert y (vars_l p))"])
      apply force
     apply (rule vars_reorder_non_triv)
    apply (unfold sum)
    apply (subst (1) coeff_l_reorder_nontriv_var)
    apply (subst sum.cong[OF refl, of _ _ "λ z. coeff_l (reorder_nontriv_var x p y) z * α z"])
    subgoal using X by auto
    subgoal by simp algebra
    done
qed

lemma reorder_nontriv_var: assumes a: "a = coeff_l p x" "a ≠ 0" 
  and y: "y ∉ vars_l p" 
  and q: "q = reorder_nontriv_var x p y" 
  and e: "e = reorder_for_var x q" 
  and r: "r = substitute_l x e p" 
shows "fun_of_lpoly r = (λ z. fun_of_lpoly p z mod a)(Some x := 0, Some y := a)" 
  "constant_l r = constant_l p mod a"
  "coeff_l r = (λ z. coeff_l p z mod a)(x := 0, y := a)"
proof -
  from a have xv: "x ∈ vars_l p" by (transfer, auto)
  with y have xy: "x ≠ y" by auto
  from q have q: "fun_of_lpoly q = (λz. fun_of_lpoly p z div a)(Some x := 1, Some y := - 1)" 
    unfolding a by transfer
  hence "fun_of_lpoly e = (λz. - (fun_of_lpoly p z div a))(Some x := 0, Some y := 1)" 
    unfolding e reorder_for_var_def using xy
    by (transfer, auto)
  thus main: "fun_of_lpoly r = (λ z. fun_of_lpoly p z mod a)(Some x := 0, Some y := a)" 
    unfolding r using a xy y
    by (transfer, auto simp: minus_mult_div_eq_mod) 
  from main show "constant_l r = constant_l p mod a" by transfer auto
  from main show "coeff_l r = (λ z. coeff_l p z mod a)(x := 0, y := a)" by transfer auto
qed

 
(* we deviate from the original algorithm, since we also substitute in the solved part in the
   griggio_solve rule; moreover we do not enforce that normalization uses a non-trivial gcd g *)
inductive griggio_equiv_step :: "'v dleq_system ⇒ 'v dleq_system ⇒ bool" where
  griggio_solve: "abs (coeff_l p x) = 1 ⟹ e = reorder_for_var x p ⟹ 
    griggio_equiv_step (S,insert p E) (insert (x, e) (map_prod id (substitute_l x e) ` S), substitute_l x e ` E)" 
| griggio_normalize: "normalize_dleq p = (g,q) ⟹ g ≥ 1 ⟹
    griggio_equiv_step (S,insert p E) (S, insert q E)" 
| griggio_trivial: "griggio_equiv_step (S, insert 0 E) (S, E)"

fun vars_system :: "'v dleq_system ⇒ 'v set" where
  "vars_system (S, E) = fst ` S ∪ ⋃ (vars_l ` (snd ` S ∪ E))" 

lemma griggio_equiv_step: assumes "griggio_equiv_step SE TF"
  shows "(satisfies_system α SE ⟷ satisfies_system α TF) ∧
         (invariant_system SE ⟶ invariant_system TF) ∧
         vars_system TF ⊆ vars_system SE" 
  using assms
proof induction
  case *: (griggio_solve p x e S E)
  from *(1) have xp: "x ∈ vars_l p" by transfer auto
  let ?E = "insert p E" 
  let ?T = "insert (x, e) (map_prod id (substitute_l x e) ` S)" 
  let ?F = "substitute_l x e ` E" 
  note reorder = reorder_for_var[OF *(1), folded *(2)]
  from reorder(1)[of α] 
  have "satisfies_system α (S, ?E) = satisfies_system α (insert (x,e) S, E)" 
    unfolding satisfies_system.simps by auto
  also have "… = satisfies_system α (?T, ?F)" 
  proof (cases "α x = eval_l α e")
    case True
    from substitute_l_in_equation[OF this] show ?thesis by auto
  qed auto
  finally have equiv: "satisfies_system α (S, ?E) = satisfies_system α (?T, ?F)" .
  moreover {
    assume inv: "invariant_system (S, ?E)" 
    have "invariant_system (?T, ?F)" 
      unfolding invariant_system.simps
    proof (intro ballI)
      fix y
      assume y: "y ∈ fst ` ?T" 
      from vars_substitute_l[of x e, unfolded reorder]
      have vars_subst: "vars_l (substitute_l x e q) ⊆ vars_l p - {x} ∪ (vars_l q - {x})" for q by auto
      from y have y: "y = x ∨ x ≠ y ∧ y ∈ fst ` S" by force
      thus "y ∉ ⋃ (vars_l ` (snd ` ?T ∪ ?F)) ∧ (∃!f. (y, f) ∈ ?T)" 
      proof
        assume y: "y = x" 
        hence "y ∉ ⋃ (vars_l ` (snd ` ?T ∪ ?F))" using vars_subst reorder(2) by auto
        moreover have "∃!f. (y, f) ∈ ?T" unfolding y 
        proof (intro ex1I[of _ e])
          fix f
          assume xf: "(x, f) ∈ ?T" 
          show "f = e" 
          proof (rule ccontr)
            assume "f ≠ e" 
            with xf have "x ∈ fst ` S" by force
            from inv[unfolded invariant_system.simps, rule_format, OF this]
            have "x ∉ vars_l p" by auto
            with *(1) show False by transfer auto
          qed
        qed force
        ultimately show ?thesis by auto
      next
        assume "x ≠ y ∧ y ∈ fst ` S" 
        hence xy: "x ≠ y" and y: "y ∈ fst ` S" by auto                    
        from inv[unfolded invariant_system.simps, rule_format, OF y]
        have nmem: "y ∉ ⋃ (vars_l ` (snd ` S ∪ insert p E))" and unique: "(∃!f. (y, f) ∈ S)" by auto
        from unique have "∃!f. (y, f) ∈ ?T" using xy by force
        moreover from nmem reorder(2) have "y ∉ vars_l e" by auto
        with nmem vars_substitute_l[of x e]
        have "y ∉ ⋃ (vars_l ` (snd ` ?T ∪ ?F))" by auto
        ultimately show ?thesis by auto
      qed
    qed
  }
  moreover
  have "vars_system (?T, ?F) ⊆ vars_system (S, ?E)"
    using reorder(2) vars_substitute_l[of x e] xp unfolding vars_system.simps 
      by (auto simp: rev_image_eqI) blast
  ultimately show ?case by auto
next
  case *: (griggio_normalize p g q S E)
  from vars_l_normalize[OF *(1)] have vars[simp]: "vars_l q = vars_l p" by auto
  from eval_normalize_dleq[OF *(1)] *(2) 
  have sat[simp]: "satisfies_dleq α p = satisfies_dleq α q" unfolding satisfies_dleq_def by auto
  show ?case by simp
next
  case griggio_trivial
  show ?case by (simp add: satisfies_dleq_def)
qed

inductive griggio_unsat :: "'v dleq ⇒ bool" where
  griggio_gcd_unsat: "¬ Gcd (coeff_l p ` vars_l p) dvd constant_l p ⟹ griggio_unsat p" 
| griggio_constant_unsat: "vars_l p = {} ⟹ p ≠ 0 ⟹ griggio_unsat p" 

lemma griggio_unsat: assumes "griggio_unsat p"
  shows "¬ satisfies_system α (S, insert p E)" 
  using assms
proof induction
  case (griggio_gcd_unsat p)
  from gcd_unsat_detection[OF refl this]
  show ?case by auto
next
  case (griggio_constant_unsat p)
  hence "eval_l α p ≠ 0" for α
    unfolding eval_l_def
  proof (transfer, goal_cases)
    case (1 p α)
    from 1(3) obtain x where "p x ≠ 0" by auto
    with 1 show ?case by (cases x, auto)
  qed
  thus ?case by (auto simp: satisfies_dleq_def)
qed

definition adjust_assign :: "'v dleq_sf list ⇒ ('v ⇒ int) ⇒ ('v ⇒ int)" where
  "adjust_assign S α x = (case map_of S x of Some p ⇒ eval_l α p | None ⇒ α x)" 

definition solution_subst :: "'v dleq_sf list ⇒ ('v ⇒ (int,'v)lpoly)" where
  "solution_subst S x = (case map_of S x of Some p ⇒ p | None ⇒ var_l x)" 

locale griggio_input = fixes
  V :: "'v :: linorder set" and
  E :: "'v dleq set" 
begin

fun invariant_state where 
  "invariant_state (Some (SF,X)) = (invariant_system SF 
     ∧ vars_system SF ⊆ V ∪ X
     ∧ V ∩ X = {}
     ∧ (∀ α. (satisfies_system α SF ⟶ Ball E (satisfies_dleq α))
           ∧ (Ball E (satisfies_dleq α) ⟶ (∃ β. satisfies_system β SF ∧ (∀ x. x ∉ X ⟶ α x = β x)))))" 
| "invariant_state None = (∀ α. ¬ Ball E (satisfies_dleq α))" 

(* The following inference rules do not enforce a normalizing strategy,
   and impose less application conditions than the original algorithm of Griggio. 
   Termination will have to be handled in the implementation. *)
inductive_set griggio_step :: "('v dleq_system × 'v set) option rel" where
  griggio_eq_step: "griggio_equiv_step SF TG ⟹ (Some (SF,X), Some (TG, X)) ∈ griggio_step" 
| griggio_fail_step: "griggio_unsat p ⟹ (Some ((S,insert p F),X), None) ∈ griggio_step" 
| griggio_complex_step: "coeff_l p x ≠ 0 
    ⟹ q = reorder_nontriv_var x p y 
    ⟹ e = reorder_for_var x q
    ⟹ y ∉ V ∪ X
    ⟹ (Some ((S,insert p F),X), 
         Some ((insert (x,e) (map_prod id (substitute_l x e) ` S), substitute_l x e ` insert p F), insert y X)) 
        ∈ griggio_step" 

lemma griggio_step: assumes "(A,B) ∈ griggio_step" 
  and "invariant_state A"
shows "invariant_state B" 
  using assms
proof (induct rule: griggio_step.induct)
  case *: (griggio_eq_step SF TG X)
  from griggio_equiv_step[OF *(1)] *(2)
  show ?case by auto
next
  case *: (griggio_fail_step p S F X)
  from griggio_unsat[OF *(1)]
  have "¬ satisfies_system α (S, insert p F)" for α by auto
  with *(2)[unfolded invariant_state.simps] have "¬ Ball E (satisfies_dleq α)" for α by blast
  then show ?case by auto
next
  case *: (griggio_complex_step p x q y e X S F)
  have sat: "∃a. satisfies_dleq (α(y := a)) q" for α 
    using reorder_nontriv_var_sat[of _ y x p] *(2) by auto
  have "invariant_state (Some ((S, insert p F), X))" by fact
  note inv = this[unfolded invariant_state.simps]
  let ?F = "insert q (insert p F)" 
  let ?Y = "insert y X" 
  let ?T = "insert (x, e) (map_prod id (substitute_l x e) ` S)" 
  let ?G = "substitute_l x e ` insert p F" 
  define SF where "SF = (S,?F)" 
  define TG where "TG = (?T,?G)" 
  define Y where "Y = ?Y" 
  from inv * have y: "y ∉ vars_system (S, insert p F)" by blast
  have inv': "invariant_state (Some ((S, ?F), ?Y))" 
    unfolding invariant_state.simps
  proof (intro allI conjI impI)
    from inv ‹y ∉ V ∪ X›
    show "V ∩ insert y X = {}" by auto
    from *(1) have xp: "x ∈ vars_l p" by transfer auto
    with vars_reorder_non_triv[of x p y, folded *(2)] 
    have vq: "vars_l q ⊆ insert y (vars_l p)" by auto
    from inv have vSF: "vars_system (S, insert p F) ⊆ V ∪ X" by auto
    with vq show "vars_system (S, insert q (insert p F)) ⊆ V ∪ insert y X" by auto
    {
      fix α
      assume "satisfies_system α (S, insert q (insert p F))" 
      hence "satisfies_system α (S, insert p F)" by auto
      with inv show "Ball E (satisfies_dleq α)" by blast
    }
    {
      fix α
      assume "Ball E (satisfies_dleq α)" 
      with inv obtain β where sat2: "satisfies_system β (S, insert p F)"
        and eq: "⋀ z. z ∉ X ⟹ α z = β z" by blast
      from sat[of β] obtain a where sat3: "satisfies_dleq (β(y := a)) q" by auto 
      let ?β = "β(y := a)" 
      show "∃β. satisfies_system β (S, ?F) ∧ (∀z. z ∉ ?Y ⟶ α z = β z)" 
      proof (intro exI[of _ ?β] conjI allI impI)
        show "z ∉ ?Y ⟹ α z = ?β z" for z
          using eq[of z] by auto
        have "satisfies_system ?β (S, ?F) = satisfies_system ?β (S, insert p F)" using sat3 by auto
        also have "… = satisfies_system β (S, insert p F)" 
          unfolding satisfies_system.simps
        proof (intro arg_cong2[of _ _ _ _ conj] ball_cong refl)
          fix r
          assume "r ∈ insert p F" 
          with y have "y ∉ vars_l r" by auto
          thus "satisfies_dleq ?β r = satisfies_dleq β r" 
            unfolding satisfies_dleq_def 
            by (subst eval_l_cong[of _ ?β β], auto)
        next
          fix zr 
          assume "zr ∈ S" 
          then obtain z r where zr: "zr = (z,r)" and "(z,r) ∈ S" by (cases zr, auto)
          hence "insert z (vars_l r) ⊆ V ∪ X" using vSF by force
          with *(4) have "z ≠ y" and "y ∉ vars_l r" by auto
          thus "satisfies_dleq_sf ?β zr = satisfies_dleq_sf β zr" 
            unfolding satisfies_dleq_sf.simps zr
            by (subst eval_l_cong[of _ ?β β], auto)
        qed
        also have … by fact
        finally show "satisfies_system ?β (S, ?F)" .
      qed
    }
    from inv have "invariant_system (S, insert p F)" by auto
    with y vq
    show "invariant_system (S, ?F)" by auto
  qed
  have step: "griggio_equiv_step (S, ?F) (?T, ?G)" 
  proof (intro griggio_equiv_step.intros(1) *(3))
    show "¦coeff_l q x¦ = 1" unfolding *(2) coeff_l_reorder_nontriv_var by simp
  qed
  from griggio_equiv_step[OF this] inv'
  show ?case unfolding SF_def[symmetric] TG_def[symmetric] Y_def[symmetric] by auto
qed

context
  assumes VE: "⋃ (vars_l ` E) ⊆ V"
begin

lemma griggio_steps: assumes "(Some (({},E),{}), SFO) ∈ griggio_step^*" (is "(?I,_) ∈ _")
  shows "invariant_state SFO" 
proof -
  define I where "I = ?I"  
  have inv: "invariant_state I" unfolding I_def using VE by auto
  from assms[folded I_def] 
  show ?thesis 
  proof (induct)
    case base
    then show ?case using inv .
  next
    case step
    then show ?case using griggio_step[OF step(2)] by auto
  qed
qed

lemma griggio_fail: assumes "(Some (({},E),{}), None) ∈ griggio_step^*" 
  shows "∄ α. α ⊨⇩d⇩i⇩o (E, {})" 
proof -
  from griggio_steps[OF assms] show ?thesis by auto
qed

(* preliminary result, does not perform substitutions, relationship of β and α not clear *)
lemma griggio_success: assumes "(Some (({},E),{}), Some ((S,{}),X)) ∈ griggio_step^*" 
    and β: "β = adjust_assign S_list α" "set S_list = S"  
  shows "β ⊨⇩d⇩i⇩o (E, {})"   
proof -
  obtain LV RV where LV: "LV = fst ` S" (* left variables of solution *)
    and RV: "RV = ⋃ (vars_l ` snd ` S)"  (* right variables of solution *)
    by auto
  have id: "satisfies_system β (S, {}) = Ball S (satisfies_dleq_sf β)" for β
    by auto
  have id2: "vars_system (S, {}) = LV ∪ RV" 
    by (auto simp: LV RV)
  have id3: "invariant_system (S, {}) = (LV ∩ RV = {} ∧ (∀x∈LV. ∃!e. (x, e) ∈ S))" 
    by (auto simp: LV RV)
  from griggio_steps[OF assms(1)]
  have "invariant_state (Some ((S, {}), X))" .
  note inv = this[unfolded invariant_state.simps id id2 id3]
  from inv have "Ball S (satisfies_dleq_sf β) ⟹ Ball E (satisfies_dleq β)" 
    by auto
  moreover {
    fix x e
    assume xe: "(x,e) ∈ S" 
    hence x: "x ∈ LV" by (force simp: LV) 
    with inv xe have "∃! e. (x,e) ∈ S" by force
    with xe have "map_of S_list x = Some e" unfolding β(2)[symmetric] 
      by (metis map_of_SomeD weak_map_of_SomeI)
    hence "β x = eval_l α e" unfolding β adjust_assign_def by simp
    also have "… = eval_l β e" 
    proof (rule eval_l_cong)
      fix y
      assume "y ∈ vars_l e" 
      with xe have "y ∈ RV" unfolding RV by force
      with inv have "y ∉ LV" by auto
      thus "α y = β y" unfolding β(2)[symmetric] β(1) adjust_assign_def LV 
        by (force split: option.splits dest: map_of_SomeD)
    qed
    finally have "satisfies_dleq_sf β (x,e)" by auto
  }
  ultimately show ?thesis by force
qed

text ‹In the following lemma we not only show that the equations E are 
  solvable, but also how the solution S can be used to process other constraints.
  Assume ‹P› describes an indexed set of polynomials, and 
  ‹f› is a formula that describes how these polynomials must be
  evaluated, e.g., ‹f i = (i 1 ≤ 0 ∧ i 2 > 5 * i 3)› for some inequalities.

  Then ‹f(P) ∧ E› is equi-satisfiable to ‹f(σ(P))› where ‹σ› is a substitution computed from S,
  and ‹adjust_assign S› is used to translated a solution in one direction.›
theorem griggio_success_translations: 
  fixes P :: "'i ⇒ (int,'v)lpoly" and f :: "('i ⇒ int) ⇒ bool" 
  assumes "(Some (({},E),{}), Some ((S,{}),X)) ∈ griggio_step^*"
    and σ: "σ = solution_subst S_list" 
    and S_list: "set S_list = S" 
  shows 
    (* f-solution with substituted polys can be translated to full solution of f and E *) 
    "f (λ i. eval_l α (substitute_all_l σ (P i))) ⟹
    β = adjust_assign S_list α ⟹ 
    f (λ i. eval_l β (P i)) ∧ β ⊨⇩d⇩i⇩o (E, {})" 
    (* solution of f and E system implies f-solution with substituted polys *) 
    "f (λ i. eval_l α (P i)) ∧ α ⊨⇩d⇩i⇩o (E, {}) ⟹
    (⋀ i. vars_l (P i) ⊆ V) ⟹
    ∃ γ. f (λ i. eval_l γ (substitute_all_l σ (P i)))" 
proof -
  assume sol: "f (λ i. eval_l α (substitute_all_l σ (P i)))" 
    and β: "β = adjust_assign S_list α" 
  from griggio_success[OF assms(1) β S_list]
  have solE: "β ⊨⇩d⇩i⇩o (E, {})" by auto
  show "f (λ i. eval_l β (P i)) ∧ β ⊨⇩d⇩i⇩o (E, {})" 
  proof (intro conjI[OF _ solE])
    {
      fix i
      have "eval_l α (substitute_all_l σ (P i)) = eval_l β (P i)" 
        unfolding eval_substitute_all_l
      proof (rule eval_l_cong)
        fix x
        show "eval_l α (σ x) = β x" unfolding σ β solution_subst_def adjust_assign_def
          by (auto split: option.splits)
      qed
    }
    with sol show "f (λ i. eval_l β (P i))" by auto
  qed
next
  assume f: "f (λi. eval_l α (P i)) ∧ α ⊨⇩d⇩i⇩o (E, {})" 
    and vV: "⋀ i. vars_l (P i) ⊆ V" 
  from griggio_steps[OF assms(1)]
  have "invariant_state (Some ((S, {}), X))" .
  note inv = this[unfolded invariant_state.simps]
  from f inv obtain γ 
    where sat: "satisfies_system γ (S, {})" and ab: "⋀ x. x ∉ X ⟹ α x = γ x" by blast
  from inv sat have E: "Ball E (satisfies_dleq γ)" by auto
  {
    fix i
    have "eval_l α (P i) = eval_l γ (P i)" 
    proof (rule eval_l_cong)
      fix x
      show "x ∈ vars_l (P i) ⟹ α x = γ x" 
        by (rule ab, insert vV[of i] inv, auto)
    qed
  }
  with f have f: "f (λi. eval_l γ (P i))" by auto
  {
    fix i
    have "eval_l (λx. eval_l γ (σ x)) (P i) = eval_l γ (P i)"
    proof (intro eval_l_cong)
      fix x
      note defs = σ solution_subst_def 
      show "eval_l γ (σ x) = γ x" 
      proof (cases "x ∈ fst ` S")
        case False 
        thus ?thesis unfolding defs S_list[symmetric] 
          by (force split: option.splits dest: map_of_SomeD)
      next
        case True
        then obtain e where xe: "(x,e) ∈ S" by force
        have "∃! e. (x,e) ∈ S" using inv True by auto
        with xe have "map_of S_list x = Some e" unfolding S_list[symmetric] 
          by (metis map_of_SomeD weak_map_of_SomeI)
        hence id: "σ x = e" unfolding defs by auto
        show ?thesis unfolding id using xe sat by auto
      qed
    qed
  }
  thus "∃γ. f (λi. eval_l γ (substitute_all_l σ (P i)))" 
    unfolding eval_substitute_all_l
    by (intro exI[of _ γ], insert f, auto)
qed

corollary griggio_success_equivalence: 
  fixes P :: "'i ⇒ (int,'v)lpoly" and f :: "('i ⇒ int) ⇒ bool" 
  assumes "(Some (({},E),{}), Some ((S,{}),X)) ∈ griggio_step^*"
    and σ: "σ = solution_subst S_list" 
    and S_list: "set S_list = S" 
    and vV: "⋀ i. vars_l (P i) ⊆ V" 
  shows 
    "(∃ α. f (λ i. eval_l α (substitute_all_l σ (P i))))
     ⟷ (∃ α. f (λ i. eval_l α (P i)) ∧ Ball E (satisfies_dleq α))"
proof -
  note main = griggio_success_translations[OF assms(1,2) S_list, of f _ P]
  from main(1)[OF _ refl] main(2)[OF _ vV]
  show ?thesis by blast
qed

end (* assuming vars(E) ⊆ V *)
end (* fixing E and V *)


end