Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Message-Id: <199212190102.AA11158@panther.cs.uidaho.edu>
To: info-hol@edu.uidaho.cs.ted
Subject: Well founded induction
Date: Fri, 18 Dec 92 17:02:12 -0800
From: Phil Windley <windley@edu.uidaho.cs.panther>


I'm trying to prove something (which is obviously true... ;-) and I seem to
need wel founded induction. Basically, its a theorem about a temporal
abstraction function (ala Melham, Herbert, Joyce, etc.)  Here are the
definitions:

let First = new_definition
   (`First`,
    "! g t. First g t = 
        (!p:time. p < t ==> ~(g p)) /\
        (g t)"
   );;

let Next = new_definition
   (`Next`,
    "! g t1 t2. Next g (t1,t2) = 
        (t1 < t2) /\ 
        (!t:time . t1 < t /\ t < t2 ==> ~(g t)) /\
        (g t2)"
   );;

let Temp_Abs = new_prim_rec_definition
   (`Temp_Abs`,
    "(Temp_Abs g 0 = @ t:time . First g t) /\
     (Temp_Abs g (SUC n) = @ t:time . Next g (Temp_Abs g n,t))"
   );;

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.

--phil--