Clean up some integerTheory material about Num constant

This is possible thanks to change in 5523065; some knock on effects.
HOL-Theorem-Prover · Jan 25, 2024 · d3f180d · d3f180d
1 parent 7193600
commit d3f180d
Show file tree

Hide file tree

Showing 3 changed files with 103 additions and 123 deletions.
diff --git a/examples/algebra/ring/ringIntegerScript.sml b/examples/algebra/ring/ringIntegerScript.sml
@@ -808,42 +808,34 @@ val Z_quotient_iso_ZN = store_thm(
          ==> &k < &n               by INT_LT_CALCULATE
          ==> k < n                 by INT_LT (or INT_LT_CALCULATE)
 *)
-val Z_euclid_ring = store_thm(
-  "Z_euclid_ring",
-  ``EuclideanRing Z (Num o ABS)``,
-  rw[EuclideanRing_def] >-
-  rw[Z_ring] >-
- (rw[Z_def, Z_add_def] >>
-  rw[EQ_IMP_THM] >>
-  `(?n. (ABS x = &n) /\ n <> 0) \/ (?n. (ABS x = -&n) /\ n <> 0) \/ (ABS x = 0)` by rw[INT_NUM_CASES] >-
-  metis_tac[NUM_OF_INT] >-
- (`- &n < 0` by rw[] >>
-  metis_tac[INT_ABS_LT0]) >>
-  fs[INT_ABS_LE0]) >>
+
+Theorem Z_euclid_ring: EuclideanRing Z Num
+Proof
+  rw[EuclideanRing_def]
+  >- rw[Z_ring]
+  >- rw[Z_def, Z_add_def] >>
   pop_assum mp_tac >>
   pop_assum mp_tac >>
   pop_assum mp_tac >>
   rw[Z_def, Z_add_def, Z_mult_def] >>
-  qexists_tac `x / y` >>
-  qexists_tac `x % y` >>
-  `(x = x / y * y + x % y) /\ if y < 0 then (y < x % y /\ x % y <= 0) else (0 <= x % y /\ x % y < y)` by rw[INT_DIVISION] >>
-  qabbrev_tac `q = x / y ` >>
-  qabbrev_tac `t = x % y ` >>
-  `(?n. (y = &n) /\ n <> 0) \/ (?n. (y = -&n) /\ n <> 0) \/ (y = 0)` by rw[INT_NUM_CASES] >| [
-    `~(y < 0)` by rw[] >>
-    `0 <= t /\ t < y` by metis_tac[] >>
-    `?k. t = &k` by metis_tac[NUM_POSINT] >>
-    `Num (ABS t) = k` by rw[INT_ABS_NUM] >>
-    `Num (ABS y) = n` by rw[INT_ABS_NUM] >>
-    metis_tac[INT_LT],
-    `y < 0` by rw[] >>
-    `y < t /\ t <=0` by metis_tac[] >>
-    `?k. t = -&k` by metis_tac[NUM_NEGINT_EXISTS] >>
-    `-&n < -&k` by rw[] >>
-    `Num (ABS t) = k` by rw[INT_ABS_NEG, INT_ABS_NUM] >>
-    `Num (ABS y) = n` by rw[INT_ABS_NEG, INT_ABS_NUM] >>
-    metis_tac[INT_LT_CALCULATE]
-  ]);
+  qexists_tac ‘x / y’ >>
+  qexists_tac ‘x % y’ >>
+  ‘(x = x / y * y + x % y) /\
+   if y < 0 then (y < x % y /\ x % y <= 0) else (0 <= x % y /\ x % y < y)’
+    by rw[INT_DIVISION] >>
+  qabbrev_tac ‘q = x / y’ >>
+  qabbrev_tac ‘t = x % y’ >>
+  ‘(?n. (y = &n) /\ n <> 0) \/ (?n. (y = -&n) /\ n <> 0) \/ (y = 0)’
+    by rw[INT_NUM_CASES]
+  >- (‘~(y < 0)’ by rw[] >>
+      ‘0 <= t /\ t < y’ by metis_tac[] >>
+      ‘?k. t = &k’ by metis_tac[NUM_POSINT] >>
+      gvs[]) >>
+  ‘y < 0’ by rw[] >>
+  ‘y < t /\ t <= 0’ by metis_tac[] >>
+  ‘?k. t = -&k’ by metis_tac[NUM_NEGINT_EXISTS] >>
+  gvs[]
+QED
 
 (* Theorem: PrincipalIdealRing Z *)
 (* Proof:

diff --git a/src/integer/integerScript.sml b/src/integer/integerScript.sml
@@ -1239,29 +1239,27 @@ Proof
                REWRITE_TAC[INT_NOT_LE, INT_LT_ADDR, INT_LT_01]]
 QED
 
