--- a/src/HOL/Binomial.thy Mon Apr 06 19:46:38 2020 +0100
+++ b/src/HOL/Binomial.thy Mon Apr 06 22:46:55 2020 +0100
@@ -1058,9 +1058,7 @@
done
also have "\<dots> =
(fact (m + r + k) div (fact k * fact (m + r)) * (fact (m + r) div (fact r * fact m)))"
- apply (subst div_mult_div_if_dvd)
- apply (auto simp: fact_fact_dvd_fact algebra_simps)
- done
+ by (auto simp: div_mult_div_if_dvd fact_fact_dvd_fact algebra_simps)
finally show ?thesis
by (simp add: binomial_altdef_nat mult.commute)
qed
@@ -1179,17 +1177,13 @@
have 2: "xs \<noteq> [] \<Longrightarrow> sum_list(tl xs) = sum_list xs - hd xs" for xs :: "nat list"
by (auto simp add: neq_Nil_conv)
have f: "bij_betw ?f ?A ?A'"
- apply (rule bij_betw_byWitness[where f' = tl])
- using assms
- apply (auto simp: 2 length_0_conv[symmetric] 1 simp del: length_0_conv)
- done
+ by (rule bij_betw_byWitness[where f' = tl]) (use assms in \<open>auto simp: 2 1 simp flip: length_0_conv\<close>)
have 3: "xs \<noteq> [] \<Longrightarrow> hd xs + (sum_list xs - hd xs) = sum_list xs" for xs :: "nat list"
by (metis 1 sum_list_simps(2) 2)
have g: "bij_betw ?g ?B ?B'"
apply (rule bij_betw_byWitness[where f' = "\<lambda>l. (hd l - 1) # tl l"])
using assms
- by (auto simp: 2 length_0_conv[symmetric] intro!: 3
- simp del: length_greater_0_conv length_0_conv)
+ by (auto simp: 2 simp flip: length_0_conv intro!: 3)
have fin: "finite {xs. size xs = M \<and> set xs \<subseteq> {0..<N}}" for M N :: nat
using finite_lists_length_eq[OF finite_atLeastLessThan] conj_commute by auto
have fin_A: "finite ?A" using fin[of _ "N+1"]
--- a/src/HOL/Real_Vector_Spaces.thy Mon Apr 06 19:46:38 2020 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy Mon Apr 06 22:46:55 2020 +0100
@@ -62,14 +62,10 @@
and span_raw_def: span = real_vector.span
and extend_basis_raw_def: extend_basis = real_vector.extend_basis
and dim_raw_def: dim = real_vector.dim
- apply unfold_locales
- apply (rule scaleR_add_right)
- apply (rule scaleR_add_left)
- apply (rule scaleR_scaleR)
- apply (rule scaleR_one)
- apply (force simp: linear_def)
- apply (force simp: linear_def real_scaleR_def[abs_def])
- done
+proof unfold_locales
+ show "Vector_Spaces.linear (*\<^sub>R) (*\<^sub>R) = linear" "Vector_Spaces.linear (*) (*\<^sub>R) = linear"
+ by (force simp: linear_def real_scaleR_def[abs_def])+
+qed (use scaleR_add_right scaleR_add_left scaleR_scaleR scaleR_one in auto)
hide_const (open)\<comment> \<open>locale constants\<close>
real_vector.dependent
@@ -86,9 +82,10 @@
rewrites "Vector_Spaces.linear (*\<^sub>R) (*\<^sub>R) = linear"
and "Vector_Spaces.linear (*) (*\<^sub>R) = linear"
defines construct_raw_def: construct = real_vector.construct
- apply unfold_locales
- unfolding linear_def real_scaleR_def
- by (rule refl)+
+proof unfold_locales
+ show "Vector_Spaces.linear (*) (*\<^sub>R) = linear"
+ unfolding linear_def real_scaleR_def by auto
+qed (auto simp: linear_def)
hide_const (open)\<comment> \<open>locale constants\<close>
real_vector.construct
@@ -390,8 +387,7 @@
by (auto simp: Reals_def)
lemma Reals_minus_iff [simp]: "- a \<in> \<real> \<longleftrightarrow> a \<in> \<real>"
- apply (auto simp: Reals_def)
- by (metis add.inverse_inverse of_real_minus rangeI)
+ using Reals_minus by fastforce
lemma Reals_diff [simp]: "a \<in> \<real> \<Longrightarrow> b \<in> \<real> \<Longrightarrow> a - b \<in> \<real>"
by (metis Reals_add Reals_minus_iff add_uminus_conv_diff)
@@ -514,10 +510,8 @@
using that by (simp add: less_le_not_le pos_le_minus_divideR_eq pos_minus_divideR_le_eq)
lemma scaleR_image_atLeastAtMost: "c > 0 \<Longrightarrow> scaleR c ` {x..y} = {c *\<^sub>R x..c *\<^sub>R y}"
- apply (auto intro!: scaleR_left_mono)
- apply (rule_tac x = "inverse c *\<^sub>R xa" in image_eqI)
- apply (simp_all add: pos_le_divideR_eq[symmetric] scaleR_scaleR scaleR_one)
- done
+ apply (auto intro!: scaleR_left_mono simp: image_iff Bex_def)
+ by (meson local.eq_iff pos_divideR_le_eq pos_le_divideR_eq)
end
@@ -1273,13 +1267,12 @@
assume "open S"
then obtain f where "\<forall>x\<in>S. 0 < f x \<and> (\<forall>y. dist y x < f x \<longrightarrow> y \<in> S)"
unfolding open_dist bchoice_iff ..
- then have *: "S = (\<Union>x\<in>S. {x - f x <..} \<inter> {..< x + f x})"
+ then have *: "(\<Union>x\<in>S. {x - f x <..} \<inter> {..< x + f x}) = S" (is "?S = S")
by (fastforce simp: dist_real_def)
- show "generate_topology (range lessThan \<union> range greaterThan) S"
- apply (subst *)
- apply (intro generate_topology_Union generate_topology.Int)
- apply (auto intro: generate_topology.Basis)
- done
+ moreover have "generate_topology (range lessThan \<union> range greaterThan) ?S"
+ by (force intro: generate_topology.Basis generate_topology_Union generate_topology.Int)
+ ultimately show "generate_topology (range lessThan \<union> range greaterThan) S"
+ by simp
next
fix S :: "real set"
assume "generate_topology (range lessThan \<union> range greaterThan) S"
@@ -1548,9 +1541,10 @@
by (simp add: diff_left diff_right)
lemma flip: "bounded_bilinear (\<lambda>x y. y ** x)"
- apply standard
- apply (simp_all add: add_right add_left scaleR_right scaleR_left)
- by (metis bounded mult.commute)
+proof
+ show "\<exists>K. \<forall>a b. norm (b ** a) \<le> norm a * norm b * K"
+ by (metis bounded mult.commute)
+qed (simp_all add: add_right add_left scaleR_right scaleR_left)
lemma comp1:
assumes "bounded_linear g"
@@ -1653,11 +1647,10 @@
qed
lemma bounded_bilinear_mult: "bounded_bilinear ((*) :: 'a \<Rightarrow> 'a \<Rightarrow> 'a::real_normed_algebra)"
- apply (rule bounded_bilinear.intro)
- apply (auto simp: algebra_simps)
- apply (rule_tac x=1 in exI)
- apply (simp add: norm_mult_ineq)
- done
+proof (rule bounded_bilinear.intro)
+ show "\<exists>K. \<forall>a b::'a. norm (a * b) \<le> norm a * norm b * K"
+ by (rule_tac x=1 in exI) (simp add: norm_mult_ineq)
+qed (auto simp: algebra_simps)
lemma bounded_linear_mult_left: "bounded_linear (\<lambda>x::'a::real_normed_algebra. x * y)"
using bounded_bilinear_mult
@@ -1678,10 +1671,10 @@
unfolding divide_inverse by (rule bounded_linear_mult_left)
lemma bounded_bilinear_scaleR: "bounded_bilinear scaleR"
- apply (rule bounded_bilinear.intro)
- apply (auto simp: algebra_simps)
- apply (rule_tac x=1 in exI, simp)
- done
+proof (rule bounded_bilinear.intro)
+ show "\<exists>K. \<forall>a b. norm (a *\<^sub>R b) \<le> norm a * norm b * K"
+ using less_eq_real_def by auto
+qed (auto simp: algebra_simps)
lemma bounded_linear_scaleR_left: "bounded_linear (\<lambda>r. scaleR r x)"
using bounded_bilinear_scaleR
@@ -1716,11 +1709,11 @@
instance real_normed_algebra_1 \<subseteq> perfect_space
proof
- show "\<not> open {x}" for x :: 'a
- apply (clarsimp simp: open_dist dist_norm)
- apply (rule_tac x = "x + of_real (e/2)" in exI)
- apply simp
- done
+ fix x::'a
+ have "\<And>e. 0 < e \<Longrightarrow> \<exists>y. norm (y - x) < e \<and> y \<noteq> x"
+ by (rule_tac x = "x + of_real (e/2)" in exI) auto
+ then show "\<not> open {x}"
+ by (clarsimp simp: open_dist dist_norm)
qed
@@ -1793,9 +1786,11 @@
qed
lemma filterlim_real_sequentially: "LIM x sequentially. real x :> at_top"
- apply (clarsimp simp: filterlim_at_top)
- apply (rule_tac c="nat \<lceil>Z + 1\<rceil>" in eventually_sequentiallyI, linarith)
- done
+proof (clarsimp simp: filterlim_at_top)
+ fix Z
+ show "\<forall>\<^sub>F x in sequentially. Z \<le> real x"
+ by (meson eventually_sequentiallyI nat_ceiling_le_eq)
+qed
lemma filterlim_nat_sequentially: "filterlim nat sequentially at_top"
proof -
@@ -1814,17 +1809,20 @@
qed
lemma filterlim_sequentially_iff_filterlim_real:
- "filterlim f sequentially F \<longleftrightarrow> filterlim (\<lambda>x. real (f x)) at_top F"
- apply (rule iffI)
- subgoal using filterlim_compose filterlim_real_sequentially by blast
- subgoal premises prems
+ "filterlim f sequentially F \<longleftrightarrow> filterlim (\<lambda>x. real (f x)) at_top F" (is "?lhs = ?rhs")
+proof
+ assume ?lhs then show ?rhs
+ using filterlim_compose filterlim_real_sequentially by blast
+next
+ assume R: ?rhs
+ show ?lhs
proof -
have "filterlim (\<lambda>x. nat (floor (real (f x)))) sequentially F"
by (intro filterlim_compose[OF filterlim_nat_sequentially]
- filterlim_compose[OF filterlim_floor_sequentially] prems)
+ filterlim_compose[OF filterlim_floor_sequentially] R)
then show ?thesis by simp
qed
- done
+qed
subsubsection \<open>Limits of Sequences\<close>
@@ -1899,10 +1897,8 @@
shows "f \<midarrow>a\<rightarrow> l"
proof -
have "\<And>S. \<lbrakk>open S; l \<in> S; \<forall>\<^sub>F x in at a. g x \<in> S\<rbrakk> \<Longrightarrow> \<forall>\<^sub>F x in at a. f x \<in> S"
- apply (clarsimp simp add: eventually_at)
- apply (rule_tac x="min d R" in exI)
- apply (auto simp: assms)
- done
+ apply (simp add: eventually_at)
+ by (metis assms(2) assms(3) dual_order.strict_trans linorder_neqE_linordered_idom)
then show ?thesis
using assms by (simp add: tendsto_def)
qed
@@ -2171,16 +2167,19 @@
have "dist (u n) l \<le> dist (u n) ((u \<circ> r) n) + dist ((u \<circ> r) n) l"
by (rule dist_triangle)
also have "\<dots> < e/2 + e/2"
- apply (intro add_strict_mono)
- using N1[of n "r n"] N2[of n] that unfolding comp_def
- by (auto simp: less_imp_le) (meson assms(2) less_imp_le order.trans seq_suble)
+ proof (intro add_strict_mono)
+ show "dist (u n) ((u \<circ> r) n) < e / 2"
+ using N1[of n "r n"] N2[of n] that unfolding comp_def
+ by (meson assms(2) le_trans max.bounded_iff strict_mono_imp_increasing)
+ show "dist ((u \<circ> r) n) l < e / 2"
+ using N2 that by auto
+ qed
finally show ?thesis by simp
qed
then show ?thesis unfolding eventually_sequentially by blast
qed
have "(\<lambda>n. dist (u n) l) \<longlonglongrightarrow> 0"
- apply (rule order_tendstoI)
- using * by auto (meson eventually_sequentiallyI less_le_trans zero_le_dist)
+ by (simp add: less_le_trans * order_tendstoI)
then show ?thesis using tendsto_dist_iff by auto
qed