theory Retype_DP

lemma create_objects_wp:
  notes set_map[simp del]
  shows
  "\<lbrace> K (obj_refs = map (\<lambda>x. {x}) (map pick obj_refs) \<and> distinct (map pick obj_refs) )
  and <(\<And>* ptr\<in>pick ` set obj_refs. ptr \<mapsto>o Untyped) \<and>* P > \<rbrace>
  create_objects obj_refs (Some obj) \<lbrace>\<lambda>r s. <(\<And>* ptr\<in>pick ` set obj_refs. ptr \<mapsto>o obj) \<and>* P > s \<rbrace>" apply (rule hoare_name_pre_state) apply (subst create_objects_mapM_x'[where ids' = "map pick obj_refs"]) apply simp apply (rule hoare_pre) apply (rule hoare_strengthen_post) apply (rule cdl.mapM_x_sep') apply (rule create_one_wp) apply (subst set_map[symmetric]) apply (subst sep_list_conj_sep_map_set_conj[symmetric]) apply (simp add:distinct_map) apply simp apply (clarsimp simp: set_map[symmetric]) apply (subst(asm) sep_list_conj_sep_map_set_conj[symmetric]) apply (simp add:distinct_map) apply (simp add:set_map) apply sep_cancel apply (erule sep_list_conj_impl[rotated]) apply (simp add:list_all2_iff) apply (clarsimp simp:zip_map1 zip_map2
    set_zip_same
    Fun.comp_def split_def) proof (induct obj_refs) case Nil show ?case using Nil.prems by simp next case Cons show ?case using Cons.prems apply clarsimp apply (erule disjE) apply (fastforce simp:sep_any_def) apply (erule(3) Cons.hyps) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (obj_refs = map (\<lambda>x. {x}) (map pick obj_refs) \<and> distinct (map pick obj_refs)) and cdl.lift ((SETSEPCONJ ptr:pick ` set obj_refs. ptr \<mapsto>o Untyped) \<and>* P)\<rbrace> create_objects obj_refs (Some obj) \<lbrace>\<lambda>r. cdl.lift ((SETSEPCONJ ptr:pick ` set obj_refs. ptr \<mapsto>o obj) \<and>* P)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (K (obj_refs = map (\<lambda>x. {x}) (map pick obj_refs) \<and> distinct (map pick obj_refs)) and cdl.lift ((SETSEPCONJ ptr:pick ` set obj_refs. ptr \<mapsto>o Untyped) \<and>* P)) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> create_objects obj_refs (Some obj) \<lbrace>\<lambda>r. cdl.lift ((SETSEPCONJ ptr:pick ` set obj_refs. ptr \<mapsto>o obj) \<and>* P)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. (K (obj_refs = map (\<lambda>x. {x}) (map pick obj_refs) \<and> distinct (map pick obj_refs)) and cdl.lift ((SETSEPCONJ ptr:pick ` set obj_refs. ptr \<mapsto>o Untyped) \<and>* P)) s \<Longrightarrow> obj_refs = map (\<lambda>x. {x}) (map pick obj_refs)
 2. \<And>s. (K (obj_refs = map (\<lambda>x. {x}) (map pick obj_refs) \<and> distinct (map pick obj_refs)) and cdl.lift ((SETSEPCONJ ptr:pick ` set obj_refs. ptr \<mapsto>o Untyped) \<and>* P)) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> mapM_x (\<lambda>id. create_objects [{id}] (Some obj)) (map pick obj_refs) \<lbrace>\<lambda>r. cdl.lift ((SETSEPCONJ ptr:pick ` set obj_refs. ptr \<mapsto>o obj) \<and>* P)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (K (obj_refs = map (\<lambda>x. {x}) (map pick obj_refs) \<and> distinct (map pick obj_refs)) and cdl.lift ((SETSEPCONJ ptr:pick ` set obj_refs. ptr \<mapsto>o Untyped) \<and>* P)) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> mapM_x (\<lambda>id. create_objects [{id}] (Some obj)) (map pick obj_refs) \<lbrace>\<lambda>r. cdl.lift ((SETSEPCONJ ptr:pick ` set obj_refs. ptr \<mapsto>o obj) \<and>* P)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. (K (obj_refs = map (\<lambda>x. {x}) (map pick obj_refs) \<and> distinct (map pick obj_refs)) and cdl.lift ((SETSEPCONJ ptr:pick ` set obj_refs. ptr \<mapsto>o Untyped) \<and>* P)) s \<Longrightarrow> \<lbrace>?Q3 s\<rbrace> mapM_x (\<lambda>id. create_objects [{id}] (Some obj)) (map pick obj_refs) \<lbrace>\<lambda>r. cdl.lift ((SETSEPCONJ ptr:pick ` set obj_refs. ptr \<mapsto>o obj) \<and>* P)\<rbrace>
 2. \<And>s sa. \<lbrakk>(K (obj_refs = map (\<lambda>x. {x}) (map pick obj_refs) \<and> distinct (map pick obj_refs)) and cdl.lift ((SETSEPCONJ ptr:pick ` set obj_refs. ptr \<mapsto>o Untyped) \<and>* P)) s; s = sa\<rbrakk> \<Longrightarrow> ?Q3 s sa proof (prove)
