kings-crown/FVELER_Isabelle huggingface dataset:
theory Trace_More_RG

lemma rg_post_add:
  "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> S \<lbrace>G\<rbrace>,\<lbrace>\<lambda>r s0 s. Q' r s0 s \<and> Q r s0 s\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> S \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>" by (erule rg_strengthen_post, simp)

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

lemma rg_post_addE:
  "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>_ s0 s. R s0 s \<and> Q s0 s\<rbrace>,\<lbrace>T\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>_ s0 s. Q s0 s\<rbrace>,\<lbrace>T\<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>_ s0 s. R s0 s \<and> Q s0 s\<rbrace>, \<lbrace>T\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_. Q\<rbrace>, \<lbrace>T\<rbrace>
theory Trace_More_RG

lemma rg_pre_add:
  "(\<forall>s0 s. P s0 s \<longrightarrow> P' s0 s) \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace> \<longleftrightarrow> \<lbrace>P and P'\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>" apply (subst iff_conv_conj_imp) by(intro conjI impI; rule rg_weaken_pre, assumption, clarsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s0 s. P s0 s \<longrightarrow> P' s0 s \<Longrightarrow> \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace> = \<lbrace>P and P'\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<forall>s0 s. P s0 s \<longrightarrow> P' s0 s \<Longrightarrow> (\<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace> \<longrightarrow> \<lbrace>P and P'\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>) \<and> (\<lbrace>P and P'\<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>)
theory Trace_More_RG

lemma rg_pre_addE:
  "(\<forall>s0 s. P s0 s \<longrightarrow> R s0 s) \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>S\<rbrace> \<longleftrightarrow> \<lbrace>P and R\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>S\<rbrace>" apply (subst iff_conv_conj_imp) by(intro conjI impI; rule rg_weaken_preE, assumption, clarsimp)

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

lemma rg_name_pre_state:
  "\<lbrakk> \<And>s0 s. P s0 s \<Longrightarrow> \<lbrace>\<lambda>_. (=) s\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>; prefix_closed f \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>" by (clarsimp simp: validI_def)

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

lemma rg_name_pre_stateE:
  "\<lbrakk>\<And>s0 s. P s0 s \<Longrightarrow> \<lbrace>\<lambda>_. (=) s\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>; prefix_closed f\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" by (clarsimp simp: validIE_def2)

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

lemma rg_vcg_if_lift_strong:
  "\<lbrakk> \<lbrace>P'\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>P\<rbrace>; \<lbrace>\<lambda>s0 s. \<not> P' s0 s\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. \<not> P rv s0 s\<rbrace>; \<lbrace>Q'\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>; \<lbrace>S'\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>S\<rbrace> \<rbrakk> \<Longrightarrow>
   \<lbrace>\<lambda>s0 s. if P' s0 s then Q' s0 s else S' s0 s\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. if P rv s0 s then Q rv s0 s else S rv s0 s\<rbrace>"

  "\<lbrakk> \<lbrace>P'\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>P\<rbrace>; \<lbrace>\<lambda>s0 s. \<not> P' s0 s\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. \<not> P rv s0 s\<rbrace>; \<lbrace>Q'\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace> Q\<rbrace>; \<lbrace>S'\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>S\<rbrace> \<rbrakk> \<Longrightarrow>
   \<lbrace>\<lambda>s0 s. if P' s0 s then Q' s0 s else S' s0 s\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. (if P rv s0 s then Q rv else S rv) s0 s\<rbrace>" by (wpsimp wp: rg_vcg_imp_lift' | assumption | fastforce)+

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

