Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
From: Wishnu Prasetya <wishnu@nl.ruu.cs>
Message-Id: <199212211537.AA25102@infix.cs.ruu.nl>
Subject: Re: Well founded induction
To: windley@edu.uidaho.cs.panther (Phil Windley)
Date: Mon, 21 Dec 92 16:37:13 MET
Cc: info-hol@edu.uidaho.cs.ted (hol mailing list)
In-Reply-To: <199212190102.AA11158@panther.cs.uidaho.edu>; from "Phil Windley" at Dec 18, 92 5:02 pm

  > Now, I want to prove:
  > 
  > g
  > "! f t.
  >   (f t)  ==>
  >   ? t'' .
  >   (Temp_Abs f t'') = t";;
  > 
  > Essentially, this says that temporal abstraction function, (Temp_Abs f) is
  > a surjection from the nats to the characteristic set of f.  The most
  > straightforward approach seems to be induction on t, but then f is not true
  > of ALL t so mathematical induction won't work. But, (Next f) is well
  > founded and so it seems that well founded induction would.
  > 
  > So, for the question: I've never done well founded induction in HOL, anyone
  > have the right theorem to supply to INDUCT_THEN?  The library on wellorder
  > doesn't seem to apply and I didn't see anything else.

There is a library that contains some basic theorems of well founded relations
available in the update-able contrib pool at

       ftp.cl.cam.ac.uk [128.232.0.56] in directory "hvg/contrib"

The library is called WF, and it should also work for version 2.0.

The library provides the following well-founded principle:

    !P. (!y. (!x. R x y /\ P x) ==> P y) ==> (!x. P x)

For any well founded relation R. So for you to use this principle, you will 
have to show first that your relation < on the time domain is indeed well
founded.

Hope this help.

Wishnu Prasetya


--