kings-crown/FVELER_Isabelle huggingface dataset:
theory Noninterference

lemma current_aag_eqI:
  "cur_domain s = cur_domain t \<Longrightarrow> current_aag s = current_aag t" by (simp add: current_aag_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cur_domain s = cur_domain t \<Longrightarrow> current_aag s = current_aag t
theory Noninterference

lemma pas_refined_current_aag':
  "\<lbrakk> reachable t; current_aag (internal_state_if s) = current_aag (internal_state_if t) \<rbrakk>
     \<Longrightarrow> pas_refined (current_aag (internal_state_if s)) (internal_state_if t)" by (fastforce intro: pas_refined_if)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reachable t; current_aag (internal_state_if s) = current_aag (internal_state_if t)\<rbrakk> \<Longrightarrow> pas_refined (current_aag (internal_state_if s)) (internal_state_if t)
theory Noninterference

lemma guarded_pas_domain_current_aag':
  "\<lbrakk> reachable t; current_aag (internal_state_if s) = current_aag (internal_state_if t) \<rbrakk>
     \<Longrightarrow> guarded_pas_domain (current_aag (internal_state_if s)) (internal_state_if t)" by (fastforce intro: guarded_pas_domain_if)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reachable t; current_aag (internal_state_if s) = current_aag (internal_state_if t)\<rbrakk> \<Longrightarrow> guarded_pas_domain (current_aag (internal_state_if s)) (internal_state_if t)
theory Noninterference

lemma pasDomainAbs_not_SilcLabel[simp]:
  "SilcLabel \<notin> pasDomainAbs initial_aag x" apply (rule pas_wellformed_noninterference_silc) apply (rule policy_wellformed) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. SilcLabel \<notin> pasDomainAbs initial_aag x proof (prove)
goal (1 subgoal):
 1. pas_wellformed_noninterference initial_aag proof (prove)
goal:
No subgoals!
theory Noninterference

lemma domain_in_ordinary_label[simp]:
  "OrdinaryLabel (label_of (the_elem (pasDomainAbs initial_aag (cur_domain s)))) =
   the_elem (pasDomainAbs initial_aag (cur_domain s))" apply (case_tac "the_elem (pasDomainAbs initial_aag (cur_domain s))") apply simp apply (metis the_label_of_domain_exists pasDomainAbs_not_SilcLabel) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. OrdinaryLabel (label_of (the_elem (pasDomainAbs initial_aag (cur_domain s)))) = the_elem (pasDomainAbs initial_aag (cur_domain s)) proof (prove)
goal (2 subgoals):
 1. \<And>x1. the_elem (pasDomainAbs initial_aag (cur_domain s)) = OrdinaryLabel x1 \<Longrightarrow> OrdinaryLabel (label_of (the_elem (pasDomainAbs initial_aag (cur_domain s)))) = the_elem (pasDomainAbs initial_aag (cur_domain s))
 2. the_elem (pasDomainAbs initial_aag (cur_domain s)) = SilcLabel \<Longrightarrow> OrdinaryLabel (label_of (the_elem (pasDomainAbs initial_aag (cur_domain s)))) = the_elem (pasDomainAbs initial_aag (cur_domain s)) proof (prove)
goal (1 subgoal):
 1. the_elem (pasDomainAbs initial_aag (cur_domain s)) = SilcLabel \<Longrightarrow> OrdinaryLabel (label_of (the_elem (pasDomainAbs initial_aag (cur_domain s)))) = the_elem (pasDomainAbs initial_aag (cur_domain s)) proof (prove)
goal:
No subgoals!
theory Noninterference

lemma schact_is_rct_eqI:
  "(s,t) \<in> uwr(Partition (partition_if s))
   \<Longrightarrow> schact_is_rct (internal_state_if s) = schact_is_rct (internal_state_if t)" apply (drule uwr_partition_if[OF _ refl refl]) apply (simp add: schact_is_rct_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. uwr2 s (Partition (partition_if s)) t \<Longrightarrow> schact_is_rct (internal_state_if s) = schact_is_rct (internal_state_if t) proof (prove)
goal (1 subgoal):
 1. states_equiv_for (\<lambda>x. pasObjectAbs initial_aag x \<in> subjectReads (pasPolicy initial_aag) (OrdinaryLabel (partition_if s))) (\<lambda>x. pasIRQAbs initial_aag x \<in> subjectReads (pasPolicy initial_aag) (OrdinaryLabel (partition_if s))) (\<lambda>x. pasASIDAbs initial_aag x \<in> subjectReads (pasPolicy initial_aag) (OrdinaryLabel (partition_if s))) (\<lambda>x. pasDomainAbs initial_aag x \<inter> subjectReads (pasPolicy initial_aag) (OrdinaryLabel (partition_if s)) \<noteq> {}) (internal_state_if s) (internal_state_if t) \<and> cur_thread (internal_state_if s) = cur_thread (internal_state_if t) \<and> cur_domain (internal_state_if s) = cur_domain (internal_state_if t) \<and> globals_equiv (internal_state_if s) (internal_state_if t) \<and> scheduler_action (internal_state_if s) = scheduler_action (internal_state_if t) \<and> work_units_completed (internal_state_if s) = work_units_completed (internal_state_if t) \<and> equiv_irq_state (machine_state (internal_state_if s)) (machine_state (internal_state_if t)) \<and> (user_modes (sys_mode_of s) \<longrightarrow> user_context_of s = user_context_of t) \<and> sys_mode_of s = sys_mode_of t \<and> equiv_for (\<lambda>x. pasObjectAbs initial_aag x = SilcLabel) kheap (internal_state_if s) (internal_state_if t) \<Longrightarrow> schact_is_rct (internal_state_if s) = schact_is_rct (internal_state_if t) proof (prove)
goal:
No subgoals!
theory Noninterference

lemma handle_ev[wp]:
  assumes ok: "equiv_valid I AA AA P f"
  assumes err: "\<And>e. equiv_valid I AA AA (E e) (handler e)"
  assumes hoare: "\<lbrace>P\<rbrace> f -, \<lbrace>E\<rbrace>"
  shows "equiv_valid I AA AA P (f <handle> handler)" apply (simp add: handleE_def handleE'_def) apply (wp err ok | wpc | simp)+ apply (insert hoare[simplified validE_E_def validE_def])[1] apply (simp split: sum.splits) by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv I AA P (f <handle> handler) proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv I AA P (do v <- f;
case v of Inl e \<Rightarrow> handler e | Inr v' \<Rightarrow> return (Inr v')
od) proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P''\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x. rv = Inl x \<longrightarrow> E x s\<rbrace>
 2. \<And>s. P s \<Longrightarrow> P s \<and> ?P'' s proof (prove)
