theory DetSchedAux_AI

lemma valid_blocked_fold_update: "valid_blocked_2 queues kh sa ct \<Longrightarrow> type \<noteq> apiobject_type.Untyped \<Longrightarrow> valid_blocked_2
          queues
          (foldr (\<lambda>p kh. kh(p \<mapsto> default_object type dev o_bits))
            ptrs
            kh) sa ct" apply (induct ptrs) apply simp apply (case_tac type) apply simp apply (clarsimp,
             clarsimp simp: valid_blocked_def st_tcb_at_kh_def obj_at_kh_def obj_at_def
                            default_object_def default_tcb_def)+ done

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