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:54:20 +0000
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA17809;
          Sun, 10 Jan 93 15:26:13 -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 AA17804;
          Sun, 10 Jan 93 15:26:07 -0800
Received: from guillemot.cl.cam.ac.uk (user tfm (rfc931)) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.4) to cl; Sun, 10 Jan 1993 23:24:00 +0000
To: weiss@edu.uidaho.cs.leopard (P. Andrew Weiss)
Cc: info-hol@edu.uidaho.cs.ted (HOL mailing list), Tom.Melham@uk.ac.cam.cl
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: Sun, 10 Jan 93 23:23:54 +0000
From: Tom Melham <Tom.Melham@uk.ac.cam.cl>
Message-Id: <"swan.cl.ca.179:10.01.93.23.24.03"@cl.cam.ac.uk>


> 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.

I would do a boring case analysis. Use the definition of MOD to prove that

   |- !n. ((SUC n) MOD (SUC(SUC 0)) = SUC 0) \/ ((SUC n) MOD (SUC(SUC 0)) = 0)

That is, in Version 2.01 do:

   load_library `arith`;;
   let thm1 = SPEC "SUC n" (REDUCE_RULE (SPEC "2" DIVISION));;
   let thm2 = CONV_RULE (REDEPTH_CONV num_CONV) (CONJUNCT2 thm1);;
   let thm3 = GEN "n:num" (REWRITE_RULE [NOT_LESS_0;LESS_THM] thm2);;

Now, do the case analysis. The cases are n=0, n=1, or n=SUC(SUC m).
The reduce library deals with the first two:
   
   g "!n. ~((SUC n) MOD (SUC(SUC 0)) = n)";;
   e (GEN_TAC THEN STRUCT_CASES_TAC (SPEC "n:num" num_CASES));;
   e REDUCE_TAC;;
   e (STRUCT_CASES_TAC (SPEC "n':num" num_CASES));;
   e REDUCE_TAC;;

Now use thm3 to do another case analysis:

   e (STRIP_THM_THEN SUBST1_TAC (SPEC "SUC(SUC n)" thm3));;
   e (REWRITE_TAC [GSYM NOT_SUC;INV_SUC_EQ]);;
   e (REWRITE_TAC [GSYM NOT_SUC;INV_SUC_EQ]);;

There is doubtless a better proof...

Tom