equal
deleted
inserted
replaced
21 br split_option_case 1; |
21 br split_option_case 1; |
22 qed "split_option_bind"; |
22 qed "split_option_bind"; |
23 |
23 |
24 goal thy |
24 goal thy |
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 Maybe.thy "(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"; |