kings-crown/FVELER_Isabelle huggingface dataset:
theory Trace_More_RG

lemma list_cases_weak_twp:
  assumes "\<lbrace>P_A\<rbrace>,\<lbrace>R\<rbrace> a \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>"
  assumes "\<And>x xs. \<lbrace>P_B\<rbrace>,\<lbrace>R\<rbrace> b x xs \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>"
  shows
  "\<lbrace>P_A and P_B\<rbrace>,\<lbrace>R\<rbrace>
   case ts of
       [] \<Rightarrow> a
     | x#xs \<Rightarrow> b x xs
   \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>" apply (cases ts) apply (simp, rule rg_weaken_pre, rule assms, simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P_A and P_B\<rbrace>, \<lbrace>R\<rbrace> case ts of [] \<Rightarrow> a | x # xs \<Rightarrow> b x xs \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. ts = [] \<Longrightarrow> \<lbrace>P_A and P_B\<rbrace>, \<lbrace>R\<rbrace> case ts of [] \<Rightarrow> a | x # xs \<Rightarrow> b x xs \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>
 2. \<And>aa list. ts = aa # list \<Longrightarrow> \<lbrace>P_A and P_B\<rbrace>, \<lbrace>R\<rbrace> case ts of [] \<Rightarrow> a | x # xs \<Rightarrow> b x xs \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace> proof (prove)
goal:
No subgoals!
theory Trace_More_RG

lemma rg_vcg_if_lift2:
  "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. (Q rv s0 s \<longrightarrow> X rv s0 s) \<and> (\<not> Q rv s0 s \<longrightarrow> Y rv s0 s)\<rbrace> \<Longrightarrow>
   \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. if Q rv s0 s then X rv s0 s else Y rv s0 s\<rbrace>"

  "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. (Q' rv \<longrightarrow> X rv s0 s) \<and> (\<not> Q' rv \<longrightarrow> Y rv s0 s)\<rbrace> \<Longrightarrow>
   \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv. if Q' rv then X rv else Y rv\<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>\<lambda>rv s0 s. (Q rv s0 s \<longrightarrow> X rv s0 s) \<and> (\<not> Q rv s0 s \<longrightarrow> Y rv s0 s)\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>rv s0 s. if Q rv s0 s then X rv s0 s else Y rv s0 s\<rbrace>) &&& (\<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>rv s0 s. (Q' rv \<longrightarrow> X rv s0 s) \<and> (\<not> Q' rv \<longrightarrow> Y rv s0 s)\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>rv. if Q' rv then X rv else Y rv\<rbrace>)
theory Trace_More_RG

lemma rg_vcg_if_lift_ER: (* Required because of lack of rv in lifting rules *)
  "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. (Q rv s0 s \<longrightarrow> X rv s0 s) \<and> (\<not> Q rv s0 s \<longrightarrow> Y rv s0 s)\<rbrace>,\<lbrace>E\<rbrace> \<Longrightarrow>
   \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. if Q rv s0 s then X rv s0 s else Y rv s0 s\<rbrace>,\<lbrace>E\<rbrace>"

  "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. (Q' rv \<longrightarrow> X rv s0 s) \<and> (\<not> Q' rv \<longrightarrow> Y rv s0 s)\<rbrace>,\<lbrace>E\<rbrace> \<Longrightarrow>
   \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv. if Q' rv then X rv else Y rv\<rbrace>,\<lbrace>E\<rbrace>" by (auto simp: validI_def validIE_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>rv s0 s. (Q rv s0 s \<longrightarrow> X rv s0 s) \<and> (\<not> Q rv s0 s \<longrightarrow> Y rv s0 s)\<rbrace>, \<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>rv s0 s. if Q rv s0 s then X rv s0 s else Y rv s0 s\<rbrace>, \<lbrace>E\<rbrace>) &&& (\<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>rv s0 s. (Q' rv \<longrightarrow> X rv s0 s) \<and> (\<not> Q' rv \<longrightarrow> Y rv s0 s)\<rbrace>, \<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>rv. if Q' rv then X rv else Y rv\<rbrace>, \<lbrace>E\<rbrace>)
theory Trace_More_RG

