theory Fastpath_C

lemma sym_refs_upd_sD:
  "\<lbrakk> sym_refs ((state_refs_of' s) (p := S)); valid_pspace' s;
            ko_at' ko p s; refs_of' (injectKO koEx) = S;
            objBits koEx = objBits ko \<rbrakk>
      \<Longrightarrow> \<exists>s'. sym_refs (state_refs_of' s')
               \<and> (\<forall>p' (ko' :: endpoint). ko_at' ko' p' s \<and> injectKO ko' \<noteq> injectKO ko
                          \<longrightarrow> ko_at' ko' p' s')
               \<and> (\<forall>p' (ko' :: Structures_H.notification). ko_at' ko' p' s \<and> injectKO ko' \<noteq> injectKO ko
                          \<longrightarrow> ko_at' ko' p' s')
               \<and> (ko_at' koEx p s')" apply (rule exI, rule conjI) apply (rule state_refs_of'_upd[where ko'="injectKO koEx" and ptr=p and s=s,
                                  THEN ssubst[where P=sym_refs], rotated 2]) apply simp+ apply (clarsimp simp: obj_at'_def ko_wp_at'_def projectKOs) apply (clarsimp simp: project_inject objBits_def) apply (clarsimp simp: obj_at'_def ps_clear_upd projectKOs
                 split: if_split) apply (clarsimp simp: project_inject objBits_def) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sym_refs ((state_refs_of' s)(p := S)); valid_pspace' s; ko_at' ko p s; refs_of' (injectKOS koEx) = S; objBits koEx = objBits ko\<rbrakk> \<Longrightarrow> \<exists>s'. sym_refs (state_refs_of' s') \<and> (\<forall>p' ko'. ko_at' ko' p' s \<and> injectKOS ko' \<noteq> injectKOS ko \<longrightarrow> ko_at' ko' p' s') \<and> (\<forall>p' ko'. ko_at' ko' p' s \<and> injectKOS ko' \<noteq> injectKOS ko \<longrightarrow> ko_at' ko' p' s') \<and> ko_at' koEx p s' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sym_refs ((state_refs_of' s)(p := S)); valid_pspace' s; ko_at' ko p s; refs_of' (injectKOS koEx) = S; objBits koEx = objBits ko\<rbrakk> \<Longrightarrow> sym_refs (state_refs_of' ?s')
 2. \<lbrakk>sym_refs ((state_refs_of' s)(p := S)); valid_pspace' s; ko_at' ko p s; refs_of' (injectKOS koEx) = S; objBits koEx = objBits ko\<rbrakk> \<Longrightarrow> (\<forall>p' ko'. ko_at' ko' p' s \<and> injectKOS ko' \<noteq> injectKOS ko \<longrightarrow> ko_at' ko' p' ?s') \<and> (\<forall>p' ko'. ko_at' ko' p' s \<and> injectKOS ko' \<noteq> injectKOS ko \<longrightarrow> ko_at' ko' p' ?s') \<and> ko_at' koEx p ?s' proof (prove)
goal (4 subgoals):
 1. \<lbrakk>sym_refs ((state_refs_of' s)(p := S)); valid_pspace' s; ko_at' ko p s; refs_of' (injectKOS koEx) = S; objBits koEx = objBits ko\<rbrakk> \<Longrightarrow> sym_refs ((state_refs_of' s)(p := refs_of' (injectKOS koEx)))
 2. \<lbrakk>sym_refs ((state_refs_of' s)(p := S)); valid_pspace' s; ko_at' ko p s; refs_of' (injectKOS koEx) = S; objBits koEx = objBits ko\<rbrakk> \<Longrightarrow> valid_pspace' s
 3. \<lbrakk>sym_refs ((state_refs_of' s)(p := S)); valid_pspace' s; ko_at' ko p s; refs_of' (injectKOS koEx) = S; objBits koEx = objBits ko\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. objBitsKO ko = objBitsKO (injectKOS koEx)) p s
 4. \<lbrakk>sym_refs ((state_refs_of' s)(p := S)); valid_pspace' s; ko_at' ko p s; refs_of' (injectKOS koEx) = S; objBits koEx = objBits ko\<rbrakk> \<Longrightarrow> (\<forall>p' ko'. ko_at' ko' p' s \<and> injectKOS ko' \<noteq> injectKOS ko \<longrightarrow> ko_at' ko' p' (s\<lparr>ksPSpace := (ksPSpace s)(p \<mapsto> injectKOS koEx)\<rparr>)) \<and> (\<forall>p' ko'. ko_at' ko' p' s \<and> injectKOS ko' \<noteq> injectKOS ko \<longrightarrow> ko_at' ko' p' (s\<lparr>ksPSpace := (ksPSpace s)(p \<mapsto> injectKOS koEx)\<rparr>)) \<and> ko_at' koEx p (s\<lparr>ksPSpace := (ksPSpace s)(p \<mapsto> injectKOS koEx)\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sym_refs ((state_refs_of' s)(p := S)); valid_pspace' s; ko_at' ko p s; refs_of' (injectKOS koEx) = S; objBits koEx = objBits ko\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. objBitsKO ko = objBitsKO (injectKOS koEx)) p s
 2. \<lbrakk>sym_refs ((state_refs_of' s)(p := S)); valid_pspace' s; ko_at' ko p s; refs_of' (injectKOS koEx) = S; objBits koEx = objBits ko\<rbrakk> \<Longrightarrow> (\<forall>p' ko'. ko_at' ko' p' s \<and> injectKOS ko' \<noteq> injectKOS ko \<longrightarrow> ko_at' ko' p' (s\<lparr>ksPSpace := (ksPSpace s)(p \<mapsto> injectKOS koEx)\<rparr>)) \<and> (\<forall>p' ko'. ko_at' ko' p' s \<and> injectKOS ko' \<noteq> injectKOS ko \<longrightarrow> ko_at' ko' p' (s\<lparr>ksPSpace := (ksPSpace s)(p \<mapsto> injectKOS koEx)\<rparr>)) \<and> ko_at' koEx p (s\<lparr>ksPSpace := (ksPSpace s)(p \<mapsto> injectKOS koEx)\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>koa. \<lbrakk>sym_refs ((state_refs_of' s)(p := refs_of' (injectKOS koEx))); valid_pspace' s; objBits koEx = objBits ko; S = refs_of' (injectKOS koEx); ksPSpace s p = Some koa; is_aligned p (objBitsKO koa); projectKO_opt koa = Some ko; ps_clear p (objBitsKO koa) s\<rbrakk> \<Longrightarrow> objBitsKO koa = objBitsKO (injectKOS koEx)
 2. \<lbrakk>sym_refs ((state_refs_of' s)(p := S)); valid_pspace' s; ko_at' ko p s; refs_of' (injectKOS koEx) = S; objBits koEx = objBits ko\<rbrakk> \<Longrightarrow> (\<forall>p' ko'. ko_at' ko' p' s \<and> injectKOS ko' \<noteq> injectKOS ko \<longrightarrow> ko_at' ko' p' (s\<lparr>ksPSpace := (ksPSpace s)(p \<mapsto> injectKOS koEx)\<rparr>)) \<and> (\<forall>p' ko'. ko_at' ko' p' s \<and> injectKOS ko' \<noteq> injectKOS ko \<longrightarrow> ko_at' ko' p' (s\<lparr>ksPSpace := (ksPSpace s)(p \<mapsto> injectKOS koEx)\<rparr>)) \<and> ko_at' koEx p (s\<lparr>ksPSpace := (ksPSpace s)(p \<mapsto> injectKOS koEx)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sym_refs ((state_refs_of' s)(p := S)); valid_pspace' s; ko_at' ko p s; refs_of' (injectKOS koEx) = S; objBits koEx = objBits ko\<rbrakk> \<Longrightarrow> (\<forall>p' ko'. ko_at' ko' p' s \<and> injectKOS ko' \<noteq> injectKOS ko \<longrightarrow> ko_at' ko' p' (s\<lparr>ksPSpace := (ksPSpace s)(p \<mapsto> injectKOS koEx)\<rparr>)) \<and> (\<forall>p' ko'. ko_at' ko' p' s \<and> injectKOS ko' \<noteq> injectKOS ko \<longrightarrow> ko_at' ko' p' (s\<lparr>ksPSpace := (ksPSpace s)(p \<mapsto> injectKOS koEx)\<rparr>)) \<and> ko_at' koEx p (s\<lparr>ksPSpace := (ksPSpace s)(p \<mapsto> injectKOS koEx)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>koa. \<lbrakk>sym_refs ((state_refs_of' s)(p := refs_of' (injectKOS koEx))); valid_pspace' s; objBits koEx = objBits ko; S = refs_of' (injectKOS koEx); ksPSpace s p = Some koa; is_aligned p (objBitsKO koa); projectKO_opt koa = Some ko; ps_clear p (objBitsKO koa) s\<rbrakk> \<Longrightarrow> (\<forall>ko'. koa = KOEndpoint ko' \<and> is_aligned p (objBitsKO (KOEndpoint ko')) \<and> ps_clear p (objBitsKO (KOEndpoint ko')) s \<and> KOEndpoint ko' \<noteq> injectKOS ko \<longrightarrow> injectKOS koEx = KOEndpoint ko') \<and> (\<forall>ko'. koa = KONotification ko' \<and> is_aligned p (objBitsKO (KONotification ko')) \<and> ps_clear p (objBitsKO (KONotification ko')) s \<and> KONotification ko' \<noteq> injectKOS ko \<longrightarrow> injectKOS koEx = KONotification ko') \<and> is_aligned p (objBitsKO (injectKOS koEx)) \<and> projectKO_opt (injectKOS koEx) = Some koEx \<and> ps_clear p (objBitsKO (injectKOS koEx)) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sym_refs ((state_refs_of' s)(p := refs_of' (injectKOS koEx))); valid_pspace' s; objBitsKO (injectKOS koEx) = objBitsKO (injectKOS ko); S = refs_of' (injectKOS koEx); ksPSpace s p = Some (injectKOS ko); is_aligned p (objBitsKO (injectKOS ko)); ps_clear p (objBitsKO (injectKOS ko)) s\<rbrakk> \<Longrightarrow> (\<forall>ko'. injectKOS ko = KOEndpoint ko' \<and> is_aligned p (objBitsKO (KOEndpoint ko')) \<and> ps_clear p (objBitsKO (KOEndpoint ko')) s \<and> KOEndpoint ko' \<noteq> injectKOS ko \<longrightarrow> injectKOS koEx = KOEndpoint ko') \<and> (\<forall>ko'. injectKOS ko = KONotification ko' \<and> is_aligned p (objBitsKO (KONotification ko')) \<and> ps_clear p (objBitsKO (KONotification ko')) s \<and> KONotification ko' \<noteq> injectKOS ko \<longrightarrow> injectKOS koEx = KONotification ko') proof (prove)
goal:
No subgoals!