author haftmann Wed Feb 17 21:51:57 2016 +0100 (2016-02-17) changeset 62349 7c23469b5118 parent 62348 9a5f43dac883 child 62350 66a381d3f88f
cleansed junk-producing interpretations for gcd/lcm on nat altogether
 src/HOL/Algebra/Exponent.thy file | annotate | diff | revisions src/HOL/GCD.thy file | annotate | diff | revisions src/HOL/NSA/Examples/NSPrimes.thy file | annotate | diff | revisions src/HOL/Number_Theory/Cong.thy file | annotate | diff | revisions src/HOL/Number_Theory/Eratosthenes.thy file | annotate | diff | revisions src/HOL/Number_Theory/Pocklington.thy file | annotate | diff | revisions src/HOL/Number_Theory/Primes.thy file | annotate | diff | revisions src/HOL/Number_Theory/UniqueFactorization.thy file | annotate | diff | revisions src/HOL/Old_Number_Theory/Primes.thy file | annotate | diff | revisions src/HOL/Rings.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Algebra/Exponent.thy	Wed Feb 17 21:51:57 2016 +0100
1.2 +++ b/src/HOL/Algebra/Exponent.thy	Wed Feb 17 21:51:57 2016 +0100
1.3 @@ -21,10 +21,10 @@
1.4  text\<open>Prime Theorems\<close>
1.5
1.6  lemma prime_iff:
1.7 -  "(prime p) = (Suc 0 < p & (\<forall>a b. p dvd a*b --> (p dvd a) | (p dvd b)))"
1.8 -apply (auto simp add: prime_gt_Suc_0_nat)
1.9 -by (metis (full_types) One_nat_def Suc_lessD dvd.order_refl nat_dvd_not_less not_prime_eq_prod_nat)
1.10 -
1.11 +  "prime p \<longleftrightarrow> Suc 0 < p \<and> (\<forall>a b. p dvd a * b \<longrightarrow> p dvd a \<or> p dvd b)"
1.12 +  by (auto simp add: prime_gt_Suc_0_nat)
1.13 +    (metis One_nat_def Suc_lessD dvd_refl nat_dvd_not_less not_prime_eq_prod_nat)
1.14 +
1.15  lemma zero_less_prime_power:
1.16    fixes p::nat shows "prime p ==> 0 < p^a"
1.17  by (force simp add: prime_iff)
```
```     2.1 --- a/src/HOL/GCD.thy	Wed Feb 17 21:51:57 2016 +0100
2.2 +++ b/src/HOL/GCD.thy	Wed Feb 17 21:51:57 2016 +0100
2.3 @@ -2167,24 +2167,4 @@
2.4  lemma dvd_gcd_D2_int: "i dvd gcd m n \<Longrightarrow> (i::int) dvd n"
2.5    by (fact dvd_gcdD2)
2.6
2.7 -interpretation dvd:
2.8 -  order "op dvd" "\<lambda>n m :: nat. n dvd m \<and> m \<noteq> n"
2.9 -  by standard (auto intro: dvd_refl dvd_trans dvd_antisym)
2.10 -
2.11 -interpretation gcd_semilattice_nat:
2.12 -  semilattice_inf gcd Rings.dvd "\<lambda>m n::nat. m dvd n \<and> m \<noteq> n"
2.13 -  by standard (auto dest: dvd_antisym dvd_trans)
2.14 -
2.15 -interpretation lcm_semilattice_nat:
2.16 -  semilattice_sup lcm Rings.dvd "\<lambda>m n::nat. m dvd n \<and> m \<noteq> n"
2.17 -  by standard simp_all
2.18 -
2.19 -interpretation gcd_lcm_lattice_nat:
2.20 -  lattice gcd Rings.dvd "\<lambda>m n::nat. m dvd n \<and> m \<noteq> n" lcm
2.21 -  ..
2.22 -
2.23 -interpretation gcd_lcm_complete_lattice_nat:
2.24 -  complete_lattice Gcd Lcm gcd Rings.dvd "\<lambda>m n. m dvd n \<and> m \<noteq> n" lcm 1 "0::nat"
2.25 -  by standard (auto simp add: Gcd_nat_def Lcm_nat_empty Lcm_nat_infinite)
2.26 -
2.27  end
```
```     3.1 --- a/src/HOL/NSA/Examples/NSPrimes.thy	Wed Feb 17 21:51:57 2016 +0100
3.2 +++ b/src/HOL/NSA/Examples/NSPrimes.thy	Wed Feb 17 21:51:57 2016 +0100
3.3 @@ -27,13 +27,19 @@
3.4  | injf_max_Suc:  "injf_max (Suc n) E = choicefun({e. e:E & injf_max n E < e})"
3.5
3.6
3.7 -lemma dvd_by_all: "\<forall>M. \<exists>N. 0 < N & (\<forall>m. 0 < m & (m::nat) <= M --> m dvd N)"
3.8 -apply (rule allI)
3.9 -apply (induct_tac "M", auto)
3.10 -apply (rule_tac x = "N * (Suc n) " in exI)
3.11 -by (metis dvd.order_refl dvd_mult dvd_mult2 le_Suc_eq nat_0_less_mult_iff zero_less_Suc)
3.12 +lemma dvd_by_all2:
3.13 +  fixes M :: nat
3.14 +  shows "\<exists>N>0. \<forall>m. 0 < m \<and> m \<le> M \<longrightarrow> m dvd N"
3.15 +apply (induct M)
3.16 +apply auto
3.17 +apply (rule_tac x = "N * (Suc M) " in exI)
3.18 +apply auto
3.19 +apply (metis dvdI dvd_add_times_triv_left_iff dvd_add_triv_right_iff dvd_refl dvd_trans le_Suc_eq mult_Suc_right)
3.20 +done
3.21
3.22 -lemmas dvd_by_all2 = dvd_by_all [THEN spec]
3.23 +lemma dvd_by_all:
3.24 +  "\<forall>M::nat. \<exists>N>0. \<forall>m. 0 < m \<and> m \<le> M \<longrightarrow> m dvd N"
3.25 +  using dvd_by_all2 by blast
3.26
3.27  lemma hypnat_of_nat_le_zero_iff [simp]: "(hypnat_of_nat n <= 0) = (n = 0)"
3.28  by (transfer, simp)
3.29 @@ -256,8 +262,9 @@
3.30  lemma hdvd_diff: "!!k m n :: hypnat. [| k dvd m; k dvd n |] ==> k dvd (m - n)"
3.31  by (transfer, rule dvd_diff_nat)
3.32
3.33 -lemma hdvd_one_eq_one: "!!x. x dvd (1::hypnat) ==> x = 1"
3.34 -by (transfer, rule gcd_lcm_complete_lattice_nat.le_bot)
3.35 +lemma hdvd_one_eq_one:
3.36 +  "\<And>x::hypnat. is_unit x \<Longrightarrow> x = 1"
3.37 +  by transfer simp
3.38
3.39  text\<open>Already proved as \<open>primes_infinite\<close>, but now using non-standard naturals.\<close>
3.40  theorem not_finite_prime: "~ finite {p::nat. prime p}"
```
```     4.1 --- a/src/HOL/Number_Theory/Cong.thy	Wed Feb 17 21:51:57 2016 +0100
4.2 +++ b/src/HOL/Number_Theory/Cong.thy	Wed Feb 17 21:51:57 2016 +0100
4.3 @@ -527,13 +527,10 @@
4.4    apply (metis cong_solve_int)
4.5    done
4.6
4.7 -lemma coprime_iff_invertible_nat: "m > 0 \<Longrightarrow> coprime a m = (EX x. [a * x = Suc 0] (mod m))"
4.8 -  apply (auto intro: cong_solve_coprime_nat)
4.9 -  apply (metis cong_Suc_0_nat cong_solve_nat gcd_nat.left_neutral)
4.10 -  apply (metis One_nat_def cong_gcd_eq_nat coprime_lmult_nat
4.11 -      gcd_lcm_complete_lattice_nat.inf_bot_right gcd.commute)
4.12 -  done
4.13 -
4.14 +lemma coprime_iff_invertible_nat:
4.15 +  "m > 0 \<Longrightarrow> coprime a m = (EX x. [a * x = Suc 0] (mod m))"
4.16 +  by (metis One_nat_def cong_gcd_eq_nat cong_solve_coprime_nat coprime_lmult_nat gcd.commute gcd_Suc_0)
4.17 +
4.18  lemma coprime_iff_invertible_int: "m > (0::int) \<Longrightarrow> coprime a m = (EX x. [a * x = 1] (mod m))"
4.19    apply (auto intro: cong_solve_coprime_int)
4.20    apply (metis cong_int_def coprime_mul_eq_int gcd_1_int gcd.commute gcd_red_int)
4.21 @@ -558,7 +555,7 @@
4.22      [x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)"
4.23    apply (cases "y \<le> x")
4.24    apply (metis cong_altdef_nat lcm_least)
4.25 -  apply (metis cong_altdef_nat cong_diff_cong_0'_nat lcm_semilattice_nat.sup.bounded_iff le0 minus_nat.diff_0)
4.26 +  apply (meson cong_altdef_nat cong_sym_nat lcm_least_iff nat_le_linear)
4.27    done
4.28
4.29  lemma cong_cong_lcm_int: "[(x::int) = y] (mod a) \<Longrightarrow>
```
```     5.1 --- a/src/HOL/Number_Theory/Eratosthenes.thy	Wed Feb 17 21:51:57 2016 +0100
5.2 +++ b/src/HOL/Number_Theory/Eratosthenes.thy	Wed Feb 17 21:51:57 2016 +0100
5.3 @@ -283,7 +283,7 @@
5.4        next
5.5          case False with \<open>m \<noteq> 1\<close> have "Suc (Suc 0) \<le> m" by arith
5.6          with \<open>m < Suc n\<close> * \<open>m dvd q\<close> have "q dvd m" by simp
5.7 -        with \<open>m dvd q\<close> show ?thesis by (simp add: dvd.eq_iff)
5.8 +        with \<open>m dvd q\<close> show ?thesis by (simp add: dvd_antisym)
5.9        qed
5.10      }
5.11      then have aux: "\<And>m q. Suc (Suc 0) \<le> q \<Longrightarrow>
```
```     6.1 --- a/src/HOL/Number_Theory/Pocklington.thy	Wed Feb 17 21:51:57 2016 +0100
6.2 +++ b/src/HOL/Number_Theory/Pocklington.thy	Wed Feb 17 21:51:57 2016 +0100
6.3 @@ -11,7 +11,7 @@
6.4  subsection\<open>Lemmas about previously defined terms\<close>
6.5
6.6  lemma prime:
6.7 -  "prime p \<longleftrightarrow> p \<noteq> 0 \<and> p\<noteq>1 \<and> (\<forall>m. 0 < m \<and> m < p \<longrightarrow> coprime p m)"
6.8 +  "prime p \<longleftrightarrow> p \<noteq> 0 \<and> p \<noteq> 1 \<and> (\<forall>m. 0 < m \<and> m < p \<longrightarrow> coprime p m)"
6.9    (is "?lhs \<longleftrightarrow> ?rhs")
6.10  proof-
6.11    {assume "p=0 \<or> p=1" hence ?thesis
6.12 @@ -39,7 +39,7 @@
6.13        {assume "q\<noteq>p" with qp have qplt: "q < p" by arith
6.14          from H qplt q0 have "coprime p q" by arith
6.15         hence ?lhs using q
6.16 -         by (metis gcd_semilattice_nat.inf_absorb2 one_not_prime_nat)}
6.17 +         by (auto dest: gcd_nat.absorb2)}
6.18        ultimately have ?lhs by blast}
6.19      ultimately have ?thesis by blast}
6.20    ultimately show ?thesis  by (cases"p=0 \<or> p=1", auto)
6.21 @@ -105,16 +105,16 @@
6.22      by (metis cong_solve_unique neq0_conv p prime_gt_0_nat px)
6.23    {assume y0: "y = 0"
6.24      with y(2) have th: "p dvd a"
6.25 -      by (metis cong_dvd_eq_nat gcd_lcm_complete_lattice_nat.top_greatest mult_0_right)
6.26 +      by (auto dest: cong_dvd_eq_nat)
6.27      have False
6.28        by (metis gcd_nat.absorb1 one_not_prime_nat p pa th)}
6.29    with y show ?thesis unfolding Ex1_def using neq0_conv by blast
6.30  qed
6.31
6.32  lemma cong_unique_inverse_prime:
6.33 -  assumes p: "prime p" and x0: "0 < x" and xp: "x < p"
6.34 +  assumes "prime p" and "0 < x" and "x < p"
6.35    shows "\<exists>!y. 0 < y \<and> y < p \<and> [x * y = 1] (mod p)"
6.36 -by (metis cong_solve_unique_nontrivial gcd_lcm_complete_lattice_nat.inf_bot_left gcd.commute assms)
6.37 +  by (rule cong_solve_unique_nontrivial) (insert assms, simp_all)
6.38
6.39  lemma chinese_remainder_coprime_unique:
6.40    fixes a::nat
6.41 @@ -469,7 +469,7 @@
6.42    "prime n \<longleftrightarrow> n \<noteq> 1 \<and> (\<forall>d. d dvd n \<and> d\<^sup>2 \<le> n \<longrightarrow> d = 1)"
6.43  proof -
6.44    {assume "n=0 \<or> n=1" hence ?thesis
6.45 -    by (metis dvd.order_refl le_refl one_not_prime_nat power_zero_numeral zero_not_prime_nat)}
6.46 +    by auto}
6.47    moreover
6.48    {assume n: "n\<noteq>0" "n\<noteq>1"
6.49      hence np: "n > 1" by arith
6.50 @@ -583,9 +583,8 @@
6.51    {fix d assume d: "d dvd p" "d dvd a" "d \<noteq> 1"
6.52      from pp[unfolded prime_def] d have dp: "d = p" by blast
6.53      from n have "n \<noteq> 0" by simp
6.54 -    then have False using d
6.55 -      by (metis coprime_minus_one_nat dp lucas_coprime_lemma an coprime_nat
6.56 -           gcd_lcm_complete_lattice_nat.top_greatest pn)}
6.57 +    then have False using d dp pn
6.58 +      by auto (metis One_nat_def Suc_pred an dvd_1_iff_1 gcd_greatest_iff lucas_coprime_lemma)}
6.59    hence cpa: "coprime p a" by auto
6.60    have arp: "coprime (a^r) p"
6.61      by (metis coprime_exp_nat cpa gcd.commute)
6.62 @@ -617,9 +616,8 @@
6.63      have th: "q dvd p - 1"
6.64        by (metis cong_to_1_nat)
6.65      have "p - 1 \<noteq> 0" using prime_ge_2_nat [OF p(1)] by arith
6.66 -    with pq p have False
6.67 -      by (metis Suc_diff_1 gcd_le2_nat gcd_semilattice_nat.inf_absorb1 not_less_eq_eq
6.68 -            prime_gt_0_nat th) }
6.69 +    with pq th have False
6.70 +      by (simp add: nat_dvd_not_less)}
6.71    with n01 show ?ths by blast
6.72  qed
6.73
6.74 @@ -649,8 +647,7 @@
6.75        have "p - 1 \<noteq> 0" using prime_ge_2_nat [OF p(1)] by arith
6.76        then have pS: "Suc (p - 1) = p" by arith
6.77        from b have d: "n dvd a^((n - 1) div p)" unfolding b0
6.78 -        by (metis b0 diff_0_eq_0 gcd_dvd2 gcd_lcm_complete_lattice_nat.inf_bot_left
6.79 -                   gcd_lcm_complete_lattice_nat.inf_top_left)
6.80 +        by auto
6.81        from divides_rexp[OF d, of "p - 1"] pS eq cong_dvd_eq_nat [OF an] n
6.82        have False
6.83          by simp}
```
```     7.1 --- a/src/HOL/Number_Theory/Primes.thy	Wed Feb 17 21:51:57 2016 +0100
7.2 +++ b/src/HOL/Number_Theory/Primes.thy	Wed Feb 17 21:51:57 2016 +0100
7.3 @@ -167,14 +167,19 @@
7.4      "prime p \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
7.5    by (rule coprime_exp2_nat, rule primes_coprime_nat)
7.6
7.7 -lemma prime_factor_nat: "n \<noteq> (1::nat) \<Longrightarrow> \<exists> p. prime p \<and> p dvd n"
7.8 -  apply (induct n rule: nat_less_induct)
7.9 -  apply (case_tac "n = 0")
7.10 -  using two_is_prime_nat
7.11 -  apply blast
7.12 -  apply (metis One_nat_def dvd.order_trans dvd_refl less_Suc0 linorder_neqE_nat
7.13 -    nat_dvd_not_less neq0_conv prime_def)
7.14 -  done
7.15 +lemma prime_factor_nat:
7.16 +  "n \<noteq> (1::nat) \<Longrightarrow> \<exists>p. prime p \<and> p dvd n"
7.17 +proof (induct n rule: nat_less_induct)
7.18 +  case (1 n) show ?case
7.19 +  proof (cases "n = 0")
7.20 +    case True then show ?thesis
7.21 +    by (auto intro: two_is_prime_nat)
7.22 +  next
7.23 +    case False with "1.prems" have "n > 1" by simp
7.24 +    with "1.hyps" show ?thesis
7.25 +    by (metis One_nat_def dvd_mult dvd_refl not_prime_eq_prod_nat order_less_irrefl)
7.26 +  qed
7.27 +qed
7.28
7.29  text \<open>One property of coprimality is easier to prove via prime factors.\<close>
7.30
7.31 @@ -417,11 +422,13 @@
7.32  lemma bezout_prime:
7.33    assumes p: "prime p" and pa: "\<not> p dvd a"
7.34    shows "\<exists>x y. a*x = Suc (p*y)"
7.35 -proof-
7.36 +proof -
7.37    have ap: "coprime a p"
7.38      by (metis gcd.commute p pa prime_imp_coprime_nat)
7.39 -  from coprime_bezout_strong[OF ap] show ?thesis
7.40 -    by (metis Suc_eq_plus1 gcd_lcm_complete_lattice_nat.bot.extremum pa)
7.41 +  moreover from p have "p \<noteq> 1" by auto
7.42 +  ultimately have "\<exists>x y. a * x = p * y + 1"
7.43 +    by (rule coprime_bezout_strong)
7.44 +  then show ?thesis by simp
7.45  qed
7.46
7.47  end
```
```     8.1 --- a/src/HOL/Number_Theory/UniqueFactorization.thy	Wed Feb 17 21:51:57 2016 +0100
8.2 +++ b/src/HOL/Number_Theory/UniqueFactorization.thy	Wed Feb 17 21:51:57 2016 +0100
8.3 @@ -653,9 +653,10 @@
8.4
8.5  lemma multiplicity_dvd'_nat:
8.6    fixes x y :: nat
8.7 -  shows "0 < x \<Longrightarrow> \<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y"
8.8 -  by (metis gcd_lcm_complete_lattice_nat.top_greatest le_refl multiplicity_dvd_nat
8.9 -      multiplicity_nonprime_nat neq0_conv)
8.10 +  assumes "0 < x"
8.11 +  assumes "\<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y"
8.12 +  shows "x dvd y"
8.13 +  using dvd_0_right assms by (metis (no_types) le0 multiplicity_dvd_nat multiplicity_nonprime_nat not_gr0)
8.14
8.15  lemma multiplicity_dvd'_int:
8.16    fixes x y :: int
```
```     9.1 --- a/src/HOL/Old_Number_Theory/Primes.thy	Wed Feb 17 21:51:57 2016 +0100
9.2 +++ b/src/HOL/Old_Number_Theory/Primes.thy	Wed Feb 17 21:51:57 2016 +0100
9.3 @@ -819,11 +819,11 @@
9.4    by (auto simp add: dvd_def coprime)
9.5
9.6  lemma mult_inj_if_coprime_nat:
9.7 -  "inj_on f A \<Longrightarrow> inj_on g B \<Longrightarrow> ALL a:A. ALL b:B. coprime (f a) (g b)
9.8 -   \<Longrightarrow> inj_on (%(a,b). f a * g b::nat) (A \<times> B)"
9.9 -apply(auto simp add:inj_on_def)
9.10 -apply(metis coprime_def dvd_triv_left gcd_proj2_if_dvd_nat gcd_semilattice_nat.inf_commute relprime_dvd_mult)
9.11 -apply (metis coprime_commute coprime_divprod dvd_triv_right gcd_semilattice_nat.dual_order.strict_trans2)
9.12 +  "inj_on f A \<Longrightarrow> inj_on g B \<Longrightarrow> \<forall>a\<in>A. \<forall>b\<in>B. Primes.coprime (f a) (g b) \<Longrightarrow>
9.13 +    inj_on (\<lambda>(a, b). f a * g b) (A \<times> B)"
9.14 +apply (auto simp add: inj_on_def)
9.15 +apply (metis coprime_def dvd_antisym dvd_triv_left relprime_dvd_mult_iff)
9.16 +apply (metis coprime_commute coprime_divprod dvd_antisym dvd_triv_right)
9.17  done
9.18
9.19  declare power_Suc0[simp del]
```
```    10.1 --- a/src/HOL/Rings.thy	Wed Feb 17 21:51:57 2016 +0100
10.2 +++ b/src/HOL/Rings.thy	Wed Feb 17 21:51:57 2016 +0100
10.3 @@ -145,7 +145,7 @@
10.4    show "a = a * 1" by simp
10.5  qed
10.6
10.7 -lemma dvd_trans:
10.8 +lemma dvd_trans [trans]:
10.9    assumes "a dvd b" and "b dvd c"
10.10    shows "a dvd c"
10.11  proof -
```