kings-crown/FVELER_Isabelle huggingface dataset:
theory Trace_More_RG

lemma rg_conj_lift_inv:
  "\<lbrakk>\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>; \<lbrace>\<lambda>s0 s. P' s0 s \<and> I s0 s\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv. I\<rbrace>;
    \<And>s0 s. P s0 s \<Longrightarrow> P' s0 s\<rbrakk>
   \<Longrightarrow> \<lbrace>\<lambda>s0 s. P s0 s \<and> I s0 s\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. Q rv s0 s \<and> I s0 s\<rbrace>" by (fastforce 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>\<lambda>s0 s. P' s0 s \<and> I s0 s\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>rv. I\<rbrace>; \<And>s0 s. P s0 s \<Longrightarrow> P' s0 s\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s0 s. P s0 s \<and> I s0 s\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>rv s0 s. Q rv s0 s \<and> I s0 s\<rbrace>
theory Trace_More_RG

lemma rg_in_rely_post:
  assumes x: "\<And>P. \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f -,\<lbrace>\<lambda>x. P\<rbrace>"
  shows      "\<lbrace>\<top>\<top>\<rbrace>,\<lbrace>R\<rbrace> f -,\<lbrace>\<lambda>rv s0 s. (rv, s) \<in> mres (rely f R s0 s)\<rbrace>" apply (clarsimp simp: validI_def validI_prefix_closed[OF x]) apply (rule back_subst[where P="\<lambda>s0. x\<in>mres (rely f R s0 s)" for x s]) apply (rule back_subst[where P="\<lambda>s. x\<in>mres (rely f R s0 s)" for x s0]) apply (drule in_mres, assumption) apply (simp add: state_unchanged_rg[OF x]) apply (simp add: last_state_unchanged_rg[OF x]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>R\<rbrace> f -, \<lbrace>\<lambda>rv s0 s. (rv, s) \<in> mres (rely f R s0 s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s0 s tr rv s'. (tr, Result (rv, s')) \<in> rely f R s0 s \<Longrightarrow> (rv, s') \<in> mres (rely f R (last_st_tr tr s0) s') proof (prove)
goal (2 subgoals):
 1. \<And>s0 s tr rv s'. (tr, Result (rv, s')) \<in> rely f R s0 s \<Longrightarrow> (rv, s') \<in> mres (rely f R (?a12 s0 s tr rv s') s')
 2. \<And>s0 s tr rv s'. (tr, Result (rv, s')) \<in> rely f R s0 s \<Longrightarrow> ?a12 s0 s tr rv s' = last_st_tr tr s0 proof (prove)
goal (3 subgoals):
 1. \<And>s0 s tr rv s'. (tr, Result (rv, s')) \<in> rely f R s0 s \<Longrightarrow> (rv, s') \<in> mres (rely f R (?a12 s0 s tr rv s') (?a18 s0 s tr rv s'))
 2. \<And>s0 s tr rv s'. (tr, Result (rv, s')) \<in> rely f R s0 s \<Longrightarrow> ?a18 s0 s tr rv s' = s'
 3. \<And>s0 s tr rv s'. (tr, Result (rv, s')) \<in> rely f R s0 s \<Longrightarrow> ?a12 s0 s tr rv s' = last_st_tr tr s0 proof (prove)
goal (2 subgoals):
 1. \<And>s0 s tr rv s'. (tr, Result (rv, s')) \<in> rely f R s0 s \<Longrightarrow> s = s'
 2. \<And>s0 s tr rv s'. (tr, Result (rv, s')) \<in> rely f R s0 s \<Longrightarrow> s0 = last_st_tr tr s0 proof (prove)
goal (1 subgoal):
 1. \<And>s0 s tr rv s'. (tr, Result (rv, s')) \<in> rely f R s0 s \<Longrightarrow> s0 = last_st_tr tr s0 proof (prove)
goal:
No subgoals!
theory Trace_More_RG

lemma list_case_throw_validIE_R:
  "\<lbrakk> \<And>y ys. xs = y # ys \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f y ys \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,- \<rbrakk> \<Longrightarrow>
   \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> case xs of [] \<Rightarrow> throwError e | x # xs \<Rightarrow> f x xs \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,-" apply (cases xs, simp_all) apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>y ys. xs = y # ys \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f y ys \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>, -) \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> case xs of [] \<Rightarrow> throwError e | x # xs \<Rightarrow> f x xs \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. xs = [] \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> throwError e \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>, - proof (prove)
goal:
No subgoals!
theory Trace_More_RG

