theory DetSchedAux_AI

lemma valid_etcb_fold_update: "valid_etcbs_2 ekh kh \<Longrightarrow> type \<noteq> apiobject_type.Untyped \<Longrightarrow> valid_etcbs_2
          (foldr (\<lambda>p ekh. ekh(p := default_ext type cdom))
            ptrs
            ekh)
          (foldr (\<lambda>p kh. kh(p \<mapsto> default_object type dev o_bits))
            ptrs
            kh)" apply (induct ptrs) apply simp apply (case_tac type) apply (clarsimp simp add: valid_etcbs_def st_tcb_at_kh_def obj_at_kh_def obj_at_def is_etcb_at_def default_object_def default_ext_def)+ done

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