(* Author: Christian Sternagel <c.sternagel@gmail.com> Author: René Thiemann <rene.thiemann@uibk.ac.at> License: LGPL *) subsection ‹The Option Monad› theory Option_Monad imports "HOL-Library.Monad_Syntax" begin declare Option.bind_cong [fundef_cong] definition guard :: "bool ⇒ unit option" where "guard b = (if b then Some () else None)" lemma guard_cong [fundef_cong]: "b = c ⟹ (c ⟹ m = n) ⟹ guard b >> m = guard c >> n" by (simp add: guard_def) lemma guard_simps: "guard b = Some x ⟷ b" "guard b = None ⟷ ¬ b" by (cases b) (simp_all add: guard_def) lemma guard_elims[elim]: "guard b = Some x ⟹ (b ⟹ P) ⟹ P" "guard b = None ⟹ (¬ b ⟹ P) ⟹ P" by (simp_all add: guard_simps) lemma guard_intros [intro, simp]: "b ⟹ guard b = Some ()" "¬ b ⟹ guard b = None" by (simp_all add: guard_simps) lemma guard_True [simp]: "guard True = Some ()" by simp lemma guard_False [simp]: "guard False = None" by simp lemma guard_and_to_bind: "guard (a ∧ b) = guard a ⤜ (λ _. guard b)" by (cases a; cases b; auto) fun zip_option :: "'a list ⇒ 'b list ⇒ ('a × 'b) list option" where "zip_option [] [] = Some []" | "zip_option (x#xs) (y#ys) = do { zs ← zip_option xs ys; Some ((x, y) # zs) }" | "zip_option (x#xs) [] = None" | "zip_option [] (y#ys) = None" text ‹induction scheme for zip› lemma zip_induct [case_names Cons_Cons Nil1 Nil2]: assumes "⋀x xs y ys. P xs ys ⟹ P (x # xs) (y # ys)" and "⋀ys. P [] ys" and "⋀xs. P xs []" shows "P xs ys" using assms by (induction_schema) (pat_completeness, lexicographic_order) lemma zip_option_same[simp]: ✐‹contributor ‹Martin Desharnais›› "zip_option xs xs = Some (zip xs xs)" by (induction xs) simp_all lemma zip_option_zip_conv: "zip_option xs ys = Some zs ⟷ length ys = length xs ∧ length zs = length xs ∧ zs = zip xs ys" proof - { assume "zip_option xs ys = Some zs" hence "length ys = length xs ∧ length zs = length xs ∧ zs = zip xs ys" proof (induct xs ys arbitrary: zs rule: zip_option.induct) case (2 x xs y ys) then obtain zs' where "zip_option xs ys = Some zs'" and "zs = (x, y) # zs'" by (cases "zip_option xs ys") auto from 2(1) [OF this(1)] and this(2) show ?case by simp qed simp_all } moreover { assume "length ys = length xs" and "zs = zip xs ys" hence "zip_option xs ys = Some zs" by (induct xs ys arbitrary: zs rule: zip_induct) force+ } ultimately show ?thesis by blast qed lemma zip_option_None: "zip_option xs ys = None ⟷ length xs ≠ length ys" proof - { assume "zip_option xs ys = None" have "length xs ≠ length ys" proof (rule ccontr) assume "¬ length xs ≠ length ys" hence "length xs = length ys" by simp hence "zip_option xs ys = Some (zip xs ys)" by (simp add: zip_option_zip_conv) with ‹zip_option xs ys = None› show False by simp qed } moreover { assume "length xs ≠ length ys" hence "zip_option xs ys = None" by (induct xs ys rule: zip_option.induct) simp_all } ultimately show ?thesis by blast qed declare zip_option.simps [simp del] lemma zip_option_intros [intro]: "⟦length ys = length xs; length zs = length xs; zs = zip xs ys⟧ ⟹ zip_option xs ys = Some zs" "length xs ≠ length ys ⟹ zip_option xs ys = None" by (simp_all add: zip_option_zip_conv zip_option_None) lemma zip_option_elims [elim]: "zip_option xs ys = Some zs ⟹ (⟦length ys = length xs; length zs = length xs; zs = zip xs ys⟧ ⟹ P) ⟹ P" "zip_option xs ys = None ⟹ (length xs ≠ length ys ⟹ P) ⟹ P" by (simp_all add: zip_option_zip_conv zip_option_None) lemma zip_option_simps [simp]: "zip_option xs ys = None ⟹ length xs = length ys ⟹ False" "zip_option xs ys = None ⟹ length xs ≠ length ys" "zip_option xs ys = Some zs ⟹ zs = zip xs ys" by (simp_all add: zip_option_None zip_option_zip_conv) fun mapM :: "('a ⇒ 'b option) ⇒ 'a list ⇒ 'b list option" where "mapM f [] = Some []" | "mapM f (x#xs) = do { y ← f x; ys ← mapM f xs; Some (y # ys) }" lemma mapM_None: "mapM f xs = None ⟷ (∃x∈set xs. f x = None)" proof (induct xs) case (Cons x xs) thus ?case by (cases "f x", simp, cases "mapM f xs", auto) qed simp lemma mapM_Some: "mapM f xs = Some ys ⟹ ys = map (λx. the (f x)) xs ∧ (∀x∈set xs. f x ≠ None)" proof (induct xs arbitrary: ys) case (Cons x xs ys) thus ?case by (cases "f x", simp, cases "mapM f xs", auto) qed simp lemma mapM_Some_idx: assumes some: "mapM f xs = Some ys" and i: "i < length xs" shows "∃y. f (xs ! i) = Some y ∧ ys ! i = y" proof - note m = mapM_Some [OF some] from m[unfolded set_conv_nth] i have "f (xs ! i) ≠ None" by auto then obtain y where "f (xs ! i) = Some y" by auto then have "f (xs ! i) = Some y ∧ ys ! i = y" unfolding m [THEN conjunct1] using i by auto then show ?thesis .. qed lemma mapM_cong [fundef_cong]: assumes "xs = ys" and "⋀x. x ∈ set ys ⟹ f x = g x" shows "mapM f xs = mapM g ys" unfolding assms(1) using assms(2) by (induct ys) auto lemma mapM_map: "mapM f xs = (if (∀x∈set xs. f x ≠ None) then Some (map (λx. the (f x)) xs) else None)" proof (cases "mapM f xs") case None thus ?thesis using mapM_None by auto next case (Some ys) with mapM_Some [OF Some] show ?thesis by auto qed lemma mapM_mono [partial_function_mono]: fixes C :: "'a ⇒ ('b ⇒ 'c option) ⇒ 'd option" assumes C: "⋀y. mono_option (C y)" shows "mono_option (λf. mapM (λy. C y f) B)" proof (induct B) case Nil show ?case unfolding mapM.simps by (rule option.const_mono) next case (Cons b B) show ?case unfolding mapM.simps by (rule bind_mono [OF C bind_mono [OF Cons option.const_mono]]) qed end