src/HOL/Word/Bool_List_Representation.thy
author huffman
Fri, 24 Feb 2012 16:59:20 +0100
changeset 46655 be76913ec1a4
parent 46653 a557db8f2fbf
child 47108 2a1953f0d20d
permissions -rw-r--r--
avoid using Int.succ_def in proofs
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
     1
(* 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
     2
  Author: Jeremy Dawson, NICTA
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
     3
44939
5930d35c976d removed unused legacy lemma names, some comment cleanup.
kleing
parents: 41842
diff changeset
     4
  Theorems to do with integers, expressed using Pls, Min, BIT,
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
     5
  theorems linking them to lists of booleans, and repeated splitting 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
     6
  and concatenation.
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
     7
*) 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
     8
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
     9
header "Bool lists and integers"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    10
37658
df789294c77a more speaking names
haftmann
parents: 37657
diff changeset
    11
theory Bool_List_Representation
df789294c77a more speaking names
haftmann
parents: 37657
diff changeset
    12
imports Bit_Int
26557
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
    13
begin
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    14
37657
17e1085d07b2 moved specific operations here
haftmann
parents: 37654
diff changeset
    15
subsection {* Operations on lists of booleans *}
17e1085d07b2 moved specific operations here
haftmann
parents: 37654
diff changeset
    16
17e1085d07b2 moved specific operations here
haftmann
parents: 37654
diff changeset
    17
primrec bl_to_bin_aux :: "bool list \<Rightarrow> int \<Rightarrow> int" where
17e1085d07b2 moved specific operations here
haftmann
parents: 37654
diff changeset
    18
  Nil: "bl_to_bin_aux [] w = w"
17e1085d07b2 moved specific operations here
haftmann
parents: 37654
diff changeset
    19
  | Cons: "bl_to_bin_aux (b # bs) w = 
17e1085d07b2 moved specific operations here
haftmann
parents: 37654
diff changeset
    20
      bl_to_bin_aux bs (w BIT (if b then 1 else 0))"
17e1085d07b2 moved specific operations here
haftmann
parents: 37654
diff changeset
    21
17e1085d07b2 moved specific operations here
haftmann
parents: 37654
diff changeset
    22
definition bl_to_bin :: "bool list \<Rightarrow> int" where
46001
0b562d564d5f redefine some binary operations on integers work on abstract numerals instead of Int.Pls and Int.Min
huffman
parents: 45997
diff changeset
    23
  bl_to_bin_def: "bl_to_bin bs = bl_to_bin_aux bs 0"
37667
41acc0fa6b6c avoid bitstrings in generated code
haftmann
parents: 37658
diff changeset
    24
37657
17e1085d07b2 moved specific operations here
haftmann
parents: 37654
diff changeset
    25
primrec bin_to_bl_aux :: "nat \<Rightarrow> int \<Rightarrow> bool list \<Rightarrow> bool list" where
17e1085d07b2 moved specific operations here
haftmann
parents: 37654
diff changeset
    26
  Z: "bin_to_bl_aux 0 w bl = bl"
17e1085d07b2 moved specific operations here
haftmann
parents: 37654
diff changeset
    27
  | Suc: "bin_to_bl_aux (Suc n) w bl =
17e1085d07b2 moved specific operations here
haftmann
parents: 37654
diff changeset
    28
      bin_to_bl_aux n (bin_rest w) ((bin_last w = 1) # bl)"
17e1085d07b2 moved specific operations here
haftmann
parents: 37654
diff changeset
    29
17e1085d07b2 moved specific operations here
haftmann
parents: 37654
diff changeset
    30
definition bin_to_bl :: "nat \<Rightarrow> int \<Rightarrow> bool list" where
17e1085d07b2 moved specific operations here
haftmann
parents: 37654
diff changeset
    31
  bin_to_bl_def : "bin_to_bl n w = bin_to_bl_aux n w []"
17e1085d07b2 moved specific operations here
haftmann
parents: 37654
diff changeset
    32
17e1085d07b2 moved specific operations here
haftmann
parents: 37654
diff changeset
    33
primrec bl_of_nth :: "nat \<Rightarrow> (nat \<Rightarrow> bool) \<Rightarrow> bool list" where
17e1085d07b2 moved specific operations here
haftmann
parents: 37654
diff changeset
    34
  Suc: "bl_of_nth (Suc n) f = f n # bl_of_nth n f"
17e1085d07b2 moved specific operations here
haftmann
parents: 37654
diff changeset
    35
  | Z: "bl_of_nth 0 f = []"
17e1085d07b2 moved specific operations here
haftmann
parents: 37654
diff changeset
    36
17e1085d07b2 moved specific operations here
haftmann
parents: 37654
diff changeset
    37
primrec takefill :: "'a \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
17e1085d07b2 moved specific operations here
haftmann
parents: 37654
diff changeset
    38
  Z: "takefill fill 0 xs = []"
17e1085d07b2 moved specific operations here
haftmann
parents: 37654
diff changeset
    39
  | Suc: "takefill fill (Suc n) xs = (
17e1085d07b2 moved specific operations here
haftmann
parents: 37654
diff changeset
    40
      case xs of [] => fill # takefill fill n xs
17e1085d07b2 moved specific operations here
haftmann
parents: 37654
diff changeset
    41
        | y # ys => y # takefill fill n ys)"
17e1085d07b2 moved specific operations here
haftmann
parents: 37654
diff changeset
    42
17e1085d07b2 moved specific operations here
haftmann
parents: 37654
diff changeset
    43
definition map2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list" where
17e1085d07b2 moved specific operations here
haftmann
parents: 37654
diff changeset
    44
  "map2 f as bs = map (split f) (zip as bs)"
17e1085d07b2 moved specific operations here
haftmann
parents: 37654
diff changeset
    45
17e1085d07b2 moved specific operations here
haftmann
parents: 37654
diff changeset
    46
lemma map2_Nil [simp]: "map2 f [] ys = []"
17e1085d07b2 moved specific operations here
haftmann
parents: 37654
diff changeset
    47
  unfolding map2_def by auto
17e1085d07b2 moved specific operations here
haftmann
parents: 37654
diff changeset
    48
17e1085d07b2 moved specific operations here
haftmann
parents: 37654
diff changeset
    49
lemma map2_Nil2 [simp]: "map2 f xs [] = []"
17e1085d07b2 moved specific operations here
haftmann
parents: 37654
diff changeset
    50
  unfolding map2_def by auto
17e1085d07b2 moved specific operations here
haftmann
parents: 37654
diff changeset
    51
17e1085d07b2 moved specific operations here
haftmann
parents: 37654
diff changeset
    52
lemma map2_Cons [simp]:
17e1085d07b2 moved specific operations here
haftmann
parents: 37654
diff changeset
    53
  "map2 f (x # xs) (y # ys) = f x y # map2 f xs ys"
17e1085d07b2 moved specific operations here
haftmann
parents: 37654
diff changeset
    54
  unfolding map2_def by auto
17e1085d07b2 moved specific operations here
haftmann
parents: 37654
diff changeset
    55
17e1085d07b2 moved specific operations here
haftmann
parents: 37654
diff changeset
    56
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
    57
subsection "Arithmetic in terms of bool lists"
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
    58
44939
5930d35c976d removed unused legacy lemma names, some comment cleanup.
kleing
parents: 41842
diff changeset
    59
text {* 
5930d35c976d removed unused legacy lemma names, some comment cleanup.
kleing
parents: 41842
diff changeset
    60
  Arithmetic operations in terms of the reversed bool list,
5930d35c976d removed unused legacy lemma names, some comment cleanup.
kleing
parents: 41842
diff changeset
    61
  assuming input list(s) the same length, and don't extend them. 
5930d35c976d removed unused legacy lemma names, some comment cleanup.
kleing
parents: 41842
diff changeset
    62
*}
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
    63
26557
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
    64
primrec rbl_succ :: "bool list => bool list" where
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
    65
  Nil: "rbl_succ Nil = Nil"
26557
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
    66
  | Cons: "rbl_succ (x # xs) = (if x then False # rbl_succ xs else True # xs)"
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
    67
26557
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
    68
primrec rbl_pred :: "bool list => bool list" where
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
    69
  Nil: "rbl_pred Nil = Nil"
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
    70
  | Cons: "rbl_pred (x # xs) = (if x then False # xs else True # rbl_pred xs)"
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
    71
26557
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
    72
primrec rbl_add :: "bool list => bool list => bool list" where
44939
5930d35c976d removed unused legacy lemma names, some comment cleanup.
kleing
parents: 41842
diff changeset
    73
  -- "result is length of first arg, second arg may be longer"
26557
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
    74
  Nil: "rbl_add Nil x = Nil"
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
    75
  | Cons: "rbl_add (y # ys) x = (let ws = rbl_add ys (tl x) in 
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
    76
    (y ~= hd x) # (if hd x & y then rbl_succ ws else ws))"
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
    77
26557
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
    78
primrec rbl_mult :: "bool list => bool list => bool list" where
44939
5930d35c976d removed unused legacy lemma names, some comment cleanup.
kleing
parents: 41842
diff changeset
    79
  -- "result is length of first arg, second arg may be longer"
26557
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
    80
  Nil: "rbl_mult Nil x = Nil"
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
    81
  | Cons: "rbl_mult (y # ys) x = (let ws = False # rbl_mult ys x in 
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
    82
    if y then rbl_add ws x else ws)"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    83
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    84
lemma butlast_power:
30971
7fbebf75b3ef funpow and relpow with shared "^^" syntax
haftmann
parents: 30952
diff changeset
    85
  "(butlast ^^ n) bl = take (length bl - n) bl"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    86
  by (induct n) (auto simp: butlast_take)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    87
46001
0b562d564d5f redefine some binary operations on integers work on abstract numerals instead of Int.Pls and Int.Min
huffman
parents: 45997
diff changeset
    88
lemma bin_to_bl_aux_zero_minus_simp [simp]:
0b562d564d5f redefine some binary operations on integers work on abstract numerals instead of Int.Pls and Int.Min
huffman
parents: 45997
diff changeset
    89
  "0 < n \<Longrightarrow> bin_to_bl_aux n 0 bl = 
