tuned proofs -- clarified flow of facts wrt. calculation;
--- 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 \<in> Units G"
have "b \<otimes> inv c = a \<otimes> c \<otimes> inv c" by (simp add: b)
- also with ccarr acarr cunit
+ also from ccarr acarr cunit
have "\<dots> = a \<otimes> (c \<otimes> inv c)" by (fast intro: m_assoc)
- also with ccarr cunit
+ also from ccarr cunit
have "\<dots> = a \<otimes> \<one>" by (simp add: Units_r_inv)
- also with acarr
+ also from acarr
have "\<dots> = a" by simp
finally have "a = b \<otimes> inv c" by simp
with ccarr cunit
--- 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 "\<forall>xs \<in> sset (stl s). xs \<noteq> []" using less(2) by (cases s) auto
ultimately have "\<exists>n m'. x = stl s !! n ! m' \<and> m' < length (stl s !! n)" by (intro less(1)) auto
--- 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 \<Rightarrow> nat"
assume "M1 \<in> multiset" "M2 \<in> multiset"
- moreover
hence "setsum M1 {a. f a = x \<and> 0 < M1 a} = setsum M1 {a. f a = x \<and> 0 < M1 a + M2 a}"
"setsum M2 {a. f a = x \<and> 0 < M2 a} = setsum M2 {a. f a = x \<and> 0 < M1 a + M2 a}"
by (auto simp: multiset_def intro!: setsum_mono_zero_cong_left)
- ultimately show "(\<Sum>a | f a = x \<and> 0 < M1 a + M2 a. M1 a + M2 a) =
+ then show "(\<Sum>a | f a = x \<and> 0 < M1 a + M2 a. M1 a + M2 a) =
setsum M1 {a. f a = x \<and> 0 < M1 a} +
setsum M2 {a. f a = x \<and> 0 < M2 a}"
by (auto simp: setsum.distrib[symmetric])
--- 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 \<in> A` obtain B where A: "A = insert x B" and "x \<notin> 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
--- 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 "\<Sqinter>A \<sqsubseteq> u"
proof -
from `A \<noteq> {}` obtain v where "v \<in> A" by blast
- moreover with assms have "v \<sqsubseteq> u" by blast
+ moreover from `v \<in> A` assms(1) have "v \<sqsubseteq> u" by blast
ultimately show ?thesis by (rule Inf_lower2)
qed
@@ -260,7 +260,7 @@
shows "u \<sqsubseteq> \<Squnion>A"
proof -
from `A \<noteq> {}` obtain v where "v \<in> A" by blast
- moreover with assms have "u \<sqsubseteq> v" by blast
+ moreover from `v \<in> A` assms(1) have "u \<sqsubseteq> v" by blast
ultimately show ?thesis by (rule Sup_upper2)
qed
--- 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 \<noteq> 0` show "arg z = x"
--- 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
--- 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 \<noteq> 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 \<noteq> 0" by simp
--- 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)]
--- 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 \<noteq> 0"
- moreover from this have h: "h \<noteq> 0"
+ assume **: "F h \<noteq> 0"
+ then have h: "h \<noteq> 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: "\<And>x. x \<noteq> 0 \<Longrightarrow> norm x < s \<Longrightarrow> ?r x < ?r h" by auto
@@ -528,11 +528,11 @@
lemma differentiable_def: "(f::real \<Rightarrow> real) differentiable x in s \<longleftrightarrow> (\<exists>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' = (\<lambda>x. x * c)"
+ then obtain c where "f' = (\<lambda>x. x * c)"
by (metis real_bounded_linear FDERIV_bounded_linear)
- ultimately show "\<exists>D. DERIV f x : s :> D"
+ with * show "\<exists>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 \<longleftrightarrow> DERIV g y :> v"
unfolding DERIV_iff2
proof (rule filterlim_cong)
- assume "eventually (\<lambda>x. f x = g x) (nhds x)"
- moreover then have "f x = g x" by (auto simp: eventually_nhds)
+ assume *: "eventually (\<lambda>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 (\<lambda>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 "\<dots> = (b - a) * (g'c * (f b - f a) - f'c * (g b - g a))" by simp
+ also from leq have "\<dots> = (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 "\<exists>c. 0 < c \<and> c < x \<and> (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 "\<exists>y. 0 < y \<and> y < x \<and> f x / g x = f' y / g' y"
using `f 0 = 0` `g 0 = 0` by (auto intro!: exI[of _ c])
--- 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 \<noteq> 0` assms have "fst qr = fst qr'"
+ from `n \<noteq> 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 {*
--- 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 "... \<le> 0" by simp
+ assume *: "1 < inverse x"
+ also from notless and * have "... \<le> 0" by simp
also have "... < 1" by (rule zero_less_one)
finally show False by auto
qed
--- 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 \<in> A` obtain B where A: "A = insert x B" and "x \<notin> 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
--- 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
--- 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 \<le> p \<and> p \<le> r"
assume i_outer: "i < l \<or> 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 \<guillemotright>= 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 \<guillemotright>= 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 \<guillemotright>= g) h" by (rule success_bind_effectI)
qed
lemma success_partitionI:
--- 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
--- 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 @@
"-\<infinity> + -\<infinity> = -(\<infinity>::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]:
"(\<infinity>::ereal) \<noteq> 0" "0 \<noteq> (\<infinity>::ereal)"
@@ -234,8 +234,8 @@
| " -\<infinity> < (\<infinity>::ereal) \<longleftrightarrow> 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 @@
"-(\<infinity>::ereal) * -\<infinity> = \<infinity>"
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 = \<infinity>" have ?thesis
proof cases
- assume "\<forall>i. f i = 0"
- moreover then have "range f = {0}" by auto
- ultimately show "c * SUPR UNIV f \<le> y" using *
+ assume **: "\<forall>i. f i = 0"
+ then have "range f = {0}" by auto
+ with ** show "c * SUPR UNIV f \<le> y" using *
by (auto simp: SUP_def min_max.sup_absorb1)
next
assume "\<not> (\<forall>i. f i = 0)"
@@ -1417,9 +1417,9 @@
from `A \<noteq> {}` obtain x where "x \<in> A" by auto
show ?thesis
proof cases
- assume "\<infinity> \<in> A"
- moreover then have "\<infinity> \<le> Sup A" by (intro complete_lattice_class.Sup_upper)
- ultimately show ?thesis by (auto intro!: exI[of _ "\<lambda>x. \<infinity>"])
+ assume *: "\<infinity> \<in> A"
+ then have "\<infinity> \<le> Sup A" by (intro complete_lattice_class.Sup_upper)
+ with * show ?thesis by (auto intro!: exI[of _ "\<lambda>x. \<infinity>"])
next
assume "\<infinity> \<notin> A"
have "\<exists>x\<in>A. 0 \<le> x"
@@ -1489,10 +1489,13 @@
fixes A :: "ereal set" assumes "A \<noteq> {}" and "\<bar>a\<bar> \<noteq> \<infinity>"
shows "Inf ((\<lambda>x. a - x) ` A) = a - Sup A"
proof -
- { fix x have "-a - -x = -(a - x)" using assms by (cases x) auto }
- moreover then have "(\<lambda>x. -a - x)`uminus`A = uminus ` (\<lambda>x. a - x) ` A"
+ {
+ fix x
+ have "-a - -x = -(a - x)" using assms by (cases x) auto
+ } note * = this
+ then have "(\<lambda>x. -a - x)`uminus`A = uminus ` (\<lambda>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 "\<infinity> \<in> A \<Longrightarrow> {ereal x <..} \<subseteq> A" "\<infinity> \<in> B \<Longrightarrow> {ereal z <..} \<subseteq> B"
- by auto
- ultimately show ?case
+ then obtain x z where "\<infinity> \<in> A \<Longrightarrow> {ereal x <..} \<subseteq> A" "\<infinity> \<in> B \<Longrightarrow> {ereal z <..} \<subseteq> B"
+ by auto
+ with Int show ?case
by (intro exI[of _ "max x z"]) fastforce
next
{ fix x have "x \<noteq> \<infinity> \<Longrightarrow> \<exists>t. x \<le> 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 "-\<infinity> \<in> A \<Longrightarrow> {..< ereal x} \<subseteq> A" "-\<infinity> \<in> B \<Longrightarrow> {..< ereal z} \<subseteq> B"
- by auto
- ultimately show ?case
+ then obtain x z where "-\<infinity> \<in> A \<Longrightarrow> {..< ereal x} \<subseteq> A" "-\<infinity> \<in> B \<Longrightarrow> {..< ereal z} \<subseteq> B"
+ by auto
+ with Int show ?case
by (intro exI[of _ "min x z"]) fastforce
next
{ fix x have "x \<noteq> - \<infinity> \<Longrightarrow> \<exists>t. ereal t \<le> x" by (cases x) auto }
--- 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 \<circ> op $ g'(a $:= b)) = (Abs_finfun (g \<circ> op $ g'))(a $:= g b)"
proof -
obtain y where y: "y \<in> finfun" and g': "g' = Abs_finfun y" by(cases g')
- moreover hence "(g \<circ> op $ g') \<in> finfun" by(simp add: finfun_left_compose)
+ moreover from g' have "(g \<circ> op $ g') \<in> finfun" by(simp add: finfun_left_compose)
moreover have "g \<circ> y(a := b) = (g \<circ> y)(a := g b)" by(auto)
ultimately show ?thesis by(simp add: finfun_comp_def finfun_update_def)
qed }
--- 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 \<noteq> g`]
- obtain n where "leastP (\<lambda>n. f$n \<noteq> g$n) n" "The (leastP (\<lambda>n. f $ n \<noteq> g $ n)) = n" by blast
- moreover hence "\<And>m. m < n \<Longrightarrow> f$m = g$m" "f$n \<noteq> g$n"
+ 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
+ moreover from n have "\<And>m. m < n \<Longrightarrow> f$m = g$m" "f$n \<noteq> g$n"
by (auto simp add: leastP_def setge_def)
ultimately show ?thesis using `j \<le> i` by simp
next
--- 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 \<noteq> 0" by (cases q) auto
- moreover with False have "0 \<noteq> Fract a b" by simp
+ with False have "0 \<noteq> Fract a b" by simp
with `b \<noteq> 0` have "a \<noteq> 0" by (simp add: Zero_fract_def eq_fract)
with Fract `q = Fract a b` `b \<noteq> 0` show thesis by auto
qed
--- 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 "\<exists>P. eventually P F \<and> y < INFI (Collect P) X"
proof cases
assume "\<exists>z. y < z \<and> z < C"
- then guess z ..
- moreover then have "z \<le> INFI {x. z < X x} X"
+ then guess z .. note z = this
+ moreover from z have "z \<le> INFI {x. z < X x} X"
by (auto intro!: INF_greatest)
ultimately show ?thesis
using y by (intro exI[of _ "\<lambda>x. z < X x"]) auto
@@ -203,7 +203,7 @@
show "f0 \<le> y"
proof cases
assume "\<exists>z. y < z \<and> z < f0"
- then guess z ..
+ then obtain z where "y < z \<and> z < f0" ..
moreover have "z \<le> INFI {x. z < f x} f"
by (rule INF_greatest) simp
ultimately show ?thesis
--- 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 \<notin> 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 \<notin> F` H0 have n0: "n \<noteq> 0 " using `finite F` by auto
- hence "\<exists>m. n = Suc m" by arith
+ hence "\<exists>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`
--- 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) \<union> 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 \<le> 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 \<le> Suc (length kvs')" by(simp add: kvs')
- moreover with True kvs'[symmetric] refl refl
+ have n2': "n div 2 \<le> 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 \<le> 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 \<le> 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 \<le> 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 \<le> 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 \<le> Suc (length kvs')" by(simp add: kvs')
- moreover with True kvs'[symmetric] refl refl
+ have n2': "n div 2 \<le> 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 \<le> 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 \<le> Suc (length kvs')" by(simp add: kvs') arith
- moreover with False kvs'[symmetric] refl refl
+ have n2': "n div 2 \<le> 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 -
--- 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: "\<forall>X. X \<subseteq> 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 \<subseteq> Z" "infinite Y" "t < s"
+ where *: "Y \<subseteq> Z" "infinite Y" "t < s"
"(\<forall>X. X \<subseteq> Y & finite X & card X = 2 --> f X = t)"
by (insert Ramsey [OF infZ part2]) auto
- moreover from this have "\<forall>x\<in>Y. \<forall>y\<in>Y. x \<noteq> y \<longrightarrow> f {x, y} = t" by auto
- ultimately show ?thesis by iprover
+ then have "\<forall>x\<in>Y. \<forall>y\<in>Y. x \<noteq> y \<longrightarrow> f {x, y} = t" by auto
+ with * show ?thesis by iprover
qed
--- 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 \<subseteq> A \<and> chain (suc X)"
proof -
- from `chain X` have "chain (suc X)" by (rule chain_suc)
- moreover then have "suc X \<subseteq> 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 \<subseteq> A" unfolding chain_def by blast
+ with * show ?thesis by blast
qed
lemma suc_Union_closed_total':
@@ -348,8 +348,8 @@
moreover have "\<forall>x\<in>C. x \<subseteq> X" using `\<Union>C \<subseteq> X` by auto
ultimately have "subset.chain A ?C"
using subset.chain_extend [of A C X] and `X \<in> A` by auto
- moreover assume "\<Union>C \<noteq> X"
- moreover then have "C \<subset> ?C" using `\<Union>C \<subseteq> X` by auto
+ moreover assume **: "\<Union>C \<noteq> X"
+ moreover from ** have "C \<subset> ?C" using `\<Union>C \<subseteq> 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 \<in> R" and "(f (Suc (Suc i)), f(Suc i)) \<in> s"
+ then obtain s where s: "s \<in> R" "(f (Suc (Suc i)), f(Suc i)) \<in> s"
using 1 by auto
- moreover hence "s initial_segment_of r \<or> r initial_segment_of s"
+ then have "s initial_segment_of r \<or> r initial_segment_of s"
using assms(1) `r \<in> 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 \<in> 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) \<in> I" using `Well_order m` and `x \<notin> Field m`
+ moreover have "(m, ?m) \<in> I" using `Well_order ?m` and `Well_order m` and `x \<notin> 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 \<notin> 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: "\<exists>r::'a rel. well_order_on A r"
--- 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 \<noteq> []` 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 \<noteq> []" 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 \<noteq> []" 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 "\<exists>m n zs. concat (replicate m zs) = xs' \<and> concat (replicate n zs) = ws"
using False and `xs' \<noteq> []` 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 \<longrightarrow> x \<noteq> a" by auto
- ultimately show ?case by(simp add: sublist_Cons cong:filter_cong)
+ then have "!x. x: set xs \<longrightarrow> x \<noteq> a" by auto
+ with Cons show ?case by(simp add: sublist_Cons cong:filter_cong)
qed
@@ -4195,8 +4200,8 @@
hence "foldr (\<lambda>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 \<union> set ys)` show "xs = ys"
+ with `inj_on f (set xs \<union> 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:
--- 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
--- 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 \<turnstile> C \<prec>C1 D'" using `C \<noteq> Object` ..
- hence "(C, D') \<in> (subcls1 G)^+" ..
- also with acyc have "C \<noteq> D'" by(auto simp add: acyclic_def)
+ hence *: "(C, D') \<in> (subcls1 G)^+" ..
+ also from * acyc have "C \<noteq> D'" by(auto simp add: acyclic_def)
with subcls "class" have "(D', C) \<in> (subcls1 G)^+" by(auto dest: rtranclD)
finally show False using acyc by(auto simp add: acyclic_def)
qed
--- 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 "\<lambda>i. i \<notin> d"] .
ultimately have "span d \<subseteq> ?B"
using span_mono[of d "?B"] span_eq[of "?B"] by blast
- moreover have "card d \<le> dim (span d)"
+ moreover have *: "card d \<le> 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 \<le> dim (span d)"
+ moreover from * have "dim ?B \<le> 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
--- 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 *:"(\<lambda>x. x *\<^sub>R f') = (\<lambda>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' \<noteq> f''"
- moreover
- hence "(\<lambda>x. x *\<^sub>R f') 1 = (\<lambda>x. x *\<^sub>R f'') 1"
- using * by (auto simp: fun_eq_iff)
- ultimately show False unfolding o_def by auto
+ assume **: "f' \<noteq> f''"
+ with * have "(\<lambda>x. x *\<^sub>R f') 1 = (\<lambda>x. x *\<^sub>R f'') 1"
+ by (auto simp: fun_eq_iff)
+ with ** show False
+ unfolding o_def by auto
qed
qed
--- 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 \<noteq> {}" shows "Sup S \<in> S"
proof -
from compact_eq_closed[of S] compact_attains_sup[of S] assms
- obtain s where "s \<in> S" "\<forall>t\<in>S. t \<le> s" by auto
- moreover then have "Sup S = s"
+ obtain s where S: "s \<in> S" "\<forall>t\<in>S. t \<le> 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 \<noteq> {}" shows "Inf S \<in> S"
proof -
from compact_eq_closed[of S] compact_attains_inf[of S] assms
- obtain s where "s \<in> S" "\<forall>t\<in>S. s \<le> t" by auto
- moreover then have "Inf S = s"
+ obtain s where S: "s \<in> S" "\<forall>t\<in>S. s \<le> t" by auto
+ then have "Inf S = s"
by (auto intro!: Inf_eqI)
- ultimately show ?thesis
+ with S show ?thesis
by simp
qed
--- 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 "\<exists>a b. k = {a..b}" by auto
have "k \<subseteq> {a..b} \<and> k \<noteq> {}"
proof (simp add: k interval_eq_empty subset_interval not_less, safe)
- fix i :: 'a assume i: "i \<in> Basis"
- moreover
+ fix i :: 'a
+ assume i: "i \<in> Basis"
with f have "f i = (a, c) \<or> f i = (c, d) \<or> f i = (d, b)"
by (auto simp: PiE_iff)
- moreover note ord[of i]
- ultimately
+ with i ord[of i]
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"
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 \<in> Basis \<rightarrow>\<^sub>E {(a, c), (c, d), (d, b)}"
+ moreover from f have "restrict f Basis \<in> Basis \<rightarrow>\<^sub>E {(a, c), (c, d), (d, b)}"
by auto
moreover from f have "x \<in> ?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} \<noteq> {}"
+ with as have "{m *\<^sub>R b + c..m *\<^sub>R a + c} \<noteq> {}"
unfolding interval_ne_empty
apply (intro ballI)
apply (erule_tac x=i in ballE)
@@ -3882,7 +3881,7 @@
done
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"
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 "(\<exists>xa. x \<bullet> i = m i * xa \<and> a \<bullet> i \<le> xa \<and> xa \<le> b \<bullet> i) \<longleftrightarrow>
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))"
- proof cases
- assume "m i \<noteq> 0"
- moreover then have *: "\<And>a b. a = m i * b \<longleftrightarrow> b = a / m i"
+ proof (cases "m i = 0")
+ case True
+ with a_le_b show ?thesis by auto
+ next
+ case False
+ then have *: "\<And>a b. a = m i * b \<longleftrightarrow> b = a / m i"
by (auto simp add: field_simps)
- moreover have
+ from False have
"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))"
"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))"
using a_le_b by (auto simp: min_def max_def mult_le_cancel_left)
- ultimately show ?thesis using a_le_b
+ with False show ?thesis using a_le_b
unfolding * by (auto simp add: le_divide_eq divide_le_eq ac_simps)
- qed (insert a_le_b, auto)
+ qed
qed
qed simp
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Sep 03 00:51:08 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Sep 03 01:12:40 2013 +0200
@@ -288,8 +288,8 @@
next
fix S
assume "open S" "x \<in> S"
- from open_prod_elim[OF this] guess a' b' .
- moreover with A(4)[of a'] B(4)[of b']
+ from open_prod_elim[OF this] guess a' b' . note a'b' = this
+ moreover from a'b' A(4)[of a'] B(4)[of b']
obtain a b where "a \<in> A" "a \<subseteq> a'" "b \<in> B" "b \<subseteq> b'" by auto
ultimately show "\<exists>a\<in>(\<lambda>(a, b). a \<times> b) ` (A \<times> B). a \<subseteq> S"
by (auto intro!: bexI[of _ "a \<times> b"] bexI[of _ a] bexI[of _ b])
@@ -3264,12 +3264,12 @@
unfolding C_def by auto
qed
then have "U \<subseteq> \<Union>C" using `U \<subseteq> \<Union>A` by auto
- ultimately obtain T where "T\<subseteq>C" "finite T" "U \<subseteq> \<Union>T"
+ ultimately obtain T where T: "T\<subseteq>C" "finite T" "U \<subseteq> \<Union>T"
using * by metis
- moreover then have "\<forall>t\<in>T. \<exists>a\<in>A. t \<inter> U \<subseteq> a"
+ then have "\<forall>t\<in>T. \<exists>a\<in>A. t \<inter> U \<subseteq> a"
by (auto simp: C_def)
then guess f unfolding bchoice_iff Bex_def ..
- ultimately show "\<exists>T\<subseteq>A. finite T \<and> U \<subseteq> \<Union>T"
+ with T show "\<exists>T\<subseteq>A. finite T \<and> U \<subseteq> \<Union>T"
unfolding C_def by (intro exI[of _ "f`T"]) fastforce
qed
@@ -3708,10 +3708,9 @@
assume f: "bounded (range f)"
obtain r where r: "subseq r" "monoseq (f \<circ> r)"
unfolding comp_def by (metis seq_monosub)
- moreover
then have "Bseq (f \<circ> r)"
unfolding Bseq_eq_bounded using f by (auto intro: bounded_subset)
- ultimately show "\<exists>l r. subseq r \<and> (f \<circ> r) ----> l"
+ with r show "\<exists>l r. subseq r \<and> (f \<circ> r) ----> l"
using Bseq_monoseq_convergent[of "f \<circ> r"] by (auto simp: convergent_def)
qed
@@ -5558,9 +5557,9 @@
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"
by metis
then have "\<forall>y\<in>t. open (b y)" "t \<subseteq> (\<Union>y\<in>t. b y)" by auto
- from compactE_image[OF `compact t` this] obtain D where "D \<subseteq> t" "finite D" "t \<subseteq> (\<Union>y\<in>D. b y)"
+ from compactE_image[OF `compact t` this] obtain D where D: "D \<subseteq> t" "finite D" "t \<subseteq> (\<Union>y\<in>D. b y)"
by auto
- moreover with c have "(\<Inter>y\<in>D. a y) \<times> t \<subseteq> (\<Union>y\<in>D. c y)"
+ moreover from D c have "(\<Inter>y\<in>D. a y) \<times> t \<subseteq> (\<Union>y\<in>D. c y)"
by (fastforce simp: subset_eq)
ultimately show "\<exists>a. open a \<and> x \<in> a \<and> (\<exists>d\<subseteq>C. finite d \<and> a \<times> t \<subseteq> \<Union>d)"
using c by (intro exI[of _ "c`D"] exI[of _ "\<Inter>(a`D)"] conjI) (auto intro!: open_INT)
@@ -7345,8 +7344,8 @@
shows "\<exists>S\<subseteq>A. card S = n"
proof cases
assume "finite A"
- from ex_bij_betw_nat_finite[OF this] guess f ..
- moreover with `n \<le> card A` have "{..< n} \<subseteq> {..< card A}" "inj_on f {..< n}"
+ from ex_bij_betw_nat_finite[OF this] guess f .. note f = this
+ moreover from f `n \<le> card A` have "{..< n} \<subseteq> {..< card A}" "inj_on f {..< n}"
by (auto simp: bij_betw_def intro: subset_inj_on)
ultimately have "f ` {..< n} \<subseteq> A" "card (f ` {..< n}) = n"
by (auto simp: bij_betw_def card_image)
--- a/src/HOL/Nat.thy Tue Sep 03 00:51:08 2013 +0200
+++ b/src/HOL/Nat.thy Tue Sep 03 01:12:40 2013 +0200
@@ -1888,8 +1888,8 @@
proof -
have "m dvd n - q \<longleftrightarrow> m dvd r * m + (n - q)"
by (auto elim: dvd_plusE)
- also with assms have "\<dots> \<longleftrightarrow> m dvd r * m + n - q" by simp
- also with assms have "\<dots> \<longleftrightarrow> m dvd (r * m - q) + n" by simp
+ also from assms have "\<dots> \<longleftrightarrow> m dvd r * m + n - q" by simp
+ also from assms have "\<dots> \<longleftrightarrow> m dvd (r * m - q) + n" by simp
also have "\<dots> \<longleftrightarrow> m dvd n + (r * m - q)" by (simp add: add_commute)
finally show ?thesis .
qed
--- a/src/HOL/Nominal/Examples/Crary.thy Tue Sep 03 00:51:08 2013 +0200
+++ b/src/HOL/Nominal/Examples/Crary.thy Tue Sep 03 01:12:40 2013 +0200
@@ -766,9 +766,8 @@
assumes "\<Gamma>' \<turnstile> t is s over \<Gamma>"
shows "\<Gamma>' \<turnstile> s is s over \<Gamma>"
proof -
- have "\<Gamma>' \<turnstile> t is s over \<Gamma>" by fact
- moreover then have "\<Gamma>' \<turnstile> s is t over \<Gamma>" using logical_symmetry by blast
- ultimately show "\<Gamma>' \<turnstile> s is s over \<Gamma>" using logical_transitivity by blast
+ from assms have "\<Gamma>' \<turnstile> s is t over \<Gamma>" using logical_symmetry by blast
+ with assms show "\<Gamma>' \<turnstile> s is s over \<Gamma>" using logical_transitivity by blast
qed
lemma logical_subst_monotonicity :
--- a/src/HOL/Number_Theory/Binomial.thy Tue Sep 03 00:51:08 2013 +0200
+++ b/src/HOL/Number_Theory/Binomial.thy Tue Sep 03 01:12:40 2013 +0200
@@ -203,7 +203,7 @@
by (subst choose_reduce_nat, auto simp add: field_simps)
also note one
also note two
- also with less have "(n - k) * fact n + (k + 1) * fact n= fact (n + 1)"
+ also from less have "(n - k) * fact n + (k + 1) * fact n= fact (n + 1)"
apply (subst fact_plus_one_nat)
apply (subst distrib_right [symmetric])
apply simp
--- a/src/HOL/Number_Theory/MiscAlgebra.thy Tue Sep 03 00:51:08 2013 +0200
+++ b/src/HOL/Number_Theory/MiscAlgebra.thy Tue Sep 03 01:12:40 2013 +0200
@@ -298,7 +298,7 @@
proof -
have "(x \<oplus> \<one>) \<otimes> (x \<oplus> \<ominus> \<one>) = x \<otimes> x \<oplus> \<ominus> \<one>"
by (simp add: ring_simprules)
- also with `x \<otimes> x = \<one>` have "\<dots> = \<zero>"
+ also from `x \<otimes> x = \<one>` have "\<dots> = \<zero>"
by (simp add: ring_simprules)
finally have "(x \<oplus> \<one>) \<otimes> (x \<oplus> \<ominus> \<one>) = \<zero>" .
then have "(x \<oplus> \<one>) = \<zero> | (x \<oplus> \<ominus> \<one>) = \<zero>"
--- a/src/HOL/Predicate.thy Tue Sep 03 00:51:08 2013 +0200
+++ b/src/HOL/Predicate.thy Tue Sep 03 01:12:40 2013 +0200
@@ -225,9 +225,9 @@
"\<exists>!x. eval A x \<Longrightarrow> eval A (singleton dfault A)"
proof -
assume assm: "\<exists>!x. eval A x"
- then obtain x where "eval A x" ..
- moreover with assm have "singleton dfault A = x" by (rule singleton_eqI)
- ultimately show ?thesis by simp
+ then obtain x where x: "eval A x" ..
+ with assm have "singleton dfault A = x" by (rule singleton_eqI)
+ with x show ?thesis by simp
qed
lemma single_singleton:
--- a/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy Tue Sep 03 00:51:08 2013 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy Tue Sep 03 01:12:40 2013 +0200
@@ -54,7 +54,8 @@
sorted_single [code_pred_intro]
sorted_many [code_pred_intro]
-code_pred sorted proof -
+code_pred sorted
+proof -
assume "sorted xa"
assume 1: "xa = [] \<Longrightarrow> thesis"
assume 2: "\<And>x. xa = [x] \<Longrightarrow> thesis"
@@ -65,9 +66,12 @@
case (Cons x xs) show ?thesis proof (cases xs)
case Nil with Cons 2 show ?thesis by simp
next
- case (Cons y zs) with `xa = x # xs` have "xa = x # y # zs" by simp
- moreover with `sorted xa` have "x \<le> y" and "sorted (y # zs)" by simp_all
- ultimately show ?thesis by (rule 3)
+ case (Cons y zs)
+ show ?thesis
+ proof (rule 3)
+ from Cons `xa = x # xs` show "xa = x # y # zs" by simp
+ with `sorted xa` show "x \<le> y" and "sorted (y # zs)" by simp_all
+ qed
qed
qed
qed
--- a/src/HOL/Probability/Binary_Product_Measure.thy Tue Sep 03 00:51:08 2013 +0200
+++ b/src/HOL/Probability/Binary_Product_Measure.thy Tue Sep 03 01:12:40 2013 +0200
@@ -177,9 +177,9 @@
by (auto intro!: measurable_If simp: space_pair_measure)
next
case (union F)
- moreover then have *: "\<And>x. emeasure M (Pair x -` (\<Union>i. F i)) = (\<Sum>i. ?s (F i) x)"
+ then have "\<And>x. emeasure M (Pair x -` (\<Union>i. F i)) = (\<Sum>i. ?s (F i) x)"
by (simp add: suminf_emeasure disjoint_family_vimageI subset_eq vimage_UN sets_pair_measure[symmetric])
- ultimately show ?case
+ with union show ?case
unfolding sets_pair_measure[symmetric] by simp
qed (auto simp add: if_distrib Int_def[symmetric] intro!: measurable_If)
@@ -515,9 +515,9 @@
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 = _")
using f proof induct
case (cong u v)
- moreover then have "?I u = ?I v"
+ then have "?I u = ?I v"
by (intro positive_integral_cong) (auto simp: space_pair_measure)
- ultimately show ?case
+ with cong show ?case
by (simp cong: positive_integral_cong)
qed (simp_all add: emeasure_pair_measure positive_integral_cmult positive_integral_add
positive_integral_monotone_convergence_SUP
--- a/src/HOL/Probability/Fin_Map.thy Tue Sep 03 00:51:08 2013 +0200
+++ b/src/HOL/Probability/Fin_Map.thy Tue Sep 03 01:12:40 2013 +0200
@@ -342,9 +342,9 @@
case (UN K)
show ?case
proof safe
- fix x X assume "x \<in> X" "X \<in> K"
- moreover with UN obtain e where "e>0" "\<And>y. dist y x < e \<longrightarrow> y \<in> X" by force
- ultimately show "\<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> \<Union>K" by auto
+ fix x X assume "x \<in> X" and X: "X \<in> K"
+ with UN obtain e where "e>0" "\<And>y. dist y x < e \<longrightarrow> y \<in> X" by force
+ with X show "\<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> \<Union>K" by auto
qed
next
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
@@ -363,12 +363,10 @@
show "y \<in> s" unfolding s
proof
show "domain y = a" using d s `a \<noteq> {}` by (auto simp: dist_le_1_imp_domain_eq a_dom)
- fix i assume "i \<in> a"
- moreover
+ fix i assume i: "i \<in> a"
hence "dist ((y)\<^sub>F i) ((x)\<^sub>F i) < es i" using d
by (auto simp: dist_finmap_def `a \<noteq> {}` intro!: le_less_trans[OF dist_proj])
- ultimately
- show "y i \<in> b i" by (rule in_b)
+ with i show "y i \<in> b i" by (rule in_b)
qed
next
assume "\<not>a \<noteq> {}"
@@ -715,9 +713,9 @@
proof -
have "\<Union>{f s|s. P s} = (\<Union>n::nat. let s = set (from_nat n) in if P s then f s else {})"
proof safe
- fix x X s assume "x \<in> f s" "P s"
- moreover with assms obtain l where "s = set l" using finite_list by blast
- ultimately show "x \<in> (\<Union>n. let s = set (from_nat n) in if P s then f s else {})" using `P s`
+ fix x X s assume *: "x \<in> f s" "P s"
+ with assms obtain l where "s = set l" using finite_list by blast
+ with * show "x \<in> (\<Union>n. let s = set (from_nat n) in if P s then f s else {})" using `P s`
by (auto intro!: exI[where x="to_nat l"])
next
fix x n assume "x \<in> (let s = set (from_nat n) in if P s then f s else {})"
--- a/src/HOL/Probability/Finite_Product_Measure.thy Tue Sep 03 00:51:08 2013 +0200
+++ b/src/HOL/Probability/Finite_Product_Measure.thy Tue Sep 03 01:12:40 2013 +0200
@@ -235,7 +235,7 @@
using sets.sets_into_space by auto
then have "A = (\<Pi>\<^sub>E i\<in>I. if i\<in>J then E i else space (M i))"
using A J by (auto simp: prod_emb_PiE)
- moreover then have "(\<lambda>i. if i\<in>J then E i else space (M i)) \<in> (\<Pi> i\<in>I. sets (M i))"
+ moreover have "(\<lambda>i. if i\<in>J then E i else space (M i)) \<in> (\<Pi> i\<in>I. sets (M i))"
using sets.top E by auto
ultimately show ?thesis using that by auto
qed
@@ -792,9 +792,9 @@
proof (intro measure_eqI[symmetric])
interpret I: finite_product_sigma_finite M "{i}" by default simp
fix A assume A: "A \<in> sets (M i)"
- moreover then have "(\<lambda>x. x i) -` A \<inter> space (Pi\<^sub>M {i} M) = (\<Pi>\<^sub>E i\<in>{i}. A)"
+ then have "(\<lambda>x. x i) -` A \<inter> space (Pi\<^sub>M {i} M) = (\<Pi>\<^sub>E i\<in>{i}. A)"
using sets.sets_into_space by (auto simp: space_PiM)
- ultimately show "emeasure (M i) A = emeasure ?D A"
+ then show "emeasure (M i) A = emeasure ?D A"
using A I.measure_times[of "\<lambda>_. A"]
by (simp add: emeasure_distr measurable_component_singleton)
qed simp
--- a/src/HOL/Probability/Infinite_Product_Measure.thy Tue Sep 03 00:51:08 2013 +0200
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy Tue Sep 03 01:12:40 2013 +0200
@@ -246,7 +246,7 @@
then show ?case by auto
qed
moreover
- then have "w k \<in> space (Pi\<^sub>M (J k) M)" by auto
+ from w have "w k \<in> space (Pi\<^sub>M (J k) M)" by auto
moreover
from w have "?a / 2 ^ (k + 1) \<le> ?q k k (w k)" by auto
then have "?M (J k) (A k) (w k) \<noteq> {}"
@@ -344,10 +344,10 @@
assume "I = {}" then show ?thesis by (simp add: space_PiM_empty)
next
assume "I \<noteq> {}"
- then obtain i where "i \<in> I" by auto
- moreover then have "emb I {i} (\<Pi>\<^sub>E i\<in>{i}. space (M i)) = (space (Pi\<^sub>M I M))"
+ then obtain i where i: "i \<in> I" by auto
+ then have "emb I {i} (\<Pi>\<^sub>E i\<in>{i}. space (M i)) = (space (Pi\<^sub>M I M))"
by (auto simp: prod_emb_def space_PiM)
- ultimately show ?thesis
+ with i show ?thesis
using emeasure_PiM_emb_not_empty[of "{i}" "\<lambda>i. space (M i)"]
by (simp add: emeasure_PiM emeasure_space_1)
qed
--- a/src/HOL/Probability/Information.thy Tue Sep 03 00:51:08 2013 +0200
+++ b/src/HOL/Probability/Information.thy Tue Sep 03 01:12:40 2013 +0200
@@ -381,10 +381,10 @@
shows "absolutely_continuous S (distr (S \<Otimes>\<^sub>M T) S fst)"
proof -
interpret sigma_finite_measure T by fact
- { fix A assume "A \<in> sets S" "emeasure S A = 0"
- moreover then have "fst -` A \<inter> space (S \<Otimes>\<^sub>M T) = A \<times> space T"
+ { fix A assume A: "A \<in> sets S" "emeasure S A = 0"
+ then have "fst -` A \<inter> space (S \<Otimes>\<^sub>M T) = A \<times> space T"
by (auto simp: space_pair_measure dest!: sets.sets_into_space)
- ultimately have "emeasure (S \<Otimes>\<^sub>M T) (fst -` A \<inter> space (S \<Otimes>\<^sub>M T)) = 0"
+ with A have "emeasure (S \<Otimes>\<^sub>M T) (fst -` A \<inter> space (S \<Otimes>\<^sub>M T)) = 0"
by (simp add: emeasure_pair_measure_Times) }
then show ?thesis
unfolding absolutely_continuous_def
@@ -398,10 +398,10 @@
shows "absolutely_continuous T (distr (S \<Otimes>\<^sub>M T) T snd)"
proof -
interpret sigma_finite_measure T by fact
- { fix A assume "A \<in> sets T" "emeasure T A = 0"
- moreover then have "snd -` A \<inter> space (S \<Otimes>\<^sub>M T) = space S \<times> A"
+ { fix A assume A: "A \<in> sets T" "emeasure T A = 0"
+ then have "snd -` A \<inter> space (S \<Otimes>\<^sub>M T) = space S \<times> A"
by (auto simp: space_pair_measure dest!: sets.sets_into_space)
- ultimately have "emeasure (S \<Otimes>\<^sub>M T) (snd -` A \<inter> space (S \<Otimes>\<^sub>M T)) = 0"
+ with A have "emeasure (S \<Otimes>\<^sub>M T) (snd -` A \<inter> space (S \<Otimes>\<^sub>M T)) = 0"
by (simp add: emeasure_pair_measure_Times) }
then show ?thesis
unfolding absolutely_continuous_def
--- a/src/HOL/Probability/Lebesgue_Integration.thy Tue Sep 03 00:51:08 2013 +0200
+++ b/src/HOL/Probability/Lebesgue_Integration.thy Tue Sep 03 01:12:40 2013 +0200
@@ -675,12 +675,11 @@
assumes f: "simple_function M f"
shows "(\<integral>\<^sup>Sx. f x * indicator A x \<partial>M) =
(\<Sum>x \<in> f ` space M. x * (emeasure M) (f -` {x} \<inter> space M \<inter> A))"
-proof cases
- assume "A = space M"
- moreover hence "(\<integral>\<^sup>Sx. f x * indicator A x \<partial>M) = integral\<^sup>S M f"
+proof (cases "A = space M")
+ case True
+ then have "(\<integral>\<^sup>Sx. f x * indicator A x \<partial>M) = integral\<^sup>S M f"
by (auto intro!: simple_integral_cong)
- moreover have "\<And>X. X \<inter> space M \<inter> space M = X \<inter> space M" by auto
- ultimately show ?thesis by (simp add: simple_integral_def)
+ with True show ?thesis by (simp add: simple_integral_def)
next
assume "A \<noteq> space M"
then obtain x where x: "x \<in> space M" "x \<notin> A" using sets.sets_into_space[OF assms(1)] by auto
@@ -1001,10 +1000,10 @@
unfolding positive_integral_def_finite[of _ "\<lambda>x. SUP i. f i x"]
proof (safe intro!: SUP_least)
fix g assume g: "simple_function M g"
- and "g \<le> max 0 \<circ> (\<lambda>x. SUP i. f i x)" "range g \<subseteq> {0..<\<infinity>}"
- moreover then have "\<And>x. 0 \<le> (SUP i. f i x)" and g': "g`space M \<subseteq> {0..<\<infinity>}"
+ and *: "g \<le> max 0 \<circ> (\<lambda>x. SUP i. f i x)" "range g \<subseteq> {0..<\<infinity>}"
+ then have "\<And>x. 0 \<le> (SUP i. f i x)" and g': "g`space M \<subseteq> {0..<\<infinity>}"
using f by (auto intro!: SUP_upper2)
- ultimately show "integral\<^sup>S M g \<le> (SUP j. integral\<^sup>P M (f j))"
+ with * show "integral\<^sup>S M g \<le> (SUP j. integral\<^sup>P M (f j))"
by (intro positive_integral_SUP_approx[OF f g _ g'])
(auto simp: le_fun_def max_def)
qed
@@ -1357,7 +1356,7 @@
proof (safe intro!: incseq_SucI)
fix n :: nat and x
assume *: "1 \<le> real n * u x"
- also from gt_1[OF this] have "real n * u x \<le> real (Suc n) * u x"
+ also from gt_1[OF *] have "real n * u x \<le> real (Suc n) * u x"
using `0 \<le> u x` by (auto intro!: ereal_mult_right_mono)
finally show "1 \<le> real (Suc n) * u x" by auto
qed
@@ -2658,10 +2657,9 @@
using f by (simp add: positive_integral_cmult)
next
case (add u v)
- moreover then have "\<And>x. f x * (v x + u x) = f x * v x + f x * u x"
+ then have "\<And>x. f x * (v x + u x) = f x * v x + f x * u x"
by (simp add: ereal_right_distrib)
- moreover note f
- ultimately show ?case
+ with add f show ?case
by (auto simp add: positive_integral_add ereal_zero_le_0_iff intro!: positive_integral_add[symmetric])
next
case (seq U)
--- a/src/HOL/Probability/Lebesgue_Measure.thy Tue Sep 03 00:51:08 2013 +0200
+++ b/src/HOL/Probability/Lebesgue_Measure.thy Tue Sep 03 01:12:40 2013 +0200
@@ -983,22 +983,20 @@
shows "integrable lborel f \<longleftrightarrow> integrable (\<Pi>\<^sub>M (i::'a)\<in>Basis. lborel) (\<lambda>x. f (p2e x))"
(is "_ \<longleftrightarrow> integrable ?B ?f")
proof
- assume "integrable lborel f"
- moreover then have f: "f \<in> borel_measurable borel"
+ assume *: "integrable lborel f"
+ then have f: "f \<in> borel_measurable borel"
by auto
- moreover with measurable_p2e
- have "f \<circ> p2e \<in> borel_measurable ?B"
+ with measurable_p2e have "f \<circ> p2e \<in> borel_measurable ?B"
by (rule measurable_comp)
- ultimately show "integrable ?B ?f"
+ with * f show "integrable ?B ?f"
by (simp add: comp_def borel_fubini_positiv_integral integrable_def)
next
- assume "integrable ?B ?f"
- moreover
+ assume *: "integrable ?B ?f"
then have "?f \<circ> e2p \<in> borel_measurable (borel::'a measure)"
by (auto intro!: measurable_e2p)
then have "f \<in> borel_measurable borel"
by (simp cong: measurable_cong)
- ultimately show "integrable lborel f"
+ with * show "integrable lborel f"
by (simp add: borel_fubini_positiv_integral integrable_def)
qed
--- a/src/HOL/Probability/Measure_Space.thy Tue Sep 03 00:51:08 2013 +0200
+++ b/src/HOL/Probability/Measure_Space.thy Tue Sep 03 01:12:40 2013 +0200
@@ -158,7 +158,8 @@
and A: "A`S \<subseteq> M"
and disj: "disjoint_family_on A S"
shows "(\<Sum>i\<in>S. f (A i)) = f (\<Union>i\<in>S. A i)"
-using `finite S` disj A proof induct
+ using `finite S` disj A
+proof induct
case empty show ?case using f by (simp add: positive_def)
next
case (insert s S)
@@ -168,7 +169,6 @@
have "A s \<in> M" using insert by blast
moreover have "(\<Union>i\<in>S. A i) \<in> M"
using insert `finite S` by auto
- moreover
ultimately have "f (A s \<union> (\<Union>i\<in>S. A i)) = f (A s) + f(\<Union>i\<in>S. A i)"
using ad UNION_in_sets A by (auto simp add: additive_def)
with insert show ?case using ad disjoint_family_on_mono[of S "insert s S" A]
@@ -781,15 +781,15 @@
using sets.sets_into_space by auto
show "{} \<in> null_sets M"
by auto
- fix A B assume sets: "A \<in> null_sets M" "B \<in> null_sets M"
- then have "A \<in> sets M" "B \<in> sets M"
+ fix A B assume null_sets: "A \<in> null_sets M" "B \<in> null_sets M"
+ then have sets: "A \<in> sets M" "B \<in> sets M"
by auto
- moreover then have "emeasure M (A \<union> B) \<le> emeasure M A + emeasure M B"
+ then have *: "emeasure M (A \<union> B) \<le> emeasure M A + emeasure M B"
"emeasure M (A - B) \<le> emeasure M A"
by (auto intro!: emeasure_subadditive emeasure_mono)
- moreover have "emeasure M B = 0" "emeasure M A = 0"
- using sets by auto
- ultimately show "A - B \<in> null_sets M" "A \<union> B \<in> null_sets M"
+ then have "emeasure M B = 0" "emeasure M A = 0"
+ using null_sets by auto
+ with sets * show "A - B \<in> null_sets M" "A \<union> B \<in> null_sets M"
by (auto intro!: antisym)
qed
@@ -1563,9 +1563,9 @@
by (auto intro!: Lim_eventually eventually_sequentiallyI[where c=i])
next
assume "\<not> (\<exists>i. \<forall>j\<ge>i. F i = F j)"
- then obtain f where "\<And>i. i \<le> f i" "\<And>i. F i \<noteq> F (f i)" by metis
- moreover then have "\<And>i. F i \<subseteq> F (f i)" using `incseq F` by (auto simp: incseq_def)
- ultimately have *: "\<And>i. F i \<subset> F (f i)" by auto
+ then obtain f where f: "\<And>i. i \<le> f i" "\<And>i. F i \<noteq> F (f i)" by metis
+ then have "\<And>i. F i \<subseteq> F (f i)" using `incseq F` by (auto simp: incseq_def)
+ with f have *: "\<And>i. F i \<subset> F (f i)" by auto
have "incseq (\<lambda>i. ?M (F i))"
using `incseq F` unfolding incseq_def by (auto simp: card_mono dest: finite_subset)
--- a/src/HOL/Probability/Projective_Limit.thy Tue Sep 03 00:51:08 2013 +0200
+++ b/src/HOL/Probability/Projective_Limit.thy Tue Sep 03 01:12:40 2013 +0200
@@ -257,14 +257,13 @@
finally have "fm n x \<in> fm n ` B n" .
thus "x \<in> B n"
proof safe
- fix y assume "y \<in> B n"
- moreover
+ fix y assume y: "y \<in> B n"
hence "y \<in> space (Pi\<^sub>M (J n) (\<lambda>_. borel))" using J sets.sets_into_space[of "B n" "P (J n)"]
by (auto simp add: proj_space proj_sets)
assume "fm n x = fm n y"
note inj_onD[OF inj_on_fm[OF space_borel],
OF `fm n x = fm n y` `x \<in> space _` `y \<in> space _`]
- ultimately show "x \<in> B n" by simp
+ with y show "x \<in> B n" by simp
qed
qed
{ fix n
@@ -438,10 +437,11 @@
apply (subst (2) tendsto_iff, subst eventually_sequentially)
proof safe
fix e :: real assume "0 < e"
- { fix i x assume "i \<ge> n" "t \<in> domain (fm n x)"
- moreover
+ { fix i x
+ assume i: "i \<ge> n"
+ assume "t \<in> domain (fm n x)"
hence "t \<in> domain (fm i x)" using J_mono[OF `i \<ge> n`] by auto
- ultimately have "(fm i x)\<^sub>F t = (fm n x)\<^sub>F t"
+ with i have "(fm i x)\<^sub>F t = (fm n x)\<^sub>F t"
using j by (auto simp: proj_fm dest!: inj_onD[OF inj_on_Utn])
} note index_shift = this
have I: "\<And>i. i \<ge> n \<Longrightarrow> Suc (diagseq i) \<ge> n"
@@ -487,11 +487,11 @@
also have "finmap_of (Utn ` J n) z = fm n (\<lambda>i. z (Utn i))"
unfolding finmap_eq_iff
proof clarsimp
- fix i assume "i \<in> J n"
- moreover hence "from_nat_into (\<Union>n. J n) (Utn i) = i"
+ fix i assume i: "i \<in> J n"
+ hence "from_nat_into (\<Union>n. J n) (Utn i) = i"
unfolding Utn_def
by (subst from_nat_into_to_nat_on[OF countable_UN_J]) auto
- ultimately show "z (Utn i) = (fm n (\<lambda>i. z (Utn i)))\<^sub>F (Utn i)"
+ with i show "z (Utn i) = (fm n (\<lambda>i. z (Utn i)))\<^sub>F (Utn i)"
by (simp add: finmap_eq_iff fm_def compose_def)
qed
finally have "fm n (\<lambda>i. z (Utn i)) \<in> K' n" .
--- a/src/HOL/Probability/Radon_Nikodym.thy Tue Sep 03 00:51:08 2013 +0200
+++ b/src/HOL/Probability/Radon_Nikodym.thy Tue Sep 03 01:12:40 2013 +0200
@@ -412,14 +412,14 @@
have ac: "absolutely_continuous M ?M" unfolding absolutely_continuous_def
proof
- fix A assume A: "A \<in> null_sets M"
- with `absolutely_continuous M N` have "A \<in> null_sets N"
+ fix A assume A_M: "A \<in> null_sets M"
+ with `absolutely_continuous M N` have A_N: "A \<in> null_sets N"
unfolding absolutely_continuous_def by auto
- moreover with A have "(\<integral>\<^sup>+ x. ?F A x \<partial>M) \<le> N A" using `f \<in> G` by (auto simp: G_def)
+ 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)
ultimately have "N A - (\<integral>\<^sup>+ x. ?F A x \<partial>M) = 0"
using positive_integral_positive[of M] by (auto intro!: antisym)
then show "A \<in> null_sets ?M"
- using A by (simp add: emeasure_M null_sets_def sets_eq)
+ using A_M by (simp add: emeasure_M null_sets_def sets_eq)
qed
have upper_bound: "\<forall>A\<in>sets M. ?M A \<le> 0"
proof (rule ccontr)
@@ -431,7 +431,7 @@
using emeasure_space[of ?M A] by (simp add: sets_eq[THEN sets_eq_imp_space_eq])
finally have pos_t: "0 < ?M (space M)" by simp
moreover
- then have "emeasure M (space M) \<noteq> 0"
+ from pos_t have "emeasure M (space M) \<noteq> 0"
using ac unfolding absolutely_continuous_def by (auto simp: null_sets_def)
then have pos_M: "0 < emeasure M (space M)"
using emeasure_nonneg[of M "space M"] by (simp add: le_less)
@@ -594,12 +594,14 @@
proof (rule disjCI, simp)
assume *: "0 < emeasure M A \<longrightarrow> N A \<noteq> \<infinity>"
show "emeasure M A = 0 \<and> N A = 0"
- proof cases
- assume "emeasure M A = 0" moreover with ac A have "N A = 0"
+ proof (cases "emeasure M A = 0")
+ case True
+ with ac A have "N A = 0"
unfolding absolutely_continuous_def by auto
- ultimately show ?thesis by simp
+ with True show ?thesis by simp
next
- assume "emeasure M A \<noteq> 0" with * have "N A \<noteq> \<infinity>" using emeasure_nonneg[of M A] by auto
+ case False
+ with * have "N A \<noteq> \<infinity>" using emeasure_nonneg[of M A] by auto
with A have "emeasure M ?O_0 + emeasure M A = emeasure M (?O_0 \<union> A)"
using Q' by (auto intro!: plus_emeasure sets.countable_UN)
also have "\<dots> = (SUP i. emeasure M (?O i \<union> A))"
--- a/src/HOL/Probability/Sigma_Algebra.thy Tue Sep 03 00:51:08 2013 +0200
+++ b/src/HOL/Probability/Sigma_Algebra.thy Tue Sep 03 01:12:40 2013 +0200
@@ -1244,8 +1244,8 @@
interpret N: sigma_algebra \<Omega>' A' using measure_measure by (auto simp: measure_space_def)
have "A = sets M" "A' = sets N"
using measure_measure by (simp_all add: sets_def Abs_measure_inverse)
- with `sets M = sets N` have "A = A'" by simp
- moreover with M.top N.top M.space_closed N.space_closed have "\<Omega> = \<Omega>'" by auto
+ with `sets M = sets N` have AA': "A = A'" by simp
+ moreover from M.top N.top M.space_closed N.space_closed AA' have "\<Omega> = \<Omega>'" by auto
moreover { fix B have "\<mu> B = \<mu>' B"
proof cases
assume "B \<in> A"
@@ -1977,7 +1977,7 @@
moreover have "D \<union> (\<Omega> - E) = (\<Union>i. ?f i)"
by (auto simp: image_iff split: split_if_asm)
moreover
- then have "disjoint_family ?f" unfolding disjoint_family_on_def
+ have "disjoint_family ?f" unfolding disjoint_family_on_def
using `D \<in> M`[THEN sets_into_space] `D \<subseteq> E` by auto
ultimately have "\<Omega> - (D \<union> (\<Omega> - E)) \<in> M"
using sets by auto
@@ -2193,11 +2193,11 @@
proof -
have "E \<subseteq> Pow \<Omega>"
using E sets_into_space by force
- then have "sigma_sets \<Omega> E = dynkin \<Omega> E"
+ then have *: "sigma_sets \<Omega> E = dynkin \<Omega> E"
using `Int_stable E` by (rule sigma_eq_dynkin)
- moreover then have "dynkin \<Omega> E = M"
+ then have "dynkin \<Omega> E = M"
using assms dynkin_subset[OF E(1)] by simp
- ultimately show ?thesis
+ with * show ?thesis
using assms by (auto simp: dynkin_def)
qed
--- a/src/HOL/Probability/ex/Dining_Cryptographers.thy Tue Sep 03 00:51:08 2013 +0200
+++ b/src/HOL/Probability/ex/Dining_Cryptographers.thy Tue Sep 03 01:12:40 2013 +0200
@@ -5,7 +5,7 @@
lemma image_ex1_eq: "inj_on f A \<Longrightarrow> (b \<in> f ` A) \<longleftrightarrow> (\<exists>!x \<in> A. b = f x)"
by (unfold inj_on_def) blast
-lemma Ex1_eq: "\<exists>! x. P x \<Longrightarrow> P x \<Longrightarrow> P y \<Longrightarrow> x = y"
+lemma Ex1_eq: "\<exists>!x. P x \<Longrightarrow> P x \<Longrightarrow> P y \<Longrightarrow> x = y"
by auto
section "Define the state space"
@@ -143,8 +143,8 @@
thus "x ! j = y ! j"
proof (induct j)
case (Suc j)
- moreover hence "j < n" by simp
- ultimately show ?case using *[OF `j < n`]
+ hence "j < n" by simp
+ with Suc show ?case using *[OF `j < n`]
by (cases "y ! j") simp_all
qed simp
qed
@@ -234,7 +234,7 @@
hence zs: "inversion (Some i, zs) = xs"
by (simp add: xs_inv[symmetric] inversion_def coin_def payer_def)
moreover
- hence Not_zs: "inversion (Some i, (map Not zs)) = xs"
+ from zs have Not_zs: "inversion (Some i, (map Not zs)) = xs"
by (simp add: xs_inv[symmetric] inversion_def coin_def payer_def)
ultimately
have "{dc \<in> dc_crypto. payer dc = Some i \<and> inversion dc = xs} =
--- a/src/HOL/Quotient_Examples/FSet.thy Tue Sep 03 00:51:08 2013 +0200
+++ b/src/HOL/Quotient_Examples/FSet.thy Tue Sep 03 01:12:40 2013 +0200
@@ -1033,9 +1033,9 @@
case (insert x A)
from insert.prems insert.hyps(1) have "\<And>z. z \<in> fset A \<longleftrightarrow> z \<in> fset (B - {|x|})"
by (auto simp add: in_fset)
- then have "A = B - {|x|}" by (rule insert.hyps(2))
- moreover with insert.prems [symmetric, of x] have "x |\<in>| B" by (simp add: in_fset)
- ultimately show ?case by (metis in_fset_mdef)
+ then have A: "A = B - {|x|}" by (rule insert.hyps(2))
+ with insert.prems [symmetric, of x] have "x |\<in>| B" by (simp add: in_fset)
+ with A show ?case by (metis in_fset_mdef)
qed
subsection {* alternate formulation with a different decomposition principle
--- a/src/HOL/Rat.thy Tue Sep 03 00:51:08 2013 +0200
+++ b/src/HOL/Rat.thy Tue Sep 03 01:12:40 2013 +0200
@@ -237,7 +237,7 @@
next
case False
then obtain a b where "q = Fract a b" and "b > 0" and "coprime a b" by (cases q) auto
- moreover with False have "0 \<noteq> Fract a b" by simp
+ with False have "0 \<noteq> Fract a b" by simp
with `b > 0` have "a \<noteq> 0" by (simp add: Zero_rat_def eq_rat)
with Fract `q = Fract a b` `b > 0` `coprime a b` show C by blast
qed
--- a/src/HOL/Real.thy Tue Sep 03 00:51:08 2013 +0200
+++ b/src/HOL/Real.thy Tue Sep 03 01:12:40 2013 +0200
@@ -947,7 +947,7 @@
using complete_real[of X] by blast
then have "Sup X = s"
unfolding Sup_real_def by (best intro: Least_equality)
- also with s z have "... \<le> z"
+ also from s z have "... \<le> z"
by blast
finally show "Sup X \<le> z" . }
note Sup_least = this
--- a/src/HOL/Real_Vector_Spaces.thy Tue Sep 03 00:51:08 2013 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy Tue Sep 03 01:12:40 2013 +0200
@@ -758,10 +758,10 @@
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))"
proof (safe intro!: exI[of _ "\<lambda>n. {y. dist x y < inverse (Suc n)}"])
fix S assume "open S" "x \<in> S"
- then obtain e where "0 < e" "{y. dist x y < e} \<subseteq> S"
+ then obtain e where e: "0 < e" and "{y. dist x y < e} \<subseteq> S"
by (auto simp: open_dist subset_eq dist_commute)
moreover
- then obtain i where "inverse (Suc i) < e"
+ from e obtain i where "inverse (Suc i) < e"
by (auto dest!: reals_Archimedean)
then have "{y. dist x y < inverse (Suc i)} \<subseteq> {y. dist x y < e}"
by auto
--- a/src/HOL/Set_Interval.thy Tue Sep 03 00:51:08 2013 +0200
+++ b/src/HOL/Set_Interval.thy Tue Sep 03 01:12:40 2013 +0200
@@ -269,9 +269,9 @@
"{a .. b} = {c} \<longleftrightarrow> a = b \<and> b = c"
proof
assume "{a..b} = {c}"
- hence "\<not> (\<not> a \<le> b)" unfolding atLeastatMost_empty_iff[symmetric] by simp
- moreover with `{a..b} = {c}` have "c \<le> a \<and> b \<le> c" by auto
- ultimately show "a = b \<and> b = c" by auto
+ hence *: "\<not> (\<not> a \<le> b)" unfolding atLeastatMost_empty_iff[symmetric] by simp
+ with `{a..b} = {c}` have "c \<le> a \<and> b \<le> c" by auto
+ with * show "a = b \<and> b = c" by auto
qed simp
lemma Icc_subset_Ici_iff[simp]:
@@ -827,21 +827,23 @@
subset is exactly that interval. *}
lemma subset_card_intvl_is_intvl:
- "A <= {k..<k+card A} \<Longrightarrow> A = {k..<k+card A}" (is "PROP ?P")
-proof cases
- assume "finite A"
- thus "PROP ?P"
- proof(induct A rule:finite_linorder_max_induct)
+ assumes "A \<subseteq> {k..<k+card A}"
+ shows "A = {k..<k+card A}"
+proof (cases "finite A")
+ case True
+ from this and assms show ?thesis
+ proof (induct A rule: finite_linorder_max_induct)
case empty thus ?case by auto
next
case (insert b A)
- moreover hence "b ~: A" by auto
- moreover have "A <= {k..<k+card A}" and "b = k+card A"
- using `b ~: A` insert by fastforce+
- ultimately show ?case by auto
+ hence *: "b \<notin> A" by auto
+ with insert have "A <= {k..<k+card A}" and "b = k+card A"
+ by fastforce+
+ with insert * show ?case by auto
qed
next
- assume "~finite A" thus "PROP ?P" by simp
+ case False
+ with assms show ?thesis by simp
qed
@@ -1470,7 +1472,7 @@
case 0 then show ?case by simp
next
case (Suc n)
- moreover with `y \<noteq> 0` have "(1 + y) ^ n = (y * inverse y) * (1 + y) ^ n" by simp
+ moreover from Suc `y \<noteq> 0` have "(1 + y) ^ n = (y * inverse y) * (1 + y) ^ n" by simp
ultimately show ?case by (simp add: field_simps divide_inverse)
qed
ultimately show ?thesis by simp
--- a/src/HOL/Statespace/DistinctTreeProver.thy Tue Sep 03 00:51:08 2013 +0200
+++ b/src/HOL/Statespace/DistinctTreeProver.thy Tue Sep 03 01:12:40 2013 +0200
@@ -572,13 +572,13 @@
shows "delete x (Node l y d r) = Some (Node l' y d r)"
proof -
from delete_Some_x_set_of [OF del_l]
- obtain "x \<in> set_of l"
+ obtain x: "x \<in> set_of l"
by simp
- moreover with dist
+ with dist
have "delete x r = None"
by (cases "delete x r") (auto dest:delete_Some_x_set_of)
- ultimately
+ with x
show ?thesis
using del_l dist
by (auto split: option.splits)
@@ -590,13 +590,13 @@
shows "delete x (Node l y d r) = Some (Node l y d r')"
proof -
from delete_Some_x_set_of [OF del_r]
- obtain "x \<in> set_of r"
+ obtain x: "x \<in> set_of r"
by simp
- moreover with dist
+ with dist
have "delete x l = None"
by (cases "delete x l") (auto dest:delete_Some_x_set_of)
- ultimately
+ with x
show ?thesis
using del_r dist
by (auto split: option.splits)
--- a/src/HOL/Topological_Spaces.thy Tue Sep 03 00:51:08 2013 +0200
+++ b/src/HOL/Topological_Spaces.thy Tue Sep 03 01:12:40 2013 +0200
@@ -2145,7 +2145,8 @@
moreover obtain b where "b \<in> B" "x < b" "b < min a y"
using cInf_less_iff[of "B \<inter> {x <..}" x "min a y"] `?z < a` `?z < y` `x < y` `y \<in> B`
by (auto intro: less_imp_le)
- moreover then have "?z \<le> b"
+ moreover have "?z \<le> b"
+ using `b \<in> B` `x < b`
by (intro cInf_lower[where z=x]) auto
moreover have "b \<in> U"
using `x \<le> ?z` `?z \<le> b` `b < min a y`
--- a/src/HOL/ex/HarmonicSeries.thy Tue Sep 03 00:51:08 2013 +0200
+++ b/src/HOL/ex/HarmonicSeries.thy Tue Sep 03 01:12:40 2013 +0200
@@ -65,7 +65,7 @@
proof -
from xs have
"x \<ge> 2^(m - 1) + 1" by auto
- moreover with mgt0 have
+ moreover from mgt0 have
"2^(m - 1) + 1 \<ge> (1::nat)" by auto
ultimately have
"x \<ge> 1" by (rule xtrans)