src/HOL/Integ/Bin.ML
author paulson
Wed Mar 03 11:15:18 1999 +0100 (1999-03-03)
changeset 6301 08245f5a436d
parent 6157 29942d3a1818
child 6394 3d9fd50fcc43
permissions -rw-r--r--
expandshort
paulson@2224
     1
(*  Title:      HOL/Integ/Bin.ML
paulson@2224
     2
    Authors:    Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@2224
     3
                David Spelt, University of Twente 
nipkow@6060
     4
                Tobias Nipkow, Technical University Munich
paulson@1632
     5
    Copyright   1994  University of Cambridge
nipkow@6060
     6
    Copyright   1996  University of Twente
nipkow@6060
     7
    Copyright   1999  TU Munich
paulson@1632
     8
nipkow@6060
     9
Arithmetic on binary integers;
nipkow@6060
    10
decision procedure for linear arithmetic.
paulson@1632
    11
*)
paulson@1632
    12
paulson@1632
    13
(** extra rules for bin_succ, bin_pred, bin_add, bin_mult **)
paulson@1632
    14
paulson@5512
    15
qed_goal "NCons_Pls_0" Bin.thy
paulson@5512
    16
    "NCons Pls False = Pls"
paulson@2224
    17
 (fn _ => [(Simp_tac 1)]);
paulson@1632
    18
paulson@5512
    19
qed_goal "NCons_Pls_1" Bin.thy
paulson@5512
    20
    "NCons Pls True = Pls BIT True"
paulson@2224
    21
 (fn _ => [(Simp_tac 1)]);
paulson@1632
    22
paulson@5512
    23
qed_goal "NCons_Min_0" Bin.thy
paulson@5512
    24
    "NCons Min False = Min BIT False"
paulson@2224
    25
 (fn _ => [(Simp_tac 1)]);
paulson@1632
    26
paulson@5512
    27
qed_goal "NCons_Min_1" Bin.thy
paulson@5512
    28
    "NCons Min True = Min"
paulson@2224
    29
 (fn _ => [(Simp_tac 1)]);
paulson@1632
    30
paulson@5512
    31
qed_goal "bin_succ_1" Bin.thy
paulson@5512
    32
    "bin_succ(w BIT True) = (bin_succ w) BIT False"
paulson@2224
    33
 (fn _ => [(Simp_tac 1)]);
paulson@1632
    34
paulson@5512
    35
qed_goal "bin_succ_0" Bin.thy
paulson@5512
    36
    "bin_succ(w BIT False) =  NCons w True"
paulson@2224
    37
 (fn _ => [(Simp_tac 1)]);
paulson@1632
    38
paulson@5512
    39
qed_goal "bin_pred_1" Bin.thy
paulson@5512
    40
    "bin_pred(w BIT True) = NCons w False"
paulson@2224
    41
 (fn _ => [(Simp_tac 1)]);
paulson@1632
    42
paulson@5512
    43
qed_goal "bin_pred_0" Bin.thy
paulson@5512
    44
    "bin_pred(w BIT False) = (bin_pred w) BIT True"
paulson@2224
    45
 (fn _ => [(Simp_tac 1)]);
paulson@1632
    46
paulson@5512
    47
qed_goal "bin_minus_1" Bin.thy
paulson@5512
    48
    "bin_minus(w BIT True) = bin_pred (NCons (bin_minus w) False)"
paulson@2224
    49
 (fn _ => [(Simp_tac 1)]);
paulson@1632
    50
paulson@5512
    51
qed_goal "bin_minus_0" Bin.thy
paulson@5512
    52
    "bin_minus(w BIT False) = (bin_minus w) BIT False"
paulson@2224
    53
 (fn _ => [(Simp_tac 1)]);
paulson@1632
    54
paulson@5491
    55
paulson@1632
    56
(*** bin_add: binary addition ***)
paulson@1632
    57
paulson@5512
    58
qed_goal "bin_add_BIT_11" Bin.thy
paulson@5512
    59
    "bin_add (v BIT True) (w BIT True) = \
paulson@5512
    60
\    NCons (bin_add v (bin_succ w)) False"
paulson@2224
    61
 (fn _ => [(Simp_tac 1)]);
paulson@1632
    62
paulson@5512
    63
qed_goal "bin_add_BIT_10" Bin.thy
paulson@5512
    64
    "bin_add (v BIT True) (w BIT False) = NCons (bin_add v w) True"
paulson@2224
    65
 (fn _ => [(Simp_tac 1)]);
paulson@1632
    66
paulson@5512
    67
qed_goal "bin_add_BIT_0" Bin.thy
paulson@5512
    68
    "bin_add (v BIT False) (w BIT y) = NCons (bin_add v w) y"
paulson@5491
    69
 (fn _ => [Auto_tac]);
paulson@1632
    70
paulson@5551
    71
Goal "bin_add w Pls = w";
paulson@5551
    72
by (induct_tac "w" 1);
paulson@5551
    73
by Auto_tac;
paulson@5551
    74
qed "bin_add_Pls_right";
paulson@1632
    75
paulson@5512
    76
qed_goal "bin_add_BIT_Min" Bin.thy
paulson@5512
    77
    "bin_add (v BIT x) Min = bin_pred (v BIT x)"
