tuned proofs
authorhaftmann
Mon Oct 09 19:10:48 2017 +0200 (19 months ago)
changeset 668376ba663ff2b1c
parent 66836 4eb431c3f974
child 66838 17989f6bc7b2
tuned proofs
src/HOL/Computational_Algebra/Primes.thy
src/HOL/Divides.thy
src/HOL/Euclidean_Division.thy
src/HOL/Library/Infinite_Set.thy
src/HOL/Number_Theory/Cong.thy
src/HOL/Number_Theory/Quadratic_Reciprocity.thy
src/HOL/Number_Theory/Residues.thy
     1.1 --- a/src/HOL/Computational_Algebra/Primes.thy	Mon Oct 09 19:10:47 2017 +0200
     1.2 +++ b/src/HOL/Computational_Algebra/Primes.thy	Mon Oct 09 19:10:48 2017 +0200
     1.3 @@ -58,6 +58,9 @@
     1.4  declare [[coercion int]]
     1.5  declare [[coercion_enabled]]
     1.6  
     1.7 +lemma Suc_0_not_prime_nat [simp]: "\<not> prime (Suc 0)"
     1.8 +  using not_prime_1 [where ?'a = nat] by simp
     1.9 +
    1.10  lemma prime_elem_nat_iff:
    1.11    "prime_elem (n :: nat) \<longleftrightarrow> (1 < n \<and> (\<forall>m. m dvd n \<longrightarrow> m = 1 \<or> m = n))"
    1.12  proof safe
    1.13 @@ -97,9 +100,17 @@
    1.14  lemma prime_nat_int_transfer [simp]: "prime (int n) \<longleftrightarrow> prime n"
    1.15    by (auto simp: prime_elem_int_nat_transfer prime_def)
    1.16  
    1.17 -lemma prime_int_nat_transfer: "prime (n::int) \<longleftrightarrow> n \<ge> 0 \<and> prime (nat n)"
    1.18 +lemma prime_int_nat_transfer: "prime (k::int) \<longleftrightarrow> k \<ge> 0 \<and> prime (nat k)"
    1.19    by (auto simp: prime_elem_int_nat_transfer prime_def)
    1.20  
    1.21 +lemma prime_elem_iff_prime_abs:
    1.22 +  "prime_elem k \<longleftrightarrow> prime \<bar>k\<bar>" for k :: int
    1.23 +  by (auto intro: primeI)
    1.24 +
    1.25 +lemma prime_nat_iff_prime:
    1.26 +  "prime (nat k) \<longleftrightarrow> prime k"
    1.27 +  by (cases "k \<ge> 0") (simp_all add: prime_int_nat_transfer)
    1.28 +
    1.29  lemma prime_int_iff:
    1.30    "prime (n::int) \<longleftrightarrow> (1 < n \<and> (\<forall>m. m \<ge> 0 \<and> m dvd n \<longrightarrow> m = 1 \<or> m = n))"
    1.31  proof (intro iffI conjI allI impI; (elim conjE)?)
    1.32 @@ -259,9 +270,6 @@
    1.33  
    1.34  subsubsection \<open>Make prime naively executable\<close>
    1.35  
    1.36 -lemma Suc_0_not_prime_nat [simp]: "~prime (Suc 0)"
    1.37 -  unfolding One_nat_def [symmetric] by (rule not_prime_1)
    1.38 -
    1.39  lemma prime_nat_iff':
    1.40    "prime (p :: nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {2..<p}. ~ n dvd p)"
    1.41  proof safe
     2.1 --- a/src/HOL/Divides.thy	Mon Oct 09 19:10:47 2017 +0200
     2.2 +++ b/src/HOL/Divides.thy	Mon Oct 09 19:10:48 2017 +0200
     2.3 @@ -1164,16 +1164,40 @@
     2.4  apply (rule div_less_dividend, simp_all)
     2.5  done
     2.6  
     2.7 -lemma nat_mod_eq_lemma: assumes xyn: "(x::nat) mod n = y mod n" and xy:"y \<le> x"
     2.8 +lemma mod_eq_dvd_iff_nat:
     2.9 +  "m mod q = n mod q \<longleftrightarrow> q dvd m - n" if "m \<ge> n" for m n q :: nat
    2.10 +proof -
    2.11 +  have "int m mod int q = int n mod int q \<longleftrightarrow> int q dvd int m - int n"
    2.12 +    by (simp add: mod_eq_dvd_iff)
    2.13 +  with that have "int (m mod q) = int (n mod q) \<longleftrightarrow> int q dvd int (m - n)"
    2.14 +    by (simp only: of_nat_mod of_nat_diff)
    2.15 +  then show ?thesis
    2.16 +    by (simp add: zdvd_int)
    2.17 +qed
    2.18 +
    2.19 +lemma mod_eq_nat1E:
    2.20 +  fixes m n q :: nat
    2.21 +  assumes "m mod q = n mod q" and "m \<ge> n"
    2.22 +  obtains s where "m = n + q * s"
    2.23 +proof -
    2.24 +  from assms have "q dvd m - n"
    2.25 +    by (simp add: mod_eq_dvd_iff_nat)
    2.26 +  then obtain s where "m - n = q * s" ..
    2.27 +  with \<open>m \<ge> n\<close> have "m = n + q * s"
    2.28 +    by simp
    2.29 +  with that show thesis .
    2.30 +qed
    2.31 +
    2.32 +lemma mod_eq_nat2E:
    2.33 +  fixes m n q :: nat
    2.34 +  assumes "m mod q = n mod q" and "n \<ge> m"
    2.35 +  obtains s where "n = m + q * s"
    2.36 +  using assms mod_eq_nat1E [of n q m] by (auto simp add: ac_simps)
    2.37 +
    2.38 +lemma nat_mod_eq_lemma:
    2.39 +  assumes "(x::nat) mod n = y mod n" and "y \<le> x"
    2.40    shows "\<exists>q. x = y + n * q"
    2.41 -proof-
    2.42 -  from xy have th: "int x - int y = int (x - y)" by simp
    2.43 -  from xyn have "int x mod int n = int y mod int n"
    2.44 -    by (simp add: zmod_int [symmetric])
    2.45 -  hence "int n dvd int x - int y" by (simp only: mod_eq_dvd_iff [symmetric])
    2.46 -  hence "n dvd x - y" by (simp add: th zdvd_int)
    2.47 -  then show ?thesis using xy unfolding dvd_def apply clarsimp apply (rule_tac x="k" in exI) by arith
    2.48 -qed
    2.49 +  using assms by (rule mod_eq_nat1E) rule
    2.50  
    2.51  lemma nat_mod_eq_iff: "(x::nat) mod n = y mod n \<longleftrightarrow> (\<exists>q1 q2. x + n * q1 = y + n * q2)"
    2.52    (is "?lhs = ?rhs")
     3.1 --- a/src/HOL/Euclidean_Division.thy	Mon Oct 09 19:10:47 2017 +0200
     3.2 +++ b/src/HOL/Euclidean_Division.thy	Mon Oct 09 19:10:48 2017 +0200
     3.3 @@ -488,6 +488,18 @@
     3.4    then show ?P by simp
     3.5  qed
     3.6  
     3.7 +lemma mod_eqE:
     3.8 +  assumes "a mod c = b mod c"
     3.9 +  obtains d where "b = a + c * d"
    3.10 +proof -
    3.11 +  from assms have "c dvd a - b"
    3.12 +    by (simp add: mod_eq_dvd_iff)
    3.13 +  then obtain d where "a - b = c * d" ..
    3.14 +  then have "b = a + c * - d"
    3.15 +    by (simp add: algebra_simps)
    3.16 +  with that show thesis .
    3.17 +qed
    3.18 +
    3.19  end
    3.20  
    3.21    
     4.1 --- a/src/HOL/Library/Infinite_Set.thy	Mon Oct 09 19:10:47 2017 +0200
     4.2 +++ b/src/HOL/Library/Infinite_Set.thy	Mon Oct 09 19:10:48 2017 +0200
     4.3 @@ -64,7 +64,12 @@
     4.4  
     4.5  lemma infinite_int_iff_infinite_nat_abs: "infinite S \<longleftrightarrow> infinite ((nat \<circ> abs) ` S)"
     4.6    for S :: "int set"
     4.7 -  by (auto simp: transfer_nat_int_set_relations o_def image_comp dest: finite_image_absD)
     4.8 +proof -
     4.9 +  have "inj_on nat (abs ` A)" for A
    4.10 +    by (rule inj_onI) auto
    4.11 +  then show ?thesis
    4.12 +    by (auto simp add: image_comp [symmetric] dest: finite_image_absD finite_imageD)
    4.13 +qed
    4.14  
    4.15  proposition infinite_int_iff_unbounded_le: "infinite S \<longleftrightarrow> (\<forall>m. \<exists>n. \<bar>n\<bar> \<ge> m \<and> n \<in> S)"
    4.16    for S :: "int set"
    4.17 @@ -181,7 +186,7 @@
    4.18    by (simp_all add: MOST_Suc_iff)
    4.19  
    4.20  lemma MOST_ge_nat: "MOST n::nat. m \<le> n"
    4.21 -  by (simp add: cofinite_eq_sequentially eventually_ge_at_top)
    4.22 +  by (simp add: cofinite_eq_sequentially)
    4.23  
    4.24  (* legacy names *)
    4.25  lemma Inf_many_def: "Inf_many P \<longleftrightarrow> infinite {x. P x}" by (fact frequently_cofinite)
     5.1 --- a/src/HOL/Number_Theory/Cong.thy	Mon Oct 09 19:10:47 2017 +0200
     5.2 +++ b/src/HOL/Number_Theory/Cong.thy	Mon Oct 09 19:10:48 2017 +0200
     5.3 @@ -318,9 +318,8 @@
     5.4  
     5.5  lemma cong_iff_lin_int: "[a = b] (mod m) \<longleftrightarrow> (\<exists>k. b = a + m * k)"
     5.6    for a b :: int
     5.7 -  apply (auto simp add: cong_altdef_int dvd_def)
     5.8 -  apply (rule_tac [!] x = "-k" in exI, auto)
     5.9 -  done
    5.10 +  by (auto simp add: cong_altdef_int algebra_simps elim!: dvdE)
    5.11 +    (simp add: distrib_right [symmetric] add_eq_0_iff)
    5.12  
    5.13  lemma cong_iff_lin_nat: "([a = b] (mod m)) \<longleftrightarrow> (\<exists>k1 k2. b + k1 * m = a + k2 * m)"
    5.14    (is "?lhs = ?rhs")
    5.15 @@ -512,7 +511,7 @@
    5.16  
    5.17  lemma cong_le_nat: "y \<le> x \<Longrightarrow> [x = y] (mod n) \<longleftrightarrow> (\<exists>q. x = q * n + y)"
    5.18    for x y :: nat
    5.19 -  by (metis cong_altdef_nat Nat.le_imp_diff_is_add dvd_def mult.commute)
    5.20 +  by (auto simp add: cong_altdef_nat le_imp_diff_is_add elim!: dvdE)
    5.21  
    5.22  lemma cong_solve_nat:
    5.23    fixes a :: nat
     6.1 --- a/src/HOL/Number_Theory/Quadratic_Reciprocity.thy	Mon Oct 09 19:10:47 2017 +0200
     6.2 +++ b/src/HOL/Number_Theory/Quadratic_Reciprocity.thy	Mon Oct 09 19:10:48 2017 +0200
     6.3 @@ -46,7 +46,7 @@
     6.4    using pq_neq p_prime primes_coprime_nat q_prime by blast
     6.5  
     6.6  lemma pq_coprime_int: "coprime (int p) (int q)"
     6.7 -  using pq_coprime transfer_int_nat_gcd(1) by presburger
     6.8 +  by (simp add: gcd_int_def pq_coprime)
     6.9  
    6.10  lemma qp_ineq: "int p * k \<le> (int p * int q - 1) div 2 \<longleftrightarrow> k \<le> (int q - 1) div 2"
    6.11  proof -
     7.1 --- a/src/HOL/Number_Theory/Residues.thy	Mon Oct 09 19:10:47 2017 +0200
     7.2 +++ b/src/HOL/Number_Theory/Residues.thy	Mon Oct 09 19:10:48 2017 +0200
     7.3 @@ -222,12 +222,11 @@
     7.4  
     7.5  lemma is_field: "field R"
     7.6  proof -
     7.7 -  have "gcd x (int p) \<noteq> 1 \<Longrightarrow> 0 \<le> x \<Longrightarrow> x < int p \<Longrightarrow> x = 0" for x
     7.8 -    by (metis dual_order.order_iff_strict gcd.commute less_le_not_le p_prime prime_imp_coprime prime_nat_int_transfer zdvd_imp_le)
     7.9 +  have "0 < x \<Longrightarrow> x < int p \<Longrightarrow> coprime (int p) x" for x
    7.10 +    by (rule prime_imp_coprime) (auto simp add: zdvd_not_zless)
    7.11    then show ?thesis
    7.12 -    apply (intro cring.field_intro2 cring)
    7.13 -     apply (auto simp add: res_carrier_eq res_one_eq res_zero_eq res_units_eq)
    7.14 -    done
    7.15 +    by (intro cring.field_intro2 cring)
    7.16 +      (auto simp add: res_carrier_eq res_one_eq res_zero_eq res_units_eq ac_simps)
    7.17  qed
    7.18  
    7.19  lemma res_prime_units_eq: "Units R = {1..p - 1}"
    7.20 @@ -256,7 +255,7 @@
    7.21      by (simp_all add: m'_def)
    7.22    then have "x \<in> Units R \<longleftrightarrow> x \<in> int ` totatives m'" for x
    7.23      unfolding res_units_eq
    7.24 -    by (cases x; cases "x = m") (auto simp: totatives_def transfer_int_nat_gcd)
    7.25 +    by (cases x; cases "x = m") (auto simp: totatives_def gcd_int_def)
    7.26    then have "Units R = int ` totatives m'"
    7.27      by blast
    7.28    then have "totatives m' = nat ` Units R"
    7.29 @@ -293,7 +292,7 @@
    7.30    case False
    7.31    with assms show ?thesis
    7.32      using residues.euler_theorem [of "int m" "int a"] transfer_int_nat_cong
    7.33 -    by (auto simp add: residues_def transfer_int_nat_gcd(1)) force
    7.34 +    by (auto simp add: residues_def gcd_int_def) force
    7.35  qed
    7.36  
    7.37  lemma fermat_theorem:
    7.38 @@ -418,7 +417,7 @@
    7.39        using that \<open>p\<ge>2\<close> by force
    7.40      then show "?L \<subseteq> ?R" by blast
    7.41      have "n \<in> ?L" if "n \<in> ?R" for n
    7.42 -      using that \<open>p\<ge>2\<close> Set_Interval.transfer_nat_int_set_functions(2) by fastforce
    7.43 +      using that \<open>p\<ge>2\<close> by (auto intro: rev_image_eqI [of "int n"])
    7.44      then show "?R \<subseteq> ?L" by blast
    7.45    qed
    7.46    moreover