[STATEMENT]
lemma invar_final_fail:
    assumes C: "conn src dst" \<comment> \<open>There is a path between
      @{text "src"} and @{text "dst"}.\<close>
    assumes INV: "bfs_invar' src dst (False, V, {}, {}, d)"
    shows False
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. False
[PROOF STEP]
txt \<open>We make a case-distinction whether \<open>d'\<le>d\<close>:\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. False
[PROOF STEP]
have "min_dist src dst \<le> d \<or> d + 1 \<le> min_dist src dst"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. min_dist src dst \<le> d \<or> d + 1 \<le> min_dist src dst
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
min_dist src dst \<le> d \<or> d + 1 \<le> min_dist src dst

goal (1 subgoal):
 1. False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
min_dist src dst \<le> d \<or> d + 1 \<le> min_dist src dst

goal (1 subgoal):
 1. False
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
min_dist src dst \<le> d \<or> d + 1 \<le> min_dist src dst

goal (1 subgoal):
 1. False
[PROOF STEP]
txt \<open>Due to the invariant, any node with a path of
        length at most \<open>d\<close> is contained in \<open>V\<close>
\<close>
[PROOF STATE]
proof (state)
this:
min_dist src dst \<le> d \<or> d + 1 \<le> min_dist src dst

goal (1 subgoal):
 1. False
[PROOF STEP]
from INV
[PROOF STATE]
proof (chain)
picking this:
bfs_invar' src dst (False, V, {}, {}, d)
[PROOF STEP]
have "\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v\<in>V"
[PROOF STATE]
proof (prove)
using this:
bfs_invar' src dst (False, V, {}, {}, d)

goal (1 subgoal):
 1. \<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V
[PROOF STEP]
unfolding bfs_invar'_def
[PROOF STATE]
proof (prove)
using this:
let (f, V, C, N, d) = (False, V, {}, {}, d) in (\<not> f \<longrightarrow> N \<subseteq> V \<and> dst \<notin> V - (C \<union> N) \<and> (\<forall>v\<in>C. conn src v \<and> min_dist src v = d) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N \<union> (\<Union> (succ ` C) - V))) \<and> (f \<longrightarrow> conn src dst \<and> min_dist src dst = d)

goal (1 subgoal):
 1. \<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V

goal (1 subgoal):
 1. False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V

goal (1 subgoal):
 1. False
[PROOF STEP]
txt \<open>This applies in the first case, hence we obtain that
        \<open>dst\<in>V\<close>\<close>
[PROOF STATE]
proof (state)
this:
\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V

goal (1 subgoal):
 1. False
[PROOF STEP]
assume A: "min_dist src dst \<le> d"
[PROOF STATE]
proof (state)
this:
min_dist src dst \<le> d

goal (1 subgoal):
 1. False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
min_dist src dst \<le> d

goal (1 subgoal):
 1. False
[PROOF STEP]
from C
[PROOF STATE]
proof (chain)
picking this:
conn src dst
[PROOF STEP]
have "dist src (min_dist src dst) dst"
[PROOF STATE]
proof (prove)
using this:
conn src dst

goal (1 subgoal):
 1. dist src (min_dist src dst) dst
[PROOF STEP]
by (blast intro: min_dist_is_dist)
[PROOF STATE]
proof (state)
this:
dist src (min_dist src dst) dst

goal (1 subgoal):
 1. False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V
min_dist src dst \<le> d
dist src (min_dist src dst) dst
[PROOF STEP]
have "dst\<in>V"
[PROOF STATE]
proof (prove)
using this:
\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V
min_dist src dst \<le> d
dist src (min_dist src dst) dst

goal (1 subgoal):
 1. dst \<in> V
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
dst \<in> V

goal (1 subgoal):
 1. False
[PROOF STEP]
txt \<open>However, as \<open>C\<close> and \<open>N\<close> are empty, the invariant
        also implies that \<open>dst\<close> is not in \<open>V\<close>:\<close>
[PROOF STATE]
proof (state)
this:
dst \<in> V

goal (1 subgoal):
 1. False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
dst \<in> V

goal (1 subgoal):
 1. False
[PROOF STEP]
from INV
[PROOF STATE]
proof (chain)
picking this:
bfs_invar' src dst (False, V, {}, {}, d)
[PROOF STEP]
have "dst\<notin>V"
[PROOF STATE]
proof (prove)
using this:
bfs_invar' src dst (False, V, {}, {}, d)

goal (1 subgoal):
 1. dst \<notin> V
[PROOF STEP]
unfolding bfs_invar'_def
[PROOF STATE]
proof (prove)
using this:
let (f, V, C, N, d) = (False, V, {}, {}, d) in (\<not> f \<longrightarrow> N \<subseteq> V \<and> dst \<notin> V - (C \<union> N) \<and> (\<forall>v\<in>C. conn src v \<and> min_dist src v = d) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N \<union> (\<Union> (succ ` C) - V))) \<and> (f \<longrightarrow> conn src dst \<and> min_dist src dst = d)

goal (1 subgoal):
 1. dst \<notin> V
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dst \<notin> V

goal (1 subgoal):
 1. False
[PROOF STEP]
txt \<open>This yields a contradiction:\<close>
[PROOF STATE]
proof (state)
this:
dst \<notin> V

goal (1 subgoal):
 1. False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
dst \<in> V
dst \<notin> V
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
dst \<in> V
dst \<notin> V

goal (1 subgoal):
 1. False
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. False
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
min_dist src dst \<le> d \<Longrightarrow> False

goal (1 subgoal):
 1. False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
min_dist src dst \<le> d \<Longrightarrow> False

goal (1 subgoal):
 1. False
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
min_dist src dst \<le> d \<Longrightarrow> False

goal (1 subgoal):
 1. False
[PROOF STEP]
txt \<open>In the case \<open>d+1 \<le> d'\<close>, we also obtain a node
        that has a shortest path of length \<open>d+1\<close>:\<close>
[PROOF STATE]
proof (state)
this:
min_dist src dst \<le> d \<Longrightarrow> False

goal (1 subgoal):
 1. False
[PROOF STEP]
assume "d+1 \<le> min_dist src dst"
[PROOF STATE]
proof (state)
this:
d + 1 \<le> min_dist src dst

goal (1 subgoal):
 1. False
[PROOF STEP]
with min_dist_le[OF C]
[PROOF STATE]
proof (chain)
picking this:
?d' \<le> min_dist src dst \<Longrightarrow> \<exists>v'. conn src v' \<and> min_dist src v' = ?d'
d + 1 \<le> min_dist src dst
[PROOF STEP]
obtain v' where
        "conn src v'" "min_dist src v' = d + 1"
[PROOF STATE]
proof (prove)
using this:
?d' \<le> min_dist src dst \<Longrightarrow> \<exists>v'. conn src v' \<and> min_dist src v' = ?d'
d + 1 \<le> min_dist src dst

