--- a/src/HOL/Algebra/Sylow.thy Thu Jan 13 21:50:13 2011 +0100
+++ b/src/HOL/Algebra/Sylow.thy Thu Jan 13 23:50:16 2011 +0100
@@ -32,8 +32,7 @@
assume "y \<in> calM"
and g: "g \<in> carrier G"
hence "y = y #> g #> (inv g)" by (simp add: coset_mult_assoc calM_def)
- thus "\<exists>g'\<in>carrier G. y = y #> g #> g'"
- by (blast intro: g inv_closed)
+ thus "\<exists>g'\<in>carrier G. y = y #> g #> g'" by (blast intro: g)
qed
lemma (in sylow) RelM_trans: "trans RelM"
@@ -121,7 +120,7 @@
lemma (in sylow) zero_less_o_G: "0 < order(G)"
apply (unfold order_def)
-apply (blast intro: one_closed zero_less_card_empty)
+apply (blast intro: zero_less_card_empty)
done
lemma (in sylow) zero_less_m: "m > 0"
@@ -169,7 +168,7 @@
lemma (in sylow_central) H_m_closed: "[| x\<in>H; y\<in>H|] ==> x \<otimes> y \<in> H"
apply (unfold H_def)
-apply (simp add: coset_mult_assoc [symmetric] m_closed)
+apply (simp add: coset_mult_assoc [symmetric])
done
lemma (in sylow_central) H_not_empty: "H \<noteq> {}"
@@ -205,16 +204,16 @@
lemma (in sylow_central) M1_cardeq_rcosetGM1g:
"g \<in> carrier G ==> card(M1 #> g) = card(M1)"
-by (simp (no_asm_simp) add: M1_subset_G card_cosets_equal rcosetsI)
+by (simp (no_asm_simp) add: card_cosets_equal rcosetsI)
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 M1_subset_G)
+apply (simp (no_asm) 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 M1_subset_G)
+apply (simp_all add: coset_mult_assoc)
done
@@ -259,7 +258,7 @@
apply (rule_tac [2] M1_subset_G)
apply (rule coset_join1 [THEN in_H_imp_eq])
apply (rule_tac [3] H_is_subgroup)
-prefer 2 apply (blast intro: m_closed M_elem_map_carrier inv_closed)
+prefer 2 apply (blast intro: M_elem_map_carrier)
apply (simp add: coset_mult_inv2 H_def M_elem_map_carrier subset_eq)
done
@@ -286,8 +285,7 @@
"(\<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!: restrictI M1_in_M
- EquivElemClass [OF RelM_equiv M_in_quot _ M1_RelM_rcosetGM1g])
+ intro!: M1_in_M EquivElemClass [OF RelM_equiv M_in_quot _ M1_RelM_rcosetGM1g])
done
text{*close to a duplicate of @{text inj_M_GmodH}*}
@@ -304,9 +302,9 @@
apply (erule_tac [2] H_elem_map_carrier)+
apply (rule_tac [2] H_is_subgroup [THEN subgroup.subset])
apply (rule coset_join2)
-apply (blast intro: m_closed inv_closed H_elem_map_carrier)
+apply (blast intro: H_elem_map_carrier)
apply (rule H_is_subgroup)
-apply (simp add: H_I coset_mult_inv2 M1_subset_G H_elem_map_carrier)
+apply (simp add: H_I coset_mult_inv2 H_elem_map_carrier)
done
lemma (in sylow_central) calM_subset_PowG: "calM \<subseteq> Pow(carrier G)"
@@ -352,7 +350,7 @@
apply (frule existsM1inM, clarify)
apply (subgoal_tac "sylow_central G p a m M1 M")
apply (blast dest: sylow_central.H_is_subgroup sylow_central.card_H_eq)
-apply (simp add: sylow_central_def sylow_central_axioms_def prems)
+apply (simp add: sylow_central_def sylow_central_axioms_def sylow_axioms calM_def RelM_def)
done
text{*Needed because the locale's automatic definition refers to
--- a/src/HOL/Metis_Examples/BigO.thy Thu Jan 13 21:50:13 2011 +0100
+++ b/src/HOL/Metis_Examples/BigO.thy Thu Jan 13 23:50:16 2011 +0100
@@ -437,11 +437,11 @@
lemma bigo_mult5: "ALL x. f x ~= 0 ==>
O(f * g) <= (f::'a => ('b::linordered_field)) *o O(g)"
proof -
- assume "ALL x. f x ~= 0"
+ assume a: "ALL x. f x ~= 0"
show "O(f * g) <= f *o O(g)"
proof
fix h
- assume "h : O(f * g)"
+ assume h: "h : O(f * g)"
then have "(%x. 1 / (f x)) * h : (%x. 1 / f x) *o O(f * g)"
by auto
also have "... <= O((%x. 1 / f x) * (f * g))"
@@ -449,7 +449,7 @@
also have "(%x. 1 / f x) * (f * g) = g"
apply (simp add: func_times)
apply (rule ext)
- apply (simp add: prems nonzero_divide_eq_eq mult_ac)
+ apply (simp add: a h nonzero_divide_eq_eq mult_ac)
done
finally have "(%x. (1::'b) / f x) * h : O(g)".
then have "f * ((%x. (1::'b) / f x) * h) : f *o O(g)"
@@ -457,7 +457,7 @@
also have "f * ((%x. (1::'b) / f x) * h) = h"
apply (simp add: func_times)
apply (rule ext)
- apply (simp add: prems nonzero_divide_eq_eq mult_ac)
+ apply (simp add: a h nonzero_divide_eq_eq mult_ac)
done
finally show "h : f *o O(g)".
qed
--- a/src/HOL/MicroJava/DFA/Err.thy Thu Jan 13 21:50:13 2011 +0100
+++ b/src/HOL/MicroJava/DFA/Err.thy Thu Jan 13 23:50:16 2011 +0100
@@ -259,7 +259,7 @@
\<lbrakk> semilat (A,r,f); x +_f y <=_r z; x:A; y:A; z:A \<rbrakk>
\<Longrightarrow> x <=_r z \<and> y <=_r z"
by (rule Semilat.plus_le_conv [OF Semilat.intro, THEN iffD1])
- from prems show ?thesis
+ from assms show ?thesis
apply (rule_tac iffI)
apply clarify
apply (drule OK_le_err_OK [THEN iffD2])
--- a/src/HOL/MicroJava/DFA/Kildall.thy Thu Jan 13 21:50:13 2011 +0100
+++ b/src/HOL/MicroJava/DFA/Kildall.thy Thu Jan 13 23:50:16 2011 +0100
@@ -172,7 +172,7 @@
done
} note this [dest]
- from prems show ?thesis by blast
+ from assms show ?thesis by blast
qed
--- a/src/HOL/MicroJava/DFA/Product.thy Thu Jan 13 21:50:13 2011 +0100
+++ b/src/HOL/MicroJava/DFA/Product.thy Thu Jan 13 23:50:16 2011 +0100
@@ -77,7 +77,7 @@
"\<And>r f z. \<lbrakk> z : err A; semilat (err A, r, f); OK x : err A; OK y : err A;
OK x +_f OK y <=_r z\<rbrakk> \<Longrightarrow> OK x <=_r z \<and> OK y <=_r z"
by (rule Semilat.plus_le_conv [OF Semilat.intro, THEN iffD1])
- from prems show ?thesis
+ from assms show ?thesis
apply (rule_tac iffI)
apply clarify
apply (drule OK_le_err_OK [THEN iffD2])
--- a/src/HOL/NSA/NSA.thy Thu Jan 13 21:50:13 2011 +0100
+++ b/src/HOL/NSA/NSA.thy Thu Jan 13 23:50:16 2011 +0100
@@ -1837,12 +1837,12 @@
by (auto dest!: st_approx_self elim!: approx_trans3)
lemma approx_st_eq:
- assumes "x \<in> HFinite" and "y \<in> HFinite" and "x @= y"
+ assumes x: "x \<in> HFinite" and y: "y \<in> HFinite" and xy: "x @= y"
shows "st x = st y"
proof -
have "st x @= x" "st y @= y" "st x \<in> Reals" "st y \<in> Reals"
- by (simp_all add: st_approx_self st_SReal prems)
- with prems show ?thesis
+ by (simp_all add: st_approx_self st_SReal x y)
+ with xy show ?thesis
by (fast elim: approx_trans approx_trans2 SReal_approx_iff [THEN iffD1])
qed
--- a/src/HOL/Number_Theory/Binomial.thy Thu Jan 13 21:50:13 2011 +0100
+++ b/src/HOL/Number_Theory/Binomial.thy Thu Jan 13 23:50:16 2011 +0100
@@ -1,7 +1,6 @@
(* Title: Binomial.thy
Authors: Lawrence C. Paulson, Jeremy Avigad, Tobias Nipkow
-
Defines the "choose" function, and establishes basic properties.
The original theory "Binomial" was by Lawrence C. Paulson, based on
@@ -9,10 +8,8 @@
which derives the definition of binomial coefficients in terms of the
factorial function, is due to Jeremy Avigad. The binomial theorem was
formalized by Tobias Nipkow.
-
*)
-
header {* Binomial *}
theory Binomial
@@ -231,11 +228,10 @@
lemma choose_altdef_int:
assumes "(0::int) <= k" and "k <= n"
shows "n choose k = fact n div (fact k * fact (n - k))"
-
- apply (subst tsub_eq [symmetric], rule prems)
+ apply (subst tsub_eq [symmetric], rule assms)
apply (rule choose_altdef_nat [transferred])
- using prems apply auto
-done
+ using assms apply auto
+ done
lemma choose_dvd_nat: "(k::nat) \<le> n \<Longrightarrow> fact k * fact (n - k) dvd fact n"
unfolding dvd_def apply (frule choose_altdef_aux_nat)
@@ -247,11 +243,10 @@
lemma choose_dvd_int:
assumes "(0::int) <= k" and "k <= n"
shows "fact k * fact (n - k) dvd fact n"
-
- apply (subst tsub_eq [symmetric], rule prems)
+ apply (subst tsub_eq [symmetric], rule assms)
apply (rule choose_dvd_nat [transferred])
- using prems apply auto
-done
+ using assms apply auto
+ done
(* generalizes Tobias Nipkow's proof to any commutative semiring *)
theorem binomial: "(a+b::'a::{comm_ring_1,power})^n =
@@ -269,7 +264,7 @@
by auto
have "(a+b)^(n+1) =
(a+b) * (SUM k=0..n. of_nat (n choose k) * a^k * b^(n-k))"
- using ih by (simp add: power_plus_one)
+ using ih by simp
also have "... = a*(SUM k=0..n. of_nat (n choose k) * a^k * b^(n-k)) +
b*(SUM k=0..n. of_nat (n choose k) * a^k * b^(n-k))"
by (rule distrib)
@@ -278,8 +273,8 @@
by (subst (1 2) power_plus_one, simp add: setsum_right_distrib mult_ac)
also have "... = (SUM k=0..n. of_nat (n choose k) * a^k * b^(n+1-k)) +
(SUM k=1..n+1. of_nat (n choose (k - 1)) * a^k * b^(n+1-k))"
- by (simp add:setsum_shift_bounds_cl_Suc_ivl Suc_diff_le
- power_Suc field_simps One_nat_def del:setsum_cl_ivl_Suc)
+ by (simp add:setsum_shift_bounds_cl_Suc_ivl Suc_diff_le
+ field_simps One_nat_def del:setsum_cl_ivl_Suc)
also have "... = a^(n+1) + b^(n+1) +
(SUM k=1..n. of_nat (n choose (k - 1)) * a^k * b^(n+1-k)) +
(SUM k=1..n. of_nat (n choose k) * a^k * b^(n+1-k))"
@@ -315,7 +310,7 @@
hence "{ T. T \<subseteq> insert x F \<and> card T = k + 1} =
{T. T \<le> F & card T = k + 1} Un
{T. T \<le> insert x F & x : T & card T = k + 1}"
- by (auto intro!: subsetI)
+ by auto
with iassms fin have "card ({T. T \<le> insert x F \<and> card T = k + 1}) =
card ({T. T \<subseteq> F \<and> card T = k + 1}) +
card ({T. T \<subseteq> insert x F \<and> x : T \<and> card T = k + 1})"
@@ -330,7 +325,7 @@
proof -
let ?f = "%T. T Un {x}"
from iassms have "inj_on ?f {T. T <= F & card T = k}"
- unfolding inj_on_def by (auto intro!: subsetI)
+ unfolding inj_on_def by auto
hence "card ({T. T <= F & card T = k}) =
card(?f ` {T. T <= F & card T = k})"
by (rule card_image [symmetric])
--- a/src/HOL/Number_Theory/Cong.thy Thu Jan 13 21:50:13 2011 +0100
+++ b/src/HOL/Number_Theory/Cong.thy Thu Jan 13 23:50:16 2011 +0100
@@ -1,9 +1,7 @@
(* Title: HOL/Library/Cong.thy
- ID:
Authors: Christophe Tabacznyj, Lawrence C. Paulson, Amine Chaieb,
Thomas M. Rasmussen, Jeremy Avigad
-
Defines congruence (notation: [x = y] (mod z)) for natural numbers and
integers.
@@ -23,10 +21,8 @@
extended to the natural numbers by Chaieb. Jeremy Avigad combined
these, revised and tidied them, made the development uniform for the
natural numbers and the integers, and added a number of new theorems.
-
*)
-
header {* Congruence *}
theory Cong
@@ -54,9 +50,6 @@
card (insert x A) = (if x \<in> A then (card A) else (card A) + 1)"
by (auto simp add: insert_absorb)
-(* why wasn't card_insert_if a simp rule? *)
-declare card_insert_disjoint [simp del]
-
lemma nat_1' [simp]: "nat 1 = 1"
by simp
@@ -221,8 +214,7 @@
assumes "(a::nat) >= c" and "b >= d" and "[a = b] (mod m)" and
"[c = d] (mod m)"
shows "[a - c = b - d] (mod m)"
-
- using prems by (rule cong_diff_aux_int [transferred]);
+ using assms by (rule cong_diff_aux_int [transferred]);
lemma cong_mult_nat:
"[(a::nat) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a * c = b * d] (mod m)"
@@ -242,13 +234,13 @@
lemma cong_exp_nat: "[(x::nat) = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)"
apply (induct k)
- apply (auto simp add: cong_refl_nat cong_mult_nat)
-done
+ apply (auto simp add: cong_mult_nat)
+ done
lemma cong_exp_int: "[(x::int) = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)"
apply (induct k)
- apply (auto simp add: cong_refl_int cong_mult_int)
-done
+ apply (auto simp add: cong_mult_int)
+ done
lemma cong_setsum_nat [rule_format]:
"(ALL x: A. [((f x)::nat) = g x] (mod m)) \<longrightarrow>
@@ -313,8 +305,7 @@
lemma cong_eq_diff_cong_0_nat:
assumes "(a::nat) >= b"
shows "[a = b] (mod m) = [a - b = 0] (mod m)"
-
- using prems by (rule cong_eq_diff_cong_0_aux_int [transferred])
+ using assms by (rule cong_eq_diff_cong_0_aux_int [transferred])
lemma cong_diff_cong_0'_nat:
"[(x::nat) = y] (mod n) \<longleftrightarrow>
@@ -364,9 +355,8 @@
lemma cong_mult_rcancel_nat:
assumes "coprime k (m::nat)"
shows "[a * k = b * k] (mod m) = [a = b] (mod m)"
-
apply (rule cong_mult_rcancel_int [transferred])
- using prems apply auto
+ using assms apply auto
done
lemma cong_mult_lcancel_nat:
@@ -383,23 +373,22 @@
\<Longrightarrow> [a = b] (mod m * n)"
apply (simp only: cong_altdef_int)
apply (erule (2) divides_mult_int)
-done
+ done
lemma coprime_cong_mult_nat:
assumes "[(a::nat) = b] (mod m)" and "[a = b] (mod n)" and "coprime m n"
shows "[a = b] (mod m * n)"
-
apply (rule coprime_cong_mult_int [transferred])
- using prems apply auto
-done
+ using assms apply auto
+ done
lemma cong_less_imp_eq_nat: "0 \<le> (a::nat) \<Longrightarrow>
a < m \<Longrightarrow> 0 \<le> b \<Longrightarrow> b < m \<Longrightarrow> [a = b] (mod m) \<Longrightarrow> a = b"
- by (auto simp add: cong_nat_def mod_pos_pos_trivial)
+ by (auto simp add: cong_nat_def)
lemma cong_less_imp_eq_int: "0 \<le> (a::int) \<Longrightarrow>
a < m \<Longrightarrow> 0 \<le> b \<Longrightarrow> b < m \<Longrightarrow> [a = b] (mod m) \<Longrightarrow> a = b"
- by (auto simp add: cong_int_def mod_pos_pos_trivial)
+ by (auto simp add: cong_int_def)
lemma cong_less_unique_nat:
"0 < (m::nat) \<Longrightarrow> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))"
@@ -412,8 +401,8 @@
"0 < (m::int) \<Longrightarrow> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))"
apply auto
apply (rule_tac x = "a mod m" in exI)
- apply (unfold cong_int_def, auto simp add: mod_pos_pos_trivial)
-done
+ apply (unfold cong_int_def, auto)
+ done
lemma cong_iff_lin_int: "([(a::int) = b] (mod m)) = (\<exists>k. b = a + m * k)"
apply (auto simp add: cong_altdef_int dvd_def field_simps)
@@ -450,15 +439,14 @@
apply (subst mult_commute)
apply (subst gcd_add_mult_int)
apply (rule gcd_commute_int)
-done
+ done
lemma cong_gcd_eq_nat:
assumes "[(a::nat) = b] (mod m)"
shows "gcd a m = gcd b m"
-
apply (rule cong_gcd_eq_int [transferred])
- using prems apply auto
-done
+ using assms apply auto
+ done
lemma cong_imp_coprime_nat: "[(a::nat) = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow>
coprime b m"
@@ -479,11 +467,11 @@
lemma cong_minus_int [iff]: "[(a::int) = b] (mod -m) = [a = b] (mod m)"
by (subst (1 2) cong_altdef_int, auto)
-lemma cong_zero_nat [iff]: "[(a::nat) = b] (mod 0) = (a = b)"
- by (auto simp add: cong_nat_def)
+lemma cong_zero_nat: "[(a::nat) = b] (mod 0) = (a = b)"
+ by auto
-lemma cong_zero_int [iff]: "[(a::int) = b] (mod 0) = (a = b)"
- by (auto simp add: cong_int_def)
+lemma cong_zero_int: "[(a::int) = b] (mod 0) = (a = b)"
+ by auto
(*
lemma mod_dvd_mod_int:
@@ -498,8 +486,8 @@
shows "(a mod b mod m) = (a mod m)"
apply (rule mod_dvd_mod_int [transferred])
- using prems apply auto
-done
+ using assms apply auto
+ done
*)
lemma cong_add_lcancel_nat:
--- a/src/HOL/Number_Theory/Fib.thy Thu Jan 13 21:50:13 2011 +0100
+++ b/src/HOL/Number_Theory/Fib.thy Thu Jan 13 23:50:16 2011 +0100
@@ -1,14 +1,12 @@
(* Title: Fib.thy
Authors: Lawrence C. Paulson, Jeremy Avigad
-
Defines the fibonacci function.
The original "Fib" is due to Lawrence C. Paulson, and was adapted by
Jeremy Avigad.
*)
-
header {* Fib *}
theory Fib
@@ -284,16 +282,15 @@
lemma gcd_fib_mod_int:
assumes "0 < (m::int)" and "0 <= n"
shows "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
-
apply (rule gcd_fib_mod_nat [transferred])
- using prems apply auto
-done
+ using assms apply auto
+ done
lemma fib_gcd_nat: "fib (gcd (m::nat) n) = gcd (fib m) (fib n)"
-- {* Law 6.111 *}
apply (induct m n rule: gcd_nat_induct)
apply (simp_all add: gcd_non_0_nat gcd_commute_nat gcd_fib_mod_nat)
-done
+ done
lemma fib_gcd_int: "m >= 0 \<Longrightarrow> n >= 0 \<Longrightarrow>
fib (gcd (m::int) n) = gcd (fib m) (fib n)"
@@ -306,7 +303,7 @@
"fib ((n::nat) + 1) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"
apply (induct n)
apply (auto simp add: atMost_plus_one_nat fib_plus_2_nat field_simps)
-done
+ done
theorem fib_mult_eq_setsum'_nat:
"fib (Suc n) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"
--- a/src/HOL/Number_Theory/MiscAlgebra.thy Thu Jan 13 21:50:13 2011 +0100
+++ b/src/HOL/Number_Theory/MiscAlgebra.thy Thu Jan 13 23:50:16 2011 +0100
@@ -69,10 +69,10 @@
lemma (in comm_monoid) units_comm_group: "comm_group(units_of G)"
apply (rule group.group_comm_groupI)
apply (rule units_group)
- apply (insert prems)
+ apply (insert comm_monoid_axioms)
apply (unfold units_of_def Units_def comm_monoid_def comm_monoid_axioms_def)
- apply auto;
-done;
+ apply auto
+ done
lemma units_of_carrier: "carrier (units_of G) = Units G"
by (unfold units_of_def, auto)
@@ -174,18 +174,18 @@
lemma (in cring) field_intro2: "\<zero>\<^bsub>R\<^esub> ~= \<one>\<^bsub>R\<^esub> \<Longrightarrow> ALL x : carrier R - {\<zero>\<^bsub>R\<^esub>}.
x : Units R \<Longrightarrow> field R"
apply (unfold_locales)
- apply (insert prems, auto)
+ apply (insert cring_axioms, auto)
apply (rule trans)
apply (subgoal_tac "a = (a \<otimes> b) \<otimes> inv b")
apply assumption
apply (subst m_assoc)
- apply (auto simp add: Units_r_inv)
+ apply auto
apply (unfold Units_def)
apply auto
-done
+ done
lemma (in monoid) inv_char: "x : carrier G \<Longrightarrow> y : carrier G \<Longrightarrow>
- x \<otimes> y = \<one> \<Longrightarrow> y \<otimes> x = \<one> \<Longrightarrow> inv x = y"
+ x \<otimes> y = \<one> \<Longrightarrow> y \<otimes> x = \<one> \<Longrightarrow> inv x = y"
apply (subgoal_tac "x : Units G")
apply (subgoal_tac "y = inv x \<otimes> \<one>")
apply simp
@@ -194,19 +194,19 @@
apply auto
apply (unfold Units_def)
apply auto
-done
+ done
lemma (in comm_monoid) comm_inv_char: "x : carrier G \<Longrightarrow> y : carrier G \<Longrightarrow>
x \<otimes> y = \<one> \<Longrightarrow> inv x = y"
apply (rule inv_char)
apply auto
apply (subst m_comm, auto)
-done
+ done
lemma (in ring) inv_neg_one [simp]: "inv (\<ominus> \<one>) = \<ominus> \<one>"
apply (rule inv_char)
apply (auto simp add: l_minus r_minus)
-done
+ done
lemma (in monoid) inv_eq_imp_eq: "x : Units G \<Longrightarrow> y : Units G \<Longrightarrow>
inv x = inv y \<Longrightarrow> x = y"
@@ -281,8 +281,8 @@
apply (subgoal_tac "\<ominus> y = \<zero> \<oplus> \<ominus> y")
apply (erule ssubst)back
apply (erule subst)
- apply (simp add: ring_simprules)+
-done
+ apply (simp_all add: ring_simprules)
+ done
(* there's a name conflict -- maybe "domain" should be
"integral_domain" *)
@@ -336,9 +336,8 @@
"x : Units G \<Longrightarrow> x (^)\<^bsub>units_of G\<^esub> (n::nat) = x (^)\<^bsub>G\<^esub> n"
apply (induct n)
apply (auto simp add: units_group group.is_monoid
- monoid.nat_pow_0 monoid.nat_pow_Suc units_of_one units_of_mult
- One_nat_def)
-done
+ monoid.nat_pow_0 monoid.nat_pow_Suc units_of_one units_of_mult)
+ done
lemma (in cring) units_power_order_eq_one: "finite (Units R) \<Longrightarrow> a : Units R
\<Longrightarrow> a (^) card(Units R) = \<one>"
@@ -349,6 +348,6 @@
apply (rule comm_group.power_order_eq_one)
apply (rule units_comm_group)
apply (unfold units_of_def, auto)
-done
+ done
end
--- a/src/HOL/Number_Theory/Residues.thy Thu Jan 13 21:50:13 2011 +0100
+++ b/src/HOL/Number_Theory/Residues.thy Thu Jan 13 23:50:16 2011 +0100
@@ -1,18 +1,17 @@
(* Title: HOL/Library/Residues.thy
- ID:
Author: Jeremy Avigad
- An algebraic treatment of residue rings, and resulting proofs of
- Euler's theorem and Wilson's theorem.
+An algebraic treatment of residue rings, and resulting proofs of
+Euler's theorem and Wilson's theorem.
*)
header {* Residue rings *}
theory Residues
imports
- UniqueFactorization
- Binomial
- MiscAlgebra
+ UniqueFactorization
+ Binomial
+ MiscAlgebra
begin
@@ -41,14 +40,13 @@
apply (insert m_gt_one)
apply (rule abelian_groupI)
apply (unfold R_def residue_ring_def)
- apply (auto simp add: mod_pos_pos_trivial mod_add_right_eq [symmetric]
- add_ac)
+ apply (auto simp add: mod_add_right_eq [symmetric] add_ac)
apply (case_tac "x = 0")
apply force
apply (subgoal_tac "(x + (m - x)) mod m = 0")
apply (erule bexI)
apply auto
-done
+ done
lemma comm_monoid: "comm_monoid R"
apply (insert m_gt_one)
@@ -59,7 +57,7 @@
apply (erule ssubst)
apply (subst zmod_zmult1_eq [symmetric])+
apply (simp_all only: mult_ac)
-done
+ done
lemma cring: "cring R"
apply (rule cringI)
@@ -70,7 +68,7 @@
apply (subst mult_commute)
apply (subst zmod_zmult1_eq [symmetric])
apply (simp add: field_simps)
-done
+ done
end
@@ -78,7 +76,8 @@
by (rule cring)
-context residues begin
+context residues
+begin
(* These lemmas translate back and forth between internal and
external concepts *)
@@ -96,7 +95,7 @@
by (unfold R_def residue_ring_def, auto)
lemma res_one_eq: "\<one> = 1"
- by (unfold R_def residue_ring_def units_of_def residue_ring_def, auto)
+ by (unfold R_def residue_ring_def units_of_def, auto)
lemma res_units_eq: "Units R = { x. 0 < x & x < m & coprime x m}"
apply (insert m_gt_one)
@@ -110,7 +109,7 @@
apply (subst (asm) coprime_iff_invertible'_int)
apply (rule m_gt_one)
apply (auto simp add: cong_int_def mult_commute)
-done
+ done
lemma res_neg_eq: "\<ominus> x = (- x) mod m"
apply (insert m_gt_one)
@@ -126,7 +125,7 @@
apply simp
apply (subst zmod_eq_dvd_iff)
apply auto
-done
+ done
lemma finite [iff]: "finite(carrier R)"
by (subst res_carrier_eq, auto)
@@ -141,7 +140,7 @@
lemma mod_in_carrier [iff]: "a mod m : carrier R"
apply (unfold res_carrier_eq)
apply (insert m_gt_one, auto)
-done
+ done
lemma add_cong: "(x mod m) \<oplus> (y mod m) = (x + y) mod m"
by (unfold R_def residue_ring_def, auto, arith)
@@ -153,25 +152,25 @@
apply (subst zmod_zmult1_eq [symmetric])
apply (subst mult_commute)
apply auto
-done
+ done
lemma zero_cong: "\<zero> = 0"
apply (unfold R_def residue_ring_def, auto)
-done
+ done
lemma one_cong: "\<one> = 1 mod m"
apply (insert m_gt_one)
apply (unfold R_def residue_ring_def, auto)
-done
+ done
(* revise algebra library to use 1? *)
lemma pow_cong: "(x mod m) (^) n = x^n mod m"
apply (insert m_gt_one)
apply (induct n)
- apply (auto simp add: nat_pow_def one_cong One_nat_def)
+ apply (auto simp add: nat_pow_def one_cong)
apply (subst mult_commute)
apply (rule mult_cong)
-done
+ done
lemma neg_cong: "\<ominus> (x mod m) = (- x) mod m"
apply (rule sym)
@@ -180,19 +179,19 @@
apply (subst add_cong)
apply (subst zero_cong)
apply auto
-done
+ done
lemma (in residues) prod_cong:
"finite A \<Longrightarrow> (\<Otimes> i:A. (f i) mod m) = (PROD i:A. f i) mod m"
apply (induct set: finite)
apply (auto simp: one_cong mult_cong)
-done
+ done
lemma (in residues) sum_cong:
"finite A \<Longrightarrow> (\<Oplus> i:A. (f i) mod m) = (SUM i: A. f i) mod m"
apply (induct set: finite)
apply (auto simp: zero_cong add_cong)
-done
+ done
lemma mod_in_res_units [simp]: "1 < m \<Longrightarrow> coprime a m \<Longrightarrow>
a mod m : Units R"
@@ -203,7 +202,7 @@
apply auto
apply (subst (asm) gcd_red_int)
apply (subst gcd_commute_int, assumption)
-done
+ done
lemma res_eq_to_cong: "((a mod m) = (b mod m)) = [a = b] (mod (m::int))"
unfolding cong_int_def by auto
@@ -227,7 +226,7 @@
apply (subst mod_add_self2 [symmetric])
apply (subst mod_pos_pos_trivial)
apply auto
-done
+ done
end
@@ -242,7 +241,7 @@
sublocale residues_prime < residues p
apply (unfold R_def residues_def)
using p_prime apply auto
-done
+ done
context residues_prime begin
@@ -259,7 +258,7 @@
apply (rule notI)
apply (frule zdvd_imp_le)
apply auto
-done
+ done
lemma res_prime_units_eq: "Units R = {1..p - 1}"
apply (subst res_units_eq)
@@ -269,7 +268,7 @@
apply (rule p_prime)
apply (rule zdvd_not_zless)
apply auto
-done
+ done
end
@@ -295,11 +294,11 @@
1 == Suc 0 coming from? *)
apply (auto simp add: card_eq_0_iff)
(* Add card_eq_0_iff as a simp rule? delete card_empty_imp? *)
-done
+ done
lemma phi_one [simp]: "phi 1 = 0"
apply (auto simp add: phi_def card_eq_0_iff)
-done
+ done
lemma (in residues) phi_eq: "phi m = card(Units R)"
by (simp add: phi_def res_units_eq)
@@ -342,7 +341,7 @@
thus ?thesis by auto
next
assume "~(m = 0 | m = 1)"
- with prems show ?thesis
+ with assms show ?thesis
by (intro residues.euler_theorem1, unfold residues_def, auto)
qed
@@ -350,18 +349,18 @@
apply (subst phi_eq)
apply (subst res_prime_units_eq)
apply auto
-done
+ done
lemma phi_prime: "prime p \<Longrightarrow> phi p = (nat p - 1)"
apply (rule residues_prime.phi_prime)
apply (erule residues_prime.intro)
-done
+ done
lemma fermat_theorem:
assumes "prime p" and "~ (p dvd a)"
shows "[a^(nat p - 1) = 1] (mod p)"
proof -
- from prems have "[a^phi p = 1] (mod p)"
+ from assms have "[a^phi p = 1] (mod p)"
apply (intro euler_theorem)
(* auto should get this next part. matching across
substitutions is needed. *)
@@ -369,7 +368,7 @@
apply (subst gcd_commute_int, erule prime_imp_coprime_int, assumption)
done
also have "phi p = nat p - 1"
- by (rule phi_prime, rule prems)
+ by (rule phi_prime, rule assms)
finally show ?thesis .
qed
@@ -377,7 +376,7 @@
subsection {* Wilson's theorem *}
lemma (in field) inv_pair_lemma: "x : Units R \<Longrightarrow> y : Units R \<Longrightarrow>
- {x, inv x} ~= {y, inv y} \<Longrightarrow> {x, inv x} Int {y, inv y} = {}"
+ {x, inv x} ~= {y, inv y} \<Longrightarrow> {x, inv x} Int {y, inv y} = {}"
apply auto
apply (erule notE)
apply (erule inv_eq_imp_eq)
@@ -385,7 +384,7 @@
apply (erule notE)
apply (erule inv_eq_imp_eq)
apply auto
-done
+ done
lemma (in residues_prime) wilson_theorem1:
assumes a: "p > 2"
@@ -411,7 +410,7 @@
apply (insert a, force)
done
also have "(\<Otimes>i:(Union ?InversePairs). i) =
- (\<Otimes> A: ?InversePairs. (\<Otimes> y:A. y))"
+ (\<Otimes>A: ?InversePairs. (\<Otimes>y:A. y))"
apply (subst finprod_Union_disjoint)
apply force
apply force
@@ -441,7 +440,7 @@
done
also have "\<dots> = fact (p - 1) mod p"
apply (subst fact_altdef_int)
- apply (insert prems, force)
+ apply (insert assms, force)
apply (subst res_prime_units_eq, rule refl)
done
finally have "fact (p - 1) mod p = \<ominus> \<one>".
--- a/src/HOL/Number_Theory/UniqueFactorization.thy Thu Jan 13 21:50:13 2011 +0100
+++ b/src/HOL/Number_Theory/UniqueFactorization.thy Thu Jan 13 23:50:16 2011 +0100
@@ -1,12 +1,11 @@
(* Title: UniqueFactorization.thy
Author: Jeremy Avigad
-
- Unique factorization for the natural numbers and the integers.
+Unique factorization for the natural numbers and the integers.
- Note: there were previous Isabelle formalizations of unique
- factorization due to Thomas Marthedal Rasmussen, and, building on
- that, by Jeremy Avigad and David Gray.
+Note: there were previous Isabelle formalizations of unique
+factorization due to Thomas Marthedal Rasmussen, and, building on
+that, by Jeremy Avigad and David Gray.
*)
header {* UniqueFactorization *}
@@ -135,14 +134,13 @@
moreover
{
assume "n > 1" and "~ prime n"
- from prems not_prime_eq_prod_nat
- obtain m k where "n = m * k & 1 < m & m < n & 1 < k & k < n"
+ with not_prime_eq_prod_nat obtain m k where n: "n = m * k & 1 < m & m < n & 1 < k & k < n"
by blast
with ih obtain Q R where "(ALL p : set_of Q. prime p) & m = (PROD i:#Q. i)"
and "(ALL p: set_of R. prime p) & k = (PROD i:#R. i)"
by blast
hence "(ALL p: set_of (Q + R). prime p) & n = (PROD i :# Q + R. i)"
- by (auto simp add: prems msetprod_Un set_of_union)
+ by (auto simp add: n msetprod_Un)
then have "EX M. (ALL p : set_of M. prime p) & n = (PROD i :# M. i)"..
}
ultimately show "EX M. (ALL p : set_of M. prime p) & n = (PROD i::nat:#M. i)"
@@ -157,13 +155,11 @@
shows
"count M a <= count N a"
proof cases
- assume "a : set_of M"
- with prems have a: "prime a"
- by auto
- with prems have "a ^ count M a dvd (PROD i :# M. i)"
+ assume M: "a : set_of M"
+ with assms have a: "prime a" by auto
+ with M have "a ^ count M a dvd (PROD i :# M. i)"
by (auto intro: dvd_setprod simp add: msetprod_def)
- also have "... dvd (PROD i :# N. i)"
- by (rule prems)
+ also have "... dvd (PROD i :# N. i)" by (rule assms)
also have "... = (PROD i : (set_of N). i ^ (count N i))"
by (simp add: msetprod_def)
also have "... =
@@ -186,7 +182,8 @@
apply (subst gcd_commute_nat)
apply (rule setprod_coprime_nat)
apply (rule primes_imp_powers_coprime_nat)
- apply (insert prems, auto)
+ using assms M
+ apply auto
done
ultimately have "a ^ count M a dvd a^(count N a)"
by (elim coprime_dvd_mult_nat)
@@ -206,9 +203,9 @@
proof -
{
fix a
- from prems have "count M a <= count N a"
+ from assms have "count M a <= count N a"
by (intro multiset_prime_factorization_unique_aux, auto)
- moreover from prems have "count N a <= count M a"
+ moreover from assms have "count N a <= count M a"
by (intro multiset_prime_factorization_unique_aux, auto)
ultimately have "count M a = count N a"
by auto
@@ -245,7 +242,6 @@
(* definitions for the natural numbers *)
instantiation nat :: unique_factorization
-
begin
definition
@@ -265,7 +261,6 @@
(* definitions for the integers *)
instantiation int :: unique_factorization
-
begin
definition
@@ -329,15 +324,14 @@
apply (case_tac "n = 0")
apply (simp add: prime_factors_nat_def multiset_prime_factorization_def)
apply (auto simp add: prime_factors_nat_def multiset_prime_factorization)
-done
+ done
lemma prime_factors_prime_int [intro]:
assumes "n >= 0" and "p : prime_factors (n::int)"
shows "prime p"
-
apply (rule prime_factors_prime_nat [transferred, of n p])
- using prems apply auto
-done
+ using assms apply auto
+ done
lemma prime_factors_gt_0_nat [elim]: "p : prime_factors x \<Longrightarrow> p > (0::nat)"
by (frule prime_factors_prime_nat, auto)
@@ -361,22 +355,19 @@
apply (unfold prime_factors_int_def multiplicity_int_def)
apply (subst prime_factors_altdef_nat)
apply (auto simp add: image_def)
-done
+ done
lemma prime_factorization_nat: "(n::nat) > 0 \<Longrightarrow>
n = (PROD p : prime_factors n. p^(multiplicity p n))"
by (frule multiset_prime_factorization,
simp add: prime_factors_nat_def multiplicity_nat_def msetprod_def)
-thm prime_factorization_nat [transferred]
-
lemma prime_factorization_int:
assumes "(n::int) > 0"
shows "n = (PROD p : prime_factors n. p^(multiplicity p n))"
-
apply (rule prime_factorization_nat [transferred, of n])
- using prems apply auto
-done
+ using assms apply auto
+ done
lemma neq_zero_eq_gt_zero_nat: "((x::nat) ~= 0) = (x > 0)"
by auto
@@ -591,10 +582,9 @@
shows
"(prime_factors k) Un (prime_factors l) = prime_factors (k * l) &
(ALL p >= 0. multiplicity p k + multiplicity p l = multiplicity p (k * l))"
-
apply (rule multiplicity_product_aux_nat [transferred, of l k])
- using prems apply auto
-done
+ using assms apply auto
+ done
lemma prime_factors_product_nat: "(k::nat) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> prime_factors (k * l) =
prime_factors k Un prime_factors l"
@@ -805,9 +795,9 @@
apply (case_tac "p >= 0")
apply (rule prime_factors_altdef2_nat [transferred])
- using prems apply auto
+ using assms apply auto
apply (auto simp add: prime_ge_0_int prime_factors_ge_0_int)
-done
+ done
lemma multiplicity_eq_nat:
fixes x and y::nat
@@ -846,7 +836,7 @@
min (multiplicity p x) (multiplicity p y)"
unfolding z_def
apply (subst multiplicity_prod_prime_powers_nat)
- apply (auto simp add: multiplicity_not_factor_nat)
+ apply auto
done
have "z dvd x"
by (intro multiplicity_dvd'_nat, auto simp add: aux)
@@ -878,7 +868,7 @@
max (multiplicity p x) (multiplicity p y)"
unfolding z_def
apply (subst multiplicity_prod_prime_powers_nat)
- apply (auto simp add: multiplicity_not_factor_nat)
+ apply auto
done
have "x dvd z"
by (intro multiplicity_dvd'_nat, auto simp add: aux)
--- a/src/HOL/Old_Number_Theory/Euler.thy Thu Jan 13 21:50:13 2011 +0100
+++ b/src/HOL/Old_Number_Theory/Euler.thy Thu Jan 13 23:50:16 2011 +0100
@@ -56,29 +56,27 @@
apply (rule bexI, auto)
done
-lemma MultInvPair_distinct: "[| zprime p; 2 < p; ~([a = 0] (mod p));
- ~([j = 0] (mod p));
- ~(QuadRes p a) |] ==>
- ~([j = a * MultInv p j] (mod p))"
+lemma MultInvPair_distinct:
+ assumes "zprime p" and "2 < p" and
+ "~([a = 0] (mod p))" and
+ "~([j = 0] (mod p))" and
+ "~(QuadRes p a)"
+ shows "~([j = a * MultInv p j] (mod p))"
proof
- assume "zprime p" and "2 < p" and "~([a = 0] (mod p))" and
- "~([j = 0] (mod p))" and "~(QuadRes p a)"
assume "[j = a * MultInv p j] (mod p)"
then have "[j * j = (a * MultInv p j) * j] (mod p)"
by (auto simp add: zcong_scalar)
then have a:"[j * j = a * (MultInv p j * j)] (mod p)"
by (auto simp add: zmult_ac)
have "[j * j = a] (mod p)"
- proof -
- from prems have b: "[MultInv p j * j = 1] (mod p)"
- by (simp add: MultInv_prop2a)
- from b a show ?thesis
- by (auto simp add: zcong_zmult_prop2)
- qed
- then have "[j^2 = a] (mod p)"
- by (metis number_of_is_id power2_eq_square succ_bin_simps)
- with prems show False
- by (simp add: QuadRes_def)
+ proof -
+ from assms(1,2,4) have "[MultInv p j * j = 1] (mod p)"
+ by (simp add: MultInv_prop2a)
+ from this and a show ?thesis
+ by (auto simp add: zcong_zmult_prop2)
+ qed
+ then have "[j^2 = a] (mod p)" by (simp add: power2_eq_square)
+ with assms show False by (simp add: QuadRes_def)
qed
lemma MultInvPair_card_two: "[| zprime p; 2 < p; ~([a = 0] (mod p));
@@ -108,33 +106,31 @@
done
lemma Union_SetS_finite: "2 < p ==> finite (Union (SetS a p))"
- by (auto simp add: SetS_finite SetS_elems_finite finite_Union)
+ by (auto simp add: SetS_finite SetS_elems_finite)
lemma card_setsum_aux: "[| finite S; \<forall>X \<in> S. finite (X::int set);
\<forall>X \<in> S. card X = n |] ==> setsum card S = setsum (%x. n) S"
by (induct set: finite) auto
-lemma SetS_card: "[| zprime p; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a) |] ==>
- int(card(SetS a p)) = (p - 1) div 2"
+lemma SetS_card:
+ assumes "zprime p" and "2 < p" and "~([a = 0] (mod p))" and "~(QuadRes p a)"
+ shows "int(card(SetS a p)) = (p - 1) div 2"
proof -
- assume "zprime p" and "2 < p" and "~([a = 0] (mod p))" and "~(QuadRes p a)"
- then have "(p - 1) = 2 * int(card(SetS a p))"
+ have "(p - 1) = 2 * int(card(SetS a p))"
proof -
have "p - 1 = int(card(Union (SetS a p)))"
- by (auto simp add: prems MultInvPair_prop2 SRStar_card)
+ by (auto simp add: assms MultInvPair_prop2 SRStar_card)
also have "... = int (setsum card (SetS a p))"
- by (auto simp add: prems SetS_finite SetS_elems_finite
- MultInvPair_prop1c [of p a] card_Union_disjoint)
+ by (auto simp add: assms SetS_finite SetS_elems_finite
+ MultInvPair_prop1c [of p a] card_Union_disjoint)
also have "... = int(setsum (%x.2) (SetS a p))"
- using prems
- by (auto simp add: SetS_elems_card SetS_finite SetS_elems_finite
+ using assms by (auto simp add: SetS_elems_card SetS_finite SetS_elems_finite
card_setsum_aux simp del: setsum_constant)
also have "... = 2 * int(card( SetS a p))"
- by (auto simp add: prems SetS_finite setsum_const2)
+ by (auto simp add: assms SetS_finite setsum_const2)
finally show ?thesis .
qed
- from this show ?thesis
- by auto
+ then show ?thesis by auto
qed
lemma SetS_setprod_prop: "[| zprime p; 2 < p; ~([a = 0] (mod p));
@@ -177,37 +173,37 @@
apply (frule d22set_g_1, auto)
done
-lemma Union_SetS_setprod_prop1: "[| zprime p; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a) |] ==>
- [\<Prod>(Union (SetS a p)) = a ^ nat ((p - 1) div 2)] (mod p)"
+lemma Union_SetS_setprod_prop1:
+ assumes "zprime p" and "2 < p" and "~([a = 0] (mod p))" and
+ "~(QuadRes p a)"
+ shows "[\<Prod>(Union (SetS a p)) = a ^ nat ((p - 1) div 2)] (mod p)"
proof -
- assume "zprime p" and "2 < p" and "~([a = 0] (mod p))" and "~(QuadRes p a)"
- then have "[\<Prod>(Union (SetS a p)) =
- setprod (setprod (%x. x)) (SetS a p)] (mod p)"
+ from assms have "[\<Prod>(Union (SetS a p)) = setprod (setprod (%x. x)) (SetS a p)] (mod p)"
by (auto simp add: SetS_finite SetS_elems_finite
- MultInvPair_prop1c setprod_Union_disjoint)
+ MultInvPair_prop1c setprod_Union_disjoint)
also have "[setprod (setprod (%x. x)) (SetS a p) =
setprod (%x. a) (SetS a p)] (mod p)"
by (rule setprod_same_function_zcong)
- (auto simp add: prems SetS_setprod_prop SetS_finite)
+ (auto simp add: assms SetS_setprod_prop SetS_finite)
also (zcong_trans) have "[setprod (%x. a) (SetS a p) =
a^(card (SetS a p))] (mod p)"
- by (auto simp add: prems SetS_finite setprod_constant)
+ by (auto simp add: assms SetS_finite setprod_constant)
finally (zcong_trans) show ?thesis
apply (rule zcong_trans)
apply (subgoal_tac "card(SetS a p) = nat((p - 1) div 2)", auto)
apply (subgoal_tac "nat(int(card(SetS a p))) = nat((p - 1) div 2)", force)
- apply (auto simp add: prems SetS_card)
+ apply (auto simp add: assms SetS_card)
done
qed
-lemma Union_SetS_setprod_prop2: "[| zprime p; 2 < p; ~([a = 0](mod p)) |] ==>
- \<Prod>(Union (SetS a p)) = zfact (p - 1)"
+lemma Union_SetS_setprod_prop2:
+ assumes "zprime p" and "2 < p" and "~([a = 0](mod p))"
+ shows "\<Prod>(Union (SetS a p)) = zfact (p - 1)"
proof -
- assume "zprime p" and "2 < p" and "~([a = 0](mod p))"
- then have "\<Prod>(Union (SetS a p)) = \<Prod>(SRStar p)"
+ from assms have "\<Prod>(Union (SetS a p)) = \<Prod>(SRStar p)"
by (auto simp add: MultInvPair_prop2)
also have "... = \<Prod>({1} \<union> (d22set (p - 1)))"
- by (auto simp add: prems SRStar_d22set_prop)
+ by (auto simp add: assms SRStar_d22set_prop)
also have "... = zfact(p - 1)"
proof -
have "~(1 \<in> d22set (p - 1)) & finite( d22set (p - 1))"
--- a/src/HOL/Old_Number_Theory/Gauss.thy Thu Jan 13 21:50:13 2011 +0100
+++ b/src/HOL/Old_Number_Theory/Gauss.thy Thu Jan 13 23:50:16 2011 +0100
@@ -79,10 +79,10 @@
by (auto simp add: C_def finite_B)
lemma finite_D: "finite (D)"
-by (auto simp add: D_def finite_Int finite_C)
+by (auto simp add: D_def finite_C)
lemma finite_E: "finite (E)"
-by (auto simp add: E_def finite_Int finite_C)
+by (auto simp add: E_def finite_C)
lemma finite_F: "finite (F)"
by (auto simp add: F_def finite_E)
@@ -125,11 +125,11 @@
with zcong_less_eq [of x y p] p_minus_one_l
order_le_less_trans [of x "(p - 1) div 2" p]
order_le_less_trans [of y "(p - 1) div 2" p] show "x = y"
- by (simp add: prems p_minus_one_l p_g_0)
+ by (simp add: b c d e p_minus_one_l p_g_0)
qed
lemma SR_B_inj: "inj_on (StandardRes p) B"
- apply (auto simp add: B_def StandardRes_def inj_on_def A_def prems)
+ apply (auto simp add: B_def StandardRes_def inj_on_def A_def)
proof -
fix x fix y
assume a: "x * a mod p = y * a mod p"
@@ -146,7 +146,7 @@
with zcong_less_eq [of x y p] p_minus_one_l
order_le_less_trans [of x "(p - 1) div 2" p]
order_le_less_trans [of y "(p - 1) div 2" p] have "x = y"
- by (simp add: prems p_minus_one_l p_g_0)
+ by (simp add: b c d e p_minus_one_l p_g_0)
then have False
by (simp add: f)
then show "a = 0"
--- a/src/HOL/Old_Number_Theory/Int2.thy Thu Jan 13 21:50:13 2011 +0100
+++ b/src/HOL/Old_Number_Theory/Int2.thy Thu Jan 13 23:50:16 2011 +0100
@@ -43,38 +43,39 @@
apply (force simp del:dvd_mult)
done
-lemma div_prop1: "[| 0 < z; (x::int) < y * z |] ==> x div z < y"
+lemma div_prop1:
+ assumes "0 < z" and "(x::int) < y * z"
+ shows "x div z < y"
proof -
- assume "0 < z" then have modth: "x mod z \<ge> 0" by simp
+ from `0 < z` have modth: "x mod z \<ge> 0" by simp
have "(x div z) * z \<le> (x div z) * z" by simp
then have "(x div z) * z \<le> (x div z) * z + x mod z" using modth by arith
also have "\<dots> = x"
by (auto simp add: zmod_zdiv_equality [symmetric] zmult_ac)
- also assume "x < y * z"
+ also note `x < y * z`
finally show ?thesis
- by (auto simp add: prems mult_less_cancel_right, insert prems, arith)
+ apply (auto simp add: mult_less_cancel_right)
+ using assms apply arith
+ done
qed
-lemma div_prop2: "[| 0 < z; (x::int) < (y * z) + z |] ==> x div z \<le> y"
+lemma div_prop2:
+ assumes "0 < z" and "(x::int) < (y * z) + z"
+ shows "x div z \<le> y"
proof -
- assume "0 < z" and "x < (y * z) + z"
- then have "x < (y + 1) * z" by (auto simp add: int_distrib)
+ from assms have "x < (y + 1) * z" by (auto simp add: int_distrib)
then have "x div z < y + 1"
- apply -
apply (rule_tac y = "y + 1" in div_prop1)
- apply (auto simp add: prems)
+ apply (auto simp add: `0 < z`)
done
then show ?thesis by auto
qed
-lemma zdiv_leq_prop: "[| 0 < y |] ==> y * (x div y) \<le> (x::int)"
+lemma zdiv_leq_prop: assumes "0 < y" shows "y * (x div y) \<le> (x::int)"
proof-
- assume "0 < y"
from zmod_zdiv_equality have "x = y * (x div y) + x mod y" by auto
- moreover have "0 \<le> x mod y"
- by (auto simp add: prems pos_mod_sign)
- ultimately show ?thesis
- by arith
+ moreover have "0 \<le> x mod y" by (auto simp add: assms)
+ ultimately show ?thesis by arith
qed
@@ -87,7 +88,7 @@
by (auto simp add: zcong_def)
lemma zcong_shift: "[a = b] (mod m) ==> [a + c = b + c] (mod m)"
- by (auto simp add: zcong_refl zcong_zadd)
+ by (auto simp add: zcong_zadd)
lemma zcong_zpower: "[x = y](mod m) ==> [x^z = y^z](mod m)"
by (induct z) (auto simp add: zcong_zmult)
@@ -126,11 +127,12 @@
x < m; y < m |] ==> x = y"
by (metis zcong_not zcong_sym zless_linear)
-lemma zcong_neg_1_impl_ne_1: "[| 2 < p; [x = -1] (mod p) |] ==>
- ~([x = 1] (mod p))"
+lemma zcong_neg_1_impl_ne_1:
+ assumes "2 < p" and "[x = -1] (mod p)"
+ shows "~([x = 1] (mod p))"
proof
- assume "2 < p" and "[x = 1] (mod p)" and "[x = -1] (mod p)"
- then have "[1 = -1] (mod p)"
+ assume "[x = 1] (mod p)"
+ with assms have "[1 = -1] (mod p)"
apply (auto simp add: zcong_sym)
apply (drule zcong_trans, auto)
done
@@ -140,7 +142,7 @@
by auto
then have "p dvd 2"
by (auto simp add: dvd_def zcong_def)
- with prems show False
+ with `2 < p` show False
by (auto simp add: zdvd_not_zless)
qed
@@ -181,15 +183,15 @@
lemma MultInv_prop2: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==>
[(x * (MultInv p x)) = 1] (mod p)"
proof (simp add: MultInv_def zcong_eq_zdvd_prop)
- assume "2 < p" and "zprime p" and "~ p dvd x"
+ assume 1: "2 < p" and 2: "zprime p" and 3: "~ p dvd x"
have "x * x ^ nat (p - 2) = x ^ (nat (p - 2) + 1)"
by auto
- also from prems have "nat (p - 2) + 1 = nat (p - 2 + 1)"
+ also from 1 have "nat (p - 2) + 1 = nat (p - 2 + 1)"
by (simp only: nat_add_distrib)
also have "p - 2 + 1 = p - 1" by arith
finally have "[x * x ^ nat (p - 2) = x ^ nat (p - 1)] (mod p)"
by (rule ssubst, auto)
- also from prems have "[x ^ nat (p - 1) = 1] (mod p)"
+ also from 2 3 have "[x ^ nat (p - 1) = 1] (mod p)"
by (auto simp add: Little_Fermat)
finally (zcong_trans) show "[x * x ^ nat (p - 2) = 1] (mod p)" .
qed
--- a/src/HOL/Old_Number_Theory/IntPrimes.thy Thu Jan 13 21:50:13 2011 +0100
+++ b/src/HOL/Old_Number_Theory/IntPrimes.thy Thu Jan 13 23:50:16 2011 +0100
@@ -277,7 +277,7 @@
by (auto simp add: zcong_def)
lemma "[a = b] (mod m) = (a mod m = b mod m)"
- apply (case_tac "m = 0", simp add: DIVISION_BY_ZERO)
+ apply (cases "m = 0", simp)
apply (simp add: linorder_neq_iff)
apply (erule disjE)
prefer 2 apply (simp add: zcong_zmod_eq)
--- a/src/HOL/Old_Number_Theory/Legacy_GCD.thy Thu Jan 13 21:50:13 2011 +0100
+++ b/src/HOL/Old_Number_Theory/Legacy_GCD.thy Thu Jan 13 23:50:16 2011 +0100
@@ -276,7 +276,7 @@
shows "\<exists>d x y. d dvd a \<and> d dvd a + b \<and> (a * x = (a + b) * y + d \<or> (a + b) * x = a * y + d)"
using ex
apply clarsimp
-apply (rule_tac x="d" in exI, simp add: dvd_add)
+apply (rule_tac x="d" in exI, simp)
apply (case_tac "a * x = b * y + d" , simp_all)
apply (rule_tac x="x + y" in exI)
apply (rule_tac x="y" in exI)
@@ -290,10 +290,10 @@
apply(induct a b rule: ind_euclid)
apply blast
apply clarify
-apply (rule_tac x="a" in exI, simp add: dvd_add)
+apply (rule_tac x="a" in exI, simp)
apply clarsimp
apply (rule_tac x="d" in exI)
-apply (case_tac "a * x = b * y + d", simp_all add: dvd_add)
+apply (case_tac "a * x = b * y + d", simp_all)
apply (rule_tac x="x+y" in exI)
apply (rule_tac x="y" in exI)
apply algebra
@@ -332,13 +332,13 @@
from divides_le[OF H(2)] b have "d < b \<or> d = b" using le_less by blast
moreover
{assume db: "d=b"
- from prems have ?thesis apply simp
+ from nz H db have ?thesis apply simp
apply (rule exI[where x = b], simp)
apply (rule exI[where x = b])
by (rule exI[where x = "a - 1"], simp add: diff_mult_distrib2)}
moreover
{assume db: "d < b"
- {assume "x=0" hence ?thesis using prems by simp }
+ {assume "x=0" hence ?thesis using nz H by simp }
moreover
{assume x0: "x \<noteq> 0" hence xp: "x > 0" by simp
@@ -426,12 +426,11 @@
qed
lemma gcd_mult': "gcd b (a * b) = b"
-by (simp add: gcd_mult mult_commute[of a b])
+by (simp add: mult_commute[of a b])
lemma gcd_add: "gcd(a + b) b = gcd a b"
"gcd(b + a) b = gcd a b" "gcd a (a + b) = gcd a b" "gcd a (b + a) = gcd a b"
-apply (simp_all add: gcd_add1)
-by (simp add: gcd_commute gcd_add1)
+by (simp_all add: gcd_commute)
lemma gcd_sub: "b <= a ==> gcd(a - b) b = gcd a b" "a <= b ==> gcd a (b - a) = gcd a b"
proof-
@@ -568,10 +567,10 @@
zgcd :: "int \<Rightarrow> int \<Rightarrow> int" where
"zgcd i j = int (gcd (nat (abs i)) (nat (abs j)))"
-lemma zgcd_zdvd1 [iff,simp, algebra]: "zgcd i j dvd i"
+lemma zgcd_zdvd1 [iff, algebra]: "zgcd i j dvd i"
by (simp add: zgcd_def int_dvd_iff)
-lemma zgcd_zdvd2 [iff,simp, algebra]: "zgcd i j dvd j"
+lemma zgcd_zdvd2 [iff, algebra]: "zgcd i j dvd j"
by (simp add: zgcd_def int_dvd_iff)
lemma zgcd_pos: "zgcd i j \<ge> 0"
@@ -637,8 +636,8 @@
let ?a' = "a div ?g"
let ?b' = "b div ?g"
let ?g' = "zgcd ?a' ?b'"
- have dvdg: "?g dvd a" "?g dvd b" by (simp_all add: zgcd_zdvd1 zgcd_zdvd2)
- have dvdg': "?g' dvd ?a'" "?g' dvd ?b'" by (simp_all add: zgcd_zdvd1 zgcd_zdvd2)
+ have dvdg: "?g dvd a" "?g dvd b" by simp_all
+ have dvdg': "?g' dvd ?a'" "?g' dvd ?b'" by simp_all
from dvdg dvdg' obtain ka kb ka' kb' where
kab: "a = ?g*ka" "b = ?g*kb" "?a' = ?g'*ka'" "?b' = ?g' * kb'"
unfolding dvd_def by blast
@@ -668,7 +667,7 @@
done
lemma zgcd_eq: "zgcd m n = zgcd n (m mod n)"
- apply (case_tac "n = 0", simp add: DIVISION_BY_ZERO)
+ apply (cases "n = 0", simp)
apply (auto simp add: linorder_neq_iff zgcd_non_0)
apply (cut_tac m = "-m" and n = "-n" in zgcd_non_0, auto)
done
@@ -683,7 +682,7 @@
by (simp add: zgcd_def abs_if int_dvd_iff dvd_int_iff nat_dvd_iff)
lemma zgcd_1_left [simp, algebra]: "zgcd 1 m = 1"
- by (simp add: zgcd_def gcd_1_left)
+ by (simp add: zgcd_def)
lemma zgcd_assoc: "zgcd (zgcd k m) n = zgcd k (zgcd m n)"
by (simp add: zgcd_def gcd_assoc)
--- a/src/HOL/Old_Number_Theory/Pocklington.thy Thu Jan 13 21:50:13 2011 +0100
+++ b/src/HOL/Old_Number_Theory/Pocklington.thy Thu Jan 13 23:50:16 2011 +0100
@@ -260,7 +260,9 @@
apply (cases "n=0", simp_all add: cong_commute)
apply (cases "n=1", simp_all add: cong_commute modeq_def)
apply arith
- by (cases "a=1", simp_all add: modeq_def cong_commute)}
+ apply (cases "a=1")
+ apply (simp_all add: modeq_def cong_commute)
+ done }
moreover
{assume n: "n\<noteq>0" "n\<noteq>1" and a:"a\<noteq>0" "a \<noteq> 1" hence a': "a \<ge> 1" by simp
hence ?thesis using cong_le[OF a', of n] by auto }
@@ -630,7 +632,7 @@
with an have "coprime (a*x) n"
by (simp add: coprime_mul_eq[of n a x] coprime_commute)
hence "?h (a*x) \<in> ?S" using nz
- by (simp add: coprime_mod[OF nz] mod_less_divisor)}
+ by (simp add: coprime_mod[OF nz])}
thus " \<forall>x\<in>{m. coprime m n \<and> m < n}.
((\<lambda>m. m mod n) \<circ> op * a) x \<in> {m. coprime m n \<and> m < n} \<and>
((\<lambda>m. m mod n) \<circ> op * a) x = ((\<lambda>m. m mod n) \<circ> op * a) x" by simp
@@ -821,7 +823,7 @@
lemma ord_minimal: "0 < m \<Longrightarrow> m < ord n a \<Longrightarrow> ~[a^m = 1] (mod n)"
using ord_works by blast
lemma ord_eq_0: "ord n a = 0 \<longleftrightarrow> ~coprime n a"
-by (cases "coprime n a", simp add: neq0_conv coprime_ord, simp add: neq0_conv ord_def)
+by (cases "coprime n a", simp add: coprime_ord, simp add: ord_def)
lemma ord_divides:
"[a ^ d = 1] (mod n) \<longleftrightarrow> ord n a dvd d" (is "?lhs \<longleftrightarrow> ?rhs")
@@ -952,8 +954,7 @@
{fix d assume d: "d dvd n" "d^2 \<le> n" and H: "\<forall>m. m dvd n \<longrightarrow> m=1 \<or> m=n"
from H d have d1n: "d = 1 \<or> d=n" by blast
{assume dn: "d=n"
- have "n^2 > n*1" using n
- by (simp add: power2_eq_square mult_less_cancel1)
+ have "n^2 > n*1" using n by (simp add: power2_eq_square)
with dn d(2) have "d=1" by simp}
with d1n have "d = 1" by blast }
moreover
@@ -985,7 +986,11 @@
{assume n: "n\<noteq>0" "n\<noteq>1"
{assume H: ?lhs
from H[unfolded prime_divisor_sqrt] n
- have ?rhs apply clarsimp by (erule_tac x="p" in allE, simp add: prime_1)
+ have ?rhs
+ apply clarsimp
+ apply (erule_tac x="p" in allE)
+ apply simp
+ done
}
moreover
{assume H: ?rhs
@@ -1018,7 +1023,7 @@
hence "a^ (n - 1) = 0" using n by (simp add: power_0_left)
with n an mod_less[of 1 n] have False by (simp add: power_0_left modeq_def)}
hence a0: "a\<noteq>0" ..
- from n nqr have aqr0: "a ^ (q * r) \<noteq> 0" using a0 by (simp add: neq0_conv)
+ from n nqr have aqr0: "a ^ (q * r) \<noteq> 0" using a0 by simp
hence "(a ^ (q * r) - 1) + 1 = a ^ (q * r)" by simp
with k l have "a ^ (q * r) = p*l*k + 1" by simp
hence "a ^ (r * q) + p * 0 = 1 + p * (l*k)" by (simp add: mult_ac)
@@ -1055,7 +1060,7 @@
from n have n0: "n \<noteq> 0" by simp
from d(2) an n12[symmetric] have a0: "a \<noteq> 0"
by - (rule ccontr, simp add: modeq_def)
- have th1: "a^ (n - 1) \<noteq> 0" using n d(2) dp a0 by (auto simp add: neq0_conv)
+ have th1: "a^ (n - 1) \<noteq> 0" using n d(2) dp a0 by auto
from coprime_minus1[OF th1, unfolded coprime]
dvd_trans[OF pn cong_1_divides[OF an]] th0 d(3) dp
have False by auto}
--- a/src/HOL/Old_Number_Theory/Primes.thy Thu Jan 13 21:50:13 2011 +0100
+++ b/src/HOL/Old_Number_Theory/Primes.thy Thu Jan 13 23:50:16 2011 +0100
@@ -222,7 +222,7 @@
thus ?thesis unfolding coprime_def .
qed
lemma coprime_lmul2: assumes dab: "coprime d (a * b)" shows "coprime d b"
-using prems unfolding coprime_bezout
+using dab unfolding coprime_bezout
apply clarsimp
apply (case_tac "d * x - a * b * y = Suc 0 ", simp_all)
apply (rule_tac x="x" in exI)
@@ -283,7 +283,8 @@
apply (simp only: z power_0_Suc)
apply (rule exI[where x=0])
apply (rule exI[where x=0])
- by simp}
+ apply simp
+ done }
moreover
{assume z: "?g \<noteq> 0"
from gcd_dvd1[of a b] gcd_dvd2[of a b] obtain a' b' where
@@ -350,7 +351,7 @@
{assume "?g = 0" with ab n have ?thesis by (simp add: gcd_zero)}
moreover
{assume z: "?g \<noteq> 0"
- hence zn: "?g ^ n \<noteq> 0" using n by (simp add: neq0_conv)
+ hence zn: "?g ^ n \<noteq> 0" using n by simp
from gcd_coprime_exists[OF z]
obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'" by blast
from ab have "(a' * ?g) ^ n dvd (b' * ?g)^n" by (simp add: ab'(1,2)[symmetric])
@@ -637,8 +638,9 @@
assume ?rhs then show ?lhs by auto
qed
-lemma power_Suc0[simp]: "Suc 0 ^ n = Suc 0"
+lemma power_Suc0: "Suc 0 ^ n = Suc 0"
unfolding One_nat_def[symmetric] power_one ..
+
lemma coprime_pow: assumes ab: "coprime a b" and abcn: "a * b = c ^n"
shows "\<exists>r s. a = r^n \<and> b = s ^n"
using ab abcn
@@ -678,7 +680,7 @@
from prime_divprod_pow[OF p(1) H(2), unfolded H(3), OF divides_exp[OF p(2), of n]]
have pnab: "p ^ n dvd a \<or> p^n dvd b" .
from p(2) obtain l where l: "c = p*l" unfolding dvd_def by blast
- have pn0: "p^n \<noteq> 0" using n prime_ge_2 [OF p(1)] by (simp add: neq0_conv)
+ have pn0: "p^n \<noteq> 0" using n prime_ge_2 [OF p(1)] by simp
{assume pa: "p^n dvd a"
then obtain k where k: "a = p^n * k" unfolding dvd_def by blast
from l have "l dvd c" by auto
@@ -785,8 +787,7 @@
case 0 thus ?case by simp
next
case (Suc n k) hence th: "x*x^n = p^k" by simp
- {assume "n = 0" with prems have ?case apply simp
- by (rule exI[where x="k"],simp)}
+ {assume "n = 0" with Suc have ?case by simp (rule exI[where x="k"], simp)}
moreover
{assume n: "n \<noteq> 0"
from prime_power_mult[OF p th]
--- a/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy Thu Jan 13 21:50:13 2011 +0100
+++ b/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy Thu Jan 13 23:50:16 2011 +0100
@@ -201,10 +201,11 @@
then show ?thesis by auto
qed
-lemma pb_neq_qa: "[|1 \<le> b; b \<le> (q - 1) div 2 |] ==>
- (p * b \<noteq> q * a)"
+lemma pb_neq_qa:
+ assumes "1 \<le> b" and "b \<le> (q - 1) div 2"
+ shows "p * b \<noteq> q * a"
proof
- assume "p * b = q * a" and "1 \<le> b" and "b \<le> (q - 1) div 2"
+ assume "p * b = q * a"
then have "q dvd (p * b)" by (auto simp add: dvd_def)
with q_prime p_g_2 have "q dvd p | q dvd b"
by (auto simp add: zprime_zdvd_zmult)
@@ -216,7 +217,7 @@
apply (drule_tac x = q and R = False in allE)
apply (simp add: QRTEMP_def)
apply (subgoal_tac "0 \<le> q", simp add: QRTEMP_def)
- apply (insert prems)
+ apply (insert assms)
apply (auto simp add: QRTEMP_def)
done
with q_g_2 p_neq_q show False by auto
@@ -225,18 +226,18 @@
then have "q \<le> b"
proof -
assume "q dvd b"
- moreover from prems have "0 < b" by auto
+ moreover from assms have "0 < b" by auto
ultimately show ?thesis using zdvd_bounds [of q b] by auto
qed
- with prems have "q \<le> (q - 1) div 2" by auto
+ with assms have "q \<le> (q - 1) div 2" by auto
then have "2 * q \<le> 2 * ((q - 1) div 2)" by arith
then have "2 * q \<le> q - 1"
proof -
- assume "2 * q \<le> 2 * ((q - 1) div 2)"
- with prems have "q \<in> zOdd" by (auto simp add: QRTEMP_def zprime_zOdd_eq_grt_2)
+ assume a: "2 * q \<le> 2 * ((q - 1) div 2)"
+ with assms have "q \<in> zOdd" by (auto simp add: QRTEMP_def zprime_zOdd_eq_grt_2)
with odd_minus_one_even have "(q - 1):zEven" by auto
with even_div_2_prop2 have "(q - 1) = 2 * ((q - 1) div 2)" by auto
- with prems show ?thesis by auto
+ with a show ?thesis by auto
qed
then have p1: "q \<le> -1" by arith
with q_g_2 show False by auto
@@ -273,7 +274,7 @@
lemma S_card: "((p - 1) div 2) * ((q - 1) div 2) = int (card(S))"
using P_set_card Q_set_card P_set_finite Q_set_finite
- by (auto simp add: S_def zmult_int setsum_constant)
+ by (auto simp add: S_def zmult_int)
lemma S1_Int_S2_prop: "S1 \<inter> S2 = {}"
by (auto simp add: S1_def S2_def)
@@ -301,11 +302,11 @@
finally show ?thesis .
qed
-lemma aux1a: "[| 0 < a; a \<le> (p - 1) div 2;
- 0 < b; b \<le> (q - 1) div 2 |] ==>
- (p * b < q * a) = (b \<le> q * a div p)"
+lemma aux1a:
+ assumes "0 < a" and "a \<le> (p - 1) div 2"
+ and "0 < b" and "b \<le> (q - 1) div 2"
+ shows "(p * b < q * a) = (b \<le> q * a div p)"
proof -
- assume "0 < a" and "a \<le> (p - 1) div 2" and "0 < b" and "b \<le> (q - 1) div 2"
have "p * b < q * a ==> b \<le> q * a div p"
proof -
assume "p * b < q * a"
@@ -329,17 +330,17 @@
then have "p * b < q * a | p * b = q * a"
by (simp only: order_le_imp_less_or_eq)
moreover have "p * b \<noteq> q * a"
- by (rule pb_neq_qa) (insert prems, auto)
+ by (rule pb_neq_qa) (insert assms, auto)
ultimately show ?thesis by auto
qed
ultimately show ?thesis ..
qed
-lemma aux1b: "[| 0 < a; a \<le> (p - 1) div 2;
- 0 < b; b \<le> (q - 1) div 2 |] ==>
- (q * a < p * b) = (a \<le> p * b div q)"
+lemma aux1b:
+ assumes "0 < a" and "a \<le> (p - 1) div 2"
+ and "0 < b" and "b \<le> (q - 1) div 2"
+ shows "(q * a < p * b) = (a \<le> p * b div q)"
proof -
- assume "0 < a" and "a \<le> (p - 1) div 2" and "0 < b" and "b \<le> (q - 1) div 2"
have "q * a < p * b ==> a \<le> p * b div q"
proof -
assume "q * a < p * b"
@@ -363,18 +364,18 @@
then have "q * a < p * b | q * a = p * b"
by (simp only: order_le_imp_less_or_eq)
moreover have "p * b \<noteq> q * a"
- by (rule pb_neq_qa) (insert prems, auto)
+ by (rule pb_neq_qa) (insert assms, auto)
ultimately show ?thesis by auto
qed
ultimately show ?thesis ..
qed
-lemma (in -) aux2: "[| zprime p; zprime q; 2 < p; 2 < q |] ==>
- (q * ((p - 1) div 2)) div p \<le> (q - 1) div 2"
+lemma (in -) aux2:
+ assumes "zprime p" and "zprime q" and "2 < p" and "2 < q"
+ shows "(q * ((p - 1) div 2)) div p \<le> (q - 1) div 2"
proof-
- assume "zprime p" and "zprime q" and "2 < p" and "2 < q"
(* Set up what's even and odd *)
- then have "p \<in> zOdd & q \<in> zOdd"
+ from assms have "p \<in> zOdd & q \<in> zOdd"
by (auto simp add: zprime_zOdd_eq_grt_2)
then have even1: "(p - 1):zEven & (q - 1):zEven"
by (auto simp add: odd_minus_one_even)
@@ -383,7 +384,7 @@
then have even3: "(((q - 1) * p) + (2 * p)):zEven"
by (auto simp: EvenOdd.even_plus_even)
(* using these prove it *)
- from prems have "q * (p - 1) < ((q - 1) * p) + (2 * p)"
+ from assms have "q * (p - 1) < ((q - 1) * p) + (2 * p)"
by (auto simp add: int_distrib)
then have "((p - 1) * q) div 2 < (((q - 1) * p) + (2 * p)) div 2"
apply (rule_tac x = "((p - 1) * q)" in even_div_2_l)
@@ -395,7 +396,7 @@
finally show ?thesis
apply (rule_tac x = " q * ((p - 1) div 2)" and
y = "(q - 1) div 2" in div_prop2)
- using prems by auto
+ using assms by auto
qed
lemma aux3a: "\<forall>j \<in> P_set. int (card (f1 j)) = (q * j) div p"
@@ -414,7 +415,7 @@
ultimately have "card ((%(x,y). y) ` (f1 j)) = card (f1 j)"
by (auto simp add: f1_def card_image)
moreover have "((%(x,y). y) ` (f1 j)) = {y. y \<in> Q_set & y \<le> (q * j) div p}"
- using prems by (auto simp add: f1_def S_def Q_set_def P_set_def image_def)
+ using j_fact by (auto simp add: f1_def S_def Q_set_def P_set_def image_def)
ultimately show ?thesis by (auto simp add: f1_def)
qed
also have "... = int (card {y. 0 < y & y \<le> (q * j) div p})"
@@ -424,18 +425,18 @@
apply (auto simp add: Q_set_def)
proof -
fix x
- assume "0 < x" and "x \<le> q * j div p"
+ assume x: "0 < x" "x \<le> q * j div p"
with j_fact P_set_def have "j \<le> (p - 1) div 2" by auto
with q_g_2 have "q * j \<le> q * ((p - 1) div 2)"
by (auto simp add: mult_le_cancel_left)
with p_g_2 have "q * j div p \<le> q * ((p - 1) div 2) div p"
by (auto simp add: zdiv_mono1)
- also from prems P_set_def have "... \<le> (q - 1) div 2"
+ also from QRTEMP_axioms j_fact P_set_def have "... \<le> (q - 1) div 2"
apply simp
apply (insert aux2)
apply (simp add: QRTEMP_def)
done
- finally show "x \<le> (q - 1) div 2" using prems by auto
+ finally show "x \<le> (q - 1) div 2" using x by auto
qed
then show ?thesis by auto
qed
@@ -470,7 +471,7 @@
ultimately have "card ((%(x,y). x) ` (f2 j)) = card (f2 j)"
by (auto simp add: f2_def card_image)
moreover have "((%(x,y). x) ` (f2 j)) = {y. y \<in> P_set & y \<le> (p * j) div q}"
- using prems by (auto simp add: f2_def S_def Q_set_def P_set_def image_def)
+ using j_fact by (auto simp add: f2_def S_def Q_set_def P_set_def image_def)
ultimately show ?thesis by (auto simp add: f2_def)
qed
also have "... = int (card {y. 0 < y & y \<le> (p * j) div q})"
@@ -480,15 +481,15 @@
apply (auto simp add: P_set_def)
proof -
fix x
- assume "0 < x" and "x \<le> p * j div q"
+ assume x: "0 < x" "x \<le> p * j div q"
with j_fact Q_set_def have "j \<le> (q - 1) div 2" by auto
with p_g_2 have "p * j \<le> p * ((q - 1) div 2)"
by (auto simp add: mult_le_cancel_left)
with q_g_2 have "p * j div q \<le> p * ((q - 1) div 2) div q"
by (auto simp add: zdiv_mono1)
- also from prems have "... \<le> (p - 1) div 2"
+ also from QRTEMP_axioms j_fact have "... \<le> (p - 1) div 2"
by (auto simp add: aux2 QRTEMP_def)
- finally show "x \<le> (p - 1) div 2" using prems by auto
+ finally show "x \<le> (p - 1) div 2" using x by auto
qed
then show ?thesis by auto
qed
@@ -587,18 +588,18 @@
lemma QR_short: "(Legendre p q) * (Legendre q p) =
(-1::int)^nat(((p - 1) div 2)*((q - 1) div 2))"
proof -
- from prems have "~([p = 0] (mod q))"
+ from QRTEMP_axioms have "~([p = 0] (mod q))"
by (auto simp add: pq_prime_neq QRTEMP_def)
- with prems Q_set_def have a1: "(Legendre p q) = (-1::int) ^
+ with QRTEMP_axioms Q_set_def have a1: "(Legendre p q) = (-1::int) ^
nat(setsum (%x. ((x * p) div q)) Q_set)"
apply (rule_tac p = q in MainQRLemma)
apply (auto simp add: zprime_zOdd_eq_grt_2 QRTEMP_def)
done
- from prems have "~([q = 0] (mod p))"
+ from QRTEMP_axioms have "~([q = 0] (mod p))"
apply (rule_tac p = q and q = p in pq_prime_neq)
apply (simp add: QRTEMP_def)+
done
- with prems P_set_def have a2: "(Legendre q p) =
+ with QRTEMP_axioms P_set_def have a2: "(Legendre q p) =
(-1::int) ^ nat(setsum (%x. ((x * q) div p)) P_set)"
apply (rule_tac p = p in MainQRLemma)
apply (auto simp add: zprime_zOdd_eq_grt_2 QRTEMP_def)
--- a/src/HOL/Old_Number_Theory/Residues.thy Thu Jan 13 21:50:13 2011 +0100
+++ b/src/HOL/Old_Number_Theory/Residues.thy Thu Jan 13 23:50:16 2011 +0100
@@ -51,10 +51,10 @@
mod_mult_eq [of x y m])
lemma StandardRes_lbound: "0 < p ==> 0 \<le> StandardRes p x"
- by (auto simp add: StandardRes_def pos_mod_sign)
+ by (auto simp add: StandardRes_def)
lemma StandardRes_ubound: "0 < p ==> StandardRes p x < p"
- by (auto simp add: StandardRes_def pos_mod_bound)
+ by (auto simp add: StandardRes_def)
lemma StandardRes_eq_zcong:
"(StandardRes m x = 0) = ([x = 0](mod m))"
@@ -71,8 +71,7 @@
lemma StandardRes_SRStar_prop1: "2 < p ==> (StandardRes p x \<in> SRStar p)
= (~[x = 0] (mod p))"
- apply (auto simp add: StandardRes_prop3 StandardRes_def
- SRStar_def pos_mod_bound)
+ apply (auto simp add: StandardRes_prop3 StandardRes_def SRStar_def)
apply (subgoal_tac "0 < p")
apply (drule_tac a = x in pos_mod_sign, arith, simp)
done
--- a/src/HOL/ex/Dedekind_Real.thy Thu Jan 13 21:50:13 2011 +0100
+++ b/src/HOL/ex/Dedekind_Real.thy Thu Jan 13 23:50:16 2011 +0100
@@ -354,30 +354,29 @@
text{*Part 2 of Dedekind sections definition*}
lemma preal_not_mem_mult_set_Ex:
- assumes A: "A \<in> preal"
- and B: "B \<in> preal"
- shows "\<exists>q. 0 < q & q \<notin> mult_set A B"
+ assumes A: "A \<in> preal"
+ and B: "B \<in> preal"
+ shows "\<exists>q. 0 < q & q \<notin> mult_set A B"
proof -
- from preal_exists_bound [OF A]
- obtain x where [simp]: "0 < x" "x \<notin> A" by blast
- from preal_exists_bound [OF B]
- obtain y where [simp]: "0 < y" "y \<notin> B" by blast
+ from preal_exists_bound [OF A] obtain x where 1 [simp]: "0 < x" "x \<notin> A" by blast
+ from preal_exists_bound [OF B] obtain y where 2 [simp]: "0 < y" "y \<notin> B" by blast
show ?thesis
proof (intro exI conjI)
show "0 < x*y" by (simp add: mult_pos_pos)
show "x * y \<notin> mult_set A B"
proof -
- { fix u::rat and v::rat
- assume "u \<in> A" and "v \<in> B" and "x*y = u*v"
- moreover
- with prems have "u<x" and "v<y" by (blast dest: not_in_preal_ub)+
- moreover
- with prems have "0\<le>v"
- by (blast intro: preal_imp_pos [OF B] order_less_imp_le prems)
- moreover
- from calculation
- have "u*v < x*y" by (blast intro: mult_strict_mono prems)
- ultimately have False by force }
+ {
+ fix u::rat and v::rat
+ assume u: "u \<in> A" and v: "v \<in> B" and xy: "x*y = u*v"
+ moreover from A B 1 2 u v have "u<x" and "v<y" by (blast dest: not_in_preal_ub)+
+ moreover
+ from A B 1 2 u v have "0\<le>v"
+ by (blast intro: preal_imp_pos [OF B] order_less_imp_le)
+ moreover
+ from A B 1 `u < x` `v < y` `0 \<le> v`
+ have "u*v < x*y" by (blast intro: mult_strict_mono)
+ ultimately have False by force
+ }
thus ?thesis by (auto simp add: mult_set_def)
qed
qed
@@ -473,7 +472,7 @@
fix x::rat and u::rat and v::rat
assume upos: "0<u" and "u<1" and v: "v \<in> A"
have vpos: "0<v" by (rule preal_imp_pos [OF A v])
- hence "u*v < 1*v" by (simp only: mult_strict_right_mono prems)
+ hence "u*v < 1*v" by (simp only: mult_strict_right_mono upos `u < 1` v)
thus "u * v \<in> A"
by (force intro: preal_downwards_closed [OF A v] mult_pos_pos
upos vpos)
@@ -673,18 +672,19 @@
proof (cases z rule: int_cases)
case (nonneg n)
show ?thesis
- proof (simp add: prems, induct n)
+ proof (simp add: nonneg, induct n)
case 0
- from preal_nonempty [OF A]
- show ?case by force
+ from preal_nonempty [OF A]
+ show ?case by force
+ next
case (Suc k)
- from this obtain b where "b \<in> A" "b + of_nat k * u \<in> A" ..
- hence "b + of_int (int k)*u + u \<in> A" by (simp add: prems)
- thus ?case by (force simp add: algebra_simps prems)
+ then obtain b where b: "b \<in> A" "b + of_nat k * u \<in> A" ..
+ hence "b + of_int (int k)*u + u \<in> A" by (simp add: assms)
+ thus ?case by (force simp add: algebra_simps b)
qed
next
case (neg n)
- with prems show ?thesis by simp
+ with assms show ?thesis by simp
qed
lemma Gleason9_34_contra:
@@ -987,10 +987,9 @@
proof -
have "0<a" by (rule preal_imp_pos [OF Rep_preal a])
moreover
- have "a < c" using prems
- by (blast intro: not_in_Rep_preal_ub )
- ultimately show ?thesis using prems
- by (simp add: preal_downwards_closed [OF Rep_preal cb])
+ have "a < c" using assms by (blast intro: not_in_Rep_preal_ub )
+ ultimately show ?thesis
+ using assms by (simp add: preal_downwards_closed [OF Rep_preal cb])
qed
lemma less_add_left_le1:
@@ -1225,13 +1224,13 @@
lemma preal_trans_lemma:
assumes "x + y1 = x1 + y"
- and "x + y2 = x2 + y"
+ and "x + y2 = x2 + y"
shows "x1 + y2 = x2 + (y1::preal)"
proof -
have "(x1 + y2) + x = (x + y2) + x1" by (simp add: add_ac)
- also have "... = (x2 + y) + x1" by (simp add: prems)
+ also have "... = (x2 + y) + x1" by (simp add: assms)
also have "... = x2 + (x1 + y)" by (simp add: add_ac)
- also have "... = x2 + (x + y1)" by (simp add: prems)
+ also have "... = x2 + (x + y1)" by (simp add: assms)
also have "... = (x2 + y1) + x" by (simp add: add_ac)
finally have "(x1 + y2) + x = (x2 + y1) + x" .
thus ?thesis by (rule add_right_imp_eq)
@@ -1436,20 +1435,20 @@
assumes eq: "a+b = c+d" and le: "c \<le> a"
shows "b \<le> (d::preal)"
proof -
- have "c+d \<le> a+d" by (simp add: prems)
- hence "a+b \<le> a+d" by (simp add: prems)
+ have "c+d \<le> a+d" by (simp add: le)
+ hence "a+b \<le> a+d" by (simp add: eq)
thus "b \<le> d" by simp
qed
lemma real_le_lemma:
assumes l: "u1 + v2 \<le> u2 + v1"
- and "x1 + v1 = u1 + y1"
- and "x2 + v2 = u2 + y2"
+ and "x1 + v1 = u1 + y1"
+ and "x2 + v2 = u2 + y2"
shows "x1 + y2 \<le> x2 + (y1::preal)"
proof -
- have "(x1+v1) + (u2+y2) = (u1+y1) + (x2+v2)" by (simp add: prems)
+ have "(x1+v1) + (u2+y2) = (u1+y1) + (x2+v2)" by (simp add: assms)
hence "(x1+y2) + (u2+v1) = (x2+y1) + (u1+v2)" by (simp add: add_ac)
- also have "... \<le> (x2+y1) + (u2+v1)" by (simp add: prems)
+ also have "... \<le> (x2+y1) + (u2+v1)" by (simp add: assms)
finally show ?thesis by simp
qed
@@ -1465,13 +1464,13 @@
lemma real_trans_lemma:
assumes "x + v \<le> u + y"
- and "u + v' \<le> u' + v"
- and "x2 + v2 = u2 + y2"
+ and "u + v' \<le> u' + v"
+ and "x2 + v2 = u2 + y2"
shows "x + v' \<le> u' + (y::preal)"
proof -
have "(x+v') + (u+v) = (x+v) + (u+v')" by (simp add: add_ac)
- also have "... \<le> (u+y) + (u+v')" by (simp add: prems)
- also have "... \<le> (u+y) + (u'+v)" by (simp add: prems)
+ also have "... \<le> (u+y) + (u+v')" by (simp add: assms)
+ also have "... \<le> (u+y) + (u'+v)" by (simp add: assms)
also have "... = (u'+y) + (u+v)" by (simp add: add_ac)
finally show ?thesis by simp
qed
@@ -1947,7 +1946,7 @@
proof -
have "\<exists>x. isLub UNIV S x"
by (rule reals_complete)
- (auto simp add: isLub_def isUb_def leastP_def setle_def setge_def prems)
+ (auto simp add: isLub_def isUb_def leastP_def setle_def setge_def assms)
thus ?thesis
by (metis UNIV_I isLub_isUb isLub_le_isUb isUbD isUb_def setleI)
qed