Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.4); Sun, 10 Jan 1993 23:18:22 +0000
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA17770;
          Sun, 10 Jan 93 14:51:52 -0800
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA17765;
          Sun, 10 Jan 93 14:51:38 -0800
Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.4) to cl; Sat, 9 Jan 1993 14:11:12 +0000
To: weiss@edu.uidaho.cs.leopard (P. Andrew Weiss)
Cc: info-hol@edu.uidaho.cs.ted (HOL mailing list)
Subject: Re: Quick help
In-Reply-To: Your message of Fri, 08 Jan 93 13:36:57 -0800. <9301082136.AA15131@leopard.cs.uidaho.edu>
Date: Sat, 09 Jan 93 14:11:07 +0000
From: John Harrison <John.Harrison@uk.ac.cam.cl>
Message-Id: <"swan.cl.ca.178:09.01.93.14.11.15"@cl.cam.ac.uk>


You write:

> Anyone know a quick and easy way to prove the following goal?
> 
> g("!n. ~((SUC n) MOD (SUC(SUC 0) = n)");;
> 
> I'm running up against a mental block, as I always seem to do
> when I try to prove anything with DIV and MOD.
> 
> Phil.

Yes, I often find things involving DIV and MOD surprisingly awkward. I think 
there's probably a need for more built-in theorems.

Anyway, here is what I first thought of -- very inelegant but it works.

  load_library `reduce`;;
  
  let th = PROVE
   ("!n. ~((SUC n) MOD (SUC(SUC 0)) = n)",
    let lemma = (CONJUNCT2 o SPEC "SUC n" o MATCH_MP DIVISION o EQT_ELIM)
      (REDUCE_CONV "0 < SUC(SUC 0)") in
    GEN_TAC THEN DISJ_CASES_TAC(REWRITE_RULE[LESS_THM; NOT_LESS_0] lemma) THEN
    ASM_REWRITE_TAC[] THEN DISCH_THEN(SUBST_ALL_TAC o SYM) THEN
    POP_ASSUM MP_TAC THEN REDUCE_TAC);;

John.