theory Prefix_Refinement

lemma matching_tr_rely_cond:
  "matching_tr sr (rev tr) (rev tr')
    \<Longrightarrow> rely_cond R s0 tr
    \<Longrightarrow> sr s0 t0
    \<Longrightarrow> rely_cond (\<lambda>t0 t. \<exists>s0 s. sr s0 t0 \<and> sr s t \<and> R s0 s) t0 tr'" apply (simp add: matching_tr_def) apply (induct arbitrary: s0 t0 rule: list_all2_induct) apply simp apply (clarsimp simp: rely_cond_def trace_steps_append last_st_tr_def hd_append) apply (intro conjI impI; clarsimp) apply blast apply (clarsimp simp: neq_Nil_conv list_all2_Cons2) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>matching_tr sr (rev tr) (rev tr'); rely_cond R s0 tr; sr s0 t0\<rbrakk> \<Longrightarrow> rely_cond (\<lambda>t0 t. \<exists>s0 s. sr s0 t0 \<and> sr s t \<and> R s0 s) t0 tr' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>list_all2 (\<lambda>(aid, as) (cid, cs). aid = cid \<and> sr as cs) tr tr'; rely_cond R s0 tr; sr s0 t0\<rbrakk> \<Longrightarrow> rely_cond (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) t0 tr' proof (prove)