goal (1 subgoal):
 1. (\<And>v'. \<lbrakk>conn src v'; min_dist src v' = d + 1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
conn src v'
min_dist src v' = d + 1

goal (1 subgoal):
 1. False
[PROOF STEP]
txt \<open>However, the invariant states that such nodes are either in
        \<open>N\<close> or are successors of \<open>C\<close>. As \<open>N\<close>
        and \<open>C\<close> are both empty, we again get a contradiction.\<close>
[PROOF STATE]
proof (state)
this:
conn src v'
min_dist src v' = d + 1

goal (1 subgoal):
 1. False
[PROOF STEP]
with INV
[PROOF STATE]
proof (chain)
picking this:
bfs_invar' src dst (False, V, {}, {}, d)
conn src v'
min_dist src v' = d + 1
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
bfs_invar' src dst (False, V, {}, {}, d)
conn src v'
min_dist src v' = d + 1

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding bfs_invar'_def
[PROOF STATE]
proof (prove)
using this:
let (f, V, C, N, d) = (False, V, {}, {}, d) in (\<not> f \<longrightarrow> N \<subseteq> V \<and> dst \<notin> V - (C \<union> N) \<and> (\<forall>v\<in>C. conn src v \<and> min_dist src v = d) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N \<union> (\<Union> (succ ` C) - V))) \<and> (f \<longrightarrow> conn src dst \<and> min_dist src dst = d)
conn src v'
min_dist src v' = d + 1

goal (1 subgoal):
 1. False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. False
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
d + 1 \<le> min_dist src dst \<Longrightarrow> False

goal (1 subgoal):
 1. False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
min_dist src dst \<le> d \<or> d + 1 \<le> min_dist src dst
min_dist src dst \<le> d \<Longrightarrow> False
d + 1 \<le> min_dist src dst \<Longrightarrow> False
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
min_dist src dst \<le> d \<or> d + 1 \<le> min_dist src dst
min_dist src dst \<le> d \<Longrightarrow> False
d + 1 \<le> min_dist src dst \<Longrightarrow> False

goal (1 subgoal):
 1. False
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem bfs_correct: "bfs src dst \<le> bfs_spec src dst"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bfs src dst \<le> bfs_spec src dst
[PROOF STEP]
unfolding bfs_def bfs_spec_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. WHILE\<^bsup>bfs_invar src dst\<^esup> (\<lambda>(f, V, C, N, d). f = False \<and> C \<noteq> {}) (\<lambda>(f, V, C, N, d). SPEC (\<lambda>v. v \<in> C) \<bind> (\<lambda>v. let C = C - {v} in if v = dst then RETURN (True, {}, {}, {}, d) else FOREACH\<^bsup>FE_invar V N v\<^esup> (succ v) (\<lambda>w (V, N). if w \<notin> V then ASSERT (w \<notin> N) \<bind> (\<lambda>_. RETURN (insert w V, insert w N)) else RETURN (V, N)) (V, N) \<bind> (\<lambda>(V, N). ASSERT (bfs_invar' src dst (f, V, C, N, d)) \<bind> (\<lambda>_. if C = {} then let C = N; N = {}; d = d + 1 in RETURN (f, V, C, N, d) else RETURN (f, V, C, N, d))))) (False, {src}, {src}, {}, 0) \<bind> (\<lambda>(f, uu_, uu_, uu_, d). if f then RETURN (Some d) else RETURN None) \<le> SPEC (\<lambda>r. case r of None \<Rightarrow> \<not> conn src dst | Some d \<Rightarrow> conn src dst \<and> min_dist src dst = d)
[PROOF STEP]
apply (intro refine_vcg)
[PROOF STATE]
proof (prove)
goal (12 subgoals):
 1. bfs_invar src dst (False, {src}, {src}, {}, 0)
 2. \<And>s a b aa ba ab bb ac bc x. \<lbrakk>bfs_invar src dst s; case s of (f, V, C, N, d) \<Rightarrow> f = False \<and> C \<noteq> {}; s = (a, b); b = (aa, ba); ba = (ab, bb); bb = (ac, bc); x \<in> ab; x = dst\<rbrakk> \<Longrightarrow> bfs_invar src dst (True, {}, {}, {}, bc)
 3. \<And>s a b aa ba ab bb ac bc x. \<lbrakk>bfs_invar src dst s; case s of (f, V, C, N, d) \<Rightarrow> f = False \<and> C \<noteq> {}; s = (a, b); b = (aa, ba); ba = (ab, bb); bb = (ac, bc); x \<in> ab; x \<noteq> dst\<rbrakk> \<Longrightarrow> finite (succ x)
 4. \<And>s a b aa ba ab bb ac bc x. \<lbrakk>bfs_invar src dst s; case s of (f, V, C, N, d) \<Rightarrow> f = False \<and> C \<noteq> {}; s = (a, b); b = (aa, ba); ba = (ab, bb); bb = (ac, bc); x \<in> ab; x \<noteq> dst\<rbrakk> \<Longrightarrow> FE_invar aa ac x (succ x) (aa, ac)
 5. \<And>s a b aa ba ab bb ac bc x xa it \<sigma> ad bd. \<lbrakk>bfs_invar src dst s; case s of (f, V, C, N, d) \<Rightarrow> f = False \<and> C \<noteq> {}; s = (a, b); b = (aa, ba); ba = (ab, bb); bb = (ac, bc); x \<in> ab; x \<noteq> dst; xa \<in> it; it \<subseteq> succ x; FE_invar aa ac x it \<sigma>; \<sigma> = (ad, bd); xa \<notin> ad\<rbrakk> \<Longrightarrow> xa \<notin> bd
 6. \<And>s a b aa ba ab bb ac bc x xa it \<sigma> ad bd. \<lbrakk>bfs_invar src dst s; case s of (f, V, C, N, d) \<Rightarrow> f = False \<and> C \<noteq> {}; s = (a, b); b = (aa, ba); ba = (ab, bb); bb = (ac, bc); x \<in> ab; x \<noteq> dst; xa \<in> it; it \<subseteq> succ x; FE_invar aa ac x it \<sigma>; \<sigma> = (ad, bd); xa \<notin> ad; xa \<notin> bd\<rbrakk> \<Longrightarrow> FE_invar aa ac x (it - {xa}) (insert xa ad, insert xa bd)
 7. \<And>s a b aa ba ab bb ac bc x xa it \<sigma> ad bd. \<lbrakk>bfs_invar src dst s; case s of (f, V, C, N, d) \<Rightarrow> f = False \<and> C \<noteq> {}; s = (a, b); b = (aa, ba); ba = (ab, bb); bb = (ac, bc); x \<in> ab; x \<noteq> dst; xa \<in> it; it \<subseteq> succ x; FE_invar aa ac x it \<sigma>; \<sigma> = (ad, bd); \<not> xa \<notin> ad\<rbrakk> \<Longrightarrow> FE_invar aa ac x (it - {xa}) (ad, bd)
 8. \<And>s a b aa ba ab bb ac bc x \<sigma> ad bd. \<lbrakk>bfs_invar src dst s; case s of (f, V, C, N, d) \<Rightarrow> f = False \<and> C \<noteq> {}; s = (a, b); b = (aa, ba); ba = (ab, bb); bb = (ac, bc); x \<in> ab; x \<noteq> dst; FE_invar aa ac x {} \<sigma>; \<sigma> = (ad, bd)\<rbrakk> \<Longrightarrow> bfs_invar' src dst (a, ad, ab - {x}, bd, bc)
 9. \<And>s a b aa ba ab bb ac bc x \<sigma> ad bd. \<lbrakk>bfs_invar src dst s; case s of (f, V, C, N, d) \<Rightarrow> f = False \<and> C \<noteq> {}; s = (a, b); b = (aa, ba); ba = (ab, bb); bb = (ac, bc); x \<in> ab; x \<noteq> dst; FE_invar aa ac x {} \<sigma>; \<sigma> = (ad, bd); bfs_invar' src dst (a, ad, ab - {x}, bd, bc); ab - {x} = {}\<rbrakk> \<Longrightarrow> bfs_invar src dst (a, ad, bd, {}, bc + 1)
 10. \<And>s a b aa ba ab bb ac bc x \<sigma> ad bd. \<lbrakk>bfs_invar src dst s; case s of (f, V, C, N, d) \<Rightarrow> f = False \<and> C \<noteq> {}; s = (a, b); b = (aa, ba); ba = (ab, bb); bb = (ac, bc); x \<in> ab; x \<noteq> dst; FE_invar aa ac x {} \<sigma>; \<sigma> = (ad, bd); bfs_invar' src dst (a, ad, ab - {x}, bd, bc); ab - {x} \<noteq> {}\<rbrakk> \<Longrightarrow> bfs_invar src dst (a, ad, ab - {x}, bd, bc)
A total of 12 subgoals...
[PROOF STEP]
unfolding FE_invar_def
[PROOF STATE]
proof (prove)
goal (12 subgoals):
 1. bfs_invar src dst (False, {src}, {src}, {}, 0)
 2. \<And>s a b aa ba ab bb ac bc x. \<lbrakk>bfs_invar src dst s; case s of (f, V, C, N, d) \<Rightarrow> f = False \<and> C \<noteq> {}; s = (a, b); b = (aa, ba); ba = (ab, bb); bb = (ac, bc); x \<in> ab; x = dst\<rbrakk> \<Longrightarrow> bfs_invar src dst (True, {}, {}, {}, bc)
 3. \<And>s a b aa ba ab bb ac bc x. \<lbrakk>bfs_invar src dst s; case s of (f, V, C, N, d) \<Rightarrow> f = False \<and> C \<noteq> {}; s = (a, b); b = (aa, ba); ba = (ab, bb); bb = (ac, bc); x \<in> ab; x \<noteq> dst\<rbrakk> \<Longrightarrow> finite (succ x)
 4. \<And>s a b aa ba ab bb ac bc x. \<lbrakk>bfs_invar src dst s; case s of (f, V, C, N, d) \<Rightarrow> f = False \<and> C \<noteq> {}; s = (a, b); b = (aa, ba); ba = (ab, bb); bb = (ac, bc); x \<in> ab; x \<noteq> dst\<rbrakk> \<Longrightarrow> let (V', N') = (aa, ac) in V' = aa \<union> (succ x - succ x) \<and> N' = ac \<union> (succ x - succ x - aa)
 5. \<And>s a b aa ba ab bb ac bc x xa it \<sigma> ad bd. \<lbrakk>bfs_invar src dst s; case s of (f, V, C, N, d) \<Rightarrow> f = False \<and> C \<noteq> {}; s = (a, b); b = (aa, ba); ba = (ab, bb); bb = (ac, bc); x \<in> ab; x \<noteq> dst; xa \<in> it; it \<subseteq> succ x; let (V', N') = \<sigma> in V' = aa \<union> (succ x - it) \<and> N' = ac \<union> (succ x - it - aa); \<sigma> = (ad, bd); xa \<notin> ad\<rbrakk> \<Longrightarrow> xa \<notin> bd
 6. \<And>s a b aa ba ab bb ac bc x xa it \<sigma> ad bd. \<lbrakk>bfs_invar src dst s; case s of (f, V, C, N, d) \<Rightarrow> f = False \<and> C \<noteq> {}; s = (a, b); b = (aa, ba); ba = (ab, bb); bb = (ac, bc); x \<in> ab; x \<noteq> dst; xa \<in> it; it \<subseteq> succ x; let (V', N') = \<sigma> in V' = aa \<union> (succ x - it) \<and> N' = ac \<union> (succ x - it - aa); \<sigma> = (ad, bd); xa \<notin> ad; xa \<notin> bd\<rbrakk> \<Longrightarrow> let (V', N') = (insert xa ad, insert xa bd) in V' = aa \<union> (succ x - (it - {xa})) \<and> N' = ac \<union> (succ x - (it - {xa}) - aa)
 7. \<And>s a b aa ba ab bb ac bc x xa it \<sigma> ad bd. \<lbrakk>bfs_invar src dst s; case s of (f, V, C, N, d) \<Rightarrow> f = False \<and> C \<noteq> {}; s = (a, b); b = (aa, ba); ba = (ab, bb); bb = (ac, bc); x \<in> ab; x \<noteq> dst; xa \<in> it; it \<subseteq> succ x; let (V', N') = \<sigma> in V' = aa \<union> (succ x - it) \<and> N' = ac \<union> (succ x - it - aa); \<sigma> = (ad, bd); \<not> xa \<notin> ad\<rbrakk> \<Longrightarrow> let (V', N') = (ad, bd) in V' = aa \<union> (succ x - (it - {xa})) \<and> N' = ac \<union> (succ x - (it - {xa}) - aa)
 8. \<And>s a b aa ba ab bb ac bc x \<sigma> ad bd. \<lbrakk>bfs_invar src dst s; case s of (f, V, C, N, d) \<Rightarrow> f = False \<and> C \<noteq> {}; s = (a, b); b = (aa, ba); ba = (ab, bb); bb = (ac, bc); x \<in> ab; x \<noteq> dst; let (V', N') = \<sigma> in V' = aa \<union> (succ x - {}) \<and> N' = ac \<union> (succ x - {} - aa); \<sigma> = (ad, bd)\<rbrakk> \<Longrightarrow> bfs_invar' src dst (a, ad, ab - {x}, bd, bc)
 9. \<And>s a b aa ba ab bb ac bc x \<sigma> ad bd. \<lbrakk>bfs_invar src dst s; case s of (f, V, C, N, d) \<Rightarrow> f = False \<and> C \<noteq> {}; s = (a, b); b = (aa, ba); ba = (ab, bb); bb = (ac, bc); x \<in> ab; x \<noteq> dst; let (V', N') = \<sigma> in V' = aa \<union> (succ x - {}) \<and> N' = ac \<union> (succ x - {} - aa); \<sigma> = (ad, bd); bfs_invar' src dst (a, ad, ab - {x}, bd, bc); ab - {x} = {}\<rbrakk> \<Longrightarrow> bfs_invar src dst (a, ad, bd, {}, bc + 1)
 10. \<And>s a b aa ba ab bb ac bc x \<sigma> ad bd. \<lbrakk>bfs_invar src dst s; case s of (f, V, C, N, d) \<Rightarrow> f = False \<and> C \<noteq> {}; s = (a, b); b = (aa, ba); ba = (ab, bb); bb = (ac, bc); x \<in> ab; x \<noteq> dst; let (V', N') = \<sigma> in V' = aa \<union> (succ x - {}) \<and> N' = ac \<union> (succ x - {} - aa); \<sigma> = (ad, bd); bfs_invar' src dst (a, ad, ab - {x}, bd, bc); ab - {x} \<noteq> {}\<rbrakk> \<Longrightarrow> bfs_invar src dst (a, ad, ab - {x}, bd, bc)
A total of 12 subgoals...
[PROOF STEP]
apply (auto simp:
      intro: invar_init invar_break )
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>ad aaa aba aca bca x xa it xb. \<lbrakk>bfs_invar src dst (False, aaa, aba, aca, bca); x \<in> aba; x \<noteq> dst; xa \<in> it; it \<subseteq> succ x; xa \<notin> aaa; \<not> ad; xa \<in> aca; xb \<in> aba\<rbrakk> \<Longrightarrow> False
 2. \<And>ad aaa aba aca bca x xa. \<lbrakk>bfs_invar src dst (False, aaa, aba, aca, bca); x \<in> aba; x \<noteq> dst; \<not> ad; \<not> bfs_invar' src dst (False, aaa \<union> succ x, aba - {x}, aca \<union> (succ x - aaa), bca); xa \<in> aba\<rbrakk> \<Longrightarrow> False
 3. \<And>ad aaa aba aca bca x xa. \<lbrakk>bfs_invar src dst (False, aaa, aba, aca, bca); x \<in> aba; x \<noteq> dst; bfs_invar' src dst (False, aaa \<union> succ x, {}, aca \<union> (succ x - aaa), bca); aba \<subseteq> {x}; \<not> ad; \<not> bfs_invar src dst (False, aaa \<union> succ x, aca \<union> (succ x - aaa), {}, Suc bca); xa \<in> aba\<rbrakk> \<Longrightarrow> False
 4. \<And>ad aaa aba aca bca x xa xb. \<lbrakk>bfs_invar src dst (False, aaa, aba, aca, bca); x \<in> aba; x \<noteq> dst; bfs_invar' src dst (False, aaa \<union> succ x, aba - {x}, aca \<union> (succ x - aaa), bca); \<not> bfs_invar src dst (False, aaa \<union> succ x, aba - {x}, aca \<union> (succ x - aaa), bca); xa \<in> aba; \<not> ad; xa \<noteq> x; xb \<in> aba\<rbrakk> \<Longrightarrow> False
 5. \<And>ad aaa aba aca bca. \<lbrakk>bfs_invar src dst (True, aaa, aba, aca, bca); ad\<rbrakk> \<Longrightarrow> conn src dst
 6. \<And>ad aaa aba aca bca. \<lbrakk>bfs_invar src dst (True, aaa, aba, aca, bca); ad\<rbrakk> \<Longrightarrow> min_dist src dst = bca
 7. \<And>ad aaa aca bca. \<lbrakk>bfs_invar src dst (False, aaa, {}, aca, bca); \<not> ad; conn src dst\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
unfolding bfs_invar_def
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>ad aaa aba aca bca x xa it xb. \<lbrakk>bfs_invar' src dst (False, aaa, aba, aca, bca) \<and> empty_assm (False, aaa, aba, aca, bca); x \<in> aba; x \<noteq> dst; xa \<in> it; it \<subseteq> succ x; xa \<notin> aaa; \<not> ad; xa \<in> aca; xb \<in> aba\<rbrakk> \<Longrightarrow> False
 2. \<And>ad aaa aba aca bca x xa. \<lbrakk>bfs_invar' src dst (False, aaa, aba, aca, bca) \<and> empty_assm (False, aaa, aba, aca, bca); x \<in> aba; x \<noteq> dst; \<not> ad; \<not> bfs_invar' src dst (False, aaa \<union> succ x, aba - {x}, aca \<union> (succ x - aaa), bca); xa \<in> aba\<rbrakk> \<Longrightarrow> False
 3. \<And>ad aaa aba aca bca x xa. \<lbrakk>bfs_invar' src dst (False, aaa, aba, aca, bca) \<and> empty_assm (False, aaa, aba, aca, bca); x \<in> aba; x \<noteq> dst; bfs_invar' src dst (False, aaa \<union> succ x, {}, aca \<union> (succ x - aaa), bca); aba \<subseteq> {x}; \<not> ad; \<not> (bfs_invar' src dst (False, aaa \<union> succ x, aca \<union> (succ x - aaa), {}, Suc bca) \<and> empty_assm (False, aaa \<union> succ x, aca \<union> (succ x - aaa), {}, Suc bca)); xa \<in> aba\<rbrakk> \<Longrightarrow> False
 4. \<And>ad aaa aba aca bca x xa xb. \<lbrakk>bfs_invar' src dst (False, aaa, aba, aca, bca) \<and> empty_assm (False, aaa, aba, aca, bca); x \<in> aba; x \<noteq> dst; bfs_invar' src dst (False, aaa \<union> succ x, aba - {x}, aca \<union> (succ x - aaa), bca); \<not> (bfs_invar' src dst (False, aaa \<union> succ x, aba - {x}, aca \<union> (succ x - aaa), bca) \<and> empty_assm (False, aaa \<union> succ x, aba - {x}, aca \<union> (succ x - aaa), bca)); xa \<in> aba; \<not> ad; xa \<noteq> x; xb \<in> aba\<rbrakk> \<Longrightarrow> False
 5. \<And>ad aaa aba aca bca. \<lbrakk>bfs_invar' src dst (True, aaa, aba, aca, bca) \<and> empty_assm (True, aaa, aba, aca, bca); ad\<rbrakk> \<Longrightarrow> conn src dst
 6. \<And>ad aaa aba aca bca. \<lbrakk>bfs_invar' src dst (True, aaa, aba, aca, bca) \<and> empty_assm (True, aaa, aba, aca, bca); ad\<rbrakk> \<Longrightarrow> min_dist src dst = bca
 7. \<And>ad aaa aca bca. \<lbrakk>bfs_invar' src dst (False, aaa, {}, aca, bca) \<and> empty_assm (False, aaa, {}, aca, bca); \<not> ad; conn src dst\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (auto simp:
      intro: invar_succ_step invar_empty_step invar_final_succeed)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>ad aaa aba aca bca x xa it xb. \<lbrakk>x \<in> aba; x \<noteq> dst; xa \<in> it; it \<subseteq> succ x; xa \<notin> aaa; \<not> ad; xa \<in> aca; xb \<in> aba; bfs_invar' src dst (False, aaa, aba, aca, bca); empty_assm (False, aaa, aba, aca, bca)\<rbrakk> \<Longrightarrow> False
 2. \<And>ad aaa aba aca bca x xa. \<lbrakk>x \<in> aba; x \<noteq> dst; bfs_invar' src dst (False, aaa \<union> succ x, {}, aca \<union> (succ x - aaa), bca); aba \<subseteq> {x}; \<not> ad; xa \<in> aba; bfs_invar' src dst (False, aaa, aba, aca, bca); empty_assm (False, aaa, aba, aca, bca); \<not> empty_assm (False, aaa \<union> succ x, aca \<union> (succ x - aaa), {}, Suc bca)\<rbrakk> \<Longrightarrow> False
 3. \<And>ad aaa aba aca bca x xa xb. \<lbrakk>x \<in> aba; x \<noteq> dst; bfs_invar' src dst (False, aaa \<union> succ x, aba - {x}, aca \<union> (succ x - aaa), bca); \<not> empty_assm (False, aaa \<union> succ x, aba - {x}, aca \<union> (succ x - aaa), bca); xa \<in> aba; \<not> ad; xa \<noteq> x; xb \<in> aba; bfs_invar' src dst (False, aaa, aba, aca, bca); empty_assm (False, aaa, aba, aca, bca)\<rbrakk> \<Longrightarrow> False
 4. \<And>ad aaa aba aca bca. \<lbrakk>ad; bfs_invar' src dst (True, aaa, aba, aca, bca); empty_assm (True, aaa, aba, aca, bca)\<rbrakk> \<Longrightarrow> conn src dst
 5. \<And>ad aaa aca bca. \<lbrakk>\<not> ad; conn src dst; bfs_invar' src dst (False, aaa, {}, aca, bca); empty_assm (False, aaa, {}, aca, bca)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
unfolding empty_assm_def
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>ad aaa aba aca bca x xa it xb. \<lbrakk>x \<in> aba; x \<noteq> dst; xa \<in> it; it \<subseteq> succ x; xa \<notin> aaa; \<not> ad; xa \<in> aca; xb \<in> aba; bfs_invar' src dst (False, aaa, aba, aca, bca); let (f, V, C, N, d) = (False, aaa, aba, aca, bca) in C = {} \<longrightarrow> N = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>ad aaa aba aca bca x xa. \<lbrakk>x \<in> aba; x \<noteq> dst; bfs_invar' src dst (False, aaa \<union> succ x, {}, aca \<union> (succ x - aaa), bca); aba \<subseteq> {x}; \<not> ad; xa \<in> aba; bfs_invar' src dst (False, aaa, aba, aca, bca); let (f, V, C, N, d) = (False, aaa, aba, aca, bca) in C = {} \<longrightarrow> N = {}; \<not> (let (f, V, C, N, d) = (False, aaa \<union> succ x, aca \<union> (succ x - aaa), {}, Suc bca) in C = {} \<longrightarrow> N = {})\<rbrakk> \<Longrightarrow> False
 3. \<And>ad aaa aba aca bca x xa xb. \<lbrakk>x \<in> aba; x \<noteq> dst; bfs_invar' src dst (False, aaa \<union> succ x, aba - {x}, aca \<union> (succ x - aaa), bca); \<not> (let (f, V, C, N, d) = (False, aaa \<union> succ x, aba - {x}, aca \<union> (succ x - aaa), bca) in C = {} \<longrightarrow> N = {}); xa \<in> aba; \<not> ad; xa \<noteq> x; xb \<in> aba; bfs_invar' src dst (False, aaa, aba, aca, bca); let (f, V, C, N, d) = (False, aaa, aba, aca, bca) in C = {} \<longrightarrow> N = {}\<rbrakk> \<Longrightarrow> False
 4. \<And>ad aaa aba aca bca. \<lbrakk>ad; bfs_invar' src dst (True, aaa, aba, aca, bca); let (f, V, C, N, d) = (True, aaa, aba, aca, bca) in C = {} \<longrightarrow> N = {}\<rbrakk> \<Longrightarrow> conn src dst
 5. \<And>ad aaa aca bca. \<lbrakk>\<not> ad; conn src dst; bfs_invar' src dst (False, aaa, {}, aca, bca); let (f, V, C, N, d) = (False, aaa, {}, aca, bca) in C = {} \<longrightarrow> N = {}\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (auto intro: invar_final_fail)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>ad aaa aba aca bca x xa it xb xc. \<lbrakk>x \<in> aba; x \<noteq> dst; xa \<in> it; it \<subseteq> succ x; xa \<notin> aaa; \<not> ad; xa \<in> aca; xb \<in> aba; bfs_invar' src dst (False, aaa, aba, aca, bca); xc \<in> aba\<rbrakk> \<Longrightarrow> False
 2. \<And>ad aaa aba aca bca x. \<lbrakk>ad; bfs_invar' src dst (True, aaa, aba, aca, bca); \<not> conn src dst; x \<in> aba\<rbrakk> \<Longrightarrow> False
 3. \<And>ad aaa aba bca. \<lbrakk>ad; bfs_invar' src dst (True, aaa, aba, {}, bca)\<rbrakk> \<Longrightarrow> conn src dst
[PROOF STEP]
unfolding bfs_invar'_def
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>ad aaa aba aca bca x xa it xb xc. \<lbrakk>x \<in> aba; x \<noteq> dst; xa \<in> it; it \<subseteq> succ x; xa \<notin> aaa; \<not> ad; xa \<in> aca; xb \<in> aba; let (f, V, C, N, d) = (False, aaa, aba, aca, bca) in (\<not> f \<longrightarrow> N \<subseteq> V \<and> dst \<notin> V - (C \<union> N) \<and> (\<forall>v\<in>C. conn src v \<and> min_dist src v = d) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N \<union> (\<Union> (succ ` C) - V))) \<and> (f \<longrightarrow> conn src dst \<and> min_dist src dst = d); xc \<in> aba\<rbrakk> \<Longrightarrow> False
 2. \<And>ad aaa aba aca bca x. \<lbrakk>ad; let (f, V, C, N, d) = (True, aaa, aba, aca, bca) in (\<not> f \<longrightarrow> N \<subseteq> V \<and> dst \<notin> V - (C \<union> N) \<and> (\<forall>v\<in>C. conn src v \<and> min_dist src v = d) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N \<union> (\<Union> (succ ` C) - V))) \<and> (f \<longrightarrow> conn src dst \<and> min_dist src dst = d); \<not> conn src dst; x \<in> aba\<rbrakk> \<Longrightarrow> False
 3. \<And>ad aaa aba bca. \<lbrakk>ad; let (f, V, C, N, d) = (True, aaa, aba, {}, bca) in (\<not> f \<longrightarrow> N \<subseteq> V \<and> dst \<notin> V - (C \<union> N) \<and> (\<forall>v\<in>C. conn src v \<and> min_dist src v = d) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N \<union> (\<Union> (succ ` C) - V))) \<and> (f \<longrightarrow> conn src dst \<and> min_dist src dst = d)\<rbrakk> \<Longrightarrow> conn src dst
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma hmr_empty_invar[simp]: "hmr_invar ([],Map.empty)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hmr_invar ([], Map.empty)
[PROOF STEP]
by (auto simp: hmr_invar_def)


