theory Prefix_Refinement

lemma is_matching_fragment_trans:
  assumes assms:
    "is_matching_fragment sr osr (=) h_tr h_res t0 R' t frag_g"
    "(g_tr, g_res) \<in> frag_g t" "length g_tr = length h_tr"
    "is_matching_fragment sr osr (=) g_tr g_res s0 R s frag_f"
  assumes sr: "equivp sr" "equivp osr"
  shows "is_matching_fragment sr osr (=) h_tr h_res s0 R s frag_f" proof - have matching_tr1:
    "matching_tr sr (rev g_tr) (rev h_tr)" using assms by (auto simp: is_matching_fragment_def matching_tr_pfx_def) hence matching_tr:
    "\<And>n. matching_tr sr (take n (rev g_tr)) (take n (rev h_tr))" by (simp add: matching_tr_def) have matching:
    "\<And>xs. matching_tr_pfx sr xs g_tr = matching_tr_pfx sr xs h_tr" apply (rule equivpE, rule sr) apply (simp add: matching_tr_pfx_def assms) apply (rule conj_cong; simp?) apply (strengthen iffI) apply (metis matching_tr transpD[OF matching_tr_transp]
                 sympD[OF matching_tr_symp]) done note is_me = matching_tr1[unfolded matching_tr_def, simplified,
    THEN list_all2_is_me, symmetric] show ?thesis using assms apply (clarsimp simp: is_matching_fragment_def matching is_me) apply (drule(1) bspec)+ apply clarsimp apply (erule tmres.rel_cases | clarsimp)+ apply (rule equivpE, rule sr(2)) apply (metis transpD) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_matching_fragment sr osr (=) h_tr h_res s0 R s frag_f proof (state)
goal (1 subgoal):
 1. is_matching_fragment sr osr (=) h_tr h_res s0 R s frag_f proof (prove)
goal (1 subgoal):
 1. matching_tr sr (rev g_tr) (rev h_tr) proof (prove)
using this:
is_matching_fragment sr osr (=) h_tr h_res t0 R' t frag_g
(g_tr, g_res) \<in> frag_g t
length g_tr = length h_tr
is_matching_fragment sr osr (=) g_tr g_res s0 R s frag_f
equivp sr
equivp osr

goal (1 subgoal):
 1. matching_tr sr (rev g_tr) (rev h_tr) proof (state)
this:
matching_tr sr (rev g_tr) (rev h_tr)

goal (1 subgoal):
 1. is_matching_fragment sr osr (=) h_tr h_res s0 R s frag_f proof (prove)
using this:
matching_tr sr (rev g_tr) (rev h_tr)

goal (1 subgoal):
 1. \<And>n. matching_tr sr (take n (rev g_tr)) (take n (rev h_tr)) proof (state)
this:
matching_tr sr (take ?n (rev g_tr)) (take ?n (rev h_tr))

goal (1 subgoal):
 1. is_matching_fragment sr osr (=) h_tr h_res s0 R s frag_f proof (prove)
goal (1 subgoal):
 1. \<And>xs. matching_tr_pfx sr xs g_tr = matching_tr_pfx sr xs h_tr proof (prove)
goal (1 subgoal):
 1. \<And>xs. \<lbrakk>reflp sr; symp sr; transp sr\<rbrakk> \<Longrightarrow> matching_tr_pfx sr xs g_tr = matching_tr_pfx sr xs h_tr proof (prove)
goal (1 subgoal):
 1. \<And>xs. \<lbrakk>reflp sr; symp sr; transp sr\<rbrakk> \<Longrightarrow> (length xs \<le> length h_tr \<and> matching_tr sr (rev xs) (take (length xs) (rev g_tr))) = (length xs \<le> length h_tr \<and> matching_tr sr (rev xs) (take (length xs) (rev h_tr))) proof (prove)
goal (1 subgoal):
 1. \<And>xs. \<lbrakk>reflp sr; symp sr; transp sr; length xs \<le> length h_tr\<rbrakk> \<Longrightarrow> matching_tr sr (rev xs) (take (length xs) (rev g_tr)) = matching_tr sr (rev xs) (take (length xs) (rev h_tr)) proof (prove)
