3 Author: Wolfgang Naraschewski and Tobias Nipkow |
3 Author: Wolfgang Naraschewski and Tobias Nipkow |
4 Copyright 1996 TU Muenchen |
4 Copyright 1996 TU Muenchen |
5 *) |
5 *) |
6 |
6 |
7 (* constructor laws for option_bind *) |
7 (* constructor laws for option_bind *) |
8 goalw thy [option_bind_def] "option_bind (Some s) f = (f s)"; |
8 Goalw [option_bind_def] "option_bind (Some s) f = (f s)"; |
9 by (Simp_tac 1); |
9 by (Simp_tac 1); |
10 qed "option_bind_Some"; |
10 qed "option_bind_Some"; |
11 |
11 |
12 goalw thy [option_bind_def] "option_bind None f = None"; |
12 Goalw [option_bind_def] "option_bind None f = None"; |
13 by (Simp_tac 1); |
13 by (Simp_tac 1); |
14 qed "option_bind_None"; |
14 qed "option_bind_None"; |
15 |
15 |
16 Addsimps [option_bind_Some,option_bind_None]; |
16 Addsimps [option_bind_Some,option_bind_None]; |
17 |
17 |
18 (* expansion of option_bind *) |
18 (* expansion of option_bind *) |
19 goalw thy [option_bind_def] "P(option_bind res f) = \ |
19 Goalw [option_bind_def] "P(option_bind res f) = \ |
20 \ ((res = None --> P None) & (!s. res = Some s --> P(f s)))"; |
20 \ ((res = None --> P None) & (!s. res = Some s --> P(f s)))"; |
21 by (rtac split_option_case 1); |
21 by (rtac split_option_case 1); |
22 qed "split_option_bind"; |
22 qed "split_option_bind"; |
23 |
23 |
24 goal thy |
24 Goal |
25 "((option_bind m f) = None) = ((m=None) | (? p. m = Some p & f p = None))"; |
25 "((option_bind m f) = None) = ((m=None) | (? p. m = Some p & f p = None))"; |
26 by (simp_tac (simpset() addsplits [split_option_bind]) 1); |
26 by (simp_tac (simpset() addsplits [split_option_bind]) 1); |
27 qed "option_bind_eq_None"; |
27 qed "option_bind_eq_None"; |
28 |
28 |
29 Addsimps [option_bind_eq_None]; |
29 Addsimps [option_bind_eq_None]; |
30 |
30 |
31 (* auxiliary lemma *) |
31 (* auxiliary lemma *) |
32 goal Maybe.thy "(y = Some x) = (Some x = y)"; |
32 Goal "(y = Some x) = (Some x = y)"; |
33 by ( simp_tac (simpset() addsimps [eq_sym_conv]) 1); |
33 by ( simp_tac (simpset() addsimps [eq_sym_conv]) 1); |
34 qed "rotate_Some"; |
34 qed "rotate_Some"; |