goal (3 subgoals):
 1. \<And>s. (K (obj_refs = map (\<lambda>x. {x}) (map pick obj_refs) \<and> distinct (map pick obj_refs)) and cdl.lift ((SETSEPCONJ ptr:pick ` set obj_refs. ptr \<mapsto>o Untyped) \<and>* P)) s \<Longrightarrow> \<lbrace>?Q3 s\<rbrace> mapM_x (\<lambda>id. create_objects [{id}] (Some obj)) (map pick obj_refs) \<lbrace>?Q6 s\<rbrace>
 2. \<And>s rv sa. \<lbrakk>(K (obj_refs = map (\<lambda>x. {x}) (map pick obj_refs) \<and> distinct (map pick obj_refs)) and cdl.lift ((SETSEPCONJ ptr:pick ` set obj_refs. ptr \<mapsto>o Untyped) \<and>* P)) s; ?Q6 s rv sa\<rbrakk> \<Longrightarrow> cdl.lift ((SETSEPCONJ ptr:pick ` set obj_refs. ptr \<mapsto>o obj) \<and>* P) sa
 3. \<And>s sa. \<lbrakk>(K (obj_refs = map (\<lambda>x. {x}) (map pick obj_refs) \<and> distinct (map pick obj_refs)) and cdl.lift ((SETSEPCONJ ptr:pick ` set obj_refs. ptr \<mapsto>o Untyped) \<and>* P)) s; s = sa\<rbrakk> \<Longrightarrow> ?Q3 s sa proof (prove)
goal (3 subgoals):
 1. \<And>s R x. \<lbrakk>(K (obj_refs = map (\<lambda>x. {x}) (map pick obj_refs) \<and> distinct (map pick obj_refs)) and cdl.lift ((SETSEPCONJ ptr:pick ` set obj_refs. ptr \<mapsto>o Untyped) \<and>* P)) s; x \<in> set (map pick obj_refs)\<rbrakk> \<Longrightarrow> \<lbrace>cdl.lift (?P9 s x \<and>* R)\<rbrace> create_objects [{x}] (Some obj) \<lbrace>\<lambda>_. cdl.lift (?Q9 s x \<and>* R)\<rbrace>
 2. \<And>s rv sa. \<lbrakk>(K (obj_refs = map (\<lambda>x. {x}) (map pick obj_refs) \<and> distinct (map pick obj_refs)) and cdl.lift ((SETSEPCONJ ptr:pick ` set obj_refs. ptr \<mapsto>o Untyped) \<and>* P)) s; cdl.lift (\<And>* map (?Q9 s) (map pick obj_refs) \<and>* ?R9 s) sa\<rbrakk> \<Longrightarrow> cdl.lift ((SETSEPCONJ ptr:pick ` set obj_refs. ptr \<mapsto>o obj) \<and>* P) sa
 3. \<And>s sa. \<lbrakk>(K (obj_refs = map (\<lambda>x. {x}) (map pick obj_refs) \<and> distinct (map pick obj_refs)) and cdl.lift ((SETSEPCONJ ptr:pick ` set obj_refs. ptr \<mapsto>o Untyped) \<and>* P)) s; s = sa\<rbrakk> \<Longrightarrow> cdl.lift (\<And>* map (?P9 s) (map pick obj_refs) \<and>* ?R9 s) sa proof (prove)
