theory Bits_R

lemma corres_empty_on_failure:
  "corres ((\<lambda>x y. r [] []) \<oplus> r) P P' m m' \<Longrightarrow>
   corres r P P' (empty_on_failure m) (emptyOnFailure m')" apply (simp add: empty_on_failure_def emptyOnFailure_def) apply (rule corres_guard_imp) apply (rule corres_split_catch) apply assumption apply (rule corres_trivial, simp) apply wp+ apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres ((\<lambda>x y. r [] []) \<oplus> r) P P' m m' \<Longrightarrow> corres r P P' (empty_on_failure m) (emptyOnFailure m') proof (prove)
goal (1 subgoal):
 1. corres ((\<lambda>x y. r [] []) \<oplus> r) P P' m m' \<Longrightarrow> corres r P P' (m <catch> (\<lambda>x. return [])) (m' <catch> (\<lambda>x. return [])) proof (prove)
goal (3 subgoals):
 1. corres ((\<lambda>x y. r [] []) \<oplus> r) P P' m m' \<Longrightarrow> corres r ?Q ?Q' (m <catch> (\<lambda>x. return [])) (m' <catch> (\<lambda>x. return []))
 2. \<And>s. \<lbrakk>corres ((\<lambda>x y. r [] []) \<oplus> r) P P' m m'; P s\<rbrakk> \<Longrightarrow> ?Q s
 3. \<And>s. \<lbrakk>corres ((\<lambda>x y. r [] []) \<oplus> r) P P' m m'; P' s\<rbrakk> \<Longrightarrow> ?Q' s proof (prove)
goal (6 subgoals):
 1. corres ((\<lambda>x y. r [] []) \<oplus> r) P P' m m' \<Longrightarrow> corres (?f4 \<oplus> r) ?P4 ?P'4 m m'
 2. \<And>x xa. \<lbrakk>corres ((\<lambda>x y. r [] []) \<oplus> r) P P' m m'; ?f4 x xa\<rbrakk> \<Longrightarrow> corres r (?E4 x) (?E'4 xa) (return []) (return [])
 3. corres ((\<lambda>x y. r [] []) \<oplus> r) P P' m m' \<Longrightarrow> \<lbrace>?Q4\<rbrace> m \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E4\<rbrace>
 4. corres ((\<lambda>x y. r [] []) \<oplus> r) P P' m m' \<Longrightarrow> \<lbrace>?Q'4\<rbrace> m' \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E'4\<rbrace>
 5. \<And>s. \<lbrakk>corres ((\<lambda>x y. r [] []) \<oplus> r) P P' m m'; P s\<rbrakk> \<Longrightarrow> (?P4 and ?Q4) s
 6. \<And>s. \<lbrakk>corres ((\<lambda>x y. r [] []) \<oplus> r) P P' m m'; P' s\<rbrakk> \<Longrightarrow> (?P'4 and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>x xa. \<lbrakk>corres ((\<lambda>x y. r [] []) \<oplus> r) P P' m m'; r [] []\<rbrakk> \<Longrightarrow> corres r (?E4 x) (?E'4 xa) (return []) (return [])
 2. corres ((\<lambda>x y. r [] []) \<oplus> r) P P' m m' \<Longrightarrow> \<lbrace>?Q4\<rbrace> m \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E4\<rbrace>
 3. corres ((\<lambda>x y. r [] []) \<oplus> r) P P' m m' \<Longrightarrow> \<lbrace>?Q'4\<rbrace> m' \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E'4\<rbrace>
 4. \<And>s. \<lbrakk>corres ((\<lambda>x y. r [] []) \<oplus> r) P P' m m'; P s\<rbrakk> \<Longrightarrow> (P and ?Q4) s
 5. \<And>s. \<lbrakk>corres ((\<lambda>x y. r [] []) \<oplus> r) P P' m m'; P' s\<rbrakk> \<Longrightarrow> (P' and ?Q'4) s proof (prove)
goal (4 subgoals):
 1. corres ((\<lambda>x y. r [] []) \<oplus> r) P P' m m' \<Longrightarrow> \<lbrace>?Q4\<rbrace> m \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>x _. True\<rbrace>
 2. corres ((\<lambda>x y. r [] []) \<oplus> r) P P' m m' \<Longrightarrow> \<lbrace>?Q'4\<rbrace> m' \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>xa _. True\<rbrace>
 3. \<And>s. \<lbrakk>corres ((\<lambda>x y. r [] []) \<oplus> r) P P' m m'; P s\<rbrakk> \<Longrightarrow> (P and ?Q4) s
 4. \<And>s. \<lbrakk>corres ((\<lambda>x y. r [] []) \<oplus> r) P P' m m'; P' s\<rbrakk> \<Longrightarrow> (P' and ?Q'4) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>corres ((\<lambda>x y. r [] []) \<oplus> r) P P' m m'; P s\<rbrakk> \<Longrightarrow> (P and (\<lambda>s. True \<and> True)) s
 2. \<And>s. \<lbrakk>corres ((\<lambda>x y. r [] []) \<oplus> r) P P' m m'; P' s\<rbrakk> \<Longrightarrow> (P' and (\<lambda>s. True \<and> True)) s proof (prove)
goal:
No subgoals!