lemma assertE_twp:
  "\<lbrace>\<lambda>s0 s. F \<longrightarrow> Q () s0 s\<rbrace>,\<lbrace>R\<rbrace> assertE F \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" apply (rule rg_pre) apply (unfold assertE_def) apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s0 s. F \<longrightarrow> Q () s0 s\<rbrace>, \<lbrace>R\<rbrace> assertE F \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace>, \<lbrace>R\<rbrace> assertE F \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>
 2. \<And>s0 s. F \<longrightarrow> Q () s0 s \<Longrightarrow> ?P' s0 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace>, \<lbrace>R\<rbrace> if F then returnOk () else fail \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>
 2. \<And>s0 s. F \<longrightarrow> Q () s0 s \<Longrightarrow> ?P' s0 s proof (prove)
goal (1 subgoal):
 1. \<And>s0 s. F \<longrightarrow> Q () s0 s \<Longrightarrow> (F \<longrightarrow> Q () s0 s) \<and> (\<not> F \<longrightarrow> True) proof (prove)
goal:
No subgoals!
theory Trace_More_RG

lemma rg_doesn't_grow_proof:
  assumes y: "\<And>s0 s. finite (S s0 s)"
  assumes x: "\<And>x. \<lbrace>\<lambda>s0 s. x \<notin> S s0 s \<and> P s0 s\<rbrace>,\<lbrace>R\<rbrace> f -,\<lbrace>\<lambda>rv s0 s. x \<notin> S s0 s\<rbrace>"
  shows      "\<lbrace>\<lambda>s0 s. card (S s0 s) < n \<and> P s0 s\<rbrace>,\<lbrace>R\<rbrace> f -,\<lbrace>\<lambda>rv s0 s. card (S s0 s) < n\<rbrace>" apply (clarsimp simp: validI_def validI_prefix_closed[OF x]) apply (erule le_less_trans[rotated]) apply (rule card_mono[OF y]) apply clarsimp apply (rule ccontr) apply (drule (2) use_validI[OF _ x, OF _ conjI]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s0 s. card (S s0 s) < n \<and> P s0 s\<rbrace>, \<lbrace>R\<rbrace> f -, \<lbrace>\<lambda>rv s0 s. card (S s0 s) < n\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s0 s tr rv s'. \<lbrakk>card (S s0 s) < n; P s0 s; (tr, Result (rv, s')) \<in> rely f R s0 s\<rbrakk> \<Longrightarrow> card (S (last_st_tr tr s0) s') < n proof (prove)
goal (1 subgoal):
 1. \<And>s0 s tr rv s'. \<lbrakk>P s0 s; (tr, Result (rv, s')) \<in> rely f R s0 s\<rbrakk> \<Longrightarrow> card (S (last_st_tr tr s0) s') \<le> card (S s0 s) proof (prove)
goal (1 subgoal):
 1. \<And>s0 s tr rv s'. \<lbrakk>P s0 s; (tr, Result (rv, s')) \<in> rely f R s0 s\<rbrakk> \<Longrightarrow> S (last_st_tr tr s0) s' \<subseteq> S s0 s proof (prove)
goal (1 subgoal):
 1. \<And>s0 s tr rv s' x. \<lbrakk>P s0 s; (tr, Result (rv, s')) \<in> rely f R s0 s; x \<in> S (last_st_tr tr s0) s'\<rbrakk> \<Longrightarrow> x \<in> S s0 s proof (prove)
goal (1 subgoal):
 1. \<And>s0 s tr rv s' x. \<lbrakk>P s0 s; (tr, Result (rv, s')) \<in> rely f R s0 s; x \<in> S (last_st_tr tr s0) s'; x \<notin> S s0 s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s0 s tr rv s' x. \<lbrakk>P s0 s; x \<in> S (last_st_tr tr s0) s'; x \<notin> S s0 s; x \<notin> S (last_st_tr tr s0) s'\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Trace_More_RG

