# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1654698987 -3600
# Node ID 1910054f8c391056f58b4deba7a1e486a51d50e1
# Parent  47abacd97f7b58cd97ebd516723d21840bfc1b15
some additional lemmas and a little tidying up

diff -r 47abacd97f7b -r 1910054f8c39 src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Wed Jun 08 09:19:57 2022 +0200
+++ b/src/HOL/Complex.thy	Wed Jun 08 15:36:27 2022 +0100
@@ -279,12 +279,7 @@
 lemma imaginary_eq_real_iff [simp]:
   assumes "y \<in> Reals" "x \<in> Reals"
   shows "\<i> * y = x \<longleftrightarrow> x=0 \<and> y=0"
-    using assms
-    unfolding Reals_def
-    apply clarify
-      apply (rule iffI)
-    apply (metis Im_complex_of_real Im_i_times Re_complex_of_real mult_eq_0_iff of_real_0)
-    by simp
+  by (metis Im_complex_of_real Im_i_times assms mult_zero_right of_real_0 of_real_Re)
 
 lemma real_eq_imaginary_iff [simp]:
   assumes "y \<in> Reals" "x \<in> Reals"
@@ -355,11 +350,7 @@
   by (simp add: norm_complex_def)
 
 lemma cmod_le: "cmod z \<le> \<bar>Re z\<bar> + \<bar>Im z\<bar>"
-  apply (subst complex_eq)
-  apply (rule order_trans)
-   apply (rule norm_triangle_ineq)
-  apply (simp add: norm_mult)
-  done
+  using norm_complex_def sqrt_sum_squares_le_sum_abs by presburger
 
 lemma cmod_eq_Re: "Im z = 0 \<Longrightarrow> cmod z = \<bar>Re z\<bar>"
   by (simp add: norm_complex_def)
@@ -412,6 +403,7 @@
 
 subsection \<open>Absolute value\<close>
 
+
 instantiation complex :: field_abs_sgn
 begin
 
@@ -419,11 +411,7 @@
   where "abs_complex = of_real \<circ> norm"
 
 instance
-  apply standard
-         apply (auto simp add: abs_complex_def complex_sgn_def norm_mult)
-  apply (auto simp add: scaleR_conv_of_real field_simps)
-  done
-
+  proof qed (auto simp add: abs_complex_def complex_sgn_def norm_divide norm_mult scaleR_conv_of_real field_simps)
 end
 
 
@@ -449,6 +437,8 @@
 lemmas has_derivative_Im [derivative_intros] = bounded_linear.has_derivative[OF bounded_linear_Im]
 lemmas sums_Re = bounded_linear.sums [OF bounded_linear_Re]
 lemmas sums_Im = bounded_linear.sums [OF bounded_linear_Im]
+lemmas Re_suminf = bounded_linear.suminf[OF bounded_linear_Re]
+lemmas Im_suminf = bounded_linear.suminf[OF bounded_linear_Im]
 
 lemma tendsto_Complex [tendsto_intros]:
   "(f \<longlongrightarrow> a) F \<Longrightarrow> (g \<longlongrightarrow> b) F \<Longrightarrow> ((\<lambda>x. Complex (f x) (g x)) \<longlongrightarrow> Complex a b) F"
@@ -781,13 +771,7 @@
   have g: "\<And>n. cmod (g n) = Re (g n)"
     using assms by (metis abs_of_nonneg in_Reals_norm)
   show ?thesis
