[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 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.

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
Conrad Watt
theory Test_Coinduction imports "Coinductive.Coinductive" begin

typedecl state

typedecl abs

  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"

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"


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