goal (1 subgoal):
 1. \<And>xs. \<lbrakk>reflp sr; symp sr; transp sr; length xs \<le> length h_tr\<rbrakk> \<Longrightarrow> (matching_tr sr (rev xs) (take (length xs) (rev g_tr)) \<longrightarrow> matching_tr sr (rev xs) (take (length xs) (rev h_tr))) \<and> (matching_tr sr (rev xs) (take (length xs) (rev h_tr)) \<longrightarrow> matching_tr sr (rev xs) (take (length xs) (rev g_tr))) proof (prove)
goal:
No subgoals! proof (state)
this:
matching_tr_pfx sr ?xs g_tr = matching_tr_pfx sr ?xs h_tr

goal (1 subgoal):
 1. is_matching_fragment sr osr (=) h_tr h_res s0 R s frag_f proof (state)
this:
\<forall>x y. (case x of (aid, as) \<Rightarrow> \<lambda>(cid, cs). aid = cid \<and> sr as cs) y \<longrightarrow> fst x = fst y \<Longrightarrow> (?n < length h_tr \<and> fst (rev h_tr ! ?n) = Me) = (?n < length g_tr \<and> fst (rev g_tr ! ?n) = Me)

goal (1 subgoal):
 1. is_matching_fragment sr osr (=) h_tr h_res s0 R s frag_f proof (prove)
goal (1 subgoal):
 1. is_matching_fragment sr osr (=) h_tr h_res s0 R s frag_f proof (prove)
using this:
is_matching_fragment sr osr (=) h_tr h_res t0 R' t frag_g
(g_tr, g_res) \<in> frag_g t
length g_tr = length h_tr
is_matching_fragment sr osr (=) g_tr g_res s0 R s frag_f
equivp sr
equivp osr

goal (1 subgoal):
 1. is_matching_fragment sr osr (=) h_tr h_res s0 R s frag_f proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(g_tr, g_res) \<in> frag_g t; length g_tr = length h_tr; equivp sr; equivp osr; (a, b) \<in> frag_f s; prefix_closed frag_g; prefix_closed frag_f; self_closed (\<lambda>xs. length xs < length h_tr \<and> fst (rev g_tr ! length xs) = Me) t frag_g; self_closed (\<lambda>xs. length xs < length h_tr \<and> fst (rev g_tr ! length xs) = Me) s frag_f; env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) h_tr \<and> rely_cond R' t0 ((Env, s) # xs)) t frag_g; env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) h_tr \<and> rely_cond R s0 ((Env, s) # xs)) s frag_f; frag_g t \<noteq> {}; \<forall>x\<in>frag_g t. case x of (tr, res) \<Rightarrow> rely_cond R' t0 tr \<and> matching_tr_pfx sr tr h_tr \<and> (length tr < length h_tr \<longrightarrow> res = Incomplete) \<and> (length tr = length h_tr \<longrightarrow> rel_tmres osr (=) res h_res); frag_f s \<noteq> {}; \<forall>x\<in>frag_f s. case x of (tr, res) \<Rightarrow> rely_cond R s0 tr \<and> matching_tr_pfx sr tr h_tr \<and> (length tr < length h_tr \<longrightarrow> res = Incomplete) \<and> (length tr = length h_tr \<longrightarrow> rel_tmres osr (=) res g_res)\<rbrakk> \<Longrightarrow> rely_cond R s0 a \<and> matching_tr_pfx sr a h_tr \<and> (length a < length h_tr \<longrightarrow> b = Incomplete) \<and> (length a = length h_tr \<longrightarrow> rel_tmres osr (=) b h_res) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(g_tr, g_res) \<in> frag_g t; length g_tr = length h_tr; equivp sr; equivp osr; (a, b) \<in> frag_f s; prefix_closed frag_g; prefix_closed frag_f; self_closed (\<lambda>xs. length xs < length h_tr \<and> fst (rev g_tr ! length xs) = Me) t frag_g; self_closed (\<lambda>xs. length xs < length h_tr \<and> fst (rev g_tr ! length xs) = Me) s frag_f; env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) h_tr \<and> rely_cond R' t0 ((Env, s) # xs)) t frag_g; env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) h_tr \<and> rely_cond R s0 ((Env, s) # xs)) s frag_f; frag_g t \<noteq> {}; frag_f s \<noteq> {}; case (g_tr, g_res) of (tr, res) \<Rightarrow> rely_cond R' t0 tr \<and> matching_tr_pfx sr tr h_tr \<and> (length tr < length h_tr \<longrightarrow> res = Incomplete) \<and> (length tr = length h_tr \<longrightarrow> rel_tmres osr (=) res h_res); case (a, b) of (tr, res) \<Rightarrow> rely_cond R s0 tr \<and> matching_tr_pfx sr tr h_tr \<and> (length tr < length h_tr \<longrightarrow> res = Incomplete) \<and> (length tr = length h_tr \<longrightarrow> rel_tmres osr (=) res g_res)\<rbrakk> \<Longrightarrow> rely_cond R s0 a \<and> matching_tr_pfx sr a h_tr \<and> (length a < length h_tr \<longrightarrow> b = Incomplete) \<and> (length a = length h_tr \<longrightarrow> rel_tmres osr (=) b h_res) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(g_tr, g_res) \<in> frag_g t; length g_tr = length h_tr; equivp sr; equivp osr; (a, b) \<in> frag_f s; prefix_closed frag_g; prefix_closed frag_f; self_closed (\<lambda>xs. length xs < length h_tr \<and> fst (rev g_tr ! length xs) = Me) t frag_g; self_closed (\<lambda>xs. length xs < length h_tr \<and> fst (rev g_tr ! length xs) = Me) s frag_f; env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) h_tr \<and> rely_cond R' t0 ((Env, s) # xs)) t frag_g; env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) h_tr \<and> rely_cond R s0 ((Env, s) # xs)) s frag_f; frag_g t \<noteq> {}; frag_f s \<noteq> {}; rely_cond R' t0 g_tr; rely_cond R s0 a; matching_tr_pfx sr g_tr h_tr; rel_tmres osr (=) g_res h_res; matching_tr_pfx sr a h_tr; length a = length h_tr; rel_tmres osr (=) b g_res\<rbrakk> \<Longrightarrow> rel_tmres osr (=) b h_res proof (prove)
