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