theory ArchCSpace_AI

lemma update_cap_data_validI [CSpace_AI_assms]:
  "s \<turnstile> cap \<Longrightarrow> s \<turnstile> update_cap_data p d cap" apply (cases cap) apply (simp_all add: is_cap_defs update_cap_data_def Let_def split_def) apply (simp add: valid_cap_def cap_aligned_def) apply (simp add: valid_cap_def cap_aligned_def) apply (simp add: the_cnode_cap_def valid_cap_def cap_aligned_def word_bits_def) apply (rename_tac arch_cap) apply (case_tac arch_cap) apply (simp_all add: is_cap_defs arch_update_cap_data_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<turnstile> cap \<Longrightarrow> s \<turnstile> update_cap_data p d cap proof (prove)
goal (12 subgoals):
 1. \<lbrakk>s \<turnstile> cap; cap = NullCap\<rbrakk> \<Longrightarrow> s \<turnstile> update_cap_data p d cap
 2. \<And>x21 x22 x23 x24. \<lbrakk>s \<turnstile> cap; cap = UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> s \<turnstile> update_cap_data p d cap
 3. \<And>x31 x32 x33. \<lbrakk>s \<turnstile> cap; cap = EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> s \<turnstile> update_cap_data p d cap
 4. \<And>x41 x42 x43. \<lbrakk>s \<turnstile> cap; cap = NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> s \<turnstile> update_cap_data p d cap
 5. \<And>x51 x52 x53. \<lbrakk>s \<turnstile> cap; cap = ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> s \<turnstile> update_cap_data p d cap
 6. \<And>x61 x62 x63. \<lbrakk>s \<turnstile> cap; cap = CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> s \<turnstile> update_cap_data p d cap
 7. \<And>x7. \<lbrakk>s \<turnstile> cap; cap = ThreadCap x7\<rbrakk> \<Longrightarrow> s \<turnstile> update_cap_data p d cap
 8. \<lbrakk>s \<turnstile> cap; cap = DomainCap\<rbrakk> \<Longrightarrow> s \<turnstile> update_cap_data p d cap
 9. \<lbrakk>s \<turnstile> cap; cap = IRQControlCap\<rbrakk> \<Longrightarrow> s \<turnstile> update_cap_data p d cap
 10. \<And>x10. \<lbrakk>s \<turnstile> cap; cap = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> s \<turnstile> update_cap_data p d cap
A total of 12 subgoals... proof (prove)
goal (4 subgoals):
 1. \<And>x31 x32 x33. \<lbrakk>s \<turnstile> EndpointCap x31 x32 x33; cap = EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> x32 = 0 \<and> \<not> p \<longrightarrow> s \<turnstile> EndpointCap x31 0 x33
 2. \<And>x41 x42 x43. \<lbrakk>s \<turnstile> NotificationCap x41 x42 x43; cap = NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> x42 = 0 \<and> \<not> p \<longrightarrow> s \<turnstile> NotificationCap x41 0 x43
 3. \<And>x61 x62 x63. \<lbrakk>s \<turnstile> CNodeCap x61 x62 x63; cap = CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> \<not> word_bits < unat ((d >> 3) && mask 5) + fst (snd (the_cnode_cap (CNodeCap x61 x62 x63))) \<longrightarrow> s \<turnstile> CNodeCap (fst (the_cnode_cap (CNodeCap x61 x62 x63))) (fst (snd (the_cnode_cap (CNodeCap x61 x62 x63)))) (drop (size ((d >> 8) && mask 18) - unat ((d >> 3) && mask 5)) (to_bl ((d >> 8) && mask 18)))
 4. \<And>x12. \<lbrakk>s \<turnstile> ArchObjectCap x12; cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> s \<turnstile> arch_update_cap_data p d x12 proof (prove)
goal (3 subgoals):
 1. \<And>x41 x42 x43. \<lbrakk>s \<turnstile> NotificationCap x41 x42 x43; cap = NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> x42 = 0 \<and> \<not> p \<longrightarrow> s \<turnstile> NotificationCap x41 0 x43
 2. \<And>x61 x62 x63. \<lbrakk>s \<turnstile> CNodeCap x61 x62 x63; cap = CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> \<not> word_bits < unat ((d >> 3) && mask 5) + fst (snd (the_cnode_cap (CNodeCap x61 x62 x63))) \<longrightarrow> s \<turnstile> CNodeCap (fst (the_cnode_cap (CNodeCap x61 x62 x63))) (fst (snd (the_cnode_cap (CNodeCap x61 x62 x63)))) (drop (size ((d >> 8) && mask 18) - unat ((d >> 3) && mask 5)) (to_bl ((d >> 8) && mask 18)))
 3. \<And>x12. \<lbrakk>s \<turnstile> ArchObjectCap x12; cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> s \<turnstile> arch_update_cap_data p d x12 proof (prove)
goal (2 subgoals):
 1. \<And>x61 x62 x63. \<lbrakk>s \<turnstile> CNodeCap x61 x62 x63; cap = CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> \<not> word_bits < unat ((d >> 3) && mask 5) + fst (snd (the_cnode_cap (CNodeCap x61 x62 x63))) \<longrightarrow> s \<turnstile> CNodeCap (fst (the_cnode_cap (CNodeCap x61 x62 x63))) (fst (snd (the_cnode_cap (CNodeCap x61 x62 x63)))) (drop (size ((d >> 8) && mask 18) - unat ((d >> 3) && mask 5)) (to_bl ((d >> 8) && mask 18)))
 2. \<And>x12. \<lbrakk>s \<turnstile> ArchObjectCap x12; cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> s \<turnstile> arch_update_cap_data p d x12 proof (prove)
goal (1 subgoal):
 1. \<And>x12. \<lbrakk>s \<turnstile> ArchObjectCap x12; cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> s \<turnstile> arch_update_cap_data p d x12 proof (prove)
goal (1 subgoal):
 1. \<And>arch_cap. \<lbrakk>s \<turnstile> ArchObjectCap arch_cap; cap = ArchObjectCap arch_cap\<rbrakk> \<Longrightarrow> s \<turnstile> arch_update_cap_data p d arch_cap proof (prove)
goal (5 subgoals):
 1. \<And>arch_cap x11 x12. \<lbrakk>s \<turnstile> ArchObjectCap arch_cap; cap = ArchObjectCap arch_cap; arch_cap = ASIDPoolCap x11 x12\<rbrakk> \<Longrightarrow> s \<turnstile> arch_update_cap_data p d arch_cap
 2. \<And>arch_cap. \<lbrakk>s \<turnstile> ArchObjectCap arch_cap; cap = ArchObjectCap arch_cap; arch_cap = ASIDControlCap\<rbrakk> \<Longrightarrow> s \<turnstile> arch_update_cap_data p d arch_cap
 3. \<And>arch_cap x31 x32 x33 x34 x35. \<lbrakk>s \<turnstile> ArchObjectCap arch_cap; cap = ArchObjectCap arch_cap; arch_cap = PageCap x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> s \<turnstile> arch_update_cap_data p d arch_cap
 4. \<And>arch_cap x41 x42. \<lbrakk>s \<turnstile> ArchObjectCap arch_cap; cap = ArchObjectCap arch_cap; arch_cap = PageTableCap x41 x42\<rbrakk> \<Longrightarrow> s \<turnstile> arch_update_cap_data p d arch_cap
 5. \<And>arch_cap x51 x52. \<lbrakk>s \<turnstile> ArchObjectCap arch_cap; cap = ArchObjectCap arch_cap; arch_cap = PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> s \<turnstile> arch_update_cap_data p d arch_cap proof (prove)
goal:
No subgoals!