src/HOL/ex/BinEx.ML
author paulson
Thu Oct 01 18:30:05 1998 +0200 (1998-10-01)
changeset 5601 b6456ccd9e3e
parent 5569 8c7e1190e789
child 5747 387b5bf9326a
permissions -rw-r--r--
revised for new treatment of integers
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@5491
    14
(** Addition **)
paulson@5491
    15
wenzelm@5199
    16
Goal "#13  +  #19 = #32";
wenzelm@5199
    17
by (Simp_tac 1);
wenzelm@5199
    18
result();
wenzelm@5199
    19
wenzelm@5199
    20
Goal "#1234  +  #5678 = #6912";
wenzelm@5199
    21
by (Simp_tac 1);
wenzelm@5199
    22
result();
wenzelm@5199
    23
paulson@5513
    24
Goal "#1359  +  #-2468 = #-1109";
wenzelm@5199
    25
by (Simp_tac 1);
wenzelm@5199
    26
result();
wenzelm@5199
    27
paulson@5513
    28
Goal "#93746 +  #-46375 = #47371";
wenzelm@5199
    29
by (Simp_tac 1);
wenzelm@5199
    30
result();
wenzelm@5199
    31
paulson@5491
    32
(** Negation **)
paulson@5491
    33
paulson@5513
    34
Goal "- #65745 = #-65745";
wenzelm@5199
    35
by (Simp_tac 1);
wenzelm@5199
    36
result();
wenzelm@5199
    37
paulson@5513
    38
Goal "- #-54321 = #54321";
wenzelm@5199
    39
by (Simp_tac 1);
wenzelm@5199
    40
result();
wenzelm@5199
    41
paulson@5491
    42
paulson@5491
    43
(** Multiplication **)
paulson@5491
    44
wenzelm@5199
    45
Goal "#13  *  #19 = #247";
wenzelm@5199
    46
by (Simp_tac 1);
wenzelm@5199
    47
result();
wenzelm@5199
    48
paulson@5513
    49
Goal "#-84  *  #51 = #-4284";
wenzelm@5199
    50
by (Simp_tac 1);
wenzelm@5199
    51
result();
wenzelm@5199
    52
wenzelm@5199
    53
Goal "#255  *  #255 = #65025";
wenzelm@5199
    54
by (Simp_tac 1);
wenzelm@5199
    55
result();
wenzelm@5199
    56
paulson@5513
    57
Goal "#1359  *  #-2468 = #-3354012";
wenzelm@5199
    58
by (Simp_tac 1);
wenzelm@5199
    59
result();
wenzelm@5199
    60
wenzelm@5199
    61
Goal "#89 * #10 ~= #889";  
wenzelm@5199
    62
by (Simp_tac 1); 
wenzelm@5199
    63
result();
wenzelm@5199
    64
wenzelm@5199
    65
Goal "#13 < #18 - #4";  
wenzelm@5199
    66
by (Simp_tac 1); 
wenzelm@5199
    67
result();
wenzelm@5199
    68
paulson@5513
    69
Goal "#-345 < #-242 + #-100";  
wenzelm@5199
    70
by (Simp_tac 1); 
wenzelm@5199
    71
result();
wenzelm@5199
    72
wenzelm@5199
    73
Goal "#13557456 < #18678654";  
wenzelm@5199
    74
by (Simp_tac 1); 
wenzelm@5199
    75
result();
wenzelm@5199
    76
wenzelm@5199
    77
Goal "#999999 <= (#1000001 + #1)-#2";  
wenzelm@5199
    78
by (Simp_tac 1); 
wenzelm@5199
    79
result();
wenzelm@5199
    80
wenzelm@5199
    81
Goal "#1234567 <= #1234567";  
wenzelm@5199
    82
by (Simp_tac 1); 
wenzelm@5199
    83
result();
paulson@5545
    84
paulson@5545
    85
paulson@5601
    86
(** Testing the cancellation of complementary terms **)
paulson@5601
    87
paulson@5601
    88
Goal "y + (x + -x) = int 0 + y";
paulson@5601
    89
by (Simp_tac 1);
paulson@5601
    90
result();
paulson@5601
    91
paulson@5601
    92
Goal "y + (-x + (- y + x)) = int 0";
paulson@5601
    93
by (Simp_tac 1);
paulson@5601
    94
result();
paulson@5601
    95
paulson@5601
    96
Goal "-x + (y + (- y + x)) = int 0";
paulson@5601
    97
by (Simp_tac 1);
paulson@5601
    98
result();
paulson@5601
    99
paulson@5601
   100
Goal "x + (x + (- x + (- x + (- y + - z)))) = int 0 - y - z";
paulson@5601
   101
by (Simp_tac 1);
paulson@5601
   102
result();
paulson@5601
   103
paulson@5601
   104
Goal "x + x - x - x - y - z = int 0 - y - z";
paulson@5601
   105
by (Simp_tac 1);
paulson@5601
   106
result();
paulson@5601
   107
paulson@5601
   108
Goal "x + y + z - (x + z) = y - int 0";
paulson@5601
   109
by (Simp_tac 1);
paulson@5601
   110
result();
paulson@5601
   111
paulson@5601
   112
Goal "x+(y+(y+(y+ (-x + -x)))) = int 0 + y - x + y + y";
paulson@5601
   113
by (Simp_tac 1);
paulson@5601
   114
result();
paulson@5601
   115
paulson@5601
   116
Goal "x+(y+(y+(y+ (-y + -x)))) = y + int 0 + y";
paulson@5601
   117
