15647

1 
(* AUTOMATICALLY GENERATED, DO NOT EDIT! *)


2 

17566

3 
theory HOL4Vec imports HOL4Base begin

14516

4 


5 
;setup_theory res_quan


6 


7 
lemma RES_FORALL_CONJ_DIST: "ALL P Q R. RES_FORALL P (%i. Q i & R i) = (RES_FORALL P Q & RES_FORALL P R)"


8 
by (import res_quan RES_FORALL_CONJ_DIST)


9 


10 
lemma RES_FORALL_DISJ_DIST: "ALL P Q R. RES_FORALL (%j. P j  Q j) R = (RES_FORALL P R & RES_FORALL Q R)"


11 
by (import res_quan RES_FORALL_DISJ_DIST)


12 


13 
lemma RES_FORALL_UNIQUE: "ALL x xa. RES_FORALL (op = xa) x = x xa"


14 
by (import res_quan RES_FORALL_UNIQUE)


15 


16 
lemma RES_FORALL_FORALL: "ALL (P::'a => bool) (R::'a => 'b => bool) x::'b.


17 
(ALL x::'b. RES_FORALL P (%i::'a. R i x)) =


18 
RES_FORALL P (%i::'a. All (R i))"


19 
by (import res_quan RES_FORALL_FORALL)


20 


21 
lemma RES_FORALL_REORDER: "ALL P Q R.


22 
RES_FORALL P (%i. RES_FORALL Q (R i)) =


23 
RES_FORALL Q (%j. RES_FORALL P (%i. R i j))"


24 
by (import res_quan RES_FORALL_REORDER)


25 


26 
lemma RES_FORALL_EMPTY: "All (RES_FORALL EMPTY)"


27 
by (import res_quan RES_FORALL_EMPTY)


28 


29 
lemma RES_FORALL_UNIV: "ALL p. RES_FORALL pred_set.UNIV p = All p"


30 
by (import res_quan RES_FORALL_UNIV)


31 


32 
lemma RES_FORALL_NULL: "ALL p m. RES_FORALL p (%x. m) = (p = EMPTY  m)"


33 
by (import res_quan RES_FORALL_NULL)


34 

17188

35 
lemma RES_EXISTS_DISJ_DIST: "ALL P Q R. RES_EXISTS P (%i. Q i  R i) = (RES_EXISTS P Q  RES_EXISTS P R)"

14516

36 
by (import res_quan RES_EXISTS_DISJ_DIST)


37 


38 
lemma RES_DISJ_EXISTS_DIST: "ALL P Q R. RES_EXISTS (%i. P i  Q i) R = (RES_EXISTS P R  RES_EXISTS Q R)"


39 
by (import res_quan RES_DISJ_EXISTS_DIST)


40 


41 
lemma RES_EXISTS_EQUAL: "ALL x xa. RES_EXISTS (op = xa) x = x xa"


42 
by (import res_quan RES_EXISTS_EQUAL)


43 


44 
lemma RES_EXISTS_REORDER: "ALL P Q R.


45 
RES_EXISTS P (%i. RES_EXISTS Q (R i)) =


46 
RES_EXISTS Q (%j. RES_EXISTS P (%i. R i j))"


47 
by (import res_quan RES_EXISTS_REORDER)


48 


49 
lemma RES_EXISTS_EMPTY: "ALL p. ~ RES_EXISTS EMPTY p"


50 
by (import res_quan RES_EXISTS_EMPTY)


51 


52 
lemma RES_EXISTS_UNIV: "ALL p. RES_EXISTS pred_set.UNIV p = Ex p"


53 
by (import res_quan RES_EXISTS_UNIV)


54 


55 
lemma RES_EXISTS_NULL: "ALL p m. RES_EXISTS p (%x. m) = (p ~= EMPTY & m)"


56 
by (import res_quan RES_EXISTS_NULL)


57 


58 
lemma RES_EXISTS_ALT: "ALL p m. RES_EXISTS p m = (IN (RES_SELECT p m) p & m (RES_SELECT p m))"


59 
by (import res_quan RES_EXISTS_ALT)


60 


61 
lemma RES_EXISTS_UNIQUE_EMPTY: "ALL p. ~ RES_EXISTS_UNIQUE EMPTY p"


62 
by (import res_quan RES_EXISTS_UNIQUE_EMPTY)


63 


64 
lemma RES_EXISTS_UNIQUE_UNIV: "ALL p. RES_EXISTS_UNIQUE pred_set.UNIV p = Ex1 p"


65 
by (import res_quan RES_EXISTS_UNIQUE_UNIV)


66 


67 
lemma RES_EXISTS_UNIQUE_NULL: "ALL p m. RES_EXISTS_UNIQUE p (%x. m) = ((EX x. p = INSERT x EMPTY) & m)"


68 
by (import res_quan RES_EXISTS_UNIQUE_NULL)


69 


70 
lemma RES_EXISTS_UNIQUE_ALT: "ALL p m.


71 
RES_EXISTS_UNIQUE p m =


72 
RES_EXISTS p (%x. m x & RES_FORALL p (%y. m y > y = x))"


73 
by (import res_quan RES_EXISTS_UNIQUE_ALT)


74 


75 
lemma RES_SELECT_EMPTY: "ALL p. RES_SELECT EMPTY p = (SOME x. False)"


76 
by (import res_quan RES_SELECT_EMPTY)


77 


78 
lemma RES_SELECT_UNIV: "ALL p. RES_SELECT pred_set.UNIV p = Eps p"


79 
by (import res_quan RES_SELECT_UNIV)


80 


81 
lemma RES_ABSTRACT: "ALL p m x. IN x p > RES_ABSTRACT p m x = m x"


82 
by (import res_quan RES_ABSTRACT)


83 


84 
lemma RES_ABSTRACT_EQUAL: "ALL p m1 m2.


85 
(ALL x. IN x p > m1 x = m2 x) > RES_ABSTRACT p m1 = RES_ABSTRACT p m2"


86 
by (import res_quan RES_ABSTRACT_EQUAL)


87 


88 
lemma RES_ABSTRACT_IDEMPOT: "ALL p m. RES_ABSTRACT p (RES_ABSTRACT p m) = RES_ABSTRACT p m"


89 
by (import res_quan RES_ABSTRACT_IDEMPOT)


90 


91 
lemma RES_ABSTRACT_EQUAL_EQ: "ALL p m1 m2.


92 
(RES_ABSTRACT p m1 = RES_ABSTRACT p m2) = (ALL x. IN x p > m1 x = m2 x)"


93 
by (import res_quan RES_ABSTRACT_EQUAL_EQ)


94 


95 
;end_setup


96 


97 
;setup_theory word_base


98 


99 
typedef (open) ('a) word = "(Collect::('a list recspace => bool) => 'a list recspace set)


100 
(%x::'a list recspace.


101 
(All::(('a list recspace => bool) => bool) => bool)


102 
(%word::'a list recspace => bool.


103 
(op >::bool => bool => bool)


104 
((All::('a list recspace => bool) => bool)


105 
(%a0::'a list recspace.


106 
(op >::bool => bool => bool)


107 
((Ex::('a list => bool) => bool)


108 
(%a::'a list.


109 
(op =::'a list recspace => 'a list recspace => bool)


110 
a0 ((CONSTR::nat


111 
=> 'a list => (nat => 'a list recspace) => 'a list recspace)


112 
(0::nat) a


113 
(%n::nat. BOTTOM::'a list recspace))))


114 
(word a0)))


115 
(word x)))"


116 
by (rule typedef_helper,import word_base word_TY_DEF)


117 


118 
lemmas word_TY_DEF = typedef_hol2hol4 [OF type_definition_word]


119 


120 
consts


121 
mk_word :: "'a list recspace => 'a word"


122 
dest_word :: "'a word => 'a list recspace"


123 


124 
specification (dest_word mk_word) word_repfns: "(ALL a::'a word. mk_word (dest_word a) = a) &


125 
(ALL r::'a list recspace.


126 
(ALL word::'a list recspace => bool.


127 
(ALL a0::'a list recspace.


128 
(EX a::'a list. a0 = CONSTR (0::nat) a (%n::nat. BOTTOM)) >


129 
word a0) >


130 
word r) =


131 
(dest_word (mk_word r) = r))"


132 
by (import word_base word_repfns)


133 


134 
consts


135 
word_base0 :: "'a list => 'a word"


136 


137 
defs


138 
word_base0_primdef: "word_base0 == %a. mk_word (CONSTR 0 a (%n. BOTTOM))"


139 


140 
lemma word_base0_def: "word_base0 = (%a. mk_word (CONSTR 0 a (%n. BOTTOM)))"


141 
by (import word_base word_base0_def)


142 


143 
constdefs


144 
WORD :: "'a list => 'a word"


145 
"WORD == word_base0"


146 


147 
lemma WORD: "WORD = word_base0"


148 
by (import word_base WORD)


149 


150 
consts


151 
word_case :: "('a list => 'b) => 'a word => 'b"


152 


153 
specification (word_case_primdef: word_case) word_case_def: "ALL f a. word_case f (WORD a) = f a"


154 
by (import word_base word_case_def)


155 


156 
consts


157 
word_size :: "('a => nat) => 'a word => nat"


158 


159 
specification (word_size_primdef: word_size) word_size_def: "ALL f a. word_size f (WORD a) = 1 + list_size f a"


160 
by (import word_base word_size_def)


161 


162 
lemma word_11: "ALL a a'. (WORD a = WORD a') = (a = a')"


163 
by (import word_base word_11)


164 


165 
lemma word_case_cong: "ALL M M' f.


166 
M = M' & (ALL a. M' = WORD a > f a = f' a) >


167 
word_case f M = word_case f' M'"


168 
by (import word_base word_case_cong)


169 


170 
lemma word_nchotomy: "ALL x. EX l. x = WORD l"


171 
by (import word_base word_nchotomy)


172 


173 
lemma word_Axiom: "ALL f. EX fn. ALL a. fn (WORD a) = f a"


174 
by (import word_base word_Axiom)


175 


176 
lemma word_induction: "ALL P. (ALL a. P (WORD a)) > All P"


177 
by (import word_base word_induction)


178 


179 
lemma word_Ax: "ALL f. EX fn. ALL a. fn (WORD a) = f a"


180 
by (import word_base word_Ax)


181 


182 
lemma WORD_11: "ALL x xa. (WORD x = WORD xa) = (x = xa)"


183 
by (import word_base WORD_11)


184 


185 
lemma word_induct: "ALL x. (ALL l. x (WORD l)) > All x"


186 
by (import word_base word_induct)


187 


188 
lemma word_cases: "ALL x. EX l. x = WORD l"


189 
by (import word_base word_cases)


190 


191 
consts


192 
WORDLEN :: "'a word => nat"


193 


194 
specification (WORDLEN) WORDLEN_DEF: "ALL l. WORDLEN (WORD l) = length l"


195 
by (import word_base WORDLEN_DEF)


196 


197 
consts


198 
PWORDLEN :: "nat => 'a word => bool"


199 


200 
defs


201 
PWORDLEN_primdef: "PWORDLEN == %n. GSPEC (%w. (w, WORDLEN w = n))"


202 


203 
lemma PWORDLEN_def: "ALL n. PWORDLEN n = GSPEC (%w. (w, WORDLEN w = n))"


204 
by (import word_base PWORDLEN_def)


205 


206 
lemma IN_PWORDLEN: "ALL n l. IN (WORD l) (PWORDLEN n) = (length l = n)"


207 
by (import word_base IN_PWORDLEN)


208 


209 
lemma PWORDLEN: "ALL n w. IN w (PWORDLEN n) = (WORDLEN w = n)"


210 
by (import word_base PWORDLEN)


211 


212 
lemma PWORDLEN0: "ALL w. IN w (PWORDLEN 0) > w = WORD []"


213 
by (import word_base PWORDLEN0)


214 


215 
lemma PWORDLEN1: "ALL x. IN (WORD [x]) (PWORDLEN 1)"


216 
by (import word_base PWORDLEN1)


217 


218 
consts


219 
WSEG :: "nat => nat => 'a word => 'a word"


220 


221 
specification (WSEG) WSEG_DEF: "ALL m k l. WSEG m k (WORD l) = WORD (LASTN m (BUTLASTN k l))"


222 
by (import word_base WSEG_DEF)


223 


224 
lemma WSEG0: "ALL k w. WSEG 0 k w = WORD []"


225 
by (import word_base WSEG0)


226 


227 
lemma WSEG_PWORDLEN: "ALL n.


228 
RES_FORALL (PWORDLEN n)


229 
(%w. ALL m k. m + k <= n > IN (WSEG m k w) (PWORDLEN m))"


230 
by (import word_base WSEG_PWORDLEN)


231 


232 
lemma WSEG_WORDLEN: "ALL x.


233 
RES_FORALL (PWORDLEN x)


234 
(%xa. ALL xb xc. xb + xc <= x > WORDLEN (WSEG xb xc xa) = xb)"


235 
by (import word_base WSEG_WORDLEN)


236 


237 
lemma WSEG_WORD_LENGTH: "ALL n. RES_FORALL (PWORDLEN n) (%w. WSEG n 0 w = w)"


238 
by (import word_base WSEG_WORD_LENGTH)


239 


240 
consts


241 
bit :: "nat => 'a word => 'a"


242 


243 
specification (bit) BIT_DEF: "ALL k l. bit k (WORD l) = ELL k l"


244 
by (import word_base BIT_DEF)


245 


246 
lemma BIT0: "ALL x. bit 0 (WORD [x]) = x"


247 
by (import word_base BIT0)


248 

14847

249 
lemma WSEG_BIT: "(All::(nat => bool) => bool)


250 
(%n::nat.


251 
(RES_FORALL::('a word => bool) => ('a word => bool) => bool)


252 
((PWORDLEN::nat => 'a word => bool) n)


253 
(%w::'a word.


254 
(All::(nat => bool) => bool)


255 
(%k::nat.


256 
(op >::bool => bool => bool)


257 
((op <::nat => nat => bool) k n)


258 
((op =::'a word => 'a word => bool)


259 
((WSEG::nat => nat => 'a word => 'a word) (1::nat) k w)


260 
((WORD::'a list => 'a word)


261 
((op #::'a => 'a list => 'a list)


262 
((bit::nat => 'a word => 'a) k w) ([]::'a list)))))))"

14516

263 
by (import word_base WSEG_BIT)


264 


265 
lemma BIT_WSEG: "ALL n.


266 
RES_FORALL (PWORDLEN n)


267 
(%w. ALL m k j.


268 
m + k <= n > j < m > bit j (WSEG m k w) = bit (j + k) w)"


269 
by (import word_base BIT_WSEG)


270 


271 
consts


272 
MSB :: "'a word => 'a"


273 


274 
specification (MSB) MSB_DEF: "ALL l. MSB (WORD l) = hd l"


275 
by (import word_base MSB_DEF)


276 


277 
lemma MSB: "ALL n. RES_FORALL (PWORDLEN n) (%w. 0 < n > MSB w = bit (PRE n) w)"


278 
by (import word_base MSB)


279 


280 
consts


281 
LSB :: "'a word => 'a"


282 


283 
specification (LSB) LSB_DEF: "ALL l. LSB (WORD l) = last l"


284 
by (import word_base LSB_DEF)


285 


286 
lemma LSB: "ALL n. RES_FORALL (PWORDLEN n) (%w. 0 < n > LSB w = bit 0 w)"


287 
by (import word_base LSB)


288 


289 
consts


290 
WSPLIT :: "nat => 'a word => 'a word * 'a word"


291 


292 
specification (WSPLIT) WSPLIT_DEF: "ALL m l. WSPLIT m (WORD l) = (WORD (BUTLASTN m l), WORD (LASTN m l))"


293 
by (import word_base WSPLIT_DEF)


294 


295 
consts


296 
WCAT :: "'a word * 'a word => 'a word"


297 


298 
specification (WCAT) WCAT_DEF: "ALL l1 l2. WCAT (WORD l1, WORD l2) = WORD (l1 @ l2)"


299 
by (import word_base WCAT_DEF)


300 

14847

301 
lemma WORD_PARTITION: "(op &::bool => bool => bool)


302 
((All::(nat => bool) => bool)


303 
(%n::nat.


304 
(RES_FORALL::('a word => bool) => ('a word => bool) => bool)


305 
((PWORDLEN::nat => 'a word => bool) n)


306 
(%w::'a word.


307 
(All::(nat => bool) => bool)


308 
(%m::nat.


309 
(op >::bool => bool => bool)


310 
((op <=::nat => nat => bool) m n)


311 
((op =::'a word => 'a word => bool)


312 
((WCAT::'a word * 'a word => 'a word)


313 
((WSPLIT::nat => 'a word => 'a word * 'a word) m w))


314 
w)))))


315 
((All::(nat => bool) => bool)


316 
(%n::nat.


317 
(All::(nat => bool) => bool)


318 
(%m::nat.


319 
(RES_FORALL::('a word => bool) => ('a word => bool) => bool)


320 
((PWORDLEN::nat => 'a word => bool) n)


321 
(%w1::'a word.


322 
(RES_FORALL::('a word => bool)


323 
=> ('a word => bool) => bool)


324 
((PWORDLEN::nat => 'a word => bool) m)


325 
(%w2::'a word.


326 
(op =::'a word * 'a word => 'a word * 'a word => bool)


327 
((WSPLIT::nat => 'a word => 'a word * 'a word) m


328 
((WCAT::'a word * 'a word => 'a word)


329 
((Pair::'a word => 'a word => 'a word * 'a word)


330 
w1 w2)))


331 
((Pair::'a word => 'a word => 'a word * 'a word) w1


332 
w2))))))"

14516

333 
by (import word_base WORD_PARTITION)


334 


335 
lemma WCAT_ASSOC: "ALL w1 w2 w3. WCAT (w1, WCAT (w2, w3)) = WCAT (WCAT (w1, w2), w3)"


336 
by (import word_base WCAT_ASSOC)


337 


338 
lemma WCAT0: "ALL w. WCAT (WORD [], w) = w & WCAT (w, WORD []) = w"


339 
by (import word_base WCAT0)


340 


341 
lemma WCAT_11: "ALL m n.


342 
RES_FORALL (PWORDLEN m)


343 
(%wm1. RES_FORALL (PWORDLEN m)


344 
(%wm2. RES_FORALL (PWORDLEN n)


345 
(%wn1. RES_FORALL (PWORDLEN n)


346 
(%wn2. (WCAT (wm1, wn1) = WCAT (wm2, wn2)) =


347 
(wm1 = wm2 & wn1 = wn2)))))"


348 
by (import word_base WCAT_11)


349 

14847

350 
lemma WSPLIT_PWORDLEN: "(All::(nat => bool) => bool)


351 
(%n::nat.


352 
(RES_FORALL::('a word => bool) => ('a word => bool) => bool)


353 
((PWORDLEN::nat => 'a word => bool) n)


354 
(%w::'a word.


355 
(All::(nat => bool) => bool)


356 
(%m::nat.


357 
(op >::bool => bool => bool)


358 
((op <=::nat => nat => bool) m n)


359 
((op &::bool => bool => bool)


360 
((IN::'a word => ('a word => bool) => bool)


361 
((fst::'a word * 'a word => 'a word)


362 
((WSPLIT::nat => 'a word => 'a word * 'a word) m w))


363 
((PWORDLEN::nat => 'a word => bool)


364 
((op ::nat => nat => nat) n m)))


365 
((IN::'a word => ('a word => bool) => bool)


366 
((snd::'a word * 'a word => 'a word)


367 
((WSPLIT::nat => 'a word => 'a word * 'a word) m w))


368 
((PWORDLEN::nat => 'a word => bool) m))))))"

14516

369 
by (import word_base WSPLIT_PWORDLEN)


370 


371 
lemma WCAT_PWORDLEN: "ALL n1.


372 
RES_FORALL (PWORDLEN n1)


373 
(%w1. ALL n2.


374 
RES_FORALL (PWORDLEN n2)


375 
(%w2. IN (WCAT (w1, w2)) (PWORDLEN (n1 + n2))))"


376 
by (import word_base WCAT_PWORDLEN)


377 


378 
lemma WORDLEN_SUC_WCAT: "ALL n w.


379 
IN w (PWORDLEN (Suc n)) >


380 
RES_EXISTS (PWORDLEN 1)


381 
(%b. RES_EXISTS (PWORDLEN n) (%w'. w = WCAT (b, w')))"


382 
by (import word_base WORDLEN_SUC_WCAT)


383 


384 
lemma WSEG_WSEG: "ALL n.


385 
RES_FORALL (PWORDLEN n)


386 
(%w. ALL m1 k1 m2 k2.


387 
m1 + k1 <= n & m2 + k2 <= m1 >


388 
WSEG m2 k2 (WSEG m1 k1 w) = WSEG m2 (k1 + k2) w)"


389 
by (import word_base WSEG_WSEG)


390 

14847

391 
lemma WSPLIT_WSEG: "(All::(nat => bool) => bool)


392 
(%n::nat.


393 
(RES_FORALL::('a word => bool) => ('a word => bool) => bool)


394 
((PWORDLEN::nat => 'a word => bool) n)


395 
(%w::'a word.


396 
(All::(nat => bool) => bool)


397 
(%k::nat.


398 
(op >::bool => bool => bool)


399 
((op <=::nat => nat => bool) k n)


400 
((op =::'a word * 'a word => 'a word * 'a word => bool)


401 
((WSPLIT::nat => 'a word => 'a word * 'a word) k w)


402 
((Pair::'a word => 'a word => 'a word * 'a word)


403 
((WSEG::nat => nat => 'a word => 'a word)


404 
((op ::nat => nat => nat) n k) k w)


405 
((WSEG::nat => nat => 'a word => 'a word) k (0::nat)


406 
w))))))"

14516

407 
by (import word_base WSPLIT_WSEG)


408 

14847

409 
lemma WSPLIT_WSEG1: "(All::(nat => bool) => bool)


410 
(%n::nat.


411 
(RES_FORALL::('a word => bool) => ('a word => bool) => bool)


412 
((PWORDLEN::nat => 'a word => bool) n)


413 
(%w::'a word.


414 
(All::(nat => bool) => bool)


415 
(%k::nat.


416 
(op >::bool => bool => bool)


417 
((op <=::nat => nat => bool) k n)


418 
((op =::'a word => 'a word => bool)


419 
((fst::'a word * 'a word => 'a word)


420 
((WSPLIT::nat => 'a word => 'a word * 'a word) k w))


421 
((WSEG::nat => nat => 'a word => 'a word)


422 
((op ::nat => nat => nat) n k) k w)))))"

14516

423 
by (import word_base WSPLIT_WSEG1)


424 

14847

425 
lemma WSPLIT_WSEG2: "(All::(nat => bool) => bool)


426 
(%n::nat.


427 
(RES_FORALL::('a word => bool) => ('a word => bool) => bool)


428 
((PWORDLEN::nat => 'a word => bool) n)


429 
(%w::'a word.


430 
(All::(nat => bool) => bool)


431 
(%k::nat.


432 
(op >::bool => bool => bool)


433 
((op <=::nat => nat => bool) k n)


434 
((op =::'a word => 'a word => bool)


435 
((snd::'a word * 'a word => 'a word)


436 
((WSPLIT::nat => 'a word => 'a word * 'a word) k w))


437 
((WSEG::nat => nat => 'a word => 'a word) k (0::nat)


438 
w)))))"

14516

439 
by (import word_base WSPLIT_WSEG2)


440 


441 
lemma WCAT_WSEG_WSEG: "ALL n.


442 
RES_FORALL (PWORDLEN n)


443 
(%w. ALL m1 m2 k.


444 
m1 + (m2 + k) <= n >


445 
WCAT (WSEG m2 (m1 + k) w, WSEG m1 k w) = WSEG (m1 + m2) k w)"


446 
by (import word_base WCAT_WSEG_WSEG)


447 


448 
lemma WORD_SPLIT: "ALL x xa.


449 
RES_FORALL (PWORDLEN (x + xa)) (%w. w = WCAT (WSEG x xa w, WSEG xa 0 w))"


450 
by (import word_base WORD_SPLIT)


451 


452 
lemma WORDLEN_SUC_WCAT_WSEG_WSEG: "RES_FORALL (PWORDLEN (Suc n)) (%w. w = WCAT (WSEG 1 n w, WSEG n 0 w))"


453 
by (import word_base WORDLEN_SUC_WCAT_WSEG_WSEG)


454 


455 
lemma WORDLEN_SUC_WCAT_WSEG_WSEG_RIGHT: "RES_FORALL (PWORDLEN (Suc n)) (%w. w = WCAT (WSEG n 1 w, WSEG 1 0 w))"


456 
by (import word_base WORDLEN_SUC_WCAT_WSEG_WSEG_RIGHT)


457 


458 
lemma WORDLEN_SUC_WCAT_BIT_WSEG: "ALL n.


459 
RES_FORALL (PWORDLEN (Suc n)) (%w. w = WCAT (WORD [bit n w], WSEG n 0 w))"


460 
by (import word_base WORDLEN_SUC_WCAT_BIT_WSEG)


461 


462 
lemma WORDLEN_SUC_WCAT_BIT_WSEG_RIGHT: "ALL n.


463 
RES_FORALL (PWORDLEN (Suc n)) (%w. w = WCAT (WSEG n 1 w, WORD [bit 0 w]))"


464 
by (import word_base WORDLEN_SUC_WCAT_BIT_WSEG_RIGHT)


465 


466 
lemma WSEG_WCAT1: "ALL n1 n2.


467 
RES_FORALL (PWORDLEN n1)


468 
(%w1. RES_FORALL (PWORDLEN n2) (%w2. WSEG n1 n2 (WCAT (w1, w2)) = w1))"


469 
by (import word_base WSEG_WCAT1)


470 


471 
lemma WSEG_WCAT2: "ALL n1 n2.


472 
RES_FORALL (PWORDLEN n1)


473 
(%w1. RES_FORALL (PWORDLEN n2) (%w2. WSEG n2 0 (WCAT (w1, w2)) = w2))"


474 
by (import word_base WSEG_WCAT2)


475 


476 
lemma WSEG_SUC: "ALL n.


477 
RES_FORALL (PWORDLEN n)


478 
(%w. ALL k m1.


479 
k + Suc m1 < n >


480 
WSEG (Suc m1) k w = WCAT (WSEG 1 (k + m1) w, WSEG m1 k w))"


481 
by (import word_base WSEG_SUC)


482 


483 
lemma WORD_CONS_WCAT: "ALL x l. WORD (x # l) = WCAT (WORD [x], WORD l)"


484 
by (import word_base WORD_CONS_WCAT)


485 


486 
lemma WORD_SNOC_WCAT: "ALL l x. WORD (SNOC x l) = WCAT (WORD l, WORD [x])"


487 
by (import word_base WORD_SNOC_WCAT)


488 


489 
lemma BIT_WCAT_FST: "ALL n1 n2.


490 
RES_FORALL (PWORDLEN n1)


491 
(%w1. RES_FORALL (PWORDLEN n2)


492 
(%w2. ALL k.


493 
n2 <= k & k < n1 + n2 >


494 
bit k (WCAT (w1, w2)) = bit (k  n2) w1))"


495 
by (import word_base BIT_WCAT_FST)


496 

14847

497 
lemma BIT_WCAT_SND: "(All::(nat => bool) => bool)


498 
(%n1::nat.


499 
(All::(nat => bool) => bool)


500 
(%n2::nat.


501 
(RES_FORALL::('a word => bool) => ('a word => bool) => bool)


502 
((PWORDLEN::nat => 'a word => bool) n1)


503 
(%w1::'a word.


504 
(RES_FORALL::('a word => bool) => ('a word => bool) => bool)


505 
((PWORDLEN::nat => 'a word => bool) n2)


506 
(%w2::'a word.


507 
(All::(nat => bool) => bool)


508 
(%k::nat.


509 
(op >::bool => bool => bool)


510 
((op <::nat => nat => bool) k n2)


511 
((op =::'a => 'a => bool)


512 
((bit::nat => 'a word => 'a) k


513 
((WCAT::'a word * 'a word => 'a word)


514 
((Pair::'a word


515 
=> 'a word => 'a word * 'a word)


516 
w1 w2)))


517 
((bit::nat => 'a word => 'a) k w2)))))))"

14516

518 
by (import word_base BIT_WCAT_SND)


519 


520 
lemma BIT_WCAT1: "ALL n. RES_FORALL (PWORDLEN n) (%w. ALL b. bit n (WCAT (WORD [b], w)) = b)"


521 
by (import word_base BIT_WCAT1)


522 


523 
lemma WSEG_WCAT_WSEG1: "ALL n1 n2.


524 
RES_FORALL (PWORDLEN n1)


525 
(%w1. RES_FORALL (PWORDLEN n2)


526 
(%w2. ALL m k.


527 
m <= n1 & n2 <= k >


528 
WSEG m k (WCAT (w1, w2)) = WSEG m (k  n2) w1))"


529 
by (import word_base WSEG_WCAT_WSEG1)


530 


531 
lemma WSEG_WCAT_WSEG2: "ALL n1 n2.


532 
RES_FORALL (PWORDLEN n1)


533 
(%w1. RES_FORALL (PWORDLEN n2)


534 
(%w2. ALL m k.


535 
m + k <= n2 > WSEG m k (WCAT (w1, w2)) = WSEG m k w2))"


536 
by (import word_base WSEG_WCAT_WSEG2)


537 


538 
lemma WSEG_WCAT_WSEG: "ALL n1 n2.


539 
RES_FORALL (PWORDLEN n1)


540 
(%w1. RES_FORALL (PWORDLEN n2)


541 
(%w2. ALL m k.


542 
m + k <= n1 + n2 & k < n2 & n2 <= m + k >


543 
WSEG m k (WCAT (w1, w2)) =


544 
WCAT (WSEG (m + k  n2) 0 w1, WSEG (n2  k) k w2)))"


545 
by (import word_base WSEG_WCAT_WSEG)


546 

14847

547 
lemma BIT_EQ_IMP_WORD_EQ: "(All::(nat => bool) => bool)


548 
(%n::nat.


549 
(RES_FORALL::('a word => bool) => ('a word => bool) => bool)


550 
((PWORDLEN::nat => 'a word => bool) n)


551 
(%w1::'a word.


552 
(RES_FORALL::('a word => bool) => ('a word => bool) => bool)


553 
((PWORDLEN::nat => 'a word => bool) n)


554 
(%w2::'a word.


555 
(op >::bool => bool => bool)


556 
((All::(nat => bool) => bool)


557 
(%k::nat.


558 
(op >::bool => bool => bool)


559 
((op <::nat => nat => bool) k n)


560 
((op =::'a => 'a => bool)


561 
((bit::nat => 'a word => 'a) k w1)


562 
((bit::nat => 'a word => 'a) k w2))))


563 
((op =::'a word => 'a word => bool) w1 w2))))"

14516

564 
by (import word_base BIT_EQ_IMP_WORD_EQ)


565 


566 
;end_setup


567 


568 
;setup_theory word_num


569 


570 
constdefs


571 
LVAL :: "('a => nat) => nat => 'a list => nat"


572 
"LVAL == %f b. foldl (%e x. b * e + f x) 0"


573 


574 
lemma LVAL_DEF: "ALL f b l. LVAL f b l = foldl (%e x. b * e + f x) 0 l"


575 
by (import word_num LVAL_DEF)


576 


577 
consts


578 
NVAL :: "('a => nat) => nat => 'a word => nat"


579 


580 
specification (NVAL) NVAL_DEF: "ALL f b l. NVAL f b (WORD l) = LVAL f b l"


581 
by (import word_num NVAL_DEF)


582 


583 
lemma LVAL: "(ALL (x::'a => nat) xa::nat. LVAL x xa [] = (0::nat)) &


584 
(ALL (x::'a list) (xa::'a => nat) (xb::nat) xc::'a.


585 
LVAL xa xb (xc # x) = xa xc * xb ^ length x + LVAL xa xb x)"


586 
by (import word_num LVAL)


587 


588 
lemma LVAL_SNOC: "ALL l h f b. LVAL f b (SNOC h l) = LVAL f b l * b + f h"


589 
by (import word_num LVAL_SNOC)


590 


591 
lemma LVAL_MAX: "ALL l f b. (ALL x. f x < b) > LVAL f b l < b ^ length l"


592 
by (import word_num LVAL_MAX)


593 


594 
lemma NVAL_MAX: "ALL f b.


595 
(ALL x. f x < b) >


596 
(ALL n. RES_FORALL (PWORDLEN n) (%w. NVAL f b w < b ^ n))"


597 
by (import word_num NVAL_MAX)


598 


599 
lemma NVAL0: "ALL x xa. NVAL x xa (WORD []) = 0"


600 
by (import word_num NVAL0)


601 


602 
lemma NVAL1: "ALL x xa xb. NVAL x xa (WORD [xb]) = x xb"


603 
by (import word_num NVAL1)


604 


605 
lemma NVAL_WORDLEN_0: "RES_FORALL (PWORDLEN 0) (%w. ALL fv r. NVAL fv r w = 0)"


606 
by (import word_num NVAL_WORDLEN_0)


607 


608 
lemma NVAL_WCAT1: "ALL w f b x. NVAL f b (WCAT (w, WORD [x])) = NVAL f b w * b + f x"


609 
by (import word_num NVAL_WCAT1)


610 


611 
lemma NVAL_WCAT2: "ALL n.


612 
RES_FORALL (PWORDLEN n)


613 
(%w. ALL f b x.


614 
NVAL f b (WCAT (WORD [x], w)) = f x * b ^ n + NVAL f b w)"


615 
by (import word_num NVAL_WCAT2)


616 


617 
lemma NVAL_WCAT: "ALL n m.


618 
RES_FORALL (PWORDLEN n)


619 
(%w1. RES_FORALL (PWORDLEN m)


620 
(%w2. ALL f b.


621 
NVAL f b (WCAT (w1, w2)) =


622 
NVAL f b w1 * b ^ m + NVAL f b w2))"


623 
by (import word_num NVAL_WCAT)


624 


625 
consts


626 
NLIST :: "nat => (nat => 'a) => nat => nat => 'a list"


627 


628 
specification (NLIST) NLIST_DEF: "(ALL (frep::nat => 'a) (b::nat) m::nat. NLIST (0::nat) frep b m = []) &


629 
(ALL (n::nat) (frep::nat => 'a) (b::nat) m::nat.


630 
NLIST (Suc n) frep b m =


631 
SNOC (frep (m mod b)) (NLIST n frep b (m div b)))"


632 
by (import word_num NLIST_DEF)


633 


634 
constdefs


635 
NWORD :: "nat => (nat => 'a) => nat => nat => 'a word"


636 
"NWORD == %n frep b m. WORD (NLIST n frep b m)"


637 


638 
lemma NWORD_DEF: "ALL n frep b m. NWORD n frep b m = WORD (NLIST n frep b m)"


639 
by (import word_num NWORD_DEF)


640 


641 
lemma NWORD_LENGTH: "ALL x xa xb xc. WORDLEN (NWORD x xa xb xc) = x"


642 
by (import word_num NWORD_LENGTH)


643 


644 
lemma NWORD_PWORDLEN: "ALL x xa xb xc. IN (NWORD x xa xb xc) (PWORDLEN x)"


645 
by (import word_num NWORD_PWORDLEN)


646 


647 
;end_setup


648 


649 
;setup_theory word_bitop


650 


651 
consts


652 
PBITOP :: "('a word => 'b word) => bool"


653 


654 
defs


655 
PBITOP_primdef: "PBITOP ==


656 
GSPEC


657 
(%oper.


658 
(oper,


659 
ALL n.


660 
RES_FORALL (PWORDLEN n)


661 
(%w. IN (oper w) (PWORDLEN n) &


662 
(ALL m k.


663 
m + k <= n > oper (WSEG m k w) = WSEG m k (oper w)))))"


664 


665 
lemma PBITOP_def: "PBITOP =


666 
GSPEC


667 
(%oper.


668 
(oper,


669 
ALL n.


670 
RES_FORALL (PWORDLEN n)


671 
(%w. IN (oper w) (PWORDLEN n) &


672 
(ALL m k.


673 
m + k <= n > oper (WSEG m k w) = WSEG m k (oper w)))))"


674 
by (import word_bitop PBITOP_def)


675 


676 
lemma IN_PBITOP: "ALL oper.


677 
IN oper PBITOP =


678 
(ALL n.


679 
RES_FORALL (PWORDLEN n)


680 
(%w. IN (oper w) (PWORDLEN n) &


681 
(ALL m k.


682 
m + k <= n > oper (WSEG m k w) = WSEG m k (oper w))))"


683 
by (import word_bitop IN_PBITOP)


684 


685 
lemma PBITOP_PWORDLEN: "RES_FORALL PBITOP


686 
(%oper. ALL n. RES_FORALL (PWORDLEN n) (%w. IN (oper w) (PWORDLEN n)))"


687 
by (import word_bitop PBITOP_PWORDLEN)


688 


689 
lemma PBITOP_WSEG: "RES_FORALL PBITOP


690 
(%oper.


691 
ALL n.


692 
RES_FORALL (PWORDLEN n)


693 
(%w. ALL m k.


694 
m + k <= n > oper (WSEG m k w) = WSEG m k (oper w)))"


695 
by (import word_bitop PBITOP_WSEG)


696 

14847

697 
lemma PBITOP_BIT: "(RES_FORALL::(('a word => 'b word) => bool)


698 
=> (('a word => 'b word) => bool) => bool)


699 
(PBITOP::('a word => 'b word) => bool)


700 
(%oper::'a word => 'b word.


701 
(All::(nat => bool) => bool)


702 
(%n::nat.


703 
(RES_FORALL::('a word => bool) => ('a word => bool) => bool)


704 
((PWORDLEN::nat => 'a word => bool) n)


705 
(%w::'a word.


706 
(All::(nat => bool) => bool)


707 
(%k::nat.


708 
(op >::bool => bool => bool)


709 
((op <::nat => nat => bool) k n)


710 
((op =::'b word => 'b word => bool)


711 
(oper


712 
((WORD::'a list => 'a word)


713 
((op #::'a => 'a list => 'a list)


714 
((bit::nat => 'a word => 'a) k w)


715 
([]::'a list))))


716 
((WORD::'b list => 'b word)


717 
((op #::'b => 'b list => 'b list)


718 
((bit::nat => 'b word => 'b) k (oper w))


719 
([]::'b list))))))))"

14516

720 
by (import word_bitop PBITOP_BIT)


721 


722 
consts


723 
PBITBOP :: "('a word => 'b word => 'c word) => bool"


724 


725 
defs


726 
PBITBOP_primdef: "PBITBOP ==


727 
GSPEC


728 
(%oper.


729 
(oper,


730 
ALL n.


731 
RES_FORALL (PWORDLEN n)


732 
(%w1. RES_FORALL (PWORDLEN n)


733 
(%w2. IN (oper w1 w2) (PWORDLEN n) &


734 
(ALL m k.


735 
m + k <= n >


736 
oper (WSEG m k w1) (WSEG m k w2) =


737 
WSEG m k (oper w1 w2))))))"


738 


739 
lemma PBITBOP_def: "PBITBOP =


740 
GSPEC


741 
(%oper.


742 
(oper,


743 
ALL n.


744 
RES_FORALL (PWORDLEN n)


745 
(%w1. RES_FORALL (PWORDLEN n)


746 
(%w2. IN (oper w1 w2) (PWORDLEN n) &


747 
(ALL m k.


748 
m + k <= n >


749 
oper (WSEG m k w1) (WSEG m k w2) =


750 
WSEG m k (oper w1 w2))))))"


751 
by (import word_bitop PBITBOP_def)


752 


753 
lemma IN_PBITBOP: "ALL oper.


754 
IN oper PBITBOP =


755 
(ALL n.


756 
RES_FORALL (PWORDLEN n)


757 
(%w1. RES_FORALL (PWORDLEN n)


758 
(%w2. IN (oper w1 w2) (PWORDLEN n) &


759 
(ALL m k.


760 
m + k <= n >


761 
oper (WSEG m k w1) (WSEG m k w2) =


762 
WSEG m k (oper w1 w2)))))"


763 
by (import word_bitop IN_PBITBOP)


764 


765 
lemma PBITBOP_PWORDLEN: "RES_FORALL PBITBOP


766 
(%oper.


767 
ALL n.


768 
RES_FORALL (PWORDLEN n)


769 
(%w1. RES_FORALL (PWORDLEN n) (%w2. IN (oper w1 w2) (PWORDLEN n))))"


770 
by (import word_bitop PBITBOP_PWORDLEN)


771 


772 
lemma PBITBOP_WSEG: "RES_FORALL PBITBOP


773 
(%oper.


774 
ALL n.


775 
RES_FORALL (PWORDLEN n)


776 
(%w1. RES_FORALL (PWORDLEN n)


777 
(%w2. ALL m k.


778 
m + k <= n >


779 
oper (WSEG m k w1) (WSEG m k w2) =


780 
WSEG m k (oper w1 w2))))"


781 
by (import word_bitop PBITBOP_WSEG)


782 


783 
lemma PBITBOP_EXISTS: "ALL f. EX x. ALL l1 l2. x (WORD l1) (WORD l2) = WORD (map2 f l1 l2)"


784 
by (import word_bitop PBITBOP_EXISTS)


785 


786 
consts


787 
WMAP :: "('a => 'b) => 'a word => 'b word"


788 


789 
specification (WMAP) WMAP_DEF: "ALL f l. WMAP f (WORD l) = WORD (map f l)"


790 
by (import word_bitop WMAP_DEF)


791 


792 
lemma WMAP_PWORDLEN: "RES_FORALL (PWORDLEN n) (%w. ALL f. IN (WMAP f w) (PWORDLEN n))"


793 
by (import word_bitop WMAP_PWORDLEN)


794 


795 
lemma WMAP_0: "ALL x. WMAP x (WORD []) = WORD []"


796 
by (import word_bitop WMAP_0)


797 

14847

798 
lemma WMAP_BIT: "(All::(nat => bool) => bool)


799 
(%n::nat.


800 
(RES_FORALL::('a word => bool) => ('a word => bool) => bool)


801 
((PWORDLEN::nat => 'a word => bool) n)


802 
(%w::'a word.


803 
(All::(nat => bool) => bool)


804 
(%k::nat.


805 
(op >::bool => bool => bool)


806 
((op <::nat => nat => bool) k n)


807 
((All::(('a => 'b) => bool) => bool)


808 
(%f::'a => 'b.


809 
(op =::'b => 'b => bool)


810 
((bit::nat => 'b word => 'b) k


811 
((WMAP::('a => 'b) => 'a word => 'b word) f w))


812 
(f ((bit::nat => 'a word => 'a) k w)))))))"

14516

813 
by (import word_bitop WMAP_BIT)


814 


815 
lemma WMAP_WSEG: "ALL n.


816 
RES_FORALL (PWORDLEN n)


817 
(%w. ALL m k.


818 
m + k <= n >


819 
(ALL f. WMAP f (WSEG m k w) = WSEG m k (WMAP f w)))"


820 
by (import word_bitop WMAP_WSEG)


821 


822 
lemma WMAP_PBITOP: "ALL f. IN (WMAP f) PBITOP"


823 
by (import word_bitop WMAP_PBITOP)


824 


825 
lemma WMAP_WCAT: "ALL w1 w2 f. WMAP f (WCAT (w1, w2)) = WCAT (WMAP f w1, WMAP f w2)"


826 
by (import word_bitop WMAP_WCAT)


827 


828 
lemma WMAP_o: "ALL w f g. WMAP g (WMAP f w) = WMAP (g o f) w"


829 
by (import word_bitop WMAP_o)


830 


831 
consts


832 
FORALLBITS :: "('a => bool) => 'a word => bool"


833 


834 
specification (FORALLBITS) FORALLBITS_DEF: "ALL P l. FORALLBITS P (WORD l) = list_all P l"


835 
by (import word_bitop FORALLBITS_DEF)


836 

14847

837 
lemma FORALLBITS: "(All::(nat => bool) => bool)


838 
(%n::nat.


839 
(RES_FORALL::('a word => bool) => ('a word => bool) => bool)


840 
((PWORDLEN::nat => 'a word => bool) n)


841 
(%w::'a word.


842 
(All::(('a => bool) => bool) => bool)


843 
(%P::'a => bool.


844 
(op =::bool => bool => bool)


845 
((FORALLBITS::('a => bool) => 'a word => bool) P w)


846 
((All::(nat => bool) => bool)


847 
(%k::nat.


848 
(op >::bool => bool => bool)


849 
((op <::nat => nat => bool) k n)


850 
(P ((bit::nat => 'a word => 'a) k w)))))))"

14516

851 
by (import word_bitop FORALLBITS)


852 


853 
lemma FORALLBITS_WSEG: "ALL n.


854 
RES_FORALL (PWORDLEN n)


855 
(%w. ALL P.


856 
FORALLBITS P w >


857 
(ALL m k. m + k <= n > FORALLBITS P (WSEG m k w)))"


858 
by (import word_bitop FORALLBITS_WSEG)


859 


860 
lemma FORALLBITS_WCAT: "ALL w1 w2 P.


861 
FORALLBITS P (WCAT (w1, w2)) = (FORALLBITS P w1 & FORALLBITS P w2)"


862 
by (import word_bitop FORALLBITS_WCAT)


863 


864 
consts


865 
EXISTSABIT :: "('a => bool) => 'a word => bool"


866 


867 
specification (EXISTSABIT) EXISTSABIT_DEF: "ALL P l. EXISTSABIT P (WORD l) = list_exists P l"


868 
by (import word_bitop EXISTSABIT_DEF)


869 


870 
lemma NOT_EXISTSABIT: "ALL P w. (~ EXISTSABIT P w) = FORALLBITS (Not o P) w"


871 
by (import word_bitop NOT_EXISTSABIT)


872 


873 
lemma NOT_FORALLBITS: "ALL P w. (~ FORALLBITS P w) = EXISTSABIT (Not o P) w"


874 
by (import word_bitop NOT_FORALLBITS)


875 

14847

876 
lemma EXISTSABIT: "(All::(nat => bool) => bool)


877 
(%n::nat.


878 
(RES_FORALL::('a word => bool) => ('a word => bool) => bool)


879 
((PWORDLEN::nat => 'a word => bool) n)


880 
(%w::'a word.


881 
(All::(('a => bool) => bool) => bool)


882 
(%P::'a => bool.


883 
(op =::bool => bool => bool)


884 
((EXISTSABIT::('a => bool) => 'a word => bool) P w)


885 
((Ex::(nat => bool) => bool)


886 
(%k::nat.


887 
(op &::bool => bool => bool)


888 
((op <::nat => nat => bool) k n)


889 
(P ((bit::nat => 'a word => 'a) k w)))))))"

14516

890 
by (import word_bitop EXISTSABIT)


891 


892 
lemma EXISTSABIT_WSEG: "ALL n.


893 
RES_FORALL (PWORDLEN n)


894 
(%w. ALL m k.


895 
m + k <= n >


896 
(ALL P. EXISTSABIT P (WSEG m k w) > EXISTSABIT P w))"


897 
by (import word_bitop EXISTSABIT_WSEG)


898 


899 
lemma EXISTSABIT_WCAT: "ALL w1 w2 P.


900 
EXISTSABIT P (WCAT (w1, w2)) = (EXISTSABIT P w1  EXISTSABIT P w2)"


901 
by (import word_bitop EXISTSABIT_WCAT)


902 


903 
constdefs


904 
SHR :: "bool => 'a => 'a word => 'a word * 'a"


905 
"SHR ==


906 
%f b w.


907 
(WCAT


908 
(if f then WSEG 1 (PRE (WORDLEN w)) w else WORD [b],


909 
WSEG (PRE (WORDLEN w)) 1 w),


910 
bit 0 w)"


911 


912 
lemma SHR_DEF: "ALL f b w.


913 
SHR f b w =


914 
(WCAT


915 
(if f then WSEG 1 (PRE (WORDLEN w)) w else WORD [b],


916 
WSEG (PRE (WORDLEN w)) 1 w),


917 
bit 0 w)"


918 
by (import word_bitop SHR_DEF)


919 


920 
constdefs


921 
SHL :: "bool => 'a word => 'a => 'a * 'a word"


922 
"SHL ==


923 
%f w b.


924 
(bit (PRE (WORDLEN w)) w,


925 
WCAT (WSEG (PRE (WORDLEN w)) 0 w, if f then WSEG 1 0 w else WORD [b]))"


926 


927 
lemma SHL_DEF: "ALL f w b.


928 
SHL f w b =


929 
(bit (PRE (WORDLEN w)) w,


930 
WCAT (WSEG (PRE (WORDLEN w)) 0 w, if f then WSEG 1 0 w else WORD [b]))"


931 
by (import word_bitop SHL_DEF)


932 


933 
lemma SHR_WSEG: "ALL n.


934 
RES_FORALL (PWORDLEN n)


935 
(%w. ALL m k.


936 
m + k <= n >


937 
0 < m >


938 
(ALL f b.


939 
SHR f b (WSEG m k w) =


940 
(if f


941 
then WCAT (WSEG 1 (k + (m  1)) w, WSEG (m  1) (k + 1) w)


942 
else WCAT (WORD [b], WSEG (m  1) (k + 1) w),


943 
bit k w)))"


944 
by (import word_bitop SHR_WSEG)


945 


946 
lemma SHR_WSEG_1F: "ALL n.


947 
RES_FORALL (PWORDLEN n)


948 
(%w. ALL b m k.


949 
m + k <= n >


950 
0 < m >


951 
SHR False b (WSEG m k w) =


952 
(WCAT (WORD [b], WSEG (m  1) (k + 1) w), bit k w))"


953 
by (import word_bitop SHR_WSEG_1F)


954 


955 
lemma SHR_WSEG_NF: "ALL n.


956 
RES_FORALL (PWORDLEN n)


957 
(%w. ALL m k.


958 
m + k < n >


959 
0 < m >


960 
SHR False (bit (m + k) w) (WSEG m k w) =


961 
(WSEG m (k + 1) w, bit k w))"


962 
by (import word_bitop SHR_WSEG_NF)


963 


964 
lemma SHL_WSEG: "ALL n.


965 
RES_FORALL (PWORDLEN n)


966 
(%w. ALL m k.


967 
m + k <= n >


968 
0 < m >


969 
(ALL f b.


970 
SHL f (WSEG m k w) b =


971 
(bit (k + (m  1)) w,


972 
if f then WCAT (WSEG (m  1) k w, WSEG 1 k w)


973 
else WCAT (WSEG (m  1) k w, WORD [b]))))"


974 
by (import word_bitop SHL_WSEG)


975 


976 
lemma SHL_WSEG_1F: "ALL n.


977 
RES_FORALL (PWORDLEN n)


978 
(%w. ALL b m k.


979 
m + k <= n >


980 
0 < m >


981 
SHL False (WSEG m k w) b =


982 
(bit (k + (m  1)) w, WCAT (WSEG (m  1) k w, WORD [b])))"


983 
by (import word_bitop SHL_WSEG_1F)


984 


985 
lemma SHL_WSEG_NF: "ALL n.


986 
RES_FORALL (PWORDLEN n)


987 
(%w. ALL m k.


988 
m + k <= n >


989 
0 < m >


990 
0 < k >


991 
SHL False (WSEG m k w) (bit (k  1) w) =


992 
(bit (k + (m  1)) w, WSEG m (k  1) w))"


993 
by (import word_bitop SHL_WSEG_NF)


994 


995 
lemma WSEG_SHL: "ALL n.


996 
RES_FORALL (PWORDLEN (Suc n))


997 
(%w. ALL m k.


998 
0 < k & m + k <= Suc n >


999 
(ALL b. WSEG m k (snd (SHL f w b)) = WSEG m (k  1) w))"


1000 
by (import word_bitop WSEG_SHL)


1001 


1002 
lemma WSEG_SHL_0: "ALL n.


1003 
RES_FORALL (PWORDLEN (Suc n))


1004 
(%w. ALL m b.


1005 
0 < m & m <= Suc n >


1006 
WSEG m 0 (snd (SHL f w b)) =


1007 
WCAT (WSEG (m  1) 0 w, if f then WSEG 1 0 w else WORD [b]))"


1008 
by (import word_bitop WSEG_SHL_0)


1009 


1010 
;end_setup


1011 


1012 
;setup_theory bword_num


1013 


1014 
constdefs


1015 
BV :: "bool => nat"


1016 
"BV == %b. if b then Suc 0 else 0"


1017 


1018 
lemma BV_DEF: "ALL b. BV b = (if b then Suc 0 else 0)"


1019 
by (import bword_num BV_DEF)


1020 


1021 
consts


1022 
BNVAL :: "bool word => nat"


1023 


1024 
specification (BNVAL) BNVAL_DEF: "ALL l. BNVAL (WORD l) = LVAL BV 2 l"


1025 
by (import bword_num BNVAL_DEF)


1026 


1027 
lemma BV_LESS_2: "ALL x. BV x < 2"


1028 
by (import bword_num BV_LESS_2)


1029 


1030 
lemma BNVAL_NVAL: "ALL w. BNVAL w = NVAL BV 2 w"


1031 
by (import bword_num BNVAL_NVAL)


1032 


1033 
lemma BNVAL0: "BNVAL (WORD []) = 0"


1034 
by (import bword_num BNVAL0)


1035 


1036 
lemma BNVAL_11: "ALL w1 w2. WORDLEN w1 = WORDLEN w2 > BNVAL w1 = BNVAL w2 > w1 = w2"


1037 
by (import bword_num BNVAL_11)


1038 


1039 
lemma BNVAL_ONTO: "ALL w. Ex (op = (BNVAL w))"


1040 
by (import bword_num BNVAL_ONTO)


1041 


1042 
lemma BNVAL_MAX: "ALL n. RES_FORALL (PWORDLEN n) (%w. BNVAL w < 2 ^ n)"


1043 
by (import bword_num BNVAL_MAX)


1044 


1045 
lemma BNVAL_WCAT1: "ALL n.


1046 
RES_FORALL (PWORDLEN n)


1047 
(%w. ALL x. BNVAL (WCAT (w, WORD [x])) = BNVAL w * 2 + BV x)"


1048 
by (import bword_num BNVAL_WCAT1)


1049 


1050 
lemma BNVAL_WCAT2: "ALL n.


1051 
RES_FORALL (PWORDLEN n)


1052 
(%w. ALL x. BNVAL (WCAT (WORD [x], w)) = BV x * 2 ^ n + BNVAL w)"


1053 
by (import bword_num BNVAL_WCAT2)


1054 


1055 
lemma BNVAL_WCAT: "ALL n m.


1056 
RES_FORALL (PWORDLEN n)


1057 
(%w1. RES_FORALL (PWORDLEN m)


1058 
(%w2. BNVAL (WCAT (w1, w2)) = BNVAL w1 * 2 ^ m + BNVAL w2))"


1059 
by (import bword_num BNVAL_WCAT)


1060 


1061 
constdefs


1062 
VB :: "nat => bool"


1063 
"VB == %n. n mod 2 ~= 0"


1064 


1065 
lemma VB_DEF: "ALL n. VB n = (n mod 2 ~= 0)"


1066 
by (import bword_num VB_DEF)


1067 


1068 
constdefs


1069 
NBWORD :: "nat => nat => bool word"


1070 
"NBWORD == %n m. WORD (NLIST n VB 2 m)"


1071 


1072 
lemma NBWORD_DEF: "ALL n m. NBWORD n m = WORD (NLIST n VB 2 m)"


1073 
by (import bword_num NBWORD_DEF)


1074 


1075 
lemma NBWORD0: "ALL x. NBWORD 0 x = WORD []"


1076 
by (import bword_num NBWORD0)


1077 


1078 
lemma WORDLEN_NBWORD: "ALL x xa. WORDLEN (NBWORD x xa) = x"


1079 
by (import bword_num WORDLEN_NBWORD)


1080 


1081 
lemma PWORDLEN_NBWORD: "ALL x xa. IN (NBWORD x xa) (PWORDLEN x)"


1082 
by (import bword_num PWORDLEN_NBWORD)


1083 


1084 
lemma NBWORD_SUC: "ALL n m. NBWORD (Suc n) m = WCAT (NBWORD n (m div 2), WORD [VB (m mod 2)])"


1085 
by (import bword_num NBWORD_SUC)


1086 


1087 
lemma VB_BV: "ALL x. VB (BV x) = x"


1088 
by (import bword_num VB_BV)


1089 

14847

1090 
lemma BV_VB: "(All::(nat => bool) => bool)


1091 
(%x::nat.


1092 
(op >::bool => bool => bool)


1093 
((op <::nat => nat => bool) x


1094 
((number_of::bin => nat)

15647

1095 
((op BIT::bin => bit => bin)


1096 
((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))


1097 
(bit.B0::bit))))

14847

1098 
((op =::nat => nat => bool) ((BV::bool => nat) ((VB::nat => bool) x))


1099 
x))"

14516

1100 
by (import bword_num BV_VB)


1101 


1102 
lemma NBWORD_BNVAL: "ALL n. RES_FORALL (PWORDLEN n) (%w. NBWORD n (BNVAL w) = w)"


1103 
by (import bword_num NBWORD_BNVAL)


1104 


1105 
lemma BNVAL_NBWORD: "ALL n m. m < 2 ^ n > BNVAL (NBWORD n m) = m"


1106 
by (import bword_num BNVAL_NBWORD)


1107 


1108 
lemma ZERO_WORD_VAL: "RES_FORALL (PWORDLEN n) (%w. (w = NBWORD n 0) = (BNVAL w = 0))"


1109 
by (import bword_num ZERO_WORD_VAL)


1110 


1111 
lemma WCAT_NBWORD_0: "ALL n1 n2. WCAT (NBWORD n1 0, NBWORD n2 0) = NBWORD (n1 + n2) 0"


1112 
by (import bword_num WCAT_NBWORD_0)


1113 


1114 
lemma WSPLIT_NBWORD_0: "ALL n m. m <= n > WSPLIT m (NBWORD n 0) = (NBWORD (n  m) 0, NBWORD m 0)"


1115 
by (import bword_num WSPLIT_NBWORD_0)


1116 

14847

1117 
lemma EQ_NBWORD0_SPLIT: "(All::(nat => bool) => bool)


1118 
(%n::nat.


1119 
(RES_FORALL::(bool word => bool) => (bool word => bool) => bool)


1120 
((PWORDLEN::nat => bool word => bool) n)


1121 
(%w::bool word.


1122 
(All::(nat => bool) => bool)


1123 
(%m::nat.


1124 
(op >::bool => bool => bool)


1125 
((op <=::nat => nat => bool) m n)


1126 
((op =::bool => bool => bool)


1127 
((op =::bool word => bool word => bool) w


1128 
((NBWORD::nat => nat => bool word) n (0::nat)))


1129 
((op &::bool => bool => bool)


1130 
((op =::bool word => bool word => bool)


1131 
((WSEG::nat => nat => bool word => bool word)


1132 
((op ::nat => nat => nat) n m) m w)


1133 
((NBWORD::nat => nat => bool word)


1134 
((op ::nat => nat => nat) n m) (0::nat)))


1135 
((op =::bool word => bool word => bool)


1136 
((WSEG::nat => nat => bool word => bool word) m


1137 
(0::nat) w)


1138 
((NBWORD::nat => nat => bool word) m (0::nat))))))))"

14516

1139 
by (import bword_num EQ_NBWORD0_SPLIT)


1140 


1141 
lemma NBWORD_MOD: "ALL n m. NBWORD n (m mod 2 ^ n) = NBWORD n m"


1142 
by (import bword_num NBWORD_MOD)


1143 


1144 
lemma WSEG_NBWORD_SUC: "ALL n m. WSEG n 0 (NBWORD (Suc n) m) = NBWORD n m"


1145 
by (import bword_num WSEG_NBWORD_SUC)


1146 


1147 
lemma NBWORD_SUC_WSEG: "ALL n. RES_FORALL (PWORDLEN (Suc n)) (%w. NBWORD n (BNVAL w) = WSEG n 0 w)"


1148 
by (import bword_num NBWORD_SUC_WSEG)


1149 

15647

1150 
lemma DOUBL_EQ_SHL: "ALL x>0.

14516

1151 
RES_FORALL (PWORDLEN x)


1152 
(%xa. ALL xb.


1153 
NBWORD x (BNVAL xa + BNVAL xa + BV xb) = snd (SHL False xa xb))"


1154 
by (import bword_num DOUBL_EQ_SHL)


1155 


1156 
lemma MSB_NBWORD: "ALL n m. bit n (NBWORD (Suc n) m) = VB (m div 2 ^ n mod 2)"


1157 
by (import bword_num MSB_NBWORD)


1158 


1159 
lemma NBWORD_SPLIT: "ALL n1 n2 m.


1160 
NBWORD (n1 + n2) m = WCAT (NBWORD n1 (m div 2 ^ n2), NBWORD n2 m)"


1161 
by (import bword_num NBWORD_SPLIT)


1162 


1163 
lemma WSEG_NBWORD: "ALL m k n.


1164 
m + k <= n > (ALL l. WSEG m k (NBWORD n l) = NBWORD m (l div 2 ^ k))"


1165 
by (import bword_num WSEG_NBWORD)


1166 


1167 
lemma NBWORD_SUC_FST: "ALL n x. NBWORD (Suc n) x = WCAT (WORD [VB (x div 2 ^ n mod 2)], NBWORD n x)"


1168 
by (import bword_num NBWORD_SUC_FST)


1169 


1170 
lemma BIT_NBWORD0: "ALL k n. k < n > bit k (NBWORD n 0) = False"


1171 
by (import bword_num BIT_NBWORD0)


1172 


1173 
lemma ADD_BNVAL_LEFT: "ALL n.


1174 
RES_FORALL (PWORDLEN (Suc n))


1175 
(%w1. RES_FORALL (PWORDLEN (Suc n))


1176 
(%w2. BNVAL w1 + BNVAL w2 =


1177 
(BV (bit n w1) + BV (bit n w2)) * 2 ^ n +


1178 
(BNVAL (WSEG n 0 w1) + BNVAL (WSEG n 0 w2))))"


1179 
by (import bword_num ADD_BNVAL_LEFT)


1180 


1181 
lemma ADD_BNVAL_RIGHT: "ALL n.


1182 
RES_FORALL (PWORDLEN (Suc n))


1183 
(%w1. RES_FORALL (PWORDLEN (Suc n))


1184 
(%w2. BNVAL w1 + BNVAL w2 =


1185 
(BNVAL (WSEG n 1 w1) + BNVAL (WSEG n 1 w2)) * 2 +


1186 
(BV (bit 0 w1) + BV (bit 0 w2))))"


1187 
by (import bword_num ADD_BNVAL_RIGHT)


1188 


1189 
lemma ADD_BNVAL_SPLIT: "ALL n1 n2.


1190 
RES_FORALL (PWORDLEN (n1 + n2))


1191 
(%w1. RES_FORALL (PWORDLEN (n1 + n2))


1192 
(%w2. BNVAL w1 + BNVAL w2 =


1193 
(BNVAL (WSEG n1 n2 w1) + BNVAL (WSEG n1 n2 w2)) * 2 ^ n2 +


1194 
(BNVAL (WSEG n2 0 w1) + BNVAL (WSEG n2 0 w2))))"


1195 
by (import bword_num ADD_BNVAL_SPLIT)


1196 


1197 
;end_setup


1198 


1199 
;setup_theory bword_arith


1200 


1201 
consts


1202 
ACARRY :: "nat => bool word => bool word => bool => bool"


1203 


1204 
specification (ACARRY) ACARRY_DEF: "(ALL w1 w2 cin. ACARRY 0 w1 w2 cin = cin) &


1205 
(ALL n w1 w2 cin.


1206 
ACARRY (Suc n) w1 w2 cin =


1207 
VB ((BV (bit n w1) + BV (bit n w2) + BV (ACARRY n w1 w2 cin)) div 2))"


1208 
by (import bword_arith ACARRY_DEF)


1209 


1210 
consts


1211 
ICARRY :: "nat => bool word => bool word => bool => bool"


1212 


1213 
specification (ICARRY) ICARRY_DEF: "(ALL w1 w2 cin. ICARRY 0 w1 w2 cin = cin) &


1214 
(ALL n w1 w2 cin.


1215 
ICARRY (Suc n) w1 w2 cin =


1216 
(bit n w1 & bit n w2  (bit n w1  bit n w2) & ICARRY n w1 w2 cin))"


1217 
by (import bword_arith ICARRY_DEF)


1218 


1219 
lemma ACARRY_EQ_ICARRY: "ALL n.


1220 
RES_FORALL (PWORDLEN n)


1221 
(%w1. RES_FORALL (PWORDLEN n)


1222 
(%w2. ALL cin k.


1223 
k <= n > ACARRY k w1 w2 cin = ICARRY k w1 w2 cin))"


1224 
by (import bword_arith ACARRY_EQ_ICARRY)


1225 


1226 
lemma BNVAL_LESS_EQ: "ALL n. RES_FORALL (PWORDLEN n) (%w. BNVAL w <= 2 ^ n  1)"


1227 
by (import bword_arith BNVAL_LESS_EQ)


1228 


1229 
lemma ADD_BNVAL_LESS_EQ1: "ALL n cin.


1230 
RES_FORALL (PWORDLEN n)


1231 
(%w1. RES_FORALL (PWORDLEN n)


1232 
(%w2. (BNVAL w1 + (BNVAL w2 + BV cin)) div 2 ^ n <= Suc 0))"


1233 
by (import bword_arith ADD_BNVAL_LESS_EQ1)


1234 


1235 
lemma ADD_BV_BNVAL_DIV_LESS_EQ1: "ALL n x1 x2 cin.


1236 
RES_FORALL (PWORDLEN n)


1237 
(%w1. RES_FORALL (PWORDLEN n)


1238 
(%w2. (BV x1 + BV x2 +


1239 
(BNVAL w1 + (BNVAL w2 + BV cin)) div 2 ^ n) div


1240 
2


1241 
<= 1))"


1242 
by (import bword_arith ADD_BV_BNVAL_DIV_LESS_EQ1)


1243 


1244 
lemma ADD_BV_BNVAL_LESS_EQ: "ALL n x1 x2 cin.


1245 
RES_FORALL (PWORDLEN n)


1246 
(%w1. RES_FORALL (PWORDLEN n)


1247 
(%w2. BV x1 + BV x2 + (BNVAL w1 + (BNVAL w2 + BV cin))


1248 
<= Suc (2 ^ Suc n)))"


1249 
by (import bword_arith ADD_BV_BNVAL_LESS_EQ)


1250 


1251 
lemma ADD_BV_BNVAL_LESS_EQ1: "ALL n x1 x2 cin.


1252 
RES_FORALL (PWORDLEN n)


1253 
(%w1. RES_FORALL (PWORDLEN n)


1254 
(%w2. (BV x1 + BV x2 + (BNVAL w1 + (BNVAL w2 + BV cin))) div


1255 
2 ^ Suc n


1256 
<= 1))"


1257 
by (import bword_arith ADD_BV_BNVAL_LESS_EQ1)


1258 

14847

1259 
lemma ACARRY_EQ_ADD_DIV: "(All::(nat => bool) => bool)


1260 
(%n::nat.


1261 
(RES_FORALL::(bool word => bool) => (bool word => bool) => bool)


1262 
((PWORDLEN::nat => bool word => bool) n)


1263 
(%w1::bool word.


1264 
(RES_FORALL::(bool word => bool) => (bool word => bool) => bool)


1265 
((PWORDLEN::nat => bool word => bool) n)


1266 
(%w2::bool word.


1267 
(All::(nat => bool) => bool)


1268 
(%k::nat.


1269 
(op >::bool => bool => bool)


1270 
((op <::nat => nat => bool) k n)


1271 
((op =::nat => nat => bool)


1272 
((BV::bool => nat)


1273 
((ACARRY::nat


1274 
=> bool word


1275 
=> bool word => bool => bool)


1276 
k w1 w2 (cin::bool)))


1277 
((op div::nat => nat => nat)


1278 
((op +::nat => nat => nat)


1279 
((op +::nat => nat => nat)


1280 
((BNVAL::bool word => nat)


1281 
((WSEG::nat => nat => bool word => bool word)


1282 
k (0::nat) w1))


1283 
((BNVAL::bool word => nat)


1284 
((WSEG::nat => nat => bool word => bool word)


1285 
k (0::nat) w2)))


1286 
((BV::bool => nat) cin))


1287 
((op ^::nat => nat => nat)


1288 
((number_of::bin => nat)

15647

1289 
((op BIT::bin => bit => bin)


1290 
((op BIT::bin => bit => bin)


1291 
(Numeral.Pls::bin) (bit.B1::bit))


1292 
(bit.B0::bit)))

14847

1293 
k)))))))"

14516

1294 
by (import bword_arith ACARRY_EQ_ADD_DIV)


1295 


1296 
lemma ADD_WORD_SPLIT: "ALL n1 n2.


1297 
RES_FORALL (PWORDLEN (n1 + n2))


1298 
(%w1. RES_FORALL (PWORDLEN (n1 + n2))


1299 
(%w2. ALL cin.


1300 
NBWORD (n1 + n2) (BNVAL w1 + BNVAL w2 + BV cin) =


1301 
WCAT


1302 
(NBWORD n1


1303 
(BNVAL (WSEG n1 n2 w1) + BNVAL (WSEG n1 n2 w2) +


1304 
BV (ACARRY n2 w1 w2 cin)),


1305 
NBWORD n2


1306 
(BNVAL (WSEG n2 0 w1) + BNVAL (WSEG n2 0 w2) +


1307 
BV cin))))"


1308 
by (import bword_arith ADD_WORD_SPLIT)


1309 


1310 
lemma WSEG_NBWORD_ADD: "ALL n.


1311 
RES_FORALL (PWORDLEN n)


1312 
(%w1. RES_FORALL (PWORDLEN n)


1313 
(%w2. ALL m k cin.


1314 
m + k <= n >


1315 
WSEG m k (NBWORD n (BNVAL w1 + BNVAL w2 + BV cin)) =


1316 
NBWORD m


1317 
(BNVAL (WSEG m k w1) + BNVAL (WSEG m k w2) +


1318 
BV (ACARRY k w1 w2 cin))))"


1319 
by (import bword_arith WSEG_NBWORD_ADD)


1320 


1321 
lemma ADD_NBWORD_EQ0_SPLIT: "ALL n1 n2.


1322 
RES_FORALL (PWORDLEN (n1 + n2))


1323 
(%w1. RES_FORALL (PWORDLEN (n1 + n2))


1324 
(%w2. ALL cin.


1325 
(NBWORD (n1 + n2) (BNVAL w1 + BNVAL w2 + BV cin) =


1326 
NBWORD (n1 + n2) 0) =


1327 
(NBWORD n1


1328 
(BNVAL (WSEG n1 n2 w1) + BNVAL (WSEG n1 n2 w2) +


1329 
BV (ACARRY n2 w1 w2 cin)) =


1330 
NBWORD n1 0 &


1331 
NBWORD n2


1332 
(BNVAL (WSEG n2 0 w1) + BNVAL (WSEG n2 0 w2) +


1333 
BV cin) =


1334 
NBWORD n2 0)))"


1335 
by (import bword_arith ADD_NBWORD_EQ0_SPLIT)


1336 


1337 
lemma ACARRY_MSB: "ALL n.


1338 
RES_FORALL (PWORDLEN n)


1339 
(%w1. RES_FORALL (PWORDLEN n)


1340 
(%w2. ALL cin.


1341 
ACARRY n w1 w2 cin =


1342 
bit n (NBWORD (Suc n) (BNVAL w1 + BNVAL w2 + BV cin))))"


1343 
by (import bword_arith ACARRY_MSB)


1344 


1345 
lemma ACARRY_WSEG: "ALL n.


1346 
RES_FORALL (PWORDLEN n)


1347 
(%w1. RES_FORALL (PWORDLEN n)


1348 
(%w2. ALL cin k m.


1349 
k < m & m <= n >


1350 
ACARRY k (WSEG m 0 w1) (WSEG m 0 w2) cin =


1351 
ACARRY k w1 w2 cin))"


1352 
by (import bword_arith ACARRY_WSEG)


1353 


1354 
lemma ICARRY_WSEG: "ALL n.


1355 
RES_FORALL (PWORDLEN n)


1356 
(%w1. RES_FORALL (PWORDLEN n)


1357 
(%w2. ALL cin k m.


1358 
k < m & m <= n >


1359 
ICARRY k (WSEG m 0 w1) (WSEG m 0 w2) cin =


1360 
ICARRY k w1 w2 cin))"


1361 
by (import bword_arith ICARRY_WSEG)


1362 


1363 
lemma ACARRY_ACARRY_WSEG: "ALL n.


1364 
RES_FORALL (PWORDLEN n)


1365 
(%w1. RES_FORALL (PWORDLEN n)


1366 
(%w2. ALL cin m k1 k2.


1367 
k1 < m & k2 < n & m + k2 <= n >


1368 
ACARRY k1 (WSEG m k2 w1) (WSEG m k2 w2)


1369 
(ACARRY k2 w1 w2 cin) =


1370 
ACARRY (k1 + k2) w1 w2 cin))"


1371 
by (import bword_arith ACARRY_ACARRY_WSEG)


1372 


1373 
;end_setup


1374 


1375 
;setup_theory bword_bitop


1376 


1377 
consts


1378 
WNOT :: "bool word => bool word"


1379 


1380 
specification (WNOT) WNOT_DEF: "ALL l. WNOT (WORD l) = WORD (map Not l)"


1381 
by (import bword_bitop WNOT_DEF)


1382 


1383 
lemma PBITOP_WNOT: "IN WNOT PBITOP"


1384 
by (import bword_bitop PBITOP_WNOT)


1385 


1386 
lemma WNOT_WNOT: "ALL w. WNOT (WNOT w) = w"


1387 
by (import bword_bitop WNOT_WNOT)


1388 


1389 
lemma WCAT_WNOT: "ALL n1 n2.


1390 
RES_FORALL (PWORDLEN n1)


1391 
(%w1. RES_FORALL (PWORDLEN n2)


1392 
(%w2. WCAT (WNOT w1, WNOT w2) = WNOT (WCAT (w1, w2))))"


1393 
by (import bword_bitop WCAT_WNOT)


1394 


1395 
consts


1396 
WAND :: "bool word => bool word => bool word"


1397 


1398 
specification (WAND) WAND_DEF: "ALL l1 l2. WAND (WORD l1) (WORD l2) = WORD (map2 op & l1 l2)"


1399 
by (import bword_bitop WAND_DEF)


1400 


1401 
lemma PBITBOP_WAND: "IN WAND PBITBOP"


1402 
by (import bword_bitop PBITBOP_WAND)


1403 


1404 
consts


1405 
WOR :: "bool word => bool word => bool word"


1406 


1407 
specification (WOR) WOR_DEF: "ALL l1 l2. WOR (WORD l1) (WORD l2) = WORD (map2 op  l1 l2)"


1408 
by (import bword_bitop WOR_DEF)


1409 


1410 
lemma PBITBOP_WOR: "IN WOR PBITBOP"


1411 
by (import bword_bitop PBITBOP_WOR)


1412 


1413 
consts


1414 
WXOR :: "bool word => bool word => bool word"


1415 


1416 
specification (WXOR) WXOR_DEF: "ALL l1 l2. WXOR (WORD l1) (WORD l2) = WORD (map2 (%x y. x ~= y) l1 l2)"


1417 
by (import bword_bitop WXOR_DEF)


1418 


1419 
lemma PBITBOP_WXOR: "IN WXOR PBITBOP"


1420 
by (import bword_bitop PBITBOP_WXOR)


1421 


1422 
;end_setup


1423 


1424 
end


1425 
