src/HOL/ex/BinEx.ML
author wenzelm
Tue May 30 16:08:38 2000 +0200 (2000-05-30)
changeset 9000 c20d58286a51
parent 8442 96023903c2df
permissions -rw-r--r--
cleaned up;
paulson@5545
     1
(*  Title:      HOL/ex/BinEx.ML
paulson@5545
     2
    ID:         $Id$
paulson@5545
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@5545
     4
    Copyright   1998  University of Cambridge
wenzelm@5199
     5
paulson@5545
     6
Examples of performing binary arithmetic by simplification
paulson@5545
     7
paulson@5545
     8
Also a proof that binary arithmetic on normalized operands 
paulson@5545
     9
yields normalized results. 
paulson@5545
    10
*)
paulson@5545
    11
paulson@7037
    12
(**** The Integers ****)
paulson@7037
    13
paulson@6920
    14
(*** Addition ***)
paulson@5491
    15
wenzelm@6909
    16
Goal "(#13::int)  +  #19 = #32";
wenzelm@5199
    17
by (Simp_tac 1);
wenzelm@5199
    18
result();
wenzelm@5199
    19
wenzelm@6909
    20
Goal "(#1234::int)  +  #5678 = #6912";
wenzelm@5199
    21
by (Simp_tac 1);
wenzelm@5199
    22
result();
wenzelm@5199
    23
wenzelm@6909
    24
Goal "(#1359::int)  +  #-2468 = #-1109";
wenzelm@5199
    25
by (Simp_tac 1);
wenzelm@5199
    26
result();
wenzelm@5199
    27
wenzelm@6909
    28
Goal "(#93746::int) +  #-46375 = #47371";
wenzelm@5199
    29
by (Simp_tac 1);
wenzelm@5199
    30
result();
wenzelm@5199
    31
paulson@6920
    32
(*** Negation ***)
paulson@5491
    33
wenzelm@6909
    34
Goal "- (#65745::int) = #-65745";
wenzelm@5199
    35
by (Simp_tac 1);
wenzelm@5199
    36
result();
wenzelm@5199
    37
wenzelm@6909
    38
Goal "- (#-54321::int) = #54321";
wenzelm@5199
    39
by (Simp_tac 1);
wenzelm@5199
    40
result();
wenzelm@5199
    41
paulson@5491
    42
paulson@6920
    43
(*** Multiplication ***)
paulson@5491
    44
wenzelm@6909
    45
Goal "(#13::int)  *  #19 = #247";
wenzelm@5199
    46
by (Simp_tac 1);
wenzelm@5199
    47
result();
wenzelm@5199
    48
wenzelm@6909
    49
Goal "(#-84::int)  *  #51 = #-4284";
wenzelm@5199
    50
by (Simp_tac 1);
wenzelm@5199
    51
result();
wenzelm@5199
    52
wenzelm@6909
    53
Goal "(#255::int)  *  #255 = #65025";
wenzelm@5199
    54
by (Simp_tac 1);
wenzelm@5199
    55
result();
wenzelm@5199
    56
wenzelm@6909
    57
Goal "(#1359::int)  *  #-2468 = #-3354012";
wenzelm@5199
    58
by (Simp_tac 1);
wenzelm@5199
    59
result();
wenzelm@5199
    60
wenzelm@6909
    61
Goal "(#89::int) * #10 ~= #889";  
wenzelm@5199
    62
by (Simp_tac 1); 
wenzelm@5199
    63
result();
wenzelm@5199
    64
wenzelm@6909
    65
Goal "(#13::int) < #18 - #4";  
wenzelm@5199
    66
by (Simp_tac 1); 
wenzelm@5199
    67
result();
wenzelm@5199
    68
wenzelm@6909
    69
Goal "(#-345::int) < #-242 + #-100";  
wenzelm@5199
    70
by (Simp_tac 1); 
wenzelm@5199
    71
result();
wenzelm@5199
    72
wenzelm@6909
    73
