[STATEMENT]
lemma hm_decrease_key_op_refine:
      "\<lbrakk>(hm,h)\<in>hmr_rel; (hm,m)\<in>heapmap_rel; m k = Some v'\<rbrakk>
        \<Longrightarrow> hm_decrease_key_op k v hm \<le>\<Down>hmr_rel (h.decrease_key_op (hm_index hm k) v h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(hm, h) \<in> hmr_rel; (hm, m) \<in> heapmap_rel; m k = Some v'\<rbrakk> \<Longrightarrow> hm_decrease_key_op k v hm \<le> \<Down> hmr_rel (h.decrease_key_op (hm_index hm k) v h)
[PROOF STEP]
unfolding hm_decrease_key_op_def h.decrease_key_op_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(hm, h) \<in> hmr_rel; (hm, m) \<in> heapmap_rel; m k = Some v'\<rbrakk> \<Longrightarrow> ASSERT (heapmap_invar hm) \<bind> (\<lambda>_. ASSERT (heapmap_\<alpha> hm k \<noteq> None \<and> prio v \<le> prio (the (heapmap_\<alpha> hm k))) \<bind> (\<lambda>_. hm_index_op hm k \<bind> (\<lambda>i. hm_update_op hm i v \<bind> (\<lambda>hm. hm_swim_op hm i)))) \<le> \<Down> hmr_rel (ASSERT (h.valid h (hm_index hm k) \<and> prio v \<le> h.prio_of h (hm_index hm k)) \<bind> (\<lambda>_. h.update_op h (hm_index hm k) v \<bind> (\<lambda>h. h.swim_op h (hm_index hm k))))
[PROOF STEP]
(*apply (rewrite at "Let (hm_index hm k) _" Let_def)*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(hm, h) \<in> hmr_rel; (hm, m) \<in> heapmap_rel; m k = Some v'\<rbrakk> \<Longrightarrow> ASSERT (heapmap_invar hm) \<bind> (\<lambda>_. ASSERT (heapmap_\<alpha> hm k \<noteq> None \<and> prio v \<le> prio (the (heapmap_\<alpha> hm k))) \<bind> (\<lambda>_. hm_index_op hm k \<bind> (\<lambda>i. hm_update_op hm i v \<bind> (\<lambda>hm. hm_swim_op hm i)))) \<le> \<Down> hmr_rel (ASSERT (h.valid h (hm_index hm k) \<and> prio v \<le> h.prio_of h (hm_index hm k)) \<bind> (\<lambda>_. h.update_op h (hm_index hm k) v \<bind> (\<lambda>h. h.swim_op h (hm_index hm k))))
[PROOF STEP]
apply (refine_rcg index_op_inline_refine)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<lbrakk>(hm, h) \<in> hmr_rel; (hm, m) \<in> heapmap_rel; m k = Some v'; h.valid h (hm_index hm k) \<and> prio v \<le> h.prio_of h (hm_index hm k)\<rbrakk> \<Longrightarrow> heapmap_invar hm
 2. \<lbrakk>(hm, h) \<in> hmr_rel; (hm, m) \<in> heapmap_rel; m k = Some v'; h.valid h (hm_index hm k) \<and> prio v \<le> h.prio_of h (hm_index hm k); heapmap_invar hm\<rbrakk> \<Longrightarrow> heapmap_\<alpha> hm k \<noteq> None
 3. \<lbrakk>(hm, h) \<in> hmr_rel; (hm, m) \<in> heapmap_rel; m k = Some v'; h.valid h (hm_index hm k) \<and> prio v \<le> h.prio_of h (hm_index hm k); heapmap_invar hm\<rbrakk> \<Longrightarrow> prio v \<le> prio (the (heapmap_\<alpha> hm k))
 4. \<lbrakk>(hm, h) \<in> hmr_rel; (hm, m) \<in> heapmap_rel; m k = Some v'; h.valid h (hm_index hm k) \<and> prio v \<le> h.prio_of h (hm_index hm k); heapmap_invar hm; heapmap_\<alpha> hm k \<noteq> None \<and> prio v \<le> prio (the (heapmap_\<alpha> hm k))\<rbrakk> \<Longrightarrow> heapmap_\<alpha> hm k \<noteq> None
 5. \<lbrakk>(hm, h) \<in> hmr_rel; (hm, m) \<in> heapmap_rel; m k = Some v'; h.valid h (hm_index hm k) \<and> prio v \<le> h.prio_of h (hm_index hm k); heapmap_invar hm; heapmap_\<alpha> hm k \<noteq> None \<and> prio v \<le> prio (the (heapmap_\<alpha> hm k))\<rbrakk> \<Longrightarrow> (hm_index hm k, hm_index hm k) \<in> nat_rel
 6. \<lbrakk>(hm, h) \<in> hmr_rel; (hm, m) \<in> heapmap_rel; m k = Some v'; h.valid h (hm_index hm k) \<and> prio v \<le> h.prio_of h (hm_index hm k); heapmap_invar hm; heapmap_\<alpha> hm k \<noteq> None \<and> prio v \<le> prio (the (heapmap_\<alpha> hm k))\<rbrakk> \<Longrightarrow> (v, v) \<in> Id
 7. \<And>hma ha. \<lbrakk>(hm, h) \<in> hmr_rel; (hm, m) \<in> heapmap_rel; m k = Some v'; h.valid h (hm_index hm k) \<and> prio v \<le> h.prio_of h (hm_index hm k); heapmap_invar hm; heapmap_\<alpha> hm k \<noteq> None \<and> prio v \<le> prio (the (heapmap_\<alpha> hm k)); (hma, ha) \<in> hmr_rel\<rbrakk> \<Longrightarrow> (hm_index hm k, hm_index hm k) \<in> nat_rel
[PROOF STEP]
unfolding hmr_rel_def heapmap_rel_def in_br_conv
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<lbrakk>h = hmr_\<alpha> hm \<and> hmr_invar hm; m = heapmap_\<alpha> hm \<and> heapmap_invar hm; m k = Some v'; h.valid h (hm_index hm k) \<and> prio v \<le> h.prio_of h (hm_index hm k)\<rbrakk> \<Longrightarrow> heapmap_invar hm
 2. \<lbrakk>h = hmr_\<alpha> hm \<and> hmr_invar hm; m = heapmap_\<alpha> hm \<and> heapmap_invar hm; m k = Some v'; h.valid h (hm_index hm k) \<and> prio v \<le> h.prio_of h (hm_index hm k); heapmap_invar hm\<rbrakk> \<Longrightarrow> heapmap_\<alpha> hm k \<noteq> None
 3. \<lbrakk>h = hmr_\<alpha> hm \<and> hmr_invar hm; m = heapmap_\<alpha> hm \<and> heapmap_invar hm; m k = Some v'; h.valid h (hm_index hm k) \<and> prio v \<le> h.prio_of h (hm_index hm k); heapmap_invar hm\<rbrakk> \<Longrightarrow> prio v \<le> prio (the (heapmap_\<alpha> hm k))
 4. \<lbrakk>h = hmr_\<alpha> hm \<and> hmr_invar hm; m = heapmap_\<alpha> hm \<and> heapmap_invar hm; m k = Some v'; h.valid h (hm_index hm k) \<and> prio v \<le> h.prio_of h (hm_index hm k); heapmap_invar hm; heapmap_\<alpha> hm k \<noteq> None \<and> prio v \<le> prio (the (heapmap_\<alpha> hm k))\<rbrakk> \<Longrightarrow> heapmap_\<alpha> hm k \<noteq> None
 5. \<lbrakk>h = hmr_\<alpha> hm \<and> hmr_invar hm; m = heapmap_\<alpha> hm \<and> heapmap_invar hm; m k = Some v'; h.valid h (hm_index hm k) \<and> prio v \<le> h.prio_of h (hm_index hm k); heapmap_invar hm; heapmap_\<alpha> hm k \<noteq> None \<and> prio v \<le> prio (the (heapmap_\<alpha> hm k))\<rbrakk> \<Longrightarrow> (hm_index hm k, hm_index hm k) \<in> nat_rel
 6. \<lbrakk>h = hmr_\<alpha> hm \<and> hmr_invar hm; m = heapmap_\<alpha> hm \<and> heapmap_invar hm; m k = Some v'; h.valid h (hm_index hm k) \<and> prio v \<le> h.prio_of h (hm_index hm k); heapmap_invar hm; heapmap_\<alpha> hm k \<noteq> None \<and> prio v \<le> prio (the (heapmap_\<alpha> hm k))\<rbrakk> \<Longrightarrow> (v, v) \<in> Id
 7. \<And>hma ha. \<lbrakk>h = hmr_\<alpha> hm \<and> hmr_invar hm; m = heapmap_\<alpha> hm \<and> heapmap_invar hm; m k = Some v'; h.valid h (hm_index hm k) \<and> prio v \<le> h.prio_of h (hm_index hm k); heapmap_invar hm; heapmap_\<alpha> hm k \<noteq> None \<and> prio v \<le> prio (the (heapmap_\<alpha> hm k)); ha = hmr_\<alpha> hma \<and> hmr_invar hma\<rbrakk> \<Longrightarrow> (hm_index hm k, hm_index hm k) \<in> nat_rel
[PROOF STEP]
apply (clarsimp_all)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma hm_index_op_inline_leof:
      assumes "f (hm_index hm k) \<le>\<^sub>n m"
      shows "do {i \<leftarrow> hm_index_op hm k; f i} \<le>\<^sub>n m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hm_index_op hm k \<bind> f \<le>\<^sub>n m
[PROOF STEP]
using hm_index_op_correct[of hm k] assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>hmr_invar hm; heapmap_\<alpha> hm k \<noteq> None\<rbrakk> \<Longrightarrow> hm_index_op hm k \<le> SPEC (\<lambda>r. r = hm_index hm k)
f (hm_index hm k) \<le>\<^sub>n m

goal (1 subgoal):
 1. hm_index_op hm k \<bind> f \<le>\<^sub>n m
[PROOF STEP]
unfolding hm_index_op_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>hmr_invar hm; heapmap_\<alpha> hm k \<noteq> None\<rbrakk> \<Longrightarrow> (case hm of (pq, m) \<Rightarrow> \<lambda>k. ASSERT (hmr_invar (pq, m) \<and> heapmap_\<alpha> (pq, m) k \<noteq> None) \<bind> (\<lambda>_. mop_list_index pq k \<bind> (\<lambda>i. RETURN (i + 1)))) k \<le> SPEC (\<lambda>r. r = hm_index hm k)
f (hm_index hm k) \<le>\<^sub>n m

goal (1 subgoal):
 1. (case hm of (pq, m) \<Rightarrow> \<lambda>k. ASSERT (hmr_invar (pq, m) \<and> heapmap_\<alpha> (pq, m) k \<noteq> None) \<bind> (\<lambda>_. mop_list_index pq k \<bind> (\<lambda>i. RETURN (i + 1)))) k \<bind> f \<le>\<^sub>n m
[PROOF STEP]
by (auto simp: pw_le_iff pw_leof_iff refine_pw_simps split: prod.splits)


[STATEMENT]
lemma hm_decrease_key_op_\<alpha>_correct:
      "heapmap_invar hm \<Longrightarrow> hm_decrease_key_op k v hm \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm(k\<mapsto>v))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. heapmap_invar hm \<Longrightarrow> hm_decrease_key_op k v hm \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm(k \<mapsto> v))
[PROOF STEP]
unfolding hm_decrease_key_op_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. heapmap_invar hm \<Longrightarrow> ASSERT (heapmap_invar hm) \<bind> (\<lambda>_. ASSERT (heapmap_\<alpha> hm k \<noteq> None \<and> prio v \<le> prio (the (heapmap_\<alpha> hm k))) \<bind> (\<lambda>_. hm_index_op hm k \<bind> (\<lambda>i. hm_update_op hm i v \<bind> (\<lambda>hm. hm_swim_op hm i)))) \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm(k \<mapsto> v))
[PROOF STEP]
apply (refine_vcg
        hm_update_op_\<alpha>_correct[THEN leof_trans]
        hm_swim_op_\<alpha>_correct[THEN leof_trans]
        hm_index_op_inline_leof
        )
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>heapmap_invar hm; heapmap_invar hm; heapmap_\<alpha> hm k \<noteq> None \<and> prio v \<le> prio (the (heapmap_\<alpha> hm k))\<rbrakk> \<Longrightarrow> hmr_invar hm
 2. \<lbrakk>heapmap_invar hm; heapmap_invar hm; heapmap_\<alpha> hm k \<noteq> None \<and> prio v \<le> prio (the (heapmap_\<alpha> hm k))\<rbrakk> \<Longrightarrow> heapmap_\<alpha> hm k \<noteq> None
 3. \<And>x xa. \<lbrakk>heapmap_invar hm; heapmap_invar hm; heapmap_\<alpha> hm k \<noteq> None \<and> prio v \<le> prio (the (heapmap_\<alpha> hm k)); x \<in> {hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm(k \<mapsto> v)}; xa \<in> {hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> x}\<rbrakk> \<Longrightarrow> heapmap_\<alpha> xa = heapmap_\<alpha> hm(k \<mapsto> v)
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma hm_decrease_key_op_aref:
      "(hm_decrease_key_op, PR_CONST (mop_pm_decrease_key prio)) \<in> Id \<rightarrow> Id \<rightarrow> heapmap_rel \<rightarrow> \<langle>heapmap_rel\<rangle>nres_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (hm_decrease_key_op, PR_CONST (mop_pm_decrease_key prio)) \<in> Id \<rightarrow> Id \<rightarrow> heapmap_rel \<rightarrow> \<langle>heapmap_rel\<rangle>nres_rel
[PROOF STEP]
unfolding PR_CONST_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (hm_decrease_key_op, mop_pm_decrease_key prio) \<in> Id \<rightarrow> Id \<rightarrow> heapmap_rel \<rightarrow> \<langle>heapmap_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 ab a'b. \<lbrakk>(a, a') \<in> Id; (aa, a'a) \<in> Id; (ab, a'b) \<in> heapmap_rel\<rbrakk> \<Longrightarrow> hm_decrease_key_op a aa ab \<le> \<Down> heapmap_rel (mop_pm_decrease_key prio a' a'a a'b)
[PROOF STEP]
apply (frule heapmap_hmr_relI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' aa a'a ab a'b. \<lbrakk>(a, a') \<in> Id; (aa, a'a) \<in> Id; (ab, a'b) \<in> heapmap_rel; (ab, hmr_\<alpha> ab) \<in> hmr_rel\<rbrakk> \<Longrightarrow> hm_decrease_key_op a aa ab \<le> \<Down> heapmap_rel (mop_pm_decrease_key prio a' a'a a'b)
[PROOF STEP]
unfolding mop_pm_decrease_key_alt
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' aa a'a ab a'b. \<lbrakk>(a, a') \<in> Id; (aa, a'a) \<in> Id; (ab, a'b) \<in> heapmap_rel; (ab, hmr_\<alpha> ab) \<in> hmr_rel\<rbrakk> \<Longrightarrow> hm_decrease_key_op a aa ab \<le> \<Down> heapmap_rel (ASSERT (pre_pm_decrease_key prio ((a', a'a), a'b)) \<bind> (\<lambda>_. RETURN (op_pm_decrease_key a' a'a a'b)))
[PROOF STEP]
apply (rule ASSERT_refine_right; clarsimp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a' a'a ab b a'b y. \<lbrakk>((ab, b), a'b) \<in> heapmap_rel; ((ab, b), hmr_\<alpha> (ab, b)) \<in> hmr_rel; prio a'a \<le> prio y; a'b a' = Some y\<rbrakk> \<Longrightarrow> hm_decrease_key_op a' a'a (ab, b) \<le> \<Down> heapmap_rel (RETURN (a'b(a' \<mapsto> a'a)))
[PROOF STEP]
apply (rule heapmap_nres_relI')
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a' a'a ab b a'b y. \<lbrakk>((ab, b), a'b) \<in> heapmap_rel; ((ab, b), hmr_\<alpha> (ab, b)) \<in> hmr_rel; prio a'a \<le> prio y; a'b a' = Some y\<rbrakk> \<Longrightarrow> hm_decrease_key_op a' a'a (ab, b) \<le> \<Down> hmr_rel (?h'18 a' a'a ab b a'b y)
 2. \<And>a' a'a ab b a'b y. \<lbrakk>((ab, b), a'b) \<in> heapmap_rel; ((ab, b), hmr_\<alpha> (ab, b)) \<in> hmr_rel; prio a'a \<le> prio y; a'b a' = Some y\<rbrakk> \<Longrightarrow> ?h'18 a' a'a ab b a'b y \<le> SPEC h.heap_invar
 3. \<And>a' a'a ab b a'b y. \<lbrakk>((ab, b), a'b) \<in> heapmap_rel; ((ab, b), hmr_\<alpha> (ab, b)) \<in> hmr_rel; prio a'a \<le> prio y; a'b a' = Some y\<rbrakk> \<Longrightarrow> hm_decrease_key_op a' a'a (ab, b) \<le>\<^sub>n SPEC (\<lambda>hm'. RETURN (heapmap_\<alpha> hm') \<le> RETURN (a'b(a' \<mapsto> a'a)))
