theory TcbAcc_R

lemma not_obj_at':
  "(\<not>obj_at' (\<lambda>tcb::tcb. P tcb) t s) = (\<not>typ_at' TCBT t s \<or> obj_at' (Not \<circ> P) t s)" apply (simp add: obj_at'_real_def projectKOs
                   typ_at'_def ko_wp_at'_def objBits_simps) apply (rule iffI) apply (clarsimp) apply (case_tac ko) apply (clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<not> obj_at' P t s) = (\<not> typ_at' TCBT t s \<or> obj_at' (Not \<circ> P) t s) proof (prove)
goal (1 subgoal):
 1. (\<forall>ko. is_aligned t (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits) \<longrightarrow> ksPSpace s t = Some ko \<longrightarrow> (\<forall>obj. ko = KOTCB obj \<longrightarrow> \<not> P obj) \<or> \<not> ps_clear t (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits) s) = ((\<forall>ko. koTypeOf ko = TCBT \<longrightarrow> is_aligned t (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits) \<longrightarrow> ksPSpace s t = Some ko \<longrightarrow> \<not> ps_clear t (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits) s) \<or> (\<exists>ko. ksPSpace s t = Some ko \<and> is_aligned t (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch a \<Rightarrow> archObjSize a | _ \<Rightarrow> pageBits) \<and> (\<exists>obj. ko = KOTCB obj \<and> \<not> P obj) \<and> ps_clear t (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch a \<Rightarrow> archObjSize a | _ \<Rightarrow> pageBits) s)) proof (prove)
goal (2 subgoals):
 1. \<forall>ko. is_aligned t (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits) \<longrightarrow> ksPSpace s t = Some ko \<longrightarrow> (\<forall>obj. ko = KOTCB obj \<longrightarrow> \<not> P obj) \<or> \<not> ps_clear t (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits) s \<Longrightarrow> (\<forall>ko. koTypeOf ko = TCBT \<longrightarrow> is_aligned t (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits) \<longrightarrow> ksPSpace s t = Some ko \<longrightarrow> \<not> ps_clear t (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits) s) \<or> (\<exists>ko. ksPSpace s t = Some ko \<and> is_aligned t (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch a \<Rightarrow> archObjSize a | _ \<Rightarrow> pageBits) \<and> (\<exists>obj. ko = KOTCB obj \<and> \<not> P obj) \<and> ps_clear t (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch a \<Rightarrow> archObjSize a | _ \<Rightarrow> pageBits) s)
 2. (\<forall>ko. koTypeOf ko = TCBT \<longrightarrow> is_aligned t (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits) \<longrightarrow> ksPSpace s t = Some ko \<longrightarrow> \<not> ps_clear t (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits) s) \<or> (\<exists>ko. ksPSpace s t = Some ko \<and> is_aligned t (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch a \<Rightarrow> archObjSize a | _ \<Rightarrow> pageBits) \<and> (\<exists>obj. ko = KOTCB obj \<and> \<not> P obj) \<and> ps_clear t (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch a \<Rightarrow> archObjSize a | _ \<Rightarrow> pageBits) s) \<Longrightarrow> \<forall>ko. is_aligned t (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits) \<longrightarrow> ksPSpace s t = Some ko \<longrightarrow> (\<forall>obj. ko = KOTCB obj \<longrightarrow> \<not> P obj) \<or> \<not> ps_clear t (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits) s proof (prove)
goal (2 subgoals):
 1. \<And>ko. \<lbrakk>\<forall>obj. ko \<noteq> KOTCB obj; koTypeOf ko = TCBT; is_aligned t (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits); ksPSpace s t = Some ko; ps_clear t (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits) s\<rbrakk> \<Longrightarrow> False
 2. (\<forall>ko. koTypeOf ko = TCBT \<longrightarrow> is_aligned t (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits) \<longrightarrow> ksPSpace s t = Some ko \<longrightarrow> \<not> ps_clear t (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits) s) \<or> (\<exists>ko. ksPSpace s t = Some ko \<and> is_aligned t (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch a \<Rightarrow> archObjSize a | _ \<Rightarrow> pageBits) \<and> (\<exists>obj. ko = KOTCB obj \<and> \<not> P obj) \<and> ps_clear t (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch a \<Rightarrow> archObjSize a | _ \<Rightarrow> pageBits) s) \<Longrightarrow> \<forall>ko. is_aligned t (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits) \<longrightarrow> ksPSpace s t = Some ko \<longrightarrow> (\<forall>obj. ko = KOTCB obj \<longrightarrow> \<not> P obj) \<or> \<not> ps_clear t (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits) s proof (prove)
goal (9 subgoals):
 1. \<And>ko x1. \<lbrakk>\<forall>obj. ko \<noteq> KOTCB obj; koTypeOf ko = TCBT; is_aligned t (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits); ksPSpace s t = Some ko; ps_clear t (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits) s; ko = KOEndpoint x1\<rbrakk> \<Longrightarrow> False
 2. \<And>ko x2. \<lbrakk>\<forall>obj. ko \<noteq> KOTCB obj; koTypeOf ko = TCBT; is_aligned t (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits); ksPSpace s t = Some ko; ps_clear t (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits) s; ko = KONotification x2\<rbrakk> \<Longrightarrow> False
 3. \<And>ko. \<lbrakk>\<forall>obj. ko \<noteq> KOTCB obj; koTypeOf ko = TCBT; is_aligned t (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits); ksPSpace s t = Some ko; ps_clear t (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits) s; ko = KOKernelData\<rbrakk> \<Longrightarrow> False
 4. \<And>ko. \<lbrakk>\<forall>obj. ko \<noteq> KOTCB obj; koTypeOf ko = TCBT; is_aligned t (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits); ksPSpace s t = Some ko; ps_clear t (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits) s; ko = KOUserData\<rbrakk> \<Longrightarrow> False
 5. \<And>ko. \<lbrakk>\<forall>obj. ko \<noteq> KOTCB obj; koTypeOf ko = TCBT; is_aligned t (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits); ksPSpace s t = Some ko; ps_clear t (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits) s; ko = KOUserDataDevice\<rbrakk> \<Longrightarrow> False
 6. \<And>ko x6. \<lbrakk>\<forall>obj. ko \<noteq> KOTCB obj; koTypeOf ko = TCBT; is_aligned t (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits); ksPSpace s t = Some ko; ps_clear t (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits) s; ko = KOTCB x6\<rbrakk> \<Longrightarrow> False
 7. \<And>ko x7. \<lbrakk>\<forall>obj. ko \<noteq> KOTCB obj; koTypeOf ko = TCBT; is_aligned t (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits); ksPSpace s t = Some ko; ps_clear t (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits) s; ko = KOCTE x7\<rbrakk> \<Longrightarrow> False
 8. \<And>ko x8. \<lbrakk>\<forall>obj. ko \<noteq> KOTCB obj; koTypeOf ko = TCBT; is_aligned t (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits); ksPSpace s t = Some ko; ps_clear t (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits) s; ko = KOArch x8\<rbrakk> \<Longrightarrow> False
 9. (\<forall>ko. koTypeOf ko = TCBT \<longrightarrow> is_aligned t (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits) \<longrightarrow> ksPSpace s t = Some ko \<longrightarrow> \<not> ps_clear t (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits) s) \<or> (\<exists>ko. ksPSpace s t = Some ko \<and> is_aligned t (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch a \<Rightarrow> archObjSize a | _ \<Rightarrow> pageBits) \<and> (\<exists>obj. ko = KOTCB obj \<and> \<not> P obj) \<and> ps_clear t (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch a \<Rightarrow> archObjSize a | _ \<Rightarrow> pageBits) s) \<Longrightarrow> \<forall>ko. is_aligned t (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits) \<longrightarrow> ksPSpace s t = Some ko \<longrightarrow> (\<forall>obj. ko = KOTCB obj \<longrightarrow> \<not> P obj) \<or> \<not> ps_clear t (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits) s proof (prove)
goal:
No subgoals!