Add |- transitive $< as an automatic rewrite to aritmeticTheory

HOL-Theorem-Prover · May 12, 2014 · 908fecc · 908fecc
1 parent 17aa113
commit 908fecc
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 4 deletions.
diff --git a/src/enumfset/totoScript.sml b/src/enumfset/totoScript.sml
@@ -622,10 +622,8 @@ REWRITE_TAC [pre_aplextoto]);
 
 val StrongLinearOrder_LESS = maybe_thm ("StrongLinearOrder_LESS",
 ``StrongLinearOrder ($< :num reln)``,
-SRW_TAC [] [StrongLinearOrder, StrongOrder_ALT,
-trichotomous, Order, irreflexive_def, transitive_def] THENL
-[IMP_RES_TAC LESS_TRANS
-,STRIP_ASSUME_TAC (Q.SPECL [`a`, `b`] LESS_LESS_CASES) THEN AR]);
+SRW_TAC [ARITH_ss] [StrongLinearOrder, StrongOrder_ALT,
+                    trichotomous, Order, irreflexive_def]);
 (* ******
 val StrongWellOrder_LESS = maybe_thm ("StrongWellOrder_LESS",
  Term`StrongWellOrder ($< :num reln)`,

diff --git a/src/num/theories/arithmeticScript.sml b/src/num/theories/arithmeticScript.sml
@@ -328,6 +328,12 @@ val LESS_TRANS = store_thm ("LESS_TRANS",
     THENL [SUBST_TAC[SYM(ASSUME (``n:num = p``))], ALL_TAC]
     THEN ASM_REWRITE_TAC[]);
 
+val transitive_LESS = store_thm(
+  "transitive_LESS[simp]",
+  ``transitive $<``,
+  REWRITE_TAC [relationTheory.transitive_def] THEN
+  MATCH_ACCEPT_TAC LESS_TRANS);
+
 val LESS_ANTISYM = store_thm ("LESS_ANTISYM",
    ``!m n. ~((m < n) /\ (n < m))``,
    REPEAT STRIP_TAC