theory Prefix_Refinement

lemma is_matching_fragment_mbind:
  "is_matching_fragment sr intsr rvr ctr cres s0 R s f_a
    \<Longrightarrow> \<forall>tr x s'. (tr, Result (x, s')) \<in> f_a s
        \<longrightarrow> is_matching_fragment sr osr rvr' ctr' cres' (last_st_tr tr s0) R s' (f_b (last_st_tr tr s0) x)
    \<Longrightarrow> \<forall>s0' x. prefix_closed (f_b s0' x)
    \<Longrightarrow> ctr'' = ctr' @ ctr
    \<Longrightarrow> cres'' = (case cres of Failed \<Rightarrow> Failed | Incomplete \<Rightarrow> Incomplete | _ \<Rightarrow> cres')
    \<Longrightarrow> (cres = Incomplete \<or> cres = Failed) \<longrightarrow> ctr' = []
    \<Longrightarrow> is_matching_fragment sr osr rvr' ctr'' cres'' s0 R s
        (mbind f_a f_b s0)" apply (subst is_matching_fragment_def, clarsimp) apply (strengthen env_closed_mbind[where ctr''=ctr', mk_strg I E]
                    prefix_closed_mbind
                    self_closed_mbind[where ctr'="ctr'", mk_strg I E]) apply (simp add: conj_comms if_bool_eq_conj mres_def split del: if_split) apply (intro conjI allI impI; clarsimp?;
    (blast intro: is_matching_fragment_prefix_closed
                  is_matching_fragment_env_closed
                  is_matching_fragment_Nil
                  is_matching_fragment_self_closed
            dest: post_by_hoare)?) apply (clarsimp simp: mbind_def) apply (frule_tac s=s in is_matching_fragment_defD) apply (drule ex_in_conv[THEN iffD2], clarsimp) apply (drule(1) bspec) apply (rename_tac res; case_tac res; clarsimp) apply (drule spec2, drule spec, drule(1) mp) apply (fastforce dest: is_matching_fragment_defD) apply (clarsimp simp: mbind_def) apply (drule(1) is_matching_fragment_trD) apply (clarsimp simp: matching_tr_pfx_def split: tmres.split_asm) apply (drule spec2, drule spec, drule(1) mp) apply (drule(1) is_matching_fragment_trD) apply (clarsimp simp: matching_tr_pfx_def matching_tr_def
                        list_all2_appendI rely_cond_append) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_matching_fragment sr intsr rvr ctr cres s0 R s f_a; \<forall>tr x s'. (tr, Result (x, s')) \<in> f_a s \<longrightarrow> is_matching_fragment sr osr rvr' ctr' cres' (last_st_tr tr s0) R s' (f_b (last_st_tr tr s0) x); \<forall>s0' x. prefix_closed (f_b s0' x); ctr'' = ctr' @ ctr; cres'' = (case cres of Failed \<Rightarrow> Failed | Incomplete \<Rightarrow> Incomplete | Result prod \<Rightarrow> cres'); cres = Incomplete \<or> cres = Failed \<longrightarrow> ctr' = []\<rbrakk> \<Longrightarrow> is_matching_fragment sr osr rvr' ctr'' cres'' s0 R s (mbind f_a f_b s0) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_matching_fragment sr intsr rvr ctr cres s0 R s f_a; \<forall>tr x s'. (tr, Result (x, s')) \<in> f_a s \<longrightarrow> is_matching_fragment sr osr rvr' ctr' cres' (last_st_tr tr s0) R s' (f_b (last_st_tr tr s0) x); \<forall>s0' x. prefix_closed (f_b s0' x); ctr'' = ctr' @ ctr; cres'' = (case cres of Failed \<Rightarrow> Failed | Incomplete \<Rightarrow> Incomplete | Result prod \<Rightarrow> cres'); cres = Incomplete \<longrightarrow> ctr' = []; cres = Failed \<longrightarrow> ctr' = []\<rbrakk> \<Longrightarrow> prefix_closed (mbind f_a f_b s0) \<and> self_closed (\<lambda>xs. length xs < length ctr' + length ctr \<and> fst ((rev ctr @ rev ctr') ! length xs) = Me) s (mbind f_a f_b s0) \<and> env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) (ctr' @ ctr) \<and> rely_cond R s0 ((Env, s) # xs)) s (mbind f_a f_b s0) \<and> mbind f_a f_b s0 s \<noteq> {} \<and> (\<forall>x\<in>mbind f_a f_b s0 s. case x of (tr, res) \<Rightarrow> rely_cond R s0 tr \<and> matching_tr_pfx sr tr (ctr' @ ctr) \<and> (length tr < length ctr' + length ctr \<longrightarrow> res = Incomplete) \<and> (length tr = length ctr' + length ctr \<longrightarrow> rel_tmres osr rvr' res (case cres of Failed \<Rightarrow> Failed | Incomplete \<Rightarrow> Incomplete | Result prod \<Rightarrow> cres'))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_matching_fragment sr intsr rvr ctr cres s0 R s f_a; \<forall>tr x s'. (tr, Result (x, s')) \<in> f_a s \<longrightarrow> is_matching_fragment sr osr rvr' ctr' cres' (last_st_tr tr s0) R s' (f_b (last_st_tr tr s0) x); \<forall>s0' x. prefix_closed (f_b s0' x); ctr'' = ctr' @ ctr; cres'' = (case cres of Failed \<Rightarrow> Failed | Incomplete \<Rightarrow> Incomplete | Result prod \<Rightarrow> cres'); cres = Incomplete \<longrightarrow> ctr' = []; cres = Failed \<longrightarrow> ctr' = []\<rbrakk> \<Longrightarrow> (prefix_closed f_a \<and> (\<forall>tr x s' s. (tr, Result (x, s')) \<in> f_a s \<longrightarrow> prefix_closed (f_b (last_st_tr tr s0) x))) \<and> ((\<forall>tr x s'. (tr, Result (x, s')) \<in> f_a s \<longrightarrow> self_closed (\<lambda>xs. length xs < length ctr' \<and> fst (rev ctr' ! length xs) = Me) s' (f_b (last_st_tr tr s0) x) \<and> [] \<in> fst ` f_b (last_st_tr tr s0) x s') \<and> (\<lambda>xs. length xs < length ctr' + length ctr \<and> fst ((rev ctr @ rev ctr') ! length xs) = Me) = (\<lambda>xs. length xs < length (ctr' @ ctr) \<and> fst (rev (ctr' @ ctr) ! length xs) = Me) \<and> (cres = Incomplete \<longrightarrow> ctr' = [])) \<and> ((\<forall>tr x s'. (tr, Result (x, s')) \<in> f_a s \<longrightarrow> env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr' \<and> rely_cond R (last_st_tr tr s0) ((Env, s) # xs)) s' (f_b (last_st_tr tr s0) x) \<and> [] \<in> fst ` f_b (last_st_tr tr s0) x s') \<and> (if cres \<in> {Incomplete, Failed} then ?ctr19 = ctr else ?ctr19 = ctr' @ ctr) \<and> (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) (ctr' @ ctr) \<and> rely_cond R s0 ((Env, s) # xs)) = (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ?ctr19 \<and> rely_cond R s0 ((Env, s) # xs))) \<and> mbind f_a f_b s0 s \<noteq> {} \<and> (\<forall>x\<in>mbind f_a f_b s0 s. case x of (tr, res) \<Rightarrow> rely_cond R s0 tr \<and> matching_tr_pfx sr tr (ctr' @ ctr) \<and> (length tr < length ctr' + length ctr \<longrightarrow> res = Incomplete) \<and> (length tr = length ctr' + length ctr \<longrightarrow> rel_tmres osr rvr' res (case cres of Failed \<Rightarrow> Failed | Incomplete \<Rightarrow> Incomplete | Result prod \<Rightarrow> cres'))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_matching_fragment sr intsr rvr ctr cres s0 R s f_a; \<forall>tr x s'. (tr, Result (x, s')) \<in> f_a s \<longrightarrow> is_matching_fragment sr osr rvr' ctr' cres' (last_st_tr tr s0) R s' (f_b (last_st_tr tr s0) x); \<forall>s0' x. prefix_closed (f_b s0' x); ctr'' = ctr' @ ctr; cres'' = (case cres of Failed \<Rightarrow> Failed | Incomplete \<Rightarrow> Incomplete | Result prod \<Rightarrow> cres'); cres = Incomplete \<longrightarrow> ctr' = []; cres = Failed \<longrightarrow> ctr' = []\<rbrakk> \<Longrightarrow> prefix_closed f_a \<and> (cres = Failed \<longrightarrow> ?ctr19 = ctr) \<and> (cres = Incomplete \<longrightarrow> ?ctr19 = ctr) \<and> mbind f_a f_b s0 s \<noteq> {} \<and> (cres \<noteq> Failed \<and> cres \<noteq> Incomplete \<longrightarrow> ?ctr19 = ctr' @ ctr) \<and> (\<lambda>xs s. rely_cond R s0 ((Env, s) # xs) \<and> matching_tr_pfx sr ((Env, s) # xs) (ctr' @ ctr)) = (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ?ctr19 \<and> rely_cond R s0 ((Env, s) # xs)) \<and> (\<forall>tr x s'. (tr, Result (x, s')) \<in> f_a s \<longrightarrow> [] \<in> fst ` f_b (last_st_tr tr s0) x s' \<and> self_closed (\<lambda>xs. length xs < length ctr' \<and> fst (rev ctr' ! length xs) = Me) s' (f_b (last_st_tr tr s0) x)) \<and> (\<forall>(tr, res)\<in>mbind f_a f_b s0 s. rely_cond R s0 tr \<and> matching_tr_pfx sr tr (ctr' @ ctr) \<and> (length tr < length ctr' + length ctr \<longrightarrow> res = Incomplete) \<and> (length tr = length ctr' + length ctr \<longrightarrow> rel_tmres osr rvr' res (case cres of Failed \<Rightarrow> Failed | Incomplete \<Rightarrow> Incomplete | Result prod \<Rightarrow> cres'))) \<and> (\<forall>tr x s'. (tr, Result (x, s')) \<in> f_a s \<longrightarrow> [] \<in> fst ` f_b (last_st_tr tr s0) x s' \<and> env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr' \<and> rely_cond R (last_st_tr tr s0) ((Env, s) # xs)) s' (f_b (last_st_tr tr s0) x)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_matching_fragment sr intsr rvr ctr cres s0 R s f_a; \<forall>tr x s'. (tr, Result (x, s')) \<in> f_a s \<longrightarrow> is_matching_fragment sr osr rvr' ctr' cres' (last_st_tr tr s0) R s' (f_b (last_st_tr tr s0) x); \<forall>s0' x. prefix_closed (f_b s0' x); ctr'' = ctr' @ ctr; cres'' = (case cres of Failed \<Rightarrow> Failed | Incomplete \<Rightarrow> Incomplete | Result prod \<Rightarrow> cres'); cres = Incomplete \<longrightarrow> ctr' = []; cres = Failed \<longrightarrow> ctr' = []; mbind f_a f_b s0 s = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>a b. \<lbrakk>is_matching_fragment sr intsr rvr ctr cres s0 R s f_a; \<forall>tr x s'. (tr, Result (x, s')) \<in> f_a s \<longrightarrow> is_matching_fragment sr osr rvr' ctr' cres' (last_st_tr tr s0) R s' (f_b (last_st_tr tr s0) x); \<forall>s0' x. prefix_closed (f_b s0' x); ctr'' = ctr' @ ctr; cres'' = (case cres of Failed \<Rightarrow> Failed | Incomplete \<Rightarrow> Incomplete | Result prod \<Rightarrow> cres'); cres = Incomplete \<longrightarrow> ctr' = []; cres = Failed \<longrightarrow> ctr' = []; (a, b) \<in> mbind f_a f_b s0 s\<rbrakk> \<Longrightarrow> rely_cond R s0 a \<and> matching_tr_pfx sr a (ctr' @ ctr) \<and> (length a < length ctr' + length ctr \<longrightarrow> b = Incomplete) \<and> (length a = length ctr' + length ctr \<longrightarrow> rel_tmres osr rvr' b (case cres of Failed \<Rightarrow> Failed | Incomplete \<Rightarrow> Incomplete | Result prod \<Rightarrow> cres')) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_matching_fragment sr intsr rvr ctr cres s0 R s f_a; \<forall>tr x s'. (tr, Result (x, s')) \<in> f_a s \<longrightarrow> is_matching_fragment sr osr rvr' ctr' cres' (last_st_tr tr s0) R s' (f_b (last_st_tr tr s0) x); \<forall>s0' x. prefix_closed (f_b s0' x); ctr'' = ctr' @ ctr; cres'' = (case cres of Failed \<Rightarrow> Failed | Incomplete \<Rightarrow> Incomplete | Result prod \<Rightarrow> cres'); cres = Incomplete \<longrightarrow> ctr' = []; cres = Failed \<longrightarrow> ctr' = []; \<forall>x\<in>f_a s. (case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ xs, x)) ` f_b (last_st_tr xs s0) rv s) = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>a b. \<lbrakk>is_matching_fragment sr intsr rvr ctr cres s0 R s f_a; \<forall>tr x s'. (tr, Result (x, s')) \<in> f_a s \<longrightarrow> is_matching_fragment sr osr rvr' ctr' cres' (last_st_tr tr s0) R s' (f_b (last_st_tr tr s0) x); \<forall>s0' x. prefix_closed (f_b s0' x); ctr'' = ctr' @ ctr; cres'' = (case cres of Failed \<Rightarrow> Failed | Incomplete \<Rightarrow> Incomplete | Result prod \<Rightarrow> cres'); cres = Incomplete \<longrightarrow> ctr' = []; cres = Failed \<longrightarrow> ctr' = []; (a, b) \<in> mbind f_a f_b s0 s\<rbrakk> \<Longrightarrow> rely_cond R s0 a \<and> matching_tr_pfx sr a (ctr' @ ctr) \<and> (length a < length ctr' + length ctr \<longrightarrow> b = Incomplete) \<and> (length a = length ctr' + length ctr \<longrightarrow> rel_tmres osr rvr' b (case cres of Failed \<Rightarrow> Failed | Incomplete \<Rightarrow> Incomplete | Result prod \<Rightarrow> cres')) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_matching_fragment sr intsr rvr ctr cres s0 R s f_a; \<forall>tr x s'. (tr, Result (x, s')) \<in> f_a s \<longrightarrow> is_matching_fragment sr osr rvr' ctr' cres' (last_st_tr tr s0) R s' (f_b (last_st_tr tr s0) x); \<forall>s0' x. prefix_closed (f_b s0' x); ctr'' = ctr' @ ctr; cres'' = (case cres of Failed \<Rightarrow> Failed | Incomplete \<Rightarrow> Incomplete | Result prod \<Rightarrow> cres'); cres = Incomplete \<longrightarrow> ctr' = []; cres = Failed \<longrightarrow> ctr' = []; \<forall>x\<in>f_a s. (case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ xs, x)) ` f_b (last_st_tr xs s0) rv s) = {}; f_a s \<noteq> {}\<rbrakk> \<Longrightarrow> False
 2. \<And>a b. \<lbrakk>is_matching_fragment sr intsr rvr ctr cres s0 R s f_a; \<forall>tr x s'. (tr, Result (x, s')) \<in> f_a s \<longrightarrow> is_matching_fragment sr osr rvr' ctr' cres' (last_st_tr tr s0) R s' (f_b (last_st_tr tr s0) x); \<forall>s0' x. prefix_closed (f_b s0' x); ctr'' = ctr' @ ctr; cres'' = (case cres of Failed \<Rightarrow> Failed | Incomplete \<Rightarrow> Incomplete | Result prod \<Rightarrow> cres'); cres = Incomplete \<longrightarrow> ctr' = []; cres = Failed \<longrightarrow> ctr' = []; (a, b) \<in> mbind f_a f_b s0 s\<rbrakk> \<Longrightarrow> rely_cond R s0 a \<and> matching_tr_pfx sr a (ctr' @ ctr) \<and> (length a < length ctr' + length ctr \<longrightarrow> b = Incomplete) \<and> (length a = length ctr' + length ctr \<longrightarrow> rel_tmres osr rvr' b (case cres of Failed \<Rightarrow> Failed | Incomplete \<Rightarrow> Incomplete | Result prod \<Rightarrow> cres')) proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>is_matching_fragment sr intsr rvr ctr cres s0 R s f_a; \<forall>tr x s'. (tr, Result (x, s')) \<in> f_a s \<longrightarrow> is_matching_fragment sr osr rvr' ctr' cres' (last_st_tr tr s0) R s' (f_b (last_st_tr tr s0) x); \<forall>s0' x. prefix_closed (f_b s0' x); ctr'' = ctr' @ ctr; cres'' = (case cres of Failed \<Rightarrow> Failed | Incomplete \<Rightarrow> Incomplete | Result prod \<Rightarrow> cres'); cres = Incomplete \<longrightarrow> ctr' = []; cres = Failed \<longrightarrow> ctr' = []; \<forall>x\<in>f_a s. (case x of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ xs, x)) ` f_b (last_st_tr xs s0) rv s) = {}; (a, b) \<in> f_a s\<rbrakk> \<Longrightarrow> False
 2. \<And>a b. \<lbrakk>is_matching_fragment sr intsr rvr ctr cres s0 R s f_a; \<forall>tr x s'. (tr, Result (x, s')) \<in> f_a s \<longrightarrow> is_matching_fragment sr osr rvr' ctr' cres' (last_st_tr tr s0) R s' (f_b (last_st_tr tr s0) x); \<forall>s0' x. prefix_closed (f_b s0' x); ctr'' = ctr' @ ctr; cres'' = (case cres of Failed \<Rightarrow> Failed | Incomplete \<Rightarrow> Incomplete | Result prod \<Rightarrow> cres'); cres = Incomplete \<longrightarrow> ctr' = []; cres = Failed \<longrightarrow> ctr' = []; (a, b) \<in> mbind f_a f_b s0 s\<rbrakk> \<Longrightarrow> rely_cond R s0 a \<and> matching_tr_pfx sr a (ctr' @ ctr) \<and> (length a < length ctr' + length ctr \<longrightarrow> b = Incomplete) \<and> (length a = length ctr' + length ctr \<longrightarrow> rel_tmres osr rvr' b (case cres of Failed \<Rightarrow> Failed | Incomplete \<Rightarrow> Incomplete | Result prod \<Rightarrow> cres')) proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>is_matching_fragment sr intsr rvr ctr cres s0 R s f_a; \<forall>tr x s'. (tr, Result (x, s')) \<in> f_a s \<longrightarrow> is_matching_fragment sr osr rvr' ctr' cres' (last_st_tr tr s0) R s' (f_b (last_st_tr tr s0) x); \<forall>s0' x. prefix_closed (f_b s0' x); ctr'' = ctr' @ ctr; cres'' = (case cres of Failed \<Rightarrow> Failed | Incomplete \<Rightarrow> Incomplete | Result prod \<Rightarrow> cres'); cres = Incomplete \<longrightarrow> ctr' = []; cres = Failed \<longrightarrow> ctr' = []; (a, b) \<in> f_a s; (case (a, b) of (xs, Failed) \<Rightarrow> {(xs, Failed)} | (xs, Incomplete) \<Rightarrow> {(xs, Incomplete)} | (xs, Result (rv, s)) \<Rightarrow> (\<lambda>x. case x of (a, x) \<Rightarrow> (a @ xs, x)) ` f_b (last_st_tr xs s0) rv s) = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>a b. \<lbrakk>is_matching_fragment sr intsr rvr ctr cres s0 R s f_a; \<forall>tr x s'. (tr, Result (x, s')) \<in> f_a s \<longrightarrow> is_matching_fragment sr osr rvr' ctr' cres' (last_st_tr tr s0) R s' (f_b (last_st_tr tr s0) x); \<forall>s0' x. prefix_closed (f_b s0' x); ctr'' = ctr' @ ctr; cres'' = (case cres of Failed \<Rightarrow> Failed | Incomplete \<Rightarrow> Incomplete | Result prod \<Rightarrow> cres'); cres = Incomplete \<longrightarrow> ctr' = []; cres = Failed \<longrightarrow> ctr' = []; (a, b) \<in> mbind f_a f_b s0 s\<rbrakk> \<Longrightarrow> rely_cond R s0 a \<and> matching_tr_pfx sr a (ctr' @ ctr) \<and> (length a < length ctr' + length ctr \<longrightarrow> b = Incomplete) \<and> (length a = length ctr' + length ctr \<longrightarrow> rel_tmres osr rvr' b (case cres of Failed \<Rightarrow> Failed | Incomplete \<Rightarrow> Incomplete | Result prod \<Rightarrow> cres')) proof (prove)
goal (2 subgoals):
 1. \<And>a aa b. \<lbrakk>is_matching_fragment sr intsr rvr ctr cres s0 R s f_a; \<forall>tr x s'. (tr, Result (x, s')) \<in> f_a s \<longrightarrow> is_matching_fragment sr osr rvr' ctr' cres' (last_st_tr tr s0) R s' (f_b (last_st_tr tr s0) x); \<forall>s0' x. prefix_closed (f_b s0' x); ctr'' = ctr' @ ctr; cres'' = (case cres of Failed \<Rightarrow> Failed | Incomplete \<Rightarrow> Incomplete | Result prod \<Rightarrow> cres'); cres = Incomplete \<longrightarrow> ctr' = []; cres = Failed \<longrightarrow> ctr' = []; (a, Result (aa, b)) \<in> f_a s; f_b (last_st_tr a s0) aa b = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>a b. \<lbrakk>is_matching_fragment sr intsr rvr ctr cres s0 R s f_a; \<forall>tr x s'. (tr, Result (x, s')) \<in> f_a s \<longrightarrow> is_matching_fragment sr osr rvr' ctr' cres' (last_st_tr tr s0) R s' (f_b (last_st_tr tr s0) x); \<forall>s0' x. prefix_closed (f_b s0' x); ctr'' = ctr' @ ctr; cres'' = (case cres of Failed \<Rightarrow> Failed | Incomplete \<Rightarrow> Incomplete | Result prod \<Rightarrow> cres'); cres = Incomplete \<longrightarrow> ctr' = []; cres = Failed \<longrightarrow> ctr' = []; (a, b) \<in> mbind f_a f_b s0 s\<rbrakk> \<Longrightarrow> rely_cond R s0 a \<and> matching_tr_pfx sr a (ctr' @ ctr) \<and> (length a < length ctr' + length ctr \<longrightarrow> b = Incomplete) \<and> (length a = length ctr' + length ctr \<longrightarrow> rel_tmres osr rvr' b (case cres of Failed \<Rightarrow> Failed | Incomplete \<Rightarrow> Incomplete | Result prod \<Rightarrow> cres')) proof (prove)
goal (2 subgoals):
 1. \<And>a aa b. \<lbrakk>is_matching_fragment sr intsr rvr ctr cres s0 R s f_a; \<forall>s0' x. prefix_closed (f_b s0' x); ctr'' = ctr' @ ctr; cres'' = (case cres of Failed \<Rightarrow> Failed | Incomplete \<Rightarrow> Incomplete | Result prod \<Rightarrow> cres'); cres = Incomplete \<longrightarrow> ctr' = []; cres = Failed \<longrightarrow> ctr' = []; (a, Result (aa, b)) \<in> f_a s; f_b (last_st_tr a s0) aa b = {}; is_matching_fragment sr osr rvr' ctr' cres' (last_st_tr a s0) R b (f_b (last_st_tr a s0) aa)\<rbrakk> \<Longrightarrow> False
 2. \<And>a b. \<lbrakk>is_matching_fragment sr intsr rvr ctr cres s0 R s f_a; \<forall>tr x s'. (tr, Result (x, s')) \<in> f_a s \<longrightarrow> is_matching_fragment sr osr rvr' ctr' cres' (last_st_tr tr s0) R s' (f_b (last_st_tr tr s0) x); \<forall>s0' x. prefix_closed (f_b s0' x); ctr'' = ctr' @ ctr; cres'' = (case cres of Failed \<Rightarrow> Failed | Incomplete \<Rightarrow> Incomplete | Result prod \<Rightarrow> cres'); cres = Incomplete \<longrightarrow> ctr' = []; cres = Failed \<longrightarrow> ctr' = []; (a, b) \<in> mbind f_a f_b s0 s\<rbrakk> \<Longrightarrow> rely_cond R s0 a \<and> matching_tr_pfx sr a (ctr' @ ctr) \<and> (length a < length ctr' + length ctr \<longrightarrow> b = Incomplete) \<and> (length a = length ctr' + length ctr \<longrightarrow> rel_tmres osr rvr' b (case cres of Failed \<Rightarrow> Failed | Incomplete \<Rightarrow> Incomplete | Result prod \<Rightarrow> cres')) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>is_matching_fragment sr intsr rvr ctr cres s0 R s f_a; \<forall>tr x s'. (tr, Result (x, s')) \<in> f_a s \<longrightarrow> is_matching_fragment sr osr rvr' ctr' cres' (last_st_tr tr s0) R s' (f_b (last_st_tr tr s0) x); \<forall>s0' x. prefix_closed (f_b s0' x); ctr'' = ctr' @ ctr; cres'' = (case cres of Failed \<Rightarrow> Failed | Incomplete \<Rightarrow> Incomplete | Result prod \<Rightarrow> cres'); cres = Incomplete \<longrightarrow> ctr' = []; cres = Failed \<longrightarrow> ctr' = []; (a, b) \<in> mbind f_a f_b s0 s\<rbrakk> \<Longrightarrow> rely_cond R s0 a \<and> matching_tr_pfx sr a (ctr' @ ctr) \<and> (length a < length ctr' + length ctr \<longrightarrow> b = Incomplete) \<and> (length a = length ctr' + length ctr \<longrightarrow> rel_tmres osr rvr' b (case cres of Failed \<Rightarrow> Failed | Incomplete \<Rightarrow> Incomplete | Result prod \<Rightarrow> cres')) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>is_matching_fragment sr intsr rvr ctr cres s0 R s f_a; \<forall>tr x s'. (tr, Result (x, s')) \<in> f_a s \<longrightarrow> is_matching_fragment sr osr rvr' ctr' cres' (last_st_tr tr s0) R s' (f_b (last_st_tr tr s0) x); \<forall>s0' x. prefix_closed (f_b s0' x); ctr'' = ctr' @ ctr; cres'' = (case cres of Failed \<Rightarrow> Failed | Incomplete \<Rightarrow> Incomplete | Result prod \<Rightarrow> cres'); cres = Incomplete \<longrightarrow> ctr' = []; cres = Failed \<longrightarrow> ctr' = []; (aa, ba) \<in> f_a s; (a, b) \<in> (case ba of Failed \<Rightarrow> {(aa, Failed)} | Incomplete \<Rightarrow> {(aa, Incomplete)} | Result (rv, s) \<Rightarrow> (\<lambda>(a, y). (a @ aa, y)) ` f_b (last_st_tr aa s0) rv s)\<rbrakk> \<Longrightarrow> rely_cond R s0 a \<and> matching_tr_pfx sr a (ctr' @ ctr) \<and> (length a < length ctr' + length ctr \<longrightarrow> b = Incomplete) \<and> (length a = length ctr' + length ctr \<longrightarrow> rel_tmres osr rvr' b (case cres of Failed \<Rightarrow> Failed | Incomplete \<Rightarrow> Incomplete | Result prod \<Rightarrow> cres')) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>\<forall>tr x s'. (tr, Result (x, s')) \<in> f_a s \<longrightarrow> is_matching_fragment sr osr rvr' ctr' cres' (last_st_tr tr s0) R s' (f_b (last_st_tr tr s0) x); \<forall>s0' x. prefix_closed (f_b s0' x); ctr'' = ctr' @ ctr; cres'' = (case cres of Failed \<Rightarrow> Failed | Incomplete \<Rightarrow> Incomplete | Result prod \<Rightarrow> cres'); cres = Incomplete \<longrightarrow> ctr' = []; cres = Failed \<longrightarrow> ctr' = []; (aa, ba) \<in> f_a s; (a, b) \<in> (case ba of Failed \<Rightarrow> {(aa, Failed)} | Incomplete \<Rightarrow> {(aa, Incomplete)} | Result (rv, s) \<Rightarrow> (\<lambda>(a, y). (a @ aa, y)) ` f_b (last_st_tr aa s0) rv s); rely_cond R s0 aa \<and> matching_tr_pfx sr aa ctr \<and> (length aa < length ctr \<longrightarrow> ba = Incomplete) \<and> (length aa = length ctr \<longrightarrow> rel_tmres intsr rvr ba cres)\<rbrakk> \<Longrightarrow> rely_cond R s0 a \<and> matching_tr_pfx sr a (ctr' @ ctr) \<and> (length a < length ctr' + length ctr \<longrightarrow> b = Incomplete) \<and> (length a = length ctr' + length ctr \<longrightarrow> rel_tmres osr rvr' b (case cres of Failed \<Rightarrow> Failed | Incomplete \<Rightarrow> Incomplete | Result prod \<Rightarrow> cres')) proof (prove)
goal (1 subgoal):
 1. \<And>aa ab bb ac bc ad bd. \<lbrakk>\<forall>tr x s'. (tr, Result (x, s')) \<in> f_a s \<longrightarrow> is_matching_fragment sr osr rvr' ctr' cres' (last_st_tr tr s0) R s' (f_b (last_st_tr tr s0) x); \<forall>s0' x. prefix_closed (f_b s0' x); ctr'' = ctr' @ ctr; rely_cond R s0 aa; matching_tr sr (rev aa) (rev ctr); length aa = length ctr; cres = Result (ab, bb); cres'' = cres'; (aa, Result (ac, bc)) \<in> f_a s; (ad, bd) \<in> f_b (last_st_tr aa s0) ac bc; rvr ac ab; intsr bc bb\<rbrakk> \<Longrightarrow> rely_cond R s0 (ad @ aa) \<and> length ad \<le> length ctr' \<and> matching_tr sr (rev aa @ rev ad) (rev ctr @ take (length ad) (rev ctr')) \<and> (length ad < length ctr' \<longrightarrow> bd = Incomplete) \<and> (length ad = length ctr' \<longrightarrow> rel_tmres osr rvr' bd cres') proof (prove)
