Fix more duplicated theorems after breakage caused by 705d331

HOL-Theorem-Prover · Sep 13, 2023 · e622e8f · e622e8f
1 parent e985be8
commit e622e8f
Show file tree

Hide file tree

Showing 8 changed files with 88 additions and 208 deletions.
diff --git a/examples/algebra/lib/helperFunctionScript.sml b/examples/algebra/lib/helperFunctionScript.sml
@@ -3666,15 +3666,16 @@ val gcd_coprime_cancel = store_thm(
    Simple proof of GCD_CANCEL_MULT:
    (a*c, b) = (a*c , b*1) = (a * c, b * (c, 1)) = (a * c, b * c, b) = ((a, b) * c, b) = (c, b) since (a,b) = 1.
 *)
-val gcd_coprime_cancel = store_thm(
-  "gcd_coprime_cancel",
-  ``!m n p. coprime p n ==> (gcd (p * m) n = gcd m n)``,
+Theorem gcd_coprime_cancel[allow_rebind]:
+  !m n p. coprime p n ==> (gcd (p * m) n = gcd m n)
+Proof
   rpt strip_tac >>
-  `gcd (p * m) n = gcd (p * m) (n * (gcd m 1))` by rw[GCD_1] >>
-  `_ = gcd (p * m) (gcd (n * m) n)` by rw[GSYM GCD_COMMON_FACTOR] >>
-  `_ = gcd (gcd (p * m) (n * m)) n` by rw[GCD_ASSOC] >>
-  `_ = gcd m n` by rw[GCD_COMMON_FACTOR, MULT_COMM] >>
-  rw[]);
+  ‘gcd (p * m) n = gcd (p * m) (n * (gcd m 1))’ by rw[GCD_1] >>
+  ‘_ = gcd (p * m) (gcd (n * m) n)’ by rw[GSYM GCD_COMMON_FACTOR] >>
+  ‘_ = gcd (gcd (p * m) (n * m)) n’ by rw[GCD_ASSOC] >>
+  ‘_ = gcd m n’ by rw[GCD_COMMON_FACTOR, MULT_COMM] >>
+  rw[]
+QED
 
 (* Theorem: prime p /\ prime q /\ p <> q ==> coprime p q *)
 (* Proof:
@@ -4062,16 +4063,6 @@ val power_predecessor_divisibility = store_thm(
   `_ = (gcd n m = n)` by rw[EXP_BASE_INJECTIVE] >>
   rw[divides_iff_gcd_fix]);
 
-(* This is numerical version of:
-poly_unity_1_divides  |- !r. Ring r /\ #1 <> #0 ==> !n. X - |1| pdivides unity n
-*)
-val power_predecessor_divisor = save_thm("power_predecessor_divisor",
-    power_predecessor_divisibility
-       |> SPEC ``t:num`` |> SPEC ``1:num`` |> SPEC ``n:num``
-       |> SIMP_RULE (srw_ss()) [] |> GEN_ALL);
-(* val power_predecessor_divisor = |- !t n. 1 < t ==> t - 1 divides t ** n - 1: thm *)
-(* However, this is too restrictive. *)
-
 (* Theorem: t - 1 divides t ** n - 1 *)
 (* Proof:
    If t = 0,
@@ -4087,19 +4078,20 @@ val power_predecessor_divisor = save_thm("power_predecessor_divisor",
        ==> t ** 1 - 1 divides t ** n - 1   by power_predecessor_divisibility
         or      t - 1 divides t ** n - 1   by EXP_1
 *)
-val power_predecessor_divisor = store_thm(
-  "power_predecessor_divisor",
-  ``!t n. t - 1 divides t ** n - 1``,
+Theorem power_predecessor_divisor:
+  !t n. t - 1 divides t ** n - 1
+Proof
   rpt strip_tac >>
   Cases_on `t = 0` >-
   simp[ZERO_EXP] >>
   Cases_on `t = 1` >-
   simp[] >>
   `1 < t` by decide_tac >>
-  metis_tac[power_predecessor_divisibility, EXP_1, ONE_DIVIDES_ALL]);
+  metis_tac[power_predecessor_divisibility, EXP_1, ONE_DIVIDES_ALL]
+QED
 
 (* Overload power predecessor *)
-val _ = overload_on("tops", ``\b:num n. b ** n - 1``);
+Overload tops = “\b:num n. b ** n - 1”
 
 (*
    power_predecessor_division_eqn

diff --git a/examples/algebra/lib/helperListScript.sml b/examples/algebra/lib/helperListScript.sml
@@ -758,10 +758,6 @@ val LAST_EL_CONS = store_thm(
 val FRONT_LENGTH = save_thm ("FRONT_LENGTH", LENGTH_FRONT);
 (* val FRONT_LENGTH = |- !l. l <> [] ==> (LENGTH (FRONT l) = PRE (LENGTH l)): thm *)
 
-val FRONT_EL = save_thm ("FRONT_EL", EL_FRONT);
-(* val FRONT_EL = |- !l n. n < LENGTH (FRONT l) /\ ~NULL l ==> (EL n (FRONT l) = EL n l) *)
-(* This is not convenient. *)
-
 (* Theorem: l <> [] /\ n < LENGTH (FRONT l) ==> (EL n (FRONT l) = EL n l) *)
 (* Proof: by EL_FRONT, NULL *)
 val FRONT_EL = store_thm(
@@ -2657,16 +2653,16 @@ val rotate_shift_element = store_thm(
   `j < LENGTH l` by decide_tac >>
   `SUC j - 1 = j` by decide_tac >>
   rw[DROP_def, TAKE_def]);
-(* Michael's proof *)
-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))``,
+
+Theorem rotate_shift_element[allow_rebind]:
+  !l n. n < LENGTH l ==> (rotate n l = EL n l::(DROP (SUC n) l ++ TAKE n l))
+Proof
   rw[rotate_def] >>
   pop_assum mp_tac >>
   qid_spec_tac `n` >>
-  Induct_on `l` >-
-  rw[] >>
-  rw[DROP_def] >> Cases_on `n` >> fs[]);
+  Induct_on `l` >- rw[] >>
+  rw[DROP_def] >> Cases_on `n` >> fs[]
+QED
 
 (* Theorem: rotate 0 l = l *)
 (* Proof:
@@ -3145,19 +3141,21 @@ val MONOLIST_EQ = store_thm(
     `set l2 = set t` by rw[] >>
     metis_tac[IN_SING]
   ]);
-(* Michael's Proof *)
-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))``,
+
+Theorem MONOLIST_EQ[allow_rebind]:
+  !l1 l2. SING (set l1) /\ SING (set l2) ==>
+          ((l1 = l2) <=> (LENGTH l1 = LENGTH l2) /\ (set l1 = set l2))
+Proof
   Induct >> rw[NOT_SING_EMPTY, SING_INSERT] >| [
     Cases_on `l2` >> rw[] >>
     full_simp_tac (srw_ss()) [SING_INSERT, EQUAL_SING] >>
     rw[LENGTH_NIL, NOT_SING_EMPTY, EQUAL_SING] >> metis_tac[],
     Cases_on `l2` >> rw[] >>
-    full_simp_tac (srw_ss()) [SING_INSERT, LENGTH_NIL, NOT_SING_EMPTY, EQUAL_SING] >>
+    full_simp_tac (srw_ss()) [SING_INSERT, LENGTH_NIL, NOT_SING_EMPTY,
+                              EQUAL_SING] >>
     metis_tac[]
-  ]);
+  ]
+QED
 
 (* Theorem: A non-mono-list has at least one element in tail that is distinct from its head.
            ~SING (set (h::t)) ==> ?h'. h' IN set t /\ h' <> h *)
@@ -4869,10 +4867,6 @@ val PROD_eq_1 = store_thm(
   Induct >>
   rw[] >>
   metis_tac[]);
-(* proof like SUM_eq_0 *)
-val PROD_eq_1 = store_thm("PROD_eq_1",
-  ``!ls. (PROD ls = 1) = !x. MEM x ls ==> (x = 1)``,
-  INDUCT_THEN list_INDUCT ASSUME_TAC THEN SRW_TAC[] [PROD, MEM] THEN METIS_TAC[]);
 
 (* Theorem: PROD (SNOC x l) = (PROD l) * x *)
 (* Proof:
@@ -4898,10 +4892,13 @@ val PROD_SNOC = store_thm(
   Induct >>
   rw[]);
 (* proof like SUM_SNOC *)
-val PROD_SNOC = store_thm("PROD_SNOC",
-    (``!x l. PROD (SNOC x l) = (PROD l) * x``),
-    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]);
+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:
@@ -4922,12 +4919,7 @@ val PROD_SNOC = store_thm("PROD_SNOC",
 val PROD_APPEND = store_thm(
   "PROD_APPEND",
   ``!l1 l2. PROD (APPEND l1 l2) = PROD l1 * PROD l2``,
-  Induct >>
-  rw[]);
-(* proof like SUM_APPEND *)
-val PROD_APPEND = store_thm("PROD_APPEND",
-    (``!l1 l2. PROD (APPEND l1 l2) = PROD l1 * PROD l2``),
-    INDUCT_THEN list_INDUCT ASSUME_TAC THEN ASM_REWRITE_TAC[PROD, APPEND, MULT_LEFT_1, MULT_ASSOC]);
+  Induct >> rw[]);
 
 (* Theorem: PROD (MAP f ls) = FOLDL (\a e. a * f e) 1 ls *)
 (* Proof:
@@ -4953,11 +4945,6 @@ val PROD_MAP_FOLDL = store_thm(
   rpt strip_tac >-
   rw[] >>
   rw[MAP_SNOC, PROD_SNOC, FOLDL_SNOC]);
-(* proof like SUM_MAP_FOLDL *)
-val PROD_MAP_FOLDL = Q.store_thm("PROD_MAP_FOLDL",
-    `!ls f. PROD (MAP f ls) = FOLDL (\a e. a * f e) 1 ls`,
-    HO_MATCH_MP_TAC SNOC_INDUCT THEN
-    SRW_TAC [] [FOLDL_SNOC, MAP_SNOC, PROD_SNOC, MAP, PROD, FOLDL]);
 
 (* Theorem: FINITE s ==> !f. PI f s = PROD (MAP f (SET_TO_LIST s)) *)
 (* Proof:
@@ -4975,14 +4962,6 @@ val PROD_IMAGE_eq_PROD_MAP_SET_TO_LIST = store_thm(
   rpt AP_THM_TAC >>
   AP_TERM_TAC >>
   rw[FUN_EQ_THM]);
-(* proof like SUM_IMAGE_eq_SUM_MAP_SET_TO_LIST *)
-val PROD_IMAGE_eq_PROD_MAP_SET_TO_LIST = Q.store_thm(
-   "PROD_IMAGE_eq_PROD_MAP_SET_TO_LIST",
-   `!s. FINITE s ==> !f. PI f s = PROD (MAP f (SET_TO_LIST s))`,
-    SRW_TAC [] [PROD_IMAGE_DEF] THEN
-    SRW_TAC [] [ITSET_eq_FOLDL_SET_TO_LIST, PROD_MAP_FOLDL] THEN
-    AP_THM_TAC THEN AP_THM_TAC THEN AP_TERM_TAC THEN
-    SRW_TAC [] [FUN_EQ_THM, arithmeticTheory.MULT_COMM]);
 
 (* Define PROD using accumulator *)
 val PROD_ACC_DEF = Lib.with_flag (Defn.def_suffix, "_DEF") Define
@@ -5019,17 +4998,9 @@ 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",
+  "PROD_PROD_ACC[compute]",
   ``!L. PROD L = PROD_ACC L 1``,
   rw[PROD_ACC_PROD_LEM]);
-(* proof like SUM_SUM_ACC *)
-val PROD_PROD_ACC = store_thm
-("PROD_PROD_ACC",
-  ``!L. PROD L = PROD_ACC L 1``,
-  PROVE_TAC [PROD_ACC_PROD_LEM, MULT_RIGHT_1]);
-
-(* Put in computeLib *)
-val _ = computeLib.add_funs [PROD_PROD_ACC];
 
 (* EVAL ``PROD [1; 2; 3; 4]``; --> 24 *)
 
@@ -5784,13 +5755,6 @@ QED
 val listRangeLHI_LEN = save_thm("listRangeLHI_LEN",  LENGTH_listRangeLHI |> GEN_ALL);
 (* val listRangeLHI_LEN = |- !lo hi. LENGTH [lo ..< hi] = hi - lo: thm *)
 
-(* Theorem: LENGTH [m ..< n] = n - m *)
-(* Proof: by LENGTH_listRangeLHI *)
-val listRangeLHI_LEN = store_thm(
-  "listRangeLHI_LEN",
-  ``!m n. LENGTH [m ..< n] = n - m``,
-  rw[LENGTH_listRangeLHI]);
-
 (* Theorem: ([m ..< n] = []) <=> n <= m *)
 (* Proof:
    If n = 0, LHS = T, RHS = T    hence true.

diff --git a/examples/algebra/lib/helperSetScript.sml b/examples/algebra/lib/helperSetScript.sml
@@ -1575,17 +1575,19 @@ val MIN_SET_EQ_0 = store_thm(
           = SUC n                                            by LESS_SUC, MAX_DEF
           = RHS
 *)
-val MAX_SET_IMAGE_SUC_COUNT = store_thm(
-  "MAX_SET_IMAGE_SUC_COUNT",
-  ``!n. MAX_SET (IMAGE SUC (count n)) = n``,
-  Induct_on `n` >-
+Theorem MAX_SET_IMAGE_SUC_COUNT:
+  !n. MAX_SET (IMAGE SUC (count n)) = n
+Proof
+  Induct_on ‘n’ >-
   rw[] >>
-  `MAX_SET (IMAGE SUC (count (SUC n))) = MAX_SET (IMAGE SUC (n INSERT count n))` by rw[COUNT_SUC] >>
-  `_ = MAX_SET ((SUC n) INSERT (IMAGE SUC (count n)))` by rw[] >>
-  `_ = MAX (SUC n) (MAX_SET (IMAGE SUC (count n)))` by rw[MAX_SET_THM] >>
-  `_ = MAX (SUC n) n` by rw[] >>
-  `_ = SUC n` by metis_tac[LESS_SUC, MAX_DEF, MAX_COMM] >>
-  rw[]);
+  ‘MAX_SET (IMAGE SUC (count (SUC n))) =
+   MAX_SET (IMAGE SUC (n INSERT count n))’ by rw[COUNT_SUC] >>
+  ‘_ = MAX_SET ((SUC n) INSERT (IMAGE SUC (count n)))’ by rw[] >>
+  ‘_ = MAX (SUC n) (MAX_SET (IMAGE SUC (count n)))’ by rw[MAX_SET_THM] >>
+  ‘_ = MAX (SUC n) n’ by rw[] >>
+  ‘_ = SUC n’ by metis_tac[LESS_SUC, MAX_DEF, MAX_COMM] >>
+  rw[]
+QED
 
 (* Another Proof: *)
 (* Theorem: MAX_SET (IMAGE SUC (count n)) = n *)
@@ -1608,13 +1610,17 @@ val MAX_SET_IMAGE_SUC_COUNT = store_thm(
           = SUC n                                           by LESS_SUC, MAX_DEF
           = RHS
 *)
-val MAX_SET_IMAGE_SUC_COUNT = store_thm(
-  "MAX_SET_IMAGE_SUC_COUNT",
-  ``!n. MAX_SET (IMAGE SUC (count n)) = n``,
+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]);
+  ‘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:
@@ -1816,34 +1822,12 @@ 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.
-*)
-val FINITE_CARD_IMAGE = store_thm(
-  "FINITE_CARD_IMAGE",
-  ``!s f. (!x y. (f x = f y) <=> (x = y)) /\ FINITE s ==> (CARD (IMAGE f s) = CARD s)``,
-  `!f. (!x y. (f x = f y) <=> (x = y)) ==> !s. FINITE s ==> (CARD (IMAGE f s) = CARD s)` suffices_by rw[] >>
-  gen_tac >>
-  strip_tac >>
-  ho_match_mp_tac FINITE_INDUCT >>
-  rw[]);
-(* Michael's proof *)
-val FINITE_CARD_IMAGE = store_thm(
-  "FINITE_CARD_IMAGE",
-  ``!s f. (!x y. (f x = f y) <=> (x = y)) /\ FINITE s ==> (CARD (IMAGE f s) = CARD s)``,
-  qsuff_tac `!f. (!x y. (f x = f y) = (x = y)) ==> !s. FINITE s ==> (CARD (IMAGE f s) = CARD s)` >-
-  metis_tac[] >>
-  gen_tac >> strip_tac >>
-  ho_match_mp_tac FINITE_INDUCT >> rw[]);
+Theorem FINITE_CARD_IMAGE:
+  !s f. (!x y. (f x = f y) <=> (x = y)) /\ FINITE s ==>
+        (CARD (IMAGE f s) = CARD s)
+Proof
+  Induct_on ‘FINITE’ >> rw[]
+QED
 
 (* Theorem: !s. FINITE s ==> CARD (IMAGE SUC s)) = CARD s *)
 (* Proof:
@@ -3071,10 +3055,10 @@ val PROD_IMAGE_CONG = store_thm(
     rw[PROD_IMAGE_EMPTY] >>
     metis_tac[PROD_IMAGE_INSERT, IN_INSERT]
   ]);
-(* proof like SUM_IMAGE_CONG *)
-val PROD_IMAGE_CONG = Q.store_thm(
-   "PROD_IMAGE_CONG",
-   `!s f1 f2. (!x. x IN s ==> (f1 x = f2 x)) ==> (PI f1 s = PI f2 s)`,
+
+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
@@ -3085,7 +3069,7 @@ val PROD_IMAGE_CONG = Q.store_thm(
    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: