theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
--- 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.
--- 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
--- 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
--- 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
--- 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
--- 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]]
--- 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
--- 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])
--- 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
--- 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
--- 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"
--- 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>
--- 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>
--- 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
--- 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 -
--- /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
--- 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"
--- 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)
--- 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
--- 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
--- 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)
--- 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>
--- 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