kings-crown/FVELER_Isabelle huggingface dataset:
theory Prefix_Refinement

lemma tr_in_parallel_validI:
  assumes elem: "(tr, res) \<in> parallel (K {(f_tr, res)}) (K {(g_tr, res)}) s"
  and trs: "(f_tr, res) \<in> f s" "(g_tr, res) \<in> g s"
  and validI: "\<lbrace>P\<rbrace>, \<lbrace>E or Gg\<rbrace> f \<lbrace>Gf\<rbrace>, \<lbrace>Q\<rbrace>" "\<lbrace>P\<rbrace>, \<lbrace>E or Gf\<rbrace> g \<lbrace>Gg\<rbrace>, \<lbrace>Q2\<rbrace>"
  and P: "P s0 s" and rel: "rely_cond E s0 tr"
  shows "rely_cond (E or Gg) s0 f_tr \<and> rely_cond (E or Gf) s0 g_tr" using parallel_rely_induct0[where R=E and G="\<top>\<top>", OF elem _ _ validI, OF P P] by (clarsimp simp: rel trs predicate2I)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rely_cond (E or Gg) s0 f_tr \<and> rely_cond (E or Gf) s0 g_tr proof (prove)
using this:
\<lbrakk>K {(f_tr, res)} s \<subseteq> f s; K {(g_tr, res)} s \<subseteq> g s; E \<le> (E or Gg); E \<le> (E or Gf); Gf \<le> (\<lambda>_ _. True); Gg \<le> (\<lambda>_ _. True); Gf \<le> (E or Gf); Gg \<le> (E or Gg); rely_cond E s0 tr\<rbrakk> \<Longrightarrow> \<exists>tr_f. (tr_f, res) \<in> K {(f_tr, res)} s \<and> (\<exists>tr_g. (tr_g, res) \<in> K {(g_tr, res)} s \<and> rely_cond (E or Gg) s0 tr_f \<and> rely_cond (E or Gf) s0 tr_g \<and> map snd tr_f = map snd tr \<and> map snd tr_g = map snd tr \<and> (\<forall>i\<le>length tr. last_st_tr (drop i tr_g) s0 = last_st_tr (drop i tr_f) s0) \<and> guar_cond (\<lambda>_ _. True) s0 tr)

goal (1 subgoal):
 1. rely_cond (E or Gg) s0 f_tr \<and> rely_cond (E or Gf) s0 g_tr
theory Prefix_Refinement

lemma is_matching_fragment_validI_disj:
  "is_matching_fragment sr osr rvr b_tr bd_res s0 R s f
    \<Longrightarrow> triv_refinement g f
    \<Longrightarrow> G = \<top>\<top> \<or> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> g \<lbrace>G\<rbrace>,\<lbrace>\<lambda>_ _ _. True\<rbrace>
    \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>_ _ _. True\<rbrace>" apply (frule is_matching_fragment_prefix_closed) apply (erule disjE) apply (simp add: validI_def guar_cond_def) apply (erule(2) validI_triv_refinement) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_matching_fragment sr osr rvr b_tr bd_res s0 R s f; triv_refinement g f; G = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> g \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_matching_fragment sr osr rvr b_tr bd_res s0 R s f; triv_refinement g f; G = (\<lambda>_ _. True) \<or> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> g \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>; prefix_closed f\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_matching_fragment sr osr rvr b_tr bd_res s0 R s f; triv_refinement g f; prefix_closed f; G = (\<lambda>_ _. True)\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>
 2. \<lbrakk>is_matching_fragment sr osr rvr b_tr bd_res s0 R s f; triv_refinement g f; prefix_closed f; \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> g \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_matching_fragment sr osr rvr b_tr bd_res s0 R s f; triv_refinement g f; prefix_closed f; \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> g \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_ _ _. True\<rbrace> proof (prove)
goal:
No subgoals!
theory Prefix_Refinement

