[STATEMENT]
lemma hm_swim_op_\<alpha>_correct: "hm_swim_op hm i \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hm_swim_op hm i \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm)
[PROOF STEP]
apply (rule leof_add_nofailI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nofail (hm_swim_op hm i) \<Longrightarrow> hm_swim_op hm i \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm)
[PROOF STEP]
apply (drule hm_swim_op_nofail_imp_valid)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hm_valid hm i \<and> h.swim_invar (hmr_\<alpha> hm) i \<Longrightarrow> hm_swim_op hm i \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm)
[PROOF STEP]
unfolding hm_swim_op_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hm_valid hm i \<and> h.swim_invar (hmr_\<alpha> hm) i \<Longrightarrow> REC\<^sub>T (\<lambda>swim (h, i). ASSERT (hm_valid h i \<and> h.swim_invar (hmr_\<alpha> h) i) \<bind> (\<lambda>_. if hm_valid h (h.parent i) then hm_prio_of_op h (h.parent i) \<bind> (\<lambda>ppi. hm_prio_of_op h i \<bind> (\<lambda>pi. if \<not> ppi \<le> pi then hm_exch_op h i (h.parent i) \<bind> (\<lambda>h. swim (h, h.parent i)) else RETURN h)) else RETURN h)) (hm, i) \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm)
[PROOF STEP]
apply (rule RECT_rule_leof[where
            pre="\<lambda>(hm',i). hm_valid hm' i \<and> heapmap_\<alpha> hm' = heapmap_\<alpha> hm"
            and V = "inv_image less_than snd"
            ])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. hm_valid hm i \<and> h.swim_invar (hmr_\<alpha> hm) i \<Longrightarrow> wf (inv_image less_than snd)
 2. hm_valid hm i \<and> h.swim_invar (hmr_\<alpha> hm) i \<Longrightarrow> case (hm, i) of (hm', i) \<Rightarrow> hm_valid hm' i \<and> heapmap_\<alpha> hm' = heapmap_\<alpha> hm
 3. \<And>f x. \<lbrakk>hm_valid hm i \<and> h.swim_invar (hmr_\<alpha> hm) i; \<And>x'. \<lbrakk>case x' of (hm', i) \<Rightarrow> hm_valid hm' i \<and> heapmap_\<alpha> hm' = heapmap_\<alpha> hm; (x', x) \<in> inv_image less_than snd\<rbrakk> \<Longrightarrow> f x' \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm); case x of (hm', i) \<Rightarrow> hm_valid hm' i \<and> heapmap_\<alpha> hm' = heapmap_\<alpha> hm; REC\<^sub>T (\<lambda>swim a. case a of (h, i) \<Rightarrow> ASSERT (hm_valid h i \<and> h.swim_invar (hmr_\<alpha> h) i) \<bind> (\<lambda>_. if hm_valid h (h.parent i) then hm_prio_of_op h (h.parent i) \<bind> (\<lambda>ppi. hm_prio_of_op h i \<bind> (\<lambda>pi. if \<not> ppi \<le> pi then hm_exch_op h i (h.parent i) \<bind> (\<lambda>h. swim (h, h.parent i)) else RETURN h)) else RETURN h)) = f\<rbrakk> \<Longrightarrow> (case x of (h, i) \<Rightarrow> ASSERT (hm_valid h i \<and> h.swim_invar (hmr_\<alpha> h) i) \<bind> (\<lambda>_. if hm_valid h (h.parent i) then hm_prio_of_op h (h.parent i) \<bind> (\<lambda>ppi. hm_prio_of_op h i \<bind> (\<lambda>pi. if \<not> ppi \<le> pi then hm_exch_op h i (h.parent i) \<bind> (\<lambda>h. f (h, h.parent i)) else RETURN h)) else RETURN h)) \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. hm_valid hm i \<and> h.swim_invar (hmr_\<alpha> hm) i \<Longrightarrow> case (hm, i) of (hm', i) \<Rightarrow> hm_valid hm' i \<and> heapmap_\<alpha> hm' = heapmap_\<alpha> hm
 2. \<And>f x. \<lbrakk>hm_valid hm i \<and> h.swim_invar (hmr_\<alpha> hm) i; \<And>x'. \<lbrakk>case x' of (hm', i) \<Rightarrow> hm_valid hm' i \<and> heapmap_\<alpha> hm' = heapmap_\<alpha> hm; (x', x) \<in> inv_image less_than snd\<rbrakk> \<Longrightarrow> f x' \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm); case x of (hm', i) \<Rightarrow> hm_valid hm' i \<and> heapmap_\<alpha> hm' = heapmap_\<alpha> hm; REC\<^sub>T (\<lambda>swim a. case a of (h, i) \<Rightarrow> ASSERT (hm_valid h i \<and> h.swim_invar (hmr_\<alpha> h) i) \<bind> (\<lambda>_. if hm_valid h (h.parent i) then hm_prio_of_op h (h.parent i) \<bind> (\<lambda>ppi. hm_prio_of_op h i \<bind> (\<lambda>pi. if \<not> ppi \<le> pi then hm_exch_op h i (h.parent i) \<bind> (\<lambda>h. swim (h, h.parent i)) else RETURN h)) else RETURN h)) = f\<rbrakk> \<Longrightarrow> (case x of (h, i) \<Rightarrow> ASSERT (hm_valid h i \<and> h.swim_invar (hmr_\<alpha> h) i) \<bind> (\<lambda>_. if hm_valid h (h.parent i) then hm_prio_of_op h (h.parent i) \<bind> (\<lambda>ppi. hm_prio_of_op h i \<bind> (\<lambda>pi. if \<not> ppi \<le> pi then hm_exch_op h i (h.parent i) \<bind> (\<lambda>h. f (h, h.parent i)) else RETURN h)) else RETURN h)) \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f x. \<lbrakk>hm_valid hm i \<and> h.swim_invar (hmr_\<alpha> hm) i; \<And>x'. \<lbrakk>case x' of (hm', i) \<Rightarrow> hm_valid hm' i \<and> heapmap_\<alpha> hm' = heapmap_\<alpha> hm; (x', x) \<in> inv_image less_than snd\<rbrakk> \<Longrightarrow> f x' \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm); case x of (hm', i) \<Rightarrow> hm_valid hm' i \<and> heapmap_\<alpha> hm' = heapmap_\<alpha> hm; REC\<^sub>T (\<lambda>swim a. case a of (h, i) \<Rightarrow> ASSERT (hm_valid h i \<and> h.swim_invar (hmr_\<alpha> h) i) \<bind> (\<lambda>_. if hm_valid h (h.parent i) then hm_prio_of_op h (h.parent i) \<bind> (\<lambda>ppi. hm_prio_of_op h i \<bind> (\<lambda>pi. if \<not> ppi \<le> pi then hm_exch_op h i (h.parent i) \<bind> (\<lambda>h. swim (h, h.parent i)) else RETURN h)) else RETURN h)) = f\<rbrakk> \<Longrightarrow> (case x of (h, i) \<Rightarrow> ASSERT (hm_valid h i \<and> h.swim_invar (hmr_\<alpha> h) i) \<bind> (\<lambda>_. if hm_valid h (h.parent i) then hm_prio_of_op h (h.parent i) \<bind> (\<lambda>ppi. hm_prio_of_op h i \<bind> (\<lambda>pi. if \<not> ppi \<le> pi then hm_exch_op h i (h.parent i) \<bind> (\<lambda>h. f (h, h.parent i)) else RETURN h)) else RETURN h)) \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm)
