theory ArchCNodeInv_AI

lemma update_cap_data_mask_Null [simp, CNodeInv_AI_assms]:
  "(update_cap_data P x (mask_cap m c) = NullCap) = (update_cap_data P x c = NullCap)" unfolding update_cap_data_def mask_cap_def apply (cases c) by (auto simp add: the_cnode_cap_def Let_def is_cap_simps cap_rights_update_def badge_update_def
                        arch_update_cap_data_def split:bool.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (update_cap_data P x (mask_cap m c) = NullCap) = (update_cap_data P x c = NullCap) proof (prove)
goal (1 subgoal):
 1. ((if is_ep_cap (cap_rights_update (cap_rights c \<inter> m) c) then if cap_ep_badge (cap_rights_update (cap_rights c \<inter> m) c) = 0 \<and> \<not> P then badge_update x (cap_rights_update (cap_rights c \<inter> m) c) else NullCap else if is_ntfn_cap (cap_rights_update (cap_rights c \<inter> m) c) then if cap_ep_badge (cap_rights_update (cap_rights c \<inter> m) c) = 0 \<and> \<not> P then badge_update x (cap_rights_update (cap_rights c \<inter> m) c) else NullCap else if is_cnode_cap (cap_rights_update (cap_rights c \<inter> m) c) then let (oref, bits, guard) = the_cnode_cap (cap_rights_update (cap_rights c \<inter> m) c); (guard_size', guard'') = update_cnode_cap_data x; guard' = drop (size guard'' - guard_size') (to_bl guard'') in if word_bits < guard_size' + bits then NullCap else CNodeCap oref bits guard' else if is_arch_cap (cap_rights_update (cap_rights c \<inter> m) c) then arch_update_cap_data P x (the_arch_cap (cap_rights_update (cap_rights c \<inter> m) c)) else cap_rights_update (cap_rights c \<inter> m) c) = NullCap) = ((if is_ep_cap c then if cap_ep_badge c = 0 \<and> \<not> P then badge_update x c else NullCap else if is_ntfn_cap c then if cap_ep_badge c = 0 \<and> \<not> P then badge_update x c else NullCap else if is_cnode_cap c then let (oref, bits, guard) = the_cnode_cap c; (guard_size', guard'') = update_cnode_cap_data x; guard' = drop (size guard'' - guard_size') (to_bl guard'') in if word_bits < guard_size' + bits then NullCap else CNodeCap oref bits guard' else if is_arch_cap c then arch_update_cap_data P x (the_arch_cap c) else c) = NullCap) proof (prove)
goal (12 subgoals):
 1. c = NullCap \<Longrightarrow> ((if is_ep_cap (cap_rights_update (cap_rights c \<inter> m) c) then if cap_ep_badge (cap_rights_update (cap_rights c \<inter> m) c) = 0 \<and> \<not> P then badge_update x (cap_rights_update (cap_rights c \<inter> m) c) else NullCap else if is_ntfn_cap (cap_rights_update (cap_rights c \<inter> m) c) then if cap_ep_badge (cap_rights_update (cap_rights c \<inter> m) c) = 0 \<and> \<not> P then badge_update x (cap_rights_update (cap_rights c \<inter> m) c) else NullCap else if is_cnode_cap (cap_rights_update (cap_rights c \<inter> m) c) then let (oref, bits, guard) = the_cnode_cap (cap_rights_update (cap_rights c \<inter> m) c); (guard_size', guard'') = update_cnode_cap_data x; guard' = drop (size guard'' - guard_size') (to_bl guard'') in if word_bits < guard_size' + bits then NullCap else CNodeCap oref bits guard' else if is_arch_cap (cap_rights_update (cap_rights c \<inter> m) c) then arch_update_cap_data P x (the_arch_cap (cap_rights_update (cap_rights c \<inter> m) c)) else cap_rights_update (cap_rights c \<inter> m) c) = NullCap) = ((if is_ep_cap c then if cap_ep_badge c = 0 \<and> \<not> P then badge_update x c else NullCap else if is_ntfn_cap c then if cap_ep_badge c = 0 \<and> \<not> P then badge_update x c else NullCap else if is_cnode_cap c then let (oref, bits, guard) = the_cnode_cap c; (guard_size', guard'') = update_cnode_cap_data x; guard' = drop (size guard'' - guard_size') (to_bl guard'') in if word_bits < guard_size' + bits then NullCap else CNodeCap oref bits guard' else if is_arch_cap c then arch_update_cap_data P x (the_arch_cap c) else c) = NullCap)
 2. \<And>x21 x22 x23 x24. c = UntypedCap x21 x22 x23 x24 \<Longrightarrow> ((if is_ep_cap (cap_rights_update (cap_rights c \<inter> m) c) then if cap_ep_badge (cap_rights_update (cap_rights c \<inter> m) c) = 0 \<and> \<not> P then badge_update x (cap_rights_update (cap_rights c \<inter> m) c) else NullCap else if is_ntfn_cap (cap_rights_update (cap_rights c \<inter> m) c) then if cap_ep_badge (cap_rights_update (cap_rights c \<inter> m) c) = 0 \<and> \<not> P then badge_update x (cap_rights_update (cap_rights c \<inter> m) c) else NullCap else if is_cnode_cap (cap_rights_update (cap_rights c \<inter> m) c) then let (oref, bits, guard) = the_cnode_cap (cap_rights_update (cap_rights c \<inter> m) c); (guard_size', guard'') = update_cnode_cap_data x; guard' = drop (size guard'' - guard_size') (to_bl guard'') in if word_bits < guard_size' + bits then NullCap else CNodeCap oref bits guard' else if is_arch_cap (cap_rights_update (cap_rights c \<inter> m) c) then arch_update_cap_data P x (the_arch_cap (cap_rights_update (cap_rights c \<inter> m) c)) else cap_rights_update (cap_rights c \<inter> m) c) = NullCap) = ((if is_ep_cap c then if cap_ep_badge c = 0 \<and> \<not> P then badge_update x c else NullCap else if is_ntfn_cap c then if cap_ep_badge c = 0 \<and> \<not> P then badge_update x c else NullCap else if is_cnode_cap c then let (oref, bits, guard) = the_cnode_cap c; (guard_size', guard'') = update_cnode_cap_data x; guard' = drop (size guard'' - guard_size') (to_bl guard'') in if word_bits < guard_size' + bits then NullCap else CNodeCap oref bits guard' else if is_arch_cap c then arch_update_cap_data P x (the_arch_cap c) else c) = NullCap)
 3. \<And>x31 x32 x33. c = EndpointCap x31 x32 x33 \<Longrightarrow> ((if is_ep_cap (cap_rights_update (cap_rights c \<inter> m) c) then if cap_ep_badge (cap_rights_update (cap_rights c \<inter> m) c) = 0 \<and> \<not> P then badge_update x (cap_rights_update (cap_rights c \<inter> m) c) else NullCap else if is_ntfn_cap (cap_rights_update (cap_rights c \<inter> m) c) then if cap_ep_badge (cap_rights_update (cap_rights c \<inter> m) c) = 0 \<and> \<not> P then badge_update x (cap_rights_update (cap_rights c \<inter> m) c) else NullCap else if is_cnode_cap (cap_rights_update (cap_rights c \<inter> m) c) then let (oref, bits, guard) = the_cnode_cap (cap_rights_update (cap_rights c \<inter> m) c); (guard_size', guard'') = update_cnode_cap_data x; guard' = drop (size guard'' - guard_size') (to_bl guard'') in if word_bits < guard_size' + bits then NullCap else CNodeCap oref bits guard' else if is_arch_cap (cap_rights_update (cap_rights c \<inter> m) c) then arch_update_cap_data P x (the_arch_cap (cap_rights_update (cap_rights c \<inter> m) c)) else cap_rights_update (cap_rights c \<inter> m) c) = NullCap) = ((if is_ep_cap c then if cap_ep_badge c = 0 \<and> \<not> P then badge_update x c else NullCap else if is_ntfn_cap c then if cap_ep_badge c = 0 \<and> \<not> P then badge_update x c else NullCap else if is_cnode_cap c then let (oref, bits, guard) = the_cnode_cap c; (guard_size', guard'') = update_cnode_cap_data x; guard' = drop (size guard'' - guard_size') (to_bl guard'') in if word_bits < guard_size' + bits then NullCap else CNodeCap oref bits guard' else if is_arch_cap c then arch_update_cap_data P x (the_arch_cap c) else c) = NullCap)
 4. \<And>x41 x42 x43. c = NotificationCap x41 x42 x43 \<Longrightarrow> ((if is_ep_cap (cap_rights_update (cap_rights c \<inter> m) c) then if cap_ep_badge (cap_rights_update (cap_rights c \<inter> m) c) = 0 \<and> \<not> P then badge_update x (cap_rights_update (cap_rights c \<inter> m) c) else NullCap else if is_ntfn_cap (cap_rights_update (cap_rights c \<inter> m) c) then if cap_ep_badge (cap_rights_update (cap_rights c \<inter> m) c) = 0 \<and> \<not> P then badge_update x (cap_rights_update (cap_rights c \<inter> m) c) else NullCap else if is_cnode_cap (cap_rights_update (cap_rights c \<inter> m) c) then let (oref, bits, guard) = the_cnode_cap (cap_rights_update (cap_rights c \<inter> m) c); (guard_size', guard'') = update_cnode_cap_data x; guard' = drop (size guard'' - guard_size') (to_bl guard'') in if word_bits < guard_size' + bits then NullCap else CNodeCap oref bits guard' else if is_arch_cap (cap_rights_update (cap_rights c \<inter> m) c) then arch_update_cap_data P x (the_arch_cap (cap_rights_update (cap_rights c \<inter> m) c)) else cap_rights_update (cap_rights c \<inter> m) c) = NullCap) = ((if is_ep_cap c then if cap_ep_badge c = 0 \<and> \<not> P then badge_update x c else NullCap else if is_ntfn_cap c then if cap_ep_badge c = 0 \<and> \<not> P then badge_update x c else NullCap else if is_cnode_cap c then let (oref, bits, guard) = the_cnode_cap c; (guard_size', guard'') = update_cnode_cap_data x; guard' = drop (size guard'' - guard_size') (to_bl guard'') in if word_bits < guard_size' + bits then NullCap else CNodeCap oref bits guard' else if is_arch_cap c then arch_update_cap_data P x (the_arch_cap c) else c) = NullCap)
 5. \<And>x51 x52 x53. c = ReplyCap x51 x52 x53 \<Longrightarrow> ((if is_ep_cap (cap_rights_update (cap_rights c \<inter> m) c) then if cap_ep_badge (cap_rights_update (cap_rights c \<inter> m) c) = 0 \<and> \<not> P then badge_update x (cap_rights_update (cap_rights c \<inter> m) c) else NullCap else if is_ntfn_cap (cap_rights_update (cap_rights c \<inter> m) c) then if cap_ep_badge (cap_rights_update (cap_rights c \<inter> m) c) = 0 \<and> \<not> P then badge_update x (cap_rights_update (cap_rights c \<inter> m) c) else NullCap else if is_cnode_cap (cap_rights_update (cap_rights c \<inter> m) c) then let (oref, bits, guard) = the_cnode_cap (cap_rights_update (cap_rights c \<inter> m) c); (guard_size', guard'') = update_cnode_cap_data x; guard' = drop (size guard'' - guard_size') (to_bl guard'') in if word_bits < guard_size' + bits then NullCap else CNodeCap oref bits guard' else if is_arch_cap (cap_rights_update (cap_rights c \<inter> m) c) then arch_update_cap_data P x (the_arch_cap (cap_rights_update (cap_rights c \<inter> m) c)) else cap_rights_update (cap_rights c \<inter> m) c) = NullCap) = ((if is_ep_cap c then if cap_ep_badge c = 0 \<and> \<not> P then badge_update x c else NullCap else if is_ntfn_cap c then if cap_ep_badge c = 0 \<and> \<not> P then badge_update x c else NullCap else if is_cnode_cap c then let (oref, bits, guard) = the_cnode_cap c; (guard_size', guard'') = update_cnode_cap_data x; guard' = drop (size guard'' - guard_size') (to_bl guard'') in if word_bits < guard_size' + bits then NullCap else CNodeCap oref bits guard' else if is_arch_cap c then arch_update_cap_data P x (the_arch_cap c) else c) = NullCap)
 6. \<And>x61 x62 x63. c = CNodeCap x61 x62 x63 \<Longrightarrow> ((if is_ep_cap (cap_rights_update (cap_rights c \<inter> m) c) then if cap_ep_badge (cap_rights_update (cap_rights c \<inter> m) c) = 0 \<and> \<not> P then badge_update x (cap_rights_update (cap_rights c \<inter> m) c) else NullCap else if is_ntfn_cap (cap_rights_update (cap_rights c \<inter> m) c) then if cap_ep_badge (cap_rights_update (cap_rights c \<inter> m) c) = 0 \<and> \<not> P then badge_update x (cap_rights_update (cap_rights c \<inter> m) c) else NullCap else if is_cnode_cap (cap_rights_update (cap_rights c \<inter> m) c) then let (oref, bits, guard) = the_cnode_cap (cap_rights_update (cap_rights c \<inter> m) c); (guard_size', guard'') = update_cnode_cap_data x; guard' = drop (size guard'' - guard_size') (to_bl guard'') in if word_bits < guard_size' + bits then NullCap else CNodeCap oref bits guard' else if is_arch_cap (cap_rights_update (cap_rights c \<inter> m) c) then arch_update_cap_data P x (the_arch_cap (cap_rights_update (cap_rights c \<inter> m) c)) else cap_rights_update (cap_rights c \<inter> m) c) = NullCap) = ((if is_ep_cap c then if cap_ep_badge c = 0 \<and> \<not> P then badge_update x c else NullCap else if is_ntfn_cap c then if cap_ep_badge c = 0 \<and> \<not> P then badge_update x c else NullCap else if is_cnode_cap c then let (oref, bits, guard) = the_cnode_cap c; (guard_size', guard'') = update_cnode_cap_data x; guard' = drop (size guard'' - guard_size') (to_bl guard'') in if word_bits < guard_size' + bits then NullCap else CNodeCap oref bits guard' else if is_arch_cap c then arch_update_cap_data P x (the_arch_cap c) else c) = NullCap)
 7. \<And>x7. c = ThreadCap x7 \<Longrightarrow> ((if is_ep_cap (cap_rights_update (cap_rights c \<inter> m) c) then if cap_ep_badge (cap_rights_update (cap_rights c \<inter> m) c) = 0 \<and> \<not> P then badge_update x (cap_rights_update (cap_rights c \<inter> m) c) else NullCap else if is_ntfn_cap (cap_rights_update (cap_rights c \<inter> m) c) then if cap_ep_badge (cap_rights_update (cap_rights c \<inter> m) c) = 0 \<and> \<not> P then badge_update x (cap_rights_update (cap_rights c \<inter> m) c) else NullCap else if is_cnode_cap (cap_rights_update (cap_rights c \<inter> m) c) then let (oref, bits, guard) = the_cnode_cap (cap_rights_update (cap_rights c \<inter> m) c); (guard_size', guard'') = update_cnode_cap_data x; guard' = drop (size guard'' - guard_size') (to_bl guard'') in if word_bits < guard_size' + bits then NullCap else CNodeCap oref bits guard' else if is_arch_cap (cap_rights_update (cap_rights c \<inter> m) c) then arch_update_cap_data P x (the_arch_cap (cap_rights_update (cap_rights c \<inter> m) c)) else cap_rights_update (cap_rights c \<inter> m) c) = NullCap) = ((if is_ep_cap c then if cap_ep_badge c = 0 \<and> \<not> P then badge_update x c else NullCap else if is_ntfn_cap c then if cap_ep_badge c = 0 \<and> \<not> P then badge_update x c else NullCap else if is_cnode_cap c then let (oref, bits, guard) = the_cnode_cap c; (guard_size', guard'') = update_cnode_cap_data x; guard' = drop (size guard'' - guard_size') (to_bl guard'') in if word_bits < guard_size' + bits then NullCap else CNodeCap oref bits guard' else if is_arch_cap c then arch_update_cap_data P x (the_arch_cap c) else c) = NullCap)
 8. c = DomainCap \<Longrightarrow> ((if is_ep_cap (cap_rights_update (cap_rights c \<inter> m) c) then if cap_ep_badge (cap_rights_update (cap_rights c \<inter> m) c) = 0 \<and> \<not> P then badge_update x (cap_rights_update (cap_rights c \<inter> m) c) else NullCap else if is_ntfn_cap (cap_rights_update (cap_rights c \<inter> m) c) then if cap_ep_badge (cap_rights_update (cap_rights c \<inter> m) c) = 0 \<and> \<not> P then badge_update x (cap_rights_update (cap_rights c \<inter> m) c) else NullCap else if is_cnode_cap (cap_rights_update (cap_rights c \<inter> m) c) then let (oref, bits, guard) = the_cnode_cap (cap_rights_update (cap_rights c \<inter> m) c); (guard_size', guard'') = update_cnode_cap_data x; guard' = drop (size guard'' - guard_size') (to_bl guard'') in if word_bits < guard_size' + bits then NullCap else CNodeCap oref bits guard' else if is_arch_cap (cap_rights_update (cap_rights c \<inter> m) c) then arch_update_cap_data P x (the_arch_cap (cap_rights_update (cap_rights c \<inter> m) c)) else cap_rights_update (cap_rights c \<inter> m) c) = NullCap) = ((if is_ep_cap c then if cap_ep_badge c = 0 \<and> \<not> P then badge_update x c else NullCap else if is_ntfn_cap c then if cap_ep_badge c = 0 \<and> \<not> P then badge_update x c else NullCap else if is_cnode_cap c then let (oref, bits, guard) = the_cnode_cap c; (guard_size', guard'') = update_cnode_cap_data x; guard' = drop (size guard'' - guard_size') (to_bl guard'') in if word_bits < guard_size' + bits then NullCap else CNodeCap oref bits guard' else if is_arch_cap c then arch_update_cap_data P x (the_arch_cap c) else c) = NullCap)
 9. c = IRQControlCap \<Longrightarrow> ((if is_ep_cap (cap_rights_update (cap_rights c \<inter> m) c) then if cap_ep_badge (cap_rights_update (cap_rights c \<inter> m) c) = 0 \<and> \<not> P then badge_update x (cap_rights_update (cap_rights c \<inter> m) c) else NullCap else if is_ntfn_cap (cap_rights_update (cap_rights c \<inter> m) c) then if cap_ep_badge (cap_rights_update (cap_rights c \<inter> m) c) = 0 \<and> \<not> P then badge_update x (cap_rights_update (cap_rights c \<inter> m) c) else NullCap else if is_cnode_cap (cap_rights_update (cap_rights c \<inter> m) c) then let (oref, bits, guard) = the_cnode_cap (cap_rights_update (cap_rights c \<inter> m) c); (guard_size', guard'') = update_cnode_cap_data x; guard' = drop (size guard'' - guard_size') (to_bl guard'') in if word_bits < guard_size' + bits then NullCap else CNodeCap oref bits guard' else if is_arch_cap (cap_rights_update (cap_rights c \<inter> m) c) then arch_update_cap_data P x (the_arch_cap (cap_rights_update (cap_rights c \<inter> m) c)) else cap_rights_update (cap_rights c \<inter> m) c) = NullCap) = ((if is_ep_cap c then if cap_ep_badge c = 0 \<and> \<not> P then badge_update x c else NullCap else if is_ntfn_cap c then if cap_ep_badge c = 0 \<and> \<not> P then badge_update x c else NullCap else if is_cnode_cap c then let (oref, bits, guard) = the_cnode_cap c; (guard_size', guard'') = update_cnode_cap_data x; guard' = drop (size guard'' - guard_size') (to_bl guard'') in if word_bits < guard_size' + bits then NullCap else CNodeCap oref bits guard' else if is_arch_cap c then arch_update_cap_data P x (the_arch_cap c) else c) = NullCap)
 10. \<And>x10. c = IRQHandlerCap x10 \<Longrightarrow> ((if is_ep_cap (cap_rights_update (cap_rights c \<inter> m) c) then if cap_ep_badge (cap_rights_update (cap_rights c \<inter> m) c) = 0 \<and> \<not> P then badge_update x (cap_rights_update (cap_rights c \<inter> m) c) else NullCap else if is_ntfn_cap (cap_rights_update (cap_rights c \<inter> m) c) then if cap_ep_badge (cap_rights_update (cap_rights c \<inter> m) c) = 0 \<and> \<not> P then badge_update x (cap_rights_update (cap_rights c \<inter> m) c) else NullCap else if is_cnode_cap (cap_rights_update (cap_rights c \<inter> m) c) then let (oref, bits, guard) = the_cnode_cap (cap_rights_update (cap_rights c \<inter> m) c); (guard_size', guard'') = update_cnode_cap_data x; guard' = drop (size guard'' - guard_size') (to_bl guard'') in if word_bits < guard_size' + bits then NullCap else CNodeCap oref bits guard' else if is_arch_cap (cap_rights_update (cap_rights c \<inter> m) c) then arch_update_cap_data P x (the_arch_cap (cap_rights_update (cap_rights c \<inter> m) c)) else cap_rights_update (cap_rights c \<inter> m) c) = NullCap) = ((if is_ep_cap c then if cap_ep_badge c = 0 \<and> \<not> P then badge_update x c else NullCap else if is_ntfn_cap c then if cap_ep_badge c = 0 \<and> \<not> P then badge_update x c else NullCap else if is_cnode_cap c then let (oref, bits, guard) = the_cnode_cap c; (guard_size', guard'') = update_cnode_cap_data x; guard' = drop (size guard'' - guard_size') (to_bl guard'') in if word_bits < guard_size' + bits then NullCap else CNodeCap oref bits guard' else if is_arch_cap c then arch_update_cap_data P x (the_arch_cap c) else c) = NullCap)
A total of 12 subgoals...