theory Invariants_AI

lemma valid_cap_def2:
  "s \<turnstile> c \<equiv> cap_aligned c \<and> wellformed_cap c \<and> valid_cap_ref c s" apply (rule eq_reflection) apply (cases c) apply (simp_all add: valid_cap_simps wellformed_cap_simps
                               valid_cap_ref_simps
                        split: option.splits) apply (fastforce+) by (simp add: valid_arch_cap_def2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<turnstile> c \<equiv> cap_aligned c \<and> wellformed_cap c \<and> valid_cap_ref c s proof (prove)
goal (1 subgoal):
 1. s \<turnstile> c = (cap_aligned c \<and> wellformed_cap c \<and> valid_cap_ref c s) proof (prove)
goal (12 subgoals):
 1. c = NullCap \<Longrightarrow> s \<turnstile> c = (cap_aligned c \<and> wellformed_cap c \<and> valid_cap_ref c s)
 2. \<And>x21 x22 x23 x24. c = UntypedCap x21 x22 x23 x24 \<Longrightarrow> s \<turnstile> c = (cap_aligned c \<and> wellformed_cap c \<and> valid_cap_ref c s)
 3. \<And>x31 x32 x33. c = EndpointCap x31 x32 x33 \<Longrightarrow> s \<turnstile> c = (cap_aligned c \<and> wellformed_cap c \<and> valid_cap_ref c s)
 4. \<And>x41 x42 x43. c = NotificationCap x41 x42 x43 \<Longrightarrow> s \<turnstile> c = (cap_aligned c \<and> wellformed_cap c \<and> valid_cap_ref c s)
 5. \<And>x51 x52 x53. c = ReplyCap x51 x52 x53 \<Longrightarrow> s \<turnstile> c = (cap_aligned c \<and> wellformed_cap c \<and> valid_cap_ref c s)
 6. \<And>x61 x62 x63. c = CNodeCap x61 x62 x63 \<Longrightarrow> s \<turnstile> c = (cap_aligned c \<and> wellformed_cap c \<and> valid_cap_ref c s)
 7. \<And>x7. c = ThreadCap x7 \<Longrightarrow> s \<turnstile> c = (cap_aligned c \<and> wellformed_cap c \<and> valid_cap_ref c s)
 8. c = DomainCap \<Longrightarrow> s \<turnstile> c = (cap_aligned c \<and> wellformed_cap c \<and> valid_cap_ref c s)
 9. c = IRQControlCap \<Longrightarrow> s \<turnstile> c = (cap_aligned c \<and> wellformed_cap c \<and> valid_cap_ref c s)
 10. \<And>x10. c = IRQHandlerCap x10 \<Longrightarrow> s \<turnstile> c = (cap_aligned c \<and> wellformed_cap c \<and> valid_cap_ref c s)
A total of 12 subgoals... proof (prove)
goal (6 subgoals):
 1. \<And>x21 x22 x23 x24. c = UntypedCap x21 x22 x23 x24 \<Longrightarrow> (cap_aligned (UntypedCap x21 x22 x23 x24) \<and> valid_untyped (UntypedCap x21 x22 x23 x24) s \<and> untyped_min_bits \<le> x23 \<and> x24 \<le> 2 ^ x23 \<and> x22 \<noteq> 0) = (cap_aligned (UntypedCap x21 x22 x23 x24) \<and> untyped_min_bits \<le> x23 \<and> valid_untyped (UntypedCap x21 x22 x23 x24) s \<and> x24 \<le> 2 ^ x23 \<and> x22 \<noteq> 0)
 2. \<And>x41 x42 x43. c = NotificationCap x41 x42 x43 \<Longrightarrow> (cap_aligned (NotificationCap x41 x42 x43) \<and> ntfn_at x41 s \<and> AllowGrant \<notin> x43 \<and> AllowGrantReply \<notin> x43) = (cap_aligned (NotificationCap x41 x42 x43) \<and> AllowGrant \<notin> x43 \<and> AllowGrantReply \<notin> x43 \<and> ntfn_at x41 s)
 3. \<And>x51 x52 x53. c = ReplyCap x51 x52 x53 \<Longrightarrow> (cap_aligned (ReplyCap x51 x52 x53) \<and> tcb_at x51 s \<and> AllowWrite \<in> x53 \<and> AllowRead \<notin> x53 \<and> AllowGrantReply \<notin> x53) = (cap_aligned (ReplyCap x51 x52 x53) \<and> AllowWrite \<in> x53 \<and> AllowRead \<notin> x53 \<and> AllowGrantReply \<notin> x53 \<and> tcb_at x51 s)
 4. \<And>x61 x62 x63. c = CNodeCap x61 x62 x63 \<Longrightarrow> (cap_aligned (CNodeCap x61 x62 x63) \<and> cap_table_at x62 x61 s \<and> 0 < x62 \<and> length x63 \<le> word_bits) = (cap_aligned (CNodeCap x61 x62 x63) \<and> 0 < x62 \<and> length x63 \<le> word_bits \<and> cap_table_at x62 x61 s)
 5. \<And>x111 x112 x113. c = Zombie x111 x112 x113 \<Longrightarrow> (x112 = None \<longrightarrow> (cap_aligned (Zombie x111 None x113) \<and> tcb_at x111 s \<and> x113 \<le> 5) = (cap_aligned (Zombie x111 None x113) \<and> x113 \<le> 5 \<and> tcb_at x111 s)) \<and> (\<forall>x2. x112 = Some x2 \<longrightarrow> (cap_aligned (Zombie x111 (Some x2) x113) \<and> cap_table_at x2 x111 s \<and> x113 \<le> 2 ^ x2 \<and> 0 < x2) = (cap_aligned (Zombie x111 (Some x2) x113) \<and> x113 \<le> 2 ^ x2 \<and> 0 < x2 \<and> cap_table_at x2 x111 s))
 6. \<And>x12. c = ArchObjectCap x12 \<Longrightarrow> (cap_aligned (ArchObjectCap x12) \<and> valid_arch_cap x12 s) = (cap_aligned (ArchObjectCap x12) \<and> wellformed_acap x12 \<and> valid_arch_cap_ref x12 s) proof (prove)
goal (1 subgoal):
 1. \<And>x12. c = ArchObjectCap x12 \<Longrightarrow> (cap_aligned (ArchObjectCap x12) \<and> valid_arch_cap x12 s) = (cap_aligned (ArchObjectCap x12) \<and> wellformed_acap x12 \<and> valid_arch_cap_ref x12 s)