Email Gateway (Aug 22 2022 at 11:04): Email Gateway (Aug 22 2022 at 11:04):From: Thomas Sewell <thomas.sewell@nicta.com.au>
I was playing around with a multiset-related problem, and I feel these
lemmas are missing from Library/Multiset.
The first two are trivia, but the last one is really useful. It's a
variant of "properties_for_sort_key", but it's much easier to apply, in
my opinion. The rest of Multiset.thy sort of hints that injectivity of
the sort key on the set of values to be sorted is a normal thing to
assume, and given that, one of the premises of "properties_for_sort_key"
is redundant, which is the point of this proof.
lemma inj_on_filter_key_eq:
"inj_on s (insert k (set xs)) ⟹ [x←xs . s k = s x] = filter (op = k) xs"
apply (induct xs)
apply simp
apply (drule meta_mp, erule subset_inj_on)
apply auto[1]
apply (drule_tac x=k and y=a in inj_on_iff, auto)
done
lemma filter_eq_replicate_count_multiset:
"filter (op = k) xs = replicate (count (multiset_of xs) k) k"
by (induct xs, auto)
lemma sort_key_multiset_eq:
assumes multiset: "multiset_of xs = multiset_of ys"
and inj_on: "inj_on f (set xs)"
shows "sort_key f xs = sort_key f ys"
proof -
from multiset have set:
"set xs = set ys"
by (metis set_of_multiset_of)
note filter = inj_on_filter_key_eq[OF subset_inj_on, OF inj_on]
show ?thesis
apply (rule properties_for_sort_key)
apply (simp add: multiset)
apply (simp add: filter set)
apply (simp add: filter_eq_replicate_count_multiset multiset)
apply simp
done
qed
Cheers,
Thomas.
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 22 2022 at 11:06):From: Thomas Sewell <thomas.sewell@nicta.com.au>
Amending my previous email, I note that my final lemma diverges more
than necessary from "properties_for_sort_key", which concludes "sort_key
f xs = ys". I still think that a "sort_key f xs = sort_key f ys" form is
useful, since that's what I first searched for. Here's an amended
version with both.
lemma inj_on_filter_key_eq:
"inj_on s (insert k (set xs)) ⟹ [x←xs . s k = s x] = filter (op = k) xs"
apply (induct xs)
apply simp
apply (drule meta_mp, erule subset_inj_on)
apply auto[1]
apply (drule_tac x=k and y=a in inj_on_iff, auto)
done
lemma filter_eq_replicate_count_multiset:
"filter (op = k) xs = replicate (count (multiset_of xs) k) k"
by (induct xs, auto)
lemma sort_key_inj_key_eq:
assumes multiset: "multiset_of xs = multiset_of ys"
and inj_on: "inj_on f (set xs)"
and ys: "sorted (map f ys)"
shows "sort_key f xs = ys"
proof -
from multiset have set:
"set xs = set ys"
by (metis set_of_multiset_of)
note filter = inj_on_filter_key_eq[OF subset_inj_on, OF inj_on]
note propk = properties_for_sort_key[OF multiset[symmetric] _ ys]
show ?thesis
apply (rule propk)
apply (simp add: filter set)
apply (simp add: filter_eq_replicate_count_multiset multiset)
done
qed
lemmas sort_key_eq_sort_key
= sort_key_inj_key_eq[where f=f and ys="sort_key f ys",
simplified] for f ys
Cheers,
Thomas.
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Last updated: Apr 26 2024 at 20:16 UTC