# HG changeset patch
# User immler
# Date 1517815819 -3600
# Node ID ed0a7090167d21d0af2f5a735b9389920e3d6349
# Parent  a93cf1d6ba87e1a227aa80bdacf4443bf795efc0
added lemmas, avoid 'float_of 0'

diff -r a93cf1d6ba87 -r ed0a7090167d src/HOL/Decision_Procs/Approximation_Bounds.thy
--- a/src/HOL/Decision_Procs/Approximation_Bounds.thy	Sat Feb 03 20:46:28 2018 +0100
+++ b/src/HOL/Decision_Procs/Approximation_Bounds.thy	Mon Feb 05 08:30:19 2018 +0100
@@ -305,8 +305,7 @@
     case (Float m e)
     hence "0 < m"
       using assms
-      apply (auto simp: sign_simps)
-      by (meson not_less powr_ge_pzero)
+      by (auto simp: sign_simps)
     hence "0 < sqrt m" by auto
 
     have int_nat_bl: "(nat (bitlen m)) = bitlen m"
@@ -1190,7 +1189,7 @@
 next
   case True
   hence "x = 0"
-    by transfer
+    by (simp add: real_of_float_eq)
   thus ?thesis
     using lb_sin_cos_aux_zero_le_one one_le_ub_sin_cos_aux
     by simp
@@ -1478,7 +1477,7 @@
         by auto
 
       have eq_4: "?x2 * Float 1 (- 1) = x * Float 1 (- 2)"
-        by transfer simp
+        by (auto simp: real_of_float_eq)
 
       have "(?lb x) \<le> ?cos x"
       proof -
@@ -2334,11 +2333,7 @@
     using \<open>real_of_float (float_divr prec 1 x) < 1\<close> by auto
 qed
 
-lemma float_pos_eq_mantissa_pos: "x > 0 \<longleftrightarrow> mantissa x > 0"
-  apply (subst Float_mantissa_exponent[of x, symmetric])
-  apply (auto simp add: zero_less_mult_iff zero_float_def  dest: less_zeroE)
-  apply (metis not_le powr_ge_pzero)
-  done
+lemmas float_pos_eq_mantissa_pos = mantissa_pos_iff[symmetric]
 
 lemma Float_pos_eq_mantissa_pos: "Float m e > 0 \<longleftrightarrow> m > 0"
   using powr_gt_zero[of 2 "e"]
@@ -2346,7 +2341,7 @@
 
 lemma Float_representation_aux:
   fixes m e
-  defines "x \<equiv> Float m e"
+  defines [THEN meta_eq_to_obj_eq]: "x \<equiv> Float m e"
   assumes "x > 0"
   shows "Float (exponent x + (bitlen (mantissa x) - 1)) 0 = Float (e + (bitlen m - 1)) 0" (is ?th1)
     and "Float (mantissa x) (- (bitlen (mantissa x) - 1)) = Float m ( - (bitlen m - 1))"  (is ?th2)
@@ -2356,9 +2351,10 @@
   thus ?th1
     using bitlen_Float[of m e] assms
     by (auto simp add: zero_less_mult_iff intro!: arg_cong2[where f=Float])
-  have "x \<noteq> float_of 0"
+  have "x \<noteq> 0"
     unfolding zero_float_def[symmetric] using \<open>0 < x\<close> by auto
-  from denormalize_shift[OF assms(1) this] guess i . note i = this
+  from denormalize_shift[OF x_def this] obtain i where
+    i: "m = mantissa x * 2 ^ i" "e = exponent x - int i" .
 
   have "2 powr (1 - (real_of_int (bitlen (mantissa x)) + real_of_int i)) =
     2 powr (1 - (real_of_int (bitlen (mantissa x)))) * inverse (2 powr (real i))"
@@ -2367,7 +2363,8 @@
     (real_of_int (mantissa x) * 2 ^ i) * 2 powr (1 - real_of_int (bitlen (mantissa x * 2 ^ i)))"
     using \<open>mantissa x > 0\<close> by (simp add: powr_realpow)
   then show ?th2
-    unfolding i by transfer auto
+    unfolding i
+    by (auto simp: real_of_float_eq)
 qed
 
 lemma compute_ln[code]:
@@ -2541,9 +2538,7 @@
     let ?x = "Float m (- (bitlen m - 1))"
 
     have "0 < m" and "m \<noteq> 0" using \<open>0 < x\<close> Float powr_gt_zero[of 2 e]
