Theory MoreCoinductiveList

section ‹Auxiliary Lemmas for Coinductive Lists›

text ‹Some lemmas to allow better reasoning with coinductive lists.›

theory MoreCoinductiveList
imports
  Main
  Coinductive.Coinductive_List
begin

subsection @{term "lset"}

lemma lset_lnth: "x  lset xs  n. lnth xs n = x"
  by (induct rule: llist.set_induct, meson lnth_0, meson lnth_Suc_LCons)

lemma lset_lnth_member: " lset xs  A; enat n < llength xs   lnth xs n  A"
  using contra_subsetD[of "lset xs" A] in_lset_conv_lnth[of _ xs] by blast

lemma lset_nth_member_inf: " ¬lfinite xs; lset xs  A   lnth xs n  A"
  by (metis contra_subsetD inf_llist_lnth lset_inf_llist rangeI)

lemma lset_intersect_lnth: "lset xs  A  {}  n. enat n < llength xs  lnth xs n  A"
  by (metis disjoint_iff_not_equal in_lset_conv_lnth)

lemma lset_ltake_Suc:
  assumes "¬lnull xs" "lnth xs 0 = x" "lset (ltake (enat n) (ltl xs))  A"
  shows "lset (ltake (enat (Suc n)) xs)  insert x A"
proof-
  have "lset (ltake (eSuc (enat n)) (LCons x (ltl xs)))  insert x A"
    using assms(3) by auto
  moreover from assms(1,2) have "LCons x (ltl xs) = xs"
    by (metis lnth_0 ltl_simps(2) not_lnull_conv)
  ultimately show ?thesis by (simp add: eSuc_enat)
qed

lemma lfinite_lset: "lfinite xs  ¬lnull xs  llast xs  lset xs"
proof (induct rule: lfinite_induct)
  case (LCons xs)
  show ?case proof (cases)
    assume *: "¬lnull (ltl xs)"
    hence "llast (ltl xs)  lset (ltl xs)" using LCons.hyps(3) by blast
    hence "llast (ltl xs)  lset xs" by (simp add: in_lset_ltlD)
    thus ?thesis by (metis * LCons.prems lhd_LCons_ltl llast_LCons2)
  qed (metis LCons.prems lhd_LCons_ltl llast_LCons llist.set_sel(1))
qed simp

lemma lset_subset: "¬(lset xs  A)  n. enat n < llength xs  lnth xs n  A"
  by (metis in_lset_conv_lnth subsetI)

subsection @{term "llength"}

lemma enat_Suc_ltl:
  assumes "enat (Suc n) < llength xs"
  shows "enat n < llength (ltl xs)"
proof-
  from assms have "eSuc (enat n) < llength xs" by (simp add: eSuc_enat)
  hence "enat n < epred (llength xs)" using eSuc_le_iff ileI1 by fastforce
  thus ?thesis by (simp add: epred_llength)
qed

lemma enat_ltl_Suc: "enat n < llength (ltl xs)  enat (Suc n) < llength xs"
  by (metis eSuc_enat ldrop_ltl leD leI lnull_ldrop)

lemma infinite_small_llength [intro]: "¬lfinite xs  enat n < llength xs"
  using enat_iless lfinite_conv_llength_enat neq_iff by blast

lemma lnull_0_llength: "¬lnull xs  enat 0 < llength xs"
  using zero_enat_def by auto

lemma Suc_llength: "enat (Suc n) < llength xs  enat n < llength xs"
  using dual_order.strict_trans enat_ord_simps(2) by blast

subsection @{term "ltake"}

lemma ltake_lnth: "ltake n xs = ltake n ys  enat m < n  lnth xs m = lnth ys m"
  by (metis lnth_ltake)

lemma lset_ltake_prefix [simp]: "n  m  lset (ltake n xs)  lset (ltake m xs)"
  by (simp add: lprefix_lsetD)

lemma lset_ltake: "(m. m < n  lnth xs m  A)  lset (ltake (enat n) xs)  A"
proof (induct n arbitrary: xs)
  case 0
  have "ltake (enat 0) xs = LNil" by (simp add: zero_enat_def)
  thus ?case by simp