lemma prefix_closed_rely:
  "prefix_closed f \<Longrightarrow> prefix_closed (rely f R s0)" apply (subst prefix_closed_def, clarsimp simp: rely_def rely_cond_Cons_eq) apply (erule(1) prefix_closedD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. prefix_closed f \<Longrightarrow> prefix_closed (rely f R s0) proof (prove)
goal (1 subgoal):
 1. \<And>s a b xs ba. \<lbrakk>prefix_closed f; ((a, b) # xs, ba) \<in> f s; rely_cond R s0 xs; a = Env \<longrightarrow> R (last_st_tr xs s0) b\<rbrakk> \<Longrightarrow> (xs, Incomplete) \<in> f s proof (prove)
goal:
No subgoals!
theory Prefix_Refinement

lemma rely_self_closed:
  "self_closed P s f \<Longrightarrow> self_closed P s (rely f R s0)" apply (subst self_closed_def, clarsimp simp: rely_def rely_cond_Cons_eq) apply (drule(2) self_closedD) apply (fastforce simp: rely_cond_Cons_eq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. self_closed P s f \<Longrightarrow> self_closed P s (rely f R s0) proof (prove)
goal (1 subgoal):
 1. \<And>xs. \<lbrakk>self_closed P s f; (xs, Incomplete) \<in> f s; rely_cond R s0 xs; P xs\<rbrakk> \<Longrightarrow> \<exists>s'. (Me, s') # xs \<in> fst ` (f s \<inter> Collect (rely_cond R s0) \<times> UNIV) proof (prove)
goal (1 subgoal):
 1. \<And>xs. \<lbrakk>(xs, Incomplete) \<in> f s; rely_cond R s0 xs; P xs; \<exists>s'. (Me, s') # xs \<in> fst ` f s\<rbrakk> \<Longrightarrow> \<exists>s'. (Me, s') # xs \<in> fst ` (f s \<inter> Collect (rely_cond R s0) \<times> UNIV) proof (prove)
goal:
No subgoals!
theory Prefix_Refinement

lemma rely_env_closed:
  "env_closed P s f
    \<Longrightarrow> (\<forall>xs s. P' xs s \<longrightarrow> rely_cond R s0 xs \<longrightarrow> P xs s \<and> R (last_st_tr xs s0) s)
    \<Longrightarrow> env_closed P' s (rely f R s0)" apply (subst env_closed_def, clarsimp simp: rely_def) apply (drule_tac s'=s' in env_closedD, assumption) apply simp apply (clarsimp simp: image_def) apply (fastforce intro: rely_cond_Cons rev_bexI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>env_closed P s f; \<forall>xs s. P' xs s \<longrightarrow> rely_cond R s0 xs \<longrightarrow> P xs s \<and> R (last_st_tr xs s0) s\<rbrakk> \<Longrightarrow> env_closed P' s (rely f R s0) proof (prove)
goal (1 subgoal):
 1. \<And>xs s'. \<lbrakk>env_closed P s f; \<forall>xs s. P' xs s \<longrightarrow> rely_cond R s0 xs \<longrightarrow> P xs s \<and> R (last_st_tr xs s0) s; (xs, Incomplete) \<in> f s; rely_cond R s0 xs; P' xs s'\<rbrakk> \<Longrightarrow> (Env, s') # xs \<in> fst ` (f s \<inter> Collect (rely_cond R s0) \<times> UNIV) proof (prove)
goal (2 subgoals):
 1. \<And>xs s'. \<lbrakk>\<forall>xs s. P' xs s \<longrightarrow> rely_cond R s0 xs \<longrightarrow> P xs s \<and> R (last_st_tr xs s0) s; (xs, Incomplete) \<in> f s; rely_cond R s0 xs; P' xs s'\<rbrakk> \<Longrightarrow> P xs s'
 2. \<And>xs s'. \<lbrakk>\<forall>xs s. P' xs s \<longrightarrow> rely_cond R s0 xs \<longrightarrow> P xs s \<and> R (last_st_tr xs s0) s; (xs, Incomplete) \<in> f s; rely_cond R s0 xs; P' xs s'; (Env, s') # xs \<in> fst ` f s\<rbrakk> \<Longrightarrow> (Env, s') # xs \<in> fst ` (f s \<inter> Collect (rely_cond R s0) \<times> UNIV) proof (prove)
goal (1 subgoal):
 1. \<And>xs s'. \<lbrakk>\<forall>xs s. P' xs s \<longrightarrow> rely_cond R s0 xs \<longrightarrow> P xs s \<and> R (last_st_tr xs s0) s; (xs, Incomplete) \<in> f s; rely_cond R s0 xs; P' xs s'; (Env, s') # xs \<in> fst ` f s\<rbrakk> \<Longrightarrow> (Env, s') # xs \<in> fst ` (f s \<inter> Collect (rely_cond R s0) \<times> UNIV) proof (prove)
goal (1 subgoal):
 1. \<And>xs s' b. \<lbrakk>\<forall>xs s. P' xs s \<longrightarrow> rely_cond R s0 xs \<longrightarrow> P xs s \<and> R (last_st_tr xs s0) s; (xs, Incomplete) \<in> f s; rely_cond R s0 xs; P' xs s'; ((Env, s') # xs, b) \<in> f s\<rbrakk> \<Longrightarrow> \<exists>x\<in>f s \<inter> Collect (rely_cond R s0) \<times> UNIV. (Env, s') # xs = fst x proof (prove)
goal:
No subgoals!
theory Prefix_Refinement

lemma validI_triv':
  "prefix_closed f \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>\<lambda>_ _. True\<rbrace>,\<lbrace>\<lambda>_ _ _. True\<rbrace>" by (simp add: validI_def guar_cond_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. prefix_closed f \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f -, \<lbrace>\<lambda>_ _ _. True\<rbrace>
theory Prefix_Refinement

lemma pfx_trace_set_allD:
  "\<forall>n. \<forall>v\<in>set (take n xs). P n v \<Longrightarrow> v \<in> set (take n xs)
    \<Longrightarrow> P n v" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>n. \<forall>v\<in>set (take n xs). P n v; v \<in> set (take n xs)\<rbrakk> \<Longrightarrow> P n v
theory Prefix_Refinement

lemma prefix_closed_UNION:
   "(\<forall>s' x. x \<in> S s' \<longrightarrow> prefix_closed (f x))
    \<Longrightarrow> prefix_closed (\<lambda>s. \<Union>x \<in> S s. f x s)" apply (simp add: prefix_closed_def) apply (blast intro: in_fst_snd_image) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s' x. x \<in> S s' \<longrightarrow> prefix_closed (f x) \<Longrightarrow> prefix_closed (\<lambda>s. \<Union>x\<in>S s. f x s) proof (prove)
goal (1 subgoal):
 1. \<forall>s' x. x \<in> S s' \<longrightarrow> (\<forall>s a b xs. (a, b) # xs \<in> fst ` f x s \<longrightarrow> (xs, Incomplete) \<in> f x s) \<Longrightarrow> \<forall>s a b xs. (a, b) # xs \<in> fst ` (\<Union>x\<in>S s. f x s) \<longrightarrow> (\<exists>x\<in>S s. (xs, Incomplete) \<in> f x s) proof (prove)
goal:
No subgoals!
theory Prefix_Refinement

lemma matching_tr_pfx_rhs_is_drop:
  fixes ys ys'
  defines "N == length ys - length ys'"
  shows
  "matching_tr_pfx sr xs ys
    \<Longrightarrow> drop N ys = ys'
    \<Longrightarrow> length xs \<le> length ys'
    \<Longrightarrow> matching_tr_pfx sr xs ys'" apply (clarsimp simp: matching_tr_pfx_def) apply (simp add: matching_tr_def list_all2_conv_all_nth
                   min_def) apply (clarsimp simp: rev_nth) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>matching_tr_pfx sr xs ys; drop N ys = ys'; length xs \<le> length ys'\<rbrakk> \<Longrightarrow> matching_tr_pfx sr xs ys' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length xs \<le> length ys - N; ys' = drop N ys; length xs \<le> length ys; matching_tr sr (rev xs) (take (length xs) (rev ys))\<rbrakk> \<Longrightarrow> matching_tr sr (rev xs) (take (length xs) (rev (drop N ys))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length xs \<le> length ys - N; ys' = drop N ys; length xs \<le> length ys; length xs = (if length ys = length xs then length ys else length xs) \<and> (\<forall>i<length xs. (case rev xs ! i of (aid, as) \<Rightarrow> \<lambda>(cid, cs). aid = cid \<and> sr as cs) (rev ys ! i))\<rbrakk> \<Longrightarrow> \<forall>i<length xs. (case rev xs ! i of (aid, as) \<Rightarrow> \<lambda>(cid, cs). aid = cid \<and> sr as cs) (rev (drop N ys) ! i) proof (prove)
goal:
No subgoals!
theory Prefix_Refinement

lemma is_matching_fragment_mresD:
  "is_matching_fragment sr osr rvr ctr cres s0 R s f
    \<Longrightarrow> (x, s') \<in> mres (f s)
    \<Longrightarrow> \<exists>y s''. cres = Result (y, s'') \<and> osr s' s'' \<and> rvr x y" apply (clarsimp simp: mres_def) apply (frule(1) is_matching_fragment_trD) apply (clarsimp simp: matching_tr_pfx_def) apply (erule tmres.rel_cases; clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_matching_fragment sr osr rvr ctr cres s0 R s f; (x, s') \<in> mres (f s)\<rbrakk> \<Longrightarrow> \<exists>y s''. cres = Result (y, s'') \<and> osr s' s'' \<and> rvr x y proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>is_matching_fragment sr osr rvr ctr cres s0 R s f; (a, Result (x, s')) \<in> f s\<rbrakk> \<Longrightarrow> \<exists>y s''. cres = Result (y, s'') \<and> osr s' s'' \<and> rvr x y proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>is_matching_fragment sr osr rvr ctr cres s0 R s f; (a, Result (x, s')) \<in> f s; rely_cond R s0 a \<and> matching_tr_pfx sr a ctr \<and> (length a < length ctr \<longrightarrow> Result (x, s') = Incomplete) \<and> (length a = length ctr \<longrightarrow> rel_tmres osr rvr (Result (x, s')) cres)\<rbrakk> \<Longrightarrow> \<exists>y s''. cres = Result (y, s'') \<and> osr s' s'' \<and> rvr x y proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>is_matching_fragment sr osr rvr ctr cres s0 R s f; (a, Result (x, s')) \<in> f s; rely_cond R s0 a; length a = length ctr; matching_tr sr (rev a) (rev ctr); rel_tmres osr rvr (Result (x, s')) cres\<rbrakk> \<Longrightarrow> \<exists>y s''. cres = Result (y, s'') \<and> osr s' s'' \<and> rvr x y proof (prove)
goal:
No subgoals!
theory Prefix_Refinement

lemma matching_tr_pfx_sr_hd_append:
  "matching_tr_pfx sr tr tr'
    \<Longrightarrow> sr s0 t0
    \<Longrightarrow> length tr \<ge> length tr'
    \<Longrightarrow> sr (hd (map snd tr @ [s0])) (hd (map snd tr' @ [t0]))" apply (clarsimp simp: matching_tr_pfx_def matching_tr_def) apply (erule list.rel_cases; clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>matching_tr_pfx sr tr tr'; sr s0 t0; length tr' \<le> length tr\<rbrakk> \<Longrightarrow> sr (hd (map snd tr @ [s0])) (hd (map snd tr' @ [t0])) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sr s0 t0; length tr = length tr'; list_all2 (\<lambda>(aid, as) (cid, cs). aid = cid \<and> sr as cs) tr tr'\<rbrakk> \<Longrightarrow> sr (hd (map snd tr @ [s0])) (hd (map snd tr' @ [t0])) proof (prove)
goal:
No subgoals!
theory Prefix_Refinement

lemma validI_relyT_mresD:
  "\<lbrace>P'\<rbrace>,\<lbrace>\<top>\<top>\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>P''\<rbrace>
    \<Longrightarrow> (rv, s') \<in> mres (f s)
    \<Longrightarrow> P' s0 s
    \<Longrightarrow> \<exists>s0'. P'' rv s0' s'" apply (clarsimp simp: mres_def) apply (drule(2) validI_rvD) apply (simp add: rely_cond_def) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P'\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>P''\<rbrace>; (rv, s') \<in> mres (f s); P' s0 s\<rbrakk> \<Longrightarrow> \<exists>s0'. P'' rv s0' s' proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>\<lbrace>P'\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>P''\<rbrace>; P' s0 s; (a, Result (rv, s')) \<in> f s\<rbrakk> \<Longrightarrow> \<exists>s0'. P'' rv s0' s' proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>P' s0 s; (a, Result (rv, s')) \<in> f s\<rbrakk> \<Longrightarrow> rely_cond (\<lambda>_ _. True) s0 a
 2. \<And>a. \<lbrakk>P' s0 s; (a, Result (rv, s')) \<in> f s; P'' rv (last_st_tr a s0) s'\<rbrakk> \<Longrightarrow> \<exists>s0'. P'' rv s0' s' proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>P' s0 s; (a, Result (rv, s')) \<in> f s; P'' rv (last_st_tr a s0) s'\<rbrakk> \<Longrightarrow> \<exists>s0'. P'' rv s0' s' proof (prove)
goal:
No subgoals!
theory Prefix_Refinement

lemma prefix_refinement_weaken_pre:
  "prefix_refinement sr isr osr rvr P' Q' AR R f g
    \<Longrightarrow> \<forall>s s0. P s0 s \<longrightarrow> P' s0 s
    \<Longrightarrow> (\<forall>s t s0 t0. isr s t \<longrightarrow> sr s0 t0 \<longrightarrow> P s0 s \<longrightarrow> Q t0 t \<longrightarrow> Q' t0 t)
    \<Longrightarrow> prefix_refinement sr isr osr rvr P Q AR R f g" by (fastforce simp: prefix_refinement_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prefix_refinement sr isr osr rvr P' Q' AR R f g; \<forall>s s0. P s0 s \<longrightarrow> P' s0 s; \<forall>s t s0 t0. isr s t \<longrightarrow> sr s0 t0 \<longrightarrow> P s0 s \<longrightarrow> Q t0 t \<longrightarrow> Q' t0 t\<rbrakk> \<Longrightarrow> prefix_refinement sr isr osr rvr P Q AR R f g
theory Prefix_Refinement

lemma default_prefix_refinement_ex:
  "is_matching_fragment sr osr rvr ctr cres s0 R s
            (\<lambda>s. aprog s \<inter> ({tr'. length tr' \<le> length ctr} \<times> UNIV))
    \<Longrightarrow> \<exists>f. is_matching_fragment sr osr rvr ctr cres s0 R s f
            \<and> triv_refinement aprog f" apply (intro exI conjI, assumption) apply (simp add: triv_refinement_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_matching_fragment sr osr rvr ctr cres s0 R s (\<lambda>s. aprog s \<inter> {tr'. length tr' \<le> length ctr} \<times> UNIV) \<Longrightarrow> \<exists>f. is_matching_fragment sr osr rvr ctr cres s0 R s f \<and> triv_refinement aprog f proof (prove)
goal (1 subgoal):
 1. is_matching_fragment sr osr rvr ctr cres s0 R s (\<lambda>s. aprog s \<inter> {tr'. length tr' \<le> length ctr} \<times> UNIV) \<Longrightarrow> triv_refinement aprog (\<lambda>s. aprog s \<inter> {tr'. length tr' \<le> length ctr} \<times> UNIV) proof (prove)
goal:
No subgoals!
theory Prefix_Refinement

lemma default_prefix_refinement_ex_match_iosr_R:
  "is_matching_fragment sr osr rvr ctr cres s0 R s
            (rely (\<lambda>s. aprog s \<inter> ({tr'. matching_tr_pfx iosr tr' ctr} \<times> UNIV)) R s0)
    \<Longrightarrow> \<exists>f. is_matching_fragment sr osr rvr ctr cres s0 R s f
            \<and> triv_refinement aprog f" apply (intro exI conjI, assumption) apply (clarsimp simp add: triv_refinement_def rely_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_matching_fragment sr osr rvr ctr cres s0 R s (rely (\<lambda>s. aprog s \<inter> {tr'. matching_tr_pfx iosr tr' ctr} \<times> UNIV) R s0) \<Longrightarrow> \<exists>f. is_matching_fragment sr osr rvr ctr cres s0 R s f \<and> triv_refinement aprog f proof (prove)
goal (1 subgoal):
 1. is_matching_fragment sr osr rvr ctr cres s0 R s (rely (\<lambda>s. aprog s \<inter> {tr'. matching_tr_pfx iosr tr' ctr} \<times> UNIV) R s0) \<Longrightarrow> triv_refinement aprog (rely (\<lambda>s. aprog s \<inter> {tr'. matching_tr_pfx iosr tr' ctr} \<times> UNIV) R s0) proof (prove)
goal:
No subgoals!
theory Prefix_Refinement

lemma is_matching_fragment_no_trace:
  "is_matching_fragment sr osr rvr [] cres s0 R s (\<lambda>s. {([], ares s)})
    = rel_tmres osr rvr (ares s) cres" by (simp add: is_matching_fragment_def prefix_closed_def
                self_closed_def env_closed_def
                matching_tr_pfx_def matching_tr_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_matching_fragment sr osr rvr [] cres s0 R s (\<lambda>s. {([], ares s)}) = rel_tmres osr rvr (ares s) cres
theory Prefix_Refinement

lemma prefix_refinement_return_imp:
  "(\<forall>s s0 t0 t. P s0 s \<and> Q t0 t \<and> isr s t \<longrightarrow> rvr rv rv' \<and> osr s t)
    \<Longrightarrow> prefix_refinement sr isr osr rvr P Q AR R (return rv) (return rv')" apply (clarsimp simp: prefix_refinement_def) apply (rule default_prefix_refinement_ex) apply (auto simp add: return_def is_matching_fragment_no_trace) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s s0 t0 t. P s0 s \<and> Q t0 t \<and> isr s t \<longrightarrow> rvr rv rv' \<and> osr s t \<Longrightarrow> prefix_refinement sr isr osr rvr P Q AR R (return rv) (return rv') proof (prove)
goal (1 subgoal):
 1. \<And>s s0 t0 t a b. \<lbrakk>\<forall>s s0 t0 t. P s0 s \<and> Q t0 t \<and> isr s t \<longrightarrow> rvr rv rv' \<and> osr s t; isr s t; P s0 s; sr s0 t0; Q t0 t; (a, b) \<in> return rv' t; rely_cond R t0 a\<rbrakk> \<Longrightarrow> \<exists>f. is_matching_fragment sr osr rvr a b s0 AR s f \<and> triv_refinement (return rv) f proof (prove)
goal (1 subgoal):
 1. \<And>s s0 t0 t a b. \<lbrakk>\<forall>s s0 t0 t. P s0 s \<and> Q t0 t \<and> isr s t \<longrightarrow> rvr rv rv' \<and> osr s t; isr s t; P s0 s; sr s0 t0; Q t0 t; (a, b) \<in> return rv' t; rely_cond R t0 a\<rbrakk> \<Longrightarrow> is_matching_fragment sr osr rvr a b s0 AR s (\<lambda>s. return rv s \<inter> {tr'. length tr' \<le> length a} \<times> UNIV) proof (prove)
goal:
No subgoals!
theory Prefix_Refinement

lemma prefix_refinement_get:
  "prefix_refinement sr iosr iosr iosr dc2 dc2 AR R get get" apply (clarsimp simp: prefix_refinement_def get_def) apply (rule default_prefix_refinement_ex) apply (simp add: is_matching_fragment_no_trace) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. prefix_refinement sr iosr iosr iosr (\<lambda>_ _. True) (\<lambda>_ _. True) AR R get get proof (prove)
goal (1 subgoal):
 1. \<And>s s0 t0 t. \<lbrakk>iosr s t; sr s0 t0\<rbrakk> \<Longrightarrow> \<exists>f. is_matching_fragment sr iosr iosr [] (Result (t, t)) s0 AR s f \<and> triv_refinement (\<lambda>s. {([], Result (s, s))}) f proof (prove)
goal (1 subgoal):
 1. \<And>s s0 t0 t. \<lbrakk>iosr s t; sr s0 t0\<rbrakk> \<Longrightarrow> is_matching_fragment sr iosr iosr [] (Result (t, t)) s0 AR s (\<lambda>s. {([], Result (s, s))} \<inter> {tr'. length tr' \<le> length []} \<times> UNIV) proof (prove)
goal:
No subgoals!
theory Prefix_Refinement

lemma prefix_refinement_put:
  "osr s t \<Longrightarrow> prefix_refinement sr isr osr dc2 dc2 dc2 AR R (put s) (put t)" apply (clarsimp simp: prefix_refinement_def put_def) apply (rule default_prefix_refinement_ex) apply (simp add: is_matching_fragment_no_trace) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. osr s t \<Longrightarrow> prefix_refinement sr isr osr (\<lambda>_ _. True) (\<lambda>_ _. True) (\<lambda>_ _. True) AR R (put s) (put t) proof (prove)
goal (1 subgoal):
 1. \<And>sa x s0 xa. \<lbrakk>osr s t; isr sa x; sr s0 xa\<rbrakk> \<Longrightarrow> \<exists>f. is_matching_fragment sr osr (\<lambda>_ _. True) [] (Result ((), t)) s0 AR sa f \<and> triv_refinement (\<lambda>_. {([], Result ((), s))}) f proof (prove)
goal (1 subgoal):
 1. \<And>sa x s0 xa. \<lbrakk>osr s t; isr sa x; sr s0 xa\<rbrakk> \<Longrightarrow> is_matching_fragment sr osr (\<lambda>_ _. True) [] (Result ((), t)) s0 AR sa (\<lambda>sa. {([], Result ((), s))} \<inter> {tr'. length tr' \<le> length []} \<times> UNIV) proof (prove)
goal:
No subgoals!
theory Prefix_Refinement

lemma prefix_refinement_select:
  "(\<forall>x \<in> T. \<exists>y \<in> S. rvr y x)
    \<Longrightarrow> prefix_refinement sr iosr iosr rvr dc2 dc2 AR R (select S) (select T)" apply (clarsimp simp: prefix_refinement_def select_def) apply (drule(1) bspec, clarsimp) apply (rule_tac x="return y" in exI) apply (simp add: is_matching_fragment_def self_closed_def env_closed_def return_def
                   prefix_closed_def matching_tr_pfx_def matching_tr_def) apply (auto simp add: triv_refinement_def return_def image_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>T. \<exists>y\<in>S. rvr y x \<Longrightarrow> prefix_refinement sr iosr iosr rvr (\<lambda>_ _. True) (\<lambda>_ _. True) AR R (select S) (select T) proof (prove)
goal (1 subgoal):
 1. \<And>s s0 t0 t x. \<lbrakk>\<forall>x\<in>T. \<exists>y\<in>S. rvr y x; iosr s t; sr s0 t0; x \<in> T\<rbrakk> \<Longrightarrow> \<exists>f. is_matching_fragment sr iosr rvr [] (Result (x, t)) s0 AR s f \<and> triv_refinement (\<lambda>s. Pair [] ` Result ` (S \<times> {s})) f proof (prove)
goal (1 subgoal):
 1. \<And>s s0 t0 t x y. \<lbrakk>iosr s t; sr s0 t0; x \<in> T; y \<in> S; rvr y x\<rbrakk> \<Longrightarrow> \<exists>f. is_matching_fragment sr iosr rvr [] (Result (x, t)) s0 AR s f \<and> triv_refinement (\<lambda>s. Pair [] ` Result ` (S \<times> {s})) f proof (prove)
goal (1 subgoal):
 1. \<And>s s0 t0 t x y. \<lbrakk>iosr s t; sr s0 t0; x \<in> T; y \<in> S; rvr y x\<rbrakk> \<Longrightarrow> is_matching_fragment sr iosr rvr [] (Result (x, t)) s0 AR s (return y) \<and> triv_refinement (\<lambda>s. Pair [] ` Result ` (S \<times> {s})) (return y) proof (prove)
goal (1 subgoal):
 1. \<And>s s0 t0 t x y. \<lbrakk>iosr s t; sr s0 t0; x \<in> T; y \<in> S; rvr y x\<rbrakk> \<Longrightarrow> triv_refinement (\<lambda>s. Pair [] ` Result ` (S \<times> {s})) (\<lambda>s. {([], Result (y, s))}) proof (prove)
goal:
No subgoals!
theory Prefix_Refinement

lemma Int_insert_left2:
  "(insert a B \<inter> C) = ((if a \<in> C then {a} else {}) \<union> (B \<inter> C))" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. insert a B \<inter> C = (if a \<in> C then {a} else {}) \<union> B \<inter> C
theory Prefix_Refinement

lemma abs_rely_stableT:
  "abs_rely_stable AR \<top>" by (simp add: abs_rely_stable_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. abs_rely_stable AR (\<lambda>_. True)