paulson@2224
    78
 (fn _ => [(Simp_tac 1)]);
paulson@1632
    79
paulson@5512
    80
qed_goal "bin_add_BIT_BIT" Bin.thy
paulson@5512
    81
    "bin_add (v BIT x) (w BIT y) = \
paulson@5512
    82
\    NCons(bin_add v (if x & y then (bin_succ w) else w)) (x~= y)"
paulson@2224
    83
 (fn _ => [(Simp_tac 1)]);
paulson@1632
    84
paulson@1632
    85
paulson@6036
    86
(*** bin_mult: binary multiplication ***)
paulson@1632
    87
paulson@5512
    88
qed_goal "bin_mult_1" Bin.thy
paulson@5512
    89
    "bin_mult (v BIT True) w = bin_add (NCons (bin_mult v w) False) w"
paulson@2224
    90
 (fn _ => [(Simp_tac 1)]);
paulson@1632
    91
paulson@5512
    92
qed_goal "bin_mult_0" Bin.thy
paulson@5512
    93
    "bin_mult (v BIT False) w = NCons (bin_mult v w) False"
paulson@2224
    94
 (fn _ => [(Simp_tac 1)]);
paulson@1632
    95
paulson@1632
    96
paulson@1632
    97
(**** The carry/borrow functions, bin_succ and bin_pred ****)
paulson@1632
    98
paulson@1632
    99
paulson@5491
   100
(**** integ_of ****)
paulson@1632
   101
paulson@5512
   102
qed_goal "integ_of_NCons" Bin.thy
paulson@5512
   103
    "integ_of(NCons w b) = integ_of(w BIT b)"
berghofe@5184
   104
 (fn _ =>[(induct_tac "w" 1),
paulson@5510
   105
          (ALLGOALS Asm_simp_tac) ]);
paulson@1632
   106
paulson@5512
   107
Addsimps [integ_of_NCons];
paulson@1632
   108
paulson@5491
   109
qed_goal "integ_of_succ" Bin.thy
paulson@5582
   110
    "integ_of(bin_succ w) = int 1 + integ_of w"
paulson@2224
   111
 (fn _ =>[(rtac bin.induct 1),
paulson@5510
   112
          (ALLGOALS(asm_simp_tac (simpset() addsimps zadd_ac))) ]);
paulson@5491
   113
paulson@5491
   114
qed_goal "integ_of_pred" Bin.thy
paulson@5582
   115
    "integ_of(bin_pred w) = - (int 1) + integ_of w"
paulson@5491
   116
 (fn _ =>[(rtac bin.induct 1),
paulson@5510
   117
          (ALLGOALS(asm_simp_tac (simpset() addsimps zadd_ac))) ]);
paulson@1632
   118
paulson@5491
   119
Goal "integ_of(bin_minus w) = - (integ_of w)";
paulson@5491
   120
by (rtac bin.induct 1);
paulson@5491
   121
by (Simp_tac 1);
paulson@5491
   122
by (Simp_tac 1);
paulson@5491
   123
by (asm_simp_tac (simpset()
paulson@5551
   124
		  delsimps [bin_pred_Pls, bin_pred_Min, bin_pred_BIT]
paulson@5491
   125
		  addsimps [integ_of_succ,integ_of_pred,
paulson@5491
   126
			    zadd_assoc]) 1);
paulson@5491
   127
qed "integ_of_minus";
paulson@1632
   128
paulson@1632
   129
 
paulson@6036
   130
val bin_add_simps = [bin_add_BIT_BIT, integ_of_succ, integ_of_pred];
paulson@1632
   131
paulson@6036
   132
(*This proof is complicated by the mutual recursion*)
paulson@5491
   133
Goal "! w. integ_of(bin_add v w) = integ_of v + integ_of w";
berghofe@5184
   134
by (induct_tac "v" 1);
nipkow@4686
   135
by (simp_tac (simpset() addsimps bin_add_simps) 1);
nipkow@4686
   136
by (simp_tac (simpset() addsimps bin_add_simps) 1);
paulson@1632
   137
by (rtac allI 1);
berghofe@5184
   138
by (induct_tac "w" 1);
paulson@5540
   139
by (ALLGOALS (asm_simp_tac (simpset() addsimps bin_add_simps @ zadd_ac)));
paulson@5491
   140
qed_spec_mp "integ_of_add";
paulson@1632
   141
paulson@5779
   142
paulson@5779
   143
(*Subtraction*)
paulson@5779
   144
Goalw [zdiff_def]
paulson@5779
   145
     "integ_of v - integ_of w = integ_of(bin_add v (bin_minus w))";
paulson@5779
   146
by (simp_tac (simpset() addsimps [integ_of_add, integ_of_minus]) 1);
paulson@5779
   147
qed "diff_integ_of_eq";
paulson@5779
   148
paulson@5512
   149
val bin_mult_simps = [zmult_zminus, integ_of_minus, integ_of_add];
paulson@1632
   150
paulson@5491
   151
Goal "integ_of(bin_mult v w) = integ_of v * integ_of w";
berghofe@5184
   152
by (induct_tac "v" 1);
nipkow@4686
   153
by (simp_tac (simpset() addsimps bin_mult_simps) 1);
nipkow@4686
   154
by (simp_tac (simpset() addsimps bin_mult_simps) 1);
paulson@5491
   155
by (asm_simp_tac
paulson@5540
   156
    (simpset() addsimps bin_mult_simps @ [zadd_zmult_distrib] @ zadd_ac) 1);
paulson@5491
   157
qed "integ_of_mult";
paulson@5491
   158
paulson@1632
   159
paulson@5491
   160
(** Simplification rules with integer constants **)
paulson@5491
   161
paulson@5491
   162
Goal "#0 + z = z";
paulson@5491
   163
by (Simp_tac 1);
paulson@5491
   164
qed "zadd_0";
paulson@5491
   165
paulson@5491
   166
Goal "z + #0 = z";
paulson@5491
   167
by (Simp_tac 1);
paulson@5491
   168
qed "zadd_0_right";
paulson@5491
   169
paulson@5592
   170
Addsimps [zadd_0, zadd_0_right];
paulson@5592
   171
paulson@5592
   172
paulson@5592
   173
(** Converting simple cases of (int n) to numerals **)
paulson@5491
   174
paulson@5592
   175
(*int 0 = #0 *)
paulson@5592
   176
bind_thm ("int_0", integ_of_Pls RS sym);
paulson@5491
   177
paulson@5592
   178
Goal "int (Suc n) = #1 + int n";
paulson@5592
   179
by (simp_tac (simpset() addsimps [zadd_int]) 1);
paulson@5592
   180
qed "int_Suc";
paulson@5510
   181
paulson@5592
   182
val int_simps = [int_0, int_Suc];
paulson@5491
   183
paulson@5491
   184
Goal "- (#0) = #0";
paulson@5491
   185
by (Simp_tac 1);
paulson@5491
   186
qed "zminus_0";
paulson@5491
   187
paulson@5491
   188
Addsimps [zminus_0];
paulson@5491
   189
paulson@5582
   190
paulson@5582
   191
Goal "#0 - x = -x";
paulson@5582
   192
by (simp_tac (simpset() addsimps [zdiff_def]) 1);
paulson@5582
   193
qed "zdiff0";
paulson@5582
   194
paulson@5582
   195
Goal "x - #0 = x";
paulson@5582
   196
by (simp_tac (simpset() addsimps [zdiff_def]) 1);
paulson@5582
   197
qed "zdiff0_right";
paulson@5582
   198
paulson@5582
   199
Goal "x - x = #0";
paulson@5582
   200
by (simp_tac (simpset() addsimps [zdiff_def]) 1);
paulson@5582
   201
qed "zdiff_self";
paulson@5582
   202
paulson@5582
   203
Addsimps [zdiff0, zdiff0_right, zdiff_self];
paulson@5582
   204
paulson@5491
   205
Goal "#0 * z = #0";
paulson@5491
   206
by (Simp_tac 1);
paulson@5491
   207
qed "zmult_0";
paulson@5491
   208
paulson@5491
   209
Goal "#1 * z = z";
paulson@5491
   210
by (Simp_tac 1);
paulson@5491
   211
qed "zmult_1";
paulson@5491
   212
paulson@5491
   213
Goal "#2 * z = z+z";
paulson@5491
   214
by (simp_tac (simpset() addsimps [zadd_zmult_distrib]) 1);
paulson@5491
   215
qed "zmult_2";
paulson@5491
   216
paulson@5491
   217
Goal "z * #0 = #0";
paulson@5491
   218
by (Simp_tac 1);
paulson@5491
   219
qed "zmult_0_right";
paulson@5491
   220
paulson@5491
   221
Goal "z * #1 = z";
paulson@5491
   222
by (Simp_tac 1);
paulson@5491
   223
qed "zmult_1_right";
paulson@5491
   224
paulson@5491
   225
Goal "z * #2 = z+z";
paulson@5491
   226
by (simp_tac (simpset() addsimps [zadd_zmult_distrib2]) 1);
paulson@5491
   227
qed "zmult_2_right";
paulson@5491
   228
paulson@5491
   229
Addsimps [zmult_0, zmult_0_right, 
paulson@5491
   230
	  zmult_1, zmult_1_right, 
paulson@5491
   231
	  zmult_2, zmult_2_right];
paulson@5491
   232
paulson@5491
   233
Goal "(w < z + #1) = (w<z | w=z)";
paulson@5592
   234
by (simp_tac (simpset() addsimps [zless_add_int_Suc_eq]) 1);
paulson@5491
   235
qed "zless_add1_eq";
paulson@5491
   236
paulson@5491
   237
Goal "(w + #1 <= z) = (w<z)";
paulson@5592
   238
by (simp_tac (simpset() addsimps [add_int_Suc_zle_eq]) 1);
paulson@5491
   239
qed "add1_zle_eq";
paulson@5491
   240
Addsimps [add1_zle_eq];
paulson@5491
   241
paulson@5540
   242
Goal "neg x = (x < #0)";
paulson@5540
   243
by (simp_tac (simpset() addsimps [neg_eq_less_nat0]) 1); 
paulson@5540
   244
qed "neg_eq_less_0"; 
paulson@5510
   245
paulson@5582
   246
Goal "(~neg x) = (int 0 <= x)";
paulson@5540
   247
by (simp_tac (simpset() addsimps [not_neg_eq_ge_nat0]) 1); 
paulson@5540
   248
qed "not_neg_eq_ge_0"; 
paulson@5510
   249
paulson@5582
   250
Goal "#0 <= int m";
paulson@5582
   251
by (Simp_tac 1);
paulson@5582
   252
qed "zero_zle_int";
paulson@5582
   253
AddIffs [zero_zle_int];
paulson@5582
   254
paulson@5510
   255
paulson@5747
   256
(** Needed because (int 0) rewrites to #0.
paulson@5747
   257
    Can these be generalized without evaluating large numbers?**)
paulson@5747
   258
paulson@5747
   259
Goal "~ (int k < #0)";
paulson@5747
   260
by (Simp_tac 1);
paulson@5747
   261
qed "int_less_0_conv";
paulson@5747
   262
paulson@5747
   263
Goal "(int k <= #0) = (k=0)";
paulson@5747
   264
by (Simp_tac 1);
paulson@5747
   265
qed "int_le_0_conv";
paulson@5747
   266
paulson@5747
   267
Goal "(int k = #0) = (k=0)";
paulson@5747
   268
by (Simp_tac 1);
paulson@5747
   269
qed "int_eq_0_conv";
paulson@5747
   270
paulson@5747
   271
Goal "(#0 = int k) = (k=0)";
paulson@5747
   272
by Auto_tac;
paulson@5747
   273
qed "int_eq_0_conv'";
paulson@5747
   274
paulson@5747
   275
Addsimps [int_less_0_conv, int_le_0_conv, int_eq_0_conv, int_eq_0_conv'];
paulson@5747
   276
paulson@5747
   277
paulson@5491
   278
(** Simplification rules for comparison of binary numbers (Norbert Voelker) **)
paulson@5491
   279
paulson@5491
   280
(** Equals (=) **)
paulson@1632
   281
paulson@5491
   282
Goalw [iszero_def]
paulson@5779
   283
  "(integ_of x = integ_of y) = iszero(integ_of (bin_add x (bin_minus y)))"; 
paulson@5491
   284
by (simp_tac (simpset() addsimps
paulson@5491
   285
              (zcompare_rls @ [integ_of_add, integ_of_minus])) 1); 
paulson@5491
   286
qed "eq_integ_of_eq"; 
paulson@5491
   287
paulson@5512
   288
Goalw [iszero_def] "iszero (integ_of Pls)"; 
paulson@5491
   289
by (Simp_tac 1); 
paulson@5512
   290
qed "iszero_integ_of_Pls"; 
paulson@5491
   291
paulson@5512
   292
Goalw [iszero_def] "~ iszero(integ_of Min)"; 
paulson@5491
   293
by (Simp_tac 1);
paulson@5512
   294
qed "nonzero_integ_of_Min"; 
paulson@5491
   295
paulson@5491
   296
Goalw [iszero_def]
paulson@5512
   297
     "iszero (integ_of (w BIT x)) = (~x & iszero (integ_of w))"; 
paulson@5491
   298
by (Simp_tac 1);
paulson@5491
   299
by (int_case_tac "integ_of w" 1); 
paulson@5491
   300
by (ALLGOALS (asm_simp_tac 
paulson@5540
   301
	      (simpset() addsimps zcompare_rls @ 
paulson@5540
   302
				  [zminus_zadd_distrib RS sym, 
paulson@5582
   303
				   zadd_int]))); 
paulson@5512
   304
qed "iszero_integ_of_BIT"; 
paulson@5491
   305
paulson@5779
   306
Goal "iszero (integ_of (w BIT False)) = iszero (integ_of w)"; 
paulson@5779
   307
by (simp_tac (HOL_ss addsimps [iszero_integ_of_BIT]) 1); 
paulson@5779
   308
qed "iszero_integ_of_0"; 
paulson@5779
   309
paulson@5779
   310
Goal "~ iszero (integ_of (w BIT True))"; 
paulson@5779
   311
by (simp_tac (HOL_ss addsimps [iszero_integ_of_BIT]) 1); 
paulson@5779
   312
qed "iszero_integ_of_1"; 
paulson@5779
   313
paulson@5779
   314
paulson@5491
   315
paulson@5491
   316
(** Less-than (<) **)
paulson@5491
   317
paulson@5491
   318
Goalw [zless_def,zdiff_def] 
paulson@5491
   319
    "integ_of x < integ_of y \
paulson@5540
   320
\    = neg (integ_of (bin_add x (bin_minus y)))";
paulson@5491
   321
by (simp_tac (simpset() addsimps bin_mult_simps) 1);
paulson@5540
   322
qed "less_integ_of_eq_neg"; 
paulson@5491
   323
paulson@5540
   324
Goal "~ neg (integ_of Pls)"; 
paulson@5491
   325
by (Simp_tac 1); 
paulson@5512
   326
qed "not_neg_integ_of_Pls"; 
paulson@5491
   327
paulson@5540
   328
Goal "neg (integ_of Min)"; 
paulson@5491
   329
by (Simp_tac 1);
paulson@5512
   330
qed "neg_integ_of_Min"; 
paulson@5491
   331
paulson@5540
   332
Goal "neg (integ_of (w BIT x)) = neg (integ_of w)"; 
paulson@5491
   333
by (Asm_simp_tac 1); 
paulson@5491
   334
by (int_case_tac "integ_of w" 1); 
paulson@5491
   335
by (ALLGOALS (asm_simp_tac 
paulson@5582
   336
	      (simpset() addsimps [zadd_int, neg_eq_less_nat0, 
paulson@5540
   337
				   symmetric zdiff_def] @ zcompare_rls))); 
paulson@5512
   338
qed "neg_integ_of_BIT"; 
paulson@5491
   339
paulson@5491
   340
paulson@5491
   341
(** Less-than-or-equals (<=) **)
paulson@5491
   342
paulson@5491
   343
Goal "(integ_of x <= integ_of y) = (~ integ_of y < integ_of x)";
paulson@5491
   344
by (simp_tac (simpset() addsimps [zle_def]) 1);
paulson@5491
   345
qed "le_integ_of_eq_not_less"; 
paulson@5491
   346
paulson@5540
   347
(*Delete the original rewrites, with their clumsy conditional expressions*)
paulson@5551
   348
Delsimps [bin_succ_BIT, bin_pred_BIT, bin_minus_BIT, 
paulson@5551
   349
          NCons_Pls, NCons_Min, bin_add_BIT, bin_mult_BIT];
paulson@5491
   350
paulson@5491
   351
(*Hide the binary representation of integer constants*)
paulson@5540
   352
Delsimps [integ_of_Pls, integ_of_Min, integ_of_BIT];
paulson@5491
   353
paulson@5779
   354
(*simplification of arithmetic operations on integer constants*)
paulson@5779
   355
val bin_arith_extra_simps =
paulson@5779
   356
    [integ_of_add RS sym,
paulson@5779
   357
     integ_of_minus RS sym,
paulson@5779
   358
     integ_of_mult RS sym,
paulson@5779
   359
     bin_succ_1, bin_succ_0, 
paulson@5779
   360
     bin_pred_1, bin_pred_0, 
paulson@5779
   361
     bin_minus_1, bin_minus_0,  
paulson@5779
   362
     bin_add_Pls_right, bin_add_BIT_Min,
paulson@5779
   363
     bin_add_BIT_0, bin_add_BIT_10, bin_add_BIT_11,
paulson@5779
   364
     diff_integ_of_eq, 
paulson@5779
   365
     bin_mult_1, bin_mult_0, 
paulson@5779
   366
     NCons_Pls_0, NCons_Pls_1, 
paulson@5779
   367
     NCons_Min_0, NCons_Min_1, NCons_BIT];
paulson@2224
   368
paulson@5779
   369
(*For making a minimal simpset, one must include these default simprules
paulson@5779
   370
  of Bin.thy.  Also include simp_thms, or at least (~False)=True*)
paulson@5779
   371
val bin_arith_simps =
paulson@5779
   372
    [bin_pred_Pls, bin_pred_Min,
paulson@5779
   373
     bin_succ_Pls, bin_succ_Min,
paulson@5779
   374
     bin_add_Pls, bin_add_Min,
paulson@5779
   375
     bin_minus_Pls, bin_minus_Min,
paulson@5779
   376
     bin_mult_Pls, bin_mult_Min] @ bin_arith_extra_simps;
paulson@2224
   377
paulson@5779
   378
(*Simplification of relational operations*)
paulson@5779
   379
val bin_rel_simps =
paulson@5779
   380
    [eq_integ_of_eq, iszero_integ_of_Pls, nonzero_integ_of_Min,
paulson@5779
   381
     iszero_integ_of_0, iszero_integ_of_1,
paulson@5779
   382
     less_integ_of_eq_neg,
paulson@5779
   383
     not_neg_integ_of_Pls, neg_integ_of_Min, neg_integ_of_BIT,
paulson@5779
   384
     le_integ_of_eq_not_less];
paulson@2224
   385
paulson@5779
   386
Addsimps bin_arith_extra_simps;
paulson@5779
   387
Addsimps bin_rel_simps;
paulson@5510
   388
nipkow@6060
   389
(*---------------------------------------------------------------------------*)
nipkow@6060
   390
(* Linear arithmetic                                                         *)
nipkow@6060
   391
(*---------------------------------------------------------------------------*)
nipkow@6060
   392
nipkow@6060
   393
(*
nipkow@6060
   394
Instantiation of the generic linear arithmetic package for int.
nipkow@6060
   395
FIXME: multiplication with constants (eg #2 * i) does not work yet.
nipkow@6060
   396
Solution: the cancellation simprocs in Int_Cancel should be able to deal with
nipkow@6060
   397
it (eg simplify #3 * i <= 2 * i to i <= #0) or `add_rules' below should
nipkow@6060
   398
include rules for turning multiplication with constants into addition.
nipkow@6060
   399
(The latter option is very inefficient!)
nipkow@6060
   400
*)
nipkow@6060
   401
nipkow@6128
   402
structure Int_LA_Data(*: LIN_ARITH_DATA*) =
nipkow@6060
   403
struct
nipkow@6101
   404
nipkow@6128
   405
val lessD = Nat_LA_Data.lessD @ [add1_zle_eq RS iffD2];
nipkow@6060
   406
nipkow@6060
   407
(* borrowed from Bin.thy: *)
nipkow@6060
   408
fun dest_bit (Const ("False", _)) = 0
nipkow@6060
   409
  | dest_bit (Const ("True", _)) = 1
nipkow@6060
   410
  | dest_bit _ = raise Match;
nipkow@6060
   411
nipkow@6060
   412
fun dest_bin tm =
nipkow@6060
   413
  let
nipkow@6060
   414
    fun bin_of (Const ("Bin.bin.Pls", _)) = []
nipkow@6060
   415
      | bin_of (Const ("Bin.bin.Min", _)) = [~1]
nipkow@6060
   416
      | bin_of (Const ("Bin.bin.op BIT", _) $ bs $ b) = dest_bit b :: bin_of bs
nipkow@6060
   417
      | bin_of _ = raise Match;
nipkow@6060
   418
nipkow@6060
   419
    fun int_of [] = 0
nipkow@6060
   420
      | int_of (b :: bs) = b + 2 * int_of bs;
nipkow@6060
   421
nipkow@6060
   422
  in int_of(bin_of tm) end;
nipkow@6060
   423
nipkow@6060
   424
fun add_atom(t,m,(p,i)) = (case assoc(p,t) of None => ((t,m)::p,i)
nipkow@6060
   425
                           | Some n => (overwrite(p,(t,n+m:int)), i));
nipkow@6060
   426
nipkow@6060
   427
(* Turn term into list of summand * multiplicity plus a constant *)
nipkow@6060
   428
fun poly(Const("op +",_) $ s $ t, m, pi) = poly(s,m,poly(t,m,pi))
nipkow@6060
   429
  | poly(Const("op -",_) $ s $ t, m, pi) = poly(s,m,poly(t,~1*m,pi))
nipkow@6060
   430
  | poly(Const("uminus",_) $ t, m, pi) =   poly(t,~1*m,pi)
nipkow@6060
   431
  | poly(all as Const("op *",_) $ (Const("Bin.integ_of",_)$c) $ t, m, pi) =
nipkow@6060
   432
      (poly(t,m*dest_bin c,pi) handle Match => add_atom(all,m,pi))
nipkow@6060
   433
  | poly(all as Const("Bin.integ_of",_)$t,m,(p,i)) =
nipkow@6060
   434
     ((p,i + m*dest_bin t) handle Match => add_atom(all,m,(p,i)))
nipkow@6060
   435
  | poly x  = add_atom x;
nipkow@6060
   436
nipkow@6128
   437
fun decomp2(rel,lhs,rhs) =
nipkow@6060
   438
  let val (p,i) = poly(lhs,1,([],0)) and (q,j) = poly(rhs,1,([],0))
nipkow@6060
   439
  in case rel of
nipkow@6060
   440
       "op <"  => Some(p,i,"<",q,j)
nipkow@6060
   441
     | "op <=" => Some(p,i,"<=",q,j)
nipkow@6060
   442
     | "op ="  => Some(p,i,"=",q,j)
nipkow@6060
   443
     | _       => None
nipkow@6060
   444
  end;
nipkow@6060
   445
nipkow@6128
   446
val intT = Type("IntDef.int",[]);
nipkow@6128
   447
fun iib T = T = ([intT,intT] ---> HOLogic.boolT);
nipkow@6060
   448
nipkow@6128
   449
fun decomp1(T,xxx) =
nipkow@6128
   450
  if iib T then decomp2 xxx else Nat_LA_Data.decomp1(T,xxx);
nipkow@6128
   451
nipkow@6128
   452
fun decomp(_$(Const(rel,T)$lhs$rhs)) = decomp1(T,(rel,lhs,rhs))
nipkow@6060
   453
  | decomp(_$(Const("Not",_)$(Const(rel,T)$lhs$rhs))) =
nipkow@6128
   454
      Nat_LA_Data.negate(decomp1(T,(rel,lhs,rhs)))
nipkow@6060
   455
  | decomp _ = None
nipkow@6060
   456
nipkow@6060
   457
(* reduce contradictory <= to False *)
nipkow@6060
   458
val add_rules = simp_thms@bin_arith_simps@bin_rel_simps@[int_0];
nipkow@6060
   459
nipkow@6128
   460
val cancel_sums_ss = Nat_LA_Data.cancel_sums_ss addsimps add_rules
nipkow@6060
   461
          addsimprocs [Int_Cancel.sum_conv, Int_Cancel.rel_conv];
nipkow@6060
   462
nipkow@6060
   463
val simp = simplify cancel_sums_ss;
nipkow@6060
   464
nipkow@6128
   465
val add_mono_thms = Nat_LA_Data.add_mono_thms @
nipkow@6128
   466
  map (fn s => prove_goal Int.thy s
nipkow@6128
   467
                 (fn prems => [cut_facts_tac prems 1,
nipkow@6128
   468
                      asm_simp_tac (simpset() addsimps [zadd_zle_mono]) 1]))
nipkow@6128
   469
    ["(i <= j) & (k <= l) ==> i + k <= j + (l::int)",
nipkow@6128
   470
     "(i  = j) & (k <= l) ==> i + k <= j + (l::int)",
nipkow@6128
   471
     "(i <= j) & (k  = l) ==> i + k <= j + (l::int)",
nipkow@6128
   472
     "(i  = j) & (k  = l) ==> i + k  = j + (l::int)"
nipkow@6128
   473
    ];
nipkow@6060
   474
nipkow@6060
   475
end;
nipkow@6060
   476
nipkow@6128
   477
(* Update parameters of arithmetic prover *)
nipkow@6128
   478
LA_Data_Ref.add_mono_thms := Int_LA_Data.add_mono_thms;
nipkow@6128
   479
LA_Data_Ref.lessD :=         Int_LA_Data.lessD;
nipkow@6128
   480
LA_Data_Ref.decomp :=        Int_LA_Data.decomp;
nipkow@6128
   481
LA_Data_Ref.simp :=          Int_LA_Data.simp;
nipkow@6128
   482
nipkow@6060
   483
nipkow@6128
   484
val int_arith_simproc_pats =
nipkow@6128
   485
  map (fn s => Thm.read_cterm (sign_of Int.thy) (s, HOLogic.boolT))
nipkow@6128
   486
      ["(m::int) < n","(m::int) <= n", "(m::int) = n"];
nipkow@6060
   487
nipkow@6128
   488
val fast_int_arith_simproc = mk_simproc "fast_int_arith" int_arith_simproc_pats
nipkow@6128
   489
                                        Fast_Arith.lin_arith_prover;
nipkow@6128
   490
nipkow@6128
   491
Addsimprocs [fast_int_arith_simproc];
nipkow@6060
   492
nipkow@6060
   493
(* FIXME: K true should be replaced by a sensible test to speed things up
nipkow@6060
   494
   in case there are lots of irrelevant terms involved.
nipkow@6157
   495
nipkow@6128
   496
val arith_tac =
nipkow@6128
   497
  refute_tac (K true) (REPEAT o split_tac[nat_diff_split])
nipkow@6128
   498
             ((REPEAT_DETERM o etac linorder_neqE) THEN' fast_arith_tac);
nipkow@6157
   499
*)
nipkow@6060
   500
nipkow@6060
   501
(* Some test data
nipkow@6060
   502
Goal "!!a::int. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d";
paulson@6301
   503
by (fast_arith_tac 1);
nipkow@6060
   504
Goal "!!a::int. [| a < b; c < d |] ==> a-d+ #2 <= b+(-c)";
paulson@6301
   505
by (fast_arith_tac 1);
nipkow@6060
   506
Goal "!!a::int. [| a < b; c < d |] ==> a+c+ #1 < b+d";
paulson@6301
   507
by (fast_arith_tac 1);
nipkow@6060
   508
Goal "!!a::int. [| a <= b; b+b <= c |] ==> a+a <= c";
paulson@6301
   509
by (fast_arith_tac 1);
nipkow@6060
   510
Goal "!!a::int. [| a+b <= i+j; a<=b; i<=j |] \
nipkow@6060
   511
\     ==> a+a <= j+j";
paulson@6301
   512
by (fast_arith_tac 1);
nipkow@6060
   513
Goal "!!a::int. [| a+b < i+j; a<b; i<j |] \
nipkow@6060
   514
\     ==> a+a - - #-1 < j+j - #3";
paulson@6301
   515
by (fast_arith_tac 1);
nipkow@6060
   516
Goal "!!a::int. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k";
paulson@6301
   517
by (arith_tac 1);
nipkow@6060
   518
Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
nipkow@6060
   519
\     ==> a <= l";
paulson@6301
   520
by (fast_arith_tac 1);
nipkow@6060
   521
Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
nipkow@6060
   522
\     ==> a+a+a+a <= l+l+l+l";
paulson@6301
   523
by (fast_arith_tac 1);
nipkow@6060
   524
Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
nipkow@6060
   525
\     ==> a+a+a+a+a <= l+l+l+l+i";
paulson@6301
   526
by (fast_arith_tac 1);
nipkow@6060
   527
Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
nipkow@6060
   528
\     ==> a+a+a+a+a+a <= l+l+l+l+i+l";
paulson@6301
   529
by (fast_arith_tac 1);
nipkow@6060
   530
*)
nipkow@6060
   531
nipkow@6060
   532
(*---------------------------------------------------------------------------*)
nipkow@6060
   533
(* End of linear arithmetic                                                  *)
nipkow@6060
   534
(*---------------------------------------------------------------------------*)
paulson@5510
   535
paulson@5592
   536
(** Simplification of arithmetic when nested to the right **)
paulson@5592
   537
paulson@5592
   538
Goal "integ_of v + (integ_of w + z) = integ_of(bin_add v w) + z";
paulson@5592
   539
by (simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1);
paulson@5592
   540
qed "add_integ_of_left";
paulson@5592
   541
paulson@5592
   542
Goal "integ_of v * (integ_of w * z) = integ_of(bin_mult v w) * z";
paulson@5592
   543
by (simp_tac (simpset() addsimps [zmult_assoc RS sym]) 1);
paulson@5592
   544
qed "mult_integ_of_left";
paulson@5592
   545
paulson@5592
   546
Addsimps [add_integ_of_left, mult_integ_of_left];
paulson@5592
   547
paulson@5510
   548
(** Simplification of inequalities involving numerical constants **)
paulson@5510
   549
paulson@5510
   550
Goal "(w <= z + #1) = (w<=z | w = z + #1)";
paulson@6301
   551
by (arith_tac 1);
paulson@5510
   552
qed "zle_add1_eq";
paulson@5510
   553
paulson@5510
   554
Goal "(w <= z - #1) = (w<z)";
paulson@6301
   555
by (arith_tac 1);
paulson@5510
   556
qed "zle_diff1_eq";
paulson@5510
   557
Addsimps [zle_diff1_eq];
paulson@5510
   558
paulson@5510
   559
(*2nd premise can be proved automatically if v is a literal*)
paulson@5510
   560
Goal "[| w <= z; #0 <= v |] ==> w <= z + v";
paulson@6301
   561
by (fast_arith_tac 1);
paulson@5510
   562
qed "zle_imp_zle_zadd";
paulson@5510
   563
paulson@5510
   564
Goal "w <= z ==> w <= z + #1";
paulson@6301
   565
by (fast_arith_tac 1);
paulson@5510
   566
qed "zle_imp_zle_zadd1";
paulson@5510
   567
paulson@5510
   568
(*2nd premise can be proved automatically if v is a literal*)
paulson@5510
   569
Goal "[| w < z; #0 <= v |] ==> w < z + v";
paulson@6301
   570
by (fast_arith_tac 1);
paulson@5510
   571
qed "zless_imp_zless_zadd";
paulson@5510
   572
paulson@5510
   573
Goal "w < z ==> w < z + #1";
paulson@6301
   574
by (fast_arith_tac 1);
paulson@5510
   575
qed "zless_imp_zless_zadd1";
paulson@5510
   576
paulson@5510
   577
Goal "(w < z + #1) = (w<=z)";
paulson@6301
   578
by (arith_tac 1);
paulson@5510
   579
qed "zle_add1_eq_le";
paulson@5510
   580
Addsimps [zle_add1_eq_le];
paulson@5510
   581
paulson@5510
   582
Goal "(z = z + w) = (w = #0)";
paulson@6301
   583
by (arith_tac 1);
paulson@5510
   584
qed "zadd_left_cancel0";
paulson@5510
   585
Addsimps [zadd_left_cancel0];
paulson@5510
   586
paulson@5510
   587
(*LOOPS as a simprule!*)
paulson@5510
   588
Goal "[| w + v < z; #0 <= v |] ==> w < z";
paulson@6301
   589
by (fast_arith_tac 1);
paulson@5510
   590
qed "zless_zadd_imp_zless";
paulson@5510
   591
paulson@5540
   592
(*LOOPS as a simprule!  Analogous to Suc_lessD*)
paulson@5510
   593
Goal "w + #1 < z ==> w < z";
paulson@6301
   594
by (fast_arith_tac 1);
paulson@5510
   595
qed "zless_zadd1_imp_zless";
paulson@5510
   596
paulson@5551
   597
Goal "w + #-1 = w - #1";
paulson@5582
   598
by (Simp_tac 1);
paulson@5551
   599
qed "zplus_minus1_conv";
paulson@5510
   600
paulson@5551
   601
paulson@5562
   602
(*** nat ***)
paulson@5551
   603
paulson@5582
   604
Goal "#0 <= z ==> int (nat z) = z"; 
paulson@5551
   605
by (asm_full_simp_tac
paulson@5562
   606
    (simpset() addsimps [neg_eq_less_0, zle_def, not_neg_nat]) 1); 
paulson@5562
   607
qed "nat_0_le"; 
paulson@5551
   608
paulson@5562
   609
Goal "z < #0 ==> nat z = 0"; 
paulson@5551
   610
by (asm_full_simp_tac
paulson@5562
   611
    (simpset() addsimps [neg_eq_less_0, zle_def, neg_nat]) 1); 
paulson@5562
   612
qed "nat_less_0"; 
paulson@5551
   613
paulson@5562
   614
Addsimps [nat_0_le, nat_less_0];
paulson@5551
   615
paulson@5582
   616
Goal "#0 <= w ==> (nat w = m) = (w = int m)";
paulson@5551
   617
by Auto_tac;
paulson@5562
   618
qed "nat_eq_iff";
paulson@5551
   619
paulson@5582
   620
Goal "#0 <= w ==> (nat w < m) = (w < int m)";
paulson@5551
   621
by (rtac iffI 1);
paulson@5551
   622
by (asm_full_simp_tac 
paulson@5582
   623
    (simpset() delsimps [zless_int] addsimps [zless_int RS sym]) 2);
paulson@5562
   624
by (etac (nat_0_le RS subst) 1);
paulson@5551
   625
by (Simp_tac 1);
paulson@5562
   626
qed "nat_less_iff";
paulson@5551
   627
paulson@5747
   628
paulson@5779
   629
(*Users don't want to see (int 0) or w + - z*)
paulson@5779
   630
Addsimps [int_0, symmetric zdiff_def];
paulson@5747
   631
paulson@5562
   632
Goal "#0 <= w ==> (nat w < nat z) = (w<z)";
paulson@5551
   633
by (case_tac "neg z" 1);
paulson@5562
   634
by (auto_tac (claset(), simpset() addsimps [nat_less_iff]));
paulson@5551
   635
by (auto_tac (claset() addIs [zless_trans], 
paulson@5747
   636
	      simpset() addsimps [neg_eq_less_0, zle_def]));
paulson@5562
   637
qed "nat_less_eq_zless";
paulson@5747
   638