Theory Equality_Detection_Impl

subsection ‹Algorithm to Detect all Implicit Equalities in ‹ℚ››

text ‹Use incremental simplex algorithm to recursively detect all
  implied equalities.›

theory Equality_Detection_Impl
  imports 
    Equality_Detection_Theory
    Simplex.Simplex_Incremental
    Deriving.Compare_Instances
begin

lemma indexed_sat_mono: "(S,v) ⊨ics cs ⟹ T ⊆ S ⟹ (T,v) ⊨ics cs" 
  by auto

lemma assert_all_simplex_plain_unsat: assumes "invariant_simplex cs J s"
  and "assert_all_simplex K s = Unsat I" 
shows "¬ (set K ∪ J, v) ⊨ics set cs"
proof -
  from assert_all_simplex_unsat[OF assms]
  show ?thesis unfolding minimal_unsat_core_def by force
qed


lemma check_simplex_plain_unsat: assumes "invariant_simplex cs J s"
  and "check_simplex s = (s',Some I)" 
shows "¬ (J, v) ⊨ics set cs"
proof -
  from check_simplex_unsat[OF assms]
  show ?thesis unfolding minimal_unsat_core_def by force
qed
  

hide_const (open) Congruence.eq

fun le_of_constraint :: "constraint ⇒ rat le_constraint" where
  "le_of_constraint (LEQ p c) = Le_Constraint Leq_Rel p c" 
| "le_of_constraint (LT p c) = Le_Constraint Lt_Rel p c" 
| "le_of_constraint (GEQ p c) = Le_Constraint Leq_Rel (-p) (-c)" 
| "le_of_constraint (GT p c) = Le_Constraint Lt_Rel (-p) (-c)" 
 

fun poly_of_constraint :: "constraint ⇒ linear_poly" where
  "poly_of_constraint (LEQ p c) = p" 
| "poly_of_constraint (LT p c) = p" 
| "poly_of_constraint (GEQ p c) = (-p)" 
| "poly_of_constraint (GT p c) = (-p)" 
 
fun const_of_constraint :: "constraint ⇒ rat" where
  "const_of_constraint (LEQ p c) = c" 
| "const_of_constraint (LT p c) = c" 
| "const_of_constraint (GEQ p c) = (-c)" 
| "const_of_constraint (GT p c) = (-c)" 

fun is_no_equality :: "constraint ⇒ bool" where
  "is_no_equality (EQ p c) = False" 
| "is_no_equality _ = True" 

fun is_equality :: "constraint ⇒ bool" where
  "is_equality (EQ p c) = True" 
| "is_equality _ = False" 

lemma le_of_constraint: "is_no_equality c ⟹ v ⊨c c ⟷ (v ⊨le le_of_constraint c)" 
  by (cases c, auto simp: valuate_uminus)


lemma le_of_constraints: "Ball cs is_no_equality ⟹ v ⊨cs cs ⟷ (∀ c ∈ cs. v ⊨le le_of_constraint c)" 
  using le_of_constraint by auto

fun is_strict :: "constraint ⇒ bool" where
  "is_strict (GT _ _) = True" 
| "is_strict (LT _ _) = True" 
| "is_strict _ = False" 

fun is_nstrict :: "constraint ⇒ bool" where
  "is_nstrict (GEQ _ _) = True" 
| "is_nstrict (LEQ _ _) = True" 
| "is_nstrict _ = False" 

lemma is_equality_iff: "is_equality c = (¬ is_strict c ∧ ¬ is_nstrict c)" 
  by (cases c, auto)

lemma is_nstrict_iff: "is_nstrict c = (¬ is_strict c ∧ ¬ is_equality c)" 
  by (cases c, auto)

fun make_strict :: "constraint ⇒ constraint" where
  "make_strict (GEQ p c) = GT p c"
| "make_strict (LEQ p c) = LT p c"
| "make_strict c = c"

fun make_equality :: "constraint ⇒ constraint" where
  "make_equality (GEQ p c) = EQ p c"
| "make_equality (LEQ p c) = EQ p c"
| "make_equality c = c" 

fun make_ineq :: "constraint ⇒ constraint" where
  "make_ineq (GEQ p c) = GEQ p c"
| "make_ineq (LEQ p c) = LEQ p c"
| "make_ineq (EQ p c) = LEQ p c"

fun make_flipped_ineq :: "constraint ⇒ constraint" where
  "make_flipped_ineq (GEQ p c) = LEQ p c"
| "make_flipped_ineq (LEQ p c) = GEQ p c"
| "make_flipped_ineq (EQ p c) = GEQ p c"

lemma poly_const_repr: assumes "is_nstrict c" 
  shows "le_of_constraint c = Le_Constraint Leq_Rel (poly_of_constraint c) (const_of_constraint c)"
    "le_of_constraint (make_strict c) = Le_Constraint Lt_Rel (poly_of_constraint c) (const_of_constraint c)"
    "le_of_constraint (make_flipped_ineq c) = Le_Constraint Leq_Rel (- poly_of_constraint c) (- const_of_constraint c)"
  using assms by (cases c, auto)+

lemma poly_const_repr_set: assumes "Ball cs is_nstrict" 
  shows "le_of_constraint ` cs = (λ c. Le_Constraint Leq_Rel (poly_of_constraint c) (const_of_constraint c)) ` cs"
    "le_of_constraint ` (make_strict ` cs) = (λ c. Le_Constraint Lt_Rel (poly_of_constraint c) (const_of_constraint c)) ` cs"
  subgoal using assms poly_const_repr(1) by simp
  subgoal using assms poly_const_repr(2) unfolding image_comp o_def by auto
  done


datatype eqd_index = 
  Ineq nat | (* inequality, non-strict *)
  FIneq nat | (* Flipped inequality *)
  SIneq nat | (* strict inequality *)
  TmpSIneq nat (* temporary strict inequality *)

fun num_of_index :: "eqd_index ⇒ nat" where
  "num_of_index (FIneq n) = n" 
| "num_of_index (Ineq n) = n" 
| "num_of_index (SIneq n) = n" 
| "num_of_index (TmpSIneq n) = n" 

derive compare_order eqd_index

fun index_constraint :: "nat × constraint ⇒ eqd_index i_constraint list" where
  "index_constraint (n, c) = (
     if is_nstrict c then [(Ineq n, c), (FIneq n, make_flipped_ineq c), (TmpSIneq n, make_strict c)] else
     if is_strict c then [(SIneq n, c)] else 
     [(Ineq n, make_ineq c), (FIneq n, make_flipped_ineq c)]
        )" 

