author | wenzelm |

Tue Sep 03 01:12:40 2013 +0200 (2013-09-03) | |

changeset 53374 | a14d2a854c02 |

parent 53373 | 3ca9e79ac926 |

child 53375 | 78693e46a237 |

tuned proofs -- clarified flow of facts wrt. calculation;

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)