[STATEMENT]
lemma [refine_dref_RELATES]: "RELATES hmr_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. RELATES hmr_rel
[PROOF STEP]
by (simp add: RELATES_def)


[STATEMENT]
lemma h_heap_invarI[simp]: "heapmap_invar hm \<Longrightarrow> h.heap_invar (hmr_\<alpha> hm)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. heapmap_invar hm \<Longrightarrow> h.heap_invar (hmr_\<alpha> hm)
[PROOF STEP]
by (simp add: heapmap_invar_def)


[STATEMENT]
lemma hmr_invarI[simp]: "heapmap_invar hm \<Longrightarrow> hmr_invar hm"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. heapmap_invar hm \<Longrightarrow> hmr_invar hm
[PROOF STEP]
unfolding heapmap_invar_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hmr_invar hm \<and> h.heap_invar (hmr_\<alpha> hm) \<Longrightarrow> hmr_invar hm
[PROOF STEP]
by blast


[STATEMENT]
lemma set_hmr_\<alpha>[simp]: "hmr_invar hm \<Longrightarrow> set (hmr_\<alpha> hm) = ran (heapmap_\<alpha> hm)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hmr_invar hm \<Longrightarrow> set (hmr_\<alpha> hm) = ran (heapmap_\<alpha> hm)
[PROOF STEP]
apply (clarsimp simp: hmr_\<alpha>_def hmr_invar_def heapmap_\<alpha>_def
        eq_commute[of "dom _" "set _"] ran_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>hm = (x, y); distinct x; set x = dom y\<rbrakk> \<Longrightarrow> (\<lambda>x. the (y x)) ` dom y = {b. \<exists>a. y a = Some b}
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma in_h_hmr_\<alpha>_conv[simp]: "hmr_invar hm \<Longrightarrow> x \<in># h.\<alpha> (hmr_\<alpha> hm) \<longleftrightarrow> x \<in> ran (heapmap_\<alpha> hm)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hmr_invar hm \<Longrightarrow> (x \<in># h.\<alpha> (hmr_\<alpha> hm)) = (x \<in> ran (heapmap_\<alpha> hm))
[PROOF STEP]
by (force simp: hmr_\<alpha>_def hmr_invar_def heapmap_\<alpha>_def in_multiset_in_set ran_is_image)


[STATEMENT]
lemma hm_length_refine: "(hm_length, length) \<in> hmr_rel \<rightarrow> nat_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (hm_length, length) \<in> hmr_rel \<rightarrow> nat_rel
[PROOF STEP]
apply (intro fun_relI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a'. (a, a') \<in> hmr_rel \<Longrightarrow> (hm_length a, length a') \<in> nat_rel
[PROOF STEP]
unfolding hm_length_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a'. (a, a') \<in> hmr_rel \<Longrightarrow> (case a of (pq, uu_) \<Rightarrow> length pq, length a') \<in> nat_rel
[PROOF STEP]
by (auto simp: hmr_rel_defs)


[STATEMENT]
lemma hm_length_hmr_\<alpha>[simp]: "length (hmr_\<alpha> hm) = hm_length hm"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (hmr_\<alpha> hm) = hm_length hm
[PROOF STEP]
by (auto simp: hm_length_def hmr_\<alpha>_def split: prod.splits)


[STATEMENT]
lemma hm_valid_hmr_\<alpha>[simp]: "h.valid (hmr_\<alpha> hm) = hm_valid hm"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h.valid (hmr_\<alpha> hm) = hm_valid hm
[PROOF STEP]
by (intro ext) (auto simp: h.valid_def hm_valid_def)


[STATEMENT]
lemma hm_key_of_op_unfold:
      shows "hm_key_of_op hm i = ASSERT (hm_valid hm i) \<then> RETURN (hm_key_of hm i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hm_key_of_op hm i = ASSERT (hm_valid hm i) \<bind> (\<lambda>_. RETURN (hm_key_of hm i))
[PROOF STEP]
unfolding hm_valid_def hm_length_def hm_key_of_op_def hm_key_of_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case hm of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) i = ASSERT (0 < i \<and> i \<le> (case hm of (pq, uu_) \<Rightarrow> length pq)) \<bind> (\<lambda>_. RETURN ((case hm of (pq, m) \<Rightarrow> \<lambda>i. pq ! (i - 1)) i))
[PROOF STEP]
by (auto split: prod.splits simp: pw_eq_iff refine_pw_simps)


[STATEMENT]
lemma val_of_hmr_\<alpha>[simp]: "hm_valid hm i \<Longrightarrow> h.val_of (hmr_\<alpha> hm) i
      = the (heapmap_\<alpha> hm (hm_key_of hm i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hm_valid hm i \<Longrightarrow> h.val_of (hmr_\<alpha> hm) i = the (heapmap_\<alpha> hm (hm_key_of hm i))
[PROOF STEP]
by (auto
        simp: hmr_\<alpha>_def h.val_of_def heapmap_\<alpha>_def hm_key_of_def hm_valid_def hm_length_def
        split: prod.splits)


[STATEMENT]
lemma hm_\<alpha>_key_ex[simp]:
      "\<lbrakk>hmr_invar hm; hm_valid hm i\<rbrakk> \<Longrightarrow> (heapmap_\<alpha> hm (hm_key_of hm i) \<noteq> None)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>hmr_invar hm; hm_valid hm i\<rbrakk> \<Longrightarrow> heapmap_\<alpha> hm (hm_key_of hm i) \<noteq> None
[PROOF STEP]
unfolding heapmap_invar_def hmr_invar_def hm_valid_def heapmap_\<alpha>_def
        hm_key_of_def hm_length_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>case hm of (pq, m) \<Rightarrow> distinct pq \<and> dom m = set pq; 0 < i \<and> i \<le> (case hm of (pq, uu_) \<Rightarrow> length pq)\<rbrakk> \<Longrightarrow> (case hm of (pq, m) \<Rightarrow> m) ((case hm of (pq, m) \<Rightarrow> \<lambda>i. pq ! (i - 1)) i) \<noteq> None
[PROOF STEP]
by (auto split: prod.splits)


[STATEMENT]
lemma hm_exch_op_invar: "hm_exch_op hm i j \<le>\<^sub>n SPEC hmr_invar"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hm_exch_op hm i j \<le>\<^sub>n SPEC hmr_invar
[PROOF STEP]
unfolding hm_exch_op_def h.exch_op_def h.val_of_op_def h.update_op_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case hm 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 j \<le>\<^sub>n SPEC hmr_invar
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case hm 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>_. ASSERT (i - Suc 0 < length pq \<and> j - Suc 0 < length pq) \<bind> (\<lambda>x. RETURN (swap pq (i - Suc 0) (j - Suc 0), m)))))) i j \<le>\<^sub>n SPEC hmr_invar
[PROOF STEP]
apply refine_vcg
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>hm = (x1, x2); hm_valid (x1, x2) i; hm_valid (x1, x2) j; hmr_invar (x1, x2); i - Suc 0 < length x1 \<and> j - Suc 0 < length x1\<rbrakk> \<Longrightarrow> hmr_invar (swap x1 (i - Suc 0) (j - Suc 0), x2)
[PROOF STEP]
apply (auto simp: hm_valid_def map_swap hm_length_def hmr_rel_defs)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma hm_exch_op_refine: "(hm_exch_op,h.exch_op) \<in> hmr_rel \<rightarrow> nat_rel \<rightarrow> nat_rel \<rightarrow> \<langle>hmr_rel\<rangle>nres_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (hm_exch_op, h.exch_op) \<in> hmr_rel \<rightarrow> nat_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 ab a'b. \<lbrakk>(a, a') \<in> hmr_rel; (aa, a'a) \<in> nat_rel; (ab, a'b) \<in> nat_rel\<rbrakk> \<Longrightarrow> hm_exch_op a aa ab \<le> \<Down> hmr_rel (h.exch_op a' a'a a'b)
[PROOF STEP]
unfolding hm_exch_op_def h.exch_op_def h.val_of_op_def h.update_op_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' aa a'a ab a'b. \<lbrakk>(a, a') \<in> hmr_rel; (aa, a'a) \<in> nat_rel; (ab, a'b) \<in> nat_rel\<rbrakk> \<Longrightarrow> (case a 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)))))) aa ab \<le> \<Down> hmr_rel (ASSERT (0 < a'a \<and> 0 < a'b) \<bind> (\<lambda>_. mop_list_swap a' (a'a - 1) (a'b - 1) \<bind> RETURN))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' aa a'a ab a'b. \<lbrakk>(a, a') \<in> hmr_rel; aa = a'a; ab = a'b\<rbrakk> \<Longrightarrow> (case a 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>_. ASSERT (i - Suc 0 < length pq \<and> j - Suc 0 < length pq) \<bind> (\<lambda>x. RETURN (swap pq (i - Suc 0) (j - Suc 0), m)))))) a'a a'b \<le> \<Down> hmr_rel (ASSERT (0 < a'a \<and> 0 < a'b) \<bind> (\<lambda>_. ASSERT (a'a - Suc 0 < length a' \<and> a'b - Suc 0 < length a') \<bind> (\<lambda>_. RETURN (swap a' (a'a - Suc 0) (a'b - Suc 0)))))
[PROOF STEP]
apply refine_vcg
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>a a' aa a'a ab a'b x1 x2. \<lbrakk>(a, a') \<in> hmr_rel; aa = a'a; ab = a'b; 0 < a'a \<and> 0 < a'b; a'a - Suc 0 < length a' \<and> a'b - Suc 0 < length a'; a = (x1, x2)\<rbrakk> \<Longrightarrow> hm_valid (x1, x2) a'a
 2. \<And>a a' aa a'a ab a'b x1 x2. \<lbrakk>(a, a') \<in> hmr_rel; aa = a'a; ab = a'b; 0 < a'a \<and> 0 < a'b; a'a - Suc 0 < length a' \<and> a'b - Suc 0 < length a'; a = (x1, x2); hm_valid (x1, x2) a'a\<rbrakk> \<Longrightarrow> hm_valid (x1, x2) a'b
 3. \<And>a a' aa a'a ab a'b x1 x2. \<lbrakk>(a, a') \<in> hmr_rel; aa = a'a; ab = a'b; 0 < a'a \<and> 0 < a'b; a'a - Suc 0 < length a' \<and> a'b - Suc 0 < length a'; a = (x1, x2); hm_valid (x1, x2) a'a; hm_valid (x1, x2) a'b\<rbrakk> \<Longrightarrow> hmr_invar (x1, x2)
 4. \<And>a a' aa a'a ab a'b x1 x2. \<lbrakk>(a, a') \<in> hmr_rel; aa = a'a; ab = a'b; 0 < a'a \<and> 0 < a'b; a'a - Suc 0 < length a' \<and> a'b - Suc 0 < length a'; a = (x1, x2); hm_valid (x1, x2) a'a; hm_valid (x1, x2) a'b; hmr_invar (x1, x2)\<rbrakk> \<Longrightarrow> a'a - Suc 0 < length x1
 5. \<And>a a' aa a'a ab a'b x1 x2. \<lbrakk>(a, a') \<in> hmr_rel; aa = a'a; ab = a'b; 0 < a'a \<and> 0 < a'b; a'a - Suc 0 < length a' \<and> a'b - Suc 0 < length a'; a = (x1, x2); hm_valid (x1, x2) a'a; hm_valid (x1, x2) a'b; hmr_invar (x1, x2)\<rbrakk> \<Longrightarrow> a'b - Suc 0 < length x1
 6. \<And>a a' aa a'a ab a'b x1 x2. \<lbrakk>(a, a') \<in> hmr_rel; aa = a'a; ab = a'b; 0 < a'a \<and> 0 < a'b; a'a - Suc 0 < length a' \<and> a'b - Suc 0 < length a'; a = (x1, x2); hm_valid (x1, x2) a'a; hm_valid (x1, x2) a'b; hmr_invar (x1, x2); a'a - Suc 0 < length x1 \<and> a'b - Suc 0 < length x1\<rbrakk> \<Longrightarrow> ((swap x1 (a'a - Suc 0) (a'b - Suc 0), x2), swap a' (a'a - Suc 0) (a'b - Suc 0)) \<in> hmr_rel
[PROOF STEP]
apply (auto simp: hm_valid_def map_swap hm_length_def hmr_rel_defs)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma hm_exch_op_\<alpha>_correct: "hm_exch_op hm i j \<le>\<^sub>n SPEC (\<lambda>hm'.
      hm_valid hm i \<and> hm_valid hm j \<and> hm'=hm_exch hm i j
      )"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hm_exch_op hm i j \<le>\<^sub>n SPEC (\<lambda>hm'. hm_valid hm i \<and> hm_valid hm j \<and> hm' = hm_exch hm i j)
[PROOF STEP]
unfolding hm_exch_op_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case hm 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 j \<le>\<^sub>n SPEC (\<lambda>hm'. hm_valid hm i \<and> hm_valid hm j \<and> hm' = hm_exch hm i j)
[PROOF STEP]
apply refine_vcg
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x1 x2. \<lbrakk>hm = (x1, x2); hm_valid (x1, x2) i; hm_valid (x1, x2) j; hmr_invar (x1, x2); i - 1 < length x1 \<and> j - 1 < length x1\<rbrakk> \<Longrightarrow> hm_valid hm i
 2. \<And>x1 x2. \<lbrakk>hm = (x1, x2); hm_valid (x1, x2) i; hm_valid (x1, x2) j; hmr_invar (x1, x2); i - 1 < length x1 \<and> j - 1 < length x1\<rbrakk> \<Longrightarrow> hm_valid hm j
 3. \<And>x1 x2. \<lbrakk>hm = (x1, x2); hm_valid (x1, x2) i; hm_valid (x1, x2) j; hmr_invar (x1, x2); i - 1 < length x1 \<and> j - 1 < length x1\<rbrakk> \<Longrightarrow> (swap x1 (i - 1) (j - 1), x2) = hm_exch hm i j
[PROOF STEP]
apply (vc_solve simp: hm_valid_def hm_length_def heapmap_\<alpha>_def solve: asm_rl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>hm = (x1, x2); hmr_invar (x1, x2); 0 < i; i \<le> length x1; 0 < j; j \<le> length x1; i - Suc 0 < length x1; j - Suc 0 < length x1\<rbrakk> \<Longrightarrow> (swap x1 (i - Suc 0) (j - Suc 0), x2) = hm_exch (x1, x2) i j
[PROOF STEP]
apply (auto simp add: hm_key_of_def hm_exch_def swap_def) []
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma hm_exch_\<alpha>[simp]: "heapmap_\<alpha> (hm_exch hm i j) = (heapmap_\<alpha> hm)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. heapmap_\<alpha> (hm_exch hm i j) = heapmap_\<alpha> hm
[PROOF STEP]
by (auto simp: heapmap_\<alpha>_def hm_exch_def split: prod.splits)


[STATEMENT]
lemma hm_exch_valid[simp]: "hm_valid (hm_exch hm i j) = hm_valid hm"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hm_valid (hm_exch hm i j) = hm_valid hm
[PROOF STEP]
by (intro ext) (auto simp: hm_valid_def hm_length_def hm_exch_def split: prod.splits)


[STATEMENT]
lemma hm_exch_length[simp]: "hm_length (hm_exch hm i j) = hm_length hm"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hm_length (hm_exch hm i j) = hm_length hm
[PROOF STEP]
by (auto simp: hm_length_def hm_exch_def split: prod.splits)


[STATEMENT]
lemma hm_exch_same[simp]: "hm_exch hm i i = hm"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hm_exch hm i i = hm
[PROOF STEP]
by (auto simp: hm_exch_def split: prod.splits)


[STATEMENT]
lemma hm_key_of_exch_conv[simp]:
      "\<lbrakk>hm_valid hm i; hm_valid hm j; hm_valid hm k\<rbrakk> \<Longrightarrow>
        hm_key_of (hm_exch hm i j) k = (
          if k=i then hm_key_of hm j
          else if k=j then hm_key_of hm i
          else hm_key_of hm k
          )"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>hm_valid hm i; hm_valid hm j; hm_valid hm k\<rbrakk> \<Longrightarrow> hm_key_of (hm_exch hm i j) k = (if k = i then hm_key_of hm j else if k = j then hm_key_of hm i else hm_key_of hm k)
[PROOF STEP]
unfolding hm_exch_def hm_valid_def hm_length_def hm_key_of_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < i \<and> i \<le> (case hm of (pq, uu_) \<Rightarrow> length pq); 0 < j \<and> j \<le> (case hm of (pq, uu_) \<Rightarrow> length pq); 0 < k \<and> k \<le> (case hm of (pq, uu_) \<Rightarrow> length pq)\<rbrakk> \<Longrightarrow> (case (case hm of (pq, m) \<Rightarrow> \<lambda>i j. (swap pq (i - 1) (j - 1), m)) i j of (pq, m) \<Rightarrow> \<lambda>i. pq ! (i - 1)) k = (if k = i then (case hm of (pq, m) \<Rightarrow> \<lambda>i. pq ! (i - 1)) j else if k = j then (case hm of (pq, m) \<Rightarrow> \<lambda>i. pq ! (i - 1)) i else (case hm of (pq, m) \<Rightarrow> \<lambda>i. pq ! (i - 1)) k)
[PROOF STEP]
by (auto split: prod.splits)


[STATEMENT]
lemma hm_key_of_exch_matching[simp]:
      "\<lbrakk>hm_valid hm i; hm_valid hm j\<rbrakk> \<Longrightarrow> hm_key_of (hm_exch hm i j) i = hm_key_of hm j"
      "\<lbrakk>hm_valid hm i; hm_valid hm j\<rbrakk> \<Longrightarrow> hm_key_of (hm_exch hm i j) j = hm_key_of hm i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>hm_valid hm i; hm_valid hm j\<rbrakk> \<Longrightarrow> hm_key_of (hm_exch hm i j) i = hm_key_of hm j) &&& (\<lbrakk>hm_valid hm i; hm_valid hm j\<rbrakk> \<Longrightarrow> hm_key_of (hm_exch hm i j) j = hm_key_of hm i)
[PROOF STEP]
by simp_all


[STATEMENT]
lemma hm_index_valid[simp]: "\<lbrakk>hmr_invar hm; heapmap_\<alpha> hm k \<noteq> None\<rbrakk> \<Longrightarrow> hm_valid hm (hm_index hm k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>hmr_invar hm; heapmap_\<alpha> hm k \<noteq> None\<rbrakk> \<Longrightarrow> hm_valid hm (hm_index hm k)
[PROOF STEP]
by (force simp: hm_valid_def heapmap_\<alpha>_def hmr_invar_def hm_index_def hm_length_def Suc_le_eq)


[STATEMENT]
lemma hm_index_key_of[simp]: "\<lbrakk>hmr_invar hm; heapmap_\<alpha> hm k \<noteq> None\<rbrakk> \<Longrightarrow> hm_key_of hm (hm_index hm k) = k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>hmr_invar hm; heapmap_\<alpha> hm k \<noteq> None\<rbrakk> \<Longrightarrow> hm_key_of hm (hm_index hm k) = k
[PROOF STEP]
by (force
          simp: hm_valid_def heapmap_\<alpha>_def hmr_invar_def hm_index_def hm_length_def hm_key_of_def Suc_le_eq)


[STATEMENT]
lemma hm_index_op_correct:
      assumes "hmr_invar hm"
      assumes "heapmap_\<alpha> hm k \<noteq> None"
      shows "hm_index_op hm k \<le> SPEC (\<lambda>r. r= hm_index hm k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hm_index_op hm k \<le> SPEC (\<lambda>r. r = hm_index hm k)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
hmr_invar hm
heapmap_\<alpha> hm k \<noteq> None

goal (1 subgoal):
 1. hm_index_op hm k \<le> SPEC (\<lambda>r. r = hm_index hm k)
[PROOF STEP]
unfolding hm_index_op_def
[PROOF STATE]
proof (prove)
using this:
hmr_invar hm
heapmap_\<alpha> hm k \<noteq> None

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 \<le> SPEC (\<lambda>r. r = hm_index hm k)
[PROOF STEP]
apply refine_vcg
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x1 x2. \<lbrakk>hmr_invar hm; heapmap_\<alpha> hm k \<noteq> None; hm = (x1, x2)\<rbrakk> \<Longrightarrow> hmr_invar (x1, x2)
 2. \<And>x1 x2. \<lbrakk>hmr_invar hm; heapmap_\<alpha> hm k \<noteq> None; hm = (x1, x2)\<rbrakk> \<Longrightarrow> heapmap_\<alpha> (x1, x2) k \<noteq> None
 3. \<And>x1 x2. \<lbrakk>hmr_invar hm; heapmap_\<alpha> hm k \<noteq> None; hm = (x1, x2); hmr_invar (x1, x2) \<and> heapmap_\<alpha> (x1, x2) k \<noteq> None\<rbrakk> \<Longrightarrow> index x1 k + 1 = hm_index hm k
[PROOF STEP]
apply (auto simp: heapmap_\<alpha>_def hmr_invar_def hm_index_def index_nth_id)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma hm_update_op_invar: "hm_update_op hm k v \<le>\<^sub>n SPEC hmr_invar"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hm_update_op hm k v \<le>\<^sub>n SPEC hmr_invar
[PROOF STEP]
unfolding hm_update_op_def h.update_op_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case hm of (pq, m) \<Rightarrow> \<lambda>i v. ASSERT (hm_valid (pq, m) i \<and> hmr_invar (pq, m)) \<bind> (\<lambda>_. mop_list_get pq (i - 1) \<bind> (\<lambda>k. RETURN (pq, m(k \<mapsto> v))))) k v \<le>\<^sub>n SPEC hmr_invar
[PROOF STEP]
apply refine_vcg
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>hm = (x1, x2); hm_valid (x1, x2) k \<and> hmr_invar (x1, x2); k - 1 < length x1\<rbrakk> \<Longrightarrow> hmr_invar (x1, x2(x1 ! (k - 1) \<mapsto> v))
[PROOF STEP]
by (auto simp: hmr_rel_defs map_distinct_upd_conv hm_valid_def hm_length_def)


[STATEMENT]
lemma hm_update_op_refine: "(hm_update_op, h.update_op) \<in> hmr_rel \<rightarrow> nat_rel \<rightarrow> Id \<rightarrow> \<langle>hmr_rel\<rangle>nres_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (hm_update_op, h.update_op) \<in> hmr_rel \<rightarrow> nat_rel \<rightarrow> Id \<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 ab a'b. \<lbrakk>(a, a') \<in> hmr_rel; (aa, a'a) \<in> nat_rel; (ab, a'b) \<in> Id\<rbrakk> \<Longrightarrow> hm_update_op a aa ab \<le> \<Down> hmr_rel (h.update_op a' a'a a'b)
[PROOF STEP]
unfolding hm_update_op_def h.update_op_def mop_list_get_alt mop_list_set_alt
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' aa a'a ab a'b. \<lbrakk>(a, a') \<in> hmr_rel; (aa, a'a) \<in> nat_rel; (ab, a'b) \<in> Id\<rbrakk> \<Longrightarrow> (case a of (pq, m) \<Rightarrow> \<lambda>i v. ASSERT (hm_valid (pq, m) i \<and> hmr_invar (pq, m)) \<bind> (\<lambda>_. ASSERT (pre_list_get (pq, i - 1)) \<bind> (\<lambda>_. RETURN (op_list_get pq (i - 1))) \<bind> (\<lambda>k. RETURN (pq, m(k \<mapsto> v))))) aa ab \<le> \<Down> hmr_rel (ASSERT (0 < a'a) \<bind> (\<lambda>_. ASSERT (pre_list_set ((a', a'a - 1), a'b)) \<bind> (\<lambda>_. RETURN (op_list_set a' (a'a - 1) a'b))))
[PROOF STEP]
apply refine_vcg
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a a' aa a'a ab a'b x1 x2. \<lbrakk>(a, a') \<in> hmr_rel; (aa, a'a) \<in> nat_rel; (ab, a'b) \<in> Id; 0 < a'a; pre_list_set ((a', a'a - 1), a'b); a = (x1, x2)\<rbrakk> \<Longrightarrow> hm_valid (x1, x2) aa
 2. \<And>a a' aa a'a ab a'b x1 x2. \<lbrakk>(a, a') \<in> hmr_rel; (aa, a'a) \<in> nat_rel; (ab, a'b) \<in> Id; 0 < a'a; pre_list_set ((a', a'a - 1), a'b); a = (x1, x2)\<rbrakk> \<Longrightarrow> hmr_invar (x1, x2)
 3. \<And>a a' aa a'a ab a'b x1 x2. \<lbrakk>(a, a') \<in> hmr_rel; (aa, a'a) \<in> nat_rel; (ab, a'b) \<in> Id; 0 < a'a; pre_list_set ((a', a'a - 1), a'b); a = (x1, x2); hm_valid (x1, x2) aa \<and> hmr_invar (x1, x2)\<rbrakk> \<Longrightarrow> pre_list_get (x1, aa - 1)
 4. \<And>a a' aa a'a ab a'b x1 x2. \<lbrakk>(a, a') \<in> hmr_rel; (aa, a'a) \<in> nat_rel; (ab, a'b) \<in> Id; 0 < a'a; pre_list_set ((a', a'a - 1), a'b); a = (x1, x2); hm_valid (x1, x2) aa \<and> hmr_invar (x1, x2); pre_list_get (x1, aa - 1)\<rbrakk> \<Longrightarrow> ((x1, x2(op_list_get x1 (aa - 1) \<mapsto> ab)), op_list_set a' (a'a - 1) a'b) \<in> hmr_rel
[PROOF STEP]
apply (auto simp: hmr_rel_defs map_distinct_upd_conv hm_valid_def hm_length_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma hm_update_op_\<alpha>_correct:
      assumes "hmr_invar hm"
      assumes "heapmap_\<alpha> hm k \<noteq> None"
      shows "hm_update_op hm (hm_index hm k) v \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = (heapmap_\<alpha> hm)(k\<mapsto>v))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hm_update_op hm (hm_index hm k) v \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm(k \<mapsto> v))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
hmr_invar hm
heapmap_\<alpha> hm k \<noteq> None

goal (1 subgoal):
 1. hm_update_op hm (hm_index hm k) v \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm(k \<mapsto> v))
[PROOF STEP]
unfolding hm_update_op_def
[PROOF STATE]
proof (prove)
using this:
hmr_invar hm
heapmap_\<alpha> hm k \<noteq> None

goal (1 subgoal):
 1. (case hm of (pq, m) \<Rightarrow> \<lambda>i v. ASSERT (hm_valid (pq, m) i \<and> hmr_invar (pq, m)) \<bind> (\<lambda>_. mop_list_get pq (i - 1) \<bind> (\<lambda>k. RETURN (pq, m(k \<mapsto> v))))) (hm_index hm k) v \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm(k \<mapsto> v))
[PROOF STEP]
apply refine_vcg
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>hmr_invar hm; heapmap_\<alpha> hm k \<noteq> None; hm = (x1, x2); hm_valid (x1, x2) (hm_index hm k) \<and> hmr_invar (x1, x2); hm_index hm k - 1 < length x1\<rbrakk> \<Longrightarrow> heapmap_\<alpha> (x1, x2(x1 ! (hm_index hm k - 1) \<mapsto> v)) = heapmap_\<alpha> hm(k \<mapsto> v)
[PROOF STEP]
apply (force simp: heapmap_rel_defs hmr_rel_defs hm_index_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma hm_butlast_op_refine: "(hm_butlast_op, h.butlast_op) \<in> hmr_rel \<rightarrow> \<langle>hmr_rel\<rangle>nres_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (hm_butlast_op, h.butlast_op) \<in> hmr_rel \<rightarrow> \<langle>hmr_rel\<rangle>nres_rel
[PROOF STEP]
supply [simp del] = map_upd_eq_restrict
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (hm_butlast_op, h.butlast_op) \<in> hmr_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'. (a, a') \<in> hmr_rel \<Longrightarrow> hm_butlast_op a \<le> \<Down> hmr_rel (h.butlast_op a')
[PROOF STEP]
unfolding hm_butlast_op_def h.butlast_op_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a'. (a, a') \<in> hmr_rel \<Longrightarrow> (case a of (pq, m) \<Rightarrow> ASSERT (hmr_invar (pq, m)) \<bind> (\<lambda>_. mop_list_get pq (length pq - 1) \<bind> (\<lambda>k. mop_list_butlast pq \<bind> (\<lambda>pq. let m = m(k := None) in RETURN (pq, m))))) \<le> \<Down> hmr_rel (mop_list_butlast a')
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a'. (a, a') \<in> hmr_rel \<Longrightarrow> (case a of (pq, m) \<Rightarrow> ASSERT (hmr_invar (pq, m)) \<bind> (\<lambda>_. ASSERT (length pq - Suc 0 < length pq) \<bind> (\<lambda>x. ASSERT (pq \<noteq> []) \<bind> (\<lambda>x. RETURN (butlast pq, m(pq ! (length pq - Suc 0) := None)))))) \<le> \<Down> hmr_rel (ASSERT (a' \<noteq> []) \<bind> (\<lambda>_. RETURN (butlast a')))
[PROOF STEP]
apply refine_vcg
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a a' aa b. \<lbrakk>(a, a') \<in> hmr_rel; a' \<noteq> []; a = (aa, b)\<rbrakk> \<Longrightarrow> hmr_invar (aa, b)
 2. \<And>a a' aa b. \<lbrakk>(a, a') \<in> hmr_rel; a' \<noteq> []; a = (aa, b); hmr_invar (aa, b)\<rbrakk> \<Longrightarrow> length aa - Suc 0 < length aa
 3. \<And>a a' aa b. \<lbrakk>(a, a') \<in> hmr_rel; a' \<noteq> []; a = (aa, b); hmr_invar (aa, b); length aa - Suc 0 < length aa\<rbrakk> \<Longrightarrow> aa \<noteq> []
 4. \<And>a a' aa b. \<lbrakk>(a, a') \<in> hmr_rel; a' \<noteq> []; a = (aa, b); hmr_invar (aa, b); length aa - Suc 0 < length aa; aa \<noteq> []\<rbrakk> \<Longrightarrow> ((butlast aa, b(aa ! (length aa - Suc 0) := None)), butlast a') \<in> hmr_rel
[PROOF STEP]
apply (clarsimp_all simp: hmr_rel_defs map_butlast distinct_butlast)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa ba. \<lbrakk>aa \<noteq> []; distinct aa; dom ba = set aa\<rbrakk> \<Longrightarrow> butlast (map (the \<circ> ba) aa) = butlast (map ((the \<circ>\<circ>\<circ> fun_upd ba) (aa ! (length aa - Suc 0)) None) aa) \<and> set aa - {aa ! (length aa - Suc 0)} = set (butlast aa)
[PROOF STEP]
apply (auto simp: neq_Nil_rev_conv) []
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma hm_butlast_op_\<alpha>_correct: "hm_butlast_op hm \<le>\<^sub>n SPEC (
      \<lambda>hm'. heapmap_\<alpha> hm' = (heapmap_\<alpha> hm)( hm_key_of hm (hm_length hm) := None ))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hm_butlast_op hm \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = (heapmap_\<alpha> hm)(hm_key_of hm (hm_length hm) := None))
[PROOF STEP]
unfolding hm_butlast_op_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case hm of (pq, m) \<Rightarrow> ASSERT (hmr_invar (pq, m)) \<bind> (\<lambda>_. mop_list_get pq (length pq - 1) \<bind> (\<lambda>k. mop_list_butlast pq \<bind> (\<lambda>pq. let m = m(k := None) in RETURN (pq, m))))) \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = (heapmap_\<alpha> hm)(hm_key_of hm (hm_length hm) := None))
[PROOF STEP]
apply refine_vcg
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>hm = (x1, x2); hmr_invar (x1, x2); length x1 - 1 < length x1; x1 \<noteq> []\<rbrakk> \<Longrightarrow> heapmap_\<alpha> (butlast x1, x2(x1 ! (length x1 - 1) := None)) = (heapmap_\<alpha> hm)(hm_key_of hm (hm_length hm) := None)
[PROOF STEP]
apply (auto simp: heapmap_\<alpha>_def hm_key_of_def hm_length_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma hm_append_op_invar: "hm_append_op hm k v \<le>\<^sub>n SPEC hmr_invar"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hm_append_op hm k v \<le>\<^sub>n SPEC hmr_invar
[PROOF STEP]
unfolding hm_append_op_def h.append_op_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case hm of (pq, m) \<Rightarrow> \<lambda>k v. ASSERT (k \<notin> dom m) \<bind> (\<lambda>_. ASSERT (hmr_invar (pq, m)) \<bind> (\<lambda>_. mop_list_append pq k \<bind> (\<lambda>pq. let m = m(k \<mapsto> v) in RETURN (pq, m))))) k v \<le>\<^sub>n SPEC hmr_invar
[PROOF STEP]
apply refine_vcg
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>hm = (x1, x2); k \<notin> dom x2; hmr_invar (x1, x2)\<rbrakk> \<Longrightarrow> hmr_invar (x1 @ [k], x2(k \<mapsto> v))
[PROOF STEP]
unfolding heapmap_\<alpha>_def hmr_rel_defs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>hm = (x1, x2); k \<notin> dom x2; case (x1, x2) of (pq, m) \<Rightarrow> distinct pq \<and> dom m = set pq\<rbrakk> \<Longrightarrow> case (x1 @ [k], x2(k \<mapsto> v)) of (pq, m) \<Rightarrow> distinct pq \<and> dom m = set pq
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma hm_append_op_refine: "\<lbrakk> heapmap_\<alpha> hm k = None; (hm,h)\<in>hmr_rel \<rbrakk>
      \<Longrightarrow> (hm_append_op hm k v, h.append_op h v) \<in> \<langle>hmr_rel\<rangle>nres_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heapmap_\<alpha> hm k = None; (hm, h) \<in> hmr_rel\<rbrakk> \<Longrightarrow> (hm_append_op hm k v, h.append_op h v) \<in> \<langle>hmr_rel\<rangle>nres_rel
[PROOF STEP]
apply (intro fun_relI nres_relI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heapmap_\<alpha> hm k = None; (hm, h) \<in> hmr_rel\<rbrakk> \<Longrightarrow> hm_append_op hm k v \<le> \<Down> hmr_rel (h.append_op h v)
[PROOF STEP]
unfolding hm_append_op_def h.append_op_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heapmap_\<alpha> hm k = None; (hm, h) \<in> hmr_rel\<rbrakk> \<Longrightarrow> (case hm of (pq, m) \<Rightarrow> \<lambda>k v. ASSERT (k \<notin> dom m) \<bind> (\<lambda>_. ASSERT (hmr_invar (pq, m)) \<bind> (\<lambda>_. mop_list_append pq k \<bind> (\<lambda>pq. let m = m(k \<mapsto> v) in RETURN (pq, m))))) k v \<le> \<Down> hmr_rel (mop_list_append h v)
[PROOF STEP]
apply refine_vcg
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x1 x2. \<lbrakk>heapmap_\<alpha> hm k = None; (hm, h) \<in> hmr_rel; hm = (x1, x2)\<rbrakk> \<Longrightarrow> k \<notin> dom x2
 2. \<And>x1 x2. \<lbrakk>heapmap_\<alpha> hm k = None; (hm, h) \<in> hmr_rel; hm = (x1, x2); k \<notin> dom x2\<rbrakk> \<Longrightarrow> hmr_invar (x1, x2)
 3. \<And>x1 x2. \<lbrakk>heapmap_\<alpha> hm k = None; (hm, h) \<in> hmr_rel; hm = (x1, x2); k \<notin> dom x2; hmr_invar (x1, x2)\<rbrakk> \<Longrightarrow> mop_list_append x1 k \<bind> (\<lambda>pq. let m = x2(k \<mapsto> v) in RETURN (pq, m)) \<le> \<Down> hmr_rel (mop_list_append h v)
[PROOF STEP]
unfolding heapmap_\<alpha>_def hmr_rel_defs
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x1 x2. \<lbrakk>(case hm of (pq, m) \<Rightarrow> m) k = None; (hm, h) \<in> {(c, a). a = (case c of (pq, m) \<Rightarrow> map (the \<circ> m) pq) \<and> (case c of (pq, m) \<Rightarrow> distinct pq \<and> dom m = set pq)}; hm = (x1, x2)\<rbrakk> \<Longrightarrow> k \<notin> dom x2
 2. \<And>x1 x2. \<lbrakk>(case hm of (pq, m) \<Rightarrow> m) k = None; (hm, h) \<in> {(c, a). a = (case c of (pq, m) \<Rightarrow> map (the \<circ> m) pq) \<and> (case c of (pq, m) \<Rightarrow> distinct pq \<and> dom m = set pq)}; hm = (x1, x2); k \<notin> dom x2\<rbrakk> \<Longrightarrow> case (x1, x2) of (pq, m) \<Rightarrow> distinct pq \<and> dom m = set pq
 3. \<And>x1 x2. \<lbrakk>(case hm of (pq, m) \<Rightarrow> m) k = None; (hm, h) \<in> {(c, a). a = (case c of (pq, m) \<Rightarrow> map (the \<circ> m) pq) \<and> (case c of (pq, m) \<Rightarrow> distinct pq \<and> dom m = set pq)}; hm = (x1, x2); k \<notin> dom x2; case (x1, x2) of (pq, m) \<Rightarrow> distinct pq \<and> dom m = set pq\<rbrakk> \<Longrightarrow> mop_list_append x1 k \<bind> (\<lambda>pq. let m = x2(k \<mapsto> v) in RETURN (pq, m)) \<le> \<Down> {(c, a). a = (case c of (pq, m) \<Rightarrow> map (the \<circ> m) pq) \<and> (case c of (pq, m) \<Rightarrow> distinct pq \<and> dom m = set pq)} (mop_list_append h v)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma hm_append_op_\<alpha>_correct:
      "hm_append_op hm k v \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = (heapmap_\<alpha> hm) (k \<mapsto> v))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hm_append_op hm k v \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm(k \<mapsto> v))
[PROOF STEP]
unfolding hm_append_op_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case hm of (pq, m) \<Rightarrow> \<lambda>k v. ASSERT (k \<notin> dom m) \<bind> (\<lambda>_. ASSERT (hmr_invar (pq, m)) \<bind> (\<lambda>_. mop_list_append pq k \<bind> (\<lambda>pq. let m = m(k \<mapsto> v) in RETURN (pq, m))))) k v \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> hm(k \<mapsto> v))
[PROOF STEP]
apply refine_vcg
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>hm = (x1, x2); k \<notin> dom x2; hmr_invar (x1, x2)\<rbrakk> \<Longrightarrow> heapmap_\<alpha> (x1 @ [k], x2(k \<mapsto> v)) = heapmap_\<alpha> hm(k \<mapsto> v)
[PROOF STEP]
by (auto simp: heapmap_\<alpha>_def)


[STATEMENT]
lemma heapmap_hmr_relI: "(hm,h)\<in>heapmap_rel \<Longrightarrow> (hm,hmr_\<alpha> hm) \<in> hmr_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (hm, h) \<in> heapmap_rel \<Longrightarrow> (hm, hmr_\<alpha> hm) \<in> hmr_rel
[PROOF STEP]
by (auto simp: heapmap_rel_defs hmr_rel_defs)


[STATEMENT]
lemma heapmap_hmr_relI': "heapmap_invar hm \<Longrightarrow> (hm,hmr_\<alpha> hm) \<in> hmr_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. heapmap_invar hm \<Longrightarrow> (hm, hmr_\<alpha> hm) \<in> hmr_rel
[PROOF STEP]
by (auto simp: heapmap_rel_defs hmr_rel_defs)


[STATEMENT]
lemma heapmap_nres_relI':
      assumes "hm \<le> \<Down>hmr_rel h'"
      assumes "h' \<le> SPEC (h.heap_invar)"
      assumes "hm \<le>\<^sub>n SPEC (\<lambda>hm'. RETURN (heapmap_\<alpha> hm') \<le> h)"
      shows "hm \<le> \<Down>heapmap_rel h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hm \<le> \<Down> heapmap_rel h
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
hm \<le> \<Down> hmr_rel h'
h' \<le> SPEC h.heap_invar
hm \<le>\<^sub>n SPEC (\<lambda>hm'. RETURN (heapmap_\<alpha> hm') \<le> h)

goal (1 subgoal):
 1. hm \<le> \<Down> heapmap_rel h
[PROOF STEP]
unfolding heapmap_rel_defs hmr_rel_def
[PROOF STATE]
proof (prove)
using this:
hm \<le> \<Down> {(c, a). a = hmr_\<alpha> c \<and> hmr_invar c} h'
h' \<le> SPEC h.heap_invar
hm \<le>\<^sub>n SPEC (\<lambda>hm'. RETURN (case hm' of (pq, m) \<Rightarrow> m) \<le> h)

goal (1 subgoal):
 1. hm \<le> \<Down> {(c, a). a = (case c of (pq, m) \<Rightarrow> m) \<and> hmr_invar c \<and> h.heap_invar (hmr_\<alpha> c)} h
[PROOF STEP]
by (auto simp: pw_le_iff pw_leof_iff refine_pw_simps)


[STATEMENT]
lemma heapmap_nres_relI'':
      assumes "hm \<le> \<Down>hmr_rel h'"
      assumes "h' \<le> SPEC \<Phi>"
      assumes "\<And>h'. \<Phi> h' \<Longrightarrow> h.heap_invar h'"
      assumes "hm \<le>\<^sub>n SPEC (\<lambda>hm'. RETURN (heapmap_\<alpha> hm') \<le> h)"
      shows "hm \<le> \<Down>heapmap_rel h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hm \<le> \<Down> heapmap_rel h
[PROOF STEP]
apply (rule heapmap_nres_relI')
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. hm \<le> \<Down> hmr_rel ?h'
 2. ?h' \<le> SPEC h.heap_invar
 3. hm \<le>\<^sub>n SPEC (\<lambda>hm'. RETURN (heapmap_\<alpha> hm') \<le> h)
[PROOF STEP]
apply fact
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. h' \<le> SPEC h.heap_invar
 2. hm \<le>\<^sub>n SPEC (\<lambda>hm'. RETURN (heapmap_\<alpha> hm') \<le> h)
[PROOF STEP]
apply (rule order_trans, fact)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. SPEC \<Phi> \<le> SPEC h.heap_invar
 2. hm \<le>\<^sub>n SPEC (\<lambda>hm'. RETURN (heapmap_\<alpha> hm') \<le> h)
[PROOF STEP]
apply (clarsimp; fact)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hm \<le>\<^sub>n SPEC (\<lambda>hm'. RETURN (heapmap_\<alpha> hm') \<le> h)
[PROOF STEP]
apply fact
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma hm_val_of_op_refine: "(hm_val_of_op,h.val_of_op) \<in> (hmr_rel \<rightarrow> nat_rel \<rightarrow> \<langle>Id\<rangle>nres_rel)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (hm_val_of_op, h.val_of_op) \<in> hmr_rel \<rightarrow> nat_rel \<rightarrow> \<langle>Id\<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_val_of_op a aa \<le> \<Down> Id (h.val_of_op a' a'a)
[PROOF STEP]
unfolding hm_val_of_op_def h.val_of_op_def
        hm_key_of_op_def hm_key_of_def hm_valid_def hm_length_def
        hm_the_lookup_op_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> (case a of (pq, m) \<Rightarrow> \<lambda>i. ASSERT (0 < i) \<bind> (\<lambda>_. mop_list_get pq (i - 1))) aa \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> a k \<noteq> None \<and> hmr_invar a) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> a k))) \<bind> RETURN) \<le> \<Down> Id (ASSERT (0 < a'a) \<bind> (\<lambda>_. mop_list_get a' (a'a - 1)))
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b a' a'a. ((a, b), a') \<in> hmr_rel \<Longrightarrow> ASSERT (0 < a'a) \<bind> (\<lambda>x. ASSERT (a'a - Suc 0 < length a) \<bind> (\<lambda>x. ASSERT ((\<exists>y. heapmap_\<alpha> (a, b) (a ! (a'a - Suc 0)) = Some y) \<and> hmr_invar (a, b)) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> (a, b) (a ! (a'a - Suc 0))))))) \<le> ASSERT (0 < a'a) \<bind> (\<lambda>_. ASSERT (a'a - Suc 0 < length a') \<bind> (\<lambda>_. RETURN (a' ! (a'a - Suc 0))))
[PROOF STEP]
apply (rule refine_IdD)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b a' a'a. ((a, b), a') \<in> hmr_rel \<Longrightarrow> ASSERT (0 < a'a) \<bind> (\<lambda>x. ASSERT (a'a - Suc 0 < length a) \<bind> (\<lambda>x. ASSERT ((\<exists>y. heapmap_\<alpha> (a, b) (a ! (a'a - Suc 0)) = Some y) \<and> hmr_invar (a, b)) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> (a, b) (a ! (a'a - Suc 0))))))) \<le> \<Down> Id (ASSERT (0 < a'a) \<bind> (\<lambda>_. ASSERT (a'a - Suc 0 < length a') \<bind> (\<lambda>_. RETURN (a' ! (a'a - Suc 0)))))
[PROOF STEP]
apply refine_vcg
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a b a' a'a. \<lbrakk>((a, b), a') \<in> hmr_rel; 0 < a'a; a'a - Suc 0 < length a'; 0 < a'a\<rbrakk> \<Longrightarrow> a'a - Suc 0 < length a
 2. \<And>a b a' a'a. \<lbrakk>((a, b), a') \<in> hmr_rel; 0 < a'a; a'a - Suc 0 < length a'; 0 < a'a; a'a - Suc 0 < length a\<rbrakk> \<Longrightarrow> \<exists>y. heapmap_\<alpha> (a, b) (a ! (a'a - Suc 0)) = Some y
 3. \<And>a b a' a'a. \<lbrakk>((a, b), a') \<in> hmr_rel; 0 < a'a; a'a - Suc 0 < length a'; 0 < a'a; a'a - Suc 0 < length a\<rbrakk> \<Longrightarrow> hmr_invar (a, b)
 4. \<And>a b a' a'a. \<lbrakk>((a, b), a') \<in> hmr_rel; 0 < a'a; a'a - Suc 0 < length a'; 0 < a'a; a'a - Suc 0 < length a; (\<exists>y. heapmap_\<alpha> (a, b) (a ! (a'a - Suc 0)) = Some y) \<and> hmr_invar (a, b)\<rbrakk> \<Longrightarrow> (the (heapmap_\<alpha> (a, b) (a ! (a'a - Suc 0))), a' ! (a'a - Suc 0)) \<in> Id
[PROOF STEP]
apply (auto simp: hmr_rel_defs heapmap_\<alpha>_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma hm_prio_of_op_refine: "(hm_prio_of_op, h.prio_of_op) \<in> hmr_rel \<rightarrow> nat_rel \<rightarrow> \<langle>Id\<rangle>nres_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (hm_prio_of_op, h.prio_of_op) \<in> hmr_rel \<rightarrow> nat_rel \<rightarrow> \<langle>Id\<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_prio_of_op a aa \<le> \<Down> Id (h.prio_of_op a' a'a)
[PROOF STEP]
unfolding hm_prio_of_op_def h.prio_of_op_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> hm_val_of_op a aa \<bind> (\<lambda>v. RETURN (prio v)) \<le> \<Down> Id (h.val_of_op a' a'a \<bind> (\<lambda>v. RETURN (prio v)))
[PROOF STEP]
apply refine_rcg
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' aa a'a v va. \<lbrakk>(a, a') \<in> hmr_rel; (aa, a'a) \<in> nat_rel; (v, va) \<in> Id\<rbrakk> \<Longrightarrow> (prio v, prio va) \<in> Id
[PROOF STEP]
by auto


[STATEMENT]
lemma hm_swim_op_refine: "(hm_swim_op, h.swim_op) \<in> hmr_rel \<rightarrow> nat_rel \<rightarrow> \<langle>hmr_rel\<rangle>nres_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (hm_swim_op, h.swim_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_swim_op a aa \<le> \<Down> hmr_rel (h.swim_op a' a'a)
[PROOF STEP]
unfolding hm_swim_op_def h.swim_op_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>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)) (a, aa) \<le> \<Down> hmr_rel (REC\<^sub>T (\<lambda>swim (h, i). ASSERT (h.valid h i \<and> h.swim_invar h i) \<bind> (\<lambda>_. if h.has_parent h i then h.prio_of_op h (h.parent i) \<bind> (\<lambda>ppi. h.prio_of_op h i \<bind> (\<lambda>pi. if \<not> ppi \<le> pi then h.exch_op h i (h.parent i) \<bind> (\<lambda>h. swim (h, h.parent i)) else RETURN h)) else RETURN h)) (a', a'a))
[PROOF STEP]
apply refine_rcg
[PROOF STATE]
proof (prove)
goal (15 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 swim swima 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> swim x \<le> \<Down> hmr_rel (swima x'); (x, x') \<in> ?R3 a a' aa a'a; x' = (x1, x2); x = (x1a, x2a); h.valid x1 x2 \<and> h.swim_invar x1 x2\<rbrakk> \<Longrightarrow> hm_valid x1a x2a
 3. \<And>a a' aa a'a swim swima 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> swim x \<le> \<Down> hmr_rel (swima x'); (x, x') \<in> ?R3 a a' aa a'a; x' = (x1, x2); x = (x1a, x2a); h.valid x1 x2 \<and> h.swim_invar x1 x2\<rbrakk> \<Longrightarrow> h.swim_invar (hmr_\<alpha> x1a) x2a
 4. \<And>a a' aa a'a swim swima 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> swim x \<le> \<Down> hmr_rel (swima x'); (x, x') \<in> ?R3 a a' aa a'a; x' = (x1, x2); x = (x1a, x2a); h.valid x1 x2 \<and> h.swim_invar x1 x2; hm_valid x1a x2a \<and> h.swim_invar (hmr_\<alpha> x1a) x2a\<rbrakk> \<Longrightarrow> hm_valid x1a (h.parent x2a) = h.has_parent x1 x2
 5. \<And>a a' aa a'a swim swima 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> swim x \<le> \<Down> hmr_rel (swima x'); (x, x') \<in> ?R3 a a' aa a'a; x' = (x1, x2); x = (x1a, x2a); h.valid x1 x2 \<and> h.swim_invar x1 x2; hm_valid x1a x2a \<and> h.swim_invar (hmr_\<alpha> x1a) x2a; hm_valid x1a (h.parent x2a); h.has_parent x1 x2\<rbrakk> \<Longrightarrow> (x1a, x1) \<in> hmr_rel
 6. \<And>a a' aa a'a swim swima 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> swim x \<le> \<Down> hmr_rel (swima x'); (x, x') \<in> ?R3 a a' aa a'a; x' = (x1, x2); x = (x1a, x2a); h.valid x1 x2 \<and> h.swim_invar x1 x2; hm_valid x1a x2a \<and> h.swim_invar (hmr_\<alpha> x1a) x2a; hm_valid x1a (h.parent x2a); h.has_parent x1 x2\<rbrakk> \<Longrightarrow> (h.parent x2a, h.parent x2) \<in> nat_rel
 7. \<And>a a' aa a'a swim swima x x' x1 x2 x1a x2a ppi ppia. \<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> swim x \<le> \<Down> hmr_rel (swima x'); (x, x') \<in> ?R3 a a' aa a'a; x' = (x1, x2); x = (x1a, x2a); h.valid x1 x2 \<and> h.swim_invar x1 x2; hm_valid x1a x2a \<and> h.swim_invar (hmr_\<alpha> x1a) x2a; hm_valid x1a (h.parent x2a); h.has_parent x1 x2; (ppi, ppia) \<in> Id\<rbrakk> \<Longrightarrow> (x1a, x1) \<in> hmr_rel
 8. \<And>a a' aa a'a swim swima x x' x1 x2 x1a x2a ppi ppia. \<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> swim x \<le> \<Down> hmr_rel (swima x'); (x, x') \<in> ?R3 a a' aa a'a; x' = (x1, x2); x = (x1a, x2a); h.valid x1 x2 \<and> h.swim_invar x1 x2; hm_valid x1a x2a \<and> h.swim_invar (hmr_\<alpha> x1a) x2a; hm_valid x1a (h.parent x2a); h.has_parent x1 x2; (ppi, ppia) \<in> Id\<rbrakk> \<Longrightarrow> (x2a, x2) \<in> nat_rel
 9. \<And>a a' aa a'a swim swima x x' x1 x2 x1a x2a ppi ppia pi pia. \<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> swim x \<le> \<Down> hmr_rel (swima x'); (x, x') \<in> ?R3 a a' aa a'a; x' = (x1, x2); x = (x1a, x2a); h.valid x1 x2 \<and> h.swim_invar x1 x2; hm_valid x1a x2a \<and> h.swim_invar (hmr_\<alpha> x1a) x2a; hm_valid x1a (h.parent x2a); h.has_parent x1 x2; (ppi, ppia) \<in> Id; (pi, pia) \<in> Id\<rbrakk> \<Longrightarrow> (\<not> ppi \<le> pi) = (\<not> ppia \<le> pia)
 10. \<And>a a' aa a'a swim swima x x' x1 x2 x1a x2a ppi ppia pi pia. \<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> swim x \<le> \<Down> hmr_rel (swima x'); (x, x') \<in> ?R3 a a' aa a'a; x' = (x1, x2); x = (x1a, x2a); h.valid x1 x2 \<and> h.swim_invar x1 x2; hm_valid x1a x2a \<and> h.swim_invar (hmr_\<alpha> x1a) x2a; hm_valid x1a (h.parent x2a); h.has_parent x1 x2; (ppi, ppia) \<in> Id; (pi, pia) \<in> Id; \<not> ppi \<le> pi; \<not> ppia \<le> pia\<rbrakk> \<Longrightarrow> (x1a, x1) \<in> hmr_rel
A total of 15 subgoals...
[PROOF STEP]
apply refine_dref_type
[PROOF STATE]
proof (prove)
goal (15 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 swim swima 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> swim x \<le> \<Down> hmr_rel (swima x'); (x, x') \<in> hmr_rel \<times>\<^sub>r nat_rel; x' = (x1, x2); x = (x1a, x2a); h.valid x1 x2 \<and> h.swim_invar x1 x2\<rbrakk> \<Longrightarrow> hm_valid x1a x2a
 3. \<And>a a' aa a'a swim swima 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> swim x \<le> \<Down> hmr_rel (swima x'); (x, x') \<in> hmr_rel \<times>\<^sub>r nat_rel; x' = (x1, x2); x = (x1a, x2a); h.valid x1 x2 \<and> h.swim_invar x1 x2\<rbrakk> \<Longrightarrow> h.swim_invar (hmr_\<alpha> x1a) x2a
 4. \<And>a a' aa a'a swim swima 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> swim x \<le> \<Down> hmr_rel (swima x'); (x, x') \<in> hmr_rel \<times>\<^sub>r nat_rel; x' = (x1, x2); x = (x1a, x2a); h.valid x1 x2 \<and> h.swim_invar x1 x2; hm_valid x1a x2a \<and> h.swim_invar (hmr_\<alpha> x1a) x2a\<rbrakk> \<Longrightarrow> hm_valid x1a (h.parent x2a) = h.has_parent x1 x2
 5. \<And>a a' aa a'a swim swima 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> swim x \<le> \<Down> hmr_rel (swima x'); (x, x') \<in> hmr_rel \<times>\<^sub>r nat_rel; x' = (x1, x2); x = (x1a, x2a); h.valid x1 x2 \<and> h.swim_invar x1 x2; hm_valid x1a x2a \<and> h.swim_invar (hmr_\<alpha> x1a) x2a; hm_valid x1a (h.parent x2a); h.has_parent x1 x2\<rbrakk> \<Longrightarrow> (x1a, x1) \<in> hmr_rel
 6. \<And>a a' aa a'a swim swima 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> swim x \<le> \<Down> hmr_rel (swima x'); (x, x') \<in> hmr_rel \<times>\<^sub>r nat_rel; x' = (x1, x2); x = (x1a, x2a); h.valid x1 x2 \<and> h.swim_invar x1 x2; hm_valid x1a x2a \<and> h.swim_invar (hmr_\<alpha> x1a) x2a; hm_valid x1a (h.parent x2a); h.has_parent x1 x2\<rbrakk> \<Longrightarrow> (h.parent x2a, h.parent x2) \<in> nat_rel
 7. \<And>a a' aa a'a swim swima x x' x1 x2 x1a x2a ppi ppia. \<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> swim x \<le> \<Down> hmr_rel (swima x'); (x, x') \<in> hmr_rel \<times>\<^sub>r nat_rel; x' = (x1, x2); x = (x1a, x2a); h.valid x1 x2 \<and> h.swim_invar x1 x2; hm_valid x1a x2a \<and> h.swim_invar (hmr_\<alpha> x1a) x2a; hm_valid x1a (h.parent x2a); h.has_parent x1 x2; (ppi, ppia) \<in> Id\<rbrakk> \<Longrightarrow> (x1a, x1) \<in> hmr_rel
 8. \<And>a a' aa a'a swim swima x x' x1 x2 x1a x2a ppi ppia. \<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> swim x \<le> \<Down> hmr_rel (swima x'); (x, x') \<in> hmr_rel \<times>\<^sub>r nat_rel; x' = (x1, x2); x = (x1a, x2a); h.valid x1 x2 \<and> h.swim_invar x1 x2; hm_valid x1a x2a \<and> h.swim_invar (hmr_\<alpha> x1a) x2a; hm_valid x1a (h.parent x2a); h.has_parent x1 x2; (ppi, ppia) \<in> Id\<rbrakk> \<Longrightarrow> (x2a, x2) \<in> nat_rel
 9. \<And>a a' aa a'a swim swima x x' x1 x2 x1a x2a ppi ppia pi pia. \<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> swim x \<le> \<Down> hmr_rel (swima x'); (x, x') \<in> hmr_rel \<times>\<^sub>r nat_rel; x' = (x1, x2); x = (x1a, x2a); h.valid x1 x2 \<and> h.swim_invar x1 x2; hm_valid x1a x2a \<and> h.swim_invar (hmr_\<alpha> x1a) x2a; hm_valid x1a (h.parent x2a); h.has_parent x1 x2; (ppi, ppia) \<in> Id; (pi, pia) \<in> Id\<rbrakk> \<Longrightarrow> (\<not> ppi \<le> pi) = (\<not> ppia \<le> pia)
 10. \<And>a a' aa a'a swim swima x x' x1 x2 x1a x2a ppi ppia pi pia. \<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> swim x \<le> \<Down> hmr_rel (swima x'); (x, x') \<in> hmr_rel \<times>\<^sub>r nat_rel; x' = (x1, x2); x = (x1a, x2a); h.valid x1 x2 \<and> h.swim_invar x1 x2; hm_valid x1a x2a \<and> h.swim_invar (hmr_\<alpha> x1a) x2a; hm_valid x1a (h.parent x2a); h.has_parent x1 x2; (ppi, ppia) \<in> Id; (pi, pia) \<in> Id; \<not> ppi \<le> pi; \<not> ppia \<le> pia\<rbrakk> \<Longrightarrow> (x1a, x1) \<in> hmr_rel
A total of 15 subgoals...
[PROOF STEP]
apply (clarsimp_all simp: hm_valid_refine[param_fo, THEN IdD])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b a' swim swima x1 x2 ad bd. \<lbrakk>((a, b), a') \<in> hmr_rel; \<And>a b ba aa. ((a, b), aa) \<in> hmr_rel \<Longrightarrow> swim ((a, b), ba) \<le> \<Down> hmr_rel (swima (aa, ba)); ((ad, bd), x1) \<in> hmr_rel; h.valid x1 x2; h.swim_invar x1 x2\<rbrakk> \<Longrightarrow> h.swim_invar (hmr_\<alpha> (ad, bd)) x2
[PROOF STEP]
apply (simp add: hmr_rel_def in_br_conv)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma hm_swim_op_nofail_imp_valid:
      "nofail (hm_swim_op hm i) \<Longrightarrow> hm_valid hm i \<and> h.swim_invar (hmr_\<alpha> hm) i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nofail (hm_swim_op hm i) \<Longrightarrow> hm_valid hm i \<and> h.swim_invar (hmr_\<alpha> hm) i
[PROOF STEP]
unfolding hm_swim_op_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nofail (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)) \<Longrightarrow> hm_valid hm i \<and> h.swim_invar (hmr_\<alpha> 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, 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. 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)) (h, h.parent i)) else RETURN h)) else RETURN h)) \<Longrightarrow> hm_valid hm i \<and> h.swim_invar (hmr_\<alpha> hm) i
[PROOF STEP]
by (auto simp: refine_pw_simps)