src/HOL/Integ/IntArith.ML
author paulson
Fri Jun 16 13:21:17 2000 +0200 (2000-06-16)
changeset 9079 8e9b7095bf59
parent 9063 0d7628966069
child 9214 9454f30eacc7
permissions -rw-r--r--
some missing simprules for integer linear arithmetic
wenzelm@7707
     1
(*  Title:      HOL/Integ/IntArith.thy
wenzelm@7707
     2
    ID:         $Id$
wenzelm@7707
     3
    Authors:    Larry Paulson and Tobias Nipkow
wenzelm@7707
     4
wenzelm@7707
     5
Simprocs and decision procedure for linear arithmetic.
wenzelm@7707
     6
*)
wenzelm@7707
     7
wenzelm@7707
     8
(*** Simprocs for numeric literals ***)
wenzelm@7707
     9
wenzelm@7707
    10
(** Combining of literal coefficients in sums of products **)
wenzelm@7707
    11
wenzelm@7707
    12
Goal "(x < y) = (x-y < (#0::int))";
wenzelm@7707
    13
by (simp_tac (simpset() addsimps zcompare_rls) 1);
wenzelm@7707
    14
qed "zless_iff_zdiff_zless_0";
wenzelm@7707
    15
wenzelm@7707
    16
Goal "(x = y) = (x-y = (#0::int))";
wenzelm@7707
    17
by (simp_tac (simpset() addsimps zcompare_rls) 1);
wenzelm@7707
    18
qed "eq_iff_zdiff_eq_0";
wenzelm@7707
    19
wenzelm@7707
    20
Goal "(x <= y) = (x-y <= (#0::int))";
wenzelm@7707
    21
by (simp_tac (simpset() addsimps zcompare_rls) 1);
wenzelm@7707
    22
qed "zle_iff_zdiff_zle_0";
wenzelm@7707
    23
wenzelm@7707
    24
paulson@8785
    25
(** For combine_numerals **)
paulson@8785
    26
paulson@8785
    27
Goal "i*u + (j*u + k) = (i+j)*u + (k::int)";
paulson@8785
    28
by (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib]) 1);
paulson@8785
    29
qed "left_zadd_zmult_distrib";
paulson@8785
    30
paulson@8785
    31
paulson@8763
    32
(** For cancel_numerals **)
paulson@8763
    33
paulson@8763
    34
val rel_iff_rel_0_rls = map (inst "y" "?u+?v")
paulson@8763
    35
                          [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0, 
paulson@8763
    36
			   zle_iff_zdiff_zle_0] @
paulson@8763
    37
		        map (inst "y" "n")
paulson@8763
    38
                          [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0, 
paulson@8763
    39
			   zle_iff_zdiff_zle_0];
paulson@8763
    40
paulson@8763
    41
Goal "!!i::int. (i*u + m = j*u + n) = ((i-j)*u + m = n)";
paulson@8763
    42
by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@
paulson@8763
    43
		                     zadd_ac@rel_iff_rel_0_rls) 1);
paulson@8763
    44
qed "eq_add_iff1";
paulson@8763
    45
paulson@8763
    46
Goal "!!i::int. (i*u + m = j*u + n) = (m = (j-i)*u + n)";
paulson@8763
    47
by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@
paulson@8763
    48
                                     zadd_ac@rel_iff_rel_0_rls) 1);
paulson@8763
    49
qed "eq_add_iff2";
paulson@8763
    50
paulson@8763
    51
Goal "!!i::int. (i*u + m < j*u + n) = ((i-j)*u + m < n)";
paulson@8763
    52
by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@
paulson@8763
    53
                                     zadd_ac@rel_iff_rel_0_rls) 1);
paulson@8763
    54
qed "less_add_iff1";
paulson@8763
    55
paulson@8763
    56
Goal "!!i::int. (i*u + m < j*u + n) = (m < (j-i)*u + n)";
paulson@8763
    57
by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@
paulson@8763
    58
                                     zadd_ac@rel_iff_rel_0_rls) 1);
paulson@8763
    59
qed "less_add_iff2";
paulson@8763
    60
paulson@8763
    61
Goal "!!i::int. (i*u + m <= j*u + n) = ((i-j)*u + m <= n)";
paulson@8763
    62
by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@
paulson@8763
    63
                                     zadd_ac@rel_iff_rel_0_rls) 1);
paulson@8763
    64
qed "le_add_iff1";
paulson@8763
    65
paulson@8763
    66
Goal "!!i::int. (i*u + m <= j*u + n) = (m <= (j-i)*u + n)";
paulson@8763
    67
by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]
paulson@8763
    68
                                     @zadd_ac@rel_iff_rel_0_rls) 1);
paulson@8763
    69
qed "le_add_iff2";
paulson@8763
    70
paulson@8799
    71
(*To tidy up the result of a simproc.  Only the RHS will be simplified.*)
paulson@8834
    72
Goal "u = u' ==> (t==u) == (t==u')";
paulson@8799
    73
by Auto_tac;
paulson@8799
    74
qed "eq_cong2";
paulson@8799
    75
paulson@8763
    76
paulson@8763
    77
structure Int_Numeral_Simprocs =
paulson@8763
    78
struct
paulson@8763
    79
paulson@8763
    80
