src/HOL/Library/Float.thy
author hoelzl
Mon, 14 Nov 2011 18:36:31 +0100
changeset 45495 c55a07526dbe
parent 44766 d4d33a4d7548
child 45772 8a8f78ce0dcf
permissions -rw-r--r--
cleaned up float theories; removed duplicate definitions and theorems
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
30122
1c912a9d8200 standard headers;
wenzelm
parents: 30034
diff changeset
     1
(*  Title:      HOL/Library/Float.thy
1c912a9d8200 standard headers;
wenzelm
parents: 30034
diff changeset
     2
    Author:     Steven Obua 2008
1c912a9d8200 standard headers;
wenzelm
parents: 30034
diff changeset
     3
    Author:     Johannes Hoelzl, TU Muenchen <hoelzl@in.tum.de> 2008 / 2009
1c912a9d8200 standard headers;
wenzelm
parents: 30034
diff changeset
     4
*)
29988
747f0c519090 add header
huffman
parents: 29804
diff changeset
     5
747f0c519090 add header
huffman
parents: 29804
diff changeset
     6
header {* Floating-Point Numbers *}
747f0c519090 add header
huffman
parents: 29804
diff changeset
     7
20485
3078fd2eec7b got rid of Numeral.bin type
haftmann
parents: 20217
diff changeset
     8
theory Float
35032
7efe662e41b4 separate library theory for type classes combining lattices with various algebraic structures
haftmann
parents: 33555
diff changeset
     9
imports Complex_Main Lattice_Algebras
20485
3078fd2eec7b got rid of Numeral.bin type
haftmann
parents: 20217
diff changeset
    10
begin
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    11
19765
dfe940911617 misc cleanup;
wenzelm
parents: 16890
diff changeset
    12
definition
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21256
diff changeset
    13
  pow2 :: "int \<Rightarrow> real" where
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
    14
  [simp]: "pow2 a = (if (0 <= a) then (2^(nat a)) else (inverse (2^(nat (-a)))))"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
    15
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
    16
datatype float = Float int int
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
    17
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
    18
primrec of_float :: "float \<Rightarrow> real" where
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
    19
  "of_float (Float a b) = real a * pow2 b"
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
    20
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
    21
defs (overloaded)
31998
2c7a24f74db9 code attributes use common underscore convention
haftmann
parents: 31863
diff changeset
    22
  real_of_float_def [code_unfold]: "real == of_float"
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
    23
41024
ba961a606c67 move coercions to appropriate places
hoelzl
parents: 39161
diff changeset
    24
declare [[coercion "% x . Float x 0"]]
ba961a606c67 move coercions to appropriate places
hoelzl
parents: 39161
diff changeset
    25
declare [[coercion "real::float\<Rightarrow>real"]]
ba961a606c67 move coercions to appropriate places
hoelzl
parents: 39161
diff changeset
    26
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
    27
primrec mantissa :: "float \<Rightarrow> int" where
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
    28
  "mantissa (Float a b) = a"
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
    29
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
    30
primrec scale :: "float \<Rightarrow> int" where
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
    31
  "scale (Float a b) = b"
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21256
diff changeset
    32
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
    33
instantiation float :: zero begin
31467
f7d2aa438bee Approximation: Implemented argument reduction for cosine. Sinus is now implemented in terms of cosine. Sqrt computes on the entire real numbers
hoelzl
parents: 31098
diff changeset
    34
definition zero_float where "0 = Float 0 0"
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
    35
instance ..
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
    36
end
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
    37
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
    38
instantiation float :: one begin
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
    39
definition one_float where "1 = Float 1 0"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
    40
instance ..
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
    41
end
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
    42
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
    43
instantiation float :: number begin
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
    44
definition number_of_float where "number_of n = Float n 0"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
    45
instance ..
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
    46
end
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    47
32069
6d28bbd33e2c prefer code_inline over code_unfold; use code_unfold_post where appropriate
haftmann
parents: 31998
diff changeset
    48
lemma number_of_float_Float [code_unfold_post]:
31467
f7d2aa438bee Approximation: Implemented argument reduction for cosine. Sinus is now implemented in terms of cosine. Sqrt computes on the entire real numbers
hoelzl
parents: 31098
diff changeset
    49
  "number_of k = Float (number_of k) 0"
f7d2aa438bee Approximation: Implemented argument reduction for cosine. Sinus is now implemented in terms of cosine. Sqrt computes on the entire real numbers
hoelzl
parents: 31098
diff changeset
    50
  by (simp add: number_of_float_def number_of_is_id)
f7d2aa438bee Approximation: Implemented argument reduction for cosine. Sinus is now implemented in terms of cosine. Sqrt computes on the entire real numbers
hoelzl
parents: 31098
diff changeset
    51
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
    52
lemma real_of_float_simp[simp]: "real (Float a b) = real a * pow2 b"
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
    53
  unfolding real_of_float_def using of_float.simps .
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
    54
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
    55
lemma real_of_float_neg_exp: "e < 0 \<Longrightarrow> real (Float m e) = real m * inverse (2^nat (-e))" by auto
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
    56
lemma real_of_float_nge0_exp: "\<not> 0 \<le> e \<Longrightarrow> real (Float m e) = real m * inverse (2^nat (-e))" by auto
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
    57
lemma real_of_float_ge0_exp: "0 \<le> e \<Longrightarrow> real (Float m e) = real m * (2^nat e)" by auto
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    58
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
    59
lemma Float_num[simp]: shows
31467
f7d2aa438bee Approximation: Implemented argument reduction for cosine. Sinus is now implemented in terms of cosine. Sqrt computes on the entire real numbers
hoelzl
parents: 31098
diff changeset
    60
   "real (Float 1 0) = 1" and "real (Float 1 1) = 2" and "real (Float 1 2) = 4" and
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
    61
   "real (Float 1 -1) = 1/2" and "real (Float 1 -2) = 1/4" and "real (Float 1 -3) = 1/8" and
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
    62
   "real (Float -1 0) = -1" and "real (Float (number_of n) 0) = number_of n"
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
    63
  by auto
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    64
31863
e391eee8bf14 Implemented taylor series expansion for approximation
hoelzl
parents: 31467
diff changeset
    65
lemma float_number_of[simp]: "real (number_of x :: float) = number_of x"
e391eee8bf14 Implemented taylor series expansion for approximation
hoelzl
parents: 31467
diff changeset
    66
  by (simp only:number_of_float_def Float_num[unfolded number_of_is_id])
e391eee8bf14 Implemented taylor series expansion for approximation
hoelzl
parents: 31467
diff changeset
    67
e391eee8bf14 Implemented taylor series expansion for approximation
hoelzl
parents: 31467
diff changeset
    68
lemma float_number_of_int[simp]: "real (Float n 0) = real n"
41528
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
    69
  by simp
31863
e391eee8bf14 Implemented taylor series expansion for approximation
hoelzl
parents: 31467
diff changeset
    70
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
    71
lemma pow2_0[simp]: "pow2 0 = 1" by simp
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
    72
lemma pow2_1[simp]: "pow2 1 = 2" by simp
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
    73
lemma pow2_neg: "pow2 x = inverse (pow2 (-x))" by simp
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
    74
45495
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 44766
diff changeset
    75
lemma pow2_powr: "pow2 a = 2 powr a"
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 44766
diff changeset
    76
  by (simp add: powr_realpow[symmetric] powr_minus)
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    77
45495
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 44766
diff changeset
    78
declare pow2_def[simp del]
19765
dfe940911617 misc cleanup;
wenzelm
parents: 16890
diff changeset
    79
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    80
lemma pow2_add: "pow2 (a+b) = (pow2 a) * (pow2 b)"
45495
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 44766
diff changeset
    81
  by (simp add: pow2_powr powr_add)
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 44766
diff changeset
    82
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 44766
diff changeset
    83
lemma pow2_diff: "pow2 (a - b) = pow2 a / pow2 b"
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 44766
diff changeset
    84
  by (simp add: pow2_powr powr_divide2)
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 44766
diff changeset
    85
  
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 44766
diff changeset
    86
lemma pow2_add1: "pow2 (1 + a) = 2 * (pow2 a)"
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 44766
diff changeset
    87
  by (simp add: pow2_add)
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    88
41528
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
    89
lemma float_components[simp]: "Float (mantissa f) (scale f) = f" by (cases f) auto
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
    90
41528
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
    91
lemma float_split: "\<exists> a b. x = Float a b" by (cases x) auto
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    92
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
    93
lemma float_split2: "(\<forall> a b. x \<noteq> Float a b) = False" by (auto simp add: float_split)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
    94
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
    95
lemma float_zero[simp]: "real (Float 0 e) = 0" by simp
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
    96
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
    97
lemma abs_div_2_less: "a \<noteq> 0 \<Longrightarrow> a \<noteq> -1 \<Longrightarrow> abs((a::int) div 2) < abs a"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
    98
by arith
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21256
diff changeset
    99
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   100
function normfloat :: "float \<Rightarrow> float" where
41528
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
   101
  "normfloat (Float a b) =
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
   102
    (if a \<noteq> 0 \<and> even a then normfloat (Float (a div 2) (b+1))
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
   103
     else if a=0 then Float 0 0 else Float a b)"
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   104
by pat_completeness auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   105
termination by (relation "measure (nat o abs o mantissa)") (auto intro: abs_div_2_less)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   106
declare normfloat.simps[simp del]
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   107
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
   108
theorem normfloat[symmetric, simp]: "real f = real (normfloat f)"
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   109
proof (induct f rule: normfloat.induct)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   110
  case (1 a b)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   111
  have real2: "2 = real (2::int)"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   112
    by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   113
  show ?case
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   114
    apply (subst normfloat.simps)
41528
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
   115
    apply auto
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   116
    apply (subst 1[symmetric])
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   117
    apply (auto simp add: pow2_add even_def)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   118
    done
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   119
qed
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   120
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   121
lemma pow2_neq_zero[simp]: "pow2 x \<noteq> 0"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   122
  by (auto simp add: pow2_def)
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   123
26313
8590bf5ef343 avoid rebinding of existing facts;
wenzelm
parents: 26086
diff changeset
   124
lemma pow2_int: "pow2 (int c) = 2^c"
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   125
by (simp add: pow2_def)
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   126
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   127
lemma zero_less_pow2[simp]:
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   128
  "0 < pow2 x"
