1300
|
1 |
open Maybe;
|
|
2 |
|
|
3 |
(* constructor laws for bind *)
|
|
4 |
goalw thy [bind_def] "(Ok s) bind f = (f s)";
|
|
5 |
by (Simp_tac 1);
|
|
6 |
qed "bind_Ok";
|
|
7 |
|
|
8 |
goalw thy [bind_def] "Fail bind f = Fail";
|
|
9 |
by (Simp_tac 1);
|
|
10 |
qed "bind_Fail";
|
|
11 |
|
|
12 |
Addsimps [bind_Ok,bind_Fail];
|
|
13 |
|
|
14 |
(* expansion of bind *)
|
|
15 |
goal thy
|
|
16 |
"P(res bind f) = ((res = Fail --> P Fail) & (!s. res = Ok s --> P(f s)))";
|
|
17 |
by (maybe.induct_tac "res" 1);
|
|
18 |
by (fast_tac (HOL_cs addss !simpset) 1);
|
|
19 |
by (Asm_simp_tac 1);
|
|
20 |
qed "expand_bind";
|
1751
|
21 |
|
1757
|
22 |
goal Maybe.thy
|
|
23 |
"((m bind f) = Fail) = ((m=Fail) | (? p. m = Ok p & f p = Fail))";
|
2031
|
24 |
by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1);
|
1757
|
25 |
qed "bind_eq_Fail";
|
|
26 |
|
|
27 |
Addsimps [bind_eq_Fail];
|