[STATEMENT]
lemma hm_pop_min_aref': "(hm_pop_min_op', mop_pm_pop_min prio) \<in> heapmap_rel \<rightarrow> \<langle>(Id\<times>\<^sub>rId) \<times>\<^sub>r heapmap_rel\<rangle>nres_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (hm_pop_min_op', mop_pm_pop_min prio) \<in> heapmap_rel \<rightarrow> \<langle>(Id \<times>\<^sub>r Id) \<times>\<^sub>r heapmap_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> heapmap_rel \<Longrightarrow> hm_pop_min_op' a \<le> \<Down> ((Id \<times>\<^sub>r Id) \<times>\<^sub>r heapmap_rel) (mop_pm_pop_min prio a')
[PROOF STEP]
apply (frule heapmap_hmr_relI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a'. \<lbrakk>(a, a') \<in> heapmap_rel; (a, hmr_\<alpha> a) \<in> hmr_rel\<rbrakk> \<Longrightarrow> hm_pop_min_op' a \<le> \<Down> ((Id \<times>\<^sub>r Id) \<times>\<^sub>r heapmap_rel) (mop_pm_pop_min prio a')
[PROOF STEP]
unfolding mop_pm_pop_min_alt
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a'. \<lbrakk>(a, a') \<in> heapmap_rel; (a, hmr_\<alpha> a) \<in> hmr_rel\<rbrakk> \<Longrightarrow> hm_pop_min_op' a \<le> \<Down> ((Id \<times>\<^sub>r Id) \<times>\<^sub>r heapmap_rel) (ASSERT (pre_pm_pop_min a') \<bind> (\<lambda>_. PR_CONST (op_pm_pop_min prio) a'))
[PROOF STEP]
apply (intro ASSERT_refine_right)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a'. \<lbrakk>(a, a') \<in> heapmap_rel; (a, hmr_\<alpha> a) \<in> hmr_rel; pre_pm_pop_min a'\<rbrakk> \<Longrightarrow> hm_pop_min_op' a \<le> \<Down> ((Id \<times>\<^sub>r Id) \<times>\<^sub>r heapmap_rel) (PR_CONST (op_pm_pop_min prio) a')
[PROOF STEP]
apply (rule heapmap_nres_rel_prodI')
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a a'. \<lbrakk>(a, a') \<in> heapmap_rel; (a, hmr_\<alpha> a) \<in> hmr_rel; pre_pm_pop_min a'\<rbrakk> \<Longrightarrow> hm_pop_min_op' a \<le> \<Down> (?S5 a a' \<times>\<^sub>r hmr_rel) (?h'x5 a a')
 2. \<And>a a'. \<lbrakk>(a, a') \<in> heapmap_rel; (a, hmr_\<alpha> a) \<in> hmr_rel; pre_pm_pop_min a'\<rbrakk> \<Longrightarrow> ?h'x5 a a' \<le> SPEC (?\<Phi>5 a a')
 3. \<And>a a' h' r. \<lbrakk>(a, a') \<in> heapmap_rel; (a, hmr_\<alpha> a) \<in> hmr_rel; pre_pm_pop_min a'; ?\<Phi>5 a a' (r, h')\<rbrakk> \<Longrightarrow> h.heap_invar h'
 4. \<And>a a'. \<lbrakk>(a, a') \<in> heapmap_rel; (a, hmr_\<alpha> a) \<in> hmr_rel; pre_pm_pop_min a'\<rbrakk> \<Longrightarrow> hm_pop_min_op' a \<le>\<^sub>n SPEC (\<lambda>(r, hm'). (\<exists>r'. (r, r') \<in> ?S5 a a' \<and> ?\<Phi>5 a a' (r', hmr_\<alpha> hm')) \<and> hmr_invar hm' \<longrightarrow> RETURN (r, heapmap_\<alpha> hm') \<le> \<Down> ((Id \<times>\<^sub>r Id) \<times>\<^sub>r Id) (PR_CONST (op_pm_pop_min prio) a'))
[PROOF STEP]
apply (erule hm_pop_min_op_refine')
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a a'. \<lbrakk>(a, a') \<in> heapmap_rel; (a, hmr_\<alpha> a) \<in> hmr_rel; pre_pm_pop_min a'\<rbrakk> \<Longrightarrow> h.pop_min_op (hmr_\<alpha> a) \<le> SPEC (?\<Phi>5 a a')
 2. \<And>a a' h' r. \<lbrakk>(a, a') \<in> heapmap_rel; (a, hmr_\<alpha> a) \<in> hmr_rel; pre_pm_pop_min a'; ?\<Phi>5 a a' (r, h')\<rbrakk> \<Longrightarrow> h.heap_invar h'
 3. \<And>a a'. \<lbrakk>(a, a') \<in> heapmap_rel; (a, hmr_\<alpha> a) \<in> hmr_rel; pre_pm_pop_min a'\<rbrakk> \<Longrightarrow> hm_pop_min_op' a \<le>\<^sub>n SPEC (\<lambda>(r, hm'). (\<exists>r'. (r, r') \<in> kvi_rel a 1 \<and> ?\<Phi>5 a a' (r', hmr_\<alpha> hm')) \<and> hmr_invar hm' \<longrightarrow> RETURN (r, heapmap_\<alpha> hm') \<le> \<Down> ((Id \<times>\<^sub>r Id) \<times>\<^sub>r Id) (PR_CONST (op_pm_pop_min prio) a'))
[PROOF STEP]
apply (unfold heapmap_rel_def hmr_rel_def in_br_conv) []
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a a'. \<lbrakk>a' = heapmap_\<alpha> a \<and> heapmap_invar a; hmr_\<alpha> a = hmr_\<alpha> a \<and> hmr_invar a; pre_pm_pop_min a'\<rbrakk> \<Longrightarrow> h.pop_min_op (hmr_\<alpha> a) \<le> SPEC (?\<Phi>5 a a')
 2. \<And>a a' h' r. \<lbrakk>(a, a') \<in> heapmap_rel; (a, hmr_\<alpha> a) \<in> hmr_rel; pre_pm_pop_min a'; ?\<Phi>5 a a' (r, h')\<rbrakk> \<Longrightarrow> h.heap_invar h'
 3. \<And>a a'. \<lbrakk>(a, a') \<in> heapmap_rel; (a, hmr_\<alpha> a) \<in> hmr_rel; pre_pm_pop_min a'\<rbrakk> \<Longrightarrow> hm_pop_min_op' a \<le>\<^sub>n SPEC (\<lambda>(r, hm'). (\<exists>r'. (r, r') \<in> kvi_rel a 1 \<and> ?\<Phi>5 a a' (r', hmr_\<alpha> hm')) \<and> hmr_invar hm' \<longrightarrow> RETURN (r, heapmap_\<alpha> hm') \<le> \<Down> ((Id \<times>\<^sub>r Id) \<times>\<^sub>r Id) (PR_CONST (op_pm_pop_min prio) a'))
[PROOF STEP]
apply (rule h.pop_min_op_correct)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a a'. \<lbrakk>a' = heapmap_\<alpha> a \<and> heapmap_invar a; hmr_\<alpha> a = hmr_\<alpha> a \<and> hmr_invar a; pre_pm_pop_min a'\<rbrakk> \<Longrightarrow> h.heap_invar (hmr_\<alpha> a)
 2. \<And>a a'. \<lbrakk>a' = heapmap_\<alpha> a \<and> heapmap_invar a; hmr_\<alpha> a = hmr_\<alpha> a \<and> hmr_invar a; pre_pm_pop_min a'\<rbrakk> \<Longrightarrow> h.\<alpha> (hmr_\<alpha> a) \<noteq> {#}
 3. \<And>a a' h' r. \<lbrakk>(a, a') \<in> heapmap_rel; (a, hmr_\<alpha> a) \<in> hmr_rel; pre_pm_pop_min a'; case (r, h') of (v, h') \<Rightarrow> h.heap_invar h' \<and> v \<in># h.\<alpha> (hmr_\<alpha> a) \<and> h.\<alpha> h' = h.\<alpha> (hmr_\<alpha> a) - {#v#} \<and> (\<forall>v'\<in>#h.\<alpha> (hmr_\<alpha> a). prio v \<le> prio v')\<rbrakk> \<Longrightarrow> h.heap_invar h'
 4. \<And>a a'. \<lbrakk>(a, a') \<in> heapmap_rel; (a, hmr_\<alpha> a) \<in> hmr_rel; pre_pm_pop_min a'\<rbrakk> \<Longrightarrow> hm_pop_min_op' a \<le>\<^sub>n SPEC (\<lambda>(r, hm'). (\<exists>r'. (r, r') \<in> kvi_rel a 1 \<and> (case (r', hmr_\<alpha> hm') of (v, h') \<Rightarrow> h.heap_invar h' \<and> v \<in># h.\<alpha> (hmr_\<alpha> a) \<and> h.\<alpha> h' = h.\<alpha> (hmr_\<alpha> a) - {#v#} \<and> (\<forall>v'\<in>#h.\<alpha> (hmr_\<alpha> a). prio v \<le> prio v'))) \<and> hmr_invar hm' \<longrightarrow> RETURN (r, heapmap_\<alpha> hm') \<le> \<Down> ((Id \<times>\<^sub>r Id) \<times>\<^sub>r Id) (PR_CONST (op_pm_pop_min prio) a'))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a a'. \<lbrakk>a' = heapmap_\<alpha> a \<and> heapmap_invar a; hmr_\<alpha> a = hmr_\<alpha> a \<and> hmr_invar a; pre_pm_pop_min a'\<rbrakk> \<Longrightarrow> h.\<alpha> (hmr_\<alpha> a) \<noteq> {#}
 2. \<And>a a' h' r. \<lbrakk>(a, a') \<in> heapmap_rel; (a, hmr_\<alpha> a) \<in> hmr_rel; pre_pm_pop_min a'; case (r, h') of (v, h') \<Rightarrow> h.heap_invar h' \<and> v \<in># h.\<alpha> (hmr_\<alpha> a) \<and> h.\<alpha> h' = h.\<alpha> (hmr_\<alpha> a) - {#v#} \<and> (\<forall>v'\<in>#h.\<alpha> (hmr_\<alpha> a). prio v \<le> prio v')\<rbrakk> \<Longrightarrow> h.heap_invar h'
 3. \<And>a a'. \<lbrakk>(a, a') \<in> heapmap_rel; (a, hmr_\<alpha> a) \<in> hmr_rel; pre_pm_pop_min a'\<rbrakk> \<Longrightarrow> hm_pop_min_op' a \<le>\<^sub>n SPEC (\<lambda>(r, hm'). (\<exists>r'. (r, r') \<in> kvi_rel a 1 \<and> (case (r', hmr_\<alpha> hm') of (v, h') \<Rightarrow> h.heap_invar h' \<and> v \<in># h.\<alpha> (hmr_\<alpha> a) \<and> h.\<alpha> h' = h.\<alpha> (hmr_\<alpha> a) - {#v#} \<and> (\<forall>v'\<in>#h.\<alpha> (hmr_\<alpha> a). prio v \<le> prio v'))) \<and> hmr_invar hm' \<longrightarrow> RETURN (r, heapmap_\<alpha> hm') \<le> \<Down> ((Id \<times>\<^sub>r Id) \<times>\<^sub>r Id) (PR_CONST (op_pm_pop_min prio) a'))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a a' h' r. \<lbrakk>(a, a') \<in> heapmap_rel; (a, hmr_\<alpha> a) \<in> hmr_rel; pre_pm_pop_min a'; case (r, h') of (v, h') \<Rightarrow> h.heap_invar h' \<and> v \<in># h.\<alpha> (hmr_\<alpha> a) \<and> h.\<alpha> h' = h.\<alpha> (hmr_\<alpha> a) - {#v#} \<and> (\<forall>v'\<in>#h.\<alpha> (hmr_\<alpha> a). prio v \<le> prio v')\<rbrakk> \<Longrightarrow> h.heap_invar h'
 2. \<And>a a'. \<lbrakk>(a, a') \<in> heapmap_rel; (a, hmr_\<alpha> a) \<in> hmr_rel; pre_pm_pop_min a'\<rbrakk> \<Longrightarrow> hm_pop_min_op' a \<le>\<^sub>n SPEC (\<lambda>(r, hm'). (\<exists>r'. (r, r') \<in> kvi_rel a 1 \<and> (case (r', hmr_\<alpha> hm') of (v, h') \<Rightarrow> h.heap_invar h' \<and> v \<in># h.\<alpha> (hmr_\<alpha> a) \<and> h.\<alpha> h' = h.\<alpha> (hmr_\<alpha> a) - {#v#} \<and> (\<forall>v'\<in>#h.\<alpha> (hmr_\<alpha> a). prio v \<le> prio v'))) \<and> hmr_invar hm' \<longrightarrow> RETURN (r, heapmap_\<alpha> hm') \<le> \<Down> ((Id \<times>\<^sub>r Id) \<times>\<^sub>r Id) (PR_CONST (op_pm_pop_min prio) a'))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a'. \<lbrakk>(a, a') \<in> heapmap_rel; (a, hmr_\<alpha> a) \<in> hmr_rel; pre_pm_pop_min a'\<rbrakk> \<Longrightarrow> hm_pop_min_op' a \<le>\<^sub>n SPEC (\<lambda>(r, hm'). (\<exists>r'. (r, r') \<in> kvi_rel a 1 \<and> (case (r', hmr_\<alpha> hm') of (v, h') \<Rightarrow> h.heap_invar h' \<and> v \<in># h.\<alpha> (hmr_\<alpha> a) \<and> h.\<alpha> h' = h.\<alpha> (hmr_\<alpha> a) - {#v#} \<and> (\<forall>v'\<in>#h.\<alpha> (hmr_\<alpha> a). prio v \<le> prio v'))) \<and> hmr_invar hm' \<longrightarrow> RETURN (r, heapmap_\<alpha> hm') \<le> \<Down> ((Id \<times>\<^sub>r Id) \<times>\<^sub>r Id) (PR_CONST (op_pm_pop_min prio) a'))
[PROOF STEP]
apply (clarsimp simp: ex_in_kvi_rel_conv split: prod.splits)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b a'. \<lbrakk>((a, b), a') \<in> heapmap_rel; ((a, b), hmr_\<alpha> (a, b)) \<in> hmr_rel; Map.empty \<noteq> a'\<rbrakk> \<Longrightarrow> hm_pop_min_op' (a, b) \<le>\<^sub>n SPEC (\<lambda>(r, hm'). fst r = hm_key_of (a, b) (Suc 0) \<and> h.heap_invar (hmr_\<alpha> hm') \<and> snd r \<in> set (hmr_\<alpha> (a, b)) \<and> h.\<alpha> (hmr_\<alpha> hm') = h.\<alpha> (hmr_\<alpha> (a, b)) - {#snd r#} \<and> (\<forall>v'\<in>set (hmr_\<alpha> (a, b)). prio (snd r) \<le> prio v') \<and> hmr_invar hm' \<longrightarrow> (case r of (k, v) \<Rightarrow> \<lambda>m'. a' k = Some v \<and> m' = a'(k := None) \<and> (\<forall>k' v'. a' k' = Some v' \<longrightarrow> prio v \<le> prio v')) (heapmap_\<alpha> hm'))
[PROOF STEP]
unfolding hm_pop_min_op'_def hm_kv_of_op_def hm_key_of_op_unfold
          hm_the_lookup_op_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b a'. \<lbrakk>((a, b), a') \<in> heapmap_rel; ((a, b), hmr_\<alpha> (a, b)) \<in> hmr_rel; Map.empty \<noteq> a'\<rbrakk> \<Longrightarrow> ASSERT (heapmap_invar (a, b)) \<bind> (\<lambda>_. ASSERT (hm_valid (a, b) 1) \<bind> (\<lambda>_. ASSERT (hm_valid (a, b) 1 \<and> hmr_invar (a, b)) \<bind> (\<lambda>_. ASSERT (hm_valid (a, b) 1) \<bind> (\<lambda>_. RETURN (hm_key_of (a, b) 1)) \<bind> (\<lambda>k. ASSERT (heapmap_\<alpha> (a, b) k \<noteq> None \<and> hmr_invar (a, b)) \<bind> (\<lambda>_. RETURN (the (heapmap_\<alpha> (a, b) k))) \<bind> (\<lambda>v. RETURN (k, v)))) \<bind> (\<lambda>kv. let l = hm_length (a, b) in hm_exch_op (a, b) 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>\<^sub>n SPEC (\<lambda>(r, hm'). fst r = hm_key_of (a, b) (Suc 0) \<and> h.heap_invar (hmr_\<alpha> hm') \<and> snd r \<in> set (hmr_\<alpha> (a, b)) \<and> h.\<alpha> (hmr_\<alpha> hm') = h.\<alpha> (hmr_\<alpha> (a, b)) - {#snd r#} \<and> (\<forall>v'\<in>set (hmr_\<alpha> (a, b)). prio (snd r) \<le> prio v') \<and> hmr_invar hm' \<longrightarrow> (case r of (k, v) \<Rightarrow> \<lambda>m'. a' k = Some v \<and> m' = a'(k := None) \<and> (\<forall>k' v'. a' k' = Some v' \<longrightarrow> prio v \<le> prio v')) (heapmap_\<alpha> hm'))
[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>a b a' x xa xb x1 x1a x2 x2a. \<lbrakk>((a, b), a') \<in> heapmap_rel; ((a, b), hmr_\<alpha> (a, b)) \<in> hmr_rel; Map.empty \<noteq> a'; heapmap_invar (a, b); hm_valid (a, b) 1; hm_valid (a, b) 1 \<and> hmr_invar (a, b); hm_valid (a, b) 1; heapmap_\<alpha> (a, b) (hm_key_of (a, b) 1) \<noteq> None \<and> hmr_invar (a, b); x \<in> {hm'. hm_valid (a, b) 1 \<and> hm_valid (a, b) (hm_length (a, b)) \<and> hm' = hm_exch (a, b) 1 (hm_length (a, b))}; xa \<in> {hm'. heapmap_\<alpha> hm' = (heapmap_\<alpha> x)(hm_key_of x (hm_length x) := None)}; hm_length (a, b) \<noteq> 1; xb \<in> {hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> xa}; x1 = (x1a, x2); ((hm_key_of (a, b) 1, the (heapmap_\<alpha> (a, b) (hm_key_of (a, b) 1))), xb) = (x1, x2a); fst x1 = hm_key_of (a, b) (Suc 0) \<and> h.heap_invar (hmr_\<alpha> x2a) \<and> snd x1 \<in> set (hmr_\<alpha> (a, b)) \<and> h.\<alpha> (hmr_\<alpha> x2a) = h.\<alpha> (hmr_\<alpha> (a, b)) - {#snd x1#} \<and> (\<forall>v'\<in>set (hmr_\<alpha> (a, b)). prio (snd x1) \<le> prio v') \<and> hmr_invar x2a\<rbrakk> \<Longrightarrow> a' x1a = Some x2
 2. \<And>a b a' x xa xb x1 x1a x2 x2a. \<lbrakk>((a, b), a') \<in> heapmap_rel; ((a, b), hmr_\<alpha> (a, b)) \<in> hmr_rel; Map.empty \<noteq> a'; heapmap_invar (a, b); hm_valid (a, b) 1; hm_valid (a, b) 1 \<and> hmr_invar (a, b); hm_valid (a, b) 1; heapmap_\<alpha> (a, b) (hm_key_of (a, b) 1) \<noteq> None \<and> hmr_invar (a, b); x \<in> {hm'. hm_valid (a, b) 1 \<and> hm_valid (a, b) (hm_length (a, b)) \<and> hm' = hm_exch (a, b) 1 (hm_length (a, b))}; xa \<in> {hm'. heapmap_\<alpha> hm' = (heapmap_\<alpha> x)(hm_key_of x (hm_length x) := None)}; hm_length (a, b) \<noteq> 1; xb \<in> {hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> xa}; x1 = (x1a, x2); ((hm_key_of (a, b) 1, the (heapmap_\<alpha> (a, b) (hm_key_of (a, b) 1))), xb) = (x1, x2a); fst x1 = hm_key_of (a, b) (Suc 0) \<and> h.heap_invar (hmr_\<alpha> x2a) \<and> snd x1 \<in> set (hmr_\<alpha> (a, b)) \<and> h.\<alpha> (hmr_\<alpha> x2a) = h.\<alpha> (hmr_\<alpha> (a, b)) - {#snd x1#} \<and> (\<forall>v'\<in>set (hmr_\<alpha> (a, b)). prio (snd x1) \<le> prio v') \<and> hmr_invar x2a\<rbrakk> \<Longrightarrow> heapmap_\<alpha> x2a = a'(x1a := None)
 3. \<And>a b a' x xa xb x1 x1a x2 x2a k' v'. \<lbrakk>((a, b), a') \<in> heapmap_rel; ((a, b), hmr_\<alpha> (a, b)) \<in> hmr_rel; Map.empty \<noteq> a'; heapmap_invar (a, b); hm_valid (a, b) 1; hm_valid (a, b) 1 \<and> hmr_invar (a, b); hm_valid (a, b) 1; heapmap_\<alpha> (a, b) (hm_key_of (a, b) 1) \<noteq> None \<and> hmr_invar (a, b); x \<in> {hm'. hm_valid (a, b) 1 \<and> hm_valid (a, b) (hm_length (a, b)) \<and> hm' = hm_exch (a, b) 1 (hm_length (a, b))}; xa \<in> {hm'. heapmap_\<alpha> hm' = (heapmap_\<alpha> x)(hm_key_of x (hm_length x) := None)}; hm_length (a, b) \<noteq> 1; xb \<in> {hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> xa}; x1 = (x1a, x2); ((hm_key_of (a, b) 1, the (heapmap_\<alpha> (a, b) (hm_key_of (a, b) 1))), xb) = (x1, x2a); fst x1 = hm_key_of (a, b) (Suc 0) \<and> h.heap_invar (hmr_\<alpha> x2a) \<and> snd x1 \<in> set (hmr_\<alpha> (a, b)) \<and> h.\<alpha> (hmr_\<alpha> x2a) = h.\<alpha> (hmr_\<alpha> (a, b)) - {#snd x1#} \<and> (\<forall>v'\<in>set (hmr_\<alpha> (a, b)). prio (snd x1) \<le> prio v') \<and> hmr_invar x2a; a' k' = Some v'\<rbrakk> \<Longrightarrow> prio x2 \<le> prio v'
 4. \<And>a b a' x xa x1 x1a x2 x2a. \<lbrakk>((a, b), a') \<in> heapmap_rel; ((a, b), hmr_\<alpha> (a, b)) \<in> hmr_rel; Map.empty \<noteq> a'; heapmap_invar (a, b); hm_valid (a, b) 1; hm_valid (a, b) 1 \<and> hmr_invar (a, b); hm_valid (a, b) 1; heapmap_\<alpha> (a, b) (hm_key_of (a, b) 1) \<noteq> None \<and> hmr_invar (a, b); x \<in> {hm'. hm_valid (a, b) 1 \<and> hm_valid (a, b) (hm_length (a, b)) \<and> hm' = hm_exch (a, b) 1 (hm_length (a, b))}; xa \<in> {hm'. heapmap_\<alpha> hm' = (heapmap_\<alpha> x)(hm_key_of x (hm_length x) := None)}; \<not> hm_length (a, b) \<noteq> 1; x1 = (x1a, x2); ((hm_key_of (a, b) 1, the (heapmap_\<alpha> (a, b) (hm_key_of (a, b) 1))), xa) = (x1, x2a); fst x1 = hm_key_of (a, b) (Suc 0) \<and> h.heap_invar (hmr_\<alpha> x2a) \<and> snd x1 \<in> set (hmr_\<alpha> (a, b)) \<and> h.\<alpha> (hmr_\<alpha> x2a) = h.\<alpha> (hmr_\<alpha> (a, b)) - {#snd x1#} \<and> (\<forall>v'\<in>set (hmr_\<alpha> (a, b)). prio (snd x1) \<le> prio v') \<and> hmr_invar x2a\<rbrakk> \<Longrightarrow> a' x1a = Some x2
 5. \<And>a b a' x xa x1 x1a x2 x2a. \<lbrakk>((a, b), a') \<in> heapmap_rel; ((a, b), hmr_\<alpha> (a, b)) \<in> hmr_rel; Map.empty \<noteq> a'; heapmap_invar (a, b); hm_valid (a, b) 1; hm_valid (a, b) 1 \<and> hmr_invar (a, b); hm_valid (a, b) 1; heapmap_\<alpha> (a, b) (hm_key_of (a, b) 1) \<noteq> None \<and> hmr_invar (a, b); x \<in> {hm'. hm_valid (a, b) 1 \<and> hm_valid (a, b) (hm_length (a, b)) \<and> hm' = hm_exch (a, b) 1 (hm_length (a, b))}; xa \<in> {hm'. heapmap_\<alpha> hm' = (heapmap_\<alpha> x)(hm_key_of x (hm_length x) := None)}; \<not> hm_length (a, b) \<noteq> 1; x1 = (x1a, x2); ((hm_key_of (a, b) 1, the (heapmap_\<alpha> (a, b) (hm_key_of (a, b) 1))), xa) = (x1, x2a); fst x1 = hm_key_of (a, b) (Suc 0) \<and> h.heap_invar (hmr_\<alpha> x2a) \<and> snd x1 \<in> set (hmr_\<alpha> (a, b)) \<and> h.\<alpha> (hmr_\<alpha> x2a) = h.\<alpha> (hmr_\<alpha> (a, b)) - {#snd x1#} \<and> (\<forall>v'\<in>set (hmr_\<alpha> (a, b)). prio (snd x1) \<le> prio v') \<and> hmr_invar x2a\<rbrakk> \<Longrightarrow> heapmap_\<alpha> x2a = a'(x1a := None)
 6. \<And>a b a' x xa x1 x1a x2 x2a k' v'. \<lbrakk>((a, b), a') \<in> heapmap_rel; ((a, b), hmr_\<alpha> (a, b)) \<in> hmr_rel; Map.empty \<noteq> a'; heapmap_invar (a, b); hm_valid (a, b) 1; hm_valid (a, b) 1 \<and> hmr_invar (a, b); hm_valid (a, b) 1; heapmap_\<alpha> (a, b) (hm_key_of (a, b) 1) \<noteq> None \<and> hmr_invar (a, b); x \<in> {hm'. hm_valid (a, b) 1 \<and> hm_valid (a, b) (hm_length (a, b)) \<and> hm' = hm_exch (a, b) 1 (hm_length (a, b))}; xa \<in> {hm'. heapmap_\<alpha> hm' = (heapmap_\<alpha> x)(hm_key_of x (hm_length x) := None)}; \<not> hm_length (a, b) \<noteq> 1; x1 = (x1a, x2); ((hm_key_of (a, b) 1, the (heapmap_\<alpha> (a, b) (hm_key_of (a, b) 1))), xa) = (x1, x2a); fst x1 = hm_key_of (a, b) (Suc 0) \<and> h.heap_invar (hmr_\<alpha> x2a) \<and> snd x1 \<in> set (hmr_\<alpha> (a, b)) \<and> h.\<alpha> (hmr_\<alpha> x2a) = h.\<alpha> (hmr_\<alpha> (a, b)) - {#snd x1#} \<and> (\<forall>v'\<in>set (hmr_\<alpha> (a, b)). prio (snd x1) \<le> prio v') \<and> hmr_invar x2a; a' k' = Some v'\<rbrakk> \<Longrightarrow> prio x2 \<le> prio v'
[PROOF STEP]
unfolding heapmap_rel_def hmr_rel_def in_br_conv
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>a b a' x xa xb x1 x1a x2 x2a. \<lbrakk>a' = heapmap_\<alpha> (a, b) \<and> heapmap_invar (a, b); hmr_\<alpha> (a, b) = hmr_\<alpha> (a, b) \<and> hmr_invar (a, b); Map.empty \<noteq> a'; heapmap_invar (a, b); hm_valid (a, b) 1; hm_valid (a, b) 1 \<and> hmr_invar (a, b); hm_valid (a, b) 1; heapmap_\<alpha> (a, b) (hm_key_of (a, b) 1) \<noteq> None \<and> hmr_invar (a, b); x \<in> {hm'. hm_valid (a, b) 1 \<and> hm_valid (a, b) (hm_length (a, b)) \<and> hm' = hm_exch (a, b) 1 (hm_length (a, b))}; xa \<in> {hm'. heapmap_\<alpha> hm' = (heapmap_\<alpha> x)(hm_key_of x (hm_length x) := None)}; hm_length (a, b) \<noteq> 1; xb \<in> {hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> xa}; x1 = (x1a, x2); ((hm_key_of (a, b) 1, the (heapmap_\<alpha> (a, b) (hm_key_of (a, b) 1))), xb) = (x1, x2a); fst x1 = hm_key_of (a, b) (Suc 0) \<and> h.heap_invar (hmr_\<alpha> x2a) \<and> snd x1 \<in> set (hmr_\<alpha> (a, b)) \<and> h.\<alpha> (hmr_\<alpha> x2a) = h.\<alpha> (hmr_\<alpha> (a, b)) - {#snd x1#} \<and> (\<forall>v'\<in>set (hmr_\<alpha> (a, b)). prio (snd x1) \<le> prio v') \<and> hmr_invar x2a\<rbrakk> \<Longrightarrow> a' x1a = Some x2
 2. \<And>a b a' x xa xb x1 x1a x2 x2a. \<lbrakk>a' = heapmap_\<alpha> (a, b) \<and> heapmap_invar (a, b); hmr_\<alpha> (a, b) = hmr_\<alpha> (a, b) \<and> hmr_invar (a, b); Map.empty \<noteq> a'; heapmap_invar (a, b); hm_valid (a, b) 1; hm_valid (a, b) 1 \<and> hmr_invar (a, b); hm_valid (a, b) 1; heapmap_\<alpha> (a, b) (hm_key_of (a, b) 1) \<noteq> None \<and> hmr_invar (a, b); x \<in> {hm'. hm_valid (a, b) 1 \<and> hm_valid (a, b) (hm_length (a, b)) \<and> hm' = hm_exch (a, b) 1 (hm_length (a, b))}; xa \<in> {hm'. heapmap_\<alpha> hm' = (heapmap_\<alpha> x)(hm_key_of x (hm_length x) := None)}; hm_length (a, b) \<noteq> 1; xb \<in> {hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> xa}; x1 = (x1a, x2); ((hm_key_of (a, b) 1, the (heapmap_\<alpha> (a, b) (hm_key_of (a, b) 1))), xb) = (x1, x2a); fst x1 = hm_key_of (a, b) (Suc 0) \<and> h.heap_invar (hmr_\<alpha> x2a) \<and> snd x1 \<in> set (hmr_\<alpha> (a, b)) \<and> h.\<alpha> (hmr_\<alpha> x2a) = h.\<alpha> (hmr_\<alpha> (a, b)) - {#snd x1#} \<and> (\<forall>v'\<in>set (hmr_\<alpha> (a, b)). prio (snd x1) \<le> prio v') \<and> hmr_invar x2a\<rbrakk> \<Longrightarrow> heapmap_\<alpha> x2a = a'(x1a := None)
 3. \<And>a b a' x xa xb x1 x1a x2 x2a k' v'. \<lbrakk>a' = heapmap_\<alpha> (a, b) \<and> heapmap_invar (a, b); hmr_\<alpha> (a, b) = hmr_\<alpha> (a, b) \<and> hmr_invar (a, b); Map.empty \<noteq> a'; heapmap_invar (a, b); hm_valid (a, b) 1; hm_valid (a, b) 1 \<and> hmr_invar (a, b); hm_valid (a, b) 1; heapmap_\<alpha> (a, b) (hm_key_of (a, b) 1) \<noteq> None \<and> hmr_invar (a, b); x \<in> {hm'. hm_valid (a, b) 1 \<and> hm_valid (a, b) (hm_length (a, b)) \<and> hm' = hm_exch (a, b) 1 (hm_length (a, b))}; xa \<in> {hm'. heapmap_\<alpha> hm' = (heapmap_\<alpha> x)(hm_key_of x (hm_length x) := None)}; hm_length (a, b) \<noteq> 1; xb \<in> {hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> xa}; x1 = (x1a, x2); ((hm_key_of (a, b) 1, the (heapmap_\<alpha> (a, b) (hm_key_of (a, b) 1))), xb) = (x1, x2a); fst x1 = hm_key_of (a, b) (Suc 0) \<and> h.heap_invar (hmr_\<alpha> x2a) \<and> snd x1 \<in> set (hmr_\<alpha> (a, b)) \<and> h.\<alpha> (hmr_\<alpha> x2a) = h.\<alpha> (hmr_\<alpha> (a, b)) - {#snd x1#} \<and> (\<forall>v'\<in>set (hmr_\<alpha> (a, b)). prio (snd x1) \<le> prio v') \<and> hmr_invar x2a; a' k' = Some v'\<rbrakk> \<Longrightarrow> prio x2 \<le> prio v'
 4. \<And>a b a' x xa x1 x1a x2 x2a. \<lbrakk>a' = heapmap_\<alpha> (a, b) \<and> heapmap_invar (a, b); hmr_\<alpha> (a, b) = hmr_\<alpha> (a, b) \<and> hmr_invar (a, b); Map.empty \<noteq> a'; heapmap_invar (a, b); hm_valid (a, b) 1; hm_valid (a, b) 1 \<and> hmr_invar (a, b); hm_valid (a, b) 1; heapmap_\<alpha> (a, b) (hm_key_of (a, b) 1) \<noteq> None \<and> hmr_invar (a, b); x \<in> {hm'. hm_valid (a, b) 1 \<and> hm_valid (a, b) (hm_length (a, b)) \<and> hm' = hm_exch (a, b) 1 (hm_length (a, b))}; xa \<in> {hm'. heapmap_\<alpha> hm' = (heapmap_\<alpha> x)(hm_key_of x (hm_length x) := None)}; \<not> hm_length (a, b) \<noteq> 1; x1 = (x1a, x2); ((hm_key_of (a, b) 1, the (heapmap_\<alpha> (a, b) (hm_key_of (a, b) 1))), xa) = (x1, x2a); fst x1 = hm_key_of (a, b) (Suc 0) \<and> h.heap_invar (hmr_\<alpha> x2a) \<and> snd x1 \<in> set (hmr_\<alpha> (a, b)) \<and> h.\<alpha> (hmr_\<alpha> x2a) = h.\<alpha> (hmr_\<alpha> (a, b)) - {#snd x1#} \<and> (\<forall>v'\<in>set (hmr_\<alpha> (a, b)). prio (snd x1) \<le> prio v') \<and> hmr_invar x2a\<rbrakk> \<Longrightarrow> a' x1a = Some x2
 5. \<And>a b a' x xa x1 x1a x2 x2a. \<lbrakk>a' = heapmap_\<alpha> (a, b) \<and> heapmap_invar (a, b); hmr_\<alpha> (a, b) = hmr_\<alpha> (a, b) \<and> hmr_invar (a, b); Map.empty \<noteq> a'; heapmap_invar (a, b); hm_valid (a, b) 1; hm_valid (a, b) 1 \<and> hmr_invar (a, b); hm_valid (a, b) 1; heapmap_\<alpha> (a, b) (hm_key_of (a, b) 1) \<noteq> None \<and> hmr_invar (a, b); x \<in> {hm'. hm_valid (a, b) 1 \<and> hm_valid (a, b) (hm_length (a, b)) \<and> hm' = hm_exch (a, b) 1 (hm_length (a, b))}; xa \<in> {hm'. heapmap_\<alpha> hm' = (heapmap_\<alpha> x)(hm_key_of x (hm_length x) := None)}; \<not> hm_length (a, b) \<noteq> 1; x1 = (x1a, x2); ((hm_key_of (a, b) 1, the (heapmap_\<alpha> (a, b) (hm_key_of (a, b) 1))), xa) = (x1, x2a); fst x1 = hm_key_of (a, b) (Suc 0) \<and> h.heap_invar (hmr_\<alpha> x2a) \<and> snd x1 \<in> set (hmr_\<alpha> (a, b)) \<and> h.\<alpha> (hmr_\<alpha> x2a) = h.\<alpha> (hmr_\<alpha> (a, b)) - {#snd x1#} \<and> (\<forall>v'\<in>set (hmr_\<alpha> (a, b)). prio (snd x1) \<le> prio v') \<and> hmr_invar x2a\<rbrakk> \<Longrightarrow> heapmap_\<alpha> x2a = a'(x1a := None)
 6. \<And>a b a' x xa x1 x1a x2 x2a k' v'. \<lbrakk>a' = heapmap_\<alpha> (a, b) \<and> heapmap_invar (a, b); hmr_\<alpha> (a, b) = hmr_\<alpha> (a, b) \<and> hmr_invar (a, b); Map.empty \<noteq> a'; heapmap_invar (a, b); hm_valid (a, b) 1; hm_valid (a, b) 1 \<and> hmr_invar (a, b); hm_valid (a, b) 1; heapmap_\<alpha> (a, b) (hm_key_of (a, b) 1) \<noteq> None \<and> hmr_invar (a, b); x \<in> {hm'. hm_valid (a, b) 1 \<and> hm_valid (a, b) (hm_length (a, b)) \<and> hm' = hm_exch (a, b) 1 (hm_length (a, b))}; xa \<in> {hm'. heapmap_\<alpha> hm' = (heapmap_\<alpha> x)(hm_key_of x (hm_length x) := None)}; \<not> hm_length (a, b) \<noteq> 1; x1 = (x1a, x2); ((hm_key_of (a, b) 1, the (heapmap_\<alpha> (a, b) (hm_key_of (a, b) 1))), xa) = (x1, x2a); fst x1 = hm_key_of (a, b) (Suc 0) \<and> h.heap_invar (hmr_\<alpha> x2a) \<and> snd x1 \<in> set (hmr_\<alpha> (a, b)) \<and> h.\<alpha> (hmr_\<alpha> x2a) = h.\<alpha> (hmr_\<alpha> (a, b)) - {#snd x1#} \<and> (\<forall>v'\<in>set (hmr_\<alpha> (a, b)). prio (snd x1) \<le> prio v') \<and> hmr_invar x2a; a' k' = Some v'\<rbrakk> \<Longrightarrow> prio x2 \<le> prio v'
[PROOF STEP]
apply (auto intro: ranI)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in -) swap_empty_iff[iff]: "swap l i j = [] \<longleftrightarrow> l=[]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (swap l i j = []) = (l = [])
[PROOF STEP]
by (auto simp: swap_def)


[STATEMENT]
lemma (in heapstruct)
      butlast_exch_last: "butlast (exch h i (length h)) = update (butlast h) i (last h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. butlast (exch h i (length h)) = update (butlast h) i (last h)
[PROOF STEP]
unfolding exch_def update_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. butlast (swap h (i - 1) (length h - 1)) = (butlast h)[i - 1 := last h]
[PROOF STEP]
apply (cases h rule: rev_cases)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. h = [] \<Longrightarrow> butlast (swap h (i - 1) (length h - 1)) = (butlast h)[i - 1 := last h]
 2. \<And>ys y. h = ys @ [y] \<Longrightarrow> butlast (swap h (i - 1) (length h - 1)) = (butlast h)[i - 1 := last h]
[PROOF STEP]
apply (auto simp: swap_def butlast_list_update)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in heapstruct) remove_op_invar:
      "\<lbrakk> heap_invar h; valid h i \<rbrakk> \<Longrightarrow> remove_op i h \<le> SPEC heap_invar"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_invar h; valid h i\<rbrakk> \<Longrightarrow> remove_op i h \<le> SPEC heap_invar
[PROOF STEP]
unfolding remove_op_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_invar h; valid h i\<rbrakk> \<Longrightarrow> ASSERT (heap_invar h) \<bind> (\<lambda>_. ASSERT (valid h i) \<bind> (\<lambda>_. let l = length h in exch_op h i l \<bind> (\<lambda>h. butlast_op h \<bind> (\<lambda>h. if i \<noteq> l then repair_op h i else RETURN h)))) \<le> SPEC heap_invar
[PROOF STEP]
apply refine_vcg
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>heap_invar h; valid h i; heap_invar h; valid h i\<rbrakk> \<Longrightarrow> valid h (length h)
 2. \<And>x. \<lbrakk>heap_invar h; valid h i; heap_invar h; valid h i; x = exch h i (length h)\<rbrakk> \<Longrightarrow> x \<noteq> []
 3. \<And>x xa. \<lbrakk>heap_invar h; valid h i; heap_invar h; valid h i; x = exch h i (length h); xa = butlast x; i \<noteq> length h\<rbrakk> \<Longrightarrow> repair_op xa i \<le> SPEC heap_invar
 4. \<And>x xa. \<lbrakk>heap_invar h; valid h i; heap_invar h; valid h i; x = exch h i (length h); xa = butlast x; \<not> i \<noteq> length h\<rbrakk> \<Longrightarrow> heap_invar xa
[PROOF STEP]
apply (auto simp: valid_def) []
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>heap_invar h; valid h i; heap_invar h; valid h i; x = exch h i (length h)\<rbrakk> \<Longrightarrow> x \<noteq> []
 2. \<And>x xa. \<lbrakk>heap_invar h; valid h i; heap_invar h; valid h i; x = exch h i (length h); xa = butlast x; i \<noteq> length h\<rbrakk> \<Longrightarrow> repair_op xa i \<le> SPEC heap_invar
 3. \<And>x xa. \<lbrakk>heap_invar h; valid h i; heap_invar h; valid h i; x = exch h i (length h); xa = butlast x; \<not> i \<noteq> length h\<rbrakk> \<Longrightarrow> heap_invar xa
[PROOF STEP]
apply (auto simp: valid_def exch_def) []
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>heap_invar h; valid h i; heap_invar h; valid h i; x = exch h i (length h); xa = butlast x; i \<noteq> length h\<rbrakk> \<Longrightarrow> repair_op xa i \<le> SPEC heap_invar
 2. \<And>x xa. \<lbrakk>heap_invar h; valid h i; heap_invar h; valid h i; x = exch h i (length h); xa = butlast x; \<not> i \<noteq> length h\<rbrakk> \<Longrightarrow> heap_invar xa
[PROOF STEP]
apply (simp add: butlast_exch_last)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>heap_invar h; valid h i; x = exch h i (length h); xa = update (butlast h) i (last h); i \<noteq> length h\<rbrakk> \<Longrightarrow> repair_op (update (butlast h) i (last h)) i \<le> SPEC heap_invar
 2. \<And>x xa. \<lbrakk>heap_invar h; valid h i; heap_invar h; valid h i; x = exch h i (length h); xa = butlast x; \<not> i \<noteq> length h\<rbrakk> \<Longrightarrow> heap_invar xa
[PROOF STEP]
apply refine_vcg
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x xa. \<lbrakk>heap_invar h; valid h i; x = exch h i (length h); xa = update (butlast h) i (last h); i \<noteq> length h\<rbrakk> \<Longrightarrow> heap_invar (butlast h)
 2. \<And>x xa. \<lbrakk>heap_invar h; valid h i; x = exch h i (length h); xa = update (butlast h) i (last h); i \<noteq> length h\<rbrakk> \<Longrightarrow> valid (butlast h) i
 3. \<And>x xa xb. \<lbrakk>heap_invar h; valid h i; x = exch h i (length h); xa = update (butlast h) i (last h); i \<noteq> length h; heap_invar xb \<and> \<alpha> xb = \<alpha> (update (butlast h) i (last h)) \<and> length xb = length (butlast h)\<rbrakk> \<Longrightarrow> heap_invar xb
 4. \<And>x xa. \<lbrakk>heap_invar h; valid h i; heap_invar h; valid h i; x = exch h i (length h); xa = butlast x; \<not> i \<noteq> length h\<rbrakk> \<Longrightarrow> heap_invar xa
[PROOF STEP]
apply auto []
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x xa. \<lbrakk>heap_invar h; valid h i; x = exch h i (length h); xa = update (butlast h) i (last h); i \<noteq> length h\<rbrakk> \<Longrightarrow> valid (butlast h) i
 2. \<And>x xa xb. \<lbrakk>heap_invar h; valid h i; x = exch h i (length h); xa = update (butlast h) i (last h); i \<noteq> length h; heap_invar xb \<and> \<alpha> xb = \<alpha> (update (butlast h) i (last h)) \<and> length xb = length (butlast h)\<rbrakk> \<Longrightarrow> heap_invar xb
 3. \<And>x xa. \<lbrakk>heap_invar h; valid h i; heap_invar h; valid h i; x = exch h i (length h); xa = butlast x; \<not> i \<noteq> length h\<rbrakk> \<Longrightarrow> heap_invar xa
[PROOF STEP]
apply auto []
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>heap_invar h; valid h i; i \<noteq> length h\<rbrakk> \<Longrightarrow> i < length h
 2. \<And>x xa xb. \<lbrakk>heap_invar h; valid h i; x = exch h i (length h); xa = update (butlast h) i (last h); i \<noteq> length h; heap_invar xb \<and> \<alpha> xb = \<alpha> (update (butlast h) i (last h)) \<and> length xb = length (butlast h)\<rbrakk> \<Longrightarrow> heap_invar xb
 3. \<And>x xa. \<lbrakk>heap_invar h; valid h i; heap_invar h; valid h i; x = exch h i (length h); xa = butlast x; \<not> i \<noteq> length h\<rbrakk> \<Longrightarrow> heap_invar xa
[PROOF STEP]
apply (auto simp: valid_def) []
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa xb. \<lbrakk>heap_invar h; valid h i; x = exch h i (length h); xa = update (butlast h) i (last h); i \<noteq> length h; heap_invar xb \<and> \<alpha> xb = \<alpha> (update (butlast h) i (last h)) \<and> length xb = length (butlast h)\<rbrakk> \<Longrightarrow> heap_invar xb
 2. \<And>x xa. \<lbrakk>heap_invar h; valid h i; heap_invar h; valid h i; x = exch h i (length h); xa = butlast x; \<not> i \<noteq> length h\<rbrakk> \<Longrightarrow> heap_invar xa
[PROOF STEP]
apply auto []
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>heap_invar h; valid h i; heap_invar h; valid h i; x = exch h i (length h); xa = butlast x; \<not> i \<noteq> length h\<rbrakk> \<Longrightarrow> heap_invar xa
[PROOF STEP]
apply auto []
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma hm_remove_op_refine[refine]:
      "\<lbrakk> (hm,m)\<in>heapmap_rel; (hm,h)\<in>hmr_rel; heapmap_\<alpha> hm k \<noteq> None\<rbrakk> \<Longrightarrow>
        hm_remove_op k hm \<le> \<Down>hmr_rel (h.remove_op (hm_index hm k) h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(hm, m) \<in> heapmap_rel; (hm, h) \<in> hmr_rel; heapmap_\<alpha> hm k \<noteq> None\<rbrakk> \<Longrightarrow> hm_remove_op k hm \<le> \<Down> hmr_rel (h.remove_op (hm_index hm k) h)
[PROOF STEP]
unfolding hm_remove_op_def h.remove_op_def heapmap_rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(hm, m) \<in> br heapmap_\<alpha> heapmap_invar; (hm, h) \<in> hmr_rel; heapmap_\<alpha> hm k \<noteq> None\<rbrakk> \<Longrightarrow> ASSERT (heapmap_invar hm) \<bind> (\<lambda>_. ASSERT (k \<in> dom (heapmap_\<alpha> hm)) \<bind> (\<lambda>_. hm_index_op hm k \<bind> (\<lambda>i. let l = hm_length hm in hm_exch_op hm i l \<bind> (\<lambda>hm. hm_butlast_op hm \<bind> (\<lambda>hm. if i \<noteq> l then hm_repair_op hm i else RETURN hm))))) \<le> \<Down> hmr_rel (ASSERT (h.heap_invar h) \<bind> (\<lambda>_. ASSERT (h.valid h (hm_index hm k)) \<bind> (\<lambda>_. let l = length h in h.exch_op h (hm_index hm k) l \<bind> (\<lambda>h. h.butlast_op h \<bind> (\<lambda>h. if hm_index hm k \<noteq> l then h.repair_op h (hm_index hm k) else RETURN h)))))
[PROOF STEP]
(*apply (rewrite at "Let (hm_index hm k) _" Let_def)*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(hm, m) \<in> br heapmap_\<alpha> heapmap_invar; (hm, h) \<in> hmr_rel; heapmap_\<alpha> hm k \<noteq> None\<rbrakk> \<Longrightarrow> ASSERT (heapmap_invar hm) \<bind> (\<lambda>_. ASSERT (k \<in> dom (heapmap_\<alpha> hm)) \<bind> (\<lambda>_. hm_index_op hm k \<bind> (\<lambda>i. let l = hm_length hm in hm_exch_op hm i l \<bind> (\<lambda>hm. hm_butlast_op hm \<bind> (\<lambda>hm. if i \<noteq> l then hm_repair_op hm i else RETURN hm))))) \<le> \<Down> hmr_rel (ASSERT (h.heap_invar h) \<bind> (\<lambda>_. ASSERT (h.valid h (hm_index hm k)) \<bind> (\<lambda>_. let l = length h in h.exch_op h (hm_index hm k) l \<bind> (\<lambda>h. h.butlast_op h \<bind> (\<lambda>h. if hm_index hm k \<noteq> l then h.repair_op h (hm_index hm k) else RETURN h)))))
[PROOF STEP]
apply (refine_rcg index_op_inline_refine)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>(hm, m) \<in> br heapmap_\<alpha> heapmap_invar; (hm, h) \<in> hmr_rel; heapmap_\<alpha> hm k \<noteq> None; h.heap_invar h; h.valid h (hm_index hm k)\<rbrakk> \<Longrightarrow> heapmap_invar hm
 2. \<lbrakk>(hm, m) \<in> br heapmap_\<alpha> heapmap_invar; (hm, h) \<in> hmr_rel; heapmap_\<alpha> hm k \<noteq> None; h.heap_invar h; h.valid h (hm_index hm k); heapmap_invar hm\<rbrakk> \<Longrightarrow> k \<in> dom (heapmap_\<alpha> hm)
 3. \<lbrakk>(hm, m) \<in> br heapmap_\<alpha> heapmap_invar; (hm, h) \<in> hmr_rel; heapmap_\<alpha> hm k \<noteq> None; h.heap_invar h; h.valid h (hm_index hm k); heapmap_invar hm; k \<in> dom (heapmap_\<alpha> hm)\<rbrakk> \<Longrightarrow> (hm_index hm k, hm_index hm k) \<in> nat_rel
 4. \<And>hma ha hmaa haa. \<lbrakk>(hm, m) \<in> br heapmap_\<alpha> heapmap_invar; (hm, h) \<in> hmr_rel; heapmap_\<alpha> hm k \<noteq> None; h.heap_invar h; h.valid h (hm_index hm k); heapmap_invar hm; k \<in> dom (heapmap_\<alpha> hm); (hma, ha) \<in> hmr_rel; (hmaa, haa) \<in> hmr_rel\<rbrakk> \<Longrightarrow> (hm_index hm k \<noteq> hm_length hm) = (hm_index hm k \<noteq> length h)
 5. \<And>hma ha hmaa haa. \<lbrakk>(hm, m) \<in> br heapmap_\<alpha> heapmap_invar; (hm, h) \<in> hmr_rel; heapmap_\<alpha> hm k \<noteq> None; h.heap_invar h; h.valid h (hm_index hm k); heapmap_invar hm; k \<in> dom (heapmap_\<alpha> hm); (hma, ha) \<in> hmr_rel; (hmaa, haa) \<in> hmr_rel; hm_index hm k \<noteq> hm_length hm; hm_index hm k \<noteq> length h\<rbrakk> \<Longrightarrow> (hm_index hm k, hm_index hm k) \<in> nat_rel
[PROOF STEP]
unfolding hmr_rel_def
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>(hm, m) \<in> br heapmap_\<alpha> heapmap_invar; (hm, h) \<in> br hmr_\<alpha> hmr_invar; heapmap_\<alpha> hm k \<noteq> None; h.heap_invar h; h.valid h (hm_index hm k)\<rbrakk> \<Longrightarrow> heapmap_invar hm
 2. \<lbrakk>(hm, m) \<in> br heapmap_\<alpha> heapmap_invar; (hm, h) \<in> br hmr_\<alpha> hmr_invar; heapmap_\<alpha> hm k \<noteq> None; h.heap_invar h; h.valid h (hm_index hm k); heapmap_invar hm\<rbrakk> \<Longrightarrow> k \<in> dom (heapmap_\<alpha> hm)
 3. \<lbrakk>(hm, m) \<in> br heapmap_\<alpha> heapmap_invar; (hm, h) \<in> br hmr_\<alpha> hmr_invar; heapmap_\<alpha> hm k \<noteq> None; h.heap_invar h; h.valid h (hm_index hm k); heapmap_invar hm; k \<in> dom (heapmap_\<alpha> hm)\<rbrakk> \<Longrightarrow> (hm_index hm k, hm_index hm k) \<in> nat_rel
 4. \<And>hma ha hmaa haa. \<lbrakk>(hm, m) \<in> br heapmap_\<alpha> heapmap_invar; (hm, h) \<in> br hmr_\<alpha> hmr_invar; heapmap_\<alpha> hm k \<noteq> None; h.heap_invar h; h.valid h (hm_index hm k); heapmap_invar hm; k \<in> dom (heapmap_\<alpha> hm); (hma, ha) \<in> br hmr_\<alpha> hmr_invar; (hmaa, haa) \<in> br hmr_\<alpha> hmr_invar\<rbrakk> \<Longrightarrow> (hm_index hm k \<noteq> hm_length hm) = (hm_index hm k \<noteq> length h)
 5. \<And>hma ha hmaa haa. \<lbrakk>(hm, m) \<in> br heapmap_\<alpha> heapmap_invar; (hm, h) \<in> br hmr_\<alpha> hmr_invar; heapmap_\<alpha> hm k \<noteq> None; h.heap_invar h; h.valid h (hm_index hm k); heapmap_invar hm; k \<in> dom (heapmap_\<alpha> hm); (hma, ha) \<in> br hmr_\<alpha> hmr_invar; (hmaa, haa) \<in> br hmr_\<alpha> hmr_invar; hm_index hm k \<noteq> hm_length hm; hm_index hm k \<noteq> length h\<rbrakk> \<Longrightarrow> (hm_index hm k, hm_index hm k) \<in> nat_rel
[PROOF STEP]
apply (auto simp: in_br_conv)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma hm_remove_op_\<alpha>_correct:
      "hm_remove_op k hm \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = (heapmap_\<alpha> hm)(k:=None))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hm_remove_op k hm \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = (heapmap_\<alpha> hm)(k := None))
[PROOF STEP]
unfolding hm_remove_op_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ASSERT (heapmap_invar hm) \<bind> (\<lambda>_. ASSERT (k \<in> dom (heapmap_\<alpha> hm)) \<bind> (\<lambda>_. hm_index_op hm k \<bind> (\<lambda>i. let l = hm_length hm in hm_exch_op hm i l \<bind> (\<lambda>hm. hm_butlast_op hm \<bind> (\<lambda>hm. if i \<noteq> l then hm_repair_op hm i else RETURN hm))))) \<le>\<^sub>n SPEC (\<lambda>hm'. heapmap_\<alpha> hm' = (heapmap_\<alpha> hm)(k := None))
[PROOF STEP]
apply (refine_vcg
        hm_exch_op_\<alpha>_correct[THEN leof_trans]
        hm_butlast_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. \<And>x xa xb. \<lbrakk>heapmap_invar hm; k \<in> dom (heapmap_\<alpha> hm); x \<in> {hm'. hm_valid hm (hm_index hm k) \<and> hm_valid hm (hm_length hm) \<and> hm' = hm_exch hm (hm_index hm k) (hm_length hm)}; xa \<in> {hm'. heapmap_\<alpha> hm' = (heapmap_\<alpha> x)(hm_key_of x (hm_length x) := None)}; hm_index hm k \<noteq> hm_length hm; xb \<in> {hm'. heapmap_\<alpha> hm' = heapmap_\<alpha> xa}\<rbrakk> \<Longrightarrow> heapmap_\<alpha> xb = (heapmap_\<alpha> hm)(k := None)
 2. \<And>x xa. \<lbrakk>heapmap_invar hm; k \<in> dom (heapmap_\<alpha> hm); x \<in> {hm'. hm_valid hm (hm_index hm k) \<and> hm_valid hm (hm_length hm) \<and> hm' = hm_exch hm (hm_index hm k) (hm_length hm)}; xa \<in> {hm'. heapmap_\<alpha> hm' = (heapmap_\<alpha> x)(hm_key_of x (hm_length x) := None)}; \<not> hm_index hm k \<noteq> hm_length hm\<rbrakk> \<Longrightarrow> heapmap_\<alpha> xa = (heapmap_\<alpha> hm)(k := None)
[PROOF STEP]
apply (auto; fail)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>heapmap_invar hm; k \<in> dom (heapmap_\<alpha> hm); x \<in> {hm'. hm_valid hm (hm_index hm k) \<and> hm_valid hm (hm_length hm) \<and> hm' = hm_exch hm (hm_index hm k) (hm_length hm)}; xa \<in> {hm'. heapmap_\<alpha> hm' = (heapmap_\<alpha> x)(hm_key_of x (hm_length x) := None)}; \<not> hm_index hm k \<noteq> hm_length hm\<rbrakk> \<Longrightarrow> heapmap_\<alpha> xa = (heapmap_\<alpha> hm)(k := None)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b y. \<lbrakk>heapmap_invar hm; hm_valid hm (hm_length hm); heapmap_\<alpha> (a, b) = (heapmap_\<alpha> hm)(hm_key_of hm (hm_length hm) := None); hm_index hm k = hm_length hm; heapmap_\<alpha> hm k = Some y\<rbrakk> \<Longrightarrow> (heapmap_\<alpha> hm)(hm_key_of hm (hm_length hm) := None) = (heapmap_\<alpha> hm)(k := None)
[PROOF STEP]
apply (rewrite at "hm_index _ k = hm_length _" in asm eq_commute)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b y. \<lbrakk>heapmap_invar hm; hm_valid hm (hm_length hm); heapmap_\<alpha> (a, b) = (heapmap_\<alpha> hm)(hm_key_of hm (hm_length hm) := None); hm_length hm = hm_index hm k; heapmap_\<alpha> hm k = Some y\<rbrakk> \<Longrightarrow> (heapmap_\<alpha> hm)(hm_key_of hm (hm_length hm) := None) = (heapmap_\<alpha> hm)(k := None)
[PROOF STEP]
apply (auto; fail)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma hm_remove_op_aref:
      "(hm_remove_op,mop_map_delete_ex) \<in> Id \<rightarrow> heapmap_rel \<rightarrow> \<langle>heapmap_rel\<rangle>nres_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (hm_remove_op, mop_map_delete_ex) \<in> 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. \<lbrakk>(a, a') \<in> Id; (aa, a'a) \<in> heapmap_rel\<rbrakk> \<Longrightarrow> hm_remove_op a aa \<le> \<Down> heapmap_rel (mop_map_delete_ex a' a'a)
[PROOF STEP]
unfolding mop_map_delete_ex_alt
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' aa a'a. \<lbrakk>(a, a') \<in> Id; (aa, a'a) \<in> heapmap_rel\<rbrakk> \<Longrightarrow> hm_remove_op a aa \<le> \<Down> heapmap_rel (ASSERT (pre_map_delete_ex (a', a'a)) \<bind> (\<lambda>_. RETURN (op_map_delete_ex a' a'a)))
[PROOF STEP]
apply (rule ASSERT_refine_right)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' aa a'a. \<lbrakk>(a, a') \<in> Id; (aa, a'a) \<in> heapmap_rel; pre_map_delete_ex (a', a'a)\<rbrakk> \<Longrightarrow> hm_remove_op a aa \<le> \<Down> heapmap_rel (RETURN (op_map_delete_ex a' a'a))
[PROOF STEP]
apply (frule heapmap_hmr_relI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' aa a'a. \<lbrakk>(a, a') \<in> Id; (aa, a'a) \<in> heapmap_rel; pre_map_delete_ex (a', a'a); (aa, hmr_\<alpha> aa) \<in> hmr_rel\<rbrakk> \<Longrightarrow> hm_remove_op a aa \<le> \<Down> heapmap_rel (RETURN (op_map_delete_ex a' a'a))
[PROOF STEP]
apply (rule heapmap_nres_relI')
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a a' aa a'a. \<lbrakk>(a, a') \<in> Id; (aa, a'a) \<in> heapmap_rel; pre_map_delete_ex (a', a'a); (aa, hmr_\<alpha> aa) \<in> hmr_rel\<rbrakk> \<Longrightarrow> hm_remove_op a aa \<le> \<Down> hmr_rel (?h'7 a a' aa a'a)
 2. \<And>a a' aa a'a. \<lbrakk>(a, a') \<in> Id; (aa, a'a) \<in> heapmap_rel; pre_map_delete_ex (a', a'a); (aa, hmr_\<alpha> aa) \<in> hmr_rel\<rbrakk> \<Longrightarrow> ?h'7 a a' aa a'a \<le> SPEC h.heap_invar
 3. \<And>a a' aa a'a. \<lbrakk>(a, a') \<in> Id; (aa, a'a) \<in> heapmap_rel; pre_map_delete_ex (a', a'a); (aa, hmr_\<alpha> aa) \<in> hmr_rel\<rbrakk> \<Longrightarrow> hm_remove_op a aa \<le>\<^sub>n SPEC (\<lambda>hm'. RETURN (heapmap_\<alpha> hm') \<le> RETURN (op_map_delete_ex a' a'a))
[PROOF STEP]
apply (rule hm_remove_op_refine; assumption?)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a a' aa a'a. \<lbrakk>(a, a') \<in> Id; (aa, a'a) \<in> heapmap_rel; pre_map_delete_ex (a', a'a); (aa, hmr_\<alpha> aa) \<in> hmr_rel\<rbrakk> \<Longrightarrow> heapmap_\<alpha> aa a \<noteq> None
 2. \<And>a a' aa a'a. \<lbrakk>(a, a') \<in> Id; (aa, a'a) \<in> heapmap_rel; pre_map_delete_ex (a', a'a); (aa, hmr_\<alpha> aa) \<in> hmr_rel\<rbrakk> \<Longrightarrow> h.remove_op (hm_index aa a) (hmr_\<alpha> aa) \<le> SPEC h.heap_invar
 3. \<And>a a' aa a'a. \<lbrakk>(a, a') \<in> Id; (aa, a'a) \<in> heapmap_rel; pre_map_delete_ex (a', a'a); (aa, hmr_\<alpha> aa) \<in> hmr_rel\<rbrakk> \<Longrightarrow> hm_remove_op a aa \<le>\<^sub>n SPEC (\<lambda>hm'. RETURN (heapmap_\<alpha> hm') \<le> RETURN (op_map_delete_ex a' a'a))
[PROOF STEP]
apply (unfold heapmap_rel_def in_br_conv; auto)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a a' aa a'a. \<lbrakk>(a, a') \<in> Id; (aa, a'a) \<in> heapmap_rel; pre_map_delete_ex (a', a'a); (aa, hmr_\<alpha> aa) \<in> hmr_rel\<rbrakk> \<Longrightarrow> h.remove_op (hm_index aa a) (hmr_\<alpha> aa) \<le> SPEC h.heap_invar
 2. \<And>a a' aa a'a. \<lbrakk>(a, a') \<in> Id; (aa, a'a) \<in> heapmap_rel; pre_map_delete_ex (a', a'a); (aa, hmr_\<alpha> aa) \<in> hmr_rel\<rbrakk> \<Longrightarrow> hm_remove_op a aa \<le>\<^sub>n SPEC (\<lambda>hm'. RETURN (heapmap_\<alpha> hm') \<le> RETURN (op_map_delete_ex a' 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' aa a'a. \<lbrakk>(a, a') \<in> Id; a'a = heapmap_\<alpha> aa \<and> heapmap_invar aa; pre_map_delete_ex (a', a'a); hmr_\<alpha> aa = hmr_\<alpha> aa \<and> hmr_invar aa\<rbrakk> \<Longrightarrow> h.remove_op (hm_index aa a) (hmr_\<alpha> aa) \<le> SPEC h.heap_invar
 2. \<And>a a' aa a'a. \<lbrakk>(a, a') \<in> Id; a'a = heapmap_\<alpha> aa \<and> heapmap_invar aa; pre_map_delete_ex (a', a'a); hmr_\<alpha> aa = hmr_\<alpha> aa \<and> hmr_invar aa\<rbrakk> \<Longrightarrow> hm_remove_op a aa \<le>\<^sub>n SPEC (\<lambda>hm'. RETURN (heapmap_\<alpha> hm') \<le> RETURN (op_map_delete_ex a' a'a))
[PROOF STEP]
apply (refine_vcg h.remove_op_invar; clarsimp; fail)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' aa a'a. \<lbrakk>(a, a') \<in> Id; a'a = heapmap_\<alpha> aa \<and> heapmap_invar aa; pre_map_delete_ex (a', a'a); hmr_\<alpha> aa = hmr_\<alpha> aa \<and> hmr_invar aa\<rbrakk> \<Longrightarrow> hm_remove_op a aa \<le>\<^sub>n SPEC (\<lambda>hm'. RETURN (heapmap_\<alpha> hm') \<le> RETURN (op_map_delete_ex a' a'a))
[PROOF STEP]
apply (refine_vcg hm_remove_op_\<alpha>_correct[THEN leof_trans]; simp; fail)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma hm_peek_min_op_aref:
      "(hm_peek_min_op, PR_CONST (mop_pm_peek_min prio)) \<in> heapmap_rel \<rightarrow> \<langle>Id\<times>\<^sub>rId\<rangle>nres_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (hm_peek_min_op, PR_CONST (mop_pm_peek_min prio)) \<in> heapmap_rel \<rightarrow> \<langle>Id \<times>\<^sub>r Id\<rangle>nres_rel
[PROOF STEP]
unfolding PR_CONST_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (hm_peek_min_op, mop_pm_peek_min prio) \<in> heapmap_rel \<rightarrow> \<langle>Id \<times>\<^sub>r Id\<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> heapmap_rel \<Longrightarrow> hm_peek_min_op a \<le> \<Down> (Id \<times>\<^sub>r Id) (mop_pm_peek_min prio a')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a a'. (a, a') \<in> heapmap_rel \<Longrightarrow> hm_peek_min_op a \<le> \<Down> (Id \<times>\<^sub>r Id) (mop_pm_peek_min prio a')
[PROOF STEP]
fix hm and m :: "'k \<rightharpoonup> 'v"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a a'. (a, a') \<in> heapmap_rel \<Longrightarrow> hm_peek_min_op a \<le> \<Down> (Id \<times>\<^sub>r Id) (mop_pm_peek_min prio a')
[PROOF STEP]
assume A: "(hm,m)\<in>heapmap_rel"
[PROOF STATE]
proof (state)
this:
(hm, m) \<in> heapmap_rel

goal (1 subgoal):
 1. \<And>a a'. (a, a') \<in> heapmap_rel \<Longrightarrow> hm_peek_min_op a \<le> \<Down> (Id \<times>\<^sub>r Id) (mop_pm_peek_min prio a')
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
(hm, m) \<in> heapmap_rel
[PROOF STEP]
have [simp]: "h.heap_invar (hmr_\<alpha> hm)" "hmr_invar hm" "m=heapmap_\<alpha> hm"
[PROOF STATE]
proof (prove)
using this:
(hm, m) \<in> heapmap_rel

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

goal (1 subgoal):
 1. h.heap_invar (hmr_\<alpha> hm) &&& hmr_invar hm &&& m = heapmap_\<alpha> hm
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
h.heap_invar (hmr_\<alpha> hm)
hmr_invar hm
m = heapmap_\<alpha> hm

goal (1 subgoal):
 1. \<And>a a'. (a, a') \<in> heapmap_rel \<Longrightarrow> hm_peek_min_op a \<le> \<Down> (Id \<times>\<^sub>r Id) (mop_pm_peek_min prio a')
[PROOF STEP]
have "hm_peek_min_op hm \<le> \<Down> (kvi_rel hm 1) (h.peek_min_op (hmr_\<alpha> hm))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hm_peek_min_op hm \<le> \<Down> (kvi_rel hm 1) (h.peek_min_op (hmr_\<alpha> hm))
[PROOF STEP]
unfolding hm_peek_min_op_def  h.peek_min_op_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hm_kv_of_op hm 1 \<le> \<Down> (kvi_rel hm 1) (ASSERT (h.heap_invar (hmr_\<alpha> hm)) \<bind> (\<lambda>_. ASSERT (h.valid (hmr_\<alpha> hm) 1) \<bind> (\<lambda>_. h.val_of_op (hmr_\<alpha> hm) 1)))
[PROOF STEP]
apply (refine_rcg hm_kv_op_refine)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h.heap_invar (hmr_\<alpha> hm); h.valid (hmr_\<alpha> hm) 1\<rbrakk> \<Longrightarrow> (hm, hmr_\<alpha> hm) \<in> hmr_rel
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
(hm, m) \<in> heapmap_rel

goal (1 subgoal):
 1. \<lbrakk>h.heap_invar (hmr_\<alpha> hm); h.valid (hmr_\<alpha> hm) 1\<rbrakk> \<Longrightarrow> (hm, hmr_\<alpha> hm) \<in> hmr_rel
[PROOF STEP]
apply (simp add: heapmap_hmr_relI)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
hm_peek_min_op hm \<le> \<Down> (kvi_rel hm 1) (h.peek_min_op (hmr_\<alpha> hm))

goal (1 subgoal):
 1. \<And>a a'. (a, a') \<in> heapmap_rel \<Longrightarrow> hm_peek_min_op a \<le> \<Down> (Id \<times>\<^sub>r Id) (mop_pm_peek_min prio a')
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
hm_peek_min_op hm \<le> \<Down> (kvi_rel hm 1) (h.peek_min_op (hmr_\<alpha> hm))

goal (1 subgoal):
 1. \<And>a a'. (a, a') \<in> heapmap_rel \<Longrightarrow> hm_peek_min_op a \<le> \<Down> (Id \<times>\<^sub>r Id) (mop_pm_peek_min prio a')
[PROOF STEP]
have "\<lbrakk>hmr_\<alpha> hm \<noteq> []\<rbrakk> \<Longrightarrow> (h.peek_min_op (hmr_\<alpha> hm))
        \<le> SPEC (\<lambda>v. v\<in>ran (heapmap_\<alpha> hm) \<and> (\<forall>v'\<in>ran (heapmap_\<alpha> hm). prio v \<le> prio v'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hmr_\<alpha> hm \<noteq> [] \<Longrightarrow> h.peek_min_op (hmr_\<alpha> hm) \<le> SPEC (\<lambda>v. v \<in> ran (heapmap_\<alpha> hm) \<and> (\<forall>v'\<in>ran (heapmap_\<alpha> hm). prio v \<le> prio v'))
[PROOF STEP]
apply refine_vcg
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. hmr_\<alpha> hm \<noteq> [] \<Longrightarrow> h.heap_invar (hmr_\<alpha> hm)
 2. hmr_\<alpha> hm \<noteq> [] \<Longrightarrow> h.\<alpha> (hmr_\<alpha> hm) \<noteq> {#}
 3. \<And>x. \<lbrakk>hmr_\<alpha> hm \<noteq> []; x \<in># h.\<alpha> (hmr_\<alpha> hm) \<and> (\<forall>v'\<in>#h.\<alpha> (hmr_\<alpha> hm). prio x \<le> prio v')\<rbrakk> \<Longrightarrow> x \<in> ran (heapmap_\<alpha> hm)
 4. \<And>x. \<lbrakk>hmr_\<alpha> hm \<noteq> []; x \<in># h.\<alpha> (hmr_\<alpha> hm) \<and> (\<forall>v'\<in>#h.\<alpha> (hmr_\<alpha> hm). prio x \<le> prio v')\<rbrakk> \<Longrightarrow> \<forall>v'\<in>ran (heapmap_\<alpha> hm). prio x \<le> prio v'
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
hmr_\<alpha> hm \<noteq> [] \<Longrightarrow> h.peek_min_op (hmr_\<alpha> hm) \<le> SPEC (\<lambda>v. v \<in> ran (heapmap_\<alpha> hm) \<and> (\<forall>v'\<in>ran (heapmap_\<alpha> hm). prio v \<le> prio v'))

goal (1 subgoal):
 1. \<And>a a'. (a, a') \<in> heapmap_rel \<Longrightarrow> hm_peek_min_op a \<le> \<Down> (Id \<times>\<^sub>r Id) (mop_pm_peek_min prio a')
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
hmr_\<alpha> hm \<noteq> [] \<Longrightarrow> hm_peek_min_op hm \<le> \<Down> (kvi_rel hm 1) (SPEC (\<lambda>v. v \<in> ran (heapmap_\<alpha> hm) \<and> (\<forall>v'\<in>ran (heapmap_\<alpha> hm). prio v \<le> prio v')))
[PROOF STEP]
show "hm_peek_min_op hm \<le> \<Down> (Id \<times>\<^sub>r Id) (mop_pm_peek_min prio m)"
[PROOF STATE]
proof (prove)
using this:
hmr_\<alpha> hm \<noteq> [] \<Longrightarrow> hm_peek_min_op hm \<le> \<Down> (kvi_rel hm 1) (SPEC (\<lambda>v. v \<in> ran (heapmap_\<alpha> hm) \<and> (\<forall>v'\<in>ran (heapmap_\<alpha> hm). prio v \<le> prio v')))

goal (1 subgoal):
 1. hm_peek_min_op hm \<le> \<Down> (Id \<times>\<^sub>r Id) (mop_pm_peek_min prio m)
[PROOF STEP]
unfolding mop_pm_peek_min_alt
[PROOF STATE]
proof (prove)
using this:
hmr_\<alpha> hm \<noteq> [] \<Longrightarrow> hm_peek_min_op hm \<le> \<Down> (kvi_rel hm 1) (SPEC (\<lambda>v. v \<in> ran (heapmap_\<alpha> hm) \<and> (\<forall>v'\<in>ran (heapmap_\<alpha> hm). prio v \<le> prio v')))

goal (1 subgoal):
 1. hm_peek_min_op hm \<le> \<Down> (Id \<times>\<^sub>r Id) (ASSERT (pre_pm_peek_min m) \<bind> (\<lambda>_. PR_CONST (op_pm_peek_min prio) m))
[PROOF STEP]
apply (simp add: pw_le_iff refine_pw_simps hm_peek_min_op_def hm_kv_of_op_def
            hm_key_of_op_unfold hm_the_lookup_op_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (heapmap_\<alpha> hm \<noteq> Map.empty \<Longrightarrow> hm_valid hm (Suc 0) \<and> (\<exists>y. heapmap_\<alpha> hm (hm_key_of hm (Suc 0)) = Some y) \<and> (\<forall>a b. (hm_valid hm (Suc 0) \<longrightarrow> (\<exists>y. heapmap_\<alpha> hm (hm_key_of hm (Suc 0)) = Some y) \<longrightarrow> hm_key_of hm (Suc 0) = a \<and> the (heapmap_\<alpha> hm (hm_key_of hm (Suc 0))) = b) \<longrightarrow> (\<exists>s'. ((a, b), s') \<in> kvi_rel hm (Suc 0) \<and> s' \<in> ran (heapmap_\<alpha> hm) \<and> (\<forall>v'\<in>ran (heapmap_\<alpha> hm). prio s' \<le> prio v')))) \<Longrightarrow> Map.empty \<noteq> heapmap_\<alpha> hm \<longrightarrow> (\<forall>k' v'. heapmap_\<alpha> hm k' = Some v' \<longrightarrow> prio (the (heapmap_\<alpha> hm (hm_key_of hm (Suc 0)))) \<le> prio v')
[PROOF STEP]
apply (fastforce simp: kvi_rel_def ran_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
hm_peek_min_op hm \<le> \<Down> (Id \<times>\<^sub>r Id) (mop_pm_peek_min prio m)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rtrancl_mono_proof[mono]:
   "(\<And>a b. x a b \<longrightarrow> y a b) \<Longrightarrow> rtranclp x a b \<longrightarrow> rtranclp y a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a b. x a b \<longrightarrow> y a b) \<Longrightarrow> x\<^sup>*\<^sup>* a b \<longrightarrow> y\<^sup>*\<^sup>* a b
[PROOF STEP]
apply (rule impI, rotate_tac, induct rule: rtranclp.induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. (\<And>a b. x a b \<longrightarrow> y a b) \<Longrightarrow> y\<^sup>*\<^sup>* a a
 2. \<And>a b c. \<lbrakk>x\<^sup>*\<^sup>* a b; (\<And>a b. x a b \<longrightarrow> y a b) \<Longrightarrow> y\<^sup>*\<^sup>* a b; x b c; \<And>a b. x a b \<longrightarrow> y a b\<rbrakk> \<Longrightarrow> y\<^sup>*\<^sup>* a c
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>x\<^sup>*\<^sup>* a b; y\<^sup>*\<^sup>* a b; x b c; \<And>a b. x a b \<longrightarrow> y a b\<rbrakk> \<Longrightarrow> y\<^sup>*\<^sup>* a c
[PROOF STEP]
apply (metis rtranclp.intros)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma no_step_final:
  assumes step: "\<Gamma> \<turnstile>(c,s) \<rightarrow> (c',s')"
  shows "final (c,s) \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. final (c, s) \<Longrightarrow> P
[PROOF STEP]
using step
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> (c, s) \<rightarrow> (c', s')

goal (1 subgoal):
 1. final (c, s) \<Longrightarrow> P
[PROOF STEP]
by induct (auto simp add: final_def)


[STATEMENT]
lemma no_step_final':
  assumes step: "\<Gamma> \<turnstile>cfg \<rightarrow> cfg'"
  shows "final cfg \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. final cfg \<Longrightarrow> P
[PROOF STEP]
using step
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> cfg \<rightarrow> cfg'

goal (1 subgoal):
 1. final cfg \<Longrightarrow> P
[PROOF STEP]
by (cases cfg, cases cfg') (auto intro: no_step_final)


[STATEMENT]
lemma no_steps_final:
"\<Gamma> \<turnstile> v \<rightarrow>\<^sup>* w \<Longrightarrow> final v \<Longrightarrow> w = v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma> \<turnstile> v \<rightarrow>\<^sup>* w; final v\<rbrakk> \<Longrightarrow> w = v
[PROOF STEP]
apply (cases v)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<Gamma> \<turnstile> v \<rightarrow>\<^sup>* w; final v; v = (a, b)\<rbrakk> \<Longrightarrow> w = v
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<Gamma> \<turnstile> (a, b) \<rightarrow>\<^sup>* w; final (a, b); v = (a, b)\<rbrakk> \<Longrightarrow> w = (a, b)
[PROOF STEP]
apply  (erule converse_rtranclpE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>final (a, b); v = (a, b); (a, b) = w\<rbrakk> \<Longrightarrow> w = (a, b)
 2. \<And>a b y. \<lbrakk>final (a, b); v = (a, b); \<Gamma>\<turnstile> (a, b) \<rightarrow> y; \<Gamma> \<turnstile> y \<rightarrow>\<^sup>* w\<rbrakk> \<Longrightarrow> w = (a, b)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b y. \<lbrakk>final (a, b); v = (a, b); \<Gamma>\<turnstile> (a, b) \<rightarrow> y; \<Gamma> \<turnstile> y \<rightarrow>\<^sup>* w\<rbrakk> \<Longrightarrow> w = (a, b)
[PROOF STEP]
apply (erule (1) no_step_final')
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma step_Fault:
  assumes step: "\<Gamma> \<turnstile> (c, s) \<rightarrow> (c', s')"
  shows "\<And>f. s=Fault f \<Longrightarrow> s'=Fault f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f. s = Fault f \<Longrightarrow> s' = Fault f
[PROOF STEP]
using step
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> (c, s) \<rightarrow> (c', s')

goal (1 subgoal):
 1. \<And>f. s = Fault f \<Longrightarrow> s' = Fault f
[PROOF STEP]
by (induct) auto


[STATEMENT]
lemma step_Stuck:
  assumes step: "\<Gamma> \<turnstile> (c, s) \<rightarrow> (c', s')"
  shows "\<And>f. s=Stuck \<Longrightarrow> s'=Stuck"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f. s = Stuck \<Longrightarrow> s' = Stuck
[PROOF STEP]
using step
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> (c, s) \<rightarrow> (c', s')

goal (1 subgoal):
 1. \<And>f. s = Stuck \<Longrightarrow> s' = Stuck
[PROOF STEP]
by (induct) auto


[STATEMENT]
lemma SeqSteps:
  assumes steps: "\<Gamma> \<turnstile>cfg\<^sub>1\<rightarrow>\<^sup>* cfg\<^sub>2"
  shows "\<And> c\<^sub>1 s c\<^sub>1' s'. \<lbrakk>cfg\<^sub>1 = (c\<^sub>1,s);cfg\<^sub>2=(c\<^sub>1',s')\<rbrakk>
          \<Longrightarrow> \<Gamma> \<turnstile>(Seq c\<^sub>1 c\<^sub>2,s) \<rightarrow>\<^sup>* (Seq c\<^sub>1' c\<^sub>2, s')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c\<^sub>1 s c\<^sub>1' s'. \<lbrakk>cfg\<^sub>1 = (c\<^sub>1, s); cfg\<^sub>2 = (c\<^sub>1', s')\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Seq c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Seq c\<^sub>1' c\<^sub>2, s')
[PROOF STEP]
using steps
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<turnstile> cfg\<^sub>1 \<rightarrow>\<^sup>* cfg\<^sub>2

goal (1 subgoal):
 1. \<And>c\<^sub>1 s c\<^sub>1' s'. \<lbrakk>cfg\<^sub>1 = (c\<^sub>1, s); cfg\<^sub>2 = (c\<^sub>1', s')\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Seq c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Seq c\<^sub>1' c\<^sub>2, s')
[PROOF STEP]
proof (induct rule: converse_rtranclp_induct [case_names Refl Trans])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>c\<^sub>1 s c\<^sub>1' s'. \<lbrakk>cfg\<^sub>2 = (c\<^sub>1, s); cfg\<^sub>2 = (c\<^sub>1', s')\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Seq c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Seq c\<^sub>1' c\<^sub>2, s')
 2. \<And>y z c\<^sub>1 s c\<^sub>1' s'. \<lbrakk>\<Gamma>\<turnstile> y \<rightarrow> z; \<Gamma> \<turnstile> z \<rightarrow>\<^sup>* cfg\<^sub>2; \<And>c\<^sub>1 s c\<^sub>1' s'. \<lbrakk>z = (c\<^sub>1, s); cfg\<^sub>2 = (c\<^sub>1', s')\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Seq c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Seq c\<^sub>1' c\<^sub>2, s'); y = (c\<^sub>1, s); cfg\<^sub>2 = (c\<^sub>1', s')\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Seq c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Seq c\<^sub>1' c\<^sub>2, s')
[PROOF STEP]
case Refl
[PROOF STATE]
proof (state)
this:
cfg\<^sub>2 = (c\<^sub>1, s)
cfg\<^sub>2 = (c\<^sub>1', s')

goal (2 subgoals):
 1. \<And>c\<^sub>1 s c\<^sub>1' s'. \<lbrakk>cfg\<^sub>2 = (c\<^sub>1, s); cfg\<^sub>2 = (c\<^sub>1', s')\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Seq c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Seq c\<^sub>1' c\<^sub>2, s')
 2. \<And>y z c\<^sub>1 s c\<^sub>1' s'. \<lbrakk>\<Gamma>\<turnstile> y \<rightarrow> z; \<Gamma> \<turnstile> z \<rightarrow>\<^sup>* cfg\<^sub>2; \<And>c\<^sub>1 s c\<^sub>1' s'. \<lbrakk>z = (c\<^sub>1, s); cfg\<^sub>2 = (c\<^sub>1', s')\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Seq c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Seq c\<^sub>1' c\<^sub>2, s'); y = (c\<^sub>1, s); cfg\<^sub>2 = (c\<^sub>1', s')\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Seq c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Seq c\<^sub>1' c\<^sub>2, s')
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
cfg\<^sub>2 = (c\<^sub>1, s)
cfg\<^sub>2 = (c\<^sub>1', s')

goal (1 subgoal):
 1. \<Gamma> \<turnstile> (Seq c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Seq c\<^sub>1' c\<^sub>2, s')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Gamma> \<turnstile> (Seq c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Seq c\<^sub>1' c\<^sub>2, s')

goal (1 subgoal):
 1. \<And>y z c\<^sub>1 s c\<^sub>1' s'. \<lbrakk>\<Gamma>\<turnstile> y \<rightarrow> z; \<Gamma> \<turnstile> z \<rightarrow>\<^sup>* cfg\<^sub>2; \<And>c\<^sub>1 s c\<^sub>1' s'. \<lbrakk>z = (c\<^sub>1, s); cfg\<^sub>2 = (c\<^sub>1', s')\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Seq c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Seq c\<^sub>1' c\<^sub>2, s'); y = (c\<^sub>1, s); cfg\<^sub>2 = (c\<^sub>1', s')\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Seq c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Seq c\<^sub>1' c\<^sub>2, s')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y z c\<^sub>1 s c\<^sub>1' s'. \<lbrakk>\<Gamma>\<turnstile> y \<rightarrow> z; \<Gamma> \<turnstile> z \<rightarrow>\<^sup>* cfg\<^sub>2; \<And>c\<^sub>1 s c\<^sub>1' s'. \<lbrakk>z = (c\<^sub>1, s); cfg\<^sub>2 = (c\<^sub>1', s')\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Seq c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Seq c\<^sub>1' c\<^sub>2, s'); y = (c\<^sub>1, s); cfg\<^sub>2 = (c\<^sub>1', s')\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Seq c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Seq c\<^sub>1' c\<^sub>2, s')
[PROOF STEP]
case (Trans cfg\<^sub>1 cfg'')
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> cfg\<^sub>1 \<rightarrow> cfg''
\<Gamma> \<turnstile> cfg'' \<rightarrow>\<^sup>* cfg\<^sub>2
\<lbrakk>cfg'' = (?c\<^sub>1, ?s); cfg\<^sub>2 = (?c\<^sub>1', ?s')\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Seq ?c\<^sub>1 c\<^sub>2, ?s) \<rightarrow>\<^sup>* (Seq ?c\<^sub>1' c\<^sub>2, ?s')
cfg\<^sub>1 = (c\<^sub>1, s)
cfg\<^sub>2 = (c\<^sub>1', s')

goal (1 subgoal):
 1. \<And>y z c\<^sub>1 s c\<^sub>1' s'. \<lbrakk>\<Gamma>\<turnstile> y \<rightarrow> z; \<Gamma> \<turnstile> z \<rightarrow>\<^sup>* cfg\<^sub>2; \<And>c\<^sub>1 s c\<^sub>1' s'. \<lbrakk>z = (c\<^sub>1, s); cfg\<^sub>2 = (c\<^sub>1', s')\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Seq c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Seq c\<^sub>1' c\<^sub>2, s'); y = (c\<^sub>1, s); cfg\<^sub>2 = (c\<^sub>1', s')\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Seq c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Seq c\<^sub>1' c\<^sub>2, s')
[PROOF STEP]
have step: "\<Gamma> \<turnstile> cfg\<^sub>1 \<rightarrow> cfg''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> cfg\<^sub>1 \<rightarrow> cfg''
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> cfg\<^sub>1 \<rightarrow> cfg''

goal (1 subgoal):
 1. \<And>y z c\<^sub>1 s c\<^sub>1' s'. \<lbrakk>\<Gamma>\<turnstile> y \<rightarrow> z; \<Gamma> \<turnstile> z \<rightarrow>\<^sup>* cfg\<^sub>2; \<And>c\<^sub>1 s c\<^sub>1' s'. \<lbrakk>z = (c\<^sub>1, s); cfg\<^sub>2 = (c\<^sub>1', s')\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Seq c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Seq c\<^sub>1' c\<^sub>2, s'); y = (c\<^sub>1, s); cfg\<^sub>2 = (c\<^sub>1', s')\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Seq c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Seq c\<^sub>1' c\<^sub>2, s')
[PROOF STEP]
have steps: "\<Gamma> \<turnstile> cfg'' \<rightarrow>\<^sup>* cfg\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma> \<turnstile> cfg'' \<rightarrow>\<^sup>* cfg\<^sub>2
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
\<Gamma> \<turnstile> cfg'' \<rightarrow>\<^sup>* cfg\<^sub>2

goal (1 subgoal):
 1. \<And>y z c\<^sub>1 s c\<^sub>1' s'. \<lbrakk>\<Gamma>\<turnstile> y \<rightarrow> z; \<Gamma> \<turnstile> z \<rightarrow>\<^sup>* cfg\<^sub>2; \<And>c\<^sub>1 s c\<^sub>1' s'. \<lbrakk>z = (c\<^sub>1, s); cfg\<^sub>2 = (c\<^sub>1', s')\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Seq c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Seq c\<^sub>1' c\<^sub>2, s'); y = (c\<^sub>1, s); cfg\<^sub>2 = (c\<^sub>1', s')\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Seq c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Seq c\<^sub>1' c\<^sub>2, s')
