theory Access_AC

lemma trcdtlist_trans:
  "\<lbrakk> integrity_cdt_list_state aag subjects s s' ;
     integrity_obj_state aag activate subjects s s' ;
     integrity_cdt_state aag subjects s s' ;
     integrity_cdt_list_state aag subjects s' s'' \<rbrakk>
     \<Longrightarrow> integrity_cdt_list_state aag subjects s s''" apply (intro allI) apply (drule_tac x=x in spec [where P="\<lambda>ptr. integrity_cdt_list _ _ _ _ ptr (_ ptr) (_ ptr)"] )+ apply (erule integrity_cdt_listE)+ apply (rule integrity_cdt_list_filt) apply (simp del: split_paired_All split_paired_Ex) apply (erule weaken_filter_eq') by (blast intro: integrity_cdt_list_intros dest: cdt_change_allowed_backward)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>integrity_cdt_list_state aag subjects s s'; integrity_obj_state aag activate subjects s s'; integrity_cdt_state aag subjects s s'; integrity_cdt_list_state aag subjects s' s''\<rbrakk> \<Longrightarrow> integrity_cdt_list_state aag subjects s s'' proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>integrity_cdt_list_state aag subjects s s'; integrity_obj_state aag activate subjects s s'; integrity_cdt_state aag subjects s s'; integrity_cdt_list_state aag subjects s' s''\<rbrakk> \<Longrightarrow> integrity_cdt_list aag subjects (cdt s) (tcb_states_of_state s) x (cdt_list s x) (cdt_list s'' x) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>integrity_obj_state aag activate subjects s s'; integrity_cdt_state aag subjects s s'; integrity_cdt_list aag subjects (cdt s) (tcb_states_of_state s) x (cdt_list s x) (cdt_list s' x); integrity_cdt_list aag subjects (cdt s') (tcb_states_of_state s') x (cdt_list s' x) (cdt_list s'' x)\<rbrakk> \<Longrightarrow> integrity_cdt_list aag subjects (cdt s) (tcb_states_of_state s) x (cdt_list s x) (cdt_list s'' x) proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>integrity_obj_state aag activate subjects s s'; integrity_cdt_state aag subjects s s'; filtered_eq (cdt_change_allowed aag subjects (cdt s) (tcb_states_of_state s)) (cdt_list s x) (cdt_list s' x); filtered_eq (cdt_change_allowed aag subjects (cdt s') (tcb_states_of_state s')) (cdt_list s' x) (cdt_list s'' x)\<rbrakk> \<Longrightarrow> integrity_cdt_list aag subjects (cdt s) (tcb_states_of_state s) x (cdt_list s x) (cdt_list s'' x)
 2. \<And>x. \<lbrakk>integrity_obj_state aag activate subjects s s'; integrity_cdt_state aag subjects s s'; filtered_eq (cdt_change_allowed aag subjects (cdt s) (tcb_states_of_state s)) (cdt_list s x) (cdt_list s' x); cdt_change_allowed aag subjects (cdt s') (tcb_states_of_state s') x\<rbrakk> \<Longrightarrow> integrity_cdt_list aag subjects (cdt s) (tcb_states_of_state s) x (cdt_list s x) (cdt_list s'' x)
 3. \<And>x. \<lbrakk>integrity_obj_state aag activate subjects s s'; integrity_cdt_state aag subjects s s'; integrity_cdt_list aag subjects (cdt s') (tcb_states_of_state s') x (cdt_list s' x) (cdt_list s'' x); cdt_change_allowed aag subjects (cdt s) (tcb_states_of_state s) x\<rbrakk> \<Longrightarrow> integrity_cdt_list aag subjects (cdt s) (tcb_states_of_state s) x (cdt_list s x) (cdt_list s'' x) proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>integrity_obj_state aag activate subjects s s'; integrity_cdt_state aag subjects s s'; filtered_eq (cdt_change_allowed aag subjects (cdt s) (tcb_states_of_state s)) (cdt_list s x) (cdt_list s' x); filtered_eq (cdt_change_allowed aag subjects (cdt s') (tcb_states_of_state s')) (cdt_list s' x) (cdt_list s'' x)\<rbrakk> \<Longrightarrow> filtered_eq (cdt_change_allowed aag subjects (cdt s) (tcb_states_of_state s)) (cdt_list s x) (cdt_list s'' x)
 2. \<And>x. \<lbrakk>integrity_obj_state aag activate subjects s s'; integrity_cdt_state aag subjects s s'; filtered_eq (cdt_change_allowed aag subjects (cdt s) (tcb_states_of_state s)) (cdt_list s x) (cdt_list s' x); cdt_change_allowed aag subjects (cdt s') (tcb_states_of_state s') x\<rbrakk> \<Longrightarrow> integrity_cdt_list aag subjects (cdt s) (tcb_states_of_state s) x (cdt_list s x) (cdt_list s'' x)
 3. \<And>x. \<lbrakk>integrity_obj_state aag activate subjects s s'; integrity_cdt_state aag subjects s s'; integrity_cdt_list aag subjects (cdt s') (tcb_states_of_state s') x (cdt_list s' x) (cdt_list s'' x); cdt_change_allowed aag subjects (cdt s) (tcb_states_of_state s) x\<rbrakk> \<Longrightarrow> integrity_cdt_list aag subjects (cdt s) (tcb_states_of_state s) x (cdt_list s x) (cdt_list s'' x) proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>integrity_obj_state aag activate subjects s s'; integrity_cdt_state aag subjects s s'; filtered_eq (cdt_change_allowed aag subjects (cdt s) (tcb_states_of_state s)) (cdt_list s x) (cdt_list s' x); filtered_eq (cdt_change_allowed aag subjects (cdt s') (tcb_states_of_state s')) (cdt_list s' x) (cdt_list s'' x)\<rbrakk> \<Longrightarrow> filtered_eq (cdt_change_allowed aag subjects (cdt s) (tcb_states_of_state s)) (cdt_list s' x) (cdt_list s'' x)
 2. \<And>x. \<lbrakk>integrity_obj_state aag activate subjects s s'; integrity_cdt_state aag subjects s s'; filtered_eq (cdt_change_allowed aag subjects (cdt s) (tcb_states_of_state s)) (cdt_list s x) (cdt_list s' x); cdt_change_allowed aag subjects (cdt s') (tcb_states_of_state s') x\<rbrakk> \<Longrightarrow> integrity_cdt_list aag subjects (cdt s) (tcb_states_of_state s) x (cdt_list s x) (cdt_list s'' x)
 3. \<And>x. \<lbrakk>integrity_obj_state aag activate subjects s s'; integrity_cdt_state aag subjects s s'; integrity_cdt_list aag subjects (cdt s') (tcb_states_of_state s') x (cdt_list s' x) (cdt_list s'' x); cdt_change_allowed aag subjects (cdt s) (tcb_states_of_state s) x\<rbrakk> \<Longrightarrow> integrity_cdt_list aag subjects (cdt s) (tcb_states_of_state s) x (cdt_list s x) (cdt_list s'' x) proof (prove)
goal (3 subgoals):
 1. \<And>x sa. \<lbrakk>integrity_obj_state aag activate subjects s s'; integrity_cdt_state aag subjects s s'; filtered_eq (cdt_change_allowed aag subjects (cdt s) (tcb_states_of_state s)) (cdt_list s x) (cdt_list s' x); cdt_change_allowed aag subjects (cdt s') (tcb_states_of_state s') sa\<rbrakk> \<Longrightarrow> cdt_change_allowed aag subjects (cdt s) (tcb_states_of_state s) sa
 2. \<And>x. \<lbrakk>integrity_obj_state aag activate subjects s s'; integrity_cdt_state aag subjects s s'; filtered_eq (cdt_change_allowed aag subjects (cdt s) (tcb_states_of_state s)) (cdt_list s x) (cdt_list s' x); cdt_change_allowed aag subjects (cdt s') (tcb_states_of_state s') x\<rbrakk> \<Longrightarrow> integrity_cdt_list aag subjects (cdt s) (tcb_states_of_state s) x (cdt_list s x) (cdt_list s'' x)
 3. \<And>x. \<lbrakk>integrity_obj_state aag activate subjects s s'; integrity_cdt_state aag subjects s s'; integrity_cdt_list aag subjects (cdt s') (tcb_states_of_state s') x (cdt_list s' x) (cdt_list s'' x); cdt_change_allowed aag subjects (cdt s) (tcb_states_of_state s) x\<rbrakk> \<Longrightarrow> integrity_cdt_list aag subjects (cdt s) (tcb_states_of_state s) x (cdt_list s x) (cdt_list s'' x)