theory KHeap_DR

lemma caps_of_state_transform_opt_cap:
  "\<lbrakk> caps_of_state s p = Some cap; valid_etcbs s;
          fst p \<noteq> idle_thread s \<rbrakk>
       \<Longrightarrow> opt_cap (transform_cslot_ptr p) (transform s)
            = Some (transform_cap cap)" apply (frule caps_of_state_cteD) apply (cases p) apply (erule cte_wp_atE) apply (clarsimp simp: opt_cap_def transform_cslot_ptr_def
                         slots_of_def transform_objects_def
                         transform_def object_slots_def
                         transform_cnode_contents_def well_formed_cnode_n_def
                  split: nat.splits) apply (frule(1) eqset_imp_iff[THEN iffD1, OF _ domI]) apply (simp add: option_map_join_def nat_to_bl_dest) apply (fastforce simp: nat_to_bl_def split: nat.splits) apply (frule(1) valid_etcbs_tcb_etcb) apply (clarsimp simp: opt_cap_def transform_cslot_ptr_def slots_of_def
                        transform_def transform_objects_def object_slots_def
                        valid_irq_node_def obj_at_def is_cap_table_def
                        transform_tcb_def tcb_slots tcb_cap_cases_def
                        bl_to_bin_tcb_cnode_index bl_to_bin_tcb_cnode_index_le0
                 split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s p = Some cap; valid_etcbs s; fst p \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> opt_cap (transform_cslot_ptr p) (transform s) = Some (transform_cap cap) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s p = Some cap; valid_etcbs s; fst p \<noteq> idle_thread s; cte_wp_at ((=) cap) p s\<rbrakk> \<Longrightarrow> opt_cap (transform_cslot_ptr p) (transform s) = Some (transform_cap cap) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>caps_of_state s p = Some cap; valid_etcbs s; fst p \<noteq> idle_thread s; cte_wp_at ((=) cap) p s; p = (a, b)\<rbrakk> \<Longrightarrow> opt_cap (transform_cslot_ptr p) (transform s) = Some (transform_cap cap) proof (prove)
goal (2 subgoals):
 1. \<And>a b sz fun cte. \<lbrakk>caps_of_state s p = Some cap; valid_etcbs s; fst p \<noteq> idle_thread s; p = (a, b); kheap s (fst p) = Some (kernel_object.CNode sz fun); well_formed_cnode_n sz fun; fun (snd p) = Some cte; cap = cte\<rbrakk> \<Longrightarrow> opt_cap (transform_cslot_ptr p) (transform s) = Some (transform_cap cap)
 2. \<And>a b tcb getF setF restr. \<lbrakk>caps_of_state s p = Some cap; valid_etcbs s; fst p \<noteq> idle_thread s; p = (a, b); kheap s (fst p) = Some (TCB tcb); tcb_cap_cases (snd p) = Some (getF, setF, restr); cap = getF tcb\<rbrakk> \<Longrightarrow> opt_cap (transform_cslot_ptr p) (transform s) = Some (transform_cap cap) proof (prove)
goal (2 subgoals):
 1. \<And>a b sz fun. \<lbrakk>caps_of_state s (a, b) = Some cap; valid_etcbs s; a \<noteq> idle_thread s; p = (a, b); kheap s a = Some (kernel_object.CNode sz fun); dom fun = {x. length x = sz}; fun b = Some cap\<rbrakk> \<Longrightarrow> (sz = 0 \<longrightarrow> (\<exists>z. option_map_join fun (nat_to_bl 0 (nat (bl_to_bin b))) = Some z \<and> transform_cap z = transform_cap cap)) \<and> (\<forall>x2. sz = Suc x2 \<longrightarrow> (\<exists>z. option_map_join fun (nat_to_bl (Suc x2) (nat (bl_to_bin b))) = Some z \<and> transform_cap z = transform_cap cap))
 2. \<And>a b tcb getF setF restr. \<lbrakk>caps_of_state s p = Some cap; valid_etcbs s; fst p \<noteq> idle_thread s; p = (a, b); kheap s (fst p) = Some (TCB tcb); tcb_cap_cases (snd p) = Some (getF, setF, restr); cap = getF tcb\<rbrakk> \<Longrightarrow> opt_cap (transform_cslot_ptr p) (transform s) = Some (transform_cap cap) proof (prove)
goal (2 subgoals):
 1. \<And>a b sz fun. \<lbrakk>caps_of_state s (a, b) = Some cap; valid_etcbs s; a \<noteq> idle_thread s; p = (a, b); kheap s a = Some (kernel_object.CNode sz fun); dom fun = {x. length x = sz}; fun b = Some cap; b \<in> {x. length x = sz}\<rbrakk> \<Longrightarrow> (sz = 0 \<longrightarrow> (\<exists>z. option_map_join fun (nat_to_bl 0 (nat (bl_to_bin b))) = Some z \<and> transform_cap z = transform_cap cap)) \<and> (\<forall>x2. sz = Suc x2 \<longrightarrow> (\<exists>z. option_map_join fun (nat_to_bl (Suc x2) (nat (bl_to_bin b))) = Some z \<and> transform_cap z = transform_cap cap))
 2. \<And>a b tcb getF setF restr. \<lbrakk>caps_of_state s p = Some cap; valid_etcbs s; fst p \<noteq> idle_thread s; p = (a, b); kheap s (fst p) = Some (TCB tcb); tcb_cap_cases (snd p) = Some (getF, setF, restr); cap = getF tcb\<rbrakk> \<Longrightarrow> opt_cap (transform_cslot_ptr p) (transform s) = Some (transform_cap cap) proof (prove)
goal (2 subgoals):
 1. \<And>a b sz fun. \<lbrakk>caps_of_state s (a, b) = Some cap; valid_etcbs s; a \<noteq> idle_thread s; p = (a, b); kheap s a = Some (kernel_object.CNode sz fun); dom fun = {x. length x = sz}; fun b = Some cap; length b = sz\<rbrakk> \<Longrightarrow> sz = 0 \<longrightarrow> (\<exists>z. (case nat_to_bl 0 (nat (bl_to_bin b)) of None \<Rightarrow> None | Some x \<Rightarrow> fun x) = Some z \<and> transform_cap z = transform_cap cap)
 2. \<And>a b tcb getF setF restr. \<lbrakk>caps_of_state s p = Some cap; valid_etcbs s; fst p \<noteq> idle_thread s; p = (a, b); kheap s (fst p) = Some (TCB tcb); tcb_cap_cases (snd p) = Some (getF, setF, restr); cap = getF tcb\<rbrakk> \<Longrightarrow> opt_cap (transform_cslot_ptr p) (transform s) = Some (transform_cap cap) proof (prove)
goal (1 subgoal):
 1. \<And>a b tcb getF setF restr. \<lbrakk>caps_of_state s p = Some cap; valid_etcbs s; fst p \<noteq> idle_thread s; p = (a, b); kheap s (fst p) = Some (TCB tcb); tcb_cap_cases (snd p) = Some (getF, setF, restr); cap = getF tcb\<rbrakk> \<Longrightarrow> opt_cap (transform_cslot_ptr p) (transform s) = Some (transform_cap cap) proof (prove)
goal (1 subgoal):
 1. \<And>a b tcb getF setF restr. \<lbrakk>caps_of_state s p = Some cap; valid_etcbs s; fst p \<noteq> idle_thread s; p = (a, b); kheap s (fst p) = Some (TCB tcb); tcb_cap_cases (snd p) = Some (getF, setF, restr); cap = getF tcb; \<exists>etcb. ekheap s (fst p) = Some etcb\<rbrakk> \<Longrightarrow> opt_cap (transform_cslot_ptr p) (transform s) = Some (transform_cap cap) proof (prove)
goal:
No subgoals!