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_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