src/HOL/ex/BinEx.ML
author paulson
Thu Sep 24 15:20:29 1998 +0200 (1998-09-24)
changeset 5545 9117a0e2bf31
parent 5513 3896c7894a57
child 5569 8c7e1190e789
permissions -rw-r--r--
added correctness proofs for arithmetic
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@5545
    86
Addsimps normal.intrs;
paulson@5545
    87
paulson@5545
    88
Goal "(w BIT b): normal ==> (w BIT b BIT c): normal";
paulson@5545
    89
by (case_tac "c" 1);
paulson@5545
    90
by Auto_tac;
paulson@5545
    91
qed "normal_BIT_I";
paulson@5545
    92
paulson@5545
    93
Addsimps [normal_BIT_I];
paulson@5545
    94
paulson@5545
    95
Goal "w BIT b: normal ==> w: normal";
paulson@5545
    96
by (etac normal.elim 1);
paulson@5545
    97
by Auto_tac;
paulson@5545
    98
qed "normal_BIT_D";
paulson@5545
    99
paulson@5545
   100
Goal "w : normal --> NCons w b : normal";
paulson@5545
   101
by (induct_tac "w" 1);
paulson@5545
   102
by (auto_tac (claset(), simpset() addsimps [NCons_Pls, NCons_Min]));
paulson@5545
   103
qed_spec_mp "NCons_normal";
paulson@5545
   104
paulson@5545
   105
Addsimps [NCons_normal];
paulson@5545
   106
paulson@5545
   107
Goal "NCons w True ~= Pls";
paulson@5545
   108
by (induct_tac "w" 1);
paulson@5545
   109
by Auto_tac;
paulson@5545
   110
qed "NCons_True";
paulson@5545
   111
paulson@5545
   112
Goal "NCons w False ~= Min";
paulson@5545
   113
by (induct_tac "w" 1);
paulson@5545
   114
by Auto_tac;
paulson@5545
   115
qed "NCons_False";
paulson@5545
   116
paulson@5545
   117
Goal "w: normal ==> bin_succ w : normal";
paulson@5545
   118
by (etac normal.induct 1);
paulson@5545
   119
by (exhaust_tac "w" 4);
paulson@5545
   120
by (auto_tac (claset(), simpset() addsimps [NCons_True, bin_succ_BIT]));
paulson@5545
   121
qed "bin_succ_normal";
paulson@5545
   122
paulson@5545
   123
Goal "w: normal ==> bin_pred w : normal";
paulson@5545
   124
by (etac normal.induct 1);
paulson@5545
   125
by (exhaust_tac "w" 3);
paulson@5545
   126
by (auto_tac (claset(), simpset() addsimps [NCons_False, bin_pred_BIT]));
paulson@5545
   127
qed "bin_pred_normal";
paulson@5545
   128
paulson@5545
   129
Addsimps [bin_succ_normal, bin_pred_normal];
paulson@5545
   130
paulson@5545
   131
Goal "w : normal --> (ALL z. z: normal --> bin_add w z : normal)";
paulson@5545
   132
by (induct_tac "w" 1);
paulson@5545
   133
by (Simp_tac 1);
paulson@5545
   134
by (Simp_tac 1);
paulson@5545
   135
by (rtac impI 1);
paulson@5545
   136
by (rtac allI 1);
paulson@5545
   137
by (induct_tac "z" 1);
paulson@5545
   138
by (ALLGOALS (asm_simp_tac (simpset() addsimps [bin_add_BIT])));
paulson@5545
   139
by (safe_tac (claset() addSDs [normal_BIT_D]));
paulson@5545
   140
by (ALLGOALS Asm_simp_tac);
paulson@5545
   141
qed_spec_mp "bin_add_normal";
paulson@5545
   142
paulson@5545
   143
paulson@5545
   144
paulson@5545
   145
Goal "w: normal ==> (w = Pls) = (integ_of w = #0)";
paulson@5545
   146
by (etac normal.induct 1);
paulson@5545
   147
by Auto_tac;
paulson@5545
   148
qed "normal_Pls_eq_0";
paulson@5545
   149
paulson@5545
   150
Goal "w : normal ==> bin_minus w : normal";
paulson@5545
   151
by (etac normal.induct 1);
paulson@5545
   152
by (ALLGOALS (asm_simp_tac (simpset() addsimps [bin_minus_BIT])));
paulson@5545
   153
by (resolve_tac normal.intrs 1);
paulson@5545
   154
by (assume_tac 1);
paulson@5545
   155
by (asm_full_simp_tac (simpset() addsimps [normal_Pls_eq_0]) 1);
paulson@5545
   156
by (asm_full_simp_tac 
paulson@5545
   157
    (simpset_of Integ.thy addsimps [integ_of_minus, iszero_def, 
paulson@5545
   158
				    zminus_exchange]) 1);
paulson@5545
   159
qed "bin_minus_normal";
paulson@5545
   160
paulson@5545
   161
paulson@5545
   162
Goal "w : normal ==> z: normal --> bin_mult w z : normal";
paulson@5545
   163
by (etac normal.induct 1);
paulson@5545
   164
by (ALLGOALS (asm_simp_tac (simpset() addsimps [bin_minus_normal,
paulson@5545
   165
						bin_mult_BIT])));
paulson@5545
   166
by (safe_tac (claset() addSDs [normal_BIT_D]));
paulson@5545
   167
by (asm_simp_tac (simpset() addsimps [bin_add_normal]) 1);
paulson@5545
   168
qed_spec_mp "bin_mult_normal";
paulson@5545
   169