theory Noninterference_Refinement

lemma ADT_C_if_Init_transport:
  "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)}" apply clarsimp apply (frule set_mp[OF global_automata_refine.init_refinement[OF c_to_haskell[OF uop_nonempty]]]) apply (clarsimp simp: Image_def lift_fst_rel_def lift_snd_rel_def) apply (frule set_mp[OF global_automata_refine.init_refinement[OF haskell_to_abs[OF uop_nonempty]]]) apply (clarsimp simp: Image_def lift_fst_rel_def lift_snd_rel_def) apply (rule_tac x=bb in exI) apply simp apply (rule conjI) apply (force simp: ADT_H_if_def) apply (rule_tac x=ba in exI) apply (clarsimp simp: ADT_A_if_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 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)} proof (prove)
goal (1 subgoal):
 1. \<And>a b ba. ((a, b), ba) \<in> Init (ADT_C_if fp utf) s0 \<Longrightarrow> \<exists>aa bb bc. (((aa, bb), bc), (a, b), ba) \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> ((aa, bb), bc) \<in> full_invs_if' \<and> (\<exists>a b ba. (((a, b), ba), (aa, bb), bc) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if ((a, b), ba)) proof (prove)
goal (1 subgoal):
 1. \<And>a b ba. \<lbrakk>((a, b), ba) \<in> Init (ADT_C_if fp utf) s0; ((a, b), ba) \<in> lift_fst_rel (lift_snd_rel rf_sr) `` Init (valid_initial_state_noenabled.ADT_H_if utf) s0\<rbrakk> \<Longrightarrow> \<exists>aa bb bc. (((aa, bb), bc), (a, b), ba) \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> ((aa, bb), bc) \<in> full_invs_if' \<and> (\<exists>a b ba. (((a, b), ba), (aa, bb), bc) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if ((a, b), ba)) proof (prove)
goal (1 subgoal):
 1. \<And>b aa bb bc. \<lbrakk>((aa, b), bc) \<in> Init (ADT_C_if fp utf) s0; ((aa, bb), bc) \<in> Init (valid_initial_state_noenabled.ADT_H_if utf) s0; (bb, b) \<in> rf_sr\<rbrakk> \<Longrightarrow> \<exists>ba. (ba, b) \<in> rf_sr \<and> ((aa, ba), bc) \<in> full_invs_if' \<and> (\<exists>b. (b, ba) \<in> state_relation \<and> invs_if ((aa, b), bc)) proof (prove)
goal (1 subgoal):
 1. \<And>b aa bb bc. \<lbrakk>((aa, b), bc) \<in> Init (ADT_C_if fp utf) s0; ((aa, bb), bc) \<in> Init (valid_initial_state_noenabled.ADT_H_if utf) s0; (bb, b) \<in> rf_sr; ((aa, bb), bc) \<in> lift_fst_rel (lift_snd_rel state_relation) `` Init (ADT_A_if utf) s0\<rbrakk> \<Longrightarrow> \<exists>ba. (ba, b) \<in> rf_sr \<and> ((aa, ba), bc) \<in> full_invs_if' \<and> (\<exists>b. (b, ba) \<in> state_relation \<and> invs_if ((aa, b), bc)) proof (prove)
goal (1 subgoal):
 1. \<And>b bb a ba bd. \<lbrakk>((a, b), bd) \<in> Init (ADT_C_if fp utf) s0; ((a, bb), bd) \<in> Init (valid_initial_state_noenabled.ADT_H_if utf) s0; (bb, b) \<in> rf_sr; ((a, ba), bd) \<in> Init (ADT_A_if utf) s0; (ba, bb) \<in> state_relation\<rbrakk> \<Longrightarrow> \<exists>ba. (ba, b) \<in> rf_sr \<and> ((a, ba), bd) \<in> full_invs_if' \<and> (\<exists>b. (b, ba) \<in> state_relation \<and> invs_if ((a, b), bd)) proof (prove)
goal (1 subgoal):
 1. \<And>b bb a ba bd. \<lbrakk>((a, b), bd) \<in> Init (ADT_C_if fp utf) s0; ((a, bb), bd) \<in> Init (valid_initial_state_noenabled.ADT_H_if utf) s0; (bb, b) \<in> rf_sr; ((a, ba), bd) \<in> Init (ADT_A_if utf) s0; (ba, bb) \<in> state_relation\<rbrakk> \<Longrightarrow> (bb, b) \<in> rf_sr \<and> ((a, bb), bd) \<in> full_invs_if' \<and> (\<exists>b. (b, bb) \<in> state_relation \<and> invs_if ((a, b), bd)) proof (prove)
goal (1 subgoal):
 1. \<And>b bb a ba bd. \<lbrakk>((a, b), bd) \<in> Init (ADT_C_if fp utf) s0; ((a, bb), bd) \<in> Init (valid_initial_state_noenabled.ADT_H_if utf) s0; (bb, b) \<in> rf_sr; ((a, ba), bd) \<in> Init (ADT_A_if utf) s0; (ba, bb) \<in> state_relation\<rbrakk> \<Longrightarrow> ((a, bb), bd) \<in> full_invs_if' \<and> (\<exists>b. (b, bb) \<in> state_relation \<and> invs_if ((a, b), bd)) proof (prove)
goal (2 subgoals):
 1. \<And>b bb a ba bd. \<lbrakk>((a, b), bd) \<in> Init (ADT_C_if fp utf) s0; ((a, bb), bd) \<in> Init (valid_initial_state_noenabled.ADT_H_if utf) s0; (bb, b) \<in> rf_sr; ((a, ba), bd) \<in> Init (ADT_A_if utf) s0; (ba, bb) \<in> state_relation\<rbrakk> \<Longrightarrow> ((a, bb), bd) \<in> full_invs_if'
 2. \<And>b bb a ba bd. \<lbrakk>((a, b), bd) \<in> Init (ADT_C_if fp utf) s0; ((a, bb), bd) \<in> Init (valid_initial_state_noenabled.ADT_H_if utf) s0; (bb, b) \<in> rf_sr; ((a, ba), bd) \<in> Init (ADT_A_if utf) s0; (ba, bb) \<in> state_relation\<rbrakk> \<Longrightarrow> \<exists>b. (b, bb) \<in> state_relation \<and> invs_if ((a, b), bd) proof (prove)
goal (1 subgoal):
 1. \<And>b bb a ba bd. \<lbrakk>((a, b), bd) \<in> Init (ADT_C_if fp utf) s0; ((a, bb), bd) \<in> Init (valid_initial_state_noenabled.ADT_H_if utf) s0; (bb, b) \<in> rf_sr; ((a, ba), bd) \<in> Init (ADT_A_if utf) s0; (ba, bb) \<in> state_relation\<rbrakk> \<Longrightarrow> \<exists>b. (b, bb) \<in> state_relation \<and> invs_if ((a, b), bd) proof (prove)
goal (1 subgoal):
 1. \<And>b bb a ba bd. \<lbrakk>((a, b), bd) \<in> Init (ADT_C_if fp utf) s0; ((a, bb), bd) \<in> Init (valid_initial_state_noenabled.ADT_H_if utf) s0; (bb, b) \<in> rf_sr; ((a, ba), bd) \<in> Init (ADT_A_if utf) s0; (ba, bb) \<in> state_relation\<rbrakk> \<Longrightarrow> (ba, bb) \<in> state_relation \<and> invs_if ((a, ba), bd) proof (prove)
goal:
No subgoals!