kings-crown/FVELER_Isabelle huggingface dataset:
theory Nondet_Total

lemma validE_NF_post_comb_conj:
  "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>!; \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>, \<lbrace>E\<rbrace>! \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> P' s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>, \<lbrace>E\<rbrace>!" unfolding validE_NF_alt_def validE_def validNF_def valid_def no_fail_def by (fastforce 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>Q'\<rbrace>, \<lbrace>E\<rbrace>!\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> P' s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' 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')) \<and> (\<forall>s. P s \<longrightarrow> \<not> snd (f 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> Q' r s')) \<and> (\<forall>s. P' s \<longrightarrow> \<not> snd (f s))\<rbrakk> \<Longrightarrow> (\<forall>s. P s \<and> 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> Q' r s')) \<and> (\<forall>s. P s \<and> P' s \<longrightarrow> \<not> snd (f s))
theory Nondet_Total

lemma validE_NF_chain:
  "\<lbrakk> \<lbrace>P'\<rbrace> a \<lbrace>R'\<rbrace>,\<lbrace>E'\<rbrace>!; \<And>s. P s \<Longrightarrow> P' s; \<And>r' s'. R' r' s' \<Longrightarrow> R r' s';
     \<And>r'' s''. E' r'' s'' \<Longrightarrow> E r'' s''\<rbrakk> \<Longrightarrow>
   \<lbrace>\<lambda>s. P s \<rbrace> a \<lbrace>\<lambda>r' s'. R r' s'\<rbrace>,\<lbrace>\<lambda>r'' s''. E r'' s''\<rbrace>!" by (fastforce simp: validE_NF_def validE_def2 no_fail_def Ball_def split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P'\<rbrace> a \<lbrace>R'\<rbrace>, \<lbrace>E'\<rbrace>!; \<And>s. P s \<Longrightarrow> P' s; \<And>r' s'. R' r' s' \<Longrightarrow> R r' s'; \<And>r'' s''. E' r'' s'' \<Longrightarrow> E r'' s''\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> a \<lbrace>R\<rbrace>, \<lbrace>E\<rbrace>!
theory Nondet_Total

lemma validE_NF_bind_wp[wp]:
  "\<lbrakk>\<And>x. \<lbrace>B x\<rbrace> g x \<lbrace>C\<rbrace>, \<lbrace>E\<rbrace>!; \<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>, \<lbrace>E\<rbrace>!\<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace> f >>=E (\<lambda>x. g x) \<lbrace>C\<rbrace>, \<lbrace>E\<rbrace>!" by (blast intro: validE_NF hoare_vcg_seqE no_fail_pre no_fail_bindE validE_validE_R validE_weaken
            elim!: validE_NFE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>x. \<lbrace>B x\<rbrace> g x \<lbrace>C\<rbrace>, \<lbrace>E\<rbrace>!; \<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>, \<lbrace>E\<rbrace>!\<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace> f >>=E g \<lbrace>C\<rbrace>, \<lbrace>E\<rbrace>!
theory Nondet_Total

lemma validNF_throwError[wp]:
  "\<lbrace>E e\<rbrace> throwError e \<lbrace>P\<rbrace>, \<lbrace>E\<rbrace>!" by (unfold validE_NF_alt_def throwError_def o_def) wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>E e\<rbrace> throwError e \<lbrace>P\<rbrace>, \<lbrace>E\<rbrace>!
theory Nondet_Total

lemma validNF_returnOk[wp]:
  "\<lbrace>P e\<rbrace> returnOk e \<lbrace>P\<rbrace>, \<lbrace>E\<rbrace>!" by (clarsimp simp: validE_NF_alt_def returnOk_def) wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P e\<rbrace> returnOk e \<lbrace>P\<rbrace>, \<lbrace>E\<rbrace>!
theory Nondet_Total

lemma validNF_whenE[wp]:
  "(P \<Longrightarrow> \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>, \<lbrace>E\<rbrace>!) \<Longrightarrow> \<lbrace>if P then Q else R ()\<rbrace> whenE P f \<lbrace>R\<rbrace>, \<lbrace>E\<rbrace>!" unfolding whenE_def by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P \<Longrightarrow> \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>, \<lbrace>E\<rbrace>!) \<Longrightarrow> \<lbrace>if P then Q else R ()\<rbrace> whenE P f \<lbrace>R\<rbrace>, \<lbrace>E\<rbrace>! proof (prove)
