src/HOL/Matrix_LP/ComputeFloat.thy
author wenzelm
Wed, 26 Oct 2016 15:14:17 +0200
changeset 64406 492de9062cd2
parent 63901 4ce989e962e0
child 65583 8d53b3bebab4
permissions -rw-r--r--
more specific hardware information: relevant for ultimate Mac OS X version;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
47455
26315a545e26 updated headers;
wenzelm
parents: 47108
diff changeset
     1
(*  Title:      HOL/Matrix_LP/ComputeFloat.thy
41959
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
63167
0909deb8059b isabelle update_cartouches -c -t;
wenzelm
parents: 62348
diff changeset
     5
section \<open>Floating Point Representation of the Reals\<close>
20717
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"
20485
3078fd2eec7b got rid of Numeral.bin type
haftmann
parents: 20217
diff changeset
     9
begin
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    10
48891
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47455
diff changeset
    11
ML_file "~~/src/Tools/float.ML"
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 47455
diff changeset
    12
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 60017
diff changeset
    13
(*FIXME surely floor should be used? This file is full of redundant material.*)
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 60017
diff changeset
    14
38273
d31a34569542 modernized some specifications;
wenzelm
parents: 35032
diff changeset
    15
definition int_of_real :: "real \<Rightarrow> int"
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 60017
diff changeset
    16
  where "int_of_real x = (SOME y. real_of_int y = x)"
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21256
diff changeset
    17
38273
d31a34569542 modernized some specifications;
wenzelm
parents: 35032
diff changeset
    18
definition real_is_int :: "real \<Rightarrow> bool"
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 60017
diff changeset
    19
  where "real_is_int x = (EX (u::int). x = real_of_int u)"
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    20
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 60017
diff changeset
    21
lemma real_is_int_def2: "real_is_int x = (x = real_of_int (int_of_real x))"
45495
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
    22
  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
    23
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 60017
diff changeset
    24
lemma real_is_int_real[simp]: "real_is_int (real_of_int (x::int))"
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    25
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
    26
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 60017
diff changeset
    27
lemma int_of_real_real[simp]: "int_of_real (real_of_int x) = x"
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    28
by (simp add: int_of_real_def)
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    29
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 60017
diff changeset
    30
lemma real_int_of_real[simp]: "real_is_int x \<Longrightarrow> real_of_int (int_of_real x) = x"
16782
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_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
    34
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
    35
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    36
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
    37
apply (subst real_is_int_def2)
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    38
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
    39
done
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 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
    42
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
    43
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    44
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
    45
apply (subst real_is_int_def2)
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    46
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
    47
done
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    48
63901
4ce989e962e0 more symbols;
wenzelm
parents: 63167
diff changeset
    49
lemma real_is_int_rep: "real_is_int x \<Longrightarrow> \<exists>!(a::int). real_of_int a = x"
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    50
by (auto simp add: real_is_int_def)
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    51
19765
dfe940911617 misc cleanup;
wenzelm
parents: 16890
diff changeset
    52
lemma int_of_real_mult:
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    53
  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
    54
  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
    55
  using assms
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 60017
diff changeset
    56
  by (auto simp add: real_is_int_def of_int_mult[symmetric]
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 60017
diff changeset
    57
           simp del: of_int_mult)
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    58
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    59
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
    60
apply (subst real_is_int_def2)
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    61
apply (simp add: int_of_real_mult)
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    62
done
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_0[simp]: "real_is_int (0::real)"
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    65
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
    66
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    67
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
    68
proof -
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 60017
diff changeset
    69
  have "real_is_int (1::real) = real_is_int(real_of_int (1::int))" by auto
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    70
  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
    71
  ultimately show ?thesis by auto
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    72
qed
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    73
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    74
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
    75
proof -
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 60017
diff changeset
    76
  have "real_is_int (-1::real) = real_is_int(real_of_int (-1::int))" by auto
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    77
  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
    78
  ultimately show ?thesis by auto
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    79
qed
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    80
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46988
diff changeset
    81
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
    82
  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
    83
54489
03ff4d1e6784 eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents: 48891
diff changeset
    84
lemma real_is_int_neg_numeral[simp]: "real_is_int (- numeral x)"
03ff4d1e6784 eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents: 48891
diff changeset
    85
  by (auto simp: real_is_int_def intro!: exI[of _ "- numeral x"])
16782
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_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
    88
by (simp add: int_of_real_def)
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    89
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    90
lemma int_of_real_1[simp]: "int_of_real (1::real) = (1::int)"
19765
dfe940911617 misc cleanup;
wenzelm
parents: 16890
diff changeset
    91
proof -
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 60017
diff changeset
    92
  have 1: "(1::real) = real_of_int (1::int)" by auto
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    93
  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
    94
qed
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
    95
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46988
diff changeset
    96
lemma int_of_real_numeral[simp]: "int_of_real (numeral b) = numeral b"
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 60017
diff changeset
    97
  unfolding int_of_real_def by simp
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46988
diff changeset
    98
54489
03ff4d1e6784 eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents: 48891
diff changeset
    99
lemma int_of_real_neg_numeral[simp]: "int_of_real (- numeral b) = - numeral b"
45495
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   100
  unfolding int_of_real_def
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 60017
diff changeset
   101
  by (metis int_of_real_def int_of_real_real of_int_minus of_int_of_nat_eq of_nat_numeral) 
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
61945
1135b8de26c3 more symbols;
wenzelm
parents: 61609
diff changeset
   109
lemma abs_div_2_less: "a \<noteq> 0 \<Longrightarrow> a \<noteq> -1 \<Longrightarrow> \<bar>(a::int) div 2\<bar> < \<bar>a\<bar>"
16782
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
62348
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 61945
diff changeset
   158
lemmas powerarith = nat_numeral power_numeral_even
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 61945
diff changeset
   159
  power_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
61609
77b453bd616f Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents: 60017
diff changeset
   162
  "float = (\<lambda>(a, b). real_of_int a * 2 powr real_of_int b)"
45495
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)"
60017
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 58889
diff changeset
   191
  by (simp add: float_def zero_le_mult_iff) (simp add: not_less [symmetric])