(*Utilities*)
paulson@8763
    81
paulson@8763
    82
fun mk_numeral n = HOLogic.number_of_const HOLogic.intT $ 
paulson@8763
    83
                   NumeralSyntax.mk_bin n;
paulson@8763
    84
paulson@8763
    85
(*Decodes a binary INTEGER*)
paulson@8785
    86
fun dest_numeral (Const("Numeral.number_of", _) $ w) = 
paulson@8785
    87
     (NumeralSyntax.dest_bin w
paulson@8785
    88
      handle Match => raise TERM("Int_Numeral_Simprocs.dest_numeral:1", [w]))
paulson@8785
    89
  | dest_numeral t = raise TERM("Int_Numeral_Simprocs.dest_numeral:2", [t]);
paulson@8763
    90
paulson@8763
    91
fun find_first_numeral past (t::terms) =
paulson@8763
    92
	((dest_numeral t, rev past @ terms)
paulson@8763
    93
	 handle TERM _ => find_first_numeral (t::past) terms)
paulson@8763
    94
  | find_first_numeral past [] = raise TERM("find_first_numeral", []);
paulson@8763
    95
paulson@8763
    96
val zero = mk_numeral 0;
paulson@8763
    97
val mk_plus = HOLogic.mk_binop "op +";
paulson@8763
    98
paulson@8763
    99
val uminus_const = Const ("uminus", HOLogic.intT --> HOLogic.intT);
paulson@8763
   100
paulson@8763
   101
