tuned proofs
authorhuffman
Tue Sep 13 17:07:33 2011 -0700 (2011-09-13)
changeset 4492158eef4843641
parent 44920 4657b4c11138
child 44922 14f7da460ce8
tuned proofs
src/HOL/Big_Operators.thy
src/HOL/Complete_Lattices.thy
src/HOL/Deriv.thy
src/HOL/Fields.thy
src/HOL/Fun.thy
src/HOL/HOL.thy
src/HOL/Hilbert_Choice.thy
src/HOL/Lattices.thy
src/HOL/List.thy
src/HOL/Map.thy
src/HOL/Orderings.thy
src/HOL/Product_Type.thy
src/HOL/Quotient.thy
src/HOL/Random.thy
src/HOL/Relation.thy
src/HOL/Rings.thy
src/HOL/Transitive_Closure.thy
src/HOL/Wellfounded.thy
     1.1 --- a/src/HOL/Big_Operators.thy	Tue Sep 13 08:21:51 2011 -0700
     1.2 +++ b/src/HOL/Big_Operators.thy	Tue Sep 13 17:07:33 2011 -0700
     1.3 @@ -1394,7 +1394,7 @@
     1.4    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}"
     1.5  using A proof (induct rule: finite_ne_induct)
     1.6    case singleton thus ?case
     1.7 -    by(simp add: inf_Sup1_distrib [OF B] fold1_singleton_def [OF Sup_fin_def])
     1.8 +    by(simp add: inf_Sup1_distrib [OF B])
     1.9  next
    1.10    case (insert x A)
    1.11    have finB: "finite {inf x b |b. b \<in> B}"
    1.12 @@ -1608,11 +1608,7 @@
    1.13  lemma Max_ge [simp]:
    1.14    assumes "finite A" and "x \<in> A"
    1.15    shows "x \<le> Max A"
    1.16 -proof -
    1.17 -  interpret semilattice_inf max "op \<ge>" "op >"
    1.18 -    by (rule max_lattice)
    1.19 -  from assms show ?thesis by (simp add: Max_def fold1_belowI)
    1.20 -qed
    1.21 +  by (simp add: Max_def semilattice_inf.fold1_belowI [OF max_lattice] assms)
    1.22  
    1.23  lemma Min_ge_iff [simp, no_atp]:
    1.24    assumes "finite A" and "A \<noteq> {}"
    1.25 @@ -1622,11 +1618,7 @@
    1.26  lemma Max_le_iff [simp, no_atp]:
    1.27    assumes "finite A" and "A \<noteq> {}"
    1.28    shows "Max A \<le> x \<longleftrightarrow> (\<forall>a\<in>A. a \<le> x)"
    1.29 -proof -
    1.30 -  interpret semilattice_inf max "op \<ge>" "op >"
    1.31 -    by (rule max_lattice)
    1.32 -  from assms show ?thesis by (simp add: Max_def below_fold1_iff)
    1.33 -qed
    1.34 +  by (simp add: Max_def semilattice_inf.below_fold1_iff [OF max_lattice] assms)
    1.35  
    1.36  lemma Min_gr_iff [simp, no_atp]:
    1.37    assumes "finite A" and "A \<noteq> {}"
    1.38 @@ -1636,12 +1628,8 @@
    1.39  lemma Max_less_iff [simp, no_atp]:
    1.40    assumes "finite A" and "A \<noteq> {}"
    1.41    shows "Max A < x \<longleftrightarrow> (\<forall>a\<in>A. a < x)"
    1.42 -proof -
    1.43 -  interpret dual: linorder "op \<ge>" "op >"
    1.44 -    by (rule dual_linorder)
    1.45 -  from assms show ?thesis
    1.46 -    by (simp add: Max_def dual.strict_below_fold1_iff [folded dual.dual_max])
    1.47 -qed
    1.48 +  by (simp add: Max_def linorder.dual_max [OF dual_linorder]
    1.49 +    linorder.strict_below_fold1_iff [OF dual_linorder] assms)
    1.50  
    1.51  lemma Min_le_iff [no_atp]:
    1.52    assumes "finite A" and "A \<noteq> {}"
    1.53 @@ -1651,12 +1639,8 @@
    1.54  lemma Max_ge_iff [no_atp]:
    1.55    assumes "finite A" and "A \<noteq> {}"
    1.56    shows "x \<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<le> a)"
    1.57 -proof -
    1.58 -  interpret dual: linorder "op \<ge>" "op >"
    1.59 -    by (rule dual_linorder)
    1.60 -  from assms show ?thesis
    1.61 -    by (simp add: Max_def dual.fold1_below_iff [folded dual.dual_max])
    1.62 -qed
    1.63 +  by (simp add: Max_def linorder.dual_max [OF dual_linorder]
    1.64 +    linorder.fold1_below_iff [OF dual_linorder] assms)
    1.65  
    1.66  lemma Min_less_iff [no_atp]:
    1.67    assumes "finite A" and "A \<noteq> {}"
    1.68 @@ -1666,12 +1650,8 @@
    1.69  lemma Max_gr_iff [no_atp]:
    1.70    assumes "finite A" and "A \<noteq> {}"
    1.71    shows "x < Max A \<longleftrightarrow> (\<exists>a\<in>A. x < a)"
    1.72 -proof -
    1.73 -  interpret dual: linorder "op \<ge>" "op >"
    1.74 -    by (rule dual_linorder)
    1.75 -  from assms show ?thesis
    1.76 -    by (simp add: Max_def dual.fold1_strict_below_iff [folded dual.dual_max])
    1.77 -qed
    1.78 +  by (simp add: Max_def linorder.dual_max [OF dual_linorder]
    1.79 +    linorder.fold1_strict_below_iff [OF dual_linorder] assms)
    1.80  
    1.81  lemma Min_eqI:
    1.82    assumes "finite A"
    1.83 @@ -1705,12 +1685,8 @@
    1.84  lemma Max_mono:
    1.85    assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
    1.86    shows "Max M \<le> Max N"
    1.87 -proof -
    1.88 -  interpret dual: linorder "op \<ge>" "op >"
    1.89 -    by (rule dual_linorder)
    1.90 -  from assms show ?thesis
    1.91 -    by (simp add: Max_def dual.fold1_antimono [folded dual.dual_max])
    1.92 -qed
    1.93 +  by (simp add: Max_def linorder.dual_max [OF dual_linorder]
    1.94 +    linorder.fold1_antimono [OF dual_linorder] assms)
    1.95  
    1.96  lemma finite_linorder_max_induct[consumes 1, case_names empty insert]:
    1.97   assumes fin: "finite A"
     2.1 --- a/src/HOL/Complete_Lattices.thy	Tue Sep 13 08:21:51 2011 -0700
     2.2 +++ b/src/HOL/Complete_Lattices.thy	Tue Sep 13 17:07:33 2011 -0700
     2.3 @@ -84,23 +84,13 @@
     2.4  
     2.5  lemma INF_foundation_dual [no_atp]:
     2.6    "complete_lattice.SUPR Inf = INFI"
     2.7 -proof (rule ext)+
     2.8 -  interpret dual: complete_lattice Sup Inf sup "op \<ge>" "op >" inf \<top> \<bottom>
     2.9 -    by (fact dual_complete_lattice)
    2.10 -  fix f :: "'b \<Rightarrow> 'a" and A
    2.11 -  show "complete_lattice.SUPR Inf A f = (\<Sqinter>a\<in>A. f a)"
    2.12 -    by (simp only: dual.SUP_def INF_def)
    2.13 -qed
    2.14 +  by (simp add: fun_eq_iff INF_def
    2.15 +    complete_lattice.SUP_def [OF dual_complete_lattice])
    2.16  
    2.17  lemma SUP_foundation_dual [no_atp]:
    2.18    "complete_lattice.INFI Sup = SUPR"
    2.19 -proof (rule ext)+
    2.20 -  interpret dual: complete_lattice Sup Inf sup "op \<ge>" "op >" inf \<top> \<bottom>
    2.21 -    by (fact dual_complete_lattice)
    2.22 -  fix f :: "'b \<Rightarrow> 'a" and A
    2.23 -  show "complete_lattice.INFI Sup A f = (\<Squnion>a\<in>A. f a)"
    2.24 -    by (simp only: dual.INF_def SUP_def)
    2.25 -qed
    2.26 +  by (simp add: fun_eq_iff SUP_def
    2.27 +    complete_lattice.INF_def [OF dual_complete_lattice])
    2.28  
    2.29  lemma INF_lower: "i \<in> A \<Longrightarrow> (\<Sqinter>i\<in>A. f i) \<sqsubseteq> f i"
    2.30    by (auto simp add: INF_def intro: Inf_lower)
    2.31 @@ -330,10 +320,10 @@
    2.32    by (auto intro: antisym SUP_upper SUP_least)
    2.33  
    2.34  lemma INF_top [simp]: "(\<Sqinter>x\<in>A. \<top>) = \<top>"
    2.35 -  by (cases "A = {}") (simp_all add: INF_empty)
    2.36 +  by (cases "A = {}") simp_all
    2.37  
    2.38  lemma SUP_bot [simp]: "(\<Squnion>x\<in>A. \<bottom>) = \<bottom>"
    2.39 -  by (cases "A = {}") (simp_all add: SUP_empty)
    2.40 +  by (cases "A = {}") simp_all
    2.41  
    2.42  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)"
    2.43    by (iprover intro: INF_lower INF_greatest order_trans antisym)
    2.44 @@ -359,11 +349,11 @@
    2.45  
    2.46  lemma INF_constant:
    2.47    "(\<Sqinter>y\<in>A. c) = (if A = {} then \<top> else c)"
    2.48 -  by (simp add: INF_empty)
    2.49 +  by simp
    2.50  
    2.51  lemma SUP_constant:
    2.52    "(\<Squnion>y\<in>A. c) = (if A = {} then \<bottom> else c)"
    2.53 -  by (simp add: SUP_empty)
    2.54 +  by simp
    2.55  
    2.56  lemma less_INF_D:
    2.57    assumes "y < (\<Sqinter>i\<in>A. f i)" "i \<in> A" shows "y < f i"
    2.58 @@ -385,11 +375,11 @@
    2.59  
    2.60  lemma INF_UNIV_bool_expand:
    2.61    "(\<Sqinter>b. A b) = A True \<sqinter> A False"
    2.62 -  by (simp add: UNIV_bool INF_empty INF_insert inf_commute)
    2.63 +  by (simp add: UNIV_bool INF_insert inf_commute)
    2.64  
    2.65  lemma SUP_UNIV_bool_expand:
    2.66    "(\<Squnion>b. A b) = A True \<squnion> A False"
    2.67 -  by (simp add: UNIV_bool SUP_empty SUP_insert sup_commute)
    2.68 +  by (simp add: UNIV_bool SUP_insert sup_commute)
    2.69  
    2.70  end
    2.71  
     3.1 --- a/src/HOL/Deriv.thy	Tue Sep 13 08:21:51 2011 -0700
     3.2 +++ b/src/HOL/Deriv.thy	Tue Sep 13 17:07:33 2011 -0700
     3.3 @@ -451,10 +451,11 @@
     3.4           \<forall>n. f(n) \<le> g(n) |]
     3.5        ==> Bseq (f :: nat \<Rightarrow> real)"
     3.6  apply (rule_tac k = "f 0" and K = "g 0" in BseqI2, rule allI)
     3.7 +apply (rule conjI)
     3.8  apply (induct_tac "n")
     3.9  apply (auto intro: order_trans)
    3.10 -apply (rule_tac y = "g (Suc na)" in order_trans)
    3.11 -apply (induct_tac [2] "na")
    3.12 +apply (rule_tac y = "g n" in order_trans)
    3.13 +apply (induct_tac [2] "n")
    3.14  apply (auto intro: order_trans)
    3.15  done
    3.16  
    3.17 @@ -470,17 +471,7 @@
    3.18  lemma f_inc_imp_le_lim:
    3.19    fixes f :: "nat \<Rightarrow> real"
    3.20    shows "\<lbrakk>\<forall>n. f n \<le> f (Suc n); convergent f\<rbrakk> \<Longrightarrow> f n \<le> lim f"
    3.21 -apply (rule linorder_not_less [THEN iffD1])
    3.22 -apply (auto simp add: convergent_LIMSEQ_iff LIMSEQ_iff monoseq_Suc)
    3.23 -apply (drule_tac x = "f n - lim f" in spec, clarsimp)
    3.24 -apply (drule_tac P = "%na. no\<le>na --> ?Q na" and x = "no + n" in spec, auto)
    3.25 -apply (subgoal_tac "lim f \<le> f (no + n) ")
    3.26 -apply (drule_tac no=no and m=n in lemma_f_mono_add)
    3.27 -apply (auto simp add: add_commute)
    3.28 -apply (induct_tac "no")
    3.29 -apply simp
    3.30 -apply (auto intro: order_trans simp add: diff_minus abs_if)
    3.31 -done
    3.32 +  by (rule incseq_le, simp add: incseq_SucI, simp add: convergent_LIMSEQ_iff)
    3.33  
    3.34  lemma lim_uminus:
    3.35    fixes g :: "nat \<Rightarrow> 'a::real_normed_vector"
    3.36 @@ -492,10 +483,7 @@
    3.37  lemma g_dec_imp_lim_le:
    3.38    fixes g :: "nat \<Rightarrow> real"
    3.39    shows "\<lbrakk>\<forall>n. g (Suc n) \<le> g(n); convergent g\<rbrakk> \<Longrightarrow> lim g \<le> g n"
    3.40 -apply (subgoal_tac "- (g n) \<le> - (lim g) ")
    3.41 -apply (cut_tac [2] f = "%x. - (g x)" in f_inc_imp_le_lim)
    3.42 -apply (auto simp add: lim_uminus convergent_minus_iff [symmetric])
    3.43 -done
    3.44 +  by (rule decseq_le, simp add: decseq_SucI, simp add: convergent_LIMSEQ_iff)
    3.45  
    3.46  lemma lemma_nest: "[| \<forall>n. f(n) \<le> f(Suc n);
    3.47           \<forall>n. g(Suc n) \<le> g(n);
    3.48 @@ -938,7 +926,7 @@
    3.49  lemma lemma_interval: "[| a < x;  x < b |] ==>
    3.50          \<exists>d::real. 0 < d &  (\<forall>y. \<bar>x-y\<bar> < d --> a \<le> y & y \<le> b)"
    3.51  apply (drule lemma_interval_lt, auto)
    3.52 -apply (auto intro!: exI)
    3.53 +apply force
    3.54  done
    3.55  
    3.56  text{*Rolle's Theorem.
     4.1 --- a/src/HOL/Fields.thy	Tue Sep 13 08:21:51 2011 -0700
     4.2 +++ b/src/HOL/Fields.thy	Tue Sep 13 17:07:33 2011 -0700
     4.3 @@ -270,7 +270,11 @@
     4.4  lemma times_divide_eq_left [simp]: "(b / c) * a = (b * a) / c"
     4.5    by (simp add: divide_inverse mult_ac)
     4.6  
     4.7 -text {* These are later declared as simp rules. *}
     4.8 +text{*It's not obvious whether @{text times_divide_eq} should be
     4.9 +  simprules or not. Their effect is to gather terms into one big
    4.10 +  fraction, like a*b*c / x*y*z. The rationale for that is unclear, but
    4.11 +  many proofs seem to need them.*}
    4.12 +
    4.13  lemmas times_divide_eq [no_atp] = times_divide_eq_right times_divide_eq_left
    4.14  
    4.15  lemma add_frac_eq:
    4.16 @@ -777,15 +781,15 @@
    4.17        have the same sign*}
    4.18  lemma divide_strict_left_mono:
    4.19    "[|b < a; 0 < c; 0 < a*b|] ==> c / a < c / b"
    4.20 -by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono)
    4.21 +  by (auto simp: field_simps zero_less_mult_iff mult_strict_right_mono)
    4.22  
    4.23  lemma divide_left_mono:
    4.24    "[|b \<le> a; 0 \<le> c; 0 < a*b|] ==> c / a \<le> c / b"
    4.25 -by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_right_mono)
    4.26 +  by (auto simp: field_simps zero_less_mult_iff mult_right_mono)
    4.27  
    4.28  lemma divide_strict_left_mono_neg:
    4.29    "[|a < b; c < 0; 0 < a*b|] ==> c / a < c / b"
    4.30 -by(auto simp: field_simps times_divide_eq zero_less_mult_iff mult_strict_right_mono_neg)
    4.31 +  by (auto simp: field_simps zero_less_mult_iff mult_strict_right_mono_neg)
    4.32  
    4.33  lemma mult_imp_div_pos_le: "0 < y ==> x <= z * y ==>
    4.34      x / y <= z"
    4.35 @@ -832,11 +836,6 @@
    4.36    apply simp_all
    4.37  done
    4.38  
    4.39 -text{*It's not obvious whether these should be simprules or not. 
    4.40 -  Their effect is to gather terms into one big fraction, like
    4.41 -  a*b*c / x*y*z. The rationale for that is unclear, but many proofs 
    4.42 -  seem to need them.*}
    4.43 -
    4.44  lemma less_half_sum: "a < b ==> a < (a+b) / (1+1)"
    4.45  by (simp add: field_simps zero_less_two)
    4.46  
     5.1 --- a/src/HOL/Fun.thy	Tue Sep 13 08:21:51 2011 -0700
     5.2 +++ b/src/HOL/Fun.thy	Tue Sep 13 17:07:33 2011 -0700
     5.3 @@ -610,7 +610,7 @@
     5.4  by auto
     5.5  
     5.6  lemma fun_upd_comp: "f \<circ> (g(x := y)) = (f \<circ> g)(x := f y)"
     5.7 -by (auto intro: ext)
     5.8 +  by auto
     5.9  
    5.10  lemma UNION_fun_upd:
    5.11    "UNION J (A(i:=B)) = (UNION (J-{i}) A \<union> (if i\<in>J then B else {}))"
     6.1 --- a/src/HOL/HOL.thy	Tue Sep 13 08:21:51 2011 -0700
     6.2 +++ b/src/HOL/HOL.thy	Tue Sep 13 17:07:33 2011 -0700
     6.3 @@ -1635,7 +1635,7 @@
     6.4    apply (rule iffI)
     6.5    apply (rule_tac a = "%x. THE y. P x y" in ex1I)
     6.6    apply (fast dest!: theI')
     6.7 -  apply (fast intro: ext the1_equality [symmetric])
     6.8 +  apply (fast intro: the1_equality [symmetric])
     6.9    apply (erule ex1E)
    6.10    apply (rule allI)
    6.11    apply (rule ex1I)
     7.1 --- a/src/HOL/Hilbert_Choice.thy	Tue Sep 13 08:21:51 2011 -0700
     7.2 +++ b/src/HOL/Hilbert_Choice.thy	Tue Sep 13 17:07:33 2011 -0700
     7.3 @@ -123,7 +123,7 @@
     7.4  by (simp add:inv_into_f_eq)
     7.5  
     7.6  lemma inj_imp_inv_eq: "[| inj f; ALL x. f(g x) = x |] ==> inv f = g"
     7.7 -by (blast intro: ext inv_into_f_eq)
     7.8 +  by (blast intro: inv_into_f_eq)
     7.9  
    7.10  text{*But is it useful?*}
    7.11  lemma inj_transfer:
    7.12 @@ -286,7 +286,7 @@
    7.13    hence "?f'' a = a'"
    7.14      using `a \<in> A` 1 3 by (auto simp add: f_inv_into_f bij_betw_def)
    7.15    moreover have "f a = a'" using assms 2 3
    7.16 -    by (auto simp add: inv_into_f_f bij_betw_def)
    7.17 +    by (auto simp add: bij_betw_def)
    7.18    ultimately show "?f'' a = f a" by simp
    7.19  qed
    7.20  
     8.1 --- a/src/HOL/Lattices.thy	Tue Sep 13 08:21:51 2011 -0700
     8.2 +++ b/src/HOL/Lattices.thy	Tue Sep 13 17:07:33 2011 -0700
     8.3 @@ -180,8 +180,8 @@
     8.4  lemma inf_left_commute: "x \<sqinter> (y \<sqinter> z) = y \<sqinter> (x \<sqinter> z)"
     8.5    by (fact inf.left_commute)
     8.6  
     8.7 -lemma inf_idem [simp]: "x \<sqinter> x = x"
     8.8 -  by (fact inf.idem)
     8.9 +lemma inf_idem: "x \<sqinter> x = x"
    8.10 +  by (fact inf.idem) (* already simp *)
    8.11  
    8.12  lemma inf_left_idem [simp]: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
    8.13    by (fact inf.left_idem)
    8.14 @@ -219,8 +219,8 @@
    8.15  lemma sup_left_commute: "x \<squnion> (y \<squnion> z) = y \<squnion> (x \<squnion> z)"
    8.16    by (fact sup.left_commute)
    8.17  
    8.18 -lemma sup_idem [simp]: "x \<squnion> x = x"
    8.19 -  by (fact sup.idem)
    8.20 +lemma sup_idem: "x \<squnion> x = x"
    8.21 +  by (fact sup.idem) (* already simp *)
    8.22  
    8.23  lemma sup_left_idem [simp]: "x \<squnion> (x \<squnion> y) = x \<squnion> y"
    8.24    by (fact sup.left_idem)
    8.25 @@ -311,23 +311,13 @@
    8.26  
    8.27  lemma less_supI1:
    8.28    "x \<sqsubset> a \<Longrightarrow> x \<sqsubset> a \<squnion> b"
    8.29 -proof -
    8.30 -  interpret dual: semilattice_inf sup "op \<ge>" "op >"
    8.31 -    by (fact dual_semilattice)
    8.32 -  assume "x \<sqsubset> a"
    8.33 -  then show "x \<sqsubset> a \<squnion> b"
    8.34 -    by (fact dual.less_infI1)
    8.35 -qed
    8.36 +  using dual_semilattice
    8.37 +  by (rule semilattice_inf.less_infI1)
    8.38  
    8.39  lemma less_supI2:
    8.40    "x \<sqsubset> b \<Longrightarrow> x \<sqsubset> a \<squnion> b"
    8.41 -proof -
    8.42 -  interpret dual: semilattice_inf sup "op \<ge>" "op >"
    8.43 -    by (fact dual_semilattice)
    8.44 -  assume "x \<sqsubset> b"
    8.45 -  then show "x \<sqsubset> a \<squnion> b"
    8.46 -    by (fact dual.less_infI2)
    8.47 -qed
    8.48 +  using dual_semilattice
    8.49 +  by (rule semilattice_inf.less_infI2)
    8.50  
    8.51  end
    8.52  
    8.53 @@ -341,16 +331,16 @@
    8.54  begin
    8.55  
    8.56  lemma sup_inf_distrib2:
    8.57 - "(y \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)"
    8.58 -by(simp add: inf_sup_aci sup_inf_distrib1)
    8.59 +  "(y \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)"
    8.60 +  by (simp add: sup_commute sup_inf_distrib1)
    8.61  
    8.62  lemma inf_sup_distrib1:
    8.63 - "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
    8.64 -by(rule distrib_imp2[OF sup_inf_distrib1])
    8.65 +  "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
    8.66 +  by (rule distrib_imp2 [OF sup_inf_distrib1])
    8.67  
    8.68  lemma inf_sup_distrib2:
    8.69 - "(y \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (z \<sqinter> x)"
    8.70 -by(simp add: inf_sup_aci inf_sup_distrib1)
    8.71 +  "(y \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (z \<sqinter> x)"
    8.72 +  by (simp add: inf_commute inf_sup_distrib1)
    8.73  
    8.74  lemma dual_distrib_lattice:
    8.75    "class.distrib_lattice sup (op \<ge>) (op >) inf"
    8.76 @@ -510,11 +500,8 @@
    8.77  
    8.78  lemma compl_sup [simp]:
    8.79    "- (x \<squnion> y) = - x \<sqinter> - y"
    8.80 -proof -
    8.81 -  interpret boolean_algebra "\<lambda>x y. x \<squnion> - y" uminus sup greater_eq greater inf \<top> \<bottom>
    8.82 -    by (rule dual_boolean_algebra)
    8.83 -  then show ?thesis by simp
    8.84 -qed
    8.85 +  using dual_boolean_algebra
    8.86 +  by (rule boolean_algebra.compl_inf)
    8.87  
    8.88  lemma compl_mono:
    8.89    "x \<sqsubseteq> y \<Longrightarrow> - y \<sqsubseteq> - x"
     9.1 --- a/src/HOL/List.thy	Tue Sep 13 08:21:51 2011 -0700
     9.2 +++ b/src/HOL/List.thy	Tue Sep 13 17:07:33 2011 -0700
     9.3 @@ -1176,7 +1176,7 @@
     9.4      have "length (filter p (x # xs)) = Suc(card ?S)"
     9.5        using Cons `p x` by simp
     9.6      also have "\<dots> = Suc(card(Suc ` ?S))" using fin
     9.7 -      by (simp add: card_image inj_Suc)
     9.8 +      by (simp add: card_image)
     9.9      also have "\<dots> = card ?S'" using eq fin
    9.10        by (simp add:card_insert_if) (simp add:image_def)
    9.11      finally show ?thesis .
    9.12 @@ -1187,7 +1187,7 @@
    9.13      have "length (filter p (x # xs)) = card ?S"
    9.14        using Cons `\<not> p x` by simp
    9.15      also have "\<dots> = card(Suc ` ?S)" using fin
    9.16 -      by (simp add: card_image inj_Suc)
    9.17 +      by (simp add: card_image)
    9.18      also have "\<dots> = card ?S'" using eq fin
    9.19        by (simp add:card_insert_if)
    9.20      finally show ?thesis .
    9.21 @@ -1529,10 +1529,10 @@
    9.22  by (induct xs) auto
    9.23  
    9.24  lemma last_ConsL: "xs = [] \<Longrightarrow> last(x#xs) = x"
    9.25 -by(simp add:last.simps)
    9.26 +  by simp
    9.27  
    9.28  lemma last_ConsR: "xs \<noteq> [] \<Longrightarrow> last(x#xs) = last xs"
    9.29 -by(simp add:last.simps)
    9.30 +  by simp
    9.31  
    9.32  lemma last_append: "last(xs @ ys) = (if ys = [] then last xs else last ys)"
    9.33  by (induct xs) (auto)
    9.34 @@ -2627,7 +2627,7 @@
    9.35  lemma nth_map_upt: "i < n-m ==> (map f [m..<n]) ! i = f(m+i)"
    9.36  apply (induct n m  arbitrary: i rule: diff_induct)
    9.37  prefer 3 apply (subst map_Suc_upt[symmetric])
    9.38 -apply (auto simp add: less_diff_conv nth_upt)
    9.39 +apply (auto simp add: less_diff_conv)
    9.40  done
    9.41  
    9.42  lemma nth_take_lemma:
    9.43 @@ -2647,9 +2647,7 @@
    9.44  
    9.45  lemma nth_equalityI:
    9.46   "[| length xs = length ys; ALL i < length xs. xs!i = ys!i |] ==> xs = ys"
    9.47 -apply (frule nth_take_lemma [OF le_refl eq_imp_le])
    9.48 -apply (simp_all add: take_all)
    9.49 -done
    9.50 +  by (frule nth_take_lemma [OF le_refl eq_imp_le]) simp_all
    9.51  
    9.52  lemma map_nth:
    9.53    "map (\<lambda>i. xs ! i) [0..<length xs] = xs"
    9.54 @@ -2666,7 +2664,7 @@
    9.55  lemma take_equalityI: "(\<forall>i. take i xs = take i ys) ==> xs = ys"
    9.56  -- {* The famous take-lemma. *}
    9.57  apply (drule_tac x = "max (length xs) (length ys)" in spec)
    9.58 -apply (simp add: le_max_iff_disj take_all)
    9.59 +apply (simp add: le_max_iff_disj)
    9.60  done
    9.61  
    9.62  
    9.63 @@ -2880,8 +2878,8 @@
    9.64  done
    9.65  
    9.66  lemma length_remdups_concat:
    9.67 - "length(remdups(concat xss)) = card(\<Union>xs \<in> set xss. set xs)"
    9.68 -by(simp add: set_concat distinct_card[symmetric])
    9.69 +  "length (remdups (concat xss)) = card (\<Union>xs\<in>set xss. set xs)"
    9.70 +  by (simp add: distinct_card [symmetric])
    9.71  
    9.72  lemma length_remdups_card_conv: "length(remdups xs) = card(set xs)"
    9.73  proof -
    9.74 @@ -3519,7 +3517,7 @@
    9.75       "sublist (l @ l') A = sublist l A @ sublist l' {j. j + length l : A}"
    9.76  apply (unfold sublist_def)
    9.77  apply (induct l' rule: rev_induct, simp)
    9.78 -apply (simp add: upt_add_eq_append[of 0] zip_append sublist_shift_lemma)
    9.79 +apply (simp add: upt_add_eq_append[of 0] sublist_shift_lemma)
    9.80  apply (simp add: add_commute)
    9.81  done
    9.82  
    9.83 @@ -3838,7 +3836,7 @@
    9.84  by(induct xs)(auto simp:set_insort)
    9.85  
    9.86  lemma distinct_sort[simp]: "distinct (sort_key f xs) = distinct xs"
    9.87 -by(induct xs)(simp_all add:distinct_insort set_sort)
    9.88 +  by (induct xs) (simp_all add: distinct_insort)
    9.89  
    9.90  lemma sorted_insort_key: "sorted (map f (insort_key f x xs)) = sorted (map f xs)"
    9.91    by (induct xs) (auto simp:sorted_Cons set_insort)
    10.1 --- a/src/HOL/Map.thy	Tue Sep 13 08:21:51 2011 -0700
    10.2 +++ b/src/HOL/Map.thy	Tue Sep 13 17:07:33 2011 -0700
    10.3 @@ -265,7 +265,7 @@
    10.4  lemma map_comp_empty [simp]:
    10.5    "m \<circ>\<^sub>m empty = empty"
    10.6    "empty \<circ>\<^sub>m m = empty"
    10.7 -by (auto simp add: map_comp_def intro: ext split: option.splits)
    10.8 +by (auto simp add: map_comp_def split: option.splits)
    10.9  
   10.10  lemma map_comp_simps [simp]:
   10.11    "m2 k = None \<Longrightarrow> (m1 \<circ>\<^sub>m m2) k = None"
   10.12 @@ -354,7 +354,7 @@
   10.13  by (simp add: restrict_map_def)
   10.14  
   10.15  lemma restrict_map_insert: "f |` (insert a A) = (f |` A)(a := f a)"
   10.16 -by (auto simp add: restrict_map_def intro: ext)
   10.17 +by (auto simp add: restrict_map_def)
   10.18  
   10.19  lemma restrict_map_empty [simp]: "empty|`D = empty"
   10.20  by (simp add: restrict_map_def)
   10.21 @@ -485,7 +485,7 @@
   10.22  subsection {* @{term [source] dom} *}
   10.23  
   10.24  lemma dom_eq_empty_conv [simp]: "dom f = {} \<longleftrightarrow> f = empty"
   10.25 -by(auto intro!:ext simp: dom_def)
   10.26 +  by (auto simp: dom_def)
   10.27  
   10.28  lemma domI: "m a = Some b ==> a : dom m"
   10.29  by(simp add:dom_def)
    11.1 --- a/src/HOL/Orderings.thy	Tue Sep 13 08:21:51 2011 -0700
    11.2 +++ b/src/HOL/Orderings.thy	Tue Sep 13 17:07:33 2011 -0700
    11.3 @@ -1309,10 +1309,10 @@
    11.4  
    11.5  instance "fun" :: (type, preorder) preorder proof
    11.6  qed (auto simp add: le_fun_def less_fun_def
    11.7 -  intro: order_trans antisym intro!: ext)
    11.8 +  intro: order_trans antisym)
    11.9  
   11.10  instance "fun" :: (type, order) order proof
   11.11 -qed (auto simp add: le_fun_def intro: antisym ext)
   11.12 +qed (auto simp add: le_fun_def intro: antisym)
   11.13  
   11.14  instantiation "fun" :: (type, bot) bot
   11.15  begin
    12.1 --- a/src/HOL/Product_Type.thy	Tue Sep 13 08:21:51 2011 -0700
    12.2 +++ b/src/HOL/Product_Type.thy	Tue Sep 13 17:07:33 2011 -0700
    12.3 @@ -830,10 +830,10 @@
    12.4    by (simp add: scomp_unfold prod_case_unfold)
    12.5  
    12.6  lemma Pair_scomp: "Pair x \<circ>\<rightarrow> f = f x"
    12.7 -  by (simp add: fun_eq_iff scomp_apply)
    12.8 +  by (simp add: fun_eq_iff)
    12.9  
   12.10  lemma scomp_Pair: "x \<circ>\<rightarrow> Pair = x"
   12.11 -  by (simp add: fun_eq_iff scomp_apply)
   12.12 +  by (simp add: fun_eq_iff)
   12.13  
   12.14  lemma scomp_scomp: "(f \<circ>\<rightarrow> g) \<circ>\<rightarrow> h = f \<circ>\<rightarrow> (\<lambda>x. g x \<circ>\<rightarrow> h)"
   12.15    by (simp add: fun_eq_iff scomp_unfold)
   12.16 @@ -842,7 +842,7 @@
   12.17    by (simp add: fun_eq_iff scomp_unfold fcomp_def)
   12.18  
   12.19  lemma fcomp_scomp: "(f \<circ>> g) \<circ>\<rightarrow> h = f \<circ>> (g \<circ>\<rightarrow> h)"
   12.20 -  by (simp add: fun_eq_iff scomp_unfold fcomp_apply)
   12.21 +  by (simp add: fun_eq_iff scomp_unfold)
   12.22  
   12.23  code_const scomp
   12.24    (Eval infixl 3 "#->")
   12.25 @@ -863,7 +863,7 @@
   12.26    by (simp add: map_pair_def)
   12.27  
   12.28  enriched_type map_pair: map_pair
   12.29 -  by (auto simp add: split_paired_all intro: ext)
   12.30 +  by (auto simp add: split_paired_all)
   12.31  
   12.32  lemma fst_map_pair [simp]:
   12.33    "fst (map_pair f g x) = f (fst x)"
   12.34 @@ -1110,10 +1110,10 @@
   12.35    by auto
   12.36  
   12.37  lemma fst_image_times[simp]: "fst ` (A \<times> B) = (if B = {} then {} else A)"
   12.38 -  by (auto intro!: image_eqI)
   12.39 +  by force
   12.40  
   12.41  lemma snd_image_times[simp]: "snd ` (A \<times> B) = (if A = {} then {} else B)"
   12.42 -  by (auto intro!: image_eqI)
   12.43 +  by force
   12.44  
   12.45  lemma insert_times_insert[simp]:
   12.46    "insert a A \<times> insert b B =
    13.1 --- a/src/HOL/Quotient.thy	Tue Sep 13 08:21:51 2011 -0700
    13.2 +++ b/src/HOL/Quotient.thy	Tue Sep 13 17:07:33 2011 -0700
    13.3 @@ -85,7 +85,7 @@
    13.4    shows "set_rel R xs ys \<longleftrightarrow> xs = ys \<and> (\<forall>x y. x \<in> xs \<longrightarrow> R x y \<longrightarrow> y \<in> xs)"
    13.5    unfolding set_rel_def
    13.6    using equivp_reflp[OF e]
    13.7 -  by auto (metis equivp_symp[OF e])+
    13.8 +  by auto (metis, metis equivp_symp[OF e])
    13.9  
   13.10  subsection {* Quotient Predicate *}
   13.11  
   13.12 @@ -269,12 +269,12 @@
   13.13  lemma ball_reg_right:
   13.14    assumes a: "\<And>x. x \<in> R \<Longrightarrow> P x \<longrightarrow> Q x"
   13.15    shows "All P \<longrightarrow> Ball R Q"
   13.16 -  using a by (metis Collect_mem_eq)
   13.17 +  using a by fast
   13.18  
   13.19  lemma bex_reg_left:
   13.20    assumes a: "\<And>x. x \<in> R \<Longrightarrow> Q x \<longrightarrow> P x"
   13.21    shows "Bex R Q \<longrightarrow> Ex P"
   13.22 -  using a by (metis Collect_mem_eq)
   13.23 +  using a by fast
   13.24  
   13.25  lemma ball_reg_left:
   13.26    assumes a: "equivp R"
   13.27 @@ -317,25 +317,25 @@
   13.28    assumes a: "!x :: 'a. (P x --> Q x)"
   13.29    and     b: "All P"
   13.30    shows "All Q"
   13.31 -  using a b by (metis)
   13.32 +  using a b by fast
   13.33  
   13.34  lemma ex_reg:
   13.35    assumes a: "!x :: 'a. (P x --> Q x)"
   13.36    and     b: "Ex P"
   13.37    shows "Ex Q"
   13.38 -  using a b by metis
   13.39 +  using a b by fast
   13.40  
   13.41  lemma ball_reg:
   13.42    assumes a: "!x :: 'a. (x \<in> R --> P x --> Q x)"
   13.43    and     b: "Ball R P"
   13.44    shows "Ball R Q"
   13.45 -  using a b by (metis Collect_mem_eq)
   13.46 +  using a b by fast
   13.47  
   13.48  lemma bex_reg:
   13.49    assumes a: "!x :: 'a. (x \<in> R --> P x --> Q x)"
   13.50    and     b: "Bex R P"
   13.51    shows "Bex R Q"
   13.52 -  using a b by (metis Collect_mem_eq)
   13.53 +  using a b by fast
   13.54  
   13.55  
   13.56  lemma ball_all_comm:
   13.57 @@ -569,7 +569,7 @@
   13.58  lemma o_rsp:
   13.59    "((R2 ===> R3) ===> (R1 ===> R2) ===> (R1 ===> R3)) op \<circ> op \<circ>"
   13.60    "(op = ===> (R1 ===> op =) ===> R1 ===> op =) op \<circ> op \<circ>"
   13.61 -  by (auto intro!: fun_relI elim: fun_relE)
   13.62 +  by (force elim: fun_relE)+
   13.63  
   13.64  lemma cond_prs:
   13.65    assumes a: "Quotient R absf repf"
   13.66 @@ -585,7 +585,7 @@
   13.67  lemma if_rsp:
   13.68    assumes q: "Quotient R Abs Rep"
   13.69    shows "(op = ===> R ===> R ===> R) If If"
   13.70 -  by (auto intro!: fun_relI)
   13.71 +  by force
   13.72  
   13.73  lemma let_prs:
   13.74    assumes q1: "Quotient R1 Abs1 Rep1"
   13.75 @@ -596,11 +596,11 @@
   13.76  
   13.77  lemma let_rsp:
   13.78    shows "(R1 ===> (R1 ===> R2) ===> R2) Let Let"
   13.79 -  by (auto intro!: fun_relI elim: fun_relE)
   13.80 +  by (force elim: fun_relE)
   13.81  
   13.82  lemma id_rsp:
   13.83    shows "(R ===> R) id id"
   13.84 -  by (auto intro: fun_relI)
   13.85 +  by auto
   13.86  
   13.87  lemma id_prs:
   13.88    assumes a: "Quotient R Abs Rep"
    14.1 --- a/src/HOL/Random.thy	Tue Sep 13 08:21:51 2011 -0700
    14.2 +++ b/src/HOL/Random.thy	Tue Sep 13 17:07:33 2011 -0700
    14.3 @@ -57,7 +57,7 @@
    14.4  
    14.5  lemma range:
    14.6    "k > 0 \<Longrightarrow> fst (range k s) < k"
    14.7 -  by (simp add: range_def scomp_apply split_def del: log.simps iterate.simps)
    14.8 +  by (simp add: range_def split_def del: log.simps iterate.simps)
    14.9  
   14.10  definition select :: "'a list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
   14.11    "select xs = range (Code_Numeral.of_nat (length xs))
   14.12 @@ -73,7 +73,7 @@
   14.13    then have
   14.14      "Code_Numeral.nat_of (fst (range (Code_Numeral.of_nat (length xs)) s)) < length xs" by simp
   14.15    then show ?thesis
   14.16 -    by (simp add: scomp_apply split_beta select_def)
   14.17 +    by (simp add: split_beta select_def)
   14.18  qed
   14.19  
   14.20  primrec pick :: "(code_numeral \<times> 'a) list \<Rightarrow> code_numeral \<Rightarrow> 'a" where
   14.21 @@ -188,4 +188,3 @@
   14.22  no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
   14.23  
   14.24  end
   14.25 -
    15.1 --- a/src/HOL/Relation.thy	Tue Sep 13 08:21:51 2011 -0700
    15.2 +++ b/src/HOL/Relation.thy	Tue Sep 13 17:07:33 2011 -0700
    15.3 @@ -420,7 +420,7 @@
    15.4  by blast
    15.5  
    15.6  lemma fst_eq_Domain: "fst ` R = Domain R"
    15.7 -by (auto intro!:image_eqI)
    15.8 +  by force
    15.9  
   15.10  lemma Domain_dprod [simp]: "Domain (dprod r s) = uprod (Domain r) (Domain s)"
   15.11  by auto
   15.12 @@ -471,7 +471,7 @@
   15.13  by blast
   15.14  
   15.15  lemma snd_eq_Range: "snd ` R = Range R"
   15.16 -by (auto intro!:image_eqI)
   15.17 +  by force
   15.18  
   15.19  
   15.20  subsection {* Field *}
    16.1 --- a/src/HOL/Rings.thy	Tue Sep 13 08:21:51 2011 -0700
    16.2 +++ b/src/HOL/Rings.thy	Tue Sep 13 17:07:33 2011 -0700
    16.3 @@ -1100,7 +1100,7 @@
    16.4  
    16.5  lemma abs_one [simp]:
    16.6    "\<bar>1\<bar> = 1"
    16.7 -  by (simp add: abs_if zero_less_one [THEN less_not_sym])
    16.8 +  by (simp add: abs_if)
    16.9  
   16.10  end
   16.11  
    17.1 --- a/src/HOL/Transitive_Closure.thy	Tue Sep 13 08:21:51 2011 -0700
    17.2 +++ b/src/HOL/Transitive_Closure.thy	Tue Sep 13 17:07:33 2011 -0700
    17.3 @@ -220,7 +220,7 @@
    17.4    apply (rename_tac a b)
    17.5    apply (case_tac "a = b")
    17.6     apply blast
    17.7 -  apply (blast intro!: r_into_rtrancl)
    17.8 +  apply blast
    17.9    done
   17.10  
   17.11  lemma rtranclp_r_diff_Id: "(inf r op ~=)^** = r^**"
    18.1 --- a/src/HOL/Wellfounded.thy	Tue Sep 13 08:21:51 2011 -0700
    18.2 +++ b/src/HOL/Wellfounded.thy	Tue Sep 13 17:07:33 2011 -0700
    18.3 @@ -190,7 +190,7 @@
    18.4    "wfP (\<lambda>x y. False)"
    18.5  proof -
    18.6    have "wfP bot" by (fact wf_empty [to_pred bot_empty_eq2])
    18.7 -  then show ?thesis by (simp add: bot_fun_def bot_bool_def)
    18.8 +  then show ?thesis by (simp add: bot_fun_def)
    18.9  qed
   18.10  
   18.11  lemma wf_Int1: "wf r ==> wf (r Int r')"
   18.12 @@ -573,7 +573,7 @@
   18.13  
   18.14  theorem accp_wfPI: "\<forall>x. accp r x ==> wfP r"
   18.15    apply (rule wfPUNIVI)
   18.16 -  apply (induct_tac P x rule: accp_induct)
   18.17 +  apply (rule_tac P=P in accp_induct)
   18.18     apply blast
   18.19    apply blast
   18.20    done