1.1 --- a/src/HOL/Algebra/Sylow.thy Thu Jan 13 21:50:13 2011 +0100
1.2 +++ b/src/HOL/Algebra/Sylow.thy Thu Jan 13 23:50:16 2011 +0100
1.3 @@ -32,8 +32,7 @@
1.4 assume "y \<in> calM"
1.5 and g: "g \<in> carrier G"
1.6 hence "y = y #> g #> (inv g)" by (simp add: coset_mult_assoc calM_def)
1.7 - thus "\<exists>g'\<in>carrier G. y = y #> g #> g'"
1.8 - by (blast intro: g inv_closed)
1.9 + thus "\<exists>g'\<in>carrier G. y = y #> g #> g'" by (blast intro: g)
1.10 qed
1.11
1.12 lemma (in sylow) RelM_trans: "trans RelM"
1.13 @@ -121,7 +120,7 @@
1.14
1.15 lemma (in sylow) zero_less_o_G: "0 < order(G)"
1.16 apply (unfold order_def)
1.17 -apply (blast intro: one_closed zero_less_card_empty)
1.18 +apply (blast intro: zero_less_card_empty)
1.19 done
1.20
1.21 lemma (in sylow) zero_less_m: "m > 0"
1.22 @@ -169,7 +168,7 @@
1.23
1.24 lemma (in sylow_central) H_m_closed: "[| x\<in>H; y\<in>H|] ==> x \<otimes> y \<in> H"
1.25 apply (unfold H_def)
1.26 -apply (simp add: coset_mult_assoc [symmetric] m_closed)
1.27 +apply (simp add: coset_mult_assoc [symmetric])
1.28 done
1.29
1.30 lemma (in sylow_central) H_not_empty: "H \<noteq> {}"
1.31 @@ -205,16 +204,16 @@
1.32
1.33 lemma (in sylow_central) M1_cardeq_rcosetGM1g:
1.34 "g \<in> carrier G ==> card(M1 #> g) = card(M1)"
1.35 -by (simp (no_asm_simp) add: M1_subset_G card_cosets_equal rcosetsI)
1.36 +by (simp (no_asm_simp) add: card_cosets_equal rcosetsI)
1.37
1.38 lemma (in sylow_central) M1_RelM_rcosetGM1g:
1.39 "g \<in> carrier G ==> (M1, M1 #> g) \<in> RelM"
1.40 -apply (simp (no_asm) add: RelM_def calM_def card_M1 M1_subset_G)
1.41 +apply (simp (no_asm) add: RelM_def calM_def card_M1)
1.42 apply (rule conjI)
1.43 apply (blast intro: rcosetGM1g_subset_G)
1.44 apply (simp (no_asm_simp) add: card_M1 M1_cardeq_rcosetGM1g)
1.45 apply (rule bexI [of _ "inv g"])
1.46 -apply (simp_all add: coset_mult_assoc M1_subset_G)
1.47 +apply (simp_all add: coset_mult_assoc)
1.48 done
1.49
1.50
1.51 @@ -259,7 +258,7 @@
1.52 apply (rule_tac [2] M1_subset_G)
1.53 apply (rule coset_join1 [THEN in_H_imp_eq])
1.54 apply (rule_tac [3] H_is_subgroup)
1.55 -prefer 2 apply (blast intro: m_closed M_elem_map_carrier inv_closed)
1.56 +prefer 2 apply (blast intro: M_elem_map_carrier)
1.57 apply (simp add: coset_mult_inv2 H_def M_elem_map_carrier subset_eq)
1.58 done
1.59
1.60 @@ -286,8 +285,7 @@
1.61 "(\<lambda>C \<in> rcosets H. M1 #> (@g. g \<in> carrier G \<and> H #> g = C)) \<in> rcosets H \<rightarrow> M"
1.62 apply (simp add: RCOSETS_def)
1.63 apply (fast intro: someI2
1.64 - intro!: restrictI M1_in_M
1.65 - EquivElemClass [OF RelM_equiv M_in_quot _ M1_RelM_rcosetGM1g])
1.66 + intro!: M1_in_M EquivElemClass [OF RelM_equiv M_in_quot _ M1_RelM_rcosetGM1g])
1.67 done
1.68
1.69 text{*close to a duplicate of @{text inj_M_GmodH}*}
1.70 @@ -304,9 +302,9 @@
1.71 apply (erule_tac [2] H_elem_map_carrier)+
1.72 apply (rule_tac [2] H_is_subgroup [THEN subgroup.subset])
1.73 apply (rule coset_join2)
1.74 -apply (blast intro: m_closed inv_closed H_elem_map_carrier)
1.75 +apply (blast intro: H_elem_map_carrier)
1.76 apply (rule H_is_subgroup)
1.77 -apply (simp add: H_I coset_mult_inv2 M1_subset_G H_elem_map_carrier)
1.78 +apply (simp add: H_I coset_mult_inv2 H_elem_map_carrier)
1.79 done
1.80
1.81 lemma (in sylow_central) calM_subset_PowG: "calM \<subseteq> Pow(carrier G)"
1.82 @@ -352,7 +350,7 @@
1.83 apply (frule existsM1inM, clarify)
1.84 apply (subgoal_tac "sylow_central G p a m M1 M")
1.85 apply (blast dest: sylow_central.H_is_subgroup sylow_central.card_H_eq)
1.86 -apply (simp add: sylow_central_def sylow_central_axioms_def prems)
1.87 +apply (simp add: sylow_central_def sylow_central_axioms_def sylow_axioms calM_def RelM_def)
1.88 done
1.89
1.90 text{*Needed because the locale's automatic definition refers to
2.1 --- a/src/HOL/Metis_Examples/BigO.thy Thu Jan 13 21:50:13 2011 +0100
2.2 +++ b/src/HOL/Metis_Examples/BigO.thy Thu Jan 13 23:50:16 2011 +0100
2.3 @@ -437,11 +437,11 @@
2.4 lemma bigo_mult5: "ALL x. f x ~= 0 ==>
2.5 O(f * g) <= (f::'a => ('b::linordered_field)) *o O(g)"
2.6 proof -
2.7 - assume "ALL x. f x ~= 0"
2.8 + assume a: "ALL x. f x ~= 0"
2.9 show "O(f * g) <= f *o O(g)"
2.10 proof
2.11 fix h
2.12 - assume "h : O(f * g)"
2.13 + assume h: "h : O(f * g)"
2.14 then have "(%x. 1 / (f x)) * h : (%x. 1 / f x) *o O(f * g)"
2.15 by auto
2.16 also have "... <= O((%x. 1 / f x) * (f * g))"
2.17 @@ -449,7 +449,7 @@
2.18 also have "(%x. 1 / f x) * (f * g) = g"
2.19 apply (simp add: func_times)
2.20 apply (rule ext)
2.21 - apply (simp add: prems nonzero_divide_eq_eq mult_ac)
2.22 + apply (simp add: a h nonzero_divide_eq_eq mult_ac)
2.23 done
2.24 finally have "(%x. (1::'b) / f x) * h : O(g)".
2.25 then have "f * ((%x. (1::'b) / f x) * h) : f *o O(g)"
2.26 @@ -457,7 +457,7 @@
2.27 also have "f * ((%x. (1::'b) / f x) * h) = h"
2.28 apply (simp add: func_times)
2.29 apply (rule ext)
2.30 - apply (simp add: prems nonzero_divide_eq_eq mult_ac)
2.31 + apply (simp add: a h nonzero_divide_eq_eq mult_ac)
2.32 done
2.33 finally show "h : f *o O(g)".
2.34 qed
3.1 --- a/src/HOL/MicroJava/DFA/Err.thy Thu Jan 13 21:50:13 2011 +0100
3.2 +++ b/src/HOL/MicroJava/DFA/Err.thy Thu Jan 13 23:50:16 2011 +0100
3.3 @@ -259,7 +259,7 @@
3.4 \<lbrakk> semilat (A,r,f); x +_f y <=_r z; x:A; y:A; z:A \<rbrakk>
3.5 \<Longrightarrow> x <=_r z \<and> y <=_r z"
3.6 by (rule Semilat.plus_le_conv [OF Semilat.intro, THEN iffD1])
3.7 - from prems show ?thesis
3.8 + from assms show ?thesis
3.9 apply (rule_tac iffI)
3.10 apply clarify
3.11 apply (drule OK_le_err_OK [THEN iffD2])
4.1 --- a/src/HOL/MicroJava/DFA/Kildall.thy Thu Jan 13 21:50:13 2011 +0100
4.2 +++ b/src/HOL/MicroJava/DFA/Kildall.thy Thu Jan 13 23:50:16 2011 +0100
4.3 @@ -172,7 +172,7 @@
4.4 done
4.5 } note this [dest]
4.6
4.7 - from prems show ?thesis by blast
4.8 + from assms show ?thesis by blast
4.9 qed
4.10
4.11
5.1 --- a/src/HOL/MicroJava/DFA/Product.thy Thu Jan 13 21:50:13 2011 +0100
5.2 +++ b/src/HOL/MicroJava/DFA/Product.thy Thu Jan 13 23:50:16 2011 +0100
5.3 @@ -77,7 +77,7 @@
5.4 "\<And>r f z. \<lbrakk> z : err A; semilat (err A, r, f); OK x : err A; OK y : err A;
5.5 OK x +_f OK y <=_r z\<rbrakk> \<Longrightarrow> OK x <=_r z \<and> OK y <=_r z"
5.6 by (rule Semilat.plus_le_conv [OF Semilat.intro, THEN iffD1])
5.7 - from prems show ?thesis
5.8 + from assms show ?thesis
5.9 apply (rule_tac iffI)
5.10 apply clarify
5.11 apply (drule OK_le_err_OK [THEN iffD2])
6.1 --- a/src/HOL/NSA/NSA.thy Thu Jan 13 21:50:13 2011 +0100
6.2 +++ b/src/HOL/NSA/NSA.thy Thu Jan 13 23:50:16 2011 +0100
6.3 @@ -1837,12 +1837,12 @@
6.4 by (auto dest!: st_approx_self elim!: approx_trans3)
6.5
6.6 lemma approx_st_eq:
6.7 - assumes "x \<in> HFinite" and "y \<in> HFinite" and "x @= y"
6.8 + assumes x: "x \<in> HFinite" and y: "y \<in> HFinite" and xy: "x @= y"
6.9 shows "st x = st y"
6.10 proof -
6.11 have "st x @= x" "st y @= y" "st x \<in> Reals" "st y \<in> Reals"
6.12 - by (simp_all add: st_approx_self st_SReal prems)
6.13 - with prems show ?thesis
6.14 + by (simp_all add: st_approx_self st_SReal x y)
6.15 + with xy show ?thesis
6.16 by (fast elim: approx_trans approx_trans2 SReal_approx_iff [THEN iffD1])
6.17 qed
6.18
7.1 --- a/src/HOL/Number_Theory/Binomial.thy Thu Jan 13 21:50:13 2011 +0100
7.2 +++ b/src/HOL/Number_Theory/Binomial.thy Thu Jan 13 23:50:16 2011 +0100
7.3 @@ -1,7 +1,6 @@
7.4 (* Title: Binomial.thy
7.5 Authors: Lawrence C. Paulson, Jeremy Avigad, Tobias Nipkow
7.6
7.7 -
7.8 Defines the "choose" function, and establishes basic properties.
7.9
7.10 The original theory "Binomial" was by Lawrence C. Paulson, based on
7.11 @@ -9,10 +8,8 @@
7.12 which derives the definition of binomial coefficients in terms of the
7.13 factorial function, is due to Jeremy Avigad. The binomial theorem was
7.14 formalized by Tobias Nipkow.
7.15 -
7.16 *)
7.17
7.18 -
7.19 header {* Binomial *}
7.20
7.21 theory Binomial
7.22 @@ -231,11 +228,10 @@
7.23 lemma choose_altdef_int:
7.24 assumes "(0::int) <= k" and "k <= n"
7.25 shows "n choose k = fact n div (fact k * fact (n - k))"
7.26 -
7.27 - apply (subst tsub_eq [symmetric], rule prems)
7.28 + apply (subst tsub_eq [symmetric], rule assms)
7.29 apply (rule choose_altdef_nat [transferred])
7.30 - using prems apply auto
7.31 -done
7.32 + using assms apply auto
7.33 + done
7.34
7.35 lemma choose_dvd_nat: "(k::nat) \<le> n \<Longrightarrow> fact k * fact (n - k) dvd fact n"
7.36 unfolding dvd_def apply (frule choose_altdef_aux_nat)
7.37 @@ -247,11 +243,10 @@
7.38 lemma choose_dvd_int:
7.39 assumes "(0::int) <= k" and "k <= n"
7.40 shows "fact k * fact (n - k) dvd fact n"
7.41 -
7.42 - apply (subst tsub_eq [symmetric], rule prems)
7.43 + apply (subst tsub_eq [symmetric], rule assms)
7.44 apply (rule choose_dvd_nat [transferred])
7.45 - using prems apply auto
7.46 -done
7.47 + using assms apply auto
7.48 + done
7.49
7.50 (* generalizes Tobias Nipkow's proof to any commutative semiring *)
7.51 theorem binomial: "(a+b::'a::{comm_ring_1,power})^n =
7.52 @@ -269,7 +264,7 @@
7.53 by auto
7.54 have "(a+b)^(n+1) =
7.55 (a+b) * (SUM k=0..n. of_nat (n choose k) * a^k * b^(n-k))"
7.56 - using ih by (simp add: power_plus_one)
7.57 + using ih by simp
7.58 also have "... = a*(SUM k=0..n. of_nat (n choose k) * a^k * b^(n-k)) +
7.59 b*(SUM k=0..n. of_nat (n choose k) * a^k * b^(n-k))"
7.60 by (rule distrib)
7.61 @@ -278,8 +273,8 @@
7.62 by (subst (1 2) power_plus_one, simp add: setsum_right_distrib mult_ac)
7.63 also have "... = (SUM k=0..n. of_nat (n choose k) * a^k * b^(n+1-k)) +
7.64 (SUM k=1..n+1. of_nat (n choose (k - 1)) * a^k * b^(n+1-k))"
7.65 - by (simp add:setsum_shift_bounds_cl_Suc_ivl Suc_diff_le
7.66 - power_Suc field_simps One_nat_def del:setsum_cl_ivl_Suc)
7.67 + by (simp add:setsum_shift_bounds_cl_Suc_ivl Suc_diff_le
7.68 + field_simps One_nat_def del:setsum_cl_ivl_Suc)
7.69 also have "... = a^(n+1) + b^(n+1) +
7.70 (SUM k=1..n. of_nat (n choose (k - 1)) * a^k * b^(n+1-k)) +
7.71 (SUM k=1..n. of_nat (n choose k) * a^k * b^(n+1-k))"
7.72 @@ -315,7 +310,7 @@
7.73 hence "{ T. T \<subseteq> insert x F \<and> card T = k + 1} =
7.74 {T. T \<le> F & card T = k + 1} Un
7.75 {T. T \<le> insert x F & x : T & card T = k + 1}"
7.76 - by (auto intro!: subsetI)
7.77 + by auto
7.78 with iassms fin have "card ({T. T \<le> insert x F \<and> card T = k + 1}) =
7.79 card ({T. T \<subseteq> F \<and> card T = k + 1}) +
7.80 card ({T. T \<subseteq> insert x F \<and> x : T \<and> card T = k + 1})"
7.81 @@ -330,7 +325,7 @@
7.82 proof -
7.83 let ?f = "%T. T Un {x}"
7.84 from iassms have "inj_on ?f {T. T <= F & card T = k}"
7.85 - unfolding inj_on_def by (auto intro!: subsetI)
7.86 + unfolding inj_on_def by auto
7.87 hence "card ({T. T <= F & card T = k}) =
7.88 card(?f ` {T. T <= F & card T = k})"
7.89 by (rule card_image [symmetric])
8.1 --- a/src/HOL/Number_Theory/Cong.thy Thu Jan 13 21:50:13 2011 +0100
8.2 +++ b/src/HOL/Number_Theory/Cong.thy Thu Jan 13 23:50:16 2011 +0100
8.3 @@ -1,9 +1,7 @@
8.4 (* Title: HOL/Library/Cong.thy
8.5 - ID:
8.6 Authors: Christophe Tabacznyj, Lawrence C. Paulson, Amine Chaieb,
8.7 Thomas M. Rasmussen, Jeremy Avigad
8.8
8.9 -
8.10 Defines congruence (notation: [x = y] (mod z)) for natural numbers and
8.11 integers.
8.12
8.13 @@ -23,10 +21,8 @@
8.14 extended to the natural numbers by Chaieb. Jeremy Avigad combined
8.15 these, revised and tidied them, made the development uniform for the
8.16 natural numbers and the integers, and added a number of new theorems.
8.17 -
8.18 *)
8.19
8.20 -
8.21 header {* Congruence *}
8.22
8.23 theory Cong
8.24 @@ -54,9 +50,6 @@
8.25 card (insert x A) = (if x \<in> A then (card A) else (card A) + 1)"
8.26 by (auto simp add: insert_absorb)
8.27
8.28 -(* why wasn't card_insert_if a simp rule? *)
8.29 -declare card_insert_disjoint [simp del]
8.30 -
8.31 lemma nat_1' [simp]: "nat 1 = 1"
8.32 by simp
8.33
8.34 @@ -221,8 +214,7 @@
8.35 assumes "(a::nat) >= c" and "b >= d" and "[a = b] (mod m)" and
8.36 "[c = d] (mod m)"
8.37 shows "[a - c = b - d] (mod m)"
8.38 -
8.39 - using prems by (rule cong_diff_aux_int [transferred]);
8.40 + using assms by (rule cong_diff_aux_int [transferred]);
8.41
8.42 lemma cong_mult_nat:
8.43 "[(a::nat) = b] (mod m) \<Longrightarrow> [c = d] (mod m) \<Longrightarrow> [a * c = b * d] (mod m)"
8.44 @@ -242,13 +234,13 @@
8.45
8.46 lemma cong_exp_nat: "[(x::nat) = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)"
8.47 apply (induct k)
8.48 - apply (auto simp add: cong_refl_nat cong_mult_nat)
8.49 -done
8.50 + apply (auto simp add: cong_mult_nat)
8.51 + done
8.52
8.53 lemma cong_exp_int: "[(x::int) = y] (mod n) \<Longrightarrow> [x^k = y^k] (mod n)"
8.54 apply (induct k)
8.55 - apply (auto simp add: cong_refl_int cong_mult_int)
8.56 -done
8.57 + apply (auto simp add: cong_mult_int)
8.58 + done
8.59
8.60 lemma cong_setsum_nat [rule_format]:
8.61 "(ALL x: A. [((f x)::nat) = g x] (mod m)) \<longrightarrow>
8.62 @@ -313,8 +305,7 @@
8.63 lemma cong_eq_diff_cong_0_nat:
8.64 assumes "(a::nat) >= b"
8.65 shows "[a = b] (mod m) = [a - b = 0] (mod m)"
8.66 -
8.67 - using prems by (rule cong_eq_diff_cong_0_aux_int [transferred])
8.68 + using assms by (rule cong_eq_diff_cong_0_aux_int [transferred])
8.69
8.70 lemma cong_diff_cong_0'_nat:
8.71 "[(x::nat) = y] (mod n) \<longleftrightarrow>
8.72 @@ -364,9 +355,8 @@
8.73 lemma cong_mult_rcancel_nat:
8.74 assumes "coprime k (m::nat)"
8.75 shows "[a * k = b * k] (mod m) = [a = b] (mod m)"
8.76 -
8.77 apply (rule cong_mult_rcancel_int [transferred])
8.78 - using prems apply auto
8.79 + using assms apply auto
8.80 done
8.81
8.82 lemma cong_mult_lcancel_nat:
8.83 @@ -383,23 +373,22 @@
8.84 \<Longrightarrow> [a = b] (mod m * n)"
8.85 apply (simp only: cong_altdef_int)
8.86 apply (erule (2) divides_mult_int)
8.87 -done
8.88 + done
8.89
8.90 lemma coprime_cong_mult_nat:
8.91 assumes "[(a::nat) = b] (mod m)" and "[a = b] (mod n)" and "coprime m n"
8.92 shows "[a = b] (mod m * n)"
8.93 -
8.94 apply (rule coprime_cong_mult_int [transferred])
8.95 - using prems apply auto
8.96 -done
8.97 + using assms apply auto
8.98 + done
8.99
8.100 lemma cong_less_imp_eq_nat: "0 \<le> (a::nat) \<Longrightarrow>
8.101 a < m \<Longrightarrow> 0 \<le> b \<Longrightarrow> b < m \<Longrightarrow> [a = b] (mod m) \<Longrightarrow> a = b"
8.102 - by (auto simp add: cong_nat_def mod_pos_pos_trivial)
8.103 + by (auto simp add: cong_nat_def)
8.104
8.105 lemma cong_less_imp_eq_int: "0 \<le> (a::int) \<Longrightarrow>
8.106 a < m \<Longrightarrow> 0 \<le> b \<Longrightarrow> b < m \<Longrightarrow> [a = b] (mod m) \<Longrightarrow> a = b"
8.107 - by (auto simp add: cong_int_def mod_pos_pos_trivial)
8.108 + by (auto simp add: cong_int_def)
8.109
8.110 lemma cong_less_unique_nat:
8.111 "0 < (m::nat) \<Longrightarrow> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))"
8.112 @@ -412,8 +401,8 @@
8.113 "0 < (m::int) \<Longrightarrow> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))"
8.114 apply auto
8.115 apply (rule_tac x = "a mod m" in exI)
8.116 - apply (unfold cong_int_def, auto simp add: mod_pos_pos_trivial)
8.117 -done
8.118 + apply (unfold cong_int_def, auto)
8.119 + done
8.120
8.121 lemma cong_iff_lin_int: "([(a::int) = b] (mod m)) = (\<exists>k. b = a + m * k)"
8.122 apply (auto simp add: cong_altdef_int dvd_def field_simps)
8.123 @@ -450,15 +439,14 @@
8.124 apply (subst mult_commute)
8.125 apply (subst gcd_add_mult_int)
8.126 apply (rule gcd_commute_int)
8.127 -done
8.128 + done
8.129
8.130 lemma cong_gcd_eq_nat:
8.131 assumes "[(a::nat) = b] (mod m)"
8.132 shows "gcd a m = gcd b m"
8.133 -
8.134 apply (rule cong_gcd_eq_int [transferred])
8.135 - using prems apply auto
8.136 -done
8.137 + using assms apply auto
8.138 + done
8.139
8.140 lemma cong_imp_coprime_nat: "[(a::nat) = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow>
8.141 coprime b m"
8.142 @@ -479,11 +467,11 @@
8.143 lemma cong_minus_int [iff]: "[(a::int) = b] (mod -m) = [a = b] (mod m)"
8.144 by (subst (1 2) cong_altdef_int, auto)
8.145
8.146 -lemma cong_zero_nat [iff]: "[(a::nat) = b] (mod 0) = (a = b)"
8.147 - by (auto simp add: cong_nat_def)
8.148 +lemma cong_zero_nat: "[(a::nat) = b] (mod 0) = (a = b)"
8.149 + by auto
8.150
8.151 -lemma cong_zero_int [iff]: "[(a::int) = b] (mod 0) = (a = b)"
8.152 - by (auto simp add: cong_int_def)
8.153 +lemma cong_zero_int: "[(a::int) = b] (mod 0) = (a = b)"
8.154 + by auto
8.155
8.156 (*
8.157 lemma mod_dvd_mod_int:
8.158 @@ -498,8 +486,8 @@
8.159 shows "(a mod b mod m) = (a mod m)"
8.160
8.161 apply (rule mod_dvd_mod_int [transferred])
8.162 - using prems apply auto
8.163 -done
8.164 + using assms apply auto
8.165 + done
8.166 *)
8.167
8.168 lemma cong_add_lcancel_nat:
9.1 --- a/src/HOL/Number_Theory/Fib.thy Thu Jan 13 21:50:13 2011 +0100
9.2 +++ b/src/HOL/Number_Theory/Fib.thy Thu Jan 13 23:50:16 2011 +0100
9.3 @@ -1,14 +1,12 @@
9.4 (* Title: Fib.thy
9.5 Authors: Lawrence C. Paulson, Jeremy Avigad
9.6
9.7 -
9.8 Defines the fibonacci function.
9.9
9.10 The original "Fib" is due to Lawrence C. Paulson, and was adapted by
9.11 Jeremy Avigad.
9.12 *)
9.13
9.14 -
9.15 header {* Fib *}
9.16
9.17 theory Fib
9.18 @@ -284,16 +282,15 @@
9.19 lemma gcd_fib_mod_int:
9.20 assumes "0 < (m::int)" and "0 <= n"
9.21 shows "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)"
9.22 -
9.23 apply (rule gcd_fib_mod_nat [transferred])
9.24 - using prems apply auto
9.25 -done
9.26 + using assms apply auto
9.27 + done
9.28
9.29 lemma fib_gcd_nat: "fib (gcd (m::nat) n) = gcd (fib m) (fib n)"
9.30 -- {* Law 6.111 *}
9.31 apply (induct m n rule: gcd_nat_induct)
9.32 apply (simp_all add: gcd_non_0_nat gcd_commute_nat gcd_fib_mod_nat)
9.33 -done
9.34 + done
9.35
9.36 lemma fib_gcd_int: "m >= 0 \<Longrightarrow> n >= 0 \<Longrightarrow>
9.37 fib (gcd (m::int) n) = gcd (fib m) (fib n)"
9.38 @@ -306,7 +303,7 @@
9.39 "fib ((n::nat) + 1) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"
9.40 apply (induct n)
9.41 apply (auto simp add: atMost_plus_one_nat fib_plus_2_nat field_simps)
9.42 -done
9.43 + done
9.44
9.45 theorem fib_mult_eq_setsum'_nat:
9.46 "fib (Suc n) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"
10.1 --- a/src/HOL/Number_Theory/MiscAlgebra.thy Thu Jan 13 21:50:13 2011 +0100
10.2 +++ b/src/HOL/Number_Theory/MiscAlgebra.thy Thu Jan 13 23:50:16 2011 +0100
10.3 @@ -69,10 +69,10 @@
10.4 lemma (in comm_monoid) units_comm_group: "comm_group(units_of G)"
10.5 apply (rule group.group_comm_groupI)
10.6 apply (rule units_group)
10.7 - apply (insert prems)
10.8 + apply (insert comm_monoid_axioms)
10.9 apply (unfold units_of_def Units_def comm_monoid_def comm_monoid_axioms_def)
10.10 - apply auto;
10.11 -done;
10.12 + apply auto
10.13 + done
10.14
10.15 lemma units_of_carrier: "carrier (units_of G) = Units G"
10.16 by (unfold units_of_def, auto)
10.17 @@ -174,18 +174,18 @@
10.18 lemma (in cring) field_intro2: "\<zero>\<^bsub>R\<^esub> ~= \<one>\<^bsub>R\<^esub> \<Longrightarrow> ALL x : carrier R - {\<zero>\<^bsub>R\<^esub>}.
10.19 x : Units R \<Longrightarrow> field R"
10.20 apply (unfold_locales)
10.21 - apply (insert prems, auto)
10.22 + apply (insert cring_axioms, auto)
10.23 apply (rule trans)
10.24 apply (subgoal_tac "a = (a \<otimes> b) \<otimes> inv b")
10.25 apply assumption
10.26 apply (subst m_assoc)
10.27 - apply (auto simp add: Units_r_inv)
10.28 + apply auto
10.29 apply (unfold Units_def)
10.30 apply auto
10.31 -done
10.32 + done
10.33
10.34 lemma (in monoid) inv_char: "x : carrier G \<Longrightarrow> y : carrier G \<Longrightarrow>
10.35 - x \<otimes> y = \<one> \<Longrightarrow> y \<otimes> x = \<one> \<Longrightarrow> inv x = y"
10.36 + x \<otimes> y = \<one> \<Longrightarrow> y \<otimes> x = \<one> \<Longrightarrow> inv x = y"
10.37 apply (subgoal_tac "x : Units G")
10.38 apply (subgoal_tac "y = inv x \<otimes> \<one>")
10.39 apply simp
10.40 @@ -194,19 +194,19 @@
10.41 apply auto
10.42 apply (unfold Units_def)
10.43 apply auto
10.44 -done
10.45 + done
10.46
10.47 lemma (in comm_monoid) comm_inv_char: "x : carrier G \<Longrightarrow> y : carrier G \<Longrightarrow>
10.48 x \<otimes> y = \<one> \<Longrightarrow> inv x = y"
10.49 apply (rule inv_char)
10.50 apply auto
10.51 apply (subst m_comm, auto)
10.52 -done
10.53 + done
10.54
10.55 lemma (in ring) inv_neg_one [simp]: "inv (\<ominus> \<one>) = \<ominus> \<one>"
10.56 apply (rule inv_char)
10.57 apply (auto simp add: l_minus r_minus)
10.58 -done
10.59 + done
10.60
10.61 lemma (in monoid) inv_eq_imp_eq: "x : Units G \<Longrightarrow> y : Units G \<Longrightarrow>
10.62 inv x = inv y \<Longrightarrow> x = y"
10.63 @@ -281,8 +281,8 @@
10.64 apply (subgoal_tac "\<ominus> y = \<zero> \<oplus> \<ominus> y")
10.65 apply (erule ssubst)back
10.66 apply (erule subst)
10.67 - apply (simp add: ring_simprules)+
10.68 -done
10.69 + apply (simp_all add: ring_simprules)
10.70 + done
10.71
10.72 (* there's a name conflict -- maybe "domain" should be
10.73 "integral_domain" *)
10.74 @@ -336,9 +336,8 @@
10.75 "x : Units G \<Longrightarrow> x (^)\<^bsub>units_of G\<^esub> (n::nat) = x (^)\<^bsub>G\<^esub> n"
10.76 apply (induct n)
10.77 apply (auto simp add: units_group group.is_monoid
10.78 - monoid.nat_pow_0 monoid.nat_pow_Suc units_of_one units_of_mult
10.79 - One_nat_def)
10.80 -done
10.81 + monoid.nat_pow_0 monoid.nat_pow_Suc units_of_one units_of_mult)
10.82 + done
10.83
10.84 lemma (in cring) units_power_order_eq_one: "finite (Units R) \<Longrightarrow> a : Units R
10.85 \<Longrightarrow> a (^) card(Units R) = \<one>"
10.86 @@ -349,6 +348,6 @@
10.87 apply (rule comm_group.power_order_eq_one)
10.88 apply (rule units_comm_group)
10.89 apply (unfold units_of_def, auto)
10.90 -done
10.91 + done
10.92
10.93 end
11.1 --- a/src/HOL/Number_Theory/Residues.thy Thu Jan 13 21:50:13 2011 +0100
11.2 +++ b/src/HOL/Number_Theory/Residues.thy Thu Jan 13 23:50:16 2011 +0100
11.3 @@ -1,18 +1,17 @@
11.4 (* Title: HOL/Library/Residues.thy
11.5 - ID:
11.6 Author: Jeremy Avigad
11.7
11.8 - An algebraic treatment of residue rings, and resulting proofs of
11.9 - Euler's theorem and Wilson's theorem.
11.10 +An algebraic treatment of residue rings, and resulting proofs of
11.11 +Euler's theorem and Wilson's theorem.
11.12 *)
11.13
11.14 header {* Residue rings *}
11.15
11.16 theory Residues
11.17 imports
11.18 - UniqueFactorization
11.19 - Binomial
11.20 - MiscAlgebra
11.21 + UniqueFactorization
11.22 + Binomial
11.23 + MiscAlgebra
11.24 begin
11.25
11.26
11.27 @@ -41,14 +40,13 @@
11.28 apply (insert m_gt_one)
11.29 apply (rule abelian_groupI)
11.30 apply (unfold R_def residue_ring_def)
11.31 - apply (auto simp add: mod_pos_pos_trivial mod_add_right_eq [symmetric]
11.32 - add_ac)
11.33 + apply (auto simp add: mod_add_right_eq [symmetric] add_ac)
11.34 apply (case_tac "x = 0")
11.35 apply force
11.36 apply (subgoal_tac "(x + (m - x)) mod m = 0")
11.37 apply (erule bexI)
11.38 apply auto
11.39 -done
11.40 + done
11.41
11.42 lemma comm_monoid: "comm_monoid R"
11.43 apply (insert m_gt_one)
11.44 @@ -59,7 +57,7 @@
11.45 apply (erule ssubst)
11.46 apply (subst zmod_zmult1_eq [symmetric])+
11.47 apply (simp_all only: mult_ac)
11.48 -done
11.49 + done
11.50
11.51 lemma cring: "cring R"
11.52 apply (rule cringI)
11.53 @@ -70,7 +68,7 @@
11.54 apply (subst mult_commute)
11.55 apply (subst zmod_zmult1_eq [symmetric])
11.56 apply (simp add: field_simps)
11.57 -done
11.58 + done
11.59
11.60 end
11.61
11.62 @@ -78,7 +76,8 @@
11.63 by (rule cring)
11.64
11.65
11.66 -context residues begin
11.67 +context residues
11.68 +begin
11.69
11.70 (* These lemmas translate back and forth between internal and
11.71 external concepts *)
11.72 @@ -96,7 +95,7 @@
11.73 by (unfold R_def residue_ring_def, auto)
11.74
11.75 lemma res_one_eq: "\<one> = 1"
11.76 - by (unfold R_def residue_ring_def units_of_def residue_ring_def, auto)
11.77 + by (unfold R_def residue_ring_def units_of_def, auto)
11.78
11.79 lemma res_units_eq: "Units R = { x. 0 < x & x < m & coprime x m}"
11.80 apply (insert m_gt_one)
11.81 @@ -110,7 +109,7 @@
11.82 apply (subst (asm) coprime_iff_invertible'_int)
11.83 apply (rule m_gt_one)
11.84 apply (auto simp add: cong_int_def mult_commute)
11.85 -done
11.86 + done
11.87
11.88 lemma res_neg_eq: "\<ominus> x = (- x) mod m"
11.89 apply (insert m_gt_one)
11.90 @@ -126,7 +125,7 @@
11.91 apply simp
11.92 apply (subst zmod_eq_dvd_iff)
11.93 apply auto
11.94 -done
11.95 + done
11.96
11.97 lemma finite [iff]: "finite(carrier R)"
11.98 by (subst res_carrier_eq, auto)
11.99 @@ -141,7 +140,7 @@
11.100 lemma mod_in_carrier [iff]: "a mod m : carrier R"
11.101 apply (unfold res_carrier_eq)
11.102 apply (insert m_gt_one, auto)
11.103 -done
11.104 + done
11.105
11.106 lemma add_cong: "(x mod m) \<oplus> (y mod m) = (x + y) mod m"
11.107 by (unfold R_def residue_ring_def, auto, arith)
11.108 @@ -153,25 +152,25 @@
11.109 apply (subst zmod_zmult1_eq [symmetric])
11.110 apply (subst mult_commute)
11.111 apply auto
11.112 -done
11.113 + done
11.114
11.115 lemma zero_cong: "\<zero> = 0"
11.116 apply (unfold R_def residue_ring_def, auto)
11.117 -done
11.118 + done
11.119
11.120 lemma one_cong: "\<one> = 1 mod m"
11.121 apply (insert m_gt_one)
11.122 apply (unfold R_def residue_ring_def, auto)
11.123 -done
11.124 + done
11.125
11.126 (* revise algebra library to use 1? *)
11.127 lemma pow_cong: "(x mod m) (^) n = x^n mod m"
11.128 apply (insert m_gt_one)
11.129 apply (induct n)
11.130 - apply (auto simp add: nat_pow_def one_cong One_nat_def)
11.131 + apply (auto simp add: nat_pow_def one_cong)
11.132 apply (subst mult_commute)
11.133 apply (rule mult_cong)
11.134 -done
11.135 + done
11.136
11.137 lemma neg_cong: "\<ominus> (x mod m) = (- x) mod m"
11.138 apply (rule sym)
11.139 @@ -180,19 +179,19 @@
11.140 apply (subst add_cong)
11.141 apply (subst zero_cong)
11.142 apply auto
11.143 -done
11.144 + done
11.145
11.146 lemma (in residues) prod_cong:
11.147 "finite A \<Longrightarrow> (\<Otimes> i:A. (f i) mod m) = (PROD i:A. f i) mod m"
11.148 apply (induct set: finite)
11.149 apply (auto simp: one_cong mult_cong)
11.150 -done
11.151 + done
11.152
11.153 lemma (in residues) sum_cong:
11.154 "finite A \<Longrightarrow> (\<Oplus> i:A. (f i) mod m) = (SUM i: A. f i) mod m"
11.155 apply (induct set: finite)
11.156 apply (auto simp: zero_cong add_cong)
11.157 -done
11.158 + done
11.159
11.160 lemma mod_in_res_units [simp]: "1 < m \<Longrightarrow> coprime a m \<Longrightarrow>
11.161 a mod m : Units R"
11.162 @@ -203,7 +202,7 @@
11.163 apply auto
11.164 apply (subst (asm) gcd_red_int)
11.165 apply (subst gcd_commute_int, assumption)
11.166 -done
11.167 + done
11.168
11.169 lemma res_eq_to_cong: "((a mod m) = (b mod m)) = [a = b] (mod (m::int))"
11.170 unfolding cong_int_def by auto
11.171 @@ -227,7 +226,7 @@
11.172 apply (subst mod_add_self2 [symmetric])
11.173 apply (subst mod_pos_pos_trivial)
11.174 apply auto
11.175 -done
11.176 + done
11.177
11.178 end
11.179
11.180 @@ -242,7 +241,7 @@
11.181 sublocale residues_prime < residues p
11.182 apply (unfold R_def residues_def)
11.183 using p_prime apply auto
11.184 -done
11.185 + done
11.186
11.187 context residues_prime begin
11.188
11.189 @@ -259,7 +258,7 @@
11.190 apply (rule notI)
11.191 apply (frule zdvd_imp_le)
11.192 apply auto
11.193 -done
11.194 + done
11.195
11.196 lemma res_prime_units_eq: "Units R = {1..p - 1}"
11.197 apply (subst res_units_eq)
11.198 @@ -269,7 +268,7 @@
11.199 apply (rule p_prime)
11.200 apply (rule zdvd_not_zless)
11.201 apply auto
11.202 -done
11.203 + done
11.204
11.205 end
11.206
11.207 @@ -295,11 +294,11 @@
11.208 1 == Suc 0 coming from? *)
11.209 apply (auto simp add: card_eq_0_iff)
11.210 (* Add card_eq_0_iff as a simp rule? delete card_empty_imp? *)
11.211 -done
11.212 + done
11.213
11.214 lemma phi_one [simp]: "phi 1 = 0"
11.215 apply (auto simp add: phi_def card_eq_0_iff)
11.216 -done
11.217 + done
11.218
11.219 lemma (in residues) phi_eq: "phi m = card(Units R)"
11.220 by (simp add: phi_def res_units_eq)
11.221 @@ -342,7 +341,7 @@
11.222 thus ?thesis by auto
11.223 next
11.224 assume "~(m = 0 | m = 1)"
11.225 - with prems show ?thesis
11.226 + with assms show ?thesis
11.227 by (intro residues.euler_theorem1, unfold residues_def, auto)
11.228 qed
11.229
11.230 @@ -350,18 +349,18 @@
11.231 apply (subst phi_eq)
11.232 apply (subst res_prime_units_eq)
11.233 apply auto
11.234 -done
11.235 + done
11.236
11.237 lemma phi_prime: "prime p \<Longrightarrow> phi p = (nat p - 1)"
11.238 apply (rule residues_prime.phi_prime)
11.239 apply (erule residues_prime.intro)
11.240 -done
11.241 + done
11.242
11.243 lemma fermat_theorem:
11.244 assumes "prime p" and "~ (p dvd a)"
11.245 shows "[a^(nat p - 1) = 1] (mod p)"
11.246 proof -
11.247 - from prems have "[a^phi p = 1] (mod p)"
11.248 + from assms have "[a^phi p = 1] (mod p)"
11.249 apply (intro euler_theorem)
11.250 (* auto should get this next part. matching across
11.251 substitutions is needed. *)
11.252 @@ -369,7 +368,7 @@
11.253 apply (subst gcd_commute_int, erule prime_imp_coprime_int, assumption)
11.254 done
11.255 also have "phi p = nat p - 1"
11.256 - by (rule phi_prime, rule prems)
11.257 + by (rule phi_prime, rule assms)
11.258 finally show ?thesis .
11.259 qed
11.260
11.261 @@ -377,7 +376,7 @@
11.262 subsection {* Wilson's theorem *}
11.263
11.264 lemma (in field) inv_pair_lemma: "x : Units R \<Longrightarrow> y : Units R \<Longrightarrow>
11.265 - {x, inv x} ~= {y, inv y} \<Longrightarrow> {x, inv x} Int {y, inv y} = {}"
11.266 + {x, inv x} ~= {y, inv y} \<Longrightarrow> {x, inv x} Int {y, inv y} = {}"
11.267 apply auto
11.268 apply (erule notE)
11.269 apply (erule inv_eq_imp_eq)
11.270 @@ -385,7 +384,7 @@
11.271 apply (erule notE)
11.272 apply (erule inv_eq_imp_eq)
11.273 apply auto
11.274 -done
11.275 + done
11.276
11.277 lemma (in residues_prime) wilson_theorem1:
11.278 assumes a: "p > 2"
11.279 @@ -411,7 +410,7 @@
11.280 apply (insert a, force)
11.281 done
11.282 also have "(\<Otimes>i:(Union ?InversePairs). i) =
11.283 - (\<Otimes> A: ?InversePairs. (\<Otimes> y:A. y))"
11.284 + (\<Otimes>A: ?InversePairs. (\<Otimes>y:A. y))"
11.285 apply (subst finprod_Union_disjoint)
11.286 apply force
11.287 apply force
11.288 @@ -441,7 +440,7 @@
11.289 done
11.290 also have "\<dots> = fact (p - 1) mod p"
11.291 apply (subst fact_altdef_int)
11.292 - apply (insert prems, force)
11.293 + apply (insert assms, force)
11.294 apply (subst res_prime_units_eq, rule refl)
11.295 done
11.296 finally have "fact (p - 1) mod p = \<ominus> \<one>".
12.1 --- a/src/HOL/Number_Theory/UniqueFactorization.thy Thu Jan 13 21:50:13 2011 +0100
12.2 +++ b/src/HOL/Number_Theory/UniqueFactorization.thy Thu Jan 13 23:50:16 2011 +0100
12.3 @@ -1,12 +1,11 @@
12.4 (* Title: UniqueFactorization.thy
12.5 Author: Jeremy Avigad
12.6
12.7 -
12.8 - Unique factorization for the natural numbers and the integers.
12.9 +Unique factorization for the natural numbers and the integers.
12.10
12.11 - Note: there were previous Isabelle formalizations of unique
12.12 - factorization due to Thomas Marthedal Rasmussen, and, building on
12.13 - that, by Jeremy Avigad and David Gray.
12.14 +Note: there were previous Isabelle formalizations of unique
12.15 +factorization due to Thomas Marthedal Rasmussen, and, building on
12.16 +that, by Jeremy Avigad and David Gray.
12.17 *)
12.18
12.19 header {* UniqueFactorization *}
12.20 @@ -135,14 +134,13 @@
12.21 moreover
12.22 {
12.23 assume "n > 1" and "~ prime n"
12.24 - from prems not_prime_eq_prod_nat
12.25 - obtain m k where "n = m * k & 1 < m & m < n & 1 < k & k < n"
12.26 + with not_prime_eq_prod_nat obtain m k where n: "n = m * k & 1 < m & m < n & 1 < k & k < n"
12.27 by blast
12.28 with ih obtain Q R where "(ALL p : set_of Q. prime p) & m = (PROD i:#Q. i)"
12.29 and "(ALL p: set_of R. prime p) & k = (PROD i:#R. i)"
12.30 by blast
12.31 hence "(ALL p: set_of (Q + R). prime p) & n = (PROD i :# Q + R. i)"
12.32 - by (auto simp add: prems msetprod_Un set_of_union)
12.33 + by (auto simp add: n msetprod_Un)
12.34 then have "EX M. (ALL p : set_of M. prime p) & n = (PROD i :# M. i)"..
12.35 }
12.36 ultimately show "EX M. (ALL p : set_of M. prime p) & n = (PROD i::nat:#M. i)"
12.37 @@ -157,13 +155,11 @@
12.38 shows
12.39 "count M a <= count N a"
12.40 proof cases
12.41 - assume "a : set_of M"
12.42 - with prems have a: "prime a"
12.43 - by auto
12.44 - with prems have "a ^ count M a dvd (PROD i :# M. i)"
12.45 + assume M: "a : set_of M"
12.46 + with assms have a: "prime a" by auto
12.47 + with M have "a ^ count M a dvd (PROD i :# M. i)"
12.48 by (auto intro: dvd_setprod simp add: msetprod_def)
12.49 - also have "... dvd (PROD i :# N. i)"
12.50 - by (rule prems)
12.51 + also have "... dvd (PROD i :# N. i)" by (rule assms)
12.52 also have "... = (PROD i : (set_of N). i ^ (count N i))"
12.53 by (simp add: msetprod_def)
12.54 also have "... =
12.55 @@ -186,7 +182,8 @@
12.56 apply (subst gcd_commute_nat)
12.57 apply (rule setprod_coprime_nat)
12.58 apply (rule primes_imp_powers_coprime_nat)
12.59 - apply (insert prems, auto)
12.60 + using assms M
12.61 + apply auto
12.62 done
12.63 ultimately have "a ^ count M a dvd a^(count N a)"
12.64 by (elim coprime_dvd_mult_nat)
12.65 @@ -206,9 +203,9 @@
12.66 proof -
12.67 {
12.68 fix a
12.69 - from prems have "count M a <= count N a"
12.70 + from assms have "count M a <= count N a"
12.71 by (intro multiset_prime_factorization_unique_aux, auto)
12.72 - moreover from prems have "count N a <= count M a"
12.73 + moreover from assms have "count N a <= count M a"
12.74 by (intro multiset_prime_factorization_unique_aux, auto)
12.75 ultimately have "count M a = count N a"
12.76 by auto
12.77 @@ -245,7 +242,6 @@
12.78 (* definitions for the natural numbers *)
12.79
12.80 instantiation nat :: unique_factorization
12.81 -
12.82 begin
12.83
12.84 definition
12.85 @@ -265,7 +261,6 @@
12.86 (* definitions for the integers *)
12.87
12.88 instantiation int :: unique_factorization
12.89 -
12.90 begin
12.91
12.92 definition
12.93 @@ -329,15 +324,14 @@
12.94 apply (case_tac "n = 0")
12.95 apply (simp add: prime_factors_nat_def multiset_prime_factorization_def)
12.96 apply (auto simp add: prime_factors_nat_def multiset_prime_factorization)
12.97 -done
12.98 + done
12.99
12.100 lemma prime_factors_prime_int [intro]:
12.101 assumes "n >= 0" and "p : prime_factors (n::int)"
12.102 shows "prime p"
12.103 -
12.104 apply (rule prime_factors_prime_nat [transferred, of n p])
12.105 - using prems apply auto
12.106 -done
12.107 + using assms apply auto
12.108 + done
12.109
12.110 lemma prime_factors_gt_0_nat [elim]: "p : prime_factors x \<Longrightarrow> p > (0::nat)"
12.111 by (frule prime_factors_prime_nat, auto)
12.112 @@ -361,22 +355,19 @@
12.113 apply (unfold prime_factors_int_def multiplicity_int_def)
12.114 apply (subst prime_factors_altdef_nat)
12.115 apply (auto simp add: image_def)
12.116 -done
12.117 + done
12.118
12.119 lemma prime_factorization_nat: "(n::nat) > 0 \<Longrightarrow>
12.120 n = (PROD p : prime_factors n. p^(multiplicity p n))"
12.121 by (frule multiset_prime_factorization,
12.122 simp add: prime_factors_nat_def multiplicity_nat_def msetprod_def)
12.123
12.124 -thm prime_factorization_nat [transferred]
12.125 -
12.126 lemma prime_factorization_int:
12.127 assumes "(n::int) > 0"
12.128 shows "n = (PROD p : prime_factors n. p^(multiplicity p n))"
12.129 -
12.130 apply (rule prime_factorization_nat [transferred, of n])
12.131 - using prems apply auto
12.132 -done
12.133 + using assms apply auto
12.134 + done
12.135
12.136 lemma neq_zero_eq_gt_zero_nat: "((x::nat) ~= 0) = (x > 0)"
12.137 by auto
12.138 @@ -591,10 +582,9 @@
12.139 shows
12.140 "(prime_factors k) Un (prime_factors l) = prime_factors (k * l) &
12.141 (ALL p >= 0. multiplicity p k + multiplicity p l = multiplicity p (k * l))"
12.142 -
12.143 apply (rule multiplicity_product_aux_nat [transferred, of l k])
12.144 - using prems apply auto
12.145 -done
12.146 + using assms apply auto
12.147 + done
12.148
12.149 lemma prime_factors_product_nat: "(k::nat) > 0 \<Longrightarrow> l > 0 \<Longrightarrow> prime_factors (k * l) =
12.150 prime_factors k Un prime_factors l"
12.151 @@ -805,9 +795,9 @@
12.152
12.153 apply (case_tac "p >= 0")
12.154 apply (rule prime_factors_altdef2_nat [transferred])
12.155 - using prems apply auto
12.156 + using assms apply auto
12.157 apply (auto simp add: prime_ge_0_int prime_factors_ge_0_int)
12.158 -done
12.159 + done
12.160
12.161 lemma multiplicity_eq_nat:
12.162 fixes x and y::nat
12.163 @@ -846,7 +836,7 @@
12.164 min (multiplicity p x) (multiplicity p y)"
12.165 unfolding z_def
12.166 apply (subst multiplicity_prod_prime_powers_nat)
12.167 - apply (auto simp add: multiplicity_not_factor_nat)
12.168 + apply auto
12.169 done
12.170 have "z dvd x"
12.171 by (intro multiplicity_dvd'_nat, auto simp add: aux)
12.172 @@ -878,7 +868,7 @@
12.173 max (multiplicity p x) (multiplicity p y)"
12.174 unfolding z_def
12.175 apply (subst multiplicity_prod_prime_powers_nat)
12.176 - apply (auto simp add: multiplicity_not_factor_nat)
12.177 + apply auto
12.178 done
12.179 have "x dvd z"
12.180 by (intro multiplicity_dvd'_nat, auto simp add: aux)
13.1 --- a/src/HOL/Old_Number_Theory/Euler.thy Thu Jan 13 21:50:13 2011 +0100
13.2 +++ b/src/HOL/Old_Number_Theory/Euler.thy Thu Jan 13 23:50:16 2011 +0100
13.3 @@ -56,29 +56,27 @@
13.4 apply (rule bexI, auto)
13.5 done
13.6
13.7 -lemma MultInvPair_distinct: "[| zprime p; 2 < p; ~([a = 0] (mod p));
13.8 - ~([j = 0] (mod p));
13.9 - ~(QuadRes p a) |] ==>
13.10 - ~([j = a * MultInv p j] (mod p))"
13.11 +lemma MultInvPair_distinct:
13.12 + assumes "zprime p" and "2 < p" and
13.13 + "~([a = 0] (mod p))" and
13.14 + "~([j = 0] (mod p))" and
13.15 + "~(QuadRes p a)"
13.16 + shows "~([j = a * MultInv p j] (mod p))"
13.17 proof
13.18 - assume "zprime p" and "2 < p" and "~([a = 0] (mod p))" and
13.19 - "~([j = 0] (mod p))" and "~(QuadRes p a)"
13.20 assume "[j = a * MultInv p j] (mod p)"
13.21 then have "[j * j = (a * MultInv p j) * j] (mod p)"
13.22 by (auto simp add: zcong_scalar)
13.23 then have a:"[j * j = a * (MultInv p j * j)] (mod p)"
13.24 by (auto simp add: zmult_ac)
13.25 have "[j * j = a] (mod p)"
13.26 - proof -
13.27 - from prems have b: "[MultInv p j * j = 1] (mod p)"
13.28 - by (simp add: MultInv_prop2a)
13.29 - from b a show ?thesis
13.30 - by (auto simp add: zcong_zmult_prop2)
13.31 - qed
13.32 - then have "[j^2 = a] (mod p)"
13.33 - by (metis number_of_is_id power2_eq_square succ_bin_simps)
13.34 - with prems show False
13.35 - by (simp add: QuadRes_def)
13.36 + proof -
13.37 + from assms(1,2,4) have "[MultInv p j * j = 1] (mod p)"
13.38 + by (simp add: MultInv_prop2a)
13.39 + from this and a show ?thesis
13.40 + by (auto simp add: zcong_zmult_prop2)
13.41 + qed
13.42 + then have "[j^2 = a] (mod p)" by (simp add: power2_eq_square)
13.43 + with assms show False by (simp add: QuadRes_def)
13.44 qed
13.45
13.46 lemma MultInvPair_card_two: "[| zprime p; 2 < p; ~([a = 0] (mod p));
13.47 @@ -108,33 +106,31 @@
13.48 done
13.49
13.50 lemma Union_SetS_finite: "2 < p ==> finite (Union (SetS a p))"
13.51 - by (auto simp add: SetS_finite SetS_elems_finite finite_Union)
13.52 + by (auto simp add: SetS_finite SetS_elems_finite)
13.53
13.54 lemma card_setsum_aux: "[| finite S; \<forall>X \<in> S. finite (X::int set);
13.55 \<forall>X \<in> S. card X = n |] ==> setsum card S = setsum (%x. n) S"
13.56 by (induct set: finite) auto
13.57
13.58 -lemma SetS_card: "[| zprime p; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a) |] ==>
13.59 - int(card(SetS a p)) = (p - 1) div 2"
13.60 +lemma SetS_card:
13.61 + assumes "zprime p" and "2 < p" and "~([a = 0] (mod p))" and "~(QuadRes p a)"
13.62 + shows "int(card(SetS a p)) = (p - 1) div 2"
13.63 proof -
13.64 - assume "zprime p" and "2 < p" and "~([a = 0] (mod p))" and "~(QuadRes p a)"
13.65 - then have "(p - 1) = 2 * int(card(SetS a p))"
13.66 + have "(p - 1) = 2 * int(card(SetS a p))"
13.67 proof -
13.68 have "p - 1 = int(card(Union (SetS a p)))"
13.69 - by (auto simp add: prems MultInvPair_prop2 SRStar_card)
13.70 + by (auto simp add: assms MultInvPair_prop2 SRStar_card)
13.71 also have "... = int (setsum card (SetS a p))"
13.72 - by (auto simp add: prems SetS_finite SetS_elems_finite
13.73 - MultInvPair_prop1c [of p a] card_Union_disjoint)
13.74 + by (auto simp add: assms SetS_finite SetS_elems_finite
13.75 + MultInvPair_prop1c [of p a] card_Union_disjoint)
13.76 also have "... = int(setsum (%x.2) (SetS a p))"
13.77 - using prems
13.78 - by (auto simp add: SetS_elems_card SetS_finite SetS_elems_finite
13.79 + using assms by (auto simp add: SetS_elems_card SetS_finite SetS_elems_finite
13.80 card_setsum_aux simp del: setsum_constant)
13.81 also have "... = 2 * int(card( SetS a p))"
13.82 - by (auto simp add: prems SetS_finite setsum_const2)
13.83 + by (auto simp add: assms SetS_finite setsum_const2)
13.84 finally show ?thesis .
13.85 qed
13.86 - from this show ?thesis
13.87 - by auto
13.88 + then show ?thesis by auto
13.89 qed
13.90
13.91 lemma SetS_setprod_prop: "[| zprime p; 2 < p; ~([a = 0] (mod p));
13.92 @@ -177,37 +173,37 @@
13.93 apply (frule d22set_g_1, auto)
13.94 done
13.95
13.96 -lemma Union_SetS_setprod_prop1: "[| zprime p; 2 < p; ~([a = 0] (mod p)); ~(QuadRes p a) |] ==>
13.97 - [\<Prod>(Union (SetS a p)) = a ^ nat ((p - 1) div 2)] (mod p)"
13.98 +lemma Union_SetS_setprod_prop1:
13.99 + assumes "zprime p" and "2 < p" and "~([a = 0] (mod p))" and
13.100 + "~(QuadRes p a)"
13.101 + shows "[\<Prod>(Union (SetS a p)) = a ^ nat ((p - 1) div 2)] (mod p)"
13.102 proof -
13.103 - assume "zprime p" and "2 < p" and "~([a = 0] (mod p))" and "~(QuadRes p a)"
13.104 - then have "[\<Prod>(Union (SetS a p)) =
13.105 - setprod (setprod (%x. x)) (SetS a p)] (mod p)"
13.106 + from assms have "[\<Prod>(Union (SetS a p)) = setprod (setprod (%x. x)) (SetS a p)] (mod p)"
13.107 by (auto simp add: SetS_finite SetS_elems_finite
13.108 - MultInvPair_prop1c setprod_Union_disjoint)
13.109 + MultInvPair_prop1c setprod_Union_disjoint)
13.110 also have "[setprod (setprod (%x. x)) (SetS a p) =
13.111 setprod (%x. a) (SetS a p)] (mod p)"
13.112 by (rule setprod_same_function_zcong)
13.113 - (auto simp add: prems SetS_setprod_prop SetS_finite)
13.114 + (auto simp add: assms SetS_setprod_prop SetS_finite)
13.115 also (zcong_trans) have "[setprod (%x. a) (SetS a p) =
13.116 a^(card (SetS a p))] (mod p)"
13.117 - by (auto simp add: prems SetS_finite setprod_constant)
13.118 + by (auto simp add: assms SetS_finite setprod_constant)
13.119 finally (zcong_trans) show ?thesis
13.120 apply (rule zcong_trans)
13.121 apply (subgoal_tac "card(SetS a p) = nat((p - 1) div 2)", auto)
13.122 apply (subgoal_tac "nat(int(card(SetS a p))) = nat((p - 1) div 2)", force)
13.123 - apply (auto simp add: prems SetS_card)
13.124 + apply (auto simp add: assms SetS_card)
13.125 done
13.126 qed
13.127
13.128 -lemma Union_SetS_setprod_prop2: "[| zprime p; 2 < p; ~([a = 0](mod p)) |] ==>
13.129 - \<Prod>(Union (SetS a p)) = zfact (p - 1)"
13.130 +lemma Union_SetS_setprod_prop2:
13.131 + assumes "zprime p" and "2 < p" and "~([a = 0](mod p))"
13.132 + shows "\<Prod>(Union (SetS a p)) = zfact (p - 1)"
13.133 proof -
13.134 - assume "zprime p" and "2 < p" and "~([a = 0](mod p))"
13.135 - then have "\<Prod>(Union (SetS a p)) = \<Prod>(SRStar p)"
13.136 + from assms have "\<Prod>(Union (SetS a p)) = \<Prod>(SRStar p)"
13.137 by (auto simp add: MultInvPair_prop2)
13.138 also have "... = \<Prod>({1} \<union> (d22set (p - 1)))"
13.139 - by (auto simp add: prems SRStar_d22set_prop)
13.140 + by (auto simp add: assms SRStar_d22set_prop)
13.141 also have "... = zfact(p - 1)"
13.142 proof -
13.143 have "~(1 \<in> d22set (p - 1)) & finite( d22set (p - 1))"
14.1 --- a/src/HOL/Old_Number_Theory/Gauss.thy Thu Jan 13 21:50:13 2011 +0100
14.2 +++ b/src/HOL/Old_Number_Theory/Gauss.thy Thu Jan 13 23:50:16 2011 +0100
14.3 @@ -79,10 +79,10 @@
14.4 by (auto simp add: C_def finite_B)
14.5
14.6 lemma finite_D: "finite (D)"
14.7 -by (auto simp add: D_def finite_Int finite_C)
14.8 +by (auto simp add: D_def finite_C)
14.9
14.10 lemma finite_E: "finite (E)"
14.11 -by (auto simp add: E_def finite_Int finite_C)
14.12 +by (auto simp add: E_def finite_C)
14.13
14.14 lemma finite_F: "finite (F)"
14.15 by (auto simp add: F_def finite_E)
14.16 @@ -125,11 +125,11 @@
14.17 with zcong_less_eq [of x y p] p_minus_one_l
14.18 order_le_less_trans [of x "(p - 1) div 2" p]
14.19 order_le_less_trans [of y "(p - 1) div 2" p] show "x = y"
14.20 - by (simp add: prems p_minus_one_l p_g_0)
14.21 + by (simp add: b c d e p_minus_one_l p_g_0)
14.22 qed
14.23
14.24 lemma SR_B_inj: "inj_on (StandardRes p) B"
14.25 - apply (auto simp add: B_def StandardRes_def inj_on_def A_def prems)
14.26 + apply (auto simp add: B_def StandardRes_def inj_on_def A_def)
14.27 proof -
14.28 fix x fix y
14.29 assume a: "x * a mod p = y * a mod p"
14.30 @@ -146,7 +146,7 @@
14.31 with zcong_less_eq [of x y p] p_minus_one_l
14.32 order_le_less_trans [of x "(p - 1) div 2" p]
14.33 order_le_less_trans [of y "(p - 1) div 2" p] have "x = y"
14.34 - by (simp add: prems p_minus_one_l p_g_0)
14.35 + by (simp add: b c d e p_minus_one_l p_g_0)
14.36 then have False
14.37 by (simp add: f)
14.38 then show "a = 0"
15.1 --- a/src/HOL/Old_Number_Theory/Int2.thy Thu Jan 13 21:50:13 2011 +0100
15.2 +++ b/src/HOL/Old_Number_Theory/Int2.thy Thu Jan 13 23:50:16 2011 +0100
15.3 @@ -43,38 +43,39 @@
15.4 apply (force simp del:dvd_mult)
15.5 done
15.6
15.7 -lemma div_prop1: "[| 0 < z; (x::int) < y * z |] ==> x div z < y"
15.8 +lemma div_prop1:
15.9 + assumes "0 < z" and "(x::int) < y * z"
15.10 + shows "x div z < y"
15.11 proof -
15.12 - assume "0 < z" then have modth: "x mod z \<ge> 0" by simp
15.13 + from `0 < z` have modth: "x mod z \<ge> 0" by simp
15.14 have "(x div z) * z \<le> (x div z) * z" by simp
15.15 then have "(x div z) * z \<le> (x div z) * z + x mod z" using modth by arith
15.16 also have "\<dots> = x"
15.17 by (auto simp add: zmod_zdiv_equality [symmetric] zmult_ac)
15.18 - also assume "x < y * z"
15.19 + also note `x < y * z`
15.20 finally show ?thesis
15.21 - by (auto simp add: prems mult_less_cancel_right, insert prems, arith)
15.22 + apply (auto simp add: mult_less_cancel_right)
15.23 + using assms apply arith
15.24 + done
15.25 qed
15.26
15.27 -lemma div_prop2: "[| 0 < z; (x::int) < (y * z) + z |] ==> x div z \<le> y"
15.28 +lemma div_prop2:
15.29 + assumes "0 < z" and "(x::int) < (y * z) + z"
15.30 + shows "x div z \<le> y"
15.31 proof -
15.32 - assume "0 < z" and "x < (y * z) + z"
15.33 - then have "x < (y + 1) * z" by (auto simp add: int_distrib)
15.34 + from assms have "x < (y + 1) * z" by (auto simp add: int_distrib)
15.35 then have "x div z < y + 1"
15.36 - apply -
15.37 apply (rule_tac y = "y + 1" in div_prop1)
15.38 - apply (auto simp add: prems)
15.39 + apply (auto simp add: `0 < z`)
15.40 done
15.41 then show ?thesis by auto
15.42 qed
15.43
15.44 -lemma zdiv_leq_prop: "[| 0 < y |] ==> y * (x div y) \<le> (x::int)"
15.45 +lemma zdiv_leq_prop: assumes "0 < y" shows "y * (x div y) \<le> (x::int)"
15.46 proof-
15.47 - assume "0 < y"
15.48 from zmod_zdiv_equality have "x = y * (x div y) + x mod y" by auto
15.49 - moreover have "0 \<le> x mod y"
15.50 - by (auto simp add: prems pos_mod_sign)
15.51 - ultimately show ?thesis
15.52 - by arith
15.53 + moreover have "0 \<le> x mod y" by (auto simp add: assms)
15.54 + ultimately show ?thesis by arith
15.55 qed
15.56
15.57
15.58 @@ -87,7 +88,7 @@
15.59 by (auto simp add: zcong_def)
15.60
15.61 lemma zcong_shift: "[a = b] (mod m) ==> [a + c = b + c] (mod m)"
15.62 - by (auto simp add: zcong_refl zcong_zadd)
15.63 + by (auto simp add: zcong_zadd)
15.64
15.65 lemma zcong_zpower: "[x = y](mod m) ==> [x^z = y^z](mod m)"
15.66 by (induct z) (auto simp add: zcong_zmult)
15.67 @@ -126,11 +127,12 @@
15.68 x < m; y < m |] ==> x = y"
15.69 by (metis zcong_not zcong_sym zless_linear)
15.70
15.71 -lemma zcong_neg_1_impl_ne_1: "[| 2 < p; [x = -1] (mod p) |] ==>
15.72 - ~([x = 1] (mod p))"
15.73 +lemma zcong_neg_1_impl_ne_1:
15.74 + assumes "2 < p" and "[x = -1] (mod p)"
15.75 + shows "~([x = 1] (mod p))"
15.76 proof
15.77 - assume "2 < p" and "[x = 1] (mod p)" and "[x = -1] (mod p)"
15.78 - then have "[1 = -1] (mod p)"
15.79 + assume "[x = 1] (mod p)"
15.80 + with assms have "[1 = -1] (mod p)"
15.81 apply (auto simp add: zcong_sym)
15.82 apply (drule zcong_trans, auto)
15.83 done
15.84 @@ -140,7 +142,7 @@
15.85 by auto
15.86 then have "p dvd 2"
15.87 by (auto simp add: dvd_def zcong_def)
15.88 - with prems show False
15.89 + with `2 < p` show False
15.90 by (auto simp add: zdvd_not_zless)
15.91 qed
15.92
15.93 @@ -181,15 +183,15 @@
15.94 lemma MultInv_prop2: "[| 2 < p; zprime p; ~([x = 0](mod p)) |] ==>
15.95 [(x * (MultInv p x)) = 1] (mod p)"
15.96 proof (simp add: MultInv_def zcong_eq_zdvd_prop)
15.97 - assume "2 < p" and "zprime p" and "~ p dvd x"
15.98 + assume 1: "2 < p" and 2: "zprime p" and 3: "~ p dvd x"
15.99 have "x * x ^ nat (p - 2) = x ^ (nat (p - 2) + 1)"
15.100 by auto
15.101 - also from prems have "nat (p - 2) + 1 = nat (p - 2 + 1)"
15.102 + also from 1 have "nat (p - 2) + 1 = nat (p - 2 + 1)"
15.103 by (simp only: nat_add_distrib)
15.104 also have "p - 2 + 1 = p - 1" by arith
15.105 finally have "[x * x ^ nat (p - 2) = x ^ nat (p - 1)] (mod p)"
15.106 by (rule ssubst, auto)
15.107 - also from prems have "[x ^ nat (p - 1) = 1] (mod p)"
15.108 + also from 2 3 have "[x ^ nat (p - 1) = 1] (mod p)"
15.109 by (auto simp add: Little_Fermat)
15.110 finally (zcong_trans) show "[x * x ^ nat (p - 2) = 1] (mod p)" .
15.111 qed
16.1 --- a/src/HOL/Old_Number_Theory/IntPrimes.thy Thu Jan 13 21:50:13 2011 +0100
16.2 +++ b/src/HOL/Old_Number_Theory/IntPrimes.thy Thu Jan 13 23:50:16 2011 +0100
16.3 @@ -277,7 +277,7 @@
16.4 by (auto simp add: zcong_def)
16.5
16.6 lemma "[a = b] (mod m) = (a mod m = b mod m)"
16.7 - apply (case_tac "m = 0", simp add: DIVISION_BY_ZERO)
16.8 + apply (cases "m = 0", simp)
16.9 apply (simp add: linorder_neq_iff)
16.10 apply (erule disjE)
16.11 prefer 2 apply (simp add: zcong_zmod_eq)
17.1 --- a/src/HOL/Old_Number_Theory/Legacy_GCD.thy Thu Jan 13 21:50:13 2011 +0100
17.2 +++ b/src/HOL/Old_Number_Theory/Legacy_GCD.thy Thu Jan 13 23:50:16 2011 +0100
17.3 @@ -276,7 +276,7 @@
17.4 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)"
17.5 using ex
17.6 apply clarsimp
17.7 -apply (rule_tac x="d" in exI, simp add: dvd_add)
17.8 +apply (rule_tac x="d" in exI, simp)
17.9 apply (case_tac "a * x = b * y + d" , simp_all)
17.10 apply (rule_tac x="x + y" in exI)
17.11 apply (rule_tac x="y" in exI)
17.12 @@ -290,10 +290,10 @@
17.13 apply(induct a b rule: ind_euclid)
17.14 apply blast
17.15 apply clarify
17.16 -apply (rule_tac x="a" in exI, simp add: dvd_add)
17.17 +apply (rule_tac x="a" in exI, simp)
17.18 apply clarsimp
17.19 apply (rule_tac x="d" in exI)
17.20 -apply (case_tac "a * x = b * y + d", simp_all add: dvd_add)
17.21 +apply (case_tac "a * x = b * y + d", simp_all)
17.22 apply (rule_tac x="x+y" in exI)
17.23 apply (rule_tac x="y" in exI)
17.24 apply algebra
17.25 @@ -332,13 +332,13 @@
17.26 from divides_le[OF H(2)] b have "d < b \<or> d = b" using le_less by blast
17.27 moreover
17.28 {assume db: "d=b"
17.29 - from prems have ?thesis apply simp
17.30 + from nz H db have ?thesis apply simp
17.31 apply (rule exI[where x = b], simp)
17.32 apply (rule exI[where x = b])
17.33 by (rule exI[where x = "a - 1"], simp add: diff_mult_distrib2)}
17.34 moreover
17.35 {assume db: "d < b"
17.36 - {assume "x=0" hence ?thesis using prems by simp }
17.37 + {assume "x=0" hence ?thesis using nz H by simp }
17.38 moreover
17.39 {assume x0: "x \<noteq> 0" hence xp: "x > 0" by simp
17.40
17.41 @@ -426,12 +426,11 @@
17.42 qed
17.43
17.44 lemma gcd_mult': "gcd b (a * b) = b"
17.45 -by (simp add: gcd_mult mult_commute[of a b])
17.46 +by (simp add: mult_commute[of a b])
17.47
17.48 lemma gcd_add: "gcd(a + b) b = gcd a b"
17.49 "gcd(b + a) b = gcd a b" "gcd a (a + b) = gcd a b" "gcd a (b + a) = gcd a b"
17.50 -apply (simp_all add: gcd_add1)
17.51 -by (simp add: gcd_commute gcd_add1)
17.52 +by (simp_all add: gcd_commute)
17.53
17.54 lemma gcd_sub: "b <= a ==> gcd(a - b) b = gcd a b" "a <= b ==> gcd a (b - a) = gcd a b"
17.55 proof-
17.56 @@ -568,10 +567,10 @@
17.57 zgcd :: "int \<Rightarrow> int \<Rightarrow> int" where
17.58 "zgcd i j = int (gcd (nat (abs i)) (nat (abs j)))"
17.59
17.60 -lemma zgcd_zdvd1 [iff,simp, algebra]: "zgcd i j dvd i"
17.61 +lemma zgcd_zdvd1 [iff, algebra]: "zgcd i j dvd i"
17.62 by (simp add: zgcd_def int_dvd_iff)
17.63
17.64 -lemma zgcd_zdvd2 [iff,simp, algebra]: "zgcd i j dvd j"
17.65 +lemma zgcd_zdvd2 [iff, algebra]: "zgcd i j dvd j"
17.66 by (simp add: zgcd_def int_dvd_iff)
17.67
17.68 lemma zgcd_pos: "zgcd i j \<ge> 0"
17.69 @@ -637,8 +636,8 @@
17.70 let ?a' = "a div ?g"
17.71 let ?b' = "b div ?g"
17.72 let ?g' = "zgcd ?a' ?b'"
17.73 - have dvdg: "?g dvd a" "?g dvd b" by (simp_all add: zgcd_zdvd1 zgcd_zdvd2)
17.74 - have dvdg': "?g' dvd ?a'" "?g' dvd ?b'" by (simp_all add: zgcd_zdvd1 zgcd_zdvd2)
17.75 + have dvdg: "?g dvd a" "?g dvd b" by simp_all
17.76 + have dvdg': "?g' dvd ?a'" "?g' dvd ?b'" by simp_all
17.77 from dvdg dvdg' obtain ka kb ka' kb' where
17.78 kab: "a = ?g*ka" "b = ?g*kb" "?a' = ?g'*ka'" "?b' = ?g' * kb'"
17.79 unfolding dvd_def by blast
17.80 @@ -668,7 +667,7 @@
17.81 done
17.82
17.83 lemma zgcd_eq: "zgcd m n = zgcd n (m mod n)"
17.84 - apply (case_tac "n = 0", simp add: DIVISION_BY_ZERO)
17.85 + apply (cases "n = 0", simp)
17.86 apply (auto simp add: linorder_neq_iff zgcd_non_0)
17.87 apply (cut_tac m = "-m" and n = "-n" in zgcd_non_0, auto)
17.88 done
17.89 @@ -683,7 +682,7 @@
17.90 by (simp add: zgcd_def abs_if int_dvd_iff dvd_int_iff nat_dvd_iff)
17.91
17.92 lemma zgcd_1_left [simp, algebra]: "zgcd 1 m = 1"
17.93 - by (simp add: zgcd_def gcd_1_left)
17.94 + by (simp add: zgcd_def)
17.95
17.96 lemma zgcd_assoc: "zgcd (zgcd k m) n = zgcd k (zgcd m n)"
17.97 by (simp add: zgcd_def gcd_assoc)
18.1 --- a/src/HOL/Old_Number_Theory/Pocklington.thy Thu Jan 13 21:50:13 2011 +0100
18.2 +++ b/src/HOL/Old_Number_Theory/Pocklington.thy Thu Jan 13 23:50:16 2011 +0100
18.3 @@ -260,7 +260,9 @@
18.4 apply (cases "n=0", simp_all add: cong_commute)
18.5 apply (cases "n=1", simp_all add: cong_commute modeq_def)
18.6 apply arith
18.7 - by (cases "a=1", simp_all add: modeq_def cong_commute)}
18.8 + apply (cases "a=1")
18.9 + apply (simp_all add: modeq_def cong_commute)
18.10 + done }
18.11 moreover
18.12 {assume n: "n\<noteq>0" "n\<noteq>1" and a:"a\<noteq>0" "a \<noteq> 1" hence a': "a \<ge> 1" by simp
18.13 hence ?thesis using cong_le[OF a', of n] by auto }
18.14 @@ -630,7 +632,7 @@
18.15 with an have "coprime (a*x) n"
18.16 by (simp add: coprime_mul_eq[of n a x] coprime_commute)
18.17 hence "?h (a*x) \<in> ?S" using nz
18.18 - by (simp add: coprime_mod[OF nz] mod_less_divisor)}
18.19 + by (simp add: coprime_mod[OF nz])}
18.20 thus " \<forall>x\<in>{m. coprime m n \<and> m < n}.
18.21 ((\<lambda>m. m mod n) \<circ> op * a) x \<in> {m. coprime m n \<and> m < n} \<and>
18.22 ((\<lambda>m. m mod n) \<circ> op * a) x = ((\<lambda>m. m mod n) \<circ> op * a) x" by simp
18.23 @@ -821,7 +823,7 @@
18.24 lemma ord_minimal: "0 < m \<Longrightarrow> m < ord n a \<Longrightarrow> ~[a^m = 1] (mod n)"
18.25 using ord_works by blast
18.26 lemma ord_eq_0: "ord n a = 0 \<longleftrightarrow> ~coprime n a"
18.27 -by (cases "coprime n a", simp add: neq0_conv coprime_ord, simp add: neq0_conv ord_def)
18.28 +by (cases "coprime n a", simp add: coprime_ord, simp add: ord_def)
18.29
18.30 lemma ord_divides:
18.31 "[a ^ d = 1] (mod n) \<longleftrightarrow> ord n a dvd d" (is "?lhs \<longleftrightarrow> ?rhs")
18.32 @@ -952,8 +954,7 @@
18.33 {fix d assume d: "d dvd n" "d^2 \<le> n" and H: "\<forall>m. m dvd n \<longrightarrow> m=1 \<or> m=n"
18.34 from H d have d1n: "d = 1 \<or> d=n" by blast
18.35 {assume dn: "d=n"
18.36 - have "n^2 > n*1" using n
18.37 - by (simp add: power2_eq_square mult_less_cancel1)
18.38 + have "n^2 > n*1" using n by (simp add: power2_eq_square)
18.39 with dn d(2) have "d=1" by simp}
18.40 with d1n have "d = 1" by blast }
18.41 moreover
18.42 @@ -985,7 +986,11 @@
18.43 {assume n: "n\<noteq>0" "n\<noteq>1"
18.44 {assume H: ?lhs
18.45 from H[unfolded prime_divisor_sqrt] n
18.46 - have ?rhs apply clarsimp by (erule_tac x="p" in allE, simp add: prime_1)
18.47 + have ?rhs
18.48 + apply clarsimp
18.49 + apply (erule_tac x="p" in allE)
18.50 + apply simp
18.51 + done
18.52 }
18.53 moreover
18.54 {assume H: ?rhs
18.55 @@ -1018,7 +1023,7 @@
18.56 hence "a^ (n - 1) = 0" using n by (simp add: power_0_left)
18.57 with n an mod_less[of 1 n] have False by (simp add: power_0_left modeq_def)}
18.58 hence a0: "a\<noteq>0" ..
18.59 - from n nqr have aqr0: "a ^ (q * r) \<noteq> 0" using a0 by (simp add: neq0_conv)
18.60 + from n nqr have aqr0: "a ^ (q * r) \<noteq> 0" using a0 by simp
18.61 hence "(a ^ (q * r) - 1) + 1 = a ^ (q * r)" by simp
18.62 with k l have "a ^ (q * r) = p*l*k + 1" by simp
18.63 hence "a ^ (r * q) + p * 0 = 1 + p * (l*k)" by (simp add: mult_ac)
18.64 @@ -1055,7 +1060,7 @@
18.65 from n have n0: "n \<noteq> 0" by simp
18.66 from d(2) an n12[symmetric] have a0: "a \<noteq> 0"
18.67 by - (rule ccontr, simp add: modeq_def)
18.68 - have th1: "a^ (n - 1) \<noteq> 0" using n d(2) dp a0 by (auto simp add: neq0_conv)
18.69 + have th1: "a^ (n - 1) \<noteq> 0" using n d(2) dp a0 by auto
18.70 from coprime_minus1[OF th1, unfolded coprime]
18.71 dvd_trans[OF pn cong_1_divides[OF an]] th0 d(3) dp
18.72 have False by auto}
19.1 --- a/src/HOL/Old_Number_Theory/Primes.thy Thu Jan 13 21:50:13 2011 +0100
19.2 +++ b/src/HOL/Old_Number_Theory/Primes.thy Thu Jan 13 23:50:16 2011 +0100
19.3 @@ -222,7 +222,7 @@
19.4 thus ?thesis unfolding coprime_def .
19.5 qed
19.6 lemma coprime_lmul2: assumes dab: "coprime d (a * b)" shows "coprime d b"
19.7 -using prems unfolding coprime_bezout
19.8 +using dab unfolding coprime_bezout
19.9 apply clarsimp
19.10 apply (case_tac "d * x - a * b * y = Suc 0 ", simp_all)
19.11 apply (rule_tac x="x" in exI)
19.12 @@ -283,7 +283,8 @@
19.13 apply (simp only: z power_0_Suc)
19.14 apply (rule exI[where x=0])
19.15 apply (rule exI[where x=0])
19.16 - by simp}
19.17 + apply simp
19.18 + done }
19.19 moreover
19.20 {assume z: "?g \<noteq> 0"
19.21 from gcd_dvd1[of a b] gcd_dvd2[of a b] obtain a' b' where
19.22 @@ -350,7 +351,7 @@
19.23 {assume "?g = 0" with ab n have ?thesis by (simp add: gcd_zero)}
19.24 moreover
19.25 {assume z: "?g \<noteq> 0"
19.26 - hence zn: "?g ^ n \<noteq> 0" using n by (simp add: neq0_conv)
19.27 + hence zn: "?g ^ n \<noteq> 0" using n by simp
19.28 from gcd_coprime_exists[OF z]
19.29 obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'" by blast
19.30 from ab have "(a' * ?g) ^ n dvd (b' * ?g)^n" by (simp add: ab'(1,2)[symmetric])
19.31 @@ -637,8 +638,9 @@
19.32 assume ?rhs then show ?lhs by auto
19.33 qed
19.34
19.35 -lemma power_Suc0[simp]: "Suc 0 ^ n = Suc 0"
19.36 +lemma power_Suc0: "Suc 0 ^ n = Suc 0"
19.37 unfolding One_nat_def[symmetric] power_one ..
19.38 +
19.39 lemma coprime_pow: assumes ab: "coprime a b" and abcn: "a * b = c ^n"
19.40 shows "\<exists>r s. a = r^n \<and> b = s ^n"
19.41 using ab abcn
19.42 @@ -678,7 +680,7 @@
19.43 from prime_divprod_pow[OF p(1) H(2), unfolded H(3), OF divides_exp[OF p(2), of n]]
19.44 have pnab: "p ^ n dvd a \<or> p^n dvd b" .
19.45 from p(2) obtain l where l: "c = p*l" unfolding dvd_def by blast
19.46 - have pn0: "p^n \<noteq> 0" using n prime_ge_2 [OF p(1)] by (simp add: neq0_conv)
19.47 + have pn0: "p^n \<noteq> 0" using n prime_ge_2 [OF p(1)] by simp
19.48 {assume pa: "p^n dvd a"
19.49 then obtain k where k: "a = p^n * k" unfolding dvd_def by blast
19.50 from l have "l dvd c" by auto
19.51 @@ -785,8 +787,7 @@
19.52 case 0 thus ?case by simp
19.53 next
19.54 case (Suc n k) hence th: "x*x^n = p^k" by simp
19.55 - {assume "n = 0" with prems have ?case apply simp
19.56 - by (rule exI[where x="k"],simp)}
19.57 + {assume "n = 0" with Suc have ?case by simp (rule exI[where x="k"], simp)}
19.58 moreover
19.59 {assume n: "n \<noteq> 0"
19.60 from prime_power_mult[OF p th]
20.1 --- a/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy Thu Jan 13 21:50:13 2011 +0100
20.2 +++ b/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy Thu Jan 13 23:50:16 2011 +0100
20.3 @@ -201,10 +201,11 @@
20.4 then show ?thesis by auto
20.5 qed
20.6
20.7 -lemma pb_neq_qa: "[|1 \<le> b; b \<le> (q - 1) div 2 |] ==>
20.8 - (p * b \<noteq> q * a)"
20.9 +lemma pb_neq_qa:
20.10 + assumes "1 \<le> b" and "b \<le> (q - 1) div 2"
20.11 + shows "p * b \<noteq> q * a"
20.12 proof
20.13 - assume "p * b = q * a" and "1 \<le> b" and "b \<le> (q - 1) div 2"
20.14 + assume "p * b = q * a"
20.15 then have "q dvd (p * b)" by (auto simp add: dvd_def)
20.16 with q_prime p_g_2 have "q dvd p | q dvd b"
20.17 by (auto simp add: zprime_zdvd_zmult)
20.18 @@ -216,7 +217,7 @@
20.19 apply (drule_tac x = q and R = False in allE)
20.20 apply (simp add: QRTEMP_def)
20.21 apply (subgoal_tac "0 \<le> q", simp add: QRTEMP_def)
20.22 - apply (insert prems)
20.23 + apply (insert assms)
20.24 apply (auto simp add: QRTEMP_def)
20.25 done
20.26 with q_g_2 p_neq_q show False by auto
20.27 @@ -225,18 +226,18 @@
20.28 then have "q \<le> b"
20.29 proof -
20.30 assume "q dvd b"
20.31 - moreover from prems have "0 < b" by auto
20.32 + moreover from assms have "0 < b" by auto
20.33 ultimately show ?thesis using zdvd_bounds [of q b] by auto
20.34 qed
20.35 - with prems have "q \<le> (q - 1) div 2" by auto
20.36 + with assms have "q \<le> (q - 1) div 2" by auto
20.37 then have "2 * q \<le> 2 * ((q - 1) div 2)" by arith
20.38 then have "2 * q \<le> q - 1"
20.39 proof -
20.40 - assume "2 * q \<le> 2 * ((q - 1) div 2)"
20.41 - with prems have "q \<in> zOdd" by (auto simp add: QRTEMP_def zprime_zOdd_eq_grt_2)
20.42 + assume a: "2 * q \<le> 2 * ((q - 1) div 2)"
20.43 + with assms have "q \<in> zOdd" by (auto simp add: QRTEMP_def zprime_zOdd_eq_grt_2)
20.44 with odd_minus_one_even have "(q - 1):zEven" by auto
20.45 with even_div_2_prop2 have "(q - 1) = 2 * ((q - 1) div 2)" by auto
20.46 - with prems show ?thesis by auto
20.47 + with a show ?thesis by auto
20.48 qed
20.49 then have p1: "q \<le> -1" by arith
20.50 with q_g_2 show False by auto
20.51 @@ -273,7 +274,7 @@
20.52
20.53 lemma S_card: "((p - 1) div 2) * ((q - 1) div 2) = int (card(S))"
20.54 using P_set_card Q_set_card P_set_finite Q_set_finite
20.55 - by (auto simp add: S_def zmult_int setsum_constant)
20.56 + by (auto simp add: S_def zmult_int)
20.57
20.58 lemma S1_Int_S2_prop: "S1 \<inter> S2 = {}"
20.59 by (auto simp add: S1_def S2_def)
20.60 @@ -301,11 +302,11 @@
20.61 finally show ?thesis .
20.62 qed
20.63
20.64 -lemma aux1a: "[| 0 < a; a \<le> (p - 1) div 2;
20.65 - 0 < b; b \<le> (q - 1) div 2 |] ==>
20.66 - (p * b < q * a) = (b \<le> q * a div p)"
20.67 +lemma aux1a:
20.68 + assumes "0 < a" and "a \<le> (p - 1) div 2"
20.69 + and "0 < b" and "b \<le> (q - 1) div 2"
20.70 + shows "(p * b < q * a) = (b \<le> q * a div p)"
20.71 proof -
20.72 - assume "0 < a" and "a \<le> (p - 1) div 2" and "0 < b" and "b \<le> (q - 1) div 2"
20.73 have "p * b < q * a ==> b \<le> q * a div p"
20.74 proof -
20.75 assume "p * b < q * a"
20.76 @@ -329,17 +330,17 @@
20.77 then have "p * b < q * a | p * b = q * a"
20.78 by (simp only: order_le_imp_less_or_eq)
20.79 moreover have "p * b \<noteq> q * a"
20.80 - by (rule pb_neq_qa) (insert prems, auto)
20.81 + by (rule pb_neq_qa) (insert assms, auto)
20.82 ultimately show ?thesis by auto
20.83 qed
20.84 ultimately show ?thesis ..
20.85 qed
20.86
20.87 -lemma aux1b: "[| 0 < a; a \<le> (p - 1) div 2;
20.88 - 0 < b; b \<le> (q - 1) div 2 |] ==>
20.89 - (q * a < p * b) = (a \<le> p * b div q)"
20.90 +lemma aux1b:
20.91 + assumes "0 < a" and "a \<le> (p - 1) div 2"
20.92 + and "0 < b" and "b \<le> (q - 1) div 2"
20.93 + shows "(q * a < p * b) = (a \<le> p * b div q)"
20.94 proof -
20.95 - assume "0 < a" and "a \<le> (p - 1) div 2" and "0 < b" and "b \<le> (q - 1) div 2"
20.96 have "q * a < p * b ==> a \<le> p * b div q"
20.97 proof -
20.98 assume "q * a < p * b"
20.99 @@ -363,18 +364,18 @@
20.100 then have "q * a < p * b | q * a = p * b"
20.101 by (simp only: order_le_imp_less_or_eq)
20.102 moreover have "p * b \<noteq> q * a"
20.103 - by (rule pb_neq_qa) (insert prems, auto)
20.104 + by (rule pb_neq_qa) (insert assms, auto)
20.105 ultimately show ?thesis by auto
20.106 qed
20.107 ultimately show ?thesis ..
20.108 qed
20.109
20.110 -lemma (in -) aux2: "[| zprime p; zprime q; 2 < p; 2 < q |] ==>
20.111 - (q * ((p - 1) div 2)) div p \<le> (q - 1) div 2"
20.112 +lemma (in -) aux2:
20.113 + assumes "zprime p" and "zprime q" and "2 < p" and "2 < q"
20.114 + shows "(q * ((p - 1) div 2)) div p \<le> (q - 1) div 2"
20.115 proof-
20.116 - assume "zprime p" and "zprime q" and "2 < p" and "2 < q"
20.117 (* Set up what's even and odd *)
20.118 - then have "p \<in> zOdd & q \<in> zOdd"
20.119 + from assms have "p \<in> zOdd & q \<in> zOdd"
20.120 by (auto simp add: zprime_zOdd_eq_grt_2)
20.121 then have even1: "(p - 1):zEven & (q - 1):zEven"
20.122 by (auto simp add: odd_minus_one_even)
20.123 @@ -383,7 +384,7 @@
20.124 then have even3: "(((q - 1) * p) + (2 * p)):zEven"
20.125 by (auto simp: EvenOdd.even_plus_even)
20.126 (* using these prove it *)
20.127 - from prems have "q * (p - 1) < ((q - 1) * p) + (2 * p)"
20.128 + from assms have "q * (p - 1) < ((q - 1) * p) + (2 * p)"
20.129 by (auto simp add: int_distrib)
20.130 then have "((p - 1) * q) div 2 < (((q - 1) * p) + (2 * p)) div 2"
20.131 apply (rule_tac x = "((p - 1) * q)" in even_div_2_l)
20.132 @@ -395,7 +396,7 @@
20.133 finally show ?thesis
20.134 apply (rule_tac x = " q * ((p - 1) div 2)" and
20.135 y = "(q - 1) div 2" in div_prop2)
20.136 - using prems by auto
20.137 + using assms by auto
20.138 qed
20.139
20.140 lemma aux3a: "\<forall>j \<in> P_set. int (card (f1 j)) = (q * j) div p"
20.141 @@ -414,7 +415,7 @@
20.142 ultimately have "card ((%(x,y). y) ` (f1 j)) = card (f1 j)"
20.143 by (auto simp add: f1_def card_image)
20.144 moreover have "((%(x,y). y) ` (f1 j)) = {y. y \<in> Q_set & y \<le> (q * j) div p}"
20.145 - using prems by (auto simp add: f1_def S_def Q_set_def P_set_def image_def)
20.146 + using j_fact by (auto simp add: f1_def S_def Q_set_def P_set_def image_def)
20.147 ultimately show ?thesis by (auto simp add: f1_def)
20.148 qed
20.149 also have "... = int (card {y. 0 < y & y \<le> (q * j) div p})"
20.150 @@ -424,18 +425,18 @@
20.151 apply (auto simp add: Q_set_def)
20.152 proof -
20.153 fix x
20.154 - assume "0 < x" and "x \<le> q * j div p"
20.155 + assume x: "0 < x" "x \<le> q * j div p"
20.156 with j_fact P_set_def have "j \<le> (p - 1) div 2" by auto
20.157 with q_g_2 have "q * j \<le> q * ((p - 1) div 2)"
20.158 by (auto simp add: mult_le_cancel_left)
20.159 with p_g_2 have "q * j div p \<le> q * ((p - 1) div 2) div p"
20.160 by (auto simp add: zdiv_mono1)
20.161 - also from prems P_set_def have "... \<le> (q - 1) div 2"
20.162 + also from QRTEMP_axioms j_fact P_set_def have "... \<le> (q - 1) div 2"
20.163 apply simp
20.164 apply (insert aux2)
20.165 apply (simp add: QRTEMP_def)
20.166 done
20.167 - finally show "x \<le> (q - 1) div 2" using prems by auto
20.168 + finally show "x \<le> (q - 1) div 2" using x by auto
20.169 qed
20.170 then show ?thesis by auto
20.171 qed
20.172 @@ -470,7 +471,7 @@
20.173 ultimately have "card ((%(x,y). x) ` (f2 j)) = card (f2 j)"
20.174 by (auto simp add: f2_def card_image)
20.175 moreover have "((%(x,y). x) ` (f2 j)) = {y. y \<in> P_set & y \<le> (p * j) div q}"
20.176 - using prems by (auto simp add: f2_def S_def Q_set_def P_set_def image_def)
20.177 + using j_fact by (auto simp add: f2_def S_def Q_set_def P_set_def image_def)
20.178 ultimately show ?thesis by (auto simp add: f2_def)
20.179 qed
20.180 also have "... = int (card {y. 0 < y & y \<le> (p * j) div q})"
20.181 @@ -480,15 +481,15 @@
20.182 apply (auto simp add: P_set_def)
20.183 proof -
20.184 fix x
20.185 - assume "0 < x" and "x \<le> p * j div q"
20.186 + assume x: "0 < x" "x \<le> p * j div q"
20.187 with j_fact Q_set_def have "j \<le> (q - 1) div 2" by auto
20.188 with p_g_2 have "p * j \<le> p * ((q - 1) div 2)"
20.189 by (auto simp add: mult_le_cancel_left)
20.190 with q_g_2 have "p * j div q \<le> p * ((q - 1) div 2) div q"
20.191 by (auto simp add: zdiv_mono1)
20.192 - also from prems have "... \<le> (p - 1) div 2"
20.193 + also from QRTEMP_axioms j_fact have "... \<le> (p - 1) div 2"
20.194 by (auto simp add: aux2 QRTEMP_def)
20.195 - finally show "x \<le> (p - 1) div 2" using prems by auto
20.196 + finally show "x \<le> (p - 1) div 2" using x by auto
20.197 qed
20.198 then show ?thesis by auto
20.199 qed
20.200 @@ -587,18 +588,18 @@
20.201 lemma QR_short: "(Legendre p q) * (Legendre q p) =
20.202 (-1::int)^nat(((p - 1) div 2)*((q - 1) div 2))"
20.203 proof -
20.204 - from prems have "~([p = 0] (mod q))"
20.205 + from QRTEMP_axioms have "~([p = 0] (mod q))"
20.206 by (auto simp add: pq_prime_neq QRTEMP_def)
20.207 - with prems Q_set_def have a1: "(Legendre p q) = (-1::int) ^
20.208 + with QRTEMP_axioms Q_set_def have a1: "(Legendre p q) = (-1::int) ^
20.209 nat(setsum (%x. ((x * p) div q)) Q_set)"
20.210 apply (rule_tac p = q in MainQRLemma)
20.211 apply (auto simp add: zprime_zOdd_eq_grt_2 QRTEMP_def)
20.212 done
20.213 - from prems have "~([q = 0] (mod p))"
20.214 + from QRTEMP_axioms have "~([q = 0] (mod p))"
20.215 apply (rule_tac p = q and q = p in pq_prime_neq)
20.216 apply (simp add: QRTEMP_def)+
20.217 done
20.218 - with prems P_set_def have a2: "(Legendre q p) =
20.219 + with QRTEMP_axioms P_set_def have a2: "(Legendre q p) =
20.220 (-1::int) ^ nat(setsum (%x. ((x * q) div p)) P_set)"
20.221 apply (rule_tac p = p in MainQRLemma)
20.222 apply (auto simp add: zprime_zOdd_eq_grt_2 QRTEMP_def)
21.1 --- a/src/HOL/Old_Number_Theory/Residues.thy Thu Jan 13 21:50:13 2011 +0100
21.2 +++ b/src/HOL/Old_Number_Theory/Residues.thy Thu Jan 13 23:50:16 2011 +0100
21.3 @@ -51,10 +51,10 @@
21.4 mod_mult_eq [of x y m])
21.5
21.6 lemma StandardRes_lbound: "0 < p ==> 0 \<le> StandardRes p x"
21.7 - by (auto simp add: StandardRes_def pos_mod_sign)
21.8 + by (auto simp add: StandardRes_def)
21.9
21.10 lemma StandardRes_ubound: "0 < p ==> StandardRes p x < p"
21.11 - by (auto simp add: StandardRes_def pos_mod_bound)
21.12 + by (auto simp add: StandardRes_def)
21.13
21.14 lemma StandardRes_eq_zcong:
21.15 "(StandardRes m x = 0) = ([x = 0](mod m))"
21.16 @@ -71,8 +71,7 @@
21.17
21.18 lemma StandardRes_SRStar_prop1: "2 < p ==> (StandardRes p x \<in> SRStar p)
21.19 = (~[x = 0] (mod p))"
21.20 - apply (auto simp add: StandardRes_prop3 StandardRes_def
21.21 - SRStar_def pos_mod_bound)
21.22 + apply (auto simp add: StandardRes_prop3 StandardRes_def SRStar_def)
21.23 apply (subgoal_tac "0 < p")
21.24 apply (drule_tac a = x in pos_mod_sign, arith, simp)
21.25 done
22.1 --- a/src/HOL/ex/Dedekind_Real.thy Thu Jan 13 21:50:13 2011 +0100
22.2 +++ b/src/HOL/ex/Dedekind_Real.thy Thu Jan 13 23:50:16 2011 +0100
22.3 @@ -354,30 +354,29 @@
22.4
22.5 text{*Part 2 of Dedekind sections definition*}
22.6 lemma preal_not_mem_mult_set_Ex:
22.7 - assumes A: "A \<in> preal"
22.8 - and B: "B \<in> preal"
22.9 - shows "\<exists>q. 0 < q & q \<notin> mult_set A B"
22.10 + assumes A: "A \<in> preal"
22.11 + and B: "B \<in> preal"
22.12 + shows "\<exists>q. 0 < q & q \<notin> mult_set A B"
22.13 proof -
22.14 - from preal_exists_bound [OF A]
22.15 - obtain x where [simp]: "0 < x" "x \<notin> A" by blast
22.16 - from preal_exists_bound [OF B]
22.17 - obtain y where [simp]: "0 < y" "y \<notin> B" by blast
22.18 + from preal_exists_bound [OF A] obtain x where 1 [simp]: "0 < x" "x \<notin> A" by blast
22.19 + from preal_exists_bound [OF B] obtain y where 2 [simp]: "0 < y" "y \<notin> B" by blast
22.20 show ?thesis
22.21 proof (intro exI conjI)
22.22 show "0 < x*y" by (simp add: mult_pos_pos)
22.23 show "x * y \<notin> mult_set A B"
22.24 proof -
22.25 - { fix u::rat and v::rat
22.26 - assume "u \<in> A" and "v \<in> B" and "x*y = u*v"
22.27 - moreover
22.28 - with prems have "u<x" and "v<y" by (blast dest: not_in_preal_ub)+
22.29 - moreover
22.30 - with prems have "0\<le>v"
22.31 - by (blast intro: preal_imp_pos [OF B] order_less_imp_le prems)
22.32 - moreover
22.33 - from calculation
22.34 - have "u*v < x*y" by (blast intro: mult_strict_mono prems)
22.35 - ultimately have False by force }
22.36 + {
22.37 + fix u::rat and v::rat
22.38 + assume u: "u \<in> A" and v: "v \<in> B" and xy: "x*y = u*v"
22.39 + moreover from A B 1 2 u v have "u<x" and "v<y" by (blast dest: not_in_preal_ub)+
22.40 + moreover
22.41 + from A B 1 2 u v have "0\<le>v"
22.42 + by (blast intro: preal_imp_pos [OF B] order_less_imp_le)
22.43 + moreover
22.44 + from A B 1 `u < x` `v < y` `0 \<le> v`
22.45 + have "u*v < x*y" by (blast intro: mult_strict_mono)
22.46 + ultimately have False by force
22.47 + }
22.48 thus ?thesis by (auto simp add: mult_set_def)
22.49 qed
22.50 qed
22.51 @@ -473,7 +472,7 @@
22.52 fix x::rat and u::rat and v::rat
22.53 assume upos: "0<u" and "u<1" and v: "v \<in> A"
22.54 have vpos: "0<v" by (rule preal_imp_pos [OF A v])
22.55 - hence "u*v < 1*v" by (simp only: mult_strict_right_mono prems)
22.56 + hence "u*v < 1*v" by (simp only: mult_strict_right_mono upos `u < 1` v)
22.57 thus "u * v \<in> A"
22.58 by (force intro: preal_downwards_closed [OF A v] mult_pos_pos
22.59 upos vpos)
22.60 @@ -673,18 +672,19 @@
22.61 proof (cases z rule: int_cases)
22.62 case (nonneg n)
22.63 show ?thesis
22.64 - proof (simp add: prems, induct n)
22.65 + proof (simp add: nonneg, induct n)
22.66 case 0
22.67 - from preal_nonempty [OF A]
22.68 - show ?case by force
22.69 + from preal_nonempty [OF A]
22.70 + show ?case by force
22.71 + next
22.72 case (Suc k)
22.73 - from this obtain b where "b \<in> A" "b + of_nat k * u \<in> A" ..
22.74 - hence "b + of_int (int k)*u + u \<in> A" by (simp add: prems)
22.75 - thus ?case by (force simp add: algebra_simps prems)
22.76 + then obtain b where b: "b \<in> A" "b + of_nat k * u \<in> A" ..
22.77 + hence "b + of_int (int k)*u + u \<in> A" by (simp add: assms)
22.78 + thus ?case by (force simp add: algebra_simps b)
22.79 qed
22.80 next
22.81 case (neg n)
22.82 - with prems show ?thesis by simp
22.83 + with assms show ?thesis by simp
22.84 qed
22.85
22.86 lemma Gleason9_34_contra:
22.87 @@ -987,10 +987,9 @@
22.88 proof -
22.89 have "0<a" by (rule preal_imp_pos [OF Rep_preal a])
22.90 moreover
22.91 - have "a < c" using prems
22.92 - by (blast intro: not_in_Rep_preal_ub )
22.93 - ultimately show ?thesis using prems
22.94 - by (simp add: preal_downwards_closed [OF Rep_preal cb])
22.95 + have "a < c" using assms by (blast intro: not_in_Rep_preal_ub )
22.96 + ultimately show ?thesis
22.97 + using assms by (simp add: preal_downwards_closed [OF Rep_preal cb])
22.98 qed
22.99
22.100 lemma less_add_left_le1:
22.101 @@ -1225,13 +1224,13 @@
22.102
22.103 lemma preal_trans_lemma:
22.104 assumes "x + y1 = x1 + y"
22.105 - and "x + y2 = x2 + y"
22.106 + and "x + y2 = x2 + y"
22.107 shows "x1 + y2 = x2 + (y1::preal)"
22.108 proof -
22.109 have "(x1 + y2) + x = (x + y2) + x1" by (simp add: add_ac)
22.110 - also have "... = (x2 + y) + x1" by (simp add: prems)
22.111 + also have "... = (x2 + y) + x1" by (simp add: assms)
22.112 also have "... = x2 + (x1 + y)" by (simp add: add_ac)
22.113 - also have "... = x2 + (x + y1)" by (simp add: prems)
22.114 + also have "... = x2 + (x + y1)" by (simp add: assms)
22.115 also have "... = (x2 + y1) + x" by (simp add: add_ac)
22.116 finally have "(x1 + y2) + x = (x2 + y1) + x" .
22.117 thus ?thesis by (rule add_right_imp_eq)
22.118 @@ -1436,20 +1435,20 @@
22.119 assumes eq: "a+b = c+d" and le: "c \<le> a"
22.120 shows "b \<le> (d::preal)"
22.121 proof -
22.122 - have "c+d \<le> a+d" by (simp add: prems)
22.123 - hence "a+b \<le> a+d" by (simp add: prems)
22.124 + have "c+d \<le> a+d" by (simp add: le)
22.125 + hence "a+b \<le> a+d" by (simp add: eq)
22.126 thus "b \<le> d" by simp
22.127 qed
22.128
22.129 lemma real_le_lemma:
22.130 assumes l: "u1 + v2 \<le> u2 + v1"
22.131 - and "x1 + v1 = u1 + y1"
22.132 - and "x2 + v2 = u2 + y2"
22.133 + and "x1 + v1 = u1 + y1"
22.134 + and "x2 + v2 = u2 + y2"
22.135 shows "x1 + y2 \<le> x2 + (y1::preal)"
22.136 proof -
22.137 - have "(x1+v1) + (u2+y2) = (u1+y1) + (x2+v2)" by (simp add: prems)
22.138 + have "(x1+v1) + (u2+y2) = (u1+y1) + (x2+v2)" by (simp add: assms)
22.139 hence "(x1+y2) + (u2+v1) = (x2+y1) + (u1+v2)" by (simp add: add_ac)
22.140 - also have "... \<le> (x2+y1) + (u2+v1)" by (simp add: prems)
22.141 + also have "... \<le> (x2+y1) + (u2+v1)" by (simp add: assms)
22.142 finally show ?thesis by simp
22.143 qed
22.144
22.145 @@ -1465,13 +1464,13 @@
22.146
22.147 lemma real_trans_lemma:
22.148 assumes "x + v \<le> u + y"
22.149 - and "u + v' \<le> u' + v"
22.150 - and "x2 + v2 = u2 + y2"
22.151 + and "u + v' \<le> u' + v"
22.152 + and "x2 + v2 = u2 + y2"
22.153 shows "x + v' \<le> u' + (y::preal)"
22.154 proof -
22.155 have "(x+v') + (u+v) = (x+v) + (u+v')" by (simp add: add_ac)
22.156 - also have "... \<le> (u+y) + (u+v')" by (simp add: prems)
22.157 - also have "... \<le> (u+y) + (u'+v)" by (simp add: prems)
22.158 + also have "... \<le> (u+y) + (u+v')" by (simp add: assms)
22.159 + also have "... \<le> (u+y) + (u'+v)" by (simp add: assms)
22.160 also have "... = (u'+y) + (u+v)" by (simp add: add_ac)
22.161 finally show ?thesis by simp
22.162 qed
22.163 @@ -1947,7 +1946,7 @@
22.164 proof -
22.165 have "\<exists>x. isLub UNIV S x"
22.166 by (rule reals_complete)
22.167 - (auto simp add: isLub_def isUb_def leastP_def setle_def setge_def prems)
22.168 + (auto simp add: isLub_def isUb_def leastP_def setle_def setge_def assms)
22.169 thus ?thesis
22.170 by (metis UNIV_I isLub_isUb isLub_le_isUb isUbD isUb_def setleI)
22.171 qed