*To*: Andreas Lochbihler <mail at andreas-lochbihler.de>*Subject*: Re: [isabelle] Coinduction on predicate defined wrt other coinductive predicates*From*: "C.A. Watt" <caw77 at cam.ac.uk>*Date*: Thu, 21 Jun 2018 14:24:39 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <2fd891e9-ab5d-7ca8-c55d-595ea4a30e8c@andreas-lochbihler.de>*References*: <2406db85f3189eb71867e27e6bcb2c84@cam.ac.uk> <2fd891e9-ab5d-7ca8-c55d-595ea4a30e8c@andreas-lochbihler.de>*User-agent*: Roundcube Webmail/1.0.12

Hi Andreas

Thanks again for your help! Best wishes Conrad On 2018-06-19 21:47, Andreas Lochbihler wrote:

Dear Conrad, Let me first summarize how I understand your abstract example. transition describes a transition system between states, and state_abs is an abstraction function on states. abs_equiv is a relation on abstract states (possibly an equivalence relation). The relation abs_trace associates with a start state all complete runs of the transition system starting in this state, as a sequence of abstracted states. P is then the relation composition of the abs_trace relation with the lifted abs_equiv relation. All the functions and predicates in here are "primitively corecursive" in that they only peel off one constructor at a time. So you don't need coinduction upto friends here. I'd recommend to actually split the abs_trace definition into two. (Warning: I haven't worked out the following in detail; it's just a sketch.) 1. Define a relation "trace" from states to complete runs of concrete states. Then prove that trace s l' ==> EX l. abs_trace s l & l = lmap state_abs l' and abs_trace s l ==> EX l'. trace s l' & l = lmap state_abs l' For the second implication, you want to define a primitively recursive function that construct a concrete run from an abstract run using Hilbert choice. In my AFP entry JinjaThreads, the theory LTS provides a bunch of examples in a similar context, e.g., the lemma Runs_into_Runs_table. 2. The property l = lmap state_abs l' is equivalent to saying "llist_all2 (BNF_Def.Grp UNIV state_abs) l l'". So we have P s l ==> EX l'. trace s l' &(llist_all2 (BNF_Def.Grp UNIV state_abs) OO llist_all2 abs_equiv) ll'and vice versa.3. Now, the crucial bit is the lemma llist.rel_Grp. With that, you cantransformllist_all2 (BNF_Def.Grp UNIV state_abs) OO llist_all2 abs_equiv into llist_all2 (BNF_Def.Grp UNIV state_abs OO abs_equiv) i.e., the equivalence closure of the abstraction function. With that characterisation, you should be able to prove a suitable coinduction rule for starting from trace's. As I mentioned earlier, my theory LTS in JinjaThreads does many such hops (except for the llist.rel_Grp part), so you may go and look for some inspiration there. Hope this helps, Andreas

**References**:**[isabelle] Coinduction on predicate defined wrt other coinductive predicates***From:*C.A. Watt

**Re: [isabelle] Coinduction on predicate defined wrt other coinductive predicates***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] 1/0=0
- Next by Date: Re: [isabelle] datatype_compat in Isabelle2018-RC0
- Previous by Thread: Re: [isabelle] Coinduction on predicate defined wrt other coinductive predicates
- Next by Thread: Re: [isabelle] [FOM] 820: Sugared ZFC Formalization/2
- Cl-isabelle-users June 2018 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