kings-crown/FVELER_Isabelle huggingface dataset:
theory Trace_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 Trace_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 Trace_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 Trace_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 Trace_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 Trace_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 Trace_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 Trace_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 Trace_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 Trace_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 Trace_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 Trace_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 Trace_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 Trace_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 Trace_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 Trace_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> mres (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> mres (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> mres (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> mres (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> mres (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!
theory Trace_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 Trace_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> mres (f s); Q s; P (S s)\<rbrakk> \<Longrightarrow> P (S b)
theory Trace_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> mres (f s)\<rbrakk> \<Longrightarrow> P (S b) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. (a, b) \<in> mres (f s) \<Longrightarrow> S b \<subseteq> S s proof (prove)
goal (1 subgoal):
 1. \<And>s a b t. \<lbrakk>(a, b) \<in> mres (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> mres (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 Trace_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> mres (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> mres (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> mres (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> mres (f s); P s\<rbrakk> \<Longrightarrow> S b \<subseteq> S s
 2. \<And>s a b. \<lbrakk>(a, b) \<in> mres (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> mres (f s); P s; x \<in> S b\<rbrakk> \<Longrightarrow> x \<in> S s
 2. \<And>s a b. \<lbrakk>(a, b) \<in> mres (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> mres (f s); P s; x \<in> S b; x \<notin> S s\<rbrakk> \<Longrightarrow> False
 2. \<And>s a b. \<lbrakk>(a, b) \<in> mres (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> mres (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> mres (f s); P s\<rbrakk> \<Longrightarrow> S b \<noteq> S s
theory Trace_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> mres (m s)\<rbrakk> \<Longrightarrow> P (f b) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. (a, b) \<in> mres (m s) \<Longrightarrow> f s = f b proof (prove)
goal (1 subgoal):
 1. \<And>s a b x. (a, b) \<in> mres (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 Trace_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 Trace_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 Trace_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 Trace_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 Trace_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 Trace_More_VCG

lemma validI:
  assumes rl: "\<And>s r s'. \<lbrakk> P s; (r, s') \<in> mres (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>mres (S s). Q r s') proof (prove)
using this:
\<lbrakk>P ?s; (?r, ?s') \<in> mres (S ?s)\<rbrakk> \<Longrightarrow> Q ?r ?s'

goal (1 subgoal):
 1. \<forall>s. P s \<longrightarrow> (\<forall>(r, s')\<in>mres (S s). Q r s')
theory Trace_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>