[PROOF STEP]
have cfg\<^sub>1: "cfg\<^sub>1 = (c\<^sub>1, s)" and cfg\<^sub>2: "cfg\<^sub>2 = (c\<^sub>1', s')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cfg\<^sub>1 = (c\<^sub>1, s) &&& cfg\<^sub>2 = (c\<^sub>1', s')
[PROOF STEP]
by fact+
[PROOF STATE]
proof (state)
this:
cfg\<^sub>1 = (c\<^sub>1, s)
cfg\<^sub>2 = (c\<^sub>1', s')

goal (1 subgoal):
 1. \<And>y z c\<^sub>1 s c\<^sub>1' s'. \<lbrakk>\<Gamma>\<turnstile> y \<rightarrow> z; \<Gamma> \<turnstile> z \<rightarrow>\<^sup>* cfg\<^sub>2; \<And>c\<^sub>1 s c\<^sub>1' s'. \<lbrakk>z = (c\<^sub>1, s); cfg\<^sub>2 = (c\<^sub>1', s')\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Seq c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Seq c\<^sub>1' c\<^sub>2, s'); y = (c\<^sub>1, s); cfg\<^sub>2 = (c\<^sub>1', s')\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Seq c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Seq c\<^sub>1' c\<^sub>2, s')
[PROOF STEP]
obtain c\<^sub>1'' s'' where cfg'': "cfg''=(c\<^sub>1'',s'')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>c\<^sub>1'' s''. cfg'' = (c\<^sub>1'', s'') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases cfg'') auto
[PROOF STATE]
proof (state)
this:
cfg'' = (c\<^sub>1'', s'')

