theory Noninterference_Refinement

lemma big_step_R_tranclp_abs':
        "\<lbrakk>(s, s')
        \<in> lift_fst_rel (lift_snd_rel state_relation) O
          lift_fst_rel (lift_snd_rel rf_sr);
        big_step_R\<^sup>+\<^sup>+ s0 s''\<rbrakk> \<Longrightarrow> s'' = (Fin (ADT_C_if fp utf) s')
       \<longrightarrow> big_step_R\<^sup>+\<^sup>+ s0 s" apply (erule tranclp_induct) apply (clarsimp simp: Fin_ADT_C_if lift_fst_rel_def) apply (rule tranclp.r_into_trancl) apply (simp add: big_step_R_def) apply (clarsimp simp: Fin_ADT_C_if lift_fst_rel_def) apply (rule tranclp.trancl_into_trancl) apply assumption apply (simp add: big_step_R_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> lift_fst_rel (lift_snd_rel state_relation) O lift_fst_rel (lift_snd_rel rf_sr); big_step_R\<^sup>+\<^sup>+ s0 s''\<rbrakk> \<Longrightarrow> s'' = Fin (ADT_C_if fp utf) s' \<longrightarrow> big_step_R\<^sup>+\<^sup>+ s0 s proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>(s, s') \<in> lift_fst_rel (lift_snd_rel state_relation) O lift_fst_rel (lift_snd_rel rf_sr); big_step_R s0 y\<rbrakk> \<Longrightarrow> y = Fin (ADT_C_if fp utf) s' \<longrightarrow> big_step_R\<^sup>+\<^sup>+ s0 s
 2. \<And>y z. \<lbrakk>(s, s') \<in> lift_fst_rel (lift_snd_rel state_relation) O lift_fst_rel (lift_snd_rel rf_sr); big_step_R\<^sup>+\<^sup>+ s0 y; big_step_R y z; y = Fin (ADT_C_if fp utf) s' \<longrightarrow> big_step_R\<^sup>+\<^sup>+ s0 s\<rbrakk> \<Longrightarrow> z = Fin (ADT_C_if fp utf) s' \<longrightarrow> big_step_R\<^sup>+\<^sup>+ s0 s proof (prove)
goal (2 subgoals):
 1. \<And>a ba aa bb ab bd bf. \<lbrakk>big_step_R s0 ((a, cstate_to_A bf), ba); s' = ((a, bf), ba); s = ((aa, bb), ba); ((aa, bb), ab, bd) \<in> lift_snd_rel state_relation; ((ab, bd), a, bf) \<in> lift_snd_rel rf_sr\<rbrakk> \<Longrightarrow> big_step_R\<^sup>+\<^sup>+ s0 ((aa, bb), ba)
 2. \<And>y z. \<lbrakk>(s, s') \<in> lift_fst_rel (lift_snd_rel state_relation) O lift_fst_rel (lift_snd_rel rf_sr); big_step_R\<^sup>+\<^sup>+ s0 y; big_step_R y z; y = Fin (ADT_C_if fp utf) s' \<longrightarrow> big_step_R\<^sup>+\<^sup>+ s0 s\<rbrakk> \<Longrightarrow> z = Fin (ADT_C_if fp utf) s' \<longrightarrow> big_step_R\<^sup>+\<^sup>+ s0 s proof (prove)
goal (2 subgoals):
 1. \<And>a ba aa bb ab bd bf. \<lbrakk>big_step_R s0 ((a, cstate_to_A bf), ba); s' = ((a, bf), ba); s = ((aa, bb), ba); ((aa, bb), ab, bd) \<in> lift_snd_rel state_relation; ((ab, bd), a, bf) \<in> lift_snd_rel rf_sr\<rbrakk> \<Longrightarrow> big_step_R s0 ((aa, bb), ba)
 2. \<And>y z. \<lbrakk>(s, s') \<in> lift_fst_rel (lift_snd_rel state_relation) O lift_fst_rel (lift_snd_rel rf_sr); big_step_R\<^sup>+\<^sup>+ s0 y; big_step_R y z; y = Fin (ADT_C_if fp utf) s' \<longrightarrow> big_step_R\<^sup>+\<^sup>+ s0 s\<rbrakk> \<Longrightarrow> z = Fin (ADT_C_if fp utf) s' \<longrightarrow> big_step_R\<^sup>+\<^sup>+ s0 s proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(s, s') \<in> lift_fst_rel (lift_snd_rel state_relation) O lift_fst_rel (lift_snd_rel rf_sr); big_step_R\<^sup>+\<^sup>+ s0 y; big_step_R y z; y = Fin (ADT_C_if fp utf) s' \<longrightarrow> big_step_R\<^sup>+\<^sup>+ s0 s\<rbrakk> \<Longrightarrow> z = Fin (ADT_C_if fp utf) s' \<longrightarrow> big_step_R\<^sup>+\<^sup>+ s0 s proof (prove)
goal (1 subgoal):
 1. \<And>a b ba aa bc ab bd ac bf bh. \<lbrakk>big_step_R\<^sup>+\<^sup>+ s0 ((a, b), ba); big_step_R ((a, b), ba) ((aa, cstate_to_A bh), bc); s' = ((aa, bh), bc); s = ((ab, bd), bc); ((ab, bd), ac, bf) \<in> lift_snd_rel state_relation; ((ac, bf), aa, bh) \<in> lift_snd_rel rf_sr; b = cstate_to_A bh \<longrightarrow> a = aa \<longrightarrow> ba \<noteq> bc\<rbrakk> \<Longrightarrow> big_step_R\<^sup>+\<^sup>+ s0 ((ab, bd), bc) proof (prove)
goal (2 subgoals):
 1. \<And>a b ba aa bc ab bd ac bf bh. \<lbrakk>big_step_R\<^sup>+\<^sup>+ s0 ((a, b), ba); big_step_R ((a, b), ba) ((aa, cstate_to_A bh), bc); s' = ((aa, bh), bc); s = ((ab, bd), bc); ((ab, bd), ac, bf) \<in> lift_snd_rel state_relation; ((ac, bf), aa, bh) \<in> lift_snd_rel rf_sr; b = cstate_to_A bh \<longrightarrow> a = aa \<longrightarrow> ba \<noteq> bc\<rbrakk> \<Longrightarrow> big_step_R\<^sup>+\<^sup>+ s0 (?b42 a b ba aa bc ab bd ac bf bh)
 2. \<And>a b ba aa bc ab bd ac bf bh. \<lbrakk>big_step_R\<^sup>+\<^sup>+ s0 ((a, b), ba); big_step_R ((a, b), ba) ((aa, cstate_to_A bh), bc); s' = ((aa, bh), bc); s = ((ab, bd), bc); ((ab, bd), ac, bf) \<in> lift_snd_rel state_relation; ((ac, bf), aa, bh) \<in> lift_snd_rel rf_sr; b = cstate_to_A bh \<longrightarrow> a = aa \<longrightarrow> ba \<noteq> bc\<rbrakk> \<Longrightarrow> big_step_R (?b42 a b ba aa bc ab bd ac bf bh) ((ab, bd), bc) proof (prove)
goal (1 subgoal):
 1. \<And>a b ba aa bc ab bd ac bf bh. \<lbrakk>big_step_R\<^sup>+\<^sup>+ s0 ((a, b), ba); big_step_R ((a, b), ba) ((aa, cstate_to_A bh), bc); s' = ((aa, bh), bc); s = ((ab, bd), bc); ((ab, bd), ac, bf) \<in> lift_snd_rel state_relation; ((ac, bf), aa, bh) \<in> lift_snd_rel rf_sr; b = cstate_to_A bh \<longrightarrow> a = aa \<longrightarrow> ba \<noteq> bc\<rbrakk> \<Longrightarrow> big_step_R ((a, b), ba) ((ab, bd), bc) proof (prove)
goal:
No subgoals!