theory Prefix_Refinement

lemma prefix_refinement_weaken_rely:
  "prefix_refinement sr isr osr r P Q AR R f g
    \<Longrightarrow> R' \<le> R \<Longrightarrow> AR' \<le> AR
    \<Longrightarrow> prefix_refinement sr isr osr r P Q AR' R' f g" apply (subst prefix_refinement_def, clarsimp) apply (drule(3) prefix_refinementD, assumption+) apply (clarsimp simp: rely_cond_def split_def le_fun_def) apply (rule exI, rule conjI, erule is_matching_fragment_add_rely) apply (simp add: le_fun_def) apply (auto simp add: triv_refinement_def rely_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prefix_refinement sr isr osr r P Q AR R f g; R' \<le> R; AR' \<le> AR\<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; R' \<le> R; AR' \<le> AR; 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>R' \<le> R; AR' \<le> AR; isr s t; P s0 s; sr s0 t0; Q t0 t; (a, b) \<in> g t; rely_cond R' t0 a; 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>\<forall>x xa. R' x xa \<longrightarrow> R x xa; \<forall>x xa. AR' x xa \<longrightarrow> AR x xa; isr s t; P s0 s; sr s0 t0; Q t0 t; (a, b) \<in> g t; \<forall>x\<in>trace_steps (rev a) t0. fst x = Env \<longrightarrow> R' (fst (snd x)) (snd (snd x)); 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 (2 subgoals):
 1. \<And>s s0 t0 t a b fa. \<lbrakk>\<forall>x xa. R' x xa \<longrightarrow> R x xa; \<forall>x xa. AR' x xa \<longrightarrow> AR x xa; isr s t; P s0 s; sr s0 t0; Q t0 t; (a, b) \<in> g t; \<forall>x\<in>trace_steps (rev a) t0. fst x = Env \<longrightarrow> R' (fst (snd x)) (snd (snd x)); triv_refinement f fa\<rbrakk> \<Longrightarrow> AR' \<le> AR
 2. \<And>s s0 t0 t a b fa. \<lbrakk>\<forall>x xa. R' x xa \<longrightarrow> R x xa; \<forall>x xa. AR' x xa \<longrightarrow> AR x xa; isr s t; P s0 s; sr s0 t0; Q t0 t; (a, b) \<in> g t; \<forall>x\<in>trace_steps (rev a) t0. fst x = Env \<longrightarrow> R' (fst (snd x)) (snd (snd x)); is_matching_fragment sr osr r a b s0 AR s fa; triv_refinement f fa\<rbrakk> \<Longrightarrow> triv_refinement f (rely fa AR' s0) proof (prove)
goal (1 subgoal):
 1. \<And>s s0 t0 t a b fa. \<lbrakk>\<forall>x xa. R' x xa \<longrightarrow> R x xa; \<forall>x xa. AR' x xa \<longrightarrow> AR x xa; isr s t; P s0 s; sr s0 t0; Q t0 t; (a, b) \<in> g t; \<forall>x\<in>trace_steps (rev a) t0. fst x = Env \<longrightarrow> R' (fst (snd x)) (snd (snd x)); is_matching_fragment sr osr r a b s0 AR s fa; triv_refinement f fa\<rbrakk> \<Longrightarrow> triv_refinement f (rely fa AR' s0) proof (prove)
goal:
No subgoals!