# 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 \Combinatorial Functions: Factorial Function, Rising Factorials, Binomial Coefficients and Binomial Theorem\ theory Binomial - imports Main + imports Pre_Main begin subsection \Factorial\ @@ -534,12 +534,12 @@ end -lemma pochhammer_nonneg: +lemma pochhammer_nonneg: fixes x :: "'a :: linordered_semidom" shows "x > 0 \ pochhammer x n \ 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 \ 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 \ 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 "\ = (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 + \ = + also have "length xs + length (y # ys) choose length xs + \ = (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 \Factorial (semi)rings\ theory Factorial_Ring -imports +imports Main - "../GCD" "~~/src/HOL/Library/Multiset" begin @@ -66,7 +65,7 @@ shows "p \ 0" using assms by (auto intro: ccontr) -lemma prime_elem_dvd_power: +lemma prime_elem_dvd_power: "prime_elem p \ p dvd x ^ n \ p dvd x" by (induction n) (auto dest: prime_elem_dvd_multD intro: dvd_trans[of _ 1]) @@ -111,7 +110,7 @@ with \irreducible p\ show False by (simp add: irreducible_not_unit) qed - + lemma unit_imp_no_prime_divisors: assumes "is_unit x" "prime_elem p" shows "\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 "\x. k dvd x * n \ 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 "\y. k dvd m*y \ n = p*y" + case 2 then obtain b where "n = p * b" by (metis dvd_mult_div_cancel) + with p pk have "\y. k dvd m*y \ 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 \ p ^ a dvd x \ p ^ b dvd n" by blast with 1 have "Suc a + b = Suc c \ p ^ Suc a dvd m \ 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 \ p ^ a dvd m \ p ^ b dvd y" by blast with 2 have "a + Suc b = Suc c \ p ^ a dvd m \ 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 "\ p dvd a" shows "p ^ n dvd b" - using \p ^ n dvd a * b\ and \n > 0\ + using \p ^ n dvd a * b\ and \n > 0\ proof (induct n arbitrary: b) case 0 then show ?case by simp next @@ -454,7 +453,7 @@ lemma prime_dvd_mult_iff: "prime p \ p dvd a * b \ p dvd a \ p dvd b" by (auto dest: prime_dvd_multD) -lemma prime_dvd_power: +lemma prime_dvd_power: "prime p \ p dvd x ^ n \ 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 \ \p dvd a \ 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 \ \p dvd a \ coprime a (p ^ m)" by (simp add: prime_elem_imp_power_coprime) @@ -625,12 +624,12 @@ proof - from ab p have "\p dvd a \ \p dvd b" by (auto simp: coprime prime_elem_def) - with p have "coprime (p^n) a \ coprime (p^n) b" + with p have "coprime (p^n) a \ 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 \ prime q \ p \ q \ coprime p q" using prime_imp_coprime primes_dvd_imp_eq by blast @@ -644,7 +643,7 @@ "x \ 0 \ \A. (\x. x \# A \ prime_elem x) \ prod_mset A = normalize x" text \Alternative characterization\ - + lemma (in normalization_semidom) factorial_semiring_altI_aux: assumes finite_divisors: "\x. x \ 0 \ finite {y. y dvd x \ normalize y = y}" assumes irreducible_imp_prime_elem: "\x. irreducible x \ 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: "\x::'a. x \ 0 \ finite {y. y dvd x \ normalize y = y}" assumes irreducible_imp_prime: "\x::'a. irreducible x \ prime_elem x" shows "OFCLASS('a :: normalization_semidom, factorial_semiring_class)" by intro_classes (rule factorial_semiring_altI_aux[OF assms]) - + text \Properties\ context factorial_semiring @@ -912,7 +911,7 @@ lemma prime_multiplicity_other: assumes "prime p" "prime q" "p \ 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 \ x \ 0 \ multiplicity p x > 0 \ p dvd x" @@ -1057,7 +1056,7 @@ also have "multiplicity p \ = 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 \ 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 \ (normalize p) = + also have "count \ (normalize p) = count (prime_factorization x) (normalize p) + count (prime_factorization y) (normalize p)" by simp - also have "\ = multiplicity p x + multiplicity p y" + also have "\ = 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) = (\x\#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 \finite A\ have "\ = (\x\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 \ 0 \ (prime_factorization x \# prime_factorization y) \ x dvd y" by (cases "y = 0") (simp_all add: prime_factorization_subset_iff_dvd) @@ -1361,7 +1360,7 @@ also have "\ = (\p \ prime_factors x. p ^ count (prime_factorization x) p)" by (subst prod_mset_multiplicity) simp_all also have "\ = (\p \ 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 = (\p\S. p ^ f p)" . also have "\ = 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 "(\p. prime p \ 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 \ = 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 \ 0 \ y \ 0 \ prime_factors (x * y) = prime_factors x \ prime_factors y" by (simp add: prime_factorization_mult) @@ -1454,7 +1453,7 @@ "(\r. p ^ r dvd a \ p ^ r dvd b) \ multiplicity p a = multiplicity p b" by (simp add: multiplicity_def) -lemma not_dvd_imp_multiplicity_0: +lemma not_dvd_imp_multiplicity_0: assumes "\p dvd x" shows "multiplicity p x = 0" proof - @@ -1740,11 +1739,11 @@ lemma assumes "x \ 0" "y \ 0" - shows gcd_eq_factorial': - "gcd x y = (\p \ prime_factors x \ prime_factors y. + shows gcd_eq_factorial': + "gcd x y = (\p \ prime_factors x \ prime_factors y. p ^ min (multiplicity p x) (multiplicity p y))" (is "_ = ?rhs1") and lcm_eq_factorial': - "lcm x y = (\p \ prime_factors x \ prime_factors y. + "lcm x y = (\p \ prime_factors x \ 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 \Greatest common divisor and least common multiple\ theory GCD - imports Main + imports Pre_Main begin subsection \Abstract bounded quasi semilattices as common foundation\ - -locale bounded_quasi_semilattice = abel_semigroup + + +locale bounded_quasi_semilattice = abel_semigroup + fixes top :: 'a ("\") and bot :: 'a ("\") and normalize :: "'a \ 'a" assumes idem_normalize [simp]: "a \<^bold>* a = normalize a" @@ -65,7 +65,7 @@ lemma top_right_normalize [simp]: "a \<^bold>* \ = normalize a" using top_left_normalize [of a] by (simp add: ac_simps) - + lemma bottom_right_bottom [simp]: "a \<^bold>* \ = \" 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 \ A" shows "F B \<^bold>* F A = F A" using assms by (simp add: union [symmetric] Un_absorb1) - + end subsection \Abstract GCD and LCM\ @@ -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 \An aside: GCD and LCM on finite sets for incomplete gcd rings\ context semiring_gcd @@ -1546,15 +1546,15 @@ abbreviation lcm_list :: "'a list \ 'a" where "lcm_list xs \ Lcm\<^sub>f\<^sub>i\<^sub>n (set xs)" - + lemma Gcd_fin_dvd: "a \ A \ 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 \ A \ 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 \ (\a\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 \ (\a\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 \Basis for universal domain\ subsubsection \Basis datatype\ @@ -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 (\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 \Importer machinery and required theorems\ 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 \Implementation of integer numbers by target-language integers\ 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 \ integer_of_num" - by transfer (simp add: fun_eq_iff) + by transfer (simp add: fun_eq_iff) lemma [code]: "Int.Neg = int_of_integer \ uminus \ 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 \ 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 \Permutations, both general and specifically on finite sets.\ theory Permutations - imports Binomial Multiset Disjoint_Sets + imports Multiset Disjoint_Sets begin subsection \Transpositions\ 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 \Stirling numbers of first and second kind\ theory Stirling -imports Binomial +imports Main begin subsection \Stirling numbers of the second kind\ 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 \Main HOL\ - -theory Main -imports Predicate_Compile Quickcheck_Narrowing Extraction Nitpick BNF_Greatest_Fixpoint Filter Conditionally_Complete_Lattices -begin - -text \ - Classical Higher-order Logic -- only ``Main'', excluding real and - complex numbers etc. -\ - -no_notation - bot ("\") and - top ("\") and - inf (infixl "\" 70) and - sup (infixl "\" 65) and - Inf ("\_" [900] 900) and - Sup ("\_" [900] 900) and - ordLeq2 (infix "<=o" 50) and - ordLeq3 (infix "\o" 50) and - ordLess2 (infix "(_,/ _)\") - -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 \ 'b \ 'b" ("(3\_./ _)" [0, 10] 10) - "_INF" :: "pttrn \ 'a set \ 'b \ 'b" ("(3\_\_./ _)" [0, 0, 10] 10) - "_SUP1" :: "pttrns \ 'b \ 'b" ("(3\_./ _)" [0, 10] 10) - "_SUP" :: "pttrn \ 'a set \ 'b \ 'b" ("(3\_\_./ _)" [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 \Nth Roots of Real Numbers\ theory NthRoot - imports Deriv Binomial + imports Deriv begin @@ -469,7 +469,7 @@ lemma real_less_rsqrt: "x\<^sup>2 < y \ 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 \ 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 \Main HOL\ + +theory Pre_Main +imports Predicate_Compile Quickcheck_Narrowing Extraction Nitpick BNF_Greatest_Fixpoint Filter Conditionally_Complete_Lattices +begin + +text \ + Classical Higher-order Logic -- only ``Main'', excluding real and + complex numbers etc. +\ + +no_notation + bot ("\") and + top ("\") and + inf (infixl "\" 70) and + sup (infixl "\" 65) and + Inf ("\_" [900] 900) and + Sup ("\_" [900] 900) and + ordLeq2 (infix "<=o" 50) and + ordLeq3 (infix "\o" 50) and + ordLess2 (infix "(_,/ _)\") + +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 \ 'b \ 'b" ("(3\_./ _)" [0, 10] 10) + "_INF" :: "pttrn \ 'a set \ 'b \ 'b" ("(3\_\_./ _)" [0, 0, 10] 10) + "_SUP1" :: "pttrns \ 'b \ 'b" ("(3\_./ _)" [0, 10] 10) + "_SUP" :: "pttrn \ 'a set \ 'b \ 'b" ("(3\_\_./ _)" [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 \Rational numbers\ theory Rat - imports GCD Archimedean_Field + imports Archimedean_Field begin subsection \Rational numbers as quotient\ @@ -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) \ 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 \Power Series, Transcendental Functions etc.\ theory Transcendental -imports Binomial Series Deriv NthRoot +imports Series Deriv NthRoot begin text \A fact theorem on reals.\ @@ -74,7 +74,7 @@ subsection \More facts about binomial coefficients\ text \ - 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. \ @@ -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 "\ < n choose k'" by (rule step.IH) finally show ?case . @@ -150,12 +150,12 @@ proof (cases "k = n div 2 \ odd n") case False with assms(2) have "2*k \ 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' \ 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 = (\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} \ {0,2*n}" by auto - also have "(\k\\. (2*n) choose k) = + also have "(\k\\. (2*n) choose k) = (\k\{0<..<2*n}. (2*n) choose k) + (\k\{0,2*n}. (2*n) choose k)" by (subst sum.union_disjoint) auto - also have "(\k\{0,2*n}. (2*n) choose k) \ (\k\1. (n choose k)\<^sup>2)" + also have "(\k\{0,2*n}. (2*n) choose k) \ (\k\1. (n choose k)\<^sup>2)" by (cases n) simp_all also from assms have "\ \ (\k\n. (n choose k)\<^sup>2)" by (intro sum_mono3) auto @@ -959,7 +959,7 @@ have summable: "summable (\n. diffs c n * z^n)" by (intro termdiff_converges[OF norm] sums_summable[OF sums]) from norm have "eventually (\z. z \ norm -` {..z. (\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 \Test of Locale Interpretation\ theory LocaleTest2 -imports Main GCD +imports Main begin section \Interpretation of Defined Concepts\ 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 \Using the transfer method between nat and int\ theory Transfer_Int_Nat -imports GCD +imports Main begin subsection \Correspondence relation\ @@ -15,7 +15,7 @@ subsection \Transfer domain rules\ -lemma Domainp_ZN [transfer_domain_rule]: "Domainp ZN = (\x. x \ 0)" +lemma Domainp_ZN [transfer_domain_rule]: "Domainp ZN = (\x. x \ 0)" unfolding ZN_def Domainp_iff[abs_def] by (auto intro: zero_le_imp_eq_int) subsection \Transfer rules\ @@ -177,7 +177,7 @@ done lemma - assumes "\x y z::int. \0 \ x; 0 \ y; 0 \ z\ \ + assumes "\x y z::int. \0 \ x; 0 \ y; 0 \ z\ \ sum_list [x, y, z] = 0 \ list_all (\x. x = 0) [x, y, z]" shows "sum_list [x, y, z] = (0::nat) \ list_all (\x. x = 0) [x, y, z]" apply transfer