author | paulson |
Tue, 10 Feb 2004 12:02:11 +0100 | |
changeset 14378 | 69c4d5997669 |
parent 14365 | 3d4df8c166ae |
child 14387 | e96d5c42c4b0 |
permissions | -rw-r--r-- |
1632 | 1 |
(* Title: HOL/Integ/Bin.thy |
6910 | 2 |
ID: $Id$ |
1632 | 3 |
Authors: Lawrence C Paulson, Cambridge University Computer Laboratory |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
4 |
David Spelt, University of Twente |
1632 | 5 |
Copyright 1994 University of Cambridge |
6 |
Copyright 1996 University of Twente |
|
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
7 |
*) |
1632 | 8 |
|
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
9 |
header{*Arithmetic on Binary Integers*} |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
10 |
|
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14365
diff
changeset
|
11 |
theory Bin = IntDef + Numeral: |
1632 | 12 |
|
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
13 |
text{*The sign @{term Pls} stands for an infinite string of leading Falses.*} |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
14 |
text{*The sign @{term Min} stands for an infinite string of leading Trues.*} |
1632 | 15 |
|
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
16 |
text{*A number can have multiple representations, namely leading Falses with |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
17 |
sign @{term Pls} and leading Trues with sign @{term Min}. |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
18 |
See @{text "ZF/Integ/twos-compl.ML"}, function @{text int_of_binary}, |
2988
d38f330e58b3
Renamed sign constructors to eliminate clash with the Plus infix of Sum.thy
paulson
parents:
1632
diff
changeset
|
19 |
for the numerical interpretation. |
1632 | 20 |
|
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
21 |
The representation expects that @{term "(m mod 2)"} is 0 or 1, |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
22 |
even if m is negative; |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
23 |
For instance, @{term "-5 div 2 = -3"} and @{term "-5 mod 2 = 1"}; thus |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
24 |
@{term "-5 = (-3)*2 + 1"}. |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
25 |
*} |
1632 | 26 |
|
27 |
consts |
|
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
28 |
NCons :: "[bin,bool]=>bin" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
29 |
bin_succ :: "bin=>bin" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
30 |
bin_pred :: "bin=>bin" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
31 |
bin_minus :: "bin=>bin" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
32 |
bin_add :: "[bin,bin]=>bin" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
33 |
bin_mult :: "[bin,bin]=>bin" |
1632 | 34 |
|
5512 | 35 |
(*NCons inserts a bit, suppressing leading 0s and 1s*) |
5184 | 36 |
primrec |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
37 |
NCons_Pls: "NCons bin.Pls b = (if b then (bin.Pls BIT b) else bin.Pls)" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
38 |
NCons_Min: "NCons bin.Min b = (if b then bin.Min else (bin.Min BIT b))" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
39 |
NCons_BIT: "NCons (w BIT x) b = (w BIT x) BIT b" |
6910 | 40 |
|
41 |
instance |
|
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
42 |
int :: number .. |
6988 | 43 |
|
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
9207
diff
changeset
|
44 |
primrec (*the type constraint is essential!*) |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
45 |
number_of_Pls: "number_of bin.Pls = 0" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
46 |
number_of_Min: "number_of bin.Min = - (1::int)" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
47 |
number_of_BIT: "number_of(w BIT x) = (if x then 1 else 0) + |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
48 |
(number_of w) + (number_of w)" |
1632 | 49 |
|
5184 | 50 |
primrec |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
51 |
bin_succ_Pls: "bin_succ bin.Pls = bin.Pls BIT True" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
52 |
bin_succ_Min: "bin_succ bin.Min = bin.Pls" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
53 |
bin_succ_BIT: "bin_succ(w BIT x) = |
5546 | 54 |
(if x then bin_succ w BIT False |
55 |
else NCons w True)" |
|
1632 | 56 |
|
5184 | 57 |
primrec |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
58 |
bin_pred_Pls: "bin_pred bin.Pls = bin.Min" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
59 |
bin_pred_Min: "bin_pred bin.Min = bin.Min BIT False" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
60 |
bin_pred_BIT: "bin_pred(w BIT x) = |
5546 | 61 |
(if x then NCons w False |
62 |
else (bin_pred w) BIT True)" |
|
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
63 |
|
5184 | 64 |
primrec |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
65 |
bin_minus_Pls: "bin_minus bin.Pls = bin.Pls" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
66 |
bin_minus_Min: "bin_minus bin.Min = bin.Pls BIT True" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
67 |
bin_minus_BIT: "bin_minus(w BIT x) = |
5546 | 68 |
(if x then bin_pred (NCons (bin_minus w) False) |
69 |
else bin_minus w BIT False)" |
|
1632 | 70 |
|
5184 | 71 |
primrec |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
72 |
bin_add_Pls: "bin_add bin.Pls w = w" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
73 |
bin_add_Min: "bin_add bin.Min w = bin_pred w" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
74 |
bin_add_BIT: |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
75 |
"bin_add (v BIT x) w = |
9207 | 76 |
(case w of Pls => v BIT x |
77 |
| Min => bin_pred (v BIT x) |
|
78 |
| (w BIT y) => |
|
79 |
NCons (bin_add v (if (x & y) then bin_succ w else w)) |
|
80 |
(x~=y))" |
|
1632 | 81 |
|
5184 | 82 |
primrec |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
83 |
bin_mult_Pls: "bin_mult bin.Pls w = bin.Pls" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
84 |
bin_mult_Min: "bin_mult bin.Min w = bin_minus w" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
85 |
bin_mult_BIT: "bin_mult (v BIT x) w = |
5546 | 86 |
(if x then (bin_add (NCons (bin_mult v w) False) w) |
87 |
else (NCons (bin_mult v w) False))" |
|
5491 | 88 |
|
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
89 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
90 |
(** extra rules for bin_succ, bin_pred, bin_add, bin_mult **) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
91 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
92 |
lemma NCons_Pls_0: "NCons bin.Pls False = bin.Pls" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
93 |
by simp |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
94 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
95 |
lemma NCons_Pls_1: "NCons bin.Pls True = bin.Pls BIT True" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
96 |
by simp |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
97 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
98 |
lemma NCons_Min_0: "NCons bin.Min False = bin.Min BIT False" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
99 |
by simp |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
100 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
101 |
lemma NCons_Min_1: "NCons bin.Min True = bin.Min" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
102 |
by simp |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
103 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
104 |
lemma bin_succ_1: "bin_succ(w BIT True) = (bin_succ w) BIT False" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
105 |
by simp |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
106 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
107 |
lemma bin_succ_0: "bin_succ(w BIT False) = NCons w True" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
108 |
by simp |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
109 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
110 |
lemma bin_pred_1: "bin_pred(w BIT True) = NCons w False" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
111 |
by simp |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
112 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
113 |
lemma bin_pred_0: "bin_pred(w BIT False) = (bin_pred w) BIT True" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
114 |
by simp |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
115 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
116 |
lemma bin_minus_1: "bin_minus(w BIT True) = bin_pred (NCons (bin_minus w) False)" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
117 |
by simp |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
118 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
119 |
lemma bin_minus_0: "bin_minus(w BIT False) = (bin_minus w) BIT False" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
120 |
by simp |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
121 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
122 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
123 |
(*** bin_add: binary addition ***) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
124 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
125 |
lemma bin_add_BIT_11: "bin_add (v BIT True) (w BIT True) = |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
126 |
NCons (bin_add v (bin_succ w)) False" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
127 |
apply simp |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
128 |
done |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
129 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
130 |
lemma bin_add_BIT_10: "bin_add (v BIT True) (w BIT False) = NCons (bin_add v w) True" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
131 |
by simp |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
132 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
133 |
lemma bin_add_BIT_0: "bin_add (v BIT False) (w BIT y) = NCons (bin_add v w) y" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
134 |
by auto |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
135 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
136 |
lemma bin_add_Pls_right: "bin_add w bin.Pls = w" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
137 |
by (induct_tac "w", auto) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
138 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
139 |
lemma bin_add_Min_right: "bin_add w bin.Min = bin_pred w" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
140 |
by (induct_tac "w", auto) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
141 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
142 |
lemma bin_add_BIT_BIT: "bin_add (v BIT x) (w BIT y) = |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
143 |
NCons(bin_add v (if x & y then (bin_succ w) else w)) (x~= y)" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
144 |
apply simp |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
145 |
done |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
146 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
147 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
148 |
(*** bin_mult: binary multiplication ***) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
149 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
150 |
lemma bin_mult_1: "bin_mult (v BIT True) w = bin_add (NCons (bin_mult v w) False) w" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
151 |
by simp |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
152 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
153 |
lemma bin_mult_0: "bin_mult (v BIT False) w = NCons (bin_mult v w) False" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
154 |
by simp |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
155 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
156 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
157 |
(**** The carry/borrow functions, bin_succ and bin_pred ****) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
158 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
159 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
160 |
(** number_of **) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
161 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
162 |
lemma number_of_NCons [simp]: |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
163 |
"number_of(NCons w b) = (number_of(w BIT b)::int)" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
164 |
apply (induct_tac "w") |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
165 |
apply (simp_all) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
166 |
done |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
167 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
168 |
lemma number_of_succ: "number_of(bin_succ w) = (1 + number_of w :: int)" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
169 |
apply (induct_tac "w") |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
170 |
apply (simp_all add: zadd_ac) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
171 |
done |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
172 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
173 |
lemma number_of_pred: "number_of(bin_pred w) = (- 1 + number_of w :: int)" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
174 |
apply (induct_tac "w") |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
175 |
apply (simp_all add: add_assoc [symmetric]) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
176 |
apply (simp add: zadd_ac) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
177 |
done |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
178 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
179 |
lemma number_of_minus: "number_of(bin_minus w) = (- (number_of w)::int)" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
180 |
apply (induct_tac "w", simp, simp) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
181 |
apply (simp del: bin_pred_Pls bin_pred_Min bin_pred_BIT add: number_of_succ number_of_pred zadd_assoc) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
182 |
done |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
183 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
184 |
(*This proof is complicated by the mutual recursion*) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
185 |
lemma number_of_add [rule_format (no_asm)]: "! w. number_of(bin_add v w) = (number_of v + number_of w::int)" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
186 |
apply (induct_tac "v", simp) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
187 |
apply (simp add: number_of_pred) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
188 |
apply (rule allI) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
189 |
apply (induct_tac "w") |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
190 |
apply (simp_all add: bin_add_BIT_BIT number_of_succ number_of_pred add_ac) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
191 |
apply (simp add: add_left_commute [of "1::int"]) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
192 |
done |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
193 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
194 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
195 |
(*Subtraction*) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
196 |
lemma diff_number_of_eq: |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
197 |
"number_of v - number_of w = (number_of(bin_add v (bin_minus w))::int)" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
198 |
apply (unfold zdiff_def) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
199 |
apply (simp add: number_of_add number_of_minus) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
200 |
done |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
201 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
202 |
lemmas bin_mult_simps = |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
203 |
int_Suc0_eq_1 zmult_zminus number_of_minus number_of_add |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
204 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
205 |
lemma number_of_mult: "number_of(bin_mult v w) = (number_of v * number_of w::int)" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
206 |
apply (induct_tac "v") |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
207 |
apply (simp add: bin_mult_simps) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
208 |
apply (simp add: bin_mult_simps) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
209 |
apply (simp add: bin_mult_simps zadd_zmult_distrib zadd_ac) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
210 |
done |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
211 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
212 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
213 |
(*The correctness of shifting. But it doesn't seem to give a measurable |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
214 |
speed-up.*) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
215 |
lemma double_number_of_BIT: "(2::int) * number_of w = number_of (w BIT False)" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
216 |
apply (induct_tac "w") |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
217 |
apply (simp_all add: bin_mult_simps zadd_zmult_distrib zadd_ac) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
218 |
done |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
219 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
220 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
221 |
(** Converting numerals 0 and 1 to their abstract versions **) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
222 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
223 |
lemma int_numeral_0_eq_0: "Numeral0 = (0::int)" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
224 |
by simp |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
225 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
226 |
lemma int_numeral_1_eq_1: "Numeral1 = (1::int)" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
227 |
by (simp add: int_1 int_Suc0_eq_1) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
228 |
|
14288 | 229 |
(*Moving negation out of products: so far for type "int" only*) |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
230 |
declare zmult_zminus [simp] zmult_zminus_right [simp] |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
231 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
232 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
233 |
(** Special-case simplification for small constants **) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
234 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
235 |
lemma zmult_minus1 [simp]: "-1 * z = -(z::int)" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
236 |
by (simp add: compare_rls int_Suc0_eq_1 zmult_zminus) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
237 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
238 |
lemma zmult_minus1_right [simp]: "z * -1 = -(z::int)" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
239 |
by (subst zmult_commute, rule zmult_minus1) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
240 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
241 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
242 |
(*Negation of a coefficient*) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
243 |
lemma zminus_number_of_zmult [simp]: "- (number_of w) * z = number_of(bin_minus w) * (z::int)" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
244 |
by (simp add: number_of_minus zmult_zminus) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
245 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
246 |
(*Integer unary minus for the abstract constant 1. Cannot be inserted |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
247 |
as a simprule until later: it is number_of_Min re-oriented!*) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
248 |
lemma zminus_1_eq_m1: "- 1 = (-1::int)" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
249 |
by simp |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
250 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
251 |
lemma zero_less_nat_eq [simp]: "(0 < nat z) = (0 < z)" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
252 |
by (cut_tac w = 0 in zless_nat_conj, auto) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
253 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
254 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
255 |
(** Simplification rules for comparison of binary numbers (Norbert Voelker) **) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
256 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
257 |
(** Equals (=) **) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
258 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
259 |
lemma eq_number_of_eq: |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
260 |
"((number_of x::int) = number_of y) = |
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14365
diff
changeset
|
261 |
iszero (number_of (bin_add x (bin_minus y)) :: int)" |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
262 |
apply (unfold iszero_def) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
263 |
apply (simp add: compare_rls number_of_add number_of_minus) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
264 |
done |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
265 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
266 |
lemma iszero_number_of_Pls: "iszero ((number_of bin.Pls)::int)" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
267 |
by (unfold iszero_def, simp) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
268 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
269 |
lemma nonzero_number_of_Min: "~ iszero ((number_of bin.Min)::int)" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
270 |
apply (unfold iszero_def) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
271 |
apply (simp add: eq_commute) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
272 |
done |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
273 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
274 |
lemma iszero_number_of_BIT: |
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14365
diff
changeset
|
275 |
"iszero (number_of (w BIT x)::int) = (~x & iszero (number_of w::int))" |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
276 |
apply (unfold iszero_def) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
277 |
apply (cases "(number_of w)::int" rule: int_cases) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
278 |
apply (simp_all (no_asm_simp) add: compare_rls zero_reorient |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
279 |
zminus_zadd_distrib [symmetric] int_Suc0_eq_1 [symmetric] zadd_int) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
280 |
done |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
281 |
|
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14365
diff
changeset
|
282 |
lemma iszero_number_of_0: |
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14365
diff
changeset
|
283 |
"iszero (number_of (w BIT False)::int) = iszero (number_of w::int)" |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
284 |
by (simp only: iszero_number_of_BIT simp_thms) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
285 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
286 |
lemma iszero_number_of_1: "~ iszero (number_of (w BIT True)::int)" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
287 |
by (simp only: iszero_number_of_BIT simp_thms) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
288 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
289 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
290 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
291 |
(** Less-than (<) **) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
292 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
293 |
lemma less_number_of_eq_neg: |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
294 |
"((number_of x::int) < number_of y) |
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14365
diff
changeset
|
295 |
= neg (number_of (bin_add x (bin_minus y)) ::int )" |
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14365
diff
changeset
|
296 |
by (simp add: neg_def number_of_add number_of_minus compare_rls) |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
297 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
298 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
299 |
(*But if Numeral0 is rewritten to 0 then this rule can't be applied: |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
300 |
Numeral0 IS (number_of Pls) *) |
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14365
diff
changeset
|
301 |
lemma not_neg_number_of_Pls: "~ neg (number_of bin.Pls ::int)" |
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14365
diff
changeset
|
302 |
by (simp add: neg_def) |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
303 |
|
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14365
diff
changeset
|
304 |
lemma neg_number_of_Min: "neg (number_of bin.Min ::int)" |
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14365
diff
changeset
|
305 |
by (simp add: neg_def int_0_less_1) |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
306 |
|
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14365
diff
changeset
|
307 |
lemma neg_number_of_BIT: |
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14365
diff
changeset
|
308 |
"neg (number_of (w BIT x)::int) = neg (number_of w ::int)" |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
309 |
apply simp |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
310 |
apply (cases "(number_of w)::int" rule: int_cases) |
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14365
diff
changeset
|
311 |
apply (simp_all (no_asm_simp) add: int_Suc0_eq_1 [symmetric] zadd_int neg_def zdiff_def [symmetric] compare_rls) |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
312 |
done |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
313 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
314 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
315 |
(** Less-than-or-equals (\<le>) **) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
316 |
|
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14288
diff
changeset
|
317 |
text{*Reduces @{term "a\<le>b"} to @{term "~ (b<a)"} for ALL numerals*} |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14288
diff
changeset
|
318 |
lemmas le_number_of_eq_not_less = |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14288
diff
changeset
|
319 |
linorder_not_less [of "number_of w" "number_of v", symmetric, standard] |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14288
diff
changeset
|
320 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14288
diff
changeset
|
321 |
declare le_number_of_eq_not_less [simp] |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14288
diff
changeset
|
322 |
|
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
323 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
324 |
(** Absolute value (abs) **) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
325 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
326 |
lemma zabs_number_of: |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
327 |
"abs(number_of x::int) = |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
328 |
(if number_of x < (0::int) then -number_of x else number_of x)" |
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14365
diff
changeset
|
329 |
by (simp add: zabs_def) |
14272
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
330 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
331 |
(*0 and 1 require special rewrites because they aren't numerals*) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
332 |
lemma zabs_0: "abs (0::int) = 0" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
333 |
by (simp add: zabs_def) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
334 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
335 |
lemma zabs_1: "abs (1::int) = 1" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
336 |
by (simp del: int_0 int_1 add: int_0 [symmetric] int_1 [symmetric] zabs_def) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
337 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
338 |
(*Re-orientation of the equation nnn=x*) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
339 |
lemma number_of_reorient: "(number_of w = x) = (x = number_of w)" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
340 |
by auto |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
341 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
342 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
343 |
(*Delete the original rewrites, with their clumsy conditional expressions*) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
344 |
declare bin_succ_BIT [simp del] bin_pred_BIT [simp del] |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
345 |
bin_minus_BIT [simp del] |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
346 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
347 |
declare bin_add_BIT [simp del] bin_mult_BIT [simp del] |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
348 |
declare NCons_Pls [simp del] NCons_Min [simp del] |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
349 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
350 |
(*Hide the binary representation of integer constants*) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
351 |
declare number_of_Pls [simp del] number_of_Min [simp del] |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
352 |
number_of_BIT [simp del] |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
353 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
354 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
355 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
356 |
(*Simplification of arithmetic operations on integer constants. |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
357 |
Note that bin_pred_Pls, etc. were added to the simpset by primrec.*) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
358 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
359 |
lemmas NCons_simps = NCons_Pls_0 NCons_Pls_1 NCons_Min_0 NCons_Min_1 NCons_BIT |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
360 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
361 |
lemmas bin_arith_extra_simps = |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
362 |
number_of_add [symmetric] |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
363 |
number_of_minus [symmetric] zminus_1_eq_m1 |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
364 |
number_of_mult [symmetric] |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
365 |
bin_succ_1 bin_succ_0 |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
366 |
bin_pred_1 bin_pred_0 |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
367 |
bin_minus_1 bin_minus_0 |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
368 |
bin_add_Pls_right bin_add_Min_right |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
369 |
bin_add_BIT_0 bin_add_BIT_10 bin_add_BIT_11 |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
370 |
diff_number_of_eq zabs_number_of zabs_0 zabs_1 |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
371 |
bin_mult_1 bin_mult_0 NCons_simps |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
372 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
373 |
(*For making a minimal simpset, one must include these default simprules |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
374 |
of thy. Also include simp_thms, or at least (~False)=True*) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
375 |
lemmas bin_arith_simps = |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
376 |
bin_pred_Pls bin_pred_Min |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
377 |
bin_succ_Pls bin_succ_Min |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
378 |
bin_add_Pls bin_add_Min |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
379 |
bin_minus_Pls bin_minus_Min |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
380 |
bin_mult_Pls bin_mult_Min bin_arith_extra_simps |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
381 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
382 |
(*Simplification of relational operations*) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
383 |
lemmas bin_rel_simps = |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
384 |
eq_number_of_eq iszero_number_of_Pls nonzero_number_of_Min |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
385 |
iszero_number_of_0 iszero_number_of_1 |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
386 |
less_number_of_eq_neg |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
387 |
not_neg_number_of_Pls not_neg_0 not_neg_1 not_iszero_1 |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
388 |
neg_number_of_Min neg_number_of_BIT |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
389 |
le_number_of_eq_not_less |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
390 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
391 |
declare bin_arith_extra_simps [simp] |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
392 |
declare bin_rel_simps [simp] |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
393 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
394 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
395 |
(** Simplification of arithmetic when nested to the right **) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
396 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
397 |
lemma add_number_of_left [simp]: "number_of v + (number_of w + z) = (number_of(bin_add v w) + z::int)" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
398 |
by (simp add: zadd_assoc [symmetric]) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
399 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
400 |
lemma mult_number_of_left [simp]: "number_of v * (number_of w * z) = (number_of(bin_mult v w) * z::int)" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
401 |
by (simp add: zmult_assoc [symmetric]) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
402 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
403 |
lemma add_number_of_diff1: |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
404 |
"number_of v + (number_of w - c) = number_of(bin_add v w) - (c::int)" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
405 |
apply (unfold zdiff_def) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
406 |
apply (rule add_number_of_left) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
407 |
done |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
408 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
409 |
lemma add_number_of_diff2 [simp]: "number_of v + (c - number_of w) = |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
410 |
number_of (bin_add v (bin_minus w)) + (c::int)" |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
411 |
apply (subst diff_number_of_eq [symmetric]) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
412 |
apply (simp only: compare_rls) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
413 |
done |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
414 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
415 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
416 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
417 |
(** Inserting these natural simprules earlier would break many proofs! **) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
418 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
419 |
(* int (Suc n) = 1 + int n *) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
420 |
declare int_Suc [simp] |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
421 |
|
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
422 |
(* Numeral0 -> 0 and Numeral1 -> 1 *) |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
423 |
declare int_numeral_0_eq_0 [simp] int_numeral_1_eq_1 [simp] |
5efbb548107d
Tidying of the integer development; towards removing the
paulson
parents:
13491
diff
changeset
|
424 |
|
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14288
diff
changeset
|
425 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14288
diff
changeset
|
426 |
(*Simplification of x-y < 0, etc.*) |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14288
diff
changeset
|
427 |
declare less_iff_diff_less_0 [symmetric, simp] |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14288
diff
changeset
|
428 |
declare eq_iff_diff_eq_0 [symmetric, simp] |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14288
diff
changeset
|
429 |
declare le_iff_diff_le_0 [symmetric, simp] |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14288
diff
changeset
|
430 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14288
diff
changeset
|
431 |
|
1632 | 432 |
end |