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