tuned proofs -- avoid unstructured calculation;
authorwenzelm
Fri Jul 22 11:00:43 2016 +0200 (2016-07-22)
changeset 63540f8652d0534fa
parent 63539 70d4d9e5707b
child 63541 e308f15cc8a7
tuned proofs -- avoid unstructured calculation;
src/HOL/Archimedean_Field.thy
src/HOL/Cardinals/Ordinal_Arithmetic.thy
src/HOL/Cardinals/Wellorder_Constructions.thy
src/HOL/Conditionally_Complete_Lattices.thy
src/HOL/Corec_Examples/LFilter.thy
src/HOL/Corec_Examples/Tests/Misc_Mono.thy
src/HOL/Filter.thy
src/HOL/Hilbert_Choice.thy
src/HOL/IMP/Compiler2.thy
src/HOL/IMP/Def_Init_Small.thy
src/HOL/Inductive.thy
src/HOL/Library/Bourbaki_Witt_Fixpoint.thy
src/HOL/Library/Continuum_Not_Denumerable.thy
src/HOL/Library/Discrete.thy
src/HOL/Library/Extended_Nonnegative_Real.thy
src/HOL/Library/Extended_Real.thy
src/HOL/Library/Function_Growth.thy
src/HOL/Library/More_List.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/Order_Continuity.thy
src/HOL/Library/Perm.thy
src/HOL/List.thy
src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
src/HOL/Multivariate_Analysis/Conformal_Mappings.thy
src/HOL/Multivariate_Analysis/Integration.thy
src/HOL/Multivariate_Analysis/Path_Connected.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/Probability/Distributions.thy
src/HOL/Probability/Finite_Product_Measure.thy
src/HOL/Probability/Giry_Monad.thy
src/HOL/Probability/Infinite_Product_Measure.thy
src/HOL/Probability/Lebesgue_Integral_Substitution.thy
src/HOL/Probability/Lebesgue_Measure.thy
src/HOL/Probability/Levy.thy
src/HOL/Probability/Measure_Space.thy
src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy
src/HOL/Probability/Probability_Mass_Function.thy
src/HOL/Probability/Radon_Nikodym.thy
src/HOL/Probability/SPMF.thy
src/HOL/Quotient_Examples/Int_Pow.thy
src/HOL/Set_Interval.thy
src/HOL/Transcendental.thy
src/HOL/ex/Ballot.thy
     1.1 --- a/src/HOL/Archimedean_Field.thy	Fri Jul 22 08:02:37 2016 +0200
     1.2 +++ b/src/HOL/Archimedean_Field.thy	Fri Jul 22 11:00:43 2016 +0200
     1.3 @@ -395,9 +395,9 @@
     1.4        by blast
     1.5      then have l: "l = - r"
     1.6        by simp
     1.7 -    moreover with \<open>l \<noteq> 0\<close> False have "r > 0"
     1.8 +    with \<open>l \<noteq> 0\<close> False have "r > 0"
     1.9        by simp
    1.10 -    ultimately show ?thesis
    1.11 +    with l show ?thesis
    1.12        using pos_mod_bound [of r]
    1.13        by (auto simp add: zmod_zminus2_eq_if less_le field_simps intro: floor_unique)
    1.14    qed
     2.1 --- a/src/HOL/Cardinals/Ordinal_Arithmetic.thy	Fri Jul 22 08:02:37 2016 +0200
     2.2 +++ b/src/HOL/Cardinals/Ordinal_Arithmetic.thy	Fri Jul 22 11:00:43 2016 +0200
     2.3 @@ -310,11 +310,11 @@
     2.4    have minim[simp]: "minim r' (Field r') \<in> Field r'"
     2.5      using wo_rel.minim_inField[unfolded wo_rel_def, OF WELL' _ r'] by auto
     2.6    { fix b
     2.7 -    assume "(b, minim r' (Field r')) \<in> r'"
     2.8 -    moreover hence "b \<in> Field r'" unfolding Field_def by auto
     2.9 +    assume b: "(b, minim r' (Field r')) \<in> r'"
    2.10 +    hence "b \<in> Field r'" unfolding Field_def by auto
    2.11      hence "(minim r' (Field r'), b) \<in> r'"
    2.12        using wo_rel.minim_least[unfolded wo_rel_def, OF WELL' subset_refl] r' by auto
    2.13 -    ultimately have "b = minim r' (Field r')"
    2.14 +    with b have "b = minim r' (Field r')"
    2.15        by (metis WELL' antisym_def linear_order_on_def partial_order_on_def well_order_on_def)
    2.16    } note * = this
    2.17    have 1: "Well_order (r *o r')" using assms by (auto simp add: oprod_Well_order)
    2.18 @@ -772,9 +772,9 @@
    2.19              have "G \<subseteq> fin_support r.zero (Field s)"
    2.20              unfolding FinFunc_def fin_support_def proof safe
    2.21                fix g assume "g \<in> G"
    2.22 -              with GF obtain f where "f \<in> F" "g = f(z := r.zero)" by auto
    2.23 -              moreover with SUPPF have "finite (SUPP f)" by blast
    2.24 -              ultimately show "finite (SUPP g)"
    2.25 +              with GF obtain f where f: "f \<in> F" "g = f(z := r.zero)" by auto
    2.26 +              with SUPPF have "finite (SUPP f)" by blast
    2.27 +              with f show "finite (SUPP g)"
    2.28                  by (elim finite_subset[rotated]) (auto simp: support_def)
    2.29              qed
    2.30              moreover from F GF zField have "G \<subseteq> Func (Field s) (Field r)"
    2.31 @@ -831,13 +831,12 @@
    2.32                    case True
    2.33                    with f have "f(z := r.zero) \<in> G" unfolding G_def by blast
    2.34                    with g0(2) f0z have "(f0(z := r.zero), f(z := r.zero)) \<in> oexp" by auto
    2.35 -                  hence "(f0(z := r.zero, z := x0), f(z := r.zero, z := x0)) \<in> oexp"
    2.36 +                  hence oexp: "(f0(z := r.zero, z := x0), f(z := r.zero, z := x0)) \<in> oexp"
    2.37                      by (elim fun_upd_same_oexp[OF _ _ zField x0Field]) simp
    2.38 -                  moreover
    2.39                    with f F(1) x0min True
    2.40                      have "(f(z := x0), f) \<in> oexp" unfolding G_def r.isMinim_def
    2.41                      by (intro fun_upd_smaller_oexp[OF _ zField x0Field]) auto
    2.42 -                  ultimately show ?thesis using transD[OF oexp_trans, of f0 "f(z := x0)" f]
    2.43 +                  with oexp show ?thesis using transD[OF oexp_trans, of f0 "f(z := x0)" f]
    2.44                      unfolding f0_def by auto
    2.45                  next
    2.46                    case False note notG = this
    2.47 @@ -1336,10 +1335,9 @@
    2.48        hence max_Field: "t.max_fun_diff h (F g) \<in> {a \<in> Field t. h a \<noteq> F g a}"
    2.49          by (rule rt.max_fun_diff_in[OF _ gh(2,3)])
    2.50        { assume *: "t.max_fun_diff h (F g) \<notin> f ` Field s"
    2.51 -        with max_Field have "F g (t.max_fun_diff h (F g)) = r.zero" unfolding F_def by auto
    2.52 -        moreover
    2.53 +        with max_Field have **: "F g (t.max_fun_diff h (F g)) = r.zero" unfolding F_def by auto
    2.54          with * gh(4) have "h (t.max_fun_diff h (F g)) = r.zero" unfolding Let_def by auto
    2.55 -        ultimately have False using max_Field gh(2,3) unfolding FinFunc_def Func_def by auto
    2.56 +        with ** have False using max_Field gh(2,3) unfolding FinFunc_def Func_def by auto
    2.57        }
    2.58        hence max_f_Field: "t.max_fun_diff h (F g) \<in> f ` Field s" by blast
    2.59        { fix z assume z: "z \<in> Field t - f ` Field s"
    2.60 @@ -1433,7 +1431,6 @@
    2.61            with f inj have neq: "?f h \<noteq> ?f g"
    2.62              unfolding fun_eq_iff inj_on_def rt.oexp_def map_option_case FinFunc_def Func_def Let_def
    2.63              by simp metis
    2.64 -          moreover
    2.65            with hg have "t.max_fun_diff (?f h) (?f g) = t.max_fun_diff h g" unfolding rt.oexp_def
    2.66              using rt.max_fun_diff[OF \<open>h \<noteq> g\<close>] rt.max_fun_diff_in[OF \<open>h \<noteq> g\<close>]
    2.67              by (subst t.max_fun_diff_def, intro t.maxim_equality)
    2.68 @@ -1441,7 +1438,7 @@
    2.69            with Field_fg Field_fh hg fz f_underS compat neq have "(?f h, ?f g) \<in> st.oexp"
    2.70               using rt.max_fun_diff[OF \<open>h \<noteq> g\<close>] rt.max_fun_diff_in[OF \<open>h \<noteq> g\<close>] unfolding st.Field_oexp
    2.71               unfolding rt.oexp_def st.oexp_def Let_def compat_def by auto
    2.72 -          ultimately show "?f h \<in> underS (s ^o t) (?f g)" unfolding underS_def by auto
    2.73 +          with neq show "?f h \<in> underS (s ^o t) (?f g)" unfolding underS_def by auto
    2.74          qed
    2.75          ultimately have "?f g \<in> Field (s ^o t) \<and> ?f ` underS (r ^o t) g \<subseteq> underS (s ^o t) (?f g)"
    2.76            by blast
    2.77 @@ -1609,12 +1606,12 @@
    2.78      have **: "(\<Union>g \<in> fg ` Field t. rs.SUPP g) =
    2.79                (\<Union>g \<in> fg ` Field t - {rs.const}. rs.SUPP g)"
    2.80        unfolding support_def by auto
    2.81 -    from * have "\<forall>g \<in> fg ` Field t. finite (rs.SUPP g)" "finite (rst.SUPP fg)"
    2.82 +    from * have ***: "\<forall>g \<in> fg ` Field t. finite (rs.SUPP g)" "finite (rst.SUPP fg)"
    2.83        unfolding rs.Field_oexp FinFunc_def Func_def fin_support_def Option.these_def by force+
    2.84 -    moreover hence "finite (fg ` Field t - {rs.const})" using *
    2.85 +    hence "finite (fg ` Field t - {rs.const})" using *
    2.86        unfolding support_def rs.zero_oexp[OF Field] FinFunc_def Func_def
    2.87        by (elim finite_surj[of _ _ fg]) (fastforce simp: image_iff Option.these_def)
    2.88 -    ultimately have "finite ((\<Union>g \<in> fg ` Field t. rs.SUPP g) \<times> rst.SUPP fg)"
    2.89 +    with *** have "finite ((\<Union>g \<in> fg ` Field t. rs.SUPP g) \<times> rst.SUPP fg)"
    2.90        by (subst **) (auto intro!: finite_cartesian_product)
    2.91      with * show "?g \<in> FinFunc r (s *o t)"
    2.92        unfolding Field_oprod rs.Field_oexp FinFunc_def Func_def fin_support_def Option.these_def
    2.93 @@ -1680,8 +1677,9 @@
    2.94            ordIso_transitive[OF oone_ordIso_oexp[OF ordIso_symmetric[OF oone_ordIso] t] oone_ordIso])
    2.95    next
    2.96       case False
    2.97 -     moreover hence "s *o t \<noteq> {}" unfolding oprod_def Field_def by fastforce
    2.98 -     ultimately show ?thesis using \<open>r = {}\<close> ozero_ordIso
    2.99 +     hence "s *o t \<noteq> {}" unfolding oprod_def Field_def by fastforce
   2.100 +     with False show ?thesis
   2.101 +       using \<open>r = {}\<close> ozero_ordIso
   2.102         by (auto simp add: s t oprod_Well_order ozero_def)
   2.103    qed
   2.104  next
     3.1 --- a/src/HOL/Cardinals/Wellorder_Constructions.thy	Fri Jul 22 08:02:37 2016 +0200
     3.2 +++ b/src/HOL/Cardinals/Wellorder_Constructions.thy	Fri Jul 22 11:00:43 2016 +0200
     3.3 @@ -606,13 +606,13 @@
     3.4  
     3.5  lemma not_isSucc_zero: "\<not> isSucc zero"
     3.6  proof
     3.7 -  assume "isSucc zero"
     3.8 -  moreover
     3.9 +  assume *: "isSucc zero"
    3.10    then obtain i where "aboveS i \<noteq> {}" and 1: "minim (Field r) = succ i"
    3.11    unfolding isSucc_def zero_def by auto
    3.12    hence "succ i \<in> Field r" by auto
    3.13 -  ultimately show False by (metis REFL isSucc_def minim_least refl_on_domain
    3.14 -    subset_refl succ_in succ_not_in zero_def)
    3.15 +  with * show False
    3.16 +    by (metis REFL isSucc_def minim_least refl_on_domain
    3.17 +        subset_refl succ_in succ_not_in zero_def)
    3.18  qed
    3.19  
    3.20  lemma isLim_zero[simp]: "isLim zero"
     4.1 --- a/src/HOL/Conditionally_Complete_Lattices.thy	Fri Jul 22 08:02:37 2016 +0200
     4.2 +++ b/src/HOL/Conditionally_Complete_Lattices.thy	Fri Jul 22 11:00:43 2016 +0200
     4.3 @@ -505,19 +505,23 @@
     4.4  
     4.5  instance
     4.6  proof
     4.7 -  fix x :: nat and X :: "nat set"
     4.8 -  { assume "x \<in> X" "bdd_below X" then show "Inf X \<le> x"
     4.9 -      by (simp add: Inf_nat_def Least_le) }
    4.10 -  { assume "X \<noteq> {}" "\<And>y. y \<in> X \<Longrightarrow> x \<le> y" then show "x \<le> Inf X"
    4.11 -      unfolding Inf_nat_def ex_in_conv[symmetric] by (rule LeastI2_ex) }
    4.12 -  { assume "x \<in> X" "bdd_above X" then show "x \<le> Sup X"
    4.13 -      by (simp add: Sup_nat_def bdd_above_nat) }
    4.14 -  { assume "X \<noteq> {}" "\<And>y. y \<in> X \<Longrightarrow> y \<le> x"
    4.15 -    moreover then have "bdd_above X"
    4.16 +  fix x :: nat
    4.17 +  fix X :: "nat set"
    4.18 +  show "Inf X \<le> x" if "x \<in> X" "bdd_below X"
    4.19 +    using that by (simp add: Inf_nat_def Least_le)
    4.20 +  show "x \<le> Inf X" if "X \<noteq> {}" "\<And>y. y \<in> X \<Longrightarrow> x \<le> y"
    4.21 +    using that unfolding Inf_nat_def ex_in_conv[symmetric] by (rule LeastI2_ex)
    4.22 +  show "x \<le> Sup X" if "x \<in> X" "bdd_above X"
    4.23 +    using that by (simp add: Sup_nat_def bdd_above_nat)
    4.24 +  show "Sup X \<le> x" if "X \<noteq> {}" "\<And>y. y \<in> X \<Longrightarrow> y \<le> x"
    4.25 +  proof -
    4.26 +    from that have "bdd_above X"
    4.27        by (auto simp: bdd_above_def)
    4.28 -    ultimately show "Sup X \<le> x"
    4.29 -      by (simp add: Sup_nat_def bdd_above_nat) }
    4.30 +    with that show ?thesis 
    4.31 +      by (simp add: Sup_nat_def bdd_above_nat)
    4.32 +  qed
    4.33  qed
    4.34 +
    4.35  end
    4.36  
    4.37  instantiation int :: conditionally_complete_linorder
     5.1 --- a/src/HOL/Corec_Examples/LFilter.thy	Fri Jul 22 08:02:37 2016 +0200
     5.2 +++ b/src/HOL/Corec_Examples/LFilter.thy	Fri Jul 22 11:00:43 2016 +0200
     5.3 @@ -30,7 +30,6 @@
     5.4    from this(1,2) obtain a where "P (lhd ((ltl ^^ a) xs))"
     5.5      by (atomize_elim, induct x xs rule: llist.set_induct)
     5.6         (auto simp: funpow_Suc_right simp del: funpow.simps(2) intro: exI[of _ 0] exI[of _ "Suc i" for i])
     5.7 -  moreover
     5.8    with \<open>\<not> P (lhd xs)\<close>
     5.9      have "(LEAST n. P (lhd ((ltl ^^ n) xs))) = Suc (LEAST n. P (lhd ((ltl ^^ Suc n) xs)))"
    5.10      by (intro Least_Suc) auto
     6.1 --- a/src/HOL/Corec_Examples/Tests/Misc_Mono.thy	Fri Jul 22 08:02:37 2016 +0200
     6.2 +++ b/src/HOL/Corec_Examples/Tests/Misc_Mono.thy	Fri Jul 22 11:00:43 2016 +0200
     6.3 @@ -382,7 +382,6 @@
     6.4    from this(1,2) obtain a where "P (head ((tail ^^ a) xs))"
     6.5      by (atomize_elim, induct xs x rule: llist_in.induct) (auto simp: funpow_Suc_right
     6.6        simp del: funpow.simps(2) intro: exI[of _ 0] exI[of _ "Suc i" for i])
     6.7 -  moreover
     6.8    with \<open>\<not> P (head xs)\<close>
     6.9      have "(LEAST n. P (head ((tail ^^ n) xs))) = Suc (LEAST n. P (head ((tail ^^ Suc n) xs)))"
    6.10      by (intro Least_Suc) auto
     7.1 --- a/src/HOL/Filter.thy	Fri Jul 22 08:02:37 2016 +0200
     7.2 +++ b/src/HOL/Filter.thy	Fri Jul 22 11:00:43 2016 +0200
     7.3 @@ -489,9 +489,9 @@
     7.4    assumes **: "\<And>i P. i \<in> I \<Longrightarrow> \<forall>\<^sub>F x in F i. P x \<Longrightarrow> \<forall>\<^sub>F x in F' i. T P x"
     7.5    shows "\<forall>\<^sub>F x in \<Sqinter>i\<in>I. F' i. T P x"
     7.6  proof -
     7.7 -  from * obtain X where "finite X" "X \<subseteq> I" "\<forall>\<^sub>F x in \<Sqinter>i\<in>X. F i. P x"
     7.8 +  from * obtain X where X: "finite X" "X \<subseteq> I" "\<forall>\<^sub>F x in \<Sqinter>i\<in>X. F i. P x"
     7.9      unfolding eventually_INF[of _ _ I] by auto
    7.10 -  moreover then have "eventually (T P) (INFIMUM X F')"
    7.11 +  then have "eventually (T P) (INFIMUM X F')"
    7.12      apply (induction X arbitrary: P)
    7.13      apply (auto simp: eventually_inf T2)
    7.14      subgoal for x S P Q R
    7.15 @@ -501,7 +501,7 @@
    7.16        apply (auto intro: T1) []
    7.17        done
    7.18      done
    7.19 -  ultimately show "\<forall>\<^sub>F x in \<Sqinter>i\<in>I. F' i. T P x"
    7.20 +  with X show "\<forall>\<^sub>F x in \<Sqinter>i\<in>I. F' i. T P x"
    7.21      by (subst eventually_INF) auto
    7.22  qed
    7.23  
    7.24 @@ -798,9 +798,10 @@
    7.25    shows "(\<forall>\<^sub>F (x, y) in A \<times>\<^sub>F B. P x) \<longleftrightarrow> (\<forall>\<^sub>F x in A. P x)"
    7.26    unfolding eventually_prod_filter
    7.27  proof safe
    7.28 -  fix R Q assume "\<forall>\<^sub>F x in A. R x" "\<forall>\<^sub>F x in B. Q x" "\<forall>x y. R x \<longrightarrow> Q y \<longrightarrow> P x"
    7.29 -  moreover with \<open>B \<noteq> bot\<close> obtain y where "Q y" by (auto dest: eventually_happens)
    7.30 -  ultimately show "eventually P A"
    7.31 +  fix R Q
    7.32 +  assume *: "\<forall>\<^sub>F x in A. R x" "\<forall>\<^sub>F x in B. Q x" "\<forall>x y. R x \<longrightarrow> Q y \<longrightarrow> P x"
    7.33 +  with \<open>B \<noteq> bot\<close> obtain y where "Q y" by (auto dest: eventually_happens)
    7.34 +  with * show "eventually P A"
    7.35      by (force elim: eventually_mono)
    7.36  next
    7.37    assume "eventually P A"
    7.38 @@ -813,9 +814,10 @@
    7.39    shows "(\<forall>\<^sub>F (x, y) in A \<times>\<^sub>F B. P y) \<longleftrightarrow> (\<forall>\<^sub>F y in B. P y)"
    7.40    unfolding eventually_prod_filter
    7.41  proof safe
    7.42 -  fix R Q assume "\<forall>\<^sub>F x in A. R x" "\<forall>\<^sub>F x in B. Q x" "\<forall>x y. R x \<longrightarrow> Q y \<longrightarrow> P y"
    7.43 -  moreover with \<open>A \<noteq> bot\<close> obtain x where "R x" by (auto dest: eventually_happens)
    7.44 -  ultimately show "eventually P B"
    7.45 +  fix R Q
    7.46 +  assume *: "\<forall>\<^sub>F x in A. R x" "\<forall>\<^sub>F x in B. Q x" "\<forall>x y. R x \<longrightarrow> Q y \<longrightarrow> P y"
    7.47 +  with \<open>A \<noteq> bot\<close> obtain x where "R x" by (auto dest: eventually_happens)
    7.48 +  with * show "eventually P B"
    7.49      by (force elim: eventually_mono)
    7.50  next
    7.51    assume "eventually P B"
    7.52 @@ -827,35 +829,40 @@
    7.53    fixes F :: "'a \<Rightarrow> 'b filter"
    7.54    assumes *: "\<And>i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> \<exists>k\<in>I. F k \<le> F i \<sqinter> F j"
    7.55    shows "(INF i:I. F i) = bot \<longleftrightarrow> (\<exists>i\<in>I. F i = bot)"
    7.56 -proof cases
    7.57 -  assume "\<exists>i\<in>I. F i = bot"
    7.58 -  moreover then have "(INF i:I. F i) \<le> bot"
    7.59 +proof (cases "\<exists>i\<in>I. F i = bot")
    7.60 +  case True
    7.61 +  then have "(INF i:I. F i) \<le> bot"
    7.62      by (auto intro: INF_lower2)
    7.63 -  ultimately show ?thesis
    7.64 +  with True show ?thesis
    7.65      by (auto simp: bot_unique)
    7.66  next
    7.67 -  assume **: "\<not> (\<exists>i\<in>I. F i = bot)"
    7.68 +  case False
    7.69    moreover have "(INF i:I. F i) \<noteq> bot"
    7.70 -  proof cases
    7.71 -    assume "I \<noteq> {}"
    7.72 +  proof (cases "I = {}")
    7.73 +    case True
    7.74 +    then show ?thesis
    7.75 +      by (auto simp add: filter_eq_iff)
    7.76 +  next
    7.77 +    case False': False
    7.78      show ?thesis
    7.79      proof (rule INF_filter_not_bot)
    7.80 -      fix J assume "finite J" "J \<subseteq> I"
    7.81 +      fix J
    7.82 +      assume "finite J" "J \<subseteq> I"
    7.83        then have "\<exists>k\<in>I. F k \<le> (\<Sqinter>i\<in>J. F i)"
    7.84 -      proof (induction J)
    7.85 -        case empty then show ?case
    7.86 +      proof (induct J)
    7.87 +        case empty
    7.88 +        then show ?case
    7.89            using \<open>I \<noteq> {}\<close> by auto
    7.90        next
    7.91          case (insert i J)
    7.92 -        moreover then obtain k where "k \<in> I" "F k \<le> (\<Sqinter>i\<in>J. F i)" by auto
    7.93 -        moreover note *[of i k]
    7.94 -        ultimately show ?case
    7.95 +        then obtain k where "k \<in> I" "F k \<le> (\<Sqinter>i\<in>J. F i)" by auto
    7.96 +        with insert *[of i k] show ?case
    7.97            by auto
    7.98        qed
    7.99 -      with ** show "(\<Sqinter>i\<in>J. F i) \<noteq> \<bottom>"
   7.100 +      with False show "(\<Sqinter>i\<in>J. F i) \<noteq> \<bottom>"
   7.101          by (auto simp: bot_unique)
   7.102      qed
   7.103 -  qed (auto simp add: filter_eq_iff)
   7.104 +  qed
   7.105    ultimately show ?thesis
   7.106      by auto
   7.107  qed
   7.108 @@ -883,9 +890,9 @@
   7.109    shows "A \<times>\<^sub>F B \<le> C \<times>\<^sub>F D \<longleftrightarrow> A \<le> C \<and> B \<le> D"
   7.110  proof safe
   7.111    assume *: "A \<times>\<^sub>F B \<le> C \<times>\<^sub>F D"
   7.112 -  moreover with assms have "A \<times>\<^sub>F B \<noteq> bot"
   7.113 +  with assms have "A \<times>\<^sub>F B \<noteq> bot"
   7.114      by (auto simp: bot_unique prod_filter_eq_bot)
   7.115 -  ultimately have "C \<times>\<^sub>F D \<noteq> bot"
   7.116 +  with * have "C \<times>\<^sub>F D \<noteq> bot"
   7.117      by (auto simp: bot_unique)
   7.118    then have nCD: "C \<noteq> bot" "D \<noteq> bot"
   7.119      by (auto simp: prod_filter_eq_bot)
     8.1 --- a/src/HOL/Hilbert_Choice.thy	Fri Jul 22 08:02:37 2016 +0200
     8.2 +++ b/src/HOL/Hilbert_Choice.thy	Fri Jul 22 11:00:43 2016 +0200
     8.3 @@ -317,14 +317,17 @@
     8.4  proof -
     8.5    define Sseq where "Sseq = rec_nat S (\<lambda>n T. T - {SOME e. e \<in> T})"
     8.6    define pick where "pick n = (SOME e. e \<in> Sseq n)" for n
     8.7 -  { fix n have "Sseq n \<subseteq> S" "\<not> finite (Sseq n)" by (induct n) (auto simp add: Sseq_def inf) }
     8.8 -  moreover then have *: "\<And>n. pick n \<in> Sseq n"
     8.9 +  have *: "Sseq n \<subseteq> S" "\<not> finite (Sseq n)" for n
    8.10 +    by (induct n) (auto simp add: Sseq_def inf)
    8.11 +  then have **: "\<And>n. pick n \<in> Sseq n"
    8.12      unfolding pick_def by (subst (asm) finite.simps) (auto simp add: ex_in_conv intro: someI_ex)
    8.13 -  ultimately have "range pick \<subseteq> S" by auto
    8.14 +  with * have "range pick \<subseteq> S" by auto
    8.15    moreover
    8.16 -  { fix n m
    8.17 -    have "pick n \<notin> Sseq (n + Suc m)" by (induct m) (auto simp add: Sseq_def pick_def)
    8.18 -    with * have "pick n \<noteq> pick (n + Suc m)" by auto
    8.19 +  {
    8.20 +    fix n m
    8.21 +    have "pick n \<notin> Sseq (n + Suc m)"
    8.22 +      by (induct m) (auto simp add: Sseq_def pick_def)
    8.23 +    with ** have "pick n \<noteq> pick (n + Suc m)" by auto
    8.24    }
    8.25    then have "inj pick" by (intro linorder_injI) (auto simp add: less_iff_Suc_add)
    8.26    ultimately show ?thesis by blast
     9.1 --- a/src/HOL/IMP/Compiler2.thy	Fri Jul 22 08:02:37 2016 +0200
     9.2 +++ b/src/HOL/IMP/Compiler2.thy	Fri Jul 22 11:00:43 2016 +0200
     9.3 @@ -366,9 +366,8 @@
     9.4      rest: "P @ P' \<turnstile> (i', s'', stk'') \<rightarrow>^k (n, s', stk')"
     9.5      by auto
     9.6    from step `size P \<le> i`
     9.7 -  have "P' \<turnstile> (i - size P, s, stk) \<rightarrow> (i' - size P, s'', stk'')" 
     9.8 +  have *: "P' \<turnstile> (i - size P, s, stk) \<rightarrow> (i' - size P, s'', stk'')" 
     9.9      by (rule exec1_drop_left)
    9.10 -  moreover
    9.11    then have "i' - size P \<in> succs P' 0"
    9.12      by (fastforce dest!: succs_iexec1 simp: exec1_def simp del: iexec.simps)
    9.13    with `exits P' \<subseteq> {0..}`
    9.14 @@ -376,8 +375,7 @@
    9.15    from rest this `exits P' \<subseteq> {0..}`     
    9.16    have "P' \<turnstile> (i' - size P, s'', stk'') \<rightarrow>^k (n - size P, s', stk')"
    9.17      by (rule Suc.IH)
    9.18 -  ultimately
    9.19 -  show ?case by auto
    9.20 +  with * show ?case by auto
    9.21  qed
    9.22  
    9.23  lemmas exec_n_drop_Cons = 
    10.1 --- a/src/HOL/IMP/Def_Init_Small.thy	Fri Jul 22 08:02:37 2016 +0200
    10.2 +++ b/src/HOL/IMP/Def_Init_Small.thy	Fri Jul 22 11:00:43 2016 +0200
    10.3 @@ -58,10 +58,9 @@
    10.4    "(c,s) \<rightarrow> (c',s') \<Longrightarrow> D (dom s) c A \<Longrightarrow> EX A'. D (dom s') c' A' & A <= A'"
    10.5  proof (induction arbitrary: A rule: small_step_induct)
    10.6    case (While b c s)
    10.7 -  then obtain A' where "vars b \<subseteq> dom s" "A = dom s" "D (dom s) c A'" by blast
    10.8 -  moreover
    10.9 +  then obtain A' where A': "vars b \<subseteq> dom s" "A = dom s" "D (dom s) c A'" by blast
   10.10    then obtain A'' where "D A' c A''" by (metis D_incr D_mono)
   10.11 -  ultimately have "D (dom s) (IF b THEN c;; WHILE b DO c ELSE SKIP) (dom s)"
   10.12 +  with A' have "D (dom s) (IF b THEN c;; WHILE b DO c ELSE SKIP) (dom s)"
   10.13      by (metis D.If[OF `vars b \<subseteq> dom s` D.Seq[OF `D (dom s) c A'` D.While[OF _ `D A' c A''`]] D.Skip] D_incr Int_absorb1 subset_trans)
   10.14    thus ?case by (metis D_incr `A = dom s`)
   10.15  next
    11.1 --- a/src/HOL/Inductive.thy	Fri Jul 22 08:02:37 2016 +0200
    11.2 +++ b/src/HOL/Inductive.thy	Fri Jul 22 11:00:43 2016 +0200
    11.3 @@ -270,10 +270,10 @@
    11.4    show "g (lfp (\<lambda>x. f (g x))) \<le> lfp (\<lambda>x. g (f x))"
    11.5    proof (rule lfp_greatest)
    11.6      fix u
    11.7 -    assume "g (f u) \<le> u"
    11.8 -    moreover then have "g (lfp (\<lambda>x. f (g x))) \<le> g (f u)"
    11.9 +    assume u: "g (f u) \<le> u"
   11.10 +    then have "g (lfp (\<lambda>x. f (g x))) \<le> g (f u)"
   11.11        by (intro assms[THEN monoD] lfp_lowerbound)
   11.12 -    ultimately show "g (lfp (\<lambda>x. f (g x))) \<le> u"
   11.13 +    with u show "g (lfp (\<lambda>x. f (g x))) \<le> u"
   11.14        by auto
   11.15    qed
   11.16  qed
   11.17 @@ -307,10 +307,11 @@
   11.18      by (rule gfp_upperbound) (simp add: gfp_unfold[OF *, symmetric])
   11.19    show "gfp (\<lambda>x. g (f x)) \<le> g (gfp (\<lambda>x. f (g x)))"
   11.20    proof (rule gfp_least)
   11.21 -    fix u assume "u \<le> g (f u)"
   11.22 -    moreover then have "g (f u) \<le> g (gfp (\<lambda>x. f (g x)))"
   11.23 +    fix u
   11.24 +    assume u: "u \<le> g (f u)"
   11.25 +    then have "g (f u) \<le> g (gfp (\<lambda>x. f (g x)))"
   11.26        by (intro assms[THEN monoD] gfp_upperbound)
   11.27 -    ultimately show "u \<le> g (gfp (\<lambda>x. f (g x)))"
   11.28 +    with u show "u \<le> g (gfp (\<lambda>x. f (g x)))"
   11.29        by auto
   11.30    qed
   11.31  qed
    12.1 --- a/src/HOL/Library/Bourbaki_Witt_Fixpoint.thy	Fri Jul 22 08:02:37 2016 +0200
    12.2 +++ b/src/HOL/Library/Bourbaki_Witt_Fixpoint.thy	Fri Jul 22 11:00:43 2016 +0200
    12.3 @@ -7,7 +7,9 @@
    12.4  
    12.5  section \<open>The Bourbaki-Witt tower construction for transfinite iteration\<close>
    12.6  
    12.7 -theory Bourbaki_Witt_Fixpoint imports Main begin
    12.8 +theory Bourbaki_Witt_Fixpoint
    12.9 +  imports Main
   12.10 +begin
   12.11  
   12.12  lemma ChainsI [intro?]:
   12.13    "(\<And>a b. \<lbrakk> a \<in> Y; b \<in> Y \<rbrakk> \<Longrightarrow> (a, b) \<in> r \<or> (b, a) \<in> r) \<Longrightarrow> Y \<in> Chains r"
   12.14 @@ -131,10 +133,10 @@
   12.15          with Sup.IH[OF z] \<open>y = a\<close> Sup.hyps(3)[OF z]
   12.16          show ?thesis by(auto dest: iterates_above_ge intro: a)
   12.17        next
   12.18 -        assume "y \<in> iterates_above (f a)"
   12.19 -        moreover with increasing[OF a] have "y \<in> Field leq"
   12.20 +        assume *: "y \<in> iterates_above (f a)"
   12.21 +        with increasing[OF a] have "y \<in> Field leq"
   12.22            by(auto dest!: iterates_above_Field intro: FieldI2)
   12.23 -        ultimately show ?thesis using y by(auto)
   12.24 +        with * show ?thesis using y by auto
   12.25        qed
   12.26      qed
   12.27      thus ?thesis by simp
    13.1 --- a/src/HOL/Library/Continuum_Not_Denumerable.thy	Fri Jul 22 08:02:37 2016 +0200
    13.2 +++ b/src/HOL/Library/Continuum_Not_Denumerable.thy	Fri Jul 22 11:00:43 2016 +0200
    13.3 @@ -153,11 +153,11 @@
    13.4    assumes "a < b" and "countable A"
    13.5    shows "\<exists>x\<in>{a<..<b}. x \<notin> A"
    13.6  proof -
    13.7 -  from \<open>countable A\<close> have "countable (A \<inter> {a<..<b})"
    13.8 +  from \<open>countable A\<close> have *: "countable (A \<inter> {a<..<b})"
    13.9      by auto
   13.10 -  moreover with \<open>a < b\<close> have "\<not> countable {a<..<b}"
   13.11 +  with \<open>a < b\<close> have "\<not> countable {a<..<b}"
   13.12      by (simp add: uncountable_open_interval)
   13.13 -  ultimately have "A \<inter> {a<..<b} \<noteq> {a<..<b}"
   13.14 +  with * have "A \<inter> {a<..<b} \<noteq> {a<..<b}"
   13.15      by auto
   13.16    then have "A \<inter> {a<..<b} \<subset> {a<..<b}"
   13.17      by (intro psubsetI) auto
    14.1 --- a/src/HOL/Library/Discrete.thy	Fri Jul 22 08:02:37 2016 +0200
    14.2 +++ b/src/HOL/Library/Discrete.thy	Fri Jul 22 11:00:43 2016 +0200
    14.3 @@ -28,11 +28,13 @@
    14.4    assume "n > 0"
    14.5    show "P n"
    14.6    proof (cases "n = 1")
    14.7 -    case True with one show ?thesis by simp
    14.8 +    case True
    14.9 +    with one show ?thesis by simp
   14.10    next
   14.11 -    case False with \<open>n > 0\<close> have "n \<ge> 2" by auto
   14.12 -    moreover with * have "P (n div 2)" .
   14.13 -    ultimately show ?thesis by (rule double)
   14.14 +    case False
   14.15 +    with \<open>n > 0\<close> have "n \<ge> 2" by auto
   14.16 +    with * have "P (n div 2)" .
   14.17 +    with \<open>n \<ge> 2\<close> show ?thesis by (rule double)
   14.18    qed
   14.19  qed
   14.20    
    15.1 --- a/src/HOL/Library/Extended_Nonnegative_Real.thy	Fri Jul 22 08:02:37 2016 +0200
    15.2 +++ b/src/HOL/Library/Extended_Nonnegative_Real.thy	Fri Jul 22 11:00:43 2016 +0200
    15.3 @@ -1067,11 +1067,11 @@
    15.4    fix x y :: ereal assume xy: "0 \<le> x" "0 \<le> y" "x < y"
    15.5    moreover
    15.6    from ereal_dense3[OF \<open>x < y\<close>]
    15.7 -  obtain r where "x < ereal (real_of_rat r)" "ereal (real_of_rat r) < y"
    15.8 +  obtain r where r: "x < ereal (real_of_rat r)" "ereal (real_of_rat r) < y"
    15.9      by auto
   15.10 -  moreover then have "0 \<le> r"
   15.11 +  then have "0 \<le> r"
   15.12      using le_less_trans[OF \<open>0 \<le> x\<close> \<open>x < ereal (real_of_rat r)\<close>] by auto
   15.13 -  ultimately show "\<exists>r. x < (sup 0 \<circ> ereal) (real_of_rat r) \<and> (sup 0 \<circ> ereal) (real_of_rat r) < y"
   15.14 +  with r show "\<exists>r. x < (sup 0 \<circ> ereal) (real_of_rat r) \<and> (sup 0 \<circ> ereal) (real_of_rat r) < y"
   15.15      by (intro exI[of _ r]) (auto simp: max_absorb2)
   15.16  qed
   15.17  
   15.18 @@ -1172,11 +1172,11 @@
   15.19        from ennreal_Ex_less_of_nat[OF r] guess n .. note n = this
   15.20        have "\<not> (X \<subseteq> enat ` {.. n})"
   15.21          using \<open>infinite X\<close> by (auto dest: finite_subset)
   15.22 -      then obtain x where "x \<in> X" "x \<notin> enat ` {..n}"
   15.23 +      then obtain x where x: "x \<in> X" "x \<notin> enat ` {..n}"
   15.24          by blast
   15.25 -      moreover then have "of_nat n \<le> x"
   15.26 +      then have "of_nat n \<le> x"
   15.27          by (cases x) (auto simp: of_nat_eq_enat)
   15.28 -      ultimately show ?thesis
   15.29 +      with x show ?thesis
   15.30          by (auto intro!: bexI[of _ x] less_le_trans[OF n])
   15.31      qed
   15.32      then have "(SUP x : X. ennreal_of_enat x) = top"
    16.1 --- a/src/HOL/Library/Extended_Real.thy	Fri Jul 22 08:02:37 2016 +0200
    16.2 +++ b/src/HOL/Library/Extended_Real.thy	Fri Jul 22 11:00:43 2016 +0200
    16.3 @@ -2036,14 +2036,15 @@
    16.4  lemma SUP_ereal_add_left:
    16.5    assumes "I \<noteq> {}" "c \<noteq> -\<infinity>"
    16.6    shows "(SUP i:I. f i + c :: ereal) = (SUP i:I. f i) + c"
    16.7 -proof cases
    16.8 -  assume "(SUP i:I. f i) = - \<infinity>"
    16.9 -  moreover then have "\<And>i. i \<in> I \<Longrightarrow> f i = -\<infinity>"
   16.10 +proof (cases "(SUP i:I. f i) = - \<infinity>")
   16.11 +  case True
   16.12 +  then have "\<And>i. i \<in> I \<Longrightarrow> f i = -\<infinity>"
   16.13      unfolding Sup_eq_MInfty by auto
   16.14 -  ultimately show ?thesis
   16.15 +  with True show ?thesis
   16.16      by (cases c) (auto simp: \<open>I \<noteq> {}\<close>)
   16.17  next
   16.18 -  assume "(SUP i:I. f i) \<noteq> - \<infinity>" then show ?thesis
   16.19 +  case False
   16.20 +  then show ?thesis
   16.21      by (subst continuous_at_Sup_mono[where f="\<lambda>x. x + c"])
   16.22         (auto simp: continuous_at_imp_continuous_at_within continuous_at mono_def ereal_add_mono \<open>I \<noteq> {}\<close> \<open>c \<noteq> -\<infinity>\<close>)
   16.23  qed
   16.24 @@ -2158,14 +2159,15 @@
   16.25    assumes "I \<noteq> {}"
   16.26    assumes f: "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i" and c: "0 \<le> c"
   16.27    shows "(SUP i:I. c * f i) = c * (SUP i:I. f i)"
   16.28 -proof cases
   16.29 -  assume "(SUP i: I. f i) = 0"
   16.30 -  moreover then have "\<And>i. i \<in> I \<Longrightarrow> f i = 0"
   16.31 +proof (cases "(SUP i: I. f i) = 0")
   16.32 +  case True
   16.33 +  then have "\<And>i. i \<in> I \<Longrightarrow> f i = 0"
   16.34      by (metis SUP_upper f antisym)
   16.35 -  ultimately show ?thesis
   16.36 +  with True show ?thesis
   16.37      by simp
   16.38  next
   16.39 -  assume "(SUP i:I. f i) \<noteq> 0" then show ?thesis
   16.40 +  case False
   16.41 +  then show ?thesis
   16.42      by (subst continuous_at_Sup_mono[where f="\<lambda>x. c * x"])
   16.43         (auto simp: mono_def continuous_at continuous_at_imp_continuous_at_within \<open>I \<noteq> {}\<close>
   16.44               intro!: ereal_mult_left_mono c)
    17.1 --- a/src/HOL/Library/Function_Growth.thy	Fri Jul 22 08:02:37 2016 +0200
    17.2 +++ b/src/HOL/Library/Function_Growth.thy	Fri Jul 22 11:00:43 2016 +0200
    17.3 @@ -36,8 +36,8 @@
    17.4    shows "a ^ (m - n) = (a ^ m) div (a ^ n)"
    17.5  proof -
    17.6    define q where "q = m - n"
    17.7 -  moreover with assms have "m = q + n" by (simp add: q_def)
    17.8 -  ultimately show ?thesis using \<open>a \<noteq> 0\<close> by (simp add: power_add)
    17.9 +  with assms have "m = q + n" by (simp add: q_def)
   17.10 +  with q_def show ?thesis using \<open>a \<noteq> 0\<close> by (simp add: power_add)
   17.11  qed
   17.12  
   17.13  
    18.1 --- a/src/HOL/Library/More_List.thy	Fri Jul 22 08:02:37 2016 +0200
    18.2 +++ b/src/HOL/Library/More_List.thy	Fri Jul 22 11:00:43 2016 +0200
    18.3 @@ -317,10 +317,10 @@
    18.4    then show ?Q
    18.5    proof (rule nth_equalityI [rule_format])
    18.6      fix n
    18.7 -    assume "n < length ?xs"
    18.8 -    moreover with len have "n < length ?ys"
    18.9 +    assume n: "n < length ?xs"
   18.10 +    with len have "n < length ?ys"
   18.11        by simp
   18.12 -    ultimately have xs: "nth_default dflt ?xs n = ?xs ! n"
   18.13 +    with n have xs: "nth_default dflt ?xs n = ?xs ! n"
   18.14        and ys: "nth_default dflt ?ys n = ?ys ! n"
   18.15        by (simp_all only: nth_default_nth)
   18.16      with eq show "?xs ! n = ?ys ! n"
    19.1 --- a/src/HOL/Library/Multiset.thy	Fri Jul 22 08:02:37 2016 +0200
    19.2 +++ b/src/HOL/Library/Multiset.thy	Fri Jul 22 11:00:43 2016 +0200
    19.3 @@ -2410,11 +2410,11 @@
    19.4          moreover have "(a, b) \<in> (r \<inter> D \<times> D)\<inverse>"
    19.5            using \<open>(b, a) \<in> r\<close> using \<open>b \<in># B\<close> and \<open>a \<in># B\<close>
    19.6            by (auto simp: D_def)
    19.7 -        ultimately obtain x where "x \<in># X" and "(a, x) \<in> r"
    19.8 +        ultimately obtain x where x: "x \<in># X" "(a, x) \<in> r"
    19.9            using "1.IH" by blast
   19.10 -        moreover then have "(b, x) \<in> r"
   19.11 +        then have "(b, x) \<in> r"
   19.12            using \<open>trans r\<close> and \<open>(b, a) \<in> r\<close> by (auto dest: transD)
   19.13 -        ultimately show ?thesis by blast
   19.14 +        with x show ?thesis by blast
   19.15        qed blast
   19.16      qed }
   19.17    note B_less = this
    20.1 --- a/src/HOL/Library/Order_Continuity.thy	Fri Jul 22 08:02:37 2016 +0200
    20.2 +++ b/src/HOL/Library/Order_Continuity.thy	Fri Jul 22 11:00:43 2016 +0200
    20.3 @@ -72,10 +72,11 @@
    20.4    shows "sup_continuous (\<lambda>x. f (g x))"
    20.5    unfolding sup_continuous_def
    20.6  proof safe
    20.7 -  fix M :: "nat \<Rightarrow> 'c" assume "mono M"
    20.8 -  moreover then have "mono (\<lambda>i. g (M i))"
    20.9 +  fix M :: "nat \<Rightarrow> 'c"
   20.10 +  assume M: "mono M"
   20.11 +  then have "mono (\<lambda>i. g (M i))"
   20.12      using sup_continuous_mono[OF g] by (auto simp: mono_def)
   20.13 -  ultimately show "f (g (SUPREMUM UNIV M)) = (SUP i. f (g (M i)))"
   20.14 +  with M show "f (g (SUPREMUM UNIV M)) = (SUP i. f (g (M i)))"
   20.15      by (auto simp: sup_continuous_def g[THEN sup_continuousD] f[THEN sup_continuousD])
   20.16  qed
   20.17  
   20.18 @@ -269,10 +270,11 @@
   20.19    shows "inf_continuous (\<lambda>x. f (g x))"
   20.20    unfolding inf_continuous_def
   20.21  proof safe
   20.22 -  fix M :: "nat \<Rightarrow> 'c" assume "antimono M"
   20.23 -  moreover then have "antimono (\<lambda>i. g (M i))"
   20.24 +  fix M :: "nat \<Rightarrow> 'c"
   20.25 +  assume M: "antimono M"
   20.26 +  then have "antimono (\<lambda>i. g (M i))"
   20.27      using inf_continuous_mono[OF g] by (auto simp: mono_def antimono_def)
   20.28 -  ultimately show "f (g (INFIMUM UNIV M)) = (INF i. f (g (M i)))"
   20.29 +  with M show "f (g (INFIMUM UNIV M)) = (INF i. f (g (M i)))"
   20.30      by (auto simp: inf_continuous_def g[THEN inf_continuousD] f[THEN inf_continuousD])
   20.31  qed
   20.32  
    21.1 --- a/src/HOL/Library/Perm.thy	Fri Jul 22 08:02:37 2016 +0200
    21.2 +++ b/src/HOL/Library/Perm.thy	Fri Jul 22 11:00:43 2016 +0200
    21.3 @@ -78,15 +78,15 @@
    21.4    assume "card (affected f) = 1"
    21.5    then obtain a where *: "affected f = {a}"
    21.6      by (rule card_1_singletonE)
    21.7 -  then have "f \<langle>$\<rangle> a \<noteq> a"
    21.8 +  then have **: "f \<langle>$\<rangle> a \<noteq> a"
    21.9      by (simp add: in_affected [symmetric])
   21.10 -  moreover with * have "f \<langle>$\<rangle> a \<notin> affected f"
   21.11 +  with * have "f \<langle>$\<rangle> a \<notin> affected f"
   21.12      by simp
   21.13    then have "f \<langle>$\<rangle> (f \<langle>$\<rangle> a) = f \<langle>$\<rangle> a"
   21.14      by (simp add: in_affected)
   21.15    then have "inv (apply f) (f \<langle>$\<rangle> (f \<langle>$\<rangle> a)) = inv (apply f) (f \<langle>$\<rangle> a)"
   21.16      by simp
   21.17 -  ultimately show False by simp
   21.18 +  with ** show False by simp
   21.19  qed
   21.20  
   21.21  
   21.22 @@ -203,15 +203,18 @@
   21.23      using assms by auto
   21.24    then show "(g * f) \<langle>$\<rangle> a = (f * g) \<langle>$\<rangle> a"
   21.25    proof cases
   21.26 -    case 1 moreover with * have "f \<langle>$\<rangle> a \<notin> affected g"
   21.27 +    case 1
   21.28 +    with * have "f \<langle>$\<rangle> a \<notin> affected g"
   21.29        by auto
   21.30 -    ultimately show ?thesis by (simp add: in_affected apply_times)
   21.31 +    with 1 show ?thesis by (simp add: in_affected apply_times)
   21.32    next
   21.33 -    case 2 moreover with * have "g \<langle>$\<rangle> a \<notin> affected f"
   21.34 +    case 2
   21.35 +    with * have "g \<langle>$\<rangle> a \<notin> affected f"
   21.36        by auto
   21.37 -    ultimately show ?thesis by (simp add: in_affected apply_times)
   21.38 +    with 2 show ?thesis by (simp add: in_affected apply_times)
   21.39    next
   21.40 -    case 3 then show ?thesis by (simp add: in_affected apply_times)
   21.41 +    case 3
   21.42 +    then show ?thesis by (simp add: in_affected apply_times)
   21.43    qed
   21.44  qed
   21.45  
    22.1 --- a/src/HOL/List.thy	Fri Jul 22 08:02:37 2016 +0200
    22.2 +++ b/src/HOL/List.thy	Fri Jul 22 11:00:43 2016 +0200
    22.3 @@ -3542,10 +3542,9 @@
    22.4  
    22.5      have "length ys = card (f ` {0 ..< size [x]})"
    22.6        using f_img by auto
    22.7 -    then have "length ys = 1" by auto
    22.8 -    moreover
    22.9 +    then have *: "length ys = 1" by auto
   22.10      then have "f 0 = 0" using f_img by auto
   22.11 -    ultimately show ?case using f_nth by (cases ys) auto
   22.12 +    with * show ?case using f_nth by (cases ys) auto
   22.13    next
   22.14      case (3 x1 x2 xs)
   22.15      from "3.prems" obtain f where f_mono: "mono f"
   22.16 @@ -5499,10 +5498,10 @@
   22.17    next
   22.18      let ?k = "length abs"
   22.19      case eq
   22.20 -    hence "abs = bcs" "b = b'" using bs bs' by auto
   22.21 -    moreover hence "(a, c') \<in> r"
   22.22 +    hence *: "abs = bcs" "b = b'" using bs bs' by auto
   22.23 +    hence "(a, c') \<in> r"
   22.24        using abr b'c'r assms unfolding trans_def by blast
   22.25 -    ultimately show ?thesis using n n' unfolding lexn_conv as bs cs by auto
   22.26 +    with * show ?thesis using n n' unfolding lexn_conv as bs cs by auto
   22.27    qed
   22.28  qed
   22.29  
   22.30 @@ -5840,8 +5839,8 @@
   22.31    (is "?lhs \<longleftrightarrow> ?rhs")
   22.32  proof
   22.33    assume ?lhs
   22.34 -  moreover hence "\<not> lexordp_eq ys xs" by induct simp_all
   22.35 -  ultimately show ?rhs by(simp add: lexordp_into_lexordp_eq)
   22.36 +  hence "\<not> lexordp_eq ys xs" by induct simp_all
   22.37 +  with \<open>?lhs\<close> show ?rhs by (simp add: lexordp_into_lexordp_eq)
   22.38  next
   22.39    assume ?rhs
   22.40    hence "lexordp_eq xs ys" "\<not> lexordp_eq ys xs" by simp_all
    23.1 --- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Fri Jul 22 08:02:37 2016 +0200
    23.2 +++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Fri Jul 22 11:00:43 2016 +0200
    23.3 @@ -71,9 +71,9 @@
    23.4  proof (induct s rule: finite_ne_induct)
    23.5    case (insert b s)
    23.6    assume *: "\<forall>x\<in>insert b s. \<forall>y\<in>insert b s. x \<le> y \<or> y \<le> x"
    23.7 -  moreover then obtain u l where "l \<in> s" "\<forall>b\<in>s. l \<le> b" "u \<in> s" "\<forall>b\<in>s. b \<le> u"
    23.8 +  then obtain u l where "l \<in> s" "\<forall>b\<in>s. l \<le> b" "u \<in> s" "\<forall>b\<in>s. b \<le> u"
    23.9      using insert by auto
   23.10 -  ultimately show "\<exists>a\<in>insert b s. \<forall>x\<in>insert b s. a \<le> x" "\<exists>a\<in>insert b s. \<forall>x\<in>insert b s. x \<le> a"
   23.11 +  with * show "\<exists>a\<in>insert b s. \<forall>x\<in>insert b s. a \<le> x" "\<exists>a\<in>insert b s. \<forall>x\<in>insert b s. x \<le> a"
   23.12      using *[rule_format, of b u] *[rule_format, of b l] by (metis insert_iff order.trans)+
   23.13  qed auto
   23.14  
    24.1 --- a/src/HOL/Multivariate_Analysis/Conformal_Mappings.thy	Fri Jul 22 08:02:37 2016 +0200
    24.2 +++ b/src/HOL/Multivariate_Analysis/Conformal_Mappings.thy	Fri Jul 22 11:00:43 2016 +0200
    24.3 @@ -1411,7 +1411,7 @@
    24.4    show no_df0: "norm(deriv f 0) \<le> 1"
    24.5      by (simp add: \<open>\<And>z. cmod z < 1 \<Longrightarrow> cmod (h z) \<le> 1\<close> df0)
    24.6    show "?Q" if "?P"
    24.7 -  using that
    24.8 +    using that
    24.9    proof
   24.10      assume "\<exists>z. cmod z < 1 \<and> z \<noteq> 0 \<and> cmod (f z) = cmod z"
   24.11      then obtain \<gamma> where \<gamma>: "cmod \<gamma> < 1" "\<gamma> \<noteq> 0" "cmod (f \<gamma>) = cmod \<gamma>" by blast
   24.12 @@ -1424,9 +1424,9 @@
   24.13        by (metis add_diff_cancel_left' diff_diff_eq2 le_less_trans noh_le norm_triangle_ineq4)
   24.14      ultimately obtain c where c: "\<And>z. norm z < 1 \<Longrightarrow> h z = c"
   24.15        using Schwarz2 [OF holh, of "1 - norm \<gamma>" \<gamma>, unfolded constant_on_def] \<gamma> by auto
   24.16 -    moreover then have "norm c = 1"
   24.17 +    then have "norm c = 1"
   24.18        using \<gamma> by force
   24.19 -    ultimately show ?thesis
   24.20 +    with c show ?thesis
   24.21        using fz_eq by auto
   24.22    next
   24.23      assume [simp]: "cmod (deriv f 0) = 1"
    25.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Fri Jul 22 08:02:37 2016 +0200
    25.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Fri Jul 22 11:00:43 2016 +0200
    25.3 @@ -10168,14 +10168,14 @@
    25.4    then have x: "{integral s (f k) |k. True} = range x"
    25.5      by auto
    25.6  
    25.7 -  have "g integrable_on s \<and> (\<lambda>k. integral s (f k)) \<longlonglongrightarrow> integral s g"
    25.8 +  have *: "g integrable_on s \<and> (\<lambda>k. integral s (f k)) \<longlonglongrightarrow> integral s g"
    25.9    proof (intro monotone_convergence_increasing allI ballI assms)
   25.10      show "bounded {integral s (f k) |k. True}"
   25.11        unfolding x by (rule convergent_imp_bounded) fact
   25.12    qed (auto intro: f)
   25.13 -  moreover then have "integral s g = x'"
   25.14 +  then have "integral s g = x'"
   25.15      by (intro LIMSEQ_unique[OF _ \<open>x \<longlonglongrightarrow> x'\<close>]) (simp add: x_eq)
   25.16 -  ultimately show ?thesis
   25.17 +  with * show ?thesis
   25.18      by (simp add: has_integral_integral)
   25.19  qed
   25.20  
   25.21 @@ -11559,18 +11559,16 @@
   25.22      with \<open>open W\<close>
   25.23      have "\<exists>X0 Y. open X0 \<and> open Y \<and> x0 \<in> X0 \<and> y \<in> Y \<and> X0 \<times> Y \<subseteq> W"
   25.24        by (rule open_prod_elim) blast
   25.25 -  } then obtain X0 Y where
   25.26 -    "\<forall>y \<in> K. open (X0 y) \<and> open (Y y) \<and> x0 \<in> X0 y \<and> y \<in> Y y \<and> X0 y \<times> Y y \<subseteq> W"
   25.27 +  }
   25.28 +  then obtain X0 Y where
   25.29 +    *: "\<forall>y \<in> K. open (X0 y) \<and> open (Y y) \<and> x0 \<in> X0 y \<and> y \<in> Y y \<and> X0 y \<times> Y y \<subseteq> W"
   25.30      by metis
   25.31 -  moreover
   25.32 -  then have "\<forall>t\<in>Y ` K. open t" "K \<subseteq> \<Union>(Y ` K)" by auto
   25.33 -  with \<open>compact K\<close> obtain CC where "CC \<subseteq> Y ` K" "finite CC" "K \<subseteq> \<Union>CC"
   25.34 +  from * have "\<forall>t\<in>Y ` K. open t" "K \<subseteq> \<Union>(Y ` K)" by auto
   25.35 +  with \<open>compact K\<close> obtain CC where CC: "CC \<subseteq> Y ` K" "finite CC" "K \<subseteq> \<Union>CC"
   25.36      by (rule compactE)
   25.37 -  moreover
   25.38 -  then obtain c where c:
   25.39 -    "\<And>C. C \<in> CC \<Longrightarrow> c C \<in> K \<and> C = Y (c C)"
   25.40 +  then obtain c where c: "\<And>C. C \<in> CC \<Longrightarrow> c C \<in> K \<and> C = Y (c C)"
   25.41      by (force intro!: choice)
   25.42 -  ultimately show ?thesis
   25.43 +  with * CC show ?thesis
   25.44      by (force intro!: exI[where x="\<Inter>C\<in>CC. X0 (c C)"])
   25.45  qed
   25.46  
    26.1 --- a/src/HOL/Multivariate_Analysis/Path_Connected.thy	Fri Jul 22 08:02:37 2016 +0200
    26.2 +++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy	Fri Jul 22 11:00:43 2016 +0200
    26.3 @@ -3057,11 +3057,11 @@
    26.4      then have ftendsw: "((\<lambda>n. f (z n)) \<circ> K) \<longlonglongrightarrow> w"
    26.5        by (metis LIMSEQ_subseq_LIMSEQ fun.map_cong0 fz tendsw)
    26.6      have zKs: "\<And>n. (z o K) n \<in> S" by (simp add: zs)
    26.7 -    have "f \<circ> z = \<xi>"  "(\<lambda>n. f (z n)) = \<xi>"
    26.8 +    have fz: "f \<circ> z = \<xi>"  "(\<lambda>n. f (z n)) = \<xi>"
    26.9        using fz by auto
   26.10 -    moreover then have "(\<xi> \<circ> K) \<longlonglongrightarrow> f y"
   26.11 +    then have "(\<xi> \<circ> K) \<longlonglongrightarrow> f y"
   26.12        by (metis (no_types) Klim zKs y contf comp_assoc continuous_on_closure_sequentially)
   26.13 -    ultimately have wy: "w = f y" using fz LIMSEQ_unique ftendsw by auto
   26.14 +    with fz have wy: "w = f y" using fz LIMSEQ_unique ftendsw by auto
   26.15      have rle: "r \<le> norm (f y - f a)"
   26.16        apply (rule le_no)
   26.17        using w wy oint
    27.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Jul 22 08:02:37 2016 +0200
    27.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Jul 22 11:00:43 2016 +0200
    27.3 @@ -4343,10 +4343,11 @@
    27.4    have "F \<noteq> bot"
    27.5      unfolding F_def
    27.6    proof (rule INF_filter_not_bot)
    27.7 -    fix X assume "X \<subseteq> insert U A" "finite X"
    27.8 -    moreover with A(2)[THEN spec, of "X - {U}"] have "U \<inter> \<Inter>(X - {U}) \<noteq> {}"
    27.9 +    fix X
   27.10 +    assume X: "X \<subseteq> insert U A" "finite X"
   27.11 +    with A(2)[THEN spec, of "X - {U}"] have "U \<inter> \<Inter>(X - {U}) \<noteq> {}"
   27.12        by auto
   27.13 -    ultimately show "(INF a:X. principal a) \<noteq> bot"
   27.14 +    with X show "(INF a:X. principal a) \<noteq> bot"
   27.15        by (auto simp add: INF_principal_finite principal_eq_bot_iff)
   27.16    qed
   27.17    moreover
   27.18 @@ -6601,13 +6602,12 @@
   27.19        then obtain xs where xs: "xs \<longlonglongrightarrow> x" "\<And>n. xs n \<in> X"
   27.20          by (auto simp: closure_sequential)
   27.21        from continuous_on_tendsto_compose[OF cont_h xs(1)] xs(2) Y
   27.22 -      have "(\<lambda>x. f (xs x)) \<longlonglongrightarrow> h x"
   27.23 +      have hx: "(\<lambda>x. f (xs x)) \<longlonglongrightarrow> h x"
   27.24          by (auto simp: set_mp extension)
   27.25 -      moreover
   27.26        then have "(\<lambda>x. f (xs x)) \<longlonglongrightarrow> y x"
   27.27          using \<open>x \<notin> X\<close> not_eventuallyD xs(2)
   27.28          by (force intro!: filterlim_compose[OF y[OF \<open>x \<in> closure X\<close>]] simp: filterlim_at xs)
   27.29 -      ultimately have "h x = y x" by (rule LIMSEQ_unique)
   27.30 +      with hx have "h x = y x" by (rule LIMSEQ_unique)
   27.31      } then
   27.32      have "h x = ?g x"
   27.33        using extension by auto
    28.1 --- a/src/HOL/Probability/Distributions.thy	Fri Jul 22 08:02:37 2016 +0200
    28.2 +++ b/src/HOL/Probability/Distributions.thy	Fri Jul 22 11:00:43 2016 +0200
    28.3 @@ -164,8 +164,8 @@
    28.4  lemma nn_integral_erlang_density:
    28.5    assumes [arith]: "0 < l"
    28.6    shows "(\<integral>\<^sup>+ x. ennreal (erlang_density k l x) * indicator {.. a} x \<partial>lborel) = erlang_CDF k l a"
    28.7 -proof cases
    28.8 -  assume [arith]: "0 \<le> a"
    28.9 +proof (cases "0 \<le> a")
   28.10 +  case [arith]: True
   28.11    have eq: "\<And>x. indicator {0..a} (x / l) = indicator {0..a*l} x"
   28.12      by (simp add: field_simps split: split_indicator)
   28.13    have "(\<integral>\<^sup>+x. ennreal (erlang_density k l x) * indicator {.. a} x \<partial>lborel) =
   28.14 @@ -182,10 +182,10 @@
   28.15      by (auto simp: erlang_CDF_def)
   28.16    finally show ?thesis .
   28.17  next
   28.18 -  assume "\<not> 0 \<le> a"
   28.19 -  moreover then have "(\<integral>\<^sup>+ x. ennreal (erlang_density k l x) * indicator {.. a} x \<partial>lborel) = (\<integral>\<^sup>+x. 0 \<partial>(lborel::real measure))"
   28.20 +  case False
   28.21 +  then have "(\<integral>\<^sup>+ x. ennreal (erlang_density k l x) * indicator {.. a} x \<partial>lborel) = (\<integral>\<^sup>+x. 0 \<partial>(lborel::real measure))"
   28.22      by (intro nn_integral_cong) (auto simp: erlang_density_def)
   28.23 -  ultimately show ?thesis
   28.24 +  with False show ?thesis
   28.25      by (simp add: erlang_CDF_def)
   28.26  qed
   28.27  
    29.1 --- a/src/HOL/Probability/Finite_Product_Measure.thy	Fri Jul 22 08:02:37 2016 +0200
    29.2 +++ b/src/HOL/Probability/Finite_Product_Measure.thy	Fri Jul 22 11:00:43 2016 +0200
    29.3 @@ -1133,10 +1133,10 @@
    29.4  lemma (in product_sigma_finite) distr_component:
    29.5    "distr (M i) (Pi\<^sub>M {i} M) (\<lambda>x. \<lambda>i\<in>{i}. x) = Pi\<^sub>M {i} M" (is "?D = ?P")
    29.6  proof (intro PiM_eqI)
    29.7 -  fix A assume "\<And>ia. ia \<in> {i} \<Longrightarrow> A ia \<in> sets (M ia)"
    29.8 -  moreover then have "(\<lambda>x. \<lambda>i\<in>{i}. x) -` Pi\<^sub>E {i} A \<inter> space (M i) = A i"
    29.9 +  fix A assume A: "\<And>ia. ia \<in> {i} \<Longrightarrow> A ia \<in> sets (M ia)"
   29.10 +  then have "(\<lambda>x. \<lambda>i\<in>{i}. x) -` Pi\<^sub>E {i} A \<inter> space (M i) = A i"
   29.11      by (auto dest: sets.sets_into_space)
   29.12 -  ultimately show "emeasure (distr (M i) (Pi\<^sub>M {i} M) (\<lambda>x. \<lambda>i\<in>{i}. x)) (Pi\<^sub>E {i} A) = (\<Prod>i\<in>{i}. emeasure (M i) (A i))"
   29.13 +  with A show "emeasure (distr (M i) (Pi\<^sub>M {i} M) (\<lambda>x. \<lambda>i\<in>{i}. x)) (Pi\<^sub>E {i} A) = (\<Prod>i\<in>{i}. emeasure (M i) (A i))"
   29.14      by (subst emeasure_distr) (auto intro!: sets_PiM_I_finite measurable_restrict)
   29.15  qed simp_all
   29.16  
    30.1 --- a/src/HOL/Probability/Giry_Monad.thy	Fri Jul 22 08:02:37 2016 +0200
    30.2 +++ b/src/HOL/Probability/Giry_Monad.thy	Fri Jul 22 11:00:43 2016 +0200
    30.3 @@ -272,28 +272,28 @@
    30.4    ultimately show ?case by simp
    30.5  next
    30.6    case (set B)
    30.7 -  moreover then have "(\<lambda>M'. \<integral>\<^sup>+M''. indicator B M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. emeasure M' B) \<in> ?B"
    30.8 +  then have "(\<lambda>M'. \<integral>\<^sup>+M''. indicator B M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. emeasure M' B) \<in> ?B"
    30.9      by (intro measurable_cong nn_integral_indicator) (simp add: space_subprob_algebra)
   30.10 -  ultimately show ?case
   30.11 +  with set show ?case
   30.12      by (simp add: measurable_emeasure_subprob_algebra)
   30.13  next
   30.14    case (mult f c)
   30.15 -  moreover then have "(\<lambda>M'. \<integral>\<^sup>+M''. c * f M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. c * \<integral>\<^sup>+M''. f M'' \<partial>M') \<in> ?B"
   30.16 +  then have "(\<lambda>M'. \<integral>\<^sup>+M''. c * f M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. c * \<integral>\<^sup>+M''. f M'' \<partial>M') \<in> ?B"
   30.17      by (intro measurable_cong nn_integral_cmult) (auto simp add: space_subprob_algebra)
   30.18 -  ultimately show ?case
   30.19 +  with mult show ?case
   30.20      by simp
   30.21  next
   30.22    case (add f g)
   30.23 -  moreover then have "(\<lambda>M'. \<integral>\<^sup>+M''. f M'' + g M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. (\<integral>\<^sup>+M''. f M'' \<partial>M') + (\<integral>\<^sup>+M''. g M'' \<partial>M')) \<in> ?B"
   30.24 +  then have "(\<lambda>M'. \<integral>\<^sup>+M''. f M'' + g M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. (\<integral>\<^sup>+M''. f M'' \<partial>M') + (\<integral>\<^sup>+M''. g M'' \<partial>M')) \<in> ?B"
   30.25      by (intro measurable_cong nn_integral_add) (auto simp add: space_subprob_algebra)
   30.26 -  ultimately show ?case
   30.27 +  with add show ?case
   30.28      by (simp add: ac_simps)
   30.29  next
   30.30    case (seq F)
   30.31 -  moreover then have "(\<lambda>M'. \<integral>\<^sup>+M''. (SUP i. F i) M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. SUP i. (\<integral>\<^sup>+M''. F i M'' \<partial>M')) \<in> ?B"
   30.32 +  then have "(\<lambda>M'. \<integral>\<^sup>+M''. (SUP i. F i) M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. SUP i. (\<integral>\<^sup>+M''. F i M'' \<partial>M')) \<in> ?B"
   30.33      unfolding SUP_apply
   30.34      by (intro measurable_cong nn_integral_monotone_convergence_SUP) (auto simp add: space_subprob_algebra)
   30.35 -  ultimately show ?case
   30.36 +  with seq show ?case
   30.37      by (simp add: ac_simps)
   30.38  qed
   30.39  
   30.40 @@ -793,10 +793,10 @@
   30.41      by simp
   30.42  next
   30.43    case (set A)
   30.44 -  moreover with M have "(\<integral>\<^sup>+ M'. integral\<^sup>N M' (indicator A) \<partial>M) = (\<integral>\<^sup>+ M'. emeasure M' A \<partial>M)"
   30.45 +  with M have "(\<integral>\<^sup>+ M'. integral\<^sup>N M' (indicator A) \<partial>M) = (\<integral>\<^sup>+ M'. emeasure M' A \<partial>M)"
   30.46      by (intro nn_integral_cong nn_integral_indicator)
   30.47         (auto simp: space_subprob_algebra dest!: sets_eq_imp_space_eq)
   30.48 -  ultimately show ?case
   30.49 +  with set show ?case
   30.50      using M by (simp add: emeasure_join)
   30.51  next
   30.52    case (mult f c)
    31.1 --- a/src/HOL/Probability/Infinite_Product_Measure.thy	Fri Jul 22 08:02:37 2016 +0200
    31.2 +++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Fri Jul 22 11:00:43 2016 +0200
    31.3 @@ -29,14 +29,18 @@
    31.4    note * = this
    31.5  
    31.6    have "emeasure (PiM I M) (emb I J (PiE J X)) = (\<Prod>i\<in>J. M i (X i))"
    31.7 -  proof cases
    31.8 -    assume "\<not> (J \<noteq> {} \<or> I = {})"
    31.9 -    then obtain i where "J = {}" "i \<in> I" by auto
   31.10 -    moreover then have "emb I {} {\<lambda>x. undefined} = emb I {i} (\<Pi>\<^sub>E i\<in>{i}. space (M i))"
   31.11 +  proof (cases "J \<noteq> {} \<or> I = {}")
   31.12 +    case False
   31.13 +    then obtain i where i: "J = {}" "i \<in> I" by auto
   31.14 +    then have "emb I {} {\<lambda>x. undefined} = emb I {i} (\<Pi>\<^sub>E i\<in>{i}. space (M i))"
   31.15        by (auto simp: space_PiM prod_emb_def)
   31.16 -    ultimately show ?thesis
   31.17 +    with i show ?thesis
   31.18        by (simp add: * M.emeasure_space_1)
   31.19 -  qed (simp add: *[OF _ assms X])
   31.20 +  next
   31.21 +    case True
   31.22 +    then show ?thesis
   31.23 +      by (simp add: *[OF _ assms X])
   31.24 +  qed
   31.25    with assms show "emeasure (distr (Pi\<^sub>M I M) (Pi\<^sub>M J M) (\<lambda>x. restrict x J)) (Pi\<^sub>E J X) = (\<Prod>i\<in>J. emeasure (M i) (X i))"
   31.26      by (subst emeasure_distr_restrict[OF _ refl]) (auto intro!: sets_PiM_I_finite X)
   31.27  qed (insert assms, auto)
    32.1 --- a/src/HOL/Probability/Lebesgue_Integral_Substitution.thy	Fri Jul 22 08:02:37 2016 +0200
    32.2 +++ b/src/HOL/Probability/Lebesgue_Integral_Substitution.thy	Fri Jul 22 11:00:43 2016 +0200
    32.3 @@ -323,9 +323,9 @@
    32.4      and "(LBINT x. f x * indicator {g a..g b} x) = (LBINT x. f (g x) * g' x * indicator {a..b} x)"
    32.5  proof-
    32.6    from derivg have contg: "continuous_on {a..b} g" by (rule has_real_derivative_imp_continuous_on)
    32.7 -  from this and contg' have Mg: "set_borel_measurable borel {a..b} g" and
    32.8 -                             Mg': "set_borel_measurable borel {a..b} g'"
    32.9 -      by (simp_all only: set_measurable_continuous_on_ivl)
   32.10 +  with contg' have Mg: "set_borel_measurable borel {a..b} g"
   32.11 +    and Mg': "set_borel_measurable borel {a..b} g'"
   32.12 +    by (simp_all only: set_measurable_continuous_on_ivl)
   32.13    from derivg derivg_nonneg have monog: "\<And>x y. a \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> y \<le> b \<Longrightarrow> g x \<le> g y"
   32.14      by (rule deriv_nonneg_imp_mono) simp_all
   32.15  
   32.16 @@ -341,18 +341,18 @@
   32.17            enn2real (\<integral>\<^sup>+ x. ennreal (f x) * indicator {g a..g b} x \<partial>lborel) -
   32.18            enn2real (\<integral>\<^sup>+ x. ennreal (- (f x)) * indicator {g a..g b} x \<partial>lborel)" using integrable
   32.19      by (subst real_lebesgue_integral_def) (simp_all add: nn_integral_set_ennreal mult.commute)
   32.20 -  also have "(\<integral>\<^sup>+x. ennreal (f x) * indicator {g a..g b} x \<partial>lborel) =
   32.21 -               (\<integral>\<^sup>+x. ennreal (f x * indicator {g a..g b} x) \<partial>lborel)"
   32.22 +  also have *: "(\<integral>\<^sup>+x. ennreal (f x) * indicator {g a..g b} x \<partial>lborel) =
   32.23 +      (\<integral>\<^sup>+x. ennreal (f x * indicator {g a..g b} x) \<partial>lborel)"
   32.24      by (intro nn_integral_cong) (simp split: split_indicator)
   32.25 -  also with M1 have A: "(\<integral>\<^sup>+ x. ennreal (f x * indicator {g a..g b} x) \<partial>lborel) =
   32.26 +  also from M1 * have A: "(\<integral>\<^sup>+ x. ennreal (f x * indicator {g a..g b} x) \<partial>lborel) =
   32.27                              (\<integral>\<^sup>+ x. ennreal (f (g x) * g' x * indicator {a..b} x) \<partial>lborel)"
   32.28      by (subst nn_integral_substitution[OF _ derivg contg' derivg_nonneg \<open>a \<le> b\<close>])
   32.29         (auto simp: nn_integral_set_ennreal mult.commute)
   32.30 -  also have "(\<integral>\<^sup>+ x. ennreal (- (f x)) * indicator {g a..g b} x \<partial>lborel) =
   32.31 -               (\<integral>\<^sup>+ x. ennreal (- (f x) * indicator {g a..g b} x) \<partial>lborel)"
   32.32 +  also have **: "(\<integral>\<^sup>+ x. ennreal (- (f x)) * indicator {g a..g b} x \<partial>lborel) =
   32.33 +      (\<integral>\<^sup>+ x. ennreal (- (f x) * indicator {g a..g b} x) \<partial>lborel)"
   32.34      by (intro nn_integral_cong) (simp split: split_indicator)
   32.35 -  also with M2 have B: "(\<integral>\<^sup>+ x. ennreal (- (f x) * indicator {g a..g b} x) \<partial>lborel) =
   32.36 -                            (\<integral>\<^sup>+ x. ennreal (- (f (g x)) * g' x * indicator {a..b} x) \<partial>lborel)"
   32.37 +  also from M2 ** have B: "(\<integral>\<^sup>+ x. ennreal (- (f x) * indicator {g a..g b} x) \<partial>lborel) =
   32.38 +        (\<integral>\<^sup>+ x. ennreal (- (f (g x)) * g' x * indicator {a..b} x) \<partial>lborel)"
   32.39      by (subst nn_integral_substitution[OF _ derivg contg' derivg_nonneg \<open>a \<le> b\<close>])
   32.40         (auto simp: nn_integral_set_ennreal mult.commute)
   32.41  
    33.1 --- a/src/HOL/Probability/Lebesgue_Measure.thy	Fri Jul 22 08:02:37 2016 +0200
    33.2 +++ b/src/HOL/Probability/Lebesgue_Measure.thy	Fri Jul 22 11:00:43 2016 +0200
    33.3 @@ -75,9 +75,9 @@
    33.4            fix i assume "i \<in> S - {m}"
    33.5            then have i: "i \<in> S" "i \<noteq> m" by auto
    33.6            { assume i': "l i < r i" "l i < r m"
    33.7 -            moreover with \<open>finite S\<close> i m have "l m \<le> l i"
    33.8 +            with \<open>finite S\<close> i m have "l m \<le> l i"
    33.9                by auto
   33.10 -            ultimately have "{l i <.. r i} \<inter> {l m <.. r m} \<noteq> {}"
   33.11 +            with i' have "{l i <.. r i} \<inter> {l m <.. r m} \<noteq> {}"
   33.12                by auto
   33.13              then have False
   33.14                using disjoint_family_onD[OF disj, of i m] i by auto }
   33.15 @@ -852,9 +852,9 @@
   33.16    shows "(f has_integral r) UNIV"
   33.17  using f proof (induct f arbitrary: r rule: borel_measurable_induct_real)
   33.18    case (set A)
   33.19 -  moreover then have "((\<lambda>x. 1) has_integral measure lborel A) A"
   33.20 +  then have "((\<lambda>x. 1) has_integral measure lborel A) A"
   33.21      by (intro has_integral_measure_lborel) (auto simp: ennreal_indicator)
   33.22 -  ultimately show ?case
   33.23 +  with set show ?case
   33.24      by (simp add: ennreal_indicator measure_def) (simp add: indicator_def)
   33.25  next
   33.26    case (mult g c)
   33.27 @@ -868,13 +868,12 @@
   33.28      by (auto intro!: has_integral_cmult_real)
   33.29  next
   33.30    case (add g h)
   33.31 -  moreover
   33.32    then have "(\<integral>\<^sup>+ x. h x + g x \<partial>lborel) = (\<integral>\<^sup>+ x. h x \<partial>lborel) + (\<integral>\<^sup>+ x. g x \<partial>lborel)"
   33.33      by (simp add: nn_integral_add)
   33.34    with add obtain a b where "0 \<le> a" "0 \<le> b" "(\<integral>\<^sup>+ x. h x \<partial>lborel) = ennreal a" "(\<integral>\<^sup>+ x. g x \<partial>lborel) = ennreal b" "r = a + b"
   33.35      by (cases "\<integral>\<^sup>+ x. h x \<partial>lborel" "\<integral>\<^sup>+ x. g x \<partial>lborel" rule: ennreal2_cases)
   33.36         (auto simp: add_top nn_integral_add top_add ennreal_plus[symmetric] simp del: ennreal_plus)
   33.37 -  ultimately show ?case
   33.38 +  with add show ?case
   33.39      by (auto intro!: has_integral_add)
   33.40  next
   33.41    case (seq U)
   33.42 @@ -1020,8 +1019,8 @@
   33.43    fixes A :: "'a::euclidean_space set"
   33.44    assumes A[measurable]: "A \<in> sets borel" and [simp]: "0 \<le> r"
   33.45    shows "((\<lambda>x. 1) has_integral r) A \<longleftrightarrow> emeasure lborel A = ennreal r"
   33.46 -proof cases
   33.47 -  assume emeasure_A: "emeasure lborel A = \<infinity>"
   33.48 +proof (cases "emeasure lborel A = \<infinity>")
   33.49 +  case emeasure_A: True
   33.50    have "\<not> (\<lambda>x. 1::real) integrable_on A"
   33.51    proof
   33.52      assume int: "(\<lambda>x. 1::real) integrable_on A"
   33.53 @@ -1035,10 +1034,10 @@
   33.54    with emeasure_A show ?thesis
   33.55      by auto
   33.56  next
   33.57 -  assume "emeasure lborel A \<noteq> \<infinity>"
   33.58 -  moreover then have "((\<lambda>x. 1) has_integral measure lborel A) A"
   33.59 +  case False
   33.60 +  then have "((\<lambda>x. 1) has_integral measure lborel A) A"
   33.61      by (simp add: has_integral_measure_lborel less_top)
   33.62 -  ultimately show ?thesis
   33.63 +  with False show ?thesis
   33.64      by (auto simp: emeasure_eq_ennreal_measure has_integral_unique)
   33.65  qed
   33.66  
    34.1 --- a/src/HOL/Probability/Levy.thy	Fri Jul 22 08:02:37 2016 +0200
    34.2 +++ b/src/HOL/Probability/Levy.thy	Fri Jul 22 11:00:43 2016 +0200
    34.3 @@ -391,23 +391,22 @@
    34.4                  continuous_intros ballI M'.isCont_char continuous_intros)
    34.5      have "cmod (CLBINT t:{-d/2..d/2}. 1 - char M' t) \<le> LBINT t:{-d/2..d/2}. cmod (1 - char M' t)"
    34.6        using integral_norm_bound[OF 2] by simp
    34.7 -    also have "\<dots> \<le> LBINT t:{-d/2..d/2}. \<epsilon> / 4"
    34.8 +    also have 4: "\<dots> \<le> LBINT t:{-d/2..d/2}. \<epsilon> / 4"
    34.9        apply (rule integral_mono [OF 3])
   34.10 -      apply (simp add: emeasure_lborel_Icc_eq)
   34.11 -      apply (case_tac "x \<in> {-d/2..d/2}", auto)
   34.12 +       apply (simp add: emeasure_lborel_Icc_eq)
   34.13 +      apply (case_tac "x \<in> {-d/2..d/2}")
   34.14 +       apply auto
   34.15        apply (subst norm_minus_commute)
   34.16        apply (rule less_imp_le)
   34.17        apply (rule d1 [simplified])
   34.18 -      using d0 by auto
   34.19 -    also with d0 have "\<dots> = d * \<epsilon> / 4"
   34.20 +      using d0 apply auto
   34.21 +      done
   34.22 +    also from d0 4 have "\<dots> = d * \<epsilon> / 4"
   34.23        by simp
   34.24      finally have bound: "cmod (CLBINT t:{-d/2..d/2}. 1 - char M' t) \<le> d * \<epsilon> / 4" .
   34.25 -    { fix n x
   34.26 -      have "cmod (1 - char (M n) x) \<le> 2"
   34.27 -        by (rule order_trans [OF norm_triangle_ineq4], auto simp add: Mn.cmod_char_le_1)
   34.28 -    } note bd1 = this
   34.29 -    have "(\<lambda>n. CLBINT t:{-d/2..d/2}. 1 - char (M n) t) \<longlonglongrightarrow> (CLBINT t:{-d/2..d/2}. 1 - char M' t)"
   34.30 -      using bd1
   34.31 +    have "cmod (1 - char (M n) x) \<le> 2" for n x
   34.32 +      by (rule order_trans [OF norm_triangle_ineq4], auto simp add: Mn.cmod_char_le_1)
   34.33 +    then have "(\<lambda>n. CLBINT t:{-d/2..d/2}. 1 - char (M n) t) \<longlonglongrightarrow> (CLBINT t:{-d/2..d/2}. 1 - char M' t)"
   34.34        apply (intro integral_dominated_convergence[where w="\<lambda>x. indicator {-d/2..d/2} x *\<^sub>R 2"])
   34.35        apply (auto intro!: char_conv tendsto_intros
   34.36                    simp: emeasure_lborel_Icc_eq
    35.1 --- a/src/HOL/Probability/Measure_Space.thy	Fri Jul 22 08:02:37 2016 +0200
    35.2 +++ b/src/HOL/Probability/Measure_Space.thy	Fri Jul 22 11:00:43 2016 +0200
    35.3 @@ -1862,7 +1862,7 @@
    35.4      using f unfolding Pi_def bij_betw_def by auto
    35.5    fix X assume "X \<in> sets (distr (count_space A) (count_space B) f)"
    35.6    then have X: "X \<in> sets (count_space B)" by auto
    35.7 -  moreover then have "f -` X \<inter> A = the_inv_into A f ` X"
    35.8 +  moreover from X have "f -` X \<inter> A = the_inv_into A f ` X"
    35.9      using f by (auto simp: bij_betw_def subset_image_iff image_iff the_inv_into_f_f intro: the_inv_into_f_f[symmetric])
   35.10    moreover have "inj_on (the_inv_into A f) B"
   35.11      using X f by (auto simp: bij_betw_def inj_on_the_inv_into)
   35.12 @@ -1932,8 +1932,8 @@
   35.13  lemma emeasure_restrict_space:
   35.14    assumes "\<Omega> \<inter> space M \<in> sets M" "A \<subseteq> \<Omega>"
   35.15    shows "emeasure (restrict_space M \<Omega>) A = emeasure M A"
   35.16 -proof cases
   35.17 -  assume "A \<in> sets M"
   35.18 +proof (cases "A \<in> sets M")
   35.19 +  case True
   35.20    show ?thesis
   35.21    proof (rule emeasure_measure_of[OF restrict_space_def])
   35.22      show "op \<inter> \<Omega> ` sets M \<subseteq> Pow (\<Omega> \<inter> space M)" "A \<in> sets (restrict_space M \<Omega>)"
   35.23 @@ -1951,10 +1951,10 @@
   35.24      qed
   35.25    qed
   35.26  next
   35.27 -  assume "A \<notin> sets M"
   35.28 -  moreover with assms have "A \<notin> sets (restrict_space M \<Omega>)"
   35.29 +  case False
   35.30 +  with assms have "A \<notin> sets (restrict_space M \<Omega>)"
   35.31      by (simp add: sets_restrict_space_iff)
   35.32 -  ultimately show ?thesis
   35.33 +  with False show ?thesis
   35.34      by (simp add: emeasure_notin_sets)
   35.35  qed
   35.36  
    36.1 --- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Fri Jul 22 08:02:37 2016 +0200
    36.2 +++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Fri Jul 22 11:00:43 2016 +0200
    36.3 @@ -1734,7 +1734,7 @@
    36.4  proof (rule measure_eqI)
    36.5    fix X assume "X \<in> sets M"
    36.6    then have X: "X \<subseteq> A" by auto
    36.7 -  moreover with A have "countable X" by (auto dest: countable_subset)
    36.8 +  moreover from A X have "countable X" by (auto dest: countable_subset)
    36.9    ultimately have
   36.10      "emeasure M X = (\<integral>\<^sup>+a. emeasure M {a} \<partial>count_space X)"
   36.11      "emeasure N X = (\<integral>\<^sup>+a. emeasure N {a} \<partial>count_space X)"
    37.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Fri Jul 22 08:02:37 2016 +0200
    37.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Fri Jul 22 11:00:43 2016 +0200
    37.3 @@ -1104,17 +1104,17 @@
    37.4    assume eq: "\<forall>x\<in>set_pmf p. \<forall>y\<in>set_pmf q. R x y \<longrightarrow> measure p {x. R x y} = measure q {y. R x y}"
    37.5  
    37.6    show "measure p C = measure q C"
    37.7 -  proof cases
    37.8 -    assume "p \<inter> C = {}"
    37.9 -    moreover then have "q \<inter> C = {}"
   37.10 +  proof (cases "p \<inter> C = {}")
   37.11 +    case True
   37.12 +    then have "q \<inter> C = {}"
   37.13        using quotient_rel_set_disjoint[OF assms C R] by simp
   37.14 -    ultimately show ?thesis
   37.15 +    with True show ?thesis
   37.16        unfolding measure_pmf_zero_iff[symmetric] by simp
   37.17    next
   37.18 -    assume "p \<inter> C \<noteq> {}"
   37.19 -    moreover then have "q \<inter> C \<noteq> {}"
   37.20 +    case False
   37.21 +    then have "q \<inter> C \<noteq> {}"
   37.22        using quotient_rel_set_disjoint[OF assms C R] by simp
   37.23 -    ultimately obtain x y where in_set: "x \<in> set_pmf p" "y \<in> set_pmf q" and in_C: "x \<in> C" "y \<in> C"
   37.24 +    with False obtain x y where in_set: "x \<in> set_pmf p" "y \<in> set_pmf q" and in_C: "x \<in> C" "y \<in> C"
   37.25        by auto
   37.26      then have "R x y"
   37.27        using in_quotient_imp_in_rel[of UNIV ?R C x y] C assms
    38.1 --- a/src/HOL/Probability/Radon_Nikodym.thy	Fri Jul 22 08:02:37 2016 +0200
    38.2 +++ b/src/HOL/Probability/Radon_Nikodym.thy	Fri Jul 22 11:00:43 2016 +0200
    38.3 @@ -840,11 +840,11 @@
    38.4    assumes "f \<in> borel_measurable M" "density M f = N"
    38.5    shows "density M (RN_deriv M N) = N"
    38.6  proof -
    38.7 -  have "\<exists>f. f \<in> borel_measurable M \<and> density M f = N"
    38.8 +  have *: "\<exists>f. f \<in> borel_measurable M \<and> density M f = N"
    38.9      using assms by auto
   38.10 -  moreover then have "density M (SOME f. f \<in> borel_measurable M \<and> density M f = N) = N"
   38.11 +  then have "density M (SOME f. f \<in> borel_measurable M \<and> density M f = N) = N"
   38.12      by (rule someI2_ex) auto
   38.13 -  ultimately show ?thesis
   38.14 +  with * show ?thesis
   38.15      by (auto simp: RN_deriv_def)
   38.16  qed
   38.17  
    39.1 --- a/src/HOL/Probability/SPMF.thy	Fri Jul 22 08:02:37 2016 +0200
    39.2 +++ b/src/HOL/Probability/SPMF.thy	Fri Jul 22 11:00:43 2016 +0200
    39.3 @@ -2520,8 +2520,8 @@
    39.4      ultimately have "(weight_spmf p * weight_spmf q) * (weight_spmf p * weight_spmf q) = 1" by simp
    39.5      hence *: "weight_spmf p * weight_spmf q = 1"
    39.6        by(metis antisym_conv less_le mult_less_cancel_left1 weight_pair_spmf weight_spmf_le_1 weight_spmf_nonneg)
    39.7 -    hence "weight_spmf p = 1" by(metis antisym_conv mult_left_le weight_spmf_le_1 weight_spmf_nonneg)
    39.8 -    moreover with * have "weight_spmf q = 1" by simp
    39.9 +    hence **: "weight_spmf p = 1" by(metis antisym_conv mult_left_le weight_spmf_le_1 weight_spmf_nonneg)
   39.10 +    moreover from * ** have "weight_spmf q = 1" by simp
   39.11      moreover note calculation }
   39.12    note full = this
   39.13  
    40.1 --- a/src/HOL/Quotient_Examples/Int_Pow.thy	Fri Jul 22 08:02:37 2016 +0200
    40.2 +++ b/src/HOL/Quotient_Examples/Int_Pow.thy	Fri Jul 22 11:00:43 2016 +0200
    40.3 @@ -41,8 +41,8 @@
    40.4    "[| x \<in> Units G; y \<in> Units G |] ==> inv (x \<otimes> y) = inv y \<otimes> inv x"
    40.5  proof -
    40.6    assume G: "x \<in> Units G"  "y \<in> Units G"
    40.7 -  moreover then have "x \<in> carrier G"  "y \<in> carrier G" by auto
    40.8 -  ultimately have "inv (x \<otimes> y) \<otimes> (x \<otimes> y) = (inv y \<otimes> inv x) \<otimes> (x \<otimes> y)"
    40.9 +  then have "x \<in> carrier G"  "y \<in> carrier G" by auto
   40.10 +  with G have "inv (x \<otimes> y) \<otimes> (x \<otimes> y) = (inv y \<otimes> inv x) \<otimes> (x \<otimes> y)"
   40.11      by (simp add: m_assoc) (simp add: m_assoc [symmetric])
   40.12    with G show ?thesis by (simp del: Units_l_inv)
   40.13  qed
    41.1 --- a/src/HOL/Set_Interval.thy	Fri Jul 22 08:02:37 2016 +0200
    41.2 +++ b/src/HOL/Set_Interval.thy	Fri Jul 22 11:00:43 2016 +0200
    41.3 @@ -578,9 +578,9 @@
    41.4    obtain y where "Max {a <..} < y"
    41.5      using gt_ex by auto
    41.6  
    41.7 -  obtain x where "a < x"
    41.8 +  obtain x where x: "a < x"
    41.9      using gt_ex by auto
   41.10 -  also then have "x \<le> Max {a <..}"
   41.11 +  also from x have "x \<le> Max {a <..}"
   41.12      by fact
   41.13    also note \<open>Max {a <..} < y\<close>
   41.14    finally have "y \<le> Max { a <..}"
    42.1 --- a/src/HOL/Transcendental.thy	Fri Jul 22 08:02:37 2016 +0200
    42.2 +++ b/src/HOL/Transcendental.thy	Fri Jul 22 11:00:43 2016 +0200
    42.3 @@ -1617,14 +1617,15 @@
    42.4  
    42.5  lemma isCont_ln:
    42.6    fixes x::real assumes "x \<noteq> 0" shows "isCont ln x"
    42.7 -proof cases
    42.8 -  assume "0 < x"
    42.9 -  moreover then have "isCont ln (exp (ln x))"
   42.10 +proof (cases "0 < x")
   42.11 +  case True
   42.12 +  then have "isCont ln (exp (ln x))"
   42.13      by (intro isCont_inv_fun[where d="\<bar>x\<bar>" and f=exp]) auto
   42.14 -  ultimately show ?thesis
   42.15 +  with True show ?thesis
   42.16      by simp
   42.17  next
   42.18 -  assume "\<not> 0 < x" with \<open>x \<noteq> 0\<close> show "isCont ln x"
   42.19 +  case False
   42.20 +  with \<open>x \<noteq> 0\<close> show "isCont ln x"
   42.21      unfolding isCont_def
   42.22      by (subst filterlim_cong[OF _ refl, of _ "nhds (ln 0)" _ "\<lambda>_. ln 0"])
   42.23         (auto simp: ln_neg_is_const not_less eventually_at dist_real_def
   42.24 @@ -4902,11 +4903,11 @@
   42.25    have x1: "x \<le> 1"
   42.26      using assms
   42.27      by (metis le_add_same_cancel1 power2_le_imp_le power_one zero_le_power2)
   42.28 -  moreover with assms have ax: "0 \<le> arccos x" "cos(arccos x) = x"
   42.29 +  with assms have ax: "0 \<le> arccos x" "cos (arccos x) = x"
   42.30      by (auto simp: arccos)
   42.31 -  moreover have "y = sqrt (1 - x\<^sup>2)" using assms
   42.32 +  from assms have "y = sqrt (1 - x\<^sup>2)"
   42.33      by (metis abs_of_nonneg add.commute add_diff_cancel real_sqrt_abs)
   42.34 -  ultimately show ?thesis using assms arccos_le_pi2 [of x]
   42.35 +  with x1 ax assms arccos_le_pi2 [of x] show ?thesis
   42.36      by (rule_tac x="arccos x" in exI) (auto simp: sin_arccos)
   42.37  qed
   42.38  
   42.39 @@ -5836,26 +5837,25 @@
   42.40      assume ?lhs
   42.41      with * have "(\<forall>i\<le>n. c i = (if i=0 then k else 0))"
   42.42        by (simp add: polyfun_eq_coeffs [symmetric])
   42.43 -    then show ?rhs
   42.44 -      by simp
   42.45 +    then show ?rhs by simp
   42.46    next
   42.47 -    assume ?rhs then show ?lhs
   42.48 -      by (induct n) auto
   42.49 +    assume ?rhs
   42.50 +    then show ?lhs by (induct n) auto
   42.51    qed
   42.52  qed
   42.53  
   42.54  lemma root_polyfun:
   42.55 -  fixes z:: "'a::idom"
   42.56 +  fixes z :: "'a::idom"
   42.57    assumes "1 \<le> n"
   42.58 -    shows "z^n = a \<longleftrightarrow> (\<Sum>i\<le>n. (if i = 0 then -a else if i=n then 1 else 0) * z^i) = 0"
   42.59 +  shows "z^n = a \<longleftrightarrow> (\<Sum>i\<le>n. (if i = 0 then -a else if i=n then 1 else 0) * z^i) = 0"
   42.60    using assms
   42.61 -  by (cases n; simp add: setsum_head_Suc atLeast0AtMost [symmetric])
   42.62 +  by (cases n) (simp_all add: setsum_head_Suc atLeast0AtMost [symmetric])
   42.63  
   42.64  lemma
   42.65 -    fixes zz :: "'a::{idom,real_normed_div_algebra}"
   42.66 +  fixes zz :: "'a::{idom,real_normed_div_algebra}"
   42.67    assumes "1 \<le> n"
   42.68 -    shows finite_roots_unity: "finite {z::'a. z^n = 1}"
   42.69 -      and card_roots_unity:   "card {z::'a. z^n = 1} \<le> n"
   42.70 +  shows finite_roots_unity: "finite {z::'a. z^n = 1}"
   42.71 +    and card_roots_unity: "card {z::'a. z^n = 1} \<le> n"
   42.72    using polyfun_rootbound [of "\<lambda>i. if i = 0 then -1 else if i=n then 1 else 0" n n] assms
   42.73    by (auto simp add: root_polyfun [OF assms])
   42.74  
    43.1 --- a/src/HOL/ex/Ballot.thy	Fri Jul 22 08:02:37 2016 +0200
    43.2 +++ b/src/HOL/ex/Ballot.thy	Fri Jul 22 11:00:43 2016 +0200
    43.3 @@ -180,10 +180,10 @@
    43.4        by auto
    43.5      show "(\<lambda>V. V - {?l}) \<in> ?V (\<lambda>V. ?l \<in> V) \<rightarrow> {V \<in> Pow {0..<a + Suc b}. card V = a \<and> ?Q V (a + Suc b)}"
    43.6        by (auto simp: Ico_subset_finite *)
    43.7 -    { fix V assume "V \<subseteq> {0..<?l}"
    43.8 -      moreover then have "finite V" "?l \<notin> V" "{0..<Suc ?l} \<inter> V = V"
    43.9 +    { fix V assume V: "V \<subseteq> {0..<?l}"
   43.10 +      then have "finite V" "?l \<notin> V" "{0..<Suc ?l} \<inter> V = V"
   43.11          by (auto dest: finite_subset)
   43.12 -      ultimately have "card (insert ?l V) = Suc (card V)"
   43.13 +      with V have "card (insert ?l V) = Suc (card V)"
   43.14          "card ({0..<m} \<inter> insert ?l V) = (if m = Suc ?l then Suc (card V) else card ({0..<m} \<inter> V))"
   43.15          if "m \<le> Suc ?l" for m
   43.16          using that by auto }