1(* ------------------------------------------------------------------------- *) 2(* Applying Ring Theory: Ring Instances *) 3(* ------------------------------------------------------------------------- *) 4 5(* 6 7Ring Instances 8=============== 9The important ones: 10 11Z_n -- Arithmetic under Modulo n. 12 13*) 14(*===========================================================================*) 15 16(* add all dependent libraries for script *) 17open HolKernel boolLib bossLib Parse; 18 19(* declare new theory at start *) 20val _ = new_theory "ringInstances"; 21 22(* ------------------------------------------------------------------------- *) 23 24 25(* val _ = load "jcLib"; *) 26open jcLib; 27 28(* Get dependent theories local *) 29(* (* val _ = load "monoidTheory"; *) *) 30(* (* val _ = load "groupTheory"; *) *) 31(* val _ = load "ringMapTheory"; *) 32open monoidTheory groupTheory ringTheory; 33(* val _ = load "monoidInstancesTheory"; *) 34open monoidInstancesTheory; 35(* val _ = load "groupInstancesTheory"; *) 36open groupInstancesTheory; 37open monoidOrderTheory groupOrderTheory; 38 39open monoidMapTheory groupMapTheory ringMapTheory; 40 41(* Get dependent theories in lib *) 42(* (* val _ = load "helperNumTheory"; -- in monoidTheory *) *) 43(* (* val _ = load "helperFunctionTheory"; -- in ringheory *) *) 44open helperNumTheory helperFunctionTheory; 45 46(* open dependent theories *) 47(* (* val _ = load "dividesTheory"; -- in helperNumTheory *) *) 48(* (* val _ = load "gcdTheory"; -- in helperNumTheory *) *) 49open pred_setTheory arithmeticTheory dividesTheory gcdTheory; 50open EulerTheory; 51 52(* val _ = load "GaussTheory"; *) 53open GaussTheory; 54 55(* val _ = load "whileTheory"; *) 56open whileTheory; (* for order computation by WHILE loop *) 57 58 59(* ------------------------------------------------------------------------- *) 60(* Ring Instances Documentation *) 61(* ------------------------------------------------------------------------- *) 62(* Ring Data type: 63 The generic symbol for ring data is r. 64 r.carrier = Carrier set of Ring, overloaded as R. 65 r.sum = Addition component of Ring, binary operation overloaded as +. 66 r.prod = Multiplication component of Ring, binary operation overloaded as *. 67*) 68(* Overloading: 69 ordz n m = order (ZN n).prod m 70 71*) 72(* Definitions and Theorems (# are exported, ! in computeLib): 73 74 The Trivial Ring (#1 = #0): 75 trivial_ring_def |- !z. trivial_ring z = 76 <|carrier := {z}; 77 sum := <|carrier := {z}; id := z; op := (\x y. z)|>; 78 prod := <|carrier := {z}; id := z; op := (\x y. z)|> 79 |> 80 trivial_ring |- !z. FiniteRing (trivial_ring z) 81 trivial_char |- !z. char (trivial_ring z) = 1 82 83 Arithmetic Modulo n: 84 ZN_def |- !n. ZN n = <|carrier := count n; sum := add_mod n; prod := times_mod n|> 85! ZN_eval |- !n. ((ZN n).carrier = count n) /\ 86 ((ZN n).sum = add_mod n) /\ ((ZN n).prod = times_mod n) 87 ZN_property |- !n. (!x. x IN (ZN n).carrier <=> x < n) /\ ((ZN n).sum.id = 0) /\ 88 ((ZN n).prod.id = if n = 1 then 0 else 1) /\ 89 (!x y. (ZN n).sum.op x y = (x + y) MOD n) /\ 90 (!x y. (ZN n).rr.op x y = (x * y) MOD n) /\ 91 FINITE (ZN n).carrier /\ (CARD (ZN n).carrier = n) 92 ZN_ids |- !n. 0 < n ==> ((ZN n).sum.id = 0) /\ ((ZN n).prod.id = 1 MOD n) 93 ZN_ids_alt |- !n. 1 < n ==> ((ZN n).sum.id = 0) /\ ((ZN n).prod.id = 1) 94 ZN_finite |- !n. FINITE (ZN n).carrier 95 ZN_card |- !n. CARD (ZN n).carrier = n 96 ZN_ring |- !n. 0 < n ==> Ring (ZN n) 97 ZN_char |- !n. 0 < n ==> (char (ZN n) = n) 98 ZN_exp |- !n. 0 < n ==> !x k. (ZN n).prod.exp x k = x ** k MOD n 99 ZN_num |- !n. 0 < n ==> !k. (ZN n).sum.exp 1 k = k MOD n 100 ZN_num_1 |- !n. (ZN n).sum.exp (ZN n).prod.id 1 = 1 MOD n 101 ZN_num_0 |- !n c. 0 < n ==> (ZN n).sum.exp 0 c = 0 102 ZN_num_mod |- !n c. 0 < n ==> (ZN n).sum.exp (ZN n).prod.id c = c MOD n 103 ZN_finite_ring |- !n. 0 < n ==> FiniteRing (ZN n) 104 ZN_invertibles_group |- !n. 0 < n ==> Group (Invertibles (ZN n).prod) 105 ZN_invertibles_finite_group |- !n. 0 < n ==> FiniteGroup (Invertibles (ZN n).prod) 106 107 ZN Inverse: 108 ZN_mult_inv_coprime |- !n. 0 < n ==> !x y. ((x * y) MOD n = 1) ==> coprime x n 109 ZN_mult_inv_coprime_iff |- !n. 1 < n ==> !x. coprime x n <=> ?y. (x * y) MOD n = 1 110 ZN_coprime_invertible |- !m n. 1 < m /\ coprime m n ==> n MOD m IN (Invertibles (ZN m).prod).carrier 111 ZN_invertibles |- !n. 1 < n ==> (Invertibles (ZN n).prod = Estar n) 112 113 ZN Order: 114 ZN_1_exp |- !n k. (ZN 1).prod.exp n k = 0 115 ZN_order_mod_1 |- !n. ordz 1 n = 1 116 ZN_order_mod |- !m n. 0 < m ==> (ordz m (n MOD m) = ordz m n) 117 ZN_invertibles_order |- !m n. 0 < m ==> (order (Invertibles (ZN m).prod) (n MOD m) = ordz m n) 118 ZN_order_0 |- !n. 0 < n ==> (ordz n 0 = if n = 1 then 1 else 0) 119 ZN_order_1 |- !n. 0 < n ==> (ordz n 1 = 1) 120 ZN_order_eq_1 |- !m n. 0 < m ==> ((ordz m n = 1) <=> (n MOD m = 1 MOD m)) 121 ZN_order_eq_1_alt |- !m n. 1 < m ==> (ordz m n = 1 <=> n MOD m = 1) 122 ZN_order_property |- !m n. 0 < m ==> (n ** ordz m n MOD m = 1 MOD m) 123 ZN_order_property_alt |- !m n. 1 < m ==> (n ** ordz m n MOD m = 1) 124 ZN_order_divisibility |- !m n. 0 < m ==> m divides n ** ordz m n - 1 125 ZN_coprime_euler_element |- !m n. 1 < m /\ coprime m n ==> n MOD m IN Euler m 126 ZN_coprime_order |- !m n. 0 < m /\ coprime m n ==> 0 < ordz m n /\ (n ** ordz m n MOD m = 1 MOD m) 127 ZN_coprime_order_alt |- !m n. 1 < m /\ coprime m n ==> 0 < ordz m n /\ (n ** ordz m n MOD m = 1) 128 ZN_coprime_order_divides_totient |- !m n. 0 < m /\ coprime m n ==> ordz m n divides totient m 129 ZN_coprime_order_divides_phi |- !m n. 0 < m /\ coprime m n ==> ordz m n divides phi m 130 ZN_coprime_order_lt |- !m n. 1 < m /\ coprime m n ==> ordz m n < m 131 ZN_coprime_exp_mod |- !m n. 0 < m /\ coprime m n ==> !k. n ** k MOD m = n ** (k MOD ordz m n) MOD m 132 ZN_order_eq_1_by_prime_factors |- !m n. 0 < m /\ coprime m n /\ 133 (!p. prime p /\ p divides n ==> (ordz m p = 1)) ==> (ordz m n = 1) 134 ZN_order_nonzero_iff |- !m n. 1 < m ==> (ordz m n <> 0 <=> ?k. 0 < k /\ (n ** k MOD m = 1)) 135 ZN_order_eq_0_iff |- !m n. 1 < m ==> (ordz m n = 0 <=> !k. 0 < k ==> n ** k MOD m <> 1) 136 ZN_order_nonzero |- !m n. 0 < m ==> (ordz m n <> 0 <=> coprime m n) 137 ZN_order_eq_0 |- !m n. 0 < m ==> ((ordz m n = 0) <=> gcd m n <> 1) 138 ZN_not_coprime |- !m n. 0 < m /\ gcd m n <> 1 ==> !k. 0 < k ==> n ** k MOD m <> 1 139 ZN_order_gt_1_property |- !m n. 0 < m /\ 1 < ordz m n ==> ?p. prime p /\ p divides n /\ 1 < ordz m p 140 ZN_order_divides_exp |- !m n k. 1 < m /\ 0 < k ==> ((n ** k MOD m = 1) <=> ordz m n divides k) 141 ZN_order_divides_phi |- !m n. 0 < m /\ 0 < ordz m n ==> ordz m n divides phi m 142 ZN_order_upper |- !m n. 0 < m ==> ordz m n <= phi m 143 ZN_order_le |- !m n. 0 < m ==> ordz m n <= m 144 ZN_order_lt |- !k n m. 0 < k /\ k < m ==> ordz k n < m 145 ZN_order_minimal |- !m n k. 0 < m /\ 0 < k /\ k < ordz m n ==> n ** k MOD m <> 1 146 ZN_coprime_order_gt_1 |- !m n. 1 < m /\ 1 < n MOD m /\ coprime m n ==> 1 < ordz m 147 ZN_order_with_coprime_1|- !m n. 1 < n /\ coprime m n /\ 1 < ordz m n ==> 1 < m 148 ZN_order_with_coprime_2|- !m n k. 1 < m /\ m divides n /\ 1 < ordz k m /\ coprime k n ==> 149 1 < n /\ 1 < k 150 ZN_order_eq_0_test |- !m n. 1 < m ==> 151 ((ordz m n = 0) <=> !j. 0 < j /\ j < m ==> n ** j MOD m <> 1) 152 ZN_order_divides_tops_index 153 |- !n j k. 1 < n /\ 0 < j /\ 1 < k ==> 154 (k divides tops n j <=> ordz k n divides j) 155 ZN_order_le_tops_index |- !n j k. 1 < n /\ 0 < j /\ 1 < k /\ k divides tops n j ==> 156 ordz k n <= j 157 158 ZN Order Candidate: 159 ZN_order_test_propery |- !m n k. 1 < m /\ 0 < k /\ (n ** k MOD m = 1) /\ 160 (!j. 0 < j /\ j < k /\ j divides phi m ==> n ** j MOD m <> 1) ==> 161 !j. 0 < j /\ j < k /\ ~(j divides phi m) ==> 162 (ordz m n = k) \/ n ** j MOD m <> 1 163 ZN_order_test_1 |- !m n k. 1 < m /\ 0 < k ==> ((ordz m n = k) <=> 164 (n ** k MOD m = 1) /\ !j. 0 < j /\ j < k ==> n ** j MOD m <> 1) 165 ZN_order_test_2 |- !m n k. 1 < m /\ 0 < k ==> ((ordz m n = k) <=> 166 (n ** k MOD m = 1) /\ 167 !j. 0 < j /\ j < k /\ j divides phi m ==> n ** j MOD m <> 1) 168 ZN_order_test_3 |- !m n k. 1 < m /\ 0 < k ==> ((ordz m n = k) <=> 169 k divides phi m /\ (n ** k MOD m = 1) /\ 170 !j. 0 < j /\ j < k /\ j divides phi m ==> n ** j MOD m <> 1) 171 ZN_order_test_4 |- !m n k. 1 < m ==> ((ordz m n = k) <=> (n ** k MOD m = 1) /\ 172 !j. 0 < j /\ j < (if k = 0 then m else k) ==> n ** j MOD m <> 1) 173 174 ZN Homomorphism: 175 ZN_to_ZN_element |- !n m x. 0 < m /\ x IN (ZN n).carrier ==> x MOD m IN (ZN m).carrier 176 ZN_to_ZN_sum_group_homo |- !n m. 0 < n /\ m divides n ==> 177 GroupHomo (\x. x MOD m) (ZN n).sum (ZN m).sum 178 ZN_to_ZN_prod_monoid_homo |- !n m. 0 < n /\ m divides n ==> 179 MonoidHomo (\x. x MOD m) (ZN n).prod (ZN m).prod 180 ZN_to_ZN_ring_homo |- !n m. 0 < n /\ m divides n ==> 181 RingHomo (\x. x MOD m) (ZN n) (ZN m) 182 183 Ring from Sets: 184 symdiff_set_inter_def |- symdiff_set_inter = 185 <|carrier := univ(:'a -> bool); sum := symdiff_set; prod := set_inter|> 186 symdiff_set_inter_ring |- Ring symdiff_set_inter 187 symdiff_set_inter_char |- char symdiff_set_inter = 2 188! symdiff_eval |- (symdiff_set.carrier = univ(:'a -> bool)) /\ 189 (!x y. symdiff_set.op x y = x UNION y DIFF x INTER y) /\ 190 (symdiff_set.id = {}) 191 192 Order Computation using a WHILE loop: 193 compute_ordz_def |- !m n. compute_ordz m n = 194 if m = 0 then ordz 0 n 195 else if m = 1 then 1 196 else if coprime m n then WHILE (\i. (n ** i) MOD m <> 1) SUC 1 197 else 0 198 WHILE_RULE_PRE_POST |- (!x. Invariant x /\ Guard x ==> f (Cmd x) < f x) /\ 199 (!x. Precond x ==> Invariant x) /\ 200 (!x. Invariant x /\ ~Guard x ==> Postcond x) /\ 201 HOARE_SPEC (\x. Invariant x /\ Guard x) Cmd Invariant ==> 202 HOARE_SPEC Precond (WHILE Guard Cmd) Postcond 203 compute_ordz_hoare |- !m n. 1 < m /\ coprime m n ==> 204 HOARE_SPEC (\i. 0 < i /\ i <= ordz m n) 205 (WHILE (\i. (n ** i) MOD m <> 1) SUC) 206 (\i. i = ordz m n) 207 compute_ordz_by_while |- !m n. 1 < m /\ coprime m n ==> !j. 0 < j /\ j <= ordz m n ==> 208 (WHILE (\i. (n ** i) MOD m <> 1) SUC j = ordz m n) 209 210 Correctness of computing ordz m n: 211 compute_ordz_0 |- !n. compute_ordz 0 n = ordz 0 212 compute_ordz_1 |- !n. compute_ordz 1 n = 1 213 compute_ordz_eqn |- !m n. compute_ordz m n = ordz m n 214! ordz_eval |- !m n. order (times_mod m) n = compute_ordz m n 215 216*) 217(* ------------------------------------------------------------------------- *) 218(* The Trivial Ring = {|0|}. *) 219(* ------------------------------------------------------------------------- *) 220 221val trivial_ring_def = Define` 222 (trivial_ring z) : 'a ring = 223 <| carrier := {z}; 224 sum := <| carrier := {z}; 225 id := z; 226 op := (\x y. z) |>; 227 prod := <| carrier := {z}; 228 id := z; 229 op := (\x y. z) |> 230 |> 231`; 232 233(* Theorem: {|0|} is indeed a ring. *) 234(* Proof: by definition, the field tables are: 235 236 + |0| * |0| 237 ------------ ----------- 238 |0| |0| |0| |0| 239*) 240val trivial_ring = store_thm( 241 "trivial_ring", 242 ``!z. FiniteRing (trivial_ring z)``, 243 rw_tac std_ss[FiniteRing_def] >| [ 244 rw_tac std_ss[trivial_ring_def, Ring_def, AbelianGroup_def, group_def_alt, IN_SING, RES_FORALL_THM, RES_EXISTS_THM] >> 245 rw_tac std_ss[AbelianMonoid_def, Monoid_def, IN_SING], 246 rw_tac std_ss[trivial_ring_def, FINITE_SING] 247 ]); 248 249(* Theorem: char (trivial_ring z) = 1 *) 250(* Proof: 251 By fiddling with properties of OLEAST. 252 This is to show: 253 (case OLEAST n. 0 < n /\ (FUNPOW (\y. z) n z = z) of NONE => 0 | SOME n => n) = 1 254 If NONE, 0 = 1 is impossible, so SOME must be true, i.e. to show: 255 ?n. 0 < n /\ (FUNPOW (\y. z) n z = z), and then that n must be 1. 256 First part is simple: 257 let n = 1, then FUNPOW (\y. z) 1 z = (\y. z) z = z by FUNPOW 258 Second part is to show: 259 0 < n /\ (FUNPOW (\y. z) n z = z) /\ !m. m < n ==> ~(0 < m) \/ FUNPOW (\y. z) m z <> z ==> n = 1 260 By contradiction, assume n <> 1, 261 then 0 < n /\ n <> 1 ==> 1 < n, 262 since 0 < 1, this means FUNPOW (\y. z) 1 z <> z, 263 but FUNPOW (\y. z) 1 z = z by FUNPOW, hence a contradiction. 264*) 265val trivial_char = store_thm( 266 "trivial_char", 267 ``!z. char (trivial_ring z) = 1``, 268 strip_tac >> 269 `FiniteRing (trivial_ring z)` by rw_tac std_ss[trivial_ring] >> 270 rw[char_def] >> 271 rw_tac std_ss[order_def, period_def, trivial_ring_def, monoid_exp_def] >> 272 DEEP_INTRO_TAC whileTheory.OLEAST_INTRO >> 273 rw_tac std_ss[] >| [ (* avoid srw_tac simplication *) 274 qexists_tac `1` >> 275 rw[], 276 (spose_not_then strip_assume_tac) >> 277 `1 < n /\ 0 < 1` by decide_tac >> 278 `FUNPOW (\y. z) 1 z <> z` by metis_tac[] >> 279 full_simp_tac (srw_ss()) [] 280 ]); 281(* Michael's proof *) 282val trivial_char = store_thm( 283 "trivial_char", 284 ``!z. char (trivial_ring z) = 1``, 285 rw[char_def, order_def, period_def, trivial_ring_def, monoid_exp_def] >> 286 DEEP_INTRO_TAC whileTheory.OLEAST_INTRO >> 287 rw_tac std_ss[] >| [ (* avoid srw_tac simplication *) 288 qexists_tac `1` >> 289 rw[], 290 `~(1 < n)` suffices_by decide_tac >> 291 strip_tac >> 292 res_tac >> 293 full_simp_tac (srw_ss()) [] 294 ]); 295 296(* ------------------------------------------------------------------------- *) 297(* Z_n, Arithmetic in Modulo n. *) 298(* ------------------------------------------------------------------------- *) 299 300(* Integer Modulo Ring *) 301val ZN_def = zDefine` 302 ZN n : num ring = 303 <| carrier := count n; 304 sum := add_mod n; 305 prod := times_mod n 306 |> 307`; 308(* 309Note: add_mod is defined in groupInstancesTheory. 310times_mod is defined in monoidInstancesTheory. 311*) 312(* Use of zDefine to avoid incorporating into computeLib, by default. *) 313 314(* 315- type_of ``ZN n``; 316> val it = ``:num ring`` : hol_type 317*) 318 319(* Theorem: Evaluation of ZN component fields. *) 320(* Proof: by ZN_def *) 321val ZN_eval = store_thm( 322 "ZN_eval[compute]", 323 ``!n. ((ZN n).carrier = count n) /\ 324 ((ZN n).sum = add_mod n) /\ 325 ((ZN n).prod = times_mod n)``, 326 rw_tac std_ss[ZN_def]); 327(* Put into computeLib, and later with ordz_eval for order computation. *) 328 329(* Theorem: property of ZN Ring *) 330(* Proof: by ZN_def, add_mod_def, times_mod_def. *) 331val ZN_property = store_thm( 332 "ZN_property", 333 ``!n. (!x. x IN (ZN n).carrier <=> x < n) /\ 334 ((ZN n).sum.id = 0) /\ 335 ((ZN n).prod.id = if n = 1 then 0 else 1) /\ 336 (!x y. (ZN n).sum.op x y = (x + y) MOD n) /\ 337 (!x y. (ZN n).prod.op x y = (x * y) MOD n) /\ 338 FINITE (ZN n).carrier /\ 339 (CARD (ZN n).carrier = n)``, 340 rw[ZN_def, add_mod_def, times_mod_def]); 341 342(* Theorem: 0 < n ==> ((ZN n).sum.id = 0) /\ ((ZN n).prod.id = 1 MOD n) *) 343(* Proof: by ZN_property *) 344val ZN_ids = store_thm( 345 "ZN_ids", 346 ``!n. 0 < n ==> ((ZN n).sum.id = 0) /\ ((ZN n).prod.id = 1 MOD n)``, 347 rw[ZN_property]); 348 349(* Theorem: 1 < n ==> ((ZN n).sum.id = 0) /\ ((ZN n).prod.id = 1) *) 350(* Proof: by ZN_ids, ONE_MOD *) 351val ZN_ids_alt = store_thm( 352 "ZN_ids_alt", 353 ``!n. 1 < n ==> ((ZN n).sum.id = 0) /\ ((ZN n).prod.id = 1)``, 354 rw[ZN_ids]); 355 356(* Theorem: (ZN n).carrier is FINITE. *) 357(* Proof: by ZN_ring and FINITE_COUNT. *) 358val ZN_finite = store_thm( 359 "ZN_finite", 360 ``!n. FINITE (ZN n).carrier``, 361 rw[ZN_def]); 362 363(* Theorem: CARD (ZN n).carrier = n *) 364(* Proof: by ZN_property. *) 365val ZN_card = store_thm( 366 "ZN_card", 367 ``!n. CARD (ZN n).carrier = n``, 368 rw[ZN_property]); 369 370(* Theorem: For n > 0, (ZN n) is a Ring. *) 371(* Proof: by checking definitions. 372 For distribution: (x * (y + z) MOD n) MOD n = ((x * y) MOD n + (x * z) MOD n) MOD n 373 LHS = (x * (y + z) MOD n) MOD n 374 = (x MOD n * ((y + z) MOD n) MOD n by LESS_MOD 375 = (x * (y + z)) MOD n by MOD_TIMES2 376 = (x * y + x * z) MOD n by LEFT_ADD_DISTRIB 377 = ((x * y) MOD n + (x + y) MOD n) MOD n by MOD_PLUS 378 = RHS 379*) 380val ZN_ring = store_thm( 381 "ZN_ring", 382 ``!n. 0 < n ==> Ring (ZN n)``, 383 rpt strip_tac >> 384 `!x. x IN count n <=> x < n` by rw[] >> 385 rw_tac std_ss[ZN_def, Ring_def] >- 386 rw_tac std_ss[add_mod_abelian_group] >- 387 rw_tac std_ss[times_mod_abelian_monoid] >- 388 rw_tac std_ss[add_mod_def, count_def] >- 389 rw_tac std_ss[times_mod_def] >> 390 rw_tac std_ss[add_mod_def, times_mod_def] >> 391 metis_tac[LEFT_ADD_DISTRIB, MOD_PLUS, MOD_TIMES2, LESS_MOD]); 392 393(* Theorem: !m n. 0 < n /\ m <= n ==> (FUNPOW (\j. (j + 1) MOD n) m 0 = m MOD n) *) 394(* Proof: by induction on m. 395 Base case: !n. 0 < n /\ 0 <= n ==> (FUNPOW (\j. (j + 1) MOD n) 0 0 = 0 MOD n) 396 By FUNPOW, !f x. FUNPOW f 0 x = x, 397 hence this is true by 0 = 0 MOD n. 398 Step case: !n. 0 < n /\ m <= n ==> (FUNPOW (\j. (j + 1) MOD n) m 0 = m MOD n) ==> 399 !n. 0 < n /\ SUC m <= n ==> (FUNPOW (\j. (j + 1) MOD n) (SUC m) 0 = SUC m MOD n) 400 By FUNPOW_SUC, !f n x. FUNPOW f (SUC n) x = f (FUNPOW f n x) 401 hence (FUNPOW (\j. (j + 1) MOD n) (SUC n) 0 402 = (\j. (j + 1) MOD n) (FUNPOW (\j. (j + 1) MOD n) n 0) by FUNPOW_SUC 403 = (\j. (j + 1) MOD n) (m MOD n) by induction hypothesis 404 = ((m MOD n) + 1) MOD n 405 = (m + 1) MOD n since m < n 406 = SUC m MOD n by ADD1 407*) 408val ZN_lemma1 = prove( 409 ``!m n. 0 < n /\ m <= n ==> (FUNPOW (\j. (j + 1) MOD n) m 0 = m MOD n)``, 410 Induct_on `m` >- 411 srw_tac[ARITH_ss][] >> 412 srw_tac[ARITH_ss][FUNPOW_SUC, ADD1]); 413 414(* Theorem: 0 < n ==> FUNPOW (\j. (j + 1) MOD n) n 0 = 0 *) 415(* Proof: 416 Put m = n in ZN_lemma1: 417 FUNPOW (\j. (j + 1) MOD n) n 0 = n MOD n = 0 by DIVMOD_ID. 418*) 419val ZN_lemma2 = prove( 420 ``!n. 0 < n ==> (FUNPOW (\j. (j + 1) MOD n) n 0 = 0)``, 421 rw_tac std_ss[ZN_lemma1]); 422 423(* Theorem: 0 < n ==> char (ZN n) = n *) 424(* Proof: 425 Depends on the "ZN_lemma": 426 0 < m /\ n <= m ==> FUNPOW (\j. (j + 1) MOD m) n 0 = n MOD m 427 which is proved by induction on n. 428 This is to show: 429 (case OLEAST n'. 0 < n' /\ (FUNPOW (\j. (1 + j) MOD n) n' 0 = 0) of NONE => 0 | SOME n => n) = n 430 If SOME, n = n is trivial. 431 If NONE, need to show impossible for 0 < n: 0 < n' /\ (FUNPOW (\j. (1 + j) MOD n) n' 0 = 0 432 Since (FUNPOW (\j. (1 + j) MOD n) n' 0 = n MOD n' = 0 by by ZN_lemma1 433 and 0 < n' /\ 0 < n ==> n MOD n' <> 0, a contradiction with n MOD n' = 0. 434*) 435val ZN_char = store_thm( 436 "ZN_char", 437 ``!n. 0 < n ==> (char (ZN n) = n)``, 438 rw_tac std_ss[char_def, order_def, period_def] >> 439 DEEP_INTRO_TAC whileTheory.OLEAST_INTRO >> 440 rw_tac std_ss[ZN_def, add_mod_def, times_mod_def, monoid_exp_def] >| [ (* avoid srw_tac simplication *) 441 qexists_tac `1` >> 442 rw[], 443 first_x_assum (qspec_then `n` mp_tac) >> 444 asm_simp_tac (srw_ss() ++ ARITH_ss) [ZN_lemma2], 445 spose_not_then strip_assume_tac >> 446 `1 < n' /\ 0 < 1` by decide_tac >> 447 `FUNPOW (\j. 0) 1 0 = 0` by rw[] >> 448 metis_tac[], 449 `~(FUNPOW (\j. (j + 1) MOD n) n 0 <> 0)` by rw_tac std_ss[ZN_lemma2] >> 450 `!j. FUNPOW (\j. (j + 1) MOD n) n 0 = FUNPOW (\j. (1 + j) MOD n) n 0` by rw_tac arith_ss [] >> 451 `~(n < n')` by metis_tac[] >> 452 `~(n' < n)` suffices_by decide_tac >> 453 rpt strip_tac >> 454 full_simp_tac (srw_ss() ++ ARITH_ss) [ZN_lemma1] 455 ]); 456(* Michael's proof *) 457val ZN_char = store_thm( 458 "ZN_char", 459 ``!n. 0 < n ==> (char (ZN n) = n)``, 460 simp_tac (srw_ss()) [char_def, order_def, period_def, ZN_def, add_mod_def, times_mod_def, monoid_exp_def] >> 461 rpt strip_tac >> 462 DEEP_INTRO_TAC whileTheory.OLEAST_INTRO >> 463 conj_tac >| [ 464 rw_tac std_ss[] >| [ (* avoid srw_tac simplication *) 465 qexists_tac `1` >> 466 rw[], 467 first_x_assum (qspec_then `n` mp_tac) >> 468 asm_simp_tac (srw_ss() ++ ARITH_ss) [ZN_lemma1] 469 ], 470 qx_gen_tac `m` >> 471 rw_tac std_ss[] >| [ (* avoid srw_tac simplication *) 472 spose_not_then strip_assume_tac >> 473 `1 < m` by decide_tac >> 474 `FUNPOW (\j. 0) 1 0 = 0` by rw[] >> 475 metis_tac[], 476 `~(m < n) /\ ~(n < m)` suffices_by decide_tac >> 477 rpt strip_tac >- 478 full_simp_tac (srw_ss() ++ ARITH_ss) [ZN_lemma1] >> 479 first_x_assum (qspec_then `n` mp_tac) >> 480 asm_simp_tac (srw_ss() ++ ARITH_ss) [ZN_lemma1] 481 ] 482 ]); 483 484(* Better proof *) 485 486(* Theorem: 0 < n ==> char (ZN n) = n *) 487(* Proof: 488 If n = 1, (ZN 1).carrier = count 1 = {0} 489 this is to show: n = 1 iff (FUNPOW (\j. 0) n 0 = 0) /\ !m. 0 < m /\ m < n ==> FUNPOW (\j. 0) m 0 <> 0 490 which is true, since FUNPOW (\j. 0) m 0 = 0 for all m, so to falsify 0 < m /\ m < n, n must be 1. 491 If n <> 1, 1 < n, 492 Ring (ZN n) by ZN_ring 493 (ZN n).sum.exp 1 n 494 = FUNPOW (\j. (1 + j) MOD n) n 0 by monoid_exp_def 495 = n MOD n = 0 by ZN_lemma2 496 Hence (ZN n).sum.exp 1 n = 0 497 meaning char (ZN n) n divides by ring_char_divides 498 Let m = char (ZN n), 499 then m <= n by DIVIDES_LE 500 (ZN n).sum.exp 1 m 501 = FUNPOW (\j. (1 + j) MOD n) m 0 by monoid_exp_def 502 = m MOD n by ZN_lemma1 503 = 0 by char_property 504 But m MOD n = 0 means n divides m by DIVIDES_MOD_0 505 Therefore m = n by DIVIDES_ANTISYM 506*) 507val ZN_char = store_thm( 508 "ZN_char", 509 ``!n. 0 < n ==> (char (ZN n) = n)``, 510 rpt strip_tac >> 511 `Ring (ZN n)` by rw_tac std_ss [ZN_ring] >> 512 `(ZN n).sum.id = 0` by rw[ZN_def, add_mod_def] >> 513 `(ZN n).sum.exp 1 n = 0` by rw[ZN_lemma2, ZN_def, add_mod_def, times_mod_def, monoid_exp_def, ADD_COMM] >> 514 Cases_on `n = 1` >| [ 515 `(ZN n).prod.id = 0` by rw[ZN_def, times_mod_def] >> 516 `(char (ZN n)) divides n` by rw[GSYM ring_char_divides] >> 517 metis_tac[DIVIDES_ONE], 518 `(ZN n).prod.id = 1` by rw[ZN_def, times_mod_def] >> 519 `(ZN n).sum.exp 1 n = 0` by rw[ZN_lemma2, ZN_def, add_mod_def, times_mod_def, monoid_exp_def, ADD_COMM] >> 520 `(char (ZN n)) divides n` by rw[GSYM ring_char_divides] >> 521 `(char (ZN n)) <= n` by rw[DIVIDES_LE] >> 522 qabbrev_tac `m = char (ZN n)` >> 523 `(ZN n).sum.exp 1 m = FUNPOW (\j. (j + 1) MOD n) m 0` by rw[ZN_def, add_mod_def, times_mod_def, monoid_exp_def, ADD_COMM] >> 524 `_ = m MOD n` by rw[ZN_lemma1] >> 525 `n divides m` by metis_tac[char_property, DIVIDES_MOD_0] >> 526 metis_tac [DIVIDES_ANTISYM] 527 ]); 528 529(* Theorem: 0 < n ==> !x k. (ZN n).prod.exp x k = (x ** k) MOD n *) 530(* Proof: 531 (ZN n).prod.exp x k 532 = (times_mod n).exp x k by ZN_def 533 = (x MOD n) ** k MOD n by times_mod_exp, 0 < n 534 = (x ** k) MOD n by EXP_MOD, 0 < n 535*) 536val ZN_exp = store_thm( 537 "ZN_exp", 538 ``!n. 0 < n ==> !x k. (ZN n).prod.exp x k = (x ** k) MOD n``, 539 rw[ZN_def, times_mod_exp]); 540 541(* Theorem: 0 < n ==> !k. (ZN n).sum.exp 1 k = k MOD n *) 542(* Proof: 543 (ZN n).sum.exp 1 k 544 = (add_mod n).exp 1 k by ZN_def 545 = (1 * k) MOD n by add_mod_exp, 0 < n 546 = k MOD n by MULT_LEFT_1 547*) 548val ZN_num = store_thm( 549 "ZN_num", 550 ``!n. 0 < n ==> !k. (ZN n).sum.exp 1 k = k MOD n``, 551 rw[ZN_def, add_mod_exp]); 552 553(* Theorem: (ZN n).sum.exp (ZN n).prod.id 1 = 1 MOD n *) 554(* Proof: 555 If n = 0, 556 (ZN 0).sum.exp (ZN 0).prod.id 1 557 = (ZN 0).sum.exp 1 1 by ZN_property, n <> 1 558 = (ZN 0).sum 0 1 by monoid_exp_def 559 = 1 MOD 0 by ZN_property 560 If n = 1. 561 (ZN 1).sum.exp (ZN 1).prod.id 1 562 = (ZN 1).sum.exp 0 1 by ZN_property, n = 1 563 = (ZN 1).sum 0 0 by monoid_exp_def 564 = 0 MOD 1 = 0 by ZN_property 565 = 1 MOD 1 by DIVMOD_ID, n <> 0 566 Otherwise, 1 < n. 567 (ZN n).sum.exp (ZN n).prod.id 1 568 = (ZN n).sum.exp 1 1 by ZN_property, n <> 1 569 = 1 MOD n by ZN_num, 0 < n 570*) 571val ZN_num_1 = store_thm( 572 "ZN_num_1", 573 ``!n. (ZN n).sum.exp (ZN n).prod.id 1 = 1 MOD n``, 574 rpt strip_tac >> 575 Cases_on `n = 0` >| [ 576 `(ZN 0).sum.exp (ZN 0).prod.id 1 = 1 MOD 0` by EVAL_TAC >> 577 rw[], 578 rw[ZN_num, ZN_property] >> 579 EVAL_TAC 580 ]); 581 582(* Theorem: 0 < n ==> ((ZN n).sum.exp 0 c = 0) *) 583(* Proof: 584 By induction on c. 585 Base: (ZN n).sum.exp 0 0 = 0 586 (ZN n).sum.exp 0 0 587 = (ZN n).sum.id by monoid_exp_0 588 = 0 by ZN_property 589 Step: (ZN n).sum.exp 0 c = 0 ==> (ZN n).sum.exp 0 (SUC c) = 0 590 (ZN n).sum.exp 0 (SUC c) 591 = (ZN n).sum.op 0 ((ZN n).sum.exp 0 c) 592 by monoid_exp_SUC 593 = (ZN n).sum.op 0 0 by induction hypothesis 594 = (ZN n).sum.id by monoid_exp_0 595 = 0 by ZN_property 596*) 597val ZN_num_0 = store_thm( 598 "ZN_num_0", 599 ``!n c. 0 < n ==> ((ZN n).sum.exp 0 c = 0)``, 600 strip_tac >> 601 Induct >- 602 rw[ZN_property] >> 603 rw[ZN_property, monoid_exp_def]); 604 605(* Theorem: 0 < n ==> ((ZN n).sum.exp (ZN n).prod.id c = c MOD n) *) 606(* Proof: 607 If n = 1, 608 (ZN 1).sum.exp (ZN 1).prod.id c 609 = (ZN 1).sum.exp 0 c by ZN_property, n = 1 610 = 0 by ZN_num_0 611 = c MOD 1 by MOD_1 612 If n <> 1, 613 (ZN n).sum.exp (ZN n).prod.id c 614 = (ZN n).sum.exp 1 c by ZN_property, n <> 1 615 = c MOD n by ZN_num, 0 < n. 616*) 617val ZN_num_mod = store_thm( 618 "ZN_num_mod", 619 ``!n c. 0 < n ==> ((ZN n).sum.exp (ZN n).prod.id c = c MOD n)``, 620 rpt strip_tac >> 621 rw[ZN_num, ZN_property] >> 622 rw[ZN_num_0]); 623 624(* Theorem: For n > 0, (ZN n) is a FINITE Ring. *) 625(* Proof: by ZN_ring and ZN_finite. *) 626val ZN_finite_ring = store_thm( 627 "ZN_finite_ring", 628 ``!n. 0 < n ==> FiniteRing (ZN n)``, 629 rw_tac std_ss[ZN_ring, ZN_finite, FiniteRing_def]); 630 631(* Theorem: FiniteGroup (Invertibles (ZN n).prod) *) 632(* Proof: 633 Note Ring (ZN n) by ZN_ring 634 so Monoid (ZN n).prod by ring_mult_monoid 635 Thus Group (Invertibles (ZN n).prod) by monoid_invertibles_is_group 636*) 637val ZN_invertibles_group = store_thm( 638 "ZN_invertibles_group", 639 ``!n. 0 < n ==> Group (Invertibles (ZN n).prod)``, 640 rw[ZN_ring, monoid_invertibles_is_group]); 641 642(* Theorem: FiniteGroup (Invertibles (ZN n).prod) *) 643(* Proof: 644 By FiniteGroup_def, this is to show: 645 (1) Group (Invertibles (ZN n).prod), true by ZN_invertibles_group 646 (2) FINITE (Invertibles (ZN n).prod).carrier 647 Note Ring (ZN n) by ZN_ring 648 Since FINITE (ZN n).carrier by ZN_finite 649 Hence FINITE (Invertibles (ZN n).prod).carrier by Invertibles_subset, SUBSET_FINITE 650*) 651val ZN_invertibles_finite_group = store_thm( 652 "ZN_invertibles_finite_group", 653 ``!n. 0 < n ==> FiniteGroup (Invertibles (ZN n).prod)``, 654 rw[FiniteGroup_def] >- 655 rw[ZN_invertibles_group] >> 656 metis_tac[ZN_finite, Invertibles_subset, SUBSET_FINITE, ZN_ring, ring_carriers]); 657 658(* ------------------------------------------------------------------------- *) 659(* ZN Inverse *) 660(* ------------------------------------------------------------------------- *) 661 662(* Theorem: 0 < n ==> !x y. ((x * y) MOD n = 1) ==> coprime x n *) 663(* Proof: 664 (x * y) MOD n = 1 665 ==> ?k. x * y = k * n + 1 by MOD_EQN 666 Let d = gcd x n, 667 Since d divides x by GCD_IS_GREATEST_COMMON_DIVISOR 668 so d divides x * y by DIVIDES_MULT 669 Also d divides n by GCD_IS_GREATEST_COMMON_DIVISOR 670 so d divides k * n by DIVIDES_MULTIPLE 671 Thus d divides gcd (k * n) (x * y) by GCD_IS_GREATEST_COMMON_DIVISOR 672 But gcd (k * n) (x * y) 673 = gcd (k * n) (k * n + 1) by above 674 = 1 by coprime_SUC 675 so d divides 1, or d = 1 by DIVIDES_ONE 676*) 677val ZN_mult_inv_coprime = store_thm( 678 "ZN_mult_inv_coprime", 679 ``!n. 0 < n ==> !x y. ((x * y) MOD n = 1) ==> coprime x n``, 680 rpt strip_tac >> 681 `?k. x * y = k * n + 1` by metis_tac[MOD_EQN] >> 682 qabbrev_tac `d = gcd x n` >> 683 `d divides x * y` by rw[DIVIDES_MULT, GCD_IS_GREATEST_COMMON_DIVISOR, Abbr`d`] >> 684 `d divides k * n` by rw[DIVIDES_MULTIPLE, GCD_IS_GREATEST_COMMON_DIVISOR, Abbr`d`] >> 685 `d divides gcd (k * n) (x * y)` by rw[GCD_IS_GREATEST_COMMON_DIVISOR] >> 686 metis_tac[coprime_SUC, DIVIDES_ONE]); 687 688(* Theorem: 1 < n ==> !x. coprime x n <=> ?y. (x * y) MOD n = 1 *) 689(* Proof: 690 If part: coprime x n ==> ?y. (x * y) MOD n = 1 691 This is true by GCD_ONE_PROPERTY 692 Only-if part: (x * y) MOD n = 1 ==> coprime x n 693 This is true by ZN_mult_inv_coprime, 0 < n 694*) 695val ZN_mult_inv_coprime_iff = store_thm( 696 "ZN_mult_inv_coprime_iff", 697 ``!n. 1 < n ==> !x. coprime x n <=> ?y. (x * y) MOD n = 1``, 698 rpt strip_tac >> 699 `0 < n` by decide_tac >> 700 rw[EQ_IMP_THM] >- 701 metis_tac[GCD_ONE_PROPERTY, GCD_SYM, MULT_COMM] >> 702 metis_tac[ZN_mult_inv_coprime]); 703 704(* Theorem: 1 < m /\ coprime m n ==> (n MOD m) IN (Invertibles (ZN m).prod).carrier *) 705(* Proof: 706 Expanding by Invertibles_def, ZN_def, this is to show: 707 (1) n MOD m < m 708 Since 1 < m ==> 0 < m, true by MOD_LESS. 709 (2) ?y. y < m /\ ((n MOD m * y) MOD m = 1) /\ ((y * n MOD m) MOD m = 1) 710 Since n MOD m < m by MOD_LESS 711 ?y. 0 < y /\ y < m /\ coprime n y /\ 712 ((y * (n MOD m)) MOD m = 1) by GCD_MOD_MULT_INV 713 The result follows by MULT_COMM 714*) 715val ZN_coprime_invertible = store_thm( 716 "ZN_coprime_invertible", 717 ``!m n. 1 < m /\ coprime m n ==> (n MOD m) IN (Invertibles (ZN m).prod).carrier``, 718 rpt strip_tac >> 719 `0 < n /\ 0 < n MOD m` by metis_tac[MOD_NONZERO_WHEN_GCD_ONE] >> 720 `0 < m` by decide_tac >> 721 rw_tac std_ss[Invertibles_def, monoid_invertibles_def, ZN_def, times_mod_def, GSPECIFICATION, IN_COUNT] >- 722 metis_tac[] >> 723 metis_tac[MOD_LESS, coprime_mod, GCD_MOD_MULT_INV, MULT_COMM]); 724 725(* Same result with a different proof. *) 726 727(* Theorem: 1 < m ==> coprime m n ==> n IN (Invertibles (ZN m).prod) *) 728(* Proof: 729 Expanding by definitions, this is to show: 730 (1) n MOD m < m 731 True by MOD_LESS 732 (2) ?y. y < m /\ ((n MOD m * y) MOD m = 1) /\ ((y * n MOD m) MOD m = 1) 733 We have n MOD m) < m by MOD_LESS 734 and 0 < (n MOD m) by MOD_NONZERO_WHEN_GCD_ONE 735 also coprime m (n MOD m) by coprime_mod 736 Hence ?y. 0 < y /\ y < m /\ 737 (y * (n MOD m)) MOD m = 1 by GCD_MOD_MULT_INV 738 and ((n MOD m) * y) MOD m = 1 by MULT_COMM 739*) 740val ZN_coprime_invertible = store_thm( 741 "ZN_coprime_invertible", 742 ``!m n. 1 < m /\ coprime m n ==> (n MOD m) IN (Invertibles (ZN m).prod).carrier``, 743 rw_tac std_ss[Invertibles_def, monoid_invertibles_def, ZN_def, times_mod_def, GSPECIFICATION, IN_COUNT] >- 744 rw[] >> 745 `0 < m` by decide_tac >> 746 `(n MOD m) < m` by rw[] >> 747 metis_tac[MOD_NONZERO_WHEN_GCD_ONE, GCD_MOD_MULT_INV, coprime_mod, MULT_COMM]); 748 749(* Theorem: 1 < n ==> (Invertibles (ZN n).prod = Estar n) *) 750(* Proof: 751 Note 1 < n ==> 0 < n /\ n <> 1 752 and (ZN n).prod.carrier = (ZN n).carrier by ZN_ring, ring_carriers, 0 < n 753 By Invertibles_def, Estar_def, this is to show: 754 (1) monoid_invertibles (ZN n).prod = Euler n 755 By monoid_invertibles_def, Euler_def, EXTENSION, ZN_property, this is to show: 756 x < n /\ (?y. y < n /\ ((x * y) MOD n = 1)) <=> 0 < x /\ x < n /\ coprime n x 757 That is: 758 (1) (x * y) MOD n = 1 ==> 0 < x 759 By contradiction, suppose x = 0. 760 Then 0 MOD n = 1 by MULT 761 or 0 = 1 by ZERO_MOD 762 which is a contradiction. 763 (2) (x * y) MOD n = 1 ==> coprime n x, true by ZN_mult_inv_coprime 764 (3) coprime n x ==> ?y. y IN (ZN n).prod.carrier /\ ((x * y) MOD n = 1) 765 Note ?z. (x * z) MOD n = 1 by ZN_mult_inv_coprime_iff 766 Let y = z MOD n. 767 Then y < n by MOD_LESS 768 so y IN (ZN n).prod.carrier by ZN_property 769 (x * y) MOD n 770 = (x * (z MOD n)) MOD n by y = z MOD n 771 = (x * z) MOD n by MOD_TIMES2, MOD_MOD 772 = 1 by above 773 (2) (ZN n).prod.op = (\i j. (i * j) MOD n), true by FUN_EQ_THM, ZN_property 774 (3) (ZN n).prod.id = 1, true by ZN_property, n <> 1 775*) 776val ZN_invertibles = store_thm( 777 "ZN_invertibles", 778 ``!n. 1 < n ==> (Invertibles (ZN n).prod = Estar n)``, 779 rpt strip_tac >> 780 `0 < n /\ n <> 1` by decide_tac >> 781 `(ZN n).prod.carrier = (ZN n).carrier` by rw[ZN_ring, ring_carriers] >> 782 rw[Invertibles_def, Estar_def] >| [ 783 rw[monoid_invertibles_def, Euler_def, EXTENSION, ZN_property] >> 784 rw[EQ_IMP_THM] >| [ 785 spose_not_then strip_assume_tac >> 786 `(x = 0) /\ (1 <> 0)` by decide_tac >> 787 metis_tac[MULT, ZERO_MOD], 788 metis_tac[ZN_mult_inv_coprime, coprime_sym], 789 `?z. (x * z) MOD n = 1` by rw[GSYM ZN_mult_inv_coprime_iff, coprime_sym] >> 790 qexists_tac `z MOD n` >> 791 rpt strip_tac >- 792 rw[MOD_LESS] >> 793 metis_tac[MOD_TIMES2, MOD_MOD] 794 ], 795 rw[FUN_EQ_THM, ZN_property], 796 rw[ZN_property] 797 ]); 798 799(* ------------------------------------------------------------------------- *) 800(* ZN Order *) 801(* ------------------------------------------------------------------------- *) 802 803(* Overload for order of m in (ZN n).prod *) 804val _ = overload_on("ordz", ``\n m. order (ZN n).prod m``); 805 806(* Order for MOD 1: 807 808I thought ordz m n is only defined for 1 < m, 809as (x ** j) MOD 1 = 0 by MOD_1, or (x ** j) MOD 1 <> 1. 810However, Ring (ZN 1) by ZN_ring. 811In fact (ZN 1) = {0} is trivial ring, or 1 = 0. 812Thus (x ** j = 1) MOD 1, and the least j is 1. 813 814*) 815 816(* Theorem: (ZN 1).prod.exp n k = 0 *) 817(* Proof: 818 By monoid_exp_def, ZN_property, this is to show: 819 FUNPOW ((ZN 1).prod.op n) k 0 = 0 820 Note (ZN 1).prod.op n = K 0 by ZN_property, FUN_EQ_THM 821 Thus the goal is: FUNPOW (K 0) k 0 = 0 822 823 By induction on k. 824 Base: FUNPOW (K 0) 0 0 = 0, true by FUNPOW 825 Step: FUNPOW (K 0) k 0 = 0 ==> FUNPOW (K 0) (SUC k) 0 = 0 826 FUNPOW (K 0) (SUC k) 0 827 = FUNPOW (K 0) k ((K 0) 0) by FUNPOW 828 = FUNPOW (K 0) k 0 by K_THM 829 = 0 by induction hypothesis 830*) 831val ZN_1_exp = store_thm( 832 "ZN_1_exp", 833 ``!n k. (ZN 1).prod.exp n k = 0``, 834 rw[monoid_exp_def, ZN_property] >> 835 `(ZN 1).prod.op n = K 0` by rw[ZN_property, FUN_EQ_THM] >> 836 rw[] >> 837 Induct_on `k` >> 838 rw[FUNPOW]); 839 840(* Theorem: ordz 1 n = 1 *) 841(* Proof: 842 By order_def, period_def, and ZN_property, this is to show: 843 (case OLEAST k. 0 < k /\ ((ZN 1).prod.exp n k = 0) of NONE => 0 | SOME k => k) = 1 844 Note (ZN 1).prod.exp n k = 0 by ZN_1_exp 845 The goal becomes: (case OLEAST k. 0 < k of NONE => 0 | SOME k => k) = 1 846 or 0 < n /\ !m. m < n ==> (m = 0) ==> n = 1 by OLEAST_INTRO 847 By contradiction, suppose n <> 1. 848 Then 1 < n by n <> 0, n <> 1 849 By implication, 1 = 0, which is a contradiction. 850*) 851val ZN_order_mod_1 = store_thm( 852 "ZN_order_mod_1", 853 ``!n. ordz 1 n = 1``, 854 rw[order_def, period_def, ZN_property] >> 855 rw[ZN_1_exp] >> 856 DEEP_INTRO_TAC whileTheory.OLEAST_INTRO >> 857 rw[] >> 858 spose_not_then strip_assume_tac >> 859 `1 < n /\ 1 <> 0` by decide_tac >> 860 metis_tac[]); 861 862(* Theorem: 0 < m ==> ordz m (n MOD m) = ordz m n *) 863(* Proof: 864 Since (ZN m).prod = times_mod m by ZN_def 865 and !k. (times_mod m).exp (n MOD m) k = (times_mod m).exp n k by times_mod_exp, MOD_MOD 866 Expanding by order_def, period_def, this is trivially true. 867*) 868val ZN_order_mod = store_thm( 869 "ZN_order_mod", 870 ``!m n. 0 < m ==> (ordz m (n MOD m) = ordz m n)``, 871 rw[ZN_def, times_mod_exp, order_def, period_def]); 872 873(* Theorem: 0 < m ==> (order (Invertibles (ZN m).prod) (n MOD m) = ordz m n) *) 874(* Proof: 875 order (Invertibles (ZN m).prod) (n MOD m) 876 = ordz m (n MOD m) by Invertibles_order 877 = ordz m n by ZN_order_mod, 0 < m 878*) 879val ZN_invertibles_order = store_thm( 880 "ZN_invertibles_order", 881 ``!m n. 0 < m ==> (order (Invertibles (ZN m).prod) (n MOD m) = ordz m n)``, 882 rw[Invertibles_order, ZN_order_mod]); 883 884(* 885> order_thm |> ISPEC ``(ZN n).prod`` |> SPEC ``0`` |> SPEC ``1``; 886val it = |- 0 < 1 ==> ((ordz n 0 = 1) <=> 887 ((ZN n).prod.exp 0 1 = (ZN n).prod.id) /\ 888 !m. 0 < m /\ m < 1 ==> (ZN n).prod.exp 0 m <> (ZN n).prod.id): thm 889> order_eq_0 |> ISPEC ``(ZN n).prod`` |> SPEC ``0``; 890val it = |- (ordz n 0 = 0) <=> !n'. 0 < n' ==> (ZN n).prod.exp 0 n' <> (ZN n).prod.id: thm 891> monoid_order_eq_1 |> ISPEC ``(ZN n).prod``; 892val it = |- Monoid (ZN n).prod ==> !x. x IN (ZN n).prod.carrier ==> ((ordz n x = 1) <=> (x = (ZN n).prod.id)): thm 893*) 894 895(* Theorem: 0 < n ==> (ordz n 0 = if n = 1 then 1 else 0) *) 896(* Proof: 897 If n = 1, 898 to show: 0 < n ==> ordz 1 0 = 1. 899 Let g = (ZN 1).prod 900 Then Monoid g by ZN_ring, ring_mult_monoid, 0 < n 901 and g.id = 0 by ZN_def, times_mod_def 902 Note 0 IN g.carrier by monoid_id_element 903 Thus ordz 1 0 = 1 by monoid_order_eq_1 904 If n <> 1, 905 to show: 0 < n /\ n <> 1 ==> ordz 1 0 = 0. 906 By order_eq_0, this is 907 to show: !k. 0 < k ==> (ZN n).prod.exp 0 k <> (ZN n).prod.id 908 or: !k. 0 < k ==> (0 ** k) MOD n <> 1 by ZN_property, ZN_exp 909 or: 0 <> 1 by ZERO_EXP, 0 < k 910 which is true. 911*) 912val ZN_order_0 = store_thm( 913 "ZN_order_0", 914 ``!n. 0 < n ==> (ordz n 0 = if n = 1 then 1 else 0)``, 915 rw[] >| [ 916 `(ZN 1).prod.id = 0` by rw[ZN_def, times_mod_def] >> 917 `Monoid (ZN 1).prod` by rw[ZN_ring, ring_mult_monoid] >> 918 metis_tac[monoid_order_eq_1, monoid_id_element], 919 rw[order_eq_0, ZN_property, ZN_exp, ZERO_EXP] 920 ]); 921 922(* Theorem: 0 < n ==> (ordz n 1 = 1) *) 923(* Proof: 924 If n = 1, 925 to show: ordz 1 1 = 1, true by ZN_order_mod_1 926 If n <> 1, 927 Note Ring (ZN n) by ZN_ring, 0 < n 928 so Monoid (ZN n).prod by ring_mult_monoid 929 and (ZN n).prod.id = 1 by ZN_property, n <> 1 930 ==> ordz n 1 = 1 by monoid_order_id 931*) 932val ZN_order_1 = store_thm( 933 "ZN_order_1", 934 ``!n. 0 < n ==> (ordz n 1 = 1)``, 935 rpt strip_tac >> 936 Cases_on `n = 1` >- 937 rw[ZN_order_mod_1] >> 938 `0 < n /\ n <> 1` by decide_tac >> 939 `Ring (ZN n)` by rw[ZN_ring] >> 940 `Monoid (ZN n).prod` by rw[ring_mult_monoid] >> 941 `(ZN n).prod.id = 1` by rw[ZN_property] >> 942 metis_tac[monoid_order_id]); 943 944(* Theorem: 0 < m ==> ((ordz m n = 1) <=> (n MOD m = 1 MOD m)) *) 945(* Proof: 946 First, Ring (ZN m) by ZN_ring, 0 < m 947 so Monoid (ZN m).prod by ring_mult_monoid 948 and (ZN m).prod.carrier = (ZN m).carrier by ring_carriers 949 with (ZN m).prod.id = 1 MOD m by ZN_property 950 951 Now, n MOD m IN (ZN m).carrier by ZN_property 952 and ordz m n = ordz m (n MOD m) by ZN_order_mod, 1 < m 953 Thus n MOD m = 1 MOD m by monoid_order_eq_1 954*) 955val ZN_order_eq_1 = store_thm( 956 "ZN_order_eq_1", 957 ``!m n. 0 < m ==> ((ordz m n = 1) <=> (n MOD m = 1 MOD m))``, 958 rpt strip_tac >> 959 `Ring (ZN m)` by rw[ZN_ring] >> 960 `Monoid (ZN m).prod` by rw[] >> 961 `ordz m n = ordz m (n MOD m)` by rw[ZN_order_mod] >> 962 rw[monoid_order_eq_1, ZN_property]); 963 964(* Theorem: 1 < m ==> ((ordz m n = 1) <=> (n MOD m = 1)) *) 965(* Proof: ZN_order_eq_1, ONE_MOD *) 966val ZN_order_eq_1_alt = store_thm( 967 "ZN_order_eq_1_alt", 968 ``!m n. 1 < m ==> ((ordz m n = 1) <=> (n MOD m = 1))``, 969 rw[ZN_order_eq_1]); 970 971(* Theorem: 0 < m ==> (n ** ordz m n MOD m = 1 MOD m) *) 972(* Proof: 973 Let k = ordz m n. 974 To show: n ** k MOD m = 1 975 n ** k MOD m 976 = (ZN m).prod.exp n k by ZN_exp, 0 < m 977 = (ZN m).prod.id by order_property 978 = 1 MOD m by ZN_property 979*) 980val ZN_order_property = store_thm( 981 "ZN_order_property", 982 ``!m n. 0 < m ==> (n ** ordz m n MOD m = 1 MOD m)``, 983 rw[order_property, ZN_property, GSYM ZN_exp]); 984 985(* Theorem: 1 < m ==> (n ** ordz m n MOD m = 1) *) 986(* Proof: by ZN_order_property, ONE_MOD *) 987val ZN_order_property_alt = store_thm( 988 "ZN_order_property_alt", 989 ``!m n. 1 < m ==> (n ** ordz m n MOD m = 1)``, 990 rw[ZN_order_property]); 991 992(* Theorem: 0 < m ==> m divides (n ** ordz m n - 1) *) 993(* Proof: 994 If m = 1, true by ONE_DIVIDES_ALL 995 If m <> 1, then 1 < m by 0 < m, m <> 1 996 Let k = ordz m n, to show: m divides n ** k - 1. 997 Since n ** k MOD m = 1 by ZN_order_property, 0 < m 998 or n ** k MOD m = 1 MOD m by ONE_MOD, 1 < m 999 so (n ** k - 1) MOD m = 0 by MOD_EQ_DIFF, 0 < m 1000 Hence m divides (n ** k - 1) by DIVIDES_MOD_0, 0 < m 1001*) 1002val ZN_order_divisibility = store_thm( 1003 "ZN_order_divisibility", 1004 ``!m n. 0 < m ==> m divides (n ** ordz m n - 1)``, 1005 rpt strip_tac >> 1006 Cases_on `m = 1` >- 1007 rw[] >> 1008 rw[DIVIDES_MOD_0, MOD_EQ_DIFF, ONE_MOD, ZN_order_property]); 1009 1010(* Theorem: 1 < m /\ coprime m n ==> (n MOD m) IN Euler m *) 1011(* Proof: 1012 By Euler_def, this is to show: 1013 (1) 0 < n MOD m. 1014 Note 0 < n by GCD_0, m <> 1 1015 Thus true by MOD_NONZERO_WHEN_GCD_ONE 1016 (2) coprime m (n MOD m), true by MOD_WITH_GCD_ONE, 0 < m. 1017*) 1018val ZN_coprime_euler_element = store_thm( 1019 "ZN_coprime_euler_element", 1020 ``!m n. 1 < m /\ coprime m n ==> (n MOD m) IN Euler m``, 1021 rw[Euler_def] >| [ 1022 `n <> 0` by metis_tac[GCD_0, LESS_NOT_EQ] >> 1023 rw[MOD_NONZERO_WHEN_GCD_ONE], 1024 rw[MOD_WITH_GCD_ONE] 1025 ]); 1026 1027(* Theorem: 0 < m /\ coprime m n ==> 0 < ordz m n /\ (n ** ordz m n MOD m = 1 MOD m) *) 1028(* Proof: 1029 If m = 1, 1030 Then ordz 1 n = 1 > 0 by ZN_order_mod_1 1031 and n ** ordz m n MOD 1 = 1 MOD 1 by MOD_1 1032 If m <> 1, 1033 Then 1 < m by m <> 1, m <> 0 1034 and 1 MOD m = 1 by ONE_MOD, 1 < m 1035 also (n MOD m) IN (Invertibles (ZN m).prod).carrier by ZN_coprime_invertible, 1 < m 1036 Now, FiniteGroup (Invertibles (ZN m).prod) by ZN_invertibles_finite_group, 0 < m 1037 and order (Invertibles (ZN m).prod) (n MOD m) = ordz m n by ZN_invertibles_order, 0 < m 1038 and (ZN m).prod.id = 1 by ZN_property, m <> 1 1039 Hence 0 < ordz m n by group_order_property 1040 and n ** (ordz m n) = (ZN m).prod.id = 1 by Invertibles_property, ZN_exp, EXP_MOD 1041*) 1042val ZN_coprime_order = store_thm( 1043 "ZN_coprime_order", 1044 ``!m n. 0 < m /\ coprime m n ==> 0 < ordz m n /\ (n ** ordz m n MOD m = 1 MOD m)``, 1045 ntac 3 strip_tac >> 1046 Cases_on `m = 1` >- 1047 rw[ZN_order_mod_1] >> 1048 `FiniteGroup (Invertibles (ZN m).prod)` by rw[ZN_invertibles_finite_group] >> 1049 `(n MOD m) IN (Invertibles (ZN m).prod).carrier` by rw[ZN_coprime_invertible] >> 1050 `order (Invertibles (ZN m).prod) (n MOD m) = ordz m n` by rw[ZN_invertibles_order] >> 1051 `(ZN m).prod.id = 1` by rw[ZN_property] >> 1052 `1 MOD m = 1` by rw[] >> 1053 metis_tac[group_order_property, Invertibles_property, ZN_exp, EXP_MOD]); 1054 1055(* This is slightly better than the next: ZN_coprime_order_alt *) 1056 1057(* Theorem: 1 < m /\ coprime m n ==> 0 < ordz m n /\ (n ** (ordz m n) = 1) *) 1058(* Proof: by ZN_coprime_order, ONE_MOD *) 1059val ZN_coprime_order_alt = store_thm( 1060 "ZN_coprime_order_alt", 1061 ``!m n. 1 < m /\ coprime m n ==> 0 < ordz m n /\ ((n ** (ordz m n)) MOD m = 1)``, 1062 rw[ZN_coprime_order]); 1063 1064(* Theorem: 0 < m /\ coprime m n ==> (ordz m n) divides (totient m) *) 1065(* Proof: 1066 If m = 1, 1067 Then ordz 1 n = 1 by ZN_order_mod_1 1068 and 1 divides (totient 1) by ONE_DIVIDES_ALL 1069 If m <> 1, then 1 < m by 0 < m, m <> 1 1070 Let x = n MOD m 1071 Step 1: show x IN (Estar m).carrier, apply Euler_Fermat_thm 1072 Since coprime m n ==> ~(m divides n) by coprime_not_divides 1073 so x <> 0 by DIVIDES_MOD_0 1074 hence 0 < x /\ x < m by MOD_LESS, 0 < m 1075 and coprime m x by coprime_mod, 0 < m 1076 Thus x IN (Estar m).carrier by Estar_element 1077 ==> x ** (totient m) MOD m = 1 by Euler_Fermat_eqn (1) 1078 Step 2: show x IN (ZN m).prod.carrier, apply monoid_order_condition 1079 Now, Ring (ZN m) by ZN_ring, 0 < m 1080 ==> Monoid (ZN m).prod by ring_mult_monoid 1081 and (ZN m).prod.id = 1 by ZN_property, m <> 1 1082 hence x IN (ZN m).prod.carrier by ZN_property, MOD_LESS, 0 < m 1083 Thus ordz m x = ordz m n by ZN_order_mod, 1 < m 1084 and (1) becomes 1085 (ZN m).prod.exp x (totient m) = (ZN m).prod.id by ZN_exp 1086 Therefore (ordz m n) divides (totient m) by monoid_order_condition 1087*) 1088val ZN_coprime_order_divides_totient = store_thm( 1089 "ZN_coprime_order_divides_totient", 1090 ``!m n. 0 < m /\ coprime m n ==> (ordz m n) divides (totient m)``, 1091 rpt strip_tac >> 1092 Cases_on `m = 1` >- 1093 rw[ZN_order_mod_1] >> 1094 qabbrev_tac `x = n MOD m` >> 1095 `x < m` by rw[Abbr`x`] >> 1096 `~(m divides n)` by rw[coprime_not_divides] >> 1097 `x <> 0` by rw[GSYM DIVIDES_MOD_0, Abbr`x`] >> 1098 `0 < x` by decide_tac >> 1099 `coprime m x` by metis_tac[coprime_mod] >> 1100 `x IN (Estar m).carrier` by rw[Estar_element] >> 1101 `x ** (totient m) MOD m = 1` by rw[Euler_Fermat_eqn] >> 1102 `Ring (ZN m)` by rw[ZN_ring] >> 1103 `Monoid (ZN m).prod` by rw[ring_mult_monoid] >> 1104 `m <> 1` by decide_tac >> 1105 `(ZN m).prod.id = 1` by rw[ZN_property] >> 1106 `x IN (ZN m).prod.carrier` by rw[ZN_property, MOD_LESS, Abbr`x`] >> 1107 metis_tac[monoid_order_condition, ZN_exp, ZN_order_mod]); 1108 1109(* Theorem: 0 < m /\ coprime m n ==> (ordz m n) divides (phi m) *) 1110(* Proof: 1111 If m = 1, then ordz 1 n = 1 by ZN_order_mod_1 1112 and 1 divides (phi 1) by ONE_DIVIDES_ALL 1113 If m <> 1, then 1 < m by 0 < m, m <> 1 1114 so phi m = totient m by phi_eq_totient, 1 < m 1115 thus (ordz m n) divides (phi m) by ZN_coprime_order_divides_totient 1116*) 1117val ZN_coprime_order_divides_phi = store_thm( 1118 "ZN_coprime_order_divides_phi", 1119 ``!m n. 0 < m /\ coprime m n ==> (ordz m n) divides (phi m)``, 1120 rpt strip_tac >> 1121 Cases_on `m = 1` >- 1122 rw[ZN_order_mod_1] >> 1123 rw[ZN_coprime_order_divides_totient, phi_eq_totient]); 1124 1125(* Theorem: 1 < m /\ coprime m n ==> ordz m n < m *) 1126(* Proof: 1127 Note ordz m n divides phi m by ZN_coprime_order_divides_phi, 0 < m 1128 and 0 < phi m by phi_pos, 0 < m 1129 Thus ordz m n <= phi m by DIVIDES_LE, 0 < phi m 1130 < m by phi_lt, 1 < m 1131*) 1132val ZN_coprime_order_lt = store_thm( 1133 "ZN_coprime_order_lt", 1134 ``!m n. 1 < m /\ coprime m n ==> ordz m n < m``, 1135 rpt strip_tac >> 1136 `0 < phi m /\ phi m < m` by rw[phi_pos, phi_lt] >> 1137 `ordz m n <= phi m` by rw[ZN_coprime_order_divides_phi, DIVIDES_LE] >> 1138 decide_tac); 1139 1140(* Theorem: 0 < m /\ coprime m n ==> !k. (n ** k) MOD m = (n ** (k MOD (ordz m n))) MOD m *) 1141(* Proof: 1142 If m = 1, true since ordz 1 n = 1 by ZN_order_mod_1 1143 If m <> 1, then 1 < m by 0 < m, m <> 1 1144 Let z = ordz m n. 1145 Note 1 < m ==> 0 < m by arithmetic 1146 and 0 < z by ZN_coprime_order_alt, 1 < m, coprime m n 1147 Let g = Invertibles (ZN m).prod, the Euler group. 1148 Then FiniteGroup g by ZN_invertibles_finite_group, 0 < m 1149 ==> n MOD m IN g.carrier by ZN_coprime_invertible, 1 < n, coprime m n 1150 Note z = ordz m n by ZN_order_mod, 1 < m 1151 = order g (n MOD m) by ZN_invertibles_order, 1 < m, coprime m n 1152 1153 Let x = n MOD m 1154 Then x IN g.carrier by above 1155 and 0 < order g x by above, 0 < z 1156 Note !x k. g.exp x k = (ZN m).prod.exp x k by Invertibles_property 1157 and !x k.(ZN m).prod.exp x k = (x ** k) MOD m by ZN_exp 1158 1159 (n ** k) MOD m 1160 = ((n MOD m) ** k) MOD m by EXP_MOD, 0 < m 1161 = ((n MOD m) ** (k MOD z)) MOD m by group_exp_mod_order, n MOD m IN g.carrier, 0 < z 1162 = ((n ** (k MOD z)) MOD m) by EXP_MOD, 0 < m 1163*) 1164val ZN_coprime_exp_mod = store_thm( 1165 "ZN_coprime_exp_mod", 1166 ``!m n. 0 < m /\ coprime m n ==> !k. (n ** k) MOD m = (n ** (k MOD (ordz m n))) MOD m``, 1167 rpt strip_tac >> 1168 Cases_on `m = 1` >- 1169 rw[ZN_order_mod_1] >> 1170 qabbrev_tac `z = ordz m n` >> 1171 `0 < m` by decide_tac >> 1172 `0 < z` by rw[ZN_coprime_order_alt, Abbr`z`] >> 1173 qabbrev_tac `g = Invertibles (ZN m).prod` >> 1174 `FiniteGroup g` by rw[ZN_invertibles_finite_group, Abbr`g`] >> 1175 `n MOD m IN g.carrier` by rw[ZN_coprime_invertible, Abbr`g`] >> 1176 `z = ordz m n` by rw[ZN_order_mod, Abbr`z`] >> 1177 `_ = order g (n MOD m)` by rw[ZN_invertibles_order, Abbr`g`] >> 1178 `Group g` by rw[finite_group_is_group] >> 1179 `(n ** k) MOD m = ((n MOD m) ** k) MOD m` by metis_tac[EXP_MOD] >> 1180 `_ = ((n MOD m) ** (k MOD z)) MOD m` by metis_tac[group_exp_mod_order, Invertibles_property, ZN_exp] >> 1181 `_ = ((n ** (k MOD z)) MOD m)` by metis_tac[EXP_MOD] >> 1182 rw[]); 1183 1184(* Theorem: 0 < m /\ coprime m n /\ (!p. prime p /\ p divides n ==> (ordz m p = 1)) ==> (ordz m n = 1) *) 1185(* Proof: 1186 If m = 1, true since ordz 1 n = 1 by ZN_order_mod_1 1187 If m <> 1, then 1 < m by 0 < m, m <> 1 1188 and 1 MOD m = 1 by ONE_MOD 1189 If n = 1, true by ZN_order_1 1190 If n <> 1, 1191 Since m <> 1, coprime m n ==> n <> 0 by GCD_0R 1192 Thus 0 < n and 1 < n by n <> 1 1193 1194 Claim: !p. prime p /\ p divides n ==> (p MOD m = 1) 1195 Proof: prime p /\ p divides n 1196 ==> coprime m n ==> coprime m p by coprime_prime_factor_coprime, GCD_SYM, 1 < m 1197 and ordz m p = 1 by implication 1198 ==> p MOD m = 1 by ZN_order_eq_1 1199 1200 Thus n MOD m = 1 by ALL_PRIME_FACTORS_MOD_EQ_1 1201 ==> ordz m p = 1 by ZN_order_eq_1 1202*) 1203val ZN_order_eq_1_by_prime_factors = store_thm( 1204 "ZN_order_eq_1_by_prime_factors", 1205 ``!m n. 0 < m /\ coprime m n /\ (!p. prime p /\ p divides n ==> (ordz m p = 1)) ==> (ordz m n = 1)``, 1206 rpt strip_tac >> 1207 Cases_on `m = 1` >- 1208 rw[ZN_order_mod_1] >> 1209 Cases_on `n = 1` >- 1210 rw[ZN_order_1] >> 1211 `n <> 0` by metis_tac[GCD_0R] >> 1212 `0 < n /\ 1 < n /\ 1 < m` by decide_tac >> 1213 `!p. prime p /\ p divides n ==> (p MOD m = 1)` by 1214 (rpt strip_tac >> 1215 `coprime m p` by metis_tac[coprime_prime_factor_coprime, GCD_SYM] >> 1216 metis_tac[ZN_order_eq_1, ONE_MOD]) >> 1217 `n MOD m = 1` by rw[ALL_PRIME_FACTORS_MOD_EQ_1] >> 1218 rw[ZN_order_eq_1]); 1219 1220(* 1221> order_eq_0 |> ISPEC ``(ZN m).prod`` |> ISPEC ``n:num``; 1222val it = |- (ordz m n = 0) <=> !n'. 0 < n' ==> (ZN m).prod.exp n n' <> (ZN m).prod.id: thm 1223*) 1224 1225(* Theorem: 1 < m ==> (ordz m n <> 0 <=> ?k. 0 < k /\ (n ** k MOD m = 1)) *) 1226(* Proof: 1227 By order_eq_0, 1228 (ordz m n = 0) <=> !k. 0 < k ==> (ZN m).prod.exp n k <> (ZN m).prod.id 1229 or (ordz m n = 0) <=> !k. 0 < k ==> n ** k MOD m <> 1 by ZN_exp, ZN_ids_alt, 0 < m, 1 < m 1230 The result follows by taking negation of both sides. 1231*) 1232val ZN_order_nonzero_iff = store_thm( 1233 "ZN_order_nonzero_iff", 1234 ``!m n. 1 < m ==> (ordz m n <> 0 <=> ?k. 0 < k /\ (n ** k MOD m = 1))``, 1235 rw[order_eq_0, ZN_exp, ZN_ids_alt]); 1236 1237(* Theorem: 1 < m ==> ((ordz m n = 0) <=> (!k. 0 < k ==> n ** k MOD m <> 1)) *) 1238(* Proof: by ZN_order_nonzero_iff *) 1239val ZN_order_eq_0_iff = store_thm( 1240 "ZN_order_eq_0_iff", 1241 ``!m n. 1 < m ==> ((ordz m n = 0) <=> (!k. 0 < k ==> n ** k MOD m <> 1))``, 1242 metis_tac[ZN_order_nonzero_iff]); 1243 1244(* Theorem: 0 < m ==> ((ordz m n <> 0) <=> coprime m n) *) 1245(* Proof: 1246 If m = 1, true since ordz 1 n = 1 <> 0 by ZN_order_mod_1 1247 and coprime 1 n by GCD_1 1248 If m <> 1, then 1 < m by 0 < m, m <> 1 1249 and 1 MOD m = 1 by ONE_MOD 1250 If part: ordz m n <> 0 ==> coprime m n 1251 Let x = n MOD m. 1252 Then ordz m n = ordz m x by ZN_order_mod, 0 < m 1253 Note Ring (ZN m) by ZN_ring, 0 < m 1254 so Monoid (ZN m).prod by ring_mult_monoid 1255 and (ZN m).prod.carrier = (ZN m).carrier by ring_carriers 1256 Note x < n by MOD_LESS, 0 < m 1257 Thus x IN (ZN m).carrier by ZN_property 1258 Now 0 < ordz m x by 0 < ordz m n = ordz m x 1259 ==> x IN (Invertibles (ZN m).prod).carrier by monoid_order_nonzero, Invertibles_carrier 1260 or x IN (Estar m).carrier by ZN_invertibles, 1 < m 1261 Hence coprime m x by Estar_element 1262 or coprime m n by coprime_mod_iff. 0 < m 1263 1264 Only-if part: coprime m n ==> ordz m n <> 0 1265 This is true by ZN_coprime_order, 0 < m 1266*) 1267val ZN_order_nonzero = store_thm( 1268 "ZN_order_nonzero", 1269 ``!m n. 0 < m ==> ((ordz m n <> 0) <=> coprime m n)``, 1270 rpt strip_tac >> 1271 Cases_on `m = 1` >- 1272 rw[ZN_order_mod_1] >> 1273 rw[EQ_IMP_THM] >| [ 1274 qabbrev_tac `x = n MOD m` >> 1275 `ordz m n = ordz m x` by rw[ZN_order_mod, Abbr`x`] >> 1276 `Monoid (ZN m).prod` by rw[ZN_ring, ring_mult_monoid] >> 1277 `(ZN m).prod.carrier = (ZN m).carrier` by rw[ZN_ring, ring_carriers] >> 1278 `x IN (ZN m).carrier` by rw[ZN_property, MOD_LESS, Abbr`x`] >> 1279 `x IN (Invertibles (ZN m).prod).carrier` by rw[monoid_order_nonzero, Invertibles_carrier] >> 1280 `x IN (Estar m).carrier` by rw[GSYM ZN_invertibles] >> 1281 `coprime m x` by metis_tac[Estar_element] >> 1282 rw[Once coprime_mod_iff], 1283 metis_tac[ZN_coprime_order, NOT_ZERO_LT_ZERO] 1284 ]); 1285 1286(* Theorem: 0 < m ==> ((ordz m n = 0) <=> ~(coprime m n)) *) 1287(* Proof: by ZN_order_nonzero *) 1288val ZN_order_eq_0 = store_thm( 1289 "ZN_order_eq_0", 1290 ``!m n. 0 < m ==> ((ordz m n = 0) <=> ~(coprime m n))``, 1291 metis_tac[ZN_order_nonzero]); 1292 1293(* Theorem: 0 < m /\ ~coprime m n ==> !k. 0 < k ==> n ** k MOD m <> 1 *) 1294(* Proof: 1295 Note m <> 1 by GCD_1 1296 and ~coprime m n ==> ordz m n = 0 by ZN_order_eq_0, 0 < m 1297 ==> !k. 0 < k ==> (n ** k) MOD m <> 1 by ZN_order_eq_0_iff, 1 < m 1298*) 1299val ZN_not_coprime = store_thm( 1300 "ZN_not_coprime", 1301 ``!m n. 0 < m /\ ~coprime m n ==> !k. 0 < k ==> n ** k MOD m <> 1``, 1302 rpt strip_tac >> 1303 `m <> 1` by metis_tac[GCD_1] >> 1304 `ordz m n = 0` by rw[ZN_order_eq_0] >> 1305 `1 < m` by decide_tac >> 1306 metis_tac[ZN_order_eq_0_iff]); 1307 1308(* Note: "Since ord k n > 1, there must exist a prime divisor p of n such that ord k p > 1." *) 1309 1310(* Theorem: 0 < m /\ 1 < ordz m n ==> ?p. prime p /\ p divides n /\ 1 < ordz m p *) 1311(* Proof: 1312 By contradiction, suppose !p. prime p /\ p divides n /\ ~(1 < ordz m p). 1313 Note ordz m n <> 0 by 1 < ordz m n 1314 Thus coprime m n by ZN_order_eq_0, 0 < m 1315 Note ordz m n <> 1 by 1 < ordz m n 1316 so m <> 1 by ZN_order_mod_1 1317 Now n <> 0 by GCD_0R, m <> 1 1318 and n <> 1 by ZN_order_1, ordz m n <> 1 1319 ==> 1 < n 1320 Note coprime m n by above 1321 ==> !p. prime p /\ p divides n 1322 ==> coprime m p by coprime_prime_factor_coprime, GCD_SYM, 1 < n 1323 ==> 0 < ordz m p by ZN_coprime_order, 0 < m 1324 ==> (ordz m p = 1) by ~(1 < ordz m p), NOT_LT_ONE, NOT_ZERO_LT_ZERO 1325 Thus ordz m n = 1 by ZN_order_eq_1_by_prime_factors 1326 This contradicts 1 < ordz m n in the premise. 1327*) 1328val ZN_order_gt_1_property = store_thm( 1329 "ZN_order_gt_1_property", 1330 ``!m n. 0 < m /\ 1 < ordz m n ==> ?p. prime p /\ p divides n /\ 1 < ordz m p``, 1331 spose_not_then strip_assume_tac >> 1332 `ordz m n <> 0 /\ ordz m n <> 1` by decide_tac >> 1333 `coprime m n` by metis_tac[ZN_order_eq_0] >> 1334 `m <> 1` by metis_tac[ZN_order_mod_1] >> 1335 `n <> 0` by metis_tac[GCD_0R] >> 1336 `n <> 1` by metis_tac[ZN_order_1] >> 1337 `1 < n` by decide_tac >> 1338 `!p. prime p /\ p divides n ==> (ordz m p = 1)` by 1339 (rpt strip_tac >> 1340 `coprime m p` by metis_tac[coprime_prime_factor_coprime, GCD_SYM] >> 1341 `0 < ordz m p` by metis_tac[ZN_coprime_order] >> 1342 metis_tac[NOT_LT_ONE, NOT_ZERO_LT_ZERO]) >> 1343 metis_tac[ZN_order_eq_1_by_prime_factors]); 1344 1345(* A better proof of the same theorem. *) 1346 1347(* Theorem: 0 < m /\ 1 < ordz m n ==> ?p. prime p /\ p divides n /\ 1 < ordz m p *) 1348(* Proof: 1349 By contradiction, suppose !p. prime p /\ p divides n /\ ~(1 < ordz m p). 1350 Note ordz m n <> 0 by 1 < ordz m n 1351 ==> coprime m n by ZN_order_eq_0, 0 < m 1352 ==> ?p. prime p /\ p divides n /\ (ordz m p <> 1) 1353 by ZN_order_eq_1_by_prime_factors, ordz m n <> 1 1354 Thus ordz m p = 0 by ~(1 < x) <=> (x = 0) \/ (x = 1) 1355 ==> p divides m by ZN_order_eq_0, PRIME_GCD, coprime_sym 1356 ==> p divides 1 by GCD_PROPERTY, coprime m n 1357 ==> p = 1 by DIVIDES_ONE 1358 ==> F by NOT_PRIME_1 1359*) 1360val ZN_order_gt_1_property = store_thm( 1361 "ZN_order_gt_1_property", 1362 ``!m n. 0 < m /\ 1 < ordz m n ==> ?p. prime p /\ p divides n /\ 1 < ordz m p``, 1363 spose_not_then strip_assume_tac >> 1364 `coprime m n` by metis_tac[ZN_order_eq_0, DECIDE``1 < x ==> x <> 0``] >> 1365 `?p. prime p /\ p divides n /\ (ordz m p <> 1)` by metis_tac[ZN_order_eq_1_by_prime_factors, LESS_NOT_EQ] >> 1366 `ordz m p = 0` by metis_tac[DECIDE``~(1 < x) <=> (x = 0) \/ (x = 1)``] >> 1367 `p divides m` by metis_tac[ZN_order_eq_0, PRIME_GCD, coprime_sym] >> 1368 `p divides 1` by metis_tac[GCD_PROPERTY] >> 1369 metis_tac[DIVIDES_ONE, NOT_PRIME_1]); 1370 1371(* 1372> group_order_divides_exp |> ISPEC ``Invertibles (ZN m).prod``; 1373val it = |- Group (Invertibles (ZN m).prod) ==> 1374 !x. x IN (Invertibles (ZN m).prod).carrier ==> 1375 !n. ((Invertibles (ZN m).prod).exp x n = (Invertibles (ZN m).prod).id) <=> 1376 order (Invertibles (ZN m).prod) x divides n: thm 1377*) 1378 1379(* Theorem: 1 < m /\ 0 < k ==> ((n ** k MOD m = 1) <=> (ordz m n) divides k) *) 1380(* Proof: 1381 Let g = Invertibles (ZN m).prod. 1382 Note g = Estar m by ZN_invertibles 1383 Thus FiniteGroup g by Estar_finite_group 1384 and Group g by finite_group_is_group 1385 Let x = n MOD m. 1386 Then x < m by MOD_LESS, 0 < m 1387 1388 If part: n ** k MOD m = 1 ==> (ordz m n) divides k 1389 Note x ** n MOD m = 1 by given 1390 ==> ordz m n <> 0 by ZN_order_nonzero_iff, 1 < m 1391 ==> coprime m n by ZN_order_eq_0, 1 < m 1392 ==> coprime m x by coprime_mod_iff, 0 < m 1393 Now 0 < x by GCD_0, coprime m x, 1 < m 1394 Thus x IN g.carrier by Estar_element, 0 < x, x < m, coprime m x 1395 Note x ** k MOD m = 1 by EXP_MOD, n ** k MOD m = 1 1396 or (Invertibles (ZN m).prod).exp x n = (Invertibles (ZN m).prod).id by Estar_exp, Estar_property 1397 ==> order (Invertibles (ZN m).prod) x divides k by group_order_divides_exp 1398 or ordz m n divides k by ZN_invertibles_order 1399 1400 Only-if part: (ordz m n) divides k ==> n ** k MOD m = 1 1401 Note (ordz m n) divides k by given 1402 ==> ordz m n <> 0 by ZERO_DIVIDES, 0 < k 1403 ==> coprime m n by ZN_order_eq_0, 1 < m 1404 ==> coprime m x by coprime_mod_iff, 0 < m 1405 Now 0 < x by GCD_0, coprime m x, 1 < m 1406 Thus x IN g.carrier by Estar_element, 0 < x, x < m, coprime m x 1407 Note ordz m x = ordz m n by ZN_order_mod, 1 < m 1408 or order (Invertibles (ZN n).prod) x divides k by ZN_invertibles_order, coprime m n 1409 ==> (Invertibles (ZN n).prod).exp x k = (Invertibles (ZN n).prod).id) by group_order_divides_exp 1410 or x ** k MOD m = 1 by Estar_exp, Estar_property 1411 or n ** k MOD m = 1 by EXP_MOD, 0 < m 1412*) 1413val ZN_order_divides_exp = store_thm( 1414 "ZN_order_divides_exp", 1415 ``!m n k. 1 < m /\ 0 < k ==> ((n ** k MOD m = 1) <=> (ordz m n) divides k)``, 1416 rpt strip_tac >> 1417 `0 < m` by decide_tac >> 1418 qabbrev_tac `g = Invertibles (ZN m).prod` >> 1419 `g = Estar m` by rw[ZN_invertibles, Abbr`g`] >> 1420 `FiniteGroup g` by rw[Estar_finite_group] >> 1421 `Group g` by rw[finite_group_is_group] >> 1422 qabbrev_tac `x = n MOD m` >> 1423 `x < m` by rw[Abbr`x`] >> 1424 rewrite_tac[EQ_IMP_THM] >> 1425 rpt strip_tac >| [ 1426 `ordz m n <> 0` by metis_tac[ZN_order_nonzero_iff] >> 1427 `coprime m n` by metis_tac[ZN_order_eq_0] >> 1428 `coprime m x` by rw[GSYM coprime_mod_iff, Abbr`x`] >> 1429 `0 < x` by metis_tac[GCD_0, NOT_ZERO_LT_ZERO, DECIDE``1 < n ==> n <> 1``] >> 1430 `x IN g.carrier` by rw[Estar_element] >> 1431 `x ** k MOD m = 1` by rw[EXP_MOD, Abbr`x`] >> 1432 `order (Invertibles (ZN m).prod) x divides k` by rw[GSYM group_order_divides_exp, Estar_exp, Estar_property] >> 1433 metis_tac[ZN_invertibles_order], 1434 `ordz m n <> 0` by metis_tac[ZERO_DIVIDES, NOT_ZERO_LT_ZERO] >> 1435 `coprime m n` by metis_tac[ZN_order_eq_0] >> 1436 `coprime m x` by rw[GSYM coprime_mod_iff, Abbr`x`] >> 1437 `0 < x` by metis_tac[GCD_0, NOT_ZERO_LT_ZERO, DECIDE``1 < n ==> n <> 1``] >> 1438 `x IN g.carrier` by rw[Estar_element] >> 1439 `ordz m x = ordz m n` by rw[ZN_order_mod, Abbr`x`] >> 1440 `x ** k MOD m = 1` by metis_tac[group_order_divides_exp, ZN_invertibles_order, Estar_exp, Estar_property] >> 1441 rw[GSYM EXP_MOD, Abbr`x`] 1442 ]); 1443 1444(* Theorem: 0 < m /\ 0 < ordz m n ==> (ordz m n) divides (phi m) *) 1445(* Proof: 1446 Note 0 < ordz m n ==> coprime m n by ZN_order_nonzero, 0 < m 1447 Thus (ordz m n) divides (phi m) by ZN_coprime_order_divides_phi, 0 < m 1448*) 1449val ZN_order_divides_phi = store_thm( 1450 "ZN_order_divides_phi", 1451 ``!m n. 0 < m /\ 0 < ordz m n ==> (ordz m n) divides (phi m)``, 1452 rpt strip_tac >> 1453 `coprime m n` by metis_tac[ZN_order_nonzero, NOT_ZERO_LT_ZERO] >> 1454 rw[ZN_coprime_order_divides_phi]); 1455 1456(* Theorem: 0 < m ==> ordz m n <= phi m *) 1457(* Proof: 1458 If ordz m n = 0, then trivially true. 1459 Otherwise, 0 < ordz m n. 1460 Note ordz m n divides phi m by ZN_order_divides_phi, 0 < m /\ 0 < ordz m n 1461 and 0 < phi m by phi_pos, 0 < m 1462 so ordz m n <= phi m by DIVIDES_LE, 0 < phi m 1463*) 1464val ZN_order_upper = store_thm( 1465 "ZN_order_upper", 1466 ``!m n. 0 < m ==> ordz m n <= phi m``, 1467 rpt strip_tac >> 1468 Cases_on `ordz m n = 0` >- 1469 rw[] >> 1470 `ordz m n divides phi m` by rw[ZN_order_divides_phi] >> 1471 `0 < phi m` by rw[phi_pos] >> 1472 rw[DIVIDES_LE]); 1473 1474(* Theorem: 0 < m ==> ordz m n <= m *) 1475(* Proof: 1476 Note ordz m n <= phi m by ZN_order_upper, 0 < m 1477 Also phi m <= m by phi_le 1478 Thus ordz m n <= m by LESS_EQ_TRANS 1479*) 1480val ZN_order_le = store_thm( 1481 "ZN_order_le", 1482 ``!m n. 0 < m ==> ordz m n <= m``, 1483 rpt strip_tac >> 1484 `ordz m n <= phi m` by rw[ZN_order_upper] >> 1485 `phi m <= m` by rw[phi_le] >> 1486 decide_tac); 1487 1488(* Theorem: 0 < k /\ k < m ==> ordz k n < m *) 1489(* Proof: 1490 Note ordz k n <= k by ZN_order_le, 0 < k 1491 and k < m by given 1492 Thus ordz k n < m by LESS_EQ_LESS_TRANS 1493*) 1494val ZN_order_lt = store_thm( 1495 "ZN_order_lt", 1496 ``!k n m. 0 < k /\ k < m ==> ordz k n < m``, 1497 rpt strip_tac >> 1498 `ordz k n <= k` by rw[ZN_order_le] >> 1499 decide_tac); 1500(* Therefore, in the search for k such that m <= ordz k n, start with k = m *) 1501 1502(* 1503val ZN_order_minimal = 1504 order_minimal |> ISPEC ``(ZN n).prod`` |> ADD_ASSUM ``1 < n`` |> DISCH_ALL 1505 |> SIMP_RULE (srw_ss() ++ numSimps.ARITH_ss) [ZN_property, ZN_exp]; 1506 1507val ZN_order_minimal = |- 1 < n ==> !x n'. 0 < n' /\ n' < ordz n x ==> x ** n' MOD n <> 1: thm 1508*) 1509 1510(* Theorem: 0 < m /\ 0 < k /\ k < ordz m n ==> n ** k MOD m <> 1 *) 1511(* Proof: 1512 Note (ZN m).prod.exp n k <> (ZN m).prod.id by order_minimal, 0 < k, k < ordz m n 1513 But (ZN m).prod.exp n k = n ** k MOD n by ZN_exp, 0 < m 1514 and m <> 1 since !k. 0 < k /\ k < 1 = F by ZN_order_mod_1, 0 < m 1515 so (ZN m).prod.id = 1 by ZN_property, m <> 1 1516 Thus n ** k MOD m <> 1 by above 1517*) 1518val ZN_order_minimal = store_thm( 1519 "ZN_order_minimal", 1520 ``!m n k. 0 < m /\ 0 < k /\ k < ordz m n ==> n ** k MOD m <> 1``, 1521 metis_tac[order_minimal, ZN_order_mod_1, ZN_property, ZN_exp, DECIDE``(0 < k /\ k < 1) = F``]); 1522 1523(* Theorem: 1 < m /\ 1 < n MOD m /\ coprime m n ==> 1 < ordz m n *) 1524(* Proof: 1525 Let x = n MOD m. 1526 Then ordz m x = ordz m n by ZN_order_mod, 0 < m 1527 and ordz m n <> 0 by ZN_order_nonzero, coprime m n 1528 and ordz m n <> 1 by ZN_order_eq_1_alt, 1 < m 1529 Thus ordz 1 < ordz m n by arithmetic 1530*) 1531val ZN_coprime_order_gt_1 = store_thm( 1532 "ZN_coprime_order_gt_1", 1533 ``!m n. 1 < m /\ 1 < n MOD m /\ coprime m n ==> 1 < ordz m n``, 1534 rpt strip_tac >> 1535 qabbrev_tac `x = n MOD m` >> 1536 `ordz m x = ordz m n` by rw[ZN_order_mod, Abbr`x`] >> 1537 `ordz m n <> 0` by rw[ZN_order_nonzero] >> 1538 `ordz m n <> 1` by rw[ZN_order_eq_1_alt, Abbr`x`] >> 1539 decide_tac); 1540 1541(* Note: 1 < n MOD m cannot be replaced by 1 < n. A counterexample: 1542 1 < m /\ 1 < n /\ coprime m n ==> 1 < ordz m n 1543 1 < 7 /\ 1 < 43 /\ coprime 7 43, but ordz 7 43 = ordz 7 (43 MOD 7) = ordz 7 1 = 1. 1544*) 1545 1546(* Theorem: 1 < n /\ coprime m n /\ 1 < ordz m n ==> 1 < m *) 1547(* Proof: 1548 Note m <> 0 by GCD_0, 1 < n 1549 and m <> 1 by ZN_order_mod_1, 1 < ordz m n 1550 Thus 1 < m 1551*) 1552val ZN_order_with_coprime_1 = store_thm( 1553 "ZN_order_with_coprime_1", 1554 ``!m n. 1 < n /\ coprime m n /\ 1 < ordz m n ==> 1 < m``, 1555 rpt strip_tac >> 1556 `m <> 0` by metis_tac[GCD_0, LESS_NOT_EQ] >> 1557 `m <> 1` by metis_tac[ZN_order_mod_1, LESS_NOT_EQ] >> 1558 decide_tac); 1559 1560(* Theorem: 1 < m /\ m divides n /\ 1 < ordz k m /\ coprime k n ==> 1 < n /\ 1 < k *) 1561(* Proof: 1562 Note k <> 1 by ZN_order_mod_1, 1 < ordz k m, 1 < m 1563 and n <> 1 by DIVIDES_ONE, m divides n, 1 < m 1564 also k <> 0 /\ n <> 0 by coprime_0L, coprime_0R 1565 so 1 < n /\ 1 < k by both not 0, not 1. 1566*) 1567val ZN_order_with_coprime_2 = store_thm( 1568 "ZN_order_with_coprime_2", 1569 ``!m n k. 1 < m /\ m divides n /\ 1 < ordz k m /\ coprime k n ==> 1 < n /\ 1 < k``, 1570 ntac 4 strip_tac >> 1571 `k <> 1` by metis_tac[ZN_order_mod_1, LESS_NOT_EQ] >> 1572 `n <> 1` by metis_tac[DIVIDES_ONE, LESS_NOT_EQ] >> 1573 `k <> 0 /\ n <> 0` by metis_tac[coprime_0L, coprime_0R] >> 1574 decide_tac); 1575 1576(* Theorem: 1 < m ==> ((ordz m n = 0) <=> (!j. 0 < j /\ j < m ==> n ** j MOD m <> 1)) *) 1577(* Proof: 1578 If part: ordz m n = 0 ==> !j. 0 < j /\ j < m ==> n ** j MOD m <> 1 1579 Note !j. 0 < j ==> n ** j MOD m <> 1 by ZN_order_eq_0_iff 1580 Thus n ** j MOD m <> 1 by just 0 < j 1581 Only-of part: !j. 0 < j /\ j < m ==> n ** j MOD m <> 1 ==> ordz m n = 0 1582 By contradiction, suppose ordz m n <> 0. 1583 Then coprime m n by ZN_order_eq_0 1584 Let k = ord z m. 1585 Then k < m by ZN_order_lt, 0 < m, coprime m n 1586 and n ** k MOD m = 1 by ZN_order_property_alt, 1 < m 1587 This contradicts n ** k MOD m <> 1 by implication 1588*) 1589val ZN_order_eq_0_test = store_thm( 1590 "ZN_order_eq_0_test", 1591 ``!m n. 1 < m ==> ((ordz m n = 0) <=> (!j. 0 < j /\ j < m ==> n ** j MOD m <> 1))``, 1592 rw[EQ_IMP_THM] >- 1593 metis_tac[ZN_order_eq_0_iff] >> 1594 spose_not_then strip_assume_tac >> 1595 `0 < ordz m n /\ 0 < m` by decide_tac >> 1596 `coprime m n` by metis_tac[ZN_order_eq_0] >> 1597 `ordz m n < m` by rw[ZN_coprime_order_lt] >> 1598 metis_tac[ZN_order_property_alt]); 1599 1600(* Theorem: 1 < n /\ 0 < j /\ 1 < k ==> 1601 (k divides (n ** j - 1) <=> (ordz k n) divides j) *) 1602(* Proof: 1603 Note 1 < n ** j by ONE_LT_EXP, 1 < n, 0 < j 1604 k divides (n ** j - 1) 1605 <=> (n ** j - 1) MOD k = 0 by DIVIDES_MOD_0, 0 < k 1606 <=> n ** j MOD k = 1 MOD k by MOD_EQ, 1 < n ** j, 0 < k 1607 = 1 by ONE_MOD, 1 < k 1608 <=> (ordz k n) divides j by ZN_order_divides_exp, 0 < j, 1 < k 1609*) 1610val ZN_order_divides_tops_index = store_thm( 1611 "ZN_order_divides_tops_index", 1612 ``!n j k. 1 < n /\ 0 < j /\ 1 < k ==> 1613 (k divides (n ** j - 1) <=> (ordz k n) divides j)``, 1614 rpt strip_tac >> 1615 `1 < n ** j` by rw[ONE_LT_EXP] >> 1616 `k divides (n ** j - 1) <=> ((n ** j - 1) MOD k = 0)` by rw[DIVIDES_MOD_0] >> 1617 `_ = (n ** j MOD k = 1 MOD k)` by rw[MOD_EQ] >> 1618 `_ = (n ** j MOD k = 1)` by rw[ONE_MOD] >> 1619 `_ = (ordz k n) divides j` by rw[ZN_order_divides_exp] >> 1620 metis_tac[]); 1621 1622(* Theorem: 1 < n /\ 0 < j /\ 1 < k /\ k divides (n ** j - 1) ==> (ordz k n) <= j *) 1623(* Proof: 1624 Note (ordz k n) divides j by ZN_order_divides_tops_index 1625 Thus (ordz k n) <= j by DIVIDES_LE, 0 < j 1626*) 1627val ZN_order_le_tops_index = store_thm( 1628 "ZN_order_le_tops_index", 1629 ``!n j k. 1 < n /\ 0 < j /\ 1 < k /\ k divides (n ** j - 1) ==> (ordz k n) <= j``, 1630 rw[GSYM ZN_order_divides_tops_index, DIVIDES_LE]); 1631 1632(* ------------------------------------------------------------------------- *) 1633(* ZN Order Test *) 1634(* ------------------------------------------------------------------------- *) 1635 1636(* Theorem: 1 < m /\ 0 < k /\ (n ** k MOD m = 1) /\ 1637 (!j. 0 < j /\ j < k /\ j divides phi m ==> n ** j MOD m <> 1) ==> 1638 !j. 0 < j /\ j < k /\ ~(j divides phi m) ==> (ordz m n = k) \/ n ** j MOD m <> 1 *) 1639(* Proof: 1640 By contradiction, suppose (ordz m n <> k) /\ (n ** j MOD m = 1). 1641 Let z = ordz m n. 1642 Then z divides j /\ z divides k by ZN_order_divides_exp 1643 so z <= k by DIVIDES_LE, 0 < k 1644 or z < k by z <> k (from contradiction assumption) 1645 Also 0 < z by ZERO_DIVIDES, z divides j, 0 < j 1646 and z divides (phi m) by ZN_order_divides_phi, 0 < z 1647 Put j = z in implication gives: n ** z MOD m <> 1 1648 This contradicts n ** z MOD m = 1 by ZN_order_property_alt, 1 < m 1649*) 1650val ZN_order_test_propery = store_thm( 1651 "ZN_order_test_propery", 1652 ``!m n k. 1 < m /\ 0 < k /\ (n ** k MOD m = 1) /\ 1653 (!j. 0 < j /\ j < k /\ j divides phi m ==> n ** j MOD m <> 1) ==> 1654 !j. 0 < j /\ j < k /\ ~(j divides phi m) ==> (ordz m n = k) \/ n ** j MOD m <> 1``, 1655 rpt strip_tac >> 1656 spose_not_then strip_assume_tac >> 1657 qabbrev_tac `z = ordz m n` >> 1658 `z divides j /\ z divides k` by rw[GSYM ZN_order_divides_exp, Abbr`z`] >> 1659 `z <= k` by rw[DIVIDES_LE] >> 1660 `z < k` by decide_tac >> 1661 `0 < z` by metis_tac[ZERO_DIVIDES, NOT_ZERO_LT_ZERO] >> 1662 `z divides (phi m)` by rw[ZN_order_divides_phi, Abbr`z`] >> 1663 metis_tac[ZN_order_property_alt]); 1664 1665(* 1666> order_thm |> GEN_ALL |> ISPEC ``(ZN m).prod`` |> ISPEC ``n:num`` |> ISPEC ``k:num``; 1667val it = |- 0 < k ==> ((ordz m n = k) <=> 1668 ((ZN m).prod.exp n k = (ZN m).prod.id) /\ 1669 !m'. 0 < m' /\ m' < k ==> (ZN m).prod.exp n m' <> (ZN m).prod.id): thm 1670*) 1671 1672(* Theorem: 1 < m /\ 0 < k ==> 1673 ((ordz m n = k) <=> ((n ** k) MOD m = 1) /\ !j. 0 < j /\ j < k ==> (n ** j) MOD m <> 1) *) 1674(* Proof: 1675 By order_thm, 0 < k ==> 1676 ((ordz m n = k) <=> ((ZN m).prod.exp n k = (ZN m).prod.id) /\ 1677 !j. 0 < j /\ j < k ==> (ZN m).prod.exp n j <> (ZN m).prod.id) 1678 Now (ZN m).prod.exp n k = (n ** k) MOD m by ZN_exp, 0 < m 1679 and (ZN m).prod.id = 1 by ZN_property, m <> 1 1680 Thus the result follows. 1681*) 1682val ZN_order_test_1 = store_thm( 1683 "ZN_order_test_1", 1684 ``!m n k. 1 < m /\ 0 < k ==> 1685 ((ordz m n = k) <=> ((n ** k) MOD m = 1) /\ !j. 0 < j /\ j < k ==> (n ** j) MOD m <> 1)``, 1686 metis_tac[order_thm, ZN_exp, ZN_ids_alt, DECIDE``1 < m ==> 0 < m``]); 1687 1688(* Theorem: 1 < m /\ 0 < k ==> ((ordz m n = k) <=> 1689 (n ** k MOD m = 1) /\ !j. 0 < j /\ j < k /\ j divides (phi m) ==> n ** j MOD m <> 1) *) 1690(* Proof: 1691 If part: ordz m n = k ==> (n ** k MOD m = 1) /\ !j. 0 < j /\ j < k /\ j divides (phi m) ==> n ** j MOD m <> 1) 1692 This is to show: 1693 (1) n ** (ordz m n) MOD m = 1, true by ZN_order_property, 1 < m. 1694 (2) !j. 0 < j /\ j < (ordz m n) /\ j divides (phi m) ==> n ** j MOD m <> 1) 1695 This is true by ZN_order_minimal, 1 < m. 1696 Only-if part: (n ** k MOD m = 1) /\ 1697 !j. 0 < j /\ j < k /\ j divides (phi m) ==> n ** j MOD m <> 1) ==> ordz m n = k 1698 Note the conditions give: 1699 !j. 0 < j /\ j < k /\ ~(j divides phi m) 1700 ==> (ordz m n = k) \/ n ** j MOD m <> 1 by ZN_order_test_propery 1701 Combining both implications, 1702 !j. 0 < j /\ j < k ==> n ** j MOD m <> 1 1703 Thus ordz m n = k by ZN_order_test_1 1704*) 1705val ZN_order_test_2 = store_thm( 1706 "ZN_order_test_2", 1707 ``!m n k. 1 < m /\ 0 < k ==> 1708 ((ordz m n = k) <=> 1709 (n ** k MOD m = 1) /\ !j. 0 < j /\ j < k /\ j divides (phi m) ==> n ** j MOD m <> 1)``, 1710 rw[EQ_IMP_THM] >- 1711 rw[ZN_order_property] >- 1712 rw[ZN_order_minimal] >> 1713 `!j. 0 < j /\ j < k /\ ~(j divides phi m) ==> 1714 (ordz m n = k) \/ n ** j MOD m <> 1` by rw[ZN_order_test_propery] >> 1715 metis_tac[ZN_order_test_1]); 1716 1717(* Theorem: 1 < m /\ 0 < k ==> ((ordz m n = k) <=> 1718 (k divides phi m) /\ (n ** k MOD m = 1) /\ !j. 0 < j /\ j < k /\ j divides (phi m) ==> n ** j MOD m <> 1) *) 1719(* Proof: 1720 If part: ordz m n = k ==> (k divides phi m) /\ 1721 (n ** k MOD m = 1) /\ !j. 0 < j /\ j < k /\ j divides (phi m) ==> n ** j MOD m <> 1) 1722 This is to show: 1723 (1) (ordz m n) divides phi m, true by ZN_order_divides_phi, 1 < m. 1724 (2) n ** (ordz m n) MOD m = 1, true by ZN_order_property, 1 < m. 1725 (3) !j. 0 < j /\ j < (ordz m n) /\ j divides (phi m) ==> n ** j MOD m <> 1) 1726 This is true by ZN_order_minimal, 1 < m. 1727 Only-if part: (k divides phi m) /\ (n ** k MOD m = 1) /\ 1728 !j. 0 < j /\ j < k /\ j divides (phi m) ==> n ** j MOD m <> 1) ==> ordz m n = k 1729 Note the conditions give: 1730 !j. 0 < j /\ j < k /\ ~(j divides phi m) 1731 ==> (ordz m n = k) \/ n ** j MOD m <> 1 by ZN_order_test_propery 1732 Combining both implications, 1733 !j. 0 < j /\ j < k ==> n ** j MOD m <> 1 1734 Thus ordz m n = k by ZN_order_test_1 1735*) 1736val ZN_order_test_3 = store_thm( 1737 "ZN_order_test_3", 1738 ``!m n k. 1 < m /\ 0 < k ==> 1739 ((ordz m n = k) <=> 1740 (k divides phi m) /\ (n ** k MOD m = 1) /\ !j. 0 < j /\ j < k /\ j divides (phi m) ==> n ** j MOD m <> 1)``, 1741 rw[EQ_IMP_THM] >- 1742 rw[ZN_order_divides_phi] >- 1743 rw[ZN_order_property] >- 1744 rw[ZN_order_minimal] >> 1745 `!j. 0 < j /\ j < k /\ ~(j divides phi m) ==> 1746 (ordz m n = k) \/ n ** j MOD m <> 1` by rw[ZN_order_test_propery] >> 1747 metis_tac[ZN_order_test_1]); 1748 1749(* Theorem: 1 < m ==> (ordz m n = k <=> n ** k MOD m = 1 /\ 1750 !j. 0 < j /\ j < (if k = 0 then m else k) ==> n ** j MOD m <> 1) *) 1751(* Proof: 1752 If k = 0, 1753 Note n ** 0 MOD m 1754 = 1 MOD m by EXP_0 1755 = 1 by ONE_MOD, 1 < m 1756 The result follows by ZN_order_eq_0_test 1757 If k <> 0, the result follows by ZN_order_test_1 1758*) 1759val ZN_order_test_4 = store_thm( 1760 "ZN_order_test_4", 1761 ``!m n k. 1 < m ==> ((ordz m n = k) <=> ((n ** k MOD m = 1) /\ 1762 !j. 0 < j /\ j < (if k = 0 then m else k) ==> n ** j MOD m <> 1))``, 1763 rpt strip_tac >> 1764 (Cases_on `k = 0` >> simp[]) >| [ 1765 `n ** 0 MOD m = 1` by rw[EXP_0] >> 1766 metis_tac[ZN_order_eq_0_test], 1767 rw[ZN_order_test_1] 1768 ]); 1769 1770(* ------------------------------------------------------------------------- *) 1771(* ZN Homomorphism *) 1772(* ------------------------------------------------------------------------- *) 1773 1774(* Theorem: 0 < m /\ x IN (ZN n).carrier ==> x MOD m IN (ZN m).carrier *) 1775(* Proof: 1776 Expand by definitions, this is to show: 1777 x < n ==> x MOD m < m, true by MOD_LESS. 1778*) 1779val ZN_to_ZN_element = store_thm( 1780 "ZN_to_ZN_element", 1781 ``!n m x. 0 < m /\ x IN (ZN n).carrier ==> x MOD m IN (ZN m).carrier``, 1782 rw[ZN_def]); 1783 1784(* Theorem: 0 < n /\ m divides n ==> GroupHomo (\x. x MOD m) (ZN n).sum (ZN m).sum *) 1785(* Proof: 1786 Note 0 < m by ZERO_DIVIDES, 0 < n 1787 Expand by definitions, this is to show: 1788 x < n /\ x' < n ==> (x + x') MOD n MOD m = (x MOD m + x' MOD m) MOD m 1789 (x + x') MOD n MOD m 1790 = (x + x') MOD m by DIVIDES_MOD_MOD, 0 < n 1791 = (x MOD m + x' MOD m) MOD m by MOD_PLUS, 0 < m 1792*) 1793val ZN_to_ZN_sum_group_homo = store_thm( 1794 "ZN_to_ZN_sum_group_homo", 1795 ``!n m. 0 < n /\ m divides n ==> GroupHomo (\x. x MOD m) (ZN n).sum (ZN m).sum``, 1796 rpt strip_tac >> 1797 `0 < m` by metis_tac[ZERO_DIVIDES, NOT_ZERO] >> 1798 rw[ZN_def, GroupHomo_def, DIVIDES_MOD_MOD, MOD_PLUS]); 1799 1800(* Theorem: 0 < n /\ m divides n ==> MonoidHomo (\x. x MOD m) (ZN n).prod (ZN m).prod *) 1801(* Proof: 1802 Note 0 < m by ZERO_DIVIDES, 0 < n 1803 Expand by definitions, this is to show: 1804 (1) x < n /\ x' < n ==> (x * x') MOD n MOD m = (x MOD m * x' MOD m) MOD m 1805 (x * x') MOD n MOD m 1806 = (x * x') MOD m by DIVIDES_MOD_MOD, 0 < n 1807 = (x MOD m * x' MOD m) MOD m by MOD_TIMES2, 0 < m 1808 (2) 0 < m /\ m <> 1 ==> 1 < m, trivially true. 1809*) 1810val ZN_to_ZN_prod_monoid_homo = store_thm( 1811 "ZN_to_ZN_prod_monoid_homo", 1812 ``!n m. 0 < n /\ m divides n ==> MonoidHomo (\x. x MOD m) (ZN n).prod (ZN m).prod``, 1813 rpt strip_tac >> 1814 `0 < m` by metis_tac[ZERO_DIVIDES, NOT_ZERO] >> 1815 rw[ZN_def, MonoidHomo_def, times_mod_def, DIVIDES_MOD_MOD] >> 1816 fs[DIVIDES_ONE]); 1817 1818(* Theorem: 0 < n /\ m divides n ==> RingHomo (\x. x MOD m) (ZN n) (ZN m) *) 1819(* Proof: 1820 By RingHomo_def, this is to show: 1821 (1) x IN (ZN n).carrier ==> x MOD m IN (ZN m).carrier 1822 Note 0 < m by ZERO_DIVIDES, 0 < n 1823 Hence true by ZN_to_ZN_element, 0 < m. 1824 (2) GroupHomo (\x. x MOD m) (ZN n).sum (ZN m).sum, true by ZN_to_ZN_sum_group_homo. 1825 (3) MonoidHomo (\x. x MOD m) (ZN n).prod (ZN m).prod, true by ZN_to_ZN_prod_monoid_homo. 1826*) 1827val ZN_to_ZN_ring_homo = store_thm( 1828 "ZN_to_ZN_ring_homo", 1829 ``!n m. 0 < n /\ m divides n ==> RingHomo (\x. x MOD m) (ZN n) (ZN m)``, 1830 rw[RingHomo_def] >- 1831 metis_tac[ZN_to_ZN_element, ZERO_DIVIDES, NOT_ZERO] >- 1832 rw[ZN_to_ZN_sum_group_homo] >> 1833 rw[ZN_to_ZN_prod_monoid_homo]); 1834 1835(* ------------------------------------------------------------------------- *) 1836(* A Ring from Sets. *) 1837(* ------------------------------------------------------------------------- *) 1838 1839(* The Ring from Group (symdiff_set) and Monoid (set_inter). *) 1840val symdiff_set_inter_def = Define` 1841 symdiff_set_inter = <| carrier := UNIV; 1842 sum := symdiff_set; 1843 prod := set_inter |> 1844`; 1845(* Evaluation is given later in symdiff_eval. *) 1846 1847(* Theorem: symdiff_set_inter is a Ring. *) 1848(* Proof: check definitions. 1849 For the distribution law: 1850 x INTER (y SYM z) = (x INTER y) SYM (x INTER z) 1851 first verify by Venn Diagram. 1852*) 1853val symdiff_set_inter_ring = store_thm( 1854 "symdiff_set_inter_ring", 1855 ``Ring symdiff_set_inter``, 1856 rw_tac std_ss[Ring_def, symdiff_set_inter_def] >- 1857 rw[symdiff_set_abelian_group] >- 1858 rw[set_inter_abelian_monoid] >- 1859 rw[symdiff_set_def] >- 1860 rw[set_inter_def] >> 1861 rw[symdiff_set_def, set_inter_def, symdiff_def, EXTENSION] >> 1862 metis_tac[]); 1863(* Michael's proof *) 1864val symdiff_set_inter_ring = store_thm( 1865 "symdiff_set_inter_ring", 1866 ``Ring symdiff_set_inter``, 1867 rw_tac std_ss[Ring_def, symdiff_set_inter_def] >> 1868 rw[symdiff_set_def, set_inter_def] >> 1869 rw[EXTENSION, symdiff_def] >> 1870 metis_tac[]); 1871 1872(* Theorem: symdiff UNIV UNIV = EMPTY` *) 1873(* Proof: by definition. *) 1874val symdiff_univ_univ_eq_empty = store_thm( 1875 "symdiff_univ_univ_eq_empty", 1876 ``symdiff UNIV UNIV = EMPTY``, 1877 rw[symdiff_def]); 1878 1879(* Note: symdiff_set_inter has carrier infinite, but characteristics 2. *) 1880 1881(* Theorem: char symdiff_set_inter = 2 *) 1882(* Proof: 1883 By definition, and making use of FUNPOW_2. 1884 First to show: 1885 ?n. 0 < n /\ (FUNPOW (symdiff univ(:'a)) n {} = {}) 1886 Put n = 2, and apply FUNPOW_2 and symdiff_def. 1887 Second to show: 1888 0 < n /\ FUNPOW (symdiff univ(:'a)) n {} = {} /\ 1889 !m. m < n ==> ~(0 < m) \/ FUNPOW (symdiff univ(:'a)) m {} <> {} ==> n = 2 1890 By contradiction. Assume n <> 2, then n < 2 or 2 < n. 1891 If n < 2, then 0 < n < 2 means n = 1, 1892 but FUNPOW (symdiff univ(:'a)) 1 {} = symdiff univ(:'a) {} = univ(:'a) <> {}, a contradiction. 1893 If 2 < n, then FUNPOW (symdiff univ(:'a)) 2 {} <> {}, contradicting FUNPOW_2 and symdiff_def. 1894*) 1895val symdiff_set_inter_char = store_thm( 1896 "symdiff_set_inter_char", 1897 ``char symdiff_set_inter = 2``, 1898 simp_tac (srw_ss()) [char_def, order_def, period_def, symdiff_set_inter_def, monoid_exp_def, symdiff_set_def, set_inter_def] >> 1899 `FUNPOW (symdiff univ(:'a)) 2 {} = {}` by rw[FUNPOW_2, symdiff_def] >> 1900 DEEP_INTRO_TAC whileTheory.OLEAST_INTRO >> 1901 rw_tac std_ss[] >| [ (* avoid srw_tac simplication *) 1902 qexists_tac `2` >> 1903 rw[], 1904 `~(n < 2) /\ ~(2 < n)` suffices_by decide_tac >> 1905 (spose_not_then strip_assume_tac) >> 1906 `2 < n ==> ~(0 < 2)` by metis_tac[] >> 1907 `n = 1` by decide_tac >> 1908 full_simp_tac (srw_ss())[symdiff_def] 1909 ]); 1910(* Similar to Michael's proof *) 1911val symdiff_set_inter_char = store_thm( 1912 "symdiff_set_inter_char", 1913 ``char symdiff_set_inter = 2``, 1914 simp_tac (srw_ss()) [char_def, order_def, period_def, symdiff_set_inter_def, monoid_exp_def, symdiff_set_def, set_inter_def] >> 1915 DEEP_INTRO_TAC whileTheory.OLEAST_INTRO >> 1916 rw_tac std_ss[] >| [ (* avoid srw_tac simplication *) 1917 qexists_tac `2` >> 1918 rw[FUNPOW_2, symdiff_def], 1919 `~(n < 2) /\ ~(2 < n)` suffices_by decide_tac >> 1920 rpt strip_tac >| [ 1921 `n = 1` by decide_tac >> 1922 full_simp_tac (srw_ss())[symdiff_def], 1923 (first_x_assum (qspec_then `2` mp_tac)) >> 1924 rw[FUNPOW_2, symdiff_def] 1925 ] 1926 ]); 1927(* Michael's proof *) 1928val symdiff_set_inter_char = store_thm( 1929 "symdiff_set_inter_char", 1930 ``char symdiff_set_inter = 2``, 1931 simp_tac (srw_ss()) [char_def, order_def, period_def, symdiff_set_inter_def, 1932 monoid_exp_def, symdiff_set_def, set_inter_def] >> 1933 DEEP_INTRO_TAC whileTheory.OLEAST_INTRO >> rw[] >| [ 1934 qexists_tac `2` >> rw[FUNPOW_2, symdiff_def], 1935 `~(n < 2) /\ ~(2 < n)` suffices_by decide_tac >> rpt strip_tac >| [ 1936 `n = 1` by decide_tac >> full_simp_tac(srw_ss())[symdiff_def], 1937 first_x_assum (qspec_then `2` mp_tac) >> rw[FUNPOW_2, symdiff_def] 1938 ] 1939 ]); 1940 1941(* Theorem: evaluation for symdiff dields. *) 1942(* Proof: by definitions. *) 1943val symdiff_eval = store_thm( 1944 "symdiff_eval", 1945 ``((symdiff_set).carrier = UNIV) /\ 1946 (!x y. (symdiff_set).op x y = (x UNION y) DIFF (x INTER y)) /\ 1947 ((symdiff_set).id = EMPTY)``, 1948 rw_tac std_ss[symdiff_set_def, symdiff_def]); 1949 1950(* val _ = export_rewrites ["symdiff_eval"]; *) 1951val _ = computeLib.add_persistent_funs ["symdiff_eval"]; 1952(* 1953EVAL ``order (symdiff_set) EMPTY``; 1954> val it = |- order symdiff_set {} = 1 : thm 1955*) 1956 1957(* ------------------------------------------------------------------------- *) 1958(* Order Computation using a WHILE loop *) 1959(* ------------------------------------------------------------------------- *) 1960 1961(* ------------------------------------------------------------------------- *) 1962(* A Small Example of WHILE loop invariant *) 1963(* ------------------------------------------------------------------------- *) 1964 1965(* Pseudocode: search through all indexes from 1. 1966 1967Input: m, n with 1 < m, 0 < n 1968Output: ordz m n, the least index j such that (n ** j = 1) (mod m) 1969 1970if ~(coprime m n) return 0 // initial check 1971// For coprime m n, search the least index j such that (n ** j = 1) (mod m). 1972// Search upwards for least index j 1973j <- 1 // initial index 1974while ((n ** i) MOD m <> 1) j <- j + 1 // increment j 1975return j // the least index j. 1976 1977*) 1978 1979(* Compute ordz m n = order (ZN m).prod n = ordz m n *) 1980val compute_ordz_def = Define` 1981 compute_ordz m n = 1982 if m = 0 then ordz 0 n 1983 else if m = 1 then 1 (* ordz 1 n = 1 *) 1984 else if coprime m n then 1985 WHILE (\i. (n ** i) MOD m <> 1) SUC 1 (* i = 1, WHILE (n ** i (MOD m) <> 1) i <- SUC i) *) 1986 else 0 (* ordz m n = 0 when ~(coprime m n) *) 1987`; 1988 1989(* Examples: 1990> EVAL ``compute_ordz 10 3``; --> 4 1991> EVAL ``compute_ordz 10 4``; --> 0 1992> EVAL ``compute_ordz 10 7``; --> 4 1993> EVAL ``compute_ordz 10 19``; --> 2 1994 1995> EVAL ``phi 10``; --> 4 1996 1997Indeed, (ordz m n) is a divisor of (phi m). 1998Since phi(10) = 4, ordz 10 n is a divisior of 4. 1999 2000> EVAL ``compute_ordz 1 19``; --> 1; 2001 2002> EVAL ``MAP (compute_ordz 7) [1 .. 6]``; = [1; 3; 6; 3; 6; 2] 2003> EVAL ``MAP (combin$C compute_ordz 10) [2 .. 13]``; = [0; 1; 0; 0; 0; 6; 0; 1; 0; 2; 0; 6] 2004 shows that, in decimals (base 10), 1/2 is finite, 1/3 has period 1, 1/7 has period 6, 2005 1/9 has period 1, 1/11 has period 2, 1/13 has period 6. 2006*) 2007 2008(* 2009> EVAL ``WHILE (\i. i <= 4) SUC 1``; 2010val it = |- WHILE (\i. i <= 4) SUC 1 = 5: thm 2011*) 2012 2013(* 2014For WHILE Guard Cmd, 2015we want to show: 2016 {Pre-condition} WHILE Guard Cmd {Post-condition} 2017 2018> WHILE_RULE; 2019val it = |- !R B C. WF R /\ (!s. B s ==> R (C s) s) ==> 2020 HOARE_SPEC (\s. P s /\ B s) C P ==> 2021 HOARE_SPEC P (WHILE B C) (\s. P s /\ ~B s): thm 2022 2023> HOARE_SPEC_DEF; 2024val it = |- !P C Q. HOARE_SPEC P C Q <=> !s. P s ==> Q (C s): thm 2025*) 2026 2027(* Theorem: (!x. Invariant x /\ Guard x ==> f (Cmd x) < f x) /\ 2028 (!x. Precond x ==> Invariant x) /\ 2029 (!x. Invariant x /\ ~Guard x ==> Postcond x) /\ 2030 HOARE_SPEC (\x. Invariant x /\ Guard x) Cmd Invariant ==> 2031 HOARE_SPEC Precond (WHILE Guard Cmd) Postcond *) 2032(* Proof: 2033 By HOARE_SPEC_DEF, change the goal to show: 2034 !s. Invariant s ==> Postcond (WHILE Guard Cmd s) 2035 By complete induction on (f s). 2036 After rewrite by WHILE, this is to show: 2037 Postcond (if Guard s then WHILE Guard Cmd (Cmd s) else s) 2038 If Guard s, 2039 With Invariant s, 2040 ==> Postcond (WHILE Guard Cmd (Cmd s)) by induction hypothesis 2041 If ~(Guard s), 2042 With Invariant s, 2043 ==> Postcond s by given 2044*) 2045val WHILE_RULE_PRE_POST = store_thm( 2046 "WHILE_RULE_PRE_POST", 2047 ``(!x. Invariant x /\ Guard x ==> f (Cmd x) < f x) /\ 2048 (!x. Precond x ==> Invariant x) /\ 2049 (!x. Invariant x /\ ~Guard x ==> Postcond x) /\ 2050 HOARE_SPEC (\x. Invariant x /\ Guard x) Cmd Invariant ==> 2051 HOARE_SPEC Precond (WHILE Guard Cmd) Postcond``, 2052 simp[HOARE_SPEC_DEF] >> 2053 rpt strip_tac >> 2054 `!s. Invariant s ==> Postcond (WHILE Guard Cmd s)` suffices_by metis_tac[] >> 2055 Q.UNDISCH_THEN `Precond s` (K ALL_TAC) >> 2056 rpt strip_tac >> 2057 completeInduct_on `f s` >> 2058 rpt strip_tac >> 2059 fs[PULL_FORALL] >> 2060 first_x_assum (qspec_then `f` assume_tac) >> 2061 rfs[] >> 2062 ONCE_REWRITE_TAC[WHILE] >> 2063 Cases_on `Guard s` >> 2064 simp[]); 2065(* Michael's version: 2066val WHILE_RULE_PRE_POST = Q.store_thm( 2067 "WHILE_RULE_PRE_POST", 2068 `(!x. Invariant x /\ Guard x ==> f (Cmd x) < f x) /\ 2069 (!x. Precond x ==> Invariant x) /\ 2070 (!x. Invariant x /\ ~Guard x ==> Postcond x) /\ 2071 HOARE_SPEC (\x. Invariant x /\ Guard x) Cmd Invariant ==> 2072 HOARE_SPEC Precond (WHILE Guard Cmd) Postcond`, 2073 simp[whileTheory.HOARE_SPEC_DEF] >> 2074 rpt strip_tac >> 2075 `!s. Invariant s ==> Postcond (WHILE Guard Cmd s)` 2076 suffices_by metis_tac[] >> 2077 Q.UNDISCH_THEN `Precond s` (K ALL_TAC) >> 2078 rpt strip_tac >> 2079 completeInduct_on `f s` >> 2080 rpt strip_tac >> 2081 fs[PULL_FORALL] >> 2082 first_x_assum (qspec_then `f` assume_tac) >> 2083 rfs[] >> 2084 ONCE_REWRITE_TAC[WHILE] >> 2085 Cases_on `Guard s` >> simp[] 2086) 2087*) 2088 2089(* Theorem: 1 < m /\ coprime m n ==> 2090 HOARE_SPEC (\i. 0 < i /\ i <= ordz m n) 2091 (WHILE (\i. (n ** i) MOD m <> 1) SUC) 2092 (\i. i = ordz m n) *) 2093(* Proof: 2094 By WHILE_RULE_PRE_POST, this is to show: 2095 ?Invariant f. (!x. (\i. 0 < i /\ i <= ordz m n) x ==> Invariant x) /\ 2096 (!x. Invariant x /\ (\i. (n ** i) MOD m <> 1) x ==> f (SUC x) < f x) /\ 2097 (!x. Invariant x /\ ~(\i. (n ** i) MOD m <> 1) x ==> (\i. i = ordz m n) x) /\ 2098 HOARE_SPEC (\x. Invariant x /\ (\i. (n ** i) MOD m <> 1) x) SUC Invariant 2099 By looking at the first requirement, and peeking at the second, 2100 let Invariant = \i. 0 < i /\ i <= ordz m n, f = \i. ordz m n - i. 2101 This is to show: 2102 (1) 1 < m /\ coprime m n /\ 0 < x /\ x <= ordz m n /\ n ** x MOD m <> 1 ==> 0 < ordz m n - x 2103 If x = ordz m n, then this is true by ZN_coprime_order_alt 2104 Otherwise, x <> ordz m n, hence 0 < ordz m n - x by arithmetic 2105 (2) 1 < m /\ coprime m n /\ 0 < x /\ x <= ordz m n /\ n ** x MOD m = 1 ==> x = ordz m n 2106 If x = ordz m n, then this is true trivially. 2107 Otherwise, x <> ordz m n, 2108 or x < ordz m n, and 0 < m, but n ** x MOD m = 1, contradicts ZN_order_minimal. 2109 (3) 1 < m /\ coprime m n ==> 2110 HOARE_SPEC (\x. (0 < x /\ x <= ordz m n) /\ n ** x MOD m <> 1) SUC (\i. 0 < i /\ i <= ordz m n) 2111 By HOARE_SPEC_DEF, this is to show: 2112 1 < m /\ coprime m n /\ 0 < x /\ x <= ordz m n /\ n ** x MOD m <> 1 ==> SUC x <= ordz m n 2113 or 1 < m /\ coprime m n /\ 0 < x /\ x <= ordz m n /\ n ** x MOD m <> 1 ==> x < ordz m n 2114 By contradiction, suppose x = ordz m n. 2115 Then n ** x MOD m = 1, a contradiction by ZN_coprime_order_alt, 1 < m 2116*) 2117val compute_ordz_hoare = store_thm( 2118 "compute_ordz_hoare", 2119 ``!m n. 1 < m /\ coprime m n ==> 2120 HOARE_SPEC (\i. 0 < i /\ i <= ordz m n) 2121 (WHILE (\i. (n ** i) MOD m <> 1) SUC) 2122 (\i. i = ordz m n)``, 2123 rpt strip_tac >> 2124 irule WHILE_RULE_PRE_POST >> 2125 qexists_tac `\i. 0 < i /\ i <= ordz m n` >> 2126 qexists_tac `\i. ordz m n - i` >> 2127 rw[] >| [ 2128 Cases_on `x = ordz m n` >| [ 2129 rw[] >> 2130 rfs[ZN_coprime_order_alt], 2131 decide_tac 2132 ], 2133 Cases_on `x = ordz m n` >- 2134 simp[] >> 2135 rfs[] >> 2136 `x < ordz m n /\ 0 < m` by decide_tac >> 2137 metis_tac[ZN_order_minimal], 2138 rw[HOARE_SPEC_DEF] >> 2139 `x < ordz m n` suffices_by decide_tac >> 2140 spose_not_then strip_assume_tac >> 2141 `x = ordz m n` by decide_tac >> 2142 rw[] >> 2143 rfs[ZN_coprime_order_alt] 2144 ]); 2145(* Michael's version: 2146val compute_ordz_hoare = prove( 2147 ``1 < m /\ coprime m n ==> 2148 HOARE_SPEC 2149 (\i. 0 < i /\ i <= ordz m n) 2150 (WHILE (\i. (n ** i) MOD m <> 1) SUC) 2151 (\i. i = ordz m n)``, 2152 strip_tac >> 2153 irule WHILE_RULE_PRE_POST >> 2154 qexists_tac `\i. 0 < i /\ i <= ordz m n` >> 2155 qexists_tac `\i. ordz m n - i` >> 2156 rw[] >| [ 2157 (* Case 1 *) 2158 reverse (Cases_on `x = ordz m n`) >- decide_tac >> 2159 rw[] >> 2160 rfs[ZN_coprime_order_alt], 2161 2162 (* Case 2 *) 2163 Cases_on `x = ordz m n` >- simp[] >> 2164 rfs[] >> 2165 `x < ordz m n /\ 0 < m` by decide_tac >> 2166 metis_tac[ZN_order_minimal], 2167 2168 (* Case 3 *) 2169 rw[HOARE_SPEC_DEF] >> 2170 `x < ordz m n` suffices_by decide_tac >> 2171 spose_not_then assume_tac >> 2172 `x = ordz m n` by decide_tac >> rw[] >> 2173 rfs[ZN_coprime_order_alt] 2174 ]); 2175*) 2176 2177(* 2178val compute_ordz_hoare = 2179 |- 1 < m /\ coprime m n ==> HOARE_SPEC (\i. 0 < i /\ i <= ordz m n) 2180 (WHILE (\i. (n ** i) MOD m <> 1) SUC) (\i. i = ordz m n): thm 2181 2182SIMP_RULE (srw_ss()) [HOARE_SPEC_DEF] compute_ordz_hoare; 2183val it = |- 1 < m /\ coprime m n ==> 2184 !i. 0 < i /\ i <= ordz m n ==> (WHILE (\i. (n ** i) MOD m <> 1) SUC i = ordz m n): thm 2185*) 2186 2187(* Theorem: 1 < m /\ coprime m n ==> 2188 !j. 0 < j /\ j <= ordz m n ==> (WHILE (\i. (n ** i) MOD m <> 1) SUC j = ordz m n) *) 2189(* Proof: 2190 By compute_ordz_hoare, we have the loop-invariant: 2191 HOARE_SPEC (\i. 0 < i /\ i <= ordz m n) 2192 (WHILE (\i. (n ** i) MOD m <> 1) SUC) 2193 (\i. i = ordz m n) 2194 Let Px = \i. 0 < i /\ i <= ordz m n be the pre-condition 2195 Cx = WHILE (\i. (n ** i) MOD m <> 1) SUC be the command body 2196 Qx = \i. i = ordz m n be the post-condition 2197 ==> HOARE_SPEC Px Cx Qx by above 2198 Apply HOARE_SPEC_DEF, |- HOARE_SPEC P C Q <=> !s. P s ==> Q (C s) 2199 Thus !j. P j ==> Qx (Cx j) 2200 or !j. 0 < j /\ j <= ordz m n ==> 2201 (WHILE (\i. (n ** i) MOD m <> 1) SUC j = ordz m n) 2202*) 2203val compute_ordz_by_while = prove( 2204 ``!m n. 1 < m /\ coprime m n ==> 2205 !j. 0 < j /\ j <= ordz m n ==> (WHILE (\i. (n ** i) MOD m <> 1) SUC j = ordz m n)``, 2206 rpt strip_tac >> 2207 `HOARE_SPEC 2208 (\i. 0 < i /\ i <= ordz m n) 2209 (WHILE (\i. (n ** i) MOD m <> 1) SUC) 2210 (\i. i = ordz m n)` by rw[compute_ordz_hoare] >> 2211 fs[HOARE_SPEC_DEF]); 2212 2213(* ------------------------------------------------------------------------- *) 2214(* Correctness of computing ordz m n. *) 2215(* ------------------------------------------------------------------------- *) 2216 2217(* Theorem: compute_ordz 0 n = ordz 0 n *) 2218(* Proof: by compute_ordz_def *) 2219val compute_ordz_0 = store_thm( 2220 "compute_ordz_0", 2221 ``!n. compute_ordz 0 n = ordz 0 n``, 2222 rw[compute_ordz_def]); 2223 2224(* Theorem: compute_ordz 1 n = 1 *) 2225(* Proof: by compute_ordz_def *) 2226val compute_ordz_1 = store_thm( 2227 "compute_ordz_1", 2228 ``!n. compute_ordz 1 n = 1``, 2229 rw[compute_ordz_def]); 2230 2231(* Theorem: compute_ordz m n = ordz m n *) 2232(* Proof: 2233 If m = 0, 2234 Then compute_ordz 0 n = ordz 0 n by compute_ordz_0 2235 If m = 1, 2236 Then compute_ordz 1 n = 1 by compute_ordz_1 2237 = ordz 1 n by ZN_order_mod_1 2238 If m <> 0, m <> 1, 2239 Then 1 < m by arithmetic 2240 If ordz m n = 0, 2241 Then ~coprime m n by ZN_order_eq_0 2242 compute_ordz m n 2243 = 0 by compute_ordz_def 2244 = ordz m n by ordz m n = 0 2245 If ordz m n <> 0, 2246 Then coprime m n by ZN_order_eq_0 2247 and 1 <= ordz m n by arithmetic 2248 compute_ordz m n 2249 = WHILE (\i. (n ** i) MOD m <> 1) SUC 1 by compute_ordz_def 2250 = ordz m n by compute_ordz_by_while, put j = 1. 2251*) 2252val compute_ordz_eqn = store_thm( 2253 "compute_ordz_eqn", 2254 ``!m n. compute_ordz m n = ordz m n``, 2255 rpt strip_tac >> 2256 Cases_on `m = 0` >- 2257 rw[compute_ordz_0] >> 2258 `0 < m` by decide_tac >> 2259 Cases_on `m = 1` >- 2260 rw[compute_ordz_1, ZN_order_mod_1] >> 2261 Cases_on `ordz m n = 0` >| [ 2262 `~coprime m n` by rw[GSYM ZN_order_eq_0] >> 2263 rw[compute_ordz_def], 2264 `coprime m n` by metis_tac[ZN_order_eq_0] >> 2265 `1 < m` by decide_tac >> 2266 rw[compute_ordz_def, compute_ordz_by_while] 2267 ]); 2268 2269(* Theorem: order (times_mod m) n = compute_ordz m n *) 2270(* Proof: by compute_ordz_eqn *) 2271val ordz_eval = store_thm( 2272 "ordz_eval[compute]", 2273 ``!m n. order (times_mod m) n = compute_ordz m n``, 2274 rw[ZN_eval, compute_ordz_eqn]); 2275(* Put in computeLib for simplifier. *) 2276 2277(* 2278> EVAL ``ordz 7 10``; 2279val it = |- ordz 7 10 = 6: thm 2280*) 2281 2282 2283(* ------------------------------------------------------------------------- *) 2284 2285(* export theory at end *) 2286val _ = export_theory(); 2287 2288(*===========================================================================*) 2289