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

```[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
```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.