45495
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 44766
diff changeset
   129
  by (simp add: pow2_powr)
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   130
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   131
lemma normfloat_imp_odd_or_zero: "normfloat f = Float a b \<Longrightarrow> odd a \<or> (a = 0 \<and> b = 0)"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   132
proof (induct f rule: normfloat.induct)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   133
  case (1 u v)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   134
  from 1 have ab: "normfloat (Float u v) = Float a b" by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   135
  {
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   136
    assume eu: "even u"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   137
    assume z: "u \<noteq> 0"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   138
    have "normfloat (Float u v) = normfloat (Float (u div 2) (v + 1))"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   139
      apply (subst normfloat.simps)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   140
      by (simp add: eu z)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   141
    with ab have "normfloat (Float (u div 2) (v + 1)) = Float a b" by simp
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   142
    with 1 eu z have ?case by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   143
  }
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   144
  note case1 = this
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   145
  {
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   146
    assume "odd u \<or> u = 0"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   147
    then have ou: "\<not> (u \<noteq> 0 \<and> even u)" by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   148
    have "normfloat (Float u v) = (if u = 0 then Float 0 0 else Float u v)"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   149
      apply (subst normfloat.simps)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   150
      apply (simp add: ou)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   151
      done
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   152
    with ab have "Float a b = (if u = 0 then Float 0 0 else Float u v)" by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   153
    then have ?case
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   154
      apply (case_tac "u=0")
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   155
      apply (auto)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   156
      by (insert ou, auto)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   157
  }
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   158
  note case2 = this
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   159
  show ?case
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   160
    apply (case_tac "odd u \<or> u = 0")
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   161
    apply (rule case2)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   162
    apply simp
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   163
    apply (rule case1)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   164
    apply auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   165
    done
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   166
qed
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   167
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   168
lemma float_eq_odd_helper: 
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   169
  assumes odd: "odd a'"
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
   170
  and floateq: "real (Float a b) = real (Float a' b')"
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   171
  shows "b \<le> b'"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   172