goal (1 subgoal):
 1. \<And>a aa ba bb bc. \<lbrakk>(g_tr, Result (aa, ba)) \<in> frag_g t; length g_tr = length h_tr; equivp sr; equivp osr; (a, Result (aa, bc)) \<in> frag_f s; prefix_closed frag_g; prefix_closed frag_f; self_closed (\<lambda>xs. length xs < length h_tr \<and> fst (rev g_tr ! length xs) = Me) t frag_g; self_closed (\<lambda>xs. length xs < length h_tr \<and> fst (rev g_tr ! length xs) = Me) s frag_f; env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) h_tr \<and> rely_cond R' t0 ((Env, s) # xs)) t frag_g; env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) h_tr \<and> rely_cond R s0 ((Env, s) # xs)) s frag_f; frag_g t \<noteq> {}; frag_f s \<noteq> {}; rely_cond R' t0 g_tr; rely_cond R s0 a; matching_tr_pfx sr g_tr h_tr; matching_tr_pfx sr a h_tr; length a = length h_tr; h_res = Result (aa, bb); osr ba bb; g_res = Result (aa, ba); osr bc ba\<rbrakk> \<Longrightarrow> osr bc bb proof (prove)
goal (1 subgoal):
 1. \<And>a aa ba bb bc. \<lbrakk>(g_tr, Result (aa, ba)) \<in> frag_g t; length g_tr = length h_tr; equivp sr; equivp osr; (a, Result (aa, bc)) \<in> frag_f s; prefix_closed frag_g; prefix_closed frag_f; self_closed (\<lambda>xs. length xs < length h_tr \<and> fst (rev g_tr ! length xs) = Me) t frag_g; self_closed (\<lambda>xs. length xs < length h_tr \<and> fst (rev g_tr ! length xs) = Me) s frag_f; env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) h_tr \<and> rely_cond R' t0 ((Env, s) # xs)) t frag_g; env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) h_tr \<and> rely_cond R s0 ((Env, s) # xs)) s frag_f; frag_g t \<noteq> {}; frag_f s \<noteq> {}; rely_cond R' t0 g_tr; rely_cond R s0 a; matching_tr_pfx sr g_tr h_tr; matching_tr_pfx sr a h_tr; length a = length h_tr; h_res = Result (aa, bb); osr ba bb; g_res = Result (aa, ba); osr bc ba; reflp osr; symp osr; transp osr\<rbrakk> \<Longrightarrow> osr bc bb proof (prove)
goal:
No subgoals! proof (state)
this:
is_matching_fragment sr osr (=) h_tr h_res s0 R s frag_f

goal:
No subgoals!