kings-crown/FVELER_Isabelle huggingface dataset:
theory Nondet_VCG

lemma catch_wp:
  "\<lbrakk> \<And>x. \<lbrace>E x\<rbrace> handler x \<lbrace>Q\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> catch f handler \<lbrace>Q\<rbrace>" unfolding catch_def valid_def validE_def return_def by (fastforce simp: bind_def split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>x. \<lbrace>E x\<rbrace> handler x \<lbrace>Q\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f <catch> handler \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>x. \<forall>s. E x s \<longrightarrow> (\<forall>(r, s')\<in>fst (handler x s). Q r s'); \<forall>s. P s \<longrightarrow> (\<forall>(r, s')\<in>fst (f s). case r of Inl e \<Rightarrow> E e s' | Inr r \<Rightarrow> Q r s')\<rbrakk> \<Longrightarrow> \<forall>s. P s \<longrightarrow> (\<forall>(r, s')\<in>fst ((f >>= case_sum handler (\<lambda>b s. ({(b, s)}, False))) s). Q r s')
theory Nondet_VCG

lemma handleE'_wp:
  "\<lbrakk> \<And>x. \<lbrace>F x\<rbrace> handler x \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>F\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f <handle2> handler \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" unfolding handleE'_def valid_def validE_def return_def by (fastforce simp: bind_def split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>x. \<lbrace>F x\<rbrace> handler x \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>F\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f <handle2> handler \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>x. \<forall>s. F x s \<longrightarrow> (\<forall>(r, s')\<in>fst (handler x s). case r of Inl e \<Rightarrow> E e s' | Inr r \<Rightarrow> Q r s'); \<forall>s. P s \<longrightarrow> (\<forall>(r, s')\<in>fst (f s). case r of Inl e \<Rightarrow> F e s' | Inr r \<Rightarrow> Q r s')\<rbrakk> \<Longrightarrow> \<forall>s. P s \<longrightarrow> (\<forall>(r, s')\<in>fst ((f >>= case_sum handler (\<lambda>v' s. ({(Inr v', s)}, False))) s). case r of Inl e \<Rightarrow> E e s' | Inr r \<Rightarrow> Q r s')
theory Nondet_VCG

lemma liftM_wp:
  "\<lbrace>P\<rbrace> m \<lbrace>Q \<circ> f\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> liftM f m \<lbrace>Q\<rbrace>" by (simp add: hoare_liftM_subst)

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

lemma liftME_wp:
  "\<lbrace>P\<rbrace> m \<lbrace>Q \<circ> f\<rbrace>,\<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> liftME f m \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" by (simp add: hoare_liftME_subst)

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

lemma assert_wp:
  "\<lbrace>\<lambda>s. P \<longrightarrow> Q () s\<rbrace> assert P \<lbrace>Q\<rbrace>" unfolding assert_def by (wpsimp wp: return_wp fail_wp | rule conjI)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P \<longrightarrow> Q () s\<rbrace> assert P \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P \<longrightarrow> Q () s\<rbrace> if P then return () else fail \<lbrace>Q\<rbrace>
theory Nondet_VCG

lemma list_cases_wp:
  assumes a: "\<lbrace>P_A\<rbrace> a \<lbrace>Q\<rbrace>"
  assumes b: "\<And>x xs. ts = x#xs \<Longrightarrow> \<lbrace>P_B x xs\<rbrace> b x xs \<lbrace>Q\<rbrace>"
  shows "\<lbrace>case_list P_A P_B ts\<rbrace> case ts of [] \<Rightarrow> a | x # xs \<Rightarrow> b x xs \<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> case ts of [] \<Rightarrow> a | x # xs \<Rightarrow> b x xs \<lbrace>Q\<rbrace>
theory Nondet_VCG

lemma alternative_wp:
  assumes x: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>"
  assumes y: "\<lbrace>P'\<rbrace> f' \<lbrace>Q\<rbrace>"
  shows      "\<lbrace>P and P'\<rbrace> f \<sqinter> f' \<lbrace>Q\<rbrace>" unfolding valid_def alternative_def using post_by_hoare[OF x] post_by_hoare[OF y] by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P and P'\<rbrace> f \<sqinter> f' \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<forall>s. (P and P') s \<longrightarrow> (\<forall>(r, s')\<in>fst (fst (f s) \<union> fst (f' s), snd (f s) \<or> snd (f' s)). Q r s') proof (prove)