proof - 
45495
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 44766
diff changeset
   173
  from odd have "a' \<noteq> 0" by auto
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 44766
diff changeset
   174
  with floateq have a': "real a' = real a * pow2 (b - b')"
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 44766
diff changeset
   175
    by (simp add: pow2_diff field_simps)
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 44766
diff changeset
   176
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   177
  {
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   178
    assume bcmp: "b > b'"
45495
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 44766
diff changeset
   179
    then have "\<exists>c::nat. b - b' = int c + 1"
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 44766
diff changeset
   180
      by arith
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 44766
diff changeset
   181
    then guess c ..
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 44766
diff changeset
   182
    with a' have "real a' = real (a * 2^c * 2)"
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 44766
diff changeset
   183
      by (simp add: pow2_def nat_add_distrib)
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 44766
diff changeset
   184
    with odd have False
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 44766
diff changeset
   185
      unfolding real_of_int_inject by simp
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   186
  }
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   187
  then show ?thesis by arith
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   188
qed
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   189
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   190
lemma float_eq_odd: 
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   191
  assumes odd1: "odd a"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   192
  and odd2: "odd a'"
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
   193
  and floateq: "real (Float a b) = real (Float a' b')"
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   194
  shows "a = a' \<and> b = b'"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   195
proof -
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   196
  from 
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   197
     float_eq_odd_helper[OF odd2 floateq] 
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   198
     float_eq_odd_helper[OF odd1 floateq[symmetric]]
41528
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
   199
  have beq: "b = b'" by arith
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   200
  with floateq show ?thesis by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   201
qed
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   202
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   203
theorem normfloat_unique:
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
   204
  assumes real_of_float_eq: "real f = real g"
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   205
  shows "normfloat f = normfloat g"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   206
proof - 
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   207
  from float_split[of "normfloat f"] obtain a b where normf:"normfloat f = Float a b" by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   208
  from float_split[of "normfloat g"] obtain a' b' where normg:"normfloat g = Float a' b'" by auto
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
   209
  have "real (normfloat f) = real (normfloat g)"
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
   210
    by (simp add: real_of_float_eq)
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
   211
  then have float_eq: "real (Float a b) = real (Float a' b')"
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   212
    by (simp add: normf normg)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   213
  have ab: "odd a \<or> (a = 0 \<and> b = 0)" by (rule normfloat_imp_odd_or_zero[OF normf])
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   214
  have ab': "odd a' \<or> (a' = 0 \<and> b' = 0)" by (rule normfloat_imp_odd_or_zero[OF normg])
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   215
  {
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   216
    assume odd: "odd a"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   217
    then have "a \<noteq> 0" by (simp add: even_def, arith)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   218
    with float_eq have "a' \<noteq> 0" by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   219
    with ab' have "odd a'" by simp
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   220
    from odd this float_eq have "a = a' \<and> b = b'" by (rule float_eq_odd)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   221
  }
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   222
  note odd_case = this
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   223
  {
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   224
    assume even: "even a"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   225
    with ab have a0: "a = 0" by simp
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   226
    with float_eq have a0': "a' = 0" by auto 
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   227
    from a0 a0' ab ab' have "a = a' \<and> b = b'" by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   228
  }
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   229
  note even_case = this
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   230
  from odd_case even_case show ?thesis
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   231
    apply (simp add: normf normg)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   232
    apply (case_tac "even a")
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   233
    apply auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   234
    done
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   235
qed
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   236
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   237
instantiation float :: plus begin
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   238
fun plus_float where
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   239
[simp del]: "(Float a_m a_e) + (Float b_m b_e) = 
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   240
     (if a_e \<le> b_e then Float (a_m + b_m * 2^(nat(b_e - a_e))) a_e 
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   241
                   else Float (a_m * 2^(nat (a_e - b_e)) + b_m) b_e)"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   242
instance ..
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   243
end
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   244
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   245
instantiation float :: uminus begin
30960
fec1a04b7220 power operation defined generic
haftmann
parents: 30242
diff changeset
   246
primrec uminus_float where [simp del]: "uminus_float (Float m e) = Float (-m) e"
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   247
instance ..
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   248
end
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   249
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   250
instantiation float :: minus begin
30960
fec1a04b7220 power operation defined generic
haftmann
parents: 30242
diff changeset
   251
definition minus_float where [simp del]: "(z::float) - w = z + (- w)"
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   252
instance ..
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   253
end
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   254
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   255
instantiation float :: times begin
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   256
fun times_float where [simp del]: "(Float a_m a_e) * (Float b_m b_e) = Float (a_m * b_m) (a_e + b_e)"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   257
instance ..
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   258
end
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   259
30960
fec1a04b7220 power operation defined generic
haftmann
parents: 30242
diff changeset
   260
primrec float_pprt :: "float \<Rightarrow> float" where
fec1a04b7220 power operation defined generic
haftmann
parents: 30242
diff changeset
   261
  "float_pprt (Float a e) = (if 0 <= a then (Float a e) else 0)"
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   262
30960
fec1a04b7220 power operation defined generic
haftmann
parents: 30242
diff changeset
   263
primrec float_nprt :: "float \<Rightarrow> float" where
fec1a04b7220 power operation defined generic
haftmann
parents: 30242
diff changeset
   264
  "float_nprt (Float a e) = (if 0 <= a then 0 else (Float a e))" 
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   265
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   266
instantiation float :: ord begin
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
   267
definition le_float_def: "z \<le> (w :: float) \<equiv> real z \<le> real w"
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
   268
definition less_float_def: "z < (w :: float) \<equiv> real z < real w"
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   269
instance ..
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   270
end
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   271
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
   272
lemma real_of_float_add[simp]: "real (a + b) = real a + real (b :: float)"
41528
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
   273
  by (cases a, cases b) (simp add: algebra_simps plus_float.simps, 
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   274
      auto simp add: pow2_int[symmetric] pow2_add[symmetric])
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   275
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
   276
lemma real_of_float_minus[simp]: "real (- a) = - real (a :: float)"
41528
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
   277
  by (cases a) (simp add: uminus_float.simps)
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   278
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
   279
lemma real_of_float_sub[simp]: "real (a - b) = real a - real (b :: float)"
41528
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
   280
  by (cases a, cases b) (simp add: minus_float_def)
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   281
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
   282
lemma real_of_float_mult[simp]: "real (a*b) = real a * real (b :: float)"
41528
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
   283
  by (cases a, cases b) (simp add: times_float.simps pow2_add)
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   284
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
   285
lemma real_of_float_0[simp]: "real (0 :: float) = 0"
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   286
  by (auto simp add: zero_float_def float_zero)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   287
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
   288
lemma real_of_float_1[simp]: "real (1 :: float) = 1"
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   289
  by (auto simp add: one_float_def)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   290
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   291
lemma zero_le_float:
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
   292
  "(0 <= real (Float a b)) = (0 <= a)"
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   293
  apply auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   294
  apply (auto simp add: zero_le_mult_iff)
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   295
  apply (insert zero_less_pow2[of b])
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   296
  apply (simp_all)
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   297
  done
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   298
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   299
lemma float_le_zero:
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
   300
  "(real (Float a b) <= 0) = (a <= 0)"
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   301
  apply auto
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   302
  apply (auto simp add: mult_le_0_iff)
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   303
  apply (insert zero_less_pow2[of b])
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   304
  apply auto
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   305
  done
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   306
39161
75849a560c09 When comparing Floats use integers instead of reals (represented as rationals), generates less code when Floats are used.
hoelzl
parents: 36778
diff changeset
   307
lemma zero_less_float:
75849a560c09 When comparing Floats use integers instead of reals (represented as rationals), generates less code when Floats are used.
hoelzl
parents: 36778
diff changeset
   308
  "(0 < real (Float a b)) = (0 < a)"
75849a560c09 When comparing Floats use integers instead of reals (represented as rationals), generates less code when Floats are used.
hoelzl
parents: 36778
diff changeset
   309
  apply auto
75849a560c09 When comparing Floats use integers instead of reals (represented as rationals), generates less code when Floats are used.
hoelzl
parents: 36778
diff changeset
   310
  apply (auto simp add: zero_less_mult_iff)
75849a560c09 When comparing Floats use integers instead of reals (represented as rationals), generates less code when Floats are used.
hoelzl
parents: 36778
diff changeset
   311
  apply (insert zero_less_pow2[of b])
75849a560c09 When comparing Floats use integers instead of reals (represented as rationals), generates less code when Floats are used.
hoelzl
parents: 36778
diff changeset
   312
  apply (simp_all)
75849a560c09 When comparing Floats use integers instead of reals (represented as rationals), generates less code when Floats are used.
hoelzl
parents: 36778
diff changeset
   313
  done
75849a560c09 When comparing Floats use integers instead of reals (represented as rationals), generates less code when Floats are used.
hoelzl
parents: 36778
diff changeset
   314
75849a560c09 When comparing Floats use integers instead of reals (represented as rationals), generates less code when Floats are used.
hoelzl
parents: 36778
diff changeset
   315
lemma float_less_zero:
75849a560c09 When comparing Floats use integers instead of reals (represented as rationals), generates less code when Floats are used.
hoelzl
parents: 36778
diff changeset
   316
  "(real (Float a b) < 0) = (a < 0)"
75849a560c09 When comparing Floats use integers instead of reals (represented as rationals), generates less code when Floats are used.
hoelzl
parents: 36778
diff changeset
   317
  apply auto
75849a560c09 When comparing Floats use integers instead of reals (represented as rationals), generates less code when Floats are used.
hoelzl
parents: 36778
diff changeset
   318
  apply (auto simp add: mult_less_0_iff)
75849a560c09 When comparing Floats use integers instead of reals (represented as rationals), generates less code when Floats are used.
hoelzl
parents: 36778
diff changeset
   319
  apply (insert zero_less_pow2[of b])
75849a560c09 When comparing Floats use integers instead of reals (represented as rationals), generates less code when Floats are used.
hoelzl
parents: 36778
diff changeset
   320
  apply (simp_all)
75849a560c09 When comparing Floats use integers instead of reals (represented as rationals), generates less code when Floats are used.
hoelzl
parents: 36778
diff changeset
   321
  done
75849a560c09 When comparing Floats use integers instead of reals (represented as rationals), generates less code when Floats are used.
hoelzl
parents: 36778
diff changeset
   322
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
   323
declare real_of_float_simp[simp del]
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   324
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
   325
lemma real_of_float_pprt[simp]: "real (float_pprt a) = pprt (real a)"
41528
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
   326
  by (cases a) (auto simp add: zero_le_float float_le_zero)
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   327
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
   328
lemma real_of_float_nprt[simp]: "real (float_nprt a) = nprt (real a)"
41528
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
   329
  by (cases a) (auto simp add: zero_le_float float_le_zero)
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   330
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   331
instance float :: ab_semigroup_add
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   332
proof (intro_classes)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   333
  fix a b c :: float
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   334
  show "a + b + c = a + (b + c)"
41528
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
   335
    by (cases a, cases b, cases c)
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
   336
      (auto simp add: algebra_simps power_add[symmetric] plus_float.simps)
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   337
next
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   338
  fix a b :: float
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   339
  show "a + b = b + a"
41528
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
   340
    by (cases a, cases b) (simp add: plus_float.simps)
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   341
qed
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   342
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   343
instance float :: comm_monoid_mult
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   344
proof (intro_classes)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   345
  fix a b c :: float
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   346
  show "a * b * c = a * (b * c)"
41528
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
   347
    by (cases a, cases b, cases c) (simp add: times_float.simps)
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   348
next
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   349
  fix a b :: float
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   350
  show "a * b = b * a"
41528
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
   351
    by (cases a, cases b) (simp add: times_float.simps)
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   352
next
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   353
  fix a :: float
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   354
  show "1 * a = a"
41528
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
   355
    by (cases a) (simp add: times_float.simps one_float_def)
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   356
qed
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   357
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   358
(* Floats do NOT form a cancel_semigroup_add: *)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   359
lemma "0 + Float 0 1 = 0 + Float 0 2"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   360
  by (simp add: plus_float.simps zero_float_def)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   361
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   362
instance float :: comm_semiring
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   363
proof (intro_classes)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   364
  fix a b c :: float
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   365
  show "(a + b) * c = a * c + b * c"
41528
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
   366
    by (cases a, cases b, cases c) (simp add: plus_float.simps times_float.simps algebra_simps)
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   367
qed
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   368
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   369
(* Floats do NOT form an order, because "(x < y) = (x <= y & x <> y)" does NOT hold *)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   370
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   371
instance float :: zero_neq_one
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   372
proof (intro_classes)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   373
  show "(0::float) \<noteq> 1"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   374
    by (simp add: zero_float_def one_float_def)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   375
qed
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   376
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   377
lemma float_le_simp: "((x::float) \<le> y) = (0 \<le> y - x)"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   378
  by (auto simp add: le_float_def)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   379
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   380
lemma float_less_simp: "((x::float) < y) = (0 < y - x)"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   381
  by (auto simp add: less_float_def)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   382
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
   383
lemma real_of_float_min: "real (min x y :: float) = min (real x) (real y)" unfolding min_def le_float_def by auto
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
   384
lemma real_of_float_max: "real (max a b :: float) = max (real a) (real b)" unfolding max_def le_float_def by auto
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   385
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
   386
lemma float_power: "real (x ^ n :: float) = real x ^ n"
30960
fec1a04b7220 power operation defined generic
haftmann
parents: 30242
diff changeset
   387
  by (induct n) simp_all
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   388
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   389
lemma zero_le_pow2[simp]: "0 \<le> pow2 s"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   390
  apply (subgoal_tac "0 < pow2 s")
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   391
  apply (auto simp only:)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   392
  apply auto
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   393
  done
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   394
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   395
lemma pow2_less_0_eq_False[simp]: "(pow2 s < 0) = False"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   396
  apply auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   397
  apply (subgoal_tac "0 \<le> pow2 s")
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   398
  apply simp
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   399
  apply simp
24301
6c7f226b24c3 changed floatarith lemmas
obua
parents: 24124
diff changeset
   400
  done
6c7f226b24c3 changed floatarith lemmas
obua
parents: 24124
diff changeset
   401
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   402
lemma pow2_le_0_eq_False[simp]: "(pow2 s \<le> 0) = False"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   403
  apply auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   404
  apply (subgoal_tac "0 < pow2 s")
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   405
  apply simp
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   406
  apply simp
24301
6c7f226b24c3 changed floatarith lemmas
obua
parents: 24124
diff changeset
   407
  done
6c7f226b24c3 changed floatarith lemmas
obua
parents: 24124
diff changeset
   408
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   409
lemma float_pos_m_pos: "0 < Float m e \<Longrightarrow> 0 < m"
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
   410
  unfolding less_float_def real_of_float_simp real_of_float_0 zero_less_mult_iff
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   411
  by auto
19765
dfe940911617 misc cleanup;
wenzelm
parents: 16890
diff changeset
   412
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   413
lemma float_pos_less1_e_neg: assumes "0 < Float m e" and "Float m e < 1" shows "e < 0"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   414
proof -
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   415
  have "0 < m" using float_pos_m_pos `0 < Float m e` by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   416
  hence "0 \<le> real m" and "1 \<le> real m" by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   417
  
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   418
  show "e < 0"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   419
  proof (rule ccontr)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   420
    assume "\<not> e < 0" hence "0 \<le> e" by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   421
    hence "1 \<le> pow2 e" unfolding pow2_def by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   422
    from mult_mono[OF `1 \<le> real m` this `0 \<le> real m`]
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
   423
    have "1 \<le> Float m e" by (simp add: le_float_def real_of_float_simp)
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   424
    thus False using `Float m e < 1` unfolding less_float_def le_float_def by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   425
  qed
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   426
qed
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   427
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   428
lemma float_less1_mantissa_bound: assumes "0 < Float m e" "Float m e < 1" shows "m < 2^(nat (-e))"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   429
proof -
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   430
  have "e < 0" using float_pos_less1_e_neg assms by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   431
  have "\<And>x. (0::real) < 2^x" by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   432
  have "real m < 2^(nat (-e))" using `Float m e < 1`
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
   433
    unfolding less_float_def real_of_float_neg_exp[OF `e < 0`] real_of_float_1
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   434
          real_mult_less_iff1[of _ _ 1, OF `0 < 2^(nat (-e))`, symmetric] 
36778
739a9379e29b avoid using real-specific versions of generic lemmas
huffman
parents: 35344
diff changeset
   435
          mult_assoc by auto
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   436
  thus ?thesis unfolding real_of_int_less_iff[symmetric] by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   437
qed
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   438
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   439
function bitlen :: "int \<Rightarrow> int" where
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   440
"bitlen 0 = 0" | 
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   441
"bitlen -1 = 1" | 
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   442
"0 < x \<Longrightarrow> bitlen x = 1 + (bitlen (x div 2))" | 
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   443
"x < -1 \<Longrightarrow> bitlen x = 1 + (bitlen (x div 2))"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   444
  apply (case_tac "x = 0 \<or> x = -1 \<or> x < -1 \<or> x > 0")
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   445
  apply auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   446
  done
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   447
termination by (relation "measure (nat o abs)", auto)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   448
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   449
lemma bitlen_ge0: "0 \<le> bitlen x" by (induct x rule: bitlen.induct, auto)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   450
lemma bitlen_ge1: "x \<noteq> 0 \<Longrightarrow> 1 \<le> bitlen x" by (induct x rule: bitlen.induct, auto simp add: bitlen_ge0)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   451
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   452
lemma bitlen_bounds': assumes "0 < x" shows "2^nat (bitlen x - 1) \<le> x \<and> x + 1 \<le> 2^nat (bitlen x)" (is "?P x")
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   453
  using `0 < x`
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   454
proof (induct x rule: bitlen.induct)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   455
  fix x
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   456
  assume "0 < x" and hyp: "0 < x div 2 \<Longrightarrow> ?P (x div 2)" hence "0 \<le> x" and "x \<noteq> 0" by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   457
  { fix x have "0 \<le> 1 + bitlen x" using bitlen_ge0[of x] by auto } note gt0_pls1 = this
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   458
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   459
  have "0 < (2::int)" by auto
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   460
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   461
  show "?P x"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   462
  proof (cases "x = 1")
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   463
    case True show "?P x" unfolding True by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   464
  next
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   465
    case False hence "2 \<le> x" using `0 < x` `x \<noteq> 1` by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   466
    hence "2 div 2 \<le> x div 2" by (rule zdiv_mono1, auto)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   467
    hence "0 < x div 2" and "x div 2 \<noteq> 0" by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   468
    hence bitlen_s1_ge0: "0 \<le> bitlen (x div 2) - 1" using bitlen_ge1[OF `x div 2 \<noteq> 0`] by auto
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   469
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   470
    { from hyp[OF `0 < x div 2`]
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   471
      have "2 ^ nat (bitlen (x div 2) - 1) \<le> x div 2" by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   472
      hence "2 ^ nat (bitlen (x div 2) - 1) * 2 \<le> x div 2 * 2" by (rule mult_right_mono, auto)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   473
      also have "\<dots> \<le> x" using `0 < x` by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   474
      finally have "2^nat (1 + bitlen (x div 2) - 1) \<le> x" unfolding power_Suc2[symmetric] Suc_nat_eq_nat_zadd1[OF bitlen_s1_ge0] by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   475
    } moreover
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   476
    { have "x + 1 \<le> x - x mod 2 + 2"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   477
      proof -
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32069
diff changeset
   478
        have "x mod 2 < 2" using `0 < x` by auto
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32069
diff changeset
   479
        hence "x < x - x mod 2 +  2" unfolding algebra_simps by auto
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32069
diff changeset
   480
        thus ?thesis by auto
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   481
      qed
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   482
      also have "x - x mod 2 + 2 = (x div 2 + 1) * 2" unfolding algebra_simps using `0 < x` zdiv_zmod_equality2[of x 2 0] by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   483
      also have "\<dots> \<le> 2^nat (bitlen (x div 2)) * 2" using hyp[OF `0 < x div 2`, THEN conjunct2] by (rule mult_right_mono, auto)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   484
      also have "\<dots> = 2^(1 + nat (bitlen (x div 2)))" unfolding power_Suc2[symmetric] by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   485
      finally have "x + 1 \<le> 2^(1 + nat (bitlen (x div 2)))" .
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   486
    }
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   487
    ultimately show ?thesis
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   488
      unfolding bitlen.simps(3)[OF `0 < x`] nat_add_distrib[OF zero_le_one bitlen_ge0]
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   489
      unfolding add_commute nat_add_distrib[OF zero_le_one gt0_pls1]
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   490
      by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   491
  qed
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   492
next
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   493
  fix x :: int assume "x < -1" and "0 < x" hence False by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   494
  thus "?P x" by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   495
qed auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   496
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   497
lemma bitlen_bounds: assumes "0 < x" shows "2^nat (bitlen x - 1) \<le> x \<and> x < 2^nat (bitlen x)"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   498
  using bitlen_bounds'[OF `0<x`] by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   499
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   500
lemma bitlen_div: assumes "0 < m" shows "1 \<le> real m / 2^nat (bitlen m - 1)" and "real m / 2^nat (bitlen m - 1) < 2"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   501
proof -
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   502
  let ?B = "2^nat(bitlen m - 1)"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   503
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   504
  have "?B \<le> m" using bitlen_bounds[OF `0 <m`] ..
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   505
  hence "1 * ?B \<le> real m" unfolding real_of_int_le_iff[symmetric] by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   506
  thus "1 \<le> real m / ?B" by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   507
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   508
  have "m \<noteq> 0" using assms by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   509
  have "0 \<le> bitlen m - 1" using bitlen_ge1[OF `m \<noteq> 0`] by auto
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   510
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   511
  have "m < 2^nat(bitlen m)" using bitlen_bounds[OF `0 <m`] ..
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   512
  also have "\<dots> = 2^nat(bitlen m - 1 + 1)" using bitlen_ge1[OF `m \<noteq> 0`] by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   513
  also have "\<dots> = ?B * 2" unfolding nat_add_distrib[OF `0 \<le> bitlen m - 1` zero_le_one] by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   514
  finally have "real m < 2 * ?B" unfolding real_of_int_less_iff[symmetric] by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   515
  hence "real m / ?B < 2 * ?B / ?B" by (rule divide_strict_right_mono, auto)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   516
  thus "real m / ?B < 2" by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   517
qed
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   518
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   519
lemma float_gt1_scale: assumes "1 \<le> Float m e"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   520
  shows "0 \<le> e + (bitlen m - 1)"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   521
proof (cases "0 \<le> e")
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   522
  have "0 < Float m e" using assms unfolding less_float_def le_float_def by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   523
  hence "0 < m" using float_pos_m_pos by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   524
  hence "m \<noteq> 0" by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   525
  case True with bitlen_ge1[OF `m \<noteq> 0`] show ?thesis by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   526
next
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   527
  have "0 < Float m e" using assms unfolding less_float_def le_float_def by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   528
  hence "0 < m" using float_pos_m_pos by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   529
  hence "m \<noteq> 0" and "1 < (2::int)" by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   530
  case False let ?S = "2^(nat (-e))"
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
   531
  have "1 \<le> real m * inverse ?S" using assms unfolding le_float_def real_of_float_nge0_exp[OF False] by auto
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   532
  hence "1 * ?S \<le> real m * inverse ?S * ?S" by (rule mult_right_mono, auto)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   533
  hence "?S \<le> real m" unfolding mult_assoc by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   534
  hence "?S \<le> m" unfolding real_of_int_le_iff[symmetric] by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   535
  from this bitlen_bounds[OF `0 < m`, THEN conjunct2]
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   536
  have "nat (-e) < (nat (bitlen m))" unfolding power_strict_increasing_iff[OF `1 < 2`, symmetric] by (rule order_le_less_trans)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   537
  hence "-e < bitlen m" using False bitlen_ge0 by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   538
  thus ?thesis by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   539
qed
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   540
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
   541
lemma normalized_float: assumes "m \<noteq> 0" shows "real (Float m (- (bitlen m - 1))) = real m / 2^nat (bitlen m - 1)"
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   542
proof (cases "- (bitlen m - 1) = 0")
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
   543
  case True show ?thesis unfolding real_of_float_simp pow2_def using True by auto
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   544
next
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   545
  case False hence P: "\<not> 0 \<le> - (bitlen m - 1)" using bitlen_ge1[OF `m \<noteq> 0`] by auto
36778
739a9379e29b avoid using real-specific versions of generic lemmas
huffman
parents: 35344
diff changeset
   546
  show ?thesis unfolding real_of_float_nge0_exp[OF P] divide_inverse by auto
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   547
qed
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   548
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   549
lemma bitlen_Pls: "bitlen (Int.Pls) = Int.Pls" by (subst Pls_def, subst Pls_def, simp)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   550
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   551
lemma bitlen_Min: "bitlen (Int.Min) = Int.Bit1 Int.Pls" by (subst Min_def, simp add: Bit1_def) 
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   552
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   553
lemma bitlen_B0: "bitlen (Int.Bit0 b) = (if iszero b then Int.Pls else Int.succ (bitlen b))"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   554
  apply (auto simp add: iszero_def succ_def)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   555
  apply (simp add: Bit0_def Pls_def)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   556
  apply (subst Bit0_def)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   557
  apply simp
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   558
  apply (subgoal_tac "0 < 2 * b \<or> 2 * b < -1")
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   559
  apply auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   560
  done
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   561
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   562
lemma bitlen_B1: "bitlen (Int.Bit1 b) = (if iszero (Int.succ b) then Int.Bit1 Int.Pls else Int.succ (bitlen b))"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   563
proof -
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   564
  have h: "! x. (2*x + 1) div 2 = (x::int)"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   565
    by arith    
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   566
  show ?thesis
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   567
    apply (auto simp add: iszero_def succ_def)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   568
    apply (subst Bit1_def)+
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   569
    apply simp
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   570
    apply (subgoal_tac "2 * b + 1 = -1")
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   571
    apply (simp only:)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   572
    apply simp_all
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   573
    apply (subst Bit1_def)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   574
    apply simp
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   575
    apply (subgoal_tac "0 < 2 * b + 1 \<or> 2 * b + 1 < -1")
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   576
    apply (auto simp add: h)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   577
    done
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   578
qed
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   579
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   580
lemma bitlen_number_of: "bitlen (number_of w) = number_of (bitlen w)"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   581
  by (simp add: number_of_is_id)
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   582
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   583
lemma [code]: "bitlen x = 
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   584
     (if x = 0  then 0 
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   585
 else if x = -1 then 1 
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   586
                else (1 + (bitlen (x div 2))))"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   587
  by (cases "x = 0 \<or> x = -1 \<or> 0 < x") auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   588
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   589
definition lapprox_posrat :: "nat \<Rightarrow> int \<Rightarrow> int \<Rightarrow> float"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   590
where
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   591
  "lapprox_posrat prec x y = 
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   592
   (let 
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   593
       l = nat (int prec + bitlen y - bitlen x) ;
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   594
       d = (x * 2^l) div y
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   595
    in normfloat (Float d (- (int l))))"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   596
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   597
lemma pow2_minus: "pow2 (-x) = inverse (pow2 x)"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   598
  unfolding pow2_neg[of "-x"] by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   599
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   600
lemma lapprox_posrat: 
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   601
  assumes x: "0 \<le> x"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   602
  and y: "0 < y"
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
   603
  shows "real (lapprox_posrat prec x y) \<le> real x / real y"
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   604
proof -
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   605
  let ?l = "nat (int prec + bitlen y - bitlen x)"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   606
  
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   607
  have "real (x * 2^?l div y) * inverse (2^?l) \<le> (real (x * 2^?l) / real y) * inverse (2^?l)" 
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   608
    by (rule mult_right_mono, fact real_of_int_div4, simp)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   609
  also have "\<dots> \<le> (real x / real y) * 2^?l * inverse (2^?l)" by auto
36778
739a9379e29b avoid using real-specific versions of generic lemmas
huffman
parents: 35344
diff changeset
   610
  finally have "real (x * 2^?l div y) * inverse (2^?l) \<le> real x / real y" unfolding mult_assoc by auto
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
   611
  thus ?thesis unfolding lapprox_posrat_def Let_def normfloat real_of_float_simp
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   612
    unfolding pow2_minus pow2_int minus_minus .
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   613
qed
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   614
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   615
lemma real_of_int_div_mult: 
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   616
  fixes x y c :: int assumes "0 < y" and "0 < c"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   617
  shows "real (x div y) \<le> real (x * c div y) * inverse (real c)"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   618
proof -
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   619
  have "c * (x div y) + 0 \<le> c * x div y" unfolding zdiv_zmult1_eq[of c x y]
44766
d4d33a4d7548 avoid using legacy theorem names
huffman
parents: 42676
diff changeset
   620
    by (rule add_left_mono, 
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   621
        auto intro!: mult_nonneg_nonneg 
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   622
             simp add: pos_imp_zdiv_nonneg_iff[OF `0 < y`] `0 < c`[THEN less_imp_le] pos_mod_sign[OF `0 < y`])
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   623
  hence "real (x div y) * real c \<le> real (x * c div y)" 
44766
d4d33a4d7548 avoid using legacy theorem names
huffman
parents: 42676
diff changeset
   624
    unfolding real_of_int_mult[symmetric] real_of_int_le_iff mult_commute by auto
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   625
  hence "real (x div y) * real c * inverse (real c) \<le> real (x * c div y) * inverse (real c)"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   626
    using `0 < c` by auto
36778
739a9379e29b avoid using real-specific versions of generic lemmas
huffman
parents: 35344
diff changeset
   627
  thus ?thesis unfolding mult_assoc using `0 < c` by auto
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   628
qed
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   629
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   630
lemma lapprox_posrat_bottom: assumes "0 < y"
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
   631
  shows "real (x div y) \<le> real (lapprox_posrat n x y)" 
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   632
proof -
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   633
  have pow: "\<And>x. (0::int) < 2^x" by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   634
  show ?thesis
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
   635
    unfolding lapprox_posrat_def Let_def real_of_float_add normfloat real_of_float_simp pow2_minus pow2_int
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   636
    using real_of_int_div_mult[OF `0 < y` pow] by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   637
qed
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   638
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   639
lemma lapprox_posrat_nonneg: assumes "0 \<le> x" and "0 < y"
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
   640
  shows "0 \<le> real (lapprox_posrat n x y)" 
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   641
proof -
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   642
  show ?thesis
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
   643
    unfolding lapprox_posrat_def Let_def real_of_float_add normfloat real_of_float_simp pow2_minus pow2_int
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   644
    using pos_imp_zdiv_nonneg_iff[OF `0 < y`] assms by (auto intro!: mult_nonneg_nonneg)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   645
qed
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   646
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   647
definition rapprox_posrat :: "nat \<Rightarrow> int \<Rightarrow> int \<Rightarrow> float"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   648
where
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   649
  "rapprox_posrat prec x y = (let
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   650
     l = nat (int prec + bitlen y - bitlen x) ;
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   651
     X = x * 2^l ;
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   652
     d = X div y ;
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   653
     m = X mod y
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   654
   in normfloat (Float (d + (if m = 0 then 0 else 1)) (- (int l))))"
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   655
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   656
lemma rapprox_posrat:
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   657
  assumes x: "0 \<le> x"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   658
  and y: "0 < y"
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
   659
  shows "real x / real y \<le> real (rapprox_posrat prec x y)"
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   660
proof -
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   661
  let ?l = "nat (int prec + bitlen y - bitlen x)" let ?X = "x * 2^?l"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   662
  show ?thesis 
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   663
  proof (cases "?X mod y = 0")
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   664
    case True hence "y \<noteq> 0" and "y dvd ?X" using `0 < y` by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   665
    from real_of_int_div[OF this]
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   666
    have "real (?X div y) * inverse (2 ^ ?l) = real ?X / real y * inverse (2 ^ ?l)" by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   667
    also have "\<dots> = real x / real y * (2^?l * inverse (2^?l))" by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   668
    finally have "real (?X div y) * inverse (2^?l) = real x / real y" by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   669
    thus ?thesis unfolding rapprox_posrat_def Let_def normfloat if_P[OF True] 
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
   670
      unfolding real_of_float_simp pow2_minus pow2_int minus_minus by auto
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   671
  next
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   672
    case False
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   673
    have "0 \<le> real y" and "real y \<noteq> 0" using `0 < y` by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   674
    have "0 \<le> real y * 2^?l" by (rule mult_nonneg_nonneg, rule `0 \<le> real y`, auto)
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   675
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   676
    have "?X = y * (?X div y) + ?X mod y" by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   677
    also have "\<dots> \<le> y * (?X div y) + y" by (rule add_mono, auto simp add: pos_mod_bound[OF `0 < y`, THEN less_imp_le])
