> On 5 Mar 2016, at 09:01, Ramana Kumar <ramana.ku...@cl.cam.ac.uk> wrote: > > I think RW_TAC doesn't handle conditional rewrites very well. Try using rw or > simp instead. >
RW_TAC handles conditional rewrites in exactly the same way as simp and rw. If I try RW_TAC list_ss [cx_length] with the repository version of HOL, it solves the goal. I turned the simplifier trace on to see the following steps taken: [953932]: rewriting LENGTH (cx l p q) with |- LENGTH p = LENGTH q ⇒ LENGTH (cx l p q) = LENGTH p [970795]: rewriting LENGTH p with [.] |- LENGTH p = LENGTH q [986129]: rewriting LENGTH q = LENGTH q with |- x = x ⇔ T [2857]: rewriting LENGTH p with [.] |- LENGTH p = LENGTH q [20122]: LENGTH q ≤ n via cache hit! simplifies to: T [36570]: rewriting LENGTH p = LENGTH q ∧ LENGTH p ≤ n ⇒ T with |- t ⇒ T ⇔ T val it = Initial goal proved. |- ∀p q n l. LENGTH p = LENGTH q ∧ LENGTH p ≤ n ⇒ LENGTH (cx l p q) ≤ n: proof ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. ------------------------------------------------------------------------------ _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
