*To*: John Wickerson <johnwickerson at cantab.net>, isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] lemma about finitely-branching finite sequences*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Tue, 17 Jun 2014 08:09:21 +0200*In-reply-to*: <7AAE3AE6-9B49-4CA8-B66E-3AA6FCC2DFBA@cantab.net>*References*: <1C7BDD54-2FF5-4A84-8DE1-DF0FCA3F05CB@cantab.net> <539EE9AD.3060000@inf.ethz.ch> <6AAC6B40-BD95-45E6-B741-7289C48763F5@cantab.net> <539F13D7.9050404@inf.ethz.ch> <7AAE3AE6-9B49-4CA8-B66E-3AA6FCC2DFBA@cantab.net>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.5.0

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?

Best, Andreas

**References**:**[isabelle] lemma about finitely-branching finite sequences***From:*John Wickerson

**Re: [isabelle] lemma about finitely-branching finite sequences***From:*Andreas Lochbihler

**Re: [isabelle] lemma about finitely-branching finite sequences***From:*John Wickerson

**Re: [isabelle] lemma about finitely-branching finite sequences***From:*Andreas Lochbihler

- Previous by Date: [isabelle] HART (Haskell and Rewriting Techniques) 2014 -- Last Call for Papers
- Next by Date: Re: [isabelle] using AFP
- Previous by Thread: Re: [isabelle] lemma about finitely-branching finite sequences
- Next by Thread: [isabelle] HART (Haskell and Rewriting Techniques) 2014 -- Last Call for Papers
- Cl-isabelle-users June 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list