[STATEMENT]
lemma prime_1_mod_4_sum_of_squares_unique:
  fixes p :: nat
  assumes "prime p" "[p = 1] (mod 4)"
  shows   "\<exists>!(x,y). x \<le> y \<and> x ^ 2 + y ^ 2 = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>!(x, y). x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p
[PROOF STEP]
proof (rule ex_ex1I)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>x. case x of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p
 2. \<And>x y. \<lbrakk>case x of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p; case y of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
obtain z where z: "gauss_int_norm z = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>z. gauss_int_norm z = p \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using prime_cong_1_mod_4_gauss_int_norm_exists[OF assms]
[PROOF STATE]
proof (prove)
using this:
\<exists>z. gauss_int_norm z = p \<and> 0 < ReZ z \<and> 0 < ImZ z

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

goal (2 subgoals):
 1. \<exists>x. case x of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p
 2. \<And>x y. \<lbrakk>case x of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p; case y of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
show "\<exists>z. case z of (x,y) \<Rightarrow> x \<le> y \<and> x ^ 2 + y ^ 2 = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>z. case z of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p
[PROOF STEP]
proof (cases "\<bar>ReZ z\<bar> \<le> \<bar>ImZ z\<bar>")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<bar>ReZ z\<bar> \<le> \<bar>ImZ z\<bar> \<Longrightarrow> \<exists>z. case z of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p
 2. \<not> \<bar>ReZ z\<bar> \<le> \<bar>ImZ z\<bar> \<Longrightarrow> \<exists>z. case z of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<bar>ReZ z\<bar> \<le> \<bar>ImZ z\<bar>

goal (2 subgoals):
 1. \<bar>ReZ z\<bar> \<le> \<bar>ImZ z\<bar> \<Longrightarrow> \<exists>z. case z of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p
 2. \<not> \<bar>ReZ z\<bar> \<le> \<bar>ImZ z\<bar> \<Longrightarrow> \<exists>z. case z of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p
[PROOF STEP]
with z
[PROOF STATE]
proof (chain)
picking this:
gauss_int_norm z = p
\<bar>ReZ z\<bar> \<le> \<bar>ImZ z\<bar>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
gauss_int_norm z = p
\<bar>ReZ z\<bar> \<le> \<bar>ImZ z\<bar>

goal (1 subgoal):
 1. \<exists>z. case z of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p
[PROOF STEP]
by
      (intro exI[of _ "(nat \<bar>ReZ z\<bar>, nat \<bar>ImZ z\<bar>)"])
      (auto simp: gauss_int_norm_def nat_add_distrib simp flip: nat_power_eq)
[PROOF STATE]
proof (state)
this:
\<exists>z. case z of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p

goal (1 subgoal):
 1. \<not> \<bar>ReZ z\<bar> \<le> \<bar>ImZ z\<bar> \<Longrightarrow> \<exists>z. case z of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> \<bar>ReZ z\<bar> \<le> \<bar>ImZ z\<bar> \<Longrightarrow> \<exists>z. case z of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> \<bar>ReZ z\<bar> \<le> \<bar>ImZ z\<bar>

goal (1 subgoal):
 1. \<not> \<bar>ReZ z\<bar> \<le> \<bar>ImZ z\<bar> \<Longrightarrow> \<exists>z. case z of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p
[PROOF STEP]
with z
[PROOF STATE]
proof (chain)
picking this:
gauss_int_norm z = p
\<not> \<bar>ReZ z\<bar> \<le> \<bar>ImZ z\<bar>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
gauss_int_norm z = p
\<not> \<bar>ReZ z\<bar> \<le> \<bar>ImZ z\<bar>

goal (1 subgoal):
 1. \<exists>z. case z of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p
[PROOF STEP]
by
      (intro exI[of _ "(nat \<bar>ImZ z\<bar>, nat \<bar>ReZ z\<bar>)"])
      (auto simp: gauss_int_norm_def nat_add_distrib simp flip: nat_power_eq)
[PROOF STATE]
proof (state)
this:
\<exists>z. case z of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>z. case z of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>case x of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p; case y of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>case x of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p; case y of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
fix z1 z2
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>case x of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p; case y of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
assume z1: "case z1 of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p"
[PROOF STATE]
proof (state)
this:
case z1 of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>case x of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p; case y of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
assume z2: "case z2 of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p"
[PROOF STATE]
proof (state)
this:
case z2 of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>case x of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p; case y of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
define z1' :: gauss_int where "z1' = of_nat (fst z1) + \<i>\<^sub>\<int> * of_nat (snd z1)"
[PROOF STATE]
proof (state)
this:
z1' = of_nat (fst z1) + \<i>\<^sub>\<int> * of_nat (snd z1)

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>case x of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p; case y of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
define z2' :: gauss_int where "z2' = of_nat (fst z2) + \<i>\<^sub>\<int> * of_nat (snd z2)"
[PROOF STATE]
proof (state)
this:
z2' = of_nat (fst z2) + \<i>\<^sub>\<int> * of_nat (snd z2)

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>case x of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p; case y of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
prime p
[p = 1] (mod 4)
[PROOF STEP]
interpret noninert_gauss_int_prime p
[PROOF STATE]
proof (prove)
using this:
prime p
[p = 1] (mod 4)

goal (1 subgoal):
 1. noninert_gauss_int_prime p
[PROOF STEP]
by unfold_locales auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>case x of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p; case y of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
have norm_z1': "gauss_int_norm z1' = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gauss_int_norm z1' = p
[PROOF STEP]
using z1
[PROOF STATE]
proof (prove)
using this:
case z1 of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p

goal (1 subgoal):
 1. gauss_int_norm z1' = p
