# HG changeset patch
# User wenzelm
# Date 1492891295 -7200
# Node ID f533820e7248d41d58de00fd57a30e94fcc0a5b0
# Parent  d164c4fc0d2c0f3cde402872ac2bb84151e79117
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;

diff -r d164c4fc0d2c -r f533820e7248 NEWS
--- a/NEWS	Sat Apr 22 12:52:55 2017 +0200
+++ b/NEWS	Sat Apr 22 22:01:35 2017 +0200
@@ -72,6 +72,9 @@
 
 *** HOL ***
 
+* Theories "GCD" and "Binomial" are already included in "Main" (instead
+of "Complex_Main".
+
 * Constants E/L/F in Library/Formal_Power_Series were renamed to
 fps_exp/fps_ln/fps_hypergeo to avoid polluting the name space.
 INCOMPATIBILITY.
diff -r d164c4fc0d2c -r f533820e7248 src/Doc/Corec/Corec.thy
--- a/src/Doc/Corec/Corec.thy	Sat Apr 22 12:52:55 2017 +0200
+++ b/src/Doc/Corec/Corec.thy	Sat Apr 22 22:01:35 2017 +0200
@@ -9,7 +9,7 @@
 *)
 
 theory Corec
-imports GCD "../Datatypes/Setup" "~~/src/HOL/Library/BNF_Corec"
+imports Main "../Datatypes/Setup" "~~/src/HOL/Library/BNF_Corec"
   "~~/src/HOL/Library/FSet"
 begin
 
diff -r d164c4fc0d2c -r f533820e7248 src/HOL/Binomial.thy
--- a/src/HOL/Binomial.thy	Sat Apr 22 12:52:55 2017 +0200
+++ b/src/HOL/Binomial.thy	Sat Apr 22 22:01:35 2017 +0200
@@ -9,7 +9,7 @@
 section \<open>Combinatorial Functions: Factorial Function, Rising Factorials, Binomial Coefficients and Binomial Theorem\<close>
 
 theory Binomial
-  imports Main
+  imports Pre_Main
 begin
 
 subsection \<open>Factorial\<close>
@@ -534,12 +534,12 @@
 
 end
 
-lemma pochhammer_nonneg: 
+lemma pochhammer_nonneg:
   fixes x :: "'a :: linordered_semidom"
   shows "x > 0 \<Longrightarrow> pochhammer x n \<ge> 0"
   by (induction n) (auto simp: pochhammer_Suc intro!: mult_nonneg_nonneg add_nonneg_nonneg)
 
-lemma pochhammer_pos: 
+lemma pochhammer_pos:
   fixes x :: "'a :: linordered_semidom"
   shows "x > 0 \<Longrightarrow> pochhammer x n > 0"
   by (induction n) (auto simp: pochhammer_Suc intro!: mult_pos_pos add_pos_nonneg)
@@ -1616,7 +1616,7 @@
   qed
 qed
 
-lemma card_disjoint_shuffle: 
+lemma card_disjoint_shuffle:
   assumes "set xs \<inter> set ys = {}"
   shows   "card (shuffle xs ys) = (length xs + length ys) choose length xs"
 using assms
@@ -1634,7 +1634,7 @@
     by (rule card_image) auto
   also have "\<dots> = (length (x # xs) + length ys) choose length (x # xs)"
     using "3.prems" by (intro "3.IH") auto
-  also have "length xs + length (y # ys) choose length xs + \<dots> = 
+  also have "length xs + length (y # ys) choose length xs + \<dots> =
                (length (x # xs) + length (y # ys)) choose length (x # xs)" by simp
   finally show ?case .
 qed auto
diff -r d164c4fc0d2c -r f533820e7248 src/HOL/Codegenerator_Test/Code_Test_GHC.thy
--- a/src/HOL/Codegenerator_Test/Code_Test_GHC.thy	Sat Apr 22 12:52:55 2017 +0200
+++ b/src/HOL/Codegenerator_Test/Code_Test_GHC.thy	Sat Apr 22 22:01:35 2017 +0200
@@ -4,7 +4,7 @@
 Test case for test_code on GHC
 *)
 
-theory Code_Test_GHC imports "../Library/Code_Test" "../GCD" begin
+theory Code_Test_GHC imports "../Library/Code_Test" begin
 
 test_code "(14 + 7 * -12 :: integer) = 140 div -2" in GHC
 
diff -r d164c4fc0d2c -r f533820e7248 src/HOL/Codegenerator_Test/Code_Test_OCaml.thy
--- a/src/HOL/Codegenerator_Test/Code_Test_OCaml.thy	Sat Apr 22 12:52:55 2017 +0200
+++ b/src/HOL/Codegenerator_Test/Code_Test_OCaml.thy	Sat Apr 22 22:01:35 2017 +0200
@@ -4,7 +4,7 @@
 Test case for test_code on OCaml
 *)
 
-theory Code_Test_OCaml imports  "../Library/Code_Test" "../GCD" begin
+theory Code_Test_OCaml imports  "../Library/Code_Test" begin
 
 test_code "14 + 7 * -12 = (140 div -2 :: integer)" in OCaml
 
