theory DetSchedAux_AI

lemma retype_etcb_at_helper: "\<lbrakk>etcb_at' P t ekh; valid_etcbs_2 ekh kh; d \<noteq> apiobject_type.Untyped;
        foldr (\<lambda>p kh. kh(p \<mapsto> default_object d dev c))
         ptrs
         kh t =
        Some (TCB tcb);
        tcb_state tcb \<noteq> Inactive\<rbrakk>
       \<Longrightarrow> etcb_at' P t
           ((foldr (\<lambda>p ekh. ekh(p := default_ext d cdom))
             ptrs)
             ekh)" apply (induct ptrs) apply simp apply (case_tac d) apply (clarsimp split: if_split_asm simp: default_tcb_def default_object_def default_ext_def etcb_at'_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>etcb_at' P t ekh; valid_etcbs_2 ekh kh; d \<noteq> Untyped; foldr (\<lambda>p kh. kh(p \<mapsto> default_object d dev c)) ptrs kh t = Some (TCB tcb); tcb_state tcb \<noteq> Inactive\<rbrakk> \<Longrightarrow> etcb_at' P t (foldr (\<lambda>p ekh. ekh(p := default_ext d cdom)) ptrs ekh) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>etcb_at' P t ekh; valid_etcbs_2 ekh kh; d \<noteq> Untyped; foldr (\<lambda>p kh. kh(p \<mapsto> default_object d dev c)) [] kh t = Some (TCB tcb); tcb_state tcb \<noteq> Inactive\<rbrakk> \<Longrightarrow> etcb_at' P t (foldr (\<lambda>p ekh. ekh(p := default_ext d cdom)) [] ekh)
 2. \<And>a ptrs. \<lbrakk>\<lbrakk>etcb_at' P t ekh; valid_etcbs_2 ekh kh; d \<noteq> Untyped; foldr (\<lambda>p kh. kh(p \<mapsto> default_object d dev c)) ptrs kh t = Some (TCB tcb); tcb_state tcb \<noteq> Inactive\<rbrakk> \<Longrightarrow> etcb_at' P t (foldr (\<lambda>p ekh. ekh(p := default_ext d cdom)) ptrs ekh); etcb_at' P t ekh; valid_etcbs_2 ekh kh; d \<noteq> Untyped; foldr (\<lambda>p kh. kh(p \<mapsto> default_object d dev c)) (a # ptrs) kh t = Some (TCB tcb); tcb_state tcb \<noteq> Inactive\<rbrakk> \<Longrightarrow> etcb_at' P t (foldr (\<lambda>p ekh. ekh(p := default_ext d cdom)) (a # ptrs) ekh) proof (prove)
goal (1 subgoal):
 1. \<And>a ptrs. \<lbrakk>\<lbrakk>etcb_at' P t ekh; valid_etcbs_2 ekh kh; d \<noteq> Untyped; foldr (\<lambda>p kh. kh(p \<mapsto> default_object d dev c)) ptrs kh t = Some (TCB tcb); tcb_state tcb \<noteq> Inactive\<rbrakk> \<Longrightarrow> etcb_at' P t (foldr (\<lambda>p ekh. ekh(p := default_ext d cdom)) ptrs ekh); etcb_at' P t ekh; valid_etcbs_2 ekh kh; d \<noteq> Untyped; foldr (\<lambda>p kh. kh(p \<mapsto> default_object d dev c)) (a # ptrs) kh t = Some (TCB tcb); tcb_state tcb \<noteq> Inactive\<rbrakk> \<Longrightarrow> etcb_at' P t (foldr (\<lambda>p ekh. ekh(p := default_ext d cdom)) (a # ptrs) ekh) proof (prove)
goal (6 subgoals):
 1. \<And>a ptrs. \<lbrakk>\<lbrakk>etcb_at' P t ekh; valid_etcbs_2 ekh kh; d \<noteq> Untyped; foldr (\<lambda>p kh. kh(p \<mapsto> default_object d dev c)) ptrs kh t = Some (TCB tcb); tcb_state tcb \<noteq> Inactive\<rbrakk> \<Longrightarrow> etcb_at' P t (foldr (\<lambda>p ekh. ekh(p := default_ext d cdom)) ptrs ekh); etcb_at' P t ekh; valid_etcbs_2 ekh kh; d \<noteq> Untyped; foldr (\<lambda>p kh. kh(p \<mapsto> default_object d dev c)) (a # ptrs) kh t = Some (TCB tcb); tcb_state tcb \<noteq> Inactive; d = Untyped\<rbrakk> \<Longrightarrow> etcb_at' P t (foldr (\<lambda>p ekh. ekh(p := default_ext d cdom)) (a # ptrs) ekh)
 2. \<And>a ptrs. \<lbrakk>\<lbrakk>etcb_at' P t ekh; valid_etcbs_2 ekh kh; d \<noteq> Untyped; foldr (\<lambda>p kh. kh(p \<mapsto> default_object d dev c)) ptrs kh t = Some (TCB tcb); tcb_state tcb \<noteq> Inactive\<rbrakk> \<Longrightarrow> etcb_at' P t (foldr (\<lambda>p ekh. ekh(p := default_ext d cdom)) ptrs ekh); etcb_at' P t ekh; valid_etcbs_2 ekh kh; d \<noteq> Untyped; foldr (\<lambda>p kh. kh(p \<mapsto> default_object d dev c)) (a # ptrs) kh t = Some (TCB tcb); tcb_state tcb \<noteq> Inactive; d = TCBObject\<rbrakk> \<Longrightarrow> etcb_at' P t (foldr (\<lambda>p ekh. ekh(p := default_ext d cdom)) (a # ptrs) ekh)
 3. \<And>a ptrs. \<lbrakk>\<lbrakk>etcb_at' P t ekh; valid_etcbs_2 ekh kh; d \<noteq> Untyped; foldr (\<lambda>p kh. kh(p \<mapsto> default_object d dev c)) ptrs kh t = Some (TCB tcb); tcb_state tcb \<noteq> Inactive\<rbrakk> \<Longrightarrow> etcb_at' P t (foldr (\<lambda>p ekh. ekh(p := default_ext d cdom)) ptrs ekh); etcb_at' P t ekh; valid_etcbs_2 ekh kh; d \<noteq> Untyped; foldr (\<lambda>p kh. kh(p \<mapsto> default_object d dev c)) (a # ptrs) kh t = Some (TCB tcb); tcb_state tcb \<noteq> Inactive; d = EndpointObject\<rbrakk> \<Longrightarrow> etcb_at' P t (foldr (\<lambda>p ekh. ekh(p := default_ext d cdom)) (a # ptrs) ekh)
 4. \<And>a ptrs. \<lbrakk>\<lbrakk>etcb_at' P t ekh; valid_etcbs_2 ekh kh; d \<noteq> Untyped; foldr (\<lambda>p kh. kh(p \<mapsto> default_object d dev c)) ptrs kh t = Some (TCB tcb); tcb_state tcb \<noteq> Inactive\<rbrakk> \<Longrightarrow> etcb_at' P t (foldr (\<lambda>p ekh. ekh(p := default_ext d cdom)) ptrs ekh); etcb_at' P t ekh; valid_etcbs_2 ekh kh; d \<noteq> Untyped; foldr (\<lambda>p kh. kh(p \<mapsto> default_object d dev c)) (a # ptrs) kh t = Some (TCB tcb); tcb_state tcb \<noteq> Inactive; d = NotificationObject\<rbrakk> \<Longrightarrow> etcb_at' P t (foldr (\<lambda>p ekh. ekh(p := default_ext d cdom)) (a # ptrs) ekh)
 5. \<And>a ptrs. \<lbrakk>\<lbrakk>etcb_at' P t ekh; valid_etcbs_2 ekh kh; d \<noteq> Untyped; foldr (\<lambda>p kh. kh(p \<mapsto> default_object d dev c)) ptrs kh t = Some (TCB tcb); tcb_state tcb \<noteq> Inactive\<rbrakk> \<Longrightarrow> etcb_at' P t (foldr (\<lambda>p ekh. ekh(p := default_ext d cdom)) ptrs ekh); etcb_at' P t ekh; valid_etcbs_2 ekh kh; d \<noteq> Untyped; foldr (\<lambda>p kh. kh(p \<mapsto> default_object d dev c)) (a # ptrs) kh t = Some (TCB tcb); tcb_state tcb \<noteq> Inactive; d = CapTableObject\<rbrakk> \<Longrightarrow> etcb_at' P t (foldr (\<lambda>p ekh. ekh(p := default_ext d cdom)) (a # ptrs) ekh)
 6. \<And>a ptrs x6. \<lbrakk>\<lbrakk>etcb_at' P t ekh; valid_etcbs_2 ekh kh; d \<noteq> Untyped; foldr (\<lambda>p kh. kh(p \<mapsto> default_object d dev c)) ptrs kh t = Some (TCB tcb); tcb_state tcb \<noteq> Inactive\<rbrakk> \<Longrightarrow> etcb_at' P t (foldr (\<lambda>p ekh. ekh(p := default_ext d cdom)) ptrs ekh); etcb_at' P t ekh; valid_etcbs_2 ekh kh; d \<noteq> Untyped; foldr (\<lambda>p kh. kh(p \<mapsto> default_object d dev c)) (a # ptrs) kh t = Some (TCB tcb); tcb_state tcb \<noteq> Inactive; d = ArchObject x6\<rbrakk> \<Longrightarrow> etcb_at' P t (foldr (\<lambda>p ekh. ekh(p := default_ext d cdom)) (a # ptrs) ekh) proof (prove)
goal:
No subgoals!