Removed redundant material related to primes
authoreberlm <eberlm@in.tum.de>
Fri Jul 22 17:35:54 2016 +0200 (2016-07-22)
changeset 63537831816778409
parent 63536 8cecf0100996
child 63538 d7b5e2a222c2
Removed redundant material related to primes
src/HOL/Algebra/Exponent.thy
src/HOL/Algebra/Sylow.thy
src/HOL/Nonstandard_Analysis/Examples/NSPrimes.thy
src/HOL/Number_Theory/Factorial_Ring.thy
src/HOL/Number_Theory/Residues.thy
src/HOL/Number_Theory/UniqueFactorization.thy
src/HOL/Proofs/Extraction/Euclid.thy
src/HOL/ROOT
     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.146 -lemma exponent_mult_add: 
   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.162 -        by (metis Suc_n_not_le_n True add_Suc add_Suc_right assms exponent_ge)
   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.37  apply (simp add: index_lem order_G power_add mult_dvd_mono multiplicity_dvd
    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.5 -    Author:     Jeremy Avigad
     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"
     8.5      "~~/src/HOL/Library/Monad_Syntax"
     8.6      "~~/src/HOL/Number_Theory/Primes"
     8.7 -    "~~/src/HOL/Number_Theory/UniqueFactorization"
     8.8      "~~/src/HOL/Library/State_Monad"
     8.9    theories
    8.10      Greatest_Common_Divisor