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