src/HOL/Library/Word.thy
author nipkow
Wed, 18 Aug 2004 11:09:40 +0200
changeset 15140 322485b816ac
parent 15131 c69542757a4d
child 15325 50ac7d2c34c9
permissions -rw-r--r--
import -> imports
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
14494
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
     1
(*  Title:      HOL/Library/Word.thy
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
     2
    ID:         $Id$
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
     3
    Author:     Sebastian Skalberg (TU Muenchen)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
     4
*)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
     5
14706
71590b7733b7 tuned document;
wenzelm
parents: 14589
diff changeset
     6
header {* Binary Words *}
14589
feae7b5fd425 tuned document;
wenzelm
parents: 14565
diff changeset
     7
15131
c69542757a4d New theory header syntax.
nipkow
parents: 15067
diff changeset
     8
theory Word
15140
322485b816ac import -> imports
nipkow
parents: 15131
diff changeset
     9
imports Main
15131
c69542757a4d New theory header syntax.
nipkow
parents: 15067
diff changeset
    10
files "word_setup.ML"
c69542757a4d New theory header syntax.
nipkow
parents: 15067
diff changeset
    11
begin
14494
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    12
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    13
subsection {* Auxilary Lemmas *}
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    14
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    15
lemma max_le [intro!]: "[| x \<le> z; y \<le> z |] ==> max x y \<le> z"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    16
  by (simp add: max_def)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    17
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    18
lemma max_mono:
15067
02be3516e90b removed some obsolete proofs
paulson
parents: 15013
diff changeset
    19
  fixes x :: "'a::linorder"
14494
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    20
  assumes mf: "mono f"
15067
02be3516e90b removed some obsolete proofs
paulson
parents: 15013
diff changeset
    21
  shows       "max (f x) (f y) \<le> f (max x y)"
14494
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    22
proof -
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    23
  from mf and le_maxI1 [of x y]
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    24
  have fx: "f x \<le> f (max x y)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    25
    by (rule monoD)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    26
  from mf and le_maxI2 [of y x]
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    27
  have fy: "f y \<le> f (max x y)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    28
    by (rule monoD)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    29
  from fx and fy
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    30
  show "max (f x) (f y) \<le> f (max x y)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    31
    by auto
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    32
qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    33
15067
02be3516e90b removed some obsolete proofs
paulson
parents: 15013
diff changeset
    34
declare zero_le_power [intro]
02be3516e90b removed some obsolete proofs
paulson
parents: 15013
diff changeset
    35
    and zero_less_power [intro]
14494
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    36
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    37
lemma int_nat_two_exp: "2 ^ k = int (2 ^ k)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    38
  by (induct k,simp_all)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    39
14589
feae7b5fd425 tuned document;
wenzelm
parents: 14565
diff changeset
    40
subsection {* Bits *}
14494
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    41
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    42
datatype bit
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    43
  = Zero ("\<zero>")
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    44
  | One ("\<one>")
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    45
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    46
consts
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    47
  bitval :: "bit => int"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    48
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    49
primrec
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    50
  "bitval \<zero> = 0"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    51
  "bitval \<one> = 1"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    52
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    53
consts
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    54
  bitnot :: "bit => bit"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    55
  bitand :: "bit => bit => bit" (infixr "bitand" 35)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    56
  bitor  :: "bit => bit => bit" (infixr "bitor"  30)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    57
  bitxor :: "bit => bit => bit" (infixr "bitxor" 30)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    58
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    59
syntax (xsymbols)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    60
  bitnot :: "bit => bit"        ("\<not>\<^sub>b _" [40] 40)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    61
  bitand :: "bit => bit => bit" (infixr "\<and>\<^sub>b" 35)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    62
  bitor  :: "bit => bit => bit" (infixr "\<or>\<^sub>b" 30)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    63
  bitxor :: "bit => bit => bit" (infixr "\<oplus>\<^sub>b" 30)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    64
14565
c6dc17aab88a use more symbols in HTML output
kleing
parents: 14494
diff changeset
    65
syntax (HTML output)
c6dc17aab88a use more symbols in HTML output
kleing
parents: 14494
diff changeset
    66
  bitnot :: "bit => bit"        ("\<not>\<^sub>b _" [40] 40)
c6dc17aab88a use more symbols in HTML output
kleing
parents: 14494
diff changeset
    67
  bitand :: "bit => bit => bit" (infixr "\<and>\<^sub>b" 35)
c6dc17aab88a use more symbols in HTML output
kleing
parents: 14494
diff changeset
    68
  bitor  :: "bit => bit => bit" (infixr "\<or>\<^sub>b" 30)
c6dc17aab88a use more symbols in HTML output
kleing
parents: 14494
diff changeset
    69
  bitxor :: "bit => bit => bit" (infixr "\<oplus>\<^sub>b" 30)
c6dc17aab88a use more symbols in HTML output
kleing
parents: 14494
diff changeset
    70
14494
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    71
primrec
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    72
  bitnot_zero: "(bitnot \<zero>) = \<one>"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    73
  bitnot_one : "(bitnot \<one>)  = \<zero>"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    74
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    75
primrec
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    76
  bitand_zero: "(\<zero> bitand y) = \<zero>"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    77
  bitand_one:  "(\<one> bitand y) = y"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    78
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    79
primrec
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    80
  bitor_zero: "(\<zero> bitor y) = y"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    81
  bitor_one:  "(\<one> bitor y) = \<one>"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    82
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    83
primrec
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    84
  bitxor_zero: "(\<zero> bitxor y) = y"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    85
  bitxor_one:  "(\<one> bitxor y) = (bitnot y)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    86
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    87
lemma [simp]: "(bitnot (bitnot b)) = b"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    88
  by (cases b,simp_all)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    89
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    90
lemma [simp]: "(b bitand b) = b"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    91
  by (cases b,simp_all)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    92
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    93
lemma [simp]: "(b bitor b) = b"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    94
  by (cases b,simp_all)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    95
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    96
lemma [simp]: "(b bitxor b) = \<zero>"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    97
  by (cases b,simp_all)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
    98
14589
feae7b5fd425 tuned document;
wenzelm
parents: 14565
diff changeset
    99
subsection {* Bit Vectors *}
14494
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   100
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   101
text {* First, a couple of theorems expressing case analysis and
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   102
induction principles for bit vectors. *}
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   103
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   104
lemma bit_list_cases:
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   105
  assumes empty: "w = [] ==> P w"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   106
  and     zero:  "!!bs. w = \<zero> # bs ==> P w"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   107
  and     one:   "!!bs. w = \<one> # bs ==> P w"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   108
  shows   "P w"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   109
proof (cases w)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   110
  assume "w = []"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   111
  thus ?thesis
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   112
    by (rule empty)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   113
next
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   114
  fix b bs
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   115
  assume [simp]: "w = b # bs"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   116
  show "P w"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   117
  proof (cases b)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   118
    assume "b = \<zero>"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   119
    hence "w = \<zero> # bs"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   120
      by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   121
    thus ?thesis
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   122
      by (rule zero)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   123
  next
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   124
    assume "b = \<one>"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   125
    hence "w = \<one> # bs"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   126
      by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   127
    thus ?thesis
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   128
      by (rule one)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   129
  qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   130
qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   131
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   132
lemma bit_list_induct:
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   133
  assumes empty: "P []"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   134
  and     zero:  "!!bs. P bs ==> P (\<zero>#bs)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   135
  and     one:   "!!bs. P bs ==> P (\<one>#bs)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   136
  shows   "P w"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   137
proof (induct w,simp_all add: empty)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   138
  fix b bs
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   139
  assume [intro!]: "P bs"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   140
  show "P (b#bs)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   141
    by (cases b,auto intro!: zero one)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   142
qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   143
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   144
constdefs
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   145
  bv_msb :: "bit list => bit"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   146
  "bv_msb w == if w = [] then \<zero> else hd w"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   147
  bv_extend :: "[nat,bit,bit list]=>bit list"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   148
  "bv_extend i b w == (replicate (i - length w) b) @ w"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   149
  bv_not :: "bit list => bit list"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   150
  "bv_not w == map bitnot w"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   151
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   152
lemma bv_length_extend [simp]: "length w \<le> i ==> length (bv_extend i b w) = i"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   153
  by (simp add: bv_extend_def)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   154
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   155
lemma [simp]: "bv_not [] = []"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   156
  by (simp add: bv_not_def)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   157
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   158
lemma [simp]: "bv_not (b#bs) = (bitnot b) # bv_not bs"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   159
  by (simp add: bv_not_def)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   160
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   161
lemma [simp]: "bv_not (bv_not w) = w"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   162
  by (rule bit_list_induct [of _ w],simp_all)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   163
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   164
lemma [simp]: "bv_msb [] = \<zero>"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   165
  by (simp add: bv_msb_def)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   166
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   167
lemma [simp]: "bv_msb (b#bs) = b"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   168
  by (simp add: bv_msb_def)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   169
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   170
lemma [simp]: "0 < length w ==> bv_msb (bv_not w) = (bitnot (bv_msb w))"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   171
  by (cases w,simp_all)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   172
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   173
lemma [simp,intro]: "bv_msb w = \<one> ==> 0 < length w"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   174
  by (cases w,simp_all)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   175
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   176
lemma [simp]: "length (bv_not w) = length w"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   177
  by (induct w,simp_all)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   178
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   179
constdefs
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   180
  bv_to_nat :: "bit list => int"