goal (2 subgoals):
 1. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> True\<rbrace> \<Longrightarrow> \<lbrace>?P''\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x. rv = Inl x \<longrightarrow> E x s\<rbrace>
 2. \<And>s. P s \<Longrightarrow> P s \<and> ?P'' s proof (prove)
goal (1 subgoal):
 1. \<And>s. P s \<Longrightarrow> P s \<and> P s
theory Noninterference

lemma pas_refined_initial_aag_reachable:
  "system.reachable (big_step_ADT_A_if utf) s0 s
   \<Longrightarrow> pas_refined initial_aag (internal_state_if s)" apply (simp add: initial_aag_bak[where s="internal_state_if s"]) apply (rule pas_refined_pasSubject_update[OF pas_refined_if pas_wellformed_cur]) apply assumption apply (clarsimp simp: current_aag_def) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reachable s \<Longrightarrow> pas_refined initial_aag (internal_state_if s) proof (prove)
goal (1 subgoal):
 1. reachable s \<Longrightarrow> pas_refined (current_aag (internal_state_if s)\<lparr>pasSubject := the_elem (pasDomainAbs (current_aag (internal_state_if s)) (cur_domain s0_internal))\<rparr>) (internal_state_if s) proof (prove)
goal (2 subgoals):
 1. reachable s \<Longrightarrow> reachable s
 2. reachable s \<Longrightarrow> the_elem (pasDomainAbs (current_aag (internal_state_if s)) (cur_domain s0_internal)) \<in> pasDomainAbs (current_aag (internal_state_if s)) ?d1 proof (prove)
