kings-crown/FVELER_Isabelle huggingface dataset:
theory Trace_RG

lemma rg_use_eq:
  assumes "\<And>P. \<lbrace>\<lambda>s0 s. P (f s)\<rbrace>,\<lbrace>R\<rbrace> m \<lbrace>G\<rbrace>,\<lbrace>\<lambda>_ s0 s. P (f s)\<rbrace>"
  assumes "\<And>f. \<lbrace>\<lambda>s0 s. P f s0 s\<rbrace>,\<lbrace>R\<rbrace> m \<lbrace>G\<rbrace>,\<lbrace>\<lambda>_ s0 s. Q f s0 s\<rbrace>"
  shows "\<lbrace>\<lambda>s0 s. P (f s) s0 s\<rbrace>,\<lbrace>R\<rbrace> m \<lbrace>G\<rbrace>,\<lbrace>\<lambda>_ s0 s. Q (f s) s0 s \<rbrace>" apply (rule rg_post_imp[where Q'="\<lambda>_ s0 s. \<exists>y. y = f s \<and> Q y s0 s"], simp) apply (wpsimp wp: rg_vcg_ex_lift assms) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s0 s. P (f s) s0 s\<rbrace>, \<lbrace>R\<rbrace> m \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_ s0 s. Q (f s) s0 s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s0 s. P (f s) s0 s\<rbrace>, \<lbrace>R\<rbrace> m \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_ s0 s. \<exists>y. y = f s \<and> Q y s0 s\<rbrace> proof (prove)
goal:
No subgoals!
theory Trace_RG

lemma rg_validE_pred_conj:
  "\<lbrakk> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>; \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q'\<rbrace>,\<lbrace>E\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q and Q'\<rbrace>,\<lbrace>E\<rbrace>" unfolding validI_def validIE_def by (simp split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q'\<rbrace>, \<lbrace>E\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q and Q'\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prefix_closed f \<and> (\<forall>s0 s tr res. P s0 s \<and> (tr, res) \<in> rely f R s0 s \<longrightarrow> guar_cond G s0 tr \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> (case rv of Inl e \<Rightarrow> E e (last_st_tr tr s0) s' | Inr r \<Rightarrow> Q r (last_st_tr tr s0) s'))); prefix_closed f \<and> (\<forall>s0 s tr res. P s0 s \<and> (tr, res) \<in> rely f R s0 s \<longrightarrow> guar_cond G s0 tr \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> (case rv of Inl e \<Rightarrow> E e (last_st_tr tr s0) s' | Inr r \<Rightarrow> Q' r (last_st_tr tr s0) s')))\<rbrakk> \<Longrightarrow> prefix_closed f \<and> (\<forall>s0 s tr res. P s0 s \<and> (tr, res) \<in> rely f R s0 s \<longrightarrow> guar_cond G s0 tr \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> (case rv of Inl e \<Rightarrow> E e (last_st_tr tr s0) s' | Inr r \<Rightarrow> (Q and Q') r (last_st_tr tr s0) s')))
theory Trace_RG

lemma rg_validE_conj:
  "\<lbrakk> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>; \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q'\<rbrace>,\<lbrace>E\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. Q rv s0 s \<and> Q' rv s0 s\<rbrace>,\<lbrace>E\<rbrace>" unfolding validI_def validIE_def by (simp split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q'\<rbrace>, \<lbrace>E\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>rv s0 s. Q rv s0 s \<and> Q' rv s0 s\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prefix_closed f \<and> (\<forall>s0 s tr res. P s0 s \<and> (tr, res) \<in> rely f R s0 s \<longrightarrow> guar_cond G s0 tr \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> (case rv of Inl e \<Rightarrow> E e (last_st_tr tr s0) s' | Inr r \<Rightarrow> Q r (last_st_tr tr s0) s'))); prefix_closed f \<and> (\<forall>s0 s tr res. P s0 s \<and> (tr, res) \<in> rely f R s0 s \<longrightarrow> guar_cond G s0 tr \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> (case rv of Inl e \<Rightarrow> E e (last_st_tr tr s0) s' | Inr r \<Rightarrow> Q' r (last_st_tr tr s0) s')))\<rbrakk> \<Longrightarrow> prefix_closed f \<and> (\<forall>s0 s tr res. P s0 s \<and> (tr, res) \<in> rely f R s0 s \<longrightarrow> guar_cond G s0 tr \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> (case rv of Inl e \<Rightarrow> E e (last_st_tr tr s0) s' | Inr r \<Rightarrow> Q r (last_st_tr tr s0) s' \<and> Q' r (last_st_tr tr s0) s')))
theory Trace_RG

lemma rg_drop_imp:
  "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. Q' rv s0 s \<longrightarrow> Q rv s0 s\<rbrace>" by (auto simp: validI_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>rv s0 s. Q' rv s0 s \<longrightarrow> Q rv s0 s\<rbrace>
theory Trace_RG

lemma rg_drop_impE:
  "\<lbrakk>\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>r. Q\<rbrace>, \<lbrace>E\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. Q' rv s0 s \<longrightarrow> Q s0 s\<rbrace>, \<lbrace>E\<rbrace>" by (simp add: validIE_weaken)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>r. Q\<rbrace>, \<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>rv s0 s. Q' rv s0 s \<longrightarrow> Q s0 s\<rbrace>, \<lbrace>E\<rbrace>
theory Trace_RG

lemma rg_drop_impE_E:
  "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>, \<lbrace>\<lambda>rv s0 s. E' rv s0 s \<longrightarrow> E rv s0 s\<rbrace>" by (auto simp: validIE_def validI_def split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>rv s0 s. E' rv s0 s \<longrightarrow> E rv s0 s\<rbrace>
theory Trace_RG

lemma rg_drop_imp_conj[wp_unsafe]:
  "\<lbrakk> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q'\<rbrace>; \<lbrace>P'\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. (Q rv s0 s \<longrightarrow> Q'' rv s0 s) \<and> Q''' rv s0 s\<rbrace> \<rbrakk> \<Longrightarrow>
   \<lbrace>P and P'\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. (Q rv s0 s \<longrightarrow> Q' rv s0 s \<and> Q'' rv s0 s) \<and> Q''' rv s0 s\<rbrace>" by (auto simp: validI_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q'\<rbrace>; \<lbrace>P'\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>rv s0 s. (Q rv s0 s \<longrightarrow> Q'' rv s0 s) \<and> Q''' rv s0 s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P and P'\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>rv s0 s. (Q rv s0 s \<longrightarrow> Q' rv s0 s \<and> Q'' rv s0 s) \<and> Q''' rv s0 s\<rbrace>
theory Trace_RG

lemma rg_vcg_set_pred_lift_mono:
  assumes f: "\<And>x. m \<lbrace>R\<rbrace>,-,\<lbrace> f x \<rbrace>"
  assumes mono: "\<And>A B. A \<subseteq> B \<Longrightarrow> P A \<Longrightarrow> P B"
  shows "m \<lbrace>R\<rbrace>,-,\<lbrace> \<lambda>s0 s. P {x. f x s0 s} \<rbrace>" by (fastforce simp: validI_def validI_prefix_closed[OF f] elim!: mono[rotated]
                dest: use_validI[OF _ f])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s0 s. P {x. f x s0 s}\<rbrace>, \<lbrace>R\<rbrace> m -, \<lbrace>\<lambda>_ s0 s. P {x. f x s0 s}\<rbrace>
theory Trace_RG

lemma rg_strengthen_pre_via_assert_forward:
  assumes pos: "\<lbrace> P \<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace> Q \<rbrace>"
  assumes rel: "\<And>s0 s. S s0 s \<longrightarrow> P s0 s \<or> N s0 s"
  assumes neg: "\<lbrace> N \<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace> \<bottom>\<bottom>\<bottom> \<rbrace>"
  shows "\<lbrace> S \<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace> Q \<rbrace>" apply (rule rg_weaken_pre) apply (rule rg_strengthen_post) apply (rule rg_vcg_disj_lift[OF pos neg]) by (auto simp: rel)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>S\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>
 2. \<And>s0 s. S s0 s \<Longrightarrow> ?P' s0 s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P'\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>?Q'3\<rbrace>
 2. \<And>v s0 s. ?Q'3 v s0 s \<Longrightarrow> Q v s0 s
 3. \<And>s0 s. S s0 s \<Longrightarrow> ?P' s0 s proof (prove)
goal (2 subgoals):
 1. \<And>v s0 s. Q v s0 s \<or> False \<Longrightarrow> Q v s0 s
 2. \<And>s0 s. S s0 s \<Longrightarrow> P s0 s \<or> N s0 s
theory Trace_RG

lemma rg_strengthen_pre_via_assert_backward:
  assumes neg: "\<lbrace> \<lambda>s0 s. \<not> E s0 s \<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace> \<bottom>\<bottom>\<bottom> \<rbrace>"
  assumes pos: "\<lbrace> P and E \<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace> Q \<rbrace>"
  shows "\<lbrace> P \<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace> Q \<rbrace>" by (rule rg_strengthen_pre_via_assert_forward[OF pos _ neg], simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>
theory Trace_RG

lemma get_tsp:
  "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> get \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. s = rv \<and> P s0 s\<rbrace>" by (simp add: get_def validI_def prefix_closed_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> get \<lbrace>G\<rbrace>, \<lbrace>\<lambda>rv s0 s. s = rv \<and> P s0 s\<rbrace>
theory Trace_RG

lemma put_tsp:
  "\<lbrace>\<top>\<top>\<rbrace>,\<lbrace>R\<rbrace> put a \<lbrace>G\<rbrace>,\<lbrace>\<lambda>_ s0 s. s = a\<rbrace>" by (simp add: put_def validI_def prefix_closed_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>R\<rbrace> put a \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_ s0 s. s = a\<rbrace>
theory Trace_RG

lemma return_tsp:
  "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> return a \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. rv = a \<and> P s0 s\<rbrace>" by (simp add:return_def validI_def prefix_closed_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> return a \<lbrace>G\<rbrace>, \<lbrace>\<lambda>rv s0 s. rv = a \<and> P s0 s\<rbrace>
theory Trace_RG

lemma rg_return_tsp: (* FIXME lib: eliminate *)
  "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> return x \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv. P and (\<lambda>_ _. rv = x)\<rbrace>" by (simp add: validI_def return_def prefix_closed_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> return x \<lbrace>G\<rbrace>, \<lbrace>\<lambda>rv. P and (\<lambda>_ _. rv = x)\<rbrace>
theory Trace_RG

lemma assert_tsp:
  "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> assert Q \<lbrace>G\<rbrace>,\<lbrace>\<lambda>_ s0 s. P s0 s \<and> Q\<rbrace>" by (simp add: assert_def fail_def return_def validI_def prefix_closed_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> assert Q \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_ s0 s. P s0 s \<and> Q\<rbrace>
theory Trace_RG

lemma rg_gets_tsp:
  "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> gets f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. rv = f s \<and> P s0 s\<rbrace>" by (simp add: validI_def simpler_gets_def prefix_closed_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> gets f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>rv s0 s. rv = f s \<and> P s0 s\<rbrace>
theory Trace_RG

lemma rg_returnOk_tsp:
  "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> returnOk x \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. rv = x \<and> P s0 s\<rbrace>, \<lbrace>Q\<rbrace>" by (simp add: validI_def validIE_def returnOk_def return_def prefix_closed_def)

\<comment> \<open>For forward reasoning in RG proofs, these lemmas allow us to step over the
    left-hand-side of monadic bind, while keeping the same precondition.\<close>

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> returnOk x \<lbrace>G\<rbrace>, \<lbrace>\<lambda>rv s0 s. rv = x \<and> P s0 s\<rbrace>, \<lbrace>Q\<rbrace>
theory Trace_RG

lemma mres_union:
  "mres (a \<union> b) = mres a \<union> mres b" by (simp add: mres_def image_Un)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mres (a \<union> b) = mres a \<union> mres b
theory Trace_RG

lemma mres_Failed_empty:
  "mres ((\<lambda>xs. (xs, Failed)) ` X ) = {}"
  "mres ((\<lambda>xs. (xs, Incomplete)) ` X ) = {}" by (auto simp add: mres_def image_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mres ((\<lambda>xs. (xs, Failed)) ` X) = {} &&& mres ((\<lambda>xs. (xs, Incomplete)) ` X) = {}
theory Trace_RG

lemma det_set_option_eq:
  "(\<Union>a\<in>m. set_option (snd a)) = {(r, s')} \<Longrightarrow>
       (ts, Some (rr, ss)) \<in> m \<Longrightarrow> rr = r \<and> ss = s'" by (metis UN_I option.set_intros prod.inject singleton_iff snd_conv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<Union>a\<in>m. set_option (snd a)) = {(r, s')}; (ts, Some (rr, ss)) \<in> m\<rbrakk> \<Longrightarrow> rr = r \<and> ss = s'
theory Trace_RG

lemma det_set_option_eq':
  "(\<Union>a\<in>m. set_option (snd a)) = {(r, s')} \<Longrightarrow>
       Some (r, s') \<in> snd ` m" using image_iff by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<Union>a\<in>m. set_option (snd a)) = {(r, s')} \<Longrightarrow> Some (r, s') \<in> snd ` m proof (prove)
using this:
(?z \<in> ?f ` ?A) = (\<exists>x\<in>?A. ?z = ?f x)

goal (1 subgoal):
 1. (\<Union>a\<in>m. set_option (snd a)) = {(r, s')} \<Longrightarrow> Some (r, s') \<in> snd ` m
theory Trace_RG

lemma validI_name_pre:
  "prefix_closed f \<Longrightarrow>
  (\<And>s0 s. P s0 s \<Longrightarrow> \<lbrace>\<lambda>s0' s'. s0' = s0 \<and> s' = s\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>)
    \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>" unfolding validI_def by metis

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prefix_closed f; \<And>s0 s. P s0 s \<Longrightarrow> \<lbrace>\<lambda>s0' s'. s0' = s0 \<and> s' = s\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prefix_closed f; \<And>s0 s. P s0 s \<Longrightarrow> prefix_closed f \<and> (\<forall>s0a sa tr res. (s0a = s0 \<and> sa = s) \<and> (tr, res) \<in> rely f R s0a sa \<longrightarrow> guar_cond G s0a tr \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> Q rv (last_st_tr tr s0a) s'))\<rbrakk> \<Longrightarrow> prefix_closed f \<and> (\<forall>s0 s tr res. P s0 s \<and> (tr, res) \<in> rely f R s0 s \<longrightarrow> guar_cond G s0 tr \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> Q rv (last_st_tr tr s0) s'))
theory Trace_RG

lemma validI_well_behaved':
  "\<lbrakk>prefix_closed f; \<lbrace>P\<rbrace>,\<lbrace>R'\<rbrace> f \<lbrace>G'\<rbrace>,\<lbrace>Q\<rbrace>; R \<le> R'; G' \<le> G\<rbrakk>
   \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>" apply (subst validI_def, clarsimp) apply (clarsimp simp add: rely_def) apply (drule (2)  validI_D) apply (fastforce simp: rely_cond_def guar_cond_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prefix_closed f; \<lbrace>P\<rbrace>, \<lbrace>R'\<rbrace> f \<lbrace>G'\<rbrace>, \<lbrace>Q\<rbrace>; R \<le> R'; G' \<le> G\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s0 s tr res. \<lbrakk>prefix_closed f; \<lbrace>P\<rbrace>, \<lbrace>R'\<rbrace> f \<lbrace>G'\<rbrace>, \<lbrace>Q\<rbrace>; R \<le> R'; G' \<le> G; P s0 s; (tr, res) \<in> rely f R s0 s\<rbrakk> \<Longrightarrow> guar_cond G s0 tr \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> Q rv (last_st_tr tr s0) s') proof (prove)
goal (1 subgoal):
 1. \<And>s0 s tr res. \<lbrakk>prefix_closed f; \<lbrace>P\<rbrace>, \<lbrace>R'\<rbrace> f \<lbrace>G'\<rbrace>, \<lbrace>Q\<rbrace>; R \<le> R'; G' \<le> G; P s0 s; (tr, res) \<in> f s; rely_cond R s0 tr\<rbrakk> \<Longrightarrow> guar_cond G s0 tr \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> Q rv (last_st_tr tr s0) s') proof (prove)
goal (2 subgoals):
 1. \<And>s0 s tr res. \<lbrakk>prefix_closed f; R \<le> R'; G' \<le> G; P s0 s; (tr, res) \<in> f s; rely_cond R s0 tr\<rbrakk> \<Longrightarrow> rely_cond R' s0 tr
 2. \<And>s0 s tr res. \<lbrakk>prefix_closed f; R \<le> R'; G' \<le> G; P s0 s; (tr, res) \<in> f s; rely_cond R s0 tr; guar_cond G' s0 tr \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> Q rv (last_st_tr tr s0) s')\<rbrakk> \<Longrightarrow> guar_cond G s0 tr \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> Q rv (last_st_tr tr s0) s') proof (prove)
goal:
No subgoals!
theory Trace_RG

lemma bind_promote_If2:
  "do x \<leftarrow> f; if P then g x else h x od
   = (if P then bind f g else bind f h)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do x <- f;
if P then g x else h x
od = (if P then f >>= g else f >>= h)
theory Trace_RG

lemma exec_put_trace[unfolded K_bind_def]:
  "(do put_trace xs; f od) s
   = (\<Union>n \<in> {n. 0 < n \<and> n \<le> length xs}. {(drop n xs, Incomplete)})
     \<union> ((\<lambda>(a, b). (a @ xs, b)) ` f s)" apply (simp add: put_trace_eq_drop bind_def) apply (safe; (clarsimp split: if_split_asm)?;
         fastforce intro: bexI[where x=0] rev_bexI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (do put_trace xs;
f
od) s = (\<Union>n\<in>{n. 0 < n \<and> n \<le> length xs}. {(drop n xs, Incomplete)}) \<union> (\<lambda>(a, b). (a @ xs, b)) ` f s proof (prove)
goal (1 subgoal):
 1. (\<Union>x\<le>length xs. case if x = 0 then Result ((), s) else Incomplete of Failed \<Rightarrow> {(drop x xs, Failed)} | Incomplete \<Rightarrow> {(drop x xs, Incomplete)} | Result (rv, s) \<Rightarrow> (\<lambda>(a, y). (a @ drop x xs, y)) ` f s) = (\<Union>n\<in>{n. 0 < n \<and> n \<le> length xs}. {(drop n xs, Incomplete)}) \<union> (\<lambda>x. case x of (a, b) \<Rightarrow> (a @ xs, b)) ` f s proof (prove)
goal:
No subgoals!
theory Trace_RG

lemma UN_If_distrib:
  "(\<Union>x \<in> S. if P x then A x else B x)
   = ((\<Union>x \<in> S \<inter> {x. P x}. A x) \<union> (\<Union>x \<in> S \<inter> {x. \<not> P x}. B x))" by (fastforce split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<Union>x\<in>S. if P x then A x else B x) = \<Union> (A ` (S \<inter> {x. P x})) \<union> \<Union> (B ` (S \<inter> {x. \<not> P x}))
theory Trace_RG

lemma eq_Me_neq_Env:
  "(x = Me) = (x \<noteq> Env)" by (cases x; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x = Me) = (x \<noteq> Env)
theory Trace_RG

lemma validI_guar_post_conj_lift:
  "\<lbrakk>\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G1\<rbrace>,\<lbrace>Q1\<rbrace>; \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G2\<rbrace>,\<lbrace>Q2\<rbrace>\<rbrakk>
   \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>\<lambda>s0 s. G1 s0 s \<and> G2 s0 s\<rbrace>,\<lbrace>\<lambda>rv s0 s. Q1 rv s0 s \<and> Q2 rv s0 s\<rbrace>" apply (frule validI_prefix_closed) apply (subst validI_def, clarsimp simp: rely_def) apply (drule(3) validI_D)+ apply (auto simp: guar_cond_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G1\<rbrace>, \<lbrace>Q1\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G2\<rbrace>, \<lbrace>Q2\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>\<lambda>s0 s. G1 s0 s \<and> G2 s0 s\<rbrace>, \<lbrace>\<lambda>rv s0 s. Q1 rv s0 s \<and> Q2 rv s0 s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G1\<rbrace>, \<lbrace>Q1\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G2\<rbrace>, \<lbrace>Q2\<rbrace>; prefix_closed f\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>\<lambda>s0 s. G1 s0 s \<and> G2 s0 s\<rbrace>, \<lbrace>\<lambda>rv s0 s. Q1 rv s0 s \<and> Q2 rv s0 s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s0 s tr res. \<lbrakk>\<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G1\<rbrace>, \<lbrace>Q1\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G2\<rbrace>, \<lbrace>Q2\<rbrace>; prefix_closed f; P s0 s; (tr, res) \<in> f s; rely_cond R s0 tr\<rbrakk> \<Longrightarrow> guar_cond (\<lambda>s0 s. G1 s0 s \<and> G2 s0 s) s0 tr \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> Q1 rv (last_st_tr tr s0) s' \<and> Q2 rv (last_st_tr tr s0) s') proof (prove)
goal (1 subgoal):
 1. \<And>s0 s tr res. \<lbrakk>prefix_closed f; P s0 s; (tr, res) \<in> f s; rely_cond R s0 tr; guar_cond G1 s0 tr \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> Q1 rv (last_st_tr tr s0) s'); guar_cond G2 s0 tr \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> Q2 rv (last_st_tr tr s0) s')\<rbrakk> \<Longrightarrow> guar_cond (\<lambda>s0 s. G1 s0 s \<and> G2 s0 s) s0 tr \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> Q1 rv (last_st_tr tr s0) s' \<and> Q2 rv (last_st_tr tr s0) s') proof (prove)
goal:
No subgoals!
theory Trace_RG

lemma validI_valid_wp:
  "\<lbrakk>\<lbrace>P\<rbrace>,\<lbrace>\<top>\<top>\<rbrace> f -,\<lbrace>\<lambda>rv _ s. Q rv s\<rbrace>\<rbrakk>
   \<Longrightarrow> \<lbrace>P s0\<rbrace> f \<lbrace>Q\<rbrace>" by (auto simp: rely_def validI_def valid_def mres_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> f -, \<lbrace>\<lambda>rv _. Q rv\<rbrace> \<Longrightarrow> \<lbrace>P s0\<rbrace> f \<lbrace>Q\<rbrace>
theory Trace_RG

lemma validI_triv_valid_eq:
  "prefix_closed f \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>\<top>\<top>\<rbrace> f -,\<lbrace>\<lambda>rv _ s. Q rv s\<rbrace> = (\<forall>s0. \<lbrace>\<lambda>s. P s0 s\<rbrace> f \<lbrace>Q\<rbrace>)" by (fastforce simp: rely_def validI_def valid_def mres_def image_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. prefix_closed f \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> f -, \<lbrace>\<lambda>rv _. Q rv\<rbrace> = (\<forall>s0. \<lbrace>P s0\<rbrace> f \<lbrace>Q\<rbrace>)