kings-crown/FVELER_Isabelle huggingface dataset:
theory Trace_RG

lemma rg_vcg_E_elim:
  "\<lbrakk>\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,-,\<lbrace>E\<rbrace>; \<lbrace>P'\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,-\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s0 s. P s0 s \<and> P' s0 s\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" by (rule rg_strengthen_postE[OF rg_vcg_conj_liftE2]) simp+

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

lemma rg_strengthen_post_R:
  "\<lbrakk> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q'\<rbrace>,-; \<And>rv s0 s. Q' rv s0 s \<Longrightarrow> Q rv s0 s \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,-" by (erule rg_post_impE)

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

lemma rg_post_comb_imp_conj:
  "\<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>; \<And>s0 s. P s0 s \<Longrightarrow> P' s0 s\<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>" by (wpsimp wp: rg_vcg_conj_lift)

(* 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>; \<And>s0 s. P s0 s \<Longrightarrow> P' s0 s\<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>
theory Trace_RG

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

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

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

lemma valid_validI_wp:
  "\<lbrakk>no_trace f; \<And>s0. \<lbrace>P s0\<rbrace> f \<lbrace>\<lambda>v. Q v s0 \<rbrace>\<rbrakk>
   \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>" by (clarsimp simp: validI_valid_no_trace_eq)

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

lemma validE_validIE_wp:
  "\<lbrakk>no_trace f; \<And>s0. \<lbrace>P s0\<rbrace> f \<lbrace>\<lambda>v. Q v s0 \<rbrace>,\<lbrace>\<lambda>v. E v s0\<rbrace>\<rbrakk>
   \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" by (clarsimp simp: validIE_validE_no_trace_eq)

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

lemma liftE_twp:
  "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> liftE f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" by simp

(* 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> liftE f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>
theory Trace_RG

lemma handleE_twp:
  assumes x: "\<And>x. \<lbrace>F x\<rbrace>,\<lbrace>R\<rbrace> handler x \<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>F\<rbrace>"
  shows      "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f <handle> handler \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" by (simp add: handleE_def handleE'_twp[OF x y])

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

lemma liftME_twp:
  "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> m \<lbrace>G\<rbrace>,\<lbrace>Q \<circ> f\<rbrace>,\<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> liftME f m \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" by (simp add: rg_liftME_subst)

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

lemma list_cases_twp:
  assumes a: "\<lbrace>P_A\<rbrace>,\<lbrace>R\<rbrace> a \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>"
  assumes b: "\<And>x xs. ts = x#xs \<Longrightarrow> \<lbrace>P_B x xs\<rbrace>,\<lbrace>R\<rbrace> b x xs \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>"
  shows "\<lbrace>case_list P_A P_B ts\<rbrace>,\<lbrace>R\<rbrace> case ts of [] \<Rightarrow> a | x # xs \<Rightarrow> b x xs \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>" by (cases ts, auto simp: a b)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>case ts of [] \<Rightarrow> P_A | x # xa \<Rightarrow> P_B x xa\<rbrace>, \<lbrace>R\<rbrace> case ts of [] \<Rightarrow> a | x # xs \<Rightarrow> b x xs \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>
theory Trace_RG

lemma rg_vcg_handle_elseE:
  "\<lbrakk> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q'\<rbrace>,\<lbrace>E'\<rbrace>; \<And>e. \<lbrace>E' e\<rbrace>,\<lbrace>R\<rbrace> g e \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>; \<And>x. \<lbrace>Q' x\<rbrace>,\<lbrace>R\<rbrace> h x \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> \<rbrakk>
   \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f <handle> g <else> h \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" unfolding handle_elseE_def validIE_def by (wpsimp wp: bind_twp_fwd | assumption | rule conjI)+

(* 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>; \<And>e. \<lbrace>E' e\<rbrace>, \<lbrace>R\<rbrace> g e \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>; \<And>x. \<lbrace>Q' x\<rbrace>, \<lbrace>R\<rbrace> h x \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f <handle> g <else> h \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<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>; \<And>e. \<lbrace>E' e\<rbrace>, \<lbrace>R\<rbrace> g e \<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>; \<And>x. \<lbrace>Q' x\<rbrace>, \<lbrace>R\<rbrace> h x \<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>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f >>= case_sum g h \<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>
theory Trace_RG

lemma alternative_twp:
  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>P and P'\<rbrace>,\<lbrace>R\<rbrace> f \<sqinter> f' \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>" unfolding validI_def apply (rule conjI, fastforce simp: validI_prefix_closed[OF x] validI_prefix_closed[OF y]) by (fastforce simp: alternative_def post_by_rg[OF x] post_by_rg[OF y] guar_by_rg[OF x] guar_by_rg[OF y])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P and P'\<rbrace>, \<lbrace>R\<rbrace> f \<sqinter> f' \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. prefix_closed (f \<sqinter> f') \<and> (\<forall>s0 s tr res. (P and P') s0 s \<and> (tr, res) \<in> rely (f \<sqinter> 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')) proof (prove)
goal (1 subgoal):
 1. \<forall>s0 s tr res. (P and P') s0 s \<and> (tr, res) \<in> rely (f \<sqinter> 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 alternativeE_twp:
  assumes "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
  assumes "\<lbrace>P'\<rbrace>,\<lbrace>R\<rbrace> f' \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
  shows   "\<lbrace>P and P'\<rbrace>,\<lbrace>R\<rbrace> f \<sqinter> f' \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" unfolding validIE_def by (wpsimp wp: assms alternative_twp | fold validIE_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P and P'\<rbrace>, \<lbrace>R\<rbrace> f \<sqinter> f' \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P and P'\<rbrace>, \<lbrace>R\<rbrace> f \<sqinter> 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>
theory Trace_RG

lemma condition_twp:
  "\<lbrakk> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> A \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>; \<lbrace>P'\<rbrace>,\<lbrace>R\<rbrace> B \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace> \<rbrakk>
   \<Longrightarrow> \<lbrace>\<lambda>s0 s. if C s then P s0 s else P' s0 s\<rbrace>,\<lbrace>R\<rbrace> condition C A B \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>" by (auto simp: condition_def validI_def prefix_closed_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> A \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>; \<lbrace>P'\<rbrace>, \<lbrace>R\<rbrace> B \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s0 s. if C s then P s0 s else P' s0 s\<rbrace>, \<lbrace>R\<rbrace> condition C
  A
  B \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>
theory Trace_RG

lemma conditionE_twp:
  "\<lbrakk> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> A \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>; \<lbrace>P'\<rbrace>,\<lbrace>R\<rbrace> B \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> \<rbrakk>
   \<Longrightarrow> \<lbrace>\<lambda>s0 s. if C s then P s0 s else P' s0 s\<rbrace>,\<lbrace>R\<rbrace> condition C A B \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" by (clarsimp simp: validIE_def condition_twp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> A \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>; \<lbrace>P'\<rbrace>, \<lbrace>R\<rbrace> B \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s0 s. if C s then P s0 s else P' s0 s\<rbrace>, \<lbrace>R\<rbrace> condition C
  A
  B \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>
theory Trace_RG

lemma when_twp[wp_split]:
  "\<lbrakk> P \<Longrightarrow> \<lbrace>P'\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>if P then P' else Q ()\<rbrace>,\<lbrace>R\<rbrace> when P f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>" unfolding when_def by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P \<Longrightarrow> \<lbrace>P'\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>) \<Longrightarrow> \<lbrace>if P then P' else Q ()\<rbrace>, \<lbrace>R\<rbrace> when P f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. (P \<Longrightarrow> \<lbrace>P'\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>) \<Longrightarrow> \<lbrace>if P then P' else Q ()\<rbrace>, \<lbrace>R\<rbrace> if P then f else return () \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>
theory Trace_RG

lemma unless_twp[wp_split]:
  "(\<not>P \<Longrightarrow> \<lbrace>P'\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>) \<Longrightarrow> \<lbrace>if P then Q () else P'\<rbrace>,\<lbrace>R\<rbrace> unless P f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>" unfolding unless_def by wpsimp (simp split: if_splits)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<not> P \<Longrightarrow> \<lbrace>P'\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>) \<Longrightarrow> \<lbrace>if P then Q () else P'\<rbrace>, \<lbrace>R\<rbrace> unless P f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<not> P \<Longrightarrow> \<lbrace>P'\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>) \<Longrightarrow> \<lbrace>if P then Q () else P'\<rbrace>, \<lbrace>R\<rbrace> when (\<not> P) f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>
theory Trace_RG

lemma whenE_twp:
  "(P \<Longrightarrow> \<lbrace>P'\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>) \<Longrightarrow> \<lbrace>if P then P' else Q ()\<rbrace>,\<lbrace>R\<rbrace> whenE P f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" unfolding whenE_def by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P \<Longrightarrow> \<lbrace>P'\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>) \<Longrightarrow> \<lbrace>if P then P' else Q ()\<rbrace>, \<lbrace>R\<rbrace> whenE P f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. (P \<Longrightarrow> \<lbrace>P'\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>) \<Longrightarrow> \<lbrace>if P then P' else Q ()\<rbrace>, \<lbrace>R\<rbrace> if P then f else returnOk () \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>
theory Trace_RG

lemma unlessE_twp:
  "(\<not> P \<Longrightarrow> \<lbrace>P'\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>) \<Longrightarrow> \<lbrace>if P then Q () else P'\<rbrace>,\<lbrace>R\<rbrace> unlessE P f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" unfolding unlessE_def by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<not> P \<Longrightarrow> \<lbrace>P'\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>) \<Longrightarrow> \<lbrace>if P then Q () else P'\<rbrace>, \<lbrace>R\<rbrace> unlessE P f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<not> P \<Longrightarrow> \<lbrace>P'\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>) \<Longrightarrow> \<lbrace>if P then Q () else P'\<rbrace>, \<lbrace>R\<rbrace> if P then returnOk () else f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>
theory Trace_RG

lemma maybeM_twp:
  "(\<And>x. y = Some x \<Longrightarrow> \<lbrace>P x\<rbrace>,\<lbrace>R\<rbrace> m x \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>) \<Longrightarrow>
   \<lbrace>\<lambda>s0 s. (\<forall>x. y = Some x \<longrightarrow> P x s0 s) \<and> (y = None \<longrightarrow> Q () s0 s)\<rbrace>,\<lbrace>R\<rbrace> maybeM m y \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>" unfolding maybeM_def by wpsimp (simp split: if_splits)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. y = Some x \<Longrightarrow> \<lbrace>P x\<rbrace>, \<lbrace>R\<rbrace> m x \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s0 s. (\<forall>x. y = Some x \<longrightarrow> P x s0 s) \<and> (y = None \<longrightarrow> Q () s0 s)\<rbrace>, \<lbrace>R\<rbrace> maybeM m y \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<And>x. y = Some x \<Longrightarrow> \<lbrace>P x\<rbrace>, \<lbrace>R\<rbrace> m x \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s0 s. (\<forall>x. y = Some x \<longrightarrow> P x s0 s) \<and> (y = None \<longrightarrow> Q () s0 s)\<rbrace>, \<lbrace>R\<rbrace> case y of None \<Rightarrow> return () | Some x \<Rightarrow> m x \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>
theory Trace_RG

lemma notM_twp:
  "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> m \<lbrace>G\<rbrace>,\<lbrace>\<lambda>c. Q (\<not> c)\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> notM m \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>" unfolding notM_def by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> m \<lbrace>G\<rbrace>, \<lbrace>\<lambda>c. Q (\<not> c)\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> notM m \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> m \<lbrace>G\<rbrace>, \<lbrace>\<lambda>c. Q (\<not> c)\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> do c <- m;
return (\<not> c)
od \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>
theory Trace_RG

lemma ifM_twp:
  assumes [wp]: "\<lbrace>Q\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>S\<rbrace>" "\<lbrace>Q'\<rbrace>,\<lbrace>R\<rbrace> g \<lbrace>G\<rbrace>,\<lbrace>S\<rbrace>"
  assumes [wp]: "\<lbrace>A\<rbrace>,\<lbrace>R\<rbrace> P \<lbrace>G\<rbrace>,\<lbrace>\<lambda>c s0 s. c \<longrightarrow> Q s0 s\<rbrace>" "\<lbrace>B\<rbrace>,\<lbrace>R\<rbrace> P \<lbrace>G\<rbrace>,\<lbrace>\<lambda>c s0 s. \<not>c \<longrightarrow> Q' s0 s\<rbrace>"
  shows "\<lbrace>A and B\<rbrace>,\<lbrace>R\<rbrace> ifM P f g \<lbrace>G\<rbrace>,\<lbrace>S\<rbrace>" unfolding ifM_def by (wpsimp wp: rg_vcg_if_split rg_vcg_conj_lift)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>A and B\<rbrace>, \<lbrace>R\<rbrace> ifM P f g \<lbrace>G\<rbrace>, \<lbrace>S\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>A and B\<rbrace>, \<lbrace>R\<rbrace> do c <- P;
if c then f else g
od \<lbrace>G\<rbrace>, \<lbrace>S\<rbrace>
theory Trace_RG

lemma andM_twp:
  assumes [wp]: "\<lbrace>Q'\<rbrace>,\<lbrace>R\<rbrace> B \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>"
  assumes [wp]: "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> A \<lbrace>G\<rbrace>,\<lbrace>\<lambda>c s0 s. c \<longrightarrow> Q' s0 s\<rbrace>" "\<lbrace>P'\<rbrace>,\<lbrace>R\<rbrace> A \<lbrace>G\<rbrace>,\<lbrace>\<lambda>c s0 s. \<not> c \<longrightarrow> Q False s0 s\<rbrace>"
  shows "\<lbrace>P and P'\<rbrace>,\<lbrace>R\<rbrace> andM A B \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>" unfolding andM_def by (wpsimp wp: ifM_twp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P and P'\<rbrace>, \<lbrace>R\<rbrace> andM A B \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P and P'\<rbrace>, \<lbrace>R\<rbrace> ifM A B (return False) \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>
theory Trace_RG

lemma orM_twp:
  assumes [wp]: "\<lbrace>Q'\<rbrace>,\<lbrace>R\<rbrace> B \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>"
  assumes [wp]: "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> A \<lbrace>G\<rbrace>,\<lbrace>\<lambda>c s0 s. c \<longrightarrow> Q True s0 s\<rbrace>" "\<lbrace>P'\<rbrace>,\<lbrace>R\<rbrace> A \<lbrace>G\<rbrace>,\<lbrace>\<lambda>c s0 s. \<not> c \<longrightarrow> Q' s0 s\<rbrace>"
  shows "\<lbrace>P and P'\<rbrace>,\<lbrace>R\<rbrace> orM A B \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>" unfolding orM_def by (wp ifM_twp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P and P'\<rbrace>, \<lbrace>R\<rbrace> orM A B \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P and P'\<rbrace>, \<lbrace>R\<rbrace> ifM A (return True) B \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>
theory Trace_RG

lemma whenM_twp:
  assumes [wp]: "\<lbrace>Q\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>S\<rbrace>"
  assumes [wp]: "\<lbrace>A\<rbrace>,\<lbrace>R\<rbrace> P \<lbrace>G\<rbrace>,\<lbrace>\<lambda>c s0 s. c \<longrightarrow> Q s0 s\<rbrace>" "\<lbrace>B\<rbrace>,\<lbrace>R\<rbrace> P \<lbrace>G\<rbrace>,\<lbrace>\<lambda>c s0 s. \<not>c \<longrightarrow> S () s0 s\<rbrace>"
  shows "\<lbrace>A and B\<rbrace>,\<lbrace>R\<rbrace> whenM P f \<lbrace>G\<rbrace>,\<lbrace>S\<rbrace>" unfolding whenM_def by (wp ifM_twp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>A and B\<rbrace>, \<lbrace>R\<rbrace> whenM P f \<lbrace>G\<rbrace>, \<lbrace>S\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>A and B\<rbrace>, \<lbrace>R\<rbrace> ifM P f (return ()) \<lbrace>G\<rbrace>, \<lbrace>S\<rbrace>
theory Trace_RG

lemma rg_K_bind[wp_split]:
  "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> K_bind f x \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>" by simp

(* 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> K_bind f x \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>
theory Trace_RG

lemma validE_K_bind[wp_split]:
  "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> x \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> K_bind x f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" by simp

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