theory Prefix_Refinement

lemma is_matching_fragment_add_rely:
  "is_matching_fragment sr osr r ctr cres s0 AR s f
    \<Longrightarrow> AR' \<le> AR
    \<Longrightarrow> is_matching_fragment sr osr r ctr cres s0 AR' s (rely f AR' s0)" apply (frule is_matching_fragment_Nil) apply (clarsimp simp: is_matching_fragment_def prefix_closed_rely
                        rely_self_closed) apply (intro conjI) apply (erule rely_env_closed) apply (frule rely_cond_mono) apply (simp add: le_fun_def rely_cond_Cons_eq) apply (fastforce simp: rely_def) apply (auto simp: rely_def)[1] done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_matching_fragment sr osr r ctr cres s0 AR s f; AR' \<le> AR\<rbrakk> \<Longrightarrow> is_matching_fragment sr osr r ctr cres s0 AR' s (rely f AR' s0) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_matching_fragment sr osr r ctr cres s0 AR s f; AR' \<le> AR; [] \<in> fst ` f s\<rbrakk> \<Longrightarrow> is_matching_fragment sr osr r ctr cres s0 AR' s (rely f AR' s0) proof (prove)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>AR' \<le> AR; ([], b) \<in> f s; prefix_closed f; self_closed (\<lambda>xs. length xs < length ctr \<and> fst (rev ctr ! length xs) = Me) s f; env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond AR s0 ((Env, s) # xs)) s f; f s \<noteq> {}; \<forall>x\<in>f s. case x of (tr, res) \<Rightarrow> rely_cond AR s0 tr \<and> matching_tr_pfx sr tr ctr \<and> (length tr < length ctr \<longrightarrow> res = Incomplete) \<and> (length tr = length ctr \<longrightarrow> rel_tmres osr r res cres)\<rbrakk> \<Longrightarrow> env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond AR' s0 ((Env, s) # xs)) s (rely f AR' s0) \<and> rely f AR' s0 s \<noteq> {} \<and> (\<forall>x\<in>rely f AR' s0 s. case x of (tr, res) \<Rightarrow> rely_cond AR' s0 tr \<and> matching_tr_pfx sr tr ctr \<and> (length tr < length ctr \<longrightarrow> res = Incomplete) \<and> (length tr = length ctr \<longrightarrow> rel_tmres osr r res cres)) proof (prove)
goal (3 subgoals):
 1. \<And>b. \<lbrakk>AR' \<le> AR; ([], b) \<in> f s; prefix_closed f; self_closed (\<lambda>xs. length xs < length ctr \<and> fst (rev ctr ! length xs) = Me) s f; env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond AR s0 ((Env, s) # xs)) s f; f s \<noteq> {}; \<forall>x\<in>f s. case x of (tr, res) \<Rightarrow> rely_cond AR s0 tr \<and> matching_tr_pfx sr tr ctr \<and> (length tr < length ctr \<longrightarrow> res = Incomplete) \<and> (length tr = length ctr \<longrightarrow> rel_tmres osr r res cres)\<rbrakk> \<Longrightarrow> env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond AR' s0 ((Env, s) # xs)) s (rely f AR' s0)
 2. \<And>b. \<lbrakk>AR' \<le> AR; ([], b) \<in> f s; prefix_closed f; self_closed (\<lambda>xs. length xs < length ctr \<and> fst (rev ctr ! length xs) = Me) s f; env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond AR s0 ((Env, s) # xs)) s f; f s \<noteq> {}; \<forall>x\<in>f s. case x of (tr, res) \<Rightarrow> rely_cond AR s0 tr \<and> matching_tr_pfx sr tr ctr \<and> (length tr < length ctr \<longrightarrow> res = Incomplete) \<and> (length tr = length ctr \<longrightarrow> rel_tmres osr r res cres)\<rbrakk> \<Longrightarrow> rely f AR' s0 s \<noteq> {}
 3. \<And>b. \<lbrakk>AR' \<le> AR; ([], b) \<in> f s; prefix_closed f; self_closed (\<lambda>xs. length xs < length ctr \<and> fst (rev ctr ! length xs) = Me) s f; env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond AR s0 ((Env, s) # xs)) s f; f s \<noteq> {}; \<forall>x\<in>f s. case x of (tr, res) \<Rightarrow> rely_cond AR s0 tr \<and> matching_tr_pfx sr tr ctr \<and> (length tr < length ctr \<longrightarrow> res = Incomplete) \<and> (length tr = length ctr \<longrightarrow> rel_tmres osr r res cres)\<rbrakk> \<Longrightarrow> \<forall>x\<in>rely f AR' s0 s. case x of (tr, res) \<Rightarrow> rely_cond AR' s0 tr \<and> matching_tr_pfx sr tr ctr \<and> (length tr < length ctr \<longrightarrow> res = Incomplete) \<and> (length tr = length ctr \<longrightarrow> rel_tmres osr r res cres) proof (prove)
goal (3 subgoals):
 1. \<And>b. \<lbrakk>AR' \<le> AR; ([], b) \<in> f s; prefix_closed f; self_closed (\<lambda>xs. length xs < length ctr \<and> fst (rev ctr ! length xs) = Me) s f; f s \<noteq> {}; \<forall>x\<in>f s. case x of (tr, res) \<Rightarrow> rely_cond AR s0 tr \<and> matching_tr_pfx sr tr ctr \<and> (length tr < length ctr \<longrightarrow> res = Incomplete) \<and> (length tr = length ctr \<longrightarrow> rel_tmres osr r res cres)\<rbrakk> \<Longrightarrow> \<forall>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond AR' s0 ((Env, s) # xs) \<longrightarrow> rely_cond AR' s0 xs \<longrightarrow> (matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond AR s0 ((Env, s) # xs)) \<and> AR' (last_st_tr xs s0) s
 2. \<And>b. \<lbrakk>AR' \<le> AR; ([], b) \<in> f s; prefix_closed f; self_closed (\<lambda>xs. length xs < length ctr \<and> fst (rev ctr ! length xs) = Me) s f; env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond AR s0 ((Env, s) # xs)) s f; f s \<noteq> {}; \<forall>x\<in>f s. case x of (tr, res) \<Rightarrow> rely_cond AR s0 tr \<and> matching_tr_pfx sr tr ctr \<and> (length tr < length ctr \<longrightarrow> res = Incomplete) \<and> (length tr = length ctr \<longrightarrow> rel_tmres osr r res cres)\<rbrakk> \<Longrightarrow> rely f AR' s0 s \<noteq> {}
 3. \<And>b. \<lbrakk>AR' \<le> AR; ([], b) \<in> f s; prefix_closed f; self_closed (\<lambda>xs. length xs < length ctr \<and> fst (rev ctr ! length xs) = Me) s f; env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond AR s0 ((Env, s) # xs)) s f; f s \<noteq> {}; \<forall>x\<in>f s. case x of (tr, res) \<Rightarrow> rely_cond AR s0 tr \<and> matching_tr_pfx sr tr ctr \<and> (length tr < length ctr \<longrightarrow> res = Incomplete) \<and> (length tr = length ctr \<longrightarrow> rel_tmres osr r res cres)\<rbrakk> \<Longrightarrow> \<forall>x\<in>rely f AR' s0 s. case x of (tr, res) \<Rightarrow> rely_cond AR' s0 tr \<and> matching_tr_pfx sr tr ctr \<and> (length tr < length ctr \<longrightarrow> res = Incomplete) \<and> (length tr = length ctr \<longrightarrow> rel_tmres osr r res cres) proof (prove)
goal (3 subgoals):
 1. \<And>b. \<lbrakk>AR' \<le> AR; ([], b) \<in> f s; prefix_closed f; self_closed (\<lambda>xs. length xs < length ctr \<and> fst (rev ctr ! length xs) = Me) s f; f s \<noteq> {}; \<forall>x\<in>f s. case x of (tr, res) \<Rightarrow> rely_cond AR s0 tr \<and> matching_tr_pfx sr tr ctr \<and> (length tr < length ctr \<longrightarrow> res = Incomplete) \<and> (length tr = length ctr \<longrightarrow> rel_tmres osr r res cres); rely_cond AR' \<le> rely_cond AR\<rbrakk> \<Longrightarrow> \<forall>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond AR' s0 ((Env, s) # xs) \<longrightarrow> rely_cond AR' s0 xs \<longrightarrow> (matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond AR s0 ((Env, s) # xs)) \<and> AR' (last_st_tr xs s0) s
 2. \<And>b. \<lbrakk>AR' \<le> AR; ([], b) \<in> f s; prefix_closed f; self_closed (\<lambda>xs. length xs < length ctr \<and> fst (rev ctr ! length xs) = Me) s f; env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond AR s0 ((Env, s) # xs)) s f; f s \<noteq> {}; \<forall>x\<in>f s. case x of (tr, res) \<Rightarrow> rely_cond AR s0 tr \<and> matching_tr_pfx sr tr ctr \<and> (length tr < length ctr \<longrightarrow> res = Incomplete) \<and> (length tr = length ctr \<longrightarrow> rel_tmres osr r res cres)\<rbrakk> \<Longrightarrow> rely f AR' s0 s \<noteq> {}
 3. \<And>b. \<lbrakk>AR' \<le> AR; ([], b) \<in> f s; prefix_closed f; self_closed (\<lambda>xs. length xs < length ctr \<and> fst (rev ctr ! length xs) = Me) s f; env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond AR s0 ((Env, s) # xs)) s f; f s \<noteq> {}; \<forall>x\<in>f s. case x of (tr, res) \<Rightarrow> rely_cond AR s0 tr \<and> matching_tr_pfx sr tr ctr \<and> (length tr < length ctr \<longrightarrow> res = Incomplete) \<and> (length tr = length ctr \<longrightarrow> rel_tmres osr r res cres)\<rbrakk> \<Longrightarrow> \<forall>x\<in>rely f AR' s0 s. case x of (tr, res) \<Rightarrow> rely_cond AR' s0 tr \<and> matching_tr_pfx sr tr ctr \<and> (length tr < length ctr \<longrightarrow> res = Incomplete) \<and> (length tr = length ctr \<longrightarrow> rel_tmres osr r res cres) proof (prove)
goal (2 subgoals):
 1. \<And>b. \<lbrakk>AR' \<le> AR; ([], b) \<in> f s; prefix_closed f; self_closed (\<lambda>xs. length xs < length ctr \<and> fst (rev ctr ! length xs) = Me) s f; env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond AR s0 ((Env, s) # xs)) s f; f s \<noteq> {}; \<forall>x\<in>f s. case x of (tr, res) \<Rightarrow> rely_cond AR s0 tr \<and> matching_tr_pfx sr tr ctr \<and> (length tr < length ctr \<longrightarrow> res = Incomplete) \<and> (length tr = length ctr \<longrightarrow> rel_tmres osr r res cres)\<rbrakk> \<Longrightarrow> rely f AR' s0 s \<noteq> {}
 2. \<And>b. \<lbrakk>AR' \<le> AR; ([], b) \<in> f s; prefix_closed f; self_closed (\<lambda>xs. length xs < length ctr \<and> fst (rev ctr ! length xs) = Me) s f; env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond AR s0 ((Env, s) # xs)) s f; f s \<noteq> {}; \<forall>x\<in>f s. case x of (tr, res) \<Rightarrow> rely_cond AR s0 tr \<and> matching_tr_pfx sr tr ctr \<and> (length tr < length ctr \<longrightarrow> res = Incomplete) \<and> (length tr = length ctr \<longrightarrow> rel_tmres osr r res cres)\<rbrakk> \<Longrightarrow> \<forall>x\<in>rely f AR' s0 s. case x of (tr, res) \<Rightarrow> rely_cond AR' s0 tr \<and> matching_tr_pfx sr tr ctr \<and> (length tr < length ctr \<longrightarrow> res = Incomplete) \<and> (length tr = length ctr \<longrightarrow> rel_tmres osr r res cres) proof (prove)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>AR' \<le> AR; ([], b) \<in> f s; prefix_closed f; self_closed (\<lambda>xs. length xs < length ctr \<and> fst (rev ctr ! length xs) = Me) s f; env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) ctr \<and> rely_cond AR s0 ((Env, s) # xs)) s f; f s \<noteq> {}; \<forall>x\<in>f s. case x of (tr, res) \<Rightarrow> rely_cond AR s0 tr \<and> matching_tr_pfx sr tr ctr \<and> (length tr < length ctr \<longrightarrow> res = Incomplete) \<and> (length tr = length ctr \<longrightarrow> rel_tmres osr r res cres)\<rbrakk> \<Longrightarrow> \<forall>x\<in>rely f AR' s0 s. case x of (tr, res) \<Rightarrow> rely_cond AR' s0 tr \<and> matching_tr_pfx sr tr ctr \<and> (length tr < length ctr \<longrightarrow> res = Incomplete) \<and> (length tr = length ctr \<longrightarrow> rel_tmres osr r res cres) proof (prove)
goal:
No subgoals!