kings-crown/FVELER_Isabelle huggingface dataset:
theory Nondet_VCG

lemma select_throwError_wp:
  "\<lbrace>\<lambda>s. \<forall>x\<in>S. Q x s\<rbrace> select S >>= throwError -, \<lbrace>Q\<rbrace>" by (simp add: bind_def throwError_def return_def select_def validE_E_def validE_def valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>x\<in>S. Q x s\<rbrace> select S >>= throwError -, \<lbrace>Q\<rbrace>
theory Nondet_VCG

lemma valid_is_triple:
  "valid P f Q = triple_judgement P f (postcondition Q (\<lambda>s f. fst (f s)))" by (simp add: triple_judgement_def valid_def postcondition_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> = triple_judgement P f (postcondition Q (\<lambda>s f. fst (f s)))
theory Nondet_VCG

lemma validE_is_triple:
  "validE P f Q E =
   triple_judgement P f
     (postconditions (postcondition Q (\<lambda>s f. {(rv, s'). (Inr rv, s') \<in> fst (f s)}))
                     (postcondition E (\<lambda>s f. {(rv, s'). (Inl rv, s') \<in> fst (f s)})))" by (fastforce simp: validE_def triple_judgement_def valid_def postcondition_def postconditions_def
                split: sum.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> = triple_judgement P f (postconditions (postcondition Q (\<lambda>s f. {(rv, s'). (Inr rv, s') \<in> fst (f s)})) (postcondition E (\<lambda>s f. {(rv, s'). (Inl rv, s') \<in> fst (f s)})))
theory Nondet_VCG

lemma validE_R_is_triple:
  "validE_R P f Q =
   triple_judgement P f (postcondition Q (\<lambda>s f. {(rv, s'). (Inr rv, s') \<in> fst (f s)}))" by (simp add: validE_R_def validE_is_triple postconditions_def postcondition_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, - = triple_judgement P f (postcondition Q (\<lambda>s f. {(rv, s'). (Inr rv, s') \<in> fst (f s)}))
theory Nondet_VCG

lemma validE_E_is_triple:
  "validE_E P f E =
   triple_judgement P f (postcondition E (\<lambda>s f. {(rv, s'). (Inl rv, s') \<in> fst (f s)}))" by (simp add: validE_E_def validE_is_triple postconditions_def postcondition_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f -, \<lbrace>E\<rbrace> = triple_judgement P f (postcondition E (\<lambda>s f. {(rv, s'). (Inl rv, s') \<in> fst (f s)}))
theory Nondet_VCG

lemma hoare_post_eq:
  "\<lbrakk> Q = Q'; \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Q = Q'; \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>
theory Nondet_VCG

lemma hoare_post_eqE1:
  "\<lbrakk> Q = Q'; \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>,\<lbrace>E\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Q = Q'; \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>, \<lbrace>E\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>
theory Nondet_VCG

lemma hoare_post_eqE_R:
  "\<lbrakk> Q = Q'; \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>,- \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Q = Q'; \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>, -\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, -
theory Nondet_VCG

lemma pred_conj_apply_elim:
  "(\<lambda>rv. Q rv and Q' rv) = (\<lambda>rv s. Q rv s \<and> Q' rv s)" by (simp add: pred_conj_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<lambda>rv. Q rv and Q' rv) = (\<lambda>rv s. Q rv s \<and> Q' rv s)
theory Nondet_VCG

lemma pred_conj_conj_elim:
  "(\<lambda>rv s. (Q rv and Q' rv) s \<and> Q'' rv s) = (\<lambda>rv s. Q rv s \<and> Q' rv s \<and> Q'' rv s)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<lambda>rv s. (Q rv and Q' rv) s \<and> Q'' rv s) = (\<lambda>rv s. Q rv s \<and> Q' rv s \<and> Q'' rv s)
theory Nondet_VCG

lemma conj_assoc_apply:
  "(\<lambda>rv s. (Q rv s \<and> Q' rv s) \<and> Q'' rv s) = (\<lambda>rv s. Q rv s \<and> Q' rv s \<and> Q'' rv s)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<lambda>rv s. (Q rv s \<and> Q' rv s) \<and> Q'' rv s) = (\<lambda>rv s. Q rv s \<and> Q' rv s \<and> Q'' rv s)
theory Nondet_VCG

lemma all_elim:
  "(\<lambda>rv s. \<forall>x. P rv s) = P" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<lambda>rv s. \<forall>x. P rv s) = P
theory Nondet_VCG

lemma all_conj_elim:
  "(\<lambda>rv s. (\<forall>x. P rv s) \<and> Q rv s) = (\<lambda>rv s. P rv s \<and> Q rv s)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<lambda>rv s. (\<forall>x. P rv s) \<and> Q rv s) = (\<lambda>rv s. P rv s \<and> Q rv s)
theory Nondet_VCG

lemma if_apply_reduct:
  "\<lbrace>P\<rbrace> If P' (f x) (g x) \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> If P' f g x \<lbrace>Q\<rbrace>" by (cases P'; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> if P' then f x else g x \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> (if P' then f else g) x \<lbrace>Q\<rbrace>
theory Nondet_VCG

lemma if_apply_reductE:
  "\<lbrace>P\<rbrace> If P' (f x) (g x) \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> If P' f g x \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" by (cases P'; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> if P' then f x else g x \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> (if P' then f else g) x \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>
theory Nondet_VCG

lemma if_apply_reductE_R:
  "\<lbrace>P\<rbrace> If P' (f x) (g x) \<lbrace>Q\<rbrace>,- \<Longrightarrow> \<lbrace>P\<rbrace> If P' f g x \<lbrace>Q\<rbrace>,-" by (cases P'; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> if P' then f x else g x \<lbrace>Q\<rbrace>, - \<Longrightarrow> \<lbrace>P\<rbrace> (if P' then f else g) x \<lbrace>Q\<rbrace>, -
theory Nondet_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 Nondet_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 Nondet_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 Nondet_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>fst (f s). Q r s'); \<forall>s. \<not> R s \<and> P' s \<longrightarrow> (\<forall>(r, s')\<in>fst (f s). Q r s')\<rbrakk> \<Longrightarrow> \<forall>s. (P and P') s \<longrightarrow> (\<forall>(r, s')\<in>fst (f s). Q r s')
theory Nondet_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 Nondet_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>fst (f s). Q' r s'); \<And>s. P s \<Longrightarrow> P' s; \<forall>s. P s \<longrightarrow> (\<forall>(r, s')\<in>fst (f s). Q' r s' \<longrightarrow> Q r s')\<rbrakk> \<Longrightarrow> \<forall>s. P s \<longrightarrow> (\<forall>(r, s')\<in>fst (f s). Q r s')
theory Nondet_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 Nondet_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 Nondet_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 Nondet_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 Nondet_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 Nondet_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>fst (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>fst (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>fst (f s). case r of Inl e \<Rightarrow> E e s' | Inr r \<Rightarrow> (Q and R) r s')
theory Nondet_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>fst (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>fst (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>fst (f s). case r of Inl e \<Rightarrow> E e s' | Inr r \<Rightarrow> Q r s' \<and> R r s')
theory Nondet_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 Nondet_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 Nondet_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 Nondet_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 Nondet_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 Nondet_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> fst (?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 Nondet_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 Nondet_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 Nondet_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 Nondet_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)

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

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> put a \<lbrace>\<lambda>_ s. s = a\<rbrace>
theory Nondet_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)

(* 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 Nondet_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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> assert Q \<lbrace>\<lambda>_ s. P s \<and> Q\<rbrace>
theory Nondet_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)

(* 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 Nondet_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)

\<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 Nondet_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 Nondet_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 Nondet_No_Fail

lemma no_failD:
  "\<lbrakk> no_fail P m; P s \<rbrakk> \<Longrightarrow> \<not>(snd (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> snd (m s)
theory Nondet_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)