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