src/HOL/Integ/Bin.ML
author wenzelm
Thu Jan 23 14:19:16 1997 +0100 (1997-01-23)
changeset 2545 d10abc8c11fb
parent 2224 4fc4b465be5b
child 2988 d38f330e58b3
permissions -rw-r--r--
added AxClasses test;
paulson@2224
     1
(*  Title:      HOL/Integ/Bin.ML
paulson@2224
     2
    Authors:    Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@2224
     3
                David Spelt, University of Twente 
paulson@1632
     4
    Copyright   1994  University of Cambridge
paulson@1632
     5
    Copyright   1996 University of Twente
paulson@1632
     6
paulson@1632
     7
Arithmetic on binary integers.
paulson@1632
     8
*)
paulson@1632
     9
paulson@1632
    10
open Bin;
paulson@1632
    11
paulson@1632
    12
(** extra rules for bin_succ, bin_pred, bin_add, bin_mult **)
paulson@1632
    13
paulson@2224
    14
qed_goal "norm_Bcons_Plus_0" Bin.thy
paulson@2224
    15
    "norm_Bcons Plus False = Plus"
paulson@2224
    16
 (fn _ => [(Simp_tac 1)]);
paulson@1632
    17
paulson@2224
    18
qed_goal "norm_Bcons_Plus_1" Bin.thy
paulson@2224
    19
    "norm_Bcons Plus True = Bcons Plus True"
paulson@2224
    20
 (fn _ => [(Simp_tac 1)]);
paulson@1632
    21
paulson@2224
    22
qed_goal "norm_Bcons_Minus_0" Bin.thy
paulson@2224
    23
    "norm_Bcons Minus False = Bcons Minus False"
paulson@2224
    24
 (fn _ => [(Simp_tac 1)]);
paulson@1632
    25
paulson@2224
    26
qed_goal "norm_Bcons_Minus_1" Bin.thy
paulson@2224
    27
    "norm_Bcons Minus True = Minus"
paulson@2224
    28
 (fn _ => [(Simp_tac 1)]);
paulson@1632
    29
paulson@2224
    30
qed_goal "norm_Bcons_Bcons" Bin.thy
paulson@2224
    31
    "norm_Bcons (Bcons w x) b = Bcons (Bcons w x) b"
paulson@2224
    32
 (fn _ => [(Simp_tac 1)]);
paulson@1632
    33
paulson@2224
    34
qed_goal "bin_succ_Bcons1" Bin.thy
paulson@2224
    35
    "bin_succ(Bcons w True) = Bcons (bin_succ w) False"
paulson@2224
    36
 (fn _ => [(Simp_tac 1)]);
paulson@1632
    37
paulson@2224
    38
qed_goal "bin_succ_Bcons0" Bin.thy
paulson@2224
    39
    "bin_succ(Bcons w False) =  norm_Bcons w True"
paulson@2224
    40
 (fn _ => [(Simp_tac 1)]);
paulson@1632
    41
paulson@2224
    42
qed_goal "bin_pred_Bcons1" Bin.thy
paulson@2224
    43
    "bin_pred(Bcons w True) = norm_Bcons w False"
paulson@2224
    44
 (fn _ => [(Simp_tac 1)]);
paulson@1632
    45
paulson@2224
    46
qed_goal "bin_pred_Bcons0" Bin.thy
paulson@2224
    47
    "bin_pred(Bcons w False) = Bcons (bin_pred w) True"
paulson@2224
    48
 (fn _ => [(Simp_tac 1)]);
paulson@1632
    49
paulson@2224
    50
qed_goal "bin_minus_Bcons1" Bin.thy
paulson@2224
    51
    "bin_minus(Bcons w True) = bin_pred (Bcons(bin_minus w) False)"
paulson@2224
    52
 (fn _ => [(Simp_tac 1)]);
paulson@1632
    53
paulson@2224
    54
qed_goal "bin_minus_Bcons0" Bin.thy
paulson@2224
    55
    "bin_minus(Bcons w False) = Bcons (bin_minus w) False"
paulson@2224
    56
 (fn _ => [(Simp_tac 1)]);
paulson@1632
    57
paulson@1632
    58
(*** bin_add: binary addition ***)
paulson@1632
    59
paulson@2224
    60