goal (1 subgoal):
 1. \<And>y z c\<^sub>1 s c\<^sub>1' s'. \<lbrakk>\<Gamma>\<turnstile> y \<rightarrow> z; \<Gamma> \<turnstile> z \<rightarrow>\<^sup>* cfg\<^sub>2; \<And>c\<^sub>1 s c\<^sub>1' s'. \<lbrakk>z = (c\<^sub>1, s); cfg\<^sub>2 = (c\<^sub>1', s')\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Seq c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Seq c\<^sub>1' c\<^sub>2, s'); y = (c\<^sub>1, s); cfg\<^sub>2 = (c\<^sub>1', s')\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Seq c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Seq c\<^sub>1' c\<^sub>2, s')
[PROOF STEP]
from step cfg\<^sub>1 cfg''
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> cfg\<^sub>1 \<rightarrow> cfg''
cfg\<^sub>1 = (c\<^sub>1, s)
cfg'' = (c\<^sub>1'', s'')
[PROOF STEP]
have "\<Gamma> \<turnstile> (c\<^sub>1,s) \<rightarrow> (c\<^sub>1'',s'')"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> cfg\<^sub>1 \<rightarrow> cfg''
cfg\<^sub>1 = (c\<^sub>1, s)
cfg'' = (c\<^sub>1'', s'')