[PROOF STEP]
apply (rule hm_decrease_key_op_refine; assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a' a'a ab b a'b y. \<lbrakk>((ab, b), a'b) \<in> heapmap_rel; ((ab, b), hmr_\<alpha> (ab, b)) \<in> hmr_rel; prio a'a \<le> prio y; a'b a' = Some y\<rbrakk> \<Longrightarrow> h.decrease_key_op (hm_index (ab, b) a') a'a (hmr_\<alpha> (ab, b)) \<le> SPEC h.heap_invar
 2. \<And>a' a'a ab b a'b y. \<lbrakk>((ab, b), a'b) \<in> heapmap_rel; ((ab, b), hmr_\<alpha> (ab, b)) \<in> hmr_rel; prio a'a \<le> prio y; a'b a' = Some y\<rbrakk> \<Longrightarrow> hm_decrease_key_op a' a'a (ab, b) \<le>\<^sub>n SPEC (\<lambda>hm'. RETURN (heapmap_\<alpha> hm') \<le> RETURN (a'b(a' \<mapsto> a'a)))
[PROOF STEP]
unfolding heapmap_rel_def hmr_rel_def in_br_conv
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a' a'a ab b a'b y. \<lbrakk>a'b = heapmap_\<alpha> (ab, b) \<and> heapmap_invar (ab, b); hmr_\<alpha> (ab, b) = hmr_\<alpha> (ab, b) \<and> hmr_invar (ab, b); prio a'a \<le> prio y; a'b a' = Some y\<rbrakk> \<Longrightarrow> h.decrease_key_op (hm_index (ab, b) a') a'a (hmr_\<alpha> (ab, b)) \<le> SPEC h.heap_invar
 2. \<And>a' a'a ab b a'b y. \<lbrakk>a'b = heapmap_\<alpha> (ab, b) \<and> heapmap_invar (ab, b); hmr_\<alpha> (ab, b) = hmr_\<alpha> (ab, b) \<and> hmr_invar (ab, b); prio a'a \<le> prio y; a'b a' = Some y\<rbrakk> \<Longrightarrow> hm_decrease_key_op a' a'a (ab, b) \<le>\<^sub>n SPEC (\<lambda>hm'. RETURN (heapmap_\<alpha> hm') \<le> RETURN (a'b(a' \<mapsto> a'a)))
[PROOF STEP]
apply (rule h.decrease_key_op_invar; simp; fail )
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a' a'a ab b a'b y. \<lbrakk>a'b = heapmap_\<alpha> (ab, b) \<and> heapmap_invar (ab, b); hmr_\<alpha> (ab, b) = hmr_\<alpha> (ab, b) \<and> hmr_invar (ab, b); prio a'a \<le> prio y; a'b a' = Some y\<rbrakk> \<Longrightarrow> hm_decrease_key_op a' a'a (ab, b) \<le>\<^sub>n SPEC (\<lambda>hm'. RETURN (heapmap_\<alpha> hm') \<le> RETURN (a'b(a' \<mapsto> a'a)))
[PROOF STEP]
apply (refine_vcg hm_decrease_key_op_\<alpha>_correct[THEN leof_trans]; simp; fail)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in heapstruct) increase_key_op_invar:
      "\<lbrakk>heap_invar h; valid h i; prio v \<ge> prio_of h i\<rbrakk> \<Longrightarrow> increase_key_op i v h \<le> SPEC heap_invar"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_invar h; valid h i; prio_of h i \<le> prio v\<rbrakk> \<Longrightarrow> increase_key_op i v h \<le> SPEC heap_invar
[PROOF STEP]
unfolding increase_key_op_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_invar h; valid h i; prio_of h i \<le> prio v\<rbrakk> \<Longrightarrow> ASSERT (valid h i \<and> prio_of h i \<le> prio v) \<bind> (\<lambda>_. update_op h i v \<bind> (\<lambda>h. sink_op h i)) \<le> SPEC heap_invar
[PROOF STEP]
apply refine_vcg
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>heap_invar h; valid h i; prio_of h i \<le> prio v; valid h i \<and> prio_of h i \<le> prio v; x = update h i v\<rbrakk> \<Longrightarrow> sink_invar x i
 2. \<And>x xa. \<lbrakk>heap_invar h; valid h i; prio_of h i \<le> prio v; valid h i \<and> prio_of h i \<le> prio v; x = update h i v; \<alpha> xa = \<alpha> x \<and> heap_invar xa \<and> length xa = length x\<rbrakk> \<Longrightarrow> heap_invar xa
[PROOF STEP]
by (auto simp: sink_invar_incr)


[STATEMENT]
lemma hm_increase_key_op_refine:
      "\<lbrakk>(hm,h)\<in>hmr_rel; (hm,m)\<in>heapmap_rel; m k = Some v'\<rbrakk>
        \<Longrightarrow> hm_increase_key_op k v hm \<le>\<Down>hmr_rel (h.increase_key_op (hm_index hm k) v h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(hm, h) \<in> hmr_rel; (hm, m) \<in> heapmap_rel; m k = Some v'\<rbrakk> \<Longrightarrow> hm_increase_key_op k v hm \<le> \<Down> hmr_rel (h.increase_key_op (hm_index hm k) v h)
[PROOF STEP]
unfolding hm_increase_key_op_def h.increase_key_op_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(hm, h) \<in> hmr_rel; (hm, m) \<in> heapmap_rel; m k = Some v'\<rbrakk> \<Longrightarrow> ASSERT (heapmap_invar hm) \<bind> (\<lambda>_. ASSERT (heapmap_\<alpha> hm k \<noteq> None \<and> prio (the (heapmap_\<alpha> hm k)) \<le> prio v) \<bind> (\<lambda>_. hm_index_op hm k \<bind> (\<lambda>i. hm_update_op hm i v \<bind> (\<lambda>hm. hm_sink_op hm i)))) \<le> \<Down> hmr_rel (ASSERT (h.valid h (hm_index hm k) \<and> h.prio_of h (hm_index hm k) \<le> prio v) \<bind> (\<lambda>_. h.update_op h (hm_index hm k) v \<bind> (\<lambda>h. h.sink_op h (hm_index hm k))))
[PROOF STEP]
(*apply (rewrite at "Let (hm_index hm k) _" Let_def)*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(hm, h) \<in> hmr_rel; (hm, m) \<in> heapmap_rel; m k = Some v'\<rbrakk> \<Longrightarrow> ASSERT (heapmap_invar hm) \<bind> (\<lambda>_. ASSERT (heapmap_\<alpha> hm k \<noteq> None \<and> prio (the (heapmap_\<alpha> hm k)) \<le> prio v) \<bind> (\<lambda>_. hm_index_op hm k \<bind> (\<lambda>i. hm_update_op hm i v \<bind> (\<lambda>hm. hm_sink_op hm i)))) \<le> \<Down> hmr_rel (ASSERT (h.valid h (hm_index hm k) \<and> h.prio_of h (hm_index hm k) \<le> prio v) \<bind> (\<lambda>_. h.update_op h (hm_index hm k) v \<bind> (\<lambda>h. h.sink_op h (hm_index hm k))))
[PROOF STEP]
apply (refine_rcg index_op_inline_refine)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<lbrakk>(hm, h) \<in> hmr_rel; (hm, m) \<in> heapmap_rel; m k = Some v'; h.valid h (hm_index hm k) \<and> h.prio_of h (hm_index hm k) \<le> prio v\<rbrakk> \<Longrightarrow> heapmap_invar hm
 2. \<lbrakk>(hm, h) \<in> hmr_rel; (hm, m) \<in> heapmap_rel; m k = Some v'; h.valid h (hm_index hm k) \<and> h.prio_of h (hm_index hm k) \<le> prio v; heapmap_invar hm\<rbrakk> \<Longrightarrow> heapmap_\<alpha> hm k \<noteq> None
 3. \<lbrakk>(hm, h) \<in> hmr_rel; (hm, m) \<in> heapmap_rel; m k = Some v'; h.valid h (hm_index hm k) \<and> h.prio_of h (hm_index hm k) \<le> prio v; heapmap_invar hm\<rbrakk> \<Longrightarrow> prio (the (heapmap_\<alpha> hm k)) \<le> prio v
 4. \<lbrakk>(hm, h) \<in> hmr_rel; (hm, m) \<in> heapmap_rel; m k = Some v'; h.valid h (hm_index hm k) \<and> h.prio_of h (hm_index hm k) \<le> prio v; heapmap_invar hm; heapmap_\<alpha> hm k \<noteq> None \<and> prio (the (heapmap_\<alpha> hm k)) \<le> prio v\<rbrakk> \<Longrightarrow> heapmap_\<alpha> hm k \<noteq> None
 5. \<lbrakk>(hm, h) \<in> hmr_rel; (hm, m) \<in> heapmap_rel; m k = Some v'; h.valid h (hm_index hm k) \<and> h.prio_of h (hm_index hm k) \<le> prio v; heapmap_invar hm; heapmap_\<alpha> hm k \<noteq> None \<and> prio (the (heapmap_\<alpha> hm k)) \<le> prio v\<rbrakk> \<Longrightarrow> (hm_index hm k, hm_index hm k) \<in> nat_rel
 6. \<lbrakk>(hm, h) \<in> hmr_rel; (hm, m) \<in> heapmap_rel; m k = Some v'; h.valid h (hm_index hm k) \<and> h.prio_of h (hm_index hm k) \<le> prio v; heapmap_invar hm; heapmap_\<alpha> hm k \<noteq> None \<and> prio (the (heapmap_\<alpha> hm k)) \<le> prio v\<rbrakk> \<Longrightarrow> (v, v) \<in> Id
 7. \<And>hma ha. \<lbrakk>(hm, h) \<in> hmr_rel; (hm, m) \<in> heapmap_rel; m k = Some v'; h.valid h (hm_index hm k) \<and> h.prio_of h (hm_index hm k) \<le> prio v; heapmap_invar hm; heapmap_\<alpha> hm k \<noteq> None \<and> prio (the (heapmap_\<alpha> hm k)) \<le> prio v; (hma, ha) \<in> hmr_rel\<rbrakk> \<Longrightarrow> (hm_index hm k, hm_index hm k) \<in> nat_rel
[PROOF STEP]
unfolding hmr_rel_def heapmap_rel_def in_br_conv
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<lbrakk>h = hmr_\<alpha> hm \<and> hmr_invar hm; m = heapmap_\<alpha> hm \<and> heapmap_invar hm; m k = Some v'; h.valid h (hm_index hm k) \<and> h.prio_of h (hm_index hm k) \<le> prio v\<rbrakk> \<Longrightarrow> heapmap_invar hm
 2. \<lbrakk>h = hmr_\<alpha> hm \<and> hmr_invar hm; m = heapmap_\<alpha> hm \<and> heapmap_invar hm; m k = Some v'; h.valid h (hm_index hm k) \<and> h.prio_of h (hm_index hm k) \<le> prio v; heapmap_invar hm\<rbrakk> \<Longrightarrow> heapmap_\<alpha> hm k \<noteq> None
 3. \<lbrakk>h = hmr_\<alpha> hm \<and> hmr_invar hm; m = heapmap_\<alpha> hm \<and> heapmap_invar hm; m k = Some v'; h.valid h (hm_index hm k) \<and> h.prio_of h (hm_index hm k) \<le> prio v; heapmap_invar hm\<rbrakk> \<Longrightarrow> prio (the (heapmap_\<alpha> hm k)) \<le> prio v
 4. \<lbrakk>h = hmr_\<alpha> hm \<and> hmr_invar hm; m = heapmap_\<alpha> hm \<and> heapmap_invar hm; m k = Some v'; h.valid h (hm_index hm k) \<and> h.prio_of h (hm_index hm k) \<le> prio v; heapmap_invar hm; heapmap_\<alpha> hm k \<noteq> None \<and> prio (the (heapmap_\<alpha> hm k)) \<le> prio v\<rbrakk> \<Longrightarrow> heapmap_\<alpha> hm k \<noteq> None
 5. \<lbrakk>h = hmr_\<alpha> hm \<and> hmr_invar hm; m = heapmap_\<alpha> hm \<and> heapmap_invar hm; m k = Some v'; h.valid h (hm_index hm k) \<and> h.prio_of h (hm_index hm k) \<le> prio v; heapmap_invar hm; heapmap_\<alpha> hm k \<noteq> None \<and> prio (the (heapmap_\<alpha> hm k)) \<le> prio v\<rbrakk> \<Longrightarrow> (hm_index hm k, hm_index hm k) \<in> nat_rel
 6. \<lbrakk>h = hmr_\<alpha> hm \<and> hmr_invar hm; m = heapmap_\<alpha> hm \<and> heapmap_invar hm; m k = Some v'; h.valid h (hm_index hm k) \<and> h.prio_of h (hm_index hm k) \<le> prio v; heapmap_invar hm; heapmap_\<alpha> hm k \<noteq> None \<and> prio (the (heapmap_\<alpha> hm k)) \<le> prio v\<rbrakk> \<Longrightarrow> (v, v) \<in> Id
 7. \<And>hma ha. \<lbrakk>h = hmr_\<alpha> hm \<and> hmr_invar hm; m = heapmap_\<alpha> hm \<and> heapmap_invar hm; m k = Some v'; h.valid h (hm_index hm k) \<and> h.prio_of h (hm_index hm k) \<le> prio v; heapmap_invar hm; heapmap_\<alpha> hm k \<noteq> None \<and> prio (the (heapmap_\<alpha> hm k)) \<le> prio v; ha = hmr_\<alpha> hma \<and> hmr_invar hma\<rbrakk> \<Longrightarrow> (hm_index hm k, hm_index hm k) \<in> nat_rel
[PROOF STEP]
apply (clarsimp_all)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma hm_increase_key_op_\<alpha>_correct:
      "heapmap_invar hm \<Longrightarrow> hm_increase_key_op k v hm \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm(k\<mapsto>v))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. heapmap_invar hm \<Longrightarrow> hm_increase_key_op k v hm \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm(k \<mapsto> v))
[PROOF STEP]
unfolding hm_increase_key_op_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. heapmap_invar hm \<Longrightarrow> ASSERT (heapmap_invar hm) \<bind> (\<lambda>_. ASSERT (heapmap_\<alpha> hm k \<noteq> None \<and> prio (the (heapmap_\<alpha> hm k)) \<le> prio v) \<bind> (\<lambda>_. hm_index_op hm k \<bind> (\<lambda>i. hm_update_op hm i v \<bind> (\<lambda>hm. hm_sink_op hm i)))) \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm(k \<mapsto> v))
[PROOF STEP]
apply (refine_vcg
        hm_update_op_\<alpha>_correct[THEN leof_trans]
        hm_sink_op_\<alpha>_correct[THEN leof_trans]
        hm_index_op_inline_leof)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>heapmap_invar hm; heapmap_invar hm; heapmap_\<alpha> hm k \<noteq> None \<and> prio (the (heapmap_\<alpha> hm k)) \<le> prio v\<rbrakk> \<Longrightarrow> hmr_invar hm
 2. \<lbrakk>heapmap_invar hm; heapmap_invar hm; heapmap_\<alpha> hm k \<noteq> None \<and> prio (the (heapmap_\<alpha> hm k)) \<le> prio v\<rbrakk> \<Longrightarrow> heapmap_\<alpha> hm k \<noteq> None
 3. \<And>x xa. \<lbrakk>heapmap_invar hm; heapmap_invar hm; heapmap_\<alpha> hm k \<noteq> None \<and> prio (the (heapmap_\<alpha> hm k)) \<le> prio v; x \<in> {hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm(k \<mapsto> v)}; xa \<in> {hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> x}\<rbrakk> \<Longrightarrow> heapmap_\<alpha> xa = heapmap_\<alpha> hm(k \<mapsto> v)
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma hm_increase_key_op_aref:
      "(hm_increase_key_op, PR_CONST (mop_pm_increase_key prio)) \<in> Id \<rightarrow> Id \<rightarrow> heapmap_rel \<rightarrow> \<langle>heapmap_rel\<rangle>nres_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (hm_increase_key_op, PR_CONST (mop_pm_increase_key prio)) \<in> Id \<rightarrow> Id \<rightarrow> heapmap_rel \<rightarrow> \<langle>heapmap_rel\<rangle>nres_rel
[PROOF STEP]
unfolding PR_CONST_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (hm_increase_key_op, mop_pm_increase_key prio) \<in> Id \<rightarrow> Id \<rightarrow> heapmap_rel \<rightarrow> \<langle>heapmap_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 ab a'b. \<lbrakk>(a, a') \<in> Id; (aa, a'a) \<in> Id; (ab, a'b) \<in> heapmap_rel\<rbrakk> \<Longrightarrow> hm_increase_key_op a aa ab \<le> \<Down> heapmap_rel (mop_pm_increase_key prio a' a'a a'b)
[PROOF STEP]
apply (frule heapmap_hmr_relI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' aa a'a ab a'b. \<lbrakk>(a, a') \<in> Id; (aa, a'a) \<in> Id; (ab, a'b) \<in> heapmap_rel; (ab, hmr_\<alpha> ab) \<in> hmr_rel\<rbrakk> \<Longrightarrow> hm_increase_key_op a aa ab \<le> \<Down> heapmap_rel (mop_pm_increase_key prio a' a'a a'b)
[PROOF STEP]
unfolding mop_pm_increase_key_alt
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' aa a'a ab a'b. \<lbrakk>(a, a') \<in> Id; (aa, a'a) \<in> Id; (ab, a'b) \<in> heapmap_rel; (ab, hmr_\<alpha> ab) \<in> hmr_rel\<rbrakk> \<Longrightarrow> hm_increase_key_op a aa ab \<le> \<Down> heapmap_rel (ASSERT (pre_pm_increase_key prio ((a', a'a), a'b)) \<bind> (\<lambda>_. RETURN (op_pm_increase_key a' a'a a'b)))
[PROOF STEP]
apply (rule ASSERT_refine_right; clarsimp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a' a'a ab b a'b y. \<lbrakk>((ab, b), a'b) \<in> heapmap_rel; ((ab, b), hmr_\<alpha> (ab, b)) \<in> hmr_rel; prio y \<le> prio a'a; a'b a' = Some y\<rbrakk> \<Longrightarrow> hm_increase_key_op a' a'a (ab, b) \<le> \<Down> heapmap_rel (RETURN (a'b(a' \<mapsto> a'a)))
[PROOF STEP]
apply (rule heapmap_nres_relI')
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a' a'a ab b a'b y. \<lbrakk>((ab, b), a'b) \<in> heapmap_rel; ((ab, b), hmr_\<alpha> (ab, b)) \<in> hmr_rel; prio y \<le> prio a'a; a'b a' = Some y\<rbrakk> \<Longrightarrow> hm_increase_key_op a' a'a (ab, b) \<le> \<Down> hmr_rel (?h'18 a' a'a ab b a'b y)
 2. \<And>a' a'a ab b a'b y. \<lbrakk>((ab, b), a'b) \<in> heapmap_rel; ((ab, b), hmr_\<alpha> (ab, b)) \<in> hmr_rel; prio y \<le> prio a'a; a'b a' = Some y\<rbrakk> \<Longrightarrow> ?h'18 a' a'a ab b a'b y \<le> SPEC h.heap_invar
 3. \<And>a' a'a ab b a'b y. \<lbrakk>((ab, b), a'b) \<in> heapmap_rel; ((ab, b), hmr_\<alpha> (ab, b)) \<in> hmr_rel; prio y \<le> prio a'a; a'b a' = Some y\<rbrakk> \<Longrightarrow> hm_increase_key_op a' a'a (ab, b) \<le>\<^sub>n SPEC (\<lambda>hm'. RETURN (heapmap_\<alpha> hm') \<le> RETURN (a'b(a' \<mapsto> a'a)))