(*Thus mk_sum[t] yields t+#0; longer sums don't have a trailing zero*)
paulson@8763
   102
fun mk_sum []        = zero
paulson@8763
   103
  | mk_sum [t,u]     = mk_plus (t, u)
paulson@8763
   104
  | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
paulson@8763
   105
paulson@8785
   106
(*this version ALWAYS includes a trailing zero*)
paulson@8785
   107
fun long_mk_sum []        = zero
paulson@8785
   108
  | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
paulson@8785
   109
paulson@8763
   110
val dest_plus = HOLogic.dest_bin "op +" HOLogic.intT;
paulson@8763
   111
paulson@8763
   112
(*decompose additions AND subtractions as a sum*)
paulson@8763
   113
fun dest_summing (pos, Const ("op +", _) $ t $ u, ts) =
paulson@8763
   114
        dest_summing (pos, t, dest_summing (pos, u, ts))
paulson@8763
   115
  | dest_summing (pos, Const ("op -", _) $ t $ u, ts) =
paulson@8763
   116
        dest_summing (pos, t, dest_summing (not pos, u, ts))
paulson@8763
   117
  | dest_summing (pos, t, ts) =
paulson@8763
   118
	if pos then t::ts else uminus_const$t :: ts;
paulson@8763
   119
paulson@8763
   120
fun dest_sum t = dest_summing (true, t, []);
paulson@8763
   121
paulson@8763
   122
val mk_diff = HOLogic.mk_binop "op -";
paulson@8763
   123
val dest_diff = HOLogic.dest_bin "op -" HOLogic.intT;
paulson@8763
   124
paulson@8763
   125
val one = mk_numeral 1;
paulson@8763
   126
val mk_times = HOLogic.mk_binop "op *";
paulson@8763
   127
paulson@8763
   128
fun mk_prod [] = one
paulson@8763
   129
  | mk_prod [t] = t
paulson@8763
   130
  | mk_prod (t :: ts) = if t = one then mk_prod ts
paulson@8763
   131
                        else mk_times (t, mk_prod ts);
paulson@8763
   132
paulson@8763
   133
val dest_times = HOLogic.dest_bin "op *" HOLogic.intT;
paulson@8763
   134
paulson@8763
   135
fun dest_prod t =
paulson@8763
   136
      let val (t,u) = dest_times t 
paulson@8763
   137
      in  dest_prod t @ dest_prod u  end
paulson@8763
   138
      handle TERM _ => [t];
paulson@8763
   139
paulson@8763
   140
(*DON'T do the obvious simplifications; that would create special cases*) 
paulson@8763
   141
fun mk_coeff (k, ts) = mk_times (mk_numeral k, ts);
paulson@8763
   142
paulson@8763
   143
(*Express t as a product of (possibly) a numeral with other sorted terms*)
paulson@8763
   144
fun dest_coeff sign (Const ("uminus", _) $ t) = dest_coeff (~sign) t
paulson@8763
   145
  | dest_coeff sign t =
paulson@8763
   146
    let val ts = sort Term.term_ord (dest_prod t)
paulson@8763
   147
	val (n, ts') = find_first_numeral [] ts
paulson@8763
   148
                          handle TERM _ => (1, ts)
paulson@8763
   149
    in (sign*n, mk_prod ts') end;
paulson@8763
   150
paulson@8763
   151
(*Find first coefficient-term THAT MATCHES u*)
paulson@8763
   152
fun find_first_coeff past u [] = raise TERM("find_first_coeff", []) 
paulson@8763
   153
  | find_first_coeff past u (t::terms) =
paulson@8763
   154
	let val (n,u') = dest_coeff 1 t
paulson@8763
   155
	in  if u aconv u' then (n, rev past @ terms)
paulson@8763
   156
			  else find_first_coeff (t::past) u terms
paulson@8763
   157
	end
paulson@8763
   158
	handle TERM _ => find_first_coeff (t::past) u terms;
paulson@8763
   159
paulson@8763
   160
paulson@8763
   161
(*Simplify #1*n and n*#1 to n*)
paulson@8763
   162
val add_0s = [zadd_0, zadd_0_right];
paulson@8763
   163
val mult_1s = [zmult_1, zmult_1_right, zmult_minus1, zmult_minus1_right];
paulson@8763
   164
paulson@8763
   165
(*To perform binary arithmetic*)
paulson@9063
   166
val bin_simps = [add_number_of_left] @ bin_arith_simps @ bin_rel_simps;
paulson@8763
   167
paulson@8787
   168
(*To evaluate binary negations of coefficients*)
paulson@8787
   169
val zminus_simps = NCons_simps @
paulson@8787
   170
                   [number_of_minus RS sym, 
paulson@8787
   171
		    bin_minus_1, bin_minus_0, bin_minus_Pls, bin_minus_Min,
paulson@8787
   172
		    bin_pred_1, bin_pred_0, bin_pred_Pls, bin_pred_Min];
paulson@8787
   173
paulson@8763
   174
(*To let us treat subtraction as addition*)
paulson@8763
   175
val diff_simps = [zdiff_def, zminus_zadd_distrib, zminus_zminus];
paulson@8763
   176
paulson@8776
   177
(*Apply the given rewrite (if present) just once*)
paulson@8799
   178
fun trans_tac None      = all_tac
paulson@8799
   179
  | trans_tac (Some th) = ALLGOALS (rtac (th RS trans));
paulson@8763
   180
paulson@8776
   181
fun prove_conv name tacs sg (t, u) =
paulson@8763
   182
  if t aconv u then None
paulson@8763
   183
  else
paulson@8799
   184
  let val ct = cterm_of sg (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u)))
paulson@8799
   185
  in Some
paulson@8799
   186
     (prove_goalw_cterm [] ct (K tacs)
paulson@8763
   187
      handle ERROR => error 
paulson@8763
   188
	  ("The error(s) above occurred while trying to prove " ^
paulson@8799
   189
	   string_of_cterm ct ^ "\nInternal failure of simproc " ^ name))
paulson@8799
   190
  end;
paulson@8799
   191
paulson@8799
   192
fun simplify_meta_eq rules =
paulson@8799
   193
    mk_meta_eq o
paulson@8834
   194
    simplify (HOL_basic_ss addeqcongs[eq_cong2] addsimps rules)
paulson@8763
   195
paulson@8763
   196
fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;
paulson@8763
   197
fun prep_pat s = Thm.read_cterm (Theory.sign_of Int.thy) (s, HOLogic.termT);
paulson@8763
   198
val prep_pats = map prep_pat;
paulson@8763
   199
paulson@8763
   200
structure CancelNumeralsCommon =
paulson@8763
   201
  struct
paulson@8763
   202
  val mk_sum    	= mk_sum
paulson@8763
   203
  val dest_sum		= dest_sum
paulson@8763
   204
  val mk_coeff		= mk_coeff
paulson@8763
   205
  val dest_coeff	= dest_coeff 1
paulson@8763
   206
  val find_first_coeff	= find_first_coeff []
paulson@8799
   207
  val trans_tac         = trans_tac
paulson@8776
   208
  val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
paulson@8787
   209
                                                     zminus_simps@zadd_ac))
paulson@8763
   210
                 THEN ALLGOALS
paulson@8776
   211
                    (simp_tac (HOL_ss addsimps [zmult_zminus_right RS sym]@
paulson@8776
   212
                                               bin_simps@zadd_ac@zmult_ac))
paulson@8763
   213
  val numeral_simp_tac	= ALLGOALS (simp_tac (HOL_ss addsimps add_0s@bin_simps))
paulson@8799
   214
  val simplify_meta_eq  = simplify_meta_eq (add_0s@mult_1s)
paulson@8763
   215
  end;
paulson@8763
   216
paulson@8763
   217
paulson@8763
   218
structure EqCancelNumerals = CancelNumeralsFun
paulson@8763
   219
 (open CancelNumeralsCommon
paulson@8776
   220
  val prove_conv = prove_conv "inteq_cancel_numerals"
paulson@8763
   221
  val mk_bal   = HOLogic.mk_eq
paulson@8763
   222
  val dest_bal = HOLogic.dest_bin "op =" HOLogic.intT
paulson@8776
   223
  val bal_add1 = eq_add_iff1 RS trans
paulson@8776
   224
  val bal_add2 = eq_add_iff2 RS trans
paulson@8763
   225
);
paulson@8763
   226
paulson@8763
   227
structure LessCancelNumerals = CancelNumeralsFun
paulson@8763
   228
 (open CancelNumeralsCommon
paulson@8776
   229
  val prove_conv = prove_conv "intless_cancel_numerals"
paulson@8763
   230
  val mk_bal   = HOLogic.mk_binrel "op <"
paulson@8763
   231
  val dest_bal = HOLogic.dest_bin "op <" HOLogic.intT
paulson@8776
   232
  val bal_add1 = less_add_iff1 RS trans
paulson@8776
   233
  val bal_add2 = less_add_iff2 RS trans
paulson@8763
   234
);
paulson@8763
   235
paulson@8763
   236
structure LeCancelNumerals = CancelNumeralsFun
paulson@8763
   237
 (open CancelNumeralsCommon
paulson@8776
   238
  val prove_conv = prove_conv "intle_cancel_numerals"
paulson@8763
   239
  val mk_bal   = HOLogic.mk_binrel "op <="
paulson@8763
   240
  val dest_bal = HOLogic.dest_bin "op <=" HOLogic.intT
paulson@8776
   241
  val bal_add1 = le_add_iff1 RS trans
paulson@8776
   242
  val bal_add2 = le_add_iff2 RS trans
paulson@8763
   243
);
paulson@8763
   244
paulson@8763
   245
val cancel_numerals = 
paulson@8763
   246
  map prep_simproc
paulson@8763
   247
   [("inteq_cancel_numerals",
paulson@8763
   248
     prep_pats ["(l::int) + m = n", "(l::int) = m + n", 
paulson@8763
   249
		"(l::int) - m = n", "(l::int) = m - n", 
paulson@8763
   250
		"(l::int) * m = n", "(l::int) = m * n"], 
paulson@8763
   251
     EqCancelNumerals.proc),
paulson@8763
   252
    ("intless_cancel_numerals", 
paulson@8763
   253
     prep_pats ["(l::int) + m < n", "(l::int) < m + n", 
paulson@8763
   254
		"(l::int) - m < n", "(l::int) < m - n", 
paulson@8763
   255
		"(l::int) * m < n", "(l::int) < m * n"], 
paulson@8763
   256
     LessCancelNumerals.proc),
paulson@8763
   257
    ("intle_cancel_numerals", 
paulson@8763
   258
     prep_pats ["(l::int) + m <= n", "(l::int) <= m + n", 
paulson@8763
   259
		"(l::int) - m <= n", "(l::int) <= m - n", 
paulson@8763
   260
		"(l::int) * m <= n", "(l::int) <= m * n"], 
paulson@8787
   261
     LeCancelNumerals.proc)];
paulson@8763
   262
paulson@8785
   263
paulson@8785
   264
structure CombineNumeralsData =
paulson@8785
   265
  struct
paulson@8785
   266
  val mk_sum    	= long_mk_sum    (*to work for e.g. #2*x + #3*x *)
paulson@8785
   267
  val dest_sum		= dest_sum
paulson@8785
   268
  val mk_coeff		= mk_coeff
paulson@8785
   269
  val dest_coeff	= dest_coeff 1
paulson@8785
   270
  val left_distrib	= left_zadd_zmult_distrib RS trans
paulson@8785
   271
  val prove_conv	= prove_conv "int_combine_numerals"
paulson@8799
   272
  val trans_tac          = trans_tac
paulson@8785
   273
  val norm_tac = ALLGOALS
paulson@8785
   274
                   (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
paulson@8787
   275
                                              zminus_simps@zadd_ac))
paulson@8785
   276
                 THEN ALLGOALS
paulson@8785
   277
                    (simp_tac (HOL_ss addsimps [zmult_zminus_right RS sym]@
paulson@8785
   278
                                               bin_simps@zadd_ac@zmult_ac))
paulson@8785
   279
  val numeral_simp_tac	= ALLGOALS 
paulson@8785
   280
                    (simp_tac (HOL_ss addsimps add_0s@bin_simps))
paulson@8799
   281
  val simplify_meta_eq  = simplify_meta_eq (add_0s@mult_1s)
paulson@8785
   282
  end;
paulson@8785
   283
paulson@8785
   284
structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
paulson@8785
   285
  
paulson@8785
   286
val combine_numerals = 
paulson@8785
   287
    prep_simproc ("int_combine_numerals",
paulson@8787
   288
		  prep_pats ["(i::int) + j", "(i::int) - j"],
paulson@8785
   289
		  CombineNumerals.proc);
paulson@8785
   290
paulson@8763
   291
end;
paulson@8763
   292
paulson@8763
   293
paulson@8763
   294
Addsimprocs Int_Numeral_Simprocs.cancel_numerals;
paulson@8785
   295
Addsimprocs [Int_Numeral_Simprocs.combine_numerals];
paulson@8785
   296
paulson@8785
   297
(*The Abel_Cancel simprocs are now obsolete*)
paulson@8785
   298
Delsimprocs [Int_Cancel.sum_conv, Int_Cancel.rel_conv];
paulson@8763
   299
paulson@8763
   300
(*examples:
paulson@8763
   301
print_depth 22;
wenzelm@9000
   302
set timing;
paulson@8763
   303
set trace_simp;
paulson@8763
   304
fun test s = (Goal s; by (Simp_tac 1)); 
paulson@8763
   305
paulson@8785
   306
test "l + #2 + #2 + #2 + (l + #2) + (oo + #2) = (uu::int)";
paulson@8785
   307
paulson@8763
   308
test "#2*u = (u::int)";
paulson@8763
   309
test "(i + j + #12 + (k::int)) - #15 = y";
paulson@8763
   310
test "(i + j + #12 + (k::int)) - #5 = y";
paulson@8763
   311
paulson@8763
   312
test "y - b < (b::int)";
paulson@8763
   313
test "y - (#3*b + c) < (b::int) - #2*c";
paulson@8763
   314
paulson@8785
   315
test "(#2*x - (u*v) + y) - v*#3*u = (w::int)";
paulson@8763
   316
test "(#2*x*u*v + (u*v)*#4 + y) - v*u*#4 = (w::int)";
paulson@8763
   317
test "(#2*x*u*v + (u*v)*#4 + y) - v*u = (w::int)";
paulson@8785
   318
test "u*v - (x*u*v + (u*v)*#4 + y) = (w::int)";
paulson@8763
   319
paulson@8763
   320
test "(i + j + #12 + (k::int)) = u + #15 + y";
paulson@8763
   321
test "(i + j*#2 + #12 + (k::int)) = j + #5 + y";
paulson@8763
   322
paulson@8763
   323
test "#2*y + #3*z + #6*w + #2*y + #3*z + #2*u = #2*y' + #3*z' + #6*w' + #2*y' + #3*z' + u + (vv::int)";
paulson@8763
   324
paulson@8785
   325
test "a + -(b+c) + b = (d::int)";
paulson@8785
   326
test "a + -(b+c) - b = (d::int)";
paulson@8785
   327
paulson@8763
   328
(*negative numerals*)
paulson@8763
   329
test "(i + j + #-2 + (k::int)) - (u + #5 + y) = zz";
paulson@8763
   330
test "(i + j + #-3 + (k::int)) < u + #5 + y";
paulson@8763
   331
test "(i + j + #3 + (k::int)) < u + #-6 + y";
paulson@8763
   332
test "(i + j + #-12 + (k::int)) - #15 = y";
paulson@8763
   333
test "(i + j + #12 + (k::int)) - #-15 = y";
paulson@8763
   334
test "(i + j + #-12 + (k::int)) - #-15 = y";
paulson@8763
   335
*)
paulson@8763
   336
paulson@8763
   337
wenzelm@7707
   338
(** Constant folding for integer plus and times **)
wenzelm@7707
   339
wenzelm@7707
   340
(*We do not need
paulson@8785
   341
    structure Nat_Plus_Assoc = Assoc_Fold (Nat_Plus_Assoc_Data);
wenzelm@7707
   342
    structure Int_Plus_Assoc = Assoc_Fold (Int_Plus_Assoc_Data);
paulson@8785
   343
  because combine_numerals does the same thing*)
wenzelm@7707
   344
wenzelm@7707
   345
structure Int_Times_Assoc_Data : ASSOC_FOLD_DATA =
wenzelm@7707
   346
struct
wenzelm@7707
   347
  val ss		= HOL_ss
wenzelm@7707
   348
  val eq_reflection	= eq_reflection
wenzelm@7707
   349
  val thy    = Bin.thy
wenzelm@7707
   350
  val T	     = HOLogic.intT
wenzelm@7707
   351
  val plus   = Const ("op *", [HOLogic.intT,HOLogic.intT] ---> HOLogic.intT);
wenzelm@7707
   352
  val add_ac = zmult_ac
wenzelm@7707
   353
end;
wenzelm@7707
   354
wenzelm@7707
   355
structure Int_Times_Assoc = Assoc_Fold (Int_Times_Assoc_Data);
wenzelm@7707
   356
wenzelm@7707
   357
Addsimprocs [Int_Times_Assoc.conv];
wenzelm@7707
   358
wenzelm@7707
   359
wenzelm@7707
   360
(** The same for the naturals **)
wenzelm@7707
   361
wenzelm@7707
   362
structure Nat_Times_Assoc_Data : ASSOC_FOLD_DATA =
wenzelm@7707
   363
struct
wenzelm@7707
   364
  val ss		= HOL_ss
wenzelm@7707
   365
  val eq_reflection	= eq_reflection
wenzelm@7707
   366
  val thy    = Bin.thy
wenzelm@7707
   367
  val T	     = HOLogic.natT
wenzelm@7707
   368
  val plus   = Const ("op *", [HOLogic.natT,HOLogic.natT] ---> HOLogic.natT);
wenzelm@7707
   369
  val add_ac = mult_ac
wenzelm@7707
   370
end;
wenzelm@7707
   371
wenzelm@7707
   372
structure Nat_Times_Assoc = Assoc_Fold (Nat_Times_Assoc_Data);
wenzelm@7707
   373
paulson@8785
   374
Addsimprocs [Nat_Times_Assoc.conv];
wenzelm@7707
   375
wenzelm@7707
   376
wenzelm@7707
   377
wenzelm@7707
   378
(*** decision procedure for linear arithmetic ***)
wenzelm@7707
   379
wenzelm@7707
   380
(*---------------------------------------------------------------------------*)
wenzelm@7707
   381
(* Linear arithmetic                                                         *)
wenzelm@7707
   382
(*---------------------------------------------------------------------------*)
wenzelm@7707
   383
wenzelm@7707
   384
(*
wenzelm@7707
   385
Instantiation of the generic linear arithmetic package for int.
wenzelm@7707
   386
*)
wenzelm@7707
   387
wenzelm@7707
   388
(* Update parameters of arithmetic prover *)
wenzelm@7707
   389
let
wenzelm@7707
   390
wenzelm@7707
   391
(* reduce contradictory <= to False *)
wenzelm@7707
   392
val add_rules = simp_thms @ bin_arith_simps @ bin_rel_simps @
paulson@8785
   393
                [int_0, zadd_0, zadd_0_right, zdiff_def,
paulson@8785
   394
		 zadd_zminus_inverse, zadd_zminus_inverse2, 
paulson@8785
   395
		 zmult_0, zmult_0_right, 
paulson@8785
   396
		 zmult_1, zmult_1_right, 
paulson@9079
   397
		 zmult_minus1, zmult_minus1_right,
paulson@9079
   398
		 zminus_zadd_distrib, zminus_zminus];
wenzelm@7707
   399
paulson@8785
   400
val simprocs = [Int_Times_Assoc.conv, Int_Numeral_Simprocs.combine_numerals]@
paulson@8785
   401
               Int_Numeral_Simprocs.cancel_numerals;
wenzelm@7707
   402
wenzelm@7707
   403
val add_mono_thms =
wenzelm@7707
   404
  map (fn s => prove_goal Int.thy s
wenzelm@7707
   405
                 (fn prems => [cut_facts_tac prems 1,
wenzelm@7707
   406
                      asm_simp_tac (simpset() addsimps [zadd_zle_mono]) 1]))
wenzelm@7707
   407
    ["(i <= j) & (k <= l) ==> i + k <= j + (l::int)",
wenzelm@7707
   408
     "(i  = j) & (k <= l) ==> i + k <= j + (l::int)",
wenzelm@7707
   409
     "(i <= j) & (k  = l) ==> i + k <= j + (l::int)",
wenzelm@7707
   410
     "(i  = j) & (k  = l) ==> i + k  = j + (l::int)"
wenzelm@7707
   411
    ];
wenzelm@7707
   412
wenzelm@7707
   413
in
wenzelm@7707
   414
LA_Data_Ref.add_mono_thms := !LA_Data_Ref.add_mono_thms @ add_mono_thms;
wenzelm@7707
   415
LA_Data_Ref.lessD := !LA_Data_Ref.lessD @ [add1_zle_eq RS iffD2];
wenzelm@7707
   416
LA_Data_Ref.ss_ref := !LA_Data_Ref.ss_ref addsimps add_rules
paulson@8796
   417
                      addsimprocs simprocs
paulson@8796
   418
                      addcongs [if_weak_cong];
wenzelm@7707
   419
LA_Data_Ref.discrete := !LA_Data_Ref.discrete @ [("IntDef.int",true)]
wenzelm@7707
   420
end;
wenzelm@7707
   421
wenzelm@7707
   422
let
wenzelm@7707
   423
val int_arith_simproc_pats =
wenzelm@7707
   424
  map (fn s => Thm.read_cterm (Theory.sign_of Int.thy) (s, HOLogic.boolT))
wenzelm@7707
   425
      ["(m::int) < n","(m::int) <= n", "(m::int) = n"];
wenzelm@7707
   426
wenzelm@7707
   427
val fast_int_arith_simproc = mk_simproc
wenzelm@7707
   428
  "fast_int_arith" int_arith_simproc_pats Fast_Arith.lin_arith_prover;
wenzelm@7707
   429
in
wenzelm@7707
   430
Addsimprocs [fast_int_arith_simproc]
wenzelm@7707
   431
end;
wenzelm@7707
   432
wenzelm@7707
   433
(* Some test data
wenzelm@7707
   434
Goal "!!a::int. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d";
wenzelm@7707
   435
by (fast_arith_tac 1);
wenzelm@7707
   436
Goal "!!a::int. [| a < b; c < d |] ==> a-d+ #2 <= b+(-c)";
wenzelm@7707
   437
by (fast_arith_tac 1);
wenzelm@7707
   438
Goal "!!a::int. [| a < b; c < d |] ==> a+c+ #1 < b+d";
wenzelm@7707
   439
by (fast_arith_tac 1);
wenzelm@7707
   440
Goal "!!a::int. [| a <= b; b+b <= c |] ==> a+a <= c";
wenzelm@7707
   441
by (fast_arith_tac 1);
wenzelm@7707
   442
Goal "!!a::int. [| a+b <= i+j; a<=b; i<=j |] \
wenzelm@7707
   443
\     ==> a+a <= j+j";
wenzelm@7707
   444
by (fast_arith_tac 1);
wenzelm@7707
   445
Goal "!!a::int. [| a+b < i+j; a<b; i<j |] \
wenzelm@7707
   446
\     ==> a+a - - #-1 < j+j - #3";
wenzelm@7707
   447
by (fast_arith_tac 1);
wenzelm@7707
   448
Goal "!!a::int. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k";
wenzelm@7707
   449
by (arith_tac 1);
wenzelm@7707
   450
Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
wenzelm@7707
   451
\     ==> a <= l";
wenzelm@7707
   452
by (fast_arith_tac 1);
wenzelm@7707
   453
Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
wenzelm@7707
   454
\     ==> a+a+a+a <= l+l+l+l";
wenzelm@7707
   455
by (fast_arith_tac 1);
wenzelm@7707
   456
Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
wenzelm@7707
   457
\     ==> a+a+a+a+a <= l+l+l+l+i";
wenzelm@7707
   458
by (fast_arith_tac 1);
wenzelm@7707
   459
Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
wenzelm@7707
   460
\     ==> a+a+a+a+a+a <= l+l+l+l+i+l";
wenzelm@7707
   461
by (fast_arith_tac 1);
nipkow@8257
   462
Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
nipkow@8257
   463
\     ==> #6*a <= #5*l+i";
nipkow@8257
   464
by (fast_arith_tac 1);
wenzelm@7707
   465
*)
wenzelm@7707
   466
wenzelm@7707
   467
(*---------------------------------------------------------------------------*)
wenzelm@7707
   468
(* End of linear arithmetic                                                  *)
wenzelm@7707
   469
(*---------------------------------------------------------------------------*)
wenzelm@7707
   470
wenzelm@7707
   471
(** Simplification of inequalities involving numerical constants **)
wenzelm@7707
   472
wenzelm@7707
   473
Goal "(w <= z - (#1::int)) = (w<(z::int))";
wenzelm@7707
   474
by (arith_tac 1);
wenzelm@7707
   475
qed "zle_diff1_eq";
wenzelm@7707
   476
Addsimps [zle_diff1_eq];
wenzelm@7707
   477
wenzelm@7707
   478
Goal "(w < z + #1) = (w<=(z::int))";
wenzelm@7707
   479
by (arith_tac 1);
wenzelm@7707
   480
qed "zle_add1_eq_le";
wenzelm@7707
   481
Addsimps [zle_add1_eq_le];
wenzelm@7707
   482
wenzelm@7707
   483
Goal "(z = z + w) = (w = (#0::int))";
wenzelm@7707
   484
by (arith_tac 1);
wenzelm@7707
   485
qed "zadd_left_cancel0";
wenzelm@7707
   486
Addsimps [zadd_left_cancel0];
wenzelm@7707
   487
wenzelm@7707
   488
wenzelm@7707
   489
(* nat *)
wenzelm@7707
   490
wenzelm@7707
   491
Goal "#0 <= z ==> int (nat z) = z"; 
wenzelm@7707
   492
by (asm_full_simp_tac
wenzelm@7707
   493
    (simpset() addsimps [neg_eq_less_0, zle_def, not_neg_nat]) 1); 
wenzelm@7707
   494
qed "nat_0_le"; 
wenzelm@7707
   495
wenzelm@7707
   496
Goal "z <= #0 ==> nat z = 0"; 
wenzelm@7707
   497
by (case_tac "z = #0" 1);
wenzelm@7707
   498
by (asm_simp_tac (simpset() addsimps [nat_le_int0]) 1); 
wenzelm@7707
   499
by (asm_full_simp_tac 
wenzelm@7707
   500
    (simpset() addsimps [neg_eq_less_0, neg_nat, linorder_neq_iff]) 1);
wenzelm@7707
   501
qed "nat_le_0"; 
wenzelm@7707
   502
wenzelm@7707
   503
Addsimps [nat_0_le, nat_le_0];
wenzelm@7707
   504
wenzelm@7707
   505
val [major,minor] = Goal "[| #0 <= z;  !!m. z = int m ==> P |] ==> P"; 
wenzelm@7707
   506
by (rtac (major RS nat_0_le RS sym RS minor) 1);
wenzelm@7707
   507
qed "nonneg_eq_int"; 
wenzelm@7707
   508
wenzelm@7707
   509
Goal "#0 <= w ==> (nat w = m) = (w = int m)";
wenzelm@7707
   510
by Auto_tac;
wenzelm@7707
   511
qed "nat_eq_iff";
wenzelm@7707
   512
paulson@8796
   513
Goal "#0 <= w ==> (m = nat w) = (w = int m)";
paulson@8796
   514
by Auto_tac;
paulson@8796
   515
qed "nat_eq_iff2";
paulson@8796
   516
wenzelm@7707
   517
Goal "#0 <= w ==> (nat w < m) = (w < int m)";
wenzelm@7707
   518
by (rtac iffI 1);
wenzelm@7707
   519
by (asm_full_simp_tac 
wenzelm@7707
   520
    (simpset() delsimps [zless_int] addsimps [zless_int RS sym]) 2);
wenzelm@7707
   521
by (etac (nat_0_le RS subst) 1);
wenzelm@7707
   522
by (Simp_tac 1);
wenzelm@7707
   523
qed "nat_less_iff";
wenzelm@7707
   524
wenzelm@7707
   525
wenzelm@7707
   526
(*Users don't want to see (int 0), int(Suc 0) or w + - z*)
wenzelm@7707
   527
Addsimps [int_0, int_Suc, symmetric zdiff_def];
wenzelm@7707
   528
wenzelm@7707
   529
Goal "nat #0 = 0";
wenzelm@7707
   530
by (simp_tac (simpset() addsimps [nat_eq_iff]) 1);
wenzelm@7707
   531
qed "nat_0";
wenzelm@7707
   532
wenzelm@7707
   533
Goal "nat #1 = 1";
wenzelm@7707
   534
by (simp_tac (simpset() addsimps [nat_eq_iff]) 1);
wenzelm@7707
   535
qed "nat_1";
wenzelm@7707
   536
wenzelm@7707
   537
Goal "nat #2 = 2";
wenzelm@7707
   538
by (simp_tac (simpset() addsimps [nat_eq_iff]) 1);
wenzelm@7707
   539
qed "nat_2";
wenzelm@7707
   540
wenzelm@7707
   541
Goal "#0 <= w ==> (nat w < nat z) = (w<z)";
wenzelm@7707
   542
by (case_tac "neg z" 1);
wenzelm@7707
   543
by (auto_tac (claset(), simpset() addsimps [nat_less_iff]));
wenzelm@7707
   544
by (auto_tac (claset() addIs [zless_trans], 
wenzelm@7707
   545
	      simpset() addsimps [neg_eq_less_0, zle_def]));
wenzelm@7707
   546
qed "nat_less_eq_zless";
wenzelm@7707
   547
wenzelm@7707
   548
Goal "#0 < w | #0 <= z ==> (nat w <= nat z) = (w<=z)";
wenzelm@7707
   549
by (auto_tac (claset(), 
wenzelm@7707
   550
	      simpset() addsimps [linorder_not_less RS sym, 
wenzelm@7707
   551
				  zless_nat_conj]));
wenzelm@7707
   552
qed "nat_le_eq_zle";
wenzelm@7707
   553
wenzelm@7707
   554
(*Analogous to zadd_int, but more easily provable using the arithmetic in Bin*)
wenzelm@7707
   555
Goal "n<=m --> int m - int n = int (m-n)";
wenzelm@7707
   556
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
wenzelm@7707
   557
by Auto_tac;
wenzelm@7707
   558
qed_spec_mp "zdiff_int";
wenzelm@7707
   559
wenzelm@7707
   560
paulson@9063
   561
(*** Some convenient biconditionals for products of signs ***)
wenzelm@7707
   562
paulson@9063
   563
Goal "[| (#0::int) < i; #0 < j |] ==> #0 < i*j";
paulson@9063
   564
by (dtac zmult_zless_mono1 1);
paulson@9063
   565
by Auto_tac; 
paulson@9063
   566
qed "zmult_pos";
wenzelm@7707
   567
paulson@9063
   568
Goal "[| i < (#0::int); j < #0 |] ==> #0 < i*j";
paulson@9063
   569
by (dtac zmult_zless_mono1_neg 1);
paulson@9063
   570
by Auto_tac; 
paulson@9063
   571
qed "zmult_neg";
wenzelm@7707
   572
paulson@9063
   573
Goal "[| (#0::int) < i; j < #0 |] ==> i*j < #0";
paulson@9063
   574
by (dtac zmult_zless_mono1_neg 1);
paulson@9063
   575
by Auto_tac; 
paulson@9063
   576
qed "zmult_pos_neg";
wenzelm@7707
   577
paulson@9063
   578
Goal "((#0::int) < x*y) = (#0 < x & #0 < y | x < #0 & y < #0)";
paulson@9063
   579
by (auto_tac (claset(), 
paulson@9063
   580
              simpset() addsimps [order_le_less, linorder_not_less,
paulson@9063
   581
	                          zmult_pos, zmult_neg]));
paulson@9063
   582
by (ALLGOALS (rtac ccontr)); 
paulson@9063
   583
by (auto_tac (claset(), 
paulson@9063
   584
	      simpset() addsimps [order_le_less, linorder_not_less]));
paulson@9063
   585
by (ALLGOALS (etac rev_mp)); 
paulson@9063
   586
by (ALLGOALS (dtac zmult_pos_neg THEN' assume_tac));
paulson@9063
   587
by (auto_tac (claset() addDs [order_less_not_sym], 
paulson@9063
   588
              simpset() addsimps [zmult_commute]));  
paulson@9063
   589
qed "int_0_less_mult_iff";
wenzelm@7707
   590
paulson@9063
   591
Goal "((#0::int) <= x*y) = (#0 <= x & #0 <= y | x <= #0 & y <= #0)";
paulson@9063
   592
by (auto_tac (claset(), 
paulson@9063
   593
              simpset() addsimps [order_le_less, linorder_not_less,  
paulson@9063
   594
                                  int_0_less_mult_iff]));
paulson@9063
   595
qed "int_0_le_mult_iff";
wenzelm@7707
   596
paulson@9063
   597
Goal "(x*y < (#0::int)) = (#0 < x & y < #0 | x < #0 & #0 < y)";
paulson@9063
   598
by (auto_tac (claset(), 
paulson@9063
   599
              simpset() addsimps [int_0_le_mult_iff, 
paulson@9063
   600
                                  linorder_not_le RS sym]));
paulson@9063
   601
by (auto_tac (claset() addDs [order_less_not_sym],  
paulson@9063
   602
              simpset() addsimps [linorder_not_le]));
paulson@9063
   603
qed "zmult_less_0_iff";
wenzelm@7707
   604
paulson@9063
   605
Goal "(x*y <= (#0::int)) = (#0 <= x & y <= #0 | x <= #0 & #0 <= y)";
paulson@9063
   606
by (auto_tac (claset() addDs [order_less_not_sym], 
paulson@9063
   607
              simpset() addsimps [int_0_less_mult_iff, 
paulson@9063
   608
                                  linorder_not_less RS sym]));
paulson@9063
   609
qed "zmult_le_0_iff";
paulson@9063
   610