goal (1 subgoal):
 1. \<Gamma>\<turnstile> (c\<^sub>1, s) \<rightarrow> (c\<^sub>1'', s'')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (c\<^sub>1, s) \<rightarrow> (c\<^sub>1'', s'')

goal (1 subgoal):
 1. \<And>y z c\<^sub>1 s c\<^sub>1' s'. \<lbrakk>\<Gamma>\<turnstile> y \<rightarrow> z; \<Gamma> \<turnstile> z \<rightarrow>\<^sup>* cfg\<^sub>2; \<And>c\<^sub>1 s c\<^sub>1' s'. \<lbrakk>z = (c\<^sub>1, s); cfg\<^sub>2 = (c\<^sub>1', s')\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Seq c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Seq c\<^sub>1' c\<^sub>2, s'); y = (c\<^sub>1, s); cfg\<^sub>2 = (c\<^sub>1', s')\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Seq c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Seq c\<^sub>1' c\<^sub>2, s')
[PROOF STEP]
hence "\<Gamma> \<turnstile> (Seq c\<^sub>1 c\<^sub>2,s) \<rightarrow> (Seq c\<^sub>1'' c\<^sub>2,s'')"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> (c\<^sub>1, s) \<rightarrow> (c\<^sub>1'', s'')

goal (1 subgoal):
 1. \<Gamma>\<turnstile> (Seq c\<^sub>1 c\<^sub>2, s) \<rightarrow> (Seq c\<^sub>1'' c\<^sub>2, s'')