0b562d564d5f redefine some binary operations on integers work on abstract numerals instead of Int.Pls and Int.Min
huffman
parents: 45997
diff changeset
    90
    bin_to_bl_aux (n - 1) 0 (False # bl)"
0b562d564d5f redefine some binary operations on integers work on abstract numerals instead of Int.Pls and Int.Min
huffman
parents: 45997
diff changeset
    91
  by (cases n) auto
0b562d564d5f redefine some binary operations on integers work on abstract numerals instead of Int.Pls and Int.Min
huffman
parents: 45997
diff changeset
    92
46617
8c5d10d41391 make bool list functions respect int/bin distinction
huffman
parents: 46240
diff changeset
    93
lemma bin_to_bl_aux_minus1_minus_simp [simp]:
8c5d10d41391 make bool list functions respect int/bin distinction
huffman
parents: 46240
diff changeset
    94
  "0 < n ==> bin_to_bl_aux n -1 bl = 
8c5d10d41391 make bool list functions respect int/bin distinction
huffman
parents: 46240
diff changeset
    95
    bin_to_bl_aux (n - 1) -1 (True # bl)"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    96
  by (cases n) auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    97
46617
8c5d10d41391 make bool list functions respect int/bin distinction
huffman
parents: 46240
diff changeset
    98
lemma bin_to_bl_aux_one_minus_simp [simp]:
8c5d10d41391 make bool list functions respect int/bin distinction
huffman
parents: 46240
diff changeset
    99
  "0 < n \<Longrightarrow> bin_to_bl_aux n 1 bl = 
8c5d10d41391 make bool list functions respect int/bin distinction
huffman
parents: 46240
diff changeset
   100
    bin_to_bl_aux (n - 1) 0 (True # bl)"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   101
  by (cases n) auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   102
26086
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 26008
diff changeset
   103
lemma bin_to_bl_aux_Bit_minus_simp [simp]:
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   104
  "0 < n ==> bin_to_bl_aux n (w BIT b) bl = 
37654
8e33b9d04a82 use existing bit type from theory Bit
haftmann
parents: 32642
diff changeset
   105
    bin_to_bl_aux (n - 1) w ((b = 1) # bl)"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   106
  by (cases n) auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   107
26086
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 26008
diff changeset
   108
lemma bin_to_bl_aux_Bit0_minus_simp [simp]:
46617
8c5d10d41391 make bool list functions respect int/bin distinction
huffman
parents: 46240
diff changeset
   109
  "0 < n ==> bin_to_bl_aux n (number_of (Int.Bit0 w)) bl = 
8c5d10d41391 make bool list functions respect int/bin distinction
huffman
parents: 46240
diff changeset
   110
    bin_to_bl_aux (n - 1) (number_of w) (False # bl)"
26086
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 26008
diff changeset
   111
  by (cases n) auto
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 26008
diff changeset
   112
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 26008
diff changeset
   113
lemma bin_to_bl_aux_Bit1_minus_simp [simp]:
46617
8c5d10d41391 make bool list functions respect int/bin distinction
huffman
parents: 46240
diff changeset
   114
  "0 < n ==> bin_to_bl_aux n (number_of (Int.Bit1 w)) bl = 
8c5d10d41391 make bool list functions respect int/bin distinction
huffman
parents: 46240
diff changeset
   115
    bin_to_bl_aux (n - 1) (number_of w) (True # bl)"
26086
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 26008
diff changeset
   116
  by (cases n) auto
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   117
44939
5930d35c976d removed unused legacy lemma names, some comment cleanup.
kleing
parents: 41842
diff changeset
   118
text {* Link between bin and bool list. *}
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   119
26557
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
   120
lemma bl_to_bin_aux_append: 
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
   121
  "bl_to_bin_aux (bs @ cs) w = bl_to_bin_aux cs (bl_to_bin_aux bs w)"
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
   122
  by (induct bs arbitrary: w) auto
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   123
26557
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
   124
lemma bin_to_bl_aux_append: 
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
   125
  "bin_to_bl_aux n w bs @ cs = bin_to_bl_aux n w (bs @ cs)"
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
   126
  by (induct n arbitrary: w bs) auto
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   127
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   128
lemma bl_to_bin_append: 
26557
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
   129
  "bl_to_bin (bs @ cs) = bl_to_bin_aux cs (bl_to_bin bs)"
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   130
  unfolding bl_to_bin_def by (rule bl_to_bin_aux_append)
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   131
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   132
lemma bin_to_bl_aux_alt: 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   133
  "bin_to_bl_aux n w bs = bin_to_bl n w @ bs" 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   134
  unfolding bin_to_bl_def by (simp add : bin_to_bl_aux_append)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   135
45996
e69d631fe9af declare simp rules immediately, instead of using 'declare' commands
huffman
parents: 45854
diff changeset
   136
lemma bin_to_bl_0 [simp]: "bin_to_bl 0 bs = []"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   137
  unfolding bin_to_bl_def by auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   138
26557
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
   139
lemma size_bin_to_bl_aux: 
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
   140
  "size (bin_to_bl_aux n w bs) = n + length bs"
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
   141
  by (induct n arbitrary: w bs) auto
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   142
45996
e69d631fe9af declare simp rules immediately, instead of using 'declare' commands
huffman
parents: 45854
diff changeset
   143
lemma size_bin_to_bl [simp]: "size (bin_to_bl n w) = n" 
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   144
  unfolding bin_to_bl_def by (simp add : size_bin_to_bl_aux)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   145
26557
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
   146
lemma bin_bl_bin': 
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
   147
  "bl_to_bin (bin_to_bl_aux n w bs) = 
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
   148
    bl_to_bin_aux bs (bintrunc n w)"
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
   149
  by (induct n arbitrary: w bs) (auto simp add : bl_to_bin_def)
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   150
45996
e69d631fe9af declare simp rules immediately, instead of using 'declare' commands
huffman
parents: 45854
diff changeset
   151
lemma bin_bl_bin [simp]: "bl_to_bin (bin_to_bl n w) = bintrunc n w"
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   152
  unfolding bin_to_bl_def bin_bl_bin' by auto
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   153
26557
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
   154
lemma bl_bin_bl':
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
   155
  "bin_to_bl (n + length bs) (bl_to_bin_aux bs w) = 
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   156
    bin_to_bl_aux n w bs"
26557
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
   157
  apply (induct bs arbitrary: w n)
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   158
   apply auto
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   159
    apply (simp_all only : add_Suc [symmetric])
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   160
    apply (auto simp add : bin_to_bl_def)
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   161
  done
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   162
45996
e69d631fe9af declare simp rules immediately, instead of using 'declare' commands
huffman
parents: 45854
diff changeset
   163
lemma bl_bin_bl [simp]: "bin_to_bl (length bs) (bl_to_bin bs) = bs"
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   164
  unfolding bl_to_bin_def
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   165
  apply (rule box_equals)
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   166
    apply (rule bl_bin_bl')
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   167
   prefer 2
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   168
   apply (rule bin_to_bl_aux.Z)
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   169
  apply simp
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   170
  done
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   171
  
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   172
lemma bl_to_bin_inj:
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   173
  "bl_to_bin bs = bl_to_bin cs ==> length bs = length cs ==> bs = cs"
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   174
  apply (rule_tac box_equals)
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   175
    defer
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   176
    apply (rule bl_bin_bl)
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   177
   apply (rule bl_bin_bl)
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   178
  apply simp
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   179
  done
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   180
45996
e69d631fe9af declare simp rules immediately, instead of using 'declare' commands
huffman
parents: 45854
diff changeset
   181
lemma bl_to_bin_False [simp]: "bl_to_bin (False # bl) = bl_to_bin bl"
46001
0b562d564d5f redefine some binary operations on integers work on abstract numerals instead of Int.Pls and Int.Min
huffman
parents: 45997
diff changeset
   182
  unfolding bl_to_bin_def by auto
45996
e69d631fe9af declare simp rules immediately, instead of using 'declare' commands
huffman
parents: 45854
diff changeset
   183
46001
0b562d564d5f redefine some binary operations on integers work on abstract numerals instead of Int.Pls and Int.Min
huffman
parents: 45997
diff changeset
   184
lemma bl_to_bin_Nil [simp]: "bl_to_bin [] = 0"
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   185
  unfolding bl_to_bin_def by auto
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   186
46001
0b562d564d5f redefine some binary operations on integers work on abstract numerals instead of Int.Pls and Int.Min
huffman
parents: 45997
diff changeset
   187
lemma bin_to_bl_zero_aux: 
0b562d564d5f redefine some binary operations on integers work on abstract numerals instead of Int.Pls and Int.Min
huffman
parents: 45997
diff changeset
   188
  "bin_to_bl_aux n 0 bl = replicate n False @ bl"
0b562d564d5f redefine some binary operations on integers work on abstract numerals instead of Int.Pls and Int.Min
huffman
parents: 45997
diff changeset
   189
  by (induct n arbitrary: bl) (auto simp: replicate_app_Cons_same)
0b562d564d5f redefine some binary operations on integers work on abstract numerals instead of Int.Pls and Int.Min
huffman
parents: 45997
diff changeset
   190
46617
8c5d10d41391 make bool list functions respect int/bin distinction
huffman
parents: 46240
diff changeset
   191
lemma bin_to_bl_zero: "bin_to_bl n 0 = replicate n False"
8c5d10d41391 make bool list functions respect int/bin distinction
huffman
parents: 46240
diff changeset
   192
  unfolding bin_to_bl_def by (simp add: bin_to_bl_zero_aux)
8c5d10d41391 make bool list functions respect int/bin distinction
huffman
parents: 46240
diff changeset
   193
8c5d10d41391 make bool list functions respect int/bin distinction
huffman
parents: 46240
diff changeset
   194
lemma bin_to_bl_minus1_aux:
8c5d10d41391 make bool list functions respect int/bin distinction
huffman
parents: 46240
diff changeset
   195
  "bin_to_bl_aux n -1 bl = replicate n True @ bl"
26557
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
   196
  by (induct n arbitrary: bl) (auto simp: replicate_app_Cons_same)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   197
46617
8c5d10d41391 make bool list functions respect int/bin distinction
huffman
parents: 46240
diff changeset
   198
lemma bin_to_bl_minus1: "bin_to_bl n -1 = replicate n True"
8c5d10d41391 make bool list functions respect int/bin distinction
huffman
parents: 46240
diff changeset
   199
  unfolding bin_to_bl_def by (simp add: bin_to_bl_minus1_aux)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   200
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   201
lemma bl_to_bin_rep_F: 
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   202
  "bl_to_bin (replicate n False @ bl) = bl_to_bin bl"
46001
0b562d564d5f redefine some binary operations on integers work on abstract numerals instead of Int.Pls and Int.Min
huffman
parents: 45997
diff changeset
   203
  apply (simp add: bin_to_bl_zero_aux [symmetric] bin_bl_bin')
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   204
  apply (simp add: bl_to_bin_def)
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   205
  done
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   206
45996
e69d631fe9af declare simp rules immediately, instead of using 'declare' commands
huffman
parents: 45854
diff changeset
   207
lemma bin_to_bl_trunc [simp]:
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   208
  "n <= m ==> bin_to_bl n (bintrunc m w) = bin_to_bl n w"
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   209
  by (auto intro: bl_to_bin_inj)
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   210
45997
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   211
lemma bin_to_bl_aux_bintr:
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   212
  "bin_to_bl_aux n (bintrunc m bin) bl = 
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   213
    replicate (n - m) False @ bin_to_bl_aux (min n m) bin bl"
45997
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   214
  apply (induct n arbitrary: m bin bl)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   215
   apply clarsimp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   216
  apply clarsimp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   217
  apply (case_tac "m")
46001
0b562d564d5f redefine some binary operations on integers work on abstract numerals instead of Int.Pls and Int.Min
huffman
parents: 45997
diff changeset
   218
   apply (clarsimp simp: bin_to_bl_zero_aux) 
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   219
   apply (erule thin_rl)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   220
   apply (induct_tac n)   
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   221
    apply auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   222
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   223
45854
40554613b4f0 replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents: 45847
diff changeset
   224
lemma bin_to_bl_bintr:
40554613b4f0 replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents: 45847
diff changeset
   225
  "bin_to_bl n (bintrunc m bin) =
40554613b4f0 replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents: 45847
diff changeset
   226
    replicate (n - m) False @ bin_to_bl (min n m) bin"
40554613b4f0 replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents: 45847
diff changeset
   227
  unfolding bin_to_bl_def by (rule bin_to_bl_aux_bintr)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   228
46001
0b562d564d5f redefine some binary operations on integers work on abstract numerals instead of Int.Pls and Int.Min
huffman
parents: 45997
diff changeset
   229
lemma bl_to_bin_rep_False: "bl_to_bin (replicate n False) = 0"
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   230
  by (induct n) auto
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   231
26557
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
   232
lemma len_bin_to_bl_aux: 
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
   233
  "length (bin_to_bl_aux n w bs) = n + length bs"
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
   234
  by (induct n arbitrary: w bs) auto
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   235
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   236
lemma len_bin_to_bl [simp]: "length (bin_to_bl n w) = n"
46617
8c5d10d41391 make bool list functions respect int/bin distinction
huffman
parents: 46240
diff changeset
   237
  by (fact size_bin_to_bl) (* FIXME: duplicate *)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   238
  
26557
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
   239
lemma sign_bl_bin': 
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
   240
  "bin_sign (bl_to_bin_aux bs w) = bin_sign w"
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
   241
  by (induct bs arbitrary: w) auto
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   242
  
46001
0b562d564d5f redefine some binary operations on integers work on abstract numerals instead of Int.Pls and Int.Min
huffman
parents: 45997
diff changeset
   243
lemma sign_bl_bin: "bin_sign (bl_to_bin bs) = 0"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   244
  unfolding bl_to_bin_def by (simp add : sign_bl_bin')
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   245
  
26557
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
   246
lemma bl_sbin_sign_aux: 
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
   247
  "hd (bin_to_bl_aux (Suc n) w bs) = 
46001
0b562d564d5f redefine some binary operations on integers work on abstract numerals instead of Int.Pls and Int.Min
huffman
parents: 45997
diff changeset
   248
    (bin_sign (sbintrunc n w) = -1)"
26557
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
   249
  apply (induct n arbitrary: w bs)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   250
   apply clarsimp
26557
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
   251
   apply (cases w rule: bin_exhaust)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   252
   apply (simp split add : bit.split)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   253
  apply clarsimp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   254
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   255
    
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   256
lemma bl_sbin_sign: 
46001
0b562d564d5f redefine some binary operations on integers work on abstract numerals instead of Int.Pls and Int.Min
huffman
parents: 45997
diff changeset
   257
  "hd (bin_to_bl (Suc n) w) = (bin_sign (sbintrunc n w) = -1)"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   258
  unfolding bin_to_bl_def by (rule bl_sbin_sign_aux)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   259
45997
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   260
lemma bin_nth_of_bl_aux:
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   261
  "bin_nth (bl_to_bin_aux bl w) n = 
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   262
    (n < size bl & rev bl ! n | n >= length bl & bin_nth w (n - size bl))"
45997
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   263
  apply (induct bl arbitrary: w)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   264
   apply clarsimp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   265
  apply clarsimp
45997
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   266
  apply (cut_tac x=n and y="size bl" in linorder_less_linear)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   267
  apply (erule disjE, simp add: nth_append)+
26557
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
   268
  apply auto
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   269
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   270
45475
b2b087c20e45 removed some old-style semicolons
huffman
parents: 44939
diff changeset
   271
lemma bin_nth_of_bl: "bin_nth (bl_to_bin bl) n = (n < length bl & rev bl ! n)"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   272
  unfolding bl_to_bin_def by (simp add : bin_nth_of_bl_aux)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   273
45997
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   274
lemma bin_nth_bl: "n < m \<Longrightarrow> bin_nth w n = nth (rev (bin_to_bl m w)) n"
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   275
  apply (induct n arbitrary: m w)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   276
   apply clarsimp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   277
   apply (case_tac m, clarsimp)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   278
   apply (clarsimp simp: bin_to_bl_def)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   279
   apply (simp add: bin_to_bl_aux_alt)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   280
  apply clarsimp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   281
  apply (case_tac m, clarsimp)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   282
  apply (clarsimp simp: bin_to_bl_def)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   283
  apply (simp add: bin_to_bl_aux_alt)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   284
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   285
45997
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   286
lemma nth_rev:
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   287
  "n < length xs \<Longrightarrow> rev xs ! n = xs ! (length xs - 1 - n)"
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   288
  apply (induct xs)
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   289
   apply simp
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   290
  apply (clarsimp simp add : nth_append nth.simps split add : nat.split)
45997
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   291
  apply (rule_tac f = "\<lambda>n. xs ! n" in arg_cong)
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   292
  apply arith
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   293
  done
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   294
45854
40554613b4f0 replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents: 45847
diff changeset
   295
lemma nth_rev_alt: "n < length ys \<Longrightarrow> ys ! n = rev ys ! (length ys - Suc n)"
40554613b4f0 replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents: 45847
diff changeset
   296
  by (simp add: nth_rev)
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   297
45997
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   298
lemma nth_bin_to_bl_aux:
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   299
  "n < m + length bl \<Longrightarrow> (bin_to_bl_aux m w bl) ! n = 
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   300
    (if n < m then bin_nth w (m - 1 - n) else bl ! (n - m))"
45997
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   301
  apply (induct m arbitrary: w n bl)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   302
   apply clarsimp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   303
  apply clarsimp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   304
  apply (case_tac w rule: bin_exhaust)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   305
  apply simp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   306
  done
45997
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   307
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   308
lemma nth_bin_to_bl: "n < m ==> (bin_to_bl m w) ! n = bin_nth w (m - Suc n)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   309
  unfolding bin_to_bl_def by (simp add : nth_bin_to_bl_aux)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   310
45997
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   311
lemma bl_to_bin_lt2p_aux:
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   312
  "bl_to_bin_aux bs w < (w + 1) * (2 ^ length bs)"
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   313
  apply (induct bs arbitrary: w)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   314
   apply clarsimp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   315
  apply clarsimp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   316
  apply safe
46240
933f35c4e126 factor-cancellation simprocs now call the full simplifier to prove that factors are non-zero
huffman
parents: 46001
diff changeset
   317
  apply (drule meta_spec, erule xtr8 [rotated], simp add: Bit_def)+
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   318
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   319
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   320
lemma bl_to_bin_lt2p: "bl_to_bin bs < (2 ^ length bs)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   321
  apply (unfold bl_to_bin_def)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   322
  apply (rule xtr1)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   323
   prefer 2
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   324
   apply (rule bl_to_bin_lt2p_aux)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   325
  apply simp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   326
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   327
45997
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   328
lemma bl_to_bin_ge2p_aux:
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   329
  "bl_to_bin_aux bs w >= w * (2 ^ length bs)"
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   330
  apply (induct bs arbitrary: w)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   331
   apply clarsimp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   332
  apply clarsimp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   333
  apply safe
46652
bec50f8b3727 avoid using BIT_simps in proofs
huffman
parents: 46645
diff changeset
   334
   apply (drule meta_spec, erule order_trans [rotated],
bec50f8b3727 avoid using BIT_simps in proofs
huffman
parents: 46645
diff changeset
   335
          simp add: Bit_B0_2t Bit_B1_2t algebra_simps)+
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   336
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   337
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   338
lemma bl_to_bin_ge0: "bl_to_bin bs >= 0"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   339
  apply (unfold bl_to_bin_def)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   340
  apply (rule xtr4)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   341
   apply (rule bl_to_bin_ge2p_aux)
46617
8c5d10d41391 make bool list functions respect int/bin distinction
huffman
parents: 46240
diff changeset
   342
  apply simp
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   343
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   344
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   345
lemma butlast_rest_bin: 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   346
  "butlast (bin_to_bl n w) = bin_to_bl (n - 1) (bin_rest w)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   347
  apply (unfold bin_to_bl_def)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   348
  apply (cases w rule: bin_exhaust)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   349
  apply (cases n, clarsimp)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   350
  apply clarsimp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   351
  apply (auto simp add: bin_to_bl_aux_alt)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   352
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   353
45854
40554613b4f0 replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents: 45847
diff changeset
   354
lemma butlast_bin_rest:
40554613b4f0 replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents: 45847
diff changeset
   355
  "butlast bl = bin_to_bl (length bl - Suc 0) (bin_rest (bl_to_bin bl))"
40554613b4f0 replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents: 45847
diff changeset
   356
  using butlast_rest_bin [where w="bl_to_bin bl" and n="length bl"] by simp
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   357
26557
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
   358
lemma butlast_rest_bl2bin_aux:
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
   359
  "bl ~= [] \<Longrightarrow>
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
   360
    bl_to_bin_aux (butlast bl) w = bin_rest (bl_to_bin_aux bl w)"
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
   361
  by (induct bl arbitrary: w) auto
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   362
  
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   363
lemma butlast_rest_bl2bin: 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   364
  "bl_to_bin (butlast bl) = bin_rest (bl_to_bin bl)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   365
  apply (unfold bl_to_bin_def)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   366
  apply (cases bl)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   367
   apply (auto simp add: butlast_rest_bl2bin_aux)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   368
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   369
45997
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   370
lemma trunc_bl2bin_aux:
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   371
  "bintrunc m (bl_to_bin_aux bl w) = 
26557
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
   372
    bl_to_bin_aux (drop (length bl - m) bl) (bintrunc (m - length bl) w)"
45997
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   373
  apply (induct bl arbitrary: w)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   374
   apply clarsimp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   375
  apply clarsimp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   376
  apply safe
45997
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   377
   apply (case_tac "m - size bl")
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   378
    apply (simp add : diff_is_0_eq [THEN iffD1, THEN Suc_diff_le])
46652
bec50f8b3727 avoid using BIT_simps in proofs
huffman
parents: 46645
diff changeset
   379
   apply simp
bec50f8b3727 avoid using BIT_simps in proofs
huffman
parents: 46645
diff changeset
   380
   apply (rule_tac f = "%nat. bl_to_bin_aux bl (bintrunc nat w BIT 1)" 
45997
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   381
                   in arg_cong)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   382
   apply simp
45997
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   383
  apply (case_tac "m - size bl")
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   384
   apply (simp add: diff_is_0_eq [THEN iffD1, THEN Suc_diff_le])
46652
bec50f8b3727 avoid using BIT_simps in proofs
huffman
parents: 46645
diff changeset
   385
  apply simp
bec50f8b3727 avoid using BIT_simps in proofs
huffman
parents: 46645
diff changeset
   386
  apply (rule_tac f = "%nat. bl_to_bin_aux bl (bintrunc nat w BIT 0)"
45997
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   387
                  in arg_cong)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   388
  apply simp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   389
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   390
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   391
lemma trunc_bl2bin: 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   392
  "bintrunc m (bl_to_bin bl) = bl_to_bin (drop (length bl - m) bl)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   393
  unfolding bl_to_bin_def by (simp add : trunc_bl2bin_aux)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   394
  
45854
40554613b4f0 replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents: 45847
diff changeset
   395
lemma trunc_bl2bin_len [simp]:
40554613b4f0 replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents: 45847
diff changeset
   396
  "bintrunc (length bl) (bl_to_bin bl) = bl_to_bin bl"
40554613b4f0 replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents: 45847
diff changeset
   397
  by (simp add: trunc_bl2bin)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   398
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   399
lemma bl2bin_drop: 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   400
  "bl_to_bin (drop k bl) = bintrunc (length bl - k) (bl_to_bin bl)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   401
  apply (rule trans)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   402
   prefer 2
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   403
   apply (rule trunc_bl2bin [symmetric])
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   404
  apply (cases "k <= length bl")
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   405
   apply auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   406
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   407
45997
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   408
lemma nth_rest_power_bin:
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   409
  "bin_nth ((bin_rest ^^ k) w) n = bin_nth w (n + k)"
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   410
  apply (induct k arbitrary: n, clarsimp)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   411
  apply clarsimp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   412
  apply (simp only: bin_nth.Suc [symmetric] add_Suc)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   413
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   414
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   415
lemma take_rest_power_bin:
30971
7fbebf75b3ef funpow and relpow with shared "^^" syntax
haftmann
parents: 30952
diff changeset
   416
  "m <= n ==> take m (bin_to_bl n w) = bin_to_bl m ((bin_rest ^^ (n - m)) w)" 
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   417
  apply (rule nth_equalityI)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   418
   apply simp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   419
  apply (clarsimp simp add: nth_bin_to_bl nth_rest_power_bin)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   420
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   421
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   422
lemma hd_butlast: "size xs > 1 ==> hd (butlast xs) = hd xs"
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   423
  by (cases xs) auto
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   424
26557
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
   425
lemma last_bin_last': 
37654
8e33b9d04a82 use existing bit type from theory Bit
haftmann
parents: 32642
diff changeset
   426
  "size xs > 0 \<Longrightarrow> last xs = (bin_last (bl_to_bin_aux xs w) = 1)" 
26557
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
   427
  by (induct xs arbitrary: w) auto
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   428
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   429
lemma last_bin_last: 
37654
8e33b9d04a82 use existing bit type from theory Bit
haftmann
parents: 32642
diff changeset
   430
  "size xs > 0 ==> last xs = (bin_last (bl_to_bin xs) = 1)" 
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   431
  unfolding bl_to_bin_def by (erule last_bin_last')
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   432
  
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   433
lemma bin_last_last: 
37654
8e33b9d04a82 use existing bit type from theory Bit
haftmann
parents: 32642
diff changeset
   434
  "bin_last w = (if last (bin_to_bl (Suc n) w) then 1 else 0)" 
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   435
  apply (unfold bin_to_bl_def)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   436
  apply simp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   437
  apply (auto simp add: bin_to_bl_aux_alt)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   438
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   439
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   440
(** links between bit-wise operations and operations on bool lists **)
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   441
    
45997
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   442
lemma bl_xor_aux_bin:
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   443
  "map2 (%x y. x ~= y) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) = 
26557
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
   444
    bin_to_bl_aux n (v XOR w) (map2 (%x y. x ~= y) bs cs)"
45997
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   445
  apply (induct n arbitrary: v w bs cs)
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   446
   apply simp
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   447
  apply (case_tac v rule: bin_exhaust)
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   448
  apply (case_tac w rule: bin_exhaust)
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   449
  apply clarsimp
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   450
  apply (case_tac b)
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   451
  apply (case_tac ba, safe, simp_all)+
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   452
  done
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   453
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   454
lemma bl_or_aux_bin:
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   455
  "map2 (op | ) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) = 
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   456
    bin_to_bl_aux n (v OR w) (map2 (op | ) bs cs)"
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   457
  apply (induct n arbitrary: v w bs cs)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   458
   apply simp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   459
  apply (case_tac v rule: bin_exhaust)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   460
  apply (case_tac w rule: bin_exhaust)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   461
  apply clarsimp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   462
  apply (case_tac b)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   463
  apply (case_tac ba, safe, simp_all)+
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   464
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   465
    
45997
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   466
lemma bl_and_aux_bin:
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   467
  "map2 (op & ) (bin_to_bl_aux n v bs) (bin_to_bl_aux n w cs) = 
26557
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
   468
    bin_to_bl_aux n (v AND w) (map2 (op & ) bs cs)" 
45997
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   469
  apply (induct n arbitrary: v w bs cs)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   470
   apply simp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   471
  apply (case_tac v rule: bin_exhaust)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   472
  apply (case_tac w rule: bin_exhaust)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   473
  apply clarsimp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   474
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   475
    
45997
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   476
lemma bl_not_aux_bin:
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   477
  "map Not (bin_to_bl_aux n w cs) = 
24353
9a7a9b19e925 use overloaded bitwise operators at type int
huffman
parents: 24350
diff changeset
   478
    bin_to_bl_aux n (NOT w) (map Not cs)"
45997
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   479
  apply (induct n arbitrary: w cs)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   480
   apply clarsimp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   481
  apply clarsimp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   482
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   483
45854
40554613b4f0 replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents: 45847
diff changeset
   484
lemma bl_not_bin: "map Not (bin_to_bl n w) = bin_to_bl n (NOT w)"
40554613b4f0 replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents: 45847
diff changeset
   485
  unfolding bin_to_bl_def by (simp add: bl_not_aux_bin)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   486
45854
40554613b4f0 replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents: 45847
diff changeset
   487
lemma bl_and_bin:
40554613b4f0 replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents: 45847
diff changeset
   488
  "map2 (op \<and>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v AND w)"
40554613b4f0 replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents: 45847
diff changeset
   489
  unfolding bin_to_bl_def by (simp add: bl_and_aux_bin)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   490
45854
40554613b4f0 replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents: 45847
diff changeset
   491
lemma bl_or_bin:
40554613b4f0 replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents: 45847
diff changeset
   492
  "map2 (op \<or>) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v OR w)"
40554613b4f0 replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents: 45847
diff changeset
   493
  unfolding bin_to_bl_def by (simp add: bl_or_aux_bin)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   494
45854
40554613b4f0 replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents: 45847
diff changeset
   495
lemma bl_xor_bin:
40554613b4f0 replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents: 45847
diff changeset
   496
  "map2 (\<lambda>x y. x \<noteq> y) (bin_to_bl n v) (bin_to_bl n w) = bin_to_bl n (v XOR w)"
40554613b4f0 replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents: 45847
diff changeset
   497
  unfolding bin_to_bl_def by (simp only: bl_xor_aux_bin map2_Nil)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   498
45997
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   499
lemma drop_bin2bl_aux:
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   500
  "drop m (bin_to_bl_aux n bin bs) = 
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   501
    bin_to_bl_aux (n - m) bin (drop (m - n) bs)"
45997
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   502
  apply (induct n arbitrary: m bin bs, clarsimp)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   503
  apply clarsimp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   504
  apply (case_tac bin rule: bin_exhaust)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   505
  apply (case_tac "m <= n", simp)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   506
  apply (case_tac "m - n", simp)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   507
  apply simp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   508
  apply (rule_tac f = "%nat. drop nat bs" in arg_cong) 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   509
  apply simp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   510
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   511
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   512
lemma drop_bin2bl: "drop m (bin_to_bl n bin) = bin_to_bl (n - m) bin"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   513
  unfolding bin_to_bl_def by (simp add : drop_bin2bl_aux)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   514
45997
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   515
lemma take_bin2bl_lem1:
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   516
  "take m (bin_to_bl_aux m w bs) = bin_to_bl m w"
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   517
  apply (induct m arbitrary: w bs, clarsimp)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   518
  apply clarsimp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   519
  apply (simp add: bin_to_bl_aux_alt)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   520
  apply (simp add: bin_to_bl_def)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   521
  apply (simp add: bin_to_bl_aux_alt)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   522
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   523
45997
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   524
lemma take_bin2bl_lem:
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   525
  "take m (bin_to_bl_aux (m + n) w bs) = 
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   526
    take m (bin_to_bl (m + n) w)"
45997
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   527
  apply (induct n arbitrary: w bs)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   528
   apply (simp_all (no_asm) add: bin_to_bl_def take_bin2bl_lem1)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   529
  apply simp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   530
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   531
45997
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   532
lemma bin_split_take:
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   533
  "bin_split n c = (a, b) \<Longrightarrow>
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   534
    bin_to_bl m a = take m (bin_to_bl (m + n) c)"
45997
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   535
  apply (induct n arbitrary: b c)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   536
   apply clarsimp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   537
  apply (clarsimp simp: Let_def split: ls_splits)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   538
  apply (simp add: bin_to_bl_def)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   539
  apply (simp add: take_bin2bl_lem)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   540
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   541
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   542
lemma bin_split_take1: 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   543
  "k = m + n ==> bin_split n c = (a, b) ==> 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   544
    bin_to_bl m a = take m (bin_to_bl k c)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   545
  by (auto elim: bin_split_take)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   546
  
45997
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   547
lemma nth_takefill: "m < n \<Longrightarrow>
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   548
    takefill fill n l ! m = (if m < length l then l ! m else fill)"
45997
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   549
  apply (induct n arbitrary: m l, clarsimp)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   550
  apply clarsimp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   551
  apply (case_tac m)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   552
   apply (simp split: list.split)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   553
  apply (simp split: list.split)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   554
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   555
45997
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   556
lemma takefill_alt:
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   557
  "takefill fill n l = take n l @ replicate (n - length l) fill"
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   558
  by (induct n arbitrary: l) (auto split: list.split)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   559
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   560
lemma takefill_replicate [simp]:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   561
  "takefill fill n (replicate m fill) = replicate n fill"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   562
  by (simp add : takefill_alt replicate_add [symmetric])
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   563
45997
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   564
lemma takefill_le':
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   565
  "n = m + k \<Longrightarrow> takefill x m (takefill x n l) = takefill x m l"
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   566
  by (induct m arbitrary: l n) (auto split: list.split)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   567
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   568
lemma length_takefill [simp]: "length (takefill fill n l) = n"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   569
  by (simp add : takefill_alt)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   570
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   571
lemma take_takefill':
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   572
  "!!w n.  n = k + m ==> take k (takefill fill n w) = takefill fill k w"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   573
  by (induct k) (auto split add : list.split) 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   574
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   575
lemma drop_takefill:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   576
  "!!w. drop k (takefill fill (m + k) w) = takefill fill m (drop k w)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   577
  by (induct k) (auto split add : list.split) 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   578
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   579
lemma takefill_le [simp]:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   580
  "m \<le> n \<Longrightarrow> takefill x m (takefill x n l) = takefill x m l"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   581
  by (auto simp: le_iff_add takefill_le')
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   582
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   583
lemma take_takefill [simp]:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   584
  "m \<le> n \<Longrightarrow> take m (takefill fill n w) = takefill fill m w"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   585
  by (auto simp: le_iff_add take_takefill')
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   586
 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   587
lemma takefill_append:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   588
  "takefill fill (m + length xs) (xs @ w) = xs @ (takefill fill m w)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   589
  by (induct xs) auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   590
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   591
lemma takefill_same': 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   592
  "l = length xs ==> takefill fill l xs = xs"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   593
  by clarify (induct xs, auto)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   594
 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   595
lemmas takefill_same [simp] = takefill_same' [OF refl]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   596
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   597
lemma takefill_bintrunc:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   598
  "takefill False n bl = rev (bin_to_bl n (bl_to_bin (rev bl)))"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   599
  apply (rule nth_equalityI)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   600
   apply simp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   601
  apply (clarsimp simp: nth_takefill nth_rev nth_bin_to_bl bin_nth_of_bl)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   602
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   603
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   604
lemma bl_bin_bl_rtf:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   605
  "bin_to_bl n (bl_to_bin bl) = rev (takefill False n (rev bl))"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   606
  by (simp add : takefill_bintrunc)
45854
40554613b4f0 replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents: 45847
diff changeset
   607
40554613b4f0 replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents: 45847
diff changeset
   608
lemma bl_bin_bl_rep_drop:
40554613b4f0 replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents: 45847
diff changeset
   609
  "bin_to_bl n (bl_to_bin bl) =
40554613b4f0 replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents: 45847
diff changeset
   610
    replicate (n - length bl) False @ drop (length bl - n) bl"
40554613b4f0 replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents: 45847
diff changeset
   611
  by (simp add: bl_bin_bl_rtf takefill_alt rev_take)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   612
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   613
lemma tf_rev:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   614
  "n + k = m + length bl ==> takefill x m (rev (takefill y n bl)) = 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   615
    rev (takefill y m (rev (takefill x k (rev bl))))"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   616
  apply (rule nth_equalityI)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   617
   apply (auto simp add: nth_takefill nth_rev)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   618
  apply (rule_tac f = "%n. bl ! n" in arg_cong) 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   619
  apply arith 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   620
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   621
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   622
lemma takefill_minus:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   623
  "0 < n ==> takefill fill (Suc (n - 1)) w = takefill fill n w"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   624
  by auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   625
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   626
lemmas takefill_Suc_cases = 
45604
29cf40fe8daf eliminated obsolete "standard";
wenzelm
parents: 45543
diff changeset
   627
  list.cases [THEN takefill.Suc [THEN trans]]
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   628
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   629
lemmas takefill_Suc_Nil = takefill_Suc_cases (1)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   630
lemmas takefill_Suc_Cons = takefill_Suc_cases (2)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   631
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   632
lemmas takefill_minus_simps = takefill_Suc_cases [THEN [2] 
45604
29cf40fe8daf eliminated obsolete "standard";
wenzelm
parents: 45543
diff changeset
   633
  takefill_minus [symmetric, THEN trans]]
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   634
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   635
lemmas takefill_pred_simps [simp] =
45604
29cf40fe8daf eliminated obsolete "standard";
wenzelm
parents: 45543
diff changeset
   636
  takefill_minus_simps [where n="number_of bin", simplified nobm1] for bin
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   637
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   638
(* links with function bl_to_bin *)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   639
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   640
lemma bl_to_bin_aux_cat: 
26557
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
   641
  "!!nv v. bl_to_bin_aux bs (bin_cat w nv v) = 
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
   642
    bin_cat w (nv + length bs) (bl_to_bin_aux bs v)"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   643
  apply (induct bs)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   644
   apply simp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   645
  apply (simp add: bin_cat_Suc_Bit [symmetric] del: bin_cat.simps)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   646
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   647
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   648
lemma bin_to_bl_aux_cat: 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   649
  "!!w bs. bin_to_bl_aux (nv + nw) (bin_cat v nw w) bs = 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   650
    bin_to_bl_aux nv v (bin_to_bl_aux nw w bs)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   651
  by (induct nw) auto 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   652
45854
40554613b4f0 replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents: 45847
diff changeset
   653
lemma bl_to_bin_aux_alt:
40554613b4f0 replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents: 45847
diff changeset
   654
  "bl_to_bin_aux bs w = bin_cat w (length bs) (bl_to_bin bs)"
46001
0b562d564d5f redefine some binary operations on integers work on abstract numerals instead of Int.Pls and Int.Min
huffman
parents: 45997
diff changeset
   655
  using bl_to_bin_aux_cat [where nv = "0" and v = "0"]
45854
40554613b4f0 replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents: 45847
diff changeset
   656
  unfolding bl_to_bin_def [symmetric] by simp
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   657
45854
40554613b4f0 replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents: 45847
diff changeset
   658
lemma bin_to_bl_cat:
40554613b4f0 replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents: 45847
diff changeset
   659
  "bin_to_bl (nv + nw) (bin_cat v nw w) =
40554613b4f0 replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents: 45847
diff changeset
   660
    bin_to_bl_aux nv v (bin_to_bl nw w)"
40554613b4f0 replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents: 45847
diff changeset
   661
  unfolding bin_to_bl_def by (simp add: bin_to_bl_aux_cat)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   662
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   663
lemmas bl_to_bin_aux_app_cat = 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   664
  trans [OF bl_to_bin_aux_append bl_to_bin_aux_alt]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   665
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   666
lemmas bin_to_bl_aux_cat_app =
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   667
  trans [OF bin_to_bl_aux_cat bin_to_bl_aux_alt]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   668
45854
40554613b4f0 replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents: 45847
diff changeset
   669
lemma bl_to_bin_app_cat:
40554613b4f0 replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents: 45847
diff changeset
   670
  "bl_to_bin (bsa @ bs) = bin_cat (bl_to_bin bsa) (length bs) (bl_to_bin bs)"
40554613b4f0 replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents: 45847
diff changeset
   671
  by (simp only: bl_to_bin_aux_app_cat bl_to_bin_def)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   672
45854
40554613b4f0 replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents: 45847
diff changeset
   673
lemma bin_to_bl_cat_app:
40554613b4f0 replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents: 45847
diff changeset
   674
  "bin_to_bl (n + nw) (bin_cat w nw wa) = bin_to_bl n w @ bin_to_bl nw wa"
40554613b4f0 replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents: 45847
diff changeset
   675
  by (simp only: bin_to_bl_def bin_to_bl_aux_cat_app)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   676
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   677
(* bl_to_bin_app_cat_alt and bl_to_bin_app_cat are easily interderivable *)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   678
lemma bl_to_bin_app_cat_alt: 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   679
  "bin_cat (bl_to_bin cs) n w = bl_to_bin (cs @ bin_to_bl n w)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   680
  by (simp add : bl_to_bin_app_cat)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   681
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   682
lemma mask_lem: "(bl_to_bin (True # replicate n False)) = 
46645
573aff6b9b0a adapt lemma mask_lem to respect int/bin distinction
huffman
parents: 46617
diff changeset
   683
    (bl_to_bin (replicate n True)) + 1"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   684
  apply (unfold bl_to_bin_def)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   685
  apply (induct n)
46645
573aff6b9b0a adapt lemma mask_lem to respect int/bin distinction
huffman
parents: 46617
diff changeset
   686
   apply simp
31790
05c92381363c corrected and unified thm names
nipkow
parents: 30971
diff changeset
   687
  apply (simp only: Suc_eq_plus1 replicate_add
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   688
                    append_Cons [symmetric] bl_to_bin_aux_append)
46645
573aff6b9b0a adapt lemma mask_lem to respect int/bin distinction
huffman
parents: 46617
diff changeset
   689
  apply (simp add: Bit_B0_2t Bit_B1_2t)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   690
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   691
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   692
(* function bl_of_nth *)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   693
lemma length_bl_of_nth [simp]: "length (bl_of_nth n f) = n"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   694
  by (induct n)  auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   695
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   696
lemma nth_bl_of_nth [simp]:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   697
  "m < n \<Longrightarrow> rev (bl_of_nth n f) ! m = f m"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   698
  apply (induct n)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   699
   apply simp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   700
  apply (clarsimp simp add : nth_append)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   701
  apply (rule_tac f = "f" in arg_cong) 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   702
  apply simp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   703
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   704
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   705
lemma bl_of_nth_inj: 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   706
  "(!!k. k < n ==> f k = g k) ==> bl_of_nth n f = bl_of_nth n g"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   707
  by (induct n)  auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   708
45997
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   709
lemma bl_of_nth_nth_le:
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   710
  "n \<le> length xs \<Longrightarrow> bl_of_nth n (nth (rev xs)) = drop (length xs - n) xs"
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   711
  apply (induct n arbitrary: xs, clarsimp)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   712
  apply clarsimp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   713
  apply (rule trans [OF _ hd_Cons_tl])
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   714
   apply (frule Suc_le_lessD)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   715
   apply (simp add: nth_rev trans [OF drop_Suc drop_tl, symmetric])
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   716
   apply (subst hd_drop_conv_nth)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   717
     apply force
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   718
    apply simp_all
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   719
  apply (rule_tac f = "%n. drop n xs" in arg_cong) 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   720
  apply simp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   721
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   722
45854
40554613b4f0 replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents: 45847
diff changeset
   723
lemma bl_of_nth_nth [simp]: "bl_of_nth (length xs) (op ! (rev xs)) = xs"
40554613b4f0 replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents: 45847
diff changeset
   724
  by (simp add: bl_of_nth_nth_le)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   725
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   726
lemma size_rbl_pred: "length (rbl_pred bl) = length bl"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   727
  by (induct bl) auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   728
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   729
lemma size_rbl_succ: "length (rbl_succ bl) = length bl"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   730
  by (induct bl) auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   731
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   732
lemma size_rbl_add:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   733
  "!!cl. length (rbl_add bl cl) = length bl"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   734
  by (induct bl) (auto simp: Let_def size_rbl_succ)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   735
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   736
lemma size_rbl_mult: 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   737
  "!!cl. length (rbl_mult bl cl) = length bl"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   738
  by (induct bl) (auto simp add : Let_def size_rbl_add)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   739
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   740
lemmas rbl_sizes [simp] = 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   741
  size_rbl_pred size_rbl_succ size_rbl_add size_rbl_mult
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   742
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   743
lemmas rbl_Nils =
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   744
  rbl_pred.Nil rbl_succ.Nil rbl_add.Nil rbl_mult.Nil
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   745
46653
a557db8f2fbf avoid using BIT_simps in proofs;
huffman
parents: 46652
diff changeset
   746
lemma pred_BIT_simps [simp]:
a557db8f2fbf avoid using BIT_simps in proofs;
huffman
parents: 46652
diff changeset
   747
  "x BIT 0 - 1 = (x - 1) BIT 1"
a557db8f2fbf avoid using BIT_simps in proofs;
huffman
parents: 46652
diff changeset
   748
  "x BIT 1 - 1 = x BIT 0"
a557db8f2fbf avoid using BIT_simps in proofs;
huffman
parents: 46652
diff changeset
   749
  by (simp_all add: Bit_B0_2t Bit_B1_2t)
a557db8f2fbf avoid using BIT_simps in proofs;
huffman
parents: 46652
diff changeset
   750
a557db8f2fbf avoid using BIT_simps in proofs;
huffman
parents: 46652
diff changeset
   751
lemma rbl_pred:
a557db8f2fbf avoid using BIT_simps in proofs;
huffman
parents: 46652
diff changeset
   752
  "rbl_pred (rev (bin_to_bl n bin)) = rev (bin_to_bl n (bin - 1))"
a557db8f2fbf avoid using BIT_simps in proofs;
huffman
parents: 46652
diff changeset
   753
  apply (induct n arbitrary: bin, simp)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   754
  apply (unfold bin_to_bl_def)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   755
  apply clarsimp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   756
  apply (case_tac bin rule: bin_exhaust)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   757
  apply (case_tac b)
46653
a557db8f2fbf avoid using BIT_simps in proofs;
huffman
parents: 46652
diff changeset
   758
   apply (clarsimp simp: bin_to_bl_aux_alt)+
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   759
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   760
46653
a557db8f2fbf avoid using BIT_simps in proofs;
huffman
parents: 46652
diff changeset
   761
lemma succ_BIT_simps [simp]:
a557db8f2fbf avoid using BIT_simps in proofs;
huffman
parents: 46652
diff changeset
   762
  "x BIT 0 + 1 = x BIT 1"
a557db8f2fbf avoid using BIT_simps in proofs;
huffman
parents: 46652
diff changeset
   763
  "x BIT 1 + 1 = (x + 1) BIT 0"
a557db8f2fbf avoid using BIT_simps in proofs;
huffman
parents: 46652
diff changeset
   764
  by (simp_all add: Bit_B0_2t Bit_B1_2t)
a557db8f2fbf avoid using BIT_simps in proofs;
huffman
parents: 46652
diff changeset
   765
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   766
lemma rbl_succ: 
46653
a557db8f2fbf avoid using BIT_simps in proofs;
huffman
parents: 46652
diff changeset
   767
  "rbl_succ (rev (bin_to_bl n bin)) = rev (bin_to_bl n (bin + 1))"
a557db8f2fbf avoid using BIT_simps in proofs;
huffman
parents: 46652
diff changeset
   768
  apply (induct n arbitrary: bin, simp)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   769
  apply (unfold bin_to_bl_def)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   770
  apply clarsimp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   771
  apply (case_tac bin rule: bin_exhaust)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   772
  apply (case_tac b)
46653
a557db8f2fbf avoid using BIT_simps in proofs;
huffman
parents: 46652
diff changeset
   773
   apply (clarsimp simp: bin_to_bl_aux_alt)+
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   774
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   775
46653
a557db8f2fbf avoid using BIT_simps in proofs;
huffman
parents: 46652
diff changeset
   776
lemma add_BIT_simps [simp]: (* FIXME: move *)
a557db8f2fbf avoid using BIT_simps in proofs;
huffman
parents: 46652
diff changeset
   777
  "x BIT 0 + y BIT 0 = (x + y) BIT 0"
a557db8f2fbf avoid using BIT_simps in proofs;
huffman
parents: 46652
diff changeset
   778
  "x BIT 0 + y BIT 1 = (x + y) BIT 1"
a557db8f2fbf avoid using BIT_simps in proofs;
huffman
parents: 46652
diff changeset
   779
  "x BIT 1 + y BIT 0 = (x + y) BIT 1"
a557db8f2fbf avoid using BIT_simps in proofs;
huffman
parents: 46652
diff changeset
   780
  "x BIT 1 + y BIT 1 = (x + y + 1) BIT 0"
a557db8f2fbf avoid using BIT_simps in proofs;
huffman
parents: 46652
diff changeset
   781
  by (simp_all add: Bit_B0_2t Bit_B1_2t)
a557db8f2fbf avoid using BIT_simps in proofs;
huffman
parents: 46652
diff changeset
   782
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   783
lemma rbl_add: 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   784
  "!!bina binb. rbl_add (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb)) = 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   785
    rev (bin_to_bl n (bina + binb))"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   786
  apply (induct n, simp)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   787
  apply (unfold bin_to_bl_def)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   788
  apply clarsimp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   789
  apply (case_tac bina rule: bin_exhaust)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   790
  apply (case_tac binb rule: bin_exhaust)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   791
  apply (case_tac b)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   792
   apply (case_tac [!] "ba")
46655
be76913ec1a4 avoid using Int.succ_def in proofs
huffman
parents: 46653
diff changeset
   793
     apply (auto simp: rbl_succ bin_to_bl_aux_alt Let_def add_ac)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   794
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   795
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   796
lemma rbl_add_app2: 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   797
  "!!blb. length blb >= length bla ==> 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   798
    rbl_add bla (blb @ blc) = rbl_add bla blb"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   799
  apply (induct bla, simp)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   800
  apply clarsimp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   801
  apply (case_tac blb, clarsimp)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   802
  apply (clarsimp simp: Let_def)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   803
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   804
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   805
lemma rbl_add_take2: 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   806
  "!!blb. length blb >= length bla ==> 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   807
    rbl_add bla (take (length bla) blb) = rbl_add bla blb"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   808
  apply (induct bla, simp)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   809
  apply clarsimp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   810
  apply (case_tac blb, clarsimp)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   811
  apply (clarsimp simp: Let_def)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   812
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   813
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   814
lemma rbl_add_long: 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   815
  "m >= n ==> rbl_add (rev (bin_to_bl n bina)) (rev (bin_to_bl m binb)) = 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   816
    rev (bin_to_bl n (bina + binb))"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   817
  apply (rule box_equals [OF _ rbl_add_take2 rbl_add])
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   818
   apply (rule_tac f = "rbl_add (rev (bin_to_bl n bina))" in arg_cong) 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   819
   apply (rule rev_swap [THEN iffD1])
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   820
   apply (simp add: rev_take drop_bin2bl)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   821
  apply simp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   822
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   823
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   824
lemma rbl_mult_app2:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   825
  "!!blb. length blb >= length bla ==> 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   826
    rbl_mult bla (blb @ blc) = rbl_mult bla blb"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   827
  apply (induct bla, simp)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   828
  apply clarsimp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   829
  apply (case_tac blb, clarsimp)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   830
  apply (clarsimp simp: Let_def rbl_add_app2)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   831
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   832
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   833
lemma rbl_mult_take2: 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   834
  "length blb >= length bla ==> 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   835
    rbl_mult bla (take (length bla) blb) = rbl_mult bla blb"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   836
  apply (rule trans)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   837
   apply (rule rbl_mult_app2 [symmetric])
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   838
   apply simp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   839
  apply (rule_tac f = "rbl_mult bla" in arg_cong) 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   840
  apply (rule append_take_drop_id)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   841
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   842
    
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   843
lemma rbl_mult_gt1: 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   844
  "m >= length bl ==> rbl_mult bl (rev (bin_to_bl m binb)) = 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   845
    rbl_mult bl (rev (bin_to_bl (length bl) binb))"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   846
  apply (rule trans)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   847
   apply (rule rbl_mult_take2 [symmetric])
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   848
   apply simp_all
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   849
  apply (rule_tac f = "rbl_mult bl" in arg_cong) 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   850
  apply (rule rev_swap [THEN iffD1])
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   851
  apply (simp add: rev_take drop_bin2bl)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   852
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   853
    
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   854
lemma rbl_mult_gt: 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   855
  "m > n ==> rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl m binb)) = 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   856
    rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb))"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   857
  by (auto intro: trans [OF rbl_mult_gt1])
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   858
  
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   859
lemmas rbl_mult_Suc = lessI [THEN rbl_mult_gt]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   860
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   861
lemma rbbl_Cons: 
37654
8e33b9d04a82 use existing bit type from theory Bit
haftmann
parents: 32642
diff changeset
   862
  "b # rev (bin_to_bl n x) = rev (bin_to_bl (Suc n) (x BIT If b 1 0))"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   863
  apply (unfold bin_to_bl_def)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   864
  apply simp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   865
  apply (simp add: bin_to_bl_aux_alt)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   866
  done
46653
a557db8f2fbf avoid using BIT_simps in proofs;
huffman
parents: 46652
diff changeset
   867
a557db8f2fbf avoid using BIT_simps in proofs;
huffman
parents: 46652
diff changeset
   868
lemma mult_BIT_simps [simp]:
a557db8f2fbf avoid using BIT_simps in proofs;
huffman
parents: 46652
diff changeset
   869
  "x BIT 0 * y = (x * y) BIT 0"
a557db8f2fbf avoid using BIT_simps in proofs;
huffman
parents: 46652
diff changeset
   870
  "x * y BIT 0 = (x * y) BIT 0"
a557db8f2fbf avoid using BIT_simps in proofs;
huffman
parents: 46652
diff changeset
   871
  "x BIT 1 * y = (x * y) BIT 0 + y"
a557db8f2fbf avoid using BIT_simps in proofs;
huffman
parents: 46652
diff changeset
   872
  by (simp_all add: Bit_B0_2t Bit_B1_2t algebra_simps)
a557db8f2fbf avoid using BIT_simps in proofs;
huffman
parents: 46652
diff changeset
   873
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   874
lemma rbl_mult: "!!bina binb. 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   875
    rbl_mult (rev (bin_to_bl n bina)) (rev (bin_to_bl n binb)) = 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   876
    rev (bin_to_bl n (bina * binb))"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   877
  apply (induct n)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   878
   apply simp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   879
  apply (unfold bin_to_bl_def)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   880
  apply clarsimp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   881
  apply (case_tac bina rule: bin_exhaust)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   882
  apply (case_tac binb rule: bin_exhaust)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   883
  apply (case_tac b)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   884
   apply (case_tac [!] "ba")
46653
a557db8f2fbf avoid using BIT_simps in proofs;
huffman
parents: 46652
diff changeset
   885
     apply (auto simp: bin_to_bl_aux_alt Let_def)
a557db8f2fbf avoid using BIT_simps in proofs;
huffman
parents: 46652
diff changeset
   886
     apply (auto simp: rbbl_Cons rbl_mult_Suc rbl_add)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   887
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   888
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   889
lemma rbl_add_split: 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   890
  "P (rbl_add (y # ys) (x # xs)) = 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   891
    (ALL ws. length ws = length ys --> ws = rbl_add ys xs --> 
26008
24c82bef5696 eliminated escaped white space;
wenzelm
parents: 25919
diff changeset
   892
    (y --> ((x --> P (False # rbl_succ ws)) & (~ x -->  P (True # ws)))) &
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   893
    (~ y --> P (x # ws)))"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   894
  apply (auto simp add: Let_def)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   895
   apply (case_tac [!] "y")
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   896
     apply auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   897
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   898
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   899
lemma rbl_mult_split: 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   900
  "P (rbl_mult (y # ys) xs) = 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   901
    (ALL ws. length ws = Suc (length ys) --> ws = False # rbl_mult ys xs --> 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   902
    (y --> P (rbl_add ws xs)) & (~ y -->  P ws))"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   903
  by (clarsimp simp add : Let_def)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   904
  
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   905
lemma and_len: "xs = ys ==> xs = ys & length xs = length ys"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   906
  by auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   907
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   908
lemma size_if: "size (if p then xs else ys) = (if p then size xs else size ys)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   909
  by auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   910
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   911
lemma tl_if: "tl (if p then xs else ys) = (if p then tl xs else tl ys)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   912
  by auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   913
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   914
lemma hd_if: "hd (if p then xs else ys) = (if p then hd xs else hd ys)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   915
  by auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   916
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   917
lemma if_Not_x: "(if p then ~ x else x) = (p = (~ x))"
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   918
  by auto
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   919
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   920
lemma if_x_Not: "(if p then x else ~ x) = (p = x)"
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   921
  by auto
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   922
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   923
lemma if_same_and: "(If p x y & If p u v) = (if p then x & u else y & v)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   924
  by auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   925
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   926
lemma if_same_eq: "(If p x y  = (If p u v)) = (if p then x = (u) else y = (v))"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   927
  by auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   928
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   929
lemma if_same_eq_not:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   930
  "(If p x y  = (~ If p u v)) = (if p then x = (~u) else y = (~v))"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   931
  by auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   932
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   933
(* note - if_Cons can cause blowup in the size, if p is complex,
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   934
  so make a simproc *)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   935
lemma if_Cons: "(if p then x # xs else y # ys) = If p x y # If p xs ys"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   936
  by auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   937
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   938
lemma if_single:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   939
  "(if xc then [xab] else [an]) = [if xc then xab else an]"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   940
  by auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   941
24465
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   942
lemma if_bool_simps:
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   943
  "If p True y = (p | y) & If p False y = (~p & y) & 
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   944
    If p y True = (p --> y) & If p y False = (p & y)"
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   945
  by auto
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   946
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   947
lemmas if_simps = if_x_Not if_Not_x if_cancel if_True if_False if_bool_simps
70f0214b3ecc revert to Word library version from 2007/08/20
huffman
parents: 24399
diff changeset
   948
45854
40554613b4f0 replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents: 45847
diff changeset
   949
lemmas seqr = eq_reflection [where x = "size w"] for w (* FIXME: delete *)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   950
45854
40554613b4f0 replace many uses of 'lemmas' with explicit 'lemma'
huffman
parents: 45847
diff changeset
   951
(* TODO: move name bindings to List.thy *)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   952
lemmas tl_Nil = tl.simps (1)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   953
lemmas tl_Cons = tl.simps (2)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   954
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   955
24350
4d74f37c6367 headers for document generation
huffman
parents: 24333
diff changeset
   956
subsection "Repeated splitting or concatenation"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   957
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   958
lemma sclem:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   959
  "size (concat (map (bin_to_bl n) xs)) = length xs * n"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   960
  by (induct xs) auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   961
45997
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   962
lemma bin_cat_foldl_lem:
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   963
  "foldl (%u. bin_cat u n) x xs = 
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   964
    bin_cat x (size xs * n) (foldl (%u. bin_cat u n) y xs)"
45997
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   965
  apply (induct xs arbitrary: x)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   966
   apply simp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   967
  apply (simp (no_asm))
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   968
  apply (frule asm_rl)
45997
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   969
  apply (drule meta_spec)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   970
  apply (erule trans)
45997
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
   971
  apply (drule_tac x = "bin_cat y n a" in meta_spec)
32642
026e7c6a6d08 be more cautious wrt. simp rules: inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp rules by default any longer
haftmann
parents: 32439
diff changeset
   972
  apply (simp add : bin_cat_assoc_sym min_max.inf_absorb2)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   973
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   974
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   975
lemma bin_rcat_bl:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   976
  "(bin_rcat n wl) = bl_to_bin (concat (map (bin_to_bl n) wl))"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   977
  apply (unfold bin_rcat_def)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   978
  apply (rule sym)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   979
  apply (induct wl)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   980
   apply (auto simp add : bl_to_bin_append)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   981
  apply (simp add : bl_to_bin_aux_alt sclem)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   982
  apply (simp add : bin_cat_foldl_lem [symmetric])
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   983
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   984
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   985
lemmas bin_rsplit_aux_simps = bin_rsplit_aux.simps bin_rsplitl_aux.simps
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   986
lemmas rsplit_aux_simps = bin_rsplit_aux_simps
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   987
45604
29cf40fe8daf eliminated obsolete "standard";
wenzelm
parents: 45543
diff changeset
   988
lemmas th_if_simp1 = split_if [where P = "op = l", THEN iffD1, THEN conjunct1, THEN mp] for l
29cf40fe8daf eliminated obsolete "standard";
wenzelm
parents: 45543
diff changeset
   989
lemmas th_if_simp2 = split_if [where P = "op = l", THEN iffD1, THEN conjunct2, THEN mp] for l
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   990
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   991
lemmas rsplit_aux_simp1s = rsplit_aux_simps [THEN th_if_simp1]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   992
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   993
lemmas rsplit_aux_simp2ls = rsplit_aux_simps [THEN th_if_simp2]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   994
(* these safe to [simp add] as require calculating m - n *)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   995
lemmas bin_rsplit_aux_simp2s [simp] = rsplit_aux_simp2ls [unfolded Let_def]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   996
lemmas rbscl = bin_rsplit_aux_simp2s (2)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   997
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   998
lemmas rsplit_aux_0_simps [simp] = 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   999
  rsplit_aux_simp1s [OF disjI1] rsplit_aux_simp1s [OF disjI2]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1000
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1001
lemma bin_rsplit_aux_append:
26557
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
  1002
  "bin_rsplit_aux n m c (bs @ cs) = bin_rsplit_aux n m c bs @ cs"
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
  1003
  apply (induct n m c bs rule: bin_rsplit_aux.induct)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1004
  apply (subst bin_rsplit_aux.simps)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1005
  apply (subst bin_rsplit_aux.simps)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1006
  apply (clarsimp split: ls_splits)
26557
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
  1007
  apply auto
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1008
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1009
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1010
lemma bin_rsplitl_aux_append:
26557
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
  1011
  "bin_rsplitl_aux n m c (bs @ cs) = bin_rsplitl_aux n m c bs @ cs"
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
  1012
  apply (induct n m c bs rule: bin_rsplitl_aux.induct)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1013
  apply (subst bin_rsplitl_aux.simps)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1014
  apply (subst bin_rsplitl_aux.simps)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1015
  apply (clarsimp split: ls_splits)
26557
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
  1016
  apply auto
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1017
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1018
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1019
lemmas rsplit_aux_apps [where bs = "[]"] =
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1020
  bin_rsplit_aux_append bin_rsplitl_aux_append
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1021
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1022
lemmas rsplit_def_auxs = bin_rsplit_def bin_rsplitl_def
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1023
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1024
lemmas rsplit_aux_alts = rsplit_aux_apps 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1025
  [unfolded append_Nil rsplit_def_auxs [symmetric]]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1026
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1027
lemma bin_split_minus: "0 < n ==> bin_split (Suc (n - 1)) w = bin_split n w"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1028
  by auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1029
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1030
lemmas bin_split_minus_simp =
45604
29cf40fe8daf eliminated obsolete "standard";
wenzelm
parents: 45543
diff changeset
  1031
  bin_split.Suc [THEN [2] bin_split_minus [symmetric, THEN trans]]
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1032
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1033
lemma bin_split_pred_simp [simp]: 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1034
  "(0::nat) < number_of bin \<Longrightarrow>
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1035
  bin_split (number_of bin) w =
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents: 25350
diff changeset
  1036
  (let (w1, w2) = bin_split (number_of (Int.pred bin)) (bin_rest w)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1037
   in (w1, w2 BIT bin_last w))" 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1038
  by (simp only: nobm1 bin_split_minus_simp)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1039
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1040
lemma bin_rsplit_aux_simp_alt:
26557
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
  1041
  "bin_rsplit_aux n m c bs =
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1042
   (if m = 0 \<or> n = 0 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1043
   then bs
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1044
   else let (a, b) = bin_split n c in bin_rsplit n (m - n, a) @ b # bs)"
26557
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
  1045
  unfolding bin_rsplit_aux.simps [of n m c bs]
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
  1046
  apply simp
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
  1047
  apply (subst rsplit_aux_alts)
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
  1048
  apply (simp add: bin_rsplit_def)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1049
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1050
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1051
lemmas bin_rsplit_simp_alt = 
45604
29cf40fe8daf eliminated obsolete "standard";
wenzelm
parents: 45543
diff changeset
  1052
  trans [OF bin_rsplit_def bin_rsplit_aux_simp_alt]
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1053
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1054
lemmas bthrs = bin_rsplit_simp_alt [THEN [2] trans]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1055
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1056
lemma bin_rsplit_size_sign' [rule_format] : 
45997
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
  1057
  "\<lbrakk>n > 0; rev sw = bin_rsplit n (nw, w)\<rbrakk> \<Longrightarrow> 
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
  1058
    (ALL v: set sw. bintrunc n v = v)"
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
  1059
  apply (induct sw arbitrary: nw w v)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1060
   apply clarsimp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1061
  apply clarsimp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1062
  apply (drule bthrs)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1063
  apply (simp (no_asm_use) add: Let_def split: ls_splits)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1064
  apply clarify
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1065
  apply (drule split_bintrunc)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1066
  apply simp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1067
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1068
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1069
lemmas bin_rsplit_size_sign = bin_rsplit_size_sign' [OF asm_rl 
45604
29cf40fe8daf eliminated obsolete "standard";
wenzelm
parents: 45543
diff changeset
  1070
  rev_rev_ident [THEN trans] set_rev [THEN equalityD2 [THEN subsetD]]]
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1071
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1072
lemma bin_nth_rsplit [rule_format] :
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1073
  "n > 0 ==> m < n ==> (ALL w k nw. rev sw = bin_rsplit n (nw, w) --> 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1074
       k < size sw --> bin_nth (sw ! k) m = bin_nth w (k * n + m))"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1075
  apply (induct sw)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1076
   apply clarsimp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1077
  apply clarsimp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1078
  apply (drule bthrs)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1079
  apply (simp (no_asm_use) add: Let_def split: ls_splits)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1080
  apply clarify
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1081
  apply (erule allE, erule impE, erule exI)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1082
  apply (case_tac k)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1083
   apply clarsimp   
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1084
   prefer 2
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1085
   apply clarsimp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1086
   apply (erule allE)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1087
   apply (erule (1) impE)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1088
   apply (drule bin_nth_split, erule conjE, erule allE,
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1089
          erule trans, simp add : add_ac)+
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1090
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1091
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1092
lemma bin_rsplit_all:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1093
  "0 < nw ==> nw <= n ==> bin_rsplit n (nw, w) = [bintrunc n w]"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1094
  unfolding bin_rsplit_def
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1095
  by (clarsimp dest!: split_bintrunc simp: rsplit_aux_simp2ls split: ls_splits)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1096
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1097
lemma bin_rsplit_l [rule_format] :
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1098
  "ALL bin. bin_rsplitl n (m, bin) = bin_rsplit n (m, bintrunc m bin)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1099
  apply (rule_tac a = "m" in wf_less_than [THEN wf_induct])
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1100
  apply (simp (no_asm) add : bin_rsplitl_def bin_rsplit_def)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1101
  apply (rule allI)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1102
  apply (subst bin_rsplitl_aux.simps)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1103
  apply (subst bin_rsplit_aux.simps)
26557
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
  1104
  apply (clarsimp simp: Let_def split: ls_splits)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1105
  apply (drule bin_split_trunc)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1106
  apply (drule sym [THEN trans], assumption)
26557
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
  1107
  apply (subst rsplit_aux_alts(1))
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
  1108
  apply (subst rsplit_aux_alts(2))
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
  1109
  apply clarsimp
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
  1110
  unfolding bin_rsplit_def bin_rsplitl_def
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
  1111
  apply simp
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1112
  done
26557
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
  1113
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1114
lemma bin_rsplit_rcat [rule_format] :
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1115
  "n > 0 --> bin_rsplit n (n * size ws, bin_rcat n ws) = map (bintrunc n) ws"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1116
  apply (unfold bin_rsplit_def bin_rcat_def)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1117
  apply (rule_tac xs = "ws" in rev_induct)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1118
   apply clarsimp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1119
  apply clarsimp
26557
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
  1120
  apply (subst rsplit_aux_alts)
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
  1121
  unfolding bin_split_cat
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
  1122
  apply simp
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1123
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1124
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1125
lemma bin_rsplit_aux_len_le [rule_format] :
26557
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
  1126
  "\<forall>ws m. n \<noteq> 0 \<longrightarrow> ws = bin_rsplit_aux n nw w bs \<longrightarrow>
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
  1127
    length ws \<le> m \<longleftrightarrow> nw + length bs * n \<le> m * n"
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
  1128
  apply (induct n nw w bs rule: bin_rsplit_aux.induct)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1129
  apply (subst bin_rsplit_aux.simps)
26557
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
  1130
  apply (simp add: lrlem Let_def split: ls_splits)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1131
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1132
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1133
lemma bin_rsplit_len_le: 
25134
3d4953e88449 Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents: 25112
diff changeset
  1134
  "n \<noteq> 0 --> ws = bin_rsplit n (nw, w) --> (length ws <= m) = (nw <= m * n)"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1135
  unfolding bin_rsplit_def by (clarsimp simp add : bin_rsplit_aux_len_le)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1136
 
45997
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
  1137
lemma bin_rsplit_aux_len:
13392893ea12 use 'induct arbitrary' instead of 'rule_format' attribute
huffman
parents: 45996
diff changeset
  1138
  "n \<noteq> 0 \<Longrightarrow> length (bin_rsplit_aux n nw w cs) =
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1139
    (nw + n - 1) div n + length cs"
26557
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
  1140
  apply (induct n nw w cs rule: bin_rsplit_aux.induct)
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1141
  apply (subst bin_rsplit_aux.simps)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1142
  apply (clarsimp simp: Let_def split: ls_splits)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1143
  apply (erule thin_rl)
27651
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27105
diff changeset
  1144
  apply (case_tac m)
16a26996c30e moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
haftmann
parents: 27105
diff changeset
  1145
  apply simp
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1146
  apply (case_tac "m <= n")
27677
646ea25ff59d (re-)added simp rules for (_ + _) div/mod _
haftmann
parents: 27651
diff changeset
  1147
  apply auto
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1148
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1149
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1150
lemma bin_rsplit_len: 
25134
3d4953e88449 Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents: 25112
diff changeset
  1151
  "n\<noteq>0 ==> length (bin_rsplit n (nw, w)) = (nw + n - 1) div n"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1152
  unfolding bin_rsplit_def by (clarsimp simp add : bin_rsplit_aux_len)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1153
26557
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
  1154
lemma bin_rsplit_aux_len_indep:
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
  1155
  "n \<noteq> 0 \<Longrightarrow> length bs = length cs \<Longrightarrow>
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
  1156
    length (bin_rsplit_aux n nw v bs) =
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
  1157
    length (bin_rsplit_aux n nw w cs)"
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
  1158
proof (induct n nw w cs arbitrary: v bs rule: bin_rsplit_aux.induct)
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
  1159
  case (1 n m w cs v bs) show ?case
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
  1160
  proof (cases "m = 0")
28298
3eb2855e5402 avoid using implicit assumptions
huffman
parents: 28059
diff changeset
  1161
    case True then show ?thesis using `length bs = length cs` by simp
26557
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
  1162
  next
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
  1163
    case False
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
  1164
    from "1.hyps" `m \<noteq> 0` `n \<noteq> 0` have hyp: "\<And>v bs. length bs = Suc (length cs) \<Longrightarrow>
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
  1165
      length (bin_rsplit_aux n (m - n) v bs) =
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
  1166
      length (bin_rsplit_aux n (m - n) (fst (bin_split n w)) (snd (bin_split n w) # cs))"
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
  1167
    by auto
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
  1168
    show ?thesis using `length bs = length cs` `n \<noteq> 0`
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
  1169
      by (auto simp add: bin_rsplit_aux_simp_alt Let_def bin_rsplit_len
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
  1170
        split: ls_splits)
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
  1171
  qed
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
  1172
qed
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1173
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1174
lemma bin_rsplit_len_indep: 
25134
3d4953e88449 Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents: 25112
diff changeset
  1175
  "n\<noteq>0 ==> length (bin_rsplit n (nw, v)) = length (bin_rsplit n (nw, w))"
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1176
  apply (unfold bin_rsplit_def)
26557
9e7f95903b24 more new primrec
haftmann
parents: 26086
diff changeset
  1177
  apply (simp (no_asm))
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1178
  apply (erule bin_rsplit_aux_len_indep)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1179
  apply (rule refl)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1180
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1181
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
  1182
end