lemma rg_pre_tautI:
  "\<lbrakk> \<lbrace>A and P\<rbrace>,\<lbrace>R\<rbrace> a \<lbrace>G\<rbrace>,\<lbrace>B\<rbrace>; \<lbrace>A and not P\<rbrace>,\<lbrace>R\<rbrace> a \<lbrace>G\<rbrace>,\<lbrace>B\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace>,\<lbrace>R\<rbrace> a \<lbrace>G\<rbrace>,\<lbrace>B\<rbrace>" by (fastforce simp: validI_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>A and P\<rbrace>, \<lbrace>R\<rbrace> a \<lbrace>G\<rbrace>, \<lbrace>B\<rbrace>; \<lbrace>A and not P\<rbrace>, \<lbrace>R\<rbrace> a \<lbrace>G\<rbrace>, \<lbrace>B\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace>, \<lbrace>R\<rbrace> a \<lbrace>G\<rbrace>, \<lbrace>B\<rbrace>
theory Trace_More_RG

lemma rg_lift_Pf_pre_conj:
  assumes P: "\<And>x. \<lbrace>\<lambda>s0 s. Q x s0 s\<rbrace>,\<lbrace>R\<rbrace> m \<lbrace>G\<rbrace>,\<lbrace>P x\<rbrace>"
  assumes f: "\<And>P. \<lbrace>\<lambda>s0 s. P (g s0 s) \<and> P' s0 s\<rbrace>,\<lbrace>R\<rbrace> m \<lbrace>G\<rbrace>,\<lbrace>\<lambda>_ s0 s. P (f s0 s)\<rbrace>"
  shows "\<lbrace>\<lambda>s0 s. Q (g s0 s) s0 s \<and> P' s0 s\<rbrace>,\<lbrace>R\<rbrace> m \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. P (f s0 s) rv s0 s\<rbrace>" apply (clarsimp simp: validI_def validI_prefix_closed[OF f] guar_by_rg[OF f]) apply (rule use_validI[OF _ P], simp) apply (rule use_validI[OF _ f], simp+) done

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

lemma rg_if_r_and:
  "\<lbrace>P\<rbrace>,\<lbrace>R'\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>r. if R r then Q r else Q' r\<rbrace>
   = \<lbrace>P\<rbrace>,\<lbrace>R'\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>r s0 s. (R r \<longrightarrow> Q r s0 s) \<and> (\<not>R r \<longrightarrow> Q' r 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>r. if R r then Q r else Q' r\<rbrace> = \<lbrace>P\<rbrace>, \<lbrace>R'\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>\<lambda>r s0 s. (R r \<longrightarrow> Q r s0 s) \<and> (\<not> R r \<longrightarrow> Q' r s0 s)\<rbrace>
theory Trace_More_RG

lemma rg_convert_imp:
  "\<lbrakk> \<lbrace>\<lambda>s0 s. \<not> P s0 s\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. \<not> Q s0 s\<rbrace>; \<lbrace>P'\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>S\<rbrace> \<rbrakk>
   \<Longrightarrow> \<lbrace>\<lambda>s0 s. P s0 s \<longrightarrow> P' s0 s\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. Q s0 s \<longrightarrow> S rv s0 s\<rbrace>" apply (simp only: imp_conv_disj) apply (erule(1) rg_vcg_disj_lift) done

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

lemma rg_case_option_wpR:
  "\<lbrakk>\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f None \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>; \<And>x. \<lbrace>P' x\<rbrace>,\<lbrace>R\<rbrace> f (Some x) \<lbrace>G\<rbrace>,\<lbrace>Q' x\<rbrace>,\<lbrace>E\<rbrace>\<rbrakk>
   \<Longrightarrow> \<lbrace>case_option P P' v\<rbrace>,\<lbrace>R\<rbrace> f v \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv. case v of None \<Rightarrow> Q rv | Some x \<Rightarrow> Q' x rv\<rbrace>,\<lbrace>E\<rbrace>" by (cases v) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f None \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>; \<And>x. \<lbrace>P' x\<rbrace>, \<lbrace>R\<rbrace> f (Some x) \<lbrace>G\<rbrace>, \<lbrace>Q' x\<rbrace>, \<lbrace>E\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>case v of None \<Rightarrow> P | Some x \<Rightarrow> P' x\<rbrace>, \<lbrace>R\<rbrace> f v \<lbrace>G\<rbrace>, \<lbrace>\<lambda>rv. case v of None \<Rightarrow> Q rv | Some x \<Rightarrow> Q' x rv\<rbrace>, \<lbrace>E\<rbrace>
theory Trace_More_RG

lemma rg_ex_all:
  "(\<forall>x. \<lbrace>P x\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>) = \<lbrace>\<lambda>s0 s. \<exists>x. P x s0 s\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>" apply (rule iffI) apply (fastforce simp: validI_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<forall>x. \<lbrace>P x\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>) = \<lbrace>\<lambda>s0 s. \<exists>x. P x s0 s\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<forall>x. \<lbrace>P x\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s0 s. \<exists>x. P x s0 s\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>
 2. \<lbrace>\<lambda>s0 s. \<exists>x. P x s0 s\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace> \<Longrightarrow> \<forall>x. \<lbrace>P x\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace> proof (prove)
goal:
No subgoals!
theory Trace_More_RG

lemma rg_imp_eq_substR:
  "\<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>\<lambda>rv s0 s. rv = x \<longrightarrow> Q x s0 s\<rbrace>,\<lbrace>E\<rbrace>" by (fastforce simp add: validI_def validIE_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>\<lambda>rv s0 s. rv = x \<longrightarrow> Q x s0 s\<rbrace>, \<lbrace>E\<rbrace>
theory Trace_More_RG

lemma rg_split_bind_case_sum:
  assumes x: "\<And>rv. \<lbrace>E rv\<rbrace>,\<lbrace>R\<rbrace> g rv \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>"
             "\<And>rv. \<lbrace>S rv\<rbrace>,\<lbrace>R\<rbrace> h rv \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>"
  assumes y: "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>S\<rbrace>,\<lbrace>E\<rbrace>"
  shows      "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f >>= case_sum g h \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>" apply (rule bind_twp[OF _ y[unfolded validIE_def]]) apply (wpsimp wp: x split: sum.splits) done

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

lemma rg_split_bind_case_sumE:
  assumes x: "\<And>rv. \<lbrace>S' rv\<rbrace>,\<lbrace>R\<rbrace> g rv \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
             "\<And>rv. \<lbrace>S rv\<rbrace>,\<lbrace>R\<rbrace> h rv \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
  assumes y: "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>S\<rbrace>,\<lbrace>S'\<rbrace>"
  shows      "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f >>= case_sum g h \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" apply (unfold validIE_def) apply (rule bind_twp[OF _ y[unfolded validIE_def]]) apply (wpsimp wp: x[unfolded validIE_def] split: sum.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f >>= case_sum g h \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<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> proof (prove)
goal (1 subgoal):
 1. \<And>r. \<lbrace>\<lambda>s0 s. case r of Inl e \<Rightarrow> S' e s0 s | Inr r \<Rightarrow> S r s0 s\<rbrace>, \<lbrace>R\<rbrace> case r of Inl x \<Rightarrow> g x | Inr x \<Rightarrow> 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> proof (prove)
goal:
No subgoals!
theory Trace_More_RG

lemma assertE_tsp:
  "\<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> assertE Q \<lbrace>G\<rbrace>,\<lbrace>\<lambda>rv s0 s. Q \<and> P s0 s\<rbrace>,\<lbrace>E\<rbrace>" by (wpsimp wp: assertE_wp)

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

lemma case_options_weak_twp:
  "\<lbrakk> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>; \<And>x. \<lbrace>P'\<rbrace>,\<lbrace>R\<rbrace> g x \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace> \<rbrakk>
   \<Longrightarrow> \<lbrace>P and P'\<rbrace>,\<lbrace>R\<rbrace> case opt of None \<Rightarrow> f | Some x \<Rightarrow> g x \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>" apply (cases opt) apply (clarsimp elim!: rg_weaken_pre) apply (rule rg_weaken_pre [where P'=P']) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>; \<And>x. \<lbrace>P'\<rbrace>, \<lbrace>R\<rbrace> g x \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P and P'\<rbrace>, \<lbrace>R\<rbrace> case opt of None \<Rightarrow> f | Some x \<Rightarrow> g x \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>; \<And>x. \<lbrace>P'\<rbrace>, \<lbrace>R\<rbrace> g x \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>; opt = None\<rbrakk> \<Longrightarrow> \<lbrace>P and P'\<rbrace>, \<lbrace>R\<rbrace> case opt of None \<Rightarrow> f | Some x \<Rightarrow> g x \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>
 2. \<And>a. \<lbrakk>\<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>; \<And>x. \<lbrace>P'\<rbrace>, \<lbrace>R\<rbrace> g x \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>; opt = Some a\<rbrakk> \<Longrightarrow> \<lbrace>P and P'\<rbrace>, \<lbrace>R\<rbrace> case opt of None \<Rightarrow> f | Some x \<Rightarrow> g x \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>\<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>; \<And>x. \<lbrace>P'\<rbrace>, \<lbrace>R\<rbrace> g x \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>; opt = Some a\<rbrakk> \<Longrightarrow> \<lbrace>P and P'\<rbrace>, \<lbrace>R\<rbrace> case opt of None \<Rightarrow> f | Some x \<Rightarrow> g x \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>\<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>; \<And>x. \<lbrace>P'\<rbrace>, \<lbrace>R\<rbrace> g x \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>; opt = Some a\<rbrakk> \<Longrightarrow> \<lbrace>P'\<rbrace>, \<lbrace>R\<rbrace> case opt of None \<Rightarrow> f | Some x \<Rightarrow> g x \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>
 2. \<And>a s0 s. \<lbrakk>\<lbrace>P\<rbrace>, \<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>; \<And>x. \<lbrace>P'\<rbrace>, \<lbrace>R\<rbrace> g x \<lbrace>G\<rbrace>, \<lbrace>Q\<rbrace>; opt = Some a; (P and P') s0 s\<rbrakk> \<Longrightarrow> P' s0 s proof (prove)
goal:
No subgoals!
theory Trace_More_RG

lemma case_option_twp_None_return:
  assumes [wp]: "\<And>x. \<lbrace>P' x\<rbrace>,\<lbrace>R\<rbrace> f x \<lbrace>G\<rbrace>,\<lbrace>\<lambda>_. Q\<rbrace>"
  shows "\<lbrakk>\<And>x s0 s. (Q and P x) s0 s \<Longrightarrow> P' x s0 s \<rbrakk>
         \<Longrightarrow> \<lbrace>Q and (\<lambda>s0 s. opt \<noteq> None \<longrightarrow> P (the opt) s0 s)\<rbrace>,\<lbrace>R\<rbrace>
             (case opt of None \<Rightarrow> return () | Some x \<Rightarrow> f x)
             \<lbrace>G\<rbrace>,\<lbrace>\<lambda>_. Q\<rbrace>" by (cases opt; wpsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x s0 s. (Q and P x) s0 s \<Longrightarrow> P' x s0 s) \<Longrightarrow> \<lbrace>Q and (\<lambda>s0 s. opt \<noteq> None \<longrightarrow> P (the opt) s0 s)\<rbrace>, \<lbrace>R\<rbrace> case opt of None \<Rightarrow> return () | Some x \<Rightarrow> f x \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_. Q\<rbrace>
theory Trace_More_RG

lemma case_option_twp_None_returnOk:
  assumes [wp]: "\<And>x. \<lbrace>P' x\<rbrace>,\<lbrace>R\<rbrace> f x \<lbrace>G\<rbrace>,\<lbrace>\<lambda>_. Q\<rbrace>,\<lbrace>E\<rbrace>"
  shows "\<lbrakk>\<And>x s0 s. (Q and P x) s0 s \<Longrightarrow> P' x s0 s \<rbrakk>
         \<Longrightarrow> \<lbrace>Q and (\<lambda>s0 s. opt \<noteq> None \<longrightarrow> P (the opt) s0 s)\<rbrace>,\<lbrace>R\<rbrace>
             (case opt of None \<Rightarrow> returnOk () | Some x \<Rightarrow> f x)
             \<lbrace>G\<rbrace>,\<lbrace>\<lambda>_. Q\<rbrace>,\<lbrace>E\<rbrace>" by (cases opt; wpsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x s0 s. (Q and P x) s0 s \<Longrightarrow> P' x s0 s) \<Longrightarrow> \<lbrace>Q and (\<lambda>s0 s. opt \<noteq> None \<longrightarrow> P (the opt) s0 s)\<rbrace>, \<lbrace>R\<rbrace> case opt of None \<Rightarrow> returnOk () | Some x \<Rightarrow> f x \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_. Q\<rbrace>, \<lbrace>E\<rbrace>