diff --git a/thys/Auto2_HOL/util_logic.ML b/thys/Auto2_HOL/util_logic.ML
--- a/thys/Auto2_HOL/util_logic.ML
+++ b/thys/Auto2_HOL/util_logic.ML
@@ -1,630 +1,630 @@
 (*
   File: util_logic.ML
   Author: Bohua Zhan
 
   Utility functions, after fixing object logic.
 *)
 
 signature BASIC_UTIL_LOGIC =
 sig
   (* Terms *)
   val Trueprop: term
   val is_Trueprop: term -> bool
   val mk_Trueprop: term -> term
   val dest_Trueprop: term -> term
   val Trueprop_conv: conv -> conv
   val pFalse: term
   val Not: term
   val mk_not: term -> term
   val dest_not: term -> term
   val is_neg: term -> bool
   val get_neg: term -> term
   val get_neg': term -> term
   val conj: term
   val is_conj: term -> bool
   val mk_conj: term * term -> term
   val strip_conj: term -> term list
   val list_conj: term list -> term
   val disj: term
   val is_disj: term -> bool
   val mk_disj: term * term -> term
   val strip_disj: term -> term list
   val list_disj: term list -> term
   val imp: term
   val is_imp: term -> bool
   val mk_imp: term * term -> term
   val dest_imp: term -> term * term
   val strip_obj_imp: term -> term list * term
   val list_obj_imp: term list * term -> term
   val is_obj_all: term -> bool
   val is_ball: term -> bool
   val mk_obj_all: term -> term -> term
   val is_ex: term -> bool
   val is_bex: term -> bool
   val mk_exists: term -> term -> term
   val is_mem: term -> bool
   val mk_mem: term * term -> term
 
   (* Theorems *)
   val is_true_th: thm -> bool
   val prop_of': thm -> term
   val cprop_of': thm -> cterm
   val concl_of': thm -> term
   val make_trueprop_eq: thm -> thm
   val assume_eq: theory -> term * term -> thm
   val apply_to_thm': conv -> thm -> thm
   val to_meta_eq: thm -> thm
   val to_obj_eq: thm -> thm
   val obj_sym: thm -> thm
   val rewr_obj_eq: thm -> conv
 
   val conj_left_th: thm -> thm
   val conj_right_th: thm -> thm
   val equiv_forward_th: thm -> thm
   val equiv_backward_th: thm -> thm
   val inv_backward_th: thm -> thm
   val to_obj_eq_th: thm -> thm
   val to_obj_eq_iff_th: thm -> thm
   val obj_sym_th: thm -> thm
 end;
 
 signature UTIL_LOGIC =
 sig
   include BASIC_UTIL_LOGIC
 
   (* Terms *)
   val term_of_bool: bool -> term
   val bool_of_term: term -> bool
 
   (* Finding subterms *)
   val list_subterms: term -> term list
   val get_all_subterms: term -> term list
   val get_all_subterms_skip_if: term -> term list
 
   (* cterms *)
   val get_cneg: cterm -> cterm
 
   (* Theorems *)
   val make_neg_eq: thm -> thm
   val rewrite_to_contra_form: conv
   val rewrite_from_contra_form: conv
   val to_obj_conv: Proof.context -> conv
   val to_obj_conv_on_horn: Proof.context -> conv
   val to_meta_conv: Proof.context -> conv
   val split_conj_th: thm -> thm list
   val split_conj_gen_th: thm -> thm list
   val split_not_disj_th: thm -> thm list
   val strip_horn': thm -> term list * term
   val mk_conjs_th: thm list -> thm
   val ex_elim: Proof.context -> term -> thm -> thm
   val force_abs_form: term -> term
   val strip_obj_horn: term -> term list * (term list * term)
   val list_obj_horn: term list * (term list * term) -> term
   val is_ex_form_gen: term -> bool
   val normalize_exists: Proof.context -> conv
   val strip_exists: term -> term list * term
 
   (* Wrapper around common tactics. *)
   val prove_by_tac: (Proof.context -> int -> tactic) -> Proof.context ->
                     thm list -> term -> thm
   val contra_by_tac: (Proof.context -> int -> tactic) -> Proof.context ->
                      thm list -> thm
 end;
 
 structure UtilLogic : UTIL_LOGIC =
 struct
 
 (* Booleans *)
 
 fun term_of_bool b = (if b then bTrue else bFalse)
 
 fun bool_of_term t =
     if t aconv bTrue then true
     else if t aconv bFalse then false
     else raise Fail "bool_of_term: unexpected t."
 
 (* Trueprop *)
 
 val Trueprop = Const (UtilBase.Trueprop_name, boolT --> propT)
 
 (* Returns whether the given term is Trueprop. *)
 fun is_Trueprop t =
     let
       val _ = assert (fastype_of t = propT) "is_Trueprop: wrong type"
     in
       case t of Const (c, _) $ _ => c = UtilBase.Trueprop_name
               | _ => false
     end
 
 fun mk_Trueprop P = Trueprop $ P
 
 fun dest_Trueprop t =
     if is_Trueprop t then dest_arg t else raise Fail "dest_Trueprop"
 
 fun Trueprop_conv cv ct =
     if is_Trueprop (Thm.term_of ct) then Conv.arg_conv cv ct
     else raise CTERM ("Trueprop_conv", [ct])
 
 val pFalse = Trueprop $ bFalse
 
 (* Not *)
 
 val Not = Const (UtilBase.Not_name, boolT --> boolT)
 
 fun mk_not P = Not $ P
 
 (* Returns whether the given term is in neg form. *)
 fun is_neg t =
     let
       val _ = assert (fastype_of t = boolT) "is_neg: wrong type"
     in
       case t of
           Const (c, _) $ _ => c = UtilBase.Not_name
         | _ => false
     end
 
 fun dest_not t =
     if is_neg t then dest_arg t else raise Fail "dest_not"
 
 (* Returns the negation of the given term. Avoids double negatives. *)
 fun get_neg t =
     if is_neg t then dest_not t else Not $ t
 
 (* Version of get_neg for Trueprop terms. *)
 fun get_neg' t =
     let
       val _ = assert (is_Trueprop t) "get_neg': input should be a Trueprop."
     in
       t |> dest_Trueprop |> get_neg |> mk_Trueprop
     end
 
 (* Conjunction and disjunction *)
 
 val conj = Const (UtilBase.Conj_name, boolT --> boolT --> boolT)
 
 fun is_conj t =
     case t of Const (c, _) $ _ $ _ => c = UtilBase.Conj_name | _ => false
 
 fun mk_conj (t, u) = conj $ t $ u
 
 fun strip_conj t =
     if is_conj t then (dest_arg1 t) :: strip_conj (dest_arg t) else [t]
 
 fun list_conj ts =
     case ts of
         [] => error "list_conj"
       | [t] => t
       | t :: rest => mk_conj (t, list_conj rest)
 
 val disj = Const (UtilBase.Disj_name, boolT --> boolT --> boolT)
 
 fun is_disj t =
     case t of Const (c, _) $ _ $ _ => c = UtilBase.Disj_name | _ => false
 
 fun mk_disj (t, u) = disj $ t $ u
 
 fun strip_disj t =
     if is_disj t then (dest_arg1 t) :: strip_disj (dest_arg t) else [t]
 
 fun list_disj ts =
     case ts of
         [] => raise Fail "list_disj"
       | [t] => t
       | t :: ts' => mk_disj (t, list_disj ts')
 
 (* Object implication *)
 
 val imp = Const (UtilBase.Imp_name, boolT --> boolT --> boolT)
 
 fun is_imp t =
     case t of Const (c, _) $ _ $ _ => c = UtilBase.Imp_name | _ => false
 
 fun mk_imp (t, u) = imp $ t $ u
 
 fun dest_imp t =
     if is_imp t then (dest_arg1 t, dest_arg t) else raise Fail "dest_imp"
 
 (* Given t of form A1 --> ... --> An, return ([A1, ..., A(n-1)], An). *)
 fun strip_obj_imp t =
     if is_imp t then
       let val (As, B') = strip_obj_imp (dest_arg t) in (dest_arg1 t :: As, B') end
     else ([], t)
 
 fun list_obj_imp (As, C) =
     case As of
         [] => C
       | A :: rest => mk_imp (A, list_obj_imp (rest, C))
 
 fun is_obj_all t =
     case t of
         Const (c, _) $ Abs _ => c = UtilBase.All_name | _ => false
 
 fun is_ball t =
     case t of
         Const (c, _) $ _ $ _ => c = UtilBase.Ball_name | _ => false
 
 fun mk_obj_all t body =
     let
       val (x, T) = Term.dest_Free t
     in
       Const (UtilBase.All_name, (T --> boolT) --> boolT) $ Term.absfree (x, T) body
     end
 
 fun is_ex t =
     case t of Const (c, _) $ Abs _ => c = UtilBase.Ex_name | _ => false
 
 fun is_bex t =
     case t of Const (c, _) $ _ $ _ => c = UtilBase.Bex_name | _ => false
 
 fun mk_exists t body =
     let
       val (x, T) = Term.dest_Free t
     in
       Const (UtilBase.Ex_name, (T --> boolT) --> boolT) $ Term.absfree (x, T) body
     end
 
 fun is_mem t =
     case t of Const (c, _) $ _ $ _ => c = UtilBase.Mem_name | _ => false
 
 fun mk_mem (x, A) =
     let
       val T = fastype_of x
     in
       Const (UtilBase.Mem_name, T --> UtilBase.mk_setT T --> boolT) $ x $ A
     end
 
 (* Finding subterms *)
 
 (* Get all subterms of t. *)
 fun list_subterms t =
     let
       fun dest_at_head t =
           case t of
               Abs (_, _, body) => dest_at_head body
             | _ => if Term.is_open t then
                      t |> Term.strip_comb |> snd |> maps dest_at_head
                    else [t]
 
       and dest t =
           case t of
               Abs _ => dest_at_head t
             | _ $ _ => t |> Term.strip_comb |> snd
             | _ => []
     in
       dest t
     end
 
 (* List all (closed) subterms. Larger ones will be listed first. *)
 fun get_all_subterms t =
     t |> list_subterms |> maps get_all_subterms |> distinct (op aconv)
       |> cons t
 
 (* List all (closed) subterms. For terms of form if cond then yes or
    no, list only subterms of cond.
  *)
 fun get_all_subterms_skip_if t =
     if UtilBase.is_if t then
       t |> Util.dest_args |> hd |> get_all_subterms_skip_if |> cons t
     else
       t |> list_subterms |> maps get_all_subterms_skip_if
         |> distinct (op aconv) |> cons t
 
 (* cterms *)
 
 fun get_cneg ct =
     let
       val t = Thm.term_of ct
       val _ = assert (fastype_of t = boolT) "get_neg: wrong type"
     in
       if is_neg t then Thm.dest_arg ct else Thm.apply UtilBase.cNot ct
     end
 
 (* Theorems *)
 
 fun is_true_th th = Thm.eq_thm_prop (th, true_th)
 fun prop_of' th = dest_Trueprop (Thm.prop_of th)
 fun cprop_of' th = Thm.dest_arg (Thm.cprop_of th)
 fun concl_of' th = dest_Trueprop (Thm.concl_of th)
 
 (* Given an equality between bools, make it an equality between props,
    by applying the function Trueprop to both sides.
  *)
 fun make_trueprop_eq th =
     Thm.combination (Thm.reflexive UtilBase.cTrueprop) th
 
 (* Assumed theorems. *)
 fun assume_eq thy (t1, t2) =
     Thm.assume (Thm.global_cterm_of thy (mk_Trueprop (mk_eq (t1, t2))))
 
 (* Apply cv to the statement of th, skipping Trueprop. *)
 fun apply_to_thm' cv th = apply_to_thm (Trueprop_conv cv) th
 
 val to_meta_eq = apply_to_thm (Util.concl_conv UtilBase.to_meta_eq_cv)
 
 val to_obj_eq = apply_to_thm (Util.concl_conv UtilBase.to_obj_eq_cv)
 
 val obj_sym = apply_to_thm (Util.concl_conv UtilBase.obj_sym_cv)
 
 (* Obtain rewriting conv from obj equality. *)
 fun rewr_obj_eq eq_th = Conv.rewr_conv (to_meta_eq eq_th)
 
 (* Given an equality A == B, make the equality ~A == ~B. Cancel ~~ on
    both sides if exists.
  *)
 fun make_neg_eq th =
     th |> Thm.combination (Thm.reflexive UtilBase.cNot)
        |> apply_to_lhs (Conv.try_conv (rewr_obj_eq UtilBase.nn_cancel_th))
        |> apply_to_rhs (Conv.try_conv (rewr_obj_eq UtilBase.nn_cancel_th))
 
 (* If ct is of the form [...] ==> False, leave it unchanged.
    Otherwise, change [...] ==> B to [..., ~ B] ==> False and change
    [...] ==> ~ B to [..., B] ==> False.
  *)
 fun rewrite_to_contra_form ct =
     let
       val (_, concl) = Logic.strip_horn (Thm.term_of ct)
       val concl' = dest_Trueprop concl
     in
       if concl' aconv bFalse then
         Conv.all_conv ct
       else if is_neg concl' then
         Util.concl_conv (Conv.rewr_conv UtilBase.to_contra_form_th') ct
       else
         Util.concl_conv (Conv.rewr_conv UtilBase.to_contra_form_th) ct
     end
 
 (* Rewrite ct from [...] ==> A ==> False to [...] ==> ~ A and from
    [...] ==> ~ A ==> False to [...] ==> A.
  *)
 fun rewrite_from_contra_form ct =
     let
       val (prems, concl) = Logic.strip_horn (Thm.term_of ct)
       val _ = assert (concl aconv pFalse)
                      "rewrite_from_contra_form: concl should be false."
       val num_prems = length prems
       val last_prem' = dest_Trueprop (nth prems (num_prems-1))
       val to_contra_form = if is_neg last_prem' then UtilBase.to_contra_form_th
                            else UtilBase.to_contra_form_th'
     in
       Util.concl_conv_n (num_prems-1)
                         (Conv.rewr_conv (meta_sym to_contra_form)) ct
     end
 
 (* Converts ==> to --> and !! to !. *)
 fun to_obj_conv ctxt ct =
     case Thm.term_of ct of
         @{const Pure.imp} $ _ $ _ =>
         Conv.every_conv [Conv.binop_conv (to_obj_conv ctxt),
                          Conv.rewr_conv UtilBase.atomize_imp_th] ct
       | Const (@{const_name Pure.all}, _) $ Abs _ =>
         Conv.every_conv [Conv.binder_conv (to_obj_conv o snd) ctxt,
                          Conv.rewr_conv UtilBase.atomize_all_th] ct
       | _ => Conv.all_conv ct
 
 (* When ct is of form A1 ==> ... ==> An, apply to_obj_conv to each Ai. *)
 fun to_obj_conv_on_horn ctxt ct =
     case Thm.term_of ct of
         @{const Pure.imp} $ _ $ _ =>
         Conv.every_conv [Conv.arg1_conv (to_obj_conv ctxt),
                          Conv.arg_conv (to_obj_conv_on_horn ctxt)] ct
       | Const (@{const_name Pure.all}, _) $ Abs _ =>
         Conv.binder_conv (to_obj_conv_on_horn o snd) ctxt ct
       | _ => Conv.all_conv ct
 
 (* Convert !! and ==> on the outermost level. Pull all !! to the front. *)
 fun to_meta_conv ctxt ct =
     let
       val t = Thm.term_of ct
     in
       if is_Trueprop t andalso is_obj_all (dest_Trueprop t) then
         Conv.every_conv [Conv.rewr_conv (meta_sym UtilBase.atomize_all_th),
                          to_meta_conv ctxt] ct
       else if is_Trueprop t andalso is_ball (dest_Trueprop t) then
         Conv.every_conv [Conv.arg_conv (rewr_obj_eq UtilBase.Ball_def_th),
                          to_meta_conv ctxt] ct
       else if is_Trueprop t andalso is_imp (dest_Trueprop t) then
         Conv.every_conv [Conv.rewr_conv (meta_sym UtilBase.atomize_imp_th),
                          to_meta_conv ctxt] ct
       else if Logic.is_all t then
         Conv.binder_conv (to_meta_conv o snd) ctxt ct
       else if Util.is_implies t then
         Conv.every_conv [Conv.arg_conv (to_meta_conv ctxt),
                          Util.swap_meta_imp_alls ctxt] ct
       else
         Conv.all_conv ct
     end
 
 (* Modify th using imp_th, and add postfix to name (if available). *)
 fun thm_RS_mod imp_th suffix th =
     (th RS imp_th) |> Drule.zero_var_indexes
                    |> Util.update_name_of_thm th suffix
 
 (* From A & B, obtain A. *)
 val conj_left_th = thm_RS_mod UtilBase.conjunct1_th "@left"
 (* From A & B, obtain B. *)
 val conj_right_th = thm_RS_mod UtilBase.conjunct2_th "@right"
 (* From (A::bool) = B, obtain A ==> B. *)
 val equiv_forward_th = thm_RS_mod UtilBase.iffD1_th "@eqforward"
 (* From (A::bool) = B, obtain B ==> A. *)
 val equiv_backward_th = thm_RS_mod UtilBase.iffD2_th "@eqbackward"
 (* From (A::bool) = B, obtain ~A ==> ~B. *)
 val inv_backward_th = thm_RS_mod UtilBase.inv_back_th "@invbackward"
 (* Same as to_obj_eq, except keeping names and indices. *)
 fun to_obj_eq_th th = th |> to_obj_eq |> Util.update_name_of_thm th "@obj_eq"
 (* Same as to_obj_eq_iff, except keeping names and indices. *)
 fun to_obj_eq_iff_th th = th |> UtilBase.to_obj_eq_iff |> Util.update_name_of_thm th "@iff"
 (* Same as obj_sym, except keeping names and indices. *)
 fun obj_sym_th th = th |> obj_sym |> Util.update_name_of_thm th "@sym"
 
 (* Given th of form (P ==>) A1 & ... & An, return theorems (P ==>) A1,
    ..., (P ==>) An, where there can be zero or more premises in front.
  *)
 fun split_conj_th th =
     if is_conj (prop_of' th) then
       (th RS UtilBase.conjunct1_th) :: (split_conj_th (th RS UtilBase.conjunct2_th))
     else [th]
 
 (* More general form. *)
 fun split_conj_gen_th th =
     if is_conj (prop_of' th) then
       maps split_conj_gen_th [th RS UtilBase.conjunct1_th,
                               th RS UtilBase.conjunct2_th]
     else [th]
 
 (* Given th of form ~ (A1 | ... | An), return theorems ~ A1, ... ~ An. *)
 fun split_not_disj_th th =
     let
       val t = prop_of' th
     in
       if is_neg t andalso is_disj (dest_not t) then
         (th RS UtilBase.or_intro1_th) :: (split_not_disj_th (th RS UtilBase.or_intro2_th))
       else [th]
     end
 
 (* Similar to Logic.strip_horn, except remove Trueprop. *)
 fun strip_horn' th = (Logic.strip_horn (Thm.prop_of th))
                          |> apfst (map dest_Trueprop)
                          |> apsnd dest_Trueprop
 
 fun mk_conjs_th ths =
     case ths of
         [] => raise Fail "mk_conjs_th"
       | [th] => th
       | th :: rest => [th, mk_conjs_th rest] MRS UtilBase.conjI_th
 
 (* Given th of form P x ==> False, where x is the given free variable,
    obtain new theorem of form (EX x. P x) ==> False. The function is
    written so it can be applied to multiple variables with fold. For
    example, "fold (ex_elim ctxt) [x, y] (P x y ==> False) will give
    (EX y x. P x y) ==> False.
  *)
 fun ex_elim ctxt freevar th =
     let
       val thy = Proof_Context.theory_of ctxt
       val th' = th |> Thm.forall_intr (Thm.cterm_of ctxt freevar)
       val head_prem = hd (Thm.prems_of UtilBase.exE_th')
       val inst = Pattern.match thy (head_prem, Thm.prop_of th') fo_init
       val exE_inst = Util.subst_thm ctxt inst UtilBase.exE_th'
     in
       Thm.elim_implies th' exE_inst
     end
 
 fun force_abs_form t =
     case t of
         Abs _ => t
       | _ => Abs ("x", domain_type (fastype_of t), t $ Bound 0)
 
 (* Normalization of object forall expressions in horn-clause form. *)
 fun strip_obj_horn t =
     if is_obj_all t then
       case t of
           _ $ Abs (abs as (_, T, _)) =>
           let
             val (x, body) = Term.dest_abs abs
             val var = Free (x, T)
             val (vars, (assum, concl)) = strip_obj_horn body
           in
             (var :: vars, (assum, concl))
           end
         | f $ arg => strip_obj_horn (f $ force_abs_form arg)
         | _ => raise Fail "strip_obj_horn"
     else if is_ball t then
       case t of
           _ $ S $ Abs (abs as (_, T, _)) =>
           let
             val (x, body) = Term.dest_abs abs
             val var = Free (x, T)
             val mem = mk_mem (var, S)
             val (vars, (assum, concl)) = strip_obj_horn body
           in
             (var :: vars, (mem :: assum, concl))
           end
         | f $ S $ arg => strip_obj_horn (f $ S $ force_abs_form arg)
         | _ => raise Fail "strip_obj_horn"
     else if is_imp t then
       let
         val (vars, (assum, concl)) = strip_obj_horn (dest_arg t)
       in
         (vars, (dest_arg1 t :: assum, concl))
       end
     else
       ([], ([], t))
 
 fun list_obj_horn (vars, (As, B)) =
     (list_obj_imp (As, B)) |> fold mk_obj_all (rev vars)
 
 (* Whether t can be immediately rewritten into EX form. *)
 fun is_ex_form_gen t =
     is_ex t orelse is_bex t orelse
     (is_neg t andalso is_obj_all (dest_not t)) orelse
     (is_neg t andalso is_ball (dest_not t)) orelse
     (is_conj t andalso is_ex_form_gen (dest_arg t))
 
 (* Rewrite A & EX v_i. B to EX v_i. A & B. *)
 fun swap_conj_exists ctxt ct =
     let
       val t = Thm.term_of ct
     in
       if is_conj t andalso is_ex (dest_arg t) then
         Conv.every_conv [rewr_obj_eq UtilBase.swap_ex_conj_th,
                          Conv.binder_conv (swap_conj_exists o snd) ctxt] ct
       else
         Conv.all_conv ct
     end
 
 (* Normalize existence statement into EX v_i. A_1 & ... & A_n. This
    includes moving as many existence quantifiers to the left as
    possible.
  *)
 fun normalize_exists ctxt ct =
     let
       val t = Thm.term_of ct
     in
       if is_ex t then
         Conv.binder_conv (normalize_exists o snd) ctxt ct
       else if is_bex t then
         Conv.every_conv [rewr_obj_eq UtilBase.Bex_def_th, normalize_exists ctxt] ct
       else if is_neg t andalso is_obj_all (dest_not t) then
         Conv.every_conv [rewr_obj_eq UtilBase.not_all_th, normalize_exists ctxt] ct
       else if is_neg t andalso is_ball (dest_not t) then
         Conv.every_conv [Conv.arg_conv (rewr_obj_eq UtilBase.Ball_def_th),
                          rewr_obj_eq UtilBase.not_all_th,
                          Conv.binder_conv (K (rewr_obj_eq UtilBase.not_imp_th)) ctxt,
                          normalize_exists ctxt] ct
       else if is_conj t then
         Conv.every_conv [Conv.arg_conv (normalize_exists ctxt),
                          swap_conj_exists ctxt] ct
       else
         Conv.all_conv ct
     end
 
 (* Assume t is in normal form. *)
 fun strip_exists t =
     if is_ex t then
       case t of
           _ $ Abs (abs as (_, T, _)) =>
           let
             val (x, body) = Term.dest_abs abs
             val var = Free (x, T)
             val (vars, body') = strip_exists body
           in
             (var :: vars, body')
           end
         | _ => raise Fail "strip_exists"
     else
       ([], t)
 
 (* Generic wrapper function. tac can be arith_tac, simp_tac, etc. *)
 fun prove_by_tac tac ctxt ths goal =
     let
       val goal' = Logic.list_implies (map Thm.prop_of ths, mk_Trueprop goal)
     in
-      ths MRS (Goal.prove ctxt [] [] goal' (K (tac ctxt 1)))
+      ths MRS (Goal.prove ctxt [] [] goal' (HEADGOAL o tac o #context))
     end
 
 fun contra_by_tac tac ctxt ths = prove_by_tac tac ctxt ths bFalse
 
 end  (* structure UtilLogic *)
 
 structure Basic_UtilLogic: BASIC_UTIL_LOGIC = UtilLogic
 open Basic_UtilLogic
diff --git a/thys/Auto2_Imperative_HOL/Functional/Indexed_PQueue.thy b/thys/Auto2_Imperative_HOL/Functional/Indexed_PQueue.thy
--- a/thys/Auto2_Imperative_HOL/Functional/Indexed_PQueue.thy
+++ b/thys/Auto2_Imperative_HOL/Functional/Indexed_PQueue.thy
@@ -1,380 +1,380 @@
 (*
   File: Indexed_PQueue.thy
   Author: Bohua Zhan
 *)
 
 section \<open>Indexed priority queues\<close>
 
 theory Indexed_PQueue
   imports Arrays_Ex Mapping_Str
 begin
 
 text \<open>
   Verification of indexed priority queue: functional part. The data
   structure is also verified by Lammich in
   \cite{Refine_Imperative_HOL-AFP}.
 \<close>
 
 subsection \<open>Successor functions, eq-pred predicate\<close>
 
 fun s1 :: "nat \<Rightarrow> nat" where "s1 m = 2 * m + 1"
 fun s2 :: "nat \<Rightarrow> nat" where "s2 m = 2 * m + 2"
 
 lemma s_inj [forward]:
   "s1 m = s1 m' \<Longrightarrow> m = m'" "s2 m = s2 m' \<Longrightarrow> m = m'" by auto
 lemma s_neq [resolve]:
   "s1 m \<noteq> s2 m'" "s1 m > m" "s2 m > m" "s2 m > s1 m" using s1.simps s2.simps by presburger+
 setup \<open>add_forward_prfstep_cond @{thm s_neq(2)} [with_term "s1 ?m"]\<close>
 setup \<open>add_forward_prfstep_cond @{thm s_neq(3)} [with_term "s2 ?m"]\<close>
 setup \<open>add_forward_prfstep_cond @{thm s_neq(4)} [with_term "s2 ?m", with_term "s1 ?m"]\<close>
 
 inductive eq_pred :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
   "eq_pred n n"
 | "eq_pred n m \<Longrightarrow> eq_pred n (s1 m)"
 | "eq_pred n m \<Longrightarrow> eq_pred n (s2 m)"
 setup \<open>add_case_induct_rule @{thm eq_pred.cases}\<close>
 setup \<open>add_prop_induct_rule @{thm eq_pred.induct}\<close>
 setup \<open>add_resolve_prfstep @{thm eq_pred.intros(1)}\<close>
 setup \<open>fold add_backward_prfstep @{thms eq_pred.intros(2,3)}\<close>
 
 lemma eq_pred_parent1 [forward]:
   "eq_pred i (s1 k) \<Longrightarrow> i \<noteq> s1 k \<Longrightarrow> eq_pred i k"
 @proof @let "v = s1 k" @prop_induct "eq_pred i v" @qed
 
 lemma eq_pred_parent2 [forward]:
   "eq_pred i (s2 k) \<Longrightarrow> i \<noteq> s2 k \<Longrightarrow> eq_pred i k"
 @proof @let "v = s2 k" @prop_induct "eq_pred i v" @qed
 
 lemma eq_pred_cases:
   "eq_pred i j \<Longrightarrow> eq_pred (s1 i) j \<or> eq_pred (s2 i) j \<or> j = i \<or> j = s1 i \<or> j = s2 i"
 @proof @prop_induct "eq_pred i j" @qed
 setup \<open>add_forward_prfstep_cond @{thm eq_pred_cases} [with_cond "?i \<noteq> s1 ?k", with_cond "?i \<noteq> s2 ?k"]\<close>
 
 lemma eq_pred_le [forward]: "eq_pred i j \<Longrightarrow> i \<le> j"
 @proof @prop_induct "eq_pred i j" @qed
 
 subsection \<open>Heap property\<close>
 
 text \<open>The corresponding tree is a heap\<close>
 definition is_heap :: "('a \<times> 'b::linorder) list \<Rightarrow> bool" where [rewrite]:
   "is_heap xs = (\<forall>i j. eq_pred i j \<longrightarrow> j < length xs \<longrightarrow> snd (xs ! i) \<le> snd (xs ! j))"
 
 lemma is_heapD:
   "is_heap xs \<Longrightarrow> j < length xs \<Longrightarrow> eq_pred i j \<Longrightarrow> snd (xs ! i) \<le> snd (xs ! j)" by auto2
 setup \<open>add_forward_prfstep_cond @{thm is_heapD} [with_term "?xs ! ?j"]\<close>
 setup \<open>del_prfstep_thm_eqforward @{thm is_heap_def}\<close>
 
 subsection \<open>Bubble-down\<close>
 
 text \<open>The corresponding tree is a heap, except k is not necessarily smaller than its descendents.\<close>
 definition is_heap_partial1 :: "('a \<times> 'b::linorder) list \<Rightarrow> nat \<Rightarrow> bool" where [rewrite]:
   "is_heap_partial1 xs k = (\<forall>i j. eq_pred i j \<longrightarrow> i \<noteq> k \<longrightarrow> j < length xs \<longrightarrow> snd (xs ! i) \<le> snd (xs ! j))"
 
 text \<open>Two cases of switching with s1 k.\<close>
 lemma bubble_down1:
   "s1 k < length xs \<Longrightarrow> is_heap_partial1 xs k \<Longrightarrow> snd (xs ! k) > snd (xs ! s1 k) \<Longrightarrow>
    snd (xs ! s1 k) \<le> snd (xs ! s2 k) \<Longrightarrow> is_heap_partial1 (list_swap xs k (s1 k)) (s1 k)" by auto2
 setup \<open>add_forward_prfstep_cond @{thm bubble_down1} [with_term "list_swap ?xs ?k (s1 ?k)"]\<close>
 
 lemma bubble_down2:
   "s1 k < length xs \<Longrightarrow> is_heap_partial1 xs k \<Longrightarrow> snd (xs ! k) > snd (xs ! s1 k) \<Longrightarrow>
    s2 k \<ge> length xs \<Longrightarrow> is_heap_partial1 (list_swap xs k (s1 k)) (s1 k)" by auto2
 setup \<open>add_forward_prfstep_cond @{thm bubble_down2} [with_term "list_swap ?xs ?k (s1 ?k)"]\<close>
 
 text \<open>One case of switching with s2 k.\<close>
 lemma bubble_down3:
   "s2 k < length xs \<Longrightarrow> is_heap_partial1 xs k \<Longrightarrow> snd (xs ! s1 k) > snd (xs ! s2 k) \<Longrightarrow>
    snd (xs ! k) > snd (xs ! s2 k) \<Longrightarrow> xs' = list_swap xs k (s2 k) \<Longrightarrow> is_heap_partial1 xs' (s2 k)" by auto2
 setup \<open>add_forward_prfstep_cond @{thm bubble_down3} [with_term "?xs'"]\<close>
 
 subsection \<open>Bubble-up\<close>
 
 fun par :: "nat \<Rightarrow> nat" where
   "par m = (m - 1) div 2"
 setup \<open>register_wellform_data ("par m", ["m \<noteq> 0"])\<close>
 
 lemma ps_inverse [rewrite]: "par (s1 k) = k" "par (s2 k) = k" by simp+
 
 lemma p_basic: "m \<noteq> 0 \<Longrightarrow> par m < m" by auto
 setup \<open>add_forward_prfstep_cond @{thm p_basic} [with_term "par ?m"]\<close>
 
 lemma p_cases: "m \<noteq> 0 \<Longrightarrow> m = s1 (par m) \<or> m = s2 (par m)" by auto
 setup \<open>add_forward_prfstep_cond @{thm p_cases} [with_term "par ?m"]\<close>
 
 lemma eq_pred_p_next:
   "i \<noteq> 0 \<Longrightarrow> eq_pred i j \<Longrightarrow> eq_pred (par i) j"
 @proof @prop_induct "eq_pred i j" @qed
 setup \<open>add_forward_prfstep_cond @{thm eq_pred_p_next} [with_term "par ?i"]\<close>
 
 lemma heap_implies_hd_min [resolve]:
   "is_heap xs \<Longrightarrow> i < length xs \<Longrightarrow> xs \<noteq> [] \<Longrightarrow> snd (hd xs) \<le> snd (xs ! i)"
 @proof
   @strong_induct i
   @case "i = 0" @apply_induct_hyp "par i"
   @have "eq_pred (par i) i"
 @qed
 
 text \<open>The corresponding tree is a heap, except k is not necessarily greater than its ancestors.\<close>
 definition is_heap_partial2 :: "('a \<times> 'b::linorder) list \<Rightarrow> nat \<Rightarrow> bool" where [rewrite]:
   "is_heap_partial2 xs k = (\<forall>i j. eq_pred i j \<longrightarrow> j < length xs \<longrightarrow> j \<noteq> k \<longrightarrow> snd (xs ! i) \<le> snd (xs ! j))"
 
 lemma bubble_up1 [forward]:
   "k < length xs \<Longrightarrow> is_heap_partial2 xs k \<Longrightarrow> snd (xs ! k) < snd (xs ! par k) \<Longrightarrow> k \<noteq> 0 \<Longrightarrow>
    is_heap_partial2 (list_swap xs k (par k)) (par k)" by auto2
 
 lemma bubble_up2 [forward]:
   "k < length xs \<Longrightarrow> is_heap_partial2 xs k \<Longrightarrow> snd (xs ! k) \<ge> snd (xs ! par k) \<Longrightarrow> k \<noteq> 0 \<Longrightarrow>
    is_heap xs" by auto2
 setup \<open>del_prfstep_thm @{thm p_cases}\<close>
 
 subsection \<open>Indexed priority queue\<close>
 
 type_synonym 'a idx_pqueue = "(nat \<times> 'a) list \<times> nat option list"
 
 fun index_of_pqueue :: "'a idx_pqueue \<Rightarrow> bool" where
   "index_of_pqueue (xs, m) = (
     (\<forall>i<length xs. fst (xs ! i) < length m \<and> m ! (fst (xs ! i)) = Some i) \<and>
     (\<forall>i. \<forall>k<length m. m ! k = Some i \<longrightarrow> i < length xs \<and> fst (xs ! i) = k))"
 setup \<open>add_rewrite_rule @{thm index_of_pqueue.simps}\<close>
 
 lemma index_of_pqueueD1:
   "i < length xs \<Longrightarrow> index_of_pqueue (xs, m) \<Longrightarrow>
    fst (xs ! i) < length m \<and> m ! (fst (xs ! i)) = Some i" by auto2
 setup \<open>add_forward_prfstep_cond @{thm index_of_pqueueD1} [with_term "?xs ! ?i"]\<close>
 
 lemma index_of_pqueueD2 [forward]:
   "k < length m \<Longrightarrow> index_of_pqueue (xs, m) \<Longrightarrow>
    m ! k = Some i \<Longrightarrow> i < length xs \<and> fst (xs ! i) = k" by auto2
 
 lemma index_of_pqueueD3 [forward]:
   "index_of_pqueue (xs, m) \<Longrightarrow> p \<in> set xs \<Longrightarrow> fst p < length m"
 @proof @obtain i where "i < length xs" "xs ! i = p" @qed
 setup \<open>del_prfstep_thm_eqforward @{thm index_of_pqueue.simps}\<close>
 
 lemma has_index_unique_key [forward]:
   "index_of_pqueue (xs, m) \<Longrightarrow> unique_keys_set (set xs)"
 @proof
   @have "\<forall>a x y. (a, x) \<in> set xs \<longrightarrow> (a, y) \<in> set xs \<longrightarrow> x = y" @with
     @obtain i where "i < length xs" "xs ! i = (a, x)"
     @obtain j where "j < length xs" "xs ! j = (a, y)"
   @end
 @qed
 
 lemma has_index_keys_of [rewrite]:
   "index_of_pqueue (xs, m) \<Longrightarrow> has_key_alist xs k \<longleftrightarrow> (k < length m \<and> m ! k \<noteq> None)"
 @proof
   @case "has_key_alist xs k" @with
     @obtain v' where "(k, v') \<in> set xs"
     @obtain i where "i < length xs \<and> xs ! i = (k, v')"
   @end
 @qed
 
 lemma has_index_distinct [forward]:
   "index_of_pqueue (xs, m) \<Longrightarrow> distinct xs"
 @proof
   @have "\<forall>i<length xs. \<forall>j<length xs. i \<noteq> j \<longrightarrow> xs ! i \<noteq> xs ! j"
 @qed
 
 subsection \<open>Basic operations on indexed\_queue\<close>
 
 fun idx_pqueue_swap_fun :: "(nat \<times> 'a) list \<times> nat option list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> (nat \<times> 'a) list \<times> nat option list" where
   "idx_pqueue_swap_fun (xs, m) i j = (
     list_swap xs i j, ((m [fst (xs ! i) := Some j]) [fst (xs ! j) := Some i]))"
 
 lemma index_of_pqueue_swap [forward_arg]:
   "i < length xs \<Longrightarrow> j < length xs \<Longrightarrow> index_of_pqueue (xs, m) \<Longrightarrow>
    index_of_pqueue (idx_pqueue_swap_fun (xs, m) i j)"
 @proof @unfold "idx_pqueue_swap_fun (xs, m) i j" @qed
 
 lemma fst_idx_pqueue_swap [rewrite]:
   "fst (idx_pqueue_swap_fun (xs, m) i j) = list_swap xs i j"
 @proof @unfold "idx_pqueue_swap_fun (xs, m) i j" @qed
 
 lemma snd_idx_pqueue_swap [rewrite]:
   "length (snd (idx_pqueue_swap_fun (xs, m) i j)) = length m"
 @proof @unfold "idx_pqueue_swap_fun (xs, m) i j" @qed
 
 fun idx_pqueue_push_fun :: "nat \<Rightarrow> 'a \<Rightarrow> 'a idx_pqueue \<Rightarrow> 'a idx_pqueue" where
   "idx_pqueue_push_fun k v (xs, m) = (xs @ [(k, v)], list_update m k (Some (length xs)))"
 
 lemma idx_pqueue_push_correct [forward_arg]:
   "index_of_pqueue (xs, m) \<Longrightarrow> k < length m \<Longrightarrow> \<not>has_key_alist xs k \<Longrightarrow>
    r = idx_pqueue_push_fun k v (xs, m) \<Longrightarrow>
    index_of_pqueue r \<and> fst r = xs @ [(k, v)] \<and> length (snd r) = length m"
 @proof @unfold "idx_pqueue_push_fun k v (xs, m)" @qed
 
 fun idx_pqueue_pop_fun :: "'a idx_pqueue \<Rightarrow> 'a idx_pqueue" where
   "idx_pqueue_pop_fun (xs, m) = (butlast xs, list_update m (fst (last xs)) None)"
 
 lemma idx_pqueue_pop_correct [forward_arg]:
   "index_of_pqueue (xs, m) \<Longrightarrow> xs \<noteq> [] \<Longrightarrow> r = idx_pqueue_pop_fun (xs, m) \<Longrightarrow>
    index_of_pqueue r \<and> fst r = butlast xs \<and> length (snd r) = length m"
 @proof
   @unfold "idx_pqueue_pop_fun (xs, m)"
   @have "length xs = length (butlast xs) + 1"
   @have "fst (xs ! length (butlast xs)) < length m"  (* TODO: remove? *)
 @qed
 
 subsection \<open>Bubble up and down\<close>
 
 function idx_bubble_down_fun :: "'a::linorder idx_pqueue \<Rightarrow> nat \<Rightarrow> 'a idx_pqueue" where
   "idx_bubble_down_fun (xs, m) k = (
     if s2 k < length xs then
       if snd (xs ! s1 k) \<le> snd (xs ! s2 k) then
         if snd (xs ! k) > snd (xs ! s1 k) then
           idx_bubble_down_fun (idx_pqueue_swap_fun (xs, m) k (s1 k)) (s1 k)
         else (xs, m)
       else
         if snd (xs ! k) > snd (xs ! s2 k) then
           idx_bubble_down_fun (idx_pqueue_swap_fun (xs, m) k (s2 k)) (s2 k)
         else (xs, m)
     else if s1 k < length xs then
       if snd (xs ! k) > snd (xs ! s1 k) then
         idx_bubble_down_fun (idx_pqueue_swap_fun (xs, m) k (s1 k)) (s1 k)
       else (xs, m)
     else (xs, m))"
   by pat_completeness auto
   termination by (relation "measure (\<lambda>((xs,_),k). (length xs - k))") (simp_all, auto2+)
 
 lemma idx_bubble_down_fun_correct:
   "r = idx_bubble_down_fun x k \<Longrightarrow> is_heap_partial1 (fst x) k \<Longrightarrow>
    is_heap (fst r) \<and> mset (fst r) = mset (fst x) \<and> length (snd r) = length (snd x)"
 @proof @fun_induct "idx_bubble_down_fun x k" @with
   @subgoal "(x = (xs, m), k = k)"
   @unfold "idx_bubble_down_fun (xs, m) k"
   @case "s2 k < length xs" @with
     @case "snd (xs ! s1 k) \<le> snd (xs ! s2 k)"
   @end
   @case "s1 k < length xs" @end
 @qed
 setup \<open>add_forward_prfstep_cond @{thm idx_bubble_down_fun_correct} [with_term "?r"]\<close>
 
 lemma idx_bubble_down_fun_correct2 [forward]:
   "index_of_pqueue x \<Longrightarrow> index_of_pqueue (idx_bubble_down_fun x k)"
 @proof @fun_induct "idx_bubble_down_fun x k" @with
   @subgoal "(x = (xs, m), k = k)"
   @unfold "idx_bubble_down_fun (xs, m) k"
   @case "s2 k < length xs" @with
     @case "snd (xs ! s1 k) \<le> snd (xs ! s2 k)"
   @end
   @case "s1 k < length xs" @end
 @qed
 
 fun idx_bubble_up_fun :: "'a::linorder idx_pqueue \<Rightarrow> nat \<Rightarrow> 'a idx_pqueue" where
   "idx_bubble_up_fun (xs, m) k = (
     if k = 0 then (xs, m)
     else if k < length xs then
       if snd (xs ! k) < snd (xs ! par k) then
         idx_bubble_up_fun (idx_pqueue_swap_fun (xs, m) k (par k)) (par k)
       else (xs, m)
     else (xs, m))"
 
 lemma idx_bubble_up_fun_correct:
   "r = idx_bubble_up_fun x k \<Longrightarrow> is_heap_partial2 (fst x) k \<Longrightarrow>
    is_heap (fst r) \<and> mset (fst r) = mset (fst x) \<and> length (snd r) = length (snd x)"
 @proof @fun_induct "idx_bubble_up_fun x k" @with
   @subgoal "(x = (xs, m), k = k)"
   @unfold "idx_bubble_up_fun (xs, m) k" @end
 @qed
 setup \<open>add_forward_prfstep_cond @{thm idx_bubble_up_fun_correct} [with_term "?r"]\<close>
 
 lemma idx_bubble_up_fun_correct2 [forward]:
   "index_of_pqueue x \<Longrightarrow> index_of_pqueue (idx_bubble_up_fun x k)"
 @proof @fun_induct "idx_bubble_up_fun x k" @with
   @subgoal "(x = (xs, m), k = k)"
   @unfold "idx_bubble_up_fun (xs, m) k" @end
 @qed
 
 subsection \<open>Main operations\<close>
 
 fun delete_min_idx_pqueue_fun :: "'a::linorder idx_pqueue \<Rightarrow> (nat \<times> 'a) \<times> 'a idx_pqueue" where
   "delete_min_idx_pqueue_fun (xs, m) = (
     let (xs', m') = idx_pqueue_swap_fun (xs, m) 0 (length xs - 1);
         a'' = idx_pqueue_pop_fun (xs', m')
      in (last xs', idx_bubble_down_fun a'' 0))"
 
 lemma delete_min_idx_pqueue_correct:
   "index_of_pqueue (xs, m) \<Longrightarrow> xs \<noteq> [] \<Longrightarrow> res = delete_min_idx_pqueue_fun (xs, m) \<Longrightarrow>
    index_of_pqueue (snd res)"
 @proof @unfold "delete_min_idx_pqueue_fun (xs, m)" @qed
 setup \<open>add_forward_prfstep_cond @{thm delete_min_idx_pqueue_correct} [with_term "?res"]\<close>
 
 lemma hd_last_swap_eval_last [rewrite]:
   "xs \<noteq> [] \<Longrightarrow> last (list_swap xs 0 (length xs - 1)) = hd xs"
 @proof
   @let "xs' = list_swap xs 0 (length xs - 1)"
   @have "last xs' = xs' ! (length xs - 1)"
 @qed
 
 text \<open>Correctness of delete-min.\<close>
 theorem delete_min_idx_pqueue_correct2:
   "is_heap xs \<Longrightarrow> xs \<noteq> [] \<Longrightarrow> res = delete_min_idx_pqueue_fun (xs, m) \<Longrightarrow> index_of_pqueue (xs, m) \<Longrightarrow>
    is_heap (fst (snd res)) \<and> fst res = hd xs \<and> length (snd (snd res)) = length m \<and>
    map_of_alist (fst (snd res)) = delete_map (fst (fst res)) (map_of_alist xs)"
 @proof @unfold "delete_min_idx_pqueue_fun (xs, m)"
   @let "xs' = list_swap xs 0 (length xs - 1)"
   @have "is_heap_partial1 (butlast xs') 0"
 @qed
 setup \<open>add_forward_prfstep_cond @{thm delete_min_idx_pqueue_correct2} [with_term "?res"]\<close>
 
 fun insert_idx_pqueue_fun :: "nat \<Rightarrow> 'a::linorder \<Rightarrow> 'a idx_pqueue \<Rightarrow> 'a idx_pqueue" where
   "insert_idx_pqueue_fun k v x = (
     let x' = idx_pqueue_push_fun k v x in
       idx_bubble_up_fun x' (length (fst x') - 1))"
 
 lemma insert_idx_pqueue_correct [forward_arg]:
   "index_of_pqueue (xs, m) \<Longrightarrow> k < length m \<Longrightarrow> \<not>has_key_alist xs k \<Longrightarrow>
    index_of_pqueue (insert_idx_pqueue_fun k v (xs, m))"
 @proof @unfold "insert_idx_pqueue_fun k v (xs, m)" @qed
 
 text \<open>Correctness of insertion.\<close>
 theorem insert_idx_pqueue_correct2:
   "index_of_pqueue (xs, m) \<Longrightarrow> is_heap xs \<Longrightarrow> k < length m \<Longrightarrow> \<not>has_key_alist xs k \<Longrightarrow>
    r = insert_idx_pqueue_fun k v (xs, m) \<Longrightarrow>
    is_heap (fst r) \<and> length (snd r) = length m \<and>
    map_of_alist (fst r) = map_of_alist xs { k \<rightarrow> v }"
 @proof @unfold "insert_idx_pqueue_fun k v (xs, m)"
   @have "is_heap_partial2 (xs @ [(k, v)]) (length xs)"
 @qed
 setup \<open>add_forward_prfstep_cond @{thm insert_idx_pqueue_correct2} [with_term "?r"]\<close>
 
 fun update_idx_pqueue_fun :: "nat \<Rightarrow> 'a::linorder \<Rightarrow> 'a idx_pqueue \<Rightarrow> 'a idx_pqueue" where
   "update_idx_pqueue_fun k v (xs, m) = (
     if m ! k = None then
       insert_idx_pqueue_fun k v (xs, m)
     else let
       i = the (m ! k);
       xs' = list_update xs i (k, v)
     in
       if snd (xs ! i) \<le> v then idx_bubble_down_fun (xs', m) i
       else idx_bubble_up_fun (xs', m) i)"
 
 lemma update_idx_pqueue_correct [forward_arg]:
   "index_of_pqueue (xs, m) \<Longrightarrow> k < length m \<Longrightarrow>
    index_of_pqueue (update_idx_pqueue_fun k v (xs, m))"
 @proof @unfold "update_idx_pqueue_fun k v (xs, m)"
-  @let "i = the (m ! k)"
-  @let "xs' = list_update xs i (k, v)"
+  @let "i' = the (m ! k)"
+  @let "xs' = list_update xs i' (k, v)"
   @case "m ! k = None"
   @have "index_of_pqueue (xs', m)"
 @qed
 
 text \<open>Correctness of update.\<close>
 theorem update_idx_pqueue_correct2:
   "index_of_pqueue (xs, m) \<Longrightarrow> is_heap xs \<Longrightarrow> k < length m \<Longrightarrow>
    r = update_idx_pqueue_fun k v (xs, m) \<Longrightarrow>
    is_heap (fst r) \<and> length (snd r) = length m \<and>
    map_of_alist (fst r) = map_of_alist xs { k \<rightarrow> v }"
 @proof @unfold "update_idx_pqueue_fun k v (xs, m)"
   @let "i = the (m ! k)"
   @let "xs' = list_update xs i (k, v)"
   @have "xs' = fst (xs', m)" (* TODO: remove *)
   @case "m ! k = None"
   @case "snd (xs ! the (m ! k)) \<le> v" @with
     @have "is_heap_partial1 xs' i"
   @end
   @have "is_heap_partial2 xs' i"
 @qed
 setup \<open>add_forward_prfstep_cond @{thm update_idx_pqueue_correct2} [with_term "?r"]\<close>
 
 end