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:00:53 +0100
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA28184;
          Thu, 28 Jul 1994 03:46:38 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Received: from irafs1.ira.uka.de by leopard.cs.byu.edu 
          with SMTP (1.37.109.8/16.2) id AA28180;
          Thu, 28 Jul 1994 03:46:24 -0600
Received: from i80fs2.ira.uka.de (actually i80fs2) by irafs1 with SMTP (PP);
          Thu, 28 Jul 1994 11:36:37 +0200
Received: from ira.uka.de by i80fs2.ira.uka.de id <10944-0@i80fs2.ira.uka.de>;
          Thu, 28 Jul 1994 11:44:04 +0200
Date: Thu, 28 Jul 94 11:44:03 EDT
From: reetz <reetz@ira.uka.de>
To: info-hol@leopard.cs.byu.edu
Cc: schneide@ira.uka.de
Subject: problems with prove_induction_thm in hol90.6
Message-Id: <"i80fs2.ira.946:28.06.94.09.44.10"@ira.uka.de>

Using hol90.6, I ran into the following error during
some type definition:



new_theory "test";

val test_thm =
 define_type
  {fixities = [Prefix,Prefix],
   name     = "test",
   type_spec= `test = test1 of 'M               |
                      test2 of test => ('M->'M) `};

- test_thm;
val it =
  |- !f0 f1.
       ?!fn.
         (!x. fn (test1 x) = f0 x) /\ (!t f. fn (test2 t f) = f1 (fn t) f t)
  : thm

(prove_induction_thm test_thm;()) handle e => print_HOL_ERR e;

Exception raised at Rec_type_support.prove_induction_thm:
 
val it = () : unit




Now, I tried a simpler type definition to see what went wrong:

val btest_thm =
 define_type
  {fixities = [Prefix,Prefix],
   name     = "btest",
   type_spec= `btest = btest1 of 'M    |
                       btest2 of btest `};

- btest_thm;
val it =
  |- !f0 f1.
       ?!fn. (!x. fn (btest1 x) = f0 x) /\ (!b. fn (btest2 b) = f1 (fn b) b)
  : thm

- (prove_induction_thm btest_thm;()) handle e => print_HOL_ERR e;
val it = () : unit

- prove_induction_thm btest_thm;
val it = |- !P. (!x. P (btest1 x)) /\ (!b. P b ==> P (btest2 b)) ==> (!b. P b)
  : thm



Now I'm not sure about what happened. Is the first type definition I
would like to do somewhat wrong or is it a bug in prove_induction_thm?

Ralf.


(********************************************************)
(*                                                      *)
(*  Ralf Reetz                                          *)
(*                                                      *)
(*  University of Karlsruhe                             *)
(*  Institut fuer Rechnerentwurf und Fehlertoleranz     *)
(*  76128 Karlsruhe, Zirkel 2, Postfach 6980, Germany   *)
(*                                                      *)
(*  e-mail: reetz@ira.uka.de                            *)
(*  WWW:    http://goethe.ira.uka.de/people/reetz.html  *)
(*                                                      *)
(********************************************************)