kings-crown/FVELER_Isabelle huggingface dataset:
theory WPEx

lemma valid_strengthen_with_mresults:
  "\<lbrakk> \<And>s rv s'. \<lbrakk> (rv, s', s) \<in> mresults f; wpex_name_for_id (Q' s rv s') \<rbrakk> \<Longrightarrow> Q rv s';
     \<And>prev_s. \<lbrace>P prev_s\<rbrace> f \<lbrace>Q' prev_s\<rbrace> \<rbrakk>
   \<Longrightarrow> \<lbrace>\<lambda>s. P s s\<rbrace> f \<lbrace>Q\<rbrace>" by (clarsimp simp: valid_def mresults_def wpex_name_for_id_def) blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s rv s'. \<lbrakk>(rv, s', s) \<in> mresults f; wpex_name_for_id (Q' s rv s')\<rbrakk> \<Longrightarrow> Q rv s'; \<And>prev_s. \<lbrace>P prev_s\<rbrace> f \<lbrace>Q' prev_s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P s s\<rbrace> f \<lbrace>Q\<rbrace>
theory WPEx

lemma wpex_name_for_idE: "wpex_name_for_id P \<Longrightarrow> P" by (simp add: wpex_name_for_id_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. wpex_name_for_id P \<Longrightarrow> P
theory WPEx

lemma "\<lbrace>P\<rbrace> do v \<leftarrow> return (Suc 0); return (Suc (Suc 0)) od \<lbrace>(=)\<rbrace>" apply (rule hoare_pre) apply (rule hoare_seq_ext)+ apply (wps | rule hoare_vcg_prop)+ oops

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> do v <- return (Suc 0);
return (Suc (Suc 0))
od \<lbrace>(=)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do v <- return (Suc 0);
return (Suc (Suc 0))
od \<lbrace>(=)\<rbrace>
 2. \<And>s. P s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>v. \<lbrace>?B3 v\<rbrace> return (Suc (Suc 0)) \<lbrace>(=)\<rbrace>
 2. \<lbrace>?Q\<rbrace> return (Suc 0) \<lbrace>?B3\<rbrace>
 3. \<And>s. P s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. P s \<Longrightarrow> Suc (Suc 0) = s
theory WPI

lemma bool_function_four_cases:
  "f = Not \<or> f = id \<or> f = (\<lambda>_. True) \<or> f = (\<lambda>_. False)" by (auto simp add: fun_eq_iff all_bool_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f = Not \<or> f = id \<or> f = (\<lambda>_. True) \<or> f = (\<lambda>_. False)
theory WPI

lemma trips_True: "trip True" by (simp add: trip_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. trip True
theory WPI

lemma trips_push_all1:
  "trip (\<forall>x. \<lbrace>\<lambda>s. Q x s\<rbrace> f \<lbrace>\<lambda>r s. Q' x r s\<rbrace>) \<Longrightarrow>
    trip (\<lbrace>\<lambda>s. \<forall>x. Q x s\<rbrace> f \<lbrace>\<lambda>r s. \<forall>x. Q' x r s\<rbrace>)" by (simp add: trip_def valid_def; blast)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. trip (\<forall>x. \<lbrace>Q x\<rbrace> f \<lbrace>Q' x\<rbrace>) \<Longrightarrow> trip \<lbrace>\<lambda>s. \<forall>x. Q x s\<rbrace> f \<lbrace>\<lambda>r s. \<forall>x. Q' x r s\<rbrace>
theory WPI

lemma trips_push_all2:
  "trip (\<forall>x y. \<lbrace>\<lambda>s. Q x y s\<rbrace> f \<lbrace>\<lambda>r s. Q' x y r s\<rbrace>) \<Longrightarrow>
    trip (\<lbrace>\<lambda>s. \<forall>x y. Q x y s\<rbrace> f \<lbrace>\<lambda>r s. \<forall>x y. Q' x y r s\<rbrace>)" by (simp add: trip_def valid_def; blast)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. trip (\<forall>x y. \<lbrace>Q x y\<rbrace> f \<lbrace>Q' x y\<rbrace>) \<Longrightarrow> trip \<lbrace>\<lambda>s. \<forall>x y. Q x y s\<rbrace> f \<lbrace>\<lambda>r s. \<forall>x y. Q' x y r s\<rbrace>
theory WPI

lemma trips_push_ex1:
  "trip (\<exists>x. \<lbrace>\<lambda>s. Q s\<rbrace> f \<lbrace>\<lambda>r s. Q' x r s\<rbrace>) \<Longrightarrow>
    trip (\<lbrace>\<lambda>s. Q s\<rbrace> f \<lbrace>\<lambda>r s. \<exists>x. Q' x r s\<rbrace>)" by (simp add: trip_def valid_def,blast)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. trip (\<exists>x. \<lbrace>Q\<rbrace> f \<lbrace>Q' x\<rbrace>) \<Longrightarrow> trip \<lbrace>Q\<rbrace> f \<lbrace>\<lambda>r s. \<exists>x. Q' x r s\<rbrace>
theory WPI

lemma trips_True_drop: "trip True \<Longrightarrow> R \<Longrightarrow> R" by -

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>trip True; R\<rbrakk> \<Longrightarrow> R
theory WPI

lemma trips_contr_drop: "trip \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_ _. False\<rbrace> \<Longrightarrow> R \<Longrightarrow> R" by -

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>trip \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_ _. False\<rbrace>; R\<rbrakk> \<Longrightarrow> R
theory WPI

lemma trip_init:
  "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. post_imp True (Q r s)\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>" apply (erule hoare_strengthen_post) by (simp add: post_imp_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. post_imp True (Q r s)\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>rv s. post_imp True (Q rv s) \<Longrightarrow> Q rv s
theory WPI

lemma trip_drop:
  "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. post_imp (Q' r s) (Q r s)\<rbrace>" apply (erule hoare_strengthen_post) by (simp add: post_imp_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. post_imp (Q' r s) (Q r s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>rv s. Q rv s \<Longrightarrow> post_imp (Q' rv s) (Q rv s)
theory WPI

lemma hoare_add_trip:
  "trip (\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>) \<Longrightarrow>
  \<lbrace>P'\<rbrace> f \<lbrace>\<lambda>r s. post_imp (Q r s \<and> Q' r s) (R r s)\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> P' s\<rbrace> f \<lbrace>\<lambda>r s. post_imp (Q' r s) (R r s)\<rbrace>" by (auto simp: trip_def valid_def post_imp_def; blast)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>trip \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; \<lbrace>P'\<rbrace> f \<lbrace>\<lambda>r s. post_imp (Q r s \<and> Q' r s) (R r s)\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> P' s\<rbrace> f \<lbrace>\<lambda>r s. post_imp (Q' r s) (R r s)\<rbrace>
theory WPI

lemma trivial_test: "atomic f a b (\<lambda>_ _. True) B \<Longrightarrow> R \<Longrightarrow> R" by -

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>atomic f a b (\<lambda>_ _. True) B; R\<rbrakk> \<Longrightarrow> R
theory Eisbach_WP

lemma packed_validE:"(\<And>si r s. packed_valid P f si r s \<Longrightarrow> Q r s) \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>" by (clarsimp simp: valid_def packed_valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>si r s. packed_valid P f si r s \<Longrightarrow> Q r s) \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>
theory Eisbach_WP

lemma packed_validI: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<Longrightarrow> \<forall>si r s. packed_valid P f si r s \<longrightarrow> Q r s" apply (clarsimp simp: valid_def packed_valid_def) by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<Longrightarrow> \<forall>si r s. packed_valid P f si r s \<longrightarrow> Q r s proof (prove)
goal (1 subgoal):
 1. \<And>si r s. \<lbrakk>\<forall>s. P s \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (r, s') \<Rightarrow> Q r s'); P si; (r, s) \<in> fst (f si)\<rbrakk> \<Longrightarrow> Q r s
theory Eisbach_WP

lemma packed_validRE:"(\<And>si r s. packed_validR P f si r s \<Longrightarrow> Q r s) \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-" apply (clarsimp simp: validE_R_def validE_def valid_def packed_validR_def) by (metis sum.case sumE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>si r s. packed_validR P f si r s \<Longrightarrow> Q r s) \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<And>si r s. P si \<and> (Inr r, s) \<in> fst (f si) \<Longrightarrow> Q r s; P s; (a, b) \<in> fst (f s)\<rbrakk> \<Longrightarrow> case a of Inl e \<Rightarrow> True | Inr r \<Rightarrow> Q r b
theory Eisbach_WP

lemma packed_validRI: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,- \<Longrightarrow> \<forall>si r s. packed_validR P f si r s \<longrightarrow> Q r s" apply (clarsimp simp: valid_def validE_R_def validE_def packed_validR_def) by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, - \<Longrightarrow> \<forall>si r s. packed_validR P f si r s \<longrightarrow> Q r s proof (prove)
goal (1 subgoal):
 1. \<And>si r s. \<lbrakk>\<forall>s. P s \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (Inl e, s') \<Rightarrow> True | (Inr ra, s') \<Rightarrow> Q ra s'); P si; (Inr r, s) \<in> fst (f si)\<rbrakk> \<Longrightarrow> Q r s
theory Eisbach_WP

lemma trivial_imp: "\<forall>r s. Q r s \<longrightarrow> Q r s" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>r s. Q r s \<longrightarrow> Q r s
theory Eisbach_WP

lemma uncurry2: "\<forall>r s. Q r s \<and> Q' r s \<longrightarrow> Q'' r s \<Longrightarrow> \<forall>r s. Q r s \<longrightarrow> Q' r s \<longrightarrow> Q'' r s" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>r s. Q r s \<and> Q' r s \<longrightarrow> Q'' r s \<Longrightarrow> \<forall>r s. Q r s \<longrightarrow> Q' r s \<longrightarrow> Q'' r s
theory Eisbach_WP

lemma hoare_decompose:
  "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. Q r s \<and> Q' r s\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<and> \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>" by (fastforce simp add: valid_def pred_conj_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. Q r s \<and> Q' r s\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<and> \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>
theory Eisbach_WP

lemma hoare_decomposeE_R:
  "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. Q r s \<and> Q' r s\<rbrace>,- \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,- \<and> \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>,-" by (fastforce simp add: validE_R_def validE_def valid_def pred_conj_def split: prod.splits sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. Q r s \<and> Q' r s\<rbrace>, - \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, - \<and> \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>, -
theory Eisbach_WP

lemma hoare_decomposeE_E:
  "\<lbrace>P\<rbrace> f -,\<lbrace>\<lambda>r s. Q r s \<and> Q' r s\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f -,\<lbrace>Q\<rbrace> \<and> \<lbrace>P\<rbrace> f -,\<lbrace>Q'\<rbrace>" by (fastforce simp add: validE_E_def validE_def valid_def pred_conj_def split: prod.splits sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f -, \<lbrace>\<lambda>r s. Q r s \<and> Q' r s\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f -, \<lbrace>Q\<rbrace> \<and> \<lbrace>P\<rbrace> f -, \<lbrace>Q'\<rbrace>
theory Eisbach_WP

lemma hoare_decomposeE:
  "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. E r s \<and> E' r s\<rbrace>,\<lbrace>\<lambda>r s. R r s \<and> R' r s\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>E\<rbrace>,- \<and> \<lbrace>P\<rbrace> f \<lbrace>E'\<rbrace>,- \<and> \<lbrace>P\<rbrace> f -,\<lbrace>R\<rbrace> \<and> \<lbrace>P\<rbrace> f -,\<lbrace>R'\<rbrace>" by (fastforce simp add: validE_R_def validE_E_def validE_def valid_def pred_conj_def split: prod.splits sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. E r s \<and> E' r s\<rbrace>, \<lbrace>\<lambda>r s. R r s \<and> R' r s\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>E\<rbrace>, - \<and> \<lbrace>P\<rbrace> f \<lbrace>E'\<rbrace>, - \<and> \<lbrace>P\<rbrace> f -, \<lbrace>R\<rbrace> \<and> \<lbrace>P\<rbrace> f -, \<lbrace>R'\<rbrace>
theory Nondet_Strengthen_Setup

lemma strengthen_hoare [strg]:
  "\<lbrakk>\<And>r s. st F (\<longrightarrow>) (Q r s) (R r s)\<rbrakk>
   \<Longrightarrow> st F (\<longrightarrow>) (\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>) (\<lbrace>P\<rbrace> f \<lbrace>R\<rbrace>)" by (cases F, auto elim: hoare_strengthen_post)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>r s. st F (\<longrightarrow>) (Q r s) (R r s)) \<Longrightarrow> st F (\<longrightarrow>) \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<lbrace>P\<rbrace> f \<lbrace>R\<rbrace>
theory Nondet_Strengthen_Setup

lemma strengthen_validE_R_cong[strg]:
  "\<lbrakk>\<And>r s. st F (\<longrightarrow>) (Q r s) (R r s)\<rbrakk>
   \<Longrightarrow> st F (\<longrightarrow>) (\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, -) (\<lbrace>P\<rbrace> f \<lbrace>R\<rbrace>, -)" by (cases F, auto intro: hoare_post_imp_R)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>r s. st F (\<longrightarrow>) (Q r s) (R r s)) \<Longrightarrow> st F (\<longrightarrow>) \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, - \<lbrace>P\<rbrace> f \<lbrace>R\<rbrace>, -
theory Nondet_Strengthen_Setup

lemma strengthen_validE_cong[strg]:
  "\<lbrakk>\<And>r s. st F (\<longrightarrow>) (Q r s) (R r s); \<And>r s. st F (\<longrightarrow>) (S r s) (T r s)\<rbrakk>
   \<Longrightarrow> st F (\<longrightarrow>) (\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>S\<rbrace>) (\<lbrace>P\<rbrace> f \<lbrace>R\<rbrace>, \<lbrace>T\<rbrace>)" by (cases F, auto elim: hoare_post_impErr)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>r s. st F (\<longrightarrow>) (Q r s) (R r s); \<And>r s. st F (\<longrightarrow>) (S r s) (T r s)\<rbrakk> \<Longrightarrow> st F (\<longrightarrow>) \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>S\<rbrace> \<lbrace>P\<rbrace> f \<lbrace>R\<rbrace>, \<lbrace>T\<rbrace>
theory Nondet_Strengthen_Setup

lemma strengthen_validE_E_cong[strg]:
  "\<lbrakk>\<And>r s. st F (\<longrightarrow>) (S r s) (T r s)\<rbrakk>
   \<Longrightarrow> st F (\<longrightarrow>) (\<lbrace>P\<rbrace> f -, \<lbrace>S\<rbrace>) (\<lbrace>P\<rbrace> f -, \<lbrace>T\<rbrace>)" by (cases F, auto elim: hoare_post_impErr simp: validE_E_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>r s. st F (\<longrightarrow>) (S r s) (T r s)) \<Longrightarrow> st F (\<longrightarrow>) \<lbrace>P\<rbrace> f -, \<lbrace>S\<rbrace> \<lbrace>P\<rbrace> f -, \<lbrace>T\<rbrace>
theory Nondet_Strengthen_Setup

lemma wpfix_strengthen_hoare:
  "\<lbrakk>\<And>s. st (\<not> F) (\<longrightarrow>) (P s) (P' s); \<And>r s. st F (\<longrightarrow>) (Q r s) (Q' r s)\<rbrakk>
   \<Longrightarrow> st F (\<longrightarrow>) (\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>) (\<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>)" by (cases F, auto elim: hoare_chain)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. st (\<not> F) (\<longrightarrow>) (P s) (P' s); \<And>r s. st F (\<longrightarrow>) (Q r s) (Q' r s)\<rbrakk> \<Longrightarrow> st F (\<longrightarrow>) \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>
theory Nondet_Strengthen_Setup

lemma wpfix_strengthen_validE_R_cong:
  "\<lbrakk>\<And>s. st (\<not> F) (\<longrightarrow>) (P s) (P' s); \<And>r s. st F (\<longrightarrow>) (Q r s) (Q' r s)\<rbrakk>
   \<Longrightarrow> st F (\<longrightarrow>) (\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, -) (\<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>, -)" by (cases F, auto elim: hoare_chainE simp: validE_R_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. st (\<not> F) (\<longrightarrow>) (P s) (P' s); \<And>r s. st F (\<longrightarrow>) (Q r s) (Q' r s)\<rbrakk> \<Longrightarrow> st F (\<longrightarrow>) \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, - \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>, -
theory Nondet_Strengthen_Setup

lemma wpfix_strengthen_validE_cong:
  "\<lbrakk>\<And>s. st (\<not> F) (\<longrightarrow>) (P s) (P' s); \<And>r s. st F (\<longrightarrow>) (Q r s) (R r s);
    \<And>r s. st F (\<longrightarrow>) (S r s) (T r s)\<rbrakk>
   \<Longrightarrow> st F (\<longrightarrow>) (\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>S\<rbrace>) (\<lbrace>P'\<rbrace> f \<lbrace>R\<rbrace>, \<lbrace>T\<rbrace>)" by (cases F, auto elim: hoare_chainE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. st (\<not> F) (\<longrightarrow>) (P s) (P' s); \<And>r s. st F (\<longrightarrow>) (Q r s) (R r s); \<And>r s. st F (\<longrightarrow>) (S r s) (T r s)\<rbrakk> \<Longrightarrow> st F (\<longrightarrow>) \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>S\<rbrace> \<lbrace>P'\<rbrace> f \<lbrace>R\<rbrace>, \<lbrace>T\<rbrace>
theory Nondet_Strengthen_Setup

lemma wpfix_strengthen_validE_E_cong:
  "\<lbrakk>\<And>s. st (\<not> F) (\<longrightarrow>) (P s) (P' s); \<And>r s. st F (\<longrightarrow>) (S r s) (T r s)\<rbrakk>
   \<Longrightarrow> st F (\<longrightarrow>) (\<lbrace>P\<rbrace> f -, \<lbrace>S\<rbrace>) (\<lbrace>P'\<rbrace> f -, \<lbrace>T\<rbrace>)" by (cases F, auto elim: hoare_chainE simp: validE_E_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. st (\<not> F) (\<longrightarrow>) (P s) (P' s); \<And>r s. st F (\<longrightarrow>) (S r s) (T r s)\<rbrakk> \<Longrightarrow> st F (\<longrightarrow>) \<lbrace>P\<rbrace> f -, \<lbrace>S\<rbrace> \<lbrace>P'\<rbrace> f -, \<lbrace>T\<rbrace>
theory Nondet_Strengthen_Setup

lemma wpfix_no_fail_cong:
  "\<lbrakk>\<And>s. st (\<not> F) (\<longrightarrow>) (P s) (P' s)\<rbrakk>
   \<Longrightarrow> st F (\<longrightarrow>) (no_fail P f) (no_fail P' f)" by (cases F, auto elim: no_fail_pre)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s. st (\<not> F) (\<longrightarrow>) (P s) (P' s)) \<Longrightarrow> st F (\<longrightarrow>) (no_fail P f) (no_fail P' f)
theory Nondet_More_VCG

lemma hoare_take_disjunct:
  "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. P' rv s \<and> (False \<or> P'' rv s)\<rbrace>
   \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>P''\<rbrace>" by (erule hoare_strengthen_post, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. P' rv s \<and> (False \<or> P'' rv s)\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>P''\<rbrace>
theory Nondet_More_VCG

lemma hoare_post_add:
  "\<lbrace>P\<rbrace> S \<lbrace>\<lambda>r s. R r s \<and> Q r s\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> S \<lbrace>Q\<rbrace>" by (erule hoare_strengthen_post, simp)

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

lemma hoare_post_addE:
  "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>_ s. R s \<and> Q s\<rbrace>, \<lbrace>T\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_ s. Q s\<rbrace>, \<lbrace>T\<rbrace>" by (erule hoare_post_impErr'; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_ s. R s \<and> Q s\<rbrace>, \<lbrace>T\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. Q\<rbrace>, \<lbrace>T\<rbrace>
theory Nondet_More_VCG

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

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

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

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

lemma hoare_name_pre_state:
  "\<lbrakk> \<And>s. P s \<Longrightarrow> \<lbrace>(=) s\<rbrace> f \<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>" by (clarsimp simp: valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s. P s \<Longrightarrow> \<lbrace>(=) s\<rbrace> f \<lbrace>Q\<rbrace>) \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>
theory Nondet_More_VCG

lemma hoare_name_pre_stateE:
  "\<lbrakk>\<And>s. P s \<Longrightarrow> \<lbrace>(=) s\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>" by (clarsimp simp: validE_def2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s. P s \<Longrightarrow> \<lbrace>(=) s\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>) \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>