kings-crown/FVELER_Isabelle huggingface dataset:
theory Nondet_More_VCG

lemma hoare_vcg_propE_R:
  "\<lbrace>\<lambda>s. P\<rbrace> f \<lbrace>\<lambda>rv s. P\<rbrace>, -" by (simp add: validE_R_def validE_def valid_def split_def split: sum.split)

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

lemma set_preserved_proof:
  assumes y: "\<And>x. \<lbrace>\<lambda>s. Q s \<and> x \<in> S s\<rbrace> f \<lbrace>\<lambda>rv s. x \<in> S s\<rbrace>"
  assumes x: "\<And>x. \<lbrace>\<lambda>s. Q s \<and> x \<notin> S s\<rbrace> f \<lbrace>\<lambda>rv s. x \<notin> S s\<rbrace>"
  shows      "\<lbrace>\<lambda>s. Q s \<and> P (S s)\<rbrace> f \<lbrace>\<lambda>rv s. P (S s)\<rbrace>" apply (clarsimp simp: valid_def) by (metis (mono_tags, lifting) equalityI post_by_hoare subsetI x y)

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

lemma set_shrink_proof:
  assumes x: "\<And>x. \<lbrace>\<lambda>s. x \<notin> S s\<rbrace> f \<lbrace>\<lambda>rv s. x \<notin> S s\<rbrace>"
  shows
  "\<lbrace>\<lambda>s. \<forall>S'. S' \<subseteq> S s \<longrightarrow> P S'\<rbrace>
   f
   \<lbrace>\<lambda>rv s. P (S s)\<rbrace>" apply (clarsimp simp: valid_def) apply (drule spec, erule mp) apply (clarsimp simp: subset_iff) apply (rule ccontr) apply (drule(1) use_valid [OF _ x]) apply simp done

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

lemma shrinks_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>"
  assumes z: "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. x \<notin> S s\<rbrace>"
  assumes w: "\<And>s. P s \<Longrightarrow> x \<in> S s"
  shows      "\<lbrace>\<lambda>s. card (S s) \<le> n \<and> P s\<rbrace> f \<lbrace>\<lambda>rv s. card (S s) < n\<rbrace>" apply (clarsimp simp: valid_def) apply (erule less_le_trans[rotated]) apply (rule psubset_card_mono[OF y]) apply (rule psubsetI) apply clarsimp apply (rule ccontr) apply (drule (2) use_valid[OF _ x, OF _ conjI]) apply simp by (metis use_valid w z)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. card (S s) \<le> 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) \<le> 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) < 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 \<subset> S s proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); P s\<rbrakk> \<Longrightarrow> S b \<subseteq> S s
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); P s\<rbrakk> \<Longrightarrow> S b \<noteq> S s proof (prove)
goal (2 subgoals):
 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
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); P s\<rbrakk> \<Longrightarrow> S b \<noteq> S s proof (prove)
goal (2 subgoals):
 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
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); P s\<rbrakk> \<Longrightarrow> S b \<noteq> S s proof (prove)
goal (2 subgoals):
 1. \<And>s a b x. \<lbrakk>P s; x \<in> S b; x \<notin> S s; x \<notin> S b\<rbrakk> \<Longrightarrow> False
 2. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); P s\<rbrakk> \<Longrightarrow> S b \<noteq> 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 \<noteq> S s
theory Nondet_More_VCG

lemma use_validE_R:
  "\<lbrakk> (Inr r, s') \<in> fst (f s); \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-; P s \<rbrakk> \<Longrightarrow> Q r s'" unfolding validE_R_def validE_def by (frule(2) use_valid, simp)

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