diff -r d164c4fc0d2c -r f533820e7248 src/HOL/Codegenerator_Test/Code_Test_Scala.thy
--- a/src/HOL/Codegenerator_Test/Code_Test_Scala.thy	Sat Apr 22 12:52:55 2017 +0200
+++ b/src/HOL/Codegenerator_Test/Code_Test_Scala.thy	Sat Apr 22 22:01:35 2017 +0200
@@ -4,7 +4,7 @@
 Test case for test_code on Scala
 *)
 
-theory Code_Test_Scala imports  "../Library/Code_Test" "../GCD" begin 
+theory Code_Test_Scala imports  "../Library/Code_Test" begin
 
 declare [[scala_case_insensitive]]
 
diff -r d164c4fc0d2c -r f533820e7248 src/HOL/Computational_Algebra/Factorial_Ring.thy
--- a/src/HOL/Computational_Algebra/Factorial_Ring.thy	Sat Apr 22 12:52:55 2017 +0200
+++ b/src/HOL/Computational_Algebra/Factorial_Ring.thy	Sat Apr 22 22:01:35 2017 +0200
@@ -6,9 +6,8 @@
 section \<open>Factorial (semi)rings\<close>
 
 theory Factorial_Ring
-imports 
+imports
   Main
-  "../GCD"
   "~~/src/HOL/Library/Multiset"
 begin
 
@@ -66,7 +65,7 @@
   shows "p \<noteq> 0"
   using assms by (auto intro: ccontr)
 
-lemma prime_elem_dvd_power: 
+lemma prime_elem_dvd_power:
   "prime_elem p \<Longrightarrow> p dvd x ^ n \<Longrightarrow> p dvd x"
   by (induction n) (auto dest: prime_elem_dvd_multD intro: dvd_trans[of _ 1])
 
@@ -111,7 +110,7 @@
   with \<open>irreducible p\<close> show False
     by (simp add: irreducible_not_unit)
 qed
-   
+
 lemma unit_imp_no_prime_divisors:
   assumes "is_unit x" "prime_elem p"
   shows   "\<not>p dvd x"
@@ -261,13 +260,13 @@
     using p prime_elem_dvd_mult_iff by blast
   then show ?thesis
   proof cases
-    case 1 then obtain a where "m = p * a" by (metis dvd_mult_div_cancel) 
+    case 1 then obtain a where "m = p * a" by (metis dvd_mult_div_cancel)
       then have "\<exists>x. k dvd x * n \<and> m = p * x"
         using p pk by (auto simp: mult.assoc)
     then show ?thesis ..
   next
-    case 2 then obtain b where "n = p * b" by (metis dvd_mult_div_cancel) 
-    with p pk have "\<exists>y. k dvd m*y \<and> n = p*y" 
+    case 2 then obtain b where "n = p * b" by (metis dvd_mult_div_cancel)
+    with p pk have "\<exists>y. k dvd m*y \<and> n = p*y"
       by (metis dvd_mult_right dvd_times_left_cancel_iff mult.left_commute mult_zero_left)
     then show ?thesis ..
   qed
@@ -285,13 +284,13 @@
     using prime_elem_dvd_cases [of _ "p^c", OF _ p] Suc.prems by force
   then show ?case
   proof cases
-    case (1 x) 
+    case (1 x)
     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
     with 1 have "Suc a + b = Suc c \<and> p ^ Suc a dvd m \<and> p ^ b dvd n"
       by (auto intro: mult_dvd_mono)
     thus ?thesis by blast
   next
-    case (2 y) 
+    case (2 y)
     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
     with 2 have "a + Suc b = Suc c \<and> p ^ a dvd m \<and> p ^ Suc b dvd n"
       by (auto intro: mult_dvd_mono)
@@ -325,7 +324,7 @@
   assumes "prime_elem p"
   assumes "p ^ n dvd a * b" and "n > 0" and "\<not> p dvd a"
   shows "p ^ n dvd b"
-  using \<open>p ^ n dvd a * b\<close> and \<open>n > 0\<close> 
+  using \<open>p ^ n dvd a * b\<close> and \<open>n > 0\<close>
 proof (induct n arbitrary: b)
   case 0 then show ?case by simp
 next
@@ -454,7 +453,7 @@
 lemma prime_dvd_mult_iff: "prime p \<Longrightarrow> p dvd a * b \<longleftrightarrow> p dvd a \<or> p dvd b"
   by (auto dest: prime_dvd_multD)
 
-lemma prime_dvd_power: 
+lemma prime_dvd_power:
   "prime p \<Longrightarrow> p dvd x ^ n \<Longrightarrow> p dvd x"
   by (auto dest!: prime_elem_dvd_power simp: prime_def)
 
@@ -610,11 +609,11 @@
   shows   "coprime p n"
   using assms by (simp add: prime_elem_imp_coprime)
 
-lemma prime_elem_imp_power_coprime: 
+lemma prime_elem_imp_power_coprime:
   "prime_elem p \<Longrightarrow> \<not>p dvd a \<Longrightarrow> coprime a (p ^ m)"
   by (auto intro!: coprime_exp dest: prime_elem_imp_coprime simp: gcd.commute)
 
-lemma prime_imp_power_coprime: 
+lemma prime_imp_power_coprime:
   "prime p \<Longrightarrow> \<not>p dvd a \<Longrightarrow> coprime a (p ^ m)"
   by (simp add: prime_elem_imp_power_coprime)
 
