theory ADT_H

lemma cap_relation_imp_CapabilityMap:
  "\<lbrakk>wellformed_cap c; cap_relation c c'\<rbrakk> \<Longrightarrow> CapabilityMap c' = c" apply (case_tac c; simp add: wellformed_cap_simps) apply (rule set_eqI, clarsimp) apply (case_tac "x", simp_all) apply (rule set_eqI, clarsimp) apply (case_tac "x", simp_all add: word_bits_def) apply clarsimp apply (simp add: set_eq_iff, rule allI) apply (case_tac x; clarsimp) apply (simp add: uint_of_bl_is_bl_to_bin bl_bin_bl[simplified]) apply (simp add: zbits_map_def split: option.splits) apply (rename_tac arch_cap) apply clarsimp apply (case_tac arch_cap, simp_all add: wellformed_cap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wellformed_cap c; cap_relation c c'\<rbrakk> \<Longrightarrow> CapabilityMap c' = c proof (prove)
goal (6 subgoals):
 1. \<And>x31 x32 x33. \<lbrakk>c' = capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33); c = cap.EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> {x. AllowWrite \<in> x33 \<and> x = AllowWrite \<or> AllowRead \<in> x33 \<and> x = AllowRead \<or> AllowGrant \<in> x33 \<and> x = AllowGrant \<or> AllowGrantReply \<in> x33 \<and> x = AllowGrantReply} = x33
 2. \<And>x41 x42 x43. \<lbrakk>AllowGrant \<notin> x43 \<and> AllowGrantReply \<notin> x43; c' = capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43); c = cap.NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> {x. AllowWrite \<in> x43 \<and> x = AllowWrite \<or> AllowRead \<in> x43 \<and> x = AllowRead} = x43
 3. \<And>x51 x52 x53. \<lbrakk>AllowWrite \<in> x53 \<and> AllowRead \<notin> x53 \<and> AllowGrantReply \<notin> x53; c' = capability.ReplyCap x51 x52 (AllowGrant \<in> x53); c = cap.ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> {x. AllowGrant \<in> x53 \<and> x = AllowGrant \<or> x = AllowWrite} = x53
 4. \<And>x61 x62 x63. \<lbrakk>0 < x62 \<and> length x63 \<le> word_bits; c' = capability.CNodeCap x61 x62 (of_bl x63) (length x63); c = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> bin_to_bl_aux (length x63) (uint (of_bl x63)) [] = x63
 5. \<And>x111 x112 x113. \<lbrakk>case x112 of None \<Rightarrow> x113 \<le> 5 | Some b \<Rightarrow> x113 \<le> 2 ^ b \<and> 0 < b; c' = capability.Zombie x111 (zbits_map x112) x113; c = cap.Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> (case zbits_map x112 of ZombieTCB \<Rightarrow> None | ZombieCNode x \<Rightarrow> Some x) = x112
 6. \<And>x12. \<lbrakk>wellformed_cap (cap.ArchObjectCap x12); \<exists>a'. acap_relation x12 a' \<and> c' = capability.ArchObjectCap a'; c = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> CapabilityMap c' = cap.ArchObjectCap x12 proof (prove)
goal (6 subgoals):
 1. \<And>x31 x32 x33 x. \<lbrakk>c' = capability.EndpointCap x31 x32 (AllowWrite \<in> x33) (AllowRead \<in> x33) (AllowGrant \<in> x33) (AllowGrantReply \<in> x33); c = cap.EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> (AllowWrite \<in> x33 \<and> x = AllowWrite \<or> AllowRead \<in> x33 \<and> x = AllowRead \<or> AllowGrant \<in> x33 \<and> x = AllowGrant \<or> AllowGrantReply \<in> x33 \<and> x = AllowGrantReply) = (x \<in> x33)
 2. \<And>x41 x42 x43. \<lbrakk>AllowGrant \<notin> x43 \<and> AllowGrantReply \<notin> x43; c' = capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43); c = cap.NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> {x. AllowWrite \<in> x43 \<and> x = AllowWrite \<or> AllowRead \<in> x43 \<and> x = AllowRead} = x43
 3. \<And>x51 x52 x53. \<lbrakk>AllowWrite \<in> x53 \<and> AllowRead \<notin> x53 \<and> AllowGrantReply \<notin> x53; c' = capability.ReplyCap x51 x52 (AllowGrant \<in> x53); c = cap.ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> {x. AllowGrant \<in> x53 \<and> x = AllowGrant \<or> x = AllowWrite} = x53
 4. \<And>x61 x62 x63. \<lbrakk>0 < x62 \<and> length x63 \<le> word_bits; c' = capability.CNodeCap x61 x62 (of_bl x63) (length x63); c = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> bin_to_bl_aux (length x63) (uint (of_bl x63)) [] = x63
 5. \<And>x111 x112 x113. \<lbrakk>case x112 of None \<Rightarrow> x113 \<le> 5 | Some b \<Rightarrow> x113 \<le> 2 ^ b \<and> 0 < b; c' = capability.Zombie x111 (zbits_map x112) x113; c = cap.Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> (case zbits_map x112 of ZombieTCB \<Rightarrow> None | ZombieCNode x \<Rightarrow> Some x) = x112
 6. \<And>x12. \<lbrakk>wellformed_cap (cap.ArchObjectCap x12); \<exists>a'. acap_relation x12 a' \<and> c' = capability.ArchObjectCap a'; c = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> CapabilityMap c' = cap.ArchObjectCap x12 proof (prove)
goal (5 subgoals):
 1. \<And>x41 x42 x43. \<lbrakk>AllowGrant \<notin> x43 \<and> AllowGrantReply \<notin> x43; c' = capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43); c = cap.NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> {x. AllowWrite \<in> x43 \<and> x = AllowWrite \<or> AllowRead \<in> x43 \<and> x = AllowRead} = x43
 2. \<And>x51 x52 x53. \<lbrakk>AllowWrite \<in> x53 \<and> AllowRead \<notin> x53 \<and> AllowGrantReply \<notin> x53; c' = capability.ReplyCap x51 x52 (AllowGrant \<in> x53); c = cap.ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> {x. AllowGrant \<in> x53 \<and> x = AllowGrant \<or> x = AllowWrite} = x53
 3. \<And>x61 x62 x63. \<lbrakk>0 < x62 \<and> length x63 \<le> word_bits; c' = capability.CNodeCap x61 x62 (of_bl x63) (length x63); c = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> bin_to_bl_aux (length x63) (uint (of_bl x63)) [] = x63
 4. \<And>x111 x112 x113. \<lbrakk>case x112 of None \<Rightarrow> x113 \<le> 5 | Some b \<Rightarrow> x113 \<le> 2 ^ b \<and> 0 < b; c' = capability.Zombie x111 (zbits_map x112) x113; c = cap.Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> (case zbits_map x112 of ZombieTCB \<Rightarrow> None | ZombieCNode x \<Rightarrow> Some x) = x112
 5. \<And>x12. \<lbrakk>wellformed_cap (cap.ArchObjectCap x12); \<exists>a'. acap_relation x12 a' \<and> c' = capability.ArchObjectCap a'; c = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> CapabilityMap c' = cap.ArchObjectCap x12 proof (prove)
goal (5 subgoals):
 1. \<And>x41 x42 x43 x. \<lbrakk>c' = capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43); c = cap.NotificationCap x41 x42 x43; AllowGrant \<notin> x43; AllowGrantReply \<notin> x43\<rbrakk> \<Longrightarrow> (AllowWrite \<in> x43 \<and> x = AllowWrite \<or> AllowRead \<in> x43 \<and> x = AllowRead) = (x \<in> x43)
 2. \<And>x51 x52 x53. \<lbrakk>AllowWrite \<in> x53 \<and> AllowRead \<notin> x53 \<and> AllowGrantReply \<notin> x53; c' = capability.ReplyCap x51 x52 (AllowGrant \<in> x53); c = cap.ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> {x. AllowGrant \<in> x53 \<and> x = AllowGrant \<or> x = AllowWrite} = x53
 3. \<And>x61 x62 x63. \<lbrakk>0 < x62 \<and> length x63 \<le> word_bits; c' = capability.CNodeCap x61 x62 (of_bl x63) (length x63); c = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> bin_to_bl_aux (length x63) (uint (of_bl x63)) [] = x63
 4. \<And>x111 x112 x113. \<lbrakk>case x112 of None \<Rightarrow> x113 \<le> 5 | Some b \<Rightarrow> x113 \<le> 2 ^ b \<and> 0 < b; c' = capability.Zombie x111 (zbits_map x112) x113; c = cap.Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> (case zbits_map x112 of ZombieTCB \<Rightarrow> None | ZombieCNode x \<Rightarrow> Some x) = x112
 5. \<And>x12. \<lbrakk>wellformed_cap (cap.ArchObjectCap x12); \<exists>a'. acap_relation x12 a' \<and> c' = capability.ArchObjectCap a'; c = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> CapabilityMap c' = cap.ArchObjectCap x12 proof (prove)
goal (4 subgoals):
 1. \<And>x51 x52 x53. \<lbrakk>AllowWrite \<in> x53 \<and> AllowRead \<notin> x53 \<and> AllowGrantReply \<notin> x53; c' = capability.ReplyCap x51 x52 (AllowGrant \<in> x53); c = cap.ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> {x. AllowGrant \<in> x53 \<and> x = AllowGrant \<or> x = AllowWrite} = x53
 2. \<And>x61 x62 x63. \<lbrakk>0 < x62 \<and> length x63 \<le> 32; c' = capability.CNodeCap x61 x62 (of_bl x63) (length x63); c = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> bin_to_bl_aux (length x63) (uint (of_bl x63)) [] = x63
 3. \<And>x111 x112 x113. \<lbrakk>case x112 of None \<Rightarrow> x113 \<le> 5 | Some b \<Rightarrow> x113 \<le> 2 ^ b \<and> 0 < b; c' = capability.Zombie x111 (zbits_map x112) x113; c = cap.Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> (case zbits_map x112 of ZombieTCB \<Rightarrow> None | ZombieCNode x \<Rightarrow> Some x) = x112
 4. \<And>x12. \<lbrakk>wellformed_cap (cap.ArchObjectCap x12); \<exists>a'. acap_relation x12 a' \<and> c' = capability.ArchObjectCap a'; c = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> CapabilityMap c' = cap.ArchObjectCap x12 proof (prove)
goal (4 subgoals):
 1. \<And>x51 x52 x53. \<lbrakk>c' = capability.ReplyCap x51 x52 (AllowGrant \<in> x53); c = cap.ReplyCap x51 x52 x53; AllowWrite \<in> x53; AllowRead \<notin> x53; AllowGrantReply \<notin> x53\<rbrakk> \<Longrightarrow> {x. AllowGrant \<in> x53 \<and> x = AllowGrant \<or> x = AllowWrite} = x53
 2. \<And>x61 x62 x63. \<lbrakk>0 < x62 \<and> length x63 \<le> 32; c' = capability.CNodeCap x61 x62 (of_bl x63) (length x63); c = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> bin_to_bl_aux (length x63) (uint (of_bl x63)) [] = x63
 3. \<And>x111 x112 x113. \<lbrakk>case x112 of None \<Rightarrow> x113 \<le> 5 | Some b \<Rightarrow> x113 \<le> 2 ^ b \<and> 0 < b; c' = capability.Zombie x111 (zbits_map x112) x113; c = cap.Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> (case zbits_map x112 of ZombieTCB \<Rightarrow> None | ZombieCNode x \<Rightarrow> Some x) = x112
 4. \<And>x12. \<lbrakk>wellformed_cap (cap.ArchObjectCap x12); \<exists>a'. acap_relation x12 a' \<and> c' = capability.ArchObjectCap a'; c = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> CapabilityMap c' = cap.ArchObjectCap x12 proof (prove)
goal (4 subgoals):
 1. \<And>x51 x52 x53 x. \<lbrakk>c' = capability.ReplyCap x51 x52 (AllowGrant \<in> x53); c = cap.ReplyCap x51 x52 x53; AllowWrite \<in> x53; AllowRead \<notin> x53; AllowGrantReply \<notin> x53\<rbrakk> \<Longrightarrow> (AllowGrant \<in> x53 \<and> x = AllowGrant \<or> x = AllowWrite) = (x \<in> x53)
 2. \<And>x61 x62 x63. \<lbrakk>0 < x62 \<and> length x63 \<le> 32; c' = capability.CNodeCap x61 x62 (of_bl x63) (length x63); c = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> bin_to_bl_aux (length x63) (uint (of_bl x63)) [] = x63
 3. \<And>x111 x112 x113. \<lbrakk>case x112 of None \<Rightarrow> x113 \<le> 5 | Some b \<Rightarrow> x113 \<le> 2 ^ b \<and> 0 < b; c' = capability.Zombie x111 (zbits_map x112) x113; c = cap.Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> (case zbits_map x112 of ZombieTCB \<Rightarrow> None | ZombieCNode x \<Rightarrow> Some x) = x112
 4. \<And>x12. \<lbrakk>wellformed_cap (cap.ArchObjectCap x12); \<exists>a'. acap_relation x12 a' \<and> c' = capability.ArchObjectCap a'; c = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> CapabilityMap c' = cap.ArchObjectCap x12 proof (prove)
goal (3 subgoals):
 1. \<And>x61 x62 x63. \<lbrakk>0 < x62 \<and> length x63 \<le> 32; c' = capability.CNodeCap x61 x62 (of_bl x63) (length x63); c = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> bin_to_bl_aux (length x63) (uint (of_bl x63)) [] = x63
 2. \<And>x111 x112 x113. \<lbrakk>case x112 of None \<Rightarrow> x113 \<le> 5 | Some b \<Rightarrow> x113 \<le> 2 ^ b \<and> 0 < b; c' = capability.Zombie x111 (zbits_map x112) x113; c = cap.Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> (case zbits_map x112 of ZombieTCB \<Rightarrow> None | ZombieCNode x \<Rightarrow> Some x) = x112
 3. \<And>x12. \<lbrakk>wellformed_cap (cap.ArchObjectCap x12); \<exists>a'. acap_relation x12 a' \<and> c' = capability.ArchObjectCap a'; c = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> CapabilityMap c' = cap.ArchObjectCap x12 proof (prove)
goal (2 subgoals):
 1. \<And>x111 x112 x113. \<lbrakk>case x112 of None \<Rightarrow> x113 \<le> 5 | Some b \<Rightarrow> x113 \<le> 2 ^ b \<and> 0 < b; c' = capability.Zombie x111 (zbits_map x112) x113; c = cap.Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> (case zbits_map x112 of ZombieTCB \<Rightarrow> None | ZombieCNode x \<Rightarrow> Some x) = x112
 2. \<And>x12. \<lbrakk>wellformed_cap (cap.ArchObjectCap x12); \<exists>a'. acap_relation x12 a' \<and> c' = capability.ArchObjectCap a'; c = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> CapabilityMap c' = cap.ArchObjectCap x12 proof (prove)
goal (1 subgoal):
 1. \<And>x12. \<lbrakk>wellformed_cap (cap.ArchObjectCap x12); \<exists>a'. acap_relation x12 a' \<and> c' = capability.ArchObjectCap a'; c = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> CapabilityMap c' = cap.ArchObjectCap x12 proof (prove)
goal (1 subgoal):
 1. \<And>arch_cap. \<lbrakk>wellformed_cap (cap.ArchObjectCap arch_cap); \<exists>a'. acap_relation arch_cap a' \<and> c' = capability.ArchObjectCap a'; c = cap.ArchObjectCap arch_cap\<rbrakk> \<Longrightarrow> CapabilityMap c' = cap.ArchObjectCap arch_cap proof (prove)
goal (1 subgoal):
 1. \<And>arch_cap a'. \<lbrakk>wellformed_cap (cap.ArchObjectCap arch_cap); c = cap.ArchObjectCap arch_cap; acap_relation arch_cap a'; c' = capability.ArchObjectCap a'\<rbrakk> \<Longrightarrow> CapabilityMap (capability.ArchObjectCap a') = cap.ArchObjectCap arch_cap proof (prove)
goal:
No subgoals!