373 | Suc: "bin_sc (Suc n) b w = bin_sc n b (bin_rest w) BIT bin_last w" |
373 | Suc: "bin_sc (Suc n) b w = bin_sc n b (bin_rest w) BIT bin_last w" |
374 |
374 |
375 (** nth bit, set/clear **) |
375 (** nth bit, set/clear **) |
376 |
376 |
377 lemma bin_nth_sc [simp]: |
377 lemma bin_nth_sc [simp]: |
378 "!!w. bin_nth (bin_sc n b w) n = (b = 1)" |
378 "bin_nth (bin_sc n b w) n = (b = 1)" |
379 by (induct n) auto |
379 by (induct n arbitrary: w) auto |
380 |
380 |
381 lemma bin_sc_sc_same [simp]: |
381 lemma bin_sc_sc_same [simp]: |
382 "!!w. bin_sc n c (bin_sc n b w) = bin_sc n c w" |
382 "bin_sc n c (bin_sc n b w) = bin_sc n c w" |
383 by (induct n) auto |
383 by (induct n arbitrary: w) auto |
384 |
384 |
385 lemma bin_sc_sc_diff: |
385 lemma bin_sc_sc_diff: |
386 "!!w m. m ~= n ==> |
386 "m ~= n ==> |
387 bin_sc m c (bin_sc n b w) = bin_sc n b (bin_sc m c w)" |
387 bin_sc m c (bin_sc n b w) = bin_sc n b (bin_sc m c w)" |
388 apply (induct n) |
388 apply (induct n arbitrary: w m) |
389 apply (case_tac [!] m) |
389 apply (case_tac [!] m) |
390 apply auto |
390 apply auto |
391 done |
391 done |
392 |
392 |
393 lemma bin_nth_sc_gen: |
393 lemma bin_nth_sc_gen: |
394 "!!w m. bin_nth (bin_sc n b w) m = (if m = n then b = 1 else bin_nth w m)" |
394 "bin_nth (bin_sc n b w) m = (if m = n then b = 1 else bin_nth w m)" |
395 by (induct n) (case_tac [!] m, auto) |
395 by (induct n arbitrary: w m) (case_tac [!] m, auto) |
396 |
396 |
397 lemma bin_sc_nth [simp]: |
397 lemma bin_sc_nth [simp]: |
398 "!!w. (bin_sc n (If (bin_nth w n) 1 0) w) = w" |
398 "(bin_sc n (If (bin_nth w n) 1 0) w) = w" |
399 by (induct n) auto |
399 by (induct n arbitrary: w) auto |
400 |
400 |
401 lemma bin_sign_sc [simp]: |
401 lemma bin_sign_sc [simp]: |
402 "!!w. bin_sign (bin_sc n b w) = bin_sign w" |
402 "bin_sign (bin_sc n b w) = bin_sign w" |
403 by (induct n) auto |
403 by (induct n arbitrary: w) auto |
404 |
404 |
405 lemma bin_sc_bintr [simp]: |
405 lemma bin_sc_bintr [simp]: |
406 "!!w m. bintrunc m (bin_sc n x (bintrunc m (w))) = bintrunc m (bin_sc n x w)" |
406 "bintrunc m (bin_sc n x (bintrunc m (w))) = bintrunc m (bin_sc n x w)" |
407 apply (induct n) |
407 apply (induct n arbitrary: w m) |
408 apply (case_tac [!] w rule: bin_exhaust) |
408 apply (case_tac [!] w rule: bin_exhaust) |
409 apply (case_tac [!] m, auto) |
409 apply (case_tac [!] m, auto) |
410 done |
410 done |
411 |
411 |
412 lemma bin_clr_le: |
412 lemma bin_clr_le: |
413 "!!w. bin_sc n 0 w <= w" |
413 "bin_sc n 0 w <= w" |
414 apply (induct n) |
414 apply (induct n arbitrary: w) |
415 apply (case_tac [!] w rule: bin_exhaust) |
415 apply (case_tac [!] w rule: bin_exhaust) |
416 apply (auto simp del: BIT_simps) |
416 apply (auto simp del: BIT_simps) |
417 apply (unfold Bit_def) |
417 apply (unfold Bit_def) |
418 apply (simp_all add: bitval_def split: bit.split) |
418 apply (simp_all add: bitval_def split: bit.split) |
419 done |
419 done |
420 |
420 |
421 lemma bin_set_ge: |
421 lemma bin_set_ge: |
422 "!!w. bin_sc n 1 w >= w" |
422 "bin_sc n 1 w >= w" |
423 apply (induct n) |
423 apply (induct n arbitrary: w) |
424 apply (case_tac [!] w rule: bin_exhaust) |
424 apply (case_tac [!] w rule: bin_exhaust) |
425 apply (auto simp del: BIT_simps) |
425 apply (auto simp del: BIT_simps) |
426 apply (unfold Bit_def) |
426 apply (unfold Bit_def) |
427 apply (simp_all add: bitval_def split: bit.split) |
427 apply (simp_all add: bitval_def split: bit.split) |
428 done |
428 done |
429 |
429 |
430 lemma bintr_bin_clr_le: |
430 lemma bintr_bin_clr_le: |
431 "!!w m. bintrunc n (bin_sc m 0 w) <= bintrunc n w" |
431 "bintrunc n (bin_sc m 0 w) <= bintrunc n w" |
432 apply (induct n) |
432 apply (induct n arbitrary: w m) |
433 apply simp |
433 apply simp |
434 apply (case_tac w rule: bin_exhaust) |
434 apply (case_tac w rule: bin_exhaust) |
435 apply (case_tac m) |
435 apply (case_tac m) |
436 apply (auto simp del: BIT_simps) |
436 apply (auto simp del: BIT_simps) |
437 apply (unfold Bit_def) |
437 apply (unfold Bit_def) |
438 apply (simp_all add: bitval_def split: bit.split) |
438 apply (simp_all add: bitval_def split: bit.split) |
439 done |
439 done |
440 |
440 |
441 lemma bintr_bin_set_ge: |
441 lemma bintr_bin_set_ge: |
442 "!!w m. bintrunc n (bin_sc m 1 w) >= bintrunc n w" |
442 "bintrunc n (bin_sc m 1 w) >= bintrunc n w" |
443 apply (induct n) |
443 apply (induct n arbitrary: w m) |
444 apply simp |
444 apply simp |
445 apply (case_tac w rule: bin_exhaust) |
445 apply (case_tac w rule: bin_exhaust) |
446 apply (case_tac m) |
446 apply (case_tac m) |
447 apply (auto simp del: BIT_simps) |
447 apply (auto simp del: BIT_simps) |
448 apply (unfold Bit_def) |
448 apply (unfold Bit_def) |
497 |
497 |
498 declare bin_rsplit_aux.simps [simp del] |
498 declare bin_rsplit_aux.simps [simp del] |
499 declare bin_rsplitl_aux.simps [simp del] |
499 declare bin_rsplitl_aux.simps [simp del] |
500 |
500 |
501 lemma bin_sign_cat: |
501 lemma bin_sign_cat: |
502 "!!y. bin_sign (bin_cat x n y) = bin_sign x" |
502 "bin_sign (bin_cat x n y) = bin_sign x" |
503 by (induct n) auto |
503 by (induct n arbitrary: y) auto |
504 |
504 |
505 lemma bin_cat_Suc_Bit: |
505 lemma bin_cat_Suc_Bit: |
506 "bin_cat w (Suc n) (v BIT b) = bin_cat w n v BIT b" |
506 "bin_cat w (Suc n) (v BIT b) = bin_cat w n v BIT b" |
507 by auto |
507 by auto |
508 |
508 |
509 lemma bin_nth_cat: |
509 lemma bin_nth_cat: |
510 "!!n y. bin_nth (bin_cat x k y) n = |
510 "bin_nth (bin_cat x k y) n = |
511 (if n < k then bin_nth y n else bin_nth x (n - k))" |
511 (if n < k then bin_nth y n else bin_nth x (n - k))" |
512 apply (induct k) |
512 apply (induct k arbitrary: n y) |
513 apply clarsimp |
513 apply clarsimp |
514 apply (case_tac n, auto) |
514 apply (case_tac n, auto) |
515 done |
515 done |
516 |
516 |
517 lemma bin_nth_split: |
517 lemma bin_nth_split: |
518 "!!b c. bin_split n c = (a, b) ==> |
518 "bin_split n c = (a, b) ==> |
519 (ALL k. bin_nth a k = bin_nth c (n + k)) & |
519 (ALL k. bin_nth a k = bin_nth c (n + k)) & |
520 (ALL k. bin_nth b k = (k < n & bin_nth c k))" |
520 (ALL k. bin_nth b k = (k < n & bin_nth c k))" |
521 apply (induct n) |
521 apply (induct n arbitrary: b c) |
522 apply clarsimp |
522 apply clarsimp |
523 apply (clarsimp simp: Let_def split: ls_splits) |
523 apply (clarsimp simp: Let_def split: ls_splits) |
524 apply (case_tac k) |
524 apply (case_tac k) |
525 apply auto |
525 apply auto |
526 done |
526 done |
527 |
527 |
528 lemma bin_cat_assoc: |
528 lemma bin_cat_assoc: |
529 "!!z. bin_cat (bin_cat x m y) n z = bin_cat x (m + n) (bin_cat y n z)" |
529 "bin_cat (bin_cat x m y) n z = bin_cat x (m + n) (bin_cat y n z)" |
530 by (induct n) auto |
530 by (induct n arbitrary: z) auto |
531 |
531 |
532 lemma bin_cat_assoc_sym: "!!z m. |
532 lemma bin_cat_assoc_sym: |
533 bin_cat x m (bin_cat y n z) = bin_cat (bin_cat x (m - n) y) (min m n) z" |
533 "bin_cat x m (bin_cat y n z) = bin_cat (bin_cat x (m - n) y) (min m n) z" |
534 apply (induct n, clarsimp) |
534 apply (induct n arbitrary: z m, clarsimp) |
535 apply (case_tac m, auto) |
535 apply (case_tac m, auto) |
536 done |
536 done |
537 |
537 |
538 lemma bin_cat_Pls [simp]: |
538 lemma bin_cat_Pls [simp]: "bin_cat Int.Pls n w = bintrunc n w" |
539 "!!w. bin_cat Int.Pls n w = bintrunc n w" |
539 by (induct n arbitrary: w) auto |
540 by (induct n) auto |
|
541 |
540 |
542 lemma bintr_cat1: |
541 lemma bintr_cat1: |
543 "!!b. bintrunc (k + n) (bin_cat a n b) = bin_cat (bintrunc k a) n b" |
542 "bintrunc (k + n) (bin_cat a n b) = bin_cat (bintrunc k a) n b" |
544 by (induct n) auto |
543 by (induct n arbitrary: b) auto |
545 |
544 |
546 lemma bintr_cat: "bintrunc m (bin_cat a n b) = |
545 lemma bintr_cat: "bintrunc m (bin_cat a n b) = |
547 bin_cat (bintrunc (m - n) a) n (bintrunc (min m n) b)" |
546 bin_cat (bintrunc (m - n) a) n (bintrunc (min m n) b)" |
548 by (rule bin_eqI) (auto simp: bin_nth_cat nth_bintr) |
547 by (rule bin_eqI) (auto simp: bin_nth_cat nth_bintr) |
549 |
548 |
550 lemma bintr_cat_same [simp]: |
549 lemma bintr_cat_same [simp]: |
551 "bintrunc n (bin_cat a n b) = bintrunc n b" |
550 "bintrunc n (bin_cat a n b) = bintrunc n b" |
552 by (auto simp add : bintr_cat) |
551 by (auto simp add : bintr_cat) |
553 |
552 |
554 lemma cat_bintr [simp]: |
553 lemma cat_bintr [simp]: |
555 "!!b. bin_cat a n (bintrunc n b) = bin_cat a n b" |
554 "bin_cat a n (bintrunc n b) = bin_cat a n b" |
556 by (induct n) auto |
555 by (induct n arbitrary: b) auto |
557 |
556 |
558 lemma split_bintrunc: |
557 lemma split_bintrunc: |
559 "!!b c. bin_split n c = (a, b) ==> b = bintrunc n c" |
558 "bin_split n c = (a, b) ==> b = bintrunc n c" |
560 by (induct n) (auto simp: Let_def split: ls_splits) |
559 by (induct n arbitrary: b c) (auto simp: Let_def split: ls_splits) |
561 |
560 |
562 lemma bin_cat_split: |
561 lemma bin_cat_split: |
563 "!!v w. bin_split n w = (u, v) ==> w = bin_cat u n v" |
562 "bin_split n w = (u, v) ==> w = bin_cat u n v" |
564 by (induct n) (auto simp: Let_def split: ls_splits) |
563 by (induct n arbitrary: v w) (auto simp: Let_def split: ls_splits) |
565 |
564 |
566 lemma bin_split_cat: |
565 lemma bin_split_cat: |
567 "!!w. bin_split n (bin_cat v n w) = (v, bintrunc n w)" |
566 "bin_split n (bin_cat v n w) = (v, bintrunc n w)" |
568 by (induct n) auto |
567 by (induct n arbitrary: w) auto |
569 |
568 |
570 lemma bin_split_Pls [simp]: |
569 lemma bin_split_Pls [simp]: |
571 "bin_split n Int.Pls = (Int.Pls, Int.Pls)" |
570 "bin_split n Int.Pls = (Int.Pls, Int.Pls)" |
572 by (induct n) (auto simp: Let_def BIT_simps split: ls_splits) |
571 by (induct n) (auto simp: Let_def BIT_simps split: ls_splits) |
573 |
572 |
574 lemma bin_split_Min [simp]: |
573 lemma bin_split_Min [simp]: |
575 "bin_split n Int.Min = (Int.Min, bintrunc n Int.Min)" |
574 "bin_split n Int.Min = (Int.Min, bintrunc n Int.Min)" |
576 by (induct n) (auto simp: Let_def split: ls_splits) |
575 by (induct n) (auto simp: Let_def split: ls_splits) |
577 |
576 |
578 lemma bin_split_trunc: |
577 lemma bin_split_trunc: |
579 "!!m b c. bin_split (min m n) c = (a, b) ==> |
578 "bin_split (min m n) c = (a, b) ==> |
580 bin_split n (bintrunc m c) = (bintrunc (m - n) a, b)" |
579 bin_split n (bintrunc m c) = (bintrunc (m - n) a, b)" |
581 apply (induct n, clarsimp) |
580 apply (induct n arbitrary: m b c, clarsimp) |
582 apply (simp add: bin_rest_trunc Let_def split: ls_splits) |
581 apply (simp add: bin_rest_trunc Let_def split: ls_splits) |
583 apply (case_tac m) |
582 apply (case_tac m) |
584 apply (auto simp: Let_def BIT_simps split: ls_splits) |
583 apply (auto simp: Let_def BIT_simps split: ls_splits) |
585 done |
584 done |
586 |
585 |
587 lemma bin_split_trunc1: |
586 lemma bin_split_trunc1: |
588 "!!m b c. bin_split n c = (a, b) ==> |
587 "bin_split n c = (a, b) ==> |
589 bin_split n (bintrunc m c) = (bintrunc (m - n) a, bintrunc m b)" |
588 bin_split n (bintrunc m c) = (bintrunc (m - n) a, bintrunc m b)" |
590 apply (induct n, clarsimp) |
589 apply (induct n arbitrary: m b c, clarsimp) |
591 apply (simp add: bin_rest_trunc Let_def split: ls_splits) |
590 apply (simp add: bin_rest_trunc Let_def split: ls_splits) |
592 apply (case_tac m) |
591 apply (case_tac m) |
593 apply (auto simp: Let_def BIT_simps split: ls_splits) |
592 apply (auto simp: Let_def BIT_simps split: ls_splits) |
594 done |
593 done |
595 |
594 |
596 lemma bin_cat_num: |
595 lemma bin_cat_num: |
597 "!!b. bin_cat a n b = a * 2 ^ n + bintrunc n b" |
596 "bin_cat a n b = a * 2 ^ n + bintrunc n b" |
598 apply (induct n, clarsimp) |
597 apply (induct n arbitrary: b, clarsimp) |
599 apply (simp add: Bit_def cong: number_of_False_cong) |
598 apply (simp add: Bit_def cong: number_of_False_cong) |
600 done |
599 done |
601 |
600 |
602 lemma bin_split_num: |
601 lemma bin_split_num: |
603 "!!b. bin_split n b = (b div 2 ^ n, b mod 2 ^ n)" |
602 "bin_split n b = (b div 2 ^ n, b mod 2 ^ n)" |
604 apply (induct n, simp add: Pls_def) |
603 apply (induct n arbitrary: b, simp add: Pls_def) |
605 apply (simp add: bin_rest_def zdiv_zmult2_eq) |
604 apply (simp add: bin_rest_def zdiv_zmult2_eq) |
606 apply (case_tac b rule: bin_exhaust) |
605 apply (case_tac b rule: bin_exhaust) |
607 apply simp |
606 apply simp |
608 apply (simp add: Bit_def mod_mult_mult1 p1mod22k bitval_def |
607 apply (simp add: Bit_def mod_mult_mult1 p1mod22k bitval_def |
609 split: bit.split |
608 split: bit.split) |
610 cong: number_of_False_cong) |
609 done |
611 done |
|
612 |
610 |
613 subsection {* Miscellaneous lemmas *} |
611 subsection {* Miscellaneous lemmas *} |
614 |
612 |
615 lemma nth_2p_bin: |
613 lemma nth_2p_bin: |
616 "!!m. bin_nth (2 ^ n) m = (m = n)" |
614 "bin_nth (2 ^ n) m = (m = n)" |
617 apply (induct n) |
615 apply (induct n arbitrary: m) |
618 apply clarsimp |
616 apply clarsimp |
619 apply safe |
617 apply safe |
620 apply (case_tac m) |
618 apply (case_tac m) |
621 apply (auto simp: trans [OF numeral_1_eq_1 [symmetric] number_of_eq]) |
619 apply (auto simp: trans [OF numeral_1_eq_1 [symmetric] number_of_eq]) |
622 apply (case_tac m) |
620 apply (case_tac m) |