qed_goal "bin_add_Bcons_Bcons11" Bin.thy
paulson@2224
    61
    "bin_add (Bcons v True) (Bcons w True) = \
paulson@2224
    62
\    norm_Bcons (bin_add v (bin_succ w)) False"
paulson@2224
    63
 (fn _ => [(Simp_tac 1)]);
paulson@1632
    64
paulson@2224
    65
qed_goal "bin_add_Bcons_Bcons10" Bin.thy
paulson@2224
    66
    "bin_add (Bcons v True) (Bcons w False) = norm_Bcons (bin_add v w) True"
paulson@2224
    67
 (fn _ => [(Simp_tac 1)]);
paulson@1632
    68
paulson@2224
    69
val lemma = prove_goal HOL.thy "(False = (~P)) = P"
paulson@2224
    70
 (fn _ => [(Fast_tac 1)]);
paulson@1632
    71
paulson@2224
    72
qed_goal "bin_add_Bcons_Bcons0" Bin.thy
paulson@2224
    73
    "bin_add (Bcons v False) (Bcons w y) = norm_Bcons (bin_add v w) y"
paulson@2224
    74
 (fn _ => [(simp_tac (!simpset addsimps [lemma]) 1)]);
paulson@1632
    75
paulson@2224
    76
qed_goal "bin_add_Bcons_Plus" Bin.thy
paulson@2224
    77
    "bin_add (Bcons v x) Plus = Bcons v x"
paulson@2224
    78
 (fn _ => [(Simp_tac 1)]);
paulson@1632
    79
paulson@2224
    80
qed_goal "bin_add_Bcons_Minus" Bin.thy
paulson@2224
    81
    "bin_add (Bcons v x) Minus = bin_pred (Bcons v x)"
paulson@2224
    82
 (fn _ => [(Simp_tac 1)]);
paulson@1632
    83
paulson@2224
    84
qed_goal "bin_add_Bcons_Bcons" Bin.thy
paulson@2224
    85
    "bin_add (Bcons v x) (Bcons w y) = \
paulson@2224
    86
\    norm_Bcons(bin_add v (if x & y then (bin_succ w) else w)) (x~= y)"
paulson@2224
    87
 (fn _ => [(Simp_tac 1)]);
paulson@1632
    88
paulson@1632
    89
paulson@1632
    90
(*** bin_add: binary multiplication ***)
paulson@1632
    91
paulson@2224
    92
qed_goal "bin_mult_Bcons1" Bin.thy
paulson@2224
    93
    "bin_mult (Bcons v True) w = bin_add (norm_Bcons (bin_mult v w) False) w"
paulson@2224
    94
 (fn _ => [(Simp_tac 1)]);
paulson@1632
    95
paulson@2224
    96
qed_goal "bin_mult_Bcons0" Bin.thy
paulson@2224
    97
    "bin_mult (Bcons v False) w = norm_Bcons (bin_mult v w) False"
paulson@2224
    98
 (fn _ => [(Simp_tac 1)]);
paulson@1632
    99
paulson@1632
   100
paulson@1632
   101
(**** The carry/borrow functions, bin_succ and bin_pred ****)
paulson@1632
   102
paulson@2224
   103
val if_ss = !simpset setloop (split_tac [expand_if]) ;
paulson@1632
   104
paulson@1632
   105
paulson@1632
   106
(**** integ_of_bin ****)
paulson@1632
   107
paulson@1632
   108
paulson@2224
   109
qed_goal "integ_of_bin_norm_Bcons" Bin.thy
paulson@2224
   110
    "integ_of_bin(norm_Bcons w b) = integ_of_bin(Bcons w b)"
paulson@2224
   111
 (fn _ =>[(bin.induct_tac "w" 1),
paulson@2224
   112
          (ALLGOALS(simp_tac if_ss)) ]);
paulson@1632
   113
paulson@2224
   114
qed_goal "integ_of_bin_succ" Bin.thy
paulson@2224
   115
    "integ_of_bin(bin_succ w) = $#1 + integ_of_bin w"
paulson@2224
   116
 (fn _ =>[(rtac bin.induct 1),
paulson@2224
   117
          (ALLGOALS(asm_simp_tac 
paulson@2224
   118
                    (if_ss addsimps (integ_of_bin_norm_Bcons::zadd_ac)))) ]);
