optionScript.sml
1(* =======================================================================*)
2(* FILE : optionScript.sml *)
3(* DESCRIPTION : Creates a theory of SML like options *)
4(* WRITES FILES : option.th *)
5(* *)
6(* AUTHOR : (c) D. Syme 1988 *)
7(* DATE : 95.04.25 *)
8(* REVISED : (Konrad Slind) Oct 9.97 to eliminate usage of *)
9(* recursive types package. Follows the development of *)
10(* Elsa Gunter in her formalization of partial functions. *)
11(* *)
12(* Dec.1998, in order to fit in with Datatype scheme *)
13(* =======================================================================*)
14
15Theory option[bare]
16Ancestors[qualified]
17 sum one relation
18Libs
19 HolKernel Parse boolLib metisLib DefnBase[qualified] simpLib
20 BasicProvers OpenTheoryMap[qualified]
21
22(*---------------------------------------------------------------------------*
23 * Define the new type. The representing type is 'a + one. The development *
24 * is adapted from Elsa Gunter's development of an option type in her *
25 * holML formalization (she called it "lift"). *
26 *---------------------------------------------------------------------------*)
27
28Theorem option_not_empty[local]:
29 ?x:'a + one. (\x.T) x
30Proof
31 BETA_TAC THEN EXISTS_TAC“x:'a + one” THEN ACCEPT_TAC TRUTH
32QED
33val option_TY_DEF = new_type_definition ("option", option_not_empty);
34
35local
36 val ns = ["Data","Option"]
37 val _ = OpenTheoryMap.OpenTheory_tyop_name
38 {tyop={Thy="option",Tyop="option"},name=(ns,"option")}
39in
40 fun ot0 x y =
41 OpenTheoryMap.OpenTheory_const_name{const={Thy="option",Name=x},name=(ns,y)}
42 fun ot x = ot0 x x
43end
44
45(*---------------------------------------------------------------------------*
46 * val option_REP_ABS_DEF = *
47 * |- (!a. option_ABS (option_REP a) = a) /\ *
48 * (!r. (\x. T) r = option_REP (option_ABS r) = r) *
49 *---------------------------------------------------------------------------*)
50
51val option_REP_ABS_DEF =
52 define_new_type_bijections
53 {name = "option_REP_ABS_DEF",
54 ABS = "option_ABS", REP = "option_REP",
55 tyax = option_TY_DEF};
56
57fun reduce thm = REWRITE_RULE[](BETA_RULE thm);
58
59(*---------------------------------------------------------------------------*
60 * option_ABS_ONE_ONE = |- !r r'. (option_ABS r = option_ABS r') = r = r' *
61 * option_ABS_ONTO = |- !a. ?r. a = option_ABS r *
62 * option_REP_ONE_ONE = |- !a a'. (option_REP a = option_REP a') = a = a' *
63 * option_REP_ONTO = |- !r. ?a. r = option_REP a *
64 *---------------------------------------------------------------------------*)
65
66val option_ABS_ONE_ONE = reduce(prove_abs_fn_one_one option_REP_ABS_DEF);
67val option_ABS_ONTO = reduce(prove_abs_fn_onto option_REP_ABS_DEF);
68val option_REP_ONE_ONE = prove_rep_fn_one_one option_REP_ABS_DEF;
69val option_REP_ONTO = reduce(prove_rep_fn_onto option_REP_ABS_DEF);
70
71val SOME_DEF = new_definition(
72 "SOME_DEF[notuserdef]",“!x. SOME x = option_ABS(INL x)”
73);
74val NONE_DEF = new_definition(
75 "NONE_DEF[notuserdef]",
76 “NONE = option_ABS(INR one)”
77);
78val _ = ot0 "SOME" "some"
79val _ = ot0 "NONE" "none"
80
81Theorem option_Axiom:
82 !e f:'a -> 'b. ?fn. (fn NONE = e) /\ (!x. fn (SOME x) = f x)
83Proof
84 REPEAT GEN_TAC THEN
85 PURE_REWRITE_TAC[SOME_DEF,NONE_DEF] THEN
86 STRIP_ASSUME_TAC
87 (BETA_RULE
88 (ISPECL [“\x. f x”, “\x:one.(e:'b)”]
89 (INST_TYPE [Type.beta |-> Type`:one`]
90 sumTheory.sum_Axiom))) THEN
91 EXISTS_TAC “\x:'a option. h(option_REP x):'b” THEN BETA_TAC THEN
92 ASM_REWRITE_TAC[reduce option_REP_ABS_DEF]
93QED
94
95Theorem option_induction:
96 !P. P NONE /\ (!a. P (SOME a)) ==> !x. P x
97Proof
98 GEN_TAC THEN PURE_REWRITE_TAC [SOME_DEF, NONE_DEF] THEN
99 REPEAT STRIP_TAC THEN
100 ONCE_REWRITE_TAC [GSYM (CONJUNCT1 option_REP_ABS_DEF)] THEN
101 SPEC_TAC (Term`option_REP (x:'a option)`, Term`s:'a + one`) THEN
102 HO_MATCH_MP_TAC sumTheory.sum_INDUCT THEN
103 ONCE_REWRITE_TAC [oneTheory.one] THEN ASM_REWRITE_TAC []
104QED
105
106Theorem option_nchotomy =
107 prove_cases_thm option_induction
108 |> hd
109 |> CONV_RULE (RENAME_VARS_CONV ["opt"] THENC
110 BINDER_CONV (RAND_CONV (RENAME_VARS_CONV ["x"])));
111
112val [option_case_def] = Prim_rec.define_case_constant option_Axiom
113val _ = ot0 "option_case" "case"
114Overload case = ``option_CASE``
115val _ = export_rewrites ["option_case_def"]
116
117(* get the names right for Cases_on ‘option’ for proofs that depend on the
118 SOME variable being an x
119*)
120val _ = TypeBase.export (
121 TypeBasePure.gen_datatype_info
122 {ax=option_Axiom, case_defs=[option_case_def], ind=option_induction}
123 |> (fn l => [TypeBasePure.put_nchotomy option_nchotomy (hd l)])
124);
125
126Theorem option_case_lazily[compute] = computeLib.lazyfy_thm option_case_def
127
128Theorem FORALL_OPTION:
129 (!opt. P opt) <=> P NONE /\ !x. P (SOME x)
130Proof METIS_TAC [option_induction]
131QED
132
133Theorem EXISTS_OPTION:
134 (?opt. P opt) <=> P NONE \/ ?x. P (SOME x)
135Proof METIS_TAC [option_nchotomy]
136QED
137
138Theorem SOME_11[simp]:
139 !x y :'a. (SOME x = SOME y) <=> (x=y)
140Proof
141 REWRITE_TAC [SOME_DEF,option_ABS_ONE_ONE,sumTheory.INR_INL_11]
142QED
143val _ = computeLib.add_persistent_funs ["SOME_11"]
144
145Theorem NOT_NONE_SOME[simp]:
146 !x:'a. ~(NONE = SOME x)
147Proof
148 REWRITE_TAC [SOME_DEF,NONE_DEF,option_ABS_ONE_ONE,sumTheory.INR_neq_INL]
149QED
150(* [simp] not needed, as simplifier automatically flips the equality for us *)
151Theorem NOT_SOME_NONE = GSYM NOT_NONE_SOME
152val _ = computeLib.add_persistent_funs ["NOT_NONE_SOME", "NOT_SOME_NONE"]
153
154
155val OPTION_MAP_DEF = new_recursive_definition
156 {name="OPTION_MAP_DEF",
157 rec_axiom=option_Axiom,
158 def = “(OPTION_MAP (f:'a->'b) (SOME x) = SOME (f x)) /\
159 (OPTION_MAP f NONE = NONE)”};
160val _ = export_rewrites ["OPTION_MAP_DEF"]
161val _ = computeLib.add_persistent_funs ["OPTION_MAP_DEF"]
162val _ = ot0 "OPTION_MAP" "map"
163
164Theorem IS_SOME_DEF[compute,simp,allow_rebind] = new_recursive_definition
165 {name="IS_SOME_DEF",
166 rec_axiom=option_Axiom,
167 def = “(IS_SOME (SOME x) = T) /\ (IS_SOME NONE = F)”};
168val _ = ot0 "IS_SOME" "isSome"
169
170Theorem IS_NONE_DEF[compute,simp,allow_rebind] = new_recursive_definition {
171 name = "IS_NONE_DEF",
172 rec_axiom = option_Axiom,
173 def = Term`(IS_NONE (SOME x) = F) /\ (IS_NONE NONE = T)`};
174val _ = ot0 "IS_NONE" "isNone"
175
176Theorem THE_DEF[compute,simp,allow_rebind] = new_recursive_definition
177 {name="THE_DEF",
178 rec_axiom=option_Axiom,
179 def = Term `THE (SOME x) = x`};
180val _ = ot0 "THE" "the"
181
182val OPTION_MAP2_DEF = Q.new_definition(
183 "OPTION_MAP2_DEF",
184 `OPTION_MAP2 f x y =
185 if IS_SOME x /\ IS_SOME y
186 then SOME (f (THE x) (THE y))
187 else NONE`);
188
189Theorem OPTION_JOIN_DEF[compute,simp,allow_rebind] = new_recursive_definition
190 {name = "OPTION_JOIN_DEF",
191 rec_axiom = option_Axiom,
192 def = Term`(OPTION_JOIN NONE = NONE) /\
193 (OPTION_JOIN (SOME x) = x)`};
194val _ = ot0 "OPTION_JOIN" "join"
195
196val option_rws =
197 [IS_SOME_DEF, THE_DEF, IS_NONE_DEF, option_nchotomy,
198 NOT_NONE_SOME,NOT_SOME_NONE, SOME_11, option_case_def,
199 OPTION_MAP_DEF, OPTION_JOIN_DEF];
200
201Theorem OPTION_MAP2_THM[simp]:
202 (OPTION_MAP2 f (SOME x) (SOME y) = SOME (f x y)) /\
203 (OPTION_MAP2 f (SOME x) NONE = NONE) /\
204 (OPTION_MAP2 f NONE (SOME y) = NONE) /\
205 (OPTION_MAP2 f NONE NONE = NONE)
206Proof
207 REWRITE_TAC (OPTION_MAP2_DEF::option_rws)
208QED
209Overload lift2[inferior] = ``OPTION_MAP2``
210val _ = computeLib.add_persistent_funs ["OPTION_MAP2_THM"]
211
212val option_rws = OPTION_MAP2_THM::option_rws;
213
214Theorem ex1_rw[local]:
215 !x. (?y. x = y) /\ (?y. y = x)
216Proof
217 GEN_TAC THEN CONJ_TAC THEN EXISTS_TAC (Term`x`) THEN REFL_TAC
218QED
219
220fun OPTION_CASES_TAC t = STRUCT_CASES_TAC (ISPEC t option_nchotomy);
221
222Theorem IS_SOME_EXISTS:
223 !opt. IS_SOME opt <=> ?x. opt = SOME x
224Proof
225 GEN_TAC THEN (Q_TAC OPTION_CASES_TAC`opt`) THEN
226 SRW_TAC[][IS_SOME_DEF]
227QED
228
229Theorem IS_NONE_EQ_NONE[simp]:
230 !x. IS_NONE x = (x = NONE)
231Proof
232 GEN_TAC THEN OPTION_CASES_TAC “(x :'a option)” THEN
233 ASM_REWRITE_TAC option_rws
234QED
235
236Theorem NOT_IS_SOME_EQ_NONE[simp]:
237 !x. ~(IS_SOME x) = (x = NONE)
238Proof
239 GEN_TAC THEN OPTION_CASES_TAC “(x :'a option)”
240 THEN ASM_REWRITE_TAC option_rws
241QED
242
243Theorem IS_SOME_EQ_NOT_NONE :
244 !x. IS_SOME x <=> x <> NONE
245Proof
246 REWRITE_TAC [GSYM NOT_IS_SOME_EQ_NONE]
247QED
248
249Theorem IS_SOME_EQ_EXISTS[local]:
250 !x. IS_SOME x = (?v. x = SOME v)
251Proof
252 GEN_TAC
253 THEN OPTION_CASES_TAC “(x :'a option)”
254 THEN ASM_REWRITE_TAC (ex1_rw::option_rws)
255QED
256
257
258Theorem IS_SOME_IMP_SOME_THE_CANCEL[local]:
259 !x:'a option. IS_SOME x ==> (SOME (THE x) = x)
260Proof
261 GEN_TAC
262 THEN OPTION_CASES_TAC “(x :'a option)”
263 THEN ASM_REWRITE_TAC option_rws
264QED
265
266Theorem option_case_ID[simp]:
267 !x:'a option. option_CASE x NONE SOME = x
268Proof
269 GEN_TAC THEN OPTION_CASES_TAC “x :'a option” THEN ASM_REWRITE_TAC option_rws
270QED
271
272Theorem IS_SOME_option_case_SOME[local]:
273 !x:'a option. IS_SOME x ==> (option_CASE x e SOME = x)
274Proof
275 GEN_TAC
276 THEN OPTION_CASES_TAC “(x :'a option)”
277 THEN ASM_REWRITE_TAC option_rws
278QED
279
280Theorem option_case_SOME_ID[simp]:
281 !x:'a option. (option_CASE x x SOME = x)
282Proof
283 GEN_TAC THEN OPTION_CASES_TAC “x :'a option” THEN ASM_REWRITE_TAC option_rws
284QED
285
286Theorem IS_SOME_option_case[local]:
287 !x:'a option. IS_SOME x ==> (option_CASE x e (f:'a->'b) = f (THE x))
288Proof
289 GEN_TAC
290 THEN OPTION_CASES_TAC “(x :'a option)”
291 THEN ASM_REWRITE_TAC option_rws
292QED
293
294
295Theorem IS_NONE_option_case[local]:
296 !x:'a option. IS_NONE x ==> (option_CASE x e f = (e:'b))
297Proof
298 GEN_TAC
299 THEN OPTION_CASES_TAC “(x :'a option)”
300 THEN ASM_REWRITE_TAC option_rws
301QED
302
303
304Theorem option_CLAUSES =
305 LIST_CONJ ([SOME_11,THE_DEF,NOT_NONE_SOME,NOT_SOME_NONE]@
306 (CONJUNCTS IS_SOME_DEF)@
307 [IS_NONE_EQ_NONE,
308 NOT_IS_SOME_EQ_NONE,
309 IS_SOME_IMP_SOME_THE_CANCEL,
310 option_case_ID,
311 option_case_SOME_ID,
312 IS_NONE_option_case,
313 IS_SOME_option_case,
314 IS_SOME_option_case_SOME]@
315 CONJUNCTS option_case_def@
316 CONJUNCTS OPTION_MAP_DEF@
317 CONJUNCTS OPTION_JOIN_DEF);
318
319Theorem option_case_compute:
320 option_CASE (x:'a option) (e:'b) f =
321 if IS_SOME x then f (THE x) else e
322Proof
323 OPTION_CASES_TAC “(x :'a option)”
324 THEN ASM_REWRITE_TAC option_rws
325QED
326
327Theorem IF_EQUALS_OPTION[simp]:
328 (((if P then SOME x else NONE) = NONE) <=> ~P) /\
329 (((if P then NONE else SOME x) = NONE) <=> P) /\
330 (((if P then SOME x else NONE) = SOME y) <=> P /\ (x = y)) /\
331 (((if P then NONE else SOME x) = SOME y) <=> ~P /\ (x = y))
332Proof
333 SRW_TAC [][]
334QED
335
336Theorem if_option_eq[simp]:
337 (((if P then X else SOME x) = NONE) <=> P /\ (X = NONE)) /\
338 (((if P then SOME x else X) = NONE) <=> ~P /\ (X = NONE)) /\
339 (((if P then X else NONE) = SOME x) <=> P /\ (X = SOME x)) /\
340 (((if P then NONE else X) = SOME x) <=> ~P /\ (X = SOME x))
341Proof
342 OPTION_CASES_TAC“X:'a option” THEN SRW_TAC [](option_rws)
343QED
344
345Theorem if_option_neq[simp]:
346 (((if P then X else NONE) ≠ NONE) <=> P /\ (X ≠ NONE)) /\
347 (((if P then NONE else X) ≠ NONE) <=> ~P /\ (X ≠ NONE))
348Proof
349 OPTION_CASES_TAC“X:'a option” THEN SRW_TAC [](option_rws)
350QED
351
352Theorem IF_NONE_EQUALS_OPTION:
353 (((if P then X else NONE) = NONE) <=> (P ==> IS_NONE X)) /\
354 (((if P then NONE else X) = NONE) <=> (IS_SOME X ==> P)) /\
355 (((if P then X else NONE) = SOME x) <=> P /\ (X = SOME x)) /\
356 (((if P then NONE else X) = SOME x) <=> ~P /\ (X = SOME x))
357Proof
358 OPTION_CASES_TAC“X:'a option” THEN SRW_TAC [](option_rws)
359QED
360
361(* ----------------------------------------------------------------------
362 OPTION_MAP theorems
363 ---------------------------------------------------------------------- *)
364
365Theorem OPTION_MAP_EQ_SOME[simp]:
366 !f (x:'a option) y.
367 (OPTION_MAP f x = SOME y) = ?z. (x = SOME z) /\ (y = f z)
368Proof
369 REPEAT GEN_TAC THEN OPTION_CASES_TAC “x:'a option” THEN
370 simpLib.SIMP_TAC boolSimps.bool_ss
371 [SOME_11, NOT_NONE_SOME, NOT_SOME_NONE, OPTION_MAP_DEF] THEN
372 mesonLib.MESON_TAC []
373QED
374
375Theorem OPTION_MAP_EQ_NONE:
376 !f x. (OPTION_MAP f x = NONE) = (x = NONE)
377Proof
378 REPEAT GEN_TAC THEN OPTION_CASES_TAC “x:'a option” THEN
379 REWRITE_TAC [option_CLAUSES]
380QED
381
382Theorem OPTION_MAP_EQ_NONE_both_ways[simp]:
383 ((OPTION_MAP f x = NONE) = (x = NONE)) /\
384 ((NONE = OPTION_MAP f x) = (x = NONE))
385Proof
386 REWRITE_TAC [OPTION_MAP_EQ_NONE] THEN
387 CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [EQ_SYM_EQ])) THEN
388 REWRITE_TAC [OPTION_MAP_EQ_NONE]
389QED
390
391Theorem OPTION_MAP_COMPOSE:
392 OPTION_MAP f (OPTION_MAP g (x:'a option)) = OPTION_MAP (f o g) x
393Proof
394 OPTION_CASES_TAC ``x:'a option`` THEN SRW_TAC [][]
395QED
396
397Theorem OPTION_MAP_CONG[defncong]:
398 !opt1 opt2 f1 f2.
399 (opt1 = opt2) /\ (!x. (opt2 = SOME x) ==> (f1 x = f2 x)) ==>
400 (OPTION_MAP f1 opt1 = OPTION_MAP f2 opt2)
401Proof
402 REPEAT STRIP_TAC THEN ASM_REWRITE_TAC [] THEN
403 Q.SPEC_THEN `opt2` FULL_STRUCT_CASES_TAC option_nchotomy THEN
404 REWRITE_TAC [OPTION_MAP_DEF, SOME_11] THEN
405 FIRST_X_ASSUM MATCH_MP_TAC THEN REWRITE_TAC [SOME_11]
406QED
407
408Theorem IS_SOME_MAP:
409 IS_SOME (OPTION_MAP f x) = IS_SOME (x : 'a option)
410Proof
411 OPTION_CASES_TAC “x:'a option” THEN
412 REWRITE_TAC [IS_SOME_DEF, OPTION_MAP_DEF]
413QED
414
415Theorem OPTION_MAP_id[simp]:
416 OPTION_MAP I (x:'a option) = x /\ OPTION_MAP (\x. x) x = x
417Proof
418 OPTION_CASES_TAC “x:'a option” THEN SRW_TAC[][]
419QED
420
421(* and one about OPTION_JOIN *)
422
423Theorem OPTION_JOIN_EQ_SOME:
424 !(x:'a option option) y. (OPTION_JOIN x = SOME y) = (x = SOME (SOME y))
425Proof
426 GEN_TAC THEN
427 Q.SUBGOAL_THEN `(x = NONE) \/ (?z. x = SOME z)` STRIP_ASSUME_TAC THENL [
428 MATCH_ACCEPT_TAC option_nchotomy,
429 ALL_TAC,
430 ALL_TAC
431 ] THEN ASM_REWRITE_TAC option_rws THEN
432 OPTION_CASES_TAC “z:'a option” THEN
433 ASM_REWRITE_TAC option_rws
434QED
435
436(* and some about OPTION_MAP2 *)
437
438Theorem OPTION_MAP2_SOME[simp]:
439 (OPTION_MAP2 f (o1:'a option) (o2:'b option) = SOME v) <=>
440 (?x1 x2. (o1 = SOME x1) /\ (o2 = SOME x2) /\ (v = f x1 x2))
441Proof
442 OPTION_CASES_TAC “o1:'a option” THEN
443 OPTION_CASES_TAC “o2:'b option” THEN
444 SRW_TAC [][EQ_IMP_THM]
445QED
446
447Theorem OPTION_MAP2_NONE[simp]:
448 OPTION_MAP2 f (o1:'a option) (o2:'b option) = NONE <=> o1 = NONE \/ o2 = NONE
449Proof
450 OPTION_CASES_TAC “o1:'a option” THEN
451 OPTION_CASES_TAC “o2:'b option” THEN
452 SRW_TAC [][]
453QED
454
455Theorem OPTION_MAP2_cong[defncong]:
456 !x1 x2 y1 y2 f1 f2.
457 (x1 = x2) /\ (y1 = y2) /\
458 (!x y. (x2 = SOME x) /\ (y2 = SOME y) ==> (f1 x y = f2 x y)) ==>
459 (OPTION_MAP2 f1 x1 y1 = OPTION_MAP2 f2 x2 y2)
460Proof
461 SRW_TAC [][] THEN
462 Q.SPEC_THEN `x1` FULL_STRUCT_CASES_TAC option_nchotomy THEN
463 Q.ISPEC_THEN `y1` FULL_STRUCT_CASES_TAC option_nchotomy THEN
464 SRW_TAC [][]
465QED
466
467Theorem OPTION_MAP_CASE:
468 OPTION_MAP f (x:'a option) = option_CASE x NONE (SOME o f)
469Proof
470 OPTION_CASES_TAC “x:'a option” THEN
471 REWRITE_TAC [combinTheory.o_THM, option_CLAUSES]
472QED
473
474(* similarly have
475``OPTION_JOIN f = option_CASE x NONE I`` ;
476``OPTION_BIND x f = option_CASE x NONE f`` ;
477*)
478
479(* ----------------------------------------------------------------------
480 The Option Monad
481
482 A monad with a zero (NONE)
483
484 * OPTION_BIND - monadic bind operation for options
485 nice syntax is
486 do
487 v <- opn1;
488 opn2
489 od
490 where opn2 may refer to v
491 * OPTION_IGNORE_BIND - bind that ignores the passed parameter, with
492 nice syntax looking like
493 do
494 opn1 ;
495 opn2
496 od
497 * OPTION_GUARD - checks a predicate and either gives a
498 successful unit value, or failure (NONE)
499 nice syntax would be
500 do
501 assert(some condition);
502 ...
503 od
504 * OPTION_CHOICE - tries one operation, and if it fails, tries
505 the second. Nice syntax would be opn1 ++ opn2
506
507 ---------------------------------------------------------------------- *)
508
509val OPTION_BIND_def = new_recursive_definition
510 {name="OPTION_BIND_def",
511 rec_axiom=option_Axiom,
512 def = “(OPTION_BIND NONE f = NONE) /\ (OPTION_BIND (SOME x) f = f x)”}
513val _= export_rewrites ["OPTION_BIND_def"]
514val _ = computeLib.add_persistent_funs ["OPTION_BIND_def"];
515
516Theorem OPTION_BIND_cong[defncong]:
517 !o1 o2 f1 f2.
518 (o1:'a option = o2) /\ (!x. (o2 = SOME x) ==> (f1 x = f2 x)) ==>
519 (OPTION_BIND o1 f1 = OPTION_BIND o2 f2)
520Proof simpLib.SIMP_TAC (srw_ss()) [FORALL_OPTION]
521QED
522
523Theorem OPTION_BIND_EQUALS_OPTION[simp]:
524 (OPTION_BIND (p:'a option) f = NONE <=>
525 p = NONE \/ ?x. p = SOME x /\ f x = NONE) /\
526 (OPTION_BIND p f = SOME y <=> ?x. p = SOME x /\ f x = SOME y)
527Proof OPTION_CASES_TAC ``p:'a option`` THEN SRW_TAC [][]
528QED
529
530Theorem IS_SOME_BIND:
531 IS_SOME (OPTION_BIND x g) ==> IS_SOME (x : 'a option)
532Proof
533 OPTION_CASES_TAC “x:'a option” THEN
534 REWRITE_TAC [IS_SOME_DEF, OPTION_BIND_def]
535QED
536
537Theorem OPTION_BIND_SOME:
538 !opt:'a option. OPTION_BIND opt SOME = opt
539Proof
540 GEN_TAC >> OPTION_CASES_TAC “opt: 'a option” >> REWRITE_TAC[OPTION_BIND_def]
541QED
542
543Theorem OPTION_BIND_eq_case:
544 OPTION_BIND (x: 'a option) f =
545 case x of NONE => NONE | SOME a => f a
546Proof
547 OPTION_CASES_TAC “x:'a option”
548 \\ SRW_TAC[][]
549QED
550
551val OPTION_IGNORE_BIND_def = new_definition(
552 "OPTION_IGNORE_BIND_def",
553 ``OPTION_IGNORE_BIND m1 m2 = OPTION_BIND m1 (K m2)``);
554
555Theorem OPTION_IGNORE_BIND_thm[simp]:
556 (OPTION_IGNORE_BIND NONE m = NONE) /\
557 (OPTION_IGNORE_BIND (SOME v) m = m)
558Proof
559 SRW_TAC[][OPTION_IGNORE_BIND_def]
560QED
561val _ = computeLib.add_persistent_funs ["OPTION_IGNORE_BIND_thm"]
562
563Theorem OPTION_IGNORE_BIND_EQUALS_OPTION[simp]:
564 ((OPTION_IGNORE_BIND (m1:'a option) m2 = NONE) <=>
565 (m1 = NONE) \/ (m2 = NONE)) /\
566 ((OPTION_IGNORE_BIND m1 m2 = SOME y) <=>
567 ?x. (m1 = SOME x) /\ (m2 = SOME y))
568Proof
569 OPTION_CASES_TAC ``m1:'a option`` THEN SRW_TAC [][]
570QED
571
572Theorem OPTION_IGNORE_BIND_cong[defncong]:
573 (o1 = o2: 'a option) /\ (!v. o2 = SOME v ==> p1 = p2:'b option) ==>
574 OPTION_IGNORE_BIND o1 p1 = OPTION_IGNORE_BIND o2 p2
575Proof
576 OPTION_CASES_TAC “o2:'a option” >> rpt strip_tac >>
577 ASM_REWRITE_TAC[OPTION_IGNORE_BIND_thm] >> first_x_assum irule >>
578 irule_at Any EQ_REFL
579QED
580
581val OPTION_GUARD_def = new_recursive_definition {
582 name = "OPTION_GUARD_def",
583 rec_axiom = boolTheory.boolAxiom,
584 def = ``(OPTION_GUARD T = SOME ()) /\
585 (OPTION_GUARD F = NONE)``};
586val _ = export_rewrites ["OPTION_GUARD_def"]
587val _ = computeLib.add_persistent_funs ["OPTION_GUARD_def"]
588(* suggest overloading this to assert when used with other monad syntax. *)
589
590Theorem OPTION_GUARD_COND:
591 OPTION_GUARD b = if b then SOME () else NONE
592Proof
593 ASM_CASES_TAC ``b:bool`` THEN ASM_REWRITE_TAC [OPTION_GUARD_def]
594QED
595
596Theorem OPTION_GUARD_EQ_THM[simp]:
597 ((OPTION_GUARD b = SOME ()) <=> b) /\
598 ((OPTION_GUARD b = NONE) <=> ~b)
599Proof
600 Cases_on `b` THEN SRW_TAC[][]
601QED
602
603val OPTION_CHOICE_def = new_recursive_definition
604 {name = "OPTION_CHOICE_def",
605 rec_axiom = option_Axiom,
606 def = ``(OPTION_CHOICE NONE m2 = m2) /\
607 (OPTION_CHOICE (SOME x) m2 = SOME x)``}
608val _ = export_rewrites ["OPTION_CHOICE_def"]
609val _ = computeLib.add_persistent_funs ["OPTION_CHOICE_def"]
610
611Theorem OPTION_CHOICE_EQ_NONE:
612 (OPTION_CHOICE (m1:'a option) m2 = NONE) <=> (m1 = NONE) /\ (m2 = NONE)
613Proof
614 OPTION_CASES_TAC ``m1:'a option`` THEN SRW_TAC[][]
615QED
616
617Theorem OPTION_CHOICE_NONE[simp]:
618 OPTION_CHOICE (m1:'a option) NONE = m1
619Proof
620 OPTION_CASES_TAC ``m1:'a option`` THEN SRW_TAC[][]
621QED
622
623val OPTION_MCOMP_def = Q.new_definition ("OPTION_MCOMP_def",
624 `OPTION_MCOMP g f m = OPTION_BIND (f m) g`) ;
625
626val o_THM = combinTheory.o_THM ;
627
628(* OPTION_MCOMP is the composition operator in the
629 Kleisli category of the option monad *)
630Theorem OPTION_MCOMP_ASSOC:
631 OPTION_MCOMP f (OPTION_MCOMP g (h : 'a -> 'b option)) =
632 OPTION_MCOMP (OPTION_MCOMP f g) h
633Proof
634 REWRITE_TAC [OPTION_MCOMP_def, FUN_EQ_THM, o_THM]
635 THEN GEN_TAC THEN OPTION_CASES_TAC ``h x : 'b option``
636 THEN REWRITE_TAC [OPTION_BIND_def, o_THM, OPTION_MCOMP_def]
637QED
638
639(* SOME is the UNIT function of the option monad,
640 and the identity arrow in the Kleisli category *)
641Theorem OPTION_MCOMP_ID:
642 (OPTION_MCOMP g SOME = g) /\ (OPTION_MCOMP SOME f = f : 'a -> 'b option)
643Proof
644 REWRITE_TAC [OPTION_MCOMP_def, OPTION_BIND_def, FUN_EQ_THM, o_THM]
645 THEN GEN_TAC THEN OPTION_CASES_TAC ``f x : 'b option``
646 THEN REWRITE_TAC [OPTION_BIND_def]
647QED
648
649
650(* ----------------------------------------------------------------------
651 OPTION_APPLY
652 ---------------------------------------------------------------------- *)
653
654val OPTION_APPLY_def = new_recursive_definition
655 {name = "OPTION_APPLY_def",
656 rec_axiom = option_Axiom,
657 def = ``(OPTION_APPLY NONE x = NONE) /\
658 (OPTION_APPLY (SOME f) x = OPTION_MAP f x)``}
659val _ = export_rewrites ["OPTION_APPLY_def"]
660
661val _ = set_mapped_fixity { fixity = Infixl 500,
662 term_name = "APPLICATIVE_FAPPLY",
663 tok = "<*>" }
664Overload APPLICATIVE_FAPPLY = ``OPTION_APPLY``
665
666(* this could be the definition of OPTION_MAP2/lift2 *)
667Theorem OPTION_APPLY_MAP2:
668 OPTION_MAP f (x:'a option) <*> (y:'b option) = OPTION_MAP2 f x y
669Proof
670 OPTION_CASES_TAC ``x:'a option`` THEN SRW_TAC[][] THEN
671 OPTION_CASES_TAC ``y:'b option`` THEN SRW_TAC[][]
672QED
673
674(* monadic "laws" - first is clause 2 of definition above, so omitted below *)
675Theorem SOME_SOME_APPLY:
676 SOME f <*> SOME x = SOME (f x)
677Proof
678 SRW_TAC[][]
679QED
680
681Theorem SOME_APPLY_PERMUTE:
682 (f:('a -> 'b) option) <*> (SOME x) = SOME (\f. f x) <*> f
683Proof
684 OPTION_CASES_TAC ``f:('a -> 'b) option`` THEN SRW_TAC[][]
685QED
686
687Theorem OPTION_APPLY_o:
688 SOME $o <*> (f:('b->'c)option) <*> (g:('a->'b) option) <*> (x:'a option) =
689 f <*> (g <*> x)
690Proof
691 OPTION_CASES_TAC ``f:('b->'c)option`` THEN SRW_TAC[][] THEN
692 OPTION_CASES_TAC ``g:('a->'b)option`` THEN SRW_TAC[][] THEN
693 OPTION_CASES_TAC ``x:'a option`` THEN SRW_TAC[][]
694QED
695
696
697
698(* ----------------------------------------------------------------------
699 OPTREL - lift a relation on 'a, 'b to 'a option, 'b option
700 ---------------------------------------------------------------------- *)
701
702val OPTREL_def = new_definition("OPTREL_def",
703 ``OPTREL R x y <=>
704 (x = NONE) /\ (y = NONE) \/
705 ?x0 y0. (x = SOME x0) /\ (y = SOME y0) /\ R x0 y0``);
706
707Theorem OPTREL_MONO:
708 (!x:'a y:'b. P x y ==> Q x y) ==> (OPTREL P x y ==> OPTREL Q x y)
709Proof
710 BasicProvers.SRW_TAC [][OPTREL_def] THEN BasicProvers.SRW_TAC [][SOME_11]
711QED
712val _ = IndDefLib.export_mono "OPTREL_MONO"
713
714Theorem OPTREL_refl[simp]:
715 (!x. R x x) ==> !x. OPTREL R x x
716Proof
717STRIP_TAC THEN GEN_TAC
718THEN OPTION_CASES_TAC ``x:'a option``
719THEN ASM_REWRITE_TAC(OPTREL_def::option_rws)
720THEN PROVE_TAC[]
721QED
722
723Theorem OPTREL_eq[simp]:
724 OPTREL (=) = (=)
725Proof
726 REWRITE_TAC[FUN_EQ_THM] >> rpt strip_tac >> Q.RENAME_TAC [‘OPTREL _ x y’] >>
727 MAP_EVERY OPTION_CASES_TAC [“x:'a option”, “y:'a option”] >>
728 simpLib.SIMP_TAC bool_ss (OPTREL_def::option_rws) >> METIS_TAC[]
729QED
730
731Theorem OPTREL_SOME:
732 (!R x y. OPTREL R (SOME x) y <=> ?z. (y = SOME z) /\ R x z) /\
733 (!R x y. OPTREL R x (SOME y) <=> ?z. (x = SOME z) /\ R z y)
734Proof
735 SRW_TAC[][OPTREL_def]
736QED
737
738Theorem OPTREL_NONE[simp]:
739 (OPTREL R NONE y <=> y = NONE) /\
740 (OPTREL R x NONE <=> x = NONE)
741Proof
742 SRW_TAC[][OPTREL_def]
743QED
744
745Theorem OPTREL_O_lemma[local]:
746 !R1 R2 l1 l2.
747 OPTREL (R1 O R2) l1 l2 <=> ?l3. OPTREL R2 l1 l3 /\ OPTREL R1 l3 l2
748Proof
749 SRW_TAC [][OPTREL_def,EQ_IMP_THM,relationTheory.O_DEF,PULL_EXISTS] >>
750 FULL_SIMP_TAC (srw_ss()) [PULL_EXISTS] >> METIS_TAC[]
751QED
752
753Theorem OPTREL_O:
754 !R1 R2. OPTREL (R1 O R2) = OPTREL R1 O OPTREL R2
755Proof
756 SRW_TAC[][FUN_EQ_THM,OPTREL_O_lemma,relationTheory.O_DEF]
757QED
758
759Theorem OPTREL_THM[simp]:
760 (OPTREL R (SOME x) NONE = F) /\
761 (OPTREL R NONE (SOME y) = F) /\
762 (OPTREL R NONE NONE = T) /\
763 (OPTREL R (SOME x) (SOME y) = R x y)
764Proof
765 SRW_TAC[][OPTREL_def]
766QED
767
768Theorem OPTREL_CONG[defncong]:
769 !(opt1:'a option) (opt2:'b option) opt1' opt2' R R'.
770 opt1 = opt1' /\ opt2 = opt2' /\
771 (!x y. opt1' = SOME x /\ opt2' = SOME y ==> R x y = R' x y) ==>
772 (OPTREL R opt1 opt2 <=> OPTREL R' opt1' opt2')
773Proof
774 SRW_TAC[][] >> pop_assum mp_tac >> OPTION_CASES_TAC “opt1 : 'a option” >>
775 OPTION_CASES_TAC “opt2 : 'b option” >> SRW_TAC[][OPTREL_def]
776QED
777
778(* ----------------------------------------------------------------------
779 some (Hilbert choice "lifted" to the option type)
780
781 some P = NONE, when P is everywhere false.
782 otherwise
783 some P = SOME x ensuring P x.
784
785 This constant saves pain when confronted with the possibility of
786 writing
787 if ?x. P x then f (@x. P x) else ...
788
789 Instead one can write
790 case (some x. P x) of SOME x -> f x || NONE -> ...
791 and avoid having to duplicate the P formula.
792 ---------------------------------------------------------------------- *)
793
794val some_def = new_definition(
795 "some_def",
796 ``some P = if ?x. P x then SOME (@x. P x) else NONE``);
797
798Theorem some_intro:
799 (!x. P x ==> Q (SOME x)) /\ ((!x. ~P x) ==> Q NONE) ==> Q (some P)
800Proof
801 SRW_TAC [][some_def] THEN METIS_TAC []
802QED
803
804Theorem some_elim:
805 Q (some P) ==> (?x. P x /\ Q (SOME x)) \/ ((!x. ~P x) /\ Q NONE)
806Proof
807 SRW_TAC [][some_def] THEN METIS_TAC []
808QED
809val _ = set_fixity "some" Binder
810
811Theorem some_F[simp]:
812 (some x. F) = NONE
813Proof
814 DEEP_INTRO_TAC some_intro THEN SRW_TAC [][]
815QED
816
817Theorem some_EQ[simp]:
818 ((some x. x = y) = SOME y) /\ ((some x. y = x) = SOME y)
819Proof
820 CONJ_TAC THEN DEEP_INTRO_TAC some_intro THEN SRW_TAC [][]
821QED
822
823(* |- !M M' v f.
824 M = M' /\ (M' = NONE ==> v = v') /\ (!x. M' = SOME x ==> f x = f' x) ==>
825 option_CASE M v f = option_CASE M' v' f'
826 *)
827Theorem option_case_cong =
828 Prim_rec.case_cong_thm option_nchotomy option_case_def;
829
830(* another similar theorem, moved here from cardinalTheory:
831 |- option_CASE x v f <=> (x = NONE ==> v) /\ !x'. x = SOME x' ==> f x'
832 *)
833Theorem option_imp_elim =
834 TypeBase.case_pred_imp_of “:'a option”
835 |> INST_TYPE [beta |-> bool]
836 |> Q.SPEC ‘I’
837 |> REWRITE_RULE [combinTheory.I_THM]
838
839val OPTION_ALL_def = new_recursive_definition {
840 def = ``(OPTION_ALL P NONE <=> T) /\ (OPTION_ALL P (SOME (x:'a)) <=> P x)``,
841 name = "OPTION_ALL_def[simp,compute]",
842 rec_axiom = option_Axiom };
843
844Theorem OPTION_ALL_MONO:
845 (!x:'a. P x ==> P' x) ==> OPTION_ALL P opt ==> OPTION_ALL P' opt
846Proof
847 Q.SPEC_THEN `opt` STRUCT_CASES_TAC option_nchotomy THEN
848 REWRITE_TAC [OPTION_ALL_def] THEN REPEAT STRIP_TAC THEN RES_TAC
849QED
850val _ = IndDefLib.export_mono "OPTION_ALL_MONO"
851
852Theorem OPTION_ALL_CONG[defncong]:
853 !opt opt' P P'.
854 (opt = opt') /\ (!x. (opt' = SOME x) ==> (P x <=> P' x)) ==>
855 (OPTION_ALL P opt <=> OPTION_ALL P' opt')
856Proof
857 simpLib.SIMP_TAC (srw_ss()) [FORALL_OPTION]
858QED
859
860Theorem option_case_eq:
861 (option_CASE (opt:'a option) nc sc = v) <=>
862 ((opt = NONE) /\ (nc = v) \/ ?x. (opt = SOME x) /\ (sc x = v))
863Proof
864 OPTION_CASES_TAC “opt:'a option” THEN SRW_TAC[][EQ_SYM_EQ, option_case_def]
865QED
866
867(* OpenTheory fix: hol-set reports the following 1 unsatisfied assumption *)
868Theorem option_case_eq' :
869 (option_CASE (x:'a option) v f = v') <=>
870 ((x = NONE) /\ (v = v') \/ ?a. (x = SOME a) /\ (f a = v'))
871Proof
872 REWRITE_TAC [option_case_eq]
873QED
874
875val S = PP.add_string and NL = PP.NL and B = PP.block PP.CONSISTENT 0
876
877Theorem option_Induct =
878 ONCE_REWRITE_RULE [boolTheory.CONJ_SYM] option_induction;
879Theorem option_CASES =
880 ONCE_REWRITE_RULE [boolTheory.DISJ_SYM] option_nchotomy;
881
882val _ = TypeBase.general_update “:'a option” (
883 TypeBasePure.put_recognizers [IS_NONE_DEF, IS_SOME_DEF] o
884 TypeBasePure.put_lift (
885 mk_var("optionSyntax.lift_option",
886 “:'type -> ('a -> 'term) -> 'a option -> 'term”)
887 ) o
888 TypeBasePure.put_destructors [THE_DEF]
889 )
890
891Theorem datatype_option:
892 DATATYPE (option (NONE:'a option) (SOME:'a -> 'a option))
893Proof
894 REWRITE_TAC [DATATYPE_TAG_THM]
895QED