tuned proofs -- clarified flow of facts wrt. calculation;
authorwenzelm
Tue Sep 03 01:12:40 2013 +0200 (2013-09-03)
changeset 53374a14d2a854c02
parent 53373 3ca9e79ac926
child 53375 78693e46a237
tuned proofs -- clarified flow of facts wrt. calculation;
src/HOL/Algebra/Divisibility.thy
src/HOL/BNF/Examples/Stream.thy
src/HOL/BNF/More_BNFs.thy
src/HOL/Big_Operators.thy
src/HOL/Complete_Lattices.thy
src/HOL/Complex.thy
src/HOL/Decision_Procs/Commutative_Ring_Complete.thy
src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
src/HOL/Deriv.thy
src/HOL/Divides.thy
src/HOL/Fields.thy
src/HOL/Finite_Set.thy
src/HOL/Imperative_HOL/Legacy_Mrec.thy
src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy
src/HOL/Imperative_HOL/ex/Sublist.thy
src/HOL/Library/Extended_Real.thy
src/HOL/Library/FinFun.thy
src/HOL/Library/Formal_Power_Series.thy
src/HOL/Library/Fraction_Field.thy
src/HOL/Library/Liminf_Limsup.thy
src/HOL/Library/Permutations.thy
src/HOL/Library/RBT_Impl.thy
src/HOL/Library/Ramsey.thy
src/HOL/Library/Zorn.thy
src/HOL/List.thy
src/HOL/Map.thy
src/HOL/MicroJava/J/TypeRel.thy
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Derivative.thy
src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
src/HOL/Multivariate_Analysis/Integration.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/Nat.thy
src/HOL/Nominal/Examples/Crary.thy
src/HOL/Number_Theory/Binomial.thy
src/HOL/Number_Theory/MiscAlgebra.thy
src/HOL/Predicate.thy
src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy
src/HOL/Probability/Binary_Product_Measure.thy
src/HOL/Probability/Fin_Map.thy
src/HOL/Probability/Finite_Product_Measure.thy
src/HOL/Probability/Infinite_Product_Measure.thy
src/HOL/Probability/Information.thy
src/HOL/Probability/Lebesgue_Integration.thy
src/HOL/Probability/Lebesgue_Measure.thy
src/HOL/Probability/Measure_Space.thy
src/HOL/Probability/Projective_Limit.thy
src/HOL/Probability/Radon_Nikodym.thy
src/HOL/Probability/Sigma_Algebra.thy
src/HOL/Probability/ex/Dining_Cryptographers.thy
src/HOL/Quotient_Examples/FSet.thy
src/HOL/Rat.thy
src/HOL/Real.thy
src/HOL/Real_Vector_Spaces.thy
src/HOL/Set_Interval.thy
src/HOL/Statespace/DistinctTreeProver.thy
src/HOL/Topological_Spaces.thy
src/HOL/ex/HarmonicSeries.thy
     1.1 --- a/src/HOL/Algebra/Divisibility.thy	Tue Sep 03 00:51:08 2013 +0200
     1.2 +++ b/src/HOL/Algebra/Divisibility.thy	Tue Sep 03 01:12:40 2013 +0200
     1.3 @@ -3637,11 +3637,11 @@
     1.4      assume cunit:"c \<in> Units G"
     1.5  
     1.6      have "b \<otimes> inv c = a \<otimes> c \<otimes> inv c" by (simp add: b)
     1.7 -    also with ccarr acarr cunit
     1.8 +    also from ccarr acarr cunit
     1.9          have "\<dots> = a \<otimes> (c \<otimes> inv c)" by (fast intro: m_assoc)
    1.10 -    also with ccarr cunit
    1.11 +    also from ccarr cunit
    1.12          have "\<dots> = a \<otimes> \<one>" by (simp add: Units_r_inv)
    1.13 -    also with acarr
    1.14 +    also from acarr
    1.15          have "\<dots> = a" by simp
    1.16      finally have "a = b \<otimes> inv c" by simp
    1.17      with ccarr cunit
     2.1 --- a/src/HOL/BNF/Examples/Stream.thy	Tue Sep 03 00:51:08 2013 +0200
     2.2 +++ b/src/HOL/BNF/Examples/Stream.thy	Tue Sep 03 01:12:40 2013 +0200
     2.3 @@ -423,9 +423,9 @@
     2.4        case False
     2.5        hence "x = flat (stl s) !! (y - length (shd s))" by (metis less(2,3) flat_snth)
     2.6        moreover
     2.7 -      { from less(2) have "length (shd s) > 0" by (cases s) simp_all
     2.8 -        moreover with False have "y > 0" by (cases y) simp_all
     2.9 -        ultimately have "y - length (shd s) < y" by simp
    2.10 +      { from less(2) have *: "length (shd s) > 0" by (cases s) simp_all
    2.11 +        with False have "y > 0" by (cases y) simp_all
    2.12 +        with * have "y - length (shd s) < y" by simp
    2.13        }
    2.14        moreover have "\<forall>xs \<in> sset (stl s). xs \<noteq> []" using less(2) by (cases s) auto
    2.15        ultimately have "\<exists>n m'. x = stl s !! n ! m' \<and> m' < length (stl s !! n)" by (intro less(1)) auto
     3.1 --- a/src/HOL/BNF/More_BNFs.thy	Tue Sep 03 00:51:08 2013 +0200
     3.2 +++ b/src/HOL/BNF/More_BNFs.thy	Tue Sep 03 01:12:40 2013 +0200
     3.3 @@ -898,11 +898,10 @@
     3.4  proof (intro multiset_eqI, transfer fixing: f)
     3.5    fix x :: 'a and M1 M2 :: "'b \<Rightarrow> nat"
     3.6    assume "M1 \<in> multiset" "M2 \<in> multiset"
     3.7 -  moreover
     3.8    hence "setsum M1 {a. f a = x \<and> 0 < M1 a} = setsum M1 {a. f a = x \<and> 0 < M1 a + M2 a}"
     3.9          "setsum M2 {a. f a = x \<and> 0 < M2 a} = setsum M2 {a. f a = x \<and> 0 < M1 a + M2 a}"
    3.10      by (auto simp: multiset_def intro!: setsum_mono_zero_cong_left)
    3.11 -  ultimately show "(\<Sum>a | f a = x \<and> 0 < M1 a + M2 a. M1 a + M2 a) =
    3.12 +  then show "(\<Sum>a | f a = x \<and> 0 < M1 a + M2 a. M1 a + M2 a) =
    3.13         setsum M1 {a. f a = x \<and> 0 < M1 a} +
    3.14         setsum M2 {a. f a = x \<and> 0 < M2 a}"
    3.15      by (auto simp: setsum.distrib[symmetric])
     4.1 --- a/src/HOL/Big_Operators.thy	Tue Sep 03 00:51:08 2013 +0200
     4.2 +++ b/src/HOL/Big_Operators.thy	Tue Sep 03 01:12:40 2013 +0200
     4.3 @@ -46,7 +46,7 @@
     4.4  proof -
     4.5    from `x \<in> A` obtain B where A: "A = insert x B" and "x \<notin> B"
     4.6      by (auto dest: mk_disjoint_insert)
     4.7 -  moreover from `finite A` this have "finite B" by simp
     4.8 +  moreover from `finite A` A have "finite B" by simp
     4.9    ultimately show ?thesis by simp
    4.10  qed
    4.11  
     5.1 --- a/src/HOL/Complete_Lattices.thy	Tue Sep 03 00:51:08 2013 +0200
     5.2 +++ b/src/HOL/Complete_Lattices.thy	Tue Sep 03 01:12:40 2013 +0200
     5.3 @@ -250,7 +250,7 @@
     5.4    shows "\<Sqinter>A \<sqsubseteq> u"
     5.5  proof -
     5.6    from `A \<noteq> {}` obtain v where "v \<in> A" by blast
     5.7 -  moreover with assms have "v \<sqsubseteq> u" by blast
     5.8 +  moreover from `v \<in> A` assms(1) have "v \<sqsubseteq> u" by blast
     5.9    ultimately show ?thesis by (rule Inf_lower2)
    5.10  qed
    5.11  
    5.12 @@ -260,7 +260,7 @@
    5.13    shows "u \<sqsubseteq> \<Squnion>A"
    5.14  proof -
    5.15    from `A \<noteq> {}` obtain v where "v \<in> A" by blast
    5.16 -  moreover with assms have "u \<sqsubseteq> v" by blast
    5.17 +  moreover from `v \<in> A` assms(1) have "u \<sqsubseteq> v" by blast
    5.18    ultimately show ?thesis by (rule Sup_upper2)
    5.19  qed
    5.20  
     6.1 --- a/src/HOL/Complex.thy	Tue Sep 03 00:51:08 2013 +0200
     6.2 +++ b/src/HOL/Complex.thy	Tue Sep 03 01:12:40 2013 +0200
     6.3 @@ -707,11 +707,11 @@
     6.4        unfolding d_def by simp
     6.5      moreover from a assms have "cos a = cos x" and "sin a = sin x"
     6.6        by (simp_all add: complex_eq_iff)
     6.7 -    hence "cos d = 1" unfolding d_def cos_diff by simp
     6.8 -    moreover hence "sin d = 0" by (rule cos_one_sin_zero)
     6.9 +    hence cos: "cos d = 1" unfolding d_def cos_diff by simp
    6.10 +    moreover from cos have "sin d = 0" by (rule cos_one_sin_zero)
    6.11      ultimately have "d = 0"
    6.12        unfolding sin_zero_iff even_mult_two_ex
    6.13 -      by (safe, auto simp add: numeral_2_eq_2 less_Suc_eq)
    6.14 +      by (auto simp add: numeral_2_eq_2 less_Suc_eq)
    6.15      thus "a = x" unfolding d_def by simp
    6.16    qed (simp add: assms del: Re_sgn Im_sgn)
    6.17    with `z \<noteq> 0` show "arg z = x"
     7.1 --- a/src/HOL/Decision_Procs/Commutative_Ring_Complete.thy	Tue Sep 03 00:51:08 2013 +0200
     7.2 +++ b/src/HOL/Decision_Procs/Commutative_Ring_Complete.thy	Tue Sep 03 01:12:40 2013 +0200
     7.3 @@ -138,7 +138,6 @@
     7.4        by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2])
     7.5      moreover
     7.6      note 6 Y0
     7.7 -    moreover
     7.8      ultimately have ?case by (simp add: mkPinj_cn) }
     7.9    moreover
    7.10    { assume "x>y" hence "EX d. x = d + y" by arith
    7.11 @@ -286,7 +285,6 @@
    7.12      from 6 have "y>0" by (cases y) (auto simp add: norm_Pinj_0_False)
    7.13      moreover
    7.14      note 6
    7.15 -    moreover
    7.16      ultimately have ?case by (simp add: mkPinj_cn) }
    7.17    moreover
    7.18    { assume "x > y" hence "EX d. x = d + y" by arith
     8.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Tue Sep 03 00:51:08 2013 +0200
     8.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Tue Sep 03 01:12:40 2013 +0200
     8.3 @@ -2168,7 +2168,6 @@
     8.4        by(simp add: r[of "- (?t / (2*?c))"] msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
     8.5    }
     8.6    moreover
     8.7 -  moreover
     8.8    {assume c: "?c = 0" and d: "?d>0"  
     8.9      from d have d'': "2*?d > 0" by (simp add: zero_less_mult_iff)
    8.10      from d have d': "2*?d \<noteq> 0" by simp
    8.11 @@ -2314,7 +2313,6 @@
    8.12        by(simp add: r[of "- (?t / (2*?c))"] msubstle_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm)
    8.13    }
    8.14    moreover
    8.15 -  moreover
    8.16    {assume c: "?c = 0" and d: "?d>0"  
    8.17      from d have d'': "2*?d > 0" by (simp add: zero_less_mult_iff)
    8.18      from d have d': "2*?d \<noteq> 0" by simp
     9.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Tue Sep 03 00:51:08 2013 +0200
     9.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Tue Sep 03 01:12:40 2013 +0200
     9.3 @@ -1314,7 +1314,7 @@
     9.4          head_isnpolyh_Suc'[OF np norm(5)] head_isnpolyh_Suc'[OF np norm(6)[simplified nn']]
     9.5        have ?case by simp}
     9.6      moreover
     9.7 -    {moreover assume nz: "n = 0"
     9.8 +    { assume nz: "n = 0"
     9.9        from polymul_degreen[OF norm(5,4), where m="0"]
    9.10          polymul_degreen[OF norm(5,3), where m="0"] nn' nz degree_eq_degreen0
    9.11        norm(5,6) degree_npolyhCN[OF norm(6)]
    10.1 --- a/src/HOL/Deriv.thy	Tue Sep 03 00:51:08 2013 +0200
    10.2 +++ b/src/HOL/Deriv.thy	Tue Sep 03 01:12:40 2013 +0200
    10.3 @@ -416,10 +416,10 @@
    10.4    proof
    10.5      fix h show "F h = 0"
    10.6      proof (rule ccontr)
    10.7 -      assume "F h \<noteq> 0"
    10.8 -      moreover from this have h: "h \<noteq> 0"
    10.9 +      assume **: "F h \<noteq> 0"
   10.10 +      then have h: "h \<noteq> 0"
   10.11          by (clarsimp simp add: F.zero)
   10.12 -      ultimately have "0 < ?r h"
   10.13 +      with ** have "0 < ?r h"
   10.14          by (simp add: divide_pos_pos)
   10.15        from LIM_D [OF * this] obtain s where s: "0 < s"
   10.16          and r: "\<And>x. x \<noteq> 0 \<Longrightarrow> norm x < s \<Longrightarrow> ?r x < ?r h" by auto
   10.17 @@ -528,11 +528,11 @@
   10.18  lemma differentiable_def: "(f::real \<Rightarrow> real) differentiable x in s \<longleftrightarrow> (\<exists>D. DERIV f x : s :> D)"
   10.19  proof safe
   10.20    assume "f differentiable x in s"
   10.21 -  then obtain f' where "FDERIV f x : s :> f'"
   10.22 +  then obtain f' where *: "FDERIV f x : s :> f'"
   10.23      unfolding isDiff_def by auto
   10.24 -  moreover then obtain c where "f' = (\<lambda>x. x * c)"
   10.25 +  then obtain c where "f' = (\<lambda>x. x * c)"
   10.26      by (metis real_bounded_linear FDERIV_bounded_linear)
   10.27 -  ultimately show "\<exists>D. DERIV f x : s :> D"
   10.28 +  with * show "\<exists>D. DERIV f x : s :> D"
   10.29      unfolding deriv_fderiv by auto
   10.30  qed (auto simp: isDiff_def deriv_fderiv)
   10.31  
   10.32 @@ -730,8 +730,8 @@
   10.33      DERIV f x :> u \<longleftrightarrow> DERIV g y :> v"
   10.34    unfolding DERIV_iff2
   10.35  proof (rule filterlim_cong)
   10.36 -  assume "eventually (\<lambda>x. f x = g x) (nhds x)"
   10.37 -  moreover then have "f x = g x" by (auto simp: eventually_nhds)
   10.38 +  assume *: "eventually (\<lambda>x. f x = g x) (nhds x)"
   10.39 +  moreover from * have "f x = g x" by (auto simp: eventually_nhds)
   10.40    moreover assume "x = y" "u = v"
   10.41    ultimately show "eventually (\<lambda>xa. (f xa - f x) / (xa - x) = (g xa - g y) / (xa - y)) (at x)"
   10.42      by (auto simp: eventually_at_filter elim: eventually_elim1)
   10.43 @@ -1348,7 +1348,7 @@
   10.44  
   10.45    {
   10.46      from cdef have "?h b - ?h a = (b - a) * l" by auto
   10.47 -    also with leq have "\<dots> = (b - a) * (g'c * (f b - f a) - f'c * (g b - g a))" by simp
   10.48 +    also from leq have "\<dots> = (b - a) * (g'c * (f b - f a) - f'c * (g b - g a))" by simp
   10.49      finally have "?h b - ?h a = (b - a) * (g'c * (f b - f a) - f'c * (g b - g a))" by simp
   10.50    }
   10.51    moreover
   10.52 @@ -1458,9 +1458,10 @@
   10.53        using `isCont g 0` g by (auto intro: DERIV_isCont simp: le_less)
   10.54      ultimately have "\<exists>c. 0 < c \<and> c < x \<and> (f x - f 0) * g' c = (g x - g 0) * f' c"
   10.55        using f g `x < a` by (intro GMVT') auto
   10.56 -    then guess c ..
   10.57 +    then obtain c where *: "0 < c" "c < x" "(f x - f 0) * g' c = (g x - g 0) * f' c"
   10.58 +      by blast
   10.59      moreover
   10.60 -    with g'(1)[of c] g'(2) have "(f x - f 0)  / (g x - g 0) = f' c / g' c"
   10.61 +    from * g'(1)[of c] g'(2) have "(f x - f 0)  / (g x - g 0) = f' c / g' c"
   10.62        by (simp add: field_simps)
   10.63      ultimately show "\<exists>y. 0 < y \<and> y < x \<and> f x / g x = f' y / g' y"
   10.64        using `f 0 = 0` `g 0 = 0` by (auto intro!: exI[of _ c])
    11.1 --- a/src/HOL/Divides.thy	Tue Sep 03 00:51:08 2013 +0200
    11.2 +++ b/src/HOL/Divides.thy	Tue Sep 03 01:12:40 2013 +0200
    11.3 @@ -742,11 +742,11 @@
    11.4    apply (subst less_iff_Suc_add)
    11.5    apply (auto simp add: add_mult_distrib)
    11.6    done
    11.7 -  from `n \<noteq> 0` assms have "fst qr = fst qr'"
    11.8 +  from `n \<noteq> 0` assms have *: "fst qr = fst qr'"
    11.9      by (auto simp add: divmod_nat_rel_def intro: order_antisym dest: aux sym)
   11.10 -  moreover from this assms have "snd qr = snd qr'"
   11.11 +  with assms have "snd qr = snd qr'"
   11.12      by (simp add: divmod_nat_rel_def)
   11.13 -  ultimately show ?thesis by (cases qr, cases qr') simp
   11.14 +  with * show ?thesis by (cases qr, cases qr') simp
   11.15  qed
   11.16  
   11.17  text {*
    12.1 --- a/src/HOL/Fields.thy	Tue Sep 03 00:51:08 2013 +0200
    12.2 +++ b/src/HOL/Fields.thy	Tue Sep 03 01:12:40 2013 +0200
    12.3 @@ -919,8 +919,8 @@
    12.4    assume notless: "~ (0 < x)"
    12.5    have "~ (1 < inverse x)"
    12.6    proof
    12.7 -    assume "1 < inverse x"
    12.8 -    also with notless have "... \<le> 0" by simp
    12.9 +    assume *: "1 < inverse x"
   12.10 +    also from notless and * have "... \<le> 0" by simp
   12.11      also have "... < 1" by (rule zero_less_one) 
   12.12      finally show False by auto
   12.13    qed
    13.1 --- a/src/HOL/Finite_Set.thy	Tue Sep 03 00:51:08 2013 +0200
    13.2 +++ b/src/HOL/Finite_Set.thy	Tue Sep 03 01:12:40 2013 +0200
    13.3 @@ -1103,7 +1103,7 @@
    13.4  proof -
    13.5    from `x \<in> A` obtain B where A: "A = insert x B" and "x \<notin> B"
    13.6      by (auto dest: mk_disjoint_insert)
    13.7 -  moreover from `finite A` this have "finite B" by simp
    13.8 +  moreover from `finite A` A have "finite B" by simp
    13.9    ultimately show ?thesis by simp
   13.10  qed
   13.11  
    14.1 --- a/src/HOL/Imperative_HOL/Legacy_Mrec.thy	Tue Sep 03 00:51:08 2013 +0200
    14.2 +++ b/src/HOL/Imperative_HOL/Legacy_Mrec.thy	Tue Sep 03 01:12:40 2013 +0200
    14.3 @@ -118,7 +118,7 @@
    14.4          proof (cases "mrec b h1")
    14.5            case (Some result)
    14.6            then obtain aaa h2 where mrec_rec: "mrec b h1 = Some (aaa, h2)" by fastforce
    14.7 -          moreover from this have "P b h1 (snd (the (mrec b h1))) (fst (the (mrec b h1)))"
    14.8 +          moreover from mrec_rec have "P b h1 (snd (the (mrec b h1))) (fst (the (mrec b h1)))"
    14.9              apply (intro 1(2))
   14.10              apply (auto simp add: Inr Inl')
   14.11              done
    15.1 --- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Tue Sep 03 00:51:08 2013 +0200
    15.2 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Tue Sep 03 01:12:40 2013 +0200
    15.3 @@ -469,12 +469,12 @@
    15.4        assume pivot: "l \<le> p \<and> p \<le> r"
    15.5        assume i_outer: "i < l \<or> r < i"
    15.6        from  partition_outer_remains [OF part True] i_outer
    15.7 -      have "Array.get h a !i = Array.get h1 a ! i" by fastforce
    15.8 +      have 2: "Array.get h a !i = Array.get h1 a ! i" by fastforce
    15.9        moreover
   15.10 -      with 1(1) [OF True pivot qs1] pivot i_outer
   15.11 -      have "Array.get h1 a ! i = Array.get h2 a ! i" by auto
   15.12 +      from 1(1) [OF True pivot qs1] pivot i_outer 2
   15.13 +      have 3: "Array.get h1 a ! i = Array.get h2 a ! i" by auto
   15.14        moreover
   15.15 -      with qs2 1(2) [of p h2 h' ret2] True pivot i_outer
   15.16 +      from qs2 1(2) [of p h2 h' ret2] True pivot i_outer 3
   15.17        have "Array.get h2 a ! i = Array.get h' a ! i" by auto
   15.18        ultimately have "Array.get h a ! i= Array.get h' a ! i" by simp
   15.19      }
   15.20 @@ -604,9 +604,9 @@
   15.21    shows "success (f \<guillemotright>= g) h"
   15.22  using assms(1) proof (rule success_effectE)
   15.23    fix h' r
   15.24 -  assume "effect f h h' r"
   15.25 -  moreover with assms(2) have "success (g r) h'" .
   15.26 -  ultimately show "success (f \<guillemotright>= g) h" by (rule success_bind_effectI)
   15.27 +  assume *: "effect f h h' r"
   15.28 +  with assms(2) have "success (g r) h'" .
   15.29 +  with * show "success (f \<guillemotright>= g) h" by (rule success_bind_effectI)
   15.30  qed
   15.31  
   15.32  lemma success_partitionI:
    16.1 --- a/src/HOL/Imperative_HOL/ex/Sublist.thy	Tue Sep 03 00:51:08 2013 +0200
    16.2 +++ b/src/HOL/Imperative_HOL/ex/Sublist.thy	Tue Sep 03 01:12:40 2013 +0200
    16.3 @@ -490,7 +490,6 @@
    16.4    moreover
    16.5    from right l_r length_eq have "sublist' r (List.length xs) xs = sublist' r (List.length ys) ys"
    16.6      by (auto simp add: length_sublist' nth_sublist' intro!: nth_equalityI)
    16.7 -  moreover
    16.8    ultimately show ?thesis by (simp add: multiset_of_append)
    16.9  qed
   16.10  
    17.1 --- a/src/HOL/Library/Extended_Real.thy	Tue Sep 03 00:51:08 2013 +0200
    17.2 +++ b/src/HOL/Library/Extended_Real.thy	Tue Sep 03 01:12:40 2013 +0200
    17.3 @@ -146,11 +146,11 @@
    17.4  "-\<infinity> + -\<infinity> = -(\<infinity>::ereal)"
    17.5  proof -
    17.6    case (goal1 P x)
    17.7 -  moreover then obtain a b where "x = (a, b)" by (cases x) auto
    17.8 -  ultimately show P
    17.9 +  then obtain a b where "x = (a, b)" by (cases x) auto
   17.10 +  with goal1 show P
   17.11     by (cases rule: ereal2_cases[of a b]) auto
   17.12  qed auto
   17.13 -termination proof qed (rule wf_empty)
   17.14 +termination by default (rule wf_empty)
   17.15  
   17.16  lemma Infty_neq_0[simp]:
   17.17    "(\<infinity>::ereal) \<noteq> 0" "0 \<noteq> (\<infinity>::ereal)"
   17.18 @@ -234,8 +234,8 @@
   17.19  | "        -\<infinity> < (\<infinity>::ereal) \<longleftrightarrow> True"
   17.20  proof -
   17.21    case (goal1 P x)
   17.22 -  moreover then obtain a b where "x = (a,b)" by (cases x) auto
   17.23 -  ultimately show P by (cases rule: ereal2_cases[of a b]) auto
   17.24 +  then obtain a b where "x = (a,b)" by (cases x) auto
   17.25 +  with goal1 show P by (cases rule: ereal2_cases[of a b]) auto
   17.26  qed simp_all
   17.27  termination by (relation "{}") simp
   17.28  
   17.29 @@ -496,8 +496,8 @@
   17.30  "-(\<infinity>::ereal) * -\<infinity> = \<infinity>"
   17.31  proof -
   17.32    case (goal1 P x)
   17.33 -  moreover then obtain a b where "x = (a, b)" by (cases x) auto
   17.34 -  ultimately show P by (cases rule: ereal2_cases[of a b]) auto
   17.35 +  then obtain a b where "x = (a, b)" by (cases x) auto
   17.36 +  with goal1 show P by (cases rule: ereal2_cases[of a b]) auto
   17.37  qed simp_all
   17.38  termination by (relation "{}") simp
   17.39  
   17.40 @@ -1338,9 +1338,9 @@
   17.41    next
   17.42      { assume "c = \<infinity>" have ?thesis
   17.43        proof cases
   17.44 -        assume "\<forall>i. f i = 0"
   17.45 -        moreover then have "range f = {0}" by auto
   17.46 -        ultimately show "c * SUPR UNIV f \<le> y" using *
   17.47 +        assume **: "\<forall>i. f i = 0"
   17.48 +        then have "range f = {0}" by auto
   17.49 +        with ** show "c * SUPR UNIV f \<le> y" using *
   17.50            by (auto simp: SUP_def min_max.sup_absorb1)
   17.51        next
   17.52          assume "\<not> (\<forall>i. f i = 0)"
   17.53 @@ -1417,9 +1417,9 @@
   17.54    from `A \<noteq> {}` obtain x where "x \<in> A" by auto
   17.55    show ?thesis
   17.56    proof cases
   17.57 -    assume "\<infinity> \<in> A"
   17.58 -    moreover then have "\<infinity> \<le> Sup A" by (intro complete_lattice_class.Sup_upper)
   17.59 -    ultimately show ?thesis by (auto intro!: exI[of _ "\<lambda>x. \<infinity>"])
   17.60 +    assume *: "\<infinity> \<in> A"
   17.61 +    then have "\<infinity> \<le> Sup A" by (intro complete_lattice_class.Sup_upper)
   17.62 +    with * show ?thesis by (auto intro!: exI[of _ "\<lambda>x. \<infinity>"])
   17.63    next
   17.64      assume "\<infinity> \<notin> A"
   17.65      have "\<exists>x\<in>A. 0 \<le> x"
   17.66 @@ -1489,10 +1489,13 @@
   17.67    fixes A :: "ereal set" assumes "A \<noteq> {}" and "\<bar>a\<bar> \<noteq> \<infinity>"
   17.68    shows "Inf ((\<lambda>x. a - x) ` A) = a - Sup A"
   17.69  proof -
   17.70 -  { fix x have "-a - -x = -(a - x)" using assms by (cases x) auto }
   17.71 -  moreover then have "(\<lambda>x. -a - x)`uminus`A = uminus ` (\<lambda>x. a - x) ` A"
   17.72 +  {
   17.73 +    fix x
   17.74 +    have "-a - -x = -(a - x)" using assms by (cases x) auto
   17.75 +  } note * = this
   17.76 +  then have "(\<lambda>x. -a - x)`uminus`A = uminus ` (\<lambda>x. a - x) ` A"
   17.77      by (auto simp: image_image)
   17.78 -  ultimately show ?thesis
   17.79 +  with * show ?thesis
   17.80      using Sup_ereal_cminus[of "uminus ` A" "-a"] assms
   17.81      by (auto simp add: ereal_Sup_uminus_image_eq ereal_Inf_uminus_image_eq)
   17.82  qed
   17.83 @@ -1606,9 +1609,9 @@
   17.84    unfolding open_ereal_generated
   17.85  proof (induct rule: generate_topology.induct)
   17.86    case (Int A B)
   17.87 -  moreover then obtain x z where "\<infinity> \<in> A \<Longrightarrow> {ereal x <..} \<subseteq> A" "\<infinity> \<in> B \<Longrightarrow> {ereal z <..} \<subseteq> B"
   17.88 -      by auto
   17.89 -  ultimately show ?case
   17.90 +  then obtain x z where "\<infinity> \<in> A \<Longrightarrow> {ereal x <..} \<subseteq> A" "\<infinity> \<in> B \<Longrightarrow> {ereal z <..} \<subseteq> B"
   17.91 +    by auto
   17.92 +  with Int show ?case
   17.93      by (intro exI[of _ "max x z"]) fastforce
   17.94  next
   17.95    { fix x have "x \<noteq> \<infinity> \<Longrightarrow> \<exists>t. x \<le> ereal t" by (cases x) auto }
   17.96 @@ -1621,9 +1624,9 @@
   17.97    unfolding open_ereal_generated
   17.98  proof (induct rule: generate_topology.induct)
   17.99    case (Int A B)
  17.100 -  moreover then obtain x z where "-\<infinity> \<in> A \<Longrightarrow> {..< ereal x} \<subseteq> A" "-\<infinity> \<in> B \<Longrightarrow> {..< ereal z} \<subseteq> B"
  17.101 -      by auto
  17.102 -  ultimately show ?case
  17.103 +  then obtain x z where "-\<infinity> \<in> A \<Longrightarrow> {..< ereal x} \<subseteq> A" "-\<infinity> \<in> B \<Longrightarrow> {..< ereal z} \<subseteq> B"
  17.104 +    by auto
  17.105 +  with Int show ?case
  17.106      by (intro exI[of _ "min x z"]) fastforce
  17.107  next
  17.108    { fix x have "x \<noteq> - \<infinity> \<Longrightarrow> \<exists>t. ereal t \<le> x" by (cases x) auto }
    18.1 --- a/src/HOL/Library/FinFun.thy	Tue Sep 03 00:51:08 2013 +0200
    18.2 +++ b/src/HOL/Library/FinFun.thy	Tue Sep 03 01:12:40 2013 +0200
    18.3 @@ -960,7 +960,7 @@
    18.4      { fix g' a b show "Abs_finfun (g \<circ> op $ g'(a $:= b)) = (Abs_finfun (g \<circ> op $ g'))(a $:= g b)"
    18.5        proof -
    18.6          obtain y where y: "y \<in> finfun" and g': "g' = Abs_finfun y" by(cases g')
    18.7 -        moreover hence "(g \<circ> op $ g') \<in> finfun" by(simp add: finfun_left_compose)
    18.8 +        moreover from g' have "(g \<circ> op $ g') \<in> finfun" by(simp add: finfun_left_compose)
    18.9          moreover have "g \<circ> y(a := b) = (g \<circ> y)(a := g b)" by(auto)
   18.10          ultimately show ?thesis by(simp add: finfun_comp_def finfun_update_def)
   18.11        qed }
    19.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Tue Sep 03 00:51:08 2013 +0200
    19.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Tue Sep 03 01:12:40 2013 +0200
    19.3 @@ -3804,8 +3804,8 @@
    19.4      by (simp add: split_if_asm dist_fps_def)
    19.5    moreover
    19.6    from fps_eq_least_unique[OF `f \<noteq> g`]
    19.7 -  obtain n where "leastP (\<lambda>n. f$n \<noteq> g$n) n" "The (leastP (\<lambda>n. f $ n \<noteq> g $ n)) = n" by blast
    19.8 -  moreover hence "\<And>m. m < n \<Longrightarrow> f$m = g$m" "f$n \<noteq> g$n"
    19.9 +  obtain n where n: "leastP (\<lambda>n. f$n \<noteq> g$n) n" "The (leastP (\<lambda>n. f $ n \<noteq> g $ n)) = n" by blast
   19.10 +  moreover from n have "\<And>m. m < n \<Longrightarrow> f$m = g$m" "f$n \<noteq> g$n"
   19.11      by (auto simp add: leastP_def setge_def)
   19.12    ultimately show ?thesis using `j \<le> i` by simp
   19.13  next
    20.1 --- a/src/HOL/Library/Fraction_Field.thy	Tue Sep 03 00:51:08 2013 +0200
    20.2 +++ b/src/HOL/Library/Fraction_Field.thy	Tue Sep 03 01:12:40 2013 +0200
    20.3 @@ -209,7 +209,7 @@
    20.4  next
    20.5    case False
    20.6    then obtain a b where "q = Fract a b" and "b \<noteq> 0" by (cases q) auto
    20.7 -  moreover with False have "0 \<noteq> Fract a b" by simp
    20.8 +  with False have "0 \<noteq> Fract a b" by simp
    20.9    with `b \<noteq> 0` have "a \<noteq> 0" by (simp add: Zero_fract_def eq_fract)
   20.10    with Fract `q = Fract a b` `b \<noteq> 0` show thesis by auto
   20.11  qed
    21.1 --- a/src/HOL/Library/Liminf_Limsup.thy	Tue Sep 03 00:51:08 2013 +0200
    21.2 +++ b/src/HOL/Library/Liminf_Limsup.thy	Tue Sep 03 01:12:40 2013 +0200
    21.3 @@ -171,8 +171,8 @@
    21.4      have "\<exists>P. eventually P F \<and> y < INFI (Collect P) X"
    21.5      proof cases
    21.6        assume "\<exists>z. y < z \<and> z < C"
    21.7 -      then guess z ..
    21.8 -      moreover then have "z \<le> INFI {x. z < X x} X"
    21.9 +      then guess z .. note z = this
   21.10 +      moreover from z have "z \<le> INFI {x. z < X x} X"
   21.11          by (auto intro!: INF_greatest)
   21.12        ultimately show ?thesis
   21.13          using y by (intro exI[of _ "\<lambda>x. z < X x"]) auto
   21.14 @@ -203,7 +203,7 @@
   21.15    show "f0 \<le> y"
   21.16    proof cases
   21.17      assume "\<exists>z. y < z \<and> z < f0"
   21.18 -    then guess z ..
   21.19 +    then obtain z where "y < z \<and> z < f0" ..
   21.20      moreover have "z \<le> INFI {x. z < f x} f"
   21.21        by (rule INF_greatest) simp
   21.22      ultimately show ?thesis
    22.1 --- a/src/HOL/Library/Permutations.thy	Tue Sep 03 00:51:08 2013 +0200
    22.2 +++ b/src/HOL/Library/Permutations.thy	Tue Sep 03 01:12:40 2013 +0200
    22.3 @@ -166,8 +166,8 @@
    22.4      have xfgpF': "?xF = ?g ` ?pF'" .
    22.5      have Fs: "card F = n - 1" using `x \<notin> F` H0 `finite F` by auto
    22.6      from insert.hyps Fs have pFs: "card ?pF = fact (n - 1)" using `finite F` by auto
    22.7 -    moreover hence "finite ?pF" using fact_gt_zero_nat by (auto intro: card_ge_0_finite)
    22.8 -    ultimately have pF'f: "finite ?pF'" using H0 `finite F`
    22.9 +    then have "finite ?pF" using fact_gt_zero_nat by (auto intro: card_ge_0_finite)
   22.10 +    then have pF'f: "finite ?pF'" using H0 `finite F`
   22.11        apply (simp only: Collect_split Collect_mem_eq)
   22.12        apply (rule finite_cartesian_product)
   22.13        apply simp_all
   22.14 @@ -195,7 +195,7 @@
   22.15        thus ?thesis  unfolding inj_on_def by blast
   22.16      qed
   22.17      from `x \<notin> F` H0 have n0: "n \<noteq> 0 " using `finite F` by auto
   22.18 -    hence "\<exists>m. n = Suc m" by arith
   22.19 +    hence "\<exists>m. n = Suc m" by presburger
   22.20      then obtain m where n[simp]: "n = Suc m" by blast
   22.21      from pFs H0 have xFc: "card ?xF = fact n"
   22.22        unfolding xfgpF' card_image[OF ginj] using `finite F` `finite ?pF`
    23.1 --- a/src/HOL/Library/RBT_Impl.thy	Tue Sep 03 00:51:08 2013 +0200
    23.2 +++ b/src/HOL/Library/RBT_Impl.thy	Tue Sep 03 01:12:40 2013 +0200
    23.3 @@ -146,8 +146,7 @@
    23.4      = Set.insert k (dom (rbt_lookup t1) \<union> dom (rbt_lookup t2))"
    23.5  proof -
    23.6    assume "rbt_sorted (Branch c t1 k v t2)"
    23.7 -  moreover from this have "rbt_sorted t1" "rbt_sorted t2" by simp_all
    23.8 -  ultimately show ?thesis by (simp add: rbt_lookup_keys)
    23.9 +  then show ?thesis by (simp add: rbt_lookup_keys)
   23.10  qed
   23.11  
   23.12  lemma finite_dom_rbt_lookup [simp, intro!]: "finite (dom (rbt_lookup t))"
   23.13 @@ -1405,14 +1404,14 @@
   23.14        proof(cases "n mod 2 = 0")
   23.15          case True note ge0 
   23.16          moreover from "1.prems" have n2: "n div 2 \<le> length kvs" by simp
   23.17 -        moreover with True have "P (n div 2) kvs" by(rule IH)
   23.18 +        moreover from True n2 have "P (n div 2) kvs" by(rule IH)
   23.19          moreover from length_rbtreeify_f[OF n2] ge0 "1.prems" obtain t k v kvs' 
   23.20            where kvs': "rbtreeify_f (n div 2) kvs = (t, (k, v) # kvs')"
   23.21            by(cases "snd (rbtreeify_f (n div 2) kvs)")
   23.22              (auto simp add: snd_def split: prod.split_asm)
   23.23          moreover from "1.prems" length_rbtreeify_f[OF n2] ge0
   23.24 -        have "n div 2 \<le> Suc (length kvs')" by(simp add: kvs')
   23.25 -        moreover with True kvs'[symmetric] refl refl
   23.26 +        have n2': "n div 2 \<le> Suc (length kvs')" by(simp add: kvs')
   23.27 +        moreover from True kvs'[symmetric] refl refl n2'
   23.28          have "Q (n div 2) kvs'" by(rule IH)
   23.29          moreover note feven[unfolded feven_def]
   23.30            (* FIXME: why does by(rule feven[unfolded feven_def]) not work? *)
   23.31 @@ -1421,14 +1420,14 @@
   23.32        next
   23.33          case False note ge0
   23.34          moreover from "1.prems" have n2: "n div 2 \<le> length kvs" by simp
   23.35 -        moreover with False have "P (n div 2) kvs" by(rule IH)
   23.36 +        moreover from False n2 have "P (n div 2) kvs" by(rule IH)
   23.37          moreover from length_rbtreeify_f[OF n2] ge0 "1.prems" obtain t k v kvs' 
   23.38            where kvs': "rbtreeify_f (n div 2) kvs = (t, (k, v) # kvs')"
   23.39            by(cases "snd (rbtreeify_f (n div 2) kvs)")
   23.40              (auto simp add: snd_def split: prod.split_asm)
   23.41          moreover from "1.prems" length_rbtreeify_f[OF n2] ge0 False
   23.42 -        have "n div 2 \<le> length kvs'" by(simp add: kvs') arith
   23.43 -        moreover with False kvs'[symmetric] refl refl have "P (n div 2) kvs'" by(rule IH)
   23.44 +        have n2': "n div 2 \<le> length kvs'" by(simp add: kvs') arith
   23.45 +        moreover from False kvs'[symmetric] refl refl n2' have "P (n div 2) kvs'" by(rule IH)
   23.46          moreover note fodd[unfolded fodd_def]
   23.47          ultimately have "P (Suc (2 * (n div 2))) kvs" by -
   23.48          thus ?thesis using False 
   23.49 @@ -1451,14 +1450,14 @@
   23.50        proof(cases "n mod 2 = 0")
   23.51          case True note ge0
   23.52          moreover from "2.prems" have n2: "n div 2 \<le> Suc (length kvs)" by simp
   23.53 -        moreover with True have "Q (n div 2) kvs" by(rule IH)
   23.54 +        moreover from True n2 have "Q (n div 2) kvs" by(rule IH)
   23.55          moreover from length_rbtreeify_g[OF ge0 n2] ge0 "2.prems" obtain t k v kvs' 
   23.56            where kvs': "rbtreeify_g (n div 2) kvs = (t, (k, v) # kvs')"
   23.57            by(cases "snd (rbtreeify_g (n div 2) kvs)")
   23.58              (auto simp add: snd_def split: prod.split_asm)
   23.59          moreover from "2.prems" length_rbtreeify_g[OF ge0 n2] ge0
   23.60 -        have "n div 2 \<le> Suc (length kvs')" by(simp add: kvs')
   23.61 -        moreover with True kvs'[symmetric] refl refl 
   23.62 +        have n2': "n div 2 \<le> Suc (length kvs')" by(simp add: kvs')
   23.63 +        moreover from True kvs'[symmetric] refl refl  n2'
   23.64          have "Q (n div 2) kvs'" by(rule IH)
   23.65          moreover note geven[unfolded geven_def]
   23.66          ultimately have "Q (2 * (n div 2)) kvs" by -
   23.67 @@ -1467,14 +1466,14 @@
   23.68        next
   23.69          case False note ge0
   23.70          moreover from "2.prems" have n2: "n div 2 \<le> length kvs" by simp
   23.71 -        moreover with False have "P (n div 2) kvs" by(rule IH)
   23.72 +        moreover from False n2 have "P (n div 2) kvs" by(rule IH)
   23.73          moreover from length_rbtreeify_f[OF n2] ge0 "2.prems" False obtain t k v kvs' 
   23.74            where kvs': "rbtreeify_f (n div 2) kvs = (t, (k, v) # kvs')"
   23.75            by(cases "snd (rbtreeify_f (n div 2) kvs)")
   23.76              (auto simp add: snd_def split: prod.split_asm, arith)
   23.77          moreover from "2.prems" length_rbtreeify_f[OF n2] ge0 False
   23.78 -        have "n div 2 \<le> Suc (length kvs')" by(simp add: kvs') arith
   23.79 -        moreover with False kvs'[symmetric] refl refl
   23.80 +        have n2': "n div 2 \<le> Suc (length kvs')" by(simp add: kvs') arith
   23.81 +        moreover from False kvs'[symmetric] refl refl n2'
   23.82          have "Q (n div 2) kvs'" by(rule IH)
   23.83          moreover note godd[unfolded godd_def]
   23.84          ultimately have "Q (Suc (2 * (n div 2))) kvs" by -
    24.1 --- a/src/HOL/Library/Ramsey.thy	Tue Sep 03 00:51:08 2013 +0200
    24.2 +++ b/src/HOL/Library/Ramsey.thy	Tue Sep 03 01:12:40 2013 +0200
    24.3 @@ -326,11 +326,11 @@
    24.4    have part2: "\<forall>X. X \<subseteq> Z & finite X & card X = 2 --> f X < s"
    24.5      using part by (fastforce simp add: eval_nat_numeral card_Suc_eq)
    24.6    obtain Y t
    24.7 -    where "Y \<subseteq> Z" "infinite Y" "t < s"
    24.8 +    where *: "Y \<subseteq> Z" "infinite Y" "t < s"
    24.9            "(\<forall>X. X \<subseteq> Y & finite X & card X = 2 --> f X = t)"
   24.10      by (insert Ramsey [OF infZ part2]) auto
   24.11 -  moreover from this have  "\<forall>x\<in>Y. \<forall>y\<in>Y. x \<noteq> y \<longrightarrow> f {x, y} = t" by auto
   24.12 -  ultimately show ?thesis by iprover
   24.13 +  then have "\<forall>x\<in>Y. \<forall>y\<in>Y. x \<noteq> y \<longrightarrow> f {x, y} = t" by auto
   24.14 +  with * show ?thesis by iprover
   24.15  qed
   24.16  
   24.17  
    25.1 --- a/src/HOL/Library/Zorn.thy	Tue Sep 03 00:51:08 2013 +0200
    25.2 +++ b/src/HOL/Library/Zorn.thy	Tue Sep 03 01:12:40 2013 +0200
    25.3 @@ -119,9 +119,9 @@
    25.4  lemma chain_sucD:
    25.5    assumes "chain X" shows "suc X \<subseteq> A \<and> chain (suc X)"
    25.6  proof -
    25.7 -  from `chain X` have "chain (suc X)" by (rule chain_suc)
    25.8 -  moreover then have "suc X \<subseteq> A" unfolding chain_def by blast
    25.9 -  ultimately show ?thesis by blast
   25.10 +  from `chain X` have *: "chain (suc X)" by (rule chain_suc)
   25.11 +  then have "suc X \<subseteq> A" unfolding chain_def by blast
   25.12 +  with * show ?thesis by blast
   25.13  qed
   25.14  
   25.15  lemma suc_Union_closed_total':
   25.16 @@ -348,8 +348,8 @@
   25.17    moreover have "\<forall>x\<in>C. x \<subseteq> X" using `\<Union>C \<subseteq> X` by auto
   25.18    ultimately have "subset.chain A ?C"
   25.19      using subset.chain_extend [of A C X] and `X \<in> A` by auto
   25.20 -  moreover assume "\<Union>C \<noteq> X"
   25.21 -  moreover then have "C \<subset> ?C" using `\<Union>C \<subseteq> X` by auto
   25.22 +  moreover assume **: "\<Union>C \<noteq> X"
   25.23 +  moreover from ** have "C \<subset> ?C" using `\<Union>C \<subseteq> X` by auto
   25.24    ultimately show False using * by blast
   25.25  qed
   25.26  
   25.27 @@ -578,11 +578,11 @@
   25.28        case 0 show ?case by fact
   25.29      next
   25.30        case (Suc i)
   25.31 -      moreover obtain s where "s \<in> R" and "(f (Suc (Suc i)), f(Suc i)) \<in> s"
   25.32 +      then obtain s where s: "s \<in> R" "(f (Suc (Suc i)), f(Suc i)) \<in> s"
   25.33          using 1 by auto
   25.34 -      moreover hence "s initial_segment_of r \<or> r initial_segment_of s"
   25.35 +      then have "s initial_segment_of r \<or> r initial_segment_of s"
   25.36          using assms(1) `r \<in> R` by (simp add: Chains_def)
   25.37 -      ultimately show ?case by (simp add: init_seg_of_def) blast
   25.38 +      with Suc s show ?case by (simp add: init_seg_of_def) blast
   25.39      qed
   25.40    }
   25.41    thus False using assms(2) and `r \<in> R`
   25.42 @@ -682,15 +682,14 @@
   25.43      qed
   25.44      ultimately have "Well_order ?m" by (simp add: order_on_defs)
   25.45  --{*We show that the extension is above m*}
   25.46 -    moreover hence "(m, ?m) \<in> I" using `Well_order m` and `x \<notin> Field m`
   25.47 +    moreover have "(m, ?m) \<in> I" using `Well_order ?m` and `Well_order m` and `x \<notin> Field m`
   25.48        by (fastforce simp: I_def init_seg_of_def Field_def)
   25.49      ultimately
   25.50  --{*This contradicts maximality of m:*}
   25.51      have False using max and `x \<notin> Field m` unfolding Field_def by blast
   25.52    }
   25.53    hence "Field m = UNIV" by auto
   25.54 -  moreover with `Well_order m` have "Well_order m" by simp
   25.55 -  ultimately show ?thesis by blast
   25.56 +  with `Well_order m` show ?thesis by blast
   25.57  qed
   25.58  
   25.59  corollary well_order_on: "\<exists>r::'a rel. well_order_on A r"
    26.1 --- a/src/HOL/List.thy	Tue Sep 03 00:51:08 2013 +0200
    26.2 +++ b/src/HOL/List.thy	Tue Sep 03 01:12:40 2013 +0200
    26.3 @@ -722,12 +722,18 @@
    26.4  using `xs \<noteq> []` proof (induct xs)
    26.5    case Nil then show ?case by simp
    26.6  next
    26.7 -  case (Cons x xs) show ?case proof (cases xs)
    26.8 -    case Nil with single show ?thesis by simp
    26.9 +  case (Cons x xs)
   26.10 +  show ?case
   26.11 +  proof (cases xs)
   26.12 +    case Nil
   26.13 +    with single show ?thesis by simp
   26.14    next
   26.15 -    case Cons then have "xs \<noteq> []" by simp
   26.16 -    moreover with Cons.hyps have "P xs" .
   26.17 -    ultimately show ?thesis by (rule cons)
   26.18 +    case Cons
   26.19 +    show ?thesis
   26.20 +    proof (rule cons)
   26.21 +      from Cons show "xs \<noteq> []" by simp
   26.22 +      with Cons.hyps show "P xs" .
   26.23 +    qed
   26.24    qed
   26.25  qed
   26.26  
   26.27 @@ -1061,12 +1067,13 @@
   26.28  lemma map_eq_imp_length_eq:
   26.29    assumes "map f xs = map g ys"
   26.30    shows "length xs = length ys"
   26.31 -using assms proof (induct ys arbitrary: xs)
   26.32 +  using assms
   26.33 +proof (induct ys arbitrary: xs)
   26.34    case Nil then show ?case by simp
   26.35  next
   26.36    case (Cons y ys) then obtain z zs where xs: "xs = z # zs" by auto
   26.37    from Cons xs have "map f zs = map g ys" by simp
   26.38 -  moreover with Cons have "length zs = length ys" by blast
   26.39 +  with Cons have "length zs = length ys" by blast
   26.40    with xs show ?case by simp
   26.41  qed
   26.42    
   26.43 @@ -1669,10 +1676,10 @@
   26.44    hence n: "n < Suc (length xs)" by simp
   26.45    moreover
   26.46    { assume "n < length xs"
   26.47 -    with n obtain n' where "length xs - n = Suc n'"
   26.48 +    with n obtain n' where n': "length xs - n = Suc n'"
   26.49        by (cases "length xs - n", auto)
   26.50      moreover
   26.51 -    then have "length xs - Suc n = n'" by simp
   26.52 +    from n' have "length xs - Suc n = n'" by simp
   26.53      ultimately
   26.54      have "xs ! (length xs - Suc n) = (x # xs) ! (length xs - n)" by simp
   26.55    }
   26.56 @@ -3801,14 +3808,12 @@
   26.57      then have "\<exists>m n zs. concat (replicate m zs) = xs' \<and> concat (replicate n zs) = ws"
   26.58        using False and `xs' \<noteq> []` and `ys' = xs' @ ws` and len
   26.59        by (intro less.hyps) auto
   26.60 -    then obtain m n zs where "concat (replicate m zs) = xs'"
   26.61 +    then obtain m n zs where *: "concat (replicate m zs) = xs'"
   26.62        and "concat (replicate n zs) = ws" by blast
   26.63 -    moreover
   26.64      then have "concat (replicate (m + n) zs) = ys'"
   26.65        using `ys' = xs' @ ws`
   26.66        by (simp add: replicate_add)
   26.67 -    ultimately
   26.68 -    show ?thesis by blast
   26.69 +    with * show ?thesis by blast
   26.70    qed
   26.71    then show ?case
   26.72      using xs'_def ys'_def by metis
   26.73 @@ -4074,8 +4079,8 @@
   26.74    case Nil thus ?case by simp
   26.75  next
   26.76    case (Cons a xs)
   26.77 -  moreover hence "!x. x: set xs \<longrightarrow> x \<noteq> a" by auto
   26.78 -  ultimately show ?case by(simp add: sublist_Cons cong:filter_cong)
   26.79 +  then have "!x. x: set xs \<longrightarrow> x \<noteq> a" by auto
   26.80 +  with Cons show ?case by(simp add: sublist_Cons cong:filter_cong)
   26.81  qed
   26.82  
   26.83  
   26.84 @@ -4195,8 +4200,8 @@
   26.85    hence "foldr (\<lambda>xs. max (length xs)) xss 0 = 0"
   26.86    proof (induct xss)
   26.87      case (Cons x xs)
   26.88 -    moreover hence "x = []" by (cases x) auto
   26.89 -    ultimately show ?case by auto
   26.90 +    then have "x = []" by (cases x) auto
   26.91 +    with Cons show ?case by auto
   26.92    qed simp
   26.93    thus ?thesis using True by simp
   26.94  next
   26.95 @@ -4585,7 +4590,7 @@
   26.96  proof -
   26.97    from assms have "map f xs = map f ys"
   26.98      by (simp add: sorted_distinct_set_unique)
   26.99 -  moreover with `inj_on f (set xs \<union> set ys)` show "xs = ys"
  26.100 +  with `inj_on f (set xs \<union> set ys)` show "xs = ys"
  26.101      by (blast intro: map_inj_on)
  26.102  qed
  26.103  
  26.104 @@ -4620,11 +4625,12 @@
  26.105  lemma foldr_max_sorted:
  26.106    assumes "sorted (rev xs)"
  26.107    shows "foldr max xs y = (if xs = [] then y else max (xs ! 0) y)"
  26.108 -using assms proof (induct xs)
  26.109 +  using assms
  26.110 +proof (induct xs)
  26.111    case (Cons x xs)
  26.112 -  moreover hence "sorted (rev xs)" using sorted_append by auto
  26.113 -  ultimately show ?case
  26.114 -    by (cases xs, auto simp add: sorted_append max_def)
  26.115 +  then have "sorted (rev xs)" using sorted_append by auto
  26.116 +  with Cons show ?case
  26.117 +    by (cases xs) (auto simp add: sorted_append max_def)
  26.118  qed simp
  26.119  
  26.120  lemma filter_equals_takeWhile_sorted_rev:
    27.1 --- a/src/HOL/Map.thy	Tue Sep 03 00:51:08 2013 +0200
    27.2 +++ b/src/HOL/Map.thy	Tue Sep 03 01:12:40 2013 +0200
    27.3 @@ -715,18 +715,19 @@
    27.4      by (rule set_map_of_compr)
    27.5    ultimately show ?rhs by simp
    27.6  next
    27.7 -  assume ?rhs show ?lhs proof
    27.8 +  assume ?rhs show ?lhs
    27.9 +  proof
   27.10      fix k
   27.11      show "map_of xs k = map_of ys k" proof (cases "map_of xs k")
   27.12        case None
   27.13 -      moreover with `?rhs` have "map_of ys k = None"
   27.14 +      with `?rhs` have "map_of ys k = None"
   27.15          by (simp add: map_of_eq_None_iff)
   27.16 -      ultimately show ?thesis by simp
   27.17 +      with None show ?thesis by simp
   27.18      next
   27.19        case (Some v)
   27.20 -      moreover with distinct `?rhs` have "map_of ys k = Some v"
   27.21 +      with distinct `?rhs` have "map_of ys k = Some v"
   27.22          by simp
   27.23 -      ultimately show ?thesis by simp
   27.24 +      with Some show ?thesis by simp
   27.25      qed
   27.26    qed
   27.27  qed
    28.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Tue Sep 03 00:51:08 2013 +0200
    28.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Tue Sep 03 01:12:40 2013 +0200
    28.3 @@ -144,8 +144,8 @@
    28.4        where "class": "class G C = Some (D', fs', ms')"
    28.5        unfolding class_def by(auto dest!: weak_map_of_SomeI)
    28.6      hence "G \<turnstile> C \<prec>C1 D'" using `C \<noteq> Object` ..
    28.7 -    hence "(C, D') \<in> (subcls1 G)^+" ..
    28.8 -    also with acyc have "C \<noteq> D'" by(auto simp add: acyclic_def)
    28.9 +    hence *: "(C, D') \<in> (subcls1 G)^+" ..
   28.10 +    also from * acyc have "C \<noteq> D'" by(auto simp add: acyclic_def)
   28.11      with subcls "class" have "(D', C) \<in> (subcls1 G)^+" by(auto dest: rtranclD)
   28.12      finally show False using acyc by(auto simp add: acyclic_def)
   28.13    qed
    29.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Tue Sep 03 00:51:08 2013 +0200
    29.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Tue Sep 03 01:12:40 2013 +0200
    29.3 @@ -2743,10 +2743,10 @@
    29.4      using subspace_substandard[of "\<lambda>i. i \<notin> d"] .
    29.5    ultimately have "span d \<subseteq> ?B"
    29.6      using span_mono[of d "?B"] span_eq[of "?B"] by blast
    29.7 -  moreover have "card d \<le> dim (span d)"
    29.8 +  moreover have *: "card d \<le> dim (span d)"
    29.9      using independent_card_le_dim[of d "span d"] independent_substdbasis[OF assms] span_inc[of d]
   29.10      by auto
   29.11 -  moreover then have "dim ?B \<le> dim (span d)"
   29.12 +  moreover from * have "dim ?B \<le> dim (span d)"
   29.13      using dim_substandard[OF assms] by auto
   29.14    ultimately show ?thesis
   29.15      using s subspace_dim_equal[of "span d" "?B"] subspace_span[of d] by auto
   29.16 @@ -8604,7 +8604,7 @@
   29.17    { fix i assume "i:I"
   29.18      { assume "e i = 0"
   29.19        have ge: "u * (c i) >= 0 & v * (d i) >= 0" using xc yc uv `i:I` by (simp add: mult_nonneg_nonneg)
   29.20 -      moreover hence "u * (c i) <= 0 & v * (d i) <= 0" using `e i = 0` e_def `i:I` by simp
   29.21 +      moreover from ge have "u * (c i) <= 0 & v * (d i) <= 0" using `e i = 0` e_def `i:I` by simp
   29.22        ultimately have "u * (c i) = 0 & v * (d i) = 0" by auto
   29.23        hence "(u * (c i))*\<^sub>R (s i)+(v * (d i))*\<^sub>R (t i) = (e i) *\<^sub>R (q i)"
   29.24           using `e i = 0` by auto
    30.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Tue Sep 03 00:51:08 2013 +0200
    30.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Tue Sep 03 01:12:40 2013 +0200
    30.3 @@ -1441,14 +1441,14 @@
    30.4    have *:"(\<lambda>x. x *\<^sub>R f') = (\<lambda>x. x *\<^sub>R f'')"
    30.5      apply(rule frechet_derivative_unique_within_closed_interval[of "a" "b"])
    30.6      using assms(3-)[unfolded has_vector_derivative_def] using assms(1-2)
    30.7 -    by (auto simp: Basis_real_def)
    30.8 +    by auto
    30.9    show ?thesis
   30.10    proof(rule ccontr)
   30.11 -    assume "f' \<noteq> f''"
   30.12 -    moreover
   30.13 -    hence "(\<lambda>x. x *\<^sub>R f') 1 = (\<lambda>x. x *\<^sub>R f'') 1"
   30.14 -      using * by (auto simp: fun_eq_iff)
   30.15 -    ultimately show False unfolding o_def by auto
   30.16 +    assume **: "f' \<noteq> f''"
   30.17 +    with * have "(\<lambda>x. x *\<^sub>R f') 1 = (\<lambda>x. x *\<^sub>R f'') 1"
   30.18 +      by (auto simp: fun_eq_iff)
   30.19 +    with ** show False
   30.20 +      unfolding o_def by auto
   30.21    qed
   30.22  qed
   30.23  
    31.1 --- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Tue Sep 03 00:51:08 2013 +0200
    31.2 +++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Tue Sep 03 01:12:40 2013 +0200
    31.3 @@ -63,10 +63,10 @@
    31.4    assumes "closed S" "S \<noteq> {}" shows "Sup S \<in> S"
    31.5  proof -
    31.6    from compact_eq_closed[of S] compact_attains_sup[of S] assms
    31.7 -  obtain s where "s \<in> S" "\<forall>t\<in>S. t \<le> s" by auto
    31.8 -  moreover then have "Sup S = s"
    31.9 +  obtain s where S: "s \<in> S" "\<forall>t\<in>S. t \<le> s" by auto
   31.10 +  then have "Sup S = s"
   31.11      by (auto intro!: Sup_eqI)
   31.12 -  ultimately show ?thesis
   31.13 +  with S show ?thesis
   31.14      by simp
   31.15  qed
   31.16  
   31.17 @@ -75,10 +75,10 @@
   31.18    assumes "closed S" "S \<noteq> {}" shows "Inf S \<in> S"
   31.19  proof -
   31.20    from compact_eq_closed[of S] compact_attains_inf[of S] assms
   31.21 -  obtain s where "s \<in> S" "\<forall>t\<in>S. s \<le> t" by auto
   31.22 -  moreover then have "Inf S = s"
   31.23 +  obtain s where S: "s \<in> S" "\<forall>t\<in>S. s \<le> t" by auto
   31.24 +  then have "Inf S = s"
   31.25      by (auto intro!: Inf_eqI)
   31.26 -  ultimately show ?thesis
   31.27 +  with S show ?thesis
   31.28      by simp
   31.29  qed
   31.30  
    32.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Tue Sep 03 00:51:08 2013 +0200
    32.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Tue Sep 03 01:12:40 2013 +0200
    32.3 @@ -905,12 +905,11 @@
    32.4        then show "\<exists>a b. k = {a..b}" by auto
    32.5        have "k \<subseteq> {a..b} \<and> k \<noteq> {}"
    32.6        proof (simp add: k interval_eq_empty subset_interval not_less, safe)
    32.7 -        fix i :: 'a assume i: "i \<in> Basis"
    32.8 -        moreover
    32.9 +        fix i :: 'a
   32.10 +        assume i: "i \<in> Basis"
   32.11          with f have "f i = (a, c) \<or> f i = (c, d) \<or> f i = (d, b)"
   32.12            by (auto simp: PiE_iff)
   32.13 -        moreover note ord[of i]
   32.14 -        ultimately
   32.15 +        with i ord[of i]
   32.16          show "a \<bullet> i \<le> fst (f i) \<bullet> i" "snd (f i) \<bullet> i \<le> b \<bullet> i" "fst (f i) \<bullet> i \<le> snd (f i) \<bullet> i"
   32.17            by (auto simp: subset_iff eucl_le[where 'a='a])
   32.18        qed
   32.19 @@ -952,7 +951,7 @@
   32.20            by auto
   32.21        qed
   32.22        then guess f unfolding bchoice_iff .. note f = this
   32.23 -      moreover then have "restrict f Basis \<in> Basis \<rightarrow>\<^sub>E {(a, c), (c, d), (d, b)}"
   32.24 +      moreover from f have "restrict f Basis \<in> Basis \<rightarrow>\<^sub>E {(a, c), (c, d), (d, b)}"
   32.25          by auto
   32.26        moreover from f have "x \<in> ?B (restrict f Basis)"
   32.27          by (auto simp: mem_interval eucl_le[where 'a='a])
   32.28 @@ -3874,7 +3873,7 @@
   32.29                      setprod_timesf setprod_constant inner_diff_left)
   32.30    next
   32.31      case False
   32.32 -    moreover with as have "{m *\<^sub>R b + c..m *\<^sub>R a + c} \<noteq> {}"
   32.33 +    with as have "{m *\<^sub>R b + c..m *\<^sub>R a + c} \<noteq> {}"
   32.34        unfolding interval_ne_empty
   32.35        apply (intro ballI)
   32.36        apply (erule_tac x=i in ballE)
   32.37 @@ -3882,7 +3881,7 @@
   32.38        done
   32.39      moreover from False have *: "\<And>i. (m *\<^sub>R a + c) \<bullet> i - (m *\<^sub>R b + c) \<bullet> i = (-m) *\<^sub>R (b - a) \<bullet> i"
   32.40        by (simp add: inner_simps field_simps)
   32.41 -    ultimately show ?thesis
   32.42 +    ultimately show ?thesis using False
   32.43        by (simp add: image_affinity_interval content_closed_interval'
   32.44                      setprod_timesf[symmetric] setprod_constant[symmetric] inner_diff_left)
   32.45    qed
   32.46 @@ -3918,17 +3917,20 @@
   32.47        unfolding interval_ne_empty by auto
   32.48      show "(\<exists>xa. x \<bullet> i = m i * xa \<and> a \<bullet> i \<le> xa \<and> xa \<le> b \<bullet> i) \<longleftrightarrow>
   32.49          min (m i * (a \<bullet> i)) (m i * (b \<bullet> i)) \<le> x \<bullet> i \<and> x \<bullet> i \<le> max (m i * (a \<bullet> i)) (m i * (b \<bullet> i))"
   32.50 -    proof cases
   32.51 -      assume "m i \<noteq> 0"
   32.52 -      moreover then have *: "\<And>a b. a = m i * b \<longleftrightarrow> b = a / m i"
   32.53 +    proof (cases "m i = 0")
   32.54 +      case True
   32.55 +      with a_le_b show ?thesis by auto
   32.56 +    next
   32.57 +      case False
   32.58 +      then have *: "\<And>a b. a = m i * b \<longleftrightarrow> b = a / m i"
   32.59          by (auto simp add: field_simps)
   32.60 -      moreover have
   32.61 +      from False have
   32.62            "min (m i * (a \<bullet> i)) (m i * (b \<bullet> i)) = (if 0 < m i then m i * (a \<bullet> i) else m i * (b \<bullet> i))"
   32.63            "max (m i * (a \<bullet> i)) (m i * (b \<bullet> i)) = (if 0 < m i then m i * (b \<bullet> i) else m i * (a \<bullet> i))"
   32.64          using a_le_b by (auto simp: min_def max_def mult_le_cancel_left)
   32.65 -      ultimately show ?thesis using a_le_b
   32.66 +      with False show ?thesis using a_le_b
   32.67          unfolding * by (auto simp add: le_divide_eq divide_le_eq ac_simps) 
   32.68 -    qed (insert a_le_b, auto)
   32.69 +    qed
   32.70    qed
   32.71  qed simp
   32.72  
    33.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Sep 03 00:51:08 2013 +0200
    33.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Sep 03 01:12:40 2013 +0200
    33.3 @@ -288,8 +288,8 @@
    33.4    next
    33.5      fix S
    33.6      assume "open S" "x \<in> S"
    33.7 -    from open_prod_elim[OF this] guess a' b' .
    33.8 -    moreover with A(4)[of a'] B(4)[of b']
    33.9 +    from open_prod_elim[OF this] guess a' b' . note a'b' = this
   33.10 +    moreover from a'b' A(4)[of a'] B(4)[of b']
   33.11      obtain a b where "a \<in> A" "a \<subseteq> a'" "b \<in> B" "b \<subseteq> b'" by auto
   33.12      ultimately show "\<exists>a\<in>(\<lambda>(a, b). a \<times> b) ` (A \<times> B). a \<subseteq> S"
   33.13        by (auto intro!: bexI[of _ "a \<times> b"] bexI[of _ a] bexI[of _ b])
   33.14 @@ -3264,12 +3264,12 @@
   33.15        unfolding C_def by auto
   33.16    qed
   33.17    then have "U \<subseteq> \<Union>C" using `U \<subseteq> \<Union>A` by auto
   33.18 -  ultimately obtain T where "T\<subseteq>C" "finite T" "U \<subseteq> \<Union>T"
   33.19 +  ultimately obtain T where T: "T\<subseteq>C" "finite T" "U \<subseteq> \<Union>T"
   33.20      using * by metis
   33.21 -  moreover then have "\<forall>t\<in>T. \<exists>a\<in>A. t \<inter> U \<subseteq> a"
   33.22 +  then have "\<forall>t\<in>T. \<exists>a\<in>A. t \<inter> U \<subseteq> a"
   33.23      by (auto simp: C_def)
   33.24    then guess f unfolding bchoice_iff Bex_def ..
   33.25 -  ultimately show "\<exists>T\<subseteq>A. finite T \<and> U \<subseteq> \<Union>T"
   33.26 +  with T show "\<exists>T\<subseteq>A. finite T \<and> U \<subseteq> \<Union>T"
   33.27      unfolding C_def by (intro exI[of _ "f`T"]) fastforce
   33.28  qed
   33.29  
   33.30 @@ -3708,10 +3708,9 @@
   33.31    assume f: "bounded (range f)"
   33.32    obtain r where r: "subseq r" "monoseq (f \<circ> r)"
   33.33      unfolding comp_def by (metis seq_monosub)
   33.34 -  moreover
   33.35    then have "Bseq (f \<circ> r)"
   33.36      unfolding Bseq_eq_bounded using f by (auto intro: bounded_subset)
   33.37 -  ultimately show "\<exists>l r. subseq r \<and> (f \<circ> r) ----> l"
   33.38 +  with r show "\<exists>l r. subseq r \<and> (f \<circ> r) ----> l"
   33.39      using Bseq_monoseq_convergent[of "f \<circ> r"] by (auto simp: convergent_def)
   33.40  qed
   33.41  
   33.42 @@ -5558,9 +5557,9 @@
   33.43        and c: "\<And>y. y \<in> t \<Longrightarrow> c y \<in> C \<and> open (a y) \<and> open (b y) \<and> x \<in> a y \<and> y \<in> b y \<and> a y \<times> b y \<subseteq> c y"
   33.44        by metis
   33.45      then have "\<forall>y\<in>t. open (b y)" "t \<subseteq> (\<Union>y\<in>t. b y)" by auto
   33.46 -    from compactE_image[OF `compact t` this] obtain D where "D \<subseteq> t" "finite D" "t \<subseteq> (\<Union>y\<in>D. b y)"
   33.47 +    from compactE_image[OF `compact t` this] obtain D where D: "D \<subseteq> t" "finite D" "t \<subseteq> (\<Union>y\<in>D. b y)"
   33.48        by auto
   33.49 -    moreover with c have "(\<Inter>y\<in>D. a y) \<times> t \<subseteq> (\<Union>y\<in>D. c y)"
   33.50 +    moreover from D c have "(\<Inter>y\<in>D. a y) \<times> t \<subseteq> (\<Union>y\<in>D. c y)"
   33.51        by (fastforce simp: subset_eq)
   33.52      ultimately show "\<exists>a. open a \<and> x \<in> a \<and> (\<exists>d\<subseteq>C. finite d \<and> a \<times> t \<subseteq> \<Union>d)"
   33.53        using c by (intro exI[of _ "c`D"] exI[of _ "\<Inter>(a`D)"] conjI) (auto intro!: open_INT)
   33.54 @@ -7345,8 +7344,8 @@
   33.55    shows "\<exists>S\<subseteq>A. card S = n"
   33.56  proof cases
   33.57    assume "finite A"
   33.58 -  from ex_bij_betw_nat_finite[OF this] guess f ..
   33.59 -  moreover with `n \<le> card A` have "{..< n} \<subseteq> {..< card A}" "inj_on f {..< n}"
   33.60 +  from ex_bij_betw_nat_finite[OF this] guess f .. note f = this
   33.61 +  moreover from f `n \<le> card A` have "{..< n} \<subseteq> {..< card A}" "inj_on f {..< n}"
   33.62      by (auto simp: bij_betw_def intro: subset_inj_on)
   33.63    ultimately have "f ` {..< n} \<subseteq> A" "card (f ` {..< n}) = n"
   33.64      by (auto simp: bij_betw_def card_image)
    34.1 --- a/src/HOL/Nat.thy	Tue Sep 03 00:51:08 2013 +0200
    34.2 +++ b/src/HOL/Nat.thy	Tue Sep 03 01:12:40 2013 +0200
    34.3 @@ -1888,8 +1888,8 @@
    34.4  proof -
    34.5    have "m dvd n - q \<longleftrightarrow> m dvd r * m + (n - q)"
    34.6      by (auto elim: dvd_plusE)
    34.7 -  also with assms have "\<dots> \<longleftrightarrow> m dvd r * m + n - q" by simp
    34.8 -  also with assms have "\<dots> \<longleftrightarrow> m dvd (r * m - q) + n" by simp
    34.9 +  also from assms have "\<dots> \<longleftrightarrow> m dvd r * m + n - q" by simp
   34.10 +  also from assms have "\<dots> \<longleftrightarrow> m dvd (r * m - q) + n" by simp
   34.11    also have "\<dots> \<longleftrightarrow> m dvd n + (r * m - q)" by (simp add: add_commute)
   34.12    finally show ?thesis .
   34.13  qed
    35.1 --- a/src/HOL/Nominal/Examples/Crary.thy	Tue Sep 03 00:51:08 2013 +0200
    35.2 +++ b/src/HOL/Nominal/Examples/Crary.thy	Tue Sep 03 01:12:40 2013 +0200
    35.3 @@ -766,9 +766,8 @@
    35.4    assumes "\<Gamma>' \<turnstile> t is s over \<Gamma>"
    35.5    shows "\<Gamma>' \<turnstile> s is s over \<Gamma>" 
    35.6  proof -
    35.7 -  have "\<Gamma>' \<turnstile> t is s over \<Gamma>" by fact
    35.8 -  moreover then have "\<Gamma>' \<turnstile> s is t over \<Gamma>" using logical_symmetry by blast
    35.9 -  ultimately show "\<Gamma>' \<turnstile> s is s over \<Gamma>" using logical_transitivity by blast
   35.10 +  from assms have "\<Gamma>' \<turnstile> s is t over \<Gamma>" using logical_symmetry by blast
   35.11 +  with assms show "\<Gamma>' \<turnstile> s is s over \<Gamma>" using logical_transitivity by blast
   35.12  qed
   35.13  
   35.14  lemma logical_subst_monotonicity :
    36.1 --- a/src/HOL/Number_Theory/Binomial.thy	Tue Sep 03 00:51:08 2013 +0200
    36.2 +++ b/src/HOL/Number_Theory/Binomial.thy	Tue Sep 03 01:12:40 2013 +0200
    36.3 @@ -203,7 +203,7 @@
    36.4      by (subst choose_reduce_nat, auto simp add: field_simps)
    36.5    also note one
    36.6    also note two
    36.7 -  also with less have "(n - k) * fact n + (k + 1) * fact n= fact (n + 1)" 
    36.8 +  also from less have "(n - k) * fact n + (k + 1) * fact n= fact (n + 1)" 
    36.9      apply (subst fact_plus_one_nat)
   36.10      apply (subst distrib_right [symmetric])
   36.11      apply simp
    37.1 --- a/src/HOL/Number_Theory/MiscAlgebra.thy	Tue Sep 03 00:51:08 2013 +0200
    37.2 +++ b/src/HOL/Number_Theory/MiscAlgebra.thy	Tue Sep 03 01:12:40 2013 +0200
    37.3 @@ -298,7 +298,7 @@
    37.4  proof -
    37.5    have "(x \<oplus> \<one>) \<otimes> (x \<oplus> \<ominus> \<one>) = x \<otimes> x \<oplus> \<ominus> \<one>"
    37.6      by (simp add: ring_simprules)
    37.7 -  also with `x \<otimes> x = \<one>` have "\<dots> = \<zero>"
    37.8 +  also from `x \<otimes> x = \<one>` have "\<dots> = \<zero>"
    37.9      by (simp add: ring_simprules)
   37.10    finally have "(x \<oplus> \<one>) \<otimes> (x \<oplus> \<ominus> \<one>) = \<zero>" .
   37.11    then have "(x \<oplus> \<one>) = \<zero> | (x \<oplus> \<ominus> \<one>) = \<zero>"
    38.1 --- a/src/HOL/Predicate.thy	Tue Sep 03 00:51:08 2013 +0200
    38.2 +++ b/src/HOL/Predicate.thy	Tue Sep 03 01:12:40 2013 +0200
    38.3 @@ -225,9 +225,9 @@
    38.4    "\<exists>!x. eval A x \<Longrightarrow> eval A (singleton dfault A)"
    38.5  proof -
    38.6    assume assm: "\<exists>!x. eval A x"
    38.7 -  then obtain x where "eval A x" ..
    38.8 -  moreover with assm have "singleton dfault A = x" by (rule singleton_eqI)
    38.9 -  ultimately show ?thesis by simp 
   38.10 +  then obtain x where x: "eval A x" ..
   38.11 +  with assm have "singleton dfault A = x" by (rule singleton_eqI)
   38.12 +  with x show ?thesis by simp
   38.13  qed
   38.14  
   38.15  lemma single_singleton:
    39.1 --- a/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Tue Sep 03 00:51:08 2013 +0200
    39.2 +++ b/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Tue Sep 03 01:12:40 2013 +0200
    39.3 @@ -54,7 +54,8 @@
    39.4    sorted_single [code_pred_intro]
    39.5    sorted_many [code_pred_intro]
    39.6  
    39.7 -code_pred sorted proof -
    39.8 +code_pred sorted
    39.9 +proof -
   39.10    assume "sorted xa"
   39.11    assume 1: "xa = [] \<Longrightarrow> thesis"
   39.12    assume 2: "\<And>x. xa = [x] \<Longrightarrow> thesis"
   39.13 @@ -65,9 +66,12 @@
   39.14      case (Cons x xs) show ?thesis proof (cases xs)
   39.15        case Nil with Cons 2 show ?thesis by simp
   39.16      next
   39.17 -      case (Cons y zs) with `xa = x # xs` have "xa = x # y # zs" by simp
   39.18 -      moreover with `sorted xa` have "x \<le> y" and "sorted (y # zs)" by simp_all
   39.19 -      ultimately show ?thesis by (rule 3)
   39.20 +      case (Cons y zs)
   39.21 +      show ?thesis
   39.22 +      proof (rule 3)
   39.23 +        from Cons `xa = x # xs` show "xa = x # y # zs" by simp
   39.24 +        with `sorted xa` show "x \<le> y" and "sorted (y # zs)" by simp_all
   39.25 +      qed
   39.26      qed
   39.27    qed
   39.28  qed
    40.1 --- a/src/HOL/Probability/Binary_Product_Measure.thy	Tue Sep 03 00:51:08 2013 +0200
    40.2 +++ b/src/HOL/Probability/Binary_Product_Measure.thy	Tue Sep 03 01:12:40 2013 +0200
    40.3 @@ -177,9 +177,9 @@
    40.4      by (auto intro!: measurable_If simp: space_pair_measure)
    40.5  next
    40.6    case (union F)
    40.7 -  moreover then have *: "\<And>x. emeasure M (Pair x -` (\<Union>i. F i)) = (\<Sum>i. ?s (F i) x)"
    40.8 +  then have "\<And>x. emeasure M (Pair x -` (\<Union>i. F i)) = (\<Sum>i. ?s (F i) x)"
    40.9      by (simp add: suminf_emeasure disjoint_family_vimageI subset_eq vimage_UN sets_pair_measure[symmetric])
   40.10 -  ultimately show ?case
   40.11 +  with union show ?case
   40.12      unfolding sets_pair_measure[symmetric] by simp
   40.13  qed (auto simp add: if_distrib Int_def[symmetric] intro!: measurable_If)
   40.14  
   40.15 @@ -515,9 +515,9 @@
   40.16    shows "(\<integral>\<^sup>+ x. \<integral>\<^sup>+ y. f (x, y) \<partial>M \<partial>M1) = integral\<^sup>P (M1 \<Otimes>\<^sub>M M) f" (is "?I f = _")
   40.17  using f proof induct
   40.18    case (cong u v)
   40.19 -  moreover then have "?I u = ?I v"
   40.20 +  then have "?I u = ?I v"
   40.21      by (intro positive_integral_cong) (auto simp: space_pair_measure)
   40.22 -  ultimately show ?case
   40.23 +  with cong show ?case
   40.24      by (simp cong: positive_integral_cong)
   40.25  qed (simp_all add: emeasure_pair_measure positive_integral_cmult positive_integral_add
   40.26                     positive_integral_monotone_convergence_SUP
    41.1 --- a/src/HOL/Probability/Fin_Map.thy	Tue Sep 03 00:51:08 2013 +0200
    41.2 +++ b/src/HOL/Probability/Fin_Map.thy	Tue Sep 03 01:12:40 2013 +0200
    41.3 @@ -342,9 +342,9 @@
    41.4        case (UN K)
    41.5        show ?case
    41.6        proof safe
    41.7 -        fix x X assume "x \<in> X" "X \<in> K"
    41.8 -        moreover with UN obtain e where "e>0" "\<And>y. dist y x < e \<longrightarrow> y \<in> X" by force
    41.9 -        ultimately show "\<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> \<Union>K" by auto
   41.10 +        fix x X assume "x \<in> X" and X: "X \<in> K"
   41.11 +        with UN obtain e where "e>0" "\<And>y. dist y x < e \<longrightarrow> y \<in> X" by force
   41.12 +        with X show "\<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> \<Union>K" by auto
   41.13        qed
   41.14      next
   41.15        case (Basis s) then obtain a b where s: "s = Pi' a b" and b: "\<And>i. i\<in>a \<Longrightarrow> open (b i)" by auto
   41.16 @@ -363,12 +363,10 @@
   41.17            show "y \<in> s" unfolding s
   41.18            proof
   41.19              show "domain y = a" using d s `a \<noteq> {}` by (auto simp: dist_le_1_imp_domain_eq a_dom)
   41.20 -            fix i assume "i \<in> a"
   41.21 -            moreover
   41.22 +            fix i assume i: "i \<in> a"
   41.23              hence "dist ((y)\<^sub>F i) ((x)\<^sub>F i) < es i" using d
   41.24                by (auto simp: dist_finmap_def `a \<noteq> {}` intro!: le_less_trans[OF dist_proj])
   41.25 -            ultimately
   41.26 -            show "y i \<in> b i" by (rule in_b)
   41.27 +            with i show "y i \<in> b i" by (rule in_b)
   41.28            qed
   41.29          next
   41.30            assume "\<not>a \<noteq> {}"
   41.31 @@ -715,9 +713,9 @@
   41.32  proof -
   41.33    have "\<Union>{f s|s. P s} = (\<Union>n::nat. let s = set (from_nat n) in if P s then f s else {})"
   41.34    proof safe
   41.35 -    fix x X s assume "x \<in> f s" "P s"
   41.36 -    moreover with assms obtain l where "s = set l" using finite_list by blast
   41.37 -    ultimately show "x \<in> (\<Union>n. let s = set (from_nat n) in if P s then f s else {})" using `P s`
   41.38 +    fix x X s assume *: "x \<in> f s" "P s"
   41.39 +    with assms obtain l where "s = set l" using finite_list by blast
   41.40 +    with * show "x \<in> (\<Union>n. let s = set (from_nat n) in if P s then f s else {})" using `P s`
   41.41        by (auto intro!: exI[where x="to_nat l"])
   41.42    next
   41.43      fix x n assume "x \<in> (let s = set (from_nat n) in if P s then f s else {})"
    42.1 --- a/src/HOL/Probability/Finite_Product_Measure.thy	Tue Sep 03 00:51:08 2013 +0200
    42.2 +++ b/src/HOL/Probability/Finite_Product_Measure.thy	Tue Sep 03 01:12:40 2013 +0200
    42.3 @@ -235,7 +235,7 @@
    42.4      using sets.sets_into_space by auto
    42.5    then have "A = (\<Pi>\<^sub>E i\<in>I. if i\<in>J then E i else space (M i))"
    42.6      using A J by (auto simp: prod_emb_PiE)
    42.7 -  moreover then have "(\<lambda>i. if i\<in>J then E i else space (M i)) \<in> (\<Pi> i\<in>I. sets (M i))"
    42.8 +  moreover have "(\<lambda>i. if i\<in>J then E i else space (M i)) \<in> (\<Pi> i\<in>I. sets (M i))"
    42.9      using sets.top E by auto
   42.10    ultimately show ?thesis using that by auto
   42.11  qed
   42.12 @@ -792,9 +792,9 @@
   42.13  proof (intro measure_eqI[symmetric])
   42.14    interpret I: finite_product_sigma_finite M "{i}" by default simp
   42.15    fix A assume A: "A \<in> sets (M i)"
   42.16 -  moreover then have "(\<lambda>x. x i) -` A \<inter> space (Pi\<^sub>M {i} M) = (\<Pi>\<^sub>E i\<in>{i}. A)"
   42.17 +  then have "(\<lambda>x. x i) -` A \<inter> space (Pi\<^sub>M {i} M) = (\<Pi>\<^sub>E i\<in>{i}. A)"
   42.18      using sets.sets_into_space by (auto simp: space_PiM)
   42.19 -  ultimately show "emeasure (M i) A = emeasure ?D A"
   42.20 +  then show "emeasure (M i) A = emeasure ?D A"
   42.21      using A I.measure_times[of "\<lambda>_. A"]
   42.22      by (simp add: emeasure_distr measurable_component_singleton)
   42.23  qed simp
    43.1 --- a/src/HOL/Probability/Infinite_Product_Measure.thy	Tue Sep 03 00:51:08 2013 +0200
    43.2 +++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Tue Sep 03 01:12:40 2013 +0200
    43.3 @@ -246,7 +246,7 @@
    43.4            then show ?case by auto
    43.5          qed
    43.6          moreover
    43.7 -        then have "w k \<in> space (Pi\<^sub>M (J k) M)" by auto
    43.8 +        from w have "w k \<in> space (Pi\<^sub>M (J k) M)" by auto
    43.9          moreover
   43.10          from w have "?a / 2 ^ (k + 1) \<le> ?q k k (w k)" by auto
   43.11          then have "?M (J k) (A k) (w k) \<noteq> {}"
   43.12 @@ -344,10 +344,10 @@
   43.13      assume "I = {}" then show ?thesis by (simp add: space_PiM_empty)
   43.14    next
   43.15      assume "I \<noteq> {}"
   43.16 -    then obtain i where "i \<in> I" by auto
   43.17 -    moreover then have "emb I {i} (\<Pi>\<^sub>E i\<in>{i}. space (M i)) = (space (Pi\<^sub>M I M))"
   43.18 +    then obtain i where i: "i \<in> I" by auto
   43.19 +    then have "emb I {i} (\<Pi>\<^sub>E i\<in>{i}. space (M i)) = (space (Pi\<^sub>M I M))"
   43.20        by (auto simp: prod_emb_def space_PiM)
   43.21 -    ultimately show ?thesis
   43.22 +    with i show ?thesis
   43.23        using emeasure_PiM_emb_not_empty[of "{i}" "\<lambda>i. space (M i)"]
   43.24        by (simp add: emeasure_PiM emeasure_space_1)
   43.25    qed
    44.1 --- a/src/HOL/Probability/Information.thy	Tue Sep 03 00:51:08 2013 +0200
    44.2 +++ b/src/HOL/Probability/Information.thy	Tue Sep 03 01:12:40 2013 +0200
    44.3 @@ -381,10 +381,10 @@
    44.4    shows "absolutely_continuous S (distr (S \<Otimes>\<^sub>M T) S fst)"
    44.5  proof -
    44.6    interpret sigma_finite_measure T by fact
    44.7 -  { fix A assume "A \<in> sets S" "emeasure S A = 0"
    44.8 -    moreover then have "fst -` A \<inter> space (S \<Otimes>\<^sub>M T) = A \<times> space T"
    44.9 +  { fix A assume A: "A \<in> sets S" "emeasure S A = 0"
   44.10 +    then have "fst -` A \<inter> space (S \<Otimes>\<^sub>M T) = A \<times> space T"
   44.11        by (auto simp: space_pair_measure dest!: sets.sets_into_space)
   44.12 -    ultimately have "emeasure (S \<Otimes>\<^sub>M T) (fst -` A \<inter> space (S \<Otimes>\<^sub>M T)) = 0"
   44.13 +    with A have "emeasure (S \<Otimes>\<^sub>M T) (fst -` A \<inter> space (S \<Otimes>\<^sub>M T)) = 0"
   44.14        by (simp add: emeasure_pair_measure_Times) }
   44.15    then show ?thesis
   44.16      unfolding absolutely_continuous_def
   44.17 @@ -398,10 +398,10 @@
   44.18    shows "absolutely_continuous T (distr (S \<Otimes>\<^sub>M T) T snd)"
   44.19  proof -
   44.20    interpret sigma_finite_measure T by fact
   44.21 -  { fix A assume "A \<in> sets T" "emeasure T A = 0"
   44.22 -    moreover then have "snd -` A \<inter> space (S \<Otimes>\<^sub>M T) = space S \<times> A"
   44.23 +  { fix A assume A: "A \<in> sets T" "emeasure T A = 0"
   44.24 +    then have "snd -` A \<inter> space (S \<Otimes>\<^sub>M T) = space S \<times> A"
   44.25        by (auto simp: space_pair_measure dest!: sets.sets_into_space)
   44.26 -    ultimately have "emeasure (S \<Otimes>\<^sub>M T) (snd -` A \<inter> space (S \<Otimes>\<^sub>M T)) = 0"
   44.27 +    with A have "emeasure (S \<Otimes>\<^sub>M T) (snd -` A \<inter> space (S \<Otimes>\<^sub>M T)) = 0"
   44.28        by (simp add: emeasure_pair_measure_Times) }
   44.29    then show ?thesis
   44.30      unfolding absolutely_continuous_def
    45.1 --- a/src/HOL/Probability/Lebesgue_Integration.thy	Tue Sep 03 00:51:08 2013 +0200
    45.2 +++ b/src/HOL/Probability/Lebesgue_Integration.thy	Tue Sep 03 01:12:40 2013 +0200
    45.3 @@ -675,12 +675,11 @@
    45.4    assumes f: "simple_function M f"
    45.5    shows "(\<integral>\<^sup>Sx. f x * indicator A x \<partial>M) =
    45.6      (\<Sum>x \<in> f ` space M. x * (emeasure M) (f -` {x} \<inter> space M \<inter> A))"
    45.7 -proof cases
    45.8 -  assume "A = space M"
    45.9 -  moreover hence "(\<integral>\<^sup>Sx. f x * indicator A x \<partial>M) = integral\<^sup>S M f"
   45.10 +proof (cases "A = space M")
   45.11 +  case True
   45.12 +  then have "(\<integral>\<^sup>Sx. f x * indicator A x \<partial>M) = integral\<^sup>S M f"
   45.13      by (auto intro!: simple_integral_cong)
   45.14 -  moreover have "\<And>X. X \<inter> space M \<inter> space M = X \<inter> space M" by auto
   45.15 -  ultimately show ?thesis by (simp add: simple_integral_def)
   45.16 +  with True show ?thesis by (simp add: simple_integral_def)
   45.17  next
   45.18    assume "A \<noteq> space M"
   45.19    then obtain x where x: "x \<in> space M" "x \<notin> A" using sets.sets_into_space[OF assms(1)] by auto
   45.20 @@ -1001,10 +1000,10 @@
   45.21      unfolding positive_integral_def_finite[of _ "\<lambda>x. SUP i. f i x"]
   45.22    proof (safe intro!: SUP_least)
   45.23      fix g assume g: "simple_function M g"
   45.24 -      and "g \<le> max 0 \<circ> (\<lambda>x. SUP i. f i x)" "range g \<subseteq> {0..<\<infinity>}"
   45.25 -    moreover then have "\<And>x. 0 \<le> (SUP i. f i x)" and g': "g`space M \<subseteq> {0..<\<infinity>}"
   45.26 +      and *: "g \<le> max 0 \<circ> (\<lambda>x. SUP i. f i x)" "range g \<subseteq> {0..<\<infinity>}"
   45.27 +    then have "\<And>x. 0 \<le> (SUP i. f i x)" and g': "g`space M \<subseteq> {0..<\<infinity>}"
   45.28        using f by (auto intro!: SUP_upper2)
   45.29 -    ultimately show "integral\<^sup>S M g \<le> (SUP j. integral\<^sup>P M (f j))"
   45.30 +    with * show "integral\<^sup>S M g \<le> (SUP j. integral\<^sup>P M (f j))"
   45.31        by (intro  positive_integral_SUP_approx[OF f g _ g'])
   45.32           (auto simp: le_fun_def max_def)
   45.33    qed
   45.34 @@ -1357,7 +1356,7 @@
   45.35        proof (safe intro!: incseq_SucI)
   45.36          fix n :: nat and x
   45.37          assume *: "1 \<le> real n * u x"
   45.38 -        also from gt_1[OF this] have "real n * u x \<le> real (Suc n) * u x"
   45.39 +        also from gt_1[OF *] have "real n * u x \<le> real (Suc n) * u x"
   45.40            using `0 \<le> u x` by (auto intro!: ereal_mult_right_mono)
   45.41          finally show "1 \<le> real (Suc n) * u x" by auto
   45.42        qed
   45.43 @@ -2658,10 +2657,9 @@
   45.44      using f by (simp add: positive_integral_cmult)
   45.45  next
   45.46    case (add u v)
   45.47 -  moreover then have "\<And>x. f x * (v x + u x) = f x * v x + f x * u x"
   45.48 +  then have "\<And>x. f x * (v x + u x) = f x * v x + f x * u x"
   45.49      by (simp add: ereal_right_distrib)
   45.50 -  moreover note f
   45.51 -  ultimately show ?case
   45.52 +  with add f show ?case
   45.53      by (auto simp add: positive_integral_add ereal_zero_le_0_iff intro!: positive_integral_add[symmetric])
   45.54  next
   45.55    case (seq U)
    46.1 --- a/src/HOL/Probability/Lebesgue_Measure.thy	Tue Sep 03 00:51:08 2013 +0200
    46.2 +++ b/src/HOL/Probability/Lebesgue_Measure.thy	Tue Sep 03 01:12:40 2013 +0200
    46.3 @@ -983,22 +983,20 @@
    46.4    shows "integrable lborel f \<longleftrightarrow> integrable (\<Pi>\<^sub>M (i::'a)\<in>Basis. lborel) (\<lambda>x. f (p2e x))"
    46.5      (is "_ \<longleftrightarrow> integrable ?B ?f")
    46.6  proof
    46.7 -  assume "integrable lborel f"
    46.8 -  moreover then have f: "f \<in> borel_measurable borel"
    46.9 +  assume *: "integrable lborel f"
   46.10 +  then have f: "f \<in> borel_measurable borel"
   46.11      by auto
   46.12 -  moreover with measurable_p2e
   46.13 -  have "f \<circ> p2e \<in> borel_measurable ?B"
   46.14 +  with measurable_p2e have "f \<circ> p2e \<in> borel_measurable ?B"
   46.15      by (rule measurable_comp)
   46.16 -  ultimately show "integrable ?B ?f"
   46.17 +  with * f show "integrable ?B ?f"
   46.18      by (simp add: comp_def borel_fubini_positiv_integral integrable_def)
   46.19  next
   46.20 -  assume "integrable ?B ?f"
   46.21 -  moreover
   46.22 +  assume *: "integrable ?B ?f"
   46.23    then have "?f \<circ> e2p \<in> borel_measurable (borel::'a measure)"
   46.24      by (auto intro!: measurable_e2p)
   46.25    then have "f \<in> borel_measurable borel"
   46.26      by (simp cong: measurable_cong)
   46.27 -  ultimately show "integrable lborel f"
   46.28 +  with * show "integrable lborel f"
   46.29      by (simp add: borel_fubini_positiv_integral integrable_def)
   46.30  qed
   46.31  
    47.1 --- a/src/HOL/Probability/Measure_Space.thy	Tue Sep 03 00:51:08 2013 +0200
    47.2 +++ b/src/HOL/Probability/Measure_Space.thy	Tue Sep 03 01:12:40 2013 +0200
    47.3 @@ -158,7 +158,8 @@
    47.4        and A: "A`S \<subseteq> M"
    47.5        and disj: "disjoint_family_on A S"
    47.6    shows  "(\<Sum>i\<in>S. f (A i)) = f (\<Union>i\<in>S. A i)"
    47.7 -using `finite S` disj A proof induct
    47.8 +  using `finite S` disj A
    47.9 +proof induct
   47.10    case empty show ?case using f by (simp add: positive_def)
   47.11  next
   47.12    case (insert s S)
   47.13 @@ -168,7 +169,6 @@
   47.14    have "A s \<in> M" using insert by blast
   47.15    moreover have "(\<Union>i\<in>S. A i) \<in> M"
   47.16      using insert `finite S` by auto
   47.17 -  moreover
   47.18    ultimately have "f (A s \<union> (\<Union>i\<in>S. A i)) = f (A s) + f(\<Union>i\<in>S. A i)"
   47.19      using ad UNION_in_sets A by (auto simp add: additive_def)
   47.20    with insert show ?case using ad disjoint_family_on_mono[of S "insert s S" A]
   47.21 @@ -781,15 +781,15 @@
   47.22      using sets.sets_into_space by auto
   47.23    show "{} \<in> null_sets M"
   47.24      by auto
   47.25 -  fix A B assume sets: "A \<in> null_sets M" "B \<in> null_sets M"
   47.26 -  then have "A \<in> sets M" "B \<in> sets M"
   47.27 +  fix A B assume null_sets: "A \<in> null_sets M" "B \<in> null_sets M"
   47.28 +  then have sets: "A \<in> sets M" "B \<in> sets M"
   47.29      by auto
   47.30 -  moreover then have "emeasure M (A \<union> B) \<le> emeasure M A + emeasure M B"
   47.31 +  then have *: "emeasure M (A \<union> B) \<le> emeasure M A + emeasure M B"
   47.32      "emeasure M (A - B) \<le> emeasure M A"
   47.33      by (auto intro!: emeasure_subadditive emeasure_mono)
   47.34 -  moreover have "emeasure M B = 0" "emeasure M A = 0"
   47.35 -    using sets by auto
   47.36 -  ultimately show "A - B \<in> null_sets M" "A \<union> B \<in> null_sets M"
   47.37 +  then have "emeasure M B = 0" "emeasure M A = 0"
   47.38 +    using null_sets by auto
   47.39 +  with sets * show "A - B \<in> null_sets M" "A \<union> B \<in> null_sets M"
   47.40      by (auto intro!: antisym)
   47.41  qed
   47.42  
   47.43 @@ -1563,9 +1563,9 @@
   47.44          by (auto intro!: Lim_eventually eventually_sequentiallyI[where c=i])
   47.45      next
   47.46        assume "\<not> (\<exists>i. \<forall>j\<ge>i. F i = F j)"
   47.47 -      then obtain f where "\<And>i. i \<le> f i" "\<And>i. F i \<noteq> F (f i)" by metis
   47.48 -      moreover then have "\<And>i. F i \<subseteq> F (f i)" using `incseq F` by (auto simp: incseq_def)
   47.49 -      ultimately have *: "\<And>i. F i \<subset> F (f i)" by auto
   47.50 +      then obtain f where f: "\<And>i. i \<le> f i" "\<And>i. F i \<noteq> F (f i)" by metis
   47.51 +      then have "\<And>i. F i \<subseteq> F (f i)" using `incseq F` by (auto simp: incseq_def)
   47.52 +      with f have *: "\<And>i. F i \<subset> F (f i)" by auto
   47.53  
   47.54        have "incseq (\<lambda>i. ?M (F i))"
   47.55          using `incseq F` unfolding incseq_def by (auto simp: card_mono dest: finite_subset)
    48.1 --- a/src/HOL/Probability/Projective_Limit.thy	Tue Sep 03 00:51:08 2013 +0200
    48.2 +++ b/src/HOL/Probability/Projective_Limit.thy	Tue Sep 03 01:12:40 2013 +0200
    48.3 @@ -257,14 +257,13 @@
    48.4          finally have "fm n x \<in> fm n ` B n" .
    48.5          thus "x \<in> B n"
    48.6          proof safe
    48.7 -          fix y assume "y \<in> B n"
    48.8 -          moreover
    48.9 +          fix y assume y: "y \<in> B n"
   48.10            hence "y \<in> space (Pi\<^sub>M (J n) (\<lambda>_. borel))" using J sets.sets_into_space[of "B n" "P (J n)"]
   48.11              by (auto simp add: proj_space proj_sets)
   48.12            assume "fm n x = fm n y"
   48.13            note inj_onD[OF inj_on_fm[OF space_borel],
   48.14              OF `fm n x = fm n y` `x \<in> space _` `y \<in> space _`]
   48.15 -          ultimately show "x \<in> B n" by simp
   48.16 +          with y show "x \<in> B n" by simp
   48.17          qed
   48.18        qed
   48.19        { fix n
   48.20 @@ -438,10 +437,11 @@
   48.21              apply (subst (2) tendsto_iff, subst eventually_sequentially)
   48.22            proof safe
   48.23              fix e :: real assume "0 < e"
   48.24 -            { fix i x assume "i \<ge> n" "t \<in> domain (fm n x)"
   48.25 -              moreover
   48.26 +            { fix i x
   48.27 +              assume i: "i \<ge> n"
   48.28 +              assume "t \<in> domain (fm n x)"
   48.29                hence "t \<in> domain (fm i x)" using J_mono[OF `i \<ge> n`] by auto
   48.30 -              ultimately have "(fm i x)\<^sub>F t = (fm n x)\<^sub>F t"
   48.31 +              with i have "(fm i x)\<^sub>F t = (fm n x)\<^sub>F t"
   48.32                  using j by (auto simp: proj_fm dest!: inj_onD[OF inj_on_Utn])
   48.33              } note index_shift = this
   48.34              have I: "\<And>i. i \<ge> n \<Longrightarrow> Suc (diagseq i) \<ge> n"
   48.35 @@ -487,11 +487,11 @@
   48.36          also have "finmap_of (Utn ` J n) z  = fm n (\<lambda>i. z (Utn i))"
   48.37            unfolding finmap_eq_iff
   48.38          proof clarsimp
   48.39 -          fix i assume "i \<in> J n"
   48.40 -          moreover hence "from_nat_into (\<Union>n. J n) (Utn i) = i"
   48.41 +          fix i assume i: "i \<in> J n"
   48.42 +          hence "from_nat_into (\<Union>n. J n) (Utn i) = i"
   48.43              unfolding Utn_def
   48.44              by (subst from_nat_into_to_nat_on[OF countable_UN_J]) auto
   48.45 -          ultimately show "z (Utn i) = (fm n (\<lambda>i. z (Utn i)))\<^sub>F (Utn i)"
   48.46 +          with i show "z (Utn i) = (fm n (\<lambda>i. z (Utn i)))\<^sub>F (Utn i)"
   48.47              by (simp add: finmap_eq_iff fm_def compose_def)
   48.48          qed
   48.49          finally have "fm n (\<lambda>i. z (Utn i)) \<in> K' n" .
    49.1 --- a/src/HOL/Probability/Radon_Nikodym.thy	Tue Sep 03 00:51:08 2013 +0200
    49.2 +++ b/src/HOL/Probability/Radon_Nikodym.thy	Tue Sep 03 01:12:40 2013 +0200
    49.3 @@ -412,14 +412,14 @@
    49.4  
    49.5    have ac: "absolutely_continuous M ?M" unfolding absolutely_continuous_def
    49.6    proof
    49.7 -    fix A assume A: "A \<in> null_sets M"
    49.8 -    with `absolutely_continuous M N` have "A \<in> null_sets N"
    49.9 +    fix A assume A_M: "A \<in> null_sets M"
   49.10 +    with `absolutely_continuous M N` have A_N: "A \<in> null_sets N"
   49.11        unfolding absolutely_continuous_def by auto
   49.12 -    moreover with A have "(\<integral>\<^sup>+ x. ?F A x \<partial>M) \<le> N A" using `f \<in> G` by (auto simp: G_def)
   49.13 +    moreover from A_M A_N have "(\<integral>\<^sup>+ x. ?F A x \<partial>M) \<le> N A" using `f \<in> G` by (auto simp: G_def)
   49.14      ultimately have "N A - (\<integral>\<^sup>+ x. ?F A x \<partial>M) = 0"
   49.15        using positive_integral_positive[of M] by (auto intro!: antisym)
   49.16      then show "A \<in> null_sets ?M"
   49.17 -      using A by (simp add: emeasure_M null_sets_def sets_eq)
   49.18 +      using A_M by (simp add: emeasure_M null_sets_def sets_eq)
   49.19    qed
   49.20    have upper_bound: "\<forall>A\<in>sets M. ?M A \<le> 0"
   49.21    proof (rule ccontr)
   49.22 @@ -431,7 +431,7 @@
   49.23        using emeasure_space[of ?M A] by (simp add: sets_eq[THEN sets_eq_imp_space_eq])
   49.24      finally have pos_t: "0 < ?M (space M)" by simp
   49.25      moreover
   49.26 -    then have "emeasure M (space M) \<noteq> 0"
   49.27 +    from pos_t have "emeasure M (space M) \<noteq> 0"
   49.28        using ac unfolding absolutely_continuous_def by (auto simp: null_sets_def)
   49.29      then have pos_M: "0 < emeasure M (space M)"
   49.30        using emeasure_nonneg[of M "space M"] by (simp add: le_less)
   49.31 @@ -594,12 +594,14 @@
   49.32        proof (rule disjCI, simp)
   49.33          assume *: "0 < emeasure M A \<longrightarrow> N A \<noteq> \<infinity>"
   49.34          show "emeasure M A = 0 \<and> N A = 0"
   49.35 -        proof cases
   49.36 -          assume "emeasure M A = 0" moreover with ac A have "N A = 0"
   49.37 +        proof (cases "emeasure M A = 0")
   49.38 +          case True
   49.39 +          with ac A have "N A = 0"
   49.40              unfolding absolutely_continuous_def by auto
   49.41 -          ultimately show ?thesis by simp
   49.42 +          with True show ?thesis by simp
   49.43          next
   49.44 -          assume "emeasure M A \<noteq> 0" with * have "N A \<noteq> \<infinity>" using emeasure_nonneg[of M A] by auto
   49.45 +          case False
   49.46 +          with * have "N A \<noteq> \<infinity>" using emeasure_nonneg[of M A] by auto
   49.47            with A have "emeasure M ?O_0 + emeasure M A = emeasure M (?O_0 \<union> A)"
   49.48              using Q' by (auto intro!: plus_emeasure sets.countable_UN)
   49.49            also have "\<dots> = (SUP i. emeasure M (?O i \<union> A))"
    50.1 --- a/src/HOL/Probability/Sigma_Algebra.thy	Tue Sep 03 00:51:08 2013 +0200
    50.2 +++ b/src/HOL/Probability/Sigma_Algebra.thy	Tue Sep 03 01:12:40 2013 +0200
    50.3 @@ -1244,8 +1244,8 @@
    50.4    interpret N: sigma_algebra \<Omega>' A' using measure_measure by (auto simp: measure_space_def)
    50.5    have "A = sets M" "A' = sets N"
    50.6      using measure_measure by (simp_all add: sets_def Abs_measure_inverse)
    50.7 -  with `sets M = sets N` have "A = A'" by simp
    50.8 -  moreover with M.top N.top M.space_closed N.space_closed have "\<Omega> = \<Omega>'" by auto
    50.9 +  with `sets M = sets N` have AA': "A = A'" by simp
   50.10 +  moreover from M.top N.top M.space_closed N.space_closed AA' have "\<Omega> = \<Omega>'" by auto
   50.11    moreover { fix B have "\<mu> B = \<mu>' B"
   50.12      proof cases
   50.13        assume "B \<in> A"
   50.14 @@ -1977,7 +1977,7 @@
   50.15    moreover have "D \<union> (\<Omega> - E) = (\<Union>i. ?f i)"
   50.16      by (auto simp: image_iff split: split_if_asm)
   50.17    moreover
   50.18 -  then have "disjoint_family ?f" unfolding disjoint_family_on_def
   50.19 +  have "disjoint_family ?f" unfolding disjoint_family_on_def
   50.20      using `D \<in> M`[THEN sets_into_space] `D \<subseteq> E` by auto
   50.21    ultimately have "\<Omega> - (D \<union> (\<Omega> - E)) \<in> M"
   50.22      using sets by auto
   50.23 @@ -2193,11 +2193,11 @@
   50.24  proof -
   50.25    have "E \<subseteq> Pow \<Omega>"
   50.26      using E sets_into_space by force
   50.27 -  then have "sigma_sets \<Omega> E = dynkin \<Omega> E"
   50.28 +  then have *: "sigma_sets \<Omega> E = dynkin \<Omega> E"
   50.29      using `Int_stable E` by (rule sigma_eq_dynkin)
   50.30 -  moreover then have "dynkin \<Omega> E = M"
   50.31 +  then have "dynkin \<Omega> E = M"
   50.32      using assms dynkin_subset[OF E(1)] by simp
   50.33 -  ultimately show ?thesis
   50.34 +  with * show ?thesis
   50.35      using assms by (auto simp: dynkin_def)
   50.36  qed
   50.37  
    51.1 --- a/src/HOL/Probability/ex/Dining_Cryptographers.thy	Tue Sep 03 00:51:08 2013 +0200
    51.2 +++ b/src/HOL/Probability/ex/Dining_Cryptographers.thy	Tue Sep 03 01:12:40 2013 +0200
    51.3 @@ -5,7 +5,7 @@
    51.4  lemma image_ex1_eq: "inj_on f A \<Longrightarrow> (b \<in> f ` A) \<longleftrightarrow> (\<exists>!x \<in> A. b = f x)"
    51.5    by (unfold inj_on_def) blast
    51.6  
    51.7 -lemma Ex1_eq: "\<exists>! x. P x \<Longrightarrow> P x \<Longrightarrow> P y \<Longrightarrow> x = y"
    51.8 +lemma Ex1_eq: "\<exists>!x. P x \<Longrightarrow> P x \<Longrightarrow> P y \<Longrightarrow> x = y"
    51.9    by auto
   51.10  
   51.11  section "Define the state space"
   51.12 @@ -143,8 +143,8 @@
   51.13          thus "x ! j = y ! j"
   51.14          proof (induct j)
   51.15            case (Suc j)
   51.16 -          moreover hence "j < n" by simp
   51.17 -          ultimately show ?case using *[OF `j < n`]
   51.18 +          hence "j < n" by simp
   51.19 +          with Suc show ?case using *[OF `j < n`]
   51.20              by (cases "y ! j") simp_all
   51.21          qed simp
   51.22        qed
   51.23 @@ -234,7 +234,7 @@
   51.24    hence zs: "inversion (Some i, zs) = xs"
   51.25      by (simp add: xs_inv[symmetric] inversion_def coin_def payer_def)
   51.26    moreover
   51.27 -  hence Not_zs: "inversion (Some i, (map Not zs)) = xs"
   51.28 +  from zs have Not_zs: "inversion (Some i, (map Not zs)) = xs"
   51.29      by (simp add: xs_inv[symmetric] inversion_def coin_def payer_def)
   51.30    ultimately
   51.31    have "{dc \<in> dc_crypto. payer dc = Some i \<and> inversion dc = xs} =
    52.1 --- a/src/HOL/Quotient_Examples/FSet.thy	Tue Sep 03 00:51:08 2013 +0200
    52.2 +++ b/src/HOL/Quotient_Examples/FSet.thy	Tue Sep 03 01:12:40 2013 +0200
    52.3 @@ -1033,9 +1033,9 @@
    52.4    case (insert x A)
    52.5    from insert.prems insert.hyps(1) have "\<And>z. z \<in> fset A \<longleftrightarrow> z \<in> fset (B - {|x|})"
    52.6      by (auto simp add: in_fset)
    52.7 -  then have "A = B - {|x|}" by (rule insert.hyps(2))
    52.8 -  moreover with insert.prems [symmetric, of x] have "x |\<in>| B" by (simp add: in_fset)
    52.9 -  ultimately show ?case by (metis in_fset_mdef)
   52.10 +  then have A: "A = B - {|x|}" by (rule insert.hyps(2))
   52.11 +  with insert.prems [symmetric, of x] have "x |\<in>| B" by (simp add: in_fset)
   52.12 +  with A show ?case by (metis in_fset_mdef)
   52.13  qed
   52.14  
   52.15  subsection {* alternate formulation with a different decomposition principle
    53.1 --- a/src/HOL/Rat.thy	Tue Sep 03 00:51:08 2013 +0200
    53.2 +++ b/src/HOL/Rat.thy	Tue Sep 03 01:12:40 2013 +0200
    53.3 @@ -237,7 +237,7 @@
    53.4  next
    53.5    case False
    53.6    then obtain a b where "q = Fract a b" and "b > 0" and "coprime a b" by (cases q) auto
    53.7 -  moreover with False have "0 \<noteq> Fract a b" by simp
    53.8 +  with False have "0 \<noteq> Fract a b" by simp
    53.9    with `b > 0` have "a \<noteq> 0" by (simp add: Zero_rat_def eq_rat)
   53.10    with Fract `q = Fract a b` `b > 0` `coprime a b` show C by blast
   53.11  qed
    54.1 --- a/src/HOL/Real.thy	Tue Sep 03 00:51:08 2013 +0200
    54.2 +++ b/src/HOL/Real.thy	Tue Sep 03 01:12:40 2013 +0200
    54.3 @@ -947,7 +947,7 @@
    54.4        using complete_real[of X] by blast
    54.5      then have "Sup X = s"
    54.6        unfolding Sup_real_def by (best intro: Least_equality)  
    54.7 -    also with s z have "... \<le> z"
    54.8 +    also from s z have "... \<le> z"
    54.9        by blast
   54.10      finally show "Sup X \<le> z" . }
   54.11    note Sup_least = this
    55.1 --- a/src/HOL/Real_Vector_Spaces.thy	Tue Sep 03 00:51:08 2013 +0200
    55.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Tue Sep 03 01:12:40 2013 +0200
    55.3 @@ -758,10 +758,10 @@
    55.4    show "\<exists>A::nat \<Rightarrow> 'a set. (\<forall>i. x \<in> A i \<and> open (A i)) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>i. A i \<subseteq> S))"
    55.5    proof (safe intro!: exI[of _ "\<lambda>n. {y. dist x y < inverse (Suc n)}"])
    55.6      fix S assume "open S" "x \<in> S"
    55.7 -    then obtain e where "0 < e" "{y. dist x y < e} \<subseteq> S"
    55.8 +    then obtain e where e: "0 < e" and "{y. dist x y < e} \<subseteq> S"
    55.9        by (auto simp: open_dist subset_eq dist_commute)
   55.10      moreover
   55.11 -    then obtain i where "inverse (Suc i) < e"
   55.12 +    from e obtain i where "inverse (Suc i) < e"
   55.13        by (auto dest!: reals_Archimedean)
   55.14      then have "{y. dist x y < inverse (Suc i)} \<subseteq> {y. dist x y < e}"
   55.15        by auto
    56.1 --- a/src/HOL/Set_Interval.thy	Tue Sep 03 00:51:08 2013 +0200
    56.2 +++ b/src/HOL/Set_Interval.thy	Tue Sep 03 01:12:40 2013 +0200
    56.3 @@ -269,9 +269,9 @@
    56.4    "{a .. b} = {c} \<longleftrightarrow> a = b \<and> b = c"
    56.5  proof
    56.6    assume "{a..b} = {c}"
    56.7 -  hence "\<not> (\<not> a \<le> b)" unfolding atLeastatMost_empty_iff[symmetric] by simp
    56.8 -  moreover with `{a..b} = {c}` have "c \<le> a \<and> b \<le> c" by auto
    56.9 -  ultimately show "a = b \<and> b = c" by auto
   56.10 +  hence *: "\<not> (\<not> a \<le> b)" unfolding atLeastatMost_empty_iff[symmetric] by simp
   56.11 +  with `{a..b} = {c}` have "c \<le> a \<and> b \<le> c" by auto
   56.12 +  with * show "a = b \<and> b = c" by auto
   56.13  qed simp
   56.14  
   56.15  lemma Icc_subset_Ici_iff[simp]:
   56.16 @@ -827,21 +827,23 @@
   56.17  subset is exactly that interval. *}
   56.18  
   56.19  lemma subset_card_intvl_is_intvl:
   56.20 -  "A <= {k..<k+card A} \<Longrightarrow> A = {k..<k+card A}" (is "PROP ?P")
   56.21 -proof cases
   56.22 -  assume "finite A"
   56.23 -  thus "PROP ?P"
   56.24 -  proof(induct A rule:finite_linorder_max_induct)
   56.25 +  assumes "A \<subseteq> {k..<k+card A}"
   56.26 +  shows "A = {k..<k+card A}"
   56.27 +proof (cases "finite A")
   56.28 +  case True
   56.29 +  from this and assms show ?thesis
   56.30 +  proof (induct A rule: finite_linorder_max_induct)
   56.31      case empty thus ?case by auto
   56.32    next
   56.33      case (insert b A)
   56.34 -    moreover hence "b ~: A" by auto
   56.35 -    moreover have "A <= {k..<k+card A}" and "b = k+card A"
   56.36 -      using `b ~: A` insert by fastforce+
   56.37 -    ultimately show ?case by auto
   56.38 +    hence *: "b \<notin> A" by auto
   56.39 +    with insert have "A <= {k..<k+card A}" and "b = k+card A"
   56.40 +      by fastforce+
   56.41 +    with insert * show ?case by auto
   56.42    qed
   56.43  next
   56.44 -  assume "~finite A" thus "PROP ?P" by simp
   56.45 +  case False
   56.46 +  with assms show ?thesis by simp
   56.47  qed
   56.48  
   56.49  
   56.50 @@ -1470,7 +1472,7 @@
   56.51      case 0 then show ?case by simp
   56.52    next
   56.53      case (Suc n)
   56.54 -    moreover with `y \<noteq> 0` have "(1 + y) ^ n = (y * inverse y) * (1 + y) ^ n" by simp 
   56.55 +    moreover from Suc `y \<noteq> 0` have "(1 + y) ^ n = (y * inverse y) * (1 + y) ^ n" by simp 
   56.56      ultimately show ?case by (simp add: field_simps divide_inverse)
   56.57    qed
   56.58    ultimately show ?thesis by simp
    57.1 --- a/src/HOL/Statespace/DistinctTreeProver.thy	Tue Sep 03 00:51:08 2013 +0200
    57.2 +++ b/src/HOL/Statespace/DistinctTreeProver.thy	Tue Sep 03 01:12:40 2013 +0200
    57.3 @@ -572,13 +572,13 @@
    57.4    shows "delete x (Node l y d r) = Some (Node l' y d r)"
    57.5  proof -
    57.6    from delete_Some_x_set_of [OF del_l]
    57.7 -  obtain "x \<in> set_of l"
    57.8 +  obtain x: "x \<in> set_of l"
    57.9      by simp
   57.10 -  moreover with dist 
   57.11 +  with dist 
   57.12    have "delete x r = None"
   57.13      by (cases "delete x r") (auto dest:delete_Some_x_set_of)
   57.14  
   57.15 -  ultimately 
   57.16 +  with x 
   57.17    show ?thesis
   57.18      using del_l dist
   57.19      by (auto split: option.splits)
   57.20 @@ -590,13 +590,13 @@
   57.21    shows "delete x (Node l y d r) = Some (Node l y d r')"
   57.22  proof -
   57.23    from delete_Some_x_set_of [OF del_r]
   57.24 -  obtain "x \<in> set_of r"
   57.25 +  obtain x: "x \<in> set_of r"
   57.26      by simp
   57.27 -  moreover with dist 
   57.28 +  with dist 
   57.29    have "delete x l = None"
   57.30      by (cases "delete x l") (auto dest:delete_Some_x_set_of)
   57.31  
   57.32 -  ultimately 
   57.33 +  with x 
   57.34    show ?thesis
   57.35      using del_r dist
   57.36      by (auto split: option.splits)
    58.1 --- a/src/HOL/Topological_Spaces.thy	Tue Sep 03 00:51:08 2013 +0200
    58.2 +++ b/src/HOL/Topological_Spaces.thy	Tue Sep 03 01:12:40 2013 +0200
    58.3 @@ -2145,7 +2145,8 @@
    58.4        moreover obtain b where "b \<in> B" "x < b" "b < min a y"
    58.5          using cInf_less_iff[of "B \<inter> {x <..}" x "min a y"] `?z < a` `?z < y` `x < y` `y \<in> B`
    58.6          by (auto intro: less_imp_le)
    58.7 -      moreover then have "?z \<le> b"
    58.8 +      moreover have "?z \<le> b"
    58.9 +        using `b \<in> B` `x < b`
   58.10          by (intro cInf_lower[where z=x]) auto
   58.11        moreover have "b \<in> U"
   58.12          using `x \<le> ?z` `?z \<le> b` `b < min a y`
    59.1 --- a/src/HOL/ex/HarmonicSeries.thy	Tue Sep 03 00:51:08 2013 +0200
    59.2 +++ b/src/HOL/ex/HarmonicSeries.thy	Tue Sep 03 01:12:40 2013 +0200
    59.3 @@ -65,7 +65,7 @@
    59.4        proof -
    59.5          from xs have
    59.6            "x \<ge> 2^(m - 1) + 1" by auto
    59.7 -        moreover with mgt0 have
    59.8 +        moreover from mgt0 have
    59.9            "2^(m - 1) + 1 \<ge> (1::nat)" by auto
   59.10          ultimately have
   59.11            "x \<ge> 1" by (rule xtrans)