# HG changeset patch
# User haftmann
# Date 1455742317 -3600
# Node ID 7c23469b5118361891d3143c3679f033dbe29fa9
# Parent  9a5f43dac883ac41532c5d8407299786284b78e0
cleansed junk-producing interpretations for gcd/lcm on nat altogether

diff -r 9a5f43dac883 -r 7c23469b5118 src/HOL/Algebra/Exponent.thy
--- a/src/HOL/Algebra/Exponent.thy	Wed Feb 17 21:51:57 2016 +0100
+++ b/src/HOL/Algebra/Exponent.thy	Wed Feb 17 21:51:57 2016 +0100
@@ -21,10 +21,10 @@
 text\<open>Prime Theorems\<close>
 
 lemma prime_iff:
-  "(prime p) = (Suc 0 < p & (\<forall>a b. p dvd a*b --> (p dvd a) | (p dvd b)))"
-apply (auto simp add: prime_gt_Suc_0_nat)
-by (metis (full_types) One_nat_def Suc_lessD dvd.order_refl nat_dvd_not_less not_prime_eq_prod_nat)
-
+  "prime p \<longleftrightarrow> Suc 0 < p \<and> (\<forall>a b. p dvd a * b \<longrightarrow> p dvd a \<or> p dvd b)"
+  by (auto simp add: prime_gt_Suc_0_nat)
+    (metis One_nat_def Suc_lessD dvd_refl nat_dvd_not_less not_prime_eq_prod_nat)
+  
 lemma zero_less_prime_power:
   fixes p::nat shows "prime p ==> 0 < p^a"
 by (force simp add: prime_iff)
diff -r 9a5f43dac883 -r 7c23469b5118 src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Wed Feb 17 21:51:57 2016 +0100
+++ b/src/HOL/GCD.thy	Wed Feb 17 21:51:57 2016 +0100
@@ -2167,24 +2167,4 @@
 lemma dvd_gcd_D2_int: "i dvd gcd m n \<Longrightarrow> (i::int) dvd n"
   by (fact dvd_gcdD2)
 
-interpretation dvd:
-  order "op dvd" "\<lambda>n m :: nat. n dvd m \<and> m \<noteq> n"
-  by standard (auto intro: dvd_refl dvd_trans dvd_antisym)
-
-interpretation gcd_semilattice_nat:
-  semilattice_inf gcd Rings.dvd "\<lambda>m n::nat. m dvd n \<and> m \<noteq> n"
-  by standard (auto dest: dvd_antisym dvd_trans)
-
-interpretation lcm_semilattice_nat:
-  semilattice_sup lcm Rings.dvd "\<lambda>m n::nat. m dvd n \<and> m \<noteq> n"
-  by standard simp_all
-
-interpretation gcd_lcm_lattice_nat:
-  lattice gcd Rings.dvd "\<lambda>m n::nat. m dvd n \<and> m \<noteq> n" lcm
-  ..
-
-interpretation gcd_lcm_complete_lattice_nat:
-  complete_lattice Gcd Lcm gcd Rings.dvd "\<lambda>m n. m dvd n \<and> m \<noteq> n" lcm 1 "0::nat"
-  by standard (auto simp add: Gcd_nat_def Lcm_nat_empty Lcm_nat_infinite)
-
 end
diff -r 9a5f43dac883 -r 7c23469b5118 src/HOL/NSA/Examples/NSPrimes.thy
--- a/src/HOL/NSA/Examples/NSPrimes.thy	Wed Feb 17 21:51:57 2016 +0100
+++ b/src/HOL/NSA/Examples/NSPrimes.thy	Wed Feb 17 21:51:57 2016 +0100
@@ -27,13 +27,19 @@
 | injf_max_Suc:  "injf_max (Suc n) E = choicefun({e. e:E & injf_max n E < e})"
 
 
