kings-crown/FVELER_Isabelle huggingface dataset:
theory Trace_VCG

lemma hoare_elim_pred_conjE1:
  "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>,\<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv. Q rv and Q' rv\<rbrace>,\<lbrace>E\<rbrace>" by (unfold pred_conj_def)

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

lemma hoare_elim_pred_conjE2:
  "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>rv s. E rv s \<and> E' rv s\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>\<lambda>rv. E rv and E' rv\<rbrace>" by (unfold pred_conj_def)

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

lemma hoare_elim_pred_conjE_R:
  "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>,- \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv. Q rv and Q' rv\<rbrace>,-" by (unfold pred_conj_def)

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

lemma hoare_pre_cases:
  "\<lbrakk> \<lbrace>\<lambda>s. R s \<and> P s\<rbrace> f \<lbrace>Q\<rbrace>; \<lbrace>\<lambda>s. \<not>R s \<and> P' s\<rbrace> f \<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P and P'\<rbrace> f \<lbrace>Q\<rbrace>" unfolding valid_def by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>\<lambda>s. R s \<and> P s\<rbrace> f \<lbrace>Q\<rbrace>; \<lbrace>\<lambda>s. \<not> R s \<and> P' s\<rbrace> f \<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P and P'\<rbrace> f \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s. R s \<and> P s \<longrightarrow> (\<forall>(r, s')\<in>mres (f s). Q r s'); \<forall>s. \<not> R s \<and> P' s \<longrightarrow> (\<forall>(r, s')\<in>mres (f s). Q r s')\<rbrakk> \<Longrightarrow> \<forall>s. (P and P') s \<longrightarrow> (\<forall>(r, s')\<in>mres (f s). Q r s')
theory Trace_VCG

lemma hoare_vcg_mp:
  "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. Q r s \<longrightarrow> Q' r s\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>" by (auto simp: 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>\<lambda>r s. Q r s \<longrightarrow> Q' r s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>
theory Trace_VCG

lemma hoare_add_post:
  "\<lbrakk> \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>; \<And>s. P s \<Longrightarrow> P' s; \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q' rv s \<longrightarrow> Q rv s\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>" unfolding valid_def by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>; \<And>s. P s \<Longrightarrow> P' s; \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q' rv s \<longrightarrow> Q rv s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s. P' s \<longrightarrow> (\<forall>(r, s')\<in>mres (f s). Q' r s'); \<And>s. P s \<Longrightarrow> P' s; \<forall>s. P s \<longrightarrow> (\<forall>(r, s')\<in>mres (f s). Q' r s' \<longrightarrow> Q r s')\<rbrakk> \<Longrightarrow> \<forall>s. P s \<longrightarrow> (\<forall>(r, s')\<in>mres (f s). Q r s')
theory Trace_VCG

lemma hoare_gen_asmE:
  "(P \<Longrightarrow> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>,-) \<Longrightarrow> \<lbrace>P' and K P\<rbrace> f \<lbrace>Q\<rbrace>, -" by (simp add: validE_R_def validE_def valid_def) blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P \<Longrightarrow> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>, -) \<Longrightarrow> \<lbrace>P' and K P\<rbrace> f \<lbrace>Q\<rbrace>, -
theory Trace_VCG

lemma hoare_list_case:
  "\<lbrakk> \<lbrace>P1\<rbrace> f f1 \<lbrace>Q\<rbrace>; \<And>y ys. xs = y#ys \<Longrightarrow> \<lbrace>P2 y ys\<rbrace> f (f2 y ys) \<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow>
   \<lbrace>case xs of [] \<Rightarrow> P1 | y#ys \<Rightarrow> P2 y ys\<rbrace> f (case xs of [] \<Rightarrow> f1 | y#ys \<Rightarrow> f2 y ys) \<lbrace>Q\<rbrace>" by (cases xs; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P1\<rbrace> f f1 \<lbrace>Q\<rbrace>; \<And>y ys. xs = y # ys \<Longrightarrow> \<lbrace>P2 y ys\<rbrace> f (f2 y ys) \<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>case xs of [] \<Rightarrow> P1 | y # ys \<Rightarrow> P2 y ys\<rbrace> f (case xs of [] \<Rightarrow> f1 | y # ys \<Rightarrow> f2 y ys) \<lbrace>Q\<rbrace>
theory Trace_VCG

lemma hoare_fail_any[simp]:
  "\<lbrace>P\<rbrace> fail \<lbrace>Q\<rbrace>" by wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> fail \<lbrace>Q\<rbrace>
