author | paulson |
Fri, 18 Sep 1998 16:04:44 +0200 | |
changeset 5509 | c38cc427976c |
parent 5491 | 22f8331cdf47 |
child 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 |
|
5509
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
9 |
Goal "(w<z) = znegative(w-z)"; |
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); |
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
11 |
qed "zless_eq_znegative"; |
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 |
|
5509
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
17 |
Goal "(w<=z) = (~ znegative(z-w))"; |
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); |
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
19 |
qed "zle_eq_not_znegative"; |
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 = |
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
24 |
[zdiff_def, zless_eq_znegative, eq_eq_iszero, zle_eq_not_znegative]; |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
25 |
|
5491 | 26 |
|
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
27 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
28 |
(*** Monotonicity results ***) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
29 |
|
5509
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
30 |
Goal "(v+z < w+z) = (v < (w::int))"; |
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
31 |
by (full_simp_tac (simpset() addsimps (zcompare_0_rls @ zadd_ac)) 1); |
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
32 |
qed "zadd_right_cancel_zless"; |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
33 |
|
5509
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
34 |
Goal "(z+v < z+w) = (v < (w::int))"; |
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
35 |
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
|
36 |
qed "zadd_left_cancel_zless"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
37 |
|
5509
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
38 |
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
|
39 |
|
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
40 |
Goal "(v+z <= w+z) = (v <= (w::int))"; |
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
41 |
by (full_simp_tac (simpset() addsimps (zcompare_0_rls @ zadd_ac)) 1); |
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
42 |
qed "zadd_right_cancel_zle"; |
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
43 |
|
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
44 |
Goal "(z+v <= z+w) = (v <= (w::int))"; |
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
45 |
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
|
46 |
qed "zadd_left_cancel_zle"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
47 |
|
5509
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
48 |
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
|
49 |
|
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
50 |
(*"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
|
51 |
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
|
52 |
|
5509
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
53 |
(*"v<=w ==> v+z <= w+z"*) |
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
54 |
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
|
55 |
|
5316 | 56 |
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
|
57 |
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
|
58 |
by (Simp_tac 1); |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
59 |
qed "zadd_zle_mono"; |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
60 |
|
5509
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
61 |
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
|
62 |
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
|
63 |
by (Simp_tac 1); |
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
64 |
qed "zadd_zless_mono"; |
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
65 |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
66 |
|
5509
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
67 |
(*** Comparison laws ***) |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
68 |
|
5491 | 69 |
Goal "(- x < - y) = (y < (x::int))"; |
5509
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
70 |
by (simp_tac (simpset() addsimps (zcompare_0_rls @ zadd_ac)) 1); |
5491 | 71 |
qed "zminus_zless_zminus"; |
72 |
Addsimps [zminus_zless_zminus]; |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
73 |
|
5491 | 74 |
Goal "(- x <= - y) = (y <= (x::int))"; |
5509
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
75 |
by (simp_tac (simpset() addsimps (zcompare_0_rls @ zadd_ac)) 1); |
5491 | 76 |
qed "zminus_zle_zminus"; |
77 |
Addsimps [zminus_zle_zminus]; |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
78 |
|
5491 | 79 |
(** 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
|
80 |
|
5491 | 81 |
Goal "(x < - y) = (y < - (x::int))"; |
5509
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
82 |
by (simp_tac (simpset() addsimps (zcompare_0_rls @ zadd_ac)) 1); |
3725 | 83 |
qed "zless_zminus"; |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
84 |
|
5491 | 85 |
Goal "(- x < y) = (- y < (x::int))"; |
5509
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
86 |
by (simp_tac (simpset() addsimps (zcompare_0_rls @ zadd_ac)) 1); |
3725 | 87 |
qed "zminus_zless"; |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
88 |
|
5491 | 89 |
Goal "(x <= - y) = (y <= - (x::int))"; |
5509
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
90 |
by (simp_tac (simpset() addsimps (zcompare_0_rls @ zadd_ac)) 1); |
3725 | 91 |
qed "zle_zminus"; |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
92 |
|
5491 | 93 |
Goal "(- x <= y) = (- y <= (x::int))"; |
5509
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
94 |
by (simp_tac (simpset() addsimps (zcompare_0_rls @ zadd_ac)) 1); |
3725 | 95 |
qed "zminus_zle"; |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
96 |
|
5509
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
97 |
Goal "$#0 < $# Suc n"; |
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
98 |
by (Simp_tac 1); |
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
99 |
qed "zero_zless_Suc"; |
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
100 |
|
5491 | 101 |
Goal "- $# Suc n < $# 0"; |
5509
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
102 |
by (simp_tac (simpset() addsimps (zcompare_0_rls @ zadd_ac)) 1); |
5491 | 103 |
qed "negative_zless_0"; |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
104 |
|
5491 | 105 |
Goal "- $# Suc n < $# m"; |
106 |
by (rtac (negative_zless_0 RS zless_zle_trans) 1); |
|
107 |
by (Simp_tac 1); |
|
108 |
qed "negative_zless"; |
|
109 |
AddIffs [negative_zless]; |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
110 |
|
5491 | 111 |
Goal "- $# n <= $#0"; |
5509
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
112 |
by (simp_tac (simpset() addsimps (zcompare_0_rls @ zadd_ac)) 1); |
5491 | 113 |
qed "negative_zle_0"; |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
114 |
|
5491 | 115 |
Goal "- $# n <= $# m"; |
5509
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
116 |
by (simp_tac (simpset() addsimps (add_znat::(zcompare_0_rls @ zadd_ac))) 1); |
5491 | 117 |
qed "negative_zle"; |
118 |
AddIffs [negative_zle]; |
|
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
119 |
|
5491 | 120 |
Goal "~($# 0 <= - $# Suc n)"; |
121 |
by (stac zle_zminus 1); |
|
122 |
by (Simp_tac 1); |
|
3725 | 123 |
qed "not_zle_0_negative"; |
5491 | 124 |
Addsimps [not_zle_0_negative]; |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
125 |
|
5491 | 126 |
Goal "($# n <= - $# m) = (n = 0 & m = 0)"; |
127 |
by Safe_tac; |
|
128 |
by (Simp_tac 3); |
|
129 |
by (dtac (zle_zminus RS iffD1) 2); |
|
130 |
by (ALLGOALS (dtac (negative_zle_0 RSN(2,zle_trans)))); |
|
131 |
by (ALLGOALS Asm_full_simp_tac); |
|
3725 | 132 |
qed "znat_zle_znegative"; |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
133 |
|
5491 | 134 |
Goal "~($# n < - $# m)"; |
135 |
by (simp_tac (simpset() addsimps [symmetric zle_def]) 1); |
|
3725 | 136 |
qed "not_znat_zless_negative"; |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
137 |
|
5491 | 138 |
Goal "(- $# n = $# m) = (n = 0 & m = 0)"; |
139 |
by (rtac iffI 1); |
|
140 |
by (rtac (znat_zle_znegative RS iffD1) 1); |
|
141 |
by (dtac sym 1); |
|
142 |
by (ALLGOALS Asm_simp_tac); |
|
3725 | 143 |
qed "negative_eq_positive"; |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
144 |
|
5491 | 145 |
Addsimps [negative_eq_positive, not_znat_zless_negative]; |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
146 |
|
5509
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
147 |
|
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
148 |
|
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5069
diff
changeset
|
149 |
Goalw [zdiff_def,zless_def] "znegative x = (x < $# 0)"; |
5491 | 150 |
by Auto_tac; |
5509
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
151 |
qed "znegative_eq_less_nat0"; |
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
152 |
|
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
153 |
Goalw [zle_def] "(~znegative x) = ($# 0 <= x)"; |
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
154 |
by (simp_tac (simpset() addsimps [znegative_eq_less_nat0]) 1); |
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
155 |
qed "not_znegative_eq_ge_nat0"; |
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
156 |
|
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
157 |
(**** zmagnitude: magnitide of an integer, as a natural number ****) |
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
158 |
|
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
159 |
Goalw [zmagnitude_def] "zmagnitude($# n) = n"; |
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
160 |
by Auto_tac; |
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
161 |
qed "zmagnitude_znat"; |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
162 |
|
5509
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
163 |
Goalw [zmagnitude_def] "zmagnitude(- $# n) = n"; |
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
164 |
by Auto_tac; |
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
165 |
qed "zmagnitude_zminus_znat"; |
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
166 |
|
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
167 |
Addsimps [zmagnitude_znat, zmagnitude_zminus_znat]; |
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
168 |
|
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
169 |
Goal "~ znegative z ==> $# (zmagnitude z) = z"; |
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
170 |
by (dtac (not_znegative_eq_ge_nat0 RS iffD1) 1); |
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
171 |
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
|
172 |
by (auto_tac (claset(), simpset() addsimps [zless_iff_Suc_zadd])); |
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
173 |
qed "not_zneg_mag"; |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
174 |
|
5491 | 175 |
Goal "znegative x ==> ? n. x = - $# Suc n"; |
5509
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
176 |
by (auto_tac (claset(), |
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
177 |
simpset() addsimps [znegative_eq_less_nat0, zless_iff_Suc_zadd, |
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
178 |
zdiff_eq_eq RS sym, zdiff_def])); |
3725 | 179 |
qed "znegativeD"; |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
180 |
|
5509
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
181 |
Goal "znegative z ==> $# (zmagnitude z) = -z"; |
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
182 |
bd znegativeD 1; |
5491 | 183 |
by Auto_tac; |
5509
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
184 |
qed "zneg_mag"; |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
185 |
|
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
186 |
(* a case theorem distinguishing positive and negative int *) |
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
187 |
|
5491 | 188 |
val prems = Goal "[|!! n. P ($# n); !! n. P (- $# Suc n) |] ==> P z"; |
5509
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
189 |
by (case_tac "znegative z" 1); |
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
190 |
by (blast_tac (claset() addSDs [znegativeD] addSIs prems) 1); |
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
191 |
be (not_zneg_mag RS subst) 1; |
c38cc427976c
Now defines "int" as a linear order; basic derivations moved to IntDef
paulson
parents:
5491
diff
changeset
|
192 |
brs prems 1; |
3725 | 193 |
qed "int_cases"; |
2224
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
194 |
|
4fc4b465be5b
New material from Norbert Voelker for efficient binary comparisons
paulson
parents:
2215
diff
changeset
|
195 |
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
|
196 |