-lemma dvd_by_all: "\<forall>M. \<exists>N. 0 < N & (\<forall>m. 0 < m & (m::nat) <= M --> m dvd N)"
-apply (rule allI)
-apply (induct_tac "M", auto)
-apply (rule_tac x = "N * (Suc n) " in exI)
-by (metis dvd.order_refl dvd_mult dvd_mult2 le_Suc_eq nat_0_less_mult_iff zero_less_Suc)
+lemma dvd_by_all2:
+  fixes M :: nat
+  shows "\<exists>N>0. \<forall>m. 0 < m \<and> m \<le> M \<longrightarrow> m dvd N"
+apply (induct M)
+apply auto
+apply (rule_tac x = "N * (Suc M) " in exI)
+apply auto
+apply (metis dvdI dvd_add_times_triv_left_iff dvd_add_triv_right_iff dvd_refl dvd_trans le_Suc_eq mult_Suc_right)
+done
 
-lemmas dvd_by_all2 = dvd_by_all [THEN spec]
+lemma dvd_by_all:
+  "\<forall>M::nat. \<exists>N>0. \<forall>m. 0 < m \<and> m \<le> M \<longrightarrow> m dvd N"
+  using dvd_by_all2 by blast
 
 lemma hypnat_of_nat_le_zero_iff [simp]: "(hypnat_of_nat n <= 0) = (n = 0)"
 by (transfer, simp)
@@ -256,8 +262,9 @@
 lemma hdvd_diff: "!!k m n :: hypnat. [| k dvd m; k dvd n |] ==> k dvd (m - n)"
 by (transfer, rule dvd_diff_nat)
 
-lemma hdvd_one_eq_one: "!!x. x dvd (1::hypnat) ==> x = 1"
-by (transfer, rule gcd_lcm_complete_lattice_nat.le_bot)
+lemma hdvd_one_eq_one:
+  "\<And>x::hypnat. is_unit x \<Longrightarrow> x = 1"
+  by transfer simp
 
 text\<open>Already proved as \<open>primes_infinite\<close>, but now using non-standard naturals.\<close>
 theorem not_finite_prime: "~ finite {p::nat. prime p}"
diff -r 9a5f43dac883 -r 7c23469b5118 src/HOL/Number_Theory/Cong.thy
--- a/src/HOL/Number_Theory/Cong.thy	Wed Feb 17 21:51:57 2016 +0100
+++ b/src/HOL/Number_Theory/Cong.thy	Wed Feb 17 21:51:57 2016 +0100
@@ -527,13 +527,10 @@
   apply (metis cong_solve_int)
   done
 
-lemma coprime_iff_invertible_nat: "m > 0 \<Longrightarrow> coprime a m = (EX x. [a * x = Suc 0] (mod m))"
-  apply (auto intro: cong_solve_coprime_nat)
-  apply (metis cong_Suc_0_nat cong_solve_nat gcd_nat.left_neutral)
-  apply (metis One_nat_def cong_gcd_eq_nat coprime_lmult_nat 
-      gcd_lcm_complete_lattice_nat.inf_bot_right gcd.commute)
-  done
-
+lemma coprime_iff_invertible_nat:
+  "m > 0 \<Longrightarrow> coprime a m = (EX x. [a * x = Suc 0] (mod m))"
+  by (metis One_nat_def cong_gcd_eq_nat cong_solve_coprime_nat coprime_lmult_nat gcd.commute gcd_Suc_0)
+  
 lemma coprime_iff_invertible_int: "m > (0::int) \<Longrightarrow> coprime a m = (EX x. [a * x = 1] (mod m))"
   apply (auto intro: cong_solve_coprime_int)
   apply (metis cong_int_def coprime_mul_eq_int gcd_1_int gcd.commute gcd_red_int)
@@ -558,7 +555,7 @@
     [x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)"
   apply (cases "y \<le> x")
   apply (metis cong_altdef_nat lcm_least)