-    apply (rule summable_comparison_test' [where g = "\<lambda>n. norm (g n)" and N=N])
-    using sg
-     apply (auto simp: summable_def)
-     apply (rule_tac x = "Re s" in exI)
-     apply (auto simp: g sums_Re)
-    apply (metis fg g)
-    done
+    by (metis fg g sg summable_comparison_test summable_complex_iff)
 qed
 
 
@@ -939,11 +923,7 @@
   by (simp add: cis.code cmod_complex_polar exp_eq_polar Complex_eq)
 
 lemma complex_exp_exists: "\<exists>a r. z = complex_of_real r * exp a"
-  apply (insert rcis_Ex [of z])
-  apply (auto simp add: exp_eq_polar rcis_def mult.assoc [symmetric])
-  apply (rule_tac x = "\<i> * complex_of_real a" in exI)
-  apply auto
-  done
+  using cis_conv_exp rcis_Ex rcis_def by force
 
 lemma exp_pi_i [simp]: "exp (of_real pi * \<i>) = -1"
   by (metis cis_conv_exp cis_pi mult.commute)
diff -r 47abacd97f7b -r 1910054f8c39 src/HOL/Real.thy
--- a/src/HOL/Real.thy	Wed Jun 08 09:19:57 2022 +0200
+++ b/src/HOL/Real.thy	Wed Jun 08 15:36:27 2022 +0100
@@ -1404,6 +1404,20 @@
 lemma of_int_floor_cancel [simp]: "of_int \<lfloor>x\<rfloor> = x \<longleftrightarrow> (\<exists>n::int. x = of_int n)"
   by (metis floor_of_int)
 
+lemma of_int_floor [simp]: "a \<in> \<int> \<Longrightarrow> of_int (floor a) = a"
+  by (metis Ints_cases of_int_floor_cancel) 
+
+lemma floor_frac [simp]: "\<lfloor>frac r\<rfloor> = 0"
+  by (simp add: frac_def)
+
+lemma frac_1 [simp]: "frac 1 = 0"
+  by (simp add: frac_def)
+
+lemma frac_in_Rats_iff [simp]:
+  fixes r::"'a::{floor_ceiling,field_char_0}"
+  shows "frac r \<in> \<rat> \<longleftrightarrow> r \<in> \<rat>"
+  by (metis Rats_add Rats_diff Rats_of_int diff_add_cancel frac_def)
+
 lemma floor_eq: "real_of_int n < x \<Longrightarrow> x < real_of_int n + 1 \<Longrightarrow> \<lfloor>x\<rfloor> = n"
   by linarith
 
@@ -1480,6 +1494,9 @@
 lemma of_int_ceiling_cancel [simp]: "of_int \<lceil>x\<rceil> = x \<longleftrightarrow> (\<exists>n::int. x = of_int n)"
   using ceiling_of_int by metis
 
+lemma of_int_ceiling [simp]: "a \<in> \<int> \<Longrightarrow> of_int (ceiling a) = a"
+  by (metis Ints_cases of_int_ceiling_cancel) 
+
 lemma ceiling_eq: "of_int n < x \<Longrightarrow> x \<le> of_int n + 1 \<Longrightarrow> \<lceil>x\<rceil> = n + 1"
   by (simp add: ceiling_unique)
 
diff -r 47abacd97f7b -r 1910054f8c39 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Wed Jun 08 09:19:57 2022 +0200
+++ b/src/HOL/Rings.thy	Wed Jun 08 15:36:27 2022 +0100
@@ -2714,6 +2714,9 @@
 lemma abs_mult_pos: "0 \<le> x \<Longrightarrow> \<bar>y\<bar> * x = \<bar>y * x\<bar>"
   by (simp add: abs_mult)
 
+lemma abs_mult_pos': "0 \<le> x \<Longrightarrow> x * \<bar>y\<bar> = \<bar>x * y\<bar>"
+  by (simp add: abs_mult)
+
 lemma abs_diff_less_iff: "\<bar>x - a\<bar> < r \<longleftrightarrow> a - r < x \<and> x < a + r"
   by (auto simp add: diff_less_eq ac_simps abs_less_iff)
 
diff -r 47abacd97f7b -r 1910054f8c39 src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Wed Jun 08 09:19:57 2022 +0200
+++ b/src/HOL/Set_Interval.thy	Wed Jun 08 15:36:27 2022 +0100
@@ -111,12 +111,10 @@
   by (auto simp add: greaterThan_def atMost_def)
 
 lemma Compl_atMost [simp]: "!!k:: 'a::linorder. -atMost k = greaterThan k"
-  apply (subst Compl_greaterThan [symmetric])
-  apply (rule double_complement)
-  done
+  by (metis Compl_greaterThan double_complement)
 
 lemma (in ord) atLeast_iff [iff]: "(i \<in> atLeast k) = (k<=i)"
-by (simp add: atLeast_def)
+  by (simp add: atLeast_def)
 
 lemma Compl_atLeast [simp]: "!!k:: 'a::linorder. -atLeast k = lessThan k"
   by (auto simp add: lessThan_def atLeast_def)
@@ -142,15 +140,15 @@
   by auto
 
 lemma atLeast_subset_iff [iff]:
-     "(atLeast x \<subseteq> atLeast y) = (y \<le> (x::'a::preorder))"
-by (blast intro: order_trans)
+  "(atLeast x \<subseteq> atLeast y) = (y \<le> (x::'a::preorder))"
+  by (blast intro: order_trans)
 
 lemma atLeast_eq_iff [iff]:
-     "(atLeast x = atLeast y) = (x = (y::'a::order))"
-by (blast intro: order_antisym order_trans)
+  "(atLeast x = atLeast y) = (x = (y::'a::order))"
+  by (blast intro: order_antisym order_trans)
 
 lemma greaterThan_subset_iff [iff]:
-     "(greaterThan x \<subseteq> greaterThan y) = (y \<le> (x::'a::linorder))"
+  "(greaterThan x \<subseteq> greaterThan y) = (y \<le> (x::'a::linorder))"
   unfolding greaterThan_def by (auto simp: linorder_not_less [symmetric])
 
 lemma greaterThan_eq_iff [iff]:
@@ -305,6 +303,10 @@
   "{l..h} = {l'..h'} = (l=l' \<and> h=h' \<or> \<not> l\<le>h \<and> \<not> l'\<le>h')"
   by (simp add: order_class.order.eq_iff) (auto intro: order_trans)
 
+lemma (in linorder) Ico_eq_Ico:
+  "{l..<h} = {l'..<h'} = (l=l' \<and> h=h' \<or> \<not> l<h \<and> \<not> l'<h')"
+  by (metis atLeastLessThan_empty_iff2 nle_le not_less ord.atLeastLessThan_iff)
+
 lemma atLeastAtMost_singleton_iff[simp]:
   "{a .. b} = {c} \<longleftrightarrow> a = b \<and> b = c"
 proof