combinator List.those;
authorhaftmann
Wed Feb 13 13:38:52 2013 +0100 (2013-02-13)
changeset 5109660e4b75fefe1
parent 51095 7ae79f2e3cc7
child 51101 66d0298fc554
child 51102 358b27c56469
combinator List.those;
simprule for case distinction on Option.map expression
src/HOL/List.thy
src/HOL/Option.thy
     1.1 --- a/src/HOL/List.thy	Wed Feb 13 13:38:52 2013 +0100
     1.2 +++ b/src/HOL/List.thy	Wed Feb 13 13:38:52 2013 +0100
     1.3 @@ -162,6 +162,13 @@
     1.4  
     1.5  hide_const (open) find
     1.6  
     1.7 +primrec those :: "'a option list \<Rightarrow> 'a list option"
     1.8 +where
     1.9 +"those [] = Some []" |
    1.10 +"those (x # xs) = (case x of
    1.11 +  None \<Rightarrow> None
    1.12 +| Some y \<Rightarrow> Option.map (Cons y) (those xs))"
    1.13 +
    1.14  primrec remove1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
    1.15  "remove1 x [] = []" |
    1.16  "remove1 x (y # xs) = (if x = y then xs else y # remove1 x xs)"
     2.1 --- a/src/HOL/Option.thy	Wed Feb 13 13:38:52 2013 +0100
     2.2 +++ b/src/HOL/Option.thy	Wed Feb 13 13:38:52 2013 +0100
     2.3 @@ -101,6 +101,10 @@
     2.4    qed
     2.5  qed
     2.6  
     2.7 +lemma option_case_map [simp]:
     2.8 +  "option_case g h (Option.map f x) = option_case g (h \<circ> f) x"
     2.9 +  by (cases x) simp_all
    2.10 +
    2.11  primrec bind :: "'a option \<Rightarrow> ('a \<Rightarrow> 'b option) \<Rightarrow> 'b option" where
    2.12  bind_lzero: "bind None f = None" |
    2.13  bind_lunit: "bind (Some x) f = f x"