44766
d4d33a4d7548 avoid using legacy theorem names
huffman
parents: 42676
diff changeset
   678
    also have "\<dots> = y * (?X div y + 1)" unfolding right_distrib by auto
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   679
    finally have "real ?X \<le> real y * real (?X div y + 1)" unfolding real_of_int_le_iff real_of_int_mult[symmetric] .
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   680
    hence "real ?X / (real y * 2^?l) \<le> real y * real (?X div y + 1) / (real y * 2^?l)" 
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   681
      by (rule divide_right_mono, simp only: `0 \<le> real y * 2^?l`)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   682
    also have "\<dots> = real y * real (?X div y + 1) / real y / 2^?l" by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   683
    also have "\<dots> = real (?X div y + 1) * inverse (2^?l)" unfolding nonzero_mult_divide_cancel_left[OF `real y \<noteq> 0`] 
36778
739a9379e29b avoid using real-specific versions of generic lemmas
huffman
parents: 35344
diff changeset
   684
      unfolding divide_inverse ..
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
   685
    finally show ?thesis unfolding rapprox_posrat_def Let_def normfloat real_of_float_simp if_not_P[OF False]
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   686
      unfolding pow2_minus pow2_int minus_minus by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   687
  qed
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   688
qed
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   689
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   690
lemma rapprox_posrat_le1: assumes "0 \<le> x" and "0 < y" and "x \<le> y"
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
   691
  shows "real (rapprox_posrat n x y) \<le> 1"
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   692
proof -
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   693
  let ?l = "nat (int n + bitlen y - bitlen x)" let ?X = "x * 2^?l"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   694
  show ?thesis
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   695
  proof (cases "?X mod y = 0")
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   696
    case True hence "y \<noteq> 0" and "y dvd ?X" using `0 < y` by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   697
    from real_of_int_div[OF this]
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   698
    have "real (?X div y) * inverse (2 ^ ?l) = real ?X / real y * inverse (2 ^ ?l)" by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   699
    also have "\<dots> = real x / real y * (2^?l * inverse (2^?l))" by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   700
    finally have "real (?X div y) * inverse (2^?l) = real x / real y" by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   701
    also have "real x / real y \<le> 1" using `0 \<le> x` and `0 < y` and `x \<le> y` by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   702
    finally show ?thesis unfolding rapprox_posrat_def Let_def normfloat if_P[OF True]
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
   703
      unfolding real_of_float_simp pow2_minus pow2_int minus_minus by auto
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   704
  next
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   705
    case False
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   706
    have "x \<noteq> y"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   707
    proof (rule ccontr)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   708
      assume "\<not> x \<noteq> y" hence "x = y" by auto
