# HG changeset patch # User paulson # Date 1652793014 -3600 # Node ID 91c16c5ad3e95efe98c0b29043ee74e4b8dc19ca # Parent 295e1c9d29945703ee27e2148e07d2654ec193d8 tidied auto / simp with null arguments diff -r 295e1c9d2994 -r 91c16c5ad3e9 src/HOL/Algebra/Divisibility.thy --- a/src/HOL/Algebra/Divisibility.thy Wed May 11 10:42:24 2022 +0200 +++ b/src/HOL/Algebra/Divisibility.thy Tue May 17 14:10:14 2022 +0100 @@ -2600,7 +2600,7 @@ next case (Cons x as) then have "x \ carrier G" "set as \ carrier G" and "a divides x \ foldr (\) as \" - by (auto simp: ) + by auto with carr aprime have "a divides x \ a divides foldr (\) as \" by (intro prime_divides) simp+ then show ?case diff -r 295e1c9d2994 -r 91c16c5ad3e9 src/HOL/Analysis/Abstract_Topology.thy --- a/src/HOL/Analysis/Abstract_Topology.thy Wed May 11 10:42:24 2022 +0200 +++ b/src/HOL/Analysis/Abstract_Topology.thy Tue May 17 14:10:14 2022 +0100 @@ -3924,7 +3924,7 @@ using \(x, y) \ E1 \ E2\ \x \ S\ \y \ T\ by auto show "(E1 \ S) \ (E2 \ T) \ U" using \E1 \ E2 \ E\ \U = _\ - by (auto simp: ) + by auto qed qed diff -r 295e1c9d2994 -r 91c16c5ad3e9 src/HOL/Analysis/Lebesgue_Integral_Substitution.thy --- a/src/HOL/Analysis/Lebesgue_Integral_Substitution.thy Wed May 11 10:42:24 2022 +0200 +++ b/src/HOL/Analysis/Lebesgue_Integral_Substitution.thy Tue May 17 14:10:14 2022 +0100 @@ -122,7 +122,7 @@ by (simp add: vimage_Compl diff_eq Int_commute[of "-A"]) also have "{g a..g b} - A = {g a..g b} - A \ {g a..g b}" by blast also have "emeasure lborel ... = g b - g a - emeasure lborel (A \ {g a..g b})" - using \A \ sets borel\ by (subst emeasure_Diff) (auto simp: ) + using \A \ sets borel\ by (subst emeasure_Diff) auto also have "emeasure lborel (A \ {g a..g b}) = \\<^sup>+x. indicator A x * indicator {g a..g b} x \lborel" using \A \ sets borel\ diff -r 295e1c9d2994 -r 91c16c5ad3e9 src/HOL/Analysis/Linear_Algebra.thy --- a/src/HOL/Analysis/Linear_Algebra.thy Wed May 11 10:42:24 2022 +0200 +++ b/src/HOL/Analysis/Linear_Algebra.thy Tue May 17 14:10:14 2022 +0100 @@ -1167,7 +1167,7 @@ next assume ?rhs then obtain u v where *: "\x. x \ S \ \c. x = u + c *\<^sub>R v" - by (auto simp: ) + by auto have "\c. x - y = c *\<^sub>R v" if "x \ S" "y \ S" for x y by (metis *[OF \x \ S\] *[OF \y \ S\] scaleR_left.diff add_diff_cancel_left) then show ?lhs diff -r 295e1c9d2994 -r 91c16c5ad3e9 src/HOL/Analysis/Lipschitz.thy --- a/src/HOL/Analysis/Lipschitz.thy Wed May 11 10:42:24 2022 +0200 +++ b/src/HOL/Analysis/Lipschitz.thy Tue May 17 14:10:14 2022 +0100 @@ -623,7 +623,7 @@ by (simp add: dist_commute) subgoal using \0 < u\ \b \ X\ - by (simp add: ) + by simp done also have "(L + 1) * dist y b \ e / 2" using le1 \0 \ L\ by simp diff -r 295e1c9d2994 -r 91c16c5ad3e9 src/HOL/Analysis/T1_Spaces.thy --- a/src/HOL/Analysis/T1_Spaces.thy Wed May 11 10:42:24 2022 +0200 +++ b/src/HOL/Analysis/T1_Spaces.thy Tue May 17 14:10:14 2022 +0100 @@ -289,7 +289,7 @@ by metis with \a \ T\ compactin_subset_topspace [OF T] have Topen: "\W \ U ` T. openin X W" and Tsub: "T \ \ (U ` T)" - by (auto simp: ) + by auto then obtain \ where \: "finite \" "\ \ U ` T" and "T \ \\" using T unfolding compactin_def by meson then obtain F where F: "finite F" "F \ T" "\ = U ` F" and SUF: "T \ \(U ` F)" and "a \ F" diff -r 295e1c9d2994 -r 91c16c5ad3e9 src/HOL/Complex_Analysis/Winding_Numbers.thy --- a/src/HOL/Complex_Analysis/Winding_Numbers.thy Wed May 11 10:42:24 2022 +0200 +++ b/src/HOL/Complex_Analysis/Winding_Numbers.thy Tue May 17 14:10:14 2022 +0100 @@ -1316,7 +1316,7 @@ also have "... < e" using \e>0\ by (auto simp: norm_mult intro: le_less_trans [OF norm_triangle_ineq4]) finally have "z \ ball 0 e" - using \e>0\ by (simp add: ) + using \e>0\ by simp then have "Im z * Re b \ Im b * Re z" using e by blast then have b: "0 < Re b" "0 < Im b" and disj: "e * Re b < - (Im b * e) \ e * Re b = - (Im b * e)" diff -r 295e1c9d2994 -r 91c16c5ad3e9 src/HOL/Computational_Algebra/Nth_Powers.thy --- a/src/HOL/Computational_Algebra/Nth_Powers.thy Wed May 11 10:42:24 2022 +0200 +++ b/src/HOL/Computational_Algebra/Nth_Powers.thy Tue May 17 14:10:14 2022 +0100 @@ -279,7 +279,7 @@ lemma nth_root_nat_naive_code [code]: "nth_root_nat m n = (if m = 0 \ n = 0 then 0 else if m = 1 \ n = 1 then n else nth_root_nat_aux m 1 1 n)" - using nth_root_nat_aux_correct[of 1 m n] by (auto simp: ) + using nth_root_nat_aux_correct[of 1 m n] by auto lemma nth_root_nat_nth_power [simp]: "k > 0 \ nth_root_nat k (n ^ k) = n" diff -r 295e1c9d2994 -r 91c16c5ad3e9 src/HOL/Decision_Procs/Approximation_Bounds.thy --- a/src/HOL/Decision_Procs/Approximation_Bounds.thy Wed May 11 10:42:24 2022 +0200 +++ b/src/HOL/Decision_Procs/Approximation_Bounds.thy Tue May 17 14:10:14 2022 +0100 @@ -333,7 +333,7 @@ "x * y \\<^sub>r mult_float_interval prec A B" if "x \\<^sub>i real_interval A" "y \\<^sub>i real_interval B" using mult_float_interval[of A B] that - by (auto simp: ) + by auto lemma mult_float_interval_mono': "set_of (mult_float_interval prec A B) \ set_of (mult_float_interval prec X Y)" diff -r 295e1c9d2994 -r 91c16c5ad3e9 src/HOL/Library/Interval.thy --- a/src/HOL/Library/Interval.thy Wed May 11 10:42:24 2022 +0200 +++ b/src/HOL/Library/Interval.thy Tue May 17 14:10:14 2022 +0100 @@ -751,8 +751,8 @@ and upper_split_interval2: "upper (snd (split_interval X m)) = max (upper X) m" subgoal by transfer auto subgoal by transfer (auto simp: min.commute) - subgoal by transfer (auto simp: ) - subgoal by transfer (auto simp: ) + subgoal by transfer auto + subgoal by transfer auto done lemma split_intervalD: "split_interval X x = (A, B) \ set_of X \ set_of A \ set_of B" diff -r 295e1c9d2994 -r 91c16c5ad3e9 src/HOL/Library/Log_Nat.thy --- a/src/HOL/Library/Log_Nat.thy Wed May 11 10:42:24 2022 +0200 +++ b/src/HOL/Library/Log_Nat.thy Tue May 17 14:10:14 2022 +0100 @@ -183,7 +183,7 @@ proof - have "0 \ log (real b) (real x)" using \b > 1\ \0 < x\ - by (auto simp: ) + by auto then have "?l \ b powr log (real b) (real x)" using \b > 1\ by (auto simp flip: powr_realpow intro!: powr_mono of_nat_floor) diff -r 295e1c9d2994 -r 91c16c5ad3e9 src/HOL/Library/Poly_Mapping.thy --- a/src/HOL/Library/Poly_Mapping.thy Wed May 11 10:42:24 2022 +0200 +++ b/src/HOL/Library/Poly_Mapping.thy Tue May 17 14:10:14 2022 +0100 @@ -1688,7 +1688,7 @@ lemma keys_cmul_iff [iff]: "i \ Poly_Mapping.keys (frag_cmul c x) \ i \ Poly_Mapping.keys x \ c \ 0" - apply (auto simp: ) + apply auto apply (meson subsetD keys_cmul) by (metis in_keys_iff lookup_frag_cmul mult_eq_0_iff) diff -r 295e1c9d2994 -r 91c16c5ad3e9 src/HOL/Probability/Distributions.thy --- a/src/HOL/Probability/Distributions.thy Wed May 11 10:42:24 2022 +0200 +++ b/src/HOL/Probability/Distributions.thy Tue May 17 14:10:14 2022 +0100 @@ -1332,7 +1332,7 @@ shows "expectation X = 0" using integral_std_normal_moment_odd[of 0] distributed_integral[OF D, of "\x. x", symmetric] - by (auto simp: ) + by auto lemma (in prob_space) normal_distributed_expectation: assumes \[arith]: "0 < \" diff -r 295e1c9d2994 -r 91c16c5ad3e9 src/HOL/Probability/Product_PMF.thy --- a/src/HOL/Probability/Product_PMF.thy Wed May 11 10:42:24 2022 +0200 +++ b/src/HOL/Probability/Product_PMF.thy Tue May 17 14:10:14 2022 +0100 @@ -354,7 +354,7 @@ Pi_pmf A dflt' (\x. g x \ (\x. return_pmf (f x)))" using assms by (simp add: map_pmf_def Pi_pmf_bind) also have "\ = Pi_pmf A dflt g \ (\h. return_pmf (\x. if x \ A then f (h x) else dflt'))" - by (subst Pi_pmf_bind[where d' = dflt]) (auto simp: ) + by (subst Pi_pmf_bind[where d' = dflt]) auto also have "\ = map_pmf (\h. f \ h) (Pi_pmf A dflt g)" unfolding map_pmf_def using set_Pi_pmf_subset'[of A dflt g] by (intro bind_pmf_cong refl arg_cong[of _ _ return_pmf]) diff -r 295e1c9d2994 -r 91c16c5ad3e9 src/HOL/Probability/Stream_Space.thy --- a/src/HOL/Probability/Stream_Space.thy Wed May 11 10:42:24 2022 +0200 +++ b/src/HOL/Probability/Stream_Space.thy Tue May 17 14:10:14 2022 +0100 @@ -493,7 +493,7 @@ proof (safe intro!: sets_Sup_in_sets del: subsetI equalityI) fix i :: nat show "space (?V i) = space ?R" - using scylinder_streams by (subst space_measure_of) (auto simp: ) + using scylinder_streams by (subst space_measure_of) auto { fix A assume "A \ G" then have "scylinder (space S) (replicate i (space S) @ [A]) = (\s. s !! i) -` A \ streams (space S)" by (induction i) (auto simp add: streams_shd streams_stl cong: conj_cong) diff -r 295e1c9d2994 -r 91c16c5ad3e9 src/HOL/Quotient.thy --- a/src/HOL/Quotient.thy Wed May 11 10:42:24 2022 +0200 +++ b/src/HOL/Quotient.thy Tue May 17 14:10:14 2022 +0100 @@ -576,7 +576,7 @@ using r Quotient3_refl1 R1 rep_abs_rsp by fastforce moreover have "R2' (Rep1 (Abs1 r)) (Rep1 (Abs1 s))" using that - apply (simp add: ) + apply simp apply (metis (full_types) Rep1 Abs1 Quotient3_rel R2 Quotient3_refl1 [OF R1] Quotient3_refl2 [OF R1] Quotient3_rel_abs [OF R1]) done moreover have "R1 (Rep1 (Abs1 s)) s" diff -r 295e1c9d2994 -r 91c16c5ad3e9 src/HOL/Rings.thy --- a/src/HOL/Rings.thy Wed May 11 10:42:24 2022 +0200 +++ b/src/HOL/Rings.thy Tue May 17 14:10:14 2022 +0100 @@ -2408,7 +2408,7 @@ proof (rule ccontr, simp add: not_less) assume "b \ a" with that show False - by (simp add: ) + by simp qed qed diff -r 295e1c9d2994 -r 91c16c5ad3e9 src/HOL/Set_Interval.thy --- a/src/HOL/Set_Interval.thy Wed May 11 10:42:24 2022 +0200 +++ b/src/HOL/Set_Interval.thy Tue May 17 14:10:14 2022 +0100 @@ -465,7 +465,7 @@ apply (auto simp:subset_eq Ball_def not_le) apply(frule_tac x=a in spec) apply(erule_tac x=d in allE) - apply (auto simp: ) + apply auto done lemma atLeastLessThan_inj: