src/HOL/Matrix_LP/ComputeFloat.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 47108 2a1953f0d20d
child 47455 26315a545e26
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
41959
b460124855b8 tuned headers;
wenzelm
parents: 41550
diff changeset
     1
(*  Title:      HOL/Matrix/ComputeFloat.thy
b460124855b8 tuned headers;
wenzelm
parents: 41550
diff changeset
     2
    Author:     Steven Obua
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
     3
*)
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
     4
20717
2244b0d719a0 add header
huffman
parents: 20485
diff changeset
     5
header {* Floating Point Representation of the Reals *}
2244b0d719a0 add header
huffman
parents: 20485
diff changeset
     6
29804
e15b74577368 Added new Float theory and moved old Library/Float.thy to ComputeFloat
hoelzl
parents: 29667
diff changeset
     7
theory ComputeFloat
41413
64cd30d6b0b8 explicit file specifications -- avoid secondary load path;
wenzelm
parents: 38273
diff changeset
     8
imports Complex_Main "~~/src/HOL/Library/Lattice_Algebras"
28952
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 27366
diff changeset
     9
uses "~~/src/Tools/float.ML" ("~~/src/HOL/Tools/float_arith.ML")
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
38273
d31a34569542 modernized some specifications;
wenzelm
parents: 35032
diff changeset
    12
definition int_of_real :: "real \<Rightarrow> int"
d31a34569542 modernized some specifications;
wenzelm
parents: 35032
diff changeset
    13
  where "int_of_real x = (SOME y. real y = x)"
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21256
diff changeset
    14
38273
d31a34569542 modernized some specifications;
wenzelm
parents: 35032
diff changeset
    15
definition real_is_int :: "real \<Rightarrow> bool"
d31a34569542 modernized some specifications;
wenzelm
parents: 35032
diff changeset
    16
  where "real_is_int x = (EX (u::int). x = real u)"
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    17
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    18
lemma real_is_int_def2: "real_is_int x = (x = real (int_of_real x))"
45495
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
    19
  by (auto simp add: real_is_int_def int_of_real_def)
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    20
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    21
lemma real_is_int_real[simp]: "real_is_int (real (x::int))"
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    22
by (auto simp add: real_is_int_def int_of_real_def)
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    23
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    24
lemma int_of_real_real[simp]: "int_of_real (real x) = x"
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    25
by (simp add: int_of_real_def)
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    26
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    27
lemma real_int_of_real[simp]: "real_is_int x \<Longrightarrow> real (int_of_real x) = x"
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    28
by (auto simp add: int_of_real_def real_is_int_def)
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    29
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    30
lemma real_is_int_add_int_of_real: "real_is_int a \<Longrightarrow> real_is_int b \<Longrightarrow> (int_of_real (a+b)) = (int_of_real a) + (int_of_real b)"
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    31
by (auto simp add: int_of_real_def real_is_int_def)
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    32
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    33
lemma real_is_int_add[simp]: "real_is_int a \<Longrightarrow> real_is_int b \<Longrightarrow> real_is_int (a+b)"
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    34
apply (subst real_is_int_def2)
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    35
apply (simp add: real_is_int_add_int_of_real real_int_of_real)
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    36
done
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    37
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    38
lemma int_of_real_sub: "real_is_int a \<Longrightarrow> real_is_int b \<Longrightarrow> (int_of_real (a-b)) = (int_of_real a) - (int_of_real b)"
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    39
by (auto simp add: int_of_real_def real_is_int_def)
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    40
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    41
lemma real_is_int_sub[simp]: "real_is_int a \<Longrightarrow> real_is_int b \<Longrightarrow> real_is_int (a-b)"
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    42
apply (subst real_is_int_def2)
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    43
apply (simp add: int_of_real_sub real_int_of_real)
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    44
done
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    45
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    46
lemma real_is_int_rep: "real_is_int x \<Longrightarrow> ?! (a::int). real a = x"
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    47
by (auto simp add: real_is_int_def)
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    48
19765
dfe940911617 misc cleanup;
wenzelm
parents: 16890
diff changeset
    49
lemma int_of_real_mult:
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    50
  assumes "real_is_int a" "real_is_int b"
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    51
  shows "(int_of_real (a*b)) = (int_of_real a) * (int_of_real b)"
45495
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
    52
  using assms
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
    53
  by (auto simp add: real_is_int_def real_of_int_mult[symmetric]
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
    54
           simp del: real_of_int_mult)
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    55
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    56
lemma real_is_int_mult[simp]: "real_is_int a \<Longrightarrow> real_is_int b \<Longrightarrow> real_is_int (a*b)"
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    57
apply (subst real_is_int_def2)
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    58
apply (simp add: int_of_real_mult)
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    59
done
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    60
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    61
lemma real_is_int_0[simp]: "real_is_int (0::real)"
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    62
by (simp add: real_is_int_def int_of_real_def)
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    63
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    64
lemma real_is_int_1[simp]: "real_is_int (1::real)"
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    65
proof -
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    66
  have "real_is_int (1::real) = real_is_int(real (1::int))" by auto
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    67
  also have "\<dots> = True" by (simp only: real_is_int_real)
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    68
  ultimately show ?thesis by auto
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    69
qed
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    70
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    71
lemma real_is_int_n1: "real_is_int (-1::real)"
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    72
proof -
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    73
  have "real_is_int (-1::real) = real_is_int(real (-1::int))" by auto
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    74
  also have "\<dots> = True" by (simp only: real_is_int_real)
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    75
  ultimately show ?thesis by auto
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    76
qed
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    77
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46988
diff changeset
    78
