kings-crown/FVELER_Isabelle huggingface dataset:
theory Access_AC

lemma aag_wellformed_all_auth_is_owns':
  "\<lbrakk> Control \<in> S; pas_wellformed aag \<rbrakk>
     \<Longrightarrow> (\<forall>auth \<in> S. aag_has_auth_to aag auth x) = (is_subject aag x)" by (fastforce simp: aag_wellformed_refl dest: aag_wellformed_Control)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Control \<in> S; pas_wellformed aag\<rbrakk> \<Longrightarrow> (\<forall>auth\<in>S. (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag) = is_subject aag x
theory Access_AC

lemma pas_refined_sita_mem:
  "\<lbrakk> (x, auth, y) \<in> state_irqs_to_policy aag s; pas_refined aag s \<rbrakk>
     \<Longrightarrow> (x, auth, y) \<in> pasPolicy aag" by (auto simp: pas_refined_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(x, auth, y) \<in> state_irqs_to_policy aag s; pas_refined aag s\<rbrakk> \<Longrightarrow> (x, auth, y) \<in> pasPolicy aag
theory Access_AC

lemma receive_blocked_on_can_receive_ipc'[elim!,simp]:
  "case_option False (receive_blocked_on ref) tsopt \<Longrightarrow> case_option False can_receive_ipc tsopt" by (cases tsopt;simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. case tsopt of None \<Rightarrow> False | Some x \<Rightarrow> receive_blocked_on ref x \<Longrightarrow> case tsopt of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x
theory Access_AC

lemma tcb_bound_notification_reset_integrity_refl[simp]:
  "tcb_bound_notification_reset_integrity ntfn ntfn subjects aag" by (simp add: tcb_bound_notification_reset_integrity_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_bound_notification_reset_integrity ntfn ntfn subjects aag
theory Access_AC

lemma allowed_call_blocked_call_blocked[elim!]:
  "allowed_call_blocked ep tst \<Longrightarrow> call_blocked ep tst" unfolding allowed_call_blocked_def call_blocked_def by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. allowed_call_blocked ep tst \<Longrightarrow> call_blocked ep tst proof (prove)
goal (1 subgoal):
 1. \<exists>pl. tst = BlockedOnSend ep pl \<and> sender_is_call pl \<and> (sender_can_grant pl \<or> sender_can_grant_reply pl) \<Longrightarrow> \<exists>pl. tst = BlockedOnSend ep pl \<and> sender_is_call pl
theory Access_AC

lemma reply_cap_deletion_integrityE:
  assumes hyp: "reply_cap_deletion_integrity subjects aag cap cap'"
  obtains "cap = cap'" | caller R where "cap = ReplyCap caller False R"
  and "cap' = NullCap" and "pasObjectAbs aag caller \<in> subjects" using hyp reply_cap_deletion_integrity_def by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap = cap' \<Longrightarrow> thesis; \<And>caller R. \<lbrakk>cap = ReplyCap caller False R; cap' = NullCap; pasObjectAbs aag caller \<in> subjects\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis proof (prove)
using this:
reply_cap_deletion_integrity subjects aag cap cap'
reply_cap_deletion_integrity ?subjects ?aag ?cap ?cap' \<equiv> ?cap = ?cap' \<or> (\<exists>caller R. ?cap = ReplyCap caller False R \<and> ?cap' = NullCap \<and> pasObjectAbs ?aag caller \<in> ?subjects)

goal (1 subgoal):
 1. \<lbrakk>cap = cap' \<Longrightarrow> thesis; \<And>caller R. \<lbrakk>cap = ReplyCap caller False R; cap' = NullCap; pasObjectAbs aag caller \<in> subjects\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
theory Access_AC

lemma reply_cap_deletion_integrity_refl[simp]:
  "reply_cap_deletion_integrity subjects aag cap cap" by (rule reply_cap_deletion_integrityI1) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reply_cap_deletion_integrity subjects aag cap cap
theory Access_AC

lemma cnode_integrityE:
  assumes hyp:"cnode_integrity subjects aag content content'"
  obtains "content l = content' l" | cap cap' where "content l = Some cap"
  and "content' l = Some cap'" and "reply_cap_deletion_integrity subjects aag cap cap'" using hyp cnode_integrityD by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>content l = content' l \<Longrightarrow> thesis; \<And>cap cap'. \<lbrakk>content l = Some cap; content' l = Some cap'; reply_cap_deletion_integrity subjects aag cap cap'\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis proof (prove)
using this:
cnode_integrity subjects aag content content'
cnode_integrity ?subjects ?aag ?content ?content' \<Longrightarrow> ?content ?l = ?content' ?l \<or> (\<exists>cap cap'. ?content ?l = Some cap \<and> ?content' ?l = Some cap' \<and> reply_cap_deletion_integrity ?subjects ?aag cap cap')

goal (1 subgoal):
 1. \<lbrakk>content l = content' l \<Longrightarrow> thesis; \<And>cap cap'. \<lbrakk>content l = Some cap; content' l = Some cap'; reply_cap_deletion_integrity subjects aag cap cap'\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
theory Access_AC

lemma troa_tro:
  "integrity_obj_atomic aag activate subjects l ko ko'
    \<Longrightarrow> integrity_obj aag activate subjects l ko ko'" unfolding integrity_obj_def by (rule r_into_rtranclp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. integrity_obj_atomic aag activate subjects l ko ko' \<Longrightarrow> integrity_obj aag activate subjects l ko ko' proof (prove)
goal (1 subgoal):
 1. integrity_obj_atomic aag activate subjects l ko ko' \<Longrightarrow> (integrity_obj_atomic aag activate subjects l)\<^sup>*\<^sup>* ko ko'
theory Access_AC

lemma tro_tcb_unbind':
  "\<lbrakk> ko = Some (TCB tcb); ko' = Some (TCB tcb');
     tcb' = tcb\<lparr>tcb_bound_notification := ntfn'\<rparr>;
     tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' subjects aag \<rbrakk>
     \<Longrightarrow> integrity_obj aag activate subjects l' ko ko'" apply (clarsimp simp:tcb_bound_notification_reset_integrity_def) apply (elim disjE) apply (rule tro_orefl;fastforce) apply (rule tro_tcb_unbind;fastforce) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko = Some (TCB tcb); ko' = Some (TCB tcb'); tcb' = tcb\<lparr>tcb_bound_notification := ntfn'\<rparr>; tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' subjects aag\<rbrakk> \<Longrightarrow> integrity_obj aag activate subjects l' ko ko' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko = Some (TCB tcb); ko' = Some (TCB (tcb\<lparr>tcb_bound_notification := ntfn'\<rparr>)); tcb' = tcb\<lparr>tcb_bound_notification := ntfn'\<rparr>; tcb_bound_notification tcb = ntfn' \<or> ntfn' = None \<and> aag_subjects_have_auth_to subjects aag Reset (the (tcb_bound_notification tcb))\<rbrakk> \<Longrightarrow> integrity_obj aag activate subjects l' (Some (TCB tcb)) (Some (TCB (tcb\<lparr>tcb_bound_notification := ntfn'\<rparr>))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ko = Some (TCB tcb); ko' = Some (TCB (tcb\<lparr>tcb_bound_notification := ntfn'\<rparr>)); tcb' = tcb\<lparr>tcb_bound_notification := ntfn'\<rparr>; tcb_bound_notification tcb = ntfn'\<rbrakk> \<Longrightarrow> integrity_obj aag activate subjects l' (Some (TCB tcb)) (Some (TCB (tcb\<lparr>tcb_bound_notification := ntfn'\<rparr>)))
 2. \<lbrakk>ko = Some (TCB tcb); ko' = Some (TCB (tcb\<lparr>tcb_bound_notification := ntfn'\<rparr>)); tcb' = tcb\<lparr>tcb_bound_notification := ntfn'\<rparr>; ntfn' = None \<and> aag_subjects_have_auth_to subjects aag Reset (the (tcb_bound_notification tcb))\<rbrakk> \<Longrightarrow> integrity_obj aag activate subjects l' (Some (TCB tcb)) (Some (TCB (tcb\<lparr>tcb_bound_notification := ntfn'\<rparr>))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko = Some (TCB tcb); ko' = Some (TCB (tcb\<lparr>tcb_bound_notification := ntfn'\<rparr>)); tcb' = tcb\<lparr>tcb_bound_notification := ntfn'\<rparr>; ntfn' = None \<and> aag_subjects_have_auth_to subjects aag Reset (the (tcb_bound_notification tcb))\<rbrakk> \<Longrightarrow> integrity_obj aag activate subjects l' (Some (TCB tcb)) (Some (TCB (tcb\<lparr>tcb_bound_notification := ntfn'\<rparr>))) proof (prove)
goal:
No subgoals!
theory Access_AC

lemma integrity_ready_queues_refl[simp]: "integrity_ready_queues aag subjects ptr s s" unfolding integrity_ready_queues_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. integrity_ready_queues aag subjects ptr s s proof (prove)
goal (1 subgoal):
 1. pasMayEditReadyQueues aag \<or> (ptr \<inter> subjects = {} \<longrightarrow> (\<exists>threads. threads @ s = s))
theory Access_AC

lemma caps_of_state_tcb_cap_cases:
  "\<lbrakk> get_tcb p s = Some tcb; idx \<in> dom tcb_cap_cases \<rbrakk>
     \<Longrightarrow> caps_of_state s (p, idx) = Some ((the (option_map fst (tcb_cap_cases idx))) tcb)" apply (clarsimp simp: dom_def) apply (erule caps_of_state_tcb') apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>get_tcb p s = Some tcb; idx \<in> dom tcb_cap_cases\<rbrakk> \<Longrightarrow> caps_of_state s (p, idx) = Some (the (map_option fst (tcb_cap_cases idx)) tcb) proof (prove)
goal (1 subgoal):
 1. \<And>a aa b. \<lbrakk>get_tcb p s = Some tcb; tcb_cap_cases idx = Some (a, aa, b)\<rbrakk> \<Longrightarrow> caps_of_state s (p, idx) = Some (a tcb) proof (prove)
goal (1 subgoal):
 1. \<And>a aa b. tcb_cap_cases idx = Some (a, aa, b) \<Longrightarrow> map_option fst (tcb_cap_cases idx) = Some a proof (prove)
goal:
No subgoals!
theory Access_AC

lemma cdt_change_allowedI:
  "\<lbrakk> m \<Turnstile> pptr \<rightarrow>* ptr; cdt_direct_change_allowed aag subjects tcbsts pptr \<rbrakk>
     \<Longrightarrow> cdt_change_allowed aag subjects m tcbsts ptr" by (fastforce simp: cdt_change_allowed_def simp del: split_paired_Ex)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<Turnstile> pptr \<rightarrow>* ptr; cdt_direct_change_allowed aag subjects tcbsts pptr\<rbrakk> \<Longrightarrow> cdt_change_allowed aag subjects m tcbsts ptr
theory Access_AC

lemma cdt_change_allowedE:
  assumes "cdt_change_allowed aag subjects m tcbsts ptr"
  obtains pptr where "m \<Turnstile> pptr \<rightarrow>* ptr" "cdt_direct_change_allowed aag subjects tcbsts pptr" using assms by (fastforce simp: cdt_change_allowed_def simp del: split_paired_Ex)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>pptr. \<lbrakk>m \<Turnstile> pptr \<rightarrow>* ptr; cdt_direct_change_allowed aag subjects tcbsts pptr\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (prove)
using this:
cdt_change_allowed aag subjects m tcbsts ptr

goal (1 subgoal):
 1. (\<And>pptr. \<lbrakk>m \<Turnstile> pptr \<rightarrow>* ptr; cdt_direct_change_allowed aag subjects tcbsts pptr\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
theory Access_AC

lemma cca_direct_single[intro]:
  "is_subject aag (fst ptr) \<Longrightarrow> cdt_change_allowed aag {pasSubject aag} m kh ptr" by (rule cca_direct) blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_subject aag (fst ptr) \<Longrightarrow> cdt_change_allowed aag {pasSubject aag} m kh ptr
theory Access_AC

lemma integrity_cdtE:
  assumes hyp:"integrity_cdt aag subjects m tcbsts ptr v v'"
  obtains "v = v'" | "cdt_change_allowed aag subjects m tcbsts ptr" using hyp integrity_cdt_def by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>v = v' \<Longrightarrow> thesis; cdt_change_allowed aag subjects m tcbsts ptr \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis proof (prove)
using this:
integrity_cdt aag subjects m tcbsts ptr v v'
integrity_cdt ?aag ?subjects ?m ?tcbsts ?ptr ?v ?v' \<equiv> ?v = ?v' \<or> cdt_change_allowed ?aag ?subjects ?m ?tcbsts ?ptr

goal (1 subgoal):
 1. \<lbrakk>v = v' \<Longrightarrow> thesis; cdt_change_allowed aag subjects m tcbsts ptr \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
theory Access_AC

lemma integrity_cdt_refl[simp]: "integrity_cdt aag subjects m kh ptr v v" by (simp add: integrity_cdt_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. integrity_cdt aag subjects m kh ptr v v
theory Access_AC

lemma integrity_cdt_change_allowed[simp,intro]:
  "cdt_change_allowed aag subjects m kh ptr \<Longrightarrow> integrity_cdt aag subjects m kh ptr v v'" by (simp add: integrity_cdt_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cdt_change_allowed aag subjects m kh ptr \<Longrightarrow> integrity_cdt aag subjects m kh ptr v v'
theory Access_AC

lemma integrity_cdt_list_refl[simp]: "integrity_cdt_list aag subjects m kh ptr v v" by (simp add: integrity_cdt_list_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. integrity_cdt_list aag subjects m kh ptr v v
theory Access_AC

lemma integrity_cdt_list_filt:
  "filtered_eq (cdt_change_allowed aag subjects m kh) l l'
   \<Longrightarrow> integrity_cdt_list aag subjects m kh ptr l l'" by (simp add: integrity_cdt_list_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. filtered_eq (cdt_change_allowed aag subjects m kh) l l' \<Longrightarrow> integrity_cdt_list aag subjects m kh ptr l l'
theory Access_AC

lemma integrity_cdt_list_change_allowed:
  "cdt_change_allowed aag subjects m kh ptr \<Longrightarrow> integrity_cdt_list aag subjects m kh ptr l l'" by (simp add: integrity_cdt_list_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cdt_change_allowed aag subjects m kh ptr \<Longrightarrow> integrity_cdt_list aag subjects m kh ptr l l'
theory Access_AC

lemma integrity_cdt_listE:
  assumes hyp:"integrity_cdt_list aag subjects m kh ptr l l'"
  obtains "filtered_eq (cdt_change_allowed aag subjects m kh) l l'" |
          "cdt_change_allowed aag subjects m kh ptr" using hyp integrity_cdt_list_def by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>filtered_eq (cdt_change_allowed aag subjects m kh) l l' \<Longrightarrow> thesis; cdt_change_allowed aag subjects m kh ptr \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis proof (prove)
using this:
integrity_cdt_list aag subjects m kh ptr l l'
integrity_cdt_list ?aag ?subjects ?m ?tcbsts ?ptr ?l ?l' \<equiv> filtered_eq (cdt_change_allowed ?aag ?subjects ?m ?tcbsts) ?l ?l' \<or> cdt_change_allowed ?aag ?subjects ?m ?tcbsts ?ptr

goal (1 subgoal):
 1. \<lbrakk>filtered_eq (cdt_change_allowed aag subjects m kh) l l' \<Longrightarrow> thesis; cdt_change_allowed aag subjects m kh ptr \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
theory Access_AC

lemma integrity_interrupts_refl[simp]: "integrity_interrupts aag subjects ptr v v" by (simp add: integrity_interrupts_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. integrity_interrupts aag subjects ptr v v
theory Access_AC

lemma tcb_bound_notification_reset_integrity_trans[elim]:
  "\<lbrakk> tcb_bound_notification_reset_integrity ntfn ntfn' subjects aag;
     tcb_bound_notification_reset_integrity ntfn' ntfn'' subjects aag \<rbrakk>
     \<Longrightarrow> tcb_bound_notification_reset_integrity ntfn ntfn'' subjects aag" by (auto simp: tcb_bound_notification_reset_integrity_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_bound_notification_reset_integrity ntfn ntfn' subjects aag; tcb_bound_notification_reset_integrity ntfn' ntfn'' subjects aag\<rbrakk> \<Longrightarrow> tcb_bound_notification_reset_integrity ntfn ntfn'' subjects aag
theory Access_AC

lemma reply_cap_deletion_integrity_trans[elim]:
  "\<lbrakk> reply_cap_deletion_integrity subjects aag cap cap';
     reply_cap_deletion_integrity subjects aag cap' cap'' \<rbrakk>
     \<Longrightarrow> reply_cap_deletion_integrity subjects aag cap cap''" by (auto simp: reply_cap_deletion_integrity_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reply_cap_deletion_integrity subjects aag cap cap'; reply_cap_deletion_integrity subjects aag cap' cap''\<rbrakk> \<Longrightarrow> reply_cap_deletion_integrity subjects aag cap cap''
theory Access_AC

lemma cnode_integrity_trans[elim]:
  "\<lbrakk> cnode_integrity subjects aag cont cont';
     cnode_integrity subjects aag cont' cont'' \<rbrakk>
     \<Longrightarrow> cnode_integrity subjects aag cont cont''" unfolding cnode_integrity_def apply (intro allI) apply (drule_tac x=l in spec)+ by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cnode_integrity subjects aag cont cont'; cnode_integrity subjects aag cont' cont''\<rbrakk> \<Longrightarrow> cnode_integrity subjects aag cont cont'' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>l. cont l = cont' l \<or> (\<exists>cap cap'. cont l = Some cap \<and> cont' l = Some cap' \<and> reply_cap_deletion_integrity subjects aag cap cap'); \<forall>l. cont' l = cont'' l \<or> (\<exists>cap cap'. cont' l = Some cap \<and> cont'' l = Some cap' \<and> reply_cap_deletion_integrity subjects aag cap cap')\<rbrakk> \<Longrightarrow> \<forall>l. cont l = cont'' l \<or> (\<exists>cap cap'. cont l = Some cap \<and> cont'' l = Some cap' \<and> reply_cap_deletion_integrity subjects aag cap cap') proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>\<forall>l. cont l = cont' l \<or> (\<exists>cap cap'. cont l = Some cap \<and> cont' l = Some cap' \<and> reply_cap_deletion_integrity subjects aag cap cap'); \<forall>l. cont' l = cont'' l \<or> (\<exists>cap cap'. cont' l = Some cap \<and> cont'' l = Some cap' \<and> reply_cap_deletion_integrity subjects aag cap cap')\<rbrakk> \<Longrightarrow> cont l = cont'' l \<or> (\<exists>cap cap'. cont l = Some cap \<and> cont'' l = Some cap' \<and> reply_cap_deletion_integrity subjects aag cap cap') proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>cont l = cont' l \<or> (\<exists>cap cap'. cont l = Some cap \<and> cont' l = Some cap' \<and> reply_cap_deletion_integrity subjects aag cap cap'); cont' l = cont'' l \<or> (\<exists>cap cap'. cont' l = Some cap \<and> cont'' l = Some cap' \<and> reply_cap_deletion_integrity subjects aag cap cap')\<rbrakk> \<Longrightarrow> cont l = cont'' l \<or> (\<exists>cap cap'. cont l = Some cap \<and> cont'' l = Some cap' \<and> reply_cap_deletion_integrity subjects aag cap cap')
theory Access_AC

lemma tcb_bound_notification_reset_eq_or_none:
  "tcb_bound_notification_reset_integrity ntfn ntfn' subjects aag \<Longrightarrow> ntfn = ntfn' \<or> ntfn' = None" by (auto simp: tcb_bound_notification_reset_integrity_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_bound_notification_reset_integrity ntfn ntfn' subjects aag \<Longrightarrow> ntfn = ntfn' \<or> ntfn' = None
theory Access_AC

lemma tro_alt_transp[intro!]:
  "transp (integrity_obj_alt (aag :: 'a PAS) activate es subjects)" by (rule transpI) (rule tro_alt_trans_spec)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. transp (integrity_obj_alt aag activate es subjects)
theory Access_AC

lemma tro_alt_reflp[intro!]:
  "reflp (integrity_obj_alt aag activate es subjects)" by (rule reflpI) (rule tro_alt_orefl; blast)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reflp (integrity_obj_alt aag activate es subjects)
theory Access_AC

lemma tro_tro_alt[elim!]:
  "integrity_obj aag activate es subjects ko ko'
  \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko'" unfolding integrity_obj_def by (subst rtranclp_id[symmetric]; fastforce elim: rtranclp_mono[THEN predicate2D,rotated])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. integrity_obj aag activate es subjects ko ko' \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko' proof (prove)
goal (1 subgoal):
 1. (integrity_obj_atomic aag activate es subjects)\<^sup>*\<^sup>* ko ko' \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko'
theory Access_AC

lemma tro_trans:
  "\<lbrakk> integrity_obj_state aag activate es s s'; integrity_obj_state aag activate es s' s'' \<rbrakk>
     \<Longrightarrow> integrity_obj_state aag activate es s s''" unfolding integrity_obj_def apply clarsimp apply (drule_tac x = x in spec)+ by force

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>integrity_obj_state aag activate es s s'; integrity_obj_state aag activate es s' s''\<rbrakk> \<Longrightarrow> integrity_obj_state aag activate es s s'' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x. (integrity_obj_atomic aag activate es (pasObjectAbs aag x))\<^sup>*\<^sup>* (kheap s x) (kheap s' x); \<forall>x. (integrity_obj_atomic aag activate es (pasObjectAbs aag x))\<^sup>*\<^sup>* (kheap s' x) (kheap s'' x)\<rbrakk> \<Longrightarrow> \<forall>x. (integrity_obj_atomic aag activate es (pasObjectAbs aag x))\<^sup>*\<^sup>* (kheap s x) (kheap s'' x) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>x. (integrity_obj_atomic aag activate es (pasObjectAbs aag x))\<^sup>*\<^sup>* (kheap s x) (kheap s' x); \<forall>x. (integrity_obj_atomic aag activate es (pasObjectAbs aag x))\<^sup>*\<^sup>* (kheap s' x) (kheap s'' x)\<rbrakk> \<Longrightarrow> (integrity_obj_atomic aag activate es (pasObjectAbs aag x))\<^sup>*\<^sup>* (kheap s x) (kheap s'' x) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>(integrity_obj_atomic aag activate es (pasObjectAbs aag x))\<^sup>*\<^sup>* (kheap s x) (kheap s' x); (integrity_obj_atomic aag activate es (pasObjectAbs aag x))\<^sup>*\<^sup>* (kheap s' x) (kheap s'' x)\<rbrakk> \<Longrightarrow> (integrity_obj_atomic aag activate es (pasObjectAbs aag x))\<^sup>*\<^sup>* (kheap s x) (kheap s'' x)
theory Access_AC

lemma tcb_states_of_state_kheap:
   "\<lbrakk> kheap s slot = Some (TCB tcb)\<rbrakk>
      \<Longrightarrow> tcb_states_of_state s slot = Some (tcb_state tcb)" by (simp add:tcb_states_of_state_def get_tcb_def split: option.splits kernel_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. kheap s slot = Some (TCB tcb) \<Longrightarrow> tcb_states_of_state s slot = Some (tcb_state tcb)
theory Access_AC

lemma tcb_states_of_state_kheapI:
   "\<lbrakk> kheap s slot = Some (TCB tcb); tcb_state tcb = tcbst \<rbrakk>
      \<Longrightarrow> tcb_states_of_state s slot = Some tcbst" by (simp add: tcb_states_of_state_def get_tcb_def split: option.splits kernel_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s slot = Some (TCB tcb); tcb_state tcb = tcbst\<rbrakk> \<Longrightarrow> tcb_states_of_state s slot = Some tcbst
theory Access_AC

lemma tcb_states_of_state_kheapD:
  "tcb_states_of_state s slot = Some tcbst \<Longrightarrow>
   \<exists>tcb. kheap s slot = Some (TCB tcb) \<and> tcb_state tcb = tcbst" by (simp add:tcb_states_of_state_def get_tcb_def split: option.splits kernel_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_states_of_state s slot = Some tcbst \<Longrightarrow> \<exists>tcb. kheap s slot = Some (TCB tcb) \<and> tcb_state tcb = tcbst
theory Access_AC

lemma tcb_states_of_state_kheapE:
  assumes "tcb_states_of_state s slot = Some tcbst"
  obtains tcb where "kheap s slot = Some (TCB tcb)" "tcb_state tcb = tcbst" using assms tcb_states_of_state_kheapD by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>tcb. \<lbrakk>kheap s slot = Some (TCB tcb); tcb_state tcb = tcbst\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (prove)
using this:
tcb_states_of_state s slot = Some tcbst
tcb_states_of_state ?s ?slot = Some ?tcbst \<Longrightarrow> \<exists>tcb. kheap ?s ?slot = Some (TCB tcb) \<and> tcb_state tcb = ?tcbst

goal (1 subgoal):
 1. (\<And>tcb. \<lbrakk>kheap s slot = Some (TCB tcb); tcb_state tcb = tcbst\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis