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