@@ -625,12 +624,12 @@
 proof -
   from ab p have "\<not>p dvd a \<or> \<not>p dvd b"
     by (auto simp: coprime prime_elem_def)
-  with p have "coprime (p^n) a \<or> coprime (p^n) b" 
+  with p have "coprime (p^n) a \<or> coprime (p^n) b"
     by (auto intro: prime_elem_imp_coprime coprime_exp_left)
   with pab show ?thesis by (auto intro: coprime_dvd_mult simp: mult_ac)
 qed
 
-lemma primes_coprime: 
+lemma primes_coprime:
   "prime p \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
   using prime_imp_coprime primes_dvd_imp_eq by blast
 
@@ -644,7 +643,7 @@
     "x \<noteq> 0 \<Longrightarrow> \<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> prod_mset A = normalize x"
 
 text \<open>Alternative characterization\<close>
-  
+
 lemma (in normalization_semidom) factorial_semiring_altI_aux:
   assumes finite_divisors: "\<And>x. x \<noteq> 0 \<Longrightarrow> finite {y. y dvd x \<and> normalize y = y}"
   assumes irreducible_imp_prime_elem: "\<And>x. irreducible x \<Longrightarrow> prime_elem x"
@@ -703,14 +702,14 @@
       from A B show ?thesis by (intro exI[of _ "A + B"]) (auto simp: c normalize_mult)
     qed
   qed
-qed 
+qed
 
 lemma factorial_semiring_altI:
   assumes finite_divisors: "\<And>x::'a. x \<noteq> 0 \<Longrightarrow> finite {y. y dvd x \<and> normalize y = y}"
   assumes irreducible_imp_prime: "\<And>x::'a. irreducible x \<Longrightarrow> prime_elem x"
   shows   "OFCLASS('a :: normalization_semidom, factorial_semiring_class)"
   by intro_classes (rule factorial_semiring_altI_aux[OF assms])
-  
+
 text \<open>Properties\<close>
 
 context factorial_semiring
@@ -912,7 +911,7 @@
 lemma prime_multiplicity_other:
   assumes "prime p" "prime q" "p \<noteq> q"
   shows   "multiplicity p q = 0"
-  using assms by (subst prime_elem_multiplicity_eq_zero_iff) (auto dest: primes_dvd_imp_eq)  
+  using assms by (subst prime_elem_multiplicity_eq_zero_iff) (auto dest: primes_dvd_imp_eq)
 
 lemma prime_multiplicity_gt_zero_iff:
   "prime_elem p \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> multiplicity p x > 0 \<longleftrightarrow> p dvd x"
@@ -1057,7 +1056,7 @@
   also have "multiplicity p \<dots> = multiplicity p x"
     by (rule multiplicity_times_unit_right) (simp add: is_unit_unit_factor)
   finally show ?thesis .
-qed simp_all   
+qed simp_all
 
 lemma multiplicity_prime [simp]: "prime_elem p \<Longrightarrow> multiplicity p p = 1"
   by (rule multiplicity_self) auto
@@ -1272,13 +1271,13 @@
 proof -
   have "multiplicity p (x * y) = count (prime_factorization (x * y)) (normalize p)"
     by (subst count_prime_factorization_prime) (simp_all add: assms)
-  also from assms 
+  also from assms
     have "prime_factorization (x * y) = prime_factorization x + prime_factorization y"
       by (intro prime_factorization_mult)
-  also have "count \<dots> (normalize p) = 
+  also have "count \<dots> (normalize p) =
     count (prime_factorization x) (normalize p) + count (prime_factorization y) (normalize p)"
     by simp
-  also have "\<dots> = multiplicity p x + multiplicity p y" 
+  also have "\<dots> = multiplicity p x + multiplicity p y"
     by (subst (1 2) count_prime_factorization_prime) (simp_all add: assms)
   finally show ?thesis .
 qed
@@ -1300,7 +1299,7 @@
 proof -
   have "multiplicity p (prod f A) = (\<Sum>x\<in>#mset_set A. multiplicity p (f x))"
     using assms by (subst prod_unfold_prod_mset)
