# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1390840732 0
# Node ID 06897ea77f7878bf6f45586a999b9dee2cea11eb
# Parent  9808f186795ce5bc695c3979cb73002557830eb3
converting to new Number_Theory

diff -r 9808f186795c -r 06897ea77f78 src/HOL/Algebra/Exponent.thy
--- a/src/HOL/Algebra/Exponent.thy	Fri Jan 24 16:54:25 2014 +0000
+++ b/src/HOL/Algebra/Exponent.thy	Mon Jan 27 16:38:52 2014 +0000
@@ -6,7 +6,7 @@
 *)
 
 theory Exponent
-imports Main "~~/src/HOL/Old_Number_Theory/Primes" "~~/src/HOL/Library/Binomial"
+imports Main "~~/src/HOL/Number_Theory/Primes" "~~/src/HOL/Number_Theory/Binomial"
 begin
 
 section {*Sylow's Theorem*}
@@ -20,31 +20,22 @@
 
 text{*Prime Theorems*}
 
-lemma prime_imp_one_less: "prime p ==> Suc 0 < p"
-by (unfold prime_def, force)
-
 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_imp_one_less)
-apply (blast dest!: prime_dvd_mult)
-apply (auto simp add: prime_def)
-apply (erule dvdE)
-apply (case_tac "k=0", simp)
-apply (drule_tac x = m in spec)
-apply (drule_tac x = k in spec)
-apply (simp add: dvd_mult_cancel1 dvd_mult_cancel2)
-done
+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)
 
-lemma zero_less_prime_power: "prime p ==> 0 < p^a"
+lemma zero_less_prime_power:
+  fixes p::nat shows "prime p ==> 0 < p^a"
 by (force simp add: prime_iff)
 
-
 lemma zero_less_card_empty: "[| finite S; S \<noteq> {} |] ==> 0 < card(S)"
 by (rule ccontr, simp)
 
 
 lemma prime_dvd_cases:
-  "[| p*k dvd m*n;  prime p |]  
+  fixes p::nat
+  shows "[| p*k dvd m*n;  prime p |]  
    ==> (\<exists>x. k dvd x*n & m = p*x) | (\<exists>y. k dvd m*y & n = p*y)"
 apply (simp add: prime_iff)
 apply (frule dvd_mult_left)
@@ -57,14 +48,13 @@
 done
 
 
-lemma prime_power_dvd_cases [rule_format (no_asm)]: "prime p
+lemma prime_power_dvd_cases [rule_format (no_asm)]: 
+fixes p::nat
+  shows "prime p
   ==> \<forall>m n. p^c dvd m*n -->  
         (\<forall>a b. a+b = Suc c --> p^a dvd m | p^b dvd n)"
 apply (induct c)
- apply clarify
- apply (case_tac "a")
-  apply simp
- apply simp
+apply (metis dvd_1_left nat_power_eq_Suc_0_iff one_is_add)
 (*inductive step*)
 apply simp
 apply clarify
@@ -88,9 +78,9 @@
 
 (*needed in this form in Sylow.ML*)
 lemma div_combine:
-  "[| prime p; ~ (p ^ (Suc r) dvd n);  p^(a+r) dvd n*k |]  
-   ==> p ^ a dvd k"
-by (drule_tac a = "Suc r" and b = a in prime_power_dvd_cases, assumption, auto)
+  fixes p::nat
+  shows "[| prime p; ~ (p ^ (Suc r) dvd n);  p^(a+r) dvd n*k |] ==> p ^ a dvd k"
+by (metis add_Suc nat_add_commute prime_power_dvd_cases)
 
 (*Lemma for power_dvd_bound*)
 lemma Suc_le_power: "Suc 0 < p ==> Suc n <= p^n"
@@ -116,14 +106,14 @@
   "[|p^k dvd n;  prime p;  0<n|] ==> k <= exponent p n"
 apply (simp add: exponent_def)
 apply (erule Greatest_le)
-apply (blast dest: prime_imp_one_less power_dvd_bound)
+apply (blast dest: prime_gt_Suc_0_nat power_dvd_bound)
 done
 
 lemma power_exponent_dvd: "s>0 ==> (p ^ exponent p s) dvd s"
 apply (simp add: exponent_def)
 apply clarify
 apply (rule_tac k = 0 in GreatestI)
