From 4404c5137d6095f4107da501e90df1078bbbc87f Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Wed, 13 Jul 2022 17:32:07 +1000 Subject: [PATCH] lib: more opt_map lemmas - equality proof by focussing on the left side of an |> - relationship between obind and opt_map Signed-off-by: Gerwin Klein --- lib/Monad_WP/OptionMonad.thy | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/lib/Monad_WP/OptionMonad.thy b/lib/Monad_WP/OptionMonad.thy index 3b8f8ef0b..a9c7c6610 100644 --- a/lib/Monad_WP/OptionMonad.thy +++ b/lib/Monad_WP/OptionMonad.thy @@ -140,6 +140,10 @@ lemma case_opt_map_distrib: = ((\s. case_option None (g |> h) (f s)))" by (fastforce simp: opt_map_def split: option.splits) +lemma opt_map_apply_left_eq: + "f s = f s' \ (f |> g) s = (f |> g) s'" + by (simp add: opt_map_def) + declare None_upd_eq[simp] (* None_upd_eq[simp] so that this pattern is by simp. Hopefully not too much slowdown. *) @@ -456,6 +460,10 @@ lemma if_comp_dist: "(if P then f else g) o h = (if P then f o h else g o h)" by auto +lemma obindK_is_opt_map: + "f \ (\x. K $ g x) = f |> g" + by (simp add: obind_def opt_map_def K_def) + section \"While" loops over option monad.\