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