goal (1 subgoal):
 1. \<And>aa ab bb ac bc ad bd. \<lbrakk>\<forall>s0' x. prefix_closed (f_b s0' x); ctr'' = ctr' @ ctr; rely_cond R s0 aa; matching_tr sr (rev aa) (rev ctr); length aa = length ctr; cres = Result (ab, bb); cres'' = cres'; (aa, Result (ac, bc)) \<in> f_a s; (ad, bd) \<in> f_b (last_st_tr aa s0) ac bc; rvr ac ab; intsr bc bb; is_matching_fragment sr osr rvr' ctr' cres' (last_st_tr aa s0) R bc (f_b (last_st_tr aa s0) ac)\<rbrakk> \<Longrightarrow> rely_cond R s0 (ad @ aa) \<and> length ad \<le> length ctr' \<and> matching_tr sr (rev aa @ rev ad) (rev ctr @ take (length ad) (rev ctr')) \<and> (length ad < length ctr' \<longrightarrow> bd = Incomplete) \<and> (length ad = length ctr' \<longrightarrow> rel_tmres osr rvr' bd cres') proof (prove)
goal (1 subgoal):
 1. \<And>aa ab bb ac bc ad bd. \<lbrakk>\<forall>s0' x. prefix_closed (f_b s0' x); ctr'' = ctr' @ ctr; rely_cond R s0 aa; matching_tr sr (rev aa) (rev ctr); length aa = length ctr; cres = Result (ab, bb); cres'' = cres'; (aa, Result (ac, bc)) \<in> f_a s; (ad, bd) \<in> f_b (last_st_tr aa s0) ac bc; rvr ac ab; intsr bc bb; rely_cond R (last_st_tr aa s0) ad \<and> matching_tr_pfx sr ad ctr' \<and> (length ad < length ctr' \<longrightarrow> bd = Incomplete) \<and> (length ad = length ctr' \<longrightarrow> rel_tmres osr rvr' bd cres')\<rbrakk> \<Longrightarrow> rely_cond R s0 (ad @ aa) \<and> length ad \<le> length ctr' \<and> matching_tr sr (rev aa @ rev ad) (rev ctr @ take (length ad) (rev ctr')) \<and> (length ad < length ctr' \<longrightarrow> bd = Incomplete) \<and> (length ad = length ctr' \<longrightarrow> rel_tmres osr rvr' bd cres') proof (prove)
goal:
No subgoals!