Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
Message-Id: <199509152324.AA044157482@bobcat.cs.byu.edu>
To: info-hol@cs.byu.edu
Subject: generalized induction tactic
Date: Fri, 15 Sep 1995 17:24:42 -0600
From: Phil Windley <windley@cs.byu.edu>


Taking a little cue from something that was mentioned at the HOL meeting, I
came back and cobbled together a generalized induction tactic.  The tactic
takes a varible to induct on as its sole argument.  The correct induction
lemma is chosen from a table and the induction is done.  The varialbe need
not be in the universally quantified variables to work.    If people like
this sort of thing, the code for define_type could be changed to
automagically install induction theorems in the table.  installing them
when theories are loaded would be trickier since there's no way to tag the
induction lemma in the theory.  Some hueristics would have to be used to
pick out the induction lemma.

Comments?

--phil--

%----------------------------------------------------------------

    GEN_INDUCT_TAC

    Phil Windley <URL: http://lal.cs.byu.edu/people/windley>

    Generalized induction tactic that uses a table mapping types 
    to induction lemmas to do the right kind of induction on a \
    named variable.

    New mappings can be added using the funtion install_induct_thm:
    
            install_induct_thm(":num",INDUCTION);;

    Named variable does not have to be in the universally quantified
    variables to work.

----------------------------------------------------------------%

letref induct_thm_table = ([]:(type#thm)list);;

induct_thm_table := ([]:(type#thm)list);;

induct_thm_table;;

let install_induct_thm (tp, tm) = 
    (induct_thm_table := (tp,tm).induct_thm_table);;

install_induct_thm(":num",INDUCTION);;

install_induct_thm(":(*)list",list_INDUCT);;


let induct_lookup tp = 
    let error_str = `Induction lemma for type not defined, use install_induct_thm to install lemma` in
    let match_types (tp1,tp2) = 
           ((match (mk_var(`foo`,tp1)) 
                   (mk_var(`foo`,tp2)));true) ? false in
    letrec aux tbl = 
       (null tbl) => failwith error_str
             | match_types (fst (hd tbl),tp) => (snd (hd tbl)) 
                                             | aux (tl tbl) in
    aux induct_thm_table;;


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);;
       

%<----------------------------------------------------------------


% simple minded induction on number %
g "! m n p . n + (m + p) = (n + m) + p";;

e(GEN_INDUCT_TAC "p:num");;


% induction on list %
g "! n (l:(*)list) (f:*->**) . f(EL n l) = EL n (MAP f l)";;

e(GEN_INDUCT_TAC "l:(*)list");;


% note that var listed on GEN_INDUCT_TAC must match %
g "! n (l:(num)list) (f:num->**) . f(EL n l) = EL n (MAP f l)";;

e(GEN_INDUCT_TAC "l:(*)list");;


% works without a universally quantified var %
g "n + (m + p) = (n + m) + p";;

e(GEN_INDUCT_TAC "p:num");;

% works with some universally quantified vars %
g "!n m . n + (m + p) = (n + m) + p";;

e(GEN_INDUCT_TAC "p:num");;

% ignores vars that aren't present %
g "!n m . n + (m + p) = (n + m) + p";;

e(GEN_INDUCT_TAC "l:num");;


% ignores vars that aren't present %
g "!n m (l:num). n + (m + p) = (n + m) + p";;

e(GEN_INDUCT_TAC "l:num");;

---------------------------------------------------------------->%