# Theory Partial_Order_Reduction.LList_Prefixes

```section ‹Prefixes on Coinductive Lists›

theory LList_Prefixes
imports
Word_Prefixes
"../Extensions/Coinductive_List_Extensions"
begin

lemma unfold_stream_siterate_smap: "unfold_stream f g = smap f ∘ siterate g"
by (rule, coinduction, auto) (metis unfold_stream_eq_SCons)+

lemma lappend_stream_of_llist:
assumes "lfinite u"
shows "stream_of_llist (u \$ v) = list_of u @- stream_of_llist v"
using assms unfolding stream_of_llist_def by induct auto

lemma llist_of_inf_llist_prefix[intro]: "u ≤⇩F⇩I v ⟹ llist_of u ≤ llist_of_stream v"
by (metis lappend_llist_of_stream_conv_shift le_llist_conv_lprefix lprefix_lappend prefix_fininfE)
lemma prefix_llist_of_inf_llist[intro]: "lfinite u ⟹ u ≤ v ⟹ list_of u ≤⇩F⇩I stream_of_llist v"
by (metis lappend_stream_of_llist le_llist_conv_lprefix lprefix_conv_lappend prefix_fininfI)

lemma lproject_prefix_limit_chain:
assumes "chain w" "⋀ k. lproject A (llist_of (w k)) ≤ x"
shows "lproject A (llist_of_stream (limit w)) ≤ x"
proof (rule lproject_prefix_limit')
fix k
obtain l where 1: "k < length (w l)" using assms(1) by rule
show "∃ v ≤ llist_of_stream (limit w). enat k < llength v ∧ lproject A v ≤ x"
proof (intro exI conjI)
show "llist_of (w l) ≤ llist_of_stream (limit w)"
using llist_of_inf_llist_prefix chain_prefix_limit assms(1) by this
show "enat k < llength (llist_of (w l))" using 1 by simp
show "lproject A (llist_of (w l)) ≤ x" using assms(2) by this
qed
qed
lemma lproject_eq_limit_chain:
assumes "chain u" "chain v" "⋀ k. project A (u k) = project A (v k)"
shows "lproject A (llist_of_stream (limit u)) = lproject A (llist_of_stream (limit v))"
proof (rule antisym)
show "lproject A (llist_of_stream (limit u)) ≤ lproject A (llist_of_stream (limit v))"
proof (rule lproject_prefix_limit_chain)
show "chain u" using assms(1) by this
next
fix k
have "lproject A (llist_of (u k)) = lproject A (llist_of (v k))" using assms(3) by simp
also have "… ≤ lproject A (llist_of_stream (limit v))" using chain_prefix_limit assms(2) by blast
finally show "lproject A (llist_of (u k)) ≤ lproject A (llist_of_stream (limit v))" by this
qed
show "lproject A (llist_of_stream (limit v)) ≤ lproject A (llist_of_stream (limit u))"
proof (rule lproject_prefix_limit_chain)
show "chain v" using assms(2) by this
next
fix k
have "lproject A (llist_of (v k)) = lproject A (llist_of (u k))" using assms(3) by simp
also have "… ≤ lproject A (llist_of_stream (limit u))" using chain_prefix_limit assms(1) by blast
finally show "lproject A (llist_of (v k)) ≤ lproject A (llist_of_stream (limit u))" by this
qed
qed

end```