author | kleing |
Sun, 19 Feb 2006 13:21:32 +0100 | |
changeset 19106 | 6e6b5b1fdc06 |
parent 15149 | c5c4884634b7 |
child 23477 | f4b83f03cac9 |
permissions | -rw-r--r-- |
14051 | 1 |
(* Title: HOL/Complex/ex/BinEx.thy |
13966
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
2 |
ID: $Id$ |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
4 |
Copyright 1999 University of Cambridge |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
5 |
*) |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
6 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
7 |
header {* Binary arithmetic examples *} |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
8 |
|
15149 | 9 |
theory BinEx |
10 |
imports Complex_Main |
|
11 |
begin |
|
13966
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
12 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
13 |
text {* |
14051 | 14 |
Examples of performing binary arithmetic by simplification. This time |
13966
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
15 |
we use the reals, though the representation is just of integers. |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
16 |
*} |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
17 |
|
14051 | 18 |
subsection{*Real Arithmetic*} |
19 |
||
20 |
subsubsection {*Addition *} |
|
13966
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
21 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
22 |
lemma "(1359::real) + -2468 = -1109" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
23 |
by simp |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
24 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
25 |
lemma "(93746::real) + -46375 = 47371" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
26 |
by simp |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
27 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
28 |
|
14051 | 29 |
subsubsection {*Negation *} |
13966
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
30 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
31 |
lemma "- (65745::real) = -65745" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
32 |
by simp |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
33 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
34 |
lemma "- (-54321::real) = 54321" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
35 |
by simp |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
36 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
37 |
|
14051 | 38 |
subsubsection {*Multiplication *} |
13966
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
39 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
40 |
lemma "(-84::real) * 51 = -4284" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
41 |
by simp |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
42 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
43 |
lemma "(255::real) * 255 = 65025" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
44 |
by simp |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
45 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
46 |
lemma "(1359::real) * -2468 = -3354012" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
47 |
by simp |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
48 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
49 |
|
14051 | 50 |
subsubsection {*Inequalities *} |
13966
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
51 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
52 |
lemma "(89::real) * 10 \<noteq> 889" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
53 |
by simp |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
54 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
55 |
lemma "(13::real) < 18 - 4" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
56 |
by simp |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
57 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
58 |
lemma "(-345::real) < -242 + -100" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
59 |
by simp |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
60 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
61 |
lemma "(13557456::real) < 18678654" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
62 |
by simp |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
63 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
64 |
lemma "(999999::real) \<le> (1000001 + 1) - 2" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
65 |
by simp |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
66 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
67 |
lemma "(1234567::real) \<le> 1234567" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
68 |
by simp |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
69 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
70 |
|
14051 | 71 |
subsubsection {*Powers *} |
13966
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
72 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
73 |
lemma "2 ^ 15 = (32768::real)" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
74 |
by simp |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
75 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
76 |
lemma "-3 ^ 7 = (-2187::real)" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
77 |
by simp |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
78 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
79 |
lemma "13 ^ 7 = (62748517::real)" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
80 |
by simp |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
81 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
82 |
lemma "3 ^ 15 = (14348907::real)" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
83 |
by simp |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
84 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
85 |
lemma "-5 ^ 11 = (-48828125::real)" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
86 |
by simp |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
87 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
88 |
|
14051 | 89 |
subsubsection {*Tests *} |
13966
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
90 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
91 |
lemma "(x + y = x) = (y = (0::real))" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
92 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
93 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
94 |
lemma "(x + y = y) = (x = (0::real))" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
95 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
96 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
97 |
lemma "(x + y = (0::real)) = (x = -y)" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
98 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
99 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
100 |
lemma "(x + y = (0::real)) = (y = -x)" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
101 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
102 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
103 |
lemma "((x + y) < (x + z)) = (y < (z::real))" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
104 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
105 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
106 |
lemma "((x + z) < (y + z)) = (x < (y::real))" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
107 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
108 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
109 |
lemma "(\<not> x < y) = (y \<le> (x::real))" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
110 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
111 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
112 |
lemma "\<not> (x < y \<and> y < (x::real))" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
113 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
114 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
115 |
lemma "(x::real) < y ==> \<not> y < x" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
116 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
117 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
118 |
lemma "((x::real) \<noteq> y) = (x < y \<or> y < x)" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
119 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
120 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
121 |
lemma "(\<not> x \<le> y) = (y < (x::real))" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
122 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
123 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
124 |
lemma "x \<le> y \<or> y \<le> (x::real)" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
125 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
126 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
127 |
lemma "x \<le> y \<or> y < (x::real)" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
128 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
129 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
130 |
lemma "x < y \<or> y \<le> (x::real)" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
131 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
132 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
133 |
lemma "x \<le> (x::real)" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
134 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
135 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
136 |
lemma "((x::real) \<le> y) = (x < y \<or> x = y)" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
137 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
138 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
139 |
lemma "((x::real) \<le> y \<and> y \<le> x) = (x = y)" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
140 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
141 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
142 |
lemma "\<not>(x < y \<and> y \<le> (x::real))" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
143 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
144 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
145 |
lemma "\<not>(x \<le> y \<and> y < (x::real))" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
146 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
147 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
148 |
lemma "(-x < (0::real)) = (0 < x)" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
149 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
150 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
151 |
lemma "((0::real) < -x) = (x < 0)" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
152 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
153 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
154 |
lemma "(-x \<le> (0::real)) = (0 \<le> x)" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
155 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
156 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
157 |
lemma "((0::real) \<le> -x) = (x \<le> 0)" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
158 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
159 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
160 |
lemma "(x::real) = y \<or> x < y \<or> y < x" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
161 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
162 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
163 |
lemma "(x::real) = 0 \<or> 0 < x \<or> 0 < -x" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
164 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
165 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
166 |
lemma "(0::real) \<le> x \<or> 0 \<le> -x" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
167 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
168 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
169 |
lemma "((x::real) + y \<le> x + z) = (y \<le> z)" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
170 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
171 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
172 |
lemma "((x::real) + z \<le> y + z) = (x \<le> y)" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
173 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
174 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
175 |
lemma "(w::real) < x \<and> y < z ==> w + y < x + z" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
176 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
177 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
178 |
lemma "(w::real) \<le> x \<and> y \<le> z ==> w + y \<le> x + z" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
179 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
180 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
181 |
lemma "(0::real) \<le> x \<and> 0 \<le> y ==> 0 \<le> x + y" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
182 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
183 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
184 |
lemma "(0::real) < x \<and> 0 < y ==> 0 < x + y" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
185 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
186 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
187 |
lemma "(-x < y) = (0 < x + (y::real))" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
188 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
189 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
190 |
lemma "(x < -y) = (x + y < (0::real))" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
191 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
192 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
193 |
lemma "(y < x + -z) = (y + z < (x::real))" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
194 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
195 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
196 |
lemma "(x + -y < z) = (x < z + (y::real))" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
197 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
198 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
199 |
lemma "x \<le> y ==> x < y + (1::real)" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
200 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
201 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
202 |
lemma "(x - y) + y = (x::real)" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
203 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
204 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
205 |
lemma "y + (x - y) = (x::real)" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
206 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
207 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
208 |
lemma "x - x = (0::real)" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
209 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
210 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
211 |
lemma "(x - y = 0) = (x = (y::real))" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
212 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
213 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
214 |
lemma "((0::real) \<le> x + x) = (0 \<le> x)" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
215 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
216 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
217 |
lemma "(-x \<le> x) = ((0::real) \<le> x)" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
218 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
219 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
220 |
lemma "(x \<le> -x) = (x \<le> (0::real))" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
221 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
222 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
223 |
lemma "(-x = (0::real)) = (x = 0)" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
224 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
225 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
226 |
lemma "-(x - y) = y - (x::real)" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
227 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
228 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
229 |
lemma "((0::real) < x - y) = (y < x)" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
230 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
231 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
232 |
lemma "((0::real) \<le> x - y) = (y \<le> x)" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
233 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
234 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
235 |
lemma "(x + y) - x = (y::real)" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
236 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
237 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
238 |
lemma "(-x = y) = (x = (-y::real))" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
239 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
240 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
241 |
lemma "x < (y::real) ==> \<not>(x = y)" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
242 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
243 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
244 |
lemma "(x \<le> x + y) = ((0::real) \<le> y)" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
245 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
246 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
247 |
lemma "(y \<le> x + y) = ((0::real) \<le> x)" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
248 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
249 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
250 |
lemma "(x < x + y) = ((0::real) < y)" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
251 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
252 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
253 |
lemma "(y < x + y) = ((0::real) < x)" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
254 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
255 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
256 |
lemma "(x - y) - x = (-y::real)" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
257 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
258 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
259 |
lemma "(x + y < z) = (x < z - (y::real))" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
260 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
261 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
262 |
lemma "(x - y < z) = (x < z + (y::real))" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
263 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
264 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
265 |
lemma "(x < y - z) = (x + z < (y::real))" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
266 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
267 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
268 |
lemma "(x \<le> y - z) = (x + z \<le> (y::real))" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
269 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
270 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
271 |
lemma "(x - y \<le> z) = (x \<le> z + (y::real))" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
272 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
273 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
274 |
lemma "(-x < -y) = (y < (x::real))" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
275 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
276 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
277 |
lemma "(-x \<le> -y) = (y \<le> (x::real))" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
278 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
279 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
280 |
lemma "(a + b) - (c + d) = (a - c) + (b - (d::real))" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
281 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
282 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
283 |
lemma "(0::real) - x = -x" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
284 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
285 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
286 |
lemma "x - (0::real) = x" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
287 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
288 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
289 |
lemma "w \<le> x \<and> y < z ==> w + y < x + (z::real)" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
290 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
291 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
292 |
lemma "w < x \<and> y \<le> z ==> w + y < x + (z::real)" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
293 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
294 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
295 |
lemma "(0::real) \<le> x \<and> 0 < y ==> 0 < x + (y::real)" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
296 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
297 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
298 |
lemma "(0::real) < x \<and> 0 \<le> y ==> 0 < x + y" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
299 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
300 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
301 |
lemma "-x - y = -(x + (y::real))" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
302 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
303 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
304 |
lemma "x - (-y) = x + (y::real)" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
305 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
306 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
307 |
lemma "-x - -y = y - (x::real)" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
308 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
309 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
310 |
lemma "(a - b) + (b - c) = a - (c::real)" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
311 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
312 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
313 |
lemma "(x = y - z) = (x + z = (y::real))" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
314 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
315 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
316 |
lemma "(x - y = z) = (x = z + (y::real))" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
317 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
318 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
319 |
lemma "x - (x - y) = (y::real)" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
320 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
321 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
322 |
lemma "x - (x + y) = -(y::real)" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
323 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
324 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
325 |
lemma "x = y ==> x \<le> (y::real)" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
326 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
327 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
328 |
lemma "(0::real) < x ==> \<not>(x = 0)" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
329 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
330 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
331 |
lemma "(x + y) * (x - y) = (x * x) - (y * y)" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
332 |
oops |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
333 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
334 |
lemma "(-x = -y) = (x = (y::real))" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
335 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
336 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
337 |
lemma "(-x < -y) = (y < (x::real))" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
338 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
339 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
340 |
lemma "!!a::real. a \<le> b ==> c \<le> d ==> x + y < z ==> a + c \<le> b + d" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
341 |
by (tactic "fast_arith_tac 1") |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
342 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
343 |
lemma "!!a::real. a < b ==> c < d ==> a - d \<le> b + (-c)" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
344 |
by (tactic "fast_arith_tac 1") |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
345 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
346 |
lemma "!!a::real. a \<le> b ==> b + b \<le> c ==> a + a \<le> c" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
347 |
by (tactic "fast_arith_tac 1") |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
348 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
349 |
lemma "!!a::real. a + b \<le> i + j ==> a \<le> b ==> i \<le> j ==> a + a \<le> j + j" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
350 |
by (tactic "fast_arith_tac 1") |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
351 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
352 |
lemma "!!a::real. a + b < i + j ==> a < b ==> i < j ==> a + a < j + j" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
353 |
by (tactic "fast_arith_tac 1") |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
354 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
355 |
lemma "!!a::real. a + b + c \<le> i + j + k \<and> a \<le> b \<and> b \<le> c \<and> i \<le> j \<and> j \<le> k --> a + a + a \<le> k + k + k" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
356 |
by arith |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
357 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
358 |
lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
359 |
==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a \<le> l" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
360 |
by (tactic "fast_arith_tac 1") |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
361 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
362 |
lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
363 |
==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a + a + a + a \<le> l + l + l + l" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
364 |
by (tactic "fast_arith_tac 1") |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
365 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
366 |
lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
367 |
==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a + a + a + a + a \<le> l + l + l + l + i" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
368 |
by (tactic "fast_arith_tac 1") |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
369 |
|
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
370 |
lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
371 |
==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a + a + a + a + a + a \<le> l + l + l + l + i + l" |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
372 |
by (tactic "fast_arith_tac 1") |
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
373 |
|
14051 | 374 |
|
375 |
subsection{*Complex Arithmetic*} |
|
376 |
||
377 |
lemma "(1359 + 93746*ii) - (2468 + 46375*ii) = -1109 + 47371*ii" |
|
378 |
by simp |
|
379 |
||
380 |
lemma "- (65745 + -47371*ii) = -65745 + 47371*ii" |
|
381 |
by simp |
|
382 |
||
383 |
text{*Multiplication requires distributive laws. Perhaps versions instantiated |
|
384 |
to literal constants should be added to the simpset.*} |
|
385 |
||
14373 | 386 |
lemmas distrib = left_distrib right_distrib left_diff_distrib right_diff_distrib |
14051 | 387 |
|
388 |
lemma "(1 + ii) * (1 - ii) = 2" |
|
389 |
by (simp add: distrib) |
|
390 |
||
391 |
lemma "(1 + 2*ii) * (1 + 3*ii) = -5 + 5*ii" |
|
392 |
by (simp add: distrib) |
|
393 |
||
394 |
lemma "(-84 + 255*ii) + (51 * 255*ii) = -84 + 13260 * ii" |
|
395 |
by (simp add: distrib) |
|
396 |
||
14373 | 397 |
text{*No inequalities or linear arithmetic: the complex numbers are unordered!*} |
14051 | 398 |
|
399 |
text{*No powers (not supported yet)*} |
|
400 |
||
13966
2160abf7cfe7
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents:
diff
changeset
|
401 |
end |