kings-crown/FVELER_Isabelle huggingface dataset:
theory Nondet_VCG

lemma hoare_vcg_imp_lift_R':
  "\<lbrakk> \<lbrace>P'\<rbrace> f \<lbrace>\<lambda>rv s. \<not> P rv s\<rbrace>, -; \<lbrace>Q'\<rbrace> f \<lbrace>Q\<rbrace>, - \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<not>P' s \<longrightarrow> Q' s\<rbrace> f \<lbrace>\<lambda>rv s. P rv s \<longrightarrow> Q rv s\<rbrace>, -" by (auto simp add: valid_def validE_R_def validE_def split_def split: sum.splits)

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

lemma hoare_vcg_imp_conj_lift[wp_comb]:
  "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<longrightarrow> Q' rv s\<rbrace>; \<lbrace>P'\<rbrace> f \<lbrace>\<lambda>rv s. (Q rv s \<longrightarrow> Q'' rv s) \<and> Q''' rv s\<rbrace> \<rbrakk> \<Longrightarrow>
   \<lbrace>P and P'\<rbrace> f \<lbrace>\<lambda>rv s. (Q rv s \<longrightarrow> Q' rv s \<and> Q'' rv s) \<and> Q''' rv s\<rbrace>" by (auto simp: valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<longrightarrow> Q' rv s\<rbrace>; \<lbrace>P'\<rbrace> f \<lbrace>\<lambda>rv s. (Q rv s \<longrightarrow> Q'' rv s) \<and> Q''' rv s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P and P'\<rbrace> f \<lbrace>\<lambda>rv s. (Q rv s \<longrightarrow> Q' rv s \<and> Q'' rv s) \<and> Q''' rv s\<rbrace>
theory Nondet_VCG

lemma hoare_absorb_imp:
  "\<lbrace> P \<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> R rv s\<rbrace> \<Longrightarrow> \<lbrace> P \<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<longrightarrow> R rv s\<rbrace>" by (erule hoare_post_imp[rotated], blast)

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

lemma hoare_vcg_const_imp_lift:
  "\<lbrakk> P \<Longrightarrow> \<lbrace>Q\<rbrace> m \<lbrace>R\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P \<longrightarrow> Q s\<rbrace> m \<lbrace>\<lambda>rv s. P \<longrightarrow> R rv s\<rbrace>" by (cases P, simp_all add: hoare_vcg_prop)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P \<Longrightarrow> \<lbrace>Q\<rbrace> m \<lbrace>R\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. P \<longrightarrow> Q s\<rbrace> m \<lbrace>\<lambda>rv s. P \<longrightarrow> R rv s\<rbrace>
theory Nondet_VCG

lemma hoare_vcg_const_imp_lift_E:
  "(P \<Longrightarrow> \<lbrace>Q\<rbrace> f -, \<lbrace>R\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. P \<longrightarrow> Q s\<rbrace> f -, \<lbrace>\<lambda>rv s. P \<longrightarrow> R rv s\<rbrace>" by (fastforce simp: validE_E_def validE_def valid_def split_def split: sum.splits)

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

lemma hoare_vcg_const_imp_lift_R:
  "(P \<Longrightarrow> \<lbrace>Q\<rbrace> m \<lbrace>R\<rbrace>,-) \<Longrightarrow> \<lbrace>\<lambda>s. P \<longrightarrow> Q s\<rbrace> m \<lbrace>\<lambda>rv s. P \<longrightarrow> R rv s\<rbrace>,-" by (fastforce simp: validE_R_def validE_def valid_def split_def split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P \<Longrightarrow> \<lbrace>Q\<rbrace> m \<lbrace>R\<rbrace>, -) \<Longrightarrow> \<lbrace>\<lambda>s. P \<longrightarrow> Q s\<rbrace> m \<lbrace>\<lambda>rv s. P \<longrightarrow> R rv s\<rbrace>, -
theory Nondet_VCG

lemma hoare_weak_lift_imp:
  "\<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. P \<longrightarrow> P' s\<rbrace> f \<lbrace>\<lambda>rv s. P \<longrightarrow> Q rv s\<rbrace>" by (auto simp add: valid_def split_def)

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

lemma hoare_weak_lift_impE:
  "\<lbrace>Q\<rbrace> m \<lbrace>R\<rbrace>,\<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. P \<longrightarrow> Q s\<rbrace> m \<lbrace>\<lambda>rv s. P \<longrightarrow> R rv s\<rbrace>,\<lbrace>\<lambda>rv s. P \<longrightarrow> E rv s\<rbrace>" by (cases P; simp add: validE_def hoare_vcg_prop)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>Q\<rbrace> m \<lbrace>R\<rbrace>, \<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. P \<longrightarrow> Q s\<rbrace> m \<lbrace>\<lambda>rv s. P \<longrightarrow> R rv s\<rbrace>, \<lbrace>\<lambda>rv s. P \<longrightarrow> E rv s\<rbrace>
theory Nondet_VCG

lemma hoare_weak_lift_imp_R:
  "\<lbrace>Q\<rbrace> m \<lbrace>R\<rbrace>,- \<Longrightarrow> \<lbrace>\<lambda>s. P \<longrightarrow> Q s\<rbrace> m \<lbrace>\<lambda>rv s. P \<longrightarrow> R rv s\<rbrace>,-" by (cases P, simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>Q\<rbrace> m \<lbrace>R\<rbrace>, - \<Longrightarrow> \<lbrace>\<lambda>s. P \<longrightarrow> Q s\<rbrace> m \<lbrace>\<lambda>rv s. P \<longrightarrow> R rv s\<rbrace>, -
theory Nondet_VCG

lemma hoare_liftP_ext:
  assumes "\<And>P x. m \<lbrace>\<lambda>s. P (f s x)\<rbrace>"
  shows "m \<lbrace>\<lambda>s. P (f s)\<rbrace>" unfolding valid_def apply clarsimp apply (erule subst[rotated, where P=P]) apply (rule ext) apply (drule use_valid, rule assms, rule refl) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (f s)\<rbrace> m \<lbrace>\<lambda>_ s. P (f s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<forall>s. P (f s) \<longrightarrow> (\<forall>(r, s')\<in>fst (m s). P (f s')) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>P (f s); (a, b) \<in> fst (m s)\<rbrakk> \<Longrightarrow> P (f b) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. (a, b) \<in> fst (m s) \<Longrightarrow> f s = f b proof (prove)
goal (1 subgoal):
 1. \<And>s a b x. (a, b) \<in> fst (m s) \<Longrightarrow> f s x = f b x proof (prove)
goal (1 subgoal):
 1. \<And>s a b x. ?t21 s a b x (f b (?x17 s a b x)) = ?t20 s a b x (f b (?x17 s a b x)) \<Longrightarrow> f s x = f b x
flex-flex pairs:
\<lambda>s a b x. ?t21 s a b x (f s (?x17 s a b x)) \<equiv>\<^sup>? \<lambda>s a b x. ?t20 s a b x (f s (?x17 s a b x)) proof (prove)
goal:
No subgoals!
theory Nondet_VCG

lemma hoare_triv:    "\<lbrace>P\<rbrace>f\<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>f\<lbrace>Q\<rbrace>" .

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

lemma hoare_trivE_R: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,- \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-" .

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, - \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, -
theory Nondet_VCG

lemma hoare_trivR_R: "\<lbrace>P\<rbrace> f -,\<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f -,\<lbrace>E\<rbrace>" .

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f -, \<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f -, \<lbrace>E\<rbrace>
theory Nondet_VCG

lemma hoare_vcg_E_conj:
  "\<lbrakk> \<lbrace>P\<rbrace> f -,\<lbrace>E\<rbrace>; \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>,\<lbrace>E'\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> P' s\<rbrace> f \<lbrace>Q'\<rbrace>, \<lbrace>\<lambda>rv s. E rv s \<and> E' rv s\<rbrace>" unfolding validE_def validE_E_def by (rule hoare_post_imp[OF _ hoare_vcg_conj_lift]; simp split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace> f -, \<lbrace>E\<rbrace>; \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>, \<lbrace>E'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> P' s\<rbrace> f \<lbrace>Q'\<rbrace>, \<lbrace>\<lambda>rv s. E rv s \<and> E' rv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> True\<rbrace>; \<lbrace>P'\<rbrace> f \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> E' e s | Inr r \<Rightarrow> Q' r s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> P' s\<rbrace> f \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> E e s \<and> E' e s | Inr r \<Rightarrow> Q' r s\<rbrace>
theory Nondet_VCG

lemma hoare_vcg_R_conj:
  "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-; \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>,- \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> P' s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>,-" unfolding validE_R_def validE_def by (rule hoare_post_imp[OF _ hoare_vcg_conj_lift]; simp split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, -; \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>, -\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> P' s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> True | Inr r \<Rightarrow> Q r s\<rbrace>; \<lbrace>P'\<rbrace> f \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> True | Inr r \<Rightarrow> Q' r s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> P' s\<rbrace> f \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> True | Inr r \<Rightarrow> Q r s \<and> Q' r s\<rbrace>
theory Nondet_VCG

lemma hoare_lift_Pf_E_R:
  "\<lbrakk> \<And>x. \<lbrace>P x\<rbrace> m \<lbrace>\<lambda>_. P x\<rbrace>, -; \<And>P. \<lbrace>\<lambda>s. P (f s)\<rbrace> m \<lbrace>\<lambda>_ s. P (f s)\<rbrace>, - \<rbrakk> \<Longrightarrow>
   \<lbrace>\<lambda>s. P (f s) s\<rbrace> m \<lbrace>\<lambda>_ s. P (f s) s\<rbrace>, -" by (fastforce simp: validE_R_def validE_def valid_def split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>x. \<lbrace>P x\<rbrace> m \<lbrace>\<lambda>_. P x\<rbrace>, -; \<And>P. \<lbrace>\<lambda>s. P (f s)\<rbrace> m \<lbrace>\<lambda>_ s. P (f s)\<rbrace>, -\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (f s) s\<rbrace> m \<lbrace>\<lambda>_ s. P (f s) s\<rbrace>, -
theory Nondet_VCG

lemma hoare_lift_Pf_E_E:
  "\<lbrakk> \<And>x. \<lbrace>P x\<rbrace> m -, \<lbrace>\<lambda>_. P x\<rbrace>; \<And>P. \<lbrace>\<lambda>s. P (f s)\<rbrace> m -, \<lbrace>\<lambda>_ s. P (f s)\<rbrace> \<rbrakk> \<Longrightarrow>
  \<lbrace>\<lambda>s. P (f s) s\<rbrace> m -, \<lbrace>\<lambda>_ s. P (f s) s\<rbrace>" by (fastforce simp: validE_E_def validE_def valid_def split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>x. \<lbrace>P x\<rbrace> m -, \<lbrace>\<lambda>_. P x\<rbrace>; \<And>P. \<lbrace>\<lambda>s. P (f s)\<rbrace> m -, \<lbrace>\<lambda>_ s. P (f s)\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P (f s) s\<rbrace> m -, \<lbrace>\<lambda>_ s. P (f s) s\<rbrace>
theory Nondet_VCG

lemma hoare_vcg_const_Ball_lift_E_E:
 "(\<And>x. x \<in> S \<Longrightarrow> \<lbrace>P x\<rbrace> f -,\<lbrace>Q x\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x \<in> S. P x s\<rbrace> f -,\<lbrace>\<lambda>rv s. \<forall>x \<in> S. Q x rv s\<rbrace>" unfolding validE_E_def validE_def valid_def by (fastforce split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. x \<in> S \<Longrightarrow> \<lbrace>P x\<rbrace> f -, \<lbrace>Q x\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x\<in>S. P x s\<rbrace> f -, \<lbrace>\<lambda>rv s. \<forall>x\<in>S. Q x rv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<And>x. x \<in> S \<Longrightarrow> \<forall>s. P x s \<longrightarrow> (\<forall>(r, s')\<in>fst (f s). case r of Inl e \<Rightarrow> Q x e s' | Inr r \<Rightarrow> True)) \<Longrightarrow> \<forall>s. (\<forall>x\<in>S. P x s) \<longrightarrow> (\<forall>(r, s')\<in>fst (f s). case r of Inl e \<Rightarrow> \<forall>x\<in>S. Q x e s' | Inr r \<Rightarrow> True)
theory Nondet_VCG

lemma hoare_vcg_imp_liftE_E:
  "\<lbrakk>\<lbrace>P'\<rbrace> f -, \<lbrace>\<lambda>rv s. \<not> P rv s\<rbrace>; \<lbrace>Q'\<rbrace> f -, \<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow>
   \<lbrace>\<lambda>s. \<not> P' s \<longrightarrow> Q' s\<rbrace> f -, \<lbrace>\<lambda>rv s. P rv s \<longrightarrow> Q rv s\<rbrace>" by (auto simp add: valid_def validE_E_def validE_def split_def split: sum.splits)

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

lemma hoare_vcg_ex_liftE:
  "\<lbrakk> \<And>x. \<lbrace>P x\<rbrace> f \<lbrace>Q x\<rbrace>,\<lbrace>E\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>x. P x s\<rbrace> f \<lbrace>\<lambda>rv s. \<exists>x. Q x rv s\<rbrace>,\<lbrace>E\<rbrace>" by (fastforce simp: validE_def valid_def split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. \<lbrace>P x\<rbrace> f \<lbrace>Q x\<rbrace>, \<lbrace>E\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>x. P x s\<rbrace> f \<lbrace>\<lambda>rv s. \<exists>x. Q x rv s\<rbrace>, \<lbrace>E\<rbrace>
theory Nondet_VCG

lemma hoare_vcg_ex_liftE_E:
  "\<lbrakk> \<And>x. \<lbrace>P x\<rbrace> f -,\<lbrace>E x\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>x. P x s\<rbrace> f -,\<lbrace>\<lambda>rv s. \<exists>x. E x rv s\<rbrace>" by (fastforce simp: validE_E_def validE_def valid_def split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. \<lbrace>P x\<rbrace> f -, \<lbrace>E x\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>x. P x s\<rbrace> f -, \<lbrace>\<lambda>rv s. \<exists>x. E x rv s\<rbrace>
theory Nondet_VCG

lemma hoare_post_imp_R:
  "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>,-; \<And>rv s. Q' rv s \<Longrightarrow> Q rv s \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-" unfolding validE_R_def by (erule hoare_post_impErr)

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

lemma hoare_post_imp_E:
  "\<lbrakk> \<lbrace>P\<rbrace> f -,\<lbrace>Q'\<rbrace>; \<And>rv s. Q' rv s \<Longrightarrow> Q rv s \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f -,\<lbrace>Q\<rbrace>" unfolding validE_E_def by (rule hoare_post_impErr)

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

lemma hoare_post_comb_imp_conj:
  "\<lbrakk> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>; \<And>s. P s \<Longrightarrow> P' s \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>" by (wpsimp wp: hoare_vcg_conj_lift)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>; \<And>s. P s \<Longrightarrow> P' s\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>
theory Nondet_VCG

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

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

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

lemma hoare_vcg_disj_lift_R:
  assumes x: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-"
  assumes y: "\<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>,-"
  shows      "\<lbrace>\<lambda>s. P s \<or> P' s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<or> Q' rv s\<rbrace>,-" using assms by (fastforce simp: validE_R_def validE_def valid_def split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P s \<or> P' s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<or> Q' rv s\<rbrace>, - proof (prove)
using this:
\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, -
\<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>, -

goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P s \<or> P' s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<or> Q' rv s\<rbrace>, -
theory Nondet_VCG

lemma hoare_vcg_all_liftE:
  "\<lbrakk> \<And>x. \<lbrace>P x\<rbrace> f \<lbrace>Q x\<rbrace>,\<lbrace>E\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x. P x s\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x. Q x rv s\<rbrace>,\<lbrace>E\<rbrace>" by (fastforce simp: validE_def valid_def split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. \<lbrace>P x\<rbrace> f \<lbrace>Q x\<rbrace>, \<lbrace>E\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x. P x s\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x. Q x rv s\<rbrace>, \<lbrace>E\<rbrace>
theory Nondet_VCG

lemma hoare_vcg_const_Ball_liftE:
  "\<lbrakk> \<And>x. x \<in> S \<Longrightarrow> \<lbrace>P x\<rbrace> f \<lbrace>Q x\<rbrace>,\<lbrace>E\<rbrace>; \<lbrace>\<lambda>s. True\<rbrace> f \<lbrace>\<lambda>r s. True\<rbrace>, \<lbrace>E\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x\<in>S. P x s\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x\<in>S. Q x rv s\<rbrace>,\<lbrace>E\<rbrace>" by (fastforce simp: validE_def valid_def split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>x. x \<in> S \<Longrightarrow> \<lbrace>P x\<rbrace> f \<lbrace>Q x\<rbrace>, \<lbrace>E\<rbrace>; \<lbrace>\<lambda>s. True\<rbrace> f \<lbrace>\<lambda>r s. True\<rbrace>, \<lbrace>E\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x\<in>S. P x s\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x\<in>S. Q x rv s\<rbrace>, \<lbrace>E\<rbrace>
theory Nondet_VCG

lemma hoare_vcg_split_lift[wp]:
  "\<lbrace>P\<rbrace> f x y \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> case (x, y) of (a, b) \<Rightarrow> f a b \<lbrace>Q\<rbrace>" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f x y \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> case (x, y) of (a, b) \<Rightarrow> f a b \<lbrace>Q\<rbrace>
theory Nondet_VCG

lemma fail_wp:
  "\<lbrace>\<top>\<rbrace> fail \<lbrace>Q\<rbrace>" by (simp add: valid_def fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> fail \<lbrace>Q\<rbrace>
theory Nondet_VCG

lemma return_wp:
  "\<lbrace>P x\<rbrace> return x \<lbrace>P\<rbrace>" by(simp add: valid_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P x\<rbrace> return x \<lbrace>P\<rbrace>
theory Nondet_VCG

lemma get_wp:
  "\<lbrace>\<lambda>s. P s s\<rbrace> get \<lbrace>P\<rbrace>" by (simp add: valid_def get_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P s s\<rbrace> get \<lbrace>P\<rbrace>
theory Nondet_VCG

lemma gets_wp:
  "\<lbrace>\<lambda>s. P (f s) s\<rbrace> gets f \<lbrace>P\<rbrace>" by(simp add: valid_def split_def gets_def return_def get_def bind_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (f s) s\<rbrace> gets f \<lbrace>P\<rbrace>
theory Nondet_VCG

lemma put_wp:
  "\<lbrace>\<lambda>_. Q () s\<rbrace> put s \<lbrace>Q\<rbrace>" by (simp add: put_def valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. Q () s\<rbrace> put s \<lbrace>Q\<rbrace>
theory Nondet_VCG

lemma modify_wp:
  "\<lbrace>\<lambda>s. Q () (f s)\<rbrace> modify f \<lbrace>Q\<rbrace>" unfolding modify_def by (wp put_wp get_wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. Q () (f s)\<rbrace> modify f \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. Q () (f s)\<rbrace> do s <- get;
put (f s)
od \<lbrace>Q\<rbrace>
theory Nondet_VCG

lemma failE_wp:
  "\<lbrace>\<top>\<rbrace> fail \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>" by (simp add: validE_def fail_wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> fail \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>
theory Nondet_VCG

lemma returnOk_wp:
  "\<lbrace>P x\<rbrace> returnOk x \<lbrace>P\<rbrace>,\<lbrace>E\<rbrace>" by (simp add: validE_def2 returnOk_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P x\<rbrace> returnOk x \<lbrace>P\<rbrace>, \<lbrace>E\<rbrace>
theory Nondet_VCG

lemma returnOKE_R_wp:
  "\<lbrace>P x\<rbrace> returnOk x \<lbrace>P\<rbrace>, -" by (simp add: validE_R_def validE_def valid_def returnOk_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P x\<rbrace> returnOk x \<lbrace>P\<rbrace>, -
theory Nondet_VCG

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

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