theory Invariants_H

lemma tcb_at_cte_at':
  "tcb_at' t s \<Longrightarrow> cte_at' t s" apply (clarsimp simp add: cte_wp_at_cases' obj_at'_def projectKO_def
                       del: disjCI) apply (case_tac ko) apply (simp_all add: projectKO_opt_tcb fail_def) apply (rule exI[where x=0]) apply (clarsimp simp add: return_def objBits_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_at' t s \<Longrightarrow> cte_wp_at' (\<lambda>_. True) t s proof (prove)
goal (1 subgoal):
 1. \<And>ko obj. \<lbrakk>ksPSpace s t = Some ko; is_aligned t (objBitsKO ko); ps_clear t (objBitsKO ko) s; fst ((case projectKO_opt ko of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s) = {(obj, s)}\<rbrakk> \<Longrightarrow> (\<exists>cte. ko = KOCTE cte) \<and> is_aligned t cte_level_bits \<and> ps_clear t cteSizeBits s \<or> (\<exists>n. (\<exists>tcb. ksPSpace s (t - n) = Some (KOTCB tcb)) \<and> is_aligned (t - n) tcbBlockSizeBits \<and> (\<exists>getF setF. tcb_cte_cases n = Some (getF, setF)) \<and> ps_clear (t - n) tcbBlockSizeBits s) proof (prove)
goal (8 subgoals):
 1. \<And>ko obj x1. \<lbrakk>ksPSpace s t = Some ko; is_aligned t (objBitsKO ko); ps_clear t (objBitsKO ko) s; fst ((case projectKO_opt ko of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s) = {(obj, s)}; ko = KOEndpoint x1\<rbrakk> \<Longrightarrow> (\<exists>cte. ko = KOCTE cte) \<and> is_aligned t cte_level_bits \<and> ps_clear t cteSizeBits s \<or> (\<exists>n. (\<exists>tcb. ksPSpace s (t - n) = Some (KOTCB tcb)) \<and> is_aligned (t - n) tcbBlockSizeBits \<and> (\<exists>getF setF. tcb_cte_cases n = Some (getF, setF)) \<and> ps_clear (t - n) tcbBlockSizeBits s)
 2. \<And>ko obj x2. \<lbrakk>ksPSpace s t = Some ko; is_aligned t (objBitsKO ko); ps_clear t (objBitsKO ko) s; fst ((case projectKO_opt ko of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s) = {(obj, s)}; ko = KONotification x2\<rbrakk> \<Longrightarrow> (\<exists>cte. ko = KOCTE cte) \<and> is_aligned t cte_level_bits \<and> ps_clear t cteSizeBits s \<or> (\<exists>n. (\<exists>tcb. ksPSpace s (t - n) = Some (KOTCB tcb)) \<and> is_aligned (t - n) tcbBlockSizeBits \<and> (\<exists>getF setF. tcb_cte_cases n = Some (getF, setF)) \<and> ps_clear (t - n) tcbBlockSizeBits s)
 3. \<And>ko obj. \<lbrakk>ksPSpace s t = Some ko; is_aligned t (objBitsKO ko); ps_clear t (objBitsKO ko) s; fst ((case projectKO_opt ko of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s) = {(obj, s)}; ko = KOKernelData\<rbrakk> \<Longrightarrow> (\<exists>cte. ko = KOCTE cte) \<and> is_aligned t cte_level_bits \<and> ps_clear t cteSizeBits s \<or> (\<exists>n. (\<exists>tcb. ksPSpace s (t - n) = Some (KOTCB tcb)) \<and> is_aligned (t - n) tcbBlockSizeBits \<and> (\<exists>getF setF. tcb_cte_cases n = Some (getF, setF)) \<and> ps_clear (t - n) tcbBlockSizeBits s)
 4. \<And>ko obj. \<lbrakk>ksPSpace s t = Some ko; is_aligned t (objBitsKO ko); ps_clear t (objBitsKO ko) s; fst ((case projectKO_opt ko of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s) = {(obj, s)}; ko = KOUserData\<rbrakk> \<Longrightarrow> (\<exists>cte. ko = KOCTE cte) \<and> is_aligned t cte_level_bits \<and> ps_clear t cteSizeBits s \<or> (\<exists>n. (\<exists>tcb. ksPSpace s (t - n) = Some (KOTCB tcb)) \<and> is_aligned (t - n) tcbBlockSizeBits \<and> (\<exists>getF setF. tcb_cte_cases n = Some (getF, setF)) \<and> ps_clear (t - n) tcbBlockSizeBits s)
 5. \<And>ko obj. \<lbrakk>ksPSpace s t = Some ko; is_aligned t (objBitsKO ko); ps_clear t (objBitsKO ko) s; fst ((case projectKO_opt ko of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s) = {(obj, s)}; ko = KOUserDataDevice\<rbrakk> \<Longrightarrow> (\<exists>cte. ko = KOCTE cte) \<and> is_aligned t cte_level_bits \<and> ps_clear t cteSizeBits s \<or> (\<exists>n. (\<exists>tcb. ksPSpace s (t - n) = Some (KOTCB tcb)) \<and> is_aligned (t - n) tcbBlockSizeBits \<and> (\<exists>getF setF. tcb_cte_cases n = Some (getF, setF)) \<and> ps_clear (t - n) tcbBlockSizeBits s)
 6. \<And>ko obj x6. \<lbrakk>ksPSpace s t = Some ko; is_aligned t (objBitsKO ko); ps_clear t (objBitsKO ko) s; fst ((case projectKO_opt ko of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s) = {(obj, s)}; ko = KOTCB x6\<rbrakk> \<Longrightarrow> (\<exists>cte. ko = KOCTE cte) \<and> is_aligned t cte_level_bits \<and> ps_clear t cteSizeBits s \<or> (\<exists>n. (\<exists>tcb. ksPSpace s (t - n) = Some (KOTCB tcb)) \<and> is_aligned (t - n) tcbBlockSizeBits \<and> (\<exists>getF setF. tcb_cte_cases n = Some (getF, setF)) \<and> ps_clear (t - n) tcbBlockSizeBits s)
 7. \<And>ko obj x7. \<lbrakk>ksPSpace s t = Some ko; is_aligned t (objBitsKO ko); ps_clear t (objBitsKO ko) s; fst ((case projectKO_opt ko of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s) = {(obj, s)}; ko = KOCTE x7\<rbrakk> \<Longrightarrow> (\<exists>cte. ko = KOCTE cte) \<and> is_aligned t cte_level_bits \<and> ps_clear t cteSizeBits s \<or> (\<exists>n. (\<exists>tcb. ksPSpace s (t - n) = Some (KOTCB tcb)) \<and> is_aligned (t - n) tcbBlockSizeBits \<and> (\<exists>getF setF. tcb_cte_cases n = Some (getF, setF)) \<and> ps_clear (t - n) tcbBlockSizeBits s)
 8. \<And>ko obj x8. \<lbrakk>ksPSpace s t = Some ko; is_aligned t (objBitsKO ko); ps_clear t (objBitsKO ko) s; fst ((case projectKO_opt ko of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s) = {(obj, s)}; ko = KOArch x8\<rbrakk> \<Longrightarrow> (\<exists>cte. ko = KOCTE cte) \<and> is_aligned t cte_level_bits \<and> ps_clear t cteSizeBits s \<or> (\<exists>n. (\<exists>tcb. ksPSpace s (t - n) = Some (KOTCB tcb)) \<and> is_aligned (t - n) tcbBlockSizeBits \<and> (\<exists>getF setF. tcb_cte_cases n = Some (getF, setF)) \<and> ps_clear (t - n) tcbBlockSizeBits s) proof (prove)
goal (1 subgoal):
 1. \<And>ko obj x6. \<lbrakk>ksPSpace s t = Some (KOTCB x6); is_aligned t (objBitsKO (KOTCB x6)); ps_clear t (objBitsKO (KOTCB x6)) s; fst (return x6 s) = {(obj, s)}; ko = KOTCB x6\<rbrakk> \<Longrightarrow> \<exists>n. (\<exists>tcb. ksPSpace s (t - n) = Some (KOTCB tcb)) \<and> is_aligned (t - n) tcbBlockSizeBits \<and> (\<exists>getF setF. tcb_cte_cases n = Some (getF, setF)) \<and> ps_clear (t - n) tcbBlockSizeBits s proof (prove)
goal (1 subgoal):
 1. \<And>ko obj x6. \<lbrakk>ksPSpace s t = Some (KOTCB x6); is_aligned t (objBitsKO (KOTCB x6)); ps_clear t (objBitsKO (KOTCB x6)) s; fst (return x6 s) = {(obj, s)}; ko = KOTCB x6\<rbrakk> \<Longrightarrow> (\<exists>tcb. ksPSpace s (t - 0) = Some (KOTCB tcb)) \<and> is_aligned (t - 0) tcbBlockSizeBits \<and> (\<exists>getF setF. tcb_cte_cases 0 = Some (getF, setF)) \<and> ps_clear (t - 0) tcbBlockSizeBits s proof (prove)
goal:
No subgoals!