--- a/src/HOL/Archimedean_Field.thy Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Archimedean_Field.thy Fri Jul 22 11:00:43 2016 +0200
@@ -395,9 +395,9 @@
by blast
then have l: "l = - r"
by simp
- moreover with \<open>l \<noteq> 0\<close> False have "r > 0"
+ with \<open>l \<noteq> 0\<close> False have "r > 0"
by simp
- ultimately show ?thesis
+ with l show ?thesis
using pos_mod_bound [of r]
by (auto simp add: zmod_zminus2_eq_if less_le field_simps intro: floor_unique)
qed
--- a/src/HOL/Cardinals/Ordinal_Arithmetic.thy Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Cardinals/Ordinal_Arithmetic.thy Fri Jul 22 11:00:43 2016 +0200
@@ -310,11 +310,11 @@
have minim[simp]: "minim r' (Field r') \<in> Field r'"
using wo_rel.minim_inField[unfolded wo_rel_def, OF WELL' _ r'] by auto
{ fix b
- assume "(b, minim r' (Field r')) \<in> r'"
- moreover hence "b \<in> Field r'" unfolding Field_def by auto
+ assume b: "(b, minim r' (Field r')) \<in> r'"
+ hence "b \<in> Field r'" unfolding Field_def by auto
hence "(minim r' (Field r'), b) \<in> r'"
using wo_rel.minim_least[unfolded wo_rel_def, OF WELL' subset_refl] r' by auto
- ultimately have "b = minim r' (Field r')"
+ with b have "b = minim r' (Field r')"
by (metis WELL' antisym_def linear_order_on_def partial_order_on_def well_order_on_def)
} note * = this
have 1: "Well_order (r *o r')" using assms by (auto simp add: oprod_Well_order)
@@ -772,9 +772,9 @@
have "G \<subseteq> fin_support r.zero (Field s)"
unfolding FinFunc_def fin_support_def proof safe
fix g assume "g \<in> G"
- with GF obtain f where "f \<in> F" "g = f(z := r.zero)" by auto
- moreover with SUPPF have "finite (SUPP f)" by blast
- ultimately show "finite (SUPP g)"
+ with GF obtain f where f: "f \<in> F" "g = f(z := r.zero)" by auto
+ with SUPPF have "finite (SUPP f)" by blast
+ with f show "finite (SUPP g)"
by (elim finite_subset[rotated]) (auto simp: support_def)
qed
moreover from F GF zField have "G \<subseteq> Func (Field s) (Field r)"
@@ -831,13 +831,12 @@
case True
with f have "f(z := r.zero) \<in> G" unfolding G_def by blast
with g0(2) f0z have "(f0(z := r.zero), f(z := r.zero)) \<in> oexp" by auto
- hence "(f0(z := r.zero, z := x0), f(z := r.zero, z := x0)) \<in> oexp"
+ hence oexp: "(f0(z := r.zero, z := x0), f(z := r.zero, z := x0)) \<in> oexp"
by (elim fun_upd_same_oexp[OF _ _ zField x0Field]) simp
- moreover
with f F(1) x0min True
have "(f(z := x0), f) \<in> oexp" unfolding G_def r.isMinim_def
by (intro fun_upd_smaller_oexp[OF _ zField x0Field]) auto
- ultimately show ?thesis using transD[OF oexp_trans, of f0 "f(z := x0)" f]
+ with oexp show ?thesis using transD[OF oexp_trans, of f0 "f(z := x0)" f]
unfolding f0_def by auto
next
case False note notG = this
@@ -1336,10 +1335,9 @@
hence max_Field: "t.max_fun_diff h (F g) \<in> {a \<in> Field t. h a \<noteq> F g a}"
by (rule rt.max_fun_diff_in[OF _ gh(2,3)])
{ assume *: "t.max_fun_diff h (F g) \<notin> f ` Field s"
- with max_Field have "F g (t.max_fun_diff h (F g)) = r.zero" unfolding F_def by auto
- moreover
+ with max_Field have **: "F g (t.max_fun_diff h (F g)) = r.zero" unfolding F_def by auto
with * gh(4) have "h (t.max_fun_diff h (F g)) = r.zero" unfolding Let_def by auto
- ultimately have False using max_Field gh(2,3) unfolding FinFunc_def Func_def by auto
+ with ** have False using max_Field gh(2,3) unfolding FinFunc_def Func_def by auto
}
hence max_f_Field: "t.max_fun_diff h (F g) \<in> f ` Field s" by blast
{ fix z assume z: "z \<in> Field t - f ` Field s"
@@ -1433,7 +1431,6 @@
with f inj have neq: "?f h \<noteq> ?f g"
unfolding fun_eq_iff inj_on_def rt.oexp_def map_option_case FinFunc_def Func_def Let_def
by simp metis
- moreover
with hg have "t.max_fun_diff (?f h) (?f g) = t.max_fun_diff h g" unfolding rt.oexp_def
using rt.max_fun_diff[OF \<open>h \<noteq> g\<close>] rt.max_fun_diff_in[OF \<open>h \<noteq> g\<close>]
by (subst t.max_fun_diff_def, intro t.maxim_equality)
@@ -1441,7 +1438,7 @@
with Field_fg Field_fh hg fz f_underS compat neq have "(?f h, ?f g) \<in> st.oexp"
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
unfolding rt.oexp_def st.oexp_def Let_def compat_def by auto
- ultimately show "?f h \<in> underS (s ^o t) (?f g)" unfolding underS_def by auto
+ with neq show "?f h \<in> underS (s ^o t) (?f g)" unfolding underS_def by auto
qed
ultimately have "?f g \<in> Field (s ^o t) \<and> ?f ` underS (r ^o t) g \<subseteq> underS (s ^o t) (?f g)"
by blast
@@ -1609,12 +1606,12 @@
have **: "(\<Union>g \<in> fg ` Field t. rs.SUPP g) =
(\<Union>g \<in> fg ` Field t - {rs.const}. rs.SUPP g)"
unfolding support_def by auto
- from * have "\<forall>g \<in> fg ` Field t. finite (rs.SUPP g)" "finite (rst.SUPP fg)"
+ from * have ***: "\<forall>g \<in> fg ` Field t. finite (rs.SUPP g)" "finite (rst.SUPP fg)"
unfolding rs.Field_oexp FinFunc_def Func_def fin_support_def Option.these_def by force+
- moreover hence "finite (fg ` Field t - {rs.const})" using *
+ hence "finite (fg ` Field t - {rs.const})" using *
unfolding support_def rs.zero_oexp[OF Field] FinFunc_def Func_def
by (elim finite_surj[of _ _ fg]) (fastforce simp: image_iff Option.these_def)
- ultimately have "finite ((\<Union>g \<in> fg ` Field t. rs.SUPP g) \<times> rst.SUPP fg)"
+ with *** have "finite ((\<Union>g \<in> fg ` Field t. rs.SUPP g) \<times> rst.SUPP fg)"
by (subst **) (auto intro!: finite_cartesian_product)
with * show "?g \<in> FinFunc r (s *o t)"
unfolding Field_oprod rs.Field_oexp FinFunc_def Func_def fin_support_def Option.these_def
@@ -1680,8 +1677,9 @@
ordIso_transitive[OF oone_ordIso_oexp[OF ordIso_symmetric[OF oone_ordIso] t] oone_ordIso])
next
case False
- moreover hence "s *o t \<noteq> {}" unfolding oprod_def Field_def by fastforce
- ultimately show ?thesis using \<open>r = {}\<close> ozero_ordIso
+ hence "s *o t \<noteq> {}" unfolding oprod_def Field_def by fastforce
+ with False show ?thesis
+ using \<open>r = {}\<close> ozero_ordIso
by (auto simp add: s t oprod_Well_order ozero_def)
qed
next
--- a/src/HOL/Cardinals/Wellorder_Constructions.thy Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Cardinals/Wellorder_Constructions.thy Fri Jul 22 11:00:43 2016 +0200
@@ -606,13 +606,13 @@
lemma not_isSucc_zero: "\<not> isSucc zero"
proof
- assume "isSucc zero"
- moreover
+ assume *: "isSucc zero"
then obtain i where "aboveS i \<noteq> {}" and 1: "minim (Field r) = succ i"
unfolding isSucc_def zero_def by auto
hence "succ i \<in> Field r" by auto
- ultimately show False by (metis REFL isSucc_def minim_least refl_on_domain
- subset_refl succ_in succ_not_in zero_def)
+ with * show False
+ by (metis REFL isSucc_def minim_least refl_on_domain
+ subset_refl succ_in succ_not_in zero_def)
qed
lemma isLim_zero[simp]: "isLim zero"
--- a/src/HOL/Conditionally_Complete_Lattices.thy Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Conditionally_Complete_Lattices.thy Fri Jul 22 11:00:43 2016 +0200
@@ -505,19 +505,23 @@
instance
proof
- fix x :: nat and X :: "nat set"
- { assume "x \<in> X" "bdd_below X" then show "Inf X \<le> x"
- by (simp add: Inf_nat_def Least_le) }
- { assume "X \<noteq> {}" "\<And>y. y \<in> X \<Longrightarrow> x \<le> y" then show "x \<le> Inf X"
- unfolding Inf_nat_def ex_in_conv[symmetric] by (rule LeastI2_ex) }
- { assume "x \<in> X" "bdd_above X" then show "x \<le> Sup X"
- by (simp add: Sup_nat_def bdd_above_nat) }
- { assume "X \<noteq> {}" "\<And>y. y \<in> X \<Longrightarrow> y \<le> x"
- moreover then have "bdd_above X"
+ fix x :: nat
+ fix X :: "nat set"
+ show "Inf X \<le> x" if "x \<in> X" "bdd_below X"
+ using that by (simp add: Inf_nat_def Least_le)
+ show "x \<le> Inf X" if "X \<noteq> {}" "\<And>y. y \<in> X \<Longrightarrow> x \<le> y"
+ using that unfolding Inf_nat_def ex_in_conv[symmetric] by (rule LeastI2_ex)
+ show "x \<le> Sup X" if "x \<in> X" "bdd_above X"
+ using that by (simp add: Sup_nat_def bdd_above_nat)
+ show "Sup X \<le> x" if "X \<noteq> {}" "\<And>y. y \<in> X \<Longrightarrow> y \<le> x"
+ proof -
+ from that have "bdd_above X"
by (auto simp: bdd_above_def)
- ultimately show "Sup X \<le> x"
- by (simp add: Sup_nat_def bdd_above_nat) }
+ with that show ?thesis
+ by (simp add: Sup_nat_def bdd_above_nat)
+ qed
qed
+
end
instantiation int :: conditionally_complete_linorder
--- a/src/HOL/Corec_Examples/LFilter.thy Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Corec_Examples/LFilter.thy Fri Jul 22 11:00:43 2016 +0200
@@ -30,7 +30,6 @@
from this(1,2) obtain a where "P (lhd ((ltl ^^ a) xs))"
by (atomize_elim, induct x xs rule: llist.set_induct)
(auto simp: funpow_Suc_right simp del: funpow.simps(2) intro: exI[of _ 0] exI[of _ "Suc i" for i])
- moreover
with \<open>\<not> P (lhd xs)\<close>
have "(LEAST n. P (lhd ((ltl ^^ n) xs))) = Suc (LEAST n. P (lhd ((ltl ^^ Suc n) xs)))"
by (intro Least_Suc) auto
--- a/src/HOL/Corec_Examples/Tests/Misc_Mono.thy Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Corec_Examples/Tests/Misc_Mono.thy Fri Jul 22 11:00:43 2016 +0200
@@ -382,7 +382,6 @@
from this(1,2) obtain a where "P (head ((tail ^^ a) xs))"
by (atomize_elim, induct xs x rule: llist_in.induct) (auto simp: funpow_Suc_right
simp del: funpow.simps(2) intro: exI[of _ 0] exI[of _ "Suc i" for i])
- moreover
with \<open>\<not> P (head xs)\<close>
have "(LEAST n. P (head ((tail ^^ n) xs))) = Suc (LEAST n. P (head ((tail ^^ Suc n) xs)))"
by (intro Least_Suc) auto
--- a/src/HOL/Filter.thy Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Filter.thy Fri Jul 22 11:00:43 2016 +0200
@@ -489,9 +489,9 @@
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"
shows "\<forall>\<^sub>F x in \<Sqinter>i\<in>I. F' i. T P x"
proof -
- from * obtain X where "finite X" "X \<subseteq> I" "\<forall>\<^sub>F x in \<Sqinter>i\<in>X. F i. P x"
+ from * obtain X where X: "finite X" "X \<subseteq> I" "\<forall>\<^sub>F x in \<Sqinter>i\<in>X. F i. P x"
unfolding eventually_INF[of _ _ I] by auto
- moreover then have "eventually (T P) (INFIMUM X F')"
+ then have "eventually (T P) (INFIMUM X F')"
apply (induction X arbitrary: P)
apply (auto simp: eventually_inf T2)
subgoal for x S P Q R
@@ -501,7 +501,7 @@
apply (auto intro: T1) []
done
done
- ultimately show "\<forall>\<^sub>F x in \<Sqinter>i\<in>I. F' i. T P x"
+ with X show "\<forall>\<^sub>F x in \<Sqinter>i\<in>I. F' i. T P x"
by (subst eventually_INF) auto
qed
@@ -798,9 +798,10 @@
shows "(\<forall>\<^sub>F (x, y) in A \<times>\<^sub>F B. P x) \<longleftrightarrow> (\<forall>\<^sub>F x in A. P x)"
unfolding eventually_prod_filter
proof safe
- 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"
- moreover with \<open>B \<noteq> bot\<close> obtain y where "Q y" by (auto dest: eventually_happens)
- ultimately show "eventually P A"
+ 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"
+ with \<open>B \<noteq> bot\<close> obtain y where "Q y" by (auto dest: eventually_happens)
+ with * show "eventually P A"
by (force elim: eventually_mono)
next
assume "eventually P A"
@@ -813,9 +814,10 @@
shows "(\<forall>\<^sub>F (x, y) in A \<times>\<^sub>F B. P y) \<longleftrightarrow> (\<forall>\<^sub>F y in B. P y)"
unfolding eventually_prod_filter
proof safe
- 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"
- moreover with \<open>A \<noteq> bot\<close> obtain x where "R x" by (auto dest: eventually_happens)
- ultimately show "eventually P B"
+ 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"
+ with \<open>A \<noteq> bot\<close> obtain x where "R x" by (auto dest: eventually_happens)
+ with * show "eventually P B"
by (force elim: eventually_mono)
next
assume "eventually P B"
@@ -827,35 +829,40 @@
fixes F :: "'a \<Rightarrow> 'b filter"
assumes *: "\<And>i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> \<exists>k\<in>I. F k \<le> F i \<sqinter> F j"
shows "(INF i:I. F i) = bot \<longleftrightarrow> (\<exists>i\<in>I. F i = bot)"
-proof cases
- assume "\<exists>i\<in>I. F i = bot"
- moreover then have "(INF i:I. F i) \<le> bot"
+proof (cases "\<exists>i\<in>I. F i = bot")
+ case True
+ then have "(INF i:I. F i) \<le> bot"
by (auto intro: INF_lower2)
- ultimately show ?thesis
+ with True show ?thesis
by (auto simp: bot_unique)
next
- assume **: "\<not> (\<exists>i\<in>I. F i = bot)"
+ case False
moreover have "(INF i:I. F i) \<noteq> bot"
- proof cases
- assume "I \<noteq> {}"
+ proof (cases "I = {}")
+ case True
+ then show ?thesis
+ by (auto simp add: filter_eq_iff)
+ next
+ case False': False
show ?thesis
proof (rule INF_filter_not_bot)
- fix J assume "finite J" "J \<subseteq> I"
+ fix J
+ assume "finite J" "J \<subseteq> I"
then have "\<exists>k\<in>I. F k \<le> (\<Sqinter>i\<in>J. F i)"
- proof (induction J)
- case empty then show ?case
+ proof (induct J)
+ case empty
+ then show ?case
using \<open>I \<noteq> {}\<close> by auto
next
case (insert i J)
- moreover then obtain k where "k \<in> I" "F k \<le> (\<Sqinter>i\<in>J. F i)" by auto
- moreover note *[of i k]
- ultimately show ?case
+ then obtain k where "k \<in> I" "F k \<le> (\<Sqinter>i\<in>J. F i)" by auto
+ with insert *[of i k] show ?case
by auto
qed
- with ** show "(\<Sqinter>i\<in>J. F i) \<noteq> \<bottom>"
+ with False show "(\<Sqinter>i\<in>J. F i) \<noteq> \<bottom>"
by (auto simp: bot_unique)
qed
- qed (auto simp add: filter_eq_iff)
+ qed
ultimately show ?thesis
by auto
qed
@@ -883,9 +890,9 @@
shows "A \<times>\<^sub>F B \<le> C \<times>\<^sub>F D \<longleftrightarrow> A \<le> C \<and> B \<le> D"
proof safe
assume *: "A \<times>\<^sub>F B \<le> C \<times>\<^sub>F D"
- moreover with assms have "A \<times>\<^sub>F B \<noteq> bot"
+ with assms have "A \<times>\<^sub>F B \<noteq> bot"
by (auto simp: bot_unique prod_filter_eq_bot)
- ultimately have "C \<times>\<^sub>F D \<noteq> bot"
+ with * have "C \<times>\<^sub>F D \<noteq> bot"
by (auto simp: bot_unique)
then have nCD: "C \<noteq> bot" "D \<noteq> bot"
by (auto simp: prod_filter_eq_bot)
--- a/src/HOL/Hilbert_Choice.thy Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Hilbert_Choice.thy Fri Jul 22 11:00:43 2016 +0200
@@ -317,14 +317,17 @@
proof -
define Sseq where "Sseq = rec_nat S (\<lambda>n T. T - {SOME e. e \<in> T})"
define pick where "pick n = (SOME e. e \<in> Sseq n)" for n
- { fix n have "Sseq n \<subseteq> S" "\<not> finite (Sseq n)" by (induct n) (auto simp add: Sseq_def inf) }
- moreover then have *: "\<And>n. pick n \<in> Sseq n"
+ have *: "Sseq n \<subseteq> S" "\<not> finite (Sseq n)" for n
+ by (induct n) (auto simp add: Sseq_def inf)
+ then have **: "\<And>n. pick n \<in> Sseq n"
unfolding pick_def by (subst (asm) finite.simps) (auto simp add: ex_in_conv intro: someI_ex)
- ultimately have "range pick \<subseteq> S" by auto
+ with * have "range pick \<subseteq> S" by auto
moreover
- { fix n m
- have "pick n \<notin> Sseq (n + Suc m)" by (induct m) (auto simp add: Sseq_def pick_def)
- with * have "pick n \<noteq> pick (n + Suc m)" by auto
+ {
+ fix n m
+ have "pick n \<notin> Sseq (n + Suc m)"
+ by (induct m) (auto simp add: Sseq_def pick_def)
+ with ** have "pick n \<noteq> pick (n + Suc m)" by auto
}
then have "inj pick" by (intro linorder_injI) (auto simp add: less_iff_Suc_add)
ultimately show ?thesis by blast
--- a/src/HOL/IMP/Compiler2.thy Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/IMP/Compiler2.thy Fri Jul 22 11:00:43 2016 +0200
@@ -366,9 +366,8 @@
rest: "P @ P' \<turnstile> (i', s'', stk'') \<rightarrow>^k (n, s', stk')"
by auto
from step `size P \<le> i`
- have "P' \<turnstile> (i - size P, s, stk) \<rightarrow> (i' - size P, s'', stk'')"
+ have *: "P' \<turnstile> (i - size P, s, stk) \<rightarrow> (i' - size P, s'', stk'')"
by (rule exec1_drop_left)
- moreover
then have "i' - size P \<in> succs P' 0"
by (fastforce dest!: succs_iexec1 simp: exec1_def simp del: iexec.simps)
with `exits P' \<subseteq> {0..}`
@@ -376,8 +375,7 @@
from rest this `exits P' \<subseteq> {0..}`
have "P' \<turnstile> (i' - size P, s'', stk'') \<rightarrow>^k (n - size P, s', stk')"
by (rule Suc.IH)
- ultimately
- show ?case by auto
+ with * show ?case by auto
qed
lemmas exec_n_drop_Cons =
--- a/src/HOL/IMP/Def_Init_Small.thy Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/IMP/Def_Init_Small.thy Fri Jul 22 11:00:43 2016 +0200
@@ -58,10 +58,9 @@
"(c,s) \<rightarrow> (c',s') \<Longrightarrow> D (dom s) c A \<Longrightarrow> EX A'. D (dom s') c' A' & A <= A'"
proof (induction arbitrary: A rule: small_step_induct)
case (While b c s)
- then obtain A' where "vars b \<subseteq> dom s" "A = dom s" "D (dom s) c A'" by blast
- moreover
+ then obtain A' where A': "vars b \<subseteq> dom s" "A = dom s" "D (dom s) c A'" by blast
then obtain A'' where "D A' c A''" by (metis D_incr D_mono)
- ultimately have "D (dom s) (IF b THEN c;; WHILE b DO c ELSE SKIP) (dom s)"
+ with A' have "D (dom s) (IF b THEN c;; WHILE b DO c ELSE SKIP) (dom s)"
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)
thus ?case by (metis D_incr `A = dom s`)
next
--- a/src/HOL/Inductive.thy Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Inductive.thy Fri Jul 22 11:00:43 2016 +0200
@@ -270,10 +270,10 @@
show "g (lfp (\<lambda>x. f (g x))) \<le> lfp (\<lambda>x. g (f x))"
proof (rule lfp_greatest)
fix u
- assume "g (f u) \<le> u"
- moreover then have "g (lfp (\<lambda>x. f (g x))) \<le> g (f u)"
+ assume u: "g (f u) \<le> u"
+ then have "g (lfp (\<lambda>x. f (g x))) \<le> g (f u)"
by (intro assms[THEN monoD] lfp_lowerbound)
- ultimately show "g (lfp (\<lambda>x. f (g x))) \<le> u"
+ with u show "g (lfp (\<lambda>x. f (g x))) \<le> u"
by auto
qed
qed
@@ -307,10 +307,11 @@
by (rule gfp_upperbound) (simp add: gfp_unfold[OF *, symmetric])
show "gfp (\<lambda>x. g (f x)) \<le> g (gfp (\<lambda>x. f (g x)))"
proof (rule gfp_least)
- fix u assume "u \<le> g (f u)"
- moreover then have "g (f u) \<le> g (gfp (\<lambda>x. f (g x)))"
+ fix u
+ assume u: "u \<le> g (f u)"
+ then have "g (f u) \<le> g (gfp (\<lambda>x. f (g x)))"
by (intro assms[THEN monoD] gfp_upperbound)
- ultimately show "u \<le> g (gfp (\<lambda>x. f (g x)))"
+ with u show "u \<le> g (gfp (\<lambda>x. f (g x)))"
by auto
qed
qed
--- a/src/HOL/Library/Bourbaki_Witt_Fixpoint.thy Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Library/Bourbaki_Witt_Fixpoint.thy Fri Jul 22 11:00:43 2016 +0200
@@ -7,7 +7,9 @@
section \<open>The Bourbaki-Witt tower construction for transfinite iteration\<close>
-theory Bourbaki_Witt_Fixpoint imports Main begin
+theory Bourbaki_Witt_Fixpoint
+ imports Main
+begin
lemma ChainsI [intro?]:
"(\<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"
@@ -131,10 +133,10 @@
with Sup.IH[OF z] \<open>y = a\<close> Sup.hyps(3)[OF z]
show ?thesis by(auto dest: iterates_above_ge intro: a)
next
- assume "y \<in> iterates_above (f a)"
- moreover with increasing[OF a] have "y \<in> Field leq"
+ assume *: "y \<in> iterates_above (f a)"
+ with increasing[OF a] have "y \<in> Field leq"
by(auto dest!: iterates_above_Field intro: FieldI2)
- ultimately show ?thesis using y by(auto)
+ with * show ?thesis using y by auto
qed
qed
thus ?thesis by simp
--- a/src/HOL/Library/Continuum_Not_Denumerable.thy Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Library/Continuum_Not_Denumerable.thy Fri Jul 22 11:00:43 2016 +0200
@@ -153,11 +153,11 @@
assumes "a < b" and "countable A"
shows "\<exists>x\<in>{a<..<b}. x \<notin> A"
proof -
- from \<open>countable A\<close> have "countable (A \<inter> {a<..<b})"
+ from \<open>countable A\<close> have *: "countable (A \<inter> {a<..<b})"
by auto
- moreover with \<open>a < b\<close> have "\<not> countable {a<..<b}"
+ with \<open>a < b\<close> have "\<not> countable {a<..<b}"
by (simp add: uncountable_open_interval)
- ultimately have "A \<inter> {a<..<b} \<noteq> {a<..<b}"
+ with * have "A \<inter> {a<..<b} \<noteq> {a<..<b}"
by auto
then have "A \<inter> {a<..<b} \<subset> {a<..<b}"
by (intro psubsetI) auto
--- a/src/HOL/Library/Discrete.thy Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Library/Discrete.thy Fri Jul 22 11:00:43 2016 +0200
@@ -28,11 +28,13 @@
assume "n > 0"
show "P n"
proof (cases "n = 1")
- case True with one show ?thesis by simp
+ case True
+ with one show ?thesis by simp
next
- case False with \<open>n > 0\<close> have "n \<ge> 2" by auto
- moreover with * have "P (n div 2)" .
- ultimately show ?thesis by (rule double)
+ case False
+ with \<open>n > 0\<close> have "n \<ge> 2" by auto
+ with * have "P (n div 2)" .
+ with \<open>n \<ge> 2\<close> show ?thesis by (rule double)
qed
qed
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy Fri Jul 22 11:00:43 2016 +0200
@@ -1067,11 +1067,11 @@
fix x y :: ereal assume xy: "0 \<le> x" "0 \<le> y" "x < y"
moreover
from ereal_dense3[OF \<open>x < y\<close>]
- obtain r where "x < ereal (real_of_rat r)" "ereal (real_of_rat r) < y"
+ obtain r where r: "x < ereal (real_of_rat r)" "ereal (real_of_rat r) < y"
by auto
- moreover then have "0 \<le> r"
+ then have "0 \<le> r"
using le_less_trans[OF \<open>0 \<le> x\<close> \<open>x < ereal (real_of_rat r)\<close>] by auto
- ultimately show "\<exists>r. x < (sup 0 \<circ> ereal) (real_of_rat r) \<and> (sup 0 \<circ> ereal) (real_of_rat r) < y"
+ with r show "\<exists>r. x < (sup 0 \<circ> ereal) (real_of_rat r) \<and> (sup 0 \<circ> ereal) (real_of_rat r) < y"
by (intro exI[of _ r]) (auto simp: max_absorb2)
qed
@@ -1172,11 +1172,11 @@
from ennreal_Ex_less_of_nat[OF r] guess n .. note n = this
have "\<not> (X \<subseteq> enat ` {.. n})"
using \<open>infinite X\<close> by (auto dest: finite_subset)
- then obtain x where "x \<in> X" "x \<notin> enat ` {..n}"
+ then obtain x where x: "x \<in> X" "x \<notin> enat ` {..n}"
by blast
- moreover then have "of_nat n \<le> x"
+ then have "of_nat n \<le> x"
by (cases x) (auto simp: of_nat_eq_enat)
- ultimately show ?thesis
+ with x show ?thesis
by (auto intro!: bexI[of _ x] less_le_trans[OF n])
qed
then have "(SUP x : X. ennreal_of_enat x) = top"
--- a/src/HOL/Library/Extended_Real.thy Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Library/Extended_Real.thy Fri Jul 22 11:00:43 2016 +0200
@@ -2036,14 +2036,15 @@
lemma SUP_ereal_add_left:
assumes "I \<noteq> {}" "c \<noteq> -\<infinity>"
shows "(SUP i:I. f i + c :: ereal) = (SUP i:I. f i) + c"
-proof cases
- assume "(SUP i:I. f i) = - \<infinity>"
- moreover then have "\<And>i. i \<in> I \<Longrightarrow> f i = -\<infinity>"
+proof (cases "(SUP i:I. f i) = - \<infinity>")
+ case True
+ then have "\<And>i. i \<in> I \<Longrightarrow> f i = -\<infinity>"
unfolding Sup_eq_MInfty by auto
- ultimately show ?thesis
+ with True show ?thesis
by (cases c) (auto simp: \<open>I \<noteq> {}\<close>)
next
- assume "(SUP i:I. f i) \<noteq> - \<infinity>" then show ?thesis
+ case False
+ then show ?thesis
by (subst continuous_at_Sup_mono[where f="\<lambda>x. x + c"])
(auto simp: continuous_at_imp_continuous_at_within continuous_at mono_def ereal_add_mono \<open>I \<noteq> {}\<close> \<open>c \<noteq> -\<infinity>\<close>)
qed
@@ -2158,14 +2159,15 @@
assumes "I \<noteq> {}"
assumes f: "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i" and c: "0 \<le> c"
shows "(SUP i:I. c * f i) = c * (SUP i:I. f i)"
-proof cases
- assume "(SUP i: I. f i) = 0"
- moreover then have "\<And>i. i \<in> I \<Longrightarrow> f i = 0"
+proof (cases "(SUP i: I. f i) = 0")
+ case True
+ then have "\<And>i. i \<in> I \<Longrightarrow> f i = 0"
by (metis SUP_upper f antisym)
- ultimately show ?thesis
+ with True show ?thesis
by simp
next
- assume "(SUP i:I. f i) \<noteq> 0" then show ?thesis
+ case False
+ then show ?thesis
by (subst continuous_at_Sup_mono[where f="\<lambda>x. c * x"])
(auto simp: mono_def continuous_at continuous_at_imp_continuous_at_within \<open>I \<noteq> {}\<close>
intro!: ereal_mult_left_mono c)
--- a/src/HOL/Library/Function_Growth.thy Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Library/Function_Growth.thy Fri Jul 22 11:00:43 2016 +0200
@@ -36,8 +36,8 @@
shows "a ^ (m - n) = (a ^ m) div (a ^ n)"
proof -
define q where "q = m - n"
- moreover with assms have "m = q + n" by (simp add: q_def)
- ultimately show ?thesis using \<open>a \<noteq> 0\<close> by (simp add: power_add)
+ with assms have "m = q + n" by (simp add: q_def)
+ with q_def show ?thesis using \<open>a \<noteq> 0\<close> by (simp add: power_add)
qed
--- a/src/HOL/Library/More_List.thy Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Library/More_List.thy Fri Jul 22 11:00:43 2016 +0200
@@ -317,10 +317,10 @@
then show ?Q
proof (rule nth_equalityI [rule_format])
fix n
- assume "n < length ?xs"
- moreover with len have "n < length ?ys"
+ assume n: "n < length ?xs"
+ with len have "n < length ?ys"
by simp
- ultimately have xs: "nth_default dflt ?xs n = ?xs ! n"
+ with n have xs: "nth_default dflt ?xs n = ?xs ! n"
and ys: "nth_default dflt ?ys n = ?ys ! n"
by (simp_all only: nth_default_nth)
with eq show "?xs ! n = ?ys ! n"
--- a/src/HOL/Library/Multiset.thy Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Library/Multiset.thy Fri Jul 22 11:00:43 2016 +0200
@@ -2410,11 +2410,11 @@
moreover have "(a, b) \<in> (r \<inter> D \<times> D)\<inverse>"
using \<open>(b, a) \<in> r\<close> using \<open>b \<in># B\<close> and \<open>a \<in># B\<close>
by (auto simp: D_def)
- ultimately obtain x where "x \<in># X" and "(a, x) \<in> r"
+ ultimately obtain x where x: "x \<in># X" "(a, x) \<in> r"
using "1.IH" by blast
- moreover then have "(b, x) \<in> r"
+ then have "(b, x) \<in> r"
using \<open>trans r\<close> and \<open>(b, a) \<in> r\<close> by (auto dest: transD)
- ultimately show ?thesis by blast
+ with x show ?thesis by blast
qed blast
qed }
note B_less = this
--- a/src/HOL/Library/Order_Continuity.thy Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Library/Order_Continuity.thy Fri Jul 22 11:00:43 2016 +0200
@@ -72,10 +72,11 @@
shows "sup_continuous (\<lambda>x. f (g x))"
unfolding sup_continuous_def
proof safe
- fix M :: "nat \<Rightarrow> 'c" assume "mono M"
- moreover then have "mono (\<lambda>i. g (M i))"
+ fix M :: "nat \<Rightarrow> 'c"
+ assume M: "mono M"
+ then have "mono (\<lambda>i. g (M i))"
using sup_continuous_mono[OF g] by (auto simp: mono_def)
- ultimately show "f (g (SUPREMUM UNIV M)) = (SUP i. f (g (M i)))"
+ with M show "f (g (SUPREMUM UNIV M)) = (SUP i. f (g (M i)))"
by (auto simp: sup_continuous_def g[THEN sup_continuousD] f[THEN sup_continuousD])
qed
@@ -269,10 +270,11 @@
shows "inf_continuous (\<lambda>x. f (g x))"
unfolding inf_continuous_def
proof safe
- fix M :: "nat \<Rightarrow> 'c" assume "antimono M"
- moreover then have "antimono (\<lambda>i. g (M i))"
+ fix M :: "nat \<Rightarrow> 'c"
+ assume M: "antimono M"
+ then have "antimono (\<lambda>i. g (M i))"
using inf_continuous_mono[OF g] by (auto simp: mono_def antimono_def)
- ultimately show "f (g (INFIMUM UNIV M)) = (INF i. f (g (M i)))"
+ with M show "f (g (INFIMUM UNIV M)) = (INF i. f (g (M i)))"
by (auto simp: inf_continuous_def g[THEN inf_continuousD] f[THEN inf_continuousD])
qed
--- a/src/HOL/Library/Perm.thy Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Library/Perm.thy Fri Jul 22 11:00:43 2016 +0200
@@ -78,15 +78,15 @@
assume "card (affected f) = 1"
then obtain a where *: "affected f = {a}"
by (rule card_1_singletonE)
- then have "f \<langle>$\<rangle> a \<noteq> a"
+ then have **: "f \<langle>$\<rangle> a \<noteq> a"
by (simp add: in_affected [symmetric])
- moreover with * have "f \<langle>$\<rangle> a \<notin> affected f"
+ with * have "f \<langle>$\<rangle> a \<notin> affected f"
by simp
then have "f \<langle>$\<rangle> (f \<langle>$\<rangle> a) = f \<langle>$\<rangle> a"
by (simp add: in_affected)
then have "inv (apply f) (f \<langle>$\<rangle> (f \<langle>$\<rangle> a)) = inv (apply f) (f \<langle>$\<rangle> a)"
by simp
- ultimately show False by simp
+ with ** show False by simp
qed
@@ -203,15 +203,18 @@
using assms by auto
then show "(g * f) \<langle>$\<rangle> a = (f * g) \<langle>$\<rangle> a"
proof cases
- case 1 moreover with * have "f \<langle>$\<rangle> a \<notin> affected g"
+ case 1
+ with * have "f \<langle>$\<rangle> a \<notin> affected g"
by auto
- ultimately show ?thesis by (simp add: in_affected apply_times)
+ with 1 show ?thesis by (simp add: in_affected apply_times)
next
- case 2 moreover with * have "g \<langle>$\<rangle> a \<notin> affected f"
+ case 2
+ with * have "g \<langle>$\<rangle> a \<notin> affected f"
by auto
- ultimately show ?thesis by (simp add: in_affected apply_times)
+ with 2 show ?thesis by (simp add: in_affected apply_times)
next
- case 3 then show ?thesis by (simp add: in_affected apply_times)
+ case 3
+ then show ?thesis by (simp add: in_affected apply_times)
qed
qed
--- a/src/HOL/List.thy Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/List.thy Fri Jul 22 11:00:43 2016 +0200
@@ -3542,10 +3542,9 @@
have "length ys = card (f ` {0 ..< size [x]})"
using f_img by auto
- then have "length ys = 1" by auto
- moreover
+ then have *: "length ys = 1" by auto
then have "f 0 = 0" using f_img by auto
- ultimately show ?case using f_nth by (cases ys) auto
+ with * show ?case using f_nth by (cases ys) auto
next
case (3 x1 x2 xs)
from "3.prems" obtain f where f_mono: "mono f"
@@ -5499,10 +5498,10 @@
next
let ?k = "length abs"
case eq
- hence "abs = bcs" "b = b'" using bs bs' by auto
- moreover hence "(a, c') \<in> r"
+ hence *: "abs = bcs" "b = b'" using bs bs' by auto
+ hence "(a, c') \<in> r"
using abr b'c'r assms unfolding trans_def by blast
- ultimately show ?thesis using n n' unfolding lexn_conv as bs cs by auto
+ with * show ?thesis using n n' unfolding lexn_conv as bs cs by auto
qed
qed
@@ -5840,8 +5839,8 @@
(is "?lhs \<longleftrightarrow> ?rhs")
proof
assume ?lhs
- moreover hence "\<not> lexordp_eq ys xs" by induct simp_all
- ultimately show ?rhs by(simp add: lexordp_into_lexordp_eq)
+ hence "\<not> lexordp_eq ys xs" by induct simp_all
+ with \<open>?lhs\<close> show ?rhs by (simp add: lexordp_into_lexordp_eq)
next
assume ?rhs
hence "lexordp_eq xs ys" "\<not> lexordp_eq ys xs" by simp_all
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Fri Jul 22 11:00:43 2016 +0200
@@ -71,9 +71,9 @@
proof (induct s rule: finite_ne_induct)
case (insert b s)
assume *: "\<forall>x\<in>insert b s. \<forall>y\<in>insert b s. x \<le> y \<or> y \<le> x"
- 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"
+ 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"
using insert by auto
- 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"
+ 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"
using *[rule_format, of b u] *[rule_format, of b l] by (metis insert_iff order.trans)+
qed auto
--- a/src/HOL/Multivariate_Analysis/Conformal_Mappings.thy Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Conformal_Mappings.thy Fri Jul 22 11:00:43 2016 +0200
@@ -1411,7 +1411,7 @@
show no_df0: "norm(deriv f 0) \<le> 1"
by (simp add: \<open>\<And>z. cmod z < 1 \<Longrightarrow> cmod (h z) \<le> 1\<close> df0)
show "?Q" if "?P"
- using that
+ using that
proof
assume "\<exists>z. cmod z < 1 \<and> z \<noteq> 0 \<and> cmod (f z) = cmod z"
then obtain \<gamma> where \<gamma>: "cmod \<gamma> < 1" "\<gamma> \<noteq> 0" "cmod (f \<gamma>) = cmod \<gamma>" by blast
@@ -1424,9 +1424,9 @@
by (metis add_diff_cancel_left' diff_diff_eq2 le_less_trans noh_le norm_triangle_ineq4)
ultimately obtain c where c: "\<And>z. norm z < 1 \<Longrightarrow> h z = c"
using Schwarz2 [OF holh, of "1 - norm \<gamma>" \<gamma>, unfolded constant_on_def] \<gamma> by auto
- moreover then have "norm c = 1"
+ then have "norm c = 1"
using \<gamma> by force
- ultimately show ?thesis
+ with c show ?thesis
using fz_eq by auto
next
assume [simp]: "cmod (deriv f 0) = 1"
--- a/src/HOL/Multivariate_Analysis/Integration.thy Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Fri Jul 22 11:00:43 2016 +0200
@@ -10168,14 +10168,14 @@
then have x: "{integral s (f k) |k. True} = range x"
by auto
- have "g integrable_on s \<and> (\<lambda>k. integral s (f k)) \<longlonglongrightarrow> integral s g"
+ have *: "g integrable_on s \<and> (\<lambda>k. integral s (f k)) \<longlonglongrightarrow> integral s g"
proof (intro monotone_convergence_increasing allI ballI assms)
show "bounded {integral s (f k) |k. True}"
unfolding x by (rule convergent_imp_bounded) fact
qed (auto intro: f)
- moreover then have "integral s g = x'"
+ then have "integral s g = x'"
by (intro LIMSEQ_unique[OF _ \<open>x \<longlonglongrightarrow> x'\<close>]) (simp add: x_eq)
- ultimately show ?thesis
+ with * show ?thesis
by (simp add: has_integral_integral)
qed
@@ -11559,18 +11559,16 @@
with \<open>open W\<close>
have "\<exists>X0 Y. open X0 \<and> open Y \<and> x0 \<in> X0 \<and> y \<in> Y \<and> X0 \<times> Y \<subseteq> W"
by (rule open_prod_elim) blast
- } then obtain X0 Y where
- "\<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"
+ }
+ then obtain X0 Y where
+ *: "\<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"
by metis
- moreover
- then have "\<forall>t\<in>Y ` K. open t" "K \<subseteq> \<Union>(Y ` K)" by auto
- with \<open>compact K\<close> obtain CC where "CC \<subseteq> Y ` K" "finite CC" "K \<subseteq> \<Union>CC"
+ from * have "\<forall>t\<in>Y ` K. open t" "K \<subseteq> \<Union>(Y ` K)" by auto
+ with \<open>compact K\<close> obtain CC where CC: "CC \<subseteq> Y ` K" "finite CC" "K \<subseteq> \<Union>CC"
by (rule compactE)
- moreover
- then obtain c where c:
- "\<And>C. C \<in> CC \<Longrightarrow> c C \<in> K \<and> C = Y (c C)"
+ then obtain c where c: "\<And>C. C \<in> CC \<Longrightarrow> c C \<in> K \<and> C = Y (c C)"
by (force intro!: choice)
- ultimately show ?thesis
+ with * CC show ?thesis
by (force intro!: exI[where x="\<Inter>C\<in>CC. X0 (c C)"])
qed
--- a/src/HOL/Multivariate_Analysis/Path_Connected.thy Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy Fri Jul 22 11:00:43 2016 +0200
@@ -3057,11 +3057,11 @@
then have ftendsw: "((\<lambda>n. f (z n)) \<circ> K) \<longlonglongrightarrow> w"
by (metis LIMSEQ_subseq_LIMSEQ fun.map_cong0 fz tendsw)
have zKs: "\<And>n. (z o K) n \<in> S" by (simp add: zs)
- have "f \<circ> z = \<xi>" "(\<lambda>n. f (z n)) = \<xi>"
+ have fz: "f \<circ> z = \<xi>" "(\<lambda>n. f (z n)) = \<xi>"
using fz by auto
- moreover then have "(\<xi> \<circ> K) \<longlonglongrightarrow> f y"
+ then have "(\<xi> \<circ> K) \<longlonglongrightarrow> f y"
by (metis (no_types) Klim zKs y contf comp_assoc continuous_on_closure_sequentially)
- ultimately have wy: "w = f y" using fz LIMSEQ_unique ftendsw by auto
+ with fz have wy: "w = f y" using fz LIMSEQ_unique ftendsw by auto
have rle: "r \<le> norm (f y - f a)"
apply (rule le_no)
using w wy oint
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Jul 22 11:00:43 2016 +0200
@@ -4343,10 +4343,11 @@
have "F \<noteq> bot"
unfolding F_def
proof (rule INF_filter_not_bot)
- fix X assume "X \<subseteq> insert U A" "finite X"
- moreover with A(2)[THEN spec, of "X - {U}"] have "U \<inter> \<Inter>(X - {U}) \<noteq> {}"
+ fix X
+ assume X: "X \<subseteq> insert U A" "finite X"
+ with A(2)[THEN spec, of "X - {U}"] have "U \<inter> \<Inter>(X - {U}) \<noteq> {}"
by auto
- ultimately show "(INF a:X. principal a) \<noteq> bot"
+ with X show "(INF a:X. principal a) \<noteq> bot"
by (auto simp add: INF_principal_finite principal_eq_bot_iff)
qed
moreover
@@ -6601,13 +6602,12 @@
then obtain xs where xs: "xs \<longlonglongrightarrow> x" "\<And>n. xs n \<in> X"
by (auto simp: closure_sequential)
from continuous_on_tendsto_compose[OF cont_h xs(1)] xs(2) Y
- have "(\<lambda>x. f (xs x)) \<longlonglongrightarrow> h x"
+ have hx: "(\<lambda>x. f (xs x)) \<longlonglongrightarrow> h x"
by (auto simp: set_mp extension)
- moreover
then have "(\<lambda>x. f (xs x)) \<longlonglongrightarrow> y x"
using \<open>x \<notin> X\<close> not_eventuallyD xs(2)
by (force intro!: filterlim_compose[OF y[OF \<open>x \<in> closure X\<close>]] simp: filterlim_at xs)
- ultimately have "h x = y x" by (rule LIMSEQ_unique)
+ with hx have "h x = y x" by (rule LIMSEQ_unique)
} then
have "h x = ?g x"
using extension by auto
--- a/src/HOL/Probability/Distributions.thy Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Probability/Distributions.thy Fri Jul 22 11:00:43 2016 +0200
@@ -164,8 +164,8 @@
lemma nn_integral_erlang_density:
assumes [arith]: "0 < l"
shows "(\<integral>\<^sup>+ x. ennreal (erlang_density k l x) * indicator {.. a} x \<partial>lborel) = erlang_CDF k l a"
-proof cases
- assume [arith]: "0 \<le> a"
+proof (cases "0 \<le> a")
+ case [arith]: True
have eq: "\<And>x. indicator {0..a} (x / l) = indicator {0..a*l} x"
by (simp add: field_simps split: split_indicator)
have "(\<integral>\<^sup>+x. ennreal (erlang_density k l x) * indicator {.. a} x \<partial>lborel) =
@@ -182,10 +182,10 @@
by (auto simp: erlang_CDF_def)
finally show ?thesis .
next
- assume "\<not> 0 \<le> a"
- 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))"
+ case False
+ then have "(\<integral>\<^sup>+ x. ennreal (erlang_density k l x) * indicator {.. a} x \<partial>lborel) = (\<integral>\<^sup>+x. 0 \<partial>(lborel::real measure))"
by (intro nn_integral_cong) (auto simp: erlang_density_def)
- ultimately show ?thesis
+ with False show ?thesis
by (simp add: erlang_CDF_def)
qed
--- a/src/HOL/Probability/Finite_Product_Measure.thy Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Probability/Finite_Product_Measure.thy Fri Jul 22 11:00:43 2016 +0200
@@ -1133,10 +1133,10 @@
lemma (in product_sigma_finite) distr_component:
"distr (M i) (Pi\<^sub>M {i} M) (\<lambda>x. \<lambda>i\<in>{i}. x) = Pi\<^sub>M {i} M" (is "?D = ?P")
proof (intro PiM_eqI)
- fix A assume "\<And>ia. ia \<in> {i} \<Longrightarrow> A ia \<in> sets (M ia)"
- moreover then have "(\<lambda>x. \<lambda>i\<in>{i}. x) -` Pi\<^sub>E {i} A \<inter> space (M i) = A i"
+ fix A assume A: "\<And>ia. ia \<in> {i} \<Longrightarrow> A ia \<in> sets (M ia)"
+ then have "(\<lambda>x. \<lambda>i\<in>{i}. x) -` Pi\<^sub>E {i} A \<inter> space (M i) = A i"
by (auto dest: sets.sets_into_space)
- 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))"
+ 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))"
by (subst emeasure_distr) (auto intro!: sets_PiM_I_finite measurable_restrict)
qed simp_all
--- a/src/HOL/Probability/Giry_Monad.thy Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Probability/Giry_Monad.thy Fri Jul 22 11:00:43 2016 +0200
@@ -272,28 +272,28 @@
ultimately show ?case by simp
next
case (set B)
- moreover then have "(\<lambda>M'. \<integral>\<^sup>+M''. indicator B M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. emeasure M' B) \<in> ?B"
+ then have "(\<lambda>M'. \<integral>\<^sup>+M''. indicator B M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. emeasure M' B) \<in> ?B"
by (intro measurable_cong nn_integral_indicator) (simp add: space_subprob_algebra)
- ultimately show ?case
+ with set show ?case
by (simp add: measurable_emeasure_subprob_algebra)
next
case (mult f c)
- 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"
+ 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"
by (intro measurable_cong nn_integral_cmult) (auto simp add: space_subprob_algebra)
- ultimately show ?case
+ with mult show ?case
by simp
next
case (add f g)
- 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"
+ 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"
by (intro measurable_cong nn_integral_add) (auto simp add: space_subprob_algebra)
- ultimately show ?case
+ with add show ?case
by (simp add: ac_simps)
next
case (seq F)
- 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"
+ 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"
unfolding SUP_apply
by (intro measurable_cong nn_integral_monotone_convergence_SUP) (auto simp add: space_subprob_algebra)
- ultimately show ?case
+ with seq show ?case
by (simp add: ac_simps)
qed
@@ -793,10 +793,10 @@
by simp
next
case (set A)
- moreover with M have "(\<integral>\<^sup>+ M'. integral\<^sup>N M' (indicator A) \<partial>M) = (\<integral>\<^sup>+ M'. emeasure M' A \<partial>M)"
+ with M have "(\<integral>\<^sup>+ M'. integral\<^sup>N M' (indicator A) \<partial>M) = (\<integral>\<^sup>+ M'. emeasure M' A \<partial>M)"
by (intro nn_integral_cong nn_integral_indicator)
(auto simp: space_subprob_algebra dest!: sets_eq_imp_space_eq)
- ultimately show ?case
+ with set show ?case
using M by (simp add: emeasure_join)
next
case (mult f c)
--- a/src/HOL/Probability/Infinite_Product_Measure.thy Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy Fri Jul 22 11:00:43 2016 +0200
@@ -29,14 +29,18 @@
note * = this
have "emeasure (PiM I M) (emb I J (PiE J X)) = (\<Prod>i\<in>J. M i (X i))"
- proof cases
- assume "\<not> (J \<noteq> {} \<or> I = {})"
- then obtain i where "J = {}" "i \<in> I" by auto
- moreover then have "emb I {} {\<lambda>x. undefined} = emb I {i} (\<Pi>\<^sub>E i\<in>{i}. space (M i))"
+ proof (cases "J \<noteq> {} \<or> I = {}")
+ case False
+ then obtain i where i: "J = {}" "i \<in> I" by auto
+ then have "emb I {} {\<lambda>x. undefined} = emb I {i} (\<Pi>\<^sub>E i\<in>{i}. space (M i))"
by (auto simp: space_PiM prod_emb_def)
- ultimately show ?thesis
+ with i show ?thesis
by (simp add: * M.emeasure_space_1)
- qed (simp add: *[OF _ assms X])
+ next
+ case True
+ then show ?thesis
+ by (simp add: *[OF _ assms X])
+ qed
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))"
by (subst emeasure_distr_restrict[OF _ refl]) (auto intro!: sets_PiM_I_finite X)
qed (insert assms, auto)
--- a/src/HOL/Probability/Lebesgue_Integral_Substitution.thy Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Probability/Lebesgue_Integral_Substitution.thy Fri Jul 22 11:00:43 2016 +0200
@@ -323,9 +323,9 @@
and "(LBINT x. f x * indicator {g a..g b} x) = (LBINT x. f (g x) * g' x * indicator {a..b} x)"
proof-
from derivg have contg: "continuous_on {a..b} g" by (rule has_real_derivative_imp_continuous_on)
- from this and contg' have Mg: "set_borel_measurable borel {a..b} g" and
- Mg': "set_borel_measurable borel {a..b} g'"
- by (simp_all only: set_measurable_continuous_on_ivl)
+ with contg' have Mg: "set_borel_measurable borel {a..b} g"
+ and Mg': "set_borel_measurable borel {a..b} g'"
+ by (simp_all only: set_measurable_continuous_on_ivl)
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"
by (rule deriv_nonneg_imp_mono) simp_all
@@ -341,18 +341,18 @@
enn2real (\<integral>\<^sup>+ x. ennreal (f x) * indicator {g a..g b} x \<partial>lborel) -
enn2real (\<integral>\<^sup>+ x. ennreal (- (f x)) * indicator {g a..g b} x \<partial>lborel)" using integrable
by (subst real_lebesgue_integral_def) (simp_all add: nn_integral_set_ennreal mult.commute)
- also have "(\<integral>\<^sup>+x. ennreal (f x) * indicator {g a..g b} x \<partial>lborel) =
- (\<integral>\<^sup>+x. ennreal (f x * indicator {g a..g b} x) \<partial>lborel)"
+ also have *: "(\<integral>\<^sup>+x. ennreal (f x) * indicator {g a..g b} x \<partial>lborel) =
+ (\<integral>\<^sup>+x. ennreal (f x * indicator {g a..g b} x) \<partial>lborel)"
by (intro nn_integral_cong) (simp split: split_indicator)
- also with M1 have A: "(\<integral>\<^sup>+ x. ennreal (f x * indicator {g a..g b} x) \<partial>lborel) =
+ also from M1 * have A: "(\<integral>\<^sup>+ x. ennreal (f x * indicator {g a..g b} x) \<partial>lborel) =
(\<integral>\<^sup>+ x. ennreal (f (g x) * g' x * indicator {a..b} x) \<partial>lborel)"
by (subst nn_integral_substitution[OF _ derivg contg' derivg_nonneg \<open>a \<le> b\<close>])
(auto simp: nn_integral_set_ennreal mult.commute)
- also have "(\<integral>\<^sup>+ x. ennreal (- (f x)) * indicator {g a..g b} x \<partial>lborel) =
- (\<integral>\<^sup>+ x. ennreal (- (f x) * indicator {g a..g b} x) \<partial>lborel)"
+ also have **: "(\<integral>\<^sup>+ x. ennreal (- (f x)) * indicator {g a..g b} x \<partial>lborel) =
+ (\<integral>\<^sup>+ x. ennreal (- (f x) * indicator {g a..g b} x) \<partial>lborel)"
by (intro nn_integral_cong) (simp split: split_indicator)
- also with M2 have B: "(\<integral>\<^sup>+ x. ennreal (- (f x) * indicator {g a..g b} x) \<partial>lborel) =
- (\<integral>\<^sup>+ x. ennreal (- (f (g x)) * g' x * indicator {a..b} x) \<partial>lborel)"
+ also from M2 ** have B: "(\<integral>\<^sup>+ x. ennreal (- (f x) * indicator {g a..g b} x) \<partial>lborel) =
+ (\<integral>\<^sup>+ x. ennreal (- (f (g x)) * g' x * indicator {a..b} x) \<partial>lborel)"
by (subst nn_integral_substitution[OF _ derivg contg' derivg_nonneg \<open>a \<le> b\<close>])
(auto simp: nn_integral_set_ennreal mult.commute)
--- a/src/HOL/Probability/Lebesgue_Measure.thy Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Probability/Lebesgue_Measure.thy Fri Jul 22 11:00:43 2016 +0200
@@ -75,9 +75,9 @@
fix i assume "i \<in> S - {m}"
then have i: "i \<in> S" "i \<noteq> m" by auto
{ assume i': "l i < r i" "l i < r m"
- moreover with \<open>finite S\<close> i m have "l m \<le> l i"
+ with \<open>finite S\<close> i m have "l m \<le> l i"
by auto
- ultimately have "{l i <.. r i} \<inter> {l m <.. r m} \<noteq> {}"
+ with i' have "{l i <.. r i} \<inter> {l m <.. r m} \<noteq> {}"
by auto
then have False
using disjoint_family_onD[OF disj, of i m] i by auto }
@@ -852,9 +852,9 @@
shows "(f has_integral r) UNIV"
using f proof (induct f arbitrary: r rule: borel_measurable_induct_real)
case (set A)
- moreover then have "((\<lambda>x. 1) has_integral measure lborel A) A"
+ then have "((\<lambda>x. 1) has_integral measure lborel A) A"
by (intro has_integral_measure_lborel) (auto simp: ennreal_indicator)
- ultimately show ?case
+ with set show ?case
by (simp add: ennreal_indicator measure_def) (simp add: indicator_def)
next
case (mult g c)
@@ -868,13 +868,12 @@
by (auto intro!: has_integral_cmult_real)
next
case (add g h)
- moreover
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)"
by (simp add: nn_integral_add)
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"
by (cases "\<integral>\<^sup>+ x. h x \<partial>lborel" "\<integral>\<^sup>+ x. g x \<partial>lborel" rule: ennreal2_cases)
(auto simp: add_top nn_integral_add top_add ennreal_plus[symmetric] simp del: ennreal_plus)
- ultimately show ?case
+ with add show ?case
by (auto intro!: has_integral_add)
next
case (seq U)
@@ -1020,8 +1019,8 @@
fixes A :: "'a::euclidean_space set"
assumes A[measurable]: "A \<in> sets borel" and [simp]: "0 \<le> r"
shows "((\<lambda>x. 1) has_integral r) A \<longleftrightarrow> emeasure lborel A = ennreal r"
-proof cases
- assume emeasure_A: "emeasure lborel A = \<infinity>"
+proof (cases "emeasure lborel A = \<infinity>")
+ case emeasure_A: True
have "\<not> (\<lambda>x. 1::real) integrable_on A"
proof
assume int: "(\<lambda>x. 1::real) integrable_on A"
@@ -1035,10 +1034,10 @@
with emeasure_A show ?thesis
by auto
next
- assume "emeasure lborel A \<noteq> \<infinity>"
- moreover then have "((\<lambda>x. 1) has_integral measure lborel A) A"
+ case False
+ then have "((\<lambda>x. 1) has_integral measure lborel A) A"
by (simp add: has_integral_measure_lborel less_top)
- ultimately show ?thesis
+ with False show ?thesis
by (auto simp: emeasure_eq_ennreal_measure has_integral_unique)
qed
--- a/src/HOL/Probability/Levy.thy Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Probability/Levy.thy Fri Jul 22 11:00:43 2016 +0200
@@ -391,23 +391,22 @@
continuous_intros ballI M'.isCont_char continuous_intros)
have "cmod (CLBINT t:{-d/2..d/2}. 1 - char M' t) \<le> LBINT t:{-d/2..d/2}. cmod (1 - char M' t)"
using integral_norm_bound[OF 2] by simp
- also have "\<dots> \<le> LBINT t:{-d/2..d/2}. \<epsilon> / 4"
+ also have 4: "\<dots> \<le> LBINT t:{-d/2..d/2}. \<epsilon> / 4"
apply (rule integral_mono [OF 3])
- apply (simp add: emeasure_lborel_Icc_eq)
- apply (case_tac "x \<in> {-d/2..d/2}", auto)
+ apply (simp add: emeasure_lborel_Icc_eq)
+ apply (case_tac "x \<in> {-d/2..d/2}")
+ apply auto
apply (subst norm_minus_commute)
apply (rule less_imp_le)
apply (rule d1 [simplified])
- using d0 by auto
- also with d0 have "\<dots> = d * \<epsilon> / 4"
+ using d0 apply auto
+ done
+ also from d0 4 have "\<dots> = d * \<epsilon> / 4"
by simp
finally have bound: "cmod (CLBINT t:{-d/2..d/2}. 1 - char M' t) \<le> d * \<epsilon> / 4" .
- { fix n x
- have "cmod (1 - char (M n) x) \<le> 2"
- by (rule order_trans [OF norm_triangle_ineq4], auto simp add: Mn.cmod_char_le_1)
- } note bd1 = this
- 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)"
- using bd1
+ have "cmod (1 - char (M n) x) \<le> 2" for n x
+ by (rule order_trans [OF norm_triangle_ineq4], auto simp add: Mn.cmod_char_le_1)
+ 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)"
apply (intro integral_dominated_convergence[where w="\<lambda>x. indicator {-d/2..d/2} x *\<^sub>R 2"])
apply (auto intro!: char_conv tendsto_intros
simp: emeasure_lborel_Icc_eq
--- a/src/HOL/Probability/Measure_Space.thy Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Probability/Measure_Space.thy Fri Jul 22 11:00:43 2016 +0200
@@ -1862,7 +1862,7 @@
using f unfolding Pi_def bij_betw_def by auto
fix X assume "X \<in> sets (distr (count_space A) (count_space B) f)"
then have X: "X \<in> sets (count_space B)" by auto
- moreover then have "f -` X \<inter> A = the_inv_into A f ` X"
+ moreover from X have "f -` X \<inter> A = the_inv_into A f ` X"
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])
moreover have "inj_on (the_inv_into A f) B"
using X f by (auto simp: bij_betw_def inj_on_the_inv_into)
@@ -1932,8 +1932,8 @@
lemma emeasure_restrict_space:
assumes "\<Omega> \<inter> space M \<in> sets M" "A \<subseteq> \<Omega>"
shows "emeasure (restrict_space M \<Omega>) A = emeasure M A"
-proof cases
- assume "A \<in> sets M"
+proof (cases "A \<in> sets M")
+ case True
show ?thesis
proof (rule emeasure_measure_of[OF restrict_space_def])
show "op \<inter> \<Omega> ` sets M \<subseteq> Pow (\<Omega> \<inter> space M)" "A \<in> sets (restrict_space M \<Omega>)"
@@ -1951,10 +1951,10 @@
qed
qed
next
- assume "A \<notin> sets M"
- moreover with assms have "A \<notin> sets (restrict_space M \<Omega>)"
+ case False
+ with assms have "A \<notin> sets (restrict_space M \<Omega>)"
by (simp add: sets_restrict_space_iff)
- ultimately show ?thesis
+ with False show ?thesis
by (simp add: emeasure_notin_sets)
qed
--- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Fri Jul 22 11:00:43 2016 +0200
@@ -1734,7 +1734,7 @@
proof (rule measure_eqI)
fix X assume "X \<in> sets M"
then have X: "X \<subseteq> A" by auto
- moreover with A have "countable X" by (auto dest: countable_subset)
+ moreover from A X have "countable X" by (auto dest: countable_subset)
ultimately have
"emeasure M X = (\<integral>\<^sup>+a. emeasure M {a} \<partial>count_space X)"
"emeasure N X = (\<integral>\<^sup>+a. emeasure N {a} \<partial>count_space X)"
--- a/src/HOL/Probability/Probability_Mass_Function.thy Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Probability/Probability_Mass_Function.thy Fri Jul 22 11:00:43 2016 +0200
@@ -1104,17 +1104,17 @@
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}"
show "measure p C = measure q C"
- proof cases
- assume "p \<inter> C = {}"
- moreover then have "q \<inter> C = {}"
+ proof (cases "p \<inter> C = {}")
+ case True
+ then have "q \<inter> C = {}"
using quotient_rel_set_disjoint[OF assms C R] by simp
- ultimately show ?thesis
+ with True show ?thesis
unfolding measure_pmf_zero_iff[symmetric] by simp
next
- assume "p \<inter> C \<noteq> {}"
- moreover then have "q \<inter> C \<noteq> {}"
+ case False
+ then have "q \<inter> C \<noteq> {}"
using quotient_rel_set_disjoint[OF assms C R] by simp
- 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"
+ 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"
by auto
then have "R x y"
using in_quotient_imp_in_rel[of UNIV ?R C x y] C assms
--- a/src/HOL/Probability/Radon_Nikodym.thy Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Probability/Radon_Nikodym.thy Fri Jul 22 11:00:43 2016 +0200
@@ -840,11 +840,11 @@
assumes "f \<in> borel_measurable M" "density M f = N"
shows "density M (RN_deriv M N) = N"
proof -
- have "\<exists>f. f \<in> borel_measurable M \<and> density M f = N"
+ have *: "\<exists>f. f \<in> borel_measurable M \<and> density M f = N"
using assms by auto
- moreover then have "density M (SOME f. f \<in> borel_measurable M \<and> density M f = N) = N"
+ then have "density M (SOME f. f \<in> borel_measurable M \<and> density M f = N) = N"
by (rule someI2_ex) auto
- ultimately show ?thesis
+ with * show ?thesis
by (auto simp: RN_deriv_def)
qed
--- a/src/HOL/Probability/SPMF.thy Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Probability/SPMF.thy Fri Jul 22 11:00:43 2016 +0200
@@ -2520,8 +2520,8 @@
ultimately have "(weight_spmf p * weight_spmf q) * (weight_spmf p * weight_spmf q) = 1" by simp
hence *: "weight_spmf p * weight_spmf q = 1"
by(metis antisym_conv less_le mult_less_cancel_left1 weight_pair_spmf weight_spmf_le_1 weight_spmf_nonneg)
- hence "weight_spmf p = 1" by(metis antisym_conv mult_left_le weight_spmf_le_1 weight_spmf_nonneg)
- moreover with * have "weight_spmf q = 1" by simp
+ hence **: "weight_spmf p = 1" by(metis antisym_conv mult_left_le weight_spmf_le_1 weight_spmf_nonneg)
+ moreover from * ** have "weight_spmf q = 1" by simp
moreover note calculation }
note full = this
--- a/src/HOL/Quotient_Examples/Int_Pow.thy Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Quotient_Examples/Int_Pow.thy Fri Jul 22 11:00:43 2016 +0200
@@ -41,8 +41,8 @@
"[| x \<in> Units G; y \<in> Units G |] ==> inv (x \<otimes> y) = inv y \<otimes> inv x"
proof -
assume G: "x \<in> Units G" "y \<in> Units G"
- moreover then have "x \<in> carrier G" "y \<in> carrier G" by auto
- ultimately have "inv (x \<otimes> y) \<otimes> (x \<otimes> y) = (inv y \<otimes> inv x) \<otimes> (x \<otimes> y)"
+ then have "x \<in> carrier G" "y \<in> carrier G" by auto
+ with G have "inv (x \<otimes> y) \<otimes> (x \<otimes> y) = (inv y \<otimes> inv x) \<otimes> (x \<otimes> y)"
by (simp add: m_assoc) (simp add: m_assoc [symmetric])
with G show ?thesis by (simp del: Units_l_inv)
qed
--- a/src/HOL/Set_Interval.thy Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Set_Interval.thy Fri Jul 22 11:00:43 2016 +0200
@@ -578,9 +578,9 @@
obtain y where "Max {a <..} < y"
using gt_ex by auto
- obtain x where "a < x"
+ obtain x where x: "a < x"
using gt_ex by auto
- also then have "x \<le> Max {a <..}"
+ also from x have "x \<le> Max {a <..}"
by fact
also note \<open>Max {a <..} < y\<close>
finally have "y \<le> Max { a <..}"
--- a/src/HOL/Transcendental.thy Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Transcendental.thy Fri Jul 22 11:00:43 2016 +0200
@@ -1617,14 +1617,15 @@
lemma isCont_ln:
fixes x::real assumes "x \<noteq> 0" shows "isCont ln x"
-proof cases
- assume "0 < x"
- moreover then have "isCont ln (exp (ln x))"
+proof (cases "0 < x")
+ case True
+ then have "isCont ln (exp (ln x))"
by (intro isCont_inv_fun[where d="\<bar>x\<bar>" and f=exp]) auto
- ultimately show ?thesis
+ with True show ?thesis
by simp
next
- assume "\<not> 0 < x" with \<open>x \<noteq> 0\<close> show "isCont ln x"
+ case False
+ with \<open>x \<noteq> 0\<close> show "isCont ln x"
unfolding isCont_def
by (subst filterlim_cong[OF _ refl, of _ "nhds (ln 0)" _ "\<lambda>_. ln 0"])
(auto simp: ln_neg_is_const not_less eventually_at dist_real_def
@@ -4902,11 +4903,11 @@
have x1: "x \<le> 1"
using assms
by (metis le_add_same_cancel1 power2_le_imp_le power_one zero_le_power2)
- moreover with assms have ax: "0 \<le> arccos x" "cos(arccos x) = x"
+ with assms have ax: "0 \<le> arccos x" "cos (arccos x) = x"
by (auto simp: arccos)
- moreover have "y = sqrt (1 - x\<^sup>2)" using assms
+ from assms have "y = sqrt (1 - x\<^sup>2)"
by (metis abs_of_nonneg add.commute add_diff_cancel real_sqrt_abs)
- ultimately show ?thesis using assms arccos_le_pi2 [of x]
+ with x1 ax assms arccos_le_pi2 [of x] show ?thesis
by (rule_tac x="arccos x" in exI) (auto simp: sin_arccos)
qed
@@ -5836,26 +5837,25 @@
assume ?lhs
with * have "(\<forall>i\<le>n. c i = (if i=0 then k else 0))"
by (simp add: polyfun_eq_coeffs [symmetric])
- then show ?rhs
- by simp
+ then show ?rhs by simp
next
- assume ?rhs then show ?lhs
- by (induct n) auto
+ assume ?rhs
+ then show ?lhs by (induct n) auto
qed
qed
lemma root_polyfun:
- fixes z:: "'a::idom"
+ fixes z :: "'a::idom"
assumes "1 \<le> n"
- 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"
+ 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"
using assms
- by (cases n; simp add: setsum_head_Suc atLeast0AtMost [symmetric])
+ by (cases n) (simp_all add: setsum_head_Suc atLeast0AtMost [symmetric])
lemma
- fixes zz :: "'a::{idom,real_normed_div_algebra}"
+ fixes zz :: "'a::{idom,real_normed_div_algebra}"
assumes "1 \<le> n"
- shows finite_roots_unity: "finite {z::'a. z^n = 1}"
- and card_roots_unity: "card {z::'a. z^n = 1} \<le> n"
+ shows finite_roots_unity: "finite {z::'a. z^n = 1}"
+ and card_roots_unity: "card {z::'a. z^n = 1} \<le> n"
using polyfun_rootbound [of "\<lambda>i. if i = 0 then -1 else if i=n then 1 else 0" n n] assms
by (auto simp add: root_polyfun [OF assms])
--- a/src/HOL/ex/Ballot.thy Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/ex/Ballot.thy Fri Jul 22 11:00:43 2016 +0200
@@ -180,10 +180,10 @@
by auto
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)}"
by (auto simp: Ico_subset_finite *)
- { fix V assume "V \<subseteq> {0..<?l}"
- moreover then have "finite V" "?l \<notin> V" "{0..<Suc ?l} \<inter> V = V"
+ { fix V assume V: "V \<subseteq> {0..<?l}"
+ then have "finite V" "?l \<notin> V" "{0..<Suc ?l} \<inter> V = V"
by (auto dest: finite_subset)
- ultimately have "card (insert ?l V) = Suc (card V)"
+ with V have "card (insert ?l V) = Suc (card V)"
"card ({0..<m} \<inter> insert ?l V) = (if m = Suc ?l then Suc (card V) else card ({0..<m} \<inter> V))"
if "m \<le> Suc ?l" for m
using that by auto }