src/HOL/Datatype.thy
changeset 14187 26dfcd0ac436
parent 13635 c41e88151b54
child 14208 144f45277d5a
--- a/src/HOL/Datatype.thy	Thu Sep 11 22:33:12 2003 +0200
+++ b/src/HOL/Datatype.thy	Sun Sep 14 17:53:27 2003 +0200
@@ -194,9 +194,17 @@
 lemma option_map_Some [simp]: "option_map f (Some x) = Some (f x)"
   by (simp add: option_map_def)
 
+lemma option_map_is_None[iff]:
+ "(option_map f opt = None) = (opt = None)"
+by (simp add: option_map_def split add: option.split)
+
 lemma option_map_eq_Some [iff]:
     "(option_map f xo = Some y) = (EX z. xo = Some z & f z = y)"
-  by (simp add: option_map_def split add: option.split)
+by (simp add: option_map_def split add: option.split)
+
+lemma option_map_comp:
+ "option_map f (option_map g opt) = option_map (f o g) opt"
+by (simp add: option_map_def split add: option.split)
 
 lemma option_map_o_sum_case [simp]:
     "option_map f o sum_case g h = sum_case (option_map f o g) (option_map f o h)"