kings-crown/FVELER_Isabelle huggingface dataset:
theory Triv_Refinement

lemma triv_refinement_mono_parallel':
  "triv_refinement a b \<Longrightarrow> triv_refinement (parallel c a) (parallel c b)" apply (simp add: triv_refinement_def parallel_def split_def) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. triv_refinement a b \<Longrightarrow> triv_refinement (parallel c a) (parallel c b) proof (prove)
goal (1 subgoal):
 1. \<forall>s. b s \<subseteq> a s \<Longrightarrow> \<forall>s. {p. \<exists>f_steps. length f_steps = length (fst p) \<and> (map (\<lambda>p. (if fst p then fst (snd p) else Env, snd (snd p))) (zip f_steps (fst p)), snd p) \<in> c s \<and> (map (\<lambda>p. (if fst p then Env else fst (snd p), snd (snd p))) (zip f_steps (fst p)), snd p) \<in> b s} \<subseteq> {p. \<exists>f_steps. length f_steps = length (fst p) \<and> (map (\<lambda>p. (if fst p then fst (snd p) else Env, snd (snd p))) (zip f_steps (fst p)), snd p) \<in> c s \<and> (map (\<lambda>p. (if fst p then Env else fst (snd p), snd (snd p))) (zip f_steps (fst p)), snd p) \<in> a s} proof (prove)
goal:
No subgoals!
theory Triv_Refinement

lemma triv_refinement_parallel:
  "triv_refinement a b
    \<Longrightarrow> triv_refinement c d
    \<Longrightarrow> triv_refinement (parallel a c) (parallel b d)" by (metis triv_refinement_mono_parallel triv_refinement_mono_parallel'
    triv_refinement_trans)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>triv_refinement a b; triv_refinement c d\<rbrakk> \<Longrightarrow> triv_refinement (parallel a c) (parallel b d)
theory Triv_Refinement

lemma select_subset:
  "(select S s \<subseteq> select S' s') = (S \<subseteq> S' \<and> (S \<noteq> {} \<longrightarrow> s = s'))" by (auto simp add: select_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (select S s \<subseteq> select S' s') = (S \<subseteq> S' \<and> (S \<noteq> {} \<longrightarrow> s = s'))
theory Triv_Refinement

lemma triv_refinement_select:
  "S' \<subseteq> S \<Longrightarrow> triv_refinement (select S) (select S')" by (simp add: triv_refinement_def select_subset)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. S' \<subseteq> S \<Longrightarrow> triv_refinement (select S) (select S')
theory Triv_Refinement

lemma triv_refinement_select_eq:
  "triv_refinement (select S) (select S') = (S' \<subseteq> S)" by (simp add: triv_refinement_def select_subset)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. triv_refinement (select S) (select S') = (S' \<subseteq> S)
theory Triv_Refinement

