[STATEMENT]
lemma is_nth_power_upto_unit_mult_coprimeD1:
  fixes x y :: "'a :: factorial_semiring"
  assumes "coprime x y" "is_nth_power_upto_unit n (x * y)"
  shows   "is_nth_power_upto_unit n x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_nth_power_upto_unit n x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_nth_power_upto_unit n x
[PROOF STEP]
consider "n = 0" | "x = 0" "n > 0" | "x \<noteq> 0" "y = 0" "n > 0" | "n > 0" "x \<noteq> 0" "y \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n = 0 \<Longrightarrow> thesis; \<lbrakk>x = (0::'a); 0 < n\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>x \<noteq> (0::'a); y = (0::'a); 0 < n\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>0 < n; x \<noteq> (0::'a); y \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<lbrakk>n = 0 \<Longrightarrow> ?thesis; \<lbrakk>x = (0::'a); 0 < n\<rbrakk> \<Longrightarrow> ?thesis; \<lbrakk>x \<noteq> (0::'a); y = (0::'a); 0 < n\<rbrakk> \<Longrightarrow> ?thesis; \<lbrakk>0 < n; x \<noteq> (0::'a); y \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. is_nth_power_upto_unit n x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>n = 0 \<Longrightarrow> ?thesis; \<lbrakk>x = (0::'a); 0 < n\<rbrakk> \<Longrightarrow> ?thesis; \<lbrakk>x \<noteq> (0::'a); y = (0::'a); 0 < n\<rbrakk> \<Longrightarrow> ?thesis; \<lbrakk>0 < n; x \<noteq> (0::'a); y \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. is_nth_power_upto_unit n x
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. n = 0 \<Longrightarrow> is_nth_power_upto_unit n x
 2. \<lbrakk>x = (0::'a); 0 < n\<rbrakk> \<Longrightarrow> is_nth_power_upto_unit n x
 3. \<lbrakk>x \<noteq> (0::'a); y = (0::'a); 0 < n\<rbrakk> \<Longrightarrow> is_nth_power_upto_unit n x
 4. \<lbrakk>0 < n; x \<noteq> (0::'a); y \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> is_nth_power_upto_unit n x
[PROOF STEP]
assume [simp]: "n = 0"
[PROOF STATE]
proof (state)
this:
n = 0

goal (4 subgoals):
 1. n = 0 \<Longrightarrow> is_nth_power_upto_unit n x
 2. \<lbrakk>x = (0::'a); 0 < n\<rbrakk> \<Longrightarrow> is_nth_power_upto_unit n x
 3. \<lbrakk>x \<noteq> (0::'a); y = (0::'a); 0 < n\<rbrakk> \<Longrightarrow> is_nth_power_upto_unit n x
 4. \<lbrakk>0 < n; x \<noteq> (0::'a); y \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> is_nth_power_upto_unit n x
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
coprime x y
is_nth_power_upto_unit n (x * y)
[PROOF STEP]
have "is_unit (x * y)"
[PROOF STATE]
proof (prove)
using this:
coprime x y
is_nth_power_upto_unit n (x * y)

goal (1 subgoal):
 1. is_unit (x * y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_unit (x * y)

goal (4 subgoals):
 1. n = 0 \<Longrightarrow> is_nth_power_upto_unit n x
 2. \<lbrakk>x = (0::'a); 0 < n\<rbrakk> \<Longrightarrow> is_nth_power_upto_unit n x
 3. \<lbrakk>x \<noteq> (0::'a); y = (0::'a); 0 < n\<rbrakk> \<Longrightarrow> is_nth_power_upto_unit n x
 4. \<lbrakk>0 < n; x \<noteq> (0::'a); y \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> is_nth_power_upto_unit n x
[PROOF STEP]
hence "is_unit x"
[PROOF STATE]
proof (prove)
using this:
is_unit (x * y)

goal (1 subgoal):
 1. is_unit x
[PROOF STEP]
using is_unit_mult_iff
[PROOF STATE]
proof (prove)
using this:
is_unit (x * y)
is_unit (?a * ?b) = (is_unit ?a \<and> is_unit ?b)

goal (1 subgoal):
 1. is_unit x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
is_unit x

goal (4 subgoals):
 1. n = 0 \<Longrightarrow> is_nth_power_upto_unit n x
 2. \<lbrakk>x = (0::'a); 0 < n\<rbrakk> \<Longrightarrow> is_nth_power_upto_unit n x
 3. \<lbrakk>x \<noteq> (0::'a); y = (0::'a); 0 < n\<rbrakk> \<Longrightarrow> is_nth_power_upto_unit n x
 4. \<lbrakk>0 < n; x \<noteq> (0::'a); y \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> is_nth_power_upto_unit n x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
is_unit x

goal (1 subgoal):
 1. is_nth_power_upto_unit n x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_unit x
coprime x y
is_nth_power_upto_unit n (x * y)

goal (1 subgoal):
 1. is_nth_power_upto_unit n x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_nth_power_upto_unit n x

goal (3 subgoals):
 1. \<lbrakk>x = (0::'a); 0 < n\<rbrakk> \<Longrightarrow> is_nth_power_upto_unit n x
 2. \<lbrakk>x \<noteq> (0::'a); y = (0::'a); 0 < n\<rbrakk> \<Longrightarrow> is_nth_power_upto_unit n x
 3. \<lbrakk>0 < n; x \<noteq> (0::'a); y \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> is_nth_power_upto_unit n x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<lbrakk>x = (0::'a); 0 < n\<rbrakk> \<Longrightarrow> is_nth_power_upto_unit n x
 2. \<lbrakk>x \<noteq> (0::'a); y = (0::'a); 0 < n\<rbrakk> \<Longrightarrow> is_nth_power_upto_unit n x
 3. \<lbrakk>0 < n; x \<noteq> (0::'a); y \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> is_nth_power_upto_unit n x
[PROOF STEP]
assume "x = 0" "n > 0"
[PROOF STATE]
proof (state)
this:
x = (0::'a)
0 < n

goal (3 subgoals):
 1. \<lbrakk>x = (0::'a); 0 < n\<rbrakk> \<Longrightarrow> is_nth_power_upto_unit n x
 2. \<lbrakk>x \<noteq> (0::'a); y = (0::'a); 0 < n\<rbrakk> \<Longrightarrow> is_nth_power_upto_unit n x
 3. \<lbrakk>0 < n; x \<noteq> (0::'a); y \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> is_nth_power_upto_unit n x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
x = (0::'a)
0 < n

goal (1 subgoal):
 1. is_nth_power_upto_unit n x
[PROOF STEP]
by (auto simp: is_nth_power_upto_unit_def)
[PROOF STATE]
proof (state)
this:
is_nth_power_upto_unit n x

goal (2 subgoals):
 1. \<lbrakk>x \<noteq> (0::'a); y = (0::'a); 0 < n\<rbrakk> \<Longrightarrow> is_nth_power_upto_unit n x
 2. \<lbrakk>0 < n; x \<noteq> (0::'a); y \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> is_nth_power_upto_unit n x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>x \<noteq> (0::'a); y = (0::'a); 0 < n\<rbrakk> \<Longrightarrow> is_nth_power_upto_unit n x
 2. \<lbrakk>0 < n; x \<noteq> (0::'a); y \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> is_nth_power_upto_unit n x
[PROOF STEP]
assume *: "x \<noteq> 0" "y = 0" "n > 0"
[PROOF STATE]
proof (state)
this:
x \<noteq> (0::'a)
y = (0::'a)
0 < n

goal (2 subgoals):
 1. \<lbrakk>x \<noteq> (0::'a); y = (0::'a); 0 < n\<rbrakk> \<Longrightarrow> is_nth_power_upto_unit n x
 2. \<lbrakk>0 < n; x \<noteq> (0::'a); y \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> is_nth_power_upto_unit n x
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
coprime x y
is_nth_power_upto_unit n (x * y)
x \<noteq> (0::'a)
y = (0::'a)
0 < n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
coprime x y
is_nth_power_upto_unit n (x * y)
x \<noteq> (0::'a)
y = (0::'a)
0 < n

goal (1 subgoal):
 1. is_nth_power_upto_unit n x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_nth_power_upto_unit n x

goal (1 subgoal):
 1. \<lbrakk>0 < n; x \<noteq> (0::'a); y \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> is_nth_power_upto_unit n x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>0 < n; x \<noteq> (0::'a); y \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> is_nth_power_upto_unit n x
[PROOF STEP]
assume *: "n > 0" and [simp]: "x \<noteq> 0" "y \<noteq> 0"
[PROOF STATE]
proof (state)
this:
0 < n
x \<noteq> (0::'a)
y \<noteq> (0::'a)

goal (1 subgoal):
 1. \<lbrakk>0 < n; x \<noteq> (0::'a); y \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> is_nth_power_upto_unit n x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_nth_power_upto_unit n x
[PROOF STEP]
proof (subst is_nth_power_upto_unit_conv_multiplicity[OF \<open>n > 0\<close>]; safe)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p. prime p \<Longrightarrow> n dvd multiplicity p x
[PROOF STEP]
fix p :: 'a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p. prime p \<Longrightarrow> n dvd multiplicity p x
[PROOF STEP]
assume p: "prime p"
[PROOF STATE]
proof (state)
this:
prime p

goal (1 subgoal):
 1. \<And>p. prime p \<Longrightarrow> n dvd multiplicity p x
[PROOF STEP]
show "n dvd multiplicity p x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n dvd multiplicity p x
[PROOF STEP]
proof (cases "p dvd x")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p dvd x \<Longrightarrow> n dvd multiplicity p x
 2. \<not> p dvd x \<Longrightarrow> n dvd multiplicity p x
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> p dvd x

goal (2 subgoals):
 1. p dvd x \<Longrightarrow> n dvd multiplicity p x
 2. \<not> p dvd x \<Longrightarrow> n dvd multiplicity p x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> p dvd x

goal (1 subgoal):
 1. n dvd multiplicity p x
[PROOF STEP]
by (simp add: not_dvd_imp_multiplicity_0)
[PROOF STATE]
proof (state)
this:
n dvd multiplicity p x

goal (1 subgoal):
 1. p dvd x \<Longrightarrow> n dvd multiplicity p x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p dvd x \<Longrightarrow> n dvd multiplicity p x
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
p dvd x

goal (1 subgoal):
 1. p dvd x \<Longrightarrow> n dvd multiplicity p x
[PROOF STEP]
have "n dvd multiplicity p (x * y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n dvd multiplicity p (x * y)
[PROOF STEP]
using assms(2) \<open>n > 0\<close> p
[PROOF STATE]
proof (prove)
using this:
is_nth_power_upto_unit n (x * y)
0 < n
prime p

goal (1 subgoal):
 1. n dvd multiplicity p (x * y)
[PROOF STEP]
by (auto simp: is_nth_power_upto_unit_conv_multiplicity)
[PROOF STATE]
proof (state)
this:
n dvd multiplicity p (x * y)

goal (1 subgoal):
 1. p dvd x \<Longrightarrow> n dvd multiplicity p x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
n dvd multiplicity p (x * y)

goal (1 subgoal):
 1. p dvd x \<Longrightarrow> n dvd multiplicity p x
[PROOF STEP]
have "\<dots> = multiplicity p x + multiplicity p y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicity p (x * y) = multiplicity p x + multiplicity p y
[PROOF STEP]
using p
[PROOF STATE]
proof (prove)
using this:
prime p

goal (1 subgoal):
 1. multiplicity p (x * y) = multiplicity p x + multiplicity p y
[PROOF STEP]
by (subst prime_elem_multiplicity_mult_distrib) auto
[PROOF STATE]
proof (state)
this:
multiplicity p (x * y) = multiplicity p x + multiplicity p y

goal (1 subgoal):
 1. p dvd x \<Longrightarrow> n dvd multiplicity p x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
multiplicity p (x * y) = multiplicity p x + multiplicity p y

goal (1 subgoal):
 1. p dvd x \<Longrightarrow> n dvd multiplicity p x
[PROOF STEP]
have "\<not>p dvd y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> p dvd y
[PROOF STEP]
using \<open>coprime x y\<close> \<open>p dvd x\<close> p not_prime_unit coprime_common_divisor
[PROOF STATE]
proof (prove)
using this:
coprime x y
p dvd x
prime p
is_unit ?x \<Longrightarrow> \<not> prime ?x
\<lbrakk>coprime ?a ?b; ?c dvd ?a; ?c dvd ?b\<rbrakk> \<Longrightarrow> is_unit ?c

goal (1 subgoal):
 1. \<not> p dvd y
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> p dvd y

goal (1 subgoal):
 1. p dvd x \<Longrightarrow> n dvd multiplicity p x
[PROOF STEP]
hence "multiplicity p y = 0"
[PROOF STATE]
proof (prove)
using this:
\<not> p dvd y

goal (1 subgoal):
 1. multiplicity p y = 0
[PROOF STEP]
by (rule not_dvd_imp_multiplicity_0)
[PROOF STATE]
proof (state)
this:
multiplicity p y = 0

goal (1 subgoal):
 1. p dvd x \<Longrightarrow> n dvd multiplicity p x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
n dvd multiplicity p x + 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n dvd multiplicity p x + 0

goal (1 subgoal):
 1. n dvd multiplicity p x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n dvd multiplicity p x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
n dvd multiplicity p x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
is_nth_power_upto_unit n x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
is_nth_power_upto_unit n x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_nth_power_upto_unit_mult_coprimeD2:
  fixes x y :: "'a :: factorial_semiring"
  assumes "coprime x y" "is_nth_power_upto_unit n (x * y)"
  shows   "is_nth_power_upto_unit n y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_nth_power_upto_unit n y
[PROOF STEP]
using assms is_nth_power_upto_unit_mult_coprimeD1[of y x]
[PROOF STATE]
proof (prove)
using this:
coprime x y
is_nth_power_upto_unit n (x * y)
\<lbrakk>coprime y x; is_nth_power_upto_unit ?n (y * x)\<rbrakk> \<Longrightarrow> is_nth_power_upto_unit ?n y

goal (1 subgoal):
 1. is_nth_power_upto_unit n y
[PROOF STEP]
by (simp_all add: mult_ac coprime_commute)


[STATEMENT]
lemma gauss_int_eq_iff: "x = y \<longleftrightarrow> ReZ x = ReZ y \<and> ImZ x = ImZ y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x = y) = (ReZ x = ReZ y \<and> ImZ x = ImZ y)
[PROOF STEP]
by (cases x; cases y) auto


[STATEMENT]
lemma gauss2complex_eq_iff [simp]: "gauss2complex z = gauss2complex u \<longleftrightarrow> z = u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (gauss2complex z = gauss2complex u) = (z = u)
[PROOF STEP]
by (simp add: complex_eq_iff gauss_int_eq_iff)


[STATEMENT]
lemma gauss_i_times_i [simp]: "\<i>\<^sub>\<int> * \<i>\<^sub>\<int> = (-1 :: gauss_int)"
  and gauss_cnj_i [simp]: "gauss_cnj \<i>\<^sub>\<int> = -\<i>\<^sub>\<int>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<i>\<^sub>\<int> * \<i>\<^sub>\<int> = - 1 &&& gauss_cnj \<i>\<^sub>\<int> = - \<i>\<^sub>\<int>
[PROOF STEP]
by (simp_all add: gauss_int_eq_iff)


[STATEMENT]
lemma gauss_cnj_eq_0_iff [simp]: "gauss_cnj z = 0 \<longleftrightarrow> z = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (gauss_cnj z = 0) = (z = 0)
[PROOF STEP]
by (auto simp: gauss_int_eq_iff)


[STATEMENT]
lemma gauss_cnj_eq_self: "Im z = 0 \<Longrightarrow> gauss_cnj z = z"
  and gauss_cnj_eq_minus_self: "Re z = 0 \<Longrightarrow> gauss_cnj z = -z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Im (gauss2complex z) = 0 \<Longrightarrow> gauss_cnj z = z) &&& (Re (gauss2complex z) = 0 \<Longrightarrow> gauss_cnj z = - z)
[PROOF STEP]
by (auto simp: gauss_int_eq_iff)


[STATEMENT]
lemma ReZ_of_nat [simp]: "ReZ (of_nat n) = of_nat n"
  and ImZ_of_nat [simp]: "ImZ (of_nat n) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ReZ (of_nat n) = int n &&& ImZ (of_nat n) = 0
[PROOF STEP]
by (induction n; simp)+


[STATEMENT]
lemma ReZ_of_int [simp]: "ReZ (of_int n) = n"
  and ImZ_of_int [simp]: "ImZ (of_int n) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ReZ (of_int n) = n &&& ImZ (of_int n) = 0
[PROOF STEP]
by (induction n; simp)+


[STATEMENT]
lemma ReZ_numeral [simp]: "ReZ (numeral n) = numeral n"
  and ImZ_numeral [simp]: "ImZ (numeral n) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ReZ (numeral n) = numeral n &&& ImZ (numeral n) = 0
[PROOF STEP]
by (subst of_nat_numeral [symmetric], subst ReZ_of_nat ImZ_of_nat, simp)+


[STATEMENT]
lemma gauss2complex_0 [simp]: "gauss2complex 0 = 0"
  and gauss2complex_1 [simp]: "gauss2complex 1 = 1"
  and gauss2complex_i [simp]: "gauss2complex \<i>\<^sub>\<int> = \<i>"
  and gauss2complex_add [simp]: "gauss2complex (x + y) = gauss2complex x + gauss2complex y"
  and gauss2complex_diff [simp]: "gauss2complex (x - y) = gauss2complex x - gauss2complex y"
  and gauss2complex_mult [simp]: "gauss2complex (x * y) = gauss2complex x * gauss2complex y"
  and gauss2complex_uminus [simp]: "gauss2complex (-x) = -gauss2complex x"
  and gauss2complex_cnj [simp]: "gauss2complex (gauss_cnj x) = cnj (gauss2complex x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((gauss2complex 0 = 0 &&& gauss2complex 1 = 1) &&& gauss2complex \<i>\<^sub>\<int> = \<i> &&& gauss2complex (x + y) = gauss2complex x + gauss2complex y) &&& (gauss2complex (x - y) = gauss2complex x - gauss2complex y &&& gauss2complex (x * y) = gauss2complex x * gauss2complex y) &&& gauss2complex (- x) = - gauss2complex x &&& gauss2complex (gauss_cnj x) = cnj (gauss2complex x)
[PROOF STEP]
by (simp_all add: complex_eq_iff)


[STATEMENT]
lemma gauss2complex_of_nat [simp]: "gauss2complex (of_nat n) = of_nat n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gauss2complex (of_nat n) = of_nat n
[PROOF STEP]
by (simp add: complex_eq_iff)


[STATEMENT]
lemma gauss2complex_eq_0_iff [simp]: "gauss2complex x = 0 \<longleftrightarrow> x = 0"
  and gauss2complex_eq_1_iff [simp]: "gauss2complex x = 1 \<longleftrightarrow> x = 1"
  and zero_eq_gauss2complex_iff [simp]: "0 = gauss2complex x \<longleftrightarrow> x = 0"
  and one_eq_gauss2complex_iff [simp]: "1 = gauss2complex x \<longleftrightarrow> x = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((gauss2complex x = 0) = (x = 0) &&& (gauss2complex x = 1) = (x = 1)) &&& (0 = gauss2complex x) = (x = 0) &&& (1 = gauss2complex x) = (x = 1)
[PROOF STEP]
by (simp_all add: complex_eq_iff gauss_int_eq_iff)


[STATEMENT]
lemma gauss_i_times_gauss_i_times [simp]: "\<i>\<^sub>\<int> * (\<i>\<^sub>\<int> * x) = (-x :: gauss_int)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<i>\<^sub>\<int> * (\<i>\<^sub>\<int> * x) = - x
[PROOF STEP]
by (subst mult.assoc [symmetric], subst gauss_i_times_i) auto


[STATEMENT]
lemma gauss_i_neq_0 [simp]: "\<i>\<^sub>\<int> \<noteq> 0" "0 \<noteq> \<i>\<^sub>\<int>"
  and gauss_i_neq_1 [simp]: "\<i>\<^sub>\<int> \<noteq> 1" "1 \<noteq> \<i>\<^sub>\<int>"
  and gauss_i_neq_of_nat [simp]: "\<i>\<^sub>\<int> \<noteq> of_nat n" "of_nat n \<noteq> \<i>\<^sub>\<int>"
  and gauss_i_neq_of_int [simp]: "\<i>\<^sub>\<int> \<noteq> of_int n" "of_int n \<noteq> \<i>\<^sub>\<int>"
  and gauss_i_neq_numeral [simp]: "\<i>\<^sub>\<int> \<noteq> numeral m" "numeral m \<noteq> \<i>\<^sub>\<int>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<i>\<^sub>\<int> \<noteq> 0 &&& 0 \<noteq> \<i>\<^sub>\<int>) &&& \<i>\<^sub>\<int> \<noteq> 1 &&& 1 \<noteq> \<i>\<^sub>\<int>) &&& (\<i>\<^sub>\<int> \<noteq> of_nat n &&& of_nat n \<noteq> \<i>\<^sub>\<int>) &&& (\<i>\<^sub>\<int> \<noteq> of_int (int n) &&& of_int (int n) \<noteq> \<i>\<^sub>\<int>) &&& \<i>\<^sub>\<int> \<noteq> numeral m &&& numeral m \<noteq> \<i>\<^sub>\<int>
[PROOF STEP]
by (auto simp: gauss_int_eq_iff)


[STATEMENT]
lemma gauss_cnj_0 [simp]: "gauss_cnj 0 = 0"
  and gauss_cnj_1 [simp]: "gauss_cnj 1 = 1"
  and gauss_cnj_cnj [simp]: "gauss_cnj (gauss_cnj z) = z"
  and gauss_cnj_uminus [simp]: "gauss_cnj (-a) = -gauss_cnj a"
  and gauss_cnj_add [simp]: "gauss_cnj (a + b) = gauss_cnj a + gauss_cnj b"
  and gauss_cnj_diff [simp]: "gauss_cnj (a - b) = gauss_cnj a - gauss_cnj b"
  and gauss_cnj_mult [simp]: "gauss_cnj (a * b) = gauss_cnj a * gauss_cnj b"
  and gauss_cnj_of_nat [simp]: "gauss_cnj (of_nat n1) = of_nat n1"
  and gauss_cnj_of_int [simp]: "gauss_cnj (of_int n2) = of_int n2"
  and gauss_cnj_numeral [simp]: "gauss_cnj (numeral n3) = numeral n3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((gauss_cnj 0 = 0 &&& gauss_cnj 1 = 1) &&& gauss_cnj (gauss_cnj z) = z &&& gauss_cnj (- a) = - gauss_cnj a &&& gauss_cnj (a + b) = gauss_cnj a + gauss_cnj b) &&& (gauss_cnj (a - b) = gauss_cnj a - gauss_cnj b &&& gauss_cnj (a * b) = gauss_cnj a * gauss_cnj b) &&& gauss_cnj (of_nat n1) = of_nat n1 &&& gauss_cnj (of_int n2) = of_int n2 &&& gauss_cnj (numeral n3) = numeral n3
[PROOF STEP]
by (simp_all add: gauss_int_eq_iff)


[STATEMENT]
lemma gauss_cnj_power [simp]: "gauss_cnj (a ^ n) = gauss_cnj a ^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gauss_cnj (a ^ n) = gauss_cnj a ^ n
[PROOF STEP]
by (induction n) auto


[STATEMENT]
lemma gauss_cnj_sum [simp]: "gauss_cnj (sum f A) = (\<Sum>x\<in>A. gauss_cnj (f x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gauss_cnj (sum f A) = (\<Sum>x\<in>A. gauss_cnj (f x))
[PROOF STEP]
by (induction A rule: infinite_finite_induct) auto


[STATEMENT]
lemma gauss_cnj_prod [simp]: "gauss_cnj (prod f A) = (\<Prod>x\<in>A. gauss_cnj (f x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gauss_cnj (prod f A) = (\<Prod>x\<in>A. gauss_cnj (f x))
[PROOF STEP]
by (induction A rule: infinite_finite_induct) auto


[STATEMENT]
lemma of_nat_dvd_of_nat:
  assumes "a dvd b"
  shows   "of_nat a dvd (of_nat b :: 'a :: comm_semiring_1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_nat a dvd of_nat b
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a dvd b

goal (1 subgoal):
 1. of_nat a dvd of_nat b
[PROOF STEP]
by auto


[STATEMENT]
lemma of_int_dvd_imp_dvd_gauss_cnj:
  fixes z :: gauss_int
  assumes "of_int n dvd z"
  shows   "of_int n dvd gauss_cnj z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int n dvd gauss_cnj z
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. of_int n dvd gauss_cnj z
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
of_int n dvd z
[PROOF STEP]
obtain u where "z = of_int n * u"
[PROOF STATE]
proof (prove)
using this:
of_int n dvd z

goal (1 subgoal):
 1. (\<And>u. z = of_int n * u \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
z = of_int n * u

goal (1 subgoal):
 1. of_int n dvd gauss_cnj z
[PROOF STEP]
hence "gauss_cnj z = of_int n * gauss_cnj u"
[PROOF STATE]
proof (prove)
using this:
z = of_int n * u

goal (1 subgoal):
 1. gauss_cnj z = of_int n * gauss_cnj u
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
gauss_cnj z = of_int n * gauss_cnj u

goal (1 subgoal):
 1. of_int n dvd gauss_cnj z
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
gauss_cnj z = of_int n * gauss_cnj u

goal (1 subgoal):
 1. of_int n dvd gauss_cnj z
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
of_int n dvd gauss_cnj z

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma of_nat_dvd_imp_dvd_gauss_cnj:
  fixes z :: gauss_int
  assumes "of_nat n dvd z"
  shows   "of_nat n dvd gauss_cnj z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_nat n dvd gauss_cnj z
[PROOF STEP]
using of_int_dvd_imp_dvd_gauss_cnj[of "int n"] assms
[PROOF STATE]
proof (prove)
using this:
of_int (int n) dvd ?z \<Longrightarrow> of_int (int n) dvd gauss_cnj ?z
of_nat n dvd z

goal (1 subgoal):
 1. of_nat n dvd gauss_cnj z
[PROOF STEP]
by simp


[STATEMENT]
lemma of_int_dvd_of_int_gauss_int_iff:
  "(of_int m :: gauss_int) dvd of_int n \<longleftrightarrow> m dvd n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (of_int m dvd of_int n) = (m dvd n)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. of_int m dvd of_int n \<Longrightarrow> m dvd n
 2. m dvd n \<Longrightarrow> of_int m dvd of_int n
[PROOF STEP]
assume "of_int m dvd (of_int n :: gauss_int)"
[PROOF STATE]
proof (state)
this:
of_int m dvd of_int n

goal (2 subgoals):
 1. of_int m dvd of_int n \<Longrightarrow> m dvd n
 2. m dvd n \<Longrightarrow> of_int m dvd of_int n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
of_int m dvd of_int n
[PROOF STEP]
obtain a :: gauss_int where "of_int n = of_int m * a"
[PROOF STATE]
proof (prove)
using this:
of_int m dvd of_int n

goal (1 subgoal):
 1. (\<And>a. of_int n = of_int m * a \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
of_int n = of_int m * a

goal (2 subgoals):
 1. of_int m dvd of_int n \<Longrightarrow> m dvd n
 2. m dvd n \<Longrightarrow> of_int m dvd of_int n
[PROOF STEP]
thus "m dvd n"
[PROOF STATE]
proof (prove)
using this:
of_int n = of_int m * a

goal (1 subgoal):
 1. m dvd n
[PROOF STEP]
by (auto simp: gauss_int_eq_iff)
[PROOF STATE]
proof (state)
this:
m dvd n

goal (1 subgoal):
 1. m dvd n \<Longrightarrow> of_int m dvd of_int n
[PROOF STEP]
qed auto


[STATEMENT]
lemma of_nat_dvd_of_nat_gauss_int_iff:
  "(of_nat m :: gauss_int) dvd of_nat n \<longleftrightarrow> m dvd n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (of_nat m dvd of_nat n) = (m dvd n)
[PROOF STEP]
using of_int_dvd_of_int_gauss_int_iff[of "int m" "int n"]
[PROOF STATE]
proof (prove)
using this:
(of_int (int m) dvd of_int (int n)) = (int m dvd int n)

goal (1 subgoal):
 1. (of_nat m dvd of_nat n) = (m dvd n)
[PROOF STEP]
by simp


[STATEMENT]
lemma gauss_cnj_dvd:
  assumes "a dvd b"
  shows   "gauss_cnj a dvd gauss_cnj b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gauss_cnj a dvd gauss_cnj b
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. gauss_cnj a dvd gauss_cnj b
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
a dvd b
[PROOF STEP]
obtain c where "b = a * c"
[PROOF STATE]
proof (prove)
using this:
a dvd b

goal (1 subgoal):
 1. (\<And>c. b = a * c \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
b = a * c

goal (1 subgoal):
 1. gauss_cnj a dvd gauss_cnj b
[PROOF STEP]
hence "gauss_cnj b = gauss_cnj a * gauss_cnj c"
[PROOF STATE]
proof (prove)
using this:
b = a * c

goal (1 subgoal):
 1. gauss_cnj b = gauss_cnj a * gauss_cnj c
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
gauss_cnj b = gauss_cnj a * gauss_cnj c

goal (1 subgoal):
 1. gauss_cnj a dvd gauss_cnj b
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
gauss_cnj b = gauss_cnj a * gauss_cnj c

goal (1 subgoal):
 1. gauss_cnj a dvd gauss_cnj b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
gauss_cnj a dvd gauss_cnj b

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma gauss_cnj_dvd_iff: "gauss_cnj a dvd gauss_cnj b \<longleftrightarrow> a dvd b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (gauss_cnj a dvd gauss_cnj b) = (a dvd b)
[PROOF STEP]
using gauss_cnj_dvd[of a b] gauss_cnj_dvd[of "gauss_cnj a" "gauss_cnj b"]
[PROOF STATE]
proof (prove)
using this:
a dvd b \<Longrightarrow> gauss_cnj a dvd gauss_cnj b
gauss_cnj a dvd gauss_cnj b \<Longrightarrow> gauss_cnj (gauss_cnj a) dvd gauss_cnj (gauss_cnj b)

goal (1 subgoal):
 1. (gauss_cnj a dvd gauss_cnj b) = (a dvd b)
[PROOF STEP]
by auto


[STATEMENT]
lemma gauss_cnj_dvd_left_iff: "gauss_cnj a dvd b \<longleftrightarrow> a dvd gauss_cnj b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (gauss_cnj a dvd b) = (a dvd gauss_cnj b)
[PROOF STEP]
by (subst gauss_cnj_dvd_iff [symmetric]) auto


[STATEMENT]
lemma gauss_cnj_dvd_right_iff: "a dvd gauss_cnj b \<longleftrightarrow> gauss_cnj a dvd b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a dvd gauss_cnj b) = (gauss_cnj a dvd b)
[PROOF STEP]
by (rule gauss_cnj_dvd_left_iff [symmetric])


[STATEMENT]
lemma gauss_int_code_post [code_post]:
  "Gauss_Int 0 0 = 0"
  "Gauss_Int 0 1 = \<i>\<^sub>\<int>"
  "Gauss_Int 0 (-1) = -\<i>\<^sub>\<int>"
  "Gauss_Int 1 0 = 1"
  "Gauss_Int 1 1 = 1 + \<i>\<^sub>\<int>"
  "Gauss_Int 1 (-1) = 1 - \<i>\<^sub>\<int>"
  "Gauss_Int (-1) 0 = -1"
  "Gauss_Int (-1) 1 = -1 + \<i>\<^sub>\<int>"
  "Gauss_Int (-1) (-1) = -1 - \<i>\<^sub>\<int>"
  "Gauss_Int (numeral b) 0 = numeral b"
  "Gauss_Int (-numeral b) 0 = -numeral b"
  "Gauss_Int (numeral b) 1 = numeral b + \<i>\<^sub>\<int>"
  "Gauss_Int (-numeral b) 1 = -numeral b + \<i>\<^sub>\<int>"
  "Gauss_Int (numeral b) (-1) = numeral b - \<i>\<^sub>\<int>"
  "Gauss_Int (-numeral b) (-1) = -numeral b - \<i>\<^sub>\<int>"
  "Gauss_Int 0 (numeral b) = numeral b * \<i>\<^sub>\<int>"
  "Gauss_Int 0 (-numeral b) = -numeral b * \<i>\<^sub>\<int>"
  "Gauss_Int 1 (numeral b) = 1 + numeral b * \<i>\<^sub>\<int>"
  "Gauss_Int 1 (-numeral b) = 1 - numeral b * \<i>\<^sub>\<int>"
  "Gauss_Int (-1) (numeral b) = -1 + numeral b * \<i>\<^sub>\<int>"
  "Gauss_Int (-1) (-numeral b) = -1 - numeral b * \<i>\<^sub>\<int>"
  "Gauss_Int (numeral a) (numeral b) = numeral a + numeral b * \<i>\<^sub>\<int>"
  "Gauss_Int (numeral a) (-numeral b) = numeral a - numeral b * \<i>\<^sub>\<int>"
  "Gauss_Int (-numeral a) (numeral b) = -numeral a + numeral b * \<i>\<^sub>\<int>"
  "Gauss_Int (-numeral a) (-numeral b) = -numeral a - numeral b * \<i>\<^sub>\<int>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (((Gauss_Int 0 0 = 0 &&& Gauss_Int 0 1 = \<i>\<^sub>\<int> &&& Gauss_Int 0 (- 1) = - \<i>\<^sub>\<int>) &&& Gauss_Int 1 0 = 1 &&& Gauss_Int 1 1 = 1 + \<i>\<^sub>\<int> &&& Gauss_Int 1 (- 1) = 1 - \<i>\<^sub>\<int>) &&& (Gauss_Int (- 1) 0 = - 1 &&& Gauss_Int (- 1) 1 = - 1 + \<i>\<^sub>\<int> &&& Gauss_Int (- 1) (- 1) = - 1 - \<i>\<^sub>\<int>) &&& Gauss_Int (numeral b) 0 = numeral b &&& Gauss_Int (- numeral b) 0 = - numeral b &&& Gauss_Int (numeral b) 1 = numeral b + \<i>\<^sub>\<int>) &&& ((Gauss_Int (- numeral b) 1 = - numeral b + \<i>\<^sub>\<int> &&& Gauss_Int (numeral b) (- 1) = numeral b - \<i>\<^sub>\<int> &&& Gauss_Int (- numeral b) (- 1) = - numeral b - \<i>\<^sub>\<int>) &&& Gauss_Int 0 (numeral b) = numeral b * \<i>\<^sub>\<int> &&& Gauss_Int 0 (- numeral b) = - numeral b * \<i>\<^sub>\<int> &&& Gauss_Int 1 (numeral b) = 1 + numeral b * \<i>\<^sub>\<int>) &&& (Gauss_Int 1 (- numeral b) = 1 - numeral b * \<i>\<^sub>\<int> &&& Gauss_Int (- 1) (numeral b) = - 1 + numeral b * \<i>\<^sub>\<int> &&& Gauss_Int (- 1) (- numeral b) = - 1 - numeral b * \<i>\<^sub>\<int>) &&& (Gauss_Int (numeral a) (numeral b) = numeral a + numeral b * \<i>\<^sub>\<int> &&& Gauss_Int (numeral a) (- numeral b) = numeral a - numeral b * \<i>\<^sub>\<int>) &&& Gauss_Int (- numeral a) (numeral b) = - numeral a + numeral b * \<i>\<^sub>\<int> &&& Gauss_Int (- numeral a) (- numeral b) = - numeral a - numeral b * \<i>\<^sub>\<int>
[PROOF STEP]
by (simp_all add: gauss_int_eq_iff)


[STATEMENT]
lemma gauss_int_norm_0 [simp]: "gauss_int_norm 0 = 0"
  and gauss_int_norm_1 [simp]: "gauss_int_norm 1 = 1"
  and gauss_int_norm_i [simp]: "gauss_int_norm \<i>\<^sub>\<int> = 1"
  and gauss_int_norm_cnj [simp]: "gauss_int_norm (gauss_cnj z) = gauss_int_norm z"
  and gauss_int_norm_of_nat [simp]: "gauss_int_norm (of_nat n) = n ^ 2"
  and gauss_int_norm_of_int [simp]: "gauss_int_norm (of_int m) = nat (m ^ 2)"
  and gauss_int_norm_of_numeral [simp]: "gauss_int_norm (numeral n') = numeral (Num.sqr n')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (gauss_int_norm 0 = 0 &&& gauss_int_norm 1 = 1 &&& gauss_int_norm \<i>\<^sub>\<int> = 1) &&& (gauss_int_norm (gauss_cnj z) = gauss_int_norm z &&& gauss_int_norm (of_nat n) = n\<^sup>2) &&& gauss_int_norm (of_int m) = nat (m\<^sup>2) &&& gauss_int_norm (numeral n') = numeral (Num.sqr n')
[PROOF STEP]
by (simp_all add: gauss_int_norm_def nat_power_eq)


[STATEMENT]
lemma gauss_int_norm_uminus [simp]: "gauss_int_norm (-z) = gauss_int_norm z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gauss_int_norm (- z) = gauss_int_norm z
[PROOF STEP]
by (simp add: gauss_int_norm_def)


[STATEMENT]
lemma gauss_int_norm_eq_0_iff [simp]: "gauss_int_norm z = 0 \<longleftrightarrow> z = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (gauss_int_norm z = 0) = (z = 0)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. gauss_int_norm z = 0 \<Longrightarrow> z = 0
 2. z = 0 \<Longrightarrow> gauss_int_norm z = 0
[PROOF STEP]
assume "gauss_int_norm z = 0"
[PROOF STATE]
proof (state)
this:
gauss_int_norm z = 0

goal (2 subgoals):
 1. gauss_int_norm z = 0 \<Longrightarrow> z = 0
 2. z = 0 \<Longrightarrow> gauss_int_norm z = 0
[PROOF STEP]
hence "ReZ z ^ 2 + ImZ z ^ 2 \<le> 0"
[PROOF STATE]
proof (prove)
using this:
gauss_int_norm z = 0

goal (1 subgoal):
 1. (ReZ z)\<^sup>2 + (ImZ z)\<^sup>2 \<le> 0
[PROOF STEP]
by (simp add: gauss_int_norm_def)
[PROOF STATE]
proof (state)
this:
(ReZ z)\<^sup>2 + (ImZ z)\<^sup>2 \<le> 0

goal (2 subgoals):
 1. gauss_int_norm z = 0 \<Longrightarrow> z = 0
 2. z = 0 \<Longrightarrow> gauss_int_norm z = 0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(ReZ z)\<^sup>2 + (ImZ z)\<^sup>2 \<le> 0

goal (2 subgoals):
 1. gauss_int_norm z = 0 \<Longrightarrow> z = 0
 2. z = 0 \<Longrightarrow> gauss_int_norm z = 0
[PROOF STEP]
have "ReZ z ^ 2 + ImZ z ^ 2 \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> (ReZ z)\<^sup>2 + (ImZ z)\<^sup>2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 \<le> (ReZ z)\<^sup>2 + (ImZ z)\<^sup>2

goal (2 subgoals):
 1. gauss_int_norm z = 0 \<Longrightarrow> z = 0
 2. z = 0 \<Longrightarrow> gauss_int_norm z = 0
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(ReZ z)\<^sup>2 + (ImZ z)\<^sup>2 \<le> 0
0 \<le> (ReZ z)\<^sup>2 + (ImZ z)\<^sup>2
[PROOF STEP]
have "ReZ z ^ 2 + ImZ z ^ 2 = 0"
[PROOF STATE]
proof (prove)
using this:
(ReZ z)\<^sup>2 + (ImZ z)\<^sup>2 \<le> 0
0 \<le> (ReZ z)\<^sup>2 + (ImZ z)\<^sup>2

goal (1 subgoal):
 1. (ReZ z)\<^sup>2 + (ImZ z)\<^sup>2 = 0
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
(ReZ z)\<^sup>2 + (ImZ z)\<^sup>2 = 0

goal (2 subgoals):
 1. gauss_int_norm z = 0 \<Longrightarrow> z = 0
 2. z = 0 \<Longrightarrow> gauss_int_norm z = 0
[PROOF STEP]
thus "z = 0"
[PROOF STATE]
proof (prove)
using this:
(ReZ z)\<^sup>2 + (ImZ z)\<^sup>2 = 0

goal (1 subgoal):
 1. z = 0
[PROOF STEP]
by (auto simp: gauss_int_eq_iff)
[PROOF STATE]
proof (state)
this:
z = 0

goal (1 subgoal):
 1. z = 0 \<Longrightarrow> gauss_int_norm z = 0
[PROOF STEP]
qed auto


[STATEMENT]
lemma gauss_int_norm_pos_iff [simp]: "gauss_int_norm z > 0 \<longleftrightarrow> z \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0 < gauss_int_norm z) = (z \<noteq> 0)
[PROOF STEP]
using gauss_int_norm_eq_0_iff[of z]
[PROOF STATE]
proof (prove)
using this:
(gauss_int_norm z = 0) = (z = 0)

goal (1 subgoal):
 1. (0 < gauss_int_norm z) = (z \<noteq> 0)
[PROOF STEP]
by (auto intro: Nat.gr0I)


[STATEMENT]
lemma real_gauss_int_norm: "real (gauss_int_norm z) = norm (gauss2complex z) ^ 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (gauss_int_norm z) = (cmod (gauss2complex z))\<^sup>2
[PROOF STEP]
by (auto simp: cmod_def gauss_int_norm_def)


[STATEMENT]
lemma gauss_int_norm_mult: "gauss_int_norm (z * u) = gauss_int_norm z * gauss_int_norm u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gauss_int_norm (z * u) = gauss_int_norm z * gauss_int_norm u
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. gauss_int_norm (z * u) = gauss_int_norm z * gauss_int_norm u
[PROOF STEP]
have "real (gauss_int_norm (z * u)) = real (gauss_int_norm z * gauss_int_norm u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (gauss_int_norm (z * u)) = real (gauss_int_norm z * gauss_int_norm u)
[PROOF STEP]
unfolding of_nat_mult
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (gauss_int_norm (z * u)) = real (gauss_int_norm z) * real (gauss_int_norm u)
[PROOF STEP]
by (simp add: real_gauss_int_norm norm_power norm_mult power_mult_distrib)
[PROOF STATE]
proof (state)
this:
real (gauss_int_norm (z * u)) = real (gauss_int_norm z * gauss_int_norm u)

goal (1 subgoal):
 1. gauss_int_norm (z * u) = gauss_int_norm z * gauss_int_norm u
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
real (gauss_int_norm (z * u)) = real (gauss_int_norm z * gauss_int_norm u)

goal (1 subgoal):
 1. gauss_int_norm (z * u) = gauss_int_norm z * gauss_int_norm u
[PROOF STEP]
by (subst (asm) of_nat_eq_iff)
[PROOF STATE]
proof (state)
this:
gauss_int_norm (z * u) = gauss_int_norm z * gauss_int_norm u

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma self_mult_gauss_cnj: "z * gauss_cnj z = of_nat (gauss_int_norm z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z * gauss_cnj z = of_nat (gauss_int_norm z)
[PROOF STEP]
by (simp add: gauss_int_norm_def gauss_int_eq_iff algebra_simps power2_eq_square)


[STATEMENT]
lemma gauss_cnj_mult_self: "gauss_cnj z * z = of_nat (gauss_int_norm z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gauss_cnj z * z = of_nat (gauss_int_norm z)
[PROOF STEP]
by (subst mult.commute, rule self_mult_gauss_cnj)


[STATEMENT]
lemma self_plus_gauss_cnj: "z + gauss_cnj z = of_int (2 * ReZ z)"
  and self_minus_gauss_cnj: "z - gauss_cnj z = of_int (2 * ImZ z) * \<i>\<^sub>\<int>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z + gauss_cnj z = of_int (2 * ReZ z) &&& z - gauss_cnj z = of_int (2 * ImZ z) * \<i>\<^sub>\<int>
[PROOF STEP]
by (auto simp: gauss_int_eq_iff)


[STATEMENT]
lemma gauss_int_norm_dvd_mono:
  assumes "a dvd b"
  shows "gauss_int_norm a dvd gauss_int_norm b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gauss_int_norm a dvd gauss_int_norm b
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. gauss_int_norm a dvd gauss_int_norm b
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
a dvd b
[PROOF STEP]
obtain c where "b = a * c"
[PROOF STATE]
proof (prove)
using this:
a dvd b

goal (1 subgoal):
 1. (\<And>c. b = a * c \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
b = a * c

goal (1 subgoal):
 1. gauss_int_norm a dvd gauss_int_norm b
[PROOF STEP]
hence "gauss_int_norm b = gauss_int_norm (a * c)"
[PROOF STATE]
proof (prove)
using this:
b = a * c

goal (1 subgoal):
 1. gauss_int_norm b = gauss_int_norm (a * c)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
gauss_int_norm b = gauss_int_norm (a * c)

goal (1 subgoal):
 1. gauss_int_norm a dvd gauss_int_norm b
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
gauss_int_norm b = gauss_int_norm (a * c)

goal (1 subgoal):
 1. gauss_int_norm a dvd gauss_int_norm b
[PROOF STEP]
by (simp add: gauss_int_norm_mult)
[PROOF STATE]
proof (state)
this:
gauss_int_norm a dvd gauss_int_norm b

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_unit_gauss_int_iff: "x dvd 1 \<longleftrightarrow> x \<in> {1, -1, \<i>\<^sub>\<int>, -\<i>\<^sub>\<int> :: gauss_int}"
  and is_unit_gauss_int_iff': "x dvd 1 \<longleftrightarrow> gauss_int_norm x = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x dvd 1) = (x \<in> {1, - 1, \<i>\<^sub>\<int>, - \<i>\<^sub>\<int>}) &&& (x dvd 1) = (gauss_int_norm x = 1)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (x dvd 1) = (x \<in> {1, - 1, \<i>\<^sub>\<int>, - \<i>\<^sub>\<int>})
 2. (x dvd 1) = (gauss_int_norm x = 1)
[PROOF STEP]
have "x dvd 1" if "x \<in> {1, -1, \<i>\<^sub>\<int>, -\<i>\<^sub>\<int>}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x dvd 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x dvd 1
[PROOF STEP]
from that
[PROOF STATE]
proof (chain)
picking this:
x \<in> {1, - 1, \<i>\<^sub>\<int>, - \<i>\<^sub>\<int>}
[PROOF STEP]
have *: "x * gauss_cnj x = 1"
[PROOF STATE]
proof (prove)
using this:
x \<in> {1, - 1, \<i>\<^sub>\<int>, - \<i>\<^sub>\<int>}

goal (1 subgoal):
 1. x * gauss_cnj x = 1
[PROOF STEP]
by (auto simp: gauss_int_norm_def)
[PROOF STATE]
proof (state)
this:
x * gauss_cnj x = 1

goal (1 subgoal):
 1. x dvd 1
[PROOF STEP]
show "x dvd 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x dvd 1
[PROOF STEP]
by (subst * [symmetric]) simp
[PROOF STATE]
proof (state)
this:
x dvd 1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<in> {1, - 1, \<i>\<^sub>\<int>, - \<i>\<^sub>\<int>} \<Longrightarrow> x dvd 1

goal (2 subgoals):
 1. (x dvd 1) = (x \<in> {1, - 1, \<i>\<^sub>\<int>, - \<i>\<^sub>\<int>})
 2. (x dvd 1) = (gauss_int_norm x = 1)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<in> {1, - 1, \<i>\<^sub>\<int>, - \<i>\<^sub>\<int>} \<Longrightarrow> x dvd 1

goal (2 subgoals):
 1. (x dvd 1) = (x \<in> {1, - 1, \<i>\<^sub>\<int>, - \<i>\<^sub>\<int>})
 2. (x dvd 1) = (gauss_int_norm x = 1)
[PROOF STEP]
have "gauss_int_norm x = 1" if "x dvd 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gauss_int_norm x = 1
[PROOF STEP]
using gauss_int_norm_dvd_mono[OF that]
[PROOF STATE]
proof (prove)
using this:
gauss_int_norm x dvd gauss_int_norm 1

goal (1 subgoal):
 1. gauss_int_norm x = 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x dvd 1 \<Longrightarrow> gauss_int_norm x = 1

goal (2 subgoals):
 1. (x dvd 1) = (x \<in> {1, - 1, \<i>\<^sub>\<int>, - \<i>\<^sub>\<int>})
 2. (x dvd 1) = (gauss_int_norm x = 1)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x dvd 1 \<Longrightarrow> gauss_int_norm x = 1

goal (2 subgoals):
 1. (x dvd 1) = (x \<in> {1, - 1, \<i>\<^sub>\<int>, - \<i>\<^sub>\<int>})
 2. (x dvd 1) = (gauss_int_norm x = 1)
[PROOF STEP]
have "x \<in> {1, -1, \<i>\<^sub>\<int>, -\<i>\<^sub>\<int>}" if "gauss_int_norm x = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> {1, - 1, \<i>\<^sub>\<int>, - \<i>\<^sub>\<int>}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<in> {1, - 1, \<i>\<^sub>\<int>, - \<i>\<^sub>\<int>}
[PROOF STEP]
from that
[PROOF STATE]
proof (chain)
picking this:
gauss_int_norm x = 1
[PROOF STEP]
have *: "(ReZ x)\<^sup>2 + (ImZ x)\<^sup>2 = 1"
[PROOF STATE]
proof (prove)
using this:
gauss_int_norm x = 1

goal (1 subgoal):
 1. (ReZ x)\<^sup>2 + (ImZ x)\<^sup>2 = 1
[PROOF STEP]
by (auto simp: gauss_int_norm_def nat_eq_iff)
[PROOF STATE]
proof (state)
this:
(ReZ x)\<^sup>2 + (ImZ x)\<^sup>2 = 1

goal (1 subgoal):
 1. x \<in> {1, - 1, \<i>\<^sub>\<int>, - \<i>\<^sub>\<int>}
[PROOF STEP]
hence "ReZ x ^ 2 \<le> 1" and "ImZ x ^ 2 \<le> 1"
[PROOF STATE]
proof (prove)
using this:
(ReZ x)\<^sup>2 + (ImZ x)\<^sup>2 = 1

goal (1 subgoal):
 1. (ReZ x)\<^sup>2 \<le> 1 &&& (ImZ x)\<^sup>2 \<le> 1
[PROOF STEP]
using zero_le_power2[of "ImZ x"] zero_le_power2[of "ReZ x"]
[PROOF STATE]
proof (prove)
using this:
(ReZ x)\<^sup>2 + (ImZ x)\<^sup>2 = 1
0 \<le> (ImZ x)\<^sup>2
0 \<le> (ReZ x)\<^sup>2

goal (1 subgoal):
 1. (ReZ x)\<^sup>2 \<le> 1 &&& (ImZ x)\<^sup>2 \<le> 1
[PROOF STEP]
by linarith+
[PROOF STATE]
proof (state)
this:
(ReZ x)\<^sup>2 \<le> 1
(ImZ x)\<^sup>2 \<le> 1

goal (1 subgoal):
 1. x \<in> {1, - 1, \<i>\<^sub>\<int>, - \<i>\<^sub>\<int>}
[PROOF STEP]
hence "\<bar>ReZ x\<bar> \<le> 1" and "\<bar>ImZ x\<bar> \<le> 1"
[PROOF STATE]
proof (prove)
using this:
(ReZ x)\<^sup>2 \<le> 1
(ImZ x)\<^sup>2 \<le> 1

goal (1 subgoal):
 1. \<bar>ReZ x\<bar> \<le> 1 &&& \<bar>ImZ x\<bar> \<le> 1
[PROOF STEP]
by (auto simp: abs_square_le_1)
[PROOF STATE]
proof (state)
this:
\<bar>ReZ x\<bar> \<le> 1
\<bar>ImZ x\<bar> \<le> 1

goal (1 subgoal):
 1. x \<in> {1, - 1, \<i>\<^sub>\<int>, - \<i>\<^sub>\<int>}
[PROOF STEP]
hence "ReZ x \<in> {-1, 0, 1}" and "ImZ x \<in> {-1, 0, 1}"
[PROOF STATE]
proof (prove)
using this:
\<bar>ReZ x\<bar> \<le> 1
\<bar>ImZ x\<bar> \<le> 1

goal (1 subgoal):
 1. ReZ x \<in> {- 1, 0, 1} &&& ImZ x \<in> {- 1, 0, 1}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ReZ x \<in> {- 1, 0, 1}
ImZ x \<in> {- 1, 0, 1}

goal (1 subgoal):
 1. x \<in> {1, - 1, \<i>\<^sub>\<int>, - \<i>\<^sub>\<int>}
[PROOF STEP]
thus "x \<in> {1, -1, \<i>\<^sub>\<int>, -\<i>\<^sub>\<int> :: gauss_int}"
[PROOF STATE]
proof (prove)
using this:
ReZ x \<in> {- 1, 0, 1}
ImZ x \<in> {- 1, 0, 1}

goal (1 subgoal):
 1. x \<in> {1, - 1, \<i>\<^sub>\<int>, - \<i>\<^sub>\<int>}
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
ReZ x \<in> {- 1, 0, 1}
ImZ x \<in> {- 1, 0, 1}
(ReZ x)\<^sup>2 + (ImZ x)\<^sup>2 = 1

goal (1 subgoal):
 1. x \<in> {1, - 1, \<i>\<^sub>\<int>, - \<i>\<^sub>\<int>}
[PROOF STEP]
by (auto simp: gauss_int_eq_iff)
[PROOF STATE]
proof (state)
this:
x \<in> {1, - 1, \<i>\<^sub>\<int>, - \<i>\<^sub>\<int>}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
gauss_int_norm x = 1 \<Longrightarrow> x \<in> {1, - 1, \<i>\<^sub>\<int>, - \<i>\<^sub>\<int>}

goal (2 subgoals):
 1. (x dvd 1) = (x \<in> {1, - 1, \<i>\<^sub>\<int>, - \<i>\<^sub>\<int>})
 2. (x dvd 1) = (gauss_int_norm x = 1)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x \<in> {1, - 1, \<i>\<^sub>\<int>, - \<i>\<^sub>\<int>} \<Longrightarrow> x dvd 1
x dvd 1 \<Longrightarrow> gauss_int_norm x = 1
gauss_int_norm x = 1 \<Longrightarrow> x \<in> {1, - 1, \<i>\<^sub>\<int>, - \<i>\<^sub>\<int>}
[PROOF STEP]
show "x dvd 1 \<longleftrightarrow> x \<in> {1, -1, \<i>\<^sub>\<int>, -\<i>\<^sub>\<int> :: gauss_int}"
              and "x dvd 1 \<longleftrightarrow> gauss_int_norm x = 1"
[PROOF STATE]
proof (prove)
using this:
x \<in> {1, - 1, \<i>\<^sub>\<int>, - \<i>\<^sub>\<int>} \<Longrightarrow> x dvd 1
x dvd 1 \<Longrightarrow> gauss_int_norm x = 1
gauss_int_norm x = 1 \<Longrightarrow> x \<in> {1, - 1, \<i>\<^sub>\<int>, - \<i>\<^sub>\<int>}

goal (1 subgoal):
 1. (x dvd 1) = (x \<in> {1, - 1, \<i>\<^sub>\<int>, - \<i>\<^sub>\<int>}) &&& (x dvd 1) = (gauss_int_norm x = 1)
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
(x dvd 1) = (x \<in> {1, - 1, \<i>\<^sub>\<int>, - \<i>\<^sub>\<int>})
(x dvd 1) = (gauss_int_norm x = 1)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_unit_gauss_i [simp, intro]: "(gauss_i :: gauss_int) dvd 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<i>\<^sub>\<int> dvd 1
[PROOF STEP]
by (simp add: is_unit_gauss_int_iff)


[STATEMENT]
lemma gauss_int_norm_eq_Suc_0_iff: "gauss_int_norm x = Suc 0 \<longleftrightarrow> x dvd 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (gauss_int_norm x = Suc 0) = (x dvd 1)
[PROOF STEP]
by (simp add: is_unit_gauss_int_iff')


[STATEMENT]
lemma is_unit_gauss_cnj [intro]: "z dvd 1 \<Longrightarrow> gauss_cnj z dvd 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z dvd 1 \<Longrightarrow> gauss_cnj z dvd 1
[PROOF STEP]
by (simp add: is_unit_gauss_int_iff')


[STATEMENT]
lemma is_unit_gauss_cnj_iff [simp]: "gauss_cnj z dvd 1 \<longleftrightarrow> z dvd 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (gauss_cnj z dvd 1) = (z dvd 1)
[PROOF STEP]
by (simp add: is_unit_gauss_int_iff')


[STATEMENT]
lemma norm_round_complex_le: "norm (z - gauss2complex (round_complex z)) ^ 2 \<le> 1 / 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cmod (z - gauss2complex (round_complex z)))\<^sup>2 \<le> 1 / 2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (cmod (z - gauss2complex (round_complex z)))\<^sup>2 \<le> 1 / 2
[PROOF STEP]
have "(Re z - ReZ (round_complex z)) ^ 2 \<le> (1 / 2) ^ 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Re z - real_of_int (ReZ (round_complex z)))\<^sup>2 \<le> (1 / 2)\<^sup>2
[PROOF STEP]
using of_int_round_abs_le[of "Re z"]
[PROOF STATE]
proof (prove)
using this:
\<bar>real_of_int (round (Re z)) - Re z\<bar> \<le> 1 / 2

goal (1 subgoal):
 1. (Re z - real_of_int (ReZ (round_complex z)))\<^sup>2 \<le> (1 / 2)\<^sup>2
[PROOF STEP]
by (subst abs_le_square_iff [symmetric]) (auto simp: abs_minus_commute)
[PROOF STATE]
proof (state)
this:
(Re z - real_of_int (ReZ (round_complex z)))\<^sup>2 \<le> (1 / 2)\<^sup>2

goal (1 subgoal):
 1. (cmod (z - gauss2complex (round_complex z)))\<^sup>2 \<le> 1 / 2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(Re z - real_of_int (ReZ (round_complex z)))\<^sup>2 \<le> (1 / 2)\<^sup>2

goal (1 subgoal):
 1. (cmod (z - gauss2complex (round_complex z)))\<^sup>2 \<le> 1 / 2
[PROOF STEP]
have "(Im z - ImZ (round_complex z)) ^ 2 \<le> (1 / 2) ^ 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Im z - real_of_int (ImZ (round_complex z)))\<^sup>2 \<le> (1 / 2)\<^sup>2
[PROOF STEP]
using of_int_round_abs_le[of "Im z"]
[PROOF STATE]
proof (prove)
using this:
\<bar>real_of_int (round (Im z)) - Im z\<bar> \<le> 1 / 2

goal (1 subgoal):
 1. (Im z - real_of_int (ImZ (round_complex z)))\<^sup>2 \<le> (1 / 2)\<^sup>2
[PROOF STEP]
by (subst abs_le_square_iff [symmetric]) (auto simp: abs_minus_commute)
[PROOF STATE]
proof (state)
this:
(Im z - real_of_int (ImZ (round_complex z)))\<^sup>2 \<le> (1 / 2)\<^sup>2

goal (1 subgoal):
 1. (cmod (z - gauss2complex (round_complex z)))\<^sup>2 \<le> 1 / 2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(Re z - real_of_int (ReZ (round_complex z)))\<^sup>2 \<le> (1 / 2)\<^sup>2
(Im z - real_of_int (ImZ (round_complex z)))\<^sup>2 \<le> (1 / 2)\<^sup>2
[PROOF STEP]
have "(Re z - ReZ (round_complex z)) ^ 2 + (Im z - ImZ (round_complex z)) ^ 2 \<le>
                     (1 / 2) ^ 2 + (1 / 2) ^ 2"
[PROOF STATE]
proof (prove)
using this:
(Re z - real_of_int (ReZ (round_complex z)))\<^sup>2 \<le> (1 / 2)\<^sup>2
(Im z - real_of_int (ImZ (round_complex z)))\<^sup>2 \<le> (1 / 2)\<^sup>2

goal (1 subgoal):
 1. (Re z - real_of_int (ReZ (round_complex z)))\<^sup>2 + (Im z - real_of_int (ImZ (round_complex z)))\<^sup>2 \<le> (1 / 2)\<^sup>2 + (1 / 2)\<^sup>2
[PROOF STEP]
by (rule add_mono)
[PROOF STATE]
proof (state)
this:
(Re z - real_of_int (ReZ (round_complex z)))\<^sup>2 + (Im z - real_of_int (ImZ (round_complex z)))\<^sup>2 \<le> (1 / 2)\<^sup>2 + (1 / 2)\<^sup>2

goal (1 subgoal):
 1. (cmod (z - gauss2complex (round_complex z)))\<^sup>2 \<le> 1 / 2
[PROOF STEP]
thus "norm (z - gauss2complex (round_complex z)) ^ 2 \<le> 1 / 2"
[PROOF STATE]
proof (prove)
using this:
(Re z - real_of_int (ReZ (round_complex z)))\<^sup>2 + (Im z - real_of_int (ImZ (round_complex z)))\<^sup>2 \<le> (1 / 2)\<^sup>2 + (1 / 2)\<^sup>2

goal (1 subgoal):
 1. (cmod (z - gauss2complex (round_complex z)))\<^sup>2 \<le> 1 / 2
[PROOF STEP]
by (simp add: cmod_def power2_eq_square)
[PROOF STATE]
proof (state)
this:
(cmod (z - gauss2complex (round_complex z)))\<^sup>2 \<le> 1 / 2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dist_round_complex_le: "dist z (gauss2complex (round_complex z)) \<le> sqrt 2 / 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist z (gauss2complex (round_complex z)) \<le> sqrt 2 / 2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dist z (gauss2complex (round_complex z)) \<le> sqrt 2 / 2
[PROOF STEP]
have "dist z (gauss2complex (round_complex z)) ^ 2 =
        norm (z - gauss2complex (round_complex z)) ^ 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (dist z (gauss2complex (round_complex z)))\<^sup>2 = (cmod (z - gauss2complex (round_complex z)))\<^sup>2
[PROOF STEP]
by (simp add: dist_norm)
[PROOF STATE]
proof (state)
this:
(dist z (gauss2complex (round_complex z)))\<^sup>2 = (cmod (z - gauss2complex (round_complex z)))\<^sup>2

goal (1 subgoal):
 1. dist z (gauss2complex (round_complex z)) \<le> sqrt 2 / 2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(dist z (gauss2complex (round_complex z)))\<^sup>2 = (cmod (z - gauss2complex (round_complex z)))\<^sup>2

goal (1 subgoal):
 1. dist z (gauss2complex (round_complex z)) \<le> sqrt 2 / 2
[PROOF STEP]
have "\<dots> \<le> 1 / 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cmod (z - gauss2complex (round_complex z)))\<^sup>2 \<le> 1 / 2
[PROOF STEP]
by (rule norm_round_complex_le)
[PROOF STATE]
proof (state)
this:
(cmod (z - gauss2complex (round_complex z)))\<^sup>2 \<le> 1 / 2

goal (1 subgoal):
 1. dist z (gauss2complex (round_complex z)) \<le> sqrt 2 / 2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(cmod (z - gauss2complex (round_complex z)))\<^sup>2 \<le> 1 / 2

goal (1 subgoal):
 1. dist z (gauss2complex (round_complex z)) \<le> sqrt 2 / 2
[PROOF STEP]
have "\<dots> = (sqrt 2 / 2) ^ 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 / 2 = (sqrt 2 / 2)\<^sup>2
[PROOF STEP]
by (simp add: power2_eq_square)
[PROOF STATE]
proof (state)
this:
1 / 2 = (sqrt 2 / 2)\<^sup>2

goal (1 subgoal):
 1. dist z (gauss2complex (round_complex z)) \<le> sqrt 2 / 2
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(dist z (gauss2complex (round_complex z)))\<^sup>2 \<le> (sqrt 2 / 2)\<^sup>2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(dist z (gauss2complex (round_complex z)))\<^sup>2 \<le> (sqrt 2 / 2)\<^sup>2

goal (1 subgoal):
 1. dist z (gauss2complex (round_complex z)) \<le> sqrt 2 / 2
[PROOF STEP]
by (rule power2_le_imp_le) auto
[PROOF STATE]
proof (state)
this:
dist z (gauss2complex (round_complex z)) \<le> sqrt 2 / 2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma normalize_gauss_int_of_nat [simp]: "normalize (of_nat n :: gauss_int) = of_nat n"
  and normalize_gauss_int_of_int [simp]: "normalize (of_int m :: gauss_int) = of_int \<bar>m\<bar>"
  and normalize_gauss_int_of_numeral [simp]: "normalize (numeral n' :: gauss_int) = numeral n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. normalize (of_nat n) = of_nat n &&& normalize (of_int m) = of_int \<bar>m\<bar> &&& normalize (numeral n') = numeral n'
[PROOF STEP]
by (auto simp: normalize_gauss_int_def)


[STATEMENT]
lemma normalize_gauss_i [simp]: "normalize \<i>\<^sub>\<int> = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. normalize \<i>\<^sub>\<int> = 1
[PROOF STEP]
by (simp add: normalize_gauss_int_def)


[STATEMENT]
lemma gauss_int_norm_normalize [simp]: "gauss_int_norm (normalize x) = gauss_int_norm x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gauss_int_norm (normalize x) = gauss_int_norm x
[PROOF STEP]
by (simp add: normalize_gauss_int_def gauss_int_norm_mult)


[STATEMENT]
lemma normalized_gauss_int:
  assumes "normalize z = z"
  shows   "ReZ z \<ge> 0" "ImZ z \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> ReZ z &&& 0 \<le> ImZ z
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
normalize z = z

goal (1 subgoal):
 1. 0 \<le> ReZ z &&& 0 \<le> ImZ z
[PROOF STEP]
by (cases "ReZ z" "0 :: int" rule: linorder_cases;
      cases "ImZ z" "0 :: int" rule: linorder_cases;
      simp add: normalize_gauss_int_def gauss_int_eq_iff)+


[STATEMENT]
lemma normalized_gauss_int':
  assumes "normalize z = z" "z \<noteq> 0"
  shows   "ReZ z > 0" "ImZ z \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < ReZ z &&& 0 \<le> ImZ z
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
normalize z = z
z \<noteq> 0

goal (1 subgoal):
 1. 0 < ReZ z &&& 0 \<le> ImZ z
[PROOF STEP]
by (cases "ReZ z" "0 :: int" rule: linorder_cases;
      cases "ImZ z" "0 :: int" rule: linorder_cases;
      simp add: normalize_gauss_int_def gauss_int_eq_iff)+


[STATEMENT]
lemma normalized_gauss_int_iff:
  "normalize z = z \<longleftrightarrow> z = 0 \<or> ReZ z > 0 \<and> ImZ z \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (normalize z = z) = (z = 0 \<or> 0 < ReZ z \<and> 0 \<le> ImZ z)
[PROOF STEP]
by (cases "ReZ z" "0 :: int" rule: linorder_cases;
      cases "ImZ z" "0 :: int" rule: linorder_cases;
      simp add: normalize_gauss_int_def gauss_int_eq_iff)+


[STATEMENT]
lemma gauss_int_norm_mod_less_aux:
  assumes [simp]: "b \<noteq> 0"
  shows   "2 * gauss_int_norm (a mod b) \<le> gauss_int_norm b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 * gauss_int_norm (a mod b) \<le> gauss_int_norm b
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 2 * gauss_int_norm (a mod b) \<le> gauss_int_norm b
[PROOF STEP]
define a' b' where "a' = gauss2complex a" and "b' = gauss2complex b"
[PROOF STATE]
proof (state)
this:
a' = gauss2complex a
b' = gauss2complex b

goal (1 subgoal):
 1. 2 * gauss_int_norm (a mod b) \<le> gauss_int_norm b
[PROOF STEP]
have [simp]: "b' \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b' \<noteq> 0
[PROOF STEP]
by (simp add: b'_def)
[PROOF STATE]
proof (state)
this:
b' \<noteq> 0

goal (1 subgoal):
 1. 2 * gauss_int_norm (a mod b) \<le> gauss_int_norm b
[PROOF STEP]
have "gauss_int_norm (a mod b) =
          norm (gauss2complex (a - round_complex (a' / b') * b)) ^ 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (gauss_int_norm (a mod b)) = (cmod (gauss2complex (a - round_complex (a' / b') * b)))\<^sup>2
[PROOF STEP]
unfolding modulo_gauss_int_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (gauss_int_norm (a - a div b * b)) = (cmod (gauss2complex (a - round_complex (a' / b') * b)))\<^sup>2
[PROOF STEP]
by (subst real_gauss_int_norm [symmetric]) (auto simp add: divide_gauss_int_def a'_def b'_def)
[PROOF STATE]
proof (state)
this:
real (gauss_int_norm (a mod b)) = (cmod (gauss2complex (a - round_complex (a' / b') * b)))\<^sup>2

goal (1 subgoal):
 1. 2 * gauss_int_norm (a mod b) \<le> gauss_int_norm b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
real (gauss_int_norm (a mod b)) = (cmod (gauss2complex (a - round_complex (a' / b') * b)))\<^sup>2

goal (1 subgoal):
 1. 2 * gauss_int_norm (a mod b) \<le> gauss_int_norm b
[PROOF STEP]
have "gauss2complex (a - round_complex (a' / b') * b) =
               a' - gauss2complex (round_complex (a' / b')) * b'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gauss2complex (a - round_complex (a' / b') * b) = a' - gauss2complex (round_complex (a' / b')) * b'
[PROOF STEP]
by (simp add: a'_def b'_def)
[PROOF STATE]
proof (state)
this:
gauss2complex (a - round_complex (a' / b') * b) = a' - gauss2complex (round_complex (a' / b')) * b'

goal (1 subgoal):
 1. 2 * gauss_int_norm (a mod b) \<le> gauss_int_norm b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
gauss2complex (a - round_complex (a' / b') * b) = a' - gauss2complex (round_complex (a' / b')) * b'

goal (1 subgoal):
 1. 2 * gauss_int_norm (a mod b) \<le> gauss_int_norm b
[PROOF STEP]
have "\<dots> = (a' / b' - gauss2complex (round_complex (a' / b'))) * b'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a' - gauss2complex (round_complex (a' / b')) * b' = (a' / b' - gauss2complex (round_complex (a' / b'))) * b'
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
a' - gauss2complex (round_complex (a' / b')) * b' = (a' / b' - gauss2complex (round_complex (a' / b'))) * b'

goal (1 subgoal):
 1. 2 * gauss_int_norm (a mod b) \<le> gauss_int_norm b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
a' - gauss2complex (round_complex (a' / b')) * b' = (a' / b' - gauss2complex (round_complex (a' / b'))) * b'

goal (1 subgoal):
 1. 2 * gauss_int_norm (a mod b) \<le> gauss_int_norm b
[PROOF STEP]
have "norm \<dots> ^ 2 = norm (a' / b' - gauss2complex (round_complex (a' / b'))) ^ 2 * norm b' ^ 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cmod ((a' / b' - gauss2complex (round_complex (a' / b'))) * b'))\<^sup>2 = (cmod (a' / b' - gauss2complex (round_complex (a' / b'))))\<^sup>2 * (cmod b')\<^sup>2
[PROOF STEP]
by (simp add: norm_mult power_mult_distrib)
[PROOF STATE]
proof (state)
this:
(cmod ((a' / b' - gauss2complex (round_complex (a' / b'))) * b'))\<^sup>2 = (cmod (a' / b' - gauss2complex (round_complex (a' / b'))))\<^sup>2 * (cmod b')\<^sup>2

goal (1 subgoal):
 1. 2 * gauss_int_norm (a mod b) \<le> gauss_int_norm b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(cmod ((a' / b' - gauss2complex (round_complex (a' / b'))) * b'))\<^sup>2 = (cmod (a' / b' - gauss2complex (round_complex (a' / b'))))\<^sup>2 * (cmod b')\<^sup>2

goal (1 subgoal):
 1. 2 * gauss_int_norm (a mod b) \<le> gauss_int_norm b
[PROOF STEP]
have "\<dots> \<le> 1 / 2 * norm b' ^ 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cmod (a' / b' - gauss2complex (round_complex (a' / b'))))\<^sup>2 * (cmod b')\<^sup>2 \<le> 1 / 2 * (cmod b')\<^sup>2
[PROOF STEP]
by (intro mult_right_mono norm_round_complex_le) auto
[PROOF STATE]
proof (state)
this:
(cmod (a' / b' - gauss2complex (round_complex (a' / b'))))\<^sup>2 * (cmod b')\<^sup>2 \<le> 1 / 2 * (cmod b')\<^sup>2

goal (1 subgoal):
 1. 2 * gauss_int_norm (a mod b) \<le> gauss_int_norm b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(cmod (a' / b' - gauss2complex (round_complex (a' / b'))))\<^sup>2 * (cmod b')\<^sup>2 \<le> 1 / 2 * (cmod b')\<^sup>2

goal (1 subgoal):
 1. 2 * gauss_int_norm (a mod b) \<le> gauss_int_norm b
[PROOF STEP]
have "norm b' ^ 2 = gauss_int_norm b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cmod b')\<^sup>2 = real (gauss_int_norm b)
[PROOF STEP]
by (simp add: b'_def real_gauss_int_norm)
[PROOF STATE]
proof (state)
this:
(cmod b')\<^sup>2 = real (gauss_int_norm b)

goal (1 subgoal):
 1. 2 * gauss_int_norm (a mod b) \<le> gauss_int_norm b
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
real (gauss_int_norm (a mod b)) \<le> 1 / 2 * real (gauss_int_norm b)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
real (gauss_int_norm (a mod b)) \<le> 1 / 2 * real (gauss_int_norm b)

goal (1 subgoal):
 1. 2 * gauss_int_norm (a mod b) \<le> gauss_int_norm b
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
2 * gauss_int_norm (a mod b) \<le> gauss_int_norm b

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma gauss_int_norm_mod_less:
  assumes [simp]: "b \<noteq> 0"
  shows   "gauss_int_norm (a mod b) < gauss_int_norm b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gauss_int_norm (a mod b) < gauss_int_norm b
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. gauss_int_norm (a mod b) < gauss_int_norm b
[PROOF STEP]
have "gauss_int_norm b > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < gauss_int_norm b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < gauss_int_norm b

goal (1 subgoal):
 1. gauss_int_norm (a mod b) < gauss_int_norm b
[PROOF STEP]
thus "gauss_int_norm (a mod b) < gauss_int_norm b"
[PROOF STATE]
proof (prove)
using this:
0 < gauss_int_norm b

goal (1 subgoal):
 1. gauss_int_norm (a mod b) < gauss_int_norm b
[PROOF STEP]
using gauss_int_norm_mod_less_aux[OF assms, of a]
[PROOF STATE]
proof (prove)
using this:
0 < gauss_int_norm b
2 * gauss_int_norm (a mod b) \<le> gauss_int_norm b

goal (1 subgoal):
 1. gauss_int_norm (a mod b) < gauss_int_norm b
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
gauss_int_norm (a mod b) < gauss_int_norm b

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma gauss_int_norm_dvd_imp_le:
  assumes "b \<noteq> 0"
  shows   "gauss_int_norm a \<le> gauss_int_norm (a * b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gauss_int_norm a \<le> gauss_int_norm (a * b)
[PROOF STEP]
proof (cases "a = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a = 0 \<Longrightarrow> gauss_int_norm a \<le> gauss_int_norm (a * b)
 2. a \<noteq> 0 \<Longrightarrow> gauss_int_norm a \<le> gauss_int_norm (a * b)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
a \<noteq> 0

goal (2 subgoals):
 1. a = 0 \<Longrightarrow> gauss_int_norm a \<le> gauss_int_norm (a * b)
 2. a \<noteq> 0 \<Longrightarrow> gauss_int_norm a \<le> gauss_int_norm (a * b)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
a \<noteq> 0

goal (1 subgoal):
 1. gauss_int_norm a \<le> gauss_int_norm (a * b)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a \<noteq> 0
b \<noteq> 0

goal (1 subgoal):
 1. gauss_int_norm a \<le> gauss_int_norm (a * b)
[PROOF STEP]
by (intro dvd_imp_le gauss_int_norm_dvd_mono) auto
[PROOF STATE]
proof (state)
this:
gauss_int_norm a \<le> gauss_int_norm (a * b)

goal (1 subgoal):
 1. a = 0 \<Longrightarrow> gauss_int_norm a \<le> gauss_int_norm (a * b)
[PROOF STEP]
qed auto


[STATEMENT]
lemma multiplicity_gauss_cnj: "multiplicity (gauss_cnj a) (gauss_cnj b) = multiplicity a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicity (gauss_cnj a) (gauss_cnj b) = multiplicity a b
[PROOF STEP]
unfolding multiplicity_def gauss_cnj_power [symmetric] gauss_cnj_dvd_iff
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if finite {n. a ^ n dvd b} then Max {n. a ^ n dvd b} else 0) = (if finite {n. a ^ n dvd b} then Max {n. a ^ n dvd b} else 0)
[PROOF STEP]
..


[STATEMENT]
lemma multiplicity_gauss_int_of_nat:
  "multiplicity (of_nat a) (of_nat b :: gauss_int) = multiplicity a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multiplicity (of_nat a) (of_nat b) = multiplicity a b
[PROOF STEP]
unfolding multiplicity_def of_nat_power [symmetric] of_nat_dvd_of_nat_gauss_int_iff
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if finite {n. a ^ n dvd b} then Max {n. a ^ n dvd b} else 0) = (if finite {n. a ^ n dvd b} then Max {n. a ^ n dvd b} else 0)
[PROOF STEP]
..


[STATEMENT]
lemma gauss_int_dvd_same_norm_imp_associated:
  assumes "z1 dvd z2" "gauss_int_norm z1 = gauss_int_norm z2"
  shows   "normalize z1 = normalize z2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. normalize z1 = normalize z2
[PROOF STEP]
proof (cases "z1 = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. z1 = 0 \<Longrightarrow> normalize z1 = normalize z2
 2. z1 \<noteq> 0 \<Longrightarrow> normalize z1 = normalize z2
[PROOF STEP]
case [simp]: False
[PROOF STATE]
proof (state)
this:
z1 \<noteq> 0

goal (2 subgoals):
 1. z1 = 0 \<Longrightarrow> normalize z1 = normalize z2
 2. z1 \<noteq> 0 \<Longrightarrow> normalize z1 = normalize z2
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
z1 dvd z2
[PROOF STEP]
obtain u where u: "z2 = z1 * u"
[PROOF STATE]
proof (prove)
using this:
z1 dvd z2

goal (1 subgoal):
 1. (\<And>u. z2 = z1 * u \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
z2 = z1 * u

goal (2 subgoals):
 1. z1 = 0 \<Longrightarrow> normalize z1 = normalize z2
 2. z1 \<noteq> 0 \<Longrightarrow> normalize z1 = normalize z2
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
z1 dvd z2
gauss_int_norm z1 = gauss_int_norm z2
[PROOF STEP]
have "gauss_int_norm u = 1"
[PROOF STATE]
proof (prove)
using this:
z1 dvd z2
gauss_int_norm z1 = gauss_int_norm z2

goal (1 subgoal):
 1. gauss_int_norm u = 1
[PROOF STEP]
by (auto simp: gauss_int_norm_mult u)
[PROOF STATE]
proof (state)
this:
gauss_int_norm u = 1

goal (2 subgoals):
 1. z1 = 0 \<Longrightarrow> normalize z1 = normalize z2
 2. z1 \<noteq> 0 \<Longrightarrow> normalize z1 = normalize z2
[PROOF STEP]
hence "is_unit u"
[PROOF STATE]
proof (prove)
using this:
gauss_int_norm u = 1

goal (1 subgoal):
 1. is_unit u
[PROOF STEP]
by (simp add: is_unit_gauss_int_iff')
[PROOF STATE]
proof (state)
this:
is_unit u

goal (2 subgoals):
 1. z1 = 0 \<Longrightarrow> normalize z1 = normalize z2
 2. z1 \<noteq> 0 \<Longrightarrow> normalize z1 = normalize z2
[PROOF STEP]
with u
[PROOF STATE]
proof (chain)
picking this:
z2 = z1 * u
is_unit u
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
z2 = z1 * u
is_unit u

goal (1 subgoal):
 1. normalize z1 = normalize z2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
normalize z1 = normalize z2

goal (1 subgoal):
 1. z1 = 0 \<Longrightarrow> normalize z1 = normalize z2
[PROOF STEP]
qed (use assms in auto)


[STATEMENT]
lemma gcd_of_int_gauss_int: "gcd (of_int a :: gauss_int) (of_int b) = of_int (gcd a b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gcd (of_int a) (of_int b) = of_int (gcd a b)
[PROOF STEP]
proof (induction "nat \<bar>b\<bar>" arbitrary: a b rule: less_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>b a. (\<And>ba a. nat \<bar>ba\<bar> < nat \<bar>b\<bar> \<Longrightarrow> gcd (of_int a) (of_int ba) = of_int (gcd a ba)) \<Longrightarrow> gcd (of_int a) (of_int b) = of_int (gcd a b)
[PROOF STEP]
case (less b a)
[PROOF STATE]
proof (state)
this:
nat \<bar>?b\<bar> < nat \<bar>b\<bar> \<Longrightarrow> gcd (of_int ?a) (of_int ?b) = of_int (gcd ?a ?b)

goal (1 subgoal):
 1. \<And>b a. (\<And>ba a. nat \<bar>ba\<bar> < nat \<bar>b\<bar> \<Longrightarrow> gcd (of_int a) (of_int ba) = of_int (gcd a ba)) \<Longrightarrow> gcd (of_int a) (of_int b) = of_int (gcd a b)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gcd (of_int a) (of_int b) = of_int (gcd a b)
[PROOF STEP]
proof (cases "b = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. b = 0 \<Longrightarrow> gcd (of_int a) (of_int b) = of_int (gcd a b)
 2. b \<noteq> 0 \<Longrightarrow> gcd (of_int a) (of_int b) = of_int (gcd a b)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
b \<noteq> 0

goal (2 subgoals):
 1. b = 0 \<Longrightarrow> gcd (of_int a) (of_int b) = of_int (gcd a b)
 2. b \<noteq> 0 \<Longrightarrow> gcd (of_int a) (of_int b) = of_int (gcd a b)
[PROOF STEP]
have "of_int (gcd a b) = (of_int (gcd b (a mod b)) :: gauss_int)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int (gcd a b) = of_int (gcd b (a mod b))
[PROOF STEP]
by (subst gcd_red_int) auto
[PROOF STATE]
proof (state)
this:
of_int (gcd a b) = of_int (gcd b (a mod b))

goal (2 subgoals):
 1. b = 0 \<Longrightarrow> gcd (of_int a) (of_int b) = of_int (gcd a b)
 2. b \<noteq> 0 \<Longrightarrow> gcd (of_int a) (of_int b) = of_int (gcd a b)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
of_int (gcd a b) = of_int (gcd b (a mod b))

goal (2 subgoals):
 1. b = 0 \<Longrightarrow> gcd (of_int a) (of_int b) = of_int (gcd a b)
 2. b \<noteq> 0 \<Longrightarrow> gcd (of_int a) (of_int b) = of_int (gcd a b)
[PROOF STEP]
have "\<dots> = gcd (of_int b) (of_int (a mod b))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int (gcd b (a mod b)) = gcd (of_int b) (of_int (a mod b))
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
b \<noteq> 0

goal (1 subgoal):
 1. of_int (gcd b (a mod b)) = gcd (of_int b) (of_int (a mod b))
[PROOF STEP]
by (intro less [symmetric]) (auto intro!: abs_mod_less)
[PROOF STATE]
proof (state)
this:
of_int (gcd b (a mod b)) = gcd (of_int b) (of_int (a mod b))

goal (2 subgoals):
 1. b = 0 \<Longrightarrow> gcd (of_int a) (of_int b) = of_int (gcd a b)
 2. b \<noteq> 0 \<Longrightarrow> gcd (of_int a) (of_int b) = of_int (gcd a b)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
of_int (gcd b (a mod b)) = gcd (of_int b) (of_int (a mod b))

goal (2 subgoals):
 1. b = 0 \<Longrightarrow> gcd (of_int a) (of_int b) = of_int (gcd a b)
 2. b \<noteq> 0 \<Longrightarrow> gcd (of_int a) (of_int b) = of_int (gcd a b)
[PROOF STEP]
have "a mod b = (a - a div b * b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a mod b = a - a div b * b
[PROOF STEP]
by (simp add: minus_div_mult_eq_mod)
[PROOF STATE]
proof (state)
this:
a mod b = a - a div b * b

goal (2 subgoals):
 1. b = 0 \<Longrightarrow> gcd (of_int a) (of_int b) = of_int (gcd a b)
 2. b \<noteq> 0 \<Longrightarrow> gcd (of_int a) (of_int b) = of_int (gcd a b)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
a mod b = a - a div b * b

goal (2 subgoals):
 1. b = 0 \<Longrightarrow> gcd (of_int a) (of_int b) = of_int (gcd a b)
 2. b \<noteq> 0 \<Longrightarrow> gcd (of_int a) (of_int b) = of_int (gcd a b)
[PROOF STEP]
have "of_int \<dots> = of_int (-(a div b)) * of_int b + (of_int a :: gauss_int)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int (a - a div b * b) = of_int (- (a div b)) * of_int b + of_int a
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
of_int (a - a div b * b) = of_int (- (a div b)) * of_int b + of_int a

goal (2 subgoals):
 1. b = 0 \<Longrightarrow> gcd (of_int a) (of_int b) = of_int (gcd a b)
 2. b \<noteq> 0 \<Longrightarrow> gcd (of_int a) (of_int b) = of_int (gcd a b)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
of_int (a - a div b * b) = of_int (- (a div b)) * of_int b + of_int a

goal (2 subgoals):
 1. b = 0 \<Longrightarrow> gcd (of_int a) (of_int b) = of_int (gcd a b)
 2. b \<noteq> 0 \<Longrightarrow> gcd (of_int a) (of_int b) = of_int (gcd a b)
[PROOF STEP]
have "gcd (of_int b) \<dots> = gcd (of_int b) (of_int a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gcd (of_int b) (of_int (- (a div b)) * of_int b + of_int a) = gcd (of_int b) (of_int a)
[PROOF STEP]
by (rule gcd_add_mult)
[PROOF STATE]
proof (state)
this:
gcd (of_int b) (of_int (- (a div b)) * of_int b + of_int a) = gcd (of_int b) (of_int a)

goal (2 subgoals):
 1. b = 0 \<Longrightarrow> gcd (of_int a) (of_int b) = of_int (gcd a b)
 2. b \<noteq> 0 \<Longrightarrow> gcd (of_int a) (of_int b) = of_int (gcd a b)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
of_int (gcd a b) = gcd (of_int b) (of_int a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
of_int (gcd a b) = gcd (of_int b) (of_int a)

goal (1 subgoal):
 1. gcd (of_int a) (of_int b) = of_int (gcd a b)
[PROOF STEP]
by (simp add: gcd.commute)
[PROOF STATE]
proof (state)
this:
gcd (of_int a) (of_int b) = of_int (gcd a b)

goal (1 subgoal):
 1. b = 0 \<Longrightarrow> gcd (of_int a) (of_int b) = of_int (gcd a b)
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
gcd (of_int a) (of_int b) = of_int (gcd a b)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma coprime_of_int_gauss_int: "coprime (of_int a :: gauss_int) (of_int b) = coprime a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coprime (of_int a) (of_int b) = coprime a b
[PROOF STEP]
unfolding coprime_iff_gcd_eq_1 gcd_of_int_gauss_int
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (of_int (gcd a b) = 1) = (gcd a b = 1)
[PROOF STEP]
by auto


[STATEMENT]
lemma coprime_of_nat_gauss_int: "coprime (of_nat a :: gauss_int) (of_nat b) = coprime a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coprime (of_nat a) (of_nat b) = coprime a b
[PROOF STEP]
unfolding coprime_iff_gcd_eq_1 gcd_of_nat_gauss_int
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (of_nat (gcd a b) = 1) = (gcd a b = 1)
[PROOF STEP]
by auto


[STATEMENT]
lemma self_dvd_gauss_cnj_iff: "z dvd gauss_cnj z \<longleftrightarrow> ReZ z = 0 \<or> ImZ z = 0 \<or> \<bar>ReZ z\<bar> = \<bar>ImZ z\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (z dvd gauss_cnj z) = (ReZ z = 0 \<or> ImZ z = 0 \<or> \<bar>ReZ z\<bar> = \<bar>ImZ z\<bar>)
[PROOF STEP]
using gauss_cnj_dvd_self_iff[of z]
[PROOF STATE]
proof (prove)
using this:
(gauss_cnj z dvd z) = (ReZ z = 0 \<or> ImZ z = 0 \<or> \<bar>ReZ z\<bar> = \<bar>ImZ z\<bar>)

goal (1 subgoal):
 1. (z dvd gauss_cnj z) = (ReZ z = 0 \<or> ImZ z = 0 \<or> \<bar>ReZ z\<bar> = \<bar>ImZ z\<bar>)
[PROOF STEP]
by (subst (asm) gauss_cnj_dvd_left_iff) auto


[STATEMENT]
lemma prime_gauss_int_norm_imp_prime_elem:
  assumes "prime (gauss_int_norm q)"
  shows   "prime_elem q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime_elem q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prime_elem q
[PROOF STEP]
have "irreducible q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. irreducible q
[PROOF STEP]
proof (rule irreducibleI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. q \<noteq> 0
 2. \<not> is_unit q
 3. \<And>a b. q = a * b \<Longrightarrow> is_unit a \<or> is_unit b
[PROOF STEP]
fix a b
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. q \<noteq> 0
 2. \<not> is_unit q
 3. \<And>a b. q = a * b \<Longrightarrow> is_unit a \<or> is_unit b
[PROOF STEP]
assume "q = a * b"
[PROOF STATE]
proof (state)
this:
q = a * b

goal (3 subgoals):
 1. q \<noteq> 0
 2. \<not> is_unit q
 3. \<And>a b. q = a * b \<Longrightarrow> is_unit a \<or> is_unit b
[PROOF STEP]
hence "gauss_int_norm q = gauss_int_norm a * gauss_int_norm b"
[PROOF STATE]
proof (prove)
using this:
q = a * b

goal (1 subgoal):
 1. gauss_int_norm q = gauss_int_norm a * gauss_int_norm b
[PROOF STEP]
by (simp_all add: gauss_int_norm_mult)
[PROOF STATE]
proof (state)
this:
gauss_int_norm q = gauss_int_norm a * gauss_int_norm b

goal (3 subgoals):
 1. q \<noteq> 0
 2. \<not> is_unit q
 3. \<And>a b. q = a * b \<Longrightarrow> is_unit a \<or> is_unit b
[PROOF STEP]
thus "is_unit a \<or> is_unit b"
[PROOF STATE]
proof (prove)
using this:
gauss_int_norm q = gauss_int_norm a * gauss_int_norm b

goal (1 subgoal):
 1. is_unit a \<or> is_unit b
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
gauss_int_norm q = gauss_int_norm a * gauss_int_norm b
prime (gauss_int_norm q)

goal (1 subgoal):
 1. is_unit a \<or> is_unit b
[PROOF STEP]
by (auto dest!: prime_product simp: gauss_int_norm_eq_Suc_0_iff)
[PROOF STATE]
proof (state)
this:
is_unit a \<or> is_unit b

goal (2 subgoals):
 1. q \<noteq> 0
 2. \<not> is_unit q
[PROOF STEP]
qed (use assms in \<open>auto simp: is_unit_gauss_int_iff'\<close>)
[PROOF STATE]
proof (state)
this:
irreducible q

goal (1 subgoal):
 1. prime_elem q
[PROOF STEP]
thus "prime_elem q"
[PROOF STATE]
proof (prove)
using this:
irreducible q

goal (1 subgoal):
 1. prime_elem q
[PROOF STEP]
using irreducible_imp_prime_elem_gcd
[PROOF STATE]
proof (prove)
using this:
irreducible q
irreducible ?x \<Longrightarrow> prime_elem ?x

goal (1 subgoal):
 1. prime_elem q
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
prime_elem q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prime_elem_gauss_cnj [intro]: "prime_elem z \<Longrightarrow> prime_elem (gauss_cnj z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime_elem z \<Longrightarrow> prime_elem (gauss_cnj z)
[PROOF STEP]
by (auto simp: prime_elem_def gauss_cnj_dvd_left_iff)


[STATEMENT]
lemma prime_elem_gauss_cnj_iff [simp]: "prime_elem (gauss_cnj z) \<longleftrightarrow> prime_elem z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime_elem (gauss_cnj z) = prime_elem z
[PROOF STEP]
using prime_elem_gauss_cnj[of z] prime_elem_gauss_cnj[of "gauss_cnj z"]
[PROOF STATE]
proof (prove)
using this:
prime_elem z \<Longrightarrow> prime_elem (gauss_cnj z)
prime_elem (gauss_cnj z) \<Longrightarrow> prime_elem (gauss_cnj (gauss_cnj z))

goal (1 subgoal):
 1. prime_elem (gauss_cnj z) = prime_elem z
[PROOF STEP]
by auto


[STATEMENT]
lemma gauss_int_2_eq: "2 = -\<i>\<^sub>\<int> * (1 + \<i>\<^sub>\<int>) ^ 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 = - \<i>\<^sub>\<int> * (1 + \<i>\<^sub>\<int>)\<^sup>2
[PROOF STEP]
by (simp add: gauss_int_eq_iff power2_eq_square)


[STATEMENT]
lemma prime_elem_one_plus_i_gauss_int: "prime_elem (1 + \<i>\<^sub>\<int>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime_elem (1 + \<i>\<^sub>\<int>)
[PROOF STEP]
by (rule prime_gauss_int_norm_imp_prime_elem) (auto simp: gauss_int_norm_def)


[STATEMENT]
lemma prime_one_plus_i_gauss_int: "prime (1 + \<i>\<^sub>\<int>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime (1 + \<i>\<^sub>\<int>)
[PROOF STEP]
by (simp add: prime_def prime_elem_one_plus_i_gauss_int
                gauss_int_eq_iff normalize_gauss_int_def)


[STATEMENT]
lemma prime_factorization_2_gauss_int:
  "prime_factorization (2 :: gauss_int) = {#1 + \<i>\<^sub>\<int>, 1 + \<i>\<^sub>\<int>#}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime_factorization 2 = {#1 + \<i>\<^sub>\<int>, 1 + \<i>\<^sub>\<int>#}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prime_factorization 2 = {#1 + \<i>\<^sub>\<int>, 1 + \<i>\<^sub>\<int>#}
[PROOF STEP]
have "prime_factorization (2 :: gauss_int) =
        (prime_factorization (prod_mset {#1 + gauss_i, 1 + gauss_i#}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime_factorization 2 = prime_factorization (\<Prod>\<^sub># {#1 + \<i>\<^sub>\<int>, 1 + \<i>\<^sub>\<int>#})
[PROOF STEP]
by (subst prime_factorization_unique) (auto simp: gauss_int_eq_iff normalize_gauss_int_def)
[PROOF STATE]
proof (state)
this:
prime_factorization 2 = prime_factorization (\<Prod>\<^sub># {#1 + \<i>\<^sub>\<int>, 1 + \<i>\<^sub>\<int>#})

goal (1 subgoal):
 1. prime_factorization 2 = {#1 + \<i>\<^sub>\<int>, 1 + \<i>\<^sub>\<int>#}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
prime_factorization 2 = prime_factorization (\<Prod>\<^sub># {#1 + \<i>\<^sub>\<int>, 1 + \<i>\<^sub>\<int>#})

goal (1 subgoal):
 1. prime_factorization 2 = {#1 + \<i>\<^sub>\<int>, 1 + \<i>\<^sub>\<int>#}
[PROOF STEP]
have "prime_factorization (prod_mset {#1 + gauss_i, 1 + gauss_i#}) =
               {#1 + gauss_i, 1 + gauss_i#}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime_factorization (\<Prod>\<^sub># {#1 + \<i>\<^sub>\<int>, 1 + \<i>\<^sub>\<int>#}) = {#1 + \<i>\<^sub>\<int>, 1 + \<i>\<^sub>\<int>#}
[PROOF STEP]
using prime_one_plus_i_gauss_int
[PROOF STATE]
proof (prove)
using this:
prime (1 + \<i>\<^sub>\<int>)

goal (1 subgoal):
 1. prime_factorization (\<Prod>\<^sub># {#1 + \<i>\<^sub>\<int>, 1 + \<i>\<^sub>\<int>#}) = {#1 + \<i>\<^sub>\<int>, 1 + \<i>\<^sub>\<int>#}
[PROOF STEP]
by (subst prime_factorization_prod_mset_primes) auto
[PROOF STATE]
proof (state)
this:
prime_factorization (\<Prod>\<^sub># {#1 + \<i>\<^sub>\<int>, 1 + \<i>\<^sub>\<int>#}) = {#1 + \<i>\<^sub>\<int>, 1 + \<i>\<^sub>\<int>#}

goal (1 subgoal):
 1. prime_factorization 2 = {#1 + \<i>\<^sub>\<int>, 1 + \<i>\<^sub>\<int>#}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
prime_factorization 2 = {#1 + \<i>\<^sub>\<int>, 1 + \<i>\<^sub>\<int>#}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
prime_factorization 2 = {#1 + \<i>\<^sub>\<int>, 1 + \<i>\<^sub>\<int>#}

goal (1 subgoal):
 1. prime_factorization 2 = {#1 + \<i>\<^sub>\<int>, 1 + \<i>\<^sub>\<int>#}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
prime_factorization 2 = {#1 + \<i>\<^sub>\<int>, 1 + \<i>\<^sub>\<int>#}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma gauss_int_norm_not_3_mod_4: "[gauss_int_norm z \<noteq> 3] (mod 4)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [gauss_int_norm z \<noteq> 3] (mod 4)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [gauss_int_norm z \<noteq> 3] (mod 4)
[PROOF STEP]
have A: "ReZ z mod 4 \<in> {0..3}" "ImZ z mod 4 \<in> {0..3}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ReZ z mod 4 \<in> {0..3} &&& ImZ z mod 4 \<in> {0..3}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ReZ z mod 4 \<in> {0..3}
ImZ z mod 4 \<in> {0..3}

goal (1 subgoal):
 1. [gauss_int_norm z \<noteq> 3] (mod 4)
[PROOF STEP]
have B: "{0..3} = {0, 1, 2, 3 :: int}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {0..3} = {0, 1, 2, 3}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{0..3} = {0, 1, 2, 3}

goal (1 subgoal):
 1. [gauss_int_norm z \<noteq> 3] (mod 4)
[PROOF STEP]
have "[ReZ z ^ 2 + ImZ z ^ 2 = (ReZ z mod 4) ^ 2 + (ImZ z mod 4) ^ 2] (mod 4)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [(ReZ z)\<^sup>2 + (ImZ z)\<^sup>2 = (ReZ z mod 4)\<^sup>2 + (ImZ z mod 4)\<^sup>2] (mod 4)
[PROOF STEP]
by (intro cong_add cong_pow) (auto simp: cong_def)
[PROOF STATE]
proof (state)
this:
[(ReZ z)\<^sup>2 + (ImZ z)\<^sup>2 = (ReZ z mod 4)\<^sup>2 + (ImZ z mod 4)\<^sup>2] (mod 4)

goal (1 subgoal):
 1. [gauss_int_norm z \<noteq> 3] (mod 4)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
[(ReZ z)\<^sup>2 + (ImZ z)\<^sup>2 = (ReZ z mod 4)\<^sup>2 + (ImZ z mod 4)\<^sup>2] (mod 4)

goal (1 subgoal):
 1. [gauss_int_norm z \<noteq> 3] (mod 4)
[PROOF STEP]
have "((ReZ z mod 4) ^ 2 + (ImZ z mod 4) ^ 2) mod 4 \<noteq> 3 mod 4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((ReZ z mod 4)\<^sup>2 + (ImZ z mod 4)\<^sup>2) mod 4 \<noteq> 3 mod 4
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
ReZ z mod 4 \<in> {0..3}
ImZ z mod 4 \<in> {0..3}

goal (1 subgoal):
 1. ((ReZ z mod 4)\<^sup>2 + (ImZ z mod 4)\<^sup>2) mod 4 \<noteq> 3 mod 4
[PROOF STEP]
unfolding B
[PROOF STATE]
proof (prove)
using this:
ReZ z mod 4 \<in> {0, 1, 2, 3}
ImZ z mod 4 \<in> {0, 1, 2, 3}

goal (1 subgoal):
 1. ((ReZ z mod 4)\<^sup>2 + (ImZ z mod 4)\<^sup>2) mod 4 \<noteq> 3 mod 4
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
((ReZ z mod 4)\<^sup>2 + (ImZ z mod 4)\<^sup>2) mod 4 \<noteq> 3 mod 4

goal (1 subgoal):
 1. [gauss_int_norm z \<noteq> 3] (mod 4)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
[(ReZ z)\<^sup>2 + (ImZ z)\<^sup>2 = (ReZ z mod 4)\<^sup>2 + (ImZ z mod 4)\<^sup>2] (mod 4)
((ReZ z mod 4)\<^sup>2 + (ImZ z mod 4)\<^sup>2) mod 4 \<noteq> 3 mod 4
[PROOF STEP]
have "[ReZ z ^ 2 + ImZ z ^ 2 \<noteq> 3] (mod 4)"
[PROOF STATE]
proof (prove)
using this:
[(ReZ z)\<^sup>2 + (ImZ z)\<^sup>2 = (ReZ z mod 4)\<^sup>2 + (ImZ z mod 4)\<^sup>2] (mod 4)
((ReZ z mod 4)\<^sup>2 + (ImZ z mod 4)\<^sup>2) mod 4 \<noteq> 3 mod 4

goal (1 subgoal):
 1. [(ReZ z)\<^sup>2 + (ImZ z)\<^sup>2 \<noteq> 3] (mod 4)
[PROOF STEP]
unfolding cong_def
[PROOF STATE]
proof (prove)
using this:
((ReZ z)\<^sup>2 + (ImZ z)\<^sup>2) mod 4 = ((ReZ z mod 4)\<^sup>2 + (ImZ z mod 4)\<^sup>2) mod 4
((ReZ z mod 4)\<^sup>2 + (ImZ z mod 4)\<^sup>2) mod 4 \<noteq> 3 mod 4

goal (1 subgoal):
 1. ((ReZ z)\<^sup>2 + (ImZ z)\<^sup>2) mod 4 \<noteq> 3 mod 4
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
[(ReZ z)\<^sup>2 + (ImZ z)\<^sup>2 \<noteq> 3] (mod 4)

goal (1 subgoal):
 1. [gauss_int_norm z \<noteq> 3] (mod 4)
[PROOF STEP]
hence "[int (nat (ReZ z ^ 2 + ImZ z ^ 2)) \<noteq> int 3] (mod (int 4))"
[PROOF STATE]
proof (prove)
using this:
[(ReZ z)\<^sup>2 + (ImZ z)\<^sup>2 \<noteq> 3] (mod 4)

goal (1 subgoal):
 1. [int (nat ((ReZ z)\<^sup>2 + (ImZ z)\<^sup>2)) \<noteq> int 3] (mod int 4)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[int (nat ((ReZ z)\<^sup>2 + (ImZ z)\<^sup>2)) \<noteq> int 3] (mod int 4)

goal (1 subgoal):
 1. [gauss_int_norm z \<noteq> 3] (mod 4)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
[int (nat ((ReZ z)\<^sup>2 + (ImZ z)\<^sup>2)) \<noteq> int 3] (mod int 4)

goal (1 subgoal):
 1. [gauss_int_norm z \<noteq> 3] (mod 4)
[PROOF STEP]
unfolding gauss_int_norm_def
[PROOF STATE]
proof (prove)
using this:
[int (nat ((ReZ z)\<^sup>2 + (ImZ z)\<^sup>2)) \<noteq> int 3] (mod int 4)

goal (1 subgoal):
 1. [nat ((ReZ z)\<^sup>2 + (ImZ z)\<^sup>2) \<noteq> 3] (mod 4)
[PROOF STEP]
by (subst (asm) cong_int_iff)
[PROOF STATE]
proof (state)
this:
[gauss_int_norm z \<noteq> 3] (mod 4)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prime_elem_gauss_int_of_nat:
  fixes n :: nat
  assumes prime: "prime n" and "[n = 3] (mod 4)"
  shows   "prime_elem (of_nat n :: gauss_int)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime_elem (of_nat n)
[PROOF STEP]
proof (intro irreducible_imp_prime_elem irreducibleI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. of_nat n \<noteq> 0
 2. \<not> is_unit (of_nat n)
 3. \<And>a b. of_nat n = a * b \<Longrightarrow> is_unit a \<or> is_unit b
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
prime n
[n = 3] (mod 4)
[PROOF STEP]
show "of_nat n \<noteq> (0 :: gauss_int)"
[PROOF STATE]
proof (prove)
using this:
prime n
[n = 3] (mod 4)

goal (1 subgoal):
 1. of_nat n \<noteq> 0
[PROOF STEP]
by (auto simp: gauss_int_eq_iff)
[PROOF STATE]
proof (state)
this:
of_nat n \<noteq> 0

goal (2 subgoals):
 1. \<not> is_unit (of_nat n)
 2. \<And>a b. of_nat n = a * b \<Longrightarrow> is_unit a \<or> is_unit b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<not> is_unit (of_nat n)
 2. \<And>a b. of_nat n = a * b \<Longrightarrow> is_unit a \<or> is_unit b
[PROOF STEP]
show "\<not>is_unit (of_nat n :: gauss_int)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_unit (of_nat n)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
prime n
[n = 3] (mod 4)

goal (1 subgoal):
 1. \<not> is_unit (of_nat n)
[PROOF STEP]
by (subst is_unit_gauss_int_iff) (auto simp: gauss_int_eq_iff)
[PROOF STATE]
proof (state)
this:
\<not> is_unit (of_nat n)

goal (1 subgoal):
 1. \<And>a b. of_nat n = a * b \<Longrightarrow> is_unit a \<or> is_unit b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. of_nat n = a * b \<Longrightarrow> is_unit a \<or> is_unit b
[PROOF STEP]
fix a b :: gauss_int
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. of_nat n = a * b \<Longrightarrow> is_unit a \<or> is_unit b
[PROOF STEP]
assume *: "of_nat n = a * b"
[PROOF STATE]
proof (state)
this:
of_nat n = a * b

goal (1 subgoal):
 1. \<And>a b. of_nat n = a * b \<Longrightarrow> is_unit a \<or> is_unit b
[PROOF STEP]
hence "gauss_int_norm (a * b) = gauss_int_norm (of_nat n)"
[PROOF STATE]
proof (prove)
using this:
of_nat n = a * b

goal (1 subgoal):
 1. gauss_int_norm (a * b) = gauss_int_norm (of_nat n)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
gauss_int_norm (a * b) = gauss_int_norm (of_nat n)

goal (1 subgoal):
 1. \<And>a b. of_nat n = a * b \<Longrightarrow> is_unit a \<or> is_unit b
[PROOF STEP]
hence *: "gauss_int_norm a * gauss_int_norm b = n ^ 2"
[PROOF STATE]
proof (prove)
using this:
gauss_int_norm (a * b) = gauss_int_norm (of_nat n)

goal (1 subgoal):
 1. gauss_int_norm a * gauss_int_norm b = n\<^sup>2
[PROOF STEP]
by (simp add: gauss_int_norm_mult power2_eq_square flip: nat_mult_distrib)
[PROOF STATE]
proof (state)
this:
gauss_int_norm a * gauss_int_norm b = n\<^sup>2

goal (1 subgoal):
 1. \<And>a b. of_nat n = a * b \<Longrightarrow> is_unit a \<or> is_unit b
[PROOF STEP]
from prime_power_mult_nat[OF prime this]
[PROOF STATE]
proof (chain)
picking this:
\<exists>i j. gauss_int_norm a = n ^ i \<and> gauss_int_norm b = n ^ j
[PROOF STEP]
obtain i j :: nat
    where ij: "gauss_int_norm a = n ^ i" "gauss_int_norm b = n ^ j"
[PROOF STATE]
proof (prove)
using this:
\<exists>i j. gauss_int_norm a = n ^ i \<and> gauss_int_norm b = n ^ j

goal (1 subgoal):
 1. (\<And>i j. \<lbrakk>gauss_int_norm a = n ^ i; gauss_int_norm b = n ^ j\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
gauss_int_norm a = n ^ i
gauss_int_norm b = n ^ j

goal (1 subgoal):
 1. \<And>a b. of_nat n = a * b \<Longrightarrow> is_unit a \<or> is_unit b
[PROOF STEP]
have "i + j = 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i + j = 2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i + j = 2
[PROOF STEP]
have "n ^ (i + j) = n ^ 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n ^ (i + j) = n\<^sup>2
[PROOF STEP]
using ij *
[PROOF STATE]
proof (prove)
using this:
gauss_int_norm a = n ^ i
gauss_int_norm b = n ^ j
gauss_int_norm a * gauss_int_norm b = n\<^sup>2

goal (1 subgoal):
 1. n ^ (i + j) = n\<^sup>2
[PROOF STEP]
by (simp add: power_add)
[PROOF STATE]
proof (state)
this:
n ^ (i + j) = n\<^sup>2

goal (1 subgoal):
 1. i + j = 2
[PROOF STEP]
from prime_power_inj[OF prime this]
[PROOF STATE]
proof (chain)
picking this:
i + j = 2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i + j = 2

goal (1 subgoal):
 1. i + j = 2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
i + j = 2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
i + j = 2

goal (1 subgoal):
 1. \<And>a b. of_nat n = a * b \<Longrightarrow> is_unit a \<or> is_unit b
[PROOF STEP]
hence "i = 0 \<and> j = 2 \<or> i = 1 \<and> j = 1 \<or> i = 2 \<and> j = 0"
[PROOF STATE]
proof (prove)
using this:
i + j = 2

goal (1 subgoal):
 1. i = 0 \<and> j = 2 \<or> i = 1 \<and> j = 1 \<or> i = 2 \<and> j = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i = 0 \<and> j = 2 \<or> i = 1 \<and> j = 1 \<or> i = 2 \<and> j = 0

goal (1 subgoal):
 1. \<And>a b. of_nat n = a * b \<Longrightarrow> is_unit a \<or> is_unit b
[PROOF STEP]
thus "is_unit a \<or> is_unit b"
[PROOF STATE]
proof (prove)
using this:
i = 0 \<and> j = 2 \<or> i = 1 \<and> j = 1 \<or> i = 2 \<and> j = 0

goal (1 subgoal):
 1. is_unit a \<or> is_unit b
[PROOF STEP]
proof (elim disjE)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. i = 0 \<and> j = 2 \<Longrightarrow> is_unit a \<or> is_unit b
 2. i = 1 \<and> j = 1 \<Longrightarrow> is_unit a \<or> is_unit b
 3. i = 2 \<and> j = 0 \<Longrightarrow> is_unit a \<or> is_unit b
[PROOF STEP]
assume "i = 1 \<and> j = 1"
[PROOF STATE]
proof (state)
this:
i = 1 \<and> j = 1

goal (3 subgoals):
 1. i = 0 \<and> j = 2 \<Longrightarrow> is_unit a \<or> is_unit b
 2. i = 1 \<and> j = 1 \<Longrightarrow> is_unit a \<or> is_unit b
 3. i = 2 \<and> j = 0 \<Longrightarrow> is_unit a \<or> is_unit b
[PROOF STEP]
with ij
[PROOF STATE]
proof (chain)
picking this:
gauss_int_norm a = n ^ i
gauss_int_norm b = n ^ j
i = 1 \<and> j = 1
[PROOF STEP]
have "gauss_int_norm a = n"
[PROOF STATE]
proof (prove)
using this:
gauss_int_norm a = n ^ i
gauss_int_norm b = n ^ j
i = 1 \<and> j = 1

goal (1 subgoal):
 1. gauss_int_norm a = n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
gauss_int_norm a = n

goal (3 subgoals):
 1. i = 0 \<and> j = 2 \<Longrightarrow> is_unit a \<or> is_unit b
 2. i = 1 \<and> j = 1 \<Longrightarrow> is_unit a \<or> is_unit b
 3. i = 2 \<and> j = 0 \<Longrightarrow> is_unit a \<or> is_unit b
[PROOF STEP]
hence "[gauss_int_norm a = n] (mod 4)"
[PROOF STATE]
proof (prove)
using this:
gauss_int_norm a = n

goal (1 subgoal):
 1. [gauss_int_norm a = n] (mod 4)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[gauss_int_norm a = n] (mod 4)

goal (3 subgoals):
 1. i = 0 \<and> j = 2 \<Longrightarrow> is_unit a \<or> is_unit b
 2. i = 1 \<and> j = 1 \<Longrightarrow> is_unit a \<or> is_unit b
 3. i = 2 \<and> j = 0 \<Longrightarrow> is_unit a \<or> is_unit b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
[gauss_int_norm a = n] (mod 4)

goal (3 subgoals):
 1. i = 0 \<and> j = 2 \<Longrightarrow> is_unit a \<or> is_unit b
 2. i = 1 \<and> j = 1 \<Longrightarrow> is_unit a \<or> is_unit b
 3. i = 2 \<and> j = 0 \<Longrightarrow> is_unit a \<or> is_unit b
[PROOF STEP]
have "[n = 3] (mod 4)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [n = 3] (mod 4)
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
[n = 3] (mod 4)

goal (3 subgoals):
 1. i = 0 \<and> j = 2 \<Longrightarrow> is_unit a \<or> is_unit b
 2. i = 1 \<and> j = 1 \<Longrightarrow> is_unit a \<or> is_unit b
 3. i = 2 \<and> j = 0 \<Longrightarrow> is_unit a \<or> is_unit b
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
[gauss_int_norm a = 3] (mod 4)
[PROOF STEP]
have "[gauss_int_norm a = 3] (mod 4)"
[PROOF STATE]
proof (prove)
using this:
[gauss_int_norm a = 3] (mod 4)

goal (1 subgoal):
 1. [gauss_int_norm a = 3] (mod 4)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
[gauss_int_norm a = 3] (mod 4)

goal (3 subgoals):
 1. i = 0 \<and> j = 2 \<Longrightarrow> is_unit a \<or> is_unit b
 2. i = 1 \<and> j = 1 \<Longrightarrow> is_unit a \<or> is_unit b
 3. i = 2 \<and> j = 0 \<Longrightarrow> is_unit a \<or> is_unit b
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
[gauss_int_norm a = 3] (mod 4)

goal (3 subgoals):
 1. i = 0 \<and> j = 2 \<Longrightarrow> is_unit a \<or> is_unit b
 2. i = 1 \<and> j = 1 \<Longrightarrow> is_unit a \<or> is_unit b
 3. i = 2 \<and> j = 0 \<Longrightarrow> is_unit a \<or> is_unit b
[PROOF STEP]
have "[gauss_int_norm a \<noteq> 3] (mod 4)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [gauss_int_norm a \<noteq> 3] (mod 4)
[PROOF STEP]
by (rule gauss_int_norm_not_3_mod_4)
[PROOF STATE]
proof (state)
this:
[gauss_int_norm a \<noteq> 3] (mod 4)

goal (3 subgoals):
 1. i = 0 \<and> j = 2 \<Longrightarrow> is_unit a \<or> is_unit b
 2. i = 1 \<and> j = 1 \<Longrightarrow> is_unit a \<or> is_unit b
 3. i = 2 \<and> j = 0 \<Longrightarrow> is_unit a \<or> is_unit b
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
[gauss_int_norm a = 3] (mod 4)
[gauss_int_norm a \<noteq> 3] (mod 4)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
[gauss_int_norm a = 3] (mod 4)
[gauss_int_norm a \<noteq> 3] (mod 4)

goal (1 subgoal):
 1. is_unit a \<or> is_unit b
[PROOF STEP]
by contradiction
[PROOF STATE]
proof (state)
this:
is_unit a \<or> is_unit b

goal (2 subgoals):
 1. i = 0 \<and> j = 2 \<Longrightarrow> is_unit a \<or> is_unit b
 2. i = 2 \<and> j = 0 \<Longrightarrow> is_unit a \<or> is_unit b
[PROOF STEP]
qed (use ij in \<open>auto simp: is_unit_gauss_int_iff'\<close>)
[PROOF STATE]
proof (state)
this:
is_unit a \<or> is_unit b

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem prime_gauss_int_of_nat:
  fixes n :: nat
  assumes prime: "prime n" and "[n = 3] (mod 4)"
  shows   "prime (of_nat n :: gauss_int)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime (of_nat n)
[PROOF STEP]
using prime_elem_gauss_int_of_nat[OF assms]
[PROOF STATE]
proof (prove)
using this:
prime_elem (of_nat n)

goal (1 subgoal):
 1. prime (of_nat n)
[PROOF STEP]
unfolding prime_def
[PROOF STATE]
proof (prove)
using this:
prime_elem (of_nat n)

goal (1 subgoal):
 1. prime_elem (of_nat n) \<and> normalize (of_nat n) = of_nat n
[PROOF STEP]
by simp