author | paulson |
Tue, 27 Jan 2004 15:39:51 +0100 | |
changeset 14365 | 3d4df8c166ae |
parent 14352 | a8b1a44d8264 |
child 14369 | c50188fe6366 |
permissions | -rw-r--r-- |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
1 |
(* Title: HOL/RealArith.thy |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
2 |
ID: $Id$ |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
4 |
Copyright 1999 University of Cambridge |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
5 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
6 |
Binary arithmetic and simplification for the reals |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
7 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
8 |
This case is reduced to that for the integers |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
9 |
*) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
10 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
11 |
theory RealArith = RealDef |
14275
031a5a051bb4
Converting more of the "real" development to Isar scripts
paulson
parents:
14270
diff
changeset
|
12 |
files ("real_arith.ML"): |
031a5a051bb4
Converting more of the "real" development to Isar scripts
paulson
parents:
14270
diff
changeset
|
13 |
|
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
14 |
instance real :: number .. |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
15 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
16 |
defs |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
17 |
real_number_of_def: |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
18 |
"number_of v == real (number_of v :: int)" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
19 |
(*::bin=>real ::bin=>int*) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
20 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
21 |
text{*Collapse applications of @{term real} to @{term number_of}*} |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
22 |
declare real_number_of_def [symmetric, simp] |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
23 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
24 |
lemma real_numeral_0_eq_0: "Numeral0 = (0::real)" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
25 |
by (simp add: real_number_of_def) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
26 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
27 |
lemma real_numeral_1_eq_1: "Numeral1 = (1::real)" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
28 |
apply (unfold real_number_of_def) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
29 |
apply (subst real_of_one [symmetric], simp) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
30 |
done |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
31 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
32 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
33 |
subsection{*Arithmetic Operations On Numerals*} |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
34 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
35 |
lemma add_real_number_of [simp]: |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
36 |
"(number_of v :: real) + number_of v' = number_of (bin_add v v')" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
37 |
by (simp only: real_number_of_def real_of_int_add number_of_add) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
38 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
39 |
lemma minus_real_number_of [simp]: |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
40 |
"- (number_of w :: real) = number_of (bin_minus w)" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
41 |
by (simp only: real_number_of_def number_of_minus real_of_int_minus) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
42 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
43 |
lemma diff_real_number_of [simp]: |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
44 |
"(number_of v :: real) - number_of w = number_of (bin_add v (bin_minus w))" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
45 |
by (simp only: real_number_of_def diff_number_of_eq real_of_int_diff) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
46 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
47 |
lemma mult_real_number_of [simp]: |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
48 |
"(number_of v :: real) * number_of v' = number_of (bin_mult v v')" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
49 |
by (simp only: real_number_of_def real_of_int_mult number_of_mult) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
50 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
51 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
52 |
text{*Lemmas for specialist use, NOT as default simprules*} |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
53 |
lemma real_mult_2: "2 * z = (z+z::real)" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
54 |
proof - |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
55 |
have eq: "(2::real) = 1 + 1" by (simp add: real_numeral_1_eq_1 [symmetric]) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
56 |
thus ?thesis by (simp add: eq left_distrib) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
57 |
qed |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
58 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
59 |
lemma real_mult_2_right: "z * 2 = (z+z::real)" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
60 |
by (subst mult_commute, rule real_mult_2) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
61 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
62 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
63 |
subsection{*Comparisons On Numerals*} |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
64 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
65 |
lemma eq_real_number_of [simp]: |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
66 |
"((number_of v :: real) = number_of v') = |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
67 |
iszero (number_of (bin_add v (bin_minus v')))" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
68 |
by (simp only: real_number_of_def real_of_int_inject eq_number_of_eq) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
69 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
70 |
text{*@{term neg} is used in rewrite rules for binary comparisons*} |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
71 |
lemma less_real_number_of [simp]: |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
72 |
"((number_of v :: real) < number_of v') = |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
73 |
neg (number_of (bin_add v (bin_minus v')))" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
74 |
by (simp only: real_number_of_def real_of_int_less_iff less_number_of_eq_neg) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
75 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
76 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
77 |
text{*New versions of existing theorems involving 0, 1*} |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
78 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
79 |
lemma real_minus_1_eq_m1 [simp]: "- 1 = (-1::real)" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
80 |
by (simp add: real_numeral_1_eq_1 [symmetric]) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
81 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
82 |
lemma real_mult_minus1 [simp]: "-1 * z = -(z::real)" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
83 |
proof - |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
84 |
have "-1 * z = (- 1) * z" by (simp add: real_minus_1_eq_m1) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
85 |
also have "... = - (1 * z)" by (simp only: minus_mult_left) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
86 |
also have "... = -z" by simp |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
87 |
finally show ?thesis . |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
88 |
qed |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
89 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
90 |
lemma real_mult_minus1_right [simp]: "z * -1 = -(z::real)" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
91 |
by (subst mult_commute, rule real_mult_minus1) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
92 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
93 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
94 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
95 |
(** real from type "nat" **) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
96 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
97 |
lemma zero_less_real_of_nat_iff [iff]: "(0 < real (n::nat)) = (0<n)" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
98 |
by (simp only: real_of_nat_less_iff real_of_nat_zero [symmetric]) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
99 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
100 |
lemma zero_le_real_of_nat_iff [iff]: "(0 <= real (n::nat)) = (0<=n)" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
101 |
by (simp only: real_of_nat_le_iff real_of_nat_zero [symmetric]) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
102 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
103 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
104 |
(*Like the ones above, for "equals"*) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
105 |
declare real_of_nat_zero_iff [iff] |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
106 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
107 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
108 |
subsection{*Simplification of Arithmetic when Nested to the Right*} |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
109 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
110 |
lemma real_add_number_of_left [simp]: |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
111 |
"number_of v + (number_of w + z) = (number_of(bin_add v w) + z::real)" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
112 |
by (simp add: add_assoc [symmetric]) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
113 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
114 |
lemma real_mult_number_of_left [simp]: |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
115 |
"number_of v * (number_of w * z) = (number_of(bin_mult v w) * z::real)" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
116 |
apply (simp (no_asm) add: mult_assoc [symmetric]) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
117 |
done |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
118 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
119 |
lemma real_add_number_of_diff1 [simp]: |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
120 |
"number_of v + (number_of w - c) = number_of(bin_add v w) - (c::real)" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
121 |
apply (unfold real_diff_def) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
122 |
apply (rule real_add_number_of_left) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
123 |
done |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
124 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
125 |
lemma real_add_number_of_diff2 [simp]: |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
126 |
"number_of v + (c - number_of w) = |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
127 |
number_of (bin_add v (bin_minus w)) + (c::real)" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
128 |
apply (subst diff_real_number_of [symmetric]) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
129 |
apply (simp only: real_diff_def add_ac) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
130 |
done |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
131 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
132 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
133 |
text{*The constant @{term neg} is used in rewrite rules for binary |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
134 |
comparisons. A complication in this proof is that both @{term real} and @{term |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
135 |
number_of} are polymorphic, so that it's difficult to know what types subterms |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
136 |
have. *} |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
137 |
lemma real_of_nat_number_of [simp]: |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
138 |
"real (number_of v :: nat) = |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
139 |
(if neg (number_of v) then 0 |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
140 |
else (number_of v :: real))" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
141 |
proof cases |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
142 |
assume "neg (number_of v)" thus ?thesis by simp |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
143 |
next |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
144 |
assume neg: "~ neg (number_of v)" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
145 |
thus ?thesis |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
146 |
by (simp only: nat_number_of_def real_of_nat_real_of_int [OF neg], simp) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
147 |
qed |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
148 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
149 |
declare real_numeral_0_eq_0 [simp] real_numeral_1_eq_1 [simp] |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
150 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
151 |
(*Simplification of x-y < 0, etc.*) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
152 |
declare less_iff_diff_less_0 [symmetric, iff] |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
153 |
declare eq_iff_diff_eq_0 [symmetric, iff] |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
154 |
declare le_iff_diff_le_0 [symmetric, iff] |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
155 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
156 |
|
14275
031a5a051bb4
Converting more of the "real" development to Isar scripts
paulson
parents:
14270
diff
changeset
|
157 |
use "real_arith.ML" |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
158 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
159 |
setup real_arith_setup |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
160 |
|
14288 | 161 |
subsection{* Simprules combining x+y and 0: ARE THEY NEEDED?*} |
162 |
||
163 |
text{*Needed in this non-standard form by Hyperreal/Transcendental*} |
|
164 |
lemma real_0_le_divide_iff: |
|
14294
f4d806fd72ce
absolute value theorems moved to HOL/Ring_and_Field
paulson
parents:
14293
diff
changeset
|
165 |
"((0::real) \<le> x/y) = ((x \<le> 0 | 0 \<le> y) & (0 \<le> x | y \<le> 0))" |
14288 | 166 |
by (simp add: real_divide_def zero_le_mult_iff, auto) |
167 |
||
168 |
lemma real_add_minus_iff [simp]: "(x + - a = (0::real)) = (x=a)" |
|
169 |
by arith |
|
170 |
||
171 |
lemma real_add_eq_0_iff [iff]: "(x+y = (0::real)) = (y = -x)" |
|
172 |
by auto |
|
173 |
||
174 |
lemma real_add_less_0_iff [iff]: "(x+y < (0::real)) = (y < -x)" |
|
175 |
by auto |
|
176 |
||
177 |
lemma real_0_less_add_iff [iff]: "((0::real) < x+y) = (-x < y)" |
|
178 |
by auto |
|
179 |
||
180 |
lemma real_add_le_0_iff [iff]: "(x+y \<le> (0::real)) = (y \<le> -x)" |
|
181 |
by auto |
|
182 |
||
183 |
lemma real_0_le_add_iff [iff]: "((0::real) \<le> x+y) = (-x \<le> y)" |
|
184 |
by auto |
|
185 |
||
186 |
||
14329 | 187 |
(** Simprules combining x-y and 0 (needed??) **) |
14288 | 188 |
|
189 |
lemma real_0_less_diff_iff [iff]: "((0::real) < x-y) = (y < x)" |
|
190 |
by auto |
|
191 |
||
192 |
lemma real_0_le_diff_iff [iff]: "((0::real) \<le> x-y) = (y \<le> x)" |
|
193 |
by auto |
|
194 |
||
195 |
(* |
|
196 |
FIXME: we should have this, as for type int, but many proofs would break. |
|
197 |
It replaces x+-y by x-y. |
|
198 |
Addsimps [symmetric real_diff_def] |
|
199 |
*) |
|
200 |
||
14321 | 201 |
subsubsection{*Division By @{term "-1"}*} |
14288 | 202 |
|
203 |
lemma real_divide_minus1 [simp]: "x/-1 = -(x::real)" |
|
204 |
by simp |
|
205 |
||
206 |
lemma real_minus1_divide [simp]: "-1/(x::real) = - (1/x)" |
|
14334 | 207 |
by (simp add: real_divide_def inverse_minus_eq) |
14288 | 208 |
|
209 |
lemma real_lbound_gt_zero: |
|
210 |
"[| (0::real) < d1; 0 < d2 |] ==> \<exists>e. 0 < e & e < d1 & e < d2" |
|
211 |
apply (rule_tac x = " (min d1 d2) /2" in exI) |
|
212 |
apply (simp add: min_def) |
|
213 |
done |
|
214 |
||
215 |
(*** Density of the Reals ***) |
|
216 |
||
14293 | 217 |
text{*Similar results are proved in @{text Ring_and_Field}*} |
14288 | 218 |
lemma real_less_half_sum: "x < y ==> x < (x+y) / (2::real)" |
14293 | 219 |
by auto |
14288 | 220 |
|
221 |
lemma real_gt_half_sum: "x < y ==> (x+y)/(2::real) < y" |
|
14293 | 222 |
by auto |
14288 | 223 |
|
224 |
lemma real_dense: "x < y ==> \<exists>r::real. x < r & r < y" |
|
14293 | 225 |
by (rule Ring_and_Field.dense) |
226 |
||
14288 | 227 |
|
14269 | 228 |
subsection{*Absolute Value Function for the Reals*} |
229 |
||
14295 | 230 |
lemma abs_nat_number_of [simp]: |
14269 | 231 |
"abs (number_of v :: real) = |
232 |
(if neg (number_of v) then number_of (bin_minus v) |
|
233 |
else number_of v)" |
|
14295 | 234 |
by (simp add: real_abs_def bin_arith_simps minus_real_number_of |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
235 |
less_real_number_of real_of_int_le_iff) |
14269 | 236 |
|
14294
f4d806fd72ce
absolute value theorems moved to HOL/Ring_and_Field
paulson
parents:
14293
diff
changeset
|
237 |
text{*FIXME: these should go!*} |
f4d806fd72ce
absolute value theorems moved to HOL/Ring_and_Field
paulson
parents:
14293
diff
changeset
|
238 |
lemma abs_eqI1: "(0::real)\<le>x ==> abs x = x" |
14269 | 239 |
by (unfold real_abs_def, simp) |
240 |
||
241 |
lemma abs_eqI2: "(0::real) < x ==> abs x = x" |
|
242 |
by (unfold real_abs_def, simp) |
|
243 |
||
244 |
lemma abs_minus_eqI2: "x < (0::real) ==> abs x = -x" |
|
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14352
diff
changeset
|
245 |
by (simp add: real_abs_def linorder_not_less [symmetric]) |
14269 | 246 |
|
247 |
lemma abs_minus_add_cancel: "abs(x + (-y)) = abs (y + (-(x::real)))" |
|
248 |
by (unfold real_abs_def, simp) |
|
249 |
||
14294
f4d806fd72ce
absolute value theorems moved to HOL/Ring_and_Field
paulson
parents:
14293
diff
changeset
|
250 |
lemma abs_minus_one [simp]: "abs (-1) = (1::real)" |
14269 | 251 |
by (unfold real_abs_def, simp) |
252 |
||
253 |
lemma abs_interval_iff: "(abs x < r) = (-r < x & x < (r::real))" |
|
14295 | 254 |
by (force simp add: Ring_and_Field.abs_less_iff) |
14269 | 255 |
|
14294
f4d806fd72ce
absolute value theorems moved to HOL/Ring_and_Field
paulson
parents:
14293
diff
changeset
|
256 |
lemma abs_le_interval_iff: "(abs x \<le> r) = (-r\<le>x & x\<le>(r::real))" |
14295 | 257 |
by (force simp add: Ring_and_Field.abs_le_iff) |
14269 | 258 |
|
14295 | 259 |
lemma abs_add_one_gt_zero [simp]: "(0::real) < 1 + abs(x)" |
14269 | 260 |
by (unfold real_abs_def, auto) |
261 |
||
14295 | 262 |
lemma abs_real_of_nat_cancel [simp]: "abs (real x) = real (x::nat)" |
263 |
by (auto intro: abs_eqI1 simp add: real_of_nat_ge_zero) |
|
14269 | 264 |
|
14295 | 265 |
lemma abs_add_one_not_less_self [simp]: "~ abs(x) + (1::real) < x" |
14334 | 266 |
apply (simp add: linorder_not_less) |
14269 | 267 |
apply (auto intro: abs_ge_self [THEN order_trans]) |
268 |
done |
|
269 |
||
14295 | 270 |
text{*Used only in Hyperreal/Lim.ML*} |
14294
f4d806fd72ce
absolute value theorems moved to HOL/Ring_and_Field
paulson
parents:
14293
diff
changeset
|
271 |
lemma abs_sum_triangle_ineq: "abs ((x::real) + y + (-l + -m)) \<le> abs(x + -l) + abs(y + -m)" |
14269 | 272 |
apply (simp add: real_add_assoc) |
14334 | 273 |
apply (rule_tac a1 = y in add_left_commute [THEN ssubst]) |
14269 | 274 |
apply (rule real_add_assoc [THEN subst]) |
275 |
apply (rule abs_triangle_ineq) |
|
276 |
done |
|
277 |
||
14288 | 278 |
|
14290 | 279 |
|
14269 | 280 |
ML |
281 |
{* |
|
14288 | 282 |
val real_0_le_divide_iff = thm"real_0_le_divide_iff"; |
283 |
val real_add_minus_iff = thm"real_add_minus_iff"; |
|
284 |
val real_add_eq_0_iff = thm"real_add_eq_0_iff"; |
|
285 |
val real_add_less_0_iff = thm"real_add_less_0_iff"; |
|
286 |
val real_0_less_add_iff = thm"real_0_less_add_iff"; |
|
287 |
val real_add_le_0_iff = thm"real_add_le_0_iff"; |
|
288 |
val real_0_le_add_iff = thm"real_0_le_add_iff"; |
|
289 |
val real_0_less_diff_iff = thm"real_0_less_diff_iff"; |
|
290 |
val real_0_le_diff_iff = thm"real_0_le_diff_iff"; |
|
291 |
val real_divide_minus1 = thm"real_divide_minus1"; |
|
292 |
val real_minus1_divide = thm"real_minus1_divide"; |
|
293 |
val real_lbound_gt_zero = thm"real_lbound_gt_zero"; |
|
294 |
val real_less_half_sum = thm"real_less_half_sum"; |
|
295 |
val real_gt_half_sum = thm"real_gt_half_sum"; |
|
296 |
val real_dense = thm"real_dense"; |
|
297 |
||
14269 | 298 |
val abs_nat_number_of = thm"abs_nat_number_of"; |
299 |
val abs_eqI1 = thm"abs_eqI1"; |
|
300 |
val abs_eqI2 = thm"abs_eqI2"; |
|
301 |
val abs_minus_eqI2 = thm"abs_minus_eqI2"; |
|
302 |
val abs_ge_zero = thm"abs_ge_zero"; |
|
303 |
val abs_idempotent = thm"abs_idempotent"; |
|
304 |
val abs_zero_iff = thm"abs_zero_iff"; |
|
305 |
val abs_ge_self = thm"abs_ge_self"; |
|
306 |
val abs_ge_minus_self = thm"abs_ge_minus_self"; |
|
307 |
val abs_mult = thm"abs_mult"; |
|
308 |
val abs_inverse = thm"abs_inverse"; |
|
309 |
val abs_triangle_ineq = thm"abs_triangle_ineq"; |
|
310 |
val abs_minus_cancel = thm"abs_minus_cancel"; |
|
311 |
val abs_minus_add_cancel = thm"abs_minus_add_cancel"; |
|
312 |
val abs_minus_one = thm"abs_minus_one"; |
|
313 |
val abs_interval_iff = thm"abs_interval_iff"; |
|
314 |
val abs_le_interval_iff = thm"abs_le_interval_iff"; |
|
315 |
val abs_add_one_gt_zero = thm"abs_add_one_gt_zero"; |
|
316 |
val abs_le_zero_iff = thm"abs_le_zero_iff"; |
|
317 |
val abs_real_of_nat_cancel = thm"abs_real_of_nat_cancel"; |
|
318 |
val abs_add_one_not_less_self = thm"abs_add_one_not_less_self"; |
|
319 |
val abs_sum_triangle_ineq = thm"abs_sum_triangle_ineq"; |
|
14294
f4d806fd72ce
absolute value theorems moved to HOL/Ring_and_Field
paulson
parents:
14293
diff
changeset
|
320 |
|
f4d806fd72ce
absolute value theorems moved to HOL/Ring_and_Field
paulson
parents:
14293
diff
changeset
|
321 |
val abs_mult_less = thm"abs_mult_less"; |
14269 | 322 |
*} |
323 |
||
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
324 |
end |