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