# HG changeset patch
# User huffman
# Date 1315958853 25200
# Node ID 58eef4843641234fb6b36b22a53590f5ca3cd627
# Parent  4657b4c111382f412684aa9b23a66cd793f452b4
tuned proofs

diff -r 4657b4c11138 -r 58eef4843641 src/HOL/Big_Operators.thy
--- a/src/HOL/Big_Operators.thy	Tue Sep 13 08:21:51 2011 -0700
+++ b/src/HOL/Big_Operators.thy	Tue Sep 13 17:07:33 2011 -0700
@@ -1394,7 +1394,7 @@
   shows "inf (\<Squnion>\<^bsub>fin\<^esub>A) (\<Squnion>\<^bsub>fin\<^esub>B) = \<Squnion>\<^bsub>fin\<^esub>{inf a b|a b. a \<in> A \<and> b \<in> B}"
 using A proof (induct rule: finite_ne_induct)
   case singleton thus ?case
-    by(simp add: inf_Sup1_distrib [OF B] fold1_singleton_def [OF Sup_fin_def])
+    by(simp add: inf_Sup1_distrib [OF B])
 next
   case (insert x A)
   have finB: "finite {inf x b |b. b \<in> B}"
@@ -1608,11 +1608,7 @@
 lemma Max_ge [simp]:
   assumes "finite A" and "x \<in> A"
   shows "x \<le> Max A"
-proof -
-  interpret semilattice_inf max "op \<ge>" "op >"
-    by (rule max_lattice)
-  from assms show ?thesis by (simp add: Max_def fold1_belowI)
-qed
+  by (simp add: Max_def semilattice_inf.fold1_belowI [OF max_lattice] assms)
 
 lemma Min_ge_iff [simp, no_atp]:
   assumes "finite A" and "A \<noteq> {}"
@@ -1622,11 +1618,7 @@
 lemma Max_le_iff [simp, no_atp]:
   assumes "finite A" and "A \<noteq> {}"
   shows "Max A \<le> x \<longleftrightarrow> (\<forall>a\<in>A. a \<le> x)"
-proof -
-  interpret semilattice_inf max "op \<ge>" "op >"
-    by (rule max_lattice)
-  from assms show ?thesis by (simp add: Max_def below_fold1_iff)
-qed
+  by (simp add: Max_def semilattice_inf.below_fold1_iff [OF max_lattice] assms)
 
 lemma Min_gr_iff [simp, no_atp]:
   assumes "finite A" and "A \<noteq> {}"
@@ -1636,12 +1628,8 @@
 lemma Max_less_iff [simp, no_atp]:
   assumes "finite A" and "A \<noteq> {}"
   shows "Max A < x \<longleftrightarrow> (\<forall>a\<in>A. a < x)"
-proof -
-  interpret dual: linorder "op \<ge>" "op >"
-    by (rule dual_linorder)
-  from assms show ?thesis
-    by (simp add: Max_def dual.strict_below_fold1_iff [folded dual.dual_max])
-qed
+  by (simp add: Max_def linorder.dual_max [OF dual_linorder]
+    linorder.strict_below_fold1_iff [OF dual_linorder] assms)
 
 lemma Min_le_iff [no_atp]:
   assumes "finite A" and "A \<noteq> {}"
@@ -1651,12 +1639,8 @@
 lemma Max_ge_iff [no_atp]:
   assumes "finite A" and "A \<noteq> {}"
   shows "x \<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<le> a)"
-proof -
-  interpret dual: linorder "op \<ge>" "op >"
-    by (rule dual_linorder)
-  from assms show ?thesis
-    by (simp add: Max_def dual.fold1_below_iff [folded dual.dual_max])
-qed
+  by (simp add: Max_def linorder.dual_max [OF dual_linorder]
+    linorder.fold1_below_iff [OF dual_linorder] assms)
 
 lemma Min_less_iff [no_atp]:
   assumes "finite A" and "A \<noteq> {}"
@@ -1666,12 +1650,8 @@
 lemma Max_gr_iff [no_atp]:
   assumes "finite A" and "A \<noteq> {}"
   shows "x < Max A \<longleftrightarrow> (\<exists>a\<in>A. x < a)"
-proof -
-  interpret dual: linorder "op \<ge>" "op >"
-    by (rule dual_linorder)
-  from assms show ?thesis
-    by (simp add: Max_def dual.fold1_strict_below_iff [folded dual.dual_max])
-qed
+  by (simp add: Max_def linorder.dual_max [OF dual_linorder]
+    linorder.fold1_strict_below_iff [OF dual_linorder] assms)
 
 lemma Min_eqI:
   assumes "finite A"