[PROOF STEP]
apply (rule hm_increase_key_op_refine; assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a' a'a ab b a'b y. \<lbrakk>((ab, b), a'b) \<in> heapmap_rel; ((ab, b), hmr_\<alpha> (ab, b)) \<in> hmr_rel; prio y \<le> prio a'a; a'b a' = Some y\<rbrakk> \<Longrightarrow> h.increase_key_op (hm_index (ab, b) a') a'a (hmr_\<alpha> (ab, b)) \<le> SPEC h.heap_invar
 2. \<And>a' a'a ab b a'b y. \<lbrakk>((ab, b), a'b) \<in> heapmap_rel; ((ab, b), hmr_\<alpha> (ab, b)) \<in> hmr_rel; prio y \<le> prio a'a; a'b a' = Some y\<rbrakk> \<Longrightarrow> hm_increase_key_op a' a'a (ab, b) \<le>\<^sub>n SPEC (\<lambda>hm'. RETURN (heapmap_\<alpha> hm') \<le> RETURN (a'b(a' \<mapsto> a'a)))
[PROOF STEP]
unfolding heapmap_rel_def hmr_rel_def in_br_conv
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a' a'a ab b a'b y. \<lbrakk>a'b = heapmap_\<alpha> (ab, b) \<and> heapmap_invar (ab, b); hmr_\<alpha> (ab, b) = hmr_\<alpha> (ab, b) \<and> hmr_invar (ab, b); prio y \<le> prio a'a; a'b a' = Some y\<rbrakk> \<Longrightarrow> h.increase_key_op (hm_index (ab, b) a') a'a (hmr_\<alpha> (ab, b)) \<le> SPEC h.heap_invar
 2. \<And>a' a'a ab b a'b y. \<lbrakk>a'b = heapmap_\<alpha> (ab, b) \<and> heapmap_invar (ab, b); hmr_\<alpha> (ab, b) = hmr_\<alpha> (ab, b) \<and> hmr_invar (ab, b); prio y \<le> prio a'a; a'b a' = Some y\<rbrakk> \<Longrightarrow> hm_increase_key_op a' a'a (ab, b) \<le>\<^sub>n SPEC (\<lambda>hm'. RETURN (heapmap_\<alpha> hm') \<le> RETURN (a'b(a' \<mapsto> a'a)))
[PROOF STEP]
apply (rule h.increase_key_op_invar; simp; fail )
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a' a'a ab b a'b y. \<lbrakk>a'b = heapmap_\<alpha> (ab, b) \<and> heapmap_invar (ab, b); hmr_\<alpha> (ab, b) = hmr_\<alpha> (ab, b) \<and> hmr_invar (ab, b); prio y \<le> prio a'a; a'b a' = Some y\<rbrakk> \<Longrightarrow> hm_increase_key_op a' a'a (ab, b) \<le>\<^sub>n SPEC (\<lambda>hm'. RETURN (heapmap_\<alpha> hm') \<le> RETURN (a'b(a' \<mapsto> a'a)))
[PROOF STEP]
apply (refine_vcg hm_increase_key_op_\<alpha>_correct[THEN leof_trans]; simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in heapstruct) change_key_op_invar:
      "\<lbrakk>heap_invar h; valid h i\<rbrakk> \<Longrightarrow> change_key_op i v h \<le> SPEC heap_invar"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_invar h; valid h i\<rbrakk> \<Longrightarrow> change_key_op i v h \<le> SPEC heap_invar
[PROOF STEP]
unfolding change_key_op_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_invar h; valid h i\<rbrakk> \<Longrightarrow> ASSERT (valid h i) \<bind> (\<lambda>_. update_op h i v \<bind> (\<lambda>h. repair_op h i)) \<le> SPEC heap_invar
[PROOF STEP]
apply (refine_vcg)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>heap_invar h; valid h i; valid h i; x = update h i v\<rbrakk> \<Longrightarrow> repair_op x i \<le> SPEC heap_invar
[PROOF STEP]
apply hypsubst
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>heap_invar h; valid h i; valid h i\<rbrakk> \<Longrightarrow> repair_op (update h i v) i \<le> SPEC heap_invar
[PROOF STEP]
apply refine_vcg
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>heap_invar h; valid h i; valid h i; heap_invar xa \<and> \<alpha> xa = \<alpha> (update h i v) \<and> length xa = length h\<rbrakk> \<Longrightarrow> heap_invar xa
[PROOF STEP]
by (auto simp: sink_invar_incr)


