*To*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Subject*: Re: [isabelle] lemma about finitely-branching finite sequences*From*: John Wickerson <johnwickerson at cantab.net>*Date*: Mon, 16 Jun 2014 17:21:53 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <539F13D7.9050404@inf.ethz.ch>*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>

Ha, it works! Thanks so much Andreas. I knew I had to generalise the induction hypothesis somehow, but just hadn't massaged the statement into *quite* the right form. John On 16 Jun 2014, at 16:57, Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch> wrote: > 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! > At the moment, your induction predicate is "%C. finite (traces C)". You have to generalise it to arbitrary states reachable from C, i.e., > > 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! > Do not use any of the basic proof rules for wf to establish the well-foundedness assumption. The resulting proof oblications are usually too complicated. Rather show that the relation "{(C2,C1). C ↝* C1 ∧ C1 ↝ C2}" is a subset of "measure f" for some measure function f on states (like the longest execution starting in the state as I suggested in my previous mail). Then, you get well-foundedness from the rules wf_subset and wf_measure. > > 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)))" >>>> >>> >>

**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: Re: [isabelle] using AFP
- 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