# HG changeset patch # User wenzelm # Date 1294959016 -3600 # Node ID 1fa4725c4656bce67605cc05e02819616c21249e # Parent 414a68d72279f9471be06ced3c34ad4e655dc4a7 eliminated global prems; tuned proofs; diff -r 414a68d72279 -r 1fa4725c4656 src/HOL/Algebra/Sylow.thy --- 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 \ calM" and g: "g \ carrier G" hence "y = y #> g #> (inv g)" by (simp add: coset_mult_assoc calM_def) - thus "\g'\carrier G. y = y #> g #> g'" - by (blast intro: g inv_closed) + thus "\g'\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\H; y\H|] ==> x \ y \ 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 \ {}" @@ -205,16 +204,16 @@ lemma (in sylow_central) M1_cardeq_rcosetGM1g: "g \ 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 \ carrier G ==> (M1, M1 #> g) \ 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 @@ "(\C \ rcosets H. M1 #> (@g. g \ carrier G \ H #> g = C)) \ rcosets H \ 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 \ 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 diff -r 414a68d72279 -r 1fa4725c4656 src/HOL/Metis_Examples/BigO.thy --- 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 diff -r 414a68d72279 -r 1fa4725c4656 src/HOL/MicroJava/DFA/Err.thy --- 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 @@ \ semilat (A,r,f); x +_f y <=_r z; x:A; y:A; z:A \ \ x <=_r z \ 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]) diff -r 414a68d72279 -r 1fa4725c4656 src/HOL/MicroJava/DFA/Kildall.thy --- 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 diff -r 414a68d72279 -r 1fa4725c4656 src/HOL/MicroJava/DFA/Product.thy --- 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 @@ "\r f z. \ z : err A; semilat (err A, r, f); OK x : err A; OK y : err A; OK x +_f OK y <=_r z\ \ OK x <=_r z \ 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]) diff -r 414a68d72279 -r 1fa4725c4656 src/HOL/NSA/NSA.thy --- 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 \ HFinite" and "y \ HFinite" and "x @= y" + assumes x: "x \ HFinite" and y: "y \ HFinite" and xy: "x @= y" shows "st x = st y" proof - have "st x @= x" "st y @= y" "st x \ Reals" "st y \ 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 diff -r 414a68d72279 -r 1fa4725c4656 src/HOL/Number_Theory/Binomial.thy --- 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) \ n \ 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 \ insert x F \ card T = k + 1} = {T. T \ F & card T = k + 1} Un {T. T \ insert x F & x : T & card T = k + 1}" - by (auto intro!: subsetI) + by auto with iassms fin have "card ({T. T \ insert x F \ card T = k + 1}) = card ({T. T \ F \ card T = k + 1}) + card ({T. T \ insert x F \ x : T \ 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]) diff -r 414a68d72279 -r 1fa4725c4656 src/HOL/Number_Theory/Cong.thy --- 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 \ 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) \ [c = d] (mod m) \ [a * c = b * d] (mod m)" @@ -242,13 +234,13 @@ lemma cong_exp_nat: "[(x::nat) = y] (mod n) \ [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) \ [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)) \ @@ -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) \ @@ -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 @@ \ [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 \ (a::nat) \ a < m \ 0 \ b \ b < m \ [a = b] (mod m) \ 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 \ (a::int) \ a < m \ 0 \ b \ b < m \ [a = b] (mod m) \ 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) \ (\!b. 0 \ b \ b < m \ [a = b] (mod m))" @@ -412,8 +401,8 @@ "0 < (m::int) \ (\!b. 0 \ b \ b < m \ [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)) = (\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) \ coprime a m \ 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: diff -r 414a68d72279 -r 1fa4725c4656 src/HOL/Number_Theory/Fib.thy --- 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 \ n >= 0 \ fib (gcd (m::int) n) = gcd (fib m) (fib n)" @@ -306,7 +303,7 @@ "fib ((n::nat) + 1) * fib n = (\k \ {..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 = (\k \ {..n}. fib k * fib k)" diff -r 414a68d72279 -r 1fa4725c4656 src/HOL/Number_Theory/MiscAlgebra.thy --- 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: "\\<^bsub>R\<^esub> ~= \\<^bsub>R\<^esub> \ ALL x : carrier R - {\\<^bsub>R\<^esub>}. x : Units R \ field R" apply (unfold_locales) - apply (insert prems, auto) + apply (insert cring_axioms, auto) apply (rule trans) apply (subgoal_tac "a = (a \ b) \ 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 \ y : carrier G \ - x \ y = \ \ y \ x = \ \ inv x = y" + x \ y = \ \ y \ x = \ \ inv x = y" apply (subgoal_tac "x : Units G") apply (subgoal_tac "y = inv x \ \") 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 \ y : carrier G \ x \ y = \ \ inv x = y" apply (rule inv_char) apply auto apply (subst m_comm, auto) -done + done lemma (in ring) inv_neg_one [simp]: "inv (\ \) = \ \" apply (rule inv_char) apply (auto simp add: l_minus r_minus) -done + done lemma (in monoid) inv_eq_imp_eq: "x : Units G \ y : Units G \ inv x = inv y \ x = y" @@ -281,8 +281,8 @@ apply (subgoal_tac "\ y = \ \ \ 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 \ 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) \ a : Units R \ a (^) card(Units R) = \" @@ -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 diff -r 414a68d72279 -r 1fa4725c4656 src/HOL/Number_Theory/Residues.thy --- 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: "\ = 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: "\ 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) \ (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: "\ = 0" apply (unfold R_def residue_ring_def, auto) -done + done lemma one_cong: "\ = 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: "\ (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 \ (\ 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 \ (\ 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 \ coprime a m \ 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 \ 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 \ y : Units R \ - {x, inv x} ~= {y, inv y} \ {x, inv x} Int {y, inv y} = {}" + {x, inv x} ~= {y, inv y} \ {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 "(\i:(Union ?InversePairs). i) = - (\ A: ?InversePairs. (\ y:A. y))" + (\A: ?InversePairs. (\y:A. y))" apply (subst finprod_Union_disjoint) apply force apply force @@ -441,7 +440,7 @@ done also have "\ = 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 = \ \". diff -r 414a68d72279 -r 1fa4725c4656 src/HOL/Number_Theory/UniqueFactorization.thy --- 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 \ 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 \ 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 \ l > 0 \ 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) diff -r 414a68d72279 -r 1fa4725c4656 src/HOL/Old_Number_Theory/Euler.thy --- 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; \X \ S. finite (X::int set); \X \ 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) |] ==> - [\(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 "[\(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 "[\(Union (SetS a p)) = - setprod (setprod (%x. x)) (SetS a p)] (mod p)" + from assms have "[\(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)) |] ==> - \(Union (SetS a p)) = zfact (p - 1)" +lemma Union_SetS_setprod_prop2: + assumes "zprime p" and "2 < p" and "~([a = 0](mod p))" + shows "\(Union (SetS a p)) = zfact (p - 1)" proof - - assume "zprime p" and "2 < p" and "~([a = 0](mod p))" - then have "\(Union (SetS a p)) = \(SRStar p)" + from assms have "\(Union (SetS a p)) = \(SRStar p)" by (auto simp add: MultInvPair_prop2) also have "... = \({1} \ (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 \ d22set (p - 1)) & finite( d22set (p - 1))" diff -r 414a68d72279 -r 1fa4725c4656 src/HOL/Old_Number_Theory/Gauss.thy --- 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" diff -r 414a68d72279 -r 1fa4725c4656 src/HOL/Old_Number_Theory/Int2.thy --- 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 \ 0" by simp + from `0 < z` have modth: "x mod z \ 0" by simp have "(x div z) * z \ (x div z) * z" by simp then have "(x div z) * z \ (x div z) * z + x mod z" using modth by arith also have "\ = 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 \ y" +lemma div_prop2: + assumes "0 < z" and "(x::int) < (y * z) + z" + shows "x div z \ 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) \ (x::int)" +lemma zdiv_leq_prop: assumes "0 < y" shows "y * (x div y) \ (x::int)" proof- - assume "0 < y" from zmod_zdiv_equality have "x = y * (x div y) + x mod y" by auto - moreover have "0 \ x mod y" - by (auto simp add: prems pos_mod_sign) - ultimately show ?thesis - by arith + moreover have "0 \ 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 diff -r 414a68d72279 -r 1fa4725c4656 src/HOL/Old_Number_Theory/IntPrimes.thy --- 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) diff -r 414a68d72279 -r 1fa4725c4656 src/HOL/Old_Number_Theory/Legacy_GCD.thy --- 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 "\d x y. d dvd a \ d dvd a + b \ (a * x = (a + b) * y + d \ (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 \ 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 \ 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 \ int \ 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 \ 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) diff -r 414a68d72279 -r 1fa4725c4656 src/HOL/Old_Number_Theory/Pocklington.thy --- 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\0" "n\1" and a:"a\0" "a \ 1" hence a': "a \ 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) \ ?S" using nz - by (simp add: coprime_mod[OF nz] mod_less_divisor)} + by (simp add: coprime_mod[OF nz])} thus " \x\{m. coprime m n \ m < n}. ((\m. m mod n) \ op * a) x \ {m. coprime m n \ m < n} \ ((\m. m mod n) \ op * a) x = ((\m. m mod n) \ op * a) x" by simp @@ -821,7 +823,7 @@ lemma ord_minimal: "0 < m \ m < ord n a \ ~[a^m = 1] (mod n)" using ord_works by blast lemma ord_eq_0: "ord n a = 0 \ ~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) \ ord n a dvd d" (is "?lhs \ ?rhs") @@ -952,8 +954,7 @@ {fix d assume d: "d dvd n" "d^2 \ n" and H: "\m. m dvd n \ m=1 \ m=n" from H d have d1n: "d = 1 \ 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\0" "n\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\0" .. - from n nqr have aqr0: "a ^ (q * r) \ 0" using a0 by (simp add: neq0_conv) + from n nqr have aqr0: "a ^ (q * r) \ 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 \ 0" by simp from d(2) an n12[symmetric] have a0: "a \ 0" by - (rule ccontr, simp add: modeq_def) - have th1: "a^ (n - 1) \ 0" using n d(2) dp a0 by (auto simp add: neq0_conv) + have th1: "a^ (n - 1) \ 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} diff -r 414a68d72279 -r 1fa4725c4656 src/HOL/Old_Number_Theory/Primes.thy --- 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 \ 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 \ 0" - hence zn: "?g ^ n \ 0" using n by (simp add: neq0_conv) + hence zn: "?g ^ n \ 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 "\r s. a = r^n \ 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 \ p^n dvd b" . from p(2) obtain l where l: "c = p*l" unfolding dvd_def by blast - have pn0: "p^n \ 0" using n prime_ge_2 [OF p(1)] by (simp add: neq0_conv) + have pn0: "p^n \ 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 \ 0" from prime_power_mult[OF p th] diff -r 414a68d72279 -r 1fa4725c4656 src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy --- 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 \ b; b \ (q - 1) div 2 |] ==> - (p * b \ q * a)" +lemma pb_neq_qa: + assumes "1 \ b" and "b \ (q - 1) div 2" + shows "p * b \ q * a" proof - assume "p * b = q * a" and "1 \ b" and "b \ (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 \ 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 \ 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 \ (q - 1) div 2" by auto + with assms have "q \ (q - 1) div 2" by auto then have "2 * q \ 2 * ((q - 1) div 2)" by arith then have "2 * q \ q - 1" proof - - assume "2 * q \ 2 * ((q - 1) div 2)" - with prems have "q \ zOdd" by (auto simp add: QRTEMP_def zprime_zOdd_eq_grt_2) + assume a: "2 * q \ 2 * ((q - 1) div 2)" + with assms have "q \ 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 \ -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 \ S2 = {}" by (auto simp add: S1_def S2_def) @@ -301,11 +302,11 @@ finally show ?thesis . qed -lemma aux1a: "[| 0 < a; a \ (p - 1) div 2; - 0 < b; b \ (q - 1) div 2 |] ==> - (p * b < q * a) = (b \ q * a div p)" +lemma aux1a: + assumes "0 < a" and "a \ (p - 1) div 2" + and "0 < b" and "b \ (q - 1) div 2" + shows "(p * b < q * a) = (b \ q * a div p)" proof - - assume "0 < a" and "a \ (p - 1) div 2" and "0 < b" and "b \ (q - 1) div 2" have "p * b < q * a ==> b \ 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 \ 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 \ (p - 1) div 2; - 0 < b; b \ (q - 1) div 2 |] ==> - (q * a < p * b) = (a \ p * b div q)" +lemma aux1b: + assumes "0 < a" and "a \ (p - 1) div 2" + and "0 < b" and "b \ (q - 1) div 2" + shows "(q * a < p * b) = (a \ p * b div q)" proof - - assume "0 < a" and "a \ (p - 1) div 2" and "0 < b" and "b \ (q - 1) div 2" have "q * a < p * b ==> a \ 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 \ 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 \ (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 \ (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 \ zOdd & q \ zOdd" + from assms have "p \ zOdd & q \ 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: "\j \ 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 \ Q_set & y \ (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 \ (q * j) div p})" @@ -424,18 +425,18 @@ apply (auto simp add: Q_set_def) proof - fix x - assume "0 < x" and "x \ q * j div p" + assume x: "0 < x" "x \ q * j div p" with j_fact P_set_def have "j \ (p - 1) div 2" by auto with q_g_2 have "q * j \ q * ((p - 1) div 2)" by (auto simp add: mult_le_cancel_left) with p_g_2 have "q * j div p \ q * ((p - 1) div 2) div p" by (auto simp add: zdiv_mono1) - also from prems P_set_def have "... \ (q - 1) div 2" + also from QRTEMP_axioms j_fact P_set_def have "... \ (q - 1) div 2" apply simp apply (insert aux2) apply (simp add: QRTEMP_def) done - finally show "x \ (q - 1) div 2" using prems by auto + finally show "x \ (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 \ P_set & y \ (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 \ (p * j) div q})" @@ -480,15 +481,15 @@ apply (auto simp add: P_set_def) proof - fix x - assume "0 < x" and "x \ p * j div q" + assume x: "0 < x" "x \ p * j div q" with j_fact Q_set_def have "j \ (q - 1) div 2" by auto with p_g_2 have "p * j \ p * ((q - 1) div 2)" by (auto simp add: mult_le_cancel_left) with q_g_2 have "p * j div q \ p * ((q - 1) div 2) div q" by (auto simp add: zdiv_mono1) - also from prems have "... \ (p - 1) div 2" + also from QRTEMP_axioms j_fact have "... \ (p - 1) div 2" by (auto simp add: aux2 QRTEMP_def) - finally show "x \ (p - 1) div 2" using prems by auto + finally show "x \ (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) diff -r 414a68d72279 -r 1fa4725c4656 src/HOL/Old_Number_Theory/Residues.thy --- 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 \ 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 \ 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 diff -r 414a68d72279 -r 1fa4725c4656 src/HOL/ex/Dedekind_Real.thy --- 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 \ preal" - and B: "B \ preal" - shows "\q. 0 < q & q \ mult_set A B" + assumes A: "A \ preal" + and B: "B \ preal" + shows "\q. 0 < q & q \ mult_set A B" proof - - from preal_exists_bound [OF A] - obtain x where [simp]: "0 < x" "x \ A" by blast - from preal_exists_bound [OF B] - obtain y where [simp]: "0 < y" "y \ B" by blast + from preal_exists_bound [OF A] obtain x where 1 [simp]: "0 < x" "x \ A" by blast + from preal_exists_bound [OF B] obtain y where 2 [simp]: "0 < y" "y \ B" by blast show ?thesis proof (intro exI conjI) show "0 < x*y" by (simp add: mult_pos_pos) show "x * y \ mult_set A B" proof - - { fix u::rat and v::rat - assume "u \ A" and "v \ B" and "x*y = u*v" - moreover - with prems have "uv" - 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 \ A" and v: "v \ B" and xy: "x*y = u*v" + moreover from A B 1 2 u v have "uv" + by (blast intro: preal_imp_pos [OF B] order_less_imp_le) + moreover + from A B 1 `u < x` `v < y` `0 \ 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 A" have vpos: "0 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 \ A" "b + of_nat k * u \ A" .. - hence "b + of_int (int k)*u + u \ A" by (simp add: prems) - thus ?case by (force simp add: algebra_simps prems) + then obtain b where b: "b \ A" "b + of_nat k * u \ A" .. + hence "b + of_int (int k)*u + u \ 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" shows "b \ (d::preal)" proof - - have "c+d \ a+d" by (simp add: prems) - hence "a+b \ a+d" by (simp add: prems) + have "c+d \ a+d" by (simp add: le) + hence "a+b \ a+d" by (simp add: eq) thus "b \ d" by simp qed lemma real_le_lemma: assumes l: "u1 + v2 \ 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 \ 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 "... \ (x2+y1) + (u2+v1)" by (simp add: prems) + also have "... \ (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 \ u + y" - and "u + v' \ u' + v" - and "x2 + v2 = u2 + y2" + and "u + v' \ u' + v" + and "x2 + v2 = u2 + y2" shows "x + v' \ u' + (y::preal)" proof - have "(x+v') + (u+v) = (x+v) + (u+v')" by (simp add: add_ac) - also have "... \ (u+y) + (u+v')" by (simp add: prems) - also have "... \ (u+y) + (u'+v)" by (simp add: prems) + also have "... \ (u+y) + (u+v')" by (simp add: assms) + also have "... \ (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 "\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