[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:
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"):
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":
"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:
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and