theory Noninterference_Refinement

lemma ADT_C_if_inv_holds_transport:
  "ADT_C_if fp utf [>
    {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)}" apply (subst arg_cong[where f="\<lambda>S. ADT_C_if fp utf [> S"]) prefer 2 apply (rule_tac A="ADT_A_if utf" in inv_holds_transport) prefer 3 apply (rule weaken_LI) apply (rule LI_abs_to_c) prefer 2 apply (rule invs_if_inv_holds_ADT_A_if) prefer 2 apply (rule inv_holds_T) apply (clarsimp simp: invs_if_full_invs_if) apply force done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ADT_C_if fp utf [> {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)} proof (prove)
goal (2 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)} = ?y
 2. ADT_C_if fp utf [> ?y proof (prove)
goal (2 subgoals):
 1. ADT_C_if fp utf [> ?y
 2. {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)} = ?y proof (prove)
goal (4 subgoals):
 1. ADT_A_if utf [> ?Ia1
 2. ADT_C_if fp utf [> ?Ic1
 3. LI (ADT_A_if utf) (ADT_C_if fp utf) ?R1 (?Ia1 \<times> ?Ic1)
 4. {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)} = {s'. \<exists>s. (s, s') \<in> ?R1 \<and> s \<in> ?Ia1 \<and> s' \<in> ?Ic1} proof (prove)
goal (4 subgoals):
 1. LI (ADT_A_if utf) (ADT_C_if fp utf) ?R1 (?Ia1 \<times> ?Ic1)
 2. ADT_A_if utf [> ?Ia1
 3. ADT_C_if fp utf [> ?Ic1
 4. {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)} = {s'. \<exists>s. (s, s') \<in> ?R1 \<and> s \<in> ?Ia1 \<and> s' \<in> ?Ic1} proof (prove)
goal (5 subgoals):
 1. LI (ADT_A_if utf) (ADT_C_if fp utf) ?R1 ?I'2
 2. ?Ia1 \<times> ?Ic1 \<subseteq> ?I'2
 3. ADT_A_if utf [> ?Ia1
 4. ADT_C_if fp utf [> ?Ic1
 5. {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)} = {s'. \<exists>s. (s, s') \<in> ?R1 \<and> s \<in> ?Ia1 \<and> s' \<in> ?Ic1} proof (prove)
goal (4 subgoals):
 1. ?Ia1 \<times> ?Ic1 \<subseteq> full_invs_if \<times> UNIV
 2. ADT_A_if utf [> ?Ia1
 3. ADT_C_if fp utf [> ?Ic1
 4. {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)} = {s'. \<exists>s. (s, s') \<in> lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'}) \<and> s \<in> ?Ia1 \<and> s' \<in> ?Ic1} proof (prove)
goal (4 subgoals):
 1. ADT_A_if utf [> ?Ia1
 2. ?Ia1 \<times> ?Ic1 \<subseteq> full_invs_if \<times> UNIV
 3. ADT_C_if fp utf [> ?Ic1
 4. {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)} = {s'. \<exists>s. (s, s') \<in> lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'}) \<and> s \<in> ?Ia1 \<and> s' \<in> ?Ic1} proof (prove)
goal (3 subgoals):
 1. Collect invs_if \<times> ?Ic1 \<subseteq> full_invs_if \<times> UNIV
 2. ADT_C_if fp utf [> ?Ic1
 3. {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)} = {s'. \<exists>s. (s, s') \<in> lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'}) \<and> s \<in> Collect invs_if \<and> s' \<in> ?Ic1} proof (prove)
goal (3 subgoals):
 1. ADT_C_if fp utf [> ?Ic1
 2. Collect invs_if \<times> ?Ic1 \<subseteq> full_invs_if \<times> UNIV
 3. {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)} = {s'. \<exists>s. (s, s') \<in> lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'}) \<and> s \<in> Collect invs_if \<and> s' \<in> ?Ic1} proof (prove)
goal (2 subgoals):
 1. Collect invs_if \<times> UNIV \<subseteq> full_invs_if \<times> UNIV
 2. {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)} = {s'. \<exists>s. (s, s') \<in> lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'}) \<and> s \<in> Collect invs_if \<and> s' \<in> UNIV} proof (prove)
goal (1 subgoal):
 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)} = {s'. \<exists>s. (s, s') \<in> lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'}) \<and> s \<in> Collect invs_if \<and> s' \<in> UNIV} proof (prove)
goal:
No subgoals!