kings-crown/FVELER_Isabelle huggingface dataset:
theory Prefix_Refinement

lemma rely_stable_rtranclp:
  "rely_stable R sr Q
    \<Longrightarrow> sr s t \<Longrightarrow> Q t
    \<Longrightarrow> rtranclp R t t'
    \<Longrightarrow> Q t'" apply (rotate_tac 3, induct arbitrary: s rule: converse_rtranclp_induct) apply simp apply (clarsimp simp: rely_stable_def) apply metis done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rely_stable R sr Q; sr s t; Q t; R\<^sup>*\<^sup>* t t'\<rbrakk> \<Longrightarrow> Q t' proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>rely_stable R sr Q; sr s t'; Q t'\<rbrakk> \<Longrightarrow> Q t'
 2. \<And>y z s. \<lbrakk>R y z; R\<^sup>*\<^sup>* z t'; \<And>s. \<lbrakk>rely_stable R sr Q; sr s z; Q z\<rbrakk> \<Longrightarrow> Q t'; rely_stable R sr Q; sr s y; Q y\<rbrakk> \<Longrightarrow> Q t' proof (prove)
goal (1 subgoal):
 1. \<And>y z s. \<lbrakk>R y z; R\<^sup>*\<^sup>* z t'; \<And>s. \<lbrakk>rely_stable R sr Q; sr s z; Q z\<rbrakk> \<Longrightarrow> Q t'; rely_stable R sr Q; sr s y; Q y\<rbrakk> \<Longrightarrow> Q t' proof (prove)
goal (1 subgoal):
 1. \<And>y z s. \<lbrakk>R y z; R\<^sup>*\<^sup>* z t'; \<And>s. sr s z \<Longrightarrow> Q t'; \<forall>s t t'. Q t \<and> sr s t \<and> R t t' \<longrightarrow> Q t' \<and> (\<exists>s'. sr s' t'); sr s y; Q y\<rbrakk> \<Longrightarrow> Q t' proof (prove)
goal:
No subgoals!
theory Prefix_Refinement

lemma abs_rely_stable_rtranclp:
  "abs_rely_stable R P
    \<Longrightarrow> P s \<Longrightarrow> rtranclp R s s'
    \<Longrightarrow> P s'" apply (rotate_tac 2, induct rule: converse_rtranclp_induct) apply simp apply (clarsimp simp: abs_rely_stable_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>abs_rely_stable R P; P s; R\<^sup>*\<^sup>* s s'\<rbrakk> \<Longrightarrow> P s' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>abs_rely_stable R P; P s'\<rbrakk> \<Longrightarrow> P s'
 2. \<And>y z. \<lbrakk>R y z; R\<^sup>*\<^sup>* z s'; \<lbrakk>abs_rely_stable R P; P z\<rbrakk> \<Longrightarrow> P s'; abs_rely_stable R P; P y\<rbrakk> \<Longrightarrow> P s' proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>R y z; R\<^sup>*\<^sup>* z s'; \<lbrakk>abs_rely_stable R P; P z\<rbrakk> \<Longrightarrow> P s'; abs_rely_stable R P; P y\<rbrakk> \<Longrightarrow> P s' proof (prove)
goal:
No subgoals!
theory Prefix_Refinement