30034
60f64f112174 removed redundant thms
nipkow
parents: 29988
diff changeset
   709
      have "?X mod y = 0" unfolding `x = y` using mod_mult_self1_is_0 by auto
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   710
      thus False using False by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   711
    qed
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   712
    hence "x < y" using `x \<le> y` by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   713
    hence "real x / real y < 1" using `0 < y` and `0 \<le> x` by auto
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   714
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   715
    from real_of_int_div4[of "?X" y]
35344
e0b46cd72414 moved some lemmas from RealPow to RealDef; changed orientation of real_of_int_power
huffman
parents: 35032
diff changeset
   716
    have "real (?X div y) \<le> (real x / real y) * 2^?l" unfolding real_of_int_mult times_divide_eq_left real_of_int_power real_number_of .
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   717
    also have "\<dots> < 1 * 2^?l" using `real x / real y < 1` by (rule mult_strict_right_mono, auto)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   718
    finally have "?X div y < 2^?l" unfolding real_of_int_less_iff[of _ "2^?l", symmetric] by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   719
    hence "?X div y + 1 \<le> 2^?l" by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   720
    hence "real (?X div y + 1) * inverse (2^?l) \<le> 2^?l * inverse (2^?l)"
35344
e0b46cd72414 moved some lemmas from RealPow to RealDef; changed orientation of real_of_int_power
huffman
parents: 35032
diff changeset
   721
      unfolding real_of_int_le_iff[of _ "2^?l", symmetric] real_of_int_power real_number_of
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   722
      by (rule mult_right_mono, auto)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   723
    hence "real (?X div y + 1) * inverse (2^?l) \<le> 1" by auto
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
   724
    thus ?thesis unfolding rapprox_posrat_def Let_def normfloat real_of_float_simp if_not_P[OF False]
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   725
      unfolding pow2_minus pow2_int minus_minus by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   726
  qed
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   727
qed
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   728
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   729
lemma zdiv_greater_zero: fixes a b :: int assumes "0 < a" and "a \<le> b"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   730
  shows "0 < b div a"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   731
proof (rule ccontr)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   732
  have "0 \<le> b" using assms by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   733
  assume "\<not> 0 < b div a" hence "b div a = 0" using `0 \<le> b`[unfolded pos_imp_zdiv_nonneg_iff[OF `0<a`, of b, symmetric]] by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   734
  have "b = a * (b div a) + b mod a" by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   735
  hence "b = b mod a" unfolding `b div a = 0` by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   736
  hence "b < a" using `0 < a`[THEN pos_mod_bound, of b] by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   737
  thus False using `a \<le> b` by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   738
qed
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   739
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   740
lemma rapprox_posrat_less1: assumes "0 \<le> x" and "0 < y" and "2 * x < y" and "0 < n"
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
   741
  shows "real (rapprox_posrat n x y) < 1"
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   742
proof (cases "x = 0")
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
   743
  case True thus ?thesis unfolding rapprox_posrat_def True Let_def normfloat real_of_float_simp by auto
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   744
next
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   745
  case False hence "0 < x" using `0 \<le> x` by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   746
  hence "x < y" using assms by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   747
  
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   748
  let ?l = "nat (int n + bitlen y - bitlen x)" let ?X = "x * 2^?l"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   749
  show ?thesis
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   750
  proof (cases "?X mod y = 0")
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   751
    case True hence "y \<noteq> 0" and "y dvd ?X" using `0 < y` by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   752
    from real_of_int_div[OF this]
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   753
    have "real (?X div y) * inverse (2 ^ ?l) = real ?X / real y * inverse (2 ^ ?l)" by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   754
    also have "\<dots> = real x / real y * (2^?l * inverse (2^?l))" by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   755
    finally have "real (?X div y) * inverse (2^?l) = real x / real y" by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   756
    also have "real x / real y < 1" using `0 \<le> x` and `0 < y` and `x < y` by auto
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
   757
    finally show ?thesis unfolding rapprox_posrat_def Let_def normfloat real_of_float_simp if_P[OF True]
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   758
      unfolding pow2_minus pow2_int minus_minus by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   759
  next
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   760
    case False
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   761
    hence "(real x / real y) < 1 / 2" using `0 < y` and `0 \<le> x` `2 * x < y` by auto
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   762
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   763
    have "0 < ?X div y"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   764
    proof -
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   765
      have "2^nat (bitlen x - 1) \<le> y" and "y < 2^nat (bitlen y)"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32069
diff changeset
   766
        using bitlen_bounds[OF `0 < x`, THEN conjunct1] bitlen_bounds[OF `0 < y`, THEN conjunct2] `x < y` by auto
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   767
      hence "(2::int)^nat (bitlen x - 1) < 2^nat (bitlen y)" by (rule order_le_less_trans)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   768
      hence "bitlen x \<le> bitlen y" by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   769
      hence len_less: "nat (bitlen x - 1) \<le> nat (int (n - 1) + bitlen y)" by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   770
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   771
      have "x \<noteq> 0" and "y \<noteq> 0" using `0 < x` `0 < y` by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   772
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   773
      have exp_eq: "nat (int (n - 1) + bitlen y) - nat (bitlen x - 1) = ?l"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32069
diff changeset
   774
        using `bitlen x \<le> bitlen y` bitlen_ge1[OF `x \<noteq> 0`] bitlen_ge1[OF `y \<noteq> 0`] `0 < n` by auto
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   775
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   776
      have "y * 2^nat (bitlen x - 1) \<le> y * x" 
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32069
diff changeset
   777
        using bitlen_bounds[OF `0 < x`, THEN conjunct1] `0 < y`[THEN less_imp_le] by (rule mult_left_mono)
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   778
      also have "\<dots> \<le> 2^nat (bitlen y) * x" using bitlen_bounds[OF `0 < y`, THEN conjunct2, THEN less_imp_le] `0 \<le> x` by (rule mult_right_mono)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   779
      also have "\<dots> \<le> x * 2^nat (int (n - 1) + bitlen y)" unfolding mult_commute[of x] by (rule mult_right_mono, auto simp add: `0 \<le> x`)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   780
      finally have "real y * 2^nat (bitlen x - 1) * inverse (2^nat (bitlen x - 1)) \<le> real x * 2^nat (int (n - 1) + bitlen y) * inverse (2^nat (bitlen x - 1))"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32069