-                   (simp_all add: prime_elem_multiplicity_prod_mset_distrib sum_unfold_sum_mset 
+                   (simp_all add: prime_elem_multiplicity_prod_mset_distrib sum_unfold_sum_mset
                       multiset.map_comp o_def)
   also from \<open>finite A\<close> have "\<dots> = (\<Sum>x\<in>A. multiplicity p (f x))"
     by (induction A rule: finite_induct) simp_all
@@ -1330,7 +1329,7 @@
   finally show ?thesis ..
 qed
 
-lemma prime_factorization_subset_imp_dvd: 
+lemma prime_factorization_subset_imp_dvd:
   "x \<noteq> 0 \<Longrightarrow> (prime_factorization x \<subseteq># prime_factorization y) \<Longrightarrow> x dvd y"
   by (cases "y = 0") (simp_all add: prime_factorization_subset_iff_dvd)
 
@@ -1361,7 +1360,7 @@
   also have "\<dots> = (\<Prod>p \<in> prime_factors x. p ^ count (prime_factorization x) p)"
     by (subst prod_mset_multiplicity) simp_all
   also have "\<dots> = (\<Prod>p \<in> prime_factors x. p ^ multiplicity p x)"
-    by (intro prod.cong) 
+    by (intro prod.cong)
       (simp_all add: assms count_prime_factorization_prime in_prime_factors_imp_prime)
   finally show ?thesis ..
 qed
@@ -1381,23 +1380,23 @@
     by (simp only: set_mset_def)
   from S(2) have "normalize n = (\<Prod>p\<in>S. p ^ f p)" .
   also have "\<dots> = prod_mset A" by (simp add: prod_mset_multiplicity S_eq set_mset_A count_A)
-  also from nz have "normalize n = prod_mset (prime_factorization n)" 
+  also from nz have "normalize n = prod_mset (prime_factorization n)"
     by (simp add: prod_mset_prime_factorization)
-  finally have "prime_factorization (prod_mset A) = 
+  finally have "prime_factorization (prod_mset A) =
                   prime_factorization (prod_mset (prime_factorization n))" by simp
   also from S(1) have "prime_factorization (prod_mset A) = A"
     by (intro prime_factorization_prod_mset_primes) (auto simp: set_mset_A)
   also have "prime_factorization (prod_mset (prime_factorization n)) = prime_factorization n"
     by (intro prime_factorization_prod_mset_primes) auto
   finally show "S = prime_factors n" by (simp add: set_mset_A [symmetric])
-  
+
   show "(\<forall>p. prime p \<longrightarrow> f p = multiplicity p n)"
   proof safe
     fix p :: 'a assume p: "prime p"
     have "multiplicity p n = multiplicity p (normalize n)" by simp
-    also have "normalize n = prod_mset A" 
+    also have "normalize n = prod_mset A"
       by (simp add: prod_mset_multiplicity S_eq set_mset_A count_A S)
-    also from p set_mset_A S(1) 
+    also from p set_mset_A S(1)
     have "multiplicity p \<dots> = sum_mset (image_mset (multiplicity p) A)"
       by (intro prime_elem_multiplicity_prod_mset_distrib) auto
     also from S(1) p
@@ -1408,7 +1407,7 @@
   qed
 qed
 
-lemma prime_factors_product: 
+lemma prime_factors_product:
   "x \<noteq> 0 \<Longrightarrow> y \<noteq> 0 \<Longrightarrow> prime_factors (x * y) = prime_factors x \<union> prime_factors y"
   by (simp add: prime_factorization_mult)
 
@@ -1454,7 +1453,7 @@
   "(\<And>r. p ^ r dvd a \<longleftrightarrow> p ^ r dvd b) \<Longrightarrow> multiplicity p a = multiplicity p b"
   by (simp add: multiplicity_def)
 
-lemma not_dvd_imp_multiplicity_0: 
+lemma not_dvd_imp_multiplicity_0:
   assumes "\<not>p dvd x"
   shows   "multiplicity p x = 0"
 proof -
@@ -1740,11 +1739,11 @@
 
 lemma
   assumes "x \<noteq> 0" "y \<noteq> 0"
-  shows gcd_eq_factorial': 
-          "gcd x y = (\<Prod>p \<in> prime_factors x \<inter> prime_factors y. 
+  shows gcd_eq_factorial':
+          "gcd x y = (\<Prod>p \<in> prime_factors x \<inter> prime_factors y.
                           p ^ min (multiplicity p x) (multiplicity p y))" (is "_ = ?rhs1")
     and lcm_eq_factorial':
-          "lcm x y = (\<Prod>p \<in> prime_factors x \<union> prime_factors y. 
+          "lcm x y = (\<Prod>p \<in> prime_factors x \<union> prime_factors y.
                           p ^ max (multiplicity p x) (multiplicity p y))" (is "_ = ?rhs2")
 proof -
   have "gcd x y = gcd_factorial x y" by (rule gcd_eq_gcd_factorial)
@@ -1784,7 +1783,7 @@
   case False
   hence "normalize (gcd x (lcm y z)) = normalize (lcm (gcd x y) (gcd x z))"
     by (intro associatedI prime_factorization_subset_imp_dvd)
