Read about our upcoming Code of Conduct on this issue

Commit 7159e427 authored by Lawrence Paulson's avatar Lawrence Paulson
Browse files

new entry Hermite_Lindemann

parent 39b6774669ae
(*
File: Algebraic_Integer_Divisibility.thy
Author: Manuel Eberl, TU München
*)
section \<open>Divisibility of algebraic integers\<close>
theory Algebraic_Integer_Divisibility
imports "Algebraic_Numbers.Algebraic_Numbers"
begin
text \<open>
In this section, we define a notion of divisibility of algebraic integers: \<open>y\<close> is divisible
by \<open>x\<close> if \<open>y / x\<close> is an algebraic integer (or if \<open>x\<close> and \<open>y\<close> are both zero).
Technically, the definition does not require \<open>x\<close> and \<open>y\<close> to be algebraic integers themselves,
but we will always use it that way (in fact, in our case \<open>x\<close> will always be a rational integer).
\<close>
definition alg_dvd :: "'a :: field \<Rightarrow> 'a \<Rightarrow> bool" (infix "alg'_dvd" 50) where
"x alg_dvd y \<longleftrightarrow> (x = 0 \<longrightarrow> y = 0) \<and> algebraic_int (y / x)"
lemma alg_dvd_imp_algebraic_int:
fixes x y :: "'a :: field_char_0"
shows "x alg_dvd y \<Longrightarrow> algebraic_int x \<Longrightarrow> algebraic_int y"
using algebraic_int_times[of "y / x" x] by (auto simp: alg_dvd_def)
lemma alg_dvd_0_left_iff [simp]: "0 alg_dvd x \<longleftrightarrow> x = 0"
by (auto simp: alg_dvd_def)
lemma alg_dvd_0_right [iff]: "x alg_dvd 0"
by (auto simp: alg_dvd_def)
lemma one_alg_dvd_iff [simp]: "1 alg_dvd x \<longleftrightarrow> algebraic_int x"
by (auto simp: alg_dvd_def)
lemma alg_dvd_of_int [intro]:
assumes "x dvd y"
shows "of_int x alg_dvd of_int y"
proof (cases "of_int x = (0 :: 'a)")
case False
from assms obtain z where z: "y = x * z"
by (elim dvdE)
have "algebraic_int (of_int z)"
by auto
also have "of_int z = of_int y / (of_int x :: 'a)"
using False by (simp add: z field_simps)
finally show ?thesis
using False by (simp add: alg_dvd_def)
qed (use assms in \<open>auto simp: alg_dvd_def\<close>)
lemma alg_dvd_of_nat [intro]:
assumes "x dvd y"
shows "of_nat x alg_dvd of_nat y"
using alg_dvd_of_int[of "int x" "int y"] assms by simp
lemma alg_dvd_of_int_iff [simp]:
"(of_int x :: 'a :: field_char_0) alg_dvd of_int y \<longleftrightarrow> x dvd y"
proof
assume "(of_int x :: 'a) alg_dvd of_int y"
hence "of_int y / (of_int x :: 'a) \<in> \<int>" and nz: "of_int x = (0::'a) \<longrightarrow> of_int y = (0::'a)"
by (auto simp: alg_dvd_def dest!: rational_algebraic_int_is_int)
then obtain n where "of_int y / of_int x = (of_int n :: 'a)"
by (elim Ints_cases)
hence "of_int y = (of_int (x * n) :: 'a)"
unfolding of_int_mult using nz by (auto simp: field_simps)
hence "y = x * n"
by (subst (asm) of_int_eq_iff)
thus "x dvd y"
by auto
qed blast
lemma alg_dvd_of_nat_iff [simp]:
"(of_nat x :: 'a :: field_char_0) alg_dvd of_nat y \<longleftrightarrow> x dvd y"
proof -
have "(of_int (int x) :: 'a) alg_dvd of_int (int y) \<longleftrightarrow> x dvd y"
by (subst alg_dvd_of_int_iff) auto
thus ?thesis unfolding of_int_of_nat_eq .
qed
lemma alg_dvd_add [intro]:
fixes x y z :: "'a :: field_char_0"
shows "x alg_dvd y \<Longrightarrow> x alg_dvd z \<Longrightarrow> x alg_dvd (y + z)"
unfolding alg_dvd_def by (auto simp: add_divide_distrib)
lemma alg_dvd_uminus_right [intro]: "x alg_dvd y \<Longrightarrow> x alg_dvd -y"
by (auto simp: alg_dvd_def)
lemma alg_dvd_uminus_right_iff [simp]: "x alg_dvd -y \<longleftrightarrow> x alg_dvd y"
using alg_dvd_uminus_right[of x y] alg_dvd_uminus_right[of x "-y"] by auto
lemma alg_dvd_diff [intro]:
fixes x y z :: "'a :: field_char_0"
shows "x alg_dvd y \<Longrightarrow> x alg_dvd z \<Longrightarrow> x alg_dvd (y - z)"
unfolding alg_dvd_def by (auto simp: diff_divide_distrib)
lemma alg_dvd_triv_left [intro]: "algebraic_int y \<Longrightarrow> x alg_dvd x * y"
by (auto simp: alg_dvd_def)
lemma alg_dvd_triv_right [intro]: "algebraic_int x \<Longrightarrow> y alg_dvd x * y"
by (auto simp: alg_dvd_def)
lemma alg_dvd_triv_left_iff: "x alg_dvd x * y \<longleftrightarrow> x = 0 \<or> algebraic_int y"
by (auto simp: alg_dvd_def)
lemma alg_dvd_triv_right_iff: "y alg_dvd x * y \<longleftrightarrow> y = 0 \<or> algebraic_int x"
by (auto simp: alg_dvd_def)
lemma alg_dvd_triv_left_iff' [simp]: "x \<noteq> 0 \<Longrightarrow> x alg_dvd x * y \<longleftrightarrow> algebraic_int y"
by (simp add: alg_dvd_triv_left_iff)
lemma alg_dvd_triv_right_iff' [simp]: "y \<noteq> 0 \<Longrightarrow> y alg_dvd x * y \<longleftrightarrow> algebraic_int x"
by (simp add: alg_dvd_triv_right_iff)
lemma alg_dvd_trans [trans]:
fixes x y z :: "'a :: field_char_0"
shows "x alg_dvd y \<Longrightarrow> y alg_dvd z \<Longrightarrow> x alg_dvd z"
using algebraic_int_times[of "y / x" "z / y"] by (auto simp: alg_dvd_def)
lemma alg_dvd_mono [simp]:
fixes a b c d :: "'a :: field_char_0"
shows "a alg_dvd c \<Longrightarrow> b alg_dvd d \<Longrightarrow> (a * b) alg_dvd (c * d)"
using algebraic_int_times[of "c / a" "d / b"] by (auto simp: alg_dvd_def)
lemma alg_dvd_mult [simp]:
fixes a b c :: "'a :: field_char_0"
shows "a alg_dvd c \<Longrightarrow> algebraic_int b \<Longrightarrow> a alg_dvd (b * c)"
using alg_dvd_mono[of a c 1 b] by (auto simp: mult.commute)
lemma alg_dvd_mult2 [simp]:
fixes a b c :: "'a :: field_char_0"
shows "a alg_dvd b \<Longrightarrow> algebraic_int c \<Longrightarrow> a alg_dvd (b * c)"
using alg_dvd_mult[of a b c] by (simp add: mult.commute)
text \<open>
A crucial theorem: if an integer \<open>x\<close> divides a rational number \<open>y\<close>, then \<open>y\<close> is in fact
also an integer, and that integer is a multiple of \<open>x\<close>.
\<close>
lemma alg_dvd_int_rat:
fixes y :: "'a :: field_char_0"
assumes "of_int x alg_dvd y" and "y \<in> \<rat>"
shows "\<exists>n. y = of_int n \<and> x dvd n"
proof (cases "x = 0")
case False
have "y / of_int x \<in> \<int>"
by (intro rational_algebraic_int_is_int) (use assms in \<open>auto simp: alg_dvd_def\<close>)
then obtain n where n: "of_int n = y / (of_int x :: 'a)"
by (elim Ints_cases) auto
hence "y = of_int (n * x)"
using False by (simp add: field_simps)
thus ?thesis by (intro exI[of _ "x * n"]) auto
qed (use assms in auto)
lemma prod_alg_dvd_prod:
fixes f :: "'a \<Rightarrow> 'b :: field_char_0"
assumes "\<And>x. x \<in> A \<Longrightarrow> f x alg_dvd g x"
shows "prod f A alg_dvd prod g A"
using assms by (induction A rule: infinite_finite_induct) auto
lemma alg_dvd_sum:
fixes f :: "'a \<Rightarrow> 'b :: field_char_0"
assumes "\<And>x. x \<in> A \<Longrightarrow> y alg_dvd f x"
shows "y alg_dvd sum f A"
using assms by (induction A rule: infinite_finite_induct) auto
lemma not_alg_dvd_sum:
fixes f :: "'a \<Rightarrow> 'b :: field_char_0"
assumes "\<And>x. x \<in> A-{x'} \<Longrightarrow> y alg_dvd f x"
assumes "\<not>y alg_dvd f x'"
assumes "x' \<in> A" "finite A"
shows "\<not>y alg_dvd sum f A"
proof
assume *: "y alg_dvd sum f A"
have "y alg_dvd sum f A - sum f (A - {x'})"
using \<open>x' \<in> A\<close> by (intro alg_dvd_diff[OF * alg_dvd_sum] assms) auto
also have "\<dots> = sum f (A - (A - {x'}))"
using assms by (subst sum_diff) auto
also have "A - (A - {x'}) = {x'}"
using assms by auto
finally show False using assms by simp
qed
lemma fact_dvd_pochhammer:
assumes "m \<le> n + 1"
shows "fact m dvd pochhammer (int n - int m + 1) m"
proof -
have "(real n gchoose m) * fact m = of_int (pochhammer (int n - int m + 1) m)"
by (simp add: gbinomial_pochhammer' pochhammer_of_int [symmetric])
also have "(real n gchoose m) * fact m = of_int (int (n choose m) * fact m)"
by (simp add: binomial_gbinomial)
finally have "int (n choose m) * fact m = pochhammer (int n - int m + 1) m"
by (subst (asm) of_int_eq_iff)
from this [symmetric] show ?thesis by simp
qed
lemma coeff_higher_pderiv:
"coeff ((pderiv ^^ m) f) n = pochhammer (of_nat (Suc n)) m * coeff f (n + m)"
by (induction m arbitrary: n) (simp_all add: coeff_pderiv pochhammer_rec algebra_simps)
lemma fact_alg_dvd_poly_higher_pderiv:
fixes p :: "'a :: field_char_0 poly"
assumes "\<And>i. algebraic_int (poly.coeff p i)" "algebraic_int x" "m \<le> k"
shows "fact m alg_dvd poly ((pderiv ^^ k) p) x"
unfolding poly_altdef
proof (intro alg_dvd_sum, goal_cases)
case (1 i)
have "(of_int (fact m) :: 'a) alg_dvd (of_int (fact k))"
by (intro alg_dvd_of_int fact_dvd assms)
also have "(of_int (fact k) :: 'a) alg_dvd of_int (pochhammer (int i + 1) k)"
using fact_dvd_pochhammer[of k "i + k"]
by (intro alg_dvd_of_int fact_dvd_pochhammer) (auto simp: algebra_simps)
finally have "fact m alg_dvd (pochhammer (of_nat i + 1) k :: 'a)"
by (simp flip: pochhammer_of_int)
also have "\<dots> alg_dvd pochhammer (of_nat i + 1) k * poly.coeff p (i + k)"
by (rule alg_dvd_triv_left) (rule assms)
also have "\<dots> = poly.coeff ((pderiv ^^ k) p) i"
unfolding coeff_higher_pderiv by (simp add: add_ac flip: pochhammer_of_int)
also have "\<dots> alg_dvd poly.coeff ((pderiv ^^ k) p) i * x ^ i"
by (intro alg_dvd_triv_left algebraic_int_power assms)
finally show ?case .
qed
end
\ No newline at end of file
(*
File: Complex_Lexorder.thy
Author: Manuel Eberl, TU München
*)
section \<open>The lexicographic ordering on complex numbers\<close>
theory Complex_Lexorder
imports Complex_Main "HOL-Library.Multiset"
begin
text \<open>
We define a lexicographic order on the complex numbers, comparing first the real parts
and, if they are equal, the imaginary parts. This ordering is of course not compatible with
multiplication, but it is compatible with addition.
\<close>
definition less_eq_complex_lex (infix "\<le>\<^sub>\<complex>" 50) where
"less_eq_complex_lex x y \<longleftrightarrow> Re x < Re y \<or> Re x = Re y \<and> Im x \<le> Im y"
definition less_complex_lex (infix "<\<^sub>\<complex>" 50) where
"less_complex_lex x y \<longleftrightarrow> Re x < Re y \<or> Re x = Re y \<and> Im x < Im y"
interpretation complex_lex:
linordered_ab_group_add "(+)" 0 "(-)" "uminus" less_eq_complex_lex less_complex_lex
by standard (auto simp: less_eq_complex_lex_def less_complex_lex_def complex_eq_iff)
lemmas [trans] =
complex_lex.order.trans complex_lex.less_le_trans
complex_lex.less_trans complex_lex.le_less_trans
lemma (in ordered_comm_monoid_add) sum_mono_complex_lex:
"(\<And>i. i\<in>K \<Longrightarrow> f i \<le>\<^sub>\<complex> g i) \<Longrightarrow> (\<Sum>i\<in>K. f i) \<le>\<^sub>\<complex> (\<Sum>i\<in>K. g i)"
by (induct K rule: infinite_finite_induct) (use complex_lex.add_mono in auto)
lemma sum_strict_mono_ex1_complex_lex:
fixes f g :: "'i \<Rightarrow> complex"
assumes "finite A"
and "\<forall>x\<in>A. f x \<le>\<^sub>\<complex> g x"
and "\<exists>a\<in>A. f a <\<^sub>\<complex> g a"
shows "sum f A <\<^sub>\<complex> sum g A"
proof-
from assms(3) obtain a where a: "a \<in> A" "f a <\<^sub>\<complex> g a" by blast
have "sum f A = sum f ((A - {a}) \<union> {a})"
by (simp add: insert_absorb[OF \<open>a \<in> A\<close>])
also have "\<dots> = sum f (A - {a}) + sum f {a}"
using \<open>finite A\<close> by (subst sum.union_disjoint) auto
also have "\<dots> \<le>\<^sub>\<complex> sum g (A - {a}) + sum f {a}"
by (intro complex_lex.add_mono sum_mono_complex_lex) (simp_all add: assms)
also have "\<dots> <\<^sub>\<complex> sum g (A - {a}) + sum g {a}"
using a by (intro complex_lex.add_strict_left_mono) auto
also have "\<dots> = sum g ((A - {a}) \<union> {a})"
using \<open>finite A\<close> by (subst sum.union_disjoint[symmetric]) auto
also have "\<dots> = sum g A" by (simp add: insert_absorb[OF \<open>a \<in> A\<close>])
finally show ?thesis
by simp
qed
lemma sum_list_mono_complex_lex:
assumes "list_all2 (\<le>\<^sub>\<complex>) xs ys"
shows "sum_list xs \<le>\<^sub>\<complex> sum_list ys"
using assms by induction (auto intro: complex_lex.add_mono)
lemma sum_mset_mono_complex_lex:
assumes "rel_mset (\<le>\<^sub>\<complex>) A B"
shows "sum_mset A \<le>\<^sub>\<complex> sum_mset B"
using assms by (auto simp: rel_mset_def sum_mset_sum_list intro: sum_list_mono_complex_lex)
lemma rel_msetI:
assumes "list_all2 R xs ys" "mset xs = A" "mset ys = B"
shows "rel_mset R A B"
using assms by (auto simp: rel_mset_def)
lemma mset_replicate [simp]: "mset (replicate n x) = replicate_mset n x"
by (induction n) auto
lemma rel_mset_replicate_mset_right:
assumes "\<And>x. x \<in># A \<Longrightarrow> R x y" "size A = n"
shows "rel_mset R A (replicate_mset n y)"
proof -
obtain xs where [simp]: "A = mset xs"
by (metis ex_mset)
from assms have "\<forall>x\<in>set xs. R x y"
by auto
hence "list_all2 R xs (replicate (length xs) y)"
by (induction xs) auto
with assms(2) show ?thesis
by (intro rel_msetI[of R xs "replicate n y"]) auto
qed
end
\ No newline at end of file
This diff is collapsed.
(*
File: Min_Int_Poly.thy
Author: Manuel Eberl, TU München
*)
section \<open>The minimal polynomial of an algebraic number\<close>
theory Min_Int_Poly
imports
"Algebraic_Numbers.Algebraic_Numbers"
"HOL-Computational_Algebra.Computational_Algebra"
More_Polynomial_HLW
begin
text \<open>
Given an algebraic number \<open>x\<close> in a field, the minimal polynomial is the unique irreducible
integer polynomial with positive leading coefficient that has \<open>x\<close> as a root.
Note that we assume characteristic 0 since the material upon which all of this builds also
assumes it.
\<close>
(* TODO Move *)
definition min_int_poly :: "'a :: field_char_0 \<Rightarrow> int poly" where
"min_int_poly x =
(if algebraic x then THE p. p represents x \<and> irreducible p \<and> Polynomial.lead_coeff p > 0
else [:0, 1:])"
lemma
fixes x :: "'a :: {field_char_0, field_gcd}"
shows min_int_poly_represents [intro]: "algebraic x \<Longrightarrow> min_int_poly x represents x"
and min_int_poly_irreducible [intro]: "irreducible (min_int_poly x)"
and lead_coeff_min_int_poly_pos: "Polynomial.lead_coeff (min_int_poly x) > 0"
proof -
note * = theI'[OF algebraic_imp_represents_unique, of x]
show "min_int_poly x represents x" if "algebraic x"
using *[OF that] by (simp add: that min_int_poly_def)
have "irreducible [:0, 1::int:]"
by (rule irreducible_linear_poly) auto
thus "irreducible (min_int_poly x)"
using * by (auto simp: min_int_poly_def)
show "Polynomial.lead_coeff (min_int_poly x) > 0"
using * by (auto simp: min_int_poly_def)
qed
lemma
fixes x :: "'a :: {field_char_0, field_gcd}"
shows degree_min_int_poly_pos [intro]: "Polynomial.degree (min_int_poly x) > 0"
and degree_min_int_poly_nonzero [simp]: "Polynomial.degree (min_int_poly x) \<noteq> 0"
proof -
show "Polynomial.degree (min_int_poly x) > 0"
proof (cases "algebraic x")
case True
hence "min_int_poly x represents x"
by auto
thus ?thesis by blast
qed (auto simp: min_int_poly_def)
thus "Polynomial.degree (min_int_poly x) \<noteq> 0"
by blast
qed
lemma min_int_poly_squarefree [intro]:
fixes x :: "'a :: {field_char_0, field_gcd}"
shows "squarefree (min_int_poly x)"
by (rule irreducible_imp_squarefree) auto
lemma min_int_poly_primitive [intro]:
fixes x :: "'a :: {field_char_0, field_gcd}"
shows "primitive (min_int_poly x)"
by (rule irreducible_imp_primitive) auto
lemma min_int_poly_content [simp]:
fixes x :: "'a :: {field_char_0, field_gcd}"
shows "content (min_int_poly x) = 1"
using min_int_poly_primitive[of x] by (simp add: primitive_def)
lemma ipoly_min_int_poly [simp]:
"algebraic x \<Longrightarrow> ipoly (min_int_poly x) (x :: 'a :: {field_gcd, field_char_0}) = 0"
using min_int_poly_represents[of x] by (auto simp: represents_def)
lemma min_int_poly_nonzero [simp]:
fixes x :: "'a :: {field_char_0, field_gcd}"
shows "min_int_poly x \<noteq> 0"
using lead_coeff_min_int_poly_pos[of x] by auto
lemma min_int_poly_normalize [simp]:
fixes x :: "'a :: {field_char_0, field_gcd}"
shows "normalize (min_int_poly x) = min_int_poly x"
unfolding normalize_poly_def using lead_coeff_min_int_poly_pos[of x] by simp
lemma min_int_poly_prime_elem [intro]:
fixes x :: "'a :: {field_char_0, field_gcd}"
shows "prime_elem (min_int_poly x)"
using min_int_poly_irreducible[of x] by blast
lemma min_int_poly_prime [intro]:
fixes x :: "'a :: {field_char_0, field_gcd}"
shows "prime (min_int_poly x)"
using min_int_poly_prime_elem[of x]
by (simp only: prime_normalize_iff [symmetric] min_int_poly_normalize)
lemma min_int_poly_unique:
fixes x :: "'a :: {field_char_0, field_gcd}"
assumes "p represents x" "irreducible p" "Polynomial.lead_coeff p > 0"
shows "min_int_poly x = p"
proof -
from assms(1) have x: "algebraic x"
using algebraic_iff_represents by blast
thus ?thesis
using the1_equality[OF algebraic_imp_represents_unique[OF x], of p] assms
unfolding min_int_poly_def by auto
qed
lemma min_int_poly_of_int [simp]:
"min_int_poly (of_int n :: 'a :: {field_char_0, field_gcd}) = [:-of_int n, 1:]"
by (intro min_int_poly_unique irreducible_linear_poly) auto
lemma min_int_poly_of_nat [simp]:
"min_int_poly (of_nat n :: 'a :: {field_char_0, field_gcd}) = [:-of_nat n, 1:]"
using min_int_poly_of_int[of "int n"] by (simp del: min_int_poly_of_int)
lemma min_int_poly_0 [simp]: "min_int_poly (0 :: 'a :: {field_char_0, field_gcd}) = [:0, 1:]"
using min_int_poly_of_int[of 0] unfolding of_int_0 by simp
lemma min_int_poly_1 [simp]: "min_int_poly (1 :: 'a :: {field_char_0, field_gcd}) = [:-1, 1:]"
using min_int_poly_of_int[of 1] unfolding of_int_1 by simp
lemma poly_min_int_poly_0_eq_0_iff [simp]:
fixes x :: "'a :: {field_char_0, field_gcd}"
assumes "algebraic x"
shows "poly (min_int_poly x) 0 = 0 \<longleftrightarrow> x = 0"
proof
assume *: "poly (min_int_poly x) 0 = 0"
show "x = 0"
proof (rule ccontr)
assume "x \<noteq> 0"
hence "poly (min_int_poly x) 0 \<noteq> 0"
using assms by (intro represents_irr_non_0) auto
with * show False by contradiction
qed
qed auto
lemma min_int_poly_conv_Gcd:
fixes x :: "'a :: {field_char_0, field_gcd}"
assumes "algebraic x"
shows "min_int_poly x = Gcd {p. p \<noteq> 0 \<and> p represents x}"
proof (rule sym, rule Gcd_eqI, (safe)?)
fix p assume p: "\<And>q. q \<in> {p. p \<noteq> 0 \<and> p represents x} \<Longrightarrow> p dvd q"
show "p dvd min_int_poly x"
using assms by (intro p) auto
next
fix p assume p: "p \<noteq> 0" "p represents x"
have "min_int_poly x represents x"
using assms by auto
hence "poly (gcd (of_int_poly (min_int_poly x)) (of_int_poly p)) x = 0"
using p by (intro poly_gcd_eq_0I) auto
hence "ipoly (gcd (min_int_poly x) p) x = 0"
by (subst (asm) gcd_of_int_poly) auto
hence "gcd (min_int_poly x) p represents x"
using p unfolding represents_def by auto
have "min_int_poly x dvd gcd (min_int_poly x) p \<or> is_unit (gcd (min_int_poly x) p)"
by (intro irreducibleD') auto
moreover from \<open>gcd (min_int_poly x) p represents x\<close> have "\<not>is_unit (gcd (min_int_poly x) p)"
by (auto simp: represents_def)
ultimately have "min_int_poly x dvd gcd (min_int_poly x) p"
by blast
also have "\<dots> dvd p"
by blast
finally show "min_int_poly x dvd p" .
qed auto
lemma min_int_poly_eqI:
fixes x :: "'a :: {field_char_0, field_gcd}"
assumes "p represents x" "irreducible p" "Polynomial.lead_coeff p \<ge> 0"
shows "min_int_poly x = p"
proof -
from assms have [simp]: "p \<noteq> 0"
by auto
have "Polynomial.lead_coeff p \<noteq> 0"
by auto
with assms(3) have "Polynomial.lead_coeff p > 0"
by linarith
moreover have "algebraic x"
using \<open>p represents x\<close> by (meson algebraic_iff_represents)
ultimately show ?thesis
unfolding min_int_poly_def
using the1_equality[OF algebraic_imp_represents_unique[OF \<open>algebraic x\<close>], of p] assms by auto
qed
end
\ No newline at end of file
(*
File: Misc_HLW.thy
Author: Manuel Eberl, TU München
*)
section \<open>Miscellaneous facts\<close>
theory Misc_HLW
imports
Complex_Main
"HOL-Library.Multiset"
"HOL-Library.Permutations"
"HOL-Library.FuncSet"
"HOL-Library.Groups_Big_Fun"
"HOL-Library.Poly_Mapping"
"HOL-Library.Landau_Symbols"
"HOL-Computational_Algebra.Computational_Algebra"
begin
lemma set_mset_subset_singletonD:
assumes "set_mset A \<subseteq> {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 "\<forall>x\<in>#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 "\<pi> permutes A"
shows "bij_betw (\<lambda>\<sigma>. \<pi> \<circ> \<sigma>) {\<sigma>. \<sigma> permutes A} {\<sigma>. \<sigma> permutes A}"
proof (rule bij_betwI)
show "(\<circ>) \<pi> \<in> {\<sigma>. \<sigma> permutes A} \<rightarrow> {\<sigma>. \<sigma> permutes A}"
by (auto intro: permutes_compose assms)
show "(\<circ>) (inv_into UNIV \<pi>) \<in> {\<sigma>. \<sigma> permutes A} \<rightarrow> {\<sigma>. \<sigma> 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 "\<pi> permutes B"
shows "bij_betw (\<lambda>f. (\<pi> \<circ> f)) (A \<rightarrow> B) (A \<rightarrow> B)"
proof (rule bij_betwI)
have *: "(\<lambda>f. (\<pi> \<circ> f)) \<in> (A \<rightarrow> B) \<rightarrow> A \<rightarrow> B" if \<pi>: "\<pi> permutes B" for \<pi>
by (auto simp: permutes_in_image[OF \<pi>])
show "(\<lambda>f. (\<pi> \<circ> f)) \<in> (A \<rightarrow> B) \<rightarrow> A \<rightarrow> B"
by (rule *) fact
show "(\<lambda>f. (inv_into UNIV \<pi> \<circ> f)) \<in> (A \<rightarrow> B) \<rightarrow> A \<rightarrow> B"
by (intro * permutes_inv) fact
qed (auto simp: permutes_inverses[OF assms] fun_eq_iff)
lemma bij_betw_compose_left_perm_PiE:
assumes "\<pi> permutes B"
shows "bij_betw (\<lambda>f. restrict (\<pi> \<circ> f) A) (A \<rightarrow>\<^sub>E B) (A \<rightarrow>\<^sub>E B)"
proof (rule bij_betwI)
have *: "(\<lambda>f. restrict (\<pi> \<circ> f) A) \<in> (A \<rightarrow>\<^sub>E B) \<rightarrow> A \<rightarrow>\<^sub>E B" if \<pi>: "\<pi> permutes B" for \<pi>
by (auto simp: permutes_in_image[OF \<pi>])
show "(\<lambda>f. restrict (\<pi> \<circ> f) A) \<in> (A \<rightarrow>\<^sub>E B) \<rightarrow> A \<rightarrow>\<^sub>E B"
by (rule *) fact
show "(\<lambda>f. restrict (inv_into UNIV \<pi> \<circ> f) A) \<in> (A \<rightarrow>\<^sub>E B) \<rightarrow> A \<rightarrow>\<^sub>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 \<subseteq> A \<and> size X = n}"
proof (rule finite_subset)
show "{X. set_mset X \<subseteq> A \<and> size X = n} \<subseteq> mset ` {xs. set xs \<subseteq> A \<and> length xs = n}"
proof
fix X assume X: "X \<in> {X. set_mset X \<subseteq> A \<and> size X = n}"
obtain xs where [simp]: "X = mset xs"
by (metis ex_mset)
thus "X \<in> mset ` {xs. set xs \<subseteq> A \<and> length xs = n}"
using X by auto
qed
next
show "finite (mset ` {xs. set xs \<subseteq> A \<and> 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 (\<lambda>x. sum_mset (image_mset g (f x))) A)"
by (induction A) auto
lemma sum_mset_image_mset_singleton: "sum_mset (image_mset (\<lambda>x. {#f x#}) A) = image_mset f A"
by (induction A) auto
lemma sum_mset_conv_sum:
"sum_mset (image_mset f A) = (\<Sum>x\<in>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 \<in># A"
by auto
define n where "n = count A x"
define A' where "A' = filter_mset (\<lambda>y. y \<noteq> x) A"
have A_eq: "A = replicate_mset n x + A'"
by (intro multiset_eqI) (auto simp: A'_def n_def)
have [simp]: "x \<notin># A'" "count A' x = 0"
by (auto simp: A'_def)
have "n \<noteq> 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' \<subset># 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') = (\<Sum>x\<in>set_mset A'. of_nat (count A' x) * f x)"
by simp
also have "\<dots> = (\<Sum>x\<in>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 + \<dots> = (\<Sum>x\<in>insert x (set_mset A'). of_nat (count A x) * f x)"
by (subst sum.insert) (auto simp: A_eq)