-      apply (auto simp add: zero_less_mult_iff)
-      using not_le powr_ge_pzero apply blast
-      done
+      by (auto simp add: zero_less_mult_iff)
     define bl where "bl = bitlen m - 1"
     hence "bl \<ge> 0"
       using \<open>m > 0\<close> by (simp add: bitlen_alt_def)
diff -r a93cf1d6ba87 -r ed0a7090167d src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Sat Feb 03 20:46:28 2018 +0100
+++ b/src/HOL/Library/Float.thy	Mon Feb 05 08:30:19 2018 +0100
@@ -300,8 +300,8 @@
   "rel_fun (=) pcr_float (- numeral :: _ \<Rightarrow> real) (- numeral :: _ \<Rightarrow> float)"
   by (simp add: rel_fun_def float.pcr_cr_eq cr_float_def)
 
-lemma float_of_numeral[simp]: "numeral k = float_of (numeral k)"
-  and float_of_neg_numeral[simp]: "- numeral k = float_of (- numeral k)"
+lemma float_of_numeral: "numeral k = float_of (numeral k)"
+  and float_of_neg_numeral: "- numeral k = float_of (- numeral k)"
   unfolding real_of_float_eq by simp_all
 
 
@@ -445,8 +445,8 @@
     snd (SOME p::int \<times> int. (f = 0 \<and> fst p = 0 \<and> snd p = 0) \<or>
       (f \<noteq> 0 \<and> real_of_float f = real_of_int (fst p) * 2 powr real_of_int (snd p) \<and> \<not> 2 dvd fst p))"
 
-lemma exponent_0[simp]: "exponent (float_of 0) = 0" (is ?E)
-  and mantissa_0[simp]: "mantissa (float_of 0) = 0" (is ?M)
+lemma exponent_0[simp]: "exponent 0 = 0" (is ?E)
+  and mantissa_0[simp]: "mantissa 0 = 0" (is ?M)
 proof -
   have "\<And>p::int \<times> int. fst p = 0 \<and> snd p = 0 \<longleftrightarrow> p = (0, 0)"
     by auto
@@ -455,13 +455,13 @@
 qed
 
 lemma mantissa_exponent: "real_of_float f = mantissa f * 2 powr exponent f" (is ?E)
-  and mantissa_not_dvd: "f \<noteq> (float_of 0) \<Longrightarrow> \<not> 2 dvd mantissa f" (is "_ \<Longrightarrow> ?D")
+  and mantissa_not_dvd: "f \<noteq> 0 \<Longrightarrow> \<not> 2 dvd mantissa f" (is "_ \<Longrightarrow> ?D")
 proof cases
-  assume [simp]: "f \<noteq> float_of 0"
+  assume [simp]: "f \<noteq> 0"
   have "f = mantissa f * 2 powr exponent f \<and> \<not> 2 dvd mantissa f"
   proof (cases f rule: float_normed_cases)
     case zero
-    then show ?thesis by (simp add: zero_float_def)
+    then show ?thesis by simp
   next
     case (powr m e)
     then have "\<exists>p::int \<times> int. (f = 0 \<and> fst p = 0 \<and> snd p = 0) \<or>
@@ -469,14 +469,37 @@
       by auto
     then show ?thesis
       unfolding exponent_def mantissa_def
-      by (rule someI2_ex) (simp add: zero_float_def)
+      by (rule someI2_ex) simp
   qed
   then show ?E ?D by auto
 qed simp
 
-lemma mantissa_noteq_0: "f \<noteq> float_of 0 \<Longrightarrow> mantissa f \<noteq> 0"
+lemma mantissa_noteq_0: "f \<noteq> 0 \<Longrightarrow> mantissa f \<noteq> 0"
   using mantissa_not_dvd[of f] by auto
 
+lemma mantissa_eq_zero_iff: "mantissa x = 0 \<longleftrightarrow> x = 0"
+  (is "?lhs \<longleftrightarrow> ?rhs")
+proof
+  show ?rhs if ?lhs
+  proof -
+    from that have z: "0 = real_of_float x"
+      using mantissa_exponent by simp
+    show ?thesis
+      by (simp add: zero_float_def z)
+  qed
+  show ?lhs if ?rhs
+    using that by simp
+qed
+
+lemma mantissa_pos_iff: "0 < mantissa x \<longleftrightarrow> 0 < x"
+  by (auto simp: mantissa_exponent sign_simps)
+
+lemma mantissa_nonneg_iff: "0 \<le> mantissa x \<longleftrightarrow> 0 \<le> x"
+  by (auto simp: mantissa_exponent sign_simps zero_le_mult_iff)
+
+lemma mantissa_neg_iff: "0 > mantissa x \<longleftrightarrow> 0 > x"
+  by (auto simp: mantissa_exponent sign_simps zero_le_mult_iff)
+
 lemma
   fixes m e :: int
   defines "f \<equiv> float_of (m * 2 powr e)"