-       (auto simp: lcm_eq_0_iff prime_factorization_gcd prime_factorization_lcm 
+       (auto simp: lcm_eq_0_iff prime_factorization_gcd prime_factorization_lcm
           subset_mset.inf_sup_distrib1)
   thus ?thesis by simp
 qed
@@ -1799,7 +1798,7 @@
   case False
   hence "normalize (lcm x (gcd y z)) = normalize (gcd (lcm x y) (lcm x z))"
     by (intro associatedI prime_factorization_subset_imp_dvd)
-       (auto simp: lcm_eq_0_iff prime_factorization_gcd prime_factorization_lcm 
+       (auto simp: lcm_eq_0_iff prime_factorization_gcd prime_factorization_lcm
           subset_mset.sup_inf_distrib1)
   thus ?thesis by simp
 qed
diff -r d164c4fc0d2c -r f533820e7248 src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Sat Apr 22 12:52:55 2017 +0200
+++ b/src/HOL/GCD.thy	Sat Apr 22 22:01:35 2017 +0200
@@ -31,12 +31,12 @@
 section \<open>Greatest common divisor and least common multiple\<close>
 
 theory GCD
-  imports Main
+  imports Pre_Main
 begin
 
 subsection \<open>Abstract bounded quasi semilattices as common foundation\<close>
-  
-locale bounded_quasi_semilattice = abel_semigroup + 
+
+locale bounded_quasi_semilattice = abel_semigroup +
   fixes top :: 'a  ("\<top>") and bot :: 'a  ("\<bottom>")
     and normalize :: "'a \<Rightarrow> 'a"
   assumes idem_normalize [simp]: "a \<^bold>* a = normalize a"
@@ -65,7 +65,7 @@
 lemma top_right_normalize [simp]:
   "a \<^bold>* \<top> = normalize a"
   using top_left_normalize [of a] by (simp add: ac_simps)
-  
+
 lemma bottom_right_bottom [simp]:
   "a \<^bold>* \<bottom> = \<bottom>"
   using bottom_left_bottom [of a] by (simp add: ac_simps)
@@ -74,7 +74,7 @@
   "a \<^bold>* normalize b = a \<^bold>* b"
   using normalize_left_idem [of b a] by (simp add: ac_simps)
 
-end    
+end
 
 locale bounded_quasi_semilattice_set = bounded_quasi_semilattice
 begin
@@ -134,7 +134,7 @@
   assumes "B \<subseteq> A"
   shows "F B \<^bold>* F A = F A"
   using assms by (simp add: union [symmetric] Un_absorb1)
-  
+
 end
 
 subsection \<open>Abstract GCD and LCM\<close>
@@ -282,7 +282,7 @@
   show "coprime 1 a" for a
     by (rule associated_eqI) simp_all
 qed simp_all
-  
+
 lemma gcd_self: "gcd a a = normalize a"
   by (fact gcd.idem_normalize)
 
@@ -1071,7 +1071,7 @@
   moreover from assms have "p dvd gcd (b * a) (b * p)"
     by (intro gcd_greatest) (simp_all add: mult.commute)
   hence "p dvd b * gcd a p" by (simp add: gcd_mult_distrib)
-  with False have "y dvd b" 
+  with False have "y dvd b"
     by (simp add: x_def y_def div_dvd_iff_mult assms)
   ultimately show ?thesis by (rule that)
 qed
@@ -1527,7 +1527,7 @@
 
 end
 
-  
+
 subsection \<open>An aside: GCD and LCM on finite sets for incomplete gcd rings\<close>
 
 context semiring_gcd
@@ -1546,15 +1546,15 @@
 
 abbreviation lcm_list :: "'a list \<Rightarrow> 'a"
   where "lcm_list xs \<equiv> Lcm\<^sub>f\<^sub>i\<^sub>n (set xs)"
-    
+
 lemma Gcd_fin_dvd:
   "a \<in> A \<Longrightarrow> Gcd\<^sub>f\<^sub>i\<^sub>n A dvd a"
-  by (induct A rule: infinite_finite_induct) 
+  by (induct A rule: infinite_finite_induct)
     (auto intro: dvd_trans)
 
 lemma dvd_Lcm_fin:
   "a \<in> A \<Longrightarrow> a dvd Lcm\<^sub>f\<^sub>i\<^sub>n A"
-  by (induct A rule: infinite_finite_induct) 
+  by (induct A rule: infinite_finite_induct)
     (auto intro: dvd_trans)
 
 lemma Gcd_fin_greatest:
@@ -1580,7 +1580,7 @@
 lemma dvd_gcd_list_iff:
   "b dvd gcd_list xs \<longleftrightarrow> (\<forall>a\<in>set xs. b dvd a)"
   by (simp add: dvd_Gcd_fin_iff)
-  
+
 lemma Lcm_fin_dvd_iff:
   "Lcm\<^sub>f\<^sub>i\<^sub>n A dvd b  \<longleftrightarrow> (\<forall>a\<in>A. a dvd b)" if "finite A"
   using that by (auto intro: Lcm_fin_least dvd_Lcm_fin dvd_trans [of _ "Lcm\<^sub>f\<^sub>i\<^sub>n A" b])
diff -r d164c4fc0d2c -r f533820e7248 src/HOL/HOLCF/Universal.thy
--- a/src/HOL/HOLCF/Universal.thy	Sat Apr 22 12:52:55 2017 +0200
+++ b/src/HOL/HOLCF/Universal.thy	Sat Apr 22 22:01:35 2017 +0200
@@ -8,6 +8,8 @@
 imports Bifinite Completion "~~/src/HOL/Library/Nat_Bijection"
 begin
 
+no_notation binomial  (infixl "choose" 65)
+
 subsection \<open>Basis for universal domain\<close>
 
 subsubsection \<open>Basis datatype\<close>
@@ -976,7 +978,7 @@
 apply (simp add: udom_approx_principal)
 apply (simp add: ubasis_until_same ubasis_le_refl)
 done
- 
+
 lemma udom_approx [simp]: "approx_chain udom_approx"
 proof
   show "chain (\<lambda>i. udom_approx i)"
@@ -990,4 +992,6 @@
 
 hide_const (open) node
 
+notation binomial  (infixl "choose" 65)
+
 end
diff -r d164c4fc0d2c -r f533820e7248 src/HOL/Import/Import_Setup.thy
--- a/src/HOL/Import/Import_Setup.thy	Sat Apr 22 12:52:55 2017 +0200
+++ b/src/HOL/Import/Import_Setup.thy	Sat Apr 22 22:01:35 2017 +0200
@@ -6,7 +6,7 @@
 section \<open>Importer machinery and required theorems\<close>
 
 theory Import_Setup
-imports Main "~~/src/HOL/Binomial"
+imports Main
 keywords "import_type_map" "import_const_map" "import_file" :: thy_decl
 begin
 
diff -r d164c4fc0d2c -r f533820e7248 src/HOL/Library/Code_Target_Int.thy
--- a/src/HOL/Library/Code_Target_Int.thy	Sat Apr 22 12:52:55 2017 +0200
+++ b/src/HOL/Library/Code_Target_Int.thy	Sat Apr 22 22:01:35 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>Implementation of integer numbers by target-language integers\<close>
 
 theory Code_Target_Int
-imports "../GCD"
+imports Main
 begin
 
 code_datatype int_of_integer
@@ -22,11 +22,11 @@
 
 lemma [code]:
   "Int.Pos = int_of_integer \<circ> integer_of_num"
-  by transfer (simp add: fun_eq_iff) 
+  by transfer (simp add: fun_eq_iff)
 
 lemma [code]:
   "Int.Neg = int_of_integer \<circ> uminus \<circ> integer_of_num"
-  by transfer (simp add: fun_eq_iff) 
+  by transfer (simp add: fun_eq_iff)
 
 lemma [code_abbrev]:
   "int_of_integer (numeral k) = Int.Pos k"
@@ -37,7 +37,7 @@
   by transfer simp
 
 context
-begin  
+begin
 
 qualified definition positive :: "num \<Rightarrow> int"
   where [simp]: "positive = numeral"
diff -r d164c4fc0d2c -r f533820e7248 src/HOL/Library/Permutations.thy
--- a/src/HOL/Library/Permutations.thy	Sat Apr 22 12:52:55 2017 +0200
+++ b/src/HOL/Library/Permutations.thy	Sat Apr 22 22:01:35 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>Permutations, both general and specifically on finite sets.\<close>
 
 theory Permutations
-  imports Binomial Multiset Disjoint_Sets
+  imports Multiset Disjoint_Sets
 begin
 
 subsection \<open>Transpositions\<close>
diff -r d164c4fc0d2c -r f533820e7248 src/HOL/Library/Stirling.thy
--- a/src/HOL/Library/Stirling.thy	Sat Apr 22 12:52:55 2017 +0200
+++ b/src/HOL/Library/Stirling.thy	Sat Apr 22 22:01:35 2017 +0200
@@ -8,7 +8,7 @@
 section \<open>Stirling numbers of first and second kind\<close>
 
 theory Stirling
-imports Binomial
+imports Main
 begin
 
 subsection \<open>Stirling numbers of the second kind\<close>
diff -r d164c4fc0d2c -r f533820e7248 src/HOL/Main.thy
--- a/src/HOL/Main.thy	Sat Apr 22 12:52:55 2017 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,42 +0,0 @@
-section \<open>Main HOL\<close>
-
-theory Main
-imports Predicate_Compile Quickcheck_Narrowing Extraction Nitpick BNF_Greatest_Fixpoint Filter Conditionally_Complete_Lattices
-begin
-
-text \<open>
-  Classical Higher-order Logic -- only ``Main'', excluding real and
-  complex numbers etc.
-\<close>
-
-no_notation
-  bot ("\<bottom>") and
-  top ("\<top>") and
-  inf (infixl "\<sqinter>" 70) and
-  sup (infixl "\<squnion>" 65) and
-  Inf ("\<Sqinter>_" [900] 900) and
-  Sup ("\<Squnion>_" [900] 900) and
-  ordLeq2 (infix "<=o" 50) and
-  ordLeq3 (infix "\<le>o" 50) and
-  ordLess2 (infix "<o" 50) and
-  ordIso2 (infix "=o" 50) and
-  card_of ("|_|") and
-  csum (infixr "+c" 65) and
-  cprod (infixr "*c" 80) and
-  cexp (infixr "^c" 90) and
-  convol ("\<langle>(_,/ _)\<rangle>")
-
-hide_const (open)
-  czero cinfinite cfinite csum cone ctwo Csum cprod cexp image2 image2p vimage2p Gr Grp collect
-  fsts snds setl setr convol pick_middlep fstOp sndOp csquare relImage relInvImage Succ Shift
-  shift proj id_bnf
-
-hide_fact (open) id_bnf_def type_definition_id_bnf_UNIV
-
-no_syntax
-  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
-  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
-  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
-  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
-
-end
diff -r d164c4fc0d2c -r f533820e7248 src/HOL/NthRoot.thy
--- a/src/HOL/NthRoot.thy	Sat Apr 22 12:52:55 2017 +0200
+++ b/src/HOL/NthRoot.thy	Sat Apr 22 22:01:35 2017 +0200
@@ -6,7 +6,7 @@
 section \<open>Nth Roots of Real Numbers\<close>
 
 theory NthRoot
-  imports Deriv Binomial
+  imports Deriv
 begin
 
 
@@ -469,7 +469,7 @@
 lemma real_less_rsqrt: "x\<^sup>2 < y \<Longrightarrow> x < sqrt y"
   using real_sqrt_less_mono[of "x\<^sup>2" y] by simp
 
-lemma real_sqrt_power_even: 
+lemma real_sqrt_power_even:
   assumes "even n" "x \<ge> 0"
   shows   "sqrt x ^ n = x ^ (n div 2)"
 proof -
diff -r d164c4fc0d2c -r f533820e7248 src/HOL/Pre_Main.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Pre_Main.thy	Sat Apr 22 22:01:35 2017 +0200
@@ -0,0 +1,42 @@
+section \<open>Main HOL\<close>
+
+theory Pre_Main
+imports Predicate_Compile Quickcheck_Narrowing Extraction Nitpick BNF_Greatest_Fixpoint Filter Conditionally_Complete_Lattices
+begin
+
+text \<open>
+  Classical Higher-order Logic -- only ``Main'', excluding real and
+  complex numbers etc.
+\<close>
+
+no_notation
+  bot ("\<bottom>") and
+  top ("\<top>") and
+  inf (infixl "\<sqinter>" 70) and
+  sup (infixl "\<squnion>" 65) and
+  Inf ("\<Sqinter>_" [900] 900) and
+  Sup ("\<Squnion>_" [900] 900) and
+  ordLeq2 (infix "<=o" 50) and
+  ordLeq3 (infix "\<le>o" 50) and
+  ordLess2 (infix "<o" 50) and
+  ordIso2 (infix "=o" 50) and
+  card_of ("|_|") and
+  csum (infixr "+c" 65) and
+  cprod (infixr "*c" 80) and
+  cexp (infixr "^c" 90) and
+  convol ("\<langle>(_,/ _)\<rangle>")
+
+hide_const (open)
+  czero cinfinite cfinite csum cone ctwo Csum cprod cexp image2 image2p vimage2p Gr Grp collect
+  fsts snds setl setr convol pick_middlep fstOp sndOp csquare relImage relInvImage Succ Shift
+  shift proj id_bnf
+
+hide_fact (open) id_bnf_def type_definition_id_bnf_UNIV
+
+no_syntax
+  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
+  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
+  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
+  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
+
+end
diff -r d164c4fc0d2c -r f533820e7248 src/HOL/ROOT
--- a/src/HOL/ROOT	Sat Apr 22 12:52:55 2017 +0200
+++ b/src/HOL/ROOT	Sat Apr 22 22:01:35 2017 +0200
@@ -23,8 +23,6 @@
   sessions
     "HOL-Library"
   theories
-    GCD
-    Binomial
     "HOL-Library.Old_Datatype"
   files
     "Tools/Quickcheck/Narrowing_Engine.hs"
diff -r d164c4fc0d2c -r f533820e7248 src/HOL/Rat.thy
--- a/src/HOL/Rat.thy	Sat Apr 22 12:52:55 2017 +0200
+++ b/src/HOL/Rat.thy	Sat Apr 22 22:01:35 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>Rational numbers\<close>
 
 theory Rat
-  imports GCD Archimedean_Field
+  imports Archimedean_Field
 begin
 
 subsection \<open>Rational numbers as quotient\<close>
@@ -403,7 +403,7 @@
 
 lemma quotient_of_denom_pos': "snd (quotient_of r) > 0"
   using quotient_of_denom_pos [of r] by (simp add: prod_eq_iff)
-    
+
 lemma quotient_of_coprime: "quotient_of r = (p, q) \<Longrightarrow> coprime p q"
   by (cases r) (simp add: quotient_of_Fract normalize_coprime)
 
diff -r d164c4fc0d2c -r f533820e7248 src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy
--- a/src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy	Sat Apr 22 12:52:55 2017 +0200
+++ b/src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy	Sat Apr 22 22:01:35 2017 +0200
@@ -4,7 +4,7 @@
 *)
 
 theory Greatest_Common_Divisor
-imports "../../SPARK" GCD
+imports "../../SPARK"
 begin
 
 spark_proof_functions
diff -r d164c4fc0d2c -r f533820e7248 src/HOL/SPARK/Manual/Simple_Greatest_Common_Divisor.thy
--- a/src/HOL/SPARK/Manual/Simple_Greatest_Common_Divisor.thy	Sat Apr 22 12:52:55 2017 +0200
+++ b/src/HOL/SPARK/Manual/Simple_Greatest_Common_Divisor.thy	Sat Apr 22 22:01:35 2017 +0200
@@ -4,7 +4,7 @@
 *)
 
 theory Simple_Greatest_Common_Divisor
