kings-crown/FVELER_Isabelle huggingface dataset:
theory Nondet_More_VCG

lemma hoare_in_monad_post:
  assumes x: "\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>x. P\<rbrace>"
  shows      "\<lbrace>\<top>\<rbrace> f \<lbrace>\<lambda>rv s. (rv, s) \<in> fst (f s)\<rbrace>" apply (clarsimp simp: valid_def) apply (rule back_subst[where P="\<lambda>s. x\<in>fst (f s)" for x], assumption) apply (simp add: state_unchanged[OF x]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> f \<lbrace>\<lambda>rv s. (rv, s) \<in> fst (f s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. (a, b) \<in> fst (f s) \<Longrightarrow> (a, b) \<in> fst (f b) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. (a, b) \<in> fst (f s) \<Longrightarrow> s = b proof (prove)
goal:
No subgoals!
theory Nondet_More_VCG

lemma list_case_throw_validE_R:
  "\<lbrakk> \<And>y ys. xs = y # ys \<Longrightarrow> \<lbrace>P\<rbrace> f y ys \<lbrace>Q\<rbrace>,- \<rbrakk> \<Longrightarrow>
   \<lbrace>P\<rbrace> case xs of [] \<Rightarrow> throwError e | x # xs \<Rightarrow> f x xs \<lbrace>Q\<rbrace>,-" apply (cases xs, simp_all) apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>y ys. xs = y # ys \<Longrightarrow> \<lbrace>P\<rbrace> f y ys \<lbrace>Q\<rbrace>, -) \<Longrightarrow> \<lbrace>P\<rbrace> case xs of [] \<Rightarrow> throwError e | x # xs \<Rightarrow> f x xs \<lbrace>Q\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. xs = [] \<Longrightarrow> \<lbrace>P\<rbrace> throwError e \<lbrace>Q\<rbrace>, - proof (prove)
goal:
No subgoals!
theory Nondet_More_VCG

lemma validE_R_sp:
  assumes x: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-"
  assumes y: "\<And>x. \<lbrace>Q x\<rbrace> g x \<lbrace>R\<rbrace>,-"
  shows "\<lbrace>P\<rbrace> f >>=E (\<lambda>x. g x) \<lbrace>R\<rbrace>,-" by (rule hoare_pre, wp x y, simp)

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

lemma valid_set_take_helper:
  "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x \<in> set (xs rv s). Q x rv s\<rbrace>
   \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x \<in> set (take (n rv s) (xs rv s)). Q x rv s\<rbrace>" apply (erule hoare_strengthen_post) apply (clarsimp dest!: in_set_takeD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x\<in>set (xs rv s). Q x rv s\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x\<in>set (take (n rv s) (xs rv s)). Q x rv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>rv s. \<forall>x\<in>set (xs rv s). Q x rv s \<Longrightarrow> \<forall>x\<in>set (take (n rv s) (xs rv s)). Q x rv s proof (prove)
goal:
No subgoals!
theory Nondet_More_VCG

lemma whenE_throwError_sp:
  "\<lbrace>P\<rbrace> whenE Q (throwError e) \<lbrace>\<lambda>rv s. \<not> Q \<and> P s\<rbrace>, -" apply (simp add: whenE_def validE_R_def) apply (intro conjI impI; wp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> whenE Q (throwError e) \<lbrace>\<lambda>rv s. \<not> Q \<and> P s\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. (Q \<longrightarrow> \<lbrace>P\<rbrace> throwError e \<lbrace>\<lambda>rv s. False\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>) \<and> (\<not> Q \<longrightarrow> \<lbrace>P\<rbrace> returnOk () \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>) proof (prove)
goal:
No subgoals!
theory Nondet_More_VCG

lemma weaker_hoare_ifE:
  assumes x: "\<lbrace>P \<rbrace> a \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
  assumes y: "\<lbrace>P'\<rbrace> b \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
  shows      "\<lbrace>P and P'\<rbrace> if test then a else b \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" apply (rule hoare_vcg_precond_impE) apply (wp x y) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P and P'\<rbrace> if test then a else b \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> if test then a else b \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>
 2. \<And>s. (P and P') s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (P and P') s \<Longrightarrow> (test \<longrightarrow> P s) \<and> (\<not> test \<longrightarrow> P' s) proof (prove)
goal:
No subgoals!
theory Nondet_More_VCG

lemma wp_split_const_if:
  assumes x: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>"
  assumes y: "\<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>"
  shows "\<lbrace>\<lambda>s. (G \<longrightarrow> P s) \<and> (\<not> G \<longrightarrow> P' s)\<rbrace> f \<lbrace>\<lambda>rv s. (G \<longrightarrow> Q rv s) \<and> (\<not> G \<longrightarrow> Q' rv s)\<rbrace>" by (cases G; simp add: x y)

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

lemma wp_split_const_if_R:
  assumes x: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-"
  assumes y: "\<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>,-"
  shows "\<lbrace>\<lambda>s. (G \<longrightarrow> P s) \<and> (\<not> G \<longrightarrow> P' s)\<rbrace> f \<lbrace>\<lambda>rv s. (G \<longrightarrow> Q rv s) \<and> (\<not> G \<longrightarrow> Q' rv s)\<rbrace>,-" by (cases G; simp add: x y)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (G \<longrightarrow> P s) \<and> (\<not> G \<longrightarrow> P' s)\<rbrace> f \<lbrace>\<lambda>rv s. (G \<longrightarrow> Q rv s) \<and> (\<not> G \<longrightarrow> Q' rv s)\<rbrace>, -
theory Nondet_More_VCG

lemma hoare_grab_asm:
  "\<lbrakk> G \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. G \<and> P s\<rbrace> f \<lbrace>Q\<rbrace>" by (cases G, simp+)

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

lemma hoare_grab_asm2:
  "\<lbrakk>P' \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> R s\<rbrace> f \<lbrace>Q\<rbrace>\<rbrakk>
   \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> P' \<and> R s\<rbrace> f \<lbrace>Q\<rbrace>" by (fastforce simp: valid_def)

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

lemma hoare_grab_exs:
  assumes x: "\<And>x. P x \<Longrightarrow> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>"
  shows      "\<lbrace>\<lambda>s. \<exists>x. P x \<and> P' s\<rbrace> f \<lbrace>Q\<rbrace>" apply (clarsimp simp: valid_def) apply (erule(2) use_valid [OF _ x]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<exists>x. P x \<and> P' s\<rbrace> f \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b x. \<lbrakk>(a, b) \<in> fst (f s); P' s; P x\<rbrakk> \<Longrightarrow> Q a b proof (prove)
goal:
No subgoals!
theory Nondet_More_VCG

lemma hoare_prop_E: "\<lbrace>\<lambda>rv. P\<rbrace> f -,\<lbrace>\<lambda>rv s. P\<rbrace>" unfolding validE_E_def by (rule hoare_pre, wp, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>rv. P\<rbrace> f -, \<lbrace>\<lambda>rv s. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>rv. P\<rbrace> f \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>rv s. P\<rbrace>
theory Nondet_More_VCG

lemma hoare_walk_assmsE:
  assumes x: "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv. P\<rbrace>" and y: "\<And>s. P s \<Longrightarrow> Q s" and z: "\<lbrace>P\<rbrace> g \<lbrace>\<lambda>rv. Q\<rbrace>"
  shows      "\<lbrace>P\<rbrace> doE x \<leftarrow> f; g odE \<lbrace>\<lambda>rv. Q\<rbrace>" apply (wp z) apply (simp add: validE_def) apply (rule hoare_strengthen_post [OF x]) apply (auto simp: y split: sum.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> doE x <- f;
g
odE \<lbrace>\<lambda>rv. Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> f \<lbrace>\<lambda>x s. P s \<and> P s\<rbrace>, \<lbrace>\<lambda>rv. Q\<rbrace>
 2. \<And>s. P s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> f \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> Q s | Inr r \<Rightarrow> P s\<rbrace>
 2. \<And>s. P s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>rv s. P s \<Longrightarrow> case rv of Inl e \<Rightarrow> Q s | Inr r \<Rightarrow> P s
 2. \<And>s. P s \<Longrightarrow> P s proof (prove)
goal:
No subgoals!
theory Nondet_More_VCG

lemma univ_wp:
  "\<lbrace>\<lambda>s. \<forall>(rv, s') \<in> fst (f s). Q rv s'\<rbrace> f \<lbrace>Q\<rbrace>" by (simp add: valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>(rv, s')\<in>fst (f s). Q rv s'\<rbrace> f \<lbrace>Q\<rbrace>
theory Nondet_More_VCG

lemma univ_get_wp:
  assumes x: "\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv. P\<rbrace>"
  shows "\<lbrace>\<lambda>s. \<forall>(rv, s') \<in> fst (f s). s = s' \<longrightarrow> Q rv s'\<rbrace> f \<lbrace>Q\<rbrace>" apply (rule hoare_pre_imp[OF _ univ_wp]) apply clarsimp apply (drule bspec, assumption, simp) apply (drule mp) apply (simp add: state_unchanged[OF x]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>(rv, s')\<in>fst (f s). s = s' \<longrightarrow> Q rv s'\<rbrace> f \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<forall>(rv, s')\<in>fst (f s). s = s' \<longrightarrow> Q rv s' \<Longrightarrow> \<forall>(rv, s')\<in>fst (f s). Q rv s' proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<forall>x\<in>fst (f s). case x of (rv, s') \<Rightarrow> s = s' \<longrightarrow> Q rv s'; (a, b) \<in> fst (f s)\<rbrakk> \<Longrightarrow> Q a b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); s = b \<longrightarrow> Q a b\<rbrakk> \<Longrightarrow> Q a b proof (prove)
goal (2 subgoals):
 1. \<And>s a b. (a, b) \<in> fst (f s) \<Longrightarrow> s = b
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); Q a b\<rbrakk> \<Longrightarrow> Q a b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); Q a b\<rbrakk> \<Longrightarrow> Q a b proof (prove)
goal:
No subgoals!
theory Nondet_More_VCG

lemma weak_if_wp:
  "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace> \<rbrakk> \<Longrightarrow>
   \<lbrace>P and P'\<rbrace> f \<lbrace>\<lambda>r. if C r then Q r else Q' r\<rbrace>" by (auto simp add: valid_def split_def)

(* 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 \<lbrace>\<lambda>r. if C r then Q r else Q' r\<rbrace>
theory Nondet_More_VCG

lemma bindE_split_recursive_asm:
  assumes x: "\<And>x s'. \<lbrakk> (Inr x, s') \<in> fst (f s) \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. B x s \<and> s = s'\<rbrace> g x \<lbrace>C\<rbrace>, \<lbrace>E\<rbrace>"
  shows      "\<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>, \<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>st. A st \<and> st = s\<rbrace> f >>=E g \<lbrace>C\<rbrace>, \<lbrace>E\<rbrace>" apply (clarsimp simp: validE_def valid_def bindE_def in_bind lift_def) apply (erule allE, erule(1) impE) apply (drule(1) bspec, simp) apply (clarsimp simp: in_throwError split: sum.splits) apply (drule x) apply (clarsimp simp: validE_def valid_def) apply (drule(1) bspec, simp split: sum.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>, \<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>st. A st \<and> st = s\<rbrace> f >>=E g \<lbrace>C\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a b s'' x. \<lbrakk>\<forall>s. A s \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (Inl e, s') \<Rightarrow> E e s' | (Inr ra, s') \<Rightarrow> B ra s'); A s; (x, s'') \<in> fst (f s); (a, b) \<in> fst ((case x of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> g v') s'')\<rbrakk> \<Longrightarrow> case a of Inl e \<Rightarrow> E e b | Inr r \<Rightarrow> C r b proof (prove)
goal (1 subgoal):
 1. \<And>a b s'' x. \<lbrakk>A s; (x, s'') \<in> fst (f s); (a, b) \<in> fst ((case x of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> g v') s''); \<forall>x\<in>fst (f s). case x of (Inl e, s') \<Rightarrow> E e s' | (Inr ra, s') \<Rightarrow> B ra s'\<rbrakk> \<Longrightarrow> case a of Inl e \<Rightarrow> E e b | Inr r \<Rightarrow> C r b proof (prove)
goal (1 subgoal):
 1. \<And>a b s'' x. \<lbrakk>A s; (x, s'') \<in> fst (f s); (a, b) \<in> fst ((case x of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> g v') s''); case x of Inl e \<Rightarrow> E e s'' | Inr r \<Rightarrow> B r s''\<rbrakk> \<Longrightarrow> case a of Inl e \<Rightarrow> E e b | Inr r \<Rightarrow> C r b proof (prove)
goal (1 subgoal):
 1. \<And>a b s'' x2. \<lbrakk>B x2 s''; A s; (Inr x2, s'') \<in> fst (f s); (a, b) \<in> fst (g x2 s'')\<rbrakk> \<Longrightarrow> (\<forall>x1. a = Inl x1 \<longrightarrow> E x1 b) \<and> (\<forall>x2. a = Inr x2 \<longrightarrow> C x2 b) proof (prove)
goal (1 subgoal):
 1. \<And>a b s'' x2. \<lbrakk>B x2 s''; A s; (a, b) \<in> fst (g x2 s''); \<lbrace>\<lambda>s. B x2 s \<and> s = s''\<rbrace> g x2 \<lbrace>C\<rbrace>, \<lbrace>E\<rbrace>\<rbrakk> \<Longrightarrow> (\<forall>x1. a = Inl x1 \<longrightarrow> E x1 b) \<and> (\<forall>x2. a = Inr x2 \<longrightarrow> C x2 b) proof (prove)
goal (1 subgoal):
 1. \<And>a b s'' x2. \<lbrakk>B x2 s''; A s; (a, b) \<in> fst (g x2 s''); \<forall>x\<in>fst (g x2 s''). case x of (Inl e, s') \<Rightarrow> E e s' | (Inr ra, s') \<Rightarrow> C ra s'\<rbrakk> \<Longrightarrow> (\<forall>x1. a = Inl x1 \<longrightarrow> E x1 b) \<and> (\<forall>x2. a = Inr x2 \<longrightarrow> C x2 b) proof (prove)
goal:
No subgoals!
theory Nondet_More_VCG

lemma validE_R_abstract_rv:
  "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>rv'. Q rv' s\<rbrace>,- \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-" by (erule hoare_post_imp_R, simp)

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

lemma validE_cases_valid:
  "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q (Inr rv) s\<rbrace>,\<lbrace>\<lambda>rv s. Q (Inl rv) s\<rbrace>
   \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>" apply (simp add: validE_def) apply (erule hoare_strengthen_post) apply (simp split: sum.split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv. Q (Inr rv)\<rbrace>, \<lbrace>\<lambda>rv. Q (Inl rv)\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> Q (Inl e) s | Inr r \<Rightarrow> Q (Inr r) s\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>rv s. case rv of Inl e \<Rightarrow> Q (Inl e) s | Inr r \<Rightarrow> Q (Inr r) s \<Longrightarrow> Q rv s proof (prove)
goal:
No subgoals!
theory Nondet_More_VCG

lemma liftM_pre:
  assumes rl: "\<lbrace>\<lambda>s. \<not> P s \<rbrace> a \<lbrace> \<lambda>_ _. False \<rbrace>"
  shows "\<lbrace>\<lambda>s. \<not> P s \<rbrace> liftM f a \<lbrace> \<lambda>_ _. False \<rbrace>" unfolding liftM_def apply (rule seq) apply (rule rl) apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> P s\<rbrace> liftM f a \<lbrace>\<lambda>_ _. False\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> P s\<rbrace> do x <- a;
return (f x)
od \<lbrace>\<lambda>_ _. False\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>\<lambda>s. \<not> P s\<rbrace> a \<lbrace>?B\<rbrace>
 2. \<And>x. ?P x \<Longrightarrow> \<lbrace>?C\<rbrace> return (f x) \<lbrace>\<lambda>_ _. False\<rbrace>
 3. \<And>x s. ?B x s \<Longrightarrow> ?P x \<and> ?C s proof (prove)
goal (2 subgoals):
 1. \<And>x. ?P x \<Longrightarrow> \<lbrace>?C\<rbrace> return (f x) \<lbrace>\<lambda>_ _. False\<rbrace>
 2. \<And>x s. False \<Longrightarrow> ?P x \<and> ?C s proof (prove)
goal (1 subgoal):
 1. \<And>x s. False \<Longrightarrow> ?P x \<and> False proof (prove)
goal:
No subgoals!
theory Nondet_More_VCG

lemma hoare_gen_asm':
  "(P \<Longrightarrow> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>) \<Longrightarrow> \<lbrace>P' and (\<lambda>_. P)\<rbrace> f \<lbrace>Q\<rbrace>" apply (auto intro: hoare_assume_pre) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P \<Longrightarrow> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>) \<Longrightarrow> \<lbrace>P' and (\<lambda>_. P)\<rbrace> f \<lbrace>Q\<rbrace> proof (prove)
goal:
No subgoals!
theory Nondet_More_VCG

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

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

lemma valid_rv_lift:
  "\<lbrace>P'\<rbrace> f \<lbrace>\<lambda>rv s. rv \<longrightarrow> Q rv s\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. P \<and> P' s\<rbrace> f \<lbrace>\<lambda>rv s. rv \<longrightarrow> P \<and> Q rv s\<rbrace>" by (fastforce simp: valid_def)

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

lemma valid_imp_ex:
  "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. \<exists>x. rv \<longrightarrow> Q rv s x\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. rv \<longrightarrow> (\<exists>x. Q rv s x)\<rbrace>" by (fastforce simp: valid_def)

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

lemma valid_rv_split:
  "\<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. rv \<longrightarrow> Q s\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. \<not>rv \<longrightarrow> Q' s\<rbrace>\<rbrakk>
   \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. if rv then Q s else Q' s\<rbrace>" by (fastforce simp: valid_def)

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

lemma hoare_rv_split:
  "\<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. rv \<longrightarrow> (Q rv s)\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. (\<not>rv) \<longrightarrow> (Q rv s)\<rbrace>\<rbrakk>
   \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>" apply (clarsimp simp: valid_def split_def) by (metis (full_types) fst_eqD snd_conv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. rv \<longrightarrow> Q rv s\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. \<not> rv \<longrightarrow> Q rv s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<forall>s. P s \<longrightarrow> (\<forall>x\<in>fst (f s). fst x \<longrightarrow> Q True (snd x)); \<forall>s. P s \<longrightarrow> (\<forall>x\<in>fst (f s). \<not> fst x \<longrightarrow> Q False (snd x)); P s; (a, b) \<in> fst (f s)\<rbrakk> \<Longrightarrow> Q a b
theory Nondet_More_VCG

lemma combine_validE:
  "\<lbrakk> \<lbrace> P \<rbrace> x \<lbrace> Q \<rbrace>,\<lbrace> E \<rbrace>; \<lbrace> P' \<rbrace> x \<lbrace> Q' \<rbrace>,\<lbrace> E' \<rbrace> \<rbrakk>
   \<Longrightarrow> \<lbrace> P and P' \<rbrace> x \<lbrace> \<lambda>r. (Q r) and (Q' r) \<rbrace>,\<lbrace>\<lambda>r. (E r) and (E' r) \<rbrace>" apply (clarsimp simp: validE_def valid_def split: sum.splits) apply (erule allE, erule (1) impE)+ apply (drule (1) bspec)+ apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace> x \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>; \<lbrace>P'\<rbrace> x \<lbrace>Q'\<rbrace>, \<lbrace>E'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P and P'\<rbrace> x \<lbrace>\<lambda>r. Q r and Q' r\<rbrace>, \<lbrace>\<lambda>r. E r and E' r\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<forall>s. P' s \<longrightarrow> (\<forall>x\<in>fst (x s). case x of (r, s') \<Rightarrow> (\<forall>x1. r = Inl x1 \<longrightarrow> E' x1 s') \<and> (\<forall>x2. r = Inr x2 \<longrightarrow> Q' x2 s')); \<forall>s. P s \<longrightarrow> (\<forall>x\<in>fst (x s). case x of (r, s') \<Rightarrow> (\<forall>x1. r = Inl x1 \<longrightarrow> E x1 s') \<and> (\<forall>x2. r = Inr x2 \<longrightarrow> Q x2 s')); (a, b) \<in> fst (x s); P s; P' s\<rbrakk> \<Longrightarrow> (\<forall>x1. a = Inl x1 \<longrightarrow> E x1 b \<and> E' x1 b) \<and> (\<forall>x2. a = Inr x2 \<longrightarrow> Q x2 b \<and> Q' x2 b) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (x s); P s; P' s; \<forall>x\<in>fst (x s). case x of (r, s') \<Rightarrow> (\<forall>x1. r = Inl x1 \<longrightarrow> E' x1 s') \<and> (\<forall>x2. r = Inr x2 \<longrightarrow> Q' x2 s'); \<forall>x\<in>fst (x s). case x of (r, s') \<Rightarrow> (\<forall>x1. r = Inl x1 \<longrightarrow> E x1 s') \<and> (\<forall>x2. r = Inr x2 \<longrightarrow> Q x2 s')\<rbrakk> \<Longrightarrow> (\<forall>x1. a = Inl x1 \<longrightarrow> E x1 b \<and> E' x1 b) \<and> (\<forall>x2. a = Inr x2 \<longrightarrow> Q x2 b \<and> Q' x2 b) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (x s); P s; P' s; case (a, b) of (r, s') \<Rightarrow> (\<forall>x1. r = Inl x1 \<longrightarrow> E' x1 s') \<and> (\<forall>x2. r = Inr x2 \<longrightarrow> Q' x2 s'); case (a, b) of (r, s') \<Rightarrow> (\<forall>x1. r = Inl x1 \<longrightarrow> E x1 s') \<and> (\<forall>x2. r = Inr x2 \<longrightarrow> Q x2 s')\<rbrakk> \<Longrightarrow> (\<forall>x1. a = Inl x1 \<longrightarrow> E x1 b \<and> E' x1 b) \<and> (\<forall>x2. a = Inr x2 \<longrightarrow> Q x2 b \<and> Q' x2 b) proof (prove)
goal:
No subgoals!
theory Nondet_More_VCG

lemma valid_case_prod:
  "\<lbrakk> \<And>x y. valid (P x y) (f x y) Q \<rbrakk> \<Longrightarrow> valid (case_prod P v) (case_prod (\<lambda>x y. f x y) v) Q" by (simp add: split_def)

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