-  apply (metis cong_altdef_nat cong_diff_cong_0'_nat lcm_semilattice_nat.sup.bounded_iff le0 minus_nat.diff_0)
+  apply (meson cong_altdef_nat cong_sym_nat lcm_least_iff nat_le_linear)
   done
 
 lemma cong_cong_lcm_int: "[(x::int) = y] (mod a) \<Longrightarrow>
diff -r 9a5f43dac883 -r 7c23469b5118 src/HOL/Number_Theory/Eratosthenes.thy
--- a/src/HOL/Number_Theory/Eratosthenes.thy	Wed Feb 17 21:51:57 2016 +0100
+++ b/src/HOL/Number_Theory/Eratosthenes.thy	Wed Feb 17 21:51:57 2016 +0100
@@ -283,7 +283,7 @@
       next
         case False with \<open>m \<noteq> 1\<close> have "Suc (Suc 0) \<le> m" by arith
         with \<open>m < Suc n\<close> * \<open>m dvd q\<close> have "q dvd m" by simp
-        with \<open>m dvd q\<close> show ?thesis by (simp add: dvd.eq_iff)
+        with \<open>m dvd q\<close> show ?thesis by (simp add: dvd_antisym)
       qed
     }
     then have aux: "\<And>m q. Suc (Suc 0) \<le> q \<Longrightarrow>
diff -r 9a5f43dac883 -r 7c23469b5118 src/HOL/Number_Theory/Pocklington.thy
--- a/src/HOL/Number_Theory/Pocklington.thy	Wed Feb 17 21:51:57 2016 +0100
+++ b/src/HOL/Number_Theory/Pocklington.thy	Wed Feb 17 21:51:57 2016 +0100
@@ -11,7 +11,7 @@
 subsection\<open>Lemmas about previously defined terms\<close>
 
 lemma prime: 
-  "prime p \<longleftrightarrow> p \<noteq> 0 \<and> p\<noteq>1 \<and> (\<forall>m. 0 < m \<and> m < p \<longrightarrow> coprime p m)"
+  "prime p \<longleftrightarrow> p \<noteq> 0 \<and> p \<noteq> 1 \<and> (\<forall>m. 0 < m \<and> m < p \<longrightarrow> coprime p m)"
   (is "?lhs \<longleftrightarrow> ?rhs")
 proof-
   {assume "p=0 \<or> p=1" hence ?thesis
@@ -39,7 +39,7 @@
       {assume "q\<noteq>p" with qp have qplt: "q < p" by arith
         from H qplt q0 have "coprime p q" by arith
        hence ?lhs using q
-         by (metis gcd_semilattice_nat.inf_absorb2 one_not_prime_nat)}
+         by (auto dest: gcd_nat.absorb2)}
       ultimately have ?lhs by blast}
     ultimately have ?thesis by blast}
   ultimately show ?thesis  by (cases"p=0 \<or> p=1", auto)
@@ -105,16 +105,16 @@
     by (metis cong_solve_unique neq0_conv p prime_gt_0_nat px)
   {assume y0: "y = 0"
     with y(2) have th: "p dvd a"
-      by (metis cong_dvd_eq_nat gcd_lcm_complete_lattice_nat.top_greatest mult_0_right) 
+      by (auto dest: cong_dvd_eq_nat)
     have False
       by (metis gcd_nat.absorb1 one_not_prime_nat p pa th)}
   with y show ?thesis unfolding Ex1_def using neq0_conv by blast
 qed
 
 lemma cong_unique_inverse_prime:
-  assumes p: "prime p" and x0: "0 < x" and xp: "x < p"
+  assumes "prime p" and "0 < x" and "x < p"
   shows "\<exists>!y. 0 < y \<and> y < p \<and> [x * y = 1] (mod p)"
-by (metis cong_solve_unique_nontrivial gcd_lcm_complete_lattice_nat.inf_bot_left gcd.commute assms) 
+  by (rule cong_solve_unique_nontrivial) (insert assms, simp_all)
 
 lemma chinese_remainder_coprime_unique:
   fixes a::nat 