[STATEMENT]
lemma hm_change_key_op_refine:
      "\<lbrakk>(hm,h)\<in>hmr_rel; (hm,m)\<in>heapmap_rel; m k = Some v'\<rbrakk>
        \<Longrightarrow> hm_change_key_op k v hm \<le>\<Down>hmr_rel (h.change_key_op (hm_index hm k) v h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(hm, h) \<in> hmr_rel; (hm, m) \<in> heapmap_rel; m k = Some v'\<rbrakk> \<Longrightarrow> hm_change_key_op k v hm \<le> \<Down> hmr_rel (h.change_key_op (hm_index hm k) v h)
[PROOF STEP]
unfolding hm_change_key_op_def h.change_key_op_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(hm, h) \<in> hmr_rel; (hm, m) \<in> heapmap_rel; m k = Some v'\<rbrakk> \<Longrightarrow> ASSERT (heapmap_invar hm) \<bind> (\<lambda>_. ASSERT (heapmap_\<alpha> hm k \<noteq> None) \<bind> (\<lambda>_. hm_index_op hm k \<bind> (\<lambda>i. hm_update_op hm i v \<bind> (\<lambda>hm. hm_repair_op hm i)))) \<le> \<Down> hmr_rel (ASSERT (h.valid h (hm_index hm k)) \<bind> (\<lambda>_. h.update_op h (hm_index hm k) v \<bind> (\<lambda>h. h.repair_op h (hm_index hm k))))
[PROOF STEP]
(*apply (rewrite at "Let (hm_index hm k) _" Let_def)*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(hm, h) \<in> hmr_rel; (hm, m) \<in> heapmap_rel; m k = Some v'\<rbrakk> \<Longrightarrow> ASSERT (heapmap_invar hm) \<bind> (\<lambda>_. ASSERT (heapmap_\<alpha> hm k \<noteq> None) \<bind> (\<lambda>_. hm_index_op hm k \<bind> (\<lambda>i. hm_update_op hm i v \<bind> (\<lambda>hm. hm_repair_op hm i)))) \<le> \<Down> hmr_rel (ASSERT (h.valid h (hm_index hm k)) \<bind> (\<lambda>_. h.update_op h (hm_index hm k) v \<bind> (\<lambda>h. h.repair_op h (hm_index hm k))))
[PROOF STEP]
apply (refine_rcg index_op_inline_refine)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>(hm, h) \<in> hmr_rel; (hm, m) \<in> heapmap_rel; m k = Some v'; h.valid h (hm_index hm k)\<rbrakk> \<Longrightarrow> heapmap_invar hm
 2. \<lbrakk>(hm, h) \<in> hmr_rel; (hm, m) \<in> heapmap_rel; m k = Some v'; h.valid h (hm_index hm k); heapmap_invar hm\<rbrakk> \<Longrightarrow> heapmap_\<alpha> hm k \<noteq> None
 3. \<lbrakk>(hm, h) \<in> hmr_rel; (hm, m) \<in> heapmap_rel; m k = Some v'; h.valid h (hm_index hm k); heapmap_invar hm; heapmap_\<alpha> hm k \<noteq> None\<rbrakk> \<Longrightarrow> (hm_index hm k, hm_index hm k) \<in> nat_rel
 4. \<lbrakk>(hm, h) \<in> hmr_rel; (hm, m) \<in> heapmap_rel; m k = Some v'; h.valid h (hm_index hm k); heapmap_invar hm; heapmap_\<alpha> hm k \<noteq> None\<rbrakk> \<Longrightarrow> (v, v) \<in> Id
 5. \<And>hma ha. \<lbrakk>(hm, h) \<in> hmr_rel; (hm, m) \<in> heapmap_rel; m k = Some v'; h.valid h (hm_index hm k); heapmap_invar hm; heapmap_\<alpha> hm k \<noteq> None; (hma, ha) \<in> hmr_rel\<rbrakk> \<Longrightarrow> (hm_index hm k, hm_index hm k) \<in> nat_rel
[PROOF STEP]
unfolding hmr_rel_def heapmap_rel_def in_br_conv
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>h = hmr_\<alpha> hm \<and> hmr_invar hm; m = heapmap_\<alpha> hm \<and> heapmap_invar hm; m k = Some v'; h.valid h (hm_index hm k)\<rbrakk> \<Longrightarrow> heapmap_invar hm
 2. \<lbrakk>h = hmr_\<alpha> hm \<and> hmr_invar hm; m = heapmap_\<alpha> hm \<and> heapmap_invar hm; m k = Some v'; h.valid h (hm_index hm k); heapmap_invar hm\<rbrakk> \<Longrightarrow> heapmap_\<alpha> hm k \<noteq> None
 3. \<lbrakk>h = hmr_\<alpha> hm \<and> hmr_invar hm; m = heapmap_\<alpha> hm \<and> heapmap_invar hm; m k = Some v'; h.valid h (hm_index hm k); heapmap_invar hm; heapmap_\<alpha> hm k \<noteq> None\<rbrakk> \<Longrightarrow> (hm_index hm k, hm_index hm k) \<in> nat_rel
 4. \<lbrakk>h = hmr_\<alpha> hm \<and> hmr_invar hm; m = heapmap_\<alpha> hm \<and> heapmap_invar hm; m k = Some v'; h.valid h (hm_index hm k); heapmap_invar hm; heapmap_\<alpha> hm k \<noteq> None\<rbrakk> \<Longrightarrow> (v, v) \<in> Id
 5. \<And>hma ha. \<lbrakk>h = hmr_\<alpha> hm \<and> hmr_invar hm; m = heapmap_\<alpha> hm \<and> heapmap_invar hm; m k = Some v'; h.valid h (hm_index hm k); heapmap_invar hm; heapmap_\<alpha> hm k \<noteq> None; ha = hmr_\<alpha> hma \<and> hmr_invar hma\<rbrakk> \<Longrightarrow> (hm_index hm k, hm_index hm k) \<in> nat_rel
[PROOF STEP]
apply (clarsimp_all)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma hm_change_key_op_\<alpha>_correct:
      "heapmap_invar hm \<Longrightarrow> hm_change_key_op k v hm \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm(k\<mapsto>v))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. heapmap_invar hm \<Longrightarrow> hm_change_key_op k v hm \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm(k \<mapsto> v))
[PROOF STEP]
unfolding hm_change_key_op_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. heapmap_invar hm \<Longrightarrow> ASSERT (heapmap_invar hm) \<bind> (\<lambda>_. ASSERT (heapmap_\<alpha> hm k \<noteq> None) \<bind> (\<lambda>_. hm_index_op hm k \<bind> (\<lambda>i. hm_update_op hm i v \<bind> (\<lambda>hm. hm_repair_op hm i)))) \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm(k \<mapsto> v))
[PROOF STEP]
apply (refine_vcg
        hm_update_op_\<alpha>_correct[THEN leof_trans]
        hm_repair_op_\<alpha>_correct[THEN leof_trans]
        hm_index_op_inline_leof)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>heapmap_invar hm; heapmap_invar hm; heapmap_\<alpha> hm k \<noteq> None\<rbrakk> \<Longrightarrow> hmr_invar hm
 2. \<And>x xa. \<lbrakk>heapmap_invar hm; heapmap_invar hm; heapmap_\<alpha> hm k \<noteq> None; x \<in> {hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm(k \<mapsto> v)}; xa \<in> {hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> x}\<rbrakk> \<Longrightarrow> heapmap_\<alpha> xa = heapmap_\<alpha> hm(k \<mapsto> v)
[PROOF STEP]
unfolding heapmap_rel_def in_br_conv
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>heapmap_invar hm; heapmap_invar hm; heapmap_\<alpha> hm k \<noteq> None\<rbrakk> \<Longrightarrow> hmr_invar hm
 2. \<And>x xa. \<lbrakk>heapmap_invar hm; heapmap_invar hm; heapmap_\<alpha> hm k \<noteq> None; x \<in> {hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm(k \<mapsto> v)}; xa \<in> {hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> x}\<rbrakk> \<Longrightarrow> heapmap_\<alpha> xa = heapmap_\<alpha> hm(k \<mapsto> v)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>heapmap_invar hm; heapmap_invar hm; heapmap_\<alpha> hm k \<noteq> None; x \<in> {hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm(k \<mapsto> v)}; xa \<in> {hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> x}\<rbrakk> \<Longrightarrow> heapmap_\<alpha> xa = heapmap_\<alpha> hm(k \<mapsto> v)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma hm_change_key_op_aref:
      "(hm_change_key_op, mop_map_update_ex) \<in> Id \<rightarrow> Id \<rightarrow> heapmap_rel \<rightarrow> \<langle>heapmap_rel\<rangle>nres_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (hm_change_key_op, mop_map_update_ex) \<in> Id \<rightarrow> Id \<rightarrow> heapmap_rel \<rightarrow> \<langle>heapmap_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 ab a'b. \<lbrakk>(a, a') \<in> Id; (aa, a'a) \<in> Id; (ab, a'b) \<in> heapmap_rel\<rbrakk> \<Longrightarrow> hm_change_key_op a aa ab \<le> \<Down> heapmap_rel (mop_map_update_ex a' a'a a'b)
[PROOF STEP]
apply (frule heapmap_hmr_relI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' aa a'a ab a'b. \<lbrakk>(a, a') \<in> Id; (aa, a'a) \<in> Id; (ab, a'b) \<in> heapmap_rel; (ab, hmr_\<alpha> ab) \<in> hmr_rel\<rbrakk> \<Longrightarrow> hm_change_key_op a aa ab \<le> \<Down> heapmap_rel (mop_map_update_ex a' a'a a'b)
[PROOF STEP]
unfolding mop_map_update_ex_alt
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' aa a'a ab a'b. \<lbrakk>(a, a') \<in> Id; (aa, a'a) \<in> Id; (ab, a'b) \<in> heapmap_rel; (ab, hmr_\<alpha> ab) \<in> hmr_rel\<rbrakk> \<Longrightarrow> hm_change_key_op a aa ab \<le> \<Down> heapmap_rel (ASSERT (pre_map_update_ex ((a', a'a), a'b)) \<bind> (\<lambda>_. RETURN (op_map_update_ex a' a'a a'b)))
[PROOF STEP]
apply (rule ASSERT_refine_right; clarsimp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a' a'a ab b a'b y. \<lbrakk>((ab, b), a'b) \<in> heapmap_rel; ((ab, b), hmr_\<alpha> (ab, b)) \<in> hmr_rel; a'b a' = Some y\<rbrakk> \<Longrightarrow> hm_change_key_op a' a'a (ab, b) \<le> \<Down> heapmap_rel (RETURN (a'b(a' \<mapsto> a'a)))
[PROOF STEP]
apply (rule heapmap_nres_relI')
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a' a'a ab b a'b y. \<lbrakk>((ab, b), a'b) \<in> heapmap_rel; ((ab, b), hmr_\<alpha> (ab, b)) \<in> hmr_rel; a'b a' = Some y\<rbrakk> \<Longrightarrow> hm_change_key_op a' a'a (ab, b) \<le> \<Down> hmr_rel (?h'17 a' a'a ab b a'b y)
 2. \<And>a' a'a ab b a'b y. \<lbrakk>((ab, b), a'b) \<in> heapmap_rel; ((ab, b), hmr_\<alpha> (ab, b)) \<in> hmr_rel; a'b a' = Some y\<rbrakk> \<Longrightarrow> ?h'17 a' a'a ab b a'b y \<le> SPEC h.heap_invar
 3. \<And>a' a'a ab b a'b y. \<lbrakk>((ab, b), a'b) \<in> heapmap_rel; ((ab, b), hmr_\<alpha> (ab, b)) \<in> hmr_rel; a'b a' = Some y\<rbrakk> \<Longrightarrow> hm_change_key_op a' a'a (ab, b) \<le>\<^sub>n SPEC (\<lambda>hm'. RETURN (heapmap_\<alpha> hm') \<le> RETURN (a'b(a' \<mapsto> a'a)))
[PROOF STEP]
apply (rule hm_change_key_op_refine; assumption)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a' a'a ab b a'b y. \<lbrakk>((ab, b), a'b) \<in> heapmap_rel; ((ab, b), hmr_\<alpha> (ab, b)) \<in> hmr_rel; a'b a' = Some y\<rbrakk> \<Longrightarrow> h.change_key_op (hm_index (ab, b) a') a'a (hmr_\<alpha> (ab, b)) \<le> SPEC h.heap_invar
 2. \<And>a' a'a ab b a'b y. \<lbrakk>((ab, b), a'b) \<in> heapmap_rel; ((ab, b), hmr_\<alpha> (ab, b)) \<in> hmr_rel; a'b a' = Some y\<rbrakk> \<Longrightarrow> hm_change_key_op a' a'a (ab, b) \<le>\<^sub>n SPEC (\<lambda>hm'. RETURN (heapmap_\<alpha> hm') \<le> RETURN (a'b(a' \<mapsto> a'a)))
[PROOF STEP]
unfolding heapmap_rel_def hmr_rel_def in_br_conv
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a' a'a ab b a'b y. \<lbrakk>a'b = heapmap_\<alpha> (ab, b) \<and> heapmap_invar (ab, b); hmr_\<alpha> (ab, b) = hmr_\<alpha> (ab, b) \<and> hmr_invar (ab, b); a'b a' = Some y\<rbrakk> \<Longrightarrow> h.change_key_op (hm_index (ab, b) a') a'a (hmr_\<alpha> (ab, b)) \<le> SPEC h.heap_invar
 2. \<And>a' a'a ab b a'b y. \<lbrakk>a'b = heapmap_\<alpha> (ab, b) \<and> heapmap_invar (ab, b); hmr_\<alpha> (ab, b) = hmr_\<alpha> (ab, b) \<and> hmr_invar (ab, b); a'b a' = Some y\<rbrakk> \<Longrightarrow> hm_change_key_op a' a'a (ab, b) \<le>\<^sub>n SPEC (\<lambda>hm'. RETURN (heapmap_\<alpha> hm') \<le> RETURN (a'b(a' \<mapsto> a'a)))
[PROOF STEP]
apply (rule h.change_key_op_invar; simp; fail )
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a' a'a ab b a'b y. \<lbrakk>a'b = heapmap_\<alpha> (ab, b) \<and> heapmap_invar (ab, b); hmr_\<alpha> (ab, b) = hmr_\<alpha> (ab, b) \<and> hmr_invar (ab, b); a'b a' = Some y\<rbrakk> \<Longrightarrow> hm_change_key_op a' a'a (ab, b) \<le>\<^sub>n SPEC (\<lambda>hm'. RETURN (heapmap_\<alpha> hm') \<le> RETURN (a'b(a' \<mapsto> a'a)))
[PROOF STEP]
apply ((refine_vcg hm_change_key_op_\<alpha>_correct[THEN leof_trans]; simp))
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in -) op_pm_set_gen_impl: "RETURN ooo op_map_update = (\<lambda>k v m. do {
      c \<leftarrow> RETURN (op_map_contains_key k m);
      if c then
        mop_map_update_ex k v m
      else
        mop_map_update_new k v m
    })"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. RETURN \<circ>\<circ>\<circ> op_map_update = (\<lambda>k v m. RETURN (op_map_contains_key k m) \<bind> (\<lambda>c. if c then mop_map_update_ex k v m else mop_map_update_new k v m))
[PROOF STEP]
apply (intro ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa m. (RETURN \<circ>\<circ>\<circ> op_map_update) x xa m = RETURN (op_map_contains_key x m) \<bind> (\<lambda>c. if c then mop_map_update_ex x xa m else mop_map_update_new x xa m)
[PROOF STEP]
unfolding op_map_contains_key_def mop_map_update_ex_def mop_map_update_new_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa m. (RETURN \<circ>\<circ>\<circ> op_map_update) x xa m = RETURN (x \<in> dom m) \<bind> (\<lambda>c. if c then curry2 (mop pre_map_update_ex (uncurry2 (RETURN \<circ>\<circ>\<circ> op_map_update_ex))) x xa m else curry2 (mop pre_map_update_new (uncurry2 (RETURN \<circ>\<circ>\<circ> op_map_update_new))) x xa m)
[PROOF STEP]
by simp


[STATEMENT]
lemma hm_set_op_aref:
      "(hm_set_op, RETURN ooo op_map_update) \<in> Id \<rightarrow> Id \<rightarrow> heapmap_rel \<rightarrow> \<langle>heapmap_rel\<rangle>nres_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (hm_set_op, RETURN \<circ>\<circ>\<circ> op_map_update) \<in> Id \<rightarrow> Id \<rightarrow> heapmap_rel \<rightarrow> \<langle>heapmap_rel\<rangle>nres_rel
[PROOF STEP]
unfolding op_pm_set_gen_impl
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (hm_set_op, \<lambda>k v m. RETURN (op_map_contains_key k m) \<bind> (\<lambda>c. if c then mop_map_update_ex k v m else mop_map_update_new k v m)) \<in> Id \<rightarrow> Id \<rightarrow> heapmap_rel \<rightarrow> \<langle>heapmap_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 ab a'b. \<lbrakk>(a, a') \<in> Id; (aa, a'a) \<in> Id; (ab, a'b) \<in> heapmap_rel\<rbrakk> \<Longrightarrow> hm_set_op a aa ab \<le> \<Down> heapmap_rel (RETURN (op_map_contains_key a' a'b) \<bind> (\<lambda>c. if c then mop_map_update_ex a' a'a a'b else mop_map_update_new a' a'a a'b))
[PROOF STEP]
unfolding hm_set_op_def o_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' aa a'a ab a'b. \<lbrakk>(a, a') \<in> Id; (aa, a'a) \<in> Id; (ab, a'b) \<in> heapmap_rel\<rbrakk> \<Longrightarrow> hm_contains_key_op a ab \<bind> (\<lambda>c. if c then hm_change_key_op a aa ab else hm_insert_op a aa ab) \<le> \<Down> heapmap_rel (RETURN (op_map_contains_key a' a'b) \<bind> (\<lambda>c. if c then mop_map_update_ex a' a'a a'b else mop_map_update_new a' a'a a'b))
[PROOF STEP]
apply (refine_rcg
        hm_contains_key_op_aref[param_fo, unfolded o_def, THEN nres_relD]
        hm_change_key_op_aref[param_fo, THEN nres_relD]
        hm_insert_op_aref[param_fo, THEN nres_relD]
        )
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' aa a'a ab a'b c ca. \<lbrakk>(a, a') \<in> Id; (aa, a'a) \<in> Id; (ab, a'b) \<in> heapmap_rel; (c, ca) \<in> bool_rel\<rbrakk> \<Longrightarrow> c = ca
[PROOF STEP]
by auto


[STATEMENT]
lemma hm_pop_min_op_refine:
      "(hm_pop_min_op, h.pop_min_op) \<in> hmr_rel \<rightarrow> \<langle>UNIV \<times>\<^sub>r hmr_rel\<rangle>nres_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (hm_pop_min_op, h.pop_min_op) \<in> hmr_rel \<rightarrow> \<langle>UNIV \<times>\<^sub>r hmr_rel\<rangle>nres_rel
