kings-crown/FVELER_Isabelle huggingface dataset:
theory Trace_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 Trace_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> mres (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> mres (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 Trace_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 Trace_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 Trace_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 Trace_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 Trace_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 Trace_Reader_Option

lemma ovalid_K_bind_wp[wp]:
  "ovalid P f Q \<Longrightarrow> ovalid P (K_bind f x) Q" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lblot>P\<rblot> f \<lblot>Q\<rblot> \<Longrightarrow> \<lblot>P\<rblot> K_bind f x \<lblot>Q\<rblot>
theory Trace_Reader_Option

lemma ovalidNF_K_bind_wp[wp]:
  "ovalidNF P f Q \<Longrightarrow> ovalidNF P (K_bind f x) Q" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ovalidNF P f Q \<Longrightarrow> ovalidNF P (K_bind f x) Q
theory Trace_Reader_Option

lemma no_ofail_K_bind[wp]:
  "no_ofail P f \<Longrightarrow> no_ofail P (K_bind f x)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_ofail P f \<Longrightarrow> no_ofail P (K_bind f x)
theory Trace_Reader_Option

lemma no_ofail_gets_the_eq:
  "no_ofail P f \<longleftrightarrow> no_fail P (gets_the (f :: ('s, 'a) lookup))" by (auto simp: no_ofail_def no_fail_def gets_the_def gets_def
                 get_def assert_opt_def bind_def return_def fail_def
         split: option.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_ofail P f = no_fail P (gets_the f)
theory Trace_Reader_Option

lemma ovalid_gets_the:
  "ovalid P f Q \<Longrightarrow> \<lbrace>P\<rbrace> gets_the f \<lbrace>Q\<rbrace>" apply wpsimp apply (fastforce dest: use_ovalid) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lblot>P\<rblot> f \<lblot>Q\<rblot> \<Longrightarrow> \<lbrace>P\<rbrace> gets_the f \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>\<lblot>P\<rblot> f \<lblot>Q\<rblot>; P s; f s = Some y\<rbrakk> \<Longrightarrow> Q y s proof (prove)
goal:
No subgoals!
theory Trace_Reader_Option

lemma gets_the_opt_map:
  "gets_the (f |> g) = do x \<leftarrow> gets_the f; assert_opt (g x) od" by (rule ext) (simp add: monad_simps opt_map_def split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. gets_the (f |> g) = do x <- gets_the f;
assert_opt (g x)
od
theory Trace_Reader_Option

lemma gets_the_opt_o:
  "gets_the (f |> Some o g) = do x \<leftarrow> gets_the f; return (g x) od" by (simp add: gets_the_opt_map assert_opt_Some)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. gets_the (f ||> g) = do x <- gets_the f;
return (g x)
od
theory Trace_Reader_Option

lemma gets_the_obind:
  "gets_the (f |>> g) = gets_the f >>= (\<lambda>x. gets_the (g x))" by (rule ext) (simp add: monad_simps obind_def split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. gets_the (f >>= g) = do x <- gets_the f;
gets_the (g x)
od
theory Trace_Reader_Option

lemma gets_the_return:
  "gets_the (oreturn x) = return x" by (simp add: monad_simps oreturn_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. gets_the (oreturn x) = return x
theory Trace_Reader_Option

lemma gets_the_fail:
  "gets_the ofail = fail" by (simp add: monad_simps ofail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. gets_the ofail = fail
theory Trace_Reader_Option

lemma gets_the_ogets:
  "gets_the (ogets s) = gets s" by (clarsimp simp: monad_simps ogets_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. gets_the (ogets s) = gets s
theory Trace_Reader_Option

lemma gets_the_returnOk:
  "gets_the (oreturnOk x) = returnOk x" by (simp add: monad_simps oreturnOk_def returnOk_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. gets_the (oreturnOk x) = returnOk x
theory Trace_Reader_Option

lemma gets_the_assert:
  "gets_the (oassert P) = assert P" by (simp add: oassert_def assert_def gets_the_fail gets_the_return)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. gets_the (oassert P) = assert P
theory Trace_Reader_Option

lemma gets_the_assert_opt:
  "gets_the (oassert_opt P) = assert_opt P" by (simp add: oassert_opt_def assert_opt_def gets_the_return gets_the_fail split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. gets_the (oassert_opt P) = assert_opt P
theory Trace_Reader_Option

lemma gets_the_if_distrib:
  "gets_the (if P then f else g) = (if P then gets_the f else gets_the g)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. gets_the (if P then f else g) = (if P then gets_the f else gets_the g)
theory Trace_Reader_Option

lemma gets_the_oapply_comp:
  "gets_the (oapply x \<circ> f) = gets_map f x" by (fastforce simp: gets_map_def gets_the_def o_def gets_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. gets_the (oapply x \<circ> f) = gets_map f x
theory Trace_Reader_Option

lemma gets_the_Some:
  "gets_the (\<lambda>_. Some x) = return x" by (simp add: gets_the_def assert_opt_Some)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. gets_the (\<lambda>_. Some x) = return x
theory Trace_Reader_Option

lemma gets_the_oapply2_comp:
  "gets_the (oapply2 y x \<circ> f) = gets_map (swp f y) x" by (clarsimp simp: gets_map_def gets_the_def o_def gets_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. gets_the (oapply2 y x \<circ> f) = gets_map (swp f y) x
theory Trace_Reader_Option

lemma mres_assert_opt:
  "mres (assert_opt opt s) = (if opt = None then {} else {(the opt,s)})" by (clarsimp simp: assert_opt_def fail_def return_def mres_def vimage_def split: option.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mres (assert_opt opt s) = (if opt = None then {} else {(the opt, s)})
theory Trace_Reader_Option

lemma gets_the_conv:
  "(gets_the B s) = (case B s of Some r' \<Rightarrow> ({([], Result (r', s))}) | _ \<Rightarrow> {([], Failed)})" by (auto simp: gets_the_def gets_def get_def bind_def return_def fail_def assert_opt_def split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. gets_the B s = (case B s of None \<Rightarrow> {([], Failed)} | Some r' \<Rightarrow> {([], Result (r', s))})
theory Trace_Reader_Option

lemma The_eqD:
  "\<lbrakk>The P = x; \<exists>!x. P x\<rbrakk> \<Longrightarrow> P x" by (metis theI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>The P = x; \<exists>!x. P x\<rbrakk> \<Longrightarrow> P x
theory Trace_Sat

lemma exs_valid_is_triple[wp_trip]:
  "exs_valid P f Q = triple_judgement P f (exs_postcondition Q (\<lambda>s f. mres (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. mres (f s)))
theory Trace_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>mres (a s). Q rv s')\<rbrakk> \<Longrightarrow> \<forall>s. P s \<longrightarrow> (\<exists>(rv, s')\<in>mres (a s). R rv s')
theory Trace_Sat

lemma use_exs_valid:
  "\<lbrakk> \<lbrace>P\<rbrace> f \<exists>\<lbrace>Q\<rbrace>; P s \<rbrakk> \<Longrightarrow> \<exists>(r, s') \<in> mres (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>mres (f s). Q r s'
theory Trace_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 Trace_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 Trace_Sat

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

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

lemma exs_valid_select[wp]:
  "\<lbrace>\<lambda>s. \<exists>r \<in> S. Q r s\<rbrace> select S \<exists>\<lbrace>Q\<rbrace>" by (auto simp: exs_valid_def select_def mres_def image_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 Trace_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 mres_def image_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 Trace_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 mres_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. Q s s\<rbrace> get \<exists>\<lbrace>Q\<rbrace>
theory Trace_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 Trace_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>mres {([], Failed)}. Q rv s')
theory Trace_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 Trace_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 Trace_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 Trace_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 mres_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 Trace_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 Strengthen_Demo

lemma predt_double_mono:
  assumes PQ: "\<And>x y. P x y \<longrightarrow> Q x y"
  assumes P: "predt f g h (predt f g h' P) x y"
  shows "predt f g h (predt f g h' Q) x y" using P apply (simp add: predt_def) apply (strengthen PQ) apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. predt f g h (predt f g h' Q) x y proof (prove)
using this:
predt f g h (predt f g h' P) x y

goal (1 subgoal):
 1. predt f g h (predt f g h' Q) x y proof (prove)
goal (1 subgoal):
 1. \<exists>x'. (\<exists>y'\<in>f y. x' \<in> g y' ` h y) \<and> (\<exists>x'a. (\<exists>y'\<in>f x'. x'a \<in> g y' ` h' x') \<and> P x x'a) \<Longrightarrow> \<exists>x'. (\<exists>y'\<in>f y. x' \<in> g y' ` h y) \<and> (\<exists>x'a. (\<exists>y'\<in>f x'. x'a \<in> g y' ` h' x') \<and> Q x x'a) proof (prove)
goal (1 subgoal):
 1. \<exists>x'. (\<exists>y'\<in>f y. x' \<in> g y' ` h y) \<and> (\<exists>x'a. (\<exists>y'\<in>f x'. x'a \<in> g y' ` h' x') \<and> P x x'a) \<Longrightarrow> \<exists>xa. (\<exists>y'\<in>f y. xa \<in> g y' ` h y) \<and> (\<exists>xb. (\<exists>y'\<in>f xa. xb \<in> g y' ` h' xa) \<and> P x xb) proof (prove)
goal:
No subgoals!
theory Strengthen_Demo

lemma predt_double_mono2:
  assumes PQ: "\<And>x y. P x y \<longrightarrow> Q x y"
  assumes P: "predt f g h (predt f g' h P) x y"
  shows "predt f g h (predt f g' h Q) x y" using P apply (clarsimp simp: predt_def) apply (strengthen bexI[mk_strg I _ A]) apply (strengthen image_eqI[mk_strg I _ A]) apply simp apply (strengthen bexI[mk_strg I _ O], assumption) apply (strengthen image_eqI[mk_strg I _ E]) apply simp apply (simp add: PQ) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. predt f g h (predt f g' h Q) x y proof (prove)
using this:
predt f g h (predt f g' h P) x y

goal (1 subgoal):
 1. predt f g h (predt f g' h Q) x y proof (prove)
goal (1 subgoal):
 1. \<And>y' xa y'a xaa. \<lbrakk>y' \<in> f y; xa \<in> h y; P x (g' y'a xaa); y'a \<in> f (g y' xa); xaa \<in> h (g y' xa)\<rbrakk> \<Longrightarrow> \<exists>x'. (\<exists>y'\<in>f y. x' \<in> g y' ` h y) \<and> (\<exists>x'a. (\<exists>y'\<in>f x'. x'a \<in> g' y' ` h x') \<and> Q x x'a) proof (prove)
goal (1 subgoal):
 1. \<And>y' xa y'a xaa. \<lbrakk>y' \<in> f y; xa \<in> h y; P x (g' y'a xaa); y'a \<in> f (g y' xa); xaa \<in> h (g y' xa)\<rbrakk> \<Longrightarrow> \<exists>xa. xa \<in> g y' ` h y \<and> (\<exists>x'. (\<exists>y'\<in>f xa. x' \<in> g' y' ` h xa) \<and> Q x x') proof (prove)
goal (1 subgoal):
 1. \<And>y' xa y'a xaa. \<lbrakk>y' \<in> f y; xa \<in> h y; P x (g' y'a xaa); y'a \<in> f (g y' xa); xaa \<in> h (g y' xa)\<rbrakk> \<Longrightarrow> \<exists>xb. xb = g y' xa \<and> (\<exists>x'. (\<exists>y'\<in>f xb. x' \<in> g' y' ` h xb) \<and> Q x x') proof (prove)
goal (1 subgoal):
 1. \<And>y' xa y'a xaa. \<lbrakk>y' \<in> f y; xa \<in> h y; P x (g' y'a xaa); y'a \<in> f (g y' xa); xaa \<in> h (g y' xa)\<rbrakk> \<Longrightarrow> \<exists>x'. (\<exists>y'a\<in>f (g y' xa). x' \<in> g' y'a ` h (g y' xa)) \<and> Q x x' proof (prove)
goal (1 subgoal):
 1. \<And>y' xa y'a xaa. \<lbrakk>y' \<in> f y; xa \<in> h y; P x (g' y'a xaa); y'a \<in> f (g y' xa); xaa \<in> h (g y' xa)\<rbrakk> \<Longrightarrow> \<exists>xb. xb \<in> g' y'a ` h (g y' xa) \<and> Q x xb proof (prove)
goal (1 subgoal):
 1. \<And>y' xa y'a xaa. \<lbrakk>y' \<in> f y; xa \<in> h y; P x (g' y'a xaa); y'a \<in> f (g y' xa); xaa \<in> h (g y' xa)\<rbrakk> \<Longrightarrow> \<exists>xa. xa = g' y'a xaa \<and> Q x xa proof (prove)
goal (1 subgoal):
 1. \<And>y' xa y'a xaa. \<lbrakk>y' \<in> f y; xa \<in> h y; P x (g' y'a xaa); y'a \<in> f (g y' xa); xaa \<in> h (g y' xa)\<rbrakk> \<Longrightarrow> Q x (g' y'a xaa) proof (prove)
goal:
No subgoals!
theory Examples

lemma "(27 :: 4 word) = -5" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 27 = - 5
theory Examples

lemma "(27 :: 4 word) = 11" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 27 = 11
theory Examples

lemma "27 \<noteq> (11 :: 6 word)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 27 \<noteq> 11
theory Examples

lemma "(127 :: 6 word) = -1" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 127 = - 1
theory Examples

lemma "word_pred 2 = 1" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. word_pred 2 = 1
theory Examples

lemma "word_succ (- 3) = -2" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. word_succ (- 3) = - 2
theory Examples

lemma "23 < (27::8 word)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 23 < 27
theory Examples

lemma "23 \<le> (27::8 word)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 23 \<le> 27