From 908fecc44772e9bddf868a114ac575f9e42b7b42 Mon Sep 17 00:00:00 2001
From: Michael Norrish <michael.norrish@nicta.com.au>
Date: Mon, 12 May 2014 15:42:05 +1000
Subject: [PATCH] Add |- transitive $< as an automatic rewrite to
 aritmeticTheory

---
 src/enumfset/totoScript.sml           | 6 ++----
 src/num/theories/arithmeticScript.sml | 6 ++++++
 2 files changed, 8 insertions(+), 4 deletions(-)

diff --git a/src/enumfset/totoScript.sml b/src/enumfset/totoScript.sml
index 4b02c7f9d4..6dabe108eb 100644
--- 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
index d9f971fe6e..dc2217adc7 100644
--- 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