GitLab will be upgraded on 31 Jan 2023 from 2.00 pm (AEDT) to 3.00 pm (AEDT). During the update, GitLab and Mattermost services will not be available. If you have any concerns with this, please talk to us at N110 (b) CSIT building.

sumMonadScript.sml 5.54 KB
Newer Older
1
open HolKernel Parse boolLib bossLib;
2
3
open sumSyntax
open DefineUtils
4
5
6
7
8
9
10
11

(* A monad for sum types, roughly equivalent to Haskell's `Either` monad. It
   favors the left side of a sum type (although `bind_right` can be used to bind
   over the right side instead). Also contains several utility functions for sum
   types.
*)
val _ = new_theory "sumMonad"

12
val _ = define_monad("left", (fn a => mk_sum(a, mk_vartype "'right")), 
13
  ``INL``, ``λx fn. sum_CASE x fn INR``)
14

15
(*
16
17
18
val return_left_INL = store_thm("return_left_INL[simp]",
  ``return_left x = INL x``,
  simp[definition "return_left_def"])
19
*)
20

21
val bind_left_INR_simp = store_thm("bind_left_INR_simp[simp]",
22
  ``bind_left (INR x) f = INR x``, simp[])
23

24
25
val bind_left_INL = store_thm("bind_left_INL[simp]",
  ``(bind_left x f = INL y) = y0. (x = INL y0)  (f y0 = INL y)``,
26
  Cases_on `x` >> simp[])
27

28
29
val bind_left_INR = store_thm("bind_left_INR",
  ``(y. x = INR y)  f. bind_left x f = x``,
30
  Cases_on `x` >> simp[])
31
32


33
34
35
36
37
38
39
val bind_right_def = Define`
  bind_right (sum : α + β) (fn : β -> α + γ) : α + γ =
    case sum of
    | INL a => INL a
    | INR b => fn b
`

40
41
val bind_right_INR = store_thm("bind_right_INR[simp]",
  ``(bind_right x f = INR y) = y0. (x = INR y0)  (f y0 = INR y)``,
42
43
  Cases_on `x` >> simp[bind_right_def])

44
45
val bind_right_INL = store_thm("bind_right_INL",
  ``(y. x = INL y)  f. bind_right x f = x``,
46
47
  Cases_on `x` >> simp[bind_right_def])

48
49
50
val lift_left_INL = store_thm("lift_left_INL[simp]",
  ``(lift_left f x = INL y) = y0. (x = INL y0)  (y = f y0)``,
  Cases_on `x` >> simp[definition "lift_left_def", bind_left_INL] >> metis_tac[])
51

52
53
val lift_left_INR = store_thm("lift_left_INR[simp]",
  ``(lift_left f x = INR y) = (x = INR y)``,
54
  Cases_on `x` >> simp[definition "lift_left_def"])
55

56
57
val lift_left_id = store_thm("lift_left_id[simp]",
  ``lift_left I x = x``,
58
  Cases_on `x` >> simp[definition "lift_left_def"])
Adam R. Nelson's avatar
Adam R. Nelson committed
59

60
61
val lift_left_compose = store_thm("lift_left_compose[simp]",
  ``lift_left (f o g) x = lift_left f (lift_left g x)``,
62
  Cases_on `x` >> simp[definition "lift_left_def"])
63

64
65
val lift_right_def = Define`
  lift_right (f : α -> β) (sum : γ + α) : γ + β =
66
    bind_right sum (INR o f)
67
68
`

69
70
val lift_right_INR = store_thm("lift_right_INR[simp]",
  ``(lift_right f x = INR y) = y0. (x = INR y0)  (y = f y0)``,
71
72
  Cases_on `x` >> simp[lift_right_def, bind_right_INR] >> metis_tac[])

73
74
val lift_right_INL = store_thm("lift_right_INL[simp]",
  ``(lift_right f x = INL y) = (x = INL y)``,
75
76
  Cases_on `x` >> simp[lift_right_def, bind_right_def])

77
78
val lift_right_id = store_thm("lift_right_id[simp]",
  ``lift_right I x = x``,
Adam R. Nelson's avatar
Adam R. Nelson committed
79
80
  Cases_on `x` >> simp[lift_right_def, bind_right_def])

