theory Access_AC

lemma pas_refined_all_children':
  "\<lbrakk> valid_mdb s; pas_refined aag s; m = (cdt s) \<rbrakk>
     \<Longrightarrow> all_children (\<lambda>x. is_subject aag (fst x) \<or> is_transferable (caps_of_state s x)) m" apply (rule all_childrenI) apply (erule disjE) apply (simp add: pas_refined_def,elim conjE) apply (rule disjCI) apply (subgoal_tac "abs_has_auth_to aag Control (fst p) (fst c)") apply (fastforce elim: aag_wellformed_control_is_owns[THEN iffD1]) apply (simp add: state_objs_to_policy_def auth_graph_map_def) apply (erule set_mp) apply (frule(1) sbta_cdt) apply force apply (rule disjI2) by (rule is_transferable_all_children[THEN all_childrenD]; solves \<open>simp\<close>)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_mdb s; pas_refined aag s; m = cdt s\<rbrakk> \<Longrightarrow> all_children (\<lambda>x. is_subject aag (fst x) \<or> is_transferable_in x s) m proof (prove)
goal (1 subgoal):
 1. \<And>c p. \<lbrakk>valid_mdb s; pas_refined aag s; m = cdt s; m c = Some p; is_subject aag (fst p) \<or> is_transferable_in p s\<rbrakk> \<Longrightarrow> is_subject aag (fst c) \<or> is_transferable_in c s proof (prove)
goal (2 subgoals):
 1. \<And>c p. \<lbrakk>valid_mdb s; pas_refined aag s; m = cdt s; m c = Some p; is_subject aag (fst p)\<rbrakk> \<Longrightarrow> is_subject aag (fst c) \<or> is_transferable_in c s
 2. \<And>c p. \<lbrakk>valid_mdb s; pas_refined aag s; m = cdt s; m c = Some p; is_transferable_in p s\<rbrakk> \<Longrightarrow> is_subject aag (fst c) \<or> is_transferable_in c s proof (prove)
goal (2 subgoals):
 1. \<And>c p. \<lbrakk>valid_mdb s; m = cdt s; cdt s c = Some p; is_subject aag (fst p); pas_wellformed aag; irq_map_wellformed aag s; tcb_domain_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag\<rbrakk> \<Longrightarrow> is_subject aag (fst c) \<or> is_transferable_in c s
 2. \<And>c p. \<lbrakk>valid_mdb s; pas_refined aag s; m = cdt s; m c = Some p; is_transferable_in p s\<rbrakk> \<Longrightarrow> is_subject aag (fst c) \<or> is_transferable_in c s proof (prove)
goal (2 subgoals):
 1. \<And>c p. \<lbrakk>valid_mdb s; m = cdt s; cdt s c = Some p; is_subject aag (fst p); pas_wellformed aag; irq_map_wellformed aag s; tcb_domain_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; \<not> is_transferable_in c s\<rbrakk> \<Longrightarrow> is_subject aag (fst c)
 2. \<And>c p. \<lbrakk>valid_mdb s; pas_refined aag s; m = cdt s; m c = Some p; is_transferable_in p s\<rbrakk> \<Longrightarrow> is_subject aag (fst c) \<or> is_transferable_in c s proof (prove)
goal (3 subgoals):
 1. \<And>c p. \<lbrakk>valid_mdb s; m = cdt s; cdt s c = Some p; is_subject aag (fst p); pas_wellformed aag; irq_map_wellformed aag s; tcb_domain_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; \<not> is_transferable_in c s; (pasObjectAbs aag (fst p), Control, pasObjectAbs aag (fst c)) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> is_subject aag (fst c)
 2. \<And>c p. \<lbrakk>valid_mdb s; m = cdt s; cdt s c = Some p; is_subject aag (fst p); pas_wellformed aag; irq_map_wellformed aag s; tcb_domain_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; \<not> is_transferable_in c s\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (fst p), Control, pasObjectAbs aag (fst c)) \<in> pasPolicy aag
 3. \<And>c p. \<lbrakk>valid_mdb s; pas_refined aag s; m = cdt s; m c = Some p; is_transferable_in p s\<rbrakk> \<Longrightarrow> is_subject aag (fst c) \<or> is_transferable_in c s proof (prove)
