theory Invariants_H

lemma typ_at_tcb':
  "typ_at' TCBT = tcb_at'" apply (rule ext)+ apply (simp add: obj_at'_real_def typ_at'_def) apply (simp add: ko_wp_at'_def) apply (rule iffI) apply clarsimp apply (case_tac ko) apply (auto simp: projectKO_opt_tcb)[9] apply (case_tac ko) apply (auto simp: projectKO_opt_tcb) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. typ_at' TCBT = tcb_at' proof (prove)
goal (1 subgoal):
 1. \<And>x xa. typ_at' TCBT x xa = tcb_at' x xa proof (prove)
goal (1 subgoal):
 1. \<And>x xa. ko_wp_at' (\<lambda>ko. koTypeOf ko = TCBT) x xa = ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj) x xa proof (prove)
goal (1 subgoal):
 1. \<And>x xa. (\<exists>ko. ksPSpace xa x = Some ko \<and> is_aligned x (objBitsKO ko) \<and> koTypeOf ko = TCBT \<and> ps_clear x (objBitsKO ko) xa) = (\<exists>ko. ksPSpace xa x = Some ko \<and> is_aligned x (objBitsKO ko) \<and> (\<exists>obj. projectKO_opt ko = Some obj) \<and> ps_clear x (objBitsKO ko) xa) proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<exists>ko. ksPSpace xa x = Some ko \<and> is_aligned x (objBitsKO ko) \<and> koTypeOf ko = TCBT \<and> ps_clear x (objBitsKO ko) xa \<Longrightarrow> \<exists>ko. ksPSpace xa x = Some ko \<and> is_aligned x (objBitsKO ko) \<and> (\<exists>obj. projectKO_opt ko = Some obj) \<and> ps_clear x (objBitsKO ko) xa
 2. \<And>x xa. \<exists>ko. ksPSpace xa x = Some ko \<and> is_aligned x (objBitsKO ko) \<and> (\<exists>obj. projectKO_opt ko = Some obj) \<and> ps_clear x (objBitsKO ko) xa \<Longrightarrow> \<exists>ko. ksPSpace xa x = Some ko \<and> is_aligned x (objBitsKO ko) \<and> koTypeOf ko = TCBT \<and> ps_clear x (objBitsKO ko) xa proof (prove)
goal (2 subgoals):
 1. \<And>x xa ko. \<lbrakk>ksPSpace xa x = Some ko; is_aligned x (objBitsKO ko); koTypeOf ko = TCBT; ps_clear x (objBitsKO ko) xa\<rbrakk> \<Longrightarrow> \<exists>obj. projectKO_opt ko = Some obj
 2. \<And>x xa. \<exists>ko. ksPSpace xa x = Some ko \<and> is_aligned x (objBitsKO ko) \<and> (\<exists>obj. projectKO_opt ko = Some obj) \<and> ps_clear x (objBitsKO ko) xa \<Longrightarrow> \<exists>ko. ksPSpace xa x = Some ko \<and> is_aligned x (objBitsKO ko) \<and> koTypeOf ko = TCBT \<and> ps_clear x (objBitsKO ko) xa proof (prove)
goal (9 subgoals):
 1. \<And>x xa ko x1. \<lbrakk>ksPSpace xa x = Some ko; is_aligned x (objBitsKO ko); koTypeOf ko = TCBT; ps_clear x (objBitsKO ko) xa; ko = KOEndpoint x1\<rbrakk> \<Longrightarrow> \<exists>obj. projectKO_opt ko = Some obj
 2. \<And>x xa ko x2. \<lbrakk>ksPSpace xa x = Some ko; is_aligned x (objBitsKO ko); koTypeOf ko = TCBT; ps_clear x (objBitsKO ko) xa; ko = KONotification x2\<rbrakk> \<Longrightarrow> \<exists>obj. projectKO_opt ko = Some obj
 3. \<And>x xa ko. \<lbrakk>ksPSpace xa x = Some ko; is_aligned x (objBitsKO ko); koTypeOf ko = TCBT; ps_clear x (objBitsKO ko) xa; ko = KOKernelData\<rbrakk> \<Longrightarrow> \<exists>obj. projectKO_opt ko = Some obj
 4. \<And>x xa ko. \<lbrakk>ksPSpace xa x = Some ko; is_aligned x (objBitsKO ko); koTypeOf ko = TCBT; ps_clear x (objBitsKO ko) xa; ko = KOUserData\<rbrakk> \<Longrightarrow> \<exists>obj. projectKO_opt ko = Some obj
 5. \<And>x xa ko. \<lbrakk>ksPSpace xa x = Some ko; is_aligned x (objBitsKO ko); koTypeOf ko = TCBT; ps_clear x (objBitsKO ko) xa; ko = KOUserDataDevice\<rbrakk> \<Longrightarrow> \<exists>obj. projectKO_opt ko = Some obj
 6. \<And>x xa ko x6. \<lbrakk>ksPSpace xa x = Some ko; is_aligned x (objBitsKO ko); koTypeOf ko = TCBT; ps_clear x (objBitsKO ko) xa; ko = KOTCB x6\<rbrakk> \<Longrightarrow> \<exists>obj. projectKO_opt ko = Some obj
 7. \<And>x xa ko x7. \<lbrakk>ksPSpace xa x = Some ko; is_aligned x (objBitsKO ko); koTypeOf ko = TCBT; ps_clear x (objBitsKO ko) xa; ko = KOCTE x7\<rbrakk> \<Longrightarrow> \<exists>obj. projectKO_opt ko = Some obj
 8. \<And>x xa ko x8. \<lbrakk>ksPSpace xa x = Some ko; is_aligned x (objBitsKO ko); koTypeOf ko = TCBT; ps_clear x (objBitsKO ko) xa; ko = KOArch x8\<rbrakk> \<Longrightarrow> \<exists>obj. projectKO_opt ko = Some obj
 9. \<And>x xa. \<exists>ko. ksPSpace xa x = Some ko \<and> is_aligned x (objBitsKO ko) \<and> (\<exists>obj. projectKO_opt ko = Some obj) \<and> ps_clear x (objBitsKO ko) xa \<Longrightarrow> \<exists>ko. ksPSpace xa x = Some ko \<and> is_aligned x (objBitsKO ko) \<and> koTypeOf ko = TCBT \<and> ps_clear x (objBitsKO ko) xa proof (prove)
goal (1 subgoal):
 1. \<And>x xa ko obj. \<lbrakk>ksPSpace xa x = Some ko; is_aligned x (objBitsKO ko); ps_clear x (objBitsKO ko) xa; (case ko of KOTCB e \<Rightarrow> Some e | _ \<Rightarrow> None) = Some obj\<rbrakk> \<Longrightarrow> koTypeOf ko = TCBT proof (prove)
goal (8 subgoals):
 1. \<And>x xa ko obj x1. \<lbrakk>ksPSpace xa x = Some ko; is_aligned x (objBitsKO ko); ps_clear x (objBitsKO ko) xa; (case ko of KOTCB e \<Rightarrow> Some e | _ \<Rightarrow> None) = Some obj; ko = KOEndpoint x1\<rbrakk> \<Longrightarrow> koTypeOf ko = TCBT
 2. \<And>x xa ko obj x2. \<lbrakk>ksPSpace xa x = Some ko; is_aligned x (objBitsKO ko); ps_clear x (objBitsKO ko) xa; (case ko of KOTCB e \<Rightarrow> Some e | _ \<Rightarrow> None) = Some obj; ko = KONotification x2\<rbrakk> \<Longrightarrow> koTypeOf ko = TCBT
 3. \<And>x xa ko obj. \<lbrakk>ksPSpace xa x = Some ko; is_aligned x (objBitsKO ko); ps_clear x (objBitsKO ko) xa; (case ko of KOTCB e \<Rightarrow> Some e | _ \<Rightarrow> None) = Some obj; ko = KOKernelData\<rbrakk> \<Longrightarrow> koTypeOf ko = TCBT
 4. \<And>x xa ko obj. \<lbrakk>ksPSpace xa x = Some ko; is_aligned x (objBitsKO ko); ps_clear x (objBitsKO ko) xa; (case ko of KOTCB e \<Rightarrow> Some e | _ \<Rightarrow> None) = Some obj; ko = KOUserData\<rbrakk> \<Longrightarrow> koTypeOf ko = TCBT
 5. \<And>x xa ko obj. \<lbrakk>ksPSpace xa x = Some ko; is_aligned x (objBitsKO ko); ps_clear x (objBitsKO ko) xa; (case ko of KOTCB e \<Rightarrow> Some e | _ \<Rightarrow> None) = Some obj; ko = KOUserDataDevice\<rbrakk> \<Longrightarrow> koTypeOf ko = TCBT
 6. \<And>x xa ko obj x6. \<lbrakk>ksPSpace xa x = Some ko; is_aligned x (objBitsKO ko); ps_clear x (objBitsKO ko) xa; (case ko of KOTCB e \<Rightarrow> Some e | _ \<Rightarrow> None) = Some obj; ko = KOTCB x6\<rbrakk> \<Longrightarrow> koTypeOf ko = TCBT
 7. \<And>x xa ko obj x7. \<lbrakk>ksPSpace xa x = Some ko; is_aligned x (objBitsKO ko); ps_clear x (objBitsKO ko) xa; (case ko of KOTCB e \<Rightarrow> Some e | _ \<Rightarrow> None) = Some obj; ko = KOCTE x7\<rbrakk> \<Longrightarrow> koTypeOf ko = TCBT
 8. \<And>x xa ko obj x8. \<lbrakk>ksPSpace xa x = Some ko; is_aligned x (objBitsKO ko); ps_clear x (objBitsKO ko) xa; (case ko of KOTCB e \<Rightarrow> Some e | _ \<Rightarrow> None) = Some obj; ko = KOArch x8\<rbrakk> \<Longrightarrow> koTypeOf ko = TCBT proof (prove)
goal:
No subgoals!