theory Bits_R

lemma corres_const_on_failure:
  "corres ((\<lambda>_ _. r x y) \<oplus> r) P P' m m' \<Longrightarrow>
   corres r P P' (const_on_failure x m) (constOnFailure y m')" apply (simp add: const_on_failure_def constOnFailure_def) apply (rule corres_guard_imp) apply (rule corres_split_catch) apply assumption apply (rule corres_trivial, simp) apply (clarsimp simp: const_def) apply wp+ apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres ((\<lambda>_ _. r x y) \<oplus> r) P P' m m' \<Longrightarrow> corres r P P' (const_on_failure x m) (constOnFailure y m') proof (prove)
goal (1 subgoal):
 1. corres ((\<lambda>_ _. r x y) \<oplus> r) P P' m m' \<Longrightarrow> corres r P P' (m <catch> (\<lambda>xa. return x)) (m' <catch> const (return y)) proof (prove)
goal (3 subgoals):
 1. corres ((\<lambda>_ _. r x y) \<oplus> r) P P' m m' \<Longrightarrow> corres r ?Q ?Q' (m <catch> (\<lambda>xa. return x)) (m' <catch> const (return y))
 2. \<And>s. \<lbrakk>corres ((\<lambda>_ _. r x y) \<oplus> r) P P' m m'; P s\<rbrakk> \<Longrightarrow> ?Q s
 3. \<And>s. \<lbrakk>corres ((\<lambda>_ _. r x y) \<oplus> r) P P' m m'; P' s\<rbrakk> \<Longrightarrow> ?Q' s proof (prove)
goal (6 subgoals):
 1. corres ((\<lambda>_ _. r x y) \<oplus> r) P P' m m' \<Longrightarrow> corres (?f4 \<oplus> r) ?P4 ?P'4 m m'
 2. \<And>xa ft'. \<lbrakk>corres ((\<lambda>_ _. r x y) \<oplus> r) P P' m m'; ?f4 xa ft'\<rbrakk> \<Longrightarrow> corres r (?E4 xa) (?E'4 ft') (return x) (const (return y) ft')
 3. corres ((\<lambda>_ _. r x y) \<oplus> r) P P' m m' \<Longrightarrow> \<lbrace>?Q4\<rbrace> m \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E4\<rbrace>
 4. corres ((\<lambda>_ _. r x y) \<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>_ _. r x y) \<oplus> r) P P' m m'; P s\<rbrakk> \<Longrightarrow> (?P4 and ?Q4) s
 6. \<And>s. \<lbrakk>corres ((\<lambda>_ _. r x y) \<oplus> r) P P' m m'; P' s\<rbrakk> \<Longrightarrow> (?P'4 and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>xa ft'. \<lbrakk>corres ((\<lambda>_ _. r x y) \<oplus> r) P P' m m'; r x y\<rbrakk> \<Longrightarrow> corres r (?E4 xa) (?E'4 ft') (return x) (const (return y) ft')
 2. corres ((\<lambda>_ _. r x y) \<oplus> r) P P' m m' \<Longrightarrow> \<lbrace>?Q4\<rbrace> m \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E4\<rbrace>
 3. corres ((\<lambda>_ _. r x y) \<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>_ _. r x y) \<oplus> r) P P' m m'; P s\<rbrakk> \<Longrightarrow> (P and ?Q4) s
 5. \<And>s. \<lbrakk>corres ((\<lambda>_ _. r x y) \<oplus> r) P P' m m'; P' s\<rbrakk> \<Longrightarrow> (P' and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>ft'. \<lbrakk>corres ((\<lambda>_ _. True) \<oplus> r) P P' m m'; r x y\<rbrakk> \<Longrightarrow> corres r (\<lambda>_. True) (\<lambda>_. True) (return x) (const (return y) ft')
 2. corres ((\<lambda>_ _. r x y) \<oplus> r) P P' m m' \<Longrightarrow> \<lbrace>?Q4\<rbrace> m \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>x _. True\<rbrace>
 3. corres ((\<lambda>_ _. r x y) \<oplus> r) P P' m m' \<Longrightarrow> \<lbrace>?Q'4\<rbrace> m' \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>ft' _. True\<rbrace>
 4. \<And>s. \<lbrakk>corres ((\<lambda>_ _. r x y) \<oplus> r) P P' m m'; P s\<rbrakk> \<Longrightarrow> (P and ?Q4) s
 5. \<And>s. \<lbrakk>corres ((\<lambda>_ _. r x y) \<oplus> r) P P' m m'; P' s\<rbrakk> \<Longrightarrow> (P' and ?Q'4) s proof (prove)
goal (4 subgoals):
 1. corres ((\<lambda>_ _. r x y) \<oplus> r) P P' m m' \<Longrightarrow> \<lbrace>?Q4\<rbrace> m \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>x _. True\<rbrace>
 2. corres ((\<lambda>_ _. r x y) \<oplus> r) P P' m m' \<Longrightarrow> \<lbrace>?Q'4\<rbrace> m' \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>ft' _. True\<rbrace>
 3. \<And>s. \<lbrakk>corres ((\<lambda>_ _. r x y) \<oplus> r) P P' m m'; P s\<rbrakk> \<Longrightarrow> (P and ?Q4) s
 4. \<And>s. \<lbrakk>corres ((\<lambda>_ _. r x y) \<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>_ _. r x y) \<oplus> r) P P' m m'; P s\<rbrakk> \<Longrightarrow> (P and (\<lambda>s. True \<and> True)) s
 2. \<And>s. \<lbrakk>corres ((\<lambda>_ _. r x y) \<oplus> r) P P' m m'; P' s\<rbrakk> \<Longrightarrow> (P' and (\<lambda>s. True \<and> True)) s proof (prove)
goal:
No subgoals!