adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

lib: add more opt_map lemmas; opt_map_left_Some, etc. 

Signed-off-by: Miki Tanaka <miki.tanaka@data61.csiro.au>
This commit is contained in:
Miki Tanaka 2020-08-21 11:48:11 +10:00 committed by Gerwin Klein
parent 12c8da5758
commit eda47153d1
1 changed files with 17 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
lib/Monad_WP/OptionMonad.thy
View File

@ -40,6 +40,18 @@ lemma opt_mapE:
"\<lbrakk> (f |> g) s = Some v; \<And>v'. \<lbrakk>f s = Some v'; g v' = Some v \<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"
by (auto simp: in_opt_map_eq)
lemma opt_map_left_Some:
"f x = Some y \<Longrightarrow> (f |> g) x = g y"
by (clarsimp simp: opt_map_def)
lemma opt_map_left_None:
"f x = None \<Longrightarrow> (f |> g) x = None"
by (clarsimp simp: opt_map_def)
lemma opt_map_assoc:
"f |> (g |> h) = f |> g |> h"
by (fastforce simp: opt_map_def split: option.splits)
lemma opt_map_upd_None:
"f(x := None) |> g = (f |> g)(x := None)"
by (auto simp: opt_map_def)
@ -50,6 +62,11 @@ lemma opt_map_upd_Some:
lemmas opt_map_upd[simp] = opt_map_upd_None opt_map_upd_Some
lemma case_opt_map_distrib:
"((\<lambda>s. case_option None g (f s)) |> h)
= ((\<lambda>s. case_option None (g |> h) (f s)))"
by (fastforce simp: opt_map_def split: option.splits)
declare None_upd_eq[simp]
(* None_upd_eq[simp] so that this pattern is by simp. Hopefully not too much slowdown. *)