@@ -488,7 +511,7 @@
   with dvd show "mantissa f = m" by auto
 next
   assume "m \<noteq> 0"
-  then have f_not_0: "f \<noteq> float_of 0" by (simp add: f_def)
+  then have f_not_0: "f \<noteq> 0" by (simp add: f_def zero_float_def)
   from mantissa_exponent[of f] have "m * 2 powr e = mantissa f * 2 powr exponent f"
     by (auto simp add: f_def)
   then show ?M ?E
@@ -509,8 +532,8 @@
   by (atomize_elim) auto
 
 lemma denormalize_shift:
-  assumes f_def: "f \<equiv> Float m e"
-    and not_0: "f \<noteq> float_of 0"
+  assumes f_def: "f = Float m e"
+    and not_0: "f \<noteq> 0"
   obtains i where "m = mantissa f * 2 ^ i" "e = exponent f - i"
 proof
   from mantissa_exponent[of f] f_def
@@ -881,20 +904,20 @@
 
 lemma bitlen_Float:
   fixes m e
-  defines "f \<equiv> Float m e"
+  defines [THEN meta_eq_to_obj_eq]: "f \<equiv> Float m e"
   shows "bitlen \<bar>mantissa f\<bar> + exponent f = (if m = 0 then 0 else bitlen \<bar>m\<bar> + e)"
 proof (cases "m = 0")
   case True
-  then show ?thesis by (simp add: f_def bitlen_alt_def Float_def)
+  then show ?thesis by (simp add: f_def bitlen_alt_def)
 next
   case False
-  then have "f \<noteq> float_of 0"
+  then have "f \<noteq> 0"
     unfolding real_of_float_eq by (simp add: f_def)
   then have "mantissa f \<noteq> 0"
-    by (simp add: mantissa_noteq_0)
+    by (simp add: mantissa_eq_zero_iff)
   moreover
   obtain i where "m = mantissa f * 2 ^ i" "e = exponent f - int i"
-    by (rule f_def[THEN denormalize_shift, OF \<open>f \<noteq> float_of 0\<close>])
+    by (rule f_def[THEN denormalize_shift, OF \<open>f \<noteq> 0\<close>])
   ultimately show ?thesis by (simp add: abs_mult)
 qed
 
@@ -904,10 +927,7 @@
 proof -
   have "0 < Float m e" using assms by auto
   then have "0 < m" using powr_gt_zero[of 2 e]
-    apply (auto simp: zero_less_mult_iff)
-    using not_le powr_ge_pzero
-    apply blast
-    done
+    by (auto simp: zero_less_mult_iff)
   then have "m \<noteq> 0" by auto
   show ?thesis
   proof (cases "0 \<le> e")
@@ -1875,20 +1895,6 @@
 lemma bitlen_1: "bitlen 1 = 1"
   by (simp add: bitlen_alt_def)
 
-lemma mantissa_eq_zero_iff: "mantissa x = 0 \<longleftrightarrow> x = 0"
-  (is "?lhs \<longleftrightarrow> ?rhs")
-proof
-  show ?rhs if ?lhs
-  proof -
-    from that have z: "0 = real_of_float x"
-      using mantissa_exponent by simp
-    show ?thesis
-      by (simp add: zero_float_def z)
-  qed
-  show ?lhs if ?rhs
-    using that by (simp add: zero_float_def)
-qed
-
 lemma float_upper_bound: "x \<le> 2 powr (bitlen \<bar>mantissa x\<bar> + exponent x)"
 proof (cases "x = 0")
   case True
@@ -2104,7 +2110,7 @@
   by (simp add: truncate_up_eq_truncate_down truncate_down_mono)
 
 lemma Float_le_zero_iff: "Float a b \<le> 0 \<longleftrightarrow> a \<le> 0"
- by (auto simp: zero_float_def mult_le_0_iff) (simp add: not_less [symmetric])
+  by (auto simp: zero_float_def mult_le_0_iff)
 
 lemma real_of_float_pprt[simp]:
   fixes a :: float
@@ -2147,7 +2153,7 @@
   by transfer simp
 
 lemma floor_pos_exp: "exponent (floor_fl x) \<ge> 0"
-proof (cases "floor_fl x = float_of 0")
+proof (cases "floor_fl x = 0")
   case True
   then show ?thesis
     by (simp add: floor_fl_def)
