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



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)))"
>>>> 
>>> 
>> 





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