theory HaskellLemmaBucket

lemma findM_on_outcome:
  assumes x: "\<And>x ys. x \<in> set xs \<Longrightarrow> \<lbrace>Q None and I\<rbrace> f x \<lbrace>\<lambda>rv s. (rv \<longrightarrow> Q (Some x) s) \<and> (\<not> rv \<longrightarrow> Q None s \<and> I s)\<rbrace>"
  shows      "\<lbrace>Q None and I\<rbrace> findM f xs \<lbrace>Q\<rbrace>" apply (rule hoare_vcg_precond_imp) apply (rule findM_on_outcome' [where fn="\<lambda>s. if I s then set xs else {}"]) apply (case_tac "x \<notin> set xs") apply simp apply (simp cong: rev_conj_cong) apply (case_tac "\<not> set xsa \<subseteq> set xs") apply simp apply simp apply (rule hoare_vcg_precond_imp) apply (rule hoare_post_imp [OF _ x]) apply clarsimp apply assumption apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>Q None and I\<rbrace> findM f xs \<lbrace>Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> findM f xs \<lbrace>Q\<rbrace>
 2. \<And>s. (Q None and I) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>x xsa. \<lbrace>\<lambda>s. Q None s \<and> x \<in> (if I s then set xs else {}) \<and> set xsa \<subseteq> (if I s then set xs else {})\<rbrace> f x \<lbrace>\<lambda>rv s. (rv \<longrightarrow> Q (Some x) s) \<and> (\<not> rv \<longrightarrow> Q None s \<and> set xsa \<subseteq> (if I s then set xs else {}))\<rbrace>
 2. \<And>s. (Q None and I) s \<Longrightarrow> Q None s \<and> set xs \<subseteq> (if I s then set xs else {}) proof (prove)
goal (3 subgoals):
 1. \<And>x xsa. x \<notin> set xs \<Longrightarrow> \<lbrace>\<lambda>s. Q None s \<and> x \<in> (if I s then set xs else {}) \<and> set xsa \<subseteq> (if I s then set xs else {})\<rbrace> f x \<lbrace>\<lambda>rv s. (rv \<longrightarrow> Q (Some x) s) \<and> (\<not> rv \<longrightarrow> Q None s \<and> set xsa \<subseteq> (if I s then set xs else {}))\<rbrace>
 2. \<And>x xsa. \<not> x \<notin> set xs \<Longrightarrow> \<lbrace>\<lambda>s. Q None s \<and> x \<in> (if I s then set xs else {}) \<and> set xsa \<subseteq> (if I s then set xs else {})\<rbrace> f x \<lbrace>\<lambda>rv s. (rv \<longrightarrow> Q (Some x) s) \<and> (\<not> rv \<longrightarrow> Q None s \<and> set xsa \<subseteq> (if I s then set xs else {}))\<rbrace>
 3. \<And>s. (Q None and I) s \<Longrightarrow> Q None s \<and> set xs \<subseteq> (if I s then set xs else {}) proof (prove)
goal (2 subgoals):
 1. \<And>x xsa. \<not> x \<notin> set xs \<Longrightarrow> \<lbrace>\<lambda>s. Q None s \<and> x \<in> (if I s then set xs else {}) \<and> set xsa \<subseteq> (if I s then set xs else {})\<rbrace> f x \<lbrace>\<lambda>rv s. (rv \<longrightarrow> Q (Some x) s) \<and> (\<not> rv \<longrightarrow> Q None s \<and> set xsa \<subseteq> (if I s then set xs else {}))\<rbrace>
 2. \<And>s. (Q None and I) s \<Longrightarrow> Q None s \<and> set xs \<subseteq> (if I s then set xs else {}) proof (prove)
goal (2 subgoals):
 1. \<And>x xsa. x \<in> set xs \<Longrightarrow> \<lbrace>\<lambda>s. Q None s \<and> set xsa \<subseteq> set xs \<and> I s\<rbrace> f x \<lbrace>\<lambda>rv s. (I s \<longrightarrow> (rv \<longrightarrow> Q (Some x) s) \<and> (\<not> rv \<longrightarrow> Q None s \<and> set xsa \<subseteq> set xs)) \<and> (\<not> I s \<longrightarrow> (rv \<longrightarrow> Q (Some x) s) \<and> (\<not> rv \<longrightarrow> Q None s \<and> xsa = []))\<rbrace>
 2. \<And>s. (Q None and I) s \<Longrightarrow> Q None s \<and> set xs \<subseteq> (if I s then set xs else {}) proof (prove)
goal (3 subgoals):
 1. \<And>x xsa. \<lbrakk>x \<in> set xs; \<not> set xsa \<subseteq> set xs\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. Q None s \<and> set xsa \<subseteq> set xs \<and> I s\<rbrace> f x \<lbrace>\<lambda>rv s. (I s \<longrightarrow> (rv \<longrightarrow> Q (Some x) s) \<and> (\<not> rv \<longrightarrow> Q None s \<and> set xsa \<subseteq> set xs)) \<and> (\<not> I s \<longrightarrow> (rv \<longrightarrow> Q (Some x) s) \<and> (\<not> rv \<longrightarrow> Q None s \<and> xsa = []))\<rbrace>
 2. \<And>x xsa. \<lbrakk>x \<in> set xs; \<not> \<not> set xsa \<subseteq> set xs\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. Q None s \<and> set xsa \<subseteq> set xs \<and> I s\<rbrace> f x \<lbrace>\<lambda>rv s. (I s \<longrightarrow> (rv \<longrightarrow> Q (Some x) s) \<and> (\<not> rv \<longrightarrow> Q None s \<and> set xsa \<subseteq> set xs)) \<and> (\<not> I s \<longrightarrow> (rv \<longrightarrow> Q (Some x) s) \<and> (\<not> rv \<longrightarrow> Q None s \<and> xsa = []))\<rbrace>
 3. \<And>s. (Q None and I) s \<Longrightarrow> Q None s \<and> set xs \<subseteq> (if I s then set xs else {}) proof (prove)
goal (2 subgoals):
 1. \<And>x xsa. \<lbrakk>x \<in> set xs; \<not> \<not> set xsa \<subseteq> set xs\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. Q None s \<and> set xsa \<subseteq> set xs \<and> I s\<rbrace> f x \<lbrace>\<lambda>rv s. (I s \<longrightarrow> (rv \<longrightarrow> Q (Some x) s) \<and> (\<not> rv \<longrightarrow> Q None s \<and> set xsa \<subseteq> set xs)) \<and> (\<not> I s \<longrightarrow> (rv \<longrightarrow> Q (Some x) s) \<and> (\<not> rv \<longrightarrow> Q None s \<and> xsa = []))\<rbrace>
 2. \<And>s. (Q None and I) s \<Longrightarrow> Q None s \<and> set xs \<subseteq> (if I s then set xs else {}) proof (prove)
goal (2 subgoals):
 1. \<And>x xsa. \<lbrakk>x \<in> set xs; set xsa \<subseteq> set xs\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. Q None s \<and> I s\<rbrace> f x \<lbrace>\<lambda>rv s. (I s \<longrightarrow> (rv \<longrightarrow> Q (Some x) s) \<and> (\<not> rv \<longrightarrow> Q None s)) \<and> (\<not> I s \<longrightarrow> (rv \<longrightarrow> Q (Some x) s) \<and> (\<not> rv \<longrightarrow> Q None s \<and> xsa = []))\<rbrace>
 2. \<And>s. (Q None and I) s \<Longrightarrow> Q None s \<and> set xs \<subseteq> (if I s then set xs else {}) proof (prove)
goal (3 subgoals):
 1. \<And>x xsa. \<lbrakk>x \<in> set xs; set xsa \<subseteq> set xs\<rbrakk> \<Longrightarrow> \<lbrace>?Q31 x xsa\<rbrace> f x \<lbrace>\<lambda>rv s. (I s \<longrightarrow> (rv \<longrightarrow> Q (Some x) s) \<and> (\<not> rv \<longrightarrow> Q None s)) \<and> (\<not> I s \<longrightarrow> (rv \<longrightarrow> Q (Some x) s) \<and> (\<not> rv \<longrightarrow> Q None s \<and> xsa = []))\<rbrace>
 2. \<And>x xsa s. \<lbrakk>x \<in> set xs; set xsa \<subseteq> set xs; Q None s \<and> I s\<rbrakk> \<Longrightarrow> ?Q31 x xsa s
 3. \<And>s. (Q None and I) s \<Longrightarrow> Q None s \<and> set xs \<subseteq> (if I s then set xs else {}) proof (prove)
goal (4 subgoals):
 1. \<And>x xsa rv s. \<lbrakk>x \<in> set xs; set xsa \<subseteq> set xs; (rv \<longrightarrow> Q (Some x) s) \<and> (\<not> rv \<longrightarrow> Q None s \<and> I s)\<rbrakk> \<Longrightarrow> (I s \<longrightarrow> (rv \<longrightarrow> Q (Some x) s) \<and> (\<not> rv \<longrightarrow> Q None s)) \<and> (\<not> I s \<longrightarrow> (rv \<longrightarrow> Q (Some x) s) \<and> (\<not> rv \<longrightarrow> Q None s \<and> xsa = []))
 2. \<And>x xsa. \<lbrakk>x \<in> set xs; set xsa \<subseteq> set xs\<rbrakk> \<Longrightarrow> x \<in> set xs
 3. \<And>x xsa s. \<lbrakk>x \<in> set xs; set xsa \<subseteq> set xs; Q None s \<and> I s\<rbrakk> \<Longrightarrow> (Q None and I) s
 4. \<And>s. (Q None and I) s \<Longrightarrow> Q None s \<and> set xs \<subseteq> (if I s then set xs else {}) proof (prove)
goal (3 subgoals):
 1. \<And>x xsa. \<lbrakk>x \<in> set xs; set xsa \<subseteq> set xs\<rbrakk> \<Longrightarrow> x \<in> set xs
 2. \<And>x xsa s. \<lbrakk>x \<in> set xs; set xsa \<subseteq> set xs; Q None s \<and> I s\<rbrakk> \<Longrightarrow> (Q None and I) s
 3. \<And>s. (Q None and I) s \<Longrightarrow> Q None s \<and> set xs \<subseteq> (if I s then set xs else {}) proof (prove)
goal (2 subgoals):
 1. \<And>x xsa s. \<lbrakk>x \<in> set xs; set xsa \<subseteq> set xs; Q None s \<and> I s\<rbrakk> \<Longrightarrow> (Q None and I) s
 2. \<And>s. (Q None and I) s \<Longrightarrow> Q None s \<and> set xs \<subseteq> (if I s then set xs else {}) proof (prove)
goal (1 subgoal):
 1. \<And>s. (Q None and I) s \<Longrightarrow> Q None s \<and> set xs \<subseteq> (if I s then set xs else {}) proof (prove)
goal:
No subgoals!