src/HOL/Word/BinGeneral.thy
author kleing
Mon, 20 Aug 2007 04:34:31 +0200
changeset 24333 e77ea0ea7f2c
child 24350 4d74f37c6367
permissions -rw-r--r--
* HOL-Word: New extensive library and type for generic, fixed size machine words, with arithemtic, bit-wise, shifting and rotating operations, reflection into int, nat, and bool lists, automation for linear arithmetic (by automatic reflection into nat or int), including lemmas on overflow and monotonicity. Instantiated to all appropriate arithmetic type classes, supporting automatic simplification of numerals on all operations. Jointly developed by NICTA, Galois, and PSU. * still to do: README.html/document + moving some of the generic lemmas to appropriate place in distribution
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
  ID:     $Id$
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
     3
  Author: Jeremy Dawson, NICTA
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
     4
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
     5
  contains basic definition to do with integers
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
     6
  expressed using Pls, Min, BIT and important resulting theorems, 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
     7
  in particular, bin_rec and related work
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
     8
*) 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
     9
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    10
theory BinGeneral imports TdThs Num_Lemmas
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    11
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    12
begin
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    13
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    14
lemma brlem: "(bin = Numeral.Min) = (- bin + Numeral.pred 0 = 0)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    15
  unfolding Min_def pred_def by arith
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    16
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    17
function
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    18
  bin_rec' :: "int * 'a * 'a * (int => bit => 'a => 'a) => 'a"  
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    19
  where 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    20
  "bin_rec' (bin, f1, f2, f3) = (if bin = Numeral.Pls then f1 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    21
    else if bin = Numeral.Min then f2
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    22
    else case bin_rl bin of (w, b) => f3 w b (bin_rec' (w, f1, f2, f3)))"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    23
  by pat_completeness auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    24
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    25
termination 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    26
  apply (relation "measure (nat o abs o fst)")
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    27
   apply simp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    28
  apply (simp add: Pls_def brlem)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    29
  apply (clarsimp simp: bin_rl_char pred_def)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    30
  apply (frule thin_rl [THEN refl [THEN bin_abs_lem [rule_format]]]) 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    31
    apply (unfold Pls_def Min_def number_of_eq)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    32
    prefer 2
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    33
    apply (erule asm_rl)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    34
   apply auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    35
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    36
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    37
constdefs
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    38
  bin_rec :: "'a => 'a => (int => bit => 'a => 'a) => int => 'a"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    39
  "bin_rec f1 f2 f3 bin == bin_rec' (bin, f1, f2, f3)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    40
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    41
consts
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    42
  -- "corresponding operations analysing bins"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    43
  bin_last :: "int => bit"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    44
  bin_rest :: "int => int"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    45
  bin_sign :: "int => int"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    46
  bin_nth :: "int => nat => bool"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    47
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    48
primrec
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    49
  Z : "bin_nth w 0 = (bin_last w = bit.B1)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    50
  Suc : "bin_nth w (Suc n) = bin_nth (bin_rest w) n"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    51
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    52
defs  
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    53
  bin_rest_def : "bin_rest w == fst (bin_rl w)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    54
  bin_last_def : "bin_last w == snd (bin_rl w)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    55
  bin_sign_def : "bin_sign == bin_rec Numeral.Pls Numeral.Min (%w b s. s)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    56
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    57
consts
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    58
  bintrunc :: "nat => int => int"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    59
primrec 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    60
  Z : "bintrunc 0 bin = Numeral.Pls"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    61
  Suc : "bintrunc (Suc n) bin = bintrunc n (bin_rest bin) BIT (bin_last bin)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    62
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    63
consts
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    64
  sbintrunc :: "nat => int => int" 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    65
primrec 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    66
  Z : "sbintrunc 0 bin = 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    67
    (case bin_last bin of bit.B1 => Numeral.Min | bit.B0 => Numeral.Pls)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    68
  Suc : "sbintrunc (Suc n) bin = sbintrunc n (bin_rest bin) BIT (bin_last bin)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    69
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    70
consts
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    71
  bin_split :: "nat => int => int * int"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    72
primrec
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    73
  Z : "bin_split 0 w = (w, Numeral.Pls)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    74
  Suc : "bin_split (Suc n) w = (let (w1, w2) = bin_split n (bin_rest w)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    75
    in (w1, w2 BIT bin_last w))"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    76
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    77
consts
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    78
  bin_cat :: "int => nat => int => int"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    79