[PROOF STEP]
by (rule step.Seq)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (Seq c\<^sub>1 c\<^sub>2, s) \<rightarrow> (Seq c\<^sub>1'' c\<^sub>2, s'')

goal (1 subgoal):
 1. \<And>y z c\<^sub>1 s c\<^sub>1' s'. \<lbrakk>\<Gamma>\<turnstile> y \<rightarrow> z; \<Gamma> \<turnstile> z \<rightarrow>\<^sup>* cfg\<^sub>2; \<And>c\<^sub>1 s c\<^sub>1' s'. \<lbrakk>z = (c\<^sub>1, s); cfg\<^sub>2 = (c\<^sub>1', s')\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Seq c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Seq c\<^sub>1' c\<^sub>2, s'); y = (c\<^sub>1, s); cfg\<^sub>2 = (c\<^sub>1', s')\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Seq c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Seq c\<^sub>1' c\<^sub>2, s')
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (Seq c\<^sub>1 c\<^sub>2, s) \<rightarrow> (Seq c\<^sub>1'' c\<^sub>2, s'')

goal (1 subgoal):
 1. \<And>y z c\<^sub>1 s c\<^sub>1' s'. \<lbrakk>\<Gamma>\<turnstile> y \<rightarrow> z; \<Gamma> \<turnstile> z \<rightarrow>\<^sup>* cfg\<^sub>2; \<And>c\<^sub>1 s c\<^sub>1' s'. \<lbrakk>z = (c\<^sub>1, s); cfg\<^sub>2 = (c\<^sub>1', s')\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Seq c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Seq c\<^sub>1' c\<^sub>2, s'); y = (c\<^sub>1, s); cfg\<^sub>2 = (c\<^sub>1', s')\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Seq c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Seq c\<^sub>1' c\<^sub>2, s')
