Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Thu, 28 Jul 1994 11:53:12 +0100
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA28492;
          Thu, 28 Jul 1994 04:48:56 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Received: from vanuata.dcs.gla.ac.uk by leopard.cs.byu.edu 
          with SMTP (1.37.109.8/16.2) id AA28488;
          Thu, 28 Jul 1994 04:48:52 -0600
Received: from hawaii.dcs.gla.ac.uk by goggins.dcs.gla.ac.uk 
          with LOCAL SMTP (PP) id <23258-0@goggins.dcs.gla.ac.uk>;
          Thu, 28 Jul 1994 11:43:51 +0100
Received: by hawaii.dcs.gla.ac.uk (4.1/Dumb) id AA25987;
          Thu, 28 Jul 94 11:43:47 BST
From: tfm <tfm@dcs.gla.ac.uk>
Message-Id: <9407281043.AA25987@hawaii.dcs.gla.ac.uk>
To: reetz <reetz@ira.uka.de>
Cc: info-hol@leopard.cs.byu.edu, schneide@ira.uka.de, tfm@dcs.gla.ac.uk
Subject: Re: problems with prove_induction_thm in hol90.6
In-Reply-To: Your message of "Thu, 28 Jul 94 11:44:03 EDT." <"i80fs2.ira.946:28.06.94.09.44.10"@ira.uka.de>
Date: Thu, 28 Jul 94 11:43:46 +0100


Further to my recent message, see the attached changes log entry from
the latest (unreleased) hol90.  My guess is that this will fix the bug.

Tom

=====================================================================

48. Fixed a bug in Rec_type_support.prove_induction_thm, noticed by La
    Bella Maurizio. Frustratingly, this bug had been fixed in hol88, but 
    not recorded on the Versions file. Anyway, at approximately line 310 of 
    src/2/rec_type_support.sml, there is a function "mk_fn" defined. This is 
    a local function to the function "prove_induction_thm". Replace the 
    definition of "mk_fn" with the following:

        fun mk_fn P ty tm = 
           let val {lhs,rhs} = dest_eq(snd(strip_forall tm))
               val c = rand lhs
               val args = snd(strip_comb rhs)
               val vars = filter is_var args
               val n = length(filter (fn t => type_of t = ty) vars)
           in if (n=0) 
              then list_mk_abs (vars, tr)
              else let val bools = gen n
                       val term = mk_disj{disj1 = list_mk_conj bools,
                                          disj2 = mk_comb{Rator = P, Rand = c}}
                   in list_mk_abs((bools@vars),term)
                   end
           end