theory Retype_AI

lemma null_filter_caps_of_state_foldr:
  fixes s sz ptr us addrs dev
  assumes tyun: "ty \<noteq> Untyped"
    and nondom: "\<forall>x \<in> set addrs. x \<notin> dom (kheap s)"
  defines "s' \<equiv> (s\<lparr>kheap := foldr (\<lambda>p ps. ps(p \<mapsto> default_object ty dev us))
                  addrs (kheap s)\<rparr>)"
  shows
  "null_filter (caps_of_state s') =
   null_filter (caps_of_state s)" unfolding s'_def apply (subst caps_of_state_foldr[OF tyun]) apply (rule ext) apply (clarsimp simp add: null_filter_def split_def empty_cnode_def
                     split: Structures_A.apiobject_type.splits) apply (subgoal_tac "a \<in> set addrs \<longrightarrow> caps_of_state s (a, b) \<noteq> Some cap.NullCap
           \<longrightarrow> None = caps_of_state s (a, b)", simp) apply clarsimp apply (subgoal_tac "tcb_cap_cases b = None", simp) apply (rule ccontr, clarsimp) apply clarsimp apply (rule sym, rule ccontr, clarsimp) apply (drule bspec[OF nondom]) apply (drule caps_of_state_cteD) apply (erule cte_wp_atE, fastforce+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. null_filter (caps_of_state s') = null_filter (caps_of_state s) proof (prove)
goal (1 subgoal):
 1. null_filter (caps_of_state (s\<lparr>kheap := foldr (\<lambda>p ps. ps(p \<mapsto> default_object ty dev us)) addrs (kheap s)\<rparr>)) = null_filter (caps_of_state s) proof (prove)
goal (1 subgoal):
 1. null_filter (\<lambda>(oref, cref). if oref \<in> set addrs then (case ty of TCBObject \<Rightarrow> map_option (\<lambda>x. NullCap) \<circ> tcb_cap_cases | CapTableObject \<Rightarrow> empty_cnode us | _ \<Rightarrow> \<lambda>x. None) cref else caps_of_state s (oref, cref)) = null_filter (caps_of_state s) proof (prove)
goal (1 subgoal):
 1. \<And>x. null_filter (\<lambda>(oref, cref). if oref \<in> set addrs then (case ty of TCBObject \<Rightarrow> map_option (\<lambda>x. NullCap) \<circ> tcb_cap_cases | CapTableObject \<Rightarrow> empty_cnode us | _ \<Rightarrow> \<lambda>x. None) cref else caps_of_state s (oref, cref)) x = null_filter (caps_of_state s) x proof (prove)
goal (1 subgoal):
 1. \<And>a b. (ty = Untyped \<longrightarrow> a \<in> set addrs \<longrightarrow> caps_of_state s (a, b) \<noteq> Some NullCap \<longrightarrow> None = caps_of_state s (a, b)) \<and> (ty = TCBObject \<longrightarrow> a \<in> set addrs \<longrightarrow> ((\<exists>a aa ba. tcb_cap_cases b = Some (a, aa, ba)) \<longrightarrow> caps_of_state s (a, b) \<noteq> Some NullCap \<longrightarrow> None = caps_of_state s (a, b)) \<and> ((\<forall>a aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<longrightarrow> (caps_of_state s (a, b) = Some NullCap \<longrightarrow> tcb_cap_cases b = None) \<and> (caps_of_state s (a, b) \<noteq> Some NullCap \<longrightarrow> map_option (\<lambda>x. NullCap) (tcb_cap_cases b) = caps_of_state s (a, b)))) \<and> (ty = EndpointObject \<longrightarrow> a \<in> set addrs \<longrightarrow> caps_of_state s (a, b) \<noteq> Some NullCap \<longrightarrow> None = caps_of_state s (a, b)) \<and> (ty = NotificationObject \<longrightarrow> a \<in> set addrs \<longrightarrow> caps_of_state s (a, b) \<noteq> Some NullCap \<longrightarrow> None = caps_of_state s (a, b)) \<and> (ty = CapTableObject \<longrightarrow> a \<in> set addrs \<longrightarrow> caps_of_state s (a, b) \<noteq> Some NullCap \<longrightarrow> None = caps_of_state s (a, b)) \<and> ((\<exists>x6. ty = ArchObject x6) \<longrightarrow> a \<in> set addrs \<longrightarrow> caps_of_state s (a, b) \<noteq> Some NullCap \<longrightarrow> None = caps_of_state s (a, b)) proof (prove)
goal (2 subgoals):
 1. \<And>a b. a \<in> set addrs \<longrightarrow> caps_of_state s (a, b) \<noteq> Some NullCap \<longrightarrow> None = caps_of_state s (a, b) \<Longrightarrow> ty = TCBObject \<longrightarrow> a \<in> set addrs \<longrightarrow> (\<forall>a aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba)) \<longrightarrow> (caps_of_state s (a, b) = Some NullCap \<longrightarrow> tcb_cap_cases b = None) \<and> (caps_of_state s (a, b) \<noteq> Some NullCap \<longrightarrow> map_option (\<lambda>x. NullCap) (tcb_cap_cases b) = caps_of_state s (a, b))
 2. \<And>a b. a \<in> set addrs \<longrightarrow> caps_of_state s (a, b) \<noteq> Some NullCap \<longrightarrow> None = caps_of_state s (a, b) proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>ty = TCBObject; a \<in> set addrs; \<forall>a aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba); caps_of_state s (a, b) \<noteq> Some NullCap \<longrightarrow> None = caps_of_state s (a, b)\<rbrakk> \<Longrightarrow> (caps_of_state s (a, b) = Some NullCap \<longrightarrow> tcb_cap_cases b = None) \<and> (caps_of_state s (a, b) \<noteq> Some NullCap \<longrightarrow> map_option (\<lambda>x. NullCap) (tcb_cap_cases b) = caps_of_state s (a, b))
 2. \<And>a b. a \<in> set addrs \<longrightarrow> caps_of_state s (a, b) \<noteq> Some NullCap \<longrightarrow> None = caps_of_state s (a, b) proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>ty = TCBObject; a \<in> set addrs; \<forall>a aa ba. tcb_cap_cases b \<noteq> Some (a, aa, ba); caps_of_state s (a, b) \<noteq> Some NullCap \<longrightarrow> None = caps_of_state s (a, b)\<rbrakk> \<Longrightarrow> tcb_cap_cases b = None
 2. \<And>a b. a \<in> set addrs \<longrightarrow> caps_of_state s (a, b) \<noteq> Some NullCap \<longrightarrow> None = caps_of_state s (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>a b. a \<in> set addrs \<longrightarrow> caps_of_state s (a, b) \<noteq> Some NullCap \<longrightarrow> None = caps_of_state s (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<in> set addrs; caps_of_state s (a, b) \<noteq> Some NullCap\<rbrakk> \<Longrightarrow> None = caps_of_state s (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>a b y. \<lbrakk>a \<in> set addrs; y \<noteq> NullCap; caps_of_state s (a, b) = Some y\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b y. \<lbrakk>y \<noteq> NullCap; caps_of_state s (a, b) = Some y; a \<notin> dom (kheap s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b y. \<lbrakk>y \<noteq> NullCap; a \<notin> dom (kheap s); cte_wp_at ((=) y) (a, b) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!