diff changeset
   781
        unfolding real_of_int_le_iff[symmetric] by auto
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   782
      hence "real y \<le> real x * (2^nat (int (n - 1) + bitlen y) / (2^nat (bitlen x - 1)))" 
36778
739a9379e29b avoid using real-specific versions of generic lemmas
huffman
parents: 35344
diff changeset
   783
        unfolding mult_assoc divide_inverse by auto
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   784
      also have "\<dots> = real x * (2^(nat (int (n - 1) + bitlen y) - nat (bitlen x - 1)))" using power_diff[of "2::real", OF _ len_less] by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   785
      finally have "y \<le> x * 2^?l" unfolding exp_eq unfolding real_of_int_le_iff[symmetric] by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   786
      thus ?thesis using zdiv_greater_zero[OF `0 < y`] by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   787
    qed
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   788
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   789
    from real_of_int_div4[of "?X" y]
35344
e0b46cd72414 moved some lemmas from RealPow to RealDef; changed orientation of real_of_int_power
huffman
parents: 35032
diff changeset
   790
    have "real (?X div y) \<le> (real x / real y) * 2^?l" unfolding real_of_int_mult times_divide_eq_left real_of_int_power real_number_of .
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   791
    also have "\<dots> < 1/2 * 2^?l" using `real x / real y < 1/2` by (rule mult_strict_right_mono, auto)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   792
    finally have "?X div y * 2 < 2^?l" unfolding real_of_int_less_iff[of _ "2^?l", symmetric] by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   793
    hence "?X div y + 1 < 2^?l" using `0 < ?X div y` by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   794
    hence "real (?X div y + 1) * inverse (2^?l) < 2^?l * inverse (2^?l)"
35344
e0b46cd72414 moved some lemmas from RealPow to RealDef; changed orientation of real_of_int_power
huffman
parents: 35032
diff changeset
   795
      unfolding real_of_int_less_iff[of _ "2^?l", symmetric] real_of_int_power real_number_of
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   796
      by (rule mult_strict_right_mono, auto)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   797
    hence "real (?X div y + 1) * inverse (2^?l) < 1" by auto
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
   798
    thus ?thesis unfolding rapprox_posrat_def Let_def normfloat real_of_float_simp if_not_P[OF False]
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   799
      unfolding pow2_minus pow2_int minus_minus by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   800
  qed
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   801
qed
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   802
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   803
lemma approx_rat_pattern: fixes P and ps :: "nat * int * int"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   804
  assumes Y: "\<And>y prec x. \<lbrakk>y = 0; ps = (prec, x, 0)\<rbrakk> \<Longrightarrow> P" 
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   805
  and A: "\<And>x y prec. \<lbrakk>0 \<le> x; 0 < y; ps = (prec, x, y)\<rbrakk> \<Longrightarrow> P"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   806
  and B: "\<And>x y prec. \<lbrakk>x < 0; 0 < y; ps = (prec, x, y)\<rbrakk> \<Longrightarrow> P"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   807
  and C: "\<And>x y prec. \<lbrakk>x < 0; y < 0; ps = (prec, x, y)\<rbrakk> \<Longrightarrow> P"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   808
  and D: "\<And>x y prec. \<lbrakk>0 \<le> x; y < 0; ps = (prec, x, y)\<rbrakk> \<Longrightarrow> P"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   809
  shows P
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   810
proof -
41528
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
   811
  obtain prec x y where [simp]: "ps = (prec, x, y)" by (cases ps) auto
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   812
  from Y have "y = 0 \<Longrightarrow> P" by auto
41528
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
   813
  moreover {
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
   814
    assume "0 < y"
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
   815
    have P
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
   816
    proof (cases "0 \<le> x")
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
   817
      case True
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
   818
      with A and `0 < y` show P by auto
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
   819
    next
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
   820
      case False
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
   821
      with B and `0 < y` show P by auto
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
   822
    qed
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
   823
  } 
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
   824
  moreover {
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
   825
    assume "y < 0"
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
   826
    have P
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
   827
    proof (cases "0 \<le> x")
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
   828
      case True
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
   829
      with D and `y < 0` show P by auto
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
   830
    next
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
   831
      case False
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
   832
      with C and `y < 0` show P by auto
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
   833
    qed
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
   834
  }
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
   835
  ultimately show P by (cases "y = 0 \<or> 0 < y \<or> y < 0") auto
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   836
qed
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   837
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   838
function lapprox_rat :: "nat \<Rightarrow> int \<Rightarrow> int \<Rightarrow> float"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   839
where
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   840
  "y = 0 \<Longrightarrow> lapprox_rat prec x y = 0"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   841
| "0 \<le> x \<Longrightarrow> 0 < y \<Longrightarrow> lapprox_rat prec x y = lapprox_posrat prec x y"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   842
| "x < 0 \<Longrightarrow> 0 < y \<Longrightarrow> lapprox_rat prec x y = - (rapprox_posrat prec (-x) y)"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   843
| "x < 0 \<Longrightarrow> y < 0 \<Longrightarrow> lapprox_rat prec x y = lapprox_posrat prec (-x) (-y)"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   844
| "0 \<le> x \<Longrightarrow> y < 0 \<Longrightarrow> lapprox_rat prec x y = - (rapprox_posrat prec x (-y))"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   845
apply simp_all by (rule approx_rat_pattern)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   846
termination by lexicographic_order
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   847
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   848
lemma compute_lapprox_rat[code]:
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   849
      "lapprox_rat prec x y = (if y = 0 then 0 else if 0 \<le> x then (if 0 < y then lapprox_posrat prec x y else - (rapprox_posrat prec x (-y))) 
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   850
                                                             else (if 0 < y then - (rapprox_posrat prec (-x) y) else lapprox_posrat prec (-x) (-y)))"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   851
  by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   852
            
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
   853
lemma lapprox_rat: "real (lapprox_rat prec x y) \<le> real x / real y"
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   854
proof -      
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   855
  have h[rule_format]: "! a b b'. b' \<le> b \<longrightarrow> a \<le> b' \<longrightarrow> a \<le> (b::real)" by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   856
  show ?thesis
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   857
    apply (case_tac "y = 0")
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   858
    apply simp
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   859
    apply (case_tac "0 \<le> x \<and> 0 < y")
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   860
    apply (simp add: lapprox_posrat)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   861
    apply (case_tac "x < 0 \<and> 0 < y")
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   862
    apply simp
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   863
    apply (subst minus_le_iff)   
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   864
    apply (rule h[OF rapprox_posrat])
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   865
    apply (simp_all)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   866
    apply (case_tac "x < 0 \<and> y < 0")
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   867
    apply simp
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   868
    apply (rule h[OF _ lapprox_posrat])
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   869
    apply (simp_all)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   870
    apply (case_tac "0 \<le> x \<and> y < 0")
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   871
    apply (simp)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   872
    apply (subst minus_le_iff)   
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   873
    apply (rule h[OF rapprox_posrat])
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   874
    apply simp_all
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   875
    apply arith
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   876
    done
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   877
qed
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   878
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   879
lemma lapprox_rat_bottom: assumes "0 \<le> x" and "0 < y"
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
   880
  shows "real (x div y) \<le> real (lapprox_rat n x y)" 
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   881
  unfolding lapprox_rat.simps(2)[OF assms]  using lapprox_posrat_bottom[OF `0<y`] .
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   882
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   883
function rapprox_rat :: "nat \<Rightarrow> int \<Rightarrow> int \<Rightarrow> float"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   884
where
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   885
  "y = 0 \<Longrightarrow> rapprox_rat prec x y = 0"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   886
| "0 \<le> x \<Longrightarrow> 0 < y \<Longrightarrow> rapprox_rat prec x y = rapprox_posrat prec x y"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   887
| "x < 0 \<Longrightarrow> 0 < y \<Longrightarrow> rapprox_rat prec x y = - (lapprox_posrat prec (-x) y)"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   888
| "x < 0 \<Longrightarrow> y < 0 \<Longrightarrow> rapprox_rat prec x y = rapprox_posrat prec (-x) (-y)"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   889
| "0 \<le> x \<Longrightarrow> y < 0 \<Longrightarrow> rapprox_rat prec x y = - (lapprox_posrat prec x (-y))"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   890
apply simp_all by (rule approx_rat_pattern)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   891
termination by lexicographic_order
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   892
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   893
lemma compute_rapprox_rat[code]:
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   894
      "rapprox_rat prec x y = (if y = 0 then 0 else if 0 \<le> x then (if 0 < y then rapprox_posrat prec x y else - (lapprox_posrat prec x (-y))) else 
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   895
                                                                  (if 0 < y then - (lapprox_posrat prec (-x) y) else rapprox_posrat prec (-x) (-y)))"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   896
  by auto
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   897
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
   898
lemma rapprox_rat: "real x / real y \<le> real (rapprox_rat prec x y)"
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   899
proof -      
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   900
  have h[rule_format]: "! a b b'. b' \<le> b \<longrightarrow> a \<le> b' \<longrightarrow> a \<le> (b::real)" by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   901
  show ?thesis
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   902
    apply (case_tac "y = 0")
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   903
    apply simp
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   904
    apply (case_tac "0 \<le> x \<and> 0 < y")
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   905
    apply (simp add: rapprox_posrat)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   906
    apply (case_tac "x < 0 \<and> 0 < y")
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   907
    apply simp
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   908
    apply (subst le_minus_iff)   
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   909
    apply (rule h[OF _ lapprox_posrat])
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   910
    apply (simp_all)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   911
    apply (case_tac "x < 0 \<and> y < 0")
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   912
    apply simp
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   913
    apply (rule h[OF rapprox_posrat])
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   914
    apply (simp_all)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   915
    apply (case_tac "0 \<le> x \<and> y < 0")
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   916
    apply (simp)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   917
    apply (subst le_minus_iff)   
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   918
    apply (rule h[OF _ lapprox_posrat])
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   919
    apply simp_all
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   920
    apply arith
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   921
    done
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   922
qed
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   923
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   924
lemma rapprox_rat_le1: assumes "0 \<le> x" and "0 < y" and "x \<le> y"
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
   925
  shows "real (rapprox_rat n x y) \<le> 1"
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   926
  unfolding rapprox_rat.simps(2)[OF `0 \<le> x` `0 < y`] using rapprox_posrat_le1[OF assms] .
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   927
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   928
lemma rapprox_rat_neg: assumes "x < 0" and "0 < y"
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
   929
  shows "real (rapprox_rat n x y) \<le> 0"
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   930
  unfolding rapprox_rat.simps(3)[OF assms] using lapprox_posrat_nonneg[of "-x" y n] assms by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   931
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   932
lemma rapprox_rat_nonneg_neg: assumes "0 \<le> x" and "y < 0"
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
   933
  shows "real (rapprox_rat n x y) \<le> 0"
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   934
  unfolding rapprox_rat.simps(5)[OF assms] using lapprox_posrat_nonneg[of x "-y" n] assms by auto
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   935
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   936
lemma rapprox_rat_nonpos_pos: assumes "x \<le> 0" and "0 < y"
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
   937
  shows "real (rapprox_rat n x y) \<le> 0"
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   938
proof (cases "x = 0") 
41528
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
   939
  case True
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
   940
  hence "0 \<le> x" by auto show ?thesis
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
   941
    unfolding rapprox_rat.simps(2)[OF `0 \<le> x` `0 < y`]
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
   942
    unfolding True rapprox_posrat_def Let_def
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
   943
    by auto
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   944
next
41528
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
   945
  case False
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
   946
  hence "x < 0" using assms by auto
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   947
  show ?thesis using rapprox_rat_neg[OF `x < 0` `0 < y`] .
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   948
qed
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   949
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   950
fun float_divl :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   951
where
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   952
  "float_divl prec (Float m1 s1) (Float m2 s2) = 
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   953
    (let
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   954
       l = lapprox_rat prec m1 m2;
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   955
       f = Float 1 (s1 - s2)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   956
     in
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   957
       f * l)"     
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   958
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
   959