lemma validI_set_take_helper:
  "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. \<forall>x \<in> set (xs rv s0 s). Q x rv s0 s\<rbrace>
   \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. \<forall>x \<in> set (take (n rv s0 s) (xs rv s0 s)). Q x rv s0 s\<rbrace>" apply (erule rg_strengthen_post) apply (clarsimp dest!: in_set_takeD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>rv s0 s. \<forall>x\<in>set (xs rv s0 s). Q x rv s0 s\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>rv s0 s. \<forall>x\<in>set (take (n rv s0 s) (xs rv s0 s)). Q x rv s0 s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>v s0 s. \<forall>x\<in>set (xs v s0 s). Q x v s0 s \<Longrightarrow> \<forall>x\<in>set (take (n v s0 s) (xs v s0 s)). Q x v s0 s proof (prove)
goal:
No subgoals!
theory Trace_More_RG

lemma whenE_throwError_tsp:
  "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> whenE Q (throwError e) \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. \<not> Q \<and> P s0 s\<rbrace>, -" apply (simp add: whenE_def) apply (intro conjI impI; wp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> whenE Q (throwError e) \<lbrace>G\<rbrace>, \<lbrace>\<lambda>rv s0 s. \<not> Q \<and> P s0 s\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. (Q \<longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> throwError e \<lbrace>G\<rbrace>, \<lbrace>\<lambda>rv s0 s. False\<rbrace>, -) \<and> (\<not> Q \<longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> returnOk () \<lbrace>G\<rbrace>, \<lbrace>\<lambda>rv. P\<rbrace>, -) proof (prove)
goal:
No subgoals!
theory Trace_More_RG

lemma weaker_rg_ifE:
  assumes x: "\<lbrace>P \<rbrace>,\<lbrace>R\<rbrace> a \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
  assumes y: "\<lbrace>P'\<rbrace>,\<lbrace>R\<rbrace> b \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
  shows      "\<lbrace>P and P'\<rbrace>,\<lbrace>R\<rbrace> if test then a else b \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" apply (rule rg_weaken_preE) apply (wp x y) apply simp done

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

lemma twp_split_const_if:
  assumes x: "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>"
  assumes y: "\<lbrace>P'\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q'\<rbrace>"
  shows "\<lbrace>\<lambda>s0 s. (S \<longrightarrow> P s0 s) \<and> (\<not> S \<longrightarrow> P' s0 s)\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. (S \<longrightarrow> Q rv s0 s) \<and> (\<not> S \<longrightarrow> Q' rv s0 s)\<rbrace>" by (cases S, simp_all add: x y)

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

lemma twp_split_const_ifE_R:
  assumes x: "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
  assumes y: "\<lbrace>P'\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q'\<rbrace>,\<lbrace>E\<rbrace>"
  shows "\<lbrace>\<lambda>s0 s. (S \<longrightarrow> P s0 s) \<and> (\<not> S \<longrightarrow> P' s0 s)\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. (S \<longrightarrow> Q rv s0 s) \<and> (\<not> S \<longrightarrow> Q' rv s0 s)\<rbrace>,\<lbrace>E\<rbrace>" by (cases S, simp_all add: x y)

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

lemma rg_disj_division:
  "\<lbrakk> P \<or> Q; P \<Longrightarrow> \<lbrace>R\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>S\<rbrace>; Q \<Longrightarrow> \<lbrace>T\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>S\<rbrace> \<rbrakk>
   \<Longrightarrow> \<lbrace>\<lambda>s0 s. (P \<longrightarrow> R s0 s) \<and> (Q \<longrightarrow> T s0 s)\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>S\<rbrace>" by (fastforce intro: rg_weaken_pre)

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

lemma rg_grab_asm:
  "\<lbrakk> P' \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>; \<not> P' \<Longrightarrow> prefix_closed f \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s0 s. P' \<and> P s0 s\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>" by (cases P'; simp)

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

lemma rg_grab_asm2:
  "\<lbrakk>P' \<Longrightarrow> \<lbrace>\<lambda>s0 s. P s0 s \<and> P'' s0 s\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>; \<not> P' \<Longrightarrow> prefix_closed f\<rbrakk>
   \<Longrightarrow> \<lbrace>\<lambda>s0 s. P s0 s \<and> P' \<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. \<lbrakk>P' \<Longrightarrow> \<lbrace>\<lambda>s0 s. P s0 s \<and> P'' s0 s\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>; \<not> P' \<Longrightarrow> prefix_closed f\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s0 s. P s0 s \<and> P' \<and> P'' s0 s\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>
theory Trace_More_RG

lemma rg_grab_exs:
  assumes x: "\<And>x. P x \<Longrightarrow> \<lbrace>P'\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>"
  assumes y: "prefix_closed f"
  shows      "\<lbrace>\<lambda>s0 s. \<exists>x. P x \<and> P' s0 s\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>" apply (clarsimp simp: validI_def y use_validI_guar[OF _ x]) apply (erule(2) use_validI [OF _ x]) done

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

lemma rg_prop_E:
  "prefix_closed f \<Longrightarrow> \<lbrace>\<lambda>s0 s. P\<rbrace>,\<lbrace>R\<rbrace> f -,-,\<lbrace>\<lambda>rv s0 s. P\<rbrace>" by wpsimp

(* 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_walk_assmsE:
  assumes x: "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv. P\<rbrace>" and y: "\<And>s0 s. P s0 s \<Longrightarrow> Q s0 s" and z: "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> g \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv. Q\<rbrace>"
  shows      "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> doE x \<leftarrow> f; g odE \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv. Q\<rbrace>" apply (wp z) apply (simp add: validIE_def) apply (rule rg_strengthen_post [OF x]) apply (auto simp: y split: sum.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> doE x <- f;
g
odE \<lbrace>G\<rbrace>, \<lbrace>\<lambda>rv. Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>x s0 s. P s0 s \<and> P s0 s\<rbrace>, \<lbrace>\<lambda>rv. Q\<rbrace>
 2. \<And>s0 s. P s0 s \<Longrightarrow> ?P' s0 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>v s0 s. case v of Inl e \<Rightarrow> Q s0 s | Inr r \<Rightarrow> P s0 s\<rbrace>
 2. \<And>s0 s. P s0 s \<Longrightarrow> ?P' s0 s proof (prove)
goal (2 subgoals):
 1. \<And>v s0 s. P s0 s \<Longrightarrow> case v of Inl e \<Rightarrow> Q s0 s | Inr r \<Rightarrow> P s0 s
 2. \<And>s0 s. P s0 s \<Longrightarrow> P s0 s proof (prove)
goal:
No subgoals!
theory Trace_More_RG

lemma weak_if_twp:
  "\<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>Q'\<rbrace> \<rbrakk> \<Longrightarrow>
   \<lbrace>P and P'\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>r. if C r then Q r else Q' r\<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>Q'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P and P'\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>r. if C r then Q r else Q' r\<rbrace>
theory Trace_More_RG

lemma weak_if_twp':
  "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>r. Q r and Q' r\<rbrace> \<Longrightarrow>
   \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>r. if C r then Q r else Q' r\<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>r. Q r and Q' r\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>r. if C r then Q r else Q' r\<rbrace>
theory Trace_More_RG

lemma validE_R_abstract_rv:
  "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. \<forall>rv'. Q rv' s0 s\<rbrace>,\<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" by (erule rg_strengthen_postE; simp)

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

lemma validIE_cases_validI:
  "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. Q (Inr rv) s0 s\<rbrace>,\<lbrace>\<lambda>rv s0 s. Q (Inl rv) s0 s\<rbrace>
   \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>" apply (simp add: validIE_def) apply (erule rg_strengthen_post) apply (simp split: sum.split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>rv. Q (Inr rv)\<rbrace>, \<lbrace>\<lambda>rv. Q (Inl rv)\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>v s0 s. case v of Inl e \<Rightarrow> Q (Inl e) s0 s | Inr r \<Rightarrow> Q (Inr r) s0 s\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>v s0 s. case v of Inl e \<Rightarrow> Q (Inl e) s0 s | Inr r \<Rightarrow> Q (Inr r) s0 s \<Longrightarrow> Q v s0 s proof (prove)
goal:
No subgoals!
theory Trace_More_RG

lemma liftM_pre_rg:
  assumes rl: "\<lbrace>\<lambda>s0 s. \<not> P s0 s \<rbrace>,\<lbrace>R\<rbrace> a \<lbrace>G\<rbrace>,\<lbrace> \<lambda>_ _ _. False \<rbrace>"
  shows "\<lbrace>\<lambda>s0 s. \<not> P s0 s \<rbrace>,\<lbrace>R\<rbrace> liftM f a \<lbrace>G\<rbrace>,\<lbrace> \<lambda>_ _ _. False \<rbrace>" unfolding liftM_def apply (rule bind_twp_fwd) apply (rule rl) apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s0 s. \<not> P s0 s\<rbrace>, \<lbrace>R\<rbrace> liftM f a \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_ _ _. False\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s0 s. \<not> P s0 s\<rbrace>, \<lbrace>R\<rbrace> do x <- a;
return (f x)
od \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_ _ _. False\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>s0 s. \<not> P s0 s\<rbrace>, \<lbrace>R\<rbrace> a \<lbrace>G\<rbrace>, \<lbrace>?Q'\<rbrace>
 2. \<And>r. \<lbrace>?Q' r\<rbrace>, \<lbrace>R\<rbrace> return (f r) \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_ _ _. False\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>r. \<lbrace>\<lambda>_ _. False\<rbrace>, \<lbrace>R\<rbrace> return (f r) \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_ _ _. False\<rbrace> proof (prove)
goal:
No subgoals!
theory Trace_More_RG

lemma rg_add_K:
  "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s0 s. P s0 s \<and> I\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. Q rv s0 s \<and> I\<rbrace>" by (fastforce 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>\<lambda>s0 s. P s0 s \<and> I\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>rv s0 s. Q rv s0 s \<and> I\<rbrace>
theory Trace_More_RG

lemma valid_rv_lift:
  "\<lbrace>P'\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. rv \<longrightarrow> Q rv s0 s\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s0 s. P \<and> P' s0 s\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. rv \<longrightarrow> P \<and> Q rv s0 s\<rbrace>" by (fastforce 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. rv \<longrightarrow> Q rv s0 s\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s0 s. P \<and> P' s0 s\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>rv s0 s. rv \<longrightarrow> P \<and> Q rv s0 s\<rbrace>
theory Trace_More_RG

lemma valid_rv_split:
  "\<lbrakk>\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. rv \<longrightarrow> Q s0 s\<rbrace>; \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. \<not>rv \<longrightarrow> Q' s0 s\<rbrace>\<rbrakk>
   \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. if rv then Q s0 s else Q' s0 s\<rbrace>" by (fastforce simp: validI_def)

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

lemma rg_rv_split:
  "\<lbrakk>\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. rv \<longrightarrow> (Q rv s0 s)\<rbrace>; \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. (\<not>rv) \<longrightarrow> (Q rv s0 s)\<rbrace>\<rbrakk>
   \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>" apply (clarsimp simp: validI_def) by (metis (full_types))

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>rv s0 s. rv \<longrightarrow> Q rv s0 s\<rbrace>; \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>rv s0 s. \<not> rv \<longrightarrow> Q rv s0 s\<rbrace>\<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 rv s'. \<lbrakk>\<forall>s0 s tr res. P s0 s \<and> (tr, res) \<in> rely f R s0 s \<longrightarrow> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> \<not> rv \<longrightarrow> Q False (last_st_tr tr s0) s'); prefix_closed f; \<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> rv \<longrightarrow> Q True (last_st_tr tr s0) s'); P s0 s; (tr, Result (rv, s')) \<in> rely f R s0 s\<rbrakk> \<Longrightarrow> Q rv (last_st_tr tr s0) s'
theory Trace_More_RG

lemma combine_validE:
  "\<lbrakk> \<lbrace> P \<rbrace>,\<lbrace>R\<rbrace> x \<lbrace>G\<rbrace>,\<lbrace> Q \<rbrace>,\<lbrace> E \<rbrace>; \<lbrace> P' \<rbrace>,\<lbrace>R\<rbrace> x \<lbrace>G\<rbrace>,\<lbrace> Q' \<rbrace>,\<lbrace> E' \<rbrace> \<rbrakk>
   \<Longrightarrow> \<lbrace> P and P' \<rbrace>,\<lbrace>R\<rbrace> x \<lbrace>G\<rbrace>,\<lbrace> \<lambda>r. Q r and Q' r \<rbrace>,\<lbrace>\<lambda>r. E r and E' r \<rbrace>" apply (clarsimp simp: validIE_def validI_def split: sum.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> x \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>; \<lbrace>P'\<rbrace>, \<lbrace>R\<rbrace> x \<lbrace>G\<rbrace>, \<lbrace>Q'\<rbrace>, \<lbrace>E'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P and P'\<rbrace>, \<lbrace>R\<rbrace> x \<lbrace>G\<rbrace>, \<lbrace>\<lambda>r. Q r and Q' r\<rbrace>, \<lbrace>\<lambda>r. E r and E' r\<rbrace> proof (prove)
goal:
No subgoals!
theory Trace_More_RG

lemma validI_case_prod:
  "\<lbrakk> \<And>x y. validI (P x y) R (f x y) G Q \<rbrakk> \<Longrightarrow> validI (case_prod P v) R (case_prod (\<lambda>x y. f x y) v) G Q" by (simp add: split_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x y. \<lbrace>P x y\<rbrace>, \<lbrace>R\<rbrace> f x y \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>) \<Longrightarrow> \<lbrace>case v of (x, xa) \<Rightarrow> P x xa\<rbrace>, \<lbrace>R\<rbrace> case v of (x, y) \<Rightarrow> f x y \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>