tgoal

Defn.tgoal : defn -> proofs

Set up a termination proof.

tgoal defn sets up a termination proof for the function represented by defn. It creates a new goalstack and makes it the focus of subsequent goalstack operations.

Failure

tgoal defn fails if defn represents a non-recursive or primitive recursive function.

Example

> val qsort_defn =
   Hol_defn "qsort"
      `(qsort ___ [] = []) /\
       (qsort ord (x::rst) =
           APPEND (qsort ord (FILTER ($~ o ord x) rst))
             (x :: qsort ord (FILTER (ord x) rst)))`;
<<HOL message: inventing new type variable names: 'a>>
val qsort_defn =
   HOL function definition (recursive)
   
   Equation(s) :
    [...] ⊢ qsort v0 [] = []
    [...]
   ⊢ qsort ord (x::rst) =
     qsort ord (FILTER ($¬ ∘ ord x) rst) ⧺ x::qsort ord (FILTER (ord x) rst)
   
   Induction :
    [...]
   ⊢ ∀P. (∀v0. P v0 []) ∧
         (∀ord x rst.
            P ord (FILTER (ord x) rst) ∧ P ord (FILTER ($¬ ∘ ord x) rst) ⇒
            P ord (x::rst)) ⇒
         ∀v v1. P v v1
   
   Termination conditions :
     0. ∀rst x ord. R (ord,FILTER (ord x) rst) (ord,x::rst)
     1. ∀rst x ord. R (ord,FILTER ($¬ ∘ ord x) rst) (ord,x::rst)
     2. WF R: DefnBase.defn

> Defn.tgoal qsort_defn;
val it =
   Proof manager status: 1 proof.
   1. Incomplete goalstack:
        Initial goal:
        ∃R. WF R ∧ (∀rst x ord. R (ord,FILTER (ord x) rst) (ord,x::rst)) ∧
            ∀rst x ord. R (ord,FILTER ($¬ ∘ ord x) rst) (ord,x::rst)

See also

TotalDefn.WF_REL_TAC, Defn.tprove, Defn.Hol_defn