-Theorem INT_LT:
-    !m n. &m:int < &n <=> m < n
+Theorem INT_LT[simp]:
+  !m n. &m:int < &n <=> m < n
 Proof
-              REPEAT GEN_TAC
-              THEN MATCH_ACCEPT_TAC ((REWRITE_RULE[] o
-                                      AP_TERM (Term `$~:bool->bool`) o
-                                      REWRITE_RULE[GSYM NOT_LESS,
-                                                   GSYM INT_NOT_LT])
-                                     (SPEC_ALL INT_LE))
+  REPEAT GEN_TAC THEN
+  MATCH_ACCEPT_TAC ((REWRITE_RULE[] o
+                     AP_TERM (Term `$~:bool->bool`) o
+                     REWRITE_RULE[GSYM NOT_LESS, GSYM INT_NOT_LT])
+                    (SPEC_ALL INT_LE))
 QED
 
-val INT_INJ =
-    store_thm("INT_INJ",
-              Term `!m n. (&m:int = &n) = (m = n)`,
-              let val th = prove(Term `(m:num = n) <=> m <= n /\ n <= m`,
-                                 EQ_TAC
-                                 THENL [DISCH_THEN SUBST1_TAC
-                                        THEN REWRITE_TAC[LESS_EQ_REFL],
-                                        MATCH_ACCEPT_TAC LESS_EQUAL_ANTISYM])
-              in
-                  REPEAT GEN_TAC
-                  THEN REWRITE_TAC[th, GSYM INT_LE_ANTISYM, INT_LE]
-              end)
+Theorem INT_INJ[simp]: !m n. (&m:int = &n) = (m = n)
+Proof
+  let val th = prove(“(m:num = n) <=> m <= n /\ n <= m”,
+                     EQ_TAC
+                     THENL [DISCH_THEN SUBST1_TAC
+                            THEN REWRITE_TAC[LESS_EQ_REFL],
+                            MATCH_ACCEPT_TAC LESS_EQUAL_ANTISYM])
+  in
+    REPEAT GEN_TAC THEN REWRITE_TAC[th, GSYM INT_LE_ANTISYM, INT_LE]
+  end
+QED
 
 val INT_ADD =
     store_thm("INT_ADD",
@@ -1561,16 +1559,17 @@ Proof
                DISCH_TAC THEN ASM_REWRITE_TAC[INT_MUL_LZERO, INT_ADD_RID]]
 QED
 
-val INT_EQ_NEG =
-    store_thm("INT_EQ_NEG",
-              Term `!x y:int. (~x = ~y) = (x = y)`,
-              REPEAT GEN_TAC THEN
-              REWRITE_TAC[GSYM INT_LE_ANTISYM, INT_LE_NEG] THEN
-              MATCH_ACCEPT_TAC CONJ_SYM);
+Theorem INT_EQ_NEG[simp]: !x y:int. (~x = ~y) = (x = y)
+Proof
+  REPEAT GEN_TAC THEN
+  REWRITE_TAC[GSYM INT_LE_ANTISYM, INT_LE_NEG] THEN
+  MATCH_ACCEPT_TAC CONJ_SYM
+QED
 
-val int_eq_calculate = prove(
-  Term`!n m. ((&n = ~&m) <=> (n = 0) /\ (m = 0)) /\
-             ((~&n = &m) <=> (n = 0) /\ (m = 0))`,
+Theorem int_eq_calculate[simp]:
+  !n m. ((&n = ~&m) <=> (n = 0) /\ (m = 0)) /\
+        ((~&n = &m) <=> (n = 0) /\ (m = 0))
+Proof
   Induct THENL [
     SIMP_TAC int_ss [INT_NEG_0, INT_INJ, GSYM INT_NEG_EQ],
     SIMP_TAC int_ss [INT] THEN GEN_TAC THEN CONJ_TAC THENL [
@@ -1580,7 +1579,8 @@ val int_eq_calculate = prove(
       SIMP_TAC int_ss [int_sub] THEN
       ASM_SIMP_TAC int_ss [INT_NEGNEG, INT_ADD]
     ]
-  ]);
+  ]
+QED
 
 Theorem INT_LT_CALCULATE:
   !n m.  (&n:int < &m <=> n < m) /\ (~&n < ~&m <=> m < n) /\
@@ -1731,39 +1731,52 @@ QED
 val Num = new_definition("Num",
   Term `Num (i:int) = @n. if 0 <= i then i = &n else i = - &n`);
 