paulson@1632
   119
paulson@2224
   120
qed_goal "integ_of_bin_pred" Bin.thy
paulson@2224
   121
    "integ_of_bin(bin_pred w) = $~ ($#1) + integ_of_bin w"
paulson@2224
   122
 (fn _ =>[(rtac bin.induct 1),
paulson@2224
   123
          (ALLGOALS(asm_simp_tac
paulson@2224
   124
                  (if_ss addsimps (integ_of_bin_norm_Bcons::zadd_ac)))) ]);
paulson@1632
   125
paulson@2224
   126
qed_goal "integ_of_bin_minus" Bin.thy
paulson@2224
   127
    "integ_of_bin(bin_minus w) = $~ (integ_of_bin w)"
paulson@2224
   128
 (fn _ =>[(rtac bin.induct 1),
paulson@2224
   129
          (Simp_tac 1),
paulson@2224
   130
          (Simp_tac 1),
paulson@2224
   131
          (asm_simp_tac (if_ss
paulson@2224
   132
                         delsimps [pred_Plus,pred_Minus,pred_Bcons]
paulson@2224
   133
                         addsimps [integ_of_bin_succ,integ_of_bin_pred,
paulson@2224
   134
                                   zadd_assoc]) 1)]);
paulson@1632
   135
paulson@1632
   136
 
paulson@2224
   137
val bin_add_simps = [add_Plus,add_Minus,bin_add_Bcons_Plus,
paulson@2224
   138
                     bin_add_Bcons_Minus,bin_add_Bcons_Bcons,
paulson@2224
   139
                     integ_of_bin_succ, integ_of_bin_pred,
paulson@2224
   140
                     integ_of_bin_norm_Bcons];
paulson@1632
   141
val bin_simps = [iob_Plus,iob_Minus,iob_Bcons];
paulson@1632
   142
paulson@2224
   143
goal Bin.thy
paulson@2224
   144
    "! w. integ_of_bin(bin_add v w) = integ_of_bin v + integ_of_bin w";
paulson@1632
   145
by (bin.induct_tac "v" 1);
paulson@2224
   146
by (simp_tac (if_ss addsimps bin_add_simps) 1);
paulson@2224
   147
by (simp_tac (if_ss addsimps bin_add_simps) 1);
paulson@1632
   148
by (rtac allI 1);
paulson@1632
   149
by (bin.induct_tac "w" 1);
paulson@2224
   150
by (asm_simp_tac (if_ss addsimps (bin_add_simps)) 1);
paulson@2224
   151
by (asm_simp_tac (if_ss addsimps (bin_add_simps @ zadd_ac)) 1);
paulson@1632
   152
by (cut_inst_tac [("P","bool")] True_or_False 1);
paulson@1632
   153
by (etac disjE 1);
paulson@2224
   154
by (asm_simp_tac (if_ss addsimps (bin_add_simps @ zadd_ac)) 1);
paulson@2224
   155
by (asm_simp_tac (if_ss addsimps (bin_add_simps @ zadd_ac)) 1);
paulson@1632
   156
val integ_of_bin_add_lemma = result();
paulson@1632
   157
paulson@1632
   158
goal Bin.thy "integ_of_bin(bin_add v w) = integ_of_bin v + integ_of_bin w";
paulson@1632
   159
by (cut_facts_tac [integ_of_bin_add_lemma] 1);
berghofe@1894
   160
by (Fast_tac 1);
paulson@1632
   161
qed "integ_of_bin_add";
paulson@1632
   162
paulson@2224
   163
val bin_mult_simps = [integ_of_bin_minus, integ_of_bin_add,
paulson@2224
   164
                      integ_of_bin_norm_Bcons];
paulson@1632
   165
paulson@1632
   166
goal Bin.thy "integ_of_bin(bin_mult v w) = integ_of_bin v * integ_of_bin w";
paulson@1632
   167
by (bin.induct_tac "v" 1);
paulson@2224
   168
by (simp_tac (if_ss addsimps bin_mult_simps) 1);
paulson@2224
   169
by (simp_tac (if_ss addsimps bin_mult_simps) 1);
paulson@1632
   170
