Theory PAC_Checker

(*
  File:         PAC_Checker.thy
  Author:       Mathias Fleury, Daniela Kaufmann, JKU
  Maintainer:   Mathias Fleury, JKU
*)
theory PAC_Checker
  imports PAC_Polynomials_Operations
    PAC_Checker_Specification
    PAC_Map_Rel
    Show.Show
    Show.Show_Instances
    PAC_Misc
begin

section ‹Executable Checker›

text ‹In this layer we finally refine the checker to executable code.›

subsection ‹Definitions›

text ‹Compared to the previous layer, we add an error message when an error is discovered. We do not
  attempt to prove anything on the error message (neither that there really is an error, nor that the
  error message is correct).
›

paragraph ‹Extended error message›

datatype 'a code_status =
  is_cfailed: CFAILED (the_error: 'a) |
  CSUCCESS |
  is_cfound: CFOUND

text ‹In the following function, we merge errors. We will never merge an error message with an
  another error message; hence we do not attempt to concatenate error messages.
›
fun merge_cstatus where
  ‹merge_cstatus (CFAILED a) _ = CFAILED a› |
  ‹merge_cstatus _ (CFAILED a) = CFAILED a› |
  ‹merge_cstatus CFOUND _ = CFOUND› |
  ‹merge_cstatus _ CFOUND = CFOUND› |
  ‹merge_cstatus _ _ = CSUCCESS›

definition code_status_status_rel :: ‹('a code_status × status) set› where
‹code_status_status_rel =
  {(CFOUND, FOUND), (CSUCCESS, SUCCESS)} ∪
  {(CFAILED a, FAILED)| a. True}›

lemma in_code_status_status_rel_iff[simp]:
  ‹(CFOUND, b) ∈ code_status_status_rel ⟷ b = FOUND›
  ‹(a, FOUND) ∈ code_status_status_rel ⟷ a = CFOUND›
  ‹(CSUCCESS, b) ∈ code_status_status_rel ⟷ b = SUCCESS›
  ‹(a, SUCCESS) ∈ code_status_status_rel ⟷ a = CSUCCESS›
  ‹(a, FAILED) ∈ code_status_status_rel ⟷ is_cfailed a›
  ‹(CFAILED C, b) ∈ code_status_status_rel ⟷ b = FAILED›
  by (cases a; cases b; auto simp: code_status_status_rel_def; fail)+


paragraph ‹Refinement relation›

fun pac_step_rel_raw :: ‹('olbl × 'lbl) set ⇒ ('a × 'b) set ⇒ ('c × 'd) set ⇒ ('a, 'c, 'olbl) pac_step ⇒ ('b, 'd, 'lbl) pac_step ⇒ bool› where
‹pac_step_rel_raw R1 R2 R3 (Add p1 p2 i r) (Add p1' p2' i' r') ⟷
   (p1, p1') ∈ R1 ∧ (p2, p2') ∈ R1 ∧ (i, i') ∈ R1 ∧
   (r, r') ∈ R2› |
‹pac_step_rel_raw R1 R2 R3 (Mult p1 p2 i r) (Mult p1' p2' i' r') ⟷
   (p1, p1') ∈ R1 ∧ (p2, p2') ∈ R2 ∧ (i, i') ∈ R1 ∧
   (r, r') ∈ R2› |
‹pac_step_rel_raw R1 R2 R3 (Del p1) (Del p1') ⟷
   (p1, p1') ∈ R1› |
‹pac_step_rel_raw R1 R2 R3 (Extension i x p1) (Extension j x' p1') ⟷
   (i, j) ∈ R1 ∧ (x, x') ∈ R3 ∧ (p1, p1') ∈ R2› |
‹pac_step_rel_raw R1 R2 R3 _ _ ⟷ False›

fun pac_step_rel_assn :: ‹('olbl ⇒ 'lbl ⇒ assn) ⇒ ('a ⇒ 'b ⇒ assn) ⇒ ('c ⇒ 'd ⇒ assn) ⇒ ('a, 'c, 'olbl) pac_step ⇒ ('b, 'd, 'lbl) pac_step ⇒ assn› where
‹pac_step_rel_assn R1 R2 R3 (Add p1 p2 i r) (Add p1' p2' i' r') =
   R1 p1 p1' * R1 p2 p2' * R1 i i' *
   R2 r r'› |
‹pac_step_rel_assn R1 R2 R3 (Mult p1 p2 i r) (Mult p1' p2' i' r') =
   R1 p1 p1' * R2 p2 p2' * R1 i i' *
   R2 r r'› |
‹pac_step_rel_assn R1 R2 R3 (Del p1) (Del p1') =
   R1 p1 p1'› |
‹pac_step_rel_assn R1 R2 R3 (Extension i x p1) (Extension i' x' p1') =
   R1 i i' * R3 x x' * R2 p1 p1'› |
‹pac_step_rel_assn R1 R2 _ _ _ = false›

lemma pac_step_rel_assn_alt_def:
  ‹pac_step_rel_assn R1 R2 R3 x y = (
  case (x, y) of
      (Add p1 p2 i r, Add p1' p2' i' r') ⇒
        R1 p1 p1' * R1 p2 p2' * R1 i i' * R2 r r'
    | (Mult p1 p2 i r, Mult p1' p2' i' r') ⇒
        R1 p1 p1' * R2 p2 p2' * R1 i i' * R2 r r'
    | (Del p1, Del p1') ⇒ R1 p1 p1'
    | (Extension i x p1, Extension i' x' p1') ⇒ R1 i i' * R3 x x' * R2 p1 p1'
    | _ ⇒ false)›
    by (auto split: pac_step.splits)


paragraph ‹Addition checking›

definition error_msg where
  ‹error_msg i msg = CFAILED (''s CHECKING failed at line '' @ show i @ '' with error '' @ msg)›

definition error_msg_notin_dom_err where
  ‹error_msg_notin_dom_err = '' notin domain''›

definition error_msg_notin_dom :: ‹nat ⇒ string› where
  ‹error_msg_notin_dom i = show i @ error_msg_notin_dom_err›

definition error_msg_reused_dom where
  ‹error_msg_reused_dom i = show i @ '' already in domain''›


definition error_msg_not_equal_dom where
  ‹error_msg_not_equal_dom p q pq r = show p @ '' + '' @ show q @ '' = '' @ show pq @ '' not equal'' @ show r›


definition check_not_equal_dom_err :: ‹llist_polynomial ⇒ llist_polynomial ⇒ llist_polynomial ⇒ llist_polynomial ⇒ string nres› where
  ‹check_not_equal_dom_err p q pq r = SPEC (λ_. True)›


definition vars_llist :: ‹llist_polynomial ⇒ string set› where
‹vars_llist  xs = ⋃(set ` fst ` set xs)›


definition check_addition_l :: ‹_ ⇒ _ ⇒ string set ⇒ nat ⇒ nat ⇒ nat ⇒ llist_polynomial ⇒ string code_status nres› where
‹check_addition_l spec A 𝒱 p q i r = do {
   let b = p ∈# dom_m A ∧ q ∈# dom_m A ∧ i ∉# dom_m A ∧ vars_llist r ⊆ 𝒱;
   if ¬b
   then RETURN (error_msg i ((if p ∉# dom_m A then error_msg_notin_dom p else []) @ (if q ∉# dom_m A then error_msg_notin_dom p else []) @
      (if i ∈# dom_m A then error_msg_reused_dom p else [])))
   else do {
     ASSERT (p ∈# dom_m A);
     let p = the (fmlookup A p);
     ASSERT (q ∈# dom_m A);
     let q = the (fmlookup A q);
     pq ← add_poly_l (p, q);
     b ← weak_equality_l pq r;
     b' ← weak_equality_l r spec;
     if b then (if b' then RETURN CFOUND else RETURN CSUCCESS)
     else do {
       c ← check_not_equal_dom_err p q pq r;
       RETURN (error_msg i c)}
   }
}›


paragraph ‹Multiplication checking›

definition check_mult_l_dom_err :: ‹bool ⇒ nat ⇒ bool ⇒ nat ⇒ string nres› where
  ‹check_mult_l_dom_err p_notin p i_already i = SPEC (λ_. True)›


definition check_mult_l_mult_err :: ‹llist_polynomial ⇒ llist_polynomial ⇒ llist_polynomial ⇒ llist_polynomial ⇒ string nres› where
  ‹check_mult_l_mult_err p q pq r = SPEC (λ_. True)›


definition check_mult_l :: ‹_ ⇒ _ ⇒ _ ⇒ nat ⇒llist_polynomial ⇒  nat ⇒ llist_polynomial ⇒ string code_status nres› where
‹check_mult_l spec A 𝒱 p q i r = do {
    let b = p ∈# dom_m A ∧ i ∉# dom_m A ∧ vars_llist q ⊆ 𝒱∧ vars_llist r ⊆ 𝒱;
    if ¬b
    then do {
      c ← check_mult_l_dom_err (p ∉# dom_m A) p (i ∈# dom_m A) i;
      RETURN (error_msg i c)}
    else do {
       ASSERT (p ∈# dom_m A);
       let p = the (fmlookup A p);
       pq ← mult_poly_full p q;
       b ← weak_equality_l pq r;
       b' ← weak_equality_l r spec;
       if b then (if b' then RETURN CFOUND else RETURN CSUCCESS) else do {
         c ← check_mult_l_mult_err p q pq r;
         RETURN (error_msg i c)
       }
     }
  }›


paragraph ‹Deletion checking›

definition check_del_l :: ‹_ ⇒ _ ⇒ nat ⇒ string code_status nres› where
‹check_del_l spec A p = RETURN CSUCCESS›


paragraph ‹Extension checking›

definition check_extension_l_dom_err :: ‹nat ⇒ string nres› where
  ‹check_extension_l_dom_err p = SPEC (λ_. True)›


definition check_extension_l_no_new_var_err :: ‹llist_polynomial ⇒ string nres› where
  ‹check_extension_l_no_new_var_err p = SPEC (λ_. True)›

definition check_extension_l_new_var_multiple_err :: ‹string ⇒ llist_polynomial ⇒ string nres› where
  ‹check_extension_l_new_var_multiple_err v p = SPEC (λ_. True)›

definition check_extension_l_side_cond_err
  :: ‹string ⇒ llist_polynomial ⇒ llist_polynomial ⇒ llist_polynomial ⇒ string nres›
where
  ‹check_extension_l_side_cond_err v p p' q = SPEC (λ_. True)›

definition check_extension_l
  :: ‹_ ⇒ _ ⇒ string set ⇒ nat ⇒ string ⇒ llist_polynomial ⇒ (string code_status) nres›
where
‹check_extension_l spec A 𝒱 i v p = do {
  let b = i ∉# dom_m A ∧ v ∉ 𝒱 ∧ ([v], -1) ∈ set p;
  if ¬b
  then do {
    c ← check_extension_l_dom_err i;
    RETURN (error_msg i c)
  } else do {
      let p' = remove1 ([v], -1) p;
      let b = vars_llist p' ⊆ 𝒱;
      if ¬b
      then do {
        c ← check_extension_l_new_var_multiple_err v p';
        RETURN (error_msg i c)
      }
      else do {
         p2 ← mult_poly_full p' p';
         let p' = map (λ(a,b). (a, -b)) p';
         q ← add_poly_l (p2, p');
         eq ← weak_equality_l q [];
         if eq then do {
           RETURN (CSUCCESS)
         } else do {
          c ← check_extension_l_side_cond_err v p p' q;
          RETURN (error_msg i c)
        }
      }
    }
  }›


lemma check_extension_alt_def:
  ‹check_extension A 𝒱 i v p ≥ do {
    b ← SPEC(λb. b ⟶ i ∉# dom_m A ∧ v ∉ 𝒱);
    if ¬b
    then RETURN (False)
    else do {
         p' ← RETURN (p + Var v);
         b ← SPEC(λb. b ⟶ vars p' ⊆ 𝒱);
         if ¬b
         then RETURN (False)
         else do {
           pq ← mult_poly_spec p' p';
           let p' = - p';
           p ← add_poly_spec pq p';
           eq ← weak_equality p 0;
           if eq then RETURN(True)
           else RETURN (False)
       }
     }
   }›
proof -
  have [intro]: ‹ab ∉ 𝒱 ⟹
       vars ba ⊆ 𝒱 ⟹
       MPoly_Type.coeff (ba + Var ab) (monomial (Suc 0) ab) = 1› for ab ba
    by (subst coeff_add[symmetric], subst not_in_vars_coeff0)
      (auto simp flip: coeff_add monom.abs_eq
        simp: not_in_vars_coeff0 MPoly_Type.coeff_def
          Var.abs_eq Var⇩0_def lookup_single_eq monom.rep_eq)
  have [simp]: ‹MPoly_Type.coeff p (monomial (Suc 0) ab) = -1›
     if ‹vars (p + Var ab) ⊆ 𝒱›
       ‹ab ∉ 𝒱›
     for ab
   proof -
     define q where ‹q ≡ p + Var ab›
     then have p: ‹p = q - Var ab›
       by auto
     show ?thesis
       unfolding p
       apply (subst coeff_minus[symmetric], subst not_in_vars_coeff0)
       using that unfolding q_def[symmetric]
       by (auto simp flip: coeff_minus simp: not_in_vars_coeff0
           Var.abs_eq Var⇩0_def simp flip: monom.abs_eq
           simp: not_in_vars_coeff0 MPoly_Type.coeff_def
           Var.abs_eq Var⇩0_def lookup_single_eq monom.rep_eq)
  qed
  have [simp]: ‹vars (p - Var ab) = vars (Var ab - p)› for ab
    using vars_uminus[of ‹p - Var ab›]
    by simp
  show ?thesis
    unfolding check_extension_def
    apply (auto 5 5 simp: check_extension_def weak_equality_def
      mult_poly_spec_def field_simps
      add_poly_spec_def power2_eq_square cong: if_cong
      intro!: intro_spec_refine[where R=Id, simplified]
      split: option.splits dest: ideal.span_add)
   done
qed

(* Copy of WB_More_Refinement *)
lemma RES_RES_RETURN_RES: ‹RES A ⤜ (λT. RES (f T)) = RES (⋃(f ` A))›
  by (auto simp: pw_eq_iff refine_pw_simps)


lemma check_add_alt_def:
  ‹check_add A 𝒱 p q i r ≥
    do {
     b ← SPEC(λb. b ⟶ p ∈# dom_m A ∧ q ∈# dom_m A ∧ i ∉# dom_m A ∧ vars r ⊆ 𝒱);
     if ¬b
     then RETURN False
     else do {
       ASSERT (p ∈# dom_m A);
       let p = the (fmlookup A p);
       ASSERT (q ∈# dom_m A);
       let q = the (fmlookup A q);
       pq ← add_poly_spec p q;
       eq ← weak_equality pq r;
       RETURN eq
     }
  }› (is ‹_ ≥ ?A›)
proof -
  have check_add_alt_def: ‹check_add A 𝒱 p q i r = do {
     b ← SPEC(λb. b ⟶ p ∈# dom_m A ∧ q ∈# dom_m A ∧ i ∉# dom_m A ∧ vars r ⊆ 𝒱);
     if ¬b then SPEC(λb. b ⟶ p ∈# dom_m A ∧ q ∈# dom_m A ∧ i ∉# dom_m A ∧ vars r ⊆ 𝒱 ∧
            the (fmlookup A p) + the (fmlookup A q) - r ∈  ideal polynomial_bool)
     else
       SPEC(λb. b ⟶ p ∈# dom_m A ∧ q ∈# dom_m A ∧ i ∉# dom_m A ∧ vars r ⊆ 𝒱 ∧
            the (fmlookup A p) + the (fmlookup A q) - r ∈  ideal polynomial_bool)}›
   (is ‹_ = ?B›)
    by (auto simp: check_add_def RES_RES_RETURN_RES)
   have ‹?A ≤ ⇓ Id (check_add A 𝒱 p q i r)›
     apply refine_vcg
     apply ((auto simp: check_add_alt_def weak_equality_def
        add_poly_spec_def RES_RES_RETURN_RES summarize_ASSERT_conv
      cong: if_cong
      intro!: ideal.span_zero;fail)+)
      done
   then show ?thesis
     unfolding check_add_alt_def[symmetric]
     by simp
qed

lemma check_mult_alt_def:
  ‹check_mult A 𝒱 p q i r ≥
    do {
     b ← SPEC(λb. b ⟶ p ∈# dom_m A ∧ i ∉# dom_m A ∧ vars q ⊆ 𝒱  ∧ vars r ⊆ 𝒱);
     if ¬b
     then RETURN False
     else do {
       ASSERT (p ∈# dom_m A);
       let p = the (fmlookup A p);
       pq ← mult_poly_spec p q;
       p ← weak_equality pq r;
       RETURN p
     }
  }›
  unfolding check_mult_def
  apply (rule refine_IdD)
  by refine_vcg
   (auto simp: check_mult_def weak_equality_def
      mult_poly_spec_def RES_RES_RETURN_RES
    intro!:  ideal.span_zero
      exI[of _ ‹the (fmlookup A p) * q›])

primrec insort_key_rel :: "('b ⇒ 'b ⇒ bool) ⇒ 'b ⇒ 'b list ⇒ 'b list" where
"insort_key_rel f x [] = [x]" |
"insort_key_rel f x (y#ys) =
  (if f x y then (x#y#ys) else y#(insort_key_rel f x ys))"

lemma set_insort_key_rel[simp]: ‹set (insort_key_rel R x xs) = insert x (set xs)›
  by (induction xs)
   auto

lemma sorted_wrt_insort_key_rel:
   ‹totalp_on (insert x (set xs)) R ⟹ transp R ⟹ reflp R ⟹
    sorted_wrt R xs ⟹ sorted_wrt R (insort_key_rel R x xs)›
  by (induction xs)
   (auto dest: transpD reflpD simp: totalp_on_def)

lemma sorted_wrt_insort_key_rel2:
   ‹totalp_on (insert x (set xs)) R ⟹ transp R ⟹ x ∉ set xs ⟹
    sorted_wrt R xs ⟹ sorted_wrt R (insort_key_rel R x xs)›
  by (induction xs)
   (auto dest: transpD simp: totalp_on_def in_mono)


paragraph ‹Step checking›

definition PAC_checker_l_step ::  ‹_ ⇒ string code_status × string set × _ ⇒ (llist_polynomial, string, nat) pac_step ⇒ _› where
  ‹PAC_checker_l_step = (λspec (st', 𝒱, A) st. case st of
     Add _ _ _ _ ⇒
       do {
         r ← full_normalize_poly (pac_res st);
        eq ← check_addition_l spec A 𝒱 (pac_src1 st) (pac_src2 st) (new_id st) r;
        let _ = eq;
        if ¬is_cfailed eq
        then RETURN (merge_cstatus st' eq,
          𝒱, fmupd (new_id st) r A)
        else RETURN (eq, 𝒱, A)
   }
   | Del _ ⇒
       do {
        eq ← check_del_l spec A (pac_src1 st);
        let _ = eq;
        if ¬is_cfailed eq
        then RETURN (merge_cstatus st' eq, 𝒱, fmdrop (pac_src1 st) A)
        else RETURN (eq, 𝒱, A)
   }
   | Mult _ _ _ _ ⇒
       do {
         r ← full_normalize_poly (pac_res st);
         q ← full_normalize_poly (pac_mult st);
        eq ← check_mult_l spec A 𝒱 (pac_src1 st) q (new_id st) r;
        let _ = eq;
        if ¬is_cfailed eq
        then RETURN (merge_cstatus st' eq,
          𝒱, fmupd (new_id st) r A)
        else RETURN (eq, 𝒱, A)
   }
   | Extension _ _ _ ⇒
       do {
         r ← full_normalize_poly (([new_var st], -1) # (pac_res st));
        (eq) ← check_extension_l spec A 𝒱 (new_id st) (new_var st) r;
        if ¬is_cfailed eq
        then do {
          RETURN (st',
            insert (new_var st) 𝒱, fmupd (new_id st) r A)}
        else RETURN (eq, 𝒱, A)
   }
 )›

lemma pac_step_rel_raw_def:
  ‹⟨K, V, R⟩ pac_step_rel_raw = pac_step_rel_raw K V R›
  by (auto intro!: ext simp: relAPP_def)

definition mononoms_equal_up_to_reorder where
  ‹mononoms_equal_up_to_reorder xs ys ⟷
     map (λ(a, b).  (mset a, b)) xs = map (λ(a, b). (mset a, b)) ys›


 definition normalize_poly_l where
  ‹normalize_poly_l p = SPEC (λp'.
     normalize_poly_p⇧*⇧* ((λ(a, b). (mset a, b)) `# mset p) ((λ(a, b). (mset a, b)) `# mset p') ∧
     0 ∉# snd `# mset p' ∧
     sorted_wrt (rel2p (term_order_rel ×⇩r int_rel)) p' ∧
     (∀ x ∈ mononoms p'. sorted_wrt (rel2p var_order_rel) x))›


definition remap_polys_l_dom_err :: ‹string nres› where
  ‹remap_polys_l_dom_err = SPEC (λ_. True)›


definition remap_polys_l :: ‹llist_polynomial ⇒ string set ⇒ (nat, llist_polynomial) fmap ⇒
   (_ code_status × string set × (nat, llist_polynomial) fmap) nres› where
  ‹remap_polys_l spec = (λ𝒱 A. do{
   dom ← SPEC(λdom. set_mset (dom_m A) ⊆ dom ∧ finite dom);
   failed ← SPEC(λ_::bool. True);
   if failed
   then do {
      c ← remap_polys_l_dom_err;
      RETURN (error_msg (0 :: nat) c, 𝒱, fmempty)
   }
   else do {
     (b, 𝒱, A) ← FOREACH dom
       (λi (b, 𝒱,  A').
          if i ∈# dom_m A
          then  do {
            p ← full_normalize_poly (the (fmlookup A i));
            eq ← weak_equality_l p spec;
            𝒱 ← RETURN(𝒱 ∪ vars_llist (the (fmlookup A i)));
            RETURN(b ∨ eq, 𝒱, fmupd i p A')
          } else RETURN (b, 𝒱, A'))
       (False, 𝒱, fmempty);
     RETURN (if b then CFOUND else CSUCCESS, 𝒱, A)
 }})›

definition PAC_checker_l where
  ‹PAC_checker_l spec A b st = do {
    (S, _) ← WHILE⇩T
       (λ((b, A), n). ¬is_cfailed b ∧ n ≠ [])
       (λ((bA), n). do {
          ASSERT(n ≠ []);
          S ← PAC_checker_l_step spec bA (hd n);
          RETURN (S, tl n)
        })
      ((b, A), st);
    RETURN S
  }›


subsection ‹Correctness›

text ‹We now enter the locale to reason about polynomials directly.›

context poly_embed
begin

abbreviation pac_step_rel where
  ‹pac_step_rel ≡ p2rel (⟨Id, fully_unsorted_poly_rel O mset_poly_rel, var_rel⟩ pac_step_rel_raw)›

abbreviation fmap_polys_rel where
  ‹fmap_polys_rel ≡ ⟨nat_rel, sorted_poly_rel O mset_poly_rel⟩fmap_rel›

lemma
  ‹normalize_poly_p s0 s ⟹
        (s0, p) ∈ mset_poly_rel ⟹
        (s, p) ∈ mset_poly_rel›
  by (auto simp: mset_poly_rel_def normalize_poly_p_poly_of_mset)

lemma vars_poly_of_vars:
  ‹vars (poly_of_vars a :: int mpoly) ⊆ (φ ` set_mset a)›
  by (induction a)
   (auto simp: vars_mult_Var)

lemma vars_polynomial_of_mset:
  ‹vars (polynomial_of_mset za) ⊆ ⋃(image φ ` (set_mset o fst) ` set_mset za)›
  apply (induction za)
  using vars_poly_of_vars
  by (fastforce elim!: in_vars_addE simp: vars_mult_Const split: if_splits)+

lemma fully_unsorted_poly_rel_vars_subset_vars_llist:
  ‹(A, B) ∈ fully_unsorted_poly_rel O mset_poly_rel ⟹ vars B ⊆ φ ` vars_llist A›
  by (auto simp: fully_unsorted_poly_list_rel_def mset_poly_rel_def
      set_rel_def var_rel_def br_def vars_llist_def list_rel_append2 list_rel_append1
      list_rel_split_right_iff list_mset_rel_def image_iff
      unsorted_term_poly_list_rel_def list_rel_split_left_iff
    dest!: set_rev_mp[OF _ vars_polynomial_of_mset] split_list
    dest: multi_member_split
    dest: arg_cong[of ‹mset _› ‹add_mset _ _› set_mset])

lemma fully_unsorted_poly_rel_extend_vars:
  ‹(A, B) ∈ fully_unsorted_poly_rel O mset_poly_rel ⟹
  (x1c, x1a) ∈ ⟨var_rel⟩set_rel ⟹
   RETURN (x1c ∪ vars_llist A)
    ≤ ⇓ (⟨var_rel⟩set_rel)
       (SPEC ((⊆) (x1a ∪ vars (B))))›
  using fully_unsorted_poly_rel_vars_subset_vars_llist[of A B]
  apply (subst RETURN_RES_refine_iff)
  apply clarsimp
  apply (rule exI[of _ ‹x1a ∪ φ ` vars_llist A›])
  apply (auto simp: set_rel_def var_rel_def br_def
    dest: fully_unsorted_poly_rel_vars_subset_vars_llist)
  done

lemma remap_polys_l_remap_polys:
  assumes
    AB: ‹(A, B) ∈ ⟨nat_rel, fully_unsorted_poly_rel O mset_poly_rel⟩fmap_rel› and
    spec: ‹(spec, spec') ∈ sorted_poly_rel O mset_poly_rel› and
    V: ‹(𝒱, 𝒱') ∈ ⟨var_rel⟩set_rel›
  shows ‹remap_polys_l spec 𝒱 A ≤
     ⇓(code_status_status_rel ×⇩r ⟨var_rel⟩set_rel ×⇩r fmap_polys_rel) (remap_polys spec' 𝒱' B)›
  (is ‹_ ≤ ⇓ ?R _›)
proof -
  have 1: ‹inj_on id (dom :: nat set)› for dom
    by auto
  have H: ‹x ∈# dom_m A ⟹
     (⋀p. (the (fmlookup A x), p) ∈ fully_unsorted_poly_rel ⟹
       (p, the (fmlookup B x)) ∈ mset_poly_rel ⟹ thesis) ⟹
     thesis› for x thesis
     using fmap_rel_nat_the_fmlookup[OF AB, of x x] fmap_rel_nat_rel_dom_m[OF AB] by auto
  have full_normalize_poly: ‹full_normalize_poly (the (fmlookup A x))
       ≤ ⇓ (sorted_poly_rel O mset_poly_rel)
          (SPEC
            (λp. the (fmlookup B x') - p ∈ More_Modules.ideal polynomial_bool ∧
                 vars p ⊆ vars (the (fmlookup B x'))))›
      if x_dom: ‹x ∈# dom_m A› and ‹(x, x') ∈ Id› for x x'
      apply (rule H[OF x_dom])
      subgoal for p
      apply (rule full_normalize_poly_normalize_poly_p[THEN order_trans])
      apply assumption
      subgoal
        using that(2) apply -
        unfolding conc_fun_chain[symmetric]
        by (rule ref_two_step', rule RES_refine)
         (auto simp: rtranclp_normalize_poly_p_poly_of_mset
          mset_poly_rel_def ideal.span_zero)
      done
      done

  have H': ‹(p, pa) ∈ sorted_poly_rel O mset_poly_rel ⟹
     weak_equality_l p spec ≤ SPEC (λeqa. eqa ⟶ pa = spec')› for p pa
    using spec by (auto simp: weak_equality_l_def weak_equality_spec_def
        list_mset_rel_def br_def mset_poly_rel_def
      dest: list_rel_term_poly_list_rel_same_rightD sorted_poly_list_relD)

  have emp: ‹(𝒱, 𝒱') ∈ ⟨var_rel⟩set_rel ⟹
    ((False, 𝒱, fmempty), False, 𝒱', fmempty) ∈ bool_rel ×⇩r ⟨var_rel⟩set_rel ×⇩r fmap_polys_rel› for 𝒱 𝒱'
    by auto
  show ?thesis
    using assms
    unfolding remap_polys_l_def remap_polys_l_dom_err_def
      remap_polys_def prod.case
    apply (refine_rcg full_normalize_poly fmap_rel_fmupd_fmap_rel)
    subgoal
      by auto
    subgoal
      by auto
    subgoal
      by (auto simp: error_msg_def)
    apply (rule 1)
    subgoal by auto
    apply (rule emp)
    subgoal
      using V by auto
    subgoal by auto
    subgoal by auto
    subgoal by (rule H')
    apply (rule fully_unsorted_poly_rel_extend_vars)
    subgoal by (auto intro!: fmap_rel_nat_the_fmlookup)
    subgoal by (auto intro!: fmap_rel_fmupd_fmap_rel)
    subgoal by (auto intro!: fmap_rel_fmupd_fmap_rel)
    subgoal by auto
    subgoal by auto
    done
qed


lemma fref_to_Down_curry:
  ‹(uncurry f, uncurry g) ∈ [P]⇩f A → ⟨B⟩nres_rel ⟹
     (⋀x x' y y'. P (x', y') ⟹ ((x, y), (x', y')) ∈ A ⟹ f x y ≤ ⇓ B (g x' y'))›
  unfolding fref_def uncurry_def nres_rel_def
  by auto

lemma weak_equality_spec_weak_equality:
  ‹(p, p') ∈ mset_poly_rel ⟹
    (r, r') ∈ mset_poly_rel ⟹
    weak_equality_spec p r ≤ weak_equality p' r'›
  unfolding weak_equality_spec_def weak_equality_def
  by (auto simp: mset_poly_rel_def)


lemma weak_equality_l_weak_equality_l'[refine]:
  ‹weak_equality_l p q ≤ ⇓ bool_rel (weak_equality p' q')›
  if ‹(p, p') ∈ sorted_poly_rel O mset_poly_rel›
    ‹(q, q') ∈ sorted_poly_rel O mset_poly_rel›
  for p p' q q'
  using that
  by (auto intro!: weak_equality_l_weak_equality_spec[THEN fref_to_Down_curry, THEN order_trans]
         ref_two_step'
         weak_equality_spec_weak_equality
      simp flip: conc_fun_chain)

lemma error_msg_ne_SUCCES[iff]:
  ‹error_msg i m ≠ CSUCCESS›
  ‹error_msg i m ≠ CFOUND›
  ‹is_cfailed (error_msg i m)›
  ‹¬is_cfound (error_msg i m)›
  by (auto simp: error_msg_def)

lemma sorted_poly_rel_vars_llist:
  ‹(r, r') ∈ sorted_poly_rel O mset_poly_rel ⟹
   vars r' ⊆ φ ` vars_llist r›
  apply (auto simp: mset_poly_rel_def
      set_rel_def var_rel_def br_def vars_llist_def list_rel_append2 list_rel_append1
      list_rel_split_right_iff list_mset_rel_def image_iff sorted_poly_list_rel_wrt_def
    dest!: set_rev_mp[OF _ vars_polynomial_of_mset]
    dest!: split_list)
    apply (auto dest!: multi_member_split simp: list_rel_append1
      term_poly_list_rel_def eq_commute[of _ ‹mset _›]
      list_rel_split_right_iff list_rel_append2 list_rel_split_left_iff
      dest: arg_cong[of ‹mset _› ‹add_mset _ _› set_mset])
    done


lemma check_addition_l_check_add:
  assumes ‹(A, B) ∈ fmap_polys_rel› and ‹(r, r') ∈ sorted_poly_rel O mset_poly_rel›
    ‹(p, p') ∈ Id› ‹(q, q') ∈ Id› ‹(i, i') ∈ nat_rel›
    ‹(𝒱', 𝒱) ∈ ⟨var_rel⟩set_rel›
  shows
    ‹check_addition_l spec A 𝒱' p q i r ≤ ⇓ {(st, b). (¬is_cfailed st ⟷ b) ∧
       (is_cfound st ⟶ spec = r)} (check_add B 𝒱 p' q' i' r')›
proof -
  have [refine]:
    ‹add_poly_l (p, q) ≤ ⇓ (sorted_poly_rel O mset_poly_rel) (add_poly_spec p' q')›
    if ‹(p, p') ∈ sorted_poly_rel O mset_poly_rel›
      ‹(q, q') ∈ sorted_poly_rel O mset_poly_rel›
    for p p' q q'
    using that
    by (auto intro!: add_poly_l_add_poly_p'[THEN order_trans] ref_two_step'
         add_poly_p'_add_poly_spec
      simp flip: conc_fun_chain)

  show ?thesis
    using assms
    unfolding check_addition_l_def
      check_not_equal_dom_err_def apply -
    apply (rule order_trans)
    defer
    apply (rule ref_two_step')
    apply (rule check_add_alt_def)
    apply refine_rcg
    subgoal
      by (drule sorted_poly_rel_vars_llist)
       (auto simp: set_rel_def var_rel_def br_def)
    subgoal
      by auto
    subgoal
      by auto
    subgoal
      by auto
    subgoal
      by auto
    subgoal
      by auto
    subgoal
      by auto
    subgoal
      by (auto simp: weak_equality_l_def bind_RES_RETURN_eq)
    done
qed

lemma check_del_l_check_del:
  ‹(A, B) ∈ fmap_polys_rel ⟹ (x3, x3a) ∈ Id ⟹ check_del_l spec A (pac_src1 (Del x3))
    ≤ ⇓ {(st, b). (¬is_cfailed st ⟷ b) ∧ (b ⟶ st = CSUCCESS)} (check_del B (pac_src1 (Del x3a)))›
  unfolding check_del_l_def check_del_def
  by (refine_vcg lhs_step_If RETURN_SPEC_refine)
    (auto simp: fmap_rel_nat_rel_dom_m bind_RES_RETURN_eq)

lemma check_mult_l_check_mult:
  assumes ‹(A, B) ∈ fmap_polys_rel› and ‹(r, r') ∈ sorted_poly_rel O mset_poly_rel› and
    ‹(q, q') ∈ sorted_poly_rel O mset_poly_rel›
    ‹(p, p') ∈ Id› ‹(i, i') ∈ nat_rel› ‹(𝒱, 𝒱') ∈ ⟨var_rel⟩set_rel›
  shows
    ‹check_mult_l spec A 𝒱 p q i r ≤ ⇓  {(st, b). (¬is_cfailed st ⟷ b) ∧
       (is_cfound st ⟶ spec = r)} (check_mult B 𝒱' p' q' i' r')›
proof -
  have [refine]:
    ‹mult_poly_full p q ≤ ⇓ (sorted_poly_rel O mset_poly_rel) (mult_poly_spec p' q')›
    if ‹(p, p') ∈ sorted_poly_rel O mset_poly_rel›
      ‹(q, q') ∈ sorted_poly_rel O mset_poly_rel›
    for p p' q q'
    using that
    by (auto intro!: mult_poly_full_mult_poly_p'[THEN order_trans] ref_two_step'
         mult_poly_p'_mult_poly_spec
      simp flip: conc_fun_chain)

  show ?thesis
    using assms
    unfolding check_mult_l_def
      check_mult_l_mult_err_def check_mult_l_dom_err_def apply -
    apply (rule order_trans)
    defer
    apply (rule ref_two_step')
    apply (rule check_mult_alt_def)
    apply refine_rcg
    subgoal
      by (drule sorted_poly_rel_vars_llist)+
        (fastforce simp: set_rel_def var_rel_def br_def)
    subgoal
      by auto
    subgoal
      by auto
    subgoal
      by auto
    subgoal
      by auto
    subgoal
      by (auto simp: weak_equality_l_def bind_RES_RETURN_eq)
    done
qed


lemma normalize_poly_normalize_poly_spec:
  assumes ‹(r, t) ∈ unsorted_poly_rel O mset_poly_rel›
  shows
    ‹normalize_poly r ≤ ⇓(sorted_poly_rel O mset_poly_rel) (normalize_poly_spec t)›
proof -
  obtain s where
    rs: ‹(r, s) ∈ unsorted_poly_rel› and
    st: ‹(s, t) ∈ mset_poly_rel›
    using assms by auto
  show ?thesis
    by (rule normalize_poly_normalize_poly_p[THEN order_trans, OF rs])
     (use st in ‹auto dest!: rtranclp_normalize_poly_p_poly_of_mset
      intro!: ref_two_step' RES_refine exI[of _ t]
      simp: normalize_poly_spec_def ideal.span_zero mset_poly_rel_def
      simp flip: conc_fun_chain›)
qed

lemma remove1_list_rel:
  ‹(xs, ys) ∈ ⟨R⟩ list_rel ⟹
  (a, b) ∈ R ⟹
  IS_RIGHT_UNIQUE R ⟹
  IS_LEFT_UNIQUE R ⟹
  (remove1 a xs, remove1 b ys) ∈ ⟨R⟩list_rel›
  by (induction xs ys rule: list_rel_induct)
   (auto simp: single_valued_def IS_LEFT_UNIQUE_def)

lemma remove1_list_rel2:
  ‹(xs, ys) ∈ ⟨R⟩ list_rel ⟹
  (a, b) ∈ R ⟹
  (⋀c. (a, c) ∈ R ⟹ c = b) ⟹
  (⋀c. (c, b) ∈ R ⟹ c = a) ⟹
  (remove1 a xs, remove1 b ys) ∈ ⟨R⟩list_rel›
  apply (induction xs ys rule: list_rel_induct)
   apply (solves ‹simp (no_asm)›)
  by (smt (verit) list_rel_simp(4) remove1.simps(2))

lemma remove1_sorted_poly_rel_mset_poly_rel:
  assumes
    ‹(r, r') ∈ sorted_poly_rel O mset_poly_rel› and
    ‹([a], 1) ∈ set r›
  shows
    ‹(remove1 ([a], 1) r, r' - Var (φ a))
          ∈ sorted_poly_rel O mset_poly_rel›
proof -
   have [simp]: ‹([a], {#a#}) ∈ term_poly_list_rel›
     ‹⋀aa. ([a], aa) ∈ term_poly_list_rel ⟷ aa = {#a#}›
     by (auto simp: term_poly_list_rel_def)
  have H:
    ‹⋀aa. ([a], aa) ∈ term_poly_list_rel ⟹ aa = {#a#}›
     ‹⋀aa. (aa, {#a#}) ∈ term_poly_list_rel ⟹ aa = [a]›
     by (auto simp: single_valued_def IS_LEFT_UNIQUE_def
       term_poly_list_rel_def)

  have [simp]: ‹Const (1 :: int) = (1 :: int mpoly)›
    by (simp add: Const.abs_eq Const⇩0_one one_mpoly.abs_eq)
  have [simp]: ‹sorted_wrt term_order (map fst r) ⟹
         sorted_wrt term_order (map fst (remove1 ([a], 1) r))›
    by (induction r) auto
  have [intro]: ‹distinct (map fst r) ⟹ distinct (map fst (remove1 x r))› for x
    by (induction r) (auto dest: notin_set_remove1)
  have [simp]: ‹(r, ya) ∈ ⟨term_poly_list_rel ×⇩r int_rel⟩list_rel ⟹
         polynomial_of_mset (mset ya) -  Var (φ a) =
         polynomial_of_mset (remove1_mset ({#a#}, 1) (mset ya))› for ya
    using assms
     by (auto simp: list_rel_append1 list_rel_split_right_iff
       dest!: split_list)

  show ?thesis
    using assms
    apply (elim relcompEpair)
    apply (rename_tac za, rule_tac b = ‹remove1_mset ({#a#}, 1) za› in relcompI)
    apply (auto simp: mset_poly_rel_def sorted_poly_list_rel_wrt_def Collect_eq_comp'
      intro!: relcompI[of _ ‹remove1 ({#a#}, 1) ya›
        for ya :: ‹(string multiset × int) list›]  remove1_list_rel2 intro: H
      simp: list_mset_rel_def br_def
      dest: in_diffD)
    done
qed

lemma remove1_sorted_poly_rel_mset_poly_rel_minus:
  assumes
    ‹(r, r') ∈ sorted_poly_rel O mset_poly_rel› and
    ‹([a], -1) ∈ set r›
  shows
    ‹(remove1 ([a], -1) r, r' + Var (φ a))
          ∈ sorted_poly_rel O mset_poly_rel›
proof -
   have [simp]: ‹([a], {#a#}) ∈ term_poly_list_rel›
     ‹⋀aa. ([a], aa) ∈ term_poly_list_rel ⟷ aa = {#a#}›
     by (auto simp: term_poly_list_rel_def)
  have H:
    ‹⋀aa. ([a], aa) ∈ term_poly_list_rel ⟹ aa = {#a#}›
     ‹⋀aa. (aa, {#a#}) ∈ term_poly_list_rel ⟹ aa = [a]›
     by (auto simp: single_valued_def IS_LEFT_UNIQUE_def
       term_poly_list_rel_def)

  have [simp]: ‹Const (1 :: int) = (1 :: int mpoly)›
    by (simp add: Const.abs_eq Const⇩0_one one_mpoly.abs_eq)
  have [simp]: ‹sorted_wrt term_order (map fst r) ⟹
         sorted_wrt term_order (map fst (remove1 ([a], -1) r))›
    by (induction r) auto
  have [intro]: ‹distinct (map fst r) ⟹ distinct (map fst (remove1 x r))› for x
    apply (induction r) apply auto
    by (meson img_fst in_set_remove1D)
  have [simp]: ‹(r, ya) ∈ ⟨term_poly_list_rel ×⇩r int_rel⟩list_rel ⟹
         polynomial_of_mset (mset ya) +  Var (φ a) =
         polynomial_of_mset (remove1_mset ({#a#}, -1) (mset ya))› for ya
    using assms
     by (auto simp: list_rel_append1 list_rel_split_right_iff
       dest!: split_list)

  show ?thesis
    using assms
    apply (elim relcompEpair)
    apply (rename_tac za, rule_tac b = ‹remove1_mset ({#a#}, -1) za› in relcompI)
    by (auto simp: mset_poly_rel_def sorted_poly_list_rel_wrt_def Collect_eq_comp'
       dest: in_diffD
       intro!: relcompI[of _ ‹remove1 ({#a#}, -1) ya›
         for ya :: ‹(string multiset × int) list›]  remove1_list_rel2 intro: H
      simp: list_mset_rel_def br_def)
qed


lemma insert_var_rel_set_rel:
  ‹(𝒱, 𝒱') ∈ ⟨var_rel⟩set_rel ⟹
  (yb, x2) ∈ var_rel ⟹
  (insert yb 𝒱, insert x2 𝒱') ∈ ⟨var_rel⟩set_rel›
  by (auto simp: var_rel_def set_rel_def)

lemma var_rel_set_rel_iff:
  ‹(𝒱, 𝒱') ∈ ⟨var_rel⟩set_rel ⟹
  (yb, x2) ∈ var_rel ⟹
  yb ∈ 𝒱 ⟷ x2 ∈  𝒱'›
  using φ_inj inj_eq by (fastforce simp: var_rel_def set_rel_def br_def)


lemma check_extension_l_check_extension:
  assumes ‹(A, B) ∈ fmap_polys_rel› and ‹(r, r') ∈ sorted_poly_rel O mset_poly_rel› and
    ‹(i, i') ∈ nat_rel› ‹(𝒱, 𝒱') ∈ ⟨var_rel⟩set_rel› ‹(x, x') ∈ var_rel›
  shows
    ‹check_extension_l spec A 𝒱 i x r ≤
      ⇓{((st), (b)).
        (¬is_cfailed st ⟷ b) ∧
       (is_cfound st ⟶ spec = r)} (check_extension B 𝒱' i' x' r')›
proof -
  have ‹x' = φ x›
    using assms(5) by (auto simp: var_rel_def br_def)
  have [refine]:
    ‹mult_poly_full p q ≤ ⇓ (sorted_poly_rel O mset_poly_rel) (mult_poly_spec p' q')›
    if ‹(p, p') ∈ sorted_poly_rel O mset_poly_rel›
      ‹(q, q') ∈ sorted_poly_rel O mset_poly_rel›
    for p p' q q'
    using that
    by (auto intro!: mult_poly_full_mult_poly_p'[THEN order_trans] ref_two_step'
         mult_poly_p'_mult_poly_spec
      simp flip: conc_fun_chain)
  have [refine]:
    ‹add_poly_l (p, q) ≤ ⇓ (sorted_poly_rel O mset_poly_rel) (add_poly_spec p' q')›
    if ‹(p, p') ∈ sorted_poly_rel O mset_poly_rel›
      ‹(q, q') ∈ sorted_poly_rel O mset_poly_rel›
    for p p' q q'
    using that
    by (auto intro!: add_poly_l_add_poly_p'[THEN order_trans] ref_two_step'
         add_poly_p'_add_poly_spec
      simp flip: conc_fun_chain)

  have [simp]: ‹(l, l') ∈ ⟨term_poly_list_rel ×⇩r int_rel⟩list_rel ⟹
       (map (λ(a, b). (a, - b)) l, map (λ(a, b). (a, - b)) l')
       ∈ ⟨term_poly_list_rel ×⇩r int_rel⟩list_rel› for l l'
     by (induction l l'  rule: list_rel_induct)
        (auto simp: list_mset_rel_def br_def)

  have [intro!]:
    ‹(x2c, za) ∈ ⟨term_poly_list_rel ×⇩r int_rel⟩list_rel O list_mset_rel ⟹
     (map (λ(a, b). (a, - b)) x2c,
        {#case x of (a, b) ⇒ (a, - b). x ∈# za#})
       ∈ ⟨term_poly_list_rel ×⇩r int_rel⟩list_rel O list_mset_rel› for x2c za
     apply (auto)
     subgoal for y
       apply (induction x2c y  rule: list_rel_induct)
       apply (auto simp: list_mset_rel_def br_def)
       apply (rename_tac a ba aa l l', rule_tac b = ‹(aa, - ba) # map (λ(a, b). (a, - b)) l'› in relcompI)
       by auto
     done
  have [simp]: ‹(λx. fst (case x of (a, b) ⇒ (a, - b))) = fst›
    by (auto intro: ext)

  have uminus: ‹(x2c, x2a) ∈ sorted_poly_rel O mset_poly_rel ⟹
       (map (λ(a, b). (a, - b)) x2c,
        - x2a)
       ∈ sorted_poly_rel O mset_poly_rel› for x2c x2a x1c x1a
     apply (clarsimp simp: sorted_poly_list_rel_wrt_def
      mset_poly_rel_def)
    apply (rule_tac b = ‹(λ(a, b). (a, - b)) `# za› in relcompI)
    by (auto simp: sorted_poly_list_rel_wrt_def
      mset_poly_rel_def comp_def polynomial_of_mset_uminus)
   have [simp]: ‹([], 0) ∈ sorted_poly_rel O mset_poly_rel›
     by (auto simp: sorted_poly_list_rel_wrt_def
      mset_poly_rel_def list_mset_rel_def br_def
      intro!: relcompI[of _ ‹{#}›])
   show ?thesis
     unfolding check_extension_l_def
       check_extension_l_dom_err_def
       check_extension_l_no_new_var_err_def
       check_extension_l_new_var_multiple_err_def
       check_extension_l_side_cond_err_def
      apply (rule order_trans)
      defer
      apply (rule ref_two_step')
      apply (rule check_extension_alt_def)
      apply (refine_vcg )
      subgoal using assms(1,3,4,5)
        by (auto simp: var_rel_set_rel_iff)
      subgoal using assms(1,3,4,5)
        by (auto simp: var_rel_set_rel_iff)
      subgoal by auto
      subgoal by auto
      apply (subst ‹x' = φ x›, rule remove1_sorted_poly_rel_mset_poly_rel_minus)
      subgoal using assms by auto
      subgoal using assms by auto
      subgoal using sorted_poly_rel_vars_llist[of ‹r› ‹r'›] assms
        by (force simp: set_rel_def var_rel_def br_def
          dest!: sorted_poly_rel_vars_llist)
      subgoal by auto
      subgoal by auto
      subgoal using assms by auto
      subgoal using assms by auto
      apply (rule uminus)
      subgoal using assms by auto
      subgoal using assms by auto
      subgoal using assms by auto
      subgoal using assms by auto
      subgoal using assms by auto
      done
qed


lemma full_normalize_poly_diff_ideal:
  fixes dom
  assumes ‹(p, p') ∈ fully_unsorted_poly_rel O mset_poly_rel›
  shows
    ‹full_normalize_poly p
    ≤ ⇓ (sorted_poly_rel O mset_poly_rel)
       (normalize_poly_spec p')›
proof -
  obtain q where
    pq: ‹(p, q) ∈ fully_unsorted_poly_rel›  and qp':‹(q, p') ∈ mset_poly_rel›
    using assms by auto
   show ?thesis
     unfolding normalize_poly_spec_def
     apply (rule full_normalize_poly_normalize_poly_p[THEN order_trans])
     apply (rule pq)
     unfolding conc_fun_chain[symmetric]
     by (rule ref_two_step', rule RES_refine)
       (use qp' in ‹auto dest!: rtranclp_normalize_poly_p_poly_of_mset
            simp: mset_poly_rel_def ideal.span_zero›)
qed

lemma insort_key_rel_decomp:
   ‹∃ys zs. xs = ys @ zs ∧ insort_key_rel R x xs = ys @ x # zs›
  apply (induction xs)
  subgoal by auto
  subgoal for a xs
    by (force intro: exI[of _ ‹a # _›])
  done

lemma list_rel_append_same_length:
   ‹length xs = length xs' ⟹ (xs @ ys, xs' @ ys') ∈ ⟨R⟩list_rel ⟷ (xs, xs') ∈ ⟨R⟩list_rel ∧ (ys, ys') ∈ ⟨R⟩list_rel›
  by (auto simp: list_rel_def list_all2_append2 dest: list_all2_lengthD)

lemma term_poly_list_rel_list_relD: ‹(ys, cs) ∈ ⟨term_poly_list_rel ×⇩r int_rel⟩list_rel ⟹
       cs = map (λ(a, y). (mset a, y)) ys›
  by (induction ys arbitrary: cs)
   (auto simp: term_poly_list_rel_def list_rel_def list_all2_append list_all2_Cons1 list_all2_Cons2)

lemma term_poly_list_rel_single: ‹([x32], {#x32#}) ∈ term_poly_list_rel›
  by (auto simp: term_poly_list_rel_def)

lemma unsorted_poly_rel_list_rel_list_rel_uminus:
   ‹(map (λ(a, b). (a, - b)) r, yc)
       ∈ ⟨unsorted_term_poly_list_rel ×⇩r int_rel⟩list_rel ⟹
       (r, map (λ(a, b). (a, - b)) yc)
       ∈ ⟨unsorted_term_poly_list_rel ×⇩r int_rel⟩list_rel›
  by (induction r arbitrary: yc)
   (auto simp: elim!: list_relE3)

lemma mset_poly_rel_minus: ‹({#(a, b)#}, v') ∈ mset_poly_rel ⟹
       (mset yc, r') ∈ mset_poly_rel ⟹
       (r, yc)
       ∈ ⟨unsorted_term_poly_list_rel ×⇩r int_rel⟩list_rel ⟹
       (add_mset (a, b) (mset yc),
        v' + r')
       ∈ mset_poly_rel›
  by (induction r arbitrary: r')
    (auto simp: mset_poly_rel_def polynomial_of_mset_uminus)

lemma fully_unsorted_poly_rel_diff:
   ‹([v], v') ∈ fully_unsorted_poly_rel O mset_poly_rel ⟹
   (r, r') ∈ fully_unsorted_poly_rel O mset_poly_rel ⟹
    (v # r,
     v' + r')
    ∈ fully_unsorted_poly_rel O mset_poly_rel›
  apply auto
  apply (rule_tac b = ‹y + ya› in relcompI)
  apply (auto simp: fully_unsorted_poly_list_rel_def list_mset_rel_def br_def)
  apply (rule_tac b = ‹yb @ yc› in relcompI)
  apply (auto elim!: list_relE3 simp: unsorted_poly_rel_list_rel_list_rel_uminus mset_poly_rel_minus)
  done

lemma PAC_checker_l_step_PAC_checker_step:
  assumes
    ‹(Ast, Bst) ∈ code_status_status_rel ×⇩r ⟨var_rel⟩set_rel ×⇩r fmap_polys_rel› and
    ‹(st, st') ∈ pac_step_rel› and
    spec: ‹(spec, spec') ∈ sorted_poly_rel O mset_poly_rel›
  shows
    ‹PAC_checker_l_step spec Ast st ≤ ⇓ (code_status_status_rel ×⇩r ⟨var_rel⟩set_rel ×⇩r fmap_polys_rel) (PAC_checker_step spec' Bst st')›
proof -
  obtain A 𝒱 cst B 𝒱' cst' where
   Ast: ‹Ast = (cst, 𝒱, A)› and
   Bst: ‹Bst = (cst', 𝒱', B)› and
   𝒱[intro]: ‹(𝒱, 𝒱') ∈  ⟨var_rel⟩set_rel›  and
   AB: ‹(A, B) ∈ fmap_polys_rel›
     ‹(cst, cst') ∈ code_status_status_rel›
    using assms(1)
    by (cases Ast; cases Bst; auto)
  have [refine]: ‹(r, ra) ∈ sorted_poly_rel O mset_poly_rel ⟹
       (eqa, eqaa)
       ∈ {(st, b). (¬ is_cfailed st ⟷ b) ∧ (is_cfound st ⟶ spec = r)} ⟹
       RETURN eqa
       ≤ ⇓ code_status_status_rel
          (SPEC
            (λst'. (¬ is_failed st' ∧
                   is_found st' ⟶
                    ra - spec' ∈ More_Modules.ideal polynomial_bool)))›
     for r ra eqa eqaa
     using spec
     by (cases eqa)
       (auto intro!: RETURN_RES_refine dest!: sorted_poly_list_relD
         simp: mset_poly_rel_def ideal.span_zero)
  have [simp]: ‹(eqa, st'a) ∈ code_status_status_rel ⟹
       (merge_cstatus cst eqa, merge_status cst' st'a)
       ∈ code_status_status_rel› for eqa st'a
     using AB
     by (cases eqa; cases st'a)
       (auto simp: code_status_status_rel_def)
  have [simp]: ‹(merge_cstatus cst CSUCCESS, cst') ∈ code_status_status_rel›
    using AB
    by (cases st)
      (auto simp: code_status_status_rel_def)
  have [simp]: ‹(x32, x32a) ∈ var_rel ⟹
        ([([x32], -1::int)], -Var x32a) ∈ fully_unsorted_poly_rel O mset_poly_rel› for x32 x32a
   by (auto simp: mset_poly_rel_def fully_unsorted_poly_list_rel_def list_mset_rel_def br_def
         unsorted_term_poly_list_rel_def var_rel_def Const_1_eq_1
       intro!: relcompI[of _ ‹{#({#x32#}, -1 :: int)#}›]
         relcompI[of _ ‹[({#x32#}, -1)]›])
  have H3: ‹p - Var a = (-Var a) + p› for p :: ‹int mpoly› and a
    by auto
  show ?thesis
    using assms(2)
    unfolding PAC_checker_l_step_def PAC_checker_step_def Ast Bst prod.case
    apply (cases st; cases st'; simp only: p2rel_def pac_step.case
      pac_step_rel_raw_def mem_Collect_eq prod.case pac_step_rel_raw.simps)
    subgoal
      apply (refine_rcg normalize_poly_normalize_poly_spec
        check_mult_l_check_mult check_addition_l_check_add
        full_normalize_poly_diff_ideal)
      subgoal using AB by auto
      subgoal using AB by auto
      subgoal by auto
      subgoal by auto
      subgoal by auto
      subgoal by (auto intro: 𝒱)
      apply assumption+
      subgoal
        by (auto simp: code_status_status_rel_def)
      subgoal
        by (auto intro!: fmap_rel_fmupd_fmap_rel
          fmap_rel_fmdrop_fmap_rel AB)
      subgoal using AB by auto
      done
    subgoal
      apply (refine_rcg normalize_poly_normalize_poly_spec
        check_mult_l_check_mult check_addition_l_check_add
        full_normalize_poly_diff_ideal[unfolded normalize_poly_spec_def[symmetric]])
      subgoal using AB by auto
      subgoal using AB by auto
      subgoal using AB by auto
      subgoal by auto
      subgoal by auto
      subgoal by auto
      apply assumption+
      subgoal
        by (auto simp: code_status_status_rel_def)
      subgoal
        by (auto intro!: fmap_rel_fmupd_fmap_rel
          fmap_rel_fmdrop_fmap_rel AB)
      subgoal using AB by auto
      done
    subgoal
      apply (refine_rcg full_normalize_poly_diff_ideal
        check_extension_l_check_extension)
      subgoal using AB by (auto intro!: fully_unsorted_poly_rel_diff[of _ ‹-Var _ :: int mpoly›, unfolded H3[symmetric]] simp: comp_def case_prod_beta)
      subgoal using AB by auto
      subgoal using AB by auto
      subgoal by auto
      subgoal by auto
      subgoal
        by (auto simp: code_status_status_rel_def)
      subgoal
        by (auto simp: AB
          intro!: fmap_rel_fmupd_fmap_rel insert_var_rel_set_rel)
      subgoal
        by (auto simp: code_status_status_rel_def AB
          code_status.is_cfailed_def)
      done
    subgoal
      apply (refine_rcg normalize_poly_normalize_poly_spec
        check_del_l_check_del check_addition_l_check_add
        full_normalize_poly_diff_ideal[unfolded normalize_poly_spec_def[symmetric]])
      subgoal using AB by auto
      subgoal using AB by auto
      subgoal
        by (auto intro!: fmap_rel_fmupd_fmap_rel
          fmap_rel_fmdrop_fmap_rel code_status_status_rel_def AB)
      subgoal
        by (auto intro!: fmap_rel_fmupd_fmap_rel
          fmap_rel_fmdrop_fmap_rel AB)
      done
    done
qed

lemma code_status_status_rel_discrim_iff:
  ‹(x1a, x1c) ∈ code_status_status_rel ⟹ is_cfailed x1a ⟷ is_failed x1c›
  ‹(x1a, x1c) ∈ code_status_status_rel ⟹ is_cfound x1a ⟷ is_found x1c›
  by (cases x1a; cases x1c; auto; fail)+

lemma PAC_checker_l_PAC_checker:
  assumes
    ‹(A, B) ∈ ⟨var_rel⟩set_rel ×⇩r fmap_polys_rel› and
    ‹(st, st') ∈ ⟨pac_step_rel⟩list_rel› and
    ‹(spec, spec') ∈ sorted_poly_rel O mset_poly_rel› and
    ‹(b, b') ∈ code_status_status_rel›
  shows
    ‹PAC_checker_l spec A b st ≤ ⇓ (code_status_status_rel ×⇩r ⟨var_rel⟩set_rel ×⇩r fmap_polys_rel) (PAC_checker spec' B b' st')›
proof -
  have [refine0]: ‹(((b, A), st), (b', B), st') ∈ ((code_status_status_rel ×⇩r ⟨var_rel⟩set_rel ×⇩r fmap_polys_rel) ×⇩r  ⟨pac_step_rel⟩list_rel)›
    using assms by (auto simp: code_status_status_rel_def)
  show ?thesis
    using assms
    unfolding PAC_checker_l_def PAC_checker_def
    apply (refine_rcg PAC_checker_l_step_PAC_checker_step
      WHILEIT_refine[where R = ‹((bool_rel ×⇩r ⟨var_rel⟩set_rel ×⇩r fmap_polys_rel) ×⇩r ⟨pac_step_rel⟩list_rel)›])
    subgoal by (auto simp: code_status_status_rel_discrim_iff)
    subgoal by auto
    subgoal by (auto simp: neq_Nil_conv)
    subgoal by (auto simp: neq_Nil_conv intro!: param_nth)
    subgoal by (auto simp: neq_Nil_conv)
    subgoal by auto
    done
qed

end

lemma in_var_order_rel_iff [code_unfold, no_atp]:
  ‹(v1, v2) ∈ var_order_rel ⟷ List.lexordp (λc1 c2. (of_char c1 :: nat) < of_char c2) v1 v2›
  by (simp add: lexordp_def var_order_rel_def less_char_def [abs_def] p2rel_def)

export_code add_poly_l' in SML module_name test

definition full_checker_l
  :: ‹llist_polynomial ⇒ (nat, llist_polynomial) fmap ⇒ (_, string, nat) pac_step list ⇒
    (string code_status × _) nres›
where
  ‹full_checker_l spec A st = do {
    spec' ← full_normalize_poly spec;
    (b, 𝒱, A) ← remap_polys_l spec' {} A;
    if is_cfailed b
    then RETURN (b, 𝒱, A)
    else do {
      let 𝒱 = 𝒱 ∪ vars_llist spec;
      PAC_checker_l spec' (𝒱, A) b st
    }
  }›


context poly_embed
begin


term normalize_poly_spec
thm full_normalize_poly_diff_ideal[unfolded normalize_poly_spec_def[symmetric]]
abbreviation unsorted_fmap_polys_rel where
  ‹unsorted_fmap_polys_rel ≡ ⟨nat_rel, fully_unsorted_poly_rel O mset_poly_rel⟩fmap_rel›

lemma full_checker_l_full_checker:
 assumes
    ‹(A, B) ∈ unsorted_fmap_polys_rel› and
    ‹(st, st') ∈ ⟨pac_step_rel⟩list_rel› and
    ‹(spec, spec') ∈ fully_unsorted_poly_rel O mset_poly_rel›
  shows
    ‹full_checker_l spec A st ≤ ⇓ (code_status_status_rel ×⇩r ⟨var_rel⟩set_rel ×⇩r fmap_polys_rel) (full_checker spec' B st')›
proof -
  have [refine]:
    ‹(spec, spec') ∈ sorted_poly_rel O mset_poly_rel ⟹
    (𝒱, 𝒱') ∈ ⟨var_rel⟩set_rel ⟹
    remap_polys_l spec 𝒱 A ≤ ⇓(code_status_status_rel ×⇩r ⟨var_rel⟩set_rel ×⇩r fmap_polys_rel)
        (remap_polys_change_all spec' 𝒱' B)› for spec spec' 𝒱 𝒱'
    apply (rule remap_polys_l_remap_polys[THEN order_trans, OF assms(1)])
    apply assumption+
    apply (rule ref_two_step[OF order.refl])
    apply(rule remap_polys_spec[THEN order_trans])
    by (rule remap_polys_polynomial_bool_remap_polys_change_all)

  show ?thesis
    unfolding full_checker_l_def full_checker_def
    apply (refine_rcg remap_polys_l_remap_polys
       full_normalize_poly_diff_ideal[unfolded normalize_poly_spec_def[symmetric]]
       PAC_checker_l_PAC_checker)
    subgoal
      using assms(3) .
    subgoal by auto
    subgoal by (auto simp: is_cfailed_def is_failed_def)
    subgoal by auto
    apply (rule fully_unsorted_poly_rel_extend_vars)
    subgoal using assms(3) .
    subgoal by auto
    subgoal by auto
    subgoal
      using assms(2) by (auto simp: p2rel_def)
    subgoal by auto
    done
qed


lemma full_checker_l_full_checker':
  ‹(uncurry2 full_checker_l, uncurry2 full_checker) ∈
  ((fully_unsorted_poly_rel O mset_poly_rel) ×⇩r unsorted_fmap_polys_rel) ×⇩r ⟨pac_step_rel⟩list_rel →⇩f
    ⟨(code_status_status_rel ×⇩r ⟨var_rel⟩set_rel ×⇩r fmap_polys_rel)⟩nres_rel›
  apply (intro frefI nres_relI)
  using full_checker_l_full_checker by force

end

definition remap_polys_l2 :: ‹llist_polynomial ⇒ string set ⇒ (nat, llist_polynomial) fmap ⇒ _ nres› where
  ‹remap_polys_l2 spec = (λ𝒱 A. do{
   n ← upper_bound_on_dom A;
   b ← RETURN (n ≥ 2^64);
   if b
   then do {
     c ← remap_polys_l_dom_err;
     RETURN (error_msg (0 ::nat) c, 𝒱, fmempty)
   }
   else do {
       (b, 𝒱, A) ← nfoldli ([0..<n]) (λ_. True)
       (λi (b, 𝒱, A').
          if i ∈# dom_m A
          then do {
            ASSERT(fmlookup A i ≠ None);
            p ← full_normalize_poly (the (fmlookup A i));
            eq ← weak_equality_l p spec;
            𝒱 ← RETURN (𝒱 ∪ vars_llist (the (fmlookup A i)));
            RETURN(b ∨ eq, 𝒱, fmupd i p A')
          } else RETURN (b, 𝒱, A')
        )
       (False, 𝒱, fmempty);
     RETURN (if b then CFOUND else CSUCCESS, 𝒱, A)
    }
 })›

lemma remap_polys_l2_remap_polys_l:
  ‹remap_polys_l2 spec 𝒱 A ≤ ⇓ Id (remap_polys_l spec 𝒱 A)›
proof -
  have [refine]: ‹(A, A') ∈ Id ⟹ upper_bound_on_dom A
    ≤ ⇓ {(n, dom). dom = set [0..<n]} (SPEC (λdom. set_mset (dom_m A') ⊆ dom ∧ finite dom))› for A A'
    unfolding upper_bound_on_dom_def
    apply (rule RES_refine)
    apply (auto simp: upper_bound_on_dom_def)
    done
  have 1: ‹inj_on id dom› for dom
    by auto
  have 2: ‹x ∈# dom_m A ⟹
       x' ∈# dom_m A' ⟹
       (x, x') ∈ nat_rel ⟹
       (A, A') ∈ Id ⟹
       full_normalize_poly (the (fmlookup A x))
       ≤ ⇓ Id
          (full_normalize_poly (the (fmlookup A' x')))›
       for A A' x x'
       by (auto)
  have 3: ‹(n, dom) ∈ {(n, dom). dom = set [0..<n]} ⟹
       ([0..<n], dom) ∈ ⟨nat_rel⟩list_set_rel› for n dom
  by (auto simp: list_set_rel_def br_def)
  have 4: ‹(p,q) ∈ Id ⟹
    weak_equality_l p spec ≤ ⇓Id (weak_equality_l q spec)› for p q spec
    by auto

  have 6: ‹a = b ⟹ (a, b) ∈ Id› for a b
    by auto
  show ?thesis
    unfolding remap_polys_l2_def remap_polys_l_def
    apply (refine_rcg LFO_refine[where R= ‹Id ×⇩r ⟨Id⟩set_rel ×⇩r Id›])
    subgoal by auto
    subgoal by auto
    subgoal by auto
    apply (rule 3)
    subgoal by auto
    subgoal by (simp add: in_dom_m_lookup_iff)
    subgoal by (simp add: in_dom_m_lookup_iff)
    apply (rule 2)
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal by auto
    apply (rule 4; assumption)
    apply (rule 6)
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal by auto
    done
qed

end