theory Trace_VCG

lemma hoare_failE[simp]:
  "\<lbrace>P\<rbrace> fail \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>" by wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> fail \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>
theory Trace_VCG

lemma hoare_FalseE[simp]:
  "\<lbrace>\<bottom>\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>" by (simp add: valid_def validE_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. False\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>
theory Trace_VCG

lemma hoare_validE_pred_conj:
  "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>R\<rbrace>, \<lbrace>E\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q and R\<rbrace>, \<lbrace>E\<rbrace>" unfolding valid_def validE_def by (simp add: split_def split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>R\<rbrace>, \<lbrace>E\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q and R\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s. P s \<longrightarrow> (\<forall>(r, s')\<in>mres (f s). case r of Inl e \<Rightarrow> E e s' | Inr r \<Rightarrow> Q r s'); \<forall>s. P s \<longrightarrow> (\<forall>(r, s')\<in>mres (f s). case r of Inl e \<Rightarrow> E e s' | Inr r \<Rightarrow> R r s')\<rbrakk> \<Longrightarrow> \<forall>s. P s \<longrightarrow> (\<forall>(r, s')\<in>mres (f s). case r of Inl e \<Rightarrow> E e s' | Inr r \<Rightarrow> (Q and R) r s')
theory Trace_VCG

lemma hoare_validE_conj:
  "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>R\<rbrace>, \<lbrace>E\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> R rv s\<rbrace>, \<lbrace>E\<rbrace>" unfolding valid_def validE_def by (simp add: split_def split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>R\<rbrace>, \<lbrace>E\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> R rv s\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s. P s \<longrightarrow> (\<forall>(r, s')\<in>mres (f s). case r of Inl e \<Rightarrow> E e s' | Inr r \<Rightarrow> Q r s'); \<forall>s. P s \<longrightarrow> (\<forall>(r, s')\<in>mres (f s). case r of Inl e \<Rightarrow> E e s' | Inr r \<Rightarrow> R r s')\<rbrakk> \<Longrightarrow> \<forall>s. P s \<longrightarrow> (\<forall>(r, s')\<in>mres (f s). case r of Inl e \<Rightarrow> E e s' | Inr r \<Rightarrow> Q r s' \<and> R r s')
theory Trace_VCG

lemma hoare_drop_imp:
  "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. R rv s \<longrightarrow> Q rv s\<rbrace>" by (auto simp: valid_def)

(* 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. R rv s \<longrightarrow> Q rv s\<rbrace>
theory Trace_VCG

lemma hoare_drop_impE_R:
  "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,- \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. R rv s \<longrightarrow> Q rv s\<rbrace>, -" by (auto simp: validE_R_def validE_def valid_def split_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. R rv s \<longrightarrow> Q rv s\<rbrace>, -
theory Trace_VCG

lemma hoare_drop_impE_E:
  "\<lbrace>P\<rbrace> f -,\<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f -, \<lbrace>\<lambda>rv s. R rv s \<longrightarrow> Q rv s\<rbrace>" by (auto simp: validE_E_def validE_def valid_def split_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. R rv s \<longrightarrow> Q rv s\<rbrace>
theory Trace_VCG

lemma hoare_drop_imp_conj[wp_unsafe]:
  "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>; \<lbrace>P'\<rbrace> f \<lbrace>\<lambda>rv s. (Q rv s \<longrightarrow> Q'' rv s) \<and> Q''' rv s\<rbrace> \<rbrakk> \<Longrightarrow>
   \<lbrace>P and P'\<rbrace> f \<lbrace>\<lambda>rv s. (Q rv s \<longrightarrow> Q' rv s \<and> Q'' rv s) \<and> Q''' rv s\<rbrace>" by (auto simp: valid_def)

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

lemma True_E_E[wp]:
  "\<lbrace>\<top>\<rbrace> f -,\<lbrace>\<top>\<top>\<rbrace>" by (auto simp: validE_E_def validE_def valid_def split: sum.splits)

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

lemma hoare_vcg_set_pred_lift:
  assumes "\<And>P x. m \<lbrace> \<lambda>s. P (f x s) \<rbrace>"
  shows "m \<lbrace> \<lambda>s. P {x. f x s} \<rbrace>" using assms[where P="\<lambda>x . x"] assms[where P=Not] use_valid by (fastforce simp: valid_def elim!: subst[rotated, where P=P])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P {x. f x s}\<rbrace> m \<lbrace>\<lambda>_ s. P {x. f x s}\<rbrace> proof (prove)
using this:
\<lbrace>f ?x\<rbrace> m \<lbrace>\<lambda>_. f ?x\<rbrace>
\<lbrace>\<lambda>s. \<not> f ?x s\<rbrace> m \<lbrace>\<lambda>_ s. \<not> f ?x s\<rbrace>
\<lbrakk>(?r, ?s') \<in> mres (?f ?s); \<lbrace>?P\<rbrace> ?f \<lbrace>?Q\<rbrace>; ?P ?s\<rbrakk> \<Longrightarrow> ?Q ?r ?s'

goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P {x. f x s}\<rbrace> m \<lbrace>\<lambda>_ s. P {x. f x s}\<rbrace>
theory Trace_VCG

lemma hoare_vcg_set_pred_lift_mono:
  assumes f: "\<And>x. m \<lbrace> f x \<rbrace>"
  assumes mono: "\<And>A B. A \<subseteq> B \<Longrightarrow> P A \<Longrightarrow> P B"
  shows "m \<lbrace> \<lambda>s. P {x. f x s} \<rbrace>" by (fastforce simp: valid_def elim!: mono[rotated] dest: use_valid[OF _ f])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P {x. f x s}\<rbrace> m \<lbrace>\<lambda>_ s. P {x. f x s}\<rbrace>
theory Trace_VCG

lemma hoare_strengthen_pre_via_assert_forward:
  assumes pos: "\<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>"
  assumes rel: "\<And>s. S s \<longrightarrow> P s \<or> N s"
  assumes neg: "\<lbrace> N \<rbrace> f \<lbrace> \<bottom>\<bottom> \<rbrace>"
  shows "\<lbrace> S \<rbrace> f \<lbrace> Q \<rbrace>" apply (rule hoare_weaken_pre) apply (rule hoare_strengthen_post) apply (rule hoare_vcg_disj_lift[OF pos neg]) by (auto simp: rel)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>S\<rbrace> f \<lbrace>Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> f \<lbrace>Q\<rbrace>
 2. \<And>s. S s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?Q\<rbrace> f \<lbrace>?Q3\<rbrace>
 2. \<And>rv s. ?Q3 rv s \<Longrightarrow> Q rv s
 3. \<And>s. S s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>rv s. Q rv s \<or> False \<Longrightarrow> Q rv s
 2. \<And>s. S s \<Longrightarrow> P s \<or> N s
theory Trace_VCG

lemma hoare_strengthen_pre_via_assert_backward:
  assumes neg: "\<lbrace> Not \<circ> E \<rbrace> f \<lbrace> \<bottom>\<bottom> \<rbrace>"
  assumes pos: "\<lbrace> P and E \<rbrace> f \<lbrace> Q \<rbrace>"
  shows "\<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>" by (rule hoare_strengthen_pre_via_assert_forward[OF pos _ neg], simp)

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

lemma get_sp:
  "\<lbrace>P\<rbrace> get \<lbrace>\<lambda>rv s. s = rv \<and> P s\<rbrace>" by(simp add:get_def valid_def mres_def)

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

lemma put_sp:
  "\<lbrace>\<top>\<rbrace> put a \<lbrace>\<lambda>_ s. s = a\<rbrace>" by(simp add:put_def valid_def mres_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> put a \<lbrace>\<lambda>_ s. s = a\<rbrace>
theory Trace_VCG

lemma return_sp:
  "\<lbrace>P\<rbrace> return a \<lbrace>\<lambda>rv s. rv = a \<and> P s\<rbrace>" by(simp add:return_def valid_def mres_def)

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

lemma hoare_return_sp: (* FIXME lib: eliminate *)
  "\<lbrace>P\<rbrace> return x \<lbrace>\<lambda>rv. P and K (rv = x)\<rbrace>" by (simp add: valid_def return_def mres_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> return x \<lbrace>\<lambda>rv. P and K (rv = x)\<rbrace>
theory Trace_VCG

lemma assert_sp:
  "\<lbrace>P\<rbrace> assert Q \<lbrace>\<lambda>_ s. P s \<and> Q \<rbrace>" by (simp add: assert_def fail_def return_def valid_def mres_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> assert Q \<lbrace>\<lambda>_ s. P s \<and> Q\<rbrace>
theory Trace_VCG

lemma hoare_gets_sp:
  "\<lbrace>P\<rbrace> gets f \<lbrace>\<lambda>rv s. rv = f s \<and> P s\<rbrace>" by (simp add: valid_def simpler_gets_def mres_def)

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

lemma hoare_returnOk_sp:
  "\<lbrace>P\<rbrace> returnOk x \<lbrace>\<lambda>rv s. rv = x \<and> P s\<rbrace>, \<lbrace>Q\<rbrace>" by (simp add: valid_def validE_def returnOk_def return_def mres_def)

\<comment> \<open>For forward reasoning in Hoare proofs, these lemmas allow us to step over the
    left-hand-side of monadic bind, while keeping the same precondition.\<close>

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> returnOk x \<lbrace>\<lambda>rv s. rv = x \<and> P s\<rbrace>, \<lbrace>Q\<rbrace>
theory Trace_No_Fail

lemma no_fail_pre[wp_pre]:
  "\<lbrakk> no_fail P f; \<And>s. Q s \<Longrightarrow> P s\<rbrakk> \<Longrightarrow> no_fail Q f" by (simp add: no_fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_fail P f; \<And>s. Q s \<Longrightarrow> P s\<rbrakk> \<Longrightarrow> no_fail Q f
theory Trace_No_Fail

lemma wpc_helper_no_fail_final:
  "no_fail Q f \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') (no_fail P f)" by (clarsimp simp: wpc_helper_def elim!: no_fail_pre)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail Q f \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') (no_fail P f)
theory Trace_No_Fail

lemma no_failD:
  "\<lbrakk> no_fail P m; P s \<rbrakk> \<Longrightarrow> \<not> failed (m s)" by (simp add: no_fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_fail P m; P s\<rbrakk> \<Longrightarrow> \<not> failed (m s)
theory Trace_No_Fail

lemma no_fail_return[simp, wp]:
  "no_fail \<top> (return x)" by (simp add: return_def no_fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) (return x)
theory Trace_No_Fail

lemma no_fail_bind[wp]:
  "\<lbrakk> no_fail P f; \<And>x. no_fail (R x) (g x); \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace> \<rbrakk> \<Longrightarrow> no_fail (P and Q) (f >>= (\<lambda>rv. g rv))" apply (simp add: no_fail_def bind_def' image_Un image_image
                   in_image_constant failed_def) apply (intro allI conjI impI) apply (fastforce simp: image_def) apply clarsimp apply (drule(1) post_by_hoare, erule in_mres) apply (fastforce simp: image_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_fail P f; \<And>x. no_fail (R x) (g x); \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>\<rbrakk> \<Longrightarrow> no_fail (P and Q) (f >>= g) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s. P s \<longrightarrow> Failed \<notin> snd ` f s; \<And>x. \<forall>s. R x s \<longrightarrow> Failed \<notin> snd ` g x s; \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>\<rbrakk> \<Longrightarrow> \<forall>s. P s \<and> Q s \<longrightarrow> (\<forall>x. (x, Failed) \<notin> f s) \<and> Failed \<notin> snd ` (\<Union>(xs, rv, s)\<in>{(xs, rv, s'). (xs, Result (rv, s')) \<in> f s}. (\<lambda>(a, y). (a @ xs, y)) ` g rv s) proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<lbrakk>\<forall>s. P s \<longrightarrow> Failed \<notin> snd ` f s; \<And>x. \<forall>s. R x s \<longrightarrow> Failed \<notin> snd ` g x s; \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>; P s \<and> Q s\<rbrakk> \<Longrightarrow> (x, Failed) \<notin> f s
 2. \<And>s. \<lbrakk>\<forall>s. P s \<longrightarrow> Failed \<notin> snd ` f s; \<And>x. \<forall>s. R x s \<longrightarrow> Failed \<notin> snd ` g x s; \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>; P s \<and> Q s\<rbrakk> \<Longrightarrow> Failed \<notin> snd ` (\<Union>(xs, rv, s)\<in>{(xs, rv, s'). (xs, Result (rv, s')) \<in> f s}. (\<lambda>(a, y). (a @ xs, y)) ` g rv s) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>s. P s \<longrightarrow> Failed \<notin> snd ` f s; \<And>x. \<forall>s. R x s \<longrightarrow> Failed \<notin> snd ` g x s; \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>; P s \<and> Q s\<rbrakk> \<Longrightarrow> Failed \<notin> snd ` (\<Union>(xs, rv, s)\<in>{(xs, rv, s'). (xs, Result (rv, s')) \<in> f s}. (\<lambda>(a, y). (a @ xs, y)) ` g rv s) proof (prove)
goal (1 subgoal):
 1. \<And>s aa ab ba ac. \<lbrakk>\<forall>s. P s \<longrightarrow> Failed \<notin> snd ` f s; \<And>x. \<forall>s. R x s \<longrightarrow> Failed \<notin> snd ` g x s; \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>; P s; Q s; (ac, Failed) \<in> g ab ba; (aa, Result (ab, ba)) \<in> f s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s aa ab ba ac. \<lbrakk>\<forall>s. P s \<longrightarrow> Failed \<notin> snd ` f s; \<And>x. \<forall>s. R x s \<longrightarrow> Failed \<notin> snd ` g x s; P s; Q s; (ac, Failed) \<in> g ab ba; (aa, Result (ab, ba)) \<in> f s; R ab ba\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Trace_No_Fail

lemma no_fail_get[simp, wp]:
  "no_fail \<top> get" by (simp add: get_def no_fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) get
theory Trace_No_Fail

lemma no_fail_put[simp, wp]:
  "no_fail \<top> (put s)" by (simp add: put_def no_fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) (put s)
theory Trace_No_Fail

lemma no_fail_modify[wp,simp]:
  "no_fail \<top> (modify f)" by (wpsimp simp: modify_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) (modify f)
theory Trace_No_Fail

lemma no_fail_gets_simp[simp]:
  "no_fail P (gets f)" by (wpsimp simp: gets_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail P (gets f)
theory Trace_No_Fail

lemma no_fail_gets[wp]:
  "no_fail \<top> (gets f)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) (gets f)
theory Trace_No_Fail

lemma no_fail_select[wp,simp]:
  "no_fail \<top> (select S)" by (simp add: no_fail_def select_def image_def failed_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) (select S)
theory Trace_No_Fail

lemma no_fail_alt[wp]:
  "\<lbrakk> no_fail P f; no_fail Q g \<rbrakk> \<Longrightarrow> no_fail (P and Q) (f \<sqinter> g)" by (auto simp: no_fail_def alternative_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_fail P f; no_fail Q g\<rbrakk> \<Longrightarrow> no_fail (P and Q) (f \<sqinter> g)
theory Trace_No_Fail

lemma no_fail_when[wp]:
  "(P \<Longrightarrow> no_fail Q f) \<Longrightarrow> no_fail (if P then Q else \<top>) (when P f)" by (simp add: when_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P \<Longrightarrow> no_fail Q f) \<Longrightarrow> no_fail (if P then Q else (\<lambda>_. True)) (when P f)
theory Trace_No_Fail

lemma no_fail_unless[wp]:
  "(\<not>P \<Longrightarrow> no_fail Q f) \<Longrightarrow> no_fail (if P then \<top> else Q) (unless P f)" by (simp add: unless_def when_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<not> P \<Longrightarrow> no_fail Q f) \<Longrightarrow> no_fail (if P then \<lambda>_. True else Q) (unless P f)
theory Trace_No_Fail

lemma no_fail_fail[simp, wp]:
  "no_fail \<bottom> fail" by (simp add: fail_def no_fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. False) fail
theory Trace_No_Fail

lemma no_fail_assert[simp, wp]:
  "no_fail (\<lambda>_. P) (assert P)" by (simp add: assert_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. P) (assert P)
theory Trace_No_Fail

lemma no_fail_assert_opt[simp, wp]:
  "no_fail (\<lambda>_. P \<noteq> None) (assert_opt P)" by (simp add: assert_opt_def split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. P \<noteq> None) (assert_opt P)
theory Trace_No_Fail

lemma no_fail_case_option[wp]:
  assumes f: "no_fail P f"
  assumes g: "\<And>x. no_fail (Q x) (g x)"
  shows "no_fail (if x = None then P else Q (the x)) (case_option f g x)" by (clarsimp simp add: f g)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (if x = None then P else Q (the x)) (case x of None \<Rightarrow> f | Some x \<Rightarrow> g x)
theory Trace_No_Fail

lemma no_fail_if[wp]:
  "\<lbrakk> P \<Longrightarrow> no_fail Q f; \<not>P \<Longrightarrow> no_fail R g \<rbrakk> \<Longrightarrow> no_fail (if P then Q else R) (if P then f else g)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<Longrightarrow> no_fail Q f; \<not> P \<Longrightarrow> no_fail R g\<rbrakk> \<Longrightarrow> no_fail (if P then Q else R) (if P then f else g)
theory Trace_No_Fail

lemma no_fail_apply[wp]:
  "no_fail P (f (g x)) \<Longrightarrow> no_fail P (f $ g x)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail P (f (g x)) \<Longrightarrow> no_fail P (f $ g x)