15013
34264f5e4691 new treatment of binary numerals
paulson
parents: 14706
diff changeset
   181
  "bv_to_nat bv == number_of (foldl (%bn b. bn BIT (b = \<one>)) Numeral.Pls bv)"
14494
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   182
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   183
lemma [simp]: "bv_to_nat [] = 0"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   184
  by (simp add: bv_to_nat_def)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   185
15013
34264f5e4691 new treatment of binary numerals
paulson
parents: 14706
diff changeset
   186
lemma pos_number_of:
34264f5e4691 new treatment of binary numerals
paulson
parents: 14706
diff changeset
   187
     "number_of (w BIT b) = (2::int) * number_of w + (if b then 1 else 0)"
34264f5e4691 new treatment of binary numerals
paulson
parents: 14706
diff changeset
   188
by (simp add: mult_2) 
14494
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   189
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   190
lemma bv_to_nat_helper [simp]: "bv_to_nat (b # bs) = bitval b * 2 ^ length bs + bv_to_nat bs"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   191
proof -
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   192
  def bv_to_nat' == "%base bv. number_of (foldl (% bn b. bn BIT (b = \<one>)) base bv)::int"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   193
  have bv_to_nat'_def: "!!base bv. bv_to_nat' base bv == number_of (foldl (% bn b. bn BIT (b = \<one>)) base bv)::int"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   194
    by (simp add: bv_to_nat'_def)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   195
  have [rule_format]: "\<forall> base bs. (0::int) \<le> number_of base --> (\<forall> b. bv_to_nat' base (b # bs) = bv_to_nat' (base BIT (b = \<one>)) bs)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   196
    by (simp add: bv_to_nat'_def)
15013
34264f5e4691 new treatment of binary numerals
paulson
parents: 14706
diff changeset
   197
  have helper [rule_format]: "\<forall> base. (0::int) \<le> number_of base --> bv_to_nat' base bs = number_of base * 2 ^ length bs + bv_to_nat' Numeral.Pls bs"
14494
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   198
  proof (induct bs,simp add: bv_to_nat'_def,clarify)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   199
    fix x xs base
15013
34264f5e4691 new treatment of binary numerals
paulson
parents: 14706
diff changeset
   200
    assume ind [rule_format]: "\<forall> base. (0::int) \<le> number_of base --> bv_to_nat' base xs = number_of base * 2 ^ length xs + bv_to_nat' Numeral.Pls xs"
14494
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   201
    assume base_pos: "(0::int) \<le> number_of base"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   202
    def qq == "number_of base::int"
15013
34264f5e4691 new treatment of binary numerals
paulson
parents: 14706
diff changeset
   203
    show "bv_to_nat' base (x # xs) = number_of base * 2 ^ (length (x # xs)) + bv_to_nat' Numeral.Pls (x # xs)"
14494
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   204
      apply (unfold bv_to_nat'_def)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   205
      apply (simp only: foldl.simps)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   206
      apply (fold bv_to_nat'_def)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   207
      apply (subst ind [of "base BIT (x = \<one>)"])
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   208
      using base_pos
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   209
      apply simp
15013
34264f5e4691 new treatment of binary numerals
paulson
parents: 14706
diff changeset
   210
      apply (subst ind [of "Numeral.Pls BIT (x = \<one>)"])
14494
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   211
      apply simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   212
      apply (subst pos_number_of [of "base" "x = \<one>"])
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   213
      using base_pos
15013
34264f5e4691 new treatment of binary numerals
paulson
parents: 14706
diff changeset
   214
      apply (subst pos_number_of [of "Numeral.Pls" "x = \<one>"])
14494
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   215
      apply (fold qq_def)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   216
      apply (simp add: ring_distrib)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   217
      done
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   218
  qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   219
  show ?thesis
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   220
    apply (unfold bv_to_nat_def [of "b # bs"])
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   221
    apply (simp only: foldl.simps)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   222
    apply (fold bv_to_nat'_def)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   223
    apply (subst helper)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   224
    apply simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   225
    apply (cases "b::bit")
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   226
    apply (simp add: bv_to_nat'_def bv_to_nat_def)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   227
    apply (simp add: iszero_def)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   228
    apply (simp add: bv_to_nat'_def bv_to_nat_def)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   229
    done
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   230
qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   231
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   232
lemma bv_to_nat0 [simp]: "bv_to_nat (\<zero>#bs) = bv_to_nat bs"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   233
  by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   234
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   235
lemma bv_to_nat1 [simp]: "bv_to_nat (\<one>#bs) = 2 ^ length bs + bv_to_nat bs"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   236
  by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   237
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   238
lemma bv_to_nat_lower_range [intro,simp]: "0 \<le> bv_to_nat w"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   239
  apply (induct w,simp_all)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   240
  apply (case_tac a,simp_all)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   241
  apply (rule add_increasing)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   242
  apply auto
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   243
  done
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   244
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   245
lemma bv_to_nat_upper_range: "bv_to_nat w < 2 ^ length w"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   246
proof (induct w,simp_all)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   247
  fix b bs
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   248
  assume "bv_to_nat bs < 2 ^ length bs"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   249
  show "bitval b * 2 ^ length bs + bv_to_nat bs < 2 * 2 ^ length bs"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   250
  proof (cases b,simp_all)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   251
    have "bv_to_nat bs < 2 ^ length bs"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   252
      .
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   253
    also have "... < 2 * 2 ^ length bs"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   254
      by auto
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   255
    finally show "bv_to_nat bs < 2 * 2 ^ length bs"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   256
      by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   257
  next
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   258
    have "bv_to_nat bs < 2 ^ length bs"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   259
      .
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   260
    hence "2 ^ length bs + bv_to_nat bs < 2 ^ length bs + 2 ^ length bs"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   261
      by arith
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   262
    also have "... = 2 * (2 ^ length bs)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   263
      by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   264
    finally show "bv_to_nat bs < 2 ^ length bs"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   265
      by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   266
  qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   267
qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   268
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   269
lemma [simp]:
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   270
  assumes wn: "n \<le> length w"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   271
  shows       "bv_extend n b w = w"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   272
  by (simp add: bv_extend_def wn)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   273
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   274
lemma [simp]:
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   275
  assumes wn: "length w < n"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   276
  shows       "bv_extend n b w = bv_extend n b (b#w)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   277
proof -
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   278
  from wn
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   279
  have s: "n - Suc (length w) + 1 = n - length w"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   280
    by arith
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   281
  have "bv_extend n b w = replicate (n - length w) b @ w"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   282
    by (simp add: bv_extend_def)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   283
  also have "... = replicate (n - Suc (length w) + 1) b @ w"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   284
    by (subst s,rule)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   285
  also have "... = (replicate (n - Suc (length w)) b @ replicate 1 b) @ w"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   286
    by (subst replicate_add,rule)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   287
  also have "... = replicate (n - Suc (length w)) b @ b # w"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   288
    by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   289
  also have "... = bv_extend n b (b#w)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   290
    by (simp add: bv_extend_def)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   291
  finally show "bv_extend n b w = bv_extend n b (b#w)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   292
    .
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   293
qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   294
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   295
consts
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   296
  rem_initial :: "bit => bit list => bit list"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   297
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   298
primrec
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   299
  "rem_initial b [] = []"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   300
  "rem_initial b (x#xs) = (if b = x then rem_initial b xs else x#xs)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   301
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   302
lemma rem_initial_length: "length (rem_initial b w) \<le> length w"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   303
  by (rule bit_list_induct [of _ w],simp_all (no_asm),safe,simp_all)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   304
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   305
lemma rem_initial_equal:
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   306
  assumes p: "length (rem_initial b w) = length w"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   307
  shows      "rem_initial b w = w"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   308
proof -
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   309
  have "length (rem_initial b w) = length w --> rem_initial b w = w"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   310
  proof (induct w,simp_all,clarify)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   311
    fix xs
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   312
    assume "length (rem_initial b xs) = length xs --> rem_initial b xs = xs"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   313
    assume f: "length (rem_initial b xs) = Suc (length xs)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   314
    with rem_initial_length [of b xs]
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   315
    show "rem_initial b xs = b#xs"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   316
      by auto
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   317
  qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   318
  thus ?thesis
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   319
    ..
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   320
qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   321
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   322
lemma bv_extend_rem_initial: "bv_extend (length w) b (rem_initial b w) = w"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   323
proof (induct w,simp_all,safe)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   324
  fix xs
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   325
  assume ind: "bv_extend (length xs) b (rem_initial b xs) = xs"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   326
  from rem_initial_length [of b xs]
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   327
  have [simp]: "Suc (length xs) - length (rem_initial b xs) = 1 + (length xs - length (rem_initial b xs))"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   328
    by arith
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   329
  have "bv_extend (Suc (length xs)) b (rem_initial b xs) = replicate (Suc (length xs) - length (rem_initial b xs)) b @ (rem_initial b xs)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   330
    by (simp add: bv_extend_def)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   331
  also have "... = replicate (1 + (length xs - length (rem_initial b xs))) b @ rem_initial b xs"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   332
    by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   333
  also have "... = (replicate 1 b @ replicate (length xs - length (rem_initial b xs)) b) @ rem_initial b xs"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   334
    by (subst replicate_add,rule refl)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   335
  also have "... = b # bv_extend (length xs) b (rem_initial b xs)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   336
    by (auto simp add: bv_extend_def [symmetric])
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   337
  also have "... = b # xs"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   338
    by (simp add: ind)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   339
  finally show "bv_extend (Suc (length xs)) b (rem_initial b xs) = b # xs"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   340
    .
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   341
qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   342
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   343
lemma rem_initial_append1:
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   344
  assumes "rem_initial b xs ~= []"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   345
  shows   "rem_initial b (xs @ ys) = rem_initial b xs @ ys"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   346
proof -
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   347
  have "rem_initial b xs ~= [] --> rem_initial b (xs @ ys) = rem_initial b xs @ ys" (is "?P xs ys")
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   348
    by (induct xs,auto)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   349
  thus ?thesis
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   350
    ..
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   351
qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   352
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   353
lemma rem_initial_append2:
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   354
  assumes "rem_initial b xs = []"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   355
  shows   "rem_initial b (xs @ ys) = rem_initial b ys"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   356
proof -
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   357
  have "rem_initial b xs = [] --> rem_initial b (xs @ ys) = rem_initial b ys" (is "?P xs ys")
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   358
    by (induct xs,auto)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   359
  thus ?thesis
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   360
    ..
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   361
qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   362
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   363
constdefs
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   364
  norm_unsigned :: "bit list => bit list"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   365
  "norm_unsigned == rem_initial \<zero>"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   366
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   367
lemma [simp]: "norm_unsigned [] = []"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   368
  by (simp add: norm_unsigned_def)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   369
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   370
lemma [simp]: "norm_unsigned (\<zero>#bs) = norm_unsigned bs"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   371
  by (simp add: norm_unsigned_def)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   372
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   373
lemma [simp]: "norm_unsigned (\<one>#bs) = \<one>#bs"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   374
  by (simp add: norm_unsigned_def)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   375
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   376
lemma [simp]: "norm_unsigned (norm_unsigned w) = norm_unsigned w"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   377
  by (rule bit_list_induct [of _ w],simp_all)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   378
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   379
consts
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   380
  nat_to_bv_helper :: "int => bit list => bit list"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   381
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   382
recdef nat_to_bv_helper "measure nat"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   383
  "nat_to_bv_helper n = (%bs. (if n \<le> 0 then bs
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   384
                               else nat_to_bv_helper (n div 2) ((if n mod 2 = 0 then \<zero> else \<one>)#bs)))"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   385
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   386
constdefs
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   387
  nat_to_bv :: "int => bit list"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   388
  "nat_to_bv n == nat_to_bv_helper n []"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   389
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   390
lemma nat_to_bv0 [simp]: "nat_to_bv 0 = []"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   391
  by (simp add: nat_to_bv_def)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   392
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   393
lemmas [simp del] = nat_to_bv_helper.simps
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   394
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   395
lemma n_div_2_cases:
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   396
  assumes n0  : "0 \<le> n"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   397
  and     zero: "(n::int) = 0 ==> R"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   398
  and     div : "[| n div 2 < n ; 0 < n |] ==> R"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   399
  shows         "R"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   400
proof (cases "n = 0")
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   401
  assume "n = 0"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   402
  thus R
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   403
    by (rule zero)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   404
next
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   405
  assume "n ~= 0"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   406
  with n0
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   407
  have nn0: "0 < n"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   408
    by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   409
  hence "n div 2 < n"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   410
    by arith
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   411
  from this and nn0
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   412
  show R
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   413
    by (rule div)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   414
qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   415
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   416
lemma int_wf_ge_induct:
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   417
  assumes base:  "P (k::int)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   418
  and     ind :  "!!i. (!!j. [| k \<le> j ; j < i |] ==> P j) ==> P i"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   419
  and     valid: "k \<le> i"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   420
  shows          "P i"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   421
proof -
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   422
  have a: "\<forall> j. k \<le> j \<and> j < i --> P j"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   423
  proof (rule int_ge_induct)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   424
    show "k \<le> i"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   425
      .
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   426
  next
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   427
    show "\<forall> j. k \<le> j \<and> j < k --> P j"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   428
      by auto
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   429
  next
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   430
    fix i
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   431
    assume "k \<le> i"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   432
    assume a: "\<forall> j. k \<le> j \<and> j < i --> P j"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   433
    have pi: "P i"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   434
    proof (rule ind)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   435
      fix j
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   436
      assume "k \<le> j" and "j < i"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   437
      with a
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   438
      show "P j"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   439
	by auto
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   440
    qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   441
    show "\<forall> j. k \<le> j \<and> j < i + 1 --> P j"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   442
    proof auto
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   443
      fix j
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   444
      assume kj: "k \<le> j"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   445
      assume ji: "j \<le> i"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   446
      show "P j"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   447
      proof (cases "j = i")
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   448
	assume "j = i"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   449
	with pi
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   450
	show "P j"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   451
	  by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   452
      next
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   453
	assume "j ~= i"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   454
	with ji
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   455
	have "j < i"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   456
	  by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   457
	with kj and a
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   458
	show "P j"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   459
	  by blast
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   460
      qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   461
    qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   462
  qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   463
  show "P i"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   464
  proof (rule ind)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   465
    fix j
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   466
    assume "k \<le> j" and "j < i"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   467
    with a
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   468
    show "P j"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   469
      by auto
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   470
  qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   471
qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   472
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   473
lemma unfold_nat_to_bv_helper:
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   474
  "0 \<le> b ==> nat_to_bv_helper b l = nat_to_bv_helper b [] @ l"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   475
proof -
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   476
  assume "0 \<le> b"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   477
  have "\<forall>l. nat_to_bv_helper b l = nat_to_bv_helper b [] @ l"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   478
  proof (rule int_wf_ge_induct [where ?i = b])
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   479
    show "0 \<le> b"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   480
      .
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   481
  next
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   482
    show "\<forall> l. nat_to_bv_helper 0 l = nat_to_bv_helper 0 [] @ l"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   483
      by (simp add: nat_to_bv_helper.simps)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   484
  next
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   485
    fix n
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   486
    assume ind: "!!j. [| 0 \<le> j ; j < n |] ==> \<forall> l. nat_to_bv_helper j l = nat_to_bv_helper j [] @ l"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   487
    show "\<forall>l. nat_to_bv_helper n l = nat_to_bv_helper n [] @ l"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   488
    proof
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   489
      fix l
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   490
      show "nat_to_bv_helper n l = nat_to_bv_helper n [] @ l"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   491
      proof (cases "n < 0")
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   492
	assume "n < 0"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   493
	thus ?thesis
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   494
	  by (simp add: nat_to_bv_helper.simps)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   495
      next
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   496
	assume "~n < 0"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   497
	show ?thesis
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   498
	proof (rule n_div_2_cases [of n])
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   499
	  from prems
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   500
	  show "0 \<le> n"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   501
	    by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   502
	next
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   503
	  assume [simp]: "n = 0"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   504
	  show ?thesis
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   505
	    apply (subst nat_to_bv_helper.simps [of n])
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   506
	    apply simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   507
	    done
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   508
	next
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   509
	  assume n2n: "n div 2 < n"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   510
	  assume [simp]: "0 < n"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   511
	  hence n20: "0 \<le> n div 2"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   512
	    by arith
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   513
	  from ind [of "n div 2"] and n2n n20
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   514
	  have ind': "\<forall>l. nat_to_bv_helper (n div 2) l = nat_to_bv_helper (n div 2) [] @ l"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   515
	    by blast
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   516
	  show ?thesis
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   517
	    apply (subst nat_to_bv_helper.simps [of n])
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   518
	    apply simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   519
	    apply (subst spec [OF ind',of "\<zero>#l"])
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   520
	    apply (subst spec [OF ind',of "\<one>#l"])
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   521
	    apply (subst spec [OF ind',of "[\<one>]"])
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   522
	    apply (subst spec [OF ind',of "[\<zero>]"])
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   523
	    apply simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   524
	    done
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   525
	qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   526
      qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   527
    qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   528
  qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   529
  thus ?thesis
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   530
    ..
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   531
qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   532
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   533
lemma nat_to_bv_non0 [simp]: "0 < n ==> nat_to_bv n = nat_to_bv (n div 2) @ [if n mod 2 = 0 then \<zero> else \<one>]"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   534
proof -
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   535
  assume [simp]: "0 < n"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   536
  show ?thesis
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   537
    apply (subst nat_to_bv_def [of n])
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   538
    apply (subst nat_to_bv_helper.simps [of n])
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   539
    apply (subst unfold_nat_to_bv_helper)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   540
    using prems
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   541
    apply arith
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   542
    apply simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   543
    apply (subst nat_to_bv_def [of "n div 2"])
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   544
    apply auto
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   545
    using prems
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   546
    apply auto
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   547
    done
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   548
qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   549
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   550
lemma bv_to_nat_dist_append: "bv_to_nat (l1 @ l2) = bv_to_nat l1 * 2 ^ length l2 + bv_to_nat l2"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   551
proof -
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   552
  have "\<forall>l2. bv_to_nat (l1 @ l2) = bv_to_nat l1 * 2 ^ length l2 + bv_to_nat l2"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   553
  proof (induct l1,simp_all)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   554
    fix x xs
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   555
    assume ind: "\<forall>l2. bv_to_nat (xs @ l2) = bv_to_nat xs * 2 ^ length l2 + bv_to_nat l2"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   556
    show "\<forall>l2. bitval x * 2 ^ (length xs + length l2) + bv_to_nat xs * 2 ^ length l2 = (bitval x * 2 ^ length xs + bv_to_nat xs) * 2 ^ length l2"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   557
    proof
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   558
      fix l2
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   559
      show "bitval x * 2 ^ (length xs + length l2) + bv_to_nat xs * 2 ^ length l2 = (bitval x * 2 ^ length xs + bv_to_nat xs) * 2 ^ length l2"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   560
      proof -
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   561
	have "(2::int) ^ (length xs + length l2) = 2 ^ length xs * 2 ^ length l2"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   562
	  by (induct "length xs",simp_all)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   563
	hence "bitval x * 2 ^ (length xs + length l2) + bv_to_nat xs * 2 ^ length l2 =
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   564
	  bitval x * 2 ^ length xs * 2 ^ length l2 + bv_to_nat xs * 2 ^ length l2"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   565
	  by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   566
	also have "... = (bitval x * 2 ^ length xs + bv_to_nat xs) * 2 ^ length l2"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   567
	  by (simp add: ring_distrib)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   568
	finally show ?thesis .
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   569
      qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   570
    qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   571
  qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   572
  thus ?thesis
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   573
    ..
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   574
qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   575
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   576
lemma bv_nat_bv [simp]:
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   577
  assumes n0: "0 \<le> n"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   578
  shows       "bv_to_nat (nat_to_bv n) = n"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   579
proof -
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   580
  have "0 \<le> n --> bv_to_nat (nat_to_bv n) = n"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   581
  proof (rule int_wf_ge_induct [where ?k = 0],simp_all,clarify)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   582
    fix n
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   583
    assume ind: "!!j. [| 0 \<le> j; j < n |] ==> bv_to_nat (nat_to_bv j) = j"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   584
    assume n0: "0 \<le> n"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   585
    show "bv_to_nat (nat_to_bv n) = n"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   586
    proof (rule n_div_2_cases [of n])
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   587
      show "0 \<le> n"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   588
	.
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   589
    next
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   590
      assume [simp]: "n = 0"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   591
      show ?thesis
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   592
	by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   593
    next
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   594
      assume nn: "n div 2 < n"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   595
      assume n0: "0 < n"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   596
      hence n20: "0 \<le> n div 2"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   597
	by arith
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   598
      from ind and n20 nn
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   599
      have ind': "bv_to_nat (nat_to_bv (n div 2)) = n div 2"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   600
	by blast
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   601
      from n0 have n0': "~ n \<le> 0"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   602
	by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   603
      show ?thesis
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   604
	apply (subst nat_to_bv_def)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   605
	apply (subst nat_to_bv_helper.simps [of n])
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   606
	apply (simp add: n0' split del: split_if)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   607
	apply (subst unfold_nat_to_bv_helper)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   608
	apply (rule n20)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   609
	apply (subst bv_to_nat_dist_append)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   610
	apply (fold nat_to_bv_def)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   611
	apply (simp add: ind' split del: split_if)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   612
	apply (cases "n mod 2 = 0")
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   613
      proof simp_all
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   614
	assume "n mod 2 = 0"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   615
	with zmod_zdiv_equality [of n 2]
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   616
	show "n div 2 * 2 = n"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   617
	  by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   618
      next
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   619
	assume "n mod 2 = 1"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   620
	with zmod_zdiv_equality [of n 2]
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   621
	show "n div 2 * 2 + 1 = n"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   622
	  by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   623
      qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   624
    qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   625
  qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   626
  with n0
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   627
  show ?thesis
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   628
    by auto
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   629
qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   630
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   631
lemma [simp]: "bv_to_nat (norm_unsigned w) = bv_to_nat w"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   632
  by (rule bit_list_induct,simp_all)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   633
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   634
lemma [simp]: "length (norm_unsigned w) \<le> length w"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   635
  by (rule bit_list_induct,simp_all)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   636
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   637
lemma bv_to_nat_rew_msb: "bv_msb w = \<one> ==> bv_to_nat w = 2 ^ (length w - 1) + bv_to_nat (tl w)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   638
  by (rule bit_list_cases [of w],simp_all)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   639
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   640
lemma norm_unsigned_result: "norm_unsigned xs = [] \<or> bv_msb (norm_unsigned xs) = \<one>"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   641
proof (rule length_induct [of _ xs])
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   642
  fix xs :: "bit list"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   643
  assume ind: "\<forall>ys. length ys < length xs --> norm_unsigned ys = [] \<or> bv_msb (norm_unsigned ys) = \<one>"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   644
  show "norm_unsigned xs = [] \<or> bv_msb (norm_unsigned xs) = \<one>"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   645
  proof (rule bit_list_cases [of xs],simp_all)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   646
    fix bs
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   647
    assume [simp]: "xs = \<zero>#bs"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   648
    from ind
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   649
    have "length bs < length xs --> norm_unsigned bs = [] \<or> bv_msb (norm_unsigned bs) = \<one>"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   650
      ..
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   651
    thus "norm_unsigned bs = [] \<or> bv_msb (norm_unsigned bs) = \<one>"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   652
      by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   653
  qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   654
qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   655
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   656
lemma norm_empty_bv_to_nat_zero:
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   657
  assumes nw: "norm_unsigned w = []"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   658
  shows       "bv_to_nat w = 0"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   659
proof -
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   660
  have "bv_to_nat w = bv_to_nat (norm_unsigned w)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   661
    by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   662
  also have "... = bv_to_nat []"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   663
    by (subst nw,rule)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   664
  also have "... = 0"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   665
    by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   666
  finally show ?thesis .
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   667
qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   668
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   669
lemma bv_to_nat_lower_limit:
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   670
  assumes w0: "0 < bv_to_nat w"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   671
  shows         "2 ^ (length (norm_unsigned w) - 1) \<le> bv_to_nat w"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   672
proof -
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   673
  from w0 and norm_unsigned_result [of w]
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   674
  have msbw: "bv_msb (norm_unsigned w) = \<one>"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   675
    by (auto simp add: norm_empty_bv_to_nat_zero)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   676
  have "2 ^ (length (norm_unsigned w) - 1) \<le> bv_to_nat (norm_unsigned w)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   677
    by (subst bv_to_nat_rew_msb [OF msbw],simp)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   678
  thus ?thesis
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   679
    by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   680
qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   681
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   682
lemmas [simp del] = nat_to_bv_non0
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   683
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   684
lemma norm_unsigned_length [intro!]: "length (norm_unsigned w) \<le> length w"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   685
  by (subst norm_unsigned_def,rule rem_initial_length)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   686
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   687
lemma norm_unsigned_equal: "length (norm_unsigned w) = length w ==> norm_unsigned w = w"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   688
  by (simp add: norm_unsigned_def,rule rem_initial_equal)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   689
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   690
lemma bv_extend_norm_unsigned: "bv_extend (length w) \<zero> (norm_unsigned w) = w"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   691
  by (simp add: norm_unsigned_def,rule bv_extend_rem_initial)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   692
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   693
lemma norm_unsigned_append1 [simp]: "norm_unsigned xs \<noteq> [] ==> norm_unsigned (xs @ ys) = norm_unsigned xs @ ys"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   694
  by (simp add: norm_unsigned_def,rule rem_initial_append1)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   695
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   696
lemma norm_unsigned_append2 [simp]: "norm_unsigned xs = [] ==> norm_unsigned (xs @ ys) = norm_unsigned ys"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   697
  by (simp add: norm_unsigned_def,rule rem_initial_append2)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   698
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   699
lemma bv_to_nat_zero_imp_empty:
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   700
  assumes "bv_to_nat w = 0"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   701
  shows   "norm_unsigned w = []"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   702
proof -
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   703
  have "bv_to_nat w = 0 --> norm_unsigned w = []"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   704
    apply (rule bit_list_induct [of _ w],simp_all)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   705
    apply (subgoal_tac "0 < 2 ^ length bs + bv_to_nat bs")
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   706
    apply simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   707
    apply (subgoal_tac "(0::int) < 2 ^ length bs")
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   708
    apply (subgoal_tac "0 \<le> bv_to_nat bs")
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   709
    apply arith
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   710
    apply auto
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   711
    done
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   712
  thus ?thesis
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   713
    ..
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   714
qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   715
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   716
lemma bv_to_nat_nzero_imp_nempty:
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   717
  assumes "bv_to_nat w \<noteq> 0"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   718
  shows   "norm_unsigned w \<noteq> []"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   719
proof -
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   720
  have "bv_to_nat w \<noteq> 0 --> norm_unsigned w \<noteq> []"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   721
    by (rule bit_list_induct [of _ w],simp_all)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   722
  thus ?thesis
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   723
    ..
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   724
qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   725
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   726
lemma nat_helper1:
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   727
  assumes ass: "nat_to_bv (bv_to_nat w) = norm_unsigned w"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   728
  shows        "nat_to_bv (2 * bv_to_nat w + bitval x) = norm_unsigned (w @ [x])"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   729
proof (cases x)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   730
  assume [simp]: "x = \<one>"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   731
  show ?thesis
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   732
    apply (simp add: nat_to_bv_non0)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   733
    apply safe
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   734
  proof -
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   735
    fix q
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   736
    assume "(2 * bv_to_nat w) + 1 = 2 * q"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   737
    hence orig: "(2 * bv_to_nat w + 1) mod 2 = 2 * q mod 2" (is "?lhs = ?rhs")
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   738
      by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   739
    have "?lhs = (1 + 2 * bv_to_nat w) mod 2"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   740
      by (simp add: add_commute)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   741
    also have "... = 1"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   742
      by (simp add: zmod_zadd1_eq)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   743
    finally have eq1: "?lhs = 1" .
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   744
    have "?rhs  = 0"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   745
      by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   746
    with orig and eq1
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   747
    have "(1::int) = 0"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   748
      by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   749
    thus "nat_to_bv ((2 * bv_to_nat w + 1) div 2) @ [\<zero>] = norm_unsigned (w @ [\<one>])"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   750
      by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   751
  next
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   752
    have "nat_to_bv ((2 * bv_to_nat w + 1) div 2) @ [\<one>] = nat_to_bv ((1 + 2 * bv_to_nat w) div 2) @ [\<one>]"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   753
      by (simp add: add_commute)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   754
    also have "... = nat_to_bv (bv_to_nat w) @ [\<one>]"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   755
      by (subst zdiv_zadd1_eq,simp)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   756
    also have "... = norm_unsigned w @ [\<one>]"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   757
      by (subst ass,rule refl)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   758
    also have "... = norm_unsigned (w @ [\<one>])"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   759
      by (cases "norm_unsigned w",simp_all)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   760
    finally show "nat_to_bv ((2 * bv_to_nat w + 1) div 2) @ [\<one>] = norm_unsigned (w @ [\<one>])"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   761
      .
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   762
  qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   763
next
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   764
  assume [simp]: "x = \<zero>"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   765
  show ?thesis
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   766
  proof (cases "bv_to_nat w = 0")
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   767
    assume "bv_to_nat w = 0"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   768
    thus ?thesis
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   769
      by (simp add: bv_to_nat_zero_imp_empty)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   770
  next
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   771
    assume "bv_to_nat w \<noteq> 0"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   772
    thus ?thesis
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   773
      apply simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   774
      apply (subst nat_to_bv_non0)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   775
      apply simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   776
      apply auto
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   777
      apply (cut_tac bv_to_nat_lower_range [of w])
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   778
      apply arith
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   779
      apply (subst ass)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   780
      apply (cases "norm_unsigned w")
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   781
      apply (simp_all add: norm_empty_bv_to_nat_zero)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   782
      done
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   783
  qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   784
qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   785
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   786
lemma nat_helper2: "nat_to_bv (2 ^ length xs + bv_to_nat xs) = \<one> # xs"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   787
proof -
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   788
  have "\<forall>xs. nat_to_bv (2 ^ length (rev xs) + bv_to_nat (rev xs)) = \<one> # (rev xs)" (is "\<forall>xs. ?P xs")
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   789
  proof
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   790
    fix xs
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   791
    show "?P xs"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   792
    proof (rule length_induct [of _ xs])
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   793
      fix xs :: "bit list"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   794
      assume ind: "\<forall>ys. length ys < length xs --> ?P ys"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   795
      show "?P xs"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   796
      proof (cases xs)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   797
	assume [simp]: "xs = []"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   798
	show ?thesis
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   799
	  by (simp add: nat_to_bv_non0)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   800
      next
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   801
	fix y ys
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   802
	assume [simp]: "xs = y # ys"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   803
	show ?thesis
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   804
	  apply simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   805
	  apply (subst bv_to_nat_dist_append)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   806
	  apply simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   807
	proof -
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   808
	  have "nat_to_bv (2 * 2 ^ length ys + (bv_to_nat (rev ys) * 2 + bitval y)) =
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   809
	    nat_to_bv (2 * (2 ^ length ys + bv_to_nat (rev ys)) + bitval y)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   810
	    by (simp add: add_ac mult_ac)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   811
	  also have "... = nat_to_bv (2 * (bv_to_nat (\<one>#rev ys)) + bitval y)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   812
	    by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   813
	  also have "... = norm_unsigned (\<one>#rev ys) @ [y]"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   814
	  proof -
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   815
	    from ind
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   816
	    have "nat_to_bv (2 ^ length (rev ys) + bv_to_nat (rev ys)) = \<one> # rev ys"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   817
	      by auto
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   818
	    hence [simp]: "nat_to_bv (2 ^ length ys + bv_to_nat (rev ys)) = \<one> # rev ys"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   819
	      by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   820
	    show ?thesis
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   821
	      apply (subst nat_helper1)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   822
	      apply simp_all
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   823
	      done
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   824
	  qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   825
	  also have "... = (\<one>#rev ys) @ [y]"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   826
	    by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   827
	  also have "... = \<one> # rev ys @ [y]"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   828
	    by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   829
	  finally show "nat_to_bv (2 * 2 ^ length ys + (bv_to_nat (rev ys) * 2 + bitval y)) = \<one> # rev ys @ [y]"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   830
	    .
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   831
	qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   832
      qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   833
    qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   834
  qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   835
  hence "nat_to_bv (2 ^ length (rev (rev xs)) + bv_to_nat (rev (rev xs))) = \<one> # rev (rev xs)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   836
    ..
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   837
  thus ?thesis
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   838
    by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   839
qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   840
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   841
lemma nat_bv_nat [simp]: "nat_to_bv (bv_to_nat w) = norm_unsigned w"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   842
proof (rule bit_list_induct [of _ w],simp_all)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   843
  fix xs
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   844
  assume "nat_to_bv (bv_to_nat xs) = norm_unsigned xs"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   845
  have "bv_to_nat xs = bv_to_nat (norm_unsigned xs)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   846
    by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   847
  have "bv_to_nat xs < 2 ^ length xs"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   848
    by (rule bv_to_nat_upper_range)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   849
  show "nat_to_bv (2 ^ length xs + bv_to_nat xs) = \<one> # xs"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   850
    by (rule nat_helper2)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   851
qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   852
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   853
lemma [simp]: "bv_to_nat (norm_unsigned xs) = bv_to_nat xs"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   854
  by (rule bit_list_induct [of _ w],simp_all)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   855
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   856
lemma bv_to_nat_qinj:
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   857
  assumes one: "bv_to_nat xs = bv_to_nat ys"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   858
  and     len: "length xs = length ys"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   859
  shows        "xs = ys"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   860
proof -
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   861
  from one
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   862
  have "nat_to_bv (bv_to_nat xs) = nat_to_bv (bv_to_nat ys)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   863
    by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   864
  hence xsys: "norm_unsigned xs = norm_unsigned ys"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   865
    by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   866
  have "xs = bv_extend (length xs) \<zero> (norm_unsigned xs)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   867
    by (simp add: bv_extend_norm_unsigned)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   868
  also have "... = bv_extend (length ys) \<zero> (norm_unsigned ys)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   869
    by (simp add: xsys len)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   870
  also have "... = ys"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   871
    by (simp add: bv_extend_norm_unsigned)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   872
  finally show ?thesis .
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   873
qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   874
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   875
lemma norm_unsigned_nat_to_bv [simp]:
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   876
  assumes [simp]: "0 \<le> n"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   877
  shows "norm_unsigned (nat_to_bv n) = nat_to_bv n"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   878
proof -
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   879
  have "norm_unsigned (nat_to_bv n) = nat_to_bv (bv_to_nat (norm_unsigned (nat_to_bv n)))"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   880
    by (subst nat_bv_nat,simp)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   881
  also have "... = nat_to_bv n"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   882
    by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   883
  finally show ?thesis .
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   884
qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   885
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   886
lemma length_nat_to_bv_upper_limit:
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   887
  assumes nk: "n \<le> 2 ^ k - 1"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   888
  shows       "length (nat_to_bv n) \<le> k"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   889
proof (cases "n \<le> 0")
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   890
  assume "n \<le> 0"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   891
  thus ?thesis
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   892
    by (simp add: nat_to_bv_def nat_to_bv_helper.simps)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   893
next
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   894
  assume "~ n \<le> 0"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   895
  hence n0: "0 < n"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   896
    by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   897
  hence n00: "0 \<le> n"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   898
    by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   899
  show ?thesis
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   900
  proof (rule ccontr)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   901
    assume "~ length (nat_to_bv n) \<le> k"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   902
    hence "k < length (nat_to_bv n)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   903
      by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   904
    hence "k \<le> length (nat_to_bv n) - 1"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   905
      by arith
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   906
    hence "(2::int) ^ k \<le> 2 ^ (length (nat_to_bv n) - 1)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   907
      by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   908
    also have "... = 2 ^ (length (norm_unsigned (nat_to_bv n)) - 1)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   909
      by (simp add: n00)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   910
    also have "... \<le> bv_to_nat (nat_to_bv n)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   911
      by (rule bv_to_nat_lower_limit,simp add: n00 n0)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   912
    also have "... = n"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   913
      by (simp add: n00)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   914
    finally have "2 ^ k \<le> n" .
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   915
    with n0
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   916
    have "2 ^ k - 1 < n"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   917
      by arith
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   918
    with nk
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   919
    show False
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   920
      by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   921
  qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   922
qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   923
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   924
lemma length_nat_to_bv_lower_limit:
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   925
  assumes nk: "2 ^ k \<le> n"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   926
  shows       "k < length (nat_to_bv n)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   927
proof (rule ccontr)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   928
  have "(0::int) \<le> 2 ^ k"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   929
    by auto
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   930
  with nk
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   931
  have [simp]: "0 \<le> n"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   932
    by auto
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   933
  assume "~ k < length (nat_to_bv n)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   934
  hence lnk: "length (nat_to_bv n) \<le> k"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   935
    by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   936
  have "n = bv_to_nat (nat_to_bv n)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   937
    by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   938
  also have "... < 2 ^ length (nat_to_bv n)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   939
    by (rule bv_to_nat_upper_range)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   940
  also from lnk have "... \<le> 2 ^ k"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   941
    by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   942
  finally have "n < 2 ^ k" .
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   943
  with nk
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   944
  show False
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   945
    by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   946
qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   947
14589
feae7b5fd425 tuned document;
wenzelm
parents: 14565
diff changeset
   948
subsection {* Unsigned Arithmetic Operations *}
14494
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   949
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   950
constdefs
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   951
  bv_add :: "[bit list, bit list ] => bit list"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   952
  "bv_add w1 w2 == nat_to_bv (bv_to_nat w1 + bv_to_nat w2)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   953
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   954
lemma [simp]: "bv_add (norm_unsigned w1) w2 = bv_add w1 w2"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   955
  by (simp add: bv_add_def)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   956
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   957
lemma [simp]: "bv_add w1 (norm_unsigned w2) = bv_add w1 w2"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   958
  by (simp add: bv_add_def)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   959
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   960
lemma [simp]: "norm_unsigned (bv_add w1 w2) = bv_add w1 w2"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   961
  apply (simp add: bv_add_def)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   962
  apply (rule norm_unsigned_nat_to_bv)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   963
  apply (subgoal_tac "0 \<le> bv_to_nat w1")
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   964
  apply (subgoal_tac "0 \<le> bv_to_nat w2")
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   965
  apply arith
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   966
  apply simp_all
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   967
  done
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   968
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   969
lemma bv_add_length: "length (bv_add w1 w2) \<le> Suc (max (length w1) (length w2))"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   970
proof (unfold bv_add_def,rule length_nat_to_bv_upper_limit)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   971
  from bv_to_nat_upper_range [of w1] and bv_to_nat_upper_range [of w2]
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   972
  have "bv_to_nat w1 + bv_to_nat w2 \<le> (2 ^ length w1 - 1) + (2 ^ length w2 - 1)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   973
    by arith
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   974
  also have "... \<le> max (2 ^ length w1 - 1) (2 ^ length w2 - 1) + max (2 ^ length w1 - 1) (2 ^ length w2 - 1)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   975
    by (rule add_mono,safe intro!: le_maxI1 le_maxI2)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   976
  also have "... = 2 * max (2 ^ length w1 - 1) (2 ^ length w2 - 1)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   977
    by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   978
  also have "... \<le> 2 ^ Suc (max (length w1) (length w2)) - 2"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   979
  proof (cases "length w1 \<le> length w2")
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   980
    assume [simp]: "length w1 \<le> length w2"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   981
    hence "(2::int) ^ length w1 \<le> 2 ^ length w2"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   982
      by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   983
    hence [simp]: "(2::int) ^ length w1 - 1 \<le> 2 ^ length w2 - 1"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   984
      by arith
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   985
    show ?thesis
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   986
      by (simp split: split_max)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   987
  next
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   988
    assume [simp]: "~ (length w1 \<le> length w2)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   989
    have "~ ((2::int) ^ length w1 - 1 \<le> 2 ^ length w2 - 1)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   990
    proof
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   991
      assume "(2::int) ^ length w1 - 1 \<le> 2 ^ length w2 - 1"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   992
      hence "((2::int) ^ length w1 - 1) + 1 \<le> (2 ^ length w2 - 1) + 1"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   993
	by (rule add_right_mono)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   994
      hence "(2::int) ^ length w1 \<le> 2 ^ length w2"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   995
	by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   996
      hence "length w1 \<le> length w2"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   997
	by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   998
      thus False
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
   999
	by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1000
    qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1001
    thus ?thesis
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1002
      by (simp split: split_max)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1003
  qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1004
  finally show "bv_to_nat w1 + bv_to_nat w2 \<le> 2 ^ Suc (max (length w1) (length w2)) - 1"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1005
    by arith
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1006
qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1007
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1008
constdefs
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1009
  bv_mult :: "[bit list, bit list ] => bit list"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1010
  "bv_mult w1 w2 == nat_to_bv (bv_to_nat w1 * bv_to_nat w2)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1011
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1012
lemma [simp]: "bv_mult (norm_unsigned w1) w2 = bv_mult w1 w2"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1013
  by (simp add: bv_mult_def)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1014
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1015
lemma [simp]: "bv_mult w1 (norm_unsigned w2) = bv_mult w1 w2"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1016
  by (simp add: bv_mult_def)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1017
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1018
lemma [simp]: "norm_unsigned (bv_mult w1 w2) = bv_mult w1 w2"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1019
  apply (simp add: bv_mult_def)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1020
  apply (rule norm_unsigned_nat_to_bv)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1021
  apply (subgoal_tac "0 * 0 \<le> bv_to_nat w1 * bv_to_nat w2")
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1022
  apply simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1023
  apply (rule mult_mono,simp_all)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1024
  done
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1025
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1026
lemma bv_mult_length: "length (bv_mult w1 w2) \<le> length w1 + length w2"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1027
proof (unfold bv_mult_def,rule length_nat_to_bv_upper_limit)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1028
  from bv_to_nat_upper_range [of w1] and bv_to_nat_upper_range [of w2]
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1029
  have h: "bv_to_nat w1 \<le> 2 ^ length w1 - 1 \<and> bv_to_nat w2 \<le> 2 ^ length w2 - 1"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1030
    by arith
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1031
  have "bv_to_nat w1 * bv_to_nat w2 \<le> (2 ^ length w1 - 1) * (2 ^ length w2 - 1)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1032
    apply (cut_tac h)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1033
    apply (rule mult_mono)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1034
    apply auto
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1035
    done
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1036
  also have "... < 2 ^ length w1 * 2 ^ length w2"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1037
    by (rule mult_strict_mono,auto)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1038
  also have "... = 2 ^ (length w1 + length w2)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1039
    by (simp add: power_add)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1040
  finally show "bv_to_nat w1 * bv_to_nat w2 \<le> 2 ^ (length w1 + length w2) - 1"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1041
    by arith
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1042
qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1043
14589
feae7b5fd425 tuned document;
wenzelm
parents: 14565
diff changeset
  1044
subsection {* Signed Vectors *}
14494
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1045
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1046
consts
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1047
  norm_signed :: "bit list => bit list"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1048
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1049
primrec
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1050
  norm_signed_Nil: "norm_signed [] = []"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1051
  norm_signed_Cons: "norm_signed (b#bs) = (case b of \<zero> => if norm_unsigned bs = [] then [] else b#norm_unsigned bs | \<one> => b#rem_initial b bs)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1052
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1053
lemma [simp]: "norm_signed [\<zero>] = []"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1054
  by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1055
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1056
lemma [simp]: "norm_signed [\<one>] = [\<one>]"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1057
  by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1058
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1059
lemma [simp]: "norm_signed (\<zero>#\<one>#xs) = \<zero>#\<one>#xs"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1060
  by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1061
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1062
lemma [simp]: "norm_signed (\<zero>#\<zero>#xs) = norm_signed (\<zero>#xs)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1063
  by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1064
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1065
lemma [simp]: "norm_signed (\<one>#\<zero>#xs) = \<one>#\<zero>#xs"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1066
  by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1067
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1068
lemma [simp]: "norm_signed (\<one>#\<one>#xs) = norm_signed (\<one>#xs)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1069
  by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1070
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1071
lemmas [simp del] = norm_signed_Cons
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1072
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1073
constdefs
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1074
  int_to_bv :: "int => bit list"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1075
  "int_to_bv n == if 0 \<le> n
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1076
                 then norm_signed (\<zero>#nat_to_bv n)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1077
                 else norm_signed (bv_not (\<zero>#nat_to_bv (-n- 1)))"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1078
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1079
lemma int_to_bv_ge0 [simp]: "0 \<le> n ==> int_to_bv n = norm_signed (\<zero> # nat_to_bv n)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1080
  by (simp add: int_to_bv_def)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1081
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1082
lemma int_to_bv_lt0 [simp]: "n < 0 ==> int_to_bv n = norm_signed (bv_not (\<zero>#nat_to_bv (-n- 1)))"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1083
  by (simp add: int_to_bv_def)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1084
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1085
lemma [simp]: "norm_signed (norm_signed w) = norm_signed w"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1086
proof (rule bit_list_induct [of _ w],simp_all)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1087
  fix xs
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1088
  assume "norm_signed (norm_signed xs) = norm_signed xs"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1089
  show "norm_signed (norm_signed (\<zero>#xs)) = norm_signed (\<zero>#xs)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1090
  proof (rule bit_list_cases [of xs],simp_all)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1091
    fix ys
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1092
    assume [symmetric,simp]: "xs = \<zero>#ys"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1093
    show "norm_signed (norm_signed (\<zero>#ys)) = norm_signed (\<zero>#ys)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1094
      by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1095
  qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1096
next
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1097
  fix xs
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1098
  assume "norm_signed (norm_signed xs) = norm_signed xs"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1099
  show "norm_signed (norm_signed (\<one>#xs)) = norm_signed (\<one>#xs)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1100
  proof (rule bit_list_cases [of xs],simp_all)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1101
    fix ys
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1102
    assume [symmetric,simp]: "xs = \<one>#ys"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1103
    show "norm_signed (norm_signed (\<one>#ys)) = norm_signed (\<one>#ys)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1104
      by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1105
  qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1106
qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1107
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1108
constdefs
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1109
  bv_to_int :: "bit list => int"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1110
  "bv_to_int w == case bv_msb w of \<zero> => bv_to_nat w | \<one> => -(bv_to_nat (bv_not w) + 1)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1111
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1112
lemma [simp]: "bv_to_int [] = 0"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1113
  by (simp add: bv_to_int_def)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1114
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1115
lemma [simp]: "bv_to_int (\<zero>#bs) = bv_to_nat bs"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1116
  by (simp add: bv_to_int_def)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1117
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1118
lemma [simp]: "bv_to_int (\<one>#bs) = -(bv_to_nat (bv_not bs) + 1)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1119
  by (simp add: bv_to_int_def)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1120
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1121
lemma [simp]: "bv_to_int (norm_signed w) = bv_to_int w"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1122
proof (rule bit_list_induct [of _ w],simp_all)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1123
  fix xs
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1124
  assume ind: "bv_to_int (norm_signed xs) = bv_to_int xs"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1125
  show "bv_to_int (norm_signed (\<zero>#xs)) = bv_to_nat xs"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1126
  proof (rule bit_list_cases [of xs],simp_all)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1127
    fix ys
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1128
    assume [simp]: "xs = \<zero>#ys"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1129
    from ind
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1130
    show "bv_to_int (norm_signed (\<zero>#ys)) = bv_to_nat ys"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1131
      by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1132
  qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1133
next
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1134
  fix xs
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1135
  assume ind: "bv_to_int (norm_signed xs) = bv_to_int xs"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1136
  show "bv_to_int (norm_signed (\<one>#xs)) = - bv_to_nat (bv_not xs) + -1"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1137
  proof (rule bit_list_cases [of xs],simp_all)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1138
    fix ys
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1139
    assume [simp]: "xs = \<one>#ys"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1140
    from ind
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1141
    show "bv_to_int (norm_signed (\<one>#ys)) = - bv_to_nat (bv_not ys) + -1"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1142
      by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1143
  qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1144
qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1145
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1146
lemma bv_to_int_upper_range: "bv_to_int w < 2 ^ (length w - 1)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1147
proof (rule bit_list_cases [of w],simp_all)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1148
  fix bs
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1149
  show "bv_to_nat bs < 2 ^ length bs"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1150
    by (rule bv_to_nat_upper_range)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1151
next
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1152
  fix bs
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1153
  have "- (bv_to_nat (bv_not bs)) + -1 \<le> 0 + 0"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1154
    by (rule add_mono,simp_all)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1155
  also have "... < 2 ^ length bs"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1156
    by (induct bs,simp_all)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1157
  finally show "- (bv_to_nat (bv_not bs)) + -1 < 2 ^ length bs"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1158
    .
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1159
qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1160
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1161
lemma bv_to_int_lower_range: "- (2 ^ (length w - 1)) \<le> bv_to_int w"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1162
proof (rule bit_list_cases [of w],simp_all)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1163
  fix bs :: "bit list"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1164
  have "- (2 ^ length bs) \<le> (0::int)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1165
    by (induct bs,simp_all)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1166
  also have "... \<le> bv_to_nat bs"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1167
    by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1168
  finally show "- (2 ^ length bs) \<le> bv_to_nat bs"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1169
    .
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1170
next
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1171
  fix bs
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1172
  from bv_to_nat_upper_range [of "bv_not bs"]
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1173
  have "bv_to_nat (bv_not bs) < 2 ^ length bs"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1174
    by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1175
  hence "bv_to_nat (bv_not bs) + 1 \<le> 2 ^ length bs"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1176
    by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1177
  thus "- (2 ^ length bs) \<le> - bv_to_nat (bv_not bs) + -1"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1178
    by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1179
qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1180
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1181
lemma int_bv_int [simp]: "int_to_bv (bv_to_int w) = norm_signed w"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1182
proof (rule bit_list_cases [of w],simp)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1183
  fix xs
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1184
  assume [simp]: "w = \<zero>#xs"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1185
  show ?thesis
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1186
    apply simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1187
    apply (subst norm_signed_Cons [of "\<zero>" "xs"])
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1188
    apply simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1189
    using norm_unsigned_result [of xs]
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1190
    apply safe
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1191
    apply (rule bit_list_cases [of "norm_unsigned xs"])
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1192
    apply simp_all
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1193
    done
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1194
next
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1195
  fix xs
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1196
  assume [simp]: "w = \<one>#xs"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1197
  show ?thesis
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1198
    apply simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1199
    apply (rule bit_list_induct [of _ xs])
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1200
    apply simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1201
    apply (subst int_to_bv_lt0)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1202
    apply (subgoal_tac "- bv_to_nat (bv_not (\<zero> # bs)) + -1 < 0 + 0")
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1203
    apply simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1204
    apply (rule add_le_less_mono)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1205
    apply simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1206
    apply (rule order_trans [of _ 0])
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1207
    apply simp
15067
02be3516e90b removed some obsolete proofs
paulson
parents: 15013
diff changeset
  1208
    apply (rule zero_le_power,simp)
14494
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1209
    apply simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1210
    apply simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1211
    apply (simp del: bv_to_nat1 bv_to_nat_helper)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1212
    apply simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1213
    done
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1214
qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1215
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1216
lemma bv_int_bv [simp]: "bv_to_int (int_to_bv i) = i"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1217
  by (cases "0 \<le> i",simp_all)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1218
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1219
lemma bv_msb_norm [simp]: "bv_msb (norm_signed w) = bv_msb w"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1220
  by (rule bit_list_cases [of w],simp_all add: norm_signed_Cons)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1221
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1222
lemma norm_signed_length: "length (norm_signed w) \<le> length w"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1223
  apply (cases w,simp_all)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1224
  apply (subst norm_signed_Cons)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1225
  apply (case_tac "a",simp_all)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1226
  apply (rule rem_initial_length)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1227
  done
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1228
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1229
lemma norm_signed_equal: "length (norm_signed w) = length w ==> norm_signed w = w"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1230
proof (rule bit_list_cases [of w],simp_all)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1231
  fix xs
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1232
  assume "length (norm_signed (\<zero>#xs)) = Suc (length xs)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1233
  thus "norm_signed (\<zero>#xs) = \<zero>#xs"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1234
    apply (simp add: norm_signed_Cons)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1235
    apply safe
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1236
    apply simp_all
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1237
    apply (rule norm_unsigned_equal)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1238
    apply assumption
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1239
    done
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1240
next
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1241
  fix xs
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1242
  assume "length (norm_signed (\<one>#xs)) = Suc (length xs)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1243
  thus "norm_signed (\<one>#xs) = \<one>#xs"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1244
    apply (simp add: norm_signed_Cons)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1245
    apply (rule rem_initial_equal)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1246
    apply assumption
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1247
    done
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1248
qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1249
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1250
lemma bv_extend_norm_signed: "bv_msb w = b ==> bv_extend (length w) b (norm_signed w) = w"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1251
proof (rule bit_list_cases [of w],simp_all)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1252
  fix xs
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1253
  show "bv_extend (Suc (length xs)) \<zero> (norm_signed (\<zero>#xs)) = \<zero>#xs"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1254
  proof (simp add: norm_signed_list_def,auto)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1255
    assume "norm_unsigned xs = []"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1256
    hence xx: "rem_initial \<zero> xs = []"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1257
      by (simp add: norm_unsigned_def)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1258
    have "bv_extend (Suc (length xs)) \<zero> (\<zero>#rem_initial \<zero> xs) = \<zero>#xs"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1259
      apply (simp add: bv_extend_def replicate_app_Cons_same)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1260
      apply (fold bv_extend_def)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1261
      apply (rule bv_extend_rem_initial)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1262
      done
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1263
    thus "bv_extend (Suc (length xs)) \<zero> [\<zero>] = \<zero>#xs"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1264
      by (simp add: xx)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1265
  next
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1266
    show "bv_extend (Suc (length xs)) \<zero> (\<zero>#norm_unsigned xs) = \<zero>#xs"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1267
      apply (simp add: norm_unsigned_def)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1268
      apply (simp add: bv_extend_def replicate_app_Cons_same)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1269
      apply (fold bv_extend_def)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1270
      apply (rule bv_extend_rem_initial)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1271
      done
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1272
  qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1273
next
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1274
  fix xs
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1275
  show "bv_extend (Suc (length xs)) \<one> (norm_signed (\<one>#xs)) = \<one>#xs"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1276
    apply (simp add: norm_signed_Cons)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1277
    apply (simp add: bv_extend_def replicate_app_Cons_same)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1278
    apply (fold bv_extend_def)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1279
    apply (rule bv_extend_rem_initial)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1280
    done
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1281
qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1282
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1283
lemma bv_to_int_qinj:
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1284
  assumes one: "bv_to_int xs = bv_to_int ys"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1285
  and     len: "length xs = length ys"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1286
  shows        "xs = ys"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1287
proof -
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1288
  from one
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1289
  have "int_to_bv (bv_to_int xs) = int_to_bv (bv_to_int ys)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1290
    by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1291
  hence xsys: "norm_signed xs = norm_signed ys"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1292
    by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1293
  hence xsys': "bv_msb xs = bv_msb ys"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1294
  proof -
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1295
    have "bv_msb xs = bv_msb (norm_signed xs)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1296
      by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1297
    also have "... = bv_msb (norm_signed ys)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1298
      by (simp add: xsys)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1299
    also have "... = bv_msb ys"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1300
      by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1301
    finally show ?thesis .
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1302
  qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1303
  have "xs = bv_extend (length xs) (bv_msb xs) (norm_signed xs)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1304
    by (simp add: bv_extend_norm_signed)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1305
  also have "... = bv_extend (length ys) (bv_msb ys) (norm_signed ys)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1306
    by (simp add: xsys xsys' len)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1307
  also have "... = ys"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1308
    by (simp add: bv_extend_norm_signed)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1309
  finally show ?thesis .
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1310
qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1311
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1312
lemma [simp]: "norm_signed (int_to_bv w) = int_to_bv w"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1313
  by (simp add: int_to_bv_def)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1314
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1315
lemma bv_to_int_msb0: "0 \<le> bv_to_int w1 ==> bv_msb w1 = \<zero>"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1316
  apply (rule bit_list_cases,simp_all)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1317
  apply (subgoal_tac "0 \<le> bv_to_nat (bv_not bs)")
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1318
  apply simp_all
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1319
  done
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1320
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1321
lemma bv_to_int_msb1: "bv_to_int w1 < 0 ==> bv_msb w1 = \<one>"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1322
  apply (rule bit_list_cases,simp_all)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1323
  apply (subgoal_tac "0 \<le> bv_to_nat bs")
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1324
  apply simp_all
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1325
  done
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1326
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1327
lemma bv_to_int_lower_limit_gt0:
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1328
  assumes w0: "0 < bv_to_int w"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1329
  shows       "2 ^ (length (norm_signed w) - 2) \<le> bv_to_int w"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1330
proof -
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1331
  from w0
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1332
  have "0 \<le> bv_to_int w"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1333
    by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1334
  hence [simp]: "bv_msb w = \<zero>"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1335
    by (rule bv_to_int_msb0)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1336
  have "2 ^ (length (norm_signed w) - 2) \<le> bv_to_int (norm_signed w)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1337
  proof (rule bit_list_cases [of w])
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1338
    assume "w = []"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1339
    with w0
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1340
    show ?thesis
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1341
      by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1342
  next
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1343
    fix w'
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1344
    assume weq: "w = \<zero> # w'"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1345
    thus ?thesis
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1346
    proof (simp add: norm_signed_Cons,safe)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1347
      assume "norm_unsigned w' = []"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1348
      with weq and w0
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1349
      show False
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1350
	by (simp add: norm_empty_bv_to_nat_zero)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1351
    next
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1352
      assume w'0: "norm_unsigned w' \<noteq> []"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1353
      have "0 < bv_to_nat w'"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1354
      proof (rule ccontr)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1355
	assume "~ (0 < bv_to_nat w')"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1356
	with bv_to_nat_lower_range [of w']
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1357
	have "bv_to_nat w' = 0"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1358
	  by arith
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1359
	hence "norm_unsigned w' = []"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1360
	  by (simp add: bv_to_nat_zero_imp_empty)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1361
	with w'0
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1362
	show False
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1363
	  by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1364
      qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1365
      with bv_to_nat_lower_limit [of w']
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1366
      have "2 ^ (length (norm_unsigned w') - 1) \<le> bv_to_nat w'"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1367
	.
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1368
      thus "2 ^ (length (norm_unsigned w') - Suc 0) \<le> bv_to_nat w'"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1369
	by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1370
    qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1371
  next
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1372
    fix w'
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1373
    assume "w = \<one> # w'"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1374
    from w0
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1375
    have "bv_msb w = \<zero>"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1376
      by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1377
    with prems
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1378
    show ?thesis
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1379
      by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1380
  qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1381
  also have "...  = bv_to_int w"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1382
    by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1383
  finally show ?thesis .
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1384
qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1385
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1386
lemma norm_signed_result: "norm_signed w = [] \<or> norm_signed w = [\<one>] \<or> bv_msb (norm_signed w) \<noteq> bv_msb (tl (norm_signed w))"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1387
  apply (rule bit_list_cases [of w],simp_all)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1388
  apply (case_tac "bs",simp_all)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1389
  apply (case_tac "a",simp_all)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1390
  apply (simp add: norm_signed_Cons)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1391
  apply safe
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1392
  apply simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1393
proof -
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1394
  fix l
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1395
  assume msb: "\<zero> = bv_msb (norm_unsigned l)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1396
  assume "norm_unsigned l \<noteq> []"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1397
  with norm_unsigned_result [of l]
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1398
  have "bv_msb (norm_unsigned l) = \<one>"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1399
    by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1400
  with msb
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1401
  show False
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1402
    by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1403
next
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1404
  fix xs
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1405
  assume p: "\<one> = bv_msb (tl (norm_signed (\<one> # xs)))"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1406
  have "\<one> \<noteq> bv_msb (tl (norm_signed (\<one> # xs)))"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1407
    by (rule bit_list_induct [of _ xs],simp_all)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1408
  with p
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1409
  show False
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1410
    by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1411
qed
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1412
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1413
lemma bv_to_int_upper_limit_lem1:
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1414
  assumes w0: "bv_to_int w < -1"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1415
  shows       "bv_to_int w < - (2 ^ (length (norm_signed w) - 2))"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1416
proof -
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1417
  from w0
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1418
  have "bv_to_int w < 0"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1419
    by simp
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1420
  hence msbw [simp]: "bv_msb w = \<one>"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1421
    by (rule bv_to_int_msb1)
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1422
  have "bv_to_int w = bv_to_int (norm_signed w)"
48ae8d678d88 Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
skalberg
parents:
diff changeset
  1423
    by simp