merged
authorAndreas Lochbihler
Tue Dec 01 17:18:34 2015 +0100 (2015-12-01)
changeset 61767f58d75535f66
parent 61766 507b39df1a57
parent 61763 96d2c1b9a30a
child 61768 99f1eaf70c3d
merged
     1.1 --- a/src/HOL/Complex.thy	Tue Dec 01 12:35:11 2015 +0100
     1.2 +++ b/src/HOL/Complex.thy	Tue Dec 01 17:18:34 2015 +0100
     1.3 @@ -748,9 +748,6 @@
     1.4  
     1.5  subsubsection \<open>Complex exponential\<close>
     1.6  
     1.7 -abbreviation Exp :: "complex \<Rightarrow> complex"
     1.8 -  where "Exp \<equiv> exp"
     1.9 -
    1.10  lemma cis_conv_exp: "cis b = exp (\<i> * b)"
    1.11  proof -
    1.12    { fix n :: nat
    1.13 @@ -766,29 +763,29 @@
    1.14               intro!: sums_unique sums_add sums_mult sums_of_real)
    1.15  qed
    1.16  
    1.17 -lemma Exp_eq_polar: "Exp z = exp (Re z) * cis (Im z)"
    1.18 +lemma exp_eq_polar: "exp z = exp (Re z) * cis (Im z)"
    1.19    unfolding cis_conv_exp exp_of_real [symmetric] mult_exp_exp by (cases z) simp
    1.20  
    1.21  lemma Re_exp: "Re (exp z) = exp (Re z) * cos (Im z)"
    1.22 -  unfolding Exp_eq_polar by simp
    1.23 +  unfolding exp_eq_polar by simp
    1.24  
    1.25  lemma Im_exp: "Im (exp z) = exp (Re z) * sin (Im z)"
    1.26 -  unfolding Exp_eq_polar by simp
    1.27 +  unfolding exp_eq_polar by simp
    1.28  
    1.29  lemma norm_cos_sin [simp]: "norm (Complex (cos t) (sin t)) = 1"
    1.30    by (simp add: norm_complex_def)
    1.31  
    1.32  lemma norm_exp_eq_Re [simp]: "norm (exp z) = exp (Re z)"
    1.33 -  by (simp add: cis.code cmod_complex_polar Exp_eq_polar)
    1.34 +  by (simp add: cis.code cmod_complex_polar exp_eq_polar)
    1.35  
    1.36 -lemma complex_Exp_Ex: "\<exists>a r. z = complex_of_real r * Exp a"
    1.37 +lemma complex_exp_exists: "\<exists>a r. z = complex_of_real r * exp a"
    1.38    apply (insert rcis_Ex [of z])
    1.39 -  apply (auto simp add: Exp_eq_polar rcis_def mult.assoc [symmetric])
    1.40 +  apply (auto simp add: exp_eq_polar rcis_def mult.assoc [symmetric])
    1.41    apply (rule_tac x = "ii * complex_of_real a" in exI, auto)
    1.42    done
    1.43  
    1.44 -lemma Exp_two_pi_i [simp]: "Exp((2::complex) * complex_of_real pi * ii) = 1"
    1.45 -  by (simp add: Exp_eq_polar complex_eq_iff)
    1.46 +lemma exp_two_pi_i [simp]: "exp(2 * complex_of_real pi * ii) = 1"
    1.47 +  by (simp add: exp_eq_polar complex_eq_iff)
    1.48  
    1.49  subsubsection \<open>Complex argument\<close>
    1.50  
     2.1 --- a/src/HOL/Decision_Procs/MIR.thy	Tue Dec 01 12:35:11 2015 +0100
     2.2 +++ b/src/HOL/Decision_Procs/MIR.thy	Tue Dec 01 17:18:34 2015 +0100
     2.3 @@ -1644,9 +1644,8 @@
     2.4    "(real_of_int (a::int) + b > 0) = (real_of_int a + real_of_int (floor b) > 0 \<or> (real_of_int a + real_of_int (floor b) = 0 \<and> real_of_int (floor b) - b < 0))"
     2.5  proof-
     2.6    have th: "(real_of_int a + b >0) = (real_of_int (-a) + (-b)< 0)" by arith
     2.7 -  show ?thesis using myless[of _ "real_of_int (floor b)"]
     2.8 -    by (simp only:th split_int_less_real'[where a="-a" and b="-b"])
     2.9 -    (simp add: algebra_simps,arith)
    2.10 +  show ?thesis 
    2.11 +    by (simp only:th split_int_less_real'[where a="-a" and b="-b"]) (auto simp add: algebra_simps)
    2.12  qed
    2.13  
    2.14  lemma split_int_le_real:
    2.15 @@ -3765,8 +3764,7 @@
    2.16  proof-
    2.17    let ?ss = "s - real_of_int (floor s)"
    2.18    from real_of_int_floor_add_one_gt[where r="s", simplified myless[of "s"]]
    2.19 -    of_int_floor_le  have ss0:"?ss \<ge> 0" and ss1:"?ss < 1"
    2.20 -    by (auto simp add: myle[of _ "s", symmetric] myless[of "?ss"])
    2.21 +    of_int_floor_le  have ss0:"?ss \<ge> 0" and ss1:"?ss < 1" by (auto simp: floor_less_cancel)
    2.22    from np have n0: "real_of_int n \<ge> 0" by simp
    2.23    from mult_left_mono[OF up n0] mult_strict_left_mono[OF u1 np]
    2.24    have nu0:"real_of_int n * u - s \<ge> -s" and nun:"real_of_int n * u -s < real_of_int n - s" by auto
    2.25 @@ -4807,7 +4805,7 @@
    2.26    shows "(Ifm bs (E p)) = (\<exists> (i::int). Ifm (real_of_int i#bs) (E (And (And (Ge(CN 0 1 (C 0))) (Lt (CN 0 1 (C (- 1))))) (exsplit p))))" (is "?lhs = ?rhs")
    2.27  proof-
    2.28    have "?rhs = (\<exists> (i::int). \<exists> x. 0\<le> x \<and> x < 1 \<and> Ifm (x#(real_of_int i)#bs) (exsplit p))"
    2.29 -    by (simp add: myless[of _ "1"] myless[of _ "0"] ac_simps)
    2.30 +    by auto
    2.31    also have "\<dots> = (\<exists> (i::int). \<exists> x. 0\<le> x \<and> x < 1 \<and> Ifm ((real_of_int i + x) #bs) p)"
    2.32      by (simp only: exsplit[OF qf] ac_simps)
    2.33    also have "\<dots> = (\<exists> x. Ifm (x#bs) p)"
     3.1 --- a/src/HOL/Finite_Set.thy	Tue Dec 01 12:35:11 2015 +0100
     3.2 +++ b/src/HOL/Finite_Set.thy	Tue Dec 01 17:18:34 2015 +0100
     3.3 @@ -319,6 +319,16 @@
     3.4    apply (simp add: finite_subset [OF inj_on_vimage_singleton] Int_Un_distrib2)
     3.5    done
     3.6  
     3.7 +lemma finite_finite_vimage_IntI:
     3.8 +  assumes "finite F" and "\<And>y. y \<in> F \<Longrightarrow> finite ((h -` {y}) \<inter> A)"
     3.9 +  shows "finite (h -` F \<inter> A)"
    3.10 +proof -
    3.11 +  have *: "h -` F \<inter> A = (\<Union> y\<in>F. (h -` {y}) \<inter> A)"
    3.12 +    by blast
    3.13 +  show ?thesis
    3.14 +    by (simp only: * assms finite_UN_I)
    3.15 +qed
    3.16 +
    3.17  lemma finite_vimageI:
    3.18    "finite F \<Longrightarrow> inj h \<Longrightarrow> finite (h -` F)"
    3.19    using finite_vimage_IntI[of F h UNIV] by auto
     4.1 --- a/src/HOL/Groups.thy	Tue Dec 01 12:35:11 2015 +0100
     4.2 +++ b/src/HOL/Groups.thy	Tue Dec 01 17:18:34 2015 +0100
     4.3 @@ -999,6 +999,9 @@
     4.4  apply (simp add: algebra_simps)
     4.5  done
     4.6  
     4.7 +lemma diff_gt_0_iff_gt [simp]: "a - b > 0 \<longleftrightarrow> a > b"
     4.8 +by (simp add: less_diff_eq)
     4.9 +
    4.10  lemma diff_le_eq[algebra_simps, field_simps]: "a - b \<le> c \<longleftrightarrow> a \<le> c + b"
    4.11  by (auto simp add: le_less diff_less_eq )
    4.12  
     5.1 --- a/src/HOL/Inequalities.thy	Tue Dec 01 12:35:11 2015 +0100
     5.2 +++ b/src/HOL/Inequalities.thy	Tue Dec 01 17:18:34 2015 +0100
     5.3 @@ -66,7 +66,6 @@
     5.4        using assms by (cases "i \<le> j") (auto simp: algebra_simps)
     5.5    } hence "?S \<le> 0"
     5.6      by (auto intro!: setsum_nonpos simp: mult_le_0_iff)
     5.7 -       (auto simp: field_simps)
     5.8    finally show ?thesis by (simp add: algebra_simps)
     5.9  qed
    5.10  
     6.1 --- a/src/HOL/Library/BigO.thy	Tue Dec 01 12:35:11 2015 +0100
     6.2 +++ b/src/HOL/Library/BigO.thy	Tue Dec 01 17:18:34 2015 +0100
     6.3 @@ -200,8 +200,6 @@
     6.4    apply (auto simp add: fun_Compl_def func_plus)
     6.5    apply (drule_tac x = x in spec)+
     6.6    apply force
     6.7 -  apply (drule_tac x = x in spec)+
     6.8 -  apply force
     6.9    done
    6.10  
    6.11  lemma bigo_abs: "(\<lambda>x. abs (f x)) =o O(f)"
     7.1 --- a/src/HOL/Library/Float.thy	Tue Dec 01 12:35:11 2015 +0100
     7.2 +++ b/src/HOL/Library/Float.thy	Tue Dec 01 17:18:34 2015 +0100
     7.3 @@ -1116,10 +1116,11 @@
     7.4  proof -
     7.5    have "0 \<le> log 2 x - real_of_int \<lfloor>log 2 x\<rfloor>"
     7.6      by (simp add: algebra_simps)
     7.7 -  from this assms
     7.8 +  with assms
     7.9    show ?thesis
    7.10 -    by (auto simp: truncate_down_def round_down_def mult_powr_eq
    7.11 +    apply (auto simp: truncate_down_def round_down_def mult_powr_eq 
    7.12        intro!: ge_one_powr_ge_zero mult_pos_pos)
    7.13 +    by linarith
    7.14  qed
    7.15  
    7.16  lemma truncate_down_nonneg: "0 \<le> y \<Longrightarrow> 0 \<le> truncate_down prec y"
     8.1 --- a/src/HOL/Library/Infinite_Set.thy	Tue Dec 01 12:35:11 2015 +0100
     8.2 +++ b/src/HOL/Library/Infinite_Set.thy	Tue Dec 01 17:18:34 2015 +0100
     8.3 @@ -72,10 +72,7 @@
     8.4      by(induction rule: finite_psubset_induct)(meson Diff_subset card_Diff1_less card_psubset finite_Diff step)
     8.5  qed    
     8.6  
     8.7 -text \<open>
     8.8 -  As a concrete example, we prove that the set of natural numbers is
     8.9 -  infinite.
    8.10 -\<close>
    8.11 +text \<open>As a concrete example, we prove that the set of natural numbers is infinite.\<close>
    8.12  
    8.13  lemma infinite_nat_iff_unbounded_le: "infinite (S::nat set) \<longleftrightarrow> (\<forall>m. \<exists>n\<ge>m. n \<in> S)"
    8.14    using frequently_cofinite[of "\<lambda>x. x \<in> S"]
    8.15 @@ -94,6 +91,7 @@
    8.16  lemma finite_nat_bounded: "finite (S::nat set) \<Longrightarrow> \<exists>k. S \<subseteq> {..<k}"
    8.17    by (simp add: finite_nat_iff_bounded)
    8.18  
    8.19 +
    8.20  text \<open>
    8.21    For a set of natural numbers to be infinite, it is enough to know
    8.22    that for any number larger than some \<open>k\<close>, there is some larger
    8.23 @@ -150,6 +148,32 @@
    8.24    obtains y where "y \<in> f`A" and "infinite (f -` {y})"
    8.25    using assms by (blast dest: inf_img_fin_dom)
    8.26  
    8.27 +proposition finite_image_absD:
    8.28 +    fixes S :: "'a::linordered_ring set"
    8.29 +    shows "finite (abs ` S) \<Longrightarrow> finite S"
    8.30 +  by (rule ccontr) (auto simp: abs_eq_iff vimage_def dest: inf_img_fin_dom)
    8.31 +
    8.32 +text \<open>The set of integers is also infinite.\<close>
    8.33 +
    8.34 +lemma infinite_int_iff_infinite_nat_abs: "infinite (S::int set) \<longleftrightarrow> infinite ((nat o abs) ` S)"
    8.35 +  by (auto simp: transfer_nat_int_set_relations o_def image_comp dest: finite_image_absD)
    8.36 +
    8.37 +proposition infinite_int_iff_unbounded_le: "infinite (S::int set) \<longleftrightarrow> (\<forall>m. \<exists>n. abs n \<ge> m \<and> n \<in> S)"
    8.38 +  apply (simp add: infinite_int_iff_infinite_nat_abs infinite_nat_iff_unbounded_le o_def image_def)
    8.39 +  apply (metis abs_ge_zero nat_le_eq_zle le_nat_iff)
    8.40 +  done
    8.41 +
    8.42 +proposition infinite_int_iff_unbounded: "infinite (S::int set) \<longleftrightarrow> (\<forall>m. \<exists>n. abs n > m \<and> n \<in> S)"
    8.43 +  apply (simp add: infinite_int_iff_infinite_nat_abs infinite_nat_iff_unbounded o_def image_def)
    8.44 +  apply (metis (full_types) nat_le_iff nat_mono not_le)
    8.45 +  done
    8.46 +
    8.47 +proposition finite_int_iff_bounded: "finite (S::int set) \<longleftrightarrow> (\<exists>k. abs ` S \<subseteq> {..<k})"
    8.48 +  using infinite_int_iff_unbounded_le[of S] by (simp add: subset_eq) (metis not_le)
    8.49 +
    8.50 +proposition finite_int_iff_bounded_le: "finite (S::int set) \<longleftrightarrow> (\<exists>k. abs ` S \<subseteq> {.. k})"
    8.51 +  using infinite_int_iff_unbounded[of S] by (simp add: subset_eq) (metis not_le)
    8.52 +
    8.53  subsection "Infinitely Many and Almost All"
    8.54  
    8.55  text \<open>
    8.56 @@ -385,24 +409,5 @@
    8.57      unfolding bij_betw_def by (auto intro: enumerate_in_set)
    8.58  qed
    8.59  
    8.60 -subsection "Miscellaneous"
    8.61 -
    8.62 -text \<open>
    8.63 -  A few trivial lemmas about sets that contain at most one element.
    8.64 -  These simplify the reasoning about deterministic automata.
    8.65 -\<close>
    8.66 -
    8.67 -definition atmost_one :: "'a set \<Rightarrow> bool"
    8.68 -  where "atmost_one S \<longleftrightarrow> (\<forall>x y. x\<in>S \<and> y\<in>S \<longrightarrow> x = y)"
    8.69 -
    8.70 -lemma atmost_one_empty: "S = {} \<Longrightarrow> atmost_one S"
    8.71 -  by (simp add: atmost_one_def)
    8.72 -
    8.73 -lemma atmost_one_singleton: "S = {x} \<Longrightarrow> atmost_one S"
    8.74 -  by (simp add: atmost_one_def)
    8.75 -
    8.76 -lemma atmost_one_unique [elim]: "atmost_one S \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> y = x"
    8.77 -  by (simp add: atmost_one_def)
    8.78 -
    8.79  end
    8.80  
     9.1 --- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Tue Dec 01 12:35:11 2015 +0100
     9.2 +++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Tue Dec 01 17:18:34 2015 +0100
     9.3 @@ -3012,7 +3012,7 @@
     9.4                   \<subseteq> ball (p t) (ee (p t))"
     9.5              apply (intro subset_path_image_join pi_hgn pi_ghn')
     9.6              using \<open>N>0\<close> Suc.prems
     9.7 -            apply (auto simp: dist_norm field_simps closed_segment_eq_real_ivl ptgh_ee)
     9.8 +            apply (auto simp: path_image_subpath dist_norm field_simps closed_segment_eq_real_ivl ptgh_ee)
     9.9              done
    9.10            have pi0: "(f has_contour_integral 0)
    9.11                         (subpath (n/ N) ((Suc n)/N) g +++ linepath(g ((Suc n) / N)) (h((Suc n) / N)) +++
    9.12 @@ -3492,7 +3492,7 @@
    9.13    by (simp add: winding_number_valid_path)
    9.14  
    9.15  lemma winding_number_subpath_trivial [simp]: "z \<noteq> g x \<Longrightarrow> winding_number (subpath x x g) z = 0"
    9.16 -  by (simp add: winding_number_valid_path)
    9.17 +  by (simp add: path_image_subpath winding_number_valid_path)
    9.18  
    9.19  lemma winding_number_join:
    9.20    assumes g1: "path g1" "z \<notin> path_image g1"
    9.21 @@ -3742,7 +3742,7 @@
    9.22          by (rule continuous_at_imp_continuous_within)
    9.23        have gdx: "\<gamma> differentiable at x"
    9.24          using x by (simp add: g_diff_at)
    9.25 -      have "((\<lambda>c. Exp (- integral {a..c} (\<lambda>x. vector_derivative \<gamma> (at x) / (\<gamma> x - z))) * (\<gamma> c - z)) has_derivative (\<lambda>h. 0))
    9.26 +      have "((\<lambda>c. exp (- integral {a..c} (\<lambda>x. vector_derivative \<gamma> (at x) / (\<gamma> x - z))) * (\<gamma> c - z)) has_derivative (\<lambda>h. 0))
    9.27            (at x within {a..b})"
    9.28          using x gdx t
    9.29          apply (clarsimp simp add: differentiable_iff_scaleR)
    9.30 @@ -3781,7 +3781,7 @@
    9.31                      "pathstart p = pathstart \<gamma>" "pathfinish p = pathfinish \<gamma>"
    9.32                      "contour_integral p (\<lambda>w. 1 / (w - z)) = complex_of_real (2 * pi) * \<i> * winding_number \<gamma> z"
    9.33      using winding_number [OF assms, of 1] by auto
    9.34 -  have [simp]: "(winding_number \<gamma> z \<in> \<int>) = (Exp (contour_integral p (\<lambda>w. 1 / (w - z))) = 1)"
    9.35 +  have [simp]: "(winding_number \<gamma> z \<in> \<int>) = (exp (contour_integral p (\<lambda>w. 1 / (w - z))) = 1)"
    9.36        using p by (simp add: exp_eq_1 complex_is_Int_iff)
    9.37    have "winding_number p z \<in> \<int> \<longleftrightarrow> pathfinish p = pathstart p"
    9.38      using p z
    9.39 @@ -3840,7 +3840,7 @@
    9.40      using eqArg by (simp add: i_def)
    9.41    have gpdt: "\<gamma> piecewise_C1_differentiable_on {0..t}"
    9.42      by (metis atLeastAtMost_iff atLeastatMost_subset_iff order_refl piecewise_C1_differentiable_on_subset gpd t)
    9.43 -  have "Exp (- i) * (\<gamma> t - z) = \<gamma> 0 - z"
    9.44 +  have "exp (- i) * (\<gamma> t - z) = \<gamma> 0 - z"
    9.45      unfolding i_def
    9.46      apply (rule winding_number_exp_integral [OF gpdt])
    9.47      using t z unfolding path_image_def
    9.48 @@ -3855,7 +3855,7 @@
    9.49      apply (subst Complex_Transcendental.Arg_eq [of r])
    9.50      apply (simp add: iArg)
    9.51      using *
    9.52 -    apply (simp add: Exp_eq_polar field_simps)
    9.53 +    apply (simp add: exp_eq_polar field_simps)
    9.54      done
    9.55    with t show ?thesis
    9.56      by (rule_tac x="exp(Re i) / norm r" in exI) (auto simp: path_image_def)
    9.57 @@ -4225,8 +4225,8 @@
    9.58      also have "... = winding_number (subpath 0 x \<gamma>) z"
    9.59        apply (subst winding_number_valid_path)
    9.60        using assms x
    9.61 -      apply (simp_all add: valid_path_subpath)
    9.62 -      by (force simp: closed_segment_eq_real_ivl path_image_def)
    9.63 +      apply (simp_all add: path_image_subpath valid_path_subpath)
    9.64 +      by (force simp: path_image_def)
    9.65      finally show ?thesis .
    9.66    qed
    9.67    show ?thesis
    9.68 @@ -4277,7 +4277,7 @@
    9.69      have gt: "\<gamma> t - z = - (of_real (exp (- (2 * pi * Im (winding_number (subpath 0 t \<gamma>) z)))) * (\<gamma> 0 - z))"
    9.70        using winding_number_exp_2pi [of "subpath 0 t \<gamma>" z]
    9.71        apply (simp add: t \<gamma> valid_path_imp_path)
    9.72 -      using closed_segment_eq_real_ivl path_image_def t z by (fastforce simp add: Euler sub12)
    9.73 +      using closed_segment_eq_real_ivl path_image_def t z by (fastforce simp: path_image_subpath Euler sub12)
    9.74      have "b < a \<bullet> \<gamma> 0"
    9.75      proof -
    9.76        have "\<gamma> 0 \<in> {c. b < a \<bullet> c}"
    9.77 @@ -4321,7 +4321,7 @@
    9.78      have "isCont (winding_number \<gamma>) z"
    9.79        by (metis continuous_at_winding_number valid_path_imp_path \<gamma> z)
    9.80      then obtain d where "d>0" and d: "\<And>x'. dist x' z < d \<Longrightarrow> dist (winding_number \<gamma> x') (winding_number \<gamma> z) < abs(Re(winding_number \<gamma> z)) - 1/2"
    9.81 -      using continuous_at_eps_delta wnz_12 diff_less_iff(1) by blast
    9.82 +      using continuous_at_eps_delta wnz_12 diff_gt_0_iff_gt by blast
    9.83      def z' \<equiv> "z - (d / (2 * cmod a)) *\<^sub>R a"
    9.84      have *: "a \<bullet> z' \<le> b - d / 3 * cmod a"
    9.85        unfolding z'_def inner_mult_right' divide_inverse
    10.1 --- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Tue Dec 01 12:35:11 2015 +0100
    10.2 +++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Tue Dec 01 17:18:34 2015 +0100
    10.3 @@ -654,7 +654,6 @@
    10.4      done
    10.5  qed
    10.6  
    10.7 -
    10.8  corollary
    10.9    shows Arg_ge_0: "0 \<le> Arg z"
   10.10      and Arg_lt_2pi: "Arg z < 2*pi"
   10.11 @@ -772,7 +771,7 @@
   10.12  lemma Arg_inverse: "Arg(inverse z) = (if z \<in> \<real> \<and> 0 \<le> Re z then Arg z else 2*pi - Arg z)"
   10.13    apply (cases "z=0", simp)
   10.14    apply (rule Arg_unique [of "inverse (norm z)"])
   10.15 -  using Arg_ge_0 [of z] Arg_lt_2pi [of z] Arg_eq [of z] Arg_eq_0 [of z] Exp_two_pi_i
   10.16 +  using Arg_ge_0 [of z] Arg_lt_2pi [of z] Arg_eq [of z] Arg_eq_0 [of z] exp_two_pi_i
   10.17    apply (auto simp: of_real_numeral algebra_simps exp_diff divide_simps)
   10.18    done
   10.19  
   10.20 @@ -849,8 +848,11 @@
   10.21    by auto
   10.22  
   10.23  lemma Arg_exp: "0 \<le> Im z \<Longrightarrow> Im z < 2*pi \<Longrightarrow> Arg(exp z) = Im z"
   10.24 -  by (rule Arg_unique [of  "exp(Re z)"]) (auto simp: Exp_eq_polar)
   10.25 -
   10.26 +  by (rule Arg_unique [of  "exp(Re z)"]) (auto simp: exp_eq_polar)
   10.27 +
   10.28 +lemma complex_split_polar:
   10.29 +  obtains r a::real where "z = complex_of_real r * (cos a + \<i> * sin a)" "0 \<le> r" "0 \<le> a" "a < 2*pi"
   10.30 +  using Arg cis.ctr cis_conv_exp by fastforce
   10.31  
   10.32  subsection\<open>Analytic properties of tangent function\<close>
   10.33  
   10.34 @@ -898,7 +900,7 @@
   10.35    have "exp(ln z) = z & -pi < Im(ln z) & Im(ln z) \<le> pi" unfolding ln_complex_def
   10.36      apply (rule theI [where a = "Complex (ln(norm z)) \<phi>"])
   10.37      using z assms \<phi>
   10.38 -    apply (auto simp: field_simps exp_complex_eqI Exp_eq_polar cis.code)
   10.39 +    apply (auto simp: field_simps exp_complex_eqI exp_eq_polar cis.code)
   10.40      done
   10.41    then show "exp(ln z) = z" "-pi < Im(ln z)" "Im(ln z) \<le> pi"
   10.42      by auto
   10.43 @@ -1516,14 +1518,14 @@
   10.44    shows "((\<lambda>z. z powr r :: complex) has_field_derivative r * z powr (r - 1)) (at z)"
   10.45  proof (subst DERIV_cong_ev[OF refl _ refl])
   10.46    from assms have "eventually (\<lambda>z. z \<noteq> 0) (nhds z)" by (intro t1_space_nhds) auto
   10.47 -  thus "eventually (\<lambda>z. z powr r = Exp (r * Ln z)) (nhds z)"
   10.48 +  thus "eventually (\<lambda>z. z powr r = exp (r * Ln z)) (nhds z)"
   10.49      unfolding powr_def by eventually_elim simp
   10.50  
   10.51 -  have "((\<lambda>z. Exp (r * Ln z)) has_field_derivative Exp (r * Ln z) * (inverse z * r)) (at z)"
   10.52 +  have "((\<lambda>z. exp (r * Ln z)) has_field_derivative exp (r * Ln z) * (inverse z * r)) (at z)"
   10.53      using assms by (auto intro!: derivative_eq_intros has_field_derivative_powr)
   10.54 -  also have "Exp (r * Ln z) * (inverse z * r) = r * z powr (r - 1)"
   10.55 +  also have "exp (r * Ln z) * (inverse z * r) = r * z powr (r - 1)"
   10.56      unfolding powr_def by (simp add: assms exp_diff field_simps)
   10.57 -  finally show "((\<lambda>z. Exp (r * Ln z)) has_field_derivative r * z powr (r - 1)) (at z)"
   10.58 +  finally show "((\<lambda>z. exp (r * Ln z)) has_field_derivative r * z powr (r - 1)) (at z)"
   10.59      by simp
   10.60  qed
   10.61  
   10.62 @@ -2405,7 +2407,7 @@
   10.63  
   10.64  lemma Re_Arcsin_bound: "abs(Re(Arcsin z)) \<le> pi"
   10.65    by (meson Re_Arcsin_bounds abs_le_iff less_eq_real_def minus_less_iff)
   10.66 - 
   10.67 +
   10.68  
   10.69  subsection\<open>Interrelations between Arcsin and Arccos\<close>
   10.70  
   10.71 @@ -2481,7 +2483,6 @@
   10.72    apply (simp add: cos_squared_eq)
   10.73    using assms
   10.74    apply (auto simp: Re_cos Im_cos add_pos_pos mult_le_0_iff zero_le_mult_iff)
   10.75 -  apply (auto simp: algebra_simps)
   10.76    done
   10.77  
   10.78  lemma sin_cos_csqrt:
   10.79 @@ -2491,7 +2492,6 @@
   10.80    apply (simp add: sin_squared_eq)
   10.81    using assms
   10.82    apply (auto simp: Re_sin Im_sin add_pos_pos mult_le_0_iff zero_le_mult_iff)
   10.83 -  apply (auto simp: algebra_simps)
   10.84    done
   10.85  
   10.86  lemma Arcsin_Arccos_csqrt_pos:
   10.87 @@ -2661,7 +2661,7 @@
   10.88    by ( simp add: of_real_sqrt del: csqrt_of_real_nonneg)
   10.89  
   10.90  lemma arcsin_arccos_sqrt_pos: "0 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> arcsin x = arccos(sqrt(1 - x\<^sup>2))"
   10.91 -  apply (simp add: abs_square_le_1 diff_le_iff arcsin_eq_Re_Arcsin arccos_eq_Re_Arccos)
   10.92 +  apply (simp add: abs_square_le_1 arcsin_eq_Re_Arcsin arccos_eq_Re_Arccos)
   10.93    apply (subst Arcsin_Arccos_csqrt_pos)
   10.94    apply (auto simp: power_le_one csqrt_1_diff_eq)
   10.95    done
   10.96 @@ -2671,7 +2671,7 @@
   10.97    by (simp add: arcsin_minus)
   10.98  
   10.99  lemma arccos_arcsin_sqrt_pos: "0 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> arccos x = arcsin(sqrt(1 - x\<^sup>2))"
  10.100 -  apply (simp add: abs_square_le_1 diff_le_iff arcsin_eq_Re_Arcsin arccos_eq_Re_Arccos)
  10.101 +  apply (simp add: abs_square_le_1 arcsin_eq_Re_Arcsin arccos_eq_Re_Arccos)
  10.102    apply (subst Arccos_Arcsin_csqrt_pos)
  10.103    apply (auto simp: power_le_one csqrt_1_diff_eq)
  10.104    done
    11.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Tue Dec 01 12:35:11 2015 +0100
    11.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Tue Dec 01 17:18:34 2015 +0100
    11.3 @@ -4397,7 +4397,7 @@
    11.4      using \<open>y \<in> s\<close>
    11.5    proof -
    11.6      show "inner (y - z) z < inner (y - z) y"
    11.7 -      apply (subst diff_less_iff(1)[symmetric])
    11.8 +      apply (subst diff_gt_0_iff_gt [symmetric])
    11.9        unfolding inner_diff_right[symmetric] and inner_gt_zero_iff
   11.10        using \<open>y\<in>s\<close> \<open>z\<notin>s\<close>
   11.11        apply auto
    12.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Tue Dec 01 12:35:11 2015 +0100
    12.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Tue Dec 01 17:18:34 2015 +0100
    12.3 @@ -688,7 +688,7 @@
    12.4      "x \<in> {a <..< b}"
    12.5      "(\<lambda>xa. f' x xa - (f b - f a) / (b - a) * xa) = (\<lambda>v. 0)" ..
    12.6    then show ?thesis
    12.7 -    by (metis (hide_lams) assms(1) diff_less_iff(1) eq_iff_diff_eq_0
    12.8 +    by (metis (hide_lams) assms(1) diff_gt_0_iff_gt eq_iff_diff_eq_0
    12.9        zero_less_mult_iff nonzero_mult_divide_cancel_right not_real_square_gt_zero
   12.10        times_divide_eq_left)
   12.11  qed
    13.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Tue Dec 01 12:35:11 2015 +0100
    13.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Tue Dec 01 17:18:34 2015 +0100
    13.3 @@ -599,7 +599,7 @@
    13.4    then have cd_ne: "\<forall>i\<in>Basis. c \<bullet> i \<le> d \<bullet> i"
    13.5      using assms unfolding box_ne_empty by auto
    13.6    have "\<And>i. i \<in> Basis \<Longrightarrow> 0 \<le> b \<bullet> i - a \<bullet> i"
    13.7 -    using ab_ne by (metis diff_le_iff(1))
    13.8 +    using ab_ne by auto
    13.9    moreover
   13.10    have "\<And>i. i \<in> Basis \<Longrightarrow> b \<bullet> i - a \<bullet> i \<le> d \<bullet> i - c \<bullet> i"
   13.11      using assms[unfolded subset_eq mem_box,rule_format,OF ab_ab(2)]
    14.1 --- a/src/HOL/Multivariate_Analysis/Path_Connected.thy	Tue Dec 01 12:35:11 2015 +0100
    14.2 +++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy	Tue Dec 01 17:18:34 2015 +0100
    14.3 @@ -375,7 +375,7 @@
    14.4  lemma path_compose_reversepath: "f o reversepath p = reversepath(f o p)"
    14.5    by (rule ext) (simp add: reversepath_def)
    14.6  
    14.7 -lemma join_paths_eq:
    14.8 +lemma joinpaths_eq:
    14.9    "(\<And>t. t \<in> {0..1} \<Longrightarrow> p t = p' t) \<Longrightarrow>
   14.10     (\<And>t. t \<in> {0..1} \<Longrightarrow> q t = q' t)
   14.11     \<Longrightarrow>  t \<in> {0..1} \<Longrightarrow> (p +++ q) t = (p' +++ q') t"
   14.12 @@ -453,8 +453,6 @@
   14.13  lemma path_join_imp: "\<lbrakk>path g1; path g2; pathfinish g1 = pathstart g2\<rbrakk> \<Longrightarrow> path(g1 +++ g2)"
   14.14    by (simp add: path_join)
   14.15  
   14.16 -lemmas join_paths_simps = path_join path_image_join pathstart_join pathfinish_join
   14.17 -
   14.18  lemma simple_path_join_loop:
   14.19    assumes "arc g1" "arc g2"
   14.20            "pathfinish g1 = pathstart g2"  "pathfinish g2 = pathstart g1"
   14.21 @@ -563,18 +561,18 @@
   14.22  definition subpath :: "real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> 'a) \<Rightarrow> real \<Rightarrow> 'a::real_normed_vector"
   14.23    where "subpath a b g \<equiv> \<lambda>x. g((b - a) * x + a)"
   14.24  
   14.25 -lemma path_image_subpath_gen [simp]:
   14.26 -  fixes g :: "real \<Rightarrow> 'a::real_normed_vector"
   14.27 +lemma path_image_subpath_gen:
   14.28 +  fixes g :: "_ \<Rightarrow> 'a::real_normed_vector"
   14.29    shows "path_image(subpath u v g) = g ` (closed_segment u v)"
   14.30    apply (simp add: closed_segment_real_eq path_image_def subpath_def)
   14.31    apply (subst o_def [of g, symmetric])
   14.32    apply (simp add: image_comp [symmetric])
   14.33    done
   14.34  
   14.35 -lemma path_image_subpath [simp]:
   14.36 +lemma path_image_subpath:
   14.37    fixes g :: "real \<Rightarrow> 'a::real_normed_vector"
   14.38    shows "path_image(subpath u v g) = (if u \<le> v then g ` {u..v} else g ` {v..u})"
   14.39 -  by (simp add: closed_segment_eq_real_ivl)
   14.40 +  by (simp add: path_image_subpath_gen closed_segment_eq_real_ivl)
   14.41  
   14.42  lemma path_subpath [simp]:
   14.43    fixes g :: "real \<Rightarrow> 'a::real_normed_vector"
   14.44 @@ -614,7 +612,7 @@
   14.45  
   14.46  lemma affine_ineq:
   14.47    fixes x :: "'a::linordered_idom"
   14.48 -  assumes "x \<le> 1" "v < u"
   14.49 +  assumes "x \<le> 1" "v \<le> u"
   14.50      shows "v + x * u \<le> u + x * v"
   14.51  proof -
   14.52    have "(1-x)*(u-v) \<ge> 0"
   14.53 @@ -726,7 +724,7 @@
   14.54  
   14.55  lemma path_image_subpath_subset:
   14.56      "\<lbrakk>path g; u \<in> {0..1}; v \<in> {0..1}\<rbrakk> \<Longrightarrow> path_image(subpath u v g) \<subseteq> path_image g"
   14.57 -  apply (simp add: closed_segment_real_eq image_affinity_atLeastAtMost)
   14.58 +  apply (simp add: closed_segment_real_eq image_affinity_atLeastAtMost path_image_subpath)
   14.59    apply (auto simp: path_image_def)
   14.60    done
   14.61  
   14.62 @@ -805,7 +803,7 @@
   14.63      apply (rule that [OF `0 \<le> u` `u \<le> 1`])
   14.64      apply (metis DiffI disj frontier_def g0 notin pathstart_def)
   14.65      using `0 \<le> u` g0 disj
   14.66 -    apply (simp add:)
   14.67 +    apply (simp add: path_image_subpath_gen)
   14.68      apply (auto simp: closed_segment_eq_real_ivl pathstart_def pathfinish_def subpath_def)
   14.69      apply (rename_tac y)
   14.70      apply (drule_tac x="y/u" in spec)
   14.71 @@ -825,7 +823,7 @@
   14.72    show ?thesis
   14.73      apply (rule that [of "subpath 0 u g"])
   14.74      using assms u
   14.75 -    apply simp_all
   14.76 +    apply (simp_all add: path_image_subpath)
   14.77      apply (simp add: pathstart_def)
   14.78      apply (force simp: closed_segment_eq_real_ivl path_image_def)
   14.79      done
   14.80 @@ -966,7 +964,7 @@
   14.81    unfolding linepath_def
   14.82    by (intro continuous_intros)
   14.83  
   14.84 -lemma continuous_on_linepath[intro]: "continuous_on s (linepath a b)"
   14.85 +lemma continuous_on_linepath [intro,continuous_intros]: "continuous_on s (linepath a b)"
   14.86    using continuous_linepath_at
   14.87    by (auto intro!: continuous_at_imp_continuous_on)
   14.88  
   14.89 @@ -982,6 +980,9 @@
   14.90    unfolding reversepath_def linepath_def
   14.91    by auto
   14.92  
   14.93 +lemma linepath_0 [simp]: "linepath 0 b x = x *\<^sub>R b"
   14.94 +  by (simp add: linepath_def)
   14.95 +
   14.96  lemma arc_linepath:
   14.97    assumes "a \<noteq> b"
   14.98    shows "arc (linepath a b)"
   14.99 @@ -1566,7 +1567,7 @@
  14.100        have CC: "1 \<le> 1 + (C - 1) * u"
  14.101          using `x \<noteq> a` `0 \<le> u`
  14.102          apply (simp add: C_def divide_simps norm_minus_commute)
  14.103 -        by (metis Bx diff_le_iff(1) less_eq_real_def mult_nonneg_nonneg)
  14.104 +        using Bx by auto
  14.105        have *: "\<And>v. (1 - u) *\<^sub>R x + u *\<^sub>R (a + v *\<^sub>R (x - a)) = a + (1 + (v - 1) * u) *\<^sub>R (x - a)"
  14.106          by (simp add: algebra_simps)
  14.107        have "a + ((1 / (1 + C * u - u)) *\<^sub>R x + ((u / (1 + C * u - u)) *\<^sub>R a + (C * u / (1 + C * u - u)) *\<^sub>R x)) =
  14.108 @@ -1601,7 +1602,7 @@
  14.109        have DD: "1 \<le> 1 + (D - 1) * u"
  14.110          using `y \<noteq> a` `0 \<le> u`
  14.111          apply (simp add: D_def divide_simps norm_minus_commute)
  14.112 -        by (metis By diff_le_iff(1) less_eq_real_def mult_nonneg_nonneg)
  14.113 +        using By by auto
  14.114        have *: "\<And>v. (1 - u) *\<^sub>R y + u *\<^sub>R (a + v *\<^sub>R (y - a)) = a + (1 + (v - 1) * u) *\<^sub>R (y - a)"
  14.115          by (simp add: algebra_simps)
  14.116        have "a + ((1 / (1 + D * u - u)) *\<^sub>R y + ((u / (1 + D * u - u)) *\<^sub>R a + (D * u / (1 + D * u - u)) *\<^sub>R y)) =
  14.117 @@ -2793,7 +2794,7 @@
  14.118  proposition homotopic_paths_sym_eq: "homotopic_paths s p q \<longleftrightarrow> homotopic_paths s q p"
  14.119    by (metis homotopic_paths_sym)
  14.120  
  14.121 -proposition homotopic_paths_trans:
  14.122 +proposition homotopic_paths_trans [trans]:
  14.123       "\<lbrakk>homotopic_paths s p q; homotopic_paths s q r\<rbrakk> \<Longrightarrow> homotopic_paths s p r"
  14.124    apply (simp add: homotopic_paths_def)
  14.125    apply (rule homotopic_with_trans, assumption)
  14.126 @@ -3262,4 +3263,83 @@
  14.127      by (metis atLeastAtMost_iff imageI le_less_trans not_le path_image_def)
  14.128  qed
  14.129  
  14.130 +subsection\<open> Homotopy and subpaths\<close>
  14.131 +
  14.132 +lemma homotopic_join_subpaths1:
  14.133 +  assumes "path g" and pag: "path_image g \<subseteq> s"
  14.134 +      and u: "u \<in> {0..1}" and v: "v \<in> {0..1}" and w: "w \<in> {0..1}" "u \<le> v" "v \<le> w"
  14.135 +    shows "homotopic_paths s (subpath u v g +++ subpath v w g) (subpath u w g)"
  14.136 +proof -
  14.137 +  have 1: "t * 2 \<le> 1 \<Longrightarrow> u + t * (v * 2) \<le> v + t * (u * 2)" for t
  14.138 +    using affine_ineq \<open>u \<le> v\<close> by fastforce
  14.139 +  have 2: "t * 2 > 1 \<Longrightarrow> u + (2*t - 1) * v \<le> v + (2*t - 1) * w" for t
  14.140 +    by (metis add_mono_thms_linordered_semiring(1) diff_gt_0_iff_gt less_eq_real_def mult.commute mult_right_mono \<open>u \<le> v\<close> \<open>v \<le> w\<close>)
  14.141 +  have t2: "\<And>t::real. t*2 = 1 \<Longrightarrow> t = 1/2" by auto
  14.142 +  show ?thesis
  14.143 +    apply (rule homotopic_paths_subset [OF _ pag])
  14.144 +    using assms
  14.145 +    apply (cases "w = u")
  14.146 +    using homotopic_paths_rinv [of "subpath u v g" "path_image g"]
  14.147 +    apply (force simp: closed_segment_eq_real_ivl image_mono path_image_def subpath_refl)
  14.148 +      apply (rule homotopic_paths_sym)
  14.149 +      apply (rule homotopic_paths_reparametrize
  14.150 +             [where f = "\<lambda>t. if  t \<le> 1 / 2
  14.151 +                             then inverse((w - u)) *\<^sub>R (2 * (v - u)) *\<^sub>R t
  14.152 +                             else inverse((w - u)) *\<^sub>R ((v - u) + (w - v) *\<^sub>R (2 *\<^sub>R t - 1))"])
  14.153 +      using \<open>path g\<close> path_subpath u w apply blast
  14.154 +      using \<open>path g\<close> path_image_subpath_subset u w(1) apply blast
  14.155 +      apply simp_all
  14.156 +      apply (subst split_01)
  14.157 +      apply (rule continuous_on_cases continuous_intros | force simp: pathfinish_def joinpaths_def)+
  14.158 +      apply (simp_all add: field_simps not_le)
  14.159 +      apply (force dest!: t2)
  14.160 +      apply (force simp: algebra_simps mult_left_mono affine_ineq dest!: 1 2)
  14.161 +      apply (simp add: joinpaths_def subpath_def)
  14.162 +      apply (force simp: algebra_simps)
  14.163 +      done
  14.164 +qed
  14.165 +
  14.166 +lemma homotopic_join_subpaths2:
  14.167 +  assumes "homotopic_paths s (subpath u v g +++ subpath v w g) (subpath u w g)"
  14.168 +    shows "homotopic_paths s (subpath w v g +++ subpath v u g) (subpath w u g)"
  14.169 +by (metis assms homotopic_paths_reversepath_D pathfinish_subpath pathstart_subpath reversepath_joinpaths reversepath_subpath)
  14.170 +
  14.171 +lemma homotopic_join_subpaths3:
  14.172 +  assumes hom: "homotopic_paths s (subpath u v g +++ subpath v w g) (subpath u w g)"
  14.173 +      and "path g" and pag: "path_image g \<subseteq> s"
  14.174 +      and u: "u \<in> {0..1}" and v: "v \<in> {0..1}" and w: "w \<in> {0..1}"
  14.175 +    shows "homotopic_paths s (subpath v w g +++ subpath w u g) (subpath v u g)"
  14.176 +proof -
  14.177 +  have "homotopic_paths s (subpath u w g +++ subpath w v g) ((subpath u v g +++ subpath v w g) +++ subpath w v g)"
  14.178 +    apply (rule homotopic_paths_join)
  14.179 +    using hom homotopic_paths_sym_eq apply blast
  14.180 +    apply (metis \<open>path g\<close> homotopic_paths_eq pag path_image_subpath_subset path_subpath subset_trans v w)
  14.181 +    apply (simp add:)
  14.182 +    done
  14.183 +  also have "homotopic_paths s ((subpath u v g +++ subpath v w g) +++ subpath w v g) (subpath u v g +++ subpath v w g +++ subpath w v g)"
  14.184 +    apply (rule homotopic_paths_sym [OF homotopic_paths_assoc])
  14.185 +    using assms by (simp_all add: path_image_subpath_subset [THEN order_trans])
  14.186 +  also have "homotopic_paths s (subpath u v g +++ subpath v w g +++ subpath w v g)
  14.187 +                               (subpath u v g +++ linepath (pathfinish (subpath u v g)) (pathfinish (subpath u v g)))"
  14.188 +    apply (rule homotopic_paths_join)
  14.189 +    apply (metis \<open>path g\<close> homotopic_paths_eq order.trans pag path_image_subpath_subset path_subpath u v)
  14.190 +    apply (metis (no_types, lifting) \<open>path g\<close> homotopic_paths_linv order_trans pag path_image_subpath_subset path_subpath pathfinish_subpath reversepath_subpath v w)
  14.191 +    apply (simp add:)
  14.192 +    done
  14.193 +  also have "homotopic_paths s (subpath u v g +++ linepath (pathfinish (subpath u v g)) (pathfinish (subpath u v g))) (subpath u v g)"
  14.194 +    apply (rule homotopic_paths_rid)
  14.195 +    using \<open>path g\<close> path_subpath u v apply blast
  14.196 +    apply (meson \<open>path g\<close> order.trans pag path_image_subpath_subset u v)
  14.197 +    done
  14.198 +  finally have "homotopic_paths s (subpath u w g +++ subpath w v g) (subpath u v g)" .
  14.199 +  then show ?thesis
  14.200 +    using homotopic_join_subpaths2 by blast
  14.201 +qed
  14.202 +
  14.203 +proposition homotopic_join_subpaths:
  14.204 +   "\<lbrakk>path g; path_image g \<subseteq> s; u \<in> {0..1}; v \<in> {0..1}; w \<in> {0..1}\<rbrakk>
  14.205 +    \<Longrightarrow> homotopic_paths s (subpath u v g +++ subpath v w g) (subpath u w g)"
  14.206 +apply (rule le_cases3 [of u v w])
  14.207 +using homotopic_join_subpaths1 homotopic_join_subpaths2 homotopic_join_subpaths3 by metis+
  14.208 +
  14.209  end
    15.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Dec 01 12:35:11 2015 +0100
    15.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Dec 01 17:18:34 2015 +0100
    15.3 @@ -817,6 +817,9 @@
    15.4  definition cball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set"
    15.5    where "cball x e = {y. dist x y \<le> e}"
    15.6  
    15.7 +definition sphere :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set"
    15.8 +  where "sphere x e = {y. dist x y = e}"
    15.9 +
   15.10  lemma mem_ball [simp]: "y \<in> ball x e \<longleftrightarrow> dist x y < e"
   15.11    by (simp add: ball_def)
   15.12  
   15.13 @@ -863,19 +866,6 @@
   15.14  lemma cball_diff_eq_sphere: "cball a r - ball a r =  {x. dist x a = r}"
   15.15    by (auto simp: cball_def ball_def dist_commute)
   15.16  
   15.17 -lemma diff_less_iff:
   15.18 -  "(a::real) - b > 0 \<longleftrightarrow> a > b"
   15.19 -  "(a::real) - b < 0 \<longleftrightarrow> a < b"
   15.20 -  "a - b < c \<longleftrightarrow> a < c + b" "a - b > c \<longleftrightarrow> a > c + b"
   15.21 -  by arith+
   15.22 -
   15.23 -lemma diff_le_iff:
   15.24 -  "(a::real) - b \<ge> 0 \<longleftrightarrow> a \<ge> b"
   15.25 -  "(a::real) - b \<le> 0 \<longleftrightarrow> a \<le> b"
   15.26 -  "a - b \<le> c \<longleftrightarrow> a \<le> c + b"
   15.27 -  "a - b \<ge> c \<longleftrightarrow> a \<ge> c + b"
   15.28 -  by arith+
   15.29 -
   15.30  lemma open_ball [intro, simp]: "open (ball x e)"
   15.31  proof -
   15.32    have "open (dist x -` {..<e})"
   15.33 @@ -7347,7 +7337,7 @@
   15.34      then have "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` cbox a b"
   15.35        unfolding image_iff Bex_def mem_box
   15.36        apply (intro exI[where x="(1 / m) *\<^sub>R (y - c)"])
   15.37 -      apply (auto simp add: pos_le_divide_eq pos_divide_le_eq mult.commute diff_le_iff inner_distrib inner_diff_left)
   15.38 +      apply (auto simp add: pos_le_divide_eq pos_divide_le_eq mult.commute inner_distrib inner_diff_left)
   15.39        done
   15.40    }
   15.41    moreover
   15.42 @@ -7357,7 +7347,7 @@
   15.43      then have "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` cbox a b"
   15.44        unfolding image_iff Bex_def mem_box
   15.45        apply (intro exI[where x="(1 / m) *\<^sub>R (y - c)"])
   15.46 -      apply (auto simp add: neg_le_divide_eq neg_divide_le_eq mult.commute diff_le_iff inner_distrib inner_diff_left)
   15.47 +      apply (auto simp add: neg_le_divide_eq neg_divide_le_eq mult.commute inner_distrib inner_diff_left)
   15.48        done
   15.49    }
   15.50    ultimately show ?thesis using False by (auto simp: cbox_def)
   15.51 @@ -8187,8 +8177,8 @@
   15.52    shows "cball a r \<subseteq> cball a' r' \<longleftrightarrow> dist a a' + r \<le> r' \<or> r < 0"
   15.53          (is "?lhs = ?rhs")
   15.54  proof
   15.55 -  assume ?lhs 
   15.56 -  then show ?rhs 
   15.57 +  assume ?lhs
   15.58 +  then show ?rhs
   15.59    proof (cases "r < 0")
   15.60      case True then show ?rhs by simp
   15.61    next
   15.62 @@ -8209,13 +8199,13 @@
   15.63          using  \<open>a \<noteq> a'\<close> by (simp add: abs_mult_pos field_simps)
   15.64        finally have [simp]: "norm (a' - (a + (r / norm (a - a')) *\<^sub>R (a - a'))) = \<bar>norm (a - a') + r\<bar>" by linarith
   15.65        show ?thesis
   15.66 -        using subsetD [where c = "a' + (1 + r / norm(a - a')) *\<^sub>R (a - a')", OF \<open>?lhs\<close>] \<open>a \<noteq> a'\<close> 
   15.67 +        using subsetD [where c = "a' + (1 + r / norm(a - a')) *\<^sub>R (a - a')", OF \<open>?lhs\<close>] \<open>a \<noteq> a'\<close>
   15.68          by (simp add: dist_norm scaleR_add_left)
   15.69      qed
   15.70      then show ?rhs by (simp add: dist_norm)
   15.71    qed
   15.72  next
   15.73 -  assume ?rhs then show ?lhs 
   15.74 +  assume ?rhs then show ?lhs
   15.75      apply (auto simp: ball_def dist_norm )
   15.76      apply (metis add.commute add_le_cancel_right dist_norm dist_triangle_alt order_trans)
   15.77      using le_less_trans apply fastforce
   15.78 @@ -8227,8 +8217,8 @@
   15.79    shows "cball a r \<subseteq> ball a' r' \<longleftrightarrow> dist a a' + r < r' \<or> r < 0"
   15.80          (is "?lhs = ?rhs")
   15.81  proof
   15.82 -  assume ?lhs 
   15.83 -  then show ?rhs 
   15.84 +  assume ?lhs
   15.85 +  then show ?rhs
   15.86    proof (cases "r < 0")
   15.87      case True then show ?rhs by simp
   15.88    next
   15.89 @@ -8256,7 +8246,7 @@
   15.90      then show ?rhs by (simp add: dist_norm)
   15.91    qed
   15.92  next
   15.93 -  assume ?rhs then show ?lhs 
   15.94 +  assume ?rhs then show ?lhs
   15.95      apply (auto simp: ball_def dist_norm )
   15.96      apply (metis add.commute add_le_cancel_right dist_norm dist_triangle_alt le_less_trans)
   15.97      using le_less_trans apply fastforce
   15.98 @@ -8268,10 +8258,10 @@
   15.99    shows "ball a r \<subseteq> cball a' r' \<longleftrightarrow> dist a a' + r \<le> r' \<or> r \<le> 0"
  15.100          (is "?lhs = ?rhs")
  15.101  proof (cases "r \<le> 0")
  15.102 -  case True then show ?thesis   
  15.103 +  case True then show ?thesis
  15.104      using dist_not_less_zero less_le_trans by force
  15.105  next
  15.106 -  case False show ?thesis  
  15.107 +  case False show ?thesis
  15.108    proof
  15.109      assume ?lhs
  15.110      then have "(cball a r \<subseteq> cball a' r')"
  15.111 @@ -8280,7 +8270,7 @@
  15.112        using False cball_subset_cball_iff by fastforce
  15.113    next
  15.114      assume ?rhs with False show ?lhs
  15.115 -      using ball_subset_cball cball_subset_cball_iff by blast 
  15.116 +      using ball_subset_cball cball_subset_cball_iff by blast
  15.117    qed
  15.118  qed
  15.119  
  15.120 @@ -8289,10 +8279,10 @@
  15.121    shows "ball a r \<subseteq> ball a' r' \<longleftrightarrow> dist a a' + r \<le> r' \<or> r \<le> 0"
  15.122          (is "?lhs = ?rhs")
  15.123  proof (cases "r \<le> 0")
  15.124 -  case True then show ?thesis   
  15.125 +  case True then show ?thesis
  15.126      using dist_not_less_zero less_le_trans by force
  15.127  next
  15.128 -  case False show ?thesis  
  15.129 +  case False show ?thesis
  15.130    proof
  15.131      assume ?lhs
  15.132      then have "0 < r'"
  15.133 @@ -8316,22 +8306,22 @@
  15.134    shows "ball x d = ball y e \<longleftrightarrow> d \<le> 0 \<and> e \<le> 0 \<or> x=y \<and> d=e"
  15.135          (is "?lhs = ?rhs")
  15.136  proof
  15.137 -  assume ?lhs 
  15.138 -  then show ?rhs 
  15.139 +  assume ?lhs
  15.140 +  then show ?rhs
  15.141    proof (cases "d \<le> 0 \<or> e \<le> 0")
  15.142 -    case True 
  15.143 +    case True
  15.144        with \<open>?lhs\<close> show ?rhs
  15.145          by safe (simp_all only: ball_eq_empty [of y e, symmetric] ball_eq_empty [of x d, symmetric])
  15.146    next
  15.147      case False
  15.148 -    with \<open>?lhs\<close> show ?rhs 
  15.149 +    with \<open>?lhs\<close> show ?rhs
  15.150        apply (auto simp add: set_eq_subset ball_subset_ball_iff dist_norm norm_minus_commute algebra_simps)
  15.151        apply (metis add_le_same_cancel1 le_add_same_cancel1 norm_ge_zero norm_pths(2) order_trans)
  15.152        apply (metis add_increasing2 add_le_imp_le_right eq_iff norm_ge_zero)
  15.153        done
  15.154    qed
  15.155  next
  15.156 -  assume ?rhs then show ?lhs 
  15.157 +  assume ?rhs then show ?lhs
  15.158      by (auto simp add: set_eq_subset ball_subset_ball_iff)
  15.159  qed
  15.160  
  15.161 @@ -8340,22 +8330,22 @@
  15.162    shows "cball x d = cball y e \<longleftrightarrow> d < 0 \<and> e < 0 \<or> x=y \<and> d=e"
  15.163          (is "?lhs = ?rhs")
  15.164  proof
  15.165 -  assume ?lhs 
  15.166 -  then show ?rhs 
  15.167 +  assume ?lhs
  15.168 +  then show ?rhs
  15.169    proof (cases "d < 0 \<or> e < 0")
  15.170 -    case True 
  15.171 +    case True
  15.172        with \<open>?lhs\<close> show ?rhs
  15.173          by safe (simp_all only: cball_eq_empty [of y e, symmetric] cball_eq_empty [of x d, symmetric])
  15.174    next
  15.175      case False
  15.176 -    with \<open>?lhs\<close> show ?rhs 
  15.177 +    with \<open>?lhs\<close> show ?rhs
  15.178        apply (auto simp add: set_eq_subset cball_subset_cball_iff dist_norm norm_minus_commute algebra_simps)
  15.179        apply (metis add_le_same_cancel1 le_add_same_cancel1 norm_ge_zero norm_pths(2) order_trans)
  15.180        apply (metis add_increasing2 add_le_imp_le_right eq_iff norm_ge_zero)
  15.181        done
  15.182    qed
  15.183  next
  15.184 -  assume ?rhs then show ?lhs 
  15.185 +  assume ?rhs then show ?lhs
  15.186      by (auto simp add: set_eq_subset cball_subset_cball_iff)
  15.187  qed
  15.188  
  15.189 @@ -8363,7 +8353,7 @@
  15.190    fixes x :: "'a :: euclidean_space"
  15.191    shows "ball x d = cball y e \<longleftrightarrow> d \<le> 0 \<and> e < 0" (is "?lhs = ?rhs")
  15.192  proof
  15.193 -  assume ?lhs 
  15.194 +  assume ?lhs
  15.195    then show ?rhs
  15.196      apply (auto simp add: set_eq_subset ball_subset_cball_iff cball_subset_ball_iff algebra_simps)
  15.197      apply (metis add_increasing2 add_le_cancel_right add_less_same_cancel1 dist_not_less_zero less_le_trans zero_le_dist)
  15.198 @@ -8371,7 +8361,7 @@
  15.199      using \<open>?lhs\<close> ball_eq_empty cball_eq_empty apply blast+
  15.200      done
  15.201  next
  15.202 -  assume ?rhs then show ?lhs 
  15.203 +  assume ?rhs then show ?lhs
  15.204      by (auto simp add: set_eq_subset ball_subset_cball_iff cball_subset_ball_iff)
  15.205  qed
  15.206  
  15.207 @@ -8379,7 +8369,7 @@
  15.208    fixes x :: "'a :: euclidean_space"
  15.209    shows "cball x d = ball y e \<longleftrightarrow> d < 0 \<and> e \<le> 0" (is "?lhs = ?rhs")
  15.210  proof
  15.211 -  assume ?lhs 
  15.212 +  assume ?lhs
  15.213    then show ?rhs
  15.214      apply (auto simp add: set_eq_subset ball_subset_cball_iff cball_subset_ball_iff algebra_simps)
  15.215      apply (metis add_increasing2 add_le_cancel_right add_less_same_cancel1 dist_not_less_zero less_le_trans zero_le_dist)
  15.216 @@ -8387,7 +8377,7 @@
  15.217      using \<open>?lhs\<close> ball_eq_empty cball_eq_empty apply blast+
  15.218      done
  15.219  next
  15.220 -  assume ?rhs then show ?lhs 
  15.221 +  assume ?rhs then show ?lhs
  15.222      by (auto simp add: set_eq_subset ball_subset_cball_iff cball_subset_ball_iff)
  15.223  qed
  15.224  
    16.1 --- a/src/HOL/Multivariate_Analysis/Weierstrass.thy	Tue Dec 01 12:35:11 2015 +0100
    16.2 +++ b/src/HOL/Multivariate_Analysis/Weierstrass.thy	Tue Dec 01 17:18:34 2015 +0100
    16.3 @@ -380,9 +380,7 @@
    16.4        by (simp add: algebra_simps power_mult power2_eq_square power_mult_distrib [symmetric])
    16.5      also have "... \<le> (1/(k * (p t))^n) * 1"
    16.6        apply (rule mult_left_mono [OF power_le_one])
    16.7 -      apply (metis diff_le_iff(1) less_eq_real_def mult.commute power_le_one power_mult ptn_pos ptn_le)
    16.8 -      using pt_pos [OF t] \<open>k>0\<close>
    16.9 -      apply auto
   16.10 +      using pt_pos \<open>k>0\<close> p01 power_le_one t apply auto
   16.11        done
   16.12      also have "... \<le> (1 / (k*\<delta>))^n"
   16.13        using \<open>k>0\<close> \<delta>01  power_mono pt_\<delta> t
    17.1 --- a/src/HOL/NSA/Examples/NSPrimes.thy	Tue Dec 01 12:35:11 2015 +0100
    17.2 +++ b/src/HOL/NSA/Examples/NSPrimes.thy	Tue Dec 01 17:18:34 2015 +0100
    17.3 @@ -61,7 +61,7 @@
    17.4  (* Goldblatt: Exercise 5.11(3a) - p 57  *)
    17.5  lemma starprime:
    17.6    "starprime = {p. 1 < p & (\<forall>m. m dvd p --> m = 1 | m = p)}"
    17.7 -by (transfer, auto simp add: prime_nat_def)
    17.8 +by (transfer, auto simp add: prime_def)
    17.9  
   17.10  (* Goldblatt Exercise 5.11(3b) - p 57  *)
   17.11  lemma hyperprime_factor_exists [rule_format]:
   17.12 @@ -262,17 +262,14 @@
   17.13  text{*Already proved as @{text primes_infinite}, but now using non-standard naturals.*}
   17.14  theorem not_finite_prime: "~ finite {p::nat. prime p}"
   17.15  apply (rule hypnat_infinite_has_nonstandard_iff [THEN iffD2])
   17.16 -apply (cut_tac hypnat_dvd_all_hypnat_of_nat)
   17.17 -apply (erule exE)
   17.18 -apply (erule conjE)
   17.19 -apply (subgoal_tac "1 < N + 1")
   17.20 -prefer 2 apply (blast intro: hypnat_add_one_gt_one)
   17.21 +using hypnat_dvd_all_hypnat_of_nat
   17.22 +apply clarify
   17.23 +apply (drule hypnat_add_one_gt_one)
   17.24  apply (drule hyperprime_factor_exists)
   17.25 -apply auto
   17.26 +apply clarify
   17.27  apply (subgoal_tac "k \<notin> hypnat_of_nat ` {p. prime p}")
   17.28 -apply (force simp add: starprime_def, safe)
   17.29 -apply (drule_tac x = x in bspec, auto)
   17.30 -apply (metis add.commute hdvd_diff hdvd_one_eq_one hypnat_diff_add_inverse2 hypnat_one_not_prime)
   17.31 +apply (force simp add: starprime_def)
   17.32 +apply (metis Compl_iff add.commute dvd_add_left_iff empty_iff hdvd_one_eq_one hypnat_one_not_prime imageE insert_iff mem_Collect_eq zero_not_prime_nat)
   17.33  done
   17.34  
   17.35  end
    18.1 --- a/src/HOL/Number_Theory/Eratosthenes.thy	Tue Dec 01 12:35:11 2015 +0100
    18.2 +++ b/src/HOL/Number_Theory/Eratosthenes.thy	Tue Dec 01 17:18:34 2015 +0100
    18.3 @@ -294,8 +294,8 @@
    18.4      from 2 show ?thesis
    18.5        apply (auto simp add: numbers_of_marks_sieve numeral_2_eq_2 set_primes_upto
    18.6          dest: prime_gt_Suc_0_nat)
    18.7 -      apply (metis One_nat_def Suc_le_eq less_not_refl prime_nat_def)
    18.8 -      apply (metis One_nat_def Suc_le_eq aux prime_nat_def)
    18.9 +      apply (metis One_nat_def Suc_le_eq less_not_refl prime_def)
   18.10 +      apply (metis One_nat_def Suc_le_eq aux prime_def)
   18.11        done
   18.12    qed
   18.13  qed
    19.1 --- a/src/HOL/Number_Theory/Pocklington.thy	Tue Dec 01 12:35:11 2015 +0100
    19.2 +++ b/src/HOL/Number_Theory/Pocklington.thy	Tue Dec 01 17:18:34 2015 +0100
    19.3 @@ -457,11 +457,11 @@
    19.4    proof
    19.5      assume "prime n"
    19.6      then show ?rhs
    19.7 -      by (metis one_not_prime_nat prime_nat_def)
    19.8 +      by (metis one_not_prime_nat prime_def)
    19.9    next
   19.10      assume ?rhs
   19.11      with False show "prime n"
   19.12 -      by (auto simp: prime_def) (metis One_nat_def prime_factor_nat prime_nat_def)
   19.13 +      by (auto simp: prime_def) (metis One_nat_def prime_factor_nat prime_def)
   19.14    qed
   19.15  qed
   19.16  
   19.17 @@ -538,7 +538,7 @@
   19.18    and pp: "prime p" and pn: "p dvd n"
   19.19    shows "[p = 1] (mod q)"
   19.20  proof -
   19.21 -  have p01: "p \<noteq> 0" "p \<noteq> 1" using pp one_not_prime_nat zero_not_prime_nat by auto
   19.22 +  have p01: "p \<noteq> 0" "p \<noteq> 1" using pp one_not_prime_nat zero_not_prime_nat by (auto intro: prime_gt_0_nat)
   19.23    obtain k where k: "a ^ (q * r) - 1 = n*k"
   19.24      by (metis an cong_to_1_nat dvd_def nqr)
   19.25    from pn[unfolded dvd_def] obtain l where l: "n = p*l" by blast
   19.26 @@ -689,7 +689,7 @@
   19.27      from p(2) obtain m where m: "n = p*m" unfolding dvd_def by blast
   19.28      from n m have m0: "m > 0" "m\<noteq>0" by auto
   19.29      have "1 < p"
   19.30 -      by (metis p(1) prime_nat_def)
   19.31 +      by (metis p(1) prime_def)
   19.32      with m0 m have mn: "m < n" by auto
   19.33      from H[rule_format, OF mn m0(2)] obtain ps where ps: "primefact ps m" ..
   19.34      from ps m p(1) have "primefact (p#ps) n" by (simp add: primefact_def)
    20.1 --- a/src/HOL/Number_Theory/Primes.thy	Tue Dec 01 12:35:11 2015 +0100
    20.2 +++ b/src/HOL/Number_Theory/Primes.thy	Tue Dec 01 17:18:34 2015 +0100
    20.3 @@ -37,38 +37,33 @@
    20.4  definition prime :: "nat \<Rightarrow> bool"
    20.5    where "prime p = (1 < p \<and> (\<forall>m. m dvd p \<longrightarrow> m = 1 \<or> m = p))"
    20.6  
    20.7 -lemmas prime_nat_def = prime_def
    20.8 -
    20.9 -
   20.10  subsection \<open>Primes\<close>
   20.11  
   20.12  lemma prime_odd_nat: "prime p \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
   20.13 -  apply (auto simp add: prime_nat_def even_iff_mod_2_eq_zero dvd_eq_mod_eq_0)
   20.14 +  apply (auto simp add: prime_def even_iff_mod_2_eq_zero dvd_eq_mod_eq_0)
   20.15    apply (metis dvd_eq_mod_eq_0 even_Suc mod_by_1 nat_dvd_not_less not_mod_2_eq_0_eq_1 zero_less_numeral)
   20.16    done
   20.17  
   20.18 -(* FIXME Is there a better way to handle these, rather than making them elim rules? *)
   20.19 +lemma prime_gt_0_nat: "prime p \<Longrightarrow> p > 0"
   20.20 +  unfolding prime_def by auto
   20.21  
   20.22 -lemma prime_gt_0_nat [elim]: "prime p \<Longrightarrow> p > 0"
   20.23 -  unfolding prime_nat_def by auto
   20.24 +lemma prime_ge_1_nat: "prime p \<Longrightarrow> p >= 1"
   20.25 +  unfolding prime_def by auto
   20.26  
   20.27 -lemma prime_ge_1_nat [elim]: "prime p \<Longrightarrow> p >= 1"
   20.28 -  unfolding prime_nat_def by auto
   20.29 +lemma prime_gt_1_nat: "prime p \<Longrightarrow> p > 1"
   20.30 +  unfolding prime_def by auto
   20.31  
   20.32 -lemma prime_gt_1_nat [elim]: "prime p \<Longrightarrow> p > 1"
   20.33 -  unfolding prime_nat_def by auto
   20.34 -
   20.35 -lemma prime_ge_Suc_0_nat [elim]: "prime p \<Longrightarrow> p >= Suc 0"
   20.36 -  unfolding prime_nat_def by auto
   20.37 +lemma prime_ge_Suc_0_nat: "prime p \<Longrightarrow> p >= Suc 0"
   20.38 +  unfolding prime_def by auto
   20.39  
   20.40 -lemma prime_gt_Suc_0_nat [elim]: "prime p \<Longrightarrow> p > Suc 0"
   20.41 -  unfolding prime_nat_def by auto
   20.42 +lemma prime_gt_Suc_0_nat: "prime p \<Longrightarrow> p > Suc 0"
   20.43 +  unfolding prime_def by auto
   20.44  
   20.45 -lemma prime_ge_2_nat [elim]: "prime p \<Longrightarrow> p >= 2"
   20.46 -  unfolding prime_nat_def by auto
   20.47 +lemma prime_ge_2_nat: "prime p \<Longrightarrow> p >= 2"
   20.48 +  unfolding prime_def by auto
   20.49  
   20.50  lemma prime_imp_coprime_nat: "prime p \<Longrightarrow> \<not> p dvd n \<Longrightarrow> coprime p n"
   20.51 -  apply (unfold prime_nat_def)
   20.52 +  apply (unfold prime_def)
   20.53    apply (metis gcd_dvd1_nat gcd_dvd2_nat)
   20.54    done
   20.55  
   20.56 @@ -105,7 +100,7 @@
   20.57  
   20.58  lemma not_prime_eq_prod_nat: "(n::nat) > 1 \<Longrightarrow> ~ prime n \<Longrightarrow>
   20.59      EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
   20.60 -  unfolding prime_nat_def dvd_def apply auto
   20.61 +  unfolding prime_def dvd_def apply auto
   20.62    by (metis mult.commute linorder_neq_iff linorder_not_le mult_1
   20.63        n_less_n_mult_m one_le_mult_iff less_imp_le_nat)
   20.64  
   20.65 @@ -129,18 +124,18 @@
   20.66  subsubsection \<open>Make prime naively executable\<close>
   20.67  
   20.68  lemma zero_not_prime_nat [simp]: "~prime (0::nat)"
   20.69 -  by (simp add: prime_nat_def)
   20.70 +  by (simp add: prime_def)
   20.71  
   20.72  lemma one_not_prime_nat [simp]: "~prime (1::nat)"
   20.73 -  by (simp add: prime_nat_def)
   20.74 +  by (simp add: prime_def)
   20.75  
   20.76  lemma Suc_0_not_prime_nat [simp]: "~prime (Suc 0)"
   20.77 -  by (simp add: prime_nat_def)
   20.78 +  by (simp add: prime_def)
   20.79  
   20.80  lemma prime_nat_code [code]:
   20.81      "prime p \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)"
   20.82    apply (simp add: Ball_def)
   20.83 -  apply (metis One_nat_def less_not_refl prime_nat_def dvd_triv_right not_prime_eq_prod_nat)
   20.84 +  apply (metis One_nat_def less_not_refl prime_def dvd_triv_right not_prime_eq_prod_nat)
   20.85    done
   20.86  
   20.87  lemma prime_nat_simp:
   20.88 @@ -178,7 +173,7 @@
   20.89    using two_is_prime_nat
   20.90    apply blast
   20.91    apply (metis One_nat_def dvd.order_trans dvd_refl less_Suc0 linorder_neqE_nat
   20.92 -    nat_dvd_not_less neq0_conv prime_nat_def)
   20.93 +    nat_dvd_not_less neq0_conv prime_def)
   20.94    done
   20.95  
   20.96  text \<open>One property of coprimality is easier to prove via prime factors.\<close>
   20.97 @@ -239,7 +234,8 @@
   20.98        by (rule dvd_diff_nat)
   20.99      then have "p dvd 1" by simp
  20.100      then have "p <= 1" by auto
  20.101 -    moreover from \<open>prime p\<close> have "p > 1" by auto
  20.102 +    moreover from \<open>prime p\<close> have "p > 1"
  20.103 +      using prime_def by blast
  20.104      ultimately have False by auto}
  20.105    then have "n < p" by presburger
  20.106    with \<open>prime p\<close> and \<open>p <= fact n + 1\<close> show ?thesis by auto
  20.107 @@ -270,7 +266,7 @@
  20.108  proof -
  20.109    from assms have
  20.110      "1 < p * q" and P: "\<And>m. m dvd p * q \<Longrightarrow> m = 1 \<or> m = p * q"
  20.111 -    unfolding prime_nat_def by auto
  20.112 +    unfolding prime_def by auto
  20.113    from \<open>1 < p * q\<close> have "p \<noteq> 0" by (cases p) auto
  20.114    then have Q: "p = p * q \<longleftrightarrow> q = 1" by auto
  20.115    have "p dvd p * q" by simp
    21.1 --- a/src/HOL/Number_Theory/UniqueFactorization.thy	Tue Dec 01 12:35:11 2015 +0100
    21.2 +++ b/src/HOL/Number_Theory/UniqueFactorization.thy	Tue Dec 01 17:18:34 2015 +0100
    21.3 @@ -107,9 +107,7 @@
    21.4    ultimately have "a ^ count M a dvd a ^ count N a"
    21.5      by (elim coprime_dvd_mult_nat)
    21.6    with a show ?thesis
    21.7 -    apply (intro power_dvd_imp_le)
    21.8 -    apply auto
    21.9 -    done
   21.10 +    using power_dvd_imp_le prime_def by blast
   21.11  next
   21.12    case False
   21.13    then show ?thesis
   21.14 @@ -247,14 +245,14 @@
   21.15    using assms apply auto
   21.16    done
   21.17  
   21.18 -lemma prime_factors_gt_0_nat [elim]:
   21.19 +lemma prime_factors_gt_0_nat:
   21.20    fixes p :: nat
   21.21    shows "p \<in> prime_factors x \<Longrightarrow> p > 0"
   21.22 -  by (auto dest!: prime_factors_prime_nat)
   21.23 +    using prime_factors_prime_nat by force
   21.24  
   21.25 -lemma prime_factors_gt_0_int [elim]:
   21.26 +lemma prime_factors_gt_0_int:
   21.27    shows "x \<ge> 0 \<Longrightarrow> p \<in> prime_factors x \<Longrightarrow> int p > (0::int)"
   21.28 -  by auto
   21.29 +    by (simp add: prime_factors_gt_0_nat)
   21.30  
   21.31  lemma prime_factors_finite_nat [iff]:
   21.32    fixes n :: nat
   21.33 @@ -303,7 +301,8 @@
   21.34  proof -
   21.35    from assms have "f \<in> multiset"
   21.36      by (auto simp add: multiset_def)
   21.37 -  moreover from assms have "n > 0" by force
   21.38 +  moreover from assms have "n > 0" 
   21.39 +    by (auto intro: prime_gt_0_nat)
   21.40    ultimately have "multiset_prime_factorization n = Abs_multiset f"
   21.41      apply (unfold multiset_prime_factorization_def)
   21.42      apply (subst if_P, assumption)
   21.43 @@ -723,16 +722,16 @@
   21.44      (\<Prod>p \<in> prime_factors x \<union> prime_factors y. p ^ min (multiplicity p x) (multiplicity p y))"
   21.45    (is "_ = ?z")
   21.46  proof -
   21.47 -  have [arith]: "?z > 0"
   21.48 -    by auto
   21.49 +  have [arith]: "?z > 0" 
   21.50 +    using prime_factors_gt_0_nat by auto
   21.51    have aux: "\<And>p. prime p \<Longrightarrow> multiplicity p ?z = min (multiplicity p x) (multiplicity p y)"
   21.52      apply (subst multiplicity_prod_prime_powers_nat)
   21.53      apply auto
   21.54      done
   21.55    have "?z dvd x"
   21.56 -    by (intro multiplicity_dvd'_nat) (auto simp add: aux)
   21.57 +    by (intro multiplicity_dvd'_nat) (auto simp add: aux intro: prime_gt_0_nat)
   21.58    moreover have "?z dvd y"
   21.59 -    by (intro multiplicity_dvd'_nat) (auto simp add: aux)
   21.60 +    by (intro multiplicity_dvd'_nat) (auto simp add: aux intro: prime_gt_0_nat)
   21.61    moreover have "w dvd x \<and> w dvd y \<longrightarrow> w dvd ?z" for w
   21.62    proof (cases "w = 0")
   21.63      case True
   21.64 @@ -758,7 +757,7 @@
   21.65    (is "_ = ?z")
   21.66  proof -
   21.67    have [arith]: "?z > 0"
   21.68 -    by auto
   21.69 +    by (auto intro: prime_gt_0_nat)
   21.70    have aux: "\<And>p. prime p \<Longrightarrow> multiplicity p ?z = max (multiplicity p x) (multiplicity p y)"
   21.71      apply (subst multiplicity_prod_prime_powers_nat)
   21.72      apply auto
   21.73 @@ -776,7 +775,7 @@
   21.74      then show ?thesis
   21.75        apply auto
   21.76        apply (rule multiplicity_dvd'_nat)
   21.77 -      apply (auto intro: dvd_multiplicity_nat simp add: aux)
   21.78 +      apply (auto intro: prime_gt_0_nat dvd_multiplicity_nat simp add: aux)
   21.79        done
   21.80    qed
   21.81    ultimately have "?z = lcm x y"
    22.1 --- a/src/HOL/Old_Number_Theory/Legacy_GCD.thy	Tue Dec 01 12:35:11 2015 +0100
    22.2 +++ b/src/HOL/Old_Number_Theory/Legacy_GCD.thy	Tue Dec 01 17:18:34 2015 +0100
    22.3 @@ -665,7 +665,8 @@
    22.4    apply (simp del: pos_mod_sign add: zgcd_def abs_if nat_mod_distrib)
    22.5    apply (auto simp add: gcd_non_0 nat_mod_distrib [symmetric] zmod_zminus1_eq_if)
    22.6    apply (frule_tac a = m in pos_mod_bound)
    22.7 -  apply (simp del: pos_mod_bound add: nat_diff_distrib gcd_diff2 nat_le_eq_zle)
    22.8 +  apply (simp del: pos_mod_bound add: algebra_simps nat_diff_distrib gcd_diff2 nat_le_eq_zle)
    22.9 +  apply (metis dual_order.strict_implies_order gcd.simps gcd_0_left gcd_diff2 mod_by_0 nat_mono)
   22.10    done
   22.11  
   22.12  lemma zgcd_eq: "zgcd m n = zgcd n (m mod n)"
    23.1 --- a/src/HOL/Orderings.thy	Tue Dec 01 12:35:11 2015 +0100
    23.2 +++ b/src/HOL/Orderings.thy	Tue Dec 01 17:18:34 2015 +0100
    23.3 @@ -310,6 +310,11 @@
    23.4    "(x \<le> y \<Longrightarrow> P) \<Longrightarrow> (y \<le> x \<Longrightarrow> P) \<Longrightarrow> P"
    23.5  using linear by blast
    23.6  
    23.7 +lemma (in linorder) le_cases3:
    23.8 +  "\<lbrakk>\<lbrakk>x \<le> y; y \<le> z\<rbrakk> \<Longrightarrow> P; \<lbrakk>y \<le> x; x \<le> z\<rbrakk> \<Longrightarrow> P; \<lbrakk>x \<le> z; z \<le> y\<rbrakk> \<Longrightarrow> P;
    23.9 +    \<lbrakk>z \<le> y; y \<le> x\<rbrakk> \<Longrightarrow> P; \<lbrakk>y \<le> z; z \<le> x\<rbrakk> \<Longrightarrow> P; \<lbrakk>z \<le> x; x \<le> y\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
   23.10 +by (blast intro: le_cases)
   23.11 +
   23.12  lemma linorder_cases [case_names less equal greater]:
   23.13    "(x < y \<Longrightarrow> P) \<Longrightarrow> (x = y \<Longrightarrow> P) \<Longrightarrow> (y < x \<Longrightarrow> P) \<Longrightarrow> P"
   23.14  using less_linear by blast
    24.1 --- a/src/HOL/Probability/Lebesgue_Measure.thy	Tue Dec 01 12:35:11 2015 +0100
    24.2 +++ b/src/HOL/Probability/Lebesgue_Measure.thy	Tue Dec 01 17:18:34 2015 +0100
    24.3 @@ -46,8 +46,8 @@
    24.4    assume l_r[simp]: "\<And>n. l n \<le> r n" and "a \<le> b" and disj: "disjoint_family (\<lambda>n. {l n<..r n})"
    24.5    assume lr_eq_ab: "(\<Union>i. {l i<..r i}) = {a<..b}"
    24.6  
    24.7 -  have [intro, simp]: "\<And>a b. a \<le> b \<Longrightarrow> 0 \<le> F b - F a"
    24.8 -    by (auto intro!: l_r mono_F simp: diff_le_iff)
    24.9 +  have [intro, simp]: "\<And>a b. a \<le> b \<Longrightarrow> F a \<le> F b"
   24.10 +    by (auto intro!: l_r mono_F)
   24.11  
   24.12    { fix S :: "nat set" assume "finite S"
   24.13      moreover note `a \<le> b`
   24.14 @@ -92,7 +92,7 @@
   24.15            by (auto simp add: Ioc_subset_iff intro!: mono_F)
   24.16          finally show ?case
   24.17            by (auto intro: add_mono)
   24.18 -      qed (simp add: `a \<le> b` less_le)
   24.19 +      qed (auto simp add: `a \<le> b` less_le)
   24.20      qed }
   24.21    note claim1 = this
   24.22  
   24.23 @@ -280,7 +280,7 @@
   24.24      by (auto simp add: claim1 intro!: suminf_bound)
   24.25    ultimately show "(\<Sum>n. ereal (F (r n) - F (l n))) = ereal (F b - F a)"
   24.26      by simp
   24.27 -qed (auto simp: Ioc_inj diff_le_iff mono_F)
   24.28 +qed (auto simp: Ioc_inj mono_F)
   24.29  
   24.30  lemma measure_interval_measure_Ioc:
   24.31    assumes "a \<le> b"
    25.1 --- a/src/HOL/Proofs/Extraction/Euclid.thy	Tue Dec 01 12:35:11 2015 +0100
    25.2 +++ b/src/HOL/Proofs/Extraction/Euclid.thy	Tue Dec 01 17:18:34 2015 +0100
    25.3 @@ -29,7 +29,7 @@
    25.4    by (induct m) auto
    25.5  
    25.6  lemma prime_eq: "prime (p::nat) = (1 < p \<and> (\<forall>m. m dvd p \<longrightarrow> 1 < m \<longrightarrow> m = p))"
    25.7 -  apply (simp add: prime_nat_def)
    25.8 +  apply (simp add: prime_def)
    25.9    apply (rule iffI)
   25.10    apply blast
   25.11    apply (erule conjE)
    26.1 --- a/src/HOL/Real_Vector_Spaces.thy	Tue Dec 01 12:35:11 2015 +0100
    26.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Tue Dec 01 17:18:34 2015 +0100
    26.3 @@ -9,6 +9,10 @@
    26.4  imports Real Topological_Spaces
    26.5  begin
    26.6  
    26.7 +
    26.8 +lemma (in ordered_ab_group_add) diff_ge_0_iff_ge [simp]: "a - b \<ge> 0 \<longleftrightarrow> a \<ge> b"
    26.9 +  by (simp add: le_diff_eq)
   26.10 +
   26.11  subsection \<open>Locale for additive functions\<close>
   26.12  
   26.13  locale additive =
   26.14 @@ -777,6 +781,11 @@
   26.15    thus ?thesis by simp
   26.16  qed
   26.17  
   26.18 +lemma norm_add_leD:
   26.19 +  fixes a b :: "'a::real_normed_vector"
   26.20 +  shows "norm (a + b) \<le> c \<Longrightarrow> norm b \<le> norm a + c"
   26.21 +    by (metis add.commute diff_le_eq norm_diff_ineq order.trans)
   26.22 +
   26.23  lemma norm_diff_triangle_ineq:
   26.24    fixes a b c d :: "'a::real_normed_vector"
   26.25    shows "norm ((a + b) - (c + d)) \<le> norm (a - c) + norm (b - d)"
    27.1 --- a/src/HOL/Rings.thy	Tue Dec 01 12:35:11 2015 +0100
    27.2 +++ b/src/HOL/Rings.thy	Tue Dec 01 17:18:34 2015 +0100
    27.3 @@ -1559,6 +1559,9 @@
    27.4  lemma not_square_less_zero [simp]: "\<not> (a * a < 0)"
    27.5    by (simp add: not_less)
    27.6  
    27.7 +proposition abs_eq_iff: "abs x = abs y \<longleftrightarrow> x = y \<or> x = -y"
    27.8 +  by (auto simp add: abs_if split: split_if_asm)
    27.9 +
   27.10  end
   27.11  
   27.12  class linordered_ring_strict = ring + linordered_semiring_strict
    28.1 --- a/src/HOL/Tools/BNF/bnf_comp.ML	Tue Dec 01 12:35:11 2015 +0100
    28.2 +++ b/src/HOL/Tools/BNF/bnf_comp.ML	Tue Dec 01 17:18:34 2015 +0100
    28.3 @@ -181,7 +181,8 @@
    28.4      val CCA = mk_T_of_bnf oDs CAs outer;
    28.5      val CBs = @{map 3} mk_T_of_bnf Dss Bss_repl inners;
    28.6      val outer_sets = mk_sets_of_bnf (replicate olive oDs) (replicate olive CAs) outer;
    28.7 -    val inner_setss = @{map 3} mk_sets_of_bnf (map (replicate ilive) Dss) (replicate olive Ass) inners;
    28.8 +    val inner_setss =
    28.9 +      @{map 3} mk_sets_of_bnf (map (replicate ilive) Dss) (replicate olive Ass) inners;
   28.10      val inner_bds = @{map 3} mk_bd_of_bnf Dss Ass_repl inners;
   28.11      val outer_bd = mk_bd_of_bnf oDs CAs outer;
   28.12  
   28.13 @@ -692,7 +693,8 @@
   28.14      val ((kill_poss, As), (inners', ((cache', unfold_set'), lthy'))) =
   28.15        normalize_bnfs qualify Ass Ds flatten_tyargs inners accum;
   28.16  
   28.17 -    val Ds = oDs @ flat (@{map 3} (uncurry append oo curry swap oo map o nth) tfreess kill_poss Dss);
   28.18 +    val Ds =
   28.19 +      oDs @ flat (@{map 3} (uncurry append oo curry swap oo map o nth) tfreess kill_poss Dss);
   28.20      val As = map TFree As;
   28.21    in
   28.22      apfst (rpair (Ds, As))
    29.1 --- a/src/HOL/Tools/BNF/bnf_comp_tactics.ML	Tue Dec 01 12:35:11 2015 +0100
    29.2 +++ b/src/HOL/Tools/BNF/bnf_comp_tactics.ML	Tue Dec 01 17:18:34 2015 +0100
    29.3 @@ -74,14 +74,16 @@
    29.4       map (fn thm => rtac ctxt (thm RS fun_cong)) set_map0s @
    29.5       [rtac ctxt (Gset_map0 RS comp_eq_dest_lhs), rtac ctxt sym, rtac ctxt trans_o_apply,
    29.6       rtac ctxt trans_image_cong_o_apply, rtac ctxt trans_image_cong_o_apply,
    29.7 -     rtac ctxt (@{thm image_cong} OF [Gset_map0 RS comp_eq_dest_lhs RS arg_cong_Union, refl] RS trans),
    29.8 +     rtac ctxt (@{thm image_cong} OF [Gset_map0 RS comp_eq_dest_lhs RS arg_cong_Union, refl]
    29.9 +       RS trans),
   29.10       rtac ctxt @{thm trans[OF comp_eq_dest[OF Union_natural[symmetric]]]}, rtac ctxt arg_cong_Union,
   29.11       rtac ctxt @{thm trans[OF comp_eq_dest_lhs[OF image_o_collect[symmetric]]]},
   29.12       rtac ctxt @{thm fun_cong[OF arg_cong[of _ _ collect]]}] @
   29.13       [REPEAT_DETERM_N (length set_map0s) o EVERY' [rtac ctxt @{thm trans[OF image_insert]},
   29.14 -        rtac ctxt @{thm arg_cong2[of _ _ _ _ insert]}, rtac ctxt @{thm ext}, rtac ctxt trans_o_apply,
   29.15 -        rtac ctxt trans_image_cong_o_apply, rtac ctxt @{thm trans[OF image_image]},
   29.16 -        rtac ctxt @{thm sym[OF trans[OF o_apply]]}, rtac ctxt @{thm image_cong[OF refl o_apply]}],
   29.17 +        rtac ctxt @{thm arg_cong2[of _ _ _ _ insert]}, rtac ctxt @{thm ext},
   29.18 +        rtac ctxt trans_o_apply, rtac ctxt trans_image_cong_o_apply,
   29.19 +        rtac ctxt @{thm trans[OF image_image]}, rtac ctxt @{thm sym[OF trans[OF o_apply]]},
   29.20 +        rtac ctxt @{thm image_cong[OF refl o_apply]}],
   29.21       rtac ctxt @{thm image_empty}]) 1;
   29.22  
   29.23  fun mk_comp_map_cong0_tac ctxt set'_eq_sets comp_set_alts map_cong0 map_cong0s =
   29.24 @@ -96,9 +98,9 @@
   29.25            EVERY' [select_prem_tac ctxt n (dtac ctxt @{thm meta_spec}) (k + 1), etac ctxt meta_mp,
   29.26              rtac ctxt (equalityD2 RS set_mp), rtac ctxt (set_alt RS fun_cong RS trans),
   29.27              rtac ctxt trans_o_apply, rtac ctxt (@{thm collect_def} RS arg_cong_Union),
   29.28 -            rtac ctxt @{thm UnionI}, rtac ctxt @{thm UN_I}, REPEAT_DETERM_N i o rtac ctxt @{thm insertI2},
   29.29 -            rtac ctxt @{thm insertI1}, rtac ctxt (o_apply RS equalityD2 RS set_mp),
   29.30 -            etac ctxt @{thm imageI}, assume_tac ctxt])
   29.31 +            rtac ctxt @{thm UnionI}, rtac ctxt @{thm UN_I},
   29.32 +            REPEAT_DETERM_N i o rtac ctxt @{thm insertI2}, rtac ctxt @{thm insertI1},
   29.33 +            rtac ctxt (o_apply RS equalityD2 RS set_mp), etac ctxt @{thm imageI}, assume_tac ctxt])
   29.34            comp_set_alts))
   29.35        map_cong0s) 1)
   29.36    end;
   29.37 @@ -220,14 +222,15 @@
   29.38  
   29.39  fun mk_permute_in_alt_tac ctxt src dest =
   29.40    (rtac ctxt @{thm Collect_cong} THEN'
   29.41 -  mk_rotate_eq_tac ctxt (rtac ctxt refl) trans @{thm conj_assoc} @{thm conj_commute} @{thm conj_cong}
   29.42 -    dest src) 1;
   29.43 +  mk_rotate_eq_tac ctxt (rtac ctxt refl) trans @{thm conj_assoc} @{thm conj_commute}
   29.44 +    @{thm conj_cong} dest src) 1;
   29.45  
   29.46  
   29.47  (* Miscellaneous *)
   29.48  
   29.49  fun mk_le_rel_OO_tac ctxt outer_le_rel_OO outer_rel_mono inner_le_rel_OOs =
   29.50 -  EVERY' (map (rtac ctxt) (@{thm order_trans} :: outer_le_rel_OO :: outer_rel_mono :: inner_le_rel_OOs)) 1;
   29.51 +  EVERY' (map (rtac ctxt) (@{thm order_trans} :: outer_le_rel_OO :: outer_rel_mono ::
   29.52 +    inner_le_rel_OOs)) 1;
   29.53  
   29.54  fun mk_simple_rel_OO_Grp_tac ctxt rel_OO_Grp in_alt_thm =
   29.55    rtac ctxt (trans OF [rel_OO_Grp, in_alt_thm RS @{thm OO_Grp_cong} RS sym]) 1;
    30.1 --- a/src/HOL/Tools/BNF/bnf_def.ML	Tue Dec 01 12:35:11 2015 +0100
    30.2 +++ b/src/HOL/Tools/BNF/bnf_def.ML	Tue Dec 01 17:18:34 2015 +0100
    30.3 @@ -1300,10 +1300,12 @@
    30.4                  val funTs = map (fn T => bdT --> T) ranTs;
    30.5                  val ran_bnfT = mk_bnf_T ranTs Calpha;
    30.6                  val (revTs, Ts) = `rev (bd_bnfT :: funTs);
    30.7 -                val cTs = map (SOME o Thm.ctyp_of lthy) [ran_bnfT, Library.foldr1 HOLogic.mk_prodT Ts];
    30.8 -                val tinst = fold (fn T => fn t => HOLogic.mk_case_prod (Term.absdummy T t)) (tl revTs)
    30.9 -                  (Term.absdummy (hd revTs) (Term.list_comb (mk_bnf_map bdTs ranTs,
   30.10 -                    map Bound (live - 1 downto 0)) $ Bound live));
   30.11 +                val cTs = map (SOME o Thm.ctyp_of lthy) [ran_bnfT,
   30.12 +                  Library.foldr1 HOLogic.mk_prodT Ts];
   30.13 +                val tinst = fold (fn T => fn t =>
   30.14 +                  HOLogic.mk_case_prod (Term.absdummy T t)) (tl revTs)
   30.15 +                    (Term.absdummy (hd revTs) (Term.list_comb (mk_bnf_map bdTs ranTs,
   30.16 +                      map Bound (live - 1 downto 0)) $ Bound live));
   30.17                  val cts = [NONE, SOME (Thm.cterm_of lthy tinst)];
   30.18                in
   30.19                  Thm.instantiate' cTs cts @{thm surj_imp_ordLeq}
   30.20 @@ -1420,7 +1422,8 @@
   30.21          val in_rel = Lazy.lazy mk_in_rel;
   30.22  
   30.23          fun mk_rel_flip () =
   30.24 -          unfold_thms lthy @{thms conversep_iff} (Lazy.force rel_conversep RS @{thm predicate2_eqD});
   30.25 +          unfold_thms lthy @{thms conversep_iff}
   30.26 +            (Lazy.force rel_conversep RS @{thm predicate2_eqD});
   30.27  
   30.28          val rel_flip = Lazy.lazy mk_rel_flip;
   30.29  
    31.1 --- a/src/HOL/Tools/BNF/bnf_def_tactics.ML	Tue Dec 01 12:35:11 2015 +0100
    31.2 +++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML	Tue Dec 01 17:18:34 2015 +0100
    31.3 @@ -97,18 +97,20 @@
    31.4  fun mk_rel_Grp_tac ctxt rel_OO_Grps map_id0 map_cong0 map_id map_comp set_maps =
    31.5    let
    31.6      val n = length set_maps;
    31.7 -    val rel_OO_Grps_tac = if null rel_OO_Grps then K all_tac else rtac ctxt (hd rel_OO_Grps RS trans);
    31.8 +    val rel_OO_Grps_tac =
    31.9 +      if null rel_OO_Grps then K all_tac else rtac ctxt (hd rel_OO_Grps RS trans);
   31.10    in
   31.11      if null set_maps then
   31.12        unfold_thms_tac ctxt ((map_id0 RS @{thm Grp_UNIV_id}) :: rel_OO_Grps) THEN
   31.13        rtac ctxt @{thm Grp_UNIV_idI[OF refl]} 1
   31.14      else
   31.15        EVERY' [rel_OO_Grps_tac, rtac ctxt @{thm antisym}, rtac ctxt @{thm predicate2I},
   31.16 -        REPEAT_DETERM o
   31.17 -          eresolve_tac ctxt [CollectE, exE, conjE, @{thm GrpE}, @{thm relcomppE}, @{thm conversepE}],
   31.18 -        hyp_subst_tac ctxt, rtac ctxt @{thm GrpI}, rtac ctxt trans, rtac ctxt map_comp, rtac ctxt map_cong0,
   31.19 -        REPEAT_DETERM_N n o
   31.20 -          EVERY' [rtac ctxt @{thm Collect_case_prod_Grp_eqD}, etac ctxt @{thm set_mp}, assume_tac ctxt],
   31.21 +        REPEAT_DETERM o eresolve_tac ctxt
   31.22 +          [CollectE, exE, conjE, @{thm GrpE}, @{thm relcomppE}, @{thm conversepE}],
   31.23 +        hyp_subst_tac ctxt, rtac ctxt @{thm GrpI}, rtac ctxt trans, rtac ctxt map_comp,
   31.24 +          rtac ctxt map_cong0,
   31.25 +        REPEAT_DETERM_N n o EVERY' [rtac ctxt @{thm Collect_case_prod_Grp_eqD},
   31.26 +          etac ctxt @{thm set_mp}, assume_tac ctxt],
   31.27          rtac ctxt CollectI,
   31.28          CONJ_WRAP' (fn thm => EVERY' [rtac ctxt (thm RS ord_eq_le_trans),
   31.29            rtac ctxt @{thm image_subsetI}, rtac ctxt @{thm Collect_case_prod_Grp_in},
   31.30 @@ -151,8 +153,9 @@
   31.31        unfold_thms_tac ctxt [rel_compp, rel_conversep, rel_Grp, @{thm vimage2p_Grp}] THEN
   31.32        TRYALL (EVERY' [rtac ctxt iffI, rtac ctxt @{thm relcomppI}, rtac ctxt @{thm GrpI},
   31.33          resolve_tac ctxt [map_id, refl], rtac ctxt CollectI,
   31.34 -        CONJ_WRAP' (K (rtac ctxt @{thm subset_UNIV})) ks, rtac ctxt @{thm relcomppI}, assume_tac ctxt,
   31.35 -        rtac ctxt @{thm conversepI}, rtac ctxt @{thm GrpI}, resolve_tac ctxt [map_id, refl], rtac ctxt CollectI,
   31.36 +        CONJ_WRAP' (K (rtac ctxt @{thm subset_UNIV})) ks, rtac ctxt @{thm relcomppI},
   31.37 +        assume_tac ctxt, rtac ctxt @{thm conversepI}, rtac ctxt @{thm GrpI},
   31.38 +        resolve_tac ctxt [map_id, refl], rtac ctxt CollectI,
   31.39          CONJ_WRAP' (K (rtac ctxt @{thm subset_UNIV})) ks,
   31.40          REPEAT_DETERM o eresolve_tac ctxt @{thms relcomppE conversepE GrpE},
   31.41          dtac ctxt (trans OF [sym, map_id]), hyp_subst_tac ctxt, assume_tac ctxt])
    32.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Dec 01 12:35:11 2015 +0100
    32.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Dec 01 17:18:34 2015 +0100
    32.3 @@ -75,8 +75,8 @@
    32.4    val fp_sugar_of_global: theory -> string -> fp_sugar option
    32.5    val fp_sugars_of: Proof.context -> fp_sugar list
    32.6    val fp_sugars_of_global: theory -> fp_sugar list
    32.7 -  val fp_sugars_interpretation: string ->
    32.8 -    (fp_sugar list -> local_theory -> local_theory)-> theory -> theory
    32.9 +  val fp_sugars_interpretation: string -> (fp_sugar list -> local_theory -> local_theory) ->
   32.10 +    theory -> theory
   32.11    val interpret_fp_sugars: (string -> bool) -> fp_sugar list -> local_theory -> local_theory
   32.12    val register_fp_sugars_raw: fp_sugar list -> local_theory -> local_theory
   32.13    val register_fp_sugars: (string -> bool) -> fp_sugar list -> local_theory -> local_theory
   32.14 @@ -334,7 +334,7 @@
   32.15  );
   32.16  
   32.17  fun fp_sugar_of_generic context =
   32.18 -  Option.map (transfer_fp_sugar (Context.theory_of context)) o Symtab.lookup (Data.get context)
   32.19 +  Option.map (transfer_fp_sugar (Context.theory_of context)) o Symtab.lookup (Data.get context);
   32.20  
   32.21  fun fp_sugars_of_generic context =
   32.22    Symtab.fold (cons o transfer_fp_sugar (Context.theory_of context) o snd) (Data.get context) [];
   32.23 @@ -1206,7 +1206,8 @@
   32.24    let
   32.25      val ctr_Tsss' = map repair_nullary_single_ctr ctr_Tsss;
   32.26      val g_absTs = map range_type fun_Ts;
   32.27 -    val g_Tsss = map repair_nullary_single_ctr (@{map 5} dest_absumprodT absTs repTs ns mss g_absTs);
   32.28 +    val g_Tsss =
   32.29 +      map repair_nullary_single_ctr (@{map 5} dest_absumprodT absTs repTs ns mss g_absTs);
   32.30      val g_Tssss = @{map 3} (fn C => map2 (map2 (map (curry (op -->) C) oo unzip_corecT)))
   32.31        Cs ctr_Tsss' g_Tsss;
   32.32      val q_Tssss = map (map (map (fn [_] => [] | [_, T] => [mk_pred1T (domain_type T)]))) g_Tssss;
   32.33 @@ -1312,7 +1313,8 @@
   32.34             ctor_rec_absTs reps fss xssss)))
   32.35    end;
   32.36  
   32.37 -fun define_corec (_, cs, cpss, (((pgss, _, _, _), cqgsss), f_absTs)) mk_binding fpTs Cs abss dtor_corec =
   32.38 +fun define_corec (_, cs, cpss, (((pgss, _, _, _), cqgsss), f_absTs)) mk_binding fpTs Cs abss
   32.39 +    dtor_corec =
   32.40    let
   32.41      val nn = length fpTs;
   32.42      val fpT = range_type (snd (strip_typeN nn (fastype_of dtor_corec)));
   32.43 @@ -1371,8 +1373,8 @@
   32.44  
   32.45      val rel_induct0_thm =
   32.46        Goal.prove_sorry lthy vars prems goal (fn {context = ctxt, prems} =>
   32.47 -        mk_rel_induct0_tac ctxt ctor_rel_induct prems (map (Thm.cterm_of ctxt) IRs) exhausts ctor_defss
   32.48 -          ctor_injects pre_rel_defs abs_inverses live_nesting_rel_eqs)
   32.49 +        mk_rel_induct0_tac ctxt ctor_rel_induct prems (map (Thm.cterm_of ctxt) IRs) exhausts
   32.50 +          ctor_defss ctor_injects pre_rel_defs abs_inverses live_nesting_rel_eqs)
   32.51        |> Thm.close_derivation;
   32.52    in
   32.53      (postproc_co_induct lthy (length fpA_Ts) @{thm predicate2D} @{thm predicate2D_conj}
   32.54 @@ -1713,8 +1715,8 @@
   32.55          val thm =
   32.56            Goal.prove_sorry lthy vars prems (HOLogic.mk_Trueprop concl)
   32.57              (fn {context = ctxt, prems} =>
   32.58 -               mk_set_induct0_tac ctxt (map (Thm.cterm_of ctxt'') Ps) prems dtor_set_inducts exhausts
   32.59 -                 set_pre_defs ctor_defs dtor_ctors Abs_pre_inverses)
   32.60 +               mk_set_induct0_tac ctxt (map (Thm.cterm_of ctxt'') Ps) prems dtor_set_inducts
   32.61 +                 exhausts set_pre_defs ctor_defs dtor_ctors Abs_pre_inverses)
   32.62            |> Thm.close_derivation;
   32.63  
   32.64          val case_names_attr =
   32.65 @@ -1811,7 +1813,8 @@
   32.66               []
   32.67             else
   32.68               [Library.foldr HOLogic.mk_imp (if n = 1 then [] else [udisc, vdisc],
   32.69 -                Library.foldr1 HOLogic.mk_conj (@{map 3} (build_rel_app rs') usels vsels ctrXs_Ts))]);
   32.70 +                Library.foldr1 HOLogic.mk_conj
   32.71 +                  (@{map 3} (build_rel_app rs') usels vsels ctrXs_Ts))]);
   32.72  
   32.73          fun mk_prem_concl rs' n udiscs uselss vdiscs vselss ctrXs_Tss =
   32.74            Library.foldr1 HOLogic.mk_conj (flat (@{map 6} (mk_prem_ctr_concls rs' n)
   32.75 @@ -2323,8 +2326,9 @@
   32.76        in
   32.77          Goal.prove_sorry lthy vars [] goal
   32.78            (fn {context = ctxt, prems = _} =>
   32.79 -             mk_rec_transfer_tac ctxt nn ns (map (Thm.cterm_of ctxt) Ss) (map (Thm.cterm_of ctxt) Rs) xsssss
   32.80 -               rec_defs xtor_co_rec_transfers pre_rel_defs live_nesting_rel_eqs)
   32.81 +             mk_rec_transfer_tac ctxt nn ns (map (Thm.cterm_of ctxt) Ss)
   32.82 +               (map (Thm.cterm_of ctxt) Rs) xsssss rec_defs xtor_co_rec_transfers pre_rel_defs
   32.83 +               live_nesting_rel_eqs)
   32.84          |> Thm.close_derivation
   32.85          |> Conjunction.elim_balanced nn
   32.86        end;
   32.87 @@ -2431,7 +2435,8 @@
   32.88          val rec_o_map_thmss = derive_rec_o_map_thmss lthy recs rec_defs;
   32.89  
   32.90          val simp_thmss =
   32.91 -          @{map 6} mk_simp_thms ctr_sugars rec_thmss map_thmss rel_injectss rel_distinctss set_thmss;
   32.92 +          @{map 6} mk_simp_thms ctr_sugars rec_thmss map_thmss rel_injectss rel_distinctss
   32.93 +            set_thmss;
   32.94  
   32.95          val common_notes =
   32.96            (if nn > 1 then
    33.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Tue Dec 01 12:35:11 2015 +0100
    33.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Tue Dec 01 17:18:34 2015 +0100
    33.3 @@ -305,13 +305,15 @@
    33.4    end;
    33.5  
    33.6  fun solve_prem_prem_tac ctxt =
    33.7 -  REPEAT o (eresolve_tac ctxt @{thms bexE rev_bexI} ORELSE' rtac ctxt @{thm rev_bexI[OF UNIV_I]} ORELSE'
    33.8 -    hyp_subst_tac ctxt ORELSE' resolve_tac ctxt @{thms disjI1 disjI2}) THEN'
    33.9 +  REPEAT o (eresolve_tac ctxt @{thms bexE rev_bexI} ORELSE'
   33.10 +    rtac ctxt @{thm rev_bexI[OF UNIV_I]} ORELSE' hyp_subst_tac ctxt ORELSE'
   33.11 +    resolve_tac ctxt @{thms disjI1 disjI2}) THEN'
   33.12    (rtac ctxt refl ORELSE' assume_tac ctxt ORELSE' rtac ctxt @{thm singletonI});
   33.13  
   33.14  fun mk_induct_leverage_prem_prems_tac ctxt nn kks fp_abs_inverses abs_inverses set_maps
   33.15      pre_set_defs =
   33.16 -  HEADGOAL (EVERY' (maps (fn kk => [select_prem_tac ctxt nn (dtac ctxt meta_spec) kk, etac ctxt meta_mp,
   33.17 +  HEADGOAL (EVERY' (maps (fn kk => [select_prem_tac ctxt nn (dtac ctxt meta_spec) kk,
   33.18 +    etac ctxt meta_mp,
   33.19      SELECT_GOAL (unfold_thms_tac ctxt (pre_set_defs @ fp_abs_inverses @ abs_inverses @ set_maps @
   33.20        sumprod_thms_set)),
   33.21      solve_prem_prem_tac ctxt]) (rev kks)));
   33.22 @@ -366,9 +368,10 @@
   33.23  fun mk_coinduct_discharge_prem_tac ctxt rel_eqs' nn kk n pre_rel_def fp_abs_inverse abs_inverse
   33.24      dtor_ctor exhaust ctr_defs discss selss =
   33.25    let val ks = 1 upto n in
   33.26 -    EVERY' ([rtac ctxt allI, rtac ctxt allI, rtac ctxt impI, select_prem_tac ctxt nn (dtac ctxt meta_spec) kk,
   33.27 -        dtac ctxt meta_spec, dtac ctxt meta_mp, assume_tac ctxt, rtac ctxt exhaust,
   33.28 -        K (co_induct_inst_as_projs_tac ctxt 0), hyp_subst_tac ctxt] @
   33.29 +    EVERY' ([rtac ctxt allI, rtac ctxt allI, rtac ctxt impI,
   33.30 +        select_prem_tac ctxt nn (dtac ctxt meta_spec) kk, dtac ctxt meta_spec, dtac ctxt meta_mp,
   33.31 +        assume_tac ctxt, rtac ctxt exhaust, K (co_induct_inst_as_projs_tac ctxt 0),
   33.32 +        hyp_subst_tac ctxt] @
   33.33        @{map 4} (fn k => fn ctr_def => fn discs => fn sels =>
   33.34          EVERY' ([rtac ctxt exhaust, K (co_induct_inst_as_projs_tac ctxt 1)] @
   33.35            map2 (fn k' => fn discs' =>
   33.36 @@ -435,8 +438,8 @@
   33.37          abs_inject :: ctor_defs @ nesting_rel_eqs @ simp_thms' @
   33.38          @{thms id_bnf_def rel_sum_simps rel_prod_apply vimage2p_def Inl_Inr_False
   33.39            iffD2[OF eq_False Inr_not_Inl] sum.inject prod.inject}) THEN
   33.40 -      REPEAT_DETERM (HEADGOAL ((REPEAT_DETERM o etac ctxt conjE) THEN' (REPEAT_DETERM o rtac ctxt conjI) THEN'
   33.41 -        (rtac ctxt refl ORELSE' assume_tac ctxt))))
   33.42 +      REPEAT_DETERM (HEADGOAL ((REPEAT_DETERM o etac ctxt conjE) THEN'
   33.43 +        (REPEAT_DETERM o rtac ctxt conjI) THEN' (rtac ctxt refl ORELSE' assume_tac ctxt))))
   33.44      cts assms exhausts discss selss ctor_defss dtor_ctors ctor_injects abs_injects rel_pre_defs
   33.45        abs_inverses);
   33.46  
   33.47 @@ -445,7 +448,8 @@
   33.48    rtac ctxt ctor_rel_induct 1 THEN EVERY (@{map 6} (fn cterm => fn exhaust => fn ctor_defs =>
   33.49        fn ctor_inject => fn rel_pre_list_def => fn Abs_inverse =>
   33.50          HEADGOAL (rtac ctxt exhaust THEN_ALL_NEW (rtac ctxt exhaust THEN_ALL_NEW
   33.51 -          (rtac ctxt (infer_instantiate' ctxt (replicate 4 NONE @ [SOME cterm]) @{thm arg_cong2} RS iffD2)
   33.52 +          (rtac ctxt (infer_instantiate' ctxt (replicate 4 NONE @ [SOME cterm]) @{thm arg_cong2}
   33.53 +              RS iffD2)
   33.54              THEN' assume_tac ctxt THEN' assume_tac ctxt THEN' TRY o resolve_tac ctxt assms))) THEN
   33.55          unfold_thms_tac ctxt (ctor_inject :: rel_pre_list_def :: ctor_defs @ nesting_rel_eqs @
   33.56            @{thms id_bnf_def vimage2p_def}) THEN
   33.57 @@ -485,12 +489,14 @@
   33.58        (rtac ctxt @{thm singletonI} ORELSE' assume_tac ctxt));
   33.59  
   33.60  fun mk_set_cases_tac ctxt ct assms exhaust sets =
   33.61 -  HEADGOAL (rtac ctxt (infer_instantiate' ctxt [SOME ct] exhaust) THEN_ALL_NEW hyp_subst_tac ctxt) THEN
   33.62 +  HEADGOAL (rtac ctxt (infer_instantiate' ctxt [SOME ct] exhaust)
   33.63 +    THEN_ALL_NEW hyp_subst_tac ctxt) THEN
   33.64    unfold_thms_tac ctxt sets THEN
   33.65    REPEAT_DETERM (HEADGOAL
   33.66      (eresolve_tac ctxt @{thms FalseE emptyE singletonE UnE UN_E insertE} ORELSE'
   33.67       hyp_subst_tac ctxt ORELSE'
   33.68 -     SELECT_GOAL (SOLVE (HEADGOAL (eresolve_tac ctxt assms THEN' REPEAT_DETERM o assume_tac ctxt)))));
   33.69 +     SELECT_GOAL (SOLVE (HEADGOAL (eresolve_tac ctxt assms THEN' REPEAT_DETERM o
   33.70 +       assume_tac ctxt)))));
   33.71  
   33.72  fun mk_set_intros_tac ctxt sets =
   33.73    TRYALL Goal.conjunction_tac THEN unfold_thms_tac ctxt sets THEN
   33.74 @@ -505,7 +511,8 @@
   33.75      val assms_tac =
   33.76        let val assms' = map (unfold_thms ctxt (@{thm id_bnf_def} :: ctor_defs)) assms in
   33.77          fold (curry (op ORELSE')) (map (fn thm =>
   33.78 -            funpow (length (Thm.prems_of thm)) (fn tac => tac THEN' assume_tac ctxt) (rtac ctxt thm)) assms')
   33.79 +            funpow (length (Thm.prems_of thm)) (fn tac => tac THEN' assume_tac ctxt)
   33.80 +              (rtac ctxt thm)) assms')
   33.81            (etac ctxt FalseE)
   33.82        end;
   33.83      val exhausts' = map (fn thm => thm RS @{thm asm_rl[of "P x y" for P x y]}) exhausts
   33.84 @@ -519,8 +526,8 @@
   33.85      unfold_thms_tac ctxt (Abs_pre_inverses @ dtor_ctors @ set_pre_defs @ ctor_defs @
   33.86        @{thms id_bnf_def o_apply sum_set_simps prod_set_simps UN_empty UN_insert Un_empty_left
   33.87          Un_empty_right empty_iff singleton_iff}) THEN
   33.88 -    REPEAT (HEADGOAL (hyp_subst_tac ctxt ORELSE' eresolve_tac ctxt @{thms UN_E UnE singletonE} ORELSE'
   33.89 -      assms_tac))
   33.90 +    REPEAT (HEADGOAL (hyp_subst_tac ctxt ORELSE'
   33.91 +      eresolve_tac ctxt @{thms UN_E UnE singletonE} ORELSE' assms_tac))
   33.92    end;
   33.93  
   33.94  end;
    34.1 --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Tue Dec 01 12:35:11 2015 +0100
    34.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Tue Dec 01 17:18:34 2015 +0100
    34.3 @@ -1009,8 +1009,8 @@
    34.4      |> map2 abs_curried_balanced arg_Tss
    34.5      |> (fn ts => Syntax.check_terms ctxt ts
    34.6        handle ERROR _ => nonprimitive_corec ctxt [])
    34.7 -    |> @{map 3} (fn b => fn mx => fn t => ((b, mx), ((Binding.concealed (Thm.def_binding b), []), t)))
    34.8 -      bs mxs
    34.9 +    |> @{map 3} (fn b => fn mx => fn t =>
   34.10 +      ((b, mx), ((Binding.concealed (Thm.def_binding b), []), t))) bs mxs
   34.11      |> rpair excludess'
   34.12    end;
   34.13  
   34.14 @@ -1037,7 +1037,8 @@
   34.15          val prems = maps (s_not_conj o #prems) disc_eqns;
   34.16          val ctr_rhs_opt = Option.map #ctr_rhs_opt sel_eqn_opt |> the_default NONE;
   34.17          val code_rhs_opt = Option.map #code_rhs_opt sel_eqn_opt |> the_default NONE;
   34.18 -        val eqn_pos = Option.map (curry (op +) 1 o #eqn_pos) sel_eqn_opt |> the_default 100000; (* FIXME *)
   34.19 +        val eqn_pos = Option.map (curry (op +) 1 o #eqn_pos) sel_eqn_opt
   34.20 +          |> the_default 100000; (* FIXME *)
   34.21  
   34.22          val extra_disc_eqn =
   34.23            {fun_name = fun_name, fun_T = fun_T, fun_args = fun_args, ctr = ctr, ctr_no = ctr_no,
   34.24 @@ -1307,7 +1308,8 @@
   34.25              Goal.prove_sorry lthy [] [] goal
   34.26                (fn {context = ctxt, prems = _} =>
   34.27                  mk_primcorec_sel_tac ctxt def_thms distincts split_sels split_sel_asms
   34.28 -                fp_nesting_maps fp_nesting_map_ident0s fp_nesting_map_comps corec_sel k m excludesss)
   34.29 +                  fp_nesting_maps fp_nesting_map_ident0s fp_nesting_map_comps corec_sel k m
   34.30 +                  excludesss)
   34.31              |> Thm.close_derivation
   34.32              |> `(is_some code_rhs_opt ? fold_thms lthy sel_defs) (*mildly too aggressive*)
   34.33              |> pair sel
   34.34 @@ -1444,7 +1446,8 @@
   34.35                        Goal.prove_sorry lthy [] [] raw_goal
   34.36                          (fn {context = ctxt, prems = _} =>
   34.37                            mk_primcorec_raw_code_tac ctxt distincts discIs split_sels split_sel_asms
   34.38 -                            ms ctr_thms (if exhaustive_code then try the_single nchotomys else NONE))
   34.39 +                            ms ctr_thms
   34.40 +                            (if exhaustive_code then try the_single nchotomys else NONE))
   34.41                        |> Thm.close_derivation;
   34.42                    in
   34.43                      Goal.prove_sorry lthy [] [] goal
    35.1 --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Tue Dec 01 12:35:11 2015 +0100
    35.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML	Tue Dec 01 17:18:34 2015 +0100
    35.3 @@ -72,7 +72,8 @@
    35.4  fun mk_primcorec_assumption_tac ctxt discIs =
    35.5    SELECT_GOAL (unfold_thms_tac ctxt @{thms fst_conv snd_conv not_not not_False_eq_True
    35.6        not_True_eq_False de_Morgan_conj de_Morgan_disj} THEN
    35.7 -    SOLVE (HEADGOAL (REPEAT o (rtac ctxt refl ORELSE' assume_tac ctxt ORELSE' etac ctxt conjE ORELSE'
    35.8 +    SOLVE (HEADGOAL (REPEAT o (rtac ctxt refl ORELSE' assume_tac ctxt ORELSE'
    35.9 +    etac ctxt conjE ORELSE'
   35.10      eresolve_tac ctxt falseEs ORELSE'
   35.11      resolve_tac ctxt @{thms TrueI conjI disjI1 disjI2} ORELSE'
   35.12      dresolve_tac ctxt discIs THEN' assume_tac ctxt ORELSE'
   35.13 @@ -137,7 +138,8 @@
   35.14      resolve_tac ctxt split_connectI ORELSE'
   35.15      Splitter.split_asm_tac ctxt (split_if_asm :: split_asms) ORELSE'
   35.16      Splitter.split_tac ctxt (split_if :: splits) ORELSE'
   35.17 -    eresolve_tac ctxt (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' assume_tac ctxt ORELSE'
   35.18 +    eresolve_tac ctxt (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN'
   35.19 +    assume_tac ctxt ORELSE'
   35.20      etac ctxt notE THEN' assume_tac ctxt ORELSE'
   35.21      (CHANGED o SELECT_GOAL (unfold_thms_tac ctxt (@{thms fst_conv snd_conv id_def comp_def split_def
   35.22           sum.case sum.sel sum.distinct[THEN eq_False[THEN iffD2]]} @
   35.23 @@ -148,7 +150,8 @@
   35.24  
   35.25  fun mk_primcorec_ctr_tac ctxt m collapse disc_fun_opt sel_funs =
   35.26    HEADGOAL (rtac ctxt ((if null sel_funs then collapse else collapse RS sym) RS trans) THEN'
   35.27 -    (the_default (K all_tac) (Option.map (rtac ctxt) disc_fun_opt)) THEN' REPEAT_DETERM_N m o assume_tac ctxt) THEN
   35.28 +    (the_default (K all_tac) (Option.map (rtac ctxt) disc_fun_opt)) THEN'
   35.29 +    REPEAT_DETERM_N m o assume_tac ctxt) THEN
   35.30    unfold_thms_tac ctxt (@{thm split_def} :: unfold_lets @ sel_funs) THEN HEADGOAL (rtac ctxt refl);
   35.31  
   35.32  fun inst_split_eq ctxt split =
    36.1 --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Tue Dec 01 12:35:11 2015 +0100
    36.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Tue Dec 01 17:18:34 2015 +0100
    36.3 @@ -458,7 +458,8 @@
    36.4      (recs, ctr_poss)
    36.5      |-> map2 (fn recx => fn ctr_pos => list_comb (recx, rec_args) |> permute_args ctr_pos)
    36.6      |> Syntax.check_terms ctxt
    36.7 -    |> @{map 3} (fn b => fn mx => fn t => ((b, mx), ((Binding.concealed (Thm.def_binding b), []), t)))
    36.8 +    |> @{map 3} (fn b => fn mx => fn t =>
    36.9 +        ((b, mx), ((Binding.concealed (Thm.def_binding b), []), t)))
   36.10        bs mxs
   36.11    end;
   36.12  
    37.1 --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML	Tue Dec 01 12:35:11 2015 +0100
    37.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML	Tue Dec 01 17:18:34 2015 +0100
    37.3 @@ -40,7 +40,8 @@
    37.4    | basic_lfp_sugars_of bs arg_Ts callers callssss0 lthy0 =
    37.5      let
    37.6        val ((missing_arg_Ts, perm0_kks,
    37.7 -            fp_sugars as {fp_nesting_bnfs, fp_co_induct_sugar = {common_co_inducts = [common_induct], ...}, ...} :: _,
    37.8 +            fp_sugars as {fp_nesting_bnfs,
    37.9 +              fp_co_induct_sugar = {common_co_inducts = [common_induct], ...}, ...} :: _,
   37.10              (lfp_sugar_thms, _)), lthy) =
   37.11          nested_to_mutual_fps (K true) Least_FP bs arg_Ts callers callssss0 lthy0;
   37.12  
    38.1 --- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Tue Dec 01 12:35:11 2015 +0100
    38.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Tue Dec 01 17:18:34 2015 +0100
    38.3 @@ -42,7 +42,8 @@
    38.4    Context.proof_map (Data.map (Symtab.update (T_name, (size_name, (size_simps, size_gen_o_maps)))));
    38.5  
    38.6  fun register_size_global T_name size_name size_simps size_gen_o_maps =
    38.7 -  Context.theory_map (Data.map (Symtab.update (T_name, (size_name, (size_simps, size_gen_o_maps)))));
    38.8 +  Context.theory_map
    38.9 +    (Data.map (Symtab.update (T_name, (size_name, (size_simps, size_gen_o_maps)))));
   38.10  
   38.11  val size_of = Symtab.lookup o Data.get o Context.Proof;
   38.12  val size_of_global = Symtab.lookup o Data.get o Context.Theory;
   38.13 @@ -70,8 +71,9 @@
   38.14  fun mk_size_neq ctxt cts exhaust sizes =
   38.15    HEADGOAL (rtac ctxt (infer_instantiate' ctxt (map SOME cts) exhaust)) THEN
   38.16    ALLGOALS (hyp_subst_tac ctxt) THEN
   38.17 -  Ctr_Sugar_Tactics.unfold_thms_tac ctxt (@{thm neq0_conv} :: sizes) THEN
   38.18 -  ALLGOALS (REPEAT_DETERM o (rtac ctxt @{thm zero_less_Suc} ORELSE' rtac ctxt @{thm trans_less_add2}));
   38.19 +  unfold_thms_tac ctxt (@{thm neq0_conv} :: sizes) THEN
   38.20 +  ALLGOALS (REPEAT_DETERM o (rtac ctxt @{thm zero_less_Suc} ORELSE'
   38.21 +    rtac ctxt @{thm trans_less_add2}));
   38.22  
   38.23  fun generate_datatype_size (fp_sugars as ({T = Type (_, As), BT = Type (_, Bs), fp = Least_FP,
   38.24          fp_res = {bnfs = fp_bnfs, ...}, fp_nesting_bnfs, live_nesting_bnfs, ...} : fp_sugar) :: _)
   38.25 @@ -236,7 +238,8 @@
   38.26          (Spec_Rules.retrieve lthy0 @{const size ('a)}
   38.27           |> map_filter (try (fn (Spec_Rules.Equational, (_, [thm])) => thm)));
   38.28  
   38.29 -      val nested_size_maps = map (mk_pointful lthy2) nested_size_gen_o_maps @ nested_size_gen_o_maps;
   38.30 +      val nested_size_maps =
   38.31 +        map (mk_pointful lthy2) nested_size_gen_o_maps @ nested_size_gen_o_maps;
   38.32        val all_inj_maps =
   38.33          @{thm prod.inj_map} :: map inj_map_of_bnf (fp_bnfs @ fp_nesting_bnfs @ live_nesting_bnfs)
   38.34          |> distinct Thm.eq_thm_prop;
    39.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Tue Dec 01 12:35:11 2015 +0100
    39.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Tue Dec 01 17:18:34 2015 +0100
    39.3 @@ -50,8 +50,8 @@
    39.4    val ctr_sugars_of_global: theory -> ctr_sugar list
    39.5    val ctr_sugar_of_case: Proof.context -> string -> ctr_sugar option
    39.6    val ctr_sugar_of_case_global: theory -> string -> ctr_sugar option
    39.7 -  val ctr_sugar_interpretation: string ->
    39.8 -    (ctr_sugar -> local_theory -> local_theory) -> theory -> theory
    39.9 +  val ctr_sugar_interpretation: string -> (ctr_sugar -> local_theory -> local_theory) -> theory ->
   39.10 +    theory
   39.11    val interpret_ctr_sugar: (string -> bool) -> ctr_sugar -> local_theory -> local_theory
   39.12    val register_ctr_sugar_raw: ctr_sugar -> local_theory -> local_theory
   39.13    val register_ctr_sugar: (string -> bool) -> ctr_sugar -> local_theory -> local_theory
    40.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML	Tue Dec 01 12:35:11 2015 +0100
    40.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML	Tue Dec 01 17:18:34 2015 +0100
    40.3 @@ -54,7 +54,8 @@
    40.4  
    40.5  fun mk_nchotomy_tac ctxt n exhaust =
    40.6    HEADGOAL (rtac ctxt allI THEN' rtac ctxt exhaust THEN'
    40.7 -    EVERY' (maps (fn k => [rtac ctxt (mk_disjIN n k), REPEAT_DETERM o rtac ctxt exI, assume_tac ctxt])
    40.8 +    EVERY' (maps (fn k =>
    40.9 +        [rtac ctxt (mk_disjIN n k), REPEAT_DETERM o rtac ctxt exI, assume_tac ctxt])
   40.10        (1 upto n)));
   40.11  
   40.12  fun mk_unique_disc_def_tac ctxt m uexhaust =
   40.13 @@ -114,7 +115,8 @@
   40.14    else
   40.15      let val ks = 1 upto n in
   40.16        HEADGOAL (rtac ctxt uexhaust_disc THEN'
   40.17 -        EVERY' (@{map 5} (fn k => fn m => fn distinct_discss => fn distinct_discss' => fn uuncollapse =>
   40.18 +        EVERY' (@{map 5} (fn k => fn m => fn distinct_discss => fn distinct_discss' =>
   40.19 +            fn uuncollapse =>
   40.20            EVERY' [rtac ctxt (uuncollapse RS trans) THEN'
   40.21              TRY o assume_tac ctxt, rtac ctxt sym, rtac ctxt vexhaust_disc,
   40.22              EVERY' (@{map 4} (fn k' => fn distinct_discs => fn distinct_discs' => fn vuncollapse =>
   40.23 @@ -124,13 +126,17 @@
   40.24                     (if m = 0 then
   40.25                        [rtac ctxt refl]
   40.26                      else
   40.27 -                      [if n = 1 then K all_tac
   40.28 -                       else EVERY' [dtac ctxt meta_mp, assume_tac ctxt, dtac ctxt meta_mp, assume_tac ctxt],
   40.29 -                       REPEAT_DETERM_N (Int.max (0, m - 1)) o etac ctxt conjE,
   40.30 -                       asm_simp_tac (ss_only [] ctxt)])
   40.31 +                      [if n = 1 then
   40.32 +                         K all_tac
   40.33 +                       else
   40.34 +                         EVERY' [dtac ctxt meta_mp, assume_tac ctxt, dtac ctxt meta_mp,
   40.35 +                           assume_tac ctxt],
   40.36 +                         REPEAT_DETERM_N (Int.max (0, m - 1)) o etac ctxt conjE,
   40.37 +                         asm_simp_tac (ss_only [] ctxt)])
   40.38                   else
   40.39                     [dtac ctxt (the_single (if k = n then distinct_discs else distinct_discs')),
   40.40 -                    etac ctxt (if k = n then @{thm iff_contradict(1)} else @{thm iff_contradict(2)}),
   40.41 +                    etac ctxt (if k = n then @{thm iff_contradict(1)}
   40.42 +                      else @{thm iff_contradict(2)}),
   40.43                      assume_tac ctxt, assume_tac ctxt]))
   40.44                ks distinct_discss distinct_discss' uncollapses)])
   40.45            ks ms distinct_discsss distinct_discsss' uncollapses))
   40.46 @@ -152,8 +158,8 @@
   40.47      val ks = 1 upto n;
   40.48    in
   40.49      HEADGOAL (rtac ctxt (case_def' RS trans) THEN' rtac ctxt @{thm the_equality} THEN'
   40.50 -      rtac ctxt (mk_disjIN n k) THEN' REPEAT_DETERM o rtac ctxt exI THEN' rtac ctxt conjI THEN' rtac ctxt refl THEN'
   40.51 -      rtac ctxt refl THEN'
   40.52 +      rtac ctxt (mk_disjIN n k) THEN' REPEAT_DETERM o rtac ctxt exI THEN' rtac ctxt conjI THEN'
   40.53 +      rtac ctxt refl THEN' rtac ctxt refl THEN'
   40.54        EVERY' (map2 (fn k' => fn distincts =>
   40.55          (if k' < n then etac ctxt disjE else K all_tac) THEN'
   40.56          (if k' = k then mk_case_same_ctr_tac ctxt injects
   40.57 @@ -182,7 +188,8 @@
   40.58         simp_tac (ss_only (@{thms simp_thms} @ cases @ nth selss (k - 1) @ nth injectss (k - 1) @
   40.59           flat (nth distinctsss (k - 1))) ctxt)) k) THEN
   40.60      ALLGOALS (etac ctxt thin_rl THEN' rtac ctxt iffI THEN'
   40.61 -      REPEAT_DETERM o rtac ctxt allI THEN' rtac ctxt impI THEN' REPEAT_DETERM o etac ctxt conjE THEN'
   40.62 +      REPEAT_DETERM o rtac ctxt allI THEN' rtac ctxt impI THEN'
   40.63 +      REPEAT_DETERM o etac ctxt conjE THEN'
   40.64        hyp_subst_tac ctxt THEN' assume_tac ctxt THEN'
   40.65        REPEAT_DETERM o etac ctxt allE THEN' etac ctxt impE THEN'
   40.66        REPEAT_DETERM o (rtac ctxt conjI THEN' rtac ctxt refl) THEN'
    41.1 --- a/src/HOL/Tools/Transfer/transfer_bnf.ML	Tue Dec 01 12:35:11 2015 +0100
    41.2 +++ b/src/HOL/Tools/Transfer/transfer_bnf.ML	Tue Dec 01 17:18:34 2015 +0100
    41.3 @@ -66,11 +66,6 @@
    41.4  
    41.5  fun bnf_of_fp_sugar (fp_sugar:fp_sugar) = nth (#bnfs (#fp_res fp_sugar)) (#fp_res_index fp_sugar)
    41.6  
    41.7 -fun fp_sugar_only_type_ctr f fp_sugars =
    41.8 -  (case filter (is_Type o T_of_bnf o bnf_of_fp_sugar) fp_sugars of
    41.9 -    [] => I
   41.10 -  | fp_sugars' => f fp_sugars')
   41.11 -
   41.12  (* relation constraints - bi_total & co. *)
   41.13  
   41.14  fun mk_relation_constraint name arg =
   41.15 @@ -410,7 +405,7 @@
   41.16  
   41.17  fun transfer_fp_sugars_interpretation fp_sugar lthy =
   41.18    let
   41.19 -    val lthy = pred_injects fp_sugar lthy
   41.20 +    val lthy = lthy |> (is_Type o T_of_bnf o bnf_of_fp_sugar) fp_sugar ? pred_injects fp_sugar
   41.21      val transfer_rules_notes = fp_sugar_transfer_rules fp_sugar
   41.22    in
   41.23      lthy
   41.24 @@ -419,7 +414,6 @@
   41.25    end
   41.26  
   41.27  val _ =
   41.28 -  Theory.setup (fp_sugars_interpretation transfer_plugin
   41.29 -    (fp_sugar_only_type_ctr (fold transfer_fp_sugars_interpretation)))
   41.30 +  Theory.setup (fp_sugars_interpretation transfer_plugin (fold transfer_fp_sugars_interpretation))
   41.31  
   41.32  end
    42.1 --- a/src/HOL/Transcendental.thy	Tue Dec 01 12:35:11 2015 +0100
    42.2 +++ b/src/HOL/Transcendental.thy	Tue Dec 01 17:18:34 2015 +0100
    42.3 @@ -10,6 +10,16 @@
    42.4  imports Binomial Series Deriv NthRoot
    42.5  begin
    42.6  
    42.7 +lemma of_int_leD: 
    42.8 +  fixes x :: "'a :: linordered_idom"
    42.9 +  shows "\<bar>of_int n\<bar> \<le> x \<Longrightarrow> n=0 \<or> x\<ge>1"
   42.10 +  by (metis (no_types) le_less_trans not_less of_int_abs of_int_less_1_iff zabs_less_one_iff)
   42.11 +
   42.12 +lemma of_int_lessD: 
   42.13 +  fixes x :: "'a :: linordered_idom"
   42.14 +  shows "\<bar>of_int n\<bar> < x \<Longrightarrow> n=0 \<or> x>1"
   42.15 +  by (metis less_le_trans not_less of_int_abs of_int_less_1_iff zabs_less_one_iff)
   42.16 +
   42.17  lemma fact_in_Reals: "fact n \<in> \<real>" by (induction n) auto
   42.18  
   42.19  lemma pochhammer_of_real: "pochhammer (of_real x) n = of_real (pochhammer x n)"
   42.20 @@ -1979,8 +1989,7 @@
   42.21        assume "x \<le> y" "y \<le> a"
   42.22        with \<open>0 < x\<close> \<open>a < 1\<close> have "0 < 1 / y - 1" "0 < y"
   42.23          by (auto simp: field_simps)
   42.24 -      with D show "\<exists>z. DERIV ?l y :> z \<and> 0 < z"
   42.25 -        by auto
   42.26 +      with D show "\<exists>z. DERIV ?l y :> z \<and> 0 < z" by blast
   42.27      qed
   42.28      also have "\<dots> \<le> 0"
   42.29        using ln_le_minus_one \<open>0 < x\<close> \<open>x < a\<close> by (auto simp: field_simps)
   42.30 @@ -3090,6 +3099,11 @@
   42.31    using cos_add [where x=x and y=x]
   42.32    by (simp add: power2_eq_square)
   42.33  
   42.34 +lemma sin_cos_le1:
   42.35 +  fixes x::real shows "abs (sin x * sin y + cos x * cos y) \<le> 1"
   42.36 +  using cos_diff [of x y]
   42.37 +  by (metis abs_cos_le_one add.commute)
   42.38 +
   42.39  lemma DERIV_fun_pow: "DERIV g x :> m ==>
   42.40        DERIV (\<lambda>x. (g x) ^ n) x :> real n * (g x) ^ (n - 1) * m"
   42.41    by (auto intro!: derivative_eq_intros simp:)
    43.1 --- a/src/HOL/ex/Dedekind_Real.thy	Tue Dec 01 12:35:11 2015 +0100
    43.2 +++ b/src/HOL/ex/Dedekind_Real.thy	Tue Dec 01 17:18:34 2015 +0100
    43.3 @@ -784,8 +784,7 @@
    43.4      qed
    43.5      hence "y < r" by simp
    43.6      with ypos have  dless: "?d < (r * ?d)/y"
    43.7 -      by (simp add: pos_less_divide_eq mult.commute [of ?d]
    43.8 -                    mult_strict_right_mono dpos)
    43.9 +      using dpos less_divide_eq_1 by fastforce
   43.10      have "r + ?d < r*x"
   43.11      proof -
   43.12        have "r + ?d < r + (r * ?d)/y" by (simp add: dless)
    44.1 --- a/src/HOL/ex/Sqrt.thy	Tue Dec 01 12:35:11 2015 +0100
    44.2 +++ b/src/HOL/ex/Sqrt.thy	Tue Dec 01 17:18:34 2015 +0100
    44.3 @@ -14,7 +14,7 @@
    44.4    assumes "prime (p::nat)"
    44.5    shows "sqrt p \<notin> \<rat>"
    44.6  proof
    44.7 -  from \<open>prime p\<close> have p: "1 < p" by (simp add: prime_nat_def)
    44.8 +  from \<open>prime p\<close> have p: "1 < p" by (simp add: prime_def)
    44.9    assume "sqrt p \<in> \<rat>"
   44.10    then obtain m n :: nat where
   44.11        n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt p\<bar> = m / n"
   44.12 @@ -59,7 +59,7 @@
   44.13    assumes "prime (p::nat)"
   44.14    shows "sqrt p \<notin> \<rat>"
   44.15  proof
   44.16 -  from \<open>prime p\<close> have p: "1 < p" by (simp add: prime_nat_def)
   44.17 +  from \<open>prime p\<close> have p: "1 < p" by (simp add: prime_def)
   44.18    assume "sqrt p \<in> \<rat>"
   44.19    then obtain m n :: nat where
   44.20        n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt p\<bar> = m / n"
    45.1 --- a/src/HOL/ex/Sqrt_Script.thy	Tue Dec 01 12:35:11 2015 +0100
    45.2 +++ b/src/HOL/ex/Sqrt_Script.thy	Tue Dec 01 17:18:34 2015 +0100
    45.3 @@ -17,7 +17,7 @@
    45.4  subsection \<open>Preliminaries\<close>
    45.5  
    45.6  lemma prime_nonzero:  "prime (p::nat) \<Longrightarrow> p \<noteq> 0"
    45.7 -  by (force simp add: prime_nat_def)
    45.8 +  by (force simp add: prime_def)
    45.9  
   45.10  lemma prime_dvd_other_side:
   45.11      "(n::nat) * n = p * (k * k) \<Longrightarrow> prime p \<Longrightarrow> p dvd n"
   45.12 @@ -32,7 +32,7 @@
   45.13    apply (erule disjE)
   45.14     apply (frule mult_le_mono, assumption)
   45.15     apply auto
   45.16 -  apply (force simp add: prime_nat_def)
   45.17 +  apply (force simp add: prime_def)
   45.18    done
   45.19  
   45.20  lemma rearrange: "(j::nat) * (p * j) = k * k \<Longrightarrow> k * k = p * (j * j)"