-imports "../SPARK" GCD
+imports "../SPARK"
 begin
 
 spark_proof_functions
diff -r d164c4fc0d2c -r f533820e7248 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Sat Apr 22 12:52:55 2017 +0200
+++ b/src/HOL/Transcendental.thy	Sat Apr 22 22:01:35 2017 +0200
@@ -7,7 +7,7 @@
 section \<open>Power Series, Transcendental Functions etc.\<close>
 
 theory Transcendental
-imports Binomial Series Deriv NthRoot
+imports Series Deriv NthRoot
 begin
 
 text \<open>A fact theorem on reals.\<close>
@@ -74,7 +74,7 @@
 subsection \<open>More facts about binomial coefficients\<close>
 
 text \<open>
-  These facts could have been proven before, but having real numbers 
+  These facts could have been proven before, but having real numbers
   makes the proofs a lot easier.
 \<close>
 
@@ -115,11 +115,11 @@
   thus ?thesis
   proof (induction rule: inc_induct)
     case base
-    with assms binomial_less_binomial_Suc[of "k' - 1" n] 
+    with assms binomial_less_binomial_Suc[of "k' - 1" n]
       show ?case by simp
   next
     case (step k)
-    from step.prems step.hyps assms have "n choose k < n choose (Suc k)" 
+    from step.prems step.hyps assms have "n choose k < n choose (Suc k)"
       by (intro binomial_less_binomial_Suc) simp_all
     also have "\<dots> < n choose k'" by (rule step.IH)
     finally show ?case .
