diff --git a/examples/AKS/compute/computeBasicScript.sml b/examples/AKS/compute/computeBasicScript.sml index b4c53a499b..33e23565ed 100644 --- a/examples/AKS/compute/computeBasicScript.sml +++ b/examples/AKS/compute/computeBasicScript.sml @@ -621,7 +621,7 @@ val exp_step_odd = store_thm( = r * 1 by MULT_RIGHT_1 = r * m ** 0 by EXP_0 If n <> 0, - then HALF n < n by HALF_LESS, 0 < n + then HALF n < n by HALF_LT, 0 < n If EVEN n, exp_step m n r = exp_step (SQ m) (HALF n) r by exp_step_even @@ -949,7 +949,7 @@ val exp_mod_binary_eqn = store_thm( = 1 MOD m by ONE_MOD, 1 < m = (a ** 0) MOD m by EXP If n <> 0, - Then HALF n < n by HALF_LESS + Then HALF n < n by HALF_LT If EVEN n, Then n MOD 2 = 0 by EVEN_MOD2 exp_mod_binary a n m @@ -986,7 +986,7 @@ val exp_mod_binary_eqn = store_thm( Cases_on `n = 0` >- rw[exp_mod_binary_0, EXP] >> `0 < m` by decide_tac >> - `HALF n < n` by rw[HALF_LESS] >> + `HALF n < n` by rw[HALF_LT] >> rw[Once exp_mod_binary_def] >| [ `((a ** 2) ** HALF n) MOD m = (a ** (2 * HALF n)) MOD m` by rw[EXP_EXP_MULT] >> `_ = (a ** n) MOD m` by rw[GSYM EVEN_HALF, EVEN_MOD2] >> @@ -1113,7 +1113,7 @@ val exp_mod_step_odd = store_thm( = (r * 1) MOD k by MULT_RIGHT_1 = (r * m ** 0) MOD k by EXP_0 If n <> 0, - then HALF n < n by HALF_LESS, 0 < n + then HALF n < n by HALF_LT, 0 < n If EVEN n, exp_mod_step m n k r = exp_mod_step ((SQ m) MOD k) (HALF n) k r by exp_mod_step_even @@ -1308,7 +1308,7 @@ val root_compute_0 = store_thm( Assume !m. m < n ==> (root_compute 1 m = m) To show: root_compute 1 n = n - Note HALF n < n by HALF_LESS, 0 < n + Note HALF n < n by HALF_LT, 0 < n root_compute 1 n = let x = 2 * root_compute 1 (n DIV (2 ** 1)) @@ -1901,13 +1901,13 @@ val gcd_compute_odd_odd = store_thm( (2) n <> 0 ==> n = gcd n 0, true by GCD_0 (3) m <> 0 ==> m = gcd m m by GCD_REF (4) n <> 0 /\ m <> 0 /\ n <> m /\ EVEN n /\ EVEN m ==> 2 * gcd_compute (HALF n) (HALF m) = gcd n m - Note HALF n < n /\ HALF m < m by HALF_LESS, 0 < n, 0 < m + Note HALF n < n /\ HALF m < m by HALF_LT, 0 < n, 0 < m so HALF n + HALF m < n + m by arithmetic 2 * gcd_compute (HALF n) (HALF m) = 2 * gcd (HALF n) (HALF m) by induction hypothesis = gcd n m by BINARY_GCD (5) n <> 0 /\ m <> 0 /\ n <> m /\ EVEN n /\ ~EVEN m ==> gcd_compute (HALF n) m = gcd n m - Note HALF n < n by HALF_LESS, 0 < n + Note HALF n < n by HALF_LT, 0 < n so HALF n + m < n + m by arithmetic Now ODD m by EVEN_ODD gcd_compute (HALF n) m @@ -1915,7 +1915,7 @@ val gcd_compute_odd_odd = store_thm( = gcd n m by BINARY_GCD (6) n <> 0 /\ m <> 0 /\ n <> m /\ ~EVEN n /\ EVEN m ==> gcd_compute n (HALF m) = gcd n m Note ODD n by EVEN_ODD - and HALF m < m by HALF_LESS, 0 < m + and HALF m < m by HALF_LT, 0 < m so n + HALF m < n + m by arithmetic gcd_compute n (HALF m) = gcd n (HALF m) by induction hypothesis @@ -1943,7 +1943,7 @@ val gcd_compute_eqn = store_thm( completeInduct_on `n + m` >> rpt strip_tac >> rw[Once gcd_compute_def] >| [ - `HALF n < n /\ HALF m < m` by rw[HALF_LESS] >> + `HALF n < n /\ HALF m < m` by rw[HALF_LT] >> `HALF n + HALF m < n + m` by rw[] >> rw[BINARY_GCD], metis_tac[BINARY_GCD, EVEN_ODD], diff --git a/examples/AKS/machine/countPolyScript.sml b/examples/AKS/machine/countPolyScript.sml index 36ce7e0419..b073389b94 100644 --- a/examples/AKS/machine/countPolyScript.sml +++ b/examples/AKS/machine/countPolyScript.sml @@ -1549,30 +1549,31 @@ val poly_X_expM_value = store_thm( = PAD_RIGHT 0 (m MOD k) [] ++ [x] ++ ls by unity_mod_zero_alt, ZN_property = PAD_LEFT 0 (m MOD k + 1) [x] ++ ls by PAD_LEFT_BY_RIGHT = lt ++ unity_mod_zero (ZN 0) (k - (m MOD k + 1)) where lt = PAD_LEFT 0 (m MOD k + 1) [x] - = lt ++ PAD_RIGHT 0 (k - (m MOD k + 1)) [] by by unity_mod_zero_alt, ZN_property + = lt ++ PAD_RIGHT 0 (k - (m MOD k + 1)) [] by unity_mod_zero_alt, ZN_property = PAD_RIGHT 0 k lt by PAD_RIGHT_BY_RIGHT, LENGTH lt = (m MOD k) + 1 = PAD_RIGHT 0 k (PAD_LEFT 0 ((m MOD k) + 1) [1 MOD 0]) *) - Theorem poly_X_expM_zero: !k m. valueOf (poly_X_expM 0 k m) = - if k = 0 then [] - else PAD_RIGHT 0 k (PAD_LEFT 0 ((m MOD k) + 1) [1 MOD 0]) -Proof[exclude_simps = MOD_0] - rpt strip_tac >> Cases_on `k <= 1` >| [ + if k = 0 then [] else PAD_RIGHT 0 k (PAD_LEFT 0 ((m MOD k) + 1) [1 MOD 0]) +Proof + rpt strip_tac >> + Cases_on `k <= 1` >| [ `k = 0 \/ k = 1` by decide_tac >- rw[poly_X_expM_def] >> rw[poly_X_expM_def, PAD_LEFT, PAD_RIGHT], - rw[poly_X_expM_def] >> + rw[] >> qabbrev_tac `x = 1 MOD 0` >> qabbrev_tac `ls = unity_mod_zero (ZN 0) (k - (m MOD k + 1))` >> - `valueOf (poly_extendM (x::ls) (m MOD k)) = unity_mod_zero (ZN n) (m MOD k) ++ (x :: ls)` by rw[poly_extendM_value] >> - `ls = PAD_RIGHT 0 (k - (m MOD k + 1)) []` by rw[unity_mod_zero_alt, ZN_property, Abbr`ls`] >> - rw[unity_mod_zero_alt, ZN_property] >> - rw[PAD_LEFT_BY_RIGHT] >> - qabbrev_tac `s = PAD_RIGHT 0 (m MOD k) [] ++ [x]` >> - `LENGTH s = m MOD k + 1` by rw[PAD_RIGHT_LENGTH, Abbr`s`] >> - metis_tac[PAD_RIGHT_BY_RIGHT] + qabbrev_tac `lt = PAD_LEFT 0 (m MOD k + 1) [x]` >> + `LENGTH lt = m MOD k + 1` by rw[PAD_LEFT_LENGTH, MAX_DEF, Abbr`lt`] >> + `valueOf (poly_X_expM 0 k m) = valueOf (poly_extendM (x::ls) (m MOD k))` by rw[poly_X_expM_def, poly_zeroM_value, Abbr`ls`] >> + `_ = unity_mod_zero (ZN n) (m MOD k) ++ (x :: ls)` by rw[poly_extendM_value] >> + `_ = PAD_RIGHT 0 (m MOD k) [] ++ [x] ++ ls` by rw[unity_mod_zero_alt, ZN_property] >> + `_ = lt ++ ls` by rw[PAD_LEFT_BY_RIGHT, Abbr`lt`] >> + `_ = lt ++ PAD_RIGHT 0 (k - (m MOD k + 1)) []` by rw[unity_mod_zero_alt, ZN_property, Abbr`ls`] >> + `_ = PAD_RIGHT 0 k lt` by metis_tac[PAD_RIGHT_BY_RIGHT] >> + fs[Abbr`lt`] ] QED diff --git a/examples/AKS/machine/countPowerScript.sml b/examples/AKS/machine/countPowerScript.sml index 5fda7c919a..7264ca42e1 100644 --- a/examples/AKS/machine/countPowerScript.sml +++ b/examples/AKS/machine/countPowerScript.sml @@ -502,7 +502,7 @@ suitable for: loop2_div_rise_count_cover_le cover k n = 1 + 5 * size n + size k ** 2 + size k * size (SQ k ** HALF n) = 1 + 5 * size n + size k ** 2 + size k * size (k ** (2 * HALF n)) by EXP_EXP_MULT - <= 1 + 5 * size n + size k ** 2 + size k * size (k ** n) by TWO_HALF_LESS_EQ, size_exp_base_le + <= 1 + 5 * size n + size k ** 2 + size k * size (k ** n) by TWO_HALF_LE_THM, size_exp_base_le <= 1 + 5 * size n + size k ** 2 + size k * (n * size k) by size_exp_upper_alt, 0 < n = 1 + 5 * size n + size k ** 2 + n * size k ** 2 by EXP_2 <= 1 + 5 * size n + (1 + n) * size k ** 2 @@ -554,7 +554,7 @@ val expM_steps_upper = store_thm( `cover k n <= 1 + 5 * size n + 8 * n ** 3 * size b ** 2` by (rw[Abbr`cover`, Abbr`f`] >> `(k ** 2) ** HALF n = k ** (2 * HALF n)` by rw[EXP_EXP_MULT] >> - `2 * HALF n <= n` by rw[TWO_HALF_LESS_EQ] >> + `2 * HALF n <= n` by rw[TWO_HALF_LE_THM] >> `size (k ** TWICE (HALF n)) <= size (k ** n)` by rw[size_exp_base_le] >> `size (k ** n) <= n * size k` by rw[size_exp_upper_alt] >> `size k * size ((k ** 2) ** HALF n) <= size k * (n * size k)` by rw[] >> diff --git a/examples/algebra/field/fieldOrderScript.sml b/examples/algebra/field/fieldOrderScript.sml index b38fe2782d..450dd5f0e7 100644 --- a/examples/algebra/field/fieldOrderScript.sml +++ b/examples/algebra/field/fieldOrderScript.sml @@ -951,7 +951,7 @@ We really need ffUnity, for the following: (* Proof: Let m = CARD R+. Then 0 < m by field_nonzero_card_pos - By EXTENSION, IN_BIGUNION, divisors_element, this is to show: + By EXTENSION, IN_BIGUNION, divisors_element_alt, this is to show: (1) x IN s ==> x IN R+ where s = forder_eq n for some n divides m Note x IN s ==> x IN R /\ forder x divides m by field_order_equal_element But x <> #0, for otherwise @@ -972,7 +972,7 @@ val field_order_equal_bigunion = store_thm( rpt (stripDup[FiniteField_def]) >> qabbrev_tac `m = CARD R+` >> `0 < m` by rw[field_nonzero_card_pos, Abbr`m`] >> - rw[EXTENSION, IN_BIGUNION, divisors_element, EQ_IMP_THM] >| [ + rw[EXTENSION, IN_BIGUNION, divisors_element_alt, EQ_IMP_THM] >| [ `x IN R /\ (forder x) divides m` by metis_tac[field_order_equal_element] >> `x <> #0` by metis_tac[field_order_eq_0, ZERO_DIVIDES, NOT_ZERO_LT_ZERO] >> metis_tac[field_nonzero_eq], diff --git a/examples/algebra/finitefield/ffConjugateScript.sml b/examples/algebra/finitefield/ffConjugateScript.sml index 544e3d6af1..b90179e811 100644 --- a/examples/algebra/finitefield/ffConjugateScript.sml +++ b/examples/algebra/finitefield/ffConjugateScript.sml @@ -2926,10 +2926,10 @@ val poly_cyclo_mod_exp_char_eq = store_thm( Claim: (BIGUNION s) <> {} Proof: By BIGUNION_EQ_EMPTY, this is to show: (1) s <> {} - Since (divisors n) <> {} by divisors_not_empty + Since (divisors n) <> {} by divisors_eq_empty, 0 < n Thus s = IMAGE f (divisors n) <> {} by IMAGE_EQ_EMPTY (2) s <> {{}} - Note !k. k IN (divisors n) ==> k divides n by divisors_element_alt + Note !k. k IN (divisors n) ==> k divides n by divisors_element_alt, 0 < n ==> k divides (CARD R+) by DIVIDES_TRANS, 0 < n, n divides (CARD R+) Also !x. x IN s ==> ?k. k IN (divisors n) /\ (x = IMAGE factor (orders f* k)) by IN_IMAGE @@ -2965,7 +2965,7 @@ val poly_unity_by_distinct_irreducibles = store_thm( `FINITE (BIGUNION s)` by rw[FINITE_BIGUNION] >> `(BIGUNION s) <> {}` by (rw[BIGUNION_EQ_EMPTY] >- - rw[divisors_not_empty, IMAGE_EQ_EMPTY, Abbr`s`] >> + rw[divisors_eq_empty, IMAGE_EQ_EMPTY, Abbr`s`] >> `!k. k IN (divisors n) ==> k divides (CARD R+)` by metis_tac[divisors_element_alt, DIVIDES_TRANS] >> `!n. f n = IMAGE factor (orders f* n)` by rw[Abbr`f`] >> `!x. x IN s ==> ?k. k IN (divisors n) /\ (x = IMAGE factor (orders f* k))` by metis_tac[IN_IMAGE] >> diff --git a/examples/algebra/finitefield/ffMasterScript.sml b/examples/algebra/finitefield/ffMasterScript.sml index efd90c49f0..59e961c4e0 100644 --- a/examples/algebra/finitefield/ffMasterScript.sml +++ b/examples/algebra/finitefield/ffMasterScript.sml @@ -160,8 +160,9 @@ open fieldBinomialTheory; (* for finite_field_freshman_all *) BIGUNION (IMAGE (monic_irreducibles_degree r) (divisors n)) monic_irreducibles_degree_member |- !r n p. p IN monic_irreducibles_degree r n <=> monic p /\ ipoly p /\ (deg p = n) - monic_irreducibles_bounded_member |- !r n p. p IN monic_irreducibles_bounded r n <=> - monic p /\ ipoly p /\ deg p <= n /\ deg p divides n + monic_irreducibles_bounded_member |- !r n p. Field r ==> + (p IN monic_irreducibles_bounded r n <=> + monic p /\ ipoly p /\ deg p <= n /\ deg p divides n) monic_irreducibles_degree_finite |- !r. FINITE R /\ #0 IN R ==> !n. FINITE (monic_irreducibles_degree r n) monic_irreducibles_bounded_finite |- !r. FINITE R /\ #0 IN R ==> @@ -1341,11 +1342,12 @@ val monic_irreducibles_degree_member = store_thm( ``!(r:'a field) n p. p IN (monic_irreducibles_degree r n) <=> monic p /\ ipoly p /\ (deg p = n)``, rw[monic_irreducibles_degree_def]); -(* Theorem: p IN (monic_irreducibles_bounded r n) <=> - monic p /\ ipoly p /\ (deg p <= n) /\ (deg p) divides n *) +(* Theorem: Field r ==> (p IN (monic_irreducibles_bounded r n) <=> + monic p /\ ipoly p /\ (deg p <= n) /\ (deg p) divides n) *) (* Proof: + Note 0 < deg p by poly_irreducible_deg_nonzero p IN (monic_irreducibles_bounded r n) - <=> p IN BIGUNION (IMAGE (monic_irreducibles_degree r) (divisors n)) by monic_irreducibles_bounded_def + <=> p IN BIGUNION (IMAGE (monic_irreducibles_degree r) (divisors n)) by monic_irreducibles_bounded_def <=> ?s. p IN s /\ s IN (IMAGE (monic_irreducibles_degree r) (divisors n)) by IN_BIGUNION Take s = monic_irreducibles_degree r (deg p), Then p IN s @@ -1356,13 +1358,14 @@ val monic_irreducibles_degree_member = store_thm( *) val monic_irreducibles_bounded_member = store_thm( "monic_irreducibles_bounded_member", - ``!(r:'a field) n p. p IN (monic_irreducibles_bounded r n) <=> - monic p /\ ipoly p /\ (deg p <= n) /\ (deg p) divides n``, + ``!(r:'a field) n p. Field r ==> + (p IN (monic_irreducibles_bounded r n) <=> + monic p /\ ipoly p /\ (deg p <= n) /\ (deg p) divides n)``, (rw[monic_irreducibles_bounded_def, monic_irreducibles_degree_member, divisors_element, EXTENSION, EQ_IMP_THM] >> simp[]) >> qexists_tac `monic_irreducibles_degree r (deg p)` >> simp[monic_irreducibles_degree_member] >> qexists_tac `deg p` >> - simp[]); + simp[poly_irreducible_deg_nonzero]); (* Theorem: FINITE R /\ #0 IN R ==> !n. FINITE (monic_irreducibles_degree r n) *) (* Proof: @@ -2574,9 +2577,6 @@ val poly_master_subfield_eq_monic_irreducibles_prod_image_alt_1 = store_thm( (* Theorem: FiniteField r /\ s <<= r /\ 0 < n ==> (master (CARD B ** n) = poly_prod_set s {poly_psi s d | d divides n}) *) (* Proof: by poly_master_subfield_eq_monic_irreducibles_prod_image *) -(* Theorem: FiniteField r /\ 0 < n ==> - (master (CARD R ** n) = PPROD {PPROD (monic_irreducibles_degree r d) | d | d divides n}) *) -(* Proof: by poly_master_eq_monic_irreducibles_prod_image *) val poly_master_subfield_eq_monic_irreducibles_prod_image_alt_2 = store_thm( "poly_master_subfield_eq_monic_irreducibles_prod_image_alt_2", ``!(r s):'a field n. FiniteField r /\ s <<= r /\ 0 < n ==> @@ -2588,7 +2588,7 @@ val poly_master_subfield_eq_monic_irreducibles_prod_image_alt_2 = store_thm( `x' = monic_irreducibles_degree s x''` suffices_by fs[divisors_def] >> rw[EXTENSION] >> metis_tac[], - metis_tac[DIVIDES_LE, divisors_element] + metis_tac[DIVIDES_LE, divisors_element_alt] ]); (* Next is better than above. *) @@ -2635,7 +2635,7 @@ val poly_master_eq_monic_irreducibles_prod_image_alt_2 = store_thm( `x' = monic_irreducibles_degree r x''` suffices_by fs[divisors_def] >> rw[EXTENSION] >> metis_tac[], - metis_tac[DIVIDES_LE, divisors_element] + metis_tac[DIVIDES_LE, divisors_element_alt] ]); (* ------------------------------------------------------------------------- *) @@ -2789,7 +2789,7 @@ val monic_irreducibles_degree_prod_set_divides_master = store_thm( Note FINITE (natural n) by natural_finite ==> FINITE t by IMAGE_FINITE - Note (divisors n) SUBSET (natural n) by divisors_subset_natural, 0 < n + Note (divisors n) SUBSET (natural n) by divisors_subset_natural ==> s SUBSET t by IMAGE_SUBSET Claim: pset t Proof: This is to show: poly (PPROD (monic_irreducibles_degree r (SUC x''))) diff --git a/examples/algebra/finitefield/ffSplitScript.sml b/examples/algebra/finitefield/ffSplitScript.sml index a16d9890e1..9dd759e1f7 100644 --- a/examples/algebra/finitefield/ffSplitScript.sml +++ b/examples/algebra/finitefield/ffSplitScript.sml @@ -2083,7 +2083,7 @@ val poly_unity_cyclo_factors_alt = store_thm( Let p = IMAGE (Phi k) (divisors k). Then unity k = PPROD p by poly_unity_cyclo_factors Note 0 < k by finite_field_card_coprime_pos - Now n IN (divisors k) by divisors_element, DIVIDES_LE + Now n IN (divisors k) by divisors_element_alt so (Phi k n) IN p by IN_IMAGE Note FINITE (divisors k) by divisors_finite so FINITE p by IMAGE_FINITE @@ -2101,7 +2101,7 @@ val poly_phi_divides_unity = store_thm( `!x. x IN p <=> ?m. (x = Phi k m) /\ m IN divisors k` by rw[Abbr`p`] >> `unity k = PPROD p` by rw[poly_unity_cyclo_factors] >> `0 < k` by metis_tac[finite_field_card_coprime_pos] >> - `n IN (divisors k)` by rw[divisors_element, DIVIDES_LE] >> + `n IN (divisors k)` by rw[divisors_element_alt] >> `(Phi k n) IN p` by metis_tac[] >> `FINITE (divisors k)` by rw[divisors_finite] >> `FINITE p` by rw[Abbr`p`] >> diff --git a/examples/algebra/finitefield/ffUnityScript.sml b/examples/algebra/finitefield/ffUnityScript.sml index e64897a45a..e01962b58c 100644 --- a/examples/algebra/finitefield/ffUnityScript.sml +++ b/examples/algebra/finitefield/ffUnityScript.sml @@ -718,10 +718,9 @@ field_order_equal_card_choices Let m = CARD R+, s = divisors m. Then 0 < m by field_nonzero_card_pos and FINITE s by divisors_finite - ==> FINITE t by IMAGE_FINITE Step 1: partition s - Let u = {n | n IN s /\ (forder_eq n = {})}, + Let u = {n | n IN s /\ forder_eq n = {}}, v = {n | n IN s /\ forder_eq n <> {}}. Then FINITE u /\ FINITE v /\ split s u v by finite_partition_by_predicate @@ -743,7 +742,7 @@ field_order_equal_card_choices Claim: SIGMA (CARD o forder_eq) v = SIGMA phi v Proof: Note !x. x IN s /\ forder_eq x <> {} ==> CARD (forder_eq x) <> 0 by field_order_equal_finite, CARD_EQ_0 - and x <> 0, or 0 < x by divisors_has_0, x IN s, m <> 0 + and 0 < x by divisors_nonzero, x IN s so CARD (forder_eq x) = phi x by field_order_equal_card_eqn or (CARD o forder_eq) x = phi x by o_THM @@ -758,13 +757,13 @@ field_order_equal_card_choices Step 3: get a contradiction Note n <= m by DIVIDES_LE, n divides m - so n IN s by divisors_element + so n IN s by divisors_element_alt, 0 < m ==> forder n IN u by IN_IMAGE or u <> {} by MEMBER_NOT_EMPTY ==> v <> s by finite_partition_property But v SUBSET s by SUBSET_UNION so v PSUBSET s by PSUBSET_DEF, v <> s - Also !x. x IN s ==> phi x <> 0 by phi_eq_0, divisors_has_0, m <> 0 + Also !x. x IN s ==> phi x <> 0 by phi_eq_0, divisors_nonzero Thus SIGMA phi v < SIGMA phi s by SUM_IMAGE_PSUBSET_LT, [2] Now SIGMA phi s = m by Gauss_little_thm @@ -790,24 +789,24 @@ val field_order_equal_nonempty = store_thm( `!n. n IN v <=> n IN s /\ forder_eq n <> {}` by rw[Abbr`v`] >> `FINITE u /\ FINITE v /\ split s u v` by metis_tac[finite_partition_by_predicate] >> `SIGMA (CARD o forder_eq) u = 0` by - (`!x. x IN u ==> ((CARD o forder_eq) x = (K 0) x)` by metis_tac[CARD_EMPTY, IN_IMAGE, combinTheory.K_THM, combinTheory.o_THM] >> + (`!x. x IN u ==> (CARD o forder_eq) x = (K 0) x` by metis_tac[CARD_EMPTY, IN_IMAGE, combinTheory.K_THM, combinTheory.o_THM] >> `SIGMA (CARD o forder_eq) u = SIGMA (K 0) u` by metis_tac[SUM_IMAGE_CONG] >> rw[SUM_IMAGE_CONSTANT]) >> `SIGMA (CARD o forder_eq) v = SIGMA phi v` by ((irule SUM_IMAGE_CONG >> rpt conj_tac) >| [ rw_tac std_ss[] >> `CARD (forder_eq x) <> 0` by metis_tac[field_order_equal_finite, CARD_EQ_0] >> - `0 < x` by metis_tac[divisors_has_0, NOT_ZERO_LT_ZERO] >> + `0 < x` by metis_tac[divisors_nonzero] >> metis_tac[field_order_equal_card_eqn], decide_tac ]) >> `m = SIGMA (CARD o forder_eq) s` by rw[field_order_equal_over_divisors_sigma_card, Abbr`s`, Abbr`m`] >> `_ = SIGMA phi v` by rw[SUM_IMAGE_DISJOINT] >> - `n IN s` by rw[divisors_element, DIVIDES_LE, Abbr`s`] >> + `n IN s` by rw[divisors_element_alt, Abbr`s`] >> `u <> {}` by metis_tac[MEMBER_NOT_EMPTY] >> `v <> s` by metis_tac[finite_partition_property] >> `v PSUBSET s` by metis_tac[PSUBSET_DEF, SUBSET_UNION] >> - `!x. x IN s ==> phi x <> 0` by metis_tac[phi_eq_0, divisors_has_0, NOT_ZERO_LT_ZERO] >> + `!x. x IN s ==> phi x <> 0` by metis_tac[phi_eq_0, divisors_nonzero, NOT_ZERO] >> `SIGMA phi v < SIGMA phi s` by metis_tac[SUM_IMAGE_PSUBSET_LT] >> `SIGMA phi s = m` by rw[Gauss_little_thm, Abbr`s`] >> decide_tac diff --git a/examples/algebra/group/groupCyclicScript.sml b/examples/algebra/group/groupCyclicScript.sml index 7e4d185d3d..1443ed2292 100644 --- a/examples/algebra/group/groupCyclicScript.sml +++ b/examples/algebra/group/groupCyclicScript.sml @@ -1097,7 +1097,7 @@ val cyclic_eq_order_partition = store_thm( ==> 0 < CARD G by finite_group_card_pos, FiniteGroup g partition (eq_order g) G = {orders g n | n | n divides (CARD G)} by cyclic_eq_order_partition - = {orders g n | n | n IN divisors (CARD G)} by rw[divisors_element_alt + = {orders g n | n | n IN divisors (CARD G)} by divisors_element_alt, 0 < CARD G *) val cyclic_eq_order_partition_alt = store_thm( "cyclic_eq_order_partition_alt", @@ -1137,7 +1137,7 @@ val cyclic_eq_order_partition_alt = store_thm( (2) x' IN divisors m ==> ?x''. (phi x' = CARD x'') /\ ?x. x IN orders g x' Let n = x', y = z ** (m DIV n). Since n IN divisors m, - ==> n divides m by divisors_element + ==> n <= m /\ n divides m by divisors_element Let s = orders g n, Then CARD s = phi n by cyclic_orders_card and y IN G by group_exp_element @@ -1206,20 +1206,21 @@ QED If part: x IN G ==> ord x <= CARD G /\ (ord x) divides (CARD G) Since FiniteGroup g ==> 0 < CARD G by finite_group_card_pos also ==> (ord x) divides (CARD G) by group_order_divides - Hence ord x <= CARD G by DIVIDES_LE + Hence ord x IN divisors (CARD G) by divisors_element_alt, 0 < CARD G Only-if part: n <= CARD G /\ n divides CARD G ==> ?x. x IN G /\ (ord x = n) True by cyclic_finite_has_order_divisor. *) -val cyclic_image_ord_is_divisors = store_thm( - "cyclic_image_ord_is_divisors", - ``!g:'a group. cyclic g /\ FINITE G ==> (IMAGE ord G = divisors (CARD G))``, +Theorem cyclic_image_ord_is_divisors: + !g:'a group. cyclic g /\ FINITE G ==> (IMAGE ord G = divisors (CARD G)) +Proof rpt strip_tac >> `Group g` by rw[] >> `FiniteGroup g` by metis_tac[FiniteGroup_def] >> - rw[EXTENSION, divisors_def, EQ_IMP_THM] >- - rw[group_order_divides, DIVIDES_LE, finite_group_card_pos] >- + `0 < CARD G` by simp[finite_group_card_pos] >> + rw[EXTENSION, divisors_element_alt, EQ_IMP_THM] >- rw[group_order_divides] >> - metis_tac[cyclic_finite_has_order_divisor]); + metis_tac[cyclic_finite_has_order_divisor] +QED (* Theorem: cyclic g /\ FINITE G ==> (partition (eq_order g) G = IMAGE (orders g) (divisors (CARD G))) *) (* Proof: @@ -1228,17 +1229,18 @@ val cyclic_image_ord_is_divisors = store_thm( so 0 < CARD G by finite_group_card_pos Then partition (eq_order g) G = {orders g n | n | n divides CARD G} by cyclic_eq_order_partition - = IMAGE (orders g) (divisors (CARD G)) by divisors_def, EXTENSION, DIVIDES_LE + = IMAGE (orders g) (divisors (CARD G)) by divisors_element_alt, 0 < CARD G *) -val cyclic_orders_partition = store_thm( - "cyclic_orders_partition", - ``!g:'a group. cyclic g /\ FINITE G ==> (partition (eq_order g) G = IMAGE (orders g) (divisors (CARD G)))``, +Theorem cyclic_orders_partition: + !g:'a group. cyclic g /\ FINITE G ==> + (partition (eq_order g) G = IMAGE (orders g) (divisors (CARD G))) +Proof rpt strip_tac >> `FiniteGroup g` by metis_tac[FiniteGroup_def, cyclic_group] >> `0 < CARD G` by rw[finite_group_card_pos] >> `partition (eq_order g) G = {orders g n | n | n divides CARD G}` by rw[cyclic_eq_order_partition] >> - rw[divisors_def, EXTENSION] >> - metis_tac[DIVIDES_LE]); + rw[divisors_element_alt, EXTENSION] +QED (* ------------------------------------------------------------------------- *) (* Finite Cyclic Group Existence. *) diff --git a/examples/algebra/lib/GaussScript.sml b/examples/algebra/lib/GaussScript.sml index 9cf3632a49..45c930ef1e 100644 --- a/examples/algebra/lib/GaussScript.sml +++ b/examples/algebra/lib/GaussScript.sml @@ -34,6 +34,10 @@ open helperNumTheory helperSetTheory helperFunctionTheory; (* (* val _ = load "gcdTheory"; -- in helperNumTheory *) *) open dividesTheory gcdTheory; +(* for SQRT and related theorems *) +(* val _ = load "logPowerTheory"; *) +open logrootTheory logPowerTheory; + (* ------------------------------------------------------------------------- *) (* Gauss' Little Theorem *) @@ -105,26 +109,31 @@ open dividesTheory gcdTheory; phi_lt |- !n. 1 < n ==> phi n < n Divisors: - divisors_def |- !n. divisors n = {d | d <= n /\ d divides n} - divisors_element |- !n d. d IN divisors n <=> d <= n /\ d divides n + divisors_def |- !n. divisors n = {d | 0 < d /\ d <= n /\ d divides n} + divisors_element |- !n d. d IN divisors n <=> 0 < d /\ d <= n /\ d divides n divisors_element_alt |- !n. 0 < n ==> !d. d IN divisors n <=> d divides n - divisors_has_one |- !n. 0 < n ==> 1 IN divisors n - divisors_has_last |- !n. n IN divisors n - divisors_not_empty |- !n. divisors n <> {} + divisors_has_element |- !n d. d IN divisors n ==> 0 < n + divisors_has_1 |- !n. 0 < n ==> 1 IN divisors n + divisors_has_last |- !n. 0 < n ==> n IN divisors n + divisors_not_empty |- !n. 0 < n ==> divisors n <> {} + divisors_0 |- divisors 0 = {} + divisors_1 |- divisors 1 = {1} + divisors_eq_empty |- !n. divisors n = {} <=> n = 0 ! divisors_eqn |- !n. divisors n = - if n = 0 then {0} - else IMAGE (\j. if j + 1 divides n then j + 1 else 1) (count n) - divisors_cofactor |- !n d. 0 < n /\ d IN divisors n ==> n DIV d IN divisors n - divisors_delete_last |- !n. 0 < n ==> (divisors n DELETE n = {m | m < n /\ m divides n}) - divisors_nonzero |- !n. 0 < n ==> !d. d IN divisors n ==> 0 < d - divisors_has_cofactor |- !n. 0 < n ==> !d. d IN divisors n ==> n DIV d IN divisors n - divisors_subset_upto |- !n. divisors n SUBSET upto n - divisors_subset_natural |- !n. 0 < n ==> divisors n SUBSET natural n + IMAGE (\j. if j + 1 divides n then j + 1 else 1) (count n) + divisors_has_factor |- !n p q. 0 < n /\ n = p * q ==> p IN divisors n /\ q IN divisors n + divisors_has_cofactor |- !n d. d IN divisors n ==> n DIV d IN divisors n + divisors_delete_last |- !n. divisors n DELETE n = {m | 0 < m /\ m < n /\ m divides n} + divisors_nonzero |- !n d. d IN divisors n ==> 0 < d + divisors_subset_natural |- !n. divisors n SUBSET natural n divisors_finite |- !n. FINITE (divisors n) - divisors_0 |- divisors 0 = {0} - divisors_1 |- divisors 1 = {1} - divisors_has_0 |- !n. 0 IN divisors n <=> (n = 0) - divisors_divisors_bij |- !n. 0 < n ==> (\d. n DIV d) PERMUTES divisors n + divisors_divisors_bij |- !n. (\d. n DIV d) PERMUTES divisors n + + An upper bound for divisors: + divisor_le_cofactor_ge |- !n p. 0 < p /\ p divides n /\ p <= SQRT n ==> SQRT n <= n DIV p + divisor_gt_cofactor_le |- !n p. 0 < p /\ p divides n /\ SQRT n < p ==> n DIV p <= SQRT n + divisors_cofactor_inj |- !n. INJ (\j. n DIV j) (divisors n) univ(:num) + divisors_card_upper |- !n. CARD (divisors n) <= TWICE (SQRT n) Gauss' Little Theorem: gcd_matches_divisor_element |- !n d. d divides n ==> @@ -133,24 +142,24 @@ open dividesTheory gcdTheory; BIJ (\j. j DIV d) (gcd_matches n d) (coprimes_by n d) gcd_matches_bij_coprimes |- !n d. 0 < n /\ d divides n ==> BIJ (\j. j DIV d) (gcd_matches n d) (coprimes (n DIV d)) - divisors_eq_gcd_image |- !n. 0 < n ==> (divisors n = IMAGE (gcd n) (natural n)) - gcd_eq_equiv_class |- !n d. feq_class (gcd n) (natural n) d = gcd_matches n d - gcd_eq_equiv_class_fun |- !n. feq_class (gcd n) (natural n) = gcd_matches n - gcd_eq_partition_by_divisors |- !n. 0 < n ==> (partition (feq (gcd n)) (natural n) = - IMAGE (gcd_matches n) (divisors n)) - gcd_eq_equiv_on_natural |- !n. feq (gcd n) equiv_on natural n + divisors_eq_gcd_image |- !n. divisors n = IMAGE (gcd n) (natural n) + gcd_eq_equiv_class |- !n d. feq_class (gcd n) (natural n) d = gcd_matches n d + gcd_eq_equiv_class_fun |- !n. feq_class (gcd n) (natural n) = gcd_matches n + gcd_eq_partition_by_divisors |- !n. partition (feq (gcd n)) (natural n) = + IMAGE (gcd_matches n) (divisors n) + gcd_eq_equiv_on_natural |- !n. feq (gcd n) equiv_on natural n sum_over_natural_by_gcd_partition - |- !f n. SIGMA f (natural n) = - SIGMA (SIGMA f) (partition (feq (gcd n)) (natural n)) - sum_over_natural_by_divisors |- !f n. SIGMA f (natural n) = - SIGMA (SIGMA f) (IMAGE (gcd_matches n) (divisors n)) - gcd_matches_from_divisors_inj |- !n. INJ (gcd_matches n) (divisors n) univ(:num -> bool) + |- !f n. SIGMA f (natural n) = + SIGMA (SIGMA f) (partition (feq (gcd n)) (natural n)) + sum_over_natural_by_divisors |- !f n. SIGMA f (natural n) = + SIGMA (SIGMA f) (IMAGE (gcd_matches n) (divisors n)) + gcd_matches_from_divisors_inj |- !n. INJ (gcd_matches n) (divisors n) univ(:num -> bool) gcd_matches_and_coprimes_by_same_size |- !n. CARD o gcd_matches n = CARD o coprimes_by n - coprimes_by_with_card |- !n. 0 < n ==> (CARD o coprimes_by n = - (\d. phi (if d IN divisors n then n DIV d else 0))) - coprimes_by_divisors_card |- !n. 0 < n ==> !x. x IN divisors n ==> - ((CARD o coprimes_by n) x = (\d. phi (n DIV d)) x) - Gauss_little_thm |- !n. n = SIGMA phi (divisors n) + coprimes_by_with_card |- !n. 0 < n ==> CARD o coprimes_by n = + (\d. phi (if d IN divisors n then n DIV d else 0)) + coprimes_by_divisors_card |- !n x. x IN divisors n ==> + (CARD o coprimes_by n) x = (\d. phi (n DIV d)) x + Gauss_little_thm |- !n. SIGMA phi (divisors n) = n Euler phi function is multiplicative for coprimes: coprimes_mult_by_image @@ -200,32 +209,40 @@ open dividesTheory gcdTheory; rec_phi_eq_phi |- !n. rec_phi n = phi n Useful Theorems: - coprimes_from_notone_inj |- INJ coprimes (univ(:num) DIFF {1}) univ(:num -> bool) - divisors_eq_image_gcd_upto |- !n. divisors n = IMAGE (gcd n) (upto n) - gcd_eq_equiv_on_upto |- !n. feq (gcd n) equiv_on upto n - gcd_eq_upto_partition_by_divisors |- !n. partition (feq (gcd n)) (upto n) = - IMAGE (preimage (gcd n) (upto n)) (divisors n) - sum_over_upto_by_gcd_partition |- !f n. SIGMA f (upto n) = - SIGMA (SIGMA f) (partition (feq (gcd n)) (upto n)) - sum_over_upto_by_divisors |- !f n. SIGMA f (upto n) = - SIGMA (SIGMA f) (IMAGE (preimage (gcd n) (upto n)) (divisors n)) - - divisors_eq_image_gcd_count |- !n. 0 < n ==> (divisors n = IMAGE (gcd n) (count n)) - gcd_eq_equiv_on_count |- !n. feq (gcd n) equiv_on count n - gcd_eq_count_partition_by_divisors |- !n. 0 < n ==> (partition (feq (gcd n)) (count n) = - IMAGE (preimage (gcd n) (count n)) (divisors n)) - sum_over_count_by_gcd_partition |- !f n. SIGMA f (count n) = - SIGMA (SIGMA f) (partition (feq (gcd n)) (count n)) - sum_over_count_by_divisors |- !f n. 0 < n ==> (SIGMA f (count n) = - SIGMA (SIGMA f) (IMAGE (preimage (gcd n) (count n)) (divisors n))) - - divisors_eq_image_gcd_natural |- !n. 0 < n ==> (divisors n = IMAGE (gcd n) (natural n)) - gcd_eq_natural_partition_by_divisors |- !n. 0 < n ==> (partition (feq (gcd n)) (natural n) = - IMAGE (preimage (gcd n) (natural n)) (divisors n)) - sum_over_natural_by_preimage_divisors |- !f n. 0 < n ==> (SIGMA f (natural n) = - SIGMA (SIGMA f) (IMAGE (preimage (gcd n) (natural n)) (divisors n))) - sum_image_divisors_cong |- !f g. (f 1 = g 1) /\ - (!n. SIGMA f (divisors n) = SIGMA g (divisors n)) ==> (f = g) + coprimes_from_not_1_inj |- INJ coprimes (univ(:num) DIFF {1}) univ(:num -> bool) + divisors_eq_image_gcd_upto |- !n. 0 < n ==> divisors n = IMAGE (gcd n) (upto n) + gcd_eq_equiv_on_upto |- !n. feq (gcd n) equiv_on upto n + gcd_eq_upto_partition_by_divisors + |- !n. 0 < n ==> + partition (feq (gcd n)) (upto n) = + IMAGE (preimage (gcd n) (upto n)) (divisors n) + sum_over_upto_by_gcd_partition + |- !f n. SIGMA f (upto n) = + SIGMA (SIGMA f) (partition (feq (gcd n)) (upto n)) + sum_over_upto_by_divisors |- !f n. 0 < n ==> + SIGMA f (upto n) = + SIGMA (SIGMA f) (IMAGE (preimage (gcd n) (upto n)) (divisors n)) + + divisors_eq_image_gcd_count |- !n. divisors n = IMAGE (gcd n) (count n) + gcd_eq_equiv_on_count |- !n. feq (gcd n) equiv_on count n + gcd_eq_count_partition_by_divisors + |- !n. partition (feq (gcd n)) (count n) = + IMAGE (preimage (gcd n) (count n)) (divisors n) + sum_over_count_by_gcd_partition + |- !f n. SIGMA f (count n) = + SIGMA (SIGMA f) (partition (feq (gcd n)) (count n)) + sum_over_count_by_divisors |- !f n. SIGMA f (count n) = + SIGMA (SIGMA f) (IMAGE (preimage (gcd n) (count n)) (divisors n)) + + divisors_eq_image_gcd_natural + |- !n. divisors n = IMAGE (gcd n) (natural n) + gcd_eq_natural_partition_by_divisors + |- !n. partition (feq (gcd n)) (natural n) = + IMAGE (preimage (gcd n) (natural n)) (divisors n) + sum_over_natural_by_preimage_divisors + |- !f n. SIGMA f (natural n) = + SIGMA (SIGMA f) (IMAGE (preimage (gcd n) (natural n)) (divisors n)) + sum_image_divisors_cong |- !f g. f 0 = g 0 /\ (!n. SIGMA f (divisors n) = SIGMA g (divisors n)) ==> f = g *) (* Theory: @@ -959,91 +976,138 @@ val phi_lt = store_thm( (* ------------------------------------------------------------------------- *) (* Define the set of divisors of a number. *) -val divisors_def = zDefine ` - divisors n = {d | d <= n /\ d divides n} -`; -(* use zDefine as this is not computationally effective. *) -(* Note: use of d <= n to give bounded divisors, so that divisors_0 = {0} only. *) +Definition divisors_def[nocompute]: + divisors n = {d | 0 < d /\ d <= n /\ d divides n} +End +(* use [nocompute] as this is not computationally effective. *) +(* Note: use of 0 < d to have positive divisors, as only 0 divides 0. *) +(* Note: use of d <= n to give divisors_0 = {}, since ALL_DIVIDES_0. *) (* Note: for 0 < n, d <= n is redundant, as DIVIDES_LE implies it. *) -(* Theorem: d IN divisors n <=> d <= n /\ d divides n *) +(* Theorem: d IN divisors n <=> 0 < d /\ d <= n /\ d divides n *) (* Proof: by divisors_def *) -val divisors_element = store_thm( - "divisors_element", - ``!n d. d IN divisors n <=> d <= n /\ d divides n``, - rw[divisors_def]); +Theorem divisors_element: + !n d. d IN divisors n <=> 0 < d /\ d <= n /\ d divides n +Proof + rw[divisors_def] +QED (* Theorem: 0 < n ==> !d. d IN divisors n <=> d divides n *) (* Proof: If part: d IN divisors n ==> d divides n - True by divisors_element + This is true by divisors_element Only-if part: 0 < n /\ d divides n ==> d IN divisors n Since 0 < n /\ d divides n - ==> 0 < d /\ d <= n by divides_pos - Hence d IN divisors n by divisors_element + ==> 0 < d /\ d <= n by divides_pos + Hence d IN divisors n by divisors_element +*) +Theorem divisors_element_alt: + !n. 0 < n ==> !d. d IN divisors n <=> d divides n +Proof + metis_tac[divisors_element, divides_pos] +QED + +(* Theorem: d IN divisors n ==> 0 < n *) +(* Proof: + Note 0 < d /\ d <= n /\ d divides n by divisors_def + so 0 < n by inequality *) -val divisors_element_alt = store_thm( - "divisors_element_alt", - ``!n. 0 < n ==> !d. d IN divisors n <=> d divides n``, - metis_tac[divisors_element, divides_pos]); +Theorem divisors_has_element: + !n d. d IN divisors n ==> 0 < n +Proof + simp[divisors_def] +QED (* Theorem: 0 < n ==> 1 IN (divisors n) *) (* Proof: - Note 0 < n ==> 1 <= n by arithmetic - and 1 divides n by ONE_DIVIDES_ALL - Hence 1 IN (divisors n) by divisors_element + Note 1 divides n by ONE_DIVIDES_ALL + Hence 1 IN (divisors n) by divisors_element_alt *) -val divisors_has_one = store_thm( - "divisors_has_one", - ``!n. 0 < n ==> 1 IN (divisors n)``, - rw[divisors_element]); +Theorem divisors_has_1: + !n. 0 < n ==> 1 IN (divisors n) +Proof + simp[divisors_element_alt] +QED -(* Theorem: n IN (divisors n) *) -(* Proof: by divisors_element *) -val divisors_has_last = store_thm( - "divisors_has_last", - ``!n. n IN (divisors n)``, - rw[divisors_element]); +(* Theorem: 0 < n ==> n IN (divisors n) *) +(* Proof: + Note n divides n by DIVIDES_REFL + Hence n IN (divisors n) by divisors_element_alt +*) +Theorem divisors_has_last: + !n. 0 < n ==> n IN (divisors n) +Proof + simp[divisors_element_alt] +QED -(* Theorem: divisors n <> {} *) +(* Theorem: 0 < n ==> divisors n <> {} *) (* Proof: by divisors_has_last, MEMBER_NOT_EMPTY *) -val divisors_not_empty = store_thm( - "divisors_not_empty", - ``!n. divisors n <> {}``, - metis_tac[divisors_has_last, MEMBER_NOT_EMPTY]); +Theorem divisors_not_empty: + !n. 0 < n ==> divisors n <> {} +Proof + metis_tac[divisors_has_last, MEMBER_NOT_EMPTY] +QED + +(* Theorem: divisors 0 = {} *) +(* Proof: by divisors_def, 0 < d /\ d <= 0 is impossible. *) +Theorem divisors_0: + divisors 0 = {} +Proof + simp[divisors_def] +QED + +(* Theorem: divisors 1 = {1} *) +(* Proof: by divisors_def, 0 < d /\ d <= 1 ==> d = 1. *) +Theorem divisors_1: + divisors 1 = {1} +Proof + rw[divisors_def, EXTENSION] +QED + +(* Theorem: divisors n = {} <=> n = 0 *) +(* Proof: + By EXTENSION, this is to show: + (1) divisors n = {} ==> n = 0 + By contradiction, suppose n <> 0. + Then 1 IN (divisors n) by divisors_has_1 + This contradicts divisors n = {} by MEMBER_NOT_EMPTY + (2) n = 0 ==> divisors n = {} + This is true by divisors_0 +*) +Theorem divisors_eq_empty: + !n. divisors n = {} <=> n = 0 +Proof + rw[EQ_IMP_THM] >- + metis_tac[divisors_has_1, MEMBER_NOT_EMPTY, NOT_ZERO] >> + simp[divisors_0] +QED (* Idea: a method to evaluate divisors. *) -(* Theorem: divisors n = - if n = 0 then {0} - else IMAGE (\j. if (j + 1) divides n then j + 1 else 1) (count n) *) +(* Theorem: divisors n = IMAGE (\j. if (j + 1) divides n then j + 1 else 1) (count n) *) (* Proof: + Let f = \j. if (j + 1) divides n then j + 1 else 1. If n = 0, divisors 0 - = {d | d <= 0 /\ d divides 0} by divisors_def - = {0} by d <= 0, and ALL_DIVIDES_0 + = {d | 0 < d /\ d <= 0 /\ d divides 0} by divisors_def + = {} by 0 < d /\ d <= 0 + = IMAGE f {} by IMAGE_EMPTY + = IMAGE f (count 0) by COUNT_0 If n <> 0, divisors n - = {d | d <= n /\ d divides n} by divisors_def - = {d | d <> 0 /\ d <= n /\ d divides n} - by ZERO_DIVIDES + = {d | 0 < d /\ d <= n /\ d divides n} by divisors_def + = {d | d <> 0 /\ d <= n /\ d divides n} by 0 < d = {k + 1 | (k + 1) <= n /\ (k + 1) divides n} - by num_CASES, d <> 0 - = {k + 1 | k < n /\ (k + 1) divides n} - by arithmetic - = IMAGE (\j. if (j + 1) divides n then j + 1 else 1) {k | k < n} - by IMAGE_DEF - = IMAGE (\j. if (j + 1) divides n then j + 1 else 1) (count n) - by count_def + by num_CASES, d <> 0 + = {k + 1 | k < n /\ (k + 1) divides n} by arithmetic + = IMAGE f {k | k < n} by IMAGE_DEF + = IMAGE f (count n) by count_def *) Theorem divisors_eqn[compute]: - !n. divisors n = - if n = 0 then {0} - else IMAGE (\j. if (j + 1) divides n then j + 1 else 1) (count n) + !n. divisors n = IMAGE (\j. if (j + 1) divides n then j + 1 else 1) (count n) Proof (rw[divisors_def, EXTENSION, EQ_IMP_THM] >> rw[]) >> - `x <> 0` by metis_tac[ZERO_DIVIDES] >> - `?k. x = SUC k` by metis_tac[num_CASES] >> + `?k. x = SUC k` by metis_tac[num_CASES, NOT_ZERO] >> qexists_tac `k` >> fs[ADD1] QED @@ -1058,161 +1122,319 @@ QED > EVAL ``divisors 9``; = {9; 3; 1}: thm *) +(* Idea: each factor of a product divides the product. *) + +(* Theorem: 0 < n /\ n = p * q ==> p IN divisors n /\ q IN divisors n *) +(* Proof: + Note 0 < p /\ 0 < q by MULT_EQ_0 + so p <= n /\ q <= n by arithmetic + and p divides n by divides_def + and q divides n by divides_def, MULT_COMM + ==> p IN divisors n /\ + q IN divisors n by divisors_element_alt, 0 < n +*) +Theorem divisors_has_factor: + !n p q. 0 < n /\ n = p * q ==> p IN divisors n /\ q IN divisors n +Proof + (rw[divisors_element_alt] >> metis_tac[MULT_EQ_0, NOT_ZERO]) +QED + (* Idea: when factor divides, its cofactor also divides. *) -(* Theorem: 0 < n /\ d IN divisors n ==> (n DIV d) IN divisors n *) +(* Theorem: d IN divisors n ==> (n DIV d) IN divisors n *) (* Proof: - Note d <= n /\ d divides n by divisors_def - so 0 < d by ZERO_DIVIDES - and n DIV d <= n by DIV_LESS_EQ, 0 < d - and n DIV d divides n by DIVIDES_COFACTOR, 0 < d + Note 0 < d /\ d <= n /\ d divides n by divisors_def + and 0 < n by 0 < d /\ d <= n + so 0 < n DIV d by DIV_POS, 0 < n + and n DIV d <= n by DIV_LESS_EQ, 0 < d + and n DIV d divides n by DIVIDES_COFACTOR, 0 < d + so (n DIV d) IN divisors n by divisors_def *) -Theorem divisors_cofactor: - !n d. 0 < n /\ d IN divisors n ==> (n DIV d) IN divisors n +Theorem divisors_has_cofactor: + !n d. d IN divisors n ==> (n DIV d) IN divisors n Proof simp [divisors_def] >> ntac 3 strip_tac >> - `0 < d` by metis_tac[ZERO_DIVIDES, NOT_ZERO] >> - rw[DIV_LESS_EQ, DIVIDES_COFACTOR] + `0 < n` by decide_tac >> + rw[DIV_POS, DIV_LESS_EQ, DIVIDES_COFACTOR] QED -(* Theorem: 0 < n ==> ((divisors n) DELETE n = {m | m < n /\ m divides n}) *) +(* Theorem: (divisors n) DELETE n = {m | 0 < m /\ m < n /\ m divides n} *) (* Proof: (divisors n) DELETE n - = {m | m <= n /\ m divides n} DELETE n by divisors_def - = {m | m <= n /\ m divides n} DIFF {n} by DELETE_DEF - = {m | m <> n /\ m <= n /\ m divides n} by IN_DIFF - = {m | m < n /\ m divides n} by LESS_OR_EQ -*) -val divisors_delete_last = store_thm( - "divisors_delete_last", - ``!n. 0 < n ==> ((divisors n) DELETE n = {m | m < n /\ m divides n})``, - rw[divisors_def, EXTENSION, EQ_IMP_THM]); - -(* Theorem: 0 < n ==> !d. d IN (divisors n) ==> 0 < d *) -(* Proof: - Since d IN (divisors n), d divides n by divisors_element - By contradiction, if d = 0, then n = 0 by ZERO_DIVIDES - This contradicts 0 < n. -*) -val divisors_nonzero = store_thm( - "divisors_nonzero", - ``!n. 0 < n ==> !d. d IN (divisors n) ==> 0 < d``, - metis_tac[divisors_element, ZERO_DIVIDES, NOT_ZERO_LT_ZERO]); - -(* Theorem: 0 < n ==> !d. d IN divisors n ==> n DIV d IN divisors n *) -(* Proof: - By divisors_element, this is to show: - 0 < n /\ d <= n /\ d divides n ==> n DIV d <= n /\ n DIV d divides n - Since 0 < n /\ d divides n ==> 0 < d by divisor_pos - so n = (n DIV d) * d by DIVIDES_EQN, 0 < d - = d * (n DIV d) by MULT_COMM - Hence (n DIV d) divides n by divides_def - and (n DIV d) <= n by DIVIDES_LE, 0 < n -*) -val divisors_has_cofactor = store_thm( - "divisors_has_cofactor", - ``!n. 0 < n ==> !d. d IN divisors n ==> n DIV d IN divisors n``, - rewrite_tac[divisors_element] >> - ntac 4 strip_tac >> - `0 < d` by metis_tac[divisor_pos] >> - `n = (n DIV d) * d` by rw[GSYM DIVIDES_EQN] >> - `_ = d * (n DIV d)` by rw[MULT_COMM] >> - metis_tac[divides_def, DIVIDES_LE]); - -(* Theorem: divisors n SUBSET upto n *) -(* Proof: by divisors_def, SUBSET_DEF *) -val divisors_subset_upto = store_thm( - "divisors_subset_upto", - ``!n. divisors n SUBSET upto n``, - rw[divisors_def, SUBSET_DEF]); - -(* Theorem: 0 < n ==> (divisors n) SUBSET (natural n) *) -(* Proof: - By SUBSET_DEF, this is to show: - x IN (divisors n) ==> x IN (natural n) - Since x IN (divisors n) - ==> x <= n /\ x divides n by divisors_element - ==> x <= n /\ 0 < x since n <> 0, so x <> 0 by ZERO_DIVIDES - ==> x IN (natural n) by natural_element -*) -val divisors_subset_natural = store_thm( - "divisors_subset_natural", - ``!n. 0 < n ==> (divisors n) SUBSET (natural n)``, - rw[divisors_element, natural_element, SUBSET_DEF] >> - metis_tac[ZERO_DIVIDES, NOT_ZERO_LT_ZERO]); - -(* Theorem: FINITE (divisors n) *) -(* Proof: - Since (divisors n) SUBSET count (SUC n) by divisors_subset_upto - and FINITE (count (SUC n)) by FINITE_COUNT - so FINITE (divisors n) by SUBSET_FINITE + = {m | 0 < m /\ m <= n /\ m divides n} DELETE n by divisors_def + = {m | 0 < m /\ m <= n /\ m divides n} DIFF {n} by DELETE_DEF + = {m | 0 < m /\ m <> n /\ m <= n /\ m divides n} by IN_DIFF + = {m | 0 < m /\ m < n /\ m divides n} by LESS_OR_EQ *) -val divisors_finite = store_thm( - "divisors_finite", - ``!n. FINITE (divisors n)``, - metis_tac[divisors_subset_upto, SUBSET_FINITE, FINITE_COUNT]); +Theorem divisors_delete_last: + !n. (divisors n) DELETE n = {m | 0 < m /\ m < n /\ m divides n} +Proof + rw[divisors_def, EXTENSION, EQ_IMP_THM] +QED -(* Theorem: divisors 0 = {0} *) -(* Proof: divisors_def *) -val divisors_0 = store_thm( - "divisors_0", - ``divisors 0 = {0}``, - rw[divisors_def]); +(* Theorem: d IN (divisors n) ==> 0 < d *) +(* Proof: by divisors_def. *) +Theorem divisors_nonzero: + !n d. d IN (divisors n) ==> 0 < d +Proof + simp[divisors_def] +QED -(* Theorem: divisors 1 = {1} *) -(* Proof: divisors_def *) -val divisors_1 = store_thm( - "divisors_1", - ``divisors 1 = {1}``, - rw[divisors_def, EXTENSION]); +(* Theorem: (divisors n) SUBSET (natural n) *) +(* Proof: + By SUBSET_DEF, this is to show: + x IN (divisors n) ==> x IN (natural n) + x IN (divisors n) + ==> 0 < x /\ x <= n /\ x divides n by divisors_element + ==> 0 < x /\ x <= n + ==> x IN (natural n) by natural_element +*) +Theorem divisors_subset_natural: + !n. (divisors n) SUBSET (natural n) +Proof + rw[divisors_element, natural_element, SUBSET_DEF] +QED -(* Theorem: 0 IN divisors n <=> (n = 0) *) +(* Theorem: FINITE (divisors n) *) (* Proof: - 0 IN divisors n - <=> 0 <= n /\ 0 divides n by divisors_element - <=> n = 0 by ZERO_DIVIDES + Since (divisors n) SUBSET (natural n) by divisors_subset_natural + and FINITE (naturnal n) by natural_finite + so FINITE (divisors n) by SUBSET_FINITE *) -val divisors_has_0 = store_thm( - "divisors_has_0", - ``!n. 0 IN divisors n <=> (n = 0)``, - rw[divisors_element]); +Theorem divisors_finite: + !n. FINITE (divisors n) +Proof + metis_tac[divisors_subset_natural, natural_finite, SUBSET_FINITE] +QED -(* Theorem: 0 < n ==> BIJ (\d. n DIV d) (divisors n) (divisors n) *) +(* Theorem: BIJ (\d. n DIV d) (divisors n) (divisors n) *) (* Proof: By BIJ_DEF, INJ_DEF, SURJ_DEF, this is to show: (1) d IN divisors n ==> n DIV d IN divisors n - True by divisors_has_cofactor. + This is true by divisors_has_cofactor (2) d IN divisors n /\ d' IN divisors n /\ n DIV d = n DIV d' ==> d = d' - d IN divisors n ==> d divides n /\ 0 < d by divisors_element, divisor_pos - d' IN divisors n ==> d' divides n /\ 0 < d' by divisors_element, divisor_pos + d IN divisors n ==> d divides n /\ 0 < d by divisors_element + d' IN divisors n ==> d' divides n /\ 0 < d' by divisors_element + Also d IN divisors n ==> 0 < n by divisors_has_element Hence n = (n DIV d) * d and n = (n DIV d') * d' by DIVIDES_EQN giving (n DIV d) * d = (n DIV d') * d' - Now (n DIV d) <> 0, otherwise contradicts 0 < n by MULT + Now (n DIV d) <> 0, otherwise contradicts n <> 0 by MULT Hence d = d' by EQ_MULT_LCANCEL - (3) same as (1), true by divisors_has_cofactor. + (3) same as (1), true by divisors_has_cofactor (4) x IN divisors n ==> ?d. d IN divisors n /\ (n DIV d = x) - x IN divisors n ==> x divides n by divisors_element + Note x IN divisors n ==> x divides n by divisors_element + and 0 < n by divisors_has_element Let d = n DIV x. Then d IN divisors n by divisors_has_cofactor - and n DIV d = n DIV (n DIV x) = x by divide_by_cofactor + and n DIV d = n DIV (n DIV x) = x by divide_by_cofactor, 0 < n *) -val divisors_divisors_bij = store_thm( - "divisors_divisors_bij", - ``!n. 0 < n ==> BIJ (\d. n DIV d) (divisors n) (divisors n)``, +Theorem divisors_divisors_bij: + !n. (\d. n DIV d) PERMUTES divisors n +Proof rw[BIJ_DEF, INJ_DEF, SURJ_DEF] >- rw[divisors_has_cofactor] >- - (`n = (n DIV d) * d` by metis_tac[DIVIDES_EQN, divisors_element, divisor_pos] >> - `n = (n DIV d') * d'` by metis_tac[DIVIDES_EQN, divisors_element, divisor_pos] >> - `n DIV d <> 0` by metis_tac[MULT, NOT_ZERO_LT_ZERO] >> + (`n = (n DIV d) * d` by metis_tac[DIVIDES_EQN, divisors_element] >> + `n = (n DIV d') * d'` by metis_tac[DIVIDES_EQN, divisors_element] >> + `0 < n` by metis_tac[divisors_has_element] >> + `n DIV d <> 0` by metis_tac[MULT, NOT_ZERO] >> metis_tac[EQ_MULT_LCANCEL]) >- rw[divisors_has_cofactor] >> - metis_tac[divisors_element, divisors_has_cofactor, divide_by_cofactor]); + `0 < n` by metis_tac[divisors_has_element] >> + metis_tac[divisors_element, divisors_has_cofactor, divide_by_cofactor] +QED -(* -> divisors_divisors_bij; -val it = |- !n. 0 < n ==> (\d. n DIV d) PERMUTES divisors n: thm +(* ------------------------------------------------------------------------- *) +(* An upper bound for divisors. *) +(* ------------------------------------------------------------------------- *) + +(* Idea: if a divisor of n is less or equal to (SQRT n), its cofactor is more or equal to (SQRT n) *) + +(* Theorem: 0 < p /\ p divides n /\ p <= SQRT n ==> SQRT n <= (n DIV p) *) +(* Proof: + Let m = SQRT n, then p <= m. + By contradiction, suppose (n DIV p) < m. + Then n = (n DIV p) * p by DIVIDES_EQN, 0 < p + <= (n DIV p) * m by p <= m + < m * m by (n DIV p) < m + <= n by SQ_SQRT_LE + giving n < n, which is a contradiction. *) +Theorem divisor_le_cofactor_ge: + !n p. 0 < p /\ p divides n /\ p <= SQRT n ==> SQRT n <= (n DIV p) +Proof + rpt strip_tac >> + qabbrev_tac `m = SQRT n` >> + spose_not_then strip_assume_tac >> + `n = (n DIV p) * p` by rfs[DIVIDES_EQN] >> + `(n DIV p) * p <= (n DIV p) * m` by fs[] >> + `(n DIV p) * m < m * m` by fs[] >> + `m * m <= n` by simp[SQ_SQRT_LE, Abbr`m`] >> + decide_tac +QED + +(* Idea: if a divisor of n is greater than (SQRT n), its cofactor is less or equal to (SQRT n) *) + +(* Theorem: 0 < p /\ p divides n /\ SQRT n < p ==> (n DIV p) <= SQRT n *) +(* Proof: + Let m = SQRT n, then m < p. + By contradiction, suppose m < (n DIV p). + Let q = (n DIV p). + Then SUC m <= p, SUC m <= q by m < p, m < q + and n = q * p by DIVIDES_EQN, 0 < p + >= (SUC m) * (SUC m) by LESS_MONO_MULT2 + = (SUC m) ** 2 by EXP_2 + > n by SQRT_PROPERTY + which is a contradiction. +*) +Theorem divisor_gt_cofactor_le: + !n p. 0 < p /\ p divides n /\ SQRT n < p ==> (n DIV p) <= SQRT n +Proof + rpt strip_tac >> + qabbrev_tac `m = SQRT n` >> + spose_not_then strip_assume_tac >> + `n = (n DIV p) * p` by rfs[DIVIDES_EQN] >> + qabbrev_tac `q = n DIV p` >> + `SUC m <= p /\ SUC m <= q` by decide_tac >> + `(SUC m) * (SUC m) <= q * p` by simp[LESS_MONO_MULT2] >> + `n < (SUC m) * (SUC m)` by metis_tac[SQRT_PROPERTY, EXP_2] >> + decide_tac +QED + +(* Idea: for (divisors n), the map (\j. n DIV j) is injective. *) + +(* Theorem: INJ (\j. n DIV j) (divisors n) univ(:num) *) +(* Proof: + By INJ_DEF, this is to show: + (1) !x. x IN (divisors n) ==> (\j. n DIV j) x IN univ(:num) + True by types, n DIV j is a number, with type :num. + (2) !x y. x IN (divisors n) /\ y IN (divisors n) /\ n DIV x = n DIV y ==> x = y + Note x divides n /\ 0 < x by divisors_def + and y divides n /\ 0 < y by divisors_def + Let p = n DIV x, q = n DIV y. + Note 0 < n by divisors_has_element + then 0 < p, 0 < q by DIV_POS, 0 < n + Then n = p * x = q * y by DIVIDES_EQN, 0 < x, 0 < y + But p = q by given + so x = y by EQ_MULT_LCANCEL +*) +Theorem divisors_cofactor_inj: + !n. INJ (\j. n DIV j) (divisors n) univ(:num) +Proof + rw[INJ_DEF, divisors_def] >> + `n = n DIV j * j` by fs[GSYM DIVIDES_EQN] >> + `n = n DIV j' * j'` by fs[GSYM DIVIDES_EQN] >> + `0 < n` by fs[GSYM divisors_has_element] >> + metis_tac[EQ_MULT_LCANCEL, DIV_POS, NOT_ZERO] +QED + +(* Idea: an upper bound for CARD (divisors n). + +To prove: 0 < n ==> CARD (divisors n) <= 2 * SQRT n +Idea of proof: + Consider the two sets, + s = {x | x IN divisors n /\ x <= SQRT n} + t = {x | x IN divisors n /\ SQRT n <= x} + Note s SUBSET (natural (SQRT n)), so CARD s <= SQRT n. + Also t SUBSET (natural (SQRT n)), so CARD t <= SQRT n. + There is a bijection between the two parts: + BIJ (\j. n DIV j) s t + Now divisors n = s UNION t + CARD (divisors n) + = CARD s + CARD t - CARD (s INTER t) + <= CARD s + CARD t + <= SQRT n + SQRT n + = 2 * SQRT n + + The BIJ part will be quite difficult. + So the actual proof is a bit different. +*) + +(* Theorem: CARD (divisors n) <= 2 * SQRT n *) +(* Proof: + Let m = SQRT n, + d = divisors n, + s = {x | x IN d /\ x <= m}, + f = \j. n DIV j, + t = IMAGE f s. + + Claim: s SUBSET natural m + Proof: By SUBSET_DEF, this is to show: + x IN d /\ x <= m ==> ?y. x = SUC y /\ y < m + Note 0 < x by divisors_nonzero + Let y = PRE x. + Then x = SUC (PRE x) by SUC_PRE + and PRE x < x by PRE_LESS + so PRE x < m by inequality, x <= m + + Claim: BIJ f s t + Proof: Note s SUBSET d by SUBSET_DEF + and INJ f d univ(:num) by divisors_cofactor_inj + so INJ f s univ(:num) by INJ_SUBSET, SUBSET_REFL + ==> BIJ f s t by INJ_IMAGE_BIJ_ALT + + Claim: d = s UNION t + Proof: By EXTENSION, EQ_IMP_THM, this is to show: + (1) x IN divisors n ==> x <= m \/ ?j. x = n DIV j /\ j IN divisors n /\ j <= m + If x <= m, this is trivial. + Otherwise, m < x. + Let j = n DIV x. + Then x = n DIV (n DIV x) by divide_by_cofactor + and (n DIV j) IN divisors n by divisors_has_cofactor + and (n DIV j) <= m by divisor_gt_cofactor_le + (2) j IN divisors n ==> n DIV j IN divisors n + This is true by divisors_has_cofactor + + Now FINITE (natural m) by natural_finite + so FINITE s by SUBSET_FINITE + and FINITE t by IMAGE_FINITE + so CARD s <= m by CARD_SUBSET, natural_card + Also CARD t = CARD s by FINITE_BIJ_CARD + + CARD d <= CARD s + CARD t by CARD_UNION_LE, d = s UNION t + <= m + m by above + = 2 * m by arithmetic +*) +Theorem divisors_card_upper: + !n. CARD (divisors n) <= 2 * SQRT n +Proof + rpt strip_tac >> + qabbrev_tac `m = SQRT n` >> + qabbrev_tac `d = divisors n` >> + qabbrev_tac `s = {x | x IN d /\ x <= m}` >> + qabbrev_tac `f = \j. n DIV j` >> + qabbrev_tac `t = (IMAGE f s)` >> + `s SUBSET (natural m)` by + (rw[SUBSET_DEF, Abbr`s`] >> + `0 < x` by metis_tac[divisors_nonzero] >> + qexists_tac `PRE x` >> + simp[]) >> + `BIJ f s t` by + (simp[Abbr`t`] >> + irule INJ_IMAGE_BIJ_ALT >> + `s SUBSET d` by rw[SUBSET_DEF, Abbr`s`] >> + `INJ f d univ(:num)` by metis_tac[divisors_cofactor_inj] >> + metis_tac[INJ_SUBSET, SUBSET_REFL]) >> + `d = s UNION t` by + (rw[EXTENSION, Abbr`d`, Abbr`s`, Abbr`t`, Abbr`f`, EQ_IMP_THM] >| [ + (Cases_on `x <= m` >> simp[]) >> + qexists_tac `n DIV x` >> + `0 < x /\ x <= n /\ x divides n` by fs[divisors_element] >> + simp[divide_by_cofactor, divisors_has_cofactor] >> + `m < x` by decide_tac >> + simp[divisor_gt_cofactor_le, Abbr`m`], + simp[divisors_has_cofactor] + ]) >> + `FINITE (natural m)` by simp[natural_finite] >> + `FINITE s /\ FINITE t` by metis_tac[SUBSET_FINITE, IMAGE_FINITE] >> + `CARD s <= m` by metis_tac[CARD_SUBSET, natural_card] >> + `CARD t = CARD s` by metis_tac[FINITE_BIJ_CARD] >> + `CARD d <= CARD s + CARD t` by metis_tac[CARD_UNION_LE] >> + decide_tac +QED + +(* This is a remarkable result! *) + (* ------------------------------------------------------------------------- *) (* Gauss' Little Theorem *) @@ -1390,34 +1612,43 @@ val gcd_matches_bij_coprimes = store_thm( which is not possible. *) -(* Theorem: 0 < n ==> (divisors n = IMAGE (gcd n) (natural n)) *) +(* Theorem: divisors n = IMAGE (gcd n) (natural n) *) (* Proof: divisors n - = {d | d <= n /\ d divides n} by divisors_def - = {d | 0 < d /\ d <= n /\ d divides n} by divisor_pos + = {d | 0 < d /\ d <= n /\ d divides n} by divisors_def = {d | d IN (natural n) /\ d divides n} by natural_element = {d | d IN (natural n) /\ (gcd d n = d)} by divides_iff_gcd_fix = {d | d IN (natural n) /\ (gcd n d = d)} by GCD_SYM = {gcd n d | d | d IN (natural n)} by replacemnt = IMAGE (gcd n) (natural n) by IMAGE_DEF + The replacemnt requires: + d IN (natural n) ==> gcd n d IN (natural n) + d IN (natural n) ==> gcd n (gcd n d) = gcd n d + which are given below. Or, by divisors_def, natuarl_elemnt, IN_IMAGE, this is to show: - (1) 0 < n /\ x <= n /\ x divides n ==> ?x'. (x = gcd n x') /\ 0 < x' /\ x' <= n - Note x divides n ==> 0 < x by divisor_pos - Also x divides n ==> gcd x n = x by divides_iff_gcd_fix + (1) 0 < x /\ x <= n /\ x divides n ==> ?y. (x = gcd n y) /\ 0 < y /\ y <= n + Note x divides n ==> gcd x n = x by divides_iff_gcd_fix or gcd n x = x by GCD_SYM Take this x, and the result follows. - (2) 0 < n /\ 0 < x' /\ x' <= n ==> gcd n x' <= n /\ gcd n x' divides n - Note gcd n x' divides n by GCD_IS_GREATEST_COMMON_DIVISOR - and gcd n x' <= n by DIVIDES_LE, 0 < n. -*) -val divisors_eq_gcd_image = store_thm( - "divisors_eq_gcd_image", - ``!n. 0 < n ==> (divisors n = IMAGE (gcd n) (natural n))``, - rw_tac std_ss[divisors_def, GSPECIFICATION, EXTENSION, IN_IMAGE, natural_element, EQ_IMP_THM] >- - metis_tac[divisor_pos, divides_iff_gcd_fix, GCD_SYM] >- - metis_tac[GCD_IS_GREATEST_COMMON_DIVISOR, DIVIDES_LE] >> - metis_tac[GCD_IS_GREATEST_COMMON_DIVISOR]); + (2) 0 < y /\ y <= n ==> 0 < gcd n y /\ gcd n y <= n /\ gcd n y divides n + Note 0 < n by arithmetic + and gcd n y divides n by GCD_IS_GREATEST_COMMON_DIVISOR, 0 < n + and 0 < gcd n y by GCD_EQ_0, n <> 0 + and gcd n y <= n by DIVIDES_LE, 0 < n +*) +Theorem divisors_eq_gcd_image: + !n. divisors n = IMAGE (gcd n) (natural n) +Proof + rw_tac std_ss[divisors_def, GSPECIFICATION, EXTENSION, IN_IMAGE, natural_element, EQ_IMP_THM] >| [ + `0 < n` by decide_tac >> + metis_tac[divides_iff_gcd_fix, GCD_SYM], + metis_tac[GCD_EQ_0, NOT_ZERO], + `0 < n` by decide_tac >> + metis_tac[GCD_IS_GREATEST_COMMON_DIVISOR, DIVIDES_LE], + metis_tac[GCD_IS_GREATEST_COMMON_DIVISOR] + ] +QED (* Theorem: feq_class (gcd n) (natural n) d = gcd_matches n d *) (* Proof: @@ -1439,18 +1670,18 @@ val gcd_eq_equiv_class_fun = store_thm( ``!n. feq_class (gcd n) (natural n) = gcd_matches n``, rw[FUN_EQ_THM, gcd_eq_equiv_class]); -(* Theorem: 0 < n ==> (partition (feq (gcd n)) (natural n) = IMAGE (gcd_matches n) (divisors n)) *) +(* Theorem: partition (feq (gcd n)) (natural n) = IMAGE (gcd_matches n) (divisors n) *) (* Proof: partition (feq (gcd n)) (natural n) - = IMAGE (equiv_class (feq (gcd n)) (natural n)) (natural n) by partition_elements + = IMAGE (equiv_class (feq (gcd n)) (natural n)) (natural n) by partition_elements = IMAGE ((feq_class (gcd n) (natural n)) o (gcd n)) (natural n) by feq_class_fun = IMAGE ((gcd_matches n) o (gcd n)) (natural n) by gcd_eq_equiv_class_fun = IMAGE (gcd_matches n) (IMAGE (gcd n) (natural n)) by IMAGE_COMPOSE - = IMAGE (gcd_matches n) (divisors n) by divisors_eq_gcd_image, 0 < n + = IMAGE (gcd_matches n) (divisors n) by divisors_eq_gcd_image, 0 < n *) -val gcd_eq_partition_by_divisors = store_thm( - "gcd_eq_partition_by_divisors", - ``!n. 0 < n ==> (partition (feq (gcd n)) (natural n) = IMAGE (gcd_matches n) (divisors n))``, +Theorem gcd_eq_partition_by_divisors: + !n. partition (feq (gcd n)) (natural n) = IMAGE (gcd_matches n) (divisors n) +Proof rpt strip_tac >> qabbrev_tac `f = gcd n` >> qabbrev_tac `s = natural n` >> @@ -1459,7 +1690,8 @@ val gcd_eq_partition_by_divisors = store_thm( `_ = IMAGE ((gcd_matches n) o f) s` by rw[gcd_eq_equiv_class_fun, Abbr`f`, Abbr`s`] >> `_ = IMAGE (gcd_matches n) (IMAGE f s)` by rw[IMAGE_COMPOSE] >> `_ = IMAGE (gcd_matches n) (divisors n)` by rw[divisors_eq_gcd_image, Abbr`f`, Abbr`s`] >> - rw[]); + simp[] +QED (* Theorem: (feq (gcd n)) equiv_on (natural n) *) (* Proof: @@ -1485,64 +1717,38 @@ val sum_over_natural_by_gcd_partition = store_thm( (* Theorem: SIGMA f (natural n) = SIGMA (SIGMA f) (IMAGE (gcd_matches n) (divisors n)) *) (* Proof: - If n = 0, - LHS = SIGMA f (natural 0) - = SIGMA f {} by natural_0 - = 0 by SUM_IMAGE_EMPTY - RHS = SIGMA (SIGMA f) (IMAGE (gcd_matches 0) (divisors 0)) - = SIGMA (SIGMA f) (IMAGE (gcd_matches 0) {0}) by divisors_0 - = SIGMA (SIGMA f) {gcd_matches 0 0} by IMAGE_SING - = SIGMA (SIGMA f) {{}} by gcd_matches_0 - = SIGMA f {} by SUM_IMAGE_SING - = 0 = LHS by SUM_IMAGE_EMPTY - Otherwise 0 < n, SIGMA f (natural n) = SIGMA (SIGMA f) (partition (feq (gcd n)) (natural n)) by sum_over_natural_by_gcd_partition - = SIGMA (SIGMA f) (IMAGE (gcd_matches n) (divisors n)) by gcd_eq_partition_by_divisors, 0 < n + = SIGMA (SIGMA f) (IMAGE (gcd_matches n) (divisors n)) by gcd_eq_partition_by_divisors *) -val sum_over_natural_by_divisors = store_thm( - "sum_over_natural_by_divisors", - ``!f n. SIGMA f (natural n) = SIGMA (SIGMA f) (IMAGE (gcd_matches n) (divisors n))``, - rpt strip_tac >> - Cases_on `n = 0` >| [ - `natural n = {}` by rw_tac std_ss[natural_0] >> - `divisors n = {0}` by rw_tac std_ss[divisors_0] >> - `IMAGE (gcd_matches n) (divisors n) = {{}}` by rw[gcd_matches_0] >> - rw[SUM_IMAGE_SING], - rw[sum_over_natural_by_gcd_partition, gcd_eq_partition_by_divisors] - ]); +Theorem sum_over_natural_by_divisors: + !f n. SIGMA f (natural n) = SIGMA (SIGMA f) (IMAGE (gcd_matches n) (divisors n)) +Proof + simp[sum_over_natural_by_gcd_partition, gcd_eq_partition_by_divisors] +QED -(* Theorem: 0 < n ==> INJ (gcd_matches n) (divisors n) univ(num) *) +(* Theorem: INJ (gcd_matches n) (divisors n) univ(num) *) (* Proof: By INJ_DEF, this is to show: x IN divisors n /\ y IN divisors n /\ gcd_matches n x = gcd_matches n y ==> x = y - If n = 0, - then divisors n = {} by divisors_0 - hence trivially true. - Otherwise 0 < n, - Note x IN divisors n - ==> x <= n /\ x divides n by divisors_element - also y IN divisors n - ==> y <= n /\ y divides n by divisors_element - Hence (gcd x n = x) /\ (gcd y n = y) by divides_iff_gcd_fix - Since x divides n, 0 < x by divisor_pos, 0 < n - Giving x IN gcd_matches n x by gcd_matches_element - so x IN gcd_matches n y by gcd_matches n x = gcd_matches n y - with gcd x n = y by gcd_matches_element - Therefore y = gcd x n = x. -*) -val gcd_matches_from_divisors_inj = store_thm( - "gcd_matches_from_divisors_inj", - ``!n. INJ (gcd_matches n) (divisors n) univ(:num -> bool)``, + Note 0 < x /\ x <= n /\ x divides n by divisors_def + also 0 < y /\ y <= n /\ y divides n by divisors_def + Hence (gcd x n = x) /\ (gcd y n = y) by divides_iff_gcd_fix + ==> x IN gcd_matches n x by gcd_matches_element + so x IN gcd_matches n y by gcd_matches n x = gcd_matches n y + with gcd x n = y by gcd_matches_element + Therefore y = gcd x n = x. +*) +Theorem gcd_matches_from_divisors_inj: + !n. INJ (gcd_matches n) (divisors n) univ(:num -> bool) +Proof rw[INJ_DEF] >> - Cases_on `n = 0` >> - fs[divisors_0] >> - `0 < n` by decide_tac >> - `x <= n /\ x divides n /\ y <= n /\ y divides n` by metis_tac[divisors_element] >> + fs[divisors_def] >> `(gcd x n = x) /\ (gcd y n = y)` by rw[GSYM divides_iff_gcd_fix] >> - metis_tac[divisor_pos, gcd_matches_element]); + metis_tac[gcd_matches_element] +QED -(* Theorem: 0 < n ==> (CARD o (gcd_matches n) = CARD o (coprimes_by n)) *) +(* Theorem: CARD o (gcd_matches n) = CARD o (coprimes_by n) *) (* Proof: By composition and FUN_EQ_THM, this is to show: !x. CARD (gcd_matches n x) = CARD (coprimes_by n x) @@ -1584,8 +1790,9 @@ val gcd_matches_and_coprimes_by_same_size = store_thm( = CARD (coprimes_by n x) by composition, combinTheory.o_THM = CARD (if x divides n then coprimes (n DIV x) else {}) by coprimes_by_def, 0 < n If x divides n, - x <= n by DIVIDES_LE - so x IN (divisors n) by divisors_element + then x <= n by DIVIDES_LE + and 0 < x by divisor_pos, 0 < n + so x IN (divisors n) by divisors_element CARD o (coprimes_by n) x = CARD (coprimes (n DIV x)) = phi (n DIV x) by phi_def @@ -1598,38 +1805,34 @@ val gcd_matches_and_coprimes_by_same_size = store_thm( Hence the same function as: \d. phi (if d IN (divisors n) then n DIV d else 0) *) -val coprimes_by_with_card = store_thm( - "coprimes_by_with_card", - ``!n. 0 < n ==> (CARD o (coprimes_by n) = \d. phi (if d IN (divisors n) then n DIV d else 0))``, +Theorem coprimes_by_with_card: + !n. 0 < n ==> (CARD o (coprimes_by n) = \d. phi (if d IN (divisors n) then n DIV d else 0)) +Proof rw[coprimes_by_def, phi_def, divisors_def, FUN_EQ_THM] >> - metis_tac[DIVIDES_LE, coprimes_0]); + metis_tac[DIVIDES_LE, divisor_pos, coprimes_0] +QED -(* Theorem: 0 < n ==> !x. x IN (divisors n) ==> ((CARD o (coprimes_by n)) x = (\d. phi (n DIV d)) x) *) +(* Theorem: x IN (divisors n) ==> (CARD o (coprimes_by n)) x = (\d. phi (n DIV d)) x *) (* Proof: - Since x IN (divisors n) ==> x divides n by divisors_element + Since x IN (divisors n) ==> x divides n by divisors_element CARD o (coprimes_by n) x - = CARD (coprimes (n DIV x)) by coprimes_by_def - = phi (n DIV x) by phi_def + = CARD (coprimes (n DIV x)) by coprimes_by_def + = phi (n DIV x) by phi_def *) -val coprimes_by_divisors_card = store_thm( - "coprimes_by_divisors_card", - ``!n. 0 < n ==> !x. x IN (divisors n) ==> ((CARD o (coprimes_by n)) x = (\d. phi (n DIV d)) x)``, - rw[coprimes_by_def, phi_def, divisors_def]); +Theorem coprimes_by_divisors_card: + !n x. x IN (divisors n) ==> (CARD o (coprimes_by n)) x = (\d. phi (n DIV d)) x +Proof + rw[coprimes_by_def, phi_def, divisors_def] +QED (* SUM_IMAGE_CONG |- (s1 = s2) /\ (!x. x IN s2 ==> (f1 x = f2 x)) ==> (SIGMA f1 s1 = SIGMA f2 s2) *) -(* Theorem: n = SIGMA phi (divisors n) *) +(* Theorem: SIGMA phi (divisors n) = n *) (* Proof: - If n = 0, - SIGMA phi (divisors 0) - = SIGMA phi {0} by divisors_0 - = phi 0 by SUM_IMAGE_SING - = 0 by phi_0 - If n <> 0, 0 < n. Note INJ (gcd_matches n) (divisors n) univ(:num -> bool) by gcd_matches_from_divisors_inj - and (\d. n DIV d) PERMUTES (divisors n) by divisors_divisors_bij, 0 < n + and (\d. n DIV d) PERMUTES (divisors n) by divisors_divisors_bij n = CARD (natural n) by natural_card = SIGMA CARD (partition (feq (gcd n)) (natural n)) by partition_CARD = SIGMA CARD (IMAGE (gcd_matches n) (divisors n)) by gcd_eq_partition_by_divisors @@ -1638,13 +1841,10 @@ SUM_IMAGE_CONG |- (s1 = s2) /\ (!x. x IN s2 ==> (f1 x = f2 x)) ==> (SIGMA f1 s1 = SIGMA (\d. phi (n DIV d)) (divisors n) by SUM_IMAGE_CONG, coprimes_by_divisors_card = SIGMA phi (divisors n) by sum_image_by_permutation *) -val Gauss_little_thm = store_thm( - "Gauss_little_thm", - ``!n. n = SIGMA phi (divisors n)``, +Theorem Gauss_little_thm: + !n. SIGMA phi (divisors n) = n +Proof rpt strip_tac >> - Cases_on `n = 0` >- - rw[divisors_0, SUM_IMAGE_SING, phi_0] >> - `0 < n` by decide_tac >> `FINITE (natural n)` by rw[natural_finite] >> `(feq (gcd n)) equiv_on (natural n)` by rw[gcd_eq_equiv_on_natural] >> `INJ (gcd_matches n) (divisors n) univ(:num -> bool)` by rw[gcd_matches_from_divisors_inj] >> @@ -1657,7 +1857,8 @@ val Gauss_little_thm = store_thm( `_ = SIGMA (CARD o (coprimes_by n)) (divisors n)` by rw[gcd_matches_and_coprimes_by_same_size] >> `_ = SIGMA (\d. phi (n DIV d)) (divisors n)` by rw[SUM_IMAGE_CONG, coprimes_by_divisors_card] >> `_ = SIGMA phi (divisors n)` by metis_tac[sum_image_by_permutation] >> - rw[]); + decide_tac +QED (* This is a milestone theorem. *) @@ -2370,7 +2571,7 @@ val rec_phi_1 = store_thm( If n = 1, rec_phi 1 = 1 by rec_phi_1 = phi 1 by phi_1 - Othewise, + Othewise, 0 < n, 1 < n. Let s = {m | m < n /\ m divides n}. Note s SUBSET (count n) by SUBSET_DEF thus FINITE s by SUBSET_FINITE, FINITE_COUNT @@ -2379,6 +2580,7 @@ val rec_phi_1 = store_thm( Also n NOTIN s by EXTENSION and n INSERT s = {m | m <= n /\ m divides n} + = {m | 0 < m /\ m <= n /\ m divides n} by divisor_pos, 0 < n = divisors n by divisors_def, EXTENSION, LESS_OR_EQ rec_phi n @@ -2390,9 +2592,9 @@ val rec_phi_1 = store_thm( = (phi n + SIGMA phi s) - (SIGMA phi s) by DELETE_NON_ELEMENT = phi n by ADD_SUB *) -val rec_phi_eq_phi = store_thm( - "rec_phi_eq_phi", - ``!n. rec_phi n = phi n``, +Theorem rec_phi_eq_phi: + !n. rec_phi n = phi n +Proof completeInduct_on `n` >> Cases_on `n = 0` >- rw[rec_phi_0, phi_0] >> @@ -2407,12 +2609,13 @@ val rec_phi_eq_phi = store_thm( `s SUBSET (count n)` by rw[SUBSET_DEF] >> `FINITE s` by metis_tac[SUBSET_FINITE, FINITE_COUNT] >> `n NOTIN s` by rw[] >> - (`n INSERT s = divisors n` by (rw[divisors_def, EXTENSION] >> metis_tac[LESS_OR_EQ, DIVIDES_REFL])) >> + (`n INSERT s = divisors n` by (rw[divisors_def, EXTENSION] >> metis_tac[divisor_pos, LESS_OR_EQ, DIVIDES_REFL])) >> `n = SIGMA phi (divisors n)` by rw[Gauss_little_thm] >> `_ = phi n + SIGMA phi (s DELETE n)` by rw[GSYM SUM_IMAGE_THM] >> `_ = phi n + t` by metis_tac[DELETE_NON_ELEMENT] >> `rec_phi n = n - t` by metis_tac[rec_phi_def] >> - decide_tac); + decide_tac +QED (* ------------------------------------------------------------------------- *) @@ -2434,8 +2637,8 @@ val rec_phi_eq_phi = store_thm( x - 1 = y - 1 by above Hence x = y by CANCEL_SUB *) -val coprimes_from_notone_inj = store_thm( - "coprimes_from_notone_inj", +val coprimes_from_not_1_inj = store_thm( + "coprimes_from_not_1_inj", ``INJ (coprimes) (univ(:num) DIFF {1}) univ(:num -> bool)``, rw[INJ_DEF] >> Cases_on `x = 0` >- @@ -2447,48 +2650,36 @@ val coprimes_from_notone_inj = store_thm( decide_tac); (* Not very useful. *) -(* Theorem: divisors n = IMAGE (gcd n) (upto n) *) +(* Here is group of related theorems for (divisors n): + divisors_eq_image_gcd_upto + divisors_eq_image_gcd_count + divisors_eq_image_gcd_natural + + This first one is proved independently, then the second and third are derived. + Of course, the best is the third one, which is now divisors_eq_gcd_image (above) + Here, I rework all proofs of these three from divisors_eq_gcd_image, + so divisors_eq_image_gcd_natural = divisors_eq_gcd_image. +*) + +(* Theorem: 0 < n ==> divisors n = IMAGE (gcd n) (upto n) *) (* Proof: + Note gcd n 0 = n by GCD_0 + and n IN divisors n by divisors_has_last, 0 < n divisors n - = {d | d <= n /\ d divides n} by divisors_def - = {d | d <= n /\ (gcd d n = d)} by divides_iff_gcd_fix - = {d | d <= n /\ (gcd n d = d)} by GCD_SYM - = {gcd n d | d | d <= n} by replacemnt - = IMAGE (gcd n) {d | d <= n} by IMAGE_DEF - = IMAGE (gcd n) (count (SUC n)) by count_def - = IMAGE (gcd n) (upto n) by notation - - By divisors_def, IN_IMAGE and EXTENSION, this is to show: - (1) x <= n /\ x divides n ==> ?x'. (x = gcd n x') /\ x' < SUC n - x <= n ==> x < SUC n by LESS_EQ_IMP_LESS_SUC - x divides n ==> x = gcd x n by divides_iff_gcd_fix - = gcd n x by GCD_SYM - (2) x' < SUC n ==> gcd n x' <= n /\ gcd n x' divides n - gcd n x' divides n by GCD_IS_GREATEST_COMMON_DIVISOR - If n = 0, x' < 1. - That is, x' = 0 by arithmetic - so gcd 0 0 = 0 <= 0 by GCD_0R - and 0 divides 0 by ZERO_DIVIDES - If n <> 0, 0 < n. - gcd n x' divides n - ==> gcd n x' <= n by DIVIDES_LE -*) -val divisors_eq_image_gcd_upto = store_thm( - "divisors_eq_image_gcd_upto", - ``!n. divisors n = IMAGE (gcd n) (upto n)``, - rw[divisors_def, EXTENSION, EQ_IMP_THM] >| [ - `x < SUC n` by decide_tac >> - metis_tac[divides_iff_gcd_fix, GCD_SYM], - Cases_on `n = 0` >| [ - `x' = 0` by decide_tac >> - `gcd 0 0 = 0` by rw[GCD_0R] >> - rw[], - `0 < n` by decide_tac >> - `(gcd n x') divides n` by rw[GCD_IS_GREATEST_COMMON_DIVISOR] >> - rw[DIVIDES_LE] - ], - rw[GCD_IS_GREATEST_COMMON_DIVISOR] - ]); + = (gcd n 0) INSERT (divisors n) by ABSORPTION + = (gcd n 0) INSERT (IMAGE (gcd n) (natural n)) by divisors_eq_gcd_image + = IMAGE (gcd n) (0 INSERT (natural n)) by IMAGE_INSERT + = IMAGE (gcd n) (upto n) by upto_by_natural +*) +Theorem divisors_eq_image_gcd_upto: + !n. 0 < n ==> divisors n = IMAGE (gcd n) (upto n) +Proof + rpt strip_tac >> + `IMAGE (gcd n) (upto n) = IMAGE (gcd n) (0 INSERT natural n)` by simp[upto_by_natural] >> + `_ = (gcd n 0) INSERT (IMAGE (gcd n) (natural n))` by fs[] >> + `_ = n INSERT (divisors n)` by fs[divisors_eq_gcd_image] >> + metis_tac[divisors_has_last, ABSORPTION] +QED (* Theorem: (feq (gcd n)) equiv_on (upto n) *) (* Proof: @@ -2500,18 +2691,18 @@ val gcd_eq_equiv_on_upto = store_thm( ``!n. (feq (gcd n)) equiv_on (upto n)``, rw[feq_equiv]); -(* Theorem: partition (feq (gcd n)) (upto n) = IMAGE (preimage (gcd n) (upto n)) (divisors n) *) +(* Theorem: 0 < n ==> partition (feq (gcd n)) (upto n) = IMAGE (preimage (gcd n) (upto n)) (divisors n) *) (* Proof: Let f = gcd n, s = upto n. partition (feq f) s = IMAGE (preimage f s o f) s by feq_partition = IMAGE (preimage f s) (IMAGE f s) by IMAGE_COMPOSE = IMAGE (preimage f s) (IMAGE (gcd n) (upto n)) by expansion - = IMAGE (preimage f s) (divisors n) by divisors_eq_image_gcd_upto + = IMAGE (preimage f s) (divisors n) by divisors_eq_image_gcd_upto, 0 < n *) val gcd_eq_upto_partition_by_divisors = store_thm( "gcd_eq_upto_partition_by_divisors", - ``!n. partition (feq (gcd n)) (upto n) = IMAGE (preimage (gcd n) (upto n)) (divisors n)``, + ``!n. 0 < n ==> partition (feq (gcd n)) (upto n) = IMAGE (preimage (gcd n) (upto n)) (divisors n)``, rpt strip_tac >> qabbrev_tac `f = gcd n` >> qabbrev_tac `s = upto n` >> @@ -2531,23 +2722,29 @@ val sum_over_upto_by_gcd_partition = store_thm( ``!f n. SIGMA f (upto n) = SIGMA (SIGMA f) (partition (feq (gcd n)) (upto n))``, rw[feq_equiv, set_sigma_by_partition]); -(* Theorem: SIGMA f (upto n) = SIGMA (SIGMA f) (IMAGE (preimage (gcd n) (upto n)) (divisors n)) *) +(* Theorem: 0 < n ==> SIGMA f (upto n) = SIGMA (SIGMA f) (IMAGE (preimage (gcd n) (upto n)) (divisors n)) *) (* Proof: SIGMA f (upto n) = SIGMA (SIGMA f) (partition (feq (gcd n)) (upto n)) by sum_over_upto_by_gcd_partition - = SIGMA (SIGMA f) (IMAGE (preimage (gcd n) (upto n)) (divisors n)) by gcd_eq_upto_partition_by_divisors + = SIGMA (SIGMA f) (IMAGE (preimage (gcd n) (upto n)) (divisors n)) by gcd_eq_upto_partition_by_divisors, 0 < n *) val sum_over_upto_by_divisors = store_thm( "sum_over_upto_by_divisors", - ``!f n. SIGMA f (upto n) = SIGMA (SIGMA f) (IMAGE (preimage (gcd n) (upto n)) (divisors n))``, + ``!f n. 0 < n ==> SIGMA f (upto n) = SIGMA (SIGMA f) (IMAGE (preimage (gcd n) (upto n)) (divisors n))``, rw[sum_over_upto_by_gcd_partition, gcd_eq_upto_partition_by_divisors]); (* Similar results based on count *) -(* Theorem: 0 < n ==> (divisors n = IMAGE (gcd n) (count n)) *) +(* Theorem: divisors n = IMAGE (gcd n) (count n) *) (* Proof: + If n = 0, + LHS = divisors 0 = {} by divisors_0 + RHS = IMAGE (gcd 0) (count 0) + = IMAGE (gcd 0) {} by COUNT_0 + = {} = LHS by IMAGE_EMPTY + If n <> 0, 0 < n. divisors n - = IMAGE (gcd n) (upto n) by divisors_eq_image_gcd_upto + = IMAGE (gcd n) (upto n) by divisors_eq_image_gcd_upto, 0 < n = IMAGE (gcd n) (n INSERT (count n)) by upto_by_count = (gcd n n) INSERT (IMAGE (gcd n) (count n)) by IMAGE_INSERT = n INSERT (IMAGE (gcd n) (count n)) by GCD_REF @@ -2555,16 +2752,20 @@ val sum_over_upto_by_divisors = store_thm( = IMAGE (gcd n) (0 INSERT (count n)) by IMAGE_INSERT = IMAGE (gcd n) (count n) by IN_COUNT, ABSORPTION, 0 < n. *) -val divisors_eq_image_gcd_count = store_thm( - "divisors_eq_image_gcd_count", - ``!n. 0 < n ==> (divisors n = IMAGE (gcd n) (count n))``, +Theorem divisors_eq_image_gcd_count: + !n. divisors n = IMAGE (gcd n) (count n) +Proof rpt strip_tac >> + Cases_on `n = 0` >- + simp[divisors_0] >> + `0 < n` by decide_tac >> `divisors n = IMAGE (gcd n) (upto n)` by rw[divisors_eq_image_gcd_upto] >> `_ = IMAGE (gcd n) (n INSERT (count n))` by rw[upto_by_count] >> `_ = n INSERT (IMAGE (gcd n) (count n))` by rw[GCD_REF] >> `_ = (gcd n 0) INSERT (IMAGE (gcd n) (count n))` by rw[GCD_0R] >> `_ = IMAGE (gcd n) (0 INSERT (count n))` by rw[] >> - metis_tac[IN_COUNT, ABSORPTION]); + metis_tac[IN_COUNT, ABSORPTION] +QED (* Theorem: (feq (gcd n)) equiv_on (count n) *) (* Proof: @@ -2576,24 +2777,25 @@ val gcd_eq_equiv_on_count = store_thm( ``!n. (feq (gcd n)) equiv_on (count n)``, rw[feq_equiv]); -(* Theorem: 0 < n ==> (partition (feq (gcd n)) (count n) = IMAGE (preimage (gcd n) (count n)) (divisors n)) *) +(* Theorem: partition (feq (gcd n)) (count n) = IMAGE (preimage (gcd n) (count n)) (divisors n) *) (* Proof: Let f = gcd n, s = count n. partition (feq f) s = IMAGE (preimage f s o f) s by feq_partition = IMAGE (preimage f s) (IMAGE f s) by IMAGE_COMPOSE = IMAGE (preimage f s) (IMAGE (gcd n) (count n)) by expansion - = IMAGE (preimage f s) (divisors n) by divisors_eq_image_gcd_count, 0 < n + = IMAGE (preimage f s) (divisors n) by divisors_eq_image_gcd_count *) -val gcd_eq_count_partition_by_divisors = store_thm( - "gcd_eq_count_partition_by_divisors", - ``!n. 0 < n ==> (partition (feq (gcd n)) (count n) = IMAGE (preimage (gcd n) (count n)) (divisors n))``, +Theorem gcd_eq_count_partition_by_divisors: + !n. partition (feq (gcd n)) (count n) = IMAGE (preimage (gcd n) (count n)) (divisors n) +Proof rpt strip_tac >> qabbrev_tac `f = gcd n` >> qabbrev_tac `s = count n` >> `partition (feq f) s = IMAGE (preimage f s o f) s` by rw[feq_partition] >> `_ = IMAGE (preimage f s) (IMAGE f s)` by rw[IMAGE_COMPOSE] >> - rw[divisors_eq_image_gcd_count, Abbr`f`, Abbr`s`]); + rw[divisors_eq_image_gcd_count, Abbr`f`, Abbr`s`] +QED (* Theorem: SIGMA f (count n) = SIGMA (SIGMA f) (partition (feq (gcd n)) (count n)) *) (* Proof: @@ -2607,108 +2809,124 @@ val sum_over_count_by_gcd_partition = store_thm( ``!f n. SIGMA f (count n) = SIGMA (SIGMA f) (partition (feq (gcd n)) (count n))``, rw[feq_equiv, set_sigma_by_partition]); -(* Theorem: 0 < n ==> (SIGMA f (count n) = SIGMA (SIGMA f) (IMAGE (preimage (gcd n) (count n)) (divisors n))) *) +(* Theorem: SIGMA f (count n) = SIGMA (SIGMA f) (IMAGE (preimage (gcd n) (count n)) (divisors n)) *) (* Proof: SIGMA f (count n) = SIGMA (SIGMA f) (partition (feq (gcd n)) (count n)) by sum_over_count_by_gcd_partition = SIGMA (SIGMA f) (IMAGE (preimage (gcd n) (count n)) (divisors n)) by gcd_eq_count_partition_by_divisors *) -val sum_over_count_by_divisors = store_thm( - "sum_over_count_by_divisors", - ``!f n. 0 < n ==> (SIGMA f (count n) = SIGMA (SIGMA f) (IMAGE (preimage (gcd n) (count n)) (divisors n)))``, - rw[sum_over_count_by_gcd_partition, gcd_eq_count_partition_by_divisors]); +Theorem sum_over_count_by_divisors: + !f n. SIGMA f (count n) = SIGMA (SIGMA f) (IMAGE (preimage (gcd n) (count n)) (divisors n)) +Proof + rw[sum_over_count_by_gcd_partition, gcd_eq_count_partition_by_divisors] +QED (* Similar results based on natural *) -(* Theorem: 0 < n ==> (divisors n = IMAGE (gcd n) (natural n)) *) +(* Theorem: divisors n = IMAGE (gcd n) (natural n) *) (* Proof: + If n = 0, + LHS = divisors 0 = {} by divisors_0 + RHS = IMAGE (gcd 0) (natural 0) + = IMAGE (gcd 0) {} by natural_0 + = {} = LHS by IMAGE_EMPTY + If n <> 0, 0 < n. divisors n - = IMAGE (gcd n) (upto n) by divisors_eq_image_gcd_upto - = IMAGE (gcd n) (0 INSERT natural n) by upto_by_natural + = IMAGE (gcd n) (upto n) by divisors_eq_image_gcd_upto, 0 < n + = IMAGE (gcd n) (0 INSERT natural n) by upto_by_natural = (gcd 0 n) INSERT (IMAGE (gcd n) (natural n)) by IMAGE_INSERT = n INSERT (IMAGE (gcd n) (natural n)) by GCD_0L = (gcd n n) INSERT (IMAGE (gcd n) (natural n)) by GCD_REF = IMAGE (gcd n) (n INSERT (natural n)) by IMAGE_INSERT = IMAGE (gcd n) (natural n) by natural_has_last, ABSORPTION, 0 < n. *) -val divisors_eq_image_gcd_natural = store_thm( - "divisors_eq_image_gcd_natural", - ``!n. 0 < n ==> (divisors n = IMAGE (gcd n) (natural n))``, +Theorem divisors_eq_image_gcd_natural: + !n. divisors n = IMAGE (gcd n) (natural n) +Proof rpt strip_tac >> + Cases_on `n = 0` >- + simp[divisors_0, natural_0] >> + `0 < n` by decide_tac >> `divisors n = IMAGE (gcd n) (upto n)` by rw[divisors_eq_image_gcd_upto] >> `_ = IMAGE (gcd n) (0 INSERT (natural n))` by rw[upto_by_natural] >> `_ = n INSERT (IMAGE (gcd n) (natural n))` by rw[GCD_0L] >> `_ = (gcd n n) INSERT (IMAGE (gcd n) (natural n))` by rw[GCD_REF] >> `_ = IMAGE (gcd n) (n INSERT (natural n))` by rw[] >> - metis_tac[natural_has_last, ABSORPTION]); + metis_tac[natural_has_last, ABSORPTION] +QED +(* This is the same as divisors_eq_gcd_image *) -(* Theorem: 0 < n ==> (partition (feq (gcd n)) (natural n) = IMAGE (preimage (gcd n) (natural n)) (divisors n)) *) +(* Theorem: partition (feq (gcd n)) (natural n) = IMAGE (preimage (gcd n) (natural n)) (divisors n) *) (* Proof: Let f = gcd n, s = natural n. partition (feq f) s = IMAGE (preimage f s o f) s by feq_partition = IMAGE (preimage f s) (IMAGE f s) by IMAGE_COMPOSE = IMAGE (preimage f s) (IMAGE (gcd n) (natural n)) by expansion - = IMAGE (preimage f s) (divisors n) by divisors_eq_image_gcd_natural, 0 < n + = IMAGE (preimage f s) (divisors n) by divisors_eq_image_gcd_natural *) -val gcd_eq_natural_partition_by_divisors = store_thm( - "gcd_eq_natural_partition_by_divisors", - ``!n. 0 < n ==> (partition (feq (gcd n)) (natural n) = IMAGE (preimage (gcd n) (natural n)) (divisors n))``, +Theorem gcd_eq_natural_partition_by_divisors: + !n. partition (feq (gcd n)) (natural n) = IMAGE (preimage (gcd n) (natural n)) (divisors n) +Proof rpt strip_tac >> qabbrev_tac `f = gcd n` >> qabbrev_tac `s = natural n` >> `partition (feq f) s = IMAGE (preimage f s o f) s` by rw[feq_partition] >> `_ = IMAGE (preimage f s) (IMAGE f s)` by rw[IMAGE_COMPOSE] >> - rw[divisors_eq_image_gcd_natural, Abbr`f`, Abbr`s`]); + rw[divisors_eq_image_gcd_natural, Abbr`f`, Abbr`s`] +QED -(* Theorem: 0 < n ==> (SIGMA f (natural n) = SIGMA (SIGMA f) (IMAGE (preimage (gcd n) (natural n)) (divisors n))) *) +(* Theorem: SIGMA f (natural n) = SIGMA (SIGMA f) (IMAGE (preimage (gcd n) (natural n)) (divisors n)) *) (* Proof: SIGMA f (natural n) = SIGMA (SIGMA f) (partition (feq (gcd n)) (natural n)) by sum_over_natural_by_gcd_partition = SIGMA (SIGMA f) (IMAGE (preimage (gcd n) (natural n)) (divisors n)) by gcd_eq_natural_partition_by_divisors *) -val sum_over_natural_by_preimage_divisors = store_thm( - "sum_over_natural_by_preimage_divisors", - ``!f n. 0 < n ==> (SIGMA f (natural n) = SIGMA (SIGMA f) (IMAGE (preimage (gcd n) (natural n)) (divisors n)))``, - rw[sum_over_natural_by_gcd_partition, gcd_eq_natural_partition_by_divisors]); +Theorem sum_over_natural_by_preimage_divisors: + !f n. SIGMA f (natural n) = SIGMA (SIGMA f) (IMAGE (preimage (gcd n) (natural n)) (divisors n)) +Proof + rw[sum_over_natural_by_gcd_partition, gcd_eq_natural_partition_by_divisors] +QED -(* Theorem: (f 1 = g 1) /\ (!n. SIGMA f (divisors n) = SIGMA g (divisors n)) ==> (f = g) *) +(* Theorem: (f 0 = g 0) /\ (!n. SIGMA f (divisors n) = SIGMA g (divisors n)) ==> (f = g) *) (* Proof: By FUN_EQ_THM, this is to show: !x. f x = g x. By complete induction on x. Let s = divisors x, t = s DELETE x. - Then x IN s by divisors_has_last - and (s = x INSERT t) /\ x NOTIN t by INSERT_DELETE, IN_DELETE + If x = 0, f 0 = g 0 is true by given + Otherwise x <> 0. + Then x IN s by divisors_has_last, 0 < x + and s = x INSERT t /\ x NOTIN t by INSERT_DELETE, IN_DELETE Note FINITE s by divisors_finite so FINITE t by FINITE_DELETE Claim: SIGMA f t = SIGMA g t Proof: By SUM_IMAGE_CONG, this is to show: !z. z IN t ==> (f z = g z) - But z IN s <=> z <= x /\ z divides x by divisors_element - so z IN t <=> z < x /\ z divides x by IN_DELETE - ==> f z = g z by induction hypothesis + But z IN s <=> 0 < z /\ z <= x /\ z divides x by divisors_element + so z IN t <=> 0 < z /\ z < x /\ z divides x by IN_DELETE + ==> f z = g z by induction hypothesis, [1] Now SIGMA f s = SIGMA g s by implication or f x + SIGMA f t = g x + SIGMA g t by SUM_IMAGE_INSERT - or f x = g x by SIGMA f t = SIGMA g t + or f x = g x by [1], SIGMA f t = SIGMA g t *) Theorem sum_image_divisors_cong: - !f g. f 1 = g 1 /\ (!n. SIGMA f (divisors n) = SIGMA g (divisors n)) ==> - f = g + !f g. (f 0 = g 0) /\ (!n. SIGMA f (divisors n) = SIGMA g (divisors n)) ==> (f = g) Proof rw[FUN_EQ_THM] >> completeInduct_on `x` >> qabbrev_tac `s = divisors x` >> qabbrev_tac `t = s DELETE x` >> + (Cases_on `x = 0` >> simp[]) >> `x IN s` by rw[divisors_has_last, Abbr`s`] >> - `(s = x INSERT t) /\ x NOTIN t` by rw[Abbr`t`] >> - `SIGMA f t = SIGMA g t` - by (irule SUM_IMAGE_CONG >> simp[] >> - rw[divisors_element, Abbr`t`, Abbr`s`]) >> + `s = x INSERT t /\ x NOTIN t` by rw[Abbr`t`] >> + `SIGMA f t = SIGMA g t` by + ((irule SUM_IMAGE_CONG >> simp[]) >> + rw[divisors_element, Abbr`t`, Abbr`s`]) >> `FINITE t` by rw[divisors_finite, Abbr`t`, Abbr`s`] >> - `SIGMA f s = f x + SIGMA f t` by simp[SUM_IMAGE_INSERT] >> - `SIGMA g s = g x + SIGMA g t` by simp[SUM_IMAGE_INSERT] >> + `SIGMA f s = f x + SIGMA f t` by rw[SUM_IMAGE_INSERT] >> + `SIGMA g s = g x + SIGMA g t` by rw[SUM_IMAGE_INSERT] >> `SIGMA f s = SIGMA g s` by metis_tac[] >> decide_tac QED diff --git a/examples/algebra/lib/MobiusScript.sml b/examples/algebra/lib/MobiusScript.sml index 4d815bce28..d6ee80d8d6 100644 --- a/examples/algebra/lib/MobiusScript.sml +++ b/examples/algebra/lib/MobiusScript.sml @@ -77,16 +77,16 @@ open EulerTheory; sq_free_disjoint_even_odd |- !s. DISJOINT (even_sq_free s) (odd_sq_free s) Less Divisors of a number: - less_divisors_element |- !n x. x IN less_divisors n <=> x < n /\ x divides n + less_divisors_element |- !n x. x IN less_divisors n <=> 0 < x /\ x < n /\ x divides n less_divisors_0 |- less_divisors 0 = {} less_divisors_1 |- less_divisors 1 = {} - less_divisors_subset_divisors |- !n. less_divisors n SUBSET divisors n + less_divisors_subset_divisors + |- !n. less_divisors n SUBSET divisors n less_divisors_finite |- !n. FINITE (less_divisors n) less_divisors_prime |- !n. prime n ==> (less_divisors n = {1}) - less_divisors_has_one |- !n. 1 < n ==> 1 IN less_divisors n + less_divisors_has_1 |- !n. 1 < n ==> 1 IN less_divisors n less_divisors_nonzero |- !n x. x IN less_divisors n ==> 0 < x - less_divisors_has_cofactor |- !n. 0 < n ==> - !d. 1 < d /\ d IN less_divisors n ==> n DIV d IN less_divisors n + less_divisors_has_cofactor |- !n d. 1 < d /\ d IN less_divisors n ==> n DIV d IN less_divisors n Proper Divisors of a number: proper_divisors_element |- !n x. x IN proper_divisors n <=> 1 < x /\ x < n /\ x divides n @@ -94,10 +94,11 @@ open EulerTheory; proper_divisors_1 |- proper_divisors 1 = {} proper_divisors_subset |- !n. proper_divisors n SUBSET less_divisors n proper_divisors_finite |- !n. FINITE (proper_divisors n) - proper_divisors_not_one |- !n. 1 NOTIN proper_divisors n - proper_divisors_by_less_divisors |- !n. proper_divisors n = less_divisors n DELETE 1 + proper_divisors_not_1 |- !n. 1 NOTIN proper_divisors n + proper_divisors_by_less_divisors + |- !n. proper_divisors n = less_divisors n DELETE 1 proper_divisors_prime |- !n. prime n ==> (proper_divisors n = {}) - proper_divisors_has_cofactor |- !n d. d IN proper_divisors n ==> n DIV d IN proper_divisors n + proper_divisors_has_cofactor|- !n d. d IN proper_divisors n ==> n DIV d IN proper_divisors n proper_divisors_min_gt_1 |- !n. proper_divisors n <> {} ==> 1 < MIN_SET (proper_divisors n) proper_divisors_max_min |- !n. proper_divisors n <> {} ==> (MAX_SET (proper_divisors n) = n DIV MIN_SET (proper_divisors n)) /\ @@ -261,22 +262,30 @@ val sq_free_disjoint = store_thm( (* ------------------------------------------------------------------------- *) (* Define the prime divisors of a number *) -val prime_factors_def = Define` +val prime_factors_def = zDefine` prime_factors n = {p | prime p /\ p IN (divisors n)} `; +(* use zDefine as this cannot be computed. *) (* prime_divisors is used in triangle.hol *) (* Theorem: p IN prime_factors n <=> prime p /\ p <= n /\ p divides n *) -(* Proof: by prime_factors_def, divisors_def *) -val prime_factors_element = store_thm( - "prime_factors_element", - ``!n p. p IN prime_factors n <=> prime p /\ p <= n /\ p divides n``, - rw[prime_factors_def, divisors_def]); +(* Proof: + p IN prime_factors n + <=> prime p /\ p IN (divisors n) by prime_factors_def + <=> prime p /\ 0 < p /\ p <= n /\ p divides n by divisors_def + <=> prime p /\ p <= n /\ p divides n by PRIME_POS +*) +Theorem prime_factors_element: + !n p. p IN prime_factors n <=> prime p /\ p <= n /\ p divides n +Proof + rw[prime_factors_def, divisors_def] >> + metis_tac[PRIME_POS] +QED (* Theorem: (prime_factors n) SUBSET (divisors n) *) (* Proof: p IN (prime_factors n) - ==> p IN (divisors n) by prime_factors_def + ==> p IN (divisors n) by prime_factors_def Hence (prime_factors n) SUBSET (divisors n) by SUBSET_DEF *) val prime_factors_subset = store_thm( @@ -286,9 +295,9 @@ val prime_factors_subset = store_thm( (* Theorem: FINITE (prime_factors n) *) (* Proof: - Since (prime_factors n) SUBSET (divisors n) by prime_factors_subset - and FINITE (divisors n) by divisors_finite - Thus FINITE (prime_factors n) by SUBSET_FINITE + Since (prime_factors n) SUBSET (divisors n) by prime_factors_subset + and FINITE (divisors n) by divisors_finite + Thus FINITE (prime_factors n) by SUBSET_FINITE *) val prime_factors_finite = store_thm( "prime_factors_finite", @@ -386,11 +395,11 @@ val sq_free_disjoint_even_odd = store_thm( (* Overload the set of divisors less than n *) val _ = overload_on("less_divisors", ``\n. {x | x IN (divisors n) /\ x <> n}``); -(* Theorem: x IN (less_divisors n) <=> (x < n /\ x divides n) *) +(* Theorem: x IN (less_divisors n) <=> (0 < x /\ x < n /\ x divides n) *) (* Proof: by divisors_element. *) val less_divisors_element = store_thm( "less_divisors_element", - ``!n x. x IN (less_divisors n) <=> (x < n /\ x divides n)``, + ``!n x. x IN (less_divisors n) <=> (0 < x /\ x < n /\ x divides n)``, rw[divisors_element, EQ_IMP_THM]); (* Theorem: less_divisors 0 = {} *) @@ -450,36 +459,32 @@ val less_divisors_prime = store_thm( <=> 1 < n /\ 1 divides n by less_divisors_element <=> T by ONE_DIVIDES_ALL *) -val less_divisors_has_one = store_thm( - "less_divisors_has_one", +val less_divisors_has_1 = store_thm( + "less_divisors_has_1", ``!n. 1 < n ==> 1 IN (less_divisors n)``, rw[less_divisors_element]); (* Theorem: x IN (less_divisors n) ==> 0 < x *) -(* Proof: - Since x IN (less_divisors n), - x < n /\ x divides n by less_divisors_element - By contradiction, if x = 0, then n = 0 by ZERO_DIVIDES - This contradicts x < n. -*) +(* Proof: by less_divisors_element. *) val less_divisors_nonzero = store_thm( "less_divisors_nonzero", ``!n x. x IN (less_divisors n) ==> 0 < x``, - metis_tac[less_divisors_element, ZERO_DIVIDES, NOT_ZERO_LT_ZERO]); + rw[less_divisors_element]); -(* Theorem: 0 < n ==> !d. 1 < d /\ d IN (less_divisors n) ==> (n DIV d) IN (less_divisors n) *) +(* Theorem: 1 < d /\ d IN (less_divisors n) ==> (n DIV d) IN (less_divisors n) *) (* Proof: d IN (less_divisors n) - ==> d IN (divisors n) by notation + ==> d IN (divisors n) by less_divisors_subset_divisors ==> (n DIV d) IN (divisors n) by divisors_has_cofactor + Note 0 < d /\ d <= n ==> 0 < n by divisors_element Also n DIV d < n by DIV_LESS, 0 < n /\ 1 < d thus n DIV d <> n by LESS_NOT_EQ Hence (n DIV d) IN (less_divisors n) by notation *) val less_divisors_has_cofactor = store_thm( "less_divisors_has_cofactor", - ``!n. 0 < n ==> !d. 1 < d /\ d IN (less_divisors n) ==> (n DIV d) IN (less_divisors n)``, - rw[divisors_has_cofactor, DIV_LESS, LESS_NOT_EQ]); + ``!n d. 1 < d /\ d IN (less_divisors n) ==> (n DIV d) IN (less_divisors n)``, + rw[divisors_has_cofactor, divisors_element, DIV_LESS, LESS_NOT_EQ]); (* ------------------------------------------------------------------------- *) (* Proper Divisors of a number. *) @@ -491,18 +496,14 @@ val _ = overload_on("proper_divisors", ``\n. {x | x IN (divisors n) /\ x <> 1 /\ (* Theorem: x IN (proper_divisors n) <=> (1 < x /\ x < n /\ x divides n) *) (* Proof: Since x IN (divisors n) - ==> x <= n /\ x divides n by divisors_element + ==> 0 < x /\ x <= n /\ x divides n by divisors_element Since x <= n but x <> n, x < n. - If x = 0, x divides n ==> n = 0 by ZERO_DIVIDES - But x <> n, so x <> 0. With x <> 0 /\ x <> 1 ==> 1 < x. *) val proper_divisors_element = store_thm( "proper_divisors_element", ``!n x. x IN (proper_divisors n) <=> (1 < x /\ x < n /\ x divides n)``, - rw[divisors_element, EQ_IMP_THM] >> - `x <> 0` by metis_tac[ZERO_DIVIDES] >> - decide_tac); + rw[divisors_element, EQ_IMP_THM]); (* Theorem: proper_divisors 0 = {} *) (* Proof: by proper_divisors_element. *) @@ -538,8 +539,8 @@ val proper_divisors_finite = store_thm( (* Theorem: 1 NOTIN (proper_divisors n) *) (* Proof: proper_divisors_element *) -val proper_divisors_not_one = store_thm( - "proper_divisors_not_one", +val proper_divisors_not_1 = store_thm( + "proper_divisors_not_1", ``!n. 1 NOTIN (proper_divisors n)``, rw[proper_divisors_element]); @@ -668,7 +669,7 @@ val proper_divisors_max_min = store_thm( (* Theorem: 1 < n ==> (MIN_SET (less_divisors n) = 1) *) (* Proof: Let s = less_divisors n. - Since 1 < n ==> 1 IN s by less_divisors_has_one + Since 1 < n ==> 1 IN s by less_divisors_has_1 so s <> {} by MEMBER_NOT_EMPTY and !y. y IN s ==> 0 < y by less_divisors_nonzero or !y. y IN s ==> 1 <= y by LESS_EQ @@ -677,7 +678,7 @@ val proper_divisors_max_min = store_thm( val less_divisors_min = store_thm( "less_divisors_min", ``!n. 1 < n ==> (MIN_SET (less_divisors n) = 1)``, - metis_tac[less_divisors_has_one, MEMBER_NOT_EMPTY, + metis_tac[less_divisors_has_1, MEMBER_NOT_EMPTY, MIN_SET_TEST, less_divisors_nonzero, LESS_EQ, ONE]); (* Theorem: MAX_SET (less_divisors n) <= n DIV 2 *) @@ -688,7 +689,7 @@ val less_divisors_min = store_thm( and 0 <= n DIV 2 is trivial. If s <> {}, Then n <> 0 /\ n <> 1 by less_divisors_0, less_divisors_1 - Note 1 IN s by less_divisors_has_one + Note 1 IN s by less_divisors_has_1 Consider t = s DELETE 1. Then t = proper_divisors n by proper_divisors_by_less_divisors If t = {}, @@ -720,7 +721,7 @@ Proof Cases_on `s = {}` >- rw[MAX_SET_EMPTY, Abbr`m`] >> `n <> 0 /\ n <> 1` by metis_tac[less_divisors_0, less_divisors_1] >> `1 < n` by decide_tac >> - `1 IN s` by rw[less_divisors_has_one, Abbr`s`] >> + `1 IN s` by rw[less_divisors_has_1, Abbr`s`] >> qabbrev_tac `t = proper_divisors n` >> `t = s DELETE 1` by rw[proper_divisors_by_less_divisors, Abbr`t`, Abbr`s`] >> Cases_on `t = {}` >| [ diff --git a/examples/algebra/lib/binomialScript.sml b/examples/algebra/lib/binomialScript.sml index e44596b774..e5419dbf38 100644 --- a/examples/algebra/lib/binomialScript.sml +++ b/examples/algebra/lib/binomialScript.sml @@ -190,9 +190,9 @@ val binomial_less_0 = store_thm( "binomial_less_0", ``!n k. n < k ==> (binomial n k = 0)``, Induct_on `n` >- - metis_tac[binomial_def, num_CASES, NOT_ZERO_LT_ZERO] >> + metis_tac[binomial_def, num_CASES, NOT_ZERO] >> rw[binomial_def] >> - `?h. k = SUC h` by metis_tac[SUC_NOT, NOT_ZERO_LT_ZERO, LESS_EQ_SUC, LESS_TRANS] >> + `?h. k = SUC h` by metis_tac[SUC_NOT, NOT_ZERO, SUC_EXISTS, LESS_TRANS] >> metis_tac[binomial_def, LESS_MONO_EQ, LESS_TRANS, LESS_SUC, ADD_0]); (* Theorem: C(n,0) = 1 *) @@ -312,7 +312,7 @@ val binomial_formula2 = store_thm( val binomial_formula3 = store_thm( "binomial_formula3", ``!n k. k <= n ==> (binomial n k = (FACT n) DIV ((FACT k) * (FACT (n - k))))``, - metis_tac[binomial_formula2, MULT_COMM, MULT_DIV, MULT_EQ_0, FACT_LESS, NOT_ZERO_LT_ZERO]); + metis_tac[binomial_formula2, MULT_COMM, MULT_DIV, MULT_EQ_0, FACT_LESS, NOT_ZERO]); (* Theorem alias. *) val binomial_fact = save_thm("binomial_fact", binomial_formula3); @@ -327,7 +327,7 @@ val binomial_fact = save_thm("binomial_fact", binomial_formula3); val binomial_n_k = store_thm( "binomial_n_k", ``!n k. k <= n ==> (binomial n k = (FACT n) DIV (FACT k) DIV (FACT (n - k)))``, - metis_tac[DIV_DIV_DIV_MULT, binomial_formula3, MULT_EQ_0, FACT_LESS, NOT_ZERO_LT_ZERO]); + metis_tac[DIV_DIV_DIV_MULT, binomial_formula3, MULT_EQ_0, FACT_LESS, NOT_ZERO]); (* Theorem: binomial n 1 = n *) (* Proof: @@ -402,7 +402,7 @@ val binomial_pos = store_thm( If part: (binomial n k = 0) ==> n < k By contradiction, suppose k <= n. Then 0 < binomial n k by binomial_pos - This contradicts binomial n k = 0 by NOT_ZERO_LT_ZERO + This contradicts binomial n k = 0 by NOT_ZERO Only-if part: n < k ==> (binomial n k = 0) This is true by binomial_less_0 *) @@ -412,7 +412,7 @@ val binomial_eq_0 = store_thm( rw[EQ_IMP_THM] >| [ spose_not_then strip_assume_tac >> `k <= n` by decide_tac >> - metis_tac[binomial_pos, NOT_ZERO_LT_ZERO], + metis_tac[binomial_pos, NOT_ZERO], rw[binomial_less_0] ]); @@ -592,7 +592,7 @@ val binomial_monotone = store_thm( `(k + 1) * binomial n (k + 1) = (n - k) * binomial n k` by rw[binomial_right_eqn] >> `HALF n <= n` by rw[DIV_LESS_EQ] >> `0 < binomial n k` by rw[binomial_pos] >> - `0 < binomial n (k + 1)` by metis_tac[MULT_0, MULT_EQ_0, NOT_ZERO_LT_ZERO] >> + `0 < binomial n (k + 1)` by metis_tac[MULT_0, MULT_EQ_0, NOT_ZERO] >> metis_tac[MULT_EQ_LESS_TO_MORE]); (* Theorem: binomial n k <= binomial n (HALF n) *) @@ -1217,7 +1217,7 @@ val binomial_product_identity = store_thm( `FACT (n - k) = binomial (n - k) (m - k) * (FACT (n - m) * FACT (m - k))` by metis_tac[binomial_formula2] >> `FACT n = FACT (n - m) * (FACT k * (FACT (m - k) * ((binomial m k) * (binomial n m))))` by metis_tac[MULT_ASSOC, MULT_COMM] >> `FACT n = FACT (n - m) * (FACT k * (FACT (m - k) * ((binomial n k) * (binomial (n - k) (m - k)))))` by metis_tac[MULT_ASSOC, MULT_COMM] >> - metis_tac[MULT_LEFT_CANCEL, FACT_LESS, NOT_ZERO_LT_ZERO]); + metis_tac[MULT_LEFT_CANCEL, FACT_LESS, NOT_ZERO]); (* Theorem: binomial n (HALF n) <= 4 ** (HALF n) *) (* Proof: @@ -1372,7 +1372,7 @@ val binomial_middle_by_stirling = store_thm( qabbrev_tac `k = HALF n` >> `0 < k` by decide_tac >> `n DIV k = 2` by metis_tac[MULT_TO_DIV, MULT_COMM] >> - `0 < pi * n` by metis_tac[MULT_EQ_0, NOT_ZERO_LT_ZERO] >> + `0 < pi * n` by metis_tac[MULT_EQ_0, NOT_ZERO] >> `0 < 2 * pi * n` by decide_tac >> `(FACT k) ** 2 = (SQRT (2 * pi * k)) ** 2 * ((k DIV e) ** k) ** 2` by rw[EXP_BASE_MULT] >> `_ = (SQRT (2 * pi * k)) ** 2 * (k DIV e) ** n` by rw[GSYM EXP_EXP_MULT] >> @@ -1384,7 +1384,7 @@ val binomial_middle_by_stirling = store_thm( (rpt strip_tac >> qabbrev_tac `c = b ** h` >> `b = c * c` by rw[GSYM EXP_EXP_MULT, Abbr`c`] >> - `0 < c` by metis_tac[MULT_EQ_0, NOT_ZERO_LT_ZERO] >> + `0 < c` by metis_tac[MULT_EQ_0, NOT_ZERO] >> `a * (c DIV b) = (a * c) DIV (c * c)` by metis_tac[MULT_COMM] >> `_ = (a DIV c) * (c DIV c)` by metis_tac[] >> metis_tac[DIVMOD_ID, MULT_RIGHT_1]) >> diff --git a/examples/algebra/lib/helperListScript.sml b/examples/algebra/lib/helperListScript.sml index 1da54733c0..67bc37acc2 100644 --- a/examples/algebra/lib/helperListScript.sml +++ b/examples/algebra/lib/helperListScript.sml @@ -3017,7 +3017,7 @@ val SUM_GENLIST_APPEND = store_thm( val SUM_DECOMPOSE_FIRST_LAST = store_thm( "SUM_DECOMPOSE_FIRST_LAST", ``!f n. 0 < n ==> (SUM (GENLIST f (SUC n)) = f 0 + SUM (GENLIST (f o SUC) (PRE n)) + f n)``, - metis_tac[SUM_DECOMPOSE_LAST, SUM_DECOMPOSE_FIRST, LESS_EQ_SUC, PRE_SUC_EQ]); + metis_tac[SUM_DECOMPOSE_LAST, SUM_DECOMPOSE_FIRST, SUC_EXISTS, PRE_SUC_EQ]); (* Theorem: (SUM l) MOD n = (SUM (MAP (\x. x MOD n) l)) MOD n *) (* Proof: by list induction. @@ -6420,7 +6420,7 @@ val GENLIST_MONO_DEC = store_thm( RHS = LAST [h] = h = LHS by LAST_DEF If ls <> [], Note h <= LAST ls by LAST_EL_CONS, increasing property - and MONO_INC ls by EL, m <= n ==> SUC m <= SUC n + and MONO_INC ls by EL, m <= n ==> SUC m <= SUC n MAX_LIST (h::ls) = MAX h (MAX_LIST ls) by MAX_LIST_def = MAX h (LAST ls) by induction hypothesis @@ -6459,7 +6459,7 @@ val MAX_LIST_MONO_INC = store_thm( RHS = HD [h] = h = LHS by HD If ls <> [], Note HD ls <= h by HD, decreasing property - and MONO_DEC ls by EL, m <= n ==> SUC m <= SUC n + and MONO_DEC ls by EL, m <= n ==> SUC m <= SUC n MAX_LIST (h::ls) = MAX h (MAX_LIST ls) by MAX_LIST_def = MAX h (HD ls) by induction hypothesis @@ -6499,7 +6499,7 @@ val MAX_LIST_MONO_DEC = store_thm( RHS = HD [h] = h = LHS by HD If ls <> [], Note h <= HD ls by HD, increasing property - and MONO_INC ls by EL, m <= n ==> SUC m <= SUC n + and MONO_INC ls by EL, m <= n ==> SUC m <= SUC n MIN_LIST (h::ls) = MIN h (MIN_LIST ls) by MIN_LIST_def = MIN h (HD ls) by induction hypothesis @@ -6539,7 +6539,7 @@ val MIN_LIST_MONO_INC = store_thm( RHS = LAST [h] = h = LHS by LAST_DEF If ls <> [], Note LAST ls <= h by LAST_EL_CONS, decreasing property - and MONO_DEC ls by EL, m <= n ==> SUC m <= SUC n + and MONO_DEC ls by EL, m <= n ==> SUC m <= SUC n MIN_LIST (h::ls) = MIN h (MIN_LIST ls) by MIN_LIST_def = MIN h (LAST ls) by induction hypothesis diff --git a/examples/algebra/lib/helperNumScript.sml b/examples/algebra/lib/helperNumScript.sml index b1df20c1c2..46d44895ce 100644 --- a/examples/algebra/lib/helperNumScript.sml +++ b/examples/algebra/lib/helperNumScript.sml @@ -41,6 +41,7 @@ open gcdTheory; (* for P_EUCLIDES *) THREE |- 3 = SUC 2 FOUR |- 4 = SUC 3 FIVE |- 5 = SUC 4 + num_nchotomy |- !m n. m = n \/ m < n \/ n < m ZERO_LE_ALL |- !n. 0 <= n NOT_ZERO |- !n. n <> 0 <=> 0 < n ONE_LT_POS |- !n. 1 < n ==> 0 < n @@ -50,7 +51,7 @@ open gcdTheory; (* for P_EUCLIDES *) LE_ONE |- !n. n <= 1 <=> (n = 0) \/ (n = 1) LESS_SUC |- !n. n < SUC n PRE_LESS |- !n. 0 < n ==> PRE n < n - LESS_EQ_SUC |- !n. 0 < n ==> ?m. n = SUC m + SUC_EXISTS |- !n. 0 < n ==> ?m. n = SUC m SUC_POS |- !n. 0 < SUC n SUC_NOT_ZERO |- !n. SUC n <> 0 ONE_NOT_ZERO |- 1 <> 0 @@ -97,7 +98,6 @@ open gcdTheory; (* for P_EUCLIDES *) Arithmetic Manipulations: MULT_POS |- !m n. 0 < m /\ 0 < n ==> 0 < m * n MULT_COMM_ASSOC |- !m n p. m * (n * p) = n * (m * p) - EQ_MULT_RCANCEL |- !m n p. (n * m = p * m) <=> (m = 0) \/ (n = p) MULT_RIGHT_CANCEL |- !m n p. (n * p = m * p) <=> (p = 0) \/ (n = m) MULT_LEFT_CANCEL |- !m n p. (p * n = p * m) <=> (p = 0) \/ (n = m) MULT_TO_DIV |- !m n. 0 < n ==> (n * m DIV n = m) @@ -137,15 +137,21 @@ open gcdTheory; (* for P_EUCLIDES *) ODD_SUC_HALF |- !n. ODD n ==> (HALF (SUC n) = SUC (HALF n)) HALF_EQ_0 |- !n. (HALF n = 0) <=> (n = 0) \/ (n = 1) HALF_EQ_SELF |- !n. (HALF n = n) <=> (n = 0) - HALF_LESS |- !n. 0 < n ==> HALF n < n + HALF_LT |- !n. 0 < n ==> HALF n < n + HALF_ADD1_LT |- !n. 2 < n ==> 1 + HALF n < n HALF_TWICE |- !n. HALF (TWICE n) = n HALF_MULT |- !m n. n * HALF m <= HALF (n * m) - TWO_HALF_LESS_EQ |- !n. 2 * HALF n <= n /\ n <= SUC (2 * HALF n) + TWO_HALF_LE_THM |- !n. 2 * HALF n <= n /\ n <= SUC (2 * HALF n) TWO_HALF_TIMES_LE |- !m n. TWICE (HALF n * m) <= n * m SUC_HALF_LE |- !n. 0 < n ==> 1 + HALF n <= n HALF_SQ_LE |- !n. HALF n ** 2 <= n ** 2 DIV 4 - HALF_LE |- !n. HALF n <= n - HALF_LE_MONO |- !x y. x <= y ==> HALF x <= HALF y + HALF_LE |- !n. HALF n <= n + HALF_LE_MONO |- !x y. x <= y ==> HALF x <= HALF y + HALF_SUC |- !n. HALF (SUC n) <= n + HALF_SUC_SUC |- !n. 0 < n ==> HALF (SUC (SUC n)) <= n + HALF_SUC_LE |- !n m. n < HALF (SUC m) ==> 2 * n + 1 <= m + HALF_EVEN_LE |- !n m. 2 * n < m ==> n <= HALF m + HALF_ODD_LT |- !n m. 2 * n + 1 < m ==> n < HALF m MULT_EVEN |- !n. EVEN n ==> !m. m * n = TWICE m * HALF n MULT_ODD |- !n. ODD n ==> !m. m * n = m + TWICE m * HALF n EVEN_MOD_EVEN |- !m. EVEN m /\ m <> 0 ==> !n. EVEN n <=> EVEN (n MOD m) @@ -328,7 +334,7 @@ open gcdTheory; (* for P_EUCLIDES *) binomial_2 |- !m n. (m + n) ** 2 = m ** 2 + n ** 2 + TWICE m * n SUC_SQ |- !n. SUC n ** 2 = SUC (n ** 2) + TWICE n SQ_LE |- !m n. m <= n ==> SQ m <= SQ n - EVEN_PRIME |- !n. EVEN n /\ prime n ==> (n = 2) + EVEN_PRIME |- !n. EVEN n /\ prime n <=> n = 2 ODD_PRIME |- !n. prime n /\ n <> 2 ==> ODD n TWO_LE_PRIME |- !p. prime p ==> 2 <= p NOT_PRIME_4 |- ~prime 4 @@ -349,10 +355,12 @@ open gcdTheory; (* for P_EUCLIDES *) ONE_LT_HALF_SQ |- !n. 1 < n ==> 1 < HALF (n ** 2) EXP_2_HALF |- !n. 0 < n ==> (HALF (2 ** n) = 2 ** (n - 1)) HALF_MULT_EVEN |- !m n. EVEN n ==> (HALF (m * n) = m * HALF n) - MULT_LESS_IMP_LESS |- !m n k. 0 < k /\ k * m < n ==> m < n + MULT_LT_IMP_LT |- !m n k. 0 < k /\ k * m < n ==> m < n + MULT_LE_IMP_LE |- !m n k. 0 < k /\ k * m <= n ==> m <= n HALF_EXP_5 |- !n. n * HALF (SQ n ** 2) <= HALF (n ** 5) LE_TWICE_ALT |- !m n. n <= TWICE m <=> n <> 0 ==> HALF (n - 1) < m HALF_DIV_TWO_POWER |- !m n. HALF n DIV 2 ** m = n DIV 2 ** SUC m + fit_for_10 |- 1 + 2 + 3 + 4 = 10 fit_for_100 |- 1 * 2 + 3 * 4 + 5 * 6 + 7 * 8 = 100 *) @@ -393,12 +401,17 @@ val _ = overload_on("TWICE", ``\n. 2 * n``); (* make divides infix *) val _ = set_fixity "divides" (Infixl 480); (* relation is 450, +/- is 500, * is 600. *) +(* Theorem alias *) +Theorem num_nchotomy = arithmeticTheory.LESS_LESS_CASES; +(* val num_nchotomy = |- !m n. m = n \/ m < n \/ n < m: thm *) + (* Theorem alias *) val ZERO_LE_ALL = save_thm("ZERO_LE_ALL", ZERO_LESS_EQ); (* val ZERO_LE_ALL = |- !n. 0 <= n: thm *) (* Theorem alias *) val NOT_ZERO = save_thm("NOT_ZERO", NOT_ZERO_LT_ZERO); +(* val NOT_ZERO = |- !n. n <> 0 <=> 0 < n: thm *) (* Theorem: !n. 1 < n ==> 0 < n *) (* Proof: by arithmetic. *) @@ -451,9 +464,9 @@ val PRE_LESS = store_thm( decide_tac); (* Theorem: 0 < n ==> ?m. n = SUC m *) -(* Proof: by NOT_ZERO_LT_ZERO. *) -val LESS_EQ_SUC = store_thm( - "LESS_EQ_SUC", +(* Proof: by NOT_ZERO_LT_ZERO, num_CASES. *) +val SUC_EXISTS = store_thm( + "SUC_EXISTS", ``!n. 0 < n ==> ?m. n = SUC m``, metis_tac[NOT_ZERO_LT_ZERO, num_CASES]); @@ -845,16 +858,6 @@ val MULT_COMM_ASSOC = store_thm( ``!m n p. m * (n * p) = n * (m * p)``, metis_tac[MULT_COMM, MULT_ASSOC]); -(* The missing theorem in arithmeticTheory. Only has EQ_MULT_LCANCEL: - |- !m n p. (m * n = m * p) <=> (m = 0) \/ (n = p): thm -*) -(* Theorem: (n * m = p * m) <=> (m = 0) \/ (n = p) *) -(* Proof: by EQ_MULT_LCANCEL, MULT_COMM *) -val EQ_MULT_RCANCEL = store_thm( - "EQ_MULT_RCANCEL", - ``!m n p. (n * m = p * m) <=> (m = 0) \/ (n = p)``, - rw[EQ_MULT_LCANCEL, MULT_COMM]); - (* Theorem: n * p = m * p <=> p = 0 \/ n = m *) (* Proof: n * p = m * p @@ -1310,14 +1313,38 @@ val HALF_EQ_SELF = store_thm( and HALF n <> n by HALF_EQ_SELF, n <> 0 so HALF n < n by arithmetic *) -val HALF_LESS = store_thm( - "HALF_LESS", +val HALF_LT = store_thm( + "HALF_LT", ``!n. 0 < n ==> HALF n < n``, rpt strip_tac >> `HALF n <= n` by rw[DIV_LESS_EQ] >> `HALF n <> n` by rw[HALF_EQ_SELF] >> decide_tac); +(* Theorem: 2 < n ==> (1 + HALF n < n) *) +(* Proof: + If EVEN n, + then 2 * HALF n = n by EVEN_HALF + so 2 + 2 * HALF n < n + n by 2 < n + or 1 + HALF n < n by arithmetic + If ~EVEN n, then ODD n by ODD_EVEN + then 1 + 2 * HALF n = 2 by ODD_HALF + so 1 + 2 * HALF n < n by 2 < n + also 2 + 2 * HALF n < n + n by 1 < n + or 1 + HALF n < n by arithmetic +*) +Theorem HALF_ADD1_LT: + !n. 2 < n ==> 1 + HALF n < n +Proof + rpt strip_tac >> + Cases_on `EVEN n` >| [ + `2 * HALF n = n` by rw[EVEN_HALF] >> + decide_tac, + `1 + 2 * HALF n = n` by rw[ODD_HALF, ODD_EVEN] >> + decide_tac + ] +QED + (* Theorem: HALF (2 * n) = n *) (* Proof: Let m = 2 * n. @@ -1374,8 +1401,8 @@ QED or n - 1 <= n <= n, Giving 2 * HALF n <= n /\ n <= SUC (2 * HALF n) *) -val TWO_HALF_LESS_EQ = store_thm( - "TWO_HALF_LESS_EQ", +val TWO_HALF_LE_THM = store_thm( + "TWO_HALF_LE_THM", ``!n. 2 * HALF n <= n /\ n <= SUC (2 * HALF n)``, strip_tac >> Cases_on `EVEN n` >- @@ -1391,7 +1418,7 @@ val TWO_HALF_LESS_EQ = store_thm( 2 * ((HALF n) * m) = 2 * (m * HALF n) by MULT_COMM <= 2 * (HALF (m * n)) by HALF_MULT - <= m * n by TWO_HALF_LESS_EQ + <= m * n by TWO_HALF_LE_THM = n * m by MULT_COMM *) val TWO_HALF_TIMES_LE = store_thm( @@ -1399,7 +1426,7 @@ val TWO_HALF_TIMES_LE = store_thm( ``!m n. 2 * ((HALF n) * m) <= n * m``, rpt strip_tac >> `2 * (m * HALF n) <= 2 * (HALF (m * n))` by rw[HALF_MULT] >> - `2 * (HALF (m * n)) <= m * n` by rw[TWO_HALF_LESS_EQ] >> + `2 * (HALF (m * n)) <= m * n` by rw[TWO_HALF_LE_THM] >> fs[]); (* Theorem: 0 < n ==> 1 + HALF n <= n *) @@ -1411,7 +1438,7 @@ val TWO_HALF_TIMES_LE = store_thm( Thus 1 + HALF n <= HALF n + HALF n by 1 <= HALF n = 2 * HALF n - <= n by TWO_HALF_LESS_EQ + <= n by TWO_HALF_LE_THM *) val SUC_HALF_LE = store_thm( "SUC_HALF_LE", @@ -1420,13 +1447,13 @@ val SUC_HALF_LE = store_thm( (Cases_on `n = 1` >> simp[]) >> `HALF n <> 0` by metis_tac[HALF_EQ_0, NOT_ZERO] >> `1 + HALF n <= 2 * HALF n` by decide_tac >> - `2 * HALF n <= n` by rw[TWO_HALF_LESS_EQ] >> + `2 * HALF n <= n` by rw[TWO_HALF_LE_THM] >> decide_tac); (* Theorem: (HALF n) ** 2 <= (n ** 2) DIV 4 *) (* Proof: Let k = HALF n. - Then 2 * k <= n by TWO_HALF_LESS_EQ + Then 2 * k <= n by TWO_HALF_LE_THM so (2 * k) ** 2 <= n ** 2 by EXP_EXP_LE_MONO and (2 * k) ** 2 DIV 4 <= n ** 2 DIV 4 by DIV_LE_MONOTONE, 0 < 4 But (2 * k) ** 2 DIV 4 @@ -1439,7 +1466,7 @@ val HALF_SQ_LE = store_thm( ``!n. (HALF n) ** 2 <= (n ** 2) DIV 4``, rpt strip_tac >> qabbrev_tac `k = HALF n` >> - `2 * k <= n` by rw[TWO_HALF_LESS_EQ, Abbr`k`] >> + `2 * k <= n` by rw[TWO_HALF_LE_THM, Abbr`k`] >> `(2 * k) ** 2 <= n ** 2` by rw[] >> `(2 * k) ** 2 DIV 4 <= n ** 2 DIV 4` by rw[DIV_LE_MONOTONE] >> `(2 * k) ** 2 DIV 4 = 4 * k ** 2 DIV 4` by rw[EXP_BASE_MULT] >> @@ -1454,6 +1481,152 @@ val HALF_LE_MONO = save_thm("HALF_LE_MONO", DIV_LE_MONOTONE |> SPEC ``2`` |> SIMP_RULE (arith_ss) []); (* val HALF_LE_MONO = |- !x y. x <= y ==> HALF x <= HALF y: thm *) +(* Theorem: HALF (SUC n) <= n *) +(* Proof: + If EVEN n, + Then ?k. n = 2 * k by EVEN_EXISTS + and SUC n = 2 * k + 1 + so HALF (SUC n) = k <= k + k = n by ineqaulities + Otherwise ODD n, by ODD_EVEN + Then ?k. n = 2 * k + 1 by ODD_EXISTS + and SUC n = 2 * k + 2 + so HALF (SUC n) = k + 1 <= k + k + 1 = n +*) +Theorem HALF_SUC: + !n. HALF (SUC n) <= n +Proof + rpt strip_tac >> + Cases_on `EVEN n` >| [ + `?k. n = 2 * k` by metis_tac[EVEN_EXISTS] >> + `HALF (SUC n) = k` by simp[ADD1] >> + decide_tac, + `?k. n = 2 * k + 1` by metis_tac[ODD_EXISTS, ODD_EVEN, ADD1] >> + `HALF (SUC n) = k + 1` by simp[ADD1] >> + decide_tac + ] +QED + +(* Theorem: 0 < n ==> HALF (SUC (SUC n)) <= n *) +(* Proof: + Note SUC (SUC n) = n + 2 by ADD1 + If EVEN n, + then ?k. n = 2 * k by EVEN_EXISTS + Since n = 2 * k <> 0 by NOT_ZERO, 0 < n + so k <> 0, or 1 <= k by MULT_EQ_0 + HALF (n + 2) + = k + 1 by arithmetic + <= k + k by above + = n + Otherwise ODD n, by ODD_EVEN + then ?k. n = 2 * k + 1 by ODD_EXISTS + HALF (n + 2) + = HALF (2 * k + 3) by arithmetic + = k + 1 by arithmetic + <= k + k + 1 by ineqaulities + = n +*) +Theorem HALF_SUC_SUC: + !n. 0 < n ==> HALF (SUC (SUC n)) <= n +Proof + rpt strip_tac >> + Cases_on `EVEN n` >| [ + `?k. n = 2 * k` by metis_tac[EVEN_EXISTS] >> + `0 < k` by metis_tac[MULT_EQ_0, NOT_ZERO] >> + `1 <= k` by decide_tac >> + `HALF (SUC (SUC n)) = k + 1` by simp[ADD1] >> + fs[], + `?k. n = 2 * k + 1` by metis_tac[ODD_EXISTS, ODD_EVEN, ADD1] >> + `HALF (SUC (SUC n)) = k + 1` by simp[ADD1] >> + fs[] + ] +QED + +(* Theorem: n < HALF (SUC m) ==> 2 * n + 1 <= m *) +(* Proof: + If EVEN m, + Then m = 2 * HALF m by EVEN_HALF + and SUC m = 2 * HALF m + 1 by ADD1 + so n < (2 * HALF m + 1) DIV 2 by given + or n < HALF m by arithmetic + 2 * n < 2 * HALF m by LT_MULT_LCANCEL + 2 * n < m by above + 2 * n + 1 <= m by arithmetic + Otherwise, ODD m by ODD_EVEN + Then m = 2 * HALF m + 1 by ODD_HALF + and SUC m = 2 * HALF m + 2 by ADD1 + so n < (2 * HALF m + 2) DIV 2 by given + or n < HALF m + 1 by arithmetic + 2 * n + 1 < 2 * HALF m + 1 by LT_MULT_LCANCEL, LT_ADD_RCANCEL + or 2 * n + 1 < m by above + Overall, 2 * n + 1 <= m. +*) +Theorem HALF_SUC_LE: + !n m. n < HALF (SUC m) ==> 2 * n + 1 <= m +Proof + rpt strip_tac >> + Cases_on `EVEN m` >| [ + `m = 2 * HALF m` by simp[EVEN_HALF] >> + `HALF (SUC m) = HALF (2 * HALF m + 1)` by metis_tac[ADD1] >> + `_ = HALF m` by simp[] >> + simp[], + `m = 2 * HALF m + 1` by simp[ODD_HALF, ODD_EVEN] >> + `HALF (SUC m) = HALF (2 * HALF m + 1 + 1)` by metis_tac[ADD1] >> + `_ = HALF m + 1` by simp[] >> + simp[] + ] +QED + +(* Theorem: 2 * n < m ==> n <= HALF m *) +(* Proof: + If EVEN m, + Then m = 2 * HALF m by EVEN_HALF + so 2 * n < 2 * HALF m by above + or n < HALF m by LT_MULT_LCANCEL + Otherwise, ODD m by ODD_EVEN + Then m = 2 * HALF m + 1 by ODD_HALF + so 2 * n < 2 * HALF m + 1 by above + so 2 * n <= 2 * HALF m by removing 1 + or n <= HALF m by LE_MULT_LCANCEL + Overall, n <= HALF m. +*) +Theorem HALF_EVEN_LE: + !n m. 2 * n < m ==> n <= HALF m +Proof + rpt strip_tac >> + Cases_on `EVEN m` >| [ + `2 * n < 2 * HALF m` by metis_tac[EVEN_HALF] >> + simp[], + `2 * n < 2 * HALF m + 1` by metis_tac[ODD_HALF, ODD_EVEN] >> + simp[] + ] +QED + +(* Theorem: 2 * n + 1 < m ==> n < HALF m *) +(* Proof: + If EVEN m, + Then m = 2 * HALF m by EVEN_HALF + so 2 * n + 1 < 2 * HALF m by above + or 2 * n < 2 * HALF m by removing 1 + or n < HALF m by LT_MULT_LCANCEL + Otherwise, ODD m by ODD_EVEN + Then m = 2 * HALF m + 1 by ODD_HALF + so 2 * n + 1 < 2 * HALF m + 1 by above + or 2 * n < 2 * HALF m by LT_ADD_RCANCEL + or n < HALF m by LT_MULT_LCANCEL + Overall, n < HALF m. +*) +Theorem HALF_ODD_LT: + !n m. 2 * n + 1 < m ==> n < HALF m +Proof + rpt strip_tac >> + Cases_on `EVEN m` >| [ + `2 * n + 1 < 2 * HALF m` by metis_tac[EVEN_HALF] >> + simp[], + `2 * n + 1 < 2 * HALF m + 1` by metis_tac[ODD_HALF, ODD_EVEN] >> + simp[] + ] +QED + (* Theorem: EVEN n ==> !m. m * n = (TWICE m) * (HALF n) *) (* Proof: (TWICE m) * (HALF n) @@ -2380,13 +2553,13 @@ val LE_MULT_LE_DIV = store_thm( Only-if part: 0 DIV m = 0 by ZERO_DIV 0 MOD m = 0 by ZERO_MOD *) -val DIV_MOD_EQ_0 = store_thm( - "DIV_MOD_EQ_0", - ``!m n. 0 < m ==> ((n DIV m = 0) /\ (n MOD m = 0) <=> (n = 0))``, +Theorem DIV_MOD_EQ_0: + !m n. 0 < m ==> ((n DIV m = 0) /\ (n MOD m = 0) <=> (n = 0)) +Proof rpt strip_tac >> - rw[EQ_IMP_THM] >- - metis_tac[DIV_EQUAL_0, LESS_MOD] >> - rw[ZERO_DIV]); + rw[EQ_IMP_THM] >> + metis_tac[DIV_EQUAL_0, LESS_MOD] +QED (* Theorem: 0 < m /\ 0 < n /\ (n MOD m = 0) ==> n DIV (SUC m) < n DIV m *) (* Proof: @@ -3842,19 +4015,29 @@ val SQ_LE = store_thm( ``!m n. m <= n ==> SQ m <= SQ n``, rw[]); -(* Theorem: EVEN n /\ prime n ==> (n = 2) *) +(* Theorem: EVEN n /\ prime n <=> n = 2 *) +(* Proof: + If part: EVEN n /\ prime n ==> n = 2 + EVEN n ==> n MOD 2 = 0 by EVEN_MOD2 + ==> 2 divides n by DIVIDES_MOD_0, 0 < 2 + ==> n = 2 by prime_def, 2 <> 1 + Only-if part: n = 2 ==> EVEN n /\ prime n + Note EVEN 2 by EVEN_2 + and prime 2 by prime_2 +*) (* Proof: EVEN n ==> n MOD 2 = 0 by EVEN_MOD2 ==> 2 divides n by DIVIDES_MOD_0, 0 < 2 ==> n = 2 by prime_def, 2 <> 1 *) -val EVEN_PRIME = store_thm( - "EVEN_PRIME", - ``!n. EVEN n /\ prime n ==> (n = 2)``, - rpt strip_tac >> +Theorem EVEN_PRIME: + !n. EVEN n /\ prime n <=> n = 2 +Proof + rw[EQ_IMP_THM] >> `0 < 2 /\ 2 <> 1` by decide_tac >> `2 divides n` by rw[DIVIDES_MOD_0, GSYM EVEN_MOD2] >> - metis_tac[prime_def]); + metis_tac[prime_def] +QED (* Theorem: prime n /\ n <> 2 ==> ODD n *) (* Proof: @@ -4426,8 +4609,8 @@ val HALF_MULT_EVEN = store_thm( Since 0 <= h * m, so k * m < n ==> m < n. *) -val MULT_LESS_IMP_LESS = store_thm( - "MULT_LESS_IMP_LESS", +val MULT_LT_IMP_LT = store_thm( + "MULT_LT_IMP_LT", ``!m n k. 0 < k /\ k * m < n ==> m < n``, rpt strip_tac >> `k <> 0` by decide_tac >> @@ -4435,6 +4618,21 @@ val MULT_LESS_IMP_LESS = store_thm( `k * m = h * m + m` by rw[ADD1] >> decide_tac); +(* Theorem: 0 < k /\ k * m <= n ==> m <= n *) +(* Proof: + Note 1 <= k by 0 < k + so 1 * m <= k * m by LE_MULT_RCANCEL + or m <= k * m <= n by inequalities +*) +Theorem MULT_LE_IMP_LE: + !m n k. 0 < k /\ k * m <= n ==> m <= n +Proof + rpt strip_tac >> + `1 <= k` by decide_tac >> + `1 * m <= k * m` by simp[] >> + decide_tac +QED + (* Theorem: n * HALF ((SQ n) ** 2) <= HALF (n ** 5) *) (* Proof: n * HALF ((SQ n) ** 2) @@ -4530,12 +4728,21 @@ val HALF_DIV_TWO_POWER = store_thm( ``!m n. (HALF n) DIV 2 ** m = n DIV (2 ** SUC m)``, rw[DIV_DIV_DIV_MULT, EXP]); +(* Theorem: 1 + 2 + 3 + 4 = 10 *) +(* Proof: by calculation. *) +Theorem fit_for_10: + 1 + 2 + 3 + 4 = 10 +Proof + decide_tac +QED + (* Theorem: 1 * 2 + 3 * 4 + 5 * 6 + 7 * 8 = 100 *) (* Proof: by calculation. *) -val fit_for_100 = store_thm( - "fit_for_100", - ``1 * 2 + 3 * 4 + 5 * 6 + 7 * 8 = 100``, - decide_tac); +Theorem fit_for_100: + 1 * 2 + 3 * 4 + 5 * 6 + 7 * 8 = 100 +Proof + decide_tac +QED (* ------------------------------------------------------------------------- *) diff --git a/examples/algebra/lib/helperSetScript.sml b/examples/algebra/lib/helperSetScript.sml index ffefb4dfeb..ccb2b2209b 100644 --- a/examples/algebra/lib/helperSetScript.sml +++ b/examples/algebra/lib/helperSetScript.sml @@ -244,6 +244,8 @@ open gcdTheory; (* for P_EUCLIDES *) SUM_IMAGE_INSERT |- !f s. FINITE s ==> !e. e NOTIN s ==> (SIGMA f (e INSERT s) = f e + SIGMA f s) SUM_IMAGE_AS_SUM_SET |- !s. FINITE s ==> !f. (!x y. (f x = f y) ==> (x = y)) ==> (SIGMA f s = SUM_SET (IMAGE f s)) + SUM_IMAGE_DOUBLET |- !f x y. x <> y ==> SIGMA f {x; y} = f x + f y + SUM_IMAGE_TRIPLET |- !f x y z. x <> y /\ y <> z /\ z <> x ==> SIGMA f {x; y; z} = f x + f y + f z SIGMA_CONSTANT |- !s. FINITE s ==> !f k. (!x. x IN s ==> (f x = k)) ==> (SIGMA f s = k * CARD s) SUM_IMAGE_CONSTANT |- !s. FINITE s ==> !c. SIGMA (K c) s = c * CARD s SIGMA_CARD_CONSTANT |- !n s. FINITE s /\ (!e. e IN s ==> CARD e = n) ==> SIGMA CARD s = n * CARD s @@ -324,6 +326,8 @@ open gcdTheory; (* for P_EUCLIDES *) set_additive_card |- SET_ADDITIVE CARD disjoint_bigunion_card |- !P. FINITE P /\ EVERY_FINITE P /\ PAIR_DISJOINT P ==> (CARD (BIGUNION P) = SIGMA CARD P) + CARD_BIGUNION_PAIR_DISJOINT |- !P. FINITE P /\ EVERY_FINITE P /\ PAIR_DISJOINT P ==> + CARD (BIGUNION P) = SIGMA CARD P set_additive_sigma |- !f. SET_ADDITIVE (SIGMA f) disjoint_bigunion_sigma |- !P. FINITE P /\ EVERY_FINITE P /\ PAIR_DISJOINT P ==> !f. SIGMA f (BIGUNION P) = SIGMA (SIGMA f) P @@ -1607,7 +1611,7 @@ val MAX_SET_IMAGE_SUC_COUNT = store_thm( Let s = {f x | HALF x <= c} Note !x. HALF x <= c ==> SUC (2 * HALF x) <= SUC (2 * c) by arithmetic - and x <= SUC (2 * HALF x) by TWO_HALF_LESS_EQ + and x <= SUC (2 * HALF x) by TWO_HALF_LE_THM so x <= SUC (2 * c) < 2 * c + 2 by arithmetic Thus s SUBSET (IMAGE f (count (2 * c + 2))) by SUBSET_DEF Note FINITE (count (2 * c + 2)) by FINITE_COUNT @@ -1623,7 +1627,7 @@ val MAX_SET_IMAGE_with_HALF = store_thm( `s SUBSET (IMAGE f (count (2 * c + 2)))` by (rw[SUBSET_DEF, Abbr`s`] >> `SUC (2 * HALF x'') <= SUC (2 * c)` by rw[] >> - `x'' <= SUC (2 * HALF x'')` by rw[TWO_HALF_LESS_EQ] >> + `x'' <= SUC (2 * HALF x'')` by rw[TWO_HALF_LE_THM] >> `x'' < 2 * c + 2` by decide_tac >> metis_tac[]) >> `FINITE s` by metis_tac[FINITE_COUNT, IMAGE_FINITE, SUBSET_FINITE] >> @@ -2606,6 +2610,58 @@ val SUM_IMAGE_AS_SUM_SET = store_thm( rw[SUM_IMAGE_THM, SUM_IMAGE_DELETE] >> metis_tac[]); +(* Theorem: x <> y ==> SIGMA f {x; y} = f x + f y *) +(* Proof: + Let s = {x; y}. + Then FINITE s by FINITE_UNION, FINITE_SING + and x INSERT s by INSERT_DEF + and s DELETE x = {y} by DELETE_DEF + SIGMA f s + = SIGMA f (x INSERT s) by above + = f x + SIGMA f (s DELETE x) by SUM_IMAGE_THM + = f x + SIGMA f {y} by above + = f x + f y by SUM_IMAGE_SING +*) +Theorem SUM_IMAGE_DOUBLET: + !f x y. x <> y ==> SIGMA f {x; y} = f x + f y +Proof + rpt strip_tac >> + qabbrev_tac `s = {x; y}` >> + `FINITE s` by fs[Abbr`s`] >> + `x INSERT s = s` by fs[Abbr`s`] >> + `s DELETE x = {x; y} DELETE x` by simp[Abbr`s`] >> + `_ = if y = x then {} else {y}` by EVAL_TAC >> + `_ = {y}` by simp[] >> + metis_tac[SUM_IMAGE_THM, SUM_IMAGE_SING] +QED + +(* Theorem: x <> y /\ y <> z /\ z <> x ==> SIGMA f {x; y; z} = f x + f y + f z *) +(* Proof: + Let s = {x; y; z}. + Then FINITE s by FINITE_UNION, FINITE_SING + and x INSERT s by INSERT_DEF + and s DELETE x = {y; z} by DELETE_DEF + SIGMA f s + = SIGMA f (x INSERT s) by above + = f x + SIGMA f (s DELETE x) by SUM_IMAGE_THM + = f x + SIGMA f {y; z} by above + = f x + f y + f z by SUM_IMAGE_DOUBLET +*) +Theorem SUM_IMAGE_TRIPLET: + !f x y z. x <> y /\ y <> z /\ z <> x ==> SIGMA f {x; y; z} = f x + f y + f z +Proof + rpt strip_tac >> + qabbrev_tac `s = {x; y; z}` >> + `FINITE s` by fs[Abbr`s`] >> + `x INSERT s = s` by fs[Abbr`s`] >> + `s DELETE x = {x; y; z} DELETE x` by simp[Abbr`s`] >> + `_ = if y = x then if z = x then {} else {z} + else y INSERT if z = x then {} else {z}` by EVAL_TAC >> + `_ = {y; z}` by simp[] >> + `SIGMA f s = f x + (f y + f z)` by metis_tac[SUM_IMAGE_THM, SUM_IMAGE_DOUBLET, SUM_IMAGE_SING] >> + decide_tac +QED + (* Theorem: FINITE s ==> !f k. (!x. x IN s ==> (f x = k)) ==> (SIGMA f s = k * CARD s) *) (* Proof: By finite induction on s. @@ -3819,6 +3875,14 @@ val disjoint_bigunion_card = store_thm( ``!P. FINITE P /\ EVERY_FINITE P /\ PAIR_DISJOINT P ==> (CARD (BIGUNION P) = SIGMA CARD P)``, rw[disjoint_bigunion_add_fun, set_additive_card]); +(* Theorem alias *) +Theorem CARD_BIGUNION_PAIR_DISJOINT = disjoint_bigunion_card; +(* +val CARD_BIGUNION_PAIR_DISJOINT = + |- !P. FINITE P /\ EVERY_FINITE P /\ PAIR_DISJOINT P ==> + CARD (BIGUNION P) = SIGMA CARD P: thm +*) + (* Theorem: SET_ADDITIVE (SIGMA f) *) (* Proof: Since SIGMA f {} = 0 by SUM_IMAGE_EMPTY diff --git a/examples/algebra/lib/logPowerScript.sml b/examples/algebra/lib/logPowerScript.sml index c9b6619d7d..6fe09404a0 100644 --- a/examples/algebra/lib/logPowerScript.sml +++ b/examples/algebra/lib/logPowerScript.sml @@ -57,17 +57,9 @@ open logrootTheory; (* for ROOT *) ROOT_EQ_0 |- !m. 0 < m ==> !n. (ROOT m n = 0) <=> (n = 0) # ROOT_1 |- !n. ROOT 1 n = n ROOT_THM |- !r. 0 < r ==> !n p. (ROOT r n = p) <=> p ** r <= n /\ n < SUC p ** r - ROOT_compute |- !r n. 0 < r ==> (ROOT r 0 = 0) /\ - (ROOT r n = (let x = 2 * ROOT r (n DIV 2 ** r) - in if n < SUC x ** r then x else SUC x)) ROOT_EQN |- !r n. 0 < r ==> (ROOT r n = (let m = TWICE (ROOT r (n DIV 2 ** r)) in m + if (m + 1) ** r <= n then 1 else 0)) - ROOT_EVAL |- !r n. ROOT r n = - if r = 0 then ROOT 0 n - else if n = 0 then 0 - else (let m = TWICE (ROOT r (n DIV 2 ** r)) - in m + if SUC m ** r <= n then 1 else 0) ROOT_SUC |- !r n. 0 < r ==> ROOT r (SUC n) = ROOT r n + if SUC n = SUC (ROOT r n) ** r then 1 else 0 @@ -79,6 +71,7 @@ open logrootTheory; (* for ROOT *) Square Root: SQRT_PROPERTY |- !n. 0 < n ==> SQRT n ** 2 <= n /\ n < SUC (SQRT n) ** 2 + SQRT_UNIQUE |- !n p. p ** 2 <= n /\ n < SUC p ** 2 ==> SQRT n = p SQRT_THM |- !n p. (SQRT n = p) <=> p ** 2 <= n /\ n < SUC p ** 2 SQ_SQRT_LE |- !n. SQ (SQRT n) <= n SQRT_LE |- !n m. n <= m ==> SQRT n <= SQRT m @@ -94,6 +87,15 @@ open logrootTheory; (* for ROOT *) SQRT_GE_SELF |- !n. n <= SQRT n <=> (n = 0) \/ (n = 1) SQRT_EQ_SELF |- !n. (SQRT n = n) <=> (n = 0) \/ (n = 1) SQRT_LE_IMP |- !n m. SQRT n <= m ==> n <= 3 * m ** 2 + SQRT_MULT_LE |- !n m. SQRT n * SQRT m <= SQRT (n * m) + + Square predicate: + square_def |- !n. square n <=> ?k. n = k * k + square_alt |- !n. square n <=> ?k. n = k ** 2 +! square_eqn |- !n. square n <=> SQRT n ** 2 = n + square_0 |- square 0 + square_1 |- square 1 + prime_non_square |- !p. prime p ==> ~square p Logarithm: LOG_EXACT_EXP |- !a. 1 < a ==> !n. LOG a (a ** n) = n @@ -436,63 +438,6 @@ val ROOT_1 = store_thm( ``!n. ROOT 1 n = n``, rw[ROOT_UNIQUE]); -(* This is a rework of logrootTheory.ROOT_COMPUTE *) - -(* Theorem: 0 < r ==> (ROOT r 0 = 0) /\ - (ROOT r n = let x = 2 * ROOT r (n DIV 2 ** r) in if n < SUC x ** r then x else SUC x) *) -(* Proof: - This is to show: - (1) ROOT r 0 = 0, true by ROOT_EQ_0 - (2) ROOT r n = (let x = 2 * ROOT r (n DIV 2 ** r) in if n < SUC x ** r then x else SUC x) - Let x = 2 * ROOT r (n DIV 2 ** r). - To show: ROOT r n = if n < SUC x ** r then x else SUC x - By ROOT_UNIQUE, this is to show: - (1) n < SUC (if n < SUC x ** r then x else SUC x) ** r - If n < SUC x ** r, to show: n < SUC x ** r, true trivially - If ~(n < SUC x ** r), to show: n < SUC (SUC x) ** r - Let y = SUC (ROOT r n) ** r. - Then n < y by ROOT - and ROOT r n <= SUC (2 * HALF (ROOT r n)) by TWO_HALF_LESS_EQ - But x = 2 * HALF (ROOT r n) by ROOT_DIV - so ROOT r n <= SUC x by above - or y <= SUC (SUC x) ** r by EXP_LE_ISO - Thus n < SUC (SUC x) ** r by LESS_LESS_EQ_TRANS - - (2) (if n < SUC x ** r then x else SUC x) ** r <= n - If n < SUC x ** r, to show: x ** r <= n - Let y = ROOT r n ** r. - Then y <= n by ROOT - and 2 * HALF (ROOT r n) <= ROOT r n by TWO_HALF_LESS_EQ - But x = 2 * HALF (ROOT r n) by ROOT_DIV - so x <= ROOT r n by above - or x ** r <= y by EXP_LE_ISO - Thus x ** r <= n by LESS_EQ_TRANS - -*) -val ROOT_compute = store_thm( - "ROOT_compute", - ``!r n. 0 < r ==> (ROOT r 0 = 0) /\ - (ROOT r n = let x = 2 * ROOT r (n DIV 2 ** r) in - if n < SUC x ** r then x else SUC x)``, - rpt strip_tac >- - rw[ROOT_EQ_0] >> - rw_tac std_ss[] >> - (irule ROOT_UNIQUE >> rpt conj_tac >> simp[]) >| [ - rw[] >> - `x = 2 * HALF (ROOT r n)` by rw[ROOT_DIV, Abbr`x`] >> - qabbrev_tac `y = SUC (ROOT r n) ** r` >> - `n < y` by rw[ROOT, Abbr`y`] >> - `ROOT r n <= SUC x` by rw[TWO_HALF_LESS_EQ] >> - `y <= SUC (SUC x) ** r` by rw[EXP_LE_ISO, Abbr`y`] >> - decide_tac, - rw[] >> - `x = 2 * HALF (ROOT r n)` by rw[ROOT_DIV, Abbr`x`] >> - qabbrev_tac `y = ROOT r n ** r` >> - `y <= n` by rw[ROOT, Abbr`y`] >> - `x <= ROOT r n` by rw[TWO_HALF_LESS_EQ] >> - `x ** r <= y` by rw[EXP_LE_ISO, Abbr`y`] >> - decide_tac - ]); (* Theorem: 0 < r ==> (ROOT r n = let m = 2 * ROOT r (n DIV 2 ** r) in m + if (m + 1) ** r <= n then 1 else 0) *) @@ -512,32 +457,6 @@ val ROOT_EQN = store_thm( rw[ROOT_COMPUTE, ADD1] >> rw[ROOT_COMPUTE, ADD1]); -(* Theorem: ROOT r n = - if r = 0 then ROOT 0 n else - if n = 0 then 0 else - let m = TWICE (ROOT r (n DIV 2 ** r)) in - m + if (SUC m) ** r <= n then 1 else 0 *) -(* Proof: by ROOT_OF_0, ROOT_EQN *) -val ROOT_EVAL = store_thm( - "ROOT_EVAL[compute]", (* put in computeLib *) - ``!r n. ROOT r n = - if r = 0 then ROOT 0 n else - if n = 0 then 0 else - let m = TWICE (ROOT r (n DIV 2 ** r)) in - m + if (SUC m) ** r <= n then 1 else 0``, - metis_tac[ROOT_OF_0, ROOT_EQN, ADD1, NOT_ZERO_LT_ZERO]); -(* Put ROOT_EVAL into computeLib *) - -(* -> EVAL ``ROOT 3 125``; -val it = |- ROOT 3 125 = 5: thm -> EVAL ``ROOT 3 100``; -val it = |- ROOT 3 100 = 4: thm -> EVAL ``MAP (ROOT 3) [1 .. 20]``; = - [1; 1; 1; 1; 1; 1; 1; 2; 2; 2; 2; 2; 2; 2; 2; 2; 2; 2; 2; 2]: thm -> EVAL ``MAP (ROOT 3) [1 .. 30]``; = - [1; 1; 1; 1; 1; 1; 1; 2; 2; 2; 2; 2; 2; 2; 2; 2; 2; 2; 2; 2; 2; 2; 2; 2; 2; 2; 3; 3; 3; 3]: thm -*) (* Theorem: 0 < r ==> (ROOT r (SUC n) = ROOT r n + if SUC n = (SUC (ROOT r n)) ** r then 1 else 0) *) @@ -760,6 +679,10 @@ val SQRT_PROPERTY = store_thm( ``!n. (SQRT n) ** 2 <= n /\ n < SUC (SQRT n) ** 2``, rw[ROOT]); +(* Get a useful theorem *) +Theorem SQRT_UNIQUE = logrootTheory.ROOT_UNIQUE |> SPEC ``2``; +(* val SQRT_UNIQUE = |- !n p. p ** 2 <= n /\ n < SUC p ** 2 ==> SQRT n = p: thm *) + (* Obtain a theorem *) val SQRT_THM = save_thm("SQRT_THM", ROOT_THM |> SPEC ``2`` |> SIMP_RULE (srw_ss())[]); @@ -953,6 +876,106 @@ val SQRT_LE_IMP = store_thm( `2 * m * m = 2 * m ** 2` by rw[] >> decide_tac); +(* Theorem: (SQRT n) * (SQRT m) <= SQRT (n * m) *) +(* Proof: + Note (SQRT n) ** 2 <= n by SQRT_PROPERTY + and (SQRT m) ** 2 <= m by SQRT_PROPERTY + so (SQRT n) ** 2 * (SQRT m) ** 2 <= n * m by LE_MONO_MULT2 + or ((SQRT n) * (SQRT m)) ** 2 <= n * m by EXP_BASE_MULT + ==> (SQRT n) * (SQRT m) <= SQRT (n * m) by SQRT_LE, SQRT_OF_SQ +*) +Theorem SQRT_MULT_LE: + !n m. (SQRT n) * (SQRT m) <= SQRT (n * m) +Proof + rpt strip_tac >> + qabbrev_tac `h = SQRT n` >> + qabbrev_tac `k = SQRT m` >> + `h ** 2 <= n` by simp[SQRT_PROPERTY, Abbr`h`] >> + `k ** 2 <= m` by simp[SQRT_PROPERTY, Abbr`k`] >> + `(h * k) ** 2 <= n * m` by metis_tac[LE_MONO_MULT2, EXP_BASE_MULT] >> + metis_tac[SQRT_LE, SQRT_OF_SQ] +QED + +(* ------------------------------------------------------------------------- *) +(* Square predicate *) +(* ------------------------------------------------------------------------- *) + +(* Define square predicate. *) + +Definition square_def[nocompute]: + square (n:num) = ?k. n = k * k +End +(* use [nocompute] as this is not effective. *) + +(* Theorem: square n = ?k. n = k ** 2 *) +(* Proof: by square_def. *) +Theorem square_alt: + !n. square n = ?k. n = k ** 2 +Proof + simp[square_def] +QED + +(* Theorem: square n <=> (SQRT n) ** 2 = n *) +(* Proof: + If part: square n ==> (SQRT n) ** 2 = n + This is true by SQRT_SQ, EXP_2 + Only-if part: (SQRT n) ** 2 = n ==> square n + Take k = SQRT n for n = k ** 2. +*) +Theorem square_eqn[compute]: + !n. square n <=> (SQRT n) ** 2 = n +Proof + metis_tac[square_def, SQRT_SQ, EXP_2] +QED + +(* +EVAL ``square 10``; F +EVAL ``square 16``; T +*) + +(* Theorem: square 0 *) +(* Proof: by 0 = 0 * 0. *) +Theorem square_0: + square 0 +Proof + simp[square_def] +QED + +(* Theorem: square 1 *) +(* Proof: by 1 = 1 * 1. *) +Theorem square_1: + square 1 +Proof + simp[square_def] +QED + +(* Theorem: prime p ==> ~square p *) +(* Proof: + By contradiction, suppose (square p). + Then p = k * k by square_def + thus k divides p by divides_def + so k = 1 or k = p by prime_def + If k = 1, + then p = 1 * 1 = 1 by arithmetic + but p <> 1 by NOT_PRIME_1 + If k = p, + then p * 1 = p * p by arithmetic + or 1 = p by EQ_MULT_LCANCEL, NOT_PRIME_0 + but p <> 1 by NOT_PRIME_1 +*) +Theorem prime_non_square: + !p. prime p ==> ~square p +Proof + rpt strip_tac >> + `?k. p = k * k` by rw[GSYM square_def] >> + `k divides p` by metis_tac[divides_def] >> + `(k = 1) \/ (k = p)` by metis_tac[prime_def] >- + fs[NOT_PRIME_1] >> + `p * 1 = p * p` by metis_tac[MULT_RIGHT_1] >> + `1 = p` by metis_tac[EQ_MULT_LCANCEL, NOT_PRIME_0] >> + metis_tac[NOT_PRIME_1] +QED + (* ------------------------------------------------------------------------- *) (* Logarithm *) (* ------------------------------------------------------------------------- *) @@ -1517,7 +1540,7 @@ val halves_pos = store_thm( By complete induction on n. Assume: !m. m < n ==> 0 < m ==> (halves m = 1 + LOG2 m) To show: 0 < n ==> (halves n = 1 + LOG2 n) - Note HALF n < n by HALF_LESS, 0 < n + Note HALF n < n by HALF_LT, 0 < n Need 0 < HALF n to apply induction hypothesis. If HALF n = 0, Then n = 1 by HALF_EQ_0 @@ -1542,7 +1565,7 @@ val halves_by_LOG2 = store_thm( rw[Once halves_def] >> Cases_on `n = 1` >- simp[Once halves_def] >> - `HALF n < n` by rw[HALF_LESS] >> + `HALF n < n` by rw[HALF_LT] >> `HALF n <> 0` by fs[HALF_EQ_0] >> simp[LOG2_BY_HALF]); @@ -2382,7 +2405,7 @@ val count_up_suc = store_thm( and 2 ** SUC t * m = 2 * 2 ** t * m by EXP = 2 * (2 ** t * m) by MULT_ASSOC - Thus (2 ** t * m) < n by MULT_LESS_IMP_LESS, 0 < 2 + Thus (2 ** t * m) < n by MULT_LT_IMP_LT, 0 < 2 count_up n m k = count_up n (2 ** SUC t * m) (SUC k + t) by induction hypothesis = count_up n (2 * (2 ** SUC t * m)) (SUC (SUC k + t)) by count_up_suc @@ -2400,7 +2423,7 @@ val count_up_suc_eqn = store_thm( `2 ** SUC t <> 0` by metis_tac[EXP_EQ_0, DECIDE``2 <> 0``] >> `2 ** SUC t * m <> 0` by metis_tac[MULT_EQ_0] >> `2 ** SUC t * m = 2 * q` by rw_tac std_ss[EXP, MULT_ASSOC, Abbr`q`] >> - `q < n` by rw[MULT_LESS_IMP_LESS] >> + `q < n` by rw[MULT_LT_IMP_LT] >> rw[count_up_suc, EXP, ADD1]); (* Theorem: m <> 0 ==> !n t. 2 ** t * m < 2 * n /\ n <= 2 ** t * m ==> !k. count_up n m k = k + t *) diff --git a/examples/algebra/lib/primePowerScript.sml b/examples/algebra/lib/primePowerScript.sml index b88010d0de..e8042caaa1 100644 --- a/examples/algebra/lib/primePowerScript.sml +++ b/examples/algebra/lib/primePowerScript.sml @@ -1259,9 +1259,10 @@ QED (* ------------------------------------------------------------------------- *) (* Define the prime divisors of a number *) -val prime_divisors_def = Define` +val prime_divisors_def = zDefine` prime_divisors n = {p | prime p /\ p divides n} `; +(* use zDefine as this is not effective. *) (* Theorem: p IN prime_divisors n <=> prime p /\ p divides n *) (* Proof: by prime_divisors_def *) diff --git a/examples/algebra/polynomial/polyBinomialScript.sml b/examples/algebra/polynomial/polyBinomialScript.sml index d02de708d9..e23eea0c73 100644 --- a/examples/algebra/polynomial/polyBinomialScript.sml +++ b/examples/algebra/polynomial/polyBinomialScript.sml @@ -1280,7 +1280,6 @@ val poly_sum_by_weak_sum_genlist = store_thm( = poly_sum (GENLIST (\j. f j * X ** j) (SUC n)) ' k by poly_sum_by_weak_sum_genlist = f k by induction hypothesis *) - Theorem poly_coeff_sum_genlist: !r:'a ring. Ring r /\ #1 <> #0 ==> @@ -1326,6 +1325,7 @@ Proof ] QED + (* ------------------------------------------------------------------------- *) (* Polynomial Identity only for Primes *) (* ------------------------------------------------------------------------- *) diff --git a/examples/algebra/ring/ringBinomialScript.sml b/examples/algebra/ring/ringBinomialScript.sml index c21dca465d..aeb810de96 100644 --- a/examples/algebra/ring/ringBinomialScript.sml +++ b/examples/algebra/ring/ringBinomialScript.sml @@ -1159,7 +1159,7 @@ val ring_freshman_thm_sub = store_thm( rw[] >> `(x + -y) ** m = x ** m + (-y) ** m` by rw[ring_freshman_thm, Abbr`m`] >> Cases_on `EVEN m` >- - rw[EVEN_PRIME, ring_neg_exp, ring_neg_char_2, Abbr`m`] >> + rw[GSYM EVEN_PRIME, ring_neg_exp, ring_neg_char_2, Abbr`m`] >> rw[ring_neg_exp]); (* Theorem: Ring r /\ prime (char r) ==> !x y. x IN R /\ y IN R ==> diff --git a/examples/fermat/count/combinatoricsScript.sml b/examples/fermat/count/combinatoricsScript.sml index a6ad0b9586..1eadaec4ac 100644 --- a/examples/fermat/count/combinatoricsScript.sml +++ b/examples/fermat/count/combinatoricsScript.sml @@ -43,7 +43,7 @@ open necklaceTheory; (* for necklace_def, necklace_finite *) (* ------------------------------------------------------------------------- *) (* Overloading (# is temporary): *) -(* +(* Definitions and Theorems (# are exported, ! are in compute): Counting number of combinations: sub_count_def |- !n k. sub_count n k = {s | s SUBSET count n /\ CARD s = k} diff --git a/examples/fermat/count/helperCountScript.sml b/examples/fermat/count/helperCountScript.sml index 05bcae9681..b76a28dd8b 100644 --- a/examples/fermat/count/helperCountScript.sml +++ b/examples/fermat/count/helperCountScript.sml @@ -29,7 +29,8 @@ open arithmeticTheory pred_setTheory; s bij_eq t = ?f. BIJ f s t s =b= t = ?f. BIJ f s t *) -(* +(* Definitions and Theorems (# are exported, ! are in compute): + Set Theorems: over_inj |- !f s t. INJ f s t ==> over f s t over_surj |- !f s t. SURJ f s t ==> over f s t diff --git a/examples/fermat/little/FLTactionScript.sml b/examples/fermat/little/FLTactionScript.sml index b842dd7860..46dbbed0e3 100644 --- a/examples/fermat/little/FLTactionScript.sml +++ b/examples/fermat/little/FLTactionScript.sml @@ -59,7 +59,7 @@ open dividesTheory; (* for divides_def, prime_def *) (* ------------------------------------------------------------------------- *) (* Overloading: *) -(* +(* Definitions and Theorems (# are exported, ! are in compute): From groupInstances: Zadd_def |- !n. Zadd n = <|carrier := count n; diff --git a/examples/fermat/little/FLTbinomialScript.sml b/examples/fermat/little/FLTbinomialScript.sml index 518ef54516..63cfff82ce 100644 --- a/examples/fermat/little/FLTbinomialScript.sml +++ b/examples/fermat/little/FLTbinomialScript.sml @@ -49,7 +49,8 @@ open dividesTheory; (* for PRIME_POS *) (* ------------------------------------------------------------------------- *) (* Overloading: *) -(* +(* Definitions and Theorems (# are exported, ! are in compute): + From helpers: PRIME_FACTOR_PROPER |- !n. 1 < n /\ ~prime n ==> ?p. prime p /\ p < n /\ p divides n MULTIPLE_INTERVAL |- !n m. n divides m ==> diff --git a/examples/fermat/little/FLTeulerScript.sml b/examples/fermat/little/FLTeulerScript.sml index e299cbf59e..ee49b5a44c 100644 --- a/examples/fermat/little/FLTeulerScript.sml +++ b/examples/fermat/little/FLTeulerScript.sml @@ -61,7 +61,8 @@ open groupOrderTheory; (* for finite_group_Fermat *) (* ------------------------------------------------------------------------- *) (* Overloading: *) -(* +(* Definitions and Theorems (# are exported, ! are in compute): + From helperFunction: coprime_mod |- !m n. 0 < m /\ coprime m n ==> coprime m (n MOD m) coprime_sym |- !x y. coprime x y <=> coprime y x diff --git a/examples/fermat/little/FLTfixedpointScript.sml b/examples/fermat/little/FLTfixedpointScript.sml index 4ac2db671e..3a7f2d0181 100644 --- a/examples/fermat/little/FLTfixedpointScript.sml +++ b/examples/fermat/little/FLTfixedpointScript.sml @@ -52,7 +52,8 @@ open groupActionTheory; (* ------------------------------------------------------------------------- *) (* Overloading: *) -(* +(* Definitions and Theorems (# are exported, ! are in compute): + From groupInstances: Zadd_element |- !n x. x IN (Zadd n).carrier <=> x < n Zadd_card |- !n. CARD (Zadd n).carrier = n diff --git a/examples/fermat/little/FLTgroupScript.sml b/examples/fermat/little/FLTgroupScript.sml index 3ba729fdf8..7af727a597 100644 --- a/examples/fermat/little/FLTgroupScript.sml +++ b/examples/fermat/little/FLTgroupScript.sml @@ -59,7 +59,8 @@ open groupOrderTheory; (* for finite_group_Fermat *) (* ------------------------------------------------------------------------- *) (* Overloading: *) -(* +(* Definitions and Theorems (# are exported, ! are in compute): + From helperNum: EUCLID_LEMMA |- !p x y. prime p ==> ((x * y) MOD p = 0 <=> x MOD p = 0 \/ y MOD p = 0) diff --git a/examples/fermat/little/FLTnecklaceScript.sml b/examples/fermat/little/FLTnecklaceScript.sml index d624ecb821..5323620dec 100644 --- a/examples/fermat/little/FLTnecklaceScript.sml +++ b/examples/fermat/little/FLTnecklaceScript.sml @@ -50,7 +50,7 @@ open gcdTheory; (* for PRIME_GCD *) (* ------------------------------------------------------------------------- *) (* Overloading: *) -(* +(* Definitions and Theorems (# are exported, ! are in compute): Cycle and Necklaces: necklace_cycle |- !n a ls k. ls IN necklace n a ==> cycle k ls IN necklace n a diff --git a/examples/fermat/little/FLTnumberScript.sml b/examples/fermat/little/FLTnumberScript.sml index 70f31b2b08..715618a033 100644 --- a/examples/fermat/little/FLTnumberScript.sml +++ b/examples/fermat/little/FLTnumberScript.sml @@ -94,7 +94,7 @@ open EulerTheory; (* for residue_def *) (* ------------------------------------------------------------------------- *) (* Overloading: *) -(* +(* Definitions and Theorems (# are exported, ! are in compute): Mapping residues to a row of residues: row_def |- !n a x. row n a x = (a * x) MOD n diff --git a/examples/fermat/little/FLTpetersenScript.sml b/examples/fermat/little/FLTpetersenScript.sml index d1b6dc7c78..7782dd91b8 100644 --- a/examples/fermat/little/FLTpetersenScript.sml +++ b/examples/fermat/little/FLTpetersenScript.sml @@ -49,7 +49,7 @@ open groupActionTheory; (* ------------------------------------------------------------------------- *) (* Overloading: *) -(* +(* Definitions and Theorems (# are exported, ! are in compute): From groupInstances: Zadd_group |- !n. 0 < n ==> Group (Zadd n) diff --git a/examples/fermat/little/cycleScript.sml b/examples/fermat/little/cycleScript.sml index c0a664c254..9f951048b7 100644 --- a/examples/fermat/little/cycleScript.sml +++ b/examples/fermat/little/cycleScript.sml @@ -58,7 +58,8 @@ open gcdTheory; (* for GCD_0R, LINEAR_GCD *) (* Overloading: ! rotate1 ls = DROP 1 ls ++ TAKE 1 ls *) -(* +(* Definitions and Theorems (# are exported, ! are in compute): + Cycle Theory: cycle_def |- !n ls. cycle n ls = FUNPOW (\ls. rotate1 ls) n ls cycle_0 |- !ls. cycle 0 ls = ls diff --git a/examples/fermat/little/necklaceScript.sml b/examples/fermat/little/necklaceScript.sml index 5b12f7cb62..78a0318fd9 100644 --- a/examples/fermat/little/necklaceScript.sml +++ b/examples/fermat/little/necklaceScript.sml @@ -54,7 +54,7 @@ open helperListTheory; (* for LENGTH_NON_NIL, LIST_TO_SET_SING_IFF *) (* ------------------------------------------------------------------------- *) (* Overloading: *) -(* +(* Definitions and Theorems (# are exported, ! are in compute): Necklace: necklace_def |- !n a. necklace n a = diff --git a/examples/fermat/little/patternScript.sml b/examples/fermat/little/patternScript.sml index 7682a8d31e..467ad459c6 100644 --- a/examples/fermat/little/patternScript.sml +++ b/examples/fermat/little/patternScript.sml @@ -135,7 +135,7 @@ open dividesTheory; (* for prime_def, NOT_PRIME_0 *) l1 == l2 = similar l1 l2 (infix) closed R s = !x y. x IN s /\ R x y ==> y IN s *) -(* +(* Definitions and Theorems (# are exported, ! are in compute): Pattern Theory: similar_def |- !l1 l2. l1 == l2 <=> ?n. l2 = cycle n l1 diff --git a/examples/fermat/twosq/helperTwosqScript.sml b/examples/fermat/twosq/helperTwosqScript.sml index bbe809c65a..3630a5c6b1 100644 --- a/examples/fermat/twosq/helperTwosqScript.sml +++ b/examples/fermat/twosq/helperTwosqScript.sml @@ -37,15 +37,9 @@ open whileTheory; (* for HOARE_SPEC_DEF *) pairing f = !u x y. f u x /\ f u y ==> x = y unique_bool f a b = f a b /\ !x y. f x y ==> (x = a) /\ (y = b) *) -(* +(* Definitions and Theorems (# are exported, ! are in compute): Number Theorems: - square_def |- !n. square n <=> ?k. n = k * k - square_alt |- !n. square n <=> ?k. n = k ** 2 - square_eqn |- !n. square n <=> SQRT n ** 2 = n - square_0 |- square 0 - square_1 |- square 1 - prime_non_square |- !p. prime p ==> ~square p prime_non_quad |- !p. prime p ==> ~(4 divides p) prime_mod_eq_0 |- !p q. prime p /\ 1 < q ==> (p MOD q = 0 <=> q = p) even_by_mod_4 |- !n. EVEN n <=> n MOD 4 = 0 \/ n MOD 4 = 2 @@ -54,7 +48,6 @@ open whileTheory; (* for HOARE_SPEC_DEF *) mod_4_odd |- !n. ODD n <=> n MOD 4 IN {1; 3} mod_4_square |- !n. n ** 2 MOD 4 IN {0; 1} mod_4_not_squares |- !n. n MOD 4 = 3 ==> !x y. n <> x ** 2 + y ** 2 - half_add1_lt |- !n. 2 < n ==> 1 + HALF n < n Arithmetic Theorems: four_squares_identity |- !a b c d. b * d <= a * c ==> @@ -147,82 +140,7 @@ val _ = clear_overloads_on "SQ"; (* Overloading for a square n *) (* val _ = overload_on ("square", ``\n:num. ?k. n = k ** 2``); *) (* Make square in computeLib, cannot be an overload. *) - -(* Define square predicate. *) - -Definition square_def[nocompute]: - square (n:num) = ?k. n = k * k -End -(* use [nocompute] as this is not effective. *) - -(* Theorem: square n = ?k. n = k ** 2 *) -(* Proof: by square_def. *) -Theorem square_alt: - !n. square n = ?k. n = k ** 2 -Proof - simp[square_def] -QED - -(* Theorem: square n <=> (SQRT n) ** 2 = n *) -(* Proof: - If part: square n ==> (SQRT n) ** 2 = n - This is true by SQRT_SQ, EXP_2 - Only-if part: (SQRT n) ** 2 = n ==> square n - Take k = SQRT n for n = k ** 2. -*) -Theorem square_eqn[compute]: - !n. square n <=> (SQRT n) ** 2 = n -Proof - metis_tac[square_def, SQRT_SQ, EXP_2] -QED - -(* -EVAL ``square 10``; F -EVAL ``square 16``; T -*) - -(* Theorem: square 0 *) -(* Proof: by 0 = 0 * 0. *) -Theorem square_0: - square 0 -Proof - simp[square_def] -QED - -(* Theorem: square 1 *) -(* Proof: by 1 = 1 * 1. *) -Theorem square_1: - square 1 -Proof - simp[square_def] -QED - -(* Theorem: prime p ==> ~square p *) -(* Proof: - By contradiction, suppose (square p). - Then p = k * k by square_def - thus k divides p by divides_def - so k = 1 or k = p by prime_def - If k = 1, - then p = 1 * 1 = 1 by arithmetic - but p <> 1 by NOT_PRIME_1 - If k = p, - then p * 1 = p * p by arithmetic - or 1 = p by EQ_MULT_LCANCEL, NOT_PRIME_0 - but p <> 1 by NOT_PRIME_1 -*) -Theorem prime_non_square: - !p. prime p ==> ~square p -Proof - rpt strip_tac >> - `?k. p = k * k` by rw[GSYM square_def] >> - `k divides p` by metis_tac[divides_def] >> - `(k = 1) \/ (k = p)` by metis_tac[prime_def] >- - fs[NOT_PRIME_1] >> - `p * 1 = p * p` by metis_tac[MULT_RIGHT_1] >> - `1 = p` by metis_tac[EQ_MULT_LCANCEL, NOT_PRIME_0] >> - metis_tac[NOT_PRIME_1] -QED +(* see square_def in logPowerTheory. *) (* Theorem: prime p ==> ~(4 divides p) *) (* Proof: @@ -438,30 +356,6 @@ Proof QED -(* Theorem: 2 < n ==> (1 + HALF n < n) *) -(* Proof: - If EVEN n, - then 2 * HALF n = n by EVEN_HALF - so 2 + 2 * HALF n < n + n by 2 < n - or 1 + HALF n < n by arithmetic - If ~EVEN n, then ODD n by ODD_EVEN - then 1 + 2 * HALF n = 2 by ODD_HALF - so 1 + 2 * HALF n < n by 2 < n - also 2 + 2 * HALF n < n + n by 1 < n - or 1 + HALF n < n by arithmetic -*) -Theorem half_add1_lt: - !n. 2 < n ==> 1 + HALF n < n -Proof - rpt strip_tac >> - Cases_on `EVEN n` >| [ - `2 * HALF n = n` by rw[EVEN_HALF] >> - decide_tac, - `1 + 2 * HALF n = n` by rw[ODD_HALF, ODD_EVEN] >> - decide_tac - ] -QED - (* ------------------------------------------------------------------------- *) (* Arithmetic Theorems *) (* ------------------------------------------------------------------------- *) diff --git a/examples/fermat/twosq/involuteActionScript.sml b/examples/fermat/twosq/involuteActionScript.sml index aa79a023b0..b718cfc82e 100644 --- a/examples/fermat/twosq/involuteActionScript.sml +++ b/examples/fermat/twosq/involuteActionScript.sml @@ -37,7 +37,9 @@ open groupActionTheory; (* for fixed_points_def *) (* ------------------------------------------------------------------------- *) (* Involution and Action Documentation *) (* ------------------------------------------------------------------------- *) -(* +(* Overloading: +*) +(* Definitions and Theorems (# are exported, ! are in compute): FUNPOW Action: funpow_action |- !f X. f involute X ==> (Z2 act X) (FUNPOW f) diff --git a/examples/fermat/twosq/involuteFixScript.sml b/examples/fermat/twosq/involuteFixScript.sml index e47bc0c597..3863e41465 100644 --- a/examples/fermat/twosq/involuteFixScript.sml +++ b/examples/fermat/twosq/involuteFixScript.sml @@ -31,7 +31,7 @@ open arithmeticTheory pred_setTheory; (* Overloading: pair_by f = \x y. (x fpair y) f *) -(* +(* Definitions and Theorems (# are exported, ! are in compute): Helper Theorems: @@ -48,6 +48,8 @@ open arithmeticTheory pred_setTheory; pairs_def |- !f s. pairs f s = {x | x IN s /\ f x <> x} fixes_element |- !f s x. x IN fixes f s <=> x IN s /\ f x = x pairs_element |- !f s x. x IN pairs f s <=> x IN s /\ f x <> x + fixes_empty |- !f. fixes f {} = {} + pairs_empty |- !f. pairs f {} = {} fixes_subset |- !f s. fixes f s SUBSET s pairs_subset |- !f s. pairs f s SUBSET s fixes_finite |- !f s. FINITE s ==> FINITE (fixes f s) @@ -262,14 +264,16 @@ Proof QED (* Define the fixed points and pairs of involution. *) -Definition fixes_def: +Definition fixes_def[nocompute]: fixes f s = {x | x IN s /\ f x = x} End +(* use [nocompute] as this is not effective. *) (* Define the pairs of involution. *) -Definition pairs_def: +Definition pairs_def[nocompute]: pairs f s = {x | x IN s /\ f x <> x} End +(* use [nocompute] as this is not effective. *) (* Theorem: x IN fixes f s <=> x IN s /\ f x = x *) (* Proof: by fixes_def *) @@ -287,6 +291,22 @@ Proof rw[pairs_def] QED +(* Theorem: fixes f {} = {} *) +(* Proof: by fixes_def. *) +Theorem fixes_empty: + !f. fixes f {} = {} +Proof + simp[fixes_def] +QED + +(* Theorem: pairs f {} = {} *) +(* Proof: by pairs_def. *) +Theorem pairs_empty: + !f. pairs f {} = {} +Proof + simp[pairs_def] +QED + (* Theorem: fixes f s SUBSET s *) (* Proof: by fixes_def *) Theorem fixes_subset: diff --git a/examples/fermat/twosq/involuteScript.sml b/examples/fermat/twosq/involuteScript.sml index 9b8b1bd407..46807b00bb 100644 --- a/examples/fermat/twosq/involuteScript.sml +++ b/examples/fermat/twosq/involuteScript.sml @@ -33,12 +33,13 @@ open arithmeticTheory pred_setTheory; f endo s = !x. x IN s ==> f x IN s f involute s = !x. x IN s ==> f x IN s /\ (f (f x) = x) *) -(* +(* Definitions and Theorems (# are exported, ! are in compute): Helper Theorem: Involution: involute_endo |- !f s. f involute s ==> f endo s + involute_empty |- !f. f involute {} involute_inj |- !f s. f involute s ==> INJ f s s involute_surj |- !f s. f involute s ==> SURJ f s s involute_bij |- !f s. f involute s ==> f PERMUTES s @@ -82,6 +83,14 @@ Proof simp[] QED +(* Theorem: f involute {} *) +(* Proof: by MEMBER_NOT_EMPTY. *) +Theorem involute_empty: + !f. f involute {} +Proof + simp[] +QED + (* Theorem: f involute s ==> INJ f s s *) (* Proof: By INJ_DEF, this is to show: diff --git a/examples/fermat/twosq/iterateComposeScript.sml b/examples/fermat/twosq/iterateComposeScript.sml index 4dae6fc18f..880cde0833 100644 --- a/examples/fermat/twosq/iterateComposeScript.sml +++ b/examples/fermat/twosq/iterateComposeScript.sml @@ -38,7 +38,7 @@ open iterateComputeTheory; (* for iterate_while_thm *) (* ------------------------------------------------------------------------- *) (* Overloading: *) -(* +(* Definitions and Theorems (# are exported, ! are in compute): Helper Theorems: @@ -132,7 +132,7 @@ open iterateComputeTheory; (* for iterate_while_thm *) involute_involute_fix_odd_period_fix |- !f g s p x. FINITE s /\ f involute s /\ g involute s /\ x IN fixes f s /\ p = iterate_period (f o g) x /\ ODD p ==> - !j. 0 < j /\ j < p ==> (FUNPOW (f o g) j x IN fixes g s <=> (j = HALF p)) + !j. j < p ==> (FUNPOW (f o g) j x IN fixes g s <=> (j = HALF p)) Iteration Mate Involution: iterate_mate_def |- !f g x. iterate_mate f g x = @@ -1162,14 +1162,13 @@ QED <=> p - 1 - j MOD p = j MOD p by iterate_period_mod_eq <=> p - 1 - j = j by LESS_MOD, p - 1 - j < p, j < p <=> 2 * j + 1 = p by arithmetic - <=> 2 * j + 1 = 2 * p DIV 2 + 1 by ODD_HALF - <=> j = p DIV 2 by EQ_MULT_LCANCEL + <=> 2 * j + 1 = 2 * p DIV 2 + 1 by ODD_HALF + <=> j = p DIV 2 by EQ_MULT_LCANCEL *) Theorem involute_involute_fix_odd_period_fix: !f g s p x. FINITE s /\ f involute s /\ g involute s /\ x IN fixes f s /\ p = iterate_period (f o g) x /\ ODD p ==> - !j. 0 < j /\ j < p ==> - (FUNPOW (f o g) j x IN fixes g s <=> j = p DIV 2) + !j. j < p ==> (FUNPOW (f o g) j x IN fixes g s <=> j = p DIV 2) Proof rpt strip_tac >> `f o g PERMUTES s` by rw[involute_involute_permutes] >> @@ -1569,7 +1568,7 @@ iterate_while_thm Let h = HALF p, z = FUNPOW (f o g) h x. Then h <> 0 by HALF_EQ_0, p <> 0, p <> 1 - and h < p by HALF_LESS, p <> 0 + and h < p by HALF_LT, p <> 0 Note (f o g) PERMUTES s by involute_involute_permutes and p <> 0 by given ODD p and z IN fixes g s by involute_involute_fix_orbit_fix_odd [1] @@ -1620,7 +1619,7 @@ Proof last_x_assum (qspecl_then [`f`, `g`, `s`, `p`, `x`] strip_assume_tac) >> rfs[], `p <> 0` by metis_tac[EVEN, ODD_EVEN] >> - `h < p` by rw[HALF_LESS, Abbr`h`] >> + `h < p` by rw[HALF_LT, Abbr`h`] >> spose_not_then strip_assume_tac >> qabbrev_tac `y = FUNPOW (f o g) j x` >> `y IN s` by rfs[fixes_element, FUNPOW_closure, Abbr`y`] >> diff --git a/examples/fermat/twosq/iterateComputeScript.sml b/examples/fermat/twosq/iterateComputeScript.sml index 9622de833a..ed01b9b867 100644 --- a/examples/fermat/twosq/iterateComputeScript.sml +++ b/examples/fermat/twosq/iterateComputeScript.sml @@ -39,7 +39,7 @@ open whileTheory; (* for WHILE definition *) (* Overloading: ! iterate x f j = FUNPOW f j x *) -(* +(* Definitions and Theorems (# are exported, ! are in compute): Helper Theorems: @@ -887,7 +887,7 @@ WHILE |> ISPEC ``g:'a -> bool`` |> ISPEC ``b:'a -> 'a`` |> ISPEC ``FUNPOW b n x` (WHILE g b x = if g (FUNPOW b k x) then WHILE g b (FUNPOW b (k + 1) x) else FUNPOW b k x) *) (* Proof: - Note FUNPOW b (k + 1) x to b (FUNPOW b k x) by FUNPOW_SUC, ADD1 + Note FUNPOW b (k + 1) x = b (FUNPOW b k x) by FUNPOW_SUC, ADD1 By induction on k. Base: WHILE g b x = if g (FUNPOW b 0 x) then WHILE g b (b (FUNPOW b 0 x)) else FUNPOW b 0 x @@ -929,6 +929,13 @@ Proof metis_tac[iterate_while_eqn] QED +(* +It is not possible to prove the following, which would be nice; +WHILE g b x = FUNPOW b k x <=> (~g (FUNPOW b k x) /\ !j. j < k ==> g (FUNPOW b j x)) + +This is because WHILE is not known to terminate. +Those are pre-conditions for WHILE to terminate. +*) (* ------------------------------------------------------------------------- *) diff --git a/examples/fermat/twosq/iterationScript.sml b/examples/fermat/twosq/iterationScript.sml index 5a8a103dac..ba8b5218f3 100644 --- a/examples/fermat/twosq/iterationScript.sml +++ b/examples/fermat/twosq/iterationScript.sml @@ -28,7 +28,9 @@ open dividesTheory; (* for divides_def *) (* ------------------------------------------------------------------------- *) (* Iteration Period Documentation *) (* ------------------------------------------------------------------------- *) -(* +(* Overloading: +*) +(* Definitions and Theorems (# are exported, ! are in compute): Helper Theorems: @@ -98,9 +100,9 @@ open dividesTheory; (* for divides_def *) p = iterate_period f x ==> iterate_period (LINV f s) x = p iterate_period_iterate - |- !f s x y. FINITE s /\ f PERMUTES s /\ x IN s /\ - y = FUNPOW f j x ==> - iterate_period f y = iterate_period f x + |- !f s x y j. FINITE s /\ f PERMUTES s /\ x IN s /\ + y = FUNPOW f j x ==> + iterate_period f y = iterate_period f x *) (* ------------------------------------------------------------------------- *) @@ -878,8 +880,8 @@ QED Thus p = q by DIVIDES_ANTISYM, [1][2] *) Theorem iterate_period_iterate: - !f s x y. FINITE s /\ f PERMUTES s /\ x IN s /\ y = FUNPOW f j x ==> - iterate_period f y = iterate_period f x + !f s x y j. FINITE s /\ f PERMUTES s /\ x IN s /\ y = FUNPOW f j x ==> + iterate_period f y = iterate_period f x Proof rpt strip_tac >> qabbrev_tac `p = iterate_period f x` >> diff --git a/examples/fermat/twosq/twoSquaresScript.sml b/examples/fermat/twosq/twoSquaresScript.sml index 670cadc458..ad1f9a6bbf 100644 --- a/examples/fermat/twosq/twoSquaresScript.sml +++ b/examples/fermat/twosq/twoSquaresScript.sml @@ -23,6 +23,7 @@ open helperSetTheory; open helperFunctionTheory; open arithmeticTheory pred_setTheory; open dividesTheory; (* for divides_def, prime_def *) +open logPowerTheory; (* for prime_non_square *) open windmillTheory; @@ -58,7 +59,7 @@ open pairTheory; (* for ELIM_UNCURRY, PAIR_FST_SND_EQ, PAIR_EQ, FORALL_PROD *) (* ------------------------------------------------------------------------- *) (* Overloading: *) -(* +(* Definitions and Theorems (# are exported, ! are in compute): Helper Theorems: @@ -82,7 +83,7 @@ open pairTheory; (* for ELIM_UNCURRY, PAIR_FST_SND_EQ, PAIR_EQ, FORALL_PROD *) Fermat Two-Squares Existence: fermat_two_squares_exists_windmill - |- !p. prime p /\ (p MOD 4 = 1) ==> ?x y. p = windmill x y y + |- !p. prime p /\ (p MOD 4 = 1) ==> ?x y. p = windmill (x, y, y) fermat_two_squares_exists_odd_even |- !p. prime p /\ (p MOD 4 = 1) ==> ?(u,v). ODD u /\ EVEN v /\ (p = u ** 2 + v ** 2) @@ -158,7 +159,6 @@ open pairTheory; (* for ELIM_UNCURRY, PAIR_FST_SND_EQ, PAIR_EQ, FORALL_PROD *) (* Two Squares Fixes. *) (* ------------------------------------------------------------------------- *) - (* Theorem: prime p /\ (p MOD 4 = 1) ==> (fixes zagier (mills p) = {(1,1,p DIV 4)}) *) (* Proof: Let s = mills p, @@ -172,12 +172,12 @@ open pairTheory; (* for ELIM_UNCURRY, PAIR_FST_SND_EQ, PAIR_EQ, FORALL_PROD *) zagier (x,y,z) = (x,y,z) by fixes_element but x <> 0 by mills_prime_triple_nonzero so x = y by zagier_fix - Now p = windmill x x z by mills_element + Now p = windmill (x, x, z) by mills_element ==> x = 1, y = 1, z = k by windmill_trivial_prime (2) (1,1,k) IN a Note p = k * 4 + p MOD 4 by DIVISION = 4 * k + 1 by p MOD 4 = 1 - = windmill 1 1 k by windmill_trivial + = windmill (1, 1, k) by windmill_trivial so (1,1,k) IN s by mills_element and zagier (1,1,k) = (1,1,k) by zagier_1_1_z ==> (1,1,k) IN a by fixes_element @@ -195,7 +195,7 @@ Proof `p_1 = p_1'` by metis_tac[zagier_fix, mills_prime_triple_nonzero] >> metis_tac[windmill_trivial_prime, mills_element], `p = k * 4 + p MOD 4` by rw[DIVISION, Abbr`k`] >> - `_ = windmill 1 1 k` by rw[windmill_trivial] >> + `_ = windmill (1, 1, k)` by rw[windmill_trivial] >> `(1,1,k) IN s` by rw[mills_element, Abbr`s`] >> fs[fixes_element, zagier_1_1_z, Abbr`a`] ] @@ -322,7 +322,6 @@ Proof metis_tac[EVEN_ODD] QED - (* Theorem: prime p /\ (p MOD 4 = 1) ==> CARD (fixes flip (mills p)) <= 1 *) (* Proof: Let s = mills p, @@ -330,28 +329,28 @@ QED The goal is: CARD b <= 1. By contradiction, suppose CARD b > 1. Then CARD b <> 0, - so ?u. u IN b by CARD_EMPTY, MEMBER_NOT_EMPTY - Note u IN s by fixes_element - and ?x y. u = (x,y,y) by triple_parts, flip_fix - Thus p = windmill x y y by mills_element + so ?u. u IN b by CARD_EMPTY, MEMBER_NOT_EMPTY + Note u IN s by fixes_element + and ?x y. u = (x,y,y) by triple_parts, flip_fix + Thus p = windmill (x, y, y) by mills_element Also CARD b <> 1, - Then ~SING b by SING_CARD_1 - so b <> EMPTY by MEMBER_NOT_EMPTY - and ?v. v IN b /\ v <> u by SING_ONE_ELEMENT, b <> EMPTY - Note v IN s by fixes_element - and ?h k. v = (h,k,k) by triple_parts, flip_fix - Thus p = windmill h k k by mills_element + Then ~SING b by SING_CARD_1 + so b <> EMPTY by MEMBER_NOT_EMPTY + and ?v. v IN b /\ v <> u by SING_ONE_ELEMENT, b <> EMPTY + Note v IN s by fixes_element + and ?h k. v = (h,k,k) by triple_parts, flip_fix + Thus p = windmill (h, k, k) by mills_element Let c = 2 * y, d = 2 * k. - Now ODD p by odd_by_mod_4, p MOD 4 = 1 + Now ODD p by odd_by_mod_4, p MOD 4 = 1 and (p = x ** 2 + c ** 2) /\ ODD x by windmill_x_y_y and (p = h ** 2 + d ** 2) /\ ODD h by windmill_x_y_y but EVEN c /\ EVEN d by EVEN_DOUBLE - ==> (x = h) /\ (c = d) by fermat_two_squares_unique_odd_even - so (x = h) /\ (y = k) by EQ_MULT_LCANCEL - or v = u by PAIR_EQ + ==> (x = h) /\ (c = d) by fermat_two_squares_unique_odd_even + so (x = h) /\ (y = k) by EQ_MULT_LCANCEL + or v = u by PAIR_EQ This contradicts v <> u. *) Theorem flip_fixes_prime_card_upper: @@ -364,12 +363,12 @@ Proof `CARD b <> 0 /\ CARD b <> 1` by decide_tac >> `?u. u IN b` by metis_tac[CARD_EMPTY, MEMBER_NOT_EMPTY] >> `u IN s /\ ?x y. u = (x,y,y)` by metis_tac[fixes_element, triple_parts, flip_fix] >> - `p = windmill x y y` by fs[mills_element, Abbr`s`] >> + `p = windmill (x, y, y)` by fs[mills_element, Abbr`s`] >> `~SING b` by metis_tac[SING_CARD_1] >> `b <> EMPTY` by metis_tac[MEMBER_NOT_EMPTY] >> `?v. v IN b /\ v <> u` by metis_tac[SING_ONE_ELEMENT] >> `v IN s /\ ?h k. v = (h,k,k)` by metis_tac[fixes_element, triple_parts, flip_fix] >> - `p = windmill h k k` by fs[mills_element, Abbr`s`] >> + `p = windmill (h, k, k)` by fs[mills_element, Abbr`s`] >> qabbrev_tac `c = 2 * y` >> qabbrev_tac `d = 2 * k` >> `ODD p` by rfs[odd_by_mod_4] >> @@ -386,7 +385,7 @@ QED (* ------------------------------------------------------------------------- *) -(* Theorem: prime p /\ (p MOD 4 = 1) ==> ?x y. p = windmill x y y *) +(* Theorem: prime p /\ (p MOD 4 = 1) ==> ?x y. p = windmill (x, y, y) *) (* Proof: Let m = mills p, the solutions (x,y,z) of p = x ** 2 + 4 * y * z. Note ~square p by prime_non_square @@ -410,10 +409,10 @@ QED (flip (x, y, z) = (x, y, z)) by fixes_element so y = z by flip_fix or (x,y,y) in m by above - Thus p = windmill x y y by mills_element + Thus p = windmill (x, y, y) by mills_element *) Theorem fermat_two_squares_exists_windmill: - !p. prime p /\ (p MOD 4 = 1) ==> ?x y. p = windmill x y y + !p. prime p /\ (p MOD 4 = 1) ==> ?x y. p = windmill (x, y, y) Proof rpt strip_tac >> qabbrev_tac `m = mills p` >> @@ -441,7 +440,7 @@ QED (* Theorem: prime p /\ (p MOD 4 = 1) ==> ?(u,v). ODD u /\ EVEN v /\ (p = u ** 2 + v ** 2) *) (* Proof: - Note ?x y. p = windmill x y y by fermat_two_squares_exists_windmill + Note ?x y. p = windmill (x, y, y) by fermat_two_squares_exists_windmill = x ** 2 + (2 * y) ** 2 by windmill_by_squares Put (u, v) = (x, 2 * y). Remains to show: ODD u /\ EVEN v. @@ -459,7 +458,7 @@ Theorem fermat_two_squares_exists_odd_even: ?(u,v). ODD u /\ EVEN v /\ (p = u ** 2 + v ** 2) Proof rw[ELIM_UNCURRY] >> - `?x y. p = windmill x y y` by rw[fermat_two_squares_exists_windmill] >> + `?x y. p = windmill (x, y, y)` by rw[fermat_two_squares_exists_windmill] >> `_ = x ** 2 + (2 * y) ** 2` by rw[windmill_by_squares] >> qabbrev_tac `u = x` >> qabbrev_tac `v = 2 * y` >> @@ -479,13 +478,12 @@ QED (* Fermat Two-Squares Theorem. *) (* ------------------------------------------------------------------------- *) - (* Theorem: prime p /\ (p MOD 4 = 1) ==> SING (fixes flip (mills p)) *) (* Proof: Let s = mills p, b = fixes flip s. The goal is: SING b. - Note ?x y. p = windmill x y y + Note ?x y. p = windmill (x, y, y) by fermat_two_squares_exists_windmill Let u = (x,y,y). Then u IN s by mills_element @@ -494,7 +492,7 @@ QED !t. t IN b ==> t = u. Note t IN s by fixes_element and ?h k. t = (h,k,k) by triple_parts, flip_fix - Thus p = windmill h k k by mills_element + Thus p = windmill (h, k, k) by mills_element Let c = 2 * y, d = 2 * k. @@ -510,7 +508,7 @@ Theorem flip_fixes_prime_sing: !p. prime p /\ (p MOD 4 = 1) ==> SING (fixes flip (mills p)) Proof rpt strip_tac >> - `?x y. p = windmill x y y` by rw[fermat_two_squares_exists_windmill] >> + `?x y. p = windmill (x, y, y)` by rw[fermat_two_squares_exists_windmill] >> qabbrev_tac `s = mills p` >> qabbrev_tac `b = fixes flip s` >> qabbrev_tac `u = (x,y,y)` >> @@ -521,7 +519,7 @@ Proof (rewrite_tac[EQ_IMP_THM] >> simp[]) >> rpt strip_tac >> `x' IN s /\ ?h k. x' = (h,k,k)` by metis_tac[fixes_element, triple_parts, flip_fix] >> - `p = windmill h k k` by fs[mills_element, Abbr`s`] >> + `p = windmill (h, k, k)` by fs[mills_element, Abbr`s`] >> qabbrev_tac `c = 2 * y` >> qabbrev_tac `d = 2 * k` >> `ODD p` by rfs[odd_by_mod_4] >> @@ -533,7 +531,6 @@ Proof simp[Abbr`u`] QED - (* Theorem: prime p /\ (p MOD 4 = 1) ==> (fixes flip (mills p) = {(let u = (1,1,p DIV 4) ; @@ -652,7 +649,6 @@ QED (* Fermat Two-Squares Algorithm. *) (* ------------------------------------------------------------------------- *) - (* Theorem: (iterate_period (zagier o flip) (1,1,z) = 1) <=> (z = 1) *) (* Proof: By iterate_period_thm, this is to show: @@ -667,7 +663,6 @@ Proof rw[iterate_period_thm, zagier_flip_1_1_z] QED - (* Theorem: prime p /\ (p MOD 4 = 1) /\ (u = (1, 1, p DIV 4)) /\ (n = iterate_period (zagier o flip) u) /\ (g = \(x,y,z). y <> z) ==> !j. j < n DIV 2 ==> g (FUNPOW (zagier o flip) j u) /\ @@ -686,7 +681,7 @@ QED so f PERMUTES s by involute_involute_permutes Also u IN s by mills_element_trivial and 0 < n by iterate_period_pos - so h < n by HALF_LESS, 0 < n + so h < n by HALF_LT, 0 < n Without assuming the following: Note fixes flip s = {v} by flip_fixes_prime @@ -694,8 +689,7 @@ QED Note fixes zagier s = {u} by zagier_fixes_prime so ODD n by involute_involute_fix_sing_period_odd Then use involute_involute_fix_odd_period_fix: - !j. 0 < j /\ j < n ==> - (FUNPOW (zagier o flip) j u IN fixes flip s <=> (j = h)) + !j. j < n ==> (FUNPOW (zagier o flip) j u IN fixes flip s <=> (j = h)) Case: n = 1, Then h = 0 by HALF_EQ_0, n <> 0 @@ -722,11 +716,7 @@ QED Now w IN s by FUNPOW_closure and flip w = w by flip_fix ==> w IN (fixes flip u} by fixes_element - If j = 0, w = u by FUNPOW_0 - Then z = 1, so n = 1 by zagier_flip_1_1_z_period, PAIR_EQ - which contradicts n <> 1. - If j <> 0, - Then j = h by involute_involute_fix_odd_period_fix + Then j = h by involute_involute_fix_odd_period_fix, j < n which contradicts j < h. *) Theorem flip_fixes_iterates_prime: @@ -744,26 +734,30 @@ Proof `FINITE s` by metis_tac[mills_non_square_finite] >> `zagier involute s` by metis_tac[zagier_involute_mills_prime] >> `flip involute s` by metis_tac[flip_involute_mills] >> + `fixes zagier s = {u}` by metis_tac[zagier_fixes_prime] >> + qabbrev_tac `X = (u = (1,1,p DIV 4))` >> + qabbrev_tac `Y = (n = iterate_period f u)` >> + qabbrev_tac `Z = (g = (\(x,y,z). y <> z))` >> + drule_then strip_assume_tac involute_involute_fix_sing_period_odd >> + last_x_assum (qspecl_then [`zagier`, `flip`, `n`, `u`] strip_assume_tac) >> + rfs[] >> `f PERMUTES s` by fs[involute_involute_permutes, Abbr`f`] >> - `u IN s` by rw[mills_element_trivial, Abbr`s` ] >> + `u IN s` by rw[mills_element_trivial, Abbr`s`, Abbr`X`] >> `0 < n` by metis_tac[iterate_period_pos] >> - `h < n` by rw[HALF_LESS, Abbr`h`] >> - `fixes zagier s = {u}` by metis_tac[zagier_fixes_prime] >> - drule_then strip_assume_tac (involute_involute_fix_sing_period_odd |> ISPEC ``zagier``) >> - last_x_assum (qspecl_then [`flip`, `n`, `u`] strip_assume_tac) >> - `ODD n` by rfs[] >> + `h < n` by rw[HALF_LT, Abbr`h`] >> Cases_on `n = 1` >| [ `h = 0` by rw[Abbr`h`] >> `v = u` by rw[Abbr`v`] >> `_ = (1,1,1)` by metis_tac[zagier_flip_1_1_z_period] >> - rfs[], + rfs[Abbr`Z`], `h <> 0` by rw[HALF_EQ_0, Abbr`h`] >> `0 < h` by decide_tac >> - drule_then strip_assume_tac (involute_involute_fix_odd_period_fix |> ISPEC ``f: num # num # num -> num # num # num``) >> - `!j. 0 < j /\ j < n ==> - (FUNPOW (zagier o flip) j u IN fixes flip s <=> (j = HALF n))` by rfs[] >> + drule_then strip_assume_tac involute_involute_fix_odd_period_fix >> + last_x_assum (qspecl_then [`zagier`, `flip`, `n`, `u`] strip_assume_tac) >> + rfs[] >> + qunabbrev_tac `Z` >> `~g v` by - (`FUNPOW (zagier o flip) h u IN fixes flip s <=> (h = HALF n)` by rfs[] >> + (`FUNPOW (zagier o flip) h u IN fixes flip s <=> (h = HALF n)` by metis_tac[] >> `v IN fixes flip s` by metis_tac[] >> `?x y z. v = (x,y,z)` by rw[triple_parts] >> `y = z` by metis_tac[fixes_element, flip_fix] >> @@ -776,19 +770,14 @@ Proof `y = z` by fs[] >> `w IN s` by rw[FUNPOW_closure, Abbr`w`] >> `w IN (fixes flip s)` by fs[flip_fix, fixes_element] >> - Cases_on `j = 0` >| [ - `w = u` by fs[Abbr`w`] >> - metis_tac[zagier_flip_1_1_z_period, PAIR_EQ], - `0 < j` by decide_tac >> - `FUNPOW (zagier o flip) j u IN fixes flip s <=> (j = HALF n)` by rfs[] >> - `j = h` by metis_tac[] >> - decide_tac - ] + `FUNPOW (zagier o flip) j u IN fixes flip s <=> (j = HALF n)` by metis_tac[LESS_TRANS] >> + `j = h` by metis_tac[] >> + decide_tac ] QED (* This proof is using: - zagier_flip_1_1_z_period and involute_involute_fix_odd_period_fix. + involute_involute_fix_odd_period_fix. In part4, there is another proof using: flip_fixes_prime, which depends on fermat_two_squares_unique_odd_even. *) @@ -798,10 +787,9 @@ QED (* ------------------------------------------------------------------------- *) (* Define the exit condition *) -val found_def = Define` +Definition found_def: found (x:num, y:num, z:num) <=> (y = z) -`; - +End (* Theorem: $~ o found = (\(x,y,z). y <> z) *) (* Proof: by found_def, FUN_EQ_THM. *) @@ -814,9 +802,9 @@ QED (* Idea: use WHILE for search. Develop theory in iterateCompute. *) (* Compute two squares of Fermat's theorem by WHILE loop. *) -val two_sq_def = Define` +Definition two_sq_def: two_sq n = WHILE ($~ o found) (zagier o flip) (1,1,n DIV 4) -`; +End (* > EVAL ``two_sq 5``; = (1,2): thm (1,1,1) @@ -826,7 +814,6 @@ val two_sq_def = Define` > EVAL ``two_sq 97``; = (9,4): thm (9,2,2) *) - (* Theorem: two_sq n = WHILE (\(x,y,z). y <> z) (zagier o flip) (1, 1, n DIV 4) *) (* Proof: by two_sq_def, found_not. *) Theorem two_sq_alt: @@ -885,7 +872,6 @@ QED (* Very good -- nice and simple! *) - (* Theorem: prime p /\ (p MOD 4 = 1) ==> HOARE_SPEC (fixes zagier (mills p)) (WHILE ($~ o found) (zagier o flip)) @@ -924,7 +910,7 @@ QED Also 0 < n by iterate_period_pos, u IN s and ODD n by involute_involute_fix_sing_period_odd so n <> 2 by EVEN_2, ODD_EVEN - ==> 1 + h < n by half_add1_lt, 2 < n + ==> 1 + h < n by HALF_ADD1_LT, 2 < n or h < n - 1 by arithmetic Now ~g v /\ (!j. j < h ==> g (FUNPOW f j u)) @@ -967,7 +953,7 @@ Proof last_x_assum (qspecl_then [`zagier`, `flip`, `n`, `u`] strip_assume_tac) >> `ODD n` by rfs[] >> `n <> 2` by metis_tac[EVEN_2, ODD_EVEN] >> - `1 + h < n` by rw[half_add1_lt, Abbr`h`] >> + `1 + h < n` by rw[HALF_ADD1_LT, Abbr`h`] >> `h < n - 1` by decide_tac >> drule_then strip_assume_tac iterate_while_hoare >> last_x_assum (qspecl_then [`u`, `f`, `n-1`, `n`, `g`, `h`] strip_assume_tac) >> @@ -976,7 +962,6 @@ Proof ] QED - (* Theorem: prime p /\ (p MOD 4 = 1) ==> let (x,y,z) = WHILE ($~ o found) (zagier o flip) (1,1,p DIV 4) in p = x ** 2 + (y + z) ** 2 *) @@ -999,8 +984,8 @@ QED and w IN b by b w, function as set so w IN s /\ y = z by fixes_element, flip_fix Thus p - = windmill x y z by mills_element, w IN s - = windmill x y y by y = z + = windmill (x, y, z) by mills_element, w IN s + = windmill (x, y, y) by y = z = x ** 2 + (2 * y) ** 2 by windmill_by_squares = x ** 2 + (y + z) ** 2 by arithmetic, y = z *) @@ -1023,9 +1008,9 @@ QED (* A beautiful theorem! *) (* Define the algorithm. *) -val two_squares_def = Define` +Definition two_squares_def: two_squares n = let (x,y,z) = two_sq n in (x, y + z) -`; +End (* > EVAL ``two_squares 5``; = (1,2) @@ -1037,7 +1022,6 @@ val two_squares_def = Define` = [(1,2); (3,2); (1,4); (5,2); (1,6); (5,4); (7,2); (5,6); (3,8); (5,8); (9,4)]: thm *) - (* Theorem: prime p /\ (p MOD 4 = 1) ==> let (u,v) = two_squares p in (p = u ** 2 + v ** 2) *) (* Proof: by two_squares_def, two_sq_def, two_sq_while_thm. *) @@ -1061,7 +1045,7 @@ QED Then t IN fixes flip (mills p) by two_sq_thm and ?x y z. t = (x,y,z) by triple_parts ==> (x,y,z) IN mills p /\ (y = z) by fixes_element, flip_fix - so p = windmill x y y by mills_element + so p = windmill (x, y, y) by mills_element = x ** 2 + (2 * y) ** 2 by windmill_by_squares = x ** 2 + (y + z) ** 2 by y = z = u ** 2 + v ** 2 by two_squares_def @@ -1075,7 +1059,7 @@ Proof `t IN fixes flip (mills p)` by rw[two_sq_thm, Abbr`t`] >> `?x y z. t = (x,y,z)` by rw[triple_parts] >> `(x,y,z) IN mills p /\ (y = z)` by fs[fixes_element, flip_fix] >> - `p = windmill x y y` by fs[mills_element] >> + `p = windmill (x, y, y)` by fs[mills_element] >> simp[windmill_by_squares] QED @@ -1152,12 +1136,12 @@ QED fixed_points (FUNPOW zagier) Z2 (mills p) = {(1,1,p DIV 4)} *) (* Proof: By fixes_def, mills_def, this is to show: - (1) p = windmill x y z /\ zagier (x,y,z) = (x,y,z) ==> (x,y,z) = (1,1,p DIV 4) + (1) p = windmill (x, y, z) /\ zagier (x,y,z) = (x,y,z) ==> (x,y,z) = (1,1,p DIV 4) Note ~square p by prime_non_square and x <> 0 by mills_element, mills_triple_nonzero so x = y by zagier_fix ==> (x,y,z) = (1,1,p DIV 4) by windmill_trivial_prime - (2) p MOD 4 = 1 ==> p = windmill 1 1 (p DIV 4) + (2) p MOD 4 = 1 ==> p = windmill (1, 1, p DIV 4) This is true by windmill_trivial_prime (3) a < 2 ==> FUNPOW zagier p (1,1,p DIV 4) = (1,1,p DIV 4) When a = 0, true by FUNPOW_0 @@ -1199,7 +1183,7 @@ QED so ?x y z. t = (x, y, z) by triple_parts and x <> 0 by mills_triple_nonzero, ~square p, p MOD 4 = 1 ==> x = y by zagier_fix - Note p = windmill x y z by mills_element + Note p = windmill (x, y, z) by mills_element ==> (x,y,z) = (1,1,p DIV 4) by windmill_trivial_prime (2) (1,1,p DIV 4) IN a diff --git a/examples/fermat/twosq/windmillScript.sml b/examples/fermat/twosq/windmillScript.sml index 02c652792e..bc70f2742f 100644 --- a/examples/fermat/twosq/windmillScript.sml +++ b/examples/fermat/twosq/windmillScript.sml @@ -28,33 +28,38 @@ open gcdTheory; (* for P_EUCLIDES *) open pairTheory; (* for FORALL_PROD, PAIR_EQ *) +(* val _ = load "GaussTheory"; *) +open logrootTheory logPowerTheory GaussTheory EulerTheory; (* for SQRT, divisors_upper_bound *) + (* ------------------------------------------------------------------------- *) (* Windmills and Involutions Documentation *) (* ------------------------------------------------------------------------- *) -(* +(* Overloading: +*) +(* Definitions and Theorems (# are exported, ! are in compute): Helper Theorem: triple_parts |- !t. ?x y z. t = (x,y,z) Windmill Theory: - windmill_def |- !x y z. windmill x y z = x ** 2 + 4 * y * z - windmill_eq_0 |- !x y z. windmill x y z = 0 <=> x = 0 /\ y * z = 0 - windmill_comm |- !x y z. windmill x y z = windmill x z y - windmill_trivial |- !k. windmill 1 1 k = 4 * k + 1 - windmill_by_squares |- !x y. windmill x y y = x ** 2 + (2 * y) ** 2 - windmill_x_y_y |- !n x y. n = windmill x y y ==> + windmill_def |- !x y z. windmill (x, y, z) = x ** 2 + 4 * y * z + windmill_eq_0 |- !x y z. windmill (x, y, z) = 0 <=> x = 0 /\ y * z = 0 + windmill_comm |- !x y z. windmill (x, y, z) = windmill (x, z, y) + windmill_trivial |- !k. windmill (1, 1, k) = 4 * k + 1 + windmill_by_squares |- !x y. windmill (x, y, y) = x ** 2 + (2 * y) ** 2 + windmill_x_y_y |- !n x y. n = windmill (x, y, y) ==> n = x ** 2 + (2 * y) ** 2 /\ (ODD n <=> ODD x) windmill_trivial_prime |- !p. prime p /\ p MOD 4 = 1 ==> - !x z. p = windmill x x z <=> x = 1 /\ z = p DIV 4 + !x z. p = windmill (x, x, z) <=> x = 1 /\ z = p DIV 4 - Mills Theory: - mills_def |- !n. mills n = {(x,y,z) | n = windmill x y z} - mills_element |- !n x y z. (x,y,z) IN mills n <=> n = windmill x y z + Set of windmills: + mills_def |- !n. mills n = {(x,y,z) | n = windmill (x, y, z)} + mills_element |- !n x y z. (x,y,z) IN mills n <=> n = windmill (x, y, z) mills_element_flip |- !n x y z. (x,y,z) IN mills n ==> (x,z,y) IN mills n mills_element_triple |- !n t. t IN mills n <=> - ?x y z. t = (x,y,z) /\ n = windmill x y z + ?x y z. t = (x,y,z) /\ n = windmill (x, y, z) mills_element_trivial |- !n. n MOD 4 = 1 ==> (1,1,n DIV 4) IN mills n mills_0 |- mills 0 = {(0,0,n) | n IN univ(:num)} UNION {(0,n,0) | n IN univ(:num)} @@ -115,14 +120,15 @@ open pairTheory; (* for FORALL_PROD, PAIR_EQ *) zagier_x_0_0 |- !x. zagier (x,0,0) = (x,x,0) zagier_0_y_0 |- !y. zagier (0,y,0) = (0,0,y) zagier_0_0_z |- !z. zagier (0,0,z) = (0,z,0) + zagier_0_1_z |- !z. zagier (0,1,z) = if z = 0 then (0,0,1) else (2,1,z - 1) zagier_0_0_0 |- zagier (0,0,0) = (0,0,0) zagier_x_y_y |- !x y. zagier (x,y,y) = if x < 2 * y then (2 * y - x,y,x) else (x - 2 * y,x,y) zagier_fix |- !x y z. x <> 0 ==> (zagier (x,y,z) = (x,y,z) <=> x = y) zagier_x_x_z |- !x z. x <> 0 ==> zagier (x,x,z) = (x,x,z) zagier_closure |- !n x y z. (x,y,z) IN mills n ==> zagier (x,y,z) IN mills n - zagier_closure_alt |- !n t. t IN mills n ==> zagier t IN mills n - zagier_involute |- !x y z. x <> 0 /\ z <> 0 ==> zagier (zagier (x,y,z)) = (x,y,z) + zagier_closure_alt |- !n t. t IN mills n ==> zagier t IN mills n + zagier_involute |- !x y z. x <> 0 /\ z <> 0 ==> zagier (zagier (x,y,z)) = (x,y,z) zagier_involute_alt |- !x y z. x * z <> 0 ==> zagier (zagier (x,y,z)) = (x,y,z) zagier_involute_thm |- !t. FST t <> 0 /\ SND (SND t) <> 0 ==> zagier (zagier t) = t doublet_def |- !x y z. doublet (x,y,z) = x * z @@ -155,25 +161,27 @@ open pairTheory; (* for FORALL_PROD, PAIR_EQ *) gap_flip_thm |- !t. gap (flip t) = gap t Zagier and Flip: + zagier_flip_eqn |- !x y z. (zagier o flip) (x,y,z) = + if x < z - y then (x + 2 * y,y,z - y - x) + else if x < 2 * z then (2 * z - x,z,x + y - z) + else (x - 2 * z,x + y - z,z) zagier_flip_1_1_z |- !z. (zagier o flip) (1,1,z) = if z = 0 then (1,2,0) else if z = 1 then (1,1,1) else if z = 2 then (3,2,0) else (3,1,z - 2) - - Computation of (mills n): - tuples_helper_def |- (!k. tuples_helper k 0 = []) /\ - !k n. tuples_helper k (SUC n) = - ZIP (GENLIST (K (SUC n)) k, - GENLIST SUC k) ++ tuples_helper k n - tuples_def |- !k. tuples k = tuples_helper k k - triples_helper_def |- (!k. triples_helper k 0 = []) /\ - !k n. triples_helper k (SUC n) = - ZIP (GENLIST (K (SUC n)) (k * k), - tuples k) ++ triples_helper k n - triples_def |- !k. triples k = triples_helper k k - mills_of_def |- !n. mills_of n = - FILTER (\(x,y,z). n = windmill x y z) (triples n) + zagier_flip_0_1_z |- !z. (zagier o flip) (0,1,z) = + if z = 0 then (0,1,0) + else (2,1,z - 1) + zagier_flip_0_y_z |- !y z. (zagier o flip) (0,y,z) = + if 0 < z - y then (2 * y,y,z - y) + else if 0 < z then (2 * z,z,y - z) + else (0,y,0) + zagier_flip_x_0_z |- !x z. (zagier o flip) (x,0,z) = + if x < z then (x,0,z - x) + else if x < 2 * z then (2 * z - x,z,x - z) + else (x - 2 * z,x - z,z) + zagier_flip_x_y_0 |- !x y. (zagier o flip) (x,y,0) = (x,x + y,0) *) (* ------------------------------------------------------------------------- *) @@ -185,12 +193,7 @@ open pairTheory; (* for FORALL_PROD, PAIR_EQ *) Theorem triple_parts: !(t :num # num # num). ?x y z. t = (x, y, z) Proof - rpt strip_tac >> - qabbrev_tac `x = FST t` >> - qabbrev_tac `y = FST (SND t)` >> - qabbrev_tac `z = SND (SND t)` >> - `t = (x, y, z)` by rw[Abbr`x`, Abbr`y`, Abbr`z`] >> - metis_tac[] + metis_tac[PAIR] QED (* ------------------------------------------------------------------------- *) @@ -345,65 +348,65 @@ QED (* Part 1: A windmill *) (* ------------------------------------------------------------------------- *) -(* Define windmill of three numbers *) +(* Define windmill of a triple *) Definition windmill_def: - windmill x y z = x ** 2 + 4 * y * z + windmill (x, y, z) = x ** 2 + 4 * y * z End -(* Theorem: windmill x y z = 0 <=> x = 0 /\ y * z = 0 *) +(* Theorem: windmill (x, y, z) = 0 <=> x = 0 /\ y * z = 0 *) (* Proof: - windmill x y z = 0 + windmill (x, y, z) = 0 <=> x ** 2 + 4 * y * z = 0 by windmill_def <=> x * x + 4 * y * z = 0 by EXP_2 <=> (x * x = 0) /\ (4 * y * z = 0) by ADD_EQ_0 <=> (x = 0) /\ (y * z = 0) by MULT_EQ_0 *) Theorem windmill_eq_0: - !x y z. windmill x y z = 0 <=> x = 0 /\ y * z = 0 + !x y z. windmill (x, y, z) = 0 <=> x = 0 /\ y * z = 0 Proof simp[windmill_def] QED -(* Theorem: windmill x y z = windmill x z y *) +(* Theorem: windmill (x, y, z) = windmill (x, z, y) *) (* Proof: - windmill x y z + windmill (x, y, z) = x ** 2 + 4 * y * z by windmill_def = x ** 2 + 4 * z * y by MULT_COMM - = windmill x z y by windmill_def + = windmill (x, z, y) by windmill_def *) Theorem windmill_comm: - !x y z. windmill x y z = windmill x z y + !x y z. windmill (x, y, z) = windmill (x, z, y) Proof simp[windmill_def] QED -(* Theorem: windmill 1 1 k = 4 * k + 1 *) +(* Theorem: windmill (1, 1, k) = 4 * k + 1 *) (* Proof: - windmill 1 1 k + windmill (1, 1, k) = 1 ** 2 + 4 * 1 * k by windmill_def = 1 + 4 * k by arithmetic = 4 * k + 1 by arithmetic *) Theorem windmill_trivial: - !k. windmill 1 1 k = 4 * k + 1 + !k. windmill (1, 1, k) = 4 * k + 1 Proof simp[windmill_def] QED -(* Theorem: windmill x y y = x ** 2 + (2 * y) ** 2 *) +(* Theorem: windmill (x, y, y) = x ** 2 + (2 * y) ** 2 *) (* Proof: - windmill x y y + windmill (x, y, y) = x ** 2 + 4 * y * y by windmill_def = x ** 2 + (2 * y) * (2 * y) by arithmetic = x ** 2 + (2 * y) ** 2 by EXP_2 *) Theorem windmill_by_squares: - !x y. windmill x y y = x ** 2 + (2 * y) ** 2 + !x y. windmill (x, y, y) = x ** 2 + (2 * y) ** 2 Proof simp[windmill_def, EXP_BASE_MULT] QED -(* Theorem: n = windmill x y y ==> +(* Theorem: n = windmill (x, y, y) ==> n = x ** 2 + (2 * y) ** 2 /\ (ODD n <=> ODD x) *) (* Proof: Note n = x ** 2 + (2 * y) ** 2 by windmill_by_squares @@ -414,7 +417,7 @@ QED <=> ODD x by ODD_SQ *) Theorem windmill_x_y_y: - !n x y. n = windmill x y y ==> + !n x y. n = windmill (x, y, y) ==> n = x ** 2 + (2 * y) ** 2 /\ (ODD n <=> ODD x) Proof ntac 4 strip_tac >> @@ -426,13 +429,13 @@ Proof QED (* Theorem: prime p /\ p MOD 4 = 1 ==> - !x z. p = windmill x x z <=> x = 1 /\ z = p DIV 4 *) + !x z. p = windmill (x, x, z) <=> x = 1 /\ z = p DIV 4 *) (* Proof: Let k = p DIV 4, Then p = 4 * k + 1 by DIVISION - If part: p = windmill x x z ==> ((x = 1) /\ (z = k)) - Note p = windmill x x z + If part: p = windmill (x, x, z) ==> ((x = 1) /\ (z = k)) + Note p = windmill (x, x, z) = x ** 2 + 4 * x * z by windmill_def = x * (x + 4 * z) by arithmetic Thus x divides p by divides_def @@ -445,13 +448,13 @@ QED then p + 4 * z = 1 by EQ_MULT_LCANCEL but 1 < p by ONE_LT_PRIME and this is impossible. - Only-if part: p = windmill 1 1 k + Only-if part: p = windmill (1, 1, k) Note p = 4 * k + 1 - = windmill 1 1 k by windmill_trivial + = windmill (1, 1, k) by windmill_trivial *) Theorem windmill_trivial_prime: !p. prime p /\ p MOD 4 = 1 ==> - !x z. p = windmill x x z <=> x = 1 /\ z = p DIV 4 + !x z. p = windmill (x, x, z) <=> x = 1 /\ z = p DIV 4 Proof rpt strip_tac >> qabbrev_tac `k = p DIV 4` >> @@ -465,10 +468,7 @@ Proof `x divides p` by metis_tac[divides_def] >> `(x = 1) \/ (x = p)` by metis_tac[prime_def] >- fs[] >> - fs[] >> - `p + 4 * z = 1` by metis_tac[MULT_RIGHT_1, NOT_PRIME_0, EQ_MULT_LCANCEL] >> - `1 < p` by rw[ONE_LT_PRIME] >> - decide_tac, + fs[], rw[windmill_trivial] ] QED @@ -480,14 +480,14 @@ QED (* The set of windmills of a number *) Definition mills_def[nocompute]: - mills n = {(x,y,z) | n = windmill x y z} + mills n = {(x,y,z) | n = windmill (x, y, z)} End (* use [nocompute] as this is not effective. *) -(* Theorem: (x, y, z) IN mills n <=> n = windmill x y z *) +(* Theorem: (x, y, z) IN mills n <=> n = windmill (x, y, z) *) (* Proof: by mills_def. *) Theorem mills_element: - !n x y z. (x, y, z) IN mills n <=> n = windmill x y z + !n x y z. (x, y, z) IN mills n <=> n = windmill (x, y, z) Proof simp[mills_def] QED @@ -495,11 +495,11 @@ QED (* Theorem: (x, y, z) IN mills n ==> (x, z, y) IN mills n *) (* Proof: (x, y, z) IN mills n - <=> n = windmill x y z by mills_def - <=> n = x ** 2 + 4 * y * z by windmill_def - <=> n = x ** 2 + 4 * z * y by MULT_COMM - <=> n = windmill x z y by windmill_def - <=> (x, z, y) IN mills n by mills_def + <=> n = windmill (x, y, z) by mills_def + <=> n = x ** 2 + 4 * y * z by windmill_def + <=> n = x ** 2 + 4 * z * y by MULT_COMM + <=> n = windmill (x, z, y) by windmill_def + <=> (x, z, y) IN mills n by mills_def *) Theorem mills_element_flip: !n x y z. (x, y, z) IN mills n ==> (x, z, y) IN mills n @@ -507,10 +507,10 @@ Proof simp[mills_def, windmill_def] QED -(* Theorem: t IN mills n <=> ?x y z. (t = (x, y, z)) /\ n = windmill x y z *) +(* Theorem: t IN mills n <=> ?x y z. (t = (x, y, z)) /\ n = windmill (x, y, z) *) (* Proof: by mills_def. *) Theorem mills_element_triple: - !n t. t IN mills n <=> ?x y z. (t = (x, y, z)) /\ n = windmill x y z + !n t. t IN mills n <=> ?x y z. (t = (x, y, z)) /\ n = windmill (x, y, z) Proof simp[mills_def, FORALL_PROD] QED @@ -519,7 +519,7 @@ QED (* Proof: Note n = (n DIV 4) * 4 + n MOD 4 by DIVISION = 4 * (n DIV 4) + 1 by arithmetic - = windmill 1 1 (n DIV 4) by windmill_trivial + = windmill (1, 1, (n DIV 4)) by windmill_trivial Thus (1, 1, n DIV 4) IN (mills n) by mills_element *) Theorem mills_element_trivial: @@ -527,7 +527,7 @@ Theorem mills_element_trivial: Proof rpt strip_tac >> `n = (n DIV 4) * 4 + n MOD 4` by rw[DIVISION] >> - `_ = windmill 1 1 (n DIV 4)` by rw[windmill_trivial] >> + `_ = windmill (1, 1, (n DIV 4))` by rw[windmill_trivial] >> fs[mills_element] QED @@ -535,7 +535,7 @@ QED {(0,n,0) | n IN univ(:num)} *) (* Proof: Let (x,y,z) IN mills 0 - Then 0 = windmill x y z by mills_def + Then 0 = windmill (x, y, z) by mills_def = x ** 2 + 4 * y * z by windmill_def ==> x ** 2 = 0 /\ 4 * y * z = 0 by ADD_EQ_0 ==> x * x = 0 /\ y * z = 0 by EXP_2 @@ -569,7 +569,7 @@ QED (* Proof: Let (x,y,z) IN mills 1 Note 4 * y * z <> 1 by MULT_EQ_1 - Then 1 = windmill x y z by mills_def + Then 1 = windmill (x, y, z) by mills_def = x ** 2 + 4 * y * z by windmill_def <=> x ** 2 = 1 /\ 4 * y * z = 0 by ADD_EQ_1 <=> x * x = 1 /\ y * z = 0 by EXP_2 @@ -670,7 +670,7 @@ QED and n <> 1 by square_1, ~square n. so 1 < n by arithmetic Thus (1,1,0) IN s by IN_CROSS, IN_COUNT, 1 < n - but windmill 1 1 0 + but windmill (1, 1, 0) = 1 <> n by windmill_trivial so (1,1,0) NOTIN t by mills_element ==> t <> s by EXTENSION @@ -696,6 +696,7 @@ Proof `CARD s = n ** 3` by rw[CARD_CROSS, Abbr`s`] >> metis_tac[CARD_PSUBSET] QED +(* This is a very generous upper bound. *) (* Theorem: ~square n ==> FINITE (mills n) *) (* Proof: @@ -716,8 +717,8 @@ QED If part: FINITE (mills n) ==> ~square n By contradiction, suppose square n. Then ?k. n = k * k = k ** 2 by square_def - Then n = k ** 2 + 4 * 0 * t for any t, - = windmill k 0 t by windmill_def + Then n = k ** 2 + 4 * 0 * t for any t + = windmill (k, 0, t) by windmill_def so (k,0,t) IN (mills n) Let f = \t:num. (k,0,t). Then INJ f univ(:num) (mills n) by INJ_DEF @@ -751,7 +752,7 @@ QED (* Proof: If part: (?y z. (0, y, z) IN mills n) ==> n MOD 4 = 0 (0, y, z) IN mills n - ==> n = windmill 0 y z by mills_def + ==> n = windmill (0, y, z) by mills_def ==> n = 0 ** 2 + 4 * y * z by windmill_def ==> n = 4 * y * z by arithmetic ==> n MOD 4 = 0 by MOD_EQ_0 @@ -786,12 +787,12 @@ QED If part: (?x z. (x, 0, z) IN mills n) \/ (?x y. (x, y, 0) IN mills n) ==> square n (x, 0, z) IN mills n - ==> n = windmill x 0 z by mills_def + ==> n = windmill (x, 0, z) by mills_def ==> n = x ** 2 + 4 * 0 * z by windmill_def ==> n = x ** 2 by arithmetic ==> square n by square_def, EXP_2 (x, y, 0) IN mills n - ==> n = windmill x y 0 by mills_def + ==> n = windmill (x, y, 0) by mills_def ==> n = x ** 2 + 4 * y * 0 by windmill_def ==> n = x ** 2 by arithmetic ==> square n by square_def, EXP_2 @@ -817,19 +818,19 @@ QED (* Theorem: n MOD 4 = 1 ==> mills n <> {} *) (* Proof: - By contradiction, suppose (mills n = EMPTY). + By contradiction, suppose (mills n = {}). Now ?k. n = k * 4 + 1 by DIVISION so n = 1 ** 2 + 4 * 1 * k by arithmetic - = windmill 1 1 k by windmill_def + = windmill (1, 1, k) by windmill_def Thus (1, 1, k) IN mills n by mills_def - This contradicts mills n = EMPTY by MEMBER_NOT_EMPTY + This contradicts mills n = {} by MEMBER_NOT_EMPTY *) Theorem mills_quad_suc_non_empty: !n. n MOD 4 = 1 ==> mills n <> {} Proof rpt strip_tac >> `?k. n = k * 4 + 1` by metis_tac[DIVISION, DECIDE``0 < 4``] >> - `_ = windmill 1 1 k` by rw[windmill_def] >> + `_ = windmill (1, 1, k)` by rw[windmill_def] >> `(1, 1, k) IN (mills n)` by metis_tac[mills_element] >> metis_tac[MEMBER_NOT_EMPTY] QED @@ -837,7 +838,7 @@ QED (* Theorem: ~square n /\ n MOD 4 <> 0 ==> !x y z. (x,y,z) IN (mills n) ==> x <> 0 /\ y <> 0 /\ z <> 0 *) (* Proof: - Note n = windmill x y z by mills_def + Note n = windmill (x, y, z) by mills_def = x ** 2 + 4 * y * z by windmill_def By contradiction, suppose x = 0, or y = 0, or z = 0. If x = 0, then n MOD 4 = 0 by MOD_EQ_0 @@ -965,8 +966,8 @@ Definition zagier_def: End (* At the two boundaries: -x = y - z, windmill x y z = (y - z) ** 2 + 4 * y * z = (y + z) ** 2, not a windmill. -x = 2 * y, windmill x y z = (2 * y) ** 2 + 4 * y * z = 4 * y * (y + z), not for a prime. +x = y - z, windmill (x, y, z) = (y - z) ** 2 + 4 * y * z = (y + z) ** 2, not a windmill. +x = 2 * y, windmill (x, y, z) = (2 * y) ** 2 + 4 * y * z = 4 * y * (y + z), not for a prime. *) @@ -1083,18 +1084,6 @@ Proof rw[zagier_def] QED -(* -g `!n x y z. (x, y, z) IN mills n ==> my_zagier (x, y, z) IN mills n`; -e (rw[mills_def, windmill_def, my_zagier_def]); (* >> 4 *) - -g `!n x y z. (x, y, z) IN mills n ==> me_zagier (x, y, z) IN mills n`; -e (rw[mills_def, windmill_def, me_zagier_def]); (* >> 3 *) -but me_zagier is wrong! - -g `!n x y z. (x, y, z) IN mills n ==> mi_zagier (x, y, z) IN mills n`; -e (rw[mills_def, windmill_def, mi_zagier_def]); (* >> 4 *) -*) - (* Theorem: zagier (x,0,0) = (x,x,0) *) (* Proof: If y = 0 and z = 0, x < y - z becomes x < 0, which is false. @@ -1133,6 +1122,23 @@ Proof simp[zagier_def] QED +(* +> zagier_0_y_z |> SPEC ``1`` |> SIMP_RULE std_ss[DECIDE``n < 1 <=> n = 0``]; +val it = |- !z. zagier (0,1,z) = if z = 0 then (0,0,1) else (2,1,z - 1): thm +*) + +(* Theorem: zagier (0,1,z) = (0,z,0) *) +(* Proof: + If x = 0 and y = 1, x < y - z becomes 0 < 1 - z, true when z = 0, giving (0,0,1). + Next x < 2 * y becomes 0 < 2 * 1 = 2, which is true. + Thus zagier (0,1,z) = (2 * y - x,y,x + z - y) = (2,1,z - 1). +*) +Theorem zagier_0_1_z: + !z. zagier (0,1,z) = if z = 0 then (0,0,1) else (2,1,z - 1) +Proof + rw[zagier_def] +QED + (* Theorem: zagier (0,0,0) = (0,0,0) *) (* Proof: by zagier_x_0_0, or zagier_0_0_z or zagier_0_y_0 *) Theorem zagier_0_0_0: @@ -1192,14 +1198,14 @@ QED By mills_def, windmill_def, zagier_def, this is to show: (1) x < y - z ==> 4 * (y * z) + x ** 2 = 4 * (z * (y - (x + z))) + (x + 2 * z) ** 2 - or windmill x y z = windmill (x + 2 * z) z (y - (x + z)) + or windmill (x, y, z) = windmill (x + 2 * z) z (y - (x + z)) From x < y - z so x + z < y by LESS_SUB_ADD_LESS, or in detail: Note x < 0 is impossible, so ~(y <= z), or z < y, implies z <= y. so x + z < y - z + z = y by SUB_ADD, z <= y Thus x + z <= y by x + z < y - windmill (x + 2 * z) z (y - (x + z)) + windmill (x + 2 * z, z ,y - (x + z)) = (x + 2 * z) ** 2 + 4 * z * (y - (x + z)) = x ** 2 + (2 * z) ** 2 + 4 * x * z + 4 * z * (y - (x + z)) by binomial_add = x ** 2 + 4 * z * z + 4 * z * x + 4 * z (y - (x + z)) by EXP_2 @@ -1209,15 +1215,15 @@ QED = x ** 2 + 4 * z * (y + (x + z) - (x + z)) = x ** 2 + 4 * z * y by ADD_SUB = x ** 2 + 4 * y * z - = windmill x y z + = windmill (x, y, z) (2) ~(x < y - z) /\ x < 2 * y ==> 4 * (y * z) + x ** 2 = 4 * (y * (x + z - y)) + (2 * y - x) ** 2 - or windmill x y z = windmill (2 * y - x) y (x + z - y) + or windmill (x, y, z) = windmill (2 * y - x) y (x + z - y) Note y - z <= x by ~(x < y - z) so y <= x + z by SUB_RIGHT_LESS_EQ - windmill (2 * y - x) y (x + z - y) + windmill (2 * y - x, y, x + z - y) = (2 * y - x) ** 2 + 4 * y * (x + z - y) = (2 * y - x) ** 2 + 8 * y * x - 8 * y * x + 4 * y * (x + z - y) by ADD_SUB = (2 * y - x) ** 2 + 8 * y * x + 4 * y * (x + z - y) - 8 * y * x by SUB_RIGHT_ADD, @@ -1234,16 +1240,16 @@ QED = x ** 2 + 4 * y * (2 * x + z) - 4 * y * (2 * x) by arithmetic = x ** 2 + 4 * y * (2 * x + z - 2 * x) by LEFT_SUB_DISTRIB = x ** 2 + 4 * y * z by ADD_SUB - = windmill x y z + = windmill (x, y, z) (3) ~(x < y - z) /\ ~(x < 2 * y) ==> 4 * (y * z) + x ** 2 = 4 * (y * (x + z - y)) + (x - 2 * y) ** 2 - or windmill x y z = windmill (x - 2 * y) y (x + z - y) + or windmill (x, y, z) = windmill (x - 2 * y) y (x + z - y) Note y - z <= x by ~(x < y - z) so y <= x + z by SUB_RIGHT_LESS_EQ Also 2 * y <= x by ~(x < 2 * y) - windmill (x - 2 * y) y (x + z - y) + windmill (x - 2 * y, y, x + z - y) = (x - 2 * y) ** 2 + 4 * y * (x + z - y) = (x - 2 * y) ** 2 + 8 * y * x - 8 * y * x + 4 * y * (x + z - y) by ADD_SUB = (x - 2 * y) ** 2 + 8 * y * x + 4 * y * (x + z - y) - 8 * y * x by SUB_RIGHT_ADD, @@ -1260,7 +1266,7 @@ QED = x ** 2 + 4 * y * (2 * x + z) - 4 * y * (2 * x) by arithmetic = x ** 2 + 4 * y * (2 * x + z - 2 * x) by LEFT_SUB_DISTRIB = x ** 2 + 4 * y * z by ADD_SUB - = windmill x y z + = windmill (x, y, z) *) Theorem zagier_closure: !n x y z. (x, y, z) IN mills n ==> zagier (x, y, z) IN mills n @@ -1727,6 +1733,52 @@ QED (* Zagier and Flip. *) (* ------------------------------------------------------------------------- *) +(* Theorem: (zagier o flip) (x, y, z) = + if x < z - y then (x + 2 * y, y, z - y - x) + else if x < 2 * z then (2 * z - x, z, x + y - z) + else (x - 2 * z, x + y - z, z) *) +(* Proof: + Let t = (x,y,z). + (zagier o flip) t + = zagier (x,z,y) by flip_def + = if x < z - y then (x + 2 * y, y, z - y - x) + else if x < 2 * z then (2 * z - x, z, x + y - z) + else (x - 2 * z, x + y - z, z) by zagier_def +*) +Theorem zagier_flip_eqn: + !x y z. (zagier o flip) (x, y, z) = + if x < z - y then (x + 2 * y, y, z - y - x) + else if x < 2 * z then (2 * z - x, z, x + y - z) + else (x - 2 * z, x + y - z, z) +Proof + rw[zagier_def, flip_def] +QED + +(* +zagier_flip_eqn |> SPEC ``x:num`` |> SPEC ``0`` |> SIMP_RULE std_ss []; +|- !z. zagier (flip (x,0,z)) = if x < z then (x,0,z - x) + else if x < 2 * z then (2 * z - x,z,x - z) + else (x - 2 * z,x - z,z) +> zagier_flip_eqn |> SPEC ``x:num`` |> SPEC ``y:num`` |> SPEC ``0`` |> SIMP_RULE std_ss []; +|- zagier (flip (x,y,0)) = (x,x + y,0) +> zagier_flip_eqn |> SPEC ``x:num`` |> SPEC ``y:num`` |> SPEC ``0`` |> SIMP_RULE std_ss [] |> GEN ``y:num`` |> GEN ``x:num``; +val it = |- !x y. zagier (flip (x,y,0)) = (x,x + y,0): thm +> zagier_flip_eqn |> SPEC ``0`` |> SIMP_RULE std_ss []; +val it = |- !y z. zagier (flip (0,y,z)) = + if 0 < z - y then (2 * y,y,z - y) else if 0 < z then (2 * z,z,y - z) else (0,y,0): thm +> zagier_flip_eqn |> SPEC ``0`` |> SPEC ``1`` |> SIMP_RULE std_ss[]; +val it = |- !z. zagier (flip (0,1,z)) = + if 0 < z - 1 then (2,1,z - 1) + else if 0 < z then (2 * z,z,1 - z) + else (0,1,0): thm +> zagier_def |> ISPEC ``1`` |> ISPEC ``z:num`` |> ISPEC ``1`` |> SIMP_RULE arith_ss []; +|- zagier (1,z,1) = + if 1 < z - 1 then (3,1,z - 2) + else if 1 < 2 * z then (2 * z - 1,z,2 - z) + else (1 - 2 * z,2 - z,z): thm +zagier_def |> ISPEC ``x:num`` |> ISPEC ``z:num`` |> ISPEC ``x:num`` |> SIMP_RULE arith_ss []; +*) + (* Theorem: (zagier o flip) (1,1,z) = if z = 0 then (1,2,0) else if z = 1 then (1,1,1) @@ -1740,13 +1792,6 @@ QED else if z = 1 then (1,1,1) else if z = 2 then (3,2,0) else (3,1,z - 2) by zagier_def - -> zagier_def |> ISPEC ``1`` |> ISPEC ``z:num`` |> ISPEC ``1`` |> SIMP_RULE arith_ss []; -|- zagier (1,z,1) = - if 1 < z - 1 then (3,1,z - 2) - else if 1 < 2 * z then (2 * z - 1,z,2 - z) - else (1 - 2 * z,2 - z,z): thm -zagier_def |> ISPEC ``x:num`` |> ISPEC ``z:num`` |> ISPEC ``x:num`` |> SIMP_RULE arith_ss []; *) Theorem zagier_flip_1_1_z: !z. (zagier o flip) (1,1,z) = @@ -1758,83 +1803,61 @@ Proof rw[zagier_def, flip_def] QED -(* ------------------------------------------------------------------------- *) -(* Computation of (mills n) *) -(* ------------------------------------------------------------------------- *) - -(* Generate the tuples *) -Definition tuples_helper_def: - tuples_helper k 0 = [] /\ - tuples_helper k (SUC n) = - ZIP ((GENLIST (K (SUC n)) k), (GENLIST SUC k)) ++ tuples_helper k n -End - -Definition tuples_def: - tuples k = tuples_helper k k -End -(* -EVAL ``tuples_helper 3 3``; -EVAL ``tuples 3``; -[(3,1); (3,2); (3,3); (2,1); (2,2); (2,3); (1,1); (1,2); (1,3)] -*) - -(* Generate the triples *) -Definition triples_helper_def: - triples_helper k 0 = [] /\ - triples_helper k (SUC n) = - ZIP ((GENLIST (K (SUC n)) (k * k)), tuples k) ++ triples_helper k n -End - -Definition triples_def: - triples k = triples_helper k k -End - -(* -EVAL ``triples_helper 3 3``; -EVAL ``triples 3``; -*) - -(* -EVAL ``FILTER (\(x, y, z). 5 = x * x + 4 * y * z) (triples 5)``; -> [(1,1,1)] -EVAL ``FILTER (\(x, y, z). 13 = x * x + 4 * y * z) (triples 13)``; -> [(3,1,1); (1,3,1); (1,1,3)] -*) - -(* Compute (mills n) *) -Definition mills_of_def: - mills_of n = FILTER (\(x, y, z). n = windmill x y z) (triples n) -End +(* Theorem: (zagier o flip) (0,1,z) = + if z = 0 then (0,1,0) + else (2,1,z - 1) *) +(* Proof: + (zagier o flip) (0,1,z) + = zagier (flip (0,1,z)) by o_THM + = zagier (0,z,1) by flip_def + = if z = 0 then (0,1,0) + else if z = 1 then (2,1,0) + else (2,1,z - 1) by zagier_def + which also holds for z = 1. -(* -EVAL ``mills_of 5``; [(1,1,1)] -EVAL ``MAP zagier (mills_of 5)``; [(1,1,1)] -EVAL ``mills_of 13``; [(3,1,1); (1,3,1); (1,1,3)] -EVAL ``MAP zagier (mills_of 13)``; [(1,3,1); (3,1,1); (1,1,3)] *) +Theorem zagier_flip_0_1_z: + !z. (zagier o flip) (0,1,z) = + if z = 0 then (0,1,0) + else (2,1,z - 1) +Proof + rw[zagier_def, flip_def] +QED -(* - -EVAL ``MAP2 (\x y. (x,y)) (GENLIST (K 1) 5) (GENLIST SUC 5)``; -EVAL ``ZIP ((GENLIST (K 1) 3), (GENLIST SUC 3))``; - -EVAL ``(count 13) CROSS (count 13) CROSS (count 13)``; -EVAL ``13 * 13 * 13``; -> 2197 - -EVAL ``count 5 CROSS (count 5 CROSS count 5)``; -EVAL ``ZIP (GENLIST SUC 5, GENLIST SUC 5)``; -EVAL ``ZIP (GENLIST SUC 5, ZIP (GENLIST SUC 5, GENLIST SUC 5))``; - -EVAL ``FILTER (\(x, y, z). 5 = x * x + 4 * y * z) (ZIP (GENLIST SUC 5, ZIP (GENLIST SUC 5, GENLIST SUC 5)))``; +(* Theorem: (zagier o flip) (0, y, z) = if 0 < z - y then (2 * y,y,z - y) + else if 0 < z then (2 * z,z,y - z) + else (0,y,0) *) +(* Proof: by zagier_flip_eqn. *) +Theorem zagier_flip_0_y_z: + !y z. (zagier o flip) (0, y, z) = + if 0 < z - y then (2 * y, y, z - y) + else if 0 < z then (2 * z, z, y - z) + else (0,y,0) +Proof + rw[zagier_flip_eqn] +QED -(* Generate the triples *) -val triples_def = Define` - triples n = FILTER (\(x, y, z). n = x * x + 4 * y * z) - (ZIP (GENLIST SUC n, ZIP (GENLIST SUC n, GENLIST SUC n))) -`; +(* Theorem: (zagier o flip) (x, 0, z) = if x < z then (x, 0, z - x) + else if x < 2 * z then (2 * z - x, z, x - z) + else (x - 2 * z, x - z, z) *) +(* Proof: by zagier_flip_eqn. *) +Theorem zagier_flip_x_0_z: + !x z. (zagier o flip) (x, 0, z) = + if x < z then (x, 0, z - x) + else if x < 2 * z then (2 * z - x, z, x - z) + else (x - 2 * z, x - z, z) +Proof + rw[zagier_flip_eqn] +QED -EVAL ``triples 5``; -> [(1,1,1)] -EVAL ``triples 13``; the list is wrong! +(* Theorem: (zagier o flip) (x, y, 0) = (x, x + y, 0) *) +(* Proof: by zagier_flip_eqn. *) +Theorem zagier_flip_x_y_0: + !x y. (zagier o flip) (x, y, 0) = (x, x + y, 0) +Proof + rw[zagier_flip_eqn] +QED -*) (* ------------------------------------------------------------------------- *) diff --git a/examples/simple_complexity/lib/bitsizeScript.sml b/examples/simple_complexity/lib/bitsizeScript.sml index 78a6e3a453..572987d0d1 100644 --- a/examples/simple_complexity/lib/bitsizeScript.sml +++ b/examples/simple_complexity/lib/bitsizeScript.sml @@ -228,7 +228,7 @@ val encode_2 = |- encode 2 = [0; 1]: thm Step: !m. m < n ==> (decode (encode m) = m) ==> n <> 0 ==> decode (encode n) = n Note ?m. n = SUC m by num_CASES - and HALF n < n by HALF_LESS, 0 < n + and HALF n < n by HALF_LT, 0 < n decode (encode n) = decode (n MOD 2::encode (HALF n)) by encode_def = n MOD 2 + 2 * decode (encode (HALF n)) by decode_def @@ -243,7 +243,7 @@ val decode_encode_eq_id = store_thm( Cases_on `n = 0` >- rw_tac std_ss[encode_def, decode_def] >> `?m. n = SUC m` by metis_tac[num_CASES] >> - `HALF n < n` by rw[HALF_LESS] >> + `HALF n < n` by rw[HALF_LT] >> `decode (encode n) = decode (n MOD 2::encode (HALF n))` by rw[encode_def] >> `_ = n MOD 2 + 2 * decode (encode (HALF n))` by rw[decode_def] >> `_ = n MOD 2 + 2 * (HALF n)` by rw[] >> @@ -367,7 +367,7 @@ val binary_1 = save_thm("binary_1", EVAL ``binary 1``); If n <> 0, By complete induction on n. Note 0 < n by n <> 0 - Thus HALF n < n by HALF_LESS + Thus HALF n < n by HALF_LT Let m = HALF n. If m = 0, @@ -392,7 +392,7 @@ val binary_length = store_thm( rw[binary_def] >> completeInduct_on `n` >> rpt strip_tac >> - `HALF n < n` by rw[HALF_LESS] >> + `HALF n < n` by rw[HALF_LT] >> qabbrev_tac `m = HALF n` >> Cases_on `m = 0` >| [ `n = 1` by metis_tac[HALF_EQ_0] >> @@ -469,7 +469,7 @@ logPowerTheory.halves_def RHS = halves 1 = 1 by halves_1 If n <> 1, HALF n <> 0 by HALF_EQ_0, 1 < n - and HALF n < n by HALF_LESS + and HALF n < n by HALF_LT size n = SUC (size (HALF n)) by size_def, 1 < n = SUC (halves (HALF n)) by induction hypothesis @@ -484,7 +484,7 @@ val size_by_halves = store_thm( Cases_on `HALF n = 0` >| [ `n = 1` by fs[HALF_EQ_0] >> simp[halves_1], - `HALF n < n` by rw[HALF_LESS] >> + `HALF n < n` by rw[HALF_LT] >> `size n = SUC (size (HALF n))` by rw[Once size_def] >> `_ = SUC (halves (HALF n))` by rw[] >> `_ = halves n` by metis_tac[halves_def] >> @@ -1627,7 +1627,7 @@ val to_bits_element = store_thm( Otherwise, m <> 0, Note ?k. m = SUC k by num_CASES Let h = 2 ** k. - Note HALF n < n by HALF_LESS, 0 < n + Note HALF n < n by HALF_LT, 0 < n and 0 < h by EXP_POS, 0 < 2 decode (to_bits n m) = decode (to_bits n (SUC k)) by m = SUC k @@ -1653,7 +1653,7 @@ val decode_to_bits_eq_mod = store_thm( rw[decode_def, to_bits_def] >> qabbrev_tac `m = SUC n'` >> qabbrev_tac `h = 2 ** n'` >> - `HALF n < n` by rw[HALF_LESS] >> + `HALF n < n` by rw[HALF_LT] >> `0 < h` by rw[EXP_POS, Abbr`h`] >> `decode (to_bits n m) = decode (n MOD 2 :: to_bits (HALF n) n')` by rw[to_bits_def, Abbr`m`] >> `_ = n MOD 2 + TWICE (decode (to_bits (HALF n) n'))` by rw[decode_def] >>