using this:
\<lbrakk>P ?s; (?r, ?s') \<in> fst (f ?s)\<rbrakk> \<Longrightarrow> Q ?r ?s'
\<lbrakk>P' ?s; (?r, ?s') \<in> fst (f' ?s)\<rbrakk> \<Longrightarrow> Q ?r ?s'

goal (1 subgoal):
 1. \<forall>s. (P and P') s \<longrightarrow> (\<forall>(r, s')\<in>fst (fst (f s) \<union> fst (f' s), snd (f s) \<or> snd (f' s)). Q r s')
theory Nondet_VCG

lemma alternativeE_wp:
  assumes "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
  assumes "\<lbrace>P'\<rbrace> f' \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
  shows   "\<lbrace>P and P'\<rbrace> f \<sqinter> f' \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" unfolding validE_def by (wpsimp wp: assms alternative_wp | fold validE_def)+

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

lemma alternativeE_R_wp:
  "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-; \<lbrace>P'\<rbrace> f' \<lbrace>Q\<rbrace>,- \<rbrakk> \<Longrightarrow> \<lbrace>P and P'\<rbrace> f \<sqinter> f' \<lbrace>Q\<rbrace>,-" unfolding validE_R_def by (rule alternativeE_wp)

(* 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>P and P'\<rbrace> f \<sqinter> f' \<lbrace>Q\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>; \<lbrace>P'\<rbrace> f' \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P and P'\<rbrace> f \<sqinter> f' \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
theory Nondet_VCG

lemma alternativeE_E_wp:
  "\<lbrakk> \<lbrace>P\<rbrace> f -,\<lbrace>Q\<rbrace>; \<lbrace>P'\<rbrace> g -,\<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P and P'\<rbrace> f \<sqinter> g -, \<lbrace>Q\<rbrace>" unfolding validE_E_def by (rule alternativeE_wp)

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

lemma select_wp:
  "\<lbrace>\<lambda>s. \<forall>x \<in> S. Q x s\<rbrace> select S \<lbrace>Q\<rbrace>" by (simp add: select_def valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>x\<in>S. Q x s\<rbrace> select S \<lbrace>Q\<rbrace>
theory Nondet_VCG

lemma select_f_wp:
  "\<lbrace>\<lambda>s. \<forall>x\<in>fst S. Q x s\<rbrace> select_f S \<lbrace>Q\<rbrace>" by (simp add: select_f_def valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>x\<in>fst S. Q x s\<rbrace> select_f S \<lbrace>Q\<rbrace>
theory Nondet_VCG

lemma state_select_wp:
  "\<lbrace>\<lambda>s. \<forall>t. (s, t) \<in> f \<longrightarrow> P () t\<rbrace> state_select f \<lbrace>P\<rbrace>" unfolding state_select_def2 by (wpsimp wp: put_wp select_wp return_wp get_wp assert_wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>t. (s, t) \<in> f \<longrightarrow> P () t\<rbrace> state_select f \<lbrace>P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>t. (s, t) \<in> f \<longrightarrow> P () t\<rbrace> do s <- get;
S <- return {s'. (s, s') \<in> f};
assert (S \<noteq> {});
select S >>= put
od \<lbrace>P\<rbrace>
theory Nondet_VCG

lemma condition_wp:
  "\<lbrakk> \<lbrace>Q\<rbrace> A \<lbrace>P\<rbrace>;  \<lbrace>R\<rbrace> B \<lbrace>P\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. if C s then Q s else R s\<rbrace> condition C A B \<lbrace>P\<rbrace>" by (clarsimp simp: condition_def valid_def)

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

lemma conditionE_wp:
  "\<lbrakk> \<lbrace>P\<rbrace> A \<lbrace>Q\<rbrace>,\<lbrace>R\<rbrace>; \<lbrace>P'\<rbrace> B \<lbrace>Q\<rbrace>,\<lbrace>R\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. if C s then P s else P' s\<rbrace> condition C A B \<lbrace>Q\<rbrace>,\<lbrace>R\<rbrace>" by (clarsimp simp: condition_def validE_def valid_def)

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

lemma state_assert_wp:
  "\<lbrace>\<lambda>s. f s \<longrightarrow> P () s\<rbrace> state_assert f \<lbrace>P\<rbrace>" unfolding state_assert_def by (wp seq_ext get_wp assert_wp)

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

lemma when_wp[wp_split]:
  "\<lbrakk> P \<Longrightarrow> \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>if P then Q else R ()\<rbrace> when P f \<lbrace>R\<rbrace>" by (clarsimp simp: when_def valid_def return_def)

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

lemma unless_wp[wp_split]:
  "(\<not>P \<Longrightarrow> \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>) \<Longrightarrow> \<lbrace>if P then R () else Q\<rbrace> unless P f \<lbrace>R\<rbrace>" unfolding unless_def by wp auto

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

lemma whenE_wp:
  "(P \<Longrightarrow> \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>, \<lbrace>E\<rbrace>) \<Longrightarrow> \<lbrace>if P then Q else R ()\<rbrace> whenE P f \<lbrace>R\<rbrace>, \<lbrace>E\<rbrace>" unfolding whenE_def by clarsimp (wp returnOk_wp)

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

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

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

lemma maybeM_wp:
  "(\<And>x. y = Some x \<Longrightarrow> \<lbrace>P x\<rbrace> m x \<lbrace>Q\<rbrace>) \<Longrightarrow>
   \<lbrace>\<lambda>s. (\<forall>x. y = Some x \<longrightarrow> P x s) \<and> (y = None \<longrightarrow> Q () s)\<rbrace> maybeM m y \<lbrace>Q\<rbrace>" unfolding maybeM_def by (wpsimp wp: return_wp) auto

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

lemma notM_wp:
  "\<lbrace>P\<rbrace> m \<lbrace>\<lambda>c. Q (\<not> c)\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> notM m \<lbrace>Q\<rbrace>" unfolding notM_def by (wpsimp wp: return_wp)

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

lemma ifM_wp:
  assumes [wp]: "\<lbrace>Q\<rbrace> f \<lbrace>S\<rbrace>" "\<lbrace>R\<rbrace> g \<lbrace>S\<rbrace>"
  assumes [wp]: "\<lbrace>A\<rbrace> P \<lbrace>\<lambda>c s. c \<longrightarrow> Q s\<rbrace>" "\<lbrace>B\<rbrace> P \<lbrace>\<lambda>c s. \<not>c \<longrightarrow> R s\<rbrace>"
  shows "\<lbrace>A and B\<rbrace> ifM P f g \<lbrace>S\<rbrace>" unfolding ifM_def by (wpsimp wp: hoare_vcg_if_split hoare_vcg_conj_lift)

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

lemma andM_wp:
  assumes [wp]: "\<lbrace>Q'\<rbrace> B \<lbrace>Q\<rbrace>"
  assumes [wp]: "\<lbrace>P\<rbrace> A \<lbrace>\<lambda>c s. c \<longrightarrow> Q' s\<rbrace>" "\<lbrace>P'\<rbrace> A \<lbrace>\<lambda>c s. \<not> c \<longrightarrow> Q False s\<rbrace>"
  shows "\<lbrace>P and P'\<rbrace> andM A B \<lbrace>Q\<rbrace>" unfolding andM_def by (wp ifM_wp return_wp)

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

lemma orM_wp:
  assumes [wp]: "\<lbrace>Q'\<rbrace> B \<lbrace>Q\<rbrace>"
  assumes [wp]: "\<lbrace>P\<rbrace> A \<lbrace>\<lambda>c s. c \<longrightarrow> Q True s\<rbrace>" "\<lbrace>P'\<rbrace> A \<lbrace>\<lambda>c s. \<not> c \<longrightarrow> Q' s\<rbrace>"
  shows "\<lbrace>P and P'\<rbrace> orM A B \<lbrace>Q\<rbrace>" unfolding orM_def by (wp ifM_wp return_wp)

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

lemma whenM_wp:
  assumes [wp]: "\<lbrace>Q\<rbrace> f \<lbrace>S\<rbrace>"
  assumes [wp]: "\<lbrace>A\<rbrace> P \<lbrace>\<lambda>c s. c \<longrightarrow> Q s\<rbrace>" "\<lbrace>B\<rbrace> P \<lbrace>\<lambda>c s. \<not>c \<longrightarrow> S () s\<rbrace>"
  shows "\<lbrace>A and B\<rbrace> whenM P f \<lbrace>S\<rbrace>" unfolding whenM_def by (wp ifM_wp return_wp)

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

lemma hoare_K_bind[wp_split]:
  "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> K_bind f x \<lbrace>Q\<rbrace>" by simp

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

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

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

lemma hoare_fun_app_wp:
  "\<lbrace>P\<rbrace> f' x \<lbrace>Q'\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f' $ x \<lbrace>Q'\<rbrace>"
  "\<lbrace>P\<rbrace> f x \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f $ x \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
  "\<lbrace>P\<rbrace> f x \<lbrace>Q\<rbrace>,- \<Longrightarrow> \<lbrace>P\<rbrace> f $ x \<lbrace>Q\<rbrace>,-"
  "\<lbrace>P\<rbrace> f x -,\<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f $ x -,\<lbrace>E\<rbrace>" by simp+

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

lemma liftE_validE_E:
  "\<lbrace>\<top>\<rbrace> liftE f -, \<lbrace>Q\<rbrace>" by (clarsimp simp: validE_E_def valid_def)

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

lemma returnOk_E:
  "\<lbrace>\<top>\<rbrace> returnOk r -, \<lbrace>Q\<rbrace>" by (simp add: validE_E_def) (wp returnOk_wp)

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

lemma case_option_wp:
  "\<lbrakk> \<And>x. \<lbrace>P x\<rbrace> m x \<lbrace>Q\<rbrace>; \<lbrace>P'\<rbrace> m' \<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow>
   \<lbrace>\<lambda>s. (x = None \<longrightarrow> P' s) \<and> (x \<noteq> None \<longrightarrow> P (the x) s)\<rbrace> case_option m' m x \<lbrace>Q\<rbrace>" by (cases x; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>x. \<lbrace>P x\<rbrace> m x \<lbrace>Q\<rbrace>; \<lbrace>P'\<rbrace> m' \<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (x = None \<longrightarrow> P' s) \<and> (x \<noteq> None \<longrightarrow> P (the x) s)\<rbrace> case x of None \<Rightarrow> m' | Some x \<Rightarrow> m x \<lbrace>Q\<rbrace>
theory Nondet_VCG

lemma case_option_wpE:
  "\<lbrakk> \<And>x. \<lbrace>P x\<rbrace> m x \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>; \<lbrace>P'\<rbrace> m' \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> \<rbrakk> \<Longrightarrow>
   \<lbrace>\<lambda>s. (x = None \<longrightarrow> P' s) \<and> (x \<noteq> None \<longrightarrow> P (the x) s)\<rbrace> case_option m' m x \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" by (cases x; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>x. \<lbrace>P x\<rbrace> m x \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>; \<lbrace>P'\<rbrace> m' \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (x = None \<longrightarrow> P' s) \<and> (x \<noteq> None \<longrightarrow> P (the x) s)\<rbrace> case x of None \<Rightarrow> m' | Some x \<Rightarrow> m x \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>
theory Nondet_VCG

lemma assert_opt_wp:
  "\<lbrace>\<lambda>s. x \<noteq> None \<longrightarrow> Q (the x) s\<rbrace> assert_opt x \<lbrace>Q\<rbrace>" unfolding assert_opt_def by (cases x; wpsimp wp: fail_wp return_wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. x \<noteq> None \<longrightarrow> Q (the x) s\<rbrace> assert_opt x \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. x \<noteq> None \<longrightarrow> Q (the x) s\<rbrace> case x of None \<Rightarrow> fail | Some v \<Rightarrow> return v \<lbrace>Q\<rbrace>
theory Nondet_VCG

lemma gets_the_wp:
  "\<lbrace>\<lambda>s. (f s \<noteq> None) \<longrightarrow> Q (the (f s)) s\<rbrace> gets_the f \<lbrace>Q\<rbrace>" unfolding gets_the_def by (wp seq_ext gets_wp assert_opt_wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. f s \<noteq> None \<longrightarrow> Q (the (f s)) s\<rbrace> gets_the f \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. f s \<noteq> None \<longrightarrow> Q (the (f s)) s\<rbrace> gets f >>= assert_opt \<lbrace>Q\<rbrace>
theory Nondet_VCG

lemma gets_the_wp': (* FIXME: should prefer this one in [wp] *)
  "\<lbrace>\<lambda>s. \<forall>rv. f s = Some rv \<longrightarrow> Q rv s\<rbrace> gets_the f \<lbrace>Q\<rbrace>" unfolding gets_the_def by (wpsimp wp: seq_ext gets_wp assert_opt_wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>rv. f s = Some rv \<longrightarrow> Q rv s\<rbrace> gets_the f \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>rv. f s = Some rv \<longrightarrow> Q rv s\<rbrace> gets f >>= assert_opt \<lbrace>Q\<rbrace>
theory Nondet_VCG

lemma gets_map_wp':
  "\<lbrace>\<lambda>s. \<forall>rv. f s p = Some rv \<longrightarrow> Q rv s\<rbrace> gets_map f p \<lbrace>Q\<rbrace>" unfolding gets_map_def by (wpsimp wp: seq_ext gets_wp assert_opt_wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>rv. f s p = Some rv \<longrightarrow> Q rv s\<rbrace> gets_map f p \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>rv. f s p = Some rv \<longrightarrow> Q rv s\<rbrace> do m <- gets f;
assert_opt (m p)
od \<lbrace>Q\<rbrace>