cleansed junk-producing interpretations for gcd/lcm on nat altogether
authorhaftmann
Wed Feb 17 21:51:57 2016 +0100 (2016-02-17)
changeset 623497c23469b5118
parent 62348 9a5f43dac883
child 62350 66a381d3f88f
cleansed junk-producing interpretations for gcd/lcm on nat altogether
src/HOL/Algebra/Exponent.thy
src/HOL/GCD.thy
src/HOL/NSA/Examples/NSPrimes.thy
src/HOL/Number_Theory/Cong.thy
src/HOL/Number_Theory/Eratosthenes.thy
src/HOL/Number_Theory/Pocklington.thy
src/HOL/Number_Theory/Primes.thy
src/HOL/Number_Theory/UniqueFactorization.thy
src/HOL/Old_Number_Theory/Primes.thy
src/HOL/Rings.thy
     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 -