1structure NDDB :> NDDB = 2struct 3 4open NDSupportTheory 5 6val C_DEF = combinTheory.C_DEF; 7val o_DEF = combinTheory.o_DEF; 8 9val one_ty = oneSyntax.one_ty; 10 11val J_tm = Term`J`; 12val KT_tm = Term`KT`; 13 14val RW_HELP_TAC = CONV_TAC (REWR_CONV FUN_EQ_THM) THEN Cases; 15 16val DEEP_SYM = GEN_ALL o SYM o SPEC_ALL; 17 18(* rich types storage *) 19 20type rich_type = { 21 inj_pair: Thm.thm, 22 ret_map : Thm.thm, 23 (* ALL *) 24 all_tm : Term.term, 25 all_thm : Thm.thm, 26 all_map : Thm.thm, 27 all_T : Thm.thm, 28 all_mono : Thm.thm 29}; 30 31(* empty types store *) 32val types = ref ([]:string list, []:rich_type list); 33 34local 35 fun insert (a:string) (b:rich_type) ([], []) = ([a], [b]) 36 | insert a b (x::xs, y::ys) = if a = x 37 then (x::xs, b::ys) 38 else ( 39 let val (X, Y) = insert a b (xs, ys) 40 in (x::X, y::Y) end) 41in 42 fun register_type(a, b) = K () (types := insert a b (!types)) 43end; 44 45 46(* *val fun_positivity_map = ``[F; T]``;*) 47 48(* map definitions *) 49val map_defs = [ 50 fun_map_def, 51 sum_map_def, 52 prod_map_def, 53 list_map_def, 54 option_map_def 55]; 56 57(* retrieve definitions *) 58 59(* ``combin$C (((combin$C $o) combin$C) o ($o o OPTION_BIND))`` *) 60 61val retrieve_defs = [ 62 fun_retrieve_def, 63 sum_retrieve_def, 64 prod_retrieve_def, 65 list_retrieve_def, 66 option_retrieve_def 67]; 68 69 70(************************ ALL definitions ************************) 71 72(*****************************************************************) 73 74val sum_prod_duality = prove(``!f1 f2. 75 (prod_retrieve f1 f2) = 76 (combin$C (sum_retrieve (combin$C f1) (combin$C f2)))``, 77 simp[C_DEF] 78>> REPEAT GEN_TAC 79>> REPEAT RW_HELP_TAC 80>> BETA_TAC 81>> simp[sum_retrieve_def, prod_retrieve_def] 82); 83 84(*-- injective pairs --*) 85 86val inj_pair_tm = prim_mk_const {Name="inj_pair", Thy="NDSupport"}; 87 88val inj_pair_id = prove(``!f. inj_pair I f``, 89 simp[inj_pair_def, combinTheory.I_DEF]); 90 91val inj_pair_some = prove(``!g. inj_pair g (\x (y:one).SOME x)``, 92 simp[inj_pair_def, ABS_SIMP]); 93 94val _ = prove(``!g. INJ g = inj_pair g J``, 95 simp[inj_pair_def, INJ_def, J_def]); 96 97 98(*(********** CLOSED UNDER INJECTIONS ******) 99val inj_pair_closed = prove(``!f g h. 100 INJ h ==> (inj_pair f g) ==> (inj_pair (f o h) (g o h))``, 101 simp[inj_pair_def, INJ_def, o_DEF] 102); 103val retrieve_map_closed = prove(`` 104(((g o (h:'b->'a)) o (f o (h:'d->'a)) = ((($o g):('b->'a)->'b->'c->'e) f) o (h:'d->'a))) `` 105``(g o h) o (f o h) = (g o f) o h`` 106simp[o_DEF, inj_pair_def] 107 108 109prove(``!f1 g1 f2 g2. 110 ((sum_retrieve g1 g2)o h) o ((sum_map f1 f2)o h) = 111 ((sum_retrieve (g1 o f1) (g2 o f2)) o h)`` 112 113Cases_on`h (INL x')` 114Cases_on`h (INL (f1 x))` 115*) 116 117(*************************** SUM TYPE ****************************) 118 119val sum_inj_pair_thm = prove(``!f1 g1 f2 g2. 120 (inj_pair f1 g1) ==> 121 (inj_pair f2 g2) ==> 122 (inj_pair (sum_map f1 f2) (sum_retrieve g1 g2))``, 123 REPEAT GEN_TAC 124>> simp[inj_pair_def] >> REPEAT DISCH_TAC >> Cases 125>> simp[pairTheory.FORALL_PROD] >> simp[sum_retrieve_def] 126>> Cases 127>> simp[sum_retrieve_def, sum_map_def, sumTheory.SUM_MAP_def] 128); 129 130val sum_retrieve_map_thm = prove(``!f1 g1 f2 g2. 131 (sum_retrieve g1 g2) o (sum_map f1 f2) = 132 (sum_retrieve (g1 o f1) (g2 o f2)) 133``, REPEAT GEN_TAC >> simp[o_DEF] 134>> RW_HELP_TAC 135>> BETA_TAC >> simp[sum_map_def] 136>> RW_HELP_TAC 137>> simp[sum_retrieve_def]); 138 139val sum_fancy_all_thm = prove(``!P Q z. sum_all P Q z = 140 (!b. sum_retrieve (\x u. SOME (P x)) (\y u. SOME (Q y)) z b <> SOME F)``, 141 GEN_TAC >> GEN_TAC >> Cases 142>> simp[pairTheory.FORALL_PROD] 143>> simp[sum_retrieve_def, sum_all_def] 144); 145 146val sum_all_map_thm = prove(``!P1 P2 f1 f2. 147 (sum_all P1 P2) o (sum_map f1 f2) = sum_all (P1 o f1) (P2 o f2) 148``, REPEAT GEN_TAC >> simp[o_DEF] 149>> RW_HELP_TAC 150>> BETA_TAC >> simp[sum_map_def] 151>> simp[sum_all_def] 152); 153 154val sum_all_T_thm = prove(``sum_all KT KT = KT``, 155 RW_HELP_TAC >> simp[sum_all_def, KT_def] 156); 157 158val sum_all_mono_thm = prove(``!P Q P' Q'. 159 (P SUBSET P') /\ (Q SUBSET Q') ==> (sum_all P Q) SUBSET (sum_all P' Q') 160``, simp[pred_setTheory.SUBSET_DEF, boolTheory.IN_DEF] 161>> REPEAT GEN_TAC >> REPEAT DISCH_TAC 162>> Cases >> simp[sum_all_def] 163); 164 165val _ = register_type("sum", { 166 inj_pair = sum_inj_pair_thm, 167 ret_map = sum_retrieve_map_thm, 168 all_tm = ``sum_all``, 169 all_thm = sum_all_def, 170 all_map = sum_all_map_thm, 171 all_T = sum_all_T_thm, 172 all_mono = sum_all_mono_thm 173}); 174 175 176(*************************** PROD TYPE ***************************) 177 178val prod_inj_pair_thm = prove(``!f1 g1 f2 g2. 179 (inj_pair f1 g1) ==> 180 (inj_pair f2 g2) ==> 181 (inj_pair (f1 ## f2) (prod_retrieve g1 g2))``, 182 REPEAT GEN_TAC 183>> simp[inj_pair_def] >> REPEAT DISCH_TAC 184>> Cases >> Cases >> DISCH_TAC >> fs[] 185>> first_assum(fn th => (Q.GENL [`z'`] 186 (Q.SPEC `INL z'` th)) |> BETA_RULE |> ASSUME_TAC) 187>> first_x_assum(fn th => (Q.GENL [`z''`] 188 (Q.SPEC `INR z''` th)) |> BETA_RULE |> ASSUME_TAC) 189>> fs[prod_retrieve_def, prod_map_def, pairTheory.PAIR_MAP] 190); 191 192val prod_retrieve_map_thm = prove(``!f1 g1 f2 g2. 193 (prod_retrieve g1 g2) o (f1 ## f2) = 194 (prod_retrieve (g1 o f1) (g2 o f2)) 195``, REPEAT GEN_TAC >> simp[o_DEF] 196>> RW_HELP_TAC >> BETA_TAC 197>> RW_HELP_TAC >> simp[prod_retrieve_def] 198); 199 200(*val prod_fancy_all_thm = prove(``!P Q z. prod_all P Q z = 201 (!b. prod_retrieve (\x u. SOME (P x)) (\y u. SOME (Q y)) z b <> SOME F)``, 202 GEN_TAC >> GEN_TAC >> Cases 203>> simp[sumTheory.FORALL_SUM] 204>> simp[prod_retrieve_def, prod_all_def] 205);*) 206 207 208val prod_all_map_thm = prove(``!P1 P2 f1 f2. 209 (prod_all P1 P2) o (prod_map f1 f2) = prod_all (P1 o f1) (P2 o f2) 210``, REPEAT GEN_TAC >> simp[o_DEF] 211>> RW_HELP_TAC 212>> BETA_TAC >> simp[prod_map_def, prod_all_def] 213); 214 215val prod_all_T_thm = prove(``prod_all KT KT = KT``, 216 RW_HELP_TAC >> simp[prod_all_def, KT_def] 217); 218 219val prod_all_mono_thm = prove(``!P Q P' Q'. 220 (P SUBSET P') /\ (Q SUBSET Q') ==> (prod_all P Q) SUBSET (prod_all P' Q') 221``, simp[pred_setTheory.SUBSET_DEF, boolTheory.IN_DEF] 222>> REPEAT GEN_TAC >> REPEAT DISCH_TAC 223>> Cases >> simp[prod_all_def] 224); 225 226 227val _ = register_type("prod", { 228 inj_pair = prod_inj_pair_thm, 229 ret_map = prod_retrieve_map_thm, 230 all_thm = prod_all_def, 231 all_tm = ``prod_all``, 232 all_map = prod_all_map_thm, 233 all_T = prod_all_T_thm, 234 all_mono = prod_all_mono_thm 235}); 236 237 238(*************************** LIST TYPE ***************************) 239 240val _ = register_type("list", { 241 inj_pair = TRUTH, 242 ret_map = TRUTH, 243 all_thm = listTheory.EVERY_DEF, 244 all_tm = ``list_all``, 245 all_map = TRUTH, all_T = TRUTH, all_mono = TRUTH 246}); 247 248(* 249val list_inj_pair_thm = prove(``!f g. 250 (inj_pair f g) ==> 251 (inj_pair (MAP f) (list_retrieve g))``, 252 REPEAT GEN_TAC 253>> simp[inj_pair_def] >> REPEAT DISCH_TAC 254 255>> Induct >> Induct_on`y` 256>> simp[listTheory.MAP] 257>> REPEAT GEN_TAC >> DISCH_TAC >> fs[] 258 259first_x_assum(fn th => (Q.SPEC `(SUC n, c)` th) |> BETA_RULE |> ASSUME_TAC) 260 261fs[list_retrieve_def] 262 263first_x_assum(fn th => (Q.SPEC `x` th) |> BETA_RULE |> ASSUME_TAC) 264 265 266>> DISCH_TAC >> fs[] 267>> first_x_assum(fn th => (Q.GENL [`c`, `n`] 268 (Q.SPEC `(n, c)` th)) |> BETA_RULE |> ASSUME_TAC) 269 270>> first_assum(fn th => ((Q.SPEC `0` th)) |> BETA_RULE |> ASSUME_TAC) 271>> 272>> first_x_assum(fn th => ((Q.SPEC `SUC n` th)) |> BETA_RULE |> ASSUME_TAC) 273 274>> fs[prod_retrieve_def, prod_map_def, pairTheory.PAIR_MAP] 275); 276 277val prod_retrieve_map_thm = prove(``!f1 g1 f2 g2. 278 (prod_retrieve g1 g2) o (f1 ## f2) = 279 (prod_retrieve (g1 o f1) (g2 o f2)) 280``, REPEAT GEN_TAC >> simp[o_DEF] 281>> RW_HELP_TAC >> BETA_TAC 282>> RW_HELP_TAC >> simp[prod_retrieve_def] 283); 284 285register_type("prod", { 286 inj_pair = pair_inj_pair_thm, 287 ret_map = prod_retrieve_map_thm, 288 map_map = TRUTH 289}); 290 291 292 293*)(* 294val list_inj_pair = prove( 295``(inj_pair f g) ==> (inj_pair (list_retrieve f) (list_map g))``, 296 297 simp[inj_pair_def, list_map_def, listTheory.MAP] >> DISCH_TAC >> Induct >> Induct >> simp[] >> Induct_on`y` >> simp[] 298 299simp[pairTheory.FORALL_PROD, list_retrieve_def] 300>> REPEAT DISCH_TAC 301*) 302 303(* 304val tm = ``(\pi. list_CASE pi (g x) (f x)) = (\pi. list_CASE pi (g y) (f y))``; 305val ass = ASSUME tm 306val th1 = AP_THM ass ``[]:'a list`` 307val th2 = BETA_RULE th1 308val one = PURE_ASM_REWRITE_RULE [listTheory.list_case_def] th2 309val th3 = BETA_RULE (Q.AP_THM ass `z::t`) 310val th4 = PURE_ASM_REWRITE_RULE [listTheory.list_case_def] th3 311val th5 = EXT (Q.GEN `t` th4) 312val two = Q.GEN `z` th5 313val th6 = CONJ two one 314 315 316Q.GENL [`y`, `x`] th6 317 318``(inj_pair f g) ==> (INJ (\t pi. list_CASE pi (g t) (f t)) (\_.T) (\_.T))`` 319 320simp[inj_pair_def, pred_setTheory.INJ_DEF] >> DISCH_TAC >> REPEAT GEN_TAC 321 322*) 323 324(*%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%*) 325 326(* constant functions 327val retrieve_k = 328 mk_abs (mk_var("x", alpha), 329 mk_abs (mk_var("y", one_ty), 330 mk_arb(gamma))); 331val map_k = I_tm;*) 332 333val some_inj_thm = prove( 334``inj_pair (\x. ()) (\x (u:one). SOME x)``, simp[inj_pair_def]); 335 336val k_inj_thm = prove( 337``inj_pair I J``, simp[inj_pair_def, J_def]); 338val k_map_map_thm = prove( 339``I o I = I``, simp[o_DEF]); 340val k_ret_map_thm = prove( 341``J o I = J``, simp[o_DEF, J_def]); 342 343val k_all_rule = prove(``KT ARB = T``, simp[KT_def]); 344 345val constantly_rich = { 346 inj_pair = k_inj_thm, 347 ret_map = k_ret_map_thm, 348 all_tm = KT_tm, 349 all_thm = prove(``!x. KT x = T``,simp[KT_def]), 350 all_map = TRUTH, 351 all_T = REFL KT_tm, 352 all_mono= SPEC KT_tm pred_setTheory.SUBSET_REFL 353} : rich_type; 354 355 356(* support for option type *) 357 358val option_inj_pair_thm = prove( 359``!f g. (inj_pair f g) ==> 360 (inj_pair (option_map f) (option_retrieve g))``, 361 REPEAT GEN_TAC 362>> simp[inj_pair_def] >> DISCH_TAC 363>> Induct >> Induct_on`y` 364>> simp[option_retrieve_def, 365 option_map_def, optionTheory.OPTION_MAP_DEF] 366); 367 368val option_map_map_thm = prove(``!f1 f2. 369 (option_map f1) o (option_map f2) = (option_map (f1 o f2)) 370``, REPEAT GEN_TAC >> simp[o_DEF] 371>> CONV_TAC (REWR_CONV FUN_EQ_THM) >> Induct 372>> simp[option_map_def, optionTheory.OPTION_MAP_DEF]); 373 374val option_retrieve_map_thm = prove(``!f g. 375 (option_retrieve g) o (option_map f) = (option_retrieve (g o f)) 376``, REPEAT GEN_TAC >> simp[o_DEF] 377>> CONV_TAC (REWR_CONV FUN_EQ_THM) >> Induct 378>> (TRY GEN_TAC) >> BETA_TAC 379>> CONV_TAC (REWR_CONV FUN_EQ_THM) >> GEN_TAC 380>> simp[option_map_def, 381 optionTheory.OPTION_MAP_DEF, option_retrieve_def]); 382 383(*val option_map_1 = prove(``option_map I = I``, 384 RW_HELP_TAC THEN simp[option_map_def, sumTheory.SUM_MAP_def] 385); 386 387val option_retrieve_1 = prove(``option_retrieve J = J``, 388REPEAT RW_HELP_TAC THEN simp[J_def] 389>> CONV_TAC (REWR_CONV FUN_EQ_THM) 390>> simp[option_retrieve_def, J_def] 391); 392*) 393 394 395val option_all_map_thm = prove(``!P f. 396 (option_all P) o (option_map f) = option_all (P o f) 397``, REPEAT GEN_TAC >> simp[o_DEF] 398>> RW_HELP_TAC 399>> BETA_TAC >> simp[option_map_def, option_all_def] 400); 401 402val option_all_T_thm = prove(``option_all KT = KT``, 403 RW_HELP_TAC >> simp[option_all_def, KT_def] 404); 405 406val option_all_mono_thm = prove(``!P P'. 407 (P SUBSET P') ==> (option_all P) SUBSET (option_all P') 408``, simp[pred_setTheory.SUBSET_DEF, boolTheory.IN_DEF] 409>> REPEAT GEN_TAC >> REPEAT DISCH_TAC 410>> Cases >> simp[option_all_def] 411); 412 413 414val _ = register_type("option", { 415 inj_pair = option_inj_pair_thm, 416 ret_map = option_retrieve_map_thm, 417 all_tm = ``option_all``, 418 all_thm = option_all_def, 419 all_map = option_all_map_thm, 420 all_T = option_all_T_thm, 421 all_mono = option_all_mono_thm 422}); 423 424(* test: all *) 425val _ = prove(``let sum_all2 = 426(\P Q x. !p. (option_CASE (sum_retrieve (\x1 _. SOME (P x1)) (\x2 _. SOME (Q x2)) x p) T I)) in ( 427 (sum_all2 P Q (INL x') = P x') 428 /\ (sum_all2 P Q (INR y') = Q y') 429)``, simp[] >> CONJ_TAC 430>> simp[pairTheory.FORALL_PROD] 431>> simp[optionTheory.option_case_def, sum_retrieve_def]); 432 433 434 435(**********************************) 436 437(* Constructor *) 438 439val inj_constr_thm = prove( 440``!f g. (inj_pair f g) ==> (INJ (\t pi. case pi of 441 [] => (f t, 0) 442 | p::ps => (case (g t p) of 443 NONE => (ARB, 0) 444 | SOME c => (case c ps of (r, n) => (r, SUC n) 445)))) 446``, REPEAT GEN_TAC 447>> simp[INJ_def, inj_pair_def, FUN_EQ_THM] 448>> DISCH_TAC >> REPEAT GEN_TAC >> DISCH_TAC 449>> first_assum (ASSUME_TAC o BETA_RULE o (Q.SPEC `[]`)) 450>> first_x_assum(fn th => (Q.GENL [`xs`,`x`] 451 (Q.SPEC `x::xs` th)) |> BETA_RULE |> ASSUME_TAC) 452>> Cases_on `g t = g t'` >> fs[] 453>> first_assum (ASSUME_TAC o (MATCH_MP (CONV_RULE 454 CONTRAPOS_CONV (Q.SPECL [`g t`, `g t'`] EQ_EXT)))) 455>> fs[] >> first_x_assum (ASSUME_TAC o (Q.SPEC `x`)) 456>> Cases_on `g t x` >> Cases_on `g t' x` 457>> fs[optionTheory.option_case_def, pairTheory.pair_CASE_def] 458>> first_x_assum (ASSUME_TAC 459 o (Q.GEN `xs` ) 460 o (PURE_REWRITE_RULE 461 [DEEP_SYM pairTheory.PAIR_FST_SND_EQ]) 462 o (Q.SPEC `xs`)) 463>> first_x_assum (mp_tac o EXT) >> simp[] 464); 465 466 467(*val inj_constr_thm = prove( 468``!f g. (inj_pair f g) ==> 469 (INJ (\t pi. list_CASE pi (f t) (g t))) 470``, REPEAT GEN_TAC 471>> simp[INJ_def, inj_pair_def, FUN_EQ_THM] 472>> DISCH_TAC >> REPEAT GEN_TAC >> DISCH_TAC 473>> first_assum (ASSUME_TAC o BETA_RULE o (Q.SPEC `[]`)) 474>> first_x_assum(fn th => (Q.GENL [`xs`,`x`] 475 (Q.SPEC `x::xs` th)) |> BETA_RULE |> ASSUME_TAC) 476>> Cases_on `g t = g t'` >> fs[] 477);*) 478 479end; 480