src/HOL/Import/HOL/HOL4Vec.thy
author haftmann
Mon Jan 30 08:20:56 2006 +0100 (2006-01-30)
changeset 18851 9502ce541f01
parent 17652 b1ef33ebfa17
child 20485 3078fd2eec7b
permissions -rw-r--r--
adaptions to codegen_package
     1 (* AUTOMATICALLY GENERATED, DO NOT EDIT! *)
     2 
     3 theory HOL4Vec imports HOL4Base begin
     4 
     5 ;setup_theory res_quan
     6 
     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)"
    10   by (import res_quan RES_FORALL_CONJ_DIST)
    11 
    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)"
    15   by (import res_quan RES_FORALL_DISJ_DIST)
    16 
    17 lemma RES_FORALL_UNIQUE: "ALL (x::'a::type => bool) xa::'a::type. RES_FORALL (op = xa) x = x xa"
    18   by (import res_quan RES_FORALL_UNIQUE)
    19 
    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))"
    23   by (import res_quan RES_FORALL_FORALL)
    24 
    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))"
    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 
    34 lemma RES_FORALL_UNIV: "ALL p::'a::type => bool. RES_FORALL pred_set.UNIV p = All p"
    35   by (import res_quan RES_FORALL_UNIV)
    36 
    37 lemma RES_FORALL_NULL: "ALL (p::'a::type => bool) m::bool.
    38    RES_FORALL p (%x::'a::type. m) = (p = EMPTY | m)"
    39   by (import res_quan RES_FORALL_NULL)
    40 
    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)"
    44   by (import res_quan RES_EXISTS_DISJ_DIST)
    45 
    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)"
    49   by (import res_quan RES_DISJ_EXISTS_DIST)
    50 
    51 lemma RES_EXISTS_EQUAL: "ALL (x::'a::type => bool) xa::'a::type. RES_EXISTS (op = xa) x = x xa"
    52   by (import res_quan RES_EXISTS_EQUAL)
    53 
    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))"
    58   by (import res_quan RES_EXISTS_REORDER)
    59 
    60 lemma RES_EXISTS_EMPTY: "ALL p::'a::type => bool. ~ RES_EXISTS EMPTY p"
    61   by (import res_quan RES_EXISTS_EMPTY)
    62 
    63 lemma RES_EXISTS_UNIV: "ALL p::'a::type => bool. RES_EXISTS pred_set.UNIV p = Ex p"
    64   by (import res_quan RES_EXISTS_UNIV)
    65 
    66 lemma RES_EXISTS_NULL: "ALL (p::'a::type => bool) m::bool.
    67    RES_EXISTS p (%x::'a::type. m) = (p ~= EMPTY & m)"
    68   by (import res_quan RES_EXISTS_NULL)
    69 
    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))"
    72   by (import res_quan RES_EXISTS_ALT)
    73 
    74 lemma RES_EXISTS_UNIQUE_EMPTY: "ALL p::'a::type => bool. ~ RES_EXISTS_UNIQUE EMPTY p"
    75   by (import res_quan RES_EXISTS_UNIQUE_EMPTY)
    76 
    77 lemma RES_EXISTS_UNIQUE_UNIV: "ALL p::'a::type => bool. RES_EXISTS_UNIQUE pred_set.UNIV p = Ex1 p"
    78   by (import res_quan RES_EXISTS_UNIQUE_UNIV)
    79 
    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)"
    83   by (import res_quan RES_EXISTS_UNIQUE_NULL)
    84 
    85 lemma RES_EXISTS_UNIQUE_ALT: "ALL (p::'a::type => bool) m::'a::type => bool.
    86    RES_EXISTS_UNIQUE p m =
    87    RES_EXISTS p
    88     (%x::'a::type. m x & RES_FORALL p (%y::'a::type. m y --> y = x))"
    89   by (import res_quan RES_EXISTS_UNIQUE_ALT)
    90 
    91 lemma RES_SELECT_EMPTY: "ALL p::'a::type => bool. RES_SELECT EMPTY p = (SOME x::'a::type. False)"
    92   by (import res_quan RES_SELECT_EMPTY)
    93 
    94 lemma RES_SELECT_UNIV: "ALL p::'a::type => bool. RES_SELECT pred_set.UNIV p = Eps p"
    95   by (import res_quan RES_SELECT_UNIV)
    96 
    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"
    99   by (import res_quan RES_ABSTRACT)
   100 
   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"
   105   by (import res_quan RES_ABSTRACT_EQUAL)
   106 
   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"
   109   by (import res_quan RES_ABSTRACT_IDEMPOT)
   110 
   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)"
   115   by (import res_quan RES_ABSTRACT_EQUAL_EQ)
   116 
   117 ;end_setup
   118 
   119 ;setup_theory word_base
   120 
   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.
   125           (op -->::bool => bool => bool)
   126            ((All::('a::type list recspace => bool) => bool)
   127              (%a0::'a::type list recspace.
   128                  (op -->::bool => bool => bool)
   129                   ((Ex::('a::type list => bool) => bool)
   130                     (%a::'a::type list.
   131                         (op =::'a::type list recspace
   132                                => 'a::type list recspace => bool)
   133                          a0 ((CONSTR::nat
   134 => 'a::type list
   135    => (nat => 'a::type list recspace) => 'a::type list recspace)
   136                               (0::nat) a
   137                               (%n::nat. BOTTOM::'a::type list recspace))))
   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
   145   mk_word :: "'a list recspace => 'a word" 
   146   dest_word :: "'a word => 'a list recspace" 
   147 
   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.
   152             (EX a::'a::type list. a0 = CONSTR 0 a (%n::nat. BOTTOM)) -->
   153             word a0) -->
   154         word r) =
   155     (dest_word (mk_word r) = r))"
   156   by (import word_base word_repfns)
   157 
   158 consts
   159   word_base0 :: "'a list => 'a word" 
   160 
   161 defs
   162   word_base0_primdef: "word_base0 == %a::'a::type list. mk_word (CONSTR 0 a (%n::nat. BOTTOM))"
   163 
   164 lemma word_base0_def: "word_base0 = (%a::'a::type list. mk_word (CONSTR 0 a (%n::nat. BOTTOM)))"
   165   by (import word_base word_base0_def)
   166 
   167 constdefs
   168   WORD :: "'a list => 'a word" 
   169   "WORD == word_base0"
   170 
   171 lemma WORD: "WORD = word_base0"
   172   by (import word_base WORD)
   173 
   174 consts
   175   word_case :: "('a list => 'b) => 'a word => 'b" 
   176 
   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"
   179   by (import word_base word_case_def)
   180 
   181 consts
   182   word_size :: "('a => nat) => 'a word => nat" 
   183 
   184 specification (word_size_primdef: word_size) word_size_def: "ALL (f::'a::type => nat) a::'a::type list.
   185    word_size f (WORD a) = 1 + list_size f a"
   186   by (import word_base word_size_def)
   187 
   188 lemma word_11: "ALL (a::'a::type list) a'::'a::type list. (WORD a = WORD a') = (a = a')"
   189   by (import word_base word_11)
   190 
   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) -->
   195    word_case f M = word_case f' M'"
   196   by (import word_base word_case_cong)
   197 
   198 lemma word_nchotomy: "ALL x::'a::type word. EX l::'a::type list. x = WORD l"
   199   by (import word_base word_nchotomy)
   200 
   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"
   203   by (import word_base word_Axiom)
   204 
   205 lemma word_induction: "ALL P::'a::type word => bool. (ALL a::'a::type list. P (WORD a)) --> All P"
   206   by (import word_base word_induction)
   207 
   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"
   210   by (import word_base word_Ax)
   211 
   212 lemma WORD_11: "ALL (x::'a::type list) xa::'a::type list. (WORD x = WORD xa) = (x = xa)"
   213   by (import word_base WORD_11)
   214 
   215 lemma word_induct: "ALL x::'a::type word => bool. (ALL l::'a::type list. x (WORD l)) --> All x"
   216   by (import word_base word_induct)
   217 
   218 lemma word_cases: "ALL x::'a::type word. EX l::'a::type list. x = WORD l"
   219   by (import word_base word_cases)
   220 
   221 consts
   222   WORDLEN :: "'a word => nat" 
   223 
   224 specification (WORDLEN) WORDLEN_DEF: "ALL l::'a::type list. WORDLEN (WORD l) = length l"
   225   by (import word_base WORDLEN_DEF)
   226 
   227 consts
   228   PWORDLEN :: "nat => 'a word => bool" 
   229 
   230 defs
   231   PWORDLEN_primdef: "PWORDLEN == %n::nat. GSPEC (%w::'a::type word. (w, WORDLEN w = n))"
   232 
   233 lemma PWORDLEN_def: "ALL n::nat. PWORDLEN n = GSPEC (%w::'a::type word. (w, WORDLEN w = n))"
   234   by (import word_base PWORDLEN_def)
   235 
   236 lemma IN_PWORDLEN: "ALL (n::nat) l::'a::type list. IN (WORD l) (PWORDLEN n) = (length l = n)"
   237   by (import word_base IN_PWORDLEN)
   238 
   239 lemma PWORDLEN: "ALL (n::nat) w::'a::type word. IN w (PWORDLEN n) = (WORDLEN w = n)"
   240   by (import word_base PWORDLEN)
   241 
   242 lemma PWORDLEN0: "ALL w::'a::type word. IN w (PWORDLEN 0) --> w = WORD []"
   243   by (import word_base PWORDLEN0)
   244 
   245 lemma PWORDLEN1: "ALL x::'a::type. IN (WORD [x]) (PWORDLEN 1)"
   246   by (import word_base PWORDLEN1)
   247 
   248 consts
   249   WSEG :: "nat => nat => 'a word => 'a word" 
   250 
   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))"
   253   by (import word_base WSEG_DEF)
   254 
   255 lemma WSEG0: "ALL (k::nat) w::'a::type word. WSEG 0 k w = WORD []"
   256   by (import word_base WSEG0)
   257 
   258 lemma WSEG_PWORDLEN: "ALL n::nat.
   259    RES_FORALL (PWORDLEN n)
   260     (%w::'a::type word.
   261         ALL (m::nat) k::nat. m + k <= n --> IN (WSEG m k w) (PWORDLEN m))"
   262   by (import word_base WSEG_PWORDLEN)
   263 
   264 lemma WSEG_WORDLEN: "ALL x::nat.
   265    RES_FORALL (PWORDLEN x)
   266     (%xa::'a::type word.
   267         ALL (xb::nat) xc::nat.
   268            xb + xc <= x --> WORDLEN (WSEG xb xc xa) = xb)"
   269   by (import word_base WSEG_WORDLEN)
   270 
   271 lemma WSEG_WORD_LENGTH: "ALL n::nat. RES_FORALL (PWORDLEN n) (%w::'a::type word. WSEG n 0 w = w)"
   272   by (import word_base WSEG_WORD_LENGTH)
   273 
   274 consts
   275   bit :: "nat => 'a word => 'a" 
   276 
   277 specification (bit) BIT_DEF: "ALL (k::nat) l::'a::type list. bit k (WORD l) = ELL k l"
   278   by (import word_base BIT_DEF)
   279 
   280 lemma BIT0: "ALL x::'a::type. bit 0 (WORD [x]) = x"
   281   by (import word_base BIT0)
   282 
   283 lemma WSEG_BIT: "(All::(nat => bool) => bool)
   284  (%n::nat.
   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.
   289           (All::(nat => bool) => bool)
   290            (%k::nat.
   291                (op -->::bool => bool => bool)
   292                 ((op <::nat => nat => bool) k n)
   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)))))))"
   300   by (import word_base WSEG_BIT)
   301 
   302 lemma BIT_WSEG: "ALL n::nat.
   303    RES_FORALL (PWORDLEN n)
   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)"
   307   by (import word_base BIT_WSEG)
   308 
   309 consts
   310   MSB :: "'a word => 'a" 
   311 
   312 specification (MSB) MSB_DEF: "ALL l::'a::type list. MSB (WORD l) = hd l"
   313   by (import word_base MSB_DEF)
   314 
   315 lemma MSB: "ALL n::nat.
   316    RES_FORALL (PWORDLEN n)
   317     (%w::'a::type word. 0 < n --> MSB w = bit (PRE n) w)"
   318   by (import word_base MSB)
   319 
   320 consts
   321   LSB :: "'a word => 'a" 
   322 
   323 specification (LSB) LSB_DEF: "ALL l::'a::type list. LSB (WORD l) = last l"
   324   by (import word_base LSB_DEF)
   325 
   326 lemma LSB: "ALL n::nat.
   327    RES_FORALL (PWORDLEN n) (%w::'a::type word. 0 < n --> LSB w = bit 0 w)"
   328   by (import word_base LSB)
   329 
   330 consts
   331   WSPLIT :: "nat => 'a word => 'a word * 'a word" 
   332 
   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))"
   335   by (import word_base WSPLIT_DEF)
   336 
   337 consts
   338   WCAT :: "'a word * 'a word => 'a word" 
   339 
   340 specification (WCAT) WCAT_DEF: "ALL (l1::'a::type list) l2::'a::type list.
   341    WCAT (WORD l1, WORD l2) = WORD (l1 @ l2)"
   342   by (import word_base WCAT_DEF)
   343 
   344 lemma WORD_PARTITION: "(op &::bool => bool => bool)
   345  ((All::(nat => bool) => bool)
   346    (%n::nat.
   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.
   351             (All::(nat => bool) => bool)
   352              (%m::nat.
   353                  (op -->::bool => bool => bool)
   354                   ((op <=::nat => nat => bool) m n)
   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))
   361                     w)))))
   362  ((All::(nat => bool) => bool)
   363    (%n::nat.
   364        (All::(nat => bool) => bool)
   365         (%m::nat.
   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))))))"
   389   by (import word_base WORD_PARTITION)
   390 
   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)"
   393   by (import word_base WCAT_ASSOC)
   394 
   395 lemma WCAT0: "ALL w::'a::type word. WCAT (WORD [], w) = w & WCAT (w, WORD []) = w"
   396   by (import word_base WCAT0)
   397 
   398 lemma WCAT_11: "ALL (m::nat) n::nat.
   399    RES_FORALL (PWORDLEN m)
   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)))))"
   409   by (import word_base WCAT_11)
   410 
   411 lemma WSPLIT_PWORDLEN: "(All::(nat => bool) => bool)
   412  (%n::nat.
   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.
   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)
   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)
   429                       ((op -::nat => nat => nat) n m)))
   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))))))"
   437   by (import word_base WSPLIT_PWORDLEN)
   438 
   439 lemma WCAT_PWORDLEN: "ALL n1::nat.
   440    RES_FORALL (PWORDLEN n1)
   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))))"
   445   by (import word_base WCAT_PWORDLEN)
   446 
   447 lemma WORDLEN_SUC_WCAT: "ALL (n::nat) w::'a::type word.
   448    IN w (PWORDLEN (Suc n)) -->
   449    RES_EXISTS (PWORDLEN 1)
   450     (%b::'a::type word.
   451         RES_EXISTS (PWORDLEN n) (%w'::'a::type word. w = WCAT (b, w')))"
   452   by (import word_base WORDLEN_SUC_WCAT)
   453 
   454 lemma WSEG_WSEG: "ALL n::nat.
   455    RES_FORALL (PWORDLEN n)
   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)"
   460   by (import word_base WSEG_WSEG)
   461 
   462 lemma WSPLIT_WSEG: "(All::(nat => bool) => bool)
   463  (%n::nat.
   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.
   468           (All::(nat => bool) => bool)
   469            (%k::nat.
   470                (op -->::bool => bool => bool)
   471                 ((op <=::nat => nat => bool) k n)
   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)
   481                       ((op -::nat => nat => nat) n k) k w)
   482                     ((WSEG::nat => nat => 'a::type word => 'a::type word) k
   483                       (0::nat) w))))))"
   484   by (import word_base WSPLIT_WSEG)
   485 
   486 lemma WSPLIT_WSEG1: "(All::(nat => bool) => bool)
   487  (%n::nat.
   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.
   492           (All::(nat => bool) => bool)
   493            (%k::nat.
   494                (op -->::bool => bool => bool)
   495                 ((op <=::nat => nat => bool) k n)
   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)
   503                     ((op -::nat => nat => nat) n k) k w)))))"
   504   by (import word_base WSPLIT_WSEG1)
   505 
   506 lemma WSPLIT_WSEG2: "(All::(nat => bool) => bool)
   507  (%n::nat.
   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.
   512           (All::(nat => bool) => bool)
   513            (%k::nat.
   514                (op -->::bool => bool => bool)
   515                 ((op <=::nat => nat => bool) k n)
   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)))))"
   524   by (import word_base WSPLIT_WSEG2)
   525 
   526 lemma WCAT_WSEG_WSEG: "ALL n::nat.
   527    RES_FORALL (PWORDLEN n)
   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)"
   532   by (import word_base WCAT_WSEG_WSEG)
   533 
   534 lemma WORD_SPLIT: "ALL (x::nat) xa::nat.
   535    RES_FORALL (PWORDLEN (x + xa))
   536     (%w::'a::type word. w = WCAT (WSEG x xa w, WSEG xa 0 w))"
   537   by (import word_base WORD_SPLIT)
   538 
   539 lemma WORDLEN_SUC_WCAT_WSEG_WSEG: "RES_FORALL (PWORDLEN (Suc (n::nat)))
   540  (%w::'a::type word. w = WCAT (WSEG 1 n w, WSEG n 0 w))"
   541   by (import word_base WORDLEN_SUC_WCAT_WSEG_WSEG)
   542 
   543 lemma WORDLEN_SUC_WCAT_WSEG_WSEG_RIGHT: "RES_FORALL (PWORDLEN (Suc (n::nat)))
   544  (%w::'a::type word. w = WCAT (WSEG n 1 w, WSEG 1 0 w))"
   545   by (import word_base WORDLEN_SUC_WCAT_WSEG_WSEG_RIGHT)
   546 
   547 lemma WORDLEN_SUC_WCAT_BIT_WSEG: "ALL n::nat.
   548    RES_FORALL (PWORDLEN (Suc n))
   549     (%w::'a::type word. w = WCAT (WORD [bit n w], WSEG n 0 w))"
   550   by (import word_base WORDLEN_SUC_WCAT_BIT_WSEG)
   551 
   552 lemma WORDLEN_SUC_WCAT_BIT_WSEG_RIGHT: "ALL n::nat.
   553    RES_FORALL (PWORDLEN (Suc n))
   554     (%w::'a::type word. w = WCAT (WSEG n 1 w, WORD [bit 0 w]))"
   555   by (import word_base WORDLEN_SUC_WCAT_BIT_WSEG_RIGHT)
   556 
   557 lemma WSEG_WCAT1: "ALL (n1::nat) n2::nat.
   558    RES_FORALL (PWORDLEN n1)
   559     (%w1::'a::type word.
   560         RES_FORALL (PWORDLEN n2)
   561          (%w2::'a::type word. WSEG n1 n2 (WCAT (w1, w2)) = w1))"
   562   by (import word_base WSEG_WCAT1)
   563 
   564 lemma WSEG_WCAT2: "ALL (n1::nat) n2::nat.
   565    RES_FORALL (PWORDLEN n1)
   566     (%w1::'a::type word.
   567         RES_FORALL (PWORDLEN n2)
   568          (%w2::'a::type word. WSEG n2 0 (WCAT (w1, w2)) = w2))"
   569   by (import word_base WSEG_WCAT2)
   570 
   571 lemma WSEG_SUC: "ALL n::nat.
   572    RES_FORALL (PWORDLEN n)
   573     (%w::'a::type word.
   574         ALL (k::nat) m1::nat.
   575            k + Suc m1 < n -->
   576            WSEG (Suc m1) k w = WCAT (WSEG 1 (k + m1) w, WSEG m1 k w))"
   577   by (import word_base WSEG_SUC)
   578 
   579 lemma WORD_CONS_WCAT: "ALL (x::'a::type) l::'a::type list. WORD (x # l) = WCAT (WORD [x], WORD l)"
   580   by (import word_base WORD_CONS_WCAT)
   581 
   582 lemma WORD_SNOC_WCAT: "ALL (l::'a::type list) x::'a::type.
   583    WORD (SNOC x l) = WCAT (WORD l, WORD [x])"
   584   by (import word_base WORD_SNOC_WCAT)
   585 
   586 lemma BIT_WCAT_FST: "ALL (n1::nat) n2::nat.
   587    RES_FORALL (PWORDLEN n1)
   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))"
   594   by (import word_base BIT_WCAT_FST)
   595 
   596 lemma BIT_WCAT_SND: "(All::(nat => bool) => bool)
   597  (%n1::nat.
   598      (All::(nat => bool) => bool)
   599       (%n2::nat.
   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.
   608                     (All::(nat => bool) => bool)
   609                      (%k::nat.
   610                          (op -->::bool => bool => bool)
   611                           ((op <::nat => nat => bool) k n2)
   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)
   618                                   w1 w2)))
   619                             ((bit::nat => 'a::type word => 'a::type) k
   620                               w2)))))))"
   621   by (import word_base BIT_WCAT_SND)
   622 
   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)"
   626   by (import word_base BIT_WCAT1)
   627 
   628 lemma WSEG_WCAT_WSEG1: "ALL (n1::nat) n2::nat.
   629    RES_FORALL (PWORDLEN n1)
   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))"
   636   by (import word_base WSEG_WCAT_WSEG1)
   637 
   638 lemma WSEG_WCAT_WSEG2: "ALL (n1::nat) n2::nat.
   639    RES_FORALL (PWORDLEN n1)
   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))"
   645   by (import word_base WSEG_WCAT_WSEG2)
   646 
   647 lemma WSEG_WCAT_WSEG: "ALL (n1::nat) n2::nat.
   648    RES_FORALL (PWORDLEN n1)
   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)) =
   655                 WCAT (WSEG (m + k - n2) 0 w1, WSEG (n2 - k) k w2)))"
   656   by (import word_base WSEG_WCAT_WSEG)
   657 
   658 lemma BIT_EQ_IMP_WORD_EQ: "(All::(nat => bool) => bool)
   659  (%n::nat.
   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.
   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)
   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))))"
   677   by (import word_base BIT_EQ_IMP_WORD_EQ)
   678 
   679 ;end_setup
   680 
   681 ;setup_theory word_num
   682 
   683 constdefs
   684   LVAL :: "('a => nat) => nat => 'a list => nat" 
   685   "LVAL ==
   686 %(f::'a::type => nat) b::nat. foldl (%(e::nat) x::'a::type. b * e + f x) 0"
   687 
   688 lemma LVAL_DEF: "ALL (f::'a::type => nat) (b::nat) l::'a::type list.
   689    LVAL f b l = foldl (%(e::nat) x::'a::type. b * e + f x) 0 l"
   690   by (import word_num LVAL_DEF)
   691 
   692 consts
   693   NVAL :: "('a => nat) => nat => 'a word => nat" 
   694 
   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"
   697   by (import word_num NVAL_DEF)
   698 
   699 lemma LVAL: "(ALL (x::'a::type => nat) xa::nat. LVAL x xa [] = 0) &
   700 (ALL (x::'a::type list) (xa::'a::type => nat) (xb::nat) xc::'a::type.
   701     LVAL xa xb (xc # x) = xa xc * xb ^ length x + LVAL xa xb x)"
   702   by (import word_num LVAL)
   703 
   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"
   706   by (import word_num LVAL_SNOC)
   707 
   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"
   710   by (import word_num LVAL_MAX)
   711 
   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))"
   716   by (import word_num NVAL_MAX)
   717 
   718 lemma NVAL0: "ALL (x::'a::type => nat) xa::nat. NVAL x xa (WORD []) = 0"
   719   by (import word_num NVAL0)
   720 
   721 lemma NVAL1: "ALL (x::'a::type => nat) (xa::nat) xb::'a::type.
   722    NVAL x xa (WORD [xb]) = x xb"
   723   by (import word_num NVAL1)
   724 
   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)"
   727   by (import word_num NVAL_WORDLEN_0)
   728 
   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"
   731   by (import word_num NVAL_WCAT1)
   732 
   733 lemma NVAL_WCAT2: "ALL n::nat.
   734    RES_FORALL (PWORDLEN n)
   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)"
   738   by (import word_num NVAL_WCAT2)
   739 
   740 lemma NVAL_WCAT: "ALL (n::nat) m::nat.
   741    RES_FORALL (PWORDLEN n)
   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))"
   748   by (import word_num NVAL_WCAT)
   749 
   750 consts
   751   NLIST :: "nat => (nat => 'a) => nat => nat => 'a list" 
   752 
   753 specification (NLIST) NLIST_DEF: "(ALL (frep::nat => 'a::type) (b::nat) m::nat. NLIST 0 frep b m = []) &
   754 (ALL (n::nat) (frep::nat => 'a::type) (b::nat) m::nat.
   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
   760   NWORD :: "nat => (nat => 'a) => nat => nat => 'a word" 
   761   "NWORD ==
   762 %(n::nat) (frep::nat => 'a::type) (b::nat) m::nat. WORD (NLIST n frep b m)"
   763 
   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)"
   766   by (import word_num NWORD_DEF)
   767 
   768 lemma NWORD_LENGTH: "ALL (x::nat) (xa::nat => 'a::type) (xb::nat) xc::nat.
   769    WORDLEN (NWORD x xa xb xc) = x"
   770   by (import word_num NWORD_LENGTH)
   771 
   772 lemma NWORD_PWORDLEN: "ALL (x::nat) (xa::nat => 'a::type) (xb::nat) xc::nat.
   773    IN (NWORD x xa xb xc) (PWORDLEN x)"
   774   by (import word_num NWORD_PWORDLEN)
   775 
   776 ;end_setup
   777 
   778 ;setup_theory word_bitop
   779 
   780 consts
   781   PBITOP :: "('a word => 'b word) => bool" 
   782 
   783 defs
   784   PBITOP_primdef: "PBITOP ==
   785 GSPEC
   786  (%oper::'a::type word => 'b::type word.
   787      (oper,
   788       ALL n::nat.
   789          RES_FORALL (PWORDLEN n)
   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)))))"
   794 
   795 lemma PBITOP_def: "PBITOP =
   796 GSPEC
   797  (%oper::'a::type word => 'b::type word.
   798      (oper,
   799       ALL n::nat.
   800          RES_FORALL (PWORDLEN n)
   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)))))"
   805   by (import word_bitop PBITOP_def)
   806 
   807 lemma IN_PBITOP: "ALL oper::'a::type word => 'b::type word.
   808    IN oper PBITOP =
   809    (ALL n::nat.
   810        RES_FORALL (PWORDLEN n)
   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))))"
   815   by (import word_bitop IN_PBITOP)
   816 
   817 lemma PBITOP_PWORDLEN: "RES_FORALL PBITOP
   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)))"
   822   by (import word_bitop PBITOP_PWORDLEN)
   823 
   824 lemma PBITOP_WSEG: "RES_FORALL PBITOP
   825  (%oper::'a::type word => 'b::type word.
   826      ALL n::nat.
   827         RES_FORALL (PWORDLEN n)
   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)))"
   831   by (import word_bitop PBITOP_WSEG)
   832 
   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.
   837      (All::(nat => bool) => bool)
   838       (%n::nat.
   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.
   843                (All::(nat => bool) => bool)
   844                 (%k::nat.
   845                     (op -->::bool => bool => bool)
   846                      ((op <::nat => nat => bool) k n)
   847                      ((op =::'b::type word => 'b::type word => bool)
   848                        (oper
   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))))))))"
   859   by (import word_bitop PBITOP_BIT)
   860 
   861 consts
   862   PBITBOP :: "('a word => 'b word => 'c word) => bool" 
   863 
   864 defs
   865   PBITBOP_primdef: "PBITBOP ==
   866 GSPEC
   867  (%oper::'a::type word => 'b::type word => 'c::type word.
   868      (oper,
   869       ALL n::nat.
   870          RES_FORALL (PWORDLEN n)
   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))))))"
   879 
   880 lemma PBITBOP_def: "PBITBOP =
   881 GSPEC
   882  (%oper::'a::type word => 'b::type word => 'c::type word.
   883      (oper,
   884       ALL n::nat.
   885          RES_FORALL (PWORDLEN n)
   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))))))"
   894   by (import word_bitop PBITBOP_def)
   895 
   896 lemma IN_PBITBOP: "ALL oper::'a::type word => 'b::type word => 'c::type word.
   897    IN oper PBITBOP =
   898    (ALL n::nat.
   899        RES_FORALL (PWORDLEN n)
   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)))))"
   908   by (import word_bitop IN_PBITBOP)
   909 
   910 lemma PBITBOP_PWORDLEN: "RES_FORALL PBITBOP
   911  (%oper::'a::type word => 'b::type word => 'c::type word.
   912      ALL n::nat.
   913         RES_FORALL (PWORDLEN n)
   914          (%w1::'a::type word.
   915              RES_FORALL (PWORDLEN n)
   916               (%w2::'b::type word. IN (oper w1 w2) (PWORDLEN n))))"
   917   by (import word_bitop PBITBOP_PWORDLEN)
   918 
   919 lemma PBITBOP_WSEG: "RES_FORALL PBITBOP
   920  (%oper::'a::type word => 'b::type word => 'c::type word.
   921      ALL n::nat.
   922         RES_FORALL (PWORDLEN n)
   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))))"
   930   by (import word_bitop PBITBOP_WSEG)
   931 
   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)"
   936   by (import word_bitop PBITBOP_EXISTS)
   937 
   938 consts
   939   WMAP :: "('a => 'b) => 'a word => 'b word" 
   940 
   941 specification (WMAP) WMAP_DEF: "ALL (f::'a::type => 'b::type) l::'a::type list.
   942    WMAP f (WORD l) = WORD (map f l)"
   943   by (import word_bitop WMAP_DEF)
   944 
   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))"
   948   by (import word_bitop WMAP_PWORDLEN)
   949 
   950 lemma WMAP_0: "ALL x::'a::type => 'b::type. WMAP x (WORD []) = WORD []"
   951   by (import word_bitop WMAP_0)
   952 
   953 lemma WMAP_BIT: "(All::(nat => bool) => bool)
   954  (%n::nat.
   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.
   959           (All::(nat => bool) => bool)
   960            (%k::nat.
   961                (op -->::bool => bool => bool)
   962                 ((op <::nat => nat => bool) k n)
   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)))))))"
   972   by (import word_bitop WMAP_BIT)
   973 
   974 lemma WMAP_WSEG: "ALL n::nat.
   975    RES_FORALL (PWORDLEN n)
   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)))"
   981   by (import word_bitop WMAP_WSEG)
   982 
   983 lemma WMAP_PBITOP: "ALL f::'a::type => 'b::type. IN (WMAP f) PBITOP"
   984   by (import word_bitop WMAP_PBITOP)
   985 
   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)"
   988   by (import word_bitop WMAP_WCAT)
   989 
   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"
   992   by (import word_bitop WMAP_o)
   993 
   994 consts
   995   FORALLBITS :: "('a => bool) => 'a word => bool" 
   996 
   997 specification (FORALLBITS) FORALLBITS_DEF: "ALL (P::'a::type => bool) l::'a::type list.
   998    FORALLBITS P (WORD l) = list_all P l"
   999   by (import word_bitop FORALLBITS_DEF)
  1000 
  1001 lemma FORALLBITS: "(All::(nat => bool) => bool)
  1002  (%n::nat.
  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.
  1009                (op =::bool => bool => bool)
  1010                 ((FORALLBITS::('a::type => bool) => 'a::type word => bool) P
  1011                   w)
  1012                 ((All::(nat => bool) => bool)
  1013                   (%k::nat.
  1014                       (op -->::bool => bool => bool)
  1015                        ((op <::nat => nat => bool) k n)
  1016                        (P ((bit::nat => 'a::type word => 'a::type) k
  1017                             w)))))))"
  1018   by (import word_bitop FORALLBITS)
  1019 
  1020 lemma FORALLBITS_WSEG: "ALL n::nat.
  1021    RES_FORALL (PWORDLEN n)
  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)))"
  1026   by (import word_bitop FORALLBITS_WSEG)
  1027 
  1028 lemma FORALLBITS_WCAT: "ALL (w1::'a::type word) (w2::'a::type word) P::'a::type => bool.
  1029    FORALLBITS P (WCAT (w1, w2)) = (FORALLBITS P w1 & FORALLBITS P w2)"
  1030   by (import word_bitop FORALLBITS_WCAT)
  1031 
  1032 consts
  1033   EXISTSABIT :: "('a => bool) => 'a word => bool" 
  1034 
  1035 specification (EXISTSABIT) EXISTSABIT_DEF: "ALL (P::'a::type => bool) l::'a::type list.
  1036    EXISTSABIT P (WORD l) = list_exists P l"
  1037   by (import word_bitop EXISTSABIT_DEF)
  1038 
  1039 lemma NOT_EXISTSABIT: "ALL (P::'a::type => bool) w::'a::type word.
  1040    (~ EXISTSABIT P w) = FORALLBITS (Not o P) w"
  1041   by (import word_bitop NOT_EXISTSABIT)
  1042 
  1043 lemma NOT_FORALLBITS: "ALL (P::'a::type => bool) w::'a::type word.
  1044    (~ FORALLBITS P w) = EXISTSABIT (Not o P) w"
  1045   by (import word_bitop NOT_FORALLBITS)
  1046 
  1047 lemma EXISTSABIT: "(All::(nat => bool) => bool)
  1048  (%n::nat.
  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.
  1055                (op =::bool => bool => bool)
  1056                 ((EXISTSABIT::('a::type => bool) => 'a::type word => bool) P
  1057                   w)
  1058                 ((Ex::(nat => bool) => bool)
  1059                   (%k::nat.
  1060                       (op &::bool => bool => bool)
  1061                        ((op <::nat => nat => bool) k n)
  1062                        (P ((bit::nat => 'a::type word => 'a::type) k
  1063                             w)))))))"
  1064   by (import word_bitop EXISTSABIT)
  1065 
  1066 lemma EXISTSABIT_WSEG: "ALL n::nat.
  1067    RES_FORALL (PWORDLEN n)
  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))"
  1073   by (import word_bitop EXISTSABIT_WSEG)
  1074 
  1075 lemma EXISTSABIT_WCAT: "ALL (w1::'a::type word) (w2::'a::type word) P::'a::type => bool.
  1076    EXISTSABIT P (WCAT (w1, w2)) = (EXISTSABIT P w1 | EXISTSABIT P w2)"
  1077   by (import word_bitop EXISTSABIT_WCAT)
  1078 
  1079 constdefs
  1080   SHR :: "bool => 'a => 'a word => 'a word * 'a" 
  1081   "SHR ==
  1082 %(f::bool) (b::'a::type) w::'a::type word.
  1083    (WCAT
  1084      (if f then WSEG 1 (PRE (WORDLEN w)) w else WORD [b],
  1085       WSEG (PRE (WORDLEN w)) 1 w),
  1086     bit 0 w)"
  1087 
  1088 lemma SHR_DEF: "ALL (f::bool) (b::'a::type) w::'a::type word.
  1089    SHR f b w =
  1090    (WCAT
  1091      (if f then WSEG 1 (PRE (WORDLEN w)) w else WORD [b],
  1092       WSEG (PRE (WORDLEN w)) 1 w),
  1093     bit 0 w)"
  1094   by (import word_bitop SHR_DEF)
  1095 
  1096 constdefs
  1097   SHL :: "bool => 'a word => 'a => 'a * 'a word" 
  1098   "SHL ==
  1099 %(f::bool) (w::'a::type word) b::'a::type.
  1100    (bit (PRE (WORDLEN w)) w,
  1101     WCAT (WSEG (PRE (WORDLEN w)) 0 w, if f then WSEG 1 0 w else WORD [b]))"
  1102 
  1103 lemma SHL_DEF: "ALL (f::bool) (w::'a::type word) b::'a::type.
  1104    SHL f w b =
  1105    (bit (PRE (WORDLEN w)) w,
  1106     WCAT (WSEG (PRE (WORDLEN w)) 0 w, if f then WSEG 1 0 w else WORD [b]))"
  1107   by (import word_bitop SHL_DEF)
  1108 
  1109 lemma SHR_WSEG: "ALL n::nat.
  1110    RES_FORALL (PWORDLEN n)
  1111     (%w::'a::type word.
  1112         ALL (m::nat) k::nat.
  1113            m + k <= n -->
  1114            0 < m -->
  1115            (ALL (f::bool) b::'a::type.
  1116                SHR f b (WSEG m k w) =
  1117                (if f
  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),
  1120                 bit k w)))"
  1121   by (import word_bitop SHR_WSEG)
  1122 
  1123 lemma SHR_WSEG_1F: "ALL n::nat.
  1124    RES_FORALL (PWORDLEN n)
  1125     (%w::'a::type word.
  1126         ALL (b::'a::type) (m::nat) k::nat.
  1127            m + k <= n -->
  1128            0 < m -->
  1129            SHR False b (WSEG m k w) =
  1130            (WCAT (WORD [b], WSEG (m - 1) (k + 1) w), bit k w))"
  1131   by (import word_bitop SHR_WSEG_1F)
  1132 
  1133 lemma SHR_WSEG_NF: "ALL n::nat.
  1134    RES_FORALL (PWORDLEN n)
  1135     (%w::'a::type word.
  1136         ALL (m::nat) k::nat.
  1137            m + k < n -->
  1138            0 < m -->
  1139            SHR False (bit (m + k) w) (WSEG m k w) =
  1140            (WSEG m (k + 1) w, bit k w))"
  1141   by (import word_bitop SHR_WSEG_NF)
  1142 
  1143 lemma SHL_WSEG: "ALL n::nat.
  1144    RES_FORALL (PWORDLEN n)
  1145     (%w::'a::type word.
  1146         ALL (m::nat) k::nat.
  1147            m + k <= n -->
  1148            0 < m -->
  1149            (ALL (f::bool) b::'a::type.
  1150                SHL f (WSEG m k w) b =
  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]))))"
  1154   by (import word_bitop SHL_WSEG)
  1155 
  1156 lemma SHL_WSEG_1F: "ALL n::nat.
  1157    RES_FORALL (PWORDLEN n)
  1158     (%w::'a::type word.
  1159         ALL (b::'a::type) (m::nat) k::nat.
  1160            m + k <= n -->
  1161            0 < m -->
  1162            SHL False (WSEG m k w) b =
  1163            (bit (k + (m - 1)) w, WCAT (WSEG (m - 1) k w, WORD [b])))"
  1164   by (import word_bitop SHL_WSEG_1F)
  1165 
  1166 lemma SHL_WSEG_NF: "ALL n::nat.
  1167    RES_FORALL (PWORDLEN n)
  1168     (%w::'a::type word.
  1169         ALL (m::nat) k::nat.
  1170            m + k <= n -->
  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))"
  1175   by (import word_bitop SHL_WSEG_NF)
  1176 
  1177 lemma WSEG_SHL: "ALL n::nat.
  1178    RES_FORALL (PWORDLEN (Suc n))
  1179     (%w::'a::type word.
  1180         ALL (m::nat) k::nat.
  1181            0 < k & m + k <= Suc n -->
  1182            (ALL b::'a::type.
  1183                WSEG m k (snd (SHL (f::bool) w b)) = WSEG m (k - 1) w))"
  1184   by (import word_bitop WSEG_SHL)
  1185 
  1186 lemma WSEG_SHL_0: "ALL n::nat.
  1187    RES_FORALL (PWORDLEN (Suc n))
  1188     (%w::'a::type word.
  1189         ALL (m::nat) b::'a::type.
  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]))"
  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" 
  1201   "BV == %b::bool. if b then Suc 0 else 0"
  1202 
  1203 lemma BV_DEF: "ALL b::bool. BV b = (if b then Suc 0 else 0)"
  1204   by (import bword_num BV_DEF)
  1205 
  1206 consts
  1207   BNVAL :: "bool word => nat" 
  1208 
  1209 specification (BNVAL) BNVAL_DEF: "ALL l::bool list. BNVAL (WORD l) = LVAL BV 2 l"
  1210   by (import bword_num BNVAL_DEF)
  1211 
  1212 lemma BV_LESS_2: "ALL x::bool. BV x < 2"
  1213   by (import bword_num BV_LESS_2)
  1214 
  1215 lemma BNVAL_NVAL: "ALL w::bool word. BNVAL w = NVAL BV 2 w"
  1216   by (import bword_num BNVAL_NVAL)
  1217 
  1218 lemma BNVAL0: "BNVAL (WORD []) = 0"
  1219   by (import bword_num BNVAL0)
  1220 
  1221 lemma BNVAL_11: "ALL (w1::bool word) w2::bool word.
  1222    WORDLEN w1 = WORDLEN w2 --> BNVAL w1 = BNVAL w2 --> w1 = w2"
  1223   by (import bword_num BNVAL_11)
  1224 
  1225 lemma BNVAL_ONTO: "ALL w::bool word. Ex (op = (BNVAL w))"
  1226   by (import bword_num BNVAL_ONTO)
  1227 
  1228 lemma BNVAL_MAX: "ALL n::nat. RES_FORALL (PWORDLEN n) (%w::bool word. BNVAL w < 2 ^ n)"
  1229   by (import bword_num BNVAL_MAX)
  1230 
  1231 lemma BNVAL_WCAT1: "ALL n::nat.
  1232    RES_FORALL (PWORDLEN n)
  1233     (%w::bool word.
  1234         ALL x::bool. BNVAL (WCAT (w, WORD [x])) = BNVAL w * 2 + BV x)"
  1235   by (import bword_num BNVAL_WCAT1)
  1236 
  1237 lemma BNVAL_WCAT2: "ALL n::nat.
  1238    RES_FORALL (PWORDLEN n)
  1239     (%w::bool word.
  1240         ALL x::bool. BNVAL (WCAT (WORD [x], w)) = BV x * 2 ^ n + BNVAL w)"
  1241   by (import bword_num BNVAL_WCAT2)
  1242 
  1243 lemma BNVAL_WCAT: "ALL (n::nat) m::nat.
  1244    RES_FORALL (PWORDLEN n)
  1245     (%w1::bool word.
  1246         RES_FORALL (PWORDLEN m)
  1247          (%w2::bool word.
  1248              BNVAL (WCAT (w1, w2)) = BNVAL w1 * 2 ^ m + BNVAL w2))"
  1249   by (import bword_num BNVAL_WCAT)
  1250 
  1251 constdefs
  1252   VB :: "nat => bool" 
  1253   "VB == %n::nat. n mod 2 ~= 0"
  1254 
  1255 lemma VB_DEF: "ALL n::nat. VB n = (n mod 2 ~= 0)"
  1256   by (import bword_num VB_DEF)
  1257 
  1258 constdefs
  1259   NBWORD :: "nat => nat => bool word" 
  1260   "NBWORD == %(n::nat) m::nat. WORD (NLIST n VB 2 m)"
  1261 
  1262 lemma NBWORD_DEF: "ALL (n::nat) m::nat. NBWORD n m = WORD (NLIST n VB 2 m)"
  1263   by (import bword_num NBWORD_DEF)
  1264 
  1265 lemma NBWORD0: "ALL x::nat. NBWORD 0 x = WORD []"
  1266   by (import bword_num NBWORD0)
  1267 
  1268 lemma WORDLEN_NBWORD: "ALL (x::nat) xa::nat. WORDLEN (NBWORD x xa) = x"
  1269   by (import bword_num WORDLEN_NBWORD)
  1270 
  1271 lemma PWORDLEN_NBWORD: "ALL (x::nat) xa::nat. IN (NBWORD x xa) (PWORDLEN x)"
  1272   by (import bword_num PWORDLEN_NBWORD)
  1273 
  1274 lemma NBWORD_SUC: "ALL (n::nat) m::nat.
  1275    NBWORD (Suc n) m = WCAT (NBWORD n (m div 2), WORD [VB (m mod 2)])"
  1276   by (import bword_num NBWORD_SUC)
  1277 
  1278 lemma VB_BV: "ALL x::bool. VB (BV x) = x"
  1279   by (import bword_num VB_BV)
  1280 
  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)
  1286           ((op BIT::bin => bit => bin)
  1287             ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
  1288             (bit.B0::bit))))
  1289       ((op =::nat => nat => bool) ((BV::bool => nat) ((VB::nat => bool) x))
  1290         x))"
  1291   by (import bword_num BV_VB)
  1292 
  1293 lemma NBWORD_BNVAL: "ALL n::nat. RES_FORALL (PWORDLEN n) (%w::bool word. NBWORD n (BNVAL w) = w)"
  1294   by (import bword_num NBWORD_BNVAL)
  1295 
  1296 lemma BNVAL_NBWORD: "ALL (n::nat) m::nat. m < 2 ^ n --> BNVAL (NBWORD n m) = m"
  1297   by (import bword_num BNVAL_NBWORD)
  1298 
  1299 lemma ZERO_WORD_VAL: "RES_FORALL (PWORDLEN (n::nat))
  1300  (%w::bool word. (w = NBWORD n 0) = (BNVAL w = 0))"
  1301   by (import bword_num ZERO_WORD_VAL)
  1302 
  1303 lemma WCAT_NBWORD_0: "ALL (n1::nat) n2::nat. WCAT (NBWORD n1 0, NBWORD n2 0) = NBWORD (n1 + n2) 0"
  1304   by (import bword_num WCAT_NBWORD_0)
  1305 
  1306 lemma WSPLIT_NBWORD_0: "ALL (n::nat) m::nat.
  1307    m <= n --> WSPLIT m (NBWORD n 0) = (NBWORD (n - m) 0, NBWORD m 0)"
  1308   by (import bword_num WSPLIT_NBWORD_0)
  1309 
  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))))))))"
  1332   by (import bword_num EQ_NBWORD0_SPLIT)
  1333 
  1334 lemma NBWORD_MOD: "ALL (n::nat) m::nat. NBWORD n (m mod 2 ^ n) = NBWORD n m"
  1335   by (import bword_num NBWORD_MOD)
  1336 
  1337 lemma WSEG_NBWORD_SUC: "ALL (n::nat) m::nat. WSEG n 0 (NBWORD (Suc n) m) = NBWORD n m"
  1338   by (import bword_num WSEG_NBWORD_SUC)
  1339 
  1340 lemma NBWORD_SUC_WSEG: "ALL n::nat.
  1341    RES_FORALL (PWORDLEN (Suc n))
  1342     (%w::bool word. NBWORD n (BNVAL w) = WSEG n 0 w)"
  1343   by (import bword_num NBWORD_SUC_WSEG)
  1344 
  1345 lemma DOUBL_EQ_SHL: "ALL x>0.
  1346    RES_FORALL (PWORDLEN x)
  1347     (%xa::bool word.
  1348         ALL xb::bool.
  1349            NBWORD x (BNVAL xa + BNVAL xa + BV xb) = snd (SHL False xa xb))"
  1350   by (import bword_num DOUBL_EQ_SHL)
  1351 
  1352 lemma MSB_NBWORD: "ALL (n::nat) m::nat. bit n (NBWORD (Suc n) m) = VB (m div 2 ^ n mod 2)"
  1353   by (import bword_num MSB_NBWORD)
  1354 
  1355 lemma NBWORD_SPLIT: "ALL (n1::nat) (n2::nat) m::nat.
  1356    NBWORD (n1 + n2) m = WCAT (NBWORD n1 (m div 2 ^ n2), NBWORD n2 m)"
  1357   by (import bword_num NBWORD_SPLIT)
  1358 
  1359 lemma WSEG_NBWORD: "ALL (m::nat) (k::nat) n::nat.
  1360    m + k <= n -->
  1361    (ALL l::nat. WSEG m k (NBWORD n l) = NBWORD m (l div 2 ^ k))"
  1362   by (import bword_num WSEG_NBWORD)
  1363 
  1364 lemma NBWORD_SUC_FST: "ALL (n::nat) x::nat.
  1365    NBWORD (Suc n) x = WCAT (WORD [VB (x div 2 ^ n mod 2)], NBWORD n x)"
  1366   by (import bword_num NBWORD_SUC_FST)
  1367 
  1368 lemma BIT_NBWORD0: "ALL (k::nat) n::nat. k < n --> bit k (NBWORD n 0) = False"
  1369   by (import bword_num BIT_NBWORD0)
  1370 
  1371 lemma ADD_BNVAL_LEFT: "ALL n::nat.
  1372    RES_FORALL (PWORDLEN (Suc n))
  1373     (%w1::bool word.
  1374         RES_FORALL (PWORDLEN (Suc n))
  1375          (%w2::bool word.
  1376              BNVAL w1 + BNVAL w2 =
  1377              (BV (bit n w1) + BV (bit n w2)) * 2 ^ n +
  1378              (BNVAL (WSEG n 0 w1) + BNVAL (WSEG n 0 w2))))"
  1379   by (import bword_num ADD_BNVAL_LEFT)
  1380 
  1381 lemma ADD_BNVAL_RIGHT: "ALL n::nat.
  1382    RES_FORALL (PWORDLEN (Suc n))
  1383     (%w1::bool word.
  1384         RES_FORALL (PWORDLEN (Suc n))
  1385          (%w2::bool word.
  1386              BNVAL w1 + BNVAL w2 =
  1387              (BNVAL (WSEG n 1 w1) + BNVAL (WSEG n 1 w2)) * 2 +
  1388              (BV (bit 0 w1) + BV (bit 0 w2))))"
  1389   by (import bword_num ADD_BNVAL_RIGHT)
  1390 
  1391 lemma ADD_BNVAL_SPLIT: "ALL (n1::nat) n2::nat.
  1392    RES_FORALL (PWORDLEN (n1 + n2))
  1393     (%w1::bool word.
  1394         RES_FORALL (PWORDLEN (n1 + n2))
  1395          (%w2::bool word.
  1396              BNVAL w1 + BNVAL w2 =
  1397              (BNVAL (WSEG n1 n2 w1) + BNVAL (WSEG n1 n2 w2)) * 2 ^ n2 +
  1398              (BNVAL (WSEG n2 0 w1) + BNVAL (WSEG n2 0 w2))))"
  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 
  1408 specification (ACARRY) ACARRY_DEF: "(ALL (w1::bool word) (w2::bool word) cin::bool. ACARRY 0 w1 w2 cin = cin) &
  1409 (ALL (n::nat) (w1::bool word) (w2::bool word) cin::bool.
  1410     ACARRY (Suc n) w1 w2 cin =
  1411     VB ((BV (bit n w1) + BV (bit n w2) + BV (ACARRY n w1 w2 cin)) div 2))"
  1412   by (import bword_arith ACARRY_DEF)
  1413 
  1414 consts
  1415   ICARRY :: "nat => bool word => bool word => bool => bool" 
  1416 
  1417 specification (ICARRY) ICARRY_DEF: "(ALL (w1::bool word) (w2::bool word) cin::bool. ICARRY 0 w1 w2 cin = cin) &
  1418 (ALL (n::nat) (w1::bool word) (w2::bool word) cin::bool.
  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 
  1423 lemma ACARRY_EQ_ICARRY: "ALL n::nat.
  1424    RES_FORALL (PWORDLEN n)
  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))"
  1430   by (import bword_arith ACARRY_EQ_ICARRY)
  1431 
  1432 lemma BNVAL_LESS_EQ: "ALL n::nat. RES_FORALL (PWORDLEN n) (%w::bool word. BNVAL w <= 2 ^ n - 1)"
  1433   by (import bword_arith BNVAL_LESS_EQ)
  1434 
  1435 lemma ADD_BNVAL_LESS_EQ1: "ALL (n::nat) cin::bool.
  1436    RES_FORALL (PWORDLEN n)
  1437     (%w1::bool word.
  1438         RES_FORALL (PWORDLEN n)
  1439          (%w2::bool word.
  1440              (BNVAL w1 + (BNVAL w2 + BV cin)) div 2 ^ n <= Suc 0))"
  1441   by (import bword_arith ADD_BNVAL_LESS_EQ1)
  1442 
  1443 lemma ADD_BV_BNVAL_DIV_LESS_EQ1: "ALL (n::nat) (x1::bool) (x2::bool) cin::bool.
  1444    RES_FORALL (PWORDLEN n)
  1445     (%w1::bool word.
  1446         RES_FORALL (PWORDLEN n)
  1447          (%w2::bool word.
  1448              (BV x1 + BV x2 +
  1449               (BNVAL w1 + (BNVAL w2 + BV cin)) div 2 ^ n) div
  1450              2
  1451              <= 1))"
  1452   by (import bword_arith ADD_BV_BNVAL_DIV_LESS_EQ1)
  1453 
  1454 lemma ADD_BV_BNVAL_LESS_EQ: "ALL (n::nat) (x1::bool) (x2::bool) cin::bool.
  1455    RES_FORALL (PWORDLEN n)
  1456     (%w1::bool word.
  1457         RES_FORALL (PWORDLEN n)
  1458          (%w2::bool word.
  1459              BV x1 + BV x2 + (BNVAL w1 + (BNVAL w2 + BV cin))
  1460              <= Suc (2 ^ Suc n)))"
  1461   by (import bword_arith ADD_BV_BNVAL_LESS_EQ)
  1462 
  1463 lemma ADD_BV_BNVAL_LESS_EQ1: "ALL (n::nat) (x1::bool) (x2::bool) cin::bool.
  1464    RES_FORALL (PWORDLEN n)
  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
  1469              2 ^ Suc n
  1470              <= 1))"
  1471   by (import bword_arith ADD_BV_BNVAL_LESS_EQ1)
  1472 
  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)
  1503                              ((op BIT::bin => bit => bin)
  1504                                ((op BIT::bin => bit => bin)
  1505                                  (Numeral.Pls::bin) (bit.B1::bit))
  1506                                (bit.B0::bit)))
  1507                            k)))))))"
  1508   by (import bword_arith ACARRY_EQ_ADD_DIV)
  1509 
  1510 lemma ADD_WORD_SPLIT: "ALL (n1::nat) n2::nat.
  1511    RES_FORALL (PWORDLEN (n1 + n2))
  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
  1522                    (BNVAL (WSEG n2 0 w1) + BNVAL (WSEG n2 0 w2) + BV cin))))"
  1523   by (import bword_arith ADD_WORD_SPLIT)
  1524 
  1525 lemma WSEG_NBWORD_ADD: "ALL n::nat.
  1526    RES_FORALL (PWORDLEN n)
  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))))"
  1536   by (import bword_arith WSEG_NBWORD_ADD)
  1537 
  1538 lemma ADD_NBWORD_EQ0_SPLIT: "ALL (n1::nat) n2::nat.
  1539    RES_FORALL (PWORDLEN (n1 + n2))
  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) =
  1545                  NBWORD (n1 + n2) 0) =
  1546                 (NBWORD n1
  1547                   (BNVAL (WSEG n1 n2 w1) + BNVAL (WSEG n1 n2 w2) +
  1548                    BV (ACARRY n2 w1 w2 cin)) =
  1549                  NBWORD n1 0 &
  1550                  NBWORD n2
  1551                   (BNVAL (WSEG n2 0 w1) + BNVAL (WSEG n2 0 w2) + BV cin) =
  1552                  NBWORD n2 0)))"
  1553   by (import bword_arith ADD_NBWORD_EQ0_SPLIT)
  1554 
  1555 lemma ACARRY_MSB: "ALL n::nat.
  1556    RES_FORALL (PWORDLEN n)
  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))))"
  1563   by (import bword_arith ACARRY_MSB)
  1564 
  1565 lemma ACARRY_WSEG: "ALL n::nat.
  1566    RES_FORALL (PWORDLEN n)
  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 -->
  1572                 ACARRY k (WSEG m 0 w1) (WSEG m 0 w2) cin =
  1573                 ACARRY k w1 w2 cin))"
  1574   by (import bword_arith ACARRY_WSEG)
  1575 
  1576 lemma ICARRY_WSEG: "ALL n::nat.
  1577    RES_FORALL (PWORDLEN n)
  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 -->
  1583                 ICARRY k (WSEG m 0 w1) (WSEG m 0 w2) cin =
  1584                 ICARRY k w1 w2 cin))"
  1585   by (import bword_arith ICARRY_WSEG)
  1586 
  1587 lemma ACARRY_ACARRY_WSEG: "ALL n::nat.
  1588    RES_FORALL (PWORDLEN n)
  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))"
  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 
  1606 specification (WNOT) WNOT_DEF: "ALL l::bool list. WNOT (WORD l) = WORD (map Not l)"
  1607   by (import bword_bitop WNOT_DEF)
  1608 
  1609 lemma PBITOP_WNOT: "IN WNOT PBITOP"
  1610   by (import bword_bitop PBITOP_WNOT)
  1611 
  1612 lemma WNOT_WNOT: "ALL w::bool word. WNOT (WNOT w) = w"
  1613   by (import bword_bitop WNOT_WNOT)
  1614 
  1615 lemma WCAT_WNOT: "ALL (n1::nat) n2::nat.
  1616    RES_FORALL (PWORDLEN n1)
  1617     (%w1::bool word.
  1618         RES_FORALL (PWORDLEN n2)
  1619          (%w2::bool word. WCAT (WNOT w1, WNOT w2) = WNOT (WCAT (w1, w2))))"
  1620   by (import bword_bitop WCAT_WNOT)
  1621 
  1622 consts
  1623   WAND :: "bool word => bool word => bool word" 
  1624 
  1625 specification (WAND) WAND_DEF: "ALL (l1::bool list) l2::bool list.
  1626    WAND (WORD l1) (WORD l2) = WORD (map2 op & l1 l2)"
  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 
  1635 specification (WOR) WOR_DEF: "ALL (l1::bool list) l2::bool list.
  1636    WOR (WORD l1) (WORD l2) = WORD (map2 op | l1 l2)"
  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 
  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)"
  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