diff --git a/thys/PAC_Checker/PAC_Checker.thy b/thys/PAC_Checker/PAC_Checker.thy
--- a/thys/PAC_Checker/PAC_Checker.thy
+++ b/thys/PAC_Checker/PAC_Checker.thy
@@ -1,1381 +1,1382 @@
 (*
   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
 begin
 
 section \<open>Executable Checker\<close>
 
 text \<open>In this layer we finally refine the checker to executable code.\<close>
 
 subsection \<open>Definitions\<close>
 
 text \<open>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).
 \<close>
 
 paragraph \<open>Extended error message\<close>
 
 datatype 'a code_status =
   is_cfailed: CFAILED (the_error: 'a) |
   CSUCCESS |
   is_cfound: CFOUND
 
 text \<open>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.
 \<close>
 fun merge_cstatus where
   \<open>merge_cstatus (CFAILED a) _ = CFAILED a\<close> |
   \<open>merge_cstatus _ (CFAILED a) = CFAILED a\<close> |
   \<open>merge_cstatus CFOUND _ = CFOUND\<close> |
   \<open>merge_cstatus _ CFOUND = CFOUND\<close> |
   \<open>merge_cstatus _ _ = CSUCCESS\<close>
 
 definition code_status_status_rel :: \<open>('a code_status \<times> status) set\<close> where
 \<open>code_status_status_rel =
   {(CFOUND, FOUND), (CSUCCESS, SUCCESS)} \<union>
   {(CFAILED a, FAILED)| a. True}\<close>
 
 lemma in_code_status_status_rel_iff[simp]:
   \<open>(CFOUND, b) \<in> code_status_status_rel \<longleftrightarrow> b = FOUND\<close>
   \<open>(a, FOUND) \<in> code_status_status_rel \<longleftrightarrow> a = CFOUND\<close>
   \<open>(CSUCCESS, b) \<in> code_status_status_rel \<longleftrightarrow> b = SUCCESS\<close>
   \<open>(a, SUCCESS) \<in> code_status_status_rel \<longleftrightarrow> a = CSUCCESS\<close>
   \<open>(a, FAILED) \<in> code_status_status_rel \<longleftrightarrow> is_cfailed a\<close>
   \<open>(CFAILED C, b) \<in> code_status_status_rel \<longleftrightarrow> b = FAILED\<close>
   by (cases a; cases b; auto simp: code_status_status_rel_def; fail)+
 
 
 paragraph \<open>Refinement relation\<close>
 
 fun pac_step_rel_raw :: \<open>('olbl \<times> 'lbl) set \<Rightarrow> ('a \<times> 'b) set \<Rightarrow> ('c \<times> 'd) set \<Rightarrow> ('a, 'c, 'olbl) pac_step \<Rightarrow> ('b, 'd, 'lbl) pac_step \<Rightarrow> bool\<close> where
 \<open>pac_step_rel_raw R1 R2 R3 (Add p1 p2 i r) (Add p1' p2' i' r') \<longleftrightarrow>
    (p1, p1') \<in> R1 \<and> (p2, p2') \<in> R1 \<and> (i, i') \<in> R1 \<and>
    (r, r') \<in> R2\<close> |
 \<open>pac_step_rel_raw R1 R2 R3 (Mult p1 p2 i r) (Mult p1' p2' i' r') \<longleftrightarrow>
    (p1, p1') \<in> R1 \<and> (p2, p2') \<in> R2 \<and> (i, i') \<in> R1 \<and>
    (r, r') \<in> R2\<close> |
 \<open>pac_step_rel_raw R1 R2 R3 (Del p1) (Del p1') \<longleftrightarrow>
    (p1, p1') \<in> R1\<close> |
 \<open>pac_step_rel_raw R1 R2 R3 (Extension i x p1) (Extension j x' p1') \<longleftrightarrow>
    (i, j) \<in> R1 \<and> (x, x') \<in> R3 \<and> (p1, p1') \<in> R2\<close> |
 \<open>pac_step_rel_raw R1 R2 R3 _ _ \<longleftrightarrow> False\<close>
 
 fun pac_step_rel_assn :: \<open>('olbl \<Rightarrow> 'lbl \<Rightarrow> assn) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> assn) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> assn) \<Rightarrow> ('a, 'c, 'olbl) pac_step \<Rightarrow> ('b, 'd, 'lbl) pac_step \<Rightarrow> assn\<close> where
 \<open>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'\<close> |
 \<open>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'\<close> |
 \<open>pac_step_rel_assn R1 R2 R3 (Del p1) (Del p1') =
    R1 p1 p1'\<close> |
 \<open>pac_step_rel_assn R1 R2 R3 (Extension i x p1) (Extension i' x' p1') =
    R1 i i' * R3 x x' * R2 p1 p1'\<close> |
 \<open>pac_step_rel_assn R1 R2 _ _ _ = false\<close>
 
 lemma pac_step_rel_assn_alt_def:
   \<open>pac_step_rel_assn R1 R2 R3 x y = (
   case (x, y) of
       (Add p1 p2 i r, Add p1' p2' i' r') \<Rightarrow>
         R1 p1 p1' * R1 p2 p2' * R1 i i' * R2 r r'
     | (Mult p1 p2 i r, Mult p1' p2' i' r') \<Rightarrow>
         R1 p1 p1' * R2 p2 p2' * R1 i i' * R2 r r'
     | (Del p1, Del p1') \<Rightarrow> R1 p1 p1'
     | (Extension i x p1, Extension i' x' p1') \<Rightarrow> R1 i i' * R3 x x' * R2 p1 p1'
     | _ \<Rightarrow> false)\<close>
     by (auto split: pac_step.splits)
 
 
 paragraph \<open>Addition checking\<close>
 
 definition error_msg where
   \<open>error_msg i msg = CFAILED (''s CHECKING failed at line '' @ show i @ '' with error '' @ msg)\<close>
 
 definition error_msg_notin_dom_err where
   \<open>error_msg_notin_dom_err = '' notin domain''\<close>
 
 definition error_msg_notin_dom :: \<open>nat \<Rightarrow> string\<close> where
   \<open>error_msg_notin_dom i = show i @ error_msg_notin_dom_err\<close>
 
 definition error_msg_reused_dom where
   \<open>error_msg_reused_dom i = show i @ '' already in domain''\<close>
 
 
 definition error_msg_not_equal_dom where
   \<open>error_msg_not_equal_dom p q pq r = show p @ '' + '' @ show q @ '' = '' @ show pq @ '' not equal'' @ show r\<close>
 
 
 definition check_not_equal_dom_err :: \<open>llist_polynomial \<Rightarrow> llist_polynomial \<Rightarrow> llist_polynomial \<Rightarrow> llist_polynomial \<Rightarrow> string nres\<close> where
   \<open>check_not_equal_dom_err p q pq r = SPEC (\<lambda>_. True)\<close>
 
 
 definition vars_llist :: \<open>llist_polynomial \<Rightarrow> string set\<close> where
 \<open>vars_llist  xs = \<Union>(set ` fst ` set xs)\<close>
 
 
 definition check_addition_l :: \<open>_ \<Rightarrow> _ \<Rightarrow> string set \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> llist_polynomial \<Rightarrow> string code_status nres\<close> where
 \<open>check_addition_l spec A \<V> p q i r = do {
    let b = p \<in># dom_m A \<and> q \<in># dom_m A \<and> i \<notin># dom_m A \<and> vars_llist r \<subseteq> \<V>;
    if \<not>b
    then RETURN (error_msg i ((if p \<notin># dom_m A then error_msg_notin_dom p else []) @ (if q \<notin># dom_m A then error_msg_notin_dom p else []) @
       (if i \<in># dom_m A then error_msg_reused_dom p else [])))
    else do {
      ASSERT (p \<in># dom_m A);
      let p = the (fmlookup A p);
      ASSERT (q \<in># dom_m A);
      let q = the (fmlookup A q);
      pq \<leftarrow> add_poly_l (p, q);
      b \<leftarrow> weak_equality_l pq r;
      b' \<leftarrow> weak_equality_l r spec;
      if b then (if b' then RETURN CFOUND else RETURN CSUCCESS)
      else do {
        c \<leftarrow> check_not_equal_dom_err p q pq r;
        RETURN (error_msg i c)}
    }
 }\<close>
 
 
 paragraph \<open>Multiplication checking\<close>
 
 definition check_mult_l_dom_err :: \<open>bool \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> nat \<Rightarrow> string nres\<close> where
   \<open>check_mult_l_dom_err p_notin p i_already i = SPEC (\<lambda>_. True)\<close>
 
 
 definition check_mult_l_mult_err :: \<open>llist_polynomial \<Rightarrow> llist_polynomial \<Rightarrow> llist_polynomial \<Rightarrow> llist_polynomial \<Rightarrow> string nres\<close> where
   \<open>check_mult_l_mult_err p q pq r = SPEC (\<lambda>_. True)\<close>
 
 
 definition check_mult_l :: \<open>_ \<Rightarrow> _ \<Rightarrow> _ \<Rightarrow> nat \<Rightarrow>llist_polynomial \<Rightarrow>  nat \<Rightarrow> llist_polynomial \<Rightarrow> string code_status nres\<close> where
 \<open>check_mult_l spec A \<V> p q i r = do {
     let b = p \<in># dom_m A \<and> i \<notin># dom_m A \<and> vars_llist q \<subseteq> \<V>\<and> vars_llist r \<subseteq> \<V>;
     if \<not>b
     then do {
       c \<leftarrow> check_mult_l_dom_err (p \<notin># dom_m A) p (i \<in># dom_m A) i;
       RETURN (error_msg i c)}
     else do {
        ASSERT (p \<in># dom_m A);
        let p = the (fmlookup A p);
        pq \<leftarrow> mult_poly_full p q;
        b \<leftarrow> weak_equality_l pq r;
        b' \<leftarrow> weak_equality_l r spec;
        if b then (if b' then RETURN CFOUND else RETURN CSUCCESS) else do {
          c \<leftarrow> check_mult_l_mult_err p q pq r;
          RETURN (error_msg i c)
        }
      }
   }\<close>
 
 
 paragraph \<open>Deletion checking\<close>
 
 definition check_del_l :: \<open>_ \<Rightarrow> _ \<Rightarrow> nat \<Rightarrow> string code_status nres\<close> where
 \<open>check_del_l spec A p = RETURN CSUCCESS\<close>
 
 
 paragraph \<open>Extension checking\<close>
 
 definition check_extension_l_dom_err :: \<open>nat \<Rightarrow> string nres\<close> where
   \<open>check_extension_l_dom_err p = SPEC (\<lambda>_. True)\<close>
 
 
 definition check_extension_l_no_new_var_err :: \<open>llist_polynomial \<Rightarrow> string nres\<close> where
   \<open>check_extension_l_no_new_var_err p = SPEC (\<lambda>_. True)\<close>
 
 definition check_extension_l_new_var_multiple_err :: \<open>string \<Rightarrow> llist_polynomial \<Rightarrow> string nres\<close> where
   \<open>check_extension_l_new_var_multiple_err v p = SPEC (\<lambda>_. True)\<close>
 
 definition check_extension_l_side_cond_err
   :: \<open>string \<Rightarrow> llist_polynomial \<Rightarrow> llist_polynomial \<Rightarrow> llist_polynomial \<Rightarrow> string nres\<close>
 where
   \<open>check_extension_l_side_cond_err v p p' q = SPEC (\<lambda>_. True)\<close>
 
 definition check_extension_l
   :: \<open>_ \<Rightarrow> _ \<Rightarrow> string set \<Rightarrow> nat \<Rightarrow> string \<Rightarrow> llist_polynomial \<Rightarrow> (string code_status) nres\<close>
 where
 \<open>check_extension_l spec A \<V> i v p = do {
   let b = i \<notin># dom_m A \<and> v \<notin> \<V> \<and> ([v], -1) \<in> set p;
   if \<not>b
   then do {
     c \<leftarrow> check_extension_l_dom_err i;
     RETURN (error_msg i c)
   } else do {
       let p' = remove1 ([v], -1) p;
       let b = vars_llist p' \<subseteq> \<V>;
       if \<not>b
       then do {
         c \<leftarrow> check_extension_l_new_var_multiple_err v p';
         RETURN (error_msg i c)
       }
       else do {
          p2 \<leftarrow> mult_poly_full p' p';
          let p' = map (\<lambda>(a,b). (a, -b)) p';
          q \<leftarrow> add_poly_l (p2, p');
          eq \<leftarrow> weak_equality_l q [];
          if eq then do {
            RETURN (CSUCCESS)
          } else do {
           c \<leftarrow> check_extension_l_side_cond_err v p p' q;
           RETURN (error_msg i c)
         }
       }
     }
   }\<close>
 
 
 lemma check_extension_alt_def:
   \<open>check_extension A \<V> i v p \<ge> do {
     b \<leftarrow> SPEC(\<lambda>b. b \<longrightarrow> i \<notin># dom_m A \<and> v \<notin> \<V>);
     if \<not>b
     then RETURN (False)
     else do {
          p' \<leftarrow> RETURN (p + Var v);
          b \<leftarrow> SPEC(\<lambda>b. b \<longrightarrow> vars p' \<subseteq> \<V>);
          if \<not>b
          then RETURN (False)
          else do {
            pq \<leftarrow> mult_poly_spec p' p';
            let p' = - p';
            p \<leftarrow> add_poly_spec pq p';
            eq \<leftarrow> weak_equality p 0;
            if eq then RETURN(True)
            else RETURN (False)
        }
      }
    }\<close>
 proof -
   have [intro]: \<open>ab \<notin> \<V> \<Longrightarrow>
        vars ba \<subseteq> \<V> \<Longrightarrow>
        MPoly_Type.coeff (ba + Var ab) (monomial (Suc 0) ab) = 1\<close> 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\<^sub>0_def lookup_single_eq monom.rep_eq)
   have [simp]: \<open>MPoly_Type.coeff p (monomial (Suc 0) ab) = -1\<close>
      if \<open>vars (p + Var ab) \<subseteq> \<V>\<close>
        \<open>ab \<notin> \<V>\<close>
      for ab
    proof -
      define q where \<open>q \<equiv> p + Var ab\<close>
      then have p: \<open>p = q - Var ab\<close>
        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\<^sub>0_def simp flip: monom.abs_eq
            simp: not_in_vars_coeff0 MPoly_Type.coeff_def
            Var.abs_eq Var\<^sub>0_def lookup_single_eq monom.rep_eq)
   qed
   have [simp]: \<open>vars (p - Var ab) = vars (Var ab - p)\<close> for ab
     using vars_uminus[of \<open>p - Var ab\<close>]
     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: \<open>RES A \<bind> (\<lambda>T. RES (f T)) = RES (\<Union>(f ` A))\<close>
   by (auto simp: pw_eq_iff refine_pw_simps)
 
 
 lemma check_add_alt_def:
   \<open>check_add A \<V> p q i r \<ge>
     do {
      b \<leftarrow> SPEC(\<lambda>b. b \<longrightarrow> p \<in># dom_m A \<and> q \<in># dom_m A \<and> i \<notin># dom_m A \<and> vars r \<subseteq> \<V>);
      if \<not>b
      then RETURN False
      else do {
        ASSERT (p \<in># dom_m A);
        let p = the (fmlookup A p);
        ASSERT (q \<in># dom_m A);
        let q = the (fmlookup A q);
        pq \<leftarrow> add_poly_spec p q;
        eq \<leftarrow> weak_equality pq r;
        RETURN eq
      }
   }\<close> (is \<open>_ \<ge> ?A\<close>)
 proof -
   have check_add_alt_def: \<open>check_add A \<V> p q i r = do {
      b \<leftarrow> SPEC(\<lambda>b. b \<longrightarrow> p \<in># dom_m A \<and> q \<in># dom_m A \<and> i \<notin># dom_m A \<and> vars r \<subseteq> \<V>);
      if \<not>b then SPEC(\<lambda>b. b \<longrightarrow> p \<in># dom_m A \<and> q \<in># dom_m A \<and> i \<notin># dom_m A \<and> vars r \<subseteq> \<V> \<and>
             the (fmlookup A p) + the (fmlookup A q) - r \<in>  ideal polynomial_bool)
      else
        SPEC(\<lambda>b. b \<longrightarrow> p \<in># dom_m A \<and> q \<in># dom_m A \<and> i \<notin># dom_m A \<and> vars r \<subseteq> \<V> \<and>
             the (fmlookup A p) + the (fmlookup A q) - r \<in>  ideal polynomial_bool)}\<close>
    (is \<open>_ = ?B\<close>)
     by (auto simp: check_add_def RES_RES_RETURN_RES)
    have \<open>?A \<le> \<Down> Id (check_add A \<V> p q i r)\<close>
      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:
   \<open>check_mult A \<V> p q i r \<ge>
     do {
      b \<leftarrow> SPEC(\<lambda>b. b \<longrightarrow> p \<in># dom_m A \<and> i \<notin># dom_m A \<and> vars q \<subseteq> \<V>  \<and> vars r \<subseteq> \<V>);
      if \<not>b
      then RETURN False
      else do {
        ASSERT (p \<in># dom_m A);
        let p = the (fmlookup A p);
        pq \<leftarrow> mult_poly_spec p q;
        p \<leftarrow> weak_equality pq r;
        RETURN p
      }
   }\<close>
   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 _ \<open>the (fmlookup A p) * q\<close>])
 
 primrec insort_key_rel :: "('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'b \<Rightarrow> 'b list \<Rightarrow> '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]: \<open>set (insort_key_rel R x xs) = insert x (set xs)\<close>
   by (induction xs)
    auto
 
 lemma sorted_wrt_insort_key_rel:
    \<open>total_on R (insert x (set xs)) \<Longrightarrow> transp R \<Longrightarrow> reflp R \<Longrightarrow>
     sorted_wrt R xs \<Longrightarrow> sorted_wrt R (insort_key_rel R x xs)\<close>
   by (induction xs)
    (auto dest: transpD reflpD simp: Restricted_Predicates.total_on_def)
 
 lemma sorted_wrt_insort_key_rel2:
    \<open>total_on R (insert x (set xs)) \<Longrightarrow> transp R \<Longrightarrow> x \<notin> set xs \<Longrightarrow>
     sorted_wrt R xs \<Longrightarrow> sorted_wrt R (insort_key_rel R x xs)\<close>
   by (induction xs)
    (auto dest: transpD simp: Restricted_Predicates.total_on_def in_mono)
 
 
 paragraph \<open>Step checking\<close>
 
 definition PAC_checker_l_step ::  \<open>_ \<Rightarrow> string code_status \<times> string set \<times> _ \<Rightarrow> (llist_polynomial, string, nat) pac_step \<Rightarrow> _\<close> where
   \<open>PAC_checker_l_step = (\<lambda>spec (st', \<V>, A) st. case st of
      Add _ _ _ _ \<Rightarrow>
        do {
          r \<leftarrow> full_normalize_poly (pac_res st);
         eq \<leftarrow> check_addition_l spec A \<V> (pac_src1 st) (pac_src2 st) (new_id st) r;
         let _ = eq;
         if \<not>is_cfailed eq
         then RETURN (merge_cstatus st' eq,
           \<V>, fmupd (new_id st) r A)
         else RETURN (eq, \<V>, A)
    }
    | Del _ \<Rightarrow>
        do {
         eq \<leftarrow> check_del_l spec A (pac_src1 st);
         let _ = eq;
         if \<not>is_cfailed eq
         then RETURN (merge_cstatus st' eq, \<V>, fmdrop (pac_src1 st) A)
         else RETURN (eq, \<V>, A)
    }
    | Mult _ _ _ _ \<Rightarrow>
        do {
          r \<leftarrow> full_normalize_poly (pac_res st);
          q \<leftarrow> full_normalize_poly (pac_mult st);
         eq \<leftarrow> check_mult_l spec A \<V> (pac_src1 st) q (new_id st) r;
         let _ = eq;
         if \<not>is_cfailed eq
         then RETURN (merge_cstatus st' eq,
           \<V>, fmupd (new_id st) r A)
         else RETURN (eq, \<V>, A)
    }
    | Extension _ _ _ \<Rightarrow>
        do {
          r \<leftarrow> full_normalize_poly (([new_var st], -1) # (pac_res st));
         (eq) \<leftarrow> check_extension_l spec A \<V> (new_id st) (new_var st) r;
         if \<not>is_cfailed eq
         then do {
           RETURN (st',
             insert (new_var st) \<V>, fmupd (new_id st) r A)}
         else RETURN (eq, \<V>, A)
    }
  )\<close>
 
 lemma pac_step_rel_raw_def:
   \<open>\<langle>K, V, R\<rangle> pac_step_rel_raw = pac_step_rel_raw K V R\<close>
   by (auto intro!: ext simp: relAPP_def)
 
 definition mononoms_equal_up_to_reorder where
   \<open>mononoms_equal_up_to_reorder xs ys \<longleftrightarrow>
      map (\<lambda>(a, b).  (mset a, b)) xs = map (\<lambda>(a, b). (mset a, b)) ys\<close>
 
 
  definition normalize_poly_l where
   \<open>normalize_poly_l p = SPEC (\<lambda>p'.
      normalize_poly_p\<^sup>*\<^sup>* ((\<lambda>(a, b). (mset a, b)) `# mset p) ((\<lambda>(a, b). (mset a, b)) `# mset p') \<and>
      0 \<notin># snd `# mset p' \<and>
      sorted_wrt (rel2p (term_order_rel \<times>\<^sub>r int_rel)) p' \<and>
      (\<forall> x \<in> mononoms p'. sorted_wrt (rel2p var_order_rel) x))\<close>
 
 
 definition remap_polys_l_dom_err :: \<open>string nres\<close> where
   \<open>remap_polys_l_dom_err = SPEC (\<lambda>_. True)\<close>
 
 
 definition remap_polys_l :: \<open>llist_polynomial \<Rightarrow> string set \<Rightarrow> (nat, llist_polynomial) fmap \<Rightarrow>
    (_ code_status \<times> string set \<times> (nat, llist_polynomial) fmap) nres\<close> where
   \<open>remap_polys_l spec = (\<lambda>\<V> A. do{
    dom \<leftarrow> SPEC(\<lambda>dom. set_mset (dom_m A) \<subseteq> dom \<and> finite dom);
    failed \<leftarrow> SPEC(\<lambda>_::bool. True);
    if failed
    then do {
       c \<leftarrow> remap_polys_l_dom_err;
       RETURN (error_msg (0 :: nat) c, \<V>, fmempty)
    }
    else do {
      (b, \<V>, A) \<leftarrow> FOREACH dom
        (\<lambda>i (b, \<V>,  A').
           if i \<in># dom_m A
           then  do {
             p \<leftarrow> full_normalize_poly (the (fmlookup A i));
             eq \<leftarrow> weak_equality_l p spec;
             \<V> \<leftarrow> RETURN(\<V> \<union> vars_llist (the (fmlookup A i)));
             RETURN(b \<or> eq, \<V>, fmupd i p A')
           } else RETURN (b, \<V>, A'))
        (False, \<V>, fmempty);
      RETURN (if b then CFOUND else CSUCCESS, \<V>, A)
  }})\<close>
 
 definition PAC_checker_l where
   \<open>PAC_checker_l spec A b st = do {
     (S, _) \<leftarrow> WHILE\<^sub>T
        (\<lambda>((b, A), n). \<not>is_cfailed b \<and> n \<noteq> [])
        (\<lambda>((bA), n). do {
           ASSERT(n \<noteq> []);
           S \<leftarrow> PAC_checker_l_step spec bA (hd n);
           RETURN (S, tl n)
         })
       ((b, A), st);
     RETURN S
   }\<close>
 
 
 subsection \<open>Correctness\<close>
 
 text \<open>We now enter the locale to reason about polynomials directly.\<close>
 
 context poly_embed
 begin
 
 abbreviation pac_step_rel where
   \<open>pac_step_rel \<equiv> p2rel (\<langle>Id, fully_unsorted_poly_rel O mset_poly_rel, var_rel\<rangle> pac_step_rel_raw)\<close>
 
 abbreviation fmap_polys_rel where
   \<open>fmap_polys_rel \<equiv> \<langle>nat_rel, sorted_poly_rel O mset_poly_rel\<rangle>fmap_rel\<close>
 
 lemma
   \<open>normalize_poly_p s0 s \<Longrightarrow>
         (s0, p) \<in> mset_poly_rel \<Longrightarrow>
         (s, p) \<in> mset_poly_rel\<close>
   by (auto simp: mset_poly_rel_def normalize_poly_p_poly_of_mset)
 
 lemma vars_poly_of_vars:
   \<open>vars (poly_of_vars a :: int mpoly) \<subseteq> (\<phi> ` set_mset a)\<close>
   by (induction a)
    (auto simp: vars_mult_Var)
 
 lemma vars_polynomial_of_mset:
   \<open>vars (polynomial_of_mset za) \<subseteq> \<Union>(image \<phi> ` (set_mset o fst) ` set_mset za)\<close>
   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:
   \<open>(A, B) \<in> fully_unsorted_poly_rel O mset_poly_rel \<Longrightarrow> vars B \<subseteq> \<phi> ` vars_llist A\<close>
   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 \<open>mset _\<close> \<open>add_mset _ _\<close> set_mset])
 
 lemma fully_unsorted_poly_rel_extend_vars:
   \<open>(A, B) \<in> fully_unsorted_poly_rel O mset_poly_rel \<Longrightarrow>
   (x1c, x1a) \<in> \<langle>var_rel\<rangle>set_rel \<Longrightarrow>
    RETURN (x1c \<union> vars_llist A)
     \<le> \<Down> (\<langle>var_rel\<rangle>set_rel)
        (SPEC ((\<subseteq>) (x1a \<union> vars (B))))\<close>
   using fully_unsorted_poly_rel_vars_subset_vars_llist[of A B]
   apply (subst RETURN_RES_refine_iff)
   apply clarsimp
   apply (rule exI[of _ \<open>x1a \<union> \<phi> ` vars_llist A\<close>])
   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: \<open>(A, B) \<in> \<langle>nat_rel, fully_unsorted_poly_rel O mset_poly_rel\<rangle>fmap_rel\<close> and
     spec: \<open>(spec, spec') \<in> sorted_poly_rel O mset_poly_rel\<close> and
     V: \<open>(\<V>, \<V>') \<in> \<langle>var_rel\<rangle>set_rel\<close>
   shows \<open>remap_polys_l spec \<V> A \<le>
      \<Down>(code_status_status_rel \<times>\<^sub>r \<langle>var_rel\<rangle>set_rel \<times>\<^sub>r fmap_polys_rel) (remap_polys spec' \<V>' B)\<close>
   (is \<open>_ \<le> \<Down> ?R _\<close>)
 proof -
   have 1: \<open>inj_on id (dom :: nat set)\<close> for dom
     by auto
   have H: \<open>x \<in># dom_m A \<Longrightarrow>
      (\<And>p. (the (fmlookup A x), p) \<in> fully_unsorted_poly_rel \<Longrightarrow>
        (p, the (fmlookup B x)) \<in> mset_poly_rel \<Longrightarrow> thesis) \<Longrightarrow>
      thesis\<close> 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: \<open>full_normalize_poly (the (fmlookup A x))
        \<le> \<Down> (sorted_poly_rel O mset_poly_rel)
           (SPEC
             (\<lambda>p. the (fmlookup B x') - p \<in> More_Modules.ideal polynomial_bool \<and>
                  vars p \<subseteq> vars (the (fmlookup B x'))))\<close>
       if x_dom: \<open>x \<in># dom_m A\<close> and \<open>(x, x') \<in> Id\<close> 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': \<open>(p, pa) \<in> sorted_poly_rel O mset_poly_rel \<Longrightarrow>
      weak_equality_l p spec \<le> SPEC (\<lambda>eqa. eqa \<longrightarrow> pa = spec')\<close> 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: \<open>(\<V>, \<V>') \<in> \<langle>var_rel\<rangle>set_rel \<Longrightarrow>
     ((False, \<V>, fmempty), False, \<V>', fmempty) \<in> bool_rel \<times>\<^sub>r \<langle>var_rel\<rangle>set_rel \<times>\<^sub>r fmap_polys_rel\<close> for \<V> \<V>'
     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:
   \<open>(uncurry f, uncurry g) \<in> [P]\<^sub>f A \<rightarrow> \<langle>B\<rangle>nres_rel \<Longrightarrow>
      (\<And>x x' y y'. P (x', y') \<Longrightarrow> ((x, y), (x', y')) \<in> A \<Longrightarrow> f x y \<le> \<Down> B (g x' y'))\<close>
   unfolding fref_def uncurry_def nres_rel_def
   by auto
 
 lemma weak_equality_spec_weak_equality:
   \<open>(p, p') \<in> mset_poly_rel \<Longrightarrow>
     (r, r') \<in> mset_poly_rel \<Longrightarrow>
     weak_equality_spec p r \<le> weak_equality p' r'\<close>
   unfolding weak_equality_spec_def weak_equality_def
   by (auto simp: mset_poly_rel_def)
 
 
 lemma weak_equality_l_weak_equality_l'[refine]:
   \<open>weak_equality_l p q \<le> \<Down> bool_rel (weak_equality p' q')\<close>
   if \<open>(p, p') \<in> sorted_poly_rel O mset_poly_rel\<close>
     \<open>(q, q') \<in> sorted_poly_rel O mset_poly_rel\<close>
   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]:
   \<open>error_msg i m \<noteq> CSUCCESS\<close>
   \<open>error_msg i m \<noteq> CFOUND\<close>
   \<open>is_cfailed (error_msg i m)\<close>
   \<open>\<not>is_cfound (error_msg i m)\<close>
   by (auto simp: error_msg_def)
 
 lemma sorted_poly_rel_vars_llist:
   \<open>(r, r') \<in> sorted_poly_rel O mset_poly_rel \<Longrightarrow>
    vars r' \<subseteq> \<phi> ` vars_llist r\<close>
   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 _ \<open>mset _\<close>]
       list_rel_split_right_iff list_rel_append2 list_rel_split_left_iff
       dest: arg_cong[of \<open>mset _\<close> \<open>add_mset _ _\<close> set_mset])
     done
 
 
 lemma check_addition_l_check_add:
   assumes \<open>(A, B) \<in> fmap_polys_rel\<close> and \<open>(r, r') \<in> sorted_poly_rel O mset_poly_rel\<close>
     \<open>(p, p') \<in> Id\<close> \<open>(q, q') \<in> Id\<close> \<open>(i, i') \<in> nat_rel\<close>
     \<open>(\<V>', \<V>) \<in> \<langle>var_rel\<rangle>set_rel\<close>
   shows
     \<open>check_addition_l spec A \<V>' p q i r \<le> \<Down> {(st, b). (\<not>is_cfailed st \<longleftrightarrow> b) \<and>
        (is_cfound st \<longrightarrow> spec = r)} (check_add B \<V> p' q' i' r')\<close>
 proof -
   have [refine]:
     \<open>add_poly_l (p, q) \<le> \<Down> (sorted_poly_rel O mset_poly_rel) (add_poly_spec p' q')\<close>
     if \<open>(p, p') \<in> sorted_poly_rel O mset_poly_rel\<close>
       \<open>(q, q') \<in> sorted_poly_rel O mset_poly_rel\<close>
     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:
   \<open>(A, B) \<in> fmap_polys_rel \<Longrightarrow> (x3, x3a) \<in> Id \<Longrightarrow> check_del_l spec A (pac_src1 (Del x3))
     \<le> \<Down> {(st, b). (\<not>is_cfailed st \<longleftrightarrow> b) \<and> (b \<longrightarrow> st = CSUCCESS)} (check_del B (pac_src1 (Del x3a)))\<close>
   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 \<open>(A, B) \<in> fmap_polys_rel\<close> and \<open>(r, r') \<in> sorted_poly_rel O mset_poly_rel\<close> and
     \<open>(q, q') \<in> sorted_poly_rel O mset_poly_rel\<close>
     \<open>(p, p') \<in> Id\<close> \<open>(i, i') \<in> nat_rel\<close> \<open>(\<V>, \<V>') \<in> \<langle>var_rel\<rangle>set_rel\<close>
   shows
     \<open>check_mult_l spec A \<V> p q i r \<le> \<Down>  {(st, b). (\<not>is_cfailed st \<longleftrightarrow> b) \<and>
        (is_cfound st \<longrightarrow> spec = r)} (check_mult B \<V>' p' q' i' r')\<close>
 proof -
   have [refine]:
     \<open>mult_poly_full p q \<le> \<Down> (sorted_poly_rel O mset_poly_rel) (mult_poly_spec p' q')\<close>
     if \<open>(p, p') \<in> sorted_poly_rel O mset_poly_rel\<close>
       \<open>(q, q') \<in> sorted_poly_rel O mset_poly_rel\<close>
     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 \<open>(r, t) \<in> unsorted_poly_rel O mset_poly_rel\<close>
   shows
     \<open>normalize_poly r \<le> \<Down>(sorted_poly_rel O mset_poly_rel) (normalize_poly_spec t)\<close>
 proof -
   obtain s where
     rs: \<open>(r, s) \<in> unsorted_poly_rel\<close> and
     st: \<open>(s, t) \<in> mset_poly_rel\<close>
     using assms by auto
   show ?thesis
     by (rule normalize_poly_normalize_poly_p[THEN order_trans, OF rs])
      (use st in \<open>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\<close>)
 qed
 
 lemma remove1_list_rel:
   \<open>(xs, ys) \<in> \<langle>R\<rangle> list_rel \<Longrightarrow>
   (a, b) \<in> R \<Longrightarrow>
   IS_RIGHT_UNIQUE R \<Longrightarrow>
   IS_LEFT_UNIQUE R \<Longrightarrow>
   (remove1 a xs, remove1 b ys) \<in> \<langle>R\<rangle>list_rel\<close>
   by (induction xs ys rule: list_rel_induct)
    (auto simp: single_valued_def IS_LEFT_UNIQUE_def)
 
 lemma remove1_list_rel2:
   \<open>(xs, ys) \<in> \<langle>R\<rangle> list_rel \<Longrightarrow>
   (a, b) \<in> R \<Longrightarrow>
   (\<And>c. (a, c) \<in> R \<Longrightarrow> c = b) \<Longrightarrow>
   (\<And>c. (c, b) \<in> R \<Longrightarrow> c = a) \<Longrightarrow>
   (remove1 a xs, remove1 b ys) \<in> \<langle>R\<rangle>list_rel\<close>
   apply (induction xs ys rule: list_rel_induct)
    apply (solves \<open>simp (no_asm)\<close>)
   by (smt list_rel_simp(4) remove1.simps(2))
 
 lemma remove1_sorted_poly_rel_mset_poly_rel:
   assumes
     \<open>(r, r') \<in> sorted_poly_rel O mset_poly_rel\<close> and
     \<open>([a], 1) \<in> set r\<close>
   shows
     \<open>(remove1 ([a], 1) r, r' - Var (\<phi> a))
           \<in> sorted_poly_rel O mset_poly_rel\<close>
 proof -
    have [simp]: \<open>([a], {#a#}) \<in> term_poly_list_rel\<close>
      \<open>\<And>aa. ([a], aa) \<in> term_poly_list_rel \<longleftrightarrow> aa = {#a#}\<close>
      by (auto simp: term_poly_list_rel_def)
   have H:
     \<open>\<And>aa. ([a], aa) \<in> term_poly_list_rel \<Longrightarrow> aa = {#a#}\<close>
      \<open>\<And>aa. (aa, {#a#}) \<in> term_poly_list_rel \<Longrightarrow> aa = [a]\<close>
      by (auto simp: single_valued_def IS_LEFT_UNIQUE_def
        term_poly_list_rel_def)
 
   have [simp]: \<open>Const (1 :: int) = (1 :: int mpoly)\<close>
     by (simp add: Const.abs_eq Const\<^sub>0_one one_mpoly.abs_eq)
   have [simp]: \<open>sorted_wrt term_order (map fst r) \<Longrightarrow>
          sorted_wrt term_order (map fst (remove1 ([a], 1) r))\<close>
     by (induction r) auto
   have [intro]: \<open>distinct (map fst r) \<Longrightarrow> distinct (map fst (remove1 x r))\<close> for x
     by (induction r) (auto dest: in_set_remove1D)
   have [simp]: \<open>(r, ya) \<in> \<langle>term_poly_list_rel \<times>\<^sub>r int_rel\<rangle>list_rel \<Longrightarrow>
          polynomial_of_mset (mset ya) -  Var (\<phi> a) =
          polynomial_of_mset (remove1_mset ({#a#}, 1) (mset ya))\<close> 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 = \<open>remove1_mset ({#a#}, 1) za\<close> in relcompI)
     apply (auto simp: mset_poly_rel_def sorted_poly_list_rel_wrt_def Collect_eq_comp'
       intro!: relcompI[of _ \<open>remove1 ({#a#}, 1) ya\<close>
         for ya :: \<open>(string multiset \<times> int) list\<close>]  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
     \<open>(r, r') \<in> sorted_poly_rel O mset_poly_rel\<close> and
     \<open>([a], -1) \<in> set r\<close>
   shows
     \<open>(remove1 ([a], -1) r, r' + Var (\<phi> a))
           \<in> sorted_poly_rel O mset_poly_rel\<close>
 proof -
    have [simp]: \<open>([a], {#a#}) \<in> term_poly_list_rel\<close>
      \<open>\<And>aa. ([a], aa) \<in> term_poly_list_rel \<longleftrightarrow> aa = {#a#}\<close>
      by (auto simp: term_poly_list_rel_def)
   have H:
     \<open>\<And>aa. ([a], aa) \<in> term_poly_list_rel \<Longrightarrow> aa = {#a#}\<close>
      \<open>\<And>aa. (aa, {#a#}) \<in> term_poly_list_rel \<Longrightarrow> aa = [a]\<close>
      by (auto simp: single_valued_def IS_LEFT_UNIQUE_def
        term_poly_list_rel_def)
 
   have [simp]: \<open>Const (1 :: int) = (1 :: int mpoly)\<close>
     by (simp add: Const.abs_eq Const\<^sub>0_one one_mpoly.abs_eq)
   have [simp]: \<open>sorted_wrt term_order (map fst r) \<Longrightarrow>
          sorted_wrt term_order (map fst (remove1 ([a], -1) r))\<close>
     by (induction r) auto
   have [intro]: \<open>distinct (map fst r) \<Longrightarrow> distinct (map fst (remove1 x r))\<close> for x
     apply (induction r) apply auto
     by (meson img_fst in_set_remove1D)
   have [simp]: \<open>(r, ya) \<in> \<langle>term_poly_list_rel \<times>\<^sub>r int_rel\<rangle>list_rel \<Longrightarrow>
          polynomial_of_mset (mset ya) +  Var (\<phi> a) =
          polynomial_of_mset (remove1_mset ({#a#}, -1) (mset ya))\<close> 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 = \<open>remove1_mset ({#a#}, -1) za\<close> in relcompI)
     by (auto simp: mset_poly_rel_def sorted_poly_list_rel_wrt_def Collect_eq_comp'
        dest: in_diffD
        intro!: relcompI[of _ \<open>remove1 ({#a#}, -1) ya\<close>
          for ya :: \<open>(string multiset \<times> int) list\<close>]  remove1_list_rel2 intro: H
       simp: list_mset_rel_def br_def)
 qed
 
 
 lemma insert_var_rel_set_rel:
   \<open>(\<V>, \<V>') \<in> \<langle>var_rel\<rangle>set_rel \<Longrightarrow>
   (yb, x2) \<in> var_rel \<Longrightarrow>
   (insert yb \<V>, insert x2 \<V>') \<in> \<langle>var_rel\<rangle>set_rel\<close>
   by (auto simp: var_rel_def set_rel_def)
 
 lemma var_rel_set_rel_iff:
   \<open>(\<V>, \<V>') \<in> \<langle>var_rel\<rangle>set_rel \<Longrightarrow>
   (yb, x2) \<in> var_rel \<Longrightarrow>
   yb \<in> \<V> \<longleftrightarrow> x2 \<in>  \<V>'\<close>
   using \<phi>_inj inj_eq by (fastforce simp: var_rel_def set_rel_def br_def)
 
 
 lemma check_extension_l_check_extension:
   assumes \<open>(A, B) \<in> fmap_polys_rel\<close> and \<open>(r, r') \<in> sorted_poly_rel O mset_poly_rel\<close> and
     \<open>(i, i') \<in> nat_rel\<close> \<open>(\<V>, \<V>') \<in> \<langle>var_rel\<rangle>set_rel\<close> \<open>(x, x') \<in> var_rel\<close>
   shows
     \<open>check_extension_l spec A \<V> i x r \<le>
       \<Down>{((st), (b)).
         (\<not>is_cfailed st \<longleftrightarrow> b) \<and>
        (is_cfound st \<longrightarrow> spec = r)} (check_extension B \<V>' i' x' r')\<close>
 proof -
   have \<open>x' = \<phi> x\<close>
     using assms(5) by (auto simp: var_rel_def br_def)
   have [refine]:
     \<open>mult_poly_full p q \<le> \<Down> (sorted_poly_rel O mset_poly_rel) (mult_poly_spec p' q')\<close>
     if \<open>(p, p') \<in> sorted_poly_rel O mset_poly_rel\<close>
       \<open>(q, q') \<in> sorted_poly_rel O mset_poly_rel\<close>
     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]:
     \<open>add_poly_l (p, q) \<le> \<Down> (sorted_poly_rel O mset_poly_rel) (add_poly_spec p' q')\<close>
     if \<open>(p, p') \<in> sorted_poly_rel O mset_poly_rel\<close>
       \<open>(q, q') \<in> sorted_poly_rel O mset_poly_rel\<close>
     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]: \<open>(l, l') \<in> \<langle>term_poly_list_rel \<times>\<^sub>r int_rel\<rangle>list_rel \<Longrightarrow>
        (map (\<lambda>(a, b). (a, - b)) l, map (\<lambda>(a, b). (a, - b)) l')
        \<in> \<langle>term_poly_list_rel \<times>\<^sub>r int_rel\<rangle>list_rel\<close> for l l'
      by (induction l l'  rule: list_rel_induct)
         (auto simp: list_mset_rel_def br_def)
 
   have [intro!]:
     \<open>(x2c, za) \<in> \<langle>term_poly_list_rel \<times>\<^sub>r int_rel\<rangle>list_rel O list_mset_rel \<Longrightarrow>
      (map (\<lambda>(a, b). (a, - b)) x2c,
         {#case x of (a, b) \<Rightarrow> (a, - b). x \<in># za#})
        \<in> \<langle>term_poly_list_rel \<times>\<^sub>r int_rel\<rangle>list_rel O list_mset_rel\<close> 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 (rule_tac b = \<open>(aa, - ba) # map (\<lambda>(a, b). (a, - b)) l'\<close> in relcompI)
+       apply (rename_tac a ba aa l l', rule_tac b = \<open>(aa, - ba) # map (\<lambda>(a, b). (a, - b)) l'\<close> in relcompI)
        by auto
      done
   have [simp]: \<open>(\<lambda>x. fst (case x of (a, b) \<Rightarrow> (a, - b))) = fst\<close>
     by (auto intro: ext)
 
   have uminus: \<open>(x2c, x2a) \<in> sorted_poly_rel O mset_poly_rel \<Longrightarrow>
        (map (\<lambda>(a, b). (a, - b)) x2c,
         - x2a)
        \<in> sorted_poly_rel O mset_poly_rel\<close> for x2c x2a x1c x1a
      apply (clarsimp simp: sorted_poly_list_rel_wrt_def
       mset_poly_rel_def)
     apply (rule_tac b = \<open>(\<lambda>(a, b). (a, - b)) `# za\<close> in relcompI)
     by (auto simp: sorted_poly_list_rel_wrt_def
       mset_poly_rel_def comp_def polynomial_of_mset_uminus)
    have [simp]: \<open>([], 0) \<in> sorted_poly_rel O mset_poly_rel\<close>
      by (auto simp: sorted_poly_list_rel_wrt_def
       mset_poly_rel_def list_mset_rel_def br_def
       intro!: relcompI[of _ \<open>{#}\<close>])
    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 \<open>x' = \<phi> x\<close>, 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 \<open>r\<close> \<open>r'\<close>] 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 \<open>(p, p') \<in> fully_unsorted_poly_rel O mset_poly_rel\<close>
   shows
     \<open>full_normalize_poly p
     \<le> \<Down> (sorted_poly_rel O mset_poly_rel)
        (normalize_poly_spec p')\<close>
 proof -
   obtain q where
     pq: \<open>(p, q) \<in> fully_unsorted_poly_rel\<close>  and qp':\<open>(q, p') \<in> mset_poly_rel\<close>
     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 \<open>auto dest!: rtranclp_normalize_poly_p_poly_of_mset
             simp: mset_poly_rel_def ideal.span_zero\<close>)
 qed
 
 lemma insort_key_rel_decomp:
    \<open>\<exists>ys zs. xs = ys @ zs \<and> insort_key_rel R x xs = ys @ x # zs\<close>
   apply (induction xs)
   subgoal by auto
   subgoal for a xs
     by (force intro: exI[of _ \<open>a # _\<close>])
   done
 
 lemma list_rel_append_same_length:
    \<open>length xs = length xs' \<Longrightarrow> (xs @ ys, xs' @ ys') \<in> \<langle>R\<rangle>list_rel \<longleftrightarrow> (xs, xs') \<in> \<langle>R\<rangle>list_rel \<and> (ys, ys') \<in> \<langle>R\<rangle>list_rel\<close>
   by (auto simp: list_rel_def list_all2_append2 dest: list_all2_lengthD)
 
 lemma term_poly_list_rel_list_relD: \<open>(ys, cs) \<in> \<langle>term_poly_list_rel \<times>\<^sub>r int_rel\<rangle>list_rel \<Longrightarrow>
        cs = map (\<lambda>(a, y). (mset a, y)) ys\<close>
   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: \<open>([x32], {#x32#}) \<in> term_poly_list_rel\<close>
   by (auto simp: term_poly_list_rel_def)
 
 lemma unsorted_poly_rel_list_rel_list_rel_uminus:
    \<open>(map (\<lambda>(a, b). (a, - b)) r, yc)
        \<in> \<langle>unsorted_term_poly_list_rel \<times>\<^sub>r int_rel\<rangle>list_rel \<Longrightarrow>
        (r, map (\<lambda>(a, b). (a, - b)) yc)
        \<in> \<langle>unsorted_term_poly_list_rel \<times>\<^sub>r int_rel\<rangle>list_rel\<close>
   by (induction r arbitrary: yc)
    (auto simp: elim!: list_relE3)
 
 lemma mset_poly_rel_minus: \<open>({#(a, b)#}, v') \<in> mset_poly_rel \<Longrightarrow>
        (mset yc, r') \<in> mset_poly_rel \<Longrightarrow>
        (r, yc)
        \<in> \<langle>unsorted_term_poly_list_rel \<times>\<^sub>r int_rel\<rangle>list_rel \<Longrightarrow>
        (add_mset (a, b) (mset yc),
         v' + r')
        \<in> mset_poly_rel\<close>
   by (induction r arbitrary: r')
     (auto simp: mset_poly_rel_def polynomial_of_mset_uminus)
 
 lemma fully_unsorted_poly_rel_diff:
    \<open>([v], v') \<in> fully_unsorted_poly_rel O mset_poly_rel \<Longrightarrow>
    (r, r') \<in> fully_unsorted_poly_rel O mset_poly_rel \<Longrightarrow>
     (v # r,
      v' + r')
     \<in> fully_unsorted_poly_rel O mset_poly_rel\<close>
   apply auto
   apply (rule_tac b = \<open>y + ya\<close> in relcompI)
   apply (auto simp: fully_unsorted_poly_list_rel_def list_mset_rel_def br_def)
   apply (rule_tac b = \<open>yb @ yc\<close> 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
     \<open>(Ast, Bst) \<in> code_status_status_rel \<times>\<^sub>r \<langle>var_rel\<rangle>set_rel \<times>\<^sub>r fmap_polys_rel\<close> and
     \<open>(st, st') \<in> pac_step_rel\<close> and
     spec: \<open>(spec, spec') \<in> sorted_poly_rel O mset_poly_rel\<close>
   shows
     \<open>PAC_checker_l_step spec Ast st \<le> \<Down> (code_status_status_rel \<times>\<^sub>r \<langle>var_rel\<rangle>set_rel \<times>\<^sub>r fmap_polys_rel) (PAC_checker_step spec' Bst st')\<close>
 proof -
   obtain A \<V> cst B \<V>' cst' where
    Ast: \<open>Ast = (cst, \<V>, A)\<close> and
    Bst: \<open>Bst = (cst', \<V>', B)\<close> and
    \<V>[intro]: \<open>(\<V>, \<V>') \<in>  \<langle>var_rel\<rangle>set_rel\<close>  and
    AB: \<open>(A, B) \<in> fmap_polys_rel\<close>
      \<open>(cst, cst') \<in> code_status_status_rel\<close>
     using assms(1)
     by (cases Ast; cases Bst; auto)
   have [refine]: \<open>(r, ra) \<in> sorted_poly_rel O mset_poly_rel \<Longrightarrow>
        (eqa, eqaa)
        \<in> {(st, b). (\<not> is_cfailed st \<longleftrightarrow> b) \<and> (is_cfound st \<longrightarrow> spec = r)} \<Longrightarrow>
        RETURN eqa
        \<le> \<Down> code_status_status_rel
           (SPEC
             (\<lambda>st'. (\<not> is_failed st' \<and>
                    is_found st' \<longrightarrow>
                     ra - spec' \<in> More_Modules.ideal polynomial_bool)))\<close>
      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]: \<open>(eqa, st'a) \<in> code_status_status_rel \<Longrightarrow>
        (merge_cstatus cst eqa, merge_status cst' st'a)
        \<in> code_status_status_rel\<close> for eqa st'a
      using AB
      by (cases eqa; cases st'a)
        (auto simp: code_status_status_rel_def)
   have [simp]: \<open>(merge_cstatus cst CSUCCESS, cst') \<in> code_status_status_rel\<close>
     using AB
     by (cases st)
       (auto simp: code_status_status_rel_def)
   have [simp]: \<open>(x32, x32a) \<in> var_rel \<Longrightarrow>
         ([([x32], -1::int)], -Var x32a) \<in> fully_unsorted_poly_rel O mset_poly_rel\<close> 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 _ \<open>{#({#x32#}, -1 :: int)#}\<close>]
          relcompI[of _ \<open>[({#x32#}, -1)]\<close>])
   have H3: \<open>p - Var a = (-Var a) + p\<close> for p :: \<open>int mpoly\<close> 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: \<V>)
       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 _ \<open>-Var _ :: int mpoly\<close>, 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:
   \<open>(x1a, x1c) \<in> code_status_status_rel \<Longrightarrow> is_cfailed x1a \<longleftrightarrow> is_failed x1c\<close>
   \<open>(x1a, x1c) \<in> code_status_status_rel \<Longrightarrow> is_cfound x1a \<longleftrightarrow> is_found x1c\<close>
   by (cases x1a; cases x1c; auto; fail)+
 
 lemma PAC_checker_l_PAC_checker:
   assumes
     \<open>(A, B) \<in> \<langle>var_rel\<rangle>set_rel \<times>\<^sub>r fmap_polys_rel\<close> and
     \<open>(st, st') \<in> \<langle>pac_step_rel\<rangle>list_rel\<close> and
     \<open>(spec, spec') \<in> sorted_poly_rel O mset_poly_rel\<close> and
     \<open>(b, b') \<in> code_status_status_rel\<close>
   shows
     \<open>PAC_checker_l spec A b st \<le> \<Down> (code_status_status_rel \<times>\<^sub>r \<langle>var_rel\<rangle>set_rel \<times>\<^sub>r fmap_polys_rel) (PAC_checker spec' B b' st')\<close>
 proof -
   have [refine0]: \<open>(((b, A), st), (b', B), st') \<in> ((code_status_status_rel \<times>\<^sub>r \<langle>var_rel\<rangle>set_rel \<times>\<^sub>r fmap_polys_rel) \<times>\<^sub>r  \<langle>pac_step_rel\<rangle>list_rel)\<close>
     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 = \<open>((bool_rel \<times>\<^sub>r \<langle>var_rel\<rangle>set_rel \<times>\<^sub>r fmap_polys_rel) \<times>\<^sub>r \<langle>pac_step_rel\<rangle>list_rel)\<close>])
     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 less_than_char_of_char[code_unfold]:
   \<open>(x, y) \<in> less_than_char \<longleftrightarrow> (of_char x :: nat) < of_char y\<close>
   by (auto simp: less_than_char_def less_char_def)
 
 
 lemmas [code] =
   add_poly_l'.simps[unfolded var_order_rel_def]
 
 export_code add_poly_l' in SML module_name test
 
 definition full_checker_l
   :: \<open>llist_polynomial \<Rightarrow> (nat, llist_polynomial) fmap \<Rightarrow> (_, string, nat) pac_step list \<Rightarrow>
     (string code_status \<times> _) nres\<close>
 where
   \<open>full_checker_l spec A st = do {
     spec' \<leftarrow> full_normalize_poly spec;
     (b, \<V>, A) \<leftarrow> remap_polys_l spec' {} A;
     if is_cfailed b
     then RETURN (b, \<V>, A)
     else do {
       let \<V> = \<V> \<union> vars_llist spec;
       PAC_checker_l spec' (\<V>, A) b st
     }
   }\<close>
 
 
 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
   \<open>unsorted_fmap_polys_rel \<equiv> \<langle>nat_rel, fully_unsorted_poly_rel O mset_poly_rel\<rangle>fmap_rel\<close>
 
 lemma full_checker_l_full_checker:
  assumes
     \<open>(A, B) \<in> unsorted_fmap_polys_rel\<close> and
     \<open>(st, st') \<in> \<langle>pac_step_rel\<rangle>list_rel\<close> and
     \<open>(spec, spec') \<in> fully_unsorted_poly_rel O mset_poly_rel\<close>
   shows
     \<open>full_checker_l spec A st \<le> \<Down> (code_status_status_rel \<times>\<^sub>r \<langle>var_rel\<rangle>set_rel \<times>\<^sub>r fmap_polys_rel) (full_checker spec' B st')\<close>
 proof -
   have [refine]:
     \<open>(spec, spec') \<in> sorted_poly_rel O mset_poly_rel \<Longrightarrow>
     (\<V>, \<V>') \<in> \<langle>var_rel\<rangle>set_rel \<Longrightarrow>
     remap_polys_l spec \<V> A \<le> \<Down>(code_status_status_rel \<times>\<^sub>r \<langle>var_rel\<rangle>set_rel \<times>\<^sub>r fmap_polys_rel)
         (remap_polys_change_all spec' \<V>' B)\<close> for spec spec' \<V> \<V>'
     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':
   \<open>(uncurry2 full_checker_l, uncurry2 full_checker) \<in>
   ((fully_unsorted_poly_rel O mset_poly_rel) \<times>\<^sub>r unsorted_fmap_polys_rel) \<times>\<^sub>r \<langle>pac_step_rel\<rangle>list_rel \<rightarrow>\<^sub>f
     \<langle>(code_status_status_rel \<times>\<^sub>r \<langle>var_rel\<rangle>set_rel \<times>\<^sub>r fmap_polys_rel)\<rangle>nres_rel\<close>
   apply (intro frefI nres_relI)
   using full_checker_l_full_checker by force
 
 end
 
 definition remap_polys_l2 :: \<open>llist_polynomial \<Rightarrow> string set \<Rightarrow> (nat, llist_polynomial) fmap \<Rightarrow> _ nres\<close> where
   \<open>remap_polys_l2 spec = (\<lambda>\<V> A. do{
    n \<leftarrow> upper_bound_on_dom A;
    b \<leftarrow> RETURN (n \<ge> 2^64);
    if b
    then do {
      c \<leftarrow> remap_polys_l_dom_err;
      RETURN (error_msg (0 ::nat) c, \<V>, fmempty)
    }
    else do {
        (b, \<V>, A) \<leftarrow> nfoldli ([0..<n]) (\<lambda>_. True)
        (\<lambda>i (b, \<V>, A').
           if i \<in># dom_m A
           then do {
             ASSERT(fmlookup A i \<noteq> None);
             p \<leftarrow> full_normalize_poly (the (fmlookup A i));
             eq \<leftarrow> weak_equality_l p spec;
             \<V> \<leftarrow> RETURN (\<V> \<union> vars_llist (the (fmlookup A i)));
             RETURN(b \<or> eq, \<V>, fmupd i p A')
           } else RETURN (b, \<V>, A')
         )
        (False, \<V>, fmempty);
      RETURN (if b then CFOUND else CSUCCESS, \<V>, A)
     }
  })\<close>
 
 lemma remap_polys_l2_remap_polys_l:
   \<open>remap_polys_l2 spec \<V> A \<le> \<Down> Id (remap_polys_l spec \<V> A)\<close>
 proof -
   have [refine]: \<open>(A, A') \<in> Id \<Longrightarrow> upper_bound_on_dom A
     \<le> \<Down> {(n, dom). dom = set [0..<n]} (SPEC (\<lambda>dom. set_mset (dom_m A') \<subseteq> dom \<and> finite dom))\<close> for A A'
     unfolding upper_bound_on_dom_def
     apply (rule RES_refine)
     apply (auto simp: upper_bound_on_dom_def)
     done
   have 1: \<open>inj_on id dom\<close> for dom
     by auto
   have 2: \<open>x \<in># dom_m A \<Longrightarrow>
        x' \<in># dom_m A' \<Longrightarrow>
        (x, x') \<in> nat_rel \<Longrightarrow>
        (A, A') \<in> Id \<Longrightarrow>
        full_normalize_poly (the (fmlookup A x))
        \<le> \<Down> Id
           (full_normalize_poly (the (fmlookup A' x')))\<close>
        for A A' x x'
        by (auto)
   have 3: \<open>(n, dom) \<in> {(n, dom). dom = set [0..<n]} \<Longrightarrow>
        ([0..<n], dom) \<in> \<langle>nat_rel\<rangle>list_set_rel\<close> for n dom
   by (auto simp: list_set_rel_def br_def)
   have 4: \<open>(p,q) \<in> Id \<Longrightarrow>
     weak_equality_l p spec \<le> \<Down>Id (weak_equality_l q spec)\<close> for p q spec
     by auto
 
   have 6: \<open>a = b \<Longrightarrow> (a, b) \<in> Id\<close> for a b
     by auto
   show ?thesis
     unfolding remap_polys_l2_def remap_polys_l_def
     apply (refine_rcg LFO_refine[where R= \<open>Id \<times>\<^sub>r \<langle>Id\<rangle>set_rel \<times>\<^sub>r Id\<close>])
     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
diff --git a/thys/PAC_Checker/PAC_Checker_Init.thy b/thys/PAC_Checker/PAC_Checker_Init.thy
--- a/thys/PAC_Checker/PAC_Checker_Init.thy
+++ b/thys/PAC_Checker/PAC_Checker_Init.thy
@@ -1,886 +1,892 @@
 (*
   File:         PAC_Checker_Init.thy
   Author:       Mathias Fleury, Daniela Kaufmann, JKU
   Maintainer:   Mathias Fleury, JKU
 *)
 theory PAC_Checker_Init
   imports  PAC_Checker WB_Sort PAC_Checker_Relation
 begin
 
 section \<open>Initial Normalisation of Polynomials\<close>
 
 subsection \<open>Sorting\<close>
 
 text \<open>Adapted from the theory \<^text>\<open>HOL-ex.MergeSort\<close> by Tobias Nipkow. We did not change much, but
    we refine it to executable code and try to improve efficiency.
 \<close>
 
 fun merge :: "_ \<Rightarrow>  'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
 where
   "merge f (x#xs) (y#ys) =
          (if f x y then x # merge f xs (y#ys) else y # merge f (x#xs) ys)"
 | "merge f xs [] = xs"
 | "merge f [] ys = ys"
 
 lemma mset_merge [simp]:
   "mset (merge f xs ys) = mset xs + mset ys"
   by (induct f xs ys rule: merge.induct) (simp_all add: ac_simps)
 
 lemma set_merge [simp]:
   "set (merge f xs ys) = set xs \<union> set ys"
   by (induct f xs ys rule: merge.induct) auto
 
 lemma sorted_merge:
   "transp f \<Longrightarrow> (\<And>x y. f x y \<or> f y x) \<Longrightarrow>
    sorted_wrt f (merge f xs ys) \<longleftrightarrow> sorted_wrt f xs \<and> sorted_wrt f ys"
   apply (induct f xs ys rule: merge.induct)
   apply (auto simp add: ball_Un not_le less_le dest: transpD)
   apply blast
   apply (blast dest: transpD)
   done
 
 fun msort :: "_ \<Rightarrow> 'a list \<Rightarrow> 'a list"
 where
   "msort f [] = []"
 | "msort f [x] = [x]"
 | "msort f xs = merge f
                       (msort f (take (size xs div 2) xs))
                       (msort f (drop (size xs div 2) xs))"
 
 fun swap_ternary :: \<open>_\<Rightarrow>nat\<Rightarrow>nat\<Rightarrow> ('a \<times> 'a \<times> 'a) \<Rightarrow> ('a \<times> 'a \<times> 'a)\<close> where
   \<open>swap_ternary f m n  =
     (if (m = 0 \<and> n = 1)
     then (\<lambda>(a, b, c). if f a b then (a, b, c)
       else (b,a,c))
     else if (m = 0 \<and> n = 2)
     then (\<lambda>(a, b, c). if f a c then (a, b, c)
       else (c,b,a))
     else if (m = 1 \<and> n = 2)
     then (\<lambda>(a, b, c). if f b c then (a, b, c)
       else (a,c,b))
     else (\<lambda>(a, b, c). (a,b,c)))\<close>
 
 fun msort2 :: "_ \<Rightarrow> 'a list \<Rightarrow> 'a list"
 where
   "msort2 f [] = []"
 | "msort2 f [x] = [x]"
 | "msort2 f [x,y] = (if f x y then [x,y] else [y,x])"
 | "msort2 f xs = merge f
                       (msort f (take (size xs div 2) xs))
                       (msort f (drop (size xs div 2) xs))"
 
 lemmas [code del] =
   msort2.simps
 
 declare msort2.simps[simp del]
 lemmas [code] =
   msort2.simps[unfolded swap_ternary.simps, simplified]
 
 declare msort2.simps[simp]
 
 lemma msort_msort2:
   fixes xs :: \<open>'a :: linorder list\<close>
   shows \<open>msort (\<le>) xs = msort2 (\<le>) xs\<close>
   apply (induction  \<open>(\<le>) :: 'a \<Rightarrow> 'a \<Rightarrow> bool\<close> xs rule: msort2.induct)
   apply (auto dest: transpD)
   done
 
 lemma sorted_msort:
   "transp f \<Longrightarrow> (\<And>x y. f x y \<or> f y x) \<Longrightarrow>
    sorted_wrt f (msort f xs)"
   by (induct f xs rule: msort.induct) (simp_all add: sorted_merge)
 
 lemma mset_msort[simp]:
   "mset (msort f xs) = mset xs"
   by (induction f xs rule: msort.induct)
     (simp_all add: union_code)
 
 
 subsection \<open>Sorting applied to monomials\<close>
 
 lemma merge_coeffs_alt_def:
   \<open>(RETURN o merge_coeffs) p =
    REC\<^sub>T(\<lambda>f p.
      (case p of
        [] \<Rightarrow> RETURN []
      | [_] => RETURN p
      | ((xs, n) # (ys, m) # p) \<Rightarrow>
       (if xs = ys
        then if n + m \<noteq> 0 then f ((xs, n + m) # p) else f p
        else do {p \<leftarrow> f ((ys, m) # p); RETURN ((xs, n) # p)})))
     p\<close>
   apply (induction p rule: merge_coeffs.induct)
   subgoal by (subst RECT_unfold, refine_mono) auto
   subgoal by (subst RECT_unfold, refine_mono) auto
   subgoal for x p y q
     by (subst RECT_unfold, refine_mono)
      (smt case_prod_conv list.simps(5) merge_coeffs.simps(3) nres_monad1
       push_in_let_conv(2))
   done
 
 lemma hn_invalid_recover:
   \<open>is_pure R \<Longrightarrow> hn_invalid R = (\<lambda>x y. R x y * true)\<close>
   \<open>is_pure R \<Longrightarrow> invalid_assn R = (\<lambda>x y. R x y * true)\<close>
   by (auto simp: is_pure_conv invalid_pure_recover hn_ctxt_def intro!: ext)
 
 lemma safe_poly_vars:
   shows
     [safe_constraint_rules]:
       "is_pure (poly_assn)" and
     [safe_constraint_rules]:
       "is_pure (monom_assn)" and
     [safe_constraint_rules]:
       "is_pure (monomial_assn)" and
     [safe_constraint_rules]:
       "is_pure string_assn"
   by (auto intro!: pure_prod list_assn_pure simp: prod_assn_pure_conv)
 
 lemma invalid_assn_distrib:
   \<open>invalid_assn monom_assn \<times>\<^sub>a invalid_assn int_assn = invalid_assn (monom_assn \<times>\<^sub>a int_assn)\<close>
     apply (simp add: invalid_pure_recover hn_invalid_recover
       safe_constraint_rules)
     apply (subst hn_invalid_recover)
     apply (rule safe_poly_vars(2))
     apply (subst hn_invalid_recover)
     apply (rule safe_poly_vars)
     apply (auto intro!: ext)
     done
 
 lemma WTF_RF_recover:
   \<open>hn_ctxt (invalid_assn monom_assn \<times>\<^sub>a invalid_assn int_assn) xb
         x'a \<or>\<^sub>A
        hn_ctxt monomial_assn xb x'a \<Longrightarrow>\<^sub>t
        hn_ctxt (monomial_assn) xb x'a\<close>
   by (smt assn_aci(5) hn_ctxt_def invalid_assn_distrib invalid_pure_recover is_pure_conv
     merge_thms(4) merge_true_star reorder_enttI safe_poly_vars(3) star_aci(2) star_aci(3))
 
 lemma WTF_RF:
   \<open>hn_ctxt (invalid_assn monom_assn \<times>\<^sub>a invalid_assn int_assn) xb x'a *
        (hn_invalid poly_assn la l'a * hn_invalid int_assn a2' a2 *
         hn_invalid monom_assn a1' a1 *
         hn_invalid poly_assn l l' *
         hn_invalid monomial_assn xa x' *
         hn_invalid poly_assn ax px) \<Longrightarrow>\<^sub>t
        hn_ctxt (monomial_assn) xb x'a *
        hn_ctxt poly_assn
         la l'a *
        hn_ctxt poly_assn l l' *
        (hn_invalid int_assn a2' a2 *
         hn_invalid monom_assn a1' a1 *
         hn_invalid monomial_assn xa x' *
         hn_invalid poly_assn ax px)\<close>
   \<open>hn_ctxt (invalid_assn monom_assn \<times>\<^sub>a invalid_assn int_assn) xa x' *
        (hn_ctxt poly_assn l l' * hn_invalid poly_assn ax px) \<Longrightarrow>\<^sub>t
        hn_ctxt (monomial_assn) xa x' *
        hn_ctxt poly_assn l l' *
        hn_ctxt poly_assn ax px *
        emp\<close>
   by sepref_dbg_trans_step+
 
 text \<open>The refinement frameword is completely lost here when synthesizing the constants -- it does
   not understant what is pure (actually everything) and what must be destroyed.\<close>
 sepref_definition merge_coeffs_impl
   is \<open>RETURN o merge_coeffs\<close>
   :: \<open>poly_assn\<^sup>d \<rightarrow>\<^sub>a poly_assn\<close>
   supply [[goals_limit=1]]
   unfolding merge_coeffs_alt_def
     HOL_list.fold_custom_empty poly_assn_alt_def
   apply (rewrite in \<open>_\<close> annotate_assn[where A=\<open>poly_assn\<close>])
   apply sepref_dbg_preproc
   apply sepref_dbg_cons_init
   apply sepref_dbg_id
   apply sepref_dbg_monadify
   apply sepref_dbg_opt_init
   apply (rule WTF_RF | sepref_dbg_trans_step)+
   apply sepref_dbg_opt
   apply sepref_dbg_cons_solve
   apply sepref_dbg_cons_solve
   apply sepref_dbg_constraints
   done
 
 definition full_quicksort_poly where
   \<open>full_quicksort_poly = full_quicksort_ref (\<lambda>x y. x = y \<or> (x, y) \<in> term_order_rel) fst\<close>
 
 lemma down_eq_id_list_rel: \<open>\<Down>(\<langle>Id\<rangle>list_rel) x = x\<close>
   by auto
 
 definition quicksort_poly:: \<open>nat \<Rightarrow> nat \<Rightarrow> llist_polynomial \<Rightarrow> (llist_polynomial) nres\<close> where
   \<open>quicksort_poly x y  z = quicksort_ref (\<le>) fst (x, y, z)\<close>
 
 term partition_between_ref
 
 definition partition_between_poly :: \<open>nat \<Rightarrow> nat \<Rightarrow> llist_polynomial \<Rightarrow> (llist_polynomial \<times> nat) nres\<close> where
   \<open>partition_between_poly = partition_between_ref (\<le>) fst\<close>
 
 definition partition_main_poly :: \<open>nat \<Rightarrow> nat \<Rightarrow> llist_polynomial \<Rightarrow> (llist_polynomial \<times> nat) nres\<close> where
   \<open>partition_main_poly = partition_main (\<le>)  fst\<close>
 
 lemma string_list_trans:
   \<open>(xa ::char list list, ya) \<in> lexord (lexord {(x, y). x < y}) \<Longrightarrow>
   (ya, z) \<in> lexord (lexord {(x, y). x < y}) \<Longrightarrow>
     (xa, z) \<in> lexord (lexord {(x, y). x < y})\<close>
   by (smt less_char_def char.less_trans less_than_char_def lexord_partial_trans p2rel_def)
 
 lemma full_quicksort_sort_poly_spec:
   \<open>(full_quicksort_poly, sort_poly_spec) \<in> \<langle>Id\<rangle>list_rel \<rightarrow>\<^sub>f \<langle>\<langle>Id\<rangle>list_rel\<rangle>nres_rel\<close>
 proof -
   have xs: \<open>(xs, xs) \<in> \<langle>Id\<rangle>list_rel\<close> and \<open>\<Down>(\<langle>Id\<rangle>list_rel) x = x\<close> for x xs
     by auto
   show ?thesis
     apply (intro frefI nres_relI)
     unfolding full_quicksort_poly_def
     apply (rule full_quicksort_ref_full_quicksort[THEN fref_to_Down_curry, THEN order_trans])
     subgoal
       by (auto simp: rel2p_def var_order_rel_def p2rel_def Relation.total_on_def
         dest: string_list_trans)
     subgoal
       using total_on_lexord_less_than_char_linear[unfolded var_order_rel_def]
       apply (auto simp: rel2p_def var_order_rel_def p2rel_def Relation.total_on_def less_char_def)
       done
     subgoal by fast
     apply (rule xs)
     apply (subst down_eq_id_list_rel)
     unfolding sorted_wrt_map sort_poly_spec_def
     apply (rule full_quicksort_correct_sorted[where R = \<open>(\<lambda>x y. x = y \<or> (x, y) \<in> term_order_rel)\<close> and h = \<open>fst\<close>,
        THEN order_trans])
     subgoal
       by (auto simp: rel2p_def var_order_rel_def p2rel_def Relation.total_on_def dest: string_list_trans)
     subgoal for x y
       using total_on_lexord_less_than_char_linear[unfolded var_order_rel_def]
       apply (auto simp: rel2p_def var_order_rel_def p2rel_def Relation.total_on_def
         less_char_def)
       done
    subgoal
     by (auto simp: rel2p_def p2rel_def)
    done
 qed
 
 
 subsection \<open>Lifting to polynomials\<close>
 
 definition merge_sort_poly :: \<open>_\<close> where
 \<open>merge_sort_poly = msort (\<lambda>a b. fst a \<le> fst b)\<close>
 
 definition merge_monoms_poly :: \<open>_\<close> where
 \<open>merge_monoms_poly = msort (\<le>)\<close>
 
 definition merge_poly :: \<open>_\<close> where
 \<open>merge_poly = merge (\<lambda>a b. fst a \<le> fst b)\<close>
 
 definition merge_monoms :: \<open>_\<close> where
 \<open>merge_monoms = merge (\<le>)\<close>
 
 definition msort_poly_impl :: \<open>(String.literal list \<times> int) list \<Rightarrow> _\<close> where
 \<open>msort_poly_impl = msort (\<lambda>a b. fst a \<le> fst b)\<close>
 
 definition msort_monoms_impl :: \<open>(String.literal list) \<Rightarrow> _\<close> where
 \<open>msort_monoms_impl = msort (\<le>)\<close>
 
 lemma msort_poly_impl_alt_def:
   \<open>msort_poly_impl xs =
     (case xs of
       [] \<Rightarrow> []
      | [a] \<Rightarrow> [a]
      | [a,b] \<Rightarrow> if fst a \<le> fst b then [a,b]else [b,a]
      | xs \<Rightarrow> merge_poly
                       (msort_poly_impl (take ((length xs) div 2) xs))
                       (msort_poly_impl (drop ((length xs) div 2) xs)))\<close>
    unfolding msort_poly_impl_def
   apply (auto split: list.splits simp: merge_poly_def)
   done
 
 lemma le_term_order_rel':
   \<open>(\<le>) = (\<lambda>x y. x = y \<or>  term_order_rel' x y)\<close>
   apply (intro ext)
   apply (auto simp add: less_list_def less_eq_list_def
     lexordp_eq_conv_lexord lexordp_def)
   using term_order_rel'_alt_def_lexord term_order_rel'_def apply blast
   using term_order_rel'_alt_def_lexord term_order_rel'_def apply blast
   done
 
 fun lexord_eq where
   \<open>lexord_eq [] _ = True\<close> |
   \<open>lexord_eq (x # xs) (y # ys) = (x < y \<or> (x = y \<and> lexord_eq xs ys))\<close> |
   \<open>lexord_eq _ _ = False\<close>
 
 lemma [simp]:
   \<open>lexord_eq [] [] = True\<close>
   \<open>lexord_eq (a # b)[] = False\<close>
   \<open>lexord_eq [] (a # b) = True\<close>
   apply auto
   done
 
 lemma var_order_rel':
   \<open>(\<le>) = (\<lambda>x y. x = y \<or> (x,y) \<in> var_order_rel)\<close>
   by (intro ext)
    (auto simp add: less_list_def less_eq_list_def
     lexordp_eq_conv_lexord lexordp_def var_order_rel_def
     lexordp_conv_lexord p2rel_def)
 
 
 lemma var_order_rel'':
   \<open>(x,y) \<in> var_order_rel \<longleftrightarrow> x < y\<close>
   by (metis leD less_than_char_linear lexord_linear neq_iff var_order_rel' var_order_rel_antisym
       var_order_rel_def)
 
 lemma lexord_eq_alt_def1:
   \<open>a \<le> b = lexord_eq a b\<close> for a b :: \<open>String.literal list\<close>
   unfolding le_term_order_rel'
   apply (induction a b rule: lexord_eq.induct)
   apply (auto simp: var_order_rel'' less_eq_list_def)
   done
 
 lemma lexord_eq_alt_def2:
   \<open>(RETURN oo lexord_eq) xs ys =
      REC\<^sub>T (\<lambda>f (xs, ys).
         case (xs, ys) of
            ([], _) \<Rightarrow> RETURN True
          | (x # xs, y # ys) \<Rightarrow>
             if x < y then RETURN True
             else if x = y then f (xs, ys) else RETURN False
         | _ \<Rightarrow> RETURN False)
         (xs, ys)\<close>
   apply (subst eq_commute)
   apply (induction xs ys rule: lexord_eq.induct)
   subgoal by (subst RECT_unfold, refine_mono) auto
   subgoal by (subst RECT_unfold, refine_mono) auto
   subgoal by (subst RECT_unfold, refine_mono) auto
   done
 
 
 definition var_order' where
   [simp]: \<open>var_order' = var_order\<close>
 
 lemma var_order_rel[def_pat_rules]:
   \<open>(\<in>)$(x,y)$var_order_rel \<equiv> var_order'$x$y\<close>
   by (auto simp: p2rel_def rel2p_def)
 
 lemma var_order_rel_alt_def:
   \<open>var_order_rel = p2rel char.lexordp\<close>
   apply (auto simp: p2rel_def char.lexordp_conv_lexord var_order_rel_def)
   using char.lexordp_conv_lexord apply auto
   done
 
 lemma var_order_rel_var_order:
   \<open>(x, y) \<in> var_order_rel \<longleftrightarrow> var_order x y\<close>
   by (auto simp: rel2p_def)
 
 lemma var_order_string_le[sepref_import_param]:
   \<open>((<), var_order') \<in> string_rel \<rightarrow> string_rel \<rightarrow> bool_rel\<close>
   apply (auto intro!: frefI simp: string_rel_def String.less_literal_def
      rel2p_def linorder.lexordp_conv_lexord[OF char.linorder_axioms,
       unfolded less_eq_char_def] var_order_rel_def
       p2rel_def
       simp flip: PAC_Polynomials_Term.less_char_def)
   using char.lexordp_conv_lexord apply auto
   done
 
 lemma [sepref_import_param]:
   \<open>( (\<le>), (\<le>)) \<in> monom_rel \<rightarrow> monom_rel \<rightarrow>bool_rel\<close>
   apply (intro fun_relI)
   using list_rel_list_rel_order_iff by fastforce
 
 lemma [sepref_import_param]:
   \<open>( (<), (<)) \<in> string_rel \<rightarrow> string_rel \<rightarrow>bool_rel\<close>
 proof -
   have [iff]: \<open>ord.lexordp (<) (literal.explode a) (literal.explode aa) \<longleftrightarrow>
        List.lexordp (<) (literal.explode a) (literal.explode aa)\<close> for a aa
     apply (rule iffI)
      apply (metis PAC_Checker_Relation.less_char_def char.lexordp_conv_lexord less_list_def
         p2rel_def var_order_rel'' var_order_rel_def)
     apply (metis PAC_Checker_Relation.less_char_def char.lexordp_conv_lexord less_list_def
         p2rel_def var_order_rel'' var_order_rel_def)
     done
   show ?thesis
     unfolding string_rel_def less_literal.rep_eq less_than_char_def
       less_eq_list_def PAC_Polynomials_Term.less_char_def[symmetric]
     by (intro fun_relI)
      (auto simp: string_rel_def less_literal.rep_eq
         less_list_def char.lexordp_conv_lexord lexordp_eq_refl
-        lexord_code lexordp_eq_conv_lexord)
+        lexordp_eq_conv_lexord)
 qed
 
+
+lemma lexordp_char_char: \<open>ord_class.lexordp = char.lexordp\<close>
+  unfolding char.lexordp_def ord_class.lexordp_def
+  by (rule arg_cong[of _ _ lfp])
+    (auto intro!: ext)
+
 lemma [sepref_import_param]:
   \<open>( (\<le>), (\<le>)) \<in> string_rel \<rightarrow> string_rel \<rightarrow>bool_rel\<close>
   unfolding string_rel_def less_eq_literal.rep_eq less_than_char_def
     less_eq_list_def PAC_Polynomials_Term.less_char_def[symmetric]
   by (intro fun_relI)
    (auto simp: string_rel_def less_eq_literal.rep_eq less_than_char_def
     less_eq_list_def char.lexordp_eq_conv_lexord lexordp_eq_refl
-    lexord_code lexordp_eq_conv_lexord
+    lexordp_eq_conv_lexord lexordp_char_char
     simp flip: less_char_def[abs_def])
 
 sepref_register lexord_eq
 sepref_definition lexord_eq_term
   is \<open>uncurry (RETURN oo lexord_eq)\<close>
   :: \<open>monom_assn\<^sup>k *\<^sub>a monom_assn\<^sup>k \<rightarrow>\<^sub>a bool_assn\<close>
   supply[[goals_limit=1]]
   unfolding lexord_eq_alt_def2
   by sepref
 
 declare lexord_eq_term.refine[sepref_fr_rules]
 
 
 lemmas [code del] = msort_poly_impl_def msort_monoms_impl_def
 lemmas [code] =
   msort_poly_impl_def[unfolded lexord_eq_alt_def1[abs_def]]
   msort_monoms_impl_def[unfolded msort_msort2]
 
 lemma term_order_rel_trans:
   \<open>(a, aa) \<in> term_order_rel \<Longrightarrow>
        (aa, ab) \<in> term_order_rel \<Longrightarrow> (a, ab) \<in> term_order_rel\<close>
   by (metis PAC_Checker_Relation.less_char_def p2rel_def string_list_trans var_order_rel_def)
 
 lemma merge_sort_poly_sort_poly_spec:
   \<open>(RETURN o merge_sort_poly, sort_poly_spec) \<in> \<langle>Id\<rangle>list_rel \<rightarrow>\<^sub>f \<langle>\<langle>Id\<rangle>list_rel\<rangle>nres_rel\<close>
   unfolding sort_poly_spec_def merge_sort_poly_def
   apply (intro frefI nres_relI)
   using total_on_lexord_less_than_char_linear var_order_rel_def
   by (auto intro!: sorted_msort simp: sorted_wrt_map rel2p_def
     le_term_order_rel' transp_def dest: term_order_rel_trans)
 
 lemma msort_alt_def:
   \<open>RETURN o (msort f) =
      REC\<^sub>T (\<lambda>g xs.
         case xs of
           [] \<Rightarrow> RETURN []
         | [x] \<Rightarrow> RETURN [x]
         | _ \<Rightarrow> do {
            a \<leftarrow> g (take (size xs div 2) xs);
            b \<leftarrow> g (drop (size xs div 2) xs);
            RETURN (merge f a b)})\<close>
   apply (intro ext)
   unfolding comp_def
   apply (induct_tac f x rule: msort.induct)
   subgoal by (subst RECT_unfold, refine_mono) auto
   subgoal by (subst RECT_unfold, refine_mono) auto
   subgoal
     by (subst RECT_unfold, refine_mono)
      (smt let_to_bind_conv list.simps(5) msort.simps(3))
   done
 
 lemma monomial_rel_order_map:
   \<open>(x, a, b) \<in> monomial_rel \<Longrightarrow>
        (y, aa, bb) \<in> monomial_rel \<Longrightarrow>
        fst x \<le> fst y \<longleftrightarrow> a \<le> aa\<close>
   apply (cases x; cases y)
   apply auto
   using list_rel_list_rel_order_iff by fastforce+
 
 
 lemma step_rewrite_pure:
   fixes K :: \<open>('olbl \<times> 'lbl) set\<close>
   shows
     \<open>pure (p2rel (\<langle>K, V, R\<rangle>pac_step_rel_raw)) = pac_step_rel_assn (pure K) (pure V) (pure R)\<close>
     \<open>monomial_assn = pure (monom_rel \<times>\<^sub>r int_rel)\<close> and
   poly_assn_list:
     \<open>poly_assn = pure (\<langle>monom_rel \<times>\<^sub>r int_rel\<rangle>list_rel)\<close>
   subgoal
     apply (intro ext)
     apply (case_tac x; case_tac xa)
     apply (auto simp: relAPP_def p2rel_def pure_def)
     done
   subgoal H
     apply (intro ext)
     apply (case_tac x; case_tac xa)
     by (simp add: list_assn_pure_conv)
   subgoal
     unfolding H
     by (simp add: list_assn_pure_conv relAPP_def)
   done
 
 lemma safe_pac_step_rel_assn[safe_constraint_rules]:
   "is_pure K \<Longrightarrow> is_pure V \<Longrightarrow> is_pure R \<Longrightarrow> is_pure (pac_step_rel_assn K V R)"
   by (auto simp: step_rewrite_pure(1)[symmetric] is_pure_conv)
 
 
 lemma merge_poly_merge_poly:
   \<open>(merge_poly, merge_poly)
    \<in> poly_rel \<rightarrow> poly_rel \<rightarrow> poly_rel\<close>
    unfolding merge_poly_def
   apply (intro fun_relI)
   subgoal for a a' aa a'a
     apply (induction \<open>(\<lambda>(a :: String.literal list \<times> int)
       (b :: String.literal list \<times> int). fst a \<le> fst b)\<close> a aa
       arbitrary: a' a'a
       rule: merge.induct)
     subgoal
       by (auto elim!: list_relE3 list_relE4 list_relE list_relE2
         simp: monomial_rel_order_map)
     subgoal
       by (auto elim!: list_relE3 list_relE)
     subgoal
       by (auto elim!: list_relE3 list_relE4 list_relE list_relE2)
     done
   done
 
 lemmas [fcomp_norm_unfold] =
   poly_assn_list[symmetric]
   step_rewrite_pure(1)
 
 lemma merge_poly_merge_poly2:
   \<open>(a, b) \<in> poly_rel \<Longrightarrow> (a', b') \<in> poly_rel \<Longrightarrow>
     (merge_poly a a', merge_poly b b') \<in> poly_rel\<close>
   using merge_poly_merge_poly
   unfolding fun_rel_def
   by auto
 
 lemma list_rel_takeD:
   \<open>(a, b) \<in> \<langle>R\<rangle>list_rel \<Longrightarrow> (n, n')\<in> Id \<Longrightarrow> (take n a, take n' b) \<in> \<langle>R\<rangle>list_rel\<close>
   by (simp add: list_rel_eq_listrel listrel_iff_nth relAPP_def)
 
 lemma list_rel_dropD:
   \<open>(a, b) \<in> \<langle>R\<rangle>list_rel \<Longrightarrow> (n, n')\<in> Id \<Longrightarrow> (drop n a, drop n' b) \<in> \<langle>R\<rangle>list_rel\<close>
   by (simp add: list_rel_eq_listrel listrel_iff_nth relAPP_def)
 
 lemma merge_sort_poly[sepref_import_param]:
   \<open>(msort_poly_impl, merge_sort_poly)
    \<in> poly_rel \<rightarrow> poly_rel\<close>
    unfolding merge_sort_poly_def msort_poly_impl_def
   apply (intro fun_relI)
   subgoal for a a'
     apply (induction \<open>(\<lambda>(a :: String.literal list \<times> int)
       (b :: String.literal list \<times> int). fst a \<le> fst b)\<close> a
       arbitrary: a'
       rule: msort.induct)
     subgoal
       by auto
     subgoal
       by (auto elim!: list_relE3 list_relE)
     subgoal premises p
       using p
       by (auto elim!: list_relE3 list_relE4 list_relE list_relE2
         simp: merge_poly_def[symmetric]
         intro!: list_rel_takeD list_rel_dropD
         intro!: merge_poly_merge_poly2 p(1)[simplified] p(2)[simplified],
         auto simp: list_rel_imp_same_length)
     done
   done
 
 
 
 lemmas [sepref_fr_rules] = merge_sort_poly[FCOMP merge_sort_poly_sort_poly_spec]
 
 sepref_definition partition_main_poly_impl
   is \<open>uncurry2 partition_main_poly\<close>
   :: \<open>nat_assn\<^sup>k *\<^sub>a nat_assn\<^sup>k *\<^sub>a poly_assn\<^sup>k \<rightarrow>\<^sub>a prod_assn poly_assn nat_assn \<close>
   unfolding partition_main_poly_def partition_main_def
     term_order_rel'_def[symmetric]
     term_order_rel'_alt_def
     le_term_order_rel'
   by sepref
 
 declare partition_main_poly_impl.refine[sepref_fr_rules]
 
 sepref_definition partition_between_poly_impl
   is \<open>uncurry2 partition_between_poly\<close>
   :: \<open>nat_assn\<^sup>k *\<^sub>a nat_assn\<^sup>k *\<^sub>a poly_assn\<^sup>k \<rightarrow>\<^sub>a prod_assn poly_assn nat_assn \<close>
   unfolding partition_between_poly_def partition_between_ref_def
     partition_main_poly_def[symmetric]
   unfolding choose_pivot3_def
     term_order_rel'_def[symmetric]
     term_order_rel'_alt_def choose_pivot_def
     lexord_eq_alt_def1
   by sepref
 
 declare partition_between_poly_impl.refine[sepref_fr_rules]
 
 sepref_definition quicksort_poly_impl
   is \<open>uncurry2 quicksort_poly\<close>
   :: \<open>nat_assn\<^sup>k *\<^sub>a nat_assn\<^sup>k *\<^sub>a poly_assn\<^sup>k \<rightarrow>\<^sub>a poly_assn\<close>
   unfolding partition_main_poly_def quicksort_ref_def quicksort_poly_def
     partition_between_poly_def[symmetric]
   by sepref
 
 lemmas [sepref_fr_rules] = quicksort_poly_impl.refine
 
 sepref_register quicksort_poly
 sepref_definition full_quicksort_poly_impl
   is \<open>full_quicksort_poly\<close>
   :: \<open>poly_assn\<^sup>k \<rightarrow>\<^sub>a poly_assn\<close>
   unfolding full_quicksort_poly_def full_quicksort_ref_def
     quicksort_poly_def[symmetric]
     le_term_order_rel'[symmetric]
     term_order_rel'_def[symmetric]
     List.null_def
   by sepref
 
 
 lemmas sort_poly_spec_hnr =
   full_quicksort_poly_impl.refine[FCOMP full_quicksort_sort_poly_spec]
 
 declare merge_coeffs_impl.refine[sepref_fr_rules]
 
 sepref_definition normalize_poly_impl
   is \<open>normalize_poly\<close>
   :: \<open>poly_assn\<^sup>k \<rightarrow>\<^sub>a poly_assn\<close>
   supply [[goals_limit=1]]
   unfolding normalize_poly_def
   by sepref
 
 declare normalize_poly_impl.refine[sepref_fr_rules]
 
 
 definition full_quicksort_vars where
   \<open>full_quicksort_vars = full_quicksort_ref (\<lambda>x y. x = y \<or> (x, y) \<in> var_order_rel) id\<close>
 
 
 definition quicksort_vars:: \<open>nat \<Rightarrow> nat \<Rightarrow> string list \<Rightarrow> (string list) nres\<close> where
   \<open>quicksort_vars x y  z = quicksort_ref (\<le>) id (x, y, z)\<close>
 
 
 definition partition_between_vars :: \<open>nat \<Rightarrow> nat \<Rightarrow> string list \<Rightarrow> (string list \<times> nat) nres\<close> where
   \<open>partition_between_vars = partition_between_ref (\<le>) id\<close>
 
 definition partition_main_vars :: \<open>nat \<Rightarrow> nat \<Rightarrow> string list \<Rightarrow> (string list \<times> nat) nres\<close> where
   \<open>partition_main_vars = partition_main (\<le>) id\<close>
 
 lemma total_on_lexord_less_than_char_linear2:
   \<open>xs \<noteq> ys \<Longrightarrow> (xs, ys) \<notin> lexord (less_than_char) \<longleftrightarrow>
        (ys, xs) \<in> lexord less_than_char\<close>
    using lexord_linear[of \<open>less_than_char\<close> xs ys]
    using lexord_linear[of \<open>less_than_char\<close>] less_than_char_linear
    apply (auto simp: Relation.total_on_def)
    using lexord_irrefl[OF irrefl_less_than_char]
      antisym_lexord[OF antisym_less_than_char irrefl_less_than_char]
    apply (auto simp: antisym_def)
    done
 
 lemma string_trans:
   \<open>(xa, ya) \<in> lexord {(x::char, y::char). x < y} \<Longrightarrow>
   (ya, z) \<in> lexord {(x::char, y::char). x < y} \<Longrightarrow>
   (xa, z) \<in> lexord {(x::char, y::char). x < y}\<close>
   by (smt less_char_def char.less_trans less_than_char_def lexord_partial_trans p2rel_def)
 
 lemma full_quicksort_sort_vars_spec:
   \<open>(full_quicksort_vars, sort_coeff) \<in> \<langle>Id\<rangle>list_rel \<rightarrow>\<^sub>f \<langle>\<langle>Id\<rangle>list_rel\<rangle>nres_rel\<close>
 proof -
   have xs: \<open>(xs, xs) \<in> \<langle>Id\<rangle>list_rel\<close> and \<open>\<Down>(\<langle>Id\<rangle>list_rel) x = x\<close> for x xs
     by auto
   show ?thesis
     apply (intro frefI nres_relI)
     unfolding full_quicksort_vars_def
     apply (rule full_quicksort_ref_full_quicksort[THEN fref_to_Down_curry, THEN order_trans])
     subgoal
       by (auto simp: rel2p_def var_order_rel_def p2rel_def Relation.total_on_def
         dest: string_trans)
     subgoal
       using total_on_lexord_less_than_char_linear2[unfolded var_order_rel_def]
       apply (auto simp: rel2p_def var_order_rel_def p2rel_def Relation.total_on_def less_char_def)
       done
     subgoal by fast
     apply (rule xs)
     apply (subst down_eq_id_list_rel)
     unfolding sorted_wrt_map sort_coeff_def
     apply (rule full_quicksort_correct_sorted[where R = \<open>(\<lambda>x y. x = y \<or> (x, y) \<in> var_order_rel)\<close> and h = \<open>id\<close>,
        THEN order_trans])
     subgoal
       by (auto simp: rel2p_def var_order_rel_def p2rel_def Relation.total_on_def dest: string_trans)
     subgoal for x y
       using total_on_lexord_less_than_char_linear2[unfolded var_order_rel_def]
       by (auto simp: rel2p_def var_order_rel_def p2rel_def Relation.total_on_def
         less_char_def)
    subgoal
     by (auto simp: rel2p_def p2rel_def rel2p_def[abs_def])
    done
 qed
 
 
 sepref_definition partition_main_vars_impl
   is \<open>uncurry2 partition_main_vars\<close>
   :: \<open>nat_assn\<^sup>k *\<^sub>a nat_assn\<^sup>k *\<^sub>a (monom_assn)\<^sup>k \<rightarrow>\<^sub>a prod_assn (monom_assn) nat_assn\<close>
   unfolding partition_main_vars_def partition_main_def
     var_order_rel_var_order
     var_order'_def[symmetric]
     term_order_rel'_alt_def
     le_term_order_rel'
     id_apply
     by sepref
 
 declare partition_main_vars_impl.refine[sepref_fr_rules]
 
 sepref_definition partition_between_vars_impl
   is \<open>uncurry2 partition_between_vars\<close>
   :: \<open>nat_assn\<^sup>k *\<^sub>a nat_assn\<^sup>k *\<^sub>a monom_assn\<^sup>k \<rightarrow>\<^sub>a prod_assn monom_assn nat_assn \<close>
   unfolding partition_between_vars_def partition_between_ref_def
     partition_main_vars_def[symmetric]
   unfolding choose_pivot3_def
     term_order_rel'_def[symmetric]
     term_order_rel'_alt_def choose_pivot_def
     le_term_order_rel' id_apply
   by sepref
 
 declare partition_between_vars_impl.refine[sepref_fr_rules]
 
 sepref_definition quicksort_vars_impl
   is \<open>uncurry2 quicksort_vars\<close>
   :: \<open>nat_assn\<^sup>k *\<^sub>a nat_assn\<^sup>k *\<^sub>a monom_assn\<^sup>k \<rightarrow>\<^sub>a monom_assn\<close>
   unfolding partition_main_vars_def quicksort_ref_def quicksort_vars_def
     partition_between_vars_def[symmetric]
   by sepref
 
 lemmas [sepref_fr_rules] = quicksort_vars_impl.refine
 
 sepref_register quicksort_vars
 
 
 lemma le_var_order_rel:
   \<open>(\<le>) = (\<lambda>x y. x = y \<or> (x, y) \<in> var_order_rel)\<close>
   by (intro ext)
    (auto simp add: less_list_def less_eq_list_def rel2p_def
       p2rel_def lexordp_conv_lexord p2rel_def var_order_rel_def
     lexordp_eq_conv_lexord lexordp_def)
 
 sepref_definition full_quicksort_vars_impl
   is \<open>full_quicksort_vars\<close>
   :: \<open>monom_assn\<^sup>k \<rightarrow>\<^sub>a monom_assn\<close>
   unfolding full_quicksort_vars_def full_quicksort_ref_def
     quicksort_vars_def[symmetric]
     le_var_order_rel[symmetric]
     term_order_rel'_def[symmetric]
     List.null_def
   by sepref
 
 
 lemmas sort_vars_spec_hnr =
   full_quicksort_vars_impl.refine[FCOMP full_quicksort_sort_vars_spec]
 
 lemma string_rel_order_map:
   \<open>(x, a) \<in> string_rel \<Longrightarrow>
        (y, aa) \<in> string_rel \<Longrightarrow>
        x \<le> y \<longleftrightarrow> a \<le> aa\<close>
   unfolding string_rel_def less_eq_literal.rep_eq less_than_char_def
     less_eq_list_def PAC_Polynomials_Term.less_char_def[symmetric]
   by (auto simp: string_rel_def less_eq_literal.rep_eq less_than_char_def
     less_eq_list_def char.lexordp_eq_conv_lexord lexordp_eq_refl
-    lexord_code lexordp_eq_conv_lexord
+    lexordp_char_char lexordp_eq_conv_lexord
     simp flip: less_char_def[abs_def])
 
 lemma merge_monoms_merge_monoms:
   \<open>(merge_monoms, merge_monoms) \<in> monom_rel \<rightarrow> monom_rel \<rightarrow> monom_rel\<close>
    unfolding merge_monoms_def
   apply (intro fun_relI)
   subgoal for a a' aa a'a
     apply (induction \<open>(\<lambda>(a :: String.literal)
       (b :: String.literal). a \<le> b)\<close> a aa
       arbitrary: a' a'a
       rule: merge.induct)
     subgoal
       by (auto elim!: list_relE3 list_relE4 list_relE list_relE2
         simp: string_rel_order_map)
     subgoal
       by (auto elim!: list_relE3 list_relE)
     subgoal
       by (auto elim!: list_relE3 list_relE4 list_relE list_relE2)
     done
   done
 
 lemma merge_monoms_merge_monoms2:
   \<open>(a, b) \<in> monom_rel \<Longrightarrow> (a', b') \<in> monom_rel \<Longrightarrow>
     (merge_monoms a a', merge_monoms b b') \<in> monom_rel\<close>
   using merge_monoms_merge_monoms
   unfolding fun_rel_def merge_monoms_def
   by auto
 
 
 lemma msort_monoms_impl:
   \<open>(msort_monoms_impl, merge_monoms_poly)
    \<in> monom_rel \<rightarrow> monom_rel\<close>
    unfolding msort_monoms_impl_def merge_monoms_poly_def
   apply (intro fun_relI)
   subgoal for a a'
     apply (induction \<open>(\<lambda>(a :: String.literal)
       (b :: String.literal). a \<le> b)\<close> a
       arbitrary: a'
       rule: msort.induct)
     subgoal
       by auto
     subgoal
       by (auto elim!: list_relE3 list_relE)
     subgoal premises p
       using p
       by (auto elim!: list_relE3 list_relE4 list_relE list_relE2
         simp: merge_monoms_def[symmetric] intro!: list_rel_takeD list_rel_dropD
         intro!: merge_monoms_merge_monoms2 p(1)[simplified] p(2)[simplified])
         (simp_all add: list_rel_imp_same_length)
     done
   done
 
 lemma merge_sort_monoms_sort_monoms_spec:
   \<open>(RETURN o merge_monoms_poly, sort_coeff) \<in> \<langle>Id\<rangle>list_rel \<rightarrow>\<^sub>f \<langle>\<langle>Id\<rangle>list_rel\<rangle>nres_rel\<close>
   unfolding merge_monoms_poly_def sort_coeff_def
   by (intro frefI nres_relI)
     (auto intro!: sorted_msort simp: sorted_wrt_map rel2p_def
      le_term_order_rel' transp_def rel2p_def[abs_def]
      simp flip: le_var_order_rel)
 
 sepref_register sort_coeff
 lemma  [sepref_fr_rules]:
   \<open>(return o msort_monoms_impl, sort_coeff) \<in> monom_assn\<^sup>k \<rightarrow>\<^sub>a monom_assn\<close>
   using msort_monoms_impl[sepref_param, FCOMP merge_sort_monoms_sort_monoms_spec]
   by auto
 
 sepref_definition sort_all_coeffs_impl
   is \<open>sort_all_coeffs\<close>
   :: \<open>poly_assn\<^sup>k \<rightarrow>\<^sub>a poly_assn\<close>
   unfolding sort_all_coeffs_def
     HOL_list.fold_custom_empty
   by sepref
 
 declare sort_all_coeffs_impl.refine[sepref_fr_rules]
 
 lemma merge_coeffs0_alt_def:
   \<open>(RETURN o merge_coeffs0) p =
    REC\<^sub>T(\<lambda>f p.
      (case p of
        [] \<Rightarrow> RETURN []
      | [p] => if snd p = 0 then RETURN [] else RETURN [p]
      | ((xs, n) # (ys, m) # p) \<Rightarrow>
       (if xs = ys
        then if n + m \<noteq> 0 then f ((xs, n + m) # p) else f p
        else if n = 0 then
           do {p \<leftarrow> f ((ys, m) # p);
             RETURN p}
        else do {p \<leftarrow> f ((ys, m) # p);
             RETURN ((xs, n) # p)})))
     p\<close>
   apply (subst eq_commute)
   apply (induction p rule: merge_coeffs0.induct)
   subgoal by (subst RECT_unfold, refine_mono) auto
   subgoal by (subst RECT_unfold, refine_mono) auto
   subgoal by (subst RECT_unfold, refine_mono) (auto simp: let_to_bind_conv)
   done
 
 text \<open>Again, Sepref does not understand what is going here.\<close>
 sepref_definition merge_coeffs0_impl
   is \<open>RETURN o merge_coeffs0\<close>
   :: \<open>poly_assn\<^sup>k \<rightarrow>\<^sub>a poly_assn\<close>
   supply [[goals_limit=1]]
   unfolding merge_coeffs0_alt_def
     HOL_list.fold_custom_empty
   apply sepref_dbg_preproc
   apply sepref_dbg_cons_init
   apply sepref_dbg_id
   apply sepref_dbg_monadify
   apply sepref_dbg_opt_init
   apply (rule WTF_RF | sepref_dbg_trans_step)+
   apply sepref_dbg_opt
   apply sepref_dbg_cons_solve
   apply sepref_dbg_cons_solve
   apply sepref_dbg_constraints
   done
 
 
 declare merge_coeffs0_impl.refine[sepref_fr_rules]
 
 sepref_definition fully_normalize_poly_impl
   is \<open>full_normalize_poly\<close>
   :: \<open>poly_assn\<^sup>k \<rightarrow>\<^sub>a poly_assn\<close>
   supply [[goals_limit=1]]
   unfolding full_normalize_poly_def
   by sepref
 
 declare fully_normalize_poly_impl.refine[sepref_fr_rules]
 
 
 end
\ No newline at end of file
diff --git a/thys/PAC_Checker/PAC_Checker_Relation.thy b/thys/PAC_Checker/PAC_Checker_Relation.thy
--- a/thys/PAC_Checker/PAC_Checker_Relation.thy
+++ b/thys/PAC_Checker/PAC_Checker_Relation.thy
@@ -1,389 +1,387 @@
 (*
   File:         PAC_Checker_Relation.thy
   Author:       Mathias Fleury, Daniela Kaufmann, JKU
   Maintainer:   Mathias Fleury, JKU
 *)
 theory PAC_Checker_Relation
   imports PAC_Checker WB_Sort "Native_Word.Uint64"
 begin
 
 section \<open>Various Refinement Relations\<close>
 
 text \<open>When writing this, it was not possible to share the definition with the IsaSAT version.\<close>
 definition uint64_nat_rel :: "(uint64 \<times> nat) set" where
  \<open>uint64_nat_rel = br nat_of_uint64 (\<lambda>_. True)\<close>
 
 abbreviation uint64_nat_assn where
   \<open>uint64_nat_assn \<equiv> pure uint64_nat_rel\<close>
 
 instantiation uint32 :: hashable
 begin
 definition hashcode_uint32 :: \<open>uint32 \<Rightarrow> uint32\<close> where
   \<open>hashcode_uint32 n = n\<close>
 
 definition def_hashmap_size_uint32 :: \<open>uint32 itself \<Rightarrow> nat\<close> where
   \<open>def_hashmap_size_uint32 = (\<lambda>_. 16)\<close>
   \<comment> \<open>same as @{typ nat}\<close>
 instance
   by standard (simp add: def_hashmap_size_uint32_def)
 end
 
 instantiation uint64 :: hashable
 begin
 definition hashcode_uint64 :: \<open>uint64 \<Rightarrow> uint32\<close> where
   \<open>hashcode_uint64 n = (uint32_of_nat (nat_of_uint64 ((n) AND ((2 :: uint64)^32 -1))))\<close>
 
 definition def_hashmap_size_uint64 :: \<open>uint64 itself \<Rightarrow> nat\<close> where
   \<open>def_hashmap_size_uint64 = (\<lambda>_. 16)\<close>
   \<comment> \<open>same as @{typ nat}\<close>
 instance
   by standard (simp add: def_hashmap_size_uint64_def)
 end
 
 lemma word_nat_of_uint64_Rep_inject[simp]: \<open>nat_of_uint64 ai = nat_of_uint64 bi \<longleftrightarrow> ai = bi\<close>
   by transfer simp
 
 instance uint64 :: heap
   by standard (auto simp: inj_def exI[of _ nat_of_uint64])
 
 instance uint64 :: semiring_numeral
   by standard
 
 lemma nat_of_uint64_012[simp]: \<open>nat_of_uint64 0 = 0\<close> \<open>nat_of_uint64 2 = 2\<close> \<open>nat_of_uint64 1 = 1\<close>
   by (transfer, auto)+
 
 definition uint64_of_nat_conv where
   [simp]: \<open>uint64_of_nat_conv (x :: nat) = x\<close>
 lemma less_upper_bintrunc_id: \<open>n < 2 ^b \<Longrightarrow> n \<ge> 0 \<Longrightarrow> bintrunc b n = n\<close>
   unfolding uint32_of_nat_def
   by (simp add: no_bintr_alt1)
 
 lemma nat_of_uint64_uint64_of_nat_id: \<open>n < 2^64 \<Longrightarrow> nat_of_uint64 (uint64_of_nat n) = n\<close>
   unfolding uint64_of_nat_def
   apply simp
   apply transfer
-  apply (auto simp: unat_def)
+  apply (subst unat_eq_nat_uint)
   apply transfer
   by (auto simp: less_upper_bintrunc_id)
 
 lemma [sepref_fr_rules]:
   \<open>(return o uint64_of_nat, RETURN o uint64_of_nat_conv) \<in> [\<lambda>a. a < 2 ^64]\<^sub>a nat_assn\<^sup>k \<rightarrow> uint64_nat_assn\<close>
   by sepref_to_hoare
    (sep_auto simp: uint64_nat_rel_def br_def nat_of_uint64_uint64_of_nat_id)
 
 definition string_rel :: \<open>(String.literal \<times> string) set\<close> where
   \<open>string_rel = {(x, y). y = String.explode x}\<close>
 
 abbreviation string_assn :: \<open>string \<Rightarrow> String.literal \<Rightarrow> assn\<close> where
   \<open>string_assn \<equiv> pure string_rel\<close>
 
 lemma eq_string_eq:
   \<open>((=), (=)) \<in> string_rel \<rightarrow> string_rel \<rightarrow> bool_rel\<close>
  by (auto intro!: frefI simp: string_rel_def String.less_literal_def
     less_than_char_def rel2p_def literal.explode_inject)
 
 lemmas eq_string_eq_hnr =
    eq_string_eq[sepref_import_param]
 
 definition string2_rel :: \<open>(string \<times> string) set\<close> where
   \<open>string2_rel \<equiv> \<langle>Id\<rangle>list_rel\<close>
 
 abbreviation string2_assn :: \<open>string \<Rightarrow> string \<Rightarrow> assn\<close> where
   \<open>string2_assn \<equiv> pure string2_rel\<close>
 
 abbreviation monom_rel where
   \<open>monom_rel \<equiv> \<langle>string_rel\<rangle>list_rel\<close>
 
 abbreviation monom_assn where
   \<open>monom_assn \<equiv> list_assn string_assn\<close>
 
 abbreviation monomial_rel where
   \<open>monomial_rel \<equiv> monom_rel \<times>\<^sub>r int_rel\<close>
 
 abbreviation monomial_assn where
   \<open>monomial_assn \<equiv> monom_assn \<times>\<^sub>a int_assn\<close>
 
 abbreviation poly_rel where
   \<open>poly_rel \<equiv> \<langle>monomial_rel\<rangle>list_rel\<close>
 
 
 abbreviation poly_assn where
   \<open>poly_assn \<equiv> list_assn monomial_assn\<close>
 
 lemma poly_assn_alt_def:
   \<open>poly_assn = pure poly_rel\<close>
   by (simp add: list_assn_pure_conv)
 
 abbreviation polys_assn where
   \<open>polys_assn \<equiv> hm_fmap_assn uint64_nat_assn poly_assn\<close>
 
 lemma string_rel_string_assn:
   \<open>(\<up> ((c, a) \<in> string_rel)) = string_assn a c\<close>
   by (auto simp: pure_app_eq)
 
 lemma single_valued_string_rel:
    \<open>single_valued string_rel\<close>
    by (auto simp: single_valued_def string_rel_def)
 
 lemma IS_LEFT_UNIQUE_string_rel:
    \<open>IS_LEFT_UNIQUE string_rel\<close>
    by (auto simp: IS_LEFT_UNIQUE_def single_valued_def string_rel_def
      literal.explode_inject)
 
 lemma IS_RIGHT_UNIQUE_string_rel:
    \<open>IS_RIGHT_UNIQUE string_rel\<close>
    by (auto simp: single_valued_def string_rel_def
      literal.explode_inject)
 
 lemma single_valued_monom_rel: \<open>single_valued monom_rel\<close>
   by (rule list_rel_sv)
     (auto intro!: frefI simp: string_rel_def
     rel2p_def single_valued_def p2rel_def)
 
 lemma single_valued_monomial_rel:
   \<open>single_valued monomial_rel\<close>
   using single_valued_monom_rel
   by (auto intro!: frefI simp:
     rel2p_def single_valued_def p2rel_def)
 
 lemma single_valued_monom_rel': \<open>IS_LEFT_UNIQUE monom_rel\<close>
   unfolding IS_LEFT_UNIQUE_def inv_list_rel_eq string2_rel_def
   by (rule list_rel_sv)+
    (auto intro!: frefI simp: string_rel_def
     rel2p_def single_valued_def p2rel_def literal.explode_inject)
 
 
 lemma single_valued_monomial_rel':
   \<open>IS_LEFT_UNIQUE monomial_rel\<close>
   using single_valued_monom_rel'
   unfolding IS_LEFT_UNIQUE_def inv_list_rel_eq
   by (auto intro!: frefI simp:
     rel2p_def single_valued_def p2rel_def)
 
 lemma [safe_constraint_rules]:
   \<open>Sepref_Constraints.CONSTRAINT single_valued string_rel\<close>
   \<open>Sepref_Constraints.CONSTRAINT IS_LEFT_UNIQUE string_rel\<close>
   by (auto simp: CONSTRAINT_def single_valued_def
     string_rel_def IS_LEFT_UNIQUE_def literal.explode_inject)
 
 lemma eq_string_monom_hnr[sepref_fr_rules]:
   \<open>(uncurry (return oo (=)), uncurry (RETURN oo (=))) \<in> monom_assn\<^sup>k *\<^sub>a monom_assn\<^sup>k \<rightarrow>\<^sub>a bool_assn\<close>
   using single_valued_monom_rel' single_valued_monom_rel
   unfolding list_assn_pure_conv
   by sepref_to_hoare
    (sep_auto simp: list_assn_pure_conv string_rel_string_assn
        single_valued_def IS_LEFT_UNIQUE_def
      dest!: mod_starD
      simp flip: inv_list_rel_eq)
 
 
 definition term_order_rel' where
   [simp]: \<open>term_order_rel' x y = ((x, y) \<in> term_order_rel)\<close>
 
 lemma term_order_rel[def_pat_rules]:
   \<open>(\<in>)$(x,y)$term_order_rel \<equiv> term_order_rel'$x$y\<close>
   by auto
 
 lemma term_order_rel_alt_def:
   \<open>term_order_rel = lexord (p2rel char.lexordp)\<close>
   by (auto simp: p2rel_def char.lexordp_conv_lexord var_order_rel_def intro!: arg_cong[of _ _ lexord])
 
 
 instantiation char :: linorder
 begin
   definition less_char where [symmetric, simp]: "less_char = PAC_Polynomials_Term.less_char"
   definition less_eq_char where [symmetric, simp]: "less_eq_char = PAC_Polynomials_Term.less_eq_char"
 instance
   apply standard
   using char.linorder_axioms
   by (auto simp: class.linorder_def class.order_def class.preorder_def
        less_eq_char_def less_than_char_def class.order_axioms_def
        class.linorder_axioms_def p2rel_def less_char_def)
 end
 
 
 instantiation list :: (linorder) linorder
 begin
   definition less_list where  "less_list = lexordp (<)"
   definition less_eq_list where "less_eq_list = lexordp_eq"
 
 instance
 proof standard
   have [dest]: \<open>\<And>x y :: 'a :: linorder list. (x, y) \<in> lexord {(x, y). x < y} \<Longrightarrow>
            lexordp_eq y x \<Longrightarrow> False\<close>
     by (metis lexordp_antisym lexordp_conv_lexord lexordp_eq_conv_lexord)
   have [simp]: \<open>\<And>x y :: 'a :: linorder list. lexordp_eq x y \<Longrightarrow>
            \<not> lexordp_eq y x \<Longrightarrow>
            (x, y) \<in> lexord {(x, y). x < y}\<close>
     using lexordp_conv_lexord lexordp_conv_lexordp_eq by blast
   show
    \<open>(x < y) = Restricted_Predicates.strict (\<le>) x y\<close>
    \<open>x \<le> x\<close>
    \<open>x \<le> y \<Longrightarrow> y \<le> z \<Longrightarrow> x \<le> z\<close>
    \<open>x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y\<close>
    \<open>x \<le> y \<or> y \<le> x\<close>
    for x y z :: \<open>'a :: linorder list\<close>
     by (auto simp: less_list_def less_eq_list_def List.lexordp_def
     lexordp_conv_lexord lexordp_into_lexordp_eq lexordp_antisym
     antisym_def lexordp_eq_refl lexordp_eq_linear intro: lexordp_eq_trans
     dest: lexordp_eq_antisym)
 qed
 
 end
 
 
 lemma term_order_rel'_alt_def_lexord:
     \<open>term_order_rel' x y = ord_class.lexordp x y\<close> and
   term_order_rel'_alt_def:
     \<open>term_order_rel' x y \<longleftrightarrow> x < y\<close>
 proof -
   show
     \<open>term_order_rel' x y = ord_class.lexordp x y\<close>
     \<open>term_order_rel' x y \<longleftrightarrow> x < y\<close>
     unfolding less_than_char_of_char[symmetric, abs_def]
     by (auto simp: lexordp_conv_lexord less_eq_list_def
          less_list_def lexordp_def var_order_rel_def
          rel2p_def term_order_rel_alt_def p2rel_def)
 qed
 
 lemma list_rel_list_rel_order_iff:
   assumes \<open>(a, b) \<in> \<langle>string_rel\<rangle>list_rel\<close> \<open>(a', b') \<in> \<langle>string_rel\<rangle>list_rel\<close>
   shows \<open>a < a' \<longleftrightarrow> b < b'\<close>
 proof
   have H: \<open>(a, b) \<in> \<langle>string_rel\<rangle>list_rel \<Longrightarrow>
        (a, cs) \<in> \<langle>string_rel\<rangle>list_rel \<Longrightarrow> b = cs\<close> for cs
      using single_valued_monom_rel' IS_RIGHT_UNIQUE_string_rel
      unfolding string2_rel_def
      by (subst (asm)list_rel_sv_iff[symmetric])
        (auto simp: single_valued_def)
   assume \<open>a < a'\<close>
   then consider
     u u' where \<open>a' = a @ u # u'\<close> |
     u aa v w aaa where \<open>a = u @ aa # v\<close> \<open>a' = u @ aaa # w\<close> \<open>aa < aaa\<close>
     by (subst (asm) less_list_def)
      (auto simp: lexord_def List.lexordp_def
       list_rel_append1 list_rel_split_right_iff)
   then show \<open>b < b'\<close>
   proof cases
     case 1
     then show \<open>b < b'\<close>
       using assms
       by (subst less_list_def)
         (auto simp: lexord_def List.lexordp_def
         list_rel_append1 list_rel_split_right_iff dest: H)
   next
     case 2
     then obtain u' aa' v' w' aaa' where
        \<open>b = u' @ aa' # v'\<close> \<open>b' = u' @ aaa' # w'\<close>
        \<open>(aa, aa') \<in> string_rel\<close>
        \<open>(aaa, aaa') \<in> string_rel\<close>
       using assms
       by (smt list_rel_append1 list_rel_split_right_iff single_valued_def single_valued_monom_rel)
     with \<open>aa < aaa\<close> have \<open>aa' < aaa'\<close>
       by (auto simp: string_rel_def less_literal.rep_eq less_list_def
         lexordp_conv_lexord lexordp_def char.lexordp_conv_lexord
-          simp flip: lexord_code less_char_def
-            PAC_Polynomials_Term.less_char_def)
+          simp flip: less_char_def PAC_Polynomials_Term.less_char_def)
     then show \<open>b < b'\<close>
       using \<open>b = u' @ aa' # v'\<close> \<open>b' = u' @ aaa' # w'\<close>
       by (subst less_list_def)
         (fastforce simp: lexord_def List.lexordp_def
         list_rel_append1 list_rel_split_right_iff)
   qed
 next
   have H: \<open>(a, b) \<in> \<langle>string_rel\<rangle>list_rel \<Longrightarrow>
        (a', b) \<in> \<langle>string_rel\<rangle>list_rel \<Longrightarrow> a = a'\<close> for a a' b
      using single_valued_monom_rel'
      by (auto simp: single_valued_def IS_LEFT_UNIQUE_def
        simp flip: inv_list_rel_eq)
   assume \<open>b < b'\<close>
   then consider
     u u' where \<open>b' = b @ u # u'\<close> |
     u aa v w aaa where \<open>b = u @ aa # v\<close> \<open>b' = u @ aaa # w\<close> \<open>aa < aaa\<close>
     by (subst (asm) less_list_def)
      (auto simp: lexord_def List.lexordp_def
       list_rel_append1 list_rel_split_right_iff)
   then show \<open>a < a'\<close>
   proof cases
     case 1
     then show \<open>a < a'\<close>
       using assms
       by (subst less_list_def)
         (auto simp: lexord_def List.lexordp_def
         list_rel_append2 list_rel_split_left_iff dest: H)
   next
     case 2
     then obtain u' aa' v' w' aaa' where
        \<open>a = u' @ aa' # v'\<close> \<open>a' = u' @ aaa' # w'\<close>
        \<open>(aa', aa) \<in> string_rel\<close>
        \<open>(aaa', aaa) \<in> string_rel\<close>
       using assms
       by (auto simp: lexord_def List.lexordp_def
         list_rel_append2 list_rel_split_left_iff dest: H)
     with \<open>aa < aaa\<close> have \<open>aa' < aaa'\<close>
       by (auto simp: string_rel_def less_literal.rep_eq less_list_def
         lexordp_conv_lexord lexordp_def char.lexordp_conv_lexord
-          simp flip: lexord_code less_char_def
-            PAC_Polynomials_Term.less_char_def)
+          simp flip: less_char_def PAC_Polynomials_Term.less_char_def)
     then show \<open>a < a'\<close>
       using \<open>a = u' @ aa' # v'\<close> \<open>a' = u' @ aaa' # w'\<close>
       by (subst less_list_def)
         (fastforce simp: lexord_def List.lexordp_def
         list_rel_append1 list_rel_split_right_iff)
   qed
 qed
 
 
 lemma string_rel_le[sepref_import_param]:
   shows \<open>((<), (<)) \<in> \<langle>string_rel\<rangle>list_rel \<rightarrow>  \<langle>string_rel\<rangle>list_rel \<rightarrow> bool_rel\<close>
   by (auto intro!: fun_relI simp: list_rel_list_rel_order_iff)
 
 (* TODO Move *)
 lemma [sepref_import_param]:
   assumes \<open>CONSTRAINT IS_LEFT_UNIQUE R\<close>  \<open>CONSTRAINT IS_RIGHT_UNIQUE R\<close>
   shows \<open>(remove1, remove1) \<in> R \<rightarrow> \<langle>R\<rangle>list_rel \<rightarrow> \<langle>R\<rangle>list_rel\<close>
   apply (intro fun_relI)
   subgoal premises p for x y xs ys
     using p(2) p(1) assms
     by (induction xs ys rule: list_rel_induct)
       (auto simp: IS_LEFT_UNIQUE_def single_valued_def)
   done
 
 instantiation pac_step :: (heap, heap, heap) heap
 begin
 
 instance
 proof standard
   obtain f :: \<open>'a \<Rightarrow> nat\<close> where
     f: \<open>inj f\<close>
     by blast
   obtain g :: \<open>nat \<times> nat \<times> nat \<times> nat \<times> nat \<Rightarrow> nat\<close> where
     g: \<open>inj g\<close>
     by blast
   obtain h :: \<open>'b \<Rightarrow> nat\<close> where
     h: \<open>inj h\<close>
     by blast
   obtain i :: \<open>'c \<Rightarrow> nat\<close> where
     i: \<open>inj i\<close>
     by blast
   have [iff]: \<open>g a = g b \<longleftrightarrow> a = b\<close>\<open>h a'' = h b'' \<longleftrightarrow> a'' = b''\<close>  \<open>f a' = f b' \<longleftrightarrow> a' = b'\<close>
     \<open>i a''' = i b''' \<longleftrightarrow> a''' = b'''\<close>  for a b a' b' a'' b'' a''' b'''
     using f g h i unfolding inj_def by blast+
   let ?f = \<open>\<lambda>x :: ('a, 'b, 'c) pac_step.
      g (case x of
         Add a b c d \<Rightarrow>     (0, i a,  i b,  i c, f d)
       | Del a  \<Rightarrow>          (1, i a,    0,   0,   0)
       | Mult a b c d \<Rightarrow>    (2, i a, f b, i c, f d)
       | Extension a b c \<Rightarrow> (3, i a, f c, 0, h b))\<close>
    have \<open>inj ?f\<close>
      apply (auto simp: inj_def)
      apply (case_tac x; case_tac y)
      apply auto
      done
    then show \<open>\<exists>f :: ('a, 'b, 'c) pac_step \<Rightarrow> nat. inj f\<close>
      by blast
 qed
 
 end
 
 end
\ No newline at end of file
diff --git a/thys/PAC_Checker/PAC_Polynomials.thy b/thys/PAC_Checker/PAC_Polynomials.thy
--- a/thys/PAC_Checker/PAC_Polynomials.thy
+++ b/thys/PAC_Checker/PAC_Polynomials.thy
@@ -1,490 +1,489 @@
 theory PAC_Polynomials
   imports PAC_Specification Finite_Map_Multiset
 begin
 
 
 section \<open>Polynomials of strings\<close>
 
 text \<open>
 
   Isabelle's definition of polynomials only work with variables of type
   \<^typ>\<open>nat\<close>. Therefore, we introduce a version that uses strings by using an injective function
   that converts a string to a natural number. It exists because strings are countable. Remark that
   the whole development is independent of the function.
 
 \<close>
 
 subsection \<open>Polynomials and Variables\<close>
 
 lemma poly_embed_EX:
   \<open>\<exists>\<phi>. bij (\<phi> :: string \<Rightarrow> nat)\<close>
   by (rule countableE_infinite[of \<open>UNIV :: string set\<close>])
      (auto intro!: infinite_UNIV_listI)
 
 text \<open>Using a multiset instead of a list has some advantage from an abstract point of view. First,
   we can have monomials that appear several times  and the coefficient can also be zero. Basically,
   we can represent un-normalised polynomials, which is very useful to talk about intermediate states
   in our program.
 \<close>
 type_synonym term_poly = \<open>string multiset\<close>
 type_synonym mset_polynomial =
   \<open>(term_poly * int) multiset\<close>
 
 definition normalized_poly :: \<open>mset_polynomial \<Rightarrow> bool\<close> where
   \<open>normalized_poly p \<longleftrightarrow>
      distinct_mset (fst `# p) \<and>
      0 \<notin># snd `# p\<close>
 
 lemma normalized_poly_simps[simp]:
   \<open>normalized_poly {#}\<close>
   \<open>normalized_poly (add_mset t p) \<longleftrightarrow> snd t \<noteq> 0 \<and>
     fst t \<notin># fst `# p \<and> normalized_poly p\<close>
   by (auto simp: normalized_poly_def)
 
 lemma normalized_poly_mono:
   \<open>normalized_poly B \<Longrightarrow> A \<subseteq># B \<Longrightarrow> normalized_poly A\<close>
   unfolding normalized_poly_def
   by (auto intro: distinct_mset_mono image_mset_subseteq_mono)
 
 definition mult_poly_by_monom :: \<open>term_poly * int \<Rightarrow> mset_polynomial \<Rightarrow> mset_polynomial\<close> where
   \<open>mult_poly_by_monom  = (\<lambda>ys q. image_mset (\<lambda>xs. (fst xs + fst ys, snd ys * snd xs)) q)\<close>
 
 
 definition mult_poly_raw :: \<open>mset_polynomial \<Rightarrow> mset_polynomial \<Rightarrow> mset_polynomial\<close> where
   \<open>mult_poly_raw p q =
     (sum_mset ((\<lambda>y. mult_poly_by_monom y q) `# p))\<close>
 
 
 definition remove_powers :: \<open>mset_polynomial \<Rightarrow> mset_polynomial\<close> where
   \<open>remove_powers xs =  image_mset (apfst remdups_mset) xs\<close>
 
 
 definition all_vars_mset :: \<open>mset_polynomial \<Rightarrow> string multiset\<close> where
   \<open>all_vars_mset p = \<Union># (fst `# p)\<close>
 
 abbreviation all_vars :: \<open>mset_polynomial \<Rightarrow> string set\<close> where
   \<open>all_vars p \<equiv> set_mset (all_vars_mset p)\<close>
 
 definition add_to_coefficient :: \<open>_ \<Rightarrow> mset_polynomial \<Rightarrow> mset_polynomial\<close>  where
   \<open>add_to_coefficient = (\<lambda>(a, n) b. {#(a', _) \<in># b. a' \<noteq> a#} +
              (if n + sum_mset (snd `# {#(a', _) \<in># b. a' = a#}) = 0 then {#}
                else {#(a, n + sum_mset (snd `# {#(a', _) \<in># b. a' = a#}))#}))\<close>
 
 definition normalize_poly :: \<open>mset_polynomial \<Rightarrow> mset_polynomial\<close> where
   \<open>normalize_poly p = fold_mset add_to_coefficient {#} p\<close>
 
 lemma add_to_coefficient_simps:
   \<open>n + sum_mset (snd `# {#(a', _) \<in># b. a' = a#}) \<noteq> 0 \<Longrightarrow>
     add_to_coefficient (a, n) b = {#(a', _) \<in># b. a' \<noteq> a#} +
              {#(a, n + sum_mset (snd `# {#(a', _) \<in># b. a' = a#}))#}\<close>
   \<open>n + sum_mset (snd `# {#(a', _) \<in># b. a' = a#}) = 0 \<Longrightarrow>
     add_to_coefficient (a, n) b = {#(a', _) \<in># b. a' \<noteq> a#}\<close> and
   add_to_coefficient_simps_If:
   \<open>add_to_coefficient (a, n) b = {#(a', _) \<in># b. a' \<noteq> a#} +
              (if n + sum_mset (snd `# {#(a', _) \<in># b. a' = a#}) = 0 then {#}
                else {#(a, n + sum_mset (snd `# {#(a', _) \<in># b. a' = a#}))#})\<close>
   by (auto simp: add_to_coefficient_def)
 
 interpretation comp_fun_commute \<open>add_to_coefficient\<close>
 proof -
-  have [simp]:
+  have [iff]:
     \<open>a \<noteq> aa \<Longrightarrow>
-    ((case x of (a', _) \<Rightarrow> a' \<noteq> aa) \<and> (case x of (a', _) \<Rightarrow> a' = a)) \<longleftrightarrow>
+    ((case x of (a', _) \<Rightarrow> a' = a) \<and> (case x of (a', _) \<Rightarrow> a' \<noteq> aa)) \<longleftrightarrow>
     (case x of (a', _) \<Rightarrow> a' = a)\<close> for a' aa a x
     by auto
   show \<open>comp_fun_commute add_to_coefficient\<close>
     unfolding add_to_coefficient_def
     by standard
-      (auto intro!: ext simp: filter_filter_mset ac_simps add_eq_0_iff
-      intro: filter_mset_cong)
+     (auto intro!: ext simp: filter_filter_mset ac_simps add_eq_0_iff)
 qed
 
 lemma normalized_poly_normalize_poly[simp]:
   \<open>normalized_poly (normalize_poly p)\<close>
   unfolding normalize_poly_def
   apply (induction p)
   subgoal by auto
   subgoal for x p
     by (cases x)
       (auto simp: add_to_coefficient_simps_If
       intro: normalized_poly_mono)
   done
 
 
 subsection \<open>Addition\<close>
 
 inductive add_poly_p :: \<open>mset_polynomial \<times> mset_polynomial \<times> mset_polynomial \<Rightarrow> mset_polynomial \<times> mset_polynomial \<times> mset_polynomial \<Rightarrow> bool\<close> where
 add_new_coeff_r:
     \<open>add_poly_p (p, add_mset x q, r) (p, q, add_mset x r)\<close> |
 add_new_coeff_l:
     \<open>add_poly_p (add_mset x p, q, r) (p, q, add_mset x r)\<close> |
 add_same_coeff_l:
     \<open>add_poly_p (add_mset (x, n) p, q, add_mset (x, m) r) (p, q, add_mset (x, n + m) r)\<close> |
 add_same_coeff_r:
     \<open>add_poly_p (p, add_mset (x, n) q, add_mset (x, m) r) (p, q, add_mset (x, n + m) r)\<close> |
 rem_0_coeff:
     \<open>add_poly_p (p, q, add_mset (x, 0) r) (p, q, r)\<close>
 
 inductive_cases add_poly_pE: \<open>add_poly_p S T\<close>
 
 lemmas add_poly_p_induct =
   add_poly_p.induct[split_format(complete)]
 
 lemma add_poly_p_empty_l:
   \<open>add_poly_p\<^sup>*\<^sup>* (p, q, r) ({#}, q, p + r)\<close>
   apply (induction p arbitrary: r)
   subgoal by auto
   subgoal
     by (metis (no_types, lifting) add_new_coeff_l r_into_rtranclp
       rtranclp_trans union_mset_add_mset_left union_mset_add_mset_right)
   done
 
 lemma add_poly_p_empty_r:
   \<open>add_poly_p\<^sup>*\<^sup>* (p, q, r) (p, {#}, q + r)\<close>
   apply (induction q arbitrary: r)
   subgoal by auto
   subgoal
     by (metis (no_types, lifting) add_new_coeff_r r_into_rtranclp
       rtranclp_trans union_mset_add_mset_left union_mset_add_mset_right)
   done
 
 lemma add_poly_p_sym:
   \<open>add_poly_p (p, q, r) (p', q', r') \<longleftrightarrow> add_poly_p (q, p, r) (q', p', r')\<close>
   apply (rule iffI)
   subgoal
     by (cases rule: add_poly_p.cases, assumption)
       (auto intro: add_poly_p.intros)
   subgoal
     by (cases rule: add_poly_p.cases, assumption)
       (auto intro: add_poly_p.intros)
   done
 
 lemma wf_if_measure_in_wf:
   \<open>wf R \<Longrightarrow> (\<And>a b. (a, b) \<in> S \<Longrightarrow> (\<nu> a, \<nu> b)\<in>R) \<Longrightarrow> wf S\<close>
   by (metis in_inv_image wfE_min wfI_min wf_inv_image)
 
 lemma lexn_n:
   \<open>n > 0 \<Longrightarrow> (x # xs, y # ys) \<in> lexn r n \<longleftrightarrow>
   (length xs = n-1 \<and> length ys = n-1) \<and> ((x, y) \<in> r \<or> (x = y \<and> (xs, ys) \<in> lexn r (n - 1)))\<close>
   apply (cases n)
    apply simp
   by (auto simp: map_prod_def image_iff lex_prod_def)
 
 lemma wf_add_poly_p:
   \<open>wf {(x, y). add_poly_p y x}\<close>
   by (rule wf_if_measure_in_wf[where R = \<open>lexn less_than 3\<close> and
      \<nu> = \<open>\<lambda>(a,b,c). [size a , size b, size c]\<close>])
     (auto simp: add_poly_p.simps wf_lexn
      simp: lexn_n simp del: lexn.simps(2))
 
 lemma mult_poly_by_monom_simps[simp]:
   \<open>mult_poly_by_monom t {#} = {#}\<close>
   \<open>mult_poly_by_monom t (ps + qs) =  mult_poly_by_monom t ps + mult_poly_by_monom t qs\<close>
   \<open>mult_poly_by_monom a (add_mset p ps) = add_mset (fst a + fst p, snd a * snd p) (mult_poly_by_monom a ps)\<close>
 proof -
   interpret comp_fun_commute \<open>(\<lambda>xs. add_mset (xs + t))\<close> for t
     by standard auto
   show
     \<open>mult_poly_by_monom t (ps + qs) =  mult_poly_by_monom t ps + mult_poly_by_monom t qs\<close> for t
     by (induction ps)
       (auto simp: mult_poly_by_monom_def)
   show
     \<open>mult_poly_by_monom a (add_mset p ps) = add_mset (fst a + fst p, snd a * snd p) (mult_poly_by_monom a ps)\<close>
     \<open>mult_poly_by_monom t {#} = {#}\<close>for t
     by (auto simp: mult_poly_by_monom_def)
 qed
 
 inductive mult_poly_p :: \<open>mset_polynomial \<Rightarrow> mset_polynomial \<times> mset_polynomial \<Rightarrow> mset_polynomial \<times> mset_polynomial \<Rightarrow> bool\<close>
   for q :: mset_polynomial where
 mult_step:
     \<open>mult_poly_p q (add_mset (xs, n) p, r) (p, (\<lambda>(ys, m). (remdups_mset (xs + ys), n * m)) `# q + r)\<close>
 
 
 lemmas mult_poly_p_induct = mult_poly_p.induct[split_format(complete)]
 
 subsection \<open>Normalisation\<close>
 
 inductive normalize_poly_p :: \<open>mset_polynomial \<Rightarrow> mset_polynomial \<Rightarrow> bool\<close>where
 rem_0_coeff[simp, intro]:
     \<open>normalize_poly_p p q \<Longrightarrow> normalize_poly_p (add_mset (xs, 0) p) q\<close> |
 merge_dup_coeff[simp, intro]:
     \<open>normalize_poly_p p q \<Longrightarrow> normalize_poly_p (add_mset (xs, m) (add_mset (xs, n) p)) (add_mset (xs, m + n) q)\<close> |
 same[simp, intro]:
     \<open>normalize_poly_p p p\<close> |
 keep_coeff[simp, intro]:
     \<open>normalize_poly_p p q \<Longrightarrow> normalize_poly_p (add_mset x p) (add_mset x q)\<close>
 
 
 subsection \<open>Correctness\<close>
 text \<open>
   This locales maps string polynomials to real polynomials.
 \<close>
 locale poly_embed =
   fixes \<phi> :: \<open>string \<Rightarrow> nat\<close>
   assumes \<phi>_inj: \<open>inj \<phi>\<close>
 begin
 
 definition poly_of_vars :: "term_poly \<Rightarrow> ('a :: {comm_semiring_1}) mpoly" where
   \<open>poly_of_vars xs = fold_mset (\<lambda>a b. Var (\<phi> a) * b) (1 :: 'a mpoly) xs\<close>
 
 lemma poly_of_vars_simps[simp]:
   shows
     \<open>poly_of_vars (add_mset x xs) = Var (\<phi> x) * (poly_of_vars xs :: ('a :: {comm_semiring_1}) mpoly)\<close> (is ?A) and
     \<open>poly_of_vars (xs + ys) = poly_of_vars xs * (poly_of_vars ys :: ('a :: {comm_semiring_1}) mpoly)\<close> (is ?B)
 proof -
   interpret comp_fun_commute \<open>(\<lambda>a b. (b :: 'a :: {comm_semiring_1} mpoly) * Var (\<phi> a))\<close>
     by standard
       (auto simp: algebra_simps ac_simps
          Var_def times_monomial_monomial intro!: ext)
 
   show ?A
     by (auto simp: poly_of_vars_def comp_fun_commute_axioms fold_mset_fusion
       ac_simps)
   show ?B
     apply (auto simp: poly_of_vars_def ac_simps)
     by (simp add: local.comp_fun_commute_axioms local.fold_mset_fusion
       semiring_normalization_rules(18))
 qed
 
 
 definition mononom_of_vars where
   \<open>mononom_of_vars \<equiv> (\<lambda>(xs, n). (+) (Const n * poly_of_vars xs))\<close>
 
 interpretation comp_fun_commute \<open>mononom_of_vars\<close>
   by standard
     (auto simp: algebra_simps ac_simps mononom_of_vars_def
        Var_def times_monomial_monomial intro!: ext)
 
 lemma [simp]:
   \<open>poly_of_vars {#} = 1\<close>
   by (auto simp: poly_of_vars_def)
 
 lemma mononom_of_vars_add[simp]:
   \<open>NO_MATCH 0 b \<Longrightarrow> mononom_of_vars xs b = Const (snd xs) * poly_of_vars (fst xs) + b\<close>
   by (cases xs)
     (auto simp: ac_simps mononom_of_vars_def)
 
 definition polynomial_of_mset :: \<open>mset_polynomial \<Rightarrow> _\<close> where
   \<open>polynomial_of_mset p = sum_mset (mononom_of_vars `# p) 0\<close>
 
 lemma polynomial_of_mset_append[simp]:
   \<open>polynomial_of_mset (xs + ys) = polynomial_of_mset xs + polynomial_of_mset ys\<close>
   by (auto simp: ac_simps Const_def polynomial_of_mset_def)
 
 lemma polynomial_of_mset_Cons[simp]:
   \<open>polynomial_of_mset (add_mset x ys) = Const (snd x) * poly_of_vars (fst x) + polynomial_of_mset ys\<close>
   by (cases x)
     (auto simp: ac_simps polynomial_of_mset_def mononom_of_vars_def)
 
 lemma polynomial_of_mset_empty[simp]:
   \<open>polynomial_of_mset {#} = 0\<close>
   by (auto simp: polynomial_of_mset_def)
 
 lemma polynomial_of_mset_mult_poly_by_monom[simp]:
   \<open>polynomial_of_mset (mult_poly_by_monom x ys) =
        (Const (snd x) * poly_of_vars (fst x) * polynomial_of_mset ys)\<close>
  by (induction ys)
    (auto simp: Const_mult algebra_simps)
 
 lemma polynomial_of_mset_mult_poly_raw[simp]:
   \<open>polynomial_of_mset (mult_poly_raw xs ys) = polynomial_of_mset xs * polynomial_of_mset ys\<close>
   unfolding mult_poly_raw_def
   by (induction xs arbitrary: ys)
    (auto simp: Const_mult algebra_simps)
 
 lemma polynomial_of_mset_uminus:
   \<open>polynomial_of_mset {#case x of (a, b) \<Rightarrow> (a, - b). x \<in># za#} =
     - polynomial_of_mset za\<close>
   by (induction za)
     auto
 
 
 lemma X2_X_polynomial_bool_mult_in:
   \<open>Var (x1) * (Var (x1) * p) -  Var (x1) * p \<in> More_Modules.ideal polynomial_bool\<close>
   using ideal_mult_right_in[OF  X2_X_in_pac_ideal[of x1 \<open>{}\<close>, unfolded pac_ideal_def], of p]
   by (auto simp: right_diff_distrib ac_simps power2_eq_square)
 
 
 lemma polynomial_of_list_remove_powers_polynomial_bool:
   \<open>(polynomial_of_mset xs) - polynomial_of_mset (remove_powers xs) \<in> ideal polynomial_bool\<close>
 proof (induction xs)
   case empty
   then show \<open>?case\<close> by (auto simp: remove_powers_def ideal.span_zero)
 next
   case (add x xs)
   have H1: \<open>x1 \<in># x2 \<Longrightarrow>
        Var (\<phi> x1) * poly_of_vars x2 - p \<in> More_Modules.ideal polynomial_bool \<longleftrightarrow>
        poly_of_vars x2 - p \<in> More_Modules.ideal polynomial_bool
        \<close> for x1 x2 p
     apply (subst (2) ideal.span_add_eq[symmetric,
       of \<open>Var (\<phi> x1) * poly_of_vars x2 - poly_of_vars x2\<close>])
     apply (drule multi_member_split)
     apply (auto simp: X2_X_polynomial_bool_mult_in)
     done
 
   have diff: \<open>poly_of_vars (x) - poly_of_vars (remdups_mset (x)) \<in> ideal polynomial_bool\<close> for x
     by (induction x)
      (auto simp: remove_powers_def ideal.span_zero H1
       simp flip: right_diff_distrib intro!: ideal.span_scale)
   have [simp]: \<open>polynomial_of_mset xs -
     polynomial_of_mset (apfst remdups_mset `# xs)
     \<in> More_Modules.ideal polynomial_bool \<Longrightarrow>
     poly_of_vars ys * poly_of_vars ys -
     poly_of_vars ys * poly_of_vars (remdups_mset ys)
     \<in> More_Modules.ideal polynomial_bool \<Longrightarrow>
     polynomial_of_mset xs + Const y * poly_of_vars ys -
     (polynomial_of_mset (apfst remdups_mset `# xs) +
     Const y * poly_of_vars (remdups_mset ys))
     \<in> More_Modules.ideal polynomial_bool\<close> for y ys
     by (metis add_diff_add diff ideal.scale_right_diff_distrib ideal.span_add ideal.span_scale)
   show ?case
     using add
     apply (cases x)
     subgoal for ys y
       using ideal_mult_right_in2[OF diff, of \<open>poly_of_vars ys\<close> ys]
       by (auto simp: remove_powers_def right_diff_distrib
         ideal.span_diff ideal.span_add field_simps)
     done
 qed
 
 lemma add_poly_p_polynomial_of_mset:
   \<open>add_poly_p (p, q, r) (p', q', r') \<Longrightarrow>
     polynomial_of_mset r + (polynomial_of_mset p + polynomial_of_mset q) =
     polynomial_of_mset r' + (polynomial_of_mset p' + polynomial_of_mset q')\<close>
   apply (induction rule: add_poly_p_induct)
   subgoal
     by auto
   subgoal
     by auto
   subgoal
     by (auto simp: algebra_simps Const_add)
   subgoal
     by (auto simp: algebra_simps Const_add)
   subgoal
     by (auto simp: algebra_simps Const_add)
   done
 
 lemma rtranclp_add_poly_p_polynomial_of_mset:
   \<open>add_poly_p\<^sup>*\<^sup>* (p, q, r) (p', q', r') \<Longrightarrow>
     polynomial_of_mset r + (polynomial_of_mset p + polynomial_of_mset q) =
     polynomial_of_mset r' + (polynomial_of_mset p' + polynomial_of_mset q')\<close>
   by (induction rule: rtranclp_induct[of add_poly_p \<open>(_, _, _)\<close> \<open>(_, _, _)\<close>, split_format(complete), of for r])
     (auto dest: add_poly_p_polynomial_of_mset)
 
 
 lemma rtranclp_add_poly_p_polynomial_of_mset_full:
   \<open>add_poly_p\<^sup>*\<^sup>* (p, q, {#}) ({#}, {#}, r') \<Longrightarrow>
     polynomial_of_mset r' = (polynomial_of_mset p + polynomial_of_mset q)\<close>
   by (drule rtranclp_add_poly_p_polynomial_of_mset)
     (auto simp: ac_simps add_eq_0_iff)
 
 lemma poly_of_vars_remdups_mset:
   \<open>poly_of_vars (remdups_mset (xs)) - (poly_of_vars xs)
     \<in> More_Modules.ideal polynomial_bool\<close>
   apply (induction xs)
   subgoal by (auto simp: ideal.span_zero)
   subgoal for x xs
     apply (cases \<open>x \<in># xs\<close>)
      apply (metis (no_types, lifting) X2_X_polynomial_bool_mult_in diff_add_cancel diff_diff_eq2
         ideal.span_diff insert_DiffM poly_of_vars_simps(1) remdups_mset_singleton_sum)
     by (metis (no_types, lifting) ideal.span_scale poly_of_vars_simps(1) remdups_mset_singleton_sum
         right_diff_distrib)
   done
 
 lemma polynomial_of_mset_mult_map:
   \<open>polynomial_of_mset
      {#case x of (ys, n) \<Rightarrow> (remdups_mset (ys + xs), n * m). x \<in># q#} -
     Const m * (poly_of_vars xs * polynomial_of_mset q)
     \<in> More_Modules.ideal polynomial_bool\<close>
   (is \<open>?P q \<in> _\<close>)
 proof (induction q)
   case empty
   then show ?case by (auto simp: algebra_simps ideal.span_zero)
 next
   case (add x q)
   then have uP:  \<open>-?P q \<in> More_Modules.ideal polynomial_bool\<close>
     using ideal.span_neg by blast
   have \<open> Const b * (Const m * poly_of_vars (remdups_mset (a + xs))) -
            Const b * (Const m * (poly_of_vars a * poly_of_vars xs))
            \<in> More_Modules.ideal polynomial_bool\<close> for a b
     by (auto simp: Const_mult simp flip: right_diff_distrib' poly_of_vars_simps
         intro!: ideal.span_scale poly_of_vars_remdups_mset)
   then show ?case
     apply (subst ideal.span_add_eq2[symmetric, OF uP])
     apply (cases x)
     apply (auto simp: field_simps Const_mult  simp flip:
         intro!: ideal.span_scale poly_of_vars_remdups_mset)
     done
 qed
 
 lemma mult_poly_p_mult_ideal:
   \<open>mult_poly_p q (p, r) (p', r') \<Longrightarrow>
      (polynomial_of_mset p' * polynomial_of_mset q + polynomial_of_mset r') - (polynomial_of_mset p * polynomial_of_mset q + polynomial_of_mset r)
        \<in> ideal polynomial_bool\<close>
 proof (induction rule: mult_poly_p_induct)
   case (mult_step xs n p r)
   show ?case
     by (auto simp: algebra_simps polynomial_of_mset_mult_map)
 qed
 
 lemma rtranclp_mult_poly_p_mult_ideal:
   \<open>(mult_poly_p q)\<^sup>*\<^sup>* (p, r) (p', r') \<Longrightarrow>
      (polynomial_of_mset p' * polynomial_of_mset q + polynomial_of_mset r') - (polynomial_of_mset p * polynomial_of_mset q + polynomial_of_mset r)
        \<in> ideal polynomial_bool\<close>
   apply (induction p' r' rule: rtranclp_induct[of \<open>mult_poly_p q\<close> \<open>(p, r)\<close> \<open>(p', q')\<close> for p' q', split_format(complete)])
   subgoal
     by (auto simp: ideal.span_zero)
   subgoal for a b aa ba
     apply (drule mult_poly_p_mult_ideal)
     apply (drule ideal.span_add)
     apply assumption
     by (auto simp: group_add_class.diff_add_eq_diff_diff_swap
         add.inverse_distrib_swap ac_simps add_diff_eq
       simp flip:  diff_add_eq_diff_diff_swap)
   done
 
 lemma rtranclp_mult_poly_p_mult_ideal_final:
   \<open>(mult_poly_p q)\<^sup>*\<^sup>* (p, {#}) ({#}, r) \<Longrightarrow>
     (polynomial_of_mset r) - (polynomial_of_mset p * polynomial_of_mset q)
        \<in> ideal polynomial_bool\<close>
   by (drule rtranclp_mult_poly_p_mult_ideal) auto
 
 lemma normalize_poly_p_poly_of_mset:
   \<open>normalize_poly_p p q \<Longrightarrow> polynomial_of_mset p = polynomial_of_mset q\<close>
   apply (induction rule: normalize_poly_p.induct)
   apply (auto simp: Const_add algebra_simps)
   done
 
 
 lemma rtranclp_normalize_poly_p_poly_of_mset:
   \<open>normalize_poly_p\<^sup>*\<^sup>* p q \<Longrightarrow> polynomial_of_mset p = polynomial_of_mset q\<close>
   by (induction rule: rtranclp_induct)
     (auto simp: normalize_poly_p_poly_of_mset)
 
 end
 
 
 text \<open>It would be nice to have the property in the other direction too, but this requires a deep
 dive into the definitions of polynomials.\<close>
 locale poly_embed_bij = poly_embed +
   fixes V N
   assumes \<phi>_bij: \<open>bij_betw \<phi> V N\<close>
 begin
 
 definition \<phi>' :: \<open>nat \<Rightarrow> string\<close> where
   \<open>\<phi>' = the_inv_into V \<phi>\<close>
 
 lemma \<phi>'_\<phi>[simp]:
   \<open>x \<in> V \<Longrightarrow> \<phi>' (\<phi> x) = x\<close>
   using \<phi>_bij unfolding \<phi>'_def
   by (meson bij_betw_imp_inj_on the_inv_into_f_f)
 
 lemma \<phi>_\<phi>'[simp]:
   \<open>x \<in> N \<Longrightarrow> \<phi> (\<phi>' x) = x\<close>
   using \<phi>_bij unfolding \<phi>'_def
   by (meson f_the_inv_into_f_bij_betw)
 
 end
 
 end
 
diff --git a/thys/PAC_Checker/WB_Sort.thy b/thys/PAC_Checker/WB_Sort.thy
--- a/thys/PAC_Checker/WB_Sort.thy
+++ b/thys/PAC_Checker/WB_Sort.thy
@@ -1,1688 +1,1688 @@
 (*
   File:         WB_Sort.thy
   Author:       Mathias Fleury, Daniela Kaufmann, JKU
   Author:       Maximilian Wuttke, Saarland University
   Maintainer:   Mathias Fleury, JKU
 
 Correctness proof contributed by Maximilian Wuttke *)
 theory WB_Sort
   imports Refine_Imperative_HOL.IICF "HOL-Library.Rewrite" Duplicate_Free_Multiset
 begin
 
 text \<open>This a complete copy-paste of the IsaFoL version because sharing is too hard.\<close>
 
 
 text \<open>Every element between \<^term>\<open>lo\<close> and \<^term>\<open>hi\<close> can be chosen as pivot element.\<close>
 definition choose_pivot :: \<open>('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat nres\<close> where
   \<open>choose_pivot _ _ _ lo hi = SPEC(\<lambda>k. k \<ge> lo \<and> k \<le> hi)\<close>
 
 text \<open>The element at index \<open>p\<close> partitions the subarray \<open>lo..hi\<close>. This means that every element \<close>
 definition isPartition_wrt :: \<open>('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'b list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool\<close> where
   \<open>isPartition_wrt R xs lo hi p \<equiv> (\<forall> i. i \<ge> lo \<and> i < p \<longrightarrow> R (xs!i) (xs!p)) \<and> (\<forall> j. j > p \<and> j \<le> hi \<longrightarrow> R (xs!p) (xs!j))\<close>
 
 lemma isPartition_wrtI:
   \<open>(\<And> i. \<lbrakk>i \<ge> lo; i < p\<rbrakk> \<Longrightarrow> R (xs!i) (xs!p)) \<Longrightarrow> (\<And> j. \<lbrakk>j > p; j \<le> hi\<rbrakk> \<Longrightarrow> R (xs!p) (xs!j)) \<Longrightarrow> isPartition_wrt R xs lo hi p\<close>
   by (simp add: isPartition_wrt_def)
 
 definition isPartition :: \<open>'a :: order list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool\<close> where
   \<open>isPartition xs lo hi p \<equiv> isPartition_wrt (\<le>) xs lo hi p\<close>
 
 abbreviation isPartition_map :: \<open>('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool\<close> where
   \<open>isPartition_map R h xs i j k \<equiv> isPartition_wrt (\<lambda>a b. R (h a) (h b)) xs i j k\<close>
 
 lemma isPartition_map_def':
   \<open>lo \<le> p \<Longrightarrow> p \<le> hi \<Longrightarrow> hi < length xs \<Longrightarrow> isPartition_map R h xs lo hi p = isPartition_wrt R (map h xs) lo hi p\<close>
   by (auto simp add: isPartition_wrt_def conjI)
 
 
 text \<open>Example: 6 is the pivot element (with index 4); \<^term>\<open>7\<close> is equal to the \<^term>\<open>length xs - 1\<close>.\<close>
 lemma \<open>isPartition [0,5,3,4,6,9,8,10::nat] 0 7 4\<close>
   by (auto simp add: isPartition_def isPartition_wrt_def nth_Cons')
 
 
 
 definition sublist :: \<open>'a list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a list\<close> where
 \<open>sublist xs i j \<equiv> take (Suc j - i) (drop i xs)\<close>
 
 (*take from HashMap *)
 lemma take_Suc0:
   "l\<noteq>[] \<Longrightarrow> take (Suc 0) l = [l!0]"
   "0 < length l \<Longrightarrow> take (Suc 0) l = [l!0]"
   "Suc n \<le> length l \<Longrightarrow> take (Suc 0) l = [l!0]"
   by (cases l, auto)+
 
 lemma sublist_single: \<open>i < length xs \<Longrightarrow> sublist xs i i = [xs!i]\<close>
   by (cases xs) (auto simp add: sublist_def take_Suc0)
 
 lemma insert_eq: \<open>insert a b = b \<union> {a}\<close>
   by auto
 
 lemma sublist_nth: \<open>\<lbrakk>lo \<le> hi; hi < length xs; k+lo \<le> hi\<rbrakk> \<Longrightarrow> (sublist xs lo hi)!k = xs!(lo+k)\<close>
   by (simp add: sublist_def)
 
 lemma sublist_length: \<open>\<lbrakk>i \<le> j; j < length xs\<rbrakk> \<Longrightarrow> length (sublist xs i j) = 1 + j - i\<close>
   by (simp add: sublist_def)
 
 lemma sublist_not_empty: \<open>\<lbrakk>i \<le> j; j < length xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> sublist xs i j \<noteq> []\<close>
   apply simp
   apply (rewrite List.length_greater_0_conv[symmetric])
   apply (rewrite sublist_length)
   by auto
 
 
 
 lemma sublist_app: \<open>\<lbrakk>i1 \<le> i2; i2 \<le> i3\<rbrakk> \<Longrightarrow> sublist xs i1 i2 @ sublist xs (Suc i2) i3 = sublist xs i1 i3\<close>
   unfolding sublist_def
   by (smt Suc_eq_plus1_left Suc_le_mono append.assoc le_SucI le_add_diff_inverse le_trans same_append_eq take_add)
 
 definition sorted_sublist_wrt :: \<open>('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'b list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool\<close> where
   \<open>sorted_sublist_wrt R xs lo hi = sorted_wrt R (sublist xs lo hi)\<close>
 
 definition sorted_sublist :: \<open>'a :: linorder list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool\<close> where
   \<open>sorted_sublist xs lo hi = sorted_sublist_wrt (\<le>) xs lo hi\<close>
 
 abbreviation sorted_sublist_map :: \<open>('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool\<close> where
   \<open>sorted_sublist_map R h xs lo hi \<equiv> sorted_sublist_wrt (\<lambda>a b. R (h a) (h b)) xs lo hi\<close>
 
 lemma sorted_sublist_map_def':
   \<open>lo < length xs \<Longrightarrow> sorted_sublist_map R h xs lo hi \<equiv> sorted_sublist_wrt R (map h xs) lo hi\<close>
   apply (simp add: sorted_sublist_wrt_def)
   by (simp add: drop_map sorted_wrt_map sublist_def take_map)
 
 lemma sorted_sublist_wrt_refl: \<open>i < length xs \<Longrightarrow> sorted_sublist_wrt R xs i i\<close>
   by (auto simp add: sorted_sublist_wrt_def sublist_single)
 
 lemma sorted_sublist_refl: \<open>i < length xs \<Longrightarrow> sorted_sublist xs i i\<close>
   by (auto simp add: sorted_sublist_def sorted_sublist_wrt_refl)
 
 lemma sublist_map: \<open>sublist (map f xs) i j = map f (sublist xs i j)\<close>
   apply (auto simp add: sublist_def)
   by (simp add: drop_map take_map)
 
 
 lemma take_set: \<open>j \<le> length xs \<Longrightarrow> x \<in> set (take j xs) \<equiv> (\<exists> k. k < j \<and> xs!k = x)\<close>
   apply (induction xs)
    apply simp
   by (meson in_set_conv_iff less_le_trans)
 
 lemma drop_set: \<open>j \<le> length xs \<Longrightarrow> x \<in> set (drop j xs) \<equiv> (\<exists>k. j\<le>k\<and>k<length xs \<and> xs!k=x)\<close>
   by (smt Misc.in_set_drop_conv_nth) (* lemma found by sledgehammer *)
 
 lemma sublist_el: \<open>i \<le> j \<Longrightarrow> j < length xs \<Longrightarrow> x \<in> set (sublist xs i j) \<equiv> (\<exists> k. k < Suc j-i \<and> xs!(i+k)=x)\<close>
   by (auto simp add: take_set sublist_def)
 
 lemma sublist_el': \<open>i \<le> j \<Longrightarrow> j < length xs \<Longrightarrow> x \<in> set (sublist xs i j) \<equiv> (\<exists> k. i\<le>k\<and>k\<le>j \<and> xs!k=x)\<close>
   apply (subst sublist_el, assumption, assumption)
   by (smt Groups.add_ac(2) le_add1 le_add_diff_inverse less_Suc_eq less_diff_conv nat_less_le order_refl)
 
 
 lemma sublist_lt: \<open>hi < lo \<Longrightarrow> sublist xs lo hi = []\<close>
   by (auto simp add: sublist_def)
 
 lemma nat_le_eq_or_lt: \<open>(a :: nat) \<le> b = (a = b \<or> a < b)\<close>
   by linarith
 
 
 lemma sorted_sublist_wrt_le: \<open>hi \<le> lo \<Longrightarrow> hi < length xs \<Longrightarrow> sorted_sublist_wrt R xs lo hi\<close>
   apply (auto simp add: nat_le_eq_or_lt)
   unfolding sorted_sublist_wrt_def
   subgoal apply (rewrite sublist_single) by auto
   subgoal by (auto simp add: sublist_lt)
   done
 
 text \<open>Elements in a sorted sublists are actually sorted\<close>
 lemma sorted_sublist_wrt_nth_le:
   assumes \<open>sorted_sublist_wrt R xs lo hi\<close> and \<open>lo \<le> hi\<close> and \<open>hi < length xs\<close> and
     \<open>lo \<le> i\<close> and \<open>i < j\<close> and \<open>j \<le> hi\<close>
   shows \<open>R (xs!i) (xs!j)\<close>
 proof -
   have A: \<open>lo < length xs\<close> using assms(2) assms(3) by linarith
   obtain i' where I: \<open>i = lo + i'\<close> using assms(4) le_Suc_ex by auto
   obtain j' where J: \<open>j = lo + j'\<close> by (meson assms(4) assms(5) dual_order.trans le_iff_add less_imp_le_nat)
   show ?thesis
     using assms(1) apply (simp add: sorted_sublist_wrt_def I J)
     apply (rewrite sublist_nth[symmetric, where k=i', where lo=lo, where hi=hi])
     using assms apply auto subgoal using I by linarith
     apply (rewrite sublist_nth[symmetric, where k=j', where lo=lo, where hi=hi])
     using assms apply auto subgoal using J by linarith
     apply (rule sorted_wrt_nth_less)
     apply auto
     subgoal using I J nat_add_left_cancel_less by blast
     subgoal apply (simp add: sublist_length) using J by linarith
     done
 qed
 
 text \<open>We can make the assumption \<^term>\<open>i < j\<close> weaker if we have a reflexivie relation.\<close>
 lemma sorted_sublist_wrt_nth_le':
   assumes ref: \<open>\<And> x. R x x\<close>
     and \<open>sorted_sublist_wrt R xs lo hi\<close> and \<open>lo \<le> hi\<close> and \<open>hi < length xs\<close>
     and \<open>lo \<le> i\<close> and \<open>i \<le> j\<close> and \<open>j \<le> hi\<close>
   shows \<open>R (xs!i) (xs!j)\<close>
 proof -
   have \<open>i < j \<or> i = j\<close> using \<open>i \<le> j\<close> by linarith
   then consider (a) \<open>i < j\<close> |
                 (b) \<open>i = j\<close> by blast
   then show ?thesis
   proof cases
     case a
     then show ?thesis
       using assms(2-5,7) sorted_sublist_wrt_nth_le by blast
   next
     case b
     then show ?thesis
       by (simp add: ref)
   qed
 qed
 
 
 
 (*
 lemma sorted_sublist_map_nth_le:
   assumes \<open>sorted_sublist_map R h xs lo hi\<close> and \<open>lo \<le> hi\<close> and \<open>hi < length xs\<close> and
     \<open>lo \<le> i\<close> and \<open>i < j\<close> and \<open>j \<le> hi\<close>
   shows \<open>R (h (xs!i)) (h (xs!j))\<close>
 proof -
   show ?thesis
     using assms by (rule sorted_sublist_wrt_nth_le)
 qed
 *)
 
 
 
 lemma sorted_sublist_le: \<open>hi \<le> lo \<Longrightarrow> hi < length xs \<Longrightarrow> sorted_sublist xs lo hi\<close>
   by (auto simp add: sorted_sublist_def sorted_sublist_wrt_le)
 
 lemma sorted_sublist_map_le: \<open>hi \<le> lo \<Longrightarrow> hi < length xs \<Longrightarrow> sorted_sublist_map R h xs lo hi\<close>
   by (auto simp add: sorted_sublist_wrt_le)
 
 lemma sublist_cons: \<open>lo < hi \<Longrightarrow> hi < length xs \<Longrightarrow> sublist xs lo hi = xs!lo # sublist xs (Suc lo) hi\<close>
   by (metis Cons_eq_appendI append_self_conv2 less_imp_le_nat less_or_eq_imp_le less_trans
       sublist_app sublist_single)
 
 lemma sorted_sublist_wrt_cons':
   \<open>sorted_sublist_wrt R xs (lo+1) hi \<Longrightarrow> lo \<le> hi \<Longrightarrow> hi < length xs \<Longrightarrow> (\<forall>j. lo<j\<and>j\<le>hi \<longrightarrow> R (xs!lo) (xs!j)) \<Longrightarrow> sorted_sublist_wrt R xs lo hi\<close>
   apply (auto simp add: nat_le_eq_or_lt sorted_sublist_wrt_def)
   apply (auto 5 4 simp add: sublist_cons sublist_el less_diff_conv add.commute[of _ lo]
       dest: Suc_lessI sublist_single)
   done
 
 lemma sorted_sublist_wrt_cons:
   assumes trans: \<open>(\<And> x y z. \<lbrakk>R x y; R y z\<rbrakk> \<Longrightarrow> R x z)\<close> and
     \<open>sorted_sublist_wrt R xs (lo+1) hi\<close> and
     \<open>lo \<le> hi\<close> and \<open>hi < length xs \<close> and \<open>R (xs!lo) (xs!(lo+1))\<close>
   shows \<open>sorted_sublist_wrt R xs lo hi\<close>
 proof -
   show ?thesis
     apply (rule sorted_sublist_wrt_cons') using assms apply auto
     subgoal premises assms' for j
     proof -
       have A: \<open>j=lo+1 \<or> j>lo+1\<close> using assms'(5) by linarith
       show ?thesis
         using A proof
         assume A: \<open>j=lo+1\<close> show ?thesis
           by (simp add: A assms')
       next
         assume A: \<open>j>lo+1\<close> show ?thesis
           apply (rule trans)
           apply (rule assms(5))
           apply (rule sorted_sublist_wrt_nth_le[OF assms(2), where i=\<open>lo+1\<close>, where j=j])
           subgoal using A assms'(6) by linarith
           subgoal using assms'(3) less_imp_diff_less by blast
           subgoal using assms'(5) by auto
           subgoal using A by linarith
           subgoal by (simp add: assms'(6))
           done
       qed
     qed
     done
 qed
 
 lemma sorted_sublist_map_cons:
   \<open>(\<And> x y z. \<lbrakk>R (h x) (h y); R (h y) (h z)\<rbrakk> \<Longrightarrow> R (h x) (h z)) \<Longrightarrow>
     sorted_sublist_map R h xs (lo+1) hi \<Longrightarrow> lo \<le> hi \<Longrightarrow> hi < length xs \<Longrightarrow> R (h (xs!lo)) (h (xs!(lo+1))) \<Longrightarrow> sorted_sublist_map R h xs lo hi\<close>
   by (blast intro: sorted_sublist_wrt_cons)
 
 
 lemma sublist_snoc: \<open>lo < hi \<Longrightarrow> hi < length xs \<Longrightarrow> sublist xs lo hi = sublist xs lo (hi-1) @ [xs!hi]\<close>
   apply (simp add: sublist_def)
 proof -
   assume a1: "lo < hi"
   assume "hi < length xs"
   then have "take lo xs @ take (Suc hi - lo) (drop lo xs) = (take lo xs @ take (hi - lo) (drop lo xs)) @ [xs ! hi]"
     using a1 by (metis (no_types) Suc_diff_le add_Suc_right hd_drop_conv_nth le_add_diff_inverse less_imp_le_nat take_add take_hd_drop)
   then show "take (Suc hi - lo) (drop lo xs) = take (hi - lo) (drop lo xs) @ [xs ! hi]"
     by simp
 qed
 
 lemma sorted_sublist_wrt_snoc':
   \<open>sorted_sublist_wrt R xs lo (hi-1) \<Longrightarrow> lo \<le> hi \<Longrightarrow> hi < length xs \<Longrightarrow> (\<forall>j. lo\<le>j\<and>j<hi \<longrightarrow> R (xs!j) (xs!hi)) \<Longrightarrow> sorted_sublist_wrt R xs lo hi\<close>
   apply (simp add: sorted_sublist_wrt_def)
   apply (auto simp add: nat_le_eq_or_lt)
   subgoal by (simp add: sublist_single)
   by (auto simp add: sublist_snoc sublist_el sorted_wrt_append add.commute[of lo] less_diff_conv
       simp: leI simp flip:nat_le_eq_or_lt)
 
 
 lemma sorted_sublist_wrt_snoc:
   assumes trans: \<open>(\<And> x y z. \<lbrakk>R x y; R y z\<rbrakk> \<Longrightarrow> R x z)\<close> and
     \<open>sorted_sublist_wrt R xs lo (hi-1)\<close> and
     \<open>lo \<le> hi\<close> and \<open>hi < length xs\<close> and \<open>(R (xs!(hi-1)) (xs!hi))\<close>
   shows \<open>sorted_sublist_wrt R xs lo hi\<close>
 proof -
   show ?thesis
     apply (rule sorted_sublist_wrt_snoc') using assms apply auto
     subgoal premises assms' for j
     proof -
       have A: \<open>j=hi-1 \<or> j<hi-1\<close> using assms'(6) by linarith
       show ?thesis
         using A proof
         assume A: \<open>j=hi-1\<close> show ?thesis
           by (simp add: A assms')
       next
         assume A: \<open>j<hi-1\<close> show ?thesis
           apply (rule trans)
            apply (rule sorted_sublist_wrt_nth_le[OF assms(2), where i=j, where j=\<open>hi-1\<close>])
                prefer 6
                apply (rule assms(5))
               apply auto
           subgoal using A assms'(5) by linarith
           subgoal using assms'(3) less_imp_diff_less by blast
           subgoal using assms'(5) by auto
           subgoal using A by linarith
           done
       qed
     qed
     done
 qed
 
 lemma sublist_split: \<open>lo \<le> hi \<Longrightarrow> lo < p \<Longrightarrow> p < hi \<Longrightarrow> hi < length xs \<Longrightarrow> sublist xs lo p @ sublist xs (p+1) hi = sublist xs lo hi\<close>
   by (simp add: sublist_app)
 
 lemma sublist_split_part: \<open>lo \<le> hi \<Longrightarrow> lo < p \<Longrightarrow> p < hi \<Longrightarrow> hi < length xs \<Longrightarrow> sublist xs lo (p-1) @ xs!p # sublist xs (p+1) hi = sublist xs lo hi\<close>
   by (auto simp add: sublist_split[symmetric] sublist_snoc[where xs=xs,where lo=lo,where hi=p])
 
 
 text \<open>A property for partitions (we always assume that \<^term>\<open>R\<close> is transitive.\<close>
 lemma isPartition_wrt_trans:
 \<open>(\<And> x y z. \<lbrakk>R x y; R y z\<rbrakk> \<Longrightarrow> R x z) \<Longrightarrow>
   isPartition_wrt R xs lo hi p \<Longrightarrow>
   (\<forall>i j. lo \<le> i \<and> i < p \<and> p < j \<and> j \<le> hi \<longrightarrow> R (xs!i) (xs!j))\<close>
   by (auto simp add: isPartition_wrt_def)
 
 lemma isPartition_map_trans:
 \<open>(\<And> x y z. \<lbrakk>R (h x) (h y); R (h y) (h z)\<rbrakk> \<Longrightarrow> R (h x) (h z)) \<Longrightarrow>
   hi < length xs \<Longrightarrow>
   isPartition_map R h xs lo hi p \<Longrightarrow>
   (\<forall>i j. lo \<le> i \<and> i < p \<and> p < j \<and> j \<le> hi \<longrightarrow> R (h (xs!i)) (h (xs!j)))\<close>
   by (auto simp add: isPartition_wrt_def)
 
 
 lemma merge_sorted_wrt_partitions_between':
   \<open>lo \<le> hi \<Longrightarrow> lo < p \<Longrightarrow> p < hi \<Longrightarrow> hi < length xs \<Longrightarrow>
     isPartition_wrt R xs lo hi p \<Longrightarrow>
     sorted_sublist_wrt R xs lo (p-1) \<Longrightarrow> sorted_sublist_wrt R xs (p+1) hi \<Longrightarrow>
     (\<forall>i j. lo \<le> i \<and> i < p \<and> p < j \<and> j \<le> hi \<longrightarrow> R (xs!i) (xs!j)) \<Longrightarrow>
     sorted_sublist_wrt R xs lo hi\<close>
   apply (auto simp add: isPartition_def isPartition_wrt_def sorted_sublist_def sorted_sublist_wrt_def sublist_map)
   apply (simp add: sublist_split_part[symmetric])
   apply (auto simp add: List.sorted_wrt_append)
   subgoal by (auto simp add: sublist_el)
   subgoal by (auto simp add: sublist_el)
   subgoal by (auto simp add: sublist_el')
   done
 
 lemma merge_sorted_wrt_partitions_between:
   \<open>(\<And> x y z. \<lbrakk>R x y; R y z\<rbrakk> \<Longrightarrow> R x z) \<Longrightarrow>
     isPartition_wrt R xs lo hi p \<Longrightarrow>
     sorted_sublist_wrt R xs lo (p-1) \<Longrightarrow> sorted_sublist_wrt R xs (p+1) hi \<Longrightarrow>
     lo \<le> hi \<Longrightarrow> hi < length xs \<Longrightarrow> lo < p \<Longrightarrow> p < hi \<Longrightarrow> hi < length xs \<Longrightarrow>
     sorted_sublist_wrt R xs lo hi\<close>
   by (simp add: merge_sorted_wrt_partitions_between' isPartition_wrt_trans)
 
 
 (*
 lemma merge_sorted_map_partitions_between:
   \<open>(\<And> x y z. \<lbrakk>R (h x) (h y); R (h y) (h z)\<rbrakk> \<Longrightarrow> R (h x) (h z)) \<Longrightarrow>
     isPartition_map R h xs lo hi p \<Longrightarrow>
     sorted_sublist_map R h xs lo (p-1) \<Longrightarrow> sorted_sublist_map R h xs (p+1) hi \<Longrightarrow>
     lo \<le> hi \<Longrightarrow> hi < length xs \<Longrightarrow> lo < p \<Longrightarrow> p < hi \<Longrightarrow> hi < length xs \<Longrightarrow>
     sorted_sublist_map R h xs lo hi\<close>
   by (simp add: merge_sorted_wrt_partitions_between' isPartition_map_trans)
 *)
 
 
 
 
 text \<open>The main theorem to merge sorted lists\<close>
 lemma merge_sorted_wrt_partitions:
   \<open>isPartition_wrt R xs lo hi p \<Longrightarrow>
     sorted_sublist_wrt R xs lo (p - Suc 0) \<Longrightarrow> sorted_sublist_wrt R xs (Suc p) hi \<Longrightarrow>
     lo \<le> hi \<Longrightarrow> lo \<le> p \<Longrightarrow> p \<le> hi \<Longrightarrow> hi < length xs \<Longrightarrow>
     (\<forall>i j. lo \<le> i \<and> i < p \<and> p < j \<and> j \<le> hi \<longrightarrow> R (xs!i) (xs!j)) \<Longrightarrow>
     sorted_sublist_wrt R xs lo hi\<close>
   subgoal premises assms
   proof -
     have C: \<open>lo=p\<and>p=hi \<or> lo=p\<and>p<hi \<or> lo<p\<and>p=hi \<or> lo<p\<and>p<hi\<close>
       using assms by linarith
     show ?thesis
       using C apply auto
       subgoal \<comment> \<open>lo=p=hi\<close>
         apply (rule sorted_sublist_wrt_refl)
         using assms by auto
       subgoal \<comment> \<open>lo=p<hi\<close>
         using assms by (simp add: isPartition_def isPartition_wrt_def sorted_sublist_wrt_cons')
       subgoal \<comment> \<open>lo<p=hi\<close>
         using assms by (simp add: isPartition_def isPartition_wrt_def sorted_sublist_wrt_snoc')
       subgoal \<comment> \<open>lo<p<hi\<close>
         using assms
         apply (rewrite merge_sorted_wrt_partitions_between'[where p=p])
         by auto
       done
   qed
   done
 
 theorem merge_sorted_map_partitions:
   \<open>(\<And> x y z. \<lbrakk>R (h x) (h y); R (h y) (h z)\<rbrakk> \<Longrightarrow> R (h x) (h z)) \<Longrightarrow>
     isPartition_map R h xs lo hi p \<Longrightarrow>
     sorted_sublist_map R h xs lo (p - Suc 0) \<Longrightarrow> sorted_sublist_map R h xs (Suc p) hi \<Longrightarrow>
     lo \<le> hi \<Longrightarrow> lo \<le> p \<Longrightarrow> p \<le> hi \<Longrightarrow> hi < length xs \<Longrightarrow>
     sorted_sublist_map R h xs lo hi\<close>
   apply (rule merge_sorted_wrt_partitions) apply auto
   by (simp add: merge_sorted_wrt_partitions isPartition_map_trans)
 
 
 lemma partition_wrt_extend:
   \<open>isPartition_wrt R xs lo' hi' p \<Longrightarrow>
   hi < length xs \<Longrightarrow>
   lo \<le> lo' \<Longrightarrow> lo' \<le> hi \<Longrightarrow> hi' \<le> hi \<Longrightarrow>
   lo' \<le> p \<Longrightarrow> p \<le> hi' \<Longrightarrow>
   (\<And> i. lo\<le>i \<Longrightarrow> i <lo' \<Longrightarrow> R (xs!i) (xs!p)) \<Longrightarrow>
   (\<And> j. hi'<j \<Longrightarrow> j\<le>hi \<Longrightarrow> R (xs!p) (xs!j)) \<Longrightarrow>
   isPartition_wrt R xs lo hi p\<close>
   unfolding isPartition_wrt_def
   apply (intro conjI)
   subgoal
     by (force simp: not_le)
   subgoal
     using leI by blast
   done
 
 lemma partition_map_extend:
   \<open>isPartition_map R h xs lo' hi' p \<Longrightarrow>
   hi < length xs \<Longrightarrow>
   lo \<le> lo' \<Longrightarrow> lo' \<le> hi \<Longrightarrow> hi' \<le> hi \<Longrightarrow>
   lo' \<le> p \<Longrightarrow> p \<le> hi' \<Longrightarrow>
   (\<And> i. lo\<le>i \<Longrightarrow> i <lo' \<Longrightarrow> R (h (xs!i)) (h (xs!p))) \<Longrightarrow>
   (\<And> j. hi'<j \<Longrightarrow> j\<le>hi \<Longrightarrow> R (h (xs!p)) (h (xs!j))) \<Longrightarrow>
   isPartition_map R h xs lo hi p\<close>
   by (auto simp add: partition_wrt_extend)
 
 
 lemma isPartition_empty:
   \<open>(\<And> j. \<lbrakk>lo < j; j \<le> hi\<rbrakk> \<Longrightarrow> R (xs ! lo) (xs ! j)) \<Longrightarrow>
   isPartition_wrt R xs lo hi lo\<close>
   by (auto simp add: isPartition_wrt_def)
 
 
 
 lemma take_ext:
   \<open>(\<forall>i<k. xs'!i=xs!i) \<Longrightarrow>
   k < length xs \<Longrightarrow> k < length xs' \<Longrightarrow>
   take k xs' = take k xs\<close>
   by (simp add: nth_take_lemma)
 
 lemma drop_ext':
   \<open>(\<forall>i. i\<ge>k \<and> i<length xs \<longrightarrow> xs'!i=xs!i) \<Longrightarrow>
    0<k \<Longrightarrow> xs\<noteq>[] \<Longrightarrow> \<comment> \<open>These corner cases will be dealt with in the next lemma\<close>
    length xs'=length xs \<Longrightarrow>
    drop k xs' = drop k xs\<close>
   apply (rewrite in \<open>drop _ \<hole> = _\<close> List.rev_rev_ident[symmetric])
   apply (rewrite in \<open>_ = drop _ \<hole>\<close> List.rev_rev_ident[symmetric])
   apply (rewrite in \<open>\<hole> = _\<close> List.drop_rev)
   apply (rewrite in \<open>_ = \<hole>\<close> List.drop_rev)
   apply simp
   apply (rule take_ext)
-  by (auto simp add: nth_rev)
+  by (auto simp add: rev_nth)
 
 lemma drop_ext:
 \<open>(\<forall>i. i\<ge>k \<and> i<length xs \<longrightarrow> xs'!i=xs!i) \<Longrightarrow>
    length xs'=length xs \<Longrightarrow>
    drop k xs' = drop k xs\<close>
   apply (cases xs)
    apply auto
   apply (cases k)
   subgoal  by (simp add: nth_equalityI)
   subgoal apply (rule drop_ext') by auto
   done
 
 
 lemma sublist_ext':
   \<open>(\<forall>i. lo\<le>i\<and>i\<le>hi \<longrightarrow> xs'!i=xs!i) \<Longrightarrow>
    length xs' = length xs \<Longrightarrow>
    lo \<le> hi \<Longrightarrow> Suc hi < length xs \<Longrightarrow>
    sublist xs' lo hi = sublist xs lo hi\<close>
   apply (simp add: sublist_def)
   apply (rule take_ext)
   by auto
 
 
 lemma lt_Suc: \<open>(a < b) = (Suc a = b \<or> Suc a < b)\<close>
   by auto
 
 lemma sublist_until_end_eq_drop: \<open>Suc hi = length xs \<Longrightarrow> sublist xs lo hi = drop lo xs\<close>
   by (simp add: sublist_def)
 
 lemma sublist_ext:
   \<open>(\<forall>i. lo\<le>i\<and>i\<le>hi \<longrightarrow> xs'!i=xs!i) \<Longrightarrow>
    length xs' = length xs \<Longrightarrow>
    lo \<le> hi \<Longrightarrow> hi < length xs \<Longrightarrow>
    sublist xs' lo hi = sublist xs lo hi\<close>
   apply (auto simp add: lt_Suc[where a=hi])
   subgoal by (auto simp add: sublist_until_end_eq_drop drop_ext)
   subgoal by (auto simp add: sublist_ext')
   done
 
 lemma sorted_wrt_lower_sublist_still_sorted:
   assumes \<open>sorted_sublist_wrt R xs lo (lo' - Suc 0)\<close> and
     \<open>lo \<le> lo'\<close> and \<open>lo' < length xs\<close> and
     \<open>(\<forall> i. lo\<le>i\<and>i<lo' \<longrightarrow> xs'!i=xs!i)\<close> and \<open>length xs' = length xs\<close>
   shows \<open>sorted_sublist_wrt R xs' lo (lo' - Suc 0)\<close>
 proof -
   have l: \<open>lo < lo' - 1 \<or> lo \<ge> lo'-1\<close>
     by linarith
   show ?thesis
     using l apply auto
     subgoal \<comment> \<open>lo < lo' - 1\<close>
       apply (auto simp add: sorted_sublist_wrt_def)
       apply (rewrite sublist_ext[where xs=xs])
       using assms by (auto simp add: sorted_sublist_wrt_def)
     subgoal \<comment> \<open>lo >= lo' - 1\<close>
       using assms by (auto simp add: sorted_sublist_wrt_le)
     done
 qed
 
 lemma sorted_map_lower_sublist_still_sorted:
   assumes \<open>sorted_sublist_map R h xs lo (lo' - Suc 0)\<close> and
     \<open>lo \<le> lo'\<close> and \<open>lo' < length xs\<close> and
     \<open>(\<forall> i. lo\<le>i\<and>i<lo' \<longrightarrow> xs'!i=xs!i)\<close> and \<open>length xs' = length xs\<close>
   shows \<open>sorted_sublist_map R h xs' lo (lo' - Suc 0)\<close>
   using assms by (rule sorted_wrt_lower_sublist_still_sorted)
 
 lemma sorted_wrt_upper_sublist_still_sorted:
   assumes \<open>sorted_sublist_wrt R xs (hi'+1) hi\<close> and
     \<open>lo \<le> lo'\<close> and \<open>hi < length xs\<close> and
     \<open>\<forall> j. hi'<j\<and>j\<le>hi \<longrightarrow> xs'!j=xs!j\<close> and \<open>length xs' = length xs\<close>
   shows \<open>sorted_sublist_wrt R xs' (hi'+1) hi\<close>
 proof -
   have l: \<open>hi' + 1 < hi \<or> hi' + 1 \<ge> hi\<close>
     by linarith
   show ?thesis
     using l apply auto
     subgoal \<comment> \<open>hi' + 1 < h\<close>
       apply (auto simp add: sorted_sublist_wrt_def)
       apply (rewrite sublist_ext[where xs=xs])
       using assms by (auto simp add: sorted_sublist_wrt_def)
     subgoal \<comment> \<open>\<^term>\<open>hi' + 1 \<ge> hi\<close>\<close>
       using assms by (auto simp add: sorted_sublist_wrt_le)
     done
 qed
 
 lemma sorted_map_upper_sublist_still_sorted:
   assumes \<open>sorted_sublist_map R h xs (hi'+1) hi\<close> and
     \<open>lo \<le> lo'\<close> and \<open>hi < length xs\<close> and
     \<open>\<forall> j. hi'<j\<and>j\<le>hi \<longrightarrow> xs'!j=xs!j\<close> and \<open>length xs' = length xs\<close>
   shows \<open>sorted_sublist_map R h xs' (hi'+1) hi\<close>
   using assms by (rule sorted_wrt_upper_sublist_still_sorted)
 
 
 
 
 
 
 
 text \<open>The specification of the partition function\<close>
 definition partition_spec :: \<open>('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> nat \<Rightarrow> bool\<close> where
   \<open>partition_spec R h xs lo hi xs' p \<equiv>
     mset xs' = mset xs \<and> \<comment> \<open>The list is a permutation\<close>
     isPartition_map R h xs' lo hi p \<and> \<comment> \<open>We have a valid partition on the resulting list\<close>
     lo \<le> p \<and> p \<le> hi \<and> \<comment> \<open>The partition index is in bounds\<close>
     (\<forall> i. i<lo \<longrightarrow> xs'!i=xs!i) \<and> (\<forall> i. hi<i\<and>i<length xs' \<longrightarrow> xs'!i=xs!i)\<close> \<comment> \<open>Everything else is unchanged.\<close>
 
 lemma in_set_take_conv_nth:
   \<open>x \<in> set (take n xs) \<longleftrightarrow> (\<exists>m<min n (length xs). xs ! m = x)\<close>
   by (metis in_set_conv_nth length_take min.commute min.strict_boundedE nth_take)
 
 lemma mset_drop_upto: \<open>mset (drop a N) = {#N!i. i \<in># mset_set {a..<length N}#}\<close>
 proof (induction N arbitrary: a)
   case Nil
   then show ?case by simp
 next
   case (Cons c N)
   have upt: \<open>{0..<Suc (length N)} = insert 0 {1..<Suc (length N)}\<close>
     by auto
   then have H: \<open>mset_set {0..<Suc (length N)} = add_mset 0 (mset_set {1..<Suc (length N)})\<close>
     unfolding upt by auto
   have mset_case_Suc: \<open>{#case x of 0 \<Rightarrow> c | Suc x \<Rightarrow> N ! x . x \<in># mset_set {Suc a..<Suc b}#} =
     {#N ! (x-1) . x \<in># mset_set {Suc a..<Suc b}#}\<close> for a b
     by (rule image_mset_cong) (auto split: nat.splits)
   have Suc_Suc: \<open>{Suc a..<Suc b} = Suc ` {a..<b}\<close> for a b
     by auto
   then have mset_set_Suc_Suc: \<open>mset_set {Suc a..<Suc b} = {#Suc n. n \<in># mset_set {a..<b}#}\<close> for a b
     unfolding Suc_Suc by (subst image_mset_mset_set[symmetric]) auto
   have *: \<open>{#N ! (x-Suc 0) . x \<in># mset_set {Suc a..<Suc b}#} = {#N ! x . x \<in># mset_set {a..<b}#}\<close>
     for a b
     by (auto simp add: mset_set_Suc_Suc multiset.map_comp comp_def)
   show ?case
     apply (cases a)
     using Cons[of 0] Cons by (auto simp: nth_Cons drop_Cons H mset_case_Suc *)
 qed
 
 (* Actually, I only need that \<open>set (sublist xs' lo hi) = set (sublist xs lo hi)\<close> *)
 lemma mathias:
   assumes
         Perm: \<open>mset xs' = mset xs\<close>
     and I: \<open>lo\<le>i\<close> \<open>i\<le>hi\<close> \<open>xs'!i=x\<close>
     and Bounds: \<open>hi < length xs\<close>
     and Fix: \<open>\<And> i. i<lo \<Longrightarrow> xs'!i = xs!i\<close> \<open>\<And> j. \<lbrakk>hi<j; j<length xs\<rbrakk> \<Longrightarrow> xs'!j = xs!j\<close>
   shows \<open>\<exists>j. lo\<le>j\<and>j\<le>hi \<and> xs!j = x\<close>
 proof -
   define xs1 xs2 xs3 xs1' xs2' xs3' where
      \<open>xs1 = take lo xs\<close> and
      \<open>xs2 = take (Suc hi - lo) (drop lo xs)\<close> and
      \<open>xs3 = drop (Suc hi) xs\<close> and
      \<open>xs1' = take lo xs'\<close> and
      \<open>xs2' = take (Suc hi - lo) (drop lo xs')\<close> and
      \<open>xs3' = drop (Suc hi) xs'\<close>
   have [simp]: \<open>length xs' = length xs\<close>
     using Perm by (auto dest: mset_eq_length)
   have [simp]: \<open>mset xs1 = mset xs1'\<close>
     using Fix(1) unfolding xs1_def xs1'_def
     by (metis Perm le_cases mset_eq_length nth_take_lemma take_all)
   have [simp]: \<open>mset xs3 = mset xs3'\<close>
     using Fix(2) unfolding xs3_def xs3'_def mset_drop_upto
     by (auto intro: image_mset_cong)
   have \<open>xs = xs1 @ xs2 @ xs3\<close> \<open>xs' = xs1' @ xs2' @ xs3'\<close>
     using I unfolding xs1_def xs2_def xs3_def xs1'_def xs2'_def xs3'_def
     by (metis append.assoc append_take_drop_id le_SucI le_add_diff_inverse order_trans take_add)+
   moreover have \<open>xs ! i = xs2 ! (i - lo)\<close> \<open>i \<ge> length xs1\<close>
     using I Bounds unfolding xs2_def xs1_def by (auto simp: nth_take min_def)
   moreover have  \<open>x \<in> set xs2'\<close>
     using I Bounds unfolding xs2'_def
     by (auto simp: in_set_take_conv_nth
        intro!: exI[of _ \<open>i - lo\<close>])
   ultimately have \<open>x \<in> set xs2\<close>
     using Perm I by (auto dest: mset_eq_setD)
   then obtain j where \<open>xs ! (lo + j) = x\<close> \<open>j \<le> hi - lo\<close>
     unfolding in_set_conv_nth xs2_def
     by auto
   then show ?thesis
     using Bounds I
     by (auto intro: exI[of _ \<open>lo+j\<close>])
 qed
 
 
 text \<open>If we fix the left and right rest of two permutated lists, then the sublists are also permutations.\<close>
 text \<open>But we only need that the sets are equal.\<close>
 lemma mset_sublist_incl:
   assumes Perm: \<open>mset xs' = mset xs\<close>
     and Fix: \<open>\<And> i. i<lo \<Longrightarrow> xs'!i = xs!i\<close> \<open>\<And> j. \<lbrakk>hi<j; j<length xs\<rbrakk> \<Longrightarrow> xs'!j = xs!j\<close>
     and bounds: \<open>lo \<le> hi\<close> \<open>hi < length xs\<close>
   shows \<open>set (sublist xs' lo hi) \<subseteq> set (sublist xs lo hi)\<close>
 proof
   fix x
   assume \<open>x \<in> set (sublist xs' lo hi)\<close>
   then have \<open>\<exists>i. lo\<le>i\<and>i\<le>hi \<and> xs'!i=x\<close>
     by (metis assms(1) bounds(1) bounds(2) size_mset sublist_el')
   then obtain i where I: \<open>lo\<le>i\<close> \<open>i\<le>hi\<close> \<open>xs'!i=x\<close> by blast
   have \<open>\<exists>j. lo\<le>j\<and>j\<le>hi \<and> xs!j=x\<close>
     using Perm I bounds(2) Fix by (rule mathias, auto)
   then show \<open>x \<in> set (sublist xs lo hi)\<close>
     by (simp add: bounds(1) bounds(2) sublist_el')
 qed
 
 
 lemma mset_sublist_eq:
   assumes \<open>mset xs' = mset xs\<close>
     and \<open>\<And> i. i<lo \<Longrightarrow> xs'!i = xs!i\<close>
     and \<open>\<And> j. \<lbrakk>hi<j; j<length xs\<rbrakk> \<Longrightarrow> xs'!j = xs!j\<close>
     and bounds: \<open>lo \<le> hi\<close> \<open>hi < length xs\<close>
   shows \<open>set (sublist xs' lo hi) = set (sublist xs lo hi)\<close>
 proof
   show \<open>set (sublist xs' lo hi) \<subseteq> set (sublist xs lo hi)\<close>
     apply (rule mset_sublist_incl)
     using assms by auto
   show \<open>set (sublist xs lo hi) \<subseteq> set (sublist xs' lo hi)\<close>
     by (rule mset_sublist_incl) (metis assms size_mset)+
 qed
 
 
 
 text \<open>Our abstract recursive quicksort procedure. We abstract over a partition procedure.\<close>
 definition quicksort :: \<open>('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> nat \<times> nat \<times> 'a list \<Rightarrow> 'a list nres\<close> where
 \<open>quicksort R h = (\<lambda>(lo,hi,xs0). do {
   RECT (\<lambda>f (lo,hi,xs). do {
       ASSERT(lo \<le> hi \<and> hi < length xs \<and> mset xs = mset xs0); \<comment> \<open>Premise for a partition function\<close>
       (xs, p) \<leftarrow> SPEC(uncurry (partition_spec R h xs lo hi)); \<comment> \<open>Abstract partition function\<close>
       ASSERT(mset xs = mset xs0);
       xs \<leftarrow> (if p-1\<le>lo then RETURN xs else f (lo, p-1, xs));
       ASSERT(mset xs = mset xs0);
       if hi\<le>p+1 then RETURN xs else f (p+1, hi, xs)
     }) (lo,hi,xs0)
   })\<close>
 
 text \<open>As premise for quicksor, we only need that the indices are ok.\<close>
 definition quicksort_pre :: \<open>('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow>  nat \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> bool\<close> where
   \<open>quicksort_pre R h xs0 lo hi xs \<equiv> lo \<le> hi \<and> hi < length xs \<and> mset xs = mset xs0\<close>
 
 definition quicksort_post :: \<open>('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool\<close> where
   \<open>quicksort_post R h lo hi xs xs' \<equiv>
     mset xs' = mset xs \<and>
     sorted_sublist_map R h xs' lo hi \<and>
     (\<forall> i. i<lo \<longrightarrow> xs'!i = xs!i) \<and>
     (\<forall> j. hi<j\<and>j<length xs \<longrightarrow> xs'!j = xs!j)\<close>
 
 text \<open>Convert Pure to HOL\<close>
 lemma quicksort_postI:
   \<open>\<lbrakk>mset xs' = mset xs; sorted_sublist_map R h xs' lo hi; (\<And> i. \<lbrakk>i<lo\<rbrakk> \<Longrightarrow> xs'!i = xs!i); (\<And> j. \<lbrakk>hi<j; j<length xs\<rbrakk> \<Longrightarrow> xs'!j = xs!j)\<rbrakk> \<Longrightarrow> quicksort_post R h lo hi xs xs'\<close>
   by (auto simp add: quicksort_post_def)
 
 
 text \<open>The first case for the correctness proof of (abstract) quicksort: We assume that we called the partition function, and we have \<^term>\<open>p-1\<le>lo\<close> and \<^term>\<open>hi\<le>p+1\<close>.\<close>
 lemma quicksort_correct_case1:
   assumes trans: \<open>\<And> x y z. \<lbrakk>R (h x) (h y); R (h y) (h z)\<rbrakk> \<Longrightarrow> R (h x) (h z)\<close> and lin: \<open>\<And>x y. x \<noteq> y \<Longrightarrow> R (h x) (h y) \<or> R (h y) (h x)\<close>
     and pre: \<open>quicksort_pre R h xs0 lo hi xs\<close>
     and part: \<open>partition_spec R h xs lo hi xs' p\<close>
     and ifs: \<open>p-1 \<le> lo\<close> \<open>hi \<le> p+1\<close>
   shows \<open>quicksort_post R h lo hi xs xs'\<close>
 proof -
   text \<open>First boilerplate code step: 'unfold' the HOL definitions in the assumptions and convert them to Pure\<close>
   have pre: \<open>lo \<le> hi\<close> \<open>hi < length xs\<close>
     using pre by (auto simp add: quicksort_pre_def)
 (*
   have part_perm: \<open>set (sublist xs' lo hi) = set (sublist xs lo hi)\<close>
     using part partition_spec_set_sublist pre(1) pre(2) by blast
 *)
   have part: \<open>mset xs' = mset xs\<close> True
     \<open>isPartition_map R h xs' lo hi p\<close> \<open>lo \<le> p\<close> \<open>p \<le> hi\<close>
     \<open>\<And> i. i<lo \<Longrightarrow> xs'!i=xs!i\<close> \<open>\<And> i. \<lbrakk>hi<i; i<length xs'\<rbrakk> \<Longrightarrow> xs'!i=xs!i\<close>
     using part by (auto simp add: partition_spec_def)
 
 
   have sorted_lower: \<open>sorted_sublist_map R h xs' lo (p - Suc 0)\<close>
   proof -
     show ?thesis
       apply (rule sorted_sublist_wrt_le)
       subgoal using ifs(1) by auto
       subgoal using ifs(1) mset_eq_length part(1) pre(1) pre(2) by fastforce
       done
   qed
 
   have sorted_upper: \<open>sorted_sublist_map R h xs' (Suc p) hi\<close>
   proof -
     show ?thesis
       apply (rule sorted_sublist_wrt_le)
       subgoal using ifs(2) by auto
       subgoal using ifs(1) mset_eq_length part(1) pre(1) pre(2) by fastforce
       done
   qed
 
   have sorted_middle: \<open>sorted_sublist_map R h xs' lo hi\<close>
   proof -
     show ?thesis
       apply (rule merge_sorted_map_partitions[where p=p])
       subgoal by (rule trans)
       subgoal by (rule part)
       subgoal by (rule sorted_lower)
       subgoal by (rule sorted_upper)
       subgoal using pre(1) by auto
       subgoal by (simp add: part(4))
       subgoal by (simp add: part(5))
       subgoal by (metis part(1) pre(2) size_mset)
       done
   qed
 
   show ?thesis
   proof (intro quicksort_postI)
     show \<open>mset xs' = mset xs\<close>
       by (simp add: part(1))
   next
     show \<open>sorted_sublist_map R h xs' lo hi\<close>
       by (rule sorted_middle)
   next
       show \<open>\<And>i. i < lo \<Longrightarrow> xs' ! i = xs ! i\<close>
       using part(6) by blast
   next
     show \<open>\<And>j. \<lbrakk>hi < j; j < length xs\<rbrakk> \<Longrightarrow> xs' ! j = xs ! j\<close>
       by (metis part(1) part(7) size_mset)
   qed
 qed
 
 
 text \<open>In the second case, we have to show that the precondition still holds for (p+1, hi, x') after the partition.\<close>
 lemma quicksort_correct_case2:
   assumes
         pre: \<open>quicksort_pre R h xs0 lo hi xs\<close>
     and part: \<open>partition_spec R h xs lo hi xs' p\<close>
     and ifs: \<open>\<not> hi \<le> p + 1\<close>
   shows \<open>quicksort_pre R h xs0 (Suc p) hi xs'\<close>
 proof -
   text \<open>First boilerplate code step: 'unfold' the HOL definitions in the assumptions and convert them to Pure\<close>
   have pre: \<open>lo \<le> hi\<close> \<open>hi < length xs\<close> \<open>mset xs = mset xs0\<close>
     using pre by (auto simp add: quicksort_pre_def)
   have part: \<open>mset xs' = mset xs\<close> True
     \<open>isPartition_map R h xs' lo hi p\<close> \<open>lo \<le> p\<close> \<open>p \<le> hi\<close>
     \<open>\<And> i. i<lo \<Longrightarrow> xs'!i=xs!i\<close> \<open>\<And> i. \<lbrakk>hi<i; i<length xs'\<rbrakk> \<Longrightarrow> xs'!i=xs!i\<close>
     using part by (auto simp add: partition_spec_def)
   show ?thesis
     unfolding quicksort_pre_def
   proof (intro conjI)
     show \<open>Suc p \<le> hi\<close>
       using ifs by linarith
     show \<open>hi < length xs'\<close>
       by (metis part(1) pre(2) size_mset)
     show \<open>mset xs' = mset xs0\<close>
       using pre(3) part(1) by (auto dest: mset_eq_setD)
   qed
 qed
 
 
 
 lemma quicksort_post_set:
   assumes \<open>quicksort_post R h lo hi xs xs'\<close>
     and bounds: \<open>lo \<le> hi\<close> \<open>hi < length xs\<close>
   shows \<open>set (sublist xs' lo hi) = set (sublist xs lo hi)\<close>
 proof -
   have \<open>mset xs' = mset xs\<close> \<open>\<And> i. i<lo \<Longrightarrow> xs'!i = xs!i\<close> \<open>\<And> j. \<lbrakk>hi<j; j<length xs\<rbrakk> \<Longrightarrow> xs'!j = xs!j\<close>
     using assms by (auto simp add: quicksort_post_def)
   then show ?thesis
     using bounds by (rule mset_sublist_eq, auto)
 qed
 
 
 text \<open>In the third case, we have run quicksort recursively on (p+1, hi, xs') after the partition, with hi<=p+1 and p-1<=lo.\<close>
 lemma quicksort_correct_case3:
   assumes trans: \<open>\<And> x y z. \<lbrakk>R (h x) (h y); R (h y) (h z)\<rbrakk> \<Longrightarrow> R (h x) (h z)\<close> and lin: \<open>\<And>x y. x \<noteq> y \<Longrightarrow> R (h x) (h y) \<or> R (h y) (h x)\<close>
     and pre: \<open>quicksort_pre R h xs0 lo hi xs\<close>
     and part: \<open>partition_spec R h xs lo hi xs' p\<close>
     and ifs: \<open>p - Suc 0 \<le> lo\<close> \<open>\<not> hi \<le> Suc p\<close>
     and IH1': \<open>quicksort_post R h (Suc p) hi xs' xs''\<close>
   shows \<open>quicksort_post R h lo hi xs xs''\<close>
 proof -
   text \<open>First boilerplate code step: 'unfold' the HOL definitions in the assumptions and convert them to Pure\<close>
   have pre: \<open>lo \<le> hi\<close> \<open>hi < length xs\<close> \<open>mset xs = mset xs0\<close>
     using pre by (auto simp add: quicksort_pre_def)
   have part: \<open>mset xs' = mset xs\<close> True
     \<open>isPartition_map R h xs' lo hi p\<close> \<open>lo \<le> p\<close> \<open>p \<le> hi\<close>
     \<open>\<And> i. i<lo \<Longrightarrow> xs'!i=xs!i\<close> \<open>\<And> i. \<lbrakk>hi<i; i<length xs'\<rbrakk> \<Longrightarrow> xs'!i=xs!i\<close>
     using part by (auto simp add: partition_spec_def)
   have IH1: \<open>mset xs'' = mset xs'\<close> \<open>sorted_sublist_map R h xs'' (Suc p) hi\<close>
       \<open>\<And> i. i<Suc p \<Longrightarrow> xs'' ! i = xs' ! i\<close> \<open>\<And> j. \<lbrakk>hi < j; j < length xs'\<rbrakk> \<Longrightarrow> xs'' ! j = xs' ! j\<close>
     using IH1' by (auto simp add: quicksort_post_def)
   note IH1_perm = quicksort_post_set[OF IH1']
 
   have still_partition: \<open>isPartition_map R h xs'' lo hi p\<close>
   proof(intro isPartition_wrtI)
     fix i assume \<open>lo \<le> i\<close> \<open>i < p\<close>
     show \<open>R (h (xs'' ! i)) (h (xs'' ! p))\<close>
       text \<open>This holds because this part hasn't changed\<close>
       using IH1(3) \<open>i < p\<close> \<open>lo \<le> i\<close> isPartition_wrt_def part(3) by fastforce
     next
       fix j assume \<open>p < j\<close> \<open>j \<le> hi\<close>
       text \<open>Obtain the position \<^term>\<open>posJ\<close> where \<^term>\<open>xs''!j\<close> was stored in \<^term>\<open>xs'\<close>.\<close>
       have \<open>xs''!j \<in> set (sublist xs'' (Suc p) hi)\<close>
         by (metis IH1(1) Suc_leI \<open>j \<le> hi\<close> \<open>p < j\<close> less_le_trans mset_eq_length part(1) pre(2) sublist_el')
       then have \<open>xs''!j \<in> set (sublist xs' (Suc p) hi)\<close>
         by (metis IH1_perm ifs(2) nat_le_linear part(1) pre(2) size_mset)
       then have \<open>\<exists> posJ. Suc p\<le>posJ\<and>posJ\<le>hi \<and> xs''!j = xs'!posJ\<close>
         by (metis Suc_leI \<open>j \<le> hi\<close> \<open>p < j\<close> less_le_trans part(1) pre(2) size_mset sublist_el')
       then obtain posJ :: nat where PosJ: \<open>Suc p\<le>posJ\<close> \<open>posJ\<le>hi\<close> \<open>xs''!j = xs'!posJ\<close> by blast
 
       then show \<open>R (h (xs'' ! p)) (h (xs'' ! j))\<close>
         by (metis IH1(3) Suc_le_lessD isPartition_wrt_def lessI part(3))
   qed
 
   have sorted_lower: \<open>sorted_sublist_map R h xs'' lo (p - Suc 0)\<close>
   proof -
     show ?thesis
       apply (rule sorted_sublist_wrt_le)
       subgoal by (simp add: ifs(1))
       subgoal using IH1(1) mset_eq_length part(1) part(5) pre(2) by fastforce
       done
   qed
 
   note sorted_upper = IH1(2)
 
   have sorted_middle: \<open>sorted_sublist_map R h xs'' lo hi\<close>
   proof -
     show ?thesis
       apply (rule merge_sorted_map_partitions[where p=p])
       subgoal by (rule trans)
       subgoal by (rule still_partition)
       subgoal by (rule sorted_lower)
       subgoal by (rule sorted_upper)
       subgoal using pre(1) by auto
       subgoal by (simp add: part(4))
       subgoal by (simp add: part(5))
       subgoal by (metis IH1(1) part(1) pre(2) size_mset)
       done
   qed
 
 
   show ?thesis
   proof (intro quicksort_postI)
     show \<open>mset xs'' = mset xs\<close>
       using part(1) IH1(1) by auto \<comment> \<open>I was faster than sledgehammer :-)\<close>
   next
     show \<open>sorted_sublist_map R h xs'' lo hi\<close>
       by (rule sorted_middle)
   next
     show \<open>\<And>i. i < lo \<Longrightarrow> xs'' ! i = xs ! i\<close>
       using IH1(3) le_SucI part(4) part(6) by auto
   next show \<open>\<And>j. hi < j \<Longrightarrow> j < length xs \<Longrightarrow> xs'' ! j = xs ! j\<close>
       by (metis IH1(4) part(1) part(7) size_mset)
   qed
 qed
 
 
 text \<open>In the 4th case, we have to show that the premise holds for \<^term>\<open>(lo,p-1,xs')\<close>, in case \<^term>\<open>\<not>p-1\<le>lo\<close>\<close>
 text \<open>Analogous to case 2.\<close>
 lemma quicksort_correct_case4:
   assumes
         pre: \<open>quicksort_pre R h xs0 lo hi xs\<close>
     and part: \<open>partition_spec R h xs lo hi xs' p\<close>
     and ifs: \<open>\<not> p - Suc 0 \<le> lo \<close>
   shows \<open>quicksort_pre R h xs0 lo (p-Suc 0) xs'\<close>
 proof -
   text \<open>First boilerplate code step: 'unfold' the HOL definitions in the assumptions and convert them to Pure\<close>
   have pre: \<open>lo \<le> hi\<close> \<open>hi < length xs\<close> \<open>mset xs0 = mset xs\<close>
     using pre by (auto simp add: quicksort_pre_def)
   have part: \<open>mset xs' = mset xs\<close> True
     \<open>isPartition_map R h xs' lo hi p\<close> \<open>lo \<le> p\<close> \<open>p \<le> hi\<close>
     \<open>\<And> i. i<lo \<Longrightarrow> xs'!i=xs!i\<close> \<open>\<And> i. \<lbrakk>hi<i; i<length xs'\<rbrakk> \<Longrightarrow> xs'!i=xs!i\<close>
     using part by (auto simp add: partition_spec_def)
 
   show ?thesis
     unfolding quicksort_pre_def
   proof (intro conjI)
     show \<open>lo \<le> p - Suc 0\<close>
       using ifs by linarith
     show \<open>p - Suc 0 < length xs'\<close>
       using mset_eq_length part(1) part(5) pre(2) by fastforce
     show \<open>mset xs' = mset xs0\<close>
       using pre(3) part(1) by (auto dest: mset_eq_setD)
   qed
 qed
 
 
 text \<open>In the 5th case, we have run quicksort recursively on (lo, p-1, xs').\<close>
 lemma quicksort_correct_case5:
   assumes trans: \<open>\<And> x y z. \<lbrakk>R (h x) (h y); R (h y) (h z)\<rbrakk> \<Longrightarrow> R (h x) (h z)\<close> and lin: \<open>\<And>x y. x \<noteq> y \<Longrightarrow> R (h x) (h y) \<or> R (h y) (h x)\<close>
     and pre: \<open>quicksort_pre R h xs0 lo hi xs\<close>
     and part: \<open>partition_spec R h xs lo hi xs' p\<close>
     and ifs:  \<open>\<not> p - Suc 0 \<le> lo\<close> \<open>hi \<le> Suc p\<close>
     and IH1': \<open>quicksort_post R h lo (p - Suc 0) xs' xs''\<close>
   shows \<open>quicksort_post R h lo hi xs xs''\<close>
 proof -
   text \<open>First boilerplate code step: 'unfold' the HOL definitions in the assumptions and convert them to Pure\<close>
   have pre: \<open>lo \<le> hi\<close> \<open>hi < length xs\<close>
     using pre by (auto simp add: quicksort_pre_def)
   have part: \<open>mset xs' = mset xs\<close> True
     \<open>isPartition_map R h xs' lo hi p\<close> \<open>lo \<le> p\<close> \<open>p \<le> hi\<close>
     \<open>\<And> i. i<lo \<Longrightarrow> xs'!i=xs!i\<close> \<open>\<And> i. \<lbrakk>hi<i; i<length xs'\<rbrakk> \<Longrightarrow> xs'!i=xs!i\<close>
     using part by (auto simp add: partition_spec_def)
   have IH1: \<open>mset xs'' = mset xs'\<close> \<open>sorted_sublist_map R h xs'' lo (p - Suc 0)\<close>
     \<open>\<And> i. i<lo \<Longrightarrow> xs''!i = xs'!i\<close> \<open>\<And> j. \<lbrakk>p-Suc 0<j; j<length xs'\<rbrakk> \<Longrightarrow> xs''!j = xs'!j\<close>
     using IH1' by (auto simp add: quicksort_post_def)
   note IH1_perm = quicksort_post_set[OF IH1']
 
 
  have still_partition: \<open>isPartition_map R h xs'' lo hi p\<close>
   proof(intro isPartition_wrtI)
     fix i assume \<open>lo \<le> i\<close> \<open>i < p\<close>
       text \<open>Obtain the position \<^term>\<open>posI\<close> where \<^term>\<open>xs''!i\<close> was stored in \<^term>\<open>xs'\<close>.\<close>
       have \<open>xs''!i \<in> set (sublist xs'' lo (p-Suc 0))\<close>
         by (metis (no_types, lifting) IH1(1) Suc_leI Suc_pred \<open>i < p\<close> \<open>lo \<le> i\<close> le_less_trans less_imp_diff_less mset_eq_length not_le not_less_zero part(1) part(5) pre(2) sublist_el')
       then have \<open>xs''!i \<in> set (sublist xs' lo (p-Suc 0))\<close>
         by (metis IH1_perm ifs(1) le_less_trans less_imp_diff_less mset_eq_length nat_le_linear part(1) part(5) pre(2))
       then have \<open>\<exists> posI. lo\<le>posI\<and>posI\<le>p-Suc 0 \<and> xs''!i = xs'!posI\<close>
       proof - \<comment> \<open>sledgehammer\<close>
         have "p - Suc 0 < length xs"
           by (meson diff_le_self le_less_trans part(5) pre(2))
         then show ?thesis
           by (metis (no_types) \<open>xs'' ! i \<in> set (sublist xs' lo (p - Suc 0))\<close> ifs(1) mset_eq_length nat_le_linear part(1) sublist_el')
       qed
       then obtain posI :: nat where PosI: \<open>lo\<le>posI\<close> \<open>posI\<le>p-Suc 0\<close> \<open>xs''!i = xs'!posI\<close> by blast
       then show \<open>R (h (xs'' ! i)) (h (xs'' ! p))\<close>
         by (metis (no_types, lifting) IH1(4) \<open>i < p\<close> diff_Suc_less isPartition_wrt_def le_less_trans mset_eq_length not_le not_less_eq part(1) part(3) part(5) pre(2) zero_less_Suc)
     next
       fix j assume \<open>p < j\<close> \<open>j \<le> hi\<close>
       then show \<open>R (h (xs'' ! p)) (h (xs'' ! j))\<close>
       text \<open>This holds because this part hasn't changed\<close>
       by (smt IH1(4) add_diff_cancel_left' add_diff_inverse_nat diff_Suc_eq_diff_pred diff_le_self ifs(1) isPartition_wrt_def le_less_Suc_eq less_le_trans mset_eq_length nat_less_le part(1) part(3) part(4) plus_1_eq_Suc pre(2))
   qed
 
 
   note sorted_lower = IH1(2)
 
   have sorted_upper: \<open>sorted_sublist_map R h xs'' (Suc p) hi\<close>
   proof -
     show ?thesis
       apply (rule sorted_sublist_wrt_le)
       subgoal by (simp add: ifs(2))
       subgoal using IH1(1) mset_eq_length part(1) part(5) pre(2) by fastforce
       done
   qed
 
 
   have sorted_middle: \<open>sorted_sublist_map R h xs'' lo hi\<close>
   proof -
     show ?thesis
       apply (rule merge_sorted_map_partitions[where p=p])
       subgoal by (rule trans)
       subgoal by (rule still_partition)
       subgoal by (rule sorted_lower)
       subgoal by (rule sorted_upper)
       subgoal using pre(1) by auto
       subgoal by (simp add: part(4))
       subgoal by (simp add: part(5))
       subgoal by (metis IH1(1) part(1) pre(2) size_mset)
       done
   qed
 
 
   show ?thesis
   proof (intro quicksort_postI)
     show \<open>mset xs'' = mset xs\<close>
       by (simp add: IH1(1) part(1))
   next
     show \<open>sorted_sublist_map R h xs'' lo hi\<close>
       by (rule sorted_middle)
   next
     show \<open>\<And>i. i < lo \<Longrightarrow> xs'' ! i = xs ! i\<close>
       by (simp add: IH1(3) part(6))
   next
     show \<open>\<And>j. hi < j \<Longrightarrow> j < length xs \<Longrightarrow> xs'' ! j = xs ! j\<close>
       by (metis IH1(4) diff_le_self dual_order.strict_trans2 mset_eq_length part(1) part(5) part(7))
   qed
 qed
 
 
 text \<open>In the 6th case, we have run quicksort recursively on (lo, p-1, xs'). We show the precondition on the second call on (p+1, hi, xs'')\<close>
 lemma quicksort_correct_case6:
   assumes
         pre: \<open>quicksort_pre R h xs0 lo hi xs\<close>
     and part: \<open>partition_spec R h xs lo hi xs' p\<close>
     and ifs:  \<open>\<not> p - Suc 0 \<le> lo\<close> \<open>\<not> hi \<le> Suc p\<close>
     and IH1: \<open>quicksort_post R h lo (p - Suc 0) xs' xs''\<close>
   shows \<open>quicksort_pre R h xs0 (Suc p) hi xs''\<close>
 proof -
   text \<open>First boilerplate code step: 'unfold' the HOL definitions in the assumptions and convert them to Pure\<close>
   have pre: \<open>lo \<le> hi\<close> \<open>hi < length xs\<close> \<open>mset xs0 = mset xs\<close>
     using pre by (auto simp add: quicksort_pre_def)
   have part: \<open>mset xs' = mset xs\<close> True
     \<open>isPartition_map R h xs' lo hi p\<close> \<open>lo \<le> p\<close> \<open>p \<le> hi\<close>
     \<open>\<And> i. i<lo \<Longrightarrow> xs'!i=xs!i\<close> \<open>\<And> i. \<lbrakk>hi<i; i<length xs'\<rbrakk> \<Longrightarrow> xs'!i=xs!i\<close>
     using part by (auto simp add: partition_spec_def)
   have IH1: \<open>mset xs'' = mset xs'\<close> \<open>sorted_sublist_map R h xs'' lo (p - Suc 0)\<close>
     \<open>\<And> i. i<lo \<Longrightarrow> xs''!i = xs'!i\<close> \<open>\<And> j. \<lbrakk>p-Suc 0<j; j<length xs'\<rbrakk> \<Longrightarrow> xs''!j = xs'!j\<close>
     using IH1 by (auto simp add: quicksort_post_def)
 
   show ?thesis
     unfolding quicksort_pre_def
   proof (intro conjI)
     show \<open>Suc p \<le> hi\<close>
       using ifs(2) by linarith
     show \<open>hi < length xs''\<close>
       using IH1(1) mset_eq_length part(1) pre(2) by fastforce
     show \<open>mset xs'' = mset xs0\<close>
       using pre(3) part(1) IH1(1) by (auto dest: mset_eq_setD)
   qed
 qed
 
 
 text \<open>In the 7th (and last) case, we have run quicksort recursively on (lo, p-1, xs'). We show the postcondition on the second call on (p+1, hi, xs'')\<close>
 lemma quicksort_correct_case7:
   assumes trans: \<open>\<And> x y z. \<lbrakk>R (h x) (h y); R (h y) (h z)\<rbrakk> \<Longrightarrow> R (h x) (h z)\<close> and lin: \<open>\<And>x y. x \<noteq> y \<Longrightarrow> R (h x) (h y) \<or> R (h y) (h x)\<close>
     and pre: \<open>quicksort_pre R h xs0 lo hi xs\<close>
     and part: \<open>partition_spec R h xs lo hi xs' p\<close>
     and ifs:  \<open>\<not> p - Suc 0 \<le> lo\<close> \<open>\<not> hi \<le> Suc p\<close>
     and IH1': \<open>quicksort_post R h lo (p - Suc 0) xs' xs''\<close>
     and IH2': \<open>quicksort_post R h (Suc p) hi xs'' xs'''\<close>
   shows \<open>quicksort_post R h lo hi xs xs'''\<close>
 proof -
   text \<open>First boilerplate code step: 'unfold' the HOL definitions in the assumptions and convert them to Pure\<close>
   have pre: \<open>lo \<le> hi\<close> \<open>hi < length xs\<close>
     using pre by (auto simp add: quicksort_pre_def)
   have part: \<open>mset xs' = mset xs\<close> True
     \<open>isPartition_map R h xs' lo hi p\<close> \<open>lo \<le> p\<close> \<open>p \<le> hi\<close>
     \<open>\<And> i. i<lo \<Longrightarrow> xs'!i=xs!i\<close> \<open>\<And> i. \<lbrakk>hi<i; i<length xs'\<rbrakk> \<Longrightarrow> xs'!i=xs!i\<close>
     using part by (auto simp add: partition_spec_def)
   have IH1: \<open>mset xs'' = mset xs'\<close> \<open>sorted_sublist_map R h xs'' lo (p - Suc 0)\<close>
     \<open>\<And> i. i<lo \<Longrightarrow> xs''!i = xs'!i\<close> \<open>\<And> j. \<lbrakk>p-Suc 0<j; j<length xs'\<rbrakk> \<Longrightarrow> xs''!j = xs'!j\<close>
     using IH1' by (auto simp add: quicksort_post_def)
   note IH1_perm = quicksort_post_set[OF IH1']
   have IH2: \<open>mset xs''' = mset xs''\<close> \<open>sorted_sublist_map R h xs''' (Suc p) hi\<close>
     \<open>\<And> i. i<Suc p \<Longrightarrow> xs'''!i = xs''!i\<close> \<open>\<And> j. \<lbrakk>hi<j; j<length xs''\<rbrakk> \<Longrightarrow> xs'''!j = xs''!j\<close>
     using IH2' by (auto simp add: quicksort_post_def)
   note IH2_perm = quicksort_post_set[OF IH2']
 
 
   text \<open>We still have a partition after the first call (same as in case 5)\<close>
   have still_partition1: \<open>isPartition_map R h xs'' lo hi p\<close>
   proof(intro isPartition_wrtI)
     fix i assume \<open>lo \<le> i\<close> \<open>i < p\<close>
       text \<open>Obtain the position \<^term>\<open>posI\<close> where \<^term>\<open>xs''!i\<close> was stored in \<^term>\<open>xs'\<close>.\<close>
       have \<open>xs''!i \<in> set (sublist xs'' lo (p-Suc 0))\<close>
         by (metis (no_types, lifting) IH1(1) Suc_leI Suc_pred \<open>i < p\<close> \<open>lo \<le> i\<close> le_less_trans less_imp_diff_less mset_eq_length not_le not_less_zero part(1) part(5) pre(2) sublist_el')
       then have \<open>xs''!i \<in> set (sublist xs' lo (p-Suc 0))\<close>
         by (metis IH1_perm ifs(1) le_less_trans less_imp_diff_less mset_eq_length nat_le_linear part(1) part(5) pre(2))
       then have \<open>\<exists> posI. lo\<le>posI\<and>posI\<le>p-Suc 0 \<and> xs''!i = xs'!posI\<close>
       proof - \<comment> \<open>sledgehammer\<close>
         have "p - Suc 0 < length xs"
           by (meson diff_le_self le_less_trans part(5) pre(2))
         then show ?thesis
           by (metis (no_types) \<open>xs'' ! i \<in> set (sublist xs' lo (p - Suc 0))\<close> ifs(1) mset_eq_length nat_le_linear part(1) sublist_el')
       qed
       then obtain posI :: nat where PosI: \<open>lo\<le>posI\<close> \<open>posI\<le>p-Suc 0\<close> \<open>xs''!i = xs'!posI\<close> by blast
       then show \<open>R (h (xs'' ! i)) (h (xs'' ! p))\<close>
         by (metis (no_types, lifting) IH1(4) \<open>i < p\<close> diff_Suc_less isPartition_wrt_def le_less_trans mset_eq_length not_le not_less_eq part(1) part(3) part(5) pre(2) zero_less_Suc)
     next
       fix j assume \<open>p < j\<close> \<open>j \<le> hi\<close>
       then show \<open>R (h (xs'' ! p)) (h (xs'' ! j))\<close>
       text \<open>This holds because this part hasn't changed\<close>
       by (smt IH1(4) add_diff_cancel_left' add_diff_inverse_nat diff_Suc_eq_diff_pred diff_le_self ifs(1) isPartition_wrt_def le_less_Suc_eq less_le_trans mset_eq_length nat_less_le part(1) part(3) part(4) plus_1_eq_Suc pre(2))
   qed
 
 
   text \<open>We still have a partition after the second call (similar as in case 3)\<close>
   have still_partition2: \<open>isPartition_map R h xs''' lo hi p\<close>
   proof(intro isPartition_wrtI)
     fix i assume \<open>lo \<le> i\<close> \<open>i < p\<close>
     show \<open>R (h (xs''' ! i)) (h (xs''' ! p))\<close>
       text \<open>This holds because this part hasn't changed\<close>
       using IH2(3) \<open>i < p\<close> \<open>lo \<le> i\<close> isPartition_wrt_def still_partition1 by fastforce
     next
       fix j assume \<open>p < j\<close> \<open>j \<le> hi\<close>
       text \<open>Obtain the position \<^term>\<open>posJ\<close> where \<^term>\<open>xs'''!j\<close> was stored in \<^term>\<open>xs'''\<close>.\<close>
       have \<open>xs'''!j \<in> set (sublist xs''' (Suc p) hi)\<close>
         by (metis IH1(1) IH2(1) Suc_leI \<open>j \<le> hi\<close> \<open>p < j\<close> ifs(2) nat_le_linear part(1) pre(2) size_mset sublist_el')
       then have \<open>xs'''!j \<in> set (sublist xs'' (Suc p) hi)\<close>
         by (metis IH1(1) IH2_perm ifs(2) mset_eq_length nat_le_linear part(1) pre(2))
       then have \<open>\<exists> posJ. Suc p\<le>posJ\<and>posJ\<le>hi \<and> xs'''!j = xs''!posJ\<close>
         by (metis IH1(1) ifs(2) mset_eq_length nat_le_linear part(1) pre(2) sublist_el')
       then obtain posJ :: nat where PosJ: \<open>Suc p\<le>posJ\<close> \<open>posJ\<le>hi\<close> \<open>xs'''!j = xs''!posJ\<close> by blast
 
       then show \<open>R (h (xs''' ! p)) (h (xs''' ! j))\<close>
       proof - \<comment> \<open>sledgehammer\<close>
         have "\<forall>n na as p. (p (as ! na::'a) (as ! posJ) \<or> posJ \<le> na) \<or> \<not> isPartition_wrt p as n hi na"
           by (metis (no_types) PosJ(2) isPartition_wrt_def not_less)
         then show ?thesis
           by (metis IH2(3) PosJ(1) PosJ(3) lessI not_less_eq_eq still_partition1)
       qed
   qed
 
 
   text \<open>We have that the lower part is sorted after the first recursive call\<close>
   note sorted_lower1 = IH1(2)
 
   text \<open>We show that it is still sorted after the second call.\<close>
   have sorted_lower2: \<open>sorted_sublist_map R h xs''' lo (p-Suc 0)\<close>
   proof -
     show ?thesis
       using sorted_lower1 apply (rule sorted_wrt_lower_sublist_still_sorted)
       subgoal by (rule part)
       subgoal
         using IH1(1) mset_eq_length part(1) part(5) pre(2) by fastforce
       subgoal
         by (simp add: IH2(3))
       subgoal
         by (metis IH2(1) size_mset)
       done
   qed
 
   text \<open>The second IH gives us the the upper list is sorted after the second recursive call\<close>
   note sorted_upper2 = IH2(2)
 
   text \<open>Finally, we have to show that the entire list is sorted after the second recursive call.\<close>
   have sorted_middle: \<open>sorted_sublist_map R h xs''' lo hi\<close>
   proof -
     show ?thesis
       apply (rule merge_sorted_map_partitions[where p=p])
       subgoal by (rule trans)
       subgoal by (rule still_partition2)
       subgoal by (rule sorted_lower2)
       subgoal by (rule sorted_upper2)
       subgoal using pre(1) by auto
       subgoal by (simp add: part(4))
       subgoal by (simp add: part(5))
       subgoal by (metis IH1(1) IH2(1) part(1) pre(2) size_mset)
       done
   qed
 
   show ?thesis
   proof (intro quicksort_postI)
     show \<open>mset xs''' = mset xs\<close>
       by (simp add: IH1(1) IH2(1) part(1))
   next
     show \<open>sorted_sublist_map R h xs''' lo hi\<close>
       by (rule sorted_middle)
   next
     show \<open>\<And>i. i < lo \<Longrightarrow> xs''' ! i = xs ! i\<close>
       using IH1(3) IH2(3) part(4) part(6) by auto
   next
     show \<open>\<And>j. hi < j \<Longrightarrow> j < length xs \<Longrightarrow> xs''' ! j = xs ! j\<close>
       by (metis IH1(1) IH1(4) IH2(4) diff_le_self ifs(2) le_SucI less_le_trans nat_le_eq_or_lt not_less part(1) part(7) size_mset)
   qed
 
 qed
 
 
 
 text \<open>We can now show the correctness of the abstract quicksort procedure, using the refinement framework and the above case lemmas.\<close>
 lemma quicksort_correct:
   assumes trans: \<open>\<And> x y z. \<lbrakk>R (h x) (h y); R (h y) (h z)\<rbrakk> \<Longrightarrow> R (h x) (h z)\<close> and lin: \<open>\<And>x y. x \<noteq> y \<Longrightarrow> R (h x) (h y) \<or> R (h y) (h x)\<close>
      and Pre: \<open>lo0 \<le> hi0\<close> \<open>hi0 < length xs0\<close>
   shows \<open>quicksort R h (lo0,hi0,xs0) \<le> \<Down> Id (SPEC(\<lambda>xs. quicksort_post R h lo0 hi0 xs0 xs))\<close>
 proof -
   have wf: \<open>wf (measure (\<lambda>(lo, hi, xs). Suc hi - lo))\<close>
     by auto
   define pre where \<open>pre = (\<lambda>(lo,hi,xs). quicksort_pre R h xs0 lo hi xs)\<close>
   define post where \<open>post = (\<lambda>(lo,hi,xs). quicksort_post R h lo hi xs)\<close>
   have pre: \<open>pre (lo0,hi0,xs0)\<close>
     unfolding quicksort_pre_def pre_def by (simp add: Pre)
 
   text \<open>We first generalize the goal a over all states.\<close>
   have \<open>WB_Sort.quicksort R h (lo0,hi0,xs0) \<le> \<Down> Id (SPEC (post (lo0,hi0,xs0)))\<close>
     unfolding quicksort_def prod.case
     apply (rule RECT_rule)
        apply (refine_mono)
       apply (rule wf)
     apply (rule pre)
     subgoal premises IH for f x
       apply (refine_vcg ASSERT_leI)
       unfolding pre_def post_def
 
       subgoal \<comment> \<open>First premise (assertion) for partition\<close>
         using IH(2) by (simp add: quicksort_pre_def pre_def)
       subgoal \<comment> \<open>Second premise (assertion) for partition\<close>
         using IH(2) by (simp add: quicksort_pre_def pre_def)
       subgoal
         using IH(2) by (auto simp add: quicksort_pre_def pre_def dest: mset_eq_setD)
 
 	text \<open>Termination case: \<^term>\<open>(p-1 \<le> lo')\<close> and \<^term>\<open>(hi' \<le> p+1)\<close>; directly show postcondition\<close>
       subgoal unfolding partition_spec_def by (auto dest: mset_eq_setD)
       subgoal \<comment> \<open>Postcondition (after partition)\<close>
         apply -
         using IH(2) unfolding pre_def apply (simp, elim conjE, split prod.splits)
         using trans lin apply (rule quicksort_correct_case1) by auto
 
       text \<open>Case \<^term>\<open>(p-1 \<le> lo')\<close> and \<^term>\<open>(hi' < p+1)\<close> (Only second recursive call)\<close>
       subgoal
         apply (rule IH(1)[THEN order_trans])
 
         text \<open>Show that the invariant holds for the second recursive call\<close>
         subgoal
           using IH(2) unfolding pre_def apply (simp, elim conjE, split prod.splits)
           apply (rule quicksort_correct_case2) by auto
 
         text \<open>Wellfoundness (easy)\<close>
         subgoal by (auto simp add: quicksort_pre_def partition_spec_def)
 
         text \<open>Show that the postcondition holds\<close>
         subgoal
           apply (simp add: Misc.subset_Collect_conv post_def, intro allI impI, elim conjE)
           using trans lin apply (rule quicksort_correct_case3)
           using IH(2) unfolding pre_def by auto
         done
 
       text \<open>Case: At least the first recursive call\<close>
       subgoal
         apply (rule IH(1)[THEN order_trans])
 
         text \<open>Show that the precondition holds for the first recursive call\<close>
         subgoal
           using IH(2) unfolding pre_def post_def apply (simp, elim conjE, split prod.splits) apply auto
           apply (rule quicksort_correct_case4) by auto
 
         text \<open>Wellfoundness for first recursive call (easy)\<close>
         subgoal by (auto simp add: quicksort_pre_def partition_spec_def)
 
         text \<open>Simplify some refinement suff...\<close>
         apply (simp add: Misc.subset_Collect_conv ASSERT_leI, intro allI impI conjI, elim conjE)
         apply (rule ASSERT_leI)
         apply (simp_all add: Misc.subset_Collect_conv ASSERT_leI)
         subgoal unfolding quicksort_post_def pre_def post_def by (auto dest: mset_eq_setD)
         text \<open>Only the first recursive call: show postcondition\<close>
         subgoal
           using trans lin apply (rule quicksort_correct_case5)
           using IH(2) unfolding pre_def post_def by auto
 
         apply (rule ASSERT_leI)
         subgoal unfolding quicksort_post_def pre_def post_def by (auto dest: mset_eq_setD)
 
         text \<open>Both recursive calls.\<close>
         subgoal
           apply (rule IH(1)[THEN order_trans])
 
           text \<open>Show precondition for second recursive call (after the first call)\<close>
           subgoal
             unfolding pre_def post_def
             apply auto
             apply (rule quicksort_correct_case6)
             using IH(2) unfolding pre_def post_def  by auto
 
           text \<open>Wellfoundedness for second recursive call (easy)\<close>
           subgoal by (auto simp add: quicksort_pre_def partition_spec_def)
 
           text \<open>Show that the postcondition holds (after both recursive calls)\<close>
           subgoal
             apply (simp add: Misc.subset_Collect_conv, intro allI impI, elim conjE)
             using trans lin apply (rule quicksort_correct_case7)
             using IH(2) unfolding pre_def post_def by auto
           done
         done
       done
     done
 
   text \<open>Finally, apply the generalized lemma to show the thesis.\<close>
   then show ?thesis unfolding post_def  by auto
 qed
 
 
 
 (* TODO: Show that our (abstract) partition satisifies the specification *)
 
 
 definition partition_main_inv :: \<open>('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> (nat\<times>nat\<times>'a list) \<Rightarrow> bool\<close> where
   \<open>partition_main_inv R h lo hi xs0 p \<equiv>
     case p of (i,j,xs) \<Rightarrow>
     j < length xs \<and> j \<le> hi \<and> i < length xs \<and> lo \<le> i \<and> i \<le> j \<and> mset xs = mset xs0 \<and>
     (\<forall>k. k \<ge> lo \<and> k < i \<longrightarrow> R (h (xs!k)) (h (xs!hi))) \<and> \<comment> \<open>All elements from \<^term>\<open>lo\<close> to \<^term>\<open>i-1\<close> are smaller than the pivot\<close>
     (\<forall>k. k \<ge> i \<and> k < j \<longrightarrow>  R (h (xs!hi)) (h (xs!k))) \<and> \<comment> \<open>All elements from \<^term>\<open>i\<close> to \<^term>\<open>j-1\<close> are greater than the pivot\<close>
     (\<forall>k. k < lo \<longrightarrow> xs!k = xs0!k) \<and> \<comment> \<open>Everything below \<^term>\<open>lo\<close> is unchanged\<close>
     (\<forall>k. k \<ge> j \<and> k < length xs \<longrightarrow> xs!k = xs0!k) \<comment> \<open>All elements from \<^term>\<open>j\<close> are unchanged (including everyting above \<^term>\<open>hi\<close>)\<close>
   \<close>
 
 text \<open>The main part of the partition function. The pivot is assumed to be the last element. This is
 exactly the "Lomuto partition scheme" partition function from Wikipedia.\<close>
 definition partition_main :: \<open>('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> ('a list \<times> nat) nres\<close> where
   \<open>partition_main R h lo hi xs0 = do {
     ASSERT(hi < length xs0);
     pivot \<leftarrow> RETURN (h (xs0 ! hi));
     (i,j,xs) \<leftarrow> WHILE\<^sub>T\<^bsup>partition_main_inv R h lo hi xs0\<^esup> \<comment> \<open>We loop from \<^term>\<open>j=lo\<close> to \<^term>\<open>j=hi-1\<close>.\<close>
       (\<lambda>(i,j,xs). j < hi)
       (\<lambda>(i,j,xs). do {
         ASSERT(i < length xs \<and> j < length xs);
       	if R (h (xs!j)) pivot
       	then RETURN (i+1, j+1, swap xs i j)
       	else RETURN (i,   j+1, xs)
       })
       (lo, lo, xs0); \<comment> \<open>i and j are both initialized to lo\<close>
     ASSERT(i < length xs \<and> j = hi \<and> lo \<le> i \<and> hi < length xs \<and> mset xs = mset xs0);
     RETURN (swap xs i hi, i)
   }\<close>
 
 (*
 definition partition_spec :: \<open>('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> nat \<Rightarrow> bool\<close> where
   \<open>partition_spec R h xs lo hi xs' p \<equiv>
     mset xs' = mset xs \<and> \<comment> \<open>The list is a permutation\<close>
     isPartition_map R h xs' lo hi p \<and> \<comment> \<open>We have a valid partition on the resulting list\<close>
     lo \<le> p \<and> p \<le> hi \<and> \<comment> \<open>The partition index is in bounds\<close>
     (\<forall> i. i<lo \<longrightarrow> xs'!i=xs!i) \<and> (\<forall> i. hi<i\<and>i<length xs' \<longrightarrow> xs'!i=xs!i)\<close> \<comment> \<open>Everything else is unchanged.\<close>
 *)
 
 lemma partition_main_correct:
   assumes bounds: \<open>hi < length xs\<close> \<open>lo \<le> hi\<close> and
     trans: \<open>\<And> x y z. \<lbrakk>R (h x) (h y); R (h y) (h z)\<rbrakk> \<Longrightarrow> R (h x) (h z)\<close> and lin: \<open>\<And>x y. R (h x) (h y) \<or> R (h y) (h x)\<close>
   shows \<open>partition_main R h lo hi xs \<le> SPEC(\<lambda>(xs', p). mset xs = mset xs' \<and>
      lo \<le> p \<and> p \<le> hi \<and> isPartition_map R h xs' lo hi p \<and> (\<forall> i. i<lo \<longrightarrow> xs'!i=xs!i) \<and> (\<forall> i. hi<i\<and>i<length xs' \<longrightarrow> xs'!i=xs!i))\<close>
 proof -
   have K: \<open>b \<le> hi - Suc n \<Longrightarrow> n > 0 \<Longrightarrow> Suc n \<le> hi \<Longrightarrow> Suc b \<le> hi - n\<close> for b hi n
     by auto
   have L: \<open>~ R (h x) (h y) \<Longrightarrow> R (h y) (h x)\<close> for x y \<comment> \<open>Corollary of linearity\<close>
     using assms by blast
   have M: \<open>a < Suc b \<equiv> a = b \<or> a < b\<close> for a b
     by linarith
   have N: \<open>(a::nat) \<le> b \<equiv> a = b \<or> a < b\<close> for a b
     by arith
 
   show ?thesis
     unfolding partition_main_def choose_pivot_def
     apply (refine_vcg WHILEIT_rule[where R = \<open>measure(\<lambda>(i,j,xs). hi-j)\<close>])
     subgoal using assms by blast \<comment> \<open>We feed our assumption to the assertion\<close>
     subgoal by auto \<comment> \<open>WF\<close>
     subgoal \<comment> \<open>Invariant holds before the first iteration\<close>
       unfolding partition_main_inv_def
       using assms apply simp by linarith
     subgoal unfolding partition_main_inv_def by simp
     subgoal unfolding partition_main_inv_def by simp
     subgoal
       unfolding partition_main_inv_def
       apply (auto dest: mset_eq_length)
       done
     subgoal unfolding partition_main_inv_def by (auto dest: mset_eq_length)
     subgoal
       unfolding partition_main_inv_def apply (auto dest: mset_eq_length)
       by (metis L M mset_eq_length nat_le_eq_or_lt)
 
     subgoal unfolding partition_main_inv_def by simp \<comment> \<open>assertions, etc\<close>
     subgoal unfolding partition_main_inv_def by simp
     subgoal unfolding partition_main_inv_def by (auto dest: mset_eq_length)
     subgoal unfolding partition_main_inv_def by simp
     subgoal unfolding partition_main_inv_def by (auto dest: mset_eq_length)
     subgoal unfolding partition_main_inv_def by (auto dest: mset_eq_length)
     subgoal unfolding partition_main_inv_def by (auto dest: mset_eq_length)
     subgoal unfolding partition_main_inv_def by simp
     subgoal unfolding partition_main_inv_def by simp
 
     subgoal \<comment> \<open>After the last iteration, we have a partitioning! :-)\<close>
       unfolding partition_main_inv_def by (auto simp add: isPartition_wrt_def)
     subgoal \<comment> \<open>And the lower out-of-bounds parts of the list haven't been changed\<close>
       unfolding partition_main_inv_def by auto
     subgoal \<comment> \<open>And the upper out-of-bounds parts of the list haven't been changed\<close>
       unfolding partition_main_inv_def by auto
     done
 qed
 
 
 definition partition_between :: \<open>('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> ('a list \<times> nat) nres\<close> where
   \<open>partition_between R h lo hi xs0 = do {
     ASSERT(hi < length xs0 \<and> lo \<le> hi);
     k \<leftarrow> choose_pivot R h xs0 lo hi; \<comment> \<open>choice of pivot\<close>
     ASSERT(k < length xs0);
     xs \<leftarrow> RETURN (swap xs0 k hi); \<comment> \<open>move the pivot to the last position, before we start the actual loop\<close>
     ASSERT(length xs = length xs0);
     partition_main R h lo hi xs
   }\<close>
 
 
 lemma partition_between_correct:
   assumes \<open>hi < length xs\<close> and \<open>lo \<le> hi\<close> and
   \<open>\<And> x y z. \<lbrakk>R (h x) (h y); R (h y) (h z)\<rbrakk> \<Longrightarrow> R (h x) (h z)\<close> and \<open>\<And>x y. R (h x) (h y) \<or> R (h y) (h x)\<close>
   shows \<open>partition_between R h lo hi xs \<le> SPEC(uncurry (partition_spec R h xs lo hi))\<close>
 proof -
   have K: \<open>b \<le> hi - Suc n \<Longrightarrow> n > 0 \<Longrightarrow> Suc n \<le> hi \<Longrightarrow> Suc b \<le> hi - n\<close> for b hi n
     by auto
   show ?thesis
     unfolding partition_between_def choose_pivot_def
     apply (refine_vcg partition_main_correct)
     using assms apply (auto dest: mset_eq_length simp add: partition_spec_def)
     by (metis dual_order.strict_trans2 less_imp_not_eq2 mset_eq_length swap_nth)
 qed
 
 
 
 text \<open>We use the median of the first, the middle, and the last element.\<close>
 definition choose_pivot3 where
   \<open>choose_pivot3 R h xs lo (hi::nat) = do {
     ASSERT(lo < length xs);
     ASSERT(hi < length xs);
     let k' = (hi - lo) div 2;
     let k = lo + k';
     ASSERT(k < length xs);
     let start = h (xs ! lo);
     let mid = h (xs ! k);
     let end = h (xs ! hi);
     if (R start mid \<and> R mid end) \<or> (R end mid \<and> R mid start) then RETURN k
     else if (R start end \<and> R end mid) \<or> (R mid end \<and> R end start) then RETURN hi
     else RETURN lo
 }\<close>
 
 \<comment> \<open>We only have to show that this procedure yields a valid index between \<open>lo\<close> and \<open>hi\<close>.\<close>
 lemma choose_pivot3_choose_pivot:
   assumes \<open>lo < length xs\<close> \<open>hi < length xs\<close> \<open>hi \<ge> lo\<close>
   shows \<open>choose_pivot3 R h xs lo hi \<le> \<Down> Id (choose_pivot R h xs lo hi)\<close>
   unfolding choose_pivot3_def choose_pivot_def
   using assms by (auto intro!: ASSERT_leI simp: Let_def)
 
 text \<open>The refined partion function: We use the above pivot function and fold instead of non-deterministic iteration.\<close>
 definition partition_between_ref
   :: \<open>('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> ('a list \<times> nat) nres\<close>
 where
   \<open>partition_between_ref R h lo hi xs0 = do {
     ASSERT(hi < length xs0 \<and> hi < length xs0 \<and> lo \<le> hi);
     k \<leftarrow> choose_pivot3 R h xs0 lo hi; \<comment> \<open>choice of pivot\<close>
     ASSERT(k < length xs0);
     xs \<leftarrow> RETURN (swap xs0 k hi); \<comment> \<open>move the pivot to the last position, before we start the actual loop\<close>
     ASSERT(length xs = length xs0);
     partition_main R h lo hi xs
   }\<close>
 
 
 lemma partition_main_ref':
   \<open>partition_main R h lo hi xs
     \<le> \<Down> ((\<lambda> a b c d. Id) a b c d) (partition_main R h lo hi xs)\<close>
   by auto
 
 
 (*TODO already exists somewhere*)
 lemma Down_id_eq:
   \<open>\<Down>Id x = x\<close>
   by auto
 
 lemma partition_between_ref_partition_between:
   \<open>partition_between_ref R h lo hi xs \<le> (partition_between R h lo hi xs)\<close>
 proof -
   have swap: \<open>(swap xs k hi, swap xs ka hi) \<in> Id\<close> if \<open>k = ka\<close>
     for k ka
     using that by auto
   have [refine0]: \<open>(h (xsa ! hi), h (xsaa ! hi)) \<in> Id\<close>
     if \<open>(xsa, xsaa) \<in> Id\<close>
     for xsa xsaa
     using that by auto
 
   show ?thesis
     apply (subst (2) Down_id_eq[symmetric])
     unfolding partition_between_ref_def
       partition_between_def
       OP_def
     apply (refine_vcg choose_pivot3_choose_pivot swap partition_main_correct)
     subgoal by auto
     subgoal by auto
     subgoal by auto
     subgoal by auto
     subgoal by auto
     subgoal by auto
     subgoal by auto
     subgoal by auto
     subgoal by auto
     by (auto intro: Refine_Basic.Id_refine dest: mset_eq_length)
 qed
 
 text \<open>Technical lemma for sepref\<close>
 
 lemma partition_between_ref_partition_between':
   \<open>(uncurry2 (partition_between_ref R h), uncurry2 (partition_between R h)) \<in>
     (nat_rel \<times>\<^sub>r nat_rel) \<times>\<^sub>r \<langle>Id\<rangle>list_rel \<rightarrow>\<^sub>f \<langle>\<langle>Id\<rangle>list_rel \<times>\<^sub>r nat_rel\<rangle>nres_rel\<close>
   by (intro frefI nres_relI)
     (auto intro: partition_between_ref_partition_between)
 
 text \<open>Example instantiation for pivot\<close>
 definition choose_pivot3_impl where
   \<open>choose_pivot3_impl = choose_pivot3 (\<le>) id\<close>
 
 
 lemma partition_between_ref_correct:
   assumes trans: \<open>\<And> x y z. \<lbrakk>R (h x) (h y); R (h y) (h z)\<rbrakk> \<Longrightarrow> R (h x) (h z)\<close> and lin: \<open>\<And>x y. R (h x) (h y) \<or> R (h y) (h x)\<close>
     and bounds: \<open>hi < length xs\<close> \<open>lo \<le> hi\<close>
   shows \<open>partition_between_ref R h lo hi xs \<le> SPEC (uncurry (partition_spec R h xs lo hi))\<close>
 proof -
   show ?thesis
     apply (rule partition_between_ref_partition_between[THEN order_trans])
     using bounds apply (rule partition_between_correct[where h=h])
     subgoal by (rule trans)
     subgoal by (rule lin)
     done
 qed
 
 
 text \<open>Refined quicksort algorithm: We use the refined partition function.\<close>
 definition quicksort_ref :: \<open>_ \<Rightarrow> _ \<Rightarrow> nat \<times> nat \<times> 'a list \<Rightarrow> 'a list nres\<close> where
 \<open>quicksort_ref R h = (\<lambda>(lo,hi,xs0).
   do {
   RECT (\<lambda>f (lo,hi,xs). do {
       ASSERT(lo \<le> hi \<and> hi < length xs0 \<and> mset xs = mset xs0);
       (xs, p) \<leftarrow> partition_between_ref R h lo hi xs; \<comment> \<open>This is the refined partition function. Note that we need the premises (trans,lin,bounds) here.\<close>
       ASSERT(mset xs = mset xs0 \<and> p \<ge> lo \<and> p < length xs0);
       xs \<leftarrow> (if p-1\<le>lo then RETURN xs else f (lo, p-1, xs));
       ASSERT(mset xs = mset xs0);
       if hi\<le>p+1 then RETURN xs else f (p+1, hi, xs)
     }) (lo,hi,xs0)
   })\<close>
 
 
 (*TODO share*)
 lemma fref_to_Down_curry2:
   \<open>(uncurry2 f, uncurry2 g) \<in> [P]\<^sub>f A \<rightarrow> \<langle>B\<rangle>nres_rel \<Longrightarrow>
      (\<And>x x' y y' z z'. P ((x', y'), z') \<Longrightarrow> (((x, y), z), ((x', y'), z')) \<in> A\<Longrightarrow>
          f x y z \<le> \<Down> B (g x' y' z'))\<close>
   unfolding fref_def uncurry_def nres_rel_def
   by auto
 
 lemma fref_to_Down_curry:
   \<open>(f, g) \<in> [P]\<^sub>f A \<rightarrow> \<langle>B\<rangle>nres_rel \<Longrightarrow>
      (\<And>x x' . P x' \<Longrightarrow> (x, x') \<in> A\<Longrightarrow>
          f x  \<le> \<Down> B (g x'))\<close>
   unfolding fref_def uncurry_def nres_rel_def
   by auto
 
 
 
 lemma quicksort_ref_quicksort:
   assumes bounds: \<open>hi < length xs\<close> \<open>lo \<le> hi\<close> and
     trans: \<open>\<And> x y z. \<lbrakk>R (h x) (h y); R (h y) (h z)\<rbrakk> \<Longrightarrow> R (h x) (h z)\<close> and lin: \<open>\<And>x y. R (h x) (h y) \<or> R (h y) (h x)\<close>
   shows \<open>quicksort_ref R h x0 \<le> \<Down> Id (quicksort R h x0)\<close>
 proof -
   have wf: \<open>wf (measure (\<lambda>(lo, hi, xs). Suc hi - lo))\<close>
     by auto
   have pre: \<open>x0 = x0' \<Longrightarrow> (x0, x0') \<in> Id \<times>\<^sub>r Id \<times>\<^sub>r \<langle>Id\<rangle>list_rel\<close> for x0 x0' :: \<open>nat \<times> nat \<times> 'b list\<close>
     by auto
   have [refine0]: \<open>(x1e = x1d) \<Longrightarrow> (x1e,x1d) \<in> Id\<close> for x1e x1d :: \<open>'b list\<close>
     by auto
 
   show ?thesis
     unfolding quicksort_def quicksort_ref_def
     apply (refine_vcg pre partition_between_ref_partition_between'[THEN fref_to_Down_curry2])
 
     text \<open>First assertion (premise for partition)\<close>
     subgoal
       by auto
     text \<open>First assertion (premise for partition)\<close>
     subgoal
       by auto
     subgoal
       by (auto dest: mset_eq_length)
     subgoal
       by (auto dest: mset_eq_length mset_eq_setD)
 
     text \<open>Correctness of the concrete partition function\<close>
     subgoal
       apply (simp, rule partition_between_ref_correct)
       subgoal by (rule trans)
       subgoal by (rule lin)
       subgoal by auto \<comment> \<open>first premise\<close>
       subgoal by auto \<comment> \<open>second premise\<close>
       done
     subgoal
       by (auto dest: mset_eq_length mset_eq_setD)
     subgoal by (auto simp: partition_spec_def isPartition_wrt_def)
     subgoal by (auto simp: partition_spec_def isPartition_wrt_def dest: mset_eq_length)
     subgoal
       by (auto dest: mset_eq_length mset_eq_setD)
     subgoal
       by (auto dest: mset_eq_length mset_eq_setD)
     subgoal
       by (auto dest: mset_eq_length mset_eq_setD)
     subgoal
       by (auto dest: mset_eq_length mset_eq_setD)
 
     by simp+
 qed
 
 \<comment> \<open>Sort the entire list\<close>
 definition full_quicksort where
   \<open>full_quicksort R h xs \<equiv> if xs = [] then RETURN xs else quicksort R h (0, length xs - 1, xs)\<close>
 
 definition full_quicksort_ref where
   \<open>full_quicksort_ref R h xs \<equiv>
     if List.null xs then RETURN xs
     else quicksort_ref R h (0, length xs - 1, xs)\<close>
 
 definition full_quicksort_impl :: \<open>nat list \<Rightarrow> nat list nres\<close> where
   \<open>full_quicksort_impl xs = full_quicksort_ref (\<le>) id xs\<close>
 
 lemma full_quicksort_ref_full_quicksort:
   assumes trans: \<open>\<And> x y z. \<lbrakk>R (h x) (h y); R (h y) (h z)\<rbrakk> \<Longrightarrow> R (h x) (h z)\<close> and lin: \<open>\<And>x y. R (h x) (h y) \<or> R (h y) (h x)\<close>
   shows \<open>(full_quicksort_ref R h, full_quicksort R h) \<in>
           \<langle>Id\<rangle>list_rel \<rightarrow>\<^sub>f \<langle> \<langle>Id\<rangle>list_rel\<rangle>nres_rel\<close>
 proof -
   show ?thesis
     unfolding full_quicksort_ref_def full_quicksort_def
     apply (intro frefI nres_relI)
     apply (auto intro!: quicksort_ref_quicksort[unfolded Down_id_eq] simp: List.null_def)
     subgoal by (rule trans)
     subgoal using lin by blast
     done
 qed
 
 
 lemma sublist_entire:
   \<open>sublist xs 0 (length xs - 1) = xs\<close>
   by (simp add: sublist_def)
 
 
 lemma sorted_sublist_wrt_entire:
   assumes \<open>sorted_sublist_wrt R xs 0 (length xs - 1)\<close>
   shows \<open>sorted_wrt R xs\<close>
 proof -
   have \<open>sorted_wrt R (sublist xs 0 (length xs - 1))\<close>
     using assms by (simp add: sorted_sublist_wrt_def )
   then show ?thesis
     by (metis sublist_entire)
 qed
 
 lemma sorted_sublist_map_entire:
   assumes \<open>sorted_sublist_map R h xs 0 (length xs - 1)\<close>
   shows \<open>sorted_wrt (\<lambda> x y. R (h x) (h y)) xs\<close>
 proof -
   show ?thesis
     using assms by (rule sorted_sublist_wrt_entire)
 qed
 
 
 text \<open>Final correctness lemma\<close>
 theorem full_quicksort_correct_sorted:
   assumes
     trans: \<open>\<And>x y z. \<lbrakk>R (h x) (h y); R (h y) (h z)\<rbrakk> \<Longrightarrow> R (h x) (h z)\<close> and lin: \<open>\<And>x y. x \<noteq> y \<Longrightarrow> R (h x) (h y) \<or> R (h y) (h x)\<close>
   shows \<open>full_quicksort R h xs \<le> \<Down> Id (SPEC(\<lambda>xs'. mset xs' = mset xs \<and> sorted_wrt (\<lambda> x y. R (h x) (h y)) xs'))\<close>
 proof -
   show ?thesis
     unfolding full_quicksort_def
     apply (refine_vcg)
     subgoal by simp \<comment> \<open>case xs=[]\<close>
     subgoal by simp \<comment> \<open>case xs=[]\<close>
 
     apply (rule quicksort_correct[THEN order_trans])
     subgoal by (rule trans)
     subgoal by (rule lin)
     subgoal by linarith
     subgoal by simp
 
     apply (simp add: Misc.subset_Collect_conv, intro allI impI conjI)
     subgoal
       by (auto simp add: quicksort_post_def)
     subgoal
       apply (rule sorted_sublist_map_entire)
       by (auto simp add: quicksort_post_def dest: mset_eq_length)
     done
 qed
 
 lemma full_quicksort_correct:
   assumes
     trans: \<open>\<And>x y z. \<lbrakk>R (h x) (h y); R (h y) (h z)\<rbrakk> \<Longrightarrow> R (h x) (h z)\<close> and
     lin: \<open>\<And>x y. R (h x) (h y) \<or> R (h y) (h x)\<close>
   shows \<open>full_quicksort R h xs \<le> \<Down> Id (SPEC(\<lambda>xs'. mset xs' = mset xs))\<close>
   by (rule order_trans[OF full_quicksort_correct_sorted])
     (use assms in auto)
 
 end