From b6d5e5827dbcb99c72a7f197abc1dc4de54b1c14 Mon Sep 17 00:00:00 2001 From: Joseph Chan Date: Thu, 21 Sep 2023 14:27:52 +1000 Subject: [PATCH] Eliminate duplicate theorems in scripts, otherwise allow rebind. --- examples/AKS/compute/computeBasicScript.sml | 73 ----- examples/AKS/compute/computePolyScript.sml | 6 +- examples/AKS/machine/countAKSScript.sml | 4 +- examples/AKS/machine/countBasicScript.sml | 4 - examples/AKS/machine/countModuloScript.sml | 7 - examples/AKS/machine/countPolyScript.sml | 30 -- examples/AKS/theories/AKSimprovedScript.sml | 118 -------- .../algebra/field/fieldInstancesScript.sml | 9 +- examples/algebra/field/fieldMapScript.sml | 19 -- examples/algebra/field/fieldScript.sml | 20 -- .../algebra/finitefield/ffConjugateScript.sml | 100 ------- .../algebra/finitefield/ffExistScript.sml | 23 +- .../algebra/finitefield/ffExtendScript.sml | 82 ------ .../algebra/finitefield/ffInstancesScript.sml | 68 ----- .../algebra/finitefield/ffMasterScript.sml | 275 ------------------ .../algebra/finitefield/ffMinimalScript.sml | 4 +- examples/algebra/finitefield/ffPolyScript.sml | 68 +---- .../algebra/finitefield/ffUnityScript.sml | 11 - examples/algebra/group/groupScript.sml | 2 - examples/algebra/lib/helperListScript.sml | 95 +++--- examples/algebra/lib/helperNumScript.sml | 43 +-- examples/algebra/lib/helperSetScript.sml | 60 +--- examples/algebra/lib/logPowerScript.sml | 47 ++- examples/algebra/lib/primePowerScript.sml | 7 +- examples/algebra/lib/sublistScript.sml | 12 + examples/algebra/lib/triangleScript.sml | 21 -- .../algebra/polynomial/polyBinomialScript.sml | 98 +------ .../algebra/polynomial/polyCyclicScript.sml | 4 +- .../algebra/polynomial/polyDividesScript.sml | 208 +------------ .../algebra/polynomial/polyDivisionScript.sml | 19 +- .../polynomial/polyFieldModuloScript.sml | 142 +-------- examples/algebra/polynomial/polyGCDScript.sml | 65 ----- examples/algebra/polynomial/polyMapScript.sml | 148 ---------- .../polynomial/polyModuloRingScript.sml | 7 - .../algebra/polynomial/polyMonicScript.sml | 11 - .../algebra/polynomial/polyProductScript.sml | 15 - .../algebra/polynomial/polyRingScript.sml | 103 ++----- .../algebra/polynomial/polyRootScript.sml | 40 +-- .../algebra/polynomial/polyWeakScript.sml | 36 +-- examples/algebra/ring/ringMapScript.sml | 19 +- examples/algebra/ring/ringScript.sml | 7 +- examples/fermat/count/combinatoricsScript.sml | 54 +--- examples/fermat/count/permutationScript.sml | 48 +-- .../fermat/little/FLTfixedpointScript.sml | 2 +- examples/fermat/little/FLTnecklaceScript.sml | 6 +- .../fermat/twosq/involuteActionScript.sml | 18 -- .../fermat/twosq/iterateComposeScript.sml | 194 +----------- examples/fermat/twosq/twoSquaresScript.sml | 76 ----- examples/fermat/twosq/windmillScript.sml | 4 +- .../lib/complexityScript.sml | 5 - .../loop/loopDecreaseScript.sml | 40 +-- .../loop/loopDivideScript.sml | 43 --- .../loop/loopIncreaseScript.sml | 75 ----- .../loop/loopMultiplyScript.sml | 76 ----- .../simple_complexity/loop/loopScript.sml | 95 ------ 55 files changed, 218 insertions(+), 2648 deletions(-) diff --git a/examples/AKS/compute/computeBasicScript.sml b/examples/AKS/compute/computeBasicScript.sml index bbae8972ca..fbc1e860b3 100644 --- a/examples/AKS/compute/computeBasicScript.sml +++ b/examples/AKS/compute/computeBasicScript.sml @@ -929,79 +929,6 @@ val exp_mod_binary_eqn = store_thm( simp[exp_mod_binary_0, ONE_MOD, EXP] >> metis_tac[exp_mod_binary_suc, MOD_MOD, MOD_TIMES2, EXP]); -(* Another proof of the same result *) - -(* Theorem: exp_mod_binary a n m = (a ** n) MOD m *) -(* Proof: - If m = 0, true trivially by exp_mod_binary_def - If m = 1, - exp_mod_binary a n m - = 1 by exp_mod_binary_def - = (a ** n) MOD 1 by MOD_1 - If m <> 0 and m <> 1, - Then 1 < m. - By complete induction on n. - Assume: !j. j < n ==> !a. exp_mod_binary a j m = a ** j MOD m - To show: exp_mod_binary a n m = a ** n MOD m - If n = 0, - exp_mod_binary a 0 m - = 1 by exp_mod_binary_0 - = 1 MOD m by ONE_MOD, 1 < m - = (a ** 0) MOD m by EXP - If n <> 0, - Then HALF n < n by HALF_LT - If EVEN n, - Then n MOD 2 = 0 by EVEN_MOD2 - exp_mod_binary a n m - = exp_mod_binary ((a * a) MOD m) (HALF n) m by exp_mod_binary_def, n MOD 2 = 0 - = exp_mod_binary ((a ** 2) MOD m) (HALF n) m by EXP_2 - = (((a ** 2) MOD m) ** (HALF n)) MOD m by induction hypothesis, HALF n < n - = ((a ** 2) ** (HALF n)) MOD m by EXP_MOD, 0 < m - = (a ** (2 * HALF n)) MOD m by EXP_EXP_MULT - = (a ** n) MOD m by EVEN_HALF - If ~EVEN n, - Then ODD n by ODD_EVEN - exp_mod_binary a n m - = (a * exp_mod_binary ((a * a) MOD m) (HALF n) m) MOD m by exp_mod_binary_def, n MOD 2 <> 0 - = (a * exp_mod_binary ((a ** 2) MOD m) (HALF n) m) MOD m by EXP_2 - = (a * (((a ** 2) MOD m) ** (HALF n)) MOD m) MOD m by induction hypothesis, HALF n < n - = (a * ((a ** 2) ** (HALF n)) MOD m) MOD m by EXP_MOD, 0 < m - = (a * (a ** (2 * HALF n)) MOD m) MOD m by EXP_EXP_MULT - = (a * a ** (2 * HALF n)) MOD m by MOD_TIMES2, 0 < m - = (a ** (1 + 2 * HALF n)) MOD m by EXP_ADD - = (a ** (2 * HALF n + 1)) MOD m by arithmetic - = (a ** n) MOD m by ODD_HALF -*) -Theorem exp_mod_binary_eqn[allow_rebind]: - !m n a. exp_mod_binary a n m = (a ** n) MOD m -Proof - ntac 2 strip_tac >> - Cases_on ‘m = 0’ >- - rw[Once exp_mod_binary_def] >> - Cases_on ‘m = 1’ >- - rw[Once exp_mod_binary_def] >> - ‘1 < m /\ 0 < m’ by decide_tac >> - completeInduct_on ‘n’ >> - rpt strip_tac >> - Cases_on ‘n = 0’ >- - rw[exp_mod_binary_0, EXP] >> - ‘0 < m’ by decide_tac >> - ‘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] >> - rw[], - ‘ODD n’ by rw[ODD_EVEN] >> - ‘(a * (a ** 2) ** HALF n) MOD m = (a * (a ** (2 * HALF n) MOD m)) MOD m’ - by rw[EXP_EXP_MULT] >> - ‘_ = (a * a ** (2 * HALF n)) MOD m’ by metis_tac[MOD_TIMES2, MOD_MOD] >> - ‘_ = (a ** (2 * HALF n + 1)) MOD m’ by rw[EXP_ADD] >> - ‘_ = a ** n MOD m’ by metis_tac[ODD_HALF] >> - rw[] - ] -QED - (* Theorem: exp_mod_binary 0 n m = (if n = 0 then 1 else 0) MOD m *) (* Proof: exp_mod_binary 0 n m diff --git a/examples/AKS/compute/computePolyScript.sml b/examples/AKS/compute/computePolyScript.sml index eedfd94bdb..85e912fb15 100644 --- a/examples/AKS/compute/computePolyScript.sml +++ b/examples/AKS/compute/computePolyScript.sml @@ -116,7 +116,7 @@ open rich_listTheory; (* for FRONT and LAST *) (turn_exp p n) (DROP n q)) unity_mod_mult_alt |- !r. Ring r /\ #1 <> #0 ==> !p q. weak p /\ weak q /\ q <> |0| ==> (unity_mod_mult r p q = psum (GENLIST (\k. q ' k o turn_exp p k) (SUC (deg q)))) - unity_mod_mult_zero |- !r p. (unity_mod_mult r p |0| = |0|) /\ (unity_mod_mult r |0| p = |0|) + unity_mod_mult_zero_alt |- !r p. (unity_mod_mult r p |0| = |0|) /\ (unity_mod_mult r |0| p = |0|) unity_mod_mult_cons |- !r. Ring r ==> !p h t. weak p /\ weak (h::t) ==> (unity_mod_mult r p (h::t) = h o p || unity_mod_mult r (turn p) t) unity_mod_mult_weak |- !r. Ring r ==> !p q. weak p /\ weak q ==> weak (unity_mod_mult r p q) @@ -1232,8 +1232,8 @@ val unity_mod_mult_alt = store_thm( (* Theorem: (unity_mod_mult r p |0| = |0|) /\ (unity_mod_mult r |0| p = |0|) *) (* Proof: by unity_mod_mult_def, poly_slide_zero. *) -val unity_mod_mult_zero = store_thm( - "unity_mod_mult_zero", +val unity_mod_mult_zero_alt = store_thm( + "unity_mod_mult_zero_alt", ``!r:'a ring p. (unity_mod_mult r p |0| = |0|) /\ (unity_mod_mult r |0| p = |0|)``, rw[unity_mod_mult_def, poly_slide_zero]); diff --git a/examples/AKS/machine/countAKSScript.sml b/examples/AKS/machine/countAKSScript.sml index 1988d968af..cca6b11a1e 100644 --- a/examples/AKS/machine/countAKSScript.sml +++ b/examples/AKS/machine/countAKSScript.sml @@ -1223,7 +1223,7 @@ val aksM_steps_base = store_thm( so 1 < size n by size n <> 0, size n <> 1 ==> 1 < size n ** 5 by ONE_LT_EXP Thus 1 + HALF (size n ** 5) - <= size n ** 5 by SUC_HALF_LE + <= size n ** 5 by HALF_ADD1_LE or c <= size n ** 5 by above and size c <= size (size n ** 5) by size_monotone_le <= 5 * size (size n) by size_exp_upper_alt @@ -1282,7 +1282,7 @@ val aksM_steps_upper = store_thm( `size n <> 1` by fs[size_eq_1] >> `1 < size n` by decide_tac >> `1 < size n ** 5` by rw[ONE_LT_EXP] >> - `1 + HALF (size n ** 5) <= size n ** 5` by rw[SUC_HALF_LE] >> + `1 + HALF (size n ** 5) <= size n ** 5` by rw[HALF_ADD1_LE] >> decide_tac) >> `size c <= 5 * size n` by (`size c <= size (size n ** 5)` by rw[size_monotone_le] >> diff --git a/examples/AKS/machine/countBasicScript.sml b/examples/AKS/machine/countBasicScript.sml index a90cd11100..e508654b7b 100644 --- a/examples/AKS/machine/countBasicScript.sml +++ b/examples/AKS/machine/countBasicScript.sml @@ -784,10 +784,6 @@ val power_twoM_steps_1 = store_thm( rw[Once power_twoM_steps_thm]); (* Derive theorems *) -val power_twoM_steps_upper = save_thm("power_twoM_steps_upper", - power_ofM_steps_upper |> SPEC ``2`` |> SIMP_RULE (srw_ss()) [GSYM power_twoM_def]); -val power_twoM_steps_bound = save_thm("power_twoM_steps_bound", - power_ofM_steps_bound |> SPEC ``2`` |> SIMP_RULE (srw_ss()) [GSYM power_twoM_def]); val power_twoM_steps_O_poly = save_thm("power_twoM_steps_O_poly", power_ofM_steps_O_poly |> SPEC ``2`` |> SIMP_RULE (srw_ss()) [GSYM power_twoM_def]); val power_twoM_steps_big_O = save_thm("power_twoM_steps_big_O", diff --git a/examples/AKS/machine/countModuloScript.sml b/examples/AKS/machine/countModuloScript.sml index 94923f303c..6703b7ddb0 100644 --- a/examples/AKS/machine/countModuloScript.sml +++ b/examples/AKS/machine/countModuloScript.sml @@ -388,13 +388,6 @@ val msqM_def = Define` msqM m x = mmulM m x x `; -(* Theorem: valueOf(msqM m x) = (x * x) MOD m *) -(* Proof: by msqM_def *) -val msqM_value = store_thm( - "msqM_value[simp]", - ``!m x. valueOf(msqM m x) = (x * x) MOD m``, - simp[msqM_def]); - (* Obtain theorems *) val msqM_value = save_thm("msqM_value[simp]", mmulM_value |> SPEC ``m:num`` |> SPEC ``x:num`` |> SPEC ``x:num`` diff --git a/examples/AKS/machine/countPolyScript.sml b/examples/AKS/machine/countPolyScript.sml index b073389b94..6073439434 100644 --- a/examples/AKS/machine/countPolyScript.sml +++ b/examples/AKS/machine/countPolyScript.sml @@ -2794,36 +2794,6 @@ This puts poly_frontM_steps in the category: list loop with body cover and exit. suitable for: loop_list_count_cover_exit_le *) -(* Theorem: stepsOf (poly_frontM p) <= 1 + 5 * LENGTH p *) -(* Proof: - Let body = (\p. 4 + if (TL p = []) then 0 else 1), - cover = (\p. 5), - exit = (\p. TL p = []), - loop = (\p. stepsOf (poly_frontM p)). - Then !p. loop p = if (p = []) then 1 else body p + if exit p then 0 else loop (TL p) - by poly_frontM_steps_thm - Now !x. body x <= cover x by cases on TL p, - and !x y. x <= y ==> cover x <= cover y by cover being a constant - Thus loop p <= 1 + cover p * LENGTH p by loop_list_count_cover_exit_le - = 1 + 5 * LENGTH p -*) -val poly_frontM_steps_upper = store_thm( - "poly_frontM_steps_upper", - ``!p. stepsOf (poly_frontM p) <= 1 + 5 * LENGTH p``, - rpt strip_tac >> - qabbrev_tac `body = \p. 4 + if (TL p = []) then 0 else 1` >> - qabbrev_tac `cover = \p:'a list. 5` >> - qabbrev_tac `exit = \p. TL p = []` >> - qabbrev_tac `loop = \p. stepsOf (poly_frontM p)` >> - `loop p <= 1 + 5 * LENGTH p` suffices_by rw[] >> - `!x. loop x = if x = [] then 1 else body x + if exit x then 0 else loop (TL x)` by metis_tac[poly_frontM_steps_thm] >> - `!x. body x <= cover x` by rw[Abbr`body`, Abbr`cover`] >> - `!x y. x <= y ==> cover x <= cover y` by rw[Abbr`cover`] >> - imp_res_tac loop_list_count_cover_exit_le >> - metis_tac[]); - -(* Michael's proof of the same theorem. *) - (* Theorem: stepsOf (poly_frontM p) <= 1 + 5 * LENGTH p *) (* Proof: Let body = (\p. 4 + if (TL p = []) then 0 else 1), diff --git a/examples/AKS/theories/AKSimprovedScript.sml b/examples/AKS/theories/AKSimprovedScript.sml index 96f6346b57..714b0dca08 100644 --- a/examples/AKS/theories/AKSimprovedScript.sml +++ b/examples/AKS/theories/AKSimprovedScript.sml @@ -1126,42 +1126,6 @@ val AKS_main_ulog_2b = store_thm( This leads to a contradiction, as [1], [2] and [3] are incompatible. *) -val AKS_main_ulog_2b = store_thm( - "AKS_main_ulog_2b", - ``!(r:'a field). FiniteField r /\ (CARD R = char r) ==> (* condition on r *) - !n k. 0 < n /\ 0 < k /\ 1 < ordz k (char r) /\ - char r divides n /\ (* conditions on n *) - k < char r /\ (ulog n) ** 2 <= ordz k n /\ (* conditions on k *) - poly_intro_range r k n (SQRT (phi k) * (ulog n)) (* AKS tests *) - ==> perfect_power n (char r)``, - rpt (stripDup[FiniteField_def]) >> - qabbrev_tac `p = char r` >> - qabbrev_tac `a = (ulog n) ** 2` >> - qabbrev_tac `s = SQRT (phi k) * ulog n` >> - `prime p` by rw[finite_field_char, Abbr`p`] >> - `1 < p` by rw[ONE_LT_PRIME] >> - `n <> 1` by metis_tac[DIVIDES_ONE, LESS_NOT_EQ] >> - `k <> 1` by metis_tac[ZN_order_mod_1, LESS_NOT_EQ] >> - `1 < n /\ 1 < k` by decide_tac >> - Cases_on `perfect_power n 2` >- - metis_tac[prime_divides_prime_power, perfect_power_def, PRIME_2] >> - `coprime n k` by - (`0 < a` by rw[ulog_pos, Abbr`a`] >> - `ordz k n <> 0` by decide_tac >> - metis_tac[ZN_order_eq_0, GCD_SYM]) >> - qabbrev_tac `t = CARD M` >> - `n IN N` by fs[setN_element] >> - `n ** SQRT t < 2 ** MIN s t` by rw[modN_card_in_exp_lt_bound_3, Abbr`t`, Abbr`s`] >> - `?z. (forderz X = k) /\ mifactor z (unity k)` by metis_tac[poly_unity_special_factor_exists] >> - `0 < s` by rw[sqrt_phi_times_ulog, Abbr`s`] >> - `s <= phi k` by metis_tac[ZN_order_condition_property_2, GCD_SYM] >> - `phi k < k` by rw[phi_lt] >> - `s < p` by decide_tac >> - `2 ** MIN s t <= CARD (Q z)` by rw[modP_card_lower_1, Abbr`t`] >> - `coprime k p` by metis_tac[coprime_prime_factor_coprime, GCD_SYM] >> - spose_not_then strip_assume_tac >> - `CARD (Q z) <= n ** SQRT t` by rw[modP_card_upper_better, Abbr`t`] >> - decide_tac); (* This is a much shorter proof of the AKS main theorem! *) @@ -1232,44 +1196,6 @@ val AKS_main_ulog_2b = store_thm( This leads to a contradiction, as [A] and [B] are incompatible. *) -val AKS_main_ulog_2b = store_thm( - "AKS_main_ulog_2b", - ``!(r:'a field). FiniteField r /\ (CARD R = char r) ==> (* condition on r *) - !n k. 0 < n /\ 0 < k /\ 1 < ordz k (char r) /\ - char r divides n /\ (* conditions on n *) - k < char r /\ (ulog n) ** 2 <= ordz k n /\ (* conditions on k *) - poly_intro_range r k n (SQRT (phi k) * (ulog n)) (* AKS tests *) - ==> perfect_power n (char r)``, - rpt (stripDup[FiniteField_def]) >> - qabbrev_tac `p = char r` >> - qabbrev_tac `a = (ulog n) ** 2` >> - qabbrev_tac `s = SQRT (phi k) * ulog n` >> - `prime p` by rw[finite_field_char, Abbr`p`] >> - `1 < p` by rw[ONE_LT_PRIME] >> - `n <> 1` by metis_tac[DIVIDES_ONE, LESS_NOT_EQ] >> - `k <> 1` by metis_tac[ZN_order_mod_1, LESS_NOT_EQ] >> - `1 < n /\ 1 < k` by decide_tac >> - Cases_on `perfect_power n 2` >- - metis_tac[prime_divides_prime_power, perfect_power_def, PRIME_2] >> - spose_not_then strip_assume_tac >> - `coprime n k` by - (`0 < a` by rw[ulog_pos, Abbr`a`] >> - `ordz k n <> 0` by decide_tac >> - metis_tac[ZN_order_eq_0, GCD_SYM]) >> - qabbrev_tac `t = CARD M` >> - `n IN N` by fs[setN_element] >> - `2 ** MIN s t <= n ** SQRT t` by - (`?z. (forderz X = k) /\ mifactor z (unity k)` by metis_tac[poly_unity_special_factor_exists] >> - `0 < s` by rw[sqrt_phi_times_ulog, Abbr`s`] >> - `s <= phi k` by metis_tac[ZN_order_condition_property_2, GCD_SYM] >> - `phi k < k` by rw[phi_lt] >> - `s < p` by decide_tac >> - `2 ** MIN s t <= CARD (Q z)` by rw[modP_card_lower_1, Abbr`t`] >> - `coprime k p` by metis_tac[coprime_prime_factor_coprime, GCD_SYM] >> - `CARD (Q z) <= n ** SQRT t` by rw[modP_card_upper_better, Abbr`t`] >> - decide_tac) >> - `n ** SQRT t < 2 ** MIN s t` by rw[modN_card_in_exp_lt_bound_3, Abbr`t`, Abbr`s`] >> - decide_tac); (* Idea: The third proof derives a contradiction by: @@ -1346,50 +1272,6 @@ val AKS_main_ulog_2b = store_thm( Since [A] and [B] are contradictory, the proof is complete. *) -val AKS_main_ulog_2b = store_thm( - "AKS_main_ulog_2b", - ``!(r:'a field). FiniteField r /\ (CARD R = char r) ==> (* condition on r *) - !n k. 0 < n /\ 0 < k /\ 1 < ordz k (char r) /\ - char r divides n /\ (* conditions on n *) - k < char r /\ (ulog n) ** 2 <= ordz k n /\ (* conditions on k *) - poly_intro_range r k n (SQRT (phi k) * (ulog n)) (* AKS tests *) - ==> perfect_power n (char r)``, - rpt (stripDup[FiniteField_def]) >> - qabbrev_tac `p = char r` >> - qabbrev_tac `a = (ulog n) ** 2` >> - qabbrev_tac `s = SQRT (phi k) * ulog n` >> - `prime p` by rw[finite_field_char, Abbr`p`] >> - `1 < p` by rw[ONE_LT_PRIME] >> - `n <> 1` by metis_tac[DIVIDES_ONE, LESS_NOT_EQ] >> - `k <> 1` by metis_tac[ZN_order_mod_1, LESS_NOT_EQ] >> - `1 < n /\ 1 < k` by decide_tac >> - Cases_on `perfect_power n 2` >- - metis_tac[prime_divides_prime_power, perfect_power_def, PRIME_2] >> - `coprime n k` by - (`0 < a` by rw[ulog_pos, Abbr`a`] >> - `ordz k n <> 0` by decide_tac >> - metis_tac[ZN_order_eq_0, GCD_SYM]) >> - `n IN N` by metis_tac[setN_element] >> - `?z. mifactor z (unity k) /\ (deg z = ordz k p) /\ (forderz X = k)` by metis_tac[poly_unity_special_factor_exists] >> - `2 ** MIN s (CARD M) < CARD (Q z)` by - ((irule modP_card_lower_better >> simp[]) >> - rpt strip_tac >| [ - `s <= phi k` by metis_tac[ZN_order_condition_property_2, GCD_SYM] >> - `phi k < k` by rw[phi_lt] >> - decide_tac, - rw[sqrt_phi_times_ulog, Abbr`s`], - `n <> 2` by metis_tac[perfect_power_self] >> - `1 < a` by rw[ulog_sq_gt_1, Abbr`a`] >> - `1 < ordz k n` by decide_tac >> - `ordz k n <= CARD M` by rw[modN_card_lower] >> - decide_tac - ]) >> - spose_not_then strip_assume_tac >> - `CARD (Q z) <= 2 ** MIN s (CARD M)` by - (`CARD (Q z) <= 2 ** MIN (SQRT (phi k) * ulog n) (CARD M)` suffices_by rw[Abbr`s`] >> - (irule modP_card_upper_better_3 >> simp[]) >> - metis_tac[coprime_prime_factor_coprime, GCD_SYM]) >> - decide_tac); (* Theorem: The AKS Main Theorem (no mention of FiniteField, but mentions (ZN n)) Given a number n > 1, diff --git a/examples/algebra/field/fieldInstancesScript.sml b/examples/algebra/field/fieldInstancesScript.sml index 85f2dc440f..3999c2a550 100644 --- a/examples/algebra/field/fieldInstancesScript.sml +++ b/examples/algebra/field/fieldInstancesScript.sml @@ -633,9 +633,9 @@ val ZN_finite_field = store_thm( Note 0 < p /\ 0 * y = 0 ==> 0 MOD p = 0 by MULT, ZERO_MOD and 0 < p /\ x * 0 = 0 ==> 0 MOD p = 0 by MULT_0, ZERO_MOD *) -val ZN_finite_field = store_thm( - "ZN_finite_field", - ``!p. prime p ==> FiniteField (ZN p)``, +Theorem ZN_finite_field[allow_rebind]: + !p. prime p ==> FiniteField (ZN p) +Proof rpt strip_tac >> (REVERSE (irule finite_field_from_finite_ring >> rpt conj_tac) >> simp[ZN_property]) >- metis_tac[NOT_PRIME_1, ONE_NOT_ZERO] >- @@ -643,7 +643,8 @@ val ZN_finite_field = store_thm( rw[EQ_IMP_THM] >- metis_tac[EUCLID_LEMMA, LESS_MOD] >- rw[] >> - rw[]); + rw[] +QED (* Theorem: prime p <=> FiniteField (ZN p) *) (* Proof: diff --git a/examples/algebra/field/fieldMapScript.sml b/examples/algebra/field/fieldMapScript.sml index 60e7aaa33f..d3b426b990 100644 --- a/examples/algebra/field/fieldMapScript.sml +++ b/examples/algebra/field/fieldMapScript.sml @@ -2265,25 +2265,6 @@ Proof rw[field_nonzero_eq, field_mult_rinv, field_mult_linv] QED -(* Theorem: Field r /\ INJ f R univ(:'b) ==> Field (ring_inj_image r f) *) -(* Proof: - By Field_def, this is to show: - (1) Ring (ring_inj_image r f), true by ring_inj_image_ring - (2) Group ((ring_inj_image r f).prod excluding (ring_inj_image r f).sum.id) - Since (ring_inj_image r f).sum.id = f #0 by ring_inj_image_def - The result follows by field_inj_image_prod_nonzero_group -*) -Theorem field_inj_image_field: - !(r:'a field) f. Field r /\ INJ f R univ(:'b) ==> Field (ring_inj_image r f) -Proof - rpt strip_tac >> - rw[Field_def] >- - rw[ring_inj_image_ring] >> - `(ring_inj_image r f).sum.id = f #0` by rw[ring_inj_image_def] >> - rw[field_inj_image_prod_nonzero_group] -QED -(* Another proof of a previous theorem. *) - (* Theorem: Field r /\ INJ f R univ(:'b) ==> FieldHomo f r (ring_inj_image r f) *) (* Proof: by ring_inj_image_ring_homo, field_is_ring *) Theorem field_inj_image_field_homo: diff --git a/examples/algebra/field/fieldScript.sml b/examples/algebra/field/fieldScript.sml index 12e557f082..fa682f997a 100644 --- a/examples/algebra/field/fieldScript.sml +++ b/examples/algebra/field/fieldScript.sml @@ -1906,18 +1906,6 @@ val field_inv_mult = store_thm( (* export simple theorem *) val _ = export_rewrites ["field_inv_mult"]; -(* Theorem: Field r ==> |/ #1 = #1 *) -(* Proof: by group_inv_id and r.prod group. *) -val field_inv_one = store_thm( - "field_inv_one", - ``!r:'a field. Field r ==> ( |/ #1 = #1)``, - metis_tac[group_inv_id |> SPEC ``f*`` |> UNDISCH_ALL - |> PROVE_HYP (field_mult_group |> SPEC_ALL |> UNDISCH_ALL |> CONJUNCT1) |> DISCH_ALL, - field_mult_group, field_nonzero_mult_property, group_id_element, field_mult_inv]); -(* > val field_inv_one = |- !r:'a field. Field r ==> ( |/ #1 = #1) : thm *) - -(* Same theorem, simple proof. *) - (* Theorem: Field r ==> |/ #1 = #1 *) (* Proof: by ring_inv_one, field_is_ring. *) val field_inv_one = store_thm( @@ -3261,14 +3249,6 @@ val finite_field_fermat_thm = store_thm( = x ** (m ** n) by finite_field_fermat_thm = x by induction hypothesis *) -val finite_field_fermat_all = store_thm( - "finite_field_fermat_all", - ``!r:'a field. FiniteField r ==> !x. x IN R ==> !n. x ** (CARD R ** n) = x``, - rpt (stripDup[FiniteField_def]) >> - qabbrev_tac `m = CARD R` >> - Induct_on `n` >- - rw[EXP] >> - rw[EXP, field_exp_mult, finite_field_fermat_thm, Abbr`m`]); val finite_field_fermat_all = store_thm( "finite_field_fermat_all", ``!r:'a field. FiniteField r ==> !x. x IN R ==> !n. x ** (CARD R ** n) = x``, diff --git a/examples/algebra/finitefield/ffConjugateScript.sml b/examples/algebra/finitefield/ffConjugateScript.sml index b90179e811..b9416c2d6e 100644 --- a/examples/algebra/finitefield/ffConjugateScript.sml +++ b/examples/algebra/finitefield/ffConjugateScript.sml @@ -1771,63 +1771,6 @@ val poly_minimal_deg_eqn = store_thm( `x IN R` by rw[field_nonzero_element] >> rw[poly_minimal_deg, finite_field_conjugates_card]); -(* Theorem: FiniteField r /\ s <<= r ==> !x. x IN R ==> degree x divides (r <:> s) *) -(* Proof: - Let d = (r <:> s), om = order (ZN (forder x)).prod (CARD B). - If x = #0, - deg (minimal #0) - = deg X by poly_minimal_zero - = 1 by poly_deg_X - and 1 divides d by ONE_DIVIDES_ALL - If x <> #0, - Note x IN R+ by field_nonzero_eq - degree x - = deg (minimal x) by notation - = om by poly_minimal_deg_eqn - and om divides d by subfield_card_order_divides_dim -*) -val poly_minimal_deg_divides_dim = store_thm( - "poly_minimal_deg_divides_dim", - ``!(r s):'a field. FiniteField r /\ s <<= r ==> !x. x IN R ==> degree x divides (r <:> s)``, - rpt (stripDup[FiniteField_def]) >> - Cases_on `x = #0` >| [ - `deg (minimal #0) = 1` by rw[poly_minimal_zero] >> - rw[ONE_DIVIDES_ALL], - `x IN R+` by rw[field_nonzero_eq] >> - rw[poly_minimal_deg_eqn, subfield_card_order_divides_dim] - ]); - -(* Another proof of the same theorem. *) - -(* Theorem: FiniteField r /\ s <<= r ==> !x. x IN R ==> degree x divides (r <:> s) *) -(* Proof: - Let d = (r <:> s), om = order (ZN (forder x)).prod (CARD B). - If x = #0, - deg (minimal #0) - = CARD (Conj #0) by poly_minimal_deg - = CARD {#0} by ring_conjugates_zero - = 1 by CARD_SING - and 1 divides d by ONE_DIVIDES_ALL - If x <> #0, - Note x IN R+ by field_nonzero_eq - degree x - = deg (minimal x) by notation - = CARD (Conj x) by poly_minimal_deg - = om by finite_field_conjugates_card, x IN R+ - and om divides d by subfield_card_order_divides_dim -*) -val poly_minimal_deg_divides_dim = store_thm( - "poly_minimal_deg_divides_dim", - ``!(r s):'a field. FiniteField r /\ s <<= r ==> !x. x IN R ==> degree x divides (r <:> s)``, - rpt (stripDup[FiniteField_def]) >> - `degree x = CARD (Conj x)` by rw[poly_minimal_deg] >> - Cases_on `x = #0` >- - rw[finite_field_conjugates_zero] >> - `x IN R+` by rw[field_nonzero_eq] >> - rw[finite_field_conjugates_card, subfield_card_order_divides_dim]); - -(* Third proof of the same theorem, without counting conjugates. *) - (* > poly_minimal_subfield_irreducible val it = |- !r. FiniteField r ==> !s. s <<= r ==> !x. x IN R ==> IPoly s (minimal x) @@ -2795,49 +2738,6 @@ val poly_unity_special_subfield_factor = store_thm( (* Cyclo and Unity polynomials by Irreducible Factors *) (* ------------------------------------------------------------------------- *) -(* Theorem: FiniteField r ==> !n. n divides CARD R+ ==> - ?s. FINITE s /\ miset s /\ s <> {} /\ (cyclo n = PPROD s) *) -(* Proof: - Let s = IMAGE factor (orders f* n). - Then cyclo n = PPROD s by poly_cyclo_def - Note (orders f* n) SUBSET R by field_orders_subset_carrier - and FINITE (orders f* n) by field_orders_finite - and (orders f* n) <> {} by finite_field_orders_nonempty_iff, n divides CARD R+ - Thus FINITE s by IMAGE_FINITE - and miset s by poly_factor_image_monic_irreducibles_set - and s <> {} by IMAGE_EMPTY - Take this s, and the result follows. -*) -val poly_cyclo_by_distinct_irreducibles = store_thm( - "poly_cyclo_by_distinct_irreducibles", - ``!r:'a field. FiniteField r ==> !n. n divides CARD R+ ==> - ?s. FINITE s /\ miset s /\ s <> {} /\ (cyclo n = PPROD s)``, - rpt (stripDup[FiniteField_def]) >> - qabbrev_tac `s = IMAGE factor (orders f* n)` >> - `(orders f* n) SUBSET R` by rw[field_orders_subset_carrier] >> - `FINITE (orders f* n)` by rw[field_orders_finite] >> - `(orders f* n) <> {}` by metis_tac[finite_field_orders_nonempty_iff] >> - `FINITE s` by rw[Abbr`s`] >> - `miset s` by metis_tac[poly_factor_image_monic_irreducibles_set] >> - `s <> {}` by rw[Abbr`s`] >> - metis_tac[poly_cyclo_def]); - -(* Another proof of the same result *) - -(* Check this out: -> poly_cyclo_eq_poly_minimal_product |> ISPEC ``r:'a field`` |> ISPEC ``r:'a field``; -val it = |- FiniteField r /\ r <<= r ==> !n. cyclo n = PPIMAGE (poly_minimal r r) (orders f* n): thm -> poly_minimal_monic |> ISPEC ``r:'a field`` |> ISPEC ``r:'a field``; -val it = |- FiniteField r /\ r <<= r ==> !x. x IN R ==> monic (poly_minimal r r x): thm -> poly_minimal_subfield_irreducible |> ISPEC ``r:'a field`` |> ISPEC ``r:'a field``; -val it = |- FiniteField r /\ r <<= r ==> !x. x IN R ==> ipoly (poly_minimal r r x): thm - -However, what does (poly_minimal r r x) look like? -> poly_minimal_deg_eqn |> ISPEC ``r:'a field`` |> ISPEC ``r:'a field``; -val it = |- FiniteField r /\ r <<= r ==> !x. x IN R+ /\ x <> #1 ==> - (deg (poly_minimal r r x) = ordz (forder x) (CARD R)): thm -*) - (* Theorem: FiniteField r ==> !n. n divides CARD R+ ==> ?s. FINITE s /\ miset s /\ s <> {} /\ (cyclo n = PPROD s) *) (* Proof: diff --git a/examples/algebra/finitefield/ffExistScript.sml b/examples/algebra/finitefield/ffExistScript.sml index 1ac60c96a0..ebb5e63f04 100644 --- a/examples/algebra/finitefield/ffExistScript.sml +++ b/examples/algebra/finitefield/ffExistScript.sml @@ -2881,7 +2881,7 @@ val it = |- !r s. FiniteField r /\ s <<= r /\ 1 < (r <:> s) ==> Note MAP (LINV up R) (Unity t n) = unity n by subring_poly_unity, field_iso_poly_unity so (MAP (LINV up R) k) pdivides (MAP (LINV up R) (Unity t n)) by field_iso_poly_divides_iff or h pdivides (unity n) by above - ==> (unity n) % h = |0| by poly_divides_mod_zero, ulead h + ==> (unity n) % h = |0| by poly_divides_alt, ulead h Step 7: setup another field/subfield pair based on h. Let u = PolyModRing r h, su = PolyModConst r h. @@ -2976,7 +2976,7 @@ val poly_unity_special_factor_exists_0 = store_thm( `poly_divides st k (Unity t n)` by metis_tac[subring_poly_divides_iff, poly_monic_ulead] >> `MAP (LINV up R) (Unity t n) = unity n` by metis_tac[subring_poly_unity, field_iso_poly_unity] >> `h pdivides (unity n)` by prove_tac[field_iso_poly_divides_iff] >> - rw[GSYM poly_divides_mod_zero]) >- + rw[GSYM poly_divides_alt]) >- rw_tac std_ss[] >> qabbrev_tac `u = PolyModRing r h` >> qabbrev_tac `su = PolyModConst r h` >> @@ -3122,7 +3122,7 @@ val poly_unity_special_factor_exists = store_thm( Note MAP (LINV up R) (Unity t n) = unity n by subring_poly_unity, field_iso_poly_unity so (MAP (LINV up R) k) pdivides (MAP (LINV up R) (Unity t n)) by field_iso_poly_divides_iff or h pdivides (unity n) by above - ==> (unity n) % h = |0| by poly_divides_mod_zero, ulead h + ==> (unity n) % h = |0| by poly_divides_alt, ulead h Step 7: setup another field/subfield pair based on h. Let u = PolyModRing r h, su = PolyModConst r h. @@ -3162,10 +3162,10 @@ val poly_unity_special_factor_exists = store_thm( so order (u.prod excluding |0|) (f x) = n by finite_field_element_mirror_order ==> order (u.prod excluding |0|) X = n by finite_field_conjugates_order *) -val poly_unity_special_factor_exists = store_thm( - "poly_unity_special_factor_exists", - ``!r:'a field. FiniteField r ==> !n. 0 < n /\ 1 < ordz n (CARD R) ==> - ?h. mifactor h (unity n) /\ (deg h = ordz n (CARD R)) /\ (order ((PolyModRing r h).prod excluding |0|) X = n)``, +Theorem poly_unity_special_factor_exists[allow_rebind]: + !r:'a field. FiniteField r ==> !n. 0 < n /\ 1 < ordz n (CARD R) ==> + ?h. mifactor h (unity n) /\ (deg h = ordz n (CARD R)) /\ (order ((PolyModRing r h).prod excluding |0|) X = n) +Proof rpt (stripDup[FiniteField_def]) >> qabbrev_tac `d = ordz n (CARD R)` >> `0 < d /\ d <> 1` by decide_tac >> @@ -3212,7 +3212,7 @@ val poly_unity_special_factor_exists = store_thm( `poly_divides st k (Unity t n)` by metis_tac[subring_poly_divides_iff, poly_monic_ulead] >> `MAP (LINV up R) (Unity t n) = unity n` by metis_tac[subring_poly_unity, field_iso_poly_unity] >> `h pdivides (unity n)` by prove_tac[field_iso_poly_divides_iff] >> - rw[GSYM poly_divides_mod_zero]) >- + rw[GSYM poly_divides_alt]) >- rw_tac std_ss[] >> qabbrev_tac `u = PolyModRing r h` >> qabbrev_tac `su = PolyModConst r h` >> @@ -3238,7 +3238,8 @@ val poly_unity_special_factor_exists = store_thm( `X IN ring_conjugates u su (f x)` by metis_tac[] >> `u.sum.id = |0|` by rw[poly_mod_ring_ids, Abbr`u`] >> `order (u.prod excluding u.sum.id) (f x) = n` by rw[finite_field_element_mirror_order, Abbr`f`] >> - metis_tac[finite_field_conjugates_order]); + metis_tac[finite_field_conjugates_order] +QED (* This is the much sought-after theorem! *) @@ -3260,7 +3261,7 @@ val poly_unity_special_factor_exists_1 = store_thm( by poly_unity_special_factor_exists Now 0 < deg z by poly_irreducible_deg_nonzero and ulead z by poly_monic_pmonic, 0 < deg z - Also z pdivides (unity k) by poly_ulead_divides_alt, unity k % z = |0| + Also z pdivides (unity k) by poly_divides_alt, unity k % z = |0| Take this z, and the result follows. *) val poly_unity_special_factor_exists_alt = store_thm( @@ -3272,7 +3273,7 @@ val poly_unity_special_factor_exists_alt = store_thm( `Ring r /\ poly (unity k)` by rw[] >> `?z. mifactor z (unity k) /\ (deg z = ordz k (CARD R)) /\ (forderz X = k)` by metis_tac[poly_unity_special_factor_exists] >> `ulead z` by rw_tac std_ss[poly_monic_ulead] >> - metis_tac[poly_ulead_divides_alt]); + metis_tac[poly_divides_alt]); (* Note: The existence of this special factor of (unity k) is critical in the correctness proof of the AKS algorithm. diff --git a/examples/algebra/finitefield/ffExtendScript.sml b/examples/algebra/finitefield/ffExtendScript.sml index 1cef106493..2fac55ad86 100644 --- a/examples/algebra/finitefield/ffExtendScript.sml +++ b/examples/algebra/finitefield/ffExtendScript.sml @@ -281,82 +281,6 @@ val finite_subset_exists = store_thm( (* Extending Finite Set *) (* ------------------------------------------------------------------------- *) -(* Theorem: FINITE t /\ s SUBSET t /\ INJ f s univ(:'b) /\ INFINITE univ(:'b) ==> - ?g. INJ g t univ(:'b) /\ !x. x IN s ==> (g x = f x) *) -(* Proof: - Let d = t DIFF s. - Then t = s UNION d by UNION_DIFF - and FINITE d by FINITE_DIFF, FINITE t - By finite induction on d. - Base case: INJ f s univ(:'b) ==> ?g. INJ g (s UNION {}) univ(:'b) /\ !x. x IN s ==> (g x = f x) - Since s UNION {} = s by UNION_EMPTY - Take g = f, and f(x) = g(x) for x IN s. - Step case: FINITE s /\ INJ f s univ(:'b) /\ INFINITE univ(:'b) ==> - ?g. INJ g (s UNION d) univ(:'b) /\ !x. x IN s ==> (g x = f x) ==> - e NOTIN d /\ INJ f s univ(:'b) ==> - ?g. INJ g (s UNION (e INSERT d)) univ(:'b) /\ !x. x IN s ==> (g x = f x) - Let t = s UNION d. - Then ?g. INJ g t univ(:'b) /\ !x. x IN s ==> (g x = f x) by induction hypothesis - If e IN s, - Then s UNION (e INSERT d) = t by EXTENSION - so take this g, and the result follows. - If e NOTIN s, - Then e NOTIN t by IN_UNION - and s UNION (e INSERT d) = e INSERT t by EXTENSION - and !x. x IN t <=> x IN s \/ x IN d by IN_UNION - Now FINITE t by FINITE_UNION - so FINITE (IMAGE g t) by IMAGE_FINITE - ==> ?y. y NOTIN (IMAGE g t) by NOT_IN_FINITE, INFINITE univ(:'b) - Let g' = \x. if x = e then y else g x. - Then INJ g' t univ(:'b) by INJ_DEF, IN_IMAGE - and !x. x IN s ==> x <> e by given, e NOTIN s - thus !x. x IN s ==> (g' x = f x) by notation, g' x = g x when e NOTIN s. -*) -val subset_inj_extension_exists = store_thm( - "subset_inj_extension_exists", - ``!s t f. FINITE t /\ s SUBSET t /\ INJ f s univ(:'b) /\ INFINITE univ(:'b) ==> - ?g. INJ g t univ(:'b) /\ !x. x IN s ==> (g x = f x)``, - rpt strip_tac >> - qabbrev_tac `d = t DIFF s` >> - `t = s UNION d` by rw[UNION_DIFF, Abbr`d`] >> - fs[] >> - `FINITE d` by rw[Abbr`d`] >> - rpt (pop_assum mp_tac) >> - `FINITE d ==> FINITE s /\ INJ f s univ(:'b) /\ INFINITE univ(:'b) ==> - ?g. INJ g (s UNION d) univ(:'b) /\ !x. x IN s ==> (g x = f x)` suffices_by metis_tac[] >> - qid_spec_tac `d` >> - Induct_on `FINITE` >> - fs[] >> - rpt strip_tac >- - metis_tac[] >> - `?g. INJ g (s UNION d) univ(:'b) /\ !x. x IN s ==> (g x = f x)` by rw[] >> - qabbrev_tac `t = s UNION d` >> - Cases_on `e IN s` >| [ - (`s UNION (e INSERT d) = t` by (rw[EXTENSION, Abbr`t`] >> metis_tac[])) >> - metis_tac[], - `e NOTIN t` by rw[Abbr`t`] >> - (`s UNION (e INSERT d) = e INSERT t` by (rw[EXTENSION, Abbr`t`] >> metis_tac[])) >> - `!x. x IN t <=> x IN s \/ x IN d` by rw[Abbr`t`] >> - `FINITE t` by rw[Abbr`t`] >> - `FINITE (IMAGE g t)` by rw[] >> - `?y. y NOTIN (IMAGE g t)` by metis_tac[NOT_IN_FINITE] >> - qexists_tac `\x. if x = e then y else g x` >> - rpt strip_tac >| [ - rw[INJ_DEF, IN_INSERT] >- - metis_tac[INJ_DEF] >- - metis_tac[IN_IMAGE] >- - metis_tac[INJ_DEF] >- - metis_tac[IN_IMAGE] >- - metis_tac[IN_IMAGE] >- - metis_tac[INJ_DEF] >- - metis_tac[IN_IMAGE] >> - metis_tac[INJ_DEF], - metis_tac[] - ] - ]); - -(* The above proof is clumsy. Next is better without FINITE induction. *) - (* Theorem: FINITE t /\ s SUBSET t /\ INJ f s univ(:'b) /\ INFINITE univ(:'b) ==> ?g. INJ g t univ(:'b) /\ !x. x IN s ==> (g x = f x) *) (* Proof: @@ -593,12 +517,6 @@ val finite_field_clone_extension_exists = store_thm( !n. 0 < n ==> ?(t:'a field) (s:'a field) f. FiniteField t /\ FiniteField s /\ FieldIso f r s /\ s <<= t /\ (CARD C = (CARD R) ** n) *) (* Proof: by finite_field_clone_extension_exists, matching types. *) -val finite_field_self_extension_exists = store_thm( - "finite_field_self_extension_exists", - ``!r:'a field. FiniteField r /\ INFINITE univ(:'a) ==> - !n. 0 < n ==> ?(t:'a field) (s:'a field) f. FiniteField t /\ FiniteField s /\ - FieldIso f r s /\ s <<= t /\ (CARD C = (CARD R) ** n)``, - rw[finite_field_clone_extension_exists]); (* Better use theorem type transform *) val finite_field_self_extension_exists = save_thm("finite_field_self_extension_exists", diff --git a/examples/algebra/finitefield/ffInstancesScript.sml b/examples/algebra/finitefield/ffInstancesScript.sml index 28aae89904..2bded74244 100644 --- a/examples/algebra/finitefield/ffInstancesScript.sml +++ b/examples/algebra/finitefield/ffInstancesScript.sml @@ -529,56 +529,6 @@ val GF_4_mult_b_a = store_thm( (* Theorem: Group ((GF_4).prod excluding [] *) (* Proof: - By Group_def, this is to show: - (1) Monoid ((GF_4).prod excluding []) - Field (GF 2) by GF_2_field - poly_monic (GF 2) h by GF_2_monic_h - irreducible (PolyRing (GF 2)) h by GF_2_irreducible_h - (PolyRing (GF 2)).sum.id = [] by poly_ring_ids - Hence true by poly_mod_ring_prod_monoid - (2) monoid_invertibles ((GF_4).prod excluding []) = ((GF_4).prod excluding []).carrier - This is to show: - x <> [] /\ x IN (GF_4).prod.carrier ==> - ?y. (y IN (GF_4).prod.carrier /\ y <> []) /\ - ((GF_4).prod.op x y = (GF_4).prod.id) /\ - ((GF_4).prod.op y x = (GF_4).prod.id) - Now, Ring (GF_4) by GF_4_ring - Hence GF_4).prod.carrier = (GF_4).carrier by ring_carriers - and GF_4).prod.id = [1] by GF_4_prod_id - Expand by GF_4_carrier, this is to show: - x IN {[]; [1]; [0; 1]; [1; 1]} /\ x <> [] ==> - ?y. (y IN {[]; [1]; [0; 1]; [1; 1]} /\ y <> []) /\ - ((GF_4).prod.op x y = [1]) /\ - ((GF_4).prod.op y x = [1]) - We have - (GF_4).prod.op [1] [1] = [1] by GF_4_mult_1_1 - (GF_4).prod.op [0;1] [1;1] = [1] by GF_4_mult_a_b - (GF_4).prod.op [1;1] [0;1] = [1] by GF_4_mult_b_a - Hence all x have inverse y. -*) -val GF_4_prod_group = store_thm( - "GF_4_prod_group", - ``Group ((GF_4).prod excluding [])``, - rw_tac std_ss[Group_def] >| [ - `Field (GF 2)` by rw[GF_2_field] >> - `poly_monic (GF 2) h` by rw[GF_2_monic_h] >> - `irreducible (PolyRing (GF 2)) h` by rw[GF_2_irreducible_h] >> - `(PolyRing (GF 2)).sum.id = []` by rw[] >> - metis_tac[poly_mod_ring_prod_monoid], - rw_tac std_ss[monoid_invertibles_def, excluding_def, IN_DIFF, IN_SING, EXTENSION, GSPECIFICATION] >> - rw[EQ_IMP_THM] >> - `Ring (GF_4)` by rw[GF_4_ring] >> - `(GF_4).prod.carrier = (GF_4).carrier` by rw[ring_carriers] >> - `(GF_4).prod.id = [1]` by rw[GF_4_prod_id] >> - full_simp_tac std_ss[GF_4_carrier] >> - `!z. z IN {[]; [1]; [0; 1]; [1; 1]} <=> (z = []) \/ (z = [1]) \/ (z = [0;1]) \/ (z = [1;1])` by rw[] >> - `(GF_4).prod.op [1] [1] = [1]` by rw[GF_4_mult_1_1] >> - `(GF_4).prod.op [0;1] [1;1] = [1]` by rw[GF_4_mult_a_b] >> - `(GF_4).prod.op [1;1] [0;1] = [1]` by rw[GF_4_mult_b_a] >> - metis_tac[NOT_CONS_NIL] - ]); - -(* Another Proof: Since Field (GF 2) by GF_2_field poly_monic (GF 2) h by GF_2_monic_h irreducible (PolyRing (GF 2)) h by GF_2_irreducible_h @@ -594,24 +544,6 @@ val GF_4_prod_group = store_thm( (* Theorem: Field (GF_4) *) (* Proof: - By Field_def, this is to show: - (1) Ring (GF_4) - True by GF_4_ring. - (2) Group ((GF_4).prod excluding (GF_4).sum.id) - Ring (GF_4) by GF_4_ring - (GF_4).sum.id = [] by GF_4_sum_id - Hence true by GF_4_prod_group -*) -val GF_4_field = store_thm( - "GF_4_field", - ``Field (GF_4)``, - rw_tac std_ss[Field_def] >- - rw[GF_4_ring] >> - `Ring (GF_4)` by rw_tac std_ss[GF_4_ring] >> - `(GF_4).sum.id = []` by rw_tac std_ss[GF_4_sum_id] >> - rw_tac std_ss[GF_4_prod_group]); - -(* Another Proof: Since Field (GF 2) by GF_2_field poly_monic (GF 2) h by GF_2_monic_h irreducible (PolyRing (GF 2)) h by GF_2_irreducible_h diff --git a/examples/algebra/finitefield/ffMasterScript.sml b/examples/algebra/finitefield/ffMasterScript.sml index 59e961c4e0..de9c2fb55f 100644 --- a/examples/algebra/finitefield/ffMasterScript.sml +++ b/examples/algebra/finitefield/ffMasterScript.sml @@ -1028,160 +1028,6 @@ val subfield_element_condition = store_thm( (* This is a milestone theorem. *) -(* Theorem: FiniteField r ==> !s. s <<= r ==> - !p. poly p ==> (Poly s p <=> (p ** CARD B = peval p (X ** CARD B))) *) -(* Proof: - Note FiniteField s by subfield_finite_field - and char s = char r by subfield_char - Let m = CARD B, c = char r. - Then prime c by finite_field_char - and ?d. 0 < d /\ (m = c ** d) by finite_field_card - - Step 1: compute p ** m - Let n = SUC (deg p). - Claim: p ** m = poly_sum (GENLIST (\k. (p ' k) ** m * (X ** m) ** k) n) - Proof: Let f = \k. p ' k, then rfun f by poly_coeff_ring_fun - p ** m - = (poly_sum (GENLIST (\k. p ' k * X ** k) n)) ** m by poly_eq_poly_sum - = (poly_sum (GENLIST (\k. f k * X ** k) n)) ** m by FUN_EQ_THM, poly_cmult_exp, poly_exp_mult_comm - = poly_sum (GENLIST (\k. f k * X ** k) ** m) n) by poly_sum_freshman_all - = poly_sum (GENLIST (\k. (f k) ** m * (X ** k) ** m) n) by EXP_BASE_MULT - = poly_sum (GENLIST (\k. (f k) ** m * (X ** m) ** k) n) by MULT_COMM - = poly_sum (GENLIST (\k. (p ' k) ** m * (X ** m) ** k) n) by f = \k. p ' k - - If part: Poly s p ==> p ** m = peval p (X ** m) - Since Poly s p - ==> !k. p ' k IN B by subfield_eq_subring, subring_poly_coeff, poly_coeff_element - ==> !k. (p ' k) ** m = p ' k by finite_field_fermat_thm, subfield_exp [1] - Thus peval p (X ** m) - = poly_sum (GENLIST (\k. p ' k * (X ** m) ** k) (SUC (deg p))) by poly_peval_by_poly_sum - = p ** m by Step 1 - - Only-if part: p ** m = peval p (X ** m) ==> Poly s p - Let q = poly_sum (GENLIST (\k. (p ' k) ** m * X ** k) n) - - Claim: p ** m = peval q (X ** m) - Proof: Note rfun (\k. (p ' k) ** m) by ring_fun_def, poly_coeff_element - Let g = (\k. (p ' k) ** m * X ** k), then poly_fun g by poly_fun_from_ring_fun - peval q (X ** m) - = poly_sum (MAP (\x. peval x (X ** m)) (GENLIST g n)) by poly_peval_poly_sum_gen, poly_fun g - = poly_sum (GENLIST ((\x. peval x (X ** m)) o g) n) by MAP_GENLIST - = poly_sum (GENLIST (\k. (p ' k) ** m * (X ** m) ** k) n) by FUN_EQ_THM, poly_peval_cmult, poly_peval_X_exp - Hence p ** m = peval q (X ** m) by Claim 1 - - Note p ** m = peval q (X ** m) by Claim 2 - Since deg (X ** m) = m by poly_deg_X_exp - and 0 < m by finite_field_card_pos - peval q (X ** m) = peval p (X ** m) - ==> q = p by poly_peval_eq, 0 < deg (X ** m) - Claim: !k. q ' k = (p ' k) ** m [1] - Proof: If p = |0|, - Then q = |0|, - so (p ' k = #0) /\ (q ' k = #0) by poly_coeff_zero - and (p ' k) ** m = #0 by field_zero_exp, m <> 0 - Hence true. - If p <> |0|, - If deg p < k, - Then (p ' k = #0) /\ (q ' k = #0) by poly_coeff_nonzero - and (p ' k) ** m = #0 by field_zero_exp, m <> 0 - Hence true. - If ~(deg p < k), - Let f = \k. p ' k ** m - Then rfun f by ring_fun_def, poly_coeff_element, ring_exp_element - and f (deg p) - = p ' (deg p) ** m - = (lead p) ** m by poly_coeff_lead, p <> |0| - <> #0 by field_exp_eq_zero, poly_lead_nonzero - q ' k - = f k by poly_sum_gen_coeff - = (p ' k) ** m - - Hence !k. q ' k = (p ' k) ** m by claim - Also !k. q ' k = p ' k by q = p, [2] - Thus !k. (p ' k) ** m = p ' k by [1], [2] - Now !k. p ' k IN R by poly_coeff_element - thus !k. p ' k IN B by subfield_element_condition - Hence cpoly r s p by common_poly_alt - or Poly s p by subring_poly_alt -*) -val subfield_poly_condition = store_thm( - "subfield_poly_condition", - ``!r:'a field. FiniteField r ==> !s. s <<= r ==> - !p. poly p ==> (Poly s p <=> (p ** CARD B = peval p (X ** CARD B)))``, - rpt (stripDup[FiniteField_def]) >> - `FiniteField s` by metis_tac[subfield_finite_field] >> - `Ring r /\ Ring s /\ #1 <> #0` by rw[] >> - qabbrev_tac `m = CARD B` >> - qabbrev_tac `c = char r` >> - `poly X /\ poly (X ** m)` by rw[] >> - `prime c` by rw[finite_field_char, Abbr`c`] >> - `char s = c` by rw[subfield_char, Abbr`c`] >> - `?d. 0 < d /\ (m = c ** d)` by metis_tac[finite_field_card] >> - qabbrev_tac `n = SUC (deg p)` >> - `p ** m = poly_sum (GENLIST (\k. (p ' k) ** m * (X ** m) ** k) n)` by - (`(\k. (p ' k * X ** k) ** m) = (\k. (p ' k) ** m * (X ** m) ** k)` by rw[FUN_EQ_THM, poly_cmult_exp, poly_exp_mult_comm] >> - qabbrev_tac `f = \k. p ' k` >> - `rfun f` by rw[poly_coeff_ring_fun, Abbr`f`] >> - `(\j. f j * X ** j) = (\k. p ' k * X ** k)` by rw[Abbr`f`] >> - `p = poly_sum (GENLIST (\k. p ' k * X ** k) n)` by rw[poly_eq_poly_sum, Abbr`n`] >> - `p ** m = poly_sum (GENLIST (\k. (p ' k * X ** k) ** m) n)` by metis_tac[poly_sum_freshman_all] >> - rw[]) >> - rewrite_tac[EQ_IMP_THM] >> - rpt strip_tac >| [ - `!k. p ' k IN B` by metis_tac[subfield_eq_subring, subring_poly_coeff, poly_coeff_element] >> - `!k. (p ' k) ** m = p ' k` by metis_tac[finite_field_fermat_thm, subfield_exp] >> - rw[poly_peval_by_poly_sum], - qabbrev_tac `q = poly_sum (GENLIST (\k. (p ' k) ** m * X ** k) n)` >> - `p ** m = peval q (X ** m)` by - (qabbrev_tac `g = (\k. (p ' k) ** m * X ** k)` >> - `poly_fun g` by rw[poly_fun_from_ring_fun, Abbr`g`] >> - `(\x. peval x (X ** m)) o g = (\k. (p ' k) ** m * (X ** m) ** k)` by rw[FUN_EQ_THM, poly_peval_cmult, poly_peval_X_exp, Abbr`g`] >> - `peval q (X ** m) = poly_sum (MAP (\x. peval x (X ** m)) (GENLIST g n))` by rw[poly_peval_poly_sum_gen, Abbr`q`, Abbr`g`] >> - `_ = poly_sum (GENLIST ((\x. peval x (X ** m)) o g) n)` by rw[MAP_GENLIST] >> - `_ = poly_sum (GENLIST (\k. p ' k ** m * (X ** m) ** k) n)` by rw[] >> - metis_tac[]) >> - `deg (X ** m) = m` by rw[] >> - `0 < m` by rw[finite_field_card_pos, Abbr`m`] >> - `m <> 0` by decide_tac >> - `poly q` by rw[poly_sum_poly, poly_list_gen_from_ring_fun, Abbr`q`] >> - `q = p` by metis_tac[poly_peval_eq] >> - `!k. q ' k = (p ' k) ** m` by - (rpt strip_tac >> - Cases_on `p = |0|` >- - rw[field_zero_exp] >> - Cases_on `deg p < k` >- - rw[poly_coeff_nonzero, field_zero_exp] >> - qabbrev_tac `f = \k. p ' k ** m` >> - `rfun f` by metis_tac[ring_fun_def, poly_coeff_element, ring_exp_element] >> - `f (deg p) = p ' (deg p) ** m` by rw[Abbr`f`] >> - `_ = (lead p) ** m` by metis_tac[poly_coeff_lead] >> - `lead p IN R` by rw[] >> - `f (deg p) <> #0` by metis_tac[field_exp_eq_zero, poly_lead_nonzero] >> - `GENLIST (\k. p ' k ** m * X ** k) n = GENLIST (\k. f k * X ** k) (SUC (deg p))` by rw[] >> - `q = poly_sum (GENLIST (\k. f k * X ** k) (SUC (deg p)))` by metis_tac[] >> - `q ' k = f k` by rw[poly_sum_gen_coeff] >> - rw[] - ) >> - `!k. q ' k = p ' k` by rw[] >> - `!k. p ' k IN B` by metis_tac[poly_coeff_element, subfield_element_condition] >> - metis_tac[subfield_is_subring, subring_poly_alt, common_poly_alt] - ]); - -(* This is a major milestone theorem. *) -(* Proof is still clunky: - Need to have: p ** m = poly_sum (GENLIST (\k. (p ' k) ** m * (X ** m) ** k) n) - This half-result is used for if-part. - Then complete by: peval q (X ** m) = poly_sum (GENLIST (\k. (p ' k) ** m * (X ** m) ** k) n) - To establish: p ** m = peval q (X ** m) for only-if part. - - Did try to show: p ** m = peval q (X ** m) in one go, - but applying this full result to if-part has problems. - - Actually, the proof is good, because the if-part depends only on p, - and it has nothing to do with q. The following is essentially a smooth-out - version of the same proof -- not much difference! -*) - (* Theorem: FiniteField r ==> !s. s <<= r ==> !p. poly p ==> (Poly s p <=> (p ** CARD B = peval p (X ** CARD B))) *) (* Proof: @@ -1507,21 +1353,6 @@ val monic_irreducibles_degree_poly_set = store_thm( ``!r:'a ring. !n. pset (monic_irreducibles_degree r n)``, metis_tac[monic_irreducibles_degree_monic_set, monic_set_poly_set]); -(* Original proof of the same theorem *) - -(* Theorem: pset (monic_irreducibles_degree r n) *) -(* Proof: - Let s = monic_irreducibles_degree r n. - !p. p IN s - ==> monic p by monic_irreducibles_degree_member - ==> poly p by poly_monic_poly - Hence pset s by notation -*) -val monic_irreducibles_degree_poly_set = store_thm( - "monic_irreducibles_degree_poly_set", - ``!r:'a ring. !n. pset (monic_irreducibles_degree r n)``, - rw[monic_irreducibles_degree_member]); - (* Theorem: Field r ==> !n. pcoprime_set (monic_irreducibles_degree r n) *) (* Proof: By poly_coprime_set_def, this is to show: @@ -1895,112 +1726,6 @@ val monic_irreducibles_degree_nonempty_inj = store_thm( rw[INJ_DEF] >> metis_tac[monic_irreducibles_degree_disjoint, INTER_IDEMPOT, DISJOINT_DEF]); -(* Theorem: SIGMA (deg o PPROD) (IMAGE (monic_irreducibles_degree r) (divisors n)) = - SIGMA (deg o PPROD o monic_irreducibles_degree r) (divisors n) *) -(* Proof: - Let f = monic_irreducibles_degree r, - s1 = {d | d IN (divisors n) /\ (f d = {})}, - s2 = {d | d IN (divisors n) /\ (f d <> {})}. - Then divisors n = s1 UNION s2 by EXTENSION - and DISJOINT s1 s2 by EXTENSION, DISJOINT_DEF - and DISJOINT (IMAGE f s1) (IMAGE f s2) by EXTENSION, DISJOINT_DEF - Now s1 SUBSET (divisors n) by SUBSET_DEF - s2 SUBSET (divisors n) by SUBSET_DEF - Since FINITE (divisors n) by divisors_finite - thus FINITE s1 /\ FINITE s2 by SUBSET_FINITE - and FINITE (IMAGE f s1) /\ FINITE (IMAGE f s2) by IMAGE_FINITE - - Step 1: decompose left summation - SIGMA (deg o PPROD) (IMAGE f (divisors n)) - = SIGMA (deg o PPROD) (IMAGE f (s1 UNION s2)) by above, divisors n = s1 UNION s2 - = SIGMA (deg o PPROD) ((IMAGE f s1) UNION (IMAGE f s2)) by IMAGE_UNION - = SIGMA (deg o PPROD) (IMAGE f s1) + - SIGMA (deg o PPROD) (IMAGE f s2) by SUM_IMAGE_DISJOINT - - Claim: SIGMA (deg o PPROD) (IMAGE f s1) = 0 - Proof: If s1 = {}, - SIGMA (deg o PPROD) (IMAGE f {}) - = SIGMA (deg o PPROD) {} by IMAGE_EMPTY - = 0 by SUM_IMAGE_EMPTY - If s1 <> {}, - Note !d. d IN s1 ==> (f d = {}) by definition of s1 - Thus !x. x IN (IMAGE f s1) ==> (x = {}) by IN_IMAGE, IMAGE_EMPTY - Since s1 <> {}, IMAGE f s1 = {{}} by SING_DEF, IN_SING, SING_ONE_ELEMENT - SIGMA (deg o PPROD) (IMAGE f {}) - = SIGMA (deg o PPROD) {{}} by above - = (deg o PPROD) {} by SUM_IMAGE_SING - = deg (PPROD {}) by function application - = deg |1| by poly_prod_set_empty - = 0 by poly_deg_one - - Step 2: decompose right summation - Also SIGMA (deg o PPROD o f) (divisors n) - = SIGMA (deg o PPROD o f) (s1 UNION s2) by above, divisors n = s1 UNION s2 - = SIGMA (deg o PPROD o f) s1 + - SIGMA (deg o PPROD o f) s2 by SUM_IMAGE_DISJOINT - - Claim: SIGMA (deg o PPROD o f) s1 = 0 - Proof: Note !d. d IN s1 ==> (f d = {}) by definition of s1 - (deg o PPROD o f) d - = deg (PPROD (f d)) by function application - = deg (PPROD {}) by above - = deg |1| by poly_prod_set_empty - = 0 by poly_deg_one - Hence SIGMA (deg o PPROD o f) s1 - = 0 * CARD s1 by SIGMA_CONSTANT - = 0 by MULT - - Claim: SIGMA (deg o PPROD) (IMAGE f s2) = SIGMA (deg o PPROD o f) (s2) - Proof: Note !d. d IN s2 ==> f d <> {} by definition of s2 - Thus INJ f s2 univ(:'a poly -> bool) by monic_irreducibles_degree_nonempty_inj - Hence SIGMA (deg o PPROD) (IMAGE f s2) - = SIGMA (deg o PPROD o f) (s2) by sum_image_by_composition - - Result follows by combining all the claims and arithmetic. -*) -val monic_irreducibles_degree_poly_prod_deg_sum = store_thm( - "monic_irreducibles_degree_poly_prod_deg_sum", - ``!r:'a ring. !n. SIGMA (deg o PPROD) (IMAGE (monic_irreducibles_degree r) (divisors n)) = - SIGMA (deg o PPROD o monic_irreducibles_degree r) (divisors n)``, - rpt strip_tac >> - qabbrev_tac `f = monic_irreducibles_degree r` >> - qabbrev_tac `s1 = {d | d IN (divisors n) /\ (f d = {})}` >> - qabbrev_tac `s2 = {d | d IN (divisors n) /\ (f d <> {})}` >> - (`divisors n = s1 UNION s2` by (rw[Abbr`s1`, Abbr`s2`, EXTENSION] >> metis_tac[])) >> - (`DISJOINT s1 s2` by (rw[Abbr`s1`, Abbr`s2`, EXTENSION, DISJOINT_DEF] >> metis_tac[])) >> - (`DISJOINT (IMAGE f s1) (IMAGE f s2)` by (rw[Abbr`s1`, Abbr`s2`, EXTENSION, DISJOINT_DEF] >> metis_tac[])) >> - `s1 SUBSET (divisors n) /\ s2 SUBSET (divisors n)` by rw[Abbr`s1`, Abbr`s2`, SUBSET_DEF] >> - `FINITE (divisors n)` by rw[divisors_finite] >> - `FINITE s1 /\ FINITE s2` by metis_tac[SUBSET_FINITE] >> - `FINITE (IMAGE f s1) /\ FINITE (IMAGE f s2)` by rw[] >> - `SIGMA (deg o PPROD) (IMAGE f (divisors n)) = SIGMA (deg o PPROD) ((IMAGE f s1) UNION (IMAGE f s2))` by rw[] >> - `_ = SIGMA (deg o PPROD) (IMAGE f s1) + SIGMA (deg o PPROD) (IMAGE f s2)` by rw[SUM_IMAGE_DISJOINT] >> - `SIGMA (deg o PPROD) (IMAGE f s1) = 0` by - (Cases_on `s1 = {}` >- - rw[SUM_IMAGE_EMPTY] >> - `!d. d IN s1 ==> (f d = {})` by rw[Abbr`s1`] >> - `!x. x IN (IMAGE f s1) ==> (x = {})` by metis_tac[IN_IMAGE, IMAGE_EMPTY] >> - `{} IN {{}} /\ IMAGE f s1 <> {}` by rw[] >> - `IMAGE f s1 = {{}}` by metis_tac[SING_DEF, IN_SING, SING_ONE_ELEMENT] >> - `SIGMA (deg o PPROD) (IMAGE f s1) = (deg o PPROD) {}` by rw[SUM_IMAGE_SING] >> - rw[poly_prod_set_empty] - ) >> - `SIGMA (deg o PPROD o f) (divisors n) = SIGMA (deg o PPROD o f) s1 + SIGMA (deg o PPROD o f) s2` by rw[SUM_IMAGE_DISJOINT] >> - `SIGMA (deg o PPROD o f) s1 = 0` by - (`!d. d IN s1 ==> (f d = {})` by rw[Abbr`s1`] >> - `!d. d IN s1 ==> ((deg o PPROD o f) d = 0)` by rw[poly_prod_set_empty] >> - metis_tac[SIGMA_CONSTANT, MULT]) >> - `SIGMA (deg o PPROD) (IMAGE f s2) = SIGMA (deg o PPROD o f) s2` by - (`!d. d IN s2 ==> f d <> {}` by rw[Abbr`s2`] >> - `INJ f s2 univ(:'a poly -> bool)` by rw[monic_irreducibles_degree_nonempty_inj, Abbr`f`] >> - rw[sum_image_by_composition]) >> - rw[]); - -(* This proof is unusual, unexpected, highly specialized and unique. *) -(* This is so unique for the next theorem that it will be a local lemma. *) - -(* Extract a general theorem from above and prove lemma again by using the general theorem *) - (* Theorem: SIGMA (deg o PPROD) (IMAGE (monic_irreducibles_degree r) (divisors n)) = SIGMA (deg o PPROD o monic_irreducibles_degree r) (divisors n) *) (* Proof: diff --git a/examples/algebra/finitefield/ffMinimalScript.sml b/examples/algebra/finitefield/ffMinimalScript.sml index 9980c07009..0eae975908 100644 --- a/examples/algebra/finitefield/ffMinimalScript.sml +++ b/examples/algebra/finitefield/ffMinimalScript.sml @@ -945,7 +945,7 @@ val poly_minimal_divides_subfield_poly_iff = store_thm( <=> eval h x = #0 by above <=> root h x by poly_root_def <=> m pdivides h by poly_minimal_divides_subfield_poly_iff - <=> h % m = |0| by poly_divides_mod_zero, ulead m + <=> h % m = |0| by poly_divides_alt, ulead m <=> p % m = q % m by poly_mod_eq, ulead m *) val poly_minimal_eval_congruence = store_thm( @@ -964,7 +964,7 @@ val poly_minimal_eval_congruence = store_thm( `_ = (eval h x = #0)` by rw[Abbr`h`] >> `_ = root h x` by rw[poly_root_def] >> `_ = (m pdivides h)` by rw[poly_minimal_divides_subfield_poly_iff, Abbr`m`] >> - `_ = (h % m = |0|)` by rw[poly_divides_mod_zero] >> + `_ = (h % m = |0|)` by rw[poly_divides_alt] >> `_ = (p % m = q % m)` by rw[poly_mod_eq, Abbr`h`] >> rw[]); diff --git a/examples/algebra/finitefield/ffPolyScript.sml b/examples/algebra/finitefield/ffPolyScript.sml index 872be2662e..8127a4eec5 100644 --- a/examples/algebra/finitefield/ffPolyScript.sml +++ b/examples/algebra/finitefield/ffPolyScript.sml @@ -937,68 +937,6 @@ val subring_poly_division_eqn = store_thm( `?u v. Poly s u /\ Poly s v /\ (p = poly_add s (poly_mult s u q) v) /\ poly_deg s v < poly_deg s q ` by rw[poly_division_eqn] >> metis_tac[subring_poly_add, subring_poly_mult, poly_mult_poly, subring_poly_deg]); -(* STOP; HERE; *) - -(* Theorem: s <= r ==> !p q. Poly s p /\ Ulead s q ==> - (poly_div s p q = p / q) /\ (poly_mod s p q = p % q) *) -(* Proof: - Note ulead q by subring_poly_ulead - and poly p by subring_poly_poly - and Deg s q = deg q by subring_poly_deg - - If deg q = 0, - Then (p / q = |/(lead q) * p) /\ (p % q = |0|) by poly_div_mod_by_const - and poly_div s p q = poly_cmult s (Inv s (Lead s q)) p /\ - poly_mod s p q = poly_zero s by poly_div_mod_by_const - but Inv s (Lead s q) = |/ (lead q) by subring_unit_inv, subring_poly_lead - Now lead q IN R by poly_lead_element - Thus poly_div s p q = p / q by subring_poly_cmult, ring_unit_inv_element - and poly_mod s p q = p % q by subring_poly_zero - - If deg q <> 0, - Then Deg q <> 0, or Pmonic s q. - Note pmonic q by subring_poly_pmonic - ==> ?u v. Poly s u /\ Poly s v /\ (p = u * q + v) /\ deg v < deg q - by subring_poly_division_eqn - - Step 1: show u = p / q, v = p % q - Note poly p /\ poly q /\ poly u /\ poly v by subring_poly_poly - ==> (u = p / q) /\ (v = p % q) by poly_div_unique, poly_mod_unique - - Step 2: show u = poly_div s p q, v = poly_mod s p q - Note Deg s v < Deg s q by subring_poly_deg - and Poly s (poly_mult s u q) by poly_mult_poly - thus p = poly_add s (poly_mult s u q) v by subring_poly_add, subring_poly_mult - ==> (u = poly_div s p q) /\ (v = poly_mod s p q) - by poly_div_unique, poly_mod_unique - - Hence (poly_div s p q = u = p / q) /\ (poly_mod s p q = v = p % q) -*) -val subring_poly_div_mod = store_thm( - "subring_poly_div_mod", - ``!(r s):'a ring. s <= r ==> !p q. Poly s p /\ Ulead s q ==> - (poly_div s p q = p / q) /\ (poly_mod s p q = p % q)``, - ntac 6 strip_tac >> - `ulead q` by metis_tac[subring_poly_ulead] >> - `poly p` by metis_tac[subring_poly_poly] >> - `Deg s q = deg q` by rw[subring_poly_deg] >> - Cases_on `deg q = 0` >| [ - `(p / q = |/(lead q) * p) /\ (p % q = |0|)` by rw[poly_div_mod_by_const] >> - `(poly_div s p q = poly_cmult s (Inv s (Lead s q)) p) /\ - (poly_mod s p q = poly_zero s)` by rw[poly_div_mod_by_const] >> - `Inv s (Lead s q) = |/ (lead q)` by metis_tac[subring_unit_inv, subring_poly_lead] >> - metis_tac[poly_lead_element, ring_unit_inv_element, subring_poly_cmult, subring_poly_zero], - `?u v. Poly s u /\ Poly s v /\ (p = u * q + v) /\ deg v < deg q` by rw[subring_poly_division_eqn] >> - `pmonic q` by metis_tac[subring_poly_pmonic, NOT_ZERO] >> - `poly u /\ poly v` by metis_tac[subring_poly_poly] >> - `Deg s v < Deg s q` by metis_tac[subring_poly_deg] >> - `Poly s (poly_mult s u q)` by rw[poly_mult_poly] >> - `p = poly_add s (poly_mult s u q) v` by metis_tac[subring_poly_add, subring_poly_mult] >> - metis_tac[poly_div_unique, poly_mod_unique] - ]); - -(* Better proof of the same theorem. *) - (* Theorem: s <= r ==> !p q. Poly s p /\ Ulead s q ==> (poly_div s p q = p / q) /\ (poly_mod s p q = p % q) *) (* Proof: @@ -1056,10 +994,10 @@ val subring_poly_divides = store_thm( and Pmonic s q ==> pmonic q by subring_poly_pmonic poly_divides s q p - <=> poly_mod s p q = poly_zero s by poly_divides_mod_zero + <=> poly_mod s p q = poly_zero s by poly_divides_alt <=> poly_mod s p q = |0| by subring_poly_zero <=> (p % q) = |0| by subring_poly_div_mod - <=> q pdivides p by poly_divides_mod_zero + <=> q pdivides p by poly_divides_alt *) val subring_poly_divides_iff = store_thm( "subring_poly_divides_iff", @@ -1068,7 +1006,7 @@ val subring_poly_divides_iff = store_thm( rpt strip_tac >> `poly p /\ ulead q` by metis_tac[subring_poly_poly, subring_poly_ulead] >> `poly_zero s = |0|` by rw[subring_poly_zero] >> - metis_tac[poly_divides_mod_zero, subring_poly_div_mod]); + metis_tac[poly_divides_alt, subring_poly_div_mod]); (* This is a generalisation of subring_poly_mult *) diff --git a/examples/algebra/finitefield/ffUnityScript.sml b/examples/algebra/finitefield/ffUnityScript.sml index e01962b58c..1acf6a7ca0 100644 --- a/examples/algebra/finitefield/ffUnityScript.sml +++ b/examples/algebra/finitefield/ffUnityScript.sml @@ -1017,17 +1017,6 @@ val field_order_equal_card_choices = store_thm( `FINITE (forder_eq n)` by rw[field_order_equal_finite] >> metis_tac[FINITE_BIJ_CARD_EQ, phi_def]); -(* Theorem: FiniteField r ==> - !n. 0 < n ==> (CARD (orders f* n) = if (n divides CARD R+ ) then phi n else 0) *) -(* Proof: field_order_equal_eq_orders, field_order_equal_card *) -val field_orders_card = store_thm( - "field_orders_card", - ``!r:'a field. FiniteField r ==> - !n. 0 < n ==> (CARD (orders f* n) = if (n divides CARD R+ ) then phi n else 0)``, - metis_tac[finite_field_is_field, field_order_equal_eq_orders, field_order_equal_card]); - -(* This one is better than the previous one! *) - (* Theorem: FiniteField r ==> !n. CARD (orders f* n) = if (n divides CARD R+ ) then phi n else 0 *) (* Proof: Note cyclic f* by finite_field_mult_group_cyclic diff --git a/examples/algebra/group/groupScript.sml b/examples/algebra/group/groupScript.sml index b6d475587b..c629111d7b 100644 --- a/examples/algebra/group/groupScript.sml +++ b/examples/algebra/group/groupScript.sml @@ -462,8 +462,6 @@ Theorem group_inv_element[simp]: !g:'a group. Group g ==> !x. x IN G ==> |/x IN G Proof rw[monoid_inv_def] QED -(* Below is too much effort for a simple theorem. *) - val gim = Group_def |> SPEC_ALL |> #1 o EQ_IMP_RULE |> UNDISCH_ALL |> CONJUNCT1; val ginv = Group_def |> SPEC_ALL |> #1 o EQ_IMP_RULE |> UNDISCH_ALL |> CONJUNCT2; diff --git a/examples/algebra/lib/helperListScript.sml b/examples/algebra/lib/helperListScript.sml index 04f4b4a081..e0c3c2b01c 100644 --- a/examples/algebra/lib/helperListScript.sml +++ b/examples/algebra/lib/helperListScript.sml @@ -80,6 +80,7 @@ open indexedListsTheory; (* for findi_def *) HEAD_MEM |- !ls. ls <> [] ==> MEM (HD ls) ls LAST_MEM |- !ls. ls <> [] ==> MEM (LAST ls) ls LAST_EQ_HD |- !h t. ~MEM h t /\ LAST (h::t) = h <=> t = [] + MEM_FRONT_NOT_LAST|- !ls. ls <> [] /\ ALL_DISTINCT ls ==> ~MEM (LAST ls) (FRONT ls) NIL_NO_MEM |- !ls. ls = [] <=> !x. ~MEM x ls MEM_APPEND_3 |- !l1 x l2 h. MEM h (l1 ++ [x] ++ l2) <=> MEM h (x::(l1 ++ l2)) DROP_1 |- !h t. DROP 1 (h::t) = t @@ -860,6 +861,33 @@ Proof metis_tac[LAST_CONS_cond, LAST_MEM] QED +(* Theorem: ls <> [] /\ ALL_DISTINCT ls ==> ~MEM (LAST ls) (FRONT ls) *) +(* Proof: + Let k = LENGTH ls. + Then 0 < k by LENGTH_EQ_0, NOT_ZERO + and LENGTH (FRONT ls) = PRE k by LENGTH_FRONT, ls <> [] + so ?n. n < PRE k /\ + LAST ls = EL n (FRONT ls) by MEM_EL + = EL n ls by FRONT_EL, ls <> [] + but LAST ls = EL (PRE k) ls by LAST_EL, ls <> [] + Thus n = PRE k by ALL_DISTINCT_EL_IMP + This contradicts n < PRE k by arithmetic +*) +Theorem MEM_FRONT_NOT_LAST: + !ls. ls <> [] /\ ALL_DISTINCT ls ==> ~MEM (LAST ls) (FRONT ls) +Proof + rpt strip_tac >> + qabbrev_tac `k = LENGTH ls` >> + `0 < k` by metis_tac[LENGTH_EQ_0, NOT_ZERO] >> + `LENGTH (FRONT ls) = PRE k` by fs[LENGTH_FRONT, Abbr`k`] >> + fs[MEM_EL] >> + `LAST ls = EL n ls` by fs[FRONT_EL] >> + `LAST ls = EL (PRE k) ls` by rfs[LAST_EL, Abbr`k`] >> + `n < k /\ PRE k < k` by decide_tac >> + `n = PRE k` by metis_tac[ALL_DISTINCT_EL_IMP] >> + decide_tac +QED + (* Theorem: ls = [] <=> !x. ~MEM x ls *) (* Proof: If part: !x. ~MEM x [], true by MEM @@ -2639,22 +2667,7 @@ val rotate_def = Define ` = EL j l :: DROP (SUC j) l by EL, DROP_def = LHS *) -val rotate_shift_element = store_thm( - "rotate_shift_element", - ``!l n. n < LENGTH l ==> (rotate n l = EL n l::(DROP (SUC n) l ++ TAKE n l))``, - rw[rotate_def] >> - pop_assum mp_tac >> - qid_spec_tac `n` >> - Induct_on `l` >- - rw[] >> - rw[DROP_def] >- - rw[EL_CONS, PRE_SUB1] >> - `?j. n = SUC j` by metis_tac[num_CASES] >> - `j < LENGTH l` by decide_tac >> - `SUC j - 1 = j` by decide_tac >> - rw[DROP_def, TAKE_def]); - -Theorem rotate_shift_element[allow_rebind]: +Theorem rotate_shift_element: !l n. n < LENGTH l ==> (rotate n l = EL n l::(DROP (SUC n) l ++ TAKE n l)) Proof rw[rotate_def] >> @@ -3115,34 +3128,7 @@ val LIST_TO_SET_SING = store_thm( so l1 = t by induction hypothesis giving l2 = h::l1 *) -val MONOLIST_EQ = store_thm( - "MONOLIST_EQ", - ``!l1 l2. SING (set l1) /\ SING (set l2) ==> - ((l1 = l2) <=> (LENGTH l1 = LENGTH l2) /\ (set l1 = set l2))``, - Induct >- - rw[] >> - rw[] >| [ - rw[EQ_IMP_THM] >- - rw[] >- - rw[] >> - `?x. l2 = [x]` by rw[GSYM LENGTH_EQ_1] >> - `set l2 = {x}` by rw[] >> - metis_tac[EQUAL_SING], - rw[EQ_IMP_THM] >- - rw[] >- - rw[] >> - `0 < LENGTH l2` by decide_tac >> - `?k t. l2 = k::t` by metis_tac[LENGTH_NON_NIL, list_CASES] >> - `LENGTH l2 = SUC (LENGTH t)` by rw[] >> - `LENGTH l1 = LENGTH t` by decide_tac >> - `set l2 = k INSERT set t` by rw[] >> - `(set t = {}) \/ (set t = {k})` by metis_tac[SING_INSERT] >- - metis_tac[LIST_TO_SET_EQ_EMPTY, LENGTH_NIL, NOT_SING_EMPTY] >> - `set l2 = set t` by rw[] >> - metis_tac[IN_SING] - ]); - -Theorem MONOLIST_EQ[allow_rebind]: +Theorem MONOLIST_EQ: !l1 l2. SING (set l1) /\ SING (set l2) ==> ((l1 = l2) <=> (LENGTH l1 = LENGTH l2) /\ (set l1 = set l2)) Proof @@ -4891,14 +4877,6 @@ val PROD_SNOC = store_thm( strip_tac >> Induct >> rw[]); -(* proof like SUM_SNOC *) -Theorem PROD_SNOC[allow_rebind]: - !x l. PROD (SNOC x l) = (PROD l) * x -Proof - GEN_TAC THEN INDUCT_THEN list_INDUCT ASSUME_TAC THEN - REWRITE_TAC[PROD, SNOC, MULT, MULT_CLAUSES] THEN - GEN_TAC THEN ASM_REWRITE_TAC[MULT_ASSOC] -QED (* Theorem: PROD (APPEND l1 l2) = PROD l1 * PROD l2 *) (* Proof: @@ -4997,10 +4975,11 @@ val PROD_ACC_PROD_LEM = store_thm (* Theorem: PROD L = PROD_ACC L 1 *) (* Proof: Put n = 1 in PROD_ACC_PROD_LEM *) -val PROD_PROD_ACC = store_thm( - "PROD_PROD_ACC[compute]", - ``!L. PROD L = PROD_ACC L 1``, - rw[PROD_ACC_PROD_LEM]); +Theorem PROD_PROD_ACC[compute]: + !L. PROD L = PROD_ACC L 1 +Proof + rw[PROD_ACC_PROD_LEM] +QED (* EVAL ``PROD [1; 2; 3; 4]``; --> 24 *) @@ -5752,8 +5731,8 @@ Proof QED (* Theorem alias *) -val listRangeLHI_LEN = save_thm("listRangeLHI_LEN", LENGTH_listRangeLHI |> GEN_ALL); -(* val listRangeLHI_LEN = |- !lo hi. LENGTH [lo ..< hi] = hi - lo: thm *) +Theorem listRangeLHI_LEN = LENGTH_listRangeLHI |> GEN_ALL |> SPEC ``m:num`` |> SPEC ``n:num`` |> GEN_ALL; +(* val listRangeLHI_LEN = |- !n m. LENGTH [m ..< n] = n - m: thm *) (* Theorem: ([m ..< n] = []) <=> n <= m *) (* Proof: diff --git a/examples/algebra/lib/helperNumScript.sml b/examples/algebra/lib/helperNumScript.sml index 955e4450fa..46ddedc7b8 100644 --- a/examples/algebra/lib/helperNumScript.sml +++ b/examples/algebra/lib/helperNumScript.sml @@ -145,7 +145,7 @@ open gcdTheory; (* for P_EUCLIDES *) HALF_MULT |- !m n. n * HALF m <= HALF (n * m) 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_ADD1_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 @@ -411,11 +411,11 @@ 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); +Theorem ZERO_LE_ALL = arithmeticTheory.ZERO_LESS_EQ; (* val ZERO_LE_ALL = |- !n. 0 <= n: thm *) (* Theorem alias *) -val NOT_ZERO = save_thm("NOT_ZERO", NOT_ZERO_LT_ZERO); +Theorem NOT_ZERO = arithmeticTheory.NOT_ZERO_LT_ZERO; (* val NOT_ZERO = |- !n. n <> 0 <=> 0 < n: thm *) (* Extract theorem *) @@ -458,6 +458,7 @@ val LE_ONE = store_thm( decide_tac); (* arithmeticTheory.LESS_EQ_SUC_REFL |- !m. m <= SUC m *) + (* Theorem: n < SUC n *) (* Proof: by arithmetic. *) val LESS_SUC = store_thm( @@ -938,7 +939,7 @@ val MULT_RIGHT_ID = store_thm( metis_tac[MULT_EQ_ID, MULT_COMM, NOT_ZERO_LT_ZERO]); (* Theorem alias *) -val MULT_EQ_SELF = save_thm("MULT_EQ_SELF", MULT_RIGHT_ID); +Theorem MULT_EQ_SELF = MULT_RIGHT_ID; (* val MULT_EQ_SELF = |- !n. 0 < n ==> !m. (n * m = n) <=> (m = 1): thm *) (* Theorem: (n * n = n) <=> ((n = 0) \/ (n = 1)) *) @@ -1367,17 +1368,9 @@ Proof ] QED -(* Theorem: HALF (2 * n) = n *) -(* Proof: - Let m = 2 * n. - Then EVEN m by EVEN_DOUBLE - so 2 * HALF m = m = 2 * n by EVEN_HALF - or HALF m = n by MULT_LEFT_CANCEL -*) -val HALF_TWICE = store_thm( - "HALF_TWICE", - ``!n. HALF (2 * n) = n``, - metis_tac[EVEN_DOUBLE, EVEN_HALF, MULT_LEFT_CANCEL, DECIDE``2 <> 0``]); +(* Theorem alias *) +Theorem HALF_TWICE = arithmeticTheory.MULT_DIV_2; +(* val HALF_TWICE = |- !n. HALF (2 * n) = n: thm *) (* Theorem: n * HALF m <= HALF (n * m) *) (* Proof: @@ -1462,8 +1455,8 @@ val TWO_HALF_TIMES_LE = store_thm( = 2 * HALF n <= n by TWO_HALF_LE_THM *) -val SUC_HALF_LE = store_thm( - "SUC_HALF_LE", +val HALF_ADD1_LE = store_thm( + "HALF_ADD1_LE", ``!n. 0 < n ==> 1 + HALF n <= n``, rpt strip_tac >> (Cases_on `n = 1` >> simp[]) >> @@ -3140,11 +3133,11 @@ Proof QED (* Theorem alias *) -val euclid_prime = save_thm("euclid_prime", P_EUCLIDES); +Theorem euclid_prime = gcdTheory.P_EUCLIDES; (* |- !p a b. prime p /\ p divides a * b ==> p divides a \/ p divides b *) (* Theorem alias *) -val euclid_coprime = save_thm("euclid_coprime", L_EUCLIDES); +Theorem euclid_coprime = gcdTheory.L_EUCLIDES; (* |- !a b c. coprime a b /\ b divides a * c ==> b divides c *) (* ------------------------------------------------------------------------- *) @@ -4620,6 +4613,18 @@ val ONE_LT_HALF_SQ = store_thm( `(2 ** 2) DIV 2 = 2` by EVAL_TAC >> decide_tac); +(* Theorem: 0 < n ==> (HALF (2 ** n) = 2 ** (n - 1)) *) +(* Proof + By induction on n. + Base: 0 < 0 ==> 2 ** 0 DIV 2 = 2 ** (0 - 1) + This is trivially true as 0 < 0 = F. + Step: 0 < n ==> HALF (2 ** n) = 2 ** (n - 1) + ==> 0 < SUC n ==> HALF (2 ** SUC n) = 2 ** (SUC n - 1) + HALF (2 ** SUC n) + = HALF (2 * 2 ** n) by EXP + = 2 ** n by MULT_TO_DIV + = 2 ** (SUC n - 1) by SUC_SUB1 +*) Theorem EXP_2_HALF: !n. 0 < n ==> (HALF (2 ** n) = 2 ** (n - 1)) Proof diff --git a/examples/algebra/lib/helperSetScript.sml b/examples/algebra/lib/helperSetScript.sml index 98b57477a1..39aba066be 100644 --- a/examples/algebra/lib/helperSetScript.sml +++ b/examples/algebra/lib/helperSetScript.sml @@ -1589,39 +1589,6 @@ Proof rw[] QED -(* Another Proof: *) -(* Theorem: MAX_SET (IMAGE SUC (count n)) = n *) -(* Proof: - By induction on n. - Base case: MAX_SET (IMAGE SUC (count 0)) = 0 - LHS = MAX_SET (IMAGE SUC (count 0)) - = MAX_SET (IMAGE SUC {}) by COUNT_ZERO - = MAX_SET {} by IMAGE_EMPTY - = 0 by MAX_SET_DEF - = RHS - Step case: MAX_SET (IMAGE SUC (count n)) = n ==> - MAX_SET (IMAGE SUC (count (SUC n))) = SUC n - Note: FINITE (IMAGE SUC (count n)) by FINITE_COUNT, IMAGE_FINITE - LHS = MAX_SET (IMAGE SUC (count (SUC n))) - = MAX_SET (IMAGE SUC (n INSERT (count n))) by COUNT_SUC - = MAX_SET ((SUC n) INSERT (IMAGE SUC (count n))) by IMAGE_INSERT - = MAX (SUC n) (MAX_SET (IMAGE SUC (count n))) by MAX_SET_THM - = MAX (SUC n) n by induction hypothesis - = SUC n by LESS_SUC, MAX_DEF - = RHS -*) -Theorem MAX_SET_IMAGE_SUC_COUNT[allow_rebind]: - !n. MAX_SET (IMAGE SUC (count n)) = n -Proof - Induct_on `n` >- - rw[MAX_SET_DEF] >> - ‘MAX_SET (IMAGE SUC (count (SUC n))) = - MAX (SUC n) (MAX_SET (IMAGE SUC (count n)))’ - by rw[COUNT_SUC, MAX_SET_THM] >> - metis_tac[MAX_SET_THM, LESS_SUC, MAX_DEF, MAX_COMM, FINITE_COUNT, - IMAGE_FINITE] -QED - (* Theorem: HALF x <= c ==> f x <= MAX_SET {f x | HALF x <= c} *) (* Proof: Let s = {f x | HALF x <= c} @@ -1822,6 +1789,18 @@ val FINITE_BIJ_PROPERTY = store_thm( val it = |- !s. FINITE s ==> CARD (IMAGE f s) <= CARD s: thm *) +(* Theorem: For a 1-1 map f: s -> s, s and (IMAGE f s) are of the same size. *) +(* Proof: + By finite induction on the set s: + Base case: CARD (IMAGE f {}) = CARD {} + True by IMAGE f {} = {} by IMAGE_EMPTY + Step case: !s. FINITE s /\ (CARD (IMAGE f s) = CARD s) ==> !e. e NOTIN s ==> (CARD (IMAGE f (e INSERT s)) = CARD (e INSERT s)) + CARD (IMAGE f (e INSERT s)) + = CARD (f e INSERT IMAGE f s) by IMAGE_INSERT + = SUC (CARD (IMAGE f s)) by CARD_INSERT: e NOTIN s, f e NOTIN s, for 1-1 map + = SUC (CARD s) by induction hypothesis + = CARD (e INSERT s) by CARD_INSERT: e NOTIN s. +*) Theorem FINITE_CARD_IMAGE: !s f. (!x y. (f x = f y) <=> (x = y)) /\ FINITE s ==> (CARD (IMAGE f s) = CARD s) @@ -3056,21 +3035,6 @@ val PROD_IMAGE_CONG = store_thm( metis_tac[PROD_IMAGE_INSERT, IN_INSERT] ]); -Theorem PROD_IMAGE_CONG[allow_rebind]: - !s f1 f2. (!x. x IN s ==> (f1 x = f2 x)) ==> (PI f1 s = PI f2 s) -Proof - SRW_TAC [][] THEN - REVERSE (Cases_on `FINITE s`) THEN1 ( - SRW_TAC [][PROD_IMAGE_DEF, Once ITSET_def] THEN - SRW_TAC [][Once ITSET_def] - ) THEN - Q.PAT_ASSUM `!x. P` MP_TAC THEN - POP_ASSUM MP_TAC THEN - Q.ID_SPEC_TAC `s` THEN - HO_MATCH_MP_TAC FINITE_INDUCT THEN - METIS_TAC [PROD_IMAGE_THM, DELETE_NON_ELEMENT, IN_INSERT] -QED - (* Theorem: FINITE s ==> !f k. (!x. x IN s ==> (f x = k)) ==> (PI f s = k ** CARD s) *) (* Proof: By finite induction on s. diff --git a/examples/algebra/lib/logPowerScript.sml b/examples/algebra/lib/logPowerScript.sml index 41e8ea9104..9d1ae42b45 100644 --- a/examples/algebra/lib/logPowerScript.sml +++ b/examples/algebra/lib/logPowerScript.sml @@ -102,6 +102,7 @@ open logrootTheory; (* for ROOT *) prime_non_square |- !p. prime p ==> ~square p SQ_SQRT_LT |- !n. ~square n ==> SQRT n * SQRT n < n SQ_SQRT_LT_alt |- !n. ~square n ==> SQRT n ** 2 < n + odd_square_lt |- !n m. ~square n ==> ((2 * m + 1) ** 2 < n <=> m < HALF (1 + SQRT n)) Logarithm: LOG_EXACT_EXP |- !a. 1 < a ==> !n. LOG a (a ** n) = n @@ -259,9 +260,9 @@ open logrootTheory; (* for ROOT *) power_free_upto_1 |- !n. n power_free_upto 1 <=> T power_free_upto_suc |- !n k. 0 < k /\ n power_free_upto k ==> (n power_free_upto k + 1 <=> ROOT (k + 1) n ** (k + 1) <> n) + power_free_check_upto |- !n b. LOG2 n <= b ==> (power_free n <=> 1 < n /\ n power_free_upto b) power_free_check_upto_LOG2 |- !n. power_free n <=> 1 < n /\ n power_free_upto LOG2 n power_free_check_upto_ulog |- !n. power_free n <=> 1 < n /\ n power_free_upto ulog n - power_free_check_upto |- !n b. LOG2 n <= b ==> (power_free n <=> 1 < n /\ n power_free_upto b) power_free_2 |- power_free 2 power_free_3 |- power_free 3 power_free_test_def |- !n. power_free_test n <=> 1 < n /\ n power_free_upto ulog n @@ -1067,6 +1068,38 @@ Proof metis_tac[SQ_SQRT_LT, EXP_2] QED +(* Theorem: ~square n ==> ((2 * m + 1) ** 2 < n <=> m < HALF (1 + SQRT n)) *) +(* Proof: + If part: (2 * m + 1) ** 2 < n ==> m < HALF (1 + SQRT n) + (2 * m + 1) ** 2 < n + ==> 2 * m + 1 <= SQRT n by SQRT_LT, SQRT_OF_SQ + ==> 2 * (m + 1) <= 1 + SQRT n by arithmetic + ==> m < HALF (1 + SQRT n) by X_LT_DIV + Only-if part: m < HALF (1 + SQRT n) ==> (2 * m + 1) ** 2 < n + m < HALF (1 + SQRT n) + <=> 2 * (m + 1) <= 1 + SQRT n by X_LT_DIV + <=> 2 * m + 1 <= SQRT n by arithmetic + <=> (2 * m + 1) ** 2 <= (SQRT n) ** 2 by EXP_EXP_LE_MONO + ==> (2 * m + 1) ** 2 <= n by SQ_SQRT_LE_alt + But n <> (2 * m + 1) ** 2 by ~square n + so (2 * m + 1) ** 2 < n +*) +Theorem odd_square_lt: + !n m. ~square n ==> ((2 * m + 1) ** 2 < n <=> m < HALF (1 + SQRT n)) +Proof + rw[EQ_IMP_THM] >| [ + `2 * m + 1 <= SQRT n` by metis_tac[SQRT_LT, SQRT_OF_SQ] >> + `2 * (m + 1) <= 1 + SQRT n` by decide_tac >> + fs[X_LT_DIV], + `2 * (m + 1) <= 1 + SQRT n` by fs[X_LT_DIV] >> + `2 * m + 1 <= SQRT n` by decide_tac >> + `(2 * m + 1) ** 2 <= (SQRT n) ** 2` by simp[] >> + `(SQRT n) ** 2 <= n` by fs[SQ_SQRT_LE_alt] >> + `n <> (2 * m + 1) ** 2` by metis_tac[square_alt] >> + decide_tac + ] +QED + (* ------------------------------------------------------------------------- *) (* Logarithm *) (* ------------------------------------------------------------------------- *) @@ -1245,15 +1278,9 @@ val LOG2_THM = save_thm("LOG2_THM", LOG_THM |> SPEC ``2`` |> SIMP_RULE (srw_ss())[]); (* val LOG2_THM = |- !n. 0 < n ==> !p. (LOG2 n = p) <=> 2 ** p <= n /\ n < 2 ** SUC p: thm *) -(* Theorem: 0 < n ==> 2 ** LOG2 n <= n /\ n < 2 ** SUC (LOG2 n) *) -(* Proof: - LOG |> SPEC ``2``; - val it = |- !n. 1 < 2 /\ 0 < n ==> 2 ** LOG2 n <= n /\ n < 2 ** SUC (LOG2 n): thm -*) -val LOG2_PROPERTY = store_thm( - "LOG2_PROPERTY", - ``!n. 0 < n ==> 2 ** LOG2 n <= n /\ n < 2 ** SUC (LOG2 n)``, - rw[LOG]); +(* Obtain a theorem *) +Theorem LOG2_PROPERTY = logrootTheory.LOG |> SPEC ``2`` |> SIMP_RULE (srw_ss())[]; +(* val LOG2_PROPERTY = |- !n. 0 < n ==> 2 ** LOG2 n <= n /\ n < 2 ** SUC (LOG2 n): thm *) (* Theorem: 0 < n ==> 2 ** LOG2 n <= n) *) (* Proof: by LOG2_PROPERTY *) diff --git a/examples/algebra/lib/primePowerScript.sml b/examples/algebra/lib/primePowerScript.sml index 2fc2f6350a..fcb25f16be 100644 --- a/examples/algebra/lib/primePowerScript.sml +++ b/examples/algebra/lib/primePowerScript.sml @@ -1301,13 +1301,14 @@ val prime_divisors_finite = store_thm( ``!n. 0 < n ==> FINITE (prime_divisors n)``, metis_tac[prime_divisors_subset_natural, natural_finite, SUBSET_FINITE]); - -(* Note: prime: num -> bool is also a set, so prime = {p | prime p} *) - +(* Theorem: prime_divisors 0 = {p | prime p} *) +(* Proof: by prime_divisors_def, ALL_DIVIDES_0 *) Theorem prime_divisors_0: prime_divisors 0 = {p | prime p} Proof rw[prime_divisors_def] QED +(* Note: prime: num -> bool is also a set, so prime = {p | prime p} *) + (* Theorem: prime_divisors n = {} *) (* Proof: by prime_divisors_def, DIVIDES_ONE, NOT_PRIME_1 *) val prime_divisors_1 = store_thm( diff --git a/examples/algebra/lib/sublistScript.sml b/examples/algebra/lib/sublistScript.sml index 594f876a4a..4963db90e8 100644 --- a/examples/algebra/lib/sublistScript.sml +++ b/examples/algebra/lib/sublistScript.sml @@ -232,6 +232,12 @@ val sublist_length = store_thm( `LENGTH t < LENGTH (h'::t)` by rw[LENGTH_TL_LT] >> decide_tac); +(* Theorem: [Reflexive] p <= p *) +(* Proof: + By induction on p. + Base: [] <= [], true by sublist_nil + Step: p <= p ==> !h. h::p <= h::p, true by sublist_cons +*) val sublist_refl = store_thm( "sublist_refl", ``!p:'a list. p <= p``, @@ -770,6 +776,12 @@ val sublist_prefix_nil = store_thm( metis_tac[] ]); +(* Theorem: [tail append - if] p <= q ==> (p ++ [h]) <= (q ++ [h]) *) +(* Proof: + p <= q + ==> SNOC h p <= SNOC h q by sublist_snoc + ==> (p ++ [h]) <= (q ++ [h]) by SNOC_APPEND +*) Theorem sublist_append_if: !p q h. p <= q ==> (p ++ [h]) <= (q ++ [h]) Proof diff --git a/examples/algebra/lib/triangleScript.sml b/examples/algebra/lib/triangleScript.sml index 83593715da..d8525aafc3 100644 --- a/examples/algebra/lib/triangleScript.sml +++ b/examples/algebra/lib/triangleScript.sml @@ -329,7 +329,6 @@ open relationTheory; (* for RTC *) lcm_run_leibniz_divisor |- !n k. k <= n ==> leibniz n k divides lcm_run (n + 1) lcm_run_lower_odd |- !n. n * 4 ** n <= lcm_run (TWICE n + 1) lcm_run_lower_even |- !n. n * 4 ** n <= lcm_run (TWICE (n + 1)) - lcm_run_lower_better |- !n. 7 <= n ==> 2 ** n <= lcm_run n lcm_run_odd_lower |- !n. ODD n ==> HALF n * HALF (2 ** n) <= lcm_run n lcm_run_even_lower |- !n. EVEN n ==> HALF (n - 2) * HALF (HALF (2 ** n)) <= lcm_run n @@ -4473,22 +4472,6 @@ val lcm_run_divisors = store_thm( `_ = lcm (n + 1) (lcm_run n)` by rw[list_lcm_snoc] >> rw[LCM_DIVISORS]); -(* Theorem: lcm_run n <= lcm_run (n + 1) *) -(* Proof: - Note 0 < lcm_run n by lcm_run_pos - lcm_run (n + 1) - = list_lcm [1 .. (n + 1)] by notation - = list_lcm (SNOC (n + 1) [1 .. n]) by listRangeINC_SNOC, 1 <= n + 1 - = lcm (n + 1) (lcm_run n) by list_lcm_snoc - >= lcm_run n by LCM_LE, 0 < n + 1 -*) -val lcm_run_monotone = store_thm( - "lcm_run_monotone", - ``!n. lcm_run n <= lcm_run (n + 1)``, - rw[lcm_run_pos, listRangeINC_SNOC, list_lcm_snoc, LCM_LE]); - -(* Another proof of same theorem *) - (* Theorem: lcm_run n <= lcm_run (n + 1) *) (* Proof: Note lcm_run n divides lcm_run (n + 1) by lcm_run_divisors @@ -4592,9 +4575,6 @@ val lcm_run_lower_even = store_thm( `2 * (n + 1) = 2 * n + 1 + 1` by decide_tac >> metis_tac[lcm_run_monotone, lcm_run_lower_odd, LESS_EQ_TRANS]); - -(* A very good result, another major theorem. *) - (* Theorem: ODD n ==> (HALF n) * HALF (2 ** n) <= lcm_run n *) (* Proof: Let k = HALF n. @@ -4761,7 +4741,6 @@ val lcm_run_lower_better = store_thm( rw[lcm_run_odd_lower_alt] ]); -(* Another way to prove this result of Nair. *) (* ------------------------------------------------------------------------- *) (* Nair's Trick -- rework *) diff --git a/examples/algebra/polynomial/polyBinomialScript.sml b/examples/algebra/polynomial/polyBinomialScript.sml index e23eea0c73..5753ccd359 100644 --- a/examples/algebra/polynomial/polyBinomialScript.sml +++ b/examples/algebra/polynomial/polyBinomialScript.sml @@ -271,7 +271,7 @@ open ringInstancesTheory; (poly_sum (GENLIST (\j. f j * X ** j) (SUC n)) = GENLIST f (SUC n)) Investigation of Symbolic Polynomial: - poly_binomial_2 |- !r p. Ring r /\ poly p ==> ((p + |1|) ** 2 = p ** 2 + ### 2 * p + |1|) + poly_binomial_2_p |- !r p. Ring r /\ poly p ==> ((p + |1|) ** 2 = p ** 2 + ### 2 * p + |1|) poly_binomial_2_X |- !r. Ring r /\ #1 <> #0 ==> ((X + |1|) ** 2 = X ** 2 + ### 2 * X + |1|) Polynomial Dilation: @@ -1015,31 +1015,6 @@ val poly_genlist = store_thm( ``!r:'a ring. !f. rfun f ==> !n. f n <> #0 ==> poly (GENLIST f (SUC n))``, rw[poly_def_alt, weak_genlist, GENLIST_LAST]); -(* Theorem: !n. plist (GENLIST (\k. f k o X ** k) n) *) -(* Proof: by induction on n. - Base case: plist (GENLIST (\k. f k o (X ** k)) 0) - GENLIST (\k. f k o X ** k) 0 = [] by GENLIST - hence true by weak_of_zero. - Step case: plist (GENLIST (\k. f k o (X ** k)) n) ==> plist (GENLIST (\k. f k o (X ** k)) (SUC n)) - GENLIST (\k. f k o (X ** k)) (SUC n) - = SNOC ((f n) o (X ** n)) (GENLIST (\k. f k o (X ** k)) n) - hence tue by poly_weak_list_SNOC. -*) -val poly_weak_list_genlist = store_thm( - "poly_weak_list_genlist", - ``!r:'a ring. Ring r ==> !f. rfun f ==> !n. plist (GENLIST (\k. (f k) o (X ** k)) n)``, - rpt strip_tac >> - `!x. f x IN R` by metis_tac [ring_fun_def] >> - Induct_on `n` >- - rw[] >> - `GENLIST (\k. f k o (X ** k)) (SUC n) = SNOC ((f n) o (X ** n)) (GENLIST (\k. f k o (X ** k)) n)` by rw_tac std_ss[GENLIST] >> - `poly X` by rw[] >> - `poly (X ** n)` by rw[] >> - `weak ((f n) o (X ** n))` by rw[] >> - rw_tac std_ss[poly_weak_list_SNOC]); - -(* Another proof of the same theorem. *) - (* Theorem: !n. plist (GENLIST (\k. (f k) o (X ** k)) n) *) (* Proof: by induction on n. Base case: plist (GENLIST (\k. f k o (X ** k)) 0) @@ -1508,65 +1483,6 @@ val poly_coeff_factor_exp = store_thm( *) -(* Theorem: [Two-Way Freshman's Theorem] - Ring r /\ #1 <> #0 ==> !c. coprime c (char r) ==> - prime (char r) <=> 1 < (char r) /\ (X + |c|) ** (char r) = X ** (char r) + |c| *) -(* Proof: - Let n = char r. - If (char r) = n = 0, - LHS prime 0 = F by PRIME_POS - RHS 1 < 0 = F hence true by default. - If (char r) = n <> 0, 0 < n. - ##c <> #0 by ring_num_char_coprime_nonzero - poly X by poly_X - poly |c| by poly_sum_num_poly - - If part: to show prime n ==> 1 < n /\ ((X + |c|) ** n = X ** n + |c|) - prime n ==> 1 < n by ONE_LT_PRIME - (X + |c|) ** n - = X ** n + |c| ** n by poly_freshman_thm - = X ** n + |c| by poly_fermat_thm - - Only-if part: to show 1 < n /\ (X + |c|) ** n = X ** n + |c| ==> prime n - Given (X + |c|) ** n = X ** n + |c| - they have equal coefficients: - !k. ((X + |c|) ** n) ' k = (X ** n + |c|) ' k - - !k. k < SUC n ==> (((X + |c|) ** n) ' k = ## (binomial n k) * ##c ** (n - k)) by poly_coeff_X_add_c_exp_n, or - !k. k < SUC n ==> (((X + |c|) ** n) ' k = ## ((binomial n k) * c ** (n - k))) by ring_num_mult_exp - - !k. 0 < k /\ k < n ==> ((X ** n + |c|) ' k = #0 by poly_coeff_X_exp_n_add_c - - Since !k. 0 < k /\ k < n ==> k < SUC n, we have - !k. 0 < k /\ k < n ==> n divides ((binomial n k) * c ** (n - k) by ring_char_divides - - coprime c n ==> !j. coprime (c ** j) n by coprime_exp - hence - !k. 0 < k /\ k < n ==> n divides (binomial n k) by L_EUCLIDES (Euclid's Lemma) - With 1 < n, prime n by prime_iff_divides_binomials -*) -val poly_ring_prime_identity = store_thm( - "poly_ring_prime_identity", - ``!r:'a ring. Ring r /\ #1 <> #0 ==> !c. coprime c (char r) ==> - (prime (char r) <=> 1 < char r /\ ((X + |c|) ** (char r) = X ** (char r) + |c|))``, - rpt strip_tac >> - qabbrev_tac `n = char r` >> - `##c <> #0` by rw[ring_num_char_coprime_nonzero] >> - `##c IN R /\ ( |c| = [##c])` by rw[poly_one_sum_n] >> - rw_tac std_ss[EQ_IMP_THM, ONE_LT_PRIME] >| [ - `poly X` by rw[] >> - `poly |c|` by rw[poly_sum_num_poly] >> - metis_tac [poly_freshman_thm, poly_fermat_thm], - `!k. ((X + |c|) ** n) ' k = (X ** n + |c|) ' k` by rw_tac std_ss[] >> - `!k. 0 < k /\ k < n ==> ((X ** n + |c|) ' k = #0)` by rw[poly_coeff_X_exp_n_add_c] >> - `!k. k < SUC n ==> (((X + |c|) ** n) ' k = ## ((binomial n k) * c ** (n - k)))` - by metis_tac[poly_coeff_X_add_c_exp_n, ring_num_mult_exp] >> - `!k. 0 < k /\ k < n ==> k < SUC n` by decide_tac >> - metis_tac [ring_char_divides, coprime_exp, L_EUCLIDES, MULT_COMM, prime_iff_divides_binomials] - ]); - -(* Better version *) - (* Theorem: [Two-Way Freshman's Theorem] Ring r ==> !c. coprime c (char r) ==> prime (char r) <=> 1 < (char r) /\ (X + |c|) ** (char r) = X ** (char r) + |c| *) @@ -3206,21 +3122,21 @@ but that is not used now as we have above: poly_sum_gen_is_genlist = p ** 2 + ###2 * p + |1| ** 2 by poly_mult_rone = p ** 2 + ###2 * p + |1| by poly_one_exp *) -val poly_binomial_2 = store_thm( - "poly_binomial_2", +val poly_binomial_2_p = store_thm( + "poly_binomial_2_p", ``!(r:'a ring) p. Ring r /\ poly p ==> ((p + |1|) ** 2 = p ** 2 + ###2 * p + |1|)``, rw[poly_add_mult_ring, ring_binomial_2, GSYM poly_ring_property]); (* Theorem: Ring r /\ #1 <> #0 ==> (X + |1|) ** 2 = X ** 2 + ###2 * X + |1| *) -(* Proof: by poly_binomial_2, poly_X. *) +(* Proof: by poly_binomial_2_p, poly_X. *) val poly_binomial_2_X = store_thm( "poly_binomial_2_X", ``!r:'a ring. Ring r /\ #1 <> #0 ==> ((X + |1|) ** 2 = X ** 2 + ###2 * X + |1|)``, - rw_tac std_ss[poly_binomial_2, poly_X]); + rw_tac std_ss[poly_binomial_2_p, poly_X]); (* -Surely, poly_binomial_2 ==> poly_binomial_2_X -But how to show: poly_binomial_2_X ==> poly_binomial_2, in General? +Surely, poly_binomial_2_p ==> poly_binomial_2_X +But how to show: poly_binomial_2_X ==> poly_binomial_2_p, in General? Something like: P |X| ==> !x. poly x ==> P x ? This old investigation is solved in this proper script. *) diff --git a/examples/algebra/polynomial/polyCyclicScript.sml b/examples/algebra/polynomial/polyCyclicScript.sml index b6ee981fc3..7a51625790 100644 --- a/examples/algebra/polynomial/polyCyclicScript.sml +++ b/examples/algebra/polynomial/polyCyclicScript.sml @@ -779,7 +779,7 @@ val poly_cyclic_cofactor = store_thm( or ~((cyclic n) % (X - |1|) = |0|) by poly_factor_one Since pmonic (X - |1|), by poly_pmonic_X_sub_c and poly (cyclic n) by poly_cyclic_poly - hence ~ ((X - |1|) pdivides (cyclic n)) by poly_ulead_divides_alt + hence ~ ((X - |1|) pdivides (cyclic n)) by poly_divides_alt *) val poly_cyclic_has_no_factor_unity_1 = store_thm( "poly_cyclic_has_no_factor_unity_1", @@ -794,7 +794,7 @@ val poly_cyclic_has_no_factor_unity_1 = store_thm( `~((cyclic n) % (unity 1) = |0|)` by metis_tac[poly_factor_one, poly_unity_1] >> `pmonic (unity 1)` by rw_tac std_ss[poly_unity_pmonic, DECIDE ``0 < 1``] >> `poly (cyclic n)` by rw[poly_cyclic_poly] >> - metis_tac[poly_ulead_divides_alt]); + metis_tac[poly_divides_alt]); (* Theorem: Field r ==> !n. 1 < n ==> ?h. ipoly h /\ h pdivides (cyclic n) *) (* Proof: diff --git a/examples/algebra/polynomial/polyDividesScript.sml b/examples/algebra/polynomial/polyDividesScript.sml index b9d299ac6a..62d8260047 100644 --- a/examples/algebra/polynomial/polyDividesScript.sml +++ b/examples/algebra/polynomial/polyDividesScript.sml @@ -102,8 +102,6 @@ open dividesTheory; poly_divides_one |- !r. Ring r ==> !p. poly p /\ p pdivides |1| <=> upoly p poly_monic_divides_deg_le |- !r. Ring r /\ #1 <> #0 ==> !p q. monic p /\ monic q /\ p pdivides q ==> deg p <= deg q - poly_divides_mod_zero |- !r. Ring r ==> !p q. poly p /\ ulead q ==> (q pdivides p <=> (p % q = |0|)) - poly_ulead_divides_alt |- !r. Ring r ==> !p q. ulead p /\ poly q ==> (p pdivides q <=> (q % p = |0|)) poly_divides_alt |- !r. Ring r ==> !p q. ulead p /\ poly q ==> (p pdivides q <=> (q % p = |0|)) poly_divides_pmod_eq_zero |- !r. Ring r ==> !p q. ulead p /\ poly q ==> (p pdivides q <=> (q == |0|) (pm p)) poly_divides_eqn |- !r. Ring r ==> !p q. ulead p /\ poly q ==> (p pdivides q <=> (q = q / p * p)) @@ -636,72 +634,6 @@ val poly_monic_divides_deg_le = store_thm( `deg (s * p) = deg s + deg p` by rw[poly_monic_deg_mult] >> decide_tac); -(* Theorem: !p q. poly p /\ ulead q ==> (q pdivides p <=> (p % q = |0|)) *) -(* Proof: - If deg q = 0, - Then p % q = |0| by poly_mod_by_const - and p = (p / q) * q + p % q by poly_division_all - = (p / q) * q by poly_add_rzero - and poly (p / q) by poly_div_poly - so q pdivides p by poly_divides_def - - Otherwise, 0 < deg q. - If part: q pdivides p ==> p % q = |0| - Note q pdivides p - ==> ?s. poly s /\ (p = s * q) by poly_divides_def - ==> p = s * q + |0| by poly_add_rzero - and deg |0| = 0 < deg q by poly_deg_zero, by pmonic q - Thus p % q = |0| by poly_mod_unique, 0 < deg q - Only-if part: p % q = |0| ==> q pdivides p - Note p = (p / q) * q + (p % q) by poly_division, 0 < deg q - or p = (p / q) * q by poly_add_rzero, p % q = |0| - with poly (p / q) by poly_div_poly - so q pdivides p by poly_divides_def -*) -val poly_divides_mod_zero = store_thm( - "poly_divides_mod_zero", - ``!r:'a ring. Ring r ==> !p q. poly p /\ ulead q ==> (q pdivides p <=> (p % q = |0|))``, - rpt strip_tac >> - Cases_on `deg q = 0` >| [ - `p % q = |0|` by rw[poly_mod_by_const] >> - `p = (p / q) * q + p % q` by rw[poly_division_all] >> - `_ = (p / q) * q` by rw[] >> - metis_tac[poly_divides_def, poly_div_poly], - `0 < deg q` by decide_tac >> - rw_tac std_ss[EQ_IMP_THM] >| [ - `?s. poly s /\ (p = s * q)` by rw[GSYM poly_divides_def] >> - `_ = s * q + |0|` by rw[] >> - `poly |0| /\ (deg |0| = 0)` by rw[] >> - metis_tac[poly_mod_unique], - `p = (p / q) * q + (p % q)` by rw[poly_division] >> - `_ = (p / q) * q` by rw[] >> - metis_tac[poly_divides_def, poly_div_poly] - ] - ]); - -(* Another proof of the same theorem, with p, q interchanged. *) - -(* Theorem: !p q. ulead p /\ poly q ==> p pdivides q <=> q % p = |0| *) -(* Proof: - If part: p pdivides q ==> q % p = |0| - Note p pdivides q - ==> ?s. poly s /\ (q = s * p) by poly_divides_def - ==> q % p = (s * p) % p = |0| by poly_mod_multiple, ulead p - Only-if part: q % p = |0| ==> p pdivides q - Note q % p = |0| - ==> ?t. poly t /\ (q = t * p) by poly_mod_eq_zero, ulead p - ==> p pdivides q by poly_divides_def -*) -val poly_ulead_divides_alt = store_thm( - "poly_ulead_divides_alt", - ``!r:'a ring. Ring r ==> !p q. ulead p /\ poly q ==> (p pdivides q <=> (q % p = |0|))``, - rw_tac std_ss[poly_divides_def] >> - rw_tac std_ss[EQ_IMP_THM] >- - rw[poly_mod_multiple] >> - rw[GSYM poly_mod_eq_zero]); - -(* Third proof of the same theorem. *) - (* Theorem: ulead p /\ poly q ==> (p pdivides q <=> q % p = |0|) *) (* Proof: p pdivides q @@ -727,7 +659,7 @@ val poly_divides_pmod_eq_zero = store_thm( (* Theorem: Ring r ==> !p q. ulead p /\ poly q ==> (p pdivides q <=> (q = (q / p) * p)) *) (* Proof: p pdivides q - <=> (q % p = |0|) by poly_divides_mod_zero + <=> (q % p = |0|) by poly_divides_alt <=> (q / p * p + (q % p) = q / p * p + |0|) by poly_add_lcancel <=> (q = q / p * p + |0|) by poly_div_mod_all_def <=> (q = q / p * p) by poly_add_rzero @@ -737,7 +669,7 @@ val poly_divides_eqn = store_thm( ``!r:'a ring. Ring r ==> !p q. ulead p /\ poly q ==> (p pdivides q <=> (q = (q / p) * p))``, rpt strip_tac >> `poly (q / p) /\ (q = q / p * p + (q % p))` by rw[poly_div_mod_all_def] >> - `p pdivides q <=> (q % p = |0|)` by rw[poly_divides_mod_zero] >> + `p pdivides q <=> (q % p = |0|)` by rw[poly_divides_alt] >> `_ = (q / p * p + (q % p) = q / p * p + |0|)` by rw[poly_add_lcancel] >> `_ = (q = q / p * p)` by metis_tac[poly_mult_poly, poly_add_rzero] >> rw[]); @@ -748,7 +680,7 @@ val poly_divides_eqn = store_thm( Thus x % q = ((x / p * p) % q + (x % p) % q) % q by poly_mod_add = (((x / p) % q) * (p % q)) % q + (x % p) % q) % q by poly_mod_mult - = (((x / p) % q) * |0|) % q + (x % p) % q) % q by poly_divides_mod_zero + = (((x / p) % q) * |0|) % q + (x % p) % q) % q by poly_divides_alt = ( |0| % q + (x % p) % q) % q by poly_mult_zero = |0| + ((x % p) % q) % q by poly_zero_mod = x % p % q by poly_mod_mod @@ -760,7 +692,7 @@ val poly_divides_mod_mod = store_thm( rpt strip_tac >> `x = x / p * p + x % p` by rw[poly_division_all] >> `((x / p) * p) % q = (((x / p) % q) * (p % q)) % q` by rw[Once poly_mod_mult] >> - `_ = |0|` by metis_tac[poly_divides_mod_zero, poly_mult_zero, poly_zero_mod] >> + `_ = |0|` by metis_tac[poly_divides_alt, poly_mult_zero, poly_zero_mod] >> qabbrev_tac `m = x / p * p` >> qabbrev_tac `y = x % p` >> `poly m /\ poly y` by rw[Abbr`m`, Abbr`y`] >> @@ -1061,27 +993,6 @@ val poly_field_divides_deg_le = store_thm( `p <> |0|` by metis_tac[poly_zero_divides] >> rw[poly_divides_deg_le, poly_field_poly_ulead]); -(* Original proof of the same theorem *) - -(* Theorem: Field r ==> poly p /\ poly q /\ q <> |0| /\ p pdivides q ==> deg p <= deg q *) -(* Proof: - Since p pdivides q, - ?t. poly t /\ (q = t * p) by poly_divides_def - Now q <> |0| ==> p <> |0| by poly_mult_rzero - ==> t <> |0| by poly_mult_lzero - Hence deg q = deg t + deg p by poly_deg_mult_nonzero - or deg p <= deq q by LESS_EQ_ADD -*) -val poly_field_divides_deg_le = store_thm( - "poly_field_divides_deg_le", - ``!r:'a field. Field r ==> - !p q. poly p /\ poly q /\ q <> |0| /\ p pdivides q ==> deg p <= deg q``, - rpt strip_tac >> - `?t. poly t /\ (q = t * p)` by rw[GSYM poly_divides_def] >> - `p <> |0| /\ t <> |0|` by metis_tac[poly_mult_zero] >> - `deg q = deg t + deg p` by rw[poly_deg_mult_nonzero] >> - rw[]); - (* Theorem: p pdivides q ==> !x. x IN R /\ root p x ==> root q x *) (* Proof: p pdivides q @@ -1228,42 +1139,6 @@ val poly_field_divides_cmult_iff = store_thm( !c. c IN R /\ c <> #0 ==> (p pdivides c * q <=> p pdivides q)``, rw[poly_divides_cmult_iff, field_nonzero_unit, GSYM field_nonzero_eq]); -(* Original proof of the same theorem *) - -(* Theorem: Field r ==> !p q. poly p /\ poly q ==> - !c. c IN R /\ c <> #0 ==> (p pdivides c * q <=> p pdivides q) *) -(* Proof: - If part: p pdivides c * q ==> p pdivides q - Note ?t. poly t /\ (c * q = t * p) by poly_divides_def - But c IN R+ by field_nonzero_eq - ==> |/ c IN R by field_inv_element - q = ( |/c * c) * q by field_mult_linv, poly_cmult_lone - = |/ c * (c * q) by poly_cmult_cmult - = |/ c * (t * p) by above - = ( |/ c * t) * p by poly_cmult_mult - Note poly ( |/ c * t) by poly_cmult_poly - Thus p pdivides q by poly_divides_def - Only-if part: p pdivides q ==> p pdivides c * q - This is true by poly_divides_cmult -*) -val poly_field_divides_cmult_iff = store_thm( - "poly_field_divides_cmult_iff", - ``!r:'a field. Field r ==> !p q. poly p /\ poly q ==> - !c. c IN R /\ c <> #0 ==> (p pdivides c * q <=> p pdivides q)``, - rpt strip_tac >> - `Ring r` by rw[] >> - rw[EQ_IMP_THM] >| [ - `?t. poly t /\ (c * q = t * p)` by rw[GSYM poly_divides_def] >> - `c IN R+` by rw[field_nonzero_eq] >> - `|/ c IN R` by rw[field_inv_element] >> - `q = ( |/c * c) * q` by rw[] >> - `_ = |/ c * (c * q)` by rw[poly_cmult_cmult] >> - `_ = |/ c * (t * p)` by rw[] >> - `_ = ( |/ c * t) * p` by rw[poly_cmult_mult] >> - metis_tac[poly_divides_def, poly_cmult_poly], - rw[poly_divides_cmult] - ]); - (* Theorem: poly p ==> !n. 0 < n ==> p pdivides (p ** n) *) (* Proof: Since 0 < n, ?m. n = SUC m by num_CASES @@ -1333,36 +1208,6 @@ val poly_field_const_divides = store_thm( ``!r:'a field. Field r ==> !c. c IN R /\ c <> #0 ==> !p. poly p ==> [c] pdivides p``, rw[poly_const_divides, field_nonzero_unit, GSYM field_nonzero_eq]); -(* Original proof of the same theorem. *) - -(* Theorem: Field r ==> !c. c IN R /\ c <> #0 ==> !p. poly p ==> [c] pdivides p *) -(* Proof: - By poly_divides_def, this is to show: - ?s. poly s /\ (p = s * [c]) - Since c IN R /\ c <> #0, - |/ c IN R /\ |/ c <> #0 by field_inv_element, field_inv_nonzero - Let s = |/ c * p - Then poly s by poly_cmult_poly - and s * [c] - = ( |/ c * p) * [c] - = p * ( |/c * [c]) by poly_mult_cmult - = p * ([|/c * c]) by poly_cmult_const_nonzero - = p * |1| by field_mult_linv - = p by poly_mult_rone -*) -val poly_field_const_divides = store_thm( - "poly_field_const_divides", - ``!r:'a field. Field r ==> !c. c IN R /\ c <> #0 ==> !p. poly p ==> [c] pdivides p``, - rw[poly_divides_def] >> - `|/ c IN R /\ |/ c <> #0` by metis_tac[field_inv_element, field_inv_nonzero, field_nonzero_eq] >> - qexists_tac `|/ c * p` >> - rw_tac std_ss[poly_cmult_poly, field_is_ring] >> - `( |/ c * p) * [c] = p * ( |/c * [c])` by rw[poly_mult_cmult] >> - `_ = p * ([|/ c * c])` by rw[poly_cmult_const_nonzero, field_nonzero_eq] >> - `_ = p * [#1]` by rw[field_mult_linv, field_nonzero_eq] >> - `_ = p * |1|` by metis_tac[poly_one, field_one_ne_zero] >> - rw[]); - (* Theorem: Ring r ==> !p q. poly p /\ poly q /\ p pdivides q ==> !c. unit c ==> (c * p) pdivides q *) (* Proof: @@ -1408,39 +1253,6 @@ val poly_field_cmult_divides = store_thm( !c. c IN R /\ c <> #0 ==> (c * p) pdivides q``, rw[poly_cmult_divides, field_nonzero_unit, GSYM field_nonzero_eq]); -(* Original proof of the same theorem. *) - -(* Theorem: Field r ==> !p q. poly p /\ poly q /\ p pdivides q ==> - !c. c IN R /\ c <> #0 ==> (c * p) pdivides q *) -(* Proof: - Since p pdivides q, - ==> ?s. poly s /\ (q = s * p) by poly_divides_def - Since c <> #0, c IN R+ by field_nonzero_eq - thus |/ c * c = #1 by field_mult_linv - q = #1 * q by poly_cmult_lone - = ( |/ c * c) * (s * p) by above - = |/ c * (c * (s * p)) by poly_cmult_cmult - = |/ c * (c * s * p) by poly_cmult_mult - = |/ c * (s * (c * p)) by poly_mult_cmult - = ( |/ c * s) * (c * p) by poly_cmult_mult - Since poly ( |/ c * s) by poly_cmult_poly - Hence (c * p) pdivides q by poly_divides_def -*) -val poly_field_cmult_divides = store_thm( - "poly_field_cmult_divides", - ``!r:'a field. Field r ==> !p q. poly p /\ poly q /\ p pdivides q ==> - !c. c IN R /\ c <> #0 ==> (c * p) pdivides q``, - rpt strip_tac >> - `?s. poly s /\ (q = s * p)` by rw[GSYM poly_divides_def] >> - `c IN R+ /\ ( |/ c * c = #1)` by rw[field_nonzero_eq, field_mult_linv] >> - `|/ c IN R /\ poly ( |/ c * s)` by rw[field_inv_element] >> - `q = ( |/ c * c) * (s * p)` by rw[] >> - `_ = |/ c * (c * (s * p))` by rw[poly_cmult_cmult] >> - `_ = |/ c * (c * s * p)` by rw[poly_cmult_mult] >> - `_ = |/ c * (s * (c * p))` by metis_tac[poly_mult_cmult, field_is_ring] >> - `_ = ( |/ c * s) * (c * p)` by rw[poly_cmult_mult] >> - metis_tac[poly_divides_def]); - (* Theorem: Field r ==> !p q. poly p /\ poly q /\ (p * q) pdivides q ==> (q = |0|) \/ (upoly p) *) (* Proof: Since (p * q) pdivides q @@ -2259,18 +2071,6 @@ val poly_field_const_unit = store_thm( ``!r:'a field. Field r ==> !h. h IN R /\ h <> #0 ==> upoly [h]``, rw[poly_field_units]); -(* Theorem: Field r /\ poly p ==> upoly p <=> ?c. c IN R /\ c <> #0 /\ p = [c] *) -(* Proof: - upoly <=> p <> |0| /\ (deg p = 0) by poly_field_units - <=> ?c. c IN R /\ c <> #0 /\ p = [c] by poly_deg_eq_0 -*) -val poly_field_unit_alt = store_thm( - "poly_field_unit_alt", - ``!r:'a field. Field r ==> !p. poly p ==> (upoly p <=> ?c. c IN R /\ c <> #0 /\ (p = [c]))``, - rw[poly_field_units, poly_deg_eq_0]); - -(* A better version of the above theorem *) - (* Theorem: Field r ==> !p. upoly p <=> ?c. c IN R /\ c <> #0 /\ (p = [c]) *) (* Proof: upoly p <=> p IN (Invertibles (PolyRing r).prod).carrier by overload diff --git a/examples/algebra/polynomial/polyDivisionScript.sml b/examples/algebra/polynomial/polyDivisionScript.sml index 8f6006eb2c..426fabd8ef 100644 --- a/examples/algebra/polynomial/polyDivisionScript.sml +++ b/examples/algebra/polynomial/polyDivisionScript.sml @@ -961,23 +961,6 @@ val poly_mod_add_assoc = store_thm( `_ = (p + (q + t) % z) % z` by rw_tac std_ss[poly_mod_add, poly_mod_mod] >> rw[]); -(* Theorem: (p - q) % z = (p % z - q % z) % z *) -(* Proof: - (p - q) % z - = (p + -q) % z by poly_sub_def - = (p % z + (-q) % z) % z by poly_mod_add - = (p % z + - (q % z)) % z by poly_mod_neg - = (p % z - q % z) % z by poly_sub_def -*) -val poly_mod_sub = store_thm( - "poly_mod_sub", - ``!r:'a ring. Ring r ==> !p q z. poly p /\ poly q /\ ulead z ==> ((p - q) % z = (p % z - q % z) % z)``, - rw[] >> - `poly (p % z) /\ poly (q % z) /\ poly (-q)` by rw[] >> - metis_tac[poly_mod_add, poly_mod_neg]); - -(* Another proof of same result. *) - (* Theorem: (p - q) % z = (p % z - q % z) % z *) (* Proof: (p - q) % z @@ -989,7 +972,7 @@ val poly_mod_sub = store_thm( val poly_mod_sub = store_thm( "poly_mod_sub", ``!r:'a ring. Ring r ==> !p q z. poly p /\ poly q /\ ulead z ==> - ((p - q) % z = (p % z - q % z) % z)``, + ((p - q) % z = (p % z - q % z) % z)``, rw[poly_sub_def, poly_mod_add, poly_mod_neg]); (* Theorem: (p * q) % z = (p % z * q % z) % z *) diff --git a/examples/algebra/polynomial/polyFieldModuloScript.sml b/examples/algebra/polynomial/polyFieldModuloScript.sml index 6e686f6d39..05d84bcbf6 100644 --- a/examples/algebra/polynomial/polyFieldModuloScript.sml +++ b/examples/algebra/polynomial/polyFieldModuloScript.sml @@ -831,12 +831,12 @@ val poly_field_mod_prime_product = store_thm( rw_tac std_ss[poly_mod_prime_product, poly_field_poly_ulead, field_is_ring]); (* Theorem: (pprime z <=> !x y. poly x /\ poly y /\ z pdivides (x * y) ==> z pdivides x \/ z pdivides y) *) -(* Proof: by poly_mod_prime_product, poly_ulead_divides_alt. *) +(* Proof: by poly_mod_prime_product, poly_divides_alt. *) val poly_prime_divides = store_thm( "poly_prime_divides", ``!r:'a ring z. Ring r /\ ulead z ==> (pprime z <=> !x y. poly x /\ poly y /\ z pdivides (x * y) ==> z pdivides x \/ z pdivides y)``, - metis_tac[poly_mod_prime_product, poly_ulead_divides_alt, poly_mult_poly]); + metis_tac[poly_mod_prime_product, poly_divides_alt, poly_mult_poly]); (* Theorem: poly t /\ pprime t /\ t pdivides (p * q) ==> (t pdivides p) \/ (t pdivides q) *) (* Proof: by ring_prime_def, poly_divides_is_ring_divides. *) @@ -1702,39 +1702,6 @@ val poly_mod_irreducible_finite_field = store_thm( rw[poly_mod_irreducible_field] >> rw[poly_mod_ring_finite, poly_irreducible_pmonic, FiniteRing_def]); -(* Another proof, not based on inverse. *) - -(* Theorem: FiniteField r ==> !p. ipoly p ==> FiniteField (PolyModRing r p) *) -(* Proof: - Note unit (lead p) /\ 0 < deg p by poly_irreducible_pmonic - By finite_field_from_finite_ring, this is to show: - (1) (PolyModRing r p).prod.id <> (PolyModRing r p).sum.id - That is to show: |1| <> |0| by poly_mod_ring_property, deg p <> 0 - This is true by poly_one_ne_poly_zero - (2) FiniteRing (PolyModRing r p) - Note FiniteField (PolyModRing r p) by poly_mod_irreducible_finite_field - ==> FiniteRing (PolyModRing r p) by finite_field_is_finite_ring - (3) After simplifying by poly_mod_ring_property, - poly x /\ poly y /\ deg x < deg p /\ deg y < deg p ==> - ((x * y) % p = |0|) <=> (x = |0|) \/ (y = |0|) - Note unit (lead p) by poly_irreducible_pmonic - ==> x % p = x and y % p = y by poly_mod_less, - Thus (x = |0|) \/ (y = |0|) by poly_mod_mult_eq_zero -*) -val poly_mod_irreducible_finite_field = store_thm( - "poly_mod_irreducible_finite_field", - ``!r:'a field. FiniteField r ==> !p. ipoly p ==> FiniteField (PolyModRing r p)``, - rpt (stripDup[FiniteField_def]) >> - `pmonic p` by rw[poly_irreducible_pmonic] >> - `deg p <> 0` by decide_tac >> - (REVERSE (irule finite_field_from_finite_ring >> rpt conj_tac)) >| [ - `|1| <> |0|` by rw[poly_one_ne_poly_zero] >> - rw_tac std_ss[poly_mod_ring_property], - rw_tac std_ss[poly_mod_irreducible_finite_field, finite_field_is_finite_ring], - rw_tac std_ss[poly_mod_ring_property] >> - metis_tac[poly_mod_mult_eq_zero, poly_mod_less, field_is_ring] - ]); - (* Theorem: FiniteField r /\ ipoly z ==> (CARD Rz = CARD R ** deg z) *) (* Proof: FiniteField r ==> Field r /\ FINITE R by FiniteField_def @@ -3777,91 +3744,6 @@ val poly_mod_eval_lift_by_poly_eval_lift = store_thm( (* Another version with evalz (lift p) (q % z) rather than evalz (lift p) q *) -(* Theorem: Ring r /\ pmonic z ==> !p q. poly p /\ poly q ==> - (evalz (lift p) (q % z) = poly_eval (PolyRing r) (lift p) q % z) *) -(* Proof: - First, #0z = |0| by poly_mod_ring_property - By induction on p. - Base case: poly [] ==> (evalz (lift []) (q % z) = poly_eval (PolyRing r) (lift []) q % z) - LHS = evalz (lift []) (q % z) - = evalz [] (q % z) by poly_lift_of_zero - = #0z by poly_eval_of_zero - = |0| by poly_mod_ring_property - RHS = poly_eval (PolyRing r) (lift []) q % z - = poly_eval (PolyRing r) [] q % z by poly_lift_of_zero - = (PolyRing r).sum.id % z by poly_eval_of_zero - = |0| % z by poly_ring_property - = |0| = LHS by poly_zero_mod - Step case: !h. poly (h::p) ==> (evalz (lift (h::p)) (q % z) = poly_eval (PolyRing r) (lift (h::p)) q % z) - poly (h::p) ==> h IN R /\ poly p by poly_cons_poly - lift (h::p) = (if h = #0 then |0| else [h])::lift p by poly_lift_cons - - Let t = poly_eval (PolyRing r) (lift p) q - The induction hypothesis is: evalz (lift p) (q % z) = t % z - and (t % z) *z (q % z) - = ((t % z) * (q % z)) % z by poly_mod_ring_property - = (t * q) % z by poly_mod_mult - - If h = #0, - LHS = evalz (lift (#0::p)) (q % z - = evalz ( |0|::lift p) (q % z) by poly_lift_cons - = |0| +z ((evalz (lift p) (q % z)) *z (q % z)) by poly_eval_cons - = |0| +z ((t % z) *z (q % z)) by induction hypothesis - = |0| +z ((t * q) % z) by above - = ( |0| + (t * q) % z) % z by poly_mod_ring_property - = ( |0| % z + (t * q) % z) % z by poly_zero_mod - = ( |0| + t * q) % z by poly_mod_add - RHS = poly_eval (PolyRing r) (lift (#0::p)) q % z - = poly_eval (PolyRing r) ( |0|::lift p) q % z by poly_lift_cons - = ( |0| + poly_eval (PolyRing r) (lift p) q * q) % z by poly_eval_cons - = ( |0| + t * q) % z by t above - = LHS - - If h <> #0, - LHS = evalz (lift (h::p)) (q % z) - = evalz ([h]::lift p) (q % z) by poly_lift_cons - = [h] +z ((evalz (lift p) (q % z)) *z (q % z)) by poly_eval_cons - = [h] +z ((t % z) *z (q % z)) by induction hypothesis - = [h] +z ((t * q) % z) by above - = ([h] + (t * q) % z) % z by poly_mod_ring_property - = ([h] % z + (t * q) % z) % z by poly_mod_const - = ([h] + t * q) % z by poly_mod_add - RHS = poly_eval (PolyRing r) (lift (h::p)) q % z - = poly_eval (PolyRing r) ([h]::lift p) q % z by poly_lift_cons - = ([h] + poly_eval (PolyRing r) (lift p) q * q) % z by poly_eval_cons - = ([h] + t * q) % z by t above - = LHS -*) -val poly_mod_eval_lift_by_poly_eval_lift_alt = store_thm( - "poly_mod_eval_lift_by_poly_eval_lift_alt", - ``!r:'a ring z. Ring r /\ pmonic z ==> !p q. poly p /\ poly q ==> - (evalz (lift p) (q % z) = poly_eval (PolyRing r) (lift p) q % z)``, - rpt strip_tac >> - `#0z = |0|` by rw[poly_mod_ring_ids] >> - Induct_on `p` >- - rw_tac std_ss[poly_lift_of_zero, poly_eval_of_zero, poly_zero_mod] >> - rw_tac std_ss[poly_cons_poly] >> - qabbrev_tac `t = poly_eval (PolyRing r) (lift p) q` >> - `poly t` by rw[poly_eval_lift_poly_poly, Abbr`t`] >> - `poly (t % z) /\ deg (t % z) < deg z` by rw[poly_deg_mod_less] >> - `poly (q % z) /\ deg (q % z) < deg z` by rw[poly_deg_mod_less] >> - `poly (t * q) /\ poly ((t * q) % z) /\ deg ((t * q) % z) < deg z` by rw[poly_deg_mod_less] >> - `(t % z) *z (q % z) = (t * q) % z` by rw[poly_mod_ring_property, poly_mod_mult] >> - rw_tac std_ss[poly_eval_cons, poly_mod_ring_property, poly_lift_cons] >| [ - rw_tac std_ss[GSYM poly_mod_mult] >> - `poly |0| /\ deg |0| < deg z` by rw[] >> - `|0| +z (t * q) % z = ( |0| + (t * q) % z) % z` by rw[poly_mod_ring_property] >> - `_ = ( |0| % z + (t * q) % z) % z` by rw[poly_zero_mod] >> - rw_tac std_ss[poly_mod_add], - rw_tac std_ss[GSYM poly_mod_mult] >> - `poly [h] /\ deg [h] < deg z` by rw[] >> - `[h] +z (t * q) % z = ([h] + (t * q) % z) % z` by rw[poly_mod_ring_property] >> - `_ = ([h] % z + (t * q) % z) % z` by rw[poly_mod_const] >> - rw_tac std_ss[poly_mod_add] - ]); - -(* Another proof of the same result. *) - (* poly_mod_eval_lift_by_poly_eval_lift; val it = |- !r z. Ring r /\ pmonic z ==> !p q. poly p /\ poly q /\ deg q < deg z ==> @@ -3910,26 +3792,6 @@ val poly_mod_lift_root_by_mod_peval = store_thm( (* Another version with q % z rather than q *) -(* Theorem: Ring r ==> !p q z. poly p /\ poly q /\ pmonic z ==> - (rootz (lift p) (q % z) <=> (peval p q % z = |0|)) *) -(* Proof: - rootz (lift p) (q % z) - <=> evalz (lift p) (q % z) = |0| by poly_root_def - <=> poly_eval (PolyRing r) (lift p) q % z = |0| by poly_mod_eval_lift_by_poly_eval_lift_alt - <=> (peval p q) % z = |0| by poly_peval_alt -*) -val poly_mod_lift_root_by_mod_peval_alt = store_thm( - "poly_mod_lift_root_by_mod_peval_alt", - ``!r:'a ring z. Ring r /\ pmonic z ==> !p q. poly p /\ poly q ==> - (rootz (lift p) (q % z) <=> (peval p q % z = |0|))``, - rpt strip_tac >> - `|0| = #0z` by rw[poly_mod_ring_ids] >> - `rootz (lift p) (q % z) <=> (evalz (lift p) (q % z) = |0|)` by rw[GSYM poly_root_def] >> - `_ = ((poly_eval (PolyRing r) (lift p) q) % z = |0|)` by rw[poly_mod_eval_lift_by_poly_eval_lift_alt] >> - rw[GSYM poly_peval_alt]); - -(* Another proof of the same result. *) - (* poly_mod_lift_root_by_mod_peval; val it = |- !r z. Ring r /\ pmonic z ==> !p q. poly p /\ poly q /\ deg q < deg z ==> diff --git a/examples/algebra/polynomial/polyGCDScript.sml b/examples/algebra/polynomial/polyGCDScript.sml index 9a179651af..4ae838f84c 100644 --- a/examples/algebra/polynomial/polyGCDScript.sml +++ b/examples/algebra/polynomial/polyGCDScript.sml @@ -1023,71 +1023,6 @@ val poly_unity_gcd_identity = store_thm( ] ]); -(* Theorem: Field r ==> !n m. (unity n) pdivides (unity m) <=> n divides m *) -(* Proof: - If n = 0, - Then X ** n - |1| = |1| - |1| = |0| by poly_exp_0 - so X ** m - |1| = |0| by poly_zero_divides - Giving X ** m = |1| by poly_sub_eq_zero - thus m = 0 by poly_X_exp_eq_one - and 0 divides 0 by ZERO_DIVIDES - - If n <> 0, 0 < n. - If part: (X ** n - |1|) pdivides (X ** m - |1|) ==> n divides m - (X ** n - |1|) pdivides (X ** m - |1|) - <=> pgcd (X ** n - |1|) (X ** m - |1|) ~~ (X ** n - |1|) by poly_divides_iff_gcd_fix - But pgcd (X ** n - |1|) (X ** m - |1|) ~~ X ** (gcd n m) - |1| by poly_unity_gcd_identity - Hence X ** n - |1| ~~ X ** (gcd n m) - |1| by poly_unit_eq_sym, poly_unit_eq_trans - Note gcd n m <> 0 since n <> 0 by GCD_EQ_0 - Since monic (X ** n - |1|) by poly_monic_X_exp_n_sub_c, 0 < n - and monic (X ** (gcd n m) - |1|) by poly_monic_X_exp_n_sub_c, 0 < gcd n m - so X ** n - |1| = X ** (gcd n m) - |1| by poly_unit_eq_monic_eq - Thus X ** n = X ** (gcd n m) by poly_sub_add - Giving n = gcd n m by poly_X_exp_eq, #1 <> #0 - or n divides m by divides_iff_gcd_fix - Only-if part: n divides m ==> (X ** n - |1|) pdivides (X ** m - |1|) - Since n divides m ==> gcd n m = n by divides_iff_gcd_fix - Hence pgcd (X ** n - |1|) (X ** m - |1|) - ~~ X ** (gcd n m) - |1| by poly_unity_gcd_identity - = X ** n - |1| by above - or (X ** n - |1|) pdivides (X ** m - |1|) by poly_divides_iff_gcd_fix -*) -val poly_unity_divisibility = store_thm( - "poly_unity_divisibility", - ``!r:'a field. Field r ==> !n m. (unity n) pdivides (unity m) <=> n divides m``, - rpt strip_tac >> - `Ring r /\ #1 <> #0` by rw[] >> - `poly X /\ !k. poly (X ** k) /\ poly (X ** k - |1|)` by rw[] >> - Cases_on `n = 0` >| [ - rw_tac std_ss[poly_exp_0, poly_sub_eq, poly_one_poly, EQ_IMP_THM] >| [ - `X ** m - |1| = |0|` by rw[GSYM poly_zero_divides] >> - `X ** m = |1|` by metis_tac[poly_sub_eq_zero, poly_one_poly] >> - metis_tac[poly_X_exp_eq_one, ZERO_DIVIDES], - `m = 0` by rw[GSYM ZERO_DIVIDES] >> - `X ** m - |1| = |0|` by rw[poly_exp_0, poly_sub_eq] >> - rw[poly_zero_divides] - ], - rw_tac std_ss[EQ_IMP_THM] >| [ - `gcd n m <> 0` by rw[GCD_EQ_0] >> - `0 < n /\ 0 < gcd n m` by decide_tac >> - `pgcd (X ** n - |1|) (X ** m - |1|) ~~ (X ** n - |1|)` by rw[GSYM poly_divides_iff_gcd_fix] >> - `pgcd (X ** n - |1|) (X ** m - |1|) ~~ X ** (gcd n m) - |1|` by rw[poly_unity_gcd_identity] >> - `X ** n - |1| ~~ X ** (gcd n m) - |1|` by metis_tac[poly_unit_eq_sym, poly_unit_eq_trans, poly_gcd_poly] >> - `|1| = ###1` by rw[poly_ring_sum_1] >> - `monic (X ** n - |1|)` by metis_tac[poly_monic_X_exp_n_sub_c] >> - `monic (X ** (gcd n m) - |1|)` by metis_tac[poly_monic_X_exp_n_sub_c] >> - `X ** n - |1| = X ** (gcd n m) - |1|` by metis_tac[poly_unit_eq_monic_eq] >> - `X ** n = X ** (gcd n m)` by metis_tac[poly_sub_add, poly_one_poly] >> - `n = gcd n m` by metis_tac[poly_X_exp_eq] >> - rw[divides_iff_gcd_fix], - `n = gcd n m` by rw[GSYM divides_iff_gcd_fix] >> - `pgcd (X ** n - |1|) (X ** m - |1|) ~~ X ** n - |1|` by metis_tac[poly_unity_gcd_identity] >> - rw[poly_divides_iff_gcd_fix] - ] - ]); - -(* This is a direct proof, relaxing to Ring r /\ #1 <> #0 *) - (* Theorem: Ring r /\ #1 <> #0 ==> !n m. (unity n) pdivides (unity m) <=> n divides m *) (* Proof: If part: X ** n - |1| pdivides X ** m - |1| ==> n divides m diff --git a/examples/algebra/polynomial/polyMapScript.sml b/examples/algebra/polynomial/polyMapScript.sml index 95a72b1897..09bde3e943 100644 --- a/examples/algebra/polynomial/polyMapScript.sml +++ b/examples/algebra/polynomial/polyMapScript.sml @@ -589,29 +589,6 @@ val poly_deg_map = store_thm( (* Ring Homomorphism *) (* ------------------------------------------------------------------------- *) -(* Theorem: (r ~r~ r_) f ==> !p. zerop p ==> zerop_ p_ *) -(* Proof: - Note f #0 = #0_ by ring_homo_zero - Now zerop p - <=> EVERY (\c. c = #0) p by zero_poly_every_zero - ==> EVERY (\c. c = #0_) p_ by EVERY_MONOTONIC_MAP - <=> zerop_ p_ by zero_poly_every_zero -*) -val ring_homo_zero_poly = store_thm( - "ring_homo_zero_poly", - ``!(r:'a ring) (r_:'b ring) f. (r ~r~ r_) f ==> !p. zerop p ==> zerop_ p_``, - rpt strip_tac >> - `f #0 = #0_` by rw[ring_homo_zero] >> - `EVERY (\c. c = #0) p` by rw[GSYM zero_poly_every_zero] >> - `!x. (\c. c = #0) x ==> ((\c. c = #0_) o f) x` by rw[] >> - qabbrev_tac `P = \c. c = #0` >> - qabbrev_tac `Q = \c. c = #0_` >> - `EVERY Q p_` by metis_tac[EVERY_MONOTONIC_MAP] >> - `EVERY (\c. c = #0_) p_` by rw[] >> - rw[zero_poly_every_zero]); - -(* Induction proof of previous theorem *) - (* Theorem: (r ~r~ r_) f ==> !p. zerop p ==> zerop_ p_ *) (* Proof: By induction on p. @@ -636,61 +613,6 @@ val ring_homo_zero_poly = store_thm( Induct_on `p` >> rw[]); -(* Theorem: (r ~r~ r_) f /\ INJ f R R_ ==> !p. weak p ==> (zerop p <=> zerop_ p_) *) -(* Proof: - If part: zerop p ==> zerop_ p_ - True by ring_homo_zero_poly. - Only-if part: zerop_ p_ ==> zerop p - Note f #0 = #0_ by ring_homo_zero - zerop_ p_ - ==> EVERY (\x. x = #0_) p_ by zero_poly_every_zero - ==> EVERY (\x. f x = #0_) p by EVERY_MAP - ==> EVERY (\x. f x = f #0) p by ring_homo_zero, [1] - Also weak p - ==> EVERY (\x. x IN R) p by weak_def_alt, [2] - - By contradiction, suppose ~zerop p. - ~zerop p - ==> ~(EVERY (\x. x = #0) p) by zero_poly_every_zero - ==> EXISTS ($~ o (\x. x = #0)) p by NOT_EVERY - ==> ?x. MEM x p /\ x <> #0 by EXISTS_MEM [3] - Since MEM x p, - ==> x IN R by EVERY_MEM and [2] - ==> f x = f #0 by EVERY_MEM and [1] - But #0 IN R by ring_zero_element - so f x <> f #0 by INJ_DEF and [3] - This contradicts f x = f #0. -*) -val ring_homo_eq_zero_poly = store_thm( - "ring_homo_eq_zero_poly", - ``!(r:'a ring) (r_:'b ring) f. (r ~r~ r_) f /\ INJ f R R_ ==> !p. weak p ==> (zerop p <=> zerop_ p_)``, - rw[EQ_IMP_THM] >- - metis_tac[ring_homo_zero_poly] >> - `EVERY (\x. x = #0_) p_` by rw[GSYM zero_poly_every_zero] >> - qabbrev_tac `P = \x. x = #0_` >> - qabbrev_tac `Q = \x. f x = #0_` >> - `(\x. P (f x)) = Q` by rw[Abbr`P`, Abbr`Q`] >> - `EVERY (\x. P (f x)) p` by metis_tac[EVERY_MAP] >> - `EVERY Q p` by rw[] >> - `EVERY (\x. f x = #0_) p` by rw[Abbr`Q`] >> - `EVERY (\x. f x = f #0) p` by metis_tac[ring_homo_zero] >> - `EVERY (\x. x IN R) p` by rw[GSYM weak_def_alt] >> - spose_not_then strip_assume_tac >> - `~(EVERY (\x. x = #0) p)` by metis_tac[zero_poly_every_zero] >> - qabbrev_tac `PP = (\x. x = #0)` >> - `EXISTS ($~ o PP) p` by metis_tac[NOT_EVERY] >> - `!x. ($~ o PP) x <=> (x <> #0)` by rw[Abbr`PP`] >> - `?x. MEM x p /\ x <> #0` by metis_tac[EXISTS_MEM] >> - qabbrev_tac `QQ = \x. x IN R` >> - `QQ x` by metis_tac[EVERY_MEM] >> - `x IN R` by fs[Abbr`QQ`] >> - qabbrev_tac `PQ = (\x. f x = f #0)` >> - `PQ x` by metis_tac[EVERY_MEM] >> - `f x = f #0` by fs[Abbr`PQ`] >> - metis_tac[INJ_DEF, ring_zero_element]); - -(* An inductive proof of the previous result. *) - (* Theorem: (r ~r~ r_) f /\ INJ f R R_ ==> !p. weak p ==> (zerop p <=> zerop_ p_) *) (* Proof: By induction on p. @@ -718,26 +640,6 @@ val ring_homo_eq_zero_poly = store_thm( rw[] >> metis_tac[ring_homo_eq_zero]); -(* Theorem: RingHomo f r r_ ==> !p. weak p ==> weak_ p_ *) -(* Proof: - Note !x. x IN R ==> f x IN R_ by ring_homo_element - weak p - <=> EVERY (\x. x IN R) p by weak_def_alt - ==> EVERY (\x. f x IN R_) p_ by EVERY_MONOTONIC_MAP - <=> weak_ p_ by weak_def_alt -*) -val ring_homo_weak = store_thm( - "ring_homo_weak", - ``!(r:'a ring) (r_:'b ring) f. RingHomo f r r_ ==> !p. weak p ==> weak_ p_``, - rw[weak_def_alt] >> - `!x. x IN R ==> f x IN R_` by metis_tac[ring_homo_element] >> - qabbrev_tac `P = \x. x IN R` >> - qabbrev_tac `Q = \x. x IN R_` >> - `!x. P x ==> (Q o f) x` by rw[Abbr`P`, Abbr`Q`] >> - metis_tac[EVERY_MONOTONIC_MAP]); - -(* An induction proof of the same theorem. *) - (* Theorem: RingHomo f r r_ ==> !p. weak p ==> weak_ p_ *) (* Proof: By induction on p. @@ -965,56 +867,6 @@ val ring_homo_poly_chop_of_chop = store_thm( metis_tac[ring_homo_zero_poly] >> metis_tac[zero_poly_eq_zero_poly_chop]); -(* Theorem: (r ~r~ r_) f ==> !p q. weak p /\ weak q ==> (MAP f (p || q) = p_ ||_ q_) *) -(* Proof: - By induction on p. - Base: !q. weak [] /\ weak q ==> (MAP f ([] || q) = MAP f [] ||_ q_) - LHS = MAP f ([] || q) - = MAP f q by weak_add_of_lzero - RHS = (MAP f []) ||_ q_ - = [] ||_ q_ by MAP - = q_ by weak_add_of_lzero - Step: !q. weak p /\ weak q ==> (MAP f (p || q) = p_ ||_ q_) ==> - !h. weak (h::p) /\ weak q ==> (MAP f ((h::p) || q) = MAP f (h::p) ||_ q_) - By induction on q. - Base: weak [] ==> (MAP f ((h::p) || []) = MAP f (h::p) ||_ MAP f []) - LHS = MAP f ((h::p) || []) - = MAP f (h::p) by weak_add_of_rzero - RHS = (MAP f (h::p)) ||_ (MAP f []) - = (MAP f (h::p)) ||_ [] by MAP - = (MAP f (h::p) by weak_add_of_rzero - Step: !q. weak p /\ weak q ==> (MAP f (p || q) = p_ ||_ q_) ==> - !h'. weak (h'::q) ==> (MAP f ((h::p) || (h'::q)) = MAP f (h::p) ||_ MAP f (h'::q)) - Note weak (h::p) ==> h IN R /\ weak p by weak_cons - and weak (h'::q) ==> h' IN R /\ weak q by weak_cons - MAP f ((h::p) || (h'::q)) - = MAP f (h + h' :: (p || q)) by weak_add_cons - = f (h + h') :: MAP f (p || q) by MAP - = f (h + h') :: p_ ||_ q_ by induction hypothesis - = (f h) +_ (f h') :: p_ ||_ q_ by ring_homo_property - = (f h:: p_) ||_ (f h':: q_) by weak_add_cons - = MAP f (h::p) ||_ MAP f (h'::q) by MAP -*) -val ring_homo_weak_add = store_thm( - "ring_homo_weak_add", - ``!(r:'a ring) (r_:'b ring) f. (r ~r~ r_) f ==> !p q. weak p /\ weak q ==> (MAP f (p || q) = p_ ||_ q_)``, - ntac 4 strip_tac >> - Induct_on `p` >- - rw[] >> - rw_tac std_ss[weak_cons] >> - Induct_on `q` >- - rw[] >> - rw_tac std_ss[weak_cons] >> - `MAP f ((h::p) || (h'::q)) = MAP f (h + h' :: (p || q))` by rw_tac std_ss[weak_add_cons] >> - `_ = f (h + h') :: MAP f (p || q)` by rw_tac std_ss[MAP] >> - `_ = f (h + h') :: p_ ||_ q_` by rw[] >> - `_ = (f h) +_ (f h') :: p_ ||_ q_` by rw[ring_homo_property] >> - `_ = (f h:: p_) ||_ (f h':: q_)` by rw_tac std_ss[weak_add_cons] >> - `_ = MAP f (h::p) ||_ MAP f (h'::q)` by rw_tac std_ss[MAP] >> - rw[]); - -(* Short proof of the same theorem. *) - (* Theorem: (r ~r~ r_) f ==> !p q. weak p /\ weak q ==> (MAP f (p || q) = p_ ||_ q_) *) (* Proof: By induction on p. diff --git a/examples/algebra/polynomial/polyModuloRingScript.sml b/examples/algebra/polynomial/polyModuloRingScript.sml index 5e02e8dda4..7b0d151dc1 100644 --- a/examples/algebra/polynomial/polyModuloRingScript.sml +++ b/examples/algebra/polynomial/polyModuloRingScript.sml @@ -1276,13 +1276,6 @@ val poly_field_ideal_cogen_property = store_thm("poly_field_ideal_cogen_property (coset (PolyRing r).sum p (principal_ideal (PolyRing r) z).carrier)) ==> (p == q) (pm z))``, rw[poly_ideal_cogen_property]); -val poly_field_mod_ring_homo_quotient_ring = store_thm("poly_field_mod_ring_homo_quotient_ring", - ``!r:'a field. Field r ==> !z. poly z /\ z <> |0| ==> - RingHomo (\x. coset (PolyRing r).sum x (principal_ideal (PolyRing r) z).carrier) - (PolyModRing r z) - (quotient_ring (PolyRing r) (principal_ideal (PolyRing r) z))``, - rw[poly_mod_ring_homo_quotient_ring]); - val poly_field_mod_sum_group_homo_quotient_ring = store_thm("poly_field_mod_sum_group_homo_quotient_ring", ``!r:'a field. Field r ==> !z. poly z /\ z <> |0| ==> GroupHomo (\x. coset (PolyRing r).sum x (principal_ideal (PolyRing r) z).carrier) diff --git a/examples/algebra/polynomial/polyMonicScript.sml b/examples/algebra/polynomial/polyMonicScript.sml index e53d240fd8..b90b9ba029 100644 --- a/examples/algebra/polynomial/polyMonicScript.sml +++ b/examples/algebra/polynomial/polyMonicScript.sml @@ -935,17 +935,6 @@ val poly_deg_X = store_thm( ``!r:'a ring. Ring r /\ #1 <> #0 ==> (deg X = 1)``, rw[]); -(* Theorem: lead X = #1 *) -(* Proof: by poly_X_def. *) -val poly_lead_X = store_thm( - "poly_lead_X", - ``!r:'a ring. Ring r /\ #1 <> #0 ==> (lead X = #1)``, - rw[]); - -(* better than: above poly_lead_X - |- !r. Ring r /\ #1 <> #0 ==> (lead X = #1) -*) - (* Theorem: lead X = #1 *) (* Proof: lead X diff --git a/examples/algebra/polynomial/polyProductScript.sml b/examples/algebra/polynomial/polyProductScript.sml index 645f0a02ef..f59227e4ca 100644 --- a/examples/algebra/polynomial/polyProductScript.sml +++ b/examples/algebra/polynomial/polyProductScript.sml @@ -508,21 +508,6 @@ val poly_prod_set_mult_eqn = store_thm( (* Theorem: Ring r ==> !p. poly p ==> (PPROD {p} = p) *) (* Proof: - Since Monoid (PolyRing r).prod by poly_mult_monoid - and p IN (PolyRing r).carrier by poly_ring_element - so GPROD_SET (PolyRing r).prod {p} = p by GPROD_SET_SING - or PPROD {p} = p by poly_prod_set_def -*) -val poly_prod_set_sing = store_thm( - "poly_prod_set_sing", - ``!r:'a ring. Ring r ==> !p. poly p ==> (PPROD {p} = p)``, - rw[poly_prod_set_def, poly_mult_monoid, GPROD_SET_SING, poly_ring_element]); - -(* Better proof of above theorem *) - -(* Theorem: Ring r ==> !p. poly p ==> (PPROD {p} = p) *) -(* Proof: - Or, Since FINITE {} by FINITE_EMPTY and pset {} by NOT_IN_EMPTY diff --git a/examples/algebra/polynomial/polyRingScript.sml b/examples/algebra/polynomial/polyRingScript.sml index 065be0a0df..967c6176d9 100644 --- a/examples/algebra/polynomial/polyRingScript.sml +++ b/examples/algebra/polynomial/polyRingScript.sml @@ -1136,23 +1136,6 @@ val poly_mult_one = store_thm( ``!r:'a ring. Ring r ==> !p. poly p ==> ( |1| * p = p) /\ (p * |1| = p)``, rw[]); -(* first try: *) -val poly_mult_one = save_thm("poly_mult_one", CONJ poly_mult_lone poly_mult_rone); -(* > val poly_mult_one = |- (!r. Ring r ==> !p. poly p ==> ( |1| * p = p)) /\ !r. Ring r ==> !p. poly p ==> (p * |1| = p) : thm *) - -(* better, but not the best: *) -val poly_mult_one = save_thm("poly_mult_one", - CONJ (poly_mult_lone |> SPEC_ALL |> UNDISCH |> SPEC_ALL) - (poly_mult_rone |> SPEC_ALL |> UNDISCH |> SPEC_ALL) |> GEN ``p:'a poly`` |> DISCH_ALL |> GEN_ALL); -(* > val poly_mult_one = |- !r. Ring r ==> !p. (poly p ==> ( |1| * p = p)) /\ (poly p ==> (p * |1| = p)) : thm *) - -(* the best: *) -val poly_mult_one = save_thm("poly_mult_one", - CONJ (poly_mult_lone |> SPEC_ALL |> UNDISCH |> SPEC_ALL |> UNDISCH) - (poly_mult_rone |> SPEC_ALL |> UNDISCH |> SPEC_ALL |> UNDISCH) - |> DISCH ``poly p`` |> GEN ``p:'a poly`` |> DISCH_ALL |> GEN_ALL); -(* > val poly_mult_one = |- !r. Ring r ==> !p. poly p ==> ( |1| * p = p) /\ (p * |1| = p) : thm *) - (* To show closure for Monoid (PolyRing r).prod. *) (* Theorem: poly p /\ poly q ==> poly (p * q) *) @@ -1374,21 +1357,27 @@ val poly_mult_one_one = lift_ring_thm "mult_one_one" "mult_one_one"; val _ = export_rewrites ["poly_mult_one_one"]; -(* Theorem: Ring r ==> ( |1| = |0| <=> !p. poly p ==> p = |0| *) -val poly_one_eq_zero = lift_ring_thm "one_eq_zero" "one_eq_zero"; -(* > val poly_one_eq_zero = |- !r. Ring r ==> (( |1| = |0|) <=> ((PolyRing r).carrier = {|0|})) : thm *) +(* Theorem: Ring r ==> ( |1| = |0| <=> !p. poly p ==> p = |0| *) (* Proof: - by above poly_one_eq_zero, and improve by ONE_ELEMENT_SING and IN_SING. + val poly_one_eq_zero = lift_ring_thm "one_eq_zero" "one_eq_zero"; + > val poly_one_eq_zero = |- !r. Ring r ==> (( |1| = |0|) <=> ((PolyRing r).carrier = {|0|})) : thm + by above and improve: + If part: |1| = |0| <=> !p. poly p ==> p = |0| + (PolyRing r).carrier = {|0|}) + <=> !p. poly p ==> p = |0| by poly_ring_property, IN_SING + Only-if part: !p. poly p ==> p = |0| ==> |1| = |0| + Put p = |1| and note that poly |1| = T by poly_one_poly *) -val poly_one_eq_zero = store_thm( - "poly_one_eq_zero", - ``!r:'a ring. Ring r ==> (( |1| = |0|) <=> !p. poly p ==> (p = |0|))``, - rw_tac std_ss[EQ_IMP_THM] >| [ - `(PolyRing r).carrier = { |0| }` by rw_tac std_ss[GSYM poly_one_eq_zero] >> - metis_tac [poly_ring_property, IN_SING], - `(PolyRing r).carrier = { |0| }` by metis_tac [poly_ring_property, poly_zero_poly, MEMBER_NOT_EMPTY, ONE_ELEMENT_SING] >> - metis_tac [poly_one_eq_zero] - ]); +(* Need rebind as lift_ring_thm stores the name poly_one_eq_zero. *) +Theorem poly_one_eq_zero[allow_rebind]: + !r:'a ring. Ring r ==> (( |1| = |0|) <=> !p. poly p ==> (p = |0|)) +Proof + rpt strip_tac >> + assume_tac (lift_ring_thm "one_eq_zero" "one_eq_zero") >> + rw_tac std_ss[EQ_IMP_THM] >- + metis_tac[poly_ring_property, IN_SING] >> + metis_tac[poly_one_poly] +QED (* Theorem: Ring r ==> ( |0| = |1|) <=> (#0 = #1) *) (* Proof: @@ -2577,14 +2566,6 @@ val poly_mult_cmult = store_thm( Hence (- p) * q = - (p * q) by poly_add_eq_zero *) -val poly_mult_lneg = store_thm( - "poly_mult_lneg", - ``!r:'a ring. Ring r ==> !p q. poly p /\ poly q ==> ((- p) * q = - (p * q))``, - rpt strip_tac >> - `poly (-p)` by rw[] >> - `poly (-p * q) /\ poly (p * q)` by rw[] >> - `(-p) * q + (p * q) = (- p + p) * q` by rw_tac std_ss[poly_mult_ladd] >> - rw_tac std_ss[GSYM poly_add_eq_zero, poly_add_lneg, poly_mult_lzero]); (* better by lifting *) val poly_mult_lneg = lift_ring_thm_with_goal "mult_lneg" "mult_lneg" ``!r:'a ring. Ring r ==> !p q. poly p /\ poly q ==> ((- p) * q = - (p * q))``; @@ -2599,10 +2580,6 @@ val poly_mult_lneg = lift_ring_thm_with_goal "mult_lneg" "mult_lneg" = - (q * p) by poly_mult_lneg = - (p * q) by poly_mult_comm *) -val poly_mult_rneg = store_thm( - "poly_mult_rneg", - ``!r:'a ring. Ring r ==> !p q. poly p /\ poly q ==> (p * (- q) = - (p * q))``, - metis_tac[poly_mult_lneg, poly_mult_comm, poly_neg_poly]); (* better by lifting *) val poly_mult_rneg = lift_ring_thm_with_goal "mult_rneg" "mult_rneg" ``!r:'a ring. Ring r ==> !p q. poly p /\ poly q ==> (p * (- q) = - (p * q))``; @@ -2619,10 +2596,6 @@ val _ = export_rewrites ["poly_mult_lneg", "poly_mult_rneg"]; Hence -(p * q) = -p * q by ring_neg_mult and -(p * q) = p * -q by ring_neg_mult *) -val poly_neg_mult = store_thm( - "poly_neg_mult", - ``!r:'a ring. Ring r ==> !p q. poly p /\ poly q ==> (-(p * q) = -p * q) /\ (-(p * q) = p * -q)``, - metis_tac[poly_add_mult_ring, poly_ring_element, ring_neg_mult]); (* better by lifting *) val poly_neg_mult = lift_ring_thm_with_goal "neg_mult" "neg_mult" ``!r:'a ring. Ring r ==> !p q. poly p /\ poly q ==> (-(p * q) = -p * q) /\ (-(p * q) = p * -q)``; @@ -2632,10 +2605,6 @@ val poly_neg_mult = lift_ring_thm_with_goal "neg_mult" "neg_mult" (* Theorem: Ring r ==> !p q. poly p /\ poly q ==> (-p * -q = p * q) *) (* Proof: by poly_ring_ring, ring_mult_neg_neg *) -val poly_mult_neg_neg = store_thm( - "poly_mult_neg_neg", - ``!r:'a ring. Ring r ==> !p q. poly p /\ poly q ==> (-p * -q = p * q)``, - metis_tac[poly_ring_ring, ring_mult_neg_neg, poly_ring_element]); (* better by lifting *) val poly_mult_neg_neg = lift_ring_thm_with_goal "mult_neg_neg" "mult_neg_neg" ``!r:'a ring. Ring r ==> !p q. poly p /\ poly q ==> (-p * -q = p * q)``; @@ -3770,8 +3739,6 @@ val poly_exp_add = store_thm( metis_tac[poly_add_mult_ring, ring_exp_add, poly_ring_property]); (* Theorem: Ring r /\ poly p ==> !m n. (p ** (n * m) = (p ** n) ** m) *) -val poly_exp_mult = lift_ring_thm "exp_mult" "exp_mult" |> REWRITE_RULE[poly_ring_element]; -(* > val poly_exp_mult = |- !r. Ring r ==> !x. poly x ==> !n k. x ** (n * k) = (x ** n) ** k: thm *) val poly_exp_mult = lift_ring_thm_with_goal "exp_mult" "exp_mult" ``!r:'a ring. Ring r ==> !p. poly p ==> !m n. p ** (n * m) = (p ** n) ** m``; (* > val poly_exp_mult = |- !r. Ring r ==> !p. poly p ==> !m n. p ** (n * m) = (p ** n) ** m : thm *) @@ -3783,8 +3750,6 @@ val poly_exp_mult = lift_ring_thm_with_goal "exp_mult" "exp_mult" = p ** (n * m) by MULT_COMM = (p ** n) ** m by poly_exp_mult *) -val poly_exp_mult_comm = lift_ring_thm "exp_mult_comm" "exp_mult_comm" |> REWRITE_RULE[poly_ring_element]; -(* > val poly_exp_mult_comm = |- !r. Ring r ==> !x. poly x ==> !m n. (x ** m) ** n = (x ** n) ** m: thm *) val poly_exp_mult_comm = lift_ring_thm_with_goal "exp_mult_comm" "exp_mult_comm" ``!r:'a ring. Ring r ==> !p. poly p ==> !m n. (p ** m) ** n = (p ** n) ** m``; (* > val poly_exp_mult_comm = |- !r. Ring r ==> !p. poly p ==> !m n. (p ** m) ** n = (p ** n) ** m: thm *) @@ -4987,36 +4952,6 @@ val poly_cmult_unit = store_thm( `_ = p` by rw[] >> simp[]); -(* Theorem: Ring r /\ poly p /\ c IN R /\ unit c ==> (p = (( |/c) * p) * [c]) *) -(* Proof: - If #1 = #0, - Then |1| = |0| by poly_one_eq_poly_zero - so p = |0| by poly_one_eq_zero - and (( |/c) * p) * [c] - = |0| * [c] by poly_cmult_zero - = |0| = p by poly_mult_lzero - Otherwise #1 <> #0, - Note |/c IN R by ring_unit_inv_element - and c <> #0 by ring_unit_nonzero, #1 <> #0 - so poly [c] by poly_nonzero_element_poly - Thus p = [c] * (( |/c) * p) by poly_cmult_unit - = (( |/c) * p) * [c] by poly_mult_comm -*) -val poly_cmult_unit_comm = store_thm( - "poly_cmult_unit_comm", - ``!r:'a ring p c. Ring r /\ poly p /\ c IN R /\ unit c ==> (p = (( |/c) * p) * [c])``, - rpt strip_tac >> - Cases_on `#1 = #0` >| [ - `|1| = |0|` by rw[poly_one_eq_poly_zero] >> - `p = |0|` by metis_tac[poly_one_eq_zero] >> - metis_tac[poly_cmult_zero, poly_mult_lzero], - `|/c IN R /\ c <> #0` by rw[ring_unit_inv_element, ring_unit_nonzero] >> - `poly [c]` by rw[poly_nonzero_element_poly] >> - metis_tac[poly_cmult_unit, poly_mult_comm, poly_cmult_poly] - ]); - -(* Another proof of the same theorem *) - (* Theorem: Ring r /\ poly p /\ c IN R /\ unit c ==> (p = (( |/c) * p) * [c]) *) (* Proof: Note |/c IN R by ring_unit_inv_element diff --git a/examples/algebra/polynomial/polyRootScript.sml b/examples/algebra/polynomial/polyRootScript.sml index eeb4c40d53..7502e90429 100644 --- a/examples/algebra/polynomial/polyRootScript.sml +++ b/examples/algebra/polynomial/polyRootScript.sml @@ -900,20 +900,6 @@ val poly_roots_factor = save_thm("poly_roots_factor", poly_factor_roots); val poly_roots_factor = |- !r. Ring r ==> !c. c IN R ==> (roots (factor c) = {c}): thm *) -(* Theorem: Ring r ==> !c. c IN R ==> (roots (factor c) = {c}) *) -(* Proof: - !x. x IN roots (factor c) - <=> root (factor c) x by poly_roots_def, or poly_roots_member - <=> eval (factor c) x = #0 by poly_root_def - <=> x - c = #0 by poly_factor_eval - <=> x = c by ring_sub_eq_zero -*) -val poly_roots_factor = store_thm( - "poly_roots_factor", - ``!r:'a ring. Ring r ==> !c. c IN R ==> (roots (factor c) = {c})``, - rw[poly_roots_def, poly_root_def, EXTENSION] >> - metis_tac[poly_factor_eval, ring_sub_eq_zero]); - (* Example: In Z_6, (x - 2)(x - 3) = x^2 - 5x + 0 = x^2 - 5x = x(x - 5) so roots (x - 2)(x - 3) = {2, 3, 0, 5} @@ -965,29 +951,6 @@ val poly_roots_X = store_thm( rw[poly_roots_def, poly_root_def, EXTENSION] >> metis_tac[poly_eval_X, ring_zero_element]); -(* Theorem: roots (p * q) = roots p UNION roots q *) -(* Proof: by p * q = |0| iff p = |0| or q = |0|. - !x. x IN roots (p * q) - <=> root (p * q) x by poly_roots_member - <=> (p * q)(x) = #0 by poly_root_def - <=> p(x) * q(x) = #0 by poly_eval_mult - <=> p(x) = #0 or q(x) = #0 by field_zero_product - <=> root p x or root q x by poly_root_def - <=> x IN roots p or x IN roots q by poly_roots_member - <=> x IN (roots p UNION roots q) by IN_UNION -*) -val poly_roots_mult = store_thm( - "poly_roots_mult", - ``!r:'a field. Field r ==> !p q. poly p /\ poly q ==> (roots (p * q) = roots p UNION roots q)``, - rw_tac std_ss[poly_roots_member, poly_root_def, EXTENSION, GSPECIFICATION, IN_UNION, EQ_IMP_THM] >- - rw_tac std_ss[GSYM field_zero_product, poly_eval_element, GSYM poly_eval_mult, field_is_ring] >- - rw_tac std_ss[] >- - rw_tac std_ss[field_mult_lzero, poly_eval_element, poly_eval_mult, field_is_ring] >- - rw_tac std_ss[] >> - rw_tac std_ss[field_mult_rzero, poly_eval_element, poly_eval_mult, field_is_ring]); - -(* A better proof of the same result. *) - (* Theorem: roots (p * q) = roots p UNION roots q *) (* Proof: by p * q = |0| iff p = |0| or q = |0|. !x. x IN roots (p * q) @@ -1005,8 +968,7 @@ val poly_roots_mult = store_thm( rpt strip_tac >> `Ring r /\ #1 <> #0` by rw[] >> rw[poly_roots_member, poly_root_def, EXTENSION, EQ_IMP_THM] >- - rw[GSYM field_zero_product, GSYM poly_eval_mult] >> - rw[]); + rw[GSYM field_zero_product, GSYM poly_eval_mult] >> rw[]); (* Theorem: Field r ==> !p n. poly p /\ 0 < n ==> (roots (p ** n) = roots p) *) (* Proof: diff --git a/examples/algebra/polynomial/polyWeakScript.sml b/examples/algebra/polynomial/polyWeakScript.sml index abfbfc4765..900f5f7d18 100644 --- a/examples/algebra/polynomial/polyWeakScript.sml +++ b/examples/algebra/polynomial/polyWeakScript.sml @@ -3289,6 +3289,8 @@ val weak_mult_ladd = store_thm( val _ = export_rewrites ["weak_mult_radd", "weak_mult_ladd"]; +(* Theorem: p o (q || t) = p o q || p o t /\ (p || q) o t = p o t || q o t *) +(* Proof: by weak_mult_radd and weak_mult_ladd. *) Theorem weak_mult_add = CONJ (weak_mult_radd |> SPEC_ALL |> UNDISCH_ALL |> SPEC_ALL |> UNDISCH_ALL) (weak_mult_ladd |> SPEC_ALL |> UNDISCH_ALL |> SPEC_ALL |> UNDISCH_ALL) @@ -4619,38 +4621,6 @@ val poly_deg_weak_eq_zero = store_thm( `!n. PRE (SUC n) = n` by decide_tac >> metis_tac[poly_deg_def, weak_cons, LENGTH, LENGTH_NIL, list_CASES, poly_zero]); -(* Theorem: deg (neg p) = deg p *) -(* Proof: by induction on p, the lists are of the same length. - Base: weak [] ==> (deg (neg []) = deg []) - true since -[] = [] by weak_neg_of_zero. - Step: weak p ==> (deg (neg p) = deg p) ==> !h. weak (h::p) ==> (deg (neg (h::p)) = deg (h::p)) - If p = [], deg - [h] = deg [-h] = 0 = deg [h], by poly_deg_const - If P <> [], - deg (neg (h::p)) - = PRE (LENGTH(-h::neg p)) by poly_deg_def, weak_neg_def - = PRE (SUC (LENGTH(neg p)) by LENGTH definition - = SUC (PRE (LENGTH(neg p)) by 0 < LENGTH p - = SUC (deg (neg p)) by poly_deg_def if p <> [] - = SUC (deg p) by induction hypothesis - = SUC (PRE (LENGTH p)) - = PRE (SUC (LENGTH p)) - = PRE (LENGTH (h::p)) - = deg (h::p) -*) -val poly_deg_weak_neg = store_thm( - "poly_deg_weak_neg", - ``!r:'a ring. Ring r ==> !p. weak p ==> (deg (neg p) = deg p)``, - strip_tac >> - strip_tac >> - Induct >- - rw[] >> - rw_tac std_ss[weak_cons, weak_neg_cons] >> - Cases_on `p = []` >> - rw[weak_neg_eq_of_zero, poly_deg_cons]); -(* Q: why the last rw[weak_neg_eq_of_zero, poly_deg_cons] when poly_deg_cons is exported? *) - -(* Try to prove using bijection of list, or list MAP. *) - (* Theorem: deg (neg p) = deg p *) (* Proof: due to lists are of the same length. If p = [], deg (neg []) = deg [] @@ -4660,7 +4630,7 @@ val poly_deg_weak_neg = store_thm( deg (neg (h::t)) = LENGTH (-t) By weak_neg_map and LENGTH_MAP, they are equal. *) -Theorem poly_deg_weak_neg[allow_rebind]: +Theorem poly_deg_weak_neg: !r:'a ring. Ring r ==> !p. weak p ==> (deg (neg p) = deg p) Proof metis_tac[poly_deg_cons_length, weak_neg_map, LENGTH_MAP, diff --git a/examples/algebra/ring/ringMapScript.sml b/examples/algebra/ring/ringMapScript.sml index e81bb3686f..904b00a76d 100644 --- a/examples/algebra/ring/ringMapScript.sml +++ b/examples/algebra/ring/ringMapScript.sml @@ -1557,16 +1557,14 @@ val subring_unit_inv_nonzero = store_thm( (* Theorem: s <= r ==> !x. Unit s x ==> (Inv s x = |/ x) *) (* Proof: - Let z = Inv s x. - Note x IN s.carrier by ring_unit_element - and z IN s.carrier by ring_unit_inv_element - Thus x IN R /\ z IN R by subring_element - Also unit x by subring_unit - x * z - = s.prod.op x z by subring_mult - = s.prod.id by ring_unit_rinv - = #1 by subring_one - Hence z = |/x by ring_unit_rinv_unique + Note s <= r ==> RingHomo I s r by subring_def + Thus |/ (I x) = I (Inv s x) by ring_homo_unit_inv + or |/ x = Inv s x by I_THM + +> ring_homo_unit_inv |> ISPEC ``s:'a ring`` |> ISPEC ``r:'a ring``; +val it = |- !f. (s ~r~ r) f ==> !x. Unit s x ==> |/ (f x) = f (Inv s x): thm +> ring_homo_inv |> ISPEC ``s:'a ring`` |> ISPEC ``r:'a ring``; +val it = |- !f. (s ~r~ r) f ==> !x. Unit s x ==> f (Inv s x) = |/ (f x): thm *) Theorem subring_unit_inv: !(r s):'a ring. s <= r ==> !x. Unit s x ==> (Inv s x = |/ x) @@ -2331,7 +2329,6 @@ Proof rw[ring_mult_comm] QED - (* Theorem: Ring r /\ INJ f R univ(:'b) ==> GroupHomo f r.sum (ring_inj_image r f).sum *) (* Proof: Note R = r.prod.carrier by ring_carriers diff --git a/examples/algebra/ring/ringScript.sml b/examples/algebra/ring/ringScript.sml index 0f23b4f743..ade062c311 100644 --- a/examples/algebra/ring/ringScript.sml +++ b/examples/algebra/ring/ringScript.sml @@ -897,8 +897,6 @@ val ring_num_suc = store_thm( ``!r:'a ring. Ring r ==> !n. ##(SUC n) = ##n + #1``, rw[ring_add_comm]); -(* Theorem: ##0 = #0 *) - (* ringTheory.ring_num_0 has Ring r ==> ##0 = #0 by lifting. but: @@ -917,9 +915,9 @@ Theorem ring_num_0[simp] = (* val ring_num_0 = |- !r. ##0 = #0: thm *) (* Obtain another theorem *) -val ring_num_one = save_thm("ring_num_one", +Theorem ring_num_one = monoid_exp_def |> ISPEC ``(r:'a ring).sum`` |> ISPEC ``#1`` |> ISPEC ``1`` - |> SIMP_RULE bool_ss [FUNPOW_1] |> GEN ``r:'a ring``); + |> SIMP_RULE bool_ss [FUNPOW_1] |> GEN ``r:'a ring`` (* val ring_num_one = |- !r. ##1 = #1 + #0: thm *) (* Do not export this one: an expansion. *) @@ -1003,6 +1001,7 @@ val ring_exp_element = lift_monoid_thm "exp_element" "exp_element"; val _ = export_rewrites ["ring_exp_element"]; (* Theorem: x ** 0 = #1 *) +(* Proof: by monoid_exp_0. *) (* Note: monoid_exp_0 |- !g x. x ** 0 = #e *) Theorem ring_exp_0[simp]: !x:'a. x ** 0 = #1 Proof rw[] diff --git a/examples/fermat/count/combinatoricsScript.sml b/examples/fermat/count/combinatoricsScript.sml index 62c470800f..c99c97514a 100644 --- a/examples/fermat/count/combinatoricsScript.sml +++ b/examples/fermat/count/combinatoricsScript.sml @@ -2469,41 +2469,6 @@ QED (* This is more restrictive than perm_set_list_not_empty, hence not useful. *) -(* Theorem: s IN (partition (feq set) (list_count n k)) ==> - (set o CHOICE) s IN (sub_count n k) *) -(* Proof: - s IN (partition (feq set) (list_count n k)) - <=> ?x. x IN list_count n k /\ - s = equiv_class (feq set) (list_count n k) x by partition_element - ==> ?x. x IN list_count n k /\ s = perm_set (set x) by list_count_set_eq_class - Thus ALL_DISTINCT x /\ set x SUBSET count n /\ LENGTH x = k - by list_count_element - and (set o CHOICE) s - = set (CHOICE (perm_set (set x))) by o_THM - Note perm_set (set x) <> {} by perm_set_list_not_empty - Let ls = CHOICE (perm_set (set x)). - Then ls IN perm_set (set x) by CHOICE_DEF - so ALL_DISTINCT ls /\ set ls = set x by perm_set_element - Thus (set o CHOICE) s = set x - With set x SUBSET count n by above - and CARD (set x) = LENGTH x = k by ALL_DISTINCT_CARD_LIST_TO_SET - so (set x) IN (sub_count n k) by sub_count_element -*) -Theorem list_count_set_map_element: - !s n k. s IN (partition (feq set) (list_count n k)) ==> - (set o CHOICE) s IN (sub_count n k) -Proof - rw_tac bool_ss [partition_element] >> - simp[list_count_set_eq_class] >> - qabbrev_tac `ls = CHOICE (perm_set (set x))` >> - `perm_set (set x) <> {}` by metis_tac[perm_set_list_not_empty] >> - `ls IN perm_set (set x)` by fs[CHOICE_DEF, Abbr`ls`] >> - fs[list_count_element, perm_set_element, sub_count_element] >> - simp[ALL_DISTINCT_CARD_LIST_TO_SET] -QED - -(* Another proof of the same theorem, slightly better. *) - (* Theorem: s IN (partition (feq set) (list_count n k)) ==> (set o CHOICE) s IN (sub_count n k) *) (* Proof: @@ -2522,7 +2487,7 @@ QED and CARD (set ls) = LENGTH ls by ALL_DISTINCT_CARD_LIST_TO_SET so set ls IN (sub_count n k) by sub_count_element_alt *) -Theorem list_count_set_map_element[allow_rebind]: +Theorem list_count_set_map_element: !s n k. s IN (partition (feq set) (list_count n k)) ==> (set o CHOICE) s IN (sub_count n k) Proof @@ -2766,21 +2731,6 @@ Proof simp[arrange_def, perm_def, list_count_0_n] QED -(* Theorem: n arrange n = perm n *) -(* Proof: - n arrange n - = CARD (list_count n n) by arrange_def - = CARD (perm_count n) by list_count_n_n - = perm n by perm_def -*) -Theorem arrange_n_n: - !n. n arrange n = perm n -Proof - simp[arrange_def, perm_def, list_count_n_n] -QED - -(* Another proof of the same theorem. *) - (* Theorem: n arrange n = perm n *) (* Proof: n arrange n @@ -2788,7 +2738,7 @@ QED = 1 * FACT n by binomial_n_n = perm n by perm_eq_fact *) -Theorem arrange_n_n[allow_rebind]: +Theorem arrange_n_n: !n. n arrange n = perm n Proof simp[arrange_formula, binomial_n_n, perm_eq_fact] diff --git a/examples/fermat/count/permutationScript.sml b/examples/fermat/count/permutationScript.sml index c3bcfd1ff7..aff5247f7e 100644 --- a/examples/fermat/count/permutationScript.sml +++ b/examples/fermat/count/permutationScript.sml @@ -392,20 +392,6 @@ Proof metis_tac[MEM_EL, list_to_bij_thm, IN_COUNT] QED -(* Theorem: ls IN perm_count n ==> list_to_bij ls PERMUTES count n *) -(* Proof: - Note INJ (list_to_bij ls) (count n) (count n) by list_to_bij_count_inj - and SURJ (list_to_bij ls) (count n) (count n) by list_to_bij_count_surj - Hence BIJ (list_to_bij ls) (count n) (count n) by BIJ_DEF -*) -Theorem list_to_bij_count_bij: - !ls n. ls IN perm_count n ==> list_to_bij ls PERMUTES count n -Proof - simp[BIJ_DEF, list_to_bij_count_inj, list_to_bij_count_surj] -QED - -(* Another proof of the same theorem. *) - (* Theorem: ls IN perm_count n ==> list_to_bij ls PERMUTES count n *) (* Proof: Note INJ (list_to_bij ls) (count n) (count n) by list_to_bij_count_inj @@ -1199,7 +1185,7 @@ QED (* Theorem: GroupIso list_to_bij (permutation_group n) (symmetric_group (count n)) *) (* Proof: by list_to_bij_map_iso, group_iso_monoid_iso. *) -Theorem permutation_group_iso_symmetric_group: +Theorem permutation_group_iso_symmetric_group[allow_rebind]: !n. GroupIso list_to_bij (permutation_group n) (symmetric_group (count n)) Proof metis_tac[list_to_bij_map_iso, group_iso_monoid_iso] @@ -1254,36 +1240,6 @@ Proof simp[perm_count_list_op_el, listRangeLHI_EL, Abbr`t`] QED -(* Theorem: ls IN perm_count n ==> (ls oo [0 ..< n]) n = ls *) -(* Proof: - Let t = [0 ..< n]. - Then t IN perm_count n by perm_count_has_id - and (ls oo t) n IN perm_count n by perm_count_list_op_closure - so LENGTH ls = n by perm_count_element_length - so LENGTH ((ls oo t) n) = n by perm_count_element_length - By LIST_EQ, it remains to show: - !x. x < n ==> EL x ((ls oo t) n) = EL x ls - - EL x ((ls oo t) n) - = EL (EL x t) ls by perm_count_list_op_el - = EL x ls by listRangeLHI_EL -*) -Theorem perm_count_list_op_rid: - !ls n. ls IN perm_count n ==> (ls oo [0 ..< n]) n = ls -Proof - rpt strip_tac >> - qabbrev_tac `t = [0 ..< n]` >> - `t IN perm_count n` by rw[perm_count_has_id, Abbr`t`] >> - `(ls oo t) n IN perm_count n` by rw[perm_count_list_op_closure] >> - imp_res_tac perm_count_element_length >> - irule LIST_EQ >> - simp[] >> - rpt strip_tac >> - simp[perm_count_list_op_el, listRangeLHI_EL, Abbr`t`] -QED - -(* A slightly better proof using map_list_to_bij_id. *) - (* Theorem: ls IN perm_count n ==> (ls oo [0 ..< n]) n = ls *) (* Proof: Let t = [0 ..< n]. @@ -1520,7 +1476,7 @@ QED (6) x IN perm_count n ==> ((permutation_group n).inv x oo x) n = [0 ..< n] This is true by permutation_group_inv, perm_count_list_op_inv *) -Theorem permutation_group_group: +Theorem permutation_group_group[allow_rebind]: !n. Group (permutation_group n) Proof rw_tac bool_ss[group_alt, permutation_group_property, RES_FORALL_THM] >- diff --git a/examples/fermat/little/FLTfixedpointScript.sml b/examples/fermat/little/FLTfixedpointScript.sml index 3a7f2d0181..302b2cb0d4 100644 --- a/examples/fermat/little/FLTfixedpointScript.sml +++ b/examples/fermat/little/FLTfixedpointScript.sml @@ -404,7 +404,7 @@ fixedpoint_prime_congruence |> ISPEC ``p:num`` |> ISPEC ``cycle``; |- !X. prime p /\ (Zadd p act X) cycle /\ FINITE X ==> CARD X MOD p = CARD (fixed_points cycle (Zadd p) X) MOD p *) -Theorem fermat_little_thm: +Theorem fermat_little_thm[allow_rebind]: !p a. prime p ==> a ** p MOD p = a MOD p Proof rpt strip_tac >> diff --git a/examples/fermat/little/FLTnecklaceScript.sml b/examples/fermat/little/FLTnecklaceScript.sml index d540de9441..aa095879ce 100644 --- a/examples/fermat/little/FLTnecklaceScript.sml +++ b/examples/fermat/little/FLTnecklaceScript.sml @@ -120,8 +120,8 @@ open gcdTheory; (* for PRIME_GCD *) ls IN e ==> ls IN multicoloured n a multicoloured_prime_order |- !p a ls. prime p /\ ls IN multicoloured p a ==> order ls = p - multicoloured_associate_card_prime - |- !p a ls. prime p /\ ls IN multicoloured p a ==> CARD (associate ls) = p + multicoloured_partition_card_prime + |- !p a e. prime p /\ e IN multicoloured_partition p a ==> CARD e = p multicoloured_card_prime |- !p a. prime p ==> CARD (multicoloured p a) = p * CARD (multicoloured_partition p a) @@ -824,7 +824,7 @@ QED = SIGMA (order l) by associate_card_eq_order = SIGMA (p) by order of a multicoloured necklace <> 1 and for prime length, order = 1 or p. - = p * CARD (multicoloured_partition p a) by SIGMA_CARD_CONSTANT + = p * CARD (multicoloured_partition p a) by multicoloured_partition_card_prime, SIGMA_CARD_CONSTANT *) Theorem multicoloured_card_prime: !p a. prime p ==> diff --git a/examples/fermat/twosq/involuteActionScript.sml b/examples/fermat/twosq/involuteActionScript.sml index b718cfc82e..e3ba4fece8 100644 --- a/examples/fermat/twosq/involuteActionScript.sml +++ b/examples/fermat/twosq/involuteActionScript.sml @@ -189,14 +189,6 @@ val funpow_reach = save_thm("funpow_reach", (* val funpow_reach = |- !f x y. reach (FUNPOW f) Z2 x y <=> ?a. a < 2 /\ FUNPOW f a x = y: thm *) -val funpow_equiv = save_thm("funpow_equiv", - reach_equiv |> ISPEC ``FUNPOW f`` |> ISPEC ``Z2`` |> GEN_ALL -); -(* val funpow_equiv = -|- !f X. Group Z2 /\ (Z2 act X) (FUNPOW f) ==> reach (FUNPOW f) Z2 equiv_on X: thm *) - -(* A better version *) - (* Theorem: f involute X ==> reach (FUNPOW f) Z2 equiv_on X *) (* Proof: Note Group Z2 by Zadd_group, 0 < 2 @@ -421,16 +413,6 @@ val involute_fixed_points_element_element = (* Involution Target Cardinality *) (* ------------------------------------------------------------------------- *) -val involute_target_card_by_types = save_thm("involute_target_card_by_types", - target_card_by_orbit_types |> ISPEC ``FUNPOW f`` |> ISPEC ``Z2`` |> GEN_ALL -); -(* val involute_target_card_by_types = -|- !f X. Group Z2 /\ (Z2 act X) (FUNPOW f) /\ FINITE X ==> - CARD X = CARD (sing_orbits (FUNPOW f) Z2 X) + - SIGMA CARD (multi_orbits (FUNPOW f) Z2 X): thm *) - -(* A better version *) - (* Theorem: FINITE X /\ f involute X ==> CARD X = CARD (sing_orbits (FUNPOW f) Z2 X) + SIGMA CARD (multi_orbits (FUNPOW f) Z2 X) *) diff --git a/examples/fermat/twosq/iterateComposeScript.sml b/examples/fermat/twosq/iterateComposeScript.sml index c6aa5cc49c..9a9ec0a44c 100644 --- a/examples/fermat/twosq/iterateComposeScript.sml +++ b/examples/fermat/twosq/iterateComposeScript.sml @@ -406,62 +406,6 @@ QED (* Idea: iterates (f o g)^i = (g o f)^j iff (i + j) MOD p = 0. *) -(* Theorem: FINITE s /\ f involute s /\ g involute s /\ - x IN s /\ p = iterate_period (f o g) x ==> - (FUNPOW (f o g) i x = FUNPOW (g o f) j x <=> (i + j) MOD p = 0) *) -(* Proof: - Note f o g PERMUTES s by involute_involute_permutes - and 0 < p by iterate_period_pos, FINITE s - - If part: FUNPOW (f o g) i x = FUNPOW (g o f) j x ==> (i + j) MOD p = 0 - FUNPOW (f o g) (i + j) x - = FUNPOW (f o g) (j + i) x by arithmetic - = FUNPOW (f o g) j (FUNPOW (f o g) i x) by FUNPOW_ADD - = FUNPOW (f o g) j (FUNPOW (g o f) j x) by given - = x by involute_funpow_inv, x IN s - Thus (i + j) MOD p = 0 by iterate_period_mod - - Only-if part: (i + j) MOD p = 0 ==> FUNPOW (f o g) i x = FUNPOW (g o f) j x - Note FUNPOW (f o g) p x = x by iterate_period_property, [1] - so ?k. (i + j) = k * p by MOD_EQ_0_DIVISOR, (i + j) MOD p = 0 - Let y = FUNPOW (f o g) i x. - Then y IN s by FUNPOW_closure, f o g PERMUTES s - FUNPOW (f o g) i x = y - = FUNPOW (g o f) j (FUNPOW (f o g) j y) by involute_funpow_inv, y IN s - = FUNPOW (g o f) j (FUNPOW (f o g) (j + i) x) by FUNPOW_ADD - = FUNPOW (g o f) j (FUNPOW (f o g) p x) by FUNPOW_MULTIPLE, 0 < p - = FUNPOW (g o f) j x by [1] -*) -Theorem iterate_involute_mod_period: - !f g s x p i j. FINITE s /\ f involute s /\ g involute s /\ - x IN s /\ p = iterate_period (f o g) x ==> - (FUNPOW (f o g) i x = FUNPOW (g o f) j x <=> (i + j) MOD p = 0) -Proof - rpt strip_tac >> - qabbrev_tac `y = FUNPOW (f o g) i x` >> - qabbrev_tac `z = FUNPOW (g o f) j x` >> - `f o g PERMUTES s` by rw[involute_involute_permutes] >> - `0 < p` by metis_tac[iterate_period_pos] >> - (rewrite_tac[EQ_IMP_THM] >> rpt strip_tac) >| [ - assume_tac involute_funpow_inv >> - last_x_assum (qspecl_then [`f`, `g`, `s`, `x`, `j`] strip_assume_tac) >> - `FUNPOW (f o g) (i + j) x = FUNPOW (f o g) (j + i) x` by simp[] >> - `_ = FUNPOW (f o g) j z` by rw[FUNPOW_ADD] >> - `_ = x` by fs[Abbr`z`] >> - metis_tac[iterate_period_mod], - `?k. (i + j) = k * p` by rfs[MOD_EQ_0_DIVISOR] >> - `y IN s` by rw[FUNPOW_closure, Abbr`y`] >> - `FUNPOW (f o g) p x = x` by rw[iterate_period_property] >> - assume_tac involute_funpow_inv >> - last_x_assum (qspecl_then [`g`, `f`, `s`, `y`, `j`] strip_assume_tac) >> - `y = FUNPOW (g o f) j (FUNPOW (f o g) j y)` by fs[] >> - `_ = FUNPOW (g o f) j (FUNPOW (f o g) (j + i) x)` by metis_tac[FUNPOW_ADD] >> - rfs[FUNPOW_MULTIPLE] - ] -QED - -(* Better proof of the same theorem. *) - (* Theorem: FINITE s /\ f involute s /\ g involute s /\ x IN s /\ p = iterate_period (f o g) x ==> (FUNPOW (f o g) i x = FUNPOW (g o f) j x <=> (i + j) MOD p = 0) *) @@ -484,7 +428,7 @@ QED <=> FUNPOW (f o g) (i + j) x = x by above <=> (i + j) MOD p = 0 by iterate_period_mod, 0 < p *) -Theorem iterate_involute_mod_period[allow_rebind]: +Theorem iterate_involute_mod_period: !f g s x p i j. FINITE s /\ f involute s /\ g involute s /\ x IN s /\ p = iterate_period (f o g) x ==> (FUNPOW (f o g) i x = FUNPOW (g o f) j x <=> (i + j) MOD p = 0) @@ -588,69 +532,6 @@ QED (* Idea: when f fixes x, then (f o g)^i = f ((f o g)^j) iff (i+j) MOD p = 0. *) -(* Theorem: FINITE s /\ f involute s /\ g involute s /\ - x IN fixes f s /\ p = iterate_period (f o g) x ==> - (FUNPOW (f o g) i x = f (FUNPOW (f o g) j x) <=> (i + j) MOD p = 0) *) -(* Proof: - Note x IN s /\ f x = x by fixes_element - - If part: FUNPOW (f o g) i x = f (FUNPOW (f o g) j x) ==> (i + j) MOD p = 0 - Note f o g PERMUTES s by involute_involute_permutes - so 0 < p by iterate_period_pos, FINITE s - FUNPOW (f o g) (i + j) x - = FUNPOW (f o g) i (FUNPOW (f o g) j x) by FUNPOW_ADD - = FUNPOW (f o g) i (f (f (FUNPOW (f o g) j x))) by FUNPOW_closure, f o g involute s - = FUNPOW (f o g) i (f (FUNPOW (f o g) i x)) by given - = f (FUNPOW (g o f) i (FUNPOW (f o g) i x)) by iterate_involute_compose_shift - = f x by involute_funpow_inv - = x by involute_fixed_points - Thus (i + j) MOD p = 0 by iterate_period_mod, 0 < p - - Only-if part: (i + j) MOD p = 0 ==> FUNPOW (f o g) i x = f (FUNPOW (f o g) j x) - f (FUNPOW (f o g) j x) - = f (FUNPOW (g o f) i x) by iterate_involute_mod_period - = FUNPOW (f o g) i (f x) by iterate_involute_compose_shift - = FUNPOW (f o g) i x by involute_fixed_points, f x = x -*) -Theorem involute_involute_fix_orbit_1: - !f g s x p i j. FINITE s /\ f involute s /\ g involute s /\ - x IN fixes f s /\ p = iterate_period (f o g) x ==> - (FUNPOW (f o g) i x = f (FUNPOW (f o g) j x) <=> - (i + j) MOD p = 0) -Proof - rpt strip_tac >> - qabbrev_tac `y = FUNPOW (f o g) i x` >> - qabbrev_tac `z = FUNPOW (f o g) j x` >> - `x IN s /\ f x = x` by fs[fixes_element] >> - (simp[EQ_IMP_THM] >> rpt strip_tac) >| [ - `f o g PERMUTES s` by rw[involute_involute_permutes] >> - `0 < p` by metis_tac[iterate_period_pos] >> - `y IN s /\ z IN s` by fs[FUNPOW_closure, Abbr`y`, Abbr`z`] >> - imp_res_tac iterate_involute_compose_shift >> - `f (FUNPOW (g o f) i y) = FUNPOW (f o g) i (f y)` by fs[] >> - assume_tac involute_funpow_inv >> - last_x_assum (qspecl_then [`g`, `f`, `s`, `x`, `i`] strip_assume_tac) >> - `FUNPOW (g o f) i y = x` by rfs[] >> - `FUNPOW (f o g) (i + j) x = FUNPOW (f o g) i z` by rw[FUNPOW_ADD, Abbr`z`] >> - `_ = FUNPOW (f o g) i (f (f z))` by rw[] >> - `_ = FUNPOW (f o g) i (f y)` by rw[] >> - `_ = f (FUNPOW (g o f) i y)` by fs[] >> - `_ = f x` by fs[Abbr`y`] >> - `_ = x` by rfs[] >> - metis_tac[iterate_period_mod], - drule_then strip_assume_tac iterate_involute_mod_period >> - `z = FUNPOW (g o f) i x` by fs[Abbr`z`] >> - imp_res_tac iterate_involute_compose_shift >> - `f (FUNPOW (g o f) i x) = FUNPOW (f o g) i (f x)` by fs[] >> - `f z = f (FUNPOW (g o f) i x)` by fs[] >> - `_ = FUNPOW (f o g) i (f x)` by fs[] >> - `_ = y` by fs[Abbr`y`] >> - simp[] - ] -QED - -(* Better proof of the same theorem. *) - (* Theorem: FINITE s /\ f involute s /\ g involute s /\ x IN fixes f s /\ p = iterate_period (f o g) x ==> (FUNPOW (f o g) i x = f (FUNPOW (f o g) j x) <=> (i + j) MOD p = 0) *) @@ -668,7 +549,7 @@ QED <=> FUNPOW (g o f) i x = FUNPOW (f o g) j x by BIJ_DEF, INJ_EQ_11 <=> (i + j) MOD p = 0 by iterate_involute_mod_period, 0 < p *) -Theorem involute_involute_fix_orbit_1[allow_rebind]: +Theorem involute_involute_fix_orbit_1: !f g s x p i j. FINITE s /\ f involute s /\ g involute s /\ x IN fixes f s /\ p = iterate_period (f o g) x ==> (FUNPOW (f o g) i x = f (FUNPOW (f o g) j x) <=> @@ -694,75 +575,6 @@ QED (* Idea: when f fixes x, then (f o g)^i = g ((f o g)^j) iff (i+j+1) MOD p = 0. *) -(* Theorem: FINITE s /\ f involute s /\ g involute s /\ - x IN fixes f s /\ p = iterate_period (f o g) x ==> - (FUNPOW (f o g) i x = g (FUNPOW (f o g) j x) <=> (i + j + 1) MOD p = 0) *) -(* Proof: - Note x IN s /\ f x = x by fixes_element - - If part: FUNPOW (f o g) i x = g (FUNPOW (f o g) j x) ==> (i + j + 1) MOD p = 0 - Note f o g PERMUTES s by involute_involute_permutes - so 0 < p by iterate_period_pos, FINITE s - FUNPOW (f o g) (i + j + 1) x - = (f o g) (FUNPOW (f o g) (i + j) x) by FUNPOW_SUC - = (f o g) (FUNPOW (f o g) i (FUNPOW (f o g) j x)) by FUNPOW_ADD - = f (g (FUNPOW (f o g) i (FUNPOW (f o g) j x))) by o_THM - = f (FUNPOW (g o f) i (g (FUNPOW (f o g) j x))) by iterate_involute_compose_shift - = f (FUNPOW (g o f) i (FUNPOW (f o g) i x)) by given - = f x by involute_funpow_inv - = x by involute_fixed_points - Thus (i + j + 1) MOD p = 0 by iterate_period_mod, 0 < p - - Only-if part: (i + j + 1) MOD p = 0 ==> FUNPOW (f o g) i x = g (FUNPOW (f o g) j x) - FUNPOW (f o g) i x - = FUNPOW (g o f) (j + 1) x by iterate_involute_mod_period - = FUNPOW (g o f) j ((g o f) x) by FUNPOW - = FUNPOW (g o f) j (g (f x)) by o_THM - = FUNPOW (g o f) j (g x) by f x = x - = g (FUNPOW (f o g) j x) by iterate_involute_compose_shift -*) -Theorem involute_involute_fix_orbit_2: - !f g s x p i j. FINITE s /\ f involute s /\ g involute s /\ - x IN fixes f s /\ p = iterate_period (f o g) x ==> - (FUNPOW (f o g) i x = g (FUNPOW (f o g) j x) <=> - (i + j + 1) MOD p = 0) -Proof - rpt strip_tac >> - qabbrev_tac `y = FUNPOW (f o g) j x` >> - qabbrev_tac `z = FUNPOW (f o g) i x` >> - `x IN s /\ f x = x` by fs[fixes_element] >> - (rewrite_tac[EQ_IMP_THM] >> rpt strip_tac) >| [ - `f o g PERMUTES s` by rw[involute_involute_permutes] >> - `0 < p` by metis_tac[iterate_period_pos] >> - `y IN s /\ z IN s` by rw[FUNPOW_closure, Abbr`y`, Abbr`z`] >> - imp_res_tac iterate_involute_compose_shift >> - `g (FUNPOW (f o g) i y) = FUNPOW (g o f) i (g y)` by fs[] >> - imp_res_tac involute_funpow_inv >> - `FUNPOW (g o f) i z = x` by fs[Abbr`z`] >> - `i + j + 1 = SUC (i + j)` by decide_tac >> - `FUNPOW (f o g) (i + j + 1) x = FUNPOW (f o g) (SUC (i + j)) x` by rw[] >> - `_ = (f o g) (FUNPOW (f o g) (i + j) x)` by fs[FUNPOW_SUC] >> - `_ = (f o g) (FUNPOW (f o g) i y)` by fs[FUNPOW_ADD, Abbr`y`] >> - `_ = f (g (FUNPOW (f o g) i y))` by rw[] >> - `_ = f (FUNPOW (g o f) i (g y))` by fs[] >> - `_ = f (FUNPOW (g o f) i z)` by metis_tac[] >> - `_ = f x` by rfs[] >> - `_ = x` by fs[] >> - metis_tac[iterate_period_mod], - drule_then strip_assume_tac iterate_involute_mod_period >> - last_x_assum (qspecl_then [`f`, `g`, `x`, `p`, `i`, `j+1`] strip_assume_tac) >> - `FUNPOW (g o f) (j + 1) x = z` by rfs[Abbr`z`] >> - drule_then strip_assume_tac iterate_involute_compose_shift >> - `g y = FUNPOW (g o f) j (g x)` by fs[Abbr`y`] >> - `_ = FUNPOW (g o f) j ((g o f) x)` by fs[] >> - `_ = FUNPOW (g o f) (j + 1) x` by rw[GSYM FUNPOW, ADD1] >> - `_ = z` by fs[] >> - simp[] - ] -QED - -(* Better proof of the same theorem. *) - (* Theorem: FINITE s /\ f involute s /\ g involute s /\ x IN fixes f s /\ p = iterate_period (f o g) x ==> (FUNPOW (f o g) i x = g (FUNPOW (f o g) j x) <=> (i + j + 1) MOD p = 0) *) @@ -778,7 +590,7 @@ QED <=> FUNPOW (f o g) i x = FUNPOW (g o f) (j + 1) x by FUNPOW <=> (i + j + 1) MOD p = 0 by iterate_involute_mod_period, 0 < p *) -Theorem involute_involute_fix_orbit_2[allow_rebind]: +Theorem involute_involute_fix_orbit_2: !f g s x p i j. FINITE s /\ f involute s /\ g involute s /\ x IN fixes f s /\ p = iterate_period (f o g) x ==> (FUNPOW (f o g) i x = g (FUNPOW (f o g) j x) <=> diff --git a/examples/fermat/twosq/twoSquaresScript.sml b/examples/fermat/twosq/twoSquaresScript.sml index ad1f9a6bbf..16415a8d41 100644 --- a/examples/fermat/twosq/twoSquaresScript.sml +++ b/examples/fermat/twosq/twoSquaresScript.sml @@ -205,7 +205,6 @@ QED (* Fermat Two-Squares Uniqueness. *) (* ------------------------------------------------------------------------- *) - (* Theorem: prime p /\ (p = a ** 2 + b ** 2) /\ (p = c ** 2 + d ** 2) ==> ({a; b} = {c; d}) *) (* Proof: @@ -303,7 +302,6 @@ Proof ] QED - (* Theorem: prime p /\ ODD a /\ EVEN b /\ (p = a ** 2 + b ** 2) /\ ODD c /\ EVEN d /\ (p = c ** 2 + d ** 2) ==> ((a = c) /\ (b = d)) *) (* Proof: @@ -384,7 +382,6 @@ QED (* Fermat Two-Squares Existence. *) (* ------------------------------------------------------------------------- *) - (* 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. @@ -436,7 +433,6 @@ Proof metis_tac[mills_element] QED - (* Theorem: prime p /\ (p MOD 4 = 1) ==> ?(u,v). ODD u /\ EVEN v /\ (p = u ** 2 + v ** 2) *) (* Proof: @@ -591,7 +587,6 @@ Proof metis_tac[flip_fixes_prime] QED - (* Theorem: !p. prime p /\ (p MOD 4 = 1) ==> ?!(u,v). ODD u /\ EVEN v /\ (p = u ** 2 + v ** 2) *) (* Proof: @@ -612,7 +607,6 @@ Proof ] QED - (* Theorem: prime p ==> ((p MOD 4 = 1) <=> ?!(u,v). ODD u /\ EVEN v /\ (p = u ** 2 + v ** 2)) *) (* Proof: @@ -776,12 +770,6 @@ Proof ] QED -(* This proof is using: - 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. -*) - (* ------------------------------------------------------------------------- *) (* Computation by WHILE loop. *) (* ------------------------------------------------------------------------- *) @@ -1036,33 +1024,6 @@ Proof fs[] QED -(* Another proof of the same theorem, using two_sq_thm. *) - -(* Theorem: prime p /\ (p MOD 4 = 1) ==> - let (u,v) = two_squares p in (p = u ** 2 + v ** 2) *) -(* Proof: - Let t = two_sq p. - 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 - = 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 -*) -Theorem two_squares_thm: - !p. prime p /\ (p MOD 4 = 1) ==> - let (u,v) = two_squares p in (p = u ** 2 + v ** 2) -Proof - rw[two_squares_def] >> - qabbrev_tac `t = two_sq p` >> - `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] >> - simp[windmill_by_squares] -QED - (* ------------------------------------------------------------------------- *) (* Fermat's Two Squares Theorem by Group Action. *) (* ------------------------------------------------------------------------- *) @@ -1130,43 +1091,6 @@ QED giving the existence of Fermat's two squares. *) -(* Proof based on involute_two_fixed_points_both_odd *) - -(* Theorem: prime p /\ p MOD 4 = 1 ==> - 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) - 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) - 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 - When a = 1, true by FUNPOW_1, zagier_fix -*) -Theorem zagier_fixed_points_sing: - !p. prime p /\ p MOD 4 = 1 ==> - fixed_points (FUNPOW zagier) Z2 (mills p) = {(1,1,p DIV 4)} -Proof - rw[fixed_points_def, mills_def, Zadd_element, EXTENSION] >> - simp[EQ_IMP_THM] >> - rpt strip_tac >| [ - rename1 ‘x = (x',y,z)’ >> - `~square p` by metis_tac[prime_non_square] >> - `p MOD 4 <> 0` by decide_tac >> - `zagier x = x` by metis_tac[FUNPOW_1, DECIDE``1 < 2``] >> - `x' = y` by metis_tac[zagier_fix, mills_element, mills_triple_nonzero] >> - metis_tac[windmill_trivial_prime], - metis_tac[windmill_trivial_prime], - (`a = 0 \/ a = 1` by decide_tac >> fs[zagier_fix]) - ] -QED - -(* A better proof of the same theorem *) - (* Theorem: prime p /\ p MOD 4 = 1 ==> fixed_points (FUNPOW zagier) Z2 (mills p) = {(1,1,p DIV 4)} *) (* Proof: diff --git a/examples/fermat/twosq/windmillScript.sml b/examples/fermat/twosq/windmillScript.sml index 6db543ed6e..ebd328286d 100644 --- a/examples/fermat/twosq/windmillScript.sml +++ b/examples/fermat/twosq/windmillScript.sml @@ -159,7 +159,7 @@ open GaussTheory; (* for divisors_has_factor *) if x < 2 * y then (2 * y - x,y,x) else (x - 2 * y,x,y) zagier_x_x_z |- !x z. x <> 0 ==> zagier (x,x,z) = (x,x,z) 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_xyz |- !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 @@ -1807,7 +1807,7 @@ QED (* Theorem: x * z <> 0 ==> zagier (zagier (x, y, z)) = (x, y, z) *) (* Proof: by MULT_EQ_0, zagier_involute. *) -Theorem zagier_involute_alt0: +Theorem zagier_involute_xyz: !x y z. x * z <> 0 ==> zagier (zagier (x, y, z)) = (x, y, z) Proof rw[zagier_involute] diff --git a/examples/simple_complexity/lib/complexityScript.sml b/examples/simple_complexity/lib/complexityScript.sml index f97abfa690..5a3a79ca9c 100644 --- a/examples/simple_complexity/lib/complexityScript.sml +++ b/examples/simple_complexity/lib/complexityScript.sml @@ -1004,11 +1004,6 @@ val poly_O_sum = store_thm( ``!n. (poly_O n) |+| (poly_O n) = poly_O n``, rw[big_O_sum_self]); -(* Derive this theorem *) -val poly_O_sum = save_thm("poly_O_sum", - big_O_sum_self |> SPEC ``POLY n`` |> GEN_ALL); -(* val poly_O_sum = |- !n. poly_O n |+| poly_O n = poly_O n: thm *) - (* Theorem: poly_O n |+| poly_O m SUBSET poly_O (MAX n m) *) (* Proof: Note poly_O n |+| poly_O m SUBSET big_O (POLY n .+. POLY m) by big_O_sum_subset diff --git a/examples/simple_complexity/loop/loopDecreaseScript.sml b/examples/simple_complexity/loop/loopDecreaseScript.sml index 27aab959e6..0b8b13af5b 100644 --- a/examples/simple_complexity/loop/loopDecreaseScript.sml +++ b/examples/simple_complexity/loop/loopDecreaseScript.sml @@ -855,8 +855,8 @@ val loop_dec_count_cover_le = store_thm( (!x. loop x = if x = 0 then c else body x + loop (x - b)) ==> !x. loop x <= c + hop b x * body x *) (* Proof: by loop_dec_count_cover_le with cover = body. *) -val loop_dec_count_cover_le = store_thm( - "loop_dec_count_cover_le", +val loop_dec_count_le = store_thm( + "loop_dec_count_le", ``!loop body cover b c. 0 < b /\ (!x. body x <= cover x) /\ MONO cover /\ (!x. loop x = if x = 0 then c else body x + loop (x - b)) ==> !x. loop x <= c + hop b x * cover x``, @@ -1905,42 +1905,6 @@ val loop_dec_count_exit_by_sum = store_thm( `loop_arg guard modify x = decrease_by b x` by rw[decrease_by_eq_loop_arg, Abbr`guard`, Abbr`modify`] >> metis_tac[]); -(* Theorem: 0 < b /\ (!x. body x <= cover x) /\ MONO cover /\ - (!x. loop x = if x = 0 then c else body x + if exit x then 0 else loop (x - b)) ==> - !x. loop x <= c + cover x * hop b x *) -(* Proof: - Let guard = (\x. x = 0), - modify = (\x. x - b), - R = measure (\x. x), - Then WF R by WF_measure - and !x. ~guard x ==> R (modify x) x by x - b < x, 0 < b - and !x y. R x y ==> cover x <= cover y by R, LESS_IMP_LESS_OR_EQ, MONO cover - Also !x. loop x = if guard x then c else body x + if exit x then 0 else loop (modify x) - by given - loop x - <= c + cover x * loop_count guard modify x by loop_modify_count_cover_exit_upper - = c + cover x * hop b x by hop_eq_loop_count -*) -val loop_dec_count_cover_exit_upper = store_thm( - "loop_dec_count_cover_exit_upper", - ``!loop body cover exit b c. 0 < b /\ (!x. body x <= cover x) /\ MONO cover /\ - (!x. loop x = if x = 0 then c else body x + if exit x then 0 else loop (x - b)) ==> - !x. loop x <= c + cover x * hop b x``, - rpt strip_tac >> - qabbrev_tac `guard = \x. x = 0` >> - qabbrev_tac `modify = \x. x - b` >> - qabbrev_tac `R = measure (\x. x)` >> - `WF R` by rw[Abbr`R`] >> - `!x. ~guard x ==> R (modify x) x` by rw[Abbr`guard`, Abbr`R`, Abbr`modify`] >> - `!x y. R x y ==> cover x <= cover y` by rw[Abbr`R`] >> - `!x. loop x = if guard x then c else body x + if exit x then 0 else loop (modify x)` by metis_tac[] >> - assume_tac (loop_modify_count_cover_exit_upper |> ISPEC ``loop:num -> num``) >> - last_x_assum (qspecl_then [`guard`, `body`, `c`, `cover`, `exit`, `modify`, `R`] strip_assume_tac) >> - `loop_count guard modify x = hop b x` by rw[hop_eq_loop_count, Abbr`guard`, Abbr`modify`] >> - metis_tac[]); - -(* This is the same, but directly from the SUM *) - (* Theorem: 0 < b /\ (!x. body x <= cover x) /\ MONO cover /\ (!x. loop x = if x = 0 then c else body x + if exit x then 0 else loop (x - b)) ==> !x. loop x <= c + cover x * hop b x *) diff --git a/examples/simple_complexity/loop/loopDivideScript.sml b/examples/simple_complexity/loop/loopDivideScript.sml index 1b7c46fbd8..711cf355f9 100644 --- a/examples/simple_complexity/loop/loopDivideScript.sml +++ b/examples/simple_complexity/loop/loopDivideScript.sml @@ -1773,13 +1773,6 @@ val divide_by_member = store_thm( rw[MEM_GENLIST] >> metis_tac[pop_property]); -(* Derive a theorem: put j = 0 in divide_by_member *) -val divide_by_head = save_thm("divide_by_head", - divide_by_member |> SPEC ``b:num`` |> SPEC ``n:num`` |> SPEC ``0`` - |> SIMP_RULE (srw_ss()) [EXP_0, DIV_1] |> GEN ``n:num`` |> GEN ``b:num``); -(* val divide_by_head = |- !b n. 1 < b /\ 0 < n /\ 1 <= n ==> MEM n (divide_by b n): thm *) -(* Not compact enough *) - (* Theorem: 1 < b /\ 0 < n ==> MEM n (divide_by b n) *) (* Proof: by divide_by_member, EXP_0, DIV_1 *) val divide_by_head = store_thm( @@ -1993,42 +1986,6 @@ val loop_div_count_exit_by_sum = store_thm( `loop_arg guard modify x = divide_by b x` by rw[divide_by_eq_loop_arg, Abbr`guard`, Abbr`modify`] >> metis_tac[]); -(* Theorem: 1 < b /\ (!x. body x <= cover x) /\ MONO cover /\ - (!x. loop x = if x = 0 then c else body x + if exit x then 0 else loop (x DIV b)) ==> - !x. loop x <= c + cover x * pop b x *) -(* Proof: - Let guard = (\x. x = 0), - modify = (\x. x DIV b), - R = measure (\x. x), - Then WF R by WF_measure - and !x. ~guard x ==> R (modify x) x by DIV_LESS, x DIV b < x, 1 < b - and !x y. R x y ==> cover x <= cover y by R, LESS_IMP_LESS_OR_EQ, MONO cover - Also !x. loop x = if guard x then c else body x + if exit x then 0 else loop (modify x) - by given - loop x - <= c + cover x * loop_count guard modify x by loop_modify_count_cover_exit_upper - = c + cover x * pop b x by pop_eq_loop_count -*) -val loop_div_count_cover_exit_upper = store_thm( - "loop_div_count_cover_exit_upper", - ``!loop body cover exit b c. 1 < b /\ (!x. body x <= cover x) /\ MONO cover /\ - (!x. loop x = if x = 0 then c else body x + if exit x then 0 else loop (x DIV b)) ==> - !x. loop x <= c + cover x * pop b x``, - rpt strip_tac >> - qabbrev_tac `guard = \x. x = 0` >> - qabbrev_tac `modify = \x. x DIV b` >> - qabbrev_tac `R = measure (\x. x)` >> - `WF R` by rw[Abbr`R`] >> - `!x. ~guard x ==> R (modify x) x` by rw[Abbr`guard`, Abbr`R`, Abbr`modify`] >> - `!x y. R x y ==> cover x <= cover y` by rw[Abbr`R`] >> - `!x. loop x = if guard x then c else body x + if exit x then 0 else loop (modify x)` by metis_tac[] >> - assume_tac (loop_modify_count_cover_exit_upper |> ISPEC ``loop:num -> num``) >> - last_x_assum (qspecl_then [`guard`, `body`, `c`, `cover`, `exit`, `modify`, `R`] strip_assume_tac) >> - `loop_count guard modify x = pop b x` by rw[pop_eq_loop_count, Abbr`guard`, Abbr`modify`] >> - metis_tac[]); - -(* This is the same, but directly from the SUM *) - (* Theorem: 1 < b /\ (!x. body x <= cover x) /\ MONO cover /\ (!x. loop x = if x = 0 then c else body x + if exit x then 0 else loop (x DIV b)) ==> !x. loop x <= c + cover x * pop b x *) diff --git a/examples/simple_complexity/loop/loopIncreaseScript.sml b/examples/simple_complexity/loop/loopIncreaseScript.sml index 49157fa478..f69fe7bfbf 100644 --- a/examples/simple_complexity/loop/loopIncreaseScript.sml +++ b/examples/simple_complexity/loop/loopIncreaseScript.sml @@ -1741,29 +1741,6 @@ val increase_by_length = store_thm( ``!b m x. LENGTH (increase_by b m x) = bop b m x``, rw[increase_by_eqn]); -(* This is the shortest proof. Others are much worse. *) - -(* Theorem: LENGTH (increase_by b m x) = bop b m x *) -(* Proof: - By induction from increase_by_def. - If b = 0 \/ m <= x, - LENGTH (increase_by b m x) - = LENGTH [] by increase_by_nil - = 0 = bop b m x by bop_0 - If b <> 0 /\ ~(m <= x) - LENGTH (increase_by b m x) - = LENGTH (x::increase_by b m (x + b)) by increase_by_cons - = SUC (LENGTH increase_by b m (x + b)) by LENGTH - = SUC (bop b m (x + b)) by induction hypothesis - = bop b m x by bop_suc -*) -val increase_by_length = store_thm( - "increase_by_length", - ``!b m x. LENGTH (increase_by b m x) = bop b m x``, - ho_match_mp_tac (theorem "increase_by_ind") >> - rw[] >> - rw[Once increase_by_def, Once bop_def]); - (* Theorem: LENGTH (increasing m c) = m - c *) (* Proof: LENGTH (increasing m c) @@ -1891,58 +1868,6 @@ val iterating_increase_eq_loop2_arg = store_thm( metis_tac[loop2_arg_cons] ]); -(* ------------------------------------------------------------------------- *) - -(* Obtain theorems from general theory *) - -(* -loop_arg_length |> SPEC_ALL |> INST_TYPE [alpha |-> ``:num``] - |> Q.INST [`modify` |-> `(\x. x + b)`, `guard` |-> `(\x. m <= x)`, `R` |-> `measure (\x. m - x)`] - |> ADD_ASSUM ``0 < b`` |> DISCH_ALL - |> SIMP_RULE (srw_ss()) [GSYM bop_eq_loop_count, GSYM increase_by_eq_loop_arg]; -val it = - |- 0 < b ==> - (!x. ~(m <= x) ==> m < x + b + (m - x) /\ 0 < m - x) ==> - !x. - LENGTH (loop_arg (\x. m <= x) (\x. x + b) x) = - loop_count (\x. m <= x) (\x. x + b) x: thm -*) - -(* Theorem: LENGTH (increase_by b m x) = bop b m x *) -(* Proof: - If b = 0, - LENGTH (increase_by 0 m x) - = LENGTH [] by increase_by_nil - = 0 = bop 0 m x by bop_0 - If 0 < b, - Let guard = (\x. m <= x), - modify = (\x. x + b), - R = measure (\x. m - x). - Then WF R by WF_measure - and !x. ~guard x ==> R (modify x) x by m - (x + b) < m - x, b <> 0 - LENGTH (increase_by b m x) - = LENGTH (loop_arg guard modify x) by increase_by_eq_loop_arg - = loop_count guard modify x by loop_arg_length - = bop b m x by bop_eq_loop_count -*) -val increase_by_length = store_thm( - "increase_by_length", - ``!b m x. LENGTH (increase_by b m x) = bop b m x``, - rpt strip_tac >> - Cases_on `b = 0` >- - rw[increase_by_nil, bop_0] >> - qabbrev_tac `guard = \x. m <= x` >> - qabbrev_tac `modify = \x. x + b` >> - qabbrev_tac `R = measure (\x. m - x)` >> - `WF R` by rw[Abbr`R`] >> - `!x. ~guard x ==> R (modify x) x` by fs[Abbr`guard`, Abbr`R`, Abbr`modify`] >> - `LENGTH (increase_by b m x) = LENGTH (loop_arg guard modify x)` by rw[increase_by_eq_loop_arg] >> - `_ = loop_count guard modify x` by metis_tac[loop_arg_length] >> - `_ = bop b m x` by rw[bop_eq_loop_count] >> - decide_tac); - -(* This just verifieds the previous direct proof by definition. *) - (* ------------------------------------------------------------------------- *) (* Increase Loop -- original *) (* ------------------------------------------------------------------------- *) diff --git a/examples/simple_complexity/loop/loopMultiplyScript.sml b/examples/simple_complexity/loop/loopMultiplyScript.sml index 194d529479..289307cdb6 100644 --- a/examples/simple_complexity/loop/loopMultiplyScript.sml +++ b/examples/simple_complexity/loop/loopMultiplyScript.sml @@ -1864,29 +1864,6 @@ val multiply_by_length = store_thm( ``!b m x. LENGTH (multiply_by b m x) = mop b m x``, rw[multiply_by_eqn]); -(* This is the shortest proof. Others are much worse. *) - -(* Theorem: LENGTH (multiply_by b m x) = mop b m x *) -(* Proof: - By induction from multiply_by_def. - If b <= 1 \/ x = 0 \/ m <= x, - LENGTH (multiply_by b m x) - = LENGTH [] by multiply_by_nil - = 0 = mop b m x by mop_0 - If 1 < b /\ x <> 0 /\ ~(m <= x) - LENGTH (multiply_by b m x) - = LENGTH (x::multiply_by b m (b * x)) by multiply_by_cons - = SUC (LENGTH multiply_by b m (b * x)) by LENGTH - = SUC (mop b m (b * x)) by induction hypothesis - = mop b m x by mop_suc -*) -val multiply_by_length = store_thm( - "multiply_by_length", - ``!b m x. LENGTH (multiply_by b m x) = mop b m x``, - ho_match_mp_tac (theorem "multiply_by_ind") >> - rw[] >> - rw[Once multiply_by_def, Once mop_def]); - (* Theorem: 1 < m ==> (LENGTH (doubling m 1) = LOG2 m + if m = 2 ** LOG2 m then 0 else 1) *) (* Proof: LENGTH (doubling m 1) @@ -2023,59 +2000,6 @@ val iterating_multiply_eq_loop2_arg = store_thm( metis_tac[loop2_arg_cons] ]); -(* ------------------------------------------------------------------------- *) - -(* Obtain theorems from general theory *) - -(* -loop_arg_length |> SPEC_ALL |> INST_TYPE [alpha |-> ``:num``] - |> Q.INST [`modify` |-> `(\x. b * x)`, `guard` |-> `(\x. x = 0 \/ m <= x)`, `R` |-> `measure (\x. m - x)`] - |> ADD_ASSUM ``1 < b`` |> DISCH_ALL - |> SIMP_RULE (srw_ss()) [GSYM mop_eq_loop_count, GSYM multiply_by_eq_loop_arg]; -val it = - |- 1 < b ==> - (!x. x <> 0 /\ ~(m <= x) ==> m < b * x + (m - x) /\ 0 < m - x) ==> - !x. LENGTH (multiply_by b m x) = mop b m x: thm -*) - -(* Theorem: LENGTH (multiply_by b m x) = mop b m x *) -(* Proof: - If b <= 1, - LENGTH (multiply_by 0 m x) - = LENGTH [] by multiply_by_nil - = 0 = mop 0 m x by mop_0 - If 1 < b, - Let guard = (\x. x = 0 \/ m <= x), - modify = (\x. b * x), - R = measure (\x. m - x). - Then WF R by WF_measure - and !x. ~guard x ==> R (modify x) x by m - (b * x) < m - x, b <> 0 - LENGTH (multiply_by b m x) - = LENGTH (loop_arg guard modify x) by multiply_by_eq_loop_arg - = loop_count guard modify x by loop_arg_length - = mop b m x by mop_eq_loop_count -*) -val multiply_by_length = store_thm( - "multiply_by_length", - ``!b m x. LENGTH (multiply_by b m x) = mop b m x``, - rpt strip_tac >> - Cases_on `b <= 1` >- - rw[multiply_by_nil, mop_0] >> - qabbrev_tac `guard = \x. x = 0 \/ m <= x` >> - qabbrev_tac `modify = \x. b * x` >> - qabbrev_tac `R = measure (\x. m - x)` >> - `WF R` by rw[Abbr`R`] >> - `!x. ~guard x ==> R (modify x) x` by - (rw[Abbr`guard`, Abbr`R`, Abbr`modify`] >> - `x < b * x` by rw[] >> - decide_tac) >> - `LENGTH (multiply_by b m x) = LENGTH (loop_arg guard modify x)` by rw[multiply_by_eq_loop_arg] >> - `_ = loop_count guard modify x` by metis_tac[loop_arg_length] >> - `_ = mop b m x` by rw[mop_eq_loop_count] >> - decide_tac); - -(* This just verifieds the previous direct proof by definition. *) - (* ------------------------------------------------------------------------- *) (* Multiplying Loop -- original *) (* ------------------------------------------------------------------------- *) diff --git a/examples/simple_complexity/loop/loopScript.sml b/examples/simple_complexity/loop/loopScript.sml index 480f654979..79a0000f54 100644 --- a/examples/simple_complexity/loop/loopScript.sml +++ b/examples/simple_complexity/loop/loopScript.sml @@ -2668,101 +2668,6 @@ val loop2_arg_cover_sum = loop2_thm_type_a "arg_cover_sum"; SUM (MAP (K (cover (p_1,p_2))) (loop2_arg guard modify transform p_1 p_2)): thm *) -(* Not using theorem transform *) - - -val loop2_arg_thm = store_thm( - "loop2_arg_thm", - ``!transform modify guard R. - WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) ==> - !x y. loop2_arg guard modify transform x y = - if guard x y then [] - else (x,y)::(loop2_arg guard modify transform (transform x) (modify y))``, - rw[loop2_arg_def] >> - imp_res_tac loop_arg_thm >> - rw[Once pairTheory.FORALL_PROD]); - -val loop2_arg_nil = store_thm( - "loop2_arg_nil", - ``!transform modify guard R. - WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) ==> - !x y. guard x y ==> (loop2_arg guard modify transform x y = [])``, - rw[loop2_arg_def] >> - imp_res_tac loop_arg_nil >> - rw[Once pairTheory.FORALL_PROD]); - -val loop2_arg_cons = store_thm( - "loop2_arg_cons", - ``!transform modify guard R. - WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) ==> - !x y. ~guard x y ==> (loop2_arg guard modify transform x y = - (x,y)::(loop2_arg guard modify transform (transform x) (modify y)))``, - rw[loop2_arg_def] >> - imp_res_tac loop_arg_cons >> - rw[Once pairTheory.FORALL_PROD]); - -val loop2_arg_length = store_thm( - "loop2_arg_length", - ``!transform modify guard R. - WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) ==> - !x y. LENGTH (loop2_arg guard modify transform x y) = - loop2_count guard modify transform x y``, - rw[loop2_arg_def, loop2_count_def] >> - imp_res_tac loop_arg_length >> - rw[Once pairTheory.FORALL_PROD]); - -(* Theorem: WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) ==> - !x y. loop2_arg guard modify transform x y = - GENLIST (\j. (FUNPOW transform j x,FUNPOW modify j y)) - (loop2_count guard modify transform x y) *) -(* Proof: by loop_arg_eqn, loop2_arg_def, loop2_count_def *) -val loop2_arg_eqn = store_thm( - "loop2_arg_eqn", - ``!transform modify guard R. - WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) ==> - !x y. loop2_arg guard modify transform x y = - GENLIST (\j. (FUNPOW transform j x,FUNPOW modify j y)) - (loop2_count guard modify transform x y)``, - rw[loop2_arg_def, loop2_count_def] >> - imp_res_tac loop_arg_eqn >> - rw[Once pairTheory.FORALL_PROD] >> - qabbrev_tac `f1 = \j. FUNPOW (\(x,y). (transform x,modify y)) j (x,y)` >> - qabbrev_tac `f2 = \j. (FUNPOW transform j x,FUNPOW modify j y)` >> - `f1 = f2` by rw[FUN_EQ_THM, FUNPOW_PAIR, Abbr`f1`, Abbr`f2`] >> - rw[]); - -val loop2_arg_element = store_thm( - "loop2_arg_element", - ``!transform modify guard R. - WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) ==> - !x y k. k < loop2_count guard modify transform x y ==> - (EL k (loop2_arg guard modify transform x y) = - (FUNPOW transform k x,FUNPOW modify k y))``, - rw[loop2_arg_def, loop2_count_def] >> - imp_res_tac loop_arg_element >> - rw[Once pairTheory.FORALL_PROD, FUNPOW_PAIR]); - -(* Theorem: WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) ==> - (!x1 x2 y1 y2. R (x1,y1) (x2,y2) ==> cover x1 y1 <= cover x2 y2) ==> - !x y. SUM (MAP (UNCURRY cover) (loop2_arg guard modify transform x y)) <= - SUM (MAP (K (cover x y)) (loop2_arg guard modify transform x y)) *) -(* Proof: by loop_arg_cover_sum, loop2_count_def, loop2_arg_def. *) -val loop2_arg_cover_sum = store_thm( - "loop2_arg_cover_sum", - ``!transform modify guard cover R. - WF R /\ (!x y. ~guard x y ==> R (transform x,modify y) (x,y)) ==> - (!x1 x2 y1 y2. R (x1,y1) (x2,y2) ==> cover x1 y1 <= cover x2 y2) ==> - !x y. SUM (MAP (UNCURRY cover) (loop2_arg guard modify transform x y)) <= - SUM (MAP (K (cover x y)) (loop2_arg guard modify transform x y))``, - rpt strip_tac >> - assume_tac (loop_arg_cover_sum |> SPEC_ALL |> INST_TYPE [alpha |-> ``:'a # 'b``] - |> SIMP_RULE (srw_ss()) [pairTheory.FORALL_PROD] - |> Q.INST [`guard` |-> `(\(x,y). gd x y)`, `modify` |-> `(\(x,y). (t x, m y))`] - |> SIMP_RULE (srw_ss()) [GSYM loop2_arg_def] |> GEN_ALL - |> CONV_RULE (RENAME_VARS_CONV ["transform", "modify", "guard"])) >> - first_x_assum (qspecl_then [`transform`, `modify`, `guard`, `UNCURRY cover`, `R`] strip_assume_tac) >> - fs[]); - (* Obtain theorems by transform *) fun loop2_thm_type_b suffix = let val th1 = DB.fetch "loop" ("loop_" ^ suffix)