Theory Word_8

(*
 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)

section "Words of Length 8"

theory Word_8
imports
  More_Word
  Enumeration_Word
  Even_More_List
  Signed_Words
  Word_Lemmas
begin

context
  includes bit_operations_syntax
begin

lemma len8: "len_of (x :: 8 itself) = 8" by simp

lemma word8_and_max_simp:
  x AND 0xFF = x for x :: 8 word
  using word_and_full_mask_simp [of x]
  by (simp add: numeral_eq_Suc mask_Suc_exp)

lemma enum_word8_eq:
  enum = [0 :: 8 word, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19,
                            20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36,
                            37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53,
                            54, 55, 56, 57, 58, 59, 60, 61, 62, 63, 64, 65, 66, 67, 68, 69, 70,
                            71, 72, 73, 74, 75, 76, 77, 78, 79, 80, 81, 82, 83, 84, 85, 86, 87,
                            88, 89, 90, 91, 92, 93, 94, 95, 96, 97, 98, 99, 100, 101, 102, 103,
                            104, 105, 106, 107, 108, 109, 110, 111, 112, 113, 114, 115, 116, 117,
                            118, 119, 120, 121, 122, 123, 124, 125, 126, 127, 128, 129, 130, 131,
                            132, 133, 134, 135, 136, 137, 138, 139, 140, 141, 142, 143, 144, 145,
                            146, 147, 148, 149, 150, 151, 152, 153, 154, 155, 156, 157, 158, 159,
                            160, 161, 162, 163, 164, 165, 166, 167, 168, 169, 170, 171, 172, 173,
                            174, 175, 176, 177, 178, 179, 180, 181, 182, 183, 184, 185, 186, 187,
                            188, 189, 190, 191, 192, 193, 194, 195, 196, 197, 198, 199, 200, 201,
                            202, 203, 204, 205, 206, 207, 208, 209, 210, 211, 212, 213, 214, 215,
                            216, 217, 218, 219, 220, 221, 222, 223, 224, 225, 226, 227, 228, 229,
                            230, 231, 232, 233, 234, 235, 236, 237, 238, 239, 240, 241, 242, 243,
                            244, 245, 246, 247, 248, 249, 250, 251, 252, 253, 254, 255] (is ?lhs = ?rhs)
proof -
  have map unat ?lhs = [0..<256]
    by (simp add: enum_word_def comp_def take_bit_nat_eq_self map_idem_upt_eq unsigned_of_nat)
  also have  = map unat ?rhs
    by (simp add: upt_zero_numeral_unfold)
  finally show ?thesis
    using unat_inj by (rule map_injective)
qed

lemma set_enum_word8_def:
  "(set enum :: 8 word set) = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19,
                            20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36,
                            37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53,
                            54, 55, 56, 57, 58, 59, 60, 61, 62, 63, 64, 65, 66, 67, 68, 69, 70,
                            71, 72, 73, 74, 75, 76, 77, 78, 79, 80, 81, 82, 83, 84, 85, 86, 87,
                            88, 89, 90, 91, 92, 93, 94, 95, 96, 97, 98, 99, 100, 101, 102, 103,
                            104, 105, 106, 107, 108, 109, 110, 111, 112, 113, 114, 115, 116, 117,
                            118, 119, 120, 121, 122, 123, 124, 125, 126, 127, 128, 129, 130, 131,
                            132, 133, 134, 135, 136, 137, 138, 139, 140, 141, 142, 143, 144, 145,
                            146, 147, 148, 149, 150, 151, 152, 153, 154, 155, 156, 157, 158, 159,
                            160, 161, 162, 163, 164, 165, 166, 167, 168, 169, 170, 171, 172, 173,
                            174, 175, 176, 177, 178, 179, 180, 181, 182, 183, 184, 185, 186, 187,
                            188, 189, 190, 191, 192, 193, 194, 195, 196, 197, 198, 199, 200, 201,
                            202, 203, 204, 205, 206, 207, 208, 209, 210, 211, 212, 213, 214, 215,
                            216, 217, 218, 219, 220, 221, 222, 223, 224, 225, 226, 227, 228, 229,
                            230, 231, 232, 233, 234, 235, 236, 237, 238, 239, 240, 241, 242, 243,
                            244, 245, 246, 247, 248, 249, 250, 251, 252, 253, 254, 255}"
  by (simp add: enum_word8_eq)

lemma set_strip_insert: " x  insert a S; x  a   x  S"
  by simp

lemma word8_exhaust:
  fixes x :: 8 word
  shows "x  0; x  1; x  2; x  3; x  4; x  5; x  6; x  7; x  8; x  9; x  10; x  11; x 
          12; x  13; x  14; x  15; x  16; x  17; x  18; x  19; x  20; x  21; x  22; x 
          23; x  24; x  25; x  26; x  27; x  28; x  29; x  30; x  31; x  32; x  33; x 
          34; x  35; x  36; x  37; x  38; x  39; x  40; x  41; x  42; x  43; x  44; x 
          45; x  46; x  47; x  48; x  49; x  50; x  51; x  52; x  53; x  54; x  55; x 
          56; x  57; x  58; x  59; x  60; x  61; x  62; x  63; x  64; x  65; x  66; x 
          67; x  68; x  69; x  70; x  71; x  72; x  73; x  74; x  75; x  76; x  77; x 
          78; x  79; x  80; x  81; x  82; x  83; x  84; x  85; x  86; x  87; x  88; x 
          89; x  90; x  91; x  92; x  93; x  94; x  95; x  96; x  97; x  98; x  99; x 
          100; x  101; x  102; x  103; x  104; x  105; x  106; x  107; x  108; x  109; x 
          110; x  111; x  112; x  113; x  114; x  115; x  116; x  117; x  118; x  119; x 
          120; x  121; x  122; x  123; x  124; x  125; x  126; x  127; x  128; x  129; x 
          130; x  131; x  132; x  133; x  134; x  135; x  136; x  137; x  138; x  139; x 
          140; x  141; x  142; x  143; x  144; x  145; x  146; x  147; x  148; x  149; x 
          150; x  151; x  152; x  153; x  154; x  155; x  156; x  157; x  158; x  159; x 
          160; x  161; x  162; x  163; x  164; x  165; x  166; x  167; x  168; x  169; x 
          170; x  171; x  172; x  173; x  174; x  175; x  176; x  177; x  178; x  179; x 
          180; x  181; x  182; x  183; x  184; x  185; x  186; x  187; x  188; x  189; x 
          190; x  191; x  192; x  193; x  194; x  195; x  196; x  197; x  198; x  199; x 
          200; x  201; x  202; x  203; x  204; x  205; x  206; x  207; x  208; x  209; x 
          210; x  211; x  212; x  213; x  214; x  215; x  216; x  217; x  218; x  219; x 
          220; x  221; x  222; x  223; x  224; x  225; x  226; x  227; x  228; x  229; x 
          230; x  231; x  232; x  233; x  234; x  235; x  236; x  237; x  238; x  239; x 
          240; x  241; x  242; x  243; x  244; x  245; x  246; x  247; x  248; x  249; x 
          250; x  251; x  252; x  253; x  254; x  255  P"
  apply (subgoal_tac "x  set enum", subst (asm) set_enum_word8_def)
    apply (drule set_strip_insert, assumption)+
   apply (erule emptyE)
  apply (subst enum_UNIV, rule UNIV_I)
  done

end

end