author | wenzelm |
Wed, 26 Oct 2016 15:14:17 +0200 | |
changeset 64406 | 492de9062cd2 |
parent 63901 | 4ce989e962e0 |
child 65583 | 8d53b3bebab4 |
permissions | -rw-r--r-- |
47455 | 1 |
(* Title: HOL/Matrix_LP/ComputeFloat.thy |
41959 | 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 | 5 |
section \<open>Floating Point Representation of the Reals\<close> |
20717 | 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 | 9 |
begin |
16782
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
10 |
|
48891 | 11 |
ML_file "~~/src/Tools/float.ML" |
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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 158 |
lemmas powerarith = nat_numeral power_numeral_even |
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 | 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 | 231 |
lemmas floatarith[simplified norm_0_1] = float_add float_add_l0 float_add_r0 float_mult float_mult_l0 float_mult_r0 |
24653 | 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 | 238 |
ML_file "float_arith.ML" |
20771 | 239 |
|
16782
b214f21ae396
- use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset
|
240 |
end |