src/HOL/Transcendental.thy

   by (simp add: cosh_def scaleR_conv_of_real)
 
 
 subsubsection \<open>More specific properties of the real functions\<close>
 
-lemma sinh_real_zero_iff [simp]: "sinh (x::real) = 0 \<longleftrightarrow> x = 0"
-proof -
-  have "(-1 :: real) < 0" by simp
-  also have "0 < exp x" by simp
-  finally have "exp x \<noteq> -1" by (intro notI) simp
-  thus ?thesis by (subst sinh_zero_iff) simp
-qed
-
 lemma plus_inverse_ge_2:
   fixes x :: real
   assumes "x > 0"
   shows   "x + inverse x \<ge> 2"
 proof -

 lemma cosh_real_nonneg[simp]: "cosh (x :: real) \<ge> 0"
   using cosh_real_ge_1[of x] by simp
 
 lemma cosh_real_nonzero [simp]: "cosh (x :: real) \<noteq> 0"
   using cosh_real_ge_1[of x] by simp
-
-lemma tanh_real_nonneg_iff [simp]: "tanh (x :: real) \<ge> 0 \<longleftrightarrow> x \<ge> 0"
-  by (simp add: tanh_def field_simps)
-
-lemma tanh_real_pos_iff [simp]: "tanh (x :: real) > 0 \<longleftrightarrow> x > 0"
-  by (simp add: tanh_def field_simps)
-
-lemma tanh_real_nonpos_iff [simp]: "tanh (x :: real) \<le> 0 \<longleftrightarrow> x \<le> 0"
-  by (simp add: tanh_def field_simps)
-
-lemma tanh_real_neg_iff [simp]: "tanh (x :: real) < 0 \<longleftrightarrow> x < 0"
-  by (simp add: tanh_def field_simps)
-
-lemma tanh_real_zero_iff [simp]: "tanh (x :: real) = 0 \<longleftrightarrow> x = 0"
-  by (simp add: tanh_def field_simps)
 
 lemma arsinh_real_def: "arsinh (x::real) = ln (x + sqrt (x^2 + 1))"
   by (simp add: arsinh_def powr_half_sqrt)
 
 lemma arcosh_real_def: "x \<ge> 1 \<Longrightarrow> arcosh (x::real) = ln (x + sqrt (x^2 - 1))"

     by (simp add: cosh_plus_sinh cosh_minus_sinh exp_minus field_simps power2_eq_square)
   also have "ln ((exp x)^2) / 2 = x" by (simp add: ln_realpow)
   finally show ?thesis .
 qed
 
+lemma sinh_real_zero_iff [simp]: "sinh x = 0 \<longleftrightarrow> x = 0"
+  by (metis arsinh_0 arsinh_sinh_real sinh_0)
+
+lemma cosh_real_one_iff [simp]: "cosh x = 1 \<longleftrightarrow> x = 0"
+  by (smt (verit, best) Transcendental.arcosh_cosh_real cosh_0 cosh_minus)
+
+lemma tanh_real_nonneg_iff [simp]: "tanh x \<ge> 0 \<longleftrightarrow> x \<ge> 0"
+  by (simp add: tanh_def field_simps)
+
+lemma tanh_real_pos_iff [simp]: "tanh x > 0 \<longleftrightarrow> x > 0"
+  by (simp add: tanh_def field_simps)
+
+lemma tanh_real_nonpos_iff [simp]: "tanh x \<le> 0 \<longleftrightarrow> x \<le> 0"
+  by (simp add: tanh_def field_simps)
+
+lemma tanh_real_neg_iff [simp]: "tanh x < 0 \<longleftrightarrow> x < 0"
+  by (simp add: tanh_def field_simps)
+
+lemma tanh_real_zero_iff [simp]: "tanh x = 0 \<longleftrightarrow> x = 0"
+  by (simp add: tanh_def field_simps)
+
 end
-
+  
 lemma sinh_real_strict_mono: "strict_mono (sinh :: real \<Rightarrow> real)"
   by (rule pos_deriv_imp_strict_mono derivative_intros)+ auto
 
 lemma cosh_real_strict_mono:
   assumes "0 \<le> x" and "x < (y::real)"