-prefer 2 apply (blast dest: prime_imp_one_less power_dvd_bound, simp)
+prefer 2 apply (blast dest: prime_gt_Suc_0_nat power_dvd_bound, simp)
 done
 
 lemma power_Suc_exponent_Not_dvd:
@@ -135,9 +125,9 @@
 done
 
 lemma exponent_power_eq [simp]: "prime p ==> exponent p (p^a) = a"
-apply (simp (no_asm_simp) add: exponent_def)
+apply (simp add: exponent_def)
 apply (rule Greatest_equality, simp)
-apply (simp (no_asm_simp) add: prime_imp_one_less power_dvd_imp_le)
+apply (simp (no_asm_simp) add: prime_gt_Suc_0_nat power_dvd_imp_le)
 done
 
 lemma exponent_equalityI:
@@ -154,8 +144,7 @@
 apply (case_tac "prime p")
 apply (rule exponent_ge)
 apply (auto simp add: power_add)
-apply (blast intro: prime_imp_one_less power_exponent_dvd mult_dvd_mono)
-done
+by (metis mult_dvd_mono power_exponent_dvd)
 
 (* exponent_mult_add, opposite inclusion *)
 lemma exponent_mult_add2: "[| a > 0; b > 0 |]  
@@ -184,14 +173,20 @@
 apply (auto dest: dvd_mult_left)
 done
 
-lemma exponent_1_eq_0 [simp]: "exponent p (Suc 0) = 0"
+lemma exponent_1_eq_0 [simp]:
+  fixes p::nat
+  shows "exponent p (Suc 0) = 0"
 apply (case_tac "prime p")
-apply (auto simp add: prime_iff not_divides_exponent_0)
+apply (metis exponent_power_eq nat_power_eq_Suc_0_iff)
+apply (simp add: prime_iff not_divides_exponent_0)
 done
 
 
 text{*Main Combinatorial Argument*}
 
+lemma gcd_mult': fixes a::nat shows "gcd b (a * b) = b"
+by (simp add: mult_commute[of a b]) 
+
 lemma le_extend_mult: "[| c > 0; a <= b |] ==> a <= b * (c::nat)"
 apply (rule_tac P = "%x. x <= b * c" in subst)
 apply (rule mult_1_right)
@@ -206,7 +201,7 @@
 apply (drule less_imp_le [of a])
 apply (drule le_imp_power_dvd)
 apply (drule_tac b = "p ^ r" in dvd_trans, assumption)
