1(* ------------------------------------------------------------------------- *) 2(* Applying Monoid Theory: Monoid Instances *) 3(* ------------------------------------------------------------------------- *) 4 5(* 6 7Monoid Instances 8=============== 9The important ones: 10 11 Zn -- Addition Modulo n, n > 0. 12Z*n -- Multiplication Modulo n, n > 1. 13 14*) 15 16(*===========================================================================*) 17 18(* add all dependent libraries for script *) 19open HolKernel boolLib bossLib Parse; 20 21(* declare new theory at start *) 22val _ = new_theory "monoidInstances"; 23 24(* ------------------------------------------------------------------------- *) 25 26 27 28(* val _ = load "jcLib"; *) 29open jcLib; 30 31(* Get dependent theories local *) 32(* val _ = load "monoidMapTheory"; *) 33open monoidTheory; 34open monoidMapTheory; (* for MonoidHomo and MonoidIso *) 35 36(* Get dependent theories in lib *) 37(* (* val _ = load "helperNumTheory"; -- in monoidTheory *) *) 38(* (* val _ = load "helperSetTheory"; -- in monoidTheory *) *) 39open helperNumTheory helperSetTheory helperFunctionTheory; 40 41(* open dependent theories *) 42(* (* val _ = load "dividesTheory"; -- in helperTheory *) *) 43(* (* val _ = load "gcdTheory"; -- in helperTheory *) *) 44open pred_setTheory arithmeticTheory dividesTheory gcdTheory; 45open listTheory; (* for list concatenation example *) 46 47(* val _ = load "logPowerTheory"; *) 48open logrootTheory logPowerTheory; (* for LOG_EXACT_EXP *) 49 50 51(* ------------------------------------------------------------------------- *) 52(* Monoid Instances Documentation *) 53(* ------------------------------------------------------------------------- *) 54(* Monoid Data type: 55 The generic symbol for monoid data is g. 56 g.carrier = Carrier set of monoid 57 g.op = Binary operation of monoid 58 g.id = Identity element of monoid 59*) 60(* Definitions and Theorems (# are exported, ! in computeLib): 61 62 The trivial monoid: 63 trivial_monoid_def |- !e. trivial_monoid e = <|carrier := {e}; id := e; op := (\x y. e)|> 64 trivial_monoid |- !e. FiniteAbelianMonoid (trivial_monoid e) 65 66 The monoid of addition modulo n: 67 plus_mod_def |- !n. plus_mod n = 68 <|carrier := count n; 69 id := 0; 70 op := (\i j. (i + j) MOD n)|> 71 plus_mod_property |- !n. ((plus_mod n).carrier = count n) /\ 72 ((plus_mod n).op = (\i j. (i + j) MOD n)) /\ 73 ((plus_mod n).id = 0) /\ 74 (!x. x IN (plus_mod n).carrier ==> x < n) /\ 75 FINITE (plus_mod n).carrier /\ 76 (CARD (plus_mod n).carrier = n) 77 plus_mod_exp |- !n. 0 < n ==> !x k. (plus_mod n).exp x k = (k * x) MOD n 78 plus_mod_monoid |- !n. 0 < n ==> Monoid (plus_mod n) 79 plus_mod_abelian_monoid |- !n. 0 < n ==> AbelianMonoid (plus_mod n) 80 plus_mod_finite |- !n. FINITE (plus_mod n).carrier 81 plus_mod_finite_monoid |- !n. 0 < n ==> FiniteMonoid (plus_mod n) 82 plus_mod_finite_abelian_monoid |- !n. 0 < n ==> FiniteAbelianMonoid (plus_mod n) 83 84 The monoid of multiplication modulo n: 85 times_mod_def |- !n. times_mod n = 86 <|carrier := count n; 87 id := if n = 1 then 0 else 1; 88 op := (\i j. (i * j) MOD n)|> 89! times_mod_eval |- !n. ((times_mod n).carrier = count n) /\ 90 (!x y. (times_mod n).op x y = (x * y) MOD n) /\ 91 ((times_mod n).id = if n = 1 then 0 else 1) 92 times_mod_property |- !n. ((times_mod n).carrier = count n) /\ 93 ((times_mod n).op = (\i j. (i * j) MOD n)) /\ 94 ((times_mod n).id = if n = 1 then 0 else 1) /\ 95 (!x. x IN (times_mod n).carrier ==> x < n) /\ 96 FINITE (times_mod n).carrier /\ 97 (CARD (times_mod n).carrier = n) 98 times_mod_exp |- !n. 0 < n ==> !x k. (times_mod n).exp x k = (x MOD n) ** k MOD n 99 times_mod_monoid |- !n. 0 < n ==> Monoid (times_mod n) 100 times_mod_abelian_monoid |- !n. 0 < n ==> AbelianMonoid (times_mod n) 101 times_mod_finite |- !n. FINITE (times_mod n).carrier 102 times_mod_finite_monoid |- !n. 0 < n ==> FiniteMonoid (times_mod n) 103 times_mod_finite_abelian_monoid |- !n. 0 < n ==> FiniteAbelianMonoid (times_mod n) 104 105 The Monoid of List concatenation: 106 lists_def |- lists = <|carrier := univ(:'a list); id := []; op := $++ |> 107 lists_monoid |- Monoid lists 108 109 The Monoids from Set: 110 set_inter_def |- set_inter = <|carrier := univ(:'a -> bool); id := univ(:'a); op := $INTER|> 111 set_inter_monoid |- Monoid set_inter 112 set_inter_abelian_monoid |- AbelianMonoid set_inter 113 set_union_def |- set_union = <|carrier := univ(:'a -> bool); id := {}; op := $UNION|> 114 set_union_monoid |- Monoid set_union 115 set_union_abelian_monoid |- AbelianMonoid set_union 116 117 Addition of numbers form a Monoid: 118 addition_monoid_def |- addition_monoid = <|carrier := univ(:num); op := $+; id := 0|> 119 addition_monoid_property |- (addition_monoid.carrier = univ(:num)) /\ 120 (addition_monoid.op = $+) /\ (addition_monoid.id = 0) 121 addition_monoid_abelian_monoid |- AbelianMonoid addition_monoid 122 addition_monoid_monoid |- Monoid addition_monoid 123 124 Multiplication of numbers form a Monoid: 125 multiplication_monoid_def |- multiplication_monoid = <|carrier := univ(:num); op := $*; id := 1|> 126 multiplication_monoid_property |- (multiplication_monoid.carrier = univ(:num)) /\ 127 (multiplication_monoid.op = $* ) /\ (multiplication_monoid.id = 1) 128 multiplication_monoid_abelian_monoid |- AbelianMonoid multiplication_monoid 129 multiplication_monoid_monoid |- Monoid multiplication_monoid 130 131 Powers of a fixed base form a Monoid: 132 power_monoid_def |- !b. power_monoid b = 133 <|carrier := {b ** j | j IN univ(:num)}; op := $*; id := 1|> 134 power_monoid_property |- !b. ((power_monoid b).carrier = {b ** j | j IN univ(:num)}) /\ 135 ((power_monoid b).op = $* ) /\ ((power_monoid b).id = 1) 136 power_monoid_abelian_monoid |- !b. AbelianMonoid (power_monoid b) 137 power_monoid_monoid |- !b. Monoid (power_monoid b) 138 139 Logarithm is an isomorphism: 140 power_to_addition_homo |- !b. 1 < b ==> MonoidHomo (LOG b) (power_monoid b) addition_monoid 141 power_to_addition_iso |- !b. 1 < b ==> MonoidIso (LOG b) (power_monoid b) addition_monoid 142 143 144*) 145(* ------------------------------------------------------------------------- *) 146(* The trivial monoid. *) 147(* ------------------------------------------------------------------------- *) 148 149(* The trivial monoid: {#e} *) 150val trivial_monoid_def = Define` 151 trivial_monoid e :'a monoid = 152 <| carrier := {e}; 153 id := e; 154 op := (\x y. e) 155 |> 156`; 157 158(* 159- type_of ``trivial_monoid e``; 160> val it = ``:'a monoid`` : hol_type 161> EVAL ``(trivial_monoid T).id``; 162val it = |- (trivial_monoid T).id <=> T: thm 163> EVAL ``(trivial_monoid 8).id``; 164val it = |- (trivial_monoid 8).id = 8: thm 165*) 166 167(* Theorem: {e} is indeed a monoid *) 168(* Proof: check by definition. *) 169val trivial_monoid = store_thm( 170 "trivial_monoid", 171 ``!e. FiniteAbelianMonoid (trivial_monoid e)``, 172 rw_tac std_ss[FiniteAbelianMonoid_def, AbelianMonoid_def, Monoid_def, trivial_monoid_def, IN_SING, FINITE_SING]); 173 174(* ------------------------------------------------------------------------- *) 175(* The monoid of addition modulo n. *) 176(* ------------------------------------------------------------------------- *) 177 178(* Additive Modulo Monoid *) 179val plus_mod_def = Define` 180 plus_mod n :num monoid = 181 <| carrier := count n; 182 id := 0; 183 op := (\i j. (i + j) MOD n) 184 |> 185`; 186(* This monoid should be upgraded to add_mod, the additive group of ZN ring later. *) 187 188(* 189- type_of ``plus_mod n``; 190> val it = ``:num monoid`` : hol_type 191> EVAL ``(plus_mod 7).op 5 6``; 192val it = |- (plus_mod 7).op 5 6 = 4: thm 193*) 194 195(* Theorem: properties of (plus_mod n) *) 196(* Proof: by plus_mod_def. *) 197val plus_mod_property = store_thm( 198 "plus_mod_property", 199 ``!n. ((plus_mod n).carrier = count n) /\ 200 ((plus_mod n).op = (\i j. (i + j) MOD n)) /\ 201 ((plus_mod n).id = 0) /\ 202 (!x. x IN (plus_mod n).carrier ==> x < n) /\ 203 (FINITE (plus_mod n).carrier) /\ 204 (CARD (plus_mod n).carrier = n)``, 205 rw[plus_mod_def]); 206 207(* Theorem: 0 < n ==> !x k. (plus_mod n).exp x k = (k * x) MOD n *) 208(* Proof: 209 Expanding by definitions, this is to show: 210 FUNPOW (\j. (x + j) MOD n) k 0 = (k * x) MOD n 211 Applyy induction on k. 212 Base case: FUNPOW (\j. (x + j) MOD n) 0 0 = (0 * x) MOD n 213 LHS = FUNPOW (\j. (x + j) MOD n) 0 0 214 = 0 by FUNPOW_0 215 = 0 MOD n by ZERO_MOD, 0 < n 216 = (0 * x) MOD n by MULT 217 = RHS 218 Step case: FUNPOW (\j. (x + j) MOD n) (SUC k) 0 = (SUC k * x) MOD n 219 LHS = FUNPOW (\j. (x + j) MOD n) (SUC k) 0 220 = (x + FUNPOW (\j. (x + j) MOD n) k 0) MOD n by FUNPOW_SUC 221 = (x + (k * x) MOD n) MOD n by induction hypothesis 222 = (x MOD n + (k * x) MOD n) MOD n by MOD_PLUS, MOD_MOD 223 = (x + k * x) MOD n by MOD_PLUS, MOD_MOD 224 = (k * x + x) MOD n by ADD_COMM 225 = ((SUC k) * x) MOD n by MULT 226 = RHS 227*) 228val plus_mod_exp = store_thm( 229 "plus_mod_exp", 230 ``!n. 0 < n ==> !x k. (plus_mod n).exp x k = (k * x) MOD n``, 231 rw_tac std_ss[plus_mod_def, monoid_exp_def] >> 232 Induct_on `k` >- 233 rw[] >> 234 rw_tac std_ss[FUNPOW_SUC] >> 235 metis_tac[MULT, ADD_COMM, MOD_PLUS, MOD_MOD]); 236 237(* Theorem: Additive Modulo n is a monoid. *) 238(* Proof: check group definitions, use MOD_ADD_ASSOC. 239*) 240val plus_mod_monoid = store_thm( 241 "plus_mod_monoid", 242 ``!n. 0 < n ==> Monoid (plus_mod n)``, 243 rw_tac std_ss[plus_mod_def, Monoid_def, count_def, GSPECIFICATION, MOD_ADD_ASSOC]); 244 245(* Theorem: Additive Modulo n is an Abelian monoid. *) 246(* Proof: by plus_mod_monoid and ADD_COMM. *) 247val plus_mod_abelian_monoid = store_thm( 248 "plus_mod_abelian_monoid", 249 ``!n. 0 < n ==> AbelianMonoid (plus_mod n)``, 250 rw[plus_mod_monoid, plus_mod_def, AbelianMonoid_def, ADD_COMM]); 251 252(* Theorem: Additive Modulo n carrier is FINITE. *) 253(* Proof: by FINITE_COUNT. *) 254val plus_mod_finite = store_thm( 255 "plus_mod_finite", 256 ``!n. FINITE (plus_mod n).carrier``, 257 rw[plus_mod_def]); 258 259(* Theorem: Additive Modulo n is a FINITE monoid. *) 260(* Proof: by plus_mod_monoid and plus_mod_finite. *) 261val plus_mod_finite_monoid = store_thm( 262 "plus_mod_finite_monoid", 263 ``!n. 0 < n ==> FiniteMonoid (plus_mod n)``, 264 rw[FiniteMonoid_def, plus_mod_monoid, plus_mod_finite]); 265 266(* Theorem: Additive Modulo n is a FINITE Abelian monoid. *) 267(* Proof: by plus_mod_abelian_monoid and plus_mod_finite. *) 268val plus_mod_finite_abelian_monoid = store_thm( 269 "plus_mod_finite_abelian_monoid", 270 ``!n. 0 < n ==> FiniteAbelianMonoid (plus_mod n)``, 271 rw[FiniteAbelianMonoid_def, plus_mod_abelian_monoid, plus_mod_finite]); 272 273(* ------------------------------------------------------------------------- *) 274(* The monoid of multiplication modulo n. *) 275(* ------------------------------------------------------------------------- *) 276 277(* Multiplicative Modulo Monoid *) 278val times_mod_def = zDefine` 279 times_mod n :num monoid = 280 <| carrier := count n; 281 id := if n = 1 then 0 else 1; 282 op := (\i j. (i * j) MOD n) 283 |> 284`; 285(* This monoid is taken as the multiplicative monoid of ZN ring later. *) 286(* Use of zDefine to avoid incorporating into computeLib, by default. *) 287(* Evaluation is given later in times_mod_eval. *) 288 289(* 290- type_of ``times_mod n``; 291> val it = ``:num monoid`` : hol_type 292> EVAL ``(times_mod 7).op 5 6``; 293val it = |- (times_mod 7).op 5 6 = 2: thm 294*) 295 296(* Theorem: times_mod evaluation. *) 297(* Proof: by times_mod_def. *) 298val times_mod_eval = store_thm( 299 "times_mod_eval[compute]", 300 ``!n. ((times_mod n).carrier = count n) /\ 301 (!x y. (times_mod n).op x y = (x * y) MOD n) /\ 302 ((times_mod n).id = if n = 1 then 0 else 1)``, 303 rw_tac std_ss[times_mod_def]); 304 305(* Theorem: properties of (times_mod n) *) 306(* Proof: by times_mod_def. *) 307val times_mod_property = store_thm( 308 "times_mod_property", 309 ``!n. ((times_mod n).carrier = count n) /\ 310 ((times_mod n).op = (\i j. (i * j) MOD n)) /\ 311 ((times_mod n).id = if n = 1 then 0 else 1) /\ 312 (!x. x IN (times_mod n).carrier ==> x < n) /\ 313 (FINITE (times_mod n).carrier) /\ 314 (CARD (times_mod n).carrier = n)``, 315 rw[times_mod_def]); 316 317(* Theorem: 0 < n ==> !x k. (times_mod n).exp x k = ((x MOD n) ** k) MOD n *) 318(* Proof: 319 Expanding by definitions, this is to show: 320 (1) n = 1 ==> FUNPOW (\j. (x * j) MOD n) k 0 = (x MOD n) ** k MOD n 321 or to show: FUNPOW (\j. 0) k 0 = 0 by MOD_1 322 Note (\j. 0) = K 0 by FUN_EQ_THM 323 and FUNPOW (K 0) k 0 = 0 by FUNPOW_K 324 (2) n <> 1 ==> FUNPOW (\j. (x * j) MOD n) k 1 = (x MOD n) ** k MOD n 325 Note 1 < n by 0 < n /\ n <> 1 326 By induction on k. 327 Base: FUNPOW (\j. (x * j) MOD n) 0 1 = (x MOD n) ** 0 MOD n 328 FUNPOW (\j. (x * j) MOD n) 0 1 329 = 1 by FUNPOW_0 330 = 1 MOD n by ONE_MOD, 1 < n 331 = ((x MOD n) ** 0) MOD n by EXP 332 Step: FUNPOW (\j. (x * j) MOD n) (SUC k) 1 = (x MOD n) ** SUC k MOD n 333 FUNPOW (\j. (x * j) MOD n) (SUC k) 1 334 = (x * FUNPOW (\j. (x * j) MOD n) k 1) MOD n by FUNPOW_SUC 335 = (x * (x MOD n) ** k MOD n) MOD n by induction hypothesis 336 = ((x MOD n) * (x MOD n) ** k MOD n) MOD n by MOD_TIMES2, MOD_MOD, 0 < n 337 = ((x MOD n) * (x MOD n) ** k) MOD n by MOD_TIMES2, MOD_MOD, 0 < n 338 = ((x MOD n) ** SUC k) MOD n by EXP 339*) 340val times_mod_exp = store_thm( 341 "times_mod_exp", 342 ``!n. 0 < n ==> !x k. (times_mod n).exp x k = ((x MOD n) ** k) MOD n``, 343 rw_tac std_ss[times_mod_def, monoid_exp_def] >| [ 344 `(\j. 0) = K 0` by rw[FUN_EQ_THM] >> 345 metis_tac[FUNPOW_K], 346 `1 < n` by decide_tac >> 347 Induct_on `k` >- 348 rw[EXP, ONE_MOD] >> 349 `FUNPOW (\j. (x * j) MOD n) (SUC k) 1 = (x * FUNPOW (\j. (x * j) MOD n) k 1) MOD n` by rw_tac std_ss[FUNPOW_SUC] >> 350 metis_tac[EXP, MOD_TIMES2, MOD_MOD] 351 ]); 352 353(* Theorem: For n > 0, Multiplication Modulo n is a monoid. *) 354(* Proof: check monoid definitions, use MOD_MULT_ASSOC. *) 355val times_mod_monoid = store_thm( 356 "times_mod_monoid", 357 ``!n. 0 < n ==> Monoid (times_mod n)``, 358 rw_tac std_ss[Monoid_def, times_mod_def, count_def, GSPECIFICATION] >| [ 359 decide_tac, 360 rw[MOD_MULT_ASSOC], 361 decide_tac 362 ]); 363 364(* Theorem: For n > 0, Multiplication Modulo n is an Abelian monoid. *) 365(* Proof: by times_mod_monoid and MULT_COMM. *) 366val times_mod_abelian_monoid = store_thm( 367 "times_mod_abelian_monoid", 368 ``!n. 0 < n ==> AbelianMonoid (times_mod n)``, 369 rw[AbelianMonoid_def, times_mod_monoid, times_mod_def, MULT_COMM]); 370 371(* Theorem: Multiplication Modulo n carrier is FINITE. *) 372(* Proof: by FINITE_COUNT. *) 373val times_mod_finite = store_thm( 374 "times_mod_finite", 375 ``!n. FINITE (times_mod n).carrier``, 376 rw[times_mod_def]); 377 378(* Theorem: For n > 0, Multiplication Modulo n is a FINITE monoid. *) 379(* Proof: by times_mod_monoid and times_mod_finite. *) 380val times_mod_finite_monoid = store_thm( 381 "times_mod_finite_monoid", 382 ``!n. 0 < n ==> FiniteMonoid (times_mod n)``, 383 rw[times_mod_monoid, times_mod_finite, FiniteMonoid_def]); 384 385(* Theorem: For n > 0, Multiplication Modulo n is a FINITE Abelian monoid. *) 386(* Proof: by times_mod_abelian_monoid and times_mod_finite. *) 387val times_mod_finite_abelian_monoid = store_thm( 388 "times_mod_finite_abelian_monoid", 389 ``!n. 0 < n ==> FiniteAbelianMonoid (times_mod n)``, 390 rw[times_mod_abelian_monoid, times_mod_finite, FiniteAbelianMonoid_def, AbelianMonoid_def]); 391 392(* 393 394- EVAL ``(plus_mod 5).op 3 4``; 395> val it = |- (plus_mod 5).op 3 4 = 2 : thm 396- EVAL ``(plus_mod 5).id``; 397> val it = |- (plus_mod 5).id = 0 : thm 398- EVAL ``(times_mod 5).op 2 3``; 399> val it = |- (times_mod 5).op 2 3 = 1 : thm 400- EVAL ``(times_mod 5).op 5 3``; 401> val it = |- (times_mod 5).id = 1 : thm 402*) 403 404(* ------------------------------------------------------------------------- *) 405(* The Monoid of List concatenation. *) 406(* ------------------------------------------------------------------------- *) 407 408val lists_def = Define` 409 lists :'a list monoid = 410 <| carrier := UNIV; 411 id := []; 412 op := list$APPEND 413 |> 414`; 415 416(* 417> EVAL ``lists.op [1;2;3] [4;5]``; 418val it = |- lists.op [1; 2; 3] [4; 5] = [1; 2; 3; 4; 5]: thm 419*) 420 421(* Theorem: Lists form a Monoid *) 422(* Proof: check definition. *) 423val lists_monoid = store_thm( 424 "lists_monoid", 425 ``Monoid lists``, 426 rw_tac std_ss[Monoid_def, lists_def, IN_UNIV, GSPECIFICATION, APPEND, APPEND_NIL, APPEND_ASSOC]); 427 428(* after a long while ... 429 430val lists_monoid = store_thm( 431 "lists_monoid", 432 ``Monoid lists``, 433 rw[Monoid_def, lists_def]); 434*) 435 436(* ------------------------------------------------------------------------- *) 437(* The Monoids from Set. *) 438(* ------------------------------------------------------------------------- *) 439 440(* The Monoid of set intersection *) 441val set_inter_def = Define` 442 set_inter = <| carrier := UNIV; 443 id := UNIV; 444 op := (INTER) |> 445`; 446 447(* 448> EVAL ``set_inter.op {1;4;5;6} {5;6;8;9}``; 449val it = |- set_inter.op {1; 4; 5; 6} {5; 6; 8; 9} = {5; 6}: thm 450*) 451 452(* Theorem: set_inter is a Monoid. *) 453(* Proof: check definitions. *) 454val set_inter_monoid = store_thm( 455 "set_inter_monoid", 456 ``Monoid set_inter``, 457 rw[Monoid_def, set_inter_def, INTER_ASSOC]); 458 459val _ = export_rewrites ["set_inter_monoid"]; 460 461(* Theorem: set_inter is an abelian Monoid. *) 462(* Proof: check definitions. *) 463val set_inter_abelian_monoid = store_thm( 464 "set_inter_abelian_monoid", 465 ``AbelianMonoid set_inter``, 466 rw[AbelianMonoid_def, set_inter_def, INTER_COMM]); 467 468val _ = export_rewrites ["set_inter_abelian_monoid"]; 469 470(* The Monoid of set union *) 471val set_union_def = Define` 472 set_union = <| carrier := UNIV; 473 id := EMPTY; 474 op := (UNION) |> 475`; 476 477(* 478> EVAL ``set_union.op {1;4;5;6} {5;6;8;9}``; 479val it = |- set_union.op {1; 4; 5; 6} {5; 6; 8; 9} = {1; 4; 5; 6; 8; 9}: thm 480*) 481 482(* Theorem: set_union is a Monoid. *) 483(* Proof: check definitions. *) 484val set_union_monoid = store_thm( 485 "set_union_monoid", 486 ``Monoid set_union``, 487 rw[Monoid_def, set_union_def, UNION_ASSOC]); 488 489val _ = export_rewrites ["set_union_monoid"]; 490 491(* Theorem: set_union is an abelian Monoid. *) 492(* Proof: check definitions. *) 493val set_union_abelian_monoid = store_thm( 494 "set_union_abelian_monoid", 495 ``AbelianMonoid set_union``, 496 rw[AbelianMonoid_def, set_union_def, UNION_COMM]); 497 498val _ = export_rewrites ["set_union_abelian_monoid"]; 499 500(* ------------------------------------------------------------------------- *) 501(* Addition of numbers form a Monoid *) 502(* ------------------------------------------------------------------------- *) 503 504(* Define the number addition monoid *) 505val addition_monoid_def = Define` 506 addition_monoid = 507 <| carrier := univ(:num); 508 op := $+; 509 id := 0; 510 |> 511`; 512 513(* 514> EVAL ``addition_monoid.op 5 6``; 515val it = |- addition_monoid.op 5 6 = 11: thm 516*) 517 518(* Theorem: properties of addition_monoid *) 519(* Proof: by addition_monoid_def *) 520val addition_monoid_property = store_thm( 521 "addition_monoid_property", 522 ``(addition_monoid.carrier = univ(:num)) /\ 523 (addition_monoid.op = $+ ) /\ 524 (addition_monoid.id = 0)``, 525 rw[addition_monoid_def]); 526 527(* Theorem: AbelianMonoid (addition_monoid) *) 528(* Proof: 529 By AbelianMonoid_def, Monoid_def, addition_monoid_def, this is to show: 530 (1) ?z. z = x + y. Take z = x + y. 531 (2) x + y + z = x + (y + z), true by ADD_ASSOC 532 (3) x + 0 = x /\ 0 + x = x, true by ADD, ADD_0 533 (4) x + y = y + x, true by ADD_COMM 534*) 535val addition_monoid_abelian_monoid = store_thm( 536 "addition_monoid_abelian_monoid", 537 ``AbelianMonoid (addition_monoid)``, 538 rw_tac std_ss[AbelianMonoid_def, Monoid_def, addition_monoid_def, GSPECIFICATION, IN_UNIV] >> 539 simp[]); 540 541(* Theorem: Monoid (addition_monoid) *) 542(* Proof: by addition_monoid_abelian_monoid, AbelianMonoid_def *) 543val addition_monoid_monoid = store_thm( 544 "addition_monoid_monoid", 545 ``Monoid (addition_monoid)``, 546 metis_tac[addition_monoid_abelian_monoid, AbelianMonoid_def]); 547 548(* ------------------------------------------------------------------------- *) 549(* Multiplication of numbers form a Monoid *) 550(* ------------------------------------------------------------------------- *) 551 552(* Define the number multiplication monoid *) 553val multiplication_monoid_def = Define` 554 multiplication_monoid = 555 <| carrier := univ(:num); 556 op := $*; 557 id := 1; 558 |> 559`; 560 561(* 562> EVAL ``multiplication_monoid.op 5 6``; 563val it = |- multiplication_monoid.op 5 6 = 30: thm 564*) 565 566(* Theorem: properties of multiplication_monoid *) 567(* Proof: by multiplication_monoid_def *) 568val multiplication_monoid_property = store_thm( 569 "multiplication_monoid_property", 570 ``(multiplication_monoid.carrier = univ(:num)) /\ 571 (multiplication_monoid.op = $* ) /\ 572 (multiplication_monoid.id = 1)``, 573 rw[multiplication_monoid_def]); 574 575(* Theorem: AbelianMonoid (multiplication_monoid) *) 576(* Proof: 577 By AbelianMonoid_def, Monoid_def, multiplication_monoid_def, this is to show: 578 (1) ?z. z = x * y. Take z = x * y. 579 (2) x * y * z = x * (y * z), true by MULT_ASSOC 580 (3) x * 1 = x /\ 1 * x = x, true by MULT, MULT_1 581 (4) x * y = y * x, true by MULT_COMM 582*) 583val multiplication_monoid_abelian_monoid = store_thm( 584 "multiplication_monoid_abelian_monoid", 585 ``AbelianMonoid (multiplication_monoid)``, 586 rw_tac std_ss[AbelianMonoid_def, Monoid_def, multiplication_monoid_def, GSPECIFICATION, IN_UNIV] >- 587 simp[] >> 588 simp[]); 589 590(* Theorem: Monoid (multiplication_monoid) *) 591(* Proof: by multiplication_monoid_abelian_monoid, AbelianMonoid_def *) 592val multiplication_monoid_monoid = store_thm( 593 "multiplication_monoid_monoid", 594 ``Monoid (multiplication_monoid)``, 595 metis_tac[multiplication_monoid_abelian_monoid, AbelianMonoid_def]); 596 597(* ------------------------------------------------------------------------- *) 598(* Powers of a fixed base form a Monoid *) 599(* ------------------------------------------------------------------------- *) 600 601(* Define the power monoid *) 602val power_monoid_def = Define` 603 power_monoid (b:num) = 604 <| carrier := {b ** j | j IN univ(:num)}; 605 op := $*; 606 id := 1; 607 |> 608`; 609 610(* 611> EVAL ``(power_monoid 2).op (2 ** 3) (2 ** 4)``; 612val it = |- (power_monoid 2).op (2 ** 3) (2 ** 4) = 128: thm 613*) 614 615(* Theorem: properties of power monoid *) 616(* Proof: by power_monoid_def *) 617val power_monoid_property = store_thm( 618 "power_monoid_property", 619 ``!b. ((power_monoid b).carrier = {b ** j | j IN univ(:num)}) /\ 620 ((power_monoid b).op = $* ) /\ 621 ((power_monoid b).id = 1)``, 622 rw[power_monoid_def]); 623 624 625(* Theorem: AbelianMonoid (power_monoid b) *) 626(* Proof: 627 By AbelianMonoid_def, Monoid_def, power_monoid_def, this is to show: 628 (1) ?j''. b ** j * b ** j' = b ** j'' 629 Take j'' = j + j', true by EXP_ADD 630 (2) b ** j * b ** j' * b ** j'' = b ** j * (b ** j' * b ** j'') 631 True by EXP_ADD, ADD_ASSOC 632 (3) ?j. b ** j = 1 633 or ?j. (b = 1) \/ (j = 0), true by j = 0. 634 (4) b ** j * b ** j' = b ** j' * b ** j 635 True by EXP_ADD, ADD_COMM 636*) 637val power_monoid_abelian_monoid = store_thm( 638 "power_monoid_abelian_monoid", 639 ``!b. AbelianMonoid (power_monoid b)``, 640 rw_tac std_ss[AbelianMonoid_def, Monoid_def, power_monoid_def, GSPECIFICATION, IN_UNIV] >- 641 metis_tac[EXP_ADD] >- 642 rw[EXP_ADD] >- 643 metis_tac[] >> 644 rw[EXP_ADD]); 645 646(* Theorem: Monoid (power_monoid b) *) 647(* Proof: by power_monoid_abelian_monoid, AbelianMonoid_def *) 648val power_monoid_monoid = store_thm( 649 "power_monoid_monoid", 650 ``!b. Monoid (power_monoid b)``, 651 metis_tac[power_monoid_abelian_monoid, AbelianMonoid_def]); 652 653(* ------------------------------------------------------------------------- *) 654(* Logarithm is an isomorphism from Power Monoid to Addition Monoid *) 655(* ------------------------------------------------------------------------- *) 656 657(* Theorem: 1 < b ==> MonoidHomo (LOG b) (power_monoid b) (addition_monoid) *) 658(* Proof: 659 By MonoidHomo_def, power_monoid_def, addition_monoid_def, this is to show: 660 (1) LOG b (b ** j * b ** j') = LOG b (b ** j) + LOG b (b ** j') 661 LOG b (b ** j * b ** j') 662 = LOG b (b ** (j + j')) by EXP_ADD 663 = j + j' by LOG_EXACT_EXP 664 = LOG b (b ** j) + LOG b (b ** j') by LOG_EXACT_EXP 665 (2) LOG b 1 = 0, true by LOG_1 666*) 667val power_to_addition_homo = store_thm( 668 "power_to_addition_homo", 669 ``!b. 1 < b ==> MonoidHomo (LOG b) (power_monoid b) (addition_monoid)``, 670 rw[MonoidHomo_def, power_monoid_def, addition_monoid_def] >- 671 rw[LOG_EXACT_EXP, GSYM EXP_ADD] >> 672 rw[LOG_1]); 673 674(* Theorem: 1 < b ==> MonoidIso (LOG b) (power_monoid b) (addition_monoid) *) 675(* Proof: 676 By MonoidIso_def, this is to show: 677 (1) MonoidHomo (LOG b) (power_monoid b) addition_monoid 678 This is true by power_to_addition_homo 679 (2) BIJ (LOG b) (power_monoid b).carrier addition_monoid.carrier 680 By BIJ_DEF, this is to show: 681 (1) INJ (LOG b) {b ** j | j IN univ(:num)} univ(:num) 682 By INJ_DEF, this is to show: 683 LOG b (b ** j) = LOG b (b ** j') ==> b ** j = b ** j' 684 LOG b (b ** j) = LOG b (b ** j') 685 ==> j = j' by LOG_EXACT_EXP 686 ==> b ** j = b ** j' 687 (2) SURJ (LOG b) {b ** j | j IN univ(:num)} univ(:num) 688 By SURJ_DEF, this is to show: 689 ?y. (?j. y = b ** j) /\ (LOG b y = x) 690 Let j = x, y = b ** x, then true by LOG_EXACT_EXP 691*) 692val power_to_addition_iso = store_thm( 693 "power_to_addition_iso", 694 ``!b. 1 < b ==> MonoidIso (LOG b) (power_monoid b) (addition_monoid)``, 695 rw[MonoidIso_def] >- 696 rw[power_to_addition_homo] >> 697 rw_tac std_ss[BIJ_DEF, power_monoid_def, addition_monoid_def] >| [ 698 rw[INJ_DEF] >> 699 rfs[LOG_EXACT_EXP], 700 rw[SURJ_DEF] >> 701 metis_tac[LOG_EXACT_EXP] 702 ]); 703 704(* ------------------------------------------------------------------------- *) 705 706(* export theory at end *) 707val _ = export_theory(); 708 709(*===========================================================================*) 710