Goal "(#13557456::int) < #18678654";  
wenzelm@5199
    74
by (Simp_tac 1); 
wenzelm@5199
    75
result();
wenzelm@5199
    76
wenzelm@6909
    77
Goal "(#999999::int) <= (#1000001 + #1)-#2";  
wenzelm@5199
    78
by (Simp_tac 1); 
wenzelm@5199
    79
result();
wenzelm@5199
    80
wenzelm@6909
    81
Goal "(#1234567::int) <= #1234567";  
wenzelm@5199
    82
by (Simp_tac 1); 
wenzelm@5199
    83
result();
paulson@5545
    84
paulson@5545
    85
paulson@7037
    86
(*** Quotient and Remainder ***)
paulson@6920
    87
paulson@6920
    88
Goal "(#10::int) div #3 = #3";
paulson@6920
    89
by (Simp_tac 1);
paulson@6920
    90
result();
paulson@6920
    91
paulson@6920
    92
Goal "(#10::int) mod #3 = #1";
paulson@6920
    93
by (Simp_tac 1);
paulson@6920
    94
result();
paulson@6920
    95
paulson@6920
    96
(** A negative divisor **)
paulson@6920
    97
paulson@6920
    98
Goal "(#10::int) div #-3 = #-4";
paulson@6920
    99
by (Simp_tac 1);
paulson@6920
   100
result();
paulson@6920
   101
paulson@6920
   102
Goal "(#10::int) mod #-3 = #-2";
paulson@6920
   103
by (Simp_tac 1);
paulson@6920
   104
result();
paulson@6920
   105
paulson@6920
   106
(** A negative dividend
paulson@6920
   107
    [ The definition agrees with mathematical convention but not with
paulson@6920
   108
      the hardware of most computers ]
paulson@6920
   109
**)
paulson@6920
   110
paulson@6920
   111
Goal "(#-10::int) div #3 = #-4";
paulson@6920
   112
by (Simp_tac 1);
paulson@6920
   113
result();
paulson@6920
   114
paulson@6920
   115
Goal "(#-10::int) mod #3 = #2";
paulson@6920
   116
by (Simp_tac 1);
paulson@6920
   117
result();
paulson@6920
   118
paulson@6920
   119
(** A negative dividend AND divisor **)
paulson@6920
   120
paulson@6920
   121
Goal "(#-10::int) div #-3 = #3";
paulson@6920
   122
by (Simp_tac 1);
paulson@6920
   123
result();
paulson@6920
   124
paulson@6920
   125
Goal "(#-10::int) mod #-3 = #-1";
paulson@6920
   126
by (Simp_tac 1);
paulson@6920
   127
result();
paulson@6920
   128
paulson@6920
   129
(** A few bigger examples **)
paulson@6920
   130
paulson@6920
   131
Goal "(#8452::int) mod #3 = #1";
paulson@6920
   132
by (Simp_tac 1);
paulson@6920
   133
result();
paulson@6920
   134
paulson@6920
   135
Goal "(#59485::int) div #434 = #137";
paulson@6920
   136
by (Simp_tac 1);
paulson@6920
   137
result();
paulson@6920
   138
paulson@6920
   139
Goal "(#1000006::int) mod #10 = #6";
paulson@6920
   140
by (Simp_tac 1);
paulson@6920
   141
result();
paulson@6920
   142
paulson@6920
   143
paulson@7037
   144
(** division by shifting **)
paulson@7037
   145
paulson@7037
   146
Goal "#10000000 div #2 = (#5000000::int)";
paulson@7037
   147
by (Simp_tac 1);
paulson@7037
   148
result();
paulson@7037
   149
paulson@7037
   150
Goal "#10000001 mod #2 = (#1::int)";
paulson@7037
   151
by (Simp_tac 1);
paulson@7037
   152
result();
paulson@7037
   153
paulson@7037
   154
Goal "#10000055 div #32 = (#312501::int)";
paulson@7037
   155
by (Simp_tac 1);
paulson@7037
   156
