Theory Partial_Order_Reduction.Coinductive_List_Extensions
section ‹Coinductive Lists›
theory Coinductive_List_Extensions
imports
Coinductive.Coinductive_List
Coinductive.Coinductive_List_Prefix
Coinductive.Coinductive_Stream
"../Extensions/List_Extensions"
"../Extensions/ESet_Extensions"
begin
hide_const (open) Sublist.prefix
hide_const (open) Sublist.suffix
declare list_of_lappend[simp]
declare lnth_lappend1[simp]
declare lnth_lappend2[simp]
declare lprefix_llength_le[dest]
declare Sup_llist_def[simp]
declare length_list_of[simp]
declare llast_linfinite[simp]
declare lnth_ltake[simp]
declare lappend_assoc[simp]
declare lprefix_lappend[simp]
lemma lprefix_lSup_revert: "lSup = Sup" "lprefix = less_eq" by auto
lemma admissible_lprefixI[cont_intro]:
assumes "mcont lub ord lSup lprefix f"
assumes "mcont lub ord lSup lprefix g"
shows "ccpo.admissible lub ord (λ x. lprefix (f x) (g x))"
using ccpo_class.admissible_leI assms unfolding lprefix_lSup_revert by this
lemma llist_lift_admissible:
assumes "ccpo.admissible lSup lprefix P"
assumes "⋀ u. u ≤ v ⟹ lfinite u ⟹ P u"
shows "P v"
using assms by (metis LNil_lprefix le_llist_conv_lprefix lfinite.simps llist_gen_induct)
abbreviation "linfinite w ≡ ¬ lfinite w"
notation LNil (‹<>›)
notation LCons (infixr ‹%› 65)
notation lzip (infixr ‹¦¦› 51)
notation lappend (infixr ‹$› 65)
notation lnth (infixl ‹?!› 100)
syntax "_llist" :: "args ⇒ 'a llist" (‹<_>›)
syntax_consts "_llist" ⇌ LCons
translations
"<a, x>" ⇌ "a % <x>"
"<a>" ⇌ "a % <>"
lemma eq_LNil_conv_lnull[simp]: "w = <> ⟷ lnull w" by auto
lemma Collect_lnull[simp]: "{w. lnull w} = {<>}" by auto
lemma inj_on_ltake: "inj_on (λ k. ltake k w) {.. llength w}"
by (rule inj_onI, auto, metis llength_ltake min_def)
lemma lnth_inf_llist'[simp]: "lnth (inf_llist f) = f" by auto
lemma not_lnull_lappend_startE[elim]:
assumes "¬ lnull w"
obtains a v
where "w = <a> $ v"
using not_lnull_conv assms by (simp, metis)
lemma not_lnull_lappend_endE[elim]:
assumes "¬ lnull w"
obtains a v
where "w = v $ <a>"
proof (cases "lfinite w")
case False
show ?thesis
proof
show "w = w $ <a>" using lappend_inf False by force
qed
next
case True
show ?thesis
using True assms that
proof (induct arbitrary: thesis)
case (lfinite_LNil)
show ?case using lfinite_LNil by auto
next
case (lfinite_LConsI w a)
show ?case
proof (cases "lnull w")
case False
obtain b v where 1: "w = v $ <b>" using lfinite_LConsI(2) False by this
show ?thesis
proof (rule lfinite_LConsI(4))
show "a % w = (a % v) $ <b>" unfolding 1 by simp
qed
next
case True
show ?thesis
proof (rule lfinite_LConsI(4))
show "a % w = <> $ <a>" using True by simp
qed
qed
qed
qed
lemma llength_lappend_startE[elim]:
assumes "llength w ≥ eSuc n"
obtains a v
where "w = <a> $ v" "llength v ≥ n"
proof -
have 1: "¬ lnull w" using assms by auto
show ?thesis using assms 1 that by auto
qed
lemma llength_lappend_endE[elim]:
assumes "llength w ≥ eSuc n"
obtains a v
where "w = v $ <a>" "llength v ≥ n"
proof -
have 1: "¬ lnull w" using assms by auto
show ?thesis using assms 1 that by auto
qed
lemma llength_lappend_start'E[elim]:
assumes "llength w = enat (Suc n)"
obtains a v
where "w = <a> $ v" "llength v = enat n"
proof -
have 1: "llength w ≥ eSuc (enat n)" using assms by simp
obtain a v where 2: "w = <a> $ v" using 1 by blast
show ?thesis
proof
show "w = <a> $ v" using 2(1) by this
show "llength v = enat n" using assms unfolding 2(1) by (simp, metis eSuc_enat eSuc_inject)
qed
qed
lemma llength_lappend_end'E[elim]:
assumes "llength w = enat (Suc n)"
obtains a v
where "w = v $ <a>" "llength v = enat n"
proof -
have 1: "llength w ≥ eSuc (enat n)" using assms by simp
obtain a v where 2: "w = v $ <a>" using 1 by blast
show ?thesis
proof
show "w = v $ <a>" using 2(1) by this
show "llength v = enat n" using assms unfolding 2(1) by (simp, metis eSuc_enat eSuc_inject)
qed
qed
lemma ltake_llast[simp]:
assumes "enat k < llength w"
shows "llast (ltake (enat (Suc k)) w) = w ?! k"
proof -
have 1: "llength (ltake (enat (Suc k)) w) = eSuc (enat k)"using min.absorb_iff1 assms by auto
have "llast (ltake (enat (Suc k)) w) = ltake (enat (Suc k)) w ?! k"
using llast_conv_lnth 1 by this
also have "… = w ?! k" by (rule lnth_ltake, simp)
finally show ?thesis by this
qed
lemma linfinite_llength[dest, simp]:
assumes "linfinite w"
shows "enat k < llength w"
using assms not_lfinite_llength by force
lemma llist_nth_eqI[intro]:
assumes "llength u = llength v"
assumes "⋀ i. enat i < llength u ⟹ enat i < llength v ⟹ u ?! i = v ?! i"
shows "u = v"
using assms
proof (coinduction arbitrary: u v)
case Eq_llist
have 10: "llength u = llength v" using Eq_llist by auto
have 11: "⋀ i. enat i < llength u ⟹ enat i < llength v ⟹ u ?! i = v ?! i"
using Eq_llist by auto
show ?case
proof (intro conjI impI exI allI)
show "lnull u ⟷ lnull v" using 10 by auto
next
assume 20: "¬ lnull u" "¬ lnull v"
show "lhd u = lhd v" using lhd_conv_lnth enat_0 11 20 by force
next
show "ltl u = ltl u" by rule
next
show "ltl v = ltl v" by rule
next
assume 30: "¬ lnull u" "¬ lnull v"
show "llength (ltl u) = llength (ltl v)" using 10 30 by force
next
fix i
assume 40: "¬ lnull u" "¬ lnull v" "enat i < llength (ltl u)" "enat i < llength (ltl v)"
have 41: "u ?! Suc i = v ?! Suc i"
proof (rule 11)
show "enat (Suc i) < llength u" using Suc_ile_eq 40(1) 40(3) by auto
show "enat (Suc i) < llength v" using Suc_ile_eq 40(2) 40(4) by auto
qed
show "ltl u ?! i = ltl v ?! i" using lnth_ltl 40(1-2) 41 by metis
qed
qed
primcorec lscan :: "('a ⇒ 'b ⇒ 'b) ⇒ 'a llist ⇒ 'b ⇒ 'b llist"
where "lscan f w a = (case w of <> ⇒ <a> | x % xs ⇒ a % lscan f xs (f x a))"
lemma lscan_simps[simp]:
"lscan f <> a = <a>"
"lscan f (x % xs) a = a % lscan f xs (f x a)"
by (metis llist.simps(4) lscan.code, metis llist.simps(5) lscan.code)
lemma lscan_lfinite[iff]: "lfinite (lscan f w a) ⟷ lfinite w"
proof
assume "lfinite (lscan f w a)"
thus "lfinite w"
proof (induct "lscan f w a" arbitrary: w a rule: lfinite_induct)
case LNil
show ?case using LNil by simp
next
case LCons
show ?case by (cases w, simp, simp add: LCons(3))
qed
next
assume "lfinite w"
thus "lfinite (lscan f w a)" by (induct arbitrary: a, auto)
qed
lemma lscan_llength[simp]: "llength (lscan f w a) = eSuc (llength w)"
proof (cases "lfinite w")
case False
have 1: "llength (lscan f w a) = ∞" using not_lfinite_llength False by auto
have 2: "llength w = ∞" using not_lfinite_llength False by auto
show ?thesis using 1 2 by simp
next
case True
show ?thesis using True by (induct arbitrary: a, auto)
qed
function lfold :: "('a ⇒ 'b ⇒ 'b) ⇒ 'a llist ⇒ 'b ⇒ 'b"
where "lfinite w ⟹ lfold f w = fold f (list_of w)" | "linfinite w ⟹ lfold f w = id"
by (auto, metis) termination by lexicographic_order
lemma lfold_llist_of[simp]: "lfold f (llist_of xs) = fold f xs" by simp
lemma finite_UNIV_llength_eq:
assumes "finite (UNIV :: 'a set)"
shows "finite {w :: 'a llist. llength w = enat n}"
proof (induct n)
case (0)
show ?case by simp
next
case (Suc n)
have 1: "finite ({v. llength v = enat n} × UNIV :: ('a llist × 'a) set)"
using Suc assms by simp
have 2: "finite ((λ (v, a). v $ <a> :: 'a llist ) ` ({v. llength v = enat n} × UNIV))"
using 1 by auto
have 3: "finite {v $ <a> :: 'a llist |v a. llength v = enat n}"
proof -
have 0: "{v $ <a> :: 'a llist |v a. llength v = enat n} =
(λ (v, a). v $ <a> :: 'a llist ) ` ({v. llength v = enat n} × UNIV)" by auto
show ?thesis using 2 unfolding 0 by this
qed
have 4: "finite {w :: 'a llist . llength w = enat (Suc n)}"
proof -
have 0: "{w :: 'a llist . llength w = enat (Suc n)} =
{v $ <a> :: 'a llist |v a. llength v = enat n}" by force
show ?thesis using 3 unfolding 0 by this
qed
show ?case using 4 by this
qed
lemma finite_UNIV_llength_le:
assumes "finite (UNIV :: 'a set)"
shows "finite {w :: 'a llist. llength w ≤ enat n}"
proof -
have 1: "{w. llength w ≤ enat n} = (⋃ k ≤ n. {w. llength w = enat k})"
by (auto, metis atMost_iff enat_ile enat_ord_simps(1))
show ?thesis unfolding 1 using finite_UNIV_llength_eq assms by auto
qed
lemma lprefix_ltake[dest]: "u ≤ v ⟹ u = ltake (llength u) v"
by (metis le_llist_conv_lprefix lprefix_conv_lappend ltake_all ltake_lappend1 order_refl)
lemma prefixes_set: "{v. v ≤ w} = {ltake k w |k. k ≤ llength w}" by fastforce
lemma esize_prefixes[simp]: "esize {v. v ≤ w} = eSuc (llength w)"
proof -
have "esize {v. v ≤ w} = esize {ltake k w |k. k ≤ llength w}" unfolding prefixes_set by rule
also have "… = esize ((λ k. ltake k w) ` {.. llength w})"
unfolding atMost_def image_Collect by rule
also have "… = esize {.. llength w}" using inj_on_ltake esize_image by blast
also have "… = eSuc (llength w)" by simp
finally show ?thesis by this
qed
lemma prefix_subsume: "v ≤ w ⟹ u ≤ w ⟹ llength v ≤ llength u ⟹ v ≤ u"
by (metis le_llist_conv_lprefix lprefix_conv_lappend
lprefix_ltake ltake_is_lprefix ltake_lappend1)
lemma ltake_infinite[simp]: "ltake ∞ w = w" by (metis enat_ord_code(3) ltake_all)
lemma lprefix_infinite:
assumes "u ≤ v" "linfinite u"
shows "u = v"
proof -
have 1: "llength u = ∞" using not_lfinite_llength assms(2) by this
have "u = ltake (llength u) v" using lprefix_ltake assms(1) by this
also have "… = v" using 1 by simp
finally show ?thesis by this
qed
instantiation llist :: (type) esize_order
begin
definition [simp]: "esize ≡ llength"
instance
proof
fix w :: "'a llist"
assume 1: "esize w ≠ ∞"
show "finite {v. v ≤ w}"
using esize_prefixes 1 by (metis eSuc_eq_infinity_iff esize_set.simps(2) esize_llist_def)
next
fix u v :: "'a llist"
assume 1: "u ≤ v"
show "esize u ≤ esize v" using lprefix_llength_le 1 by auto
next
fix u v :: "'a llist"
assume 1: "u < v"
show "esize u < esize v" using lstrict_prefix_llength_less 1 by auto
qed
end
subsection ‹Index Sets›
definition liset :: "'a set ⇒ 'a llist ⇒ nat set"
where "liset A w ≡ {i. enat i < llength w ∧ w ?! i ∈ A}"
lemma lisetI[intro]:
assumes "enat i < llength w" "w ?! i ∈ A"
shows "i ∈ liset A w"
using assms unfolding liset_def by auto
lemma lisetD[dest]:
assumes "i ∈ liset A w"
shows "enat i < llength w" "w ?! i ∈ A"
using assms unfolding liset_def by auto
lemma liset_finite:
assumes "lfinite w"
shows "finite (liset A w)"
proof
show "liset A w ⊆ {i. enat i < llength w}" by auto
show "finite {i. enat i < llength w}" using lfinite_finite_index assms by this
qed
lemma liset_nil[simp]: "liset A <> = {}" by auto
lemma liset_cons_not_member[simp]:
assumes "a ∉ A"
shows "liset A (a % w) = Suc ` liset A w"
proof -
have "liset A (a % w) = {i. enat i < llength (a % w) ∧ (a % w) ?! i ∈ A}" by auto
also have "… = Suc ` {i. enat (Suc i) < llength (a % w) ∧ (a % w) ?! Suc i ∈ A}"
using Collect_split_Suc(1) assms by simp
also have "… = Suc ` {i. enat i < llength w ∧ w ?! i ∈ A}" using Suc_ile_eq by simp
also have "… = Suc ` liset A w" by auto
finally show ?thesis by this
qed
lemma liset_cons_member[simp]:
assumes "a ∈ A"
shows "liset A (a % w) = {0} ∪ Suc ` liset A w"
proof -
have "liset A (a % w) = {i. enat i < llength (a % w) ∧ (a % w) ?! i ∈ A}" by auto
also have "… = {0} ∪ Suc ` {i. enat (Suc i) < llength (a % w) ∧ (a % w) ?! Suc i ∈ A}"
using Collect_split_Suc(2) assms by simp
also have "… = {0} ∪ Suc ` {i. enat i < llength w ∧ w ?! i ∈ A}" using Suc_ile_eq by simp
also have "… = {0} ∪ Suc ` liset A w" by auto
finally show ?thesis by this
qed
lemma liset_prefix:
assumes "i ∈ liset A v" "u ≤ v" "enat i < llength u"
shows "i ∈ liset A u"
unfolding liset_def
proof (intro CollectI conjI)
have 1: "v ?! i ∈ A" using assms(1) by auto
show "enat i < llength u" using assms(3) by this
show "u ?! i ∈ A" using lprefix_lnthD assms(2, 3) 1 by force
qed
lemma liset_suffix:
assumes "i ∈ liset A u" "u ≤ v"
shows "i ∈ liset A v"
unfolding liset_def
proof (intro CollectI conjI)
have 1: "enat i < llength u" "u ?! i ∈ A" using assms(1) by auto
show "enat i < llength v" using lprefix_llength_le 1(1) assms(2) by fastforce
show "v ?! i ∈ A" using lprefix_lnthD assms(2) 1 by force
qed
lemma liset_ltake[simp]: "liset A (ltake (enat k) w) = liset A w ∩ {..< k}"
proof (intro equalityI subsetI)
fix i
assume 1: "i ∈ liset A (ltake (enat k) w)"
have 2: "enat i < enat k" using 1 by auto
have 3: "ltake (enat k) w ?! i = w ?! i" using lnth_ltake 2 by this
show "i ∈ liset A w ∩ {..< k}" using 1 3 by fastforce
next
fix i
assume 1: "i ∈ liset A w ∩ {..< k}"
have 2: "enat i < enat k" using 1 by auto
have 3: "ltake (enat k) w ?! i = w ?! i" using lnth_ltake 2 by this
show "i ∈ liset A (ltake (enat k) w)" using 1 3 by fastforce
qed
lemma liset_mono[dest]: "u ≤ v ⟹ liset A u ⊆ liset A v"
unfolding liset_def using lprefix_lnthD by fastforce
lemma liset_cont[dest]:
assumes "Complete_Partial_Order.chain less_eq C" "C ≠ {}"
shows "liset A (⨆ C) = (⋃ w ∈ C. liset A w)"
proof safe
fix i
assume 1: "i ∈ liset A (⨆ C)"
show "i ∈ (⋃ w ∈ C. liset A w)"
proof (cases "finite C")
case False
obtain w where 2: "w ∈ C" "enat i < llength w"
using esize_llist_def infinite_chain_arbitrary_esize assms(1) False Suc_ile_eq by metis
have 3: "w ≤ ⨆ C" using chain_lprefix_lSup assms(1) 2(1) by simp
have 4: "i ∈ liset A w" using liset_prefix 1 3 2(2) by this
show ?thesis using 2(1) 4 by auto
next
case True
have 2: "⨆ C ∈ C" using in_chain_finite assms(1) True assms(2) by this
show ?thesis using 1 2 by auto
qed
next
fix w i
assume 1: "w ∈ C" "i ∈ liset A w"
have 2: "w ≤ ⨆ C" using chain_lprefix_lSup assms(1) 1(1) by simp
show "i ∈ liset A (⨆ C)" using liset_suffix 1(2) 2 by this
qed
lemma liset_mcont: "Complete_Partial_Order2.mcont lSup lprefix Sup less_eq (liset A)"
unfolding lprefix_lSup_revert by (blast intro: mcontI monotoneI contI)
lemmas mcont2mcont_liset = liset_mcont[THEN lfp.mcont2mcont, simp, cont_intro]
subsection ‹Selections›
abbreviation "lproject A ≡ lfilter (λ a. a ∈ A)"
abbreviation "lselect s w ≡ lnths w s"
lemma lselect_to_lproject: "lselect s w = lmap fst (lproject (UNIV × s) (w ¦¦ iterates Suc 0))"
proof -
have 1: "{(x, y). y ∈ s} = UNIV × s" by auto
have "lselect s w = lmap fst (lproject {(x, y). y ∈ s} (w ¦¦ iterates Suc 0))"
unfolding lnths_def by simp
also have "… = lmap fst (lproject (UNIV × s) (w ¦¦ iterates Suc 0))" unfolding 1 by rule
finally show ?thesis by this
qed
lemma lproject_to_lselect: "lproject A w = lselect (liset A w) w"
unfolding lfilter_conv_lnths liset_def by rule
lemma lproject_llength[simp]: "llength (lproject A w) = esize (liset A w)"
by (induct rule: llist_induct) (auto)
lemma lproject_lfinite[simp]: "lfinite (lproject A w) ⟷ finite (liset A w)"
using lproject_llength esize_iff_infinite llength_eq_infty_conv_lfinite by metis
lemma lselect_restrict_indices[simp]: "lselect {i ∈ s. enat i < llength w} w = lselect s w"
proof (rule lnths_cong)
show "w = w" by rule
next
fix n
assume 1: "enat n < llength w"
show "n ∈ {i ∈ s. enat i < llength w} ⟷ n ∈ s" using 1 by blast
qed
lemma lselect_llength: "llength (lselect s w) = esize {i ∈ s. enat i < llength w}"
proof -
have 1: "⋀ i. enat i < llength w ⟹ (w ¦¦ iterates Suc 0) ?! i = (w ?! i, i)"
by (metis Suc_funpow enat.distinct(1) enat_ord_simps(4) llength_iterates lnth_iterates
lnth_lzip monoid_add_class.add.right_neutral)
have 2: "{i. enat i < llength w ∧ (w ¦¦ iterates Suc 0) ?! i ∈ UNIV × s} =
{i ∈ s. enat i < llength w}" using 1 by auto
have "llength (lselect s w) = esize (liset (UNIV × s) (w ¦¦ iterates Suc 0))"
unfolding lselect_to_lproject by simp
also have "… = esize {i. enat i < llength w ∧ (w ¦¦ iterates Suc 0) ?! i ∈ UNIV × s}"
unfolding liset_def by simp
also have "… = esize {i ∈ s. enat i < llength w}" unfolding 2 by rule
finally show ?thesis by this
qed
lemma lselect_llength_le[simp]: "llength (lselect s w) ≤ esize s"
proof -
have "llength (lselect s w) = esize {i ∈ s. enat i < llength w}"
unfolding lselect_llength by rule
also have "… = esize (s ∩ {i. enat i < llength w})" unfolding Collect_conj_eq by simp
also have "… ≤ esize s" by blast
finally show ?thesis by this
qed
lemma least_lselect_llength:
assumes "¬ lnull (lselect s w)"
shows "enat (least s) < llength w"
proof -
have 0: "llength (lselect s w) > 0" using assms by auto
have 1: "⋀ i. i ∈ s ⟹ least s ≤ i" using Least_le 0 by fast
obtain i where 2: "i ∈ s" "enat i < llength w" using 0 unfolding lselect_llength by auto
have "enat (least s) ≤ enat i" using 1 2(1) by auto
also have "… < llength w" using 2(2) by this
finally show "enat (least s) < llength w" by this
qed
lemma lselect_lnull: "lnull (lselect s w) ⟷ (∀ i ∈ s. enat i ≥ llength w)"
unfolding llength_eq_0[symmetric] lselect_llength by auto
lemma lselect_discard_start:
assumes "⋀ i. i ∈ s ⟹ k ≤ i"
shows "lselect {i. k + i ∈ s} (ldropn k w) = lselect s w"
proof -
have 1: "lselect s (ltake (enat k) w) = <>"
using assms by (fastforce simp add: lselect_lnull min_le_iff_disj)
have "lselect {m. k + m ∈ s} (ldropn k w) =
lselect s (ltake (enat k) w) $ lselect {m. k + m ∈ s} (ldropn k w)" unfolding 1 by simp
also have "… = lselect s w" using lnths_split by rule
finally show ?thesis by this
qed
lemma lselect_discard_end:
assumes "⋀ i. i ∈ s ⟹ i < k"
shows "lselect s (ltake (enat k) w) = lselect s w"
proof -
have 1: "lselect {m. k + m ∈ s} (ldropn k w) = <>"
using assms by (fastforce simp add: lselect_lnull min_le_iff_disj)
have "lselect s (ltake (enat k) w) =
lselect s (ltake (enat k) w) $ lselect {m. k + m ∈ s} (ldropn k w)" unfolding 1 by simp
also have "… = lselect s w" using lnths_split by rule
finally show ?thesis by this
qed
lemma lselect_least:
assumes "¬ lnull (lselect s w)"
shows "lselect s w = w ?! least s % lselect (s - {least s}) w"
proof -
have 0: "s ≠ {}" using assms by auto
have 1: "least s ∈ s" using LeastI 0 by fast
have 2: "⋀ i. i ∈ s ⟹ least s ≤ i" using Least_le 0 by fast
have 3: "⋀ i. i ∈ s - {least s} ⟹ Suc (least s) ≤ i" using least_unique 2 by force
have 4: "insert (least s) (s - {least s}) = s" using 1 by auto
have 5: "enat (least s) < llength w" using least_lselect_llength assms by this
have 6: "lselect (s - {least s}) (ltake (enat (least s)) w) = <>"
by (rule, auto simp: lselect_llength dest: least_not_less)
have 7: "lselect {i. Suc (least s) + i ∈ s - {least s}} (ldropn (Suc (least s)) w) =
lselect (s - {least s}) w" using lselect_discard_start 3 by this
have "lselect s w = lselect (insert (least s) (s - {least s})) w" unfolding 4 by simp
also have "… = lselect (s - {least s}) (ltake (enat (least s)) w) $ <w ?! least s> $
lselect {m. Suc (least s) + m ∈ s - {least s}} (ldropn (Suc (least s)) w)"
unfolding lnths_insert[OF 5] by simp
also have "… = <w ?! least s> $
lselect {m. Suc (least s) + m ∈ s - {least s}} (ldropn (Suc (least s)) w)"
unfolding 6 by simp
also have "… = w ?! (least s) % lselect (s - {least s}) w" unfolding 7 by simp
finally show ?thesis by this
qed
lemma lselect_lnth[simp]:
assumes "enat i < llength (lselect s w)"
shows "lselect s w ?! i = w ?! nth_least s i"
using assms
proof (induct i arbitrary: s)
case 0
have 1: "¬ lnull (lselect s w)" using 0 by auto
show ?case using lselect_least 1 by force
next
case (Suc i)
have 1: "¬ lnull (lselect s w)" using Suc(2) by auto
have 2: "lselect s w = w ?! least s % lselect (s - {least s}) w" using lselect_least 1 by this
have 3: "llength (lselect s w) = eSuc (llength (lselect (s - {least s}) w))" using 2 by simp
have 4: "enat i < llength (lselect (s - {least s}) w)" using 3 Suc(2) by simp
have "lselect s w ?! Suc i = (w ?! least s % lselect (s - {least s}) w) ?! Suc i" using 2 by simp
also have "… = lselect (s - {least s}) w ?! i" by simp
also have "… = w ?! nth_least (s - {least s}) i" using Suc(1) 4 by simp
also have "… = w ?! nth_least s (Suc i)" by simp
finally show ?case by this
qed
lemma lproject_lnth[simp]:
assumes "enat i < llength (lproject A w)"
shows "lproject A w ?! i = w ?! nth_least (liset A w) i"
using assms unfolding lproject_to_lselect by simp
lemma lproject_ltake[simp]:
assumes "enat k ≤ llength (lproject A w)"
shows "lproject A (ltake (enat (nth_least (lift (liset A w)) k)) w) =
ltake (enat k) (lproject A w)"
proof
have "llength (lproject A (ltake (enat (nth_least (lift (liset A w)) k)) w)) =
enat (card (liset A w ∩ {..< nth_least (lift (liset A w)) k}))" by simp
also have "… = enat (card {i ∈ liset A w. i < nth_least (lift (liset A w)) k})"
unfolding lessThan_def Collect_conj_eq by simp
also have "… = enat k" using assms by simp
also have "… = llength (ltake (enat k) (lproject A w))" using min_absorb1 assms by force
finally show "llength (lproject A (ltake (enat (nth_least (lift (liset A w)) k)) w)) =
llength (ltake (enat k) (lproject A w))" by this
next
fix i
assume 1: "enat i < llength (lproject A (ltake (enat (nth_least (lift (liset A w)) k)) w))"
assume 2: "enat i < llength (ltake (enat k) (lproject A w))"
obtain k' where 3: "k = Suc k'" using 2 nat.exhaust by auto
have 4: "enat k' < llength (lproject A w)" using assms 3 by simp
have 5: "i ≤ k'" using 2 3 by simp
have 6: "nth_least (lift (liset A w)) k = Suc (nth_least (liset A w) k')"
using 3 4 by (simp del: nth_least.simps)
have 7: "nth_least (liset A w) i < Suc (nth_least (liset A w) k')"
proof -
have "nth_least (liset A w) i ≤ nth_least (liset A w) k'" using 4 5 by simp
also have "… < Suc (nth_least (liset A w) k')" by simp
finally show ?thesis by this
qed
have 8: "nth_least (liset A w ∩ {..< Suc (nth_least (liset A w) k')}) i =
nth_least (liset A w) i"
proof (rule nth_least_eq)
show "enat i < esize (liset A w ∩ {..< Suc (nth_least (liset A w) k')})" using 1 6 by simp
have "enat i ≤ enat k'" using 5 by simp
also have "enat k' < esize (liset A w)" using 4 by simp
finally show "enat i < esize (liset A w)" by this
next
fix j
assume 1: "j ≤ nth_least (liset A w) i"
show "j ∈ liset A w ∩ {..< Suc (nth_least (liset A w) k')} ⟷ j ∈ liset A w"
using 1 7 by simp
qed
have "lproject A (ltake (enat (nth_least (lift (liset A w)) k)) w) ?! i =
ltake (enat (Suc (nth_least (liset A w) k'))) w ?!
nth_least (liset A w ∩ {..< Suc (nth_least (liset A w) k')}) i"
using 1 6 by simp
also have "… = ltake (enat (Suc (nth_least (liset A w) k'))) w ?! nth_least (liset A w) i"
using 8 by simp
also have "… = w ?! nth_least (liset A w) i" using 7 by simp
also have "… = lproject A w ?! i" using 2 by simp
also have "… = ltake (enat k) (lproject A w) ?! i" using 2 by simp
finally show "lproject A (ltake (enat (nth_least (lift (liset A w)) k)) w) ?! i =
ltake (enat k) (lproject A w) ?! i" by this
qed
lemma llength_less_llength_lselect_less:
"enat i < esize s ∧ enat (nth_least s i) < llength w ⟷ enat i < llength (lselect s w)"
using nth_least_less_esize_less unfolding lselect_llength by this
lemma lselect_lselect'':
assumes "⋀ i. i ∈ s ⟹ enat i < llength w"
assumes "⋀ i. i ∈ t ⟹ enat i < llength (lselect s w)"
shows "lselect t (lselect s w) = lselect (nth_least s ` t) w"
proof
note lselect_llength[simp]
have 1: "⋀ i. i ∈ nth_least s ` t ⟹ enat i < llength w" using assms by auto
have 2: "t ⊆ {i. enat i < esize s}"
using assms(2) lselect_llength_le less_le_trans by blast
have 3: "inj_on (nth_least s) t" using inj_on_subset nth_least.inj_on 2 by this
have "llength (lselect t (lselect s w)) = esize t" using assms(2) by simp
also have "… = esize (nth_least s ` t)" using 3 by auto
also have "… = llength (lselect (nth_least s ` t) w)" using 1 by simp
finally show "llength (lselect t (lselect s w)) = llength (lselect (nth_least s ` t) w)"
by this
next
fix i
assume 1: "enat i < llength (lselect t (lselect s w))"
assume 2: "enat i < llength (lselect (nth_least s ` t) w)"
have 3: "enat i < esize t" using less_le_trans 1 lselect_llength_le by this
have 4: "⋀ i. i ∈ t ⟹ enat i < esize s"
using assms(2) lselect_llength_le less_le_trans by blast
have "lselect t (lselect s w) ?! i = lselect s w ?! nth_least t i" using 1 by simp
also have "… = w ?! nth_least s (nth_least t i)" using assms(2) 3 by simp
also have "… = w ?! nth_least (nth_least s ` t) i" using 3 4 by simp
also have "… = lselect (nth_least s ` t) w ?! i" using 2 by simp
finally show "lselect t (lselect s w) ?! i = lselect (nth_least s ` t) w ?! i" by this
qed
lemma lselect_lselect'[simp]:
assumes "⋀ i. i ∈ t ⟹ enat i < esize s"
shows "lselect t (lselect s w) = lselect (nth_least s ` t) w"
proof -
have 1: "nth_least {i ∈ s. enat i < llength w} ` {i ∈ t. enat i < llength (lselect s w)} =
{i ∈ nth_least s ` t. enat i < llength w}"
unfolding Compr_image_eq
proof (rule image_cong)
show "{i ∈ t. enat i < llength (lselect s w)} = {i ∈ t. enat (nth_least s i) < llength w}"
using llength_less_llength_lselect_less assms by blast
next
fix i
assume 1: "i ∈ {i ∈ t. enat (nth_least s i) < llength w}"
have 2: "enat i < esize {i ∈ s. enat i < llength w}"
using nth_least_less_esize_less assms 1 by blast
show "nth_least {i ∈ s. enat i < llength w} i = nth_least s i" using 2 by simp
qed
have "lselect t (lselect s w) =
lselect {i ∈ t. enat i < llength (lselect s w)} (lselect {i ∈ s. enat i < llength w} w)"
by simp
also have "… = lselect (nth_least {i ∈ s. enat i < llength w} `
{i ∈ t. enat i < llength (lselect s w)}) w"
by (rule lselect_lselect'', auto simp: lselect_llength)
also have "… = lselect {i ∈ nth_least s ` t. enat i < llength w} w" unfolding 1 by rule
also have "… = lselect (nth_least s ` t) w" by simp
finally show ?thesis by this
qed
lemma lselect_lselect:
"lselect t (lselect s w) = lselect (nth_least s ` {i ∈ t. enat i < esize s}) w"
proof -
have "lselect t (lselect s w) = lselect {i ∈ t. enat i < llength (lselect s w)} (lselect s w)"
by simp
also have "… = lselect (nth_least s ` {i ∈ t. enat i < llength (lselect s w)}) w"
using lselect_llength_le less_le_trans by (blast intro: lselect_lselect')
also have "… = lselect (nth_least s ` {i ∈ t. enat i < esize s}) w"
using llength_less_llength_lselect_less by (auto intro!: lnths_cong)
finally show ?thesis by this
qed
lemma lselect_lproject':
assumes "⋀ i. i ∈ s ⟹ enat i < llength w"
shows "lproject A (lselect s w) = lselect (s ∩ liset A w) w"
proof -
have 1: "⋀ i. i ∈ liset A (lselect s w) ⟹ enat i < esize s" using less_le_trans by force
have 2: "{i ∈ liset A (lselect s w). enat i < esize s} = liset A (lselect s w)"
using 1 by auto
have 3: "nth_least s ` liset A (lselect s w) = s ∩ liset A w"
proof safe
fix k
assume 4: "k ∈ liset A (lselect s w)"
show "nth_least s k ∈ s" using 1 4 by simp
show "nth_least s k ∈ liset A w"
using llength_less_llength_lselect_less 4 unfolding liset_def by auto
next
fix k
assume 1: "k ∈ s" "k ∈ liset A w"
have 2: "nth_least s (card {i ∈ s. i < k}) = k" using nth_least_card 1(1) by this
have 3: "enat (card {i ∈ s. i < k}) < llength (lselect s w)"
unfolding lselect_llength using assms 1(1) by simp
show "k ∈ nth_least s ` liset A (lselect s w)"
proof
show "k = nth_least s (card {i ∈ s. i < k})" using 2 by simp
show "card {i ∈ s. i < k} ∈ liset A (lselect s w)" using 1(2) 2 3 by fastforce
qed
qed
have "lproject A (lselect s w) = lselect (liset A (lselect s w)) (lselect s w)"
unfolding lproject_to_lselect by rule
also have "… = lselect (nth_least s ` {i ∈ liset A (lselect s w). enat i < esize s}) w"
unfolding lselect_lselect by rule
also have "… = lselect (nth_least s ` liset A (lselect s w)) w" unfolding 2 by rule
also have "… = lselect (s ∩ liset A w) w" unfolding 3 by rule
finally show ?thesis by this
qed
lemma lselect_lproject[simp]: "lproject A (lselect s w) = lselect (s ∩ liset A w) w"
proof -
have 1: "{i ∈ s. enat i < llength w} ∩ liset A w = s ∩ liset A w" by auto
have "lproject A (lselect s w) = lproject A (lselect {i ∈ s. enat i < llength w} w)" by simp
also have "… = lselect ({i ∈ s. enat i < llength w} ∩ liset A w) w"
by (rule lselect_lproject', simp)
also have "… = lselect (s ∩ liset A w) w" unfolding 1 by rule
finally show ?thesis by this
qed
lemma lproject_lselect_subset[simp]:
assumes "liset A w ⊆ s"
shows "lproject A (lselect s w) = lproject A w"
proof -
have 1: "s ∩ liset A w = liset A w" using assms by auto
have "lproject A (lselect s w) = lselect (s ∩ liset A w) w" by simp
also have "… = lselect (liset A w) w" unfolding 1 by rule
also have "… = lproject A w" unfolding lproject_to_lselect by rule
finally show ?thesis by this
qed
lemma lselect_prefix[intro]:
assumes "u ≤ v"
shows "lselect s u ≤ lselect s v"
proof (cases "lfinite u")
case False
show ?thesis using lprefix_infinite assms False by auto
next
case True
obtain k where 1: "llength u = enat k" using True length_list_of by metis
obtain w where 2: "v = u $ w" using lprefix_conv_lappend assms by auto
have "lselect s u ≤ lselect s u $ lselect {n. n + k ∈ s} w" by simp
also have "… = lselect s (u $ w)" using lnths_lappend_lfinite[symmetric] 1 by this
also have "… = lselect s v" unfolding 2 by rule
finally show ?thesis by this
qed
lemma lproject_prefix[intro]:
assumes "u ≤ v"
shows "lproject A u ≤ lproject A v"
using lprefix_lfilterI assms by auto
lemma lproject_prefix_limit[intro?]:
assumes "⋀ v. v ≤ w ⟹ lfinite v ⟹ lproject A v ≤ x"
shows "lproject A w ≤ x"
proof -
have 1: "ccpo.admissible lSup lprefix (λ v. lproject A v ≤ x)" by simp
show ?thesis using llist_lift_admissible 1 assms(1) by this
qed
lemma lproject_prefix_limit':
assumes "⋀ k. ∃ v. v ≤ w ∧ enat k < llength v ∧ lproject A v ≤ x"
shows "lproject A w ≤ x"
proof (rule lproject_prefix_limit)
fix u
assume 1: "u ≤ w" "lfinite u"
obtain k where 2: "llength u = enat k" using 1(2) by (metis length_list_of)
obtain v where 3: "v ≤ w" "llength u < llength v" "lproject A v ≤ x"
unfolding 2 using assms(1) by auto
have 4: "llength u ≤ llength v" using 3(2) by simp
have 5: "u ≤ v" using prefix_subsume 1(1) 3(1) 4 by this
have "lproject A u ≤ lproject A v" using 5 by rule
also have "… ≤ x" using 3(3) by this
finally show "lproject A u ≤ x" by this
qed
end