theory Tcb_DR

lemma update_cnode_cap_data:
  "\<lbrakk>Some af = (if w = 0 then Some ab else Some (CSpace_A.update_cap_data False w ab)); Structures_A.is_cnode_cap af\<rbrakk>
  \<Longrightarrow> transform_cap af = cdl_update_cnode_cap_data (transform_cap ab) w" apply (clarsimp simp:is_cap_simps) apply (clarsimp split:if_splits) apply (simp add:cdl_update_cnode_cap_data_def CSpace_D.update_cap_data_def) apply (clarsimp simp: update_cap_data_def arch_update_cap_data_def split:if_splits) apply ((cases ab,simp_all add:badge_update_def)+)[2] apply (clarsimp simp:is_cap_simps the_cnode_cap_def word_size split:if_split_asm simp:Let_def) apply (clarsimp simp:cdl_update_cnode_cap_data_def word_bits_def of_drop_to_bl
    word_size mask_twice dest!:leI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Some af = (if w = 0 then Some ab else Some (CSpace_A.update_cap_data False w ab)); Structures_A.is_cnode_cap af\<rbrakk> \<Longrightarrow> transform_cap af = cdl_update_cnode_cap_data (transform_cap ab) w proof (prove)
goal (1 subgoal):
 1. \<And>r bits g. \<lbrakk>Some (cap.CNodeCap r bits g) = (if w = 0 then Some ab else Some (CSpace_A.update_cap_data False w ab)); af = cap.CNodeCap r bits g\<rbrakk> \<Longrightarrow> cdl_cap.CNodeCap r (of_bl g) (length g) bits = cdl_update_cnode_cap_data (transform_cap ab) w proof (prove)
goal (2 subgoals):
 1. \<And>r bits g. \<lbrakk>af = cap.CNodeCap r bits g; w = 0; ab = cap.CNodeCap r bits g\<rbrakk> \<Longrightarrow> cdl_cap.CNodeCap r (of_bl g) (length g) bits = cdl_update_cnode_cap_data (cdl_cap.CNodeCap r (of_bl g) (length g) bits) 0
 2. \<And>r bits g. \<lbrakk>af = CSpace_A.update_cap_data False w ab; w \<noteq> 0; cap.CNodeCap r bits g = CSpace_A.update_cap_data False w ab\<rbrakk> \<Longrightarrow> cdl_cap.CNodeCap r (of_bl g) (length g) bits = cdl_update_cnode_cap_data (transform_cap ab) w proof (prove)
goal (1 subgoal):
 1. \<And>r bits g. \<lbrakk>af = CSpace_A.update_cap_data False w ab; w \<noteq> 0; cap.CNodeCap r bits g = CSpace_A.update_cap_data False w ab\<rbrakk> \<Longrightarrow> cdl_cap.CNodeCap r (of_bl g) (length g) bits = cdl_update_cnode_cap_data (transform_cap ab) w proof (prove)
goal (3 subgoals):
 1. \<And>r bits g. \<lbrakk>Structures_A.is_ep_cap ab; af = Structures_A.badge_update w ab; w \<noteq> 0; cap_ep_badge ab = 0; cap.CNodeCap r bits g = Structures_A.badge_update w ab\<rbrakk> \<Longrightarrow> cdl_cap.CNodeCap r (of_bl g) (length g) bits = cdl_update_cnode_cap_data (transform_cap ab) w
 2. \<And>r bits g. \<lbrakk>w \<noteq> 0; Structures_A.is_ntfn_cap ab; cap.CNodeCap r bits g = Structures_A.badge_update w ab; \<not> Structures_A.is_ep_cap ab; cap_ep_badge ab = 0; af = Structures_A.badge_update w ab\<rbrakk> \<Longrightarrow> cdl_cap.CNodeCap r (of_bl g) (length g) bits = cdl_update_cnode_cap_data (transform_cap ab) w
 3. \<And>r bits g. \<lbrakk>w \<noteq> 0; \<not> Structures_A.is_ntfn_cap ab; cap.CNodeCap r bits g = (case the_cnode_cap ab of (oref, bits, guard) \<Rightarrow> if word_bits < unat ((w >> 3) && mask 5) + bits then cap.NullCap else cap.CNodeCap oref bits (drop (size ((w >> 8) && mask 18) - unat ((w >> 3) && mask 5)) (to_bl ((w >> 8) && mask 18)))); \<not> Structures_A.is_ep_cap ab; Structures_A.is_cnode_cap ab; af = (case the_cnode_cap ab of (oref, bits, guard) \<Rightarrow> if word_bits < unat ((w >> 3) && mask 5) + bits then cap.NullCap else cap.CNodeCap oref bits (drop (size ((w >> 8) && mask 18) - unat ((w >> 3) && mask 5)) (to_bl ((w >> 8) && mask 18))))\<rbrakk> \<Longrightarrow> cdl_cap.CNodeCap r (of_bl g) (length g) bits = cdl_update_cnode_cap_data (transform_cap ab) w proof (prove)
goal (1 subgoal):
 1. \<And>r bits g. \<lbrakk>w \<noteq> 0; \<not> Structures_A.is_ntfn_cap ab; cap.CNodeCap r bits g = (case the_cnode_cap ab of (oref, bits, guard) \<Rightarrow> if word_bits < unat ((w >> 3) && mask 5) + bits then cap.NullCap else cap.CNodeCap oref bits (drop (size ((w >> 8) && mask 18) - unat ((w >> 3) && mask 5)) (to_bl ((w >> 8) && mask 18)))); \<not> Structures_A.is_ep_cap ab; Structures_A.is_cnode_cap ab; af = (case the_cnode_cap ab of (oref, bits, guard) \<Rightarrow> if word_bits < unat ((w >> 3) && mask 5) + bits then cap.NullCap else cap.CNodeCap oref bits (drop (size ((w >> 8) && mask 18) - unat ((w >> 3) && mask 5)) (to_bl ((w >> 8) && mask 18))))\<rbrakk> \<Longrightarrow> cdl_cap.CNodeCap r (of_bl g) (length g) bits = cdl_update_cnode_cap_data (transform_cap ab) w proof (prove)
goal (1 subgoal):
 1. \<And>r bits ga. \<lbrakk>af = cap.CNodeCap r bits (drop (32 - unat ((w >> 3) && mask 5)) (to_bl ((w >> 8) && mask 18))); ab = cap.CNodeCap r bits ga; w \<noteq> 0; \<not> word_bits < unat ((w >> 3) && mask 5) + bits\<rbrakk> \<Longrightarrow> cdl_cap.CNodeCap r (of_bl (drop (32 - unat ((w >> 3) && mask 5)) (to_bl ((w >> 8) && mask 18)))) (32 - (32 - unat ((w >> 3) && mask 5))) bits = cdl_update_cnode_cap_data (cdl_cap.CNodeCap r (of_bl ga) (length ga) bits) w proof (prove)
goal:
No subgoals!