Theory Misc_HLW
section ‹Miscellaneous facts›
theory Misc_HLW
imports
Complex_Main
"HOL-Library.Multiset"
"HOL-Library.FuncSet"
"HOL-Library.Groups_Big_Fun"
"HOL-Library.Poly_Mapping"
"HOL-Library.Landau_Symbols"
"HOL-Combinatorics.Permutations"
"HOL-Computational_Algebra.Computational_Algebra"
begin
lemma set_mset_subset_singletonD:
assumes "set_mset A ⊆ {x}"
shows "A = replicate_mset (size A) x"
using assms by (induction A) auto
lemma image_mset_eq_replicate_msetD:
assumes "image_mset f A = replicate_mset n y"
shows "∀x∈#A. f x = y"
proof -
have "f ` set_mset A = set_mset (image_mset f A)"
by simp
also note assms
finally show ?thesis by (auto split: if_splits)
qed
lemma bij_betw_permutes_compose_left:
assumes "π permutes A"
shows "bij_betw (λσ. π ∘ σ) {σ. σ permutes A} {σ. σ permutes A}"
proof (rule bij_betwI)
show "(∘) π ∈ {σ. σ permutes A} → {σ. σ permutes A}"
by (auto intro: permutes_compose assms)
show "(∘) (inv_into UNIV π) ∈ {σ. σ permutes A} → {σ. σ permutes A}"
by (auto intro: permutes_compose assms permutes_inv)
qed (use permutes_inverses[OF assms] in auto)
lemma bij_betw_compose_left_perm_Pi:
assumes "π permutes B"
shows "bij_betw (λf. (π ∘ f)) (A → B) (A → B)"
proof (rule bij_betwI)
have *: "(λf. (π ∘ f)) ∈ (A → B) → A → B" if π: "π permutes B" for π
by (auto simp: permutes_in_image[OF π])
show "(λf. (π ∘ f)) ∈ (A → B) → A → B"
by (rule *) fact
show "(λf. (inv_into UNIV π ∘ f)) ∈ (A → B) → A → B"
by (intro * permutes_inv) fact
qed (auto simp: permutes_inverses[OF assms] fun_eq_iff)
lemma bij_betw_compose_left_perm_PiE:
assumes "π permutes B"
shows "bij_betw (λf. restrict (π ∘ f) A) (A →⇩E B) (A →⇩E B)"
proof (rule bij_betwI)
have *: "(λf. restrict (π ∘ f) A) ∈ (A →⇩E B) → A →⇩E B" if π: "π permutes B" for π
by (auto simp: permutes_in_image[OF π])
show "(λf. restrict (π ∘ f) A) ∈ (A →⇩E B) → A →⇩E B"
by (rule *) fact
show "(λf. restrict (inv_into UNIV π ∘ f) A) ∈ (A →⇩E B) → A →⇩E B"
by (intro * permutes_inv) fact
qed (auto simp: permutes_inverses[OF assms] fun_eq_iff)
lemma bij_betw_image_mset_set:
assumes "bij_betw f A B"
shows "image_mset f (mset_set A) = mset_set B"
using assms by (simp add: bij_betw_def image_mset_mset_set)
lemma finite_multisets_of_size:
assumes "finite A"
shows "finite {X. set_mset X ⊆ A ∧ size X = n}"
proof (rule finite_subset)
show "{X. set_mset X ⊆ A ∧ size X = n} ⊆ mset ` {xs. set xs ⊆ A ∧ length xs = n}"
proof
fix X assume X: "X ∈ {X. set_mset X ⊆ A ∧ size X = n}"
obtain xs where [simp]: "X = mset xs"
by (metis ex_mset)
thus "X ∈ mset ` {xs. set xs ⊆ A ∧ length xs = n}"
using X by auto
qed
next
show "finite (mset ` {xs. set xs ⊆ A ∧ length xs = n})"
by (intro finite_imageI finite_lists_length_eq assms)
qed
lemma sum_mset_image_mset_sum_mset_image_mset:
"sum_mset (image_mset g (sum_mset (image_mset f A))) =
sum_mset (image_mset (λx. sum_mset (image_mset g (f x))) A)"
by (induction A) auto
lemma sum_mset_image_mset_singleton: "sum_mset (image_mset (λx. {#f x#}) A) = image_mset f A"
by (induction A) auto
lemma sum_mset_conv_sum:
"sum_mset (image_mset f A) = (∑x∈set_mset A. of_nat (count A x) * f x)"
proof (induction A rule: full_multiset_induct)
case (less A)
show ?case
proof (cases "A = {#}")
case False
then obtain x where x: "x ∈# A"
by auto
define n where "n = count A x"
define A' where "A' = filter_mset (λy. y ≠ x) A"
have A_eq: "A = replicate_mset n x + A'"
by (intro multiset_eqI) (auto simp: A'_def n_def)
have [simp]: "x ∉# A'" "count A' x = 0"
by (auto simp: A'_def)
have "n ≠ 0"
using x by (auto simp: n_def)
have "sum_mset (image_mset f A) = of_nat n * f x + sum_mset (image_mset f A')"
by (simp add: A_eq)
also have "A' ⊂# A"
unfolding A'_def using x by (simp add: filter_mset_eq_conv subset_mset_def)
with less.IH have "sum_mset (image_mset f A') = (∑x∈set_mset A'. of_nat (count A' x) * f x)"
by simp
also have "… = (∑x∈set_mset A'. of_nat (count A x) * f x)"
by (intro sum.cong) (auto simp: A_eq)
also have "of_nat n * f x + … = (∑x∈insert x (set_mset A'). of_nat (count A x) * f x)"
by (subst sum.insert) (auto simp: A_eq)
also from ‹n ≠ 0› have "insert x (set_mset A') = set_mset A"
by (auto simp: A_eq)
finally show ?thesis .
qed auto
qed
lemma sum_mset_conv_Sum_any:
"sum_mset (image_mset f A) = Sum_any (λx. of_nat (count A x) * f x)"
proof -
have "sum_mset (image_mset f A) = (∑x∈set_mset A. of_nat (count A x) * f x)"
by (rule sum_mset_conv_sum)
also have "… = Sum_any (λx. of_nat (count A x) * f x)"
proof (rule Sum_any.expand_superset [symmetric])
show "{x. of_nat (count A x) * f x ≠ 0} ⊆ set_mset A"
proof
fix x assume "x ∈ {x. of_nat (count A x) * f x ≠ 0}"
hence "count A x ≠ 0"
by (intro notI) auto
thus "x ∈# A"
by auto
qed
qed auto
finally show ?thesis .
qed
lemma Sum_any_sum_swap:
assumes "finite A" "⋀y. finite {x. f x y ≠ 0}"
shows "Sum_any (λx. sum (f x) A) = (∑y∈A. Sum_any (λx. f x y))"
proof -
have "Sum_any (λx. sum (f x) A) = Sum_any (λx. Sum_any (λy. f x y when y ∈ A))"
unfolding when_def by (subst Sum_any.conditionalize) (use assms in simp_all)
also have "… = Sum_any (λy. Sum_any (λx. f x y when y ∈ A))"
by (intro Sum_any.swap[of "(⋃y∈A. {x. f x y ≠ 0}) × A"] finite_SigmaI finite_UN_I assms) auto
also have "(λy. Sum_any (λx. f x y when y ∈ A)) = (λy. Sum_any (λx. f x y) when y ∈ A)"
by (auto simp: when_def)
also have "Sum_any … = (∑y∈A. Sum_any (λx. f x y))"
unfolding when_def by (subst Sum_any.conditionalize) (use assms in simp_all)
finally show ?thesis .
qed
lemma (in landau_pair) big_power:
assumes "f ∈ L F g"
shows "(λx. f x ^ n) ∈ L F (λx. g x ^ n)"
using big_prod[of "{..<n}" "λ_. f" F "λ_. g"] assms by simp
lemma (in landau_pair) small_power:
assumes "f ∈ l F g" "n > 0"
shows "(λx. f x ^ n) ∈ l F (λx. g x ^ n)"
using assms(2,1)
by (induction rule: nat_induct_non_zero) (auto intro!: small.mult)
lemma pairwise_imp_disjoint_family_on:
assumes "pairwise R A"
assumes "⋀m n. m ∈ A ⟹ n ∈ A ⟹ R m n ⟹ f m ∩ f n = {}"
shows "disjoint_family_on f A"
using assms
unfolding disjoint_family_on_def pairwise_def by blast
lemma (in comm_monoid_set) If_eq:
assumes "y ∈ A" "finite A"
shows "F (λx. g x (if x = y then h1 x else h2 x)) A = f (g y (h1 y)) (F (λx. g x (h2 x)) (A-{y}))"
proof -
have "F (λx. g x (if x = y then h1 x else h2 x)) A =
f (g y (h1 y)) (F (λx. g x (if x = y then h1 x else h2 x)) (A-{y}))"
using assms by (subst remove[of _ y]) auto
also have "F (λx. g x (if x = y then h1 x else h2 x)) (A-{y}) = F (λx. g x (h2 x)) (A-{y})"
by (intro cong) auto
finally show ?thesis by simp
qed
lemma prod_nonzeroI:
fixes f :: "'a ⇒ 'b :: {semiring_no_zero_divisors, comm_semiring_1}"
assumes "⋀x. x ∈ A ⟹ f x ≠ 0"
shows "prod f A ≠ 0"
using assms by (induction rule: infinite_finite_induct) auto
lemma frequently_prime_cofinite: "frequently (prime :: nat ⇒ bool) cofinite"
unfolding INFM_nat_le by (meson bigger_prime less_imp_le)
lemma frequently_eventually_mono:
assumes "frequently Q F" "eventually P F" "⋀x. P x ⟹ Q x ⟹ R x"
shows "frequently R F"
proof (rule frequently_mp[OF _ assms(1)])
show "eventually (λx. Q x ⟶ R x) F"
using assms(2) by eventually_elim (use assms(3) in blast)
qed
lemma bij_betw_Diff:
assumes "bij_betw f A B" "bij_betw f A' B'" "A' ⊆ A" "B' ⊆ B"
shows "bij_betw f (A - A') (B - B')"
unfolding bij_betw_def
proof
have "inj_on f A"
using assms(1) by (auto simp: bij_betw_def)
thus "inj_on f (A - A')"
by (rule inj_on_subset) auto
have "f ` (A - A') = f ` A - f ` A'"
by (intro inj_on_image_set_diff[OF ‹inj_on f A›]) (use ‹A' ⊆ A› in auto)
also have "… = B - B'"
using assms(1,2) by (auto simp: bij_betw_def)
finally show "f` (A - A') = B - B'" .
qed
lemma bij_betw_singleton: "bij_betw f {x} {y} ⟷ f x = y"
by (auto simp: bij_betw_def)
end