goal (2 subgoals):
 1. \<And>s0 t0. \<lbrakk>rely_cond R s0 []; sr s0 t0\<rbrakk> \<Longrightarrow> rely_cond (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) t0 []
 2. \<And>x xs y ys s0 t0. \<lbrakk>(case x of (aid, as) \<Rightarrow> \<lambda>(cid, cs). aid = cid \<and> sr as cs) y; list_all2 (\<lambda>a. case a of (aid, as) \<Rightarrow> \<lambda>(cid, cs). aid = cid \<and> sr as cs) xs ys; \<And>s0 t0. \<lbrakk>rely_cond R s0 xs; sr s0 t0\<rbrakk> \<Longrightarrow> rely_cond (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) t0 ys; rely_cond R s0 (x # xs); sr s0 t0\<rbrakk> \<Longrightarrow> rely_cond (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) t0 (y # ys) proof (prove)
goal (1 subgoal):
 1. \<And>x xs y ys s0 t0. \<lbrakk>(case x of (aid, as) \<Rightarrow> \<lambda>(cid, cs). aid = cid \<and> sr as cs) y; list_all2 (\<lambda>a. case a of (aid, as) \<Rightarrow> \<lambda>(cid, cs). aid = cid \<and> sr as cs) xs ys; \<And>s0 t0. \<lbrakk>rely_cond R s0 xs; sr s0 t0\<rbrakk> \<Longrightarrow> rely_cond (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) t0 ys; rely_cond R s0 (x # xs); sr s0 t0\<rbrakk> \<Longrightarrow> rely_cond (\<lambda>t0 t. \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s t \<and> R s0 s)) t0 (y # ys) proof (prove)
goal (1 subgoal):
 1. \<And>b xs aa ba ys s0 t0. \<lbrakk>list_all2 (\<lambda>(aid, as) (cid, cs). aid = cid \<and> sr as cs) xs ys; \<And>s0 t0. \<lbrakk>\<forall>x\<in>trace_steps (rev xs) s0. case x of (ident, s0, s) \<Rightarrow> ident = Env \<longrightarrow> R s0 s; sr s0 t0\<rbrakk> \<Longrightarrow> \<forall>x\<in>trace_steps (rev ys) t0. case x of (ident, s0, s) \<Rightarrow> ident = Env \<longrightarrow> (\<exists>s0a. sr s0a s0 \<and> (\<exists>sa. sr sa s \<and> R s0a sa)); sr s0 t0; sr b ba; aa = Env \<longrightarrow> R (if xs = [] then hd [s0] else hd (map snd xs)) b; \<forall>x\<in>trace_steps (rev xs) s0. case x of (ident, s0, s) \<Rightarrow> ident = Env \<longrightarrow> R s0 s\<rbrakk> \<Longrightarrow> (ys = [] \<longrightarrow> aa = Env \<longrightarrow> (\<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s ba \<and> R s0 s))) \<and> (ys \<noteq> [] \<longrightarrow> aa = Env \<longrightarrow> (\<exists>s0. sr s0 (hd (map snd ys)) \<and> (\<exists>s. sr s ba \<and> R s0 s))) proof (prove)
goal (2 subgoals):
 1. \<And>b ba s0 t0. \<lbrakk>sr s0 t0; sr b ba; R s0 b\<rbrakk> \<Longrightarrow> \<exists>s0. sr s0 t0 \<and> (\<exists>s. sr s ba \<and> R s0 s)
 2. \<And>b xs ba ys s0 t0. \<lbrakk>list_all2 (\<lambda>(aid, as) (cid, cs). aid = cid \<and> sr as cs) xs ys; \<And>s0 t0. \<lbrakk>\<forall>x\<in>trace_steps (rev xs) s0. case x of (ident, s0, s) \<Rightarrow> ident = Env \<longrightarrow> R s0 s; sr s0 t0\<rbrakk> \<Longrightarrow> \<forall>x\<in>trace_steps (rev ys) t0. case x of (ident, s0, s) \<Rightarrow> ident = Env \<longrightarrow> (\<exists>s0a. sr s0a s0 \<and> (\<exists>sa. sr sa s \<and> R s0a sa)); sr s0 t0; sr b ba; R (if xs = [] then hd [s0] else hd (map snd xs)) b; \<forall>x\<in>trace_steps (rev xs) s0. case x of (ident, s0, s) \<Rightarrow> ident = Env \<longrightarrow> R s0 s; ys \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>s0. sr s0 (hd (map snd ys)) \<and> (\<exists>s. sr s ba \<and> R s0 s) proof (prove)
goal (1 subgoal):
 1. \<And>b xs ba ys s0 t0. \<lbrakk>list_all2 (\<lambda>(aid, as) (cid, cs). aid = cid \<and> sr as cs) xs ys; \<And>s0 t0. \<lbrakk>\<forall>x\<in>trace_steps (rev xs) s0. case x of (ident, s0, s) \<Rightarrow> ident = Env \<longrightarrow> R s0 s; sr s0 t0\<rbrakk> \<Longrightarrow> \<forall>x\<in>trace_steps (rev ys) t0. case x of (ident, s0, s) \<Rightarrow> ident = Env \<longrightarrow> (\<exists>s0a. sr s0a s0 \<and> (\<exists>sa. sr sa s \<and> R s0a sa)); sr s0 t0; sr b ba; R (if xs = [] then hd [s0] else hd (map snd xs)) b; \<forall>x\<in>trace_steps (rev xs) s0. case x of (ident, s0, s) \<Rightarrow> ident = Env \<longrightarrow> R s0 s; ys \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>s0. sr s0 (hd (map snd ys)) \<and> (\<exists>s. sr s ba \<and> R s0 s) proof (prove)
goal (1 subgoal):
 1. \<And>b ba s0 t0 a bb ysa bc zs. \<lbrakk>\<And>s0 t0. \<lbrakk>\<forall>x\<in>trace_steps (rev zs @ [(a, bc)]) s0. case x of (ident, s0, s) \<Rightarrow> ident = Env \<longrightarrow> R s0 s; sr s0 t0\<rbrakk> \<Longrightarrow> \<forall>x\<in>trace_steps (rev ysa @ [(a, bb)]) t0. case x of (ident, s0, s) \<Rightarrow> ident = Env \<longrightarrow> (\<exists>s0a. sr s0a s0 \<and> (\<exists>sa. sr sa s \<and> R s0a sa)); sr s0 t0; sr b ba; R bc b; \<forall>x\<in>trace_steps (rev zs @ [(a, bc)]) s0. case x of (ident, s0, s) \<Rightarrow> ident = Env \<longrightarrow> R s0 s; sr bc bb; list_all2 (\<lambda>(aid, as) (cid, cs). aid = cid \<and> sr as cs) zs ysa\<rbrakk> \<Longrightarrow> \<exists>s0. sr s0 bb \<and> (\<exists>s. sr s ba \<and> R s0 s) proof (prove)
goal:
No subgoals!