equal
deleted
inserted
replaced
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 goal thy |
19 goalw thy [option_bind_def] "P(option_bind res f) = \ |
20 "P(option_bind res f) = ((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 (option.induct_tac "res" 1); |
21 br split_option_case 1; |
22 by (fast_tac (HOL_cs addss !simpset) 1); |
22 qed "split_option_bind"; |
23 by (Asm_simp_tac 1); |
|
24 qed "expand_option_bind"; |
|
25 |
23 |
26 goal thy |
24 goal thy |
27 "((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))"; |
28 by(simp_tac (!simpset addsplits [expand_option_bind]) 1); |
26 by(simp_tac (!simpset addsplits [split_option_bind]) 1); |
29 qed "option_bind_eq_None"; |
27 qed "option_bind_eq_None"; |
30 |
28 |
31 Addsimps [option_bind_eq_None]; |
29 Addsimps [option_bind_eq_None]; |
32 |
30 |
33 (* auxiliary lemma *) |
31 (* auxiliary lemma *) |