[PROOF STEP]
unfolding hm_prio_of_op_def hm_val_of_op_def
        hm_exch_op_def hm_key_of_op_def hm_the_lookup_op_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f x. \<lbrakk>hm_valid hm i \<and> h.swim_invar (hmr_\<alpha> hm) i; \<And>x'. \<lbrakk>case x' of (hm', i) \<Rightarrow> hm_valid hm' i \<and> heapmap_\<alpha> hm' = heapmap_\<alpha> hm; (x', x) \<in> inv_image less_than snd\<rbrakk> \<Longrightarrow> f x' \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm); case x of (hm', i) \<Rightarrow> hm_valid hm' i \<and> heapmap_\<alpha> hm' = heapmap_\<alpha> hm; REC\<^sub>T (\<lambda>swim a. case a of (h, i) \<Rightarrow> ASSERT (hm_valid h i \<and> h.swim_invar (hmr_\<alpha> h) i) \<bind> (\<lambda>_. if hm_valid h (h.parent i) then (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) (h.parent i) \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>ppi. (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) i \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pi. if \<not> ppi \<le> pi then (case h of (pq, m) \<Rightarrow> \<lambda>i j. ASSERT (hm_valid (pq, m) i) \<bind> (\<lambda>_. ASSERT (hm_valid (pq, m) j) \<bind> (\<lambda>_. ASSERT (hmr_invar (pq, m)) \<bind> (\<lambda>_. mop_list_swap pq (i - 1) (j - 1) \<bind> (\<lambda>pq. RETURN (pq, m)))))) i (h.parent i) \<bind> (\<lambda>h. swim (h, h.parent i)) else RETURN h)) else RETURN h)) = f\<rbrakk> \<Longrightarrow> (case x of (h, i) \<Rightarrow> ASSERT (hm_valid h i \<and> h.swim_invar (hmr_\<alpha> h) i) \<bind> (\<lambda>_. if hm_valid h (h.parent i) then (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) (h.parent i) \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>ppi. (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) i \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pi. if \<not> ppi \<le> pi then (case h of (pq, m) \<Rightarrow> \<lambda>i j. ASSERT (hm_valid (pq, m) i) \<bind> (\<lambda>_. ASSERT (hm_valid (pq, m) j) \<bind> (\<lambda>_. ASSERT (hmr_invar (pq, m)) \<bind> (\<lambda>_. mop_list_swap pq (i - 1) (j - 1) \<bind> (\<lambda>pq. RETURN (pq, m)))))) i (h.parent i) \<bind> (\<lambda>h. f (h, h.parent i)) else RETURN h)) else RETURN h)) \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm)
