author | nipkow |
Thu, 24 Apr 1997 18:51:14 +0200 | |
changeset 3044 | 3e3087aa69e7 |
parent 2520 | aecaa76e7eff |
child 3919 | c036caebfc75 |
permissions | -rw-r--r-- |
2520 | 1 |
(* Title: HOL/W0/Maybe.ML |
2 |
ID: $Id$ |
|
3 |
Author: Dieter Nazareth and Tobias Nipkow |
|
4 |
Copyright 1995 TU Muenchen |
|
5 |
*) |
|
6 |
||
2518
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
7 |
|
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
8 |
(* constructor laws for bind *) |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
9 |
goalw thy [bind_def] "(Ok s) bind f = (f s)"; |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
10 |
by (Simp_tac 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
11 |
qed "bind_Ok"; |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
12 |
|
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
13 |
goalw thy [bind_def] "Fail bind f = Fail"; |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
14 |
by (Simp_tac 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
15 |
qed "bind_Fail"; |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
16 |
|
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
17 |
Addsimps [bind_Ok,bind_Fail]; |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
18 |
|
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
19 |
(* expansion of bind *) |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
20 |
goal thy |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
21 |
"P(res bind f) = ((res = Fail --> P Fail) & (!s. res = Ok s --> P(f s)))"; |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
22 |
by (maybe.induct_tac "res" 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
23 |
by (fast_tac (HOL_cs addss !simpset) 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
24 |
by (Asm_simp_tac 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
25 |
qed "expand_bind"; |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
26 |
|
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
27 |
goal Maybe.thy |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
28 |
"((m bind f) = Fail) = ((m=Fail) | (? p. m = Ok p & f p = Fail))"; |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
29 |
by (simp_tac (!simpset setloop (split_tac [expand_bind])) 1); |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
30 |
qed "bind_eq_Fail"; |
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
31 |
|
bee082efaa46
This is the old version og MiniML for the monomorphic case.
nipkow
parents:
diff
changeset
|
32 |
Addsimps [bind_eq_Fail]; |