lemma rg_vcg_propE_R:
  "prefix_closed f \<Longrightarrow> \<lbrace>\<lambda>s0 s. P\<rbrace>,\<lbrace>R\<rbrace> f -,\<lbrace>\<lambda>rv s0 s. P\<rbrace>,-" by (simp add: validIE_def validI_def split: sum.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. prefix_closed f \<Longrightarrow> \<lbrace>\<lambda>s0 s. P\<rbrace>, \<lbrace>R\<rbrace> f -, \<lbrace>\<lambda>rv s0 s. P\<rbrace>, -
theory Trace_More_RG

lemma rg_set_preserved_proof:
  assumes y: "\<And>x. \<lbrace>\<lambda>s0 s. Q s0 s \<and> x \<in> S s0 s\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. x \<in> S s0 s\<rbrace>"
  assumes x: "\<And>x. \<lbrace>\<lambda>s0 s. Q s0 s \<and> x \<notin> S s0 s\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. x \<notin> S s0 s\<rbrace>"
  shows      "\<lbrace>\<lambda>s0 s. Q s0 s \<and> P (S s0 s)\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. P (S s0 s)\<rbrace>" apply (clarsimp simp: validI_def) by (metis (mono_tags, lifting) equalityI validI_prefix_closed post_by_rg guar_by_rg subsetI x y)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s0 s. Q s0 s \<and> P (S s0 s)\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>rv s0 s. P (S s0 s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. prefix_closed f \<and> (\<forall>s0 s tr res. Q s0 s \<and> P (S 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> P (S (last_st_tr tr s0) s')))
theory Trace_More_RG

lemma rg_set_shrink_proof:
  assumes x: "\<And>x. \<lbrace>\<lambda>s0 s. x \<notin> S s0 s\<rbrace>,\<lbrace>R\<rbrace> f -,\<lbrace>\<lambda>rv s0 s. x \<notin> S s0 s\<rbrace>"
  shows
  "\<lbrace>\<lambda>s0 s. \<forall>S'. S' \<subseteq> S s0 s \<longrightarrow> P S'\<rbrace>,\<lbrace>R\<rbrace>
   f
   -,\<lbrace>\<lambda>rv s0 s. P (S s0 s)\<rbrace>" apply (clarsimp simp: validI_def validI_prefix_closed[OF x]) apply (drule spec, erule mp) apply (clarsimp simp: subset_iff) apply (rule ccontr) apply (drule(1) use_validI [OF _ x]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s0 s. \<forall>S'\<subseteq>S s0 s. P S'\<rbrace>, \<lbrace>R\<rbrace> f -, \<lbrace>\<lambda>rv s0 s. P (S s0 s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s0 s tr rv s'. \<lbrakk>\<forall>S'\<subseteq>S s0 s. P S'; (tr, Result (rv, s')) \<in> rely f R s0 s\<rbrakk> \<Longrightarrow> P (S (last_st_tr tr s0) s') proof (prove)
goal (1 subgoal):
 1. \<And>s0 s tr rv s'. (tr, Result (rv, s')) \<in> rely f R s0 s \<Longrightarrow> S (last_st_tr tr s0) s' \<subseteq> S s0 s proof (prove)
goal (1 subgoal):
 1. \<And>s0 s tr rv s' t. \<lbrakk>(tr, Result (rv, s')) \<in> rely f R s0 s; t \<in> S (last_st_tr tr s0) s'\<rbrakk> \<Longrightarrow> t \<in> S s0 s proof (prove)
goal (1 subgoal):
 1. \<And>s0 s tr rv s' t. \<lbrakk>(tr, Result (rv, s')) \<in> rely f R s0 s; t \<in> S (last_st_tr tr s0) s'; t \<notin> S s0 s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s0 s tr rv s' t. \<lbrakk>t \<in> S (last_st_tr tr s0) s'; t \<notin> S s0 s; t \<notin> S (last_st_tr tr s0) s'\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Trace_More_RG

lemma use_validIE_R':
  "\<lbrakk>(tr, Result (Inr r, s')) \<in> rely f R s0 s; \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>; P s0 s; s0' = last_st_tr tr s0\<rbrakk>
   \<Longrightarrow> Q r s0' s'" unfolding validIE_def by (frule(3) use_validI', simp)

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

