author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 47108  2a1953f0d20d 
child 47455  26315a545e26 
permissions  rwrr 
41959  1 
(* Title: HOL/Matrix/ComputeFloat.thy 
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  5 
header {* Floating Point Representation of the Reals *} 
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  10 
begin 
16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

11 

38273  12 
definition int_of_real :: "real \<Rightarrow> int" 
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  15 
definition real_is_int :: "real \<Rightarrow> bool" 
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 (ab)) = (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 (ab)" 
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  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  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  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  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(e2e1)), e1) else float (a1*2^(nat (e1e2))+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  234 
lemmas floatarith[simplified norm_0_1] = float_add float_add_l0 float_add_r0 float_mult float_mult_l0 float_mult_r0 
24653  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  242 

16782
b214f21ae396
 use TableFun instead of homebrew binary tree in am_interpreter.ML
obua
parents:
diff
changeset

243 
end 