45495
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   192
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   193
lemma float_le_zero:
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   194
  "(float (a,b) <= 0) = (a <= 0)"
60017
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 58889
diff changeset
   195
  by (simp add: float_def mult_le_0_iff) (simp add: not_less [symmetric])
45495
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   196
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   197
lemma float_abs:
61945
1135b8de26c3 more symbols;
wenzelm
parents: 61609
diff changeset
   198
  "\<bar>float (a,b)\<bar> = (if 0 <= a then (float (a,b)) else (float (-a,b)))"
60017
b785d6d06430 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
paulson <lp15@cam.ac.uk>
parents: 58889
diff changeset
   199
  by (simp add: float_def abs_if mult_less_0_iff not_less)
45495
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   200
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   201
lemma float_zero:
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   202
  "float (0, b) = 0"
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   203
  by (simp add: float_def)
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   204
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   205
lemma float_pprt:
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   206
  "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
   207
  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
   208
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   209
lemma float_nprt:
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   210
  "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
   211
  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
   212
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   213
definition lbound :: "real \<Rightarrow> real"
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   214
  where "lbound x = min 0 x"
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 ubound :: "real \<Rightarrow> real"
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   217
  where "ubound x = max 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
lemma lbound: "lbound x \<le> x"   
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   220
  by (simp add: lbound_def)
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 ubound: "x \<le> ubound x"
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   223
  by (simp add: ubound_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 pprt_lbound: "pprt (lbound x) = float (0, 0)"
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   226
  by (auto simp: float_def lbound_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 nprt_ubound: "nprt (ubound 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 ubound_def)
c55a07526dbe cleaned up float theories; removed duplicate definitions and theorems
hoelzl
parents: 42676
diff changeset
   230
24301
6c7f226b24c3 changed floatarith lemmas
obua
parents: 24124
diff changeset
   231
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
   232
          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
   233
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   234
(* for use with the compute oracle *)
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46988
diff changeset
   235
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
   236
  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
   237
56255
968667bbb8d2 more antiquotations;
wenzelm
parents: 54489
diff changeset
   238
ML_file "float_arith.ML"
20771
89bec28a03c8 proper use of float.ML;
wenzelm
parents: 20717
diff changeset
   239
16782
b214f21ae396 - use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff changeset
   240
end