# Re: [isabelle] Coinduction on predicate defined wrt other coinductive predicates

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) l l'
and vice versa.
3. Now, the crucial bit is the lemma llist.rel_Grp. With that, you can transform
llist_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

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