lemma triv_refinement_rely:
  "(\<And>s0 s. R' s0 s \<Longrightarrow> R s0 s) \<Longrightarrow>
   triv_refinement (rely f R s0) (rely f R' s0)" unfolding rely_def triv_refinement_def rely_cond_def by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s0 s. R' s0 s \<Longrightarrow> R s0 s) \<Longrightarrow> triv_refinement (rely f R s0) (rely f R' s0) proof (prove)
goal (1 subgoal):
 1. (\<And>s0 s. R' s0 s \<Longrightarrow> R s0 s) \<Longrightarrow> \<forall>s. f s \<inter> {tr. \<forall>(ident, s0, s)\<in>trace_steps (rev tr) s0. ident = Env \<longrightarrow> R' s0 s} \<times> UNIV \<subseteq> f s \<inter> {tr. \<forall>(ident, s0, s)\<in>trace_steps (rev tr) s0. ident = Env \<longrightarrow> R s0 s} \<times> UNIV
theory Triv_Refinement

lemma triv_refinement_rely2:
  "triv_refinement f g \<Longrightarrow>
   triv_refinement (rely f R s0) (rely g R s0)" unfolding rely_def triv_refinement_def rely_cond_def by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. triv_refinement f g \<Longrightarrow> triv_refinement (rely f R s0) (rely g R s0) proof (prove)
goal (1 subgoal):
 1. \<forall>s. g s \<subseteq> f s \<Longrightarrow> \<forall>s. g s \<inter> {tr. \<forall>(ident, s0, s)\<in>trace_steps (rev tr) s0. ident = Env \<longrightarrow> R s0 s} \<times> UNIV \<subseteq> f s \<inter> {tr. \<forall>(ident, s0, s)\<in>trace_steps (rev tr) s0. ident = Env \<longrightarrow> R s0 s} \<times> UNIV
theory Triv_Refinement

lemma rely_rely_triv_refinement:
 "(\<And>s0 s. R s0 s \<Longrightarrow> R' s0 s) \<Longrightarrow>
 triv_refinement (rely f R' s0) (rely (rely f R s0) R' s0)" by (clarsimp simp: triv_refinement_def rely_def parallel_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s0 s. R s0 s \<Longrightarrow> R' s0 s) \<Longrightarrow> triv_refinement (rely f R' s0) (rely (rely f R s0) R' s0)
theory Triv_Refinement

lemma validI_triv_refinement:
  "triv_refinement f g
    \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>
    \<Longrightarrow> prefix_closed g
    \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> g \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>" unfolding rely_def triv_refinement_def validI_def by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>triv_refinement f g; \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>; prefix_closed g\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> g \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s. g s \<subseteq> f s; prefix_closed f \<and> (\<forall>s0 s tr res. P s0 s \<and> (tr, res) \<in> f s \<inter> Collect (rely_cond R s0) \<times> UNIV \<longrightarrow> guar_cond G s0 tr \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> Q rv (last_st_tr tr s0) s')); prefix_closed g\<rbrakk> \<Longrightarrow> prefix_closed g \<and> (\<forall>s0 s tr res. P s0 s \<and> (tr, res) \<in> g s \<inter> Collect (rely_cond R s0) \<times> UNIV \<longrightarrow> guar_cond G s0 tr \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> Q rv (last_st_tr tr s0) s'))
theory Triv_Refinement

lemma valid_triv_refinement:
  "triv_refinement f g
    \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>
    \<Longrightarrow> \<lbrace>P\<rbrace> g \<lbrace>Q\<rbrace>" unfolding rely_def triv_refinement_def valid_def mres_def by (fastforce elim: image_eqI[rotated])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>triv_refinement f g; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> g \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s. g s \<subseteq> f s; \<forall>s. P s \<longrightarrow> (\<forall>(r, s')\<in>Result -` snd ` f s. Q r s')\<rbrakk> \<Longrightarrow> \<forall>s. P s \<longrightarrow> (\<forall>(r, s')\<in>Result -` snd ` g s. Q r s')
theory Triv_Refinement

lemma triv_refinement_refl:
  "triv_refinement f f" by (simp add: triv_refinement_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. triv_refinement f f
theory Triv_Refinement

lemma triv_refinement_select_concrete_All:
  "\<forall>x \<in> S. triv_refinement aprog (cprog x)
    \<Longrightarrow> triv_refinement aprog (select S >>= cprog)" by (auto simp add: triv_refinement_def bind_def select_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>S. triv_refinement aprog (cprog x) \<Longrightarrow> triv_refinement aprog (select S >>= cprog)
theory Prefix_Refinement

lemma env_closed_strengthen_cond:
  "env_closed P s f
    \<Longrightarrow> (\<forall>xs s. Q xs s \<longrightarrow> P xs s)
    \<Longrightarrow> env_closed Q s f" by (simp add: env_closed_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>env_closed P s f; \<forall>xs s. Q xs s \<longrightarrow> P xs s\<rbrakk> \<Longrightarrow> env_closed Q s f
theory Prefix_Refinement

lemma matching_tr_pfx_aCons:
  "matching_tr_pfx sr ((tmid, s) # atr) ctr
    = (\<exists>s'. length atr < length ctr \<and> rev ctr ! length atr = (tmid, s')
        \<and> sr s s' \<and> matching_tr_pfx sr atr ctr)" apply (simp add: matching_tr_pfx_def matching_tr_def Suc_le_eq
                   list_all2_conv_all_nth less_Suc_eq all_conj_distrib) apply (simp add: nth_append prod_eq_iff) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. matching_tr_pfx sr ((tmid, s) # atr) ctr = (\<exists>s'. length atr < length ctr \<and> rev ctr ! length atr = (tmid, s') \<and> sr s s' \<and> matching_tr_pfx sr atr ctr) proof (prove)
goal (1 subgoal):
 1. (length atr < length ctr \<and> Suc (length atr) = min (length ctr) (Suc (length atr)) \<and> (\<forall>i<length atr. (case (rev atr @ [(tmid, s)]) ! i of (aid, as) \<Rightarrow> \<lambda>(cid, cs). aid = cid \<and> sr as cs) (rev ctr ! i)) \<and> (case (rev atr @ [(tmid, s)]) ! length atr of (aid, as) \<Rightarrow> \<lambda>(cid, cs). aid = cid \<and> sr as cs) (rev ctr ! length atr)) = (length atr < length ctr \<and> (\<exists>s'. rev ctr ! length atr = (tmid, s') \<and> sr s s' \<and> length atr \<le> length ctr \<and> length atr = min (length ctr) (length atr) \<and> (\<forall>i<length atr. (case rev atr ! i of (aid, as) \<Rightarrow> \<lambda>(cid, cs). aid = cid \<and> sr as cs) (rev ctr ! i)))) proof (prove)
goal (1 subgoal):
 1. (length atr < length ctr \<and> Suc (length atr) = min (length ctr) (Suc (length atr)) \<and> (\<forall>i<length atr. (case rev atr ! i of (aid, as) \<Rightarrow> \<lambda>(cid, cs). aid = cid \<and> sr as cs) (rev ctr ! i)) \<and> (case rev ctr ! length atr of (cid, cs) \<Rightarrow> tmid = cid \<and> sr s cs)) = (length atr < length ctr \<and> fst (rev ctr ! length atr) = tmid \<and> sr s (snd (rev ctr ! length atr)) \<and> length atr \<le> length ctr \<and> length atr = min (length ctr) (length atr) \<and> (\<forall>i<length atr. (case rev atr ! i of (aid, as) \<Rightarrow> \<lambda>(cid, cs). aid = cid \<and> sr as cs) (rev ctr ! i))) proof (prove)
goal:
No subgoals!
theory Prefix_Refinement

lemma rely_cond_hd:
  "rely_cond R s0 xs \<Longrightarrow> xs \<noteq> []
    \<Longrightarrow> fst (hd xs) = Env \<longrightarrow> R (last_st_tr (tl xs) s0) (snd (hd xs))" by (clarsimp simp: rely_cond_def neq_Nil_conv trace_steps_append
              split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rely_cond R s0 xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> fst (hd xs) = Env \<longrightarrow> R (last_st_tr (tl xs) s0) (snd (hd xs))
theory Prefix_Refinement

lemma diff_Suc_eq_if:
  "(Suc n - m) = (if m \<le> n then Suc (n - m) else 0)" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Suc n - m = (if m \<le> n then Suc (n - m) else 0)
theory Prefix_Refinement

lemma rely_cond_nth:
  "rely_cond R s0 tr \<Longrightarrow> n < length tr
    \<Longrightarrow> fst (rev tr ! n) = Env \<longrightarrow> R ((if n = 0 then s0 else snd (rev tr ! (n - 1)))) (snd (rev tr ! n))" by (simp add: rely_cond_def trace_steps_rev_drop_nth[where n=0, simplified])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rely_cond R s0 tr; n < length tr\<rbrakk> \<Longrightarrow> fst (rev tr ! n) = Env \<longrightarrow> R (if n = 0 then s0 else snd (rev tr ! (n - 1))) (snd (rev tr ! n))
theory Prefix_Refinement

lemma is_matching_fragment_Nil:
  "is_matching_fragment sr osr rvr ctr cres s0 R s f
    \<Longrightarrow> [] \<in> fst ` f s" apply (clarsimp simp: is_matching_fragment_def) apply (clarsimp simp only: set_eq_iff empty_iff simp_thms not_all) apply (drule(1) prefix_closed_drop[where tr=tr and n="length tr" for tr]) apply (clarsimp simp add: in_fst_snd_image) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_matching_fragment sr osr rvr ctr cres s0 R s f \<Longrightarrow> [] \<in> fst ` f s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>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 R s0 ((Env, s) # xs)) s f; f s \<noteq> {}; \<forall>x\<in>f s. case x of (tr, res) \<Rightarrow> rely_cond R 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 rvr res cres)\<rbrakk> \<Longrightarrow> [] \<in> fst ` f s proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>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 R s0 ((Env, s) # xs)) s f; \<forall>(tr, res)\<in>f s. rely_cond R 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 rvr res cres); (a, b) \<in> f s\<rbrakk> \<Longrightarrow> [] \<in> fst ` f s proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>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 R s0 ((Env, s) # xs)) s f; \<forall>(tr, res)\<in>f s. rely_cond R 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 rvr res cres); \<exists>res'. (drop (length a) a, res') \<in> f s\<rbrakk> \<Longrightarrow> [] \<in> fst ` f s proof (prove)
goal:
No subgoals!
theory Prefix_Refinement

theorem prefix_refinement_rely_cond_trD:
  assumes preds: "prefix_refinement sr isr osr rvr P Q R' R aprog cprog"
    "isr s t" "P s0 s" "Q t0 t" "(ctr, cres) \<in> cprog t"
    "rely_cond R t0 ctr" "sr s0 t0"
  and sr: "(\<forall>s t t'. sr s t \<longrightarrow> R t t' \<longrightarrow> (\<exists>s'. sr s' t' \<and> R' s s'))"
  shows "\<exists>(atr, ares) \<in> aprog s. matching_tr sr atr ctr
                    \<and> rel_tmres osr rvr ares cres
                    \<and> rely_cond R' s0 atr" proof - obtain f where subs: "f s \<subseteq> aprog s"
      and match: "is_matching_fragment sr osr rvr ctr cres s0 R' s f" using prefix_refinementD[OF preds(1-3) _ preds(4-5)] preds(6-) by (auto simp add: triv_refinement_def) show ?thesis using matching_fragment_matching_tr[OF match _ _ sr] preds subs by blast qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<exists>(atr, ares)\<in>aprog s. matching_tr sr atr ctr \<and> rel_tmres osr rvr ares cres \<and> rely_cond R' s0 atr proof (state)
goal (1 subgoal):
 1. \<exists>(atr, ares)\<in>aprog s. matching_tr sr atr ctr \<and> rel_tmres osr rvr ares cres \<and> rely_cond R' s0 atr proof (prove)
goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f s \<subseteq> aprog s; is_matching_fragment sr osr rvr ctr cres s0 R' s f\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (prove)
using this:
sr s0 t0 \<Longrightarrow> case (ctr, cres) of (ctr, cres) \<Rightarrow> rely_cond R t0 ctr \<longrightarrow> (\<exists>f. is_matching_fragment sr osr rvr ctr cres s0 R' s f \<and> triv_refinement aprog f)
rely_cond R t0 ctr
sr s0 t0

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f s \<subseteq> aprog s; is_matching_fragment sr osr rvr ctr cres s0 R' s f\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
f s \<subseteq> aprog s
is_matching_fragment sr osr rvr ctr cres s0 R' s f

goal (1 subgoal):
 1. \<exists>(atr, ares)\<in>aprog s. matching_tr sr atr ctr \<and> rel_tmres osr rvr ares cres \<and> rely_cond R' s0 atr proof (prove)
goal (1 subgoal):
 1. \<exists>(atr, ares)\<in>aprog s. matching_tr sr atr ctr \<and> rel_tmres osr rvr ares cres \<and> rely_cond R' s0 atr proof (prove)
using this:
\<lbrakk>rely_cond R ?t0.0 ctr; sr s0 ?t0.0\<rbrakk> \<Longrightarrow> \<exists>(atr, ares)\<in>f s. matching_tr sr atr ctr \<and> rel_tmres osr rvr ares cres \<and> rely_cond R' s0 atr
prefix_refinement sr isr osr rvr P Q R' R aprog cprog
isr s t
P s0 s
Q t0 t
(ctr, cres) \<in> cprog t
rely_cond R t0 ctr
sr s0 t0
f s \<subseteq> aprog s

goal (1 subgoal):
 1. \<exists>(atr, ares)\<in>aprog s. matching_tr sr atr ctr \<and> rel_tmres osr rvr ares cres \<and> rely_cond R' s0 atr proof (state)
this:
\<exists>(atr, ares)\<in>aprog s. matching_tr sr atr ctr \<and> rel_tmres osr rvr ares cres \<and> rely_cond R' s0 atr

goal:
No subgoals!
theory Prefix_Refinement

lemma rely_cond_True:
  "rely_cond (\<lambda>_ _. True) = (\<lambda>_ _. True)" by (simp add: rely_cond_def fun_eq_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rely_cond (\<lambda>_ _. True) = (\<lambda>_ _. True)
theory Prefix_Refinement

lemma ball_set_zip_conv_nth:
  "(\<forall>x \<in> set (zip ys zs). P x)
    = (\<forall>n. n < length ys \<longrightarrow> n < length zs \<longrightarrow> P (ys ! n, zs ! n))" by (auto simp add: Ball_def in_set_zip)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<forall>x\<in>set (zip ys zs). P x) = (\<forall>n<length ys. n < length zs \<longrightarrow> P (ys ! n, zs ! n))
theory Prefix_Refinement

lemma tr_in_parallel:
  "(tr, res) \<in> parallel f g s
    \<Longrightarrow> \<exists>f_tr g_tr. (f_tr, res) \<in> f s \<and> (g_tr, res) \<in> g s
        \<and> (tr, res) \<in> parallel (K {(f_tr, res)}) (K {(g_tr, res)}) s" apply (clarsimp simp: parallel_def) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (tr, res) \<in> parallel f g s \<Longrightarrow> \<exists>f_tr g_tr. (f_tr, res) \<in> f s \<and> (g_tr, res) \<in> g s \<and> (tr, res) \<in> parallel (K {(f_tr, res)}) (K {(g_tr, res)}) s proof (prove)
goal (1 subgoal):
 1. \<And>f_steps. \<lbrakk>length f_steps = length tr; (map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps tr, res) \<in> f s; (map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps tr, res) \<in> g s\<rbrakk> \<Longrightarrow> \<exists>f_tr. (f_tr, res) \<in> f s \<and> (\<exists>g_tr. (g_tr, res) \<in> g s \<and> (\<exists>f_steps. length f_steps = length tr \<and> map2 (\<lambda>f_step (id, y). (if f_step then id else Env, y)) f_steps tr = f_tr \<and> map2 (\<lambda>f_step (id, y). (if f_step then Env else id, y)) f_steps tr = g_tr)) proof (prove)
goal:
No subgoals!
theory Prefix_Refinement

lemma matching_env_closedD:
  "(tr, res) \<in> f s
    \<Longrightarrow> is_matching_fragment sr osr rvr ctr cres s0 R s f
    \<Longrightarrow> length tr < length ctr
    \<Longrightarrow> fst (rev ctr ! length tr) = Env
    \<Longrightarrow> sr s' (snd (rev ctr ! length tr))
    \<Longrightarrow> R (last_st_tr tr s0) s'
    \<Longrightarrow> (Env, s') # tr \<in> fst ` f s" apply (frule(1) is_matching_fragment_trD, clarsimp) apply (erule(1) env_closedD[OF is_matching_fragment_env_closed]) apply (clarsimp simp: matching_tr_pfx_aCons rely_cond_Cons_eq prod_eq_iff) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(tr, res) \<in> f s; is_matching_fragment sr osr rvr ctr cres s0 R s f; length tr < length ctr; fst (rev ctr ! length tr) = Env; sr s' (snd (rev ctr ! length tr)); R (last_st_tr tr s0) s'\<rbrakk> \<Longrightarrow> (Env, s') # tr \<in> fst ` f s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(tr, Incomplete) \<in> f s; is_matching_fragment sr osr rvr ctr cres s0 R s f; length tr < length ctr; fst (rev ctr ! length tr) = Env; sr s' (snd (rev ctr ! length tr)); R (last_st_tr tr s0) s'; rely_cond R s0 tr; matching_tr_pfx sr tr ctr; res = Incomplete\<rbrakk> \<Longrightarrow> (Env, s') # tr \<in> fst ` f s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(tr, Incomplete) \<in> f s; length tr < length ctr; fst (rev ctr ! length tr) = Env; sr s' (snd (rev ctr ! length tr)); R (last_st_tr tr s0) s'; rely_cond R s0 tr; matching_tr_pfx sr tr ctr; res = Incomplete\<rbrakk> \<Longrightarrow> matching_tr_pfx sr ((Env, s') # tr) ctr \<and> rely_cond R s0 ((Env, s') # tr) proof (prove)
goal:
No subgoals!
theory Prefix_Refinement

lemma forward_enabled_reflp:
  "reflp P \<Longrightarrow> forward_enabled P" by (auto simp add: reflp_def forward_enabled_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reflp P \<Longrightarrow> forward_enabled P
theory Prefix_Refinement

lemma par_tr_fin_principle_triv_refinement:
  "par_tr_fin_principle aprog
    \<Longrightarrow> triv_refinement aprog cprog
    \<Longrightarrow> par_tr_fin_principle cprog" by (fastforce simp: par_tr_fin_principle_def triv_refinement_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>par_tr_fin_principle aprog; triv_refinement aprog cprog\<rbrakk> \<Longrightarrow> par_tr_fin_principle cprog
theory Prefix_Refinement

lemma matching_tr_pfx_parallel_zip:
  "matching_tr_pfx sr a_pfx a_tr
    \<Longrightarrow> matching_tr_pfx sr b_pfx b_tr
    \<Longrightarrow> length a_pfx = length b_pfx
    \<Longrightarrow> list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) a_tr b_tr
    \<Longrightarrow> matching_tr_pfx sr (map parallel_mrg (zip a_pfx b_pfx)) (map parallel_mrg (zip a_tr b_tr))" apply (clarsimp simp: matching_tr_pfx_def matching_tr_def list_all2_lengthD) apply (clarsimp simp: list_all2_conv_all_nth) apply (clarsimp simp: rev_map split_def zip_rev[symmetric]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>matching_tr_pfx sr a_pfx a_tr; matching_tr_pfx sr b_pfx b_tr; length a_pfx = length b_pfx; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) a_tr b_tr\<rbrakk> \<Longrightarrow> matching_tr_pfx sr (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) a_pfx b_pfx) (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) a_tr b_tr) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>list_all2 (\<lambda>(aid, as) (cid, cs). aid = cid \<and> sr as cs) (rev b_pfx) (take (length b_pfx) (rev b_tr)); length a_pfx = length b_pfx; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) a_tr b_tr; length b_pfx \<le> length b_tr; list_all2 (\<lambda>(aid, as) (cid, cs). aid = cid \<and> sr as cs) (rev a_pfx) (take (length b_pfx) (rev a_tr))\<rbrakk> \<Longrightarrow> list_all2 (\<lambda>(aid, as) (cid, cs). aid = cid \<and> sr as cs) (rev (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) a_pfx b_pfx)) (take (length b_pfx) (rev (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) a_tr b_tr))) proof (prove)
goal (1 subgoal):
 1. \<And>i aid as cid cs. \<lbrakk>\<forall>i<length b_pfx. (case rev b_pfx ! i of (aid, as) \<Rightarrow> \<lambda>(cid, cs). aid = cid \<and> sr as cs) (rev b_tr ! i); length a_pfx = length b_pfx; length b_pfx \<le> length b_tr; \<forall>i<length b_pfx. (case rev a_pfx ! i of (aid, as) \<Rightarrow> \<lambda>(cid, cs). aid = cid \<and> sr as cs) (rev a_tr ! i); length a_tr = length b_tr; \<forall>i<length b_tr. (fst (a_tr ! i) = Env \<or> fst (b_tr ! i) = Env) \<and> snd (a_tr ! i) = snd (b_tr ! i); i < length b_pfx; (aid, as) = rev (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) a_pfx b_pfx) ! i; rev (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) a_tr b_tr) ! i = (cid, cs)\<rbrakk> \<Longrightarrow> aid = cid \<and> sr as cs proof (prove)
goal:
No subgoals!
theory Prefix_Refinement

lemma drop_sub_Suc_is_Cons:
  "n = length xs \<Longrightarrow> m < length xs \<Longrightarrow> drop (n - Suc m) xs = (rev xs ! m) # drop (n - m) xs" apply (rule nth_equalityI; clarsimp) apply (clarsimp simp add: nth_Cons' rev_nth) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n = length xs; m < length xs\<rbrakk> \<Longrightarrow> drop (n - Suc m) xs = rev xs ! m # drop (n - m) xs proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>n = length xs; m < length xs; i < Suc m\<rbrakk> \<Longrightarrow> xs ! (length xs + i - Suc m) = (rev xs ! m # drop (length xs - m) xs) ! i proof (prove)
goal:
No subgoals!
theory Prefix_Refinement

lemma le_sub_eq_0:
  "((x :: nat) \<le> x - y) = (x = 0 \<or> y = 0)" by arith

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x \<le> x - y) = (x = 0 \<or> y = 0)