by (cut_inst_tac [("P","bool")] True_or_False 1);
paulson@1632
   171
by (etac disjE 1);
paulson@2224
   172
by (asm_simp_tac (if_ss addsimps (bin_mult_simps @ [zadd_zmult_distrib])) 2);
paulson@2224
   173
by (asm_simp_tac (if_ss addsimps (bin_mult_simps @ [zadd_zmult_distrib] @ 
paulson@2224
   174
                                  zadd_ac)) 1);
paulson@1632
   175
qed "integ_of_bin_mult";
paulson@1632
   176
paulson@1632
   177
paulson@1632
   178
Delsimps [succ_Bcons,pred_Bcons,min_Bcons,add_Bcons,mult_Bcons,
paulson@2224
   179
          iob_Plus,iob_Minus,iob_Bcons,
paulson@2224
   180
          norm_Plus,norm_Minus,norm_Bcons];
paulson@1632
   181
paulson@1632
   182
Addsimps [integ_of_bin_add RS sym,
paulson@2224
   183
          integ_of_bin_minus RS sym,
paulson@2224
   184
          integ_of_bin_mult RS sym,
paulson@2224
   185
          bin_succ_Bcons1,bin_succ_Bcons0,
paulson@2224
   186
          bin_pred_Bcons1,bin_pred_Bcons0,
paulson@2224
   187
          bin_minus_Bcons1,bin_minus_Bcons0, 
paulson@2224
   188
          bin_add_Bcons_Plus,bin_add_Bcons_Minus,
paulson@2224
   189
          bin_add_Bcons_Bcons0,bin_add_Bcons_Bcons10,bin_add_Bcons_Bcons11,
paulson@2224
   190
          bin_mult_Bcons1,bin_mult_Bcons0,
paulson@2224
   191
          norm_Bcons_Plus_0,norm_Bcons_Plus_1,
paulson@2224
   192
          norm_Bcons_Minus_0,norm_Bcons_Minus_1,
paulson@2224
   193
          norm_Bcons_Bcons];
paulson@2224
   194
paulson@2224
   195
paulson@2224
   196
(** Simplification rules for comparison of binary numbers (Norbert Völker) **) 
paulson@2224
   197
paulson@2224
   198
Addsimps [zadd_assoc];
paulson@2224
   199
paulson@2224
   200
goal Bin.thy  
paulson@2224
   201
    "(integ_of_bin x = integ_of_bin y) \ 
paulson@2224
   202