-val NUM_OF_INT =
-    store_thm("NUM_OF_INT[simp]",
-              Term `!n. Num(&n) = n`,
-              GEN_TAC THEN REWRITE_TAC[Num, INT_INJ, INT_POS] THEN
-              CONV_TAC(LAND_CONV(ONCE_DEPTH_CONV SYM_CONV)) THEN
-              REWRITE_TAC[SELECT_REFL]);
-val _ = computeLib.add_persistent_funs ["NUM_OF_INT"]
-
-val NUM_OF_NEG_INT =
-    store_thm("NUM_OF_NEG_INT[simp]",
-              Term `!n. Num(-&n) = n`,
-              GEN_TAC THEN
-              REWRITE_TAC[Num, INT_INJ, INT_POS, INT_EQ_NEG] THEN
-              Cases_on ‘0 <= -&n’ THEN ASM_REWRITE_TAC [] THEN
-              CONV_TAC (RATOR_CONV (ONCE_REWRITE_CONV [EQ_SYM_EQ])) THEN
-              REWRITE_TAC [SELECT_REFL] THEN
-              POP_ASSUM MP_TAC THEN
-              REWRITE_TAC [INT_NEG_GE0,INT_LE,LE] THEN
-              STRIP_TAC THEN ASM_REWRITE_TAC [INT_NEG_0,INT_INJ] THEN
-              REWRITE_TAC [SELECT_REFL]);
-val _ = computeLib.add_persistent_funs ["NUM_OF_NEG_INT"]
-
-val INT_OF_NUM =
-    store_thm("INT_OF_NUM",
-              Term `!i. (&(Num i) = i) <=> 0 <= i`,
-              GEN_TAC THEN EQ_TAC THEN1
-                (DISCH_THEN(SUBST1_TAC o SYM) THEN MATCH_ACCEPT_TAC INT_POS) THEN
-              DISCH_THEN(ASSUME_TAC o EXISTENCE o MATCH_MP NUM_POSINT) THEN
-              REWRITE_TAC[Num] THEN CONV_TAC SYM_CONV THEN
-              POP_ASSUM STRIP_ASSUME_TAC THEN
-              ASM_REWRITE_TAC [INT_POS,INT_INJ] THEN
-              CONV_TAC (RAND_CONV (ONCE_REWRITE_CONV [EQ_SYM_EQ])) THEN
-              REWRITE_TAC [SELECT_REFL]);
+Theorem NUM_OF_INT[simp,compute]:
+  !n. Num(&n) = n
+Proof
+  GEN_TAC THEN REWRITE_TAC[Num, INT_INJ, INT_POS] THEN
+  CONV_TAC(LAND_CONV(ONCE_DEPTH_CONV SYM_CONV)) THEN
+  REWRITE_TAC[SELECT_REFL]
+QED
+
+Theorem NUM_OF_NEG_INT[simp,compute]:
+  !n. Num(-&n) = n
+Proof
+  GEN_TAC THEN
+  REWRITE_TAC[Num, INT_INJ, INT_POS, INT_EQ_NEG] THEN
+  Cases_on ‘0 <= -&n’ THEN ASM_REWRITE_TAC [] THEN
+  CONV_TAC (RATOR_CONV (ONCE_REWRITE_CONV [EQ_SYM_EQ])) THEN
+  REWRITE_TAC [SELECT_REFL] THEN
+  POP_ASSUM MP_TAC THEN
+  REWRITE_TAC [INT_NEG_GE0,INT_LE,LE] THEN
+  STRIP_TAC THEN ASM_REWRITE_TAC [INT_NEG_0,INT_INJ] THEN
+  REWRITE_TAC [SELECT_REFL]
+QED
+
+Theorem INT_OF_NUM[simp]:
+  !i. (&(Num i) = i) <=> 0 <= i
+Proof
+  GEN_TAC THEN EQ_TAC THEN1
+   (DISCH_THEN(SUBST1_TAC o SYM) THEN MATCH_ACCEPT_TAC INT_POS) THEN
+  DISCH_THEN(ASSUME_TAC o EXISTENCE o MATCH_MP NUM_POSINT) THEN
+  REWRITE_TAC[Num] THEN CONV_TAC SYM_CONV THEN
+  POP_ASSUM STRIP_ASSUME_TAC THEN
+  ASM_REWRITE_TAC [INT_POS,INT_INJ] THEN
+  CONV_TAC (RAND_CONV (ONCE_REWRITE_CONV [EQ_SYM_EQ])) THEN
+  REWRITE_TAC [SELECT_REFL]
+QED
+
+Theorem NUM_EQ0[simp]:
+  Num i = 0 <=> i = 0
+Proof
+  Cases_on ‘i’ >> simp[]
+QED
+
+Theorem Num_EQ:
+  Num a = Num b <=> a=b \/ a=-b
+Proof
+  Cases_on ‘a’ >> Cases_on ‘b’ >> simp[]
+QED
 
 val LE_NUM_OF_INT = store_thm
   ("LE_NUM_OF_INT",
@@ -3500,9 +3513,9 @@ val _ = BasicProvers.export_rewrites
          "INT_DIVIDES_RADD", "INT_DIVIDES_REFL", "INT_DIVIDES_RMUL",
          "INT_DIVIDES_RSUB", "INT_DIV", "INT_QUOT", "INT_DIV_1",
          "INT_QUOT_1", "INT_DIV_ID", "INT_QUOT_ID", "INT_DIV_NEG",
-         "INT_QUOT_NEG", "INT_ENTIRE", "INT_EQ_CALCULATE",
+         "INT_QUOT_NEG", "INT_ENTIRE",
          "INT_EQ_LADD", "INT_EQ_LMUL", "INT_EQ_RADD", "INT_EQ_LMUL",
-         "INT_EXP", "INT_EXP_EQ0", "INT_INJ", "INT_LE", "INT_LE_ADD",
+         "INT_EXP", "INT_EXP_EQ0", "INT_LE", "INT_LE_ADD",
          "INT_LE_ADDL", "INT_LE_ADDR", "INT_LE_DOUBLE", "INT_LE_LADD",
          "INT_LE_MUL", "INT_LE_NEG", "INT_LE_NEGL", "INT_LE_NEGR",
          "INT_LE_RADD", "INT_LE_SQUARE", "INT_LT_ADD",

diff --git a/src/rational/ratScript.sml b/src/rational/ratScript.sml
@@ -2608,32 +2608,7 @@ val rat_of_int_def = Define ‘
 Theorem rat_of_int_11[simp]:
   (rat_of_int i1 = rat_of_int i2) <=> (i1 = i2)
 Proof
-  simp[EQ_IMP_THM] >> simp[rat_of_int_def] >> Cases_on ‘i1 < 0’ >>
-  Cases_on ‘i2 < 0’ >> simp[]
-  >- (‘0 <= -i1 /\ 0 <= -i2’ by simp[] >>
-      rpt (pop_assum
-             (mp_tac o CONV_RULE (REWR_CONV (GSYM integerTheory.INT_OF_NUM))))>>
-      ntac 2 strip_tac >> disch_then (mp_tac o AP_TERM ``$& : num -> int``) >>
-      ntac 2 (pop_assum SUBST1_TAC) >> simp[integerTheory.INT_EQ_CALCULATE])
-  >- (rename [‘a < 0’, ‘~(b < 0)’] >>
-      ‘0 <= -a /\ 0 <= b’ by (simp[] >> fs[integerTheory.INT_NOT_LT]) >>
-      rpt (pop_assum
-             (mp_tac o CONV_RULE (REWR_CONV (GSYM integerTheory.INT_OF_NUM))))>>
-      ntac 2 strip_tac >>
-      disch_then (CONJUNCTS_THEN (mp_tac o AP_TERM ``$& : num -> int``)) >>
-      ntac 2 (pop_assum SUBST1_TAC) >> simp[integerTheory.INT_EQ_CALCULATE])
-  >- (rename [‘a < 0’, ‘~(b < 0)’] >>
-      ‘0 <= -a /\ 0 <= b’ by (simp[] >> fs[integerTheory.INT_NOT_LT]) >>
-      rpt (pop_assum
-             (mp_tac o CONV_RULE (REWR_CONV (GSYM integerTheory.INT_OF_NUM))))>>
-      ntac 2 strip_tac >>
-      disch_then (CONJUNCTS_THEN (mp_tac o AP_TERM ``$& : num -> int``)) >>
-      ntac 2 (pop_assum SUBST1_TAC) >> simp[integerTheory.INT_EQ_CALCULATE])
-  >- (‘0 <= i1 /\ 0 <= i2’ by fs[integerTheory.INT_NOT_LT] >>
-      rpt (pop_assum
-             (mp_tac o CONV_RULE (REWR_CONV (GSYM integerTheory.INT_OF_NUM))))>>
-      ntac 2 strip_tac >> disch_then (mp_tac o AP_TERM ``$& : num -> int``) >>
-      ntac 2 (pop_assum SUBST1_TAC) >> simp[integerTheory.INT_EQ_CALCULATE])
+  Cases_on ‘i1’ >> Cases_on ‘i2’ >> simp[rat_of_int_def]
 QED
 
 Theorem rat_of_int_of_num[simp]: rat_of_int (&x) = &x