
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