definition init_constraints :: "constraint list ⇒ eqd_index i_constraint list × nat list × nat list × nat list" where
  "init_constraints cs = (let 
     ics' = zip [0 ..< length cs] cs;
     ics = concat (map index_constraint ics');
     ineqs = map fst (filter (is_nstrict o snd) ics');
     sneqs = map fst (filter (is_strict o snd) ics');
     eqs = map fst (filter (is_equality o snd) ics')
    in (ics, ineqs, sneqs, eqs))"

definition index_of :: "nat list ⇒ nat list ⇒ nat list ⇒ eqd_index list" where
  "index_of ineqs sineqs eqs = map SIneq sineqs @ map Ineq eqs @ map FIneq eqs @ map Ineq ineqs" 

context 
  fixes cs :: "constraint list" 
  and ics :: "eqd_index i_constraint list" 
begin

definition cs_of :: "nat list ⇒ nat list ⇒ nat list ⇒ constraint set" where
  "cs_of ineqs sineqs eqs = Simplex.restrict_to (set (index_of ineqs sineqs eqs)) (set ics)" 

lemma init_constraints: assumes init: "init_constraints cs = (ics, ineqs, sineqs, eqs)" 
  shows "v ⊨cs cs_of ineqs sineqs eqs ⟷ v ⊨cs set cs"
    "distinct_indices ics" 
    "fst ` set ics = set (map SIneq sineqs @ map Ineq eqs @ map FIneq eqs @ map Ineq ineqs @ map FIneq ineqs @ map TmpSIneq ineqs)" (is "_ = ?l")
    "set eqs = {i. i < length cs ∧ is_equality (cs ! i)}" 
    "set ineqs = {i. i < length cs ∧ is_nstrict (cs ! i)}"
    "set sineqs = {i. i < length cs ∧ is_strict (cs ! i)}" 
    "set ics =
       (λi. (Ineq i, make_ineq (cs ! i))) ` set eqs ∪
       (λi. (FIneq i, make_flipped_ineq (cs ! i))) ` set eqs ∪
       ((λi. (Ineq i, cs ! i)) ` set ineqs ∪
       (λi. (FIneq i, make_flipped_ineq (cs ! i))) ` set ineqs ∪
       (λi. (TmpSIneq i, make_strict (cs ! i))) ` set ineqs) ∪
       (λi. (SIneq i, cs ! i)) ` set sineqs" (is "_ = ?Large") 
    "distinct (eqs @ ineqs @ sineqs)" 
    "set (eqs @ ineqs @ sineqs) = {0 ..< length cs}" 
proof -
  let ?R = "Simplex.restrict_to (Ineq ` set ineqs ∪ SIneq ` set sineqs ∪ Ineq ` set eqs ∪ FIneq ` set eqs) (set ics)" 
  let ?n = "length cs" 
  let ?I = "Ineq ` set ineqs ∪ SIneq ` set sineqs ∪ Ineq ` set eqs ∪ FIneq ` set eqs" 
  define ics' where "ics' = zip [0 ..< ?n] cs" 
  from init[unfolded init_constraints_def Let_def, folded ics'_def]
  have ics: "ics = concat (map index_constraint ics')" and
    eqs: "eqs = map fst (filter (is_equality ∘ snd) ics')" and
    ineqs: "ineqs = map fst (filter (is_nstrict ∘ snd) ics')" and
    sineqs: "sineqs = map fst (filter (is_strict ∘ snd) ics')" by auto
  from eqs show eqs': "set eqs = {i. i < ?n ∧ is_equality (cs ! i)}" 
    by (force simp: set_zip ics'_def)
  from ineqs show ineqs': "set ineqs = {i. i < ?n ∧ is_nstrict (cs ! i)}" 
    by (force simp: set_zip ics'_def)
  from sineqs show sineqs': "set sineqs = {i. i < ?n ∧ is_strict (cs ! i)}" 
    by (force simp: set_zip ics'_def)
  show "set (eqs @ ineqs @ sineqs) = {0 ..< ?n}" 
    unfolding set_append eqs' ineqs' sineqs' 
    by (auto simp: is_nstrict_iff)
  show "distinct (eqs @ ineqs @ sineqs)" unfolding distinct_append
    unfolding ineqs eqs sineqs ics'_def
    by (auto intro: distinct_map_filter simp: set_zip is_nstrict_iff)
      (simp add: is_equality_iff)
  from eqs' have eqs'': "i ∈ set eqs ⟹ index_constraint (i, cs ! i) = 
     [(Ineq i, make_ineq (cs ! i)), (FIneq i, make_flipped_ineq (cs ! i))]" for i 
    by (cases "cs ! i", auto)
  from ineqs' have ineqs'': "i ∈ set ineqs ⟹ index_constraint (i, cs ! i) = 
     [(Ineq i, cs ! i), (FIneq i, make_flipped_ineq (cs ! i)), (TmpSIneq i, make_strict (cs ! i))]" for i 
    by (cases "cs ! i", auto)
  from sineqs' have sineqs'': "i ∈ set sineqs ⟹ index_constraint (i, cs ! i) = 
     [(SIneq i, cs ! i)]" for i 
    by (cases "cs ! i", auto)
  let ?IC = "λ I. ⋃ (set ` index_constraint ` (λi. (i, cs ! i)) ` I)" 
  have "set ics' = (λ i. (i, cs ! i)) ` {i. i < ?n}" unfolding ics'_def
    by (force simp: set_zip)
  also have "{i. i < ?n} = set eqs ∪ set ineqs ∪ set sineqs" 
    unfolding ineqs' eqs' sineqs' 
    by (auto simp: is_equality_iff)
  finally have "set ics = ?IC (set eqs ∪ set ineqs ∪ set sineqs)" unfolding ics set_concat set_map
    by auto
  also have "… = ?IC (set eqs) ∪ ?IC (set ineqs) ∪ ?IC (set sineqs)" by auto
  also have "?IC (set eqs) = (λ i. (Ineq i, make_ineq (cs ! i))) ` set eqs
      ∪ (λ i. (FIneq i, make_flipped_ineq (cs ! i))) ` set eqs" 
    using eqs'' by auto
  also have "?IC (set ineqs) = (λ i. (Ineq i,  cs ! i)) ` set ineqs
      ∪ (λ i. (FIneq i, make_flipped_ineq (cs ! i))) ` set ineqs
      ∪ (λ i. (TmpSIneq i, make_strict (cs ! i))) ` set ineqs" 
    using ineqs'' by auto
  also have "?IC (set sineqs) = (λ i. (SIneq i,  cs ! i)) ` set sineqs" 
    using sineqs'' by auto
  finally show icsL: "set ics = ?Large" by auto
  show "fst ` set ics = ?l" unfolding icsL set_map set_append image_Un image_comp o_def fst_conv
    by auto
  have "distinct (map fst ics')" unfolding ics'_def by auto
  thus dist: "distinct_indices ics" unfolding ics
  proof (induct ics')
    case (Cons ic ics)
    obtain i c where ic: "ic = (i,c)" by force
    {
      fix j
      assume j: "j ∈ fst ` set (index_constraint (i, c))" 
        "j ∈ fst ` (⋃a∈set ics. set (index_constraint a))" 
      from j(1) have ji: "num_of_index j = i" by (cases c, auto)
      from j(2) obtain i' c' where ic': "(i',c') ∈ set ics" and "j ∈ fst ` set (index_constraint (i',c'))" by force
      from this(2) have ji': "num_of_index j = i'" by (cases c', auto)
      with ji have "i = i'" by auto
      with ic' ic Cons(2) have False by force
    } note tedious = this
    show ?case unfolding ic distinct_indices_def
      apply (simp del: index_constraint.simps, intro conjI)
      subgoal by (cases c, auto)
      subgoal using Cons by (auto simp: distinct_indices_def)
      subgoal using tedious by blast
      done
  qed (simp add: distinct_indices_def)

  show "v ⊨cs cs_of ineqs sineqs eqs ⟷ v ⊨cs set cs" 
  proof
    assume v: "v ⊨cs cs_of ineqs sineqs eqs" 
    {
      fix c
      assume "c ∈ set cs"
      then obtain i where c: "c = cs ! i" and i: "i < ?n" unfolding set_conv_nth by auto
      hence ic: "(i,c) ∈ set ics'" unfolding ics'_def set_zip by force
      hence ics: "set (index_constraint (i,c)) ⊆ set ics" unfolding ics by force
      consider (e) "is_equality c" | (s) "is_strict c" | (n) "is_nstrict c" by (cases c, auto)
      hence "v ⊨c c" 
      proof cases
        case e
        hence eqs: "i ∈ set eqs" unfolding eqs using ic by force
        from e have "{(FIneq i, make_flipped_ineq c), (Ineq i, make_ineq c)} ⊆ set (index_constraint (i,c))" by (cases c, auto)
        moreover with ics have "{(FIneq i, make_flipped_ineq c), (Ineq i, make_ineq c)} ⊆ set ics" by auto
        ultimately have "{make_flipped_ineq c, make_ineq c} ⊆ cs_of ineqs sineqs eqs" unfolding cs_of_def using eqs 
          unfolding index_of_def using e by (cases c, force+)
        with v have "v ⊨c make_flipped_ineq c" "v ⊨c make_ineq c" by auto
        with e show ?thesis by (cases c, auto)
      next
        case s
        hence sineqs: "i ∈ set sineqs" unfolding sineqs using ic by force
        from s have "(SIneq i, c) ∈ set (index_constraint (i,c))" by (cases c, auto)
        moreover with ics have "(SIneq i, c) ∈ set ics" by auto
        ultimately have "c ∈ cs_of ineqs sineqs eqs" unfolding cs_of_def using sineqs
          unfolding index_of_def using s by (cases c, force+)
        with v show "v ⊨c c" by auto
      next
        case n
        hence ineq: "i ∈ set ineqs" unfolding ineqs using ic by force
        from n have "(Ineq i, c) ∈ set (index_constraint (i,c))" by (cases c, auto)
        moreover with ics have "(Ineq i, c) ∈ set ics" by auto
        ultimately have "c ∈ cs_of ineqs sineqs eqs" unfolding cs_of_def using ineq
          unfolding index_of_def using n by (cases c, force+)
        with v show "v ⊨c c" by auto
      qed
    }
    thus "v ⊨cs set cs" by auto
  next
    assume v: "v ⊨cs set cs" 
    {
      fix c
      assume "c ∈ cs_of ineqs sineqs eqs"
      hence "c ∈ ?R" unfolding cs_of_def index_of_def by auto
      then obtain i where i: "i ∈ ?I" and ic: "(i,c) ∈ set ics" by force
      from ic[unfolded ics] obtain kd where ic: "(i,c) ∈ set (index_constraint kd)" and mem: "kd ∈ set ics'" by auto
      from mem[unfolded ics'_def] obtain k d where kd: "kd = (k,d)" and d: "d ∈ set cs" and k: "k < ?n" "d = cs ! k" 
        unfolding set_conv_nth by force
      from v d have vd: "v ⊨c d" by auto
      consider (s) j where "i = SIneq j" "j ∈ set sineqs" | (e) j where "i = Ineq j ∨ i = FIneq j" "j ∈ set eqs" | (n) j where "i = Ineq j" "j ∈ set ineqs" 
        using i by auto
      then have "v ⊨c c" 
      proof cases
        case n
        from ic[unfolded n kd] have j: "j = k" by (cases d, auto)
        from n(2)[unfolded ineqs j] obtain eq where keq: "(k,eq) ∈ set ics'" and nstr: "is_nstrict eq" by force
        from keq[unfolded ics'_def] k have "eq = d" unfolding set_conv_nth by force
        with nstr have "is_nstrict d" by auto
        with ic[unfolded n kd] have "c = d" by (cases d, auto)
        then show ?thesis using vd by auto
      next
        case e
        from ic e kd have j: "j = k" by (cases d, auto)
        from e(2)[unfolded eqs j] obtain eq where keq: "(k,eq) ∈ set ics'" and iseq: "is_equality eq" by force
        from keq[unfolded ics'_def] k have "eq = d" unfolding set_conv_nth by force
        with iseq have eq: "is_equality d" by auto
        with ic e kd have "c = make_ineq d ∨ c = make_flipped_ineq d" by (cases d, auto)
        then show ?thesis using vd eq by (cases d, auto)
      next
        case s
        from ic[unfolded s kd] have j: "j = k" by (cases d, auto)
        from s(2)[unfolded sineqs j] obtain eq where keq: "(k,eq) ∈ set ics'" and str: "is_strict eq" by force
        from keq[unfolded ics'_def] k have "eq = d" unfolding set_conv_nth by force
        with str have "is_strict d" by auto
        with ic[unfolded s kd] have "c = d" by (cases d, auto)
        then show ?thesis using vd by auto
      qed
    }
    thus "v ⊨cs cs_of ineqs sineqs eqs" by auto
  qed
qed

definition init_eq_finder_rat :: "(eqd_index simplex_state × nat list × nat list × nat list) option" where
  "init_eq_finder_rat = (case init_constraints cs of (ics, ineqs, sineqs, eqs)
      ⇒ let s0 = init_simplex ics
       in (case assert_all_simplex (index_of ineqs sineqs eqs) s0
         of Unsat _ ⇒ None
          | Inr s1 ⇒ (case check_simplex s1
         of (_, Some _) ⇒ None
          | (s2, None) ⇒ Some (s2, ineqs, sineqs, eqs))))" 


partial_function (tailrec) eq_finder_main_rat :: "eqd_index simplex_state ⇒ nat list ⇒ nat list ⇒ nat list × nat list × (var ⇒ rat)" where
  [code]: "eq_finder_main_rat s ineq eq = (if ineq = [] then (ineq, eq, solution_simplex s) else let
      cp = checkpoint_simplex s;
      res_strict = (case assert_all_simplex (map TmpSIneq ineq) s  ― ‹Make all inequalities strict and test sat›
          of Unsat C ⇒ Inl (s, C)
           | Inr s1 ⇒ (case check_simplex s1 of
              (s2, None) ⇒ Inr (solution_simplex s2)
            | (s2, Some C) ⇒ Inl (backtrack_simplex cp s2, C)))
     in case res_strict of 
       Inr sol ⇒ (ineq, eq, sol)   ― ‹if indeed all equalities are strictly sat, then no further equality is implied›
     | Inl (s2, C) ⇒ let
         eq' = remdups [i. TmpSIneq i <- C]; ― ‹collect all indices of the strict inequalities within the minimal unsat-core›
              ― ‹the remdups might not be necessary, however the simplex interfact does not ensure distinctness of C›
         s3 = sum.projr (assert_all_simplex (map FIneq eq') s2); ― ‹and permantly add the flipped inequalities›
         s4 = fst (check_simplex s3); ― ‹this check will succeed, no unsat can be reported here›
         ineq' = filter (λ i. i ∉ set eq') ineq ― ‹add eq' from inequalities to equalities and continue›
       in eq_finder_main_rat s4 ineq' (eq' @ eq))" 

definition eq_finder_rat :: "(nat list × (var ⇒ rat)) option" where
  "eq_finder_rat = (case init_eq_finder_rat of None ⇒ None
    | Some (s, ineqs, sineqs, eqs) ⇒ Some (
      case eq_finder_main_rat s ineqs eqs of (ineq, eq, sol)
      ⇒ (eq, sol)))" 
 
context
  fixes eqs ineqs sineqs:: "nat list" 
  assumes init_cs: "init_constraints cs = (ics, ineqs, sineqs, eqs)" 
begin

definition equiv_to_cs where 
  "equiv_to_cs eq = (∀v. v ⊨cs set cs = (set (index_of ineqs sineqs eq), v) ⊨ics set ics)"

definition "strict_ineq_sat ineq eq v = ((set (index_of ineqs sineqs eq) ∪ TmpSIneq ` set ineq, v) ⊨ics set ics)"

lemma init_eq_finder_rat: "init_eq_finder_rat = None ⟹ ∄ v. v ⊨cs set cs" 
  "init_eq_finder_rat = Some (s, ineq, sineq, eq) ⟹ 
      checked_simplex ics (set (index_of ineqs sineqs eq)) s 
    ∧ eq = eqs ∧ ineq = ineqs ∧ sineq = sineqs
    ∧ equiv_to_cs eq
    ∧ distinct (ineq @ sineq @ eq)
    ∧ set (ineq @ sineq @ eq) = {0 ..< length cs}" 
proof (atomize(full), goal_cases)
  case 1
  define s0 where "s0 = init_simplex ics" 
  define I where "I = index_of ineqs sineqs eqs" 
  note init = init_eq_finder_rat_def[unfolded init_cs split Let_def, folded s0_def I_def]
  note init_cs = init_constraints[OF init_cs, unfolded cs_of_def, folded I_def]
  from init_simplex[of ics, folded s0_def]
  have s0: "invariant_simplex ics {} s0" by (rule checked_invariant_simplex)
  show ?case
  proof (cases "assert_all_simplex I s0")
    case Inl (* unsat *)
    from assert_all_simplex_plain_unsat[OF s0 Inl]
    have "∄ v. (set I,v) ⊨ics set ics" by auto
    hence "∄ v. v ⊨cs set cs" using init_cs(1) by auto
    with Inl init show ?thesis by auto
  next
    case (Inr s1)
    obtain s2 res where ch: "check_simplex s1 = (s2, res)" by force
    note init = init[unfolded Inr ch split sum.simps]
    from assert_all_simplex_ok[OF s0 Inr]
    have s1: "invariant_simplex ics (set I) s1" by auto
    show ?thesis
    proof (cases res)
      case Some
      note ch = ch[unfolded Some]
      from check_simplex_plain_unsat[OF s1 ch] init_cs(1)
        Some ch init 
      show ?thesis by auto
    next
      case None
      note ch = ch[unfolded None]
      note init = init[unfolded None option.simps]
      from check_simplex_ok[OF s1 ch]
      have s2: "checked_simplex ics (set I) s2" .
      from init s2 init_cs(1,8,9) show ?thesis unfolding I_def equiv_to_cs_def by fastforce
    qed
  qed
qed

lemma eq_finder_main_rat: fixes Ineq Eq 
  assumes "checked_simplex ics (set (index_of ineqs sineqs eq)) s" 
  and "set ineq ⊆ set ineqs" 
  and "set eqs ⊆ set eq ∧ set eq ∪ set ineq = set eqs ∪ set ineqs" 
  and "eq_finder_main_rat s ineq eq = (Ineq, Eq, v_sol)" 
  and "equiv_to_cs eq" 
  and "distinct (ineq @ eq)" 
shows "set Ineq ⊆ set ineqs" "set eqs ⊆ set Eq" "set Ineq ∪ set Eq = set eqs ∪ set ineqs"  
  and "equiv_to_cs Eq" (* equivalence to original system *)
  and "strict_ineq_sat Ineq Eq v_sol" (* v_sol is a solution where all non-strict inequalities are satisfied strictly *)
  and "distinct (Ineq @ Eq)" 
proof (atomize(full), goal_cases)
  case 1
  show ?case using assms
  proof (induction ineq arbitrary: s eq rule: length_induct)
    case (1 ineq s eq)
    define I where "I = set (index_of ineqs sineqs eq)" 
    note s = "1.prems"(1)[folded I_def]
    note ineq = "1.prems"(2)
    note eq = "1.prems"(3)
    note res = "1.prems"(4)[unfolded eq_finder_main_rat.simps[of _ ineq]]
    note equiv = "1.prems"(5)
    note dist = "1.prems"(6)
    note IH = "1.IH"[rule_format]
    from s have inv: "invariant_simplex ics I s" by (rule checked_invariant_simplex)
    note sol = solution_simplex[OF s refl]
    show ?case
    proof (cases "ineq = []")
      case True
      with res have "Ineq = []" "Eq = eq" "v_sol = solution_simplex s" by auto
      with True have "strict_ineq_sat Ineq Eq v_sol = ((I, solution_simplex s) ⊨ics set ics)" 
        unfolding strict_ineq_sat_def by (auto simp: I_def)
      with sol have "strict_ineq_sat Ineq Eq v_sol" by auto
      with True res eq ineq equiv sol dist show ?thesis by (auto simp: equiv_to_cs_def strict_ineq_sat_def)
    next
      case False
      hence False: "(ineq = []) = False" by auto
      define cp where "cp = checkpoint_simplex s" 
      let ?J = "I ∪ TmpSIneq ` set ineq" 
      let ?ass = "assert_all_simplex (map TmpSIneq ineq) s" 
      define inner where "inner = (case assert_all_simplex (map TmpSIneq ineq) s of Inl I ⇒ Inl (s, I)
        | Inr s1 ⇒ (case check_simplex s1 of (s2, None) ⇒ Inr (solution_simplex s2) | (s2, Some I) ⇒ Inl (backtrack_simplex cp s2, I)))" 
      note res = res[unfolded False if_False, folded cp_def, unfolded Let_def, folded inner_def]
      {
        fix s2 C
        assume "inner = Inl (s2, C)" 
        note inner = this[unfolded inner_def sum.simps] 
        have "set C ⊆ ?J ∧ minimal_unsat_core (set C) ics ∧ invariant_simplex ics I s2"
        proof (cases ?ass)
          case unsat: (Inl D)
          with inner have "D = C" "s2 = s" by auto
          with assert_all_simplex_unsat[OF inv unsat] inv show ?thesis by auto
        next
          case ass: (Inr s1)
          note inner = inner[unfolded ass sum.simps]
          from inner obtain s3 where check: "check_simplex s1 = (s3, Some C)" 
            and s2: "s2 = backtrack_simplex cp s3" 
            by (cases "check_simplex s1", auto split: option.splits)
          note s1 = assert_all_simplex_ok[OF inv ass]
          from check_simplex_unsat[OF s1 check]
          have s3: "weak_invariant_simplex ics ?J s3" and C: "set C ⊆ ?J" "minimal_unsat_core (set C) ics" by auto
          from backtrack_simplex[OF s cp_def[symmetric] s3 s2[symmetric]]
          have s2: "invariant_simplex ics I s2" by auto
          from s2 C show ?thesis by auto
        qed
      } note inner_Some = this

      show ?thesis
      proof (cases inner)
        case (Inr sol)
        note inner = this[unfolded inner_def] 
        from inner obtain s1 where ass: "?ass = Inr s1" by (cases ?ass, auto)
        note inner = inner[unfolded ass sum.simps]
        from inner obtain s2 where check: "check_simplex s1 = (s2, None)" by (cases "check_simplex s1", auto split: option.splits)
        from solution_simplex[OF check_simplex_ok[OF assert_all_simplex_ok[OF inv ass] check]]
        have "(?J, sol) ⊨ics set ics" using inner[unfolded check split option.simps] by auto
        hence str: "strict_ineq_sat ineq eq sol" unfolding I_def strict_ineq_sat_def by auto
        from res[unfolded Inr] have id: "Ineq = ineq" "Eq = eq" "v_sol = sol" by auto
        show ?thesis unfolding id using dist eq ineq equiv str by auto
      next
        case (Inl pair)
        then obtain s2 C where inner: "inner = Inl (s2, C)" by (cases pair, auto)
        from inner_Some[OF this]
        have C: "set C ⊆ I ∪ TmpSIneq ` set ineq" 
          and unsat: "minimal_unsat_core (set C) ics" 
          and s2: "invariant_simplex ics I s2" 
          by auto
        define eq' where "eq' = remdups [i. TmpSIneq i <- C]" 
        have ran: "range TmpSIneq ∩ I = {}" unfolding I_def index_of_def by auto
        {
          assume "eq' = []" 
          hence CI: "set C ⊆ I" using C ran eq'_def by force
          from unsat have "∄ v. (set C, v) ⊨ics set ics" unfolding minimal_unsat_core_def by auto
          with indexed_sat_mono[OF sol CI] have False by auto
        }
        hence eq': "eq' ≠ []" by auto
        let ?eq = "eq' @ eq" 
        define s3 where "s3 = sum.projr (assert_all_simplex (map FIneq eq') s2)" 
        define s4 where "s4 = fst (check_simplex s3)" 
        define ineq' where "ineq' = filter (λi. i ∉ set eq') ineq" 
        have eq'_ineq: "set eq' ⊆ set ineq" using C ran unfolding eq'_def by auto
        have eq_new: "set eqs ⊆ set ?eq ∧ set ?eq ∪ set ineq' = set eqs ∪ set ineqs" using eq'_ineq ineq eq
          by (auto simp: ineq'_def)
        have dist: "distinct (ineq' @ eq' @ eq)" using dist unfolding ineq'_def using eq'_ineq
            unfolding eq'_def by auto
        have ineq_new: "set ineq' ⊆ set ineqs" using ineq unfolding ineq'_def by auto
        from eq' eq'_ineq have len: "length ineq' < length ineq" unfolding ineq'_def
          by (metis empty_filter_conv filter_True length_filter_less subsetD)
        note res = res[unfolded inner sum.simps split, folded eq'_def, folded s3_def, folded ineq'_def s4_def]
        show ?thesis 
        proof (rule IH[OF len _ ineq_new eq_new res _ dist])
          define I' where "I' = index_of ineqs sineqs ?eq" 
          have II': "set I' = set (map FIneq eq') ∪ I" unfolding I'_def I_def index_of_def using ineq eq'_ineq by auto
          show equiv_new: "equiv_to_cs ?eq" 
          proof -
            define c_of where "c_of I = Simplex.restrict_to I (set ics)" for I  
            have "?thesis ⟷ (∀v. (I, v) ⊨ics set ics ⟷ (FIneq ` set eq' ∪ I, v) ⊨ics set ics)" 
              unfolding equiv_to_cs_def using equiv[unfolded equiv_to_cs_def]
              unfolding I'_def[symmetric] I_def[symmetric] II' by auto
            also have "… ⟷ (∀v. v ⊨cs c_of I ⟶ v ⊨cs c_of (FIneq ` set eq'))"
              unfolding c_of_def by auto
            also have "…" 
            proof (intro allI impI)
              fix v
              assume v: "v ⊨cs c_of I" 
              let ?Ineq = "Equality_Detection_Impl.Ineq ` set ineq"  
              let ?SIneq = "Equality_Detection_Impl.TmpSIneq ` set ineq"
              from init_constraints[OF init_cs]
              have dist: "distinct (map fst ics)" unfolding distinct_indices_def by auto
              {
                fix c i
                assume c: "c ∈ c_of {i}" 
                have "c_of {i} = {c}" 
                proof -
                  {
                    fix d
                    assume "d ∈ c_of {i}" 
                    from this[unfolded c_of_def] 
                    have d: "(i, d) ∈ set ics" by force
                    from c[unfolded c_of_def]
                    have c: "(i, c) ∈ set ics" by force
                    from c d dist have "c = d" by (metis eq_key_imp_eq_value)
                  }
                  with c show ?thesis by blast
                qed
              } note c_of_inj = this

              let ?n = "length cs" 
              {
                note init_cs' = init_cs[unfolded init_constraints_def Let_def]
                fix i
                assume "i ∈ set ineq" 
                with ineq have "i ∈ set ineqs" by auto
                with init_cs'
                have "i ∈ set (map fst (filter (is_nstrict ∘ snd) (zip [0..<length cs] cs)))" by auto
                hence i_n: "i < ?n" and nstr: "is_nstrict (cs ! i)" by (auto simp: set_zip)
                hence "(i, cs ! i) ∈ set (zip [0..<?n] cs)" by (force simp: set_zip)
                with init_cs' have "set (index_constraint (i, cs ! i)) ⊆ set ics" by force
                hence 
                  "cs ! i ∈ c_of {Equality_Detection_Impl.Ineq i}" 
                  "make_strict (cs ! i) ∈ c_of {TmpSIneq i}" 
                  "make_flipped_ineq (cs ! i) ∈ c_of {FIneq i}" 
                  using nstr unfolding c_of_def by (cases "cs ! i"; force)+
                with c_of_inj 
                have "c_of {Equality_Detection_Impl.Ineq i} = {cs ! i}" 
                  "c_of {TmpSIneq i} = {make_strict (cs ! i)}" 
                  "c_of {FIneq i} = {make_flipped_ineq (cs ! i)}" 
                  by auto
                note nstr this i_n
              } note c_of_ineq = this

              have cIneq: "c_of ?Ineq = ((!) cs) ` set ineq" using c_of_ineq(2) unfolding c_of_def by blast
              have cSIneq: "c_of ?SIneq = (make_strict o (!) cs) ` set ineq" 
                using c_of_ineq(3) unfolding c_of_def o_def by blast

              have "I ∪ ?Ineq = I" using ineq unfolding I_def index_of_def by auto
              with v have "v ⊨cs (c_of I ∪ c_of ?Ineq)" unfolding c_of_def by auto
              hence v: "v ⊨cs (c_of I ∪ ((!) cs) ` set ineq)" unfolding cIneq by auto 
              have "Ball (snd ` set ics) is_no_equality" 
                using init_cs[unfolded init_constraints_def Let_def] 
                apply clarsimp
                subgoal for i c j d by (cases d, auto)
                done
              hence no_eq_c: "Ball (c_of I) is_no_equality" for I unfolding c_of_def by auto
              have no_eq_ineq: "i ∈ set ineq ⟹ is_no_equality (cs ! i)" for i using c_of_ineq(1)[of i] by (cases "cs ! i", auto)
              define CI where "CI = le_of_constraint ` (c_of I)" 
              from v have v: "∀ c ∈ CI ∪ le_of_constraint ` ((!) cs ` set ineq). (v ⊨le c)"
                unfolding CI_def 
                by (subst (asm) le_of_constraints, insert no_eq_ineq no_eq_c, auto)
              define p where "p = (λ i. poly_of_constraint (cs ! i))" 
              define co where "co = (λ i. const_of_constraint (cs ! i))" 
              have nstri: "Ball ((!) cs ` set ineq) is_nstrict" using c_of_ineq(1) by auto
              have lecs_ineq: "set ine ⊆ set ineq ⟹ le_of_constraint` ((!) cs ` set ine) = (λi. Le_Constraint Leq_Rel (p i) (co i)) ` set ine" for ine
                by (subst poly_const_repr_set, insert nstri, auto simp: p_def co_def)
              from v lecs_ineq[OF subset_refl]
              have v: "∀ c ∈ CI ∪ (λi. Le_Constraint Leq_Rel (p i) (co i)) ` set ineq. (v ⊨le c)" by auto
              have finCI: "finite CI" unfolding CI_def c_of_def by auto
              note main_step = equality_detection_rat[OF finCI finite_set _ _ _ v]
  
              let ?C = "le_of_constraint ` (c_of (set C))" 
              from C have "c_of (set C) ⊆ c_of I ∪ c_of ?SIneq" unfolding c_of_def by auto
              hence "c_of (set C) ⊆ c_of I ∪ (make_strict o (!) cs) ` set ineq" unfolding cSIneq .
              hence "?C ⊆ CI ∪ le_of_constraint ` ((make_strict o (!) cs) ` set ineq)" 
                unfolding CI_def by auto
              also have "le_of_constraint` ((make_strict o (!) cs) ` set ineq) = (λi. Le_Constraint Lt_Rel (p i) (co i)) ` set ineq" 
                unfolding o_def unfolding p_def co_def 
                using poly_const_repr_set(2)[OF nstri, unfolded image_comp o_def] by auto
              finally have "?C ⊆ CI ∪ (λi. Le_Constraint Lt_Rel (p i) (co i)) ` set ineq" by auto

              note main_step = main_step[OF this]

              from unsat[unfolded minimal_unsat_core_def]
              have "∄v. (set C, v) ⊨ics set ics" by auto
              hence "∄v. v ⊨cs c_of (set C)" unfolding c_of_def by auto
              hence "∄v. ∀c∈le_of_constraint ` (c_of (set C)). v ⊨le c" 
                by (subst (asm) le_of_constraints[OF no_eq_c], auto)

              note main_step = main_step[OF this]

              {
                fix D 
                assume "D ⊂ le_of_constraint ` (c_of (set C))" 
                hence "∃ CS. le_of_constraint ` CS = D ∧ CS ⊂ c_of (set C)" 
                  by (metis subset_image_iff subset_not_subset_eq)
                then obtain CS where D: "D = le_of_constraint ` CS" and sub: "CS ⊂ c_of (set C)" by auto
                define c_fun where "c_fun i = (THE x. x ∈ c_of {i})" for i  
                {
                  fix C'
                  assume C': "C' ⊆ set C" 
                  {
                    fix i
                    assume "i ∈ C'" 
                    with C' C have "i ∈ I ∪ TmpSIneq ` set ineq" by auto
                    from this[unfolded I_def index_of_def] ineq eq
                    have "i ∈ set (map SIneq sineqs @ map Equality_Detection_Impl.Ineq eqs @ 
                      map FIneq eqs @ map Equality_Detection_Impl.Ineq ineqs @ map FIneq ineqs @ map TmpSIneq ineqs)" (is "_ ∈ ?S")
                      by auto
                    also have "?S ⊆ fst ` set ics" using init_constraints(3)[OF init_cs] by auto
                    finally have "i ∈ fst ` set ics" by auto
                    then obtain c where "(i,c) ∈ set ics" by force
                    hence "c ∈ c_of {i}" unfolding c_of_def by force
                    from c_of_inj[OF this] have c: "c_of {i} = {c}" by auto
                    hence "c_fun i = c" unfolding c_fun_def by auto
                    with c have "c_of {i} = {c_fun i}" by auto
                  }
                  hence "c_of C' = c_fun ` C'" unfolding c_of_def by blast
                } note to_c_fun = this
                from sub[unfolded to_c_fun[OF subset_refl]]
                have "CS ⊂ c_fun ` set C" by auto
                hence "∃ C'. C' ⊂ set C ∧ CS = c_fun ` C'"
                  by (metis subset_image_iff subset_not_subset_eq)
                then obtain C' where sub: "C' ⊂ set C" and CS: "CS = c_fun ` C'" by auto
                from CS to_c_fun[of C'] sub have CS: "CS = c_of C'" by auto
                from unsat[unfolded minimal_unsat_core_def] dist sub
                have "∃v. (C', v) ⊨ics set ics"
                  unfolding distinct_indices_def by auto
                hence "∃v. v ⊨cs CS" unfolding CS c_of_def by auto
                hence "∃v. ∀c∈D. v ⊨le c" unfolding D
                  by (subst (asm) le_of_constraints, unfold CS, insert no_eq_c, auto)
              } 

              note main_step = main_step[OF this]
                               
              {
                fix i e
                assume ieq': "i ∈ set eq'" and mem: "(FIneq i, e) ∈ set ics" 
                from ieq' eq'_def have tmp: "TmpSIneq i ∈ set C" by auto
                have i: "i ∈ set ineq" using ieq' eq'_ineq by auto
                from c_of_ineq(1,3,5)[OF i] tmp
                have *: "make_strict (cs ! i) ∈ c_of (set C)" "is_nstrict (cs ! i)" "i < ?n" 
                  by (auto simp: c_of_def)
                from *(3) have "(i, cs ! i) ∈ set (zip [0..< ?n] cs)" by (force simp: set_zip set_conv_nth)
                hence "set (index_constraint (i, cs ! i)) ⊆ set ics" using init_cs[unfolded init_constraints_def Let_def]
                  by force
                hence "(FIneq i, make_flipped_ineq (cs ! i)) ∈ set ics" using *(2) by (cases "cs ! i", auto)
                with mem dist have e: "e = make_flipped_ineq (cs ! i)" by (metis eq_key_imp_eq_value)
                have "le_of_constraint (make_strict (cs ! i)) = Le_Constraint Lt_Rel (p i) (co i)"  
                  by (subst poly_const_repr(2), insert *, auto simp: p_def co_def)
                from this * have "Le_Constraint Lt_Rel (p i) (co i) ∈ le_of_constraint ` (c_of (set C))" 
                  by force
                from main_step[OF _ i this] 
                have eq: "(p i) ⦃ v ⦄ = co i" by auto
                have id: "le_of_constraint (make_flipped_ineq (cs ! i)) = Le_Constraint Leq_Rel (- p i) (- co i)" 
                  by (subst poly_const_repr(3), insert *, auto simp: p_def co_def)
                from * have "is_no_equality (make_flipped_ineq (cs ! i))" by (cases "cs ! i", auto)
                from le_of_constraint[OF this, of v]
                have "v ⊨c e" using e id eq by (simp add: valuate_uminus)
              }
              thus "v ⊨cs c_of (FIneq ` set eq')" unfolding c_of_def by auto
            qed
            finally show ?thesis by simp
          qed
          from equiv equiv_new sol 
          have sol: "(set I', solution_simplex s) ⊨ics set ics" unfolding equiv_to_cs_def index_of_def I_def I'_def by auto
          have II': "set I' = set (map FIneq eq') ∪ I" unfolding I'_def I_def index_of_def using eq'_ineq ineq by auto
          let ?ass = "assert_all_simplex (map FIneq eq') s2" 
          {
            fix K
            assume "?ass = Unsat K" 
            from assert_all_simplex_plain_unsat[OF s2 this, folded II'] sol have False by auto
          }
          hence ass: "?ass = Inr s3" unfolding s3_def by (cases ?ass, auto)
          from assert_all_simplex_ok[OF s2 ass]
          have s3: "invariant_simplex ics (set I') s3" unfolding II' by (simp add: ac_simps)
          from s4_def[unfolded ass, simplified] obtain c where 
            "check_simplex s3 = (s4, c)" by (cases "check_simplex s3", auto)
          with check_simplex_plain_unsat[OF s3] sol 
          have "check_simplex s3 = (s4, None)" by (cases c, auto)
          from check_simplex_ok[OF s3 this]
          show "checked_simplex ics (set (index_of ineqs sineqs (eq' @ eq))) s4" unfolding I'_def .
        qed
      qed
    qed
  qed
qed

lemma eq_finder_rat_in_ctxt: "eq_finder_rat = None ⟹ ∄ v. v ⊨cs set cs" 
  "eq_finder_rat = Some (eq_idx, v_sol) ⟹ {i . i < length cs ∧ is_equality (cs ! i)} ⊆ set eq_idx ∧
     set eq_idx ⊆ {0 ..< length cs} ∧
     distinct eq_idx" (is "_ ⟹ ?main1")
  "eq_finder_rat = Some (eq_idx, v_sol) ⟹
     set feq = make_equality ` (!) cs ` set eq_idx ⟹
     set fineq = (!) cs ` ({0 ..< length cs} - set eq_idx) ⟹
     (∀ v. v ⊨cs set cs ⟷ v ⊨cs (set feq ∪ set fineq)) ∧
     Ball (set feq) is_equality ∧ Ball (set fineq) is_no_equality ∧
     (v_sol ⊨cs (set feq ∪ make_strict ` set fineq))" (is "_ ⟹ _ ⟹ _ ⟹ ?main2")
proof -
  assume "eq_finder_rat = None" 
  from this[unfolded eq_finder_rat_def] have "init_eq_finder_rat = None" by (cases init_eq_finder_rat, auto)
  from init_eq_finder_rat(1)[OF this] show "∄ v. v ⊨cs set cs" .
next
  assume "eq_finder_rat = Some (eq_idx, v_sol)" 
  note res = this[unfolded eq_finder_rat_def] 
  then obtain s ineq sineq eq 
    where init: "init_eq_finder_rat = Some (s, ineq, sineq, eq)" 
    by (cases init_eq_finder_rat, auto)
  from init_eq_finder_rat(2)[OF init] have sineq: "sineq = sineqs"
      and dist: "distinct (ineq @ sineq @ eq)" and set: "set (ineq @ sineq @ eq) = {0..<length cs}" by auto
  note res = res[unfolded init option.simps split sineq]
  from res
  obtain fi fe where main: "eq_finder_main_rat s ineq eq = (fi,fe, v_sol)" 
    by (cases "eq_finder_main_rat s ineq eq", auto)
  note res = res[unfolded main split]
  from res have eq_idx: "eq_idx = fe" 
    by auto
  from dist have dist': "distinct (ineq @ eq)" by auto
  from init_eq_finder_rat(2)[OF init]
  have "checked_simplex ics (set (index_of ineqs sineqs eq)) s" and
    **: "set ineq ⊆ set ineqs" "set eqs ⊆ set eq ∧ set eq ∪ set ineq = set eqs ∪ set ineqs" 
    "equiv_to_cs eq" 
    and ***: "{0..<length cs} = set (ineq @ sineq @ eq)" "distinct (ineq @ sineq @ eq)" 
    by auto
  from eq_finder_main_rat[OF this(1,2,3) main this(4) dist']
  have *: "set fi ⊆ set ineqs" "set eqs ⊆ set fe" "set fe ∪ set fi = set eqs ∪ set ineqs"
    and equiv: "equiv_to_cs fe" 
    and sat: "strict_ineq_sat fi fe v_sol"
    and dist'': "distinct (fi @ fe)" by auto

  note init = init_cs[unfolded init_constraints_def Let_def]
  note init' = init_constraints[OF init_cs]
  note eqs = init'(4)

  show ?main1
  proof (intro conjI)
    show "distinct eq_idx" unfolding eq_idx using dist'' by auto
    show "{i . i < length cs ∧ is_equality (cs ! i)} ⊆ set eq_idx" 
      unfolding eq_idx using set * ** eqs by auto
    show "set eq_idx ⊆ {0..<length cs}" unfolding eq_idx using set * ** by auto
  qed

  assume feq: "set feq = make_equality ` (!) cs ` set eq_idx" 
  assume fineq: "set fineq = (!) cs ` ({0 ..< length cs} - set eq_idx)"
  from feq eq_idx 
  have feq: "set feq = set (map (λi. make_equality (cs ! i)) fe)" by auto
  have fineq: "set fineq = set (map ((!) cs) (sineqs @ fi))" 
    unfolding set_map *** using ***(2) unfolding sineq eq_idx fineq
    apply (intro image_cong[OF _ refl])
    unfolding *** sineq using * **(1-2) dist'' by auto
  note ineqs  = init'(5)
  note sineqs = init'(6)
  note ics = init'(7)
  from *(3) have fe: "i ∈ set fe ⟹ is_equality (cs ! i) ∨ is_nstrict (cs ! i)" for i
    unfolding eqs ineqs by auto
  let ?n = "length cs" 
  show ?main2
  proof (intro conjI ballI allI)
    define c_of where "c_of I = Simplex.restrict_to I (set ics)" for I  
    have [simp]: "c_of (I ∪ J) = c_of I ∪ c_of J" for I J unfolding c_of_def by auto
    {
      fix v
      have cs: "v ⊨cs set cs = v ⊨cs c_of (set (index_of ineqs sineqs fe))" (is "_ = ?cond")
        using equiv[unfolded equiv_to_cs_def] unfolding c_of_def by auto
      have "?cond ⟷ v ⊨cs c_of (SIneq ` set sineqs) 
      ∧ (v ⊨cs c_of (Ineq ` set fe)
      ∧ v ⊨cs c_of (FIneq ` set fe))
      ∧ v ⊨cs c_of (Ineq ` set ineqs)" unfolding index_of_def
        by auto
      also have "c_of (SIneq ` set sineqs) = ((!) cs) ` set sineqs" 
        unfolding c_of_def ics
        unfolding sineqs by force
      also have "c_of (Ineq ` set ineqs) = ((!) cs) ` set ineqs" 
        unfolding c_of_def ics
        unfolding ineqs eqs 
        by (auto simp: is_nstrict_iff) force
      also have "c_of (FIneq ` set fe) = (λ i. make_flipped_ineq (cs ! i)) ` set fe" (is "?l = ?r")
      proof 
        show "?l ⊆ ?r" 
          unfolding c_of_def ics using fe *(3)
          unfolding ineqs eqs by auto
        show "?r ⊆ ?l" 
        proof
          fix c
          assume "c ∈ ?r" 
          then obtain i where i: "i ∈ set fe" and c: "c = make_flipped_ineq (cs ! i)" 
            by auto
          from * i have i': "i ∈ set eqs ∪ set ineqs" by auto
          have "(FIneq i, c) ∈ set ics ∩ {FIneq i} × UNIV" 
            unfolding c ics using i' by auto
          hence "c ∈ c_of {FIneq i}" unfolding c_of_def by force
          with i show "c ∈ ?l" unfolding c_of_def by auto
        qed
      qed
      also have "c_of (Ineq ` set fe) = (λ i. make_ineq (cs ! i)) ` set fe" (is "?l = ?r")
      proof 
        {
          fix i
          have "i ∈ set fe ⟹ is_nstrict (cs ! i) ⟹ cs ! i ∈ (λi. make_ineq (cs ! i)) ` set fe" 
            by (cases "cs ! i"; force)
        }
        thus "?l ⊆ ?r" 
          unfolding c_of_def ics using fe *(3)
          unfolding ineqs eqs by auto
        show "?r ⊆ ?l" 
        proof
          fix c
          assume "c ∈ ?r" 
          then obtain i where i: "i ∈ set fe" and c: "c = make_ineq (cs ! i)" 
            by auto
          from * i have i': "i ∈ set eqs ∪ set ineqs" by auto
          from fe[OF i]
          have "(Ineq i, c) ∈ set ics ∩ {Ineq i} × UNIV" 
          proof 
            assume "is_equality (cs ! i)" 
            with i' have "i ∈ set eqs" unfolding ineqs by (cases "cs ! i", auto)
            thus ?thesis 
              unfolding c ics using i' by (cases "cs ! i"; force)
          next
            assume stri: "is_nstrict (cs ! i)" 
            with i' have i': "i ∈ set ineqs" unfolding eqs by (cases "cs ! i", auto)
            from stri have c: "c = cs ! i" unfolding c by (cases "cs ! i", auto)
            thus ?thesis 
              unfolding c ics using i' by (cases "cs ! i"; force)
          qed
          hence "c ∈ c_of {Ineq i}" unfolding c_of_def by force
          with i show "c ∈ ?l" unfolding c_of_def by auto
        qed
      qed
      also have "v ⊨cs ((λi. make_ineq (cs ! i)) ` set fe) ∧
      v ⊨cs ((λi. make_flipped_ineq (cs ! i)) ` set fe)
      ⟷ v ⊨cs ((λ i. make_equality (cs ! i)) ` set fe)" (is "?l = ?r")
      proof -
        have "?l ⟷ (∀ i ∈ set fe. v ⊨c make_ineq (cs ! i) ∧ v ⊨c make_flipped_ineq (cs ! i))" 
          by auto
        also have "… ⟷ (∀ i ∈ set fe. v ⊨c make_equality (cs ! i))" 
          apply (intro ball_cong[OF refl])
          subgoal for i using fe[of i]
            by (cases "cs ! i", auto)
          done
        also have "… ⟷ ?r" by auto
        finally show "?l = ?r" .
      qed
      finally have "?cond ⟷
        v ⊨cs ((!) cs ` (set sineqs ∪ set ineqs) ∪ (λi. make_equality (cs ! i)) ` set fe)" 
        by auto
      also have "… ⟷ v ⊨cs (set feq ∪ set fineq)" (is "?l = ?r")
      proof
        show "?l ⟹ ?r" unfolding feq fineq using * by auto
        assume v: ?r
        show ?l
        proof
          fix c 
          assume c: "c ∈ (!) cs ` (set sineqs ∪ set ineqs) ∪
             (λi. make_equality (cs ! i)) ` set fe" 
          show "v ⊨c c" 
          proof (cases "c ∈ (!) cs ` (set sineqs ∪ set fi) ∪
             (λi. make_equality (cs ! i)) ` set fe") 
            case True
            thus ?thesis using v feq fineq * by auto
          next
            case False
            with c obtain i where "i ∈ set ineqs - set fi" and c: "c = cs ! i" by auto
            with * have i: "i ∈ set fe" by auto
            with v have "v ⊨c make_equality (cs ! i)" 
              using v feq fineq * by auto
            with fe[OF i] show ?thesis unfolding c by (cases "cs ! i", auto)
          qed
        qed
      qed
      finally have main: "?cond ⟷ v ⊨cs (set feq ∪ set fineq)" by auto
      with cs show "v ⊨cs set cs = v ⊨cs (set feq ∪ set fineq)" by auto
      note main
    } note main = this 
    fix c
    {
      assume "c ∈ set feq" 
      from this[unfolded feq] obtain i where i: "i ∈ set fe" 
        and c: "c = make_equality (cs ! i)" by auto
      from i * have "i ∈ set eqs ∪ set ineqs" by auto
      hence "is_equality (cs ! i) ∨ is_nstrict (cs ! i)" 
        unfolding ineqs eqs by auto
      thus "is_equality c" unfolding c
        by (cases "cs ! i", auto)
    }  
    {
      assume "c ∈ set fineq" 
      from this[unfolded fineq] * obtain i where i: "i ∈ set sineqs ∪ set ineqs" 
        and c: "c = cs ! i" by auto
      hence "is_nstrict c ∨ is_strict c" unfolding c sineqs ineqs by auto
      thus "is_no_equality c" by (cases c, auto)
    }
    from sat[unfolded strict_ineq_sat_def] 
    have old: "v_sol ⊨cs c_of (set (index_of ineqs sineqs fe))" and new: "v_sol ⊨cs c_of (TmpSIneq ` set fi)" 
      by (auto simp: c_of_def)
    have tmp: "c_of (TmpSIneq ` set fi) = (λ i. make_strict (cs ! i)) ` set fi" 
      apply (rule sym)
      unfolding c_of_def ics using *(1) unfolding ineqs 
      by force

    fix c
    assume "c ∈ set feq ∪ make_strict ` set fineq"
    thus "v_sol ⊨c c" 
    proof
      assume "c ∈ set feq" 
      thus ?thesis using old[unfolded main] by auto
    next
      assume "c ∈ make_strict ` set fineq" 
      from this[unfolded fineq]
      obtain i where i: "i ∈ set sineqs ∨ i ∈ set fi" 
        and c: "c = make_strict (cs ! i)" by force
      from i show ?thesis 
      proof
        assume "i ∈ set fi" 
        with new[unfolded tmp] c show ?thesis by auto
      next
        assume i: "i ∈ set sineqs" 
        hence v: "v_sol ⊨c (cs ! i)" using old[unfolded main]
          unfolding fineq by auto
        from i[unfolded sineqs] have "make_strict (cs ! i) = cs ! i" 
          by (cases "cs ! i", auto)
        with v show ?thesis unfolding c by auto
      qed
    qed
  qed
qed


end
end


lemma eq_finder_rat: 
  "eq_finder_rat cs = None ⟹ ∄v. v ⊨cs set cs" (is "?p1 ⟹ ?g1")
  "eq_finder_rat cs = Some (eq_idx, v_sol) ⟹ 
    {i . i < length cs ∧ is_equality (cs ! i)} ⊆ set eq_idx ∧
    set eq_idx ⊆ {0 ..< length cs} ∧
    distinct eq_idx" (is "?p2 ⟹ ?g2")
  "eq_finder_rat cs = Some (eq_idx, v_sol) ⟹
   set eq = make_equality ` (!) cs ` set eq_idx ⟹
   set ineq = (!) cs ` ({0 ..< length cs} - set eq_idx) ⟹
    (∀v. v ⊨cs set cs ⟷ v ⊨cs (set eq ∪ set ineq)) ∧
    Ball (set eq) is_equality ∧ Ball (set ineq) is_no_equality ∧
    (v_sol ⊨cs (set eq ∪ make_strict ` set ineq))" 
    (is "?p2 ⟹ ?p3 ⟹ ?p4 ⟹ ?g3")
proof -
  obtain ics ineqs sineqs eqs
    where "init_constraints cs = (ics, ineqs, sineqs, eqs)" 
    by (cases "init_constraints cs")
  from eq_finder_rat_in_ctxt[OF this]
  show "?p1 ⟹ ?g1" "?p2 ⟹ ?g2" "?p2 ⟹ ?p3 ⟹ ?p4 ⟹ ?g3" by auto
qed

hide_fact eq_finder_rat_in_ctxt

end