errorMonadScript.sml

1Theory errorMonad
2
3Datatype: error = return 'a | error 'e
4End
5
6Theorem EXISTS_ERROR:
7  (?e:('a,'e)error. P e) <=> (?a. P (return a)) \/ (?e. P (error e))
8Proof
9  iff_tac >> strip_tac
10  >- (Cases_on ‘e’ >> simp[] >> metis_tac[]) >>
11  first_assum $ irule_at Any
12QED
13
14Theorem FORALL_ERROR:
15  (!e:('a,'e)error. P e) <=> (!a. P (return a)) /\ !e. P (error e)
16Proof
17  simp[EQ_IMP_THM] >> strip_tac >> Cases >> simp[]
18QED
19
20Definition bind_def[simp]:
21  bind (return v) f = f v /\
22  bind (error e) f = error e
23End
24
25Definition try_def[simp]:
26  try (return v) f = return v ∧
27  try (error e) f = f e
28End
29
30Definition choice_def:
31  choice (return v) m = return v /\
32  choice (error e) m = m
33End
34
35Definition guard_def:
36  guard e b = if b then return () else error e
37End
38
39Theorem bind_return:
40  bind m return = m
41Proof
42  Cases_on ‘m’ >> simp[]
43QED
44
45Theorem bind_EQ_return:
46  bind m f = return v <=> ?u. m = return u /\ f u = return v
47Proof
48  Cases_on ‘m’ >> simp[]
49QED
50
51Theorem bind_EQ_error:
52  bind m f = error e <=> m = error e \/ ?u. m = return u /\ f u = error e
53Proof
54  Cases_on ‘m’ >> simp[]
55QED
56
57val _ = monadsyntax.declare_monad("error",
58  {bind = “bind”, choice = SOME “choice”, fail = SOME “error”,
59   guard = SOME “guard”, ignorebind = NONE, unit = “return”})
60
61