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

```Hello

```
I've been attempting some coinductive proofs, and I've hit a situation where I'm not sure to proceed. Any help would be greatly appreciated. I've tried to make the situation as abstract as possible in the attached theory file.
```
```
In this setting, I have a predicate P defined in terms of two coinductive predicates. I would like to be able to perform coinduction on it. I can define a variant of P, P_co, directly as a coinduction, effectively unfolding the two underlying predicates simultaneously, and this allows me to prove everything I want to coinductively.
```
```
In other areas of my proof, I would strongly prefer to use P's representation. I want to either derive a coinduction rule for P so that I no longer need P_co, or to prove that P_co implies P, whichever is easier. However I've not been able to complete either proof.
```
```
I imagine this has some relation to the discussion/solutions presented below, but I've not been able to follow through the connection myself.
```https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-November/msg00045.html
https://isabelle.in.tum.de/dist/Isabelle2017/doc/corec.pdf

```
Thanks in advance for any comments or suggestions. I'm new to coinduction in Isabelle (and in general), so apologies if there is something fundamental that I've missed.
```
Best wishes
```theory Test_Coinduction imports "Coinductive.Coinductive" begin

typedecl state

typedecl abs

consts
transition :: "state \<Rightarrow> state \<Rightarrow> bool"
state_abs :: "state \<Rightarrow> abs"
abs_equiv :: "abs \<Rightarrow> abs \<Rightarrow> bool"

coinductive abs_trace :: "state \<Rightarrow> abs llist \<Rightarrow> bool" where
base:"\<lbrakk> \<forall>s2. \<not>transition s1 s2\<rbrakk> \<Longrightarrow> abs_trace s1 (LNil)"
| step:"\<lbrakk> transition s1 s2; abs_trace s2 l; state_abs s1 = as1\<rbrakk> \<Longrightarrow> abs_trace s1 (LCons as1 l)"

definition P :: "state \<Rightarrow> abs llist \<Rightarrow> bool" where
"P s l \<equiv> \<exists>l'. abs_trace s l' \<and> llist_all2 abs_equiv l l'"

coinductive P_co :: "state \<Rightarrow> abs llist \<Rightarrow> bool" where
base:"\<lbrakk> \<forall>s2. \<not>transition s1 s2\<rbrakk> \<Longrightarrow> P_co s1 (LNil)"
| step:"\<lbrakk> transition s1 s2; P_co s2 l; state_abs s1 = as1; abs_equiv as as1 \<rbrakk> \<Longrightarrow> P_co s1 (LCons as l)"

lemma P_co_imp_P:
assumes "P_co s al"
shows "P s al"
sorry

thm P_co.coinduct

lemma P_coinduct:
assumes "X xa xb"
and "(\<And>x1 x2.
X x1 x2 \<Longrightarrow>
(\<exists>a. x1 = a \<and> x2 = LNil \<and> (\<forall>b. \<not> transition a b)) \<or>
(\<exists>a b l aa' aa.
x1 = a \<and>
x2 = LCons aa l \<and>
transition a b \<and>
(X b l \<or> P b l) \<and>
state_abs a = aa' \<and> abs_equiv aa aa'))"
shows "P xa xb"
sorry

end```

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