theory ArchKHeap_AI

lemma set_object_vs_lookup:
  "\<lbrace>\<lambda>s. obj_at (\<lambda>ko'. vs_refs ko = vs_refs ko') p s \<and> P (vs_lookup s) \<rbrace>
  set_object p ko
  \<lbrace>\<lambda>_ s. P (vs_lookup s)\<rbrace>" apply (simp add: set_object_def get_object_def) apply wp apply clarsimp apply (erule rsubst [where P=P]) apply (rule order_antisym) apply (rule vs_lookup_sub) apply (clarsimp simp: obj_at_def) apply simp apply (rule vs_lookup_sub) 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. obj_at (\<lambda>ko'. vs_refs ko = vs_refs ko') p s \<and> P (vs_lookup s)\<rbrace> set_object p ko \<lbrace>\<lambda>_ s. P (vs_lookup s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. obj_at (\<lambda>ko'. vs_refs ko = vs_refs ko') p s \<and> P (vs_lookup 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. P (vs_lookup s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. obj_at (\<lambda>ko'. vs_refs ko = vs_refs ko') p s \<and> P (vs_lookup s) \<Longrightarrow> (\<exists>y. kheap s p = Some y) \<longrightarrow> a_type (the (kheap s p)) = a_type ko \<longrightarrow> P (vs_lookup (s\<lparr>kheap := (kheap s)(p \<mapsto> ko)\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>obj_at (\<lambda>ko'. vs_refs ko = vs_refs ko') p s; P (vs_lookup s); kheap s p = Some y; a_type y = a_type ko\<rbrakk> \<Longrightarrow> P (vs_lookup (s\<lparr>kheap := \<lambda>a. if a = p then Some ko else kheap s a\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>obj_at (\<lambda>ko'. vs_refs ko = vs_refs ko') p s; kheap s p = Some y; a_type y = a_type ko\<rbrakk> \<Longrightarrow> vs_lookup s = vs_lookup (s\<lparr>kheap := \<lambda>a. if a = p then Some ko else kheap s a\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s y. \<lbrakk>obj_at (\<lambda>ko'. vs_refs ko = vs_refs ko') p s; kheap s p = Some y; a_type y = a_type ko\<rbrakk> \<Longrightarrow> vs_lookup s \<subseteq> vs_lookup (s\<lparr>kheap := \<lambda>a. if a = p then Some ko else kheap s a\<rparr>)
 2. \<And>s y. \<lbrakk>obj_at (\<lambda>ko'. vs_refs ko = vs_refs ko') p s; kheap s p = Some y; a_type y = a_type ko\<rbrakk> \<Longrightarrow> vs_lookup (s\<lparr>kheap := \<lambda>a. if a = p then Some ko else kheap s a\<rparr>) \<subseteq> vs_lookup s proof (prove)
goal (3 subgoals):
 1. \<And>s y koa pa. \<lbrakk>obj_at (\<lambda>ko'. vs_refs ko = vs_refs ko') p s; kheap s p = Some y; a_type y = a_type ko; ko_at koa pa s\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko'. vs_refs koa \<subseteq> vs_refs ko') pa (s\<lparr>kheap := \<lambda>a. if a = p then Some ko else kheap s a\<rparr>)
 2. \<And>s y. \<lbrakk>obj_at (\<lambda>ko'. vs_refs ko = vs_refs ko') p s; kheap s p = Some y; a_type y = a_type ko\<rbrakk> \<Longrightarrow> graph_of (asid_table s) \<subseteq> graph_of (asid_table (s\<lparr>kheap := \<lambda>a. if a = p then Some ko else kheap s a\<rparr>))
 3. \<And>s y. \<lbrakk>obj_at (\<lambda>ko'. vs_refs ko = vs_refs ko') p s; kheap s p = Some y; a_type y = a_type ko\<rbrakk> \<Longrightarrow> vs_lookup (s\<lparr>kheap := \<lambda>a. if a = p then Some ko else kheap s a\<rparr>) \<subseteq> vs_lookup s proof (prove)
goal (2 subgoals):
 1. \<And>s y. \<lbrakk>obj_at (\<lambda>ko'. vs_refs ko = vs_refs ko') p s; kheap s p = Some y; a_type y = a_type ko\<rbrakk> \<Longrightarrow> graph_of (asid_table s) \<subseteq> graph_of (asid_table (s\<lparr>kheap := \<lambda>a. if a = p then Some ko else kheap s a\<rparr>))
 2. \<And>s y. \<lbrakk>obj_at (\<lambda>ko'. vs_refs ko = vs_refs ko') p s; kheap s p = Some y; a_type y = a_type ko\<rbrakk> \<Longrightarrow> vs_lookup (s\<lparr>kheap := \<lambda>a. if a = p then Some ko else kheap s a\<rparr>) \<subseteq> vs_lookup s proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>obj_at (\<lambda>ko'. vs_refs ko = vs_refs ko') p s; kheap s p = Some y; a_type y = a_type ko\<rbrakk> \<Longrightarrow> vs_lookup (s\<lparr>kheap := \<lambda>a. if a = p then Some ko else kheap s a\<rparr>) \<subseteq> vs_lookup s proof (prove)
goal (2 subgoals):
 1. \<And>s y koa pa. \<lbrakk>obj_at (\<lambda>ko'. vs_refs ko = 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. \<lbrakk>obj_at (\<lambda>ko'. vs_refs ko = 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. \<lbrakk>obj_at (\<lambda>ko'. vs_refs ko = 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!