theory Retype_DP

lemma retype_region_wp:
  "\<lbrace> K (default_object target_type target_bits minBound = Some obj
     \<and> target_type \<noteq> UntypedType \<and> distinct (map pick obj_refs)
     \<and> obj_refs = map (\<lambda>x. {x}) (map pick obj_refs)
     \<and> set (map pick obj_refs) \<subseteq> obj_range )
     and (\<lambda>s. cdl_current_domain s = minBound)
     and <(\<And>* ptr\<in>obj_range. ptr \<mapsto>o Untyped) \<and>* P > \<rbrace>
  retype_region target_bits target_type obj_refs
  \<lbrace>\<lambda>r s. <(\<And>* ptr\<in>set (map pick obj_refs). ptr \<mapsto>o obj)
  \<and>* (\<And>* ptr\<in>obj_range - set (map pick obj_refs). ptr \<mapsto>o Untyped) \<and>* P > s\<rbrace>" apply (rule hoare_name_pre_state) apply (rule hoare_pre) apply (clarsimp simp:retype_region_def) apply wp apply (rule_tac P="current_domain = minBound" in hoare_gen_asm) apply (wp create_objects_wp | simp)+ apply (subst sep_conj_assoc[symmetric]) apply (subst sep.prod.union_disjoint [symmetric]) apply simp+ apply (simp add:Un_absorb1) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (default_object target_type target_bits minBound = Some obj \<and> target_type \<noteq> UntypedType \<and> distinct (map pick obj_refs) \<and> obj_refs = map (\<lambda>x. {x}) (map pick obj_refs) \<and> set (map pick obj_refs) \<subseteq> obj_range) and (\<lambda>s. cdl_current_domain s = minBound) and cdl.lift ((SETSEPCONJ ptr:obj_range. ptr \<mapsto>o Untyped) \<and>* P)\<rbrace> retype_region target_bits target_type obj_refs \<lbrace>\<lambda>r. cdl.lift ((SETSEPCONJ ptr:set (map pick obj_refs). ptr \<mapsto>o obj) \<and>* (SETSEPCONJ ptr:obj_range - set (map pick obj_refs). ptr \<mapsto>o Untyped) \<and>* P)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (K (default_object target_type target_bits minBound = Some obj \<and> target_type \<noteq> UntypedType \<and> distinct (map pick obj_refs) \<and> obj_refs = map (\<lambda>x. {x}) (map pick obj_refs) \<and> set (map pick obj_refs) \<subseteq> obj_range) and (\<lambda>s. cdl_current_domain s = minBound) and cdl.lift ((SETSEPCONJ ptr:obj_range. ptr \<mapsto>o Untyped) \<and>* P)) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> retype_region target_bits target_type obj_refs \<lbrace>\<lambda>r. cdl.lift ((SETSEPCONJ ptr:set (map pick obj_refs). ptr \<mapsto>o obj) \<and>* (SETSEPCONJ ptr:obj_range - set (map pick obj_refs). ptr \<mapsto>o Untyped) \<and>* P)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. (K (default_object target_type target_bits minBound = Some obj \<and> target_type \<noteq> UntypedType \<and> distinct (map pick obj_refs) \<and> obj_refs = map (\<lambda>x. {x}) (map pick obj_refs) \<and> set (map pick obj_refs) \<subseteq> obj_range) and (\<lambda>s. cdl_current_domain s = minBound) and cdl.lift ((SETSEPCONJ ptr:obj_range. ptr \<mapsto>o Untyped) \<and>* P)) s \<Longrightarrow> \<lbrace>?Q2 s\<rbrace> retype_region target_bits target_type obj_refs \<lbrace>\<lambda>r. cdl.lift ((SETSEPCONJ ptr:set (map pick obj_refs). ptr \<mapsto>o obj) \<and>* (SETSEPCONJ ptr:obj_range - set (map pick obj_refs). ptr \<mapsto>o Untyped) \<and>* P)\<rbrace>
 2. \<And>s sa. \<lbrakk>(K (default_object target_type target_bits minBound = Some obj \<and> target_type \<noteq> UntypedType \<and> distinct (map pick obj_refs) \<and> obj_refs = map (\<lambda>x. {x}) (map pick obj_refs) \<and> set (map pick obj_refs) \<subseteq> obj_range) and (\<lambda>s. cdl_current_domain s = minBound) and cdl.lift ((SETSEPCONJ ptr:obj_range. ptr \<mapsto>o Untyped) \<and>* P)) s; s = sa\<rbrakk> \<Longrightarrow> ?Q2 s sa proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>default_object target_type target_bits minBound = Some obj; target_type \<noteq> UntypedType; distinct (map pick obj_refs); obj_refs = map ((\<lambda>x. {x}) \<circ> pick) obj_refs; pick ` set obj_refs \<subseteq> obj_range; cdl_current_domain s = minBound; cdl.lift ((SETSEPCONJ ptr:obj_range. ptr \<mapsto>o Untyped) \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?Q2 s\<rbrace> do y <- do current_domain <- gets cdl_current_domain;
create_objects obj_refs (default_object target_type target_bits current_domain)
od;
return obj_refs
od \<lbrace>\<lambda>r. cdl.lift ((SETSEPCONJ ptr:pick ` set obj_refs. ptr \<mapsto>o obj) \<and>* (SETSEPCONJ ptr:obj_range - pick ` set obj_refs. ptr \<mapsto>o Untyped) \<and>* P)\<rbrace>
 2. \<And>s sa. \<lbrakk>(K (default_object target_type target_bits minBound = Some obj \<and> target_type \<noteq> UntypedType \<and> distinct (map pick obj_refs) \<and> obj_refs = map (\<lambda>x. {x}) (map pick obj_refs) \<and> set (map pick obj_refs) \<subseteq> obj_range) and (\<lambda>s. cdl_current_domain s = minBound) and cdl.lift ((SETSEPCONJ ptr:obj_range. ptr \<mapsto>o Untyped) \<and>* P)) s; s = sa\<rbrakk> \<Longrightarrow> ?Q2 s sa proof (prove)
goal (3 subgoals):
 1. \<And>s current_domain. \<lbrakk>default_object target_type target_bits minBound = Some obj; target_type \<noteq> UntypedType; distinct (map pick obj_refs); obj_refs = map ((\<lambda>x. {x}) \<circ> pick) obj_refs; pick ` set obj_refs \<subseteq> obj_range; cdl_current_domain s = minBound; cdl.lift ((SETSEPCONJ ptr:obj_range. ptr \<mapsto>o Untyped) \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?B20 s current_domain\<rbrace> create_objects obj_refs (default_object target_type target_bits current_domain) \<lbrace>\<lambda>y. cdl.lift ((SETSEPCONJ ptr:pick ` set obj_refs. ptr \<mapsto>o obj) \<and>* (SETSEPCONJ ptr:obj_range - pick ` set obj_refs. ptr \<mapsto>o Untyped) \<and>* P)\<rbrace>
 2. \<And>s. \<lbrakk>default_object target_type target_bits minBound = Some obj; target_type \<noteq> UntypedType; distinct (map pick obj_refs); obj_refs = map ((\<lambda>x. {x}) \<circ> pick) obj_refs; pick ` set obj_refs \<subseteq> obj_range; cdl_current_domain s = minBound; cdl.lift ((SETSEPCONJ ptr:obj_range. ptr \<mapsto>o Untyped) \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?Q2 s\<rbrace> gets cdl_current_domain \<lbrace>?B20 s\<rbrace>
 3. \<And>s sa. \<lbrakk>(K (default_object target_type target_bits minBound = Some obj \<and> target_type \<noteq> UntypedType \<and> distinct (map pick obj_refs) \<and> obj_refs = map (\<lambda>x. {x}) (map pick obj_refs) \<and> set (map pick obj_refs) \<subseteq> obj_range) and (\<lambda>s. cdl_current_domain s = minBound) and cdl.lift ((SETSEPCONJ ptr:obj_range. ptr \<mapsto>o Untyped) \<and>* P)) s; s = sa\<rbrakk> \<Longrightarrow> ?Q2 s sa proof (prove)
goal (3 subgoals):
 1. \<And>s current_domain. \<lbrakk>default_object target_type target_bits minBound = Some obj; target_type \<noteq> UntypedType; distinct (map pick obj_refs); obj_refs = map ((\<lambda>x. {x}) \<circ> pick) obj_refs; pick ` set obj_refs \<subseteq> obj_range; cdl_current_domain s = minBound; cdl.lift ((SETSEPCONJ ptr:obj_range. ptr \<mapsto>o Untyped) \<and>* P) s; current_domain = minBound\<rbrakk> \<Longrightarrow> \<lbrace>?P'22 s current_domain\<rbrace> create_objects obj_refs (default_object target_type target_bits current_domain) \<lbrace>\<lambda>y. cdl.lift ((SETSEPCONJ ptr:pick ` set obj_refs. ptr \<mapsto>o obj) \<and>* (SETSEPCONJ ptr:obj_range - pick ` set obj_refs. ptr \<mapsto>o Untyped) \<and>* P)\<rbrace>
 2. \<And>s. \<lbrakk>default_object target_type target_bits minBound = Some obj; target_type \<noteq> UntypedType; distinct (map pick obj_refs); obj_refs = map ((\<lambda>x. {x}) \<circ> pick) obj_refs; pick ` set obj_refs \<subseteq> obj_range; cdl_current_domain s = minBound; cdl.lift ((SETSEPCONJ ptr:obj_range. ptr \<mapsto>o Untyped) \<and>* P) s\<rbrakk> \<Longrightarrow> \<lbrace>?Q2 s\<rbrace> gets cdl_current_domain \<lbrace>\<lambda>current_domain. ?P'22 s current_domain and K (current_domain = minBound)\<rbrace>
 3. \<And>s sa. \<lbrakk>(K (default_object target_type target_bits minBound = Some obj \<and> target_type \<noteq> UntypedType \<and> distinct (map pick obj_refs) \<and> obj_refs = map (\<lambda>x. {x}) (map pick obj_refs) \<and> set (map pick obj_refs) \<subseteq> obj_range) and (\<lambda>s. cdl_current_domain s = minBound) and cdl.lift ((SETSEPCONJ ptr:obj_range. ptr \<mapsto>o Untyped) \<and>* P)) s; s = sa\<rbrakk> \<Longrightarrow> ?Q2 s sa proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>default_object target_type target_bits minBound = Some obj \<and> target_type \<noteq> UntypedType \<and> distinct (map pick obj_refs) \<and> obj_refs = map ((\<lambda>x. {x}) \<circ> pick) obj_refs \<and> pick ` set obj_refs \<subseteq> obj_range \<and> cdl_current_domain sa = minBound \<and> cdl.lift ((SETSEPCONJ ptr:obj_range. ptr \<mapsto>o Untyped) \<and>* P) sa; s = sa\<rbrakk> \<Longrightarrow> cdl.lift ((SETSEPCONJ ptr:pick ` set obj_refs. ptr \<mapsto>o Untyped) \<and>* (SETSEPCONJ ptr:obj_range - pick ` set obj_refs. ptr \<mapsto>o Untyped) \<and>* P) sa proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>default_object target_type target_bits minBound = Some obj \<and> target_type \<noteq> UntypedType \<and> distinct (map pick obj_refs) \<and> obj_refs = map ((\<lambda>x. {x}) \<circ> pick) obj_refs \<and> pick ` set obj_refs \<subseteq> obj_range \<and> cdl_current_domain sa = minBound \<and> cdl.lift ((SETSEPCONJ ptr:obj_range. ptr \<mapsto>o Untyped) \<and>* P) sa; s = sa\<rbrakk> \<Longrightarrow> cdl.lift (((SETSEPCONJ ptr:pick ` set obj_refs. ptr \<mapsto>o Untyped) \<and>* (SETSEPCONJ ptr:obj_range - pick ` set obj_refs. ptr \<mapsto>o Untyped)) \<and>* P) sa proof (prove)
goal (4 subgoals):
 1. \<And>s sa. \<lbrakk>default_object target_type target_bits minBound = Some obj \<and> target_type \<noteq> UntypedType \<and> distinct (map pick obj_refs) \<and> obj_refs = map ((\<lambda>x. {x}) \<circ> pick) obj_refs \<and> pick ` set obj_refs \<subseteq> obj_range \<and> cdl_current_domain sa = minBound \<and> cdl.lift ((SETSEPCONJ ptr:obj_range. ptr \<mapsto>o Untyped) \<and>* P) sa; s = sa\<rbrakk> \<Longrightarrow> finite (pick ` set obj_refs)
 2. \<And>s sa. \<lbrakk>default_object target_type target_bits minBound = Some obj \<and> target_type \<noteq> UntypedType \<and> distinct (map pick obj_refs) \<and> obj_refs = map ((\<lambda>x. {x}) \<circ> pick) obj_refs \<and> pick ` set obj_refs \<subseteq> obj_range \<and> cdl_current_domain sa = minBound \<and> cdl.lift ((SETSEPCONJ ptr:obj_range. ptr \<mapsto>o Untyped) \<and>* P) sa; s = sa\<rbrakk> \<Longrightarrow> finite (obj_range - pick ` set obj_refs)
 3. \<And>s sa. \<lbrakk>default_object target_type target_bits minBound = Some obj \<and> target_type \<noteq> UntypedType \<and> distinct (map pick obj_refs) \<and> obj_refs = map ((\<lambda>x. {x}) \<circ> pick) obj_refs \<and> pick ` set obj_refs \<subseteq> obj_range \<and> cdl_current_domain sa = minBound \<and> cdl.lift ((SETSEPCONJ ptr:obj_range. ptr \<mapsto>o Untyped) \<and>* P) sa; s = sa\<rbrakk> \<Longrightarrow> pick ` set obj_refs \<inter> (obj_range - pick ` set obj_refs) = {}
 4. \<And>s sa. \<lbrakk>default_object target_type target_bits minBound = Some obj \<and> target_type \<noteq> UntypedType \<and> distinct (map pick obj_refs) \<and> obj_refs = map ((\<lambda>x. {x}) \<circ> pick) obj_refs \<and> pick ` set obj_refs \<subseteq> obj_range \<and> cdl_current_domain sa = minBound \<and> cdl.lift ((SETSEPCONJ ptr:obj_range. ptr \<mapsto>o Untyped) \<and>* P) sa; s = sa\<rbrakk> \<Longrightarrow> cdl.lift ((SETSEPCONJ ptr:pick ` set obj_refs \<union> (obj_range - pick ` set obj_refs). ptr \<mapsto>o Untyped) \<and>* P) sa proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>default_object target_type target_bits minBound = Some obj \<and> target_type \<noteq> UntypedType \<and> distinct (map pick obj_refs) \<and> obj_refs = map ((\<lambda>x. {x}) \<circ> pick) obj_refs \<and> pick ` set obj_refs \<subseteq> obj_range \<and> cdl_current_domain sa = minBound \<and> cdl.lift ((SETSEPCONJ ptr:obj_range. ptr \<mapsto>o Untyped) \<and>* P) sa; s = sa\<rbrakk> \<Longrightarrow> cdl.lift ((SETSEPCONJ ptr:pick ` set obj_refs \<union> obj_range. ptr \<mapsto>o Untyped) \<and>* P) sa proof (prove)
goal:
No subgoals!