src/HOL/Datatype.thy
changeset 14187 26dfcd0ac436
parent 13635 c41e88151b54
child 14208 144f45277d5a
     1.1 --- a/src/HOL/Datatype.thy	Thu Sep 11 22:33:12 2003 +0200
     1.2 +++ b/src/HOL/Datatype.thy	Sun Sep 14 17:53:27 2003 +0200
     1.3 @@ -194,9 +194,17 @@
     1.4  lemma option_map_Some [simp]: "option_map f (Some x) = Some (f x)"
     1.5    by (simp add: option_map_def)
     1.6  
     1.7 +lemma option_map_is_None[iff]:
     1.8 + "(option_map f opt = None) = (opt = None)"
     1.9 +by (simp add: option_map_def split add: option.split)
    1.10 +
    1.11  lemma option_map_eq_Some [iff]:
    1.12      "(option_map f xo = Some y) = (EX z. xo = Some z & f z = y)"
    1.13 -  by (simp add: option_map_def split add: option.split)
    1.14 +by (simp add: option_map_def split add: option.split)
    1.15 +
    1.16 +lemma option_map_comp:
    1.17 + "option_map f (option_map g opt) = option_map (f o g) opt"
    1.18 +by (simp add: option_map_def split add: option.split)
    1.19  
    1.20  lemma option_map_o_sum_case [simp]:
    1.21      "option_map f o sum_case g h = sum_case (option_map f o g) (option_map f o h)"