theory Prefix_Refinement

lemma prefix_refinement_weaken_srs:
  "prefix_refinement sr isr osr r P Q AR R f g
    \<Longrightarrow> isr' \<le> isr \<Longrightarrow> osr \<le> osr' \<Longrightarrow> sr \<le> sr
    \<Longrightarrow> prefix_refinement sr isr' osr' r P Q AR R f g" apply (subst prefix_refinement_def, clarsimp) apply (drule(1) predicate2D) apply (drule(5) prefix_refinementD) apply 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) apply (erule(1) predicate2D) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prefix_refinement sr isr osr r P Q AR R f g; isr' \<le> isr; osr \<le> osr'; sr \<le> sr\<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; isr' \<le> isr; osr \<le> osr'; 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. \<lbrakk>prefix_refinement sr isr osr r P Q AR R f g; osr \<le> osr'; isr' s t; P s0 s; sr s0 t0; Q t0 t; (a, b) \<in> g t; rely_cond R t0 a; isr s t\<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. \<lbrakk>osr \<le> osr'; isr' s t; P s0 s; sr s0 t0; Q t0 t; (a, b) \<in> g t; rely_cond R t0 a; isr s t; case (a, b) of (ctr, cres) \<Rightarrow> rely_cond R t0 ctr \<longrightarrow> (\<exists>fa. is_matching_fragment sr osr r ctr cres s0 AR s fa \<and> 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>osr \<le> osr'; isr' s t; P s0 s; sr s0 t0; Q t0 t; (a, b) \<in> g t; rely_cond R t0 a; isr s t; 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>osr \<le> osr'; isr' s t; P s0 s; sr s0 t0; Q t0 t; (a, b) \<in> g t; rely_cond R t0 a; isr s t; 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>osr \<le> osr'; isr' s t; P s0 s; sr s0 t0; Q t0 t; (a, b) \<in> g t; rely_cond R t0 a; isr s t; 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>osr \<le> osr'; isr' s t; P s0 s; sr s0 t0; Q t0 t; (a, b) \<in> g t; rely_cond R t0 a; isr s t; 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 (1 subgoal):
 1. \<And>s s0 t0 t a fa aa ab bb ac bc. \<lbrakk>osr \<le> osr'; isr' s t; P s0 s; sr s0 t0; Q t0 t; (a, Result (ac, bc)) \<in> g t; rely_cond R t0 a; isr s t; triv_refinement f fa; (aa, Result (ab, bb)) \<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; r ab ac; osr bb bc\<rbrakk> \<Longrightarrow> osr' bb bc proof (prove)
goal:
No subgoals!