by (Simp_tac 1);
paulson@5601
   118
result();
paulson@5601
   119
paulson@5601
   120
Goal "x + y - x + z - x - y - z + x < int 1";
paulson@5601
   121
by (Simp_tac 1);
paulson@5601
   122
result();
paulson@5601
   123
paulson@5601
   124
paulson@5545
   125
Addsimps normal.intrs;
paulson@5545
   126
paulson@5545
   127
Goal "(w BIT b): normal ==> (w BIT b BIT c): normal";
paulson@5545
   128
by (case_tac "c" 1);
paulson@5545
   129
by Auto_tac;
paulson@5545
   130
qed "normal_BIT_I";
paulson@5545
   131
paulson@5545
   132
Addsimps [normal_BIT_I];
paulson@5545
   133
paulson@5545
   134
Goal "w BIT b: normal ==> w: normal";
paulson@5545
   135
by (etac normal.elim 1);
paulson@5545
   136
by Auto_tac;
paulson@5545
   137
qed "normal_BIT_D";
paulson@5545
   138
paulson@5545
   139
Goal "w : normal --> NCons w b : normal";
paulson@5545
   140
by (induct_tac "w" 1);
paulson@5545
   141
by (auto_tac (claset(), simpset() addsimps [NCons_Pls, NCons_Min]));
paulson@5545
   142
qed_spec_mp "NCons_normal";
paulson@5545
   143
paulson@5545
   144
Addsimps [NCons_normal];
paulson@5545
   145
paulson@5545
   146
Goal "NCons w True ~= Pls";
paulson@5545
   147
by (induct_tac "w" 1);
paulson@5545
   148
by Auto_tac;
paulson@5545
   149
qed "NCons_True";
paulson@5545
   150
paulson@5545
   151
Goal "NCons w False ~= Min";
paulson@5545
   152
by (induct_tac "w" 1);
paulson@5545
   153
by Auto_tac;
paulson@5545
   154
qed "NCons_False";
paulson@5545
   155
paulson@5545
   156
Goal "w: normal ==> bin_succ w : normal";
paulson@5545
   157
by (etac normal.induct 1);
paulson@5545
   158
by (exhaust_tac "w" 4);
paulson@5545
   159
by (auto_tac (claset(), simpset() addsimps [NCons_True, bin_succ_BIT]));
paulson@5545
   160
qed "bin_succ_normal";
paulson@5545
   161
paulson@5545
   162
Goal "w: normal ==> bin_pred w : normal";
paulson@5545
   163
by (etac normal.induct 1);
paulson@5545
   164
by (exhaust_tac "w" 3);
paulson@5545
   165
by (auto_tac (claset(), simpset() addsimps [NCons_False, bin_pred_BIT]));
paulson@5545
   166
qed "bin_pred_normal";
paulson@5545
   167
paulson@5545
   168
Addsimps [bin_succ_normal, bin_pred_normal];
paulson@5545
   169
paulson@5545
   170
Goal "w : normal --> (ALL z. z: normal --> bin_add w z : normal)";
paulson@5545
   171
by (induct_tac "w" 1);
paulson@5545
   172
by (Simp_tac 1);
paulson@5545
   173
by (Simp_tac 1);
paulson@5545
   174
by (rtac impI 1);
paulson@5545
   175
by (rtac allI 1);
paulson@5545
   176
by (induct_tac "z" 1);
paulson@5545
   177
by (ALLGOALS (asm_simp_tac (simpset() addsimps [bin_add_BIT])));
paulson@5545
   178
by (safe_tac (claset() addSDs [normal_BIT_D]));
paulson@5545
   179
by (ALLGOALS Asm_simp_tac);
paulson@5545
   180
qed_spec_mp "bin_add_normal";
paulson@5545
   181
paulson@5545
   182
Goal "w: normal ==> (w = Pls) = (integ_of w = #0)";
paulson@5545
   183
by (etac normal.induct 1);
paulson@5545
   184
by Auto_tac;
paulson@5545
   185
qed "normal_Pls_eq_0";
paulson@5545
   186
paulson@5545
   187
Goal "w : normal ==> bin_minus w : normal";
paulson@5545
   188
by (etac normal.induct 1);
paulson@5545
   189
by (ALLGOALS (asm_simp_tac (simpset() addsimps [bin_minus_BIT])));
paulson@5545
   190
by (resolve_tac normal.intrs 1);
paulson@5545
   191
by (assume_tac 1);
paulson@5545
   192
by (asm_full_simp_tac (simpset() addsimps [normal_Pls_eq_0]) 1);
paulson@5545
   193
by (asm_full_simp_tac 
paulson@5569
   194
    (simpset_of Int.thy addsimps [integ_of_minus, iszero_def, 
paulson@5569
   195
				  zminus_exchange]) 1);
paulson@5545
   196
qed "bin_minus_normal";
paulson@5545
   197
paulson@5545
   198
Goal "w : normal ==> z: normal --> bin_mult w z : normal";
paulson@5545
   199
by (etac normal.induct 1);
paulson@5569
   200
by (ALLGOALS
paulson@5569
   201
    (asm_simp_tac (simpset() addsimps [bin_minus_normal, bin_mult_BIT])));
paulson@5545
   202
by (safe_tac (claset() addSDs [normal_BIT_D]));
paulson@5545
   203
by (asm_simp_tac (simpset() addsimps [bin_add_normal]) 1);
paulson@5545
   204
qed_spec_mp "bin_mult_normal";
paulson@5545
   205