author haftmann Mon Oct 09 19:10:48 2017 +0200 (19 months ago) changeset 66837 6ba663ff2b1c parent 66836 4eb431c3f974 child 66838 17989f6bc7b2
tuned proofs
 src/HOL/Computational_Algebra/Primes.thy file | annotate | diff | revisions src/HOL/Divides.thy file | annotate | diff | revisions src/HOL/Euclidean_Division.thy file | annotate | diff | revisions src/HOL/Library/Infinite_Set.thy file | annotate | diff | revisions src/HOL/Number_Theory/Cong.thy file | annotate | diff | revisions src/HOL/Number_Theory/Quadratic_Reciprocity.thy file | annotate | diff | revisions src/HOL/Number_Theory/Residues.thy file | annotate | diff | revisions
```     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.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.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.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.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
```