[PROOF STEP]
apply (refine_vcg)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>f x x1 x1a x2 x1b x2a x2b. \<lbrakk>hm_valid hm i \<and> h.swim_invar (hmr_\<alpha> hm) i; \<And>x'. \<lbrakk>case x' of (hm', i) \<Rightarrow> hm_valid hm' i \<and> heapmap_\<alpha> hm' = heapmap_\<alpha> hm; (x', x) \<in> inv_image less_than snd\<rbrakk> \<Longrightarrow> f x' \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm); case x of (hm', i) \<Rightarrow> hm_valid hm' i \<and> heapmap_\<alpha> hm' = heapmap_\<alpha> hm; REC\<^sub>T (\<lambda>swim a. case a of (h, i) \<Rightarrow> ASSERT (hm_valid h i \<and> h.swim_invar (hmr_\<alpha> h) i) \<bind> (\<lambda>_. if hm_valid h (h.parent i) then (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) (h.parent i) \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>ppi. (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) i \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pi. if \<not> ppi \<le> pi then (case h of (pq, m) \<Rightarrow> \<lambda>i j. ASSERT (hm_valid (pq, m) i) \<bind> (\<lambda>_. ASSERT (hm_valid (pq, m) j) \<bind> (\<lambda>_. ASSERT (hmr_invar (pq, m)) \<bind> (\<lambda>_. mop_list_swap pq (i - 1) (j - 1) \<bind> (\<lambda>pq. RETURN (pq, m)))))) i (h.parent i) \<bind> (\<lambda>h. swim (h, h.parent i)) else RETURN h)) else RETURN h)) = f; x1 = (x1a, x2); x1 = (x1b, x2a); x = (x1, x2b); hm_valid x1 x2b \<and> h.swim_invar (hmr_\<alpha> x1) x2b; hm_valid x1 (h.parent x2b); 0 < h.parent x2b; h.parent x2b - 1 < length x1b; heapmap_\<alpha> x1 (x1b ! (h.parent x2b - 1)) \<noteq> None \<and> hmr_invar x1; 0 < x2b; x2b - 1 < length x1b; heapmap_\<alpha> x1 (x1b ! (x2b - 1)) \<noteq> None \<and> hmr_invar x1; \<not> prio (the (heapmap_\<alpha> x1 (x1b ! (h.parent x2b - 1)))) \<le> prio (the (heapmap_\<alpha> x1 (x1b ! (x2b - 1)))); hm_valid (x1a, x2) x2b; hm_valid (x1a, x2) (h.parent x2b); hmr_invar (x1a, x2); x2b - 1 < length x1a \<and> h.parent x2b - 1 < length x1a\<rbrakk> \<Longrightarrow> f ((swap x1a (x2b - 1) (h.parent x2b - 1), x2), h.parent x2b) \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm)
 2. \<And>f x x1 x1a x2 x1b x2a x2b. \<lbrakk>hm_valid hm i \<and> h.swim_invar (hmr_\<alpha> hm) i; \<And>x'. \<lbrakk>case x' of (hm', i) \<Rightarrow> hm_valid hm' i \<and> heapmap_\<alpha> hm' = heapmap_\<alpha> hm; (x', x) \<in> inv_image less_than snd\<rbrakk> \<Longrightarrow> f x' \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm); case x of (hm', i) \<Rightarrow> hm_valid hm' i \<and> heapmap_\<alpha> hm' = heapmap_\<alpha> hm; REC\<^sub>T (\<lambda>swim a. case a of (h, i) \<Rightarrow> ASSERT (hm_valid h i \<and> h.swim_invar (hmr_\<alpha> h) i) \<bind> (\<lambda>_. if hm_valid h (h.parent i) then (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) (h.parent i) \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>ppi. (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) i \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pi. if \<not> ppi \<le> pi then (case h of (pq, m) \<Rightarrow> \<lambda>i j. ASSERT (hm_valid (pq, m) i) \<bind> (\<lambda>_. ASSERT (hm_valid (pq, m) j) \<bind> (\<lambda>_. ASSERT (hmr_invar (pq, m)) \<bind> (\<lambda>_. mop_list_swap pq (i - 1) (j - 1) \<bind> (\<lambda>pq. RETURN (pq, m)))))) i (h.parent i) \<bind> (\<lambda>h. swim (h, h.parent i)) else RETURN h)) else RETURN h)) = f; x1 = (x1a, x2); x1 = (x1b, x2a); x = (x1, x2b); hm_valid x1 x2b \<and> h.swim_invar (hmr_\<alpha> x1) x2b; hm_valid x1 (h.parent x2b); 0 < h.parent x2b; h.parent x2b - 1 < length x1b; heapmap_\<alpha> x1 (x1b ! (h.parent x2b - 1)) \<noteq> None \<and> hmr_invar x1; 0 < x2b; x2b - 1 < length x1b; heapmap_\<alpha> x1 (x1b ! (x2b - 1)) \<noteq> None \<and> hmr_invar x1; \<not> \<not> prio (the (heapmap_\<alpha> x1 (x1b ! (h.parent x2b - 1)))) \<le> prio (the (heapmap_\<alpha> x1 (x1b ! (x2b - 1))))\<rbrakk> \<Longrightarrow> heapmap_\<alpha> x1 = heapmap_\<alpha> hm
 3. \<And>f x x1 x1a x2 x1b x2a x2b. \<lbrakk>hm_valid hm i \<and> h.swim_invar (hmr_\<alpha> hm) i; \<And>x'. \<lbrakk>case x' of (hm', i) \<Rightarrow> hm_valid hm' i \<and> heapmap_\<alpha> hm' = heapmap_\<alpha> hm; (x', x) \<in> inv_image less_than snd\<rbrakk> \<Longrightarrow> f x' \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm); case x of (hm', i) \<Rightarrow> hm_valid hm' i \<and> heapmap_\<alpha> hm' = heapmap_\<alpha> hm; REC\<^sub>T (\<lambda>swim a. case a of (h, i) \<Rightarrow> ASSERT (hm_valid h i \<and> h.swim_invar (hmr_\<alpha> h) i) \<bind> (\<lambda>_. if hm_valid h (h.parent i) then (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) (h.parent i) \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>ppi. (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) i \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pi. if \<not> ppi \<le> pi then (case h of (pq, m) \<Rightarrow> \<lambda>i j. ASSERT (hm_valid (pq, m) i) \<bind> (\<lambda>_. ASSERT (hm_valid (pq, m) j) \<bind> (\<lambda>_. ASSERT (hmr_invar (pq, m)) \<bind> (\<lambda>_. mop_list_swap pq (i - 1) (j - 1) \<bind> (\<lambda>pq. RETURN (pq, m)))))) i (h.parent i) \<bind> (\<lambda>h. swim (h, h.parent i)) else RETURN h)) else RETURN h)) = f; x1 = (x1a, x2); x1 = (x1b, x2a); x = (x1, x2b); hm_valid x1 x2b \<and> h.swim_invar (hmr_\<alpha> x1) x2b; \<not> hm_valid x1 (h.parent x2b)\<rbrakk> \<Longrightarrow> heapmap_\<alpha> x1 = heapmap_\<alpha> hm