[PROOF STEP]
by (simp add: z1'_def gauss_int_norm_def case_prod_unfold nat_add_distrib nat_power_eq)
[PROOF STATE]
proof (state)
this:
gauss_int_norm z1' = p

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>case x of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p; case y of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
have norm_z2': "gauss_int_norm z2' = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gauss_int_norm z2' = p
[PROOF STEP]
using z2
[PROOF STATE]
proof (prove)
using this:
case z2 of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p

goal (1 subgoal):
 1. gauss_int_norm z2' = p
[PROOF STEP]
by (simp add: z2'_def gauss_int_norm_def case_prod_unfold nat_add_distrib nat_power_eq)
[PROOF STATE]
proof (state)
this:
gauss_int_norm z2' = p

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>case x of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p; case y of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
have sgns: "fst z1 > 0" "snd z1 > 0" "fst z2 > 0" "snd z2 > 0" "fst z1 \<noteq> snd z1" "fst z2 \<noteq> snd z2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0 < fst z1 &&& 0 < snd z1 &&& 0 < fst z2) &&& 0 < snd z2 &&& fst z1 \<noteq> snd z1 &&& fst z2 \<noteq> snd z2
[PROOF STEP]
using prime_1_mod_4_sum_of_squares_unique_aux[OF assms, of "fst z1" "snd z1"] z1
          prime_1_mod_4_sum_of_squares_unique_aux[OF assms, of "fst z2" "snd z2"] z2
[PROOF STATE]
proof (prove)
using this:
(fst z1)\<^sup>2 + (snd z1)\<^sup>2 = p \<Longrightarrow> 0 < fst z1 \<and> 0 < snd z1 \<and> fst z1 \<noteq> snd z1
case z1 of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p
(fst z2)\<^sup>2 + (snd z2)\<^sup>2 = p \<Longrightarrow> 0 < fst z2 \<and> 0 < snd z2 \<and> fst z2 \<noteq> snd z2
case z2 of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p

goal (1 subgoal):
 1. (0 < fst z1 &&& 0 < snd z1 &&& 0 < fst z2) &&& 0 < snd z2 &&& fst z1 \<noteq> snd z1 &&& fst z2 \<noteq> snd z2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < fst z1
0 < snd z1
0 < fst z2
0 < snd z2
fst z1 \<noteq> snd z1
fst z2 \<noteq> snd z2

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>case x of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p; case y of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
have [simp]: "normalize z1' = z1'" "normalize z2' = z2'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. normalize z1' = z1' &&& normalize z2' = z2'
[PROOF STEP]
using sgns
[PROOF STATE]
proof (prove)
using this:
0 < fst z1
0 < snd z1
0 < fst z2
0 < snd z2
fst z1 \<noteq> snd z1
fst z2 \<noteq> snd z2

goal (1 subgoal):
 1. normalize z1' = z1' &&& normalize z2' = z2'
[PROOF STEP]
by (subst normalized_gauss_int_iff; simp add: z1'_def z2'_def)+
[PROOF STATE]
proof (state)
this:
normalize z1' = z1'
normalize z2' = z2'

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>case x of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p; case y of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
have "prime z1'" "prime z2'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime z1' &&& prime z2'
[PROOF STEP]
using norm_z1' norm_z2' assms
[PROOF STATE]
proof (prove)
using this:
gauss_int_norm z1' = p
gauss_int_norm z2' = p
prime p
[p = 1] (mod 4)

goal (1 subgoal):
 1. prime z1' &&& prime z2'
[PROOF STEP]
unfolding prime_def
[PROOF STATE]
proof (prove)
using this:
gauss_int_norm z1' = p
gauss_int_norm z2' = p
prime_elem p \<and> normalize p = p
[p = 1] (mod 4)

goal (1 subgoal):
 1. prime_elem z1' \<and> normalize z1' = z1' &&& prime_elem z2' \<and> normalize z2' = z2'
[PROOF STEP]
by (auto simp: prime_gauss_int_norm_imp_prime_elem)
[PROOF STATE]
proof (state)
this:
prime z1'
prime z2'

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>case x of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p; case y of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
have "of_nat p = z1' * gauss_cnj z1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_nat p = z1' * gauss_cnj z1'
[PROOF STEP]
by (simp add: self_mult_gauss_cnj norm_z1')
[PROOF STATE]
proof (state)
this:
of_nat p = z1' * gauss_cnj z1'

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>case x of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p; case y of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
hence "z1' dvd of_nat p"
[PROOF STATE]
proof (prove)
using this:
of_nat p = z1' * gauss_cnj z1'

goal (1 subgoal):
 1. z1' dvd of_nat p
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
z1' dvd of_nat p

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>case x of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p; case y of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
z1' dvd of_nat p

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>case x of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p; case y of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
have "of_nat p = z2' * gauss_cnj z2'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_nat p = z2' * gauss_cnj z2'
[PROOF STEP]
by (simp add: self_mult_gauss_cnj norm_z2')
[PROOF STATE]
proof (state)
this:
of_nat p = z2' * gauss_cnj z2'

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>case x of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p; case y of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
z1' dvd z2' * gauss_cnj z2'
[PROOF STEP]
have "z1' dvd z2' \<or> z1' dvd gauss_cnj z2'"
[PROOF STATE]
proof (prove)
using this:
z1' dvd z2' * gauss_cnj z2'

goal (1 subgoal):
 1. z1' dvd z2' \<or> z1' dvd gauss_cnj z2'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
z1' dvd z2' * gauss_cnj z2'
prime p
[p = 1] (mod 4)

goal (1 subgoal):
 1. z1' dvd z2' \<or> z1' dvd gauss_cnj z2'
[PROOF STEP]
by (subst (asm) prime_elem_dvd_mult_iff)
       (simp add: norm_z1' prime_gauss_int_norm_imp_prime_elem)
[PROOF STATE]
proof (state)
this:
z1' dvd z2' \<or> z1' dvd gauss_cnj z2'

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>case x of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p; case y of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
thus "z1 = z2"
[PROOF STATE]
proof (prove)
using this:
z1' dvd z2' \<or> z1' dvd gauss_cnj z2'

goal (1 subgoal):
 1. z1 = z2
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. z1' dvd z2' \<Longrightarrow> z1 = z2
 2. z1' dvd gauss_cnj z2' \<Longrightarrow> z1 = z2
[PROOF STEP]
assume "z1' dvd z2'"
[PROOF STATE]
proof (state)
this:
z1' dvd z2'

goal (2 subgoals):
 1. z1' dvd z2' \<Longrightarrow> z1 = z2
 2. z1' dvd gauss_cnj z2' \<Longrightarrow> z1 = z2
[PROOF STEP]
with \<open>prime z1'\<close> \<open>prime z2'\<close>
[PROOF STATE]
proof (chain)
picking this:
prime z1'
prime z2'
z1' dvd z2'
[PROOF STEP]
have "z1' = z2'"
[PROOF STATE]
proof (prove)
using this:
prime z1'
prime z2'
z1' dvd z2'

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

goal (2 subgoals):
 1. z1' dvd z2' \<Longrightarrow> z1 = z2
 2. z1' dvd gauss_cnj z2' \<Longrightarrow> z1 = z2
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
z1' = z2'

goal (1 subgoal):
 1. z1 = z2
[PROOF STEP]
by (simp add: z1'_def z2'_def gauss_int_eq_iff prod_eq_iff)
[PROOF STATE]
proof (state)
this:
z1 = z2

goal (1 subgoal):
 1. z1' dvd gauss_cnj z2' \<Longrightarrow> z1 = z2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. z1' dvd gauss_cnj z2' \<Longrightarrow> z1 = z2
[PROOF STEP]
assume dvd: "z1' dvd gauss_cnj z2'"
[PROOF STATE]
proof (state)
this:
z1' dvd gauss_cnj z2'

goal (1 subgoal):
 1. z1' dvd gauss_cnj z2' \<Longrightarrow> z1 = z2
[PROOF STEP]
have "normalize (\<i>\<^sub>\<int> * gauss_cnj z2') = \<i>\<^sub>\<int> * gauss_cnj z2'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. normalize (\<i>\<^sub>\<int> * gauss_cnj z2') = \<i>\<^sub>\<int> * gauss_cnj z2'
[PROOF STEP]
using sgns
[PROOF STATE]
proof (prove)
using this:
0 < fst z1
0 < snd z1
0 < fst z2
0 < snd z2
fst z1 \<noteq> snd z1
fst z2 \<noteq> snd z2

goal (1 subgoal):
 1. normalize (\<i>\<^sub>\<int> * gauss_cnj z2') = \<i>\<^sub>\<int> * gauss_cnj z2'
[PROOF STEP]
by (subst normalized_gauss_int_iff) (auto simp: z2'_def)
[PROOF STATE]
proof (state)
this:
normalize (\<i>\<^sub>\<int> * gauss_cnj z2') = \<i>\<^sub>\<int> * gauss_cnj z2'

goal (1 subgoal):
 1. z1' dvd gauss_cnj z2' \<Longrightarrow> z1 = z2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
normalize (\<i>\<^sub>\<int> * gauss_cnj z2') = \<i>\<^sub>\<int> * gauss_cnj z2'

goal (1 subgoal):
 1. z1' dvd gauss_cnj z2' \<Longrightarrow> z1 = z2
[PROOF STEP]
have "prime_elem (\<i>\<^sub>\<int> * gauss_cnj z2')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime_elem (\<i>\<^sub>\<int> * gauss_cnj z2')
[PROOF STEP]
by (rule prime_gauss_int_norm_imp_prime_elem)
         (simp add: gauss_int_norm_mult norm_z2' \<open>prime p\<close>)
[PROOF STATE]
proof (state)
this:
prime_elem (\<i>\<^sub>\<int> * gauss_cnj z2')

goal (1 subgoal):
 1. z1' dvd gauss_cnj z2' \<Longrightarrow> z1 = z2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
normalize (\<i>\<^sub>\<int> * gauss_cnj z2') = \<i>\<^sub>\<int> * gauss_cnj z2'
prime_elem (\<i>\<^sub>\<int> * gauss_cnj z2')
[PROOF STEP]
have "prime (\<i>\<^sub>\<int> * gauss_cnj z2')"
[PROOF STATE]
proof (prove)
using this:
normalize (\<i>\<^sub>\<int> * gauss_cnj z2') = \<i>\<^sub>\<int> * gauss_cnj z2'
prime_elem (\<i>\<^sub>\<int> * gauss_cnj z2')

goal (1 subgoal):
 1. prime (\<i>\<^sub>\<int> * gauss_cnj z2')
[PROOF STEP]
by (simp add: prime_def)
[PROOF STATE]
proof (state)
this:
prime (\<i>\<^sub>\<int> * gauss_cnj z2')

goal (1 subgoal):
 1. z1' dvd gauss_cnj z2' \<Longrightarrow> z1 = z2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
prime (\<i>\<^sub>\<int> * gauss_cnj z2')

goal (1 subgoal):
 1. z1' dvd gauss_cnj z2' \<Longrightarrow> z1 = z2
[PROOF STEP]
from dvd
[PROOF STATE]
proof (chain)
picking this:
z1' dvd gauss_cnj z2'
[PROOF STEP]
have "z1' dvd \<i>\<^sub>\<int> * gauss_cnj z2'"
[PROOF STATE]
proof (prove)
using this:
z1' dvd gauss_cnj z2'

goal (1 subgoal):
 1. z1' dvd \<i>\<^sub>\<int> * gauss_cnj z2'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
z1' dvd \<i>\<^sub>\<int> * gauss_cnj z2'

goal (1 subgoal):
 1. z1' dvd gauss_cnj z2' \<Longrightarrow> z1 = z2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
prime (\<i>\<^sub>\<int> * gauss_cnj z2')
z1' dvd \<i>\<^sub>\<int> * gauss_cnj z2'
[PROOF STEP]
have "z1' = \<i>\<^sub>\<int> * gauss_cnj z2'"
[PROOF STATE]
proof (prove)
using this:
prime (\<i>\<^sub>\<int> * gauss_cnj z2')
z1' dvd \<i>\<^sub>\<int> * gauss_cnj z2'

goal (1 subgoal):
 1. z1' = \<i>\<^sub>\<int> * gauss_cnj z2'
[PROOF STEP]
using \<open>prime z1'\<close>
[PROOF STATE]
proof (prove)
using this:
prime (\<i>\<^sub>\<int> * gauss_cnj z2')
z1' dvd \<i>\<^sub>\<int> * gauss_cnj z2'
prime z1'

goal (1 subgoal):
 1. z1' = \<i>\<^sub>\<int> * gauss_cnj z2'
[PROOF STEP]
by (simp add: primes_dvd_imp_eq)
[PROOF STATE]
proof (state)
this:
z1' = \<i>\<^sub>\<int> * gauss_cnj z2'

goal (1 subgoal):
 1. z1' dvd gauss_cnj z2' \<Longrightarrow> z1 = z2
[PROOF STEP]
hence False
[PROOF STATE]
proof (prove)
using this:
z1' = \<i>\<^sub>\<int> * gauss_cnj z2'

goal (1 subgoal):
 1. False
[PROOF STEP]
using z1 z2 sgns
[PROOF STATE]
proof (prove)
using this:
z1' = \<i>\<^sub>\<int> * gauss_cnj z2'
case z1 of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p
case z2 of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p
0 < fst z1
0 < snd z1
0 < fst z2
0 < snd z2
fst z1 \<noteq> snd z1
fst z2 \<noteq> snd z2

goal (1 subgoal):
 1. False
[PROOF STEP]
by (auto simp: gauss_int_eq_iff z1'_def z2'_def)
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. z1' dvd gauss_cnj z2' \<Longrightarrow> z1 = z2
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
False

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
z1 = z2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma two_sum_of_squares_nat_iff: "(x :: nat) ^ 2 + y ^ 2 = 2 \<longleftrightarrow> x = 1 \<and> y = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x\<^sup>2 + y\<^sup>2 = 2) = (x = 1 \<and> y = 1)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x\<^sup>2 + y\<^sup>2 = 2 \<Longrightarrow> x = 1 \<and> y = 1
 2. x = 1 \<and> y = 1 \<Longrightarrow> x\<^sup>2 + y\<^sup>2 = 2
[PROOF STEP]
assume eq: "x ^ 2 + y ^ 2 = 2"
[PROOF STATE]
proof (state)
this:
x\<^sup>2 + y\<^sup>2 = 2

goal (2 subgoals):
 1. x\<^sup>2 + y\<^sup>2 = 2 \<Longrightarrow> x = 1 \<and> y = 1
 2. x = 1 \<and> y = 1 \<Longrightarrow> x\<^sup>2 + y\<^sup>2 = 2
[PROOF STEP]
have square_neq_2: "n ^ 2 \<noteq> 2" for n :: nat
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n\<^sup>2 \<noteq> 2
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n\<^sup>2 = 2 \<Longrightarrow> False
[PROOF STEP]
assume *: "n ^ 2 = 2"
[PROOF STATE]
proof (state)
this:
n\<^sup>2 = 2

goal (1 subgoal):
 1. n\<^sup>2 = 2 \<Longrightarrow> False
[PROOF STEP]
have "prime (2 :: nat)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime 2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
prime 2

goal (1 subgoal):
 1. n\<^sup>2 = 2 \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
prime 2

goal (1 subgoal):
 1. False
[PROOF STEP]
by (subst (asm) * [symmetric]) (auto simp: prime_power_iff)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?n\<^sup>2 \<noteq> 2

goal (2 subgoals):
 1. x\<^sup>2 + y\<^sup>2 = 2 \<Longrightarrow> x = 1 \<and> y = 1
 2. x = 1 \<and> y = 1 \<Longrightarrow> x\<^sup>2 + y\<^sup>2 = 2
[PROOF STEP]
from eq
[PROOF STATE]
proof (chain)
picking this:
x\<^sup>2 + y\<^sup>2 = 2
[PROOF STEP]
have "x ^ 2 < 2 ^ 2" "y ^ 2 < 2 ^ 2"
[PROOF STATE]
proof (prove)
using this:
x\<^sup>2 + y\<^sup>2 = 2

goal (1 subgoal):
 1. x\<^sup>2 < 2\<^sup>2 &&& y\<^sup>2 < 2\<^sup>2
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
x\<^sup>2 < 2\<^sup>2
y\<^sup>2 < 2\<^sup>2

goal (2 subgoals):
 1. x\<^sup>2 + y\<^sup>2 = 2 \<Longrightarrow> x = 1 \<and> y = 1
 2. x = 1 \<and> y = 1 \<Longrightarrow> x\<^sup>2 + y\<^sup>2 = 2
[PROOF STEP]
hence "x < 2" "y < 2"
[PROOF STATE]
proof (prove)
using this:
x\<^sup>2 < 2\<^sup>2
y\<^sup>2 < 2\<^sup>2

goal (1 subgoal):
 1. x < 2 &&& y < 2
[PROOF STEP]
using power2_less_imp_less[of x 2] power2_less_imp_less[of y 2]
[PROOF STATE]
proof (prove)
using this:
x\<^sup>2 < 2\<^sup>2
y\<^sup>2 < 2\<^sup>2
\<lbrakk>x\<^sup>2 < 2\<^sup>2; 0 \<le> 2\<rbrakk> \<Longrightarrow> x < 2
\<lbrakk>y\<^sup>2 < 2\<^sup>2; 0 \<le> 2\<rbrakk> \<Longrightarrow> y < 2

goal (1 subgoal):
 1. x < 2 &&& y < 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x < 2
y < 2

goal (2 subgoals):
 1. x\<^sup>2 + y\<^sup>2 = 2 \<Longrightarrow> x = 1 \<and> y = 1
 2. x = 1 \<and> y = 1 \<Longrightarrow> x\<^sup>2 + y\<^sup>2 = 2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x < 2
y < 2

goal (2 subgoals):
 1. x\<^sup>2 + y\<^sup>2 = 2 \<Longrightarrow> x = 1 \<and> y = 1
 2. x = 1 \<and> y = 1 \<Longrightarrow> x\<^sup>2 + y\<^sup>2 = 2
[PROOF STEP]
have "x > 0" "y > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < x &&& 0 < y
[PROOF STEP]
using eq square_neq_2[of x] square_neq_2[of y]
[PROOF STATE]
proof (prove)
using this:
x\<^sup>2 + y\<^sup>2 = 2
x\<^sup>2 \<noteq> 2
y\<^sup>2 \<noteq> 2

goal (1 subgoal):
 1. 0 < x &&& 0 < y
[PROOF STEP]
by (auto intro!: Nat.gr0I)
[PROOF STATE]
proof (state)
this:
0 < x
0 < y

goal (2 subgoals):
 1. x\<^sup>2 + y\<^sup>2 = 2 \<Longrightarrow> x = 1 \<and> y = 1
 2. x = 1 \<and> y = 1 \<Longrightarrow> x\<^sup>2 + y\<^sup>2 = 2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x < 2
y < 2
0 < x
0 < y
[PROOF STEP]
show "x = 1 \<and> y = 1"
[PROOF STATE]
proof (prove)
using this:
x < 2
y < 2
0 < x
0 < y

goal (1 subgoal):
 1. x = 1 \<and> y = 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x = 1 \<and> y = 1

goal (1 subgoal):
 1. x = 1 \<and> y = 1 \<Longrightarrow> x\<^sup>2 + y\<^sup>2 = 2
[PROOF STEP]
qed auto


[STATEMENT]
lemma prime_sum_of_squares_unique:
  fixes p :: nat
  assumes "prime p" "p = 2 \<or> [p = 1] (mod 4)"
  shows   "\<exists>!(x,y). x \<le> y \<and> x ^ 2 + y ^ 2 = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>!(x, y). x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
p = 2 \<or> [p = 1] (mod 4)

goal (1 subgoal):
 1. \<exists>!(x, y). x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p = 2 \<Longrightarrow> \<exists>!(x, y). x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p
 2. [p = 1] (mod 4) \<Longrightarrow> \<exists>!(x, y). x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p
[PROOF STEP]
assume [simp]: "p = 2"
[PROOF STATE]
proof (state)
this:
p = 2

goal (2 subgoals):
 1. p = 2 \<Longrightarrow> \<exists>!(x, y). x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p
 2. [p = 1] (mod 4) \<Longrightarrow> \<exists>!(x, y). x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p
[PROOF STEP]
have **: "(\<lambda>(x,y). x \<le> y \<and> x ^ 2 + y ^ 2 = p) = (\<lambda>z. z = (1,1 :: nat))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>(x, y). x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p) = (\<lambda>z. z = (1, 1))
[PROOF STEP]
using two_sum_of_squares_nat_iff
[PROOF STATE]
proof (prove)
using this:
(?x\<^sup>2 + ?y\<^sup>2 = 2) = (?x = 1 \<and> ?y = 1)

goal (1 subgoal):
 1. (\<lambda>(x, y). x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p) = (\<lambda>z. z = (1, 1))
[PROOF STEP]
by (auto simp: fun_eq_iff)
[PROOF STATE]
proof (state)
this:
(\<lambda>(x, y). x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p) = (\<lambda>z. z = (1, 1))

goal (2 subgoals):
 1. p = 2 \<Longrightarrow> \<exists>!(x, y). x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p
 2. [p = 1] (mod 4) \<Longrightarrow> \<exists>!(x, y). x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lambda>(x, y). x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p) = (\<lambda>z. z = (1, 1))

goal (1 subgoal):
 1. \<exists>!(x, y). x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p
[PROOF STEP]
by (subst **) auto
[PROOF STATE]
proof (state)
this:
\<exists>!(x, y). x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p

goal (1 subgoal):
 1. [p = 1] (mod 4) \<Longrightarrow> \<exists>!(x, y). x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p
[PROOF STEP]
qed (use prime_1_mod_4_sum_of_squares_unique[of p] assms in auto)


[STATEMENT]
lemma prime_square_sum_nat_decomp_eqI:
  assumes "prime p" "x ^ 2 + y ^ 2 = p" "x \<le> y"
  shows   "prime_square_sum_nat_decomp p = (x, y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime_square_sum_nat_decomp p = (x, y)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prime_square_sum_nat_decomp p = (x, y)
[PROOF STEP]
have "[gauss_int_norm (of_nat x + \<i>\<^sub>\<int> * of_nat y) \<noteq> 3] (mod 4)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [gauss_int_norm (of_nat x + \<i>\<^sub>\<int> * of_nat y) \<noteq> 3] (mod 4)
[PROOF STEP]
by (rule gauss_int_norm_not_3_mod_4)
[PROOF STATE]
proof (state)
this:
[gauss_int_norm (of_nat x + \<i>\<^sub>\<int> * of_nat y) \<noteq> 3] (mod 4)

goal (1 subgoal):
 1. prime_square_sum_nat_decomp p = (x, y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
[gauss_int_norm (of_nat x + \<i>\<^sub>\<int> * of_nat y) \<noteq> 3] (mod 4)

goal (1 subgoal):
 1. prime_square_sum_nat_decomp p = (x, y)
[PROOF STEP]
have "gauss_int_norm (of_nat x + \<i>\<^sub>\<int> * of_nat y) = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gauss_int_norm (of_nat x + \<i>\<^sub>\<int> * of_nat y) = p
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
prime p
x\<^sup>2 + y\<^sup>2 = p
x \<le> y

goal (1 subgoal):
 1. gauss_int_norm (of_nat x + \<i>\<^sub>\<int> * of_nat y) = p
[PROOF STEP]
by (auto simp: gauss_int_norm_def nat_add_distrib nat_power_eq)
[PROOF STATE]
proof (state)
this:
gauss_int_norm (of_nat x + \<i>\<^sub>\<int> * of_nat y) = p

goal (1 subgoal):
 1. prime_square_sum_nat_decomp p = (x, y)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
[p \<noteq> 3] (mod 4)
[PROOF STEP]
have "[p \<noteq> 3] (mod 4)"
[PROOF STATE]
proof (prove)
using this:
[p \<noteq> 3] (mod 4)

goal (1 subgoal):
 1. [p \<noteq> 3] (mod 4)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
[p \<noteq> 3] (mod 4)

goal (1 subgoal):
 1. prime_square_sum_nat_decomp p = (x, y)
[PROOF STEP]
with prime_mod_4_cases[of p] assms
[PROOF STATE]
proof (chain)
picking this:
prime p \<Longrightarrow> p = 2 \<or> [p = 1] (mod 4) \<or> [p = 3] (mod 4)
prime p
x\<^sup>2 + y\<^sup>2 = p
x \<le> y
[p \<noteq> 3] (mod 4)
[PROOF STEP]
have *: "p = 2 \<or> [p = 1] (mod 4)"
[PROOF STATE]
proof (prove)
using this:
prime p \<Longrightarrow> p = 2 \<or> [p = 1] (mod 4) \<or> [p = 3] (mod 4)
prime p
x\<^sup>2 + y\<^sup>2 = p
x \<le> y
[p \<noteq> 3] (mod 4)

goal (1 subgoal):
 1. p = 2 \<or> [p = 1] (mod 4)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p = 2 \<or> [p = 1] (mod 4)

goal (1 subgoal):
 1. prime_square_sum_nat_decomp p = (x, y)
[PROOF STEP]
have "prime_square_sum_nat_decomp p = (THE (x,y). x \<le> y \<and> x ^ 2 + y ^ 2 = p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime_square_sum_nat_decomp p = (THE (x, y). x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p)
[PROOF STEP]
using * \<open>prime p\<close>
[PROOF STATE]
proof (prove)
using this:
p = 2 \<or> [p = 1] (mod 4)
prime p

goal (1 subgoal):
 1. prime_square_sum_nat_decomp p = (THE (x, y). x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p)
[PROOF STEP]
by (simp add: prime_square_sum_nat_decomp_def)
[PROOF STATE]
proof (state)
this:
prime_square_sum_nat_decomp p = (THE (x, y). x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p)

goal (1 subgoal):
 1. prime_square_sum_nat_decomp p = (x, y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
prime_square_sum_nat_decomp p = (THE (x, y). x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p)

goal (1 subgoal):
 1. prime_square_sum_nat_decomp p = (x, y)
[PROOF STEP]
have "\<dots> = (x, y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (THE (x, y). x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p) = (x, y)
[PROOF STEP]
proof (rule the1_equality)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>!x. case x of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p
 2. case (x, y) of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p
[PROOF STEP]
show "\<exists>!(x,y). x \<le> y \<and> x ^ 2 + y ^ 2 = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>!(x, y). x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p
[PROOF STEP]
using \<open>prime p\<close> *
[PROOF STATE]
proof (prove)
using this:
prime p
p = 2 \<or> [p = 1] (mod 4)

goal (1 subgoal):
 1. \<exists>!(x, y). x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p
[PROOF STEP]
by (rule prime_sum_of_squares_unique)
[PROOF STATE]
proof (state)
this:
\<exists>!(x, y). x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p

goal (1 subgoal):
 1. case (x, y) of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p
[PROOF STEP]
qed (use assms in auto)
[PROOF STATE]
proof (state)
this:
(THE (x, y). x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p) = (x, y)

goal (1 subgoal):
 1. prime_square_sum_nat_decomp p = (x, y)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
prime_square_sum_nat_decomp p = (x, y)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
prime_square_sum_nat_decomp p = (x, y)

goal (1 subgoal):
 1. prime_square_sum_nat_decomp p = (x, y)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
prime_square_sum_nat_decomp p = (x, y)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prime_square_sum_nat_decomp_correct:
  assumes "prime p" "p = 2 \<or> [p = 1] (mod 4)"
  defines "z \<equiv> prime_square_sum_nat_decomp p"
  shows "fst z ^ 2 + snd z ^ 2 = p" "fst z \<le> snd z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (fst z)\<^sup>2 + (snd z)\<^sup>2 = p &&& fst z \<le> snd z
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (fst z)\<^sup>2 + (snd z)\<^sup>2 = p
 2. fst z \<le> snd z
[PROOF STEP]
define z' where "z' = (THE (x,y). x \<le> y \<and> x ^ 2 + y ^ 2 = p)"
[PROOF STATE]
proof (state)
this:
z' = (THE (x, y). x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p)

goal (2 subgoals):
 1. (fst z)\<^sup>2 + (snd z)\<^sup>2 = p
 2. fst z \<le> snd z
[PROOF STEP]
have "z = z'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z = z'
[PROOF STEP]
unfolding z_def z'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime_square_sum_nat_decomp p = (THE (x, y). x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
prime p
p = 2 \<or> [p = 1] (mod 4)
z \<equiv> prime_square_sum_nat_decomp p

goal (1 subgoal):
 1. prime_square_sum_nat_decomp p = (THE (x, y). x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p)
[PROOF STEP]
by (simp add: prime_square_sum_nat_decomp_def)
[PROOF STATE]
proof (state)
this:
z = z'

goal (2 subgoals):
 1. (fst z)\<^sup>2 + (snd z)\<^sup>2 = p
 2. fst z \<le> snd z
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
z = z'

goal (2 subgoals):
 1. (fst z)\<^sup>2 + (snd z)\<^sup>2 = p
 2. fst z \<le> snd z
[PROOF STEP]
have"\<exists>!(x,y). x \<le> y \<and> x ^ 2 + y ^ 2 = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>!(x, y). x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
prime p
p = 2 \<or> [p = 1] (mod 4)
z \<equiv> prime_square_sum_nat_decomp p

goal (1 subgoal):
 1. \<exists>!(x, y). x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p
[PROOF STEP]
by (intro prime_sum_of_squares_unique)
[PROOF STATE]
proof (state)
this:
\<exists>!(x, y). x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p

goal (2 subgoals):
 1. (fst z)\<^sup>2 + (snd z)\<^sup>2 = p
 2. fst z \<le> snd z
[PROOF STEP]
hence "case z' of (x, y) \<Rightarrow> x \<le> y \<and> x ^ 2 + y ^ 2 = p"
[PROOF STATE]
proof (prove)
using this:
\<exists>!(x, y). x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p

goal (1 subgoal):
 1. case z' of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p
[PROOF STEP]
unfolding z'_def
[PROOF STATE]
proof (prove)
using this:
\<exists>!(x, y). x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p

goal (1 subgoal):
 1. case THE (x, y). x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p
[PROOF STEP]
by (rule theI')
[PROOF STATE]
proof (state)
this:
case z' of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p

goal (2 subgoals):
 1. (fst z)\<^sup>2 + (snd z)\<^sup>2 = p
 2. fst z \<le> snd z
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
case z of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p
[PROOF STEP]
show "fst z ^ 2 + snd z ^ 2 = p" "fst z \<le> snd z"
[PROOF STATE]
proof (prove)
using this:
case z of (x, y) \<Rightarrow> x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p

goal (1 subgoal):
 1. (fst z)\<^sup>2 + (snd z)\<^sup>2 = p &&& fst z \<le> snd z
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(fst z)\<^sup>2 + (snd z)\<^sup>2 = p
fst z \<le> snd z

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sum_of_squares_nat_bound:
  fixes x y n :: nat
  assumes "x ^ 2 + y ^ 2 = n"
  shows   "x \<le> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> n
[PROOF STEP]
proof (cases "x = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = 0 \<Longrightarrow> x \<le> n
 2. x \<noteq> 0 \<Longrightarrow> x \<le> n
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
x \<noteq> 0

goal (2 subgoals):
 1. x = 0 \<Longrightarrow> x \<le> n
 2. x \<noteq> 0 \<Longrightarrow> x \<le> n
[PROOF STEP]
hence "x * 1 \<le> x ^ 2"
[PROOF STATE]
proof (prove)
using this:
x \<noteq> 0

goal (1 subgoal):
 1. x * 1 \<le> x\<^sup>2
[PROOF STEP]
unfolding power2_eq_square
[PROOF STATE]
proof (prove)
using this:
x \<noteq> 0

goal (1 subgoal):
 1. x * 1 \<le> x * x
[PROOF STEP]
by (intro mult_mono) auto
[PROOF STATE]
proof (state)
this:
x * 1 \<le> x\<^sup>2

goal (2 subgoals):
 1. x = 0 \<Longrightarrow> x \<le> n
 2. x \<noteq> 0 \<Longrightarrow> x \<le> n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x * 1 \<le> x\<^sup>2

goal (2 subgoals):
 1. x = 0 \<Longrightarrow> x \<le> n
 2. x \<noteq> 0 \<Longrightarrow> x \<le> n
[PROOF STEP]
have "\<dots> \<le> x ^ 2 + y ^ 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sup>2 \<le> x\<^sup>2 + y\<^sup>2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x\<^sup>2 \<le> x\<^sup>2 + y\<^sup>2

goal (2 subgoals):
 1. x = 0 \<Longrightarrow> x \<le> n
 2. x \<noteq> 0 \<Longrightarrow> x \<le> n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x\<^sup>2 \<le> x\<^sup>2 + y\<^sup>2

goal (2 subgoals):
 1. x = 0 \<Longrightarrow> x \<le> n
 2. x \<noteq> 0 \<Longrightarrow> x \<le> n
[PROOF STEP]
have "\<dots> = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sup>2 + y\<^sup>2 = n
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
x\<^sup>2 + y\<^sup>2 = n

goal (2 subgoals):
 1. x = 0 \<Longrightarrow> x \<le> n
 2. x \<noteq> 0 \<Longrightarrow> x \<le> n
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
x * 1 \<le> n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x * 1 \<le> n

goal (1 subgoal):
 1. x \<le> n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<le> n

goal (1 subgoal):
 1. x = 0 \<Longrightarrow> x \<le> n
[PROOF STEP]
qed auto


[STATEMENT]
lemma sum_of_squares_nat_bound':
  fixes x y n :: nat
  assumes "x ^ 2 + y ^ 2 = n"
  shows   "y \<le> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<le> n
[PROOF STEP]
using sum_of_squares_nat_bound[of y x] assms
[PROOF STATE]
proof (prove)
using this:
y\<^sup>2 + x\<^sup>2 = ?n \<Longrightarrow> y \<le> ?n
x\<^sup>2 + y\<^sup>2 = n

goal (1 subgoal):
 1. y \<le> n
[PROOF STEP]
by (simp add: add.commute)


[STATEMENT]
lemma is_singleton_conv_Ex1:
  "is_singleton A \<longleftrightarrow> (\<exists>!x. x \<in> A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_singleton A = (\<exists>!x. x \<in> A)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. is_singleton A \<Longrightarrow> \<exists>!x. x \<in> A
 2. \<exists>!x. x \<in> A \<Longrightarrow> is_singleton A
[PROOF STEP]
assume "is_singleton A"
[PROOF STATE]
proof (state)
this:
is_singleton A

goal (2 subgoals):
 1. is_singleton A \<Longrightarrow> \<exists>!x. x \<in> A
 2. \<exists>!x. x \<in> A \<Longrightarrow> is_singleton A
[PROOF STEP]
thus "\<exists>!x. x \<in> A"
[PROOF STATE]
proof (prove)
using this:
is_singleton A

goal (1 subgoal):
 1. \<exists>!x. x \<in> A
[PROOF STEP]
by (auto elim!: is_singletonE)
[PROOF STATE]
proof (state)
this:
\<exists>!x. x \<in> A

goal (1 subgoal):
 1. \<exists>!x. x \<in> A \<Longrightarrow> is_singleton A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>!x. x \<in> A \<Longrightarrow> is_singleton A
[PROOF STEP]
assume "\<exists>!x. x \<in> A"
[PROOF STATE]
proof (state)
this:
\<exists>!x. x \<in> A

goal (1 subgoal):
 1. \<exists>!x. x \<in> A \<Longrightarrow> is_singleton A
[PROOF STEP]
thus "is_singleton A"
[PROOF STATE]
proof (prove)
using this:
\<exists>!x. x \<in> A

goal (1 subgoal):
 1. is_singleton A
[PROOF STEP]
by (metis equals0D is_singletonI')
[PROOF STATE]
proof (state)
this:
is_singleton A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma the_elemI:
  assumes "is_singleton A"
  shows   "the_elem A \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the_elem A \<in> A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_singleton A

goal (1 subgoal):
 1. the_elem A \<in> A
[PROOF STEP]
by (elim is_singletonE) auto


[STATEMENT]
lemma prime_square_sum_nat_decomp_code_aux:
  assumes "prime p" "p = 2 \<or> [p = 1] (mod 4)"
  defines "z \<equiv> the_elem (Set.filter (\<lambda>(x,y). x ^ 2 + y ^ 2 = p) (SIGMA x:{0..p}. {x..p}))"
  shows "prime_square_sum_nat_decomp p = z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime_square_sum_nat_decomp p = z
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prime_square_sum_nat_decomp p = z
[PROOF STEP]
let ?A = "Set.filter (\<lambda>(x,y). x ^ 2 + y ^ 2 = p) (SIGMA x:{0..p}. {x..p})"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prime_square_sum_nat_decomp p = z
[PROOF STEP]
have eq: "?A = {(x,y). x \<le> y \<and> x ^ 2 + y ^ 2 = p}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Set.filter (\<lambda>(x, y). x\<^sup>2 + y\<^sup>2 = p) (SIGMA x:{0..p}. {x..p}) = {(x, y). x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p}
[PROOF STEP]
using sum_of_squares_nat_bound [of _ _ p] sum_of_squares_nat_bound' [of _ _ p]
[PROOF STATE]
proof (prove)
using this:
?x\<^sup>2 + ?y\<^sup>2 = p \<Longrightarrow> ?x \<le> p
?x\<^sup>2 + ?y\<^sup>2 = p \<Longrightarrow> ?y \<le> p

goal (1 subgoal):
 1. Set.filter (\<lambda>(x, y). x\<^sup>2 + y\<^sup>2 = p) (SIGMA x:{0..p}. {x..p}) = {(x, y). x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Set.filter (\<lambda>(x, y). x\<^sup>2 + y\<^sup>2 = p) (SIGMA x:{0..p}. {x..p}) = {(x, y). x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p}

goal (1 subgoal):
 1. prime_square_sum_nat_decomp p = z
[PROOF STEP]
have z: "z \<in> Set.filter (\<lambda>(x,y). x ^ 2 + y ^ 2 = p) (SIGMA x:{0..p}. {x..p})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z \<in> Set.filter (\<lambda>(x, y). x\<^sup>2 + y\<^sup>2 = p) (SIGMA x:{0..p}. {x..p})
[PROOF STEP]
unfolding z_def eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the_elem {(x, y). x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p} \<in> {(x, y). x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p}
[PROOF STEP]
using prime_sum_of_squares_unique[OF assms(1,2)]
[PROOF STATE]
proof (prove)
using this:
\<exists>!(x, y). x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p

goal (1 subgoal):
 1. the_elem {(x, y). x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p} \<in> {(x, y). x \<le> y \<and> x\<^sup>2 + y\<^sup>2 = p}
[PROOF STEP]
by (intro the_elemI) (simp add: is_singleton_conv_Ex1)
[PROOF STATE]
proof (state)
this:
z \<in> Set.filter (\<lambda>(x, y). x\<^sup>2 + y\<^sup>2 = p) (SIGMA x:{0..p}. {x..p})

goal (1 subgoal):
 1. prime_square_sum_nat_decomp p = z
[PROOF STEP]
have "prime_square_sum_nat_decomp p = (fst z, snd z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime_square_sum_nat_decomp p = (fst z, snd z)
[PROOF STEP]
using z
[PROOF STATE]
proof (prove)
using this:
z \<in> Set.filter (\<lambda>(x, y). x\<^sup>2 + y\<^sup>2 = p) (SIGMA x:{0..p}. {x..p})

goal (1 subgoal):
 1. prime_square_sum_nat_decomp p = (fst z, snd z)
[PROOF STEP]
by (intro prime_square_sum_nat_decomp_eqI[OF assms(1)]) auto
[PROOF STATE]
proof (state)
this:
prime_square_sum_nat_decomp p = (fst z, snd z)

goal (1 subgoal):
 1. prime_square_sum_nat_decomp p = z
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
prime_square_sum_nat_decomp p = (fst z, snd z)

goal (1 subgoal):
 1. prime_square_sum_nat_decomp p = z
[PROOF STEP]
have "\<dots> = z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (fst z, snd z) = z
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(fst z, snd z) = z

goal (1 subgoal):
 1. prime_square_sum_nat_decomp p = z
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
prime_square_sum_nat_decomp p = z
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
prime_square_sum_nat_decomp p = z

goal (1 subgoal):
 1. prime_square_sum_nat_decomp p = z
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
prime_square_sum_nat_decomp p = z

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prime_square_sum_nat_decomp_code [code]:
  "prime_square_sum_nat_decomp p =
     (if prime p \<and> (p = 2 \<or> [p = 1] (mod 4))
      then the_elem (Set.filter (\<lambda>(x,y). x ^ 2 + y ^ 2 = p) (SIGMA x:{0..p}. {x..p}))
      else (0, 0))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime_square_sum_nat_decomp p = (if prime p \<and> (p = 2 \<or> [p = 1] (mod 4)) then the_elem (Set.filter (\<lambda>(x, y). x\<^sup>2 + y\<^sup>2 = p) (SIGMA x:{0..p}. {x..p})) else (0, 0))
[PROOF STEP]
using prime_square_sum_nat_decomp_code_aux[of p]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>prime p; p = 2 \<or> [p = 1] (mod 4)\<rbrakk> \<Longrightarrow> prime_square_sum_nat_decomp p = the_elem (Set.filter (\<lambda>(x, y). x\<^sup>2 + y\<^sup>2 = p) (SIGMA x:{0..p}. {x..p}))

goal (1 subgoal):
 1. prime_square_sum_nat_decomp p = (if prime p \<and> (p = 2 \<or> [p = 1] (mod 4)) then the_elem (Set.filter (\<lambda>(x, y). x\<^sup>2 + y\<^sup>2 = p) (SIGMA x:{0..p}. {x..p})) else (0, 0))
[PROOF STEP]
by (auto simp: prime_square_sum_nat_decomp_def)


[STATEMENT]
lemma factor_gauss_int_prime_nat_correct:
  assumes "prime p"
  shows   "set (factor_gauss_int_prime_nat p) = prime_factors (of_nat p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (factor_gauss_int_prime_nat p) = prime_factors (of_nat p)
[PROOF STEP]
using prime_mod_4_cases[OF assms]
[PROOF STATE]
proof (prove)
using this:
p = 2 \<or> [p = 1] (mod 4) \<or> [p = 3] (mod 4)

goal (1 subgoal):
 1. set (factor_gauss_int_prime_nat p) = prime_factors (of_nat p)
[PROOF STEP]
proof (elim disjE)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. p = 2 \<Longrightarrow> set (factor_gauss_int_prime_nat p) = prime_factors (of_nat p)
 2. [p = 1] (mod 4) \<Longrightarrow> set (factor_gauss_int_prime_nat p) = prime_factors (of_nat p)
 3. [p = 3] (mod 4) \<Longrightarrow> set (factor_gauss_int_prime_nat p) = prime_factors (of_nat p)
[PROOF STEP]
assume "p = 2"
[PROOF STATE]
proof (state)
this:
p = 2

goal (3 subgoals):
 1. p = 2 \<Longrightarrow> set (factor_gauss_int_prime_nat p) = prime_factors (of_nat p)
 2. [p = 1] (mod 4) \<Longrightarrow> set (factor_gauss_int_prime_nat p) = prime_factors (of_nat p)
 3. [p = 3] (mod 4) \<Longrightarrow> set (factor_gauss_int_prime_nat p) = prime_factors (of_nat p)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
p = 2

goal (1 subgoal):
 1. set (factor_gauss_int_prime_nat p) = prime_factors (of_nat p)
[PROOF STEP]
by (auto simp: prime_factorization_2_gauss_int factor_gauss_int_prime_nat_def)
[PROOF STATE]
proof (state)
this:
set (factor_gauss_int_prime_nat p) = prime_factors (of_nat p)

goal (2 subgoals):
 1. [p = 1] (mod 4) \<Longrightarrow> set (factor_gauss_int_prime_nat p) = prime_factors (of_nat p)
 2. [p = 3] (mod 4) \<Longrightarrow> set (factor_gauss_int_prime_nat p) = prime_factors (of_nat p)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. [p = 1] (mod 4) \<Longrightarrow> set (factor_gauss_int_prime_nat p) = prime_factors (of_nat p)
 2. [p = 3] (mod 4) \<Longrightarrow> set (factor_gauss_int_prime_nat p) = prime_factors (of_nat p)
[PROOF STEP]
assume *: "[p = 3] (mod 4)"
[PROOF STATE]
proof (state)
this:
[p = 3] (mod 4)

goal (2 subgoals):
 1. [p = 1] (mod 4) \<Longrightarrow> set (factor_gauss_int_prime_nat p) = prime_factors (of_nat p)
 2. [p = 3] (mod 4) \<Longrightarrow> set (factor_gauss_int_prime_nat p) = prime_factors (of_nat p)
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
prime p
[p = 3] (mod 4)
[PROOF STEP]
have "prime (of_nat p :: gauss_int)"
[PROOF STATE]
proof (prove)
using this:
prime p
[p = 3] (mod 4)

goal (1 subgoal):
 1. prime (of_nat p)
[PROOF STEP]
by (intro prime_gauss_int_of_nat)
[PROOF STATE]
proof (state)
this:
prime (of_nat p)

goal (2 subgoals):
 1. [p = 1] (mod 4) \<Longrightarrow> set (factor_gauss_int_prime_nat p) = prime_factors (of_nat p)
 2. [p = 3] (mod 4) \<Longrightarrow> set (factor_gauss_int_prime_nat p) = prime_factors (of_nat p)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
prime (of_nat p)

goal (1 subgoal):
 1. set (factor_gauss_int_prime_nat p) = prime_factors (of_nat p)
[PROOF STEP]
using assms *
[PROOF STATE]
proof (prove)
using this:
prime (of_nat p)
prime p
[p = 3] (mod 4)

goal (1 subgoal):
 1. set (factor_gauss_int_prime_nat p) = prime_factors (of_nat p)
[PROOF STEP]
by (auto simp: prime_factorization_prime factor_gauss_int_prime_nat_def cong_def)
[PROOF STATE]
proof (state)
this:
set (factor_gauss_int_prime_nat p) = prime_factors (of_nat p)

goal (1 subgoal):
 1. [p = 1] (mod 4) \<Longrightarrow> set (factor_gauss_int_prime_nat p) = prime_factors (of_nat p)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [p = 1] (mod 4) \<Longrightarrow> set (factor_gauss_int_prime_nat p) = prime_factors (of_nat p)
[PROOF STEP]
assume *: "[p = 1] (mod 4)"
[PROOF STATE]
proof (state)
this:
[p = 1] (mod 4)

goal (1 subgoal):
 1. [p = 1] (mod 4) \<Longrightarrow> set (factor_gauss_int_prime_nat p) = prime_factors (of_nat p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[p = 1] (mod 4)
[PROOF STEP]
interpret noninert_gauss_int_prime p
[PROOF STATE]
proof (prove)
using this:
[p = 1] (mod 4)

goal (1 subgoal):
 1. noninert_gauss_int_prime p
[PROOF STEP]
using \<open>prime p\<close>
[PROOF STATE]
proof (prove)
using this:
[p = 1] (mod 4)
prime p

goal (1 subgoal):
 1. noninert_gauss_int_prime p
[PROOF STEP]
by unfold_locales
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [p = 1] (mod 4) \<Longrightarrow> set (factor_gauss_int_prime_nat p) = prime_factors (of_nat p)
[PROOF STEP]
define z where "z = prime_square_sum_nat_decomp p"
[PROOF STATE]
proof (state)
this:
z = prime_square_sum_nat_decomp p

goal (1 subgoal):
 1. [p = 1] (mod 4) \<Longrightarrow> set (factor_gauss_int_prime_nat p) = prime_factors (of_nat p)
[PROOF STEP]
define x y where "x = fst z" and "y = snd z"
[PROOF STATE]
proof (state)
this:
x = fst z
y = snd z

goal (1 subgoal):
 1. [p = 1] (mod 4) \<Longrightarrow> set (factor_gauss_int_prime_nat p) = prime_factors (of_nat p)
[PROOF STEP]
have xy: "x ^ 2 + y ^ 2 = p" "x \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sup>2 + y\<^sup>2 = p &&& x \<le> y
[PROOF STEP]
using prime_square_sum_nat_decomp_correct[of p] * assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>prime p; p = 2 \<or> [p = 1] (mod 4)\<rbrakk> \<Longrightarrow> (fst (prime_square_sum_nat_decomp p))\<^sup>2 + (snd (prime_square_sum_nat_decomp p))\<^sup>2 = p
\<lbrakk>prime p; p = 2 \<or> [p = 1] (mod 4)\<rbrakk> \<Longrightarrow> fst (prime_square_sum_nat_decomp p) \<le> snd (prime_square_sum_nat_decomp p)
[p = 1] (mod 4)
prime p

goal (1 subgoal):
 1. x\<^sup>2 + y\<^sup>2 = p &&& x \<le> y
[PROOF STEP]
by (auto simp: x_def y_def z_def)
[PROOF STATE]
proof (state)
this:
x\<^sup>2 + y\<^sup>2 = p
x \<le> y

goal (1 subgoal):
 1. [p = 1] (mod 4) \<Longrightarrow> set (factor_gauss_int_prime_nat p) = prime_factors (of_nat p)
[PROOF STEP]
from xy
[PROOF STATE]
proof (chain)
picking this:
x\<^sup>2 + y\<^sup>2 = p
x \<le> y
[PROOF STEP]
have xy_signs: "x > 0" "y > 0"
[PROOF STATE]
proof (prove)
using this:
x\<^sup>2 + y\<^sup>2 = p
x \<le> y

goal (1 subgoal):
 1. 0 < x &&& 0 < y
[PROOF STEP]
using prime_1_mod_4_sum_of_squares_unique_aux[of p x y] assms *
[PROOF STATE]
proof (prove)
using this:
x\<^sup>2 + y\<^sup>2 = p
x \<le> y
\<lbrakk>prime p; [p = 1] (mod 4); x\<^sup>2 + y\<^sup>2 = p\<rbrakk> \<Longrightarrow> 0 < x \<and> 0 < y \<and> x \<noteq> y
prime p
[p = 1] (mod 4)

goal (1 subgoal):
 1. 0 < x &&& 0 < y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < x
0 < y

goal (1 subgoal):
 1. [p = 1] (mod 4) \<Longrightarrow> set (factor_gauss_int_prime_nat p) = prime_factors (of_nat p)
[PROOF STEP]
have norms: "gauss_int_norm (of_nat x + \<i>\<^sub>\<int> * of_nat y) = p"
              "gauss_int_norm (of_nat y + \<i>\<^sub>\<int> * of_nat x) = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gauss_int_norm (of_nat x + \<i>\<^sub>\<int> * of_nat y) = p &&& gauss_int_norm (of_nat y + \<i>\<^sub>\<int> * of_nat x) = p
[PROOF STEP]
using xy
[PROOF STATE]
proof (prove)
using this:
x\<^sup>2 + y\<^sup>2 = p
x \<le> y

goal (1 subgoal):
 1. gauss_int_norm (of_nat x + \<i>\<^sub>\<int> * of_nat y) = p &&& gauss_int_norm (of_nat y + \<i>\<^sub>\<int> * of_nat x) = p
[PROOF STEP]
by (auto simp: gauss_int_norm_def nat_add_distrib nat_power_eq)
[PROOF STATE]
proof (state)
this:
gauss_int_norm (of_nat x + \<i>\<^sub>\<int> * of_nat y) = p
gauss_int_norm (of_nat y + \<i>\<^sub>\<int> * of_nat x) = p

goal (1 subgoal):
 1. [p = 1] (mod 4) \<Longrightarrow> set (factor_gauss_int_prime_nat p) = prime_factors (of_nat p)
[PROOF STEP]
have prime: "prime (of_nat x + \<i>\<^sub>\<int> * of_nat y)" "prime (of_nat y + \<i>\<^sub>\<int> * of_nat x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime (of_nat x + \<i>\<^sub>\<int> * of_nat y) &&& prime (of_nat y + \<i>\<^sub>\<int> * of_nat x)
[PROOF STEP]
using norms xy_signs \<open>prime p\<close>
[PROOF STATE]
proof (prove)
using this:
gauss_int_norm (of_nat x + \<i>\<^sub>\<int> * of_nat y) = p
gauss_int_norm (of_nat y + \<i>\<^sub>\<int> * of_nat x) = p
0 < x
0 < y
prime p

goal (1 subgoal):
 1. prime (of_nat x + \<i>\<^sub>\<int> * of_nat y) &&& prime (of_nat y + \<i>\<^sub>\<int> * of_nat x)
[PROOF STEP]
unfolding prime_def normalized_gauss_int_iff
[PROOF STATE]
proof (prove)
using this:
gauss_int_norm (of_nat x + \<i>\<^sub>\<int> * of_nat y) = p
gauss_int_norm (of_nat y + \<i>\<^sub>\<int> * of_nat x) = p
0 < x
0 < y
prime_elem p \<and> normalize p = p

goal (1 subgoal):
 1. prime_elem (of_nat x + \<i>\<^sub>\<int> * of_nat y) \<and> (of_nat x + \<i>\<^sub>\<int> * of_nat y = 0 \<or> 0 < ReZ (of_nat x + \<i>\<^sub>\<int> * of_nat y) \<and> 0 \<le> ImZ (of_nat x + \<i>\<^sub>\<int> * of_nat y)) &&& prime_elem (of_nat y + \<i>\<^sub>\<int> * of_nat x) \<and> (of_nat y + \<i>\<^sub>\<int> * of_nat x = 0 \<or> 0 < ReZ (of_nat y + \<i>\<^sub>\<int> * of_nat x) \<and> 0 \<le> ImZ (of_nat y + \<i>\<^sub>\<int> * of_nat x))
[PROOF STEP]
by (auto intro!: prime_gauss_int_norm_imp_prime_elem)
[PROOF STATE]
proof (state)
this:
prime (of_nat x + \<i>\<^sub>\<int> * of_nat y)
prime (of_nat y + \<i>\<^sub>\<int> * of_nat x)

goal (1 subgoal):
 1. [p = 1] (mod 4) \<Longrightarrow> set (factor_gauss_int_prime_nat p) = prime_factors (of_nat p)
[PROOF STEP]
have "normalize ((of_nat x + \<i>\<^sub>\<int> * of_nat y) * (of_nat y + \<i>\<^sub>\<int> * of_nat x)) = of_nat p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. normalize ((of_nat x + \<i>\<^sub>\<int> * of_nat y) * (of_nat y + \<i>\<^sub>\<int> * of_nat x)) = of_nat p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. normalize ((of_nat x + \<i>\<^sub>\<int> * of_nat y) * (of_nat y + \<i>\<^sub>\<int> * of_nat x)) = of_nat p
[PROOF STEP]
have "(of_nat x + \<i>\<^sub>\<int> * of_nat y) * (of_nat y + \<i>\<^sub>\<int> * of_nat x) = (\<i>\<^sub>\<int> * of_nat p :: gauss_int)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (of_nat x + \<i>\<^sub>\<int> * of_nat y) * (of_nat y + \<i>\<^sub>\<int> * of_nat x) = \<i>\<^sub>\<int> * of_nat p
[PROOF STEP]
by (subst xy(1) [symmetric]) (auto simp: gauss_int_eq_iff power2_eq_square)
[PROOF STATE]
proof (state)
this:
(of_nat x + \<i>\<^sub>\<int> * of_nat y) * (of_nat y + \<i>\<^sub>\<int> * of_nat x) = \<i>\<^sub>\<int> * of_nat p

goal (1 subgoal):
 1. normalize ((of_nat x + \<i>\<^sub>\<int> * of_nat y) * (of_nat y + \<i>\<^sub>\<int> * of_nat x)) = of_nat p
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(of_nat x + \<i>\<^sub>\<int> * of_nat y) * (of_nat y + \<i>\<^sub>\<int> * of_nat x) = \<i>\<^sub>\<int> * of_nat p

goal (1 subgoal):
 1. normalize ((of_nat x + \<i>\<^sub>\<int> * of_nat y) * (of_nat y + \<i>\<^sub>\<int> * of_nat x)) = of_nat p
[PROOF STEP]
have "normalize \<dots> = of_nat p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. normalize (\<i>\<^sub>\<int> * of_nat p) = of_nat p
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
normalize (\<i>\<^sub>\<int> * of_nat p) = of_nat p

goal (1 subgoal):
 1. normalize ((of_nat x + \<i>\<^sub>\<int> * of_nat y) * (of_nat y + \<i>\<^sub>\<int> * of_nat x)) = of_nat p
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
normalize ((of_nat x + \<i>\<^sub>\<int> * of_nat y) * (of_nat y + \<i>\<^sub>\<int> * of_nat x)) = of_nat p
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
normalize ((of_nat x + \<i>\<^sub>\<int> * of_nat y) * (of_nat y + \<i>\<^sub>\<int> * of_nat x)) = of_nat p

goal (1 subgoal):
 1. normalize ((of_nat x + \<i>\<^sub>\<int> * of_nat y) * (of_nat y + \<i>\<^sub>\<int> * of_nat x)) = of_nat p
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
normalize ((of_nat x + \<i>\<^sub>\<int> * of_nat y) * (of_nat y + \<i>\<^sub>\<int> * of_nat x)) = of_nat p

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
normalize ((of_nat x + \<i>\<^sub>\<int> * of_nat y) * (of_nat y + \<i>\<^sub>\<int> * of_nat x)) = of_nat p

goal (1 subgoal):
 1. [p = 1] (mod 4) \<Longrightarrow> set (factor_gauss_int_prime_nat p) = prime_factors (of_nat p)
[PROOF STEP]
hence "prime_factorization (of_nat p) =
         prime_factorization (prod_mset {#of_nat x + \<i>\<^sub>\<int> * of_nat y, of_nat y + \<i>\<^sub>\<int> * of_nat x#})"
[PROOF STATE]
proof (prove)
using this:
normalize ((of_nat x + \<i>\<^sub>\<int> * of_nat y) * (of_nat y + \<i>\<^sub>\<int> * of_nat x)) = of_nat p

goal (1 subgoal):
 1. prime_factorization (of_nat p) = prime_factorization (\<Prod>\<^sub># {#of_nat x + \<i>\<^sub>\<int> * of_nat y, of_nat y + \<i>\<^sub>\<int> * of_nat x#})
[PROOF STEP]
using assms xy
[PROOF STATE]
proof (prove)
using this:
normalize ((of_nat x + \<i>\<^sub>\<int> * of_nat y) * (of_nat y + \<i>\<^sub>\<int> * of_nat x)) = of_nat p
prime p
x\<^sup>2 + y\<^sup>2 = p
x \<le> y

goal (1 subgoal):
 1. prime_factorization (of_nat p) = prime_factorization (\<Prod>\<^sub># {#of_nat x + \<i>\<^sub>\<int> * of_nat y, of_nat y + \<i>\<^sub>\<int> * of_nat x#})
[PROOF STEP]
by (subst prime_factorization_unique) (auto simp: gauss_int_eq_iff)
[PROOF STATE]
proof (state)
this:
prime_factorization (of_nat p) = prime_factorization (\<Prod>\<^sub># {#of_nat x + \<i>\<^sub>\<int> * of_nat y, of_nat y + \<i>\<^sub>\<int> * of_nat x#})

goal (1 subgoal):
 1. [p = 1] (mod 4) \<Longrightarrow> set (factor_gauss_int_prime_nat p) = prime_factors (of_nat p)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
prime_factorization (of_nat p) = prime_factorization (\<Prod>\<^sub># {#of_nat x + \<i>\<^sub>\<int> * of_nat y, of_nat y + \<i>\<^sub>\<int> * of_nat x#})

goal (1 subgoal):
 1. [p = 1] (mod 4) \<Longrightarrow> set (factor_gauss_int_prime_nat p) = prime_factors (of_nat p)
[PROOF STEP]
have "\<dots> = {#of_nat x + \<i>\<^sub>\<int> * of_nat y, of_nat y + \<i>\<^sub>\<int> * of_nat x#}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime_factorization (\<Prod>\<^sub># {#of_nat x + \<i>\<^sub>\<int> * of_nat y, of_nat y + \<i>\<^sub>\<int> * of_nat x#}) = {#of_nat x + \<i>\<^sub>\<int> * of_nat y, of_nat y + \<i>\<^sub>\<int> * of_nat x#}
[PROOF STEP]
using prime
[PROOF STATE]
proof (prove)
using this:
prime (of_nat x + \<i>\<^sub>\<int> * of_nat y)
prime (of_nat y + \<i>\<^sub>\<int> * of_nat x)

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

goal (1 subgoal):
 1. [p = 1] (mod 4) \<Longrightarrow> set (factor_gauss_int_prime_nat p) = prime_factors (of_nat p)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
prime_factorization (of_nat p) = {#of_nat x + \<i>\<^sub>\<int> * of_nat y, of_nat y + \<i>\<^sub>\<int> * of_nat x#}
[PROOF STEP]
have "prime_factors (of_nat p) = {of_nat x + \<i>\<^sub>\<int> * of_nat y, of_nat y + \<i>\<^sub>\<int> * of_nat x}"
[PROOF STATE]
proof (prove)
using this:
prime_factorization (of_nat p) = {#of_nat x + \<i>\<^sub>\<int> * of_nat y, of_nat y + \<i>\<^sub>\<int> * of_nat x#}

goal (1 subgoal):
 1. prime_factors (of_nat p) = {of_nat x + \<i>\<^sub>\<int> * of_nat y, of_nat y + \<i>\<^sub>\<int> * of_nat x}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
prime_factors (of_nat p) = {of_nat x + \<i>\<^sub>\<int> * of_nat y, of_nat y + \<i>\<^sub>\<int> * of_nat x}

goal (1 subgoal):
 1. [p = 1] (mod 4) \<Longrightarrow> set (factor_gauss_int_prime_nat p) = prime_factors (of_nat p)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
prime_factors (of_nat p) = {of_nat x + \<i>\<^sub>\<int> * of_nat y, of_nat y + \<i>\<^sub>\<int> * of_nat x}

goal (1 subgoal):
 1. [p = 1] (mod 4) \<Longrightarrow> set (factor_gauss_int_prime_nat p) = prime_factors (of_nat p)
[PROOF STEP]
have "\<dots> = set (factor_gauss_int_prime_nat p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {of_nat x + \<i>\<^sub>\<int> * of_nat y, of_nat y + \<i>\<^sub>\<int> * of_nat x} = set (factor_gauss_int_prime_nat p)
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
[p = 1] (mod 4)

goal (1 subgoal):
 1. {of_nat x + \<i>\<^sub>\<int> * of_nat y, of_nat y + \<i>\<^sub>\<int> * of_nat x} = set (factor_gauss_int_prime_nat p)
[PROOF STEP]
unfolding factor_gauss_int_prime_nat_def case_prod_unfold
[PROOF STATE]
proof (prove)
using this:
[p = 1] (mod 4)

goal (1 subgoal):
 1. {of_nat x + \<i>\<^sub>\<int> * of_nat y, of_nat y + \<i>\<^sub>\<int> * of_nat x} = set (if p = 2 then [1 + \<i>\<^sub>\<int>] else if [p = 3] (mod 4) then [of_nat p] else [of_nat (fst (prime_square_sum_nat_decomp p)) + \<i>\<^sub>\<int> * of_nat (snd (prime_square_sum_nat_decomp p)), of_nat (snd (prime_square_sum_nat_decomp p)) + \<i>\<^sub>\<int> * of_nat (fst (prime_square_sum_nat_decomp p))])
[PROOF STEP]
by (auto simp: cong_def x_def y_def z_def)
[PROOF STATE]
proof (state)
this:
{of_nat x + \<i>\<^sub>\<int> * of_nat y, of_nat y + \<i>\<^sub>\<int> * of_nat x} = set (factor_gauss_int_prime_nat p)

goal (1 subgoal):
 1. [p = 1] (mod 4) \<Longrightarrow> set (factor_gauss_int_prime_nat p) = prime_factors (of_nat p)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
prime_factors (of_nat p) = set (factor_gauss_int_prime_nat p)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
prime_factors (of_nat p) = set (factor_gauss_int_prime_nat p)

goal (1 subgoal):
 1. set (factor_gauss_int_prime_nat p) = prime_factors (of_nat p)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
set (factor_gauss_int_prime_nat p) = prime_factors (of_nat p)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prime_factors_gauss_int_of_nat_correct:
  "prime_factors_gauss_int_of_nat n = prime_factors (of_nat n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime_factors_gauss_int_of_nat n = prime_factors (of_nat n)
[PROOF STEP]
proof (cases "n = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n = 0 \<Longrightarrow> prime_factors_gauss_int_of_nat n = prime_factors (of_nat n)
 2. n \<noteq> 0 \<Longrightarrow> prime_factors_gauss_int_of_nat n = prime_factors (of_nat n)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
n \<noteq> 0

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> prime_factors_gauss_int_of_nat n = prime_factors (of_nat n)
 2. n \<noteq> 0 \<Longrightarrow> prime_factors_gauss_int_of_nat n = prime_factors (of_nat n)
[PROOF STEP]
from False
[PROOF STATE]
proof (chain)
picking this:
n \<noteq> 0
[PROOF STEP]
have [simp]: "n > 0"
[PROOF STATE]
proof (prove)
using this:
n \<noteq> 0

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

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> prime_factors_gauss_int_of_nat n = prime_factors (of_nat n)
 2. n \<noteq> 0 \<Longrightarrow> prime_factors_gauss_int_of_nat n = prime_factors (of_nat n)
[PROOF STEP]
have "prime_factors (of_nat n :: gauss_int) =
          prime_factors (of_nat (prod_mset (prime_factorization n)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime_factors (of_nat n) = prime_factors (of_nat (\<Prod>\<^sub># (prime_factorization n)))
[PROOF STEP]
by (subst prod_mset_prime_factorization_nat [symmetric]) auto
[PROOF STATE]
proof (state)
this:
prime_factors (of_nat n) = prime_factors (of_nat (\<Prod>\<^sub># (prime_factorization n)))

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> prime_factors_gauss_int_of_nat n = prime_factors (of_nat n)
 2. n \<noteq> 0 \<Longrightarrow> prime_factors_gauss_int_of_nat n = prime_factors (of_nat n)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
prime_factors (of_nat n) = prime_factors (of_nat (\<Prod>\<^sub># (prime_factorization n)))

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> prime_factors_gauss_int_of_nat n = prime_factors (of_nat n)
 2. n \<noteq> 0 \<Longrightarrow> prime_factors_gauss_int_of_nat n = prime_factors (of_nat n)
[PROOF STEP]
have "\<dots> = prime_factors (prod_mset (image_mset of_nat (prime_factorization n)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime_factors (of_nat (\<Prod>\<^sub># (prime_factorization n))) = prime_factors (\<Prod>\<^sub># (image_mset of_nat (prime_factorization n)))
[PROOF STEP]
by (subst of_nat_prod_mset) auto
[PROOF STATE]
proof (state)
this:
prime_factors (of_nat (\<Prod>\<^sub># (prime_factorization n))) = prime_factors (\<Prod>\<^sub># (image_mset of_nat (prime_factorization n)))

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> prime_factors_gauss_int_of_nat n = prime_factors (of_nat n)
 2. n \<noteq> 0 \<Longrightarrow> prime_factors_gauss_int_of_nat n = prime_factors (of_nat n)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
prime_factors (of_nat (\<Prod>\<^sub># (prime_factorization n))) = prime_factors (\<Prod>\<^sub># (image_mset of_nat (prime_factorization n)))

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> prime_factors_gauss_int_of_nat n = prime_factors (of_nat n)
 2. n \<noteq> 0 \<Longrightarrow> prime_factors_gauss_int_of_nat n = prime_factors (of_nat n)
[PROOF STEP]
have "\<dots> = (\<Union>p\<in>prime_factors n. prime_factors (of_nat p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime_factors (\<Prod>\<^sub># (image_mset of_nat (prime_factorization n))) = (\<Union>p\<in>prime_factors n. prime_factors (of_nat p))
[PROOF STEP]
by (subst prime_factorization_prod_mset) auto
[PROOF STATE]
proof (state)
this:
prime_factors (\<Prod>\<^sub># (image_mset of_nat (prime_factorization n))) = (\<Union>p\<in>prime_factors n. prime_factors (of_nat p))

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> prime_factors_gauss_int_of_nat n = prime_factors (of_nat n)
 2. n \<noteq> 0 \<Longrightarrow> prime_factors_gauss_int_of_nat n = prime_factors (of_nat n)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
prime_factors (\<Prod>\<^sub># (image_mset of_nat (prime_factorization n))) = (\<Union>p\<in>prime_factors n. prime_factors (of_nat p))

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> prime_factors_gauss_int_of_nat n = prime_factors (of_nat n)
 2. n \<noteq> 0 \<Longrightarrow> prime_factors_gauss_int_of_nat n = prime_factors (of_nat n)
[PROOF STEP]
have "\<dots> = (\<Union>p\<in>prime_factors n. set (factor_gauss_int_prime_nat p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>p\<in>prime_factors n. prime_factors (of_nat p)) = (\<Union>p\<in>prime_factors n. set (factor_gauss_int_prime_nat p))
[PROOF STEP]
by (intro SUP_cong refl factor_gauss_int_prime_nat_correct [symmetric]) auto
[PROOF STATE]
proof (state)
this:
(\<Union>p\<in>prime_factors n. prime_factors (of_nat p)) = (\<Union>p\<in>prime_factors n. set (factor_gauss_int_prime_nat p))

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> prime_factors_gauss_int_of_nat n = prime_factors (of_nat n)
 2. n \<noteq> 0 \<Longrightarrow> prime_factors_gauss_int_of_nat n = prime_factors (of_nat n)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
prime_factors (of_nat n) = (\<Union>p\<in>prime_factors n. set (factor_gauss_int_prime_nat p))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
prime_factors (of_nat n) = (\<Union>p\<in>prime_factors n. set (factor_gauss_int_prime_nat p))

goal (1 subgoal):
 1. prime_factors_gauss_int_of_nat n = prime_factors (of_nat n)
[PROOF STEP]
by (simp add: prime_factors_gauss_int_of_nat_def)
[PROOF STATE]
proof (state)
this:
prime_factors_gauss_int_of_nat n = prime_factors (of_nat n)

goal (1 subgoal):
 1. n = 0 \<Longrightarrow> prime_factors_gauss_int_of_nat n = prime_factors (of_nat n)
[PROOF STEP]
qed (auto simp:  prime_factors_gauss_int_of_nat_def)


[STATEMENT]
lemma prime_factors_gauss_int_correct [code_unfold]: "prime_factors z = prime_factors_gauss_int z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime_factors z = prime_factors_gauss_int z
[PROOF STEP]
proof (cases "z = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. z = 0 \<Longrightarrow> prime_factors z = prime_factors_gauss_int z
 2. z \<noteq> 0 \<Longrightarrow> prime_factors z = prime_factors_gauss_int z
[PROOF STEP]
case [simp]: False
[PROOF STATE]
proof (state)
this:
z \<noteq> 0

goal (2 subgoals):
 1. z = 0 \<Longrightarrow> prime_factors z = prime_factors_gauss_int z
 2. z \<noteq> 0 \<Longrightarrow> prime_factors z = prime_factors_gauss_int z
[PROOF STEP]
define n where "n = gauss_int_norm z"
[PROOF STATE]
proof (state)
this:
n = gauss_int_norm z

goal (2 subgoals):
 1. z = 0 \<Longrightarrow> prime_factors z = prime_factors_gauss_int z
 2. z \<noteq> 0 \<Longrightarrow> prime_factors z = prime_factors_gauss_int z
[PROOF STEP]
from False
[PROOF STATE]
proof (chain)
picking this:
z \<noteq> 0
[PROOF STEP]
have [simp]: "n > 0"
[PROOF STATE]
proof (prove)
using this:
z \<noteq> 0

goal (1 subgoal):
 1. 0 < n
[PROOF STEP]
by (auto simp: n_def)
[PROOF STATE]
proof (state)
this:
0 < n

goal (2 subgoals):
 1. z = 0 \<Longrightarrow> prime_factors z = prime_factors_gauss_int z
 2. z \<noteq> 0 \<Longrightarrow> prime_factors z = prime_factors_gauss_int z
[PROOF STEP]
have "prime_factors_gauss_int z = Set.filter (\<lambda>p. p dvd z) (prime_factors (of_nat n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime_factors_gauss_int z = Set.filter (\<lambda>p. p dvd z) (prime_factors (of_nat n))
[PROOF STEP]
by (simp add: prime_factors_gauss_int_of_nat_correct prime_factors_gauss_int_def n_def)
[PROOF STATE]
proof (state)
this:
prime_factors_gauss_int z = Set.filter (\<lambda>p. p dvd z) (prime_factors (of_nat n))

goal (2 subgoals):
 1. z = 0 \<Longrightarrow> prime_factors z = prime_factors_gauss_int z
 2. z \<noteq> 0 \<Longrightarrow> prime_factors z = prime_factors_gauss_int z
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
prime_factors_gauss_int z = Set.filter (\<lambda>p. p dvd z) (prime_factors (of_nat n))

goal (2 subgoals):
 1. z = 0 \<Longrightarrow> prime_factors z = prime_factors_gauss_int z
 2. z \<noteq> 0 \<Longrightarrow> prime_factors z = prime_factors_gauss_int z
[PROOF STEP]
have "of_nat n = z * gauss_cnj z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_nat n = z * gauss_cnj z
[PROOF STEP]
by (simp add: n_def self_mult_gauss_cnj)
[PROOF STATE]
proof (state)
this:
of_nat n = z * gauss_cnj z

goal (2 subgoals):
 1. z = 0 \<Longrightarrow> prime_factors z = prime_factors_gauss_int z
 2. z \<noteq> 0 \<Longrightarrow> prime_factors z = prime_factors_gauss_int z
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
of_nat n = z * gauss_cnj z

goal (2 subgoals):
 1. z = 0 \<Longrightarrow> prime_factors z = prime_factors_gauss_int z
 2. z \<noteq> 0 \<Longrightarrow> prime_factors z = prime_factors_gauss_int z
[PROOF STEP]
have "prime_factors \<dots> = prime_factors z \<union> prime_factors (gauss_cnj z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime_factors (z * gauss_cnj z) = prime_factors z \<union> prime_factors (gauss_cnj z)
[PROOF STEP]
by (subst prime_factors_product) auto
[PROOF STATE]
proof (state)
this:
prime_factors (z * gauss_cnj z) = prime_factors z \<union> prime_factors (gauss_cnj z)

goal (2 subgoals):
 1. z = 0 \<Longrightarrow> prime_factors z = prime_factors_gauss_int z
 2. z \<noteq> 0 \<Longrightarrow> prime_factors z = prime_factors_gauss_int z
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
prime_factors (z * gauss_cnj z) = prime_factors z \<union> prime_factors (gauss_cnj z)

goal (2 subgoals):
 1. z = 0 \<Longrightarrow> prime_factors z = prime_factors_gauss_int z
 2. z \<noteq> 0 \<Longrightarrow> prime_factors z = prime_factors_gauss_int z
[PROOF STEP]
have "Set.filter (\<lambda>p. p dvd z) \<dots> = prime_factors z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Set.filter (\<lambda>p. p dvd z) (prime_factors z \<union> prime_factors (gauss_cnj z)) = prime_factors z
[PROOF STEP]
by (auto simp: in_prime_factors_iff)
[PROOF STATE]
proof (state)
this:
Set.filter (\<lambda>p. p dvd z) (prime_factors z \<union> prime_factors (gauss_cnj z)) = prime_factors z

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

goal (1 subgoal):
 1. prime_factors z = prime_factors_gauss_int z
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
prime_factors z = prime_factors_gauss_int z

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


[STATEMENT]
lemma card_union': "(finite s) \<and> (finite t) \<and> (disjnt s t) \<Longrightarrow> (card (s \<union> t) = card s + card t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite s \<and> finite t \<and> disjnt s t \<Longrightarrow> card (s \<union> t) = card s + card t
[PROOF STEP]
by (simp add: card_Un_disjoint disjnt_def)


[STATEMENT]
lemma CARD_INJ_IMAGE_2:
  fixes f s
  assumes "finite s" "(\<forall>x y. ((x \<in> s) \<and> (y \<in> s)) \<longrightarrow> ((f x = f y) \<longleftrightarrow> (x = y)))"
  shows "(card (f ` s) = card s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (f ` s) = card s
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card (f ` s) = card s
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card (f ` s) = card s
[PROOF STEP]
fix x y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card (f ` s) = card s
[PROOF STEP]
assume "x \<in> s" "y \<in> s"
[PROOF STATE]
proof (state)
this:
x \<in> s
y \<in> s

goal (1 subgoal):
 1. card (f ` s) = card s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> s
y \<in> s
[PROOF STEP]
have "f x = f y \<longrightarrow> x = y"
[PROOF STATE]
proof (prove)
using this:
x \<in> s
y \<in> s

goal (1 subgoal):
 1. f x = f y \<longrightarrow> x = y
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
x \<in> s
y \<in> s
\<forall>x y. x \<in> s \<and> y \<in> s \<longrightarrow> (f x = f y) = (x = y)

goal (1 subgoal):
 1. f x = f y \<longrightarrow> x = y
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f x = f y \<longrightarrow> x = y

goal (1 subgoal):
 1. card (f ` s) = card s
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x2 \<in> s; ?y2 \<in> s\<rbrakk> \<Longrightarrow> f ?x2 = f ?y2 \<longrightarrow> ?x2 = ?y2

goal (1 subgoal):
 1. card (f ` s) = card s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?x2 \<in> s; ?y2 \<in> s\<rbrakk> \<Longrightarrow> f ?x2 = f ?y2 \<longrightarrow> ?x2 = ?y2
[PROOF STEP]
have "inj_on f s"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x2 \<in> s; ?y2 \<in> s\<rbrakk> \<Longrightarrow> f ?x2 = f ?y2 \<longrightarrow> ?x2 = ?y2

goal (1 subgoal):
 1. inj_on f s
[PROOF STEP]
by (simp add: inj_onI)
[PROOF STATE]
proof (state)
this:
inj_on f s

goal (1 subgoal):
 1. card (f ` s) = card s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
inj_on f s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
inj_on f s

goal (1 subgoal):
 1. card (f ` s) = card s
[PROOF STEP]
using assms(1) inj_on_iff_eq_card
[PROOF STATE]
proof (prove)
using this:
inj_on f s
finite s
finite ?A \<Longrightarrow> inj_on ?f ?A = (card (?f ` ?A) = card ?A)

goal (1 subgoal):
 1. card (f ` s) = card s
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
card (f ` s) = card s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma scc_main_lemma_x: "\<And>s t x. (x \<in> s) \<and> \<not>(x \<in> t) \<Longrightarrow> \<not>(s = t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s t x. x \<in> s \<and> x \<notin> t \<Longrightarrow> s \<noteq> t
[PROOF STEP]
by blast


[STATEMENT]
lemma neq_funs_neq_images:
  fixes s
  assumes "\<forall>x. x \<in> s \<longrightarrow> (\<forall>y. y \<in> s \<longrightarrow> f1 x \<noteq> f2 y)" "\<exists>x. x \<in> s"
  shows "f1 ` s \<noteq> f2 ` s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f1 ` s \<noteq> f2 ` s
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>x. x \<in> s \<longrightarrow> (\<forall>y. y \<in> s \<longrightarrow> f1 x \<noteq> f2 y)
\<exists>x. x \<in> s

goal (1 subgoal):
 1. f1 ` s \<noteq> f2 ` s
[PROOF STEP]
by blast


[STATEMENT]
lemma mems_le_finite_i:
  fixes s :: "nat set" and k :: nat
  shows "(\<forall> x. x \<in> s \<longrightarrow> x \<le> k) \<Longrightarrow> finite s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. x \<in> s \<longrightarrow> x \<le> k \<Longrightarrow> finite s
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>x. x \<in> s \<longrightarrow> x \<le> k \<Longrightarrow> finite s
[PROOF STEP]
assume P: "(\<forall> x. x \<in> s \<longrightarrow> x \<le> k)"
[PROOF STATE]
proof (state)
this:
\<forall>x. x \<in> s \<longrightarrow> x \<le> k

goal (1 subgoal):
 1. \<forall>x. x \<in> s \<longrightarrow> x \<le> k \<Longrightarrow> finite s
[PROOF STEP]
let ?f = "id :: nat \<Rightarrow> nat"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>x. x \<in> s \<longrightarrow> x \<le> k \<Longrightarrow> finite s
[PROOF STEP]
let ?S = "{i. i \<le> k}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>x. x \<in> s \<longrightarrow> x \<le> k \<Longrightarrow> finite s
[PROOF STEP]
have "s \<subseteq> ?S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<subseteq> {i. i \<le> k}
[PROOF STEP]
using P
[PROOF STATE]
proof (prove)
using this:
\<forall>x. x \<in> s \<longrightarrow> x \<le> k

goal (1 subgoal):
 1. s \<subseteq> {i. i \<le> k}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
s \<subseteq> {i. i \<le> k}

goal (1 subgoal):
 1. \<forall>x. x \<in> s \<longrightarrow> x \<le> k \<Longrightarrow> finite s
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
s \<subseteq> {i. i \<le> k}

goal (1 subgoal):
 1. \<forall>x. x \<in> s \<longrightarrow> x \<le> k \<Longrightarrow> finite s
[PROOF STEP]
have "?f ` ?S = ?S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. id ` {i. i \<le> k} = {i. i \<le> k}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
id ` {i. i \<le> k} = {i. i \<le> k}

goal (1 subgoal):
 1. \<forall>x. x \<in> s \<longrightarrow> x \<le> k \<Longrightarrow> finite s
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
id ` {i. i \<le> k} = {i. i \<le> k}

goal (1 subgoal):
 1. \<forall>x. x \<in> s \<longrightarrow> x \<le> k \<Longrightarrow> finite s
[PROOF STEP]
have "finite ?S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {i. i \<le> k}
[PROOF STEP]
using nat_seg_image_imp_finite
[PROOF STATE]
proof (prove)
using this:
?A = ?f ` {i. i < ?n} \<Longrightarrow> finite ?A

goal (1 subgoal):
 1. finite {i. i \<le> k}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite {i. i \<le> k}

goal (1 subgoal):
 1. \<forall>x. x \<in> s \<longrightarrow> x \<le> k \<Longrightarrow> finite s
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite {i. i \<le> k}

goal (1 subgoal):
 1. \<forall>x. x \<in> s \<longrightarrow> x \<le> k \<Longrightarrow> finite s
[PROOF STEP]
have "finite s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite s
[PROOF STEP]
using calculation finite_subset
[PROOF STATE]
proof (prove)
using this:
s \<subseteq> {i. i \<le> k}
id ` {i. i \<le> k} = {i. i \<le> k}
finite {i. i \<le> k}
\<lbrakk>?A \<subseteq> ?B; finite ?B\<rbrakk> \<Longrightarrow> finite ?A

goal (1 subgoal):
 1. finite s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite s

goal (1 subgoal):
 1. \<forall>x. x \<in> s \<longrightarrow> x \<le> k \<Longrightarrow> finite s
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
s \<subseteq> {i. i \<le> k}
id ` {i. i \<le> k} = {i. i \<le> k}
finite {i. i \<le> k}
finite s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
s \<subseteq> {i. i \<le> k}
id ` {i. i \<le> k} = {i. i \<le> k}
finite {i. i \<le> k}
finite s

goal (1 subgoal):
 1. finite s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mems_le_finite:
  fixes s :: "nat set" and k :: nat
  shows "\<And>(s :: nat set) k. (\<forall> x. x \<in> s \<longrightarrow> x \<le> k) \<Longrightarrow> finite s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s k. \<forall>x. x \<in> s \<longrightarrow> x \<le> k \<Longrightarrow> finite s
[PROOF STEP]
using mems_le_finite_i
[PROOF STATE]
proof (prove)
using this:
\<forall>x. x \<in> ?s \<longrightarrow> x \<le> ?k \<Longrightarrow> finite ?s

goal (1 subgoal):
 1. \<And>s k. \<forall>x. x \<in> s \<longrightarrow> x \<le> k \<Longrightarrow> finite s
[PROOF STEP]
by auto

\<comment> \<open>NOTE translated `s` to `nat set` (more generality wasn't required.).\<close>


[STATEMENT]
lemma mem_le_imp_MIN_le:
  fixes s :: "nat set" and k :: nat
  assumes "\<exists>x. (x \<in> s) \<and> (x \<le> k)"
  shows "(Inf s \<le> k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Inf s \<le> k
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Inf s \<le> k
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<exists>x. x \<in> s \<and> x \<le> k
[PROOF STEP]
obtain x where 1: "x \<in> s" "x \<le> k"
[PROOF STATE]
proof (prove)
using this:
\<exists>x. x \<in> s \<and> x \<le> k

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> s; x \<le> k\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> s
x \<le> k

goal (1 subgoal):
 1. Inf s \<le> k
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
x \<in> s
x \<le> k

goal (1 subgoal):
 1. Inf s \<le> k
[PROOF STEP]
assume C: "Inf s > k"
[PROOF STATE]
proof (state)
this:
k < Inf s

goal (1 subgoal):
 1. Inf s \<le> k
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k < Inf s
[PROOF STEP]
have "Inf s > x"
[PROOF STATE]
proof (prove)
using this:
k < Inf s

goal (1 subgoal):
 1. x < Inf s
[PROOF STEP]
using 1(2)
[PROOF STATE]
proof (prove)
using this:
k < Inf s
x \<le> k

goal (1 subgoal):
 1. x < Inf s
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
x < Inf s

goal (1 subgoal):
 1. Inf s \<le> k
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x < Inf s
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
x < Inf s

goal (1 subgoal):
 1. False
[PROOF STEP]
using 1(1) cInf_lower leD
[PROOF STATE]
proof (prove)
using this:
x < Inf s
x \<in> s
\<lbrakk>?x \<in> ?X; bdd_below ?X\<rbrakk> \<Longrightarrow> Inf ?X \<le> ?x
?y \<le> ?x \<Longrightarrow> \<not> ?x < ?y

goal (1 subgoal):
 1. False
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. Inf s \<le> k
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
k < Inf s \<Longrightarrow> False

goal (1 subgoal):
 1. Inf s \<le> k
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k < Inf s \<Longrightarrow> False
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
k < Inf s \<Longrightarrow> False

goal (1 subgoal):
 1. Inf s \<le> k
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
Inf s \<le> k

goal:
No subgoals!
[PROOF STEP]
qed

\<comment> \<open>NOTE
  nat --> bool is the type of a HOL4 set and was translated to 'nat set'.\<close>
\<comment> \<open>NOTE
  We cannot use 'Min' instead of 'Inf' because there is no indication that '{n. s n}' will be
finite. Without that @{term "Min {n. s n} \<in> {n. s n}"} is not necessarily true.\<close>


[STATEMENT]
lemma mem_lt_imp_MIN_lt:
  fixes s :: "nat set" and k :: nat
  assumes "(\<exists>x. x \<in> s \<and> x < k)"
  shows "(Inf s) < k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Inf s < k
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Inf s < k
[PROOF STEP]
obtain x where 1: "x \<in> s" "x < k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> s; x < k\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<exists>x. x \<in> s \<and> x < k

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> s; x < k\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> s
x < k

goal (1 subgoal):
 1. Inf s < k
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> s
x < k
[PROOF STEP]
have 2: "s \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
x \<in> s
x < k

goal (1 subgoal):
 1. s \<noteq> {}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
s \<noteq> {}

goal (1 subgoal):
 1. Inf s < k
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s \<noteq> {}
[PROOF STEP]
have "Inf s \<in> s"
[PROOF STATE]
proof (prove)
using this:
s \<noteq> {}

goal (1 subgoal):
 1. Inf s \<in> s
[PROOF STEP]
using Inf_nat_def LeastI
[PROOF STATE]
proof (prove)
using this:
s \<noteq> {}
Inf ?X = (LEAST n. n \<in> ?X)
?P ?k \<Longrightarrow> ?P (LEAST x. ?P x)

goal (1 subgoal):
 1. Inf s \<in> s
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
Inf s \<in> s

goal (1 subgoal):
 1. Inf s < k
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Inf s \<in> s

goal (1 subgoal):
 1. Inf s < k
[PROOF STEP]
have "\<forall>x\<in>s. Inf s \<le> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>s. Inf s \<le> x
[PROOF STEP]
by (simp add: cInf_lower)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>s. Inf s \<le> x

goal (1 subgoal):
 1. Inf s < k
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Inf s \<in> s
\<forall>x\<in>s. Inf s \<le> x
[PROOF STEP]
show "(Inf s) < k"
[PROOF STATE]
proof (prove)
using this:
Inf s \<in> s
\<forall>x\<in>s. Inf s \<le> x

goal (1 subgoal):
 1. Inf s < k
[PROOF STEP]
using assms leD
[PROOF STATE]
proof (prove)
using this:
Inf s \<in> s
\<forall>x\<in>s. Inf s \<le> x
\<exists>x. x \<in> s \<and> x < k
?y \<le> ?x \<Longrightarrow> \<not> ?x < ?y

goal (1 subgoal):
 1. Inf s < k
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
Inf s < k

goal:
No subgoals!
[PROOF STEP]
qed

\<comment> \<open>NOTE type for 'k' had to be fixed (type unordered error; also not true for e.g. real sets).\<close>


[STATEMENT]
lemma bound_child_parent_neq_mems_state_set_neq_len:
  fixes s and k :: nat
  assumes "(\<forall>x. x \<in> s \<longrightarrow> x < k)"
  shows "finite s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite s
[PROOF STEP]
using assms bounded_nat_set_is_finite
[PROOF STATE]
proof (prove)
using this:
\<forall>x. x \<in> s \<longrightarrow> x < k
\<forall>i\<in>?N. i < ?n \<Longrightarrow> finite ?N

goal (1 subgoal):
 1. finite s
[PROOF STEP]
by blast


[STATEMENT]
lemma bound_main_lemma_2: "\<And>(s :: nat set) k. (s \<noteq> {}) \<and> (\<forall>x. x \<in> s \<longrightarrow> x \<le> k) \<Longrightarrow> Sup s \<le> k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s k. s \<noteq> {} \<and> (\<forall>x. x \<in> s \<longrightarrow> x \<le> k) \<Longrightarrow> Sup s \<le> k
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s k. s \<noteq> {} \<and> (\<forall>x. x \<in> s \<longrightarrow> x \<le> k) \<Longrightarrow> Sup s \<le> k
[PROOF STEP]
fix s :: "nat set" and k
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s k. s \<noteq> {} \<and> (\<forall>x. x \<in> s \<longrightarrow> x \<le> k) \<Longrightarrow> Sup s \<le> k
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s k. s \<noteq> {} \<and> (\<forall>x. x \<in> s \<longrightarrow> x \<le> k) \<Longrightarrow> Sup s \<le> k
[PROOF STEP]
assume P1: "s \<noteq> {}"
[PROOF STATE]
proof (state)
this:
s \<noteq> {}

goal (1 subgoal):
 1. \<And>s k. s \<noteq> {} \<and> (\<forall>x. x \<in> s \<longrightarrow> x \<le> k) \<Longrightarrow> Sup s \<le> k
[PROOF STEP]
assume P2: "(\<forall>x. x \<in> s \<longrightarrow> x \<le> k)"
[PROOF STATE]
proof (state)
this:
\<forall>x. x \<in> s \<longrightarrow> x \<le> k

goal (1 subgoal):
 1. \<And>s k. s \<noteq> {} \<and> (\<forall>x. x \<in> s \<longrightarrow> x \<le> k) \<Longrightarrow> Sup s \<le> k
[PROOF STEP]
have "finite s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite s
[PROOF STEP]
using P2 mems_le_finite
[PROOF STATE]
proof (prove)
using this:
\<forall>x. x \<in> s \<longrightarrow> x \<le> k
\<forall>x. x \<in> ?s \<longrightarrow> x \<le> ?k \<Longrightarrow> finite ?s

goal (1 subgoal):
 1. finite s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite s

goal (1 subgoal):
 1. \<And>s k. s \<noteq> {} \<and> (\<forall>x. x \<in> s \<longrightarrow> x \<le> k) \<Longrightarrow> Sup s \<le> k
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite s

goal (1 subgoal):
 1. \<And>s k. s \<noteq> {} \<and> (\<forall>x. x \<in> s \<longrightarrow> x \<le> k) \<Longrightarrow> Sup s \<le> k
[PROOF STEP]
have "Max s \<in> s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Max s \<in> s
[PROOF STEP]
using P1 calculation Max_in
[PROOF STATE]
proof (prove)
using this:
s \<noteq> {}
finite s
\<lbrakk>finite ?A; ?A \<noteq> {}\<rbrakk> \<Longrightarrow> Max ?A \<in> ?A

goal (1 subgoal):
 1. Max s \<in> s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Max s \<in> s

goal (1 subgoal):
 1. \<And>s k. s \<noteq> {} \<and> (\<forall>x. x \<in> s \<longrightarrow> x \<le> k) \<Longrightarrow> Sup s \<le> k
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Max s \<in> s

goal (1 subgoal):
 1. \<And>s k. s \<noteq> {} \<and> (\<forall>x. x \<in> s \<longrightarrow> x \<le> k) \<Longrightarrow> Sup s \<le> k
[PROOF STEP]
have "Max s \<le> k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Max s \<le> k
[PROOF STEP]
using P2 calculation
[PROOF STATE]
proof (prove)
using this:
\<forall>x. x \<in> s \<longrightarrow> x \<le> k
finite s
Max s \<in> s

goal (1 subgoal):
 1. Max s \<le> k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Max s \<le> k

goal (1 subgoal):
 1. \<And>s k. s \<noteq> {} \<and> (\<forall>x. x \<in> s \<longrightarrow> x \<le> k) \<Longrightarrow> Sup s \<le> k
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>s \<noteq> {}; \<forall>x. x \<in> s \<longrightarrow> x \<le> k\<rbrakk> \<Longrightarrow> Max s \<le> k

goal (1 subgoal):
 1. \<And>s k. s \<noteq> {} \<and> (\<forall>x. x \<in> s \<longrightarrow> x \<le> k) \<Longrightarrow> Sup s \<le> k
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>s \<noteq> {}; \<forall>x. x \<in> s \<longrightarrow> x \<le> k\<rbrakk> \<Longrightarrow> Max s \<le> k
[PROOF STEP]
show "(s \<noteq> {}) \<and> (\<forall>x. x \<in> s \<longrightarrow> x \<le> k) \<Longrightarrow> Sup s \<le> k"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>s \<noteq> {}; \<forall>x. x \<in> s \<longrightarrow> x \<le> k\<rbrakk> \<Longrightarrow> Max s \<le> k

goal (1 subgoal):
 1. s \<noteq> {} \<and> (\<forall>x. x \<in> s \<longrightarrow> x \<le> k) \<Longrightarrow> Sup s \<le> k
[PROOF STEP]
by (simp add: Sup_nat_def)
[PROOF STATE]
proof (state)
this:
s \<noteq> {} \<and> (\<forall>x. x \<in> s \<longrightarrow> x \<le> k) \<Longrightarrow> Sup s \<le> k

goal:
No subgoals!
[PROOF STEP]
qed

\<comment> \<open>NOTE type of 'k' fixed to nat to be able to use 'bound\_child\_parent\_neq\_mems\_state\_set\_neq\_len'.\<close>


[STATEMENT]
lemma bound_child_parent_not_eq_last_diff_paths: "\<And>s (k :: nat).
  (s \<noteq> {})
  \<Longrightarrow> (\<forall>x. x \<in> s \<longrightarrow> x < k)
  \<Longrightarrow> Sup s < k
"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s k. \<lbrakk>s \<noteq> {}; \<forall>x. x \<in> s \<longrightarrow> x < k\<rbrakk> \<Longrightarrow> Sup s < k
[PROOF STEP]
by (simp add: Sup_nat_def bound_child_parent_neq_mems_state_set_neq_len)