[PROOF STEP]
apply (intro fun_relI nres_relI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a'. (a, a') \<in> hmr_rel \<Longrightarrow> hm_pop_min_op a \<le> \<Down> (UNIV \<times>\<^sub>r hmr_rel) (h.pop_min_op a')
[PROOF STEP]
unfolding hm_pop_min_op_def h.pop_min_op_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a'. (a, a') \<in> hmr_rel \<Longrightarrow> ASSERT (heapmap_invar a) \<bind> (\<lambda>_. ASSERT (hm_valid a 1) \<bind> (\<lambda>_. hm_key_of_op a 1 \<bind> (\<lambda>k. hm_the_lookup_op a k \<bind> (\<lambda>v. let l = hm_length a in hm_exch_op a 1 l \<bind> (\<lambda>hm. hm_butlast_op hm \<bind> (\<lambda>hm. if l \<noteq> 1 then hm_sink_op hm 1 \<bind> (\<lambda>hm. RETURN ((k, v), hm)) else RETURN ((k, v), hm))))))) \<le> \<Down> (UNIV \<times>\<^sub>r hmr_rel) (ASSERT (h.heap_invar a') \<bind> (\<lambda>_. ASSERT (h.valid a' 1) \<bind> (\<lambda>_. h.val_of_op a' 1 \<bind> (\<lambda>m. let l = length a' in h.exch_op a' 1 l \<bind> (\<lambda>h. h.butlast_op h \<bind> (\<lambda>h. if l \<noteq> 1 then h.sink_op h 1 \<bind> (\<lambda>h. RETURN (m, h)) else RETURN (m, h)))))))
[PROOF STEP]
(* Project away stuff of second component *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a'. (a, a') \<in> hmr_rel \<Longrightarrow> ASSERT (heapmap_invar a) \<bind> (\<lambda>_. ASSERT (hm_valid a 1) \<bind> (\<lambda>_. hm_key_of_op a 1 \<bind> (\<lambda>k. hm_the_lookup_op a k \<bind> (\<lambda>v. let l = hm_length a in hm_exch_op a 1 l \<bind> (\<lambda>hm. hm_butlast_op hm \<bind> (\<lambda>hm. if l \<noteq> 1 then hm_sink_op hm 1 \<bind> (\<lambda>hm. RETURN ((k, v), hm)) else RETURN ((k, v), hm))))))) \<le> \<Down> (UNIV \<times>\<^sub>r hmr_rel) (ASSERT (h.heap_invar a') \<bind> (\<lambda>_. ASSERT (h.valid a' 1) \<bind> (\<lambda>_. h.val_of_op a' 1 \<bind> (\<lambda>m. let l = length a' in h.exch_op a' 1 l \<bind> (\<lambda>h. h.butlast_op h \<bind> (\<lambda>h. if l \<noteq> 1 then h.sink_op h 1 \<bind> (\<lambda>h. RETURN (m, h)) else RETURN (m, h)))))))
[PROOF STEP]
unfolding ignore_snd_refine_conv hm_the_lookup_op_def hm_key_of_op_unfold
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a'. (a, a') \<in> hmr_rel \<Longrightarrow> ASSERT (heapmap_invar a) \<bind> (\<lambda>_. ASSERT (hm_valid a 1) \<bind> (\<lambda>_. ASSERT (hm_valid a 1) \<bind> (\<lambda>_. RETURN (hm_key_of a 1)) \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> a k \<noteq> None \<and> hmr_invar a) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> a k))) \<bind> (\<lambda>v. let l = hm_length a in hm_exch_op a 1 l \<bind> (\<lambda>hm. hm_butlast_op hm \<bind> (\<lambda>hm. if l \<noteq> 1 then hm_sink_op hm 1 \<bind> (\<lambda>hm. RETURN ((k, v), hm)) else RETURN ((k, v), hm))))))) \<le> \<Down> (UNIV \<times>\<^sub>r hmr_rel) (ASSERT (h.heap_invar a') \<bind> (\<lambda>_. ASSERT (h.valid a' 1) \<bind> (\<lambda>_. h.val_of_op a' 1 \<bind> (\<lambda>m. let l = length a' in h.exch_op a' 1 l \<bind> (\<lambda>h. h.butlast_op h \<bind> (\<lambda>h. if l \<noteq> 1 then h.sink_op h 1 \<bind> (\<lambda>h. RETURN (m, h)) else RETURN (m, h)))))))
[PROOF STEP]
apply (simp cong: if_cong add: Let_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a'. (a, a') \<in> hmr_rel \<Longrightarrow> ASSERT (heapmap_invar a) \<bind> (\<lambda>_. ASSERT (hm_valid a (Suc 0)) \<bind> (\<lambda>_. ASSERT (hm_valid a (Suc 0)) \<bind> (\<lambda>x. ASSERT ((\<exists>y. heapmap_\<alpha> a (hm_key_of a (Suc 0)) = Some y) \<and> hmr_invar a) \<bind> (\<lambda>x. hm_exch_op a (Suc 0) (hm_length a) \<bind> (\<lambda>hm. hm_butlast_op hm \<bind> (\<lambda>hm. if hm_length a = Suc 0 then RETURN ((hm_key_of a (Suc 0), the (heapmap_\<alpha> a (hm_key_of a (Suc 0)))), hm) else hm_sink_op hm (Suc 0) \<bind> (\<lambda>hm. RETURN ((hm_key_of a (Suc 0), the (heapmap_\<alpha> a (hm_key_of a (Suc 0)))), hm)))))))) \<le> \<Down> (UNIV \<times>\<^sub>r hmr_rel) (ASSERT (h.heap_invar a') \<bind> (\<lambda>_. ASSERT (h.valid a' (Suc 0)) \<bind> (\<lambda>_. h.val_of_op a' (Suc 0) \<bind> (\<lambda>m. h.exch_op a' (Suc 0) (length a') \<bind> (\<lambda>h. h.butlast_op h \<bind> (\<lambda>h. if length a' = Suc 0 then RETURN (m, h) else h.sink_op h (Suc 0) \<bind> (\<lambda>h. RETURN (m, h))))))))
[PROOF STEP]
apply (simp add: unused_bind_conv h.val_of_op_def refine_pw_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a'. (a, a') \<in> hmr_rel \<Longrightarrow> ASSERT (heapmap_invar a) \<bind> (\<lambda>_. ASSERT (hm_valid a (Suc 0)) \<bind> (\<lambda>_. ASSERT (hm_valid a (Suc 0)) \<bind> (\<lambda>x. ASSERT ((\<exists>y. heapmap_\<alpha> a (hm_key_of a (Suc 0)) = Some y) \<and> hmr_invar a) \<bind> (\<lambda>x. hm_exch_op a (Suc 0) (hm_length a) \<bind> (\<lambda>hm. hm_butlast_op hm \<bind> (\<lambda>hm. if hm_length a = Suc 0 then RETURN ((hm_key_of a (Suc 0), the (heapmap_\<alpha> a (hm_key_of a (Suc 0)))), hm) else hm_sink_op hm (Suc 0) \<bind> (\<lambda>hm. RETURN ((hm_key_of a (Suc 0), the (heapmap_\<alpha> a (hm_key_of a (Suc 0)))), hm)))))))) \<le> \<Down> (UNIV \<times>\<^sub>r hmr_rel) (ASSERT (h.heap_invar a') \<bind> (\<lambda>_. ASSERT (h.valid a' (Suc 0)) \<bind> (\<lambda>_. ASSERT (a' \<noteq> []) \<bind> (\<lambda>x. h.exch_op a' (Suc 0) (length a') \<bind> (\<lambda>h. h.butlast_op h \<bind> (\<lambda>h. if length a' = Suc 0 then RETURN (a' ! 0, h) else h.sink_op h (Suc 0) \<bind> (\<lambda>h. RETURN (a' ! 0, h))))))))
[PROOF STEP]
(* Prove refinement *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a'. (a, a') \<in> hmr_rel \<Longrightarrow> ASSERT (heapmap_invar a) \<bind> (\<lambda>_. ASSERT (hm_valid a (Suc 0)) \<bind> (\<lambda>_. ASSERT (hm_valid a (Suc 0)) \<bind> (\<lambda>x. ASSERT ((\<exists>y. heapmap_\<alpha> a (hm_key_of a (Suc 0)) = Some y) \<and> hmr_invar a) \<bind> (\<lambda>x. hm_exch_op a (Suc 0) (hm_length a) \<bind> (\<lambda>hm. hm_butlast_op hm \<bind> (\<lambda>hm. if hm_length a = Suc 0 then RETURN ((hm_key_of a (Suc 0), the (heapmap_\<alpha> a (hm_key_of a (Suc 0)))), hm) else hm_sink_op hm (Suc 0) \<bind> (\<lambda>hm. RETURN ((hm_key_of a (Suc 0), the (heapmap_\<alpha> a (hm_key_of a (Suc 0)))), hm)))))))) \<le> \<Down> (UNIV \<times>\<^sub>r hmr_rel) (ASSERT (h.heap_invar a') \<bind> (\<lambda>_. ASSERT (h.valid a' (Suc 0)) \<bind> (\<lambda>_. ASSERT (a' \<noteq> []) \<bind> (\<lambda>x. h.exch_op a' (Suc 0) (length a') \<bind> (\<lambda>h. h.butlast_op h \<bind> (\<lambda>h. if length a' = Suc 0 then RETURN (a' ! 0, h) else h.sink_op h (Suc 0) \<bind> (\<lambda>h. RETURN (a' ! 0, h))))))))
[PROOF STEP]
apply refine_rcg
[PROOF STATE]
proof (prove)
goal (9 subgoals):
 1. \<And>a a'. \<lbrakk>(a, a') \<in> hmr_rel; h.heap_invar a'; h.valid a' (Suc 0); a' \<noteq> []\<rbrakk> \<Longrightarrow> heapmap_invar a
 2. \<And>a a'. \<lbrakk>(a, a') \<in> hmr_rel; h.heap_invar a'; h.valid a' (Suc 0); a' \<noteq> []; heapmap_invar a\<rbrakk> \<Longrightarrow> hm_valid a (Suc 0)
 3. \<And>a a'. \<lbrakk>(a, a') \<in> hmr_rel; h.heap_invar a'; h.valid a' (Suc 0); a' \<noteq> []; heapmap_invar a; hm_valid a (Suc 0); hm_valid a (Suc 0)\<rbrakk> \<Longrightarrow> \<exists>y. heapmap_\<alpha> a (hm_key_of a (Suc 0)) = Some y
 4. \<And>a a'. \<lbrakk>(a, a') \<in> hmr_rel; h.heap_invar a'; h.valid a' (Suc 0); a' \<noteq> []; heapmap_invar a; hm_valid a (Suc 0); hm_valid a (Suc 0)\<rbrakk> \<Longrightarrow> hmr_invar a
 5. \<And>a a'. \<lbrakk>(a, a') \<in> hmr_rel; h.heap_invar a'; h.valid a' (Suc 0); a' \<noteq> []; heapmap_invar a; hm_valid a (Suc 0); hm_valid a (Suc 0); (\<exists>y. heapmap_\<alpha> a (hm_key_of a (Suc 0)) = Some y) \<and> hmr_invar a\<rbrakk> \<Longrightarrow> (Suc 0, Suc 0) \<in> nat_rel
 6. \<And>a a' hm h hma ha. \<lbrakk>(a, a') \<in> hmr_rel; h.heap_invar a'; h.valid a' (Suc 0); a' \<noteq> []; heapmap_invar a; hm_valid a (Suc 0); hm_valid a (Suc 0); (\<exists>y. heapmap_\<alpha> a (hm_key_of a (Suc 0)) = Some y) \<and> hmr_invar a; (hm, h) \<in> hmr_rel; (hma, ha) \<in> hmr_rel\<rbrakk> \<Longrightarrow> (hm_length a = Suc 0) = (length a' = Suc 0)
 7. \<And>a a' hm h hma ha. \<lbrakk>(a, a') \<in> hmr_rel; h.heap_invar a'; h.valid a' (Suc 0); a' \<noteq> []; heapmap_invar a; hm_valid a (Suc 0); hm_valid a (Suc 0); (\<exists>y. heapmap_\<alpha> a (hm_key_of a (Suc 0)) = Some y) \<and> hmr_invar a; (hm, h) \<in> hmr_rel; (hma, ha) \<in> hmr_rel; hm_length a = Suc 0; length a' = Suc 0\<rbrakk> \<Longrightarrow> (((hm_key_of a (Suc 0), the (heapmap_\<alpha> a (hm_key_of a (Suc 0)))), hma), a' ! 0, ha) \<in> UNIV \<times>\<^sub>r hmr_rel
 8. \<And>a a' hm h hma ha. \<lbrakk>(a, a') \<in> hmr_rel; h.heap_invar a'; h.valid a' (Suc 0); a' \<noteq> []; heapmap_invar a; hm_valid a (Suc 0); hm_valid a (Suc 0); (\<exists>y. heapmap_\<alpha> a (hm_key_of a (Suc 0)) = Some y) \<and> hmr_invar a; (hm, h) \<in> hmr_rel; (hma, ha) \<in> hmr_rel; hm_length a \<noteq> Suc 0; length a' \<noteq> Suc 0\<rbrakk> \<Longrightarrow> (Suc 0, Suc 0) \<in> nat_rel
 9. \<And>a a' hm h hma ha hmb hb. \<lbrakk>(a, a') \<in> hmr_rel; h.heap_invar a'; h.valid a' (Suc 0); a' \<noteq> []; heapmap_invar a; hm_valid a (Suc 0); hm_valid a (Suc 0); (\<exists>y. heapmap_\<alpha> a (hm_key_of a (Suc 0)) = Some y) \<and> hmr_invar a; (hm, h) \<in> hmr_rel; (hma, ha) \<in> hmr_rel; hm_length a \<noteq> Suc 0; length a' \<noteq> Suc 0; (hmb, hb) \<in> hmr_rel\<rbrakk> \<Longrightarrow> (((hm_key_of a (Suc 0), the (heapmap_\<alpha> a (hm_key_of a (Suc 0)))), hmb), a' ! 0, hb) \<in> UNIV \<times>\<^sub>r hmr_rel
[PROOF STEP]
unfolding hmr_rel_def in_br_conv
[PROOF STATE]
proof (prove)
goal (9 subgoals):
 1. \<And>a a'. \<lbrakk>a' = hmr_\<alpha> a \<and> hmr_invar a; h.heap_invar a'; h.valid a' (Suc 0); a' \<noteq> []\<rbrakk> \<Longrightarrow> heapmap_invar a
 2. \<And>a a'. \<lbrakk>a' = hmr_\<alpha> a \<and> hmr_invar a; h.heap_invar a'; h.valid a' (Suc 0); a' \<noteq> []; heapmap_invar a\<rbrakk> \<Longrightarrow> hm_valid a (Suc 0)
 3. \<And>a a'. \<lbrakk>a' = hmr_\<alpha> a \<and> hmr_invar a; h.heap_invar a'; h.valid a' (Suc 0); a' \<noteq> []; heapmap_invar a; hm_valid a (Suc 0); hm_valid a (Suc 0)\<rbrakk> \<Longrightarrow> \<exists>y. heapmap_\<alpha> a (hm_key_of a (Suc 0)) = Some y
 4. \<And>a a'. \<lbrakk>a' = hmr_\<alpha> a \<and> hmr_invar a; h.heap_invar a'; h.valid a' (Suc 0); a' \<noteq> []; heapmap_invar a; hm_valid a (Suc 0); hm_valid a (Suc 0)\<rbrakk> \<Longrightarrow> hmr_invar a
 5. \<And>a a'. \<lbrakk>a' = hmr_\<alpha> a \<and> hmr_invar a; h.heap_invar a'; h.valid a' (Suc 0); a' \<noteq> []; heapmap_invar a; hm_valid a (Suc 0); hm_valid a (Suc 0); (\<exists>y. heapmap_\<alpha> a (hm_key_of a (Suc 0)) = Some y) \<and> hmr_invar a\<rbrakk> \<Longrightarrow> (Suc 0, Suc 0) \<in> nat_rel
 6. \<And>a a' hm h hma ha. \<lbrakk>a' = hmr_\<alpha> a \<and> hmr_invar a; h.heap_invar a'; h.valid a' (Suc 0); a' \<noteq> []; heapmap_invar a; hm_valid a (Suc 0); hm_valid a (Suc 0); (\<exists>y. heapmap_\<alpha> a (hm_key_of a (Suc 0)) = Some y) \<and> hmr_invar a; h = hmr_\<alpha> hm \<and> hmr_invar hm; ha = hmr_\<alpha> hma \<and> hmr_invar hma\<rbrakk> \<Longrightarrow> (hm_length a = Suc 0) = (length a' = Suc 0)
 7. \<And>a a' hm h hma ha. \<lbrakk>a' = hmr_\<alpha> a \<and> hmr_invar a; h.heap_invar a'; h.valid a' (Suc 0); a' \<noteq> []; heapmap_invar a; hm_valid a (Suc 0); hm_valid a (Suc 0); (\<exists>y. heapmap_\<alpha> a (hm_key_of a (Suc 0)) = Some y) \<and> hmr_invar a; h = hmr_\<alpha> hm \<and> hmr_invar hm; ha = hmr_\<alpha> hma \<and> hmr_invar hma; hm_length a = Suc 0; length a' = Suc 0\<rbrakk> \<Longrightarrow> (((hm_key_of a (Suc 0), the (heapmap_\<alpha> a (hm_key_of a (Suc 0)))), hma), a' ! 0, ha) \<in> UNIV \<times>\<^sub>r br hmr_\<alpha> hmr_invar
 8. \<And>a a' hm h hma ha. \<lbrakk>a' = hmr_\<alpha> a \<and> hmr_invar a; h.heap_invar a'; h.valid a' (Suc 0); a' \<noteq> []; heapmap_invar a; hm_valid a (Suc 0); hm_valid a (Suc 0); (\<exists>y. heapmap_\<alpha> a (hm_key_of a (Suc 0)) = Some y) \<and> hmr_invar a; h = hmr_\<alpha> hm \<and> hmr_invar hm; ha = hmr_\<alpha> hma \<and> hmr_invar hma; hm_length a \<noteq> Suc 0; length a' \<noteq> Suc 0\<rbrakk> \<Longrightarrow> (Suc 0, Suc 0) \<in> nat_rel
 9. \<And>a a' hm h hma ha hmb hb. \<lbrakk>a' = hmr_\<alpha> a \<and> hmr_invar a; h.heap_invar a'; h.valid a' (Suc 0); a' \<noteq> []; heapmap_invar a; hm_valid a (Suc 0); hm_valid a (Suc 0); (\<exists>y. heapmap_\<alpha> a (hm_key_of a (Suc 0)) = Some y) \<and> hmr_invar a; h = hmr_\<alpha> hm \<and> hmr_invar hm; ha = hmr_\<alpha> hma \<and> hmr_invar hma; hm_length a \<noteq> Suc 0; length a' \<noteq> Suc 0; hb = hmr_\<alpha> hmb \<and> hmr_invar hmb\<rbrakk> \<Longrightarrow> (((hm_key_of a (Suc 0), the (heapmap_\<alpha> a (hm_key_of a (Suc 0)))), hmb), a' ! 0, hb) \<in> UNIV \<times>\<^sub>r br hmr_\<alpha> hmr_invar
[PROOF STEP]
apply (unfold heapmap_invar_def;simp)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>a a'. \<lbrakk>a' = hmr_\<alpha> a \<and> hmr_invar a; h.heap_invar a'; h.valid a' (Suc 0); a' \<noteq> []; heapmap_invar a\<rbrakk> \<Longrightarrow> hm_valid a (Suc 0)
 2. \<And>a a'. \<lbrakk>a' = hmr_\<alpha> a \<and> hmr_invar a; h.heap_invar a'; h.valid a' (Suc 0); a' \<noteq> []; heapmap_invar a; hm_valid a (Suc 0); hm_valid a (Suc 0)\<rbrakk> \<Longrightarrow> \<exists>y. heapmap_\<alpha> a (hm_key_of a (Suc 0)) = Some y
 3. \<And>a a'. \<lbrakk>a' = hmr_\<alpha> a \<and> hmr_invar a; h.heap_invar a'; h.valid a' (Suc 0); a' \<noteq> []; heapmap_invar a; hm_valid a (Suc 0); hm_valid a (Suc 0)\<rbrakk> \<Longrightarrow> hmr_invar a
 4. \<And>a a'. \<lbrakk>a' = hmr_\<alpha> a \<and> hmr_invar a; h.heap_invar a'; h.valid a' (Suc 0); a' \<noteq> []; heapmap_invar a; hm_valid a (Suc 0); hm_valid a (Suc 0); (\<exists>y. heapmap_\<alpha> a (hm_key_of a (Suc 0)) = Some y) \<and> hmr_invar a\<rbrakk> \<Longrightarrow> (Suc 0, Suc 0) \<in> nat_rel
 5. \<And>a a' hm h hma ha. \<lbrakk>a' = hmr_\<alpha> a \<and> hmr_invar a; h.heap_invar a'; h.valid a' (Suc 0); a' \<noteq> []; heapmap_invar a; hm_valid a (Suc 0); hm_valid a (Suc 0); (\<exists>y. heapmap_\<alpha> a (hm_key_of a (Suc 0)) = Some y) \<and> hmr_invar a; h = hmr_\<alpha> hm \<and> hmr_invar hm; ha = hmr_\<alpha> hma \<and> hmr_invar hma\<rbrakk> \<Longrightarrow> (hm_length a = Suc 0) = (length a' = Suc 0)
 6. \<And>a a' hm h hma ha. \<lbrakk>a' = hmr_\<alpha> a \<and> hmr_invar a; h.heap_invar a'; h.valid a' (Suc 0); a' \<noteq> []; heapmap_invar a; hm_valid a (Suc 0); hm_valid a (Suc 0); (\<exists>y. heapmap_\<alpha> a (hm_key_of a (Suc 0)) = Some y) \<and> hmr_invar a; h = hmr_\<alpha> hm \<and> hmr_invar hm; ha = hmr_\<alpha> hma \<and> hmr_invar hma; hm_length a = Suc 0; length a' = Suc 0\<rbrakk> \<Longrightarrow> (((hm_key_of a (Suc 0), the (heapmap_\<alpha> a (hm_key_of a (Suc 0)))), hma), a' ! 0, ha) \<in> UNIV \<times>\<^sub>r br hmr_\<alpha> hmr_invar
 7. \<And>a a' hm h hma ha. \<lbrakk>a' = hmr_\<alpha> a \<and> hmr_invar a; h.heap_invar a'; h.valid a' (Suc 0); a' \<noteq> []; heapmap_invar a; hm_valid a (Suc 0); hm_valid a (Suc 0); (\<exists>y. heapmap_\<alpha> a (hm_key_of a (Suc 0)) = Some y) \<and> hmr_invar a; h = hmr_\<alpha> hm \<and> hmr_invar hm; ha = hmr_\<alpha> hma \<and> hmr_invar hma; hm_length a \<noteq> Suc 0; length a' \<noteq> Suc 0\<rbrakk> \<Longrightarrow> (Suc 0, Suc 0) \<in> nat_rel
 8. \<And>a a' hm h hma ha hmb hb. \<lbrakk>a' = hmr_\<alpha> a \<and> hmr_invar a; h.heap_invar a'; h.valid a' (Suc 0); a' \<noteq> []; heapmap_invar a; hm_valid a (Suc 0); hm_valid a (Suc 0); (\<exists>y. heapmap_\<alpha> a (hm_key_of a (Suc 0)) = Some y) \<and> hmr_invar a; h = hmr_\<alpha> hm \<and> hmr_invar hm; ha = hmr_\<alpha> hma \<and> hmr_invar hma; hm_length a \<noteq> Suc 0; length a' \<noteq> Suc 0; hb = hmr_\<alpha> hmb \<and> hmr_invar hmb\<rbrakk> \<Longrightarrow> (((hm_key_of a (Suc 0), the (heapmap_\<alpha> a (hm_key_of a (Suc 0)))), hmb), a' ! 0, hb) \<in> UNIV \<times>\<^sub>r br hmr_\<alpha> hmr_invar
[PROOF STEP]
apply (auto simp: in_br_conv)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma heapmap_min_prop:
      assumes INV: "heapmap_invar hm"
      assumes V': "heapmap_\<alpha> hm k = Some v'"
      assumes NE: "hm_valid hm (Suc 0)"
      shows "prio (the (heapmap_\<alpha> hm (hm_key_of hm (Suc 0)))) \<le> prio v'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prio (the (heapmap_\<alpha> hm (hm_key_of hm (Suc 0)))) \<le> prio v'
[PROOF STEP]
proof -
      \<comment> \<open>Transform into the domain of heaps\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prio (the (heapmap_\<alpha> hm (hm_key_of hm (Suc 0)))) \<le> prio v'
[PROOF STEP]
obtain pq m where [simp]: "hm=(pq,m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>pq m. hm = (pq, m) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases hm)
[PROOF STATE]
proof (state)
this:
hm = (pq, m)

goal (1 subgoal):
 1. prio (the (heapmap_\<alpha> hm (hm_key_of hm (Suc 0)))) \<le> prio v'
[PROOF STEP]
from NE
[PROOF STATE]
proof (chain)
picking this:
hm_valid hm (Suc 0)
[PROOF STEP]
have [simp]: "pq\<noteq>[]"
[PROOF STATE]
proof (prove)
using this:
hm_valid hm (Suc 0)

goal (1 subgoal):
 1. pq \<noteq> []
[PROOF STEP]
by (auto simp: hm_valid_def hm_length_def)
[PROOF STATE]
proof (state)
this:
pq \<noteq> []

goal (1 subgoal):
 1. prio (the (heapmap_\<alpha> hm (hm_key_of hm (Suc 0)))) \<le> prio v'
[PROOF STEP]
have CNV_LHS: "prio (the (heapmap_\<alpha> hm (hm_key_of hm (Suc 0))))
        = h.prio_of (hmr_\<alpha> hm) (Suc 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prio (the (heapmap_\<alpha> hm (hm_key_of hm (Suc 0)))) = h.prio_of (hmr_\<alpha> hm) (Suc 0)
[PROOF STEP]
by (auto simp: heapmap_\<alpha>_def hm_key_of_def hmr_\<alpha>_def h.val_of_def)
[PROOF STATE]
proof (state)
this:
prio (the (heapmap_\<alpha> hm (hm_key_of hm (Suc 0)))) = h.prio_of (hmr_\<alpha> hm) (Suc 0)

goal (1 subgoal):
 1. prio (the (heapmap_\<alpha> hm (hm_key_of hm (Suc 0)))) \<le> prio v'
[PROOF STEP]
from INV
[PROOF STATE]
proof (chain)
picking this:
heapmap_invar hm
[PROOF STEP]
have INV': "h.heap_invar (hmr_\<alpha> hm)"
[PROOF STATE]
proof (prove)
using this:
heapmap_invar hm

goal (1 subgoal):
 1. h.heap_invar (hmr_\<alpha> hm)
[PROOF STEP]
unfolding heapmap_invar_def
[PROOF STATE]
proof (prove)
using this:
hmr_invar hm \<and> h.heap_invar (hmr_\<alpha> hm)

goal (1 subgoal):
 1. h.heap_invar (hmr_\<alpha> hm)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
h.heap_invar (hmr_\<alpha> hm)

goal (1 subgoal):
 1. prio (the (heapmap_\<alpha> hm (hm_key_of hm (Suc 0)))) \<le> prio v'
[PROOF STEP]
from V' INV
[PROOF STATE]
proof (chain)
picking this:
heapmap_\<alpha> hm k = Some v'
heapmap_invar hm
[PROOF STEP]
obtain i where IDX: "h.valid (hmr_\<alpha> hm) i"
        and CNV_RHS: "prio v' = h.prio_of (hmr_\<alpha> hm) i"
[PROOF STATE]
proof (prove)
using this:
heapmap_\<alpha> hm k = Some v'
heapmap_invar hm

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>h.valid (hmr_\<alpha> hm) i; prio v' = h.prio_of (hmr_\<alpha> hm) i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply (clarsimp simp: heapmap_\<alpha>_def heapmap_invar_def hmr_invar_def hmr_\<alpha>_def
          h.valid_def h.val_of_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>i. \<lbrakk>0 < i \<and> i \<le> length pq; prio v' = prio (map (the \<circ> m) pq ! (i - Suc 0))\<rbrakk> \<Longrightarrow> thesis; m k = Some v'; distinct pq; dom m = set pq; h.heap_invar (map (the \<circ> m) pq)\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by (metis (no_types, opaque_lifting) Suc_leI comp_apply diff_Suc_Suc
          diff_zero domI index_less_size_conv neq0_conv nth_index nth_map
          old.nat.distinct(2) option.sel)
[PROOF STATE]
proof (state)
this:
h.valid (hmr_\<alpha> hm) i
prio v' = h.prio_of (hmr_\<alpha> hm) i

goal (1 subgoal):
 1. prio (the (heapmap_\<alpha> hm (hm_key_of hm (Suc 0)))) \<le> prio v'
[PROOF STEP]
from h.heap_min_prop[OF INV' IDX]
[PROOF STATE]
proof (chain)
picking this:
h.prio_of (hmr_\<alpha> hm) (Suc 0) \<le> h.prio_of (hmr_\<alpha> hm) i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
h.prio_of (hmr_\<alpha> hm) (Suc 0) \<le> h.prio_of (hmr_\<alpha> hm) i

goal (1 subgoal):
 1. prio (the (heapmap_\<alpha> hm (hm_key_of hm (Suc 0)))) \<le> prio v'
[PROOF STEP]
unfolding CNV_LHS CNV_RHS
[PROOF STATE]
proof (prove)
using this:
h.prio_of (hmr_\<alpha> hm) (Suc 0) \<le> h.prio_of (hmr_\<alpha> hm) i

goal (1 subgoal):
 1. h.prio_of (hmr_\<alpha> hm) (Suc 0) \<le> h.prio_of (hmr_\<alpha> hm) i
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
prio (the (heapmap_\<alpha> hm (hm_key_of hm (Suc 0)))) \<le> prio v'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma hm_pop_min_\<alpha>_correct: "hm_pop_min_op hm \<le>\<^sub>n SPEC (\<lambda>((k,v),hm').
        heapmap_\<alpha> hm k = Some v
      \<and> heapmap_\<alpha> hm' = (heapmap_\<alpha> hm)(k:=None)
      \<and> (\<forall>k' v'. heapmap_\<alpha> hm k' = Some v' \<longrightarrow> prio v \<le> prio v'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hm_pop_min_op hm \<le>\<^sub>n SPEC (\<lambda>((k, v), hm'). heapmap_\<alpha> hm k = Some v \<and> heapmap_\<alpha> hm' = (heapmap_\<alpha> hm)(k := None) \<and> (\<forall>k' v'. heapmap_\<alpha> hm k' = Some v' \<longrightarrow> prio v \<le> prio v'))
[PROOF STEP]
unfolding hm_pop_min_op_def hm_key_of_op_unfold hm_the_lookup_op_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ASSERT (heapmap_invar hm) \<bind> (\<lambda>_. ASSERT (hm_valid hm 1) \<bind> (\<lambda>_. ASSERT (hm_valid hm 1) \<bind> (\<lambda>_. RETURN (hm_key_of hm 1)) \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> hm k \<noteq> None \<and> hmr_invar hm) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> hm k))) \<bind> (\<lambda>v. let l = hm_length hm in hm_exch_op hm 1 l \<bind> (\<lambda>hm. hm_butlast_op hm \<bind> (\<lambda>hm. if l \<noteq> 1 then hm_sink_op hm 1 \<bind> (\<lambda>hm. RETURN ((k, v), hm)) else RETURN ((k, v), hm))))))) \<le>\<^sub>n SPEC (\<lambda>((k, v), hm'). heapmap_\<alpha> hm k = Some v \<and> heapmap_\<alpha> hm' = (heapmap_\<alpha> hm)(k := None) \<and> (\<forall>k' v'. heapmap_\<alpha> hm k' = Some v' \<longrightarrow> prio v \<le> prio v'))
[PROOF STEP]
apply (refine_vcg
        hm_exch_op_\<alpha>_correct[THEN leof_trans]
        hm_butlast_op_\<alpha>_correct[THEN leof_trans]
        hm_sink_op_\<alpha>_correct[THEN leof_trans]
        )
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>x xa xb x1 x1a x2 x2a. \<lbrakk>heapmap_invar hm; hm_valid hm 1; hm_valid hm 1; heapmap_\<alpha> hm (hm_key_of hm 1) \<noteq> None \<and> hmr_invar hm; x \<in> {hm'. hm_valid hm 1 \<and> hm_valid hm (hm_length hm) \<and> hm' = hm_exch hm 1 (hm_length hm)}; xa \<in> {hm'. heapmap_\<alpha> hm' = (heapmap_\<alpha> x)(hm_key_of x (hm_length x) := None)}; hm_length hm \<noteq> 1; xb \<in> {hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> xa}; x1 = (x1a, x2); ((hm_key_of hm 1, the (heapmap_\<alpha> hm (hm_key_of hm 1))), xb) = (x1, x2a)\<rbrakk> \<Longrightarrow> heapmap_\<alpha> hm x1a = Some x2
 2. \<And>x xa xb x1 x1a x2 x2a. \<lbrakk>heapmap_invar hm; hm_valid hm 1; hm_valid hm 1; heapmap_\<alpha> hm (hm_key_of hm 1) \<noteq> None \<and> hmr_invar hm; x \<in> {hm'. hm_valid hm 1 \<and> hm_valid hm (hm_length hm) \<and> hm' = hm_exch hm 1 (hm_length hm)}; xa \<in> {hm'. heapmap_\<alpha> hm' = (heapmap_\<alpha> x)(hm_key_of x (hm_length x) := None)}; hm_length hm \<noteq> 1; xb \<in> {hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> xa}; x1 = (x1a, x2); ((hm_key_of hm 1, the (heapmap_\<alpha> hm (hm_key_of hm 1))), xb) = (x1, x2a)\<rbrakk> \<Longrightarrow> heapmap_\<alpha> x2a = (heapmap_\<alpha> hm)(x1a := None)
 3. \<And>x xa xb x1 x1a x2 x2a k' v'. \<lbrakk>heapmap_invar hm; hm_valid hm 1; hm_valid hm 1; heapmap_\<alpha> hm (hm_key_of hm 1) \<noteq> None \<and> hmr_invar hm; x \<in> {hm'. hm_valid hm 1 \<and> hm_valid hm (hm_length hm) \<and> hm' = hm_exch hm 1 (hm_length hm)}; xa \<in> {hm'. heapmap_\<alpha> hm' = (heapmap_\<alpha> x)(hm_key_of x (hm_length x) := None)}; hm_length hm \<noteq> 1; xb \<in> {hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> xa}; x1 = (x1a, x2); ((hm_key_of hm 1, the (heapmap_\<alpha> hm (hm_key_of hm 1))), xb) = (x1, x2a); heapmap_\<alpha> hm k' = Some v'\<rbrakk> \<Longrightarrow> prio x2 \<le> prio v'
 4. \<And>x xa x1 x1a x2 x2a. \<lbrakk>heapmap_invar hm; hm_valid hm 1; hm_valid hm 1; heapmap_\<alpha> hm (hm_key_of hm 1) \<noteq> None \<and> hmr_invar hm; x \<in> {hm'. hm_valid hm 1 \<and> hm_valid hm (hm_length hm) \<and> hm' = hm_exch hm 1 (hm_length hm)}; xa \<in> {hm'. heapmap_\<alpha> hm' = (heapmap_\<alpha> x)(hm_key_of x (hm_length x) := None)}; \<not> hm_length hm \<noteq> 1; x1 = (x1a, x2); ((hm_key_of hm 1, the (heapmap_\<alpha> hm (hm_key_of hm 1))), xa) = (x1, x2a)\<rbrakk> \<Longrightarrow> heapmap_\<alpha> hm x1a = Some x2
 5. \<And>x xa x1 x1a x2 x2a. \<lbrakk>heapmap_invar hm; hm_valid hm 1; hm_valid hm 1; heapmap_\<alpha> hm (hm_key_of hm 1) \<noteq> None \<and> hmr_invar hm; x \<in> {hm'. hm_valid hm 1 \<and> hm_valid hm (hm_length hm) \<and> hm' = hm_exch hm 1 (hm_length hm)}; xa \<in> {hm'. heapmap_\<alpha> hm' = (heapmap_\<alpha> x)(hm_key_of x (hm_length x) := None)}; \<not> hm_length hm \<noteq> 1; x1 = (x1a, x2); ((hm_key_of hm 1, the (heapmap_\<alpha> hm (hm_key_of hm 1))), xa) = (x1, x2a)\<rbrakk> \<Longrightarrow> heapmap_\<alpha> x2a = (heapmap_\<alpha> hm)(x1a := None)
 6. \<And>x xa x1 x1a x2 x2a k' v'. \<lbrakk>heapmap_invar hm; hm_valid hm 1; hm_valid hm 1; heapmap_\<alpha> hm (hm_key_of hm 1) \<noteq> None \<and> hmr_invar hm; x \<in> {hm'. hm_valid hm 1 \<and> hm_valid hm (hm_length hm) \<and> hm' = hm_exch hm 1 (hm_length hm)}; xa \<in> {hm'. heapmap_\<alpha> hm' = (heapmap_\<alpha> x)(hm_key_of x (hm_length x) := None)}; \<not> hm_length hm \<noteq> 1; x1 = (x1a, x2); ((hm_key_of hm 1, the (heapmap_\<alpha> hm (hm_key_of hm 1))), xa) = (x1, x2a); heapmap_\<alpha> hm k' = Some v'\<rbrakk> \<Longrightarrow> prio x2 \<le> prio v'
[PROOF STEP]
apply (auto simp: heapmap_min_prop)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma hm_kv_op_refine[refine]:
      assumes "(hm,h)\<in>hmr_rel"
      shows "hm_kv_of_op hm i \<le> \<Down>(kvi_rel hm i) (h.val_of_op h i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hm_kv_of_op hm i \<le> \<Down> (kvi_rel hm i) (h.val_of_op h i)
[PROOF STEP]
unfolding hm_kv_of_op_def h.val_of_op_def kvi_rel_def
        hm_key_of_op_unfold hm_the_lookup_op_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ASSERT (hm_valid hm i \<and> hmr_invar hm) \<bind> (\<lambda>_. ASSERT (hm_valid hm i) \<bind> (\<lambda>_. RETURN (hm_key_of hm i)) \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> hm k \<noteq> None \<and> hmr_invar hm) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> hm k))) \<bind> (\<lambda>v. RETURN (k, v)))) \<le> \<Down> {((k, v), v) |k v. hm_key_of hm i = k} (ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get h (i - 1)))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ASSERT (hm_valid hm i \<and> hmr_invar hm) \<bind> (\<lambda>_. ASSERT (hm_valid hm i) \<bind> (\<lambda>x. ASSERT ((\<exists>y. heapmap_\<alpha> hm (hm_key_of hm i) = Some y) \<and> hmr_invar hm) \<bind> (\<lambda>x. RETURN (hm_key_of hm i, the (heapmap_\<alpha> hm (hm_key_of hm i)))))) \<le> \<Down> {uu_. \<exists>v. uu_ = ((hm_key_of hm i, v), v)} (ASSERT (0 < i) \<bind> (\<lambda>_. ASSERT (i - Suc 0 < length h) \<bind> (\<lambda>_. RETURN (h ! (i - Suc 0)))))
