src/HOL/Option.thy
changeset 58916 229765cc3414
parent 58895 de0a4a76d7aa
child 59521 ef8ac8d2315e
     1.1 --- a/src/HOL/Option.thy	Fri Nov 07 12:24:56 2014 +0100
     1.2 +++ b/src/HOL/Option.thy	Fri Nov 07 11:28:37 2014 +0100
     1.3 @@ -5,7 +5,7 @@
     1.4  section {* Datatype option *}
     1.5  
     1.6  theory Option
     1.7 -imports BNF_Least_Fixpoint Finite_Set
     1.8 +imports Lifting Finite_Set
     1.9  begin
    1.10  
    1.11  datatype 'a option =
    1.12 @@ -114,6 +114,12 @@
    1.13    "case_option g h (map_option f x) = case_option g (h \<circ> f) x"
    1.14    by (cases x) simp_all
    1.15  
    1.16 +lemma rel_option_iff:
    1.17 +  "rel_option R x y = (case (x, y) of (None, None) \<Rightarrow> True
    1.18 +    | (Some x, Some y) \<Rightarrow> R x y
    1.19 +    | _ \<Rightarrow> False)"
    1.20 +by (auto split: prod.split option.split)
    1.21 +
    1.22  primrec bind :: "'a option \<Rightarrow> ('a \<Rightarrow> 'b option) \<Rightarrow> 'b option" where
    1.23  bind_lzero: "bind None f = None" |
    1.24  bind_lunit: "bind (Some x) f = f x"
    1.25 @@ -192,6 +198,20 @@
    1.26  hide_fact (open) bind_cong
    1.27  
    1.28  
    1.29 +subsection {* Transfer rules for the Transfer package *}
    1.30 +
    1.31 +context
    1.32 +begin
    1.33 +interpretation lifting_syntax .
    1.34 +
    1.35 +lemma option_bind_transfer [transfer_rule]:
    1.36 +  "(rel_option A ===> (A ===> rel_option B) ===> rel_option B)
    1.37 +    Option.bind Option.bind"
    1.38 +  unfolding rel_fun_def split_option_all by simp
    1.39 +
    1.40 +end
    1.41 +
    1.42 +
    1.43  subsubsection {* Interaction with finite sets *}
    1.44  
    1.45  lemma finite_option_UNIV [simp]: