|
1 (* Title: HOL/Integ/Int.ML |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1998 University of Cambridge |
|
5 |
|
6 Type "int" is a linear order |
|
7 *) |
|
8 |
|
9 Goal "(w<z) = neg(w-z)"; |
|
10 by (simp_tac (simpset() addsimps [zless_def]) 1); |
|
11 qed "zless_eq_neg"; |
|
12 |
|
13 Goal "(w=z) = iszero(w-z)"; |
|
14 by (simp_tac (simpset() addsimps [iszero_def, zdiff_eq_eq]) 1); |
|
15 qed "eq_eq_iszero"; |
|
16 |
|
17 Goal "(w<=z) = (~ neg(z-w))"; |
|
18 by (simp_tac (simpset() addsimps [zle_def, zless_def]) 1); |
|
19 qed "zle_eq_not_neg"; |
|
20 |
|
21 (*This list of rewrites simplifies (in)equalities by subtracting the RHS |
|
22 from the LHS, then using the cancellation simproc. Use with zadd_ac.*) |
|
23 val zcompare_0_rls = |
|
24 [zdiff_def, zless_eq_neg, eq_eq_iszero, zle_eq_not_neg]; |
|
25 |
|
26 |
|
27 (*** Monotonicity results ***) |
|
28 |
|
29 Goal "(v+z < w+z) = (v < (w::int))"; |
|
30 by (full_simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1); |
|
31 qed "zadd_right_cancel_zless"; |
|
32 |
|
33 Goal "(z+v < z+w) = (v < (w::int))"; |
|
34 by (full_simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1); |
|
35 qed "zadd_left_cancel_zless"; |
|
36 |
|
37 Addsimps [zadd_right_cancel_zless, zadd_left_cancel_zless]; |
|
38 |
|
39 Goal "(v+z <= w+z) = (v <= (w::int))"; |
|
40 by (full_simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1); |
|
41 qed "zadd_right_cancel_zle"; |
|
42 |
|
43 Goal "(z+v <= z+w) = (v <= (w::int))"; |
|
44 by (full_simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1); |
|
45 qed "zadd_left_cancel_zle"; |
|
46 |
|
47 Addsimps [zadd_right_cancel_zle, zadd_left_cancel_zle]; |
|
48 |
|
49 (*"v<=w ==> v+z <= w+z"*) |
|
50 bind_thm ("zadd_zless_mono1", zadd_right_cancel_zless RS iffD2); |
|
51 |
|
52 (*"v<=w ==> v+z <= w+z"*) |
|
53 bind_thm ("zadd_zle_mono1", zadd_right_cancel_zle RS iffD2); |
|
54 |
|
55 Goal "!!z z'::int. [| w'<=w; z'<=z |] ==> w' + z' <= w + z"; |
|
56 by (etac (zadd_zle_mono1 RS zle_trans) 1); |
|
57 by (Simp_tac 1); |
|
58 qed "zadd_zle_mono"; |
|
59 |
|
60 Goal "!!z z'::int. [| w'<w; z'<=z |] ==> w' + z' < w + z"; |
|
61 by (etac (zadd_zless_mono1 RS zless_zle_trans) 1); |
|
62 by (Simp_tac 1); |
|
63 qed "zadd_zless_mono"; |
|
64 |
|
65 |
|
66 (*** Comparison laws ***) |
|
67 |
|
68 Goal "(- x < - y) = (y < (x::int))"; |
|
69 by (simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1); |
|
70 qed "zminus_zless_zminus"; |
|
71 Addsimps [zminus_zless_zminus]; |
|
72 |
|
73 Goal "(- x <= - y) = (y <= (x::int))"; |
|
74 by (simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1); |
|
75 qed "zminus_zle_zminus"; |
|
76 Addsimps [zminus_zle_zminus]; |
|
77 |
|
78 (** The next several equations can make the simplifier loop! **) |
|
79 |
|
80 Goal "(x < - y) = (y < - (x::int))"; |
|
81 by (simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1); |
|
82 qed "zless_zminus"; |
|
83 |
|
84 Goal "(- x < y) = (- y < (x::int))"; |
|
85 by (simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1); |
|
86 qed "zminus_zless"; |
|
87 |
|
88 Goal "(x <= - y) = (y <= - (x::int))"; |
|
89 by (simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1); |
|
90 qed "zle_zminus"; |
|
91 |
|
92 Goal "(- x <= y) = (- y <= (x::int))"; |
|
93 by (simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1); |
|
94 qed "zminus_zle"; |
|
95 |
|
96 Goal "- $# Suc n < $# 0"; |
|
97 by (simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1); |
|
98 qed "negative_zless_0"; |
|
99 |
|
100 Goal "- $# Suc n < $# m"; |
|
101 by (rtac (negative_zless_0 RS zless_zle_trans) 1); |
|
102 by (Simp_tac 1); |
|
103 qed "negative_zless"; |
|
104 AddIffs [negative_zless]; |
|
105 |
|
106 Goal "- $# n <= $#0"; |
|
107 by (simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1); |
|
108 qed "negative_zle_0"; |
|
109 |
|
110 Goal "- $# n <= $# m"; |
|
111 by (simp_tac (simpset() addsimps add_nat :: zcompare_0_rls @ zadd_ac) 1); |
|
112 qed "negative_zle"; |
|
113 AddIffs [negative_zle]; |
|
114 |
|
115 Goal "~($# 0 <= - $# Suc n)"; |
|
116 by (stac zle_zminus 1); |
|
117 by (Simp_tac 1); |
|
118 qed "not_zle_0_negative"; |
|
119 Addsimps [not_zle_0_negative]; |
|
120 |
|
121 Goal "($# n <= - $# m) = (n = 0 & m = 0)"; |
|
122 by Safe_tac; |
|
123 by (Simp_tac 3); |
|
124 by (dtac (zle_zminus RS iffD1) 2); |
|
125 by (ALLGOALS (dtac (negative_zle_0 RSN(2,zle_trans)))); |
|
126 by (ALLGOALS Asm_full_simp_tac); |
|
127 qed "int_zle_neg"; |
|
128 |
|
129 Goal "~($# n < - $# m)"; |
|
130 by (simp_tac (simpset() addsimps [symmetric zle_def]) 1); |
|
131 qed "not_int_zless_negative"; |
|
132 |
|
133 Goal "(- $# n = $# m) = (n = 0 & m = 0)"; |
|
134 by (rtac iffI 1); |
|
135 by (rtac (int_zle_neg RS iffD1) 1); |
|
136 by (dtac sym 1); |
|
137 by (ALLGOALS Asm_simp_tac); |
|
138 qed "negative_eq_positive"; |
|
139 |
|
140 Addsimps [negative_eq_positive, not_int_zless_negative]; |
|
141 |
|
142 |
|
143 Goal "(w <= z) = (EX n. z = w + $# n)"; |
|
144 by (auto_tac (claset(), |
|
145 simpset() addsimps [zless_iff_Suc_zadd, integ_le_less])); |
|
146 by (ALLGOALS (full_simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac))); |
|
147 by (ALLGOALS (full_simp_tac (simpset() addsimps [iszero_def]))); |
|
148 by (blast_tac (claset() addIs [Suc_pred RS sym]) 1); |
|
149 qed "zle_iff_zadd"; |
|
150 |
|
151 |
|
152 Goalw [zdiff_def,zless_def] "neg x = (x < $# 0)"; |
|
153 by Auto_tac; |
|
154 qed "neg_eq_less_nat0"; |
|
155 |
|
156 Goalw [zle_def] "(~neg x) = ($# 0 <= x)"; |
|
157 by (simp_tac (simpset() addsimps [neg_eq_less_nat0]) 1); |
|
158 qed "not_neg_eq_ge_nat0"; |
|
159 |
|
160 |
|
161 (**** nat: magnitide of an integer, as a natural number ****) |
|
162 |
|
163 Goalw [nat_def] "nat($# n) = n"; |
|
164 by Auto_tac; |
|
165 qed "nat_nat"; |
|
166 |
|
167 Goalw [nat_def] "nat(- $# n) = 0"; |
|
168 by (auto_tac (claset(), |
|
169 simpset() addsimps [neg_eq_less_nat0, zminus_zless])); |
|
170 qed "nat_zminus_nat"; |
|
171 |
|
172 Addsimps [nat_nat, nat_zminus_nat]; |
|
173 |
|
174 Goal "~ neg z ==> $# (nat z) = z"; |
|
175 by (dtac (not_neg_eq_ge_nat0 RS iffD1) 1); |
|
176 by (dtac zle_imp_zless_or_eq 1); |
|
177 by (auto_tac (claset(), simpset() addsimps [zless_iff_Suc_zadd])); |
|
178 qed "not_neg_nat"; |
|
179 |
|
180 Goal "neg x ==> ? n. x = - $# Suc n"; |
|
181 by (auto_tac (claset(), |
|
182 simpset() addsimps [neg_eq_less_nat0, zless_iff_Suc_zadd, |
|
183 zdiff_eq_eq RS sym, zdiff_def])); |
|
184 qed "negD"; |
|
185 |
|
186 Goalw [nat_def] "neg z ==> nat z = 0"; |
|
187 by Auto_tac; |
|
188 qed "neg_nat"; |
|
189 |
|
190 (* a case theorem distinguishing positive and negative int *) |
|
191 |
|
192 val prems = Goal "[|!! n. P ($# n); !! n. P (- $# Suc n) |] ==> P z"; |
|
193 by (case_tac "neg z" 1); |
|
194 by (blast_tac (claset() addSDs [negD] addSIs prems) 1); |
|
195 by (etac (not_neg_nat RS subst) 1); |
|
196 by (resolve_tac prems 1); |
|
197 qed "int_cases"; |
|
198 |
|
199 fun int_case_tac x = res_inst_tac [("z",x)] int_cases; |
|
200 |