-apply (metis diff_is_0_eq dvd_diffD1 gcd_dvd2 gcd_mult' gr0I le_extend_mult less_diff_conv nat_dvd_not_less nat_mult_commute not_add_less2 xt1(10))
+apply (metis diff_is_0_eq dvd_diffD1 gcd_dvd2_nat gcd_mult' gr0I le_extend_mult less_diff_conv nat_dvd_not_less nat_mult_commute not_add_less2 xt1(10))
 done
 
 lemma p_fac_forw: "[| (m::nat) > 0; k>0; k < p^a; (p^r) dvd (p^a)* m - k |]  
@@ -295,7 +290,7 @@
 (*now the hard case, simplified to
     exponent p (Suc (p ^ a * m + i - p ^ a)) = exponent p (Suc i) *)
 apply (subgoal_tac "0<p")
- prefer 2 apply (force dest!: prime_imp_one_less)
+ prefer 2 apply (force dest!: prime_gt_Suc_0_nat)
 apply (subst exponent_p_a_m_k_equation, auto)
 done
 
@@ -311,14 +306,13 @@
   transform the binomial coefficient, then use @{text exponent_mult_add}.*}
 apply (subgoal_tac "exponent p ((( (p^a) * m) choose p^a) * p^a) = 
                     a + exponent p m")
- apply (simp del: bad_Sucs add: zero_less_binomial_iff exponent_mult_add prime_iff)
+ apply (simp add: exponent_mult_add)
 txt{*one subgoal left!*}
 apply (subst times_binomial_minus1_eq, simp, simp)
 apply (subst exponent_mult_add, simp)
-apply (simp (no_asm_simp) add: zero_less_binomial_iff)
+apply (simp (no_asm_simp))
 apply arith
 apply (simp del: bad_Sucs add: exponent_mult_add const_p_fac_right)
 done
 
-
 end
diff -r 9808f186795c -r 06897ea77f78 src/HOL/Algebra/IntRing.thy
--- a/src/HOL/Algebra/IntRing.thy	Fri Jan 24 16:54:25 2014 +0000
+++ b/src/HOL/Algebra/IntRing.thy	Mon Jan 27 16:38:52 2014 +0000
@@ -4,7 +4,7 @@
 *)
 
 theory IntRing
-imports QuotRing Lattice Int "~~/src/HOL/Old_Number_Theory/Primes"
+imports QuotRing Lattice Int "~~/src/HOL/Number_Theory/Primes"
 begin
 
 section {* The Ring of Integers *}
@@ -257,9 +257,8 @@
  apply (elim exE)
 proof -
   fix a b x
-
-  from prime
-      have ppos: "0 <= p" by (simp add: prime_def)
+  have ppos: "0 <= p"
+    by (metis prime linear nat_0_iff zero_not_prime_nat)
   have unnat: "!!x. nat p dvd nat (abs x) ==> p dvd x"
   proof -
     fix x
@@ -267,19 +266,18 @@
     hence "int (nat p) dvd x" by (simp add: int_dvd_iff[symmetric])
     thus "p dvd x" by (simp add: ppos)
   qed
-
-
   assume "a * b = x * p"
   hence "p dvd a * b" by simp
   hence "nat p dvd nat (abs (a * b))" using ppos by (simp add: nat_dvd_iff)
   hence "nat p dvd (nat (abs a) * nat (abs b))" by (simp add: nat_abs_mult_distrib)
-  hence "nat p dvd nat (abs a) | nat p dvd nat (abs b)" by (rule prime_dvd_mult[OF prime])
+  hence "nat p dvd nat (abs a) | nat p dvd nat (abs b)"
+    by (metis prime prime_dvd_mult_eq_nat) 
   hence "p dvd a | p dvd b" by (fast intro: unnat)
   thus "(EX x. a = x * p) | (EX x. b = x * p)"
   proof
     assume "p dvd a"
     hence "EX x. a = p * x" by (simp add: dvd_def)
-    from this obtain x
+    then obtain x
         where "a = p * x" by fast
     hence "a = x * p" by simp
     hence "EX x. a = x * p" by simp
@@ -287,7 +285,7 @@
   next
     assume "p dvd b"
     hence "EX x. b = p * x" by (simp add: dvd_def)
-    from this obtain x
+    then obtain x
         where "b = p * x" by fast
     hence "b = x * p" by simp
     hence "EX x. b = x * p" by simp
@@ -295,14 +293,12 @@
   qed
 next
   assume "UNIV = {uu. EX x. uu = x * p}"
-  from this obtain x 
-      where "1 = x * p" by best
-  from this [symmetric]
-      have "p * x = 1" by (subst mult_commute)
+  then obtain x where "1 = x * p" by best
+  then have "p * x = 1" by (metis mult_commute)
   hence "\<bar>p * x\<bar> = 1" by simp
   hence "\<bar>p\<bar> = 1" by (rule abs_zmult_eq_1)
-  from this and prime
-      show "False" by (simp add: prime_def)
+  then  show "False" 
+    by (metis prime abs_of_pos one_not_prime_int prime_gt_0_int prime_int_def) 
 qed
 
 
@@ -355,7 +351,7 @@
 proof -
   from kIl[unfolded ZMod_def]
       have "\<exists>xl\<in>Idl\<^bsub>\<Z>\<^esub> {l}. k = xl + r" by (simp add: a_r_coset_defs)
-  from this obtain xl
+  then obtain xl
       where xl: "xl \<in> Idl\<^bsub>\<Z>\<^esub> {l}"
       and k: "k = xl + r"
       by auto
@@ -376,9 +372,9 @@
       have "b \<in> ZMod m a"
       unfolding ZMod_def
       by (simp add: a_repr_independenceD)
-  from this
+  then
       have "EX x. b = x * m + a" by (rule rcos_zfact)
-  from this obtain x
+  then obtain x
       where "b = x * m + a"
       by fast
 
diff -r 9808f186795c -r 06897ea77f78 src/HOL/Algebra/Sylow.thy
--- a/src/HOL/Algebra/Sylow.thy	Fri Jan 24 16:54:25 2014 +0000
+++ b/src/HOL/Algebra/Sylow.thy	Mon Jan 27 16:38:52 2014 +0000
@@ -72,7 +72,7 @@
 lemma (in sylow_central) exists_x_in_M1: "\<exists>x. x\<in>M1"
 apply (subgoal_tac "0 < card M1")
  apply (blast dest: card_nonempty)
-apply (cut_tac prime_p [THEN prime_imp_one_less])
+apply (cut_tac prime_p [THEN prime_gt_Suc_0_nat])
 apply (simp (no_asm_simp) add: card_M1)
 done
 
@@ -208,12 +208,11 @@
 
 lemma (in sylow_central) M1_RelM_rcosetGM1g:
      "g \<in> carrier G ==> (M1, M1 #> g) \<in> RelM"
-apply (simp (no_asm) add: RelM_def calM_def card_M1)
+apply (simp add: RelM_def calM_def card_M1)
 apply (rule conjI)
  apply (blast intro: rcosetGM1g_subset_G)
-apply (simp (no_asm_simp) add: card_M1 M1_cardeq_rcosetGM1g)
-apply (rule bexI [of _ "inv g"])
-apply (simp_all add: coset_mult_assoc)
+apply (simp add: card_M1 M1_cardeq_rcosetGM1g)
+apply (metis M1_subset_G coset_mult_assoc coset_mult_one r_inv_ex)
 done
 
 
@@ -241,10 +240,7 @@
 
 lemma (in sylow_central) M_funcset_rcosets_H:
      "(%x:M. H #> (SOME g. g \<in> carrier G & M1 #> g = x)) \<in> M \<rightarrow> rcosets H"
-apply (rule rcosetsI [THEN restrictI])
-apply (rule H_is_subgroup [THEN subgroup.subset])
-apply (erule M_elem_map_carrier)
-done
+  by (metis (lifting) H_is_subgroup M_elem_map_carrier rcosetsI restrictI subgroup_imp_subset)
 
 lemma (in sylow_central) inj_M_GmodH: "\<exists>f \<in> M\<rightarrow>rcosets H. inj_on f M"
 apply (rule bexI)
@@ -275,17 +271,11 @@
 lemmas (in sylow_central) H_elem_map_eq =
         H_elem_map [THEN someI_ex, THEN conjunct2]
 
-
-lemma EquivElemClass:
-     "[|equiv A r; M \<in> A//r; M1\<in>M; (M1,M2) \<in> r |] ==> M2 \<in> M"
-by (unfold equiv_def quotient_def sym_def trans_def, blast)
-
-
 lemma (in sylow_central) rcosets_H_funcset_M:
   "(\<lambda>C \<in> rcosets H. M1 #> (@g. g \<in> carrier G \<and> H #> g = C)) \<in> rcosets H \<rightarrow> M"
 apply (simp add: RCOSETS_def)
 apply (fast intro: someI2
-            intro!: M1_in_M EquivElemClass [OF RelM_equiv M_in_quot _  M1_RelM_rcosetGM1g])
+            intro!: M1_in_M in_quotient_imp_closed [OF RelM_equiv M_in_quot _  M1_RelM_rcosetGM1g])
 done
 
 text{*close to a duplicate of @{text inj_M_GmodH}*}
@@ -312,10 +302,7 @@
 
 
 lemma (in sylow_central) finite_M: "finite M"
-apply (rule finite_subset)
-apply (rule M_subset_calM [THEN subset_trans])
-apply (rule calM_subset_PowG, blast)
-done
+by (metis M_subset_calM finite_calM rev_finite_subset)
 
 lemma (in sylow_central) cardMeqIndexH: "card(M) = card(rcosets H)"
 apply (insert inj_M_GmodH inj_GmodH_M)