kings-crown/FVELER_Isabelle huggingface dataset:
theory Nondet_More_VCG

lemma hoare_vcg_imp_lift_pre_add:
  "\<lbrakk> \<lbrace>P and Q\<rbrace> f \<lbrace>\<lambda>rv s. R rv s\<rbrace>; f \<lbrace>\<lambda>s. \<not> Q s\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q s \<longrightarrow> R rv s\<rbrace>" apply (rule hoare_weaken_pre) apply (rule hoare_vcg_imp_lift') apply fastforce apply fastforce apply (clarsimp simp: pred_conj_def valid_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P and Q\<rbrace> f \<lbrace>R\<rbrace>; \<lbrace>\<lambda>s. \<not> Q s\<rbrace> f \<lbrace>\<lambda>_ s. \<not> Q s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q s \<longrightarrow> R rv s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<lbrace>P and Q\<rbrace> f \<lbrace>R\<rbrace>; \<lbrace>\<lambda>s. \<not> Q s\<rbrace> f \<lbrace>\<lambda>_ s. \<not> Q s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?Q\<rbrace> f \<lbrace>\<lambda>rv s. Q s \<longrightarrow> R rv s\<rbrace>
 2. \<And>s. \<lbrakk>\<lbrace>P and Q\<rbrace> f \<lbrace>R\<rbrace>; \<lbrace>\<lambda>s. \<not> Q s\<rbrace> f \<lbrace>\<lambda>_ s. \<not> Q s\<rbrace>; P s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<lbrace>P and Q\<rbrace> f \<lbrace>R\<rbrace>; \<lbrace>\<lambda>s. \<not> Q s\<rbrace> f \<lbrace>\<lambda>_ s. \<not> Q s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?P'3\<rbrace> f \<lbrace>\<lambda>rv s. \<not> Q s\<rbrace>
 2. \<lbrakk>\<lbrace>P and Q\<rbrace> f \<lbrace>R\<rbrace>; \<lbrace>\<lambda>s. \<not> Q s\<rbrace> f \<lbrace>\<lambda>_ s. \<not> Q s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?Q'3\<rbrace> f \<lbrace>R\<rbrace>
 3. \<And>s. \<lbrakk>\<lbrace>P and Q\<rbrace> f \<lbrace>R\<rbrace>; \<lbrace>\<lambda>s. \<not> Q s\<rbrace> f \<lbrace>\<lambda>_ s. \<not> Q s\<rbrace>; P s\<rbrakk> \<Longrightarrow> \<not> ?P'3 s \<longrightarrow> ?Q'3 s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<lbrace>P and Q\<rbrace> f \<lbrace>R\<rbrace>; \<lbrace>\<lambda>s. \<not> Q s\<rbrace> f \<lbrace>\<lambda>_ s. \<not> Q s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?Q'3\<rbrace> f \<lbrace>R\<rbrace>
 2. \<And>s. \<lbrakk>\<lbrace>P and Q\<rbrace> f \<lbrace>R\<rbrace>; \<lbrace>\<lambda>s. \<not> Q s\<rbrace> f \<lbrace>\<lambda>_ s. \<not> Q s\<rbrace>; P s\<rbrakk> \<Longrightarrow> \<not> \<not> Q s \<longrightarrow> ?Q'3 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<lbrace>P and Q\<rbrace> f \<lbrace>R\<rbrace>; \<lbrace>\<lambda>s. \<not> Q s\<rbrace> f \<lbrace>\<lambda>_ s. \<not> Q s\<rbrace>; P s\<rbrakk> \<Longrightarrow> \<not> \<not> Q s \<longrightarrow> (P and Q) s proof (prove)
goal:
No subgoals!
theory Nondet_More_VCG

lemma hoare_lift_Pf_pre_conj:
  assumes P: "\<And>x. \<lbrace>\<lambda>s. Q x s\<rbrace> m \<lbrace>P x\<rbrace>"
  assumes f: "\<And>P. \<lbrace>\<lambda>s. P (g s) \<and> R s\<rbrace> m \<lbrace>\<lambda>_ s. P (f s)\<rbrace>"
  shows "\<lbrace>\<lambda>s. Q (g s) s \<and> R s\<rbrace> m \<lbrace>\<lambda>rv s. P (f s) rv s\<rbrace>" apply (clarsimp simp: valid_def) apply (rule use_valid [OF _ P], simp) apply (rule use_valid [OF _ f], simp, simp) done

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

lemma hoare_if_r_and:
  "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>r. if R r then Q r else Q' r\<rbrace>
   = \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. (R r \<longrightarrow> Q r s) \<and> (\<not>R r \<longrightarrow> Q' r s)\<rbrace>" by (fastforce simp: valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r. if R r then Q r else Q' r\<rbrace> = \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. (R r \<longrightarrow> Q r s) \<and> (\<not> R r \<longrightarrow> Q' r s)\<rbrace>
theory Nondet_More_VCG

lemma hoare_vcg_ex_lift_R:
  "\<lbrakk> \<And>v. \<lbrace>P v\<rbrace> f \<lbrace>Q v\<rbrace>,- \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>v. P v s\<rbrace> f \<lbrace>\<lambda>rv s. \<exists>v. Q v rv s\<rbrace>,-" apply (simp add: validE_R_def validE_def) apply (rule hoare_strengthen_post, erule hoare_vcg_ex_lift) apply (auto split: sum.split) done

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

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

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

lemma hoare_vcg_conj_liftE_R:
  "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>P'\<rbrace>,-; \<lbrace>Q\<rbrace> f \<lbrace>Q'\<rbrace>,- \<rbrakk> \<Longrightarrow> \<lbrace>P and Q\<rbrace> f \<lbrace>\<lambda>rv s. P' rv s \<and> Q' rv s\<rbrace>, -" apply (simp add: validE_R_def validE_def valid_def split: sum.splits) apply blast done

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

lemma K_valid[wp]:
  "\<lbrace>K P\<rbrace> f \<lbrace>\<lambda>_. K P\<rbrace>" by (simp add: valid_def)

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

lemma hoare_ex_all:
  "(\<forall>x. \<lbrace>P x\<rbrace> f \<lbrace>Q\<rbrace>) = \<lbrace>\<lambda>s. \<exists>x. P x s\<rbrace> f \<lbrace>Q\<rbrace>" apply (rule iffI) apply (fastforce simp: valid_def)+ done

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

lemma hoare_imp_eq_substR:
  "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,- \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. rv = x \<longrightarrow> Q x s\<rbrace>,-" by (fastforce simp add: valid_def validE_R_def validE_def split: sum.splits)

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

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

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

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

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

lemma assertE_sp:
  "\<lbrace>P\<rbrace> assertE Q \<lbrace>\<lambda>rv s. Q \<and> P s\<rbrace>,\<lbrace>E\<rbrace>" by (clarsimp simp: assertE_def) wp

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

lemma throwErrorE_E [wp]:
  "\<lbrace>Q e\<rbrace> throwError e -, \<lbrace>Q\<rbrace>" by (simp add: validE_E_def) wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>Q e\<rbrace> throwError e -, \<lbrace>Q\<rbrace>
theory Nondet_More_VCG

lemma gets_inv [simp]:
  "\<lbrace> P \<rbrace> gets f \<lbrace> \<lambda>r. P \<rbrace>" by (simp add: gets_def, wp)

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

lemma select_inv:
  "\<lbrace> P \<rbrace> select S \<lbrace> \<lambda>r. P \<rbrace>" by wpsimp

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

lemma assert_opt_inv: "\<lbrace>P\<rbrace> assert_opt Q \<lbrace>\<lambda>r. P\<rbrace>" unfolding assert_opt_def by (cases Q) simp+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> assert_opt Q \<lbrace>\<lambda>r. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> case Q of None \<Rightarrow> fail | Some v \<Rightarrow> return v \<lbrace>\<lambda>r. P\<rbrace>
theory Nondet_More_VCG

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

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

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

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

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

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

lemma list_cases_weak_wp:
  assumes "\<lbrace>P_A\<rbrace> a \<lbrace>Q\<rbrace>"
  assumes "\<And>x xs. \<lbrace>P_B\<rbrace> b x xs \<lbrace>Q\<rbrace>"
  shows
  "\<lbrace>P_A and P_B\<rbrace>
   case ts of
       [] \<Rightarrow> a
     | x#xs \<Rightarrow> b x xs
   \<lbrace>Q\<rbrace>" apply (cases ts) apply (simp, rule hoare_weaken_pre, rule assms, simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P_A and P_B\<rbrace> case ts of [] \<Rightarrow> a | x # xs \<Rightarrow> b x xs \<lbrace>Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. ts = [] \<Longrightarrow> \<lbrace>P_A and P_B\<rbrace> case ts of [] \<Rightarrow> a | x # xs \<Rightarrow> b x xs \<lbrace>Q\<rbrace>
 2. \<And>aa list. ts = aa # list \<Longrightarrow> \<lbrace>P_A and P_B\<rbrace> case ts of [] \<Rightarrow> a | x # xs \<Rightarrow> b x xs \<lbrace>Q\<rbrace> proof (prove)
goal:
No subgoals!
theory Nondet_More_VCG

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

  "\<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv s. (P' rv \<longrightarrow> X rv s) \<and> (\<not> P' rv \<longrightarrow> Y rv s)\<rbrace> \<Longrightarrow>
   \<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv. if P' rv 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 rv s \<longrightarrow> X rv s) \<and> (\<not> P rv s \<longrightarrow> Y rv s)\<rbrace> \<Longrightarrow> \<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv s. if P rv s then X rv s else Y rv s\<rbrace>) &&& (\<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv s. (P' rv \<longrightarrow> X rv s) \<and> (\<not> P' rv \<longrightarrow> Y rv s)\<rbrace> \<Longrightarrow> \<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv. if P' rv then X rv else Y rv\<rbrace>)
theory Nondet_More_VCG

lemma hoare_vcg_if_lift_ER: (* Required because of lack of rv in lifting rules *)
  "\<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv s. (P rv s \<longrightarrow> X rv s) \<and> (\<not> P rv s \<longrightarrow> Y rv s)\<rbrace>, - \<Longrightarrow>
   \<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv s. if P rv s then X rv s else Y rv s\<rbrace>, -"

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

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

lemma hoare_list_all_lift:
  "(\<And>r. r \<in> set xs \<Longrightarrow> \<lbrace>Q r\<rbrace> f \<lbrace>\<lambda>rv. Q r\<rbrace>)
   \<Longrightarrow> \<lbrace>\<lambda>s. list_all (\<lambda>r. Q r s) xs\<rbrace> f \<lbrace>\<lambda>rv s. list_all (\<lambda>r. Q r s) xs\<rbrace>" apply (induct xs; simp) apply wpsimp apply (rule hoare_vcg_conj_lift; simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>r. r \<in> set xs \<Longrightarrow> \<lbrace>Q r\<rbrace> f \<lbrace>\<lambda>rv. Q r\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. list_all (\<lambda>r. Q r s) xs\<rbrace> f \<lbrace>\<lambda>rv s. list_all (\<lambda>r. Q r s) xs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>s. True\<rbrace> f \<lbrace>\<lambda>rv s. True\<rbrace>
 2. \<And>a xs. \<lbrakk>\<lbrace>\<lambda>s. list_all (\<lambda>r. Q r s) xs\<rbrace> f \<lbrace>\<lambda>rv s. list_all (\<lambda>r. Q r s) xs\<rbrace>; \<And>r. r = a \<or> r \<in> set xs \<Longrightarrow> \<lbrace>Q r\<rbrace> f \<lbrace>\<lambda>rv. Q r\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. Q a s \<and> list_all (\<lambda>r. Q r s) xs\<rbrace> f \<lbrace>\<lambda>rv s. Q a s \<and> list_all (\<lambda>r. Q r s) xs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>\<lbrace>\<lambda>s. list_all (\<lambda>r. Q r s) xs\<rbrace> f \<lbrace>\<lambda>rv s. list_all (\<lambda>r. Q r s) xs\<rbrace>; \<And>r. r = a \<or> r \<in> set xs \<Longrightarrow> \<lbrace>Q r\<rbrace> f \<lbrace>\<lambda>rv. Q r\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. Q a s \<and> list_all (\<lambda>r. Q r s) xs\<rbrace> f \<lbrace>\<lambda>rv s. Q a s \<and> list_all (\<lambda>r. Q r s) xs\<rbrace> proof (prove)
goal:
No subgoals!
theory Nondet_More_VCG

lemma undefined_valid: "\<lbrace>\<bottom>\<rbrace> undefined \<lbrace>Q\<rbrace>" by (rule hoare_pre_cont)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. False\<rbrace> undefined \<lbrace>Q\<rbrace>
theory Nondet_More_VCG

lemma assertE_wp:
  "\<lbrace>\<lambda>s. F \<longrightarrow> Q () s\<rbrace> assertE F \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" apply (rule hoare_pre) apply (unfold assertE_def) apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. F \<longrightarrow> Q () s\<rbrace> assertE F \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> assertE F \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>
 2. \<And>s. F \<longrightarrow> Q () s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> if F then returnOk () else fail \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>
 2. \<And>s. F \<longrightarrow> Q () s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. F \<longrightarrow> Q () s \<Longrightarrow> (F \<longrightarrow> Q () s) \<and> (\<not> F \<longrightarrow> True) proof (prove)
goal:
No subgoals!
theory Nondet_More_VCG

lemma doesn't_grow_proof:
  assumes y: "\<And>s. finite (S s)"
  assumes x: "\<And>x. \<lbrace>\<lambda>s. x \<notin> S s \<and> P s\<rbrace> f \<lbrace>\<lambda>rv s. x \<notin> S s\<rbrace>"
  shows      "\<lbrace>\<lambda>s. card (S s) < n \<and> P s\<rbrace> f \<lbrace>\<lambda>rv s. card (S s) < n\<rbrace>" apply (clarsimp simp: valid_def) apply (erule le_less_trans[rotated]) apply (rule card_mono[OF y]) apply clarsimp apply (rule ccontr) apply (drule (2) use_valid[OF _ x, OF _ conjI]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. card (S s) < n \<and> P s\<rbrace> f \<lbrace>\<lambda>rv s. card (S s) < n\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); card (S s) < n; P s\<rbrakk> \<Longrightarrow> card (S b) < n proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); P s\<rbrakk> \<Longrightarrow> card (S b) \<le> card (S s) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); P s\<rbrakk> \<Longrightarrow> S b \<subseteq> S s proof (prove)
goal (1 subgoal):
 1. \<And>s a b x. \<lbrakk>(a, b) \<in> fst (f s); P s; x \<in> S b\<rbrakk> \<Longrightarrow> x \<in> S s proof (prove)
goal (1 subgoal):
 1. \<And>s a b x. \<lbrakk>(a, b) \<in> fst (f s); P s; x \<in> S b; x \<notin> S s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s a b x. \<lbrakk>P s; x \<in> S b; x \<notin> S s; x \<notin> S b\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!