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; Wed, 24 Nov 1993 12:10:22 +0000
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA02492;
          Wed, 24 Nov 1993 04:59:25 -0700
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: bulk
Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu 
          with SMTP (1.37.109.8/16.2) id AA02488;
          Wed, 24 Nov 1993 04:59:23 -0700
Received: from Maui.CS.UCLA.EDU by dworshak.cs.uidaho.edu 
          with SMTP (1.37.109.4/16.2) id AA06613; Wed, 24 Nov 93 03:57:08 -0800
Received: from LocalHost.cs.ucla.edu 
          by maui.cs.ucla.edu (Sendmail 5.61d+YP/3.23) id AA20024;
          Wed, 24 Nov 93 03:57:06 -0800
Message-Id: <9311241157.AA20024@maui.cs.ucla.edu>
To: info-hol@cs.uidaho.edu
Subject: General induction
Date: Wed, 24 Nov 93 03:57:05 PST
From: chou@cs.ucla.edu

Lately I had occasions to use general induction, whose current formulation in HOL90 is:

    |- !P. (P 0) /\ (!n. (!m. m < n ==> P m) ==> P n) ==> (!n. P n)

Note that the hypothesis (P 0) is not needed: it is implied by the second hypothesis.
So I rewrote the related proof procedures, which you may find useful.

Cheers,
- Ching Tsun


val STRONG_INDUCT_THM = store_thm ("STRONG_INDUCT_THM",
(--`
  !P. ( !n. (!m. m < n ==> P(m)) ==> P(n) ) ==> ( !n. P(n) )
`--), (
  REPEAT (FILTER_STRIP_TAC (--`n:num`--)) THEN
  Gen_induction.GEN_INDUCT_TAC THENL
  [ RULE_ASSUM_TAC (REWRITE_RULE [NOT_LESS_0] o SPEC (--`0`--)) , RES_TAC ]
)) ;

(*----------------------------------------------------------------------------
  STRONG_INDUCT_RULE : thm -> thm -> thm
  

    A |- !n. (!m. m < n ==> P(m)) ==> P(n)
  ------------------------------------------
                A |- !n. P(n)
----------------------------------------------------------------------------*)

fun STRONG_INDUCT_RULE (thm)=
let
  val {Bvar = n, Body = body1} = (dest_forall (concl thm)) ;
  val {ant = test, conseq = Pn} = (dest_imp body1) ;
  val {Bvar = m, Body = body2} = (dest_forall test) ;
  val ind = (BETA_RULE o SPEC (--` \^n. ^Pn `--) o C EQ_MP STRONG_INDUCT_THM)
  ( ALPHA (--` !P. (! n. (! m. m< n ==> P m) ==> P n) ==> (! n. P n) `--)
          (--` !P. (!^n. (!^m.^m<^n ==> P^m) ==> P^n) ==> (!^n. P^n) `--) ) ;
in
  (MP ind thm)
end ;

(*----------------------------------------------------------------------------
  STRONG_INDUCT_TAC : tactic
  

             A ?- !n. P(n)
  ===================================
    A, (!m. m < n ==> P(m)) ?- P(n)
----------------------------------------------------------------------------*)

fun STRONG_INDUCT_TAC (gl, g) =
let
  val {Bvar = n, Body = Pn} = (dest_forall g) ;
  val n' = (variant ((free_vars g) @ (free_varsl gl)) n) ;
  val Pn' = (subst [{residue = n', redex = n}] Pn) ;
  val m' = (variant (free_vars Pn) (--`m:num`--)) ;
  val Pm' = (subst [{residue = m', redex = n}] Pn) ;
  val asm = (--` !^m'. (^m' < ^n') ==> ^Pm' `--) ;
  fun tfn (thm) = (EQ_MP (ALPHA (concl thm) g) thm) ;
  fun jfn [thm] = (tfn (STRONG_INDUCT_RULE (GEN n' (DISCH asm thm)))) ;
in
  ( [(asm::gl, Pn')] , jfn)
end ;