summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Fri, 22 Jul 2016 11:00:43 +0200 | |

changeset 63540 | f8652d0534fa |

parent 63539 | 70d4d9e5707b |

child 63541 | e308f15cc8a7 |

tuned proofs -- avoid unstructured calculation;

--- 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 }