theory Retype_AI

lemma caps_of_state_foldr:
  assumes tyun: "ty \<noteq> Untyped"
  fixes s sz ptr us addrs dev
  defines "s' \<equiv> (s\<lparr>kheap := foldr (\<lambda>p ps. ps(p \<mapsto> default_object ty dev us))
                  addrs (kheap s)\<rparr>)"
  shows
  "caps_of_state s' =
  (\<lambda>(oref,cref). if oref \<in> set addrs
                 then (case ty of Structures_A.CapTableObject \<Rightarrow> empty_cnode us
                               | Structures_A.TCBObject \<Rightarrow> option_map (\<lambda>x. cap.NullCap) \<circ> tcb_cap_cases
                               | _ \<Rightarrow> Map.empty) cref
                 else caps_of_state s (oref,cref))" apply (rule ext)+ apply (case_tac x) apply (rename_tac oref cref) apply (simp add: caps_of_state_cte_wp_at split del: if_split) apply (case_tac "\<exists>cap. cte_wp_at ((=) cap) (oref, cref) s'") apply clarsimp apply (simp add: s'_def cte_wp_at_cases) apply (erule disjE) apply (clarsimp simp add: foldr_upd_app_if default_object_def caps_of_state_cte_wp_at
                     cte_wp_at_cases tyun empty_cnode_def
           split: if_split_asm Structures_A.apiobject_type.splits) apply (clarsimp simp add: foldr_upd_app_if default_object_def caps_of_state_cte_wp_at
                             cte_wp_at_cases tyun empty_cnode_def default_tcb_def
          split: if_split_asm Structures_A.apiobject_type.splits) apply (clarsimp simp: tcb_cap_cases_def split: if_split_asm) apply simp apply (simp add: cte_wp_at_cases s'_def foldr_upd_app_if) apply (rule conjI) apply (clarsimp simp: default_object_def wf_empty_bits
                  split: Structures_A.apiobject_type.split_asm) apply (fastforce simp: tcb_cap_cases_def split: if_split_asm) apply clarsimp apply (simp add: caps_of_state_cte_wp_at) apply (simp add: cte_wp_at_cases) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. caps_of_state s' = (\<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)) proof (prove)
goal (1 subgoal):
 1. \<And>x. caps_of_state s' x = (case x of (oref, cref) \<Rightarrow> 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)) proof (prove)
goal (1 subgoal):
 1. \<And>x a b. x = (a, b) \<Longrightarrow> caps_of_state s' x = (case x of (oref, cref) \<Rightarrow> 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)) proof (prove)
goal (1 subgoal):
 1. \<And>x oref cref. x = (oref, cref) \<Longrightarrow> caps_of_state s' x = (case x of (oref, cref) \<Rightarrow> 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)) proof (prove)
goal (1 subgoal):
 1. \<And>x oref cref. x = (oref, cref) \<Longrightarrow> (if \<exists>cap. cte_wp_at ((=) cap) (oref, cref) s' then Some (THE cap. cte_wp_at ((=) cap) (oref, cref) s') else None) = (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)) proof (prove)