[PROOF STEP]
apply refine_vcg
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>0 < i; i - Suc 0 < length h\<rbrakk> \<Longrightarrow> hm_valid hm i
 2. \<lbrakk>0 < i; i - Suc 0 < length h\<rbrakk> \<Longrightarrow> hmr_invar hm
 3. \<lbrakk>0 < i; i - Suc 0 < length h; hm_valid hm i \<and> hmr_invar hm\<rbrakk> \<Longrightarrow> hm_valid hm i
 4. \<lbrakk>0 < i; i - Suc 0 < length h; hm_valid hm i \<and> hmr_invar hm; hm_valid hm i\<rbrakk> \<Longrightarrow> \<exists>y. heapmap_\<alpha> hm (hm_key_of hm i) = Some y
 5. \<lbrakk>0 < i; i - Suc 0 < length h; hm_valid hm i \<and> hmr_invar hm; hm_valid hm i\<rbrakk> \<Longrightarrow> hmr_invar hm
 6. \<lbrakk>0 < i; i - Suc 0 < length h; hm_valid hm i \<and> hmr_invar hm; hm_valid hm i; (\<exists>y. heapmap_\<alpha> hm (hm_key_of hm i) = Some y) \<and> hmr_invar hm\<rbrakk> \<Longrightarrow> ((hm_key_of hm i, the (heapmap_\<alpha> hm (hm_key_of hm i))), h ! (i - Suc 0)) \<in> {uu_. \<exists>v. uu_ = ((hm_key_of hm i, v), v)}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(hm, h) \<in> hmr_rel