@@ -469,7 +469,7 @@
   "prime n \<longleftrightarrow> n \<noteq> 1 \<and> (\<forall>d. d dvd n \<and> d\<^sup>2 \<le> n \<longrightarrow> d = 1)"
 proof -
   {assume "n=0 \<or> n=1" hence ?thesis
-    by (metis dvd.order_refl le_refl one_not_prime_nat power_zero_numeral zero_not_prime_nat)}
+    by auto}
   moreover
   {assume n: "n\<noteq>0" "n\<noteq>1"
     hence np: "n > 1" by arith
@@ -583,9 +583,8 @@
   {fix d assume d: "d dvd p" "d dvd a" "d \<noteq> 1"
     from pp[unfolded prime_def] d have dp: "d = p" by blast
     from n have "n \<noteq> 0" by simp
-    then have False using d
-      by (metis coprime_minus_one_nat dp lucas_coprime_lemma an coprime_nat 
-           gcd_lcm_complete_lattice_nat.top_greatest pn)} 
+    then have False using d dp pn
+      by auto (metis One_nat_def Suc_pred an dvd_1_iff_1 gcd_greatest_iff lucas_coprime_lemma)} 
   hence cpa: "coprime p a" by auto
   have arp: "coprime (a^r) p"
     by (metis coprime_exp_nat cpa gcd.commute) 
@@ -617,9 +616,8 @@
     have th: "q dvd p - 1"
       by (metis cong_to_1_nat) 
     have "p - 1 \<noteq> 0" using prime_ge_2_nat [OF p(1)] by arith
-    with pq p have False
-      by (metis Suc_diff_1 gcd_le2_nat gcd_semilattice_nat.inf_absorb1 not_less_eq_eq
-            prime_gt_0_nat th) }
+    with pq th have False
+      by (simp add: nat_dvd_not_less)}
   with n01 show ?ths by blast
 qed
 
@@ -649,8 +647,7 @@
       have "p - 1 \<noteq> 0" using prime_ge_2_nat [OF p(1)] by arith
       then have pS: "Suc (p - 1) = p" by arith
       from b have d: "n dvd a^((n - 1) div p)" unfolding b0
-        by (metis b0 diff_0_eq_0 gcd_dvd2 gcd_lcm_complete_lattice_nat.inf_bot_left 
-                   gcd_lcm_complete_lattice_nat.inf_top_left) 
+        by auto
       from divides_rexp[OF d, of "p - 1"] pS eq cong_dvd_eq_nat [OF an] n
       have False
         by simp}
diff -r 9a5f43dac883 -r 7c23469b5118 src/HOL/Number_Theory/Primes.thy
--- a/src/HOL/Number_Theory/Primes.thy	Wed Feb 17 21:51:57 2016 +0100
+++ b/src/HOL/Number_Theory/Primes.thy	Wed Feb 17 21:51:57 2016 +0100
@@ -167,14 +167,19 @@
     "prime p \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
   by (rule coprime_exp2_nat, rule primes_coprime_nat)
 
-lemma prime_factor_nat: "n \<noteq> (1::nat) \<Longrightarrow> \<exists> p. prime p \<and> p dvd n"
-  apply (induct n rule: nat_less_induct)
-  apply (case_tac "n = 0")
-  using two_is_prime_nat
-  apply blast
-  apply (metis One_nat_def dvd.order_trans dvd_refl less_Suc0 linorder_neqE_nat
-    nat_dvd_not_less neq0_conv prime_def)
-  done
+lemma prime_factor_nat:
+  "n \<noteq> (1::nat) \<Longrightarrow> \<exists>p. prime p \<and> p dvd n"
+proof (induct n rule: nat_less_induct)
+  case (1 n) show ?case
+  proof (cases "n = 0")
+    case True then show ?thesis
+    by (auto intro: two_is_prime_nat)
+  next
+    case False with "1.prems" have "n > 1" by simp
+    with "1.hyps" show ?thesis
+    by (metis One_nat_def dvd_mult dvd_refl not_prime_eq_prod_nat order_less_irrefl)
+  qed
+qed
 
 text \<open>One property of coprimality is easier to prove via prime factors.\<close>
 
