theory Noninterference_Refinement

lemma big_step_ADT_C_if_enabled_system:
  "enabled_system (big_step_ADT_C_if utf) s0" apply (simp add: big_step_ADT_C_if_def) apply (rule_tac measuref="internal_R (ADT_C_if fp utf) measuref_if" in big_step_adt_enabled_system) apply simp apply (force simp: big_step_R_def internal_R_def) apply (rule Init_Fin_serial_weak_strengthen) apply (rule ADT_C_if_Init_Fin_serial_weak) apply (rule ADT_C_if_inv_holds_transport) apply force apply (rule ADT_C_if_Init_transport) apply (rule ADT_C_if_big_step_R_terminate) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. enabled_system (big_step_ADT_C_if utf) s0 proof (prove)
goal (1 subgoal):
 1. enabled_system (big_step_adt (ADT_C_if fp utf) (internal_R (ADT_C_if fp utf) big_step_R) big_step_evmap) s0 proof (prove)
goal (4 subgoals):
 1. \<forall>x y. x = y
 2. \<And>s. \<not> internal_R (ADT_C_if fp utf) big_step_R s s
 3. Init_Fin_serial_weak (ADT_C_if fp utf) s0 ?I
 4. rel_terminate (ADT_C_if fp utf) s0 (internal_R (ADT_C_if fp utf) big_step_R) ?I (internal_R (ADT_C_if fp utf) measuref_if) proof (prove)
goal (3 subgoals):
 1. \<And>s. \<not> internal_R (ADT_C_if fp utf) big_step_R s s
 2. Init_Fin_serial_weak (ADT_C_if fp utf) s0 ?I
 3. rel_terminate (ADT_C_if fp utf) s0 (internal_R (ADT_C_if fp utf) big_step_R) ?I (internal_R (ADT_C_if fp utf) measuref_if) proof (prove)
goal (2 subgoals):
 1. Init_Fin_serial_weak (ADT_C_if fp utf) s0 ?I
 2. rel_terminate (ADT_C_if fp utf) s0 (internal_R (ADT_C_if fp utf) big_step_R) ?I (internal_R (ADT_C_if fp utf) measuref_if) proof (prove)
goal (5 subgoals):
 1. Init_Fin_serial_weak (ADT_C_if fp utf) s0 ?I7
 2. ADT_C_if fp utf [> ?I
 3. ?I \<subseteq> ?I7
 4. Init (ADT_C_if fp utf) s0 \<subseteq> ?I
 5. rel_terminate (ADT_C_if fp utf) s0 (internal_R (ADT_C_if fp utf) big_step_R) ?I (internal_R (ADT_C_if fp utf) measuref_if) proof (prove)
goal (4 subgoals):
 1. ADT_C_if fp utf [> ?I
 2. ?I \<subseteq> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if'}
 3. Init (ADT_C_if fp utf) s0 \<subseteq> ?I
 4. rel_terminate (ADT_C_if fp utf) s0 (internal_R (ADT_C_if fp utf) big_step_R) ?I (internal_R (ADT_C_if fp utf) measuref_if) proof (prove)
goal (3 subgoals):
 1. {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)} \<subseteq> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if'}
 2. Init (ADT_C_if fp utf) s0 \<subseteq> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}
 3. rel_terminate (ADT_C_if fp utf) s0 (internal_R (ADT_C_if fp utf) big_step_R) {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)} (internal_R (ADT_C_if fp utf) measuref_if) proof (prove)
goal (2 subgoals):
 1. Init (ADT_C_if fp utf) s0 \<subseteq> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}
 2. rel_terminate (ADT_C_if fp utf) s0 (internal_R (ADT_C_if fp utf) big_step_R) {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)} (internal_R (ADT_C_if fp utf) measuref_if) proof (prove)
goal (1 subgoal):
 1. rel_terminate (ADT_C_if fp utf) s0 (internal_R (ADT_C_if fp utf) big_step_R) {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)} (internal_R (ADT_C_if fp utf) measuref_if) proof (prove)
goal:
No subgoals!