theory Finalise_DR

lemma dcorres_might_throw:
  "\<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> b \<lbrace>\<lambda>r. (=) s\<rbrace>\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) \<top> \<top> might_throw (throw_on_false a b)" apply (simp add: liftE_bindE unlessE_def
    might_throw_def throw_on_false_def split:if_splits) apply (rule corres_symb_exec_r) apply (clarsimp split:if_splits) apply (intro conjI impI) apply (rule corres_alternate1) apply (simp add:returnOk_def) apply (rule corres_alternate2) apply simp apply (wp hoare_TrueI) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s. \<lbrace>(=) s\<rbrace> b \<lbrace>\<lambda>r. (=) s\<rbrace>) \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (\<lambda>_. True) might_throw (throw_on_false a b) proof (prove)
goal (1 subgoal):
 1. (\<And>s. \<lbrace>(=) s\<rbrace> b \<lbrace>\<lambda>r. (=) s\<rbrace>) \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (\<lambda>_. True) (returnOk () \<sqinter> throw) (do v <- b;
if v then returnOk () else throwError a
od) proof (prove)
goal (4 subgoals):
 1. \<And>v. (\<And>s. \<lbrace>(=) s\<rbrace> b \<lbrace>\<lambda>r. (=) s\<rbrace>) \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (?Q' v) (returnOk () \<sqinter> throw) (if v then returnOk () else throwError a)
 2. (\<And>s. \<lbrace>(=) s\<rbrace> b \<lbrace>\<lambda>r. (=) s\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> b \<lbrace>?Q'\<rbrace>
 3. \<And>s. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> b \<lbrace>\<lambda>r. (=) s\<rbrace>; True\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> b \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> b \<lbrace>\<lambda>r. (=) s\<rbrace>; False\<rbrakk> \<Longrightarrow> no_fail (\<lambda>_. True) b proof (prove)
goal (4 subgoals):
 1. \<And>v. (\<And>s. \<lbrace>(=) s\<rbrace> b \<lbrace>\<lambda>r. (=) s\<rbrace>) \<Longrightarrow> (v \<longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (?Q' True) (returnOk () \<sqinter> throw) (returnOk ())) \<and> (\<not> v \<longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (?Q' False) (returnOk () \<sqinter> throw) (throwError a))
 2. (\<And>s. \<lbrace>(=) s\<rbrace> b \<lbrace>\<lambda>r. (=) s\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> b \<lbrace>?Q'\<rbrace>
 3. \<And>s. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> b \<lbrace>\<lambda>r. (=) s\<rbrace>; True\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> b \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> b \<lbrace>\<lambda>r. (=) s\<rbrace>; False\<rbrakk> \<Longrightarrow> no_fail (\<lambda>_. True) b proof (prove)
goal (5 subgoals):
 1. \<And>v. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> b \<lbrace>\<lambda>r. (=) s\<rbrace>; v\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (?Q' True) (returnOk () \<sqinter> throw) (returnOk ())
 2. \<And>v. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> b \<lbrace>\<lambda>r. (=) s\<rbrace>; \<not> v\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (?Q' False) (returnOk () \<sqinter> throw) (throwError a)
 3. (\<And>s. \<lbrace>(=) s\<rbrace> b \<lbrace>\<lambda>r. (=) s\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> b \<lbrace>?Q'\<rbrace>
 4. \<And>s. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> b \<lbrace>\<lambda>r. (=) s\<rbrace>; True\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> b \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> b \<lbrace>\<lambda>r. (=) s\<rbrace>; False\<rbrakk> \<Longrightarrow> no_fail (\<lambda>_. True) b proof (prove)
goal (5 subgoals):
 1. \<And>v. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> b \<lbrace>\<lambda>r. (=) s\<rbrace>; v\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (?Q' True) (returnOk ()) (returnOk ())
 2. \<And>v. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> b \<lbrace>\<lambda>r. (=) s\<rbrace>; \<not> v\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (?Q' False) (returnOk () \<sqinter> throw) (throwError a)
 3. (\<And>s. \<lbrace>(=) s\<rbrace> b \<lbrace>\<lambda>r. (=) s\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> b \<lbrace>?Q'\<rbrace>
 4. \<And>s. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> b \<lbrace>\<lambda>r. (=) s\<rbrace>; True\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> b \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> b \<lbrace>\<lambda>r. (=) s\<rbrace>; False\<rbrakk> \<Longrightarrow> no_fail (\<lambda>_. True) b proof (prove)
goal (4 subgoals):
 1. \<And>v. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> b \<lbrace>\<lambda>r. (=) s\<rbrace>; \<not> v\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (?Q' False) (returnOk () \<sqinter> throw) (throwError a)
 2. (\<And>s. \<lbrace>(=) s\<rbrace> b \<lbrace>\<lambda>r. (=) s\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> b \<lbrace>?Q'\<rbrace>
 3. \<And>s. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> b \<lbrace>\<lambda>r. (=) s\<rbrace>; True\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> b \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> b \<lbrace>\<lambda>r. (=) s\<rbrace>; False\<rbrakk> \<Longrightarrow> no_fail (\<lambda>_. True) b proof (prove)
goal (4 subgoals):
 1. \<And>v. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> b \<lbrace>\<lambda>r. (=) s\<rbrace>; \<not> v\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (?Q' False) throw (throwError a)
 2. (\<And>s. \<lbrace>(=) s\<rbrace> b \<lbrace>\<lambda>r. (=) s\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> b \<lbrace>?Q'\<rbrace>
 3. \<And>s. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> b \<lbrace>\<lambda>r. (=) s\<rbrace>; True\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> b \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> b \<lbrace>\<lambda>r. (=) s\<rbrace>; False\<rbrakk> \<Longrightarrow> no_fail (\<lambda>_. True) b proof (prove)
goal (3 subgoals):
 1. (\<And>s. \<lbrace>(=) s\<rbrace> b \<lbrace>\<lambda>r. (=) s\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> b \<lbrace>?Q'\<rbrace>
 2. \<And>s. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> b \<lbrace>\<lambda>r. (=) s\<rbrace>; True\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> b \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> b \<lbrace>\<lambda>r. (=) s\<rbrace>; False\<rbrakk> \<Longrightarrow> no_fail (\<lambda>_. True) b proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> b \<lbrace>\<lambda>r. (=) s\<rbrace>; True\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> b \<lbrace>\<lambda>r. (=) s\<rbrace>
 2. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> b \<lbrace>\<lambda>r. (=) s\<rbrace>; False\<rbrakk> \<Longrightarrow> no_fail (\<lambda>_. True) b proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> b \<lbrace>\<lambda>r. (=) s\<rbrace>; False\<rbrakk> \<Longrightarrow> no_fail (\<lambda>_. True) b proof (prove)
goal:
No subgoals!