Theory Misc
section ‹Auxiliary material›
theory Misc
imports "HOL-Analysis.Analysis"
begin
text ‹Based on @{term sorted_list_of_set} and @{term the_inv_into} we construct a bijection between
a finite set A of type 'a::linorder and a set of natural numbers @{term "{..< card A}"}›
lemma bij_betw_mono_on_the_inv_into:
fixes A::"'a::linorder set" and B::"'b::linorder set"
assumes b: "bij_betw f A B" and m: "mono_on A f"
shows "mono_on B (the_inv_into A f)"
proof (rule ccontr)
assume "¬ mono_on B (the_inv_into A f)"
then have "∃r s. r ∈ B ∧ s ∈ B ∧ r ≤ s ∧ ¬ the_inv_into A f s ≥ the_inv_into A f r"
unfolding mono_on_def by blast
then obtain r s where rs: "r ∈ B" "s ∈ B" "r ≤ s" "the_inv_into A f s < the_inv_into A f r"
by fastforce
have f: "f (the_inv_into A f b) = b" if "b ∈ B" for b
using that assms f_the_inv_into_f_bij_betw by metis
have "the_inv_into A f s ∈ A" "the_inv_into A f r ∈ A"
using rs assms by (auto simp add: bij_betw_def the_inv_into_into)
then have "f (the_inv_into A f s) ≤ f (the_inv_into A f r)"
using rs by (intro mono_onD[OF m]) (auto)
then have "r = s"
using rs f by simp
then show False
using rs by auto
qed
lemma rev_removeAll_removeAll_rev: "rev (removeAll x xs) = removeAll x (rev xs)"
by (simp add: removeAll_filter_not_eq rev_filter)
lemma sorted_list_of_set_Min_Cons:
assumes "finite A" "A ≠ {}"
shows "sorted_list_of_set A = Min A # sorted_list_of_set (A - {Min A})"
proof -
have *: "A = insert (Min A) A"
using assms Min_in by (auto)
then have "sorted_list_of_set A = insort (Min A) (sorted_list_of_set (A - {Min A}))"
using assms by (subst *, intro sorted_list_of_set_insert_remove) auto
also have "… = Min A # sorted_list_of_set (A - {Min A})"
using assms by (intro insort_is_Cons) (auto)
finally show ?thesis
by simp
qed
lemma sorted_list_of_set_filter:
assumes "finite A"
shows "sorted_list_of_set ({x∈A. P x}) = filter P (sorted_list_of_set A)"
using assms proof (induction "sorted_list_of_set A" arbitrary: A)
case (Cons x xs)
have x: "x ∈ A"
using Cons sorted_list_of_set list.set_intros(1) by metis
have "sorted_list_of_set A = Min A # sorted_list_of_set (A - {Min A})"
using Cons by (intro sorted_list_of_set_Min_Cons) auto
then have 1: "x = Min A" "xs = sorted_list_of_set (A - {x})"
using Cons by auto
{ assume Px: "P x"
have 2: "sorted_list_of_set {x ∈ A. P x} = Min {x ∈ A. P x} # sorted_list_of_set ({x ∈ A. P x} - {Min {x ∈ A. P x}})"
using Px Cons 1 sorted_list_of_set_eq_Nil_iff
by (intro sorted_list_of_set_Min_Cons) fastforce+
also have 3: "Min {x ∈ A. P x} = x"
using Cons 1 Px x by (auto intro!: Min_eqI)
also have 4: "{x ∈ A. P x} - {x} = {y ∈ A - {x}. P y}"
by blast
also have 5: "sorted_list_of_set {y ∈ A - {x}. P y} = filter P (sorted_list_of_set (A - {x}))"
using 1 Cons by (intro Cons) (auto)
also have "… = filter P xs"
using 1 by simp
also have "filter P (sorted_list_of_set A) = x # filter P xs"
using Px by (simp flip: ‹x # xs = sorted_list_of_set A›)
finally have ?case
by auto }
moreover
{ assume Px: "¬ P x"
then have "{x ∈ A. P x} = {y ∈ A - {x}. P y}"
by blast
also have "sorted_list_of_set … = filter P (sorted_list_of_set (A - {x}))"
using 1 Cons by (intro Cons) auto
also have "filter P (sorted_list_of_set (A - {x})) = filter P (sorted_list_of_set A)"
using 1 Px by (simp flip: ‹x # xs = sorted_list_of_set A›)
finally have ?case
by simp }
ultimately show ?case
by blast
qed (use sorted_list_of_set_eq_Nil_iff in fastforce)
lemma sorted_list_of_set_Max_snoc:
assumes "finite A" "A ≠ {}"
shows "sorted_list_of_set A = sorted_list_of_set (A - {Max A}) @ [Max A]"
proof -
have *: "A = insert (Max A) A"
using assms Max_in by (auto)
then have "sorted_list_of_set A = insort (Max A) (sorted_list_of_set (A - {Max A}))"
using assms by (subst *, intro sorted_list_of_set_insert_remove) auto
also have "… = sorted_list_of_set (A - {Max A}) @ [Max A]"
using assms by (intro sorted_insort_is_snoc) (auto)
finally show ?thesis
by simp
qed
lemma sorted_list_of_set_image:
assumes "mono_on A g" "inj_on g A"
shows "(sorted_list_of_set (g ` A)) = map g (sorted_list_of_set A)"
proof (cases "finite A")
case True
then show ?thesis
using assms proof (induction "sorted_list_of_set A" arbitrary: A)
case Nil
then show ?case
using sorted_list_of_set_eq_Nil_iff by fastforce
next
case (Cons x xs A)
have not_empty_A: "A ≠ {}"
using Cons sorted_list_of_set_eq_Nil_iff by auto
have *: "Min (g ` A) = g (Min A)"
proof -
have "g (Min A) ≤ g a" if "a ∈ A" for a
using that Cons Min_in Min_le not_empty_A by (auto intro!: mono_onD[of _ g])
then show ?thesis
using Cons not_empty_A by (intro Min_eqI) auto
qed
have "g ` A ≠ {}" "finite (g ` A)"
using Cons by auto
then have "(sorted_list_of_set (g ` A)) =
Min (g ` A) # sorted_list_of_set ((g ` A) - {Min (g ` A)})"
by (auto simp add: sorted_list_of_set_Min_Cons)
also have "(g ` A) - {Min (g ` A)} = g ` (A - {Min A})"
using Cons Min_in not_empty_A * by (subst inj_on_image_set_diff[of _ A]) auto
also have "sorted_list_of_set (g ` (A - {Min A})) = map g (sorted_list_of_set (A - {Min A}))"
using not_empty_A Cons mono_on_subset[of A _ "A - {Min A}"] inj_on_subset[of _ A "A - {Min A}"]
by (intro Cons) (auto simp add: sorted_list_of_set_Min_Cons)
finally show ?case
using Cons not_empty_A * by (auto simp add: sorted_list_of_set_Min_Cons)
qed
next
case False
then show ?thesis
using assms by (simp add: finite_image_iff)
qed
lemma sorted_list_of_set_length: "length (sorted_list_of_set A) = card A"
using distinct_card sorted_list_of_set[of A] by (cases "finite A") fastforce+
lemma sorted_list_of_set_bij_betw:
assumes "finite A"
shows "bij_betw (λn. sorted_list_of_set A ! n) {..<card A} A"
by (rule bij_betw_nth) (fastforce simp add: assms sorted_list_of_set_length)+
lemma nth_mono_on:
assumes "sorted xs" "distinct xs" "set xs = A"
shows "mono_on {..<card A} (λn. xs ! n)"
using assms by (intro mono_onI sorted_nth_mono) (auto simp add: distinct_card)
lemma sorted_list_of_set_mono_on:
"finite A ⟹ mono_on {..<card A} (λn. sorted_list_of_set A ! n)"
by (rule nth_mono_on) (auto)
definition bij_mono_map_set_to_nat :: "'a::linorder set ⇒ 'a ⇒ nat" where
"bij_mono_map_set_to_nat A =
(λx. if x ∈ A then the_inv_into {..<card A} ((!) (sorted_list_of_set A)) x
else card A)"
lemma bij_mono_map_set_to_nat:
assumes "finite A"
shows "bij_betw (bij_mono_map_set_to_nat A) A {..<card A}"
"mono_on A (bij_mono_map_set_to_nat A)"
"(bij_mono_map_set_to_nat A) ` A = {..<card A}"
proof -
let ?f = "bij_mono_map_set_to_nat A"
have "bij_betw (the_inv_into {..<card A} ((!) (sorted_list_of_set A))) A {..<card A}"
using assms sorted_list_of_set_bij_betw bij_betw_the_inv_into by blast
moreover have "bij_betw (the_inv_into {..<card A} ((!) (sorted_list_of_set A))) A {..<card A}
= bij_betw ?f A {..<card A}"
unfolding bij_mono_map_set_to_nat_def by (rule bij_betw_cong) simp
ultimately show *: "bij_betw (bij_mono_map_set_to_nat A) A {..<card A}"
by blast
have "mono_on A (the_inv_into {..<card A} ((!) (sorted_list_of_set A)))"
using assms sorted_list_of_set_bij_betw
sorted_list_of_set_mono_on by (intro bij_betw_mono_on_the_inv_into) auto
then show "mono_on A (bij_mono_map_set_to_nat A)"
unfolding bij_mono_map_set_to_nat_def using mono_onD by (intro mono_onI) (auto)
show "?f ` A = {..<card A}"
using assms bij_betw_imp_surj_on * by blast
qed
end