[PROOF STEP]
apply (vc_solve simp add: hm_valid_def hm_length_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1a x2 x2b y ya. \<lbrakk>\<And>a b ba. \<lbrakk>0 < ba \<and> ba \<le> length a \<and> heapmap_\<alpha> (a, b) = heapmap_\<alpha> hm; ba < x2b\<rbrakk> \<Longrightarrow> REC\<^sub>T (\<lambda>swim (h, i). ASSERT (0 < i \<and> i \<le> (case h of (pq, uu_) \<Rightarrow> length pq) \<and> h.swim_invar (hmr_\<alpha> h) i) \<bind> (\<lambda>_. if 0 < h.parent i \<and> h.parent i \<le> (case h of (pq, uu_) \<Rightarrow> length pq) then (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) (h.parent i) \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>ppi. (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) i \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pi. if \<not> ppi \<le> pi then (case h of (pq, m) \<Rightarrow> \<lambda>i j. ASSERT (hm_valid (pq, m) i) \<bind> (\<lambda>_. ASSERT (hm_valid (pq, m) j) \<bind> (\<lambda>_. ASSERT (hmr_invar (pq, m)) \<bind> (\<lambda>_. mop_list_swap pq (i - 1) (j - 1) \<bind> (\<lambda>pq. RETURN (pq, m)))))) i (h.parent i) \<bind> (\<lambda>h. swim (h, h.parent i)) else RETURN h)) else RETURN h)) ((a, b), ba) \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm); h.swim_invar (hmr_\<alpha> (x1a, x2)) x2b; h.parent x2b \<le> length x1a; 0 < h.parent x2b; h.parent x2b - Suc 0 < length x1a; 0 < x2b; x2b - Suc 0 < length x1a; \<not> prio y \<le> prio ya; hmr_invar (x1a, x2); heapmap_\<alpha> hm (x1a ! (h.parent x2b - Suc 0)) = Some y; heapmap_\<alpha> hm (x1a ! (x2b - Suc 0)) = Some ya; 0 < i; x2b \<le> length x1a; heapmap_\<alpha> (x1a, x2) = heapmap_\<alpha> hm; i \<le> (case hm of (pq, uu_) \<Rightarrow> length pq); h.swim_invar (hmr_\<alpha> hm) i\<rbrakk> \<Longrightarrow> REC\<^sub>T (\<lambda>swim (h, i). ASSERT (0 < i \<and> i \<le> (case h of (pq, uu_) \<Rightarrow> length pq) \<and> h.swim_invar (hmr_\<alpha> h) i) \<bind> (\<lambda>_. if 0 < h.parent i \<and> h.parent i \<le> (case h of (pq, uu_) \<Rightarrow> length pq) then (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) (h.parent i) \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>ppi. (case h of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) i \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> h k \<noteq> None \<and> hmr_invar h) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> h k))) \<bind> RETURN) \<bind> (\<lambda>v. RETURN (prio v)) \<bind> (\<lambda>pi. if \<not> ppi \<le> pi then (case h of (pq, m) \<Rightarrow> \<lambda>i j. ASSERT (hm_valid (pq, m) i) \<bind> (\<lambda>_. ASSERT (hm_valid (pq, m) j) \<bind> (\<lambda>_. ASSERT (hmr_invar (pq, m)) \<bind> (\<lambda>_. mop_list_swap pq (i - 1) (j - 1) \<bind> (\<lambda>pq. RETURN (pq, m)))))) i (h.parent i) \<bind> (\<lambda>h. swim (h, h.parent i)) else RETURN h)) else RETURN h)) ((swap x1a (x2b - Suc 0) (h.parent x2b - Suc 0), x2), h.parent x2b) \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm)
[PROOF STEP]
apply rprems
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x1a x2 x2b y ya. \<lbrakk>h.swim_invar (hmr_\<alpha> (x1a, x2)) x2b; h.parent x2b \<le> length x1a; 0 < h.parent x2b; h.parent x2b - Suc 0 < length x1a; 0 < x2b; x2b - Suc 0 < length x1a; \<not> prio y \<le> prio ya; hmr_invar (x1a, x2); heapmap_\<alpha> hm (x1a ! (h.parent x2b - Suc 0)) = Some y; heapmap_\<alpha> hm (x1a ! (x2b - Suc 0)) = Some ya; 0 < i; x2b \<le> length x1a; heapmap_\<alpha> (x1a, x2) = heapmap_\<alpha> hm; i \<le> (case hm of (pq, uu_) \<Rightarrow> length pq); h.swim_invar (hmr_\<alpha> hm) i\<rbrakk> \<Longrightarrow> 0 < h.parent x2b \<and> h.parent x2b \<le> length (swap x1a (x2b - Suc 0) (h.parent x2b - Suc 0)) \<and> heapmap_\<alpha> (swap x1a (x2b - Suc 0) (h.parent x2b - Suc 0), x2) = heapmap_\<alpha> hm
 2. \<And>x1a x2 x2b y ya. \<lbrakk>h.swim_invar (hmr_\<alpha> (x1a, x2)) x2b; h.parent x2b \<le> length x1a; 0 < h.parent x2b; h.parent x2b - Suc 0 < length x1a; 0 < x2b; x2b - Suc 0 < length x1a; \<not> prio y \<le> prio ya; hmr_invar (x1a, x2); heapmap_\<alpha> hm (x1a ! (h.parent x2b - Suc 0)) = Some y; heapmap_\<alpha> hm (x1a ! (x2b - Suc 0)) = Some ya; 0 < i; x2b \<le> length x1a; heapmap_\<alpha> (x1a, x2) = heapmap_\<alpha> hm; i \<le> (case hm of (pq, uu_) \<Rightarrow> length pq); h.swim_invar (hmr_\<alpha> hm) i\<rbrakk> \<Longrightarrow> h.parent x2b < x2b