[PROOF STEP]
from Trans.hyps (3) [OF cfg'' cfg\<^sub>2]
[PROOF STATE]
proof (chain)
picking this:
\<Gamma> \<turnstile> (Seq c\<^sub>1'' c\<^sub>2, s'') \<rightarrow>\<^sup>* (Seq c\<^sub>1' c\<^sub>2, s')
[PROOF STEP]
have "\<Gamma> \<turnstile> (Seq c\<^sub>1'' c\<^sub>2, s'') \<rightarrow>\<^sup>* (Seq c\<^sub>1' c\<^sub>2, s')"
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<turnstile> (Seq c\<^sub>1'' c\<^sub>2, s'') \<rightarrow>\<^sup>* (Seq c\<^sub>1' c\<^sub>2, s')

goal (1 subgoal):
 1. \<Gamma> \<turnstile> (Seq c\<^sub>1'' c\<^sub>2, s'') \<rightarrow>\<^sup>* (Seq c\<^sub>1' c\<^sub>2, s')
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<Gamma> \<turnstile> (Seq c\<^sub>1'' c\<^sub>2, s'') \<rightarrow>\<^sup>* (Seq c\<^sub>1' c\<^sub>2, s')

goal (1 subgoal):
 1. \<And>y z c\<^sub>1 s c\<^sub>1' s'. \<lbrakk>\<Gamma>\<turnstile> y \<rightarrow> z; \<Gamma> \<turnstile> z \<rightarrow>\<^sup>* cfg\<^sub>2; \<And>c\<^sub>1 s c\<^sub>1' s'. \<lbrakk>z = (c\<^sub>1, s); cfg\<^sub>2 = (c\<^sub>1', s')\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Seq c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Seq c\<^sub>1' c\<^sub>2, s'); y = (c\<^sub>1, s); cfg\<^sub>2 = (c\<^sub>1', s')\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Seq c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Seq c\<^sub>1' c\<^sub>2, s')
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<Gamma> \<turnstile> (Seq c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Seq c\<^sub>1' c\<^sub>2, s')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<turnstile> (Seq c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Seq c\<^sub>1' c\<^sub>2, s')