@@ -2156,7 +2162,7 @@
   have eq: "floor_fl x = Float \<lfloor>real_of_float x\<rfloor> 0"
     by transfer simp
   obtain i where "\<lfloor>real_of_float x\<rfloor> = mantissa (floor_fl x) * 2 ^ i" "0 = exponent (floor_fl x) - int i"
-    by (rule denormalize_shift[OF eq[THEN eq_reflection] False])
+    by (rule denormalize_shift[OF eq False])
   then show ?thesis
     by simp
 qed
@@ -2164,11 +2170,14 @@
 lemma compute_mantissa[code]:
   "mantissa (Float m e) =
     (if m = 0 then 0 else if 2 dvd m then mantissa (normfloat (Float m e)) else m)"
-  by (auto simp: mantissa_float Float.abs_eq)
+  by (auto simp: mantissa_float Float.abs_eq zero_float_def[symmetric])
 
 lemma compute_exponent[code]:
   "exponent (Float m e) =
     (if m = 0 then 0 else if 2 dvd m then exponent (normfloat (Float m e)) else e)"
-  by (auto simp: exponent_float Float.abs_eq)
+  by (auto simp: exponent_float Float.abs_eq zero_float_def[symmetric])
+
+lifting_update Float.float.lifting
+lifting_forget Float.float.lifting
 
 end
diff -r a93cf1d6ba87 -r ed0a7090167d src/HOL/Library/Log_Nat.thy
--- a/src/HOL/Library/Log_Nat.thy	Sat Feb 03 20:46:28 2018 +0100
+++ b/src/HOL/Library/Log_Nat.thy	Mon Feb 05 08:30:19 2018 +0100
@@ -200,8 +200,11 @@
 lemma bitlen_alt_def: "bitlen a = (if a > 0 then \<lfloor>log 2 a\<rfloor> + 1 else 0)"
 by (simp add: bitlen_def floorlog_def)
 
+lemma bitlen_zero[simp]: "bitlen 0 = 0"
+  by (auto simp: bitlen_def floorlog_def)
+
 lemma bitlen_nonneg: "0 \<le> bitlen x"
-by (simp add: bitlen_def)
+  by (simp add: bitlen_def)
 
 lemma bitlen_bounds:
   assumes "x > 0"
diff -r a93cf1d6ba87 -r ed0a7090167d src/HOL/Matrix_LP/ComputeFloat.thy
--- a/src/HOL/Matrix_LP/ComputeFloat.thy	Sat Feb 03 20:46:28 2018 +0100
+++ b/src/HOL/Matrix_LP/ComputeFloat.thy	Mon Feb 05 08:30:19 2018 +0100
@@ -188,11 +188,11 @@
 
 lemma zero_le_float:
   "(0 <= float (a,b)) = (0 <= a)"
-  by (simp add: float_def zero_le_mult_iff) (simp add: not_less [symmetric])
+  by (simp add: float_def zero_le_mult_iff)
 
 lemma float_le_zero:
   "(float (a,b) <= 0) = (a <= 0)"
-  by (simp add: float_def mult_le_0_iff) (simp add: not_less [symmetric])
+  by (simp add: float_def mult_le_0_iff)
 
 lemma float_abs:
   "\<bar>float (a,b)\<bar> = (if 0 <= a then (float (a,b)) else (float (-a,b)))"
diff -r a93cf1d6ba87 -r ed0a7090167d src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Sat Feb 03 20:46:28 2018 +0100
+++ b/src/HOL/Transcendental.thy	Mon Feb 05 08:30:19 2018 +0100
@@ -2495,6 +2495,9 @@
   for x y :: real
   by (simp add: powr_def)
 
+lemma powr_non_neg[simp]: "\<not>a powr x < 0" for a x::real
+  using powr_ge_pzero[of a x] by arith
+
 lemma powr_divide: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> (x / y) powr a = (x powr a) / (y powr a)"
   for a b x :: real
   apply (simp add: divide_inverse positive_imp_inverse_positive powr_mult)
@@ -2606,6 +2609,10 @@
   for a x :: real
   by (simp add: powr_def)
 
+lemma powr_nonneg_iff[simp]: "a powr x \<le> 0 \<longleftrightarrow> a = 0"
+  for a x::real
+  by (meson not_less powr_gt_zero)
+
 lemma log_add_eq_powr: "0 < b \<Longrightarrow> b \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> log b x + y = log b (x * b powr y)"
   and add_log_eq_powr: "0 < b \<Longrightarrow> b \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> y + log b x = log b (b powr y * x)"
   and log_minus_eq_powr: "0 < b \<Longrightarrow> b \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> log b x - y = log b (x * b powr -y)"