Theory Countable_Multiset
theory Countable_Multiset
imports
"HOL-Library.Countable_Set_Type"
"HOL-Library.Extended_Nat"
"Coinductive.Coinductive_List"
"HOL-Library.BNF_Corec"
Infinite_Sums_Enat
begin
section ‹Miscellaneous (Mostly About Lazy Lists)›
lemma bij_betw_singl_remap: ‹bij_betw π A B ⟹ x ∈ A ⟹ y ∈ B ⟹
bij_betw (π(inv_into A π y := π x)) (A - {x}) (B - {y})›
by (auto simp: bij_betw_def inj_on_def image_iff)
lemma ldropWhile_eq_LCons_iff: ‹ldropWhile P lxs = LCons x lxs' ⟷ (¬ P x ∧
(∃xs. lxs = lappend (llist_of xs) (LCons x lxs') ∧ (∀x ∈ set xs. P x)))›
proof -
have False
if ‹ldropWhile P lxs = LCons x lxs'› and ‹P x›
using that by (metis lhd_LCons lhd_ldropWhile llist.disc(2) lnull_ldropWhile)
moreover have ‹∃xs. lxs = lappend (llist_of xs) (LCons x lxs') ∧ (∀x∈set xs. P x)›
if ‹ldropWhile P lxs = LCons x lxs'›
using that by (metis eq_LConsD in_lset_lappend_iff lappend_ltakeWhile_ldropWhile
ldropWhile_eq_LNil_iff llist_of_list_of lset_llist_of lset_ltakeWhileD)
ultimately show ?thesis
by (auto simp: ldropWhile_lappend)
qed
lemma ltakeWhile_ldropWhile_decomp:
assumes ‹x ∈ lset lxs›
shows ‹lxs = lappend (ltakeWhile ((≠) x) lxs) (LCons x (ltl (ldropWhile ((≠) x) lxs)))›
proof (subst lappend_ltakeWhile_ldropWhile[symmetric, of lxs ‹(≠) x›], rule arg_cong[where f=‹lappend _›])
from assms show ‹ldropWhile ((≠) x) lxs = LCons x (ltl (ldropWhile ((≠) x) lxs))›
by (cases ‹ldropWhile ((≠) x) lxs›)
(auto simp: ldropWhile_eq_LNil_iff lhd_ldropWhile[where P=‹(≠) x›, simplified, symmetric] dest!: eq_LConsD)
qed
lemma lzip_lmap_same: ‹lzip (lmap f lxs) (lmap g lxs) = lmap (λx. (f x, g x)) lxs›
by (coinduction arbitrary: lxs) auto
lemma llength_not_lnull: ‹¬ lnull lxs ⟹ llength lxs = eSuc (llength (ltl lxs))›
by (auto simp: lnull_def neq_LNil_conv)
primrec ltaken :: ‹nat ⇒ 'a llist ⇒ 'a list› where
‹ltaken 0 lxs = []›
| ‹ltaken (Suc i) lxs = (case lxs of LNil ⇒ [] | LCons x lxs ⇒ x # ltaken i lxs)›
lemma nth_ltaken: ‹m < n ⟹ n ≤ llength lxs ⟹ nth (ltaken n lxs) m = lnth lxs m›
by (induct n arbitrary: m lxs) (auto simp: nth_Cons' gr0_conv_Suc simp flip: eSuc_enat split: llist.splits)
lemma set_ltaken: ‹set (ltaken n lxs) ⊆ lset lxs›
by (induct n arbitrary: lxs) (force split: llist.splits)+
lemma length_ltaken: ‹length (ltaken n lxs) = (if enat n ≤ llength lxs then n else the_enat (llength lxs))›
by (induct n arbitrary: lxs)
(auto simp: enat_0 min_def not_le eSuc_enat enat_0_iff eSuc_enat_iff elim!: less_enatE split: llist.splits)
lemma set_ltaken_conv: ‹n ≤ llength lxs ⟹ set (ltaken n lxs) = lnth lxs ` {0..<n}›
proof (induct n arbitrary: lxs)
case (Suc n)
then show ?case
by (cases lxs)
(force simp flip: eSuc_enat simp: image_iff lnth_LCons' dest: bspec[of _ _ ‹Suc _›])+
qed simp
lemma ltaken_lappend:
‹ltaken n (lappend lxs lys) = (case llength lxs of ∞ ⇒ ltaken n lxs | enat m ⇒ ltaken n lxs @ ltaken (n - m) lys)›
by (induct n arbitrary: lxs) (auto split: enat.splits simp: enat_0_iff eSuc_enat_iff eSuc_eq_infinity_iff split: llist.splits)
lemma ltaken_LNil[simp]: ‹ltaken i LNil = []›
by (cases i) auto
section ‹enat as a Codatatype›