@@ -1705,12 +1685,8 @@
 lemma Max_mono:
   assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
   shows "Max M \<le> Max N"
-proof -
-  interpret dual: linorder "op \<ge>" "op >"
-    by (rule dual_linorder)
-  from assms show ?thesis
-    by (simp add: Max_def dual.fold1_antimono [folded dual.dual_max])
-qed
+  by (simp add: Max_def linorder.dual_max [OF dual_linorder]
+    linorder.fold1_antimono [OF dual_linorder] assms)
 
 lemma finite_linorder_max_induct[consumes 1, case_names empty insert]:
  assumes fin: "finite A"
diff -r 4657b4c11138 -r 58eef4843641 src/HOL/Complete_Lattices.thy
--- a/src/HOL/Complete_Lattices.thy	Tue Sep 13 08:21:51 2011 -0700
+++ b/src/HOL/Complete_Lattices.thy	Tue Sep 13 17:07:33 2011 -0700
@@ -84,23 +84,13 @@
 
 lemma INF_foundation_dual [no_atp]:
   "complete_lattice.SUPR Inf = INFI"
-proof (rule ext)+
-  interpret dual: complete_lattice Sup Inf sup "op \<ge>" "op >" inf \<top> \<bottom>
-    by (fact dual_complete_lattice)
-  fix f :: "'b \<Rightarrow> 'a" and A
-  show "complete_lattice.SUPR Inf A f = (\<Sqinter>a\<in>A. f a)"
-    by (simp only: dual.SUP_def INF_def)
-qed
+  by (simp add: fun_eq_iff INF_def
+    complete_lattice.SUP_def [OF dual_complete_lattice])
 
 lemma SUP_foundation_dual [no_atp]:
   "complete_lattice.INFI Sup = SUPR"
-proof (rule ext)+
-  interpret dual: complete_lattice Sup Inf sup "op \<ge>" "op >" inf \<top> \<bottom>
-    by (fact dual_complete_lattice)
-  fix f :: "'b \<Rightarrow> 'a" and A
-  show "complete_lattice.INFI Sup A f = (\<Squnion>a\<in>A. f a)"
-    by (simp only: dual.INF_def SUP_def)
-qed
+  by (simp add: fun_eq_iff SUP_def
+    complete_lattice.INF_def [OF dual_complete_lattice])
 
 lemma INF_lower: "i \<in> A \<Longrightarrow> (\<Sqinter>i\<in>A. f i) \<sqsubseteq> f i"
   by (auto simp add: INF_def intro: Inf_lower)
@@ -330,10 +320,10 @@
   by (auto intro: antisym SUP_upper SUP_least)
 
 lemma INF_top [simp]: "(\<Sqinter>x\<in>A. \<top>) = \<top>"
-  by (cases "A = {}") (simp_all add: INF_empty)
+  by (cases "A = {}") simp_all
 
 lemma SUP_bot [simp]: "(\<Squnion>x\<in>A. \<bottom>) = \<bottom>"
-  by (cases "A = {}") (simp_all add: SUP_empty)
+  by (cases "A = {}") simp_all
 
 lemma INF_commute: "(\<Sqinter>i\<in>A. \<Sqinter>j\<in>B. f i j) = (\<Sqinter>j\<in>B. \<Sqinter>i\<in>A. f i j)"
   by (iprover intro: INF_lower INF_greatest order_trans antisym)
@@ -359,11 +349,11 @@
 
 lemma INF_constant:
   "(\<Sqinter>y\<in>A. c) = (if A = {} then \<top> else c)"
-  by (simp add: INF_empty)
+  by simp
 
 lemma SUP_constant:
   "(\<Squnion>y\<in>A. c) = (if A = {} then \<bottom> else c)"
-  by (simp add: SUP_empty)
+  by simp
 
 lemma less_INF_D:
   assumes "y < (\<Sqinter>i\<in>A. f i)" "i \<in> A" shows "y < f i"
@@ -385,11 +375,11 @@
 
 lemma INF_UNIV_bool_expand:
   "(\<Sqinter>b. A b) = A True \<sqinter> A False"
-  by (simp add: UNIV_bool INF_empty INF_insert inf_commute)
+  by (simp add: UNIV_bool INF_insert inf_commute)
 
 lemma SUP_UNIV_bool_expand:
   "(\<Squnion>b. A b) = A True \<squnion> A False"
-  by (simp add: UNIV_bool SUP_empty SUP_insert sup_commute)
+  by (simp add: UNIV_bool SUP_insert sup_commute)
 
 end
 