goal (2 subgoals):
 1. \<And>s rv sa. \<lbrakk>(K (obj_refs = map (\<lambda>x. {x}) (map pick obj_refs) \<and> distinct (map pick obj_refs)) and cdl.lift ((SETSEPCONJ ptr:pick ` set obj_refs. ptr \<mapsto>o Untyped) \<and>* P)) s; cdl.lift (\<And>* map (\<lambda>x. x \<mapsto>o obj) (map pick obj_refs) \<and>* ?R9 s) sa\<rbrakk> \<Longrightarrow> cdl.lift ((SETSEPCONJ ptr:pick ` set obj_refs. ptr \<mapsto>o obj) \<and>* P) sa
 2. \<And>s sa. \<lbrakk>(K (obj_refs = map (\<lambda>x. {x}) (map pick obj_refs) \<and> distinct (map pick obj_refs)) and cdl.lift ((SETSEPCONJ ptr:pick ` set obj_refs. ptr \<mapsto>o Untyped) \<and>* P)) s; s = sa\<rbrakk> \<Longrightarrow> cdl.lift (\<And>* map sep_any_map_o (map pick obj_refs) \<and>* ?R9 s) sa proof (prove)
goal (2 subgoals):
 1. \<And>s rv sa. \<lbrakk>(K (obj_refs = map (\<lambda>x. {x}) (map pick obj_refs) \<and> distinct (map pick obj_refs)) and cdl.lift ((SETSEPCONJ ptr:pick ` set obj_refs. ptr \<mapsto>o Untyped) \<and>* P)) s; cdl.lift (\<And>* map (\<lambda>x. x \<mapsto>o obj) (map pick obj_refs) \<and>* ?R9 s) sa\<rbrakk> \<Longrightarrow> cdl.lift ((SETSEPCONJ ptr:set (map pick obj_refs). ptr \<mapsto>o obj) \<and>* P) sa
 2. \<And>s sa. \<lbrakk>(K (obj_refs = map (\<lambda>x. {x}) (map pick obj_refs) \<and> distinct (map pick obj_refs)) and cdl.lift ((SETSEPCONJ ptr:pick ` set obj_refs. ptr \<mapsto>o Untyped) \<and>* P)) s; s = sa\<rbrakk> \<Longrightarrow> cdl.lift (\<And>* map sep_any_map_o (map pick obj_refs) \<and>* ?R9 s) sa proof (prove)
goal (3 subgoals):
 1. \<And>s rv sa. \<lbrakk>(K (obj_refs = map (\<lambda>x. {x}) (map pick obj_refs) \<and> distinct (map pick obj_refs)) and cdl.lift ((SETSEPCONJ ptr:pick ` set obj_refs. ptr \<mapsto>o Untyped) \<and>* P)) s; cdl.lift (\<And>* map (\<lambda>x. x \<mapsto>o obj) (map pick obj_refs) \<and>* ?R9 s) sa\<rbrakk> \<Longrightarrow> distinct (map pick obj_refs)
 2. \<And>s rv sa. \<lbrakk>(K (obj_refs = map (\<lambda>x. {x}) (map pick obj_refs) \<and> distinct (map pick obj_refs)) and cdl.lift ((SETSEPCONJ ptr:pick ` set obj_refs. ptr \<mapsto>o Untyped) \<and>* P)) s; cdl.lift (\<And>* map (\<lambda>x. x \<mapsto>o obj) (map pick obj_refs) \<and>* ?R9 s) sa\<rbrakk> \<Longrightarrow> cdl.lift (\<And>* map (\<lambda>ptr. ptr \<mapsto>o obj) (map pick obj_refs) \<and>* P) sa
 3. \<And>s sa. \<lbrakk>(K (obj_refs = map (\<lambda>x. {x}) (map pick obj_refs) \<and> distinct (map pick obj_refs)) and cdl.lift ((SETSEPCONJ ptr:pick ` set obj_refs. ptr \<mapsto>o Untyped) \<and>* P)) s; s = sa\<rbrakk> \<Longrightarrow> cdl.lift (\<And>* map sep_any_map_o (map pick obj_refs) \<and>* ?R9 s) sa proof (prove)
goal (2 subgoals):
 1. \<And>s rv sa. \<lbrakk>(K (obj_refs = map (\<lambda>x. {x}) (map pick obj_refs) \<and> distinct (map pick obj_refs)) and cdl.lift ((SETSEPCONJ ptr:pick ` set obj_refs. ptr \<mapsto>o Untyped) \<and>* P)) s; cdl.lift (\<And>* map (\<lambda>x. x \<mapsto>o obj) (map pick obj_refs) \<and>* ?R9 s) sa\<rbrakk> \<Longrightarrow> cdl.lift (\<And>* map (\<lambda>ptr. ptr \<mapsto>o obj) (map pick obj_refs) \<and>* P) sa
 2. \<And>s sa. \<lbrakk>(K (obj_refs = map (\<lambda>x. {x}) (map pick obj_refs) \<and> distinct (map pick obj_refs)) and cdl.lift ((SETSEPCONJ ptr:pick ` set obj_refs. ptr \<mapsto>o Untyped) \<and>* P)) s; s = sa\<rbrakk> \<Longrightarrow> cdl.lift (\<And>* map sep_any_map_o (map pick obj_refs) \<and>* ?R9 s) sa proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>(K (obj_refs = map (\<lambda>x. {x}) (map pick obj_refs) \<and> distinct (map pick obj_refs)) and cdl.lift ((SETSEPCONJ ptr:pick ` set obj_refs. ptr \<mapsto>o Untyped) \<and>* P)) s; s = sa\<rbrakk> \<Longrightarrow> cdl.lift (\<And>* map sep_any_map_o (map pick obj_refs) \<and>* P) sa proof (prove)
goal (1 subgoal):
 1. \<And>sa. \<lbrakk>obj_refs = map ((\<lambda>x. {x}) \<circ> pick) obj_refs; distinct (map pick obj_refs); cdl.lift ((SETSEPCONJ ptr:set (map pick obj_refs). ptr \<mapsto>o Untyped) \<and>* P) sa\<rbrakk> \<Longrightarrow> cdl.lift (\<And>* map (sep_any_map_o \<circ> pick) obj_refs \<and>* P) sa proof (prove)
goal (2 subgoals):
 1. \<And>sa. \<lbrakk>obj_refs = map ((\<lambda>x. {x}) \<circ> pick) obj_refs; distinct (map pick obj_refs)\<rbrakk> \<Longrightarrow> distinct (map pick obj_refs)
 2. \<And>sa. \<lbrakk>obj_refs = map ((\<lambda>x. {x}) \<circ> pick) obj_refs; distinct (map pick obj_refs); cdl.lift (\<And>* map (\<lambda>ptr. ptr \<mapsto>o Untyped) (map pick obj_refs) \<and>* P) sa\<rbrakk> \<Longrightarrow> cdl.lift (\<And>* map (sep_any_map_o \<circ> pick) obj_refs \<and>* P) sa proof (prove)
goal (1 subgoal):
 1. \<And>sa. \<lbrakk>obj_refs = map ((\<lambda>x. {x}) \<circ> pick) obj_refs; distinct (map pick obj_refs); cdl.lift (\<And>* map (\<lambda>ptr. ptr \<mapsto>o Untyped) (map pick obj_refs) \<and>* P) sa\<rbrakk> \<Longrightarrow> cdl.lift (\<And>* map (sep_any_map_o \<circ> pick) obj_refs \<and>* P) sa proof (prove)
goal (1 subgoal):
 1. \<And>sa. \<lbrakk>obj_refs = map ((\<lambda>x. {x}) \<circ> pick) obj_refs; distinct (map pick obj_refs); cdl.lift (\<And>* map ((\<lambda>ptr. ptr \<mapsto>o Untyped) \<circ> pick) obj_refs \<and>* P) sa\<rbrakk> \<Longrightarrow> cdl.lift (\<And>* map (sep_any_map_o \<circ> pick) obj_refs \<and>* P) sa proof (prove)
goal (1 subgoal):
 1. \<And>sa s. \<lbrakk>obj_refs = map ((\<lambda>x. {x}) \<circ> pick) obj_refs; distinct (map pick obj_refs); (\<And>* map ((\<lambda>ptr. ptr \<mapsto>o Untyped) \<circ> pick) obj_refs) s\<rbrakk> \<Longrightarrow> (\<And>* map (sep_any_map_o \<circ> pick) obj_refs) s proof (prove)
goal (1 subgoal):
 1. \<And>sa s. \<lbrakk>obj_refs = map ((\<lambda>x. {x}) \<circ> pick) obj_refs; distinct (map pick obj_refs)\<rbrakk> \<Longrightarrow> list_all2 (\<lambda>x y. \<forall>s. x s \<longrightarrow> y s) (map ((\<lambda>ptr. ptr \<mapsto>o Untyped) \<circ> pick) obj_refs) (map (sep_any_map_o \<circ> pick) obj_refs) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>obj_refs = map ((\<lambda>x. {x}) \<circ> pick) obj_refs; distinct (map pick obj_refs)\<rbrakk> \<Longrightarrow> \<forall>(x, y)\<in>set (zip (map ((\<lambda>ptr. ptr \<mapsto>o Untyped) \<circ> pick) obj_refs) (map (sep_any_map_o \<circ> pick) obj_refs)). \<forall>s. x s \<longrightarrow> y s proof (prove)
goal (1 subgoal):
 1. \<And>a b s. \<lbrakk>obj_refs = map (\<lambda>x. {pick x}) obj_refs; distinct (map pick obj_refs); (a, b) \<in> set (map (\<lambda>x. (pick (fst x) \<mapsto>o Untyped, (pick (snd x)) \<mapsto>o -)) (zip obj_refs obj_refs)); a s\<rbrakk> \<Longrightarrow> b s proof (state)
goal (2 subgoals):
 1. \<And>a b s. \<lbrakk>[] = map (\<lambda>x. {pick x}) []; distinct (map pick []); (a, b) \<in> set (map (\<lambda>x. (pick (fst x) \<mapsto>o Untyped, (pick (snd x)) \<mapsto>o -)) (zip [] [])); a s\<rbrakk> \<Longrightarrow> b s
 2. \<And>a obj_refs aa b s. \<lbrakk>\<And>a b s. \<lbrakk>obj_refs = map (\<lambda>x. {pick x}) obj_refs; distinct (map pick obj_refs); (a, b) \<in> set (map (\<lambda>x. (pick (fst x) \<mapsto>o Untyped, (pick (snd x)) \<mapsto>o -)) (zip obj_refs obj_refs)); a s\<rbrakk> \<Longrightarrow> b s; a # obj_refs = map (\<lambda>x. {pick x}) (a # obj_refs); distinct (map pick (a # obj_refs)); (aa, b) \<in> set (map (\<lambda>x. (pick (fst x) \<mapsto>o Untyped, (pick (snd x)) \<mapsto>o -)) (zip (a # obj_refs) (a # obj_refs))); aa s\<rbrakk> \<Longrightarrow> b s proof (state)
this:
[] = map (\<lambda>x. {pick x}) []
distinct (map pick [])
(a, b) \<in> set (map (\<lambda>x. (pick (fst x) \<mapsto>o Untyped, (pick (snd x)) \<mapsto>o -)) (zip [] []))
a s

goal (2 subgoals):
 1. \<And>a b s. \<lbrakk>[] = map (\<lambda>x. {pick x}) []; distinct (map pick []); (a, b) \<in> set (map (\<lambda>x. (pick (fst x) \<mapsto>o Untyped, (pick (snd x)) \<mapsto>o -)) (zip [] [])); a s\<rbrakk> \<Longrightarrow> b s
 2. \<And>a obj_refs aa b s. \<lbrakk>\<And>a b s. \<lbrakk>obj_refs = map (\<lambda>x. {pick x}) obj_refs; distinct (map pick obj_refs); (a, b) \<in> set (map (\<lambda>x. (pick (fst x) \<mapsto>o Untyped, (pick (snd x)) \<mapsto>o -)) (zip obj_refs obj_refs)); a s\<rbrakk> \<Longrightarrow> b s; a # obj_refs = map (\<lambda>x. {pick x}) (a # obj_refs); distinct (map pick (a # obj_refs)); (aa, b) \<in> set (map (\<lambda>x. (pick (fst x) \<mapsto>o Untyped, (pick (snd x)) \<mapsto>o -)) (zip (a # obj_refs) (a # obj_refs))); aa s\<rbrakk> \<Longrightarrow> b s proof (prove)
goal (1 subgoal):
 1. b s proof (prove)
using this:
[] = map (\<lambda>x. {pick x}) []
distinct (map pick [])
(a, b) \<in> set (map (\<lambda>x. (pick (fst x) \<mapsto>o Untyped, (pick (snd x)) \<mapsto>o -)) (zip [] []))
a s

goal (1 subgoal):
 1. b s proof (state)
this:
b s

goal (1 subgoal):
 1. \<And>a obj_refs aa b s. \<lbrakk>\<And>a b s. \<lbrakk>obj_refs = map (\<lambda>x. {pick x}) obj_refs; distinct (map pick obj_refs); (a, b) \<in> set (map (\<lambda>x. (pick (fst x) \<mapsto>o Untyped, (pick (snd x)) \<mapsto>o -)) (zip obj_refs obj_refs)); a s\<rbrakk> \<Longrightarrow> b s; a # obj_refs = map (\<lambda>x. {pick x}) (a # obj_refs); distinct (map pick (a # obj_refs)); (aa, b) \<in> set (map (\<lambda>x. (pick (fst x) \<mapsto>o Untyped, (pick (snd x)) \<mapsto>o -)) (zip (a # obj_refs) (a # obj_refs))); aa s\<rbrakk> \<Longrightarrow> b s proof (state)
goal (1 subgoal):
 1. \<And>a obj_refs aa b s. \<lbrakk>\<And>a b s. \<lbrakk>obj_refs = map (\<lambda>x. {pick x}) obj_refs; distinct (map pick obj_refs); (a, b) \<in> set (map (\<lambda>x. (pick (fst x) \<mapsto>o Untyped, (pick (snd x)) \<mapsto>o -)) (zip obj_refs obj_refs)); a s\<rbrakk> \<Longrightarrow> b s; a # obj_refs = map (\<lambda>x. {pick x}) (a # obj_refs); distinct (map pick (a # obj_refs)); (aa, b) \<in> set (map (\<lambda>x. (pick (fst x) \<mapsto>o Untyped, (pick (snd x)) \<mapsto>o -)) (zip (a # obj_refs) (a # obj_refs))); aa s\<rbrakk> \<Longrightarrow> b s proof (state)
this:
\<lbrakk>obj_refs_ = map (\<lambda>x. {pick x}) obj_refs_; distinct (map pick obj_refs_); (?a, ?b) \<in> set (map (\<lambda>x. (pick (fst x) \<mapsto>o Untyped, (pick (snd x)) \<mapsto>o -)) (zip obj_refs_ obj_refs_)); ?a ?s\<rbrakk> \<Longrightarrow> ?b ?s
a_ # obj_refs_ = map (\<lambda>x. {pick x}) (a_ # obj_refs_)
distinct (map pick (a_ # obj_refs_))
(a, b) \<in> set (map (\<lambda>x. (pick (fst x) \<mapsto>o Untyped, (pick (snd x)) \<mapsto>o -)) (zip (a_ # obj_refs_) (a_ # obj_refs_)))
a s

goal (1 subgoal):
 1. \<And>a obj_refs aa b s. \<lbrakk>\<And>a b s. \<lbrakk>obj_refs = map (\<lambda>x. {pick x}) obj_refs; distinct (map pick obj_refs); (a, b) \<in> set (map (\<lambda>x. (pick (fst x) \<mapsto>o Untyped, (pick (snd x)) \<mapsto>o -)) (zip obj_refs obj_refs)); a s\<rbrakk> \<Longrightarrow> b s; a # obj_refs = map (\<lambda>x. {pick x}) (a # obj_refs); distinct (map pick (a # obj_refs)); (aa, b) \<in> set (map (\<lambda>x. (pick (fst x) \<mapsto>o Untyped, (pick (snd x)) \<mapsto>o -)) (zip (a # obj_refs) (a # obj_refs))); aa s\<rbrakk> \<Longrightarrow> b s proof (prove)
goal (1 subgoal):
 1. b s proof (prove)
using this:
a_ # obj_refs_ = map (\<lambda>x. {pick x}) (a_ # obj_refs_)
distinct (map pick (a_ # obj_refs_))
(a, b) \<in> set (map (\<lambda>x. (pick (fst x) \<mapsto>o Untyped, (pick (snd x)) \<mapsto>o -)) (zip (a_ # obj_refs_) (a_ # obj_refs_)))
a s

goal (1 subgoal):
 1. b s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a = pick a_ \<mapsto>o Untyped \<and> b = (pick a_) \<mapsto>o - \<or> (a, b) \<in> set (map (\<lambda>x. (pick (fst x) \<mapsto>o Untyped, (pick (snd x)) \<mapsto>o -)) (zip obj_refs_ obj_refs_)); a s; a_ = {pick a_}; obj_refs_ = map (\<lambda>x. {pick x}) obj_refs_; pick a_ \<notin> set (map pick obj_refs_); distinct (map pick obj_refs_)\<rbrakk> \<Longrightarrow> b s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a s; a_ = {pick a_}; obj_refs_ = map (\<lambda>x. {pick x}) obj_refs_; pick a_ \<notin> set (map pick obj_refs_); distinct (map pick obj_refs_); a = pick a_ \<mapsto>o Untyped \<and> b = (pick a_) \<mapsto>o -\<rbrakk> \<Longrightarrow> b s
 2. \<lbrakk>a s; a_ = {pick a_}; obj_refs_ = map (\<lambda>x. {pick x}) obj_refs_; pick a_ \<notin> set (map pick obj_refs_); distinct (map pick obj_refs_); (a, b) \<in> set (map (\<lambda>x. (pick (fst x) \<mapsto>o Untyped, (pick (snd x)) \<mapsto>o -)) (zip obj_refs_ obj_refs_))\<rbrakk> \<Longrightarrow> b s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a s; a_ = {pick a_}; obj_refs_ = map (\<lambda>x. {pick x}) obj_refs_; pick a_ \<notin> set (map pick obj_refs_); distinct (map pick obj_refs_); (a, b) \<in> set (map (\<lambda>x. (pick (fst x) \<mapsto>o Untyped, (pick (snd x)) \<mapsto>o -)) (zip obj_refs_ obj_refs_))\<rbrakk> \<Longrightarrow> b s proof (prove)
goal:
No subgoals! proof (state)
this:
b s

goal:
No subgoals!