kings-crown/FVELER_Isabelle huggingface dataset:
theory Nondet_While_Loop_Rules

lemma validNF_whileLoopE_inv [wp]:
  assumes inv: "\<And>r s. \<lbrace>\<lambda>s'. I r s' \<and> C r s' \<and> s' = s \<rbrace> B r \<lbrace> \<lambda>r' s'. I r' s' \<and> ((r', s'), (r, s)) \<in> R \<rbrace>,\<lbrace> E \<rbrace>!"
  and wf_R: "wf R"
  and post_cond: "\<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s"
  shows "\<lbrace>I r\<rbrace> whileLoopE_inv C B r I R \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>!" apply (clarsimp simp: whileLoopE_inv_def) apply (metis validNF_whileLoopE [OF _ inv] post_cond wf_R) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>I r\<rbrace> whileLoopE_inv C B r I R \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<lbrace>I r\<rbrace> whileLoopE C
  B r \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>! proof (prove)
goal:
No subgoals!
theory Nondet_While_Loop_Rules

lemma validNF_whileLoopE_inv_measure [wp]:
  assumes inv: "\<And>r s. \<lbrace>\<lambda>s'. I r s' \<and> C r s' \<and> s' = s \<rbrace> B r \<lbrace> \<lambda>r' s'. I r' s' \<and> M r' s' < M r s \<rbrace>, \<lbrace> E \<rbrace>!"
  and post_cond: "\<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s"
  shows "\<lbrace>I r\<rbrace> whileLoopE_inv C B r I (measure' (\<lambda>(r, s). M r s)) \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>!" apply (rule validNF_whileLoopE_inv) apply clarsimp apply (rule inv) apply clarsimp apply (metis post_cond) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>I r\<rbrace> whileLoopE_inv C B r I (measure' (\<lambda>(r, s). M r s)) \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>! proof (prove)
goal (3 subgoals):
 1. \<And>r s. \<lbrace>\<lambda>s'. I r s' \<and> C r s' \<and> s' = s\<rbrace> B r \<lbrace>\<lambda>r' s'. I r' s' \<and> ((r', s'), r, s) \<in> measure' (\<lambda>a. case a of (r, s) \<Rightarrow> M r s)\<rbrace>, \<lbrace>E\<rbrace>!
 2. wf (measure' (\<lambda>a. case a of (r, s) \<Rightarrow> M r s))
 3. \<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s proof (prove)
goal (3 subgoals):
 1. \<And>r s. \<lbrace>\<lambda>s'. I r s' \<and> C r s' \<and> s' = s\<rbrace> B r \<lbrace>\<lambda>r' s'. I r' s' \<and> M r' s' < M r s\<rbrace>, \<lbrace>E\<rbrace>!
 2. wf (measure' (\<lambda>a. case a of (r, s) \<Rightarrow> M r s))
 3. \<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s proof (prove)
goal (2 subgoals):
 1. wf (measure' (\<lambda>a. case a of (r, s) \<Rightarrow> M r s))
 2. \<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s proof (prove)
goal (1 subgoal):
 1. \<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s proof (prove)
goal:
No subgoals!
theory Nondet_While_Loop_Rules

lemma validNF_whileLoopE_inv_measure_twosteps:
  assumes inv: "\<And>r. \<lbrace>\<lambda>s'. I r s' \<and> C r s' \<rbrace> B r \<lbrace> \<lambda>r' s'. I r' s' \<rbrace>, \<lbrace> E \<rbrace>!"
  assumes measure: "\<And>r m. \<lbrace>\<lambda>s. I r s \<and> C r s \<and> M r s = m \<rbrace> B r \<lbrace> \<lambda>r' s'. M r' s' < m \<rbrace>, \<lbrace> \<lambda>_ _. True \<rbrace>"
  and post_cond: "\<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s"
  shows "\<lbrace>I r\<rbrace> whileLoopE_inv C B r I (measure' (\<lambda>(r, s). M r s)) \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>!" apply (rule validNF_whileLoopE_inv_measure) apply (rule validE_NF_weaken_pre) apply (rule validE_NF_post_comb_conj_L) apply (rule inv) apply (rule measure) apply fast apply (metis post_cond) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>I r\<rbrace> whileLoopE_inv C B r I (measure' (\<lambda>(r, s). M r s)) \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>! proof (prove)
goal (2 subgoals):
 1. \<And>r s. \<lbrace>\<lambda>s'. I r s' \<and> C r s' \<and> s' = s\<rbrace> B r \<lbrace>\<lambda>r' s'. I r' s' \<and> M r' s' < M r s\<rbrace>, \<lbrace>E\<rbrace>!
 2. \<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s proof (prove)
goal (3 subgoals):
 1. \<And>r s. \<lbrace>?Q3 r s\<rbrace> B r \<lbrace>\<lambda>r' s'. I r' s' \<and> M r' s' < M r s\<rbrace>, \<lbrace>E\<rbrace>!
 2. \<And>r s sa. I r sa \<and> C r sa \<and> sa = s \<Longrightarrow> ?Q3 r s sa
 3. \<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s proof (prove)
goal (4 subgoals):
 1. \<And>r s. \<lbrace>?P6 r s\<rbrace> B r \<lbrace>I\<rbrace>, \<lbrace>E\<rbrace>!
 2. \<And>r s. \<lbrace>?P'6 r s\<rbrace> B r \<lbrace>\<lambda>rv sa. M rv sa < M r s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>r s sa. I r sa \<and> C r sa \<and> sa = s \<Longrightarrow> ?P6 r s sa \<and> ?P'6 r s sa
 4. \<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s proof (prove)
goal (3 subgoals):
 1. \<And>r s. \<lbrace>?P'6 r s\<rbrace> B r \<lbrace>\<lambda>rv sa. M rv sa < M r s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>r s sa. I r sa \<and> C r sa \<and> sa = s \<Longrightarrow> (I r sa \<and> C r sa) \<and> ?P'6 r s sa
 3. \<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s proof (prove)
goal (2 subgoals):
 1. \<And>r s sa. I r sa \<and> C r sa \<and> sa = s \<Longrightarrow> (I r sa \<and> C r sa) \<and> I r sa \<and> C r sa \<and> M r sa = M r s
 2. \<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s proof (prove)
goal (1 subgoal):
 1. \<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s proof (prove)
goal:
No subgoals!
theory Nondet_While_Loop_Rules

lemma whileLoopE_wp_inv [wp]:
  "\<lbrakk> \<And>r. \<lbrace>\<lambda>s. I r s \<and> C r s\<rbrace> B r \<lbrace>I\<rbrace>,\<lbrace>E\<rbrace>; \<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s \<rbrakk>
      \<Longrightarrow> \<lbrace> I r \<rbrace> whileLoopE_inv C B r I M \<lbrace> Q \<rbrace>,\<lbrace> E \<rbrace>" apply (clarsimp simp: whileLoopE_inv_def) apply (rule validE_whileLoopE [where I=I], auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>r. \<lbrace>\<lambda>s. I r s \<and> C r s\<rbrace> B r \<lbrace>I\<rbrace>, \<lbrace>E\<rbrace>; \<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s\<rbrakk> \<Longrightarrow> \<lbrace>I r\<rbrace> whileLoopE_inv C B r I M \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>r. \<lbrace>\<lambda>s. I r s \<and> C r s\<rbrace> B r \<lbrace>I\<rbrace>, \<lbrace>E\<rbrace>; \<And>r s. \<lbrakk>I r s; \<not> C r s\<rbrakk> \<Longrightarrow> Q r s\<rbrakk> \<Longrightarrow> \<lbrace>I r\<rbrace> whileLoopE C
  B r \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal:
No subgoals!
theory Nondet_While_Loop_Rules

lemma whileLoop_rule_strong_no_fail:
  assumes init_U: "\<lbrace> \<lambda>s'. s' = s \<rbrace> whileLoop C B r \<lbrace> \<lambda>r s. (r, s) \<in> fst Q \<rbrace>!"
  and path_exists: "\<And>r'' s''. \<lbrakk> (r'', s'') \<in> fst Q \<rbrakk> \<Longrightarrow> \<lbrace> \<lambda>s'. s' = s \<rbrace> whileLoop C B r \<exists>\<lbrace> \<lambda>r s. r = r'' \<and> s = s'' \<rbrace>"
  and loop_no_fail: "\<not> snd Q"
  shows "whileLoop C B r s = Q" apply (rule whileLoop_rule_strong) apply (metis init_U validNF_valid) apply (metis path_exists) apply (metis loop_no_fail) apply (metis (lifting, no_types) init_U validNF_chain) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. whileLoop C
  B r s = Q proof (prove)
goal (4 subgoals):
 1. \<lbrace>\<lambda>s'. s' = s\<rbrace> whileLoop C
  B r \<lbrace>\<lambda>r s. (r, s) \<in> fst Q\<rbrace>
 2. \<And>r'' s''. (r'', s'') \<in> fst Q \<Longrightarrow> \<lbrace>\<lambda>s'. s' = s\<rbrace> whileLoop C
  B r \<exists>\<lbrace>\<lambda>r s. r = r'' \<and> s = s''\<rbrace>
 3. snd Q \<Longrightarrow> snd (whileLoop C
  B r s)
 4. \<not> snd Q \<Longrightarrow> \<lbrace>\<lambda>s'. s' = s\<rbrace> whileLoop C
  B r \<lbrace>\<lambda>_ _. True\<rbrace>! proof (prove)
goal (3 subgoals):
 1. \<And>r'' s''. (r'', s'') \<in> fst Q \<Longrightarrow> \<lbrace>\<lambda>s'. s' = s\<rbrace> whileLoop C
  B r \<exists>\<lbrace>\<lambda>r s. r = r'' \<and> s = s''\<rbrace>
 2. snd Q \<Longrightarrow> snd (whileLoop C
  B r s)
 3. \<not> snd Q \<Longrightarrow> \<lbrace>\<lambda>s'. s' = s\<rbrace> whileLoop C
  B r \<lbrace>\<lambda>_ _. True\<rbrace>! proof (prove)
goal (2 subgoals):
 1. snd Q \<Longrightarrow> snd (whileLoop C
  B r s)
 2. \<not> snd Q \<Longrightarrow> \<lbrace>\<lambda>s'. s' = s\<rbrace> whileLoop C
  B r \<lbrace>\<lambda>_ _. True\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<not> snd Q \<Longrightarrow> \<lbrace>\<lambda>s'. s' = s\<rbrace> whileLoop C
  B r \<lbrace>\<lambda>_ _. True\<rbrace>! proof (prove)
goal:
No subgoals!
theory Nondet_While_Loop_Rules

lemma whileM_wp_gen:
  assumes termin:"\<And>s. I False s \<Longrightarrow> Q s"
  assumes [wp]: "\<lbrace>I'\<rbrace> C \<lbrace>I\<rbrace>"
  assumes [wp]: "\<lbrace>I True\<rbrace> f \<lbrace>\<lambda>_. I'\<rbrace>"
  shows "\<lbrace>I'\<rbrace> whileM C f \<lbrace>\<lambda>_. Q\<rbrace>" unfolding whileM_def using termin by (wpsimp wp: whileLoop_wp[where I=I])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>I'\<rbrace> whileM C f \<lbrace>\<lambda>_. Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>I'\<rbrace> do c <- C;
whileLoop (\<lambda>c s. c)
  (\<lambda>_. do f;
C
od) c;
return ()
od \<lbrace>\<lambda>_. Q\<rbrace> proof (prove)
using this:
I False ?s \<Longrightarrow> Q ?s

goal (1 subgoal):
 1. \<lbrace>I'\<rbrace> do c <- C;
whileLoop (\<lambda>c s. c)
  (\<lambda>_. do f;
C
od) c;
return ()
od \<lbrace>\<lambda>_. Q\<rbrace>
theory Nondet_While_Loop_Rules

lemma whileM_inv:
  "\<lbrakk>f \<lbrace>Q\<rbrace>; P \<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow> whileM P f \<lbrace>Q\<rbrace>" by (fastforce intro: whileM_wp_gen)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>Q\<rbrace> f \<lbrace>\<lambda>_. Q\<rbrace>; \<lbrace>Q\<rbrace> P \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>Q\<rbrace> whileM P f \<lbrace>\<lambda>_. Q\<rbrace>
theory Nondet_No_Throw

lemma no_throw_def':
  "no_throw P A = (\<forall>s. P s \<longrightarrow> (\<forall>(r, t) \<in> fst (A s). (\<exists>x. r = Inr x)))" by (clarsimp simp: no_throw_def validE_def2 split_def split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_throw P A = (\<forall>s. P s \<longrightarrow> (\<forall>(r, t)\<in>fst (A s). \<exists>x. r = Inr x))
theory Nondet_No_Throw

lemma no_throw_returnOk[simp]:
  "no_throw P (returnOk a)" unfolding no_throw_def by wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_throw P (returnOk a) proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> returnOk a \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_ _. False\<rbrace>
theory Nondet_No_Throw

lemma no_throw_liftE[simp]:
  "no_throw P (liftE x)" by (wpsimp simp: liftE_def no_throw_def validE_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_throw P (liftE x)
theory Nondet_No_Throw

lemma no_throw_bindE:
  "\<lbrakk> no_throw A X; \<And>a. no_throw B (Y a); \<lbrace> A \<rbrace> X \<lbrace> \<lambda>_. B \<rbrace>,\<lbrace> \<lambda>_ _. True \<rbrace> \<rbrakk>
   \<Longrightarrow> no_throw A (X >>=E Y)" unfolding no_throw_def using hoare_validE_cases seqE by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_throw A X; \<And>a. no_throw B (Y a); \<lbrace>A\<rbrace> X \<lbrace>\<lambda>_. B\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>\<rbrakk> \<Longrightarrow> no_throw A (X >>=E Y) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>A\<rbrace> X \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_ _. False\<rbrace>; \<And>a. \<lbrace>B\<rbrace> Y a \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_ _. False\<rbrace>; \<lbrace>A\<rbrace> X \<lbrace>\<lambda>_. B\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace> X >>=E Y \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_ _. False\<rbrace> proof (prove)
using this:
\<lbrakk>\<lbrace>?P\<rbrace> ?f \<lbrace>?Q\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>; \<lbrace>?P\<rbrace> ?f \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?R\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?P\<rbrace> ?f \<lbrace>?Q\<rbrace>, \<lbrace>?R\<rbrace>
\<lbrakk>\<lbrace>?A\<rbrace> ?f \<lbrace>?B\<rbrace>, \<lbrace>?E\<rbrace>; \<And>x. \<lbrace>?B x\<rbrace> ?g x \<lbrace>?C\<rbrace>, \<lbrace>?E\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?A\<rbrace> ?f >>=E ?g \<lbrace>?C\<rbrace>, \<lbrace>?E\<rbrace>

goal (1 subgoal):
 1. \<lbrakk>\<lbrace>A\<rbrace> X \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_ _. False\<rbrace>; \<And>a. \<lbrace>B\<rbrace> Y a \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_ _. False\<rbrace>; \<lbrace>A\<rbrace> X \<lbrace>\<lambda>_. B\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace> X >>=E Y \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_ _. False\<rbrace>
theory Nondet_No_Throw

lemma no_throw_bindE_simple:
  "\<lbrakk> no_throw \<top> L; \<And>x. no_throw \<top> (R x) \<rbrakk> \<Longrightarrow> no_throw \<top> (L >>=E R)" using hoareE_TrueI no_throw_bindE by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_throw (\<lambda>_. True) L; \<And>x. no_throw (\<lambda>_. True) (R x)\<rbrakk> \<Longrightarrow> no_throw (\<lambda>_. True) (L >>=E R) proof (prove)
using this:
\<lbrace>?P\<rbrace> ?f \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>r _. True\<rbrace>
\<lbrakk>no_throw ?A ?X; \<And>a. no_throw ?B (?Y a); \<lbrace>?A\<rbrace> ?X \<lbrace>\<lambda>_. ?B\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>\<rbrakk> \<Longrightarrow> no_throw ?A (?X >>=E ?Y)

goal (1 subgoal):
 1. \<lbrakk>no_throw (\<lambda>_. True) L; \<And>x. no_throw (\<lambda>_. True) (R x)\<rbrakk> \<Longrightarrow> no_throw (\<lambda>_. True) (L >>=E R)
theory Nondet_No_Throw

lemma no_throw_handleE_simple:
  "\<lbrakk> \<And>x. no_throw \<top> L \<or> no_throw \<top> (R x) \<rbrakk> \<Longrightarrow> no_throw \<top> (L <handle> R)" by (fastforce simp: no_throw_def' handleE_def handleE'_def validE_def valid_def bind_def return_def
                split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. no_throw (\<lambda>_. True) L \<or> no_throw (\<lambda>_. True) (R x)) \<Longrightarrow> no_throw (\<lambda>_. True) (L <handle> R)
theory Nondet_No_Throw

lemma no_throw_handle2:
  "\<lbrakk> \<And>a. no_throw Y (B a); \<lbrace> X \<rbrace> A \<lbrace> \<lambda>_ _. True \<rbrace>,\<lbrace> \<lambda>_. Y \<rbrace> \<rbrakk> \<Longrightarrow> no_throw X (A <handle2> B)" by (fastforce simp: no_throw_def' handleE'_def validE_def valid_def bind_def return_def
                split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>a. no_throw Y (B a); \<lbrace>X\<rbrace> A \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_. Y\<rbrace>\<rbrakk> \<Longrightarrow> no_throw X (A <handle2> B)
theory Nondet_No_Throw

lemma no_throw_handle:
  "\<lbrakk> \<And>a. no_throw Y (B a); \<lbrace> X \<rbrace> A \<lbrace> \<lambda>_ _. True \<rbrace>,\<lbrace> \<lambda>_. Y \<rbrace> \<rbrakk> \<Longrightarrow> no_throw X (A <handle> B)" unfolding handleE_def by (rule no_throw_handle2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>a. no_throw Y (B a); \<lbrace>X\<rbrace> A \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_. Y\<rbrace>\<rbrakk> \<Longrightarrow> no_throw X (A <handle> B) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>a. no_throw Y (B a); \<lbrace>X\<rbrace> A \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_. Y\<rbrace>\<rbrakk> \<Longrightarrow> no_throw X (A <handle2> B)
theory Nondet_No_Throw

lemma no_throw_fail[simp]:
  "no_throw P fail" by (clarsimp simp: no_throw_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_throw P fail
theory Nondet_No_Throw

lemma bindE_fail_propagates:
  "\<lbrakk> no_throw \<top> A; empty_fail A \<rbrakk> \<Longrightarrow> A >>=E (\<lambda>_. fail) = fail" by (fastforce simp: no_throw_def validE_def valid_def bind_def empty_fail_def
                      bindE_def split_def fail_def Nondet_Monad.lift_def throwError_def
                split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_throw (\<lambda>_. True) A; empty_fail A\<rbrakk> \<Longrightarrow> doE _ <- A;
fail
odE = fail
theory Nondet_No_Throw

lemma whileLoopE_nothrow:
  "\<lbrakk> \<And>x. no_throw \<top> (B x) \<rbrakk> \<Longrightarrow> no_throw \<top> (whileLoopE C B x)" unfolding no_throw_def by (fastforce intro!: validE_whileLoopE intro: validE_weaken)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. no_throw (\<lambda>_. True) (B x)) \<Longrightarrow> no_throw (\<lambda>_. True) (whileLoopE C
  B x) proof (prove)
goal (1 subgoal):
 1. (\<And>x. \<lbrace>\<lambda>_. True\<rbrace> B x \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_ _. False\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> whileLoopE C
  B x \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_ _. False\<rbrace>
theory Nondet_No_Throw

lemma handleE'_nothrow_lhs:
  "no_throw \<top> L \<Longrightarrow> no_throw \<top> (L <handle2> R)" unfolding no_throw_def using handleE'_wp[rotated] by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_throw (\<lambda>_. True) L \<Longrightarrow> no_throw (\<lambda>_. True) (L <handle2> R) proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> L \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_ _. False\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> L <handle2> R \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_ _. False\<rbrace> proof (prove)
using this:
\<lbrakk>\<lbrace>?P\<rbrace> ?f \<lbrace>?Q\<rbrace>, \<lbrace>?F\<rbrace>; \<And>x. \<lbrace>?F x\<rbrace> ?handler x \<lbrace>?Q\<rbrace>, \<lbrace>?E\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?P\<rbrace> ?f <handle2> ?handler \<lbrace>?Q\<rbrace>, \<lbrace>?E\<rbrace>

goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> L \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_ _. False\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> L <handle2> R \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_ _. False\<rbrace>
theory Nondet_No_Throw

lemma handleE'_nothrow_rhs:
  "\<lbrakk> \<And>x. no_throw \<top> (R x) \<rbrakk> \<Longrightarrow> no_throw \<top> (L <handle2> R)" unfolding no_throw_def by (metis hoareE_TrueI no_throw_def no_throw_handle2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. no_throw (\<lambda>_. True) (R x)) \<Longrightarrow> no_throw (\<lambda>_. True) (L <handle2> R) proof (prove)
goal (1 subgoal):
 1. (\<And>x. \<lbrace>\<lambda>_. True\<rbrace> R x \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_ _. False\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> L <handle2> R \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_ _. False\<rbrace>
theory Nondet_No_Throw

lemma handleE_nothrow_lhs:
  "no_throw \<top> L \<Longrightarrow> no_throw \<top> (L <handle> R)" by (metis handleE'_nothrow_lhs handleE_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_throw (\<lambda>_. True) L \<Longrightarrow> no_throw (\<lambda>_. True) (L <handle> R)
theory Nondet_No_Throw

lemma handleE_nothrow_rhs:
  "\<lbrakk> \<And>x. no_throw \<top> (R x) \<rbrakk> \<Longrightarrow> no_throw \<top> (L <handle> R)" by (metis no_throw_handleE_simple)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. no_throw (\<lambda>_. True) (R x)) \<Longrightarrow> no_throw (\<lambda>_. True) (L <handle> R)
theory Nondet_No_Throw

lemma no_throw_Inr:
  "\<lbrakk> x \<in> fst (A s); no_throw P A; P s \<rbrakk> \<Longrightarrow> \<exists>y. fst x = Inr y" by (fastforce simp: no_throw_def' split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> fst (A s); no_throw P A; P s\<rbrakk> \<Longrightarrow> \<exists>y. fst x = Inr y
theory Nondet_No_Throw

lemma no_throw_handleE':
  "no_throw \<top> A \<Longrightarrow> (A <handle2> B) = A" apply (rule monad_eqI; monad_eq) apply (fastforce dest: no_throw_Inr) apply (metis (lifting) fst_conv no_throw_Inr) apply (fastforce dest: no_throw_Inr) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_throw (\<lambda>_. True) A \<Longrightarrow> (A <handle2> B) = A proof (prove)
goal (3 subgoals):
 1. \<And>r t s. \<lbrakk>no_throw (\<lambda>_. True) A; (\<exists>ex. r = Inr ex \<and> (Inr ex, t) \<in> fst (A s)) \<or> (\<exists>rv' s''. (r, t) \<in> fst (B rv' s'') \<and> (Inl rv', s'') \<in> fst (A s))\<rbrakk> \<Longrightarrow> (r, t) \<in> fst (A s)
 2. \<And>r t s. \<lbrakk>no_throw (\<lambda>_. True) A; (r, t) \<in> fst (A s); \<forall>rv' s''. (r, t) \<in> fst (B rv' s'') \<longrightarrow> (Inl rv', s'') \<notin> fst (A s)\<rbrakk> \<Longrightarrow> \<exists>ex. r = Inr ex \<and> (Inr ex, t) \<in> fst (A s)
 3. \<And>x. no_throw (\<lambda>_. True) A \<Longrightarrow> (snd (A x) \<or> (\<exists>r s'. (r, s') \<in> fst (A x) \<and> (\<exists>a. r = Inl a \<and> snd (B a s')))) = snd (A x) proof (prove)
goal (2 subgoals):
 1. \<And>r t s. \<lbrakk>no_throw (\<lambda>_. True) A; (r, t) \<in> fst (A s); \<forall>rv' s''. (r, t) \<in> fst (B rv' s'') \<longrightarrow> (Inl rv', s'') \<notin> fst (A s)\<rbrakk> \<Longrightarrow> \<exists>ex. r = Inr ex \<and> (Inr ex, t) \<in> fst (A s)
 2. \<And>x. no_throw (\<lambda>_. True) A \<Longrightarrow> (snd (A x) \<or> (\<exists>r s'. (r, s') \<in> fst (A x) \<and> (\<exists>a. r = Inl a \<and> snd (B a s')))) = snd (A x) proof (prove)
goal (1 subgoal):
 1. \<And>x. no_throw (\<lambda>_. True) A \<Longrightarrow> (snd (A x) \<or> (\<exists>r s'. (r, s') \<in> fst (A x) \<and> (\<exists>a. r = Inl a \<and> snd (B a s')))) = snd (A x) proof (prove)
goal:
No subgoals!
theory Nondet_No_Throw

lemma no_throw_handleE:
  "no_throw \<top> A \<Longrightarrow> (A <handle> B) = A" unfolding handleE_def by (auto simp: no_throw_handleE')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_throw (\<lambda>_. True) A \<Longrightarrow> (A <handle> B) = A proof (prove)
goal (1 subgoal):
 1. no_throw (\<lambda>_. True) A \<Longrightarrow> (A <handle2> B) = A
theory Nondet_No_Throw

lemma bindE_handleE_join:
  "no_throw \<top> A \<Longrightarrow> (A >>=E (\<lambda>x. (B x) <handle> C)) = ((A >>=E B <handle> C))" by (monad_eq simp: Bex_def Ball_def no_throw_def') blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_throw (\<lambda>_. True) A \<Longrightarrow> doE x <- A;
B x <handle> C
odE = (A >>=E B <handle> C)
theory CutMon

lemma cutMon_walk_bind:
  "cutMon ((=) s) (f >>= g) =
   (cutMon ((=) s) f >>= (\<lambda>rv. cutMon (\<lambda>s'. (rv, s') \<in> fst (f s)) (g rv)))" apply (rule ext, simp add: cutMon_def bind_def fail_def) apply (auto simp: split_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cutMon ((=) s) (f >>= g) = do rv <- cutMon ((=) s) f;
cutMon (\<lambda>s'. (rv, s') \<in> fst (f s)) (g rv)
od proof (prove)
goal (1 subgoal):
 1. \<And>x. s = x \<longrightarrow> (\<Union>a\<in>fst (f x). fst (case a of (x, xa) \<Rightarrow> g x xa)) = (\<Union>xa\<in>fst (f x). fst (case xa of (rv, s) \<Rightarrow> if (rv, s) \<in> fst (f x) then g rv s else fail s)) \<and> ((\<exists>x\<in>fst (f x). snd (case x of (x, xa) \<Rightarrow> g x xa)) \<or> snd (f x)) = ((\<exists>xa\<in>fst (f x). snd (case xa of (rv, s) \<Rightarrow> if (rv, s) \<in> fst (f x) then g rv s else fail s)) \<or> snd (f x)) proof (prove)
goal:
No subgoals!