goal (1 subgoal):
 1. reachable s \<Longrightarrow> the_elem (pasDomainAbs (current_aag (internal_state_if s)) (cur_domain s0_internal)) \<in> pasDomainAbs (current_aag (internal_state_if s)) ?d1 proof (prove)
goal (1 subgoal):
 1. reachable s \<Longrightarrow> the_elem (pasDomainAbs initial_aag (cur_domain s0_internal)) \<in> pasDomainAbs initial_aag ?d1 proof (prove)
goal:
No subgoals!
theory Noninterference

lemma silc_inv_initial_aag_reachable:
  "system.reachable (big_step_ADT_A_if utf) s0 s
   \<Longrightarrow> silc_inv initial_aag s0_internal (internal_state_if s)" apply (simp add: silc_inv_cur[symmetric]) apply (fastforce dest: reachable_invs_if simp: invs_if_def Invs_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reachable s \<Longrightarrow> silc_inv initial_aag s0_internal (internal_state_if s) proof (prove)
goal (1 subgoal):
 1. reachable s \<Longrightarrow> silc_inv (current_aag (internal_state_if s)) s0_internal (internal_state_if s) proof (prove)
goal:
No subgoals!
theory Noninterference

lemma uwr_def_cur:
  "uwr \<equiv> same_for (current_aag (internal_state_if s))" by (simp add: uwr_def current_aag_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. uwr \<equiv> same_for (current_aag (internal_state_if s))
theory Noninterference

lemma Step_big_step_ADT_A_if:
  "data_type.Step (big_step_ADT_A_if utf) = big_steps (ADT_A_if utf) big_step_R big_step_evmap" by (simp add: big_step_ADT_A_if_def big_step_adt_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. data_type.Step (big_step_ADT_A_if utf) = big_steps (ADT_A_if utf) big_step_R big_step_evmap
theory Noninterference

lemma partitionIntegrity_refl:
  "partitionIntegrity aag s s" by (fastforce simp: partitionIntegrity_def silc_dom_equiv_def domain_fields_equiv_def
               intro: integrity_refl globals_equiv_scheduler_refl equiv_for_refl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partitionIntegrity aag s s
theory Noninterference

lemma check_active_irq_A_if_partitionIntegrity:
  "((a, b), x, aa, ba) \<in> check_active_irq_A_if
   \<Longrightarrow> partitionIntegrity (current_aag b) b ba" apply (simp add: check_active_irq_A_if_def) apply (erule use_valid) apply (wp check_active_irq_if_partitionIntegrity) apply (rule partitionIntegrity_refl) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((a, b), x, aa, ba) \<in> check_active_irq_A_if \<Longrightarrow> partitionIntegrity (current_aag b) b ba proof (prove)
goal (1 subgoal):
 1. ((x, aa), ba) \<in> fst (check_active_irq_if a b) \<Longrightarrow> partitionIntegrity (current_aag b) b ba proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P\<rbrace> check_active_irq_if a \<lbrace>\<lambda>a. partitionIntegrity (current_aag b) b\<rbrace>
 2. ?P b proof (prove)
goal (1 subgoal):
 1. partitionIntegrity (current_aag b) b b proof (prove)
goal:
No subgoals!
theory Noninterference

lemma check_active_irq_A_if_result_state:
  "((a, b), x, aa, ba) \<in> check_active_irq_A_if
   \<Longrightarrow> ba = (b\<lparr>machine_state := (machine_state b)\<lparr>irq_state := irq_state_of_state b + 1\<rparr>\<rparr>)" apply (simp add: check_active_irq_A_if_def check_active_irq_if_def) apply (erule use_valid) apply (wp dmo_getActiveIRQ_wp) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((a, b), x, aa, ba) \<in> check_active_irq_A_if \<Longrightarrow> ba = b\<lparr>machine_state := machine_state b\<lparr>irq_state := irq_state_of_state b + 1\<rparr>\<rparr> proof (prove)
goal (1 subgoal):
 1. ((x, aa), ba) \<in> fst ((do irq <- do_machine_op (getActiveIRQ False);
return (irq, a)
od) b) \<Longrightarrow> ba = b\<lparr>machine_state := machine_state b\<lparr>irq_state := Suc (irq_state_of_state b)\<rparr>\<rparr> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P1\<rbrace> do irq <- do_machine_op (getActiveIRQ False);
return (irq, a)
od \<lbrace>\<lambda>a c. c = b\<lparr>machine_state := machine_state b\<lparr>irq_state := Suc (irq_state_of_state b)\<rparr>\<rparr>\<rbrace>
 2. ?P1 b proof (prove)
goal (1 subgoal):
 1. b\<lparr>machine_state := machine_state b\<lparr>irq_state := irq_state_of_state b + 1\<rparr>\<rparr> = b\<lparr>machine_state := machine_state b\<lparr>irq_state := Suc (irq_state_of_state b)\<rparr>\<rparr> proof (prove)
goal:
No subgoals!
theory Noninterference

lemma not_schedule_modes_KernelEntry:
  "(\<not> scheduler_modes (KernelEntry event)) = (event \<noteq> Interrupt)" by (case_tac event, simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<not> scheduler_modes (KernelEntry event)) = (event \<noteq> Interrupt)
theory Noninterference

lemma Step_ADT_A_if'':
  "\<lbrakk> (s, t) \<in> data_type.Step (ADT_A_if utf) (); system.reachable (ADT_A_if utf) s0 s \<rbrakk>
     \<Longrightarrow> (s, t) \<in> system.Step (ADT_A_if utf) ()" apply (simp add: system.reachable_def) apply (clarsimp) apply (frule execution_invs) apply (frule invs_if_full_invs_if) apply (frule execution_restrict) apply (simp add: system.Step_def execution_def steps_def ADT_A_if_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, t) \<in> data_type.Step (ADT_A_if utf) (); system.reachable (ADT_A_if utf) s0 s\<rbrakk> \<Longrightarrow> (s, t) \<in> system.Step (ADT_A_if utf) () proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, t) \<in> data_type.Step (ADT_A_if utf) (); \<exists>js. s \<in> execution (ADT_A_if utf) s0 js\<rbrakk> \<Longrightarrow> (s, t) \<in> system.Step (ADT_A_if utf) () proof (prove)
goal (1 subgoal):
 1. \<And>js. \<lbrakk>(s, t) \<in> data_type.Step (ADT_A_if utf) (); s \<in> execution (ADT_A_if utf) s0 js\<rbrakk> \<Longrightarrow> (s, t) \<in> system.Step (ADT_A_if utf) () proof (prove)
goal (1 subgoal):
 1. \<And>js. \<lbrakk>(s, t) \<in> data_type.Step (ADT_A_if utf) (); s \<in> execution (ADT_A_if utf) s0 js; invs_if s\<rbrakk> \<Longrightarrow> (s, t) \<in> system.Step (ADT_A_if utf) () proof (prove)
goal (1 subgoal):
 1. \<And>js. \<lbrakk>(s, t) \<in> data_type.Step (ADT_A_if utf) (); s \<in> execution (ADT_A_if utf) s0 js; invs_if s; s \<in> full_invs_if\<rbrakk> \<Longrightarrow> (s, t) \<in> system.Step (ADT_A_if utf) () proof (prove)
goal (1 subgoal):
 1. \<And>js. \<lbrakk>(s, t) \<in> data_type.Step (ADT_A_if utf) (); s \<in> execution (ADT_A_if utf) s0 js; invs_if s; s \<in> full_invs_if; step_restrict s\<rbrakk> \<Longrightarrow> (s, t) \<in> system.Step (ADT_A_if utf) () proof (prove)
goal:
No subgoals!
theory Noninterference

lemma partitionIntegrity_current_aag_eq:
  "partitionIntegrity (current_aag s) s s' \<Longrightarrow> current_aag s' = current_aag s" by (simp add: current_aag_def partitionIntegrity_def domain_fields_equiv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. partitionIntegrity (current_aag s) s s' \<Longrightarrow> current_aag s' = current_aag s
theory Noninterference

lemma partitionIntegrity_trans':
  "\<lbrakk> partitionIntegrity (current_aag s) s s';
     partitionIntegrity (current_aag s') s' t \<rbrakk>
     \<Longrightarrow> partitionIntegrity (current_aag s) s t" apply (rule partitionIntegrity_trans, assumption) apply (simp add: partitionIntegrity_current_aag_eq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>partitionIntegrity (current_aag s) s s'; partitionIntegrity (current_aag s') s' t\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag s) s t proof (prove)
goal (1 subgoal):
 1. \<lbrakk>partitionIntegrity (current_aag s) s s'; partitionIntegrity (current_aag s') s' t\<rbrakk> \<Longrightarrow> partitionIntegrity (current_aag s) s' t proof (prove)
goal:
No subgoals!
theory Noninterference

lemma reachable_Step':
  "\<lbrakk> system.reachable (big_step_ADT_A_if utf) s0 s;
     (s, s') \<in> data_type.Step (big_step_ADT_A_if utf) a \<rbrakk>
     \<Longrightarrow> system.reachable (big_step_ADT_A_if utf) s0 s'" apply (rule reachable_Step, assumption) apply (drule small_step_reachable) apply (frule ADT_A_if_reachable_full_invs_if) apply (drule ADT_A_if_reachable_step_restrict) apply (clarsimp simp: system.Step_def execution_def big_step_ADT_A_if_def
                        Fin_big_step_adt Fin_ADT_if steps_eq_Run) apply (simp add: big_step_ADT_A_if_def big_step_adt_def Init_ADT_if) apply (cases s) apply (case_tac a) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reachable s; (s, s') \<in> data_type.Step (big_step_ADT_A_if utf) a\<rbrakk> \<Longrightarrow> reachable s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reachable s; (s, s') \<in> data_type.Step (big_step_ADT_A_if utf) a\<rbrakk> \<Longrightarrow> (s, s') \<in> ni.Step ?a proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> data_type.Step (big_step_ADT_A_if utf) a; system.reachable (ADT_A_if utf) s0 s\<rbrakk> \<Longrightarrow> (s, s') \<in> ni.Step ?a proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> data_type.Step (big_step_ADT_A_if utf) a; system.reachable (ADT_A_if utf) s0 s; s \<in> full_invs_if\<rbrakk> \<Longrightarrow> (s, s') \<in> ni.Step ?a proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> data_type.Step (big_step_ADT_A_if utf) a; s \<in> full_invs_if; step_restrict s\<rbrakk> \<Longrightarrow> (s, s') \<in> ni.Step ?a proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> data_type.Step (big_step_adt (ADT_A_if utf) big_step_R big_step_evmap) (); s \<in> full_invs_if; step_restrict s\<rbrakk> \<Longrightarrow> \<exists>a b ba. ((a, b), ba) \<in> Init (big_step_adt (ADT_A_if utf) big_step_R big_step_evmap) s \<and> (((a, b), ba), s') \<in> data_type.Step (big_step_adt (ADT_A_if utf) big_step_R big_step_evmap) () proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> big_steps (ADT_A_if utf) big_step_R big_step_evmap (); s \<in> full_invs_if; step_restrict s\<rbrakk> \<Longrightarrow> \<exists>a b ba. ((a, b), ba) = s \<and> (((a, b), ba), s') \<in> big_steps (ADT_A_if utf) big_step_R big_step_evmap () proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(s, s') \<in> big_steps (ADT_A_if utf) big_step_R big_step_evmap (); s \<in> full_invs_if; step_restrict s; s = (a, b)\<rbrakk> \<Longrightarrow> \<exists>a b ba. ((a, b), ba) = s \<and> (((a, b), ba), s') \<in> big_steps (ADT_A_if utf) big_step_R big_step_evmap () proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>(s, s') \<in> big_steps (ADT_A_if utf) big_step_R big_step_evmap (); s \<in> full_invs_if; step_restrict s; s = (a, b); a = (aa, ba)\<rbrakk> \<Longrightarrow> \<exists>a b ba. ((a, b), ba) = s \<and> (((a, b), ba), s') \<in> big_steps (ADT_A_if utf) big_step_R big_step_evmap () proof (prove)
goal:
No subgoals!
theory Noninterference

lemma Step_cur_domain_unchanged:
  "\<lbrakk> system.reachable (big_step_ADT_A_if utf) s0 s;
     (s, s') \<in> Simulation.Step (big_step_ADT_A_if utf) (); part s \<noteq> PSched \<rbrakk>
     \<Longrightarrow> cur_domain (internal_state_if s') = cur_domain (internal_state_if s)" by (fastforce dest: Step_partitionIntegrity
                simp: partitionIntegrity_def domain_fields_equiv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reachable s; (s, s') \<in> data_type.Step (big_step_ADT_A_if utf) (); part s \<noteq> PSched\<rbrakk> \<Longrightarrow> cur_domain (internal_state_if s') = cur_domain (internal_state_if s)
theory Noninterference

lemma Step_current_aag_unchanged:
  "\<lbrakk> system.reachable (big_step_ADT_A_if utf) s0 s;
     (s, s') \<in> Simulation.Step (big_step_ADT_A_if utf) (); part s \<noteq> PSched \<rbrakk>
     \<Longrightarrow> current_aag (internal_state_if s') = current_aag (internal_state_if s)" apply (simp add: current_aag_def) apply (metis Step_cur_domain_unchanged) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reachable s; (s, s') \<in> data_type.Step (big_step_ADT_A_if utf) (); part s \<noteq> PSched\<rbrakk> \<Longrightarrow> current_aag (internal_state_if s') = current_aag (internal_state_if s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reachable s; (s, s') \<in> data_type.Step (big_step_ADT_A_if utf) (); part s \<noteq> PSched\<rbrakk> \<Longrightarrow> initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain (internal_state_if s')))\<rparr> = initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain (internal_state_if s)))\<rparr> proof (prove)
goal:
No subgoals!
theory Noninterference

lemma not_PSched:
  "\<lbrakk> (x, u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched \<rbrakk>
     \<Longrightarrow> x \<noteq> PSched" apply (erule contrapos_nn) apply simp apply (rule schedFlowsToAll) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(x, u) \<notin> policyFlows (pasPolicy initial_aag); u \<noteq> PSched\<rbrakk> \<Longrightarrow> x \<noteq> PSched proof (prove)
goal (1 subgoal):
 1. \<lbrakk>u \<noteq> PSched; x = PSched\<rbrakk> \<Longrightarrow> policy2 x u proof (prove)
goal (1 subgoal):
 1. \<lbrakk>u \<noteq> PSched; x = PSched\<rbrakk> \<Longrightarrow> policy2 PSched u proof (prove)
goal:
No subgoals!
theory Noninterference

lemma not_PSched_big_step_R:
  "\<lbrakk> part s \<noteq> PSched; big_step_R s t \<rbrakk>
     \<Longrightarrow> sys_mode_of s = KernelExit \<and> interrupted_modes (sys_mode_of t)" apply (clarsimp simp: part_def big_step_R_def sys_mode_of_def split: if_split_asm) apply (cases s, simp, case_tac b; simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>part s \<noteq> PSched; big_step_R s t\<rbrakk> \<Longrightarrow> sys_mode_of s = KernelExit \<and> interrupted_modes (sys_mode_of t) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> scheduler_modes (snd s); interrupted_modes (snd s); snd t = KernelExit\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Noninterference

lemma sub_big_steps_App:
  "(s',as @ [a]) \<in> sub_big_steps A R s
   \<Longrightarrow> \<exists>s'a. (s'a, as) \<in> sub_big_steps A R s \<and> (s'a, s') \<in> data_type.Step A a \<and> \<not> R s s'" by (erule sub_big_steps.cases; fastforce)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (s', as @ [a]) \<in> sub_big_steps A R s \<Longrightarrow> \<exists>s'a. (s'a, as) \<in> sub_big_steps A R s \<and> (s'a, s') \<in> data_type.Step A a \<and> \<not> R s s'
theory Noninterference

lemma globals_equiv_idle_thread_ptr:
  "globals_equiv s t \<Longrightarrow> idle_thread s= idle_thread t" by (simp add: globals_equiv_def idle_equiv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. globals_equiv s t \<Longrightarrow> idle_thread s = idle_thread t