Read about our upcoming Code of Conduct on this issue

Commit 06809460 authored by Andreas Lochbihler's avatar Andreas Lochbihler
Browse files

merge from afp-2021

......@@ -664,6 +664,39 @@ abstract =
developed in the AFP entry on the transcendence of
title = The Hermite–Lindemann–Weierstraß Transcendence Theorem
author = Manuel Eberl <>
topic = Mathematics/Number theory
date = 2021-03-03
notify =
abstract =
<p>This article provides a formalisation of the
Hermite-Lindemann-Weierstraß Theorem (also known as simply
Hermite-Lindemann or Lindemann-Weierstraß). This theorem is one of the
crowning achievements of 19th century number theory.</p>
<p>The theorem states that if $\alpha_1, \ldots,
\alpha_n\in\mathbb{C}$ are algebraic numbers that are linearly
independent over $\mathbb{Z}$, then $e^{\alpha_1},\ldots,e^{\alpha_n}$
are algebraically independent over $\mathbb{Q}$.</p>
<p>Like the <a
formalisation in Coq by Bernard</a>, I proceeded by formalising
version of the theorem and proof</a> and then deriving the
original one from that. Baker's version states that for any
algebraic numbers $\beta_1, \ldots, \beta_n\in\mathbb{C}$ and distinct
algebraic numbers $\alpha_i, \ldots, \alpha_n\in\mathbb{C}$, we have
$\beta_1 e^{\alpha_1} + \ldots + \beta_n e^{\alpha_n} = 0$ if and only
if all the $\beta_i$ are zero.</p> <p>This has a number of
direct corollaries, e.g.:</p> <ul> <li>$e$ and $\pi$
are transcendental</li> <li>$e^z$, $\sin z$, $\tan z$,
etc. are transcendental for algebraic
$z\in\mathbb{C}\setminus\{0\}$</li> <li>$\ln z$ is
transcendental for algebraic $z\in\mathbb{C}\setminus\{0,
1\}$</li> </ul>
title = A Framework for Verifying Depth-First Search Algorithms
author = Peter Lammich <>, René Neumann <>
......@@ -10153,6 +10186,19 @@ abstract =
algorithm, the Deutsch-Jozsa algorithm and the quantum Prisoner's
title = Quantum projective measurements and the CHSH inequality
author = Mnacho Echenim <>
topic = Computer science/Algorithms/Quantum computing, Mathematics/Physics/Quantum information
date = 2021-03-03
notify =
abstract =
This work contains a formalization of quantum projective measurements,
also known as von Neumann measurements, which are based on elements of
spectral theory. We also formalized the CHSH inequality, an inequality
involving expectations in a probability space that is violated by
quantum measurements, thus proving that quantum mechanics cannot be modeled with an underlying local hidden-variable theory.
title = Finite Map Extras
author = Javier Díaz <>
......@@ -10309,3 +10355,47 @@ abstract =
discussed in greater detail in the corresponding <a
title = The Sunflower Lemma of Erdős and Rado
author = René Thiemann <>
topic = Mathematics/Combinatorics
date = 2021-02-25
notify =
abstract =
We formally define sunflowers and provide a formalization of the
sunflower lemma of Erd&odblac;s and Rado: whenever a set of
size-<i>k</i>-sets has a larger cardinality than
<i>(r - 1)<sup>k</sup> &middot; k!</i>,
then it contains a sunflower of cardinality <i>r</i>.
title = Mereology
author = Ben Blumson <>
topic = Logic/Philosophical aspects
date = 2021-03-01
notify =
abstract =
We use Isabelle/HOL to verify elementary theorems and alternative
axiomatizations of classical extensional mereology.
title = Two algorithms based on modular arithmetic: lattice basis reduction and Hermite normal form computation
author = Ralph Bottesch <>, Jose Divasón <>, René Thiemann <>
topic = Computer science/Algorithms/Mathematical
date = 2021-03-12
notify =
abstract =
We verify two algorithms for which modular arithmetic plays an
essential role: Storjohann's variant of the LLL lattice basis
reduction algorithm and Kopparty's algorithm for computing the
Hermite normal form of a matrix. To do this, we also formalize some
facts about the modulo operation with symmetric range. Our
implementations are based on the original papers, but are otherwise
efficient. For basis reduction we formalize two versions: one that
includes all of the optimizations/heuristics from Storjohann's
paper, and one excluding a heuristic that we observed to often
decrease efficiency. We also provide a fast, self-contained certifier
for basis reduction, based on the efficient Hermite normal form
......@@ -30,6 +30,8 @@ Isabelle. Older versions of archive entries will remain available.</p>
<a href="">Technische Universit&auml;t M&uuml;nchen</a></li>
<li><a href="">Gerwin Klein</a>,
<a href="">Data61</a></li>
<li><a href="">Andreas Lochbihler</a>,
<a href="">Digital Asset</a></li>
<li><a href="">Tobias Nipkow</a>,
<a href="">Technische Universit&auml;t M&uuml;nchen</a></li>
<li><a href="">Larry Paulson</a>,
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"
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).
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"
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 .
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>.
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"
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
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
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 .
\ 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"
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.
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"
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
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
\ 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
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.
(* 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:])"
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)
fixes x :: "'a :: {field_char_0, field_gcd}"
shows degree_min_int_poly_pos [intro]: " (min_int_poly x) > 0"
and degree_min_int_poly_nonzero [simp]: " (min_int_poly x) \<noteq> 0"
proof -
show " (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 " (min_int_poly x) \<noteq> 0"
by blast
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
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"
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 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
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
\ No newline at end of file
File: Misc_HLW.thy
Author: Manuel Eberl, TU München
section \<open>Miscellaneous facts\<close>
theory Misc_HLW