Eliminate duplicate theorems in scripts, otherwise allow rebind.

HOL-Theorem-Prover · Sep 21, 2023 · b6d5e58 · b6d5e58
1 parent 58d0603
commit b6d5e58
Show file tree

Hide file tree

Showing 55 changed files with 218 additions and 2,648 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -633,17 +633,18 @@ 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] >-
   rw[ZN_finite_ring, PRIME_POS] >>
   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
@@ -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: