2525
|
1 |
(* Title: HOL/MiniML/Maybe.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Wolfgang Naraschewski and Tobias Nipkow
|
|
4 |
Copyright 1996 TU Muenchen
|
|
5 |
*)
|
1300
|
6 |
|
2525
|
7 |
(* constructor laws for option_bind *)
|
|
8 |
goalw thy [option_bind_def] "option_bind (Some s) f = (f s)";
|
1300
|
9 |
by (Simp_tac 1);
|
2525
|
10 |
qed "option_bind_Some";
|
1300
|
11 |
|
2525
|
12 |
goalw thy [option_bind_def] "option_bind None f = None";
|
|
13 |
by (Simp_tac 1);
|
|
14 |
qed "option_bind_None";
|
1300
|
15 |
|
2525
|
16 |
Addsimps [option_bind_Some,option_bind_None];
|
|
17 |
|
|
18 |
(* expansion of option_bind *)
|
1300
|
19 |
goal thy
|
2525
|
20 |
"P(option_bind res f) = ((res = None --> P None) & (!s. res = Some s --> P(f s)))";
|
|
21 |
by (option.induct_tac "res" 1);
|
1300
|
22 |
by (fast_tac (HOL_cs addss !simpset) 1);
|
|
23 |
by (Asm_simp_tac 1);
|
2525
|
24 |
qed "expand_option_bind";
|
1751
|
25 |
|
2625
|
26 |
goal thy
|
2525
|
27 |
"((option_bind m f) = None) = ((m=None) | (? p. m = Some p & f p = None))";
|
3919
|
28 |
by(simp_tac (!simpset addsplits [expand_option_bind]) 1);
|
2525
|
29 |
qed "option_bind_eq_None";
|
1757
|
30 |
|
2525
|
31 |
Addsimps [option_bind_eq_None];
|
2625
|
32 |
|
|
33 |
(* auxiliary lemma *)
|
|
34 |
goal Maybe.thy "(y = Some x) = (Some x = y)";
|
|
35 |
by( simp_tac (!simpset addsimps [eq_sym_conv]) 1);
|
|
36 |
qed "rotate_Some";
|