lemma real_is_int_numeral[simp]: "real_is_int (numeral x)"
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46988
diff changeset
    79
  by (auto simp: real_is_int_def intro!: exI[of _ "numeral x"])
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46988
diff changeset
    80
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46988
diff changeset
    81
lemma real_is_int_neg_numeral[simp]: "real_is_int (neg_numeral x)"
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46988
diff changeset
    82
  by (auto simp: real_is_int_def intro!: exI[of _ "neg_numeral x"])
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    83
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    84
lemma int_of_real_0[simp]: "int_of_real (0::real) = (0::int)"
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    85
by (simp add: int_of_real_def)
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    86
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    87
lemma int_of_real_1[simp]: "int_of_real (1::real) = (1::int)"
19765
dfe940911617 misc cleanup;
wenzelm
parents: 16890
diff changeset
    88
proof -
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    89
  have 1: "(1::real) = real (1::int)" by auto
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    90
  show ?thesis by (simp only: 1 int_of_real_real)
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    91
qed
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    92
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46988
diff changeset
    93
lemma int_of_real_numeral[simp]: "int_of_real (numeral b) = numeral b"
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46988
diff changeset
    94
  unfolding int_of_real_def
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46988
diff changeset
    95
  by (intro some_equality)
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46988
diff changeset
    96
     (auto simp add: real_of_int_inject[symmetric] simp del: real_of_int_inject)
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46988
diff changeset
    97
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46988
diff changeset
    98
lemma int_of_real_neg_numeral[simp]: "int_of_real (neg_numeral b) = neg_numeral b"
45495
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
    99
  unfolding int_of_real_def
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   100
  by (intro some_equality)
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   101
     (auto simp add: real_of_int_inject[symmetric] simp del: real_of_int_inject)
19765
dfe940911617 misc cleanup;
wenzelm
parents: 16890
diff changeset
   102
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   103
lemma int_div_zdiv: "int (a div b) = (int a) div (int b)"
23431
25ca91279a9b change simp rules for of_nat to work like int did previously (reorient of_nat_Suc, remove of_nat_mult [simp]); preserve original variable names in legacy int theorems
huffman
parents: 23365
diff changeset
   104
by (rule zdiv_int)
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   105
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   106
lemma int_mod_zmod: "int (a mod b) = (int a) mod (int b)"
23431
25ca91279a9b change simp rules for of_nat to work like int did previously (reorient of_nat_Suc, remove of_nat_mult [simp]); preserve original variable names in legacy int theorems
huffman
parents: 23365
diff changeset
   107
by (rule zmod_int)
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   108
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   109
lemma abs_div_2_less: "a \<noteq> 0 \<Longrightarrow> a \<noteq> -1 \<Longrightarrow> abs((a::int) div 2) < abs a"
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   110
by arith
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   111
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46988
diff changeset
   112
lemma norm_0_1: "(1::_::numeral) = Numeral1"
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   113
  by auto
19765
dfe940911617 misc cleanup;
wenzelm
parents: 16890
diff changeset
   114
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   115
lemma add_left_zero: "0 + a = (a::'a::comm_monoid_add)"
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   116
  by simp
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   117
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   118
lemma add_right_zero: "a + 0 = (a::'a::comm_monoid_add)"
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   119
  by simp
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   120
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   121
lemma mult_left_one: "1 * a = (a::'a::semiring_1)"
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   122
  by simp
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   123
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   124
lemma mult_right_one: "a * 1 = (a::'a::semiring_1)"
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   125
  by simp
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   126
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46988
diff changeset
   127
lemma int_pow_0: "(a::int)^0 = 1"
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   128
  by simp
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   129
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   130
lemma int_pow_1: "(a::int)^(Numeral1) = a"
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   131
  by simp
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   132
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46988
diff changeset
   133
lemma one_eq_Numeral1_nring: "(1::'a::numeral) = Numeral1"
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   134
  by simp
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   135
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   136
lemma one_eq_Numeral1_nat: "(1::nat) = Numeral1"
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   137
  by simp
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   138
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46988
diff changeset
   139
lemma zpower_Pls: "(z::int)^0 = Numeral1"
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   140
  by simp
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   141
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   142
lemma fst_cong: "a=a' \<Longrightarrow> fst (a,b) = fst (a',b)"
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   143
  by simp
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   144
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   145
lemma snd_cong: "b=b' \<Longrightarrow> snd (a,b) = snd (a,b')"
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   146
  by simp
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   147
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   148
lemma lift_bool: "x \<Longrightarrow> x=True"
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   149
  by simp
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   150
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   151
lemma nlift_bool: "~x \<Longrightarrow> x=False"
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   152
  by simp
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   153
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   154
lemma not_false_eq_true: "(~ False) = True" by simp
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   155
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   156
lemma not_true_eq_false: "(~ True) = False" by simp
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   157
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46988
diff changeset
   158
