theory Corres_UL

lemma corres_symb_exec_catch_r:
  "\<lbrakk> \<And>rv. corres_underlying sr nf nf' r P (Q' rv) f (h rv);
        \<lbrace>P'\<rbrace> g \<lbrace>\<bottom>\<bottom>\<rbrace>, \<lbrace>Q'\<rbrace>; \<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>r. (=) s\<rbrace>; nf' \<Longrightarrow> no_fail P' g \<rbrakk>
      \<Longrightarrow> corres_underlying sr nf nf' r P P' f (g <catch> h)" apply (simp add: catch_def) apply (rule corres_symb_exec_r, simp_all) apply (rule_tac F="isLeft x" in corres_gen_asm2) apply (simp add: isLeft_case_sum) apply assumption apply (simp add: validE_def) apply (erule hoare_chain, simp_all)[1] apply (simp split: sum.split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>rv. corres_underlying sr nf nf' r P (Q' rv) f (h rv); \<lbrace>P'\<rbrace> g \<lbrace>\<lambda>_ _. False\<rbrace>, \<lbrace>Q'\<rbrace>; \<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>r. (=) s\<rbrace>; nf' \<Longrightarrow> no_fail P' g\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r P P' f (g <catch> h) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>rv. corres_underlying sr nf nf' r P (Q' rv) f (h rv); \<lbrace>P'\<rbrace> g \<lbrace>\<lambda>_ _. False\<rbrace>, \<lbrace>Q'\<rbrace>; \<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>r. (=) s\<rbrace>; nf' \<Longrightarrow> no_fail P' g\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r P P' f (do x <- g;
case x of Inl e \<Rightarrow> h e | Inr b \<Rightarrow> return b
od) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<And>rv. corres_underlying sr nf nf' r P (Q' rv) f (h rv); \<lbrace>P'\<rbrace> g \<lbrace>\<lambda>_ _. False\<rbrace>, \<lbrace>Q'\<rbrace>; \<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>r. (=) s\<rbrace>; nf' \<Longrightarrow> no_fail P' g\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r P (?Q' x) f (case x of Inl e \<Rightarrow> h e | Inr b \<Rightarrow> return b)
 2. \<lbrakk>\<And>rv. corres_underlying sr nf nf' r P (Q' rv) f (h rv); \<lbrace>P'\<rbrace> g \<lbrace>\<lambda>_ _. False\<rbrace>, \<lbrace>Q'\<rbrace>; \<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>r. (=) s\<rbrace>; nf' \<Longrightarrow> no_fail P' g\<rbrakk> \<Longrightarrow> \<lbrace>P'\<rbrace> g \<lbrace>?Q'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<And>rv. corres_underlying sr nf nf' r P (Q' rv) f (h rv); \<lbrace>P'\<rbrace> g \<lbrace>\<lambda>_ _. False\<rbrace>, \<lbrace>Q'\<rbrace>; \<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>r. (=) s\<rbrace>; nf' \<Longrightarrow> no_fail P' g; isLeft x\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r P (?P'5 x) f (case x of Inl e \<Rightarrow> h e | Inr b \<Rightarrow> return b)
 2. \<lbrakk>\<And>rv. corres_underlying sr nf nf' r P (Q' rv) f (h rv); \<lbrace>P'\<rbrace> g \<lbrace>\<lambda>_ _. False\<rbrace>, \<lbrace>Q'\<rbrace>; \<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>r. (=) s\<rbrace>; nf' \<Longrightarrow> no_fail P' g\<rbrakk> \<Longrightarrow> \<lbrace>P'\<rbrace> g \<lbrace>\<lambda>x. ?P'5 x and (\<lambda>s. isLeft x)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<And>rv. corres_underlying sr nf nf' r P (Q' rv) f (h rv); \<lbrace>P'\<rbrace> g \<lbrace>\<lambda>_ _. False\<rbrace>, \<lbrace>Q'\<rbrace>; \<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>r. (=) s\<rbrace>; nf' \<Longrightarrow> no_fail P' g; isLeft x\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r P (?P'5 x) f (h (theLeft x))
 2. \<lbrakk>\<And>rv. corres_underlying sr nf nf' r P (Q' rv) f (h rv); \<lbrace>P'\<rbrace> g \<lbrace>\<lambda>_ _. False\<rbrace>, \<lbrace>Q'\<rbrace>; \<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>r. (=) s\<rbrace>; nf' \<Longrightarrow> no_fail P' g\<rbrakk> \<Longrightarrow> \<lbrace>P'\<rbrace> g \<lbrace>\<lambda>x. ?P'5 x and (\<lambda>s. isLeft x)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>rv. corres_underlying sr nf nf' r P (Q' rv) f (h rv); \<lbrace>P'\<rbrace> g \<lbrace>\<lambda>_ _. False\<rbrace>, \<lbrace>Q'\<rbrace>; \<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>r. (=) s\<rbrace>; nf' \<Longrightarrow> no_fail P' g\<rbrakk> \<Longrightarrow> \<lbrace>P'\<rbrace> g \<lbrace>\<lambda>x. Q' (theLeft x) and (\<lambda>s. isLeft x)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>rv. corres_underlying sr nf nf' r P (Q' rv) f (h rv); \<lbrace>P'\<rbrace> g \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> Q' e s | Inr r \<Rightarrow> False\<rbrace>; \<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>r. (=) s\<rbrace>; nf' \<Longrightarrow> no_fail P' g\<rbrakk> \<Longrightarrow> \<lbrace>P'\<rbrace> g \<lbrace>\<lambda>x. Q' (theLeft x) and (\<lambda>s. isLeft x)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>rv s. \<lbrakk>\<And>rv. corres_underlying sr nf nf' r P (Q' rv) f (h rv); \<And>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>r. (=) s\<rbrace>; nf' \<Longrightarrow> no_fail P' g; case rv of Inl e \<Rightarrow> Q' e s | Inr r \<Rightarrow> False\<rbrakk> \<Longrightarrow> Q' (theLeft rv) s \<and> isLeft rv proof (prove)
goal:
No subgoals!