theory Noninterference

lemma user_small_Step_partitionIntegrity:
  "\<lbrakk> ((a, b), x, aa, ba) \<in> check_active_irq_A_if;
     ct_running b; Invs b; ((aa, ba), y, ab, bb) \<in> do_user_op_A_if utf \<rbrakk>
     \<Longrightarrow> partitionIntegrity (current_aag b) b bb" apply (rule partitionIntegrity_trans'[rotated]) apply (rule do_user_op_A_if_partitionIntegrity) apply assumption apply (drule check_active_irq_A_if_result_state) apply simp apply (drule check_active_irq_A_if_result_state) apply (simp add: Invs_def current_aag_def) apply (rule check_active_irq_A_if_partitionIntegrity) apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>((a, b), x, aa, ba) \<in> check_active_irq_A_if; ct_running b; Invs b; ((aa, ba), y, ab, bb) \<in> do_user_op_A_if utf\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag b) b bb proof (prove)
goal (2 subgoals):
 1. \<lbrakk>((a, b), x, aa, ba) \<in> check_active_irq_A_if; ct_running b; Invs b; ((aa, ba), y, ab, bb) \<in> do_user_op_A_if utf\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag ?s') ?s' bb
 2. \<lbrakk>((a, b), x, aa, ba) \<in> check_active_irq_A_if; ct_running b; Invs b; ((aa, ba), y, ab, bb) \<in> do_user_op_A_if utf\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag b) b ?s' proof (prove)
goal (4 subgoals):
 1. \<lbrakk>((a, b), x, aa, ba) \<in> check_active_irq_A_if; ct_running b; Invs b; ((aa, ba), y, ab, bb) \<in> do_user_op_A_if utf\<rbrakk> \<Longrightarrow> ((?a3, ?s'), ?x3, ?aa3, bb) \<in> do_user_op_A_if ?uop3
 2. \<lbrakk>((a, b), x, aa, ba) \<in> check_active_irq_A_if; ct_running b; Invs b; ((aa, ba), y, ab, bb) \<in> do_user_op_A_if utf\<rbrakk> \<Longrightarrow> ct_running ?s'
 3. \<lbrakk>((a, b), x, aa, ba) \<in> check_active_irq_A_if; ct_running b; Invs b; ((aa, ba), y, ab, bb) \<in> do_user_op_A_if utf\<rbrakk> \<Longrightarrow> Invs ?s'
 4. \<lbrakk>((a, b), x, aa, ba) \<in> check_active_irq_A_if; ct_running b; Invs b; ((aa, ba), y, ab, bb) \<in> do_user_op_A_if utf\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag b) b ?s' proof (prove)
goal (3 subgoals):
 1. \<lbrakk>((a, b), x, aa, ba) \<in> check_active_irq_A_if; ct_running b; Invs b; ((aa, ba), y, ab, bb) \<in> do_user_op_A_if utf\<rbrakk> \<Longrightarrow> ct_running ba
 2. \<lbrakk>((a, b), x, aa, ba) \<in> check_active_irq_A_if; ct_running b; Invs b; ((aa, ba), y, ab, bb) \<in> do_user_op_A_if utf\<rbrakk> \<Longrightarrow> Invs ba
 3. \<lbrakk>((a, b), x, aa, ba) \<in> check_active_irq_A_if; ct_running b; Invs b; ((aa, ba), y, ab, bb) \<in> do_user_op_A_if utf\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag b) b ba proof (prove)
goal (3 subgoals):
 1. \<lbrakk>ct_running b; Invs b; ((aa, ba), y, ab, bb) \<in> do_user_op_A_if utf; ba = b\<lparr>machine_state := machine_state b\<lparr>irq_state := irq_state_of_state b + 1\<rparr>\<rparr>\<rbrakk> \<Longrightarrow> ct_running ba
 2. \<lbrakk>((a, b), x, aa, ba) \<in> check_active_irq_A_if; ct_running b; Invs b; ((aa, ba), y, ab, bb) \<in> do_user_op_A_if utf\<rbrakk> \<Longrightarrow> Invs ba
 3. \<lbrakk>((a, b), x, aa, ba) \<in> check_active_irq_A_if; ct_running b; Invs b; ((aa, ba), y, ab, bb) \<in> do_user_op_A_if utf\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag b) b ba proof (prove)
goal (2 subgoals):
 1. \<lbrakk>((a, b), x, aa, ba) \<in> check_active_irq_A_if; ct_running b; Invs b; ((aa, ba), y, ab, bb) \<in> do_user_op_A_if utf\<rbrakk> \<Longrightarrow> Invs ba
 2. \<lbrakk>((a, b), x, aa, ba) \<in> check_active_irq_A_if; ct_running b; Invs b; ((aa, ba), y, ab, bb) \<in> do_user_op_A_if utf\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag b) b ba proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ct_running b; Invs b; ((aa, ba), y, ab, bb) \<in> do_user_op_A_if utf; ba = b\<lparr>machine_state := machine_state b\<lparr>irq_state := irq_state_of_state b + 1\<rparr>\<rparr>\<rbrakk> \<Longrightarrow> Invs ba
 2. \<lbrakk>((a, b), x, aa, ba) \<in> check_active_irq_A_if; ct_running b; Invs b; ((aa, ba), y, ab, bb) \<in> do_user_op_A_if utf\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag b) b ba proof (prove)
goal (1 subgoal):
 1. \<lbrakk>((a, b), x, aa, ba) \<in> check_active_irq_A_if; ct_running b; Invs b; ((aa, ba), y, ab, bb) \<in> do_user_op_A_if utf\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag b) b ba proof (prove)
goal (1 subgoal):
 1. \<lbrakk>((a, b), x, aa, ba) \<in> check_active_irq_A_if; ct_running b; Invs b; ((aa, ba), y, ab, bb) \<in> do_user_op_A_if utf\<rbrakk> \<Longrightarrow> ((?a11, b), ?x11, ?aa11, ba) \<in> check_active_irq_A_if proof (prove)
goal:
No subgoals!