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

Hi John, On 16/06/14 16:48, John Wickerson wrote:

Thanks very much for your reply Andreas. I had actually tried the idea of using "well-foundedness of ↝ restricted to the states reachable from C", but couldn't make it work. I've just tried it again, encouraged by your suggestion, but I'm still struggling. Specifically, I'm phrasing my lemma like this (↝* is an abbreviation I defined for the reflexive transitive closure of ↝):lemma assumes "wf {(C2,C1). C ↝* C1 ∧ C1 ↝ C2}" shows "finite (traces C)"I use wf_induct:proof (rule wf_induct[OF assms])That reduces the problem to the following (I've made the assumption slightly more readable):fix C1 assume 1: "∀C2. C ↝* C1 ∧ C1 ↝ C2 ⟶ finite (traces C2)" show "finite (traces C1)"My specific problem is that before I can exploit fact "1", I need to show that C1 is indeed reachable from C. I simply don't have that fact anywhere!

lemma assumes "wf {(C2,C1). C ↝* C1 ∧ C1 ↝ C2}" and "C ↝* C1" shows "finite (traces C1)" using assms proof(induction C1 rule: wf_induct_rule)

Do you have any further tips that might help me? Many many thanks!

Andreas

On 16 Jun 2014, at 13:57, Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch> wrote:Hi John, On 16/06/14 14:00, John Wickerson wrote:I have a relation "↝" representing the reductions of a small-step operational semantics. By construction, every configuration can only reduce to finitely-many next configurations. Given an initial configuration C, I would like to prove that if every execution starting from C gets stuck after a finite number of steps, then there are only finitely-many executions of C0. I'm having quite a bit of difficulty getting my head round how to prove this. I can do it if I assume that the entire "↝" relation is well-founded, but that's too strong an assumption,Your assumption is that all executions starting in C eventually get stuck. You can prove that this is equivalent to the well-foundedness of ↝ restricted to the states reachable from C. Then, you can use well-founded induction to show finiteness, probably similar to what you already have. To show well-foundedness, you can take the length of the longest execution starting in a state as measure function. Hope this helps, Andreas since I need it to be possible for *some* executions to diverge, just not those that start from C.I have a sense that my lemma, if it is indeed true, will have been proven before, perhaps in the context of graph theory, or computability theory. I'd really appreciate any hints the Isabelle community might have for how I might prove this, or where/whether it has already been proven. Thanks! John ps. In case more precision is appropriate... I'm defining executions like this:definition executions :: "config ⇒ (nat ⇒ config option) set" where "executions C ≡ {π. π 0 = Some C ∧ (∀i. case π i of None ⇒ π (i+1) = None | Some C ⇒ if reduce C=[] then π (i+1) = None else π (i+1) ∈ Some ` set (reduce C))}"and my lemma is:lemma assumes "∀π ∈ executions C. ∃i > 0. finite_seq i π" shows "finite (executions C)"and I define finite_seq like so:fun finite_seq where "finite_seq 0 π = (∀i. π i = None)" | "finite_seq (Suc i) π = (π 0 ≠ None ∧ finite_seq i (λi. π (Suc i)))"

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

**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

- Previous by Date: Re: [isabelle] lemma about finitely-branching finite sequences
- Next by Date: Re: [isabelle] using AFP
- Previous by Thread: Re: [isabelle] lemma about finitely-branching finite sequences
- Next by Thread: Re: [isabelle] lemma about finitely-branching finite sequences
- 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