lemmas powerarith = nat_numeral zpower_numeral_even
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46988
diff changeset
   159
  zpower_numeral_odd zpower_Pls
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   160
45495
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   161
definition float :: "(int \<times> int) \<Rightarrow> real" where
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   162
  "float = (\<lambda>(a, b). real a * 2 powr real b)"
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   163
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   164
lemma float_add_l0: "float (0, e) + x = x"
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   165
  by (simp add: float_def)
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   166
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   167
lemma float_add_r0: "x + float (0, e) = x"
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   168
  by (simp add: float_def)
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   169
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   170
lemma float_add:
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   171
  "float (a1, e1) + float (a2, e2) =
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   172
  (if e1<=e2 then float (a1+a2*2^(nat(e2-e1)), e1) else float (a1*2^(nat (e1-e2))+a2, e2))"
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   173
  by (simp add: float_def algebra_simps powr_realpow[symmetric] powr_divide2[symmetric])
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   174
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   175
lemma float_mult_l0: "float (0, e) * x = float (0, 0)"
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   176
  by (simp add: float_def)
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   177
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   178
lemma float_mult_r0: "x * float (0, e) = float (0, 0)"
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   179
  by (simp add: float_def)
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   180
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   181
lemma float_mult:
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   182
  "float (a1, e1) * float (a2, e2) = (float (a1 * a2, e1 + e2))"
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   183
  by (simp add: float_def powr_add)
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   184
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   185
lemma float_minus:
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   186
  "- (float (a,b)) = float (-a, b)"
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   187
  by (simp add: float_def)
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   188
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   189
lemma zero_le_float:
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   190
  "(0 <= float (a,b)) = (0 <= a)"
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   191
  using powr_gt_zero[of 2 "real b", arith]
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   192
  by (simp add: float_def zero_le_mult_iff)
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   193
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   194
lemma float_le_zero:
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   195
  "(float (a,b) <= 0) = (a <= 0)"
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   196
  using powr_gt_zero[of 2 "real b", arith]
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   197
  by (simp add: float_def mult_le_0_iff)
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   198
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   199
lemma float_abs:
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   200
  "abs (float (a,b)) = (if 0 <= a then (float (a,b)) else (float (-a,b)))"
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   201
  using powr_gt_zero[of 2 "real b", arith]
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   202
  by (simp add: float_def abs_if mult_less_0_iff)
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   203
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   204
lemma float_zero:
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   205
  "float (0, b) = 0"
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   206
  by (simp add: float_def)
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   207
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   208
lemma float_pprt:
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   209
  "pprt (float (a, b)) = (if 0 <= a then (float (a,b)) else (float (0, b)))"
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   210
  by (auto simp add: zero_le_float float_le_zero float_zero)
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   211
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   212
lemma float_nprt:
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   213
  "nprt (float (a, b)) = (if 0 <= a then (float (0,b)) else (float (a, b)))"
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   214
  by (auto simp add: zero_le_float float_le_zero float_zero)
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   215
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   216
definition lbound :: "real \<Rightarrow> real"
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   217
  where "lbound x = min 0 x"
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   218
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   219
definition ubound :: "real \<Rightarrow> real"
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   220
  where "ubound x = max 0 x"
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   221
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   222
lemma lbound: "lbound x \<le> x"   
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   223
  by (simp add: lbound_def)
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   224
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   225
lemma ubound: "x \<le> ubound x"
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   226
  by (simp add: ubound_def)
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   227
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   228
lemma pprt_lbound: "pprt (lbound x) = float (0, 0)"
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   229
  by (auto simp: float_def lbound_def)
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   230
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   231
lemma nprt_ubound: "nprt (ubound x) = float (0, 0)"
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   232
  by (auto simp: float_def ubound_def)
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   233
24301
6c7f226b24c3 changed floatarith lemmas
obua
parents: 24124
diff changeset
   234
lemmas floatarith[simplified norm_0_1] = float_add float_add_l0 float_add_r0 float_mult float_mult_l0 float_mult_r0 
24653
3d3ebc0c927c changed lemmas
obua
parents: 24301
diff changeset
   235
          float_minus float_abs zero_le_float float_pprt float_nprt pprt_lbound nprt_ubound
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   236
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   237
(* for use with the compute oracle *)
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46988
diff changeset
   238
lemmas arith = arith_simps rel_simps diff_nat_numeral nat_0
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46988
diff changeset
   239
  nat_neg_numeral powerarith floatarith not_false_eq_true not_true_eq_false
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   240
28952
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 27366
diff changeset
   241
use "~~/src/HOL/Tools/float_arith.ML"
20771
89bec28a03c8 proper use of float.ML;
wenzelm
parents: 20717
diff changeset
   242
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   243
end