goal (6 subgoals):
 1. \<lbrakk>0 < i; i - Suc 0 < length h\<rbrakk> \<Longrightarrow> hm_valid hm i
 2. \<lbrakk>0 < i; i - Suc 0 < length h\<rbrakk> \<Longrightarrow> hmr_invar hm
 3. \<lbrakk>0 < i; i - Suc 0 < length h; hm_valid hm i \<and> hmr_invar hm\<rbrakk> \<Longrightarrow> hm_valid hm i
 4. \<lbrakk>0 < i; i - Suc 0 < length h; hm_valid hm i \<and> hmr_invar hm; hm_valid hm i\<rbrakk> \<Longrightarrow> \<exists>y. heapmap_\<alpha> hm (hm_key_of hm i) = Some y
 5. \<lbrakk>0 < i; i - Suc 0 < length h; hm_valid hm i \<and> hmr_invar hm; hm_valid hm i\<rbrakk> \<Longrightarrow> hmr_invar hm
 6. \<lbrakk>0 < i; i - Suc 0 < length h; hm_valid hm i \<and> hmr_invar hm; hm_valid hm i; (\<exists>y. heapmap_\<alpha> hm (hm_key_of hm i) = Some y) \<and> hmr_invar hm\<rbrakk> \<Longrightarrow> ((hm_key_of hm i, the (heapmap_\<alpha> hm (hm_key_of hm i))), h ! (i - Suc 0)) \<in> {uu_. \<exists>v. uu_ = ((hm_key_of hm i, v), v)}
[PROOF STEP]
by (auto
        simp: hm_valid_def hm_length_def hmr_rel_defs heapmap_\<alpha>_def hm_key_of_def
        split: prod.splits)


[STATEMENT]
lemma hm_pop_min_op_refine':
      "\<lbrakk> (hm,h)\<in>hmr_rel \<rbrakk> \<Longrightarrow> hm_pop_min_op' hm \<le> \<Down>(kvi_rel hm 1 \<times>\<^sub>r hmr_rel) (h.pop_min_op h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (hm, h) \<in> hmr_rel \<Longrightarrow> hm_pop_min_op' hm \<le> \<Down> (kvi_rel hm 1 \<times>\<^sub>r hmr_rel) (h.pop_min_op h)
