theory Monad_Lists

lemma case_option_find_give_me_a_map:
  "case_option a return (find f xs)
    = liftM projl
      (mapME (\<lambda>x. if (f x) then throwError x else returnOk ()) xs
        >>=E (\<lambda>x. assert (\<forall>x \<in> set xs. \<not> f x)
                >>= (\<lambda>_. liftM (Inl :: 'a \<Rightarrow> 'a + unit) a)))" apply (induct xs) apply simp apply (simp add: liftM_def mapME_Nil) apply (simp add: mapME_Cons split: if_split) apply (clarsimp simp add: throwError_def bindE_def bind_assoc
                            liftM_def) apply (rule bind_cong [OF refl]) apply (simp add: lift_def throwError_def returnOk_def split: sum.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (case find f xs of None \<Rightarrow> a | Some x \<Rightarrow> return x) = liftM projl (doE x <- mapME (\<lambda>x. if f x then throwError x else returnOk ()) xs;
do _ <- assert (\<forall>x\<in>set xs. \<not> f x);
liftM Inl a
od
odE) proof (prove)
goal (2 subgoals):
 1. (case find f [] of None \<Rightarrow> a | Some a \<Rightarrow> return a) = liftM projl (doE x <- mapME (\<lambda>x. if f x then throwError x else returnOk ()) [];
do _ <- assert (\<forall>x\<in>set []. \<not> f x);
liftM Inl a
od
odE)
 2. \<And>aa xs. (case find f xs of None \<Rightarrow> a | Some a \<Rightarrow> return a) = liftM projl (doE x <- mapME (\<lambda>x. if f x then throwError x else returnOk ()) xs;
do _ <- assert (\<forall>x\<in>set xs. \<not> f x);
liftM Inl a
od
odE) \<Longrightarrow> (case find f (aa # xs) of None \<Rightarrow> a | Some a \<Rightarrow> return a) = liftM projl (doE x <- mapME (\<lambda>x. if f x then throwError x else returnOk ()) (aa # xs);
do _ <- assert (\<forall>x\<in>set (aa # xs). \<not> f x);
liftM Inl a
od
odE) proof (prove)
goal (2 subgoals):
 1. a = liftM projl (doE x <- mapME (\<lambda>x. if f x then throwError x else returnOk ()) [];
liftM Inl a
odE)
 2. \<And>aa xs. (case find f xs of None \<Rightarrow> a | Some a \<Rightarrow> return a) = liftM projl (doE x <- mapME (\<lambda>x. if f x then throwError x else returnOk ()) xs;
do _ <- assert (\<forall>x\<in>set xs. \<not> f x);
liftM Inl a
od
odE) \<Longrightarrow> (case find f (aa # xs) of None \<Rightarrow> a | Some a \<Rightarrow> return a) = liftM projl (doE x <- mapME (\<lambda>x. if f x then throwError x else returnOk ()) (aa # xs);
do _ <- assert (\<forall>x\<in>set (aa # xs). \<not> f x);
liftM Inl a
od
odE) proof (prove)
goal (1 subgoal):
 1. \<And>aa xs. (case find f xs of None \<Rightarrow> a | Some a \<Rightarrow> return a) = liftM projl (doE x <- mapME (\<lambda>x. if f x then throwError x else returnOk ()) xs;
do _ <- assert (\<forall>x\<in>set xs. \<not> f x);
liftM Inl a
od
odE) \<Longrightarrow> (case find f (aa # xs) of None \<Rightarrow> a | Some a \<Rightarrow> return a) = liftM projl (doE x <- mapME (\<lambda>x. if f x then throwError x else returnOk ()) (aa # xs);
do _ <- assert (\<forall>x\<in>set (aa # xs). \<not> f x);
liftM Inl a
od
odE) proof (prove)
goal (1 subgoal):
 1. \<And>aa xs. (case find f xs of None \<Rightarrow> a | Some a \<Rightarrow> return a) = liftM projl (doE x <- mapME (\<lambda>x. if f x then throwError x else returnOk ()) xs;
do _ <- assert (\<forall>x\<in>set xs. \<not> f x);
liftM Inl a
od
odE) \<Longrightarrow> (f aa \<longrightarrow> return aa = liftM projl (throwError aa)) \<and> (\<not> f aa \<longrightarrow> liftM projl (doE x <- mapME (\<lambda>x. if f x then throwError x else returnOk ()) xs;
do _ <- assert (\<forall>x\<in>set xs. \<not> f x);
liftM Inl a
od
odE) = liftM projl (doE x <- doE ys <- mapME (\<lambda>x. if f x then throwError x else returnOk ()) xs;
returnOk (() # ys)
odE;
do _ <- assert (\<forall>x\<in>set xs. \<not> f x);
liftM Inl a
od
odE)) proof (prove)
goal (1 subgoal):
 1. \<And>aa xs. \<lbrakk>(case find f xs of None \<Rightarrow> a | Some a \<Rightarrow> return a) = do x <- mapME (\<lambda>x. if f x then throwError x else returnOk ()) xs;
x <- lift (\<lambda>x. do _ <- assert (\<forall>x\<in>set xs. \<not> f x);
x <- a;
return (Inl x)
od) x;
return (projl x)
od; \<not> f aa\<rbrakk> \<Longrightarrow> do x <- mapME (\<lambda>x. if f x then throwError x else returnOk ()) xs;
x <- lift (\<lambda>x. do _ <- assert (\<forall>x\<in>set xs. \<not> f x);
x <- a;
return (Inl x)
od) x;
return (projl x)
od = do x <- mapME (\<lambda>x. if f x then throwError x else returnOk ()) xs;
x <- lift (\<lambda>ys. returnOk (() # ys)) x;
x <- lift (\<lambda>x. do _ <- assert (\<forall>x\<in>set xs. \<not> f x);
x <- a;
return (Inl x)
od) x;
return (projl x)
od proof (prove)
goal (1 subgoal):
 1. \<And>aa xs v s s'. \<lbrakk>(case find f xs of None \<Rightarrow> a | Some a \<Rightarrow> return a) = do x <- mapME (\<lambda>x. if f x then throwError x else returnOk ()) xs;
x <- lift (\<lambda>x. do _ <- assert (\<forall>x\<in>set xs. \<not> f x);
x <- a;
return (Inl x)
od) x;
return (projl x)
od; \<not> f aa; (v, s') \<in> fst (mapME (\<lambda>x. if f x then throwError x else returnOk ()) xs s)\<rbrakk> \<Longrightarrow> (do x <- lift (\<lambda>x. do _ <- assert (\<forall>x\<in>set xs. \<not> f x);
x <- a;
return (Inl x)
od) v;
return (projl x)
od) s' = (do x <- lift (\<lambda>ys. returnOk (() # ys)) v;
x <- lift (\<lambda>x. do _ <- assert (\<forall>x\<in>set xs. \<not> f x);
x <- a;
return (Inl x)
od) x;
return (projl x)
od) s' proof (prove)
goal:
No subgoals!