[isabelle] Recursion on finite, lazy lists (llists)

["Denis Bueno" <dbueno at gmail.com>]

[The following is all in context of the LList2 library, available from afp.]

During the course of a proof I attempt to ensure that a finite llist
does not have any of a certain element.  After many unsuccessful
attempts at actual pattern matching using LNil and LCons (using fun
and primrec) I finally saw the definition of llength in LList2.thy:

    constdefs
    llength :: "'a llist => nat"
    "llength == finlsts_rec 0 (λ a r n. Suc n)"

This uses the completely opaque (to me) `finlsts_rec' operator.  I
gather the following from its uses:

    - 0 is the base case; if the list is LNil, 0 is returned
    - a is the current element of the list
    - r is the rest of the list
    - n is the current "accumulator state"
    - it has some special magic for telling Isabelle it will only deal
with finite llists

These observations lead me to the following definition, `noBot'
(mnemonic: "no bottom state"):

    constdefs
      noBot :: "state llist => bool"
      "noBot == finlsts_rec True (% s r b. b & (s ~= BottomState))"

As a sanity check, I try to prove that "noBot LNil = True":

    lemma
    "noBot LNil = True" unfolding noBot_def using finlsts_rec_LNil
(*here*) by blast

When ProofGeneral has consumed everything up to "(*here*)", the
proofstate looks like:

    using this:
      finlsts_rec ?c ?d LNil = ?c

    goal (1 subgoal):
     1. finlsts_rec True (%s r b. b & s ~= BottomState) LNil = True

This looks like it can be proved directly by unification.  Consuming
the blast does not prove the theorem, even after a long time.

What exactly is going on here?

-- 
 Denis