goal (2 subgoals):
 1. \<And>c p. \<lbrakk>valid_mdb s; m = cdt s; cdt s c = Some p; is_subject aag (fst p); pas_wellformed aag; irq_map_wellformed aag s; tcb_domain_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; \<not> is_transferable_in c s\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (fst p), Control, pasObjectAbs aag (fst c)) \<in> pasPolicy aag
 2. \<And>c p. \<lbrakk>valid_mdb s; pas_refined aag s; m = cdt s; m c = Some p; is_transferable_in p s\<rbrakk> \<Longrightarrow> is_subject aag (fst c) \<or> is_transferable_in c s proof (prove)
goal (2 subgoals):
 1. \<And>c p. \<lbrakk>valid_mdb s; m = cdt s; cdt s c = Some p; is_subject aag (fst p); pas_wellformed aag; irq_map_wellformed aag s; tcb_domain_map_wellformed aag s; {(pasObjectAbs aag x, auth, pasObjectAbs aag y) |x auth y. (x, auth, y) \<in> state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s)} \<subseteq> pasPolicy aag; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; \<not> is_transferable_in c s\<rbrakk> \<Longrightarrow> (pasSubject aag, Control, pasObjectAbs aag (fst c)) \<in> pasPolicy aag
 2. \<And>c p. \<lbrakk>valid_mdb s; pas_refined aag s; m = cdt s; m c = Some p; is_transferable_in p s\<rbrakk> \<Longrightarrow> is_subject aag (fst c) \<or> is_transferable_in c s proof (prove)
goal (2 subgoals):
 1. \<And>c p. \<lbrakk>valid_mdb s; m = cdt s; cdt s c = Some p; is_subject aag (fst p); pas_wellformed aag; irq_map_wellformed aag s; tcb_domain_map_wellformed aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; \<not> is_transferable_in c s\<rbrakk> \<Longrightarrow> (pasSubject aag, Control, pasObjectAbs aag (fst c)) \<in> {(pasObjectAbs aag x, auth, pasObjectAbs aag y) |x auth y. (x, auth, y) \<in> state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s)}
 2. \<And>c p. \<lbrakk>valid_mdb s; pas_refined aag s; m = cdt s; m c = Some p; is_transferable_in p s\<rbrakk> \<Longrightarrow> is_subject aag (fst c) \<or> is_transferable_in c s proof (prove)
goal (2 subgoals):
 1. \<And>c p. \<lbrakk>valid_mdb s; m = cdt s; cdt s c = Some p; is_subject aag (fst p); pas_wellformed aag; irq_map_wellformed aag s; tcb_domain_map_wellformed aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; \<not> is_transferable_in c s; (fst p, Control, fst c) \<in> state_bits_to_policy (caps_of_state s) (?thread_sts23 c p) (?thread_bas23 c p) (cdt s) (?vrefs23 c p)\<rbrakk> \<Longrightarrow> (pasSubject aag, Control, pasObjectAbs aag (fst c)) \<in> {(pasObjectAbs aag x, auth, pasObjectAbs aag y) |x auth y. (x, auth, y) \<in> state_bits_to_policy (caps_of_state s) (thread_st_auth s) (thread_bound_ntfns s) (cdt s) (state_vrefs s)}
 2. \<And>c p. \<lbrakk>valid_mdb s; pas_refined aag s; m = cdt s; m c = Some p; is_transferable_in p s\<rbrakk> \<Longrightarrow> is_subject aag (fst c) \<or> is_transferable_in c s proof (prove)
goal (1 subgoal):
 1. \<And>c p. \<lbrakk>valid_mdb s; pas_refined aag s; m = cdt s; m c = Some p; is_transferable_in p s\<rbrakk> \<Longrightarrow> is_subject aag (fst c) \<or> is_transferable_in c s proof (prove)
goal (1 subgoal):
 1. \<And>c p. \<lbrakk>valid_mdb s; pas_refined aag s; m = cdt s; m c = Some p; is_transferable_in p s\<rbrakk> \<Longrightarrow> is_transferable_in c s