[PROOF STEP]
apply (vc_solve simp: heapmap_\<alpha>_def h.parent_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma hm_sink_op_refine: "(hm_sink_op, h.sink_op) \<in> hmr_rel \<rightarrow> nat_rel \<rightarrow> \<langle>hmr_rel\<rangle>nres_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (hm_sink_op, h.sink_op) \<in> hmr_rel \<rightarrow> nat_rel \<rightarrow> \<langle>hmr_rel\<rangle>nres_rel
[PROOF STEP]
apply (intro fun_relI nres_relI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' aa a'a. \<lbrakk>(a, a') \<in> hmr_rel; (aa, a'a) \<in> nat_rel\<rbrakk> \<Longrightarrow> hm_sink_op a aa \<le> \<Down> hmr_rel (h.sink_op a' a'a)
[PROOF STEP]
unfolding hm_sink_op_def h.sink_op_opt_eq[symmetric] h.sink_op_opt_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' aa a'a. \<lbrakk>(a, a') \<in> hmr_rel; (aa, a'a) \<in> nat_rel\<rbrakk> \<Longrightarrow> REC\<^sub>T (\<lambda>D (h, k). ASSERT (0 < k \<and> k \<le> hm_length h) \<bind> (\<lambda>_. let len = hm_length h in if 2 * k \<le> len then let j = 2 * k in hm_prio_of_op h j \<bind> (\<lambda>pj. (if j < len then hm_prio_of_op h (Suc j) \<bind> (\<lambda>psj. if psj < pj then RETURN (j + 1) else RETURN j) else RETURN j) \<bind> (\<lambda>j. hm_prio_of_op h j \<bind> (\<lambda>pj. hm_prio_of_op h k \<bind> (\<lambda>pk. if pj < pk then hm_exch_op h k j \<bind> (\<lambda>h. D (h, j)) else RETURN h)))) else RETURN h)) (a, aa) \<le> \<Down> hmr_rel (REC\<^sub>T (\<lambda>D (h, k). ASSERT (0 < k \<and> k \<le> length h) \<bind> (\<lambda>_. let len = length h in if 2 * k \<le> len then let j = 2 * k in h.prio_of_op h j \<bind> (\<lambda>pj. (if j < len then h.prio_of_op h (Suc j) \<bind> (\<lambda>psj. if psj < pj then RETURN (j + 1) else RETURN j) else RETURN j) \<bind> (\<lambda>j. h.prio_of_op h j \<bind> (\<lambda>pj. h.prio_of_op h k \<bind> (\<lambda>pk. if pj < pk then h.exch_op h k j \<bind> (\<lambda>h. D (h, j)) else RETURN h)))) else RETURN h)) (a', a'a))
[PROOF STEP]
apply refine_rcg
[PROOF STATE]
proof (prove)
goal (24 subgoals):
 1. \<And>a a' aa a'a. \<lbrakk>(a, a') \<in> hmr_rel; (aa, a'a) \<in> nat_rel\<rbrakk> \<Longrightarrow> ((a, aa), a', a'a) \<in> ?R3 a a' aa a'a
 2. \<And>a a' aa a'a D Da x x' x1 x2 x1a x2a. \<lbrakk>(a, a') \<in> hmr_rel; (aa, a'a) \<in> nat_rel; \<And>x x'. (x, x') \<in> ?R3 a a' aa a'a \<Longrightarrow> D x \<le> \<Down> hmr_rel (Da x'); (x, x') \<in> ?R3 a a' aa a'a; x' = (x1, x2); x = (x1a, x2a); 0 < x2 \<and> x2 \<le> length x1\<rbrakk> \<Longrightarrow> 0 < x2a
 3. \<And>a a' aa a'a D Da x x' x1 x2 x1a x2a. \<lbrakk>(a, a') \<in> hmr_rel; (aa, a'a) \<in> nat_rel; \<And>x x'. (x, x') \<in> ?R3 a a' aa a'a \<Longrightarrow> D x \<le> \<Down> hmr_rel (Da x'); (x, x') \<in> ?R3 a a' aa a'a; x' = (x1, x2); x = (x1a, x2a); 0 < x2 \<and> x2 \<le> length x1\<rbrakk> \<Longrightarrow> x2a \<le> hm_length x1a
 4. \<And>a a' aa a'a D Da x x' x1 x2 x1a x2a. \<lbrakk>(a, a') \<in> hmr_rel; (aa, a'a) \<in> nat_rel; \<And>x x'. (x, x') \<in> ?R3 a a' aa a'a \<Longrightarrow> D x \<le> \<Down> hmr_rel (Da x'); (x, x') \<in> ?R3 a a' aa a'a; x' = (x1, x2); x = (x1a, x2a); 0 < x2 \<and> x2 \<le> length x1; 0 < x2a \<and> x2a \<le> hm_length x1a\<rbrakk> \<Longrightarrow> (2 * x2a \<le> hm_length x1a) = (2 * x2 \<le> length x1)
 5. \<And>a a' aa a'a D Da x x' x1 x2 x1a x2a. \<lbrakk>(a, a') \<in> hmr_rel; (aa, a'a) \<in> nat_rel; \<And>x x'. (x, x') \<in> ?R3 a a' aa a'a \<Longrightarrow> D x \<le> \<Down> hmr_rel (Da x'); (x, x') \<in> ?R3 a a' aa a'a; x' = (x1, x2); x = (x1a, x2a); 0 < x2 \<and> x2 \<le> length x1; 0 < x2a \<and> x2a \<le> hm_length x1a; 2 * x2a \<le> hm_length x1a; 2 * x2 \<le> length x1\<rbrakk> \<Longrightarrow> (x1a, x1) \<in> hmr_rel
 6. \<And>a a' aa a'a D Da x x' x1 x2 x1a x2a. \<lbrakk>(a, a') \<in> hmr_rel; (aa, a'a) \<in> nat_rel; \<And>x x'. (x, x') \<in> ?R3 a a' aa a'a \<Longrightarrow> D x \<le> \<Down> hmr_rel (Da x'); (x, x') \<in> ?R3 a a' aa a'a; x' = (x1, x2); x = (x1a, x2a); 0 < x2 \<and> x2 \<le> length x1; 0 < x2a \<and> x2a \<le> hm_length x1a; 2 * x2a \<le> hm_length x1a; 2 * x2 \<le> length x1\<rbrakk> \<Longrightarrow> (2 * x2a, 2 * x2) \<in> nat_rel
 7. \<And>a a' aa a'a D Da x x' x1 x2 x1a x2a pj pja. \<lbrakk>(a, a') \<in> hmr_rel; (aa, a'a) \<in> nat_rel; \<And>x x'. (x, x') \<in> ?R3 a a' aa a'a \<Longrightarrow> D x \<le> \<Down> hmr_rel (Da x'); (x, x') \<in> ?R3 a a' aa a'a; x' = (x1, x2); x = (x1a, x2a); 0 < x2 \<and> x2 \<le> length x1; 0 < x2a \<and> x2a \<le> hm_length x1a; 2 * x2a \<le> hm_length x1a; 2 * x2 \<le> length x1; (pj, pja) \<in> Id\<rbrakk> \<Longrightarrow> (2 * x2a < hm_length x1a) = (2 * x2 < length x1)
 8. \<And>a a' aa a'a D Da x x' x1 x2 x1a x2a pj pja. \<lbrakk>(a, a') \<in> hmr_rel; (aa, a'a) \<in> nat_rel; \<And>x x'. (x, x') \<in> ?R3 a a' aa a'a \<Longrightarrow> D x \<le> \<Down> hmr_rel (Da x'); (x, x') \<in> ?R3 a a' aa a'a; x' = (x1, x2); x = (x1a, x2a); 0 < x2 \<and> x2 \<le> length x1; 0 < x2a \<and> x2a \<le> hm_length x1a; 2 * x2a \<le> hm_length x1a; 2 * x2 \<le> length x1; (pj, pja) \<in> Id; 2 * x2a < hm_length x1a; 2 * x2 < length x1\<rbrakk> \<Longrightarrow> (x1a, x1) \<in> hmr_rel
 9. \<And>a a' aa a'a D Da x x' x1 x2 x1a x2a pj pja. \<lbrakk>(a, a') \<in> hmr_rel; (aa, a'a) \<in> nat_rel; \<And>x x'. (x, x') \<in> ?R3 a a' aa a'a \<Longrightarrow> D x \<le> \<Down> hmr_rel (Da x'); (x, x') \<in> ?R3 a a' aa a'a; x' = (x1, x2); x = (x1a, x2a); 0 < x2 \<and> x2 \<le> length x1; 0 < x2a \<and> x2a \<le> hm_length x1a; 2 * x2a \<le> hm_length x1a; 2 * x2 \<le> length x1; (pj, pja) \<in> Id; 2 * x2a < hm_length x1a; 2 * x2 < length x1\<rbrakk> \<Longrightarrow> (Suc (2 * x2a), Suc (2 * x2)) \<in> nat_rel
 10. \<And>a a' aa a'a D Da x x' x1 x2 x1a x2a pj pja psj psja. \<lbrakk>(a, a') \<in> hmr_rel; (aa, a'a) \<in> nat_rel; \<And>x x'. (x, x') \<in> ?R3 a a' aa a'a \<Longrightarrow> D x \<le> \<Down> hmr_rel (Da x'); (x, x') \<in> ?R3 a a' aa a'a; x' = (x1, x2); x = (x1a, x2a); 0 < x2 \<and> x2 \<le> length x1; 0 < x2a \<and> x2a \<le> hm_length x1a; 2 * x2a \<le> hm_length x1a; 2 * x2 \<le> length x1; (pj, pja) \<in> Id; 2 * x2a < hm_length x1a; 2 * x2 < length x1; (psj, psja) \<in> Id\<rbrakk> \<Longrightarrow> (psj < pj) = (psja < pja)
A total of 24 subgoals...
[PROOF STEP]
apply refine_dref_type
[PROOF STATE]
proof (prove)
goal (22 subgoals):
 1. \<And>a a' aa a'a. \<lbrakk>(a, a') \<in> hmr_rel; (aa, a'a) \<in> nat_rel\<rbrakk> \<Longrightarrow> ((a, aa), a', a'a) \<in> hmr_rel \<times>\<^sub>r nat_rel
 2. \<And>a a' aa a'a D Da x x' x1 x2 x1a x2a. \<lbrakk>(a, a') \<in> hmr_rel; (aa, a'a) \<in> nat_rel; \<And>x x'. (x, x') \<in> hmr_rel \<times>\<^sub>r nat_rel \<Longrightarrow> D x \<le> \<Down> hmr_rel (Da x'); (x, x') \<in> hmr_rel \<times>\<^sub>r nat_rel; x' = (x1, x2); x = (x1a, x2a); 0 < x2 \<and> x2 \<le> length x1\<rbrakk> \<Longrightarrow> 0 < x2a
 3. \<And>a a' aa a'a D Da x x' x1 x2 x1a x2a. \<lbrakk>(a, a') \<in> hmr_rel; (aa, a'a) \<in> nat_rel; \<And>x x'. (x, x') \<in> hmr_rel \<times>\<^sub>r nat_rel \<Longrightarrow> D x \<le> \<Down> hmr_rel (Da x'); (x, x') \<in> hmr_rel \<times>\<^sub>r nat_rel; x' = (x1, x2); x = (x1a, x2a); 0 < x2 \<and> x2 \<le> length x1\<rbrakk> \<Longrightarrow> x2a \<le> hm_length x1a
 4. \<And>a a' aa a'a D Da x x' x1 x2 x1a x2a. \<lbrakk>(a, a') \<in> hmr_rel; (aa, a'a) \<in> nat_rel; \<And>x x'. (x, x') \<in> hmr_rel \<times>\<^sub>r nat_rel \<Longrightarrow> D x \<le> \<Down> hmr_rel (Da x'); (x, x') \<in> hmr_rel \<times>\<^sub>r nat_rel; x' = (x1, x2); x = (x1a, x2a); 0 < x2 \<and> x2 \<le> length x1; 0 < x2a \<and> x2a \<le> hm_length x1a\<rbrakk> \<Longrightarrow> (2 * x2a \<le> hm_length x1a) = (2 * x2 \<le> length x1)
 5. \<And>a a' aa a'a D Da x x' x1 x2 x1a x2a. \<lbrakk>(a, a') \<in> hmr_rel; (aa, a'a) \<in> nat_rel; \<And>x x'. (x, x') \<in> hmr_rel \<times>\<^sub>r nat_rel \<Longrightarrow> D x \<le> \<Down> hmr_rel (Da x'); (x, x') \<in> hmr_rel \<times>\<^sub>r nat_rel; x' = (x1, x2); x = (x1a, x2a); 0 < x2 \<and> x2 \<le> length x1; 0 < x2a \<and> x2a \<le> hm_length x1a; 2 * x2a \<le> hm_length x1a; 2 * x2 \<le> length x1\<rbrakk> \<Longrightarrow> (x1a, x1) \<in> hmr_rel
 6. \<And>a a' aa a'a D Da x x' x1 x2 x1a x2a. \<lbrakk>(a, a') \<in> hmr_rel; (aa, a'a) \<in> nat_rel; \<And>x x'. (x, x') \<in> hmr_rel \<times>\<^sub>r nat_rel \<Longrightarrow> D x \<le> \<Down> hmr_rel (Da x'); (x, x') \<in> hmr_rel \<times>\<^sub>r nat_rel; x' = (x1, x2); x = (x1a, x2a); 0 < x2 \<and> x2 \<le> length x1; 0 < x2a \<and> x2a \<le> hm_length x1a; 2 * x2a \<le> hm_length x1a; 2 * x2 \<le> length x1\<rbrakk> \<Longrightarrow> (2 * x2a, 2 * x2) \<in> nat_rel
 7. \<And>a a' aa a'a D Da x x' x1 x2 x1a x2a pj pja. \<lbrakk>(a, a') \<in> hmr_rel; (aa, a'a) \<in> nat_rel; \<And>x x'. (x, x') \<in> hmr_rel \<times>\<^sub>r nat_rel \<Longrightarrow> D x \<le> \<Down> hmr_rel (Da x'); (x, x') \<in> hmr_rel \<times>\<^sub>r nat_rel; x' = (x1, x2); x = (x1a, x2a); 0 < x2 \<and> x2 \<le> length x1; 0 < x2a \<and> x2a \<le> hm_length x1a; 2 * x2a \<le> hm_length x1a; 2 * x2 \<le> length x1; (pj, pja) \<in> Id\<rbrakk> \<Longrightarrow> (2 * x2a < hm_length x1a) = (2 * x2 < length x1)
 8. \<And>a a' aa a'a D Da x x' x1 x2 x1a x2a pj pja. \<lbrakk>(a, a') \<in> hmr_rel; (aa, a'a) \<in> nat_rel; \<And>x x'. (x, x') \<in> hmr_rel \<times>\<^sub>r nat_rel \<Longrightarrow> D x \<le> \<Down> hmr_rel (Da x'); (x, x') \<in> hmr_rel \<times>\<^sub>r nat_rel; x' = (x1, x2); x = (x1a, x2a); 0 < x2 \<and> x2 \<le> length x1; 0 < x2a \<and> x2a \<le> hm_length x1a; 2 * x2a \<le> hm_length x1a; 2 * x2 \<le> length x1; (pj, pja) \<in> Id; 2 * x2a < hm_length x1a; 2 * x2 < length x1\<rbrakk> \<Longrightarrow> (x1a, x1) \<in> hmr_rel
 9. \<And>a a' aa a'a D Da x x' x1 x2 x1a x2a pj pja. \<lbrakk>(a, a') \<in> hmr_rel; (aa, a'a) \<in> nat_rel; \<And>x x'. (x, x') \<in> hmr_rel \<times>\<^sub>r nat_rel \<Longrightarrow> D x \<le> \<Down> hmr_rel (Da x'); (x, x') \<in> hmr_rel \<times>\<^sub>r nat_rel; x' = (x1, x2); x = (x1a, x2a); 0 < x2 \<and> x2 \<le> length x1; 0 < x2a \<and> x2a \<le> hm_length x1a; 2 * x2a \<le> hm_length x1a; 2 * x2 \<le> length x1; (pj, pja) \<in> Id; 2 * x2a < hm_length x1a; 2 * x2 < length x1\<rbrakk> \<Longrightarrow> (Suc (2 * x2a), Suc (2 * x2)) \<in> nat_rel
 10. \<And>a a' aa a'a D Da x x' x1 x2 x1a x2a pj pja psj psja. \<lbrakk>(a, a') \<in> hmr_rel; (aa, a'a) \<in> nat_rel; \<And>x x'. (x, x') \<in> hmr_rel \<times>\<^sub>r nat_rel \<Longrightarrow> D x \<le> \<Down> hmr_rel (Da x'); (x, x') \<in> hmr_rel \<times>\<^sub>r nat_rel; x' = (x1, x2); x = (x1a, x2a); 0 < x2 \<and> x2 \<le> length x1; 0 < x2a \<and> x2a \<le> hm_length x1a; 2 * x2a \<le> hm_length x1a; 2 * x2 \<le> length x1; (pj, pja) \<in> Id; 2 * x2a < hm_length x1a; 2 * x2 < length x1; (psj, psja) \<in> Id\<rbrakk> \<Longrightarrow> (psj < pj) = (psja < pja)
A total of 22 subgoals...
[PROOF STEP]
unfolding hmr_rel_def heapmap_rel_def
[PROOF STATE]
proof (prove)
goal (22 subgoals):
 1. \<And>a a' aa a'a. \<lbrakk>(a, a') \<in> br hmr_\<alpha> hmr_invar; (aa, a'a) \<in> nat_rel\<rbrakk> \<Longrightarrow> ((a, aa), a', a'a) \<in> br hmr_\<alpha> hmr_invar \<times>\<^sub>r nat_rel
 2. \<And>a a' aa a'a D Da x x' x1 x2 x1a x2a. \<lbrakk>(a, a') \<in> br hmr_\<alpha> hmr_invar; (aa, a'a) \<in> nat_rel; \<And>x x'. (x, x') \<in> br hmr_\<alpha> hmr_invar \<times>\<^sub>r nat_rel \<Longrightarrow> D x \<le> \<Down> (br hmr_\<alpha> hmr_invar) (Da x'); (x, x') \<in> br hmr_\<alpha> hmr_invar \<times>\<^sub>r nat_rel; x' = (x1, x2); x = (x1a, x2a); 0 < x2 \<and> x2 \<le> length x1\<rbrakk> \<Longrightarrow> 0 < x2a
 3. \<And>a a' aa a'a D Da x x' x1 x2 x1a x2a. \<lbrakk>(a, a') \<in> br hmr_\<alpha> hmr_invar; (aa, a'a) \<in> nat_rel; \<And>x x'. (x, x') \<in> br hmr_\<alpha> hmr_invar \<times>\<^sub>r nat_rel \<Longrightarrow> D x \<le> \<Down> (br hmr_\<alpha> hmr_invar) (Da x'); (x, x') \<in> br hmr_\<alpha> hmr_invar \<times>\<^sub>r nat_rel; x' = (x1, x2); x = (x1a, x2a); 0 < x2 \<and> x2 \<le> length x1\<rbrakk> \<Longrightarrow> x2a \<le> hm_length x1a
 4. \<And>a a' aa a'a D Da x x' x1 x2 x1a x2a. \<lbrakk>(a, a') \<in> br hmr_\<alpha> hmr_invar; (aa, a'a) \<in> nat_rel; \<And>x x'. (x, x') \<in> br hmr_\<alpha> hmr_invar \<times>\<^sub>r nat_rel \<Longrightarrow> D x \<le> \<Down> (br hmr_\<alpha> hmr_invar) (Da x'); (x, x') \<in> br hmr_\<alpha> hmr_invar \<times>\<^sub>r nat_rel; x' = (x1, x2); x = (x1a, x2a); 0 < x2 \<and> x2 \<le> length x1; 0 < x2a \<and> x2a \<le> hm_length x1a\<rbrakk> \<Longrightarrow> (2 * x2a \<le> hm_length x1a) = (2 * x2 \<le> length x1)
 5. \<And>a a' aa a'a D Da x x' x1 x2 x1a x2a. \<lbrakk>(a, a') \<in> br hmr_\<alpha> hmr_invar; (aa, a'a) \<in> nat_rel; \<And>x x'. (x, x') \<in> br hmr_\<alpha> hmr_invar \<times>\<^sub>r nat_rel \<Longrightarrow> D x \<le> \<Down> (br hmr_\<alpha> hmr_invar) (Da x'); (x, x') \<in> br hmr_\<alpha> hmr_invar \<times>\<^sub>r nat_rel; x' = (x1, x2); x = (x1a, x2a); 0 < x2 \<and> x2 \<le> length x1; 0 < x2a \<and> x2a \<le> hm_length x1a; 2 * x2a \<le> hm_length x1a; 2 * x2 \<le> length x1\<rbrakk> \<Longrightarrow> (x1a, x1) \<in> br hmr_\<alpha> hmr_invar
 6. \<And>a a' aa a'a D Da x x' x1 x2 x1a x2a. \<lbrakk>(a, a') \<in> br hmr_\<alpha> hmr_invar; (aa, a'a) \<in> nat_rel; \<And>x x'. (x, x') \<in> br hmr_\<alpha> hmr_invar \<times>\<^sub>r nat_rel \<Longrightarrow> D x \<le> \<Down> (br hmr_\<alpha> hmr_invar) (Da x'); (x, x') \<in> br hmr_\<alpha> hmr_invar \<times>\<^sub>r nat_rel; x' = (x1, x2); x = (x1a, x2a); 0 < x2 \<and> x2 \<le> length x1; 0 < x2a \<and> x2a \<le> hm_length x1a; 2 * x2a \<le> hm_length x1a; 2 * x2 \<le> length x1\<rbrakk> \<Longrightarrow> (2 * x2a, 2 * x2) \<in> nat_rel
 7. \<And>a a' aa a'a D Da x x' x1 x2 x1a x2a pj pja. \<lbrakk>(a, a') \<in> br hmr_\<alpha> hmr_invar; (aa, a'a) \<in> nat_rel; \<And>x x'. (x, x') \<in> br hmr_\<alpha> hmr_invar \<times>\<^sub>r nat_rel \<Longrightarrow> D x \<le> \<Down> (br hmr_\<alpha> hmr_invar) (Da x'); (x, x') \<in> br hmr_\<alpha> hmr_invar \<times>\<^sub>r nat_rel; x' = (x1, x2); x = (x1a, x2a); 0 < x2 \<and> x2 \<le> length x1; 0 < x2a \<and> x2a \<le> hm_length x1a; 2 * x2a \<le> hm_length x1a; 2 * x2 \<le> length x1; (pj, pja) \<in> Id\<rbrakk> \<Longrightarrow> (2 * x2a < hm_length x1a) = (2 * x2 < length x1)
 8. \<And>a a' aa a'a D Da x x' x1 x2 x1a x2a pj pja. \<lbrakk>(a, a') \<in> br hmr_\<alpha> hmr_invar; (aa, a'a) \<in> nat_rel; \<And>x x'. (x, x') \<in> br hmr_\<alpha> hmr_invar \<times>\<^sub>r nat_rel \<Longrightarrow> D x \<le> \<Down> (br hmr_\<alpha> hmr_invar) (Da x'); (x, x') \<in> br hmr_\<alpha> hmr_invar \<times>\<^sub>r nat_rel; x' = (x1, x2); x = (x1a, x2a); 0 < x2 \<and> x2 \<le> length x1; 0 < x2a \<and> x2a \<le> hm_length x1a; 2 * x2a \<le> hm_length x1a; 2 * x2 \<le> length x1; (pj, pja) \<in> Id; 2 * x2a < hm_length x1a; 2 * x2 < length x1\<rbrakk> \<Longrightarrow> (x1a, x1) \<in> br hmr_\<alpha> hmr_invar
 9. \<And>a a' aa a'a D Da x x' x1 x2 x1a x2a pj pja. \<lbrakk>(a, a') \<in> br hmr_\<alpha> hmr_invar; (aa, a'a) \<in> nat_rel; \<And>x x'. (x, x') \<in> br hmr_\<alpha> hmr_invar \<times>\<^sub>r nat_rel \<Longrightarrow> D x \<le> \<Down> (br hmr_\<alpha> hmr_invar) (Da x'); (x, x') \<in> br hmr_\<alpha> hmr_invar \<times>\<^sub>r nat_rel; x' = (x1, x2); x = (x1a, x2a); 0 < x2 \<and> x2 \<le> length x1; 0 < x2a \<and> x2a \<le> hm_length x1a; 2 * x2a \<le> hm_length x1a; 2 * x2 \<le> length x1; (pj, pja) \<in> Id; 2 * x2a < hm_length x1a; 2 * x2 < length x1\<rbrakk> \<Longrightarrow> (Suc (2 * x2a), Suc (2 * x2)) \<in> nat_rel
 10. \<And>a a' aa a'a D Da x x' x1 x2 x1a x2a pj pja psj psja. \<lbrakk>(a, a') \<in> br hmr_\<alpha> hmr_invar; (aa, a'a) \<in> nat_rel; \<And>x x'. (x, x') \<in> br hmr_\<alpha> hmr_invar \<times>\<^sub>r nat_rel \<Longrightarrow> D x \<le> \<Down> (br hmr_\<alpha> hmr_invar) (Da x'); (x, x') \<in> br hmr_\<alpha> hmr_invar \<times>\<^sub>r nat_rel; x' = (x1, x2); x = (x1a, x2a); 0 < x2 \<and> x2 \<le> length x1; 0 < x2a \<and> x2a \<le> hm_length x1a; 2 * x2a \<le> hm_length x1a; 2 * x2 \<le> length x1; (pj, pja) \<in> Id; 2 * x2a < hm_length x1a; 2 * x2 < length x1; (psj, psja) \<in> Id\<rbrakk> \<Longrightarrow> (psj < pj) = (psja < pja)
A total of 22 subgoals...
[PROOF STEP]
apply (clarsimp_all simp: in_br_conv)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma hm_sink_op_nofail_imp_valid: "nofail (hm_sink_op hm i) \<Longrightarrow> hm_valid hm i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nofail (hm_sink_op hm i) \<Longrightarrow> hm_valid hm i
[PROOF STEP]
unfolding hm_sink_op_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nofail (REC\<^sub>T (\<lambda>D (h, k). ASSERT (0 < k \<and> k \<le> hm_length h) \<bind> (\<lambda>_. let len = hm_length h in if 2 * k \<le> len then let j = 2 * k in hm_prio_of_op h j \<bind> (\<lambda>pj. (if j < len then hm_prio_of_op h (Suc j) \<bind> (\<lambda>psj. if psj < pj then RETURN (j + 1) else RETURN j) else RETURN j) \<bind> (\<lambda>j. hm_prio_of_op h j \<bind> (\<lambda>pj. hm_prio_of_op h k \<bind> (\<lambda>pk. if pj < pk then hm_exch_op h k j \<bind> (\<lambda>h. D (h, j)) else RETURN h)))) else RETURN h)) (hm, i)) \<Longrightarrow> hm_valid hm i
[PROOF STEP]
apply (subst (asm) RECT_unfold, refine_mono)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nofail (case (hm, i) of (h, k) \<Rightarrow> ASSERT (0 < k \<and> k \<le> hm_length h) \<bind> (\<lambda>_. let len = hm_length h in if 2 * k \<le> len then let j = 2 * k in hm_prio_of_op h j \<bind> (\<lambda>pj. (if j < len then hm_prio_of_op h (Suc j) \<bind> (\<lambda>psj. if psj < pj then RETURN (j + 1) else RETURN j) else RETURN j) \<bind> (\<lambda>j. hm_prio_of_op h j \<bind> (\<lambda>pj. hm_prio_of_op h k \<bind> (\<lambda>pk. if pj < pk then hm_exch_op h k j \<bind> (\<lambda>h. REC\<^sub>T (\<lambda>D (h, k). ASSERT (0 < k \<and> k \<le> hm_length h) \<bind> (\<lambda>_. let len = hm_length h in if 2 * k \<le> len then let j = 2 * k in hm_prio_of_op h j \<bind> (\<lambda>pj. (if j < len then hm_prio_of_op h (Suc j) \<bind> (\<lambda>psj. if psj < pj then RETURN (j + 1) else RETURN j) else RETURN j) \<bind> (\<lambda>j. hm_prio_of_op h j \<bind> (\<lambda>pj. hm_prio_of_op h k \<bind> (\<lambda>pk. if pj < pk then hm_exch_op h k j \<bind> (\<lambda>h. D (h, j)) else RETURN h)))) else RETURN h)) (h, j)) else RETURN h)))) else RETURN h)) \<Longrightarrow> hm_valid hm i
[PROOF STEP]
by (auto simp: refine_pw_simps hm_valid_def)