goal (1 subgoal):
 1. (P \<Longrightarrow> \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>, \<lbrace>E\<rbrace>!) \<Longrightarrow> \<lbrace>if P then Q else R ()\<rbrace> if P then f else returnOk () \<lbrace>R\<rbrace>, \<lbrace>E\<rbrace>!
theory Nondet_Total

lemma validNF_nobindE[wp]:
  "\<lbrakk> \<lbrace>B\<rbrace> g \<lbrace>C\<rbrace>,\<lbrace>E\<rbrace>!; \<lbrace>A\<rbrace> f \<lbrace>\<lambda>r s. B s\<rbrace>,\<lbrace>E\<rbrace>! \<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace> doE f; g odE \<lbrace>C\<rbrace>,\<lbrace>E\<rbrace>!" by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>B\<rbrace> g \<lbrace>C\<rbrace>, \<lbrace>E\<rbrace>!; \<lbrace>A\<rbrace> f \<lbrace>\<lambda>r. B\<rbrace>, \<lbrace>E\<rbrace>!\<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace> doE f;
g
odE \<lbrace>C\<rbrace>, \<lbrace>E\<rbrace>!
theory Nondet_Total

lemma validNF_cong:
  "\<lbrakk> \<And>s. P s = P' s; \<And>s. P s \<Longrightarrow> m s = m' s;
     \<And>r' s' s. \<lbrakk> P s; (r', s') \<in> fst (m s) \<rbrakk> \<Longrightarrow> Q r' s' = Q' r' s' \<rbrakk> \<Longrightarrow>
   (\<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>!) = (\<lbrace>P'\<rbrace> m' \<lbrace>Q'\<rbrace>!)" by (fastforce simp: validNF_alt_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. P s = P' s; \<And>s. P s \<Longrightarrow> m s = m' s; \<And>r' s' s. \<lbrakk>P s; (r', s') \<in> fst (m s)\<rbrakk> \<Longrightarrow> Q r' s' = Q' r' s'\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>! = \<lbrace>P'\<rbrace> m' \<lbrace>Q'\<rbrace>!
theory Nondet_Total

lemma validE_NF_liftE[wp]:
  "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>! \<Longrightarrow> \<lbrace>P\<rbrace> liftE f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>!" by (wpsimp simp: validE_NF_alt_def liftE_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>! \<Longrightarrow> \<lbrace>P\<rbrace> liftE f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>!
theory Nondet_Total

lemma validE_NF_handleE'[wp]:
  "\<lbrakk> \<And>x. \<lbrace>F x\<rbrace> handler x \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>!; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>F\<rbrace>! \<rbrakk> \<Longrightarrow>
   \<lbrace>P\<rbrace> f <handle2> (\<lambda>x. handler x) \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>!" unfolding validE_NF_alt_def handleE'_def apply (erule validNF_bind[rotated]) apply (clarsimp split: sum.splits) apply wpsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>x. \<lbrace>F x\<rbrace> handler x \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>!; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>F\<rbrace>!\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f <handle2> handler \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>x. \<lbrace>F x\<rbrace> handler x \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> Q r s\<rbrace>!; \<lbrace>P\<rbrace> f \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> F e s | Inr r \<Rightarrow> Q r s\<rbrace>!\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f >>= case_sum handler (\<lambda>v'. return (Inr v')) \<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. (\<And>x. \<lbrace>F x\<rbrace> handler x \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> Q r s\<rbrace>!) \<Longrightarrow> \<lbrace>\<lambda>s. case x of Inl e \<Rightarrow> F e s | Inr r \<Rightarrow> Q r s\<rbrace> case x of Inl x \<Rightarrow> handler x | Inr v' \<Rightarrow> return (Inr v') \<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>x2. (\<And>x. \<lbrace>F x\<rbrace> handler x \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> Q r s\<rbrace>!) \<Longrightarrow> \<lbrace>Q x2\<rbrace> return (Inr x2) \<lbrace>\<lambda>v s. (\<forall>x1. v = Inl x1 \<longrightarrow> E x1 s) \<and> (\<forall>x2. v = Inr x2 \<longrightarrow> Q x2 s)\<rbrace>! proof (prove)
goal:
No subgoals!
theory Nondet_Total

lemma validE_NF_handleE[wp]:
  "\<lbrakk> \<And>x. \<lbrace>F x\<rbrace> handler x \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>!; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>F\<rbrace>! \<rbrakk> \<Longrightarrow>
   \<lbrace>P\<rbrace> f <handle> handler \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>!" unfolding handleE_def by (metis validE_NF_handleE')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>x. \<lbrace>F x\<rbrace> handler x \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>!; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>F\<rbrace>!\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f <handle> handler \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>x. \<lbrace>F x\<rbrace> handler x \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>!; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>F\<rbrace>!\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f <handle2> handler \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>!
theory Nondet_Total

lemma validE_NF_condition[wp]:
  "\<lbrakk> \<lbrace> Q \<rbrace> A \<lbrace>P\<rbrace>,\<lbrace> E \<rbrace>!; \<lbrace> R \<rbrace> B \<lbrace>P\<rbrace>,\<lbrace> E \<rbrace>! \<rbrakk> \<Longrightarrow>
   \<lbrace>\<lambda>s. if C s then Q s else R s\<rbrace> condition C A B \<lbrace>P\<rbrace>,\<lbrace> E \<rbrace>!" by (erule validE_NFE)+ (wpsimp wp: validE_NF)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>Q\<rbrace> A \<lbrace>P\<rbrace>, \<lbrace>E\<rbrace>!; \<lbrace>R\<rbrace> B \<lbrace>P\<rbrace>, \<lbrace>E\<rbrace>!\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. if C s then Q s else R s\<rbrace> condition C
  A
  B \<lbrace>P\<rbrace>, \<lbrace>E\<rbrace>!
theory Nondet_Total

lemma hoare_assume_preNF:
  "(\<And>s. P s \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>!) \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>!" by (simp add: validNF_alt_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s. P s \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>!) \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>!
theory Nondet_Sat

lemma exs_valid_is_triple[wp_trip]:
  "exs_valid P f Q = triple_judgement P f (exs_postcondition Q (\<lambda>s f. fst (f s)))" by (simp add: triple_judgement_def exs_postcondition_def exs_valid_def)

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

lemma exs_hoare_post_imp:
  "\<lbrakk>\<And>r s. Q r s \<Longrightarrow> R r s; \<lbrace>P\<rbrace> a \<exists>\<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> a \<exists>\<lbrace>R\<rbrace>" unfolding exs_valid_def by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>r s. Q r s \<Longrightarrow> R r s; \<lbrace>P\<rbrace> a \<exists>\<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> a \<exists>\<lbrace>R\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>r s. Q r s \<Longrightarrow> R r s; \<forall>s. P s \<longrightarrow> (\<exists>(rv, s')\<in>fst (a s). Q rv s')\<rbrakk> \<Longrightarrow> \<forall>s. P s \<longrightarrow> (\<exists>(rv, s')\<in>fst (a s). R rv s')
theory Nondet_Sat

lemma use_exs_valid:
  "\<lbrakk> \<lbrace>P\<rbrace> f \<exists>\<lbrace>Q\<rbrace>; P s \<rbrakk> \<Longrightarrow> \<exists>(r, s') \<in> fst (f s). Q r s'" by (simp add: exs_valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace> f \<exists>\<lbrace>Q\<rbrace>; P s\<rbrakk> \<Longrightarrow> \<exists>(r, s')\<in>fst (f s). Q r s'
theory Nondet_Sat

lemma exs_valid_weaken_pre[wp_pre]:
  "\<lbrakk> \<lbrace>P'\<rbrace> f \<exists>\<lbrace>Q\<rbrace>; \<And>s. P s \<Longrightarrow> P' s \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<exists>\<lbrace>Q\<rbrace>" by (clarsimp simp: exs_valid_def)

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

lemma exs_valid_chain:
  "\<lbrakk> \<lbrace>P\<rbrace> f \<exists>\<lbrace>Q\<rbrace>; \<And>s. R s \<Longrightarrow> P s; \<And>r s. Q r s \<Longrightarrow> S r s \<rbrakk> \<Longrightarrow> \<lbrace>R\<rbrace> f \<exists>\<lbrace>S\<rbrace>" by (fastforce simp: exs_valid_def Bex_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace> f \<exists>\<lbrace>Q\<rbrace>; \<And>s. R s \<Longrightarrow> P s; \<And>r s. Q r s \<Longrightarrow> S r s\<rbrakk> \<Longrightarrow> \<lbrace>R\<rbrace> f \<exists>\<lbrace>S\<rbrace>
theory Nondet_Sat

lemma exs_valid_bind[wp_split]:
  "\<lbrakk> \<And>rv. \<lbrace>B rv\<rbrace> g rv \<exists>\<lbrace>C\<rbrace>; \<lbrace>A\<rbrace> f \<exists>\<lbrace>B\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace> f >>= (\<lambda>rv. g rv) \<exists>\<lbrace>C\<rbrace>" by (clarsimp simp: exs_valid_def bind_def')
     blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>rv. \<lbrace>B rv\<rbrace> g rv \<exists>\<lbrace>C\<rbrace>; \<lbrace>A\<rbrace> f \<exists>\<lbrace>B\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace> f >>= g \<exists>\<lbrace>C\<rbrace>
theory Nondet_Sat

lemma exs_valid_return[wp]:
  "\<lbrace>Q v\<rbrace> return v \<exists>\<lbrace>Q\<rbrace>" by (clarsimp simp: exs_valid_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>Q v\<rbrace> return v \<exists>\<lbrace>Q\<rbrace>
theory Nondet_Sat

lemma exs_valid_select[wp]:
  "\<lbrace>\<lambda>s. \<exists>r \<in> S. Q r s\<rbrace> select S \<exists>\<lbrace>Q\<rbrace>" by (clarsimp simp: exs_valid_def select_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<exists>r\<in>S. Q r s\<rbrace> select S \<exists>\<lbrace>Q\<rbrace>
theory Nondet_Sat

lemma exs_valid_alt[wp]:
  "\<lbrakk> \<lbrace>P\<rbrace> f \<exists>\<lbrace>Q\<rbrace>; \<lbrace>P'\<rbrace> g \<exists>\<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P or P'\<rbrace> f \<sqinter> g \<exists>\<lbrace>Q\<rbrace>" by (fastforce simp: exs_valid_def alternative_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace> f \<exists>\<lbrace>Q\<rbrace>; \<lbrace>P'\<rbrace> g \<exists>\<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P or P'\<rbrace> f \<sqinter> g \<exists>\<lbrace>Q\<rbrace>
theory Nondet_Sat

lemma exs_valid_get[wp]:
  "\<lbrace>\<lambda>s. Q s s\<rbrace> get \<exists>\<lbrace> Q \<rbrace>" by (clarsimp simp: exs_valid_def get_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. Q s s\<rbrace> get \<exists>\<lbrace>Q\<rbrace>
theory Nondet_Sat

lemma exs_valid_gets[wp]:
  "\<lbrace>\<lambda>s. Q (f s) s\<rbrace> gets f \<exists>\<lbrace>Q\<rbrace>" by (clarsimp simp: gets_def) wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. Q (f s) s\<rbrace> gets f \<exists>\<lbrace>Q\<rbrace>
theory Nondet_Sat

lemma exs_valid_fail[wp]:
  "\<lbrace>\<lambda>s. False\<rbrace> fail \<exists>\<lbrace>Q\<rbrace>" unfolding fail_def exs_valid_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. False\<rbrace> fail \<exists>\<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<forall>s. False \<longrightarrow> (\<exists>(rv, s')\<in>fst ({}, True). Q rv s')
theory Nondet_Sat

lemma exs_valid_assert[wp]:
  "\<lbrace>\<lambda>s. Q () s \<and> G\<rbrace> assert G \<exists>\<lbrace>Q\<rbrace>" unfolding assert_def by (wpsimp | rule conjI)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. Q () s \<and> G\<rbrace> assert G \<exists>\<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. Q () s \<and> G\<rbrace> if G then return () else fail \<exists>\<lbrace>Q\<rbrace>
theory Nondet_Sat

lemma exs_valid_state_assert[wp]:
  "\<lbrace>\<lambda>s. Q () s \<and> G s\<rbrace> state_assert G \<exists>\<lbrace>Q\<rbrace>" unfolding state_assert_def by wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. Q () s \<and> G s\<rbrace> state_assert G \<exists>\<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. Q () s \<and> G s\<rbrace> do s <- get;
assert (G s)
od \<exists>\<lbrace>Q\<rbrace>
theory Nondet_Sat

lemma exs_valid_condition[wp]:
  "\<lbrakk> \<lbrace>P\<rbrace> l \<exists>\<lbrace>Q\<rbrace>; \<lbrace>P'\<rbrace> r \<exists>\<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (C s \<and> P s) \<or> (\<not> C s \<and> P' s)\<rbrace> condition C l r \<exists>\<lbrace>Q\<rbrace>" by (clarsimp simp: condition_def exs_valid_def split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace> l \<exists>\<lbrace>Q\<rbrace>; \<lbrace>P'\<rbrace> r \<exists>\<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. C s \<and> P s \<or> \<not> C s \<and> P' s\<rbrace> condition C
  l
  r \<exists>\<lbrace>Q\<rbrace>
theory Nondet_Sat

lemma exs_valid_assert_opt[wp]:
  "\<lbrace>\<lambda>s. \<exists>x. G = Some x \<and> Q x s\<rbrace> assert_opt G \<exists>\<lbrace>Q\<rbrace>" by (clarsimp simp: assert_opt_def exs_valid_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<exists>x. G = Some x \<and> Q x s\<rbrace> assert_opt G \<exists>\<lbrace>Q\<rbrace>
theory Nondet_Sat

lemma gets_the_exs_valid[wp]:
  "\<lbrace>\<lambda>s. \<exists>x. h s = Some x \<and> Q x s\<rbrace> gets_the h \<exists>\<lbrace>Q\<rbrace>" by (wpsimp simp: gets_the_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<exists>x. h s = Some x \<and> Q x s\<rbrace> gets_the h \<exists>\<lbrace>Q\<rbrace>
theory Nondet_While_Loop_Rules

lemma in_measure'[simp, code_unfold]:
  "((x,y) \<in> measure' f) = (f x < f y)" by (simp add:measure'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((x, y) \<in> measure' f) = (f x < f y)
theory Nondet_While_Loop_Rules

lemma wf_measure'[iff]:
  "wf (measure' f)" apply (clarsimp simp: measure'_def) apply (insert wf_inv_image [OF wellorder_class.wf, where f=f]) apply (clarsimp simp: inv_image_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. wf (measure' f) proof (prove)
goal (1 subgoal):
 1. wf {(a, b). f a < f b} proof (prove)
goal (1 subgoal):
 1. wf (inv_image {(x, y). x < y} f) \<Longrightarrow> wf {(a, b). f a < f b} proof (prove)
goal:
No subgoals!
theory Nondet_While_Loop_Rules

lemma wf_wellorder_measure:
  "wf {(a, b). (M a :: 'a :: wellorder) < M b}" apply (subgoal_tac "wf (inv_image ({(a, b). a < b}) M)") apply (clarsimp simp: inv_image_def) apply (rule wf_inv_image) apply (rule wellorder_class.wf) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. wf {(a, b). M a < M b} proof (prove)
goal (2 subgoals):
 1. wf (inv_image {(a, b). a < b} M) \<Longrightarrow> wf {(a, b). M a < M b}
 2. wf (inv_image {(a, b). a < b} M) proof (prove)
goal (1 subgoal):
 1. wf (inv_image {(a, b). a < b} M) proof (prove)
goal (1 subgoal):
 1. wf {(a, b). a < b} proof (prove)
goal:
No subgoals!
theory Nondet_While_Loop_Rules

lemma whileLoop_add_inv:
  "whileLoop B C = (\<lambda>x. whileLoop_inv B C x I (measure' M))" by (clarsimp simp: whileLoop_inv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. whileLoop B
  C = (\<lambda>x. whileLoop_inv B C x I (measure' M))
theory Nondet_While_Loop_Rules

lemma whileLoopE_add_inv:
  "whileLoopE B C = (\<lambda>x. whileLoopE_inv B C x I (measure' M))" by (clarsimp simp: whileLoopE_inv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. whileLoopE B
  C = (\<lambda>x. whileLoopE_inv B C x I (measure' M))
theory Nondet_While_Loop_Rules

lemma whileLoop_terminates_unfold:
  "\<lbrakk> whileLoop_terminates C B r s; (r', s') \<in> fst (B r s); C r s \<rbrakk> \<Longrightarrow>
   whileLoop_terminates C B r' s'" by (force elim!: whileLoop_terminates.cases)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>whileLoop_terminates C B r s; (r', s') \<in> fst (B r s); C r s\<rbrakk> \<Longrightarrow> whileLoop_terminates C B r' s'
theory Nondet_While_Loop_Rules

lemma snd_whileLoop_first_step: "\<lbrakk> \<not> snd (whileLoop C B r s); C r s \<rbrakk> \<Longrightarrow> \<not> snd (B r s)" apply (subst (asm) whileLoop_unroll) apply (clarsimp simp: bind_def condition_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> snd (whileLoop C
  B r s); C r s\<rbrakk> \<Longrightarrow> \<not> snd (B r s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> snd (condition (C r)
  (B r >>= whileLoop C
  B)
  (return r) s); C r s\<rbrakk> \<Longrightarrow> \<not> snd (B r s) proof (prove)
goal:
No subgoals!
theory Nondet_While_Loop_Rules

lemma snd_whileLoopE_first_step: "\<lbrakk> \<not> snd (whileLoopE C B r s); C r s \<rbrakk> \<Longrightarrow> \<not> snd (B r s)" apply (subgoal_tac "\<lbrakk> \<not> snd (whileLoopE C B r s); C r s \<rbrakk> \<Longrightarrow> \<not> snd ((lift B (Inr r)) s)") apply (clarsimp simp: lift_def) apply (unfold whileLoopE_def) apply (erule snd_whileLoop_first_step) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> snd (whileLoopE C
  B r s); C r s\<rbrakk> \<Longrightarrow> \<not> snd (B r s) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<not> snd (whileLoopE C
  B r s); C r s; \<lbrakk>\<not> snd (whileLoopE C
  B r s); C r s\<rbrakk> \<Longrightarrow> \<not> snd (lift B (Inr r) s)\<rbrakk> \<Longrightarrow> \<not> snd (B r s)
 2. \<lbrakk>\<not> snd (whileLoopE C
  B r s); C r s; \<not> snd (whileLoopE C
  B r s); C r s\<rbrakk> \<Longrightarrow> \<not> snd (lift B (Inr r) s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> snd (whileLoopE C
  B r s); C r s; \<not> snd (whileLoopE C
  B r s); C r s\<rbrakk> \<Longrightarrow> \<not> snd (lift B (Inr r) s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> snd (whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift B) (Inr r) s); C r s; \<not> snd (whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift B) (Inr r) s); C r s\<rbrakk> \<Longrightarrow> \<not> snd (lift B (Inr r) s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>C r s; \<not> snd (whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift B) (Inr r) s); C r s\<rbrakk> \<Longrightarrow> case Inr r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s proof (prove)
goal:
No subgoals!
theory Nondet_While_Loop_Rules

lemma snd_whileLoop_unfold:
  "\<lbrakk> \<not> snd (whileLoop C B r s); C r s; (r', s') \<in> fst (B r s) \<rbrakk> \<Longrightarrow> \<not> snd (whileLoop C B r' s')" apply (clarsimp simp: whileLoop_def) apply (auto elim: whileLoop_results.cases whileLoop_terminates.cases
              intro: whileLoop_results.intros whileLoop_terminates.intros) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> snd (whileLoop C
  B r s); C r s; (r', s') \<in> fst (B r s)\<rbrakk> \<Longrightarrow> \<not> snd (whileLoop C
  B r' s') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>C r s; (r', s') \<in> fst (B r s); (Some (r, s), None) \<notin> whileLoop_results C B; whileLoop_terminates C B r s\<rbrakk> \<Longrightarrow> (Some (r', s'), None) \<notin> whileLoop_results C B \<and> whileLoop_terminates C B r' s' proof (prove)
goal:
No subgoals!