lemma use_validIE_guar:
  "\<lbrakk>(tr, res) \<in> rely f R s0 s; \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>; P s0 s\<rbrakk>
   \<Longrightarrow> guar_cond G s0 tr" unfolding validIE_def by (frule(2) use_validI_guar, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(tr, res) \<in> rely f R s0 s; \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>; P s0 s\<rbrakk> \<Longrightarrow> guar_cond G s0 tr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(tr, res) \<in> rely f R s0 s; \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>v s0 s. case v of Inl e \<Rightarrow> E e s0 s | Inr r \<Rightarrow> Q r s0 s\<rbrace>; P s0 s\<rbrakk> \<Longrightarrow> guar_cond G s0 tr
theory Trace_More_RG

lemma validI_preservation_ex:
  assumes x: "\<And>x P. \<lbrace>\<lambda>s0 s. P (f s0 s x :: 'b)\<rbrace>,\<lbrace>R\<rbrace> m \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. P (f s0 s x)\<rbrace>"
  shows      "\<lbrace>\<lambda>s0 s. P (f s0 s :: 'a \<Rightarrow> 'b)\<rbrace>,\<lbrace>R\<rbrace> m \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. P (f s0 s)\<rbrace>" apply (clarsimp simp: validI_def validI_prefix_closed[OF x] guar_by_rg[OF x]) apply (erule subst[rotated, where P=P]) apply (rule ext) apply (erule use_validI [OF _ x]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s0 s. P (f s0 s)\<rbrace>, \<lbrace>R\<rbrace> m \<lbrace>G\<rbrace>, \<lbrace>\<lambda>rv s0 s. P (f s0 s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s0 s tr rv s'. \<lbrakk>P (f s0 s); (tr, Result (rv, s')) \<in> rely m R s0 s\<rbrakk> \<Longrightarrow> P (f (last_st_tr tr s0) s') proof (prove)
goal (1 subgoal):
 1. \<And>s0 s tr rv s'. (tr, Result (rv, s')) \<in> rely m R s0 s \<Longrightarrow> f s0 s = f (last_st_tr tr s0) s' proof (prove)
goal (1 subgoal):
 1. \<And>s0 s tr rv s' x. (tr, Result (rv, s')) \<in> rely m R s0 s \<Longrightarrow> f s0 s x = f (last_st_tr tr s0) s' x proof (prove)
goal (1 subgoal):
 1. \<And>s0 s tr rv s' x. f s0 s x = f s0 s x proof (prove)
goal:
No subgoals!
theory Trace_More_RG

lemma whenE_invI:
  assumes a: "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>_. P\<rbrace>"
  shows "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> whenE Q f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>_. P\<rbrace>" by (wpsimp wp: a)

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

lemma ifM_throwError_returnOkI:
  "\<lbrace>Q\<rbrace>,\<lbrace>R\<rbrace> test \<lbrace>G\<rbrace>,\<lbrace>\<lambda>c s0 s. \<not> c \<longrightarrow> P s0 s\<rbrace>
   \<Longrightarrow> \<lbrace>Q\<rbrace>,\<lbrace>R\<rbrace> ifM test (throwError e) (returnOk ()) \<lbrace>G\<rbrace>,\<lbrace>\<lambda>_. P\<rbrace>, -" unfolding ifM_def apply (fold liftE_bindE) apply wpsimp apply assumption apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> test \<lbrace>G\<rbrace>, \<lbrace>\<lambda>c s0 s. \<not> c \<longrightarrow> P s0 s\<rbrace> \<Longrightarrow> \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> ifM test (throwError e) (returnOk ()) \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> test \<lbrace>G\<rbrace>, \<lbrace>\<lambda>c s0 s. \<not> c \<longrightarrow> P s0 s\<rbrace> \<Longrightarrow> \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> do c <- test;
if c then throwError e else returnOk ()
od \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> test \<lbrace>G\<rbrace>, \<lbrace>\<lambda>c s0 s. \<not> c \<longrightarrow> P s0 s\<rbrace> \<Longrightarrow> \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> doE c <- liftE test;
if c then throwError e else returnOk ()
odE \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> test \<lbrace>G\<rbrace>, \<lbrace>\<lambda>c s0 s. \<not> c \<longrightarrow> P s0 s\<rbrace> \<Longrightarrow> \<lbrace>?P'1\<rbrace>, \<lbrace>R\<rbrace> test \<lbrace>G\<rbrace>, \<lbrace>\<lambda>c s0 s. \<not> c \<longrightarrow> P s0 s\<rbrace>
 2. \<And>s0 s. \<lbrakk>\<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> test \<lbrace>G\<rbrace>, \<lbrace>\<lambda>c s0 s. \<not> c \<longrightarrow> P s0 s\<rbrace>; Q s0 s\<rbrakk> \<Longrightarrow> ?P'1 s0 s proof (prove)
