--- 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
--- 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
--- 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)