@@ -417,11 +422,13 @@
 lemma bezout_prime:
   assumes p: "prime p" and pa: "\<not> p dvd a"
   shows "\<exists>x y. a*x = Suc (p*y)"
-proof-
+proof -
   have ap: "coprime a p"
     by (metis gcd.commute p pa prime_imp_coprime_nat)
-  from coprime_bezout_strong[OF ap] show ?thesis
-    by (metis Suc_eq_plus1 gcd_lcm_complete_lattice_nat.bot.extremum pa)
+  moreover from p have "p \<noteq> 1" by auto
+  ultimately have "\<exists>x y. a * x = p * y + 1"
+    by (rule coprime_bezout_strong)
+  then show ?thesis by simp    
 qed
 
 end
diff -r 9a5f43dac883 -r 7c23469b5118 src/HOL/Number_Theory/UniqueFactorization.thy
--- a/src/HOL/Number_Theory/UniqueFactorization.thy	Wed Feb 17 21:51:57 2016 +0100
+++ b/src/HOL/Number_Theory/UniqueFactorization.thy	Wed Feb 17 21:51:57 2016 +0100
@@ -653,9 +653,10 @@
 
 lemma multiplicity_dvd'_nat:
   fixes x y :: nat
-  shows "0 < x \<Longrightarrow> \<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y"
-  by (metis gcd_lcm_complete_lattice_nat.top_greatest le_refl multiplicity_dvd_nat
-      multiplicity_nonprime_nat neq0_conv)
+  assumes "0 < x"
+  assumes "\<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y"
+  shows "x dvd y"
+  using dvd_0_right assms by (metis (no_types) le0 multiplicity_dvd_nat multiplicity_nonprime_nat not_gr0)
 
 lemma multiplicity_dvd'_int:
   fixes x y :: int
diff -r 9a5f43dac883 -r 7c23469b5118 src/HOL/Old_Number_Theory/Primes.thy
--- a/src/HOL/Old_Number_Theory/Primes.thy	Wed Feb 17 21:51:57 2016 +0100
+++ b/src/HOL/Old_Number_Theory/Primes.thy	Wed Feb 17 21:51:57 2016 +0100
@@ -819,11 +819,11 @@
   by (auto simp add: dvd_def coprime)
 
 lemma mult_inj_if_coprime_nat:
-  "inj_on f A \<Longrightarrow> inj_on g B \<Longrightarrow> ALL a:A. ALL b:B. coprime (f a) (g b)
-   \<Longrightarrow> inj_on (%(a,b). f a * g b::nat) (A \<times> B)"
-apply(auto simp add:inj_on_def)
-apply(metis coprime_def dvd_triv_left gcd_proj2_if_dvd_nat gcd_semilattice_nat.inf_commute relprime_dvd_mult)
-apply (metis coprime_commute coprime_divprod dvd_triv_right gcd_semilattice_nat.dual_order.strict_trans2)
+  "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>
+    inj_on (\<lambda>(a, b). f a * g b) (A \<times> B)"
+apply (auto simp add: inj_on_def)
+apply (metis coprime_def dvd_antisym dvd_triv_left relprime_dvd_mult_iff)
+apply (metis coprime_commute coprime_divprod dvd_antisym dvd_triv_right)
 done
 
 declare power_Suc0[simp del]
diff -r 9a5f43dac883 -r 7c23469b5118 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Wed Feb 17 21:51:57 2016 +0100
+++ b/src/HOL/Rings.thy	Wed Feb 17 21:51:57 2016 +0100
@@ -145,7 +145,7 @@
   show "a = a * 1" by simp
 qed
 
-lemma dvd_trans:
+lemma dvd_trans [trans]:
   assumes "a dvd b" and "b dvd c"
   shows "a dvd c"
 proof -