81
82
val lift_right_compose = store_thm("lift_right_compose[simp]",
  ``lift_right (f o g) x = lift_right f (lift_right g x)``,
Adam R. Nelson's avatar
Adam R. Nelson committed
83
84
  Cases_on `x` >> simp[lift_right_def, bind_right_def])

85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
(* Merge left side of sum into right side *)
val merge_right_def = Define`
  merge_right (f : α -> β) (sum : α + β) : β =
    case sum of
    | INL a => f a
    | INR b => b
`

(* Merge right side of sum into left side *)
val merge_left_def = Define`
  merge_left (f : β -> α) (sum : α + β) : α =
    case sum of
    | INL a => a
    | INR b => f b
`

val left_set_def = Define`
102
  left_set (sum : α + β) = case sum of INL a => {a} | INR _ => 
103
104
105
`

val right_set_def = Define`
106
107
108
109
110
111
112
113
114
  right_set (sum : α + β) = case sum of INL _ =>  | INR b => {b}
`

val left_list_def = Define`
  left_list (sum : α + β) = case sum of INL a => [a] | INR _ => []
`

val right_list_def = Define`
  right_list (sum : α + β) = case sum of INL _ => [] | INR b => [b]
115
116
`

117
(* Monad laws for bind_left: left identity, right identity, and associativity *)
118
val bind_left_monad_left_id = store_thm("bind_left_monad_left_id[simp]",
119
  ``bind_left (INL a) f = f a``, simp[])
120
121
val bind_left_monad_right_id = store_thm("bind_left_monad_right_id[simp]",
  ``bind_left m INL = m``,
122
  Cases_on `m` >> simp[])
123
124
val bind_left_monad_assoc = store_thm("bind_left_monad_assoc",
  ``bind_left (bind_left m f) g = bind_left m (λx. bind_left (f x) g)``,
125
126
127
  Cases_on `m` >> simp[])
val _ = computeLib.add_funs[
  ]
128
129

(* Monad laws for bind_right: left identity, right identity, and associativity *)
130
131
132
133
134
135
val bind_right_monad_left_id = store_thm("bind_right_monad_left_id[simp]",
  ``bind_right (INR a) f = f a``, simp[bind_right_def])
val bind_right_monad_right_id = store_thm("bind_right_monad_right_id[simp]",
  ``bind_right m INR = m``, Cases_on `m` >> simp[bind_right_def])
val bind_right_monad_assoc = store_thm("bind_right_monad_assoc",
  ``bind_right (bind_right m f) g = bind_right m (λx. bind_right (f x) g)``,
136
137
  Cases_on `m` >> simp[bind_right_def])

138
139
140
141
142
143
144
145
146
147
148
(* Applicative laws for ap_left *)
val ap_left_identity = store_thm("ap_left_identity",
  ``INL I <*> v = v``,
  rw[definition "ap_left_def"] >> metis_tac[bind_left_monad_right_id])

(* TODO: homomorphism, interchange *)

val ap_left_composition = store_thm("ap_left_composition",
  ``INL $o <*> u <*> v <*> w = u <*> (v <*> w)``,
  Cases_on `u` >> Cases_on `v` >> Cases_on `w` >> rw[definition "ap_left_def"])

Adam R. Nelson's avatar
Adam R. Nelson committed
149
(* Other theorems that use the monad laws *)
150
151
val left_set_image = store_thm("left_set_image",
  ``left_set (lift_left f x) = IMAGE f (left_set x)``,
Adam R. Nelson's avatar
Adam R. Nelson committed
152
  Cases_on `x`
153
  >- simp[definition "lift_left_def", left_set_def]
Adam R. Nelson's avatar
Adam R. Nelson committed
154
155
  >- simp[left_set_def, METIS_PROVE [lift_left_INR] ``lift_left f (INR y) = INR y``])

156
157
val bind_left_unit_INL = store_thm("bind_left_unit_INL[simp]",
  ``monad_unitbind (INL a) b = b``, simp[])
158

159
val bind_left_unit_INR = store_thm("bind_left_unit_INR[simp]",
160
  ``monad_unitbind (INR a) b = INR a``, simp[])
161

162
val _ = export_theory()
163