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