diff -r 4657b4c11138 -r 58eef4843641 src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Tue Sep 13 08:21:51 2011 -0700
+++ b/src/HOL/Deriv.thy	Tue Sep 13 17:07:33 2011 -0700
@@ -451,10 +451,11 @@
          \<forall>n. f(n) \<le> g(n) |]
       ==> Bseq (f :: nat \<Rightarrow> real)"
 apply (rule_tac k = "f 0" and K = "g 0" in BseqI2, rule allI)
+apply (rule conjI)
 apply (induct_tac "n")
 apply (auto intro: order_trans)
-apply (rule_tac y = "g (Suc na)" in order_trans)
-apply (induct_tac [2] "na")
+apply (rule_tac y = "g n" in order_trans)
+apply (induct_tac [2] "n")
 apply (auto intro: order_trans)
 done
 
@@ -470,17 +471,7 @@
 lemma f_inc_imp_le_lim:
   fixes f :: "nat \<Rightarrow> real"
   shows "\<lbrakk>\<forall>n. f n \<le> f (Suc n); convergent f\<rbrakk> \<Longrightarrow> f n \<le> lim f"
-apply (rule linorder_not_less [THEN iffD1])
-apply (auto simp add: convergent_LIMSEQ_iff LIMSEQ_iff monoseq_Suc)
-apply (drule_tac x = "f n - lim f" in spec, clarsimp)
-apply (drule_tac P = "%na. no\<le>na --> ?Q na" and x = "no + n" in spec, auto)
-apply (subgoal_tac "lim f \<le> f (no + n) ")
-apply (drule_tac no=no and m=n in lemma_f_mono_add)
-apply (auto simp add: add_commute)
-apply (induct_tac "no")
-apply simp
-apply (auto intro: order_trans simp add: diff_minus abs_if)
-done
+  by (rule incseq_le, simp add: incseq_SucI, simp add: convergent_LIMSEQ_iff)
 
 lemma lim_uminus:
   fixes g :: "nat \<Rightarrow> 'a::real_normed_vector"
@@ -492,10 +483,7 @@
 lemma g_dec_imp_lim_le:
   fixes g :: "nat \<Rightarrow> real"
   shows "\<lbrakk>\<forall>n. g (Suc n) \<le> g(n); convergent g\<rbrakk> \<Longrightarrow> lim g \<le> g n"
-apply (subgoal_tac "- (g n) \<le> - (lim g) ")
-apply (cut_tac [2] f = "%x. - (g x)" in f_inc_imp_le_lim)
-apply (auto simp add: lim_uminus convergent_minus_iff [symmetric])
-done
+  by (rule decseq_le, simp add: decseq_SucI, simp add: convergent_LIMSEQ_iff)
 
 lemma lemma_nest: "[| \<forall>n. f(n) \<le> f(Suc n);
          \<forall>n. g(Suc n) \<le> g(n);
@@ -938,7 +926,7 @@
 lemma lemma_interval: "[| a < x;  x < b |] ==>
         \<exists>d::real. 0 < d &  (\<forall>y. \<bar>x-y\<bar> < d --> a \<le> y & y \<le> b)"
 apply (drule lemma_interval_lt, auto)
-apply (auto intro!: exI)
+apply force
 done
 
 text{*Rolle's Theorem.
diff -r 4657b4c11138 -r 58eef4843641 src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Tue Sep 13 08:21:51 2011 -0700
+++ b/src/HOL/Fields.thy	Tue Sep 13 17:07:33 2011 -0700
@@ -270,7 +270,11 @@
 lemma times_divide_eq_left [simp]: "(b / c) * a = (b * a) / c"
   by (simp add: divide_inverse mult_ac)
 
-text {* These are later declared as simp rules. *}
+text{*It's not obvious whether @{text times_divide_eq} should be
+  simprules or not. Their effect is to gather terms into one big
+  fraction, like a*b*c / x*y*z. The rationale for that is unclear, but
+  many proofs seem to need them.*}
+
 lemmas times_divide_eq [no_atp] = times_divide_eq_right times_divide_eq_left
 
 lemma add_frac_eq:
@@ -777,15 +781,15 @@
       have the same sign*}
 lemma divide_strict_left_mono:
   "[|b < a; 0 < c; 0 < a*b|] ==> c / a < c / b"
-by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono)
+  by (auto simp: field_simps zero_less_mult_iff mult_strict_right_mono)
 
 lemma divide_left_mono:
   "[|b \<le> a; 0 \<le> c; 0 < a*b|] ==> c / a \<le> c / b"
-by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_right_mono)
+  by (auto simp: field_simps zero_less_mult_iff mult_right_mono)
 
 lemma divide_strict_left_mono_neg:
   "[|a < b; c < 0; 0 < a*b|] ==> c / a < c / b"