lemma valid_preservation_ex:
  assumes x: "\<And>x P. \<lbrace>\<lambda>s. P (f s x :: 'b)\<rbrace> m \<lbrace>\<lambda>rv s. P (f s x)\<rbrace>"
  shows      "\<lbrace>\<lambda>s. P (f s :: 'a \<Rightarrow> 'b)\<rbrace> m \<lbrace>\<lambda>rv s. P (f s)\<rbrace>" apply (clarsimp simp: valid_def) apply (erule subst[rotated, where P=P]) apply (rule ext) apply (erule use_valid [OF _ x]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (f s)\<rbrace> m \<lbrace>\<lambda>rv s. P (f s)\<rbrace> 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. f s x = f s x proof (prove)
goal:
No subgoals!
theory Nondet_More_VCG

lemma whenE_inv:
  assumes a: "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>"
  shows "\<lbrace>P\<rbrace> whenE Q f \<lbrace>\<lambda>_. P\<rbrace>" by (wpsimp wp: a)

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

lemma whenE_throwError_wp:
  "\<lbrace>\<lambda>s. \<not> P \<longrightarrow> Q s\<rbrace> whenE P (throwError e) \<lbrace>\<lambda>_. Q\<rbrace>, \<lbrace>\<top>\<top>\<rbrace>" by wpsimp

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

lemma ifM_throwError_returnOk:
  "\<lbrace>Q\<rbrace> test \<lbrace>\<lambda>c s. \<not> c \<longrightarrow> P s\<rbrace> \<Longrightarrow> \<lbrace>Q\<rbrace> ifM test (throwError e) (returnOk ()) \<lbrace>\<lambda>_. P\<rbrace>, -" unfolding ifM_def apply (fold liftE_bindE) apply wpsimp apply assumption apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>Q\<rbrace> test \<lbrace>\<lambda>c s. \<not> c \<longrightarrow> P s\<rbrace> \<Longrightarrow> \<lbrace>Q\<rbrace> ifM test (throwError e) (returnOk ()) \<lbrace>\<lambda>_. P\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>Q\<rbrace> test \<lbrace>\<lambda>c s. \<not> c \<longrightarrow> P s\<rbrace> \<Longrightarrow> \<lbrace>Q\<rbrace> do c <- test;
if c then throwError e else returnOk ()
od \<lbrace>\<lambda>_. P\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>Q\<rbrace> test \<lbrace>\<lambda>c s. \<not> c \<longrightarrow> P s\<rbrace> \<Longrightarrow> \<lbrace>Q\<rbrace> doE c <- liftE test;
if c then throwError e else returnOk ()
odE \<lbrace>\<lambda>_. P\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>Q\<rbrace> test \<lbrace>\<lambda>c s. \<not> c \<longrightarrow> P s\<rbrace> \<Longrightarrow> \<lbrace>?P'8\<rbrace> test \<lbrace>\<lambda>c s. \<not> c \<longrightarrow> P s\<rbrace>
 2. \<And>s. \<lbrakk>\<lbrace>Q\<rbrace> test \<lbrace>\<lambda>c s. \<not> c \<longrightarrow> P s\<rbrace>; Q s\<rbrakk> \<Longrightarrow> True \<and> ?P'8 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<lbrace>Q\<rbrace> test \<lbrace>\<lambda>c s. \<not> c \<longrightarrow> P s\<rbrace>; Q s\<rbrakk> \<Longrightarrow> True \<and> Q s proof (prove)
goal:
No subgoals!
theory Nondet_More_VCG

lemma ifME_liftE:
  "ifME (liftE test) a b = ifM test a b" by (simp add: ifME_def ifM_def liftE_bindE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ifME (liftE test) a b = ifM test a b
theory Nondet_More_VCG

lemma gets_the_inv: "\<lbrace>P\<rbrace> gets_the V \<lbrace>\<lambda>rv. P\<rbrace>" by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> gets_the V \<lbrace>\<lambda>rv. P\<rbrace>
theory Nondet_More_VCG

lemma select_f_inv:
  "\<lbrace>P\<rbrace> select_f S \<lbrace>\<lambda>_. P\<rbrace>" by (simp add: select_f_def valid_def)

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

lemma validI:
  assumes rl: "\<And>s r s'. \<lbrakk> P s; (r, s') \<in> fst (S s) \<rbrakk> \<Longrightarrow> Q r s'"
  shows "\<lbrace>P\<rbrace> S \<lbrace>Q\<rbrace>" unfolding valid_def using rl by safe

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

goal (1 subgoal):
 1. \<forall>s. P s \<longrightarrow> (\<forall>(r, s')\<in>fst (S s). Q r s')
theory Nondet_More_VCG

lemma opt_return_pres_lift:
  assumes x: "\<And>v. \<lbrace>P\<rbrace> f v \<lbrace>\<lambda>rv. P\<rbrace>"
  shows      "\<lbrace>P\<rbrace> case x of None \<Rightarrow> return () | Some v \<Rightarrow> f v \<lbrace>\<lambda>rv. P\<rbrace>" by (wpsimp wp: x)

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

lemma valid_return_unit:
  "\<lbrace>P\<rbrace> f >>= (\<lambda>_. return ()) \<lbrace>\<lambda>r. Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r. Q\<rbrace>" by (auto simp: valid_def in_bind in_return Ball_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> do _ <- f;
return ()
od \<lbrace>\<lambda>r. Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r. Q\<rbrace>
theory Nondet_More_VCG

lemma hoare_weak_lift_imp_conj:
  "\<lbrakk> \<lbrace>Q\<rbrace> m \<lbrace>Q'\<rbrace>; \<lbrace>R\<rbrace> m \<lbrace>R'\<rbrace> \<rbrakk>
   \<Longrightarrow> \<lbrace>\<lambda>s. (P \<longrightarrow> Q s) \<and> R s\<rbrace> m \<lbrace>\<lambda>rv s. (P \<longrightarrow> Q' rv s) \<and> R' rv s\<rbrace>" apply (rule hoare_vcg_conj_lift) apply (rule hoare_weak_lift_imp) apply assumption+ done

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

lemma hoare_eq_P:
  assumes "\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>"
  shows "\<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>" by (rule assms)

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

lemma hoare_validE_R_conj:
  "\<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, -; \<lbrace>P\<rbrace> f \<lbrace>R\<rbrace>, -\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q and R\<rbrace>, -" by (simp add: valid_def validE_def validE_R_def Let_def split_def 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>R\<rbrace>, -\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q and R\<rbrace>, -
theory Nondet_More_VCG

lemma P_bool_lift:
  assumes t: "\<lbrace>Q\<rbrace> f \<lbrace>\<lambda>r. Q\<rbrace>"
  assumes f: "\<lbrace>\<lambda>s. \<not>Q s\<rbrace> f \<lbrace>\<lambda>r s. \<not>Q s\<rbrace>"
  shows "\<lbrace>\<lambda>s. P (Q s)\<rbrace> f \<lbrace>\<lambda>r s. P (Q s)\<rbrace>" apply (clarsimp simp: valid_def) apply (rule back_subst[where P=P], assumption) apply (rule iffI) apply (erule (1) use_valid [OF _ t]) apply (rule classical) apply (drule (1) use_valid [OF _ f]) apply simp done

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

lemma gets_sp: "\<lbrace>P\<rbrace> gets f \<lbrace>\<lambda>rv. P and (\<lambda>s. f s = rv)\<rbrace>" by (wp, simp)

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

lemma hoare_Ball_helper:
  assumes x: "\<And>x. \<lbrace>P x\<rbrace> f \<lbrace>Q x\<rbrace>"
  assumes y: "\<And>P. \<lbrace>\<lambda>s. P (S s)\<rbrace> f \<lbrace>\<lambda>rv s. P (S s)\<rbrace>"
  shows "\<lbrace>\<lambda>s. \<forall>x \<in> S s. P x s\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x \<in> S s. Q x rv s\<rbrace>" apply (clarsimp simp: valid_def) apply (drule bspec, erule back_subst[where P="\<lambda>A. x\<in>A" for x]) apply (erule post_by_hoare[OF y, rotated]) apply (rule refl) apply (erule (1) post_by_hoare[OF x]) done

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

lemma handy_prop_divs:
  assumes x: "\<And>P. \<lbrace>\<lambda>s. P (Q s) \<and> S s\<rbrace> f \<lbrace>\<lambda>rv s. P (Q' rv s)\<rbrace>"
             "\<And>P. \<lbrace>\<lambda>s. P (R s) \<and> S s\<rbrace> f \<lbrace>\<lambda>rv s. P (R' rv s)\<rbrace>"
  shows      "\<lbrace>\<lambda>s. P (Q s \<and> R s) \<and> S s\<rbrace> f \<lbrace>\<lambda>rv s. P (Q' rv s \<and> R' rv s)\<rbrace>"
             "\<lbrace>\<lambda>s. P (Q s \<or> R s) \<and> S s\<rbrace> f \<lbrace>\<lambda>rv s. P (Q' rv s \<or> R' rv s)\<rbrace>" apply (clarsimp simp: valid_def
                  elim!: subst[rotated, where P=P]) apply (rule use_valid [OF _ x(1)], assumption) apply (rule use_valid [OF _ x(2)], assumption) apply simp apply (clarsimp simp: valid_def
                 elim!: subst[rotated, where P=P]) apply (rule use_valid [OF _ x(1)], assumption) apply (rule use_valid [OF _ x(2)], assumption) apply simp done

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

lemma hoare_set_preserved:
  assumes x: "\<And>x. \<lbrace>fn' x\<rbrace> m \<lbrace>\<lambda>rv. fn x\<rbrace>"
  shows      "\<lbrace>\<lambda>s. set xs \<subseteq> {x. fn' x s}\<rbrace> m \<lbrace>\<lambda>rv s. set xs \<subseteq> {x. fn x s}\<rbrace>" apply (induct xs) apply simp apply wp apply simp apply (rule hoare_vcg_conj_lift) apply (rule x) apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. set xs \<subseteq> {x. fn' x s}\<rbrace> m \<lbrace>\<lambda>rv s. set xs \<subseteq> {x. fn x s}\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>s. set [] \<subseteq> {x. fn' x s}\<rbrace> m \<lbrace>\<lambda>rv s. set [] \<subseteq> {x. fn x s}\<rbrace>
 2. \<And>a xs. \<lbrace>\<lambda>s. set xs \<subseteq> {x. fn' x s}\<rbrace> m \<lbrace>\<lambda>rv s. set xs \<subseteq> {x. fn x s}\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. set (a # xs) \<subseteq> {x. fn' x s}\<rbrace> m \<lbrace>\<lambda>rv s. set (a # xs) \<subseteq> {x. fn x s}\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>s. True\<rbrace> m \<lbrace>\<lambda>rv s. True\<rbrace>
 2. \<And>a xs. \<lbrace>\<lambda>s. set xs \<subseteq> {x. fn' x s}\<rbrace> m \<lbrace>\<lambda>rv s. set xs \<subseteq> {x. fn x s}\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. set (a # xs) \<subseteq> {x. fn' x s}\<rbrace> m \<lbrace>\<lambda>rv s. set (a # xs) \<subseteq> {x. fn x s}\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrace>\<lambda>s. set xs \<subseteq> {x. fn' x s}\<rbrace> m \<lbrace>\<lambda>rv s. set xs \<subseteq> {x. fn x s}\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. set (a # xs) \<subseteq> {x. fn' x s}\<rbrace> m \<lbrace>\<lambda>rv s. set (a # xs) \<subseteq> {x. fn x s}\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrace>\<lambda>s. set xs \<subseteq> {x. fn' x s}\<rbrace> m \<lbrace>\<lambda>rv s. set xs \<subseteq> {x. fn x s}\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. fn' a s \<and> set xs \<subseteq> {x. fn' x s}\<rbrace> m \<lbrace>\<lambda>rv s. fn a s \<and> set xs \<subseteq> {x. fn x s}\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>a xs. \<lbrace>\<lambda>s. set xs \<subseteq> {x. fn' x s}\<rbrace> m \<lbrace>\<lambda>rv s. set xs \<subseteq> {x. fn x s}\<rbrace> \<Longrightarrow> \<lbrace>fn' a\<rbrace> m \<lbrace>\<lambda>rv. fn a\<rbrace>
 2. \<And>a xs. \<lbrace>\<lambda>s. set xs \<subseteq> {x. fn' x s}\<rbrace> m \<lbrace>\<lambda>rv s. set xs \<subseteq> {x. fn x s}\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. set xs \<subseteq> {x. fn' x s}\<rbrace> m \<lbrace>\<lambda>rv s. set xs \<subseteq> {x. fn x s}\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrace>\<lambda>s. set xs \<subseteq> {x. fn' x s}\<rbrace> m \<lbrace>\<lambda>rv s. set xs \<subseteq> {x. fn x s}\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. set xs \<subseteq> {x. fn' x s}\<rbrace> m \<lbrace>\<lambda>rv s. set xs \<subseteq> {x. fn x s}\<rbrace> proof (prove)
goal:
No subgoals!
theory Nondet_More_VCG

lemma hoare_conj_lift_inv:
  "\<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; \<lbrace>\<lambda>s. P' s \<and> I s\<rbrace> f \<lbrace>\<lambda>rv. I\<rbrace>;
    \<And>s. P s \<Longrightarrow> P' s\<rbrakk>
   \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> I s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> I s\<rbrace>" by (fastforce simp: valid_def)

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