src/HOL/Integ/NatSimprocs.ML
author paulson
Fri Apr 21 11:29:57 2000 +0200 (2000-04-21)
changeset 8759 49154c960140
child 8766 1ef6e77e12ee
permissions -rw-r--r--
new file containing simproc invocations, from NatBin.ML
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@8759
    14
qed "add_nat_number_of_add";
paulson@8759
    15
paulson@8759
    16
paulson@8759
    17
(** For cancel_numerals **)
paulson@8759
    18
paulson@8759
    19
Goal "j <= (i::nat) ==> ((i*u + m) - (j*u + n)) = (((i-j)*u + m) - n)";
paulson@8759
    20
by (asm_simp_tac (simpset() addsplits [nat_diff_split'] 
paulson@8759
    21
		            addsimps [add_mult_distrib]) 1);
paulson@8759
    22
qed "diff_add_eq1";
paulson@8759
    23
paulson@8759
    24
Goal "i <= (j::nat) ==> ((i*u + m) - (j*u + n)) = (m - ((j-i)*u + n))";
paulson@8759
    25
by (asm_simp_tac (simpset() addsplits [nat_diff_split'] 
paulson@8759
    26
		            addsimps [add_mult_distrib]) 1);
paulson@8759
    27
qed "diff_add_eq2";
paulson@8759
    28
paulson@8759
    29
Goal "j <= (i::nat) ==> (i*u + m = j*u + n) = ((i-j)*u + m = n)";
paulson@8759
    30
by (auto_tac (claset(), simpset() addsplits [nat_diff_split'] 
paulson@8759
    31
                                  addsimps [add_mult_distrib]));
paulson@8759
    32
qed "eq_add_iff1";
paulson@8759
    33
paulson@8759
    34
Goal "i <= (j::nat) ==> (i*u + m = j*u + n) = (m = (j-i)*u + n)";
paulson@8759
    35
by (auto_tac (claset(), simpset() addsplits [nat_diff_split'] 
paulson@8759
    36
                                  addsimps [add_mult_distrib]));
paulson@8759
    37
qed "eq_add_iff2";
paulson@8759
    38
paulson@8759
    39
Goal "j <= (i::nat) ==> (i*u + m < j*u + n) = ((i-j)*u + m < n)";
paulson@8759
    40
by (auto_tac (claset(), simpset() addsplits [nat_diff_split'] 
paulson@8759
    41
                                  addsimps [add_mult_distrib]));
paulson@8759
    42
qed "less_add_iff1";
paulson@8759
    43
paulson@8759
    44
Goal "i <= (j::nat) ==> (i*u + m < j*u + n) = (m < (j-i)*u + n)";
paulson@8759
    45
by (auto_tac (claset(), simpset() addsplits [nat_diff_split'] 
paulson@8759
    46
                                  addsimps [add_mult_distrib]));
paulson@8759
    47
qed "less_add_iff2";
paulson@8759
    48
paulson@8759
    49
Goal "j <= (i::nat) ==> (i*u + m <= j*u + n) = ((i-j)*u + m <= n)";
paulson@8759
    50
by (auto_tac (claset(), simpset() addsplits [nat_diff_split'] 
paulson@8759
    51
                                  addsimps [add_mult_distrib]));
paulson@8759
    52
qed "le_add_iff1";
paulson@8759
    53
paulson@8759
    54
Goal "i <= (j::nat) ==> (i*u + m <= j*u + n) = (m <= (j-i)*u + n)";
paulson@8759
    55
by (auto_tac (claset(), simpset() addsplits [nat_diff_split'] 
paulson@8759
    56
                                  addsimps [add_mult_distrib]));
paulson@8759
    57
qed "le_add_iff2";
paulson@8759
    58
paulson@8759
    59
structure Nat_Numeral_Simprocs =
paulson@8759
    60
struct
paulson@8759
    61
paulson@8759
    62
(*Utilities for simproc inverse_fold*)
paulson@8759
    63
paulson@8759
    64
fun mk_numeral n = HOLogic.number_of_const $ NumeralSyntax.mk_bin n;
paulson@8759
    65
paulson@8759
    66
(*Decodes a unary or binary numeral to a NATURAL NUMBER*)
paulson@8759
    67
fun dest_numeral (Const ("0", _)) = 0
paulson@8759
    68
  | dest_numeral (Const ("Suc", _) $ t) = 1 + dest_numeral t
paulson@8759
    69
  | dest_numeral (Const("Numeral.number_of", _) $ w) = 
paulson@8759
    70
        BasisLibrary.Int.max (0, NumeralSyntax.dest_bin w)
paulson@8759
    71
  | dest_numeral t = raise TERM("dest_numeral", [t]);
paulson@8759
    72
paulson@8759
    73
fun find_first_numeral past (t::terms) =
paulson@8759
    74
	((dest_numeral t, t, rev past @ terms)
paulson@8759
    75
	 handle TERM _ => find_first_numeral (t::past) terms)
paulson@8759
    76
  | find_first_numeral past [] = raise TERM("find_first_numeral", []);
paulson@8759
    77
paulson@8759
    78
val zero = mk_numeral 0;
paulson@8759
    79
val mk_plus = HOLogic.mk_binop "op +";
paulson@8759
    80
paulson@8759
    81
fun mk_sum []        = zero
paulson@8759
    82
  | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
paulson@8759
    83
paulson@8759
    84
val dest_plus = HOLogic.dest_bin "op +" HOLogic.natT;
paulson@8759
    85
paulson@8759
    86
(*extract the outer Sucs from a term and convert them to a binary numeral*)
paulson@8759
    87
fun dest_Sucs (k, Const ("Suc", _) $ t) = dest_Sucs (k+1, t)
paulson@8759
    88
  | dest_Sucs (0, t) = t
paulson@8759
    89
  | dest_Sucs (k, t) = mk_plus (mk_numeral k, t);
paulson@8759
    90
paulson@8759
    91
fun dest_sum t =
paulson@8759
    92
      let val (t,u) = dest_plus t 
paulson@8759
    93
      in  dest_sum t @ dest_sum u  end
paulson@8759
    94
      handle TERM _ => [t];
paulson@8759
    95
paulson@8759
    96
fun dest_Sucs_sum t = dest_sum (dest_Sucs (0,t));
paulson@8759
    97
paulson@8759
    98
val mk_diff = HOLogic.mk_binop "op -";
paulson@8759
    99
val dest_diff = HOLogic.dest_bin "op -" HOLogic.natT;
paulson@8759
   100
paulson@8759
   101
val mk_eqv = HOLogic.mk_Trueprop o HOLogic.mk_eq;
paulson@8759
   102
paulson@8759
   103
fun prove_conv tacs sg (t, u) =
paulson@8759
   104
  if t aconv u then None
paulson@8759
   105
  else
paulson@8759
   106
  Some
paulson@8759
   107
     (mk_meta_eq (prove_goalw_cterm [] (cterm_of sg (mk_eqv (t, u)))
paulson@8759
   108
	(K tacs))
paulson@8759
   109
      handle ERROR => error 
paulson@8759
   110
	  ("The error(s) above occurred while trying to prove " ^
paulson@8759
   111
	   (string_of_cterm (cterm_of sg (mk_eqv (t, u))))));
paulson@8759
   112
paulson@8759
   113
fun all_simp_tac ss rules = ALLGOALS (simp_tac (ss addsimps rules));
paulson@8759
   114
paulson@8759
   115
val add_norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_ac));
paulson@8759
   116
paulson@8759
   117
(****combine_coeffs will make this obsolete****)
paulson@8759
   118
structure FoldSucData =
paulson@8759
   119
  struct
paulson@8759
   120
  val mk_numeral	= mk_numeral
paulson@8759
   121
  val dest_numeral	= dest_numeral
paulson@8759
   122
  val find_first_numeral = find_first_numeral []
paulson@8759
   123
  val mk_sum		= mk_sum
paulson@8759
   124
  val dest_sum		= dest_Sucs_sum
paulson@8759
   125
  val mk_diff    	= HOLogic.mk_binop "op -"
paulson@8759
   126
  val dest_diff		= HOLogic.dest_bin "op -" HOLogic.natT
paulson@8759
   127
  val dest_Suc		= HOLogic.dest_Suc
paulson@8759
   128
  val double_diff_eq	= diff_add_assoc_diff
paulson@8759
   129
  val move_diff_eq	= diff_add_assoc2
paulson@8759
   130
  val prove_conv	= prove_conv
paulson@8759
   131
  val numeral_simp_tac	= all_simp_tac (simpset()
paulson@8759
   132
					  addsimps [Suc_nat_number_of_add])
paulson@8759
   133
  val add_norm_tac	= ALLGOALS (simp_tac (simpset() addsimps Suc_eq_add_numeral_1::add_ac))
paulson@8759
   134
  end;
paulson@8759
   135
paulson@8759
   136
structure FoldSuc = FoldSucFun (FoldSucData);
paulson@8759
   137
paulson@8759
   138
fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;
paulson@8759
   139
fun prep_pat s = Thm.read_cterm (Theory.sign_of Arith.thy) (s, HOLogic.termT);
paulson@8759
   140
val prep_pats = map prep_pat;
paulson@8759
   141
paulson@8759
   142
val fold_Suc = 
paulson@8759
   143
    prep_simproc ("fold_Suc", 
paulson@8759
   144
		  [prep_pat "Suc (i + j)"], 
paulson@8759
   145
		  FoldSuc.proc);
paulson@8759
   146
paulson@8759
   147
(*** Now for CancelNumerals ***)
paulson@8759
   148
paulson@8759
   149
val one = mk_numeral 1;
paulson@8759
   150
val mk_times = HOLogic.mk_binop "op *";
paulson@8759
   151
paulson@8759
   152
fun mk_prod [] = one
paulson@8759
   153
  | mk_prod [t] = t
paulson@8759
   154
  | mk_prod (t :: ts) = if t = one then mk_prod ts
paulson@8759
   155
                        else mk_times (t, mk_prod ts);
paulson@8759
   156
paulson@8759
   157
val dest_times = HOLogic.dest_bin "op *" HOLogic.natT;
paulson@8759
   158
paulson@8759
   159
fun dest_prod t =
paulson@8759
   160
      let val (t,u) = dest_times t 
paulson@8759
   161
      in  dest_prod t @ dest_prod u  end
paulson@8759
   162
      handle TERM _ => [t];
paulson@8759
   163
paulson@8759
   164
(*DON'T do the obvious simplifications; that would create special cases*) 
paulson@8759
   165
fun mk_coeff (k, ts) = mk_times (mk_numeral k, ts);
paulson@8759
   166
paulson@8759
   167
(*Express t as a product of (possibly) a numeral with other sorted terms*)
paulson@8759
   168
fun dest_coeff t =
paulson@8759
   169
    let val ts = sort Term.term_ord (dest_prod t)
paulson@8759
   170
	val (n, _, ts') = find_first_numeral [] ts
paulson@8759
   171
                          handle TERM _ => (1, one, ts)
paulson@8759
   172
    in (n, mk_prod ts') end;
paulson@8759
   173
paulson@8759
   174
(*Find first coefficient-term THAT MATCHES u*)
paulson@8759
   175
fun find_first_coeff past u [] = raise TERM("find_first_coeff", []) 
paulson@8759
   176
  | find_first_coeff past u (t::terms) =
paulson@8759
   177
	let val (n,u') = dest_coeff t
paulson@8759
   178
	in  if u aconv u' then (n, rev past @ terms)
paulson@8759
   179
			  else find_first_coeff (t::past) u terms
paulson@8759
   180
	end
paulson@8759
   181
	handle TERM _ => find_first_coeff (t::past) u terms;
paulson@8759
   182
paulson@8759
   183
paulson@8759
   184
(*Simplify #1*n and n*#1 to n*)
paulson@8759
   185
val add_0s = map (rename_numerals NatBin.thy) [add_0, add_0_right];
paulson@8759
   186
val mult_1s = map (rename_numerals NatBin.thy) [mult_1, mult_1_right];
paulson@8759
   187
paulson@8759
   188
val bin_simps = [add_nat_number_of, add_nat_number_of_add] @ 
paulson@8759
   189
                bin_arith_simps @ bin_rel_simps;
paulson@8759
   190
paulson@8759
   191
structure CancelNumeralsCommon =
paulson@8759
   192
  struct
paulson@8759
   193
  val mk_sum    	= mk_sum
paulson@8759
   194
  val dest_sum		= dest_Sucs_sum
paulson@8759
   195
  val mk_coeff		= mk_coeff
paulson@8759
   196
  val dest_coeff	= dest_coeff
paulson@8759
   197
  val find_first_coeff	= find_first_coeff []
paulson@8759
   198
  val prove_conv	= prove_conv
paulson@8759
   199
  val numeral_simp_tac	= ALLGOALS (simp_tac (simpset() addsimps [numeral_0_eq_0 RS sym]))
paulson@8759
   200
  val norm_tac = ALLGOALS
paulson@8759
   201
                   (simp_tac (HOL_ss addsimps add_0s@mult_1s@bin_simps@
paulson@8759
   202
                                              [Suc_eq_add_numeral_1]@add_ac))
paulson@8759
   203
                 THEN ALLGOALS (simp_tac (HOL_ss addsimps mult_ac))
paulson@8759
   204
  end;
paulson@8759
   205
paulson@8759
   206
paulson@8759
   207
(* nat eq *)
paulson@8759
   208
structure EqCancelNumerals = CancelNumeralsFun
paulson@8759
   209
 (open CancelNumeralsCommon
paulson@8759
   210
  val mk_bal   = HOLogic.mk_eq
paulson@8759
   211
  val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
paulson@8759
   212
  val bal_add1	= eq_add_iff1 RS trans
paulson@8759
   213
  val bal_add2	= eq_add_iff2 RS trans
paulson@8759
   214
);
paulson@8759
   215
paulson@8759
   216
(* nat less *)
paulson@8759
   217
structure LessCancelNumerals = CancelNumeralsFun
paulson@8759
   218
 (open CancelNumeralsCommon
paulson@8759
   219
  val mk_bal   = HOLogic.mk_binrel "op <"
paulson@8759
   220
  val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT
paulson@8759
   221
  val bal_add1	= less_add_iff1 RS trans
paulson@8759
   222
  val bal_add2	= less_add_iff2 RS trans
paulson@8759
   223
);
paulson@8759
   224
paulson@8759
   225
(* nat le *)
paulson@8759
   226
structure LeCancelNumerals = CancelNumeralsFun
paulson@8759
   227
 (open CancelNumeralsCommon
paulson@8759
   228
  val mk_bal   = HOLogic.mk_binrel "op <="
paulson@8759
   229
  val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT
paulson@8759
   230
  val bal_add1	= le_add_iff1 RS trans
paulson@8759
   231
  val bal_add2	= le_add_iff2 RS trans
paulson@8759
   232
);
paulson@8759
   233
paulson@8759
   234
(* nat diff *)
paulson@8759
   235
structure DiffCancelNumerals = CancelNumeralsFun
paulson@8759
   236
 (open CancelNumeralsCommon
paulson@8759
   237
  val mk_bal   = HOLogic.mk_binop "op -"
paulson@8759
   238
  val dest_bal = HOLogic.dest_bin "op -" HOLogic.natT
paulson@8759
   239
  val bal_add1	= diff_add_eq1 RS trans
paulson@8759
   240
  val bal_add2	= diff_add_eq2 RS trans
paulson@8759
   241
);
paulson@8759
   242
paulson@8759
   243
paulson@8759
   244
val cancel_numerals = 
paulson@8759
   245
  map prep_simproc
paulson@8759
   246
   [("nateq_cancel_numerals",
paulson@8759
   247
     prep_pats ["(l::nat) + m = n", "(l::nat) = m + n", 
paulson@8759
   248
		"(l::nat) * m = n", "(l::nat) = m * n", 
paulson@8759
   249
		"Suc m = n", "m = Suc n"], 
paulson@8759
   250
     EqCancelNumerals.proc),
paulson@8759
   251
    ("natless_cancel_numerals", 
paulson@8759
   252
     prep_pats ["(l::nat) + m < n", "(l::nat) < m + n", 
paulson@8759
   253
		"(l::nat) * m < n", "(l::nat) < m * n", 
paulson@8759
   254
		"Suc m < n", "m < Suc n"], 
paulson@8759
   255
     LessCancelNumerals.proc),
paulson@8759
   256
    ("natle_cancel_numerals", 
paulson@8759
   257
     prep_pats ["(l::nat) + m <= n", "(l::nat) <= m + n", 
paulson@8759
   258
		"(l::nat) * m <= n", "(l::nat) <= m * n", 
paulson@8759
   259
		"Suc m <= n", "m <= Suc n"], 
paulson@8759
   260
     LeCancelNumerals.proc),
paulson@8759
   261
    ("natdiff_cancel_numerals", 
paulson@8759
   262
     prep_pats ["((l::nat) + m) - n", "(l::nat) - (m + n)", 
paulson@8759
   263
		"(l::nat) * m - n", "(l::nat) - m * n", 
paulson@8759
   264
		"Suc m - n", "m - Suc n"], 
paulson@8759
   265
     DiffCancelNumerals.proc)];
paulson@8759
   266
paulson@8759
   267
paulson@8759
   268
end;
paulson@8759
   269
paulson@8759
   270
paulson@8759
   271
Addsimprocs [Nat_Numeral_Simprocs.fold_Suc];
paulson@8759
   272
Addsimprocs Nat_Numeral_Simprocs.cancel_numerals;
paulson@8759
   273
paulson@8759
   274
(*examples:
paulson@8759
   275
print_depth 22;
paulson@8759
   276
set proof_timing;
paulson@8759
   277
set trace_simp;
paulson@8759
   278
fun test s = (Goal s; by (Simp_tac 1)); 
paulson@8759
   279
paulson@8759
   280
(*cancel_numerals*)
paulson@8759
   281
test "(#2*length xs < #2*length xs + j)";
paulson@8759
   282
test "(#2*length xs < length xs * #2 + j)";
paulson@8759
   283
test "#2*u = (u::nat)";
paulson@8759
   284
test "#2*u = Suc (u)";
paulson@8759
   285
test "(i + j + #12 + (k::nat)) - #15 = y";
paulson@8759
   286
test "(i + j + #12 + (k::nat)) - #5 = y";
paulson@8759
   287
test "Suc u - #2 = y";
paulson@8759
   288
test "Suc (Suc (Suc u)) - #2 = y";
paulson@8759
   289
(*Unary*)
paulson@8759
   290
test "(i + j + #2 + (k::nat)) - 1 = y";
paulson@8759
   291
test "(i + j + #1 + (k::nat)) - 2 = y";
paulson@8759
   292
paulson@8759
   293
test "(#2*x + (u*v) + y) - v*#3*u = (w::nat)";
paulson@8759
   294
test "(#2*x*u*v + (u*v)*#4 + y) - v*u*#4 = (w::nat)";
paulson@8759
   295
test "(#2*x*u*v + (u*v)*#4 + y) - v*u = (w::nat)";
paulson@8759
   296
test "Suc (Suc (#2*x*u*v + u*#4 + y)) - u = w";
paulson@8759
   297
test "Suc ((u*v)*#4) - v*#3*u = w";
paulson@8759
   298
test "Suc (Suc ((u*v)*#3)) - v*#3*u = w";
paulson@8759
   299
paulson@8759
   300
test "(i + j + #12 + (k::nat)) = u + #15 + y";
paulson@8759
   301
test "(i + j + #32 + (k::nat)) - (u + #15 + y) = zz";
paulson@8759
   302
test "(i + j + #12 + (k::nat)) = u + #5 + y";
paulson@8759
   303
(*Suc*)
paulson@8759
   304
test "(i + j + #12 + k) = Suc (u + y)";
paulson@8759
   305
test "Suc (Suc (Suc (Suc (Suc (u + y))))) <= ((i + j) + #41 + k)";
paulson@8759
   306
test "(i + j + #5 + k) < Suc (Suc (Suc (Suc (Suc (u + y)))))";
paulson@8759
   307
test "Suc (Suc (Suc (Suc (Suc (u + y))))) - #5 = v";
paulson@8759
   308
test "(i + j + #5 + k) = Suc (Suc (Suc (Suc (Suc (Suc (Suc (u + y)))))))";
paulson@8759
   309
test "#2*y + #3*z + #2*u = Suc (u)";
paulson@8759
   310
test "#2*y + #3*z + #6*w + #2*y + #3*z + #2*u = Suc (u)";
paulson@8759
   311
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
   312
test "#6 + #2*y + #3*z + #4*u = Suc (vv + #2*u + z)";
paulson@8759
   313
paulson@8759
   314
(*negative numerals: FAIL*)
paulson@8759
   315
test "(i + j + #-23 + (k::nat)) < u + #15 + y";
paulson@8759
   316
test "(i + j + #3 + (k::nat)) < u + #-15 + y";
paulson@8759
   317
test "(i + j + #-12 + (k::nat)) - #15 = y";
paulson@8759
   318
test "(i + j + #12 + (k::nat)) - #-15 = y";
paulson@8759
   319
test "(i + j + #-12 + (k::nat)) - #-15 = y";
paulson@8759
   320
paulson@8759
   321
(*fold_Suc*)
paulson@8759
   322
test "Suc (i + j + #3 + k) = u";
paulson@8759
   323
(*negative numerals*)
paulson@8759
   324
test "Suc (i + j + #-3 + k) = u";
paulson@8759
   325
*)
paulson@8759
   326
paulson@8759
   327
paulson@8759
   328
(*** Prepare linear arithmetic for nat numerals ***)
paulson@8759
   329
paulson@8759
   330
let
paulson@8759
   331
paulson@8759
   332
(* reduce contradictory <= to False *)
paulson@8759
   333
val add_rules =
paulson@8759
   334
  [add_nat_number_of, diff_nat_number_of, mult_nat_number_of,
paulson@8759
   335
   eq_nat_number_of, less_nat_number_of, le_nat_number_of_eq_not_less,
paulson@8759
   336
   le_Suc_number_of,le_number_of_Suc,
paulson@8759
   337
   less_Suc_number_of,less_number_of_Suc,
paulson@8759
   338
   Suc_eq_number_of,eq_number_of_Suc,
paulson@8759
   339
   eq_number_of_0, eq_0_number_of, less_0_number_of,
paulson@8759
   340
   nat_number_of, Let_number_of, if_True, if_False];
paulson@8759
   341
paulson@8759
   342
val simprocs = [Nat_Plus_Assoc.conv,Nat_Times_Assoc.conv];
paulson@8759
   343
paulson@8759
   344
in
paulson@8759
   345
LA_Data_Ref.ss_ref := !LA_Data_Ref.ss_ref addsimps add_rules
paulson@8759
   346
                      addsimprocs simprocs
paulson@8759
   347
end;
paulson@8759
   348
paulson@8759
   349
paulson@8759
   350
paulson@8759
   351
(** For simplifying  Suc m - #n **)
paulson@8759
   352
paulson@8759
   353
Goal "#0 < n ==> Suc m - n = m - (n - #1)";
paulson@8759
   354
by (asm_full_simp_tac (numeral_ss addsplits [nat_diff_split']) 1);
paulson@8759
   355
qed "Suc_diff_eq_diff_pred";
paulson@8759
   356
paulson@8759
   357
(*Now just instantiating n to (number_of v) does the right simplification,
paulson@8759
   358
  but with some redundant inequality tests.*)
paulson@8759
   359
paulson@8759
   360
Goal "neg (number_of (bin_pred v)) = (number_of v = 0)";
paulson@8759
   361
by (subgoal_tac "neg (number_of (bin_pred v)) = (number_of v < 1)" 1);
paulson@8759
   362
by (Asm_simp_tac 1);
paulson@8759
   363
by (stac less_number_of_Suc 1);
paulson@8759
   364
by (Simp_tac 1);
paulson@8759
   365
qed "neg_number_of_bin_pred_iff_0";
paulson@8759
   366
paulson@8759
   367
Goal "neg (number_of (bin_minus v)) ==> \
paulson@8759
   368
\     Suc m - (number_of v) = m - (number_of (bin_pred v))";
paulson@8759
   369
by (stac Suc_diff_eq_diff_pred 1);
paulson@8759
   370
by (Simp_tac 1);
paulson@8759
   371
by (Simp_tac 1);
paulson@8759
   372
by (asm_full_simp_tac
paulson@8759
   373
    (simpset_of Int.thy addsimps [less_0_number_of RS sym, 
paulson@8759
   374
				  neg_number_of_bin_pred_iff_0]) 1);
paulson@8759
   375
qed "Suc_diff_number_of";
paulson@8759
   376
paulson@8759
   377
(* now redundant because of the inverse_fold simproc
paulson@8759
   378
    Addsimps [Suc_diff_number_of]; *)
paulson@8759
   379
paulson@8759
   380
paulson@8759
   381
(** For simplifying  #m - Suc n **)
paulson@8759
   382
paulson@8759
   383
Goal "m - Suc n = (m - #1) - n";
paulson@8759
   384
by (simp_tac (numeral_ss addsplits [nat_diff_split']) 1);
paulson@8759
   385
qed "diff_Suc_eq_diff_pred";
paulson@8759
   386
paulson@8759
   387
Addsimps [inst "m" "number_of ?v" diff_Suc_eq_diff_pred];