next
  case (Suc n)
  show ?case proof (cases)
    assume "xs  LNil"
    then obtain x xs' where xs: "xs = LCons x xs'" by (meson neq_LNil_conv)
    { fix m assume "m < n"
      hence "Suc m < Suc n" by simp
      hence "lnth xs (Suc m)  A" using Suc.prems by presburger
      hence "lnth xs' m  A" using xs by simp
    }
    hence "lset (ltake (enat n) xs')  A" using Suc.hyps by blast
    moreover have "ltake (enat (Suc n)) xs = LCons x (ltake (enat n) xs')"
      using xs ltake_eSuc_LCons[of _ x xs'] by (metis (no_types) eSuc_enat)
    moreover have "x  A" using Suc.prems xs by force
    ultimately show ?thesis by simp
  qed simp
qed

lemma llength_ltake': "enat n < llength xs  llength (ltake (enat n) xs) = enat n"
  by (metis llength_ltake min.strict_order_iff)

lemma llast_ltake:
  assumes "enat (Suc n) < llength xs"
  shows "llast (ltake (enat (Suc n)) xs) = lnth xs n" (is "llast ?A = _")
  unfolding llast_def using llength_ltake'[OF assms] by (auto simp add: lnth_ltake)

lemma lset_ltake_ltl: "lset (ltake (enat n) (ltl xs))  lset (ltake (enat (Suc n)) xs)"
proof (cases)
  assume "¬lnull xs"
  then obtain v0 where "xs = LCons v0 (ltl xs)" by (metis lhd_LCons_ltl)
  hence "ltake (eSuc (enat n)) xs = LCons v0 (ltake (enat n) (ltl xs))"
    by (metis ltake_eSuc_LCons)
  hence "lset (ltake (enat (Suc n)) xs) = lset (LCons v0 (ltake (enat n) (ltl xs)))"
    by (simp add: eSuc_enat)
  thus ?thesis using lset_LCons[of v0 "ltake (enat n) (ltl xs)"] by blast
qed (simp add: lnull_def)

subsection @{term "ldropn"}

lemma ltl_ldrop: " xs. P xs  P (ltl xs); P xs   P (ldropn n xs)"
  unfolding ldropn_def by (induct n) simp_all

subsection @{term "lfinite"}

lemma lfinite_drop_set: "lfinite xs  n. v  lset (ldrop n xs)"
  by (metis ldrop_inf lmember_code(1) lset_lmember)

lemma index_infinite_set:
  " ¬lfinite x; lnth x m = y; i. lnth x i = y  (m > i. lnth x m = y)   y  lset (ldropn n x)"
proof (induct n arbitrary: x m)
  case 0 thus ?case using lset_nth_member_inf by auto
next
  case (Suc n)
  obtain a xs where x: "x = LCons a xs" by (meson Suc.prems(1) lnull_imp_lfinite not_lnull_conv)
  obtain j where j: "j > m" "lnth x j = y" using Suc.prems(2,3) by blast
  have "lnth xs (j - 1) = y" by (metis lnth_LCons' j(1,2) not_less0 x)
  moreover {
    fix i assume "lnth xs i = y"
    hence "lnth x (Suc i) = y" by (simp add: x)
    hence "j>i. lnth xs j = y" by (metis Suc.prems(3) Suc_lessE lnth_Suc_LCons x)
  }
  ultimately show ?case using Suc.hyps Suc.prems(1) x by auto
qed

subsection @{term "lmap"}

lemma lnth_lmap_ldropn:
  "enat n < llength xs  lnth (lmap f (ldropn n xs)) 0 = lnth (lmap f xs) n"
  by (simp add: lhd_ldropn lnth_0_conv_lhd)

lemma lnth_lmap_ldropn_Suc:
  "enat (Suc n) < llength xs  lnth (lmap f (ldropn n xs)) (Suc 0) = lnth (lmap f xs) (Suc n)"
  by (metis (no_types, lifting) Suc_llength ldropn_ltl leD llist.map_disc_iff lnth_lmap_ldropn
                                lnth_ltl lnull_ldropn ltl_ldropn ltl_lmap)

subsection ‹Notation›

text ‹We introduce the notation \$ to denote @{term "lnth"}.›

notation lnth (infix "$" 61)

end