Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2);
          Thu, 3 Dec 1992 13:45:08 +0000
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA20481;
          Thu, 3 Dec 92 05:11:10 -0800
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from nene.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA20476;
          Thu, 3 Dec 92 05:10:58 -0800
Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by nene.cl.cam.ac.uk 
          with SMTP (PP-6.3) to cl; Thu, 3 Dec 1992 13:09:59 +0000
To: Wishnu Prasetya <wishnu@nl.ruu.cs>
Cc: info-hol@edu.uidaho.cs.ted (hol mailing list)
Subject: Re: HELP: RES_TAC
In-Reply-To: Your message of Thu, 03 Dec 92 13:41:45 +0700. <199212031241.AA01381@infix.cs.ruu.nl>
Date: Thu, 03 Dec 92 13:09:53 +0000
From: John Harrison <John.Harrison@uk.ac.cam.cl>
Message-Id: <"nene.cl.ca.461:03.12.92.13.10.01"@cl.cam.ac.uk>


Wishnu Prasetya asks:

> Just a small question. Any idea why RES_TAC does not create any new assumption
> in the case below? I would say it should.
> 
>    OK..
>    "WELL_FOUNDED(R 0)"
>        [ "0 < n \/ (0 = n) ==> WELL_FOUNDED(R 0)" ]
>        [ "0 < n \/ (0 = n)" ]
> 
>    () : void
> 
>    #e RES_TAC;;
>    OK..
>    "WELL_FOUNDED(R 0)"
>        [ "0 < n \/ (0 = n) ==> WELL_FOUNDED(R 0)" ]
>        [ "0 < n \/ (0 = n)" ]
> 
>    () : void
> 
>    #

I think the problem arises because the resolution tactics do some
canonicalization using RES_CANON behind the scenes; the implication
you have is split into two separate theorems, neither of which then
matches the disjunction:

  #"0 num_lt n \/ (0 = n) ==> (WELL_FOUNDED:*->bool)(R 0)";;
  "0 num_lt n \/ (0 = n) ==> WELL_FOUNDED(R 0)" : term
  Run time: 0.0s
  
  #ASSUME it;;
  . |- 0 num_lt n \/ (0 = n) ==> WELL_FOUNDED(R 0)
  Run time: 0.0s
  Intermediate theorems generated: 1
  
  #RES_CANON it;;
  [. |- 0 num_lt n ==> WELL_FOUNDED(R 0);
   . |- (0 = n) ==> WELL_FOUNDED(R 0)]
  : thm list
  Run time: 0.1s
  Intermediate theorems generated: 14

I believe that

  FIRST_ASSUM DISJ_CASES_TAC THEN RES_TAC

would work. I would prefer:

  FIRST_ASSUM MATCH_MP_TAC THEN FIRST_ASSUM ACCEPT_TAC

I tend to avoid resolution precisely because it does peculiar
things like this without user control.

John.