theory Orphanage

lemma findM_on_success:
  "\<lbrakk> \<And>x. \<lbrace> P x \<rbrace> f x \<lbrace> \<lambda>rv s. rv \<rbrace>; \<And>x y. \<lbrace> P x \<rbrace> f y \<lbrace> \<lambda>rv. P x \<rbrace> \<rbrakk> \<Longrightarrow>
   \<lbrace> \<lambda>s. \<exists>x \<in> set xs. P x s \<rbrace> findM f xs \<lbrace> \<lambda>rv s. \<exists> y. rv = Some y \<rbrace>" apply (induct xs; clarsimp) apply wp+ apply (clarsimp simp: imp_conv_disj Bex_def) apply (wp hoare_vcg_disj_lift hoare_vcg_ex_lift | clarsimp | assumption)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>x. \<lbrace>P x\<rbrace> f x \<lbrace>\<lambda>rv s. rv\<rbrace>; \<And>x y. \<lbrace>P x\<rbrace> f y \<lbrace>\<lambda>rv. P x\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>x\<in>set xs. P x s\<rbrace> findM f xs \<lbrace>\<lambda>rv s. \<exists>y. rv = Some y\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>\<lbrace>\<lambda>s. \<exists>x\<in>set xs. P x s\<rbrace> findM f xs \<lbrace>\<lambda>rv s. \<exists>y. rv = Some y\<rbrace>; \<And>x. \<lbrace>P x\<rbrace> f x \<lbrace>\<lambda>rv s. rv\<rbrace>; \<And>x y. \<lbrace>P x\<rbrace> f y \<lbrace>\<lambda>rv. P x\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P a s \<or> (\<exists>x\<in>set xs. P x s)\<rbrace> do r <- f a;
if r then return (Some a) else findM f xs
od \<lbrace>\<lambda>rv s. \<exists>y. rv = Some y\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>a xs. \<lbrakk>\<lbrace>\<lambda>s. \<exists>x\<in>set xs. P x s\<rbrace> findM f xs \<lbrace>\<lambda>rv s. \<exists>y. rv = Some y\<rbrace>; \<And>x. \<lbrace>P x\<rbrace> f x \<lbrace>\<lambda>rv s. rv\<rbrace>; \<And>x y. \<lbrace>P x\<rbrace> f y \<lbrace>\<lambda>rv. P x\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 a xs\<rbrace> f a \<lbrace>\<lambda>r s. (r \<longrightarrow> (\<exists>y. Some a = Some y)) \<and> (\<not> r \<longrightarrow> (\<exists>x\<in>set xs. P x s))\<rbrace>
 2. \<And>a xs s. \<lbrakk>\<lbrace>\<lambda>s. \<exists>x\<in>set xs. P x s\<rbrace> findM f xs \<lbrace>\<lambda>rv s. \<exists>y. rv = Some y\<rbrace>; \<And>x. \<lbrace>P x\<rbrace> f x \<lbrace>\<lambda>rv s. rv\<rbrace>; \<And>x y. \<lbrace>P x\<rbrace> f y \<lbrace>\<lambda>rv. P x\<rbrace>; P a s \<or> (\<exists>x\<in>set xs. P x s)\<rbrakk> \<Longrightarrow> ?Q12 a xs s proof (prove)
goal (2 subgoals):
 1. \<And>a xs. \<lbrakk>\<lbrace>\<lambda>s. \<exists>x. x \<in> set xs \<and> P x s\<rbrace> findM f xs \<lbrace>\<lambda>rv s. \<exists>y. rv = Some y\<rbrace>; \<And>x. \<lbrace>P x\<rbrace> f x \<lbrace>\<lambda>rv s. rv\<rbrace>; \<And>x y. \<lbrace>P x\<rbrace> f y \<lbrace>\<lambda>rv. P x\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 a xs\<rbrace> f a \<lbrace>\<lambda>r s. r \<or> (\<exists>x. x \<in> set xs \<and> P x s)\<rbrace>
 2. \<And>a xs s. \<lbrakk>\<lbrace>\<lambda>s. \<exists>x\<in>set xs. P x s\<rbrace> findM f xs \<lbrace>\<lambda>rv s. \<exists>y. rv = Some y\<rbrace>; \<And>x. \<lbrace>P x\<rbrace> f x \<lbrace>\<lambda>rv s. rv\<rbrace>; \<And>x y. \<lbrace>P x\<rbrace> f y \<lbrace>\<lambda>rv. P x\<rbrace>; P a s \<or> (\<exists>x\<in>set xs. P x s)\<rbrakk> \<Longrightarrow> ?Q12 a xs s proof (prove)
goal:
No subgoals!