author | paulson |
Thu, 24 Sep 1998 15:23:47 +0200 | |
changeset 5547 | 29f09a778037 |
parent 5540 | 0f16c3b66ab4 |
permissions | -rw-r--r-- |
5509
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
1 |
(* Title: Integ.thy |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
2 |
ID: $Id$ |
5509
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
4 |
Copyright 1998 University of Cambridge |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
5 |
|
5509
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
6 |
Type "int" is a linear order |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
7 |
*) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
8 |
|
5540 | 9 |
Goal "(w<z) = neg(w-z)"; |
5509
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
10 |
by (simp_tac (simpset() addsimps [zless_def]) 1); |
5540 | 11 |
qed "zless_eq_neg"; |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
12 |
|
5509
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
13 |
Goal "(w=z) = iszero(w-z)"; |
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
14 |
by (simp_tac (simpset() addsimps [iszero_def, zdiff_eq_eq]) 1); |
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
15 |
qed "eq_eq_iszero"; |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
16 |
|
5540 | 17 |
Goal "(w<=z) = (~ neg(z-w))"; |
5509
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
18 |
by (simp_tac (simpset() addsimps [zle_def, zless_def]) 1); |
5540 | 19 |
qed "zle_eq_not_neg"; |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
20 |
|
5509
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
21 |
(*This list of rewrites simplifies (in)equalities by subtracting the RHS |
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
22 |
from the LHS, then using the cancellation simproc. Use with zadd_ac.*) |
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
23 |
val zcompare_0_rls = |
5540 | 24 |
[zdiff_def, zless_eq_neg, eq_eq_iszero, zle_eq_not_neg]; |
5491 | 25 |
|
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
26 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
27 |
(*** Monotonicity results ***) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
28 |
|
5509
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
29 |
Goal "(v+z < w+z) = (v < (w::int))"; |
5540 | 30 |
by (full_simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1); |
5509
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
31 |
qed "zadd_right_cancel_zless"; |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
32 |
|
5509
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
33 |
Goal "(z+v < z+w) = (v < (w::int))"; |
5540 | 34 |
by (full_simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
35 |
qed "zadd_left_cancel_zless"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
36 |
|
5509
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
37 |
Addsimps [zadd_right_cancel_zless, zadd_left_cancel_zless]; |
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
38 |
|
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
39 |
Goal "(v+z <= w+z) = (v <= (w::int))"; |
5540 | 40 |
by (full_simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1); |
5509
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
41 |
qed "zadd_right_cancel_zle"; |
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
42 |
|
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
43 |
Goal "(z+v <= z+w) = (v <= (w::int))"; |
5540 | 44 |
by (full_simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
45 |
qed "zadd_left_cancel_zle"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
46 |
|
5509
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
47 |
Addsimps [zadd_right_cancel_zle, zadd_left_cancel_zle]; |
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
48 |
|
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
49 |
(*"v<=w ==> v+z <= w+z"*) |
5509
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
50 |
bind_thm ("zadd_zless_mono1", zadd_right_cancel_zless RS iffD2); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
51 |
|
5509
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
52 |
(*"v<=w ==> v+z <= w+z"*) |
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
53 |
bind_thm ("zadd_zle_mono1", zadd_right_cancel_zle RS iffD2); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
54 |
|
5316 | 55 |
Goal "!!z z'::int. [| w'<=w; z'<=z |] ==> w' + z' <= w + z"; |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
56 |
by (etac (zadd_zle_mono1 RS zle_trans) 1); |
5509
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
57 |
by (Simp_tac 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
58 |
qed "zadd_zle_mono"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
59 |
|
5509
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
60 |
Goal "!!z z'::int. [| w'<w; z'<=z |] ==> w' + z' < w + z"; |
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
61 |
by (etac (zadd_zless_mono1 RS zless_zle_trans) 1); |
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
62 |
by (Simp_tac 1); |
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
63 |
qed "zadd_zless_mono"; |
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
64 |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
65 |
|
5509
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
66 |
(*** Comparison laws ***) |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
67 |
|
5491 | 68 |
Goal "(- x < - y) = (y < (x::int))"; |
5540 | 69 |
by (simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1); |
5491 | 70 |
qed "zminus_zless_zminus"; |
71 |
Addsimps [zminus_zless_zminus]; |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
72 |
|
5491 | 73 |
Goal "(- x <= - y) = (y <= (x::int))"; |
5540 | 74 |
by (simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1); |
5491 | 75 |
qed "zminus_zle_zminus"; |
76 |
Addsimps [zminus_zle_zminus]; |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
77 |
|
5491 | 78 |
(** The next several equations can make the simplifier loop! **) |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
79 |
|
5491 | 80 |
Goal "(x < - y) = (y < - (x::int))"; |
5540 | 81 |
by (simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1); |
3725 | 82 |
qed "zless_zminus"; |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
83 |
|
5491 | 84 |
Goal "(- x < y) = (- y < (x::int))"; |
5540 | 85 |
by (simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1); |
3725 | 86 |
qed "zminus_zless"; |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
87 |
|
5491 | 88 |
Goal "(x <= - y) = (y <= - (x::int))"; |
5540 | 89 |
by (simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1); |
3725 | 90 |
qed "zle_zminus"; |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
91 |
|
5491 | 92 |
Goal "(- x <= y) = (- y <= (x::int))"; |
5540 | 93 |
by (simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1); |
3725 | 94 |
qed "zminus_zle"; |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
95 |
|
5491 | 96 |
Goal "- $# Suc n < $# 0"; |
5540 | 97 |
by (simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1); |
5491 | 98 |
qed "negative_zless_0"; |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
99 |
|
5491 | 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]; |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
105 |
|
5491 | 106 |
Goal "- $# n <= $#0"; |
5540 | 107 |
by (simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1); |
5491 | 108 |
qed "negative_zle_0"; |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
109 |
|
5491 | 110 |
Goal "- $# n <= $# m"; |
5540 | 111 |
by (simp_tac (simpset() addsimps add_nat :: zcompare_0_rls @ zadd_ac) 1); |
5491 | 112 |
qed "negative_zle"; |
113 |
AddIffs [negative_zle]; |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
114 |
|
5491 | 115 |
Goal "~($# 0 <= - $# Suc n)"; |
116 |
by (stac zle_zminus 1); |
|
117 |
by (Simp_tac 1); |
|
3725 | 118 |
qed "not_zle_0_negative"; |
5491 | 119 |
Addsimps [not_zle_0_negative]; |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
120 |
|
5491 | 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); |
|
5540 | 127 |
qed "nat_zle_neg"; |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
128 |
|
5491 | 129 |
Goal "~($# n < - $# m)"; |
130 |
by (simp_tac (simpset() addsimps [symmetric zle_def]) 1); |
|
5540 | 131 |
qed "not_nat_zless_negative"; |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
132 |
|
5491 | 133 |
Goal "(- $# n = $# m) = (n = 0 & m = 0)"; |
134 |
by (rtac iffI 1); |
|
5540 | 135 |
by (rtac (nat_zle_neg RS iffD1) 1); |
5491 | 136 |
by (dtac sym 1); |
137 |
by (ALLGOALS Asm_simp_tac); |
|
3725 | 138 |
qed "negative_eq_positive"; |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
139 |
|
5540 | 140 |
Addsimps [negative_eq_positive, not_nat_zless_negative]; |
141 |
||
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
142 |
|
5540 | 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"; |
|
5509
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
159 |
|
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
160 |
|
5540 | 161 |
(**** nat_of: magnitide of an integer, as a natural number ****) |
5509
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
162 |
|
5540 | 163 |
Goalw [nat_of_def] "nat_of($# n) = n"; |
164 |
by Auto_tac; |
|
165 |
qed "nat_of_nat"; |
|
5509
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
166 |
|
5547
29f09a778037
Function nat_of now maps negative integers to zero, not their absolute value
paulson
parents:
5540
diff
changeset
|
167 |
Goalw [nat_of_def] "nat_of(- $# n) = 0"; |
29f09a778037
Function nat_of now maps negative integers to zero, not their absolute value
paulson
parents:
5540
diff
changeset
|
168 |
by (auto_tac (claset(), |
29f09a778037
Function nat_of now maps negative integers to zero, not their absolute value
paulson
parents:
5540
diff
changeset
|
169 |
simpset() addsimps [neg_eq_less_nat0, zminus_zless])); |
5540 | 170 |
qed "nat_of_zminus_nat"; |
5509
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
171 |
|
5540 | 172 |
Addsimps [nat_of_nat, nat_of_zminus_nat]; |
5509
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
173 |
|
5540 | 174 |
Goal "~ neg z ==> $# (nat_of z) = z"; |
175 |
by (dtac (not_neg_eq_ge_nat0 RS iffD1) 1); |
|
5509
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
176 |
by (dtac zle_imp_zless_or_eq 1); |
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
177 |
by (auto_tac (claset(), simpset() addsimps [zless_iff_Suc_zadd])); |
5540 | 178 |
qed "not_neg_nat_of"; |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
179 |
|
5540 | 180 |
Goal "neg x ==> ? n. x = - $# Suc n"; |
5509
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
181 |
by (auto_tac (claset(), |
5540 | 182 |
simpset() addsimps [neg_eq_less_nat0, zless_iff_Suc_zadd, |
5509
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
183 |
zdiff_eq_eq RS sym, zdiff_def])); |
5540 | 184 |
qed "negD"; |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
185 |
|
5547
29f09a778037
Function nat_of now maps negative integers to zero, not their absolute value
paulson
parents:
5540
diff
changeset
|
186 |
Goalw [nat_of_def] "neg z ==> nat_of z = 0"; |
5491 | 187 |
by Auto_tac; |
5540 | 188 |
qed "neg_nat_of"; |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
189 |
|
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
190 |
(* a case theorem distinguishing positive and negative int *) |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
191 |
|
5491 | 192 |
val prems = Goal "[|!! n. P ($# n); !! n. P (- $# Suc n) |] ==> P z"; |
5540 | 193 |
by (case_tac "neg z" 1); |
194 |
by (blast_tac (claset() addSDs [negD] addSIs prems) 1); |
|
195 |
by (etac (not_neg_nat_of RS subst) 1); |
|
196 |
by (resolve_tac prems 1); |
|
3725 | 197 |
qed "int_cases"; |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
198 |
|
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
199 |
fun int_case_tac x = res_inst_tac [("z",x)] int_cases; |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
200 |