goal (1 subgoal):
 1. \<Gamma> \<turnstile> (Seq c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Seq c\<^sub>1' c\<^sub>2, s')
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<Gamma> \<turnstile> (Seq c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Seq c\<^sub>1' c\<^sub>2, s')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma CatchSteps:
  assumes steps: "\<Gamma> \<turnstile>cfg\<^sub>1\<rightarrow>\<^sup>* cfg\<^sub>2"
  shows "\<And> c\<^sub>1 s c\<^sub>1' s'. \<lbrakk>cfg\<^sub>1 = (c\<^sub>1,s); cfg\<^sub>2=(c\<^sub>1',s')\<rbrakk>
          \<Longrightarrow> \<Gamma> \<turnstile>(Catch c\<^sub>1 c\<^sub>2,s) \<rightarrow>\<^sup>* (Catch c\<^sub>1' c\<^sub>2, s')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c\<^sub>1 s c\<^sub>1' s'. \<lbrakk>cfg\<^sub>1 = (c\<^sub>1, s); cfg\<^sub>2 = (c\<^sub>1', s')\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Catch c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Catch c\<^sub>1' c\<^sub>2, s')
[PROOF STEP]
using steps
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<turnstile> cfg\<^sub>1 \<rightarrow>\<^sup>* cfg\<^sub>2

goal (1 subgoal):
 1. \<And>c\<^sub>1 s c\<^sub>1' s'. \<lbrakk>cfg\<^sub>1 = (c\<^sub>1, s); cfg\<^sub>2 = (c\<^sub>1', s')\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Catch c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Catch c\<^sub>1' c\<^sub>2, s')
[PROOF STEP]
proof (induct rule: converse_rtranclp_induct [case_names Refl Trans])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>c\<^sub>1 s c\<^sub>1' s'. \<lbrakk>cfg\<^sub>2 = (c\<^sub>1, s); cfg\<^sub>2 = (c\<^sub>1', s')\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Catch c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Catch c\<^sub>1' c\<^sub>2, s')
 2. \<And>y z c\<^sub>1 s c\<^sub>1' s'. \<lbrakk>\<Gamma>\<turnstile> y \<rightarrow> z; \<Gamma> \<turnstile> z \<rightarrow>\<^sup>* cfg\<^sub>2; \<And>c\<^sub>1 s c\<^sub>1' s'. \<lbrakk>z = (c\<^sub>1, s); cfg\<^sub>2 = (c\<^sub>1', s')\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Catch c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Catch c\<^sub>1' c\<^sub>2, s'); y = (c\<^sub>1, s); cfg\<^sub>2 = (c\<^sub>1', s')\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Catch c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Catch c\<^sub>1' c\<^sub>2, s')
[PROOF STEP]
case Refl
[PROOF STATE]
proof (state)
this:
cfg\<^sub>2 = (c\<^sub>1, s)
cfg\<^sub>2 = (c\<^sub>1', s')