goal (1 subgoal):
 1. \<And>s0 s. \<lbrakk>\<lbrace>Q\<rbrace>, \<lbrace>R\<rbrace> test \<lbrace>G\<rbrace>, \<lbrace>\<lambda>c s0 s. \<not> c \<longrightarrow> P s0 s\<rbrace>; Q s0 s\<rbrakk> \<Longrightarrow> Q s0 s proof (prove)
goal:
No subgoals!
theory Trace_More_RG

lemma validI_I:
  assumes px: "prefix_closed S"
  assumes gc: "\<And>s0 s tr res. \<lbrakk> P s0 s; (tr, res) \<in> (rely S R s0 s)\<rbrakk> \<Longrightarrow> guar_cond G s0 tr"
  assumes rl: "\<And>s0 s tr r s'. \<lbrakk> P s0 s; (tr, Result (r, s')) \<in> (rely S R s0 s) \<rbrakk> \<Longrightarrow> Q r (last_st_tr tr s0) s'"
  shows "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> S \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>" unfolding validI_def using px gc rl by safe

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> S \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. prefix_closed S \<and> (\<forall>s0 s tr res. P s0 s \<and> (tr, res) \<in> rely S 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')) proof (prove)
using this:
prefix_closed S
\<lbrakk>P ?s0.0 ?s; (?tr, ?res) \<in> rely S R ?s0.0 ?s\<rbrakk> \<Longrightarrow> guar_cond G ?s0.0 ?tr
\<lbrakk>P ?s0.0 ?s; (?tr, Result (?r, ?s')) \<in> rely S R ?s0.0 ?s\<rbrakk> \<Longrightarrow> Q ?r (last_st_tr ?tr ?s0.0) ?s'

goal (1 subgoal):
 1. prefix_closed S \<and> (\<forall>s0 s tr res. P s0 s \<and> (tr, res) \<in> rely S 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_More_RG

lemma rg_eq_P:
  assumes "\<And>P. \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>_. P\<rbrace>"
  shows "\<lbrace>\<lambda>_. (=) s\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>_ _. (=) s\<rbrace>" by (rule assms)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. (=) s\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_ _. (=) s\<rbrace>
theory Trace_More_RG

lemma valid_case_option_post_twp:
  "\<lbrakk>\<And>x. \<lbrace>P x\<rbrace>,\<lbrace>R\<rbrace> f -,\<lbrace>\<lambda>rv. Q x\<rbrace>\<rbrakk> \<Longrightarrow>
   \<lbrace>\<lambda>s0 s. case ep of Some x \<Rightarrow> P x s0 s | _ \<Rightarrow> True\<rbrace>,\<lbrace>R\<rbrace>
   f
   -,\<lbrace>\<lambda>rv s0 s. case ep of Some x \<Rightarrow> Q x s0 s | _ \<Rightarrow> True\<rbrace>" by (cases ep; fastforce simp: rg_TrueI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. \<lbrace>P x\<rbrace>, \<lbrace>R\<rbrace> f -, \<lbrace>\<lambda>rv. Q x\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s0 s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> P x s0 s\<rbrace>, \<lbrace>R\<rbrace> f -, \<lbrace>\<lambda>rv s0 s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> Q x s0 s\<rbrace>
theory Trace_More_RG

lemma P_bool_lift:
  assumes t: "\<lbrace>Q\<rbrace>,\<lbrace>R\<rbrace> f -,\<lbrace>\<lambda>r. Q\<rbrace>"
  assumes f: "\<lbrace>\<lambda>s0 s. \<not>Q s0 s\<rbrace>,\<lbrace>R\<rbrace> f -,\<lbrace>\<lambda>r s0 s. \<not>Q s0 s\<rbrace>"
  shows "\<lbrace>\<lambda>s0 s. P (Q s0 s)\<rbrace>,\<lbrace>R\<rbrace> f -,\<lbrace>\<lambda>r s0 s. P (Q s0 s)\<rbrace>" apply (clarsimp simp: validI_def validI_prefix_closed[OF f]) apply (rule back_subst[where P=P], assumption) apply (rule iffI) apply (erule (1) use_validI [OF _ t]) apply (rule classical) apply (drule (1) use_validI [OF _ f]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s0 s. P (Q s0 s)\<rbrace>, \<lbrace>R\<rbrace> f -, \<lbrace>\<lambda>r s0 s. P (Q s0 s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s0 s tr rv s'. \<lbrakk>P (Q s0 s); (tr, Result (rv, s')) \<in> rely f R s0 s\<rbrakk> \<Longrightarrow> P (Q (last_st_tr tr s0) s') proof (prove)
goal (1 subgoal):
 1. \<And>s0 s tr rv s'. \<lbrakk>P (Q s0 s); (tr, Result (rv, s')) \<in> rely f R s0 s\<rbrakk> \<Longrightarrow> Q s0 s = Q (last_st_tr tr s0) s' proof (prove)
goal (2 subgoals):
 1. \<And>s0 s tr rv s'. \<lbrakk>P (Q s0 s); (tr, Result (rv, s')) \<in> rely f R s0 s; Q s0 s\<rbrakk> \<Longrightarrow> Q (last_st_tr tr s0) s'
 2. \<And>s0 s tr rv s'. \<lbrakk>P (Q s0 s); (tr, Result (rv, s')) \<in> rely f R s0 s; Q (last_st_tr tr s0) s'\<rbrakk> \<Longrightarrow> Q s0 s proof (prove)
