[isabelle] Coinduction on predicate defined wrt other coinductive predicates
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
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.
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.
theory Test_Coinduction imports "Coinductive.Coinductive" begin
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)"
assumes "P_co s al"
shows "P s al"
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"
This archive was generated by a fusion of
Pipermail (Mailman edition) and