equal
deleted
inserted
replaced
4 Copyright 1995 TU Muenchen |
4 Copyright 1995 TU Muenchen |
5 *) |
5 *) |
6 |
6 |
7 |
7 |
8 (* constructor laws for bind *) |
8 (* constructor laws for bind *) |
9 goalw thy [bind_def] "(Ok s) bind f = (f s)"; |
9 Goalw [bind_def] "(Ok s) bind f = (f s)"; |
10 by (Simp_tac 1); |
10 by (Simp_tac 1); |
11 qed "bind_Ok"; |
11 qed "bind_Ok"; |
12 |
12 |
13 goalw thy [bind_def] "Fail bind f = Fail"; |
13 Goalw [bind_def] "Fail bind f = Fail"; |
14 by (Simp_tac 1); |
14 by (Simp_tac 1); |
15 qed "bind_Fail"; |
15 qed "bind_Fail"; |
16 |
16 |
17 Addsimps [bind_Ok,bind_Fail]; |
17 Addsimps [bind_Ok,bind_Fail]; |
18 |
18 |
19 (* case splitting of bind *) |
19 (* case splitting of bind *) |
20 goal thy |
20 Goal |
21 "P(res bind f) = ((res = Fail --> P Fail) & (!s. res = Ok s --> P(f s)))"; |
21 "P(res bind f) = ((res = Fail --> P Fail) & (!s. res = Ok s --> P(f s)))"; |
22 by (induct_tac "res" 1); |
22 by (induct_tac "res" 1); |
23 by (fast_tac (HOL_cs addss simpset()) 1); |
23 by (fast_tac (HOL_cs addss simpset()) 1); |
24 by (Asm_simp_tac 1); |
24 by (Asm_simp_tac 1); |
25 qed "split_bind"; |
25 qed "split_bind"; |
26 |
26 |
27 goal Maybe.thy |
27 Goal |
28 "((m bind f) = Fail) = ((m=Fail) | (? p. m = Ok p & f p = Fail))"; |
28 "((m bind f) = Fail) = ((m=Fail) | (? p. m = Ok p & f p = Fail))"; |
29 by (simp_tac (simpset() addsplits [split_bind]) 1); |
29 by (simp_tac (simpset() addsplits [split_bind]) 1); |
30 qed "bind_eq_Fail"; |
30 qed "bind_eq_Fail"; |
31 |
31 |
32 Addsimps [bind_eq_Fail]; |
32 Addsimps [bind_eq_Fail]; |