primrec
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    80
  Z : "bin_cat w 0 v = w"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    81
  Suc : "bin_cat w (Suc n) v = bin_cat w n (bin_rest v) BIT bin_last v"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    82
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    83
lemmas funpow_minus_simp = 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    84
  trans [OF gen_minus [where f = "power f"] funpow_Suc, standard]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    85
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    86
lemmas funpow_pred_simp [simp] =
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    87
  funpow_minus_simp [of "number_of bin", simplified nobm1, standard]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    88
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    89
lemmas replicate_minus_simp = 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    90
  trans [OF gen_minus [where f = "%n. replicate n x"] replicate.replicate_Suc,
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    91
         standard]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    92
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    93
lemmas replicate_pred_simp [simp] =
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    94
  replicate_minus_simp [of "number_of bin", simplified nobm1, standard]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    95
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    96
lemmas power_Suc_no [simp] = power_Suc [of "number_of ?a"]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    97
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    98
lemmas power_minus_simp = 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
    99
  trans [OF gen_minus [where f = "power f"] power_Suc, standard]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   100
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   101
lemmas power_pred_simp = 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   102
  power_minus_simp [of "number_of bin", simplified nobm1, standard]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   103
lemmas power_pred_simp_no [simp] = power_pred_simp [where f= "number_of ?f"]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   104
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   105
lemma bin_rl: "bin_rl w = (bin_rest w, bin_last w)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   106
  unfolding bin_rest_def bin_last_def by auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   107
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   108
lemmas bin_rl_simp [simp] = iffD1 [OF bin_rl_char bin_rl]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   109
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   110
lemma bin_rec_PM:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   111
  "f = bin_rec f1 f2 f3 ==> f Numeral.Pls = f1 & f Numeral.Min = f2"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   112
  apply safe
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   113
   apply (unfold bin_rec_def)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   114
   apply (auto intro: bin_rec'.simps [THEN trans])
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   115
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   116
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   117
lemmas bin_rec_Pls = refl [THEN bin_rec_PM, THEN conjunct1, standard]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   118
lemmas bin_rec_Min = refl [THEN bin_rec_PM, THEN conjunct2, standard]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   119
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   120
lemma bin_rec_Bit:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   121
  "f = bin_rec f1 f2 f3  ==> f3 Numeral.Pls bit.B0 f1 = f1 ==> 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   122
    f3 Numeral.Min bit.B1 f2 = f2 ==> f (w BIT b) = f3 w b (f w)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   123
  apply clarify
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   124
  apply (unfold bin_rec_def)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   125
  apply (rule bin_rec'.simps [THEN trans])
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   126
  apply auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   127
       apply (unfold Pls_def Min_def Bit_def)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   128
       apply (cases b, auto)+
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   129
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   130
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   131
lemmas bin_rec_simps = refl [THEN bin_rec_Bit] bin_rec_Pls bin_rec_Min
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   132
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   133
lemma bin_rest_simps [simp]: 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   134
  "bin_rest Numeral.Pls = Numeral.Pls"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   135
  "bin_rest Numeral.Min = Numeral.Min"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   136
  "bin_rest (w BIT b) = w"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   137
  unfolding bin_rest_def by auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   138
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   139
lemma bin_last_simps [simp]: 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   140
  "bin_last Numeral.Pls = bit.B0"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   141
  "bin_last Numeral.Min = bit.B1"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   142
  "bin_last (w BIT b) = b"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   143
  unfolding bin_last_def by auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   144
    
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   145
lemma bin_sign_simps [simp]:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   146
  "bin_sign Numeral.Pls = Numeral.Pls"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   147
  "bin_sign Numeral.Min = Numeral.Min"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   148
  "bin_sign (w BIT b) = bin_sign w"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   149
  unfolding bin_sign_def by (auto simp: bin_rec_simps)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   150
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   151
lemma bin_r_l_extras [simp]:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   152
  "bin_last 0 = bit.B0"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   153
  "bin_last (- 1) = bit.B1"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   154
  "bin_last -1 = bit.B1"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   155
  "bin_last 1 = bit.B1"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   156
  "bin_rest 1 = 0"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   157
  "bin_rest 0 = 0"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   158
  "bin_rest (- 1) = - 1"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   159
  "bin_rest -1 = -1"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   160
  apply (unfold number_of_Min)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   161
  apply (unfold Pls_def [symmetric] Min_def [symmetric])
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   162
  apply (unfold numeral_1_eq_1 [symmetric])
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   163
  apply (auto simp: number_of_eq) 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   164
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   165
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   166
lemma bin_last_mod: 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   167
  "bin_last w = (if w mod 2 = 0 then bit.B0 else bit.B1)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   168
  apply (case_tac w rule: bin_exhaust)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   169
  apply (case_tac b)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   170
   apply auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   171
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   172
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   173
lemma bin_rest_div: 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   174
  "bin_rest w = w div 2"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   175
  apply (case_tac w rule: bin_exhaust)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   176
  apply (rule trans)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   177
   apply clarsimp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   178
   apply (rule refl)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   179
  apply (drule trans)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   180
   apply (rule Bit_def)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   181
  apply (simp add: z1pdiv2 split: bit.split)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   182
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   183
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   184
lemma Bit_div2 [simp]: "(w BIT b) div 2 = w"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   185
  unfolding bin_rest_div [symmetric] by auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   186
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   187
lemma bin_nth_lem [rule_format]:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   188
  "ALL y. bin_nth x = bin_nth y --> x = y"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   189
  apply (induct x rule: bin_induct)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   190
    apply safe
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   191
    apply (erule rev_mp)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   192
    apply (induct_tac y rule: bin_induct)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   193
      apply safe
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   194
      apply (drule_tac x=0 in fun_cong, force)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   195
     apply (erule notE, rule ext, 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   196
            drule_tac x="Suc x" in fun_cong, force)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   197
    apply (drule_tac x=0 in fun_cong, force)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   198
   apply (erule rev_mp)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   199
   apply (induct_tac y rule: bin_induct)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   200
     apply safe
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   201
     apply (drule_tac x=0 in fun_cong, force)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   202
    apply (erule notE, rule ext, 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   203
           drule_tac x="Suc x" in fun_cong, force)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   204
   apply (drule_tac x=0 in fun_cong, force)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   205
  apply (case_tac y rule: bin_exhaust)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   206
  apply clarify
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   207
  apply (erule allE)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   208
  apply (erule impE)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   209
   prefer 2
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   210
   apply (erule BIT_eqI)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   211
   apply (drule_tac x=0 in fun_cong, force)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   212
  apply (rule ext)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   213
  apply (drule_tac x="Suc ?x" in fun_cong, force)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   214
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   215
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   216
lemma bin_nth_eq_iff: "(bin_nth x = bin_nth y) = (x = y)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   217
  by (auto elim: bin_nth_lem)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   218
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   219
lemmas bin_eqI = ext [THEN bin_nth_eq_iff [THEN iffD1], standard]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   220
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   221
lemma bin_nth_Pls [simp]: "~ bin_nth Numeral.Pls n"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   222
  by (induct n) auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   223
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   224
lemma bin_nth_Min [simp]: "bin_nth Numeral.Min n"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   225
  by (induct n) auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   226
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   227
lemma bin_nth_0_BIT: "bin_nth (w BIT b) 0 = (b = bit.B1)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   228
  by auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   229
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   230
lemma bin_nth_Suc_BIT: "bin_nth (w BIT b) (Suc n) = bin_nth w n"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   231
  by auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   232
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   233
lemma bin_nth_minus [simp]: "0 < n ==> bin_nth (w BIT b) n = bin_nth w (n - 1)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   234
  by (cases n) auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   235
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   236
lemmas bin_nth_0 = bin_nth.simps(1)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   237
lemmas bin_nth_Suc = bin_nth.simps(2)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   238
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   239
lemmas bin_nth_simps = 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   240
  bin_nth_0 bin_nth_Suc bin_nth_Pls bin_nth_Min bin_nth_minus
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   241
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   242
lemma sign_bintr:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   243
  "!!w. bin_sign (bintrunc n w) = Numeral.Pls"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   244
  by (induct n) auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   245
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   246
lemma bin_sign_rest [simp]: 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   247
  "bin_sign (bin_rest w) = (bin_sign w)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   248
  by (case_tac w rule: bin_exhaust) auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   249
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   250
lemma bintrunc_mod2p:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   251
  "!!w. bintrunc n w = (w mod 2 ^ n :: int)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   252
  apply (induct n, clarsimp)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   253
  apply (simp add: bin_last_mod bin_rest_div Bit_def zmod_zmult2_eq
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   254
              cong: number_of_False_cong)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   255
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   256
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   257
lemma sbintrunc_mod2p:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   258
  "!!w. sbintrunc n w = ((w + 2 ^ n) mod 2 ^ (Suc n) - 2 ^ n :: int)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   259
  apply (induct n)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   260
   apply clarsimp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   261
   apply (subst zmod_zadd_left_eq)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   262
   apply (simp add: bin_last_mod)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   263
   apply (simp add: number_of_eq)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   264
  apply clarsimp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   265
  apply (simp add: bin_last_mod bin_rest_div Bit_def 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   266
              cong: number_of_False_cong)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   267
  apply (clarsimp simp: zmod_zmult_zmult1 [symmetric] 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   268
         zmod_zdiv_equality [THEN diff_eq_eq [THEN iffD2 [THEN sym]]])
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   269
  apply (rule trans [symmetric, OF _ emep1])
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   270
     apply auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   271
  apply (auto simp: even_def)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   272
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   273
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   274
lemmas m2pths [OF zless2p, standard] = pos_mod_sign pos_mod_bound
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   275
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   276
lemma list_exhaust_size_gt0:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   277
  assumes y: "\<And>a list. y = a # list \<Longrightarrow> P"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   278
  shows "0 < length y \<Longrightarrow> P"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   279
  apply (cases y, simp)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   280
  apply (rule y)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   281
  apply fastsimp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   282
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   283
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   284
lemma list_exhaust_size_eq0:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   285
  assumes y: "y = [] \<Longrightarrow> P"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   286
  shows "length y = 0 \<Longrightarrow> P"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   287
  apply (cases y)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   288
   apply (rule y, simp)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   289
  apply simp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   290
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   291
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   292
lemma size_Cons_lem_eq:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   293
  "y = xa # list ==> size y = Suc k ==> size list = k"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   294
  by auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   295
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   296
lemma size_Cons_lem_eq_bin:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   297
  "y = xa # list ==> size y = number_of (Numeral.succ k) ==> 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   298
    size list = number_of k"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   299
  by (auto simp: pred_def succ_def split add : split_if_asm)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   300
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   301
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   302
section "Simplifications for (s)bintrunc"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   303
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   304
lemma bit_bool:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   305
  "(b = (b' = bit.B1)) = (b' = (if b then bit.B1 else bit.B0))"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   306
  by (cases b') auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   307
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   308
lemmas bit_bool1 [simp] = refl [THEN bit_bool [THEN iffD1], symmetric]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   309
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   310
lemma bin_sign_lem:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   311
  "!!bin. (bin_sign (sbintrunc n bin) = Numeral.Min) = bin_nth bin n"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   312
  apply (induct n)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   313
   apply (case_tac bin rule: bin_exhaust, case_tac b, auto)+
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   314
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   315
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   316
lemma nth_bintr:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   317
  "!!w m. bin_nth (bintrunc m w) n = (n < m & bin_nth w n)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   318
  apply (induct n)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   319
   apply (case_tac m, auto)[1]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   320
  apply (case_tac m, auto)[1]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   321
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   322
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   323
lemma nth_sbintr:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   324
  "!!w m. bin_nth (sbintrunc m w) n = 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   325
          (if n < m then bin_nth w n else bin_nth w m)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   326
  apply (induct n)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   327
   apply (case_tac m, simp_all split: bit.splits)[1]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   328
  apply (case_tac m, simp_all split: bit.splits)[1]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   329
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   330
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   331
lemma bin_nth_Bit:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   332
  "bin_nth (w BIT b) n = (n = 0 & b = bit.B1 | (EX m. n = Suc m & bin_nth w m))"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   333
  by (cases n) auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   334
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   335
lemma bintrunc_bintrunc_l:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   336
  "n <= m ==> (bintrunc m (bintrunc n w) = bintrunc n w)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   337
  by (rule bin_eqI) (auto simp add : nth_bintr)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   338
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   339
lemma sbintrunc_sbintrunc_l:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   340
  "n <= m ==> (sbintrunc m (sbintrunc n w) = sbintrunc n w)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   341
  by (rule bin_eqI) (auto simp: nth_sbintr min_def)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   342
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   343
lemma bintrunc_bintrunc_ge:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   344
  "n <= m ==> (bintrunc n (bintrunc m w) = bintrunc n w)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   345
  by (rule bin_eqI) (auto simp: nth_bintr)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   346
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   347
lemma bintrunc_bintrunc_min [simp]:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   348
  "bintrunc m (bintrunc n w) = bintrunc (min m n) w"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   349
  apply (unfold min_def)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   350
  apply (rule bin_eqI)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   351
  apply (auto simp: nth_bintr)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   352
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   353
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   354
lemma sbintrunc_sbintrunc_min [simp]:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   355
  "sbintrunc m (sbintrunc n w) = sbintrunc (min m n) w"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   356
  apply (unfold min_def)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   357
  apply (rule bin_eqI)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   358
  apply (auto simp: nth_sbintr)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   359
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   360
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   361
lemmas bintrunc_Pls = 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   362
  bintrunc.Suc [where bin="Numeral.Pls", simplified bin_last_simps bin_rest_simps]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   363
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   364
lemmas bintrunc_Min [simp] = 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   365
  bintrunc.Suc [where bin="Numeral.Min", simplified bin_last_simps bin_rest_simps]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   366
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   367
lemmas bintrunc_BIT  [simp] = 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   368
  bintrunc.Suc [where bin="?w BIT ?b", simplified bin_last_simps bin_rest_simps]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   369
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   370
lemmas bintrunc_Sucs = bintrunc_Pls bintrunc_Min bintrunc_BIT
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   371
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   372
lemmas sbintrunc_Suc_Pls = 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   373
  sbintrunc.Suc [where bin="Numeral.Pls", simplified bin_last_simps bin_rest_simps]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   374
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   375
lemmas sbintrunc_Suc_Min = 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   376
  sbintrunc.Suc [where bin="Numeral.Min", simplified bin_last_simps bin_rest_simps]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   377
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   378
lemmas sbintrunc_Suc_BIT [simp] = 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   379
  sbintrunc.Suc [where bin="?w BIT ?b", simplified bin_last_simps bin_rest_simps]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   380
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   381
lemmas sbintrunc_Sucs = sbintrunc_Suc_Pls sbintrunc_Suc_Min sbintrunc_Suc_BIT
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   382
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   383
lemmas sbintrunc_Pls = 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   384
  sbintrunc.Z [where bin="Numeral.Pls", 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   385
               simplified bin_last_simps bin_rest_simps bit.simps]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   386
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   387
lemmas sbintrunc_Min = 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   388
  sbintrunc.Z [where bin="Numeral.Min", 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   389
               simplified bin_last_simps bin_rest_simps bit.simps]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   390
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   391
lemmas sbintrunc_0_BIT_B0 [simp] = 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   392
  sbintrunc.Z [where bin="?w BIT bit.B0", 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   393
               simplified bin_last_simps bin_rest_simps bit.simps]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   394
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   395
lemmas sbintrunc_0_BIT_B1 [simp] = 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   396
  sbintrunc.Z [where bin="?w BIT bit.B1", 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   397
               simplified bin_last_simps bin_rest_simps bit.simps]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   398
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   399
lemmas sbintrunc_0_simps =
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   400
  sbintrunc_Pls sbintrunc_Min sbintrunc_0_BIT_B0 sbintrunc_0_BIT_B1
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   401
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   402
lemmas bintrunc_simps = bintrunc.Z bintrunc_Sucs
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   403
lemmas sbintrunc_simps = sbintrunc_0_simps sbintrunc_Sucs
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   404
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   405
lemma bintrunc_minus:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   406
  "0 < n ==> bintrunc (Suc (n - 1)) w = bintrunc n w"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   407
  by auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   408
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   409
lemma sbintrunc_minus:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   410
  "0 < n ==> sbintrunc (Suc (n - 1)) w = sbintrunc n w"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   411
  by auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   412
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   413
lemmas bintrunc_minus_simps = 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   414
  bintrunc_Sucs [THEN [2] bintrunc_minus [symmetric, THEN trans], standard]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   415
lemmas sbintrunc_minus_simps = 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   416
  sbintrunc_Sucs [THEN [2] sbintrunc_minus [symmetric, THEN trans], standard]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   417
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   418
lemma bintrunc_n_Pls [simp]:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   419
  "bintrunc n Numeral.Pls = Numeral.Pls"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   420
  by (induct n) auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   421
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   422
lemma sbintrunc_n_PM [simp]:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   423
  "sbintrunc n Numeral.Pls = Numeral.Pls"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   424
  "sbintrunc n Numeral.Min = Numeral.Min"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   425
  by (induct n) auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   426
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   427
lemmas thobini1 = arg_cong [where f = "%w. w BIT ?b"]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   428
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   429
lemmas bintrunc_BIT_I = trans [OF bintrunc_BIT thobini1]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   430
lemmas bintrunc_Min_I = trans [OF bintrunc_Min thobini1]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   431
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   432
lemmas bmsts = bintrunc_minus_simps [THEN thobini1 [THEN [2] trans], standard]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   433
lemmas bintrunc_Pls_minus_I = bmsts(1)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   434
lemmas bintrunc_Min_minus_I = bmsts(2)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   435
lemmas bintrunc_BIT_minus_I = bmsts(3)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   436
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   437
lemma bintrunc_0_Min: "bintrunc 0 Numeral.Min = Numeral.Pls"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   438
  by auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   439
lemma bintrunc_0_BIT: "bintrunc 0 (w BIT b) = Numeral.Pls"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   440
  by auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   441
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   442
lemma bintrunc_Suc_lem:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   443
  "bintrunc (Suc n) x = y ==> m = Suc n ==> bintrunc m x = y"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   444
  by auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   445
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   446
lemmas bintrunc_Suc_Ialts = 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   447
  bintrunc_Min_I bintrunc_BIT_I [THEN bintrunc_Suc_lem, standard]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   448
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   449
lemmas sbintrunc_BIT_I = trans [OF sbintrunc_Suc_BIT thobini1]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   450
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   451
lemmas sbintrunc_Suc_Is = 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   452
  sbintrunc_Sucs [THEN thobini1 [THEN [2] trans], standard]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   453
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   454
lemmas sbintrunc_Suc_minus_Is = 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   455
  sbintrunc_minus_simps [THEN thobini1 [THEN [2] trans], standard]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   456
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   457
lemma sbintrunc_Suc_lem:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   458
  "sbintrunc (Suc n) x = y ==> m = Suc n ==> sbintrunc m x = y"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   459
  by auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   460
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   461
lemmas sbintrunc_Suc_Ialts = 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   462
  sbintrunc_Suc_Is [THEN sbintrunc_Suc_lem, standard]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   463
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   464
lemma sbintrunc_bintrunc_lt:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   465
  "m > n ==> sbintrunc n (bintrunc m w) = sbintrunc n w"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   466
  by (rule bin_eqI) (auto simp: nth_sbintr nth_bintr)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   467
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   468
lemma bintrunc_sbintrunc_le:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   469
  "m <= Suc n ==> bintrunc m (sbintrunc n w) = bintrunc m w"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   470
  apply (rule bin_eqI)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   471
  apply (auto simp: nth_sbintr nth_bintr)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   472
   apply (subgoal_tac "x=n", safe, arith+)[1]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   473
  apply (subgoal_tac "x=n", safe, arith+)[1]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   474
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   475
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   476
lemmas bintrunc_sbintrunc [simp] = order_refl [THEN bintrunc_sbintrunc_le]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   477
lemmas sbintrunc_bintrunc [simp] = lessI [THEN sbintrunc_bintrunc_lt]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   478
lemmas bintrunc_bintrunc [simp] = order_refl [THEN bintrunc_bintrunc_l]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   479
lemmas sbintrunc_sbintrunc [simp] = order_refl [THEN sbintrunc_sbintrunc_l] 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   480
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   481
lemma bintrunc_sbintrunc' [simp]:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   482
  "0 < n \<Longrightarrow> bintrunc n (sbintrunc (n - 1) w) = bintrunc n w"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   483
  by (cases n) (auto simp del: bintrunc.Suc)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   484
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   485
lemma sbintrunc_bintrunc' [simp]:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   486
  "0 < n \<Longrightarrow> sbintrunc (n - 1) (bintrunc n w) = sbintrunc (n - 1) w"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   487
  by (cases n) (auto simp del: bintrunc.Suc)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   488
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   489
lemma bin_sbin_eq_iff: 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   490
  "bintrunc (Suc n) x = bintrunc (Suc n) y <-> 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   491
   sbintrunc n x = sbintrunc n y"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   492
  apply (rule iffI)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   493
   apply (rule box_equals [OF _ sbintrunc_bintrunc sbintrunc_bintrunc])
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   494
   apply simp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   495
  apply (rule box_equals [OF _ bintrunc_sbintrunc bintrunc_sbintrunc])
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   496
  apply simp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   497
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   498
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   499
lemma bin_sbin_eq_iff':
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   500
  "0 < n \<Longrightarrow> bintrunc n x = bintrunc n y <-> 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   501
            sbintrunc (n - 1) x = sbintrunc (n - 1) y"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   502
  by (cases n) (simp_all add: bin_sbin_eq_iff del: bintrunc.Suc)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   503
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   504
lemmas bintrunc_sbintruncS0 [simp] = bintrunc_sbintrunc' [unfolded One_nat_def]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   505
lemmas sbintrunc_bintruncS0 [simp] = sbintrunc_bintrunc' [unfolded One_nat_def]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   506
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   507
lemmas bintrunc_bintrunc_l' = le_add1 [THEN bintrunc_bintrunc_l]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   508
lemmas sbintrunc_sbintrunc_l' = le_add1 [THEN sbintrunc_sbintrunc_l]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   509
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   510
(* although bintrunc_minus_simps, if added to default simpset,
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   511
  tends to get applied where it's not wanted in developing the theories,
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   512
  we get a version for when the word length is given literally *)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   513
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   514
lemmas nat_non0_gr = 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   515
  trans [OF iszero_def [THEN Not_eq_iff [THEN iffD2]] neq0_conv, standard]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   516
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   517
lemmas bintrunc_pred_simps [simp] = 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   518
  bintrunc_minus_simps [of "number_of bin", simplified nobm1, standard]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   519
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   520
lemmas sbintrunc_pred_simps [simp] = 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   521
  sbintrunc_minus_simps [of "number_of bin", simplified nobm1, standard]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   522
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   523
lemma no_bintr_alt:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   524
  "number_of (bintrunc n w) = w mod 2 ^ n"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   525
  by (simp add: number_of_eq bintrunc_mod2p)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   526
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   527
lemma no_bintr_alt1: "bintrunc n = (%w. w mod 2 ^ n :: int)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   528
  by (rule ext) (rule bintrunc_mod2p)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   529
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   530
lemma range_bintrunc: "range (bintrunc n) = {i. 0 <= i & i < 2 ^ n}"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   531
  apply (unfold no_bintr_alt1)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   532
  apply (auto simp add: image_iff)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   533
  apply (rule exI)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   534
  apply (auto intro: int_mod_lem [THEN iffD1, symmetric])
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   535
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   536
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   537
lemma no_bintr: 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   538
  "number_of (bintrunc n w) = (number_of w mod 2 ^ n :: int)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   539
  by (simp add : bintrunc_mod2p number_of_eq)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   540
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   541
lemma no_sbintr_alt2: 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   542
  "sbintrunc n = (%w. (w + 2 ^ n) mod 2 ^ Suc n - 2 ^ n :: int)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   543
  by (rule ext) (simp add : sbintrunc_mod2p)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   544
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   545
lemma no_sbintr: 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   546
  "number_of (sbintrunc n w) = 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   547
   ((number_of w + 2 ^ n) mod 2 ^ Suc n - 2 ^ n :: int)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   548
  by (simp add : no_sbintr_alt2 number_of_eq)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   549
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   550
lemma range_sbintrunc: 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   551
  "range (sbintrunc n) = {i. - (2 ^ n) <= i & i < 2 ^ n}"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   552
  apply (unfold no_sbintr_alt2)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   553
  apply (auto simp add: image_iff eq_diff_eq)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   554
  apply (rule exI)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   555
  apply (auto intro: int_mod_lem [THEN iffD1, symmetric])
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   556
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   557
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   558
lemmas sb_inc_lem = int_mod_ge' 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   559
  [where n = "2 ^ (Suc ?k)" and b = "?a + 2 ^ ?k", 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   560
   simplified zless2p, OF _ TrueI]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   561
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   562
lemmas sb_inc_lem' = 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   563
  iffD1 [OF less_diff_eq, THEN sb_inc_lem, simplified OrderedGroup.diff_0]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   564
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   565
lemma sbintrunc_inc:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   566
  "x < - (2 ^ n) ==> x + 2 ^ (Suc n) <= sbintrunc n x"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   567
  unfolding no_sbintr_alt2 by (drule sb_inc_lem') simp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   568
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   569
lemmas sb_dec_lem = int_mod_le' 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   570
  [where n = "2 ^ (Suc ?k)" and b = "?a + 2 ^ ?k", 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   571
  simplified zless2p, OF _ TrueI, simplified]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   572
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   573
lemmas sb_dec_lem' = iffD1 [OF diff_le_eq', THEN sb_dec_lem, simplified]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   574
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   575
lemma sbintrunc_dec:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   576
  "x >= (2 ^ n) ==> x - 2 ^ (Suc n) >= sbintrunc n x"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   577
  unfolding no_sbintr_alt2 by (drule sb_dec_lem') simp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   578
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   579
lemmas zmod_uminus' = zmod_uminus [where b="?c"]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   580
lemmas zpower_zmod' = zpower_zmod [where m="?c" and y="?k"]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   581
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   582
lemmas brdmod1s' [symmetric] = 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   583
  zmod_zadd_left_eq zmod_zadd_right_eq 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   584
  zmod_zsub_left_eq zmod_zsub_right_eq 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   585
  zmod_zmult1_eq zmod_zmult1_eq_rev 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   586
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   587
lemmas brdmods' [symmetric] = 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   588
  zpower_zmod' [symmetric]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   589
  trans [OF zmod_zadd_left_eq zmod_zadd_right_eq] 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   590
  trans [OF zmod_zsub_left_eq zmod_zsub_right_eq] 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   591
  trans [OF zmod_zmult1_eq zmod_zmult1_eq_rev] 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   592
  zmod_uminus' [symmetric]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   593
  zmod_zadd_left_eq [where b = "1"]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   594
  zmod_zsub_left_eq [where b = "1"]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   595
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   596
lemmas bintr_arith1s =
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   597
  brdmod1s' [where c="2^?n", folded pred_def succ_def bintrunc_mod2p]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   598
lemmas bintr_ariths =
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   599
  brdmods' [where c="2^?n", folded pred_def succ_def bintrunc_mod2p]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   600
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   601
lemma bintr_ge0: "(0 :: int) <= number_of (bintrunc n w)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   602
  by (simp add : no_bintr m2pths)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   603
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   604
lemma bintr_lt2p: "number_of (bintrunc n w) < (2 ^ n :: int)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   605
  by (simp add : no_bintr m2pths)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   606
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   607
lemma bintr_Min: 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   608
  "number_of (bintrunc n Numeral.Min) = (2 ^ n :: int) - 1"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   609
  by (simp add : no_bintr m1mod2k)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   610
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   611
lemma sbintr_ge: "(- (2 ^ n) :: int) <= number_of (sbintrunc n w)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   612
  by (simp add : no_sbintr m2pths)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   613
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   614
lemma sbintr_lt: "number_of (sbintrunc n w) < (2 ^ n :: int)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   615
  by (simp add : no_sbintr m2pths)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   616
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   617
lemma bintrunc_Suc:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   618
  "bintrunc (Suc n) bin = bintrunc n (bin_rest bin) BIT bin_last bin"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   619
  by (case_tac bin rule: bin_exhaust) auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   620
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   621
lemma sign_Pls_ge_0: 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   622
  "(bin_sign bin = Numeral.Pls) = (number_of bin >= (0 :: int))"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   623
  by (induct bin rule: bin_induct) auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   624
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   625
lemma sign_Min_lt_0: 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   626
  "(bin_sign bin = Numeral.Min) = (number_of bin < (0 :: int))"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   627
  by (induct bin rule: bin_induct) auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   628
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   629
lemmas sign_Min_neg = trans [OF sign_Min_lt_0 neg_def [symmetric]] 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   630
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   631
lemma bin_rest_trunc:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   632
  "!!bin. (bin_rest (bintrunc n bin)) = bintrunc (n - 1) (bin_rest bin)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   633
  by (induct n) auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   634
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   635
lemma bin_rest_power_trunc [rule_format] :
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   636
  "(bin_rest ^ k) (bintrunc n bin) = 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   637
    bintrunc (n - k) ((bin_rest ^ k) bin)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   638
  by (induct k) (auto simp: bin_rest_trunc)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   639
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   640
lemma bin_rest_trunc_i:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   641
  "bintrunc n (bin_rest bin) = bin_rest (bintrunc (Suc n) bin)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   642
  by auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   643
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   644
lemma bin_rest_strunc:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   645
  "!!bin. bin_rest (sbintrunc (Suc n) bin) = sbintrunc n (bin_rest bin)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   646
  by (induct n) auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   647
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   648
lemma bintrunc_rest [simp]: 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   649
  "!!bin. bintrunc n (bin_rest (bintrunc n bin)) = bin_rest (bintrunc n bin)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   650
  apply (induct n, simp)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   651
  apply (case_tac bin rule: bin_exhaust)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   652
  apply (auto simp: bintrunc_bintrunc_l)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   653
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   654
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   655
lemma sbintrunc_rest [simp]:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   656
  "!!bin. sbintrunc n (bin_rest (sbintrunc n bin)) = bin_rest (sbintrunc n bin)"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   657
  apply (induct n, simp)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   658
  apply (case_tac bin rule: bin_exhaust)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   659
  apply (auto simp: bintrunc_bintrunc_l split: bit.splits)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   660
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   661
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   662
lemma bintrunc_rest':
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   663
  "bintrunc n o bin_rest o bintrunc n = bin_rest o bintrunc n"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   664
  by (rule ext) auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   665
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   666
lemma sbintrunc_rest' :
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   667
  "sbintrunc n o bin_rest o sbintrunc n = bin_rest o sbintrunc n"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   668
  by (rule ext) auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   669
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   670
lemma rco_lem:
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   671
  "f o g o f = g o f ==> f o (g o f) ^ n = g ^ n o f"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   672
  apply (rule ext)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   673
  apply (induct_tac n)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   674
   apply (simp_all (no_asm))
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   675
  apply (drule fun_cong)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   676
  apply (unfold o_def)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   677
  apply (erule trans)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   678
  apply simp
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   679
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   680
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   681
lemma rco_alt: "(f o g) ^ n o f = f o (g o f) ^ n"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   682
  apply (rule ext)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   683
  apply (induct n)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   684
   apply (simp_all add: o_def)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   685
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   686
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   687
lemmas rco_bintr = bintrunc_rest' 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   688
  [THEN rco_lem [THEN fun_cong], unfolded o_def]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   689
lemmas rco_sbintr = sbintrunc_rest' 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   690
  [THEN rco_lem [THEN fun_cong], unfolded o_def]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   691
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   692
lemmas ls_splits = 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   693
  prod.split split_split prod.split_asm split_split_asm split_if_asm
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   694
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   695
lemma not_B1_is_B0: "y \<noteq> bit.B1 \<Longrightarrow> y = bit.B0"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   696
  by (cases y) auto
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   697
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   698
lemma B1_ass_B0: 
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   699
  assumes y: "y = bit.B0 \<Longrightarrow> y = bit.B1"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   700
  shows "y = bit.B1"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   701
  apply (rule classical)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   702
  apply (drule not_B1_is_B0)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   703
  apply (erule y)
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   704
  done
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   705
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   706
-- "simplifications for specific word lengths"
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   707
lemmas n2s_ths [THEN eq_reflection] = add_2_eq_Suc add_2_eq_Suc'
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   708
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   709
lemmas s2n_ths = n2s_ths [symmetric]
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   710
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   711
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   712
end
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   713
e77ea0ea7f2c * HOL-Word:
kleing
parents:
diff changeset
   714