Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
Message-Id: <199509171334.HAA22687@bunsen.cs.byu.edu>
To: Phil Windley <windley@cs.byu.edu>
Cc: info-hol@cs.byu.edu, tfm@dcs.gla.ac.uk
Subject: Re: generalized induction tactic
In-Reply-To: Your message of "Fri, 15 Sep 1995 17:24:42 MDT." <199509152324.AA044157482@bobcat.cs.byu.edu>
Date: Sun, 17 Sep 1995 14:35:00 +0100
From: Tom Melham <tfm@dcs.gla.ac.uk>


> Taking a little cue from something that was mentioned at the HOL meeting, I
> came back and cobbled together a generalized induction tactic.   ...
> ...
> Comments?

Well, I could suggest an improvement to the code:

>     let GEN_INDUCT_TAC var (asl,go) =
>         let (_,tp) = dest_var var in
>         let ind_thm = induct_lookup tp in
>         is_forall go => (
>            let (vars,_) = strip_forall go in
>            (mem var vars) =>
>     	   (REPEAT (FILTER_GEN_TAC var)
>     	    THEN (INDUCT_THEN ind_thm STRIP_ASSUME_TAC)) (asl,go) 
>            |
>     	   (SPEC_TAC (var,var) 
>                 THEN (INDUCT_THEN ind_thm STRIP_ASSUME_TAC)) (asl,go))
>         |
>            (SPEC_TAC (var,var) 
>             THEN (INDUCT_THEN ind_thm STRIP_ASSUME_TAC)) (asl,go);;

The function 

   INDUCT_THEN : thm -> thm_tactic -> tactic

is written so that it eagerly does some computation when applied
to an induction theorem -- in order to produce a faster tactic.
For example, in HOL88:

   #INDUCT_THEN list_INDUCT;;
   - : (thm_tactic -> tactic)
   Run time: 0.0s
   Intermediate theorems generated: 22

The number of intermediate theorems is trivial in this case, but
gets a lot larger for big recursive types. In general,

   INDUCT_THEN <induction-theorem-for-:ty>

computes a `fast' tactic function of type thm_tactic -> tactic
for doing induction on type :ty (e.g., it knows where to do beta-
reductions).  The problem with the above code is that GEN_INDUCT_TAC 
doesn't do this computation ahead of time and once-and-for-all. Instead,
it does it each time you want to do an induction.

I would suggest a table with pre-computed tactics for each type.

Tom