paulson@7037
   157
Goal "#10000055 mod #32 = (#23::int)";
paulson@7037
   158
by (Simp_tac 1);
paulson@7037
   159
paulson@7037
   160
Goal "#100094 div #144 = (#695::int)";
paulson@7037
   161
by (Simp_tac 1);
paulson@7037
   162
result();
paulson@7037
   163
paulson@7037
   164
Goal "#100094 mod #144 = (#14::int)";
paulson@7037
   165
by (Simp_tac 1);
paulson@7037
   166
result();
paulson@7037
   167
paulson@7037
   168
paulson@7037
   169
paulson@7037
   170
(**** The Natural Numbers ****)
paulson@7037
   171
paulson@7037
   172
(** Successor **)
paulson@7037
   173
paulson@7037
   174
Goal "Suc #99999 = #100000";
paulson@7037
   175
by (asm_simp_tac (simpset() addsimps [Suc_nat_number_of]) 1);
paulson@7037
   176
	(*not a default rewrite since sometimes we want to have Suc(#nnn)*)
paulson@7037
   177
result();
paulson@7037
   178
paulson@7037
   179
paulson@7037
   180
(** Addition **)
paulson@7037
   181
paulson@7037
   182
Goal "(#13::nat)  +  #19 = #32";
paulson@7037
   183
by (Simp_tac 1);
paulson@7037
   184
result();
paulson@7037
   185
paulson@7037
   186
Goal "(#1234::nat)  +  #5678 = #6912";
paulson@7037
   187
by (Simp_tac 1);
paulson@7037
   188
result();
paulson@7037
   189
paulson@7037
   190
Goal "(#973646::nat) +  #6475 = #980121";
paulson@7037
   191
by (Simp_tac 1);
paulson@7037
   192
result();
paulson@7037
   193
paulson@7037
   194
paulson@7037
   195
(** Subtraction **)
paulson@7037
   196
paulson@7037
   197
Goal "(#32::nat)  -  #14 = #18";
paulson@7037
   198
by (Simp_tac 1);
paulson@7037
   199
result();
paulson@7037
   200
paulson@7037
   201
Goal "(#14::nat)  -  #15 = #0";
paulson@7037
   202
by (Simp_tac 1);
paulson@7037
   203
result();
paulson@7037
   204
paulson@7037
   205
Goal "(#14::nat)  -  #1576644 = #0";
paulson@7037
   206
by (Simp_tac 1);
paulson@7037
   207
result();
paulson@7037
   208
paulson@7037
   209
Goal "(#48273776::nat)  -  #3873737 = #44400039";
paulson@7037
   210
by (Simp_tac 1);
paulson@7037
   211
result();
paulson@7037
   212
paulson@7037
   213
paulson@7037
   214
(** Multiplication **)
paulson@7037
   215
paulson@7037
   216
Goal "(#12::nat) * #11 = #132";
paulson@7037
   217
by (Simp_tac 1);
paulson@7037
   218
result();
paulson@7037
   219
paulson@7037
   220
Goal "(#647::nat) * #3643 = #2357021";
paulson@7037
   221
by (Simp_tac 1);
paulson@7037
   222
result();
paulson@7037
   223
paulson@7037
   224
paulson@7037
   225
(** Quotient and Remainder **)
paulson@7037
   226
paulson@7037
   227
Goal "(#10::nat) div #3 = #3";
paulson@7037
   228
by (Simp_tac 1);
paulson@7037
   229
result();
paulson@7037
   230
paulson@7037
   231
Goal "(#10::nat) mod #3 = #1";
paulson@7037
   232
by (Simp_tac 1);
paulson@7037
   233
result();
paulson@7037
   234
paulson@7037
   235
Goal "(#10000::nat) div #9 = #1111";
paulson@7037
   236
by (Simp_tac 1);
paulson@7037
   237
result();
paulson@7037
   238
paulson@7037
   239
Goal "(#10000::nat) mod #9 = #1";
paulson@7037
   240
by (Simp_tac 1);
paulson@7037
   241
result();
paulson@7037
   242
paulson@7037
   243
Goal "(#10000::nat) div #16 = #625";
paulson@7037
   244
by (Simp_tac 1);
paulson@7037
   245
result();
paulson@7037
   246
paulson@7037
   247
Goal "(#10000::nat) mod #16 = #0";
paulson@7037
   248
by (Simp_tac 1);
paulson@7037
   249
result();
paulson@7037
   250
paulson@7037
   251
paulson@6920
   252
(*** Testing the cancellation of complementary terms ***)
paulson@5601
   253
wenzelm@6909
   254
Goal "y + (x + -x) = (#0::int) + y";
paulson@5601
   255
by (Simp_tac 1);
paulson@5601
   256
result();
paulson@5601
   257
wenzelm@6909
   258
Goal "y + (-x + (- y + x)) = (#0::int)";
paulson@5601
   259
by (Simp_tac 1);
paulson@5601
   260
result();
paulson@5601
   261
wenzelm@6909
   262
Goal "-x + (y + (- y + x)) = (#0::int)";
paulson@5601
   263
by (Simp_tac 1);
paulson@5601
   264
result();
paulson@5601
   265
wenzelm@6909
   266
Goal "x + (x + (- x + (- x + (- y + - z)))) = (#0::int) - y - z";
paulson@5601
   267
by (Simp_tac 1);
paulson@5601
   268
result();
paulson@5601
   269
wenzelm@6909
   270
Goal "x + x - x - x - y - z = (#0::int) - y - z";
paulson@5601
   271
by (Simp_tac 1);
paulson@5601
   272
result();
paulson@5601
   273
wenzelm@6909
   274
Goal "x + y + z - (x + z) = y - (#0::int)";
paulson@5601
   275
by (Simp_tac 1);
paulson@5601
   276
result();
paulson@5601
   277
wenzelm@6909
   278
Goal "x+(y+(y+(y+ (-x + -x)))) = (#0::int) + y - x + y + y";
paulson@5601
   279
by (Simp_tac 1);
paulson@5601
   280
result();
paulson@5601
   281
wenzelm@6909
   282
Goal "x+(y+(y+(y+ (-y + -x)))) = y + (#0::int) + y";
paulson@5601
   283
by (Simp_tac 1);
paulson@5601
   284
result();
paulson@5601
   285
wenzelm@6909
   286
Goal "x + y - x + z - x - y - z + x < (#1::int)";
paulson@5601
   287
by (Simp_tac 1);
paulson@5601
   288
result();
paulson@5601
   289
paulson@5601
   290
paulson@5545
   291
Addsimps normal.intrs;
paulson@5545
   292
paulson@5545
   293
Goal "(w BIT b): normal ==> (w BIT b BIT c): normal";
paulson@5545
   294
by (case_tac "c" 1);
paulson@5545
   295
by Auto_tac;
paulson@5545
   296
qed "normal_BIT_I";
paulson@5545
   297
paulson@5545
   298
Addsimps [normal_BIT_I];
paulson@5545
   299
paulson@5545
   300
Goal "w BIT b: normal ==> w: normal";
paulson@5545
   301
by (etac normal.elim 1);
paulson@5545
   302
by Auto_tac;
paulson@5545
   303
qed "normal_BIT_D";
paulson@5545
   304
paulson@5545
   305
Goal "w : normal --> NCons w b : normal";
paulson@5545
   306
by (induct_tac "w" 1);
paulson@5545
   307
by (auto_tac (claset(), simpset() addsimps [NCons_Pls, NCons_Min]));
paulson@5545
   308
qed_spec_mp "NCons_normal";
paulson@5545
   309
paulson@5545
   310
Addsimps [NCons_normal];
paulson@5545
   311
paulson@5545
   312
Goal "NCons w True ~= Pls";
paulson@5545
   313
by (induct_tac "w" 1);
paulson@5545
   314
by Auto_tac;
paulson@5545
   315
qed "NCons_True";
paulson@5545
   316
paulson@5545
   317
Goal "NCons w False ~= Min";
paulson@5545
   318
by (induct_tac "w" 1);
paulson@5545
   319
by Auto_tac;
paulson@5545
   320
qed "NCons_False";
paulson@5545
   321
paulson@5545
   322
Goal "w: normal ==> bin_succ w : normal";
paulson@5545
   323
by (etac normal.induct 1);
wenzelm@8442
   324
by (case_tac "w" 4);
paulson@5545
   325
by (auto_tac (claset(), simpset() addsimps [NCons_True, bin_succ_BIT]));
paulson@5545
   326
qed "bin_succ_normal";
paulson@5545
   327
paulson@5545
   328
Goal "w: normal ==> bin_pred w : normal";
paulson@5545
   329
by (etac normal.induct 1);
wenzelm@8442
   330
by (case_tac "w" 3);
paulson@5545
   331
by (auto_tac (claset(), simpset() addsimps [NCons_False, bin_pred_BIT]));
paulson@5545
   332
qed "bin_pred_normal";
paulson@5545
   333
paulson@5545
   334
Addsimps [bin_succ_normal, bin_pred_normal];
paulson@5545
   335
paulson@5545
   336
Goal "w : normal --> (ALL z. z: normal --> bin_add w z : normal)";
paulson@5545
   337
by (induct_tac "w" 1);
paulson@5545
   338
by (Simp_tac 1);
paulson@5545
   339
by (Simp_tac 1);
paulson@5545
   340
by (rtac impI 1);
paulson@5545
   341
by (rtac allI 1);
paulson@5545
   342
by (induct_tac "z" 1);
paulson@5545
   343
by (ALLGOALS (asm_simp_tac (simpset() addsimps [bin_add_BIT])));
paulson@5545
   344
by (safe_tac (claset() addSDs [normal_BIT_D]));
paulson@5545
   345
by (ALLGOALS Asm_simp_tac);
paulson@5545
   346
qed_spec_mp "bin_add_normal";
paulson@5545
   347
wenzelm@6909
   348
Goal "w: normal ==> (w = Pls) = (number_of w = (#0::int))";
paulson@5545
   349
by (etac normal.induct 1);
paulson@5545
   350
by Auto_tac;
paulson@5545
   351
qed "normal_Pls_eq_0";
paulson@5545
   352
paulson@5545
   353
Goal "w : normal ==> bin_minus w : normal";
paulson@5545
   354
by (etac normal.induct 1);
paulson@5545
   355
by (ALLGOALS (asm_simp_tac (simpset() addsimps [bin_minus_BIT])));
paulson@5545
   356
by (resolve_tac normal.intrs 1);
paulson@5545
   357
by (assume_tac 1);
paulson@5545
   358
by (asm_full_simp_tac (simpset() addsimps [normal_Pls_eq_0]) 1);
paulson@5545
   359
by (asm_full_simp_tac 
paulson@6920
   360
    (simpset_of Int.thy 
paulson@6920
   361
     addsimps [number_of_minus, iszero_def, 
paulson@6920
   362
	       read_instantiate [("y","int 0")] zminus_equation]) 1);
paulson@6920
   363
by (etac not_sym 1);
paulson@5545
   364
qed "bin_minus_normal";
paulson@5545
   365
paulson@5545
   366
Goal "w : normal ==> z: normal --> bin_mult w z : normal";
paulson@5545
   367
by (etac normal.induct 1);
paulson@5569
   368
by (ALLGOALS
paulson@5569
   369
    (asm_simp_tac (simpset() addsimps [bin_minus_normal, bin_mult_BIT])));
paulson@5545
   370
by (safe_tac (claset() addSDs [normal_BIT_D]));
paulson@5545
   371
by (asm_simp_tac (simpset() addsimps [bin_add_normal]) 1);
paulson@5545
   372
qed_spec_mp "bin_mult_normal";