Re: [isabelle] lemma about finitely-branching finite sequences



Hi John,

I've started thinking about how to obtain the wf assumption, using the wf_measure approach you suggest. I haven't got far enough yet to know if it will definitely work or definitely not work, but I just wanted to raise with you an initial concern I have, about the use of "longest_execution" as the measure function. The thing is, if I define longest_execution in the obvious way...

definition longest_execution :: "config ⇒ nat"
where
   "longest_execution C ≡ Max {j . ∃π ∈ traces C. finite_seq j π}"


... then "longest_execution C" is only well-defined if C has only finitely-many executions. (Sorry, I realise I keep switching randomly between "execution" and "trace".) And to show that C has only finitely-many executions, I need the lemma that I'm trying to prove!

In short, I'm worried that there might be some horrible circularity going on here. Does my reasoning make sense to you?
I had the same concern, but I think that you could avoid the circularity by defining the longest execution recursively. However, I meanwhile realised that you can show well-foundedness more easily with the lemma finite_acyclic_wf (without going over the longest execution). Acyclicity of the reachable graph should be easy to show because otherwise, you have a loop and you could construct an infinite execution by looping. For finiteness, you will need something like a Koenig's lemma to go from traces to states (If every node in a connected graph has finitely many successors and there are infinitely many nodes, then there is an infinite path). You can find an example of such a lemma (for an undirected graph) in my AFP entry Coinductive (theory Koenigslemma).

Best,
Andreas




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