theory Prefix_Refinement

lemma prefix_refinement_weaken_rel:
  "prefix_refinement sr isr osr r P Q AR R f g
    \<Longrightarrow> \<forall>rv rv'. r rv rv' \<longrightarrow> r' rv rv'
    \<Longrightarrow> prefix_refinement sr isr osr r' P Q AR R f g" apply (subst prefix_refinement_def, clarsimp) apply (drule(5) prefix_refinementD, clarsimp) apply (rule exI, rule conjI[rotated], assumption) apply (clarsimp simp: is_matching_fragment_def) apply (drule(1) bspec, clarsimp) apply (erule tmres.rel_cases; clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prefix_refinement sr isr osr r P Q AR R f g; \<forall>rv rv'. r rv rv' \<longrightarrow> r' rv rv'\<rbrakk> \<Longrightarrow> prefix_refinement sr isr osr r' P Q AR R f g proof (prove)
goal (1 subgoal):
 1. \<And>s s0 t0 t a b. \<lbrakk>prefix_refinement sr isr osr r P Q AR R f g; \<forall>rv rv'. r rv rv' \<longrightarrow> r' rv rv'; isr s t; P s0 s; sr s0 t0; Q t0 t; (a, b) \<in> g t; rely_cond R t0 a\<rbrakk> \<Longrightarrow> \<exists>fa. is_matching_fragment sr osr r' a b s0 AR s fa \<and> triv_refinement f fa proof (prove)
goal (1 subgoal):
 1. \<And>s s0 t0 t a b fa. \<lbrakk>\<forall>rv rv'. r rv rv' \<longrightarrow> r' rv rv'; isr s t; P s0 s; sr s0 t0; Q t0 t; (a, b) \<in> g t; rely_cond R t0 a; is_matching_fragment sr osr r a b s0 AR s fa; triv_refinement f fa\<rbrakk> \<Longrightarrow> \<exists>fa. is_matching_fragment sr osr r' a b s0 AR s fa \<and> triv_refinement f fa proof (prove)
goal (1 subgoal):
 1. \<And>s s0 t0 t a b fa. \<lbrakk>\<forall>rv rv'. r rv rv' \<longrightarrow> r' rv rv'; isr s t; P s0 s; sr s0 t0; Q t0 t; (a, b) \<in> g t; rely_cond R t0 a; is_matching_fragment sr osr r a b s0 AR s fa; triv_refinement f fa\<rbrakk> \<Longrightarrow> is_matching_fragment sr osr r' a b s0 AR s fa proof (prove)
goal (1 subgoal):
 1. \<And>s s0 t0 t a b fa aa ba. \<lbrakk>\<forall>rv rv'. r rv rv' \<longrightarrow> r' rv rv'; isr s t; P s0 s; sr s0 t0; Q t0 t; (a, b) \<in> g t; rely_cond R t0 a; triv_refinement f fa; (aa, ba) \<in> fa s; prefix_closed fa; self_closed (\<lambda>xs. length xs < length a \<and> fst (rev a ! length xs) = Me) s fa; env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) a \<and> rely_cond AR s0 ((Env, s) # xs)) s fa; fa s \<noteq> {}; \<forall>x\<in>fa s. case x of (tr, res) \<Rightarrow> rely_cond AR s0 tr \<and> matching_tr_pfx sr tr a \<and> (length tr < length a \<longrightarrow> res = Incomplete) \<and> (length tr = length a \<longrightarrow> rel_tmres osr r res b)\<rbrakk> \<Longrightarrow> rely_cond AR s0 aa \<and> matching_tr_pfx sr aa a \<and> (length aa < length a \<longrightarrow> ba = Incomplete) \<and> (length aa = length a \<longrightarrow> rel_tmres osr r' ba b) proof (prove)
goal (1 subgoal):
 1. \<And>s s0 t0 t a b fa aa ba. \<lbrakk>\<forall>rv rv'. r rv rv' \<longrightarrow> r' rv rv'; isr s t; P s0 s; sr s0 t0; Q t0 t; (a, b) \<in> g t; rely_cond R t0 a; triv_refinement f fa; (aa, ba) \<in> fa s; prefix_closed fa; self_closed (\<lambda>xs. length xs < length a \<and> fst (rev a ! length xs) = Me) s fa; env_closed (\<lambda>xs s. matching_tr_pfx sr ((Env, s) # xs) a \<and> rely_cond AR s0 ((Env, s) # xs)) s fa; fa s \<noteq> {}; rely_cond AR s0 aa; matching_tr_pfx sr aa a; length aa = length a; rel_tmres osr r ba b\<rbrakk> \<Longrightarrow> rel_tmres osr r' ba b proof (prove)
goal:
No subgoals!