src/HOL/Integ/NatSimprocs.ML
author wenzelm
Tue May 30 16:08:38 2000 +0200 (2000-05-30)
changeset 9000 c20d58286a51
parent 8935 548901d05a0e
child 9436 62bb04ab4b01
permissions -rw-r--r--
cleaned up;
paulson@8759
     1
(*  Title:      HOL/NatSimprocs.ML
paulson@8759
     2
    ID:         $Id$
paulson@8759
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@8759
     4
    Copyright   2000  University of Cambridge
paulson@8759
     5
paulson@8759
     6
Simprocs for nat numerals
paulson@8759
     7
*)
paulson@8759
     8
paulson@8759
     9
Goal "number_of v + (number_of v' + (k::nat)) = \
paulson@8759
    10
\        (if neg (number_of v) then number_of v' + k \
paulson@8759
    11
\         else if neg (number_of v') then number_of v + k \
paulson@8759
    12
\         else number_of (bin_add v v') + k)";
paulson@8759
    13
by (Simp_tac 1);
paulson@8766
    14
qed "nat_number_of_add_left";
paulson@8759
    15
paulson@8759
    16
paulson@8776
    17
(** For combine_numerals **)
paulson@8776
    18
paulson@8776
    19
Goal "i*u + (j*u + k) = (i+j)*u + (k::nat)";
paulson@8776
    20
by (asm_simp_tac (simpset() addsimps [add_mult_distrib]) 1);
paulson@8776
    21
qed "left_add_mult_distrib";
paulson@8776
    22
paulson@8776
    23
paulson@8759
    24
(** For cancel_numerals **)
paulson@8759
    25
paulson@8759
    26
Goal "j <= (i::nat) ==> ((i*u + m) - (j*u + n)) = (((i-j)*u + m) - n)";
paulson@8865
    27
by (asm_simp_tac (simpset() addsplits [nat_diff_split] 
paulson@8759
    28
		            addsimps [add_mult_distrib]) 1);
paulson@8766
    29
qed "nat_diff_add_eq1";
paulson@8759
    30
paulson@8759
    31
Goal "i <= (j::nat) ==> ((i*u + m) - (j*u + n)) = (m - ((j-i)*u + n))";
paulson@8865
    32
by (asm_simp_tac (simpset() addsplits [nat_diff_split] 
paulson@8759
    33
		            addsimps [add_mult_distrib]) 1);
paulson@8766
    34
qed "nat_diff_add_eq2";
paulson@8759
    35
paulson@8759
    36
Goal "j <= (i::nat) ==> (i*u + m = j*u + n) = ((i-j)*u + m = n)";
paulson@8865
    37
by (auto_tac (claset(), simpset() addsplits [nat_diff_split] 
paulson@8759
    38
                                  addsimps [add_mult_distrib]));
paulson@8766
    39
qed "nat_eq_add_iff1";
paulson@8759
    40
paulson@8759
    41
Goal "i <= (j::nat) ==> (i*u + m = j*u + n) = (m = (j-i)*u + n)";
paulson@8865
    42
by (auto_tac (claset(), simpset() addsplits [nat_diff_split] 
paulson@8759
    43
                                  addsimps [add_mult_distrib]));
paulson@8766
    44
qed "nat_eq_add_iff2";
paulson@8759
    45
paulson@8759
    46
Goal "j <= (i::nat) ==> (i*u + m < j*u + n) = ((i-j)*u + m < n)";
paulson@8865
    47
by (auto_tac (claset(), simpset() addsplits [nat_diff_split] 
paulson@8759
    48
                                  addsimps [add_mult_distrib]));
paulson@8766
    49
qed "nat_less_add_iff1";
paulson@8759
    50
paulson@8759
    51
Goal "i <= (j::nat) ==> (i*u + m < j*u + n) = (m < (j-i)*u + n)";
paulson@8865
    52
by (auto_tac (claset(), simpset() addsplits [nat_diff_split] 
paulson@8759
    53
                                  addsimps [add_mult_distrib]));
paulson@8766
    54
qed "nat_less_add_iff2";
paulson@8759
    55
paulson@8759
    56
Goal "j <= (i::nat) ==> (i*u + m <= j*u + n) = ((i-j)*u + m <= n)";
paulson@8865
    57
by (auto_tac (claset(), simpset() addsplits [nat_diff_split] 
paulson@8759
    58
                                  addsimps [add_mult_distrib]));
paulson@8766
    59
qed "nat_le_add_iff1";
paulson@8759
    60
paulson@8759
    61
Goal "i <= (j::nat) ==> (i*u + m <= j*u + n) = (m <= (j-i)*u + n)";
paulson@8865
    62
by (auto_tac (claset(), simpset() addsplits [nat_diff_split] 
paulson@8759
    63
                                  addsimps [add_mult_distrib]));
paulson@8766
    64
qed "nat_le_add_iff2";
paulson@8759
    65
paulson@8776
    66
paulson@8759
    67
structure Nat_Numeral_Simprocs =
paulson@8759
    68
struct
paulson@8759
    69
paulson@8766
    70
(*Utilities*)
paulson@8759
    71
paulson@8766
    72
fun mk_numeral n = HOLogic.number_of_const HOLogic.natT $ 
paulson@8766
    73
                   NumeralSyntax.mk_bin n;
paulson@8759
    74
paulson@8759
    75
(*Decodes a unary or binary numeral to a NATURAL NUMBER*)
paulson@8759
    76
fun dest_numeral (Const ("0", _)) = 0
paulson@8759
    77
  | dest_numeral (Const ("Suc", _) $ t) = 1 + dest_numeral t
paulson@8759
    78
  | dest_numeral (Const("Numeral.number_of", _) $ w) = 
paulson@8785
    79
      (BasisLibrary.Int.max (0, NumeralSyntax.dest_bin w)
paulson@8785
    80
       handle Match => raise TERM("Nat_Numeral_Simprocs.dest_numeral:1", [w]))
paulson@8785
    81
  | dest_numeral t = raise TERM("Nat_Numeral_Simprocs.dest_numeral:2", [t]);
paulson@8759
    82
paulson@8759
    83
fun find_first_numeral past (t::terms) =
paulson@8759
    84
	((dest_numeral t, t, rev past @ terms)
paulson@8759
    85
	 handle TERM _ => find_first_numeral (t::past) terms)
paulson@8759
    86
  | find_first_numeral past [] = raise TERM("find_first_numeral", []);
paulson@8759
    87
paulson@8759
    88
val zero = mk_numeral 0;
paulson@8759
    89
val mk_plus = HOLogic.mk_binop "op +";
paulson@8759
    90
paulson@8766
    91
(*Thus mk_sum[t] yields t+#0; longer sums don't have a trailing zero*)
paulson@8759
    92
fun mk_sum []        = zero
paulson@8766
    93
  | mk_sum [t,u]     = mk_plus (t, u)
paulson@8759
    94
  | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
paulson@8759
    95
paulson@8776
    96
(*this version ALWAYS includes a trailing zero*)
paulson@8776
    97
fun long_mk_sum []        = zero
paulson@8776
    98
  | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
paulson@8776
    99
paulson@8759
   100
val dest_plus = HOLogic.dest_bin "op +" HOLogic.natT;
paulson@8759
   101
paulson@8759
   102
(*extract the outer Sucs from a term and convert them to a binary numeral*)
paulson@8759
   103
fun dest_Sucs (k, Const ("Suc", _) $ t) = dest_Sucs (k+1, t)
paulson@8759
   104
  | dest_Sucs (0, t) = t
paulson@8759
   105
  | dest_Sucs (k, t) = mk_plus (mk_numeral k, t);
paulson@8759
   106
paulson@8759
   107
fun dest_sum t =
paulson@8759
   108
      let val (t,u) = dest_plus t 
paulson@8759
   109
      in  dest_sum t @ dest_sum u  end
paulson@8759
   110
      handle TERM _ => [t];
paulson@8759
   111
paulson@8759
   112
fun dest_Sucs_sum t = dest_sum (dest_Sucs (0,t));
paulson@8759
   113
paulson@8799
   114
val trans_tac = Int_Numeral_Simprocs.trans_tac;
paulson@8759
   115
paulson@8776
   116
val prove_conv = Int_Numeral_Simprocs.prove_conv;
paulson@8759
   117
paulson@8766
   118
val bin_simps = [add_nat_number_of, nat_number_of_add_left,
paulson@8766
   119
		 diff_nat_number_of, le_nat_number_of_eq_not_less, 
paulson@8766
   120
		 less_nat_number_of, Let_number_of, nat_number_of] @ 
paulson@8766
   121
                bin_arith_simps @ bin_rel_simps;
paulson@8759
   122
paulson@8759
   123
fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;
paulson@8759
   124
fun prep_pat s = Thm.read_cterm (Theory.sign_of Arith.thy) (s, HOLogic.termT);
paulson@8759
   125
val prep_pats = map prep_pat;
paulson@8759
   126
paulson@8759
   127
paulson@8776
   128
(*** CancelNumerals simprocs ***)
paulson@8759
   129
paulson@8759
   130
val one = mk_numeral 1;
paulson@8759
   131
val mk_times = HOLogic.mk_binop "op *";
paulson@8759
   132
paulson@8759
   133
fun mk_prod [] = one
paulson@8759
   134
  | mk_prod [t] = t
paulson@8759
   135
  | mk_prod (t :: ts) = if t = one then mk_prod ts
paulson@8759
   136
                        else mk_times (t, mk_prod ts);
paulson@8759
   137
paulson@8759
   138
val dest_times = HOLogic.dest_bin "op *" HOLogic.natT;
paulson@8759
   139
paulson@8759
   140
fun dest_prod t =
paulson@8759
   141
      let val (t,u) = dest_times t 
paulson@8759
   142
      in  dest_prod t @ dest_prod u  end
paulson@8759
   143
      handle TERM _ => [t];
paulson@8759
   144
paulson@8759
   145
(*DON'T do the obvious simplifications; that would create special cases*) 
paulson@8759
   146
fun mk_coeff (k, ts) = mk_times (mk_numeral k, ts);
paulson@8759
   147
paulson@8759
   148
(*Express t as a product of (possibly) a numeral with other sorted terms*)
paulson@8759
   149
fun dest_coeff t =
paulson@8759
   150
    let val ts = sort Term.term_ord (dest_prod t)
paulson@8759
   151
	val (n, _, ts') = find_first_numeral [] ts
paulson@8759
   152
                          handle TERM _ => (1, one, ts)
paulson@8759
   153
    in (n, mk_prod ts') end;
paulson@8759
   154
paulson@8759
   155
(*Find first coefficient-term THAT MATCHES u*)
paulson@8759
   156
fun find_first_coeff past u [] = raise TERM("find_first_coeff", []) 
paulson@8759
   157
  | find_first_coeff past u (t::terms) =
paulson@8759
   158
	let val (n,u') = dest_coeff t
paulson@8759
   159
	in  if u aconv u' then (n, rev past @ terms)
paulson@8759
   160
			  else find_first_coeff (t::past) u terms
paulson@8759
   161
	end
paulson@8759
   162
	handle TERM _ => find_first_coeff (t::past) u terms;
paulson@8759
   163
paulson@8759
   164
paulson@8759
   165
(*Simplify #1*n and n*#1 to n*)
paulson@8759
   166
val add_0s = map (rename_numerals NatBin.thy) [add_0, add_0_right];
paulson@8759
   167
val mult_1s = map (rename_numerals NatBin.thy) [mult_1, mult_1_right];
paulson@8759
   168
paulson@8865
   169
(*Final simplification: cancel + and *; replace #0 by 0 and #1 by 1*)
paulson@8865
   170
val simplify_meta_eq = 
paulson@8865
   171
    Int_Numeral_Simprocs.simplify_meta_eq
paulson@8865
   172
         [numeral_0_eq_0, numeral_1_eq_1, add_0, add_0_right,
paulson@8865
   173
	 mult_0, mult_0_right, mult_1, mult_1_right];
paulson@8865
   174
paulson@8759
   175
structure CancelNumeralsCommon =
paulson@8759
   176
  struct
paulson@8759
   177
  val mk_sum    	= mk_sum
paulson@8759
   178
  val dest_sum		= dest_Sucs_sum
paulson@8759
   179
  val mk_coeff		= mk_coeff
paulson@8759
   180
  val dest_coeff	= dest_coeff
paulson@8759
   181
  val find_first_coeff	= find_first_coeff []
paulson@8799
   182
  val trans_tac          = trans_tac
paulson@8759
   183
  val norm_tac = ALLGOALS
paulson@8785
   184
                   (simp_tac (HOL_ss addsimps add_0s@mult_1s@
paulson@8776
   185
                                       [add_0, Suc_eq_add_numeral_1]@add_ac))
paulson@8785
   186
                 THEN ALLGOALS (simp_tac
paulson@8785
   187
				(HOL_ss addsimps bin_simps@add_ac@mult_ac))
paulson@8766
   188
  val numeral_simp_tac	= ALLGOALS
paulson@8766
   189
                (simp_tac (HOL_ss addsimps [numeral_0_eq_0 RS sym]@add_0s@bin_simps))
paulson@8865
   190
  val simplify_meta_eq  = simplify_meta_eq
paulson@8759
   191
  end;
paulson@8759
   192
paulson@8759
   193
paulson@8759
   194
structure EqCancelNumerals = CancelNumeralsFun
paulson@8759
   195
 (open CancelNumeralsCommon
paulson@8776
   196
  val prove_conv = prove_conv "nateq_cancel_numerals"
paulson@8759
   197
  val mk_bal   = HOLogic.mk_eq
paulson@8759
   198
  val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
paulson@8776
   199
  val bal_add1 = nat_eq_add_iff1 RS trans
paulson@8776
   200
  val bal_add2 = nat_eq_add_iff2 RS trans
paulson@8759
   201
);
paulson@8759
   202
paulson@8759
   203
structure LessCancelNumerals = CancelNumeralsFun
paulson@8759
   204
 (open CancelNumeralsCommon
paulson@8776
   205
  val prove_conv = prove_conv "natless_cancel_numerals"
paulson@8759
   206
  val mk_bal   = HOLogic.mk_binrel "op <"
paulson@8759
   207
  val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT
paulson@8776
   208
  val bal_add1 = nat_less_add_iff1 RS trans
paulson@8776
   209
  val bal_add2 = nat_less_add_iff2 RS trans
paulson@8759
   210
);
paulson@8759
   211
paulson@8759
   212
structure LeCancelNumerals = CancelNumeralsFun
paulson@8759
   213
 (open CancelNumeralsCommon
paulson@8776
   214
  val prove_conv = prove_conv "natle_cancel_numerals"
paulson@8759
   215
  val mk_bal   = HOLogic.mk_binrel "op <="
paulson@8759
   216
  val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT
paulson@8776
   217
  val bal_add1 = nat_le_add_iff1 RS trans
paulson@8776
   218
  val bal_add2 = nat_le_add_iff2 RS trans
paulson@8759
   219
);
paulson@8759
   220
paulson@8759
   221
structure DiffCancelNumerals = CancelNumeralsFun
paulson@8759
   222
 (open CancelNumeralsCommon
paulson@8776
   223
  val prove_conv = prove_conv "natdiff_cancel_numerals"
paulson@8759
   224
  val mk_bal   = HOLogic.mk_binop "op -"
paulson@8759
   225
  val dest_bal = HOLogic.dest_bin "op -" HOLogic.natT
paulson@8776
   226
  val bal_add1 = nat_diff_add_eq1 RS trans
paulson@8776
   227
  val bal_add2 = nat_diff_add_eq2 RS trans
paulson@8759
   228
);
paulson@8759
   229
paulson@8759
   230
paulson@8759
   231
val cancel_numerals = 
paulson@8759
   232
  map prep_simproc
paulson@8759
   233
   [("nateq_cancel_numerals",
paulson@8759
   234
     prep_pats ["(l::nat) + m = n", "(l::nat) = m + n", 
paulson@8759
   235
		"(l::nat) * m = n", "(l::nat) = m * n", 
paulson@8759
   236
		"Suc m = n", "m = Suc n"], 
paulson@8759
   237
     EqCancelNumerals.proc),
paulson@8759
   238
    ("natless_cancel_numerals", 
paulson@8759
   239
     prep_pats ["(l::nat) + m < n", "(l::nat) < m + n", 
paulson@8759
   240
		"(l::nat) * m < n", "(l::nat) < m * n", 
paulson@8759
   241
		"Suc m < n", "m < Suc n"], 
paulson@8759
   242
     LessCancelNumerals.proc),
paulson@8759
   243
    ("natle_cancel_numerals", 
paulson@8759
   244
     prep_pats ["(l::nat) + m <= n", "(l::nat) <= m + n", 
paulson@8759
   245
		"(l::nat) * m <= n", "(l::nat) <= m * n", 
paulson@8759
   246
		"Suc m <= n", "m <= Suc n"], 
paulson@8759
   247
     LeCancelNumerals.proc),
paulson@8759
   248
    ("natdiff_cancel_numerals", 
paulson@8759
   249
     prep_pats ["((l::nat) + m) - n", "(l::nat) - (m + n)", 
paulson@8759
   250
		"(l::nat) * m - n", "(l::nat) - m * n", 
paulson@8759
   251
		"Suc m - n", "m - Suc n"], 
paulson@8759
   252
     DiffCancelNumerals.proc)];
paulson@8759
   253
paulson@8759
   254
paulson@8776
   255
structure CombineNumeralsData =
paulson@8776
   256
  struct
paulson@8776
   257
  val mk_sum    	= long_mk_sum    (*to work for e.g. #2*x + #3*x *)
paulson@8776
   258
  val dest_sum		= dest_Sucs_sum
paulson@8776
   259
  val mk_coeff		= mk_coeff
paulson@8776
   260
  val dest_coeff	= dest_coeff
paulson@8776
   261
  val left_distrib	= left_add_mult_distrib RS trans
paulson@8776
   262
  val prove_conv	= prove_conv "nat_combine_numerals"
paulson@8799
   263
  val trans_tac          = trans_tac
paulson@8776
   264
  val norm_tac = ALLGOALS
paulson@8785
   265
                   (simp_tac (HOL_ss addsimps add_0s@mult_1s@
paulson@8776
   266
                                       [add_0, Suc_eq_add_numeral_1]@add_ac))
paulson@8785
   267
                 THEN ALLGOALS (simp_tac
paulson@8785
   268
				(HOL_ss addsimps bin_simps@add_ac@mult_ac))
paulson@8776
   269
  val numeral_simp_tac	= ALLGOALS
paulson@8776
   270
                (simp_tac (HOL_ss addsimps [numeral_0_eq_0 RS sym]@add_0s@bin_simps))
paulson@8865
   271
  val simplify_meta_eq  = simplify_meta_eq
paulson@8776
   272
  end;
paulson@8776
   273
paulson@8776
   274
structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
paulson@8776
   275
  
paulson@8776
   276
val combine_numerals = 
paulson@8776
   277
    prep_simproc ("nat_combine_numerals",
paulson@8787
   278
		  prep_pats ["(i::nat) + j", "Suc (i + j)"],
paulson@8776
   279
		  CombineNumerals.proc);
paulson@8776
   280
paulson@8759
   281
end;
paulson@8759
   282
paulson@8759
   283
paulson@8759
   284
Addsimprocs Nat_Numeral_Simprocs.cancel_numerals;
paulson@8776
   285
Addsimprocs [Nat_Numeral_Simprocs.combine_numerals];
paulson@8759
   286
paulson@8850
   287
paulson@8759
   288
(*examples:
paulson@8759
   289
print_depth 22;
wenzelm@9000
   290
set timing;
paulson@8759
   291
set trace_simp;
paulson@8759
   292
fun test s = (Goal s; by (Simp_tac 1)); 
paulson@8759
   293
paulson@8759
   294
(*cancel_numerals*)
paulson@8787
   295
test "l +( #2) + (#2) + #2 + (l + #2) + (oo  + #2) = (uu::nat)";
paulson@8759
   296
test "(#2*length xs < #2*length xs + j)";
paulson@8759
   297
test "(#2*length xs < length xs * #2 + j)";
paulson@8759
   298
test "#2*u = (u::nat)";
paulson@8759
   299
test "#2*u = Suc (u)";
paulson@8759
   300
test "(i + j + #12 + (k::nat)) - #15 = y";
paulson@8759
   301
test "(i + j + #12 + (k::nat)) - #5 = y";
paulson@8759
   302
test "Suc u - #2 = y";
paulson@8759
   303
test "Suc (Suc (Suc u)) - #2 = y";
paulson@8759
   304
test "(i + j + #2 + (k::nat)) - 1 = y";
paulson@8759
   305
test "(i + j + #1 + (k::nat)) - 2 = y";
paulson@8759
   306
paulson@8759
   307
test "(#2*x + (u*v) + y) - v*#3*u = (w::nat)";
paulson@8865
   308
test "(#2*x*u*v + #5 + (u*v)*#4 + y) - v*u*#4 = (w::nat)";
paulson@8759
   309
test "(#2*x*u*v + (u*v)*#4 + y) - v*u = (w::nat)";
paulson@8759
   310
test "Suc (Suc (#2*x*u*v + u*#4 + y)) - u = w";
paulson@8759
   311
test "Suc ((u*v)*#4) - v*#3*u = w";
paulson@8759
   312
test "Suc (Suc ((u*v)*#3)) - v*#3*u = w";
paulson@8759
   313
paulson@8759
   314
test "(i + j + #12 + (k::nat)) = u + #15 + y";
paulson@8759
   315
test "(i + j + #32 + (k::nat)) - (u + #15 + y) = zz";
paulson@8759
   316
test "(i + j + #12 + (k::nat)) = u + #5 + y";
paulson@8759
   317
(*Suc*)
paulson@8759
   318
test "(i + j + #12 + k) = Suc (u + y)";
paulson@8759
   319
test "Suc (Suc (Suc (Suc (Suc (u + y))))) <= ((i + j) + #41 + k)";
paulson@8759
   320
test "(i + j + #5 + k) < Suc (Suc (Suc (Suc (Suc (u + y)))))";
paulson@8759
   321
test "Suc (Suc (Suc (Suc (Suc (u + y))))) - #5 = v";
paulson@8759
   322
test "(i + j + #5 + k) = Suc (Suc (Suc (Suc (Suc (Suc (Suc (u + y)))))))";
paulson@8759
   323
test "#2*y + #3*z + #2*u = Suc (u)";
paulson@8759
   324
test "#2*y + #3*z + #6*w + #2*y + #3*z + #2*u = Suc (u)";
paulson@8759
   325
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::nat)";
paulson@8759
   326
test "#6 + #2*y + #3*z + #4*u = Suc (vv + #2*u + z)";
paulson@8776
   327
test "(#2*n*m) < (#3*(m*n)) + (u::nat)";
paulson@8759
   328
paulson@8759
   329
(*negative numerals: FAIL*)
paulson@8759
   330
test "(i + j + #-23 + (k::nat)) < u + #15 + y";
paulson@8759
   331
test "(i + j + #3 + (k::nat)) < u + #-15 + y";
paulson@8759
   332
test "(i + j + #-12 + (k::nat)) - #15 = y";
paulson@8759
   333
test "(i + j + #12 + (k::nat)) - #-15 = y";
paulson@8759
   334
test "(i + j + #-12 + (k::nat)) - #-15 = y";
paulson@8759
   335
paulson@8776
   336
(*combine_numerals*)
paulson@8776
   337
test "k + #3*k = (u::nat)";
paulson@8776
   338
test "Suc (i + #3) = u";
paulson@8759
   339
test "Suc (i + j + #3 + k) = u";
paulson@8776
   340
test "k + j + #3*k + j = (u::nat)";
paulson@8776
   341
test "Suc (j*i + i + k + #5 + #3*k + i*j*#4) = (u::nat)";
paulson@8776
   342
test "(#2*n*m) + (#3*(m*n)) = (u::nat)";
paulson@8776
   343
(*negative numerals: FAIL*)
paulson@8759
   344
test "Suc (i + j + #-3 + k) = u";
paulson@8759
   345
*)
paulson@8759
   346
paulson@8759
   347
paulson@8759
   348
(*** Prepare linear arithmetic for nat numerals ***)
paulson@8759
   349
paulson@8759
   350
let
paulson@8759
   351
paulson@8759
   352
(* reduce contradictory <= to False *)
paulson@8759
   353
val add_rules =
paulson@8759
   354
  [add_nat_number_of, diff_nat_number_of, mult_nat_number_of,
paulson@8759
   355
   eq_nat_number_of, less_nat_number_of, le_nat_number_of_eq_not_less,
paulson@8759
   356
   le_Suc_number_of,le_number_of_Suc,
paulson@8759
   357
   less_Suc_number_of,less_number_of_Suc,
paulson@8759
   358
   Suc_eq_number_of,eq_number_of_Suc,
paulson@8759
   359
   eq_number_of_0, eq_0_number_of, less_0_number_of,
paulson@8759
   360
   nat_number_of, Let_number_of, if_True, if_False];
paulson@8759
   361
paulson@8776
   362
val simprocs = [Nat_Times_Assoc.conv,
paulson@8776
   363
		Nat_Numeral_Simprocs.combine_numerals]@ 
paulson@8776
   364
		Nat_Numeral_Simprocs.cancel_numerals;
paulson@8759
   365
paulson@8759
   366
in
paulson@8776
   367
LA_Data_Ref.ss_ref := !LA_Data_Ref.ss_ref addsimps add_rules 
paulson@8776
   368
                                          addsimps basic_renamed_arith_simps
paulson@8776
   369
                                          addsimprocs simprocs
paulson@8759
   370
end;
paulson@8759
   371
paulson@8759
   372
paulson@8759
   373
paulson@8759
   374
(** For simplifying  Suc m - #n **)
paulson@8759
   375
paulson@8759
   376
Goal "#0 < n ==> Suc m - n = m - (n - #1)";
paulson@8865
   377
by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
paulson@8759
   378
qed "Suc_diff_eq_diff_pred";
paulson@8759
   379
paulson@8759
   380
(*Now just instantiating n to (number_of v) does the right simplification,
paulson@8759
   381
  but with some redundant inequality tests.*)
paulson@8759
   382
paulson@8935
   383
Goal "neg (number_of (bin_pred v)) = (number_of v = (0::nat))";
paulson@8759
   384
by (subgoal_tac "neg (number_of (bin_pred v)) = (number_of v < 1)" 1);
paulson@8759
   385
by (Asm_simp_tac 1);
paulson@8759
   386
by (stac less_number_of_Suc 1);
paulson@8759
   387
by (Simp_tac 1);
paulson@8759
   388
qed "neg_number_of_bin_pred_iff_0";
paulson@8759
   389
paulson@8759
   390
Goal "neg (number_of (bin_minus v)) ==> \
paulson@8759
   391
\     Suc m - (number_of v) = m - (number_of (bin_pred v))";
paulson@8759
   392
by (stac Suc_diff_eq_diff_pred 1);
paulson@8759
   393
by (Simp_tac 1);
paulson@8759
   394
by (Simp_tac 1);
paulson@8759
   395
by (asm_full_simp_tac
paulson@8865
   396
    (simpset_of Int.thy addsimps [diff_nat_number_of, less_0_number_of RS sym, 
paulson@8759
   397
				  neg_number_of_bin_pred_iff_0]) 1);
paulson@8759
   398
qed "Suc_diff_number_of";
paulson@8759
   399
paulson@8759
   400
(* now redundant because of the inverse_fold simproc
paulson@8759
   401
    Addsimps [Suc_diff_number_of]; *)
paulson@8759
   402
paulson@8865
   403
Goal "nat_case a f (number_of v) = \
paulson@8865
   404
\       (let pv = number_of (bin_pred v) in \
paulson@8865
   405
\        if neg pv then a else f (nat pv))";
paulson@8865
   406
by (simp_tac
paulson@8865
   407
    (simpset() addsplits [nat.split]
paulson@8865
   408
			addsimps [Let_def, neg_number_of_bin_pred_iff_0]) 1);
paulson@8865
   409
qed "nat_case_number_of"; 
paulson@8865
   410
paulson@8865
   411
Goal "nat_case a f ((number_of v) + n) = \
paulson@8865
   412
\      (let pv = number_of (bin_pred v) in \
paulson@8865
   413
\        if neg pv then nat_case a f n else f (nat pv + n))";
paulson@8865
   414
by (stac add_eq_if 1);
paulson@8865
   415
by (asm_simp_tac
paulson@8865
   416
    (simpset() addsplits [nat.split]
paulson@8865
   417
               addsimps [Let_def, neg_imp_number_of_eq_0, 
paulson@8865
   418
			 neg_number_of_bin_pred_iff_0]) 1);
paulson@8865
   419
qed "nat_case_add_eq_if";
paulson@8865
   420
paulson@8865
   421
Addsimps [nat_case_number_of, nat_case_add_eq_if];
paulson@8865
   422
paulson@8865
   423
paulson@8865
   424
Goal "nat_rec a f (number_of v) = \
paulson@8865
   425
\       (let pv = number_of (bin_pred v) in \
paulson@8865
   426
\        if neg pv then a else f (nat pv) (nat_rec a f (nat pv)))";
paulson@8865
   427
by (case_tac "(number_of v)::nat" 1);
paulson@8865
   428
by (ALLGOALS (asm_simp_tac
paulson@8865
   429
	      (simpset() addsimps [Let_def, neg_number_of_bin_pred_iff_0])));
paulson@8865
   430
by (asm_full_simp_tac (simpset() addsplits [split_if_asm]) 1);
paulson@8865
   431
qed "nat_rec_number_of"; 
paulson@8865
   432
paulson@8865
   433
Goal "nat_rec a f (number_of v + n) = \
paulson@8865
   434
\       (let pv = number_of (bin_pred v) in \
paulson@8865
   435
\        if neg pv then nat_rec a f n \
paulson@8865
   436
\                  else f (nat pv + n) (nat_rec a f (nat pv + n)))";
paulson@8865
   437
by (stac add_eq_if 1);
paulson@8865
   438
by (asm_simp_tac
paulson@8865
   439
    (simpset() addsplits [nat.split]
paulson@8865
   440
               addsimps [Let_def, neg_imp_number_of_eq_0, 
paulson@8865
   441
			 neg_number_of_bin_pred_iff_0]) 1);
paulson@8865
   442
qed "nat_rec_add_eq_if"; 
paulson@8865
   443
paulson@8865
   444
Addsimps [nat_rec_number_of, nat_rec_add_eq_if];
paulson@8865
   445
paulson@8759
   446
paulson@8759
   447
(** For simplifying  #m - Suc n **)
paulson@8759
   448
paulson@8759
   449
Goal "m - Suc n = (m - #1) - n";
paulson@8865
   450
by (simp_tac (numeral_ss addsplits [nat_diff_split]) 1);
paulson@8759
   451
qed "diff_Suc_eq_diff_pred";
paulson@8759
   452
paulson@8877
   453
(*Obsolete because of natdiff_cancel_numerals
paulson@8877
   454
    Addsimps [inst "m" "number_of ?v" diff_Suc_eq_diff_pred];
paulson@8877
   455
  It LOOPS if #1 is being replaced by 1.
paulson@8877
   456
*)
paulson@8776
   457
paulson@8776
   458
paulson@8776
   459
(** Evens and Odds, for Mutilated Chess Board **)
paulson@8776
   460
paulson@8776
   461
(*Case analysis on b<#2*)
paulson@8776
   462
Goal "(n::nat) < #2 ==> n = #0 | n = #1";
paulson@8776
   463
by (arith_tac 1);
paulson@8776
   464
qed "less_2_cases";
paulson@8776
   465
paulson@8776
   466
Goal "Suc(Suc(m)) mod #2 = m mod #2";
paulson@8776
   467
by (subgoal_tac "m mod #2 < #2" 1);
paulson@8776
   468
by (Asm_simp_tac 2);
paulson@8776
   469
be (less_2_cases RS disjE) 1;
paulson@8776
   470
by (ALLGOALS (asm_simp_tac (simpset() addsimps [mod_Suc])));
paulson@8776
   471
qed "mod2_Suc_Suc";
paulson@8776
   472
Addsimps [mod2_Suc_Suc];
paulson@8776
   473
paulson@8935
   474
Goal "!!m::nat. (0 < m mod #2) = (m mod #2 = #1)";
paulson@8776
   475
by (subgoal_tac "m mod #2 < #2" 1);
paulson@8776
   476
by (Asm_simp_tac 2);
paulson@8776
   477
by (auto_tac (claset(), simpset() delsimps [mod_less_divisor]));
paulson@8776
   478
qed "mod2_gr_0";
paulson@8776
   479
Addsimps [mod2_gr_0, rename_numerals thy mod2_gr_0];
paulson@8776
   480
paulson@8877
   481
(** Removal of small numerals: #0, #1 and (in additive positions) #2 **)
paulson@8877
   482
paulson@8877
   483
Goal "#2 + n = Suc (Suc n)";
paulson@8877
   484
by (Simp_tac 1);
paulson@8877
   485
qed "add_2_eq_Suc";
paulson@8877
   486
paulson@8877
   487
Goal "n + #2 = Suc (Suc n)";
paulson@8877
   488
by (Simp_tac 1);
paulson@8877
   489
qed "add_2_eq_Suc'";
paulson@8877
   490
paulson@8877
   491
Addsimps [numeral_0_eq_0, numeral_1_eq_1, add_2_eq_Suc, add_2_eq_Suc'];
paulson@8877
   492
paulson@8877
   493
(*Can be used to eliminate long strings of Sucs, but not by default*)
paulson@8877
   494
Goal "Suc (Suc (Suc n)) = #3 + n";
paulson@8877
   495
by (Simp_tac 1);
paulson@8877
   496
qed "Suc3_eq_add_3";