# HG changeset patch # User wenzelm # Date 1378163560 -7200 # Node ID a14d2a854c0241b418ec7b7dd6c31dc026e7f61c # Parent 3ca9e79ac926e70eb048959c03231690191066ab tuned proofs -- clarified flow of facts wrt. calculation; diff -r 3ca9e79ac926 -r a14d2a854c02 src/HOL/Algebra/Divisibility.thy --- a/src/HOL/Algebra/Divisibility.thy Tue Sep 03 00:51:08 2013 +0200 +++ b/src/HOL/Algebra/Divisibility.thy Tue Sep 03 01:12:40 2013 +0200 @@ -3637,11 +3637,11 @@ assume cunit:"c \ Units G" have "b \ inv c = a \ c \ inv c" by (simp add: b) - also with ccarr acarr cunit + also from ccarr acarr cunit have "\ = a \ (c \ inv c)" by (fast intro: m_assoc) - also with ccarr cunit + also from ccarr cunit have "\ = a \ \" by (simp add: Units_r_inv) - also with acarr + also from acarr have "\ = a" by simp finally have "a = b \ inv c" by simp with ccarr cunit diff -r 3ca9e79ac926 -r a14d2a854c02 src/HOL/BNF/Examples/Stream.thy --- a/src/HOL/BNF/Examples/Stream.thy Tue Sep 03 00:51:08 2013 +0200 +++ b/src/HOL/BNF/Examples/Stream.thy Tue Sep 03 01:12:40 2013 +0200 @@ -423,9 +423,9 @@ case False hence "x = flat (stl s) !! (y - length (shd s))" by (metis less(2,3) flat_snth) moreover - { from less(2) have "length (shd s) > 0" by (cases s) simp_all - moreover with False have "y > 0" by (cases y) simp_all - ultimately have "y - length (shd s) < y" by simp + { from less(2) have *: "length (shd s) > 0" by (cases s) simp_all + with False have "y > 0" by (cases y) simp_all + with * have "y - length (shd s) < y" by simp } moreover have "\xs \ sset (stl s). xs \ []" using less(2) by (cases s) auto ultimately have "\n m'. x = stl s !! n ! m' \ m' < length (stl s !! n)" by (intro less(1)) auto diff -r 3ca9e79ac926 -r a14d2a854c02 src/HOL/BNF/More_BNFs.thy --- a/src/HOL/BNF/More_BNFs.thy Tue Sep 03 00:51:08 2013 +0200 +++ b/src/HOL/BNF/More_BNFs.thy Tue Sep 03 01:12:40 2013 +0200 @@ -898,11 +898,10 @@ proof (intro multiset_eqI, transfer fixing: f) fix x :: 'a and M1 M2 :: "'b \ nat" assume "M1 \ multiset" "M2 \ multiset" - moreover hence "setsum M1 {a. f a = x \ 0 < M1 a} = setsum M1 {a. f a = x \ 0 < M1 a + M2 a}" "setsum M2 {a. f a = x \ 0 < M2 a} = setsum M2 {a. f a = x \ 0 < M1 a + M2 a}" by (auto simp: multiset_def intro!: setsum_mono_zero_cong_left) - ultimately show "(\a | f a = x \ 0 < M1 a + M2 a. M1 a + M2 a) = + then show "(\a | f a = x \ 0 < M1 a + M2 a. M1 a + M2 a) = setsum M1 {a. f a = x \ 0 < M1 a} + setsum M2 {a. f a = x \ 0 < M2 a}" by (auto simp: setsum.distrib[symmetric]) diff -r 3ca9e79ac926 -r a14d2a854c02 src/HOL/Big_Operators.thy --- a/src/HOL/Big_Operators.thy Tue Sep 03 00:51:08 2013 +0200 +++ b/src/HOL/Big_Operators.thy Tue Sep 03 01:12:40 2013 +0200 @@ -46,7 +46,7 @@ proof - from `x \ A` obtain B where A: "A = insert x B" and "x \ B" by (auto dest: mk_disjoint_insert) - moreover from `finite A` this have "finite B" by simp + moreover from `finite A` A have "finite B" by simp ultimately show ?thesis by simp qed diff -r 3ca9e79ac926 -r a14d2a854c02 src/HOL/Complete_Lattices.thy --- a/src/HOL/Complete_Lattices.thy Tue Sep 03 00:51:08 2013 +0200 +++ b/src/HOL/Complete_Lattices.thy Tue Sep 03 01:12:40 2013 +0200 @@ -250,7 +250,7 @@ shows "\A \ u" proof - from `A \ {}` obtain v where "v \ A" by blast - moreover with assms have "v \ u" by blast + moreover from `v \ A` assms(1) have "v \ u" by blast ultimately show ?thesis by (rule Inf_lower2) qed @@ -260,7 +260,7 @@ shows "u \ \A" proof - from `A \ {}` obtain v where "v \ A" by blast - moreover with assms have "u \ v" by blast + moreover from `v \ A` assms(1) have "u \ v" by blast ultimately show ?thesis by (rule Sup_upper2) qed diff -r 3ca9e79ac926 -r a14d2a854c02 src/HOL/Complex.thy --- a/src/HOL/Complex.thy Tue Sep 03 00:51:08 2013 +0200 +++ b/src/HOL/Complex.thy Tue Sep 03 01:12:40 2013 +0200 @@ -707,11 +707,11 @@ unfolding d_def by simp moreover from a assms have "cos a = cos x" and "sin a = sin x" by (simp_all add: complex_eq_iff) - hence "cos d = 1" unfolding d_def cos_diff by simp - moreover hence "sin d = 0" by (rule cos_one_sin_zero) + hence cos: "cos d = 1" unfolding d_def cos_diff by simp + moreover from cos have "sin d = 0" by (rule cos_one_sin_zero) ultimately have "d = 0" unfolding sin_zero_iff even_mult_two_ex - by (safe, auto simp add: numeral_2_eq_2 less_Suc_eq) + by (auto simp add: numeral_2_eq_2 less_Suc_eq) thus "a = x" unfolding d_def by simp qed (simp add: assms del: Re_sgn Im_sgn) with `z \ 0` show "arg z = x" diff -r 3ca9e79ac926 -r a14d2a854c02 src/HOL/Decision_Procs/Commutative_Ring_Complete.thy --- a/src/HOL/Decision_Procs/Commutative_Ring_Complete.thy Tue Sep 03 00:51:08 2013 +0200 +++ b/src/HOL/Decision_Procs/Commutative_Ring_Complete.thy Tue Sep 03 01:12:40 2013 +0200 @@ -138,7 +138,6 @@ by (auto simp add: norm_Pinj[of _ P2] norm_Pinj[of _ Q2]) moreover note 6 Y0 - moreover ultimately have ?case by (simp add: mkPinj_cn) } moreover { assume "x>y" hence "EX d. x = d + y" by arith @@ -286,7 +285,6 @@ from 6 have "y>0" by (cases y) (auto simp add: norm_Pinj_0_False) moreover note 6 - moreover ultimately have ?case by (simp add: mkPinj_cn) } moreover { assume "x > y" hence "EX d. x = d + y" by arith diff -r 3ca9e79ac926 -r a14d2a854c02 src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Tue Sep 03 00:51:08 2013 +0200 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Tue Sep 03 01:12:40 2013 +0200 @@ -2168,7 +2168,6 @@ by(simp add: r[of "- (?t / (2*?c))"] msubstlt_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm) } moreover - moreover {assume c: "?c = 0" and d: "?d>0" from d have d'': "2*?d > 0" by (simp add: zero_less_mult_iff) from d have d': "2*?d \ 0" by simp @@ -2314,7 +2313,6 @@ by(simp add: r[of "- (?t / (2*?c))"] msubstle_def Let_def evaldjf_ex field_simps lt polyneg_norm polymul_norm) } moreover - moreover {assume c: "?c = 0" and d: "?d>0" from d have d'': "2*?d > 0" by (simp add: zero_less_mult_iff) from d have d': "2*?d \ 0" by simp diff -r 3ca9e79ac926 -r a14d2a854c02 src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Tue Sep 03 00:51:08 2013 +0200 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Tue Sep 03 01:12:40 2013 +0200 @@ -1314,7 +1314,7 @@ head_isnpolyh_Suc'[OF np norm(5)] head_isnpolyh_Suc'[OF np norm(6)[simplified nn']] have ?case by simp} moreover - {moreover assume nz: "n = 0" + { assume nz: "n = 0" from polymul_degreen[OF norm(5,4), where m="0"] polymul_degreen[OF norm(5,3), where m="0"] nn' nz degree_eq_degreen0 norm(5,6) degree_npolyhCN[OF norm(6)] diff -r 3ca9e79ac926 -r a14d2a854c02 src/HOL/Deriv.thy --- a/src/HOL/Deriv.thy Tue Sep 03 00:51:08 2013 +0200 +++ b/src/HOL/Deriv.thy Tue Sep 03 01:12:40 2013 +0200 @@ -416,10 +416,10 @@ proof fix h show "F h = 0" proof (rule ccontr) - assume "F h \ 0" - moreover from this have h: "h \ 0" + assume **: "F h \ 0" + then have h: "h \ 0" by (clarsimp simp add: F.zero) - ultimately have "0 < ?r h" + with ** have "0 < ?r h" by (simp add: divide_pos_pos) from LIM_D [OF * this] obtain s where s: "0 < s" and r: "\x. x \ 0 \ norm x < s \ ?r x < ?r h" by auto @@ -528,11 +528,11 @@ lemma differentiable_def: "(f::real \ real) differentiable x in s \ (\D. DERIV f x : s :> D)" proof safe assume "f differentiable x in s" - then obtain f' where "FDERIV f x : s :> f'" + then obtain f' where *: "FDERIV f x : s :> f'" unfolding isDiff_def by auto - moreover then obtain c where "f' = (\x. x * c)" + then obtain c where "f' = (\x. x * c)" by (metis real_bounded_linear FDERIV_bounded_linear) - ultimately show "\D. DERIV f x : s :> D" + with * show "\D. DERIV f x : s :> D" unfolding deriv_fderiv by auto qed (auto simp: isDiff_def deriv_fderiv) @@ -730,8 +730,8 @@ DERIV f x :> u \ DERIV g y :> v" unfolding DERIV_iff2 proof (rule filterlim_cong) - assume "eventually (\x. f x = g x) (nhds x)" - moreover then have "f x = g x" by (auto simp: eventually_nhds) + assume *: "eventually (\x. f x = g x) (nhds x)" + moreover from * have "f x = g x" by (auto simp: eventually_nhds) moreover assume "x = y" "u = v" ultimately show "eventually (\xa. (f xa - f x) / (xa - x) = (g xa - g y) / (xa - y)) (at x)" by (auto simp: eventually_at_filter elim: eventually_elim1) @@ -1348,7 +1348,7 @@ { from cdef have "?h b - ?h a = (b - a) * l" by auto - also with leq have "\ = (b - a) * (g'c * (f b - f a) - f'c * (g b - g a))" by simp + also from leq have "\ = (b - a) * (g'c * (f b - f a) - f'c * (g b - g a))" by simp finally have "?h b - ?h a = (b - a) * (g'c * (f b - f a) - f'c * (g b - g a))" by simp } moreover @@ -1458,9 +1458,10 @@ using `isCont g 0` g by (auto intro: DERIV_isCont simp: le_less) ultimately have "\c. 0 < c \ c < x \ (f x - f 0) * g' c = (g x - g 0) * f' c" using f g `x < a` by (intro GMVT') auto - then guess c .. + then obtain c where *: "0 < c" "c < x" "(f x - f 0) * g' c = (g x - g 0) * f' c" + by blast moreover - with g'(1)[of c] g'(2) have "(f x - f 0) / (g x - g 0) = f' c / g' c" + from * g'(1)[of c] g'(2) have "(f x - f 0) / (g x - g 0) = f' c / g' c" by (simp add: field_simps) ultimately show "\y. 0 < y \ y < x \ f x / g x = f' y / g' y" using `f 0 = 0` `g 0 = 0` by (auto intro!: exI[of _ c]) diff -r 3ca9e79ac926 -r a14d2a854c02 src/HOL/Divides.thy --- a/src/HOL/Divides.thy Tue Sep 03 00:51:08 2013 +0200 +++ b/src/HOL/Divides.thy Tue Sep 03 01:12:40 2013 +0200 @@ -742,11 +742,11 @@ apply (subst less_iff_Suc_add) apply (auto simp add: add_mult_distrib) done - from `n \ 0` assms have "fst qr = fst qr'" + from `n \ 0` assms have *: "fst qr = fst qr'" by (auto simp add: divmod_nat_rel_def intro: order_antisym dest: aux sym) - moreover from this assms have "snd qr = snd qr'" + with assms have "snd qr = snd qr'" by (simp add: divmod_nat_rel_def) - ultimately show ?thesis by (cases qr, cases qr') simp + with * show ?thesis by (cases qr, cases qr') simp qed text {* diff -r 3ca9e79ac926 -r a14d2a854c02 src/HOL/Fields.thy --- a/src/HOL/Fields.thy Tue Sep 03 00:51:08 2013 +0200 +++ b/src/HOL/Fields.thy Tue Sep 03 01:12:40 2013 +0200 @@ -919,8 +919,8 @@ assume notless: "~ (0 < x)" have "~ (1 < inverse x)" proof - assume "1 < inverse x" - also with notless have "... \ 0" by simp + assume *: "1 < inverse x" + also from notless and * have "... \ 0" by simp also have "... < 1" by (rule zero_less_one) finally show False by auto qed diff -r 3ca9e79ac926 -r a14d2a854c02 src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Tue Sep 03 00:51:08 2013 +0200 +++ b/src/HOL/Finite_Set.thy Tue Sep 03 01:12:40 2013 +0200 @@ -1103,7 +1103,7 @@ proof - from `x \ A` obtain B where A: "A = insert x B" and "x \ B" by (auto dest: mk_disjoint_insert) - moreover from `finite A` this have "finite B" by simp + moreover from `finite A` A have "finite B" by simp ultimately show ?thesis by simp qed diff -r 3ca9e79ac926 -r a14d2a854c02 src/HOL/Imperative_HOL/Legacy_Mrec.thy --- a/src/HOL/Imperative_HOL/Legacy_Mrec.thy Tue Sep 03 00:51:08 2013 +0200 +++ b/src/HOL/Imperative_HOL/Legacy_Mrec.thy Tue Sep 03 01:12:40 2013 +0200 @@ -118,7 +118,7 @@ proof (cases "mrec b h1") case (Some result) then obtain aaa h2 where mrec_rec: "mrec b h1 = Some (aaa, h2)" by fastforce - moreover from this have "P b h1 (snd (the (mrec b h1))) (fst (the (mrec b h1)))" + moreover from mrec_rec have "P b h1 (snd (the (mrec b h1))) (fst (the (mrec b h1)))" apply (intro 1(2)) apply (auto simp add: Inr Inl') done diff -r 3ca9e79ac926 -r a14d2a854c02 src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy --- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Tue Sep 03 00:51:08 2013 +0200 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Tue Sep 03 01:12:40 2013 +0200 @@ -469,12 +469,12 @@ assume pivot: "l \ p \ p \ r" assume i_outer: "i < l \ r < i" from partition_outer_remains [OF part True] i_outer - have "Array.get h a !i = Array.get h1 a ! i" by fastforce + have 2: "Array.get h a !i = Array.get h1 a ! i" by fastforce moreover - with 1(1) [OF True pivot qs1] pivot i_outer - have "Array.get h1 a ! i = Array.get h2 a ! i" by auto + from 1(1) [OF True pivot qs1] pivot i_outer 2 + have 3: "Array.get h1 a ! i = Array.get h2 a ! i" by auto moreover - with qs2 1(2) [of p h2 h' ret2] True pivot i_outer + from qs2 1(2) [of p h2 h' ret2] True pivot i_outer 3 have "Array.get h2 a ! i = Array.get h' a ! i" by auto ultimately have "Array.get h a ! i= Array.get h' a ! i" by simp } @@ -604,9 +604,9 @@ shows "success (f \= g) h" using assms(1) proof (rule success_effectE) fix h' r - assume "effect f h h' r" - moreover with assms(2) have "success (g r) h'" . - ultimately show "success (f \= g) h" by (rule success_bind_effectI) + assume *: "effect f h h' r" + with assms(2) have "success (g r) h'" . + with * show "success (f \= g) h" by (rule success_bind_effectI) qed lemma success_partitionI: diff -r 3ca9e79ac926 -r a14d2a854c02 src/HOL/Imperative_HOL/ex/Sublist.thy --- a/src/HOL/Imperative_HOL/ex/Sublist.thy Tue Sep 03 00:51:08 2013 +0200 +++ b/src/HOL/Imperative_HOL/ex/Sublist.thy Tue Sep 03 01:12:40 2013 +0200 @@ -490,7 +490,6 @@ moreover from right l_r length_eq have "sublist' r (List.length xs) xs = sublist' r (List.length ys) ys" by (auto simp add: length_sublist' nth_sublist' intro!: nth_equalityI) - moreover ultimately show ?thesis by (simp add: multiset_of_append) qed diff -r 3ca9e79ac926 -r a14d2a854c02 src/HOL/Library/Extended_Real.thy --- a/src/HOL/Library/Extended_Real.thy Tue Sep 03 00:51:08 2013 +0200 +++ b/src/HOL/Library/Extended_Real.thy Tue Sep 03 01:12:40 2013 +0200 @@ -146,11 +146,11 @@ "-\ + -\ = -(\::ereal)" proof - case (goal1 P x) - moreover then obtain a b where "x = (a, b)" by (cases x) auto - ultimately show P + then obtain a b where "x = (a, b)" by (cases x) auto + with goal1 show P by (cases rule: ereal2_cases[of a b]) auto qed auto -termination proof qed (rule wf_empty) +termination by default (rule wf_empty) lemma Infty_neq_0[simp]: "(\::ereal) \ 0" "0 \ (\::ereal)" @@ -234,8 +234,8 @@ | " -\ < (\::ereal) \ True" proof - case (goal1 P x) - moreover then obtain a b where "x = (a,b)" by (cases x) auto - ultimately show P by (cases rule: ereal2_cases[of a b]) auto + then obtain a b where "x = (a,b)" by (cases x) auto + with goal1 show P by (cases rule: ereal2_cases[of a b]) auto qed simp_all termination by (relation "{}") simp @@ -496,8 +496,8 @@ "-(\::ereal) * -\ = \" proof - case (goal1 P x) - moreover then obtain a b where "x = (a, b)" by (cases x) auto - ultimately show P by (cases rule: ereal2_cases[of a b]) auto + then obtain a b where "x = (a, b)" by (cases x) auto + with goal1 show P by (cases rule: ereal2_cases[of a b]) auto qed simp_all termination by (relation "{}") simp @@ -1338,9 +1338,9 @@ next { assume "c = \" have ?thesis proof cases - assume "\i. f i = 0" - moreover then have "range f = {0}" by auto - ultimately show "c * SUPR UNIV f \ y" using * + assume **: "\i. f i = 0" + then have "range f = {0}" by auto + with ** show "c * SUPR UNIV f \ y" using * by (auto simp: SUP_def min_max.sup_absorb1) next assume "\ (\i. f i = 0)" @@ -1417,9 +1417,9 @@ from `A \ {}` obtain x where "x \ A" by auto show ?thesis proof cases - assume "\ \ A" - moreover then have "\ \ Sup A" by (intro complete_lattice_class.Sup_upper) - ultimately show ?thesis by (auto intro!: exI[of _ "\x. \"]) + assume *: "\ \ A" + then have "\ \ Sup A" by (intro complete_lattice_class.Sup_upper) + with * show ?thesis by (auto intro!: exI[of _ "\x. \"]) next assume "\ \ A" have "\x\A. 0 \ x" @@ -1489,10 +1489,13 @@ fixes A :: "ereal set" assumes "A \ {}" and "\a\ \ \" shows "Inf ((\x. a - x) ` A) = a - Sup A" proof - - { fix x have "-a - -x = -(a - x)" using assms by (cases x) auto } - moreover then have "(\x. -a - x)`uminus`A = uminus ` (\x. a - x) ` A" + { + fix x + have "-a - -x = -(a - x)" using assms by (cases x) auto + } note * = this + then have "(\x. -a - x)`uminus`A = uminus ` (\x. a - x) ` A" by (auto simp: image_image) - ultimately show ?thesis + with * show ?thesis using Sup_ereal_cminus[of "uminus ` A" "-a"] assms by (auto simp add: ereal_Sup_uminus_image_eq ereal_Inf_uminus_image_eq) qed @@ -1606,9 +1609,9 @@ unfolding open_ereal_generated proof (induct rule: generate_topology.induct) case (Int A B) - moreover then obtain x z where "\ \ A \ {ereal x <..} \ A" "\ \ B \ {ereal z <..} \ B" - by auto - ultimately show ?case + then obtain x z where "\ \ A \ {ereal x <..} \ A" "\ \ B \ {ereal z <..} \ B" + by auto + with Int show ?case by (intro exI[of _ "max x z"]) fastforce next { fix x have "x \ \ \ \t. x \ ereal t" by (cases x) auto } @@ -1621,9 +1624,9 @@ unfolding open_ereal_generated proof (induct rule: generate_topology.induct) case (Int A B) - moreover then obtain x z where "-\ \ A \ {..< ereal x} \ A" "-\ \ B \ {..< ereal z} \ B" - by auto - ultimately show ?case + then obtain x z where "-\ \ A \ {..< ereal x} \ A" "-\ \ B \ {..< ereal z} \ B" + by auto + with Int show ?case by (intro exI[of _ "min x z"]) fastforce next { fix x have "x \ - \ \ \t. ereal t \ x" by (cases x) auto } diff -r 3ca9e79ac926 -r a14d2a854c02 src/HOL/Library/FinFun.thy --- a/src/HOL/Library/FinFun.thy Tue Sep 03 00:51:08 2013 +0200 +++ b/src/HOL/Library/FinFun.thy Tue Sep 03 01:12:40 2013 +0200 @@ -960,7 +960,7 @@ { fix g' a b show "Abs_finfun (g \ op $ g'(a $:= b)) = (Abs_finfun (g \ op $ g'))(a $:= g b)" proof - obtain y where y: "y \ finfun" and g': "g' = Abs_finfun y" by(cases g') - moreover hence "(g \ op $ g') \ finfun" by(simp add: finfun_left_compose) + moreover from g' have "(g \ op $ g') \ finfun" by(simp add: finfun_left_compose) moreover have "g \ y(a := b) = (g \ y)(a := g b)" by(auto) ultimately show ?thesis by(simp add: finfun_comp_def finfun_update_def) qed } diff -r 3ca9e79ac926 -r a14d2a854c02 src/HOL/Library/Formal_Power_Series.thy --- a/src/HOL/Library/Formal_Power_Series.thy Tue Sep 03 00:51:08 2013 +0200 +++ b/src/HOL/Library/Formal_Power_Series.thy Tue Sep 03 01:12:40 2013 +0200 @@ -3804,8 +3804,8 @@ by (simp add: split_if_asm dist_fps_def) moreover from fps_eq_least_unique[OF `f \ g`] - obtain n where "leastP (\n. f$n \ g$n) n" "The (leastP (\n. f $ n \ g $ n)) = n" by blast - moreover hence "\m. m < n \ f$m = g$m" "f$n \ g$n" + obtain n where n: "leastP (\n. f$n \ g$n) n" "The (leastP (\n. f $ n \ g $ n)) = n" by blast + moreover from n have "\m. m < n \ f$m = g$m" "f$n \ g$n" by (auto simp add: leastP_def setge_def) ultimately show ?thesis using `j \ i` by simp next diff -r 3ca9e79ac926 -r a14d2a854c02 src/HOL/Library/Fraction_Field.thy --- a/src/HOL/Library/Fraction_Field.thy Tue Sep 03 00:51:08 2013 +0200 +++ b/src/HOL/Library/Fraction_Field.thy Tue Sep 03 01:12:40 2013 +0200 @@ -209,7 +209,7 @@ next case False then obtain a b where "q = Fract a b" and "b \ 0" by (cases q) auto - moreover with False have "0 \ Fract a b" by simp + with False have "0 \ Fract a b" by simp with `b \ 0` have "a \ 0" by (simp add: Zero_fract_def eq_fract) with Fract `q = Fract a b` `b \ 0` show thesis by auto qed diff -r 3ca9e79ac926 -r a14d2a854c02 src/HOL/Library/Liminf_Limsup.thy --- a/src/HOL/Library/Liminf_Limsup.thy Tue Sep 03 00:51:08 2013 +0200 +++ b/src/HOL/Library/Liminf_Limsup.thy Tue Sep 03 01:12:40 2013 +0200 @@ -171,8 +171,8 @@ have "\P. eventually P F \ y < INFI (Collect P) X" proof cases assume "\z. y < z \ z < C" - then guess z .. - moreover then have "z \ INFI {x. z < X x} X" + then guess z .. note z = this + moreover from z have "z \ INFI {x. z < X x} X" by (auto intro!: INF_greatest) ultimately show ?thesis using y by (intro exI[of _ "\x. z < X x"]) auto @@ -203,7 +203,7 @@ show "f0 \ y" proof cases assume "\z. y < z \ z < f0" - then guess z .. + then obtain z where "y < z \ z < f0" .. moreover have "z \ INFI {x. z < f x} f" by (rule INF_greatest) simp ultimately show ?thesis diff -r 3ca9e79ac926 -r a14d2a854c02 src/HOL/Library/Permutations.thy --- a/src/HOL/Library/Permutations.thy Tue Sep 03 00:51:08 2013 +0200 +++ b/src/HOL/Library/Permutations.thy Tue Sep 03 01:12:40 2013 +0200 @@ -166,8 +166,8 @@ have xfgpF': "?xF = ?g ` ?pF'" . have Fs: "card F = n - 1" using `x \ F` H0 `finite F` by auto from insert.hyps Fs have pFs: "card ?pF = fact (n - 1)" using `finite F` by auto - moreover hence "finite ?pF" using fact_gt_zero_nat by (auto intro: card_ge_0_finite) - ultimately have pF'f: "finite ?pF'" using H0 `finite F` + then have "finite ?pF" using fact_gt_zero_nat by (auto intro: card_ge_0_finite) + then have pF'f: "finite ?pF'" using H0 `finite F` apply (simp only: Collect_split Collect_mem_eq) apply (rule finite_cartesian_product) apply simp_all @@ -195,7 +195,7 @@ thus ?thesis unfolding inj_on_def by blast qed from `x \ F` H0 have n0: "n \ 0 " using `finite F` by auto - hence "\m. n = Suc m" by arith + hence "\m. n = Suc m" by presburger then obtain m where n[simp]: "n = Suc m" by blast from pFs H0 have xFc: "card ?xF = fact n" unfolding xfgpF' card_image[OF ginj] using `finite F` `finite ?pF` diff -r 3ca9e79ac926 -r a14d2a854c02 src/HOL/Library/RBT_Impl.thy --- a/src/HOL/Library/RBT_Impl.thy Tue Sep 03 00:51:08 2013 +0200 +++ b/src/HOL/Library/RBT_Impl.thy Tue Sep 03 01:12:40 2013 +0200 @@ -146,8 +146,7 @@ = Set.insert k (dom (rbt_lookup t1) \ dom (rbt_lookup t2))" proof - assume "rbt_sorted (Branch c t1 k v t2)" - moreover from this have "rbt_sorted t1" "rbt_sorted t2" by simp_all - ultimately show ?thesis by (simp add: rbt_lookup_keys) + then show ?thesis by (simp add: rbt_lookup_keys) qed lemma finite_dom_rbt_lookup [simp, intro!]: "finite (dom (rbt_lookup t))" @@ -1405,14 +1404,14 @@ proof(cases "n mod 2 = 0") case True note ge0 moreover from "1.prems" have n2: "n div 2 \ length kvs" by simp - moreover with True have "P (n div 2) kvs" by(rule IH) + moreover from True n2 have "P (n div 2) kvs" by(rule IH) moreover from length_rbtreeify_f[OF n2] ge0 "1.prems" obtain t k v kvs' where kvs': "rbtreeify_f (n div 2) kvs = (t, (k, v) # kvs')" by(cases "snd (rbtreeify_f (n div 2) kvs)") (auto simp add: snd_def split: prod.split_asm) moreover from "1.prems" length_rbtreeify_f[OF n2] ge0 - have "n div 2 \ Suc (length kvs')" by(simp add: kvs') - moreover with True kvs'[symmetric] refl refl + have n2': "n div 2 \ Suc (length kvs')" by(simp add: kvs') + moreover from True kvs'[symmetric] refl refl n2' have "Q (n div 2) kvs'" by(rule IH) moreover note feven[unfolded feven_def] (* FIXME: why does by(rule feven[unfolded feven_def]) not work? *) @@ -1421,14 +1420,14 @@ next case False note ge0 moreover from "1.prems" have n2: "n div 2 \ length kvs" by simp - moreover with False have "P (n div 2) kvs" by(rule IH) + moreover from False n2 have "P (n div 2) kvs" by(rule IH) moreover from length_rbtreeify_f[OF n2] ge0 "1.prems" obtain t k v kvs' where kvs': "rbtreeify_f (n div 2) kvs = (t, (k, v) # kvs')" by(cases "snd (rbtreeify_f (n div 2) kvs)") (auto simp add: snd_def split: prod.split_asm) moreover from "1.prems" length_rbtreeify_f[OF n2] ge0 False - have "n div 2 \ length kvs'" by(simp add: kvs') arith - moreover with False kvs'[symmetric] refl refl have "P (n div 2) kvs'" by(rule IH) + have n2': "n div 2 \ length kvs'" by(simp add: kvs') arith + moreover from False kvs'[symmetric] refl refl n2' have "P (n div 2) kvs'" by(rule IH) moreover note fodd[unfolded fodd_def] ultimately have "P (Suc (2 * (n div 2))) kvs" by - thus ?thesis using False @@ -1451,14 +1450,14 @@ proof(cases "n mod 2 = 0") case True note ge0 moreover from "2.prems" have n2: "n div 2 \ Suc (length kvs)" by simp - moreover with True have "Q (n div 2) kvs" by(rule IH) + moreover from True n2 have "Q (n div 2) kvs" by(rule IH) moreover from length_rbtreeify_g[OF ge0 n2] ge0 "2.prems" obtain t k v kvs' where kvs': "rbtreeify_g (n div 2) kvs = (t, (k, v) # kvs')" by(cases "snd (rbtreeify_g (n div 2) kvs)") (auto simp add: snd_def split: prod.split_asm) moreover from "2.prems" length_rbtreeify_g[OF ge0 n2] ge0 - have "n div 2 \ Suc (length kvs')" by(simp add: kvs') - moreover with True kvs'[symmetric] refl refl + have n2': "n div 2 \ Suc (length kvs')" by(simp add: kvs') + moreover from True kvs'[symmetric] refl refl n2' have "Q (n div 2) kvs'" by(rule IH) moreover note geven[unfolded geven_def] ultimately have "Q (2 * (n div 2)) kvs" by - @@ -1467,14 +1466,14 @@ next case False note ge0 moreover from "2.prems" have n2: "n div 2 \ length kvs" by simp - moreover with False have "P (n div 2) kvs" by(rule IH) + moreover from False n2 have "P (n div 2) kvs" by(rule IH) moreover from length_rbtreeify_f[OF n2] ge0 "2.prems" False obtain t k v kvs' where kvs': "rbtreeify_f (n div 2) kvs = (t, (k, v) # kvs')" by(cases "snd (rbtreeify_f (n div 2) kvs)") (auto simp add: snd_def split: prod.split_asm, arith) moreover from "2.prems" length_rbtreeify_f[OF n2] ge0 False - have "n div 2 \ Suc (length kvs')" by(simp add: kvs') arith - moreover with False kvs'[symmetric] refl refl + have n2': "n div 2 \ Suc (length kvs')" by(simp add: kvs') arith + moreover from False kvs'[symmetric] refl refl n2' have "Q (n div 2) kvs'" by(rule IH) moreover note godd[unfolded godd_def] ultimately have "Q (Suc (2 * (n div 2))) kvs" by - diff -r 3ca9e79ac926 -r a14d2a854c02 src/HOL/Library/Ramsey.thy --- a/src/HOL/Library/Ramsey.thy Tue Sep 03 00:51:08 2013 +0200 +++ b/src/HOL/Library/Ramsey.thy Tue Sep 03 01:12:40 2013 +0200 @@ -326,11 +326,11 @@ have part2: "\X. X \ Z & finite X & card X = 2 --> f X < s" using part by (fastforce simp add: eval_nat_numeral card_Suc_eq) obtain Y t - where "Y \ Z" "infinite Y" "t < s" + where *: "Y \ Z" "infinite Y" "t < s" "(\X. X \ Y & finite X & card X = 2 --> f X = t)" by (insert Ramsey [OF infZ part2]) auto - moreover from this have "\x\Y. \y\Y. x \ y \ f {x, y} = t" by auto - ultimately show ?thesis by iprover + then have "\x\Y. \y\Y. x \ y \ f {x, y} = t" by auto + with * show ?thesis by iprover qed diff -r 3ca9e79ac926 -r a14d2a854c02 src/HOL/Library/Zorn.thy --- a/src/HOL/Library/Zorn.thy Tue Sep 03 00:51:08 2013 +0200 +++ b/src/HOL/Library/Zorn.thy Tue Sep 03 01:12:40 2013 +0200 @@ -119,9 +119,9 @@ lemma chain_sucD: assumes "chain X" shows "suc X \ A \ chain (suc X)" proof - - from `chain X` have "chain (suc X)" by (rule chain_suc) - moreover then have "suc X \ A" unfolding chain_def by blast - ultimately show ?thesis by blast + from `chain X` have *: "chain (suc X)" by (rule chain_suc) + then have "suc X \ A" unfolding chain_def by blast + with * show ?thesis by blast qed lemma suc_Union_closed_total': @@ -348,8 +348,8 @@ moreover have "\x\C. x \ X" using `\C \ X` by auto ultimately have "subset.chain A ?C" using subset.chain_extend [of A C X] and `X \ A` by auto - moreover assume "\C \ X" - moreover then have "C \ ?C" using `\C \ X` by auto + moreover assume **: "\C \ X" + moreover from ** have "C \ ?C" using `\C \ X` by auto ultimately show False using * by blast qed @@ -578,11 +578,11 @@ case 0 show ?case by fact next case (Suc i) - moreover obtain s where "s \ R" and "(f (Suc (Suc i)), f(Suc i)) \ s" + then obtain s where s: "s \ R" "(f (Suc (Suc i)), f(Suc i)) \ s" using 1 by auto - moreover hence "s initial_segment_of r \ r initial_segment_of s" + then have "s initial_segment_of r \ r initial_segment_of s" using assms(1) `r \ R` by (simp add: Chains_def) - ultimately show ?case by (simp add: init_seg_of_def) blast + with Suc s show ?case by (simp add: init_seg_of_def) blast qed } thus False using assms(2) and `r \ R` @@ -682,15 +682,14 @@ qed ultimately have "Well_order ?m" by (simp add: order_on_defs) --{*We show that the extension is above m*} - moreover hence "(m, ?m) \ I" using `Well_order m` and `x \ Field m` + moreover have "(m, ?m) \ I" using `Well_order ?m` and `Well_order m` and `x \ Field m` by (fastforce simp: I_def init_seg_of_def Field_def) ultimately --{*This contradicts maximality of m:*} have False using max and `x \ Field m` unfolding Field_def by blast } hence "Field m = UNIV" by auto - moreover with `Well_order m` have "Well_order m" by simp - ultimately show ?thesis by blast + with `Well_order m` show ?thesis by blast qed corollary well_order_on: "\r::'a rel. well_order_on A r" diff -r 3ca9e79ac926 -r a14d2a854c02 src/HOL/List.thy --- a/src/HOL/List.thy Tue Sep 03 00:51:08 2013 +0200 +++ b/src/HOL/List.thy Tue Sep 03 01:12:40 2013 +0200 @@ -722,12 +722,18 @@ using `xs \ []` proof (induct xs) case Nil then show ?case by simp next - case (Cons x xs) show ?case proof (cases xs) - case Nil with single show ?thesis by simp + case (Cons x xs) + show ?case + proof (cases xs) + case Nil + with single show ?thesis by simp next - case Cons then have "xs \ []" by simp - moreover with Cons.hyps have "P xs" . - ultimately show ?thesis by (rule cons) + case Cons + show ?thesis + proof (rule cons) + from Cons show "xs \ []" by simp + with Cons.hyps show "P xs" . + qed qed qed @@ -1061,12 +1067,13 @@ lemma map_eq_imp_length_eq: assumes "map f xs = map g ys" shows "length xs = length ys" -using assms proof (induct ys arbitrary: xs) + using assms +proof (induct ys arbitrary: xs) case Nil then show ?case by simp next case (Cons y ys) then obtain z zs where xs: "xs = z # zs" by auto from Cons xs have "map f zs = map g ys" by simp - moreover with Cons have "length zs = length ys" by blast + with Cons have "length zs = length ys" by blast with xs show ?case by simp qed @@ -1669,10 +1676,10 @@ hence n: "n < Suc (length xs)" by simp moreover { assume "n < length xs" - with n obtain n' where "length xs - n = Suc n'" + with n obtain n' where n': "length xs - n = Suc n'" by (cases "length xs - n", auto) moreover - then have "length xs - Suc n = n'" by simp + from n' have "length xs - Suc n = n'" by simp ultimately have "xs ! (length xs - Suc n) = (x # xs) ! (length xs - n)" by simp } @@ -3801,14 +3808,12 @@ then have "\m n zs. concat (replicate m zs) = xs' \ concat (replicate n zs) = ws" using False and `xs' \ []` and `ys' = xs' @ ws` and len by (intro less.hyps) auto - then obtain m n zs where "concat (replicate m zs) = xs'" + then obtain m n zs where *: "concat (replicate m zs) = xs'" and "concat (replicate n zs) = ws" by blast - moreover then have "concat (replicate (m + n) zs) = ys'" using `ys' = xs' @ ws` by (simp add: replicate_add) - ultimately - show ?thesis by blast + with * show ?thesis by blast qed then show ?case using xs'_def ys'_def by metis @@ -4074,8 +4079,8 @@ case Nil thus ?case by simp next case (Cons a xs) - moreover hence "!x. x: set xs \ x \ a" by auto - ultimately show ?case by(simp add: sublist_Cons cong:filter_cong) + then have "!x. x: set xs \ x \ a" by auto + with Cons show ?case by(simp add: sublist_Cons cong:filter_cong) qed @@ -4195,8 +4200,8 @@ hence "foldr (\xs. max (length xs)) xss 0 = 0" proof (induct xss) case (Cons x xs) - moreover hence "x = []" by (cases x) auto - ultimately show ?case by auto + then have "x = []" by (cases x) auto + with Cons show ?case by auto qed simp thus ?thesis using True by simp next @@ -4585,7 +4590,7 @@ proof - from assms have "map f xs = map f ys" by (simp add: sorted_distinct_set_unique) - moreover with `inj_on f (set xs \ set ys)` show "xs = ys" + with `inj_on f (set xs \ set ys)` show "xs = ys" by (blast intro: map_inj_on) qed @@ -4620,11 +4625,12 @@ lemma foldr_max_sorted: assumes "sorted (rev xs)" shows "foldr max xs y = (if xs = [] then y else max (xs ! 0) y)" -using assms proof (induct xs) + using assms +proof (induct xs) case (Cons x xs) - moreover hence "sorted (rev xs)" using sorted_append by auto - ultimately show ?case - by (cases xs, auto simp add: sorted_append max_def) + then have "sorted (rev xs)" using sorted_append by auto + with Cons show ?case + by (cases xs) (auto simp add: sorted_append max_def) qed simp lemma filter_equals_takeWhile_sorted_rev: diff -r 3ca9e79ac926 -r a14d2a854c02 src/HOL/Map.thy --- a/src/HOL/Map.thy Tue Sep 03 00:51:08 2013 +0200 +++ b/src/HOL/Map.thy Tue Sep 03 01:12:40 2013 +0200 @@ -715,18 +715,19 @@ by (rule set_map_of_compr) ultimately show ?rhs by simp next - assume ?rhs show ?lhs proof + assume ?rhs show ?lhs + proof fix k show "map_of xs k = map_of ys k" proof (cases "map_of xs k") case None - moreover with `?rhs` have "map_of ys k = None" + with `?rhs` have "map_of ys k = None" by (simp add: map_of_eq_None_iff) - ultimately show ?thesis by simp + with None show ?thesis by simp next case (Some v) - moreover with distinct `?rhs` have "map_of ys k = Some v" + with distinct `?rhs` have "map_of ys k = Some v" by simp - ultimately show ?thesis by simp + with Some show ?thesis by simp qed qed qed diff -r 3ca9e79ac926 -r a14d2a854c02 src/HOL/MicroJava/J/TypeRel.thy --- a/src/HOL/MicroJava/J/TypeRel.thy Tue Sep 03 00:51:08 2013 +0200 +++ b/src/HOL/MicroJava/J/TypeRel.thy Tue Sep 03 01:12:40 2013 +0200 @@ -144,8 +144,8 @@ where "class": "class G C = Some (D', fs', ms')" unfolding class_def by(auto dest!: weak_map_of_SomeI) hence "G \ C \C1 D'" using `C \ Object` .. - hence "(C, D') \ (subcls1 G)^+" .. - also with acyc have "C \ D'" by(auto simp add: acyclic_def) + hence *: "(C, D') \ (subcls1 G)^+" .. + also from * acyc have "C \ D'" by(auto simp add: acyclic_def) with subcls "class" have "(D', C) \ (subcls1 G)^+" by(auto dest: rtranclD) finally show False using acyc by(auto simp add: acyclic_def) qed diff -r 3ca9e79ac926 -r a14d2a854c02 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Tue Sep 03 00:51:08 2013 +0200 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Tue Sep 03 01:12:40 2013 +0200 @@ -2743,10 +2743,10 @@ using subspace_substandard[of "\i. i \ d"] . ultimately have "span d \ ?B" using span_mono[of d "?B"] span_eq[of "?B"] by blast - moreover have "card d \ dim (span d)" + moreover have *: "card d \ dim (span d)" using independent_card_le_dim[of d "span d"] independent_substdbasis[OF assms] span_inc[of d] by auto - moreover then have "dim ?B \ dim (span d)" + moreover from * have "dim ?B \ dim (span d)" using dim_substandard[OF assms] by auto ultimately show ?thesis using s subspace_dim_equal[of "span d" "?B"] subspace_span[of d] by auto @@ -8604,7 +8604,7 @@ { fix i assume "i:I" { assume "e i = 0" have ge: "u * (c i) >= 0 & v * (d i) >= 0" using xc yc uv `i:I` by (simp add: mult_nonneg_nonneg) - moreover hence "u * (c i) <= 0 & v * (d i) <= 0" using `e i = 0` e_def `i:I` by simp + moreover from ge have "u * (c i) <= 0 & v * (d i) <= 0" using `e i = 0` e_def `i:I` by simp ultimately have "u * (c i) = 0 & v * (d i) = 0" by auto hence "(u * (c i))*\<^sub>R (s i)+(v * (d i))*\<^sub>R (t i) = (e i) *\<^sub>R (q i)" using `e i = 0` by auto diff -r 3ca9e79ac926 -r a14d2a854c02 src/HOL/Multivariate_Analysis/Derivative.thy --- a/src/HOL/Multivariate_Analysis/Derivative.thy Tue Sep 03 00:51:08 2013 +0200 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy Tue Sep 03 01:12:40 2013 +0200 @@ -1441,14 +1441,14 @@ have *:"(\x. x *\<^sub>R f') = (\x. x *\<^sub>R f'')" apply(rule frechet_derivative_unique_within_closed_interval[of "a" "b"]) using assms(3-)[unfolded has_vector_derivative_def] using assms(1-2) - by (auto simp: Basis_real_def) + by auto show ?thesis proof(rule ccontr) - assume "f' \ f''" - moreover - hence "(\x. x *\<^sub>R f') 1 = (\x. x *\<^sub>R f'') 1" - using * by (auto simp: fun_eq_iff) - ultimately show False unfolding o_def by auto + assume **: "f' \ f''" + with * have "(\x. x *\<^sub>R f') 1 = (\x. x *\<^sub>R f'') 1" + by (auto simp: fun_eq_iff) + with ** show False + unfolding o_def by auto qed qed diff -r 3ca9e79ac926 -r a14d2a854c02 src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy --- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Tue Sep 03 00:51:08 2013 +0200 +++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Tue Sep 03 01:12:40 2013 +0200 @@ -63,10 +63,10 @@ assumes "closed S" "S \ {}" shows "Sup S \ S" proof - from compact_eq_closed[of S] compact_attains_sup[of S] assms - obtain s where "s \ S" "\t\S. t \ s" by auto - moreover then have "Sup S = s" + obtain s where S: "s \ S" "\t\S. t \ s" by auto + then have "Sup S = s" by (auto intro!: Sup_eqI) - ultimately show ?thesis + with S show ?thesis by simp qed @@ -75,10 +75,10 @@ assumes "closed S" "S \ {}" shows "Inf S \ S" proof - from compact_eq_closed[of S] compact_attains_inf[of S] assms - obtain s where "s \ S" "\t\S. s \ t" by auto - moreover then have "Inf S = s" + obtain s where S: "s \ S" "\t\S. s \ t" by auto + then have "Inf S = s" by (auto intro!: Inf_eqI) - ultimately show ?thesis + with S show ?thesis by simp qed diff -r 3ca9e79ac926 -r a14d2a854c02 src/HOL/Multivariate_Analysis/Integration.thy --- a/src/HOL/Multivariate_Analysis/Integration.thy Tue Sep 03 00:51:08 2013 +0200 +++ b/src/HOL/Multivariate_Analysis/Integration.thy Tue Sep 03 01:12:40 2013 +0200 @@ -905,12 +905,11 @@ then show "\a b. k = {a..b}" by auto have "k \ {a..b} \ k \ {}" proof (simp add: k interval_eq_empty subset_interval not_less, safe) - fix i :: 'a assume i: "i \ Basis" - moreover + fix i :: 'a + assume i: "i \ Basis" with f have "f i = (a, c) \ f i = (c, d) \ f i = (d, b)" by (auto simp: PiE_iff) - moreover note ord[of i] - ultimately + with i ord[of i] show "a \ i \ fst (f i) \ i" "snd (f i) \ i \ b \ i" "fst (f i) \ i \ snd (f i) \ i" by (auto simp: subset_iff eucl_le[where 'a='a]) qed @@ -952,7 +951,7 @@ by auto qed then guess f unfolding bchoice_iff .. note f = this - moreover then have "restrict f Basis \ Basis \\<^sub>E {(a, c), (c, d), (d, b)}" + moreover from f have "restrict f Basis \ Basis \\<^sub>E {(a, c), (c, d), (d, b)}" by auto moreover from f have "x \ ?B (restrict f Basis)" by (auto simp: mem_interval eucl_le[where 'a='a]) @@ -3874,7 +3873,7 @@ setprod_timesf setprod_constant inner_diff_left) next case False - moreover with as have "{m *\<^sub>R b + c..m *\<^sub>R a + c} \ {}" + with as have "{m *\<^sub>R b + c..m *\<^sub>R a + c} \ {}" unfolding interval_ne_empty apply (intro ballI) apply (erule_tac x=i in ballE) @@ -3882,7 +3881,7 @@ done moreover from False have *: "\i. (m *\<^sub>R a + c) \ i - (m *\<^sub>R b + c) \ i = (-m) *\<^sub>R (b - a) \ i" by (simp add: inner_simps field_simps) - ultimately show ?thesis + ultimately show ?thesis using False by (simp add: image_affinity_interval content_closed_interval' setprod_timesf[symmetric] setprod_constant[symmetric] inner_diff_left) qed @@ -3918,17 +3917,20 @@ unfolding interval_ne_empty by auto show "(\xa. x \ i = m i * xa \ a \ i \ xa \ xa \ b \ i) \ min (m i * (a \ i)) (m i * (b \ i)) \ x \ i \ x \ i \ max (m i * (a \ i)) (m i * (b \ i))" - proof cases - assume "m i \ 0" - moreover then have *: "\a b. a = m i * b \ b = a / m i" + proof (cases "m i = 0") + case True + with a_le_b show ?thesis by auto + next + case False + then have *: "\a b. a = m i * b \ b = a / m i" by (auto simp add: field_simps) - moreover have + from False have "min (m i * (a \