4 Copyright 1996 TU Muenchen |
4 Copyright 1996 TU Muenchen |
5 |
5 |
6 Universal error monad. |
6 Universal error monad. |
7 *) |
7 *) |
8 |
8 |
9 Maybe = Main + |
9 theory Maybe = Main: |
10 |
10 |
11 constdefs |
11 constdefs |
12 option_bind :: ['a option, 'a => 'b option] => 'b option |
12 option_bind :: "['a option, 'a => 'b option] => 'b option" |
13 "option_bind m f == case m of None => None | Some r => f r" |
13 "option_bind m f == case m of None => None | Some r => f r" |
14 |
14 |
15 syntax "@option_bind" :: [pttrns,'a option,'b] => 'c ("(_ := _;//_)" 0) |
15 syntax "@option_bind" :: "[pttrns,'a option,'b] => 'c" ("(_ := _;//_)" 0) |
16 translations "P := E; F" == "option_bind E (%P. F)" |
16 translations "P := E; F" == "option_bind E (%P. F)" |
17 |
17 |
|
18 |
|
19 (* constructor laws for option_bind *) |
|
20 lemma option_bind_Some: "option_bind (Some s) f = (f s)" |
|
21 apply (unfold option_bind_def) |
|
22 apply (simp (no_asm)) |
|
23 done |
|
24 |
|
25 lemma option_bind_None: "option_bind None f = None" |
|
26 apply (unfold option_bind_def) |
|
27 apply (simp (no_asm)) |
|
28 done |
|
29 |
|
30 declare option_bind_Some [simp] option_bind_None [simp] |
|
31 |
|
32 (* expansion of option_bind *) |
|
33 lemma split_option_bind: "P(option_bind res f) = |
|
34 ((res = None --> P None) & (!s. res = Some s --> P(f s)))" |
|
35 apply (unfold option_bind_def) |
|
36 apply (rule option.split) |
|
37 done |
|
38 |
|
39 lemma option_bind_eq_None: |
|
40 "((option_bind m f) = None) = ((m=None) | (? p. m = Some p & f p = None))" |
|
41 apply (simp (no_asm) split add: split_option_bind) |
|
42 done |
|
43 |
|
44 declare option_bind_eq_None [simp] |
|
45 |
|
46 (* auxiliary lemma *) |
|
47 lemma rotate_Some: "(y = Some x) = (Some x = y)" |
|
48 apply ( simp (no_asm) add: eq_sym_conv) |
|
49 done |
|
50 |
18 end |
51 end |