15647
|
1 |
(* AUTOMATICALLY GENERATED, DO NOT EDIT! *)
|
|
2 |
|
17566
|
3 |
theory HOL4Vec imports HOL4Base begin
|
14516
|
4 |
|
|
5 |
;setup_theory res_quan
|
|
6 |
|
17644
|
7 |
lemma RES_FORALL_CONJ_DIST: "ALL (P::'a::type => bool) (Q::'a::type => bool) R::'a::type => bool.
|
|
8 |
RES_FORALL P (%i::'a::type. Q i & R i) =
|
|
9 |
(RES_FORALL P Q & RES_FORALL P R)"
|
14516
|
10 |
by (import res_quan RES_FORALL_CONJ_DIST)
|
|
11 |
|
17644
|
12 |
lemma RES_FORALL_DISJ_DIST: "ALL (P::'a::type => bool) (Q::'a::type => bool) R::'a::type => bool.
|
|
13 |
RES_FORALL (%j::'a::type. P j | Q j) R =
|
|
14 |
(RES_FORALL P R & RES_FORALL Q R)"
|
14516
|
15 |
by (import res_quan RES_FORALL_DISJ_DIST)
|
|
16 |
|
17644
|
17 |
lemma RES_FORALL_UNIQUE: "ALL (x::'a::type => bool) xa::'a::type. RES_FORALL (op = xa) x = x xa"
|
14516
|
18 |
by (import res_quan RES_FORALL_UNIQUE)
|
|
19 |
|
17644
|
20 |
lemma RES_FORALL_FORALL: "ALL (P::'a::type => bool) (R::'a::type => 'b::type => bool) x::'b::type.
|
|
21 |
(ALL x::'b::type. RES_FORALL P (%i::'a::type. R i x)) =
|
|
22 |
RES_FORALL P (%i::'a::type. All (R i))"
|
14516
|
23 |
by (import res_quan RES_FORALL_FORALL)
|
|
24 |
|
17644
|
25 |
lemma RES_FORALL_REORDER: "ALL (P::'a::type => bool) (Q::'b::type => bool)
|
|
26 |
R::'a::type => 'b::type => bool.
|
|
27 |
RES_FORALL P (%i::'a::type. RES_FORALL Q (R i)) =
|
|
28 |
RES_FORALL Q (%j::'b::type. RES_FORALL P (%i::'a::type. R i j))"
|
14516
|
29 |
by (import res_quan RES_FORALL_REORDER)
|
|
30 |
|
|
31 |
lemma RES_FORALL_EMPTY: "All (RES_FORALL EMPTY)"
|
|
32 |
by (import res_quan RES_FORALL_EMPTY)
|
|
33 |
|
17644
|
34 |
lemma RES_FORALL_UNIV: "ALL p::'a::type => bool. RES_FORALL pred_set.UNIV p = All p"
|
14516
|
35 |
by (import res_quan RES_FORALL_UNIV)
|
|
36 |
|
17644
|
37 |
lemma RES_FORALL_NULL: "ALL (p::'a::type => bool) m::bool.
|
|
38 |
RES_FORALL p (%x::'a::type. m) = (p = EMPTY | m)"
|
14516
|
39 |
by (import res_quan RES_FORALL_NULL)
|
|
40 |
|
17644
|
41 |
lemma RES_EXISTS_DISJ_DIST: "ALL (P::'a::type => bool) (Q::'a::type => bool) R::'a::type => bool.
|
|
42 |
RES_EXISTS P (%i::'a::type. Q i | R i) =
|
|
43 |
(RES_EXISTS P Q | RES_EXISTS P R)"
|
14516
|
44 |
by (import res_quan RES_EXISTS_DISJ_DIST)
|
|
45 |
|
17644
|
46 |
lemma RES_DISJ_EXISTS_DIST: "ALL (P::'a::type => bool) (Q::'a::type => bool) R::'a::type => bool.
|
|
47 |
RES_EXISTS (%i::'a::type. P i | Q i) R =
|
|
48 |
(RES_EXISTS P R | RES_EXISTS Q R)"
|
14516
|
49 |
by (import res_quan RES_DISJ_EXISTS_DIST)
|
|
50 |
|
17644
|
51 |
lemma RES_EXISTS_EQUAL: "ALL (x::'a::type => bool) xa::'a::type. RES_EXISTS (op = xa) x = x xa"
|
14516
|
52 |
by (import res_quan RES_EXISTS_EQUAL)
|
|
53 |
|
17644
|
54 |
lemma RES_EXISTS_REORDER: "ALL (P::'a::type => bool) (Q::'b::type => bool)
|
|
55 |
R::'a::type => 'b::type => bool.
|
|
56 |
RES_EXISTS P (%i::'a::type. RES_EXISTS Q (R i)) =
|
|
57 |
RES_EXISTS Q (%j::'b::type. RES_EXISTS P (%i::'a::type. R i j))"
|
14516
|
58 |
by (import res_quan RES_EXISTS_REORDER)
|
|
59 |
|
17644
|
60 |
lemma RES_EXISTS_EMPTY: "ALL p::'a::type => bool. ~ RES_EXISTS EMPTY p"
|
14516
|
61 |
by (import res_quan RES_EXISTS_EMPTY)
|
|
62 |
|
17644
|
63 |
lemma RES_EXISTS_UNIV: "ALL p::'a::type => bool. RES_EXISTS pred_set.UNIV p = Ex p"
|
14516
|
64 |
by (import res_quan RES_EXISTS_UNIV)
|
|
65 |
|
17644
|
66 |
lemma RES_EXISTS_NULL: "ALL (p::'a::type => bool) m::bool.
|
|
67 |
RES_EXISTS p (%x::'a::type. m) = (p ~= EMPTY & m)"
|
14516
|
68 |
by (import res_quan RES_EXISTS_NULL)
|
|
69 |
|
17644
|
70 |
lemma RES_EXISTS_ALT: "ALL (p::'a::type => bool) m::'a::type => bool.
|
|
71 |
RES_EXISTS p m = (IN (RES_SELECT p m) p & m (RES_SELECT p m))"
|
14516
|
72 |
by (import res_quan RES_EXISTS_ALT)
|
|
73 |
|
17644
|
74 |
lemma RES_EXISTS_UNIQUE_EMPTY: "ALL p::'a::type => bool. ~ RES_EXISTS_UNIQUE EMPTY p"
|
14516
|
75 |
by (import res_quan RES_EXISTS_UNIQUE_EMPTY)
|
|
76 |
|
17644
|
77 |
lemma RES_EXISTS_UNIQUE_UNIV: "ALL p::'a::type => bool. RES_EXISTS_UNIQUE pred_set.UNIV p = Ex1 p"
|
14516
|
78 |
by (import res_quan RES_EXISTS_UNIQUE_UNIV)
|
|
79 |
|
17644
|
80 |
lemma RES_EXISTS_UNIQUE_NULL: "ALL (p::'a::type => bool) m::bool.
|
|
81 |
RES_EXISTS_UNIQUE p (%x::'a::type. m) =
|
|
82 |
((EX x::'a::type. p = INSERT x EMPTY) & m)"
|
14516
|
83 |
by (import res_quan RES_EXISTS_UNIQUE_NULL)
|
|
84 |
|
17644
|
85 |
lemma RES_EXISTS_UNIQUE_ALT: "ALL (p::'a::type => bool) m::'a::type => bool.
|
14516
|
86 |
RES_EXISTS_UNIQUE p m =
|
17644
|
87 |
RES_EXISTS p
|
|
88 |
(%x::'a::type. m x & RES_FORALL p (%y::'a::type. m y --> y = x))"
|
14516
|
89 |
by (import res_quan RES_EXISTS_UNIQUE_ALT)
|
|
90 |
|
17644
|
91 |
lemma RES_SELECT_EMPTY: "ALL p::'a::type => bool. RES_SELECT EMPTY p = (SOME x::'a::type. False)"
|
14516
|
92 |
by (import res_quan RES_SELECT_EMPTY)
|
|
93 |
|
17644
|
94 |
lemma RES_SELECT_UNIV: "ALL p::'a::type => bool. RES_SELECT pred_set.UNIV p = Eps p"
|
14516
|
95 |
by (import res_quan RES_SELECT_UNIV)
|
|
96 |
|
17644
|
97 |
lemma RES_ABSTRACT: "ALL (p::'a::type => bool) (m::'a::type => 'b::type) x::'a::type.
|
|
98 |
IN x p --> RES_ABSTRACT p m x = m x"
|
14516
|
99 |
by (import res_quan RES_ABSTRACT)
|
|
100 |
|
17644
|
101 |
lemma RES_ABSTRACT_EQUAL: "ALL (p::'a::type => bool) (m1::'a::type => 'b::type)
|
|
102 |
m2::'a::type => 'b::type.
|
|
103 |
(ALL x::'a::type. IN x p --> m1 x = m2 x) -->
|
|
104 |
RES_ABSTRACT p m1 = RES_ABSTRACT p m2"
|
14516
|
105 |
by (import res_quan RES_ABSTRACT_EQUAL)
|
|
106 |
|
17644
|
107 |
lemma RES_ABSTRACT_IDEMPOT: "ALL (p::'a::type => bool) m::'a::type => 'b::type.
|
|
108 |
RES_ABSTRACT p (RES_ABSTRACT p m) = RES_ABSTRACT p m"
|
14516
|
109 |
by (import res_quan RES_ABSTRACT_IDEMPOT)
|
|
110 |
|
17644
|
111 |
lemma RES_ABSTRACT_EQUAL_EQ: "ALL (p::'a::type => bool) (m1::'a::type => 'b::type)
|
|
112 |
m2::'a::type => 'b::type.
|
|
113 |
(RES_ABSTRACT p m1 = RES_ABSTRACT p m2) =
|
|
114 |
(ALL x::'a::type. IN x p --> m1 x = m2 x)"
|
14516
|
115 |
by (import res_quan RES_ABSTRACT_EQUAL_EQ)
|
|
116 |
|
|
117 |
;end_setup
|
|
118 |
|
|
119 |
;setup_theory word_base
|
|
120 |
|
17644
|
121 |
typedef (open) ('a) word = "(Collect::('a::type list recspace => bool) => 'a::type list recspace set)
|
|
122 |
(%x::'a::type list recspace.
|
|
123 |
(All::(('a::type list recspace => bool) => bool) => bool)
|
|
124 |
(%word::'a::type list recspace => bool.
|
14516
|
125 |
(op -->::bool => bool => bool)
|
17644
|
126 |
((All::('a::type list recspace => bool) => bool)
|
|
127 |
(%a0::'a::type list recspace.
|
14516
|
128 |
(op -->::bool => bool => bool)
|
17644
|
129 |
((Ex::('a::type list => bool) => bool)
|
|
130 |
(%a::'a::type list.
|
|
131 |
(op =::'a::type list recspace
|
|
132 |
=> 'a::type list recspace => bool)
|
14516
|
133 |
a0 ((CONSTR::nat
|
17644
|
134 |
=> 'a::type list
|
|
135 |
=> (nat => 'a::type list recspace) => 'a::type list recspace)
|
14516
|
136 |
(0::nat) a
|
17644
|
137 |
(%n::nat. BOTTOM::'a::type list recspace))))
|
14516
|
138 |
(word a0)))
|
|
139 |
(word x)))"
|
|
140 |
by (rule typedef_helper,import word_base word_TY_DEF)
|
|
141 |
|
|
142 |
lemmas word_TY_DEF = typedef_hol2hol4 [OF type_definition_word]
|
|
143 |
|
|
144 |
consts
|
17652
|
145 |
mk_word :: "'a list recspace => 'a word"
|
|
146 |
dest_word :: "'a word => 'a list recspace"
|
14516
|
147 |
|
17644
|
148 |
specification (dest_word mk_word) word_repfns: "(ALL a::'a::type word. mk_word (dest_word a) = a) &
|
|
149 |
(ALL r::'a::type list recspace.
|
|
150 |
(ALL word::'a::type list recspace => bool.
|
|
151 |
(ALL a0::'a::type list recspace.
|
17652
|
152 |
(EX a::'a::type list. a0 = CONSTR 0 a (%n::nat. BOTTOM)) -->
|
14516
|
153 |
word a0) -->
|
|
154 |
word r) =
|
|
155 |
(dest_word (mk_word r) = r))"
|
|
156 |
by (import word_base word_repfns)
|
|
157 |
|
|
158 |
consts
|
17652
|
159 |
word_base0 :: "'a list => 'a word"
|
14516
|
160 |
|
|
161 |
defs
|
17652
|
162 |
word_base0_primdef: "word_base0 == %a::'a::type list. mk_word (CONSTR 0 a (%n::nat. BOTTOM))"
|
14516
|
163 |
|
17652
|
164 |
lemma word_base0_def: "word_base0 = (%a::'a::type list. mk_word (CONSTR 0 a (%n::nat. BOTTOM)))"
|
14516
|
165 |
by (import word_base word_base0_def)
|
|
166 |
|
|
167 |
constdefs
|
17652
|
168 |
WORD :: "'a list => 'a word"
|
14516
|
169 |
"WORD == word_base0"
|
|
170 |
|
|
171 |
lemma WORD: "WORD = word_base0"
|
|
172 |
by (import word_base WORD)
|
|
173 |
|
|
174 |
consts
|
17652
|
175 |
word_case :: "('a list => 'b) => 'a word => 'b"
|
14516
|
176 |
|
17644
|
177 |
specification (word_case_primdef: word_case) word_case_def: "ALL (f::'a::type list => 'b::type) a::'a::type list.
|
|
178 |
word_case f (WORD a) = f a"
|
14516
|
179 |
by (import word_base word_case_def)
|
|
180 |
|
|
181 |
consts
|
17652
|
182 |
word_size :: "('a => nat) => 'a word => nat"
|
14516
|
183 |
|
17644
|
184 |
specification (word_size_primdef: word_size) word_size_def: "ALL (f::'a::type => nat) a::'a::type list.
|
17652
|
185 |
word_size f (WORD a) = 1 + list_size f a"
|
14516
|
186 |
by (import word_base word_size_def)
|
|
187 |
|
17644
|
188 |
lemma word_11: "ALL (a::'a::type list) a'::'a::type list. (WORD a = WORD a') = (a = a')"
|
14516
|
189 |
by (import word_base word_11)
|
|
190 |
|
17644
|
191 |
lemma word_case_cong: "ALL (M::'a::type word) (M'::'a::type word) f::'a::type list => 'b::type.
|
|
192 |
M = M' &
|
|
193 |
(ALL a::'a::type list.
|
|
194 |
M' = WORD a --> f a = (f'::'a::type list => 'b::type) a) -->
|
14516
|
195 |
word_case f M = word_case f' M'"
|
|
196 |
by (import word_base word_case_cong)
|
|
197 |
|
17644
|
198 |
lemma word_nchotomy: "ALL x::'a::type word. EX l::'a::type list. x = WORD l"
|
14516
|
199 |
by (import word_base word_nchotomy)
|
|
200 |
|
17644
|
201 |
lemma word_Axiom: "ALL f::'a::type list => 'b::type.
|
|
202 |
EX fn::'a::type word => 'b::type. ALL a::'a::type list. fn (WORD a) = f a"
|
14516
|
203 |
by (import word_base word_Axiom)
|
|
204 |
|
17644
|
205 |
lemma word_induction: "ALL P::'a::type word => bool. (ALL a::'a::type list. P (WORD a)) --> All P"
|
14516
|
206 |
by (import word_base word_induction)
|
|
207 |
|
17644
|
208 |
lemma word_Ax: "ALL f::'a::type list => 'b::type.
|
|
209 |
EX fn::'a::type word => 'b::type. ALL a::'a::type list. fn (WORD a) = f a"
|
14516
|
210 |
by (import word_base word_Ax)
|
|
211 |
|
17644
|
212 |
lemma WORD_11: "ALL (x::'a::type list) xa::'a::type list. (WORD x = WORD xa) = (x = xa)"
|
14516
|
213 |
by (import word_base WORD_11)
|
|
214 |
|
17644
|
215 |
lemma word_induct: "ALL x::'a::type word => bool. (ALL l::'a::type list. x (WORD l)) --> All x"
|
14516
|
216 |
by (import word_base word_induct)
|
|
217 |
|
17644
|
218 |
lemma word_cases: "ALL x::'a::type word. EX l::'a::type list. x = WORD l"
|
14516
|
219 |
by (import word_base word_cases)
|
|
220 |
|
|
221 |
consts
|
17652
|
222 |
WORDLEN :: "'a word => nat"
|
14516
|
223 |
|
17644
|
224 |
specification (WORDLEN) WORDLEN_DEF: "ALL l::'a::type list. WORDLEN (WORD l) = length l"
|
14516
|
225 |
by (import word_base WORDLEN_DEF)
|
|
226 |
|
|
227 |
consts
|
17652
|
228 |
PWORDLEN :: "nat => 'a word => bool"
|
14516
|
229 |
|
|
230 |
defs
|
17644
|
231 |
PWORDLEN_primdef: "PWORDLEN == %n::nat. GSPEC (%w::'a::type word. (w, WORDLEN w = n))"
|
14516
|
232 |
|
17644
|
233 |
lemma PWORDLEN_def: "ALL n::nat. PWORDLEN n = GSPEC (%w::'a::type word. (w, WORDLEN w = n))"
|
14516
|
234 |
by (import word_base PWORDLEN_def)
|
|
235 |
|
17644
|
236 |
lemma IN_PWORDLEN: "ALL (n::nat) l::'a::type list. IN (WORD l) (PWORDLEN n) = (length l = n)"
|
14516
|
237 |
by (import word_base IN_PWORDLEN)
|
|
238 |
|
17644
|
239 |
lemma PWORDLEN: "ALL (n::nat) w::'a::type word. IN w (PWORDLEN n) = (WORDLEN w = n)"
|
14516
|
240 |
by (import word_base PWORDLEN)
|
|
241 |
|
17652
|
242 |
lemma PWORDLEN0: "ALL w::'a::type word. IN w (PWORDLEN 0) --> w = WORD []"
|
14516
|
243 |
by (import word_base PWORDLEN0)
|
|
244 |
|
17652
|
245 |
lemma PWORDLEN1: "ALL x::'a::type. IN (WORD [x]) (PWORDLEN 1)"
|
14516
|
246 |
by (import word_base PWORDLEN1)
|
|
247 |
|
|
248 |
consts
|
17652
|
249 |
WSEG :: "nat => nat => 'a word => 'a word"
|
14516
|
250 |
|
17644
|
251 |
specification (WSEG) WSEG_DEF: "ALL (m::nat) (k::nat) l::'a::type list.
|
|
252 |
WSEG m k (WORD l) = WORD (LASTN m (BUTLASTN k l))"
|
14516
|
253 |
by (import word_base WSEG_DEF)
|
|
254 |
|
17652
|
255 |
lemma WSEG0: "ALL (k::nat) w::'a::type word. WSEG 0 k w = WORD []"
|
14516
|
256 |
by (import word_base WSEG0)
|
|
257 |
|
17644
|
258 |
lemma WSEG_PWORDLEN: "ALL n::nat.
|
14516
|
259 |
RES_FORALL (PWORDLEN n)
|
17644
|
260 |
(%w::'a::type word.
|
|
261 |
ALL (m::nat) k::nat. m + k <= n --> IN (WSEG m k w) (PWORDLEN m))"
|
14516
|
262 |
by (import word_base WSEG_PWORDLEN)
|
|
263 |
|
17644
|
264 |
lemma WSEG_WORDLEN: "ALL x::nat.
|
14516
|
265 |
RES_FORALL (PWORDLEN x)
|
17644
|
266 |
(%xa::'a::type word.
|
|
267 |
ALL (xb::nat) xc::nat.
|
|
268 |
xb + xc <= x --> WORDLEN (WSEG xb xc xa) = xb)"
|
14516
|
269 |
by (import word_base WSEG_WORDLEN)
|
|
270 |
|
17652
|
271 |
lemma WSEG_WORD_LENGTH: "ALL n::nat. RES_FORALL (PWORDLEN n) (%w::'a::type word. WSEG n 0 w = w)"
|
14516
|
272 |
by (import word_base WSEG_WORD_LENGTH)
|
|
273 |
|
|
274 |
consts
|
17652
|
275 |
bit :: "nat => 'a word => 'a"
|
14516
|
276 |
|
17644
|
277 |
specification (bit) BIT_DEF: "ALL (k::nat) l::'a::type list. bit k (WORD l) = ELL k l"
|
14516
|
278 |
by (import word_base BIT_DEF)
|
|
279 |
|
17652
|
280 |
lemma BIT0: "ALL x::'a::type. bit 0 (WORD [x]) = x"
|
14516
|
281 |
by (import word_base BIT0)
|
|
282 |
|
14847
|
283 |
lemma WSEG_BIT: "(All::(nat => bool) => bool)
|
|
284 |
(%n::nat.
|
17644
|
285 |
(RES_FORALL::('a::type word => bool)
|
|
286 |
=> ('a::type word => bool) => bool)
|
|
287 |
((PWORDLEN::nat => 'a::type word => bool) n)
|
|
288 |
(%w::'a::type word.
|
14847
|
289 |
(All::(nat => bool) => bool)
|
|
290 |
(%k::nat.
|
|
291 |
(op -->::bool => bool => bool)
|
|
292 |
((op <::nat => nat => bool) k n)
|
17644
|
293 |
((op =::'a::type word => 'a::type word => bool)
|
|
294 |
((WSEG::nat => nat => 'a::type word => 'a::type word)
|
|
295 |
(1::nat) k w)
|
|
296 |
((WORD::'a::type list => 'a::type word)
|
|
297 |
((op #::'a::type => 'a::type list => 'a::type list)
|
|
298 |
((bit::nat => 'a::type word => 'a::type) k w)
|
|
299 |
([]::'a::type list)))))))"
|
14516
|
300 |
by (import word_base WSEG_BIT)
|
|
301 |
|
17644
|
302 |
lemma BIT_WSEG: "ALL n::nat.
|
14516
|
303 |
RES_FORALL (PWORDLEN n)
|
17644
|
304 |
(%w::'a::type word.
|
|
305 |
ALL (m::nat) (k::nat) j::nat.
|
|
306 |
m + k <= n --> j < m --> bit j (WSEG m k w) = bit (j + k) w)"
|
14516
|
307 |
by (import word_base BIT_WSEG)
|
|
308 |
|
|
309 |
consts
|
17652
|
310 |
MSB :: "'a word => 'a"
|
14516
|
311 |
|
17644
|
312 |
specification (MSB) MSB_DEF: "ALL l::'a::type list. MSB (WORD l) = hd l"
|
14516
|
313 |
by (import word_base MSB_DEF)
|
|
314 |
|
17644
|
315 |
lemma MSB: "ALL n::nat.
|
|
316 |
RES_FORALL (PWORDLEN n)
|
17652
|
317 |
(%w::'a::type word. 0 < n --> MSB w = bit (PRE n) w)"
|
14516
|
318 |
by (import word_base MSB)
|
|
319 |
|
|
320 |
consts
|
17652
|
321 |
LSB :: "'a word => 'a"
|
14516
|
322 |
|
17644
|
323 |
specification (LSB) LSB_DEF: "ALL l::'a::type list. LSB (WORD l) = last l"
|
14516
|
324 |
by (import word_base LSB_DEF)
|
|
325 |
|
17644
|
326 |
lemma LSB: "ALL n::nat.
|
17652
|
327 |
RES_FORALL (PWORDLEN n) (%w::'a::type word. 0 < n --> LSB w = bit 0 w)"
|
14516
|
328 |
by (import word_base LSB)
|
|
329 |
|
|
330 |
consts
|
17652
|
331 |
WSPLIT :: "nat => 'a word => 'a word * 'a word"
|
14516
|
332 |
|
17644
|
333 |
specification (WSPLIT) WSPLIT_DEF: "ALL (m::nat) l::'a::type list.
|
|
334 |
WSPLIT m (WORD l) = (WORD (BUTLASTN m l), WORD (LASTN m l))"
|
14516
|
335 |
by (import word_base WSPLIT_DEF)
|
|
336 |
|
|
337 |
consts
|
17652
|
338 |
WCAT :: "'a word * 'a word => 'a word"
|
14516
|
339 |
|
17644
|
340 |
specification (WCAT) WCAT_DEF: "ALL (l1::'a::type list) l2::'a::type list.
|
|
341 |
WCAT (WORD l1, WORD l2) = WORD (l1 @ l2)"
|
14516
|
342 |
by (import word_base WCAT_DEF)
|
|
343 |
|
14847
|
344 |
lemma WORD_PARTITION: "(op &::bool => bool => bool)
|
|
345 |
((All::(nat => bool) => bool)
|
|
346 |
(%n::nat.
|
17644
|
347 |
(RES_FORALL::('a::type word => bool)
|
|
348 |
=> ('a::type word => bool) => bool)
|
|
349 |
((PWORDLEN::nat => 'a::type word => bool) n)
|
|
350 |
(%w::'a::type word.
|
14847
|
351 |
(All::(nat => bool) => bool)
|
|
352 |
(%m::nat.
|
|
353 |
(op -->::bool => bool => bool)
|
|
354 |
((op <=::nat => nat => bool) m n)
|
17644
|
355 |
((op =::'a::type word => 'a::type word => bool)
|
|
356 |
((WCAT::'a::type word * 'a::type word => 'a::type word)
|
|
357 |
((WSPLIT::nat
|
|
358 |
=> 'a::type word
|
|
359 |
=> 'a::type word * 'a::type word)
|
|
360 |
m w))
|
14847
|
361 |
w)))))
|
|
362 |
((All::(nat => bool) => bool)
|
|
363 |
(%n::nat.
|
|
364 |
(All::(nat => bool) => bool)
|
|
365 |
(%m::nat.
|
17644
|
366 |
(RES_FORALL::('a::type word => bool)
|
|
367 |
=> ('a::type word => bool) => bool)
|
|
368 |
((PWORDLEN::nat => 'a::type word => bool) n)
|
|
369 |
(%w1::'a::type word.
|
|
370 |
(RES_FORALL::('a::type word => bool)
|
|
371 |
=> ('a::type word => bool) => bool)
|
|
372 |
((PWORDLEN::nat => 'a::type word => bool) m)
|
|
373 |
(%w2::'a::type word.
|
|
374 |
(op =::'a::type word * 'a::type word
|
|
375 |
=> 'a::type word * 'a::type word => bool)
|
|
376 |
((WSPLIT::nat
|
|
377 |
=> 'a::type word
|
|
378 |
=> 'a::type word * 'a::type word)
|
|
379 |
m ((WCAT::'a::type word * 'a::type word
|
|
380 |
=> 'a::type word)
|
|
381 |
((Pair::'a::type word
|
|
382 |
=> 'a::type word
|
|
383 |
=> 'a::type word * 'a::type word)
|
|
384 |
w1 w2)))
|
|
385 |
((Pair::'a::type word
|
|
386 |
=> 'a::type word
|
|
387 |
=> 'a::type word * 'a::type word)
|
|
388 |
w1 w2))))))"
|
14516
|
389 |
by (import word_base WORD_PARTITION)
|
|
390 |
|
17644
|
391 |
lemma WCAT_ASSOC: "ALL (w1::'a::type word) (w2::'a::type word) w3::'a::type word.
|
|
392 |
WCAT (w1, WCAT (w2, w3)) = WCAT (WCAT (w1, w2), w3)"
|
14516
|
393 |
by (import word_base WCAT_ASSOC)
|
|
394 |
|
17644
|
395 |
lemma WCAT0: "ALL w::'a::type word. WCAT (WORD [], w) = w & WCAT (w, WORD []) = w"
|
14516
|
396 |
by (import word_base WCAT0)
|
|
397 |
|
17644
|
398 |
lemma WCAT_11: "ALL (m::nat) n::nat.
|
14516
|
399 |
RES_FORALL (PWORDLEN m)
|
17644
|
400 |
(%wm1::'a::type word.
|
|
401 |
RES_FORALL (PWORDLEN m)
|
|
402 |
(%wm2::'a::type word.
|
|
403 |
RES_FORALL (PWORDLEN n)
|
|
404 |
(%wn1::'a::type word.
|
|
405 |
RES_FORALL (PWORDLEN n)
|
|
406 |
(%wn2::'a::type word.
|
|
407 |
(WCAT (wm1, wn1) = WCAT (wm2, wn2)) =
|
|
408 |
(wm1 = wm2 & wn1 = wn2)))))"
|
14516
|
409 |
by (import word_base WCAT_11)
|
|
410 |
|
14847
|
411 |
lemma WSPLIT_PWORDLEN: "(All::(nat => bool) => bool)
|
|
412 |
(%n::nat.
|
17644
|
413 |
(RES_FORALL::('a::type word => bool)
|
|
414 |
=> ('a::type word => bool) => bool)
|
|
415 |
((PWORDLEN::nat => 'a::type word => bool) n)
|
|
416 |
(%w::'a::type word.
|
14847
|
417 |
(All::(nat => bool) => bool)
|
|
418 |
(%m::nat.
|
|
419 |
(op -->::bool => bool => bool)
|
|
420 |
((op <=::nat => nat => bool) m n)
|
|
421 |
((op &::bool => bool => bool)
|
17644
|
422 |
((IN::'a::type word => ('a::type word => bool) => bool)
|
|
423 |
((fst::'a::type word * 'a::type word => 'a::type word)
|
|
424 |
((WSPLIT::nat
|
|
425 |
=> 'a::type word
|
|
426 |
=> 'a::type word * 'a::type word)
|
|
427 |
m w))
|
|
428 |
((PWORDLEN::nat => 'a::type word => bool)
|
14847
|
429 |
((op -::nat => nat => nat) n m)))
|
17644
|
430 |
((IN::'a::type word => ('a::type word => bool) => bool)
|
|
431 |
((snd::'a::type word * 'a::type word => 'a::type word)
|
|
432 |
((WSPLIT::nat
|
|
433 |
=> 'a::type word
|
|
434 |
=> 'a::type word * 'a::type word)
|
|
435 |
m w))
|
|
436 |
((PWORDLEN::nat => 'a::type word => bool) m))))))"
|
14516
|
437 |
by (import word_base WSPLIT_PWORDLEN)
|
|
438 |
|
17644
|
439 |
lemma WCAT_PWORDLEN: "ALL n1::nat.
|
14516
|
440 |
RES_FORALL (PWORDLEN n1)
|
17644
|
441 |
(%w1::'a::type word.
|
|
442 |
ALL n2::nat.
|
|
443 |
RES_FORALL (PWORDLEN n2)
|
|
444 |
(%w2::'a::type word. IN (WCAT (w1, w2)) (PWORDLEN (n1 + n2))))"
|
14516
|
445 |
by (import word_base WCAT_PWORDLEN)
|
|
446 |
|
17644
|
447 |
lemma WORDLEN_SUC_WCAT: "ALL (n::nat) w::'a::type word.
|
14516
|
448 |
IN w (PWORDLEN (Suc n)) -->
|
17652
|
449 |
RES_EXISTS (PWORDLEN 1)
|
17644
|
450 |
(%b::'a::type word.
|
|
451 |
RES_EXISTS (PWORDLEN n) (%w'::'a::type word. w = WCAT (b, w')))"
|
14516
|
452 |
by (import word_base WORDLEN_SUC_WCAT)
|
|
453 |
|
17644
|
454 |
lemma WSEG_WSEG: "ALL n::nat.
|
14516
|
455 |
RES_FORALL (PWORDLEN n)
|
17644
|
456 |
(%w::'a::type word.
|
|
457 |
ALL (m1::nat) (k1::nat) (m2::nat) k2::nat.
|
|
458 |
m1 + k1 <= n & m2 + k2 <= m1 -->
|
|
459 |
WSEG m2 k2 (WSEG m1 k1 w) = WSEG m2 (k1 + k2) w)"
|
14516
|
460 |
by (import word_base WSEG_WSEG)
|
|
461 |
|
14847
|
462 |
lemma WSPLIT_WSEG: "(All::(nat => bool) => bool)
|
|
463 |
(%n::nat.
|
17644
|
464 |
(RES_FORALL::('a::type word => bool)
|
|
465 |
=> ('a::type word => bool) => bool)
|
|
466 |
((PWORDLEN::nat => 'a::type word => bool) n)
|
|
467 |
(%w::'a::type word.
|
14847
|
468 |
(All::(nat => bool) => bool)
|
|
469 |
(%k::nat.
|
|
470 |
(op -->::bool => bool => bool)
|
|
471 |
((op <=::nat => nat => bool) k n)
|
17644
|
472 |
((op =::'a::type word * 'a::type word
|
|
473 |
=> 'a::type word * 'a::type word => bool)
|
|
474 |
((WSPLIT::nat
|
|
475 |
=> 'a::type word
|
|
476 |
=> 'a::type word * 'a::type word)
|
|
477 |
k w)
|
|
478 |
((Pair::'a::type word
|
|
479 |
=> 'a::type word => 'a::type word * 'a::type word)
|
|
480 |
((WSEG::nat => nat => 'a::type word => 'a::type word)
|
14847
|
481 |
((op -::nat => nat => nat) n k) k w)
|
17644
|
482 |
((WSEG::nat => nat => 'a::type word => 'a::type word) k
|
|
483 |
(0::nat) w))))))"
|
14516
|
484 |
by (import word_base WSPLIT_WSEG)
|
|
485 |
|
14847
|
486 |
lemma WSPLIT_WSEG1: "(All::(nat => bool) => bool)
|
|
487 |
(%n::nat.
|
17644
|
488 |
(RES_FORALL::('a::type word => bool)
|
|
489 |
=> ('a::type word => bool) => bool)
|
|
490 |
((PWORDLEN::nat => 'a::type word => bool) n)
|
|
491 |
(%w::'a::type word.
|
14847
|
492 |
(All::(nat => bool) => bool)
|
|
493 |
(%k::nat.
|
|
494 |
(op -->::bool => bool => bool)
|
|
495 |
((op <=::nat => nat => bool) k n)
|
17644
|
496 |
((op =::'a::type word => 'a::type word => bool)
|
|
497 |
((fst::'a::type word * 'a::type word => 'a::type word)
|
|
498 |
((WSPLIT::nat
|
|
499 |
=> 'a::type word
|
|
500 |
=> 'a::type word * 'a::type word)
|
|
501 |
k w))
|
|
502 |
((WSEG::nat => nat => 'a::type word => 'a::type word)
|
14847
|
503 |
((op -::nat => nat => nat) n k) k w)))))"
|
14516
|
504 |
by (import word_base WSPLIT_WSEG1)
|
|
505 |
|
14847
|
506 |
lemma WSPLIT_WSEG2: "(All::(nat => bool) => bool)
|
|
507 |
(%n::nat.
|
17644
|
508 |
(RES_FORALL::('a::type word => bool)
|
|
509 |
=> ('a::type word => bool) => bool)
|
|
510 |
((PWORDLEN::nat => 'a::type word => bool) n)
|
|
511 |
(%w::'a::type word.
|
14847
|
512 |
(All::(nat => bool) => bool)
|
|
513 |
(%k::nat.
|
|
514 |
(op -->::bool => bool => bool)
|
|
515 |
((op <=::nat => nat => bool) k n)
|
17644
|
516 |
((op =::'a::type word => 'a::type word => bool)
|
|
517 |
((snd::'a::type word * 'a::type word => 'a::type word)
|
|
518 |
((WSPLIT::nat
|
|
519 |
=> 'a::type word
|
|
520 |
=> 'a::type word * 'a::type word)
|
|
521 |
k w))
|
|
522 |
((WSEG::nat => nat => 'a::type word => 'a::type word) k
|
|
523 |
(0::nat) w)))))"
|
14516
|
524 |
by (import word_base WSPLIT_WSEG2)
|
|
525 |
|
17644
|
526 |
lemma WCAT_WSEG_WSEG: "ALL n::nat.
|
14516
|
527 |
RES_FORALL (PWORDLEN n)
|
17644
|
528 |
(%w::'a::type word.
|
|
529 |
ALL (m1::nat) (m2::nat) k::nat.
|
|
530 |
m1 + (m2 + k) <= n -->
|
|
531 |
WCAT (WSEG m2 (m1 + k) w, WSEG m1 k w) = WSEG (m1 + m2) k w)"
|
14516
|
532 |
by (import word_base WCAT_WSEG_WSEG)
|
|
533 |
|
17644
|
534 |
lemma WORD_SPLIT: "ALL (x::nat) xa::nat.
|
|
535 |
RES_FORALL (PWORDLEN (x + xa))
|
17652
|
536 |
(%w::'a::type word. w = WCAT (WSEG x xa w, WSEG xa 0 w))"
|
14516
|
537 |
by (import word_base WORD_SPLIT)
|
|
538 |
|
17644
|
539 |
lemma WORDLEN_SUC_WCAT_WSEG_WSEG: "RES_FORALL (PWORDLEN (Suc (n::nat)))
|
17652
|
540 |
(%w::'a::type word. w = WCAT (WSEG 1 n w, WSEG n 0 w))"
|
14516
|
541 |
by (import word_base WORDLEN_SUC_WCAT_WSEG_WSEG)
|
|
542 |
|
17644
|
543 |
lemma WORDLEN_SUC_WCAT_WSEG_WSEG_RIGHT: "RES_FORALL (PWORDLEN (Suc (n::nat)))
|
17652
|
544 |
(%w::'a::type word. w = WCAT (WSEG n 1 w, WSEG 1 0 w))"
|
14516
|
545 |
by (import word_base WORDLEN_SUC_WCAT_WSEG_WSEG_RIGHT)
|
|
546 |
|
17644
|
547 |
lemma WORDLEN_SUC_WCAT_BIT_WSEG: "ALL n::nat.
|
|
548 |
RES_FORALL (PWORDLEN (Suc n))
|
17652
|
549 |
(%w::'a::type word. w = WCAT (WORD [bit n w], WSEG n 0 w))"
|
14516
|
550 |
by (import word_base WORDLEN_SUC_WCAT_BIT_WSEG)
|
|
551 |
|
17644
|
552 |
lemma WORDLEN_SUC_WCAT_BIT_WSEG_RIGHT: "ALL n::nat.
|
|
553 |
RES_FORALL (PWORDLEN (Suc n))
|
17652
|
554 |
(%w::'a::type word. w = WCAT (WSEG n 1 w, WORD [bit 0 w]))"
|
14516
|
555 |
by (import word_base WORDLEN_SUC_WCAT_BIT_WSEG_RIGHT)
|
|
556 |
|
17644
|
557 |
lemma WSEG_WCAT1: "ALL (n1::nat) n2::nat.
|
14516
|
558 |
RES_FORALL (PWORDLEN n1)
|
17644
|
559 |
(%w1::'a::type word.
|
|
560 |
RES_FORALL (PWORDLEN n2)
|
|
561 |
(%w2::'a::type word. WSEG n1 n2 (WCAT (w1, w2)) = w1))"
|
14516
|
562 |
by (import word_base WSEG_WCAT1)
|
|
563 |
|
17644
|
564 |
lemma WSEG_WCAT2: "ALL (n1::nat) n2::nat.
|
14516
|
565 |
RES_FORALL (PWORDLEN n1)
|
17644
|
566 |
(%w1::'a::type word.
|
|
567 |
RES_FORALL (PWORDLEN n2)
|
17652
|
568 |
(%w2::'a::type word. WSEG n2 0 (WCAT (w1, w2)) = w2))"
|
14516
|
569 |
by (import word_base WSEG_WCAT2)
|
|
570 |
|
17644
|
571 |
lemma WSEG_SUC: "ALL n::nat.
|
14516
|
572 |
RES_FORALL (PWORDLEN n)
|
17644
|
573 |
(%w::'a::type word.
|
|
574 |
ALL (k::nat) m1::nat.
|
|
575 |
k + Suc m1 < n -->
|
17652
|
576 |
WSEG (Suc m1) k w = WCAT (WSEG 1 (k + m1) w, WSEG m1 k w))"
|
14516
|
577 |
by (import word_base WSEG_SUC)
|
|
578 |
|
17644
|
579 |
lemma WORD_CONS_WCAT: "ALL (x::'a::type) l::'a::type list. WORD (x # l) = WCAT (WORD [x], WORD l)"
|
14516
|
580 |
by (import word_base WORD_CONS_WCAT)
|
|
581 |
|
17644
|
582 |
lemma WORD_SNOC_WCAT: "ALL (l::'a::type list) x::'a::type.
|
|
583 |
WORD (SNOC x l) = WCAT (WORD l, WORD [x])"
|
14516
|
584 |
by (import word_base WORD_SNOC_WCAT)
|
|
585 |
|
17644
|
586 |
lemma BIT_WCAT_FST: "ALL (n1::nat) n2::nat.
|
14516
|
587 |
RES_FORALL (PWORDLEN n1)
|
17644
|
588 |
(%w1::'a::type word.
|
|
589 |
RES_FORALL (PWORDLEN n2)
|
|
590 |
(%w2::'a::type word.
|
|
591 |
ALL k::nat.
|
|
592 |
n2 <= k & k < n1 + n2 -->
|
|
593 |
bit k (WCAT (w1, w2)) = bit (k - n2) w1))"
|
14516
|
594 |
by (import word_base BIT_WCAT_FST)
|
|
595 |
|
14847
|
596 |
lemma BIT_WCAT_SND: "(All::(nat => bool) => bool)
|
|
597 |
(%n1::nat.
|
|
598 |
(All::(nat => bool) => bool)
|
|
599 |
(%n2::nat.
|
17644
|
600 |
(RES_FORALL::('a::type word => bool)
|
|
601 |
=> ('a::type word => bool) => bool)
|
|
602 |
((PWORDLEN::nat => 'a::type word => bool) n1)
|
|
603 |
(%w1::'a::type word.
|
|
604 |
(RES_FORALL::('a::type word => bool)
|
|
605 |
=> ('a::type word => bool) => bool)
|
|
606 |
((PWORDLEN::nat => 'a::type word => bool) n2)
|
|
607 |
(%w2::'a::type word.
|
14847
|
608 |
(All::(nat => bool) => bool)
|
|
609 |
(%k::nat.
|
|
610 |
(op -->::bool => bool => bool)
|
|
611 |
((op <::nat => nat => bool) k n2)
|
17644
|
612 |
((op =::'a::type => 'a::type => bool)
|
|
613 |
((bit::nat => 'a::type word => 'a::type) k
|
|
614 |
((WCAT::'a::type word * 'a::type word
|
|
615 |
=> 'a::type word)
|
|
616 |
((Pair::'a::type word
|
|
617 |
=> 'a::type word => 'a::type word * 'a::type word)
|
14847
|
618 |
w1 w2)))
|
17644
|
619 |
((bit::nat => 'a::type word => 'a::type) k
|
|
620 |
w2)))))))"
|
14516
|
621 |
by (import word_base BIT_WCAT_SND)
|
|
622 |
|
17644
|
623 |
lemma BIT_WCAT1: "ALL n::nat.
|
|
624 |
RES_FORALL (PWORDLEN n)
|
|
625 |
(%w::'a::type word. ALL b::'a::type. bit n (WCAT (WORD [b], w)) = b)"
|
14516
|
626 |
by (import word_base BIT_WCAT1)
|
|
627 |
|
17644
|
628 |
lemma WSEG_WCAT_WSEG1: "ALL (n1::nat) n2::nat.
|
14516
|
629 |
RES_FORALL (PWORDLEN n1)
|
17644
|
630 |
(%w1::'a::type word.
|
|
631 |
RES_FORALL (PWORDLEN n2)
|
|
632 |
(%w2::'a::type word.
|
|
633 |
ALL (m::nat) k::nat.
|
|
634 |
m <= n1 & n2 <= k -->
|
|
635 |
WSEG m k (WCAT (w1, w2)) = WSEG m (k - n2) w1))"
|
14516
|
636 |
by (import word_base WSEG_WCAT_WSEG1)
|
|
637 |
|
17644
|
638 |
lemma WSEG_WCAT_WSEG2: "ALL (n1::nat) n2::nat.
|
14516
|
639 |
RES_FORALL (PWORDLEN n1)
|
17644
|
640 |
(%w1::'a::type word.
|
|
641 |
RES_FORALL (PWORDLEN n2)
|
|
642 |
(%w2::'a::type word.
|
|
643 |
ALL (m::nat) k::nat.
|
|
644 |
m + k <= n2 --> WSEG m k (WCAT (w1, w2)) = WSEG m k w2))"
|
14516
|
645 |
by (import word_base WSEG_WCAT_WSEG2)
|
|
646 |
|
17644
|
647 |
lemma WSEG_WCAT_WSEG: "ALL (n1::nat) n2::nat.
|
14516
|
648 |
RES_FORALL (PWORDLEN n1)
|
17644
|
649 |
(%w1::'a::type word.
|
|
650 |
RES_FORALL (PWORDLEN n2)
|
|
651 |
(%w2::'a::type word.
|
|
652 |
ALL (m::nat) k::nat.
|
|
653 |
m + k <= n1 + n2 & k < n2 & n2 <= m + k -->
|
|
654 |
WSEG m k (WCAT (w1, w2)) =
|
17652
|
655 |
WCAT (WSEG (m + k - n2) 0 w1, WSEG (n2 - k) k w2)))"
|
14516
|
656 |
by (import word_base WSEG_WCAT_WSEG)
|
|
657 |
|
14847
|
658 |
lemma BIT_EQ_IMP_WORD_EQ: "(All::(nat => bool) => bool)
|
|
659 |
(%n::nat.
|
17644
|
660 |
(RES_FORALL::('a::type word => bool)
|
|
661 |
=> ('a::type word => bool) => bool)
|
|
662 |
((PWORDLEN::nat => 'a::type word => bool) n)
|
|
663 |
(%w1::'a::type word.
|
|
664 |
(RES_FORALL::('a::type word => bool)
|
|
665 |
=> ('a::type word => bool) => bool)
|
|
666 |
((PWORDLEN::nat => 'a::type word => bool) n)
|
|
667 |
(%w2::'a::type word.
|
14847
|
668 |
(op -->::bool => bool => bool)
|
|
669 |
((All::(nat => bool) => bool)
|
|
670 |
(%k::nat.
|
|
671 |
(op -->::bool => bool => bool)
|
|
672 |
((op <::nat => nat => bool) k n)
|
17644
|
673 |
((op =::'a::type => 'a::type => bool)
|
|
674 |
((bit::nat => 'a::type word => 'a::type) k w1)
|
|
675 |
((bit::nat => 'a::type word => 'a::type) k w2))))
|
|
676 |
((op =::'a::type word => 'a::type word => bool) w1 w2))))"
|
14516
|
677 |
by (import word_base BIT_EQ_IMP_WORD_EQ)
|
|
678 |
|
|
679 |
;end_setup
|
|
680 |
|
|
681 |
;setup_theory word_num
|
|
682 |
|
|
683 |
constdefs
|
17652
|
684 |
LVAL :: "('a => nat) => nat => 'a list => nat"
|
17644
|
685 |
"LVAL ==
|
17652
|
686 |
%(f::'a::type => nat) b::nat. foldl (%(e::nat) x::'a::type. b * e + f x) 0"
|
14516
|
687 |
|
17644
|
688 |
lemma LVAL_DEF: "ALL (f::'a::type => nat) (b::nat) l::'a::type list.
|
17652
|
689 |
LVAL f b l = foldl (%(e::nat) x::'a::type. b * e + f x) 0 l"
|
14516
|
690 |
by (import word_num LVAL_DEF)
|
|
691 |
|
|
692 |
consts
|
17652
|
693 |
NVAL :: "('a => nat) => nat => 'a word => nat"
|
14516
|
694 |
|
17644
|
695 |
specification (NVAL) NVAL_DEF: "ALL (f::'a::type => nat) (b::nat) l::'a::type list.
|
|
696 |
NVAL f b (WORD l) = LVAL f b l"
|
14516
|
697 |
by (import word_num NVAL_DEF)
|
|
698 |
|
17652
|
699 |
lemma LVAL: "(ALL (x::'a::type => nat) xa::nat. LVAL x xa [] = 0) &
|
17644
|
700 |
(ALL (x::'a::type list) (xa::'a::type => nat) (xb::nat) xc::'a::type.
|
14516
|
701 |
LVAL xa xb (xc # x) = xa xc * xb ^ length x + LVAL xa xb x)"
|
|
702 |
by (import word_num LVAL)
|
|
703 |
|
17644
|
704 |
lemma LVAL_SNOC: "ALL (l::'a::type list) (h::'a::type) (f::'a::type => nat) b::nat.
|
|
705 |
LVAL f b (SNOC h l) = LVAL f b l * b + f h"
|
14516
|
706 |
by (import word_num LVAL_SNOC)
|
|
707 |
|
17644
|
708 |
lemma LVAL_MAX: "ALL (l::'a::type list) (f::'a::type => nat) b::nat.
|
|
709 |
(ALL x::'a::type. f x < b) --> LVAL f b l < b ^ length l"
|
14516
|
710 |
by (import word_num LVAL_MAX)
|
|
711 |
|
17644
|
712 |
lemma NVAL_MAX: "ALL (f::'a::type => nat) b::nat.
|
|
713 |
(ALL x::'a::type. f x < b) -->
|
|
714 |
(ALL n::nat.
|
|
715 |
RES_FORALL (PWORDLEN n) (%w::'a::type word. NVAL f b w < b ^ n))"
|
14516
|
716 |
by (import word_num NVAL_MAX)
|
|
717 |
|
17652
|
718 |
lemma NVAL0: "ALL (x::'a::type => nat) xa::nat. NVAL x xa (WORD []) = 0"
|
14516
|
719 |
by (import word_num NVAL0)
|
|
720 |
|
17644
|
721 |
lemma NVAL1: "ALL (x::'a::type => nat) (xa::nat) xb::'a::type.
|
|
722 |
NVAL x xa (WORD [xb]) = x xb"
|
14516
|
723 |
by (import word_num NVAL1)
|
|
724 |
|
17652
|
725 |
lemma NVAL_WORDLEN_0: "RES_FORALL (PWORDLEN 0)
|
|
726 |
(%w::'a::type word. ALL (fv::'a::type => nat) r::nat. NVAL fv r w = 0)"
|
14516
|
727 |
by (import word_num NVAL_WORDLEN_0)
|
|
728 |
|
17644
|
729 |
lemma NVAL_WCAT1: "ALL (w::'a::type word) (f::'a::type => nat) (b::nat) x::'a::type.
|
|
730 |
NVAL f b (WCAT (w, WORD [x])) = NVAL f b w * b + f x"
|
14516
|
731 |
by (import word_num NVAL_WCAT1)
|
|
732 |
|
17644
|
733 |
lemma NVAL_WCAT2: "ALL n::nat.
|
14516
|
734 |
RES_FORALL (PWORDLEN n)
|
17644
|
735 |
(%w::'a::type word.
|
|
736 |
ALL (f::'a::type => nat) (b::nat) x::'a::type.
|
|
737 |
NVAL f b (WCAT (WORD [x], w)) = f x * b ^ n + NVAL f b w)"
|
14516
|
738 |
by (import word_num NVAL_WCAT2)
|
|
739 |
|
17644
|
740 |
lemma NVAL_WCAT: "ALL (n::nat) m::nat.
|
14516
|
741 |
RES_FORALL (PWORDLEN n)
|
17644
|
742 |
(%w1::'a::type word.
|
|
743 |
RES_FORALL (PWORDLEN m)
|
|
744 |
(%w2::'a::type word.
|
|
745 |
ALL (f::'a::type => nat) b::nat.
|
|
746 |
NVAL f b (WCAT (w1, w2)) =
|
|
747 |
NVAL f b w1 * b ^ m + NVAL f b w2))"
|
14516
|
748 |
by (import word_num NVAL_WCAT)
|
|
749 |
|
|
750 |
consts
|
17652
|
751 |
NLIST :: "nat => (nat => 'a) => nat => nat => 'a list"
|
14516
|
752 |
|
17652
|
753 |
specification (NLIST) NLIST_DEF: "(ALL (frep::nat => 'a::type) (b::nat) m::nat. NLIST 0 frep b m = []) &
|
17644
|
754 |
(ALL (n::nat) (frep::nat => 'a::type) (b::nat) m::nat.
|
14516
|
755 |
NLIST (Suc n) frep b m =
|
|
756 |
SNOC (frep (m mod b)) (NLIST n frep b (m div b)))"
|
|
757 |
by (import word_num NLIST_DEF)
|
|
758 |
|
|
759 |
constdefs
|
17652
|
760 |
NWORD :: "nat => (nat => 'a) => nat => nat => 'a word"
|
17644
|
761 |
"NWORD ==
|
|
762 |
%(n::nat) (frep::nat => 'a::type) (b::nat) m::nat. WORD (NLIST n frep b m)"
|
14516
|
763 |
|
17644
|
764 |
lemma NWORD_DEF: "ALL (n::nat) (frep::nat => 'a::type) (b::nat) m::nat.
|
|
765 |
NWORD n frep b m = WORD (NLIST n frep b m)"
|
14516
|
766 |
by (import word_num NWORD_DEF)
|
|
767 |
|
17644
|
768 |
lemma NWORD_LENGTH: "ALL (x::nat) (xa::nat => 'a::type) (xb::nat) xc::nat.
|
|
769 |
WORDLEN (NWORD x xa xb xc) = x"
|
14516
|
770 |
by (import word_num NWORD_LENGTH)
|
|
771 |
|
17644
|
772 |
lemma NWORD_PWORDLEN: "ALL (x::nat) (xa::nat => 'a::type) (xb::nat) xc::nat.
|
|
773 |
IN (NWORD x xa xb xc) (PWORDLEN x)"
|
14516
|
774 |
by (import word_num NWORD_PWORDLEN)
|
|
775 |
|
|
776 |
;end_setup
|
|
777 |
|
|
778 |
;setup_theory word_bitop
|
|
779 |
|
|
780 |
consts
|
17652
|
781 |
PBITOP :: "('a word => 'b word) => bool"
|
14516
|
782 |
|
|
783 |
defs
|
|
784 |
PBITOP_primdef: "PBITOP ==
|
|
785 |
GSPEC
|
17644
|
786 |
(%oper::'a::type word => 'b::type word.
|
14516
|
787 |
(oper,
|
17644
|
788 |
ALL n::nat.
|
14516
|
789 |
RES_FORALL (PWORDLEN n)
|
17644
|
790 |
(%w::'a::type word.
|
|
791 |
IN (oper w) (PWORDLEN n) &
|
|
792 |
(ALL (m::nat) k::nat.
|
|
793 |
m + k <= n --> oper (WSEG m k w) = WSEG m k (oper w)))))"
|
14516
|
794 |
|
|
795 |
lemma PBITOP_def: "PBITOP =
|
|
796 |
GSPEC
|
17644
|
797 |
(%oper::'a::type word => 'b::type word.
|
14516
|
798 |
(oper,
|
17644
|
799 |
ALL n::nat.
|
14516
|
800 |
RES_FORALL (PWORDLEN n)
|
17644
|
801 |
(%w::'a::type word.
|
|
802 |
IN (oper w) (PWORDLEN n) &
|
|
803 |
(ALL (m::nat) k::nat.
|
|
804 |
m + k <= n --> oper (WSEG m k w) = WSEG m k (oper w)))))"
|
14516
|
805 |
by (import word_bitop PBITOP_def)
|
|
806 |
|
17644
|
807 |
lemma IN_PBITOP: "ALL oper::'a::type word => 'b::type word.
|
14516
|
808 |
IN oper PBITOP =
|
17644
|
809 |
(ALL n::nat.
|
14516
|
810 |
RES_FORALL (PWORDLEN n)
|
17644
|
811 |
(%w::'a::type word.
|
|
812 |
IN (oper w) (PWORDLEN n) &
|
|
813 |
(ALL (m::nat) k::nat.
|
|
814 |
m + k <= n --> oper (WSEG m k w) = WSEG m k (oper w))))"
|
14516
|
815 |
by (import word_bitop IN_PBITOP)
|
|
816 |
|
|
817 |
lemma PBITOP_PWORDLEN: "RES_FORALL PBITOP
|
17644
|
818 |
(%oper::'a::type word => 'b::type word.
|
|
819 |
ALL n::nat.
|
|
820 |
RES_FORALL (PWORDLEN n)
|
|
821 |
(%w::'a::type word. IN (oper w) (PWORDLEN n)))"
|
14516
|
822 |
by (import word_bitop PBITOP_PWORDLEN)
|
|
823 |
|
|
824 |
lemma PBITOP_WSEG: "RES_FORALL PBITOP
|
17644
|
825 |
(%oper::'a::type word => 'b::type word.
|
|
826 |
ALL n::nat.
|
14516
|
827 |
RES_FORALL (PWORDLEN n)
|
17644
|
828 |
(%w::'a::type word.
|
|
829 |
ALL (m::nat) k::nat.
|
|
830 |
m + k <= n --> oper (WSEG m k w) = WSEG m k (oper w)))"
|
14516
|
831 |
by (import word_bitop PBITOP_WSEG)
|
|
832 |
|
17644
|
833 |
lemma PBITOP_BIT: "(RES_FORALL::(('a::type word => 'b::type word) => bool)
|
|
834 |
=> (('a::type word => 'b::type word) => bool) => bool)
|
|
835 |
(PBITOP::('a::type word => 'b::type word) => bool)
|
|
836 |
(%oper::'a::type word => 'b::type word.
|
14847
|
837 |
(All::(nat => bool) => bool)
|
|
838 |
(%n::nat.
|
17644
|
839 |
(RES_FORALL::('a::type word => bool)
|
|
840 |
=> ('a::type word => bool) => bool)
|
|
841 |
((PWORDLEN::nat => 'a::type word => bool) n)
|
|
842 |
(%w::'a::type word.
|
14847
|
843 |
(All::(nat => bool) => bool)
|
|
844 |
(%k::nat.
|
|
845 |
(op -->::bool => bool => bool)
|
|
846 |
((op <::nat => nat => bool) k n)
|
17644
|
847 |
((op =::'b::type word => 'b::type word => bool)
|
14847
|
848 |
(oper
|
17644
|
849 |
((WORD::'a::type list => 'a::type word)
|
|
850 |
((op #::'a::type
|
|
851 |
=> 'a::type list => 'a::type list)
|
|
852 |
((bit::nat => 'a::type word => 'a::type) k w)
|
|
853 |
([]::'a::type list))))
|
|
854 |
((WORD::'b::type list => 'b::type word)
|
|
855 |
((op #::'b::type => 'b::type list => 'b::type list)
|
|
856 |
((bit::nat => 'b::type word => 'b::type) k
|
|
857 |
(oper w))
|
|
858 |
([]::'b::type list))))))))"
|
14516
|
859 |
by (import word_bitop PBITOP_BIT)
|
|
860 |
|
|
861 |
consts
|
17652
|
862 |
PBITBOP :: "('a word => 'b word => 'c word) => bool"
|
14516
|
863 |
|
|
864 |
defs
|
|
865 |
PBITBOP_primdef: "PBITBOP ==
|
|
866 |
GSPEC
|
17644
|
867 |
(%oper::'a::type word => 'b::type word => 'c::type word.
|
14516
|
868 |
(oper,
|
17644
|
869 |
ALL n::nat.
|
14516
|
870 |
RES_FORALL (PWORDLEN n)
|
17644
|
871 |
(%w1::'a::type word.
|
|
872 |
RES_FORALL (PWORDLEN n)
|
|
873 |
(%w2::'b::type word.
|
|
874 |
IN (oper w1 w2) (PWORDLEN n) &
|
|
875 |
(ALL (m::nat) k::nat.
|
|
876 |
m + k <= n -->
|
|
877 |
oper (WSEG m k w1) (WSEG m k w2) =
|
|
878 |
WSEG m k (oper w1 w2))))))"
|
14516
|
879 |
|
|
880 |
lemma PBITBOP_def: "PBITBOP =
|
|
881 |
GSPEC
|
17644
|
882 |
(%oper::'a::type word => 'b::type word => 'c::type word.
|
14516
|
883 |
(oper,
|
17644
|
884 |
ALL n::nat.
|
14516
|
885 |
RES_FORALL (PWORDLEN n)
|
17644
|
886 |
(%w1::'a::type word.
|
|
887 |
RES_FORALL (PWORDLEN n)
|
|
888 |
(%w2::'b::type word.
|
|
889 |
IN (oper w1 w2) (PWORDLEN n) &
|
|
890 |
(ALL (m::nat) k::nat.
|
|
891 |
m + k <= n -->
|
|
892 |
oper (WSEG m k w1) (WSEG m k w2) =
|
|
893 |
WSEG m k (oper w1 w2))))))"
|
14516
|
894 |
by (import word_bitop PBITBOP_def)
|
|
895 |
|
17644
|
896 |
lemma IN_PBITBOP: "ALL oper::'a::type word => 'b::type word => 'c::type word.
|
14516
|
897 |
IN oper PBITBOP =
|
17644
|
898 |
(ALL n::nat.
|
14516
|
899 |
RES_FORALL (PWORDLEN n)
|
17644
|
900 |
(%w1::'a::type word.
|
|
901 |
RES_FORALL (PWORDLEN n)
|
|
902 |
(%w2::'b::type word.
|
|
903 |
IN (oper w1 w2) (PWORDLEN n) &
|
|
904 |
(ALL (m::nat) k::nat.
|
|
905 |
m + k <= n -->
|
|
906 |
oper (WSEG m k w1) (WSEG m k w2) =
|
|
907 |
WSEG m k (oper w1 w2)))))"
|
14516
|
908 |
by (import word_bitop IN_PBITBOP)
|
|
909 |
|
|
910 |
lemma PBITBOP_PWORDLEN: "RES_FORALL PBITBOP
|
17644
|
911 |
(%oper::'a::type word => 'b::type word => 'c::type word.
|
|
912 |
ALL n::nat.
|
14516
|
913 |
RES_FORALL (PWORDLEN n)
|
17644
|
914 |
(%w1::'a::type word.
|
|
915 |
RES_FORALL (PWORDLEN n)
|
|
916 |
(%w2::'b::type word. IN (oper w1 w2) (PWORDLEN n))))"
|
14516
|
917 |
by (import word_bitop PBITBOP_PWORDLEN)
|
|
918 |
|
|
919 |
lemma PBITBOP_WSEG: "RES_FORALL PBITBOP
|
17644
|
920 |
(%oper::'a::type word => 'b::type word => 'c::type word.
|
|
921 |
ALL n::nat.
|
14516
|
922 |
RES_FORALL (PWORDLEN n)
|
17644
|
923 |
(%w1::'a::type word.
|
|
924 |
RES_FORALL (PWORDLEN n)
|
|
925 |
(%w2::'b::type word.
|
|
926 |
ALL (m::nat) k::nat.
|
|
927 |
m + k <= n -->
|
|
928 |
oper (WSEG m k w1) (WSEG m k w2) =
|
|
929 |
WSEG m k (oper w1 w2))))"
|
14516
|
930 |
by (import word_bitop PBITBOP_WSEG)
|
|
931 |
|
17644
|
932 |
lemma PBITBOP_EXISTS: "ALL f::'a::type => 'b::type => 'c::type.
|
|
933 |
EX x::'a::type word => 'b::type word => 'c::type word.
|
|
934 |
ALL (l1::'a::type list) l2::'b::type list.
|
|
935 |
x (WORD l1) (WORD l2) = WORD (map2 f l1 l2)"
|
14516
|
936 |
by (import word_bitop PBITBOP_EXISTS)
|
|
937 |
|
|
938 |
consts
|
17652
|
939 |
WMAP :: "('a => 'b) => 'a word => 'b word"
|
14516
|
940 |
|
17644
|
941 |
specification (WMAP) WMAP_DEF: "ALL (f::'a::type => 'b::type) l::'a::type list.
|
|
942 |
WMAP f (WORD l) = WORD (map f l)"
|
14516
|
943 |
by (import word_bitop WMAP_DEF)
|
|
944 |
|
17644
|
945 |
lemma WMAP_PWORDLEN: "RES_FORALL (PWORDLEN (n::nat))
|
|
946 |
(%w::'a::type word.
|
|
947 |
ALL f::'a::type => 'b::type. IN (WMAP f w) (PWORDLEN n))"
|
14516
|
948 |
by (import word_bitop WMAP_PWORDLEN)
|
|
949 |
|
17644
|
950 |
lemma WMAP_0: "ALL x::'a::type => 'b::type. WMAP x (WORD []) = WORD []"
|
14516
|
951 |
by (import word_bitop WMAP_0)
|
|
952 |
|
14847
|
953 |
lemma WMAP_BIT: "(All::(nat => bool) => bool)
|
|
954 |
(%n::nat.
|
17644
|
955 |
(RES_FORALL::('a::type word => bool)
|
|
956 |
=> ('a::type word => bool) => bool)
|
|
957 |
((PWORDLEN::nat => 'a::type word => bool) n)
|
|
958 |
(%w::'a::type word.
|
14847
|
959 |
(All::(nat => bool) => bool)
|
|
960 |
(%k::nat.
|
|
961 |
(op -->::bool => bool => bool)
|
|
962 |
((op <::nat => nat => bool) k n)
|
17644
|
963 |
((All::(('a::type => 'b::type) => bool) => bool)
|
|
964 |
(%f::'a::type => 'b::type.
|
|
965 |
(op =::'b::type => 'b::type => bool)
|
|
966 |
((bit::nat => 'b::type word => 'b::type) k
|
|
967 |
((WMAP::('a::type => 'b::type)
|
|
968 |
=> 'a::type word => 'b::type word)
|
|
969 |
f w))
|
|
970 |
(f ((bit::nat => 'a::type word => 'a::type) k
|
|
971 |
w)))))))"
|
14516
|
972 |
by (import word_bitop WMAP_BIT)
|
|
973 |
|
17644
|
974 |
lemma WMAP_WSEG: "ALL n::nat.
|
14516
|
975 |
RES_FORALL (PWORDLEN n)
|
17644
|
976 |
(%w::'a::type word.
|
|
977 |
ALL (m::nat) k::nat.
|
|
978 |
m + k <= n -->
|
|
979 |
(ALL f::'a::type => 'b::type.
|
|
980 |
WMAP f (WSEG m k w) = WSEG m k (WMAP f w)))"
|
14516
|
981 |
by (import word_bitop WMAP_WSEG)
|
|
982 |
|
17644
|
983 |
lemma WMAP_PBITOP: "ALL f::'a::type => 'b::type. IN (WMAP f) PBITOP"
|
14516
|
984 |
by (import word_bitop WMAP_PBITOP)
|
|
985 |
|
17644
|
986 |
lemma WMAP_WCAT: "ALL (w1::'a::type word) (w2::'a::type word) f::'a::type => 'b::type.
|
|
987 |
WMAP f (WCAT (w1, w2)) = WCAT (WMAP f w1, WMAP f w2)"
|
14516
|
988 |
by (import word_bitop WMAP_WCAT)
|
|
989 |
|
17644
|
990 |
lemma WMAP_o: "ALL (w::'a::type word) (f::'a::type => 'b::type) g::'b::type => 'c::type.
|
|
991 |
WMAP g (WMAP f w) = WMAP (g o f) w"
|
14516
|
992 |
by (import word_bitop WMAP_o)
|
|
993 |
|
|
994 |
consts
|
17652
|
995 |
FORALLBITS :: "('a => bool) => 'a word => bool"
|
14516
|
996 |
|
17644
|
997 |
specification (FORALLBITS) FORALLBITS_DEF: "ALL (P::'a::type => bool) l::'a::type list.
|
|
998 |
FORALLBITS P (WORD l) = list_all P l"
|
14516
|
999 |
by (import word_bitop FORALLBITS_DEF)
|
|
1000 |
|
14847
|
1001 |
lemma FORALLBITS: "(All::(nat => bool) => bool)
|
|
1002 |
(%n::nat.
|
17644
|
1003 |
(RES_FORALL::('a::type word => bool)
|
|
1004 |
=> ('a::type word => bool) => bool)
|
|
1005 |
((PWORDLEN::nat => 'a::type word => bool) n)
|
|
1006 |
(%w::'a::type word.
|
|
1007 |
(All::(('a::type => bool) => bool) => bool)
|
|
1008 |
(%P::'a::type => bool.
|
14847
|
1009 |
(op =::bool => bool => bool)
|
17644
|
1010 |
((FORALLBITS::('a::type => bool) => 'a::type word => bool) P
|
|
1011 |
w)
|
14847
|
1012 |
((All::(nat => bool) => bool)
|
|
1013 |
(%k::nat.
|
|
1014 |
(op -->::bool => bool => bool)
|
|
1015 |
((op <::nat => nat => bool) k n)
|
17644
|
1016 |
(P ((bit::nat => 'a::type word => 'a::type) k
|
|
1017 |
w)))))))"
|
14516
|
1018 |
by (import word_bitop FORALLBITS)
|
|
1019 |
|
17644
|
1020 |
lemma FORALLBITS_WSEG: "ALL n::nat.
|
14516
|
1021 |
RES_FORALL (PWORDLEN n)
|
17644
|
1022 |
(%w::'a::type word.
|
|
1023 |
ALL P::'a::type => bool.
|
|
1024 |
FORALLBITS P w -->
|
|
1025 |
(ALL (m::nat) k::nat. m + k <= n --> FORALLBITS P (WSEG m k w)))"
|
14516
|
1026 |
by (import word_bitop FORALLBITS_WSEG)
|
|
1027 |
|
17644
|
1028 |
lemma FORALLBITS_WCAT: "ALL (w1::'a::type word) (w2::'a::type word) P::'a::type => bool.
|
14516
|
1029 |
FORALLBITS P (WCAT (w1, w2)) = (FORALLBITS P w1 & FORALLBITS P w2)"
|
|
1030 |
by (import word_bitop FORALLBITS_WCAT)
|
|
1031 |
|
|
1032 |
consts
|
17652
|
1033 |
EXISTSABIT :: "('a => bool) => 'a word => bool"
|
14516
|
1034 |
|
17644
|
1035 |
specification (EXISTSABIT) EXISTSABIT_DEF: "ALL (P::'a::type => bool) l::'a::type list.
|
|
1036 |
EXISTSABIT P (WORD l) = list_exists P l"
|
14516
|
1037 |
by (import word_bitop EXISTSABIT_DEF)
|
|
1038 |
|
17644
|
1039 |
lemma NOT_EXISTSABIT: "ALL (P::'a::type => bool) w::'a::type word.
|
|
1040 |
(~ EXISTSABIT P w) = FORALLBITS (Not o P) w"
|
14516
|
1041 |
by (import word_bitop NOT_EXISTSABIT)
|
|
1042 |
|
17644
|
1043 |
lemma NOT_FORALLBITS: "ALL (P::'a::type => bool) w::'a::type word.
|
|
1044 |
(~ FORALLBITS P w) = EXISTSABIT (Not o P) w"
|
14516
|
1045 |
by (import word_bitop NOT_FORALLBITS)
|
|
1046 |
|
14847
|
1047 |
lemma EXISTSABIT: "(All::(nat => bool) => bool)
|
|
1048 |
(%n::nat.
|
17644
|
1049 |
(RES_FORALL::('a::type word => bool)
|
|
1050 |
=> ('a::type word => bool) => bool)
|
|
1051 |
((PWORDLEN::nat => 'a::type word => bool) n)
|
|
1052 |
(%w::'a::type word.
|
|
1053 |
(All::(('a::type => bool) => bool) => bool)
|
|
1054 |
(%P::'a::type => bool.
|
14847
|
1055 |
(op =::bool => bool => bool)
|
17644
|
1056 |
((EXISTSABIT::('a::type => bool) => 'a::type word => bool) P
|
|
1057 |
w)
|
14847
|
1058 |
((Ex::(nat => bool) => bool)
|
|
1059 |
(%k::nat.
|
|
1060 |
(op &::bool => bool => bool)
|
|
1061 |
((op <::nat => nat => bool) k n)
|
17644
|
1062 |
(P ((bit::nat => 'a::type word => 'a::type) k
|
|
1063 |
w)))))))"
|
14516
|
1064 |
by (import word_bitop EXISTSABIT)
|
|
1065 |
|
17644
|
1066 |
lemma EXISTSABIT_WSEG: "ALL n::nat.
|
14516
|
1067 |
RES_FORALL (PWORDLEN n)
|
17644
|
1068 |
(%w::'a::type word.
|
|
1069 |
ALL (m::nat) k::nat.
|
|
1070 |
m + k <= n -->
|
|
1071 |
(ALL P::'a::type => bool.
|
|
1072 |
EXISTSABIT P (WSEG m k w) --> EXISTSABIT P w))"
|
14516
|
1073 |
by (import word_bitop EXISTSABIT_WSEG)
|
|
1074 |
|
17644
|
1075 |
lemma EXISTSABIT_WCAT: "ALL (w1::'a::type word) (w2::'a::type word) P::'a::type => bool.
|
14516
|
1076 |
EXISTSABIT P (WCAT (w1, w2)) = (EXISTSABIT P w1 | EXISTSABIT P w2)"
|
|
1077 |
by (import word_bitop EXISTSABIT_WCAT)
|
|
1078 |
|
|
1079 |
constdefs
|
17652
|
1080 |
SHR :: "bool => 'a => 'a word => 'a word * 'a"
|
14516
|
1081 |
"SHR ==
|
17644
|
1082 |
%(f::bool) (b::'a::type) w::'a::type word.
|
14516
|
1083 |
(WCAT
|
17652
|
1084 |
(if f then WSEG 1 (PRE (WORDLEN w)) w else WORD [b],
|
|
1085 |
WSEG (PRE (WORDLEN w)) 1 w),
|
|
1086 |
bit 0 w)"
|
14516
|
1087 |
|
17644
|
1088 |
lemma SHR_DEF: "ALL (f::bool) (b::'a::type) w::'a::type word.
|
14516
|
1089 |
SHR f b w =
|
|
1090 |
(WCAT
|
17652
|
1091 |
(if f then WSEG 1 (PRE (WORDLEN w)) w else WORD [b],
|
|
1092 |
WSEG (PRE (WORDLEN w)) 1 w),
|
|
1093 |
bit 0 w)"
|
14516
|
1094 |
by (import word_bitop SHR_DEF)
|
|
1095 |
|
|
1096 |
constdefs
|
17652
|
1097 |
SHL :: "bool => 'a word => 'a => 'a * 'a word"
|
14516
|
1098 |
"SHL ==
|
17644
|
1099 |
%(f::bool) (w::'a::type word) b::'a::type.
|
14516
|
1100 |
(bit (PRE (WORDLEN w)) w,
|
17652
|
1101 |
WCAT (WSEG (PRE (WORDLEN w)) 0 w, if f then WSEG 1 0 w else WORD [b]))"
|
14516
|
1102 |
|
17644
|
1103 |
lemma SHL_DEF: "ALL (f::bool) (w::'a::type word) b::'a::type.
|
14516
|
1104 |
SHL f w b =
|
|
1105 |
(bit (PRE (WORDLEN w)) w,
|
17652
|
1106 |
WCAT (WSEG (PRE (WORDLEN w)) 0 w, if f then WSEG 1 0 w else WORD [b]))"
|
14516
|
1107 |
by (import word_bitop SHL_DEF)
|
|
1108 |
|
17644
|
1109 |
lemma SHR_WSEG: "ALL n::nat.
|
14516
|
1110 |
RES_FORALL (PWORDLEN n)
|
17644
|
1111 |
(%w::'a::type word.
|
|
1112 |
ALL (m::nat) k::nat.
|
|
1113 |
m + k <= n -->
|
17652
|
1114 |
0 < m -->
|
17644
|
1115 |
(ALL (f::bool) b::'a::type.
|
|
1116 |
SHR f b (WSEG m k w) =
|
|
1117 |
(if f
|
17652
|
1118 |
then WCAT (WSEG 1 (k + (m - 1)) w, WSEG (m - 1) (k + 1) w)
|
|
1119 |
else WCAT (WORD [b], WSEG (m - 1) (k + 1) w),
|
17644
|
1120 |
bit k w)))"
|
14516
|
1121 |
by (import word_bitop SHR_WSEG)
|
|
1122 |
|
17644
|
1123 |
lemma SHR_WSEG_1F: "ALL n::nat.
|
14516
|
1124 |
RES_FORALL (PWORDLEN n)
|
17644
|
1125 |
(%w::'a::type word.
|
|
1126 |
ALL (b::'a::type) (m::nat) k::nat.
|
|
1127 |
m + k <= n -->
|
17652
|
1128 |
0 < m -->
|
17644
|
1129 |
SHR False b (WSEG m k w) =
|
17652
|
1130 |
(WCAT (WORD [b], WSEG (m - 1) (k + 1) w), bit k w))"
|
14516
|
1131 |
by (import word_bitop SHR_WSEG_1F)
|
|
1132 |
|
17644
|
1133 |
lemma SHR_WSEG_NF: "ALL n::nat.
|
14516
|
1134 |
RES_FORALL (PWORDLEN n)
|
17644
|
1135 |
(%w::'a::type word.
|
|
1136 |
ALL (m::nat) k::nat.
|
|
1137 |
m + k < n -->
|
17652
|
1138 |
0 < m -->
|
17644
|
1139 |
SHR False (bit (m + k) w) (WSEG m k w) =
|
17652
|
1140 |
(WSEG m (k + 1) w, bit k w))"
|
14516
|
1141 |
by (import word_bitop SHR_WSEG_NF)
|
|
1142 |
|
17644
|
1143 |
lemma SHL_WSEG: "ALL n::nat.
|
14516
|
1144 |
RES_FORALL (PWORDLEN n)
|
17644
|
1145 |
(%w::'a::type word.
|
|
1146 |
ALL (m::nat) k::nat.
|
|
1147 |
m + k <= n -->
|
17652
|
1148 |
0 < m -->
|
17644
|
1149 |
(ALL (f::bool) b::'a::type.
|
|
1150 |
SHL f (WSEG m k w) b =
|
17652
|
1151 |
(bit (k + (m - 1)) w,
|
|
1152 |
if f then WCAT (WSEG (m - 1) k w, WSEG 1 k w)
|
|
1153 |
else WCAT (WSEG (m - 1) k w, WORD [b]))))"
|
14516
|
1154 |
by (import word_bitop SHL_WSEG)
|
|
1155 |
|
17644
|
1156 |
lemma SHL_WSEG_1F: "ALL n::nat.
|
14516
|
1157 |
RES_FORALL (PWORDLEN n)
|
17644
|
1158 |
(%w::'a::type word.
|
|
1159 |
ALL (b::'a::type) (m::nat) k::nat.
|
|
1160 |
m + k <= n -->
|
17652
|
1161 |
0 < m -->
|
17644
|
1162 |
SHL False (WSEG m k w) b =
|
17652
|
1163 |
(bit (k + (m - 1)) w, WCAT (WSEG (m - 1) k w, WORD [b])))"
|
14516
|
1164 |
by (import word_bitop SHL_WSEG_1F)
|
|
1165 |
|
17644
|
1166 |
lemma SHL_WSEG_NF: "ALL n::nat.
|
14516
|
1167 |
RES_FORALL (PWORDLEN n)
|
17644
|
1168 |
(%w::'a::type word.
|
|
1169 |
ALL (m::nat) k::nat.
|
|
1170 |
m + k <= n -->
|
17652
|
1171 |
0 < m -->
|
|
1172 |
0 < k -->
|
|
1173 |
SHL False (WSEG m k w) (bit (k - 1) w) =
|
|
1174 |
(bit (k + (m - 1)) w, WSEG m (k - 1) w))"
|
14516
|
1175 |
by (import word_bitop SHL_WSEG_NF)
|
|
1176 |
|
17644
|
1177 |
lemma WSEG_SHL: "ALL n::nat.
|
14516
|
1178 |
RES_FORALL (PWORDLEN (Suc n))
|
17644
|
1179 |
(%w::'a::type word.
|
|
1180 |
ALL (m::nat) k::nat.
|
17652
|
1181 |
0 < k & m + k <= Suc n -->
|
17644
|
1182 |
(ALL b::'a::type.
|
17652
|
1183 |
WSEG m k (snd (SHL (f::bool) w b)) = WSEG m (k - 1) w))"
|
14516
|
1184 |
by (import word_bitop WSEG_SHL)
|
|
1185 |
|
17644
|
1186 |
lemma WSEG_SHL_0: "ALL n::nat.
|
14516
|
1187 |
RES_FORALL (PWORDLEN (Suc n))
|
17644
|
1188 |
(%w::'a::type word.
|
|
1189 |
ALL (m::nat) b::'a::type.
|
17652
|
1190 |
0 < m & m <= Suc n -->
|
|
1191 |
WSEG m 0 (snd (SHL (f::bool) w b)) =
|
|
1192 |
WCAT (WSEG (m - 1) 0 w, if f then WSEG 1 0 w else WORD [b]))"
|
14516
|
1193 |
by (import word_bitop WSEG_SHL_0)
|
|
1194 |
|
|
1195 |
;end_setup
|
|
1196 |
|
|
1197 |
;setup_theory bword_num
|
|
1198 |
|
|
1199 |
constdefs
|
|
1200 |
BV :: "bool => nat"
|
17652
|
1201 |
"BV == %b::bool. if b then Suc 0 else 0"
|
14516
|
1202 |
|
17652
|
1203 |
lemma BV_DEF: "ALL b::bool. BV b = (if b then Suc 0 else 0)"
|
14516
|
1204 |
by (import bword_num BV_DEF)
|
|
1205 |
|
|
1206 |
consts
|
|
1207 |
BNVAL :: "bool word => nat"
|
|
1208 |
|
17652
|
1209 |
specification (BNVAL) BNVAL_DEF: "ALL l::bool list. BNVAL (WORD l) = LVAL BV 2 l"
|
14516
|
1210 |
by (import bword_num BNVAL_DEF)
|
|
1211 |
|
17652
|
1212 |
lemma BV_LESS_2: "ALL x::bool. BV x < 2"
|
14516
|
1213 |
by (import bword_num BV_LESS_2)
|
|
1214 |
|
17652
|
1215 |
lemma BNVAL_NVAL: "ALL w::bool word. BNVAL w = NVAL BV 2 w"
|
14516
|
1216 |
by (import bword_num BNVAL_NVAL)
|
|
1217 |
|
17652
|
1218 |
lemma BNVAL0: "BNVAL (WORD []) = 0"
|
14516
|
1219 |
by (import bword_num BNVAL0)
|
|
1220 |
|
17644
|
1221 |
lemma BNVAL_11: "ALL (w1::bool word) w2::bool word.
|
|
1222 |
WORDLEN w1 = WORDLEN w2 --> BNVAL w1 = BNVAL w2 --> w1 = w2"
|
14516
|
1223 |
by (import bword_num BNVAL_11)
|
|
1224 |
|
17644
|
1225 |
lemma BNVAL_ONTO: "ALL w::bool word. Ex (op = (BNVAL w))"
|
14516
|
1226 |
by (import bword_num BNVAL_ONTO)
|
|
1227 |
|
17652
|
1228 |
lemma BNVAL_MAX: "ALL n::nat. RES_FORALL (PWORDLEN n) (%w::bool word. BNVAL w < 2 ^ n)"
|
14516
|
1229 |
by (import bword_num BNVAL_MAX)
|
|
1230 |
|
17644
|
1231 |
lemma BNVAL_WCAT1: "ALL n::nat.
|
14516
|
1232 |
RES_FORALL (PWORDLEN n)
|
17644
|
1233 |
(%w::bool word.
|
17652
|
1234 |
ALL x::bool. BNVAL (WCAT (w, WORD [x])) = BNVAL w * 2 + BV x)"
|
14516
|
1235 |
by (import bword_num BNVAL_WCAT1)
|
|
1236 |
|
17644
|
1237 |
lemma BNVAL_WCAT2: "ALL n::nat.
|
14516
|
1238 |
RES_FORALL (PWORDLEN n)
|
17644
|
1239 |
(%w::bool word.
|
17652
|
1240 |
ALL x::bool. BNVAL (WCAT (WORD [x], w)) = BV x * 2 ^ n + BNVAL w)"
|
14516
|
1241 |
by (import bword_num BNVAL_WCAT2)
|
|
1242 |
|
17644
|
1243 |
lemma BNVAL_WCAT: "ALL (n::nat) m::nat.
|
14516
|
1244 |
RES_FORALL (PWORDLEN n)
|
17644
|
1245 |
(%w1::bool word.
|
|
1246 |
RES_FORALL (PWORDLEN m)
|
|
1247 |
(%w2::bool word.
|
17652
|
1248 |
BNVAL (WCAT (w1, w2)) = BNVAL w1 * 2 ^ m + BNVAL w2))"
|
14516
|
1249 |
by (import bword_num BNVAL_WCAT)
|
|
1250 |
|
|
1251 |
constdefs
|
|
1252 |
VB :: "nat => bool"
|
17652
|
1253 |
"VB == %n::nat. n mod 2 ~= 0"
|
14516
|
1254 |
|
17652
|
1255 |
lemma VB_DEF: "ALL n::nat. VB n = (n mod 2 ~= 0)"
|
14516
|
1256 |
by (import bword_num VB_DEF)
|
|
1257 |
|
|
1258 |
constdefs
|
|
1259 |
NBWORD :: "nat => nat => bool word"
|
17652
|
1260 |
"NBWORD == %(n::nat) m::nat. WORD (NLIST n VB 2 m)"
|
14516
|
1261 |
|
17652
|
1262 |
lemma NBWORD_DEF: "ALL (n::nat) m::nat. NBWORD n m = WORD (NLIST n VB 2 m)"
|
14516
|
1263 |
by (import bword_num NBWORD_DEF)
|
|
1264 |
|
17652
|
1265 |
lemma NBWORD0: "ALL x::nat. NBWORD 0 x = WORD []"
|
14516
|
1266 |
by (import bword_num NBWORD0)
|
|
1267 |
|
17644
|
1268 |
lemma WORDLEN_NBWORD: "ALL (x::nat) xa::nat. WORDLEN (NBWORD x xa) = x"
|
14516
|
1269 |
by (import bword_num WORDLEN_NBWORD)
|
|
1270 |
|
17644
|
1271 |
lemma PWORDLEN_NBWORD: "ALL (x::nat) xa::nat. IN (NBWORD x xa) (PWORDLEN x)"
|
14516
|
1272 |
by (import bword_num PWORDLEN_NBWORD)
|
|
1273 |
|
17644
|
1274 |
lemma NBWORD_SUC: "ALL (n::nat) m::nat.
|
17652
|
1275 |
NBWORD (Suc n) m = WCAT (NBWORD n (m div 2), WORD [VB (m mod 2)])"
|
14516
|
1276 |
by (import bword_num NBWORD_SUC)
|
|
1277 |
|
17644
|
1278 |
lemma VB_BV: "ALL x::bool. VB (BV x) = x"
|
14516
|
1279 |
by (import bword_num VB_BV)
|
|
1280 |
|
14847
|
1281 |
lemma BV_VB: "(All::(nat => bool) => bool)
|
|
1282 |
(%x::nat.
|
|
1283 |
(op -->::bool => bool => bool)
|
|
1284 |
((op <::nat => nat => bool) x
|
|
1285 |
((number_of::bin => nat)
|
15647
|
1286 |
((op BIT::bin => bit => bin)
|
|
1287 |
((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
|
|
1288 |
(bit.B0::bit))))
|
14847
|
1289 |
((op =::nat => nat => bool) ((BV::bool => nat) ((VB::nat => bool) x))
|
|
1290 |
x))"
|
14516
|
1291 |
by (import bword_num BV_VB)
|
|
1292 |
|
17644
|
1293 |
lemma NBWORD_BNVAL: "ALL n::nat. RES_FORALL (PWORDLEN n) (%w::bool word. NBWORD n (BNVAL w) = w)"
|
14516
|
1294 |
by (import bword_num NBWORD_BNVAL)
|
|
1295 |
|
17652
|
1296 |
lemma BNVAL_NBWORD: "ALL (n::nat) m::nat. m < 2 ^ n --> BNVAL (NBWORD n m) = m"
|
14516
|
1297 |
by (import bword_num BNVAL_NBWORD)
|
|
1298 |
|
17644
|
1299 |
lemma ZERO_WORD_VAL: "RES_FORALL (PWORDLEN (n::nat))
|
17652
|
1300 |
(%w::bool word. (w = NBWORD n 0) = (BNVAL w = 0))"
|
14516
|
1301 |
by (import bword_num ZERO_WORD_VAL)
|
|
1302 |
|
17652
|
1303 |
lemma WCAT_NBWORD_0: "ALL (n1::nat) n2::nat. WCAT (NBWORD n1 0, NBWORD n2 0) = NBWORD (n1 + n2) 0"
|
14516
|
1304 |
by (import bword_num WCAT_NBWORD_0)
|
|
1305 |
|
17644
|
1306 |
lemma WSPLIT_NBWORD_0: "ALL (n::nat) m::nat.
|
17652
|
1307 |
m <= n --> WSPLIT m (NBWORD n 0) = (NBWORD (n - m) 0, NBWORD m 0)"
|
14516
|
1308 |
by (import bword_num WSPLIT_NBWORD_0)
|
|
1309 |
|
14847
|
1310 |
lemma EQ_NBWORD0_SPLIT: "(All::(nat => bool) => bool)
|
|
1311 |
(%n::nat.
|
|
1312 |
(RES_FORALL::(bool word => bool) => (bool word => bool) => bool)
|
|
1313 |
((PWORDLEN::nat => bool word => bool) n)
|
|
1314 |
(%w::bool word.
|
|
1315 |
(All::(nat => bool) => bool)
|
|
1316 |
(%m::nat.
|
|
1317 |
(op -->::bool => bool => bool)
|
|
1318 |
((op <=::nat => nat => bool) m n)
|
|
1319 |
((op =::bool => bool => bool)
|
|
1320 |
((op =::bool word => bool word => bool) w
|
|
1321 |
((NBWORD::nat => nat => bool word) n (0::nat)))
|
|
1322 |
((op &::bool => bool => bool)
|
|
1323 |
((op =::bool word => bool word => bool)
|
|
1324 |
((WSEG::nat => nat => bool word => bool word)
|
|
1325 |
((op -::nat => nat => nat) n m) m w)
|
|
1326 |
((NBWORD::nat => nat => bool word)
|
|
1327 |
((op -::nat => nat => nat) n m) (0::nat)))
|
|
1328 |
((op =::bool word => bool word => bool)
|
|
1329 |
((WSEG::nat => nat => bool word => bool word) m
|
|
1330 |
(0::nat) w)
|
|
1331 |
((NBWORD::nat => nat => bool word) m (0::nat))))))))"
|
14516
|
1332 |
by (import bword_num EQ_NBWORD0_SPLIT)
|
|
1333 |
|
17652
|
1334 |
lemma NBWORD_MOD: "ALL (n::nat) m::nat. NBWORD n (m mod 2 ^ n) = NBWORD n m"
|
14516
|
1335 |
by (import bword_num NBWORD_MOD)
|
|
1336 |
|
17652
|
1337 |
lemma WSEG_NBWORD_SUC: "ALL (n::nat) m::nat. WSEG n 0 (NBWORD (Suc n) m) = NBWORD n m"
|
14516
|
1338 |
by (import bword_num WSEG_NBWORD_SUC)
|
|
1339 |
|
17644
|
1340 |
lemma NBWORD_SUC_WSEG: "ALL n::nat.
|
|
1341 |
RES_FORALL (PWORDLEN (Suc n))
|
17652
|
1342 |
(%w::bool word. NBWORD n (BNVAL w) = WSEG n 0 w)"
|
14516
|
1343 |
by (import bword_num NBWORD_SUC_WSEG)
|
|
1344 |
|
17652
|
1345 |
lemma DOUBL_EQ_SHL: "ALL x>0.
|
14516
|
1346 |
RES_FORALL (PWORDLEN x)
|
17644
|
1347 |
(%xa::bool word.
|
|
1348 |
ALL xb::bool.
|
|
1349 |
NBWORD x (BNVAL xa + BNVAL xa + BV xb) = snd (SHL False xa xb))"
|
14516
|
1350 |
by (import bword_num DOUBL_EQ_SHL)
|
|
1351 |
|
17652
|
1352 |
lemma MSB_NBWORD: "ALL (n::nat) m::nat. bit n (NBWORD (Suc n) m) = VB (m div 2 ^ n mod 2)"
|
14516
|
1353 |
by (import bword_num MSB_NBWORD)
|
|
1354 |
|
17644
|
1355 |
lemma NBWORD_SPLIT: "ALL (n1::nat) (n2::nat) m::nat.
|
17652
|
1356 |
NBWORD (n1 + n2) m = WCAT (NBWORD n1 (m div 2 ^ n2), NBWORD n2 m)"
|
14516
|
1357 |
by (import bword_num NBWORD_SPLIT)
|
|
1358 |
|
17644
|
1359 |
lemma WSEG_NBWORD: "ALL (m::nat) (k::nat) n::nat.
|
|
1360 |
m + k <= n -->
|
17652
|
1361 |
(ALL l::nat. WSEG m k (NBWORD n l) = NBWORD m (l div 2 ^ k))"
|
14516
|
1362 |
by (import bword_num WSEG_NBWORD)
|
|
1363 |
|
17644
|
1364 |
lemma NBWORD_SUC_FST: "ALL (n::nat) x::nat.
|
17652
|
1365 |
NBWORD (Suc n) x = WCAT (WORD [VB (x div 2 ^ n mod 2)], NBWORD n x)"
|
14516
|
1366 |
by (import bword_num NBWORD_SUC_FST)
|
|
1367 |
|
17652
|
1368 |
lemma BIT_NBWORD0: "ALL (k::nat) n::nat. k < n --> bit k (NBWORD n 0) = False"
|
14516
|
1369 |
by (import bword_num BIT_NBWORD0)
|
|
1370 |
|
17644
|
1371 |
lemma ADD_BNVAL_LEFT: "ALL n::nat.
|
14516
|
1372 |
RES_FORALL (PWORDLEN (Suc n))
|
17644
|
1373 |
(%w1::bool word.
|
|
1374 |
RES_FORALL (PWORDLEN (Suc n))
|
|
1375 |
(%w2::bool word.
|
|
1376 |
BNVAL w1 + BNVAL w2 =
|
17652
|
1377 |
(BV (bit n w1) + BV (bit n w2)) * 2 ^ n +
|
|
1378 |
(BNVAL (WSEG n 0 w1) + BNVAL (WSEG n 0 w2))))"
|
14516
|
1379 |
by (import bword_num ADD_BNVAL_LEFT)
|
|
1380 |
|
17644
|
1381 |
lemma ADD_BNVAL_RIGHT: "ALL n::nat.
|
14516
|
1382 |
RES_FORALL (PWORDLEN (Suc n))
|
17644
|
1383 |
(%w1::bool word.
|
|
1384 |
RES_FORALL (PWORDLEN (Suc n))
|
|
1385 |
(%w2::bool word.
|
|
1386 |
BNVAL w1 + BNVAL w2 =
|
17652
|
1387 |
(BNVAL (WSEG n 1 w1) + BNVAL (WSEG n 1 w2)) * 2 +
|
|
1388 |
(BV (bit 0 w1) + BV (bit 0 w2))))"
|
14516
|
1389 |
by (import bword_num ADD_BNVAL_RIGHT)
|
|
1390 |
|
17644
|
1391 |
lemma ADD_BNVAL_SPLIT: "ALL (n1::nat) n2::nat.
|
14516
|
1392 |
RES_FORALL (PWORDLEN (n1 + n2))
|
17644
|
1393 |
(%w1::bool word.
|
|
1394 |
RES_FORALL (PWORDLEN (n1 + n2))
|
|
1395 |
(%w2::bool word.
|
|
1396 |
BNVAL w1 + BNVAL w2 =
|
17652
|
1397 |
(BNVAL (WSEG n1 n2 w1) + BNVAL (WSEG n1 n2 w2)) * 2 ^ n2 +
|
|
1398 |
(BNVAL (WSEG n2 0 w1) + BNVAL (WSEG n2 0 w2))))"
|
14516
|
1399 |
by (import bword_num ADD_BNVAL_SPLIT)
|
|
1400 |
|
|
1401 |
;end_setup
|
|
1402 |
|
|
1403 |
;setup_theory bword_arith
|
|
1404 |
|
|
1405 |
consts
|
|
1406 |
ACARRY :: "nat => bool word => bool word => bool => bool"
|
|
1407 |
|
17652
|
1408 |
specification (ACARRY) ACARRY_DEF: "(ALL (w1::bool word) (w2::bool word) cin::bool. ACARRY 0 w1 w2 cin = cin) &
|
17644
|
1409 |
(ALL (n::nat) (w1::bool word) (w2::bool word) cin::bool.
|
14516
|
1410 |
ACARRY (Suc n) w1 w2 cin =
|
17652
|
1411 |
VB ((BV (bit n w1) + BV (bit n w2) + BV (ACARRY n w1 w2 cin)) div 2))"
|
14516
|
1412 |
by (import bword_arith ACARRY_DEF)
|
|
1413 |
|
|
1414 |
consts
|
|
1415 |
ICARRY :: "nat => bool word => bool word => bool => bool"
|
|
1416 |
|
17652
|
1417 |
specification (ICARRY) ICARRY_DEF: "(ALL (w1::bool word) (w2::bool word) cin::bool. ICARRY 0 w1 w2 cin = cin) &
|
17644
|
1418 |
(ALL (n::nat) (w1::bool word) (w2::bool word) cin::bool.
|
14516
|
1419 |
ICARRY (Suc n) w1 w2 cin =
|
|
1420 |
(bit n w1 & bit n w2 | (bit n w1 | bit n w2) & ICARRY n w1 w2 cin))"
|
|
1421 |
by (import bword_arith ICARRY_DEF)
|
|
1422 |
|
17644
|
1423 |
lemma ACARRY_EQ_ICARRY: "ALL n::nat.
|
14516
|
1424 |
RES_FORALL (PWORDLEN n)
|
17644
|
1425 |
(%w1::bool word.
|
|
1426 |
RES_FORALL (PWORDLEN n)
|
|
1427 |
(%w2::bool word.
|
|
1428 |
ALL (cin::bool) k::nat.
|
|
1429 |
k <= n --> ACARRY k w1 w2 cin = ICARRY k w1 w2 cin))"
|
14516
|
1430 |
by (import bword_arith ACARRY_EQ_ICARRY)
|
|
1431 |
|
17652
|
1432 |
lemma BNVAL_LESS_EQ: "ALL n::nat. RES_FORALL (PWORDLEN n) (%w::bool word. BNVAL w <= 2 ^ n - 1)"
|
14516
|
1433 |
by (import bword_arith BNVAL_LESS_EQ)
|
|
1434 |
|
17644
|
1435 |
lemma ADD_BNVAL_LESS_EQ1: "ALL (n::nat) cin::bool.
|
14516
|
1436 |
RES_FORALL (PWORDLEN n)
|
17644
|
1437 |
(%w1::bool word.
|
|
1438 |
RES_FORALL (PWORDLEN n)
|
|
1439 |
(%w2::bool word.
|
17652
|
1440 |
(BNVAL w1 + (BNVAL w2 + BV cin)) div 2 ^ n <= Suc 0))"
|
14516
|
1441 |
by (import bword_arith ADD_BNVAL_LESS_EQ1)
|
|
1442 |
|
17644
|
1443 |
lemma ADD_BV_BNVAL_DIV_LESS_EQ1: "ALL (n::nat) (x1::bool) (x2::bool) cin::bool.
|
14516
|
1444 |
RES_FORALL (PWORDLEN n)
|
17644
|
1445 |
(%w1::bool word.
|
|
1446 |
RES_FORALL (PWORDLEN n)
|
|
1447 |
(%w2::bool word.
|
|
1448 |
(BV x1 + BV x2 +
|
17652
|
1449 |
(BNVAL w1 + (BNVAL w2 + BV cin)) div 2 ^ n) div
|
|
1450 |
2
|
|
1451 |
<= 1))"
|
14516
|
1452 |
by (import bword_arith ADD_BV_BNVAL_DIV_LESS_EQ1)
|
|
1453 |
|
17644
|
1454 |
lemma ADD_BV_BNVAL_LESS_EQ: "ALL (n::nat) (x1::bool) (x2::bool) cin::bool.
|
14516
|
1455 |
RES_FORALL (PWORDLEN n)
|
17644
|
1456 |
(%w1::bool word.
|
|
1457 |
RES_FORALL (PWORDLEN n)
|
|
1458 |
(%w2::bool word.
|
|
1459 |
BV x1 + BV x2 + (BNVAL w1 + (BNVAL w2 + BV cin))
|
17652
|
1460 |
<= Suc (2 ^ Suc n)))"
|
14516
|
1461 |
by (import bword_arith ADD_BV_BNVAL_LESS_EQ)
|
|
1462 |
|
17644
|
1463 |
lemma ADD_BV_BNVAL_LESS_EQ1: "ALL (n::nat) (x1::bool) (x2::bool) cin::bool.
|
14516
|
1464 |
RES_FORALL (PWORDLEN n)
|
17644
|
1465 |
(%w1::bool word.
|
|
1466 |
RES_FORALL (PWORDLEN n)
|
|
1467 |
(%w2::bool word.
|
|
1468 |
(BV x1 + BV x2 + (BNVAL w1 + (BNVAL w2 + BV cin))) div
|
17652
|
1469 |
2 ^ Suc n
|
|
1470 |
<= 1))"
|
14516
|
1471 |
by (import bword_arith ADD_BV_BNVAL_LESS_EQ1)
|
|
1472 |
|
14847
|
1473 |
lemma ACARRY_EQ_ADD_DIV: "(All::(nat => bool) => bool)
|
|
1474 |
(%n::nat.
|
|
1475 |
(RES_FORALL::(bool word => bool) => (bool word => bool) => bool)
|
|
1476 |
((PWORDLEN::nat => bool word => bool) n)
|
|
1477 |
(%w1::bool word.
|
|
1478 |
(RES_FORALL::(bool word => bool) => (bool word => bool) => bool)
|
|
1479 |
((PWORDLEN::nat => bool word => bool) n)
|
|
1480 |
(%w2::bool word.
|
|
1481 |
(All::(nat => bool) => bool)
|
|
1482 |
(%k::nat.
|
|
1483 |
(op -->::bool => bool => bool)
|
|
1484 |
((op <::nat => nat => bool) k n)
|
|
1485 |
((op =::nat => nat => bool)
|
|
1486 |
((BV::bool => nat)
|
|
1487 |
((ACARRY::nat
|
|
1488 |
=> bool word
|
|
1489 |
=> bool word => bool => bool)
|
|
1490 |
k w1 w2 (cin::bool)))
|
|
1491 |
((op div::nat => nat => nat)
|
|
1492 |
((op +::nat => nat => nat)
|
|
1493 |
((op +::nat => nat => nat)
|
|
1494 |
((BNVAL::bool word => nat)
|
|
1495 |
((WSEG::nat => nat => bool word => bool word)
|
|
1496 |
k (0::nat) w1))
|
|
1497 |
((BNVAL::bool word => nat)
|
|
1498 |
((WSEG::nat => nat => bool word => bool word)
|
|
1499 |
k (0::nat) w2)))
|
|
1500 |
((BV::bool => nat) cin))
|
|
1501 |
((op ^::nat => nat => nat)
|
|
1502 |
((number_of::bin => nat)
|
15647
|
1503 |
((op BIT::bin => bit => bin)
|
|
1504 |
((op BIT::bin => bit => bin)
|
|
1505 |
(Numeral.Pls::bin) (bit.B1::bit))
|
|
1506 |
(bit.B0::bit)))
|
14847
|
1507 |
k)))))))"
|
14516
|
1508 |
by (import bword_arith ACARRY_EQ_ADD_DIV)
|
|
1509 |
|
17644
|
1510 |
lemma ADD_WORD_SPLIT: "ALL (n1::nat) n2::nat.
|
14516
|
1511 |
RES_FORALL (PWORDLEN (n1 + n2))
|
17644
|
1512 |
(%w1::bool word.
|
|
1513 |
RES_FORALL (PWORDLEN (n1 + n2))
|
|
1514 |
(%w2::bool word.
|
|
1515 |
ALL cin::bool.
|
|
1516 |
NBWORD (n1 + n2) (BNVAL w1 + BNVAL w2 + BV cin) =
|
|
1517 |
WCAT
|
|
1518 |
(NBWORD n1
|
|
1519 |
(BNVAL (WSEG n1 n2 w1) + BNVAL (WSEG n1 n2 w2) +
|
|
1520 |
BV (ACARRY n2 w1 w2 cin)),
|
|
1521 |
NBWORD n2
|
17652
|
1522 |
(BNVAL (WSEG n2 0 w1) + BNVAL (WSEG n2 0 w2) + BV cin))))"
|
14516
|
1523 |
by (import bword_arith ADD_WORD_SPLIT)
|
|
1524 |
|
17644
|
1525 |
lemma WSEG_NBWORD_ADD: "ALL n::nat.
|
14516
|
1526 |
RES_FORALL (PWORDLEN n)
|
17644
|
1527 |
(%w1::bool word.
|
|
1528 |
RES_FORALL (PWORDLEN n)
|
|
1529 |
(%w2::bool word.
|
|
1530 |
ALL (m::nat) (k::nat) cin::bool.
|
|
1531 |
m + k <= n -->
|
|
1532 |
WSEG m k (NBWORD n (BNVAL w1 + BNVAL w2 + BV cin)) =
|
|
1533 |
NBWORD m
|
|
1534 |
(BNVAL (WSEG m k w1) + BNVAL (WSEG m k w2) +
|
|
1535 |
BV (ACARRY k w1 w2 cin))))"
|
14516
|
1536 |
by (import bword_arith WSEG_NBWORD_ADD)
|
|
1537 |
|
17644
|
1538 |
lemma ADD_NBWORD_EQ0_SPLIT: "ALL (n1::nat) n2::nat.
|
14516
|
1539 |
RES_FORALL (PWORDLEN (n1 + n2))
|
17644
|
1540 |
(%w1::bool word.
|
|
1541 |
RES_FORALL (PWORDLEN (n1 + n2))
|
|
1542 |
(%w2::bool word.
|
|
1543 |
ALL cin::bool.
|
|
1544 |
(NBWORD (n1 + n2) (BNVAL w1 + BNVAL w2 + BV cin) =
|
17652
|
1545 |
NBWORD (n1 + n2) 0) =
|
17644
|
1546 |
(NBWORD n1
|
|
1547 |
(BNVAL (WSEG n1 n2 w1) + BNVAL (WSEG n1 n2 w2) +
|
|
1548 |
BV (ACARRY n2 w1 w2 cin)) =
|
17652
|
1549 |
NBWORD n1 0 &
|
17644
|
1550 |
NBWORD n2
|
17652
|
1551 |
(BNVAL (WSEG n2 0 w1) + BNVAL (WSEG n2 0 w2) + BV cin) =
|
|
1552 |
NBWORD n2 0)))"
|
14516
|
1553 |
by (import bword_arith ADD_NBWORD_EQ0_SPLIT)
|
|
1554 |
|
17644
|
1555 |
lemma ACARRY_MSB: "ALL n::nat.
|
14516
|
1556 |
RES_FORALL (PWORDLEN n)
|
17644
|
1557 |
(%w1::bool word.
|
|
1558 |
RES_FORALL (PWORDLEN n)
|
|
1559 |
(%w2::bool word.
|
|
1560 |
ALL cin::bool.
|
|
1561 |
ACARRY n w1 w2 cin =
|
|
1562 |
bit n (NBWORD (Suc n) (BNVAL w1 + BNVAL w2 + BV cin))))"
|
14516
|
1563 |
by (import bword_arith ACARRY_MSB)
|
|
1564 |
|
17644
|
1565 |
lemma ACARRY_WSEG: "ALL n::nat.
|
14516
|
1566 |
RES_FORALL (PWORDLEN n)
|
17644
|
1567 |
(%w1::bool word.
|
|
1568 |
RES_FORALL (PWORDLEN n)
|
|
1569 |
(%w2::bool word.
|
|
1570 |
ALL (cin::bool) (k::nat) m::nat.
|
|
1571 |
k < m & m <= n -->
|
17652
|
1572 |
ACARRY k (WSEG m 0 w1) (WSEG m 0 w2) cin =
|
17644
|
1573 |
ACARRY k w1 w2 cin))"
|
14516
|
1574 |
by (import bword_arith ACARRY_WSEG)
|
|
1575 |
|
17644
|
1576 |
lemma ICARRY_WSEG: "ALL n::nat.
|
14516
|
1577 |
RES_FORALL (PWORDLEN n)
|
17644
|
1578 |
(%w1::bool word.
|
|
1579 |
RES_FORALL (PWORDLEN n)
|
|
1580 |
(%w2::bool word.
|
|
1581 |
ALL (cin::bool) (k::nat) m::nat.
|
|
1582 |
k < m & m <= n -->
|
17652
|
1583 |
ICARRY k (WSEG m 0 w1) (WSEG m 0 w2) cin =
|
17644
|
1584 |
ICARRY k w1 w2 cin))"
|
14516
|
1585 |
by (import bword_arith ICARRY_WSEG)
|
|
1586 |
|
17644
|
1587 |
lemma ACARRY_ACARRY_WSEG: "ALL n::nat.
|
14516
|
1588 |
RES_FORALL (PWORDLEN n)
|
17644
|
1589 |
(%w1::bool word.
|
|
1590 |
RES_FORALL (PWORDLEN n)
|
|
1591 |
(%w2::bool word.
|
|
1592 |
ALL (cin::bool) (m::nat) (k1::nat) k2::nat.
|
|
1593 |
k1 < m & k2 < n & m + k2 <= n -->
|
|
1594 |
ACARRY k1 (WSEG m k2 w1) (WSEG m k2 w2)
|
|
1595 |
(ACARRY k2 w1 w2 cin) =
|
|
1596 |
ACARRY (k1 + k2) w1 w2 cin))"
|
14516
|
1597 |
by (import bword_arith ACARRY_ACARRY_WSEG)
|
|
1598 |
|
|
1599 |
;end_setup
|
|
1600 |
|
|
1601 |
;setup_theory bword_bitop
|
|
1602 |
|
|
1603 |
consts
|
|
1604 |
WNOT :: "bool word => bool word"
|
|
1605 |
|
17644
|
1606 |
specification (WNOT) WNOT_DEF: "ALL l::bool list. WNOT (WORD l) = WORD (map Not l)"
|
14516
|
1607 |
by (import bword_bitop WNOT_DEF)
|
|
1608 |
|
|
1609 |
lemma PBITOP_WNOT: "IN WNOT PBITOP"
|
|
1610 |
by (import bword_bitop PBITOP_WNOT)
|
|
1611 |
|
17644
|
1612 |
lemma WNOT_WNOT: "ALL w::bool word. WNOT (WNOT w) = w"
|
14516
|
1613 |
by (import bword_bitop WNOT_WNOT)
|
|
1614 |
|
17644
|
1615 |
lemma WCAT_WNOT: "ALL (n1::nat) n2::nat.
|
14516
|
1616 |
RES_FORALL (PWORDLEN n1)
|
17644
|
1617 |
(%w1::bool word.
|
|
1618 |
RES_FORALL (PWORDLEN n2)
|
|
1619 |
(%w2::bool word. WCAT (WNOT w1, WNOT w2) = WNOT (WCAT (w1, w2))))"
|
14516
|
1620 |
by (import bword_bitop WCAT_WNOT)
|
|
1621 |
|
|
1622 |
consts
|
|
1623 |
WAND :: "bool word => bool word => bool word"
|
|
1624 |
|
17644
|
1625 |
specification (WAND) WAND_DEF: "ALL (l1::bool list) l2::bool list.
|
|
1626 |
WAND (WORD l1) (WORD l2) = WORD (map2 op & l1 l2)"
|
14516
|
1627 |
by (import bword_bitop WAND_DEF)
|
|
1628 |
|
|
1629 |
lemma PBITBOP_WAND: "IN WAND PBITBOP"
|
|
1630 |
by (import bword_bitop PBITBOP_WAND)
|
|
1631 |
|
|
1632 |
consts
|
|
1633 |
WOR :: "bool word => bool word => bool word"
|
|
1634 |
|
17644
|
1635 |
specification (WOR) WOR_DEF: "ALL (l1::bool list) l2::bool list.
|
|
1636 |
WOR (WORD l1) (WORD l2) = WORD (map2 op | l1 l2)"
|
14516
|
1637 |
by (import bword_bitop WOR_DEF)
|
|
1638 |
|
|
1639 |
lemma PBITBOP_WOR: "IN WOR PBITBOP"
|
|
1640 |
by (import bword_bitop PBITBOP_WOR)
|
|
1641 |
|
|
1642 |
consts
|
|
1643 |
WXOR :: "bool word => bool word => bool word"
|
|
1644 |
|
17644
|
1645 |
specification (WXOR) WXOR_DEF: "ALL (l1::bool list) l2::bool list.
|
|
1646 |
WXOR (WORD l1) (WORD l2) = WORD (map2 (%(x::bool) y::bool. x ~= y) l1 l2)"
|
14516
|
1647 |
by (import bword_bitop WXOR_DEF)
|
|
1648 |
|
|
1649 |
lemma PBITBOP_WXOR: "IN WXOR PBITBOP"
|
|
1650 |
by (import bword_bitop PBITBOP_WXOR)
|
|
1651 |
|
|
1652 |
;end_setup
|
|
1653 |
|
|
1654 |
end
|
|
1655 |
|