theory Noninterference

lemma non_PSched_steps_run_in_lock_step:
  "\<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s;
    (s', t) \<in> data_type.Step (ADT_A_if utf) (); big_step_R s t;
    (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa;
    (s'a, ta) \<in> data_type.Step (ADT_A_if utf) (); big_step_R sa ta;
    (s, sa) \<in> uwr PSched; (s, sa) \<in> uwr (part s);
    system.reachable (big_step_ADT_A_if utf) s0 s;
    system.reachable (big_step_ADT_A_if utf) s0 sa;
    part s \<noteq> PSched\<rbrakk>
   \<Longrightarrow> asa = as" apply (case_tac "asa = as", assumption) apply (drule unit_lists_unequal) apply (erule disjE) apply (drule non_PSched_steps_run_in_lock_step', simp+) apply (frule schedIncludesCurrentDom[symmetric]) apply (drule_tac as=asa and asa=as in non_PSched_steps_run_in_lock_step', (simp add: uwr_sym)+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> data_type.Step (ADT_A_if utf) (); big_step_R s t; (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) (); big_step_R sa ta; uwr2 s PSched sa; uwr2 s (part s) sa; reachable s; reachable sa; part s \<noteq> PSched\<rbrakk> \<Longrightarrow> asa = as proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> data_type.Step (ADT_A_if utf) (); big_step_R s t; (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) (); big_step_R sa ta; uwr2 s PSched sa; uwr2 s (part s) sa; reachable s; reachable sa; part s \<noteq> PSched; asa \<noteq> as\<rbrakk> \<Longrightarrow> asa = as proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> data_type.Step (ADT_A_if utf) (); big_step_R s t; (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) (); big_step_R sa ta; uwr2 s PSched sa; uwr2 s (part s) sa; reachable s; reachable sa; part s \<noteq> PSched; asa < as \<or> as < asa\<rbrakk> \<Longrightarrow> asa = as proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> data_type.Step (ADT_A_if utf) (); big_step_R s t; (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) (); big_step_R sa ta; uwr2 s PSched sa; uwr2 s (part s) sa; reachable s; reachable sa; part s \<noteq> PSched; asa < as\<rbrakk> \<Longrightarrow> asa = as
 2. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> data_type.Step (ADT_A_if utf) (); big_step_R s t; (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) (); big_step_R sa ta; uwr2 s PSched sa; uwr2 s (part s) sa; reachable s; reachable sa; part s \<noteq> PSched; as < asa\<rbrakk> \<Longrightarrow> asa = as proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> data_type.Step (ADT_A_if utf) (); big_step_R s t; (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) (); big_step_R sa ta; uwr2 s PSched sa; uwr2 s (part s) sa; reachable s; reachable sa; part s \<noteq> PSched; as < asa\<rbrakk> \<Longrightarrow> asa = as proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s', as) \<in> sub_big_steps (ADT_A_if utf) big_step_R s; (s', t) \<in> data_type.Step (ADT_A_if utf) (); big_step_R s t; (s'a, asa) \<in> sub_big_steps (ADT_A_if utf) big_step_R sa; (s'a, ta) \<in> data_type.Step (ADT_A_if utf) (); big_step_R sa ta; uwr2 s PSched sa; uwr2 s (part s) sa; reachable s; reachable sa; part s \<noteq> PSched; as < asa; part sa = part s\<rbrakk> \<Longrightarrow> asa = as proof (prove)
goal:
No subgoals!