tuned proofs;
authorwenzelm
Thu Jul 09 00:40:57 2015 +0200 (2015-07-09)
changeset 6069829e8bdc41f90
parent 60697 e266d5463e9d
child 60699 7bf560b196a3
tuned proofs;
src/HOL/Decision_Procs/Polynomial_List.thy
src/HOL/Decision_Procs/Rat_Pair.thy
src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
src/HOL/Library/Float.thy
src/HOL/Library/Lattice_Algebras.thy
     1.1 --- a/src/HOL/Decision_Procs/Polynomial_List.thy	Thu Jul 09 00:39:49 2015 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Polynomial_List.thy	Thu Jul 09 00:40:57 2015 +0200
     1.3 @@ -129,29 +129,38 @@
     1.4      by (cases a) (simp_all add: add.commute)
     1.5  qed
     1.6  
     1.7 -lemma (in comm_semiring_0) padd_assoc: "\<forall>b c. (a +++ b) +++ c = a +++ (b +++ c)"
     1.8 -  apply (induct a)
     1.9 -  apply simp
    1.10 -  apply clarify
    1.11 -  apply (case_tac b)
    1.12 -  apply (simp_all add: ac_simps)
    1.13 -  done
    1.14 +lemma (in comm_semiring_0) padd_assoc: "(a +++ b) +++ c = a +++ (b +++ c)"
    1.15 +proof (induct a arbitrary: b c)
    1.16 +  case Nil
    1.17 +  then show ?case
    1.18 +    by simp
    1.19 +next
    1.20 +  case Cons
    1.21 +  then show ?case
    1.22 +    by (cases b) (simp_all add: ac_simps)
    1.23 +qed
    1.24  
    1.25  lemma (in semiring_0) poly_cmult_distr: "a %* (p +++ q) = a %* p +++ a %* q"
    1.26 -  apply (induct p arbitrary: q)
    1.27 -  apply simp
    1.28 -  apply (case_tac q)
    1.29 -  apply (simp_all add: distrib_left)
    1.30 -  done
    1.31 +proof (induct p arbitrary: q)
    1.32 +  case Nil
    1.33 +  then show ?case
    1.34 +    by simp
    1.35 +next
    1.36 +  case Cons
    1.37 +  then show ?case
    1.38 +    by (cases q) (simp_all add: distrib_left)
    1.39 +qed
    1.40  
    1.41  lemma (in ring_1) pmult_by_x[simp]: "[0, 1] *** t = 0 # t"
    1.42 -  apply (induct t)
    1.43 -  apply simp
    1.44 -  apply (auto simp add: padd_commut)
    1.45 -  apply (case_tac t)
    1.46 -  apply auto
    1.47 -  done
    1.48 -
    1.49 +proof (induct t)
    1.50 +  case Nil
    1.51 +  then show ?case
    1.52 +    by simp
    1.53 +next
    1.54 +  case (Cons a t)
    1.55 +  then show ?case
    1.56 +    by (cases t) (auto simp add: padd_commut)
    1.57 +qed
    1.58  
    1.59  text \<open>Properties of evaluation of polynomials.\<close>
    1.60  
    1.61 @@ -167,18 +176,21 @@
    1.62  qed
    1.63  
    1.64  lemma (in comm_semiring_0) poly_cmult: "poly (c %* p) x = c * poly p x"
    1.65 -  apply (induct p)
    1.66 -  apply (case_tac [2] "x = zero")
    1.67 -  apply (auto simp add: distrib_left ac_simps)
    1.68 -  done
    1.69 +proof (induct p)
    1.70 +  case Nil
    1.71 +  then show ?case
    1.72 +    by simp
    1.73 +next
    1.74 +  case Cons
    1.75 +  then show ?case
    1.76 +    by (cases "x = zero") (auto simp add: distrib_left ac_simps)
    1.77 +qed
    1.78  
    1.79  lemma (in comm_semiring_0) poly_cmult_map: "poly (map (op * c) p) x = c * poly p x"
    1.80    by (induct p) (auto simp add: distrib_left ac_simps)
    1.81  
    1.82  lemma (in comm_ring_1) poly_minus: "poly (-- p) x = - (poly p x)"
    1.83 -  apply (simp add: poly_minus_def)
    1.84 -  apply (auto simp add: poly_cmult)
    1.85 -  done
    1.86 +  by (simp add: poly_minus_def) (auto simp add: poly_cmult)
    1.87  
    1.88  lemma (in comm_semiring_0) poly_mult: "poly (p1 *** p2) x = poly p1 x * poly p2 x"
    1.89  proof (induct p1 arbitrary: p2)
    1.90 @@ -186,7 +198,7 @@
    1.91    then show ?case
    1.92      by simp
    1.93  next
    1.94 -  case (Cons a as p2)
    1.95 +  case (Cons a as)
    1.96    then show ?case
    1.97      by (cases as) (simp_all add: poly_cmult poly_add distrib_right distrib_left ac_simps)
    1.98  qed
    1.99 @@ -216,16 +228,16 @@
   1.100  
   1.101  subsection \<open>Key Property: if @{term "f a = 0"} then @{term "(x - a)"} divides @{term "p(x)"}.\<close>
   1.102  
   1.103 -lemma (in comm_ring_1) lemma_poly_linear_rem: "\<forall>h. \<exists>q r. h#t = [r] +++ [-a, 1] *** q"
   1.104 -proof (induct t)
   1.105 +lemma (in comm_ring_1) lemma_poly_linear_rem: "\<exists>q r. h#t = [r] +++ [-a, 1] *** q"
   1.106 +proof (induct t arbitrary: h)
   1.107    case Nil
   1.108 -  have "[h] = [h] +++ [- a, 1] *** []" for h by simp
   1.109 +  have "[h] = [h] +++ [- a, 1] *** []" by simp
   1.110    then show ?case by blast
   1.111  next
   1.112    case (Cons  x xs)
   1.113 -  have "\<exists>q r. h # x # xs = [r] +++ [-a, 1] *** q" for h
   1.114 +  have "\<exists>q r. h # x # xs = [r] +++ [-a, 1] *** q"
   1.115    proof -
   1.116 -    from Cons.hyps obtain q r where qr: "x # xs = [r] +++ [- a, 1] *** q"
   1.117 +    from Cons obtain q r where qr: "x # xs = [r] +++ [- a, 1] *** q"
   1.118        by blast
   1.119      have "h # x # xs = [a * r + h] +++ [-a, 1] *** (r # q)"
   1.120        using qr by (cases q) (simp_all add: algebra_simps)
   1.121 @@ -237,7 +249,7 @@
   1.122  lemma (in comm_ring_1) poly_linear_rem: "\<exists>q r. h#t = [r] +++ [-a, 1] *** q"
   1.123    using lemma_poly_linear_rem [where t = t and a = a] by auto
   1.124  
   1.125 -lemma (in comm_ring_1) poly_linear_divides: "(poly p a = 0) \<longleftrightarrow> p = [] \<or> (\<exists>q. p = [-a, 1] *** q)"
   1.126 +lemma (in comm_ring_1) poly_linear_divides: "poly p a = 0 \<longleftrightarrow> p = [] \<or> (\<exists>q. p = [-a, 1] *** q)"
   1.127  proof (cases p)
   1.128    case Nil
   1.129    then show ?thesis by simp
   1.130 @@ -264,12 +276,12 @@
   1.131  qed
   1.132  
   1.133  lemma (in semiring_0) lemma_poly_length_mult[simp]:
   1.134 -  "\<forall>h k a. length (k %* p +++  (h # (a %* p))) = Suc (length p)"
   1.135 -  by (induct p) auto
   1.136 +  "length (k %* p +++  (h # (a %* p))) = Suc (length p)"
   1.137 +  by (induct p arbitrary: h k a) auto
   1.138  
   1.139  lemma (in semiring_0) lemma_poly_length_mult2[simp]:
   1.140 -  "\<forall>h k. length (k %* p +++  (h # p)) = Suc (length p)"
   1.141 -  by (induct p) auto
   1.142 +  "length (k %* p +++  (h # p)) = Suc (length p)"
   1.143 +  by (induct p arbitrary: h k) auto
   1.144  
   1.145  lemma (in ring_1) poly_length_mult[simp]: "length([-a,1] *** q) = Suc (length q)"
   1.146    by auto
   1.147 @@ -281,9 +293,9 @@
   1.148    by (induct p) auto
   1.149  
   1.150  lemma (in semiring_0) poly_add_length: "length (p1 +++ p2) = max (length p1) (length p2)"
   1.151 -  by (induct p1 arbitrary: p2) (simp_all, arith)
   1.152 +  by (induct p1 arbitrary: p2) auto
   1.153  
   1.154 -lemma (in semiring_0) poly_root_mult_length[simp]: "length([a,b] *** p) = Suc (length p)"
   1.155 +lemma (in semiring_0) poly_root_mult_length[simp]: "length ([a, b] *** p) = Suc (length p)"
   1.156    by (simp add: poly_add_length)
   1.157  
   1.158  lemma (in idom) poly_mult_not_eq_poly_Nil[simp]:
   1.159 @@ -301,15 +313,15 @@
   1.160  
   1.161  text \<open>A nontrivial polynomial of degree n has no more than n roots.\<close>
   1.162  lemma (in idom) poly_roots_index_lemma:
   1.163 -  assumes p: "poly p x \<noteq> poly [] x"
   1.164 -    and n: "length p = n"
   1.165 +  assumes "poly p x \<noteq> poly [] x"
   1.166 +    and "length p = n"
   1.167    shows "\<exists>i. \<forall>x. poly p x = 0 \<longrightarrow> (\<exists>m\<le>n. x = i m)"
   1.168 -  using p n
   1.169 +  using assms
   1.170  proof (induct n arbitrary: p x)
   1.171    case 0
   1.172    then show ?case by simp
   1.173  next
   1.174 -  case (Suc n p x)
   1.175 +  case (Suc n)
   1.176    have False if C: "\<And>i. \<exists>x. poly p x = 0 \<and> (\<forall>m\<le>Suc n. x \<noteq> i m)"
   1.177    proof -
   1.178      from Suc.prems have p0: "poly p x \<noteq> 0" "p \<noteq> []"
   1.179 @@ -325,14 +337,14 @@
   1.180        using q Suc.prems(2) by simp
   1.181      from q p0 have qx: "poly q x \<noteq> poly [] x"
   1.182        by (auto simp add: poly_mult poly_add poly_cmult)
   1.183 -    from Suc.hyps[OF qx lg] obtain i where i: "\<forall>x. poly q x = 0 \<longrightarrow> (\<exists>m\<le>n. x = i m)"
   1.184 +    from Suc.hyps[OF qx lg] obtain i where i: "\<And>x. poly q x = 0 \<longrightarrow> (\<exists>m\<le>n. x = i m)"
   1.185        by blast
   1.186      let ?i = "\<lambda>m. if m = Suc n then a else i m"
   1.187      from C[of ?i] obtain y where y: "poly p y = 0" "\<forall>m\<le> Suc n. y \<noteq> ?i m"
   1.188        by blast
   1.189      from y have "y = a \<or> poly q y = 0"
   1.190        by (simp only: q poly_mult_eq_zero_disj poly_add) (simp add: algebra_simps)
   1.191 -    with i[rule_format, of y] y(1) y(2) show ?thesis
   1.192 +    with i[of y] y(1) y(2) show ?thesis
   1.193        apply auto
   1.194        apply (erule_tac x = "m" in allE)
   1.195        apply auto
   1.196 @@ -343,12 +355,13 @@
   1.197  
   1.198  
   1.199  lemma (in idom) poly_roots_index_length:
   1.200 -  "poly p x \<noteq> poly [] x \<Longrightarrow> \<exists>i. \<forall>x. (poly p x = 0) \<longrightarrow> (\<exists>n. n \<le> length p \<and> x = i n)"
   1.201 +  "poly p x \<noteq> poly [] x \<Longrightarrow> \<exists>i. \<forall>x. poly p x = 0 \<longrightarrow> (\<exists>n. n \<le> length p \<and> x = i n)"
   1.202    by (blast intro: poly_roots_index_lemma)
   1.203  
   1.204  lemma (in idom) poly_roots_finite_lemma1:
   1.205 -  "poly p x \<noteq> poly [] x \<Longrightarrow> \<exists>N i. \<forall>x. (poly p x = 0) \<longrightarrow> (\<exists>n::nat. n < N \<and> x = i n)"
   1.206 -  apply (drule poly_roots_index_length, safe)
   1.207 +  "poly p x \<noteq> poly [] x \<Longrightarrow> \<exists>N i. \<forall>x. poly p x = 0 \<longrightarrow> (\<exists>n::nat. n < N \<and> x = i n)"
   1.208 +  apply (drule poly_roots_index_length)
   1.209 +  apply safe
   1.210    apply (rule_tac x = "Suc (length p)" in exI)
   1.211    apply (rule_tac x = i in exI)
   1.212    apply (simp add: less_Suc_eq_le)
   1.213 @@ -358,8 +371,10 @@
   1.214    assumes "\<forall>x. P x \<longrightarrow> (\<exists>n. n < length j \<and> x = j!n)"
   1.215    shows "finite {x. P x}"
   1.216  proof -
   1.217 -  from assms have "{x. P x} \<subseteq> set j" by auto
   1.218 -  then show ?thesis using finite_subset by auto
   1.219 +  from assms have "{x. P x} \<subseteq> set j"
   1.220 +    by auto
   1.221 +  then show ?thesis
   1.222 +    using finite_subset by auto
   1.223  qed
   1.224  
   1.225  lemma (in idom) poly_roots_finite_lemma2:
   1.226 @@ -379,7 +394,8 @@
   1.227    assume F: "finite (UNIV :: 'a set)"
   1.228    have "finite (UNIV :: nat set)"
   1.229    proof (rule finite_imageD)
   1.230 -    have "of_nat ` UNIV \<subseteq> UNIV" by simp
   1.231 +    have "of_nat ` UNIV \<subseteq> UNIV"
   1.232 +      by simp
   1.233      then show "finite (of_nat ` UNIV :: 'a set)"
   1.234        using F by (rule finite_subset)
   1.235      show "inj (of_nat :: nat \<Rightarrow> 'a)"
   1.236 @@ -499,12 +515,18 @@
   1.237  qed
   1.238  
   1.239  lemma (in idom_char_0) poly_zero: "poly p = poly [] \<longleftrightarrow> (\<forall>c \<in> set p. c = 0)"
   1.240 -  apply (induct p)
   1.241 -  apply simp
   1.242 -  apply (rule iffI)
   1.243 -  apply (drule poly_zero_lemma')
   1.244 -  apply auto
   1.245 -  done
   1.246 +proof (induct p)
   1.247 +  case Nil
   1.248 +  then show ?case by simp
   1.249 +next
   1.250 +  case Cons
   1.251 +  show ?case
   1.252 +    apply (rule iffI)
   1.253 +    apply (drule poly_zero_lemma')
   1.254 +    using Cons
   1.255 +    apply auto
   1.256 +    done
   1.257 +qed
   1.258  
   1.259  lemma (in idom_char_0) poly_0: "\<forall>c \<in> set p. c = 0 \<Longrightarrow> poly p x = 0"
   1.260    unfolding poly_zero[symmetric] by simp
   1.261 @@ -594,10 +616,10 @@
   1.262  text \<open>At last, we can consider the order of a root.\<close>
   1.263  
   1.264  lemma (in idom_char_0) poly_order_exists_lemma:
   1.265 -  assumes lp: "length p = d"
   1.266 -    and p: "poly p \<noteq> poly []"
   1.267 +  assumes "length p = d"
   1.268 +    and "poly p \<noteq> poly []"
   1.269    shows "\<exists>n q. p = mulexp n [-a, 1] q \<and> poly q a \<noteq> 0"
   1.270 -  using lp p
   1.271 +  using assms
   1.272  proof (induct d arbitrary: p)
   1.273    case 0
   1.274    then show ?case by simp
   1.275 @@ -613,15 +635,15 @@
   1.276      from True[unfolded poly_linear_divides] pN obtain q where q: "p = [-a, 1] *** q"
   1.277        by blast
   1.278      from q h True have qh: "length q = n" "poly q \<noteq> poly []"
   1.279 -      apply -
   1.280 -      apply simp
   1.281 +      apply simp_all
   1.282        apply (simp only: fun_eq_iff)
   1.283        apply (rule ccontr)
   1.284        apply (simp add: fun_eq_iff poly_add poly_cmult)
   1.285        done
   1.286      from Suc.hyps[OF qh] obtain m r where mr: "q = mulexp m [-a,1] r" "poly r a \<noteq> 0"
   1.287        by blast
   1.288 -    from mr q have "p = mulexp (Suc m) [-a,1] r \<and> poly r a \<noteq> 0" by simp
   1.289 +    from mr q have "p = mulexp (Suc m) [-a,1] r \<and> poly r a \<noteq> 0"
   1.290 +      by simp
   1.291      then show ?thesis by blast
   1.292    next
   1.293      case False
   1.294 @@ -680,7 +702,7 @@
   1.295        case 0
   1.296        show ?case
   1.297        proof (rule ccontr)
   1.298 -        assume "\<not> poly (mulexp 0 [- a, 1] q) \<noteq> poly ([- a, 1] %^ Suc 0 *** m)"
   1.299 +        assume "\<not> ?thesis"
   1.300          then have "poly q a = 0"
   1.301            by (simp add: poly_add poly_cmult)
   1.302          with \<open>poly q a \<noteq> 0\<close> show False
   1.303 @@ -689,7 +711,7 @@
   1.304      next
   1.305        case (Suc n)
   1.306        show ?case
   1.307 -        by (rule pexp_Suc [THEN ssubst], rule ccontr)
   1.308 +        by (rule pexp_Suc [THEN ssubst])
   1.309            (simp add: poly_mult_left_cancel poly_mult_assoc Suc del: pmult_Cons pexp_Suc)
   1.310      qed
   1.311      ultimately show False by simp
   1.312 @@ -906,8 +928,7 @@
   1.313  lemma (in semiring_0) pnormal_id: "pnormal p \<longleftrightarrow> 0 < length p \<and> last p \<noteq> 0"
   1.314    using pnormal_last_length pnormal_length pnormal_last_nonzero by blast
   1.315  
   1.316 -lemma (in idom_char_0) poly_Cons_eq:
   1.317 -  "poly (c # cs) = poly (d # ds) \<longleftrightarrow> c = d \<and> poly cs = poly ds"
   1.318 +lemma (in idom_char_0) poly_Cons_eq: "poly (c # cs) = poly (d # ds) \<longleftrightarrow> c = d \<and> poly cs = poly ds"
   1.319    (is "?lhs \<longleftrightarrow> ?rhs")
   1.320  proof
   1.321    show ?rhs if ?lhs
   1.322 @@ -974,11 +995,12 @@
   1.323    "last ((a %* p) +++ (x # (b %* p))) = (if p = [] then x else b * last p)"
   1.324    apply (induct p arbitrary: a x b)
   1.325    apply auto
   1.326 -  apply (rename_tac a p aa x b)
   1.327 -  apply (subgoal_tac "padd (cmult aa p) (times b a # cmult b p) \<noteq> []")
   1.328 -  apply simp
   1.329 -  apply (induct_tac p)
   1.330 -  apply auto
   1.331 +  subgoal for a p c x b
   1.332 +    apply (subgoal_tac "padd (cmult c p) (times b a # cmult b p) \<noteq> []")
   1.333 +    apply simp
   1.334 +    apply (induct p)
   1.335 +    apply auto
   1.336 +    done
   1.337    done
   1.338  
   1.339  lemma (in semiring_1) last_linear_mul:
   1.340 @@ -1097,13 +1119,18 @@
   1.341  lemma poly_mono:
   1.342    fixes x :: "'a::linordered_idom"
   1.343    shows "abs x \<le> k \<Longrightarrow> abs (poly p x) \<le> poly (map abs p) k"
   1.344 -  apply (induct p)
   1.345 -  apply auto
   1.346 -  apply (rename_tac a p)
   1.347 -  apply (rule_tac y = "abs a + abs (x * poly p x)" in order_trans)
   1.348 -  apply (rule abs_triangle_ineq)
   1.349 -  apply (auto intro!: mult_mono simp add: abs_mult)
   1.350 -  done
   1.351 +proof (induct p)
   1.352 +  case Nil
   1.353 +  then show ?case by simp
   1.354 +next
   1.355 +  case (Cons a p)
   1.356 +  then show ?case
   1.357 +    apply auto
   1.358 +    apply (rule_tac y = "abs a + abs (x * poly p x)" in order_trans)
   1.359 +    apply (rule abs_triangle_ineq)
   1.360 +    apply (auto intro!: mult_mono simp add: abs_mult)
   1.361 +    done
   1.362 +qed
   1.363  
   1.364  lemma (in semiring_0) poly_Sing: "poly [c] x = c"
   1.365    by simp
     2.1 --- a/src/HOL/Decision_Procs/Rat_Pair.thy	Thu Jul 09 00:39:49 2015 +0200
     2.2 +++ b/src/HOL/Decision_Procs/Rat_Pair.thy	Thu Jul 09 00:40:57 2015 +0200
     2.3 @@ -328,13 +328,7 @@
     2.4    proof cases
     2.5      case 1
     2.6      then show ?thesis
     2.7 -      apply (cases "a = 0")
     2.8 -      apply (simp_all add: x y Nmul_def INum_def Let_def)
     2.9 -      apply (cases "b = 0")
    2.10 -      apply simp_all
    2.11 -      apply (cases "a' = 0")
    2.12 -      apply simp_all
    2.13 -      done
    2.14 +      by (auto simp add: x y Nmul_def INum_def)
    2.15    next
    2.16      case neq: 2
    2.17      let ?g = "gcd (a * a') (b * b')"
    2.18 @@ -347,21 +341,21 @@
    2.19    qed
    2.20  qed
    2.21  
    2.22 -lemma Nneg[simp]: "INum (~\<^sub>N x) = - (INum x ::'a::field)"
    2.23 +lemma Nneg[simp]: "INum (~\<^sub>N x) = - (INum x :: 'a::field)"
    2.24    by (simp add: Nneg_def split_def INum_def)
    2.25  
    2.26 -lemma Nsub[simp]: "INum (x -\<^sub>N y) = INum x - (INum y:: 'a :: {field_char_0,field})"
    2.27 +lemma Nsub[simp]: "INum (x -\<^sub>N y) = INum x - (INum y:: 'a::{field_char_0,field})"
    2.28    by (simp add: Nsub_def split_def)
    2.29  
    2.30 -lemma Ninv[simp]: "INum (Ninv x) = (1::'a :: field) / (INum x)"
    2.31 +lemma Ninv[simp]: "INum (Ninv x) = (1 :: 'a::field) / INum x"
    2.32    by (simp add: Ninv_def INum_def split_def)
    2.33  
    2.34 -lemma Ndiv[simp]: "INum (x \<div>\<^sub>N y) = INum x / (INum y ::'a :: {field_char_0,field})"
    2.35 +lemma Ndiv[simp]: "INum (x \<div>\<^sub>N y) = INum x / (INum y :: 'a::{field_char_0,field})"
    2.36    by (simp add: Ndiv_def)
    2.37  
    2.38  lemma Nlt0_iff[simp]:
    2.39    assumes nx: "isnormNum x"
    2.40 -  shows "((INum x :: 'a::{field_char_0,linordered_field})< 0) = 0>\<^sub>N x"
    2.41 +  shows "((INum x :: 'a::{field_char_0,linordered_field}) < 0) = 0>\<^sub>N x"
    2.42  proof -
    2.43    obtain a b where x: "x = (a, b)" by (cases x)
    2.44    show ?thesis
    2.45 @@ -401,7 +395,7 @@
    2.46  
    2.47  lemma Ngt0_iff[simp]:
    2.48    assumes nx: "isnormNum x"
    2.49 -  shows "((INum x :: 'a::{field_char_0,linordered_field})> 0) = 0<\<^sub>N x"
    2.50 +  shows "((INum x :: 'a::{field_char_0,linordered_field}) > 0) = 0<\<^sub>N x"
    2.51  proof -
    2.52    obtain a b where x: "x = (a, b)" by (cases x)
    2.53    show ?thesis
    2.54 @@ -421,7 +415,7 @@
    2.55  
    2.56  lemma Nge0_iff[simp]:
    2.57    assumes nx: "isnormNum x"
    2.58 -  shows "((INum x :: 'a::{field_char_0,linordered_field}) \<ge> 0) = 0\<le>\<^sub>N x"
    2.59 +  shows "(INum x :: 'a::{field_char_0,linordered_field}) \<ge> 0 \<longleftrightarrow> 0\<le>\<^sub>N x"
    2.60  proof -
    2.61    obtain a b where x: "x = (a, b)" by (cases x)
    2.62    show ?thesis
    2.63 @@ -442,12 +436,12 @@
    2.64  lemma Nlt_iff[simp]:
    2.65    assumes nx: "isnormNum x"
    2.66      and ny: "isnormNum y"
    2.67 -  shows "((INum x :: 'a::{field_char_0,linordered_field}) < INum y) = (x <\<^sub>N y)"
    2.68 +  shows "((INum x :: 'a::{field_char_0,linordered_field}) < INum y) \<longleftrightarrow> x <\<^sub>N y"
    2.69  proof -
    2.70    let ?z = "0::'a"
    2.71 -  have "((INum x ::'a) < INum y) = (INum (x -\<^sub>N y) < ?z)"
    2.72 +  have "((INum x ::'a) < INum y) \<longleftrightarrow> INum (x -\<^sub>N y) < ?z"
    2.73      using nx ny by simp
    2.74 -  also have "\<dots> = (0>\<^sub>N (x -\<^sub>N y))"
    2.75 +  also have "\<dots> \<longleftrightarrow> 0>\<^sub>N (x -\<^sub>N y)"
    2.76      using Nlt0_iff[OF Nsub_normN[OF ny]] by simp
    2.77    finally show ?thesis
    2.78      by (simp add: Nlt_def)
    2.79 @@ -456,11 +450,11 @@
    2.80  lemma Nle_iff[simp]:
    2.81    assumes nx: "isnormNum x"
    2.82      and ny: "isnormNum y"
    2.83 -  shows "((INum x :: 'a::{field_char_0,linordered_field})\<le> INum y) = (x \<le>\<^sub>N y)"
    2.84 +  shows "((INum x :: 'a::{field_char_0,linordered_field}) \<le> INum y) \<longleftrightarrow> x \<le>\<^sub>N y"
    2.85  proof -
    2.86 -  have "((INum x ::'a) \<le> INum y) = (INum (x -\<^sub>N y) \<le> (0::'a))"
    2.87 +  have "((INum x ::'a) \<le> INum y) \<longleftrightarrow> INum (x -\<^sub>N y) \<le> (0::'a)"
    2.88      using nx ny by simp
    2.89 -  also have "\<dots> = (0\<ge>\<^sub>N (x -\<^sub>N y))"
    2.90 +  also have "\<dots> \<longleftrightarrow> 0\<ge>\<^sub>N (x -\<^sub>N y)"
    2.91      using Nle0_iff[OF Nsub_normN[OF ny]] by simp
    2.92    finally show ?thesis
    2.93      by (simp add: Nle_def)
    2.94 @@ -508,7 +502,7 @@
    2.95    shows "normNum (normNum x) = normNum x"
    2.96    by simp
    2.97  
    2.98 -lemma normNum0[simp]: "normNum (0,b) = 0\<^sub>N" "normNum (a,0) = 0\<^sub>N"
    2.99 +lemma normNum0[simp]: "normNum (0, b) = 0\<^sub>N" "normNum (a, 0) = 0\<^sub>N"
   2.100    by (simp_all add: normNum_def)
   2.101  
   2.102  lemma normNum_Nadd:
   2.103 @@ -520,29 +514,40 @@
   2.104    assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   2.105    shows "normNum x +\<^sub>N y = x +\<^sub>N y"
   2.106  proof -
   2.107 -  have n: "isnormNum (normNum x +\<^sub>N y)" "isnormNum (x +\<^sub>N y)" by simp_all
   2.108 -  have "INum (normNum x +\<^sub>N y) = INum x + (INum y :: 'a)" by simp
   2.109 -  also have "\<dots> = INum (x +\<^sub>N y)" by simp
   2.110 -  finally show ?thesis using isnormNum_unique[OF n] by simp
   2.111 +  have n: "isnormNum (normNum x +\<^sub>N y)" "isnormNum (x +\<^sub>N y)"
   2.112 +    by simp_all
   2.113 +  have "INum (normNum x +\<^sub>N y) = INum x + (INum y :: 'a)"
   2.114 +    by simp
   2.115 +  also have "\<dots> = INum (x +\<^sub>N y)"
   2.116 +    by simp
   2.117 +  finally show ?thesis
   2.118 +    using isnormNum_unique[OF n] by simp
   2.119  qed
   2.120  
   2.121  lemma Nadd_normNum2[simp]:
   2.122    assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   2.123    shows "x +\<^sub>N normNum y = x +\<^sub>N y"
   2.124  proof -
   2.125 -  have n: "isnormNum (x +\<^sub>N normNum y)" "isnormNum (x +\<^sub>N y)" by simp_all
   2.126 -  have "INum (x +\<^sub>N normNum y) = INum x + (INum y :: 'a)" by simp
   2.127 -  also have "\<dots> = INum (x +\<^sub>N y)" by simp
   2.128 -  finally show ?thesis using isnormNum_unique[OF n] by simp
   2.129 +  have n: "isnormNum (x +\<^sub>N normNum y)" "isnormNum (x +\<^sub>N y)"
   2.130 +    by simp_all
   2.131 +  have "INum (x +\<^sub>N normNum y) = INum x + (INum y :: 'a)"
   2.132 +    by simp
   2.133 +  also have "\<dots> = INum (x +\<^sub>N y)"
   2.134 +    by simp
   2.135 +  finally show ?thesis
   2.136 +    using isnormNum_unique[OF n] by simp
   2.137  qed
   2.138  
   2.139  lemma Nadd_assoc:
   2.140    assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   2.141    shows "x +\<^sub>N y +\<^sub>N z = x +\<^sub>N (y +\<^sub>N z)"
   2.142  proof -
   2.143 -  have n: "isnormNum (x +\<^sub>N y +\<^sub>N z)" "isnormNum (x +\<^sub>N (y +\<^sub>N z))" by simp_all
   2.144 -  have "INum (x +\<^sub>N y +\<^sub>N z) = (INum (x +\<^sub>N (y +\<^sub>N z)) :: 'a)" by simp
   2.145 -  with isnormNum_unique[OF n] show ?thesis by simp
   2.146 +  have n: "isnormNum (x +\<^sub>N y +\<^sub>N z)" "isnormNum (x +\<^sub>N (y +\<^sub>N z))"
   2.147 +    by simp_all
   2.148 +  have "INum (x +\<^sub>N y +\<^sub>N z) = (INum (x +\<^sub>N (y +\<^sub>N z)) :: 'a)"
   2.149 +    by simp
   2.150 +  with isnormNum_unique[OF n] show ?thesis
   2.151 +    by simp
   2.152  qed
   2.153  
   2.154  lemma Nmul_commute: "isnormNum x \<Longrightarrow> isnormNum y \<Longrightarrow> x *\<^sub>N y = y *\<^sub>N x"
   2.155 @@ -557,8 +562,10 @@
   2.156  proof -
   2.157    from nx ny nz have n: "isnormNum (x *\<^sub>N y *\<^sub>N z)" "isnormNum (x *\<^sub>N (y *\<^sub>N z))"
   2.158      by simp_all
   2.159 -  have "INum (x +\<^sub>N y +\<^sub>N z) = (INum (x +\<^sub>N (y +\<^sub>N z)) :: 'a)" by simp
   2.160 -  with isnormNum_unique[OF n] show ?thesis by simp
   2.161 +  have "INum (x +\<^sub>N y +\<^sub>N z) = (INum (x +\<^sub>N (y +\<^sub>N z)) :: 'a)"
   2.162 +    by simp
   2.163 +  with isnormNum_unique[OF n] show ?thesis
   2.164 +    by simp
   2.165  qed
   2.166  
   2.167  lemma Nsub0:
   2.168 @@ -568,9 +575,12 @@
   2.169    shows "x -\<^sub>N y = 0\<^sub>N \<longleftrightarrow> x = y"
   2.170  proof -
   2.171    from isnormNum_unique[where 'a = 'a, OF Nsub_normN[OF y], where y="0\<^sub>N"]
   2.172 -  have "(x -\<^sub>N y = 0\<^sub>N) = (INum (x -\<^sub>N y) = (INum 0\<^sub>N :: 'a)) " by simp
   2.173 -  also have "\<dots> = (INum x = (INum y :: 'a))" by simp
   2.174 -  also have "\<dots> = (x = y)" using x y by simp
   2.175 +  have "x -\<^sub>N y = 0\<^sub>N \<longleftrightarrow> INum (x -\<^sub>N y) = (INum 0\<^sub>N :: 'a)"
   2.176 +    by simp
   2.177 +  also have "\<dots> \<longleftrightarrow> INum x = (INum y :: 'a)"
   2.178 +    by simp
   2.179 +  also have "\<dots> \<longleftrightarrow> x = y"
   2.180 +    using x y by simp
   2.181    finally show ?thesis .
   2.182  qed
   2.183  
     3.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Thu Jul 09 00:39:49 2015 +0200
     3.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Thu Jul 09 00:40:57 2015 +0200
     3.3 @@ -8,7 +8,7 @@
     3.4  imports Complex_Main Rat_Pair Polynomial_List
     3.5  begin
     3.6  
     3.7 -subsection\<open>Datatype of polynomial expressions\<close>
     3.8 +subsection \<open>Datatype of polynomial expressions\<close>
     3.9  
    3.10  datatype poly = C Num | Bound nat | Add poly poly | Sub poly poly
    3.11    | Mul poly poly| Neg poly| Pw poly nat| CN poly nat poly
    3.12 @@ -66,7 +66,7 @@
    3.13  | "decrpoly a = a"
    3.14  
    3.15  
    3.16 -subsection\<open>Degrees and heads and coefficients\<close>
    3.17 +subsection \<open>Degrees and heads and coefficients\<close>
    3.18  
    3.19  fun degree :: "poly \<Rightarrow> nat"
    3.20  where
    3.21 @@ -78,7 +78,8 @@
    3.22    "head (CN c 0 p) = head p"
    3.23  | "head p = p"
    3.24  
    3.25 -(* More general notions of degree and head *)
    3.26 +text \<open>More general notions of degree and head.\<close>
    3.27 +
    3.28  fun degreen :: "poly \<Rightarrow> nat \<Rightarrow> nat"
    3.29  where
    3.30    "degreen (CN c n p) = (\<lambda>m. if n = m then 1 + degreen p n else 0)"
    3.31 @@ -110,7 +111,7 @@
    3.32  | "headconst (C n) = n"
    3.33  
    3.34  
    3.35 -subsection\<open>Operations for normalization\<close>
    3.36 +subsection \<open>Operations for normalization\<close>
    3.37  
    3.38  declare if_cong[fundef_cong del]
    3.39  declare let_cong[fundef_cong del]
    3.40 @@ -179,7 +180,7 @@
    3.41  | "polynate (Pw p n) = polynate p ^\<^sub>p n"
    3.42  | "polynate (CN c n p) = polynate (Add c (Mul (Bound n) p))"
    3.43  | "polynate (C c) = C (normNum c)"
    3.44 -by pat_completeness auto
    3.45 +  by pat_completeness auto
    3.46  termination by (relation "measure polysize") auto
    3.47  
    3.48  fun poly_cmul :: "Num \<Rightarrow> poly \<Rightarrow> poly"
    3.49 @@ -233,7 +234,7 @@
    3.50  | "poly_deriv p = 0\<^sub>p"
    3.51  
    3.52  
    3.53 -subsection\<open>Semantics of the polynomial representation\<close>
    3.54 +subsection \<open>Semantics of the polynomial representation\<close>
    3.55  
    3.56  primrec Ipoly :: "'a list \<Rightarrow> poly \<Rightarrow> 'a::{field_char_0,field,power}"
    3.57  where
    3.58 @@ -246,8 +247,7 @@
    3.59  | "Ipoly bs (Pw t n) = Ipoly bs t ^ n"
    3.60  | "Ipoly bs (CN c n p) = Ipoly bs c + (bs!n) * Ipoly bs p"
    3.61  
    3.62 -abbreviation Ipoly_syntax :: "poly \<Rightarrow> 'a list \<Rightarrow>'a::{field_char_0,field,power}"
    3.63 -    ("\<lparr>_\<rparr>\<^sub>p\<^bsup>_\<^esup>")
    3.64 +abbreviation Ipoly_syntax :: "poly \<Rightarrow> 'a list \<Rightarrow>'a::{field_char_0,field,power}"  ("\<lparr>_\<rparr>\<^sub>p\<^bsup>_\<^esup>")
    3.65    where "\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<equiv> Ipoly bs p"
    3.66  
    3.67  lemma Ipoly_CInt: "Ipoly bs (C (i, 1)) = of_int i"
    3.68 @@ -273,14 +273,14 @@
    3.69  definition isnpoly :: "poly \<Rightarrow> bool"
    3.70    where "isnpoly p = isnpolyh p 0"
    3.71  
    3.72 -text\<open>polyadd preserves normal forms\<close>
    3.73 +text \<open>polyadd preserves normal forms\<close>
    3.74  
    3.75  lemma polyadd_normh: "isnpolyh p n0 \<Longrightarrow> isnpolyh q n1 \<Longrightarrow> isnpolyh (polyadd p q) (min n0 n1)"
    3.76  proof (induct p q arbitrary: n0 n1 rule: polyadd.induct)
    3.77    case (2 ab c' n' p' n0 n1)
    3.78    from 2 have  th1: "isnpolyh (C ab) (Suc n')"
    3.79      by simp
    3.80 -  from 2(3) have th2: "isnpolyh c' (Suc n')"  and nplen1: "n' \<ge> n1"
    3.81 +  from 2(3) have th2: "isnpolyh c' (Suc n')" and nplen1: "n' \<ge> n1"
    3.82      by simp_all
    3.83    with isnpolyh_mono have cp: "isnpolyh c' (Suc n')"
    3.84      by simp
    3.85 @@ -314,11 +314,11 @@
    3.86      by simp
    3.87    from 4 have n'gen1: "n' \<ge> n1"
    3.88      by simp
    3.89 -  have "n < n' \<or> n' < n \<or> n = n'"
    3.90 -    by auto
    3.91 -  moreover
    3.92 -  {
    3.93 -    assume eq: "n = n'"
    3.94 +  consider (eq) "n = n'" | (lt) "n < n'" | (gt) "n > n'"
    3.95 +    by arith
    3.96 +  then show ?case
    3.97 +  proof cases
    3.98 +    case eq
    3.99      with "4.hyps"(3)[OF nc nc']
   3.100      have ncc':"isnpolyh (c +\<^sub>p c') (Suc n)"
   3.101        by auto
   3.102 @@ -329,12 +329,10 @@
   3.103        by simp
   3.104      have minle: "min n0 n1 \<le> n'"
   3.105        using ngen0 n'gen1 eq by simp
   3.106 -    from minle npp' ncc'n01 4 eq ngen0 n'gen1 ncc' have ?case
   3.107 +    from minle npp' ncc'n01 4 eq ngen0 n'gen1 ncc' show ?thesis
   3.108        by (simp add: Let_def)
   3.109 -  }
   3.110 -  moreover
   3.111 -  {
   3.112 -    assume lt: "n < n'"
   3.113 +  next
   3.114 +    case lt
   3.115      have "min n0 n1 \<le> n0"
   3.116        by simp
   3.117      with 4 lt have th1:"min n0 n1 \<le> n"
   3.118 @@ -347,12 +345,10 @@
   3.119        by arith
   3.120      from "4.hyps"(1)[OF th21 th22] have "isnpolyh (polyadd c (CN c' n' p')) (Suc n)"
   3.121        using th23 by simp
   3.122 -    with 4 lt th1 have ?case
   3.123 +    with 4 lt th1 show ?thesis
   3.124        by simp
   3.125 -  }
   3.126 -  moreover
   3.127 -  {
   3.128 -    assume gt: "n' < n"
   3.129 +  next
   3.130 +    case gt
   3.131      then have gt': "n' < n \<and> \<not> n < n'"
   3.132        by simp
   3.133      have "min n0 n1 \<le> n1"
   3.134 @@ -367,10 +363,9 @@
   3.135        by arith
   3.136      from "4.hyps"(2)[OF th22 th21] have "isnpolyh (polyadd (CN c n p) c') (Suc n')"
   3.137        using th23 by simp
   3.138 -    with 4 gt th1 have ?case
   3.139 +    with 4 gt th1 show ?thesis
   3.140        by simp
   3.141 -  }
   3.142 -  ultimately show ?case by blast
   3.143 +  qed
   3.144  qed auto
   3.145  
   3.146  lemma polyadd[simp]: "Ipoly bs (polyadd p q) = Ipoly bs p + Ipoly bs q"
   3.147 @@ -378,9 +373,9 @@
   3.148       (auto simp add: Let_def field_simps distrib_left[symmetric] simp del: distrib_left_NO_MATCH)
   3.149  
   3.150  lemma polyadd_norm: "isnpoly p \<Longrightarrow> isnpoly q \<Longrightarrow> isnpoly (polyadd p q)"
   3.151 -  using polyadd_normh[of "p" "0" "q" "0"] isnpoly_def by simp
   3.152 +  using polyadd_normh[of p 0 q 0] isnpoly_def by simp
   3.153  
   3.154 -text\<open>The degree of addition and other general lemmas needed for the normal form of polymul\<close>
   3.155 +text \<open>The degree of addition and other general lemmas needed for the normal form of polymul.\<close>
   3.156  
   3.157  lemma polyadd_different_degreen:
   3.158    assumes "isnpolyh p n0"
   3.159 @@ -391,17 +386,13 @@
   3.160    using assms
   3.161  proof (induct p q arbitrary: m n0 n1 rule: polyadd.induct)
   3.162    case (4 c n p c' n' p' m n0 n1)
   3.163 -  have "n' = n \<or> n < n' \<or> n' < n" by arith
   3.164 -  then show ?case
   3.165 -  proof (elim disjE)
   3.166 -    assume [simp]: "n' = n"
   3.167 -    from 4(4)[of n n m] 4(3)[of "Suc n" "Suc n" m] 4(5-7)
   3.168 +  show ?case
   3.169 +  proof (cases "n = n'")
   3.170 +    case True
   3.171 +    with 4(4)[of n n m] 4(3)[of "Suc n" "Suc n" m] 4(5-7)
   3.172      show ?thesis by (auto simp: Let_def)
   3.173    next
   3.174 -    assume "n < n'"
   3.175 -    with 4 show ?thesis by auto
   3.176 -  next
   3.177 -    assume "n' < n"
   3.178 +    case False
   3.179      with 4 show ?thesis by auto
   3.180    qed
   3.181  qed auto
   3.182 @@ -441,13 +432,15 @@
   3.183      by (cases n) auto
   3.184  next
   3.185    case (4 c n p c' n' p' n0 n1 m)
   3.186 -  have "n' = n \<or> n < n' \<or> n' < n" by arith
   3.187 -  then show ?case
   3.188 -  proof (elim disjE)
   3.189 -    assume [simp]: "n' = n"
   3.190 -    from 4(4)[of n n m] 4(3)[of "Suc n" "Suc n" m] 4(5-7)
   3.191 +  show ?case
   3.192 +  proof (cases "n = n'")
   3.193 +    case True
   3.194 +    with 4(4)[of n n m] 4(3)[of "Suc n" "Suc n" m] 4(5-7)
   3.195      show ?thesis by (auto simp: Let_def)
   3.196 -  qed simp_all
   3.197 +  next
   3.198 +    case False
   3.199 +    then show ?thesis by simp
   3.200 +  qed
   3.201  qed auto
   3.202  
   3.203  lemma polyadd_eq_const_degreen:
   3.204 @@ -458,26 +451,16 @@
   3.205    using assms
   3.206  proof (induct p q arbitrary: m n0 n1 c rule: polyadd.induct)
   3.207    case (4 c n p c' n' p' m n0 n1 x)
   3.208 -  {
   3.209 -    assume nn': "n' < n"
   3.210 -    then have ?case using 4 by simp
   3.211 -  }
   3.212 -  moreover
   3.213 -  {
   3.214 -    assume nn': "\<not> n' < n"
   3.215 -    then have "n < n' \<or> n = n'" by arith
   3.216 -    moreover { assume "n < n'" with 4 have ?case by simp }
   3.217 -    moreover
   3.218 -    {
   3.219 -      assume eq: "n = n'"
   3.220 -      then have ?case using 4
   3.221 -        apply (cases "p +\<^sub>p p' = 0\<^sub>p")
   3.222 -        apply (auto simp add: Let_def)
   3.223 -        done
   3.224 -    }
   3.225 -    ultimately have ?case by blast
   3.226 -  }
   3.227 -  ultimately show ?case by blast
   3.228 +  consider "n = n'" | "n > n' \<or> n < n'" by arith
   3.229 +  then show ?case
   3.230 +  proof cases
   3.231 +    case 1
   3.232 +    with 4 show ?thesis
   3.233 +      by (cases "p +\<^sub>p p' = 0\<^sub>p") (auto simp add: Let_def)
   3.234 +  next
   3.235 +    case 2
   3.236 +    with 4 show ?thesis by auto
   3.237 +  qed
   3.238  qed simp_all
   3.239  
   3.240  lemma polymul_properties:
   3.241 @@ -500,7 +483,7 @@
   3.242      then show ?case by auto
   3.243    next
   3.244      case (3 n0 n1)
   3.245 -    then show ?case  using "2.hyps" by auto
   3.246 +    then show ?case using "2.hyps" by auto
   3.247    }
   3.248  next
   3.249    case (3 c n p c')
   3.250 @@ -720,7 +703,7 @@
   3.251  qed
   3.252  
   3.253  
   3.254 -text\<open>polyneg is a negation and preserves normal forms\<close>
   3.255 +text \<open>polyneg is a negation and preserves normal forms\<close>
   3.256  
   3.257  lemma polyneg[simp]: "Ipoly bs (polyneg p) = - Ipoly bs p"
   3.258    by (induct p rule: polyneg.induct) auto
   3.259 @@ -738,7 +721,7 @@
   3.260    using isnpoly_def polyneg_normh by simp
   3.261  
   3.262  
   3.263 -text\<open>polysub is a substraction and preserves normal forms\<close>
   3.264 +text \<open>polysub is a substraction and preserves normal forms\<close>
   3.265  
   3.266  lemma polysub[simp]: "Ipoly bs (polysub p q) = Ipoly bs p - Ipoly bs q"
   3.267    by (simp add: polysub_def)
   3.268 @@ -762,7 +745,7 @@
   3.269    by (induct p q arbitrary: n0 n1 rule:polyadd.induct)
   3.270      (auto simp: Nsub0[simplified Nsub_def] Let_def)
   3.271  
   3.272 -text\<open>polypow is a power function and preserves normal forms\<close>
   3.273 +text \<open>polypow is a power function and preserves normal forms\<close>
   3.274  
   3.275  lemma polypow[simp]:
   3.276    "Ipoly bs (polypow n p) = (Ipoly bs p :: 'a::{field_char_0,field}) ^ n"
   3.277 @@ -830,7 +813,7 @@
   3.278    shows "isnpoly p \<Longrightarrow> isnpoly (polypow k p)"
   3.279    by (simp add: polypow_normh isnpoly_def)
   3.280  
   3.281 -text\<open>Finally the whole normalization\<close>
   3.282 +text \<open>Finally the whole normalization\<close>
   3.283  
   3.284  lemma polynate [simp]:
   3.285    "Ipoly bs (polynate p) = (Ipoly bs p :: 'a ::{field_char_0,field})"
   3.286 @@ -843,7 +826,7 @@
   3.287       (simp_all add: polyadd_norm polymul_norm polysub_norm polyneg_norm polypow_norm,
   3.288        simp_all add: isnpoly_def)
   3.289  
   3.290 -text\<open>shift1\<close>
   3.291 +text \<open>shift1\<close>
   3.292  
   3.293  
   3.294  lemma shift1: "Ipoly bs (shift1 p) = Ipoly bs (Mul (Bound 0) p)"
   3.295 @@ -1254,7 +1237,7 @@
   3.296  qed
   3.297  
   3.298  
   3.299 -text\<open>consequences of unicity on the algorithms for polynomial normalization\<close>
   3.300 +text \<open>consequences of unicity on the algorithms for polynomial normalization\<close>
   3.301  
   3.302  lemma polyadd_commute:
   3.303    assumes "SORT_CONSTRAINT('a::{field_char_0,field})"
   3.304 @@ -1328,7 +1311,7 @@
   3.305    unfolding poly_nate_polypoly' by auto
   3.306  
   3.307  
   3.308 -subsection\<open>heads, degrees and all that\<close>
   3.309 +subsection \<open>heads, degrees and all that\<close>
   3.310  
   3.311  lemma degree_eq_degreen0: "degree p = degreen p 0"
   3.312    by (induct p rule: degree.induct) simp_all
     4.1 --- a/src/HOL/Library/Float.thy	Thu Jul 09 00:39:49 2015 +0200
     4.2 +++ b/src/HOL/Library/Float.thy	Thu Jul 09 00:40:57 2015 +0200
     4.3 @@ -22,6 +22,7 @@
     4.4    real_of_float_def[code_unfold]: "real \<equiv> real_of_float"
     4.5  
     4.6  instance ..
     4.7 +
     4.8  end
     4.9  
    4.10  lemma type_definition_float': "type_definition real float_of float"
    4.11 @@ -34,7 +35,8 @@
    4.12  declare [[coercion "real :: float \<Rightarrow> real"]]
    4.13  
    4.14  lemma real_of_float_eq:
    4.15 -  fixes f1 f2 :: float shows "f1 = f2 \<longleftrightarrow> real f1 = real f2"
    4.16 +  fixes f1 f2 :: float
    4.17 +  shows "f1 = f2 \<longleftrightarrow> real f1 = real f2"
    4.18    unfolding real_of_float_def real_of_float_inject ..
    4.19  
    4.20  lemma float_of_real[simp]: "float_of (real x) = x"
    4.21 @@ -43,40 +45,63 @@
    4.22  lemma real_float[simp]: "x \<in> float \<Longrightarrow> real (float_of x) = x"
    4.23    unfolding real_of_float_def by (rule float_of_inverse)
    4.24  
    4.25 +
    4.26  subsection \<open>Real operations preserving the representation as floating point number\<close>
    4.27  
    4.28  lemma floatI: fixes m e :: int shows "m * 2 powr e = x \<Longrightarrow> x \<in> float"
    4.29    by (auto simp: float_def)
    4.30  
    4.31 -lemma zero_float[simp]: "0 \<in> float" by (auto simp: float_def)
    4.32 -lemma one_float[simp]: "1 \<in> float" by (intro floatI[of 1 0]) simp
    4.33 -lemma numeral_float[simp]: "numeral i \<in> float" by (intro floatI[of "numeral i" 0]) simp
    4.34 -lemma neg_numeral_float[simp]: "- numeral i \<in> float" by (intro floatI[of "- numeral i" 0]) simp
    4.35 -lemma real_of_int_float[simp]: "real (x :: int) \<in> float" by (intro floatI[of x 0]) simp
    4.36 -lemma real_of_nat_float[simp]: "real (x :: nat) \<in> float" by (intro floatI[of x 0]) simp
    4.37 -lemma two_powr_int_float[simp]: "2 powr (real (i::int)) \<in> float" by (intro floatI[of 1 i]) simp
    4.38 -lemma two_powr_nat_float[simp]: "2 powr (real (i::nat)) \<in> float" by (intro floatI[of 1 i]) simp
    4.39 -lemma two_powr_minus_int_float[simp]: "2 powr - (real (i::int)) \<in> float" by (intro floatI[of 1 "-i"]) simp
    4.40 -lemma two_powr_minus_nat_float[simp]: "2 powr - (real (i::nat)) \<in> float" by (intro floatI[of 1 "-i"]) simp
    4.41 -lemma two_powr_numeral_float[simp]: "2 powr numeral i \<in> float" by (intro floatI[of 1 "numeral i"]) simp
    4.42 -lemma two_powr_neg_numeral_float[simp]: "2 powr - numeral i \<in> float" by (intro floatI[of 1 "- numeral i"]) simp
    4.43 -lemma two_pow_float[simp]: "2 ^ n \<in> float" by (intro floatI[of 1 "n"]) (simp add: powr_realpow)
    4.44 -lemma real_of_float_float[simp]: "real (f::float) \<in> float" by (cases f) simp
    4.45 +lemma zero_float[simp]: "0 \<in> float"
    4.46 +  by (auto simp: float_def)
    4.47 +lemma one_float[simp]: "1 \<in> float"
    4.48 +  by (intro floatI[of 1 0]) simp
    4.49 +lemma numeral_float[simp]: "numeral i \<in> float"
    4.50 +  by (intro floatI[of "numeral i" 0]) simp
    4.51 +lemma neg_numeral_float[simp]: "- numeral i \<in> float"
    4.52 +  by (intro floatI[of "- numeral i" 0]) simp
    4.53 +lemma real_of_int_float[simp]: "real (x :: int) \<in> float"
    4.54 +  by (intro floatI[of x 0]) simp
    4.55 +lemma real_of_nat_float[simp]: "real (x :: nat) \<in> float"
    4.56 +  by (intro floatI[of x 0]) simp
    4.57 +lemma two_powr_int_float[simp]: "2 powr (real (i::int)) \<in> float"
    4.58 +  by (intro floatI[of 1 i]) simp
    4.59 +lemma two_powr_nat_float[simp]: "2 powr (real (i::nat)) \<in> float"
    4.60 +  by (intro floatI[of 1 i]) simp
    4.61 +lemma two_powr_minus_int_float[simp]: "2 powr - (real (i::int)) \<in> float"
    4.62 +  by (intro floatI[of 1 "-i"]) simp
    4.63 +lemma two_powr_minus_nat_float[simp]: "2 powr - (real (i::nat)) \<in> float"
    4.64 +  by (intro floatI[of 1 "-i"]) simp
    4.65 +lemma two_powr_numeral_float[simp]: "2 powr numeral i \<in> float"
    4.66 +  by (intro floatI[of 1 "numeral i"]) simp
    4.67 +lemma two_powr_neg_numeral_float[simp]: "2 powr - numeral i \<in> float"
    4.68 +  by (intro floatI[of 1 "- numeral i"]) simp
    4.69 +lemma two_pow_float[simp]: "2 ^ n \<in> float"
    4.70 +  by (intro floatI[of 1 "n"]) (simp add: powr_realpow)
    4.71 +lemma real_of_float_float[simp]: "real (f::float) \<in> float"
    4.72 +  by (cases f) simp
    4.73  
    4.74  lemma plus_float[simp]: "r \<in> float \<Longrightarrow> p \<in> float \<Longrightarrow> r + p \<in> float"
    4.75    unfolding float_def
    4.76  proof (safe, simp)
    4.77 -  fix e1 m1 e2 m2 :: int
    4.78 -  { fix e1 m1 e2 m2 :: int assume "e1 \<le> e2"
    4.79 -    then have "m1 * 2 powr e1 + m2 * 2 powr e2 = (m1 + m2 * 2 ^ nat (e2 - e1)) * 2 powr e1"
    4.80 +  have *: "\<exists>(m::int) (e::int). m1 * 2 powr e1 + m2 * 2 powr e2 = m * 2 powr e"
    4.81 +    if "e1 \<le> e2" for e1 m1 e2 m2 :: int
    4.82 +  proof -
    4.83 +    from that have "m1 * 2 powr e1 + m2 * 2 powr e2 = (m1 + m2 * 2 ^ nat (e2 - e1)) * 2 powr e1"
    4.84        by (simp add: powr_realpow[symmetric] powr_divide2[symmetric] field_simps)
    4.85 -    then have "\<exists>(m::int) (e::int). m1 * 2 powr e1 + m2 * 2 powr e2 = m * 2 powr e"
    4.86 -      by blast }
    4.87 -  note * = this
    4.88 -  show "\<exists>(m::int) (e::int). m1 * 2 powr e1 + m2 * 2 powr e2 = m * 2 powr e"
    4.89 -  proof (cases e1 e2 rule: linorder_le_cases)
    4.90 -    assume "e2 \<le> e1" from *[OF this, of m2 m1] show ?thesis by (simp add: ac_simps)
    4.91 -  qed (rule *)
    4.92 +    then show ?thesis
    4.93 +      by blast
    4.94 +  qed
    4.95 +  fix e1 m1 e2 m2 :: int
    4.96 +  consider "e2 \<le> e1" | "e1 \<le> e2" by (rule linorder_le_cases)
    4.97 +  then show "\<exists>(m::int) (e::int). m1 * 2 powr e1 + m2 * 2 powr e2 = m * 2 powr e"
    4.98 +  proof cases
    4.99 +    case 1
   4.100 +    from *[OF this, of m2 m1] show ?thesis
   4.101 +      by (simp add: ac_simps)
   4.102 +  next
   4.103 +    case 2
   4.104 +    then show ?thesis by (rule *)
   4.105 +  qed
   4.106  qed
   4.107  
   4.108  lemma uminus_float[simp]: "x \<in> float \<Longrightarrow> -x \<in> float"
   4.109 @@ -125,7 +150,8 @@
   4.110    done
   4.111  
   4.112  lemma div_numeral_Bit0_float[simp]:
   4.113 -  assumes x: "x / numeral n \<in> float" shows "x / (numeral (Num.Bit0 n)) \<in> float"
   4.114 +  assumes x: "x / numeral n \<in> float"
   4.115 +  shows "x / (numeral (Num.Bit0 n)) \<in> float"
   4.116  proof -
   4.117    have "(x / numeral n) / 2^1 \<in> float"
   4.118      by (intro x div_power_2_float)
   4.119 @@ -135,32 +161,38 @@
   4.120  qed
   4.121  
   4.122  lemma div_neg_numeral_Bit0_float[simp]:
   4.123 -  assumes x: "x / numeral n \<in> float" shows "x / (- numeral (Num.Bit0 n)) \<in> float"
   4.124 +  assumes x: "x / numeral n \<in> float"
   4.125 +  shows "x / (- numeral (Num.Bit0 n)) \<in> float"
   4.126  proof -
   4.127 -  have "- (x / numeral (Num.Bit0 n)) \<in> float" using x by simp
   4.128 +  have "- (x / numeral (Num.Bit0 n)) \<in> float"
   4.129 +    using x by simp
   4.130    also have "- (x / numeral (Num.Bit0 n)) = x / - numeral (Num.Bit0 n)"
   4.131      by simp
   4.132    finally show ?thesis .
   4.133  qed
   4.134  
   4.135 -lemma power_float[simp]: assumes "a \<in> float" shows "a ^ b \<in> float"
   4.136 +lemma power_float[simp]:
   4.137 +  assumes "a \<in> float"
   4.138 +  shows "a ^ b \<in> float"
   4.139  proof -
   4.140 -  from assms obtain m e::int where "a = m * 2 powr e"
   4.141 +  from assms obtain m e :: int where "a = m * 2 powr e"
   4.142      by (auto simp: float_def)
   4.143 -  thus ?thesis
   4.144 +  then show ?thesis
   4.145      by (auto intro!: floatI[where m="m^b" and e = "e*b"]
   4.146        simp: power_mult_distrib powr_realpow[symmetric] powr_powr)
   4.147  qed
   4.148  
   4.149 -lift_definition Float :: "int \<Rightarrow> int \<Rightarrow> float" is "\<lambda>(m::int) (e::int). m * 2 powr e" by simp
   4.150 +lift_definition Float :: "int \<Rightarrow> int \<Rightarrow> float" is "\<lambda>(m::int) (e::int). m * 2 powr e"
   4.151 +  by simp
   4.152  declare Float.rep_eq[simp]
   4.153  
   4.154  lemma compute_real_of_float[code]:
   4.155    "real_of_float (Float m e) = (if e \<ge> 0 then m * 2 ^ nat e else m / 2 ^ (nat (-e)))"
   4.156 -by (simp add: real_of_float_def[symmetric] powr_int)
   4.157 +  by (simp add: real_of_float_def[symmetric] powr_int)
   4.158  
   4.159  code_datatype Float
   4.160  
   4.161 +
   4.162  subsection \<open>Arithmetic operations on floating point numbers\<close>
   4.163  
   4.164  instantiation float :: "{ring_1, linorder, linordered_ring, linordered_idom, numeral, equal}"
   4.165 @@ -192,16 +224,20 @@
   4.166  declare less_float.rep_eq[simp]
   4.167  
   4.168  instance
   4.169 -  proof qed (transfer, fastforce simp add: field_simps intro: mult_left_mono mult_right_mono)+
   4.170 +  by (standard; transfer; fastforce simp add: field_simps intro: mult_left_mono mult_right_mono)+
   4.171 +
   4.172  end
   4.173  
   4.174  lemma Float_0_eq_0[simp]: "Float 0 e = 0"
   4.175    by transfer simp
   4.176  
   4.177 -lemma real_of_float_power[simp]: fixes f::float shows "real (f^n) = real f^n"
   4.178 +lemma real_of_float_power[simp]:
   4.179 +  fixes f :: float
   4.180 +  shows "real (f^n) = real f^n"
   4.181    by (induct n) simp_all
   4.182  
   4.183 -lemma fixes x y::float
   4.184 +lemma
   4.185 +  fixes x y :: float
   4.186    shows real_of_float_min: "real (min x y) = min (real x) (real y)"
   4.187      and real_of_float_max: "real (max x y) = max (real x) (real y)"
   4.188    by (simp_all add: min_def max_def)
   4.189 @@ -219,9 +255,9 @@
   4.190      apply transfer
   4.191      apply simp
   4.192      done
   4.193 -  assume "a < b"
   4.194 -  then show "\<exists>c. a < c \<and> c < b"
   4.195 -    apply (intro exI[of _ "(a + b) * Float 1 (- 1)"])
   4.196 +  show "\<exists>c. a < c \<and> c < b" if "a < b"
   4.197 +    apply (rule exI[of _ "(a + b) * Float 1 (- 1)"])
   4.198 +    using that
   4.199      apply transfer
   4.200      apply (simp add: powr_minus)
   4.201      done
   4.202 @@ -230,11 +266,11 @@
   4.203  instantiation float :: lattice_ab_group_add
   4.204  begin
   4.205  
   4.206 -definition inf_float::"float\<Rightarrow>float\<Rightarrow>float"
   4.207 -where "inf_float a b = min a b"
   4.208 +definition inf_float :: "float \<Rightarrow> float \<Rightarrow> float"
   4.209 +  where "inf_float a b = min a b"
   4.210  
   4.211 -definition sup_float::"float\<Rightarrow>float\<Rightarrow>float"
   4.212 -where "sup_float a b = max a b"
   4.213 +definition sup_float :: "float \<Rightarrow> float \<Rightarrow> float"
   4.214 +  where "sup_float a b = max a b"
   4.215  
   4.216  instance
   4.217    by (standard; transfer; simp add: inf_float_def sup_float_def real_of_float_min real_of_float_max)
   4.218 @@ -250,20 +286,21 @@
   4.219  
   4.220  lemma transfer_numeral [transfer_rule]:
   4.221    "rel_fun (op =) pcr_float (numeral :: _ \<Rightarrow> real) (numeral :: _ \<Rightarrow> float)"
   4.222 -  unfolding rel_fun_def float.pcr_cr_eq  cr_float_def by simp
   4.223 +  by (simp add: rel_fun_def float.pcr_cr_eq cr_float_def)
   4.224  
   4.225  lemma float_neg_numeral[simp]: "real (- numeral x :: float) = - numeral x"
   4.226    by simp
   4.227  
   4.228  lemma transfer_neg_numeral [transfer_rule]:
   4.229    "rel_fun (op =) pcr_float (- numeral :: _ \<Rightarrow> real) (- numeral :: _ \<Rightarrow> float)"
   4.230 -  unfolding rel_fun_def float.pcr_cr_eq cr_float_def by simp
   4.231 +  by (simp add: rel_fun_def float.pcr_cr_eq cr_float_def)
   4.232  
   4.233  lemma
   4.234    shows float_of_numeral[simp]: "numeral k = float_of (numeral k)"
   4.235      and float_of_neg_numeral[simp]: "- numeral k = float_of (- numeral k)"
   4.236    unfolding real_of_float_eq by simp_all
   4.237  
   4.238 +
   4.239  subsection \<open>Quickcheck\<close>
   4.240  
   4.241  instantiation float :: exhaustive
   4.242 @@ -311,39 +348,51 @@
   4.243    assumes H: "\<And>n. (\<And>i. \<bar>i\<bar> < \<bar>n\<bar> \<Longrightarrow> P i) \<Longrightarrow> P n"
   4.244    shows "P j"
   4.245  proof (induct "nat \<bar>j\<bar>" arbitrary: j rule: less_induct)
   4.246 -  case less show ?case by (rule H[OF less]) simp
   4.247 +  case less
   4.248 +  show ?case by (rule H[OF less]) simp
   4.249  qed
   4.250  
   4.251  lemma int_cancel_factors:
   4.252 -  fixes n :: int assumes "1 < r" shows "n = 0 \<or> (\<exists>k i. n = k * r ^ i \<and> \<not> r dvd k)"
   4.253 +  fixes n :: int
   4.254 +  assumes "1 < r"
   4.255 +  shows "n = 0 \<or> (\<exists>k i. n = k * r ^ i \<and> \<not> r dvd k)"
   4.256  proof (induct n rule: int_induct_abs)
   4.257    case (less n)
   4.258 -  { fix m assume n: "n \<noteq> 0" "n = m * r"
   4.259 -    then have "\<bar>m \<bar> < \<bar>n\<bar>"
   4.260 +  have "\<exists>k i. n = k * r ^ Suc i \<and> \<not> r dvd k" if "n \<noteq> 0" "n = m * r" for m
   4.261 +  proof -
   4.262 +    from that have "\<bar>m \<bar> < \<bar>n\<bar>"
   4.263        using \<open>1 < r\<close> by (simp add: abs_mult)
   4.264 -    from less[OF this] n have "\<exists>k i. n = k * r ^ Suc i \<and> \<not> r dvd k" by auto }
   4.265 +    from less[OF this] that show ?thesis by auto
   4.266 +  qed
   4.267    then show ?case
   4.268      by (metis dvd_def monoid_mult_class.mult.right_neutral mult.commute power_0)
   4.269  qed
   4.270  
   4.271  lemma mult_powr_eq_mult_powr_iff_asym:
   4.272    fixes m1 m2 e1 e2 :: int
   4.273 -  assumes m1: "\<not> 2 dvd m1" and "e1 \<le> e2"
   4.274 +  assumes m1: "\<not> 2 dvd m1"
   4.275 +    and "e1 \<le> e2"
   4.276    shows "m1 * 2 powr e1 = m2 * 2 powr e2 \<longleftrightarrow> m1 = m2 \<and> e1 = e2"
   4.277 +  (is "?lhs \<longleftrightarrow> ?rhs")
   4.278  proof
   4.279 -  have "m1 \<noteq> 0" using m1 unfolding dvd_def by auto
   4.280 -  assume eq: "m1 * 2 powr e1 = m2 * 2 powr e2"
   4.281 -  with \<open>e1 \<le> e2\<close> have "m1 = m2 * 2 powr nat (e2 - e1)"
   4.282 -    by (simp add: powr_divide2[symmetric] field_simps)
   4.283 -  also have "\<dots> = m2 * 2^nat (e2 - e1)"
   4.284 -    by (simp add: powr_realpow)
   4.285 -  finally have m1_eq: "m1 = m2 * 2^nat (e2 - e1)"
   4.286 -    unfolding real_of_int_inject .
   4.287 -  with m1 have "m1 = m2"
   4.288 -    by (cases "nat (e2 - e1)") (auto simp add: dvd_def)
   4.289 -  then show "m1 = m2 \<and> e1 = e2"
   4.290 -    using eq \<open>m1 \<noteq> 0\<close> by (simp add: powr_inj)
   4.291 -qed simp
   4.292 +  show ?rhs if eq: ?lhs
   4.293 +  proof -
   4.294 +    have "m1 \<noteq> 0"
   4.295 +      using m1 unfolding dvd_def by auto
   4.296 +    from \<open>e1 \<le> e2\<close> eq have "m1 = m2 * 2 powr nat (e2 - e1)"
   4.297 +      by (simp add: powr_divide2[symmetric] field_simps)
   4.298 +    also have "\<dots> = m2 * 2^nat (e2 - e1)"
   4.299 +      by (simp add: powr_realpow)
   4.300 +    finally have m1_eq: "m1 = m2 * 2^nat (e2 - e1)"
   4.301 +      unfolding real_of_int_inject .
   4.302 +    with m1 have "m1 = m2"
   4.303 +      by (cases "nat (e2 - e1)") (auto simp add: dvd_def)
   4.304 +    then show ?thesis
   4.305 +      using eq \<open>m1 \<noteq> 0\<close> by (simp add: powr_inj)
   4.306 +  qed
   4.307 +  show ?lhs if ?rhs
   4.308 +    using that by simp
   4.309 +qed
   4.310  
   4.311  lemma mult_powr_eq_mult_powr_iff:
   4.312    fixes m1 m2 e1 e2 :: int
   4.313 @@ -356,16 +405,18 @@
   4.314    assumes x: "x \<in> float"
   4.315    obtains (zero) "x = 0"
   4.316     | (powr) m e :: int where "x = m * 2 powr e" "\<not> 2 dvd m" "x \<noteq> 0"
   4.317 -proof atomize_elim
   4.318 -  { assume "x \<noteq> 0"
   4.319 -    from x obtain m e :: int where x: "x = m * 2 powr e" by (auto simp: float_def)
   4.320 +proof -
   4.321 +  {
   4.322 +    assume "x \<noteq> 0"
   4.323 +    from x obtain m e :: int where x: "x = m * 2 powr e"
   4.324 +      by (auto simp: float_def)
   4.325      with \<open>x \<noteq> 0\<close> int_cancel_factors[of 2 m] obtain k i where "m = k * 2 ^ i" "\<not> 2 dvd k"
   4.326        by auto
   4.327      with \<open>\<not> 2 dvd k\<close> x have "\<exists>(m::int) (e::int). x = m * 2 powr e \<and> \<not> (2::int) dvd m"
   4.328        by (rule_tac exI[of _ "k"], rule_tac exI[of _ "e + int i"])
   4.329 -         (simp add: powr_add powr_realpow) }
   4.330 -  then show "x = 0 \<or> (\<exists>(m::int) (e::int). x = m * 2 powr e \<and> \<not> (2::int) dvd m \<and> x \<noteq> 0)"
   4.331 -    by blast
   4.332 +        (simp add: powr_add powr_realpow)
   4.333 +  }
   4.334 +  with that show thesis by blast
   4.335  qed
   4.336  
   4.337  lemma float_normed_cases:
   4.338 @@ -373,7 +424,8 @@
   4.339    obtains (zero) "f = 0"
   4.340     | (powr) m e :: int where "real f = m * 2 powr e" "\<not> 2 dvd m" "f \<noteq> 0"
   4.341  proof (atomize_elim, induct f)
   4.342 -  case (float_of y) then show ?case
   4.343 +  case (float_of y)
   4.344 +  then show ?case
   4.345      by (cases rule: floatE_normed) (auto simp: zero_float_def)
   4.346  qed
   4.347  
   4.348 @@ -389,7 +441,8 @@
   4.349    shows exponent_0[simp]: "exponent (float_of 0) = 0" (is ?E)
   4.350      and mantissa_0[simp]: "mantissa (float_of 0) = 0" (is ?M)
   4.351  proof -
   4.352 -  have "\<And>p::int \<times> int. fst p = 0 \<and> snd p = 0 \<longleftrightarrow> p = (0, 0)" by auto
   4.353 +  have "\<And>p::int \<times> int. fst p = 0 \<and> snd p = 0 \<longleftrightarrow> p = (0, 0)"
   4.354 +    by auto
   4.355    then show ?E ?M
   4.356      by (auto simp add: mantissa_def exponent_def zero_float_def)
   4.357  qed
   4.358 @@ -398,17 +451,20 @@
   4.359    shows mantissa_exponent: "real f = mantissa f * 2 powr exponent f" (is ?E)
   4.360      and mantissa_not_dvd: "f \<noteq> (float_of 0) \<Longrightarrow> \<not> 2 dvd mantissa f" (is "_ \<Longrightarrow> ?D")
   4.361  proof cases
   4.362 -  assume [simp]: "f \<noteq> (float_of 0)"
   4.363 +  assume [simp]: "f \<noteq> float_of 0"
   4.364    have "f = mantissa f * 2 powr exponent f \<and> \<not> 2 dvd mantissa f"
   4.365    proof (cases f rule: float_normed_cases)
   4.366 +    case zero
   4.367 +    then show ?thesis by  (simp add: zero_float_def)
   4.368 +  next
   4.369      case (powr m e)
   4.370 -    then have "\<exists>p::int \<times> int. (f = 0 \<and> fst p = 0 \<and> snd p = 0)
   4.371 -     \<or> (f \<noteq> 0 \<and> real f = real (fst p) * 2 powr real (snd p) \<and> \<not> 2 dvd fst p)"
   4.372 +    then have "\<exists>p::int \<times> int. (f = 0 \<and> fst p = 0 \<and> snd p = 0) \<or>
   4.373 +      (f \<noteq> 0 \<and> real f = real (fst p) * 2 powr real (snd p) \<and> \<not> 2 dvd fst p)"
   4.374        by auto
   4.375      then show ?thesis
   4.376        unfolding exponent_def mantissa_def
   4.377        by (rule someI2_ex) (simp add: zero_float_def)
   4.378 -  qed (simp add: zero_float_def)
   4.379 +  qed
   4.380    then show ?E ?D by auto
   4.381  qed simp
   4.382  
   4.383 @@ -422,31 +478,33 @@
   4.384    shows mantissa_float: "mantissa f = m" (is "?M")
   4.385      and exponent_float: "m \<noteq> 0 \<Longrightarrow> exponent f = e" (is "_ \<Longrightarrow> ?E")
   4.386  proof cases
   4.387 -  assume "m = 0" with dvd show "mantissa f = m" by auto
   4.388 +  assume "m = 0"
   4.389 +  with dvd show "mantissa f = m" by auto
   4.390  next
   4.391    assume "m \<noteq> 0"
   4.392    then have f_not_0: "f \<noteq> float_of 0" by (simp add: f_def)
   4.393 -  from mantissa_exponent[of f]
   4.394 -  have "m * 2 powr e = mantissa f * 2 powr exponent f"
   4.395 +  from mantissa_exponent[of f] have "m * 2 powr e = mantissa f * 2 powr exponent f"
   4.396      by (auto simp add: f_def)
   4.397    then show "?M" "?E"
   4.398      using mantissa_not_dvd[OF f_not_0] dvd
   4.399      by (auto simp: mult_powr_eq_mult_powr_iff)
   4.400  qed
   4.401  
   4.402 +
   4.403  subsection \<open>Compute arithmetic operations\<close>
   4.404  
   4.405  lemma Float_mantissa_exponent: "Float (mantissa f) (exponent f) = f"
   4.406    unfolding real_of_float_eq mantissa_exponent[of f] by simp
   4.407  
   4.408 -lemma Float_cases[case_names Float, cases type: float]:
   4.409 +lemma Float_cases [cases type: float]:
   4.410    fixes f :: float
   4.411    obtains (Float) m e :: int where "f = Float m e"
   4.412    using Float_mantissa_exponent[symmetric]
   4.413    by (atomize_elim) auto
   4.414  
   4.415  lemma denormalize_shift:
   4.416 -  assumes f_def: "f \<equiv> Float m e" and not_0: "f \<noteq> float_of 0"
   4.417 +  assumes f_def: "f \<equiv> Float m e"
   4.418 +    and not_0: "f \<noteq> float_of 0"
   4.419    obtains i where "m = mantissa f * 2 ^ i" "e = exponent f - i"
   4.420  proof
   4.421    from mantissa_exponent[of f] f_def
   4.422 @@ -481,87 +539,75 @@
   4.423      unfolding real_of_int_inject by auto
   4.424  qed
   4.425  
   4.426 -lemma compute_float_zero[code_unfold, code]: "0 = Float 0 0"
   4.427 -  by transfer simp
   4.428 -hide_fact (open) compute_float_zero
   4.429 +context
   4.430 +begin
   4.431  
   4.432 -lemma compute_float_one[code_unfold, code]: "1 = Float 1 0"
   4.433 +qualified lemma compute_float_zero[code_unfold, code]: "0 = Float 0 0"
   4.434    by transfer simp
   4.435 -hide_fact (open) compute_float_one
   4.436 +
   4.437 +qualified lemma compute_float_one[code_unfold, code]: "1 = Float 1 0"
   4.438 +  by transfer simp
   4.439  
   4.440  lift_definition normfloat :: "float \<Rightarrow> float" is "\<lambda>x. x" .
   4.441  lemma normloat_id[simp]: "normfloat x = x" by transfer rule
   4.442  
   4.443 -lemma compute_normfloat[code]: "normfloat (Float m e) =
   4.444 +qualified lemma compute_normfloat[code]: "normfloat (Float m e) =
   4.445    (if m mod 2 = 0 \<and> m \<noteq> 0 then normfloat (Float (m div 2) (e + 1))
   4.446                             else if m = 0 then 0 else Float m e)"
   4.447    by transfer (auto simp add: powr_add zmod_eq_0_iff)
   4.448 -hide_fact (open) compute_normfloat
   4.449  
   4.450 -lemma compute_float_numeral[code_abbrev]: "Float (numeral k) 0 = numeral k"
   4.451 +qualified lemma compute_float_numeral[code_abbrev]: "Float (numeral k) 0 = numeral k"
   4.452    by transfer simp
   4.453 -hide_fact (open) compute_float_numeral
   4.454  
   4.455 -lemma compute_float_neg_numeral[code_abbrev]: "Float (- numeral k) 0 = - numeral k"
   4.456 +qualified lemma compute_float_neg_numeral[code_abbrev]: "Float (- numeral k) 0 = - numeral k"
   4.457    by transfer simp
   4.458 -hide_fact (open) compute_float_neg_numeral
   4.459  
   4.460 -lemma compute_float_uminus[code]: "- Float m1 e1 = Float (- m1) e1"
   4.461 +qualified lemma compute_float_uminus[code]: "- Float m1 e1 = Float (- m1) e1"
   4.462    by transfer simp
   4.463 -hide_fact (open) compute_float_uminus
   4.464  
   4.465 -lemma compute_float_times[code]: "Float m1 e1 * Float m2 e2 = Float (m1 * m2) (e1 + e2)"
   4.466 +qualified lemma compute_float_times[code]: "Float m1 e1 * Float m2 e2 = Float (m1 * m2) (e1 + e2)"
   4.467    by transfer (simp add: field_simps powr_add)
   4.468 -hide_fact (open) compute_float_times
   4.469  
   4.470 -lemma compute_float_plus[code]: "Float m1 e1 + Float m2 e2 =
   4.471 +qualified lemma compute_float_plus[code]: "Float m1 e1 + Float m2 e2 =
   4.472    (if m1 = 0 then Float m2 e2 else if m2 = 0 then Float m1 e1 else
   4.473    if e1 \<le> e2 then Float (m1 + m2 * 2^nat (e2 - e1)) e1
   4.474                else Float (m2 + m1 * 2^nat (e1 - e2)) e2)"
   4.475    by transfer (simp add: field_simps powr_realpow[symmetric] powr_divide2[symmetric])
   4.476 -hide_fact (open) compute_float_plus
   4.477  
   4.478 -lemma compute_float_minus[code]: fixes f g::float shows "f - g = f + (-g)"
   4.479 +qualified lemma compute_float_minus[code]: fixes f g::float shows "f - g = f + (-g)"
   4.480    by simp
   4.481 -hide_fact (open) compute_float_minus
   4.482  
   4.483 -lemma compute_float_sgn[code]: "sgn (Float m1 e1) = (if 0 < m1 then 1 else if m1 < 0 then -1 else 0)"
   4.484 +qualified lemma compute_float_sgn[code]: "sgn (Float m1 e1) = (if 0 < m1 then 1 else if m1 < 0 then -1 else 0)"
   4.485    by transfer (simp add: sgn_times)
   4.486 -hide_fact (open) compute_float_sgn
   4.487  
   4.488  lift_definition is_float_pos :: "float \<Rightarrow> bool" is "op < 0 :: real \<Rightarrow> bool" .
   4.489  
   4.490 -lemma compute_is_float_pos[code]: "is_float_pos (Float m e) \<longleftrightarrow> 0 < m"
   4.491 +qualified lemma compute_is_float_pos[code]: "is_float_pos (Float m e) \<longleftrightarrow> 0 < m"
   4.492    by transfer (auto simp add: zero_less_mult_iff not_le[symmetric, of _ 0])
   4.493 -hide_fact (open) compute_is_float_pos
   4.494  
   4.495 -lemma compute_float_less[code]: "a < b \<longleftrightarrow> is_float_pos (b - a)"
   4.496 +qualified lemma compute_float_less[code]: "a < b \<longleftrightarrow> is_float_pos (b - a)"
   4.497    by transfer (simp add: field_simps)
   4.498 -hide_fact (open) compute_float_less
   4.499  
   4.500  lift_definition is_float_nonneg :: "float \<Rightarrow> bool" is "op \<le> 0 :: real \<Rightarrow> bool" .
   4.501  
   4.502 -lemma compute_is_float_nonneg[code]: "is_float_nonneg (Float m e) \<longleftrightarrow> 0 \<le> m"
   4.503 +qualified lemma compute_is_float_nonneg[code]: "is_float_nonneg (Float m e) \<longleftrightarrow> 0 \<le> m"
   4.504    by transfer (auto simp add: zero_le_mult_iff not_less[symmetric, of _ 0])
   4.505 -hide_fact (open) compute_is_float_nonneg
   4.506  
   4.507 -lemma compute_float_le[code]: "a \<le> b \<longleftrightarrow> is_float_nonneg (b - a)"
   4.508 +qualified lemma compute_float_le[code]: "a \<le> b \<longleftrightarrow> is_float_nonneg (b - a)"
   4.509    by transfer (simp add: field_simps)
   4.510 -hide_fact (open) compute_float_le
   4.511  
   4.512  lift_definition is_float_zero :: "float \<Rightarrow> bool"  is "op = 0 :: real \<Rightarrow> bool" .
   4.513  
   4.514 -lemma compute_is_float_zero[code]: "is_float_zero (Float m e) \<longleftrightarrow> 0 = m"
   4.515 +qualified lemma compute_is_float_zero[code]: "is_float_zero (Float m e) \<longleftrightarrow> 0 = m"
   4.516    by transfer (auto simp add: is_float_zero_def)
   4.517 -hide_fact (open) compute_is_float_zero
   4.518  
   4.519 -lemma compute_float_abs[code]: "abs (Float m e) = Float (abs m) e"
   4.520 +qualified lemma compute_float_abs[code]: "abs (Float m e) = Float (abs m) e"
   4.521    by transfer (simp add: abs_mult)
   4.522 -hide_fact (open) compute_float_abs
   4.523  
   4.524 -lemma compute_float_eq[code]: "equal_class.equal f g = is_float_zero (f - g)"
   4.525 +qualified lemma compute_float_eq[code]: "equal_class.equal f g = is_float_zero (f - g)"
   4.526    by transfer simp
   4.527 -hide_fact (open) compute_float_eq
   4.528 +
   4.529 +end
   4.530  
   4.531  
   4.532  subsection \<open>Lemmas for types @{typ real}, @{typ nat}, @{typ int}\<close>
   4.533 @@ -590,11 +636,11 @@
   4.534  
   4.535  subsection \<open>Rounding Real Numbers\<close>
   4.536  
   4.537 -definition round_down :: "int \<Rightarrow> real \<Rightarrow> real" where
   4.538 -  "round_down prec x = floor (x * 2 powr prec) * 2 powr -prec"
   4.539 +definition round_down :: "int \<Rightarrow> real \<Rightarrow> real"
   4.540 +  where "round_down prec x = floor (x * 2 powr prec) * 2 powr -prec"
   4.541  
   4.542 -definition round_up :: "int \<Rightarrow> real \<Rightarrow> real" where
   4.543 -  "round_up prec x = ceiling (x * 2 powr prec) * 2 powr -prec"
   4.544 +definition round_up :: "int \<Rightarrow> real \<Rightarrow> real"
   4.545 +  where "round_up prec x = ceiling (x * 2 powr prec) * 2 powr -prec"
   4.546  
   4.547  lemma round_down_float[simp]: "round_down prec x \<in> float"
   4.548    unfolding round_down_def
   4.549 @@ -692,7 +738,7 @@
   4.550    from neg have "2 powr real p \<le> 2 powr 0"
   4.551      by (intro powr_mono) auto
   4.552    also have "\<dots> \<le> \<lfloor>2 powr 0::real\<rfloor>" by simp
   4.553 -  also have "... \<le> \<lfloor>x * 2 powr (real p)\<rfloor>" 
   4.554 +  also have "\<dots> \<le> \<lfloor>x * 2 powr (real p)\<rfloor>"
   4.555      unfolding real_of_int_le_iff
   4.556      using x x_le by (intro floor_mono) (simp add: powr_minus_divide field_simps)
   4.557    finally show ?thesis
   4.558 @@ -707,9 +753,11 @@
   4.559  
   4.560  subsection \<open>Rounding Floats\<close>
   4.561  
   4.562 -definition div_twopow::"int \<Rightarrow> nat \<Rightarrow> int" where [simp]: "div_twopow x n = x div (2 ^ n)"
   4.563 +definition div_twopow :: "int \<Rightarrow> nat \<Rightarrow> int"
   4.564 +  where [simp]: "div_twopow x n = x div (2 ^ n)"
   4.565  
   4.566 -definition mod_twopow::"int \<Rightarrow> nat \<Rightarrow> int" where [simp]: "mod_twopow x n = x mod (2 ^ n)"
   4.567 +definition mod_twopow :: "int \<Rightarrow> nat \<Rightarrow> int"
   4.568 +  where [simp]: "mod_twopow x n = x mod (2 ^ n)"
   4.569  
   4.570  lemma compute_div_twopow[code]:
   4.571    "div_twopow x n = (if x = 0 \<or> x = -1 \<or> n = 0 then x else div_twopow (x div 2) (n - 1))"
   4.572 @@ -722,51 +770,54 @@
   4.573  lift_definition float_up :: "int \<Rightarrow> float \<Rightarrow> float" is round_up by simp
   4.574  declare float_up.rep_eq[simp]
   4.575  
   4.576 -lemma round_up_correct:
   4.577 -  shows "round_up e f - f \<in> {0..2 powr -e}"
   4.578 -unfolding atLeastAtMost_iff
   4.579 +lemma round_up_correct: "round_up e f - f \<in> {0..2 powr -e}"
   4.580 +  unfolding atLeastAtMost_iff
   4.581  proof
   4.582 -  have "round_up e f - f \<le> round_up e f - round_down e f" using round_down by simp
   4.583 -  also have "\<dots> \<le> 2 powr -e" using round_up_diff_round_down by simp
   4.584 +  have "round_up e f - f \<le> round_up e f - round_down e f"
   4.585 +    using round_down by simp
   4.586 +  also have "\<dots> \<le> 2 powr -e"
   4.587 +    using round_up_diff_round_down by simp
   4.588    finally show "round_up e f - f \<le> 2 powr - (real e)"
   4.589      by simp
   4.590  qed (simp add: algebra_simps round_up)
   4.591  
   4.592 -lemma float_up_correct:
   4.593 -  shows "real (float_up e f) - real f \<in> {0..2 powr -e}"
   4.594 +lemma float_up_correct: "real (float_up e f) - real f \<in> {0..2 powr -e}"
   4.595    by transfer (rule round_up_correct)
   4.596  
   4.597  lift_definition float_down :: "int \<Rightarrow> float \<Rightarrow> float" is round_down by simp
   4.598  declare float_down.rep_eq[simp]
   4.599  
   4.600 -lemma round_down_correct:
   4.601 -  shows "f - (round_down e f) \<in> {0..2 powr -e}"
   4.602 -unfolding atLeastAtMost_iff
   4.603 +lemma round_down_correct: "f - (round_down e f) \<in> {0..2 powr -e}"
   4.604 +  unfolding atLeastAtMost_iff
   4.605  proof
   4.606 -  have "f - round_down e f \<le> round_up e f - round_down e f" using round_up by simp
   4.607 -  also have "\<dots> \<le> 2 powr -e" using round_up_diff_round_down by simp
   4.608 +  have "f - round_down e f \<le> round_up e f - round_down e f"
   4.609 +    using round_up by simp
   4.610 +  also have "\<dots> \<le> 2 powr -e"
   4.611 +    using round_up_diff_round_down by simp
   4.612    finally show "f - round_down e f \<le> 2 powr - (real e)"
   4.613      by simp
   4.614  qed (simp add: algebra_simps round_down)
   4.615  
   4.616 -lemma float_down_correct:
   4.617 -  shows "real f - real (float_down e f) \<in> {0..2 powr -e}"
   4.618 +lemma float_down_correct: "real f - real (float_down e f) \<in> {0..2 powr -e}"
   4.619    by transfer (rule round_down_correct)
   4.620  
   4.621 -lemma compute_float_down[code]:
   4.622 +context
   4.623 +begin
   4.624 +
   4.625 +qualified lemma compute_float_down[code]:
   4.626    "float_down p (Float m e) =
   4.627      (if p + e < 0 then Float (div_twopow m (nat (-(p + e)))) (-p) else Float m e)"
   4.628 -proof cases
   4.629 -  assume "p + e < 0"
   4.630 -  hence "real ((2::int) ^ nat (-(p + e))) = 2 powr (-(p + e))"
   4.631 +proof (cases "p + e < 0")
   4.632 +  case True
   4.633 +  then have "real ((2::int) ^ nat (-(p + e))) = 2 powr (-(p + e))"
   4.634      using powr_realpow[of 2 "nat (-(p + e))"] by simp
   4.635 -  also have "... = 1 / 2 powr p / 2 powr e"
   4.636 +  also have "\<dots> = 1 / 2 powr p / 2 powr e"
   4.637      unfolding powr_minus_divide real_of_int_minus by (simp add: powr_add)
   4.638    finally show ?thesis
   4.639      using \<open>p + e < 0\<close>
   4.640      by transfer (simp add: ac_simps round_down_def floor_divide_eq_div[symmetric])
   4.641  next
   4.642 -  assume "\<not> p + e < 0"
   4.643 +  case False
   4.644    then have r: "real e + real p = real (nat (e + p))" by simp
   4.645    have r: "\<lfloor>(m * 2 powr e) * 2 powr real p\<rfloor> = (m * 2 powr e) * 2 powr real p"
   4.646      by (auto intro: exI[where x="m*2^nat (e+p)"]
   4.647 @@ -774,7 +825,6 @@
   4.648    with \<open>\<not> p + e < 0\<close> show ?thesis
   4.649      by transfer (auto simp add: round_down_def field_simps powr_add powr_minus)
   4.650  qed
   4.651 -hide_fact (open) compute_float_down
   4.652  
   4.653  lemma abs_round_down_le: "\<bar>f - (round_down e f)\<bar> \<le> 2 powr -e"
   4.654    using round_down_correct[of f e] by simp
   4.655 @@ -786,75 +836,100 @@
   4.656    by (auto simp: round_down_def)
   4.657  
   4.658  lemma ceil_divide_floor_conv:
   4.659 -assumes "b \<noteq> 0"
   4.660 -shows "\<lceil>real a / real b\<rceil> = (if b dvd a then a div b else \<lfloor>real a / real b\<rfloor> + 1)"
   4.661 -proof cases
   4.662 -  assume "\<not> b dvd a"
   4.663 -  hence "a mod b \<noteq> 0" by auto
   4.664 -  hence ne: "real (a mod b) / real b \<noteq> 0" using \<open>b \<noteq> 0\<close> by auto
   4.665 +  assumes "b \<noteq> 0"
   4.666 +  shows "\<lceil>real a / real b\<rceil> = (if b dvd a then a div b else \<lfloor>real a / real b\<rfloor> + 1)"
   4.667 +proof (cases "b dvd a")
   4.668 +  case True
   4.669 +  then show ?thesis
   4.670 +    by (simp add: ceiling_def real_of_int_minus[symmetric] divide_minus_left[symmetric]
   4.671 +      floor_divide_eq_div dvd_neg_div del: divide_minus_left real_of_int_minus)
   4.672 +next
   4.673 +  case False
   4.674 +  then have "a mod b \<noteq> 0"
   4.675 +    by auto
   4.676 +  then have ne: "real (a mod b) / real b \<noteq> 0"
   4.677 +    using \<open>b \<noteq> 0\<close> by auto
   4.678    have "\<lceil>real a / real b\<rceil> = \<lfloor>real a / real b\<rfloor> + 1"
   4.679 -  apply (rule ceiling_eq) apply (auto simp: floor_divide_eq_div[symmetric])
   4.680 +    apply (rule ceiling_eq)
   4.681 +    apply (auto simp: floor_divide_eq_div[symmetric])
   4.682    proof -
   4.683 -    have "real \<lfloor>real a / real b\<rfloor> \<le> real a / real b" by simp
   4.684 +    have "real \<lfloor>real a / real b\<rfloor> \<le> real a / real b"
   4.685 +      by simp
   4.686      moreover have "real \<lfloor>real a / real b\<rfloor> \<noteq> real a / real b"
   4.687 -    apply (subst (2) real_of_int_div_aux) unfolding floor_divide_eq_div using ne \<open>b \<noteq> 0\<close> by auto
   4.688 +      apply (subst (2) real_of_int_div_aux)
   4.689 +      unfolding floor_divide_eq_div
   4.690 +      using ne \<open>b \<noteq> 0\<close> apply auto
   4.691 +      done
   4.692      ultimately show "real \<lfloor>real a / real b\<rfloor> < real a / real b" by arith
   4.693    qed
   4.694 -  thus ?thesis using \<open>\<not> b dvd a\<close> by simp
   4.695 -qed (simp add: ceiling_def real_of_int_minus[symmetric] divide_minus_left[symmetric]
   4.696 -  floor_divide_eq_div dvd_neg_div del: divide_minus_left real_of_int_minus)
   4.697 +  then show ?thesis
   4.698 +    using \<open>\<not> b dvd a\<close> by simp
   4.699 +qed
   4.700  
   4.701 -lemma compute_float_up[code]:
   4.702 -  "float_up p x = - float_down p (-x)"
   4.703 +qualified lemma compute_float_up[code]: "float_up p x = - float_down p (-x)"
   4.704    by transfer (simp add: round_down_uminus_eq)
   4.705 -hide_fact (open) compute_float_up
   4.706 +
   4.707 +end
   4.708  
   4.709  
   4.710  subsection \<open>Compute bitlen of integers\<close>
   4.711  
   4.712 -definition bitlen :: "int \<Rightarrow> int" where
   4.713 -  "bitlen a = (if a > 0 then \<lfloor>log 2 a\<rfloor> + 1 else 0)"
   4.714 +definition bitlen :: "int \<Rightarrow> int"
   4.715 +  where "bitlen a = (if a > 0 then \<lfloor>log 2 a\<rfloor> + 1 else 0)"
   4.716  
   4.717  lemma bitlen_nonneg: "0 \<le> bitlen x"
   4.718  proof -
   4.719 -  {
   4.720 -    assume "0 > x"
   4.721 -    have "-1 = log 2 (inverse 2)" by (subst log_inverse) simp_all
   4.722 -    also have "... < log 2 (-x)" using \<open>0 > x\<close> by auto
   4.723 -    finally have "-1 < log 2 (-x)" .
   4.724 -  } thus "0 \<le> bitlen x" unfolding bitlen_def by (auto intro!: add_nonneg_nonneg)
   4.725 +  have "-1 < log 2 (-x)" if "0 > x"
   4.726 +  proof -
   4.727 +    have "-1 = log 2 (inverse 2)"
   4.728 +      by (subst log_inverse) simp_all
   4.729 +    also have "\<dots> < log 2 (-x)"
   4.730 +      using \<open>0 > x\<close> by auto
   4.731 +    finally show ?thesis .
   4.732 +  qed
   4.733 +  then show ?thesis
   4.734 +    unfolding bitlen_def by (auto intro!: add_nonneg_nonneg)
   4.735  qed
   4.736  
   4.737  lemma bitlen_bounds:
   4.738    assumes "x > 0"
   4.739    shows "2 ^ nat (bitlen x - 1) \<le> x \<and> x < 2 ^ nat (bitlen x)"
   4.740  proof
   4.741 -  have "(2::real) ^ nat \<lfloor>log 2 (real x)\<rfloor> = 2 powr real (floor (log 2 (real x)))"
   4.742 -    using powr_realpow[symmetric, of 2 "nat \<lfloor>log 2 (real x)\<rfloor>"] \<open>x > 0\<close>
   4.743 -    using real_nat_eq_real[of "floor (log 2 (real x))"]
   4.744 -    by simp
   4.745 -  also have "... \<le> 2 powr log 2 (real x)"
   4.746 -    by simp
   4.747 -  also have "... = real x"
   4.748 -    using \<open>0 < x\<close> by simp
   4.749 -  finally have "2 ^ nat \<lfloor>log 2 (real x)\<rfloor> \<le> real x" by simp
   4.750 -  thus "2 ^ nat (bitlen x - 1) \<le> x" using \<open>x > 0\<close>
   4.751 -    by (simp add: bitlen_def)
   4.752 -next
   4.753 -  have "x \<le> 2 powr (log 2 x)" using \<open>x > 0\<close> by simp
   4.754 -  also have "... < 2 ^ nat (\<lfloor>log 2 (real x)\<rfloor> + 1)"
   4.755 -    apply (simp add: powr_realpow[symmetric])
   4.756 -    using \<open>x > 0\<close> by simp
   4.757 -  finally show "x < 2 ^ nat (bitlen x)" using \<open>x > 0\<close>
   4.758 -    by (simp add: bitlen_def ac_simps)
   4.759 +  show "2 ^ nat (bitlen x - 1) \<le> x"
   4.760 +  proof -
   4.761 +    have "(2::real) ^ nat \<lfloor>log 2 (real x)\<rfloor> = 2 powr real (floor (log 2 (real x)))"
   4.762 +      using powr_realpow[symmetric, of 2 "nat \<lfloor>log 2 (real x)\<rfloor>"] \<open>x > 0\<close>
   4.763 +      using real_nat_eq_real[of "floor (log 2 (real x))"]
   4.764 +      by simp
   4.765 +    also have "\<dots> \<le> 2 powr log 2 (real x)"
   4.766 +      by simp
   4.767 +    also have "\<dots> = real x"
   4.768 +      using \<open>0 < x\<close> by simp
   4.769 +    finally have "2 ^ nat \<lfloor>log 2 (real x)\<rfloor> \<le> real x"
   4.770 +      by simp
   4.771 +    then show ?thesis
   4.772 +      using \<open>0 < x\<close> by (simp add: bitlen_def)
   4.773 +  qed
   4.774 +  show "x < 2 ^ nat (bitlen x)"
   4.775 +  proof -
   4.776 +    have "x \<le> 2 powr (log 2 x)"
   4.777 +      using \<open>x > 0\<close> by simp
   4.778 +    also have "\<dots> < 2 ^ nat (\<lfloor>log 2 (real x)\<rfloor> + 1)"
   4.779 +      apply (simp add: powr_realpow[symmetric])
   4.780 +      using \<open>x > 0\<close> apply simp
   4.781 +      done
   4.782 +    finally show ?thesis
   4.783 +      using \<open>x > 0\<close> by (simp add: bitlen_def ac_simps)
   4.784 +  qed
   4.785  qed
   4.786  
   4.787  lemma bitlen_pow2[simp]:
   4.788    assumes "b > 0"
   4.789    shows "bitlen (b * 2 ^ c) = bitlen b + c"
   4.790  proof -
   4.791 -  from assms have "b * 2 ^ c > 0" by auto
   4.792 -  thus ?thesis
   4.793 +  from assms have "b * 2 ^ c > 0"
   4.794 +    by auto
   4.795 +  then show ?thesis
   4.796      using floor_add[of "log 2 b" c] assms
   4.797      by (auto simp add: log_mult log_nat_power bitlen_def)
   4.798  qed
   4.799 @@ -868,9 +943,9 @@
   4.800    then show ?thesis by (simp add: f_def bitlen_def Float_def)
   4.801  next
   4.802    case False
   4.803 -  hence "f \<noteq> float_of 0"
   4.804 +  then have "f \<noteq> float_of 0"
   4.805      unfolding real_of_float_eq by (simp add: f_def)
   4.806 -  hence "mantissa f \<noteq> 0"
   4.807 +  then have "mantissa f \<noteq> 0"
   4.808      by (simp add: mantissa_noteq_0)
   4.809    moreover
   4.810    obtain i where "m = mantissa f * 2 ^ i" "e = exponent f - int i"
   4.811 @@ -878,22 +953,27 @@
   4.812    ultimately show ?thesis by (simp add: abs_mult)
   4.813  qed
   4.814  
   4.815 -lemma compute_bitlen[code]:
   4.816 -  shows "bitlen x = (if x > 0 then bitlen (x div 2) + 1 else 0)"
   4.817 +context
   4.818 +begin
   4.819 +
   4.820 +qualified lemma compute_bitlen[code]: "bitlen x = (if x > 0 then bitlen (x div 2) + 1 else 0)"
   4.821  proof -
   4.822    { assume "2 \<le> x"
   4.823      then have "\<lfloor>log 2 (x div 2)\<rfloor> + 1 = \<lfloor>log 2 (x - x mod 2)\<rfloor>"
   4.824        by (simp add: log_mult zmod_zdiv_equality')
   4.825      also have "\<dots> = \<lfloor>log 2 (real x)\<rfloor>"
   4.826 -    proof cases
   4.827 -      assume "x mod 2 = 0" then show ?thesis by simp
   4.828 +    proof (cases "x mod 2 = 0")
   4.829 +      case True
   4.830 +      then show ?thesis by simp
   4.831      next
   4.832 +      case False
   4.833        def n \<equiv> "\<lfloor>log 2 (real x)\<rfloor>"
   4.834        then have "0 \<le> n"
   4.835          using \<open>2 \<le> x\<close> by simp
   4.836 -      assume "x mod 2 \<noteq> 0"
   4.837 -      with \<open>2 \<le> x\<close> have "x mod 2 = 1" "\<not> 2 dvd x" by (auto simp add: dvd_eq_mod_eq_0)
   4.838 -      with \<open>2 \<le> x\<close> have "x \<noteq> 2^nat n" by (cases "nat n") auto
   4.839 +      from \<open>2 \<le> x\<close> False have "x mod 2 = 1" "\<not> 2 dvd x"
   4.840 +        by (auto simp add: dvd_eq_mod_eq_0)
   4.841 +      with \<open>2 \<le> x\<close> have "x \<noteq> 2 ^ nat n"
   4.842 +        by (cases "nat n") auto
   4.843        moreover
   4.844        { have "real (2^nat n :: int) = 2 powr (nat n)"
   4.845            by (simp add: powr_realpow)
   4.846 @@ -922,62 +1002,87 @@
   4.847      unfolding bitlen_def
   4.848      by (auto simp: pos_imp_zdiv_pos_iff not_le)
   4.849  qed
   4.850 -hide_fact (open) compute_bitlen
   4.851 +
   4.852 +end
   4.853  
   4.854  lemma float_gt1_scale: assumes "1 \<le> Float m e"
   4.855    shows "0 \<le> e + (bitlen m - 1)"
   4.856  proof -
   4.857    have "0 < Float m e" using assms by auto
   4.858 -  hence "0 < m" using powr_gt_zero[of 2 e]  
   4.859 +  then have "0 < m" using powr_gt_zero[of 2 e]
   4.860      apply (auto simp: zero_less_mult_iff)
   4.861 -    using not_le powr_ge_pzero by blast
   4.862 -  hence "m \<noteq> 0" by auto
   4.863 +    using not_le powr_ge_pzero apply blast
   4.864 +    done
   4.865 +  then have "m \<noteq> 0" by auto
   4.866    show ?thesis
   4.867    proof (cases "0 \<le> e")
   4.868 -    case True thus ?thesis using \<open>0 < m\<close>  by (simp add: bitlen_def)
   4.869 +    case True
   4.870 +    then show ?thesis
   4.871 +      using \<open>0 < m\<close> by (simp add: bitlen_def)
   4.872    next
   4.873 +    case False
   4.874      have "(1::int) < 2" by simp
   4.875 -    case False let ?S = "2^(nat (-e))"
   4.876 -    have "inverse (2 ^ nat (- e)) = 2 powr e" using assms False powr_realpow[of 2 "nat (-e)"]
   4.877 +    let ?S = "2^(nat (-e))"
   4.878 +    have "inverse (2 ^ nat (- e)) = 2 powr e"
   4.879 +      using assms False powr_realpow[of 2 "nat (-e)"]
   4.880        by (auto simp: powr_minus field_simps)
   4.881 -    hence "1 \<le> real m * inverse ?S" using assms False powr_realpow[of 2 "nat (-e)"]
   4.882 +    then have "1 \<le> real m * inverse ?S"
   4.883 +      using assms False powr_realpow[of 2 "nat (-e)"]
   4.884        by (auto simp: powr_minus)
   4.885 -    hence "1 * ?S \<le> real m * inverse ?S * ?S" by (rule mult_right_mono, auto)
   4.886 -    hence "?S \<le> real m" unfolding mult.assoc by auto
   4.887 -    hence "?S \<le> m" unfolding real_of_int_le_iff[symmetric] by auto
   4.888 +    then have "1 * ?S \<le> real m * inverse ?S * ?S"
   4.889 +      by (rule mult_right_mono) auto
   4.890 +    then have "?S \<le> real m"
   4.891 +      unfolding mult.assoc by auto
   4.892 +    then have "?S \<le> m"
   4.893 +      unfolding real_of_int_le_iff[symmetric] by auto
   4.894      from this bitlen_bounds[OF \<open>0 < m\<close>, THEN conjunct2]
   4.895 -    have "nat (-e) < (nat (bitlen m))" unfolding power_strict_increasing_iff[OF \<open>1 < 2\<close>, symmetric]
   4.896 +    have "nat (-e) < (nat (bitlen m))"
   4.897 +      unfolding power_strict_increasing_iff[OF \<open>1 < 2\<close>, symmetric]
   4.898        by (rule order_le_less_trans)
   4.899 -    hence "-e < bitlen m" using False by auto
   4.900 -    thus ?thesis by auto
   4.901 +    then have "-e < bitlen m"
   4.902 +      using False by auto
   4.903 +    then show ?thesis
   4.904 +      by auto
   4.905    qed
   4.906  qed
   4.907  
   4.908  lemma bitlen_div:
   4.909    assumes "0 < m"
   4.910 -  shows "1 \<le> real m / 2^nat (bitlen m - 1)" and "real m / 2^nat (bitlen m - 1) < 2"
   4.911 +  shows "1 \<le> real m / 2^nat (bitlen m - 1)"
   4.912 +    and "real m / 2^nat (bitlen m - 1) < 2"
   4.913  proof -
   4.914    let ?B = "2^nat(bitlen m - 1)"
   4.915  
   4.916    have "?B \<le> m" using bitlen_bounds[OF \<open>0 <m\<close>] ..
   4.917 -  hence "1 * ?B \<le> real m" unfolding real_of_int_le_iff[symmetric] by auto
   4.918 -  thus "1 \<le> real m / ?B" by auto
   4.919 +  then have "1 * ?B \<le> real m"
   4.920 +    unfolding real_of_int_le_iff[symmetric] by auto
   4.921 +  then show "1 \<le> real m / ?B"
   4.922 +    by auto
   4.923  
   4.924 -  have "m \<noteq> 0" using assms by auto
   4.925 -  have "0 \<le> bitlen m - 1" using \<open>0 < m\<close> by (auto simp: bitlen_def)
   4.926 +  have "m \<noteq> 0"
   4.927 +    using assms by auto
   4.928 +  have "0 \<le> bitlen m - 1"
   4.929 +    using \<open>0 < m\<close> by (auto simp: bitlen_def)
   4.930  
   4.931 -  have "m < 2^nat(bitlen m)" using bitlen_bounds[OF \<open>0 <m\<close>] ..
   4.932 -  also have "\<dots> = 2^nat(bitlen m - 1 + 1)" using \<open>0 < m\<close> by (auto simp: bitlen_def)
   4.933 -  also have "\<dots> = ?B * 2" unfolding nat_add_distrib[OF \<open>0 \<le> bitlen m - 1\<close> zero_le_one] by auto
   4.934 -  finally have "real m < 2 * ?B" unfolding real_of_int_less_iff[symmetric] by auto
   4.935 -  hence "real m / ?B < 2 * ?B / ?B" by (rule divide_strict_right_mono, auto)
   4.936 -  thus "real m / ?B < 2" by auto
   4.937 +  have "m < 2^nat(bitlen m)"
   4.938 +    using bitlen_bounds[OF \<open>0 <m\<close>] ..
   4.939 +  also have "\<dots> = 2^nat(bitlen m - 1 + 1)"
   4.940 +    using \<open>0 < m\<close> by (auto simp: bitlen_def)
   4.941 +  also have "\<dots> = ?B * 2"
   4.942 +    unfolding nat_add_distrib[OF \<open>0 \<le> bitlen m - 1\<close> zero_le_one] by auto
   4.943 +  finally have "real m < 2 * ?B"
   4.944 +    unfolding real_of_int_less_iff[symmetric] by auto
   4.945 +  then have "real m / ?B < 2 * ?B / ?B"
   4.946 +    by (rule divide_strict_right_mono) auto
   4.947 +  then show "real m / ?B < 2"
   4.948 +    by auto
   4.949  qed
   4.950  
   4.951 +
   4.952  subsection \<open>Truncating Real Numbers\<close>
   4.953  
   4.954 -definition truncate_down::"nat \<Rightarrow> real \<Rightarrow> real" where
   4.955 -  "truncate_down prec x = round_down (prec - \<lfloor>log 2 \<bar>x\<bar>\<rfloor> - 1) x"
   4.956 +definition truncate_down::"nat \<Rightarrow> real \<Rightarrow> real"
   4.957 +  where "truncate_down prec x = round_down (prec - \<lfloor>log 2 \<bar>x\<bar>\<rfloor> - 1) x"
   4.958  
   4.959  lemma truncate_down: "truncate_down prec x \<le> x"
   4.960    using round_down by (simp add: truncate_down_def)
   4.961 @@ -991,8 +1096,8 @@
   4.962  lemma truncate_down_float[simp]: "truncate_down p x \<in> float"
   4.963    by (auto simp: truncate_down_def)
   4.964  
   4.965 -definition truncate_up::"nat \<Rightarrow> real \<Rightarrow> real" where
   4.966 -  "truncate_up prec x = round_up (prec - \<lfloor>log 2 \<bar>x\<bar>\<rfloor> - 1) x"
   4.967 +definition truncate_up::"nat \<Rightarrow> real \<Rightarrow> real"
   4.968 +  where "truncate_up prec x = round_up (prec - \<lfloor>log 2 \<bar>x\<bar>\<rfloor> - 1) x"
   4.969  
   4.970  lemma truncate_up: "x \<le> truncate_up prec x"
   4.971    using round_up by (simp add: truncate_up_def)
   4.972 @@ -1035,22 +1140,28 @@
   4.973    by (auto simp: truncate_up_def round_up_def intro!: mult_nonpos_nonneg)
   4.974  
   4.975  lemma truncate_up_le1:
   4.976 -  assumes "x \<le> 1" "1 \<le> p" shows "truncate_up p x \<le> 1"
   4.977 +  assumes "x \<le> 1" "1 \<le> p"
   4.978 +  shows "truncate_up p x \<le> 1"
   4.979  proof -
   4.980 -  {
   4.981 -    assume "x \<le> 0"
   4.982 -    with truncate_up_nonpos[OF this, of p] have ?thesis by simp
   4.983 -  } moreover {
   4.984 -    assume "x > 0"
   4.985 -    hence le: "\<lfloor>log 2 \<bar>x\<bar>\<rfloor> \<le> 0"
   4.986 +  consider "x \<le> 0" | "x > 0"
   4.987 +    by arith
   4.988 +  then show ?thesis
   4.989 +  proof cases
   4.990 +    case 1
   4.991 +    with truncate_up_nonpos[OF this, of p] show ?thesis
   4.992 +      by simp
   4.993 +  next
   4.994 +    case 2
   4.995 +    then have le: "\<lfloor>log 2 \<bar>x\<bar>\<rfloor> \<le> 0"
   4.996        using assms by (auto simp: log_less_iff)
   4.997      from assms have "1 \<le> int p" by simp
   4.998      from add_mono[OF this le]
   4.999 -    have ?thesis using assms
  4.1000 -      by (simp add: truncate_up_def round_up_le1 add_mono)
  4.1001 -  } ultimately show ?thesis by arith
  4.1002 +    show ?thesis
  4.1003 +      using assms by (simp add: truncate_up_def round_up_le1 add_mono)
  4.1004 +  qed
  4.1005  qed
  4.1006  
  4.1007 +
  4.1008  subsection \<open>Truncating Floats\<close>
  4.1009  
  4.1010  lift_definition float_round_up :: "nat \<Rightarrow> float \<Rightarrow> float" is truncate_up
  4.1011 @@ -1078,25 +1189,30 @@
  4.1012    and minus_float_round_down_eq: "- float_round_down prec x = float_round_up prec (- x)"
  4.1013    by (transfer, simp add: truncate_down_uminus_eq truncate_up_uminus_eq)+
  4.1014  
  4.1015 -lemma compute_float_round_down[code]:
  4.1016 +context
  4.1017 +begin
  4.1018 +
  4.1019 +qualified lemma compute_float_round_down[code]:
  4.1020    "float_round_down prec (Float m e) = (let d = bitlen (abs m) - int prec in
  4.1021      if 0 < d then Float (div_twopow m (nat d)) (e + d)
  4.1022               else Float m e)"
  4.1023    using Float.compute_float_down[of "prec - bitlen \<bar>m\<bar> - e" m e, symmetric]
  4.1024    by transfer (simp add: field_simps abs_mult log_mult bitlen_def truncate_down_def
  4.1025      cong del: if_weak_cong)
  4.1026 -hide_fact (open) compute_float_round_down
  4.1027  
  4.1028 -lemma compute_float_round_up[code]:
  4.1029 +qualified lemma compute_float_round_up[code]:
  4.1030    "float_round_up prec x = - float_round_down prec (-x)"
  4.1031    by transfer (simp add: truncate_down_uminus_eq)
  4.1032 -hide_fact (open) compute_float_round_up
  4.1033 +
  4.1034 +end
  4.1035  
  4.1036  
  4.1037  subsection \<open>Approximation of positive rationals\<close>
  4.1038  
  4.1039 -lemma div_mult_twopow_eq: fixes a b::nat shows "a div ((2::nat) ^ n) div b = a div (b * 2 ^ n)"
  4.1040 -  by (cases "b=0") (simp_all add: div_mult2_eq[symmetric] ac_simps)
  4.1041 +lemma div_mult_twopow_eq:
  4.1042 +  fixes a b :: nat
  4.1043 +  shows "a div ((2::nat) ^ n) div b = a div (b * 2 ^ n)"
  4.1044 +  by (cases "b = 0") (simp_all add: div_mult2_eq[symmetric] ac_simps)
  4.1045  
  4.1046  lemma real_div_nat_eq_floor_of_divide:
  4.1047    fixes a b :: nat
  4.1048 @@ -1106,23 +1222,29 @@
  4.1049  definition "rat_precision prec x y = int prec - (bitlen x - bitlen y)"
  4.1050  
  4.1051  lift_definition lapprox_posrat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> float"
  4.1052 -  is "\<lambda>prec (x::nat) (y::nat). round_down (rat_precision prec x y) (x / y)" by simp
  4.1053 +  is "\<lambda>prec (x::nat) (y::nat). round_down (rat_precision prec x y) (x / y)"
  4.1054 +  by simp
  4.1055  
  4.1056 -lemma compute_lapprox_posrat[code]:
  4.1057 +context
  4.1058 +begin
  4.1059 +
  4.1060 +qualified lemma compute_lapprox_posrat[code]:
  4.1061    fixes prec x y
  4.1062    shows "lapprox_posrat prec x y =
  4.1063     (let
  4.1064 -       l = rat_precision prec x y;
  4.1065 -       d = if 0 \<le> l then x * 2^nat l div y else x div 2^nat (- l) div y
  4.1066 +      l = rat_precision prec x y;
  4.1067 +      d = if 0 \<le> l then x * 2^nat l div y else x div 2^nat (- l) div y
  4.1068      in normfloat (Float d (- l)))"
  4.1069      unfolding div_mult_twopow_eq
  4.1070      by transfer
  4.1071         (simp add: round_down_def powr_int real_div_nat_eq_floor_of_divide field_simps Let_def
  4.1072               del: two_powr_minus_int_float)
  4.1073 -hide_fact (open) compute_lapprox_posrat
  4.1074 +
  4.1075 +end
  4.1076  
  4.1077  lift_definition rapprox_posrat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> float"
  4.1078 -  is "\<lambda>prec (x::nat) (y::nat). round_up (rat_precision prec x y) (x / y)" by simp
  4.1079 +  is "\<lambda>prec (x::nat) (y::nat). round_up (rat_precision prec x y) (x / y)" by
  4.1080 +  simp
  4.1081  
  4.1082  context
  4.1083    notes divmod_int_mod_div[simp]
  4.1084 @@ -1137,14 +1259,16 @@
  4.1085       (d, m) = divmod_int (fst X) (snd X)
  4.1086     in normfloat (Float (d + (if m = 0 \<or> y = 0 then 0 else 1)) (- l)))"
  4.1087  proof (cases "y = 0")
  4.1088 -  assume "y = 0" thus ?thesis by transfer simp
  4.1089 +  assume "y = 0"
  4.1090 +  then show ?thesis by transfer simp
  4.1091  next
  4.1092    assume "y \<noteq> 0"
  4.1093    show ?thesis
  4.1094    proof (cases "0 \<le> l")
  4.1095 -    assume "0 \<le> l"
  4.1096 +    case True
  4.1097      def x' \<equiv> "x * 2 ^ nat l"
  4.1098 -    have "int x * 2 ^ nat l = x'" by (simp add: x'_def int_mult int_power)
  4.1099 +    have "int x * 2 ^ nat l = x'"
  4.1100 +      by (simp add: x'_def int_mult int_power)
  4.1101      moreover have "real x * 2 powr real l = real x'"
  4.1102        by (simp add: powr_realpow[symmetric] \<open>0 \<le> l\<close> x'_def)
  4.1103      ultimately show ?thesis
  4.1104 @@ -1152,7 +1276,7 @@
  4.1105          l_def[symmetric, THEN meta_eq_to_obj_eq]
  4.1106        by transfer (auto simp add: floor_divide_eq_div [symmetric] round_up_def)
  4.1107     next
  4.1108 -    assume "\<not> 0 \<le> l"
  4.1109 +    case False
  4.1110      def y' \<equiv> "y * 2 ^ nat (- l)"
  4.1111      from \<open>y \<noteq> 0\<close> have "y' \<noteq> 0" by (simp add: y'_def)
  4.1112      have "int y * 2 ^ nat (- l) = y'" by (simp add: y'_def int_mult int_power)
  4.1113 @@ -1170,38 +1294,48 @@
  4.1114  end
  4.1115  
  4.1116  lemma rat_precision_pos:
  4.1117 -  assumes "0 \<le> x" and "0 < y" and "2 * x < y" and "0 < n"
  4.1118 +  assumes "0 \<le> x"
  4.1119 +    and "0 < y"
  4.1120 +    and "2 * x < y"
  4.1121 +    and "0 < n"
  4.1122    shows "rat_precision n (int x) (int y) > 0"
  4.1123  proof -
  4.1124 -  { assume "0 < x" hence "log 2 x + 1 = log 2 (2 * x)" by (simp add: log_mult) }
  4.1125 -  hence "bitlen (int x) < bitlen (int y)" using assms
  4.1126 +  have "0 < x \<Longrightarrow> log 2 x + 1 = log 2 (2 * x)"
  4.1127 +    by (simp add: log_mult)
  4.1128 +  then have "bitlen (int x) < bitlen (int y)"
  4.1129 +    using assms
  4.1130      by (simp add: bitlen_def del: floor_add_one)
  4.1131        (auto intro!: floor_mono simp add: floor_add_one[symmetric] simp del: floor_add floor_add_one)
  4.1132 -  thus ?thesis
  4.1133 -    using assms by (auto intro!: pos_add_strict simp add: field_simps rat_precision_def)
  4.1134 +  then show ?thesis
  4.1135 +    using assms
  4.1136 +    by (auto intro!: pos_add_strict simp add: field_simps rat_precision_def)
  4.1137  qed
  4.1138  
  4.1139  lemma rapprox_posrat_less1:
  4.1140 -  shows "0 \<le> x \<Longrightarrow> 0 < y \<Longrightarrow> 2 * x < y \<Longrightarrow> 0 < n \<Longrightarrow> real (rapprox_posrat n x y) < 1"
  4.1141 +  "0 \<le> x \<Longrightarrow> 0 < y \<Longrightarrow> 2 * x < y \<Longrightarrow> 0 < n \<Longrightarrow> real (rapprox_posrat n x y) < 1"
  4.1142    by transfer (simp add: rat_precision_pos round_up_less1)
  4.1143  
  4.1144  lift_definition lapprox_rat :: "nat \<Rightarrow> int \<Rightarrow> int \<Rightarrow> float" is
  4.1145 -  "\<lambda>prec (x::int) (y::int). round_down (rat_precision prec \<bar>x\<bar> \<bar>y\<bar>) (x / y)" by simp
  4.1146 +  "\<lambda>prec (x::int) (y::int). round_down (rat_precision prec \<bar>x\<bar> \<bar>y\<bar>) (x / y)"
  4.1147 +  by simp
  4.1148  
  4.1149 -lemma compute_lapprox_rat[code]:
  4.1150 +context
  4.1151 +begin
  4.1152 +
  4.1153 +qualified lemma compute_lapprox_rat[code]:
  4.1154    "lapprox_rat prec x y =
  4.1155 -    (if y = 0 then 0
  4.1156 +   (if y = 0 then 0
  4.1157      else if 0 \<le> x then
  4.1158 -      (if 0 < y then lapprox_posrat prec (nat x) (nat y)
  4.1159 +     (if 0 < y then lapprox_posrat prec (nat x) (nat y)
  4.1160        else - (rapprox_posrat prec (nat x) (nat (-y))))
  4.1161        else (if 0 < y
  4.1162          then - (rapprox_posrat prec (nat (-x)) (nat y))
  4.1163          else lapprox_posrat prec (nat (-x)) (nat (-y))))"
  4.1164    by transfer (auto simp: round_up_def round_down_def ceiling_def ac_simps)
  4.1165 -hide_fact (open) compute_lapprox_rat
  4.1166  
  4.1167  lift_definition rapprox_rat :: "nat \<Rightarrow> int \<Rightarrow> int \<Rightarrow> float" is
  4.1168 -  "\<lambda>prec (x::int) (y::int). round_up (rat_precision prec \<bar>x\<bar> \<bar>y\<bar>) (x / y)" by simp
  4.1169 +  "\<lambda>prec (x::int) (y::int). round_up (rat_precision prec \<bar>x\<bar> \<bar>y\<bar>) (x / y)"
  4.1170 +  by simp
  4.1171  
  4.1172  lemma "rapprox_rat = rapprox_posrat"
  4.1173    by transfer auto
  4.1174 @@ -1209,10 +1343,12 @@
  4.1175  lemma "lapprox_rat = lapprox_posrat"
  4.1176    by transfer auto
  4.1177  
  4.1178 -lemma compute_rapprox_rat[code]:
  4.1179 +qualified lemma compute_rapprox_rat[code]:
  4.1180    "rapprox_rat prec x y = - lapprox_rat prec (-x) y"
  4.1181    by transfer (simp add: round_down_uminus_eq)
  4.1182 -hide_fact (open) compute_rapprox_rat
  4.1183 +
  4.1184 +end
  4.1185 +
  4.1186  
  4.1187  subsection \<open>Division\<close>
  4.1188  
  4.1189 @@ -1223,47 +1359,58 @@
  4.1190  lift_definition float_divl :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" is real_divl
  4.1191    by (simp add: real_divl_def)
  4.1192  
  4.1193 -lemma compute_float_divl[code]:
  4.1194 +context
  4.1195 +begin
  4.1196 +
  4.1197 +qualified lemma compute_float_divl[code]:
  4.1198    "float_divl prec (Float m1 s1) (Float m2 s2) = lapprox_rat prec m1 m2 * Float 1 (s1 - s2)"
  4.1199 -proof cases
  4.1200 +proof (cases "m1 \<noteq> 0 \<and> m2 \<noteq> 0")
  4.1201 +  case True
  4.1202    let ?f1 = "real m1 * 2 powr real s1" and ?f2 = "real m2 * 2 powr real s2"
  4.1203    let ?m = "real m1 / real m2" and ?s = "2 powr real (s1 - s2)"
  4.1204 -  assume not_0: "m1 \<noteq> 0 \<and> m2 \<noteq> 0"
  4.1205 -  then have eq2: "(int prec + \<lfloor>log 2 \<bar>?f2\<bar>\<rfloor> - \<lfloor>log 2 \<bar>?f1\<bar>\<rfloor>) = rat_precision prec \<bar>m1\<bar> \<bar>m2\<bar> + (s2 - s1)"
  4.1206 +  from True have eq2: "(int prec + \<lfloor>log 2 \<bar>?f2\<bar>\<rfloor> - \<lfloor>log 2 \<bar>?f1\<bar>\<rfloor>) =
  4.1207 +    rat_precision prec \<bar>m1\<bar> \<bar>m2\<bar> + (s2 - s1)"
  4.1208      by (simp add: abs_mult log_mult rat_precision_def bitlen_def)
  4.1209    have eq1: "real m1 * 2 powr real s1 / (real m2 * 2 powr real s2) = ?m * ?s"
  4.1210      by (simp add: field_simps powr_divide2[symmetric])
  4.1211 -
  4.1212 -  show ?thesis
  4.1213 -    using not_0
  4.1214 +  from True show ?thesis
  4.1215      by (transfer fixing: m1 s1 m2 s2 prec) (unfold eq1 eq2 round_down_shift real_divl_def,
  4.1216        simp add: field_simps)
  4.1217 -qed (transfer, auto simp: real_divl_def)
  4.1218 -hide_fact (open) compute_float_divl
  4.1219 +next
  4.1220 +  case False
  4.1221 +  then show ?thesis by transfer (auto simp: real_divl_def)
  4.1222 +qed
  4.1223  
  4.1224  lift_definition float_divr :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" is real_divr
  4.1225    by (simp add: real_divr_def)
  4.1226  
  4.1227 -lemma compute_float_divr[code]:
  4.1228 +qualified lemma compute_float_divr[code]:
  4.1229    "float_divr prec x y = - float_divl prec (-x) y"
  4.1230    by transfer (simp add: real_divr_def real_divl_def round_down_uminus_eq)
  4.1231 -hide_fact (open) compute_float_divr
  4.1232 +
  4.1233 +end
  4.1234  
  4.1235  
  4.1236  subsection \<open>Approximate Power\<close>
  4.1237  
  4.1238 -lemma div2_less_self[termination_simp]: fixes n::nat shows "odd n \<Longrightarrow> n div 2 < n"
  4.1239 +lemma div2_less_self[termination_simp]:
  4.1240 +  fixes n :: nat
  4.1241 +  shows "odd n \<Longrightarrow> n div 2 < n"
  4.1242    by (simp add: odd_pos)
  4.1243  
  4.1244 -fun power_down :: "nat \<Rightarrow> real \<Rightarrow> nat \<Rightarrow> real" where
  4.1245 +fun power_down :: "nat \<Rightarrow> real \<Rightarrow> nat \<Rightarrow> real"
  4.1246 +where
  4.1247    "power_down p x 0 = 1"
  4.1248  | "power_down p x (Suc n) =
  4.1249 -    (if odd n then truncate_down (Suc p) ((power_down p x (Suc n div 2))\<^sup>2) else truncate_down (Suc p) (x * power_down p x n))"
  4.1250 +    (if odd n then truncate_down (Suc p) ((power_down p x (Suc n div 2))\<^sup>2)
  4.1251 +     else truncate_down (Suc p) (x * power_down p x n))"
  4.1252  
  4.1253 -fun power_up :: "nat \<Rightarrow> real \<Rightarrow> nat \<Rightarrow> real" where
  4.1254 +fun power_up :: "nat \<Rightarrow> real \<Rightarrow> nat \<Rightarrow> real"
  4.1255 +where
  4.1256    "power_up p x 0 = 1"
  4.1257  | "power_up p x (Suc n) =
  4.1258 -    (if odd n then truncate_up p ((power_up p x (Suc n div 2))\<^sup>2) else truncate_up p (x * power_up p x n))"
  4.1259 +    (if odd n then truncate_up p ((power_up p x (Suc n div 2))\<^sup>2)
  4.1260 +     else truncate_up p (x * power_up p x n))"
  4.1261  
  4.1262  lift_definition power_up_fl :: "nat \<Rightarrow> float \<Rightarrow> nat \<Rightarrow> float" is power_up
  4.1263    by (induct_tac rule: power_up.induct) simp_all
  4.1264 @@ -1279,11 +1426,13 @@
  4.1265  lemma compute_power_up_fl[code]:
  4.1266    "power_up_fl p x 0 = 1"
  4.1267    "power_up_fl p x (Suc n) =
  4.1268 -    (if odd n then float_round_up p ((power_up_fl p x (Suc n div 2))\<^sup>2) else float_round_up p (x * power_up_fl p x n))"
  4.1269 +    (if odd n then float_round_up p ((power_up_fl p x (Suc n div 2))\<^sup>2)
  4.1270 +     else float_round_up p (x * power_up_fl p x n))"
  4.1271    and compute_power_down_fl[code]:
  4.1272    "power_down_fl p x 0 = 1"
  4.1273    "power_down_fl p x (Suc n) =
  4.1274 -    (if odd n then float_round_down (Suc p) ((power_down_fl p x (Suc n div 2))\<^sup>2) else float_round_down (Suc p) (x * power_down_fl p x n))"
  4.1275 +    (if odd n then float_round_down (Suc p) ((power_down_fl p x (Suc n div 2))\<^sup>2)
  4.1276 +     else float_round_down (Suc p) (x * power_down_fl p x n))"
  4.1277    unfolding atomize_conj
  4.1278    by transfer simp
  4.1279  
  4.1280 @@ -1300,7 +1449,7 @@
  4.1281    case (2 p x n)
  4.1282    {
  4.1283      assume "odd n"
  4.1284 -    hence "(power_down p x (Suc n div 2)) ^ 2 \<le> (x ^ (Suc n div 2)) ^ 2"
  4.1285 +    then have "(power_down p x (Suc n div 2)) ^ 2 \<le> (x ^ (Suc n div 2)) ^ 2"
  4.1286        using 2
  4.1287        by (auto intro: power_mono power_down_nonneg simp del: odd_Suc_div_two)
  4.1288      also have "\<dots> = x ^ (Suc n div 2 * 2)"
  4.1289 @@ -1310,7 +1459,8 @@
  4.1290      finally have ?case
  4.1291        using \<open>odd n\<close>
  4.1292        by (auto intro!: truncate_down_le simp del: odd_Suc_div_two)
  4.1293 -  } thus ?case
  4.1294 +  }
  4.1295 +  then show ?case
  4.1296      by (auto intro!: truncate_down_le mult_left_mono 2 mult_nonneg_nonneg power_down_nonneg)
  4.1297  qed simp
  4.1298  
  4.1299 @@ -1319,9 +1469,9 @@
  4.1300    case (2 p x n)
  4.1301    {
  4.1302      assume "odd n"
  4.1303 -    hence "Suc n = Suc n div 2 * 2"
  4.1304 +    then have "Suc n = Suc n div 2 * 2"
  4.1305        using \<open>odd n\<close> even_Suc by presburger
  4.1306 -    hence "x ^ Suc n \<le> (x ^ (Suc n div 2))\<^sup>2"
  4.1307 +    then have "x ^ Suc n \<le> (x ^ (Suc n div 2))\<^sup>2"
  4.1308        by (simp add: power_mult[symmetric])
  4.1309      also have "\<dots> \<le> (power_up p x (Suc n div 2))\<^sup>2"
  4.1310        using 2 \<open>odd n\<close>
  4.1311 @@ -1329,7 +1479,8 @@
  4.1312      finally have ?case
  4.1313        using \<open>odd n\<close>
  4.1314        by (auto intro!: truncate_up_le simp del: odd_Suc_div_two )
  4.1315 -  } thus ?case
  4.1316 +  }
  4.1317 +  then show ?case
  4.1318      by (auto intro!: truncate_up_le mult_left_mono 2)
  4.1319  qed simp
  4.1320  
  4.1321 @@ -1383,8 +1534,7 @@
  4.1322    using truncate_down_uminus_eq[of p "x + y"]
  4.1323    by (auto simp: plus_down_def plus_up_def)
  4.1324  
  4.1325 -lemma
  4.1326 -  truncate_down_log2_eqI:
  4.1327 +lemma truncate_down_log2_eqI:
  4.1328    assumes "\<lfloor>log 2 \<bar>x\<bar>\<rfloor> = \<lfloor>log 2 \<bar>y\<bar>\<rfloor>"
  4.1329    assumes "\<lfloor>x * 2 powr (p - \<lfloor>log 2 \<bar>x\<bar>\<rfloor> - 1)\<rfloor> = \<lfloor>y * 2 powr (p - \<lfloor>log 2 \<bar>x\<bar>\<rfloor> - 1)\<rfloor>"
  4.1330    shows "truncate_down p x = truncate_down p y"
  4.1331 @@ -1395,40 +1545,43 @@
  4.1332      (metis Float.compute_bitlen add.commute bitlen_def bitlen_nonneg less_add_same_cancel2 not_less
  4.1333        zero_less_one)
  4.1334  
  4.1335 -lemma
  4.1336 -  sum_neq_zeroI:
  4.1337 -  fixes a k::real
  4.1338 +lemma sum_neq_zeroI:
  4.1339 +  fixes a k :: real
  4.1340    shows "abs a \<ge> k \<Longrightarrow> abs b < k \<Longrightarrow> a + b \<noteq> 0"
  4.1341      and "abs a > k \<Longrightarrow> abs b \<le> k \<Longrightarrow> a + b \<noteq> 0"
  4.1342    by auto
  4.1343  
  4.1344 -lemma
  4.1345 -  abs_real_le_2_powr_bitlen[simp]:
  4.1346 -  "\<bar>real m2\<bar> < 2 powr real (bitlen \<bar>m2\<bar>)"
  4.1347 -proof cases
  4.1348 -  assume "m2 \<noteq> 0"
  4.1349 -  hence "\<bar>m2\<bar> < 2 ^ nat (bitlen \<bar>m2\<bar>)"
  4.1350 +lemma abs_real_le_2_powr_bitlen[simp]: "\<bar>real m2\<bar> < 2 powr real (bitlen \<bar>m2\<bar>)"
  4.1351 +proof (cases "m2 = 0")
  4.1352 +  case True
  4.1353 +  then show ?thesis by simp
  4.1354 +next
  4.1355 +  case False
  4.1356 +  then have "\<bar>m2\<bar> < 2 ^ nat (bitlen \<bar>m2\<bar>)"
  4.1357      using bitlen_bounds[of "\<bar>m2\<bar>"]
  4.1358      by (auto simp: powr_add bitlen_nonneg)
  4.1359 -  thus ?thesis
  4.1360 +  then show ?thesis
  4.1361      by (simp add: powr_int bitlen_nonneg real_of_int_less_iff[symmetric])
  4.1362 -qed simp
  4.1363 +qed
  4.1364  
  4.1365  lemma floor_sum_times_2_powr_sgn_eq:
  4.1366 -  fixes ai p q::int
  4.1367 -  and a b::real
  4.1368 +  fixes ai p q :: int
  4.1369 +    and a b :: real
  4.1370    assumes "a * 2 powr p = ai"
  4.1371 -  assumes b_le_1: "abs (b * 2 powr (p + 1)) \<le> 1"
  4.1372 -  assumes leqp: "q \<le> p"
  4.1373 +    and b_le_1: "abs (b * 2 powr (p + 1)) \<le> 1"
  4.1374 +    and leqp: "q \<le> p"
  4.1375    shows "\<lfloor>(a + b) * 2 powr q\<rfloor> = \<lfloor>(2 * ai + sgn b) * 2 powr (q - p - 1)\<rfloor>"
  4.1376  proof -
  4.1377 -  {
  4.1378 -    assume "b = 0"
  4.1379 -    hence ?thesis
  4.1380 +  consider "b = 0" | "b > 0" | "b < 0" by arith
  4.1381 +  then show ?thesis
  4.1382 +  proof cases
  4.1383 +    case 1
  4.1384 +    then show ?thesis
  4.1385        by (simp add: assms(1)[symmetric] powr_add[symmetric] algebra_simps powr_mult_base)
  4.1386 -  } moreover {
  4.1387 -    assume "b > 0"
  4.1388 -    hence "b * 2 powr p < abs (b * 2 powr (p + 1))" by simp
  4.1389 +  next
  4.1390 +    case 2
  4.1391 +    then have "b * 2 powr p < abs (b * 2 powr (p + 1))"
  4.1392 +      by simp
  4.1393      also note b_le_1
  4.1394      finally have b_less_1: "b * 2 powr real p < 1" .
  4.1395  
  4.1396 @@ -1455,13 +1608,12 @@
  4.1397          by (simp del: real_of_int_power add: floor_divide_real_eq_div floor_eq)
  4.1398        finally
  4.1399        have "\<lfloor>(2 * ai + (sgn b)) * 2 powr (real (q - p) - 1)\<rfloor> =
  4.1400 -          \<lfloor>real ai / real ((2::int) ^ nat (p - q))\<rfloor>"
  4.1401 -        .
  4.1402 -    } ultimately have ?thesis by simp
  4.1403 -  } moreover {
  4.1404 -    assume "\<not> 0 \<le> b"
  4.1405 -    hence "0 > b" by simp
  4.1406 -    hence floor_eq: "\<lfloor>b * 2 powr (real p + 1)\<rfloor> = -1"
  4.1407 +          \<lfloor>real ai / real ((2::int) ^ nat (p - q))\<rfloor>" .
  4.1408 +    }
  4.1409 +    ultimately show ?thesis by simp
  4.1410 +  next
  4.1411 +    case 3
  4.1412 +    then have floor_eq: "\<lfloor>b * 2 powr (real p + 1)\<rfloor> = -1"
  4.1413        using b_le_1
  4.1414        by (auto simp: floor_eq_iff algebra_simps pos_divide_le_eq[symmetric] abs_if divide_powr_uminus
  4.1415          intro!: mult_neg_pos split: split_if_asm)
  4.1416 @@ -1479,22 +1631,26 @@
  4.1417          del: real_of_int_mult real_of_int_power real_of_int_diff)
  4.1418      also have "\<dots> = \<lfloor>(2 * ai - 1) * 2 powr (q - p - 1)\<rfloor>"
  4.1419        using assms by (simp add: algebra_simps divide_powr_uminus powr_realpow[symmetric])
  4.1420 -    finally have ?thesis using \<open>b < 0\<close> by simp
  4.1421 -  } ultimately show ?thesis by arith
  4.1422 +    finally show ?thesis
  4.1423 +      using \<open>b < 0\<close> by simp
  4.1424 +  qed
  4.1425  qed
  4.1426  
  4.1427 -lemma
  4.1428 -  log2_abs_int_add_less_half_sgn_eq:
  4.1429 -  fixes ai::int and b::real
  4.1430 -  assumes "abs b \<le> 1/2" "ai \<noteq> 0"
  4.1431 +lemma log2_abs_int_add_less_half_sgn_eq:
  4.1432 +  fixes ai :: int
  4.1433 +    and b :: real
  4.1434 +  assumes "abs b \<le> 1/2"
  4.1435 +    and "ai \<noteq> 0"
  4.1436    shows "\<lfloor>log 2 \<bar>real ai + b\<bar>\<rfloor> = \<lfloor>log 2 \<bar>ai + sgn b / 2\<bar>\<rfloor>"
  4.1437 -proof cases
  4.1438 -  assume "b = 0" thus ?thesis by simp
  4.1439 +proof (cases "b = 0")
  4.1440 +  case True
  4.1441 +  then show ?thesis by simp
  4.1442  next
  4.1443 -  assume "b \<noteq> 0"
  4.1444 +  case False
  4.1445    def k \<equiv> "\<lfloor>log 2 \<bar>ai\<bar>\<rfloor>"
  4.1446 -  hence "\<lfloor>log 2 \<bar>ai\<bar>\<rfloor> = k" by simp
  4.1447 -  hence k: "2 powr k \<le> \<bar>ai\<bar>" "\<bar>ai\<bar> < 2 powr (k + 1)"
  4.1448 +  then have "\<lfloor>log 2 \<bar>ai\<bar>\<rfloor> = k"
  4.1449 +    by simp
  4.1450 +  then have k: "2 powr k \<le> \<bar>ai\<bar>" "\<bar>ai\<bar> < 2 powr (k + 1)"
  4.1451      by (simp_all add: floor_log_eq_powr_iff \<open>ai \<noteq> 0\<close>)
  4.1452    have "k \<ge> 0"
  4.1453      using assms by (auto simp: k_def)
  4.1454 @@ -1502,7 +1658,7 @@
  4.1455    have r: "0 \<le> r" "r < 2 powr k"
  4.1456      using \<open>k \<ge> 0\<close> k
  4.1457      by (auto simp: r_def k_def algebra_simps powr_add abs_if powr_int)
  4.1458 -  hence "r \<le> (2::int) ^ nat k - 1"
  4.1459 +  then have "r \<le> (2::int) ^ nat k - 1"
  4.1460      using \<open>k \<ge> 0\<close> by (auto simp: powr_int)
  4.1461    from this[simplified real_of_int_le_iff[symmetric]] \<open>0 \<le> k\<close>
  4.1462    have r_le: "r \<le> 2 powr k - 1"
  4.1463 @@ -1511,7 +1667,7 @@
  4.1464    have "\<bar>ai\<bar> = 2 powr k + r"
  4.1465      using \<open>k \<ge> 0\<close> by (auto simp: k_def r_def powr_realpow[symmetric])
  4.1466  
  4.1467 -  have pos: "\<And>b::real. abs b < 1 \<Longrightarrow> 0 < 2 powr k + (r + b)"
  4.1468 +  have pos: "abs b < 1 \<Longrightarrow> 0 < 2 powr k + (r + b)" for b :: real
  4.1469      using \<open>0 \<le> k\<close> \<open>ai \<noteq> 0\<close>
  4.1470      by (auto simp add: r_def powr_realpow[symmetric] abs_if sgn_if algebra_simps
  4.1471        split: split_if_asm)
  4.1472 @@ -1557,8 +1713,12 @@
  4.1473    finally show ?thesis .
  4.1474  qed
  4.1475  
  4.1476 -lemma compute_far_float_plus_down:
  4.1477 -  fixes m1 e1 m2 e2::int and p::nat
  4.1478 +context
  4.1479 +begin
  4.1480 +
  4.1481 +qualified lemma compute_far_float_plus_down:
  4.1482 +  fixes m1 e1 m2 e2 :: int
  4.1483 +    and p :: nat
  4.1484    defines "k1 \<equiv> p - nat (bitlen \<bar>m1\<bar>)"
  4.1485    assumes H: "bitlen \<bar>m2\<bar> \<le> e1 - e2 - k1 - 2" "m1 \<noteq> 0" "m2 \<noteq> 0" "e1 \<ge> e2"
  4.1486    shows "float_plus_down p (Float m1 e1) (Float m2 e2) =
  4.1487 @@ -1584,7 +1744,7 @@
  4.1488    finally have abs_m2_less_half: "\<bar>?m2\<bar> < 1 / 2"
  4.1489      by simp
  4.1490  
  4.1491 -  hence "\<bar>real m2\<bar> < 2 powr -(?shift + 1)"
  4.1492 +  then have "\<bar>real m2\<bar> < 2 powr -(?shift + 1)"
  4.1493      unfolding powr_minus_divide by (auto simp: bitlen_def field_simps powr_mult_base abs_mult)
  4.1494    also have "\<dots> \<le> 2 powr real (e1 - e2 - 2)"
  4.1495      by simp
  4.1496 @@ -1593,7 +1753,7 @@
  4.1497    also have "1/4 < \<bar>real m1\<bar> / 2" using \<open>m1 \<noteq> 0\<close> by simp
  4.1498    finally have b_less_half_a: "\<bar>?b\<bar> < 1/2 * \<bar>?a\<bar>"
  4.1499      by (simp add: algebra_simps powr_mult_base abs_mult)
  4.1500 -  hence a_half_less_sum: "\<bar>?a\<bar> / 2 < \<bar>?sum\<bar>"
  4.1501 +  then have a_half_less_sum: "\<bar>?a\<bar> / 2 < \<bar>?sum\<bar>"
  4.1502      by (auto simp: field_simps abs_if split: split_if_asm)
  4.1503  
  4.1504    from b_less_half_a have "\<bar>?b\<bar> < \<bar>?a\<bar>" "\<bar>?b\<bar> \<le> \<bar>?a\<bar>"
  4.1505 @@ -1602,14 +1762,14 @@
  4.1506    have "\<bar>real (Float m1 e1)\<bar> \<ge> 1/4 * 2 powr real e1"
  4.1507      using \<open>m1 \<noteq> 0\<close>
  4.1508      by (auto simp: powr_add powr_int bitlen_nonneg divide_right_mono abs_mult)
  4.1509 -  hence "?sum \<noteq> 0" using b_less_quarter
  4.1510 +  then have "?sum \<noteq> 0" using b_less_quarter
  4.1511      by (rule sum_neq_zeroI)
  4.1512 -  hence "?m1 + ?m2 \<noteq> 0"
  4.1513 +  then have "?m1 + ?m2 \<noteq> 0"
  4.1514      unfolding sum_eq by (simp add: abs_mult zero_less_mult_iff)
  4.1515  
  4.1516    have "\<bar>real ?m1\<bar> \<ge> 2 ^ Suc k1" "\<bar>?m2'\<bar> < 2 ^ Suc k1"
  4.1517      using \<open>m1 \<noteq> 0\<close> \<open>m2 \<noteq> 0\<close> by (auto simp: sgn_if less_1_mult abs_mult simp del: power.simps)
  4.1518 -  hence sum'_nz: "?m1 + ?m2' \<noteq> 0"
  4.1519 +  then have sum'_nz: "?m1 + ?m2' \<noteq> 0"
  4.1520      by (intro sum_neq_zeroI)
  4.1521  
  4.1522    have "\<lfloor>log 2 \<bar>real (Float m1 e1) + real (Float m2 e2)\<bar>\<rfloor> = \<lfloor>log 2 \<bar>?m1 + ?m2\<bar>\<rfloor> + ?e"
  4.1523 @@ -1624,13 +1784,13 @@
  4.1524    also
  4.1525    have "\<bar>?m1 + ?m2'\<bar> * 2 powr ?e = \<bar>?m1 * 2 + sgn m2\<bar> * 2 powr (?e - 1)"
  4.1526      by (auto simp: field_simps powr_minus[symmetric] powr_divide2[symmetric] powr_mult_base)
  4.1527 -  hence "\<lfloor>log 2 \<bar>?m1 + ?m2'\<bar>\<rfloor> + ?e = \<lfloor>log 2 \<bar>real (Float (?m1 * 2 + sgn m2) (?e - 1))\<bar>\<rfloor>"
  4.1528 +  then have "\<lfloor>log 2 \<bar>?m1 + ?m2'\<bar>\<rfloor> + ?e = \<lfloor>log 2 \<bar>real (Float (?m1 * 2 + sgn m2) (?e - 1))\<bar>\<rfloor>"
  4.1529      using \<open>?m1 + ?m2' \<noteq> 0\<close>
  4.1530      unfolding floor_add[symmetric]
  4.1531      by (simp add: log_add_eq_powr abs_mult_pos)
  4.1532    finally
  4.1533    have "\<lfloor>log 2 \<bar>?sum\<bar>\<rfloor> = \<lfloor>log 2 \<bar>real (Float (?m1*2 + sgn m2) (?e - 1))\<bar>\<rfloor>" .
  4.1534 -  hence "plus_down p (Float m1 e1) (Float m2 e2) =
  4.1535 +  then have "plus_down p (Float m1 e1) (Float m2 e2) =
  4.1536        truncate_down p (Float (?m1*2 + sgn m2) (?e - 1))"
  4.1537      unfolding plus_down_def
  4.1538    proof (rule truncate_down_log2_eqI)
  4.1539 @@ -1668,14 +1828,14 @@
  4.1540      finally
  4.1541      show "\<lfloor>(?a + ?b) * 2 powr ?f\<rfloor> = \<lfloor>real (Float (?m1 * 2 + sgn m2) (?e - 1)) * 2 powr ?f\<rfloor>" .
  4.1542    qed
  4.1543 -  thus ?thesis
  4.1544 +  then show ?thesis
  4.1545      by transfer (simp add: plus_down_def ac_simps Let_def)
  4.1546  qed
  4.1547  
  4.1548  lemma compute_float_plus_down_naive[code]: "float_plus_down p x y = float_round_down p (x + y)"
  4.1549    by transfer (auto simp: plus_down_def)
  4.1550  
  4.1551 -lemma compute_float_plus_down[code]:
  4.1552 +qualified lemma compute_float_plus_down[code]:
  4.1553    fixes p::nat and m1 e1 m2 e2::int
  4.1554    shows "float_plus_down p (Float m1 e1) (Float m2 e2) =
  4.1555      (if m1 = 0 then float_round_down p (Float m2 e2)
  4.1556 @@ -1689,53 +1849,66 @@
  4.1557      else float_plus_down p (Float m2 e2) (Float m1 e1)))"
  4.1558  proof -
  4.1559    {
  4.1560 -    assume H: "bitlen \<bar>m2\<bar> \<le> e1 - e2 - (p - nat (bitlen \<bar>m1\<bar>)) - 2" "m1 \<noteq> 0" "m2 \<noteq> 0" "e1 \<ge> e2"
  4.1561 -    note compute_far_float_plus_down[OF H]
  4.1562 +    assume "bitlen \<bar>m2\<bar> \<le> e1 - e2 - (p - nat (bitlen \<bar>m1\<bar>)) - 2" "m1 \<noteq> 0" "m2 \<noteq> 0" "e1 \<ge> e2"
  4.1563 +    note compute_far_float_plus_down[OF this]
  4.1564    }
  4.1565 -  thus ?thesis
  4.1566 +  then show ?thesis
  4.1567      by transfer (simp add: Let_def plus_down_def ac_simps)
  4.1568  qed
  4.1569 -hide_fact (open) compute_far_float_plus_down
  4.1570 -hide_fact (open) compute_float_plus_down
  4.1571  
  4.1572 -lemma compute_float_plus_up[code]: "float_plus_up p x y = - float_plus_down p (-x) (-y)"
  4.1573 +qualified lemma compute_float_plus_up[code]: "float_plus_up p x y = - float_plus_down p (-x) (-y)"
  4.1574    using truncate_down_uminus_eq[of p "x + y"]
  4.1575    by transfer (simp add: plus_down_def plus_up_def ac_simps)
  4.1576 -hide_fact (open) compute_float_plus_up
  4.1577  
  4.1578  lemma mantissa_zero[simp]: "mantissa 0 = 0"
  4.1579 -by (metis mantissa_0 zero_float.abs_eq)
  4.1580 +  by (metis mantissa_0 zero_float.abs_eq)
  4.1581 +
  4.1582 +end
  4.1583  
  4.1584  
  4.1585  subsection \<open>Lemmas needed by Approximate\<close>
  4.1586  
  4.1587 -lemma Float_num[simp]: shows
  4.1588 -   "real (Float 1 0) = 1" and "real (Float 1 1) = 2" and "real (Float 1 2) = 4" and
  4.1589 -   "real (Float 1 (- 1)) = 1/2" and "real (Float 1 (- 2)) = 1/4" and "real (Float 1 (- 3)) = 1/8" and
  4.1590 -   "real (Float (- 1) 0) = -1" and "real (Float (number_of n) 0) = number_of n"
  4.1591 -using two_powr_int_float[of 2] two_powr_int_float[of "-1"] two_powr_int_float[of "-2"] two_powr_int_float[of "-3"]
  4.1592 -using powr_realpow[of 2 2] powr_realpow[of 2 3]
  4.1593 -using powr_minus[of 2 1] powr_minus[of 2 2] powr_minus[of 2 3]
  4.1594 -by auto
  4.1595 +lemma Float_num[simp]:
  4.1596 +   "real (Float 1 0) = 1"
  4.1597 +   "real (Float 1 1) = 2"
  4.1598 +   "real (Float 1 2) = 4"
  4.1599 +   "real (Float 1 (- 1)) = 1/2"
  4.1600 +   "real (Float 1 (- 2)) = 1/4"
  4.1601 +   "real (Float 1 (- 3)) = 1/8"
  4.1602 +   "real (Float (- 1) 0) = -1"
  4.1603 +   "real (Float (number_of n) 0) = number_of n"
  4.1604 +  using two_powr_int_float[of 2] two_powr_int_float[of "-1"] two_powr_int_float[of "-2"]
  4.1605 +    two_powr_int_float[of "-3"]
  4.1606 +  using powr_realpow[of 2 2] powr_realpow[of 2 3]
  4.1607 +  using powr_minus[of 2 1] powr_minus[of 2 2] powr_minus[of 2 3]
  4.1608 +  by auto
  4.1609  
  4.1610 -lemma real_of_Float_int[simp]: "real (Float n 0) = real n" by simp
  4.1611 +lemma real_of_Float_int[simp]: "real (Float n 0) = real n"
  4.1612 +  by simp
  4.1613  
  4.1614 -lemma float_zero[simp]: "real (Float 0 e) = 0" by simp
  4.1615 +lemma float_zero[simp]: "real (Float 0 e) = 0"
  4.1616 +  by simp
  4.1617  
  4.1618  lemma abs_div_2_less: "a \<noteq> 0 \<Longrightarrow> a \<noteq> -1 \<Longrightarrow> abs((a::int) div 2) < abs a"
  4.1619 -by arith
  4.1620 +  by arith
  4.1621  
  4.1622 -lemma lapprox_rat:
  4.1623 -  shows "real (lapprox_rat prec x y) \<le> real x / real y"
  4.1624 +lemma lapprox_rat: "real (lapprox_rat prec x y) \<le> real x / real y"
  4.1625    using round_down by (simp add: lapprox_rat_def)
  4.1626  
  4.1627 -lemma mult_div_le: fixes a b:: int assumes "b > 0" shows "a \<ge> b * (a div b)"
  4.1628 +lemma mult_div_le:
  4.1629 +  fixes a b :: int
  4.1630 +  assumes "b > 0"
  4.1631 +  shows "a \<ge> b * (a div b)"
  4.1632  proof -
  4.1633 -  from zmod_zdiv_equality'[of a b]
  4.1634 -  have "a = b * (a div b) + a mod b" by simp
  4.1635 -  also have "... \<ge> b * (a div b) + 0" apply (rule add_left_mono) apply (rule pos_mod_sign)
  4.1636 -  using assms by simp
  4.1637 -  finally show ?thesis by simp
  4.1638 +  from zmod_zdiv_equality'[of a b] have "a = b * (a div b) + a mod b"
  4.1639 +    by simp
  4.1640 +  also have "\<dots> \<ge> b * (a div b) + 0"
  4.1641 +    apply (rule add_left_mono)
  4.1642 +    apply (rule pos_mod_sign)
  4.1643 +    using assms apply simp
  4.1644 +    done
  4.1645 +  finally show ?thesis
  4.1646 +    by simp
  4.1647  qed
  4.1648  
  4.1649  lemma lapprox_rat_nonneg:
  4.1650 @@ -1758,12 +1931,10 @@
  4.1651      by transfer (auto intro!: round_up_le1 simp: rat_precision_def)
  4.1652  qed
  4.1653  
  4.1654 -lemma rapprox_rat_nonneg_nonpos:
  4.1655 -  "0 \<le> x \<Longrightarrow> y \<le> 0 \<Longrightarrow> real (rapprox_rat n x y) \<le> 0"
  4.1656 +lemma rapprox_rat_nonneg_nonpos: "0 \<le> x \<Longrightarrow> y \<le> 0 \<Longrightarrow> real (rapprox_rat n x y) \<le> 0"
  4.1657    by transfer (simp add: round_up_le0 divide_nonneg_nonpos)
  4.1658  
  4.1659 -lemma rapprox_rat_nonpos_nonneg:
  4.1660 -  "x \<le> 0 \<Longrightarrow> 0 \<le> y \<Longrightarrow> real (rapprox_rat n x y) \<le> 0"
  4.1661 +lemma rapprox_rat_nonpos_nonneg: "x \<le> 0 \<Longrightarrow> 0 \<le> y \<Longrightarrow> real (rapprox_rat n x y) \<le> 0"
  4.1662    by transfer (simp add: round_up_le0 divide_nonpos_nonneg)
  4.1663  
  4.1664  lemma real_divl: "real_divl prec x y \<le> x / y"
  4.1665 @@ -1793,17 +1964,32 @@
  4.1666    by (simp add: bitlen_def)
  4.1667  
  4.1668  lemma mantissa_eq_zero_iff: "mantissa x = 0 \<longleftrightarrow> x = 0"
  4.1669 +  (is "?lhs \<longleftrightarrow> ?rhs")
  4.1670  proof
  4.1671 -  assume "mantissa x = 0" hence z: "0 = real x" using mantissa_exponent by simp
  4.1672 -  show "x = 0" by (simp add: zero_float_def z)
  4.1673 -qed (simp add: zero_float_def)
  4.1674 +  show ?rhs if ?lhs
  4.1675 +  proof -
  4.1676 +    from that have z: "0 = real x"
  4.1677 +      using mantissa_exponent by simp
  4.1678 +    show ?thesis
  4.1679 +      by (simp add: zero_float_def z)
  4.1680 +  qed
  4.1681 +  show ?lhs if ?rhs
  4.1682 +    using that by (simp add: zero_float_def)
  4.1683 +qed
  4.1684  
  4.1685  lemma float_upper_bound: "x \<le> 2 powr (bitlen \<bar>mantissa x\<bar> + exponent x)"
  4.1686 -proof (cases "x = 0", simp)
  4.1687 -  assume "x \<noteq> 0" hence "mantissa x \<noteq> 0" using mantissa_eq_zero_iff by auto
  4.1688 -  have "x = mantissa x * 2 powr (exponent x)" by (rule mantissa_exponent)
  4.1689 -  also have "mantissa x \<le> \<bar>mantissa x\<bar>" by simp
  4.1690 -  also have "... \<le> 2 powr (bitlen \<bar>mantissa x\<bar>)"
  4.1691 +proof (cases "x = 0")
  4.1692 +  case True
  4.1693 +  then show ?thesis by simp
  4.1694 +next
  4.1695 +  case False
  4.1696 +  then have "mantissa x \<noteq> 0"
  4.1697 +    using mantissa_eq_zero_iff by auto
  4.1698 +  have "x = mantissa x * 2 powr (exponent x)"
  4.1699 +    by (rule mantissa_exponent)
  4.1700 +  also have "mantissa x \<le> \<bar>mantissa x\<bar>"
  4.1701 +    by simp
  4.1702 +  also have "\<dots> \<le> 2 powr (bitlen \<bar>mantissa x\<bar>)"
  4.1703      using bitlen_bounds[of "\<bar>mantissa x\<bar>"] bitlen_nonneg \<open>mantissa x \<noteq> 0\<close>
  4.1704      by (auto simp del: real_of_int_abs simp add: powr_int)
  4.1705    finally show ?thesis by (simp add: powr_add)
  4.1706 @@ -1813,22 +1999,28 @@
  4.1707    assumes "0 < x" "x \<le> 1" "prec \<ge> 1"
  4.1708    shows "1 \<le> real_divl prec 1 x"
  4.1709  proof -
  4.1710 -  have "log 2 x \<le> real prec + real \<lfloor>log 2 x\<rfloor>" using \<open>prec \<ge> 1\<close> by arith
  4.1711 +  have "log 2 x \<le> real prec + real \<lfloor>log 2 x\<rfloor>"
  4.1712 +    using \<open>prec \<ge> 1\<close> by arith
  4.1713    from this assms show ?thesis
  4.1714      by (simp add: real_divl_def log_divide round_down_ge1)
  4.1715  qed
  4.1716  
  4.1717  lemma float_divl_pos_less1_bound:
  4.1718    "0 < real x \<Longrightarrow> real x \<le> 1 \<Longrightarrow> prec \<ge> 1 \<Longrightarrow> 1 \<le> real (float_divl prec 1 x)"
  4.1719 -  by (transfer, rule real_divl_pos_less1_bound)
  4.1720 +  by transfer (rule real_divl_pos_less1_bound)
  4.1721  
  4.1722  lemma float_divr: "real x / real y \<le> real (float_divr prec x y)"
  4.1723    by transfer (rule real_divr)
  4.1724  
  4.1725 -lemma real_divr_pos_less1_lower_bound: assumes "0 < x" and "x \<le> 1" shows "1 \<le> real_divr prec 1 x"
  4.1726 +lemma real_divr_pos_less1_lower_bound:
  4.1727 +  assumes "0 < x"
  4.1728 +    and "x \<le> 1"
  4.1729 +  shows "1 \<le> real_divr prec 1 x"
  4.1730  proof -
  4.1731 -  have "1 \<le> 1 / x" using \<open>0 < x\<close> and \<open>x <= 1\<close> by auto
  4.1732 -  also have "\<dots> \<le> real_divr prec 1 x" using real_divr[where x=1 and y=x] by auto
  4.1733 +  have "1 \<le> 1 / x"
  4.1734 +    using \<open>0 < x\<close> and \<open>x <= 1\<close> by auto
  4.1735 +  also have "\<dots> \<le> real_divr prec 1 x"
  4.1736 +    using real_divr[where x=1 and y=x] by auto
  4.1737    finally show ?thesis by auto
  4.1738  qed
  4.1739  
  4.1740 @@ -1855,19 +2047,21 @@
  4.1741    assumes "0 \<le> x" "x \<le> y"
  4.1742    shows "truncate_up prec x \<le> truncate_up prec y"
  4.1743  proof -
  4.1744 -  {
  4.1745 -    assume "\<lfloor>log 2 x\<rfloor> = \<lfloor>log 2 y\<rfloor>"
  4.1746 -    hence ?thesis
  4.1747 +  consider "\<lfloor>log 2 x\<rfloor> = \<lfloor>log 2 y\<rfloor>" | "\<lfloor>log 2 x\<rfloor> \<noteq> \<lfloor>log 2 y\<rfloor>" "0 < x" | "x \<le> 0"
  4.1748 +    by arith
  4.1749 +  then show ?thesis
  4.1750 +  proof cases
  4.1751 +    case 1
  4.1752 +    then show ?thesis
  4.1753        using assms
  4.1754        by (auto simp: truncate_up_def round_up_def intro!: ceiling_mono)
  4.1755 -  } moreover {
  4.1756 -    assume "0 < x"
  4.1757 -    hence "log 2 x \<le> log 2 y" using assms by auto
  4.1758 -    moreover
  4.1759 -    assume "\<lfloor>log 2 x\<rfloor> \<noteq> \<lfloor>log 2 y\<rfloor>"
  4.1760 -    ultimately have logless: "log 2 x < log 2 y" and flogless: "\<lfloor>log 2 x\<rfloor> < \<lfloor>log 2 y\<rfloor>"
  4.1761 -      unfolding atomize_conj
  4.1762 -      by (metis floor_less_cancel linorder_cases not_le)
  4.1763 +  next
  4.1764 +    case 2
  4.1765 +    from assms \<open>0 < x\<close> have "log 2 x \<le> log 2 y"
  4.1766 +      by auto
  4.1767 +    with \<open>\<lfloor>log 2 x\<rfloor> \<noteq> \<lfloor>log 2 y\<rfloor>\<close>
  4.1768 +    have logless: "log 2 x < log 2 y" and flogless: "\<lfloor>log 2 x\<rfloor> < \<lfloor>log 2 y\<rfloor>"
  4.1769 +      by (metis floor_less_cancel linorder_cases not_le)+
  4.1770      have "truncate_up prec x =
  4.1771        real \<lceil>x * 2 powr real (int prec - \<lfloor>log 2 x\<rfloor> - 1)\<rceil> * 2 powr - real (int prec - \<lfloor>log 2 x\<rfloor> - 1)"
  4.1772        using assms by (simp add: truncate_up_def round_up_def)
  4.1773 @@ -1876,10 +2070,10 @@
  4.1774        have "x * 2 powr real (int prec - \<lfloor>log 2 x\<rfloor> - 1) \<le> x * (2 powr real prec / (2 powr log 2 x))"
  4.1775          using real_of_int_floor_add_one_ge[of "log 2 x"] assms
  4.1776          by (auto simp add: algebra_simps powr_divide2 intro!: mult_left_mono)
  4.1777 -      thus "x * 2 powr real (int prec - \<lfloor>log 2 x\<rfloor> - 1) \<le> real ((2::int) ^ prec)"
  4.1778 +      then show "x * 2 powr real (int prec - \<lfloor>log 2 x\<rfloor> - 1) \<le> real ((2::int) ^ prec)"
  4.1779          using \<open>0 < x\<close> by (simp add: powr_realpow)
  4.1780      qed
  4.1781 -    hence "real \<lceil>x * 2 powr real (int prec - \<lfloor>log 2 x\<rfloor> - 1)\<rceil> \<le> 2 powr int prec"
  4.1782 +    then have "real \<lceil>x * 2 powr real (int prec - \<lfloor>log 2 x\<rfloor> - 1)\<rceil> \<le> 2 powr int prec"
  4.1783        by (auto simp: powr_realpow)
  4.1784      also
  4.1785      have "2 powr - real (int prec - \<lfloor>log 2 x\<rfloor> - 1) \<le> 2 powr - real (int prec - \<lfloor>log 2 y\<rfloor>)"
  4.1786 @@ -1896,14 +2090,13 @@
  4.1787        by (simp add: powr_add)
  4.1788      also have "\<dots> \<le> truncate_up prec y"
  4.1789        by (rule truncate_up)
  4.1790 -    finally have ?thesis .
  4.1791 -  } moreover {
  4.1792 -    assume "~ 0 < x"
  4.1793 -    hence ?thesis
  4.1794 +    finally show ?thesis .
  4.1795 +  next
  4.1796 +    case 3
  4.1797 +    then show ?thesis
  4.1798        using assms
  4.1799        by (auto intro!: truncate_up_le)
  4.1800 -  } ultimately show ?thesis
  4.1801 -    by blast
  4.1802 +  qed
  4.1803  qed
  4.1804  
  4.1805  lemma truncate_up_switch_sign_mono:
  4.1806 @@ -1931,20 +2124,22 @@
  4.1807    finally have "\<lfloor>x * 2 powr (- real \<lfloor>log 2 x\<rfloor> - 1)\<rfloor> < 1"
  4.1808      unfolding less_ceiling_eq real_of_int_minus real_of_one
  4.1809      by simp
  4.1810 -  moreover
  4.1811 -  have "0 \<le> \<lfloor>x * 2 powr (- real \<lfloor>log 2 x\<rfloor> - 1)\<rfloor>"
  4.1812 +  moreover have "0 \<le> \<lfloor>x * 2 powr (- real \<lfloor>log 2 x\<rfloor> - 1)\<rfloor>"
  4.1813      using \<open>x > 0\<close> by auto
  4.1814    ultimately have "\<lfloor>x * 2 powr (- real \<lfloor>log 2 x\<rfloor> - 1)\<rfloor> \<in> {0 ..< 1}"
  4.1815      by simp
  4.1816 -  also have "\<dots> \<subseteq> {0}" by auto
  4.1817 -  finally have "\<lfloor>x * 2 powr (- real \<lfloor>log 2 x\<rfloor> - 1)\<rfloor> = 0" by simp
  4.1818 +  also have "\<dots> \<subseteq> {0}"
  4.1819 +    by auto
  4.1820 +  finally have "\<lfloor>x * 2 powr (- real \<lfloor>log 2 x\<rfloor> - 1)\<rfloor> = 0"
  4.1821 +    by simp
  4.1822    with assms show ?thesis
  4.1823      by (auto simp: truncate_down_def round_down_def)
  4.1824  qed
  4.1825  
  4.1826  lemma truncate_down_switch_sign_mono:
  4.1827 -  assumes "x \<le> 0" "0 \<le> y"
  4.1828 -  assumes "x \<le> y"
  4.1829 +  assumes "x \<le> 0"
  4.1830 +    and "0 \<le> y"
  4.1831 +    and "x \<le> y"
  4.1832    shows "truncate_down prec x \<le> truncate_down prec y"
  4.1833  proof -
  4.1834    note truncate_down_le[OF \<open>x \<le> 0\<close>]
  4.1835 @@ -1956,32 +2151,36 @@
  4.1836    assumes "0 \<le> x" "x \<le> y"
  4.1837    shows "truncate_down prec x \<le> truncate_down prec y"
  4.1838  proof -
  4.1839 -  {
  4.1840 -    assume "0 < x" "prec = 0"
  4.1841 -    with assms have ?thesis
  4.1842 +  consider "0 < x" "prec = 0" | "x \<le> 0" | "\<lfloor>log 2 \<bar>x\<bar>\<rfloor> = \<lfloor>log 2 \<bar>y\<bar>\<rfloor>" |
  4.1843 +    "0 < x" "\<lfloor>log 2 \<bar>x\<bar>\<rfloor> \<noteq> \<lfloor>log 2 \<bar>y\<bar>\<rfloor>" "prec \<noteq> 0"
  4.1844 +    by arith
  4.1845 +  then show ?thesis
  4.1846 +  proof cases
  4.1847 +    case 1
  4.1848 +    with assms show ?thesis
  4.1849        by (simp add: truncate_down_zeroprec_mono)
  4.1850 -  } moreover {
  4.1851 -    assume "~ 0 < x"
  4.1852 +  next
  4.1853 +    case 2
  4.1854      with assms have "x = 0" "0 \<le> y" by simp_all
  4.1855 -    hence ?thesis
  4.1856 +    then show ?thesis
  4.1857        by (auto intro!: truncate_down_nonneg)
  4.1858 -  } moreover {
  4.1859 -    assume "\<lfloor>log 2 \<bar>x\<bar>\<rfloor> = \<lfloor>log 2 \<bar>y\<bar>\<rfloor>"
  4.1860 -    hence ?thesis
  4.1861 +  next
  4.1862 +    case 3
  4.1863 +    then show ?thesis
  4.1864        using assms
  4.1865        by (auto simp: truncate_down_def round_down_def intro!: floor_mono)
  4.1866 -  } moreover {
  4.1867 -    assume "0 < x"
  4.1868 -    hence "log 2 x \<le> log 2 y" "0 < y" "0 \<le> y" using assms by auto
  4.1869 -    moreover
  4.1870 -    assume "\<lfloor>log 2 \<bar>x\<bar>\<rfloor> \<noteq> \<lfloor>log 2 \<bar>y\<bar>\<rfloor>"
  4.1871 -    ultimately have logless: "log 2 x < log 2 y" and flogless: "\<lfloor>log 2 x\<rfloor> < \<lfloor>log 2 y\<rfloor>"
  4.1872 +  next
  4.1873 +    case 4
  4.1874 +    from \<open>0 < x\<close> have "log 2 x \<le> log 2 y" "0 < y" "0 \<le> y"
  4.1875 +      using assms by auto
  4.1876 +    with \<open>\<lfloor>log 2 \<bar>x\<bar>\<rfloor> \<noteq> \<lfloor>log 2 \<bar>y\<bar>\<rfloor>\<close>
  4.1877 +    have logless: "log 2 x < log 2 y" and flogless: "\<lfloor>log 2 x\<rfloor> < \<lfloor>log 2 y\<rfloor>"
  4.1878        unfolding atomize_conj abs_of_pos[OF \<open>0 < x\<close>] abs_of_pos[OF \<open>0 < y\<close>]
  4.1879        by (metis floor_less_cancel linorder_cases not_le)
  4.1880 -    assume "prec \<noteq> 0" hence [simp]: "prec \<ge> Suc 0" by auto
  4.1881 +    from \<open>prec \<noteq> 0\<close> have [simp]: "prec \<ge> Suc 0"
  4.1882 +      by auto
  4.1883      have "2 powr (prec - 1) \<le> y * 2 powr real (prec - 1) / (2 powr log 2 y)"
  4.1884 -      using \<open>0 < y\<close>
  4.1885 -      by simp
  4.1886 +      using \<open>0 < y\<close> by simp
  4.1887      also have "\<dots> \<le> y * 2 powr real prec / (2 powr (real \<lfloor>log 2 y\<rfloor> + 1))"
  4.1888        using \<open>0 \<le> y\<close> \<open>0 \<le> x\<close> assms(2)
  4.1889        by (auto intro!: powr_mono divide_left_mono
  4.1890 @@ -1992,7 +2191,7 @@
  4.1891      finally have "(2 ^ (prec - 1)) \<le> \<lfloor>y * 2 powr real (int prec - \<lfloor>log 2 \<bar>y\<bar>\<rfloor> - 1)\<rfloor>"
  4.1892        using \<open>0 \<le> y\<close>
  4.1893        by (auto simp: powr_divide2[symmetric] le_floor_eq powr_realpow)
  4.1894 -    hence "(2 ^ (prec - 1)) * 2 powr - real (int prec - \<lfloor>log 2 \<bar>y\<bar>\<rfloor> - 1) \<le> truncate_down prec y"
  4.1895 +    then have "(2 ^ (prec - 1)) * 2 powr - real (int prec - \<lfloor>log 2 \<bar>y\<bar>\<rfloor> - 1) \<le> truncate_down prec y"
  4.1896        by (auto simp: truncate_down_def round_down_def)
  4.1897      moreover
  4.1898      {
  4.1899 @@ -2006,9 +2205,10 @@
  4.1900          by (auto intro!: floor_mono)
  4.1901        finally have "x \<le> (2 ^ (prec - 1)) * 2 powr - real (int prec - \<lfloor>log 2 \<bar>y\<bar>\<rfloor> - 1)"
  4.1902          by (auto simp: powr_realpow[symmetric] powr_divide2[symmetric] assms real_of_nat_diff)
  4.1903 -    } ultimately have ?thesis
  4.1904 +    }
  4.1905 +    ultimately show ?thesis
  4.1906        by (metis dual_order.trans truncate_down)
  4.1907 -  } ultimately show ?thesis by blast
  4.1908 +  qed
  4.1909  qed
  4.1910  
  4.1911  lemma truncate_down_eq_truncate_up: "truncate_down p x = - truncate_up p (-x)"
  4.1912 @@ -2029,49 +2229,62 @@
  4.1913  lemma Float_le_zero_iff: "Float a b \<le> 0 \<longleftrightarrow> a \<le> 0"
  4.1914   by (auto simp: zero_float_def mult_le_0_iff) (simp add: not_less [symmetric])
  4.1915  
  4.1916 -lemma real_of_float_pprt[simp]: fixes a::float shows "real (pprt a) = pprt (real a)"
  4.1917 +lemma real_of_float_pprt[simp]:
  4.1918 +  fixes a :: float
  4.1919 +  shows "real (pprt a) = pprt (real a)"
  4.1920    unfolding pprt_def sup_float_def max_def sup_real_def by auto
  4.1921  
  4.1922 -lemma real_of_float_nprt[simp]: fixes a::float shows "real (nprt a) = nprt (real a)"
  4.1923 +lemma real_of_float_nprt[simp]:
  4.1924 +  fixes a :: float
  4.1925 +  shows "real (nprt a) = nprt (real a)"
  4.1926    unfolding nprt_def inf_float_def min_def inf_real_def by auto
  4.1927  
  4.1928 +context
  4.1929 +begin
  4.1930 +
  4.1931  lift_definition int_floor_fl :: "float \<Rightarrow> int" is floor .
  4.1932  
  4.1933 -lemma compute_int_floor_fl[code]:
  4.1934 +qualified lemma compute_int_floor_fl[code]:
  4.1935    "int_floor_fl (Float m e) = (if 0 \<le> e then m * 2 ^ nat e else m div (2 ^ (nat (-e))))"
  4.1936    by transfer (simp add: powr_int int_of_reals floor_divide_eq_div del: real_of_ints)
  4.1937 -hide_fact (open) compute_int_floor_fl
  4.1938  
  4.1939  lift_definition floor_fl :: "float \<Rightarrow> float" is "\<lambda>x. real (floor x)" by simp
  4.1940  
  4.1941 -lemma compute_floor_fl[code]:
  4.1942 +qualified lemma compute_floor_fl[code]:
  4.1943    "floor_fl (Float m e) = (if 0 \<le> e then Float m e else Float (m div (2 ^ (nat (-e)))) 0)"
  4.1944    by transfer (simp add: powr_int int_of_reals floor_divide_eq_div del: real_of_ints)
  4.1945 -hide_fact (open) compute_floor_fl
  4.1946 +
  4.1947 +end
  4.1948  
  4.1949 -lemma floor_fl: "real (floor_fl x) \<le> real x" by transfer simp
  4.1950 +lemma floor_fl: "real (floor_fl x) \<le> real x"
  4.1951 +  by transfer simp
  4.1952  
  4.1953 -lemma int_floor_fl: "real (int_floor_fl x) \<le> real x" by transfer simp
  4.1954 +lemma int_floor_fl: "real (int_floor_fl x) \<le> real x"
  4.1955 +  by transfer simp
  4.1956  
  4.1957  lemma floor_pos_exp: "exponent (floor_fl x) \<ge> 0"
  4.1958  proof (cases "floor_fl x = float_of 0")
  4.1959    case True
  4.1960 -  then show ?thesis by (simp add: floor_fl_def)
  4.1961 +  then show ?thesis
  4.1962 +    by (simp add: floor_fl_def)
  4.1963  next
  4.1964    case False
  4.1965 -  have eq: "floor_fl x = Float \<lfloor>real x\<rfloor> 0" by transfer simp
  4.1966 +  have eq: "floor_fl x = Float \<lfloor>real x\<rfloor> 0"
  4.1967 +    by transfer simp
  4.1968    obtain i where "\<lfloor>real x\<rfloor> = mantissa (floor_fl x) * 2 ^ i" "0 = exponent (floor_fl x) - int i"
  4.1969      by (rule denormalize_shift[OF eq[THEN eq_reflection] False])
  4.1970 -  then show ?thesis by simp
  4.1971 +  then show ?thesis
  4.1972 +    by simp
  4.1973  qed
  4.1974  
  4.1975  lemma compute_mantissa[code]:
  4.1976 -  "mantissa (Float m e) = (if m = 0 then 0 else if 2 dvd m then mantissa (normfloat (Float m e)) else m)"
  4.1977 +  "mantissa (Float m e) =
  4.1978 +    (if m = 0 then 0 else if 2 dvd m then mantissa (normfloat (Float m e)) else m)"
  4.1979    by (auto simp: mantissa_float Float.abs_eq)
  4.1980  
  4.1981  lemma compute_exponent[code]:
  4.1982 -  "exponent (Float m e) = (if m = 0 then 0 else if 2 dvd m then exponent (normfloat (Float m e)) else e)"
  4.1983 +  "exponent (Float m e) =
  4.1984 +    (if m = 0 then 0 else if 2 dvd m then exponent (normfloat (Float m e)) else e)"
  4.1985    by (auto simp: exponent_float Float.abs_eq)
  4.1986  
  4.1987  end
  4.1988 -
     5.1 --- a/src/HOL/Library/Lattice_Algebras.thy	Thu Jul 09 00:39:49 2015 +0200
     5.2 +++ b/src/HOL/Library/Lattice_Algebras.thy	Thu Jul 09 00:40:57 2015 +0200
     5.3 @@ -145,7 +145,8 @@
     5.4  lemma nprt_le_zero[simp]: "nprt a \<le> 0"
     5.5    by (simp add: nprt_def)
     5.6  
     5.7 -lemma le_eq_neg: "a \<le> - b \<longleftrightarrow> a + b \<le> 0" (is "?l = ?r")
     5.8 +lemma le_eq_neg: "a \<le> - b \<longleftrightarrow> a + b \<le> 0"
     5.9 +  (is "?l = ?r")
    5.10  proof
    5.11    assume ?l
    5.12    then show ?r
    5.13 @@ -177,25 +178,24 @@
    5.14  lemma nprt_eq_0 [simp, no_atp]: "0 \<le> x \<Longrightarrow> nprt x = 0"
    5.15    by (simp add: nprt_def inf_absorb2)
    5.16  
    5.17 -lemma sup_0_imp_0: "sup a (- a) = 0 \<Longrightarrow> a = 0"
    5.18 +lemma sup_0_imp_0:
    5.19 +  assumes "sup a (- a) = 0"
    5.20 +  shows "a = 0"
    5.21  proof -
    5.22 -  {
    5.23 -    fix a :: 'a
    5.24 -    assume hyp: "sup a (- a) = 0"
    5.25 -    then have "sup a (- a) + a = a"
    5.26 +  have p: "0 \<le> a" if "sup a (- a) = 0" for a :: 'a
    5.27 +  proof -
    5.28 +    from that have "sup a (- a) + a = a"
    5.29        by simp
    5.30      then have "sup (a + a) 0 = a"
    5.31        by (simp add: add_sup_distrib_right)
    5.32      then have "sup (a + a) 0 \<le> a"
    5.33        by simp
    5.34 -    then have "0 \<le> a"
    5.35 +    then show ?thesis
    5.36        by (blast intro: order_trans inf_sup_ord)
    5.37 -  }
    5.38 -  note p = this
    5.39 -  assume hyp:"sup a (-a) = 0"
    5.40 -  then have hyp2:"sup (-a) (-(-a)) = 0"
    5.41 +  qed
    5.42 +  from assms have **: "sup (-a) (-(-a)) = 0"
    5.43      by (simp add: sup_commute)
    5.44 -  from p[OF hyp] p[OF hyp2] show "a = 0"
    5.45 +  from p[OF assms] p[OF **] show "a = 0"
    5.46      by simp
    5.47  qed
    5.48  
    5.49 @@ -217,49 +217,50 @@
    5.50    apply simp
    5.51    done
    5.52  
    5.53 -lemma zero_le_double_add_iff_zero_le_single_add [simp]:
    5.54 -  "0 \<le> a + a \<longleftrightarrow> 0 \<le> a"
    5.55 +lemma zero_le_double_add_iff_zero_le_single_add [simp]: "0 \<le> a + a \<longleftrightarrow> 0 \<le> a"
    5.56 +  (is "?lhs \<longleftrightarrow> ?rhs")
    5.57  proof
    5.58 -  assume "0 \<le> a + a"
    5.59 -  then have a: "inf (a + a) 0 = 0"
    5.60 -    by (simp add: inf_commute inf_absorb1)
    5.61 -  have "inf a 0 + inf a 0 = inf (inf (a + a) 0) a"  (is "?l=_")
    5.62 -    by (simp add: add_sup_inf_distribs inf_aci)
    5.63 -  then have "?l = 0 + inf a 0"
    5.64 -    by (simp add: a, simp add: inf_commute)
    5.65 -  then have "inf a 0 = 0"
    5.66 -    by (simp only: add_right_cancel)
    5.67 -  then show "0 \<le> a"
    5.68 -    unfolding le_iff_inf by (simp add: inf_commute)
    5.69 -next
    5.70 -  assume a: "0 \<le> a"
    5.71 -  show "0 \<le> a + a"
    5.72 -    by (simp add: add_mono[OF a a, simplified])
    5.73 +  show ?rhs if ?lhs
    5.74 +  proof -
    5.75 +    from that have a: "inf (a + a) 0 = 0"
    5.76 +      by (simp add: inf_commute inf_absorb1)
    5.77 +    have "inf a 0 + inf a 0 = inf (inf (a + a) 0) a"  (is "?l=_")
    5.78 +      by (simp add: add_sup_inf_distribs inf_aci)
    5.79 +    then have "?l = 0 + inf a 0"
    5.80 +      by (simp add: a, simp add: inf_commute)
    5.81 +    then have "inf a 0 = 0"
    5.82 +      by (simp only: add_right_cancel)
    5.83 +    then show ?thesis
    5.84 +      unfolding le_iff_inf by (simp add: inf_commute)
    5.85 +  qed
    5.86 +  show ?lhs if ?rhs
    5.87 +    by (simp add: add_mono[OF that that, simplified])
    5.88  qed
    5.89  
    5.90  lemma double_zero [simp]: "a + a = 0 \<longleftrightarrow> a = 0"
    5.91 +  (is "?lhs \<longleftrightarrow> ?rhs")
    5.92  proof
    5.93 -  assume assm: "a + a = 0"
    5.94 -  then have "a + a + - a = - a"
    5.95 -    by simp
    5.96 -  then have "a + (a + - a) = - a"
    5.97 -    by (simp only: add.assoc)
    5.98 -  then have a: "- a = a"
    5.99 -    by simp
   5.100 -  show "a = 0"
   5.101 -    apply (rule antisym)
   5.102 -    apply (unfold neg_le_iff_le [symmetric, of a])
   5.103 -    unfolding a
   5.104 -    apply simp
   5.105 -    unfolding zero_le_double_add_iff_zero_le_single_add [symmetric, of a]
   5.106 -    unfolding assm
   5.107 -    unfolding le_less
   5.108 -    apply simp_all
   5.109 -    done
   5.110 -next
   5.111 -  assume "a = 0"
   5.112 -  then show "a + a = 0"
   5.113 -    by simp
   5.114 +  show ?rhs if ?lhs
   5.115 +  proof -
   5.116 +    from that have "a + a + - a = - a"
   5.117 +      by simp
   5.118 +    then have "a + (a + - a) = - a"
   5.119 +      by (simp only: add.assoc)
   5.120 +    then have a: "- a = a"
   5.121 +      by simp
   5.122 +    show ?thesis
   5.123 +      apply (rule antisym)
   5.124 +      apply (unfold neg_le_iff_le [symmetric, of a])
   5.125 +      unfolding a
   5.126 +      apply simp
   5.127 +      unfolding zero_le_double_add_iff_zero_le_single_add [symmetric, of a]
   5.128 +      unfolding that
   5.129 +      unfolding le_less
   5.130 +      apply simp_all
   5.131 +      done
   5.132 +  qed
   5.133 +  show ?lhs if ?rhs
   5.134 +    using that by simp
   5.135  qed
   5.136  
   5.137  lemma zero_less_double_add_iff_zero_less_single_add [simp]: "0 < a + a \<longleftrightarrow> 0 < a"
   5.138 @@ -281,19 +282,17 @@
   5.139      done
   5.140  qed
   5.141  
   5.142 -lemma double_add_le_zero_iff_single_add_le_zero [simp]:
   5.143 -  "a + a \<le> 0 \<longleftrightarrow> a \<le> 0"
   5.144 +lemma double_add_le_zero_iff_single_add_le_zero [simp]: "a + a \<le> 0 \<longleftrightarrow> a \<le> 0"
   5.145  proof -
   5.146    have "a + a \<le> 0 \<longleftrightarrow> 0 \<le> - (a + a)"
   5.147 -    by (subst le_minus_iff, simp)
   5.148 +    by (subst le_minus_iff) simp
   5.149    moreover have "\<dots> \<longleftrightarrow> a \<le> 0"
   5.150      by (simp only: minus_add_distrib zero_le_double_add_iff_zero_le_single_add) simp
   5.151    ultimately show ?thesis
   5.152      by blast
   5.153  qed
   5.154  
   5.155 -lemma double_add_less_zero_iff_single_less_zero [simp]:
   5.156 -  "a + a < 0 \<longleftrightarrow> a < 0"
   5.157 +lemma double_add_less_zero_iff_single_less_zero [simp]: "a + a < 0 \<longleftrightarrow> a < 0"
   5.158  proof -
   5.159    have "a + a < 0 \<longleftrightarrow> 0 < - (a + a)"
   5.160      by (subst less_minus_iff) simp
   5.161 @@ -316,8 +315,8 @@
   5.162  
   5.163  lemma minus_le_self_iff: "- a \<le> a \<longleftrightarrow> 0 \<le> a"
   5.164  proof -
   5.165 -  from add_le_cancel_left [of "uminus a" zero "plus a a"]
   5.166    have "- a \<le> a \<longleftrightarrow> 0 \<le> a + a"
   5.167 +    using add_le_cancel_left [of "uminus a" zero "plus a a"]
   5.168      by (simp add: add.assoc[symmetric])
   5.169    then show ?thesis
   5.170      by simp
   5.171 @@ -370,15 +369,14 @@
   5.172  
   5.173  subclass ordered_ab_group_add_abs
   5.174  proof
   5.175 -  have abs_ge_zero [simp]: "\<And>a. 0 \<le> \<bar>a\<bar>"
   5.176 +  have abs_ge_zero [simp]: "0 \<le> \<bar>a\<bar>" for a
   5.177    proof -
   5.178 -    fix a b
   5.179      have a: "a \<le> \<bar>a\<bar>" and b: "- a \<le> \<bar>a\<bar>"
   5.180        by (auto simp add: abs_lattice)
   5.181      show "0 \<le> \<bar>a\<bar>"
   5.182        by (rule add_mono [OF a b, simplified])
   5.183    qed
   5.184 -  have abs_leI: "\<And>a b. a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b"
   5.185 +  have abs_leI: "a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b" for a b
   5.186      by (simp add: abs_lattice le_supI)
   5.187    fix a b
   5.188    show "0 \<le> \<bar>a\<bar>"
   5.189 @@ -387,15 +385,12 @@
   5.190      by (auto simp add: abs_lattice)
   5.191    show "\<bar>-a\<bar> = \<bar>a\<bar>"
   5.192      by (simp add: abs_lattice sup_commute)
   5.193 -  {
   5.194 -    assume "a \<le> b"
   5.195 -    then show "- a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b"
   5.196 -      by (rule abs_leI)
   5.197 -  }
   5.198 +  show "- a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b" if "a \<le> b"
   5.199 +    using that by (rule abs_leI)
   5.200    show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
   5.201    proof -
   5.202      have g: "\<bar>a\<bar> + \<bar>b\<bar> = sup (a + b) (sup (- a - b) (sup (- a + b) (a + (- b))))"
   5.203 -      (is "_=sup ?m ?n")
   5.204 +      (is "_ = sup ?m ?n")
   5.205        by (simp add: abs_lattice add_sup_inf_distribs ac_simps)
   5.206      have a: "a + b \<le> sup ?m ?n"
   5.207        by simp
   5.208 @@ -420,25 +415,23 @@
   5.209  end
   5.210  
   5.211  lemma sup_eq_if:
   5.212 -  fixes a :: "'a::{lattice_ab_group_add, linorder}"
   5.213 +  fixes a :: "'a::{lattice_ab_group_add,linorder}"
   5.214    shows "sup a (- a) = (if a < 0 then - a else a)"
   5.215 -proof -
   5.216 -  note add_le_cancel_right [of a a "- a", symmetric, simplified]
   5.217 -  moreover note add_le_cancel_right [of "-a" a a, symmetric, simplified]
   5.218 -  then show ?thesis by (auto simp: sup_max max.absorb1 max.absorb2)
   5.219 -qed
   5.220 +  using add_le_cancel_right [of a a "- a", symmetric, simplified]
   5.221 +    and add_le_cancel_right [of "-a" a a, symmetric, simplified]
   5.222 +  by (auto simp: sup_max max.absorb1 max.absorb2)
   5.223  
   5.224  lemma abs_if_lattice:
   5.225 -  fixes a :: "'a::{lattice_ab_group_add_abs, linorder}"
   5.226 +  fixes a :: "'a::{lattice_ab_group_add_abs,linorder}"
   5.227    shows "\<bar>a\<bar> = (if a < 0 then - a else a)"
   5.228    by auto
   5.229  
   5.230  lemma estimate_by_abs:
   5.231    fixes a b c :: "'a::lattice_ab_group_add_abs"
   5.232 -  shows "a + b \<le> c \<Longrightarrow> a \<le> c + \<bar>b\<bar>"
   5.233 +  assumes "a + b \<le> c"
   5.234 +  shows "a \<le> c + \<bar>b\<bar>"
   5.235  proof -
   5.236 -  assume "a + b \<le> c"
   5.237 -  then have "a \<le> c + (- b)"
   5.238 +  from assms have "a \<le> c + (- b)"
   5.239      by (simp add: algebra_simps)
   5.240    have "- b \<le> \<bar>b\<bar>"
   5.241      by (rule abs_ge_minus_self)
   5.242 @@ -464,15 +457,12 @@
   5.243    let ?y = "pprt a * pprt b + pprt a * nprt b + nprt a * pprt b + nprt a * nprt b"
   5.244    have a: "\<bar>a\<bar> * \<bar>b\<bar> = ?x"
   5.245      by (simp only: abs_prts[of a] abs_prts[of b] algebra_simps)
   5.246 -  {
   5.247 -    fix u v :: 'a
   5.248 -    have bh: "u = a \<Longrightarrow> v = b \<Longrightarrow>
   5.249 -              u * v = pprt a * pprt b + pprt a * nprt b +
   5.250 -                      nprt a * pprt b + nprt a * nprt b"
   5.251 -      apply (subst prts[of u], subst prts[of v])
   5.252 -      apply (simp add: algebra_simps)
   5.253 -      done
   5.254 -  }
   5.255 +  have bh: "u = a \<Longrightarrow> v = b \<Longrightarrow>
   5.256 +            u * v = pprt a * pprt b + pprt a * nprt b +
   5.257 +                    nprt a * pprt b + nprt a * nprt b" for u v :: 'a
   5.258 +    apply (subst prts[of u], subst prts[of v])
   5.259 +    apply (simp add: algebra_simps)
   5.260 +    done
   5.261    note b = this[OF refl[of a] refl[of b]]
   5.262    have xy: "- ?x \<le> ?y"
   5.263      apply simp
   5.264 @@ -552,9 +542,7 @@
   5.265      pprt a2 * pprt b2 + pprt a1 * nprt b2 + nprt a2 * pprt b1 + nprt a1 * nprt b1"
   5.266  proof -
   5.267    have "a * b = (pprt a + nprt a) * (pprt b + nprt b)"
   5.268 -    apply (subst prts[symmetric])+
   5.269 -    apply simp
   5.270 -    done
   5.271 +    by (subst prts[symmetric])+ simp
   5.272    then have "a * b = pprt a * pprt b + pprt a * nprt b + nprt a * pprt b + nprt a * nprt b"
   5.273      by (simp add: algebra_simps)
   5.274    moreover have "pprt a * pprt b \<le> pprt a2 * pprt b2"
   5.275 @@ -587,9 +575,7 @@
   5.276        by simp
   5.277    qed
   5.278    ultimately show ?thesis
   5.279 -    apply -
   5.280 -    apply (rule add_mono | simp)+
   5.281 -    done
   5.282 +    by - (rule add_mono | simp)+
   5.283  qed
   5.284  
   5.285  lemma mult_ge_prts:
   5.286 @@ -607,7 +593,8 @@
   5.287      by auto
   5.288    from mult_le_prts[of "- a2" "- a" "- a1" "b1" b "b2",
   5.289      OF a1 a2 assms(3) assms(4), simplified nprt_neg pprt_neg]
   5.290 -  have le: "- (a * b) \<le> - nprt a1 * pprt b2 + - nprt a2 * nprt b2 +
   5.291 +  have le: "- (a * b) \<le>
   5.292 +    - nprt a1 * pprt b2 + - nprt a2 * nprt b2 +
   5.293      - pprt a1 * pprt b1 + - pprt a2 * nprt b1"
   5.294      by simp
   5.295    then have "- (- nprt a1 * pprt b2 + - nprt a2 * nprt b2 +