-by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono_neg)
+  by (auto simp: field_simps zero_less_mult_iff mult_strict_right_mono_neg)
 
 lemma mult_imp_div_pos_le: "0 < y ==> x <= z * y ==>
     x / y <= z"
@@ -832,11 +836,6 @@
   apply simp_all
 done
 
-text{*It's not obvious whether these should be simprules or not. 
-  Their effect is to gather terms into one big fraction, like
-  a*b*c / x*y*z. The rationale for that is unclear, but many proofs 
-  seem to need them.*}
-
 lemma less_half_sum: "a < b ==> a < (a+b) / (1+1)"
 by (simp add: field_simps zero_less_two)
 
diff -r 4657b4c11138 -r 58eef4843641 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Tue Sep 13 08:21:51 2011 -0700
+++ b/src/HOL/Fun.thy	Tue Sep 13 17:07:33 2011 -0700
@@ -610,7 +610,7 @@
 by auto
 
 lemma fun_upd_comp: "f \<circ> (g(x := y)) = (f \<circ> g)(x := f y)"
-by (auto intro: ext)
+  by auto
 
 lemma UNION_fun_upd:
   "UNION J (A(i:=B)) = (UNION (J-{i}) A \<union> (if i\<in>J then B else {}))"
diff -r 4657b4c11138 -r 58eef4843641 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue Sep 13 08:21:51 2011 -0700
+++ b/src/HOL/HOL.thy	Tue Sep 13 17:07:33 2011 -0700
@@ -1635,7 +1635,7 @@
   apply (rule iffI)
   apply (rule_tac a = "%x. THE y. P x y" in ex1I)
   apply (fast dest!: theI')
-  apply (fast intro: ext the1_equality [symmetric])
+  apply (fast intro: the1_equality [symmetric])
   apply (erule ex1E)
   apply (rule allI)
   apply (rule ex1I)
diff -r 4657b4c11138 -r 58eef4843641 src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Tue Sep 13 08:21:51 2011 -0700
+++ b/src/HOL/Hilbert_Choice.thy	Tue Sep 13 17:07:33 2011 -0700
@@ -123,7 +123,7 @@
 by (simp add:inv_into_f_eq)
 
 lemma inj_imp_inv_eq: "[| inj f; ALL x. f(g x) = x |] ==> inv f = g"
-by (blast intro: ext inv_into_f_eq)
+  by (blast intro: inv_into_f_eq)
 
 text{*But is it useful?*}
 lemma inj_transfer:
@@ -286,7 +286,7 @@
   hence "?f'' a = a'"
     using `a \<in> A` 1 3 by (auto simp add: f_inv_into_f bij_betw_def)
   moreover have "f a = a'" using assms 2 3
-    by (auto simp add: inv_into_f_f bij_betw_def)
+    by (auto simp add: bij_betw_def)
   ultimately show "?f'' a = f a" by simp
 qed
 
diff -r 4657b4c11138 -r 58eef4843641 src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Tue Sep 13 08:21:51 2011 -0700
+++ b/src/HOL/Lattices.thy	Tue Sep 13 17:07:33 2011 -0700
@@ -180,8 +180,8 @@
 lemma inf_left_commute: "x \<sqinter> (y \<sqinter> z) = y \<sqinter> (x \<sqinter> z)"
   by (fact inf.left_commute)
 
-lemma inf_idem [simp]: "x \<sqinter> x = x"
-  by (fact inf.idem)
+lemma inf_idem: "x \<sqinter> x = x"
+  by (fact inf.idem) (* already simp *)
 
 lemma inf_left_idem [simp]: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
   by (fact inf.left_idem)
@@ -219,8 +219,8 @@
 lemma sup_left_commute: "x \<squnion> (y \<squnion> z) = y \<squnion> (x \<squnion> z)"
   by (fact sup.left_commute)
 
-lemma sup_idem [simp]: "x \<squnion> x = x"
-  by (fact sup.idem)
+lemma sup_idem: "x \<squnion> x = x"
+  by (fact sup.idem) (* already simp *)
 
 lemma sup_left_idem [simp]: "x \<squnion> (x \<squnion> y) = x \<squnion> y"
   by (fact sup.left_idem)
@@ -311,23 +311,13 @@
 
 lemma less_supI1:
   "x \<sqsubset> a \<Longrightarrow> x \<sqsubset> a \<squnion> b"
-proof -
-  interpret dual: semilattice_inf sup "op \<ge>" "op >"
-    by (fact dual_semilattice)
-  assume "x \<sqsubset> a"
-  then show "x \<sqsubset> a \<squnion> b"
-    by (fact dual.less_infI1)
-qed
+  using dual_semilattice
+  by (rule semilattice_inf.less_infI1)
 
 lemma less_supI2:
   "x \<sqsubset> b \<Longrightarrow> x \<sqsubset> a \<squnion> b"
-proof -
-  interpret dual: semilattice_inf sup "op \<ge>" "op >"
-    by (fact dual_semilattice)
-  assume "x \<sqsubset> b"
-  then show "x \<sqsubset> a \<squnion> b"
-    by (fact dual.less_infI2)
-qed
+  using dual_semilattice
+  by (rule semilattice_inf.less_infI2)
 
 end
 
@@ -341,16 +331,16 @@
 begin
 
 lemma sup_inf_distrib2:
- "(y \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)"
-by(simp add: inf_sup_aci sup_inf_distrib1)
+  "(y \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)"
+  by (simp add: sup_commute sup_inf_distrib1)
 
 lemma inf_sup_distrib1:
- "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
-by(rule distrib_imp2[OF sup_inf_distrib1])
+  "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
+  by (rule distrib_imp2 [OF sup_inf_distrib1])
 
 lemma inf_sup_distrib2:
- "(y \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (z \<sqinter> x)"
-by(simp add: inf_sup_aci inf_sup_distrib1)
+  "(y \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (z \<sqinter> x)"
+  by (simp add: inf_commute inf_sup_distrib1)
 
 lemma dual_distrib_lattice:
   "class.distrib_lattice sup (op \<ge>) (op >) inf"
@@ -510,11 +500,8 @@
 
 lemma compl_sup [simp]:
   "- (x \<squnion> y) = - x \<sqinter> - y"
-proof -
-  interpret boolean_algebra "\<lambda>x y. x \<squnion> - y" uminus sup greater_eq greater inf \<top> \<bottom>
-    by (rule dual_boolean_algebra)
-  then show ?thesis by simp
-qed
+  using dual_boolean_algebra
+  by (rule boolean_algebra.compl_inf)
 
 lemma compl_mono:
   "x \<sqsubseteq> y \<Longrightarrow> - y \<sqsubseteq> - x"
diff -r 4657b4c11138 -r 58eef4843641 src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Sep 13 08:21:51 2011 -0700
+++ b/src/HOL/List.thy	Tue Sep 13 17:07:33 2011 -0700
@@ -1176,7 +1176,7 @@
     have "length (filter p (x # xs)) = Suc(card ?S)"
       using Cons `p x` by simp
     also have "\<dots> = Suc(card(Suc ` ?S))" using fin
-      by (simp add: card_image inj_Suc)
+      by (simp add: card_image)
     also have "\<dots> = card ?S'" using eq fin
       by (simp add:card_insert_if) (simp add:image_def)
     finally show ?thesis .
@@ -1187,7 +1187,7 @@
     have "length (filter p (x # xs)) = card ?S"
       using Cons `\<not> p x` by simp
     also have "\<dots> = card(Suc ` ?S)" using fin
-      by (simp add: card_image inj_Suc)
+      by (simp add: card_image)
     also have "\<dots> = card ?S'" using eq fin
       by (simp add:card_insert_if)
     finally show ?thesis .
@@ -1529,10 +1529,10 @@
 by (induct xs) auto
 
 lemma last_ConsL: "xs = [] \<Longrightarrow> last(x#xs) = x"
-by(simp add:last.simps)
+  by simp
 
 lemma last_ConsR: "xs \<noteq> [] \<Longrightarrow> last(x#xs) = last xs"
-by(simp add:last.simps)
+  by simp
 
 lemma last_append: "last(xs @ ys) = (if ys = [] then last xs else last ys)"
 by (induct xs) (auto)
@@ -2627,7 +2627,7 @@
 lemma nth_map_upt: "i < n-m ==> (map f [m..<n]) ! i = f(m+i)"
 apply (induct n m  arbitrary: i rule: diff_induct)
 prefer 3 apply (subst map_Suc_upt[symmetric])
-apply (auto simp add: less_diff_conv nth_upt)
+apply (auto simp add: less_diff_conv)
 done
 
 lemma nth_take_lemma:
@@ -2647,9 +2647,7 @@
 
 lemma nth_equalityI:
  "[| length xs = length ys; ALL i < length xs. xs!i = ys!i |] ==> xs = ys"
-apply (frule nth_take_lemma [OF le_refl eq_imp_le])
-apply (simp_all add: take_all)
-done
+  by (frule nth_take_lemma [OF le_refl eq_imp_le]) simp_all
 
 lemma map_nth:
   "map (\<lambda>i. xs ! i) [0..<length xs] = xs"
@@ -2666,7 +2664,7 @@
 lemma take_equalityI: "(\<forall>i. take i xs = take i ys) ==> xs = ys"
 -- {* The famous take-lemma. *}
 apply (drule_tac x = "max (length xs) (length ys)" in spec)
-apply (simp add: le_max_iff_disj take_all)
+apply (simp add: le_max_iff_disj)
 done
 
 
@@ -2880,8 +2878,8 @@
 done
 
 lemma length_remdups_concat:
- "length(remdups(concat xss)) = card(\<Union>xs \<in> set xss. set xs)"
-by(simp add: set_concat distinct_card[symmetric])
+  "length (remdups (concat xss)) = card (\<Union>xs\<in>set xss. set xs)"
+  by (simp add: distinct_card [symmetric])
 
 lemma length_remdups_card_conv: "length(remdups xs) = card(set xs)"
 proof -
@@ -3519,7 +3517,7 @@
      "sublist (l @ l') A = sublist l A @ sublist l' {j. j + length l : A}"
 apply (unfold sublist_def)
 apply (induct l' rule: rev_induct, simp)
-apply (simp add: upt_add_eq_append[of 0] zip_append sublist_shift_lemma)
+apply (simp add: upt_add_eq_append[of 0] sublist_shift_lemma)
 apply (simp add: add_commute)
 done
 
@@ -3838,7 +3836,7 @@
 by(induct xs)(auto simp:set_insort)
 
 lemma distinct_sort[simp]: "distinct (sort_key f xs) = distinct xs"
-by(induct xs)(simp_all add:distinct_insort set_sort)
+  by (induct xs) (simp_all add: distinct_insort)
 
 lemma sorted_insort_key: "sorted (map f (insort_key f x xs)) = sorted (map f xs)"
   by (induct xs) (auto simp:sorted_Cons set_insort)
diff -r 4657b4c11138 -r 58eef4843641 src/HOL/Map.thy
--- a/src/HOL/Map.thy	Tue Sep 13 08:21:51 2011 -0700
+++ b/src/HOL/Map.thy	Tue Sep 13 17:07:33 2011 -0700
@@ -265,7 +265,7 @@
 lemma map_comp_empty [simp]:
   "m \<circ>\<^sub>m empty = empty"
   "empty \<circ>\<^sub>m m = empty"
-by (auto simp add: map_comp_def intro: ext split: option.splits)
+by (auto simp add: map_comp_def split: option.splits)
 
 lemma map_comp_simps [simp]:
   "m2 k = None \<Longrightarrow> (m1 \<circ>\<^sub>m m2) k = None"
@@ -354,7 +354,7 @@
 by (simp add: restrict_map_def)
 
 lemma restrict_map_insert: "f |` (insert a A) = (f |` A)(a := f a)"
-by (auto simp add: restrict_map_def intro: ext)
+by (auto simp add: restrict_map_def)
 
 lemma restrict_map_empty [simp]: "empty|`D = empty"
 by (simp add: restrict_map_def)
@@ -485,7 +485,7 @@
 subsection {* @{term [source] dom} *}
 
 lemma dom_eq_empty_conv [simp]: "dom f = {} \<longleftrightarrow> f = empty"
-by(auto intro!:ext simp: dom_def)
+  by (auto simp: dom_def)
 
 lemma domI: "m a = Some b ==> a : dom m"
 by(simp add:dom_def)
diff -r 4657b4c11138 -r 58eef4843641 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Tue Sep 13 08:21:51 2011 -0700
+++ b/src/HOL/Orderings.thy	Tue Sep 13 17:07:33 2011 -0700
@@ -1309,10 +1309,10 @@
 
 instance "fun" :: (type, preorder) preorder proof
 qed (auto simp add: le_fun_def less_fun_def
-  intro: order_trans antisym intro!: ext)
+  intro: order_trans antisym)
 
 instance "fun" :: (type, order) order proof
-qed (auto simp add: le_fun_def intro: antisym ext)
+qed (auto simp add: le_fun_def intro: antisym)
 
 instantiation "fun" :: (type, bot) bot
 begin
diff -r 4657b4c11138 -r 58eef4843641 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Tue Sep 13 08:21:51 2011 -0700
+++ b/src/HOL/Product_Type.thy	Tue Sep 13 17:07:33 2011 -0700
@@ -830,10 +830,10 @@
   by (simp add: scomp_unfold prod_case_unfold)
 
 lemma Pair_scomp: "Pair x \<circ>\<rightarrow> f = f x"
-  by (simp add: fun_eq_iff scomp_apply)
+  by (simp add: fun_eq_iff)
 
 lemma scomp_Pair: "x \<circ>\<rightarrow> Pair = x"
-  by (simp add: fun_eq_iff scomp_apply)
+  by (simp add: fun_eq_iff)
 
 lemma scomp_scomp: "(f \<circ>\<rightarrow> g) \<circ>\<rightarrow> h = f \<circ>\<rightarrow> (\<lambda>x. g x \<circ>\<rightarrow> h)"
   by (simp add: fun_eq_iff scomp_unfold)
@@ -842,7 +842,7 @@
   by (simp add: fun_eq_iff scomp_unfold fcomp_def)
 
 lemma fcomp_scomp: "(f \<circ>> g) \<circ>\<rightarrow> h = f \<circ>> (g \<circ>\<rightarrow> h)"
-  by (simp add: fun_eq_iff scomp_unfold fcomp_apply)
+  by (simp add: fun_eq_iff scomp_unfold)
 
 code_const scomp
   (Eval infixl 3 "#->")
@@ -863,7 +863,7 @@
   by (simp add: map_pair_def)
 
 enriched_type map_pair: map_pair
-  by (auto simp add: split_paired_all intro: ext)
+  by (auto simp add: split_paired_all)
 
 lemma fst_map_pair [simp]:
   "fst (map_pair f g x) = f (fst x)"
@@ -1110,10 +1110,10 @@
   by auto
 
 lemma fst_image_times[simp]: "fst ` (A \<times> B) = (if B = {} then {} else A)"
-  by (auto intro!: image_eqI)
+  by force
 
 lemma snd_image_times[simp]: "snd ` (A \<times> B) = (if A = {} then {} else B)"
-  by (auto intro!: image_eqI)
+  by force
 
 lemma insert_times_insert[simp]:
   "insert a A \<times> insert b B =
diff -r 4657b4c11138 -r 58eef4843641 src/HOL/Quotient.thy
--- a/src/HOL/Quotient.thy	Tue Sep 13 08:21:51 2011 -0700
+++ b/src/HOL/Quotient.thy	Tue Sep 13 17:07:33 2011 -0700
@@ -85,7 +85,7 @@
   shows "set_rel R xs ys \<longleftrightarrow> xs = ys \<and> (\<forall>x y. x \<in> xs \<longrightarrow> R x y \<longrightarrow> y \<in> xs)"
   unfolding set_rel_def
   using equivp_reflp[OF e]
-  by auto (metis equivp_symp[OF e])+
+  by auto (metis, metis equivp_symp[OF e])
 
 subsection {* Quotient Predicate *}
 
@@ -269,12 +269,12 @@
 lemma ball_reg_right:
   assumes a: "\<And>x. x \<in> R \<Longrightarrow> P x \<longrightarrow> Q x"
   shows "All P \<longrightarrow> Ball R Q"
-  using a by (metis Collect_mem_eq)
+  using a by fast
 
 lemma bex_reg_left:
   assumes a: "\<And>x. x \<in> R \<Longrightarrow> Q x \<longrightarrow> P x"
   shows "Bex R Q \<longrightarrow> Ex P"
-  using a by (metis Collect_mem_eq)
+  using a by fast
 
 lemma ball_reg_left:
   assumes a: "equivp R"
@@ -317,25 +317,25 @@
   assumes a: "!x :: 'a. (P x --> Q x)"
   and     b: "All P"
   shows "All Q"
-  using a b by (metis)
+  using a b by fast
 
 lemma ex_reg:
   assumes a: "!x :: 'a. (P x --> Q x)"
   and     b: "Ex P"
   shows "Ex Q"
-  using a b by metis
+  using a b by fast
 
 lemma ball_reg:
   assumes a: "!x :: 'a. (x \<in> R --> P x --> Q x)"
   and     b: "Ball R P"
   shows "Ball R Q"
-  using a b by (metis Collect_mem_eq)
+  using a b by fast
 
 lemma bex_reg:
   assumes a: "!x :: 'a. (x \<in> R --> P x --> Q x)"
   and     b: "Bex R P"
   shows "Bex R Q"
-  using a b by (metis Collect_mem_eq)
+  using a b by fast
 
 
 lemma ball_all_comm:
@@ -569,7 +569,7 @@
 lemma o_rsp:
   "((R2 ===> R3) ===> (R1 ===> R2) ===> (R1 ===> R3)) op \<circ> op \<circ>"
   "(op = ===> (R1 ===> op =) ===> R1 ===> op =) op \<circ> op \<circ>"
-  by (auto intro!: fun_relI elim: fun_relE)
+  by (force elim: fun_relE)+
 
 lemma cond_prs:
   assumes a: "Quotient R absf repf"
@@ -585,7 +585,7 @@
 lemma if_rsp:
   assumes q: "Quotient R Abs Rep"
   shows "(op = ===> R ===> R ===> R) If If"
-  by (auto intro!: fun_relI)
+  by force
 
 lemma let_prs:
   assumes q1: "Quotient R1 Abs1 Rep1"
@@ -596,11 +596,11 @@
 
 lemma let_rsp:
   shows "(R1 ===> (R1 ===> R2) ===> R2) Let Let"
-  by (auto intro!: fun_relI elim: fun_relE)
+  by (force elim: fun_relE)
 
 lemma id_rsp:
   shows "(R ===> R) id id"
-  by (auto intro: fun_relI)
+  by auto
 
 lemma id_prs:
   assumes a: "Quotient R Abs Rep"
diff -r 4657b4c11138 -r 58eef4843641 src/HOL/Random.thy
--- a/src/HOL/Random.thy	Tue Sep 13 08:21:51 2011 -0700
+++ b/src/HOL/Random.thy	Tue Sep 13 17:07:33 2011 -0700
@@ -57,7 +57,7 @@
 
 lemma range:
   "k > 0 \<Longrightarrow> fst (range k s) < k"
-  by (simp add: range_def scomp_apply split_def del: log.simps iterate.simps)
+  by (simp add: range_def split_def del: log.simps iterate.simps)
 
 definition select :: "'a list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
   "select xs = range (Code_Numeral.of_nat (length xs))
@@ -73,7 +73,7 @@
   then have
     "Code_Numeral.nat_of (fst (range (Code_Numeral.of_nat (length xs)) s)) < length xs" by simp
   then show ?thesis
-    by (simp add: scomp_apply split_beta select_def)
+    by (simp add: split_beta select_def)
 qed
 
 primrec pick :: "(code_numeral \<times> 'a) list \<Rightarrow> code_numeral \<Rightarrow> 'a" where
@@ -188,4 +188,3 @@
 no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
 
 end
-
diff -r 4657b4c11138 -r 58eef4843641 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Tue Sep 13 08:21:51 2011 -0700
+++ b/src/HOL/Relation.thy	Tue Sep 13 17:07:33 2011 -0700
@@ -420,7 +420,7 @@
 by blast
 
 lemma fst_eq_Domain: "fst ` R = Domain R"
-by (auto intro!:image_eqI)
+  by force
 
 lemma Domain_dprod [simp]: "Domain (dprod r s) = uprod (Domain r) (Domain s)"
 by auto
@@ -471,7 +471,7 @@
 by blast
 
 lemma snd_eq_Range: "snd ` R = Range R"
-by (auto intro!:image_eqI)
+  by force
 
 
 subsection {* Field *}
diff -r 4657b4c11138 -r 58eef4843641 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Tue Sep 13 08:21:51 2011 -0700
+++ b/src/HOL/Rings.thy	Tue Sep 13 17:07:33 2011 -0700
@@ -1100,7 +1100,7 @@
 
 lemma abs_one [simp]:
   "\<bar>1\<bar> = 1"
-  by (simp add: abs_if zero_less_one [THEN less_not_sym])
+  by (simp add: abs_if)
 
 end
 
diff -r 4657b4c11138 -r 58eef4843641 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Tue Sep 13 08:21:51 2011 -0700
+++ b/src/HOL/Transitive_Closure.thy	Tue Sep 13 17:07:33 2011 -0700
@@ -220,7 +220,7 @@
   apply (rename_tac a b)
   apply (case_tac "a = b")
    apply blast
-  apply (blast intro!: r_into_rtrancl)
+  apply blast
   done
 
 lemma rtranclp_r_diff_Id: "(inf r op ~=)^** = r^**"
diff -r 4657b4c11138 -r 58eef4843641 src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Tue Sep 13 08:21:51 2011 -0700
+++ b/src/HOL/Wellfounded.thy	Tue Sep 13 17:07:33 2011 -0700
@@ -190,7 +190,7 @@
   "wfP (\<lambda>x y. False)"
 proof -
   have "wfP bot" by (fact wf_empty [to_pred bot_empty_eq2])
-  then show ?thesis by (simp add: bot_fun_def bot_bool_def)
+  then show ?thesis by (simp add: bot_fun_def)
 qed
 
 lemma wf_Int1: "wf r ==> wf (r Int r')"
@@ -573,7 +573,7 @@
 
 theorem accp_wfPI: "\<forall>x. accp r x ==> wfP r"
   apply (rule wfPUNIVI)
-  apply (induct_tac P x rule: accp_induct)
+  apply (rule_tac P=P in accp_induct)
    apply blast
   apply blast
   done