@@ -150,12 +150,12 @@
   proof (cases "k = n div 2 \<and> odd n")
     case False
     with assms(2) have "2*k \<ge> n" by presburger
-    with not_eq assms binomial_strict_antimono[of k k' n] 
+    with not_eq assms binomial_strict_antimono[of k k' n]
       show ?thesis by simp
   next
     case True
     have "n choose k' \<le> n choose (Suc (n div 2))"
-    proof (cases "k' = Suc (n div 2)") 
+    proof (cases "k' = Suc (n div 2)")
       case False
       with assms True not_eq have "Suc (n div 2) < k'" by simp
       with assms binomial_strict_antimono[of "Suc (n div 2)" k' n] True
@@ -191,10 +191,10 @@
     have "4 ^ n = (\<Sum>k=0..2*n. (2*n) choose k)"
     by (simp add: power_mult power2_eq_square One_nat_def [symmetric] del: One_nat_def)
   also have "{0..2*n} = {0<..<2*n} \<union> {0,2*n}" by auto
-  also have "(\<Sum>k\<in>\<dots>. (2*n) choose k) = 
+  also have "(\<Sum>k\<in>\<dots>. (2*n) choose k) =
                (\<Sum>k\<in>{0<..<2*n}. (2*n) choose k) + (\<Sum>k\<in>{0,2*n}. (2*n) choose k)"
     by (subst sum.union_disjoint) auto
-  also have "(\<Sum>k\<in>{0,2*n}. (2*n) choose k) \<le> (\<Sum>k\<le>1. (n choose k)\<^sup>2)" 
+  also have "(\<Sum>k\<in>{0,2*n}. (2*n) choose k) \<le> (\<Sum>k\<le>1. (n choose k)\<^sup>2)"
     by (cases n) simp_all
   also from assms have "\<dots> \<le> (\<Sum>k\<le>n. (n choose k)\<^sup>2)"
     by (intro sum_mono3) auto
@@ -959,7 +959,7 @@
   have summable: "summable (\<lambda>n. diffs c n * z^n)"
     by (intro termdiff_converges[OF norm] sums_summable[OF sums])
   from norm have "eventually (\<lambda>z. z \<in> norm -` {..<K}) (nhds z)"
-    by (intro eventually_nhds_in_open open_vimage) 
+    by (intro eventually_nhds_in_open open_vimage)
        (simp_all add: continuous_on_norm continuous_on_id)
   hence eq: "eventually (\<lambda>z. (\<Sum>n. c n * z^n) = f z) (nhds z)"
     by eventually_elim (insert sums, simp add: sums_iff)
diff -r d164c4fc0d2c -r f533820e7248 src/HOL/ex/LocaleTest2.thy
--- a/src/HOL/ex/LocaleTest2.thy	Sat Apr 22 12:52:55 2017 +0200
+++ b/src/HOL/ex/LocaleTest2.thy	Sat Apr 22 22:01:35 2017 +0200
@@ -11,7 +11,7 @@
 section \<open>Test of Locale Interpretation\<close>
 
 theory LocaleTest2
-imports Main GCD
+imports Main
 begin
 
 section \<open>Interpretation of Defined Concepts\<close>
diff -r d164c4fc0d2c -r f533820e7248 src/HOL/ex/Transfer_Int_Nat.thy
--- a/src/HOL/ex/Transfer_Int_Nat.thy	Sat Apr 22 12:52:55 2017 +0200
+++ b/src/HOL/ex/Transfer_Int_Nat.thy	Sat Apr 22 22:01:35 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>Using the transfer method between nat and int\<close>
 
 theory Transfer_Int_Nat
-imports GCD
+imports Main
 begin
 
 subsection \<open>Correspondence relation\<close>
@@ -15,7 +15,7 @@
 
 subsection \<open>Transfer domain rules\<close>
 
-lemma Domainp_ZN [transfer_domain_rule]: "Domainp ZN = (\<lambda>x. x \<ge> 0)" 
+lemma Domainp_ZN [transfer_domain_rule]: "Domainp ZN = (\<lambda>x. x \<ge> 0)"
   unfolding ZN_def Domainp_iff[abs_def] by (auto intro: zero_le_imp_eq_int)
 
 subsection \<open>Transfer rules\<close>
@@ -177,7 +177,7 @@
 done
 
 lemma
-  assumes "\<And>x y z::int. \<lbrakk>0 \<le> x; 0 \<le> y; 0 \<le> z\<rbrakk> \<Longrightarrow> 
+  assumes "\<And>x y z::int. \<lbrakk>0 \<le> x; 0 \<le> y; 0 \<le> z\<rbrakk> \<Longrightarrow>
     sum_list [x, y, z] = 0 \<longleftrightarrow> list_all (\<lambda>x. x = 0) [x, y, z]"
   shows "sum_list [x, y, z] = (0::nat) \<longleftrightarrow> list_all (\<lambda>x. x = 0) [x, y, z]"
 apply transfer