author eberlm Fri Jul 22 17:35:54 2016 +0200 (2016-07-22) changeset 63537 831816778409 parent 63536 8cecf0100996 child 63538 d7b5e2a222c2
Removed redundant material related to primes
 src/HOL/Algebra/Exponent.thy file | annotate | diff | revisions src/HOL/Algebra/Sylow.thy file | annotate | diff | revisions src/HOL/Nonstandard_Analysis/Examples/NSPrimes.thy file | annotate | diff | revisions src/HOL/Number_Theory/Factorial_Ring.thy file | annotate | diff | revisions src/HOL/Number_Theory/Residues.thy file | annotate | diff | revisions src/HOL/Number_Theory/UniqueFactorization.thy file | annotate | diff | revisions src/HOL/Proofs/Extraction/Euclid.thy file | annotate | diff | revisions src/HOL/ROOT file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Algebra/Exponent.thy	Fri Jul 22 15:39:32 2016 +0200
1.2 +++ b/src/HOL/Algebra/Exponent.thy	Fri Jul 22 17:35:54 2016 +0200
1.3 @@ -13,183 +13,16 @@
1.4
1.5  text \<open>The Combinatorial Argument Underlying the First Sylow Theorem\<close>
1.6
1.7 -
1.8 -subsection\<open>Prime Theorems\<close>
1.9 -
1.10 -lemma prime_dvd_cases:
1.11 -  assumes pk: "p*k dvd m*n" and p: "prime p"
1.12 -  shows "(\<exists>x. k dvd x*n \<and> m = p*x) \<or> (\<exists>y. k dvd m*y \<and> n = p*y)"
1.13 -proof -
1.14 -  have "p dvd m*n" using dvd_mult_left pk by blast
1.15 -  then consider "p dvd m" | "p dvd n"
1.16 -    using p is_prime_dvd_mult_iff by blast
1.17 -  then show ?thesis
1.18 -  proof cases
1.19 -    case 1 then obtain a where "m = p * a" by (metis dvd_mult_div_cancel)
1.20 -      then have "\<exists>x. k dvd x * n \<and> m = p * x"
1.21 -        using p pk by (auto simp: mult.assoc)
1.22 -    then show ?thesis ..
1.23 -  next
1.24 -    case 2 then obtain b where "n = p * b" by (metis dvd_mult_div_cancel)
1.25 -    with p pk have "\<exists>y. k dvd m*y \<and> n = p*y"
1.26 -      by (metis dvd_mult_right dvd_times_left_cancel_iff mult.left_commute mult_zero_left)
1.27 -    then show ?thesis ..
1.28 -  qed
1.29 -qed
1.30 -
1.31 -lemma prime_power_dvd_prod:
1.32 -  assumes pc: "p^c dvd m*n" and p: "prime p"
1.33 -  shows "\<exists>a b. a+b = c \<and> p^a dvd m \<and> p^b dvd n"
1.34 -using pc
1.35 -proof (induct c arbitrary: m n)
1.36 -  case 0 show ?case by simp
1.37 -next
1.38 -  case (Suc c)
1.39 -  consider x where "p^c dvd x*n" "m = p*x" | y where "p^c dvd m*y" "n = p*y"
1.40 -    using prime_dvd_cases [of _ "p^c", OF _ p] Suc.prems by force
1.41 -  then show ?case
1.42 -  proof cases
1.43 -    case (1 x)
1.44 -    with Suc.hyps[of x n] obtain a b where "a + b = c \<and> p ^ a dvd x \<and> p ^ b dvd n" by blast
1.45 -    with 1 have "Suc a + b = Suc c \<and> p ^ Suc a dvd m \<and> p ^ b dvd n"
1.46 -      by (auto intro: mult_dvd_mono)
1.47 -    thus ?thesis by blast
1.48 -  next
1.49 -    case (2 y)
1.50 -    with Suc.hyps[of m y] obtain a b where "a + b = c \<and> p ^ a dvd m \<and> p ^ b dvd y" by blast
1.51 -    with 2 have "a + Suc b = Suc c \<and> p ^ a dvd m \<and> p ^ Suc b dvd n"
1.52 -      by (auto intro: mult_dvd_mono)
1.53 -    with Suc.hyps [of m y] show "\<exists>a b. a + b = Suc c \<and> p ^ a dvd m \<and> p ^ b dvd n"
1.54 -      by force
1.55 -  qed
1.56 -qed
1.57 -
1.58 -lemma add_eq_Suc_lem: "a+b = Suc (x+y) \<Longrightarrow> a \<le> x \<or> b \<le> y"
1.59 -  by arith
1.60 -
1.61 -lemma prime_power_dvd_cases:
1.62 -     "\<lbrakk>p^c dvd m * n; a + b = Suc c; prime p\<rbrakk> \<Longrightarrow> p ^ a dvd m \<or> p ^ b dvd n"
1.63 -  using power_le_dvd prime_power_dvd_prod by (blast dest: prime_power_dvd_prod add_eq_Suc_lem)
1.64 -
1.65  text\<open>needed in this form to prove Sylow's theorem\<close>
1.66 -corollary div_combine: "\<lbrakk>prime p; \<not> p ^ Suc r dvd n; p ^ (a + r) dvd n * k\<rbrakk> \<Longrightarrow> p ^ a dvd k"
1.67 +corollary (in algebraic_semidom) div_combine:
1.68 +  "\<lbrakk>is_prime_elem p; \<not> p ^ Suc r dvd n; p ^ (a + r) dvd n * k\<rbrakk> \<Longrightarrow> p ^ a dvd k"
1.69    by (metis add_Suc_right mult.commute prime_power_dvd_cases)
1.70
1.71 -
1.72 -subsection\<open>The Exponent Function\<close>
1.73 -
1.74 -abbreviation (input) "exponent \<equiv> multiplicity"
1.75 -
1.76 -(*
1.77 -definition
1.78 -  exponent :: "nat => nat => nat"
1.79 -  where "exponent p s = (if prime p then (GREATEST r. p^r dvd s) else 0)"
1.80 -*)
1.81 -
1.82 -(*lemma exponent_eq_0 [simp]: "\<not> prime p \<Longrightarrow> exponent p s = 0"
1.83 -  by (simp add: exponent_def)*)
1.84 -
1.85 -lemma Suc_le_power: "Suc 0 < p \<Longrightarrow> Suc n \<le> p ^ n"
1.86 -  by (induct n) (auto simp: Suc_le_eq le_less_trans)
1.87 -
1.88 -(*
1.89 -text\<open>An upper bound for the @{term n} such that @{term"p^n dvd a"}: needed for GREATEST to exist\<close>
1.90 -lemma power_dvd_bound: "\<lbrakk>p ^ n dvd a; Suc 0 < p; 0 < a\<rbrakk> \<Longrightarrow> n < a"
1.91 -  by (meson Suc_le_lessD Suc_le_power dvd_imp_le le_trans)
1.92 -*)
1.93 -
1.94 -(*
1.95 -lemma exponent_ge:
1.96 -  assumes "p ^ k dvd n" "prime p" "0 < n"
1.97 -    shows "k \<le> exponent p n"
1.98 -proof -
1.99 -  have "Suc 0 < p"
1.100 -    using \<open>prime p\<close> by (simp add: prime_def)
1.101 -  with assms show ?thesis
1.102 -    by (simp add: \<open>prime p\<close> exponent_def) (meson Greatest_le power_dvd_bound)
1.103 -qed
1.104 -*)
1.105 -
1.106 -(*
1.107 -lemma power_exponent_dvd: "p ^ exponent p s dvd s"
1.108 -proof (cases "s = 0")
1.109 -  case True then show ?thesis by simp
1.110 -next
1.111 -  case False then show ?thesis
1.112 -    apply (simp add: exponent_def, clarify)
1.113 -    apply (rule GreatestI [where k = 0])
1.114 -    apply (auto dest: prime_gt_Suc_0_nat power_dvd_bound)
1.115 -    done
1.116 -qed
1.117 -*)
1.118 -
1.119 -(*lemma power_Suc_exponent_Not_dvd:
1.120 -    "\<lbrakk>p * p ^ exponent p s dvd s; prime p\<rbrakk> \<Longrightarrow> s = 0"
1.121 -  by (metis exponent_ge neq0_conv not_less_eq_eq order_refl power_Suc)
1.122 -*)
1.123 -
1.124 -
1.125 -(*
1.126 -lemma exponent_power_eq [simp]: "prime p \<Longrightarrow> exponent p (p ^ a) = a"
1.127 -  apply (simp add: exponent_def)
1.128 -  apply (rule Greatest_equality, simp)
1.129 -  apply (simp add: prime_gt_Suc_0_nat power_dvd_imp_le)
1.130 -  done
1.131 -*)
1.132 -
1.133 -(*
1.134 -lemma exponent_1_eq_0 [simp]: "exponent p (Suc 0) = 0"
1.135 -  apply (case_tac "prime p")
1.136 -  apply (metis exponent_power_eq nat_power_eq_Suc_0_iff)
1.137 -  apply simp
1.138 -  done
1.139 -*)
1.140 -
1.141 -lemma exponent_equalityI:
1.142 -  "(\<And>r. p ^ r dvd a \<longleftrightarrow> p ^ r dvd b) \<Longrightarrow> exponent p a = exponent p b"
1.143 -  by (simp add: multiplicity_def)
1.144 -
1.145 -(*
1.147 -  assumes "a > 0" "b > 0"
1.148 -    shows "exponent p (a * b) = (exponent p a) + (exponent p b)"
1.149 -proof (cases "prime p")
1.150 -  case False then show ?thesis by simp
1.151 -next
1.152 -  case True show ?thesis
1.153 -  proof (rule order_antisym)
1.154 -    show "exponent p a + exponent p b \<le> exponent p (a * b)"
1.155 -      by (rule exponent_ge) (auto simp: mult_dvd_mono power_add power_exponent_dvd \<open>prime p\<close> assms)
1.156 -  next
1.157 -    { assume "exponent p a + exponent p b < exponent p (a * b)"
1.158 -      then have "p ^ (Suc (exponent p a + exponent p b)) dvd a * b"
1.159 -        by (meson Suc_le_eq power_exponent_dvd power_le_dvd)
1.160 -      with prime_power_dvd_cases [where  a = "Suc (exponent p a)" and b = "Suc (exponent p b)"]
1.161 -      have False
1.163 -    }
1.164 -  then show "exponent p (a * b) \<le> exponent p a + exponent p b" by (blast intro: leI)
1.165 -  qed
1.166 -qed
1.167 -*)
1.168 -
1.169 -lemma not_dvd_imp_multiplicity_0:
1.170 -  assumes "\<not>p dvd x"
1.171 -  shows   "multiplicity p x = 0"
1.172 -proof -
1.173 -  from assms have "multiplicity p x < 1"
1.174 -    by (intro multiplicity_lessI) auto
1.175 -  thus ?thesis by simp
1.176 -qed
1.177 -
1.178 -
1.179 -subsection\<open>The Main Combinatorial Argument\<close>
1.180 -
1.181  lemma exponent_p_a_m_k_equation:
1.182    fixes p :: nat
1.183    assumes "0 < m" "0 < k" "p \<noteq> 0" "k < p^a"
1.184 -    shows "exponent p (p^a * m - k) = exponent p (p^a - k)"
1.185 -proof (rule exponent_equalityI [OF iffI])
1.186 +    shows "multiplicity p (p^a * m - k) = multiplicity p (p^a - k)"
1.187 +proof (rule multiplicity_cong [OF iffI])
1.188    fix r
1.189    assume *: "p ^ r dvd p ^ a * m - k"
1.190    show "p ^ r dvd p ^ a - k"
1.191 @@ -218,16 +51,16 @@
1.192
1.193  lemma p_not_div_choose_lemma:
1.194    fixes p :: nat
1.195 -  assumes eeq: "\<And>i. Suc i < K \<Longrightarrow> exponent p (Suc i) = exponent p (Suc (j + i))"
1.196 +  assumes eeq: "\<And>i. Suc i < K \<Longrightarrow> multiplicity p (Suc i) = multiplicity p (Suc (j + i))"
1.197        and "k < K" and p: "prime p"
1.198 -    shows "exponent p (j + k choose k) = 0"
1.199 +    shows "multiplicity p (j + k choose k) = 0"
1.200    using \<open>k < K\<close>
1.201  proof (induction k)
1.202    case 0 then show ?case by simp
1.203  next
1.204    case (Suc k)
1.205    then have *: "(Suc (j+k) choose Suc k) > 0" by simp
1.206 -  then have "exponent p ((Suc (j+k) choose Suc k) * Suc k) = exponent p (Suc k)"
1.207 +  then have "multiplicity p ((Suc (j+k) choose Suc k) * Suc k) = multiplicity p (Suc k)"
1.208      by (subst Suc_times_binomial_eq [symmetric], subst prime_multiplicity_mult_distrib)
1.209         (insert p Suc.prems, simp_all add: eeq [symmetric] Suc.IH)
1.210    with p * show ?case
1.211 @@ -237,8 +70,8 @@
1.212  text\<open>The lemma above, with two changes of variables\<close>
1.213  lemma p_not_div_choose:
1.214    assumes "k < K" and "k \<le> n"
1.215 -      and eeq: "\<And>j. \<lbrakk>0<j; j<K\<rbrakk> \<Longrightarrow> exponent p (n - k + (K - j)) = exponent p (K - j)" "is_prime p"
1.216 -    shows "exponent p (n choose k) = 0"
1.217 +      and eeq: "\<And>j. \<lbrakk>0<j; j<K\<rbrakk> \<Longrightarrow> multiplicity p (n - k + (K - j)) = multiplicity p (K - j)" "is_prime p"
1.218 +    shows "multiplicity p (n choose k) = 0"
1.219  apply (rule p_not_div_choose_lemma [of K p "n-k" k, simplified assms nat_minus_add_max max_absorb1])
1.220  apply (metis add_Suc_right eeq diff_diff_cancel order_less_imp_le zero_less_Suc zero_less_diff)
1.221  apply (rule TrueI)+
1.222 @@ -246,14 +79,14 @@
1.223
1.224  proposition const_p_fac:
1.225    assumes "m>0" and prime: "is_prime p"
1.226 -  shows "exponent p (p^a * m choose p^a) = exponent p m"
1.227 +  shows "multiplicity p (p^a * m choose p^a) = multiplicity p m"
1.228  proof-
1.229    from assms have p: "0 < p ^ a" "0 < p^a * m" "p^a \<le> p^a * m"
1.230      by (auto simp: prime_gt_0_nat)
1.231 -  have *: "exponent p ((p^a * m - 1) choose (p^a - 1)) = 0"
1.232 +  have *: "multiplicity p ((p^a * m - 1) choose (p^a - 1)) = 0"
1.233      apply (rule p_not_div_choose [where K = "p^a"])
1.234      using p exponent_p_a_m_k_equation by (auto simp: diff_le_mono prime)
1.235 -  have "exponent p ((p ^ a * m choose p ^ a) * p ^ a) = a + exponent p m"
1.236 +  have "multiplicity p ((p ^ a * m choose p ^ a) * p ^ a) = a + multiplicity p m"
1.237    proof -
1.238      have "(p ^ a * m choose p ^ a) * p ^ a = p ^ a * m * (p ^ a * m - 1 choose (p ^ a - 1))"
1.239        (is "_ = ?rhs") using prime
```
```     2.1 --- a/src/HOL/Algebra/Sylow.thy	Fri Jul 22 15:39:32 2016 +0200
2.2 +++ b/src/HOL/Algebra/Sylow.thy	Fri Jul 22 17:35:54 2016 +0200
2.3 @@ -60,7 +60,7 @@
2.4  locale sylow_central = sylow +
2.5    fixes H and M1 and M
2.6    assumes M_in_quot:  "M \<in> calM // RelM"
2.7 -      and not_dvd_M:  "~(p ^ Suc(exponent p m) dvd card(M))"
2.8 +      and not_dvd_M:  "~(p ^ Suc(multiplicity p m) dvd card(M))"
2.9        and M1_in_M:    "M1 \<in> M"
2.10    defines "H == {g. g\<in>carrier G & M1 #> g = M1}"
2.11
2.12 @@ -128,7 +128,7 @@
2.13  by (simp add: card_calM zero_less_binomial le_extend_mult zero_less_m)
2.14
2.15  lemma max_p_div_calM:
2.16 -     "~ (p ^ Suc(exponent p m) dvd card(calM))"
2.17 +     "~ (p ^ Suc(multiplicity p m) dvd card(calM))"
2.18  proof
2.19    assume "p ^ Suc (multiplicity p m) dvd card calM"
2.20    with zero_less_card_calM prime_p
2.21 @@ -145,7 +145,7 @@
2.22    by (rule_tac B = "Pow (carrier G) " in finite_subset) auto
2.23
2.24  lemma lemma_A1:
2.25 -     "\<exists>M \<in> calM // RelM. ~ (p ^ Suc(exponent p m) dvd card(M))"
2.26 +     "\<exists>M \<in> calM // RelM. ~ (p ^ Suc(multiplicity p m) dvd card(M))"
2.27    using RelM_equiv equiv_imp_dvd_card finite_calM max_p_div_calM by blast
2.28
2.29  end
2.30 @@ -307,7 +307,7 @@
2.31
2.32  lemma (in sylow_central) lemma_leq1: "p^a \<le> card(H)"
2.33  apply (rule dvd_imp_le)
2.34 - apply (rule div_combine [OF prime_p not_dvd_M])
2.35 + apply (rule div_combine [OF prime_imp_prime_elem[OF prime_p] not_dvd_M])
2.36   prefer 2 apply (blast intro: subgroup.finite_imp_card_positive H_is_subgroup)
2.38                   zero_less_m)
```
```     3.1 --- a/src/HOL/Nonstandard_Analysis/Examples/NSPrimes.thy	Fri Jul 22 15:39:32 2016 +0200
3.2 +++ b/src/HOL/Nonstandard_Analysis/Examples/NSPrimes.thy	Fri Jul 22 17:35:54 2016 +0200
3.3 @@ -7,7 +7,7 @@
3.4  section\<open>The Nonstandard Primes as an Extension of the Prime Numbers\<close>
3.5
3.6  theory NSPrimes
3.7 -imports "~~/src/HOL/Number_Theory/UniqueFactorization" "../Hyperreal"
3.8 +imports "~~/src/HOL/Number_Theory/Primes" "../Hyperreal"
3.9  begin
3.10
3.11  text\<open>These can be used to derive an alternative proof of the infinitude of
```
```     4.1 --- a/src/HOL/Number_Theory/Factorial_Ring.thy	Fri Jul 22 15:39:32 2016 +0200
4.2 +++ b/src/HOL/Number_Theory/Factorial_Ring.thy	Fri Jul 22 17:35:54 2016 +0200
4.3 @@ -233,6 +233,61 @@
4.4    "is_unit a \<Longrightarrow> is_prime_elem (a * p) \<longleftrightarrow> is_prime_elem p"
4.5    by (auto simp: is_prime_elem_def mult.commute[of a] is_unit_mult_iff mult_unit_dvd_iff)
4.6
4.7 +lemma prime_dvd_cases:
4.8 +  assumes pk: "p*k dvd m*n" and p: "is_prime_elem p"
4.9 +  shows "(\<exists>x. k dvd x*n \<and> m = p*x) \<or> (\<exists>y. k dvd m*y \<and> n = p*y)"
4.10 +proof -
4.11 +  have "p dvd m*n" using dvd_mult_left pk by blast
4.12 +  then consider "p dvd m" | "p dvd n"
4.13 +    using p prime_dvd_mult_iff by blast
4.14 +  then show ?thesis
4.15 +  proof cases
4.16 +    case 1 then obtain a where "m = p * a" by (metis dvd_mult_div_cancel)
4.17 +      then have "\<exists>x. k dvd x * n \<and> m = p * x"
4.18 +        using p pk by (auto simp: mult.assoc)
4.19 +    then show ?thesis ..
4.20 +  next
4.21 +    case 2 then obtain b where "n = p * b" by (metis dvd_mult_div_cancel)
4.22 +    with p pk have "\<exists>y. k dvd m*y \<and> n = p*y"
4.23 +      by (metis dvd_mult_right dvd_times_left_cancel_iff mult.left_commute mult_zero_left)
4.24 +    then show ?thesis ..
4.25 +  qed
4.26 +qed
4.27 +
4.28 +lemma prime_power_dvd_prod:
4.29 +  assumes pc: "p^c dvd m*n" and p: "is_prime_elem p"
4.30 +  shows "\<exists>a b. a+b = c \<and> p^a dvd m \<and> p^b dvd n"
4.31 +using pc
4.32 +proof (induct c arbitrary: m n)
4.33 +  case 0 show ?case by simp
4.34 +next
4.35 +  case (Suc c)
4.36 +  consider x where "p^c dvd x*n" "m = p*x" | y where "p^c dvd m*y" "n = p*y"
4.37 +    using prime_dvd_cases [of _ "p^c", OF _ p] Suc.prems by force
4.38 +  then show ?case
4.39 +  proof cases
4.40 +    case (1 x)
4.41 +    with Suc.hyps[of x n] obtain a b where "a + b = c \<and> p ^ a dvd x \<and> p ^ b dvd n" by blast
4.42 +    with 1 have "Suc a + b = Suc c \<and> p ^ Suc a dvd m \<and> p ^ b dvd n"
4.43 +      by (auto intro: mult_dvd_mono)
4.44 +    thus ?thesis by blast
4.45 +  next
4.46 +    case (2 y)
4.47 +    with Suc.hyps[of m y] obtain a b where "a + b = c \<and> p ^ a dvd m \<and> p ^ b dvd y" by blast
4.48 +    with 2 have "a + Suc b = Suc c \<and> p ^ a dvd m \<and> p ^ Suc b dvd n"
4.49 +      by (auto intro: mult_dvd_mono)
4.50 +    with Suc.hyps [of m y] show "\<exists>a b. a + b = Suc c \<and> p ^ a dvd m \<and> p ^ b dvd n"
4.51 +      by force
4.52 +  qed
4.53 +qed
4.54 +
4.55 +lemma add_eq_Suc_lem: "a+b = Suc (x+y) \<Longrightarrow> a \<le> x \<or> b \<le> y"
4.56 +  by arith
4.57 +
4.58 +lemma prime_power_dvd_cases:
4.59 +     "\<lbrakk>p^c dvd m * n; a + b = Suc c; is_prime_elem p\<rbrakk> \<Longrightarrow> p ^ a dvd m \<or> p ^ b dvd n"
4.60 +  using power_le_dvd prime_power_dvd_prod by (blast dest: prime_power_dvd_prod add_eq_Suc_lem)
4.61 +
4.62  end
4.63
4.64  context normalization_semidom
4.65 @@ -1384,6 +1439,19 @@
4.66    finally show ?thesis .
4.67  qed
4.68
4.69 +lemma multiplicity_cong:
4.70 +  "(\<And>r. p ^ r dvd a \<longleftrightarrow> p ^ r dvd b) \<Longrightarrow> multiplicity p a = multiplicity p b"
4.71 +  by (simp add: multiplicity_def)
4.72 +
4.73 +lemma not_dvd_imp_multiplicity_0:
4.74 +  assumes "\<not>p dvd x"
4.75 +  shows   "multiplicity p x = 0"
4.76 +proof -
4.77 +  from assms have "multiplicity p x < 1"
4.78 +    by (intro multiplicity_lessI) auto
4.79 +  thus ?thesis by simp
4.80 +qed
4.81 +
4.82
4.83  definition "gcd_factorial a b = (if a = 0 then normalize b
4.84       else if b = 0 then normalize a
```
```     5.1 --- a/src/HOL/Number_Theory/Residues.thy	Fri Jul 22 15:39:32 2016 +0200
5.2 +++ b/src/HOL/Number_Theory/Residues.thy	Fri Jul 22 17:35:54 2016 +0200
5.3 @@ -8,7 +8,7 @@
5.4  section \<open>Residue rings\<close>
5.5
5.6  theory Residues
5.7 -imports UniqueFactorization MiscAlgebra
5.8 +imports Cong MiscAlgebra
5.9  begin
5.10
5.11  subsection \<open>A locale for residue rings\<close>
```
```     6.1 --- a/src/HOL/Number_Theory/UniqueFactorization.thy	Fri Jul 22 15:39:32 2016 +0200
6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
6.3 @@ -1,15 +0,0 @@
6.4 -(*  Title:      HOL/Number_Theory/UniqueFactorization.thy
6.6 -
6.7 -Note: there were previous Isabelle formalizations of unique
6.8 -factorization due to Thomas Marthedal Rasmussen, and, building on
6.9 -that, by Jeremy Avigad and David Gray.
6.10 -*)
6.11 -
6.12 -section \<open>Unique factorization for the natural numbers and the integers\<close>
6.13 -
6.14 -theory UniqueFactorization
6.15 -imports Cong "~~/src/HOL/Library/Multiset"
6.16 -begin
6.17 -
6.18 -end
```
```     7.1 --- a/src/HOL/Proofs/Extraction/Euclid.thy	Fri Jul 22 15:39:32 2016 +0200
7.2 +++ b/src/HOL/Proofs/Extraction/Euclid.thy	Fri Jul 22 17:35:54 2016 +0200
7.3 @@ -8,7 +8,7 @@
7.4
7.5  theory Euclid
7.6  imports
7.7 -  "~~/src/HOL/Number_Theory/UniqueFactorization"
7.8 +  "~~/src/HOL/Number_Theory/Primes"
7.9    Util
7.10    "~~/src/HOL/Library/Code_Target_Numeral"
7.11  begin
```
```     8.1 --- a/src/HOL/ROOT	Fri Jul 22 15:39:32 2016 +0200
8.2 +++ b/src/HOL/ROOT	Fri Jul 22 17:35:54 2016 +0200
8.3 @@ -416,7 +416,6 @@
8.4      "~~/src/HOL/Library/Code_Target_Numeral"