eliminated global prems;
authorwenzelm
Fri Jan 14 15:44:47 2011 +0100 (2011-01-14)
changeset 41550efa734d9b221
parent 41549 2c65ad10bec8
child 41551 791b139a6c1e
eliminated global prems;
tuned proofs;
src/HOL/Big_Operators.thy
src/HOL/Deriv.thy
src/HOL/Divides.thy
src/HOL/Fact.thy
src/HOL/Finite_Set.thy
src/HOL/GCD.thy
src/HOL/Import/HOL4Compat.thy
src/HOL/Import/HOL4Setup.thy
src/HOL/Lim.thy
src/HOL/Ln.thy
src/HOL/Log.thy
src/HOL/Map.thy
src/HOL/Matrix/ComputeFloat.thy
src/HOL/Matrix/LP.thy
src/HOL/Nominal/Nominal.thy
src/HOL/Power.thy
src/HOL/Predicate.thy
src/HOL/RComplete.thy
src/HOL/RealDef.thy
src/HOL/Transcendental.thy
src/HOL/Word/Word.thy
     1.1 --- a/src/HOL/Big_Operators.thy	Fri Jan 14 15:43:04 2011 +0100
     1.2 +++ b/src/HOL/Big_Operators.thy	Fri Jan 14 15:44:47 2011 +0100
     1.3 @@ -172,7 +172,7 @@
     1.4  lemma (in comm_monoid_add) setsum_reindex_cong:
     1.5     "[|inj_on f A; B = f ` A; !!a. a:A \<Longrightarrow> g a = h (f a)|] 
     1.6      ==> setsum h B = setsum g A"
     1.7 -  by (simp add: setsum_reindex cong: setsum_cong)
     1.8 +  by (simp add: setsum_reindex)
     1.9  
    1.10  lemma (in comm_monoid_add) setsum_0[simp]: "setsum (%i. 0) A = 0"
    1.11    by (cases "finite A") (erule finite_induct, auto)
    1.12 @@ -288,7 +288,7 @@
    1.13    shows "setsum f (UNION I A) = (\<Sum>i\<in>I. setsum f (A i))"
    1.14  proof -
    1.15    interpret comm_monoid_mult "op +" 0 by (fact comm_monoid_mult)
    1.16 -  from assms show ?thesis by (simp add: setsum_def fold_image_UN_disjoint cong: setsum_cong)
    1.17 +  from assms show ?thesis by (simp add: setsum_def fold_image_UN_disjoint)
    1.18  qed
    1.19  
    1.20  text{*No need to assume that @{term C} is finite.  If infinite, the rhs is
    1.21 @@ -310,7 +310,7 @@
    1.22    shows "(\<Sum>x\<in>A. (\<Sum>y\<in>B x. f x y)) = (\<Sum>(x,y)\<in>(SIGMA x:A. B x). f x y)"
    1.23  proof -
    1.24    interpret comm_monoid_mult "op +" 0 by (fact comm_monoid_mult)
    1.25 -  from assms show ?thesis by (simp add: setsum_def fold_image_Sigma split_def cong: setsum_cong)
    1.26 +  from assms show ?thesis by (simp add: setsum_def fold_image_Sigma split_def)
    1.27  qed
    1.28  
    1.29  text{*Here we can eliminate the finiteness assumptions, by cases.*}
    1.30 @@ -498,7 +498,7 @@
    1.31    assumes "finite A"  "A \<noteq> {}"
    1.32      and "!!x. x:A \<Longrightarrow> f x < g x"
    1.33    shows "setsum f A < setsum g A"
    1.34 -  using prems
    1.35 +  using assms
    1.36  proof (induct rule: finite_ne_induct)
    1.37    case singleton thus ?case by simp
    1.38  next
    1.39 @@ -775,7 +775,7 @@
    1.40  apply (subgoal_tac
    1.41           "setsum (%i. card (A i)) I = setsum (%i. (setsum (%x. 1) (A i))) I")
    1.42  apply (simp add: setsum_UN_disjoint del: setsum_constant)
    1.43 -apply (simp cong: setsum_cong)
    1.44 +apply simp
    1.45  done
    1.46  
    1.47  lemma card_Union_disjoint:
    1.48 @@ -947,7 +947,7 @@
    1.49    let ?f = "(\<lambda>k. if k=a then b k else 1)"
    1.50    {assume a: "a \<notin> S"
    1.51      hence "\<forall> k\<in> S. ?f k = 1" by simp
    1.52 -    hence ?thesis  using a by (simp add: setprod_1 cong add: setprod_cong) }
    1.53 +    hence ?thesis  using a by (simp add: setprod_1) }
    1.54    moreover 
    1.55    {assume a: "a \<in> S"
    1.56      let ?A = "S - {a}"
    1.57 @@ -959,7 +959,7 @@
    1.58      have "setprod ?f ?A * setprod ?f ?B = setprod ?f S"
    1.59        using setprod_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
    1.60        by simp
    1.61 -    then have ?thesis  using a by (simp add: fA1 cong add: setprod_cong cong del: if_weak_cong)}
    1.62 +    then have ?thesis using a by (simp add: fA1 cong: setprod_cong cong del: if_weak_cong)}
    1.63    ultimately show ?thesis by blast
    1.64  qed
    1.65  
    1.66 @@ -975,7 +975,7 @@
    1.67      "finite I ==> (ALL i:I. finite (A i)) ==>
    1.68          (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
    1.69        setprod f (UNION I A) = setprod (%i. setprod f (A i)) I"
    1.70 -by(simp add: setprod_def fold_image_UN_disjoint cong: setprod_cong)
    1.71 +  by (simp add: setprod_def fold_image_UN_disjoint)
    1.72  
    1.73  lemma setprod_Union_disjoint:
    1.74    "[| (ALL A:C. finite A);
    1.75 @@ -990,7 +990,7 @@
    1.76  lemma setprod_Sigma: "finite A ==> ALL x:A. finite (B x) ==>
    1.77      (\<Prod>x\<in>A. (\<Prod>y\<in> B x. f x y)) =
    1.78      (\<Prod>(x,y)\<in>(SIGMA x:A. B x). f x y)"
    1.79 -by(simp add:setprod_def fold_image_Sigma split_def cong:setprod_cong)
    1.80 +by(simp add:setprod_def fold_image_Sigma split_def)
    1.81  
    1.82  text{*Here we can eliminate the finiteness assumptions, by cases.*}
    1.83  lemma setprod_cartesian_product: 
    1.84 @@ -1332,7 +1332,7 @@
    1.85    shows "sup (\<Sqinter>\<^bsub>fin\<^esub>A) (\<Sqinter>\<^bsub>fin\<^esub>B) = \<Sqinter>\<^bsub>fin\<^esub>{sup a b|a b. a \<in> A \<and> b \<in> B}"
    1.86  using A proof (induct rule: finite_ne_induct)
    1.87    case singleton thus ?case
    1.88 -    by (simp add: sup_Inf1_distrib [OF B] fold1_singleton_def [OF Inf_fin_def])
    1.89 +    by (simp add: sup_Inf1_distrib [OF B])
    1.90  next
    1.91    interpret ab_semigroup_idem_mult inf
    1.92      by (rule ab_semigroup_idem_mult_inf)
    1.93 @@ -1347,7 +1347,7 @@
    1.94    qed
    1.95    have ne: "{sup a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
    1.96    have "sup (\<Sqinter>\<^bsub>fin\<^esub>(insert x A)) (\<Sqinter>\<^bsub>fin\<^esub>B) = sup (inf x (\<Sqinter>\<^bsub>fin\<^esub>A)) (\<Sqinter>\<^bsub>fin\<^esub>B)"
    1.97 -    using insert by (simp add: fold1_insert_idem_def [OF Inf_fin_def])
    1.98 +    using insert by simp
    1.99    also have "\<dots> = inf (sup x (\<Sqinter>\<^bsub>fin\<^esub>B)) (sup (\<Sqinter>\<^bsub>fin\<^esub>A) (\<Sqinter>\<^bsub>fin\<^esub>B))" by(rule sup_inf_distrib2)
   1.100    also have "\<dots> = inf (\<Sqinter>\<^bsub>fin\<^esub>{sup x b|b. b \<in> B}) (\<Sqinter>\<^bsub>fin\<^esub>{sup a b|a b. a \<in> A \<and> b \<in> B})"
   1.101      using insert by(simp add:sup_Inf1_distrib[OF B])
   1.102 @@ -1391,7 +1391,7 @@
   1.103    interpret ab_semigroup_idem_mult sup
   1.104      by (rule ab_semigroup_idem_mult_sup)
   1.105    have "inf (\<Squnion>\<^bsub>fin\<^esub>(insert x A)) (\<Squnion>\<^bsub>fin\<^esub>B) = inf (sup x (\<Squnion>\<^bsub>fin\<^esub>A)) (\<Squnion>\<^bsub>fin\<^esub>B)"
   1.106 -    using insert by (simp add: fold1_insert_idem_def [OF Sup_fin_def])
   1.107 +    using insert by simp
   1.108    also have "\<dots> = sup (inf x (\<Squnion>\<^bsub>fin\<^esub>B)) (inf (\<Squnion>\<^bsub>fin\<^esub>A) (\<Squnion>\<^bsub>fin\<^esub>B))" by(rule inf_sup_distrib2)
   1.109    also have "\<dots> = sup (\<Squnion>\<^bsub>fin\<^esub>{inf x b|b. b \<in> B}) (\<Squnion>\<^bsub>fin\<^esub>{inf a b|a b. a \<in> A \<and> b \<in> B})"
   1.110      using insert by(simp add:inf_Sup1_distrib[OF B])
   1.111 @@ -1551,15 +1551,15 @@
   1.112  next
   1.113    interpret ab_semigroup_idem_mult min
   1.114      by (rule ab_semigroup_idem_mult_min)
   1.115 -  assume "A \<noteq> B"
   1.116 +  assume neq: "A \<noteq> B"
   1.117    have B: "B = A \<union> (B-A)" using `A \<subseteq> B` by blast
   1.118    have "fold1 min B = fold1 min (A \<union> (B-A))" by(subst B)(rule refl)
   1.119    also have "\<dots> = min (fold1 min A) (fold1 min (B-A))"
   1.120    proof -
   1.121      have "finite A" by(rule finite_subset[OF `A \<subseteq> B` `finite B`])
   1.122 -    moreover have "finite(B-A)" by(rule finite_Diff[OF `finite B`]) (* by(blast intro:finite_Diff prems) fails *)
   1.123 -    moreover have "(B-A) \<noteq> {}" using prems by blast
   1.124 -    moreover have "A Int (B-A) = {}" using prems by blast
   1.125 +    moreover have "finite(B-A)" by(rule finite_Diff[OF `finite B`])
   1.126 +    moreover have "(B-A) \<noteq> {}" using assms neq by blast
   1.127 +    moreover have "A Int (B-A) = {}" using assms by blast
   1.128      ultimately show ?thesis using `A \<noteq> {}` by (rule_tac fold1_Un)
   1.129    qed
   1.130    also have "\<dots> \<le> fold1 min A" by (simp add: min_le_iff_disj)
     2.1 --- a/src/HOL/Deriv.thy	Fri Jan 14 15:43:04 2011 +0100
     2.2 +++ b/src/HOL/Deriv.thy	Fri Jan 14 15:44:47 2011 +0100
     2.3 @@ -355,7 +355,7 @@
     2.4  lemma differentiableE [elim?]:
     2.5    assumes "f differentiable x"
     2.6    obtains df where "DERIV f x :> df"
     2.7 -  using prems unfolding differentiable_def ..
     2.8 +  using assms unfolding differentiable_def ..
     2.9  
    2.10  lemma differentiableD: "f differentiable x ==> \<exists>D. DERIV f x :> D"
    2.11  by (simp add: differentiable_def)
    2.12 @@ -408,7 +408,7 @@
    2.13    assumes "f differentiable x"
    2.14    assumes "g differentiable x"
    2.15    shows "(\<lambda>x. f x - g x) differentiable x"
    2.16 -  unfolding diff_minus using prems by simp
    2.17 +  unfolding diff_minus using assms by simp
    2.18  
    2.19  lemma differentiable_mult [simp]:
    2.20    assumes "f differentiable x"
    2.21 @@ -437,13 +437,16 @@
    2.22    assumes "f differentiable x"
    2.23    assumes "g differentiable x" and "g x \<noteq> 0"
    2.24    shows "(\<lambda>x. f x / g x) differentiable x"
    2.25 -  unfolding divide_inverse using prems by simp
    2.26 +  unfolding divide_inverse using assms by simp
    2.27  
    2.28  lemma differentiable_power [simp]:
    2.29    fixes f :: "'a::{real_normed_field} \<Rightarrow> 'a"
    2.30    assumes "f differentiable x"
    2.31    shows "(\<lambda>x. f x ^ n) differentiable x"
    2.32 -  by (induct n, simp, simp add: prems)
    2.33 +  apply (induct n)
    2.34 +  apply simp
    2.35 +  apply (simp add: assms)
    2.36 +  done
    2.37  
    2.38  
    2.39  subsection {* Nested Intervals and Bisection *}
    2.40 @@ -1227,7 +1230,7 @@
    2.41    assumes "a < b" and "\<forall>x. a \<le> x & x \<le> b --> (EX y. DERIV f x :> y & y > 0)"
    2.42    shows "f a < f b"
    2.43  proof (rule ccontr)
    2.44 -  assume "~ f a < f b"
    2.45 +  assume f: "~ f a < f b"
    2.46    have "EX l z. a < z & z < b & DERIV f z :> l
    2.47        & f b - f a = (b - a) * l"
    2.48      apply (rule MVT)
    2.49 @@ -1236,13 +1239,12 @@
    2.50        apply (metis DERIV_isCont)
    2.51       apply (metis differentiableI less_le)
    2.52      done
    2.53 -  then obtain l z where "a < z" and "z < b" and "DERIV f z :> l"
    2.54 +  then obtain l z where z: "a < z" "z < b" "DERIV f z :> l"
    2.55        and "f b - f a = (b - a) * l"
    2.56      by auto
    2.57 -  
    2.58 -  from prems have "~(l > 0)"
    2.59 +  with assms f have "~(l > 0)"
    2.60      by (metis linorder_not_le mult_le_0_iff diff_le_0_iff_le)
    2.61 -  with prems show False
    2.62 +  with assms z show False
    2.63      by (metis DERIV_unique less_le)
    2.64  qed
    2.65  
    2.66 @@ -1252,9 +1254,8 @@
    2.67      "\<forall>x. a \<le> x & x \<le> b --> (\<exists>y. DERIV f x :> y & y \<ge> 0)"
    2.68    shows "f a \<le> f b"
    2.69  proof (rule ccontr, cases "a = b")
    2.70 -  assume "~ f a \<le> f b"
    2.71 -  assume "a = b"
    2.72 -  with prems show False by auto
    2.73 +  assume "~ f a \<le> f b" and "a = b"
    2.74 +  then show False by auto
    2.75  next
    2.76    assume A: "~ f a \<le> f b"
    2.77    assume B: "a ~= b"
    2.78 @@ -1266,13 +1267,13 @@
    2.79        apply (metis DERIV_isCont)
    2.80       apply (metis differentiableI less_le)
    2.81      done
    2.82 -  then obtain l z where "a < z" and "z < b" and "DERIV f z :> l"
    2.83 +  then obtain l z where z: "a < z" "z < b" "DERIV f z :> l"
    2.84        and C: "f b - f a = (b - a) * l"
    2.85      by auto
    2.86    with A have "a < b" "f b < f a" by auto
    2.87    with C have "\<not> l \<ge> 0" by (auto simp add: not_le algebra_simps)
    2.88      (metis A add_le_cancel_right assms(1) less_eq_real_def mult_right_mono real_add_left_mono real_le_linear real_le_refl)
    2.89 -  with prems show False
    2.90 +  with assms z show False
    2.91      by (metis DERIV_unique order_less_imp_le)
    2.92  qed
    2.93  
    2.94 @@ -1509,14 +1510,14 @@
    2.95  theorem GMVT:
    2.96    fixes a b :: real
    2.97    assumes alb: "a < b"
    2.98 -  and fc: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x"
    2.99 -  and fd: "\<forall>x. a < x \<and> x < b \<longrightarrow> f differentiable x"
   2.100 -  and gc: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont g x"
   2.101 -  and gd: "\<forall>x. a < x \<and> x < b \<longrightarrow> g differentiable x"
   2.102 +    and fc: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x"
   2.103 +    and fd: "\<forall>x. a < x \<and> x < b \<longrightarrow> f differentiable x"
   2.104 +    and gc: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont g x"
   2.105 +    and gd: "\<forall>x. a < x \<and> x < b \<longrightarrow> g differentiable x"
   2.106    shows "\<exists>g'c f'c c. DERIV g c :> g'c \<and> DERIV f c :> f'c \<and> a < c \<and> c < b \<and> ((f b - f a) * g'c) = ((g b - g a) * f'c)"
   2.107  proof -
   2.108    let ?h = "\<lambda>x. (f b - f a)*(g x) - (g b - g a)*(f x)"
   2.109 -  from prems have "a < b" by simp
   2.110 +  from assms have "a < b" by simp
   2.111    moreover have "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont ?h x"
   2.112    proof -
   2.113      have "\<forall>x. a <= x \<and> x <= b \<longrightarrow> isCont (\<lambda>x. f b - f a) x" by simp
     3.1 --- a/src/HOL/Divides.thy	Fri Jan 14 15:43:04 2011 +0100
     3.2 +++ b/src/HOL/Divides.thy	Fri Jan 14 15:44:47 2011 +0100
     3.3 @@ -681,8 +681,8 @@
     3.4  ML {*
     3.5  local
     3.6  
     3.7 -structure CancelDivMod = CancelDivModFun(struct
     3.8 -
     3.9 +structure CancelDivMod = CancelDivModFun
    3.10 +(
    3.11    val div_name = @{const_name div};
    3.12    val mod_name = @{const_name mod};
    3.13    val mk_binop = HOLogic.mk_binop;
    3.14 @@ -691,12 +691,9 @@
    3.15  
    3.16    val div_mod_eqs = map mk_meta_eq [@{thm div_mod_equality}, @{thm div_mod_equality2}];
    3.17  
    3.18 -  val trans = trans;
    3.19 -
    3.20    val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac
    3.21      (@{thm add_0_left} :: @{thm add_0_right} :: @{thms add_ac}))
    3.22 -
    3.23 -end)
    3.24 +)
    3.25  
    3.26  in
    3.27  
    3.28 @@ -1352,15 +1349,16 @@
    3.29  theorem posDivAlg_correct:
    3.30    assumes "0 \<le> a" and "0 < b"
    3.31    shows "divmod_int_rel a b (posDivAlg a b)"
    3.32 -using prems apply (induct a b rule: posDivAlg.induct)
    3.33 -apply auto
    3.34 -apply (simp add: divmod_int_rel_def)
    3.35 -apply (subst posDivAlg_eqn, simp add: right_distrib)
    3.36 -apply (case_tac "a < b")
    3.37 -apply simp_all
    3.38 -apply (erule splitE)
    3.39 -apply (auto simp add: right_distrib Let_def mult_ac mult_2_right)
    3.40 -done
    3.41 +  using assms
    3.42 +  apply (induct a b rule: posDivAlg.induct)
    3.43 +  apply auto
    3.44 +  apply (simp add: divmod_int_rel_def)
    3.45 +  apply (subst posDivAlg_eqn, simp add: right_distrib)
    3.46 +  apply (case_tac "a < b")
    3.47 +  apply simp_all
    3.48 +  apply (erule splitE)
    3.49 +  apply (auto simp add: right_distrib Let_def mult_ac mult_2_right)
    3.50 +  done
    3.51  
    3.52  
    3.53  subsubsection{*Correctness of @{term negDivAlg}, the Algorithm for Negative Dividends*}
    3.54 @@ -1381,15 +1379,16 @@
    3.55  lemma negDivAlg_correct:
    3.56    assumes "a < 0" and "b > 0"
    3.57    shows "divmod_int_rel a b (negDivAlg a b)"
    3.58 -using prems apply (induct a b rule: negDivAlg.induct)
    3.59 -apply (auto simp add: linorder_not_le)
    3.60 -apply (simp add: divmod_int_rel_def)
    3.61 -apply (subst negDivAlg_eqn, assumption)
    3.62 -apply (case_tac "a + b < (0\<Colon>int)")
    3.63 -apply simp_all
    3.64 -apply (erule splitE)
    3.65 -apply (auto simp add: right_distrib Let_def mult_ac mult_2_right)
    3.66 -done
    3.67 +  using assms
    3.68 +  apply (induct a b rule: negDivAlg.induct)
    3.69 +  apply (auto simp add: linorder_not_le)
    3.70 +  apply (simp add: divmod_int_rel_def)
    3.71 +  apply (subst negDivAlg_eqn, assumption)
    3.72 +  apply (case_tac "a + b < (0\<Colon>int)")
    3.73 +  apply simp_all
    3.74 +  apply (erule splitE)
    3.75 +  apply (auto simp add: right_distrib Let_def mult_ac mult_2_right)
    3.76 +  done
    3.77  
    3.78  
    3.79  subsubsection{*Existence Shown by Proving the Division Algorithm to be Correct*}
    3.80 @@ -1440,8 +1439,8 @@
    3.81  ML {*
    3.82  local
    3.83  
    3.84 -structure CancelDivMod = CancelDivModFun(struct
    3.85 -
    3.86 +structure CancelDivMod = CancelDivModFun
    3.87 +(
    3.88    val div_name = @{const_name div};
    3.89    val mod_name = @{const_name mod};
    3.90    val mk_binop = HOLogic.mk_binop;
    3.91 @@ -1450,12 +1449,9 @@
    3.92  
    3.93    val div_mod_eqs = map mk_meta_eq [@{thm zdiv_zmod_equality}, @{thm zdiv_zmod_equality2}];
    3.94  
    3.95 -  val trans = trans;
    3.96 -
    3.97    val prove_eq_sums = Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac 
    3.98      (@{thm diff_minus} :: @{thms add_0s} @ @{thms add_ac}))
    3.99 -
   3.100 -end)
   3.101 +)
   3.102  
   3.103  in
   3.104  
     4.1 --- a/src/HOL/Fact.thy	Fri Jan 14 15:43:04 2011 +0100
     4.2 +++ b/src/HOL/Fact.thy	Fri Jan 14 15:44:47 2011 +0100
     4.3 @@ -12,12 +12,9 @@
     4.4  begin
     4.5  
     4.6  class fact =
     4.7 -
     4.8 -fixes 
     4.9 -  fact :: "'a \<Rightarrow> 'a"
    4.10 +  fixes fact :: "'a \<Rightarrow> 'a"
    4.11  
    4.12  instantiation nat :: fact
    4.13 -
    4.14  begin 
    4.15  
    4.16  fun
    4.17 @@ -26,7 +23,7 @@
    4.18    fact_0_nat: "fact_nat 0 = Suc 0"
    4.19  | fact_Suc: "fact_nat (Suc x) = Suc x * fact x"
    4.20  
    4.21 -instance proof qed
    4.22 +instance ..
    4.23  
    4.24  end
    4.25  
    4.26 @@ -93,8 +90,7 @@
    4.27  lemma fact_plus_one_int: 
    4.28    assumes "n >= 0"
    4.29    shows "fact ((n::int) + 1) = (n + 1) * fact n"
    4.30 -
    4.31 -  using prems unfolding fact_int_def 
    4.32 +  using assms unfolding fact_int_def 
    4.33    by (simp add: nat_add_distrib algebra_simps int_mult)
    4.34  
    4.35  lemma fact_reduce_nat: "(n::nat) > 0 \<Longrightarrow> fact n = n * fact (n - 1)"
    4.36 @@ -102,19 +98,19 @@
    4.37    apply (erule ssubst)
    4.38    apply (subst fact_Suc)
    4.39    apply simp_all
    4.40 -done
    4.41 +  done
    4.42  
    4.43  lemma fact_reduce_int: "(n::int) > 0 \<Longrightarrow> fact n = n * fact (n - 1)"
    4.44    apply (subgoal_tac "n = (n - 1) + 1")
    4.45    apply (erule ssubst)
    4.46    apply (subst fact_plus_one_int)
    4.47    apply simp_all
    4.48 -done
    4.49 +  done
    4.50  
    4.51  lemma fact_nonzero_nat [simp]: "fact (n::nat) \<noteq> 0"
    4.52    apply (induct n)
    4.53    apply (auto simp add: fact_plus_one_nat)
    4.54 -done
    4.55 +  done
    4.56  
    4.57  lemma fact_nonzero_int [simp]: "n >= 0 \<Longrightarrow> fact (n::int) ~= 0"
    4.58    by (simp add: fact_int_def)
    4.59 @@ -137,7 +133,7 @@
    4.60    apply (erule ssubst)
    4.61    apply (subst zle_int)
    4.62    apply auto
    4.63 -done
    4.64 +  done
    4.65  
    4.66  lemma dvd_fact_nat [rule_format]: "1 <= m \<longrightarrow> m <= n \<longrightarrow> m dvd fact (n::nat)"
    4.67    apply (induct n)
    4.68 @@ -147,7 +143,7 @@
    4.69    apply (erule ssubst)
    4.70    apply (rule dvd_triv_left)
    4.71    apply auto
    4.72 -done
    4.73 +  done
    4.74  
    4.75  lemma dvd_fact_int [rule_format]: "1 <= m \<longrightarrow> m <= n \<longrightarrow> m dvd fact (n::int)"
    4.76    apply (case_tac "1 <= n")
    4.77 @@ -155,7 +151,7 @@
    4.78    apply (auto simp add: fact_plus_one_int)
    4.79    apply (subgoal_tac "m = i + 1")
    4.80    apply auto
    4.81 -done
    4.82 +  done
    4.83  
    4.84  lemma interval_plus_one_nat: "(i::nat) <= j + 1 \<Longrightarrow> 
    4.85    {i..j+1} = {i..j} Un {j+1}"
     5.1 --- a/src/HOL/Finite_Set.thy	Fri Jan 14 15:43:04 2011 +0100
     5.2 +++ b/src/HOL/Finite_Set.thy	Fri Jan 14 15:44:47 2011 +0100
     5.3 @@ -803,7 +803,7 @@
     5.4  proof -
     5.5    interpret fun_left_comm_idem inf by (fact fun_left_comm_idem_inf)
     5.6    from `finite A` show ?thesis by (induct A arbitrary: B)
     5.7 -    (simp_all add: Inf_empty Inf_insert inf_commute fold_fun_comm)
     5.8 +    (simp_all add: Inf_insert inf_commute fold_fun_comm)
     5.9  qed
    5.10  
    5.11  lemma sup_Sup_fold_sup:
    5.12 @@ -812,7 +812,7 @@
    5.13  proof -
    5.14    interpret fun_left_comm_idem sup by (fact fun_left_comm_idem_sup)
    5.15    from `finite A` show ?thesis by (induct A arbitrary: B)
    5.16 -    (simp_all add: Sup_empty Sup_insert sup_commute fold_fun_comm)
    5.17 +    (simp_all add: Sup_insert sup_commute fold_fun_comm)
    5.18  qed
    5.19  
    5.20  lemma Inf_fold_inf:
    5.21 @@ -833,7 +833,7 @@
    5.22    interpret fun_left_comm_idem "\<lambda>A. inf (f A)" by (fact fun_left_comm_idem_apply)
    5.23    from `finite A` show "?fold = ?inf"
    5.24    by (induct A arbitrary: B)
    5.25 -    (simp_all add: INFI_def Inf_empty Inf_insert inf_left_commute)
    5.26 +    (simp_all add: INFI_def Inf_insert inf_left_commute)
    5.27  qed
    5.28  
    5.29  lemma sup_SUPR_fold_sup:
    5.30 @@ -844,7 +844,7 @@
    5.31    interpret fun_left_comm_idem "\<lambda>A. sup (f A)" by (fact fun_left_comm_idem_apply)
    5.32    from `finite A` show "?fold = ?sup"
    5.33    by (induct A arbitrary: B)
    5.34 -    (simp_all add: SUPR_def Sup_empty Sup_insert sup_left_commute)
    5.35 +    (simp_all add: SUPR_def Sup_insert sup_left_commute)
    5.36  qed
    5.37  
    5.38  lemma INFI_fold_inf:
    5.39 @@ -1197,19 +1197,19 @@
    5.40      by (auto simp add: nonempty_iff)
    5.41    show ?thesis
    5.42    proof cases
    5.43 -    assume "a = x"
    5.44 -    thus ?thesis
    5.45 +    assume a: "a = x"
    5.46 +    show ?thesis
    5.47      proof cases
    5.48        assume "A' = {}"
    5.49 -      with prems show ?thesis by simp
    5.50 +      with A' a show ?thesis by simp
    5.51      next
    5.52        assume "A' \<noteq> {}"
    5.53 -      with prems show ?thesis
    5.54 +      with A A' a show ?thesis
    5.55          by (simp add: fold1_insert mult_assoc [symmetric])
    5.56      qed
    5.57    next
    5.58      assume "a \<noteq> x"
    5.59 -    with prems show ?thesis
    5.60 +    with A A' show ?thesis
    5.61        by (simp add: insert_commute fold1_eq_fold)
    5.62    qed
    5.63  qed
     6.1 --- a/src/HOL/GCD.thy	Fri Jan 14 15:43:04 2011 +0100
     6.2 +++ b/src/HOL/GCD.thy	Fri Jan 14 15:44:47 2011 +0100
     6.3 @@ -36,11 +36,8 @@
     6.4  subsection {* GCD and LCM definitions *}
     6.5  
     6.6  class gcd = zero + one + dvd +
     6.7 -
     6.8 -fixes
     6.9 -  gcd :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" and
    6.10 -  lcm :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    6.11 -
    6.12 +  fixes gcd :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    6.13 +    and lcm :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    6.14  begin
    6.15  
    6.16  abbreviation
    6.17 @@ -186,7 +183,7 @@
    6.18        and "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (lcm (-x) y)"
    6.19        and "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (lcm (-x) (-y))"
    6.20    shows "P (lcm x y)"
    6.21 -by (insert prems, auto simp add: lcm_neg1_int lcm_neg2_int, arith)
    6.22 +  using assms by (auto simp add: lcm_neg1_int lcm_neg2_int) arith
    6.23  
    6.24  lemma lcm_ge_0_int [simp]: "lcm (x::int) y >= 0"
    6.25    by (simp add: lcm_int_def)
    6.26 @@ -632,13 +629,12 @@
    6.27    apply (subgoal_tac "b' = b div gcd a b")
    6.28    apply (erule ssubst)
    6.29    apply (rule div_gcd_coprime_nat)
    6.30 -  using prems
    6.31 -  apply force
    6.32 +  using z apply force
    6.33    apply (subst (1) b)
    6.34    using z apply force
    6.35    apply (subst (1) a)
    6.36    using z apply force
    6.37 -done
    6.38 +  done
    6.39  
    6.40  lemma gcd_coprime_int:
    6.41    assumes z: "gcd (a::int) b \<noteq> 0" and a: "a = a' * gcd a b" and
    6.42 @@ -650,13 +646,12 @@
    6.43    apply (subgoal_tac "b' = b div gcd a b")
    6.44    apply (erule ssubst)
    6.45    apply (rule div_gcd_coprime_int)
    6.46 -  using prems
    6.47 -  apply force
    6.48 +  using z apply force
    6.49    apply (subst (1) b)
    6.50    using z apply force
    6.51    apply (subst (1) a)
    6.52    using z apply force
    6.53 -done
    6.54 +  done
    6.55  
    6.56  lemma coprime_mult_nat: assumes da: "coprime (d::nat) a" and db: "coprime d b"
    6.57      shows "coprime d (a * b)"
    6.58 @@ -1192,13 +1187,13 @@
    6.59         by auto
    6.60       moreover
    6.61       {assume db: "d=b"
    6.62 -       from prems have ?thesis apply simp
    6.63 +       with nz H have ?thesis apply simp
    6.64           apply (rule exI[where x = b], simp)
    6.65           apply (rule exI[where x = b])
    6.66          by (rule exI[where x = "a - 1"], simp add: diff_mult_distrib2)}
    6.67      moreover
    6.68      {assume db: "d < b"
    6.69 -        {assume "x=0" hence ?thesis  using prems by simp }
    6.70 +        {assume "x=0" hence ?thesis using nz H by simp }
    6.71          moreover
    6.72          {assume x0: "x \<noteq> 0" hence xp: "x > 0" by simp
    6.73            from db have "d \<le> b - 1" by simp
     7.1 --- a/src/HOL/Import/HOL4Compat.thy	Fri Jan 14 15:43:04 2011 +0100
     7.2 +++ b/src/HOL/Import/HOL4Compat.thy	Fri Jan 14 15:44:47 2011 +0100
     7.3 @@ -64,10 +64,10 @@
     7.4    by simp
     7.5  
     7.6  lemma sum_case_def: "(ALL f g x. sum_case f g (Inl x) = f x) & (ALL f g y. sum_case f g (Inr y) = g y)"
     7.7 -  by simp;
     7.8 +  by simp
     7.9  
    7.10  lemma one: "ALL v. v = ()"
    7.11 -  by simp;
    7.12 +  by simp
    7.13  
    7.14  lemma option_case_def: "(!u f. option_case u f None = u) & (!u f x. option_case u f (Some x) = f x)"
    7.15    by simp
    7.16 @@ -103,7 +103,7 @@
    7.17    by (simp add: map_pair_def split_def)
    7.18  
    7.19  lemma pair_case_def: "split = split"
    7.20 -  ..;
    7.21 +  ..
    7.22  
    7.23  lemma LESS_OR_EQ: "m <= (n::nat) = (m < n | m = n)"
    7.24    by auto
    7.25 @@ -128,12 +128,12 @@
    7.26  
    7.27  lemma LESS_DEF: "m < n = (? P. (!n. P (Suc n) --> P n) & P m & ~P n)"
    7.28  proof safe
    7.29 -  assume "m < n"
    7.30 +  assume 1: "m < n"
    7.31    def P == "%n. n <= m"
    7.32    have "(!n. P (Suc n) \<longrightarrow> P n) & P m & ~P n"
    7.33    proof (auto simp add: P_def)
    7.34      assume "n <= m"
    7.35 -    from prems
    7.36 +    with 1
    7.37      show False
    7.38        by auto
    7.39    qed
    7.40 @@ -187,7 +187,7 @@
    7.41      show "m < n"
    7.42        ..
    7.43    qed
    7.44 -qed;
    7.45 +qed
    7.46  
    7.47  definition FUNPOW :: "('a => 'a) => nat => 'a => 'a" where
    7.48    "FUNPOW f n == f ^^ n"
    7.49 @@ -242,10 +242,10 @@
    7.50    by auto
    7.51  
    7.52  lemma num_case_def: "(!b f. nat_case b f 0 = b) & (!b f n. nat_case b f (Suc n) = f n)"
    7.53 -  by simp;
    7.54 +  by simp
    7.55  
    7.56  lemma divides_def: "(a::nat) dvd b = (? q. b = q * a)"
    7.57 -  by (auto simp add: dvd_def);
    7.58 +  by (auto simp add: dvd_def)
    7.59  
    7.60  lemma list_case_def: "(!v f. list_case v f [] = v) & (!v f a0 a1. list_case v f (a0#a1) = f a0 a1)"
    7.61    by simp
    7.62 @@ -263,21 +263,21 @@
    7.63             (list_case v f M = list_case v' f' M')"
    7.64  proof clarify
    7.65    fix M M' v f
    7.66 -  assume "M' = [] \<longrightarrow> v = v'"
    7.67 -    and "!a0 a1. M' = a0 # a1 \<longrightarrow> f a0 a1 = f' a0 a1"
    7.68 +  assume 1: "M' = [] \<longrightarrow> v = v'"
    7.69 +    and 2: "!a0 a1. M' = a0 # a1 \<longrightarrow> f a0 a1 = f' a0 a1"
    7.70    show "list_case v f M' = list_case v' f' M'"
    7.71    proof (rule List.list.case_cong)
    7.72      show "M' = M'"
    7.73        ..
    7.74    next
    7.75      assume "M' = []"
    7.76 -    with prems
    7.77 +    with 1 2
    7.78      show "v = v'"
    7.79        by auto
    7.80    next
    7.81      fix a0 a1
    7.82      assume "M' = a0 # a1"
    7.83 -    with prems
    7.84 +    with 1 2
    7.85      show "f a0 a1 = f' a0 a1"
    7.86        by auto
    7.87    qed
    7.88 @@ -302,14 +302,14 @@
    7.89      by auto
    7.90  next
    7.91    fix fn1 fn2
    7.92 -  assume "ALL h t. fn1 (h # t) = f (fn1 t) h t"
    7.93 -  assume "ALL h t. fn2 (h # t) = f (fn2 t) h t"
    7.94 -  assume "fn2 [] = fn1 []"
    7.95 +  assume 1: "ALL h t. fn1 (h # t) = f (fn1 t) h t"
    7.96 +  assume 2: "ALL h t. fn2 (h # t) = f (fn2 t) h t"
    7.97 +  assume 3: "fn2 [] = fn1 []"
    7.98    show "fn1 = fn2"
    7.99    proof
   7.100      fix xs
   7.101      show "fn1 xs = fn2 xs"
   7.102 -      by (induct xs,simp_all add: prems) 
   7.103 +      by (induct xs) (simp_all add: 1 2 3) 
   7.104    qed
   7.105  qed
   7.106  
   7.107 @@ -411,7 +411,7 @@
   7.108    by (simp add: Let_def)
   7.109  
   7.110  lemma REVERSE: "(rev [] = []) & (!h t. rev (h#t) = (rev t) @ [h])"
   7.111 -  by simp;
   7.112 +  by simp
   7.113  
   7.114  lemma REAL_SUP_ALLPOS: "\<lbrakk> ALL x. P (x::real) \<longrightarrow> 0 < x ; EX x. P x; EX z. ALL x. P x \<longrightarrow> x < z \<rbrakk> \<Longrightarrow> EX s. ALL y. (EX x. P x & y < x) = (y < s)"
   7.115  proof safe
   7.116 @@ -424,12 +424,11 @@
   7.117      show "ALL x : Collect P. 0 < x"
   7.118      proof safe
   7.119        fix x
   7.120 -      assume "P x"
   7.121 +      assume P: "P x"
   7.122        from allx
   7.123        have "P x \<longrightarrow> 0 < x"
   7.124          ..
   7.125 -      thus "0 < x"
   7.126 -        by (simp add: prems)
   7.127 +      with P show "0 < x" by simp
   7.128      qed
   7.129    next
   7.130      from px
   7.131 @@ -461,7 +460,7 @@
   7.132    by simp
   7.133  
   7.134  lemma REAL_LT_TOTAL: "((x::real) = y) | x < y | y < x"
   7.135 -  by auto;
   7.136 +  by auto
   7.137  
   7.138  lemma [hol4rew]: "real (0::nat) = 0"
   7.139    by simp
     8.1 --- a/src/HOL/Import/HOL4Setup.thy	Fri Jan 14 15:43:04 2011 +0100
     8.2 +++ b/src/HOL/Import/HOL4Setup.thy	Fri Jan 14 15:44:47 2011 +0100
     8.3 @@ -90,11 +90,11 @@
     8.4    have ed: "TYPE_DEFINITION P Rep"
     8.5    proof (auto simp add: TYPE_DEFINITION)
     8.6      fix x y
     8.7 -    assume "Rep x = Rep y"
     8.8 +    assume b: "Rep x = Rep y"
     8.9      from td have "x = Abs (Rep x)"
    8.10        by auto
    8.11      also have "Abs (Rep x) = Abs (Rep y)"
    8.12 -      by (simp add: prems)
    8.13 +      by (simp add: b)
    8.14      also from td have "Abs (Rep y) = y"
    8.15        by auto
    8.16      finally show "x = y" .
     9.1 --- a/src/HOL/Lim.thy	Fri Jan 14 15:43:04 2011 +0100
     9.2 +++ b/src/HOL/Lim.thy	Fri Jan 14 15:44:47 2011 +0100
     9.3 @@ -653,7 +653,7 @@
     9.4    moreover have "\<forall>n. ?F n \<noteq> a"
     9.5      by (rule allI) (rule F1)
     9.6  
     9.7 -  moreover from prems have "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L" by simp
     9.8 +  moreover note `\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L`
     9.9    ultimately have "(\<lambda>n. X (?F n)) ----> L" by simp
    9.10    
    9.11    moreover have "\<not> ((\<lambda>n. X (?F n)) ----> L)"
    10.1 --- a/src/HOL/Ln.thy	Fri Jan 14 15:43:04 2011 +0100
    10.2 +++ b/src/HOL/Ln.thy	Fri Jan 14 15:44:47 2011 +0100
    10.3 @@ -71,7 +71,7 @@
    10.4      qed
    10.5      moreover have "x ^ (Suc n + 2) <= x ^ (n + 2)"
    10.6        apply (simp add: mult_compare_simps)
    10.7 -      apply (simp add: prems)
    10.8 +      apply (simp add: assms)
    10.9        apply (subgoal_tac "0 <= x * (x * x^n)")
   10.10        apply force
   10.11        apply (rule mult_nonneg_nonneg, rule a)+
   10.12 @@ -91,7 +91,7 @@
   10.13        by simp
   10.14      also have "... <= 1 / 2 * (x ^ 2 / 2 * (1 / 2) ^ n)"
   10.15        apply (rule mult_left_mono)
   10.16 -      apply (rule prems)
   10.17 +      apply (rule c)
   10.18        apply simp
   10.19        done
   10.20      also have "... = x ^ 2 / 2 * (1 / 2 * (1 / 2) ^ n)"
   10.21 @@ -129,7 +129,7 @@
   10.22      have "suminf (%n. inverse(fact (n+2)) * (x ^ (n+2))) <=
   10.23          suminf (%n. (x^2/2) * ((1/2)^n))"
   10.24        apply (rule summable_le)
   10.25 -      apply (auto simp only: aux1 prems)
   10.26 +      apply (auto simp only: aux1 a b)
   10.27        apply (rule exp_tail_after_first_two_terms_summable)
   10.28        by (rule sums_summable, rule aux2)  
   10.29      also have "... = x^2"
   10.30 @@ -155,14 +155,14 @@
   10.31      apply (rule divide_left_mono)
   10.32      apply (auto simp add: exp_ge_add_one_self_aux)
   10.33      apply (rule add_nonneg_nonneg)
   10.34 -    apply (insert prems, auto)
   10.35 +    using a apply auto
   10.36      apply (rule mult_pos_pos)
   10.37      apply auto
   10.38      apply (rule add_pos_nonneg)
   10.39      apply auto
   10.40      done
   10.41    also from a have "... <= 1 + x"
   10.42 -    by(simp add:field_simps zero_compare_simps)
   10.43 +    by (simp add: field_simps zero_compare_simps)
   10.44    finally show ?thesis .
   10.45  qed
   10.46  
   10.47 @@ -192,14 +192,14 @@
   10.48    finally have "(1 - x) * (1 + x + x ^ 2) <= 1" .
   10.49    moreover have "0 < 1 + x + x^2"
   10.50      apply (rule add_pos_nonneg)
   10.51 -    apply (insert a, auto)
   10.52 +    using a apply auto
   10.53      done
   10.54    ultimately have "1 - x <= 1 / (1 + x + x^2)"
   10.55      by (elim mult_imp_le_div_pos)
   10.56    also have "... <= 1 / exp x"
   10.57      apply (rule divide_left_mono)
   10.58      apply (rule exp_bound, rule a)
   10.59 -    apply (insert prems, auto)
   10.60 +    using a b apply auto
   10.61      apply (rule mult_pos_pos)
   10.62      apply (rule add_pos_nonneg)
   10.63      apply auto
   10.64 @@ -256,10 +256,10 @@
   10.65    also have "- (x / (1 - x)) = -x / (1 - x)"
   10.66      by auto
   10.67    finally have d: "- x / (1 - x) <= ln (1 - x)" .
   10.68 -  have "0 < 1 - x" using prems by simp
   10.69 +  have "0 < 1 - x" using a b by simp
   10.70    hence e: "-x - 2 * x^2 <= - x / (1 - x)"
   10.71 -    using mult_right_le_one_le[of "x*x" "2*x"] prems
   10.72 -    by(simp add:field_simps power2_eq_square)
   10.73 +    using mult_right_le_one_le[of "x*x" "2*x"] a b
   10.74 +    by (simp add:field_simps power2_eq_square)
   10.75    from e d show "- x - 2 * x^2 <= ln (1 - x)"
   10.76      by (rule order_trans)
   10.77  qed
   10.78 @@ -292,7 +292,7 @@
   10.79      "0 <= x ==> x <= 1 ==> abs(ln (1 + x) - x) <= x^2"
   10.80  proof -
   10.81    assume x: "0 <= x"
   10.82 -  assume "x <= 1"
   10.83 +  assume x1: "x <= 1"
   10.84    from x have "ln (1 + x) <= x"
   10.85      by (rule ln_add_one_self_le_self)
   10.86    then have "ln (1 + x) - x <= 0" 
   10.87 @@ -303,7 +303,7 @@
   10.88      by simp
   10.89    also have "... <= x^2"
   10.90    proof -
   10.91 -    from prems have "x - x^2 <= ln (1 + x)"
   10.92 +    from x x1 have "x - x^2 <= ln (1 + x)"
   10.93        by (intro ln_one_plus_pos_lower_bound)
   10.94      thus ?thesis
   10.95        by simp
   10.96 @@ -314,19 +314,19 @@
   10.97  lemma abs_ln_one_plus_x_minus_x_bound_nonpos:
   10.98      "-(1 / 2) <= x ==> x <= 0 ==> abs(ln (1 + x) - x) <= 2 * x^2"
   10.99  proof -
  10.100 -  assume "-(1 / 2) <= x"
  10.101 -  assume "x <= 0"
  10.102 +  assume a: "-(1 / 2) <= x"
  10.103 +  assume b: "x <= 0"
  10.104    have "abs(ln (1 + x) - x) = x - ln(1 - (-x))" 
  10.105      apply (subst abs_of_nonpos)
  10.106      apply simp
  10.107      apply (rule ln_add_one_self_le_self2)
  10.108 -    apply (insert prems, auto)
  10.109 +    using a apply auto
  10.110      done
  10.111    also have "... <= 2 * x^2"
  10.112      apply (subgoal_tac "- (-x) - 2 * (-x)^2 <= ln (1 - (-x))")
  10.113      apply (simp add: algebra_simps)
  10.114      apply (rule ln_one_minus_pos_lower_bound)
  10.115 -    apply (insert prems, auto)
  10.116 +    using a b apply auto
  10.117      done
  10.118    finally show ?thesis .
  10.119  qed
  10.120 @@ -343,9 +343,9 @@
  10.121  
  10.122  lemma ln_x_over_x_mono: "exp 1 <= x ==> x <= y ==> (ln y / y) <= (ln x / x)"  
  10.123  proof -
  10.124 -  assume "exp 1 <= x" and "x <= y"
  10.125 +  assume x: "exp 1 <= x" "x <= y"
  10.126    have a: "0 < x" and b: "0 < y"
  10.127 -    apply (insert prems)
  10.128 +    apply (insert x)
  10.129      apply (subgoal_tac "0 < exp (1::real)")
  10.130      apply arith
  10.131      apply auto
  10.132 @@ -361,12 +361,12 @@
  10.133      done
  10.134    also have "y / x = (x + (y - x)) / x"
  10.135      by simp
  10.136 -  also have "... = 1 + (y - x) / x" using a prems by(simp add:field_simps)
  10.137 +  also have "... = 1 + (y - x) / x" using x a by (simp add: field_simps)
  10.138    also have "x * ln(1 + (y - x) / x) <= x * ((y - x) / x)"
  10.139      apply (rule mult_left_mono)
  10.140      apply (rule ln_add_one_self_le_self)
  10.141      apply (rule divide_nonneg_pos)
  10.142 -    apply (insert prems a, simp_all) 
  10.143 +    using x a apply simp_all
  10.144      done
  10.145    also have "... = y - x" using a by simp
  10.146    also have "... = (y - x) * ln (exp 1)" by simp
  10.147 @@ -375,16 +375,16 @@
  10.148      apply (subst ln_le_cancel_iff)
  10.149      apply force
  10.150      apply (rule a)
  10.151 -    apply (rule prems)
  10.152 -    apply (insert prems, simp)
  10.153 +    apply (rule x)
  10.154 +    using x apply simp
  10.155      done
  10.156    also have "... = y * ln x - x * ln x"
  10.157      by (rule left_diff_distrib)
  10.158    finally have "x * ln y <= y * ln x"
  10.159      by arith
  10.160 -  then have "ln y <= (y * ln x) / x" using a by(simp add:field_simps)
  10.161 -  also have "... = y * (ln x / x)"  by simp
  10.162 -  finally show ?thesis using b by(simp add:field_simps)
  10.163 +  then have "ln y <= (y * ln x) / x" using a by (simp add: field_simps)
  10.164 +  also have "... = y * (ln x / x)" by simp
  10.165 +  finally show ?thesis using b by (simp add: field_simps)
  10.166  qed
  10.167  
  10.168  end
    11.1 --- a/src/HOL/Log.thy	Fri Jan 14 15:43:04 2011 +0100
    11.2 +++ b/src/HOL/Log.thy	Fri Jan 14 15:44:47 2011 +0100
    11.3 @@ -251,10 +251,11 @@
    11.4    apply (erule order_less_imp_le)
    11.5  done
    11.6  
    11.7 -lemma ln_powr_bound2: "1 < x ==> 0 < a ==> (ln x) powr a <= (a powr a) * x"
    11.8 +lemma ln_powr_bound2:
    11.9 +  assumes "1 < x" and "0 < a"
   11.10 +  shows "(ln x) powr a <= (a powr a) * x"
   11.11  proof -
   11.12 -  assume "1 < x" and "0 < a"
   11.13 -  then have "ln x <= (x powr (1 / a)) / (1 / a)"
   11.14 +  from assms have "ln x <= (x powr (1 / a)) / (1 / a)"
   11.15      apply (intro ln_powr_bound)
   11.16      apply (erule order_less_imp_le)
   11.17      apply (rule divide_pos_pos)
   11.18 @@ -264,14 +265,14 @@
   11.19      by simp
   11.20    finally have "(ln x) powr a <= (a * (x powr (1 / a))) powr a"
   11.21      apply (intro powr_mono2)
   11.22 -    apply (rule order_less_imp_le, rule prems)
   11.23 +    apply (rule order_less_imp_le, rule assms)
   11.24      apply (rule ln_gt_zero)
   11.25 -    apply (rule prems)
   11.26 +    apply (rule assms)
   11.27      apply assumption
   11.28      done
   11.29    also have "... = (a powr a) * ((x powr (1 / a)) powr a)"
   11.30      apply (rule powr_mult)
   11.31 -    apply (rule prems)
   11.32 +    apply (rule assms)
   11.33      apply (rule powr_gt_zero)
   11.34      done
   11.35    also have "(x powr (1 / a)) powr a = x powr ((1 / a) * a)"
   11.36 @@ -279,35 +280,37 @@
   11.37    also have "... = x"
   11.38      apply simp
   11.39      apply (subgoal_tac "a ~= 0")
   11.40 -    apply (insert prems, auto)
   11.41 +    using assms apply auto
   11.42      done
   11.43    finally show ?thesis .
   11.44  qed
   11.45  
   11.46 -lemma LIMSEQ_neg_powr: "0 < s ==> (%x. (real x) powr - s) ----> 0"
   11.47 +lemma LIMSEQ_neg_powr:
   11.48 +  assumes s: "0 < s"
   11.49 +  shows "(%x. (real x) powr - s) ----> 0"
   11.50    apply (unfold LIMSEQ_iff)
   11.51    apply clarsimp
   11.52    apply (rule_tac x = "natfloor(r powr (1 / - s)) + 1" in exI)
   11.53    apply clarify
   11.54 -  proof -
   11.55 -    fix r fix n
   11.56 -    assume "0 < s" and "0 < r" and "natfloor (r powr (1 / - s)) + 1 <= n"
   11.57 -    have "r powr (1 / - s) < real(natfloor(r powr (1 / - s))) + 1"
   11.58 -      by (rule real_natfloor_add_one_gt)
   11.59 -    also have "... = real(natfloor(r powr (1 / -s)) + 1)"
   11.60 -      by simp
   11.61 -    also have "... <= real n"
   11.62 -      apply (subst real_of_nat_le_iff)
   11.63 -      apply (rule prems)
   11.64 -      done
   11.65 -    finally have "r powr (1 / - s) < real n".
   11.66 -    then have "real n powr (- s) < (r powr (1 / - s)) powr - s" 
   11.67 -      apply (intro powr_less_mono2_neg)
   11.68 -      apply (auto simp add: prems)
   11.69 -      done
   11.70 -    also have "... = r"
   11.71 -      by (simp add: powr_powr prems less_imp_neq [THEN not_sym])
   11.72 -    finally show "real n powr - s < r" .
   11.73 -  qed
   11.74 +proof -
   11.75 +  fix r fix n
   11.76 +  assume r: "0 < r" and n: "natfloor (r powr (1 / - s)) + 1 <= n"
   11.77 +  have "r powr (1 / - s) < real(natfloor(r powr (1 / - s))) + 1"
   11.78 +    by (rule real_natfloor_add_one_gt)
   11.79 +  also have "... = real(natfloor(r powr (1 / -s)) + 1)"
   11.80 +    by simp
   11.81 +  also have "... <= real n"
   11.82 +    apply (subst real_of_nat_le_iff)
   11.83 +    apply (rule n)
   11.84 +    done
   11.85 +  finally have "r powr (1 / - s) < real n".
   11.86 +  then have "real n powr (- s) < (r powr (1 / - s)) powr - s" 
   11.87 +    apply (intro powr_less_mono2_neg)
   11.88 +    apply (auto simp add: s)
   11.89 +    done
   11.90 +  also have "... = r"
   11.91 +    by (simp add: powr_powr s r less_imp_neq [THEN not_sym])
   11.92 +  finally show "real n powr - s < r" .
   11.93 +qed
   11.94  
   11.95  end
    12.1 --- a/src/HOL/Map.thy	Fri Jan 14 15:43:04 2011 +0100
    12.2 +++ b/src/HOL/Map.thy	Fri Jan 14 15:44:47 2011 +0100
    12.3 @@ -111,7 +111,7 @@
    12.4    assumes "m(a\<mapsto>x) = n(a\<mapsto>y)"
    12.5    shows "x = y"
    12.6  proof -
    12.7 -  from prems have "(m(a\<mapsto>x)) a = (n(a\<mapsto>y)) a" by simp
    12.8 +  from assms have "(m(a\<mapsto>x)) a = (n(a\<mapsto>y)) a" by simp
    12.9    then show ?thesis by simp
   12.10  qed
   12.11  
    13.1 --- a/src/HOL/Matrix/ComputeFloat.thy	Fri Jan 14 15:43:04 2011 +0100
    13.2 +++ b/src/HOL/Matrix/ComputeFloat.thy	Fri Jan 14 15:44:47 2011 +0100
    13.3 @@ -57,7 +57,7 @@
    13.4      show ?case by simp
    13.5    next
    13.6      case (Suc m)
    13.7 -    show ?case by (auto simp add: algebra_simps pow2_add1 prems)
    13.8 +    show ?case by (auto simp add: algebra_simps pow2_add1 1 Suc)
    13.9    qed
   13.10  next
   13.11    case (2 n)
   13.12 @@ -88,7 +88,7 @@
   13.13        apply (subst pow2_neg[of "int m - a + 1"])
   13.14        apply (subst pow2_neg[of "int m + 1"])
   13.15        apply auto
   13.16 -      apply (insert prems)
   13.17 +      apply (insert Suc)
   13.18        apply (auto simp add: algebra_simps)
   13.19        done
   13.20    qed
   13.21 @@ -147,8 +147,8 @@
   13.22    assumes "real_is_int a" "real_is_int b"
   13.23    shows "(int_of_real (a*b)) = (int_of_real a) * (int_of_real b)"
   13.24  proof -
   13.25 -  from prems have a: "?! (a'::int). real a' = a" by (rule_tac real_is_int_rep, auto)
   13.26 -  from prems have b: "?! (b'::int). real b' = b" by (rule_tac real_is_int_rep, auto)
   13.27 +  from assms have a: "?! (a'::int). real a' = a" by (rule_tac real_is_int_rep, auto)
   13.28 +  from assms have b: "?! (b'::int). real b' = b" by (rule_tac real_is_int_rep, auto)
   13.29    from a obtain a'::int where a':"a = real a'" by auto
   13.30    from b obtain b'::int where b':"b = real b'" by auto
   13.31    have r: "real a' * real b' = real (a' * b')" by auto
   13.32 @@ -286,16 +286,16 @@
   13.33        show ?case
   13.34        proof cases
   13.35          assume u: "u \<noteq> 0 \<and> even u"
   13.36 -        with prems have ind: "float (u div 2, v + 1) = float (norm_float (u div 2) (v + 1))" by auto
   13.37 +        with 1 have ind: "float (u div 2, v + 1) = float (norm_float (u div 2) (v + 1))" by auto
   13.38          with u have "float (u,v) = float (u div 2, v+1)" by (simp add: float_transfer_even)
   13.39          then show ?thesis
   13.40            apply (subst norm_float.simps)
   13.41            apply (simp add: ind)
   13.42            done
   13.43        next
   13.44 -        assume "~(u \<noteq> 0 \<and> even u)"
   13.45 -        then show ?thesis
   13.46 -          by (simp add: prems float_def)
   13.47 +        assume nu: "~(u \<noteq> 0 \<and> even u)"
   13.48 +        show ?thesis
   13.49 +          by (simp add: nu float_def)
   13.50        qed
   13.51      qed
   13.52    }
    14.1 --- a/src/HOL/Matrix/LP.thy	Fri Jan 14 15:43:04 2011 +0100
    14.2 +++ b/src/HOL/Matrix/LP.thy	Fri Jan 14 15:44:47 2011 +0100
    14.3 @@ -12,7 +12,7 @@
    14.4    "c <= d"    
    14.5    shows "a <= b + d"
    14.6    apply (rule_tac order_trans[where y = "b+c"])
    14.7 -  apply (simp_all add: prems)
    14.8 +  apply (simp_all add: assms)
    14.9    done
   14.10  
   14.11  lemma linprog_dual_estimate:
   14.12 @@ -26,8 +26,8 @@
   14.13    shows
   14.14    "c * x \<le> y * b' + (y * \<delta>A + abs (y * A' - c') + \<delta>c) * r"
   14.15  proof -
   14.16 -  from prems have 1: "y * b <= y * b'" by (simp add: mult_left_mono)
   14.17 -  from prems have 2: "y * (A * x) <= y * b" by (simp add: mult_left_mono) 
   14.18 +  from assms have 1: "y * b <= y * b'" by (simp add: mult_left_mono)
   14.19 +  from assms have 2: "y * (A * x) <= y * b" by (simp add: mult_left_mono) 
   14.20    have 3: "y * (A * x) = c * x + (y * (A - A') + (y * A' - c') + (c'-c)) * x" by (simp add: algebra_simps)  
   14.21    from 1 2 3 have 4: "c * x + (y * (A - A') + (y * A' - c') + (c'-c)) * x <= y * b'" by simp
   14.22    have 5: "c * x <= y * b' + abs((y * (A - A') + (y * A' - c') + (c'-c)) * x)"
   14.23 @@ -44,23 +44,23 @@
   14.24    have 11: "abs (c'-c) = abs (c-c')" 
   14.25      by (subst 10, subst abs_minus_cancel, simp)
   14.26    have 12: "(abs y * abs (A-A') + abs (y*A'-c') + abs (c'-c)) * abs x <= (abs y * abs (A-A') + abs (y*A'-c') + \<delta>c) * abs x"
   14.27 -    by (simp add: 11 prems mult_right_mono)
   14.28 +    by (simp add: 11 assms mult_right_mono)
   14.29    have 13: "(abs y * abs (A-A') + abs (y*A'-c') + \<delta>c) * abs x <= (abs y * \<delta>A + abs (y*A'-c') + \<delta>c) * abs x"
   14.30 -    by (simp add: prems mult_right_mono mult_left_mono)  
   14.31 +    by (simp add: assms mult_right_mono mult_left_mono)  
   14.32    have r: "(abs y * \<delta>A + abs (y*A'-c') + \<delta>c) * abs x <=  (abs y * \<delta>A + abs (y*A'-c') + \<delta>c) * r"
   14.33      apply (rule mult_left_mono)
   14.34 -    apply (simp add: prems)
   14.35 +    apply (simp add: assms)
   14.36      apply (rule_tac add_mono[of "0::'a" _ "0", simplified])+
   14.37      apply (rule mult_left_mono[of "0" "\<delta>A", simplified])
   14.38      apply (simp_all)
   14.39 -    apply (rule order_trans[where y="abs (A-A')"], simp_all add: prems)
   14.40 -    apply (rule order_trans[where y="abs (c-c')"], simp_all add: prems)
   14.41 +    apply (rule order_trans[where y="abs (A-A')"], simp_all add: assms)
   14.42 +    apply (rule order_trans[where y="abs (c-c')"], simp_all add: assms)
   14.43      done    
   14.44    from 6 7 8 9 12 13 r have 14:" abs((y * (A - A') + (y * A' - c') + (c'-c)) * x) <=(abs y * \<delta>A + abs (y*A'-c') + \<delta>c) * r"     
   14.45      by (simp)
   14.46    show ?thesis
   14.47      apply (rule le_add_right_mono[of _ _ "abs((y * (A - A') + (y * A' - c') + (c'-c)) * x)"])
   14.48 -    apply (simp_all only: 5 14[simplified abs_of_nonneg[of y, simplified prems]])
   14.49 +    apply (simp_all only: 5 14[simplified abs_of_nonneg[of y, simplified assms]])
   14.50      done
   14.51  qed
   14.52  
   14.53 @@ -73,10 +73,10 @@
   14.54    have "0 <= A - A1"    
   14.55    proof -
   14.56      have 1: "A - A1 = A + (- A1)" by simp
   14.57 -    show ?thesis by (simp only: 1 add_right_mono[of A1 A "-A1", simplified, simplified prems])
   14.58 +    show ?thesis by (simp only: 1 add_right_mono[of A1 A "-A1", simplified, simplified assms])
   14.59    qed
   14.60    then have "abs (A-A1) = A-A1" by (rule abs_of_nonneg)
   14.61 -  with prems show "abs (A-A1) <= (A2-A1)" by simp
   14.62 +  with assms show "abs (A-A1) <= (A2-A1)" by simp
   14.63  qed
   14.64  
   14.65  lemma mult_le_prts:
   14.66 @@ -95,31 +95,31 @@
   14.67    then have "a * b = pprt a * pprt b + pprt a * nprt b + nprt a * pprt b + nprt a * nprt b"
   14.68      by (simp add: algebra_simps)
   14.69    moreover have "pprt a * pprt b <= pprt a2 * pprt b2"
   14.70 -    by (simp_all add: prems mult_mono)
   14.71 +    by (simp_all add: assms mult_mono)
   14.72    moreover have "pprt a * nprt b <= pprt a1 * nprt b2"
   14.73    proof -
   14.74      have "pprt a * nprt b <= pprt a * nprt b2"
   14.75 -      by (simp add: mult_left_mono prems)
   14.76 +      by (simp add: mult_left_mono assms)
   14.77      moreover have "pprt a * nprt b2 <= pprt a1 * nprt b2"
   14.78 -      by (simp add: mult_right_mono_neg prems)
   14.79 +      by (simp add: mult_right_mono_neg assms)
   14.80      ultimately show ?thesis
   14.81        by simp
   14.82    qed
   14.83    moreover have "nprt a * pprt b <= nprt a2 * pprt b1"
   14.84    proof - 
   14.85      have "nprt a * pprt b <= nprt a2 * pprt b"
   14.86 -      by (simp add: mult_right_mono prems)
   14.87 +      by (simp add: mult_right_mono assms)
   14.88      moreover have "nprt a2 * pprt b <= nprt a2 * pprt b1"
   14.89 -      by (simp add: mult_left_mono_neg prems)
   14.90 +      by (simp add: mult_left_mono_neg assms)
   14.91      ultimately show ?thesis
   14.92        by simp
   14.93    qed
   14.94    moreover have "nprt a * nprt b <= nprt a1 * nprt b1"
   14.95    proof -
   14.96      have "nprt a * nprt b <= nprt a * nprt b1"
   14.97 -      by (simp add: mult_left_mono_neg prems)
   14.98 +      by (simp add: mult_left_mono_neg assms)
   14.99      moreover have "nprt a * nprt b1 <= nprt a1 * nprt b1"
  14.100 -      by (simp add: mult_right_mono_neg prems)
  14.101 +      by (simp add: mult_right_mono_neg assms)
  14.102      ultimately show ?thesis
  14.103        by simp
  14.104    qed
  14.105 @@ -141,19 +141,19 @@
  14.106    "c * x \<le> y * b + (let s1 = c1 - y * A2; s2 = c2 - y * A1 in pprt s2 * pprt r2 + pprt s1 * nprt r2 + nprt s2 * pprt r1 + nprt s1 * nprt r1)"
  14.107    (is "_ <= _ + ?C")
  14.108  proof -
  14.109 -  from prems have "y * (A * x) <= y * b" by (simp add: mult_left_mono) 
  14.110 +  from assms have "y * (A * x) <= y * b" by (simp add: mult_left_mono) 
  14.111    moreover have "y * (A * x) = c * x + (y * A - c) * x" by (simp add: algebra_simps)  
  14.112    ultimately have "c * x + (y * A - c) * x <= y * b" by simp
  14.113    then have "c * x <= y * b - (y * A - c) * x" by (simp add: le_diff_eq)
  14.114    then have cx: "c * x <= y * b + (c - y * A) * x" by (simp add: algebra_simps)
  14.115    have s2: "c - y * A <= c2 - y * A1"
  14.116 -    by (simp add: diff_minus prems add_mono mult_left_mono)
  14.117 +    by (simp add: diff_minus assms add_mono mult_left_mono)
  14.118    have s1: "c1 - y * A2 <= c - y * A"
  14.119 -    by (simp add: diff_minus prems add_mono mult_left_mono)
  14.120 +    by (simp add: diff_minus assms add_mono mult_left_mono)
  14.121    have prts: "(c - y * A) * x <= ?C"
  14.122      apply (simp add: Let_def)
  14.123      apply (rule mult_le_prts)
  14.124 -    apply (simp_all add: prems s1 s2)
  14.125 +    apply (simp_all add: assms s1 s2)
  14.126      done
  14.127    then have "y * b + (c - y * A) * x <= y * b + ?C"
  14.128      by simp
    15.1 --- a/src/HOL/Nominal/Nominal.thy	Fri Jan 14 15:43:04 2011 +0100
    15.2 +++ b/src/HOL/Nominal/Nominal.thy	Fri Jan 14 15:44:47 2011 +0100
    15.3 @@ -785,7 +785,7 @@
    15.4    hence "((UNIV::'x set) - A) \<noteq> ({}::'x set)" by (force simp only:)
    15.5    then obtain c::"'x" where "c\<in>((UNIV::'x set) - A)" by force
    15.6    then have "c\<notin>A" by simp
    15.7 -  then show ?thesis using prems by simp 
    15.8 +  then show ?thesis ..
    15.9  qed
   15.10  
   15.11  text {* there always exists a fresh name for an object with finite support *}
    16.1 --- a/src/HOL/Power.thy	Fri Jan 14 15:43:04 2011 +0100
    16.2 +++ b/src/HOL/Power.thy	Fri Jan 14 15:44:47 2011 +0100
    16.3 @@ -297,7 +297,7 @@
    16.4    assume "~ a \<le> b"
    16.5    then have "b < a" by (simp only: linorder_not_le)
    16.6    then have "b ^ Suc n < a ^ Suc n"
    16.7 -    by (simp only: prems power_strict_mono)
    16.8 +    by (simp only: assms power_strict_mono)
    16.9    from le and this show False
   16.10      by (simp add: linorder_not_less [symmetric])
   16.11  qed
    17.1 --- a/src/HOL/Predicate.thy	Fri Jan 14 15:43:04 2011 +0100
    17.2 +++ b/src/HOL/Predicate.thy	Fri Jan 14 15:44:47 2011 +0100
    17.3 @@ -93,10 +93,10 @@
    17.4  subsubsection {* Top and bottom elements *}
    17.5  
    17.6  lemma bot1E [no_atp, elim!]: "bot x \<Longrightarrow> P"
    17.7 -  by (simp add: bot_fun_def bot_bool_def)
    17.8 +  by (simp add: bot_fun_def)
    17.9  
   17.10  lemma bot2E [elim!]: "bot x y \<Longrightarrow> P"
   17.11 -  by (simp add: bot_fun_def bot_bool_def)
   17.12 +  by (simp add: bot_fun_def)
   17.13  
   17.14  lemma bot_empty_eq: "bot = (\<lambda>x. x \<in> {})"
   17.15    by (auto simp add: fun_eq_iff)
   17.16 @@ -105,64 +105,64 @@
   17.17    by (auto simp add: fun_eq_iff)
   17.18  
   17.19  lemma top1I [intro!]: "top x"
   17.20 -  by (simp add: top_fun_def top_bool_def)
   17.21 +  by (simp add: top_fun_def)
   17.22  
   17.23  lemma top2I [intro!]: "top x y"
   17.24 -  by (simp add: top_fun_def top_bool_def)
   17.25 +  by (simp add: top_fun_def)
   17.26  
   17.27  
   17.28  subsubsection {* Binary intersection *}
   17.29  
   17.30  lemma inf1I [intro!]: "A x ==> B x ==> inf A B x"
   17.31 -  by (simp add: inf_fun_def inf_bool_def)
   17.32 +  by (simp add: inf_fun_def)
   17.33  
   17.34  lemma inf2I [intro!]: "A x y ==> B x y ==> inf A B x y"
   17.35 -  by (simp add: inf_fun_def inf_bool_def)
   17.36 +  by (simp add: inf_fun_def)
   17.37  
   17.38  lemma inf1E [elim!]: "inf A B x ==> (A x ==> B x ==> P) ==> P"
   17.39 -  by (simp add: inf_fun_def inf_bool_def)
   17.40 +  by (simp add: inf_fun_def)
   17.41  
   17.42  lemma inf2E [elim!]: "inf A B x y ==> (A x y ==> B x y ==> P) ==> P"
   17.43 -  by (simp add: inf_fun_def inf_bool_def)
   17.44 +  by (simp add: inf_fun_def)
   17.45  
   17.46  lemma inf1D1: "inf A B x ==> A x"
   17.47 -  by (simp add: inf_fun_def inf_bool_def)
   17.48 +  by (simp add: inf_fun_def)
   17.49  
   17.50  lemma inf2D1: "inf A B x y ==> A x y"
   17.51 -  by (simp add: inf_fun_def inf_bool_def)
   17.52 +  by (simp add: inf_fun_def)
   17.53  
   17.54  lemma inf1D2: "inf A B x ==> B x"
   17.55 -  by (simp add: inf_fun_def inf_bool_def)
   17.56 +  by (simp add: inf_fun_def)
   17.57  
   17.58  lemma inf2D2: "inf A B x y ==> B x y"
   17.59 -  by (simp add: inf_fun_def inf_bool_def)
   17.60 +  by (simp add: inf_fun_def)
   17.61  
   17.62  lemma inf_Int_eq: "inf (\<lambda>x. x \<in> R) (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<inter> S)"
   17.63 -  by (simp add: inf_fun_def inf_bool_def mem_def)
   17.64 +  by (simp add: inf_fun_def mem_def)
   17.65  
   17.66  lemma inf_Int_eq2 [pred_set_conv]: "inf (\<lambda>x y. (x, y) \<in> R) (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<inter> S)"
   17.67 -  by (simp add: inf_fun_def inf_bool_def mem_def)
   17.68 +  by (simp add: inf_fun_def mem_def)
   17.69  
   17.70  
   17.71  subsubsection {* Binary union *}
   17.72  
   17.73  lemma sup1I1 [elim?]: "A x \<Longrightarrow> sup A B x"
   17.74 -  by (simp add: sup_fun_def sup_bool_def)
   17.75 +  by (simp add: sup_fun_def)
   17.76  
   17.77  lemma sup2I1 [elim?]: "A x y \<Longrightarrow> sup A B x y"
   17.78 -  by (simp add: sup_fun_def sup_bool_def)
   17.79 +  by (simp add: sup_fun_def)
   17.80  
   17.81  lemma sup1I2 [elim?]: "B x \<Longrightarrow> sup A B x"
   17.82 -  by (simp add: sup_fun_def sup_bool_def)
   17.83 +  by (simp add: sup_fun_def)
   17.84  
   17.85  lemma sup2I2 [elim?]: "B x y \<Longrightarrow> sup A B x y"
   17.86 -  by (simp add: sup_fun_def sup_bool_def)
   17.87 +  by (simp add: sup_fun_def)
   17.88  
   17.89  lemma sup1E [elim!]: "sup A B x ==> (A x ==> P) ==> (B x ==> P) ==> P"
   17.90 -  by (simp add: sup_fun_def sup_bool_def) iprover
   17.91 +  by (simp add: sup_fun_def) iprover
   17.92  
   17.93  lemma sup2E [elim!]: "sup A B x y ==> (A x y ==> P) ==> (B x y ==> P) ==> P"
   17.94 -  by (simp add: sup_fun_def sup_bool_def) iprover
   17.95 +  by (simp add: sup_fun_def) iprover
   17.96  
   17.97  text {*
   17.98    \medskip Classical introduction rule: no commitment to @{text A} vs
   17.99 @@ -170,16 +170,16 @@
  17.100  *}
  17.101  
  17.102  lemma sup1CI [intro!]: "(~ B x ==> A x) ==> sup A B x"
  17.103 -  by (auto simp add: sup_fun_def sup_bool_def)
  17.104 +  by (auto simp add: sup_fun_def)
  17.105  
  17.106  lemma sup2CI [intro!]: "(~ B x y ==> A x y) ==> sup A B x y"
  17.107 -  by (auto simp add: sup_fun_def sup_bool_def)
  17.108 +  by (auto simp add: sup_fun_def)
  17.109  
  17.110  lemma sup_Un_eq: "sup (\<lambda>x. x \<in> R) (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<union> S)"
  17.111 -  by (simp add: sup_fun_def sup_bool_def mem_def)
  17.112 +  by (simp add: sup_fun_def mem_def)
  17.113  
  17.114  lemma sup_Un_eq2 [pred_set_conv]: "sup (\<lambda>x y. (x, y) \<in> R) (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<union> S)"
  17.115 -  by (simp add: sup_fun_def sup_bool_def mem_def)
  17.116 +  by (simp add: sup_fun_def mem_def)
  17.117  
  17.118  
  17.119  subsubsection {* Intersections of families *}
  17.120 @@ -257,7 +257,7 @@
  17.121  
  17.122  lemma pred_comp_rel_comp_eq [pred_set_conv]:
  17.123    "((\<lambda>x y. (x, y) \<in> r) OO (\<lambda>x y. (x, y) \<in> s)) = (\<lambda>x y. (x, y) \<in> r O s)"
  17.124 -  by (auto simp add: fun_eq_iff elim: pred_compE)
  17.125 +  by (auto simp add: fun_eq_iff)
  17.126  
  17.127  
  17.128  subsubsection {* Converse *}
  17.129 @@ -292,12 +292,10 @@
  17.130      elim: pred_compE dest: conversepD)
  17.131  
  17.132  lemma converse_meet: "(inf r s)^--1 = inf r^--1 s^--1"
  17.133 -  by (simp add: inf_fun_def inf_bool_def)
  17.134 -    (iprover intro: conversepI ext dest: conversepD)
  17.135 +  by (simp add: inf_fun_def) (iprover intro: conversepI ext dest: conversepD)
  17.136  
  17.137  lemma converse_join: "(sup r s)^--1 = sup r^--1 s^--1"
  17.138 -  by (simp add: sup_fun_def sup_bool_def)
  17.139 -    (iprover intro: conversepI ext dest: conversepD)
  17.140 +  by (simp add: sup_fun_def) (iprover intro: conversepI ext dest: conversepD)
  17.141  
  17.142  lemma conversep_noteq [simp]: "(op ~=)^--1 = op ~="
  17.143    by (auto simp add: fun_eq_iff)
  17.144 @@ -756,7 +754,7 @@
  17.145      apply (rule ext)
  17.146      apply (simp add: unit_eq)
  17.147      done
  17.148 -  from this prems show ?thesis by blast
  17.149 +  from this assms show ?thesis by blast
  17.150  qed
  17.151  
  17.152  lemma unit_pred_cases:
    18.1 --- a/src/HOL/RComplete.thy	Fri Jan 14 15:43:04 2011 +0100
    18.2 +++ b/src/HOL/RComplete.thy	Fri Jan 14 15:44:47 2011 +0100
    18.3 @@ -517,10 +517,10 @@
    18.4    apply simp
    18.5  done
    18.6  
    18.7 -lemma natfloor_div_nat: "1 <= x ==> y > 0 ==>
    18.8 -  natfloor (x / real y) = natfloor x div y"
    18.9 +lemma natfloor_div_nat:
   18.10 +  assumes "1 <= x" and "y > 0"
   18.11 +  shows "natfloor (x / real y) = natfloor x div y"
   18.12  proof -
   18.13 -  assume "1 <= (x::real)" and "(y::nat) > 0"
   18.14    have "natfloor x = (natfloor x) div y * y + (natfloor x) mod y"
   18.15      by simp
   18.16    then have a: "real(natfloor x) = real ((natfloor x) div y) * real y +
   18.17 @@ -535,8 +535,7 @@
   18.18      by simp
   18.19    also have "... = real((natfloor x) div y) + real((natfloor x) mod y) /
   18.20      real y + (x - real(natfloor x)) / real y"
   18.21 -    by (auto simp add: algebra_simps add_divide_distrib
   18.22 -      diff_divide_distrib prems)
   18.23 +    by (auto simp add: algebra_simps add_divide_distrib diff_divide_distrib)
   18.24    finally have "natfloor (x / real y) = natfloor(...)" by simp
   18.25    also have "... = natfloor(real((natfloor x) mod y) /
   18.26      real y + (x - real(natfloor x)) / real y + real((natfloor x) div y))"
   18.27 @@ -547,11 +546,11 @@
   18.28      apply (rule add_nonneg_nonneg)
   18.29      apply (rule divide_nonneg_pos)
   18.30      apply simp
   18.31 -    apply (simp add: prems)
   18.32 +    apply (simp add: assms)
   18.33      apply (rule divide_nonneg_pos)
   18.34      apply (simp add: algebra_simps)
   18.35      apply (rule real_natfloor_le)
   18.36 -    apply (insert prems, auto)
   18.37 +    using assms apply auto
   18.38      done
   18.39    also have "natfloor(real((natfloor x) mod y) /
   18.40      real y + (x - real(natfloor x)) / real y) = 0"
   18.41 @@ -560,13 +559,13 @@
   18.42      apply (rule add_nonneg_nonneg)
   18.43      apply (rule divide_nonneg_pos)
   18.44      apply force
   18.45 -    apply (force simp add: prems)
   18.46 +    apply (force simp add: assms)
   18.47      apply (rule divide_nonneg_pos)
   18.48      apply (simp add: algebra_simps)
   18.49      apply (rule real_natfloor_le)
   18.50 -    apply (auto simp add: prems)
   18.51 -    apply (insert prems, arith)
   18.52 -    apply (simp add: add_divide_distrib [THEN sym])
   18.53 +    apply (auto simp add: assms)
   18.54 +    using assms apply arith
   18.55 +    using assms apply (simp add: add_divide_distrib [THEN sym])
   18.56      apply (subgoal_tac "real y = real y - 1 + 1")
   18.57      apply (erule ssubst)
   18.58      apply (rule add_le_less_mono)
    19.1 --- a/src/HOL/RealDef.thy	Fri Jan 14 15:43:04 2011 +0100
    19.2 +++ b/src/HOL/RealDef.thy	Fri Jan 14 15:44:47 2011 +0100
    19.3 @@ -1200,7 +1200,7 @@
    19.4  lemma real_of_int_div_aux: "d ~= 0 ==> (real (x::int)) / (real d) = 
    19.5      real (x div d) + (real (x mod d)) / (real d)"
    19.6  proof -
    19.7 -  assume "d ~= 0"
    19.8 +  assume d: "d ~= 0"
    19.9    have "x = (x div d) * d + x mod d"
   19.10      by auto
   19.11    then have "real x = real (x div d) * real d + real(x mod d)"
   19.12 @@ -1208,7 +1208,7 @@
   19.13    then have "real x / real d = ... / real d"
   19.14      by simp
   19.15    then show ?thesis
   19.16 -    by (auto simp add: add_divide_distrib algebra_simps prems)
   19.17 +    by (auto simp add: add_divide_distrib algebra_simps d)
   19.18  qed
   19.19  
   19.20  lemma real_of_int_div: "(d::int) ~= 0 ==> d dvd n ==>
   19.21 @@ -1353,7 +1353,7 @@
   19.22  lemma real_of_nat_div_aux: "0 < d ==> (real (x::nat)) / (real d) = 
   19.23      real (x div d) + (real (x mod d)) / (real d)"
   19.24  proof -
   19.25 -  assume "0 < d"
   19.26 +  assume d: "0 < d"
   19.27    have "x = (x div d) * d + x mod d"
   19.28      by auto
   19.29    then have "real x = real (x div d) * real d + real(x mod d)"
   19.30 @@ -1361,7 +1361,7 @@
   19.31    then have "real x / real d = \<dots> / real d"
   19.32      by simp
   19.33    then show ?thesis
   19.34 -    by (auto simp add: add_divide_distrib algebra_simps prems)
   19.35 +    by (auto simp add: add_divide_distrib algebra_simps d)
   19.36  qed
   19.37  
   19.38  lemma real_of_nat_div: "0 < (d::nat) ==> d dvd n ==>
    20.1 --- a/src/HOL/Transcendental.thy	Fri Jan 14 15:43:04 2011 +0100
    20.2 +++ b/src/HOL/Transcendental.thy	Fri Jan 14 15:44:47 2011 +0100
    20.3 @@ -164,7 +164,7 @@
    20.4    { 
    20.5      have "?s 0 = 0" by auto
    20.6      have Suc_m1: "\<And> n. Suc n - 1 = n" by auto
    20.7 -    { fix B T E have "(if \<not> B then T else E) = (if B then E else T)" by auto } note if_eq = this
    20.8 +    have if_eq: "\<And>B T E. (if \<not> B then T else E) = (if B then E else T)" by auto
    20.9  
   20.10      have "?s sums y" using sums_if'[OF `f sums y`] .
   20.11      from this[unfolded sums_def, THEN LIMSEQ_Suc] 
   20.12 @@ -348,7 +348,7 @@
   20.13    fixes z :: "'a :: {monoid_mult,comm_ring}" shows
   20.14    "(\<Sum>p=0..<m. (((z + h) ^ (m - p)) * (z ^ p)) - (z ^ m)) =  
   20.15     (\<Sum>p=0..<m. (z ^ p) * (((z + h) ^ (m - p)) - (z ^ (m - p))))"
   20.16 -by(auto simp add: algebra_simps power_add [symmetric] cong: strong_setsum_cong)
   20.17 +by(auto simp add: algebra_simps power_add [symmetric])
   20.18  
   20.19  lemma sumr_diff_mult_const2:
   20.20    "setsum f {0..<n} - of_nat n * (r::'a::ring_1) = (\<Sum>i = 0..<n. f i - r)"
   20.21 @@ -1849,7 +1849,7 @@
   20.22  lemma sin_less_zero: 
   20.23    assumes lb: "- pi/2 < x" and "x < 0" shows "sin x < 0"
   20.24  proof -
   20.25 -  have "0 < sin (- x)" using prems by (simp only: sin_gt_zero2) 
   20.26 +  have "0 < sin (- x)" using assms by (simp only: sin_gt_zero2) 
   20.27    thus ?thesis by simp
   20.28  qed
   20.29  
   20.30 @@ -2107,7 +2107,7 @@
   20.31  lemma tan_less_zero: 
   20.32    assumes lb: "- pi/2 < x" and "x < 0" shows "tan x < 0"
   20.33  proof -
   20.34 -  have "0 < tan (- x)" using prems by (simp only: tan_gt_zero) 
   20.35 +  have "0 < tan (- x)" using assms by (simp only: tan_gt_zero) 
   20.36    thus ?thesis by simp
   20.37  qed
   20.38  
    21.1 --- a/src/HOL/Word/Word.thy	Fri Jan 14 15:43:04 2011 +0100
    21.2 +++ b/src/HOL/Word/Word.thy	Fri Jan 14 15:44:47 2011 +0100
    21.3 @@ -2171,7 +2171,7 @@
    21.4  
    21.5  lemma word_of_int_power_hom: 
    21.6    "word_of_int a ^ n = (word_of_int (a ^ n) :: 'a :: len word)"
    21.7 -  by (induct n) (simp_all add : word_of_int_hom_syms power_Suc)
    21.8 +  by (induct n) (simp_all add: word_of_int_hom_syms)
    21.9  
   21.10  lemma word_arith_power_alt: 
   21.11    "a ^ n = (word_of_int (uint a ^ n) :: 'a :: len word)"
   21.12 @@ -2367,7 +2367,7 @@
   21.13    using word_of_int_Ex [where x=x] 
   21.14          word_of_int_Ex [where x=y] 
   21.15          word_of_int_Ex [where x=z]   
   21.16 -  by (auto simp: bwsimps bbw_ao_dist simp del: bin_ops_comm)
   21.17 +  by (auto simp: bwsimps bbw_ao_dist)
   21.18  
   21.19  lemma word_oa_dist:
   21.20    fixes x :: "'a::len0 word"
   21.21 @@ -2375,7 +2375,7 @@
   21.22    using word_of_int_Ex [where x=x] 
   21.23          word_of_int_Ex [where x=y] 
   21.24          word_of_int_Ex [where x=z]   
   21.25 -  by (auto simp: bwsimps bbw_oa_dist simp del: bin_ops_comm)
   21.26 +  by (auto simp: bwsimps bbw_oa_dist)
   21.27  
   21.28  lemma word_add_not [simp]: 
   21.29    fixes x :: "'a::len0 word"
   21.30 @@ -2571,7 +2571,7 @@
   21.31    fixes w :: "'a::len0 word"
   21.32    assumes "m ~= n"
   21.33    shows "set_bit (set_bit w m x) n y = set_bit (set_bit w n y) m x" 
   21.34 -  by (rule word_eqI) (clarsimp simp add : test_bit_set_gen word_size prems)
   21.35 +  by (rule word_eqI) (clarsimp simp add: test_bit_set_gen word_size assms)
   21.36      
   21.37  lemma test_bit_no': 
   21.38    fixes w :: "'a::len0 word"
   21.39 @@ -2623,7 +2623,7 @@
   21.40    done
   21.41  
   21.42  lemma word_msb_n1: "msb (-1::'a::len word)"
   21.43 -  unfolding word_msb_alt word_msb_alt to_bl_n1 by simp
   21.44 +  unfolding word_msb_alt to_bl_n1 by simp
   21.45  
   21.46  declare word_set_set_same [simp] word_set_nth [simp]
   21.47    test_bit_no [simp] word_set_no [simp] nth_0 [simp]
   21.48 @@ -3047,7 +3047,7 @@
   21.49  
   21.50  lemma shiftl_t2n: "shiftl (w :: 'a :: len word) n = 2 ^ n * w"
   21.51    unfolding shiftl_def 
   21.52 -  by (induct n) (auto simp: shiftl1_2t power_Suc)
   21.53 +  by (induct n) (auto simp: shiftl1_2t)
   21.54  
   21.55  lemma shiftr1_bintr [simp]:
   21.56    "(shiftr1 (number_of w) :: 'a :: len0 word) = 
   21.57 @@ -3940,12 +3940,12 @@
   21.58       apply (clarsimp simp: word_size)+
   21.59    apply (rule trans)
   21.60    apply (rule test_bit_rcat [OF refl refl])
   21.61 -  apply (simp add : word_size msrevs)
   21.62 +  apply (simp add: word_size msrevs)
   21.63    apply (subst nth_rev)
   21.64     apply arith
   21.65 -  apply (simp add : le0 [THEN [2] xtr7, THEN diff_Suc_less])
   21.66 +  apply (simp add: le0 [THEN [2] xtr7, THEN diff_Suc_less])
   21.67    apply safe
   21.68 -  apply (simp add : diff_mult_distrib)
   21.69 +  apply (simp add: diff_mult_distrib)
   21.70    apply (rule mpl_lem)
   21.71    apply (cases "size ws")
   21.72     apply simp_all