theory Orphanage

lemma findM_failure':
  "\<lbrakk> \<And>x S. \<lbrace> \<lambda>s. P S s \<rbrace> f x \<lbrace> \<lambda>rv s. \<not> rv \<longrightarrow> P (insert x S) s \<rbrace> \<rbrakk> \<Longrightarrow>
   \<lbrace> \<lambda>s. P S s \<rbrace> findM f xs \<lbrace> \<lambda>rv s. rv = None \<longrightarrow> P (S \<union> set xs) s \<rbrace>" apply (induct xs arbitrary: S) apply (clarsimp, wp, clarsimp) apply clarsimp apply (rule hoare_seq_ext[rotated], assumption) apply (case_tac r) apply (clarsimp, wp, clarsimp) apply clarsimp apply (rule hoare_strengthen_post, assumption) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x S. \<lbrace>P S\<rbrace> f x \<lbrace>\<lambda>rv s. \<not> rv \<longrightarrow> P (insert x S) s\<rbrace>) \<Longrightarrow> \<lbrace>P S\<rbrace> findM f xs \<lbrace>\<lambda>rv s. rv = None \<longrightarrow> P (S \<union> set xs) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>S. (\<And>x S. \<lbrace>P S\<rbrace> f x \<lbrace>\<lambda>rv s. \<not> rv \<longrightarrow> P (insert x S) s\<rbrace>) \<Longrightarrow> \<lbrace>P S\<rbrace> findM f [] \<lbrace>\<lambda>rv s. rv = None \<longrightarrow> P (S \<union> set []) s\<rbrace>
 2. \<And>a xs S. \<lbrakk>\<And>S. (\<And>x S. \<lbrace>P S\<rbrace> f x \<lbrace>\<lambda>rv s. \<not> rv \<longrightarrow> P (insert x S) s\<rbrace>) \<Longrightarrow> \<lbrace>P S\<rbrace> findM f xs \<lbrace>\<lambda>rv s. rv = None \<longrightarrow> P (S \<union> set xs) s\<rbrace>; \<And>x S. \<lbrace>P S\<rbrace> f x \<lbrace>\<lambda>rv s. \<not> rv \<longrightarrow> P (insert x S) s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P S\<rbrace> findM f (a # xs) \<lbrace>\<lambda>rv s. rv = None \<longrightarrow> P (S \<union> set (a # xs)) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a xs S. \<lbrakk>\<And>S. (\<And>x S. \<lbrace>P S\<rbrace> f x \<lbrace>\<lambda>rv s. \<not> rv \<longrightarrow> P (insert x S) s\<rbrace>) \<Longrightarrow> \<lbrace>P S\<rbrace> findM f xs \<lbrace>\<lambda>rv s. rv = None \<longrightarrow> P (S \<union> set xs) s\<rbrace>; \<And>x S. \<lbrace>P S\<rbrace> f x \<lbrace>\<lambda>rv s. \<not> rv \<longrightarrow> P (insert x S) s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P S\<rbrace> findM f (a # xs) \<lbrace>\<lambda>rv s. rv = None \<longrightarrow> P (S \<union> set (a # xs)) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a xs S. \<lbrakk>\<And>S. \<lbrace>P S\<rbrace> findM f xs \<lbrace>\<lambda>rv s. rv = None \<longrightarrow> P (S \<union> set xs) s\<rbrace>; \<And>x S. \<lbrace>P S\<rbrace> f x \<lbrace>\<lambda>rv s. \<not> rv \<longrightarrow> P (insert x S) s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P S\<rbrace> do r <- f a;
if r then return (Some a) else findM f xs
od \<lbrace>\<lambda>rv s. rv = None \<longrightarrow> P (insert a (S \<union> set xs)) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a xs S r. \<lbrakk>\<And>S. \<lbrace>P S\<rbrace> findM f xs \<lbrace>\<lambda>rv s. rv = None \<longrightarrow> P (S \<union> set xs) s\<rbrace>; \<And>x S. \<lbrace>P S\<rbrace> f x \<lbrace>\<lambda>rv s. \<not> rv \<longrightarrow> P (insert x S) s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<not> r \<longrightarrow> P (insert a S) s\<rbrace> if r then return (Some a) else findM f xs \<lbrace>\<lambda>rv s. rv = None \<longrightarrow> P (insert a (S \<union> set xs)) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>a xs S r. \<lbrakk>\<And>S. \<lbrace>P S\<rbrace> findM f xs \<lbrace>\<lambda>rv s. rv = None \<longrightarrow> P (S \<union> set xs) s\<rbrace>; \<And>x S. \<lbrace>P S\<rbrace> f x \<lbrace>\<lambda>rv s. \<not> rv \<longrightarrow> P (insert x S) s\<rbrace>; r\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<not> r \<longrightarrow> P (insert a S) s\<rbrace> if r then return (Some a) else findM f xs \<lbrace>\<lambda>rv s. rv = None \<longrightarrow> P (insert a (S \<union> set xs)) s\<rbrace>
 2. \<And>a xs S r. \<lbrakk>\<And>S. \<lbrace>P S\<rbrace> findM f xs \<lbrace>\<lambda>rv s. rv = None \<longrightarrow> P (S \<union> set xs) s\<rbrace>; \<And>x S. \<lbrace>P S\<rbrace> f x \<lbrace>\<lambda>rv s. \<not> rv \<longrightarrow> P (insert x S) s\<rbrace>; \<not> r\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<not> r \<longrightarrow> P (insert a S) s\<rbrace> if r then return (Some a) else findM f xs \<lbrace>\<lambda>rv s. rv = None \<longrightarrow> P (insert a (S \<union> set xs)) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a xs S r. \<lbrakk>\<And>S. \<lbrace>P S\<rbrace> findM f xs \<lbrace>\<lambda>rv s. rv = None \<longrightarrow> P (S \<union> set xs) s\<rbrace>; \<And>x S. \<lbrace>P S\<rbrace> f x \<lbrace>\<lambda>rv s. \<not> rv \<longrightarrow> P (insert x S) s\<rbrace>; \<not> r\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<not> r \<longrightarrow> P (insert a S) s\<rbrace> if r then return (Some a) else findM f xs \<lbrace>\<lambda>rv s. rv = None \<longrightarrow> P (insert a (S \<union> set xs)) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a xs S r. \<lbrakk>\<And>S. \<lbrace>P S\<rbrace> findM f xs \<lbrace>\<lambda>rv s. rv = None \<longrightarrow> P (S \<union> set xs) s\<rbrace>; \<And>x S. \<lbrace>P S\<rbrace> f x \<lbrace>\<lambda>rv s. \<not> rv \<longrightarrow> P (insert x S) s\<rbrace>; \<not> r\<rbrakk> \<Longrightarrow> \<lbrace>P (insert a S)\<rbrace> findM f xs \<lbrace>\<lambda>rv s. rv = None \<longrightarrow> P (insert a (S \<union> set xs)) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a xs S r rv s. \<lbrakk>\<And>S. \<lbrace>P S\<rbrace> findM f xs \<lbrace>\<lambda>rv s. rv = None \<longrightarrow> P (S \<union> set xs) s\<rbrace>; \<And>x S. \<lbrace>P S\<rbrace> f x \<lbrace>\<lambda>rv s. \<not> rv \<longrightarrow> P (insert x S) s\<rbrace>; \<not> r; rv = None \<longrightarrow> P (insert a S \<union> set xs) s\<rbrakk> \<Longrightarrow> rv = None \<longrightarrow> P (insert a (S \<union> set xs)) s proof (prove)
goal:
No subgoals!