theory ArchKHeap_AI

lemma set_object_vspace_objs:
  "\<lbrace>valid_vspace_objs and typ_at (a_type ko) p and
    obj_at (\<lambda>ko'. vs_refs ko \<subseteq> vs_refs ko') p  and
    (\<lambda>s. case ko of ArchObj ao \<Rightarrow>
             (\<exists>\<rhd>p)s \<longrightarrow> valid_vspace_obj ao s
            | _ \<Rightarrow> True)\<rbrace>
  set_object p ko
  \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace>" apply (simp add: valid_vspace_objs_def) apply (wp hoare_vcg_all_lift hoare_vcg_disj_lift) apply (subst imp_conv_disj) apply (subst imp_conv_disj) apply (wp hoare_vcg_all_lift hoare_vcg_disj_lift set_object_neg_lookup set_object_neg_ko) apply (wp valid_vspace_obj_typ2 [where Q="typ_at (a_type ko) p"] set_object_typ_at
         | simp)+ apply (clarsimp simp: pred_neg_def obj_at_def) apply (case_tac ko; auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vspace_objs and typ_at (a_type ko) p and obj_at (\<lambda>ko'. vs_refs ko \<subseteq> vs_refs ko') p and (\<lambda>s. case ko of ArchObj ao \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> valid_vspace_obj ao s | _ \<Rightarrow> True)\<rbrace> set_object p ko \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s)) and typ_at (a_type ko) p and obj_at (\<lambda>ko'. vs_refs ko \<subseteq> vs_refs ko') p and (\<lambda>s. case ko of ArchObj ao \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> valid_vspace_obj ao s | _ \<Rightarrow> True)\<rbrace> set_object p ko \<lbrace>\<lambda>_ s. \<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>pa. \<lbrace>?P6 pa\<rbrace> set_object p ko \<lbrace>\<lambda>rv s. (\<exists>rs. (rs \<rhd> pa) s) \<longrightarrow> (\<forall>ao. ako_at ao pa s \<longrightarrow> valid_vspace_obj ao s)\<rbrace>
 2. \<And>s. ((\<lambda>s. \<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s)) and typ_at (a_type ko) p and obj_at (\<lambda>ko'. vs_refs ko \<subseteq> vs_refs ko') p and (\<lambda>s. case ko of ArchObj ao \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> valid_vspace_obj ao s | _ \<Rightarrow> True)) s \<Longrightarrow> \<forall>x. ?P6 x s proof (prove)
goal (2 subgoals):
 1. \<And>pa. \<lbrace>?P8 pa pa\<rbrace> set_object p ko \<lbrace>\<lambda>rv s. (\<nexists>rs. (rs \<rhd> pa) s) \<or> (\<forall>ao. ako_at ao pa s \<longrightarrow> valid_vspace_obj ao s)\<rbrace>
 2. \<And>s. ((\<lambda>s. \<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s)) and typ_at (a_type ko) p and obj_at (\<lambda>ko'. vs_refs ko \<subseteq> vs_refs ko') p and (\<lambda>s. case ko of ArchObj ao \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> valid_vspace_obj ao s | _ \<Rightarrow> True)) s \<Longrightarrow> \<forall>x. ?P8 x x s proof (prove)
goal (2 subgoals):
 1. \<And>pa. \<lbrace>?P11 pa pa pa\<rbrace> set_object p ko \<lbrace>\<lambda>rv s. (\<nexists>rs. (rs \<rhd> pa) s) \<or> (\<forall>ao. \<not> ako_at ao pa s \<or> valid_vspace_obj ao s)\<rbrace>
 2. \<And>s. ((\<lambda>s. \<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s)) and typ_at (a_type ko) p and obj_at (\<lambda>ko'. vs_refs ko \<subseteq> vs_refs ko') p and (\<lambda>s. case ko of ArchObj ao \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> valid_vspace_obj ao s | _ \<Rightarrow> True)) s \<Longrightarrow> \<forall>x. ?P8 x x s
flex-flex pairs:
\<lambda>p. ?P11 p p p \<equiv>\<^sup>? \<lambda>p. ?P8 p p proof (prove)
goal (2 subgoals):
 1. \<And>pa ao. \<lbrace>\<lambda>s. ?P'31 pa pa pa s ao\<rbrace> set_object p ko \<lbrace>\<lambda>rv. valid_vspace_obj ao\<rbrace>
 2. \<And>s. ((\<lambda>s. \<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s)) and typ_at (a_type ko) p and obj_at (\<lambda>ko'. vs_refs ko \<subseteq> vs_refs ko') p and (\<lambda>s. case ko of ArchObj ao \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> valid_vspace_obj ao s | _ \<Rightarrow> True)) s \<Longrightarrow> \<forall>x. (\<nexists>rs. (rs \<rhd> x) s) \<and> obj_at (\<lambda>ko'. vs_refs ko \<subseteq> vs_refs ko') p s \<or> (\<forall>xa. (not ako_at xa x and K (p = x \<longrightarrow> ko \<noteq> ArchObj xa)) s \<or> ?P'27 x x s xa)
flex-flex pairs:
\<lambda>p. ?P'31 p p p \<equiv>\<^sup>? \<lambda>p. ?P'27 p p proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s)) \<and> typ_at (a_type ko) p s \<and> obj_at (\<lambda>ko'. vs_refs ko \<subseteq> vs_refs ko') p s \<and> (case ko of ArchObj ao \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> valid_vspace_obj ao s | _ \<Rightarrow> True) \<Longrightarrow> \<forall>x. (\<forall>rs. (rs, x) \<notin> vs_lookup s) \<or> (\<forall>xa. \<not> ako_at xa x s \<and> (p = x \<longrightarrow> ko \<noteq> ArchObj xa) \<or> valid_vspace_obj xa s) proof (prove)
goal (1 subgoal):
 1. \<And>s x koa xa rs. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. kheap s p = Some (ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); case ko of ArchObj ao \<Rightarrow> (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> valid_vspace_obj ao s | _ \<Rightarrow> True; a_type koa = a_type ko; kheap s p = Some koa; vs_refs ko \<subseteq> vs_refs koa; \<not> valid_vspace_obj xa s; kheap s x = Some (ArchObj xa) \<or> p = x \<and> ko = ArchObj xa; (rs \<rhd> x) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!