goal (2 subgoals):
 1. \<And>x oref cref. \<lbrakk>x = (oref, cref); \<exists>cap. cte_wp_at ((=) cap) (oref, cref) s'\<rbrakk> \<Longrightarrow> (if \<exists>cap. cte_wp_at ((=) cap) (oref, cref) s' then Some (THE cap. cte_wp_at ((=) cap) (oref, cref) s') else None) = (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))
 2. \<And>x oref cref. \<lbrakk>x = (oref, cref); \<nexists>cap. cte_wp_at ((=) cap) (oref, cref) s'\<rbrakk> \<Longrightarrow> (if \<exists>cap. cte_wp_at ((=) cap) (oref, cref) s' then Some (THE cap. cte_wp_at ((=) cap) (oref, cref) s') else None) = (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)) proof (prove)
goal (2 subgoals):
 1. \<And>oref cref cap. cte_wp_at ((=) cap) (oref, cref) s' \<Longrightarrow> (oref \<in> set addrs \<longrightarrow> Some (THE cap. cte_wp_at ((=) cap) (oref, cref) s') = (case ty of TCBObject \<Rightarrow> map_option (\<lambda>x. NullCap) \<circ> tcb_cap_cases | CapTableObject \<Rightarrow> empty_cnode us | _ \<Rightarrow> \<lambda>x. None) cref) \<and> (oref \<notin> set addrs \<longrightarrow> Some (THE cap. cte_wp_at ((=) cap) (oref, cref) s') = caps_of_state s (oref, cref))
 2. \<And>x oref cref. \<lbrakk>x = (oref, cref); \<nexists>cap. cte_wp_at ((=) cap) (oref, cref) s'\<rbrakk> \<Longrightarrow> (if \<exists>cap. cte_wp_at ((=) cap) (oref, cref) s' then Some (THE cap. cte_wp_at ((=) cap) (oref, cref) s') else None) = (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)) proof (prove)
goal (2 subgoals):
 1. \<And>oref cref cap. (\<exists>sz fun. foldr (\<lambda>p ps. ps(p \<mapsto> default_object ty dev us)) addrs (kheap s) oref = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> fun cref = Some cap) \<or> (\<exists>tcb. foldr (\<lambda>p ps. ps(p \<mapsto> default_object ty dev us)) addrs (kheap s) oref = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases cref = Some (get, set, restr)) \<and> cap = get tcb)) \<Longrightarrow> (oref \<in> set addrs \<longrightarrow> Some (THE cap. (\<exists>sz fun. foldr (\<lambda>p ps. ps(p \<mapsto> default_object ty dev us)) addrs (kheap s) oref = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> fun cref = Some cap) \<or> (\<exists>tcb. foldr (\<lambda>p ps. ps(p \<mapsto> default_object ty dev us)) addrs (kheap s) oref = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases cref = Some (get, set, restr)) \<and> cap = get tcb))) = (case ty of TCBObject \<Rightarrow> map_option (\<lambda>x. NullCap) \<circ> tcb_cap_cases | CapTableObject \<Rightarrow> empty_cnode us | _ \<Rightarrow> \<lambda>x. None) cref) \<and> (oref \<notin> set addrs \<longrightarrow> Some (THE cap. (\<exists>sz fun. foldr (\<lambda>p ps. ps(p \<mapsto> default_object ty dev us)) addrs (kheap s) oref = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> fun cref = Some cap) \<or> (\<exists>tcb. foldr (\<lambda>p ps. ps(p \<mapsto> default_object ty dev us)) addrs (kheap s) oref = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases cref = Some (get, set, restr)) \<and> cap = get tcb))) = caps_of_state s (oref, cref))
 2. \<And>x oref cref. \<lbrakk>x = (oref, cref); \<nexists>cap. cte_wp_at ((=) cap) (oref, cref) s'\<rbrakk> \<Longrightarrow> (if \<exists>cap. cte_wp_at ((=) cap) (oref, cref) s' then Some (THE cap. cte_wp_at ((=) cap) (oref, cref) s') else None) = (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)) proof (prove)
goal (3 subgoals):
 1. \<And>oref cref cap. \<exists>sz fun. foldr (\<lambda>p ps. ps(p \<mapsto> default_object ty dev us)) addrs (kheap s) oref = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> fun cref = Some cap \<Longrightarrow> (oref \<in> set addrs \<longrightarrow> Some (THE cap. (\<exists>sz fun. foldr (\<lambda>p ps. ps(p \<mapsto> default_object ty dev us)) addrs (kheap s) oref = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> fun cref = Some cap) \<or> (\<exists>tcb. foldr (\<lambda>p ps. ps(p \<mapsto> default_object ty dev us)) addrs (kheap s) oref = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases cref = Some (get, set, restr)) \<and> cap = get tcb))) = (case ty of TCBObject \<Rightarrow> map_option (\<lambda>x. NullCap) \<circ> tcb_cap_cases | CapTableObject \<Rightarrow> empty_cnode us | _ \<Rightarrow> \<lambda>x. None) cref) \<and> (oref \<notin> set addrs \<longrightarrow> Some (THE cap. (\<exists>sz fun. foldr (\<lambda>p ps. ps(p \<mapsto> default_object ty dev us)) addrs (kheap s) oref = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> fun cref = Some cap) \<or> (\<exists>tcb. foldr (\<lambda>p ps. ps(p \<mapsto> default_object ty dev us)) addrs (kheap s) oref = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases cref = Some (get, set, restr)) \<and> cap = get tcb))) = caps_of_state s (oref, cref))
 2. \<And>oref cref cap. \<exists>tcb. foldr (\<lambda>p ps. ps(p \<mapsto> default_object ty dev us)) addrs (kheap s) oref = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases cref = Some (get, set, restr)) \<and> cap = get tcb) \<Longrightarrow> (oref \<in> set addrs \<longrightarrow> Some (THE cap. (\<exists>sz fun. foldr (\<lambda>p ps. ps(p \<mapsto> default_object ty dev us)) addrs (kheap s) oref = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> fun cref = Some cap) \<or> (\<exists>tcb. foldr (\<lambda>p ps. ps(p \<mapsto> default_object ty dev us)) addrs (kheap s) oref = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases cref = Some (get, set, restr)) \<and> cap = get tcb))) = (case ty of TCBObject \<Rightarrow> map_option (\<lambda>x. NullCap) \<circ> tcb_cap_cases | CapTableObject \<Rightarrow> empty_cnode us | _ \<Rightarrow> \<lambda>x. None) cref) \<and> (oref \<notin> set addrs \<longrightarrow> Some (THE cap. (\<exists>sz fun. foldr (\<lambda>p ps. ps(p \<mapsto> default_object ty dev us)) addrs (kheap s) oref = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> fun cref = Some cap) \<or> (\<exists>tcb. foldr (\<lambda>p ps. ps(p \<mapsto> default_object ty dev us)) addrs (kheap s) oref = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases cref = Some (get, set, restr)) \<and> cap = get tcb))) = caps_of_state s (oref, cref))
 3. \<And>x oref cref. \<lbrakk>x = (oref, cref); \<nexists>cap. cte_wp_at ((=) cap) (oref, cref) s'\<rbrakk> \<Longrightarrow> (if \<exists>cap. cte_wp_at ((=) cap) (oref, cref) s' then Some (THE cap. cte_wp_at ((=) cap) (oref, cref) s') else None) = (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)) proof (prove)
goal (2 subgoals):
 1. \<And>oref cref cap. \<exists>tcb. foldr (\<lambda>p ps. ps(p \<mapsto> default_object ty dev us)) addrs (kheap s) oref = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases cref = Some (get, set, restr)) \<and> cap = get tcb) \<Longrightarrow> (oref \<in> set addrs \<longrightarrow> Some (THE cap. (\<exists>sz fun. foldr (\<lambda>p ps. ps(p \<mapsto> default_object ty dev us)) addrs (kheap s) oref = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> fun cref = Some cap) \<or> (\<exists>tcb. foldr (\<lambda>p ps. ps(p \<mapsto> default_object ty dev us)) addrs (kheap s) oref = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases cref = Some (get, set, restr)) \<and> cap = get tcb))) = (case ty of TCBObject \<Rightarrow> map_option (\<lambda>x. NullCap) \<circ> tcb_cap_cases | CapTableObject \<Rightarrow> empty_cnode us | _ \<Rightarrow> \<lambda>x. None) cref) \<and> (oref \<notin> set addrs \<longrightarrow> Some (THE cap. (\<exists>sz fun. foldr (\<lambda>p ps. ps(p \<mapsto> default_object ty dev us)) addrs (kheap s) oref = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> fun cref = Some cap) \<or> (\<exists>tcb. foldr (\<lambda>p ps. ps(p \<mapsto> default_object ty dev us)) addrs (kheap s) oref = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases cref = Some (get, set, restr)) \<and> cap = get tcb))) = caps_of_state s (oref, cref))
 2. \<And>x oref cref. \<lbrakk>x = (oref, cref); \<nexists>cap. cte_wp_at ((=) cap) (oref, cref) s'\<rbrakk> \<Longrightarrow> (if \<exists>cap. cte_wp_at ((=) cap) (oref, cref) s' then Some (THE cap. cte_wp_at ((=) cap) (oref, cref) s') else None) = (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)) proof (prove)
goal (2 subgoals):
 1. \<And>oref cref get seta restr. \<lbrakk>oref \<in> set addrs; ty = TCBObject; tcb_cap_cases cref = Some (get, seta, restr)\<rbrakk> \<Longrightarrow> ((\<exists>cap. (\<exists>sz fun. kheap s oref = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> fun cref = Some cap) \<or> (\<exists>tcb. kheap s oref = Some (TCB tcb) \<and> cap = get tcb)) \<longrightarrow> get \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = Inactive, tcb_fault_handler = [False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False], tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = minBound, tcb_arch = default_arch_tcb\<rparr> = NullCap) \<and> ((\<forall>cap. (\<forall>sz fun. well_formed_cnode_n sz fun \<longrightarrow> kheap s oref = Some (CNode sz fun) \<longrightarrow> fun cref \<noteq> Some cap) \<and> (\<forall>tcb. kheap s oref = Some (TCB tcb) \<longrightarrow> cap \<noteq> get tcb)) \<longrightarrow> get \<lparr>tcb_ctable = NullCap, tcb_vtable = NullCap, tcb_reply = NullCap, tcb_caller = NullCap, tcb_ipcframe = NullCap, tcb_state = Inactive, tcb_fault_handler = [False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False], tcb_ipc_buffer = 0, tcb_fault = None, tcb_bound_notification = None, tcb_mcpriority = minBound, tcb_arch = default_arch_tcb\<rparr> = NullCap)
 2. \<And>x oref cref. \<lbrakk>x = (oref, cref); \<nexists>cap. cte_wp_at ((=) cap) (oref, cref) s'\<rbrakk> \<Longrightarrow> (if \<exists>cap. cte_wp_at ((=) cap) (oref, cref) s' then Some (THE cap. cte_wp_at ((=) cap) (oref, cref) s') else None) = (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)) proof (prove)
goal (1 subgoal):
 1. \<And>x oref cref. \<lbrakk>x = (oref, cref); \<nexists>cap. cte_wp_at ((=) cap) (oref, cref) s'\<rbrakk> \<Longrightarrow> (if \<exists>cap. cte_wp_at ((=) cap) (oref, cref) s' then Some (THE cap. cte_wp_at ((=) cap) (oref, cref) s') else None) = (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)) proof (prove)
goal (1 subgoal):
 1. \<And>x oref cref. \<lbrakk>x = (oref, cref); \<forall>cap. \<not> cte_wp_at ((=) cap) (oref, cref) s'\<rbrakk> \<Longrightarrow> (oref \<in> set addrs \<longrightarrow> None = (case ty of TCBObject \<Rightarrow> map_option (\<lambda>x. NullCap) \<circ> tcb_cap_cases | CapTableObject \<Rightarrow> empty_cnode us | _ \<Rightarrow> \<lambda>x. None) cref) \<and> (oref \<notin> set addrs \<longrightarrow> None = caps_of_state s (oref, cref)) proof (prove)
goal (1 subgoal):
 1. \<And>x oref cref. \<lbrakk>x = (oref, cref); \<forall>cap. (\<forall>sz fun. well_formed_cnode_n sz fun \<longrightarrow> (if oref \<in> set addrs then Some (default_object ty dev us) else kheap s oref) = Some (CNode sz fun) \<longrightarrow> fun cref \<noteq> Some cap) \<and> (\<forall>tcb. (if oref \<in> set addrs then Some (default_object ty dev us) else kheap s oref) = Some (TCB tcb) \<longrightarrow> (\<forall>get. (\<forall>set restr. tcb_cap_cases cref \<noteq> Some (get, set, restr)) \<or> cap \<noteq> get tcb))\<rbrakk> \<Longrightarrow> (oref \<in> set addrs \<longrightarrow> None = (case ty of TCBObject \<Rightarrow> map_option (\<lambda>x. NullCap) \<circ> tcb_cap_cases | CapTableObject \<Rightarrow> empty_cnode us | _ \<Rightarrow> \<lambda>x. None) cref) \<and> (oref \<notin> set addrs \<longrightarrow> None = caps_of_state s (oref, cref)) proof (prove)
goal (2 subgoals):
 1. \<And>x oref cref. \<lbrakk>x = (oref, cref); \<forall>cap. (\<forall>sz fun. well_formed_cnode_n sz fun \<longrightarrow> (if oref \<in> set addrs then Some (default_object ty dev us) else kheap s oref) = Some (CNode sz fun) \<longrightarrow> fun cref \<noteq> Some cap) \<and> (\<forall>tcb. (if oref \<in> set addrs then Some (default_object ty dev us) else kheap s oref) = Some (TCB tcb) \<longrightarrow> (\<forall>get. (\<forall>set restr. tcb_cap_cases cref \<noteq> Some (get, set, restr)) \<or> cap \<noteq> get tcb))\<rbrakk> \<Longrightarrow> oref \<in> set addrs \<longrightarrow> None = (case ty of TCBObject \<Rightarrow> map_option (\<lambda>x. NullCap) \<circ> tcb_cap_cases | CapTableObject \<Rightarrow> empty_cnode us | _ \<Rightarrow> \<lambda>x. None) cref
 2. \<And>x oref cref. \<lbrakk>x = (oref, cref); \<forall>cap. (\<forall>sz fun. well_formed_cnode_n sz fun \<longrightarrow> (if oref \<in> set addrs then Some (default_object ty dev us) else kheap s oref) = Some (CNode sz fun) \<longrightarrow> fun cref \<noteq> Some cap) \<and> (\<forall>tcb. (if oref \<in> set addrs then Some (default_object ty dev us) else kheap s oref) = Some (TCB tcb) \<longrightarrow> (\<forall>get. (\<forall>set restr. tcb_cap_cases cref \<noteq> Some (get, set, restr)) \<or> cap \<noteq> get tcb))\<rbrakk> \<Longrightarrow> oref \<notin> set addrs \<longrightarrow> None = caps_of_state s (oref, cref) proof (prove)
goal (2 subgoals):
 1. \<And>oref cref. \<lbrakk>oref \<in> set addrs; ty = TCBObject; \<forall>cap get. (\<forall>set restr. tcb_cap_cases cref \<noteq> Some (get, set, restr)) \<or> cap \<noteq> get default_tcb\<rbrakk> \<Longrightarrow> tcb_cap_cases cref = None
 2. \<And>x oref cref. \<lbrakk>x = (oref, cref); \<forall>cap. (\<forall>sz fun. well_formed_cnode_n sz fun \<longrightarrow> (if oref \<in> set addrs then Some (default_object ty dev us) else kheap s oref) = Some (CNode sz fun) \<longrightarrow> fun cref \<noteq> Some cap) \<and> (\<forall>tcb. (if oref \<in> set addrs then Some (default_object ty dev us) else kheap s oref) = Some (TCB tcb) \<longrightarrow> (\<forall>get. (\<forall>set restr. tcb_cap_cases cref \<noteq> Some (get, set, restr)) \<or> cap \<noteq> get tcb))\<rbrakk> \<Longrightarrow> oref \<notin> set addrs \<longrightarrow> None = caps_of_state s (oref, cref) proof (prove)
goal (1 subgoal):
 1. \<And>x oref cref. \<lbrakk>x = (oref, cref); \<forall>cap. (\<forall>sz fun. well_formed_cnode_n sz fun \<longrightarrow> (if oref \<in> set addrs then Some (default_object ty dev us) else kheap s oref) = Some (CNode sz fun) \<longrightarrow> fun cref \<noteq> Some cap) \<and> (\<forall>tcb. (if oref \<in> set addrs then Some (default_object ty dev us) else kheap s oref) = Some (TCB tcb) \<longrightarrow> (\<forall>get. (\<forall>set restr. tcb_cap_cases cref \<noteq> Some (get, set, restr)) \<or> cap \<noteq> get tcb))\<rbrakk> \<Longrightarrow> oref \<notin> set addrs \<longrightarrow> None = caps_of_state s (oref, cref) proof (prove)
goal (1 subgoal):
 1. \<And>oref cref. \<lbrakk>\<forall>cap. (\<forall>sz fun. well_formed_cnode_n sz fun \<longrightarrow> kheap s oref = Some (CNode sz fun) \<longrightarrow> fun cref \<noteq> Some cap) \<and> (\<forall>tcb. kheap s oref = Some (TCB tcb) \<longrightarrow> (\<forall>get. (\<forall>set restr. tcb_cap_cases cref \<noteq> Some (get, set, restr)) \<or> cap \<noteq> get tcb)); oref \<notin> set addrs\<rbrakk> \<Longrightarrow> None = caps_of_state s (oref, cref) proof (prove)
goal (1 subgoal):
 1. \<And>oref cref. \<lbrakk>\<forall>cap. (\<forall>sz fun. well_formed_cnode_n sz fun \<longrightarrow> kheap s oref = Some (CNode sz fun) \<longrightarrow> fun cref \<noteq> Some cap) \<and> (\<forall>tcb. kheap s oref = Some (TCB tcb) \<longrightarrow> (\<forall>get. (\<forall>set restr. tcb_cap_cases cref \<noteq> Some (get, set, restr)) \<or> cap \<noteq> get tcb)); oref \<notin> set addrs\<rbrakk> \<Longrightarrow> \<forall>cap. \<not> cte_wp_at ((=) cap) (oref, cref) s proof (prove)
goal:
No subgoals!