goal (2 subgoals):
 1. \<And>c\<^sub>1 s c\<^sub>1' s'. \<lbrakk>cfg\<^sub>2 = (c\<^sub>1, s); cfg\<^sub>2 = (c\<^sub>1', s')\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Catch c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Catch c\<^sub>1' c\<^sub>2, s')
 2. \<And>y z c\<^sub>1 s c\<^sub>1' s'. \<lbrakk>\<Gamma>\<turnstile> y \<rightarrow> z; \<Gamma> \<turnstile> z \<rightarrow>\<^sup>* cfg\<^sub>2; \<And>c\<^sub>1 s c\<^sub>1' s'. \<lbrakk>z = (c\<^sub>1, s); cfg\<^sub>2 = (c\<^sub>1', s')\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Catch c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Catch c\<^sub>1' c\<^sub>2, s'); y = (c\<^sub>1, s); cfg\<^sub>2 = (c\<^sub>1', s')\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Catch c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Catch c\<^sub>1' c\<^sub>2, s')
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
cfg\<^sub>2 = (c\<^sub>1, s)
cfg\<^sub>2 = (c\<^sub>1', s')

goal (1 subgoal):
 1. \<Gamma> \<turnstile> (Catch c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Catch c\<^sub>1' c\<^sub>2, s')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Gamma> \<turnstile> (Catch c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Catch c\<^sub>1' c\<^sub>2, s')

goal (1 subgoal):
 1. \<And>y z c\<^sub>1 s c\<^sub>1' s'. \<lbrakk>\<Gamma>\<turnstile> y \<rightarrow> z; \<Gamma> \<turnstile> z \<rightarrow>\<^sup>* cfg\<^sub>2; \<And>c\<^sub>1 s c\<^sub>1' s'. \<lbrakk>z = (c\<^sub>1, s); cfg\<^sub>2 = (c\<^sub>1', s')\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Catch c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Catch c\<^sub>1' c\<^sub>2, s'); y = (c\<^sub>1, s); cfg\<^sub>2 = (c\<^sub>1', s')\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Catch c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Catch c\<^sub>1' c\<^sub>2, s')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y z c\<^sub>1 s c\<^sub>1' s'. \<lbrakk>\<Gamma>\<turnstile> y \<rightarrow> z; \<Gamma> \<turnstile> z \<rightarrow>\<^sup>* cfg\<^sub>2; \<And>c\<^sub>1 s c\<^sub>1' s'. \<lbrakk>z = (c\<^sub>1, s); cfg\<^sub>2 = (c\<^sub>1', s')\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Catch c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Catch c\<^sub>1' c\<^sub>2, s'); y = (c\<^sub>1, s); cfg\<^sub>2 = (c\<^sub>1', s')\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Catch c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Catch c\<^sub>1' c\<^sub>2, s')
[PROOF STEP]
case (Trans cfg\<^sub>1 cfg'')
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> cfg\<^sub>1 \<rightarrow> cfg''
\<Gamma> \<turnstile> cfg'' \<rightarrow>\<^sup>* cfg\<^sub>2
\<lbrakk>cfg'' = (?c\<^sub>1, ?s); cfg\<^sub>2 = (?c\<^sub>1', ?s')\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Catch ?c\<^sub>1 c\<^sub>2, ?s) \<rightarrow>\<^sup>* (Catch ?c\<^sub>1' c\<^sub>2, ?s')
cfg\<^sub>1 = (c\<^sub>1, s)
cfg\<^sub>2 = (c\<^sub>1', s')

goal (1 subgoal):
 1. \<And>y z c\<^sub>1 s c\<^sub>1' s'. \<lbrakk>\<Gamma>\<turnstile> y \<rightarrow> z; \<Gamma> \<turnstile> z \<rightarrow>\<^sup>* cfg\<^sub>2; \<And>c\<^sub>1 s c\<^sub>1' s'. \<lbrakk>z = (c\<^sub>1, s); cfg\<^sub>2 = (c\<^sub>1', s')\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Catch c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Catch c\<^sub>1' c\<^sub>2, s'); y = (c\<^sub>1, s); cfg\<^sub>2 = (c\<^sub>1', s')\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Catch c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Catch c\<^sub>1' c\<^sub>2, s')
[PROOF STEP]
have step: "\<Gamma> \<turnstile> cfg\<^sub>1 \<rightarrow> cfg''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> cfg\<^sub>1 \<rightarrow> cfg''
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> cfg\<^sub>1 \<rightarrow> cfg''

goal (1 subgoal):
 1. \<And>y z c\<^sub>1 s c\<^sub>1' s'. \<lbrakk>\<Gamma>\<turnstile> y \<rightarrow> z; \<Gamma> \<turnstile> z \<rightarrow>\<^sup>* cfg\<^sub>2; \<And>c\<^sub>1 s c\<^sub>1' s'. \<lbrakk>z = (c\<^sub>1, s); cfg\<^sub>2 = (c\<^sub>1', s')\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Catch c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Catch c\<^sub>1' c\<^sub>2, s'); y = (c\<^sub>1, s); cfg\<^sub>2 = (c\<^sub>1', s')\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Catch c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Catch c\<^sub>1' c\<^sub>2, s')
[PROOF STEP]
have steps: "\<Gamma> \<turnstile> cfg'' \<rightarrow>\<^sup>* cfg\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma> \<turnstile> cfg'' \<rightarrow>\<^sup>* cfg\<^sub>2
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
\<Gamma> \<turnstile> cfg'' \<rightarrow>\<^sup>* cfg\<^sub>2

goal (1 subgoal):
 1. \<And>y z c\<^sub>1 s c\<^sub>1' s'. \<lbrakk>\<Gamma>\<turnstile> y \<rightarrow> z; \<Gamma> \<turnstile> z \<rightarrow>\<^sup>* cfg\<^sub>2; \<And>c\<^sub>1 s c\<^sub>1' s'. \<lbrakk>z = (c\<^sub>1, s); cfg\<^sub>2 = (c\<^sub>1', s')\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Catch c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Catch c\<^sub>1' c\<^sub>2, s'); y = (c\<^sub>1, s); cfg\<^sub>2 = (c\<^sub>1', s')\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Catch c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Catch c\<^sub>1' c\<^sub>2, s')
[PROOF STEP]
have cfg\<^sub>1: "cfg\<^sub>1 = (c\<^sub>1, s)" and cfg\<^sub>2: "cfg\<^sub>2 = (c\<^sub>1', s')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cfg\<^sub>1 = (c\<^sub>1, s) &&& cfg\<^sub>2 = (c\<^sub>1', s')
[PROOF STEP]
by fact+
[PROOF STATE]
proof (state)
this:
cfg\<^sub>1 = (c\<^sub>1, s)
cfg\<^sub>2 = (c\<^sub>1', s')

goal (1 subgoal):
 1. \<And>y z c\<^sub>1 s c\<^sub>1' s'. \<lbrakk>\<Gamma>\<turnstile> y \<rightarrow> z; \<Gamma> \<turnstile> z \<rightarrow>\<^sup>* cfg\<^sub>2; \<And>c\<^sub>1 s c\<^sub>1' s'. \<lbrakk>z = (c\<^sub>1, s); cfg\<^sub>2 = (c\<^sub>1', s')\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Catch c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Catch c\<^sub>1' c\<^sub>2, s'); y = (c\<^sub>1, s); cfg\<^sub>2 = (c\<^sub>1', s')\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Catch c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Catch c\<^sub>1' c\<^sub>2, s')
[PROOF STEP]
obtain c\<^sub>1'' s'' where cfg'': "cfg''=(c\<^sub>1'',s'')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>c\<^sub>1'' s''. cfg'' = (c\<^sub>1'', s'') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases cfg'') auto
[PROOF STATE]
proof (state)
this:
cfg'' = (c\<^sub>1'', s'')

goal (1 subgoal):
 1. \<And>y z c\<^sub>1 s c\<^sub>1' s'. \<lbrakk>\<Gamma>\<turnstile> y \<rightarrow> z; \<Gamma> \<turnstile> z \<rightarrow>\<^sup>* cfg\<^sub>2; \<And>c\<^sub>1 s c\<^sub>1' s'. \<lbrakk>z = (c\<^sub>1, s); cfg\<^sub>2 = (c\<^sub>1', s')\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Catch c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Catch c\<^sub>1' c\<^sub>2, s'); y = (c\<^sub>1, s); cfg\<^sub>2 = (c\<^sub>1', s')\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Catch c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Catch c\<^sub>1' c\<^sub>2, s')
[PROOF STEP]
from step cfg\<^sub>1 cfg''
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> cfg\<^sub>1 \<rightarrow> cfg''
cfg\<^sub>1 = (c\<^sub>1, s)
cfg'' = (c\<^sub>1'', s'')
[PROOF STEP]
have s: "\<Gamma> \<turnstile> (c\<^sub>1,s) \<rightarrow> (c\<^sub>1'',s'')"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> cfg\<^sub>1 \<rightarrow> cfg''
cfg\<^sub>1 = (c\<^sub>1, s)
cfg'' = (c\<^sub>1'', s'')

goal (1 subgoal):
 1. \<Gamma>\<turnstile> (c\<^sub>1, s) \<rightarrow> (c\<^sub>1'', s'')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (c\<^sub>1, s) \<rightarrow> (c\<^sub>1'', s'')

goal (1 subgoal):
 1. \<And>y z c\<^sub>1 s c\<^sub>1' s'. \<lbrakk>\<Gamma>\<turnstile> y \<rightarrow> z; \<Gamma> \<turnstile> z \<rightarrow>\<^sup>* cfg\<^sub>2; \<And>c\<^sub>1 s c\<^sub>1' s'. \<lbrakk>z = (c\<^sub>1, s); cfg\<^sub>2 = (c\<^sub>1', s')\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Catch c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Catch c\<^sub>1' c\<^sub>2, s'); y = (c\<^sub>1, s); cfg\<^sub>2 = (c\<^sub>1', s')\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Catch c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Catch c\<^sub>1' c\<^sub>2, s')
[PROOF STEP]
hence "\<Gamma> \<turnstile> (Catch c\<^sub>1 c\<^sub>2,s) \<rightarrow> (Catch c\<^sub>1'' c\<^sub>2,s'')"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> (c\<^sub>1, s) \<rightarrow> (c\<^sub>1'', s'')

goal (1 subgoal):
 1. \<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2, s) \<rightarrow> (Catch c\<^sub>1'' c\<^sub>2, s'')
[PROOF STEP]
by (rule step.Catch)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2, s) \<rightarrow> (Catch c\<^sub>1'' c\<^sub>2, s'')

goal (1 subgoal):
 1. \<And>y z c\<^sub>1 s c\<^sub>1' s'. \<lbrakk>\<Gamma>\<turnstile> y \<rightarrow> z; \<Gamma> \<turnstile> z \<rightarrow>\<^sup>* cfg\<^sub>2; \<And>c\<^sub>1 s c\<^sub>1' s'. \<lbrakk>z = (c\<^sub>1, s); cfg\<^sub>2 = (c\<^sub>1', s')\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Catch c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Catch c\<^sub>1' c\<^sub>2, s'); y = (c\<^sub>1, s); cfg\<^sub>2 = (c\<^sub>1', s')\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Catch c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Catch c\<^sub>1' c\<^sub>2, s')
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> (Catch c\<^sub>1 c\<^sub>2, s) \<rightarrow> (Catch c\<^sub>1'' c\<^sub>2, s'')

goal (1 subgoal):
 1. \<And>y z c\<^sub>1 s c\<^sub>1' s'. \<lbrakk>\<Gamma>\<turnstile> y \<rightarrow> z; \<Gamma> \<turnstile> z \<rightarrow>\<^sup>* cfg\<^sub>2; \<And>c\<^sub>1 s c\<^sub>1' s'. \<lbrakk>z = (c\<^sub>1, s); cfg\<^sub>2 = (c\<^sub>1', s')\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Catch c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Catch c\<^sub>1' c\<^sub>2, s'); y = (c\<^sub>1, s); cfg\<^sub>2 = (c\<^sub>1', s')\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Catch c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Catch c\<^sub>1' c\<^sub>2, s')
[PROOF STEP]
from Trans.hyps (3) [OF cfg'' cfg\<^sub>2]
[PROOF STATE]
proof (chain)
picking this:
\<Gamma> \<turnstile> (Catch c\<^sub>1'' c\<^sub>2, s'') \<rightarrow>\<^sup>* (Catch c\<^sub>1' c\<^sub>2, s')
[PROOF STEP]
have "\<Gamma> \<turnstile> (Catch c\<^sub>1'' c\<^sub>2, s'') \<rightarrow>\<^sup>* (Catch c\<^sub>1' c\<^sub>2, s')"
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<turnstile> (Catch c\<^sub>1'' c\<^sub>2, s'') \<rightarrow>\<^sup>* (Catch c\<^sub>1' c\<^sub>2, s')

goal (1 subgoal):
 1. \<Gamma> \<turnstile> (Catch c\<^sub>1'' c\<^sub>2, s'') \<rightarrow>\<^sup>* (Catch c\<^sub>1' c\<^sub>2, s')
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<Gamma> \<turnstile> (Catch c\<^sub>1'' c\<^sub>2, s'') \<rightarrow>\<^sup>* (Catch c\<^sub>1' c\<^sub>2, s')

goal (1 subgoal):
 1. \<And>y z c\<^sub>1 s c\<^sub>1' s'. \<lbrakk>\<Gamma>\<turnstile> y \<rightarrow> z; \<Gamma> \<turnstile> z \<rightarrow>\<^sup>* cfg\<^sub>2; \<And>c\<^sub>1 s c\<^sub>1' s'. \<lbrakk>z = (c\<^sub>1, s); cfg\<^sub>2 = (c\<^sub>1', s')\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Catch c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Catch c\<^sub>1' c\<^sub>2, s'); y = (c\<^sub>1, s); cfg\<^sub>2 = (c\<^sub>1', s')\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Catch c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Catch c\<^sub>1' c\<^sub>2, s')
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<Gamma> \<turnstile> (Catch c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Catch c\<^sub>1' c\<^sub>2, s')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<turnstile> (Catch c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Catch c\<^sub>1' c\<^sub>2, s')

goal (1 subgoal):
 1. \<Gamma> \<turnstile> (Catch c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Catch c\<^sub>1' c\<^sub>2, s')
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<Gamma> \<turnstile> (Catch c\<^sub>1 c\<^sub>2, s) \<rightarrow>\<^sup>* (Catch c\<^sub>1' c\<^sub>2, s')

goal:
No subgoals!
[PROOF STEP]
qed