\   = (integ_of_bin (bin_add x (bin_minus y)) = $# 0)"; 
paulson@2224
   203
  by (simp_tac (HOL_ss addsimps
paulson@2224
   204
                [integ_of_bin_add, integ_of_bin_minus,zdiff_def]) 1); 
paulson@2224
   205
  by (rtac iffI 1); 
paulson@2224
   206
  by (etac ssubst 1);
paulson@2224
   207
  by (rtac zadd_zminus_inverse 1); 
paulson@2224
   208
  by (dres_inst_tac [("f","(% z. z + integ_of_bin y)")] arg_cong 1); 
paulson@2224
   209
  by (asm_full_simp_tac 
paulson@2224
   210
      (HOL_ss addsimps[zadd_assoc,zadd_0,zadd_0_right, 
paulson@2224
   211
                       zadd_zminus_inverse2]) 1); 
paulson@2224
   212
val iob_eq_eq_diff_0 = result(); 
paulson@2224
   213
paulson@2224
   214
goal Bin.thy "(integ_of_bin Plus = $# 0) = True"; 
paulson@2224
   215
  by (stac iob_Plus 1); by (Simp_tac 1); 
paulson@2224
   216
val iob_Plus_eq_0 = result(); 
paulson@2224
   217
paulson@2224
   218
goal Bin.thy "(integ_of_bin Minus = $# 0) = False"; 
paulson@2224
   219
  by (stac iob_Minus 1); 
paulson@2224
   220
  by (Simp_tac 1);
paulson@2224
   221
val iob_Minus_not_eq_0 = result(); 
paulson@2224
   222
paulson@2224
   223
goal Bin.thy 
paulson@2224
   224
    "(integ_of_bin (Bcons w x) = $# 0) = (~x & integ_of_bin w = $# 0)"; 
paulson@2224
   225
  by (stac iob_Bcons 1);
paulson@2224
   226
  by (case_tac "x" 1); 
paulson@2224
   227
  by (ALLGOALS Asm_simp_tac); 
paulson@2224
   228
  by (ALLGOALS(asm_simp_tac (HOL_ss addsimps [integ_of_bin_add]))); 
paulson@2224
   229
  by (ALLGOALS(int_case_tac "integ_of_bin w")); 
paulson@2224
   230
  by (ALLGOALS(asm_simp_tac 
paulson@2224
   231
               (!simpset addsimps[zminus_zadd_distrib RS sym, 
paulson@2224
   232
                                znat_add RS sym]))); 
paulson@2224
   233
  by (stac eq_False_conv 1); 
paulson@2224
   234
  by (rtac notI 1); 
paulson@2224
   235
  by (dres_inst_tac [("f","(% z. z +  $# Suc (Suc (n + n)))")] arg_cong 1); 
paulson@2224
   236
  by (Asm_full_simp_tac 1); 
paulson@2224
   237
val iob_Bcons_eq_0 = result(); 
paulson@2224
   238
paulson@2224
   239
goalw Bin.thy [zless_def,zdiff_def] 
paulson@2224
   240
    "integ_of_bin x < integ_of_bin y \
paulson@2224
   241
\    = (integ_of_bin (bin_add x (bin_minus y)) < $# 0)";
paulson@2224
   242
  by (Simp_tac 1); 
paulson@2224
   243
val iob_less_eq_diff_lt_0 = result(); 
paulson@2224
   244
paulson@2224
   245
goal Bin.thy "(integ_of_bin Plus < $# 0) = False"; 
paulson@2224
   246
  by (stac iob_Plus 1); by (Simp_tac 1); 
paulson@2224
   247
val iob_Plus_not_lt_0 = result(); 
paulson@2224
   248
paulson@2224
   249
goal Bin.thy "(integ_of_bin Minus < $# 0) = True"; 
paulson@2224
   250
  by (stac iob_Minus 1); by (Simp_tac 1);
paulson@2224
   251
val iob_Minus_lt_0 = result(); 
paulson@2224
   252
paulson@2224
   253
goal Bin.thy 
paulson@2224
   254
    "(integ_of_bin (Bcons w x) < $# 0) = (integ_of_bin w < $# 0)"; 
paulson@2224
   255
  by (stac iob_Bcons 1);
paulson@2224
   256
  by (case_tac "x" 1); 
paulson@2224
   257
  by (ALLGOALS Asm_simp_tac); 
paulson@2224
   258
  by (ALLGOALS(asm_simp_tac (HOL_ss addsimps [integ_of_bin_add]))); 
paulson@2224
   259
  by (ALLGOALS(int_case_tac "integ_of_bin w")); 
paulson@2224
   260
  by (ALLGOALS(asm_simp_tac 
paulson@2224
   261
               (!simpset addsimps[zminus_zadd_distrib RS sym, 
paulson@2224
   262
                                znat_add RS sym]))); 
paulson@2224
   263
  by (stac (zadd_zminus_inverse RS sym) 1); 
paulson@2224
   264
  by (rtac zadd_zless_mono1 1); 
paulson@2224
   265
  by (Simp_tac 1); 
paulson@2224
   266
val iob_Bcons_lt_0 = result(); 
paulson@2224
   267
paulson@2224
   268
goal Bin.thy
paulson@2224
   269
  "integ_of_bin x <= integ_of_bin y \
paulson@2224
   270
\  = ( integ_of_bin (bin_add x (bin_minus y)) < $# 0 \
paulson@2224
   271
\    | integ_of_bin (bin_add x (bin_minus y)) = $# 0)";
paulson@2224
   272
by (simp_tac (HOL_ss addsimps 
paulson@2224
   273
              [zle_eq_zless_or_eq,iob_less_eq_diff_lt_0,zdiff_def
paulson@2224
   274
               ,iob_eq_eq_diff_0,integ_of_bin_minus,integ_of_bin_add]) 1);
paulson@2224
   275
val iob_le_diff_lt_0_or_eq_0 = result(); 
paulson@2224
   276
paulson@2224
   277
Delsimps [zless_eq_less, zle_eq_le, zadd_assoc, znegative_zminus_znat, 
paulson@2224
   278
          not_znegative_znat, zero_zless_Suc_pos, negative_zless_0, 
paulson@2224
   279
          negative_zle_0, not_zle_0_negative, not_znat_zless_negative, 
paulson@2224
   280
          zminus_zless_zminus, zminus_zle_zminus, negative_eq_positive]; 
paulson@2224
   281
paulson@2224
   282
Addsimps [zdiff_def, iob_eq_eq_diff_0, iob_less_eq_diff_lt_0, 
paulson@2224
   283
          iob_le_diff_lt_0_or_eq_0, iob_Plus_eq_0, iob_Minus_not_eq_0, 
paulson@2224
   284
          iob_Bcons_eq_0, iob_Plus_not_lt_0, iob_Minus_lt_0, iob_Bcons_lt_0];
paulson@2224
   285
paulson@1632
   286
paulson@1632
   287
(*** Examples of performing binary arithmetic by simplification ***)
paulson@1632
   288
paulson@1632
   289
goal Bin.thy "#13  +  #19 = #32";
paulson@1632
   290
by (Simp_tac 1);
paulson@1632
   291
result();
paulson@1632
   292
paulson@1632
   293
goal Bin.thy "#1234  +  #5678 = #6912";
paulson@1632
   294
by (Simp_tac 1);
paulson@1632
   295
result();
paulson@1632
   296
paulson@1632
   297
goal Bin.thy "#1359  +  #~2468 = #~1109";
paulson@1632
   298
by (Simp_tac 1);
paulson@1632
   299
result();
paulson@1632
   300
paulson@1632
   301
goal Bin.thy "#93746 +  #~46375 = #47371";
paulson@1632
   302
by (Simp_tac 1);
paulson@1632
   303
result();
paulson@1632
   304
paulson@1632
   305
goal Bin.thy "$~ #65745 = #~65745";
paulson@1632
   306
by (Simp_tac 1);
paulson@1632
   307
result();
paulson@1632
   308
paulson@1632
   309
goal Bin.thy "$~ #~54321 = #54321";
paulson@1632
   310
by (Simp_tac 1);
paulson@1632
   311
result();
paulson@1632
   312
paulson@1632
   313
goal Bin.thy "#13  *  #19 = #247";
paulson@1632
   314
by (Simp_tac 1);
paulson@1632
   315
result();
paulson@1632
   316
paulson@1632
   317
goal Bin.thy "#~84  *  #51 = #~4284";
paulson@1632
   318
by (Simp_tac 1);
paulson@1632
   319
result();
paulson@1632
   320
paulson@1632
   321
goal Bin.thy "#255  *  #255 = #65025";
paulson@1632
   322
by (Simp_tac 1);
paulson@1632
   323
result();
paulson@1632
   324
paulson@1632
   325
goal Bin.thy "#1359  *  #~2468 = #~3354012";
paulson@1632
   326
by (Simp_tac 1);
paulson@1632
   327
result();
paulson@2224
   328
paulson@2224
   329
goal Bin.thy "#89 * #10 ~= #889";  
paulson@2224
   330
by (Simp_tac 1); 
paulson@2224
   331
result();
paulson@2224
   332
paulson@2224
   333
goal Bin.thy "#13 < #18 - #4";  
paulson@2224
   334
by (Simp_tac 1); 
paulson@2224
   335
result();
paulson@2224
   336
paulson@2224
   337
goal Bin.thy "#~345 < #~242 + #~100";  
paulson@2224
   338
by (Simp_tac 1); 
paulson@2224
   339
result();
paulson@2224
   340
paulson@2224
   341
goal Bin.thy "#13557456 < #18678654";  
paulson@2224
   342
by (Simp_tac 1); 
paulson@2224
   343
result();
paulson@2224
   344
paulson@2224
   345
goal Bin.thy "#999999 <= (#1000001 + #1)-#2";  
paulson@2224
   346
by (Simp_tac 1); 
paulson@2224
   347
result();
paulson@2224
   348
paulson@2224
   349
goal Bin.thy "#1234567 <= #1234567";  
paulson@2224
   350
by (Simp_tac 1); 
paulson@2224
   351
result();