goal (1 subgoal):
 1. \<And>s0 s tr rv s'. \<lbrakk>P (Q s0 s); (tr, Result (rv, s')) \<in> rely f R s0 s; Q (last_st_tr tr s0) s'\<rbrakk> \<Longrightarrow> Q s0 s proof (prove)
goal (1 subgoal):
 1. \<And>s0 s tr rv s'. \<lbrakk>P (Q s0 s); (tr, Result (rv, s')) \<in> rely f R s0 s; Q (last_st_tr tr s0) s'; \<not> Q s0 s\<rbrakk> \<Longrightarrow> Q s0 s proof (prove)
goal (1 subgoal):
 1. \<And>s0 s tr rv s'. \<lbrakk>P (Q s0 s); Q (last_st_tr tr s0) s'; \<not> Q s0 s; \<not> Q (last_st_tr tr s0) s'\<rbrakk> \<Longrightarrow> Q s0 s proof (prove)
goal:
No subgoals!
theory Trace_More_RG

lemma gets_sp: "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> gets f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv. P and (\<lambda>s0 s. f s = rv)\<rbrace>" by (wp, simp)

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

lemma post_by_rg2:
  "\<lbrakk>\<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>; (tr, Result (rv, s')) \<in> rely f R s0 s; P s0 s\<rbrakk>
  \<Longrightarrow> Q rv (last_st_tr tr s0) s'" by (rule post_by_rg, assumption+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>; (tr, Result (rv, s')) \<in> rely f R s0 s; P s0 s\<rbrakk> \<Longrightarrow> Q rv (last_st_tr tr s0) s'
theory Trace_More_RG

lemma rg_as_subst:
  "\<lbrakk> \<And>P. \<lbrace>\<lambda>s0 s. P (fn s0 s)\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. P (fn s0 s)\<rbrace>;
     \<And>v :: 'a. \<lbrace>P v\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q v\<rbrace> \<rbrakk> \<Longrightarrow>
   \<lbrace>\<lambda>s0 s. P (fn s0 s) s0 s\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. Q (fn s0 s) rv s0 s\<rbrace>" by (rule rg_lift_Pf3)

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

lemma rg_ex_pre_conj:
  "\<lbrakk>\<And>x. \<lbrace>\<lambda>s0 s. P x s0 s \<and> P' s0 s\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>\<rbrakk>
   \<Longrightarrow> \<lbrace>\<lambda>s0 s. (\<exists>x. P x s0 s) \<and> P' s0 s\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>" by (fastforce simp: validI_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. \<lbrace>\<lambda>s0 s. P x s0 s \<and> P' s0 s\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s0 s. (\<exists>x. P x s0 s) \<and> P' s0 s\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>