eliminated global prems;
authorwenzelm
Thu Jan 13 23:50:16 2011 +0100 (2011-01-13 ago)
changeset 415411fa4725c4656
parent 41540 414a68d72279
child 41542 a5478b1c8b8a
child 41543 646a1399e792
child 41548 bd0bebf93fa6
eliminated global prems;
tuned proofs;
src/HOL/Algebra/Sylow.thy
src/HOL/Metis_Examples/BigO.thy
src/HOL/MicroJava/DFA/Err.thy
src/HOL/MicroJava/DFA/Kildall.thy
src/HOL/MicroJava/DFA/Product.thy
src/HOL/NSA/NSA.thy
src/HOL/Number_Theory/Binomial.thy
src/HOL/Number_Theory/Cong.thy
src/HOL/Number_Theory/Fib.thy
src/HOL/Number_Theory/MiscAlgebra.thy
src/HOL/Number_Theory/Residues.thy
src/HOL/Number_Theory/UniqueFactorization.thy
src/HOL/Old_Number_Theory/Euler.thy
src/HOL/Old_Number_Theory/Gauss.thy
src/HOL/Old_Number_Theory/Int2.thy
src/HOL/Old_Number_Theory/IntPrimes.thy
src/HOL/Old_Number_Theory/Legacy_GCD.thy
src/HOL/Old_Number_Theory/Pocklington.thy
src/HOL/Old_Number_Theory/Primes.thy
src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy
src/HOL/Old_Number_Theory/Residues.thy
src/HOL/ex/Dedekind_Real.thy
     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