lemma float_divl: "real (float_divl prec x y) \<le> real x / real y"
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   960
proof - 
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   961
  from float_split[of x] obtain mx sx where x: "x = Float mx sx" by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   962
  from float_split[of y] obtain my sy where y: "y = Float my sy" by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   963
  have "real mx / real my \<le> (real mx * pow2 sx / (real my * pow2 sy)) / (pow2 (sx - sy))"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   964
    apply (case_tac "my = 0")
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   965
    apply simp
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   966
    apply (case_tac "my > 0")       
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   967
    apply (subst pos_le_divide_eq)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   968
    apply simp
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   969
    apply (subst pos_le_divide_eq)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   970
    apply (simp add: mult_pos_pos)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   971
    apply simp
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   972
    apply (subst pow2_add[symmetric])
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   973
    apply simp
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   974
    apply (subgoal_tac "my < 0")
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   975
    apply auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   976
    apply (simp add: field_simps)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   977
    apply (subst pow2_add[symmetric])
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   978
    apply (simp add: field_simps)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   979
    done
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
   980
  then have "real (lapprox_rat prec mx my) \<le> (real mx * pow2 sx / (real my * pow2 sy)) / (pow2 (sx - sy))"
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   981
    by (rule order_trans[OF lapprox_rat])
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
   982
  then have "real (lapprox_rat prec mx my) * pow2 (sx - sy) \<le> real mx * pow2 sx / (real my * pow2 sy)"
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   983
    apply (subst pos_le_divide_eq[symmetric])
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   984
    apply simp_all
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   985
    done
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
   986
  then have "pow2 (sx - sy) * real (lapprox_rat prec mx my) \<le> real mx * pow2 sx / (real my * pow2 sy)"
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   987
    by (simp add: algebra_simps)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   988
  then show ?thesis
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
   989
    by (simp add: x y Let_def real_of_float_simp)
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   990
qed
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   991
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   992
lemma float_divl_lower_bound: assumes "0 \<le> x" and "0 < y" shows "0 \<le> float_divl prec x y"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   993
proof (cases x, cases y)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   994
  fix xm xe ym ye :: int
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
   995
  assume x_eq: "x = Float xm xe" and y_eq: "y = Float ym ye"
41528
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
   996
  have "0 \<le> xm"
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
   997
    using `0 \<le> x`[unfolded x_eq le_float_def real_of_float_simp real_of_float_0 zero_le_mult_iff]
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
   998
    by auto
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
   999
  have "0 < ym"
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
  1000
    using `0 < y`[unfolded y_eq less_float_def real_of_float_simp real_of_float_0 zero_less_mult_iff]
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
  1001
    by auto
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
  1002
41528
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
  1003
  have "\<And>n. 0 \<le> real (Float 1 n)"
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
  1004
    unfolding real_of_float_simp using zero_le_pow2 by auto
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
  1005
  moreover have "0 \<le> real (lapprox_rat prec xm ym)"
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
  1006
    apply (rule order_trans[OF _ lapprox_rat_bottom[OF `0 \<le> xm` `0 < ym`]])
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
  1007
    apply (auto simp add: `0 \<le> xm` pos_imp_zdiv_nonneg_iff[OF `0 < ym`])
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
  1008
    done
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1009
  ultimately show "0 \<le> float_divl prec x y"
41528
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
  1010
    unfolding x_eq y_eq float_divl.simps Let_def le_float_def real_of_float_0
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
  1011
    by (auto intro!: mult_nonneg_nonneg)
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1012
qed
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1013
41528
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
  1014
lemma float_divl_pos_less1_bound:
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
  1015
  assumes "0 < x" and "x < 1" and "0 < prec"
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
  1016
  shows "1 \<le> float_divl prec 1 x"
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1017
proof (cases x)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1018
  case (Float m e)
41528
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
  1019
  from `0 < x` `x < 1` have "0 < m" "e < 0"
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
  1020
    using float_pos_m_pos float_pos_less1_e_neg unfolding Float by auto
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1021
  let ?b = "nat (bitlen m)" and ?e = "nat (-e)"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1022
  have "1 \<le> m" and "m \<noteq> 0" using `0 < m` by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1023
  with bitlen_bounds[OF `0 < m`] have "m < 2^?b" and "(2::int) \<le> 2^?b" by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1024
  hence "1 \<le> bitlen m" using power_le_imp_le_exp[of "2::int" 1 ?b] by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1025
  hence pow_split: "nat (int prec + bitlen m - 1) = (prec - 1) + ?b" using `0 < prec` by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1026
  
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1027
  have pow_not0: "\<And>x. (2::real)^x \<noteq> 0" by auto
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
  1028
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1029
  from float_less1_mantissa_bound `0 < x` `x < 1` Float 
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1030
  have "m < 2^?e" by auto
41528
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
  1031
  with bitlen_bounds[OF `0 < m`, THEN conjunct1] have "(2::int)^nat (bitlen m - 1) < 2^?e"
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
  1032
    by (rule order_le_less_trans)
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1033
  from power_less_imp_less_exp[OF _ this]
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1034
  have "bitlen m \<le> - e" by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1035
  hence "(2::real)^?b \<le> 2^?e" by auto
41528
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
  1036
  hence "(2::real)^?b * inverse (2^?b) \<le> 2^?e * inverse (2^?b)"
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
  1037
    by (rule mult_right_mono) auto
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1038
  hence "(1::real) \<le> 2^?e * inverse (2^?b)" by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1039
  also
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1040
  let ?d = "real (2 ^ nat (int prec + bitlen m - 1) div m) * inverse (2 ^ nat (int prec + bitlen m - 1))"
41528
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
  1041
  {
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
  1042
    have "2^(prec - 1) * m \<le> 2^(prec - 1) * 2^?b"
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
  1043
      using `m < 2^?b`[THEN less_imp_le] by (rule mult_left_mono) auto
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
  1044
    also have "\<dots> = 2 ^ nat (int prec + bitlen m - 1)"
44766
d4d33a4d7548 avoid using legacy theorem names
huffman
parents: 42676
diff changeset
  1045
      unfolding pow_split power_add by auto
41528
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
  1046
    finally have "2^(prec - 1) * m div m \<le> 2 ^ nat (int prec + bitlen m - 1) div m"
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
  1047
      using `0 < m` by (rule zdiv_mono1)
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
  1048
    hence "2^(prec - 1) \<le> 2 ^ nat (int prec + bitlen m - 1) div m"
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
  1049
      unfolding div_mult_self2_is_id[OF `m \<noteq> 0`] .
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1050
    hence "2^(prec - 1) * inverse (2 ^ nat (int prec + bitlen m - 1)) \<le> ?d"
41528
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
  1051
      unfolding real_of_int_le_iff[of "2^(prec - 1)", symmetric] by auto
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
  1052
  }
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
  1053
  from mult_left_mono[OF this [unfolded pow_split power_add inverse_mult_distrib mult_assoc[symmetric] right_inverse[OF pow_not0] mult_1_left], of "2^?e"]
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1054
  have "2^?e * inverse (2^?b) \<le> 2^?e * ?d" unfolding pow_split power_add by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1055
  finally have "1 \<le> 2^?e * ?d" .
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1056
  
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1057
  have e_nat: "0 - e = int (nat (-e))" using `e < 0` by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1058
  have "bitlen 1 = 1" using bitlen.simps by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1059
  
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1060
  show ?thesis 
41528
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
  1061
    unfolding one_float_def Float float_divl.simps Let_def
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
  1062
      lapprox_rat.simps(2)[OF zero_le_one `0 < m`]
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
  1063
      lapprox_posrat_def `bitlen 1 = 1`
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
  1064
    unfolding le_float_def real_of_float_mult normfloat real_of_float_simp
276078f01ada eliminated global prems;
wenzelm
parents: 41024
diff changeset
  1065
      pow2_minus pow2_int e_nat
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1066
    using `1 \<le> 2^?e * ?d` by (auto simp add: pow2_def)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1067
qed
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
  1068
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1069
fun float_divr :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1070
where
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1071
  "float_divr prec (Float m1 s1) (Float m2 s2) = 
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1072
    (let
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1073
       r = rapprox_rat prec m1 m2;
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1074
       f = Float 1 (s1 - s2)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1075
     in
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1076
       f * r)"  
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
  1077
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
  1078
lemma float_divr: "real x / real y \<le> real (float_divr prec x y)"
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1079
proof - 
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1080
  from float_split[of x] obtain mx sx where x: "x = Float mx sx" by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1081
  from float_split[of y] obtain my sy where y: "y = Float my sy" by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1082
  have "real mx / real my \<ge> (real mx * pow2 sx / (real my * pow2 sy)) / (pow2 (sx - sy))"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1083
    apply (case_tac "my = 0")
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1084
    apply simp
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1085
    apply (case_tac "my > 0")
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1086
    apply auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1087
    apply (subst pos_divide_le_eq)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1088
    apply (rule mult_pos_pos)+
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1089
    apply simp_all
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1090
    apply (subst pow2_add[symmetric])
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1091
    apply simp
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1092
    apply (subgoal_tac "my < 0")
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1093
    apply auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1094
    apply (simp add: field_simps)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1095
    apply (subst pow2_add[symmetric])
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1096
    apply (simp add: field_simps)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1097
    done
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
  1098
  then have "real (rapprox_rat prec mx my) \<ge> (real mx * pow2 sx / (real my * pow2 sy)) / (pow2 (sx - sy))"
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1099
    by (rule order_trans[OF _ rapprox_rat])
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
  1100
  then have "real (rapprox_rat prec mx my) * pow2 (sx - sy) \<ge> real mx * pow2 sx / (real my * pow2 sy)"
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1101
    apply (subst pos_divide_le_eq[symmetric])
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1102
    apply simp_all
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1103
    done
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1104
  then show ?thesis
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
  1105
    by (simp add: x y Let_def algebra_simps real_of_float_simp)
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1106
qed
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
  1107
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1108
lemma float_divr_pos_less1_lower_bound: assumes "0 < x" and "x < 1" shows "1 \<le> float_divr prec 1 x"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1109
proof -
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
  1110
  have "1 \<le> 1 / real x" using `0 < x` and `x < 1` unfolding less_float_def by auto
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
  1111
  also have "\<dots> \<le> real (float_divr prec 1 x)" using float_divr[where x=1 and y=x] by auto
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1112
  finally show ?thesis unfolding le_float_def by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1113
