theory Access_AC

lemma trcdt_trans:
  "\<lbrakk> integrity_cdt_state aag subjects s s' ;
     integrity_obj_state aag activate subjects s s' ;
     integrity_cdt_state aag subjects s' s'' \<rbrakk>
     \<Longrightarrow> integrity_cdt_state aag subjects s s''" apply (intro allI) apply (frule_tac x=x in spec) apply (frule_tac x=x in spec[where P = "\<lambda>x. integrity_cdt _ _ (cdt s') _ x (_ x) (_ x)"]) apply (erule integrity_cdtE)+ apply simp by (blast dest: cdt_change_allowed_backward)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>integrity_cdt_state aag subjects s s'; integrity_obj_state aag activate subjects s s'; integrity_cdt_state aag subjects s' s''\<rbrakk> \<Longrightarrow> integrity_cdt_state aag subjects s s'' proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>integrity_cdt_state aag subjects s s'; integrity_obj_state aag activate subjects s s'; integrity_cdt_state aag subjects s' s''\<rbrakk> \<Longrightarrow> integrity_cdt aag subjects (cdt s) (tcb_states_of_state s) x (cdt s x, is_original_cap s x) (cdt s'' x, is_original_cap s'' x) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>integrity_cdt_state aag subjects s s'; integrity_obj_state aag activate subjects s s'; integrity_cdt_state aag subjects s' s''; integrity_cdt aag subjects (cdt s) (tcb_states_of_state s) x (cdt s x, is_original_cap s x) (cdt s' x, is_original_cap s' x)\<rbrakk> \<Longrightarrow> integrity_cdt aag subjects (cdt s) (tcb_states_of_state s) x (cdt s x, is_original_cap s x) (cdt s'' x, is_original_cap s'' x) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>integrity_cdt_state aag subjects s s'; integrity_obj_state aag activate subjects s s'; integrity_cdt_state aag subjects s' s''; integrity_cdt aag subjects (cdt s) (tcb_states_of_state s) x (cdt s x, is_original_cap s x) (cdt s' x, is_original_cap s' x); integrity_cdt aag subjects (cdt s') (tcb_states_of_state s') x (cdt s' x, is_original_cap s' x) (cdt s'' x, is_original_cap s'' x)\<rbrakk> \<Longrightarrow> integrity_cdt aag subjects (cdt s) (tcb_states_of_state s) x (cdt s x, is_original_cap s x) (cdt s'' x, is_original_cap s'' x) proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>integrity_cdt_state aag subjects s s'; integrity_obj_state aag activate subjects s s'; integrity_cdt_state aag subjects s' s''; (cdt s x, is_original_cap s x) = (cdt s' x, is_original_cap s' x); (cdt s' x, is_original_cap s' x) = (cdt s'' x, is_original_cap s'' x)\<rbrakk> \<Longrightarrow> integrity_cdt aag subjects (cdt s) (tcb_states_of_state s) x (cdt s x, is_original_cap s x) (cdt s'' x, is_original_cap s'' x)
 2. \<And>x. \<lbrakk>integrity_cdt_state aag subjects s s'; integrity_obj_state aag activate subjects s s'; integrity_cdt_state aag subjects s' s''; (cdt s x, is_original_cap s x) = (cdt s' x, is_original_cap s' x); cdt_change_allowed aag subjects (cdt s') (tcb_states_of_state s') x\<rbrakk> \<Longrightarrow> integrity_cdt aag subjects (cdt s) (tcb_states_of_state s) x (cdt s x, is_original_cap s x) (cdt s'' x, is_original_cap s'' x)
 3. \<And>x. \<lbrakk>integrity_cdt_state aag subjects s s'; integrity_obj_state aag activate subjects s s'; integrity_cdt_state aag subjects s' s''; integrity_cdt aag subjects (cdt s') (tcb_states_of_state s') x (cdt s' x, is_original_cap s' x) (cdt s'' x, is_original_cap s'' x); cdt_change_allowed aag subjects (cdt s) (tcb_states_of_state s) x\<rbrakk> \<Longrightarrow> integrity_cdt aag subjects (cdt s) (tcb_states_of_state s) x (cdt s x, is_original_cap s x) (cdt s'' x, is_original_cap s'' x) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>integrity_cdt_state aag subjects s s'; integrity_obj_state aag activate subjects s s'; integrity_cdt_state aag subjects s' s''; (cdt s x, is_original_cap s x) = (cdt s' x, is_original_cap s' x); cdt_change_allowed aag subjects (cdt s') (tcb_states_of_state s') x\<rbrakk> \<Longrightarrow> integrity_cdt aag subjects (cdt s) (tcb_states_of_state s) x (cdt s x, is_original_cap s x) (cdt s'' x, is_original_cap s'' x)
 2. \<And>x. \<lbrakk>integrity_cdt_state aag subjects s s'; integrity_obj_state aag activate subjects s s'; integrity_cdt_state aag subjects s' s''; integrity_cdt aag subjects (cdt s') (tcb_states_of_state s') x (cdt s' x, is_original_cap s' x) (cdt s'' x, is_original_cap s'' x); cdt_change_allowed aag subjects (cdt s) (tcb_states_of_state s) x\<rbrakk> \<Longrightarrow> integrity_cdt aag subjects (cdt s) (tcb_states_of_state s) x (cdt s x, is_original_cap s x) (cdt s'' x, is_original_cap s'' x)