I'd like to write down some definitions (and prove some lemmas!) about paths in a graph. Let's say that the graph is given implicitly by a relation of type 'a => 'a => bool
. To talk about a possibly infinite path in the graph, I thought a sensible thing was to use a lazy list codatatype like 'a llist
as given in "Defining (Co)datatypes and Primitively (Co)recursive Functions in Isabelle/HOL" (datatypes.pdf
in the Isabelle distribution).
This works well enough, but I'd then I'd like to define a predicate that takes such a list and a graph relation and evaluates to true iff the list defines a valid path in the graph: any pair of adjacent entries in the list must be an edge.
If I was using 'a list
as a type to represent the paths, this would be easy: I'd just define the predicate using primrec
. However, the co-inductive definitions I can find all seem to generate or consume the data one element at a time, rather than being able to make a statement about the whole thing. Obviously, I realise that the resulting predicate won't be computable (because it is making a statement about infinite streams), so it might have a \forall in there somewhere, but that's fine - I want to use it for developing a theory, not generating code.
How can I define such a predicate? (And how could I prove the obvious associated introduction and elimination lemmas that make it useful?)
Thanks!