qed
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1114
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1115
lemma float_divr_nonpos_pos_upper_bound: assumes "x \<le> 0" and "0 < y" shows "float_divr prec x y \<le> 0"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1116
proof (cases x, cases y)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1117
  fix xm xe ym ye :: int
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1118
  assume x_eq: "x = Float xm xe" and y_eq: "y = Float ym ye"
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
  1119
  have "xm \<le> 0" using `x \<le> 0`[unfolded x_eq le_float_def real_of_float_simp real_of_float_0 mult_le_0_iff] by auto
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
  1120
  have "0 < ym" using `0 < y`[unfolded y_eq less_float_def real_of_float_simp real_of_float_0 zero_less_mult_iff] by auto
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1121
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
  1122
  have "\<And>n. 0 \<le> real (Float 1 n)" unfolding real_of_float_simp using zero_le_pow2 by auto
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
  1123
  moreover have "real (rapprox_rat prec xm ym) \<le> 0" using rapprox_rat_nonpos_pos[OF `xm \<le> 0` `0 < ym`] .
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1124
  ultimately show "float_divr prec x y \<le> 0"
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
  1125
    unfolding x_eq y_eq float_divr.simps Let_def le_float_def real_of_float_0 real_of_float_mult by (auto intro!: mult_nonneg_nonpos)
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1126
qed
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
  1127
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1128
lemma float_divr_nonneg_neg_upper_bound: assumes "0 \<le> x" and "y < 0" shows "float_divr prec x y \<le> 0"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1129
proof (cases x, cases y)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1130
  fix xm xe ym ye :: int
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1131
  assume x_eq: "x = Float xm xe" and y_eq: "y = Float ym ye"
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
  1132
  have "0 \<le> xm" using `0 \<le> x`[unfolded x_eq le_float_def real_of_float_simp real_of_float_0 zero_le_mult_iff] by auto
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
  1133
  have "ym < 0" using `y < 0`[unfolded y_eq less_float_def real_of_float_simp real_of_float_0 mult_less_0_iff] by auto
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1134
  hence "0 < - ym" by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1135
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
  1136
  have "\<And>n. 0 \<le> real (Float 1 n)" unfolding real_of_float_simp using zero_le_pow2 by auto
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
  1137
  moreover have "real (rapprox_rat prec xm ym) \<le> 0" using rapprox_rat_nonneg_neg[OF `0 \<le> xm` `ym < 0`] .
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1138
  ultimately show "float_divr prec x y \<le> 0"
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
  1139
    unfolding x_eq y_eq float_divr.simps Let_def le_float_def real_of_float_0 real_of_float_mult by (auto intro!: mult_nonneg_nonpos)
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1140
qed
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1141
30960
fec1a04b7220 power operation defined generic
haftmann
parents: 30242
diff changeset
  1142
primrec round_down :: "nat \<Rightarrow> float \<Rightarrow> float" where
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1143
"round_down prec (Float m e) = (let d = bitlen m - int prec in
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1144
     if 0 < d then let P = 2^nat d ; n = m div P in Float n (e + d)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1145
              else Float m e)"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1146
30960
fec1a04b7220 power operation defined generic
haftmann
parents: 30242
diff changeset
  1147
primrec round_up :: "nat \<Rightarrow> float \<Rightarrow> float" where
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1148
"round_up prec (Float m e) = (let d = bitlen m - int prec in
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1149
  if 0 < d then let P = 2^nat d ; n = m div P ; r = m mod P in Float (n + (if r = 0 then 0 else 1)) (e + d) 
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1150
           else Float m e)"
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
  1151
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
  1152
lemma round_up: "real x \<le> real (round_up prec x)"
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1153
proof (cases x)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1154
  case (Float m e)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1155
  let ?d = "bitlen m - int prec"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1156
  let ?p = "(2::int)^nat ?d"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1157
  have "0 < ?p" by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1158
  show "?thesis"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1159
  proof (cases "0 < ?d")
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1160
    case True
35344
e0b46cd72414 moved some lemmas from RealPow to RealDef; changed orientation of real_of_int_power
huffman
parents: 35032
diff changeset
  1161
    hence pow_d: "pow2 ?d = real ?p" using pow2_int[symmetric] by simp
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1162
    show ?thesis
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1163
    proof (cases "m mod ?p = 0")
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1164
      case True
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1165
      have m: "m = m div ?p * ?p + 0" unfolding True[symmetric] using zdiv_zmod_equality2[where k=0, unfolded monoid_add_class.add_0_right, symmetric] .
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
  1166
      have "real (Float m e) = real (Float (m div ?p) (e + ?d))" unfolding real_of_float_simp arg_cong[OF m, of real]
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32069
diff changeset
  1167
        by (auto simp add: pow2_add `0 < ?d` pow_d)
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1168
      thus ?thesis
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32069
diff changeset
  1169
        unfolding Float round_up.simps Let_def if_P[OF `m mod ?p = 0`] if_P[OF `0 < ?d`]
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32069
diff changeset
  1170
        by auto
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1171
    next
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1172
      case False
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1173
      have "m = m div ?p * ?p + m mod ?p" unfolding zdiv_zmod_equality2[where k=0, unfolded monoid_add_class.add_0_right] ..
44766
d4d33a4d7548 avoid using legacy theorem names
huffman
parents: 42676
diff changeset
  1174
      also have "\<dots> \<le> (m div ?p + 1) * ?p" unfolding left_distrib mult_1 by (rule add_left_mono, rule pos_mod_bound[OF `0 < ?p`, THEN less_imp_le])
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
  1175
      finally have "real (Float m e) \<le> real (Float (m div ?p + 1) (e + ?d))" unfolding real_of_float_simp add_commute[of e]
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32069
diff changeset
  1176
        unfolding pow2_add mult_assoc[symmetric] real_of_int_le_iff[of m, symmetric]
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32069
diff changeset
  1177
        by (auto intro!: mult_mono simp add: pow2_add `0 < ?d` pow_d)
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1178
      thus ?thesis
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32069
diff changeset
  1179
        unfolding Float round_up.simps Let_def if_not_P[OF `\<not> m mod ?p = 0`] if_P[OF `0 < ?d`] .
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1180
    qed
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1181
  next
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1182
    case False
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1183
    show ?thesis
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1184
      unfolding Float round_up.simps Let_def if_not_P[OF False] .. 
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1185
  qed
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1186
qed
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
  1187
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
  1188
lemma round_down: "real (round_down prec x) \<le> real x"
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1189
proof (cases x)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1190
  case (Float m e)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1191
  let ?d = "bitlen m - int prec"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1192
  let ?p = "(2::int)^nat ?d"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1193
  have "0 < ?p" by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1194
  show "?thesis"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1195
  proof (cases "0 < ?d")
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1196
    case True
35344
e0b46cd72414 moved some lemmas from RealPow to RealDef; changed orientation of real_of_int_power
huffman
parents: 35032
diff changeset
  1197
    hence pow_d: "pow2 ?d = real ?p" using pow2_int[symmetric] by simp
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1198
    have "m div ?p * ?p \<le> m div ?p * ?p + m mod ?p" by (auto simp add: pos_mod_bound[OF `0 < ?p`, THEN less_imp_le])
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1199
    also have "\<dots> \<le> m" unfolding zdiv_zmod_equality2[where k=0, unfolded monoid_add_class.add_0_right] ..
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
  1200
    finally have "real (Float (m div ?p) (e + ?d)) \<le> real (Float m e)" unfolding real_of_float_simp add_commute[of e]
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1201
      unfolding pow2_add mult_assoc[symmetric] real_of_int_le_iff[of _ m, symmetric]
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1202
      by (auto intro!: mult_mono simp add: pow2_add `0 < ?d` pow_d)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1203
    thus ?thesis
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1204
      unfolding Float round_down.simps Let_def if_P[OF `0 < ?d`] .
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1205
  next
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1206
    case False
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1207
    show ?thesis
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1208
      unfolding Float round_down.simps Let_def if_not_P[OF False] .. 
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1209
  qed
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1210
qed
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1211
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1212
definition lb_mult :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" where
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1213
"lb_mult prec x y = (case normfloat (x * y) of Float m e \<Rightarrow> let
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1214
    l = bitlen m - int prec
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1215
  in if l > 0 then Float (m div (2^nat l)) (e + l)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1216
              else Float m e)"
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
  1217
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1218
definition ub_mult :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" where
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1219
"ub_mult prec x y = (case normfloat (x * y) of Float m e \<Rightarrow> let
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1220
    l = bitlen m - int prec
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1221
  in if l > 0 then Float (m div (2^nat l) + 1) (e + l)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1222
              else Float m e)"
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
  1223
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
  1224
lemma lb_mult: "real (lb_mult prec x y) \<le> real (x * y)"
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1225
proof (cases "normfloat (x * y)")
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1226
  case (Float m e)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1227
  hence "odd m \<or> (m = 0 \<and> e = 0)" by (rule normfloat_imp_odd_or_zero)
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1228
  let ?l = "bitlen m - int prec"
31098
73dd67adf90a replaced Ifloat => real_of_float and real, renamed ApproxEq => inequality, uneq => interpret_inequality, uneq' => approx_inequality, Ifloatarith => interpret_floatarith
hoelzl
parents: 31021
diff changeset
  1229
  have "real (lb_mult prec x y) \<le> real (normfloat (x * y))"
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1230
  proof (cases "?l > 0")
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1231
    case False thus ?thesis unfolding lb_mult_def Float Let_def float.cases by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1232
  next
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1233
    case True
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1234
    have "real (m div 2^(nat ?l)) * pow2 ?l \<le> real m"
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1235
    proof -
35344
e0b46cd72414 moved some lemmas from RealPow to RealDef; changed orientation of real_of_int_power
huffman
parents: 35032
diff changeset
  1236
      have "real (m div 2^(nat ?l)) * pow2 ?l = real (2^(nat ?l) * (m div 2^(nat ?l)))" unfolding real_of_int_mult real_of_int_power real_number_of unfolding pow2_int[symmetric] 
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32069
diff changeset
  1237
        using `?l > 0` by auto
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
  1238
      also have "\<dots> \<le> real (2^(nat ?l) * (m div 2^(nat ?l)) + m mod 2^(nat ?l))" unfolding real_of_int_add by auto
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
ho&#