theory ArchKHeap_AI

lemma set_object_neg_lookup:
  "\<lbrace>\<lambda>s. \<not> (\<exists>rs. (rs \<rhd> p') s) \<and> obj_at (\<lambda>ko'. vs_refs ko \<subseteq> vs_refs ko') p s \<rbrace>
  set_object p ko
  \<lbrace>\<lambda>_ s. \<not> (\<exists>rs. (rs \<rhd> p') s)\<rbrace>" apply (simp add: set_object_def get_object_def) apply wp apply clarsimp apply (erule_tac x=rs in allE) apply (erule notE) apply (erule vs_lookup_stateI) apply (clarsimp simp: obj_at_def split: if_split_asm) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<nexists>rs. (rs \<rhd> p') s) \<and> obj_at (\<lambda>ko'. vs_refs ko \<subseteq> vs_refs ko') p s\<rbrace> set_object p ko \<lbrace>\<lambda>_ s. \<nexists>rs. (rs \<rhd> p') s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>rs. (rs, p') \<notin> vs_lookup s) \<and> obj_at (\<lambda>ko'. vs_refs ko \<subseteq> vs_refs ko') p s\<rbrace> do kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh p = Some y);
return (the (kh p))
od;
y <- assert (a_type kobj = a_type ko);
s <- get;
put (s\<lparr>kheap := (kheap s)(p \<mapsto> ko)\<rparr>)
od \<lbrace>\<lambda>_ s. \<forall>rs. (rs, p') \<notin> vs_lookup s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<forall>rs. (rs, p') \<notin> vs_lookup s) \<and> obj_at (\<lambda>ko'. vs_refs ko \<subseteq> vs_refs ko') p s \<Longrightarrow> (\<exists>y. kheap s p = Some y) \<longrightarrow> a_type (the (kheap s p)) = a_type ko \<longrightarrow> (\<forall>rs. (rs, p') \<notin> vs_lookup (s\<lparr>kheap := (kheap s)(p \<mapsto> ko)\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s y rs. \<lbrakk>\<forall>rs. (rs, p') \<notin> vs_lookup s; obj_at (\<lambda>ko'. vs_refs ko \<subseteq> vs_refs ko') p s; kheap s p = Some y; a_type y = a_type ko; (rs \<rhd> p') (s\<lparr>kheap := \<lambda>a. if a = p then Some ko else kheap s a\<rparr>)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s y rs. \<lbrakk>obj_at (\<lambda>ko'. vs_refs ko \<subseteq> vs_refs ko') p s; kheap s p = Some y; a_type y = a_type ko; (rs \<rhd> p') (s\<lparr>kheap := \<lambda>a. if a = p then Some ko else kheap s a\<rparr>); (rs, p') \<notin> vs_lookup s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s y rs. \<lbrakk>obj_at (\<lambda>ko'. vs_refs ko \<subseteq> vs_refs ko') p s; kheap s p = Some y; a_type y = a_type ko; (rs \<rhd> p') (s\<lparr>kheap := \<lambda>a. if a = p then Some ko else kheap s a\<rparr>)\<rbrakk> \<Longrightarrow> (rs \<rhd> p') s proof (prove)
goal (2 subgoals):
 1. \<And>s y rs koa pa. \<lbrakk>obj_at (\<lambda>ko'. vs_refs ko \<subseteq> vs_refs ko') p s; kheap s p = Some y; a_type y = a_type ko; ko_at koa pa (s\<lparr>kheap := \<lambda>a. if a = p then Some ko else kheap s a\<rparr>)\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko'. vs_refs koa \<subseteq> vs_refs ko') pa s
 2. \<And>s y rs. \<lbrakk>obj_at (\<lambda>ko'. vs_refs ko \<subseteq> vs_refs ko') p s; kheap s p = Some y; a_type y = a_type ko\<rbrakk> \<Longrightarrow> graph_of (asid_table (s\<lparr>kheap := \<lambda>a. if a = p then Some ko else kheap s a\<rparr>)) \<subseteq> graph_of (asid_table s) proof (prove)
goal (1 subgoal):
 1. \<And>s y rs. \<lbrakk>obj_at (\<lambda>ko'. vs_refs ko \<subseteq> vs_refs ko') p s; kheap s p = Some y; a_type y = a_type ko\<rbrakk> \<Longrightarrow> graph_of (asid_table (s\<lparr>kheap := \<lambda>a. if a = p then Some ko else kheap s a\<rparr>)) \<subseteq> graph_of (asid_table s) proof (prove)
goal:
No subgoals!