lemma mapM_x_Cons:
  "mapM_x f (x # xs) = do f x; mapM_x f xs od" by (simp add: mapM_x_def sequence_x_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mapM_x f (x # xs) = do f x;
mapM_x f xs
od
theory Prefix_Refinement

lemma prefix_refinement_assume_pre:
  "(P \<Longrightarrow> prefix_refinement sr isr osr rvr P' Q' AR R f g)
    \<Longrightarrow> prefix_refinement sr isr osr rvr (P' and (\<lambda>_ _. P)) Q' AR R f g"
  "(P \<Longrightarrow> prefix_refinement sr isr osr rvr P' Q' AR R f g)
    \<Longrightarrow> prefix_refinement sr isr osr rvr P' (Q' and (\<lambda>_ _. P)) AR R f g" by (auto simp: prefix_refinement_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((P \<Longrightarrow> prefix_refinement sr isr osr rvr P' Q' AR R f g) \<Longrightarrow> prefix_refinement sr isr osr rvr (P' and (\<lambda>_ _. P)) Q' AR R f g) &&& ((P \<Longrightarrow> prefix_refinement sr isr osr rvr P' Q' AR R f g) \<Longrightarrow> prefix_refinement sr isr osr rvr P' (Q' and (\<lambda>_ _. P)) AR R f g)
theory Prefix_Refinement

lemma prefix_refinement_gets:
  "\<forall>s t. iosr s t \<and> P s \<and> Q t \<longrightarrow> rvr (f s) (f' t)
    \<Longrightarrow> prefix_refinement sr iosr iosr rvr (\<lambda>_. P) (\<lambda>_. Q) AR R (gets f) (gets f')" apply (simp add: gets_def) apply (rule prefix_refinement_get_pre) apply (rule prefix_refinement_return_imp) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s t. iosr s t \<and> P s \<and> Q t \<longrightarrow> rvr (f s) (f' t) \<Longrightarrow> prefix_refinement sr iosr iosr rvr (\<lambda>_. P) (\<lambda>_. Q) AR R (gets f) (gets f') proof (prove)
goal (1 subgoal):
 1. \<forall>s t. iosr s t \<and> P s \<and> Q t \<longrightarrow> rvr (f s) (f' t) \<Longrightarrow> prefix_refinement sr iosr iosr rvr (\<lambda>_. P) (\<lambda>_. Q) AR R (do s <- get;
return (f s)
od) (do s <- get;
return (f' s)
od) proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>\<forall>s t. iosr s t \<and> P s \<and> Q t \<longrightarrow> rvr (f s) (f' t); iosr x y\<rbrakk> \<Longrightarrow> prefix_refinement sr iosr iosr rvr (\<lambda>s0 s. s = x \<and> P s) (\<lambda>s0 s. s = y \<and> Q s) AR R (return (f x)) (return (f' y)) proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>\<forall>s t. iosr s t \<and> P s \<and> Q t \<longrightarrow> rvr (f s) (f' t); iosr x y\<rbrakk> \<Longrightarrow> \<forall>s s0 t0 t. (s = x \<and> P s) \<and> (t = y \<and> Q t) \<and> iosr s t \<longrightarrow> rvr (f x) (f' y) \<and> iosr s t proof (prove)
goal:
No subgoals!
theory Prefix_Refinement

lemma prefix_refinement_fail:
  "prefix_refinement sr isr osr rvr \<top>\<top> \<top>\<top> AR R fail fail" apply (clarsimp simp: prefix_refinement_def fail_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 isr osr rvr (\<lambda>_ _. True) (\<lambda>_ _. True) AR R fail fail proof (prove)
goal (1 subgoal):
 1. \<And>s x s0 xa. \<lbrakk>isr s x; sr s0 xa\<rbrakk> \<Longrightarrow> \<exists>f. is_matching_fragment sr osr rvr [] Failed s0 AR s f \<and> triv_refinement (\<lambda>s. {([], Failed)}) f proof (prove)
goal (1 subgoal):
 1. \<And>s x s0 xa. \<lbrakk>isr s x; sr s0 xa\<rbrakk> \<Longrightarrow> is_matching_fragment sr osr rvr [] Failed s0 AR s (\<lambda>s. {([], Failed)} \<inter> {tr'. length tr' \<le> length []} \<times> UNIV) proof (prove)
goal:
No subgoals!
theory Prefix_Refinement

lemma prefix_refinement_assert:
  "P = P' \<Longrightarrow> prefix_refinement sr iosr iosr \<top>\<top> \<top>\<top> \<top>\<top> AR R (assert P) (assert P')" by (simp add: assert_def prefix_refinement_fail prefix_refinement_return_imp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P = P' \<Longrightarrow> prefix_refinement sr iosr iosr (\<lambda>_ _. True) (\<lambda>_ _. True) (\<lambda>_ _. True) AR R (assert P) (assert P')
theory Prefix_Refinement

lemma par_tr_fin_bind:
  "(\<forall>x. par_tr_fin_principle (g x)) \<Longrightarrow> par_tr_fin_principle (f >>= g)" apply (clarsimp simp: par_tr_fin_principle_def bind_def) apply (clarsimp split: tmres.split_asm) apply (fastforce simp: last_st_tr_def hd_append) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>x. par_tr_fin_principle (g x) \<Longrightarrow> par_tr_fin_principle (f >>= g) proof (prove)
goal (1 subgoal):
 1. \<And>s tr s' a b. \<lbrakk>\<forall>x s tr s'. (tr, Result ((), s')) \<in> g x s \<longrightarrow> s' = last_st_tr tr s \<and> tr \<noteq> []; (a, b) \<in> f s; (tr, Result ((), s')) \<in> (case b of Failed \<Rightarrow> {(a, Failed)} | Incomplete \<Rightarrow> {(a, Incomplete)} | Result (rv, s) \<Rightarrow> (\<lambda>(aa, y). (aa @ a, y)) ` g rv s)\<rbrakk> \<Longrightarrow> s' = last_st_tr tr s \<and> tr \<noteq> [] proof (prove)
goal (1 subgoal):
 1. \<And>s s' a aa ba ab. \<lbrakk>\<forall>x s tr s'. (tr, Result ((), s')) \<in> g x s \<longrightarrow> s' = last_st_tr tr s \<and> tr \<noteq> []; (a, Result (aa, ba)) \<in> f s; (ab, Result ((), s')) \<in> g aa ba\<rbrakk> \<Longrightarrow> s' = last_st_tr ab (last_st_tr a s) proof (prove)
goal:
No subgoals!
theory Prefix_Refinement

lemma par_tr_fin_commit_step:
  "par_tr_fin_principle commit_step" by (simp add: par_tr_fin_principle_def commit_step_def
                bind_def get_def return_def put_trace_elem_def
         split: tmres.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. par_tr_fin_principle commit_step
theory Prefix_Refinement

lemma par_tr_fin_interference:
  "par_tr_fin_principle interference" apply (simp add: interference_def env_steps_repeat repeat_def select_early) apply (rule par_tr_fin_bind[rule_format]) apply (rule par_tr_fin_add_env_n_steps) apply (rule par_tr_fin_commit_step) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. par_tr_fin_principle interference proof (prove)
goal (1 subgoal):
 1. par_tr_fin_principle (do n <- select UNIV;
y <- commit_step;
env_n_steps n
od) proof (prove)
goal (1 subgoal):
 1. \<And>x. par_tr_fin_principle (do y <- commit_step;
env_n_steps x
od) proof (prove)
goal (1 subgoal):
 1. \<And>x. par_tr_fin_principle commit_step proof (prove)
goal:
No subgoals!
theory Prefix_Refinement

lemma prefix_refinement_triv_refinement_abs:
  "triv_refinement f f'
    \<Longrightarrow> prefix_refinement sr isr osr rvr P Q AR R f' g
    \<Longrightarrow> prefix_refinement sr isr osr rvr P Q AR R f g" apply (clarsimp simp: prefix_refinement_def) apply (strengthen triv_refinement_trans[mk_strg I E]) apply fastforce done

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

lemma prefix_refinement_triv_refinement_conc:
  "prefix_refinement sr isr osr rvr P Q AR R f g'
    \<Longrightarrow> triv_refinement g' g
    \<Longrightarrow> prefix_refinement sr isr osr rvr P Q AR R f g" apply (clarsimp simp: prefix_refinement_def triv_refinement_def) apply blast done

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

lemma rely_cond_mono:
  "R \<le> R' \<Longrightarrow> rely_cond R \<le> rely_cond R'" by (simp add: le_fun_def rely_cond_def split_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. R \<le> R' \<Longrightarrow> rely_cond R \<le> rely_cond R'
theory Prefix_Refinement

lemma matching_tr_transp:
  "transp sr \<Longrightarrow> transp (matching_tr sr)" apply (simp add: matching_tr_def) apply (rule list.rel_transp) apply (rule transpI; clarsimp) apply (metis transp_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. transp sr \<Longrightarrow> transp (matching_tr sr) proof (prove)
goal (1 subgoal):
 1. transp sr \<Longrightarrow> transp (list_all2 (\<lambda>(aid, as) (cid, cs). aid = cid \<and> sr as cs)) proof (prove)
goal (1 subgoal):
 1. transp sr \<Longrightarrow> transp (\<lambda>(aid, as) (cid, cs). aid = cid \<and> sr as cs) proof (prove)
goal (1 subgoal):
 1. \<And>b ba bb. \<lbrakk>transp sr; sr b ba; sr ba bb\<rbrakk> \<Longrightarrow> sr b bb proof (prove)
goal:
No subgoals!
theory Prefix_Refinement

lemma matching_tr_symp:
  "symp sr \<Longrightarrow> symp (matching_tr sr)" apply (simp add: matching_tr_def rel_prod_conv[symmetric]) apply (intro list.rel_symp prod.rel_symp; simp?) apply (simp add: sympI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. symp sr \<Longrightarrow> symp (matching_tr sr) proof (prove)
goal (1 subgoal):
 1. symp sr \<Longrightarrow> symp (list_all2 (rel_prod (=) sr)) proof (prove)
goal (1 subgoal):
 1. symp sr \<Longrightarrow> symp (=) proof (prove)
goal:
No subgoals!
theory Prefix_Refinement

lemma list_all2_is_me:
  "list_all2 P tr tr'
    \<Longrightarrow> \<forall>x y. P x y \<longrightarrow> fst x = fst y
    \<Longrightarrow> (n < length tr \<and> fst (rev tr ! n) = Me)
        = (n < length tr' \<and> fst (rev tr' ! n) = Me)" apply (rule conj_cong, simp add: list_all2_lengthD) apply (frule list_all2_rev_nthD, simp add: list_all2_lengthD) apply (cases "rev tr ! n", cases "rev tr' ! n", auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>list_all2 P tr tr'; \<forall>x y. P x y \<longrightarrow> fst x = fst y\<rbrakk> \<Longrightarrow> (n < length tr \<and> fst (rev tr ! n) = Me) = (n < length tr' \<and> fst (rev tr' ! n) = Me) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>list_all2 P tr tr'; \<forall>x y. P x y \<longrightarrow> fst x = fst y; n < length tr'\<rbrakk> \<Longrightarrow> (fst (rev tr ! n) = Me) = (fst (rev tr' ! n) = Me) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>list_all2 P tr tr'; \<forall>x y. P x y \<longrightarrow> fst x = fst y; n < length tr'; P (rev tr ! n) (rev tr' ! n)\<rbrakk> \<Longrightarrow> (fst (rev tr ! n) = Me) = (fst (rev tr' ! n) = Me) proof (prove)
goal:
No subgoals!
theory Trace_Det

lemma det_set_iff:
  "det f \<Longrightarrow> (r \<in> mres (f s)) = (mres (f s) = {r})" unfolding det_def mres_def by (fastforce elim: allE[where x=s])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. det f \<Longrightarrow> (r \<in> mres (f s)) = (mres (f s) = {r}) proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<exists>r. f s = {([], Result r)} \<Longrightarrow> (r \<in> Result -` snd ` f s) = (Result -` snd ` f s = {r})
theory Trace_Det

lemma return_det[iff]:
  "det (return x)" by (simp add: det_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. det (return x)
theory Trace_Det

lemma put_det[iff]:
  "det (put s)" by (simp add: det_def put_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. det (put s)
theory Trace_Det

lemma get_det[iff]:
  "det get" by (simp add: det_def get_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. det get
theory Trace_Det

lemma det_gets[iff]:
  "det (gets f)" by (auto simp add: gets_def det_def get_def return_def bind_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. det (gets f)
theory Trace_Det

lemma det_UN:
  "det f \<Longrightarrow> (\<Union>x \<in> mres (f s). g x) = (g (THE x. x \<in> mres (f s)))" unfolding det_def mres_def apply simp apply (drule spec [of _ s]) apply (clarsimp simp: vimage_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. det f \<Longrightarrow> \<Union> (g ` mres (f s)) = g (THE x. x \<in> mres (f s)) proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<exists>r. f s = {([], Result r)} \<Longrightarrow> \<Union> (g ` Result -` snd ` f s) = g (THE x. x \<in> Result -` snd ` f s) proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<exists>a b. f s = {([], Result (a, b))} \<Longrightarrow> \<Union> (g ` Result -` snd ` f s) = g (THE x. Result x \<in> snd ` f s) proof (prove)
goal (1 subgoal):
 1. \<exists>a b. f s = {([], Result (a, b))} \<Longrightarrow> \<Union> (g ` Result -` snd ` f s) = g (THE x. Result x \<in> snd ` f s) proof (prove)
goal:
No subgoals!
theory Trace_Det

lemma bind_detI[simp, intro!]:
  "\<lbrakk> det f; \<forall>x. det (g x) \<rbrakk> \<Longrightarrow> det (f >>= g)" unfolding bind_def det_def apply (erule all_reg[rotated]) by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>det f; \<forall>x. det (g x)\<rbrakk> \<Longrightarrow> det (f >>= g) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s. \<exists>r. f s = {([], Result r)}; \<forall>x s. \<exists>r. g x s = {([], Result r)}\<rbrakk> \<Longrightarrow> \<forall>s. \<exists>r. (\<Union>(xs, y)\<in>f s. case_tmres {(xs, Failed)} {(xs, Incomplete)} (\<lambda>(rv, s). (\<lambda>(a, y). (a @ xs, y)) ` g rv s) y) = {([], Result r)} proof (prove)
goal (1 subgoal):
 1. \<forall>x s. \<exists>r. g x s = {([], Result r)} \<Longrightarrow> \<forall>x. (\<exists>r. f x = {([], Result r)}) \<longrightarrow> (\<exists>r. (\<Union>(xs, y)\<in>f x. case_tmres {(xs, Failed)} {(xs, Incomplete)} (\<lambda>(rv, s). (\<lambda>(a, y). (a @ xs, y)) ` g rv s) y) = {([], Result r)})
theory Trace_Det

lemma det_modify[iff]:
  "det (modify f)" by (simp add: modify_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. det (modify f)
theory Trace_Det

lemma the_run_stateI:
  "mres (M s) = {s'} \<Longrightarrow> the_run_state M s = s'" by (simp add: the_run_state_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mres (M s) = {s'} \<Longrightarrow> the_run_state M s = s'
theory Trace_Det

lemma the_run_state_det:
  "\<lbrakk> s' \<in> mres (M s); det M \<rbrakk> \<Longrightarrow> the_run_state M s = s'" by (simp add: the_run_stateI det_set_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s' \<in> mres (M s); det M\<rbrakk> \<Longrightarrow> the_run_state M s = s'
theory Atomicity_Lib

lemma pfx_refn_interferences:
  " env_stable AR R sr iosr (\<lambda>t. True)
    \<Longrightarrow> prefix_refinement sr iosr iosr (\<top>\<top>) (\<top>\<top>) (\<top>\<top>) AR R interferences interferences" apply (rule prefix_refinement_repeat) apply (erule prefix_refinement_interference) apply wp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. env_stable AR R sr iosr (\<lambda>t. True) \<Longrightarrow> prefix_refinement sr iosr iosr (\<lambda>_ _. True) (\<lambda>_ _. True) (\<lambda>_ _. True) AR R interferences interferences proof (prove)
goal (3 subgoals):
 1. env_stable AR R sr iosr (\<lambda>t. True) \<Longrightarrow> prefix_refinement sr iosr iosr (\<lambda>_ _. True) (\<lambda>_ _. True) (\<lambda>_ _. True) AR R interference interference
 2. env_stable AR R sr iosr (\<lambda>t. True) \<Longrightarrow> \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>AR\<rbrace> interference -, \<lbrace>\<lambda>_ _ _. True\<rbrace>
 3. env_stable AR R sr iosr (\<lambda>t. True) \<Longrightarrow> \<lbrace>\<lambda>t0 t. True \<and> (\<exists>s0 s. sr s0 t0 \<and> iosr s t)\<rbrace>, \<lbrace>R\<rbrace> interference -, \<lbrace>\<lambda>_ _ _. True\<rbrace> proof (prove)
goal (2 subgoals):
 1. env_stable AR R sr iosr (\<lambda>t. True) \<Longrightarrow> \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>AR\<rbrace> interference -, \<lbrace>\<lambda>_ _ _. True\<rbrace>
 2. env_stable AR R sr iosr (\<lambda>t. True) \<Longrightarrow> \<lbrace>\<lambda>t0 t. True \<and> (\<exists>s0 s. sr s0 t0 \<and> iosr s t)\<rbrace>, \<lbrace>R\<rbrace> interference -, \<lbrace>\<lambda>_ _ _. True\<rbrace> proof (prove)
goal:
No subgoals!
theory Atomicity_Lib

lemma repeat_n_validI:
  "\<lbrace>I\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>_. I\<rbrace>
    \<Longrightarrow> \<lbrace>I\<rbrace>,\<lbrace>R\<rbrace> repeat_n n f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>_. I\<rbrace>" apply (induct n) apply wpsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>I\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_. I\<rbrace> \<Longrightarrow> \<lbrace>I\<rbrace>, \<lbrace>R\<rbrace> repeat_n n f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_. I\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>I\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_. I\<rbrace> \<Longrightarrow> \<lbrace>I\<rbrace>, \<lbrace>R\<rbrace> repeat_n 0 f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_. I\<rbrace>
 2. \<And>n. \<lbrakk>\<lbrace>I\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_. I\<rbrace> \<Longrightarrow> \<lbrace>I\<rbrace>, \<lbrace>R\<rbrace> repeat_n n f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_. I\<rbrace>; \<lbrace>I\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_. I\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>I\<rbrace>, \<lbrace>R\<rbrace> repeat_n (Suc n) f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_. I\<rbrace> proof (prove)
goal:
No subgoals!
theory Atomicity_Lib

lemma repeat_validI:
  "\<lbrace>I\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>_. I\<rbrace>
    \<Longrightarrow> \<lbrace>I\<rbrace>,\<lbrace>R\<rbrace> repeat f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>_. I\<rbrace>" apply (simp add: repeat_def) apply (wpsimp wp: repeat_n_validI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>I\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_. I\<rbrace> \<Longrightarrow> \<lbrace>I\<rbrace>, \<lbrace>R\<rbrace> repeat f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_. I\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>I\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_. I\<rbrace> \<Longrightarrow> \<lbrace>I\<rbrace>, \<lbrace>R\<rbrace> do n <- select UNIV;
repeat_n n f
od \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_. I\<rbrace> proof (prove)
goal:
No subgoals!