[PROOF STEP]
unfolding hm_pop_min_op'_def h.pop_min_op_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (hm, h) \<in> hmr_rel \<Longrightarrow> ASSERT (heapmap_invar hm) \<bind> (\<lambda>_. ASSERT (hm_valid hm 1) \<bind> (\<lambda>_. hm_kv_of_op hm 1 \<bind> (\<lambda>kv. let l = hm_length hm in hm_exch_op hm 1 l \<bind> (\<lambda>hm. hm_butlast_op hm \<bind> (\<lambda>hm. if l \<noteq> 1 then hm_sink_op hm 1 \<bind> (\<lambda>hm. RETURN (kv, hm)) else RETURN (kv, hm)))))) \<le> \<Down> (kvi_rel hm 1 \<times>\<^sub>r hmr_rel) (ASSERT (h.heap_invar h) \<bind> (\<lambda>_. ASSERT (h.valid h 1) \<bind> (\<lambda>_. h.val_of_op h 1 \<bind> (\<lambda>m. let l = length h in h.exch_op h 1 l \<bind> (\<lambda>h. h.butlast_op h \<bind> (\<lambda>h. if l \<noteq> 1 then h.sink_op h 1 \<bind> (\<lambda>h. RETURN (m, h)) else RETURN (m, h)))))))
[PROOF STEP]
(* Project away stuff of second component *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (hm, h) \<in> hmr_rel \<Longrightarrow> ASSERT (heapmap_invar hm) \<bind> (\<lambda>_. ASSERT (hm_valid hm 1) \<bind> (\<lambda>_. hm_kv_of_op hm 1 \<bind> (\<lambda>kv. let l = hm_length hm in hm_exch_op hm 1 l \<bind> (\<lambda>hm. hm_butlast_op hm \<bind> (\<lambda>hm. if l \<noteq> 1 then hm_sink_op hm 1 \<bind> (\<lambda>hm. RETURN (kv, hm)) else RETURN (kv, hm)))))) \<le> \<Down> (kvi_rel hm 1 \<times>\<^sub>r hmr_rel) (ASSERT (h.heap_invar h) \<bind> (\<lambda>_. ASSERT (h.valid h 1) \<bind> (\<lambda>_. h.val_of_op h 1 \<bind> (\<lambda>m. let l = length h in h.exch_op h 1 l \<bind> (\<lambda>h. h.butlast_op h \<bind> (\<lambda>h. if l \<noteq> 1 then h.sink_op h 1 \<bind> (\<lambda>h. RETURN (m, h)) else RETURN (m, h)))))))
[PROOF STEP]
unfolding ignore_snd_refine_conv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (hm, h) \<in> hmr_rel \<Longrightarrow> ASSERT (heapmap_invar hm) \<bind> (\<lambda>_. ASSERT (hm_valid hm 1) \<bind> (\<lambda>_. hm_kv_of_op hm 1 \<bind> (\<lambda>kv. let l = hm_length hm in hm_exch_op hm 1 l \<bind> (\<lambda>hm. hm_butlast_op hm \<bind> (\<lambda>hm. if l \<noteq> 1 then hm_sink_op hm 1 \<bind> (\<lambda>hm. RETURN (kv, hm)) else RETURN (kv, hm)))))) \<le> \<Down> (kvi_rel hm 1 \<times>\<^sub>r hmr_rel) (ASSERT (h.heap_invar h) \<bind> (\<lambda>_. ASSERT (h.valid h 1) \<bind> (\<lambda>_. h.val_of_op h 1 \<bind> (\<lambda>m. let l = length h in h.exch_op h 1 l \<bind> (\<lambda>h. h.butlast_op h \<bind> (\<lambda>h. if l \<noteq> 1 then h.sink_op h 1 \<bind> (\<lambda>h. RETURN (m, h)) else RETURN (m, h)))))))
[PROOF STEP]
(* Prove refinement *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (hm, h) \<in> hmr_rel \<Longrightarrow> ASSERT (heapmap_invar hm) \<bind> (\<lambda>_. ASSERT (hm_valid hm 1) \<bind> (\<lambda>_. hm_kv_of_op hm 1 \<bind> (\<lambda>kv. let l = hm_length hm in hm_exch_op hm 1 l \<bind> (\<lambda>hm. hm_butlast_op hm \<bind> (\<lambda>hm. if l \<noteq> 1 then hm_sink_op hm 1 \<bind> (\<lambda>hm. RETURN (kv, hm)) else RETURN (kv, hm)))))) \<le> \<Down> (kvi_rel hm 1 \<times>\<^sub>r hmr_rel) (ASSERT (h.heap_invar h) \<bind> (\<lambda>_. ASSERT (h.valid h 1) \<bind> (\<lambda>_. h.val_of_op h 1 \<bind> (\<lambda>m. let l = length h in h.exch_op h 1 l \<bind> (\<lambda>h. h.butlast_op h \<bind> (\<lambda>h. if l \<noteq> 1 then h.sink_op h 1 \<bind> (\<lambda>h. RETURN (m, h)) else RETURN (m, h)))))))
[PROOF STEP]
apply refine_rcg
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<lbrakk>(hm, h) \<in> hmr_rel; h.heap_invar h; h.valid h 1\<rbrakk> \<Longrightarrow> heapmap_invar hm
 2. \<lbrakk>(hm, h) \<in> hmr_rel; h.heap_invar h; h.valid h 1; heapmap_invar hm\<rbrakk> \<Longrightarrow> hm_valid hm 1
 3. \<And>kv m. \<lbrakk>(hm, h) \<in> hmr_rel; h.heap_invar h; h.valid h 1; heapmap_invar hm; hm_valid hm 1; (kv, m) \<in> kvi_rel hm 1\<rbrakk> \<Longrightarrow> (1, 1) \<in> nat_rel
 4. \<And>kv m hma ha hmaa haa. \<lbrakk>(hm, h) \<in> hmr_rel; h.heap_invar h; h.valid h 1; heapmap_invar hm; hm_valid hm 1; (kv, m) \<in> kvi_rel hm 1; (hma, ha) \<in> hmr_rel; (hmaa, haa) \<in> hmr_rel\<rbrakk> \<Longrightarrow> (hm_length hm \<noteq> 1) = (length h \<noteq> 1)
 5. \<And>kv m hma ha hmaa haa. \<lbrakk>(hm, h) \<in> hmr_rel; h.heap_invar h; h.valid h 1; heapmap_invar hm; hm_valid hm 1; (kv, m) \<in> kvi_rel hm 1; (hma, ha) \<in> hmr_rel; (hmaa, haa) \<in> hmr_rel; hm_length hm \<noteq> 1; length h \<noteq> 1\<rbrakk> \<Longrightarrow> (1, 1) \<in> nat_rel
 6. \<And>kv m hma ha hmaa haa hmb hb. \<lbrakk>(hm, h) \<in> hmr_rel; h.heap_invar h; h.valid h 1; heapmap_invar hm; hm_valid hm 1; (kv, m) \<in> kvi_rel hm 1; (hma, ha) \<in> hmr_rel; (hmaa, haa) \<in> hmr_rel; hm_length hm \<noteq> 1; length h \<noteq> 1; (hmb, hb) \<in> hmr_rel\<rbrakk> \<Longrightarrow> ((kv, hmb), m, hb) \<in> kvi_rel hm 1 \<times>\<^sub>r hmr_rel
 7. \<And>kv m hma ha hmaa haa. \<lbrakk>(hm, h) \<in> hmr_rel; h.heap_invar h; h.valid h 1; heapmap_invar hm; hm_valid hm 1; (kv, m) \<in> kvi_rel hm 1; (hma, ha) \<in> hmr_rel; (hmaa, haa) \<in> hmr_rel; \<not> hm_length hm \<noteq> 1; \<not> length h \<noteq> 1\<rbrakk> \<Longrightarrow> ((kv, hmaa), m, haa) \<in> kvi_rel hm 1 \<times>\<^sub>r hmr_rel
[PROOF STEP]
unfolding hmr_rel_def heapmap_rel_def
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<lbrakk>(hm, h) \<in> br hmr_\<alpha> hmr_invar; h.heap_invar h; h.valid h 1\<rbrakk> \<Longrightarrow> heapmap_invar hm
 2. \<lbrakk>(hm, h) \<in> br hmr_\<alpha> hmr_invar; h.heap_invar h; h.valid h 1; heapmap_invar hm\<rbrakk> \<Longrightarrow> hm_valid hm 1
 3. \<And>kv m. \<lbrakk>(hm, h) \<in> br hmr_\<alpha> hmr_invar; h.heap_invar h; h.valid h 1; heapmap_invar hm; hm_valid hm 1; (kv, m) \<in> kvi_rel hm 1\<rbrakk> \<Longrightarrow> (1, 1) \<in> nat_rel
 4. \<And>kv m hma ha hmaa haa. \<lbrakk>(hm, h) \<in> br hmr_\<alpha> hmr_invar; h.heap_invar h; h.valid h 1; heapmap_invar hm; hm_valid hm 1; (kv, m) \<in> kvi_rel hm 1; (hma, ha) \<in> br hmr_\<alpha> hmr_invar; (hmaa, haa) \<in> br hmr_\<alpha> hmr_invar\<rbrakk> \<Longrightarrow> (hm_length hm \<noteq> 1) = (length h \<noteq> 1)
 5. \<And>kv m hma ha hmaa haa. \<lbrakk>(hm, h) \<in> br hmr_\<alpha> hmr_invar; h.heap_invar h; h.valid h 1; heapmap_invar hm; hm_valid hm 1; (kv, m) \<in> kvi_rel hm 1; (hma, ha) \<in> br hmr_\<alpha> hmr_invar; (hmaa, haa) \<in> br hmr_\<alpha> hmr_invar; hm_length hm \<noteq> 1; length h \<noteq> 1\<rbrakk> \<Longrightarrow> (1, 1) \<in> nat_rel
 6. \<And>kv m hma ha hmaa haa hmb hb. \<lbrakk>(hm, h) \<in> br hmr_\<alpha> hmr_invar; h.heap_invar h; h.valid h 1; heapmap_invar hm; hm_valid hm 1; (kv, m) \<in> kvi_rel hm 1; (hma, ha) \<in> br hmr_\<alpha> hmr_invar; (hmaa, haa) \<in> br hmr_\<alpha> hmr_invar; hm_length hm \<noteq> 1; length h \<noteq> 1; (hmb, hb) \<in> br hmr_\<alpha> hmr_invar\<rbrakk> \<Longrightarrow> ((kv, hmb), m, hb) \<in> kvi_rel hm 1 \<times>\<^sub>r br hmr_\<alpha> hmr_invar
 7. \<And>kv m hma ha hmaa haa. \<lbrakk>(hm, h) \<in> br hmr_\<alpha> hmr_invar; h.heap_invar h; h.valid h 1; heapmap_invar hm; hm_valid hm 1; (kv, m) \<in> kvi_rel hm 1; (hma, ha) \<in> br hmr_\<alpha> hmr_invar; (hmaa, haa) \<in> br hmr_\<alpha> hmr_invar; \<not> hm_length hm \<noteq> 1; \<not> length h \<noteq> 1\<rbrakk> \<Longrightarrow> ((kv, hmaa), m, haa) \<in> kvi_rel hm 1 \<times>\<^sub>r br hmr_\<alpha> hmr_invar
[PROOF STEP]
apply (unfold heapmap_invar_def; simp add: in_br_conv)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>(hm, h) \<in> br hmr_\<alpha> hmr_invar; h.heap_invar h; h.valid h 1; heapmap_invar hm\<rbrakk> \<Longrightarrow> hm_valid hm 1
 2. \<And>kv m. \<lbrakk>(hm, h) \<in> br hmr_\<alpha> hmr_invar; h.heap_invar h; h.valid h 1; heapmap_invar hm; hm_valid hm 1; (kv, m) \<in> kvi_rel hm 1\<rbrakk> \<Longrightarrow> (1, 1) \<in> nat_rel
 3. \<And>kv m hma ha hmaa haa. \<lbrakk>(hm, h) \<in> br hmr_\<alpha> hmr_invar; h.heap_invar h; h.valid h 1; heapmap_invar hm; hm_valid hm 1; (kv, m) \<in> kvi_rel hm 1; (hma, ha) \<in> br hmr_\<alpha> hmr_invar; (hmaa, haa) \<in> br hmr_\<alpha> hmr_invar\<rbrakk> \<Longrightarrow> (hm_length hm \<noteq> 1) = (length h \<noteq> 1)
 4. \<And>kv m hma ha hmaa haa. \<lbrakk>(hm, h) \<in> br hmr_\<alpha> hmr_invar; h.heap_invar h; h.valid h 1; heapmap_invar hm; hm_valid hm 1; (kv, m) \<in> kvi_rel hm 1; (hma, ha) \<in> br hmr_\<alpha> hmr_invar; (hmaa, haa) \<in> br hmr_\<alpha> hmr_invar; hm_length hm \<noteq> 1; length h \<noteq> 1\<rbrakk> \<Longrightarrow> (1, 1) \<in> nat_rel
 5. \<And>kv m hma ha hmaa haa hmb hb. \<lbrakk>(hm, h) \<in> br hmr_\<alpha> hmr_invar; h.heap_invar h; h.valid h 1; heapmap_invar hm; hm_valid hm 1; (kv, m) \<in> kvi_rel hm 1; (hma, ha) \<in> br hmr_\<alpha> hmr_invar; (hmaa, haa) \<in> br hmr_\<alpha> hmr_invar; hm_length hm \<noteq> 1; length h \<noteq> 1; (hmb, hb) \<in> br hmr_\<alpha> hmr_invar\<rbrakk> \<Longrightarrow> ((kv, hmb), m, hb) \<in> kvi_rel hm 1 \<times>\<^sub>r br hmr_\<alpha> hmr_invar
 6. \<And>kv m hma ha hmaa haa. \<lbrakk>(hm, h) \<in> br hmr_\<alpha> hmr_invar; h.heap_invar h; h.valid h 1; heapmap_invar hm; hm_valid hm 1; (kv, m) \<in> kvi_rel hm 1; (hma, ha) \<in> br hmr_\<alpha> hmr_invar; (hmaa, haa) \<in> br hmr_\<alpha> hmr_invar; \<not> hm_length hm \<noteq> 1; \<not> length h \<noteq> 1\<rbrakk> \<Longrightarrow> ((kv, hmaa), m, haa) \<in> kvi_rel hm 1 \<times>\<^sub>r br hmr_\<alpha> hmr_invar
[PROOF STEP]
apply (simp_all add: in_br_conv)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma heapmap_nres_rel_prodI':
      assumes "hmx \<le> \<Down>(S \<times>\<^sub>r hmr_rel) h'x"
      assumes "h'x \<le> SPEC \<Phi>"
      assumes "\<And>h' r. \<Phi> (r,h') \<Longrightarrow> h.heap_invar h'"
      assumes "hmx \<le>\<^sub>n SPEC (\<lambda>(r,hm'). (\<exists>r'. (r,r')\<in>S \<and> \<Phi> (r',hmr_\<alpha> hm')) \<and> hmr_invar hm' \<longrightarrow> RETURN (r,heapmap_\<alpha> hm') \<le> \<Down>(R\<times>\<^sub>rId) hx)"
      shows "hmx \<le> \<Down>(R\<times>\<^sub>rheapmap_rel) hx"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hmx \<le> \<Down> (R \<times>\<^sub>r heapmap_rel) hx
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
hmx \<le> \<Down> (S \<times>\<^sub>r hmr_rel) h'x
h'x \<le> SPEC \<Phi>
\<Phi> (?r34, ?h'34) \<Longrightarrow> h.heap_invar ?h'34
hmx \<le>\<^sub>n SPEC (\<lambda>(r, hm'). (\<exists>r'. (r, r') \<in> S \<and> \<Phi> (r', hmr_\<alpha> hm')) \<and> hmr_invar hm' \<longrightarrow> RETURN (r, heapmap_\<alpha> hm') \<le> \<Down> (R \<times>\<^sub>r Id) hx)

goal (1 subgoal):
 1. hmx \<le> \<Down> (R \<times>\<^sub>r heapmap_rel) hx
[PROOF STEP]
unfolding heapmap_rel_def hmr_rel_def heapmap_invar_def
[PROOF STATE]
proof (prove)
using this:
hmx \<le> \<Down> (S \<times>\<^sub>r br hmr_\<alpha> hmr_invar) h'x
h'x \<le> SPEC \<Phi>
\<Phi> (?r34, ?h'34) \<Longrightarrow> h.heap_invar ?h'34
hmx \<le>\<^sub>n SPEC (\<lambda>(r, hm'). (\<exists>r'. (r, r') \<in> S \<and> \<Phi> (r', hmr_\<alpha> hm')) \<and> hmr_invar hm' \<longrightarrow> RETURN (r, heapmap_\<alpha> hm') \<le> \<Down> (R \<times>\<^sub>r Id) hx)

goal (1 subgoal):
 1. hmx \<le> \<Down> (R \<times>\<^sub>r br heapmap_\<alpha> (\<lambda>hm. hmr_invar hm \<and> h.heap_invar (hmr_\<alpha> hm))) hx
[PROOF STEP]
apply (auto
        simp: pw_le_iff pw_leof_iff refine_pw_simps in_br_conv
        )
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa b. \<lbrakk>\<And>r h'. \<Phi> (r, h') \<Longrightarrow> h.heap_invar h'; \<forall>a aa b. inres hmx (a, aa, b) \<longrightarrow> (\<exists>r'. (a, r') \<in> S \<and> \<Phi> (r', hmr_\<alpha> (aa, b))) \<and> hmr_invar (aa, b) \<longrightarrow> (\<exists>ab. (a, ab) \<in> R \<and> inres hx (ab, heapmap_\<alpha> (aa, b))); nofail hmx; \<forall>a aa b. inres hmx (a, aa, b) \<longrightarrow> (\<exists>ab. (a, ab) \<in> S \<and> hmr_invar (aa, b) \<and> inres h'x (ab, hmr_\<alpha> (aa, b))); nofail h'x; \<forall>a b. inres h'x (a, b) \<longrightarrow> \<Phi> (a, b); nofail hx; inres hmx (a, aa, b)\<rbrakk> \<Longrightarrow> \<exists>ab. (a, ab) \<in> R \<and> hmr_invar (aa, b) \<and> h.heap_invar (hmr_\<alpha> (aa, b)) \<and> inres hx (ab, heapmap_\<alpha> (aa, b))
[PROOF STEP]
by meson


[STATEMENT]
lemma ex_in_kvi_rel_conv:
      "(\<exists>r'. (r,r')\<in>kvi_rel hm i \<and> \<Phi> r') \<longleftrightarrow> (fst r = hm_key_of hm i \<and> \<Phi> (snd r))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>r'. (r, r') \<in> kvi_rel hm i \<and> \<Phi> r') = (fst r = hm_key_of hm i \<and> \<Phi> (snd r))
[PROOF STEP]
unfolding kvi_rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>r'. (r, r') \<in> {((k, v), v) |k v. hm_key_of hm i = k} \<and> \<Phi> r') = (fst r = hm_key_of hm i \<and> \<Phi> (snd r))
[PROOF STEP]
apply (cases r)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. r = (a, b) \<Longrightarrow> (\<exists>r'. (r, r') \<in> {((k, v), v) |k v. hm_key_of hm i = k} \<and> \<Phi> r') = (fst r = hm_key_of hm i \<and> \<Phi> (snd r))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done