src/HOL/nat_simprocs.ML
author wenzelm
Fri Mar 28 19:43:54 2008 +0100 (2008-03-28)
changeset 26462 dac4e2bce00d
parent 25919 8b1c0d434824
child 27651 16a26996c30e
permissions -rw-r--r--
avoid rebinding of existing facts;
wenzelm@23164
     1
(*  Title:      HOL/nat_simprocs.ML
wenzelm@23164
     2
    ID:         $Id$
wenzelm@23164
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
wenzelm@23164
     4
    Copyright   2000  University of Cambridge
wenzelm@23164
     5
wenzelm@23164
     6
Simprocs for nat numerals.
wenzelm@23164
     7
*)
wenzelm@23164
     8
wenzelm@23164
     9
structure Nat_Numeral_Simprocs =
wenzelm@23164
    10
struct
wenzelm@23164
    11
wenzelm@23164
    12
(*Maps n to #n for n = 0, 1, 2*)
wenzelm@23164
    13
val numeral_syms =
huffman@23471
    14
       [@{thm nat_numeral_0_eq_0} RS sym, @{thm nat_numeral_1_eq_1} RS sym, @{thm numeral_2_eq_2} RS sym];
wenzelm@23164
    15
val numeral_sym_ss = HOL_ss addsimps numeral_syms;
wenzelm@23164
    16
wenzelm@23164
    17
fun rename_numerals th =
wenzelm@23164
    18
    simplify numeral_sym_ss (Thm.transfer (the_context ()) th);
wenzelm@23164
    19
wenzelm@23164
    20
(*Utilities*)
wenzelm@23164
    21
wenzelm@23164
    22
fun mk_number n = HOLogic.number_of_const HOLogic.natT $ HOLogic.mk_numeral n;
wenzelm@24630
    23
fun dest_number t = Int.max (0, snd (HOLogic.dest_number t));
wenzelm@23164
    24
wenzelm@23164
    25
fun find_first_numeral past (t::terms) =
wenzelm@23164
    26
        ((dest_number t, t, rev past @ terms)
wenzelm@23164
    27
         handle TERM _ => find_first_numeral (t::past) terms)
wenzelm@23164
    28
  | find_first_numeral past [] = raise TERM("find_first_numeral", []);
wenzelm@23164
    29
wenzelm@23164
    30
val zero = mk_number 0;
wenzelm@23164
    31
val mk_plus = HOLogic.mk_binop @{const_name HOL.plus};
wenzelm@23164
    32
wenzelm@23164
    33
(*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*)
wenzelm@23164
    34
fun mk_sum []        = zero
wenzelm@23164
    35
  | mk_sum [t,u]     = mk_plus (t, u)
wenzelm@23164
    36
  | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
wenzelm@23164
    37
wenzelm@23164
    38
(*this version ALWAYS includes a trailing zero*)
wenzelm@23164
    39
fun long_mk_sum []        = HOLogic.zero
wenzelm@23164
    40
  | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
wenzelm@23164
    41
wenzelm@23164
    42
val dest_plus = HOLogic.dest_bin @{const_name HOL.plus} HOLogic.natT;
wenzelm@23164
    43
wenzelm@23164
    44
wenzelm@23164
    45
(** Other simproc items **)
wenzelm@23164
    46
wenzelm@23164
    47
val trans_tac = Int_Numeral_Simprocs.trans_tac;
wenzelm@23164
    48
wenzelm@23164
    49
val bin_simps =
huffman@23471
    50
     [@{thm nat_numeral_0_eq_0} RS sym, @{thm nat_numeral_1_eq_1} RS sym,
huffman@23471
    51
      @{thm add_nat_number_of}, @{thm nat_number_of_add_left}, 
huffman@23471
    52
      @{thm diff_nat_number_of}, @{thm le_number_of_eq_not_less},
huffman@23471
    53
      @{thm mult_nat_number_of}, @{thm nat_number_of_mult_left}, 
huffman@23471
    54
      @{thm less_nat_number_of}, 
huffman@23471
    55
      @{thm Let_number_of}, @{thm nat_number_of}] @
haftmann@25481
    56
     @{thms arith_simps} @ @{thms rel_simps};
wenzelm@23164
    57
wenzelm@23164
    58
fun prep_simproc (name, pats, proc) =
wenzelm@23164
    59
  Simplifier.simproc (the_context ()) name pats proc;
wenzelm@23164
    60
wenzelm@23164
    61
wenzelm@23164
    62
(*** CancelNumerals simprocs ***)
wenzelm@23164
    63
wenzelm@23164
    64
val one = mk_number 1;
wenzelm@23164
    65
val mk_times = HOLogic.mk_binop @{const_name HOL.times};
wenzelm@23164
    66
wenzelm@23164
    67
fun mk_prod [] = one
wenzelm@23164
    68
  | mk_prod [t] = t
wenzelm@23164
    69
  | mk_prod (t :: ts) = if t = one then mk_prod ts
wenzelm@23164
    70
                        else mk_times (t, mk_prod ts);
wenzelm@23164
    71
wenzelm@23164
    72
val dest_times = HOLogic.dest_bin @{const_name HOL.times} HOLogic.natT;
wenzelm@23164
    73
wenzelm@23164
    74
fun dest_prod t =
wenzelm@23164
    75
      let val (t,u) = dest_times t
wenzelm@23164
    76
      in  dest_prod t @ dest_prod u  end
wenzelm@23164
    77
      handle TERM _ => [t];
wenzelm@23164
    78
wenzelm@23164
    79
(*DON'T do the obvious simplifications; that would create special cases*)
wenzelm@23164
    80
fun mk_coeff (k,t) = mk_times (mk_number k, t);
wenzelm@23164
    81
wenzelm@23164
    82
(*Express t as a product of (possibly) a numeral with other factors, sorted*)
wenzelm@23164
    83
fun dest_coeff t =
wenzelm@23164
    84
    let val ts = sort Term.term_ord (dest_prod t)
wenzelm@23164
    85
        val (n, _, ts') = find_first_numeral [] ts
wenzelm@23164
    86
                          handle TERM _ => (1, one, ts)
wenzelm@23164
    87
    in (n, mk_prod ts') end;
wenzelm@23164
    88
wenzelm@23164
    89
(*Find first coefficient-term THAT MATCHES u*)
wenzelm@23164
    90
fun find_first_coeff past u [] = raise TERM("find_first_coeff", [])
wenzelm@23164
    91
  | find_first_coeff past u (t::terms) =
wenzelm@23164
    92
        let val (n,u') = dest_coeff t
wenzelm@23164
    93
        in  if u aconv u' then (n, rev past @ terms)
wenzelm@23164
    94
                          else find_first_coeff (t::past) u terms
wenzelm@23164
    95
        end
wenzelm@23164
    96
        handle TERM _ => find_first_coeff (t::past) u terms;
wenzelm@23164
    97
wenzelm@23164
    98
wenzelm@23164
    99
(*Split up a sum into the list of its constituent terms, on the way removing any
wenzelm@23164
   100
  Sucs and counting them.*)
wenzelm@23164
   101
fun dest_Suc_sum (Const ("Suc", _) $ t, (k,ts)) = dest_Suc_sum (t, (k+1,ts))
wenzelm@23164
   102
  | dest_Suc_sum (t, (k,ts)) = 
wenzelm@23164
   103
      let val (t1,t2) = dest_plus t
wenzelm@23164
   104
      in  dest_Suc_sum (t1, dest_Suc_sum (t2, (k,ts)))  end
wenzelm@23164
   105
      handle TERM _ => (k, t::ts);
wenzelm@23164
   106
wenzelm@23164
   107
(*Code for testing whether numerals are already used in the goal*)
haftmann@25919
   108
fun is_numeral (Const(@{const_name Int.number_of}, _) $ w) = true
wenzelm@23164
   109
  | is_numeral _ = false;
wenzelm@23164
   110
wenzelm@23164
   111
fun prod_has_numeral t = exists is_numeral (dest_prod t);
wenzelm@23164
   112
wenzelm@23164
   113
(*The Sucs found in the term are converted to a binary numeral. If relaxed is false,
wenzelm@23164
   114
  an exception is raised unless the original expression contains at least one
wenzelm@23164
   115
  numeral in a coefficient position.  This prevents nat_combine_numerals from 
wenzelm@23164
   116
  introducing numerals to goals.*)
wenzelm@23164
   117
fun dest_Sucs_sum relaxed t = 
wenzelm@23164
   118
  let val (k,ts) = dest_Suc_sum (t,(0,[]))
wenzelm@23164
   119
  in
wenzelm@23164
   120
     if relaxed orelse exists prod_has_numeral ts then 
wenzelm@23164
   121
       if k=0 then ts
wenzelm@24630
   122
       else mk_number k :: ts
wenzelm@23164
   123
     else raise TERM("Nat_Numeral_Simprocs.dest_Sucs_sum", [t])
wenzelm@23164
   124
  end;
wenzelm@23164
   125
wenzelm@23164
   126
wenzelm@23164
   127
(*Simplify 1*n and n*1 to n*)
haftmann@23881
   128
val add_0s  = map rename_numerals [@{thm add_0}, @{thm add_0_right}];
wenzelm@23164
   129
val mult_1s = map rename_numerals [@{thm nat_mult_1}, @{thm nat_mult_1_right}];
wenzelm@23164
   130
wenzelm@23164
   131
(*Final simplification: cancel + and *; replace Numeral0 by 0 and Numeral1 by 1*)
wenzelm@23164
   132
wenzelm@23164
   133
(*And these help the simproc return False when appropriate, which helps
wenzelm@23164
   134
  the arith prover.*)
haftmann@23881
   135
val contra_rules = [@{thm add_Suc}, @{thm add_Suc_right}, @{thm Zero_not_Suc},
haftmann@23881
   136
  @{thm Suc_not_Zero}, @{thm le_0_eq}];
wenzelm@23164
   137
wenzelm@23164
   138
val simplify_meta_eq =
wenzelm@23164
   139
    Int_Numeral_Simprocs.simplify_meta_eq
huffman@23471
   140
        ([@{thm nat_numeral_0_eq_0}, @{thm numeral_1_eq_Suc_0}, @{thm add_0}, @{thm add_0_right},
huffman@23471
   141
          @{thm mult_0}, @{thm mult_0_right}, @{thm mult_1}, @{thm mult_1_right}] @ contra_rules);
wenzelm@23164
   142
wenzelm@23164
   143
wenzelm@23164
   144
(*Like HOL_ss but with an ordering that brings numerals to the front
wenzelm@23164
   145
  under AC-rewriting.*)
wenzelm@23164
   146
val num_ss = Int_Numeral_Simprocs.num_ss;
wenzelm@23164
   147
wenzelm@23164
   148
(*** Applying CancelNumeralsFun ***)
wenzelm@23164
   149
wenzelm@23164
   150
structure CancelNumeralsCommon =
wenzelm@23164
   151
  struct
wenzelm@23164
   152
  val mk_sum            = (fn T:typ => mk_sum)
wenzelm@23164
   153
  val dest_sum          = dest_Sucs_sum true
wenzelm@23164
   154
  val mk_coeff          = mk_coeff
wenzelm@23164
   155
  val dest_coeff        = dest_coeff
wenzelm@23164
   156
  val find_first_coeff  = find_first_coeff []
wenzelm@23164
   157
  val trans_tac         = fn _ => trans_tac
wenzelm@23164
   158
wenzelm@23164
   159
  val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
haftmann@23881
   160
    [@{thm Suc_eq_add_numeral_1_left}] @ @{thms add_ac}
haftmann@23881
   161
  val norm_ss2 = num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
wenzelm@23164
   162
  fun norm_tac ss = 
wenzelm@23164
   163
    ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
wenzelm@23164
   164
    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
wenzelm@23164
   165
wenzelm@23164
   166
  val numeral_simp_ss = HOL_ss addsimps add_0s @ bin_simps;
wenzelm@23164
   167
  fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss));
wenzelm@23164
   168
  val simplify_meta_eq  = simplify_meta_eq
wenzelm@23164
   169
  end;
wenzelm@23164
   170
wenzelm@23164
   171
wenzelm@23164
   172
structure EqCancelNumerals = CancelNumeralsFun
wenzelm@23164
   173
 (open CancelNumeralsCommon
wenzelm@23164
   174
  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
wenzelm@23164
   175
  val mk_bal   = HOLogic.mk_eq
wenzelm@23164
   176
  val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
huffman@23471
   177
  val bal_add1 = @{thm nat_eq_add_iff1} RS trans
huffman@23471
   178
  val bal_add2 = @{thm nat_eq_add_iff2} RS trans
wenzelm@23164
   179
);
wenzelm@23164
   180
wenzelm@23164
   181
structure LessCancelNumerals = CancelNumeralsFun
wenzelm@23164
   182
 (open CancelNumeralsCommon
wenzelm@23164
   183
  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
haftmann@23881
   184
  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
haftmann@23881
   185
  val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT
huffman@23471
   186
  val bal_add1 = @{thm nat_less_add_iff1} RS trans
huffman@23471
   187
  val bal_add2 = @{thm nat_less_add_iff2} RS trans
wenzelm@23164
   188
);
wenzelm@23164
   189
wenzelm@23164
   190
structure LeCancelNumerals = CancelNumeralsFun
wenzelm@23164
   191
 (open CancelNumeralsCommon
wenzelm@23164
   192
  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
haftmann@23881
   193
  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
haftmann@23881
   194
  val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT
huffman@23471
   195
  val bal_add1 = @{thm nat_le_add_iff1} RS trans
huffman@23471
   196
  val bal_add2 = @{thm nat_le_add_iff2} RS trans
wenzelm@23164
   197
);
wenzelm@23164
   198
wenzelm@23164
   199
structure DiffCancelNumerals = CancelNumeralsFun
wenzelm@23164
   200
 (open CancelNumeralsCommon
wenzelm@23164
   201
  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
wenzelm@23164
   202
  val mk_bal   = HOLogic.mk_binop @{const_name HOL.minus}
wenzelm@23164
   203
  val dest_bal = HOLogic.dest_bin @{const_name HOL.minus} HOLogic.natT
huffman@23471
   204
  val bal_add1 = @{thm nat_diff_add_eq1} RS trans
huffman@23471
   205
  val bal_add2 = @{thm nat_diff_add_eq2} RS trans
wenzelm@23164
   206
);
wenzelm@23164
   207
wenzelm@23164
   208
wenzelm@23164
   209
val cancel_numerals =
wenzelm@23164
   210
  map prep_simproc
wenzelm@23164
   211
   [("nateq_cancel_numerals",
wenzelm@23164
   212
     ["(l::nat) + m = n", "(l::nat) = m + n",
wenzelm@23164
   213
      "(l::nat) * m = n", "(l::nat) = m * n",
wenzelm@23164
   214
      "Suc m = n", "m = Suc n"],
wenzelm@23164
   215
     K EqCancelNumerals.proc),
wenzelm@23164
   216
    ("natless_cancel_numerals",
wenzelm@23164
   217
     ["(l::nat) + m < n", "(l::nat) < m + n",
wenzelm@23164
   218
      "(l::nat) * m < n", "(l::nat) < m * n",
wenzelm@23164
   219
      "Suc m < n", "m < Suc n"],
wenzelm@23164
   220
     K LessCancelNumerals.proc),
wenzelm@23164
   221
    ("natle_cancel_numerals",
wenzelm@23164
   222
     ["(l::nat) + m <= n", "(l::nat) <= m + n",
wenzelm@23164
   223
      "(l::nat) * m <= n", "(l::nat) <= m * n",
wenzelm@23164
   224
      "Suc m <= n", "m <= Suc n"],
wenzelm@23164
   225
     K LeCancelNumerals.proc),
wenzelm@23164
   226
    ("natdiff_cancel_numerals",
wenzelm@23164
   227
     ["((l::nat) + m) - n", "(l::nat) - (m + n)",
wenzelm@23164
   228
      "(l::nat) * m - n", "(l::nat) - m * n",
wenzelm@23164
   229
      "Suc m - n", "m - Suc n"],
wenzelm@23164
   230
     K DiffCancelNumerals.proc)];
wenzelm@23164
   231
wenzelm@23164
   232
wenzelm@23164
   233
(*** Applying CombineNumeralsFun ***)
wenzelm@23164
   234
wenzelm@23164
   235
structure CombineNumeralsData =
wenzelm@23164
   236
  struct
wenzelm@24630
   237
  type coeff            = int
wenzelm@24630
   238
  val iszero            = (fn x => x = 0)
wenzelm@24630
   239
  val add               = op +
wenzelm@23164
   240
  val mk_sum            = (fn T:typ => long_mk_sum)  (*to work for 2*x + 3*x *)
wenzelm@23164
   241
  val dest_sum          = dest_Sucs_sum false
wenzelm@23164
   242
  val mk_coeff          = mk_coeff
wenzelm@23164
   243
  val dest_coeff        = dest_coeff
huffman@23471
   244
  val left_distrib      = @{thm left_add_mult_distrib} RS trans
wenzelm@23164
   245
  val prove_conv        = Int_Numeral_Base_Simprocs.prove_conv_nohyps
wenzelm@23164
   246
  val trans_tac         = fn _ => trans_tac
wenzelm@23164
   247
haftmann@23881
   248
  val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1}] @ @{thms add_ac}
haftmann@23881
   249
  val norm_ss2 = num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
wenzelm@23164
   250
  fun norm_tac ss =
wenzelm@23164
   251
    ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
wenzelm@23164
   252
    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
wenzelm@23164
   253
wenzelm@23164
   254
  val numeral_simp_ss = HOL_ss addsimps add_0s @ bin_simps;
wenzelm@23164
   255
  fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
wenzelm@23164
   256
  val simplify_meta_eq  = simplify_meta_eq
wenzelm@23164
   257
  end;
wenzelm@23164
   258
wenzelm@23164
   259
structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
wenzelm@23164
   260
wenzelm@23164
   261
val combine_numerals =
wenzelm@23164
   262
  prep_simproc ("nat_combine_numerals", ["(i::nat) + j", "Suc (i + j)"], K CombineNumerals.proc);
wenzelm@23164
   263
wenzelm@23164
   264
wenzelm@23164
   265
(*** Applying CancelNumeralFactorFun ***)
wenzelm@23164
   266
wenzelm@23164
   267
structure CancelNumeralFactorCommon =
wenzelm@23164
   268
  struct
wenzelm@23164
   269
  val mk_coeff          = mk_coeff
wenzelm@23164
   270
  val dest_coeff        = dest_coeff
wenzelm@23164
   271
  val trans_tac         = fn _ => trans_tac
wenzelm@23164
   272
wenzelm@23164
   273
  val norm_ss1 = num_ss addsimps
haftmann@23881
   274
    numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1_left}] @ @{thms add_ac}
haftmann@23881
   275
  val norm_ss2 = num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
wenzelm@23164
   276
  fun norm_tac ss =
wenzelm@23164
   277
    ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
wenzelm@23164
   278
    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
wenzelm@23164
   279
wenzelm@23164
   280
  val numeral_simp_ss = HOL_ss addsimps bin_simps
wenzelm@23164
   281
  fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
wenzelm@23164
   282
  val simplify_meta_eq  = simplify_meta_eq
wenzelm@23164
   283
  end
wenzelm@23164
   284
wenzelm@23164
   285
structure DivCancelNumeralFactor = CancelNumeralFactorFun
wenzelm@23164
   286
 (open CancelNumeralFactorCommon
wenzelm@23164
   287
  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
wenzelm@23164
   288
  val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
wenzelm@23164
   289
  val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.natT
huffman@23471
   290
  val cancel = @{thm nat_mult_div_cancel1} RS trans
wenzelm@23164
   291
  val neg_exchanges = false
wenzelm@23164
   292
)
wenzelm@23164
   293
nipkow@23969
   294
structure DvdCancelNumeralFactor = CancelNumeralFactorFun
nipkow@23969
   295
 (open CancelNumeralFactorCommon
nipkow@23969
   296
  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
nipkow@23969
   297
  val mk_bal   = HOLogic.mk_binrel @{const_name Divides.dvd}
nipkow@23969
   298
  val dest_bal = HOLogic.dest_bin @{const_name Divides.dvd} HOLogic.natT
nipkow@23969
   299
  val cancel = @{thm nat_mult_dvd_cancel1} RS trans
nipkow@23969
   300
  val neg_exchanges = false
nipkow@23969
   301
)
nipkow@23969
   302
wenzelm@23164
   303
structure EqCancelNumeralFactor = CancelNumeralFactorFun
wenzelm@23164
   304
 (open CancelNumeralFactorCommon
wenzelm@23164
   305
  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
wenzelm@23164
   306
  val mk_bal   = HOLogic.mk_eq
wenzelm@23164
   307
  val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
huffman@23471
   308
  val cancel = @{thm nat_mult_eq_cancel1} RS trans
wenzelm@23164
   309
  val neg_exchanges = false
wenzelm@23164
   310
)
wenzelm@23164
   311
wenzelm@23164
   312
structure LessCancelNumeralFactor = CancelNumeralFactorFun
wenzelm@23164
   313
 (open CancelNumeralFactorCommon
wenzelm@23164
   314
  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
haftmann@23881
   315
  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
haftmann@23881
   316
  val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT
huffman@23471
   317
  val cancel = @{thm nat_mult_less_cancel1} RS trans
wenzelm@23164
   318
  val neg_exchanges = true
wenzelm@23164
   319
)
wenzelm@23164
   320
wenzelm@23164
   321
structure LeCancelNumeralFactor = CancelNumeralFactorFun
wenzelm@23164
   322
 (open CancelNumeralFactorCommon
wenzelm@23164
   323
  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
haftmann@23881
   324
  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
haftmann@23881
   325
  val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT
huffman@23471
   326
  val cancel = @{thm nat_mult_le_cancel1} RS trans
wenzelm@23164
   327
  val neg_exchanges = true
wenzelm@23164
   328
)
wenzelm@23164
   329
wenzelm@23164
   330
val cancel_numeral_factors =
wenzelm@23164
   331
  map prep_simproc
wenzelm@23164
   332
   [("nateq_cancel_numeral_factors",
wenzelm@23164
   333
     ["(l::nat) * m = n", "(l::nat) = m * n"],
wenzelm@23164
   334
     K EqCancelNumeralFactor.proc),
wenzelm@23164
   335
    ("natless_cancel_numeral_factors",
wenzelm@23164
   336
     ["(l::nat) * m < n", "(l::nat) < m * n"],
wenzelm@23164
   337
     K LessCancelNumeralFactor.proc),
wenzelm@23164
   338
    ("natle_cancel_numeral_factors",
wenzelm@23164
   339
     ["(l::nat) * m <= n", "(l::nat) <= m * n"],
wenzelm@23164
   340
     K LeCancelNumeralFactor.proc),
wenzelm@23164
   341
    ("natdiv_cancel_numeral_factors",
wenzelm@23164
   342
     ["((l::nat) * m) div n", "(l::nat) div (m * n)"],
nipkow@23969
   343
     K DivCancelNumeralFactor.proc),
nipkow@23969
   344
    ("natdvd_cancel_numeral_factors",
nipkow@23969
   345
     ["((l::nat) * m) dvd n", "(l::nat) dvd (m * n)"],
nipkow@23969
   346
     K DvdCancelNumeralFactor.proc)];
wenzelm@23164
   347
wenzelm@23164
   348
wenzelm@23164
   349
wenzelm@23164
   350
(*** Applying ExtractCommonTermFun ***)
wenzelm@23164
   351
wenzelm@23164
   352
(*this version ALWAYS includes a trailing one*)
wenzelm@23164
   353
fun long_mk_prod []        = one
wenzelm@23164
   354
  | long_mk_prod (t :: ts) = mk_times (t, mk_prod ts);
wenzelm@23164
   355
wenzelm@23164
   356
(*Find first term that matches u*)
wenzelm@23164
   357
fun find_first_t past u []         = raise TERM("find_first_t", [])
wenzelm@23164
   358
  | find_first_t past u (t::terms) =
wenzelm@23164
   359
        if u aconv t then (rev past @ terms)
wenzelm@23164
   360
        else find_first_t (t::past) u terms
wenzelm@23164
   361
        handle TERM _ => find_first_t (t::past) u terms;
wenzelm@23164
   362
wenzelm@23164
   363
(** Final simplification for the CancelFactor simprocs **)
wenzelm@23164
   364
val simplify_one = Int_Numeral_Simprocs.simplify_meta_eq  
wenzelm@23164
   365
  [@{thm mult_1_left}, @{thm mult_1_right}, @{thm div_1}, @{thm numeral_1_eq_Suc_0}];
wenzelm@23164
   366
wenzelm@23164
   367
fun cancel_simplify_meta_eq cancel_th ss th =
wenzelm@23164
   368
    simplify_one ss (([th, cancel_th]) MRS trans);
wenzelm@23164
   369
wenzelm@23164
   370
structure CancelFactorCommon =
wenzelm@23164
   371
  struct
wenzelm@23164
   372
  val mk_sum            = (fn T:typ => long_mk_prod)
wenzelm@23164
   373
  val dest_sum          = dest_prod
wenzelm@23164
   374
  val mk_coeff          = mk_coeff
wenzelm@23164
   375
  val dest_coeff        = dest_coeff
wenzelm@23164
   376
  val find_first        = find_first_t []
wenzelm@23164
   377
  val trans_tac         = fn _ => trans_tac
haftmann@23881
   378
  val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac}
wenzelm@23164
   379
  fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
wenzelm@23164
   380
  end;
wenzelm@23164
   381
wenzelm@23164
   382
structure EqCancelFactor = ExtractCommonTermFun
wenzelm@23164
   383
 (open CancelFactorCommon
wenzelm@23164
   384
  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
wenzelm@23164
   385
  val mk_bal   = HOLogic.mk_eq
wenzelm@23164
   386
  val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
huffman@23471
   387
  val simplify_meta_eq  = cancel_simplify_meta_eq @{thm nat_mult_eq_cancel_disj}
wenzelm@23164
   388
);
wenzelm@23164
   389
wenzelm@23164
   390
structure LessCancelFactor = ExtractCommonTermFun
wenzelm@23164
   391
 (open CancelFactorCommon
wenzelm@23164
   392
  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
haftmann@23881
   393
  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
haftmann@23881
   394
  val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT
huffman@23471
   395
  val simplify_meta_eq  = cancel_simplify_meta_eq @{thm nat_mult_less_cancel_disj}
wenzelm@23164
   396
);
wenzelm@23164
   397
wenzelm@23164
   398
structure LeCancelFactor = ExtractCommonTermFun
wenzelm@23164
   399
 (open CancelFactorCommon
wenzelm@23164
   400
  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
haftmann@23881
   401
  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
haftmann@23881
   402
  val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT
huffman@23471
   403
  val simplify_meta_eq  = cancel_simplify_meta_eq @{thm nat_mult_le_cancel_disj}
wenzelm@23164
   404
);
wenzelm@23164
   405
wenzelm@23164
   406
structure DivideCancelFactor = ExtractCommonTermFun
wenzelm@23164
   407
 (open CancelFactorCommon
wenzelm@23164
   408
  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
wenzelm@23164
   409
  val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
wenzelm@23164
   410
  val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.natT
huffman@23471
   411
  val simplify_meta_eq  = cancel_simplify_meta_eq @{thm nat_mult_div_cancel_disj}
wenzelm@23164
   412
);
wenzelm@23164
   413
nipkow@23969
   414
structure DvdCancelFactor = ExtractCommonTermFun
nipkow@23969
   415
 (open CancelFactorCommon
nipkow@23969
   416
  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
nipkow@23969
   417
  val mk_bal   = HOLogic.mk_binrel @{const_name Divides.dvd}
nipkow@23969
   418
  val dest_bal = HOLogic.dest_bin @{const_name Divides.dvd} HOLogic.natT
nipkow@23969
   419
  val simplify_meta_eq  = cancel_simplify_meta_eq @{thm nat_mult_dvd_cancel_disj}
nipkow@23969
   420
);
nipkow@23969
   421
wenzelm@23164
   422
val cancel_factor =
wenzelm@23164
   423
  map prep_simproc
wenzelm@23164
   424
   [("nat_eq_cancel_factor",
wenzelm@23164
   425
     ["(l::nat) * m = n", "(l::nat) = m * n"],
wenzelm@23164
   426
     K EqCancelFactor.proc),
wenzelm@23164
   427
    ("nat_less_cancel_factor",
wenzelm@23164
   428
     ["(l::nat) * m < n", "(l::nat) < m * n"],
wenzelm@23164
   429
     K LessCancelFactor.proc),
wenzelm@23164
   430
    ("nat_le_cancel_factor",
wenzelm@23164
   431
     ["(l::nat) * m <= n", "(l::nat) <= m * n"],
wenzelm@23164
   432
     K LeCancelFactor.proc),
wenzelm@23164
   433
    ("nat_divide_cancel_factor",
wenzelm@23164
   434
     ["((l::nat) * m) div n", "(l::nat) div (m * n)"],
nipkow@23969
   435
     K DivideCancelFactor.proc),
nipkow@23969
   436
    ("nat_dvd_cancel_factor",
nipkow@23969
   437
     ["((l::nat) * m) dvd n", "(l::nat) dvd (m * n)"],
nipkow@23969
   438
     K DvdCancelFactor.proc)];
wenzelm@23164
   439
wenzelm@23164
   440
end;
wenzelm@23164
   441
wenzelm@23164
   442
wenzelm@23164
   443
Addsimprocs Nat_Numeral_Simprocs.cancel_numerals;
wenzelm@23164
   444
Addsimprocs [Nat_Numeral_Simprocs.combine_numerals];
wenzelm@23164
   445
Addsimprocs Nat_Numeral_Simprocs.cancel_numeral_factors;
wenzelm@23164
   446
Addsimprocs Nat_Numeral_Simprocs.cancel_factor;
wenzelm@23164
   447
wenzelm@23164
   448
wenzelm@23164
   449
(*examples:
wenzelm@23164
   450
print_depth 22;
wenzelm@23164
   451
set timing;
wenzelm@23164
   452
set trace_simp;
wenzelm@23164
   453
fun test s = (Goal s; by (Simp_tac 1));
wenzelm@23164
   454
wenzelm@23164
   455
(*cancel_numerals*)
wenzelm@23164
   456
test "l +( 2) + (2) + 2 + (l + 2) + (oo  + 2) = (uu::nat)";
wenzelm@23164
   457
test "(2*length xs < 2*length xs + j)";
wenzelm@23164
   458
test "(2*length xs < length xs * 2 + j)";
wenzelm@23164
   459
test "2*u = (u::nat)";
wenzelm@23164
   460
test "2*u = Suc (u)";
wenzelm@23164
   461
test "(i + j + 12 + (k::nat)) - 15 = y";
wenzelm@23164
   462
test "(i + j + 12 + (k::nat)) - 5 = y";
wenzelm@23164
   463
test "Suc u - 2 = y";
wenzelm@23164
   464
test "Suc (Suc (Suc u)) - 2 = y";
wenzelm@23164
   465
test "(i + j + 2 + (k::nat)) - 1 = y";
wenzelm@23164
   466
test "(i + j + 1 + (k::nat)) - 2 = y";
wenzelm@23164
   467
wenzelm@23164
   468
test "(2*x + (u*v) + y) - v*3*u = (w::nat)";
wenzelm@23164
   469
test "(2*x*u*v + 5 + (u*v)*4 + y) - v*u*4 = (w::nat)";
wenzelm@23164
   470
test "(2*x*u*v + (u*v)*4 + y) - v*u = (w::nat)";
wenzelm@23164
   471
test "Suc (Suc (2*x*u*v + u*4 + y)) - u = w";
wenzelm@23164
   472
test "Suc ((u*v)*4) - v*3*u = w";
wenzelm@23164
   473
test "Suc (Suc ((u*v)*3)) - v*3*u = w";
wenzelm@23164
   474
wenzelm@23164
   475
test "(i + j + 12 + (k::nat)) = u + 15 + y";
wenzelm@23164
   476
test "(i + j + 32 + (k::nat)) - (u + 15 + y) = zz";
wenzelm@23164
   477
test "(i + j + 12 + (k::nat)) = u + 5 + y";
wenzelm@23164
   478
(*Suc*)
wenzelm@23164
   479
test "(i + j + 12 + k) = Suc (u + y)";
wenzelm@23164
   480
test "Suc (Suc (Suc (Suc (Suc (u + y))))) <= ((i + j) + 41 + k)";
wenzelm@23164
   481
test "(i + j + 5 + k) < Suc (Suc (Suc (Suc (Suc (u + y)))))";
wenzelm@23164
   482
test "Suc (Suc (Suc (Suc (Suc (u + y))))) - 5 = v";
wenzelm@23164
   483
test "(i + j + 5 + k) = Suc (Suc (Suc (Suc (Suc (Suc (Suc (u + y)))))))";
wenzelm@23164
   484
test "2*y + 3*z + 2*u = Suc (u)";
wenzelm@23164
   485
test "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = Suc (u)";
wenzelm@23164
   486
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)";
wenzelm@23164
   487
test "6 + 2*y + 3*z + 4*u = Suc (vv + 2*u + z)";
wenzelm@23164
   488
test "(2*n*m) < (3*(m*n)) + (u::nat)";
wenzelm@23164
   489
wenzelm@23164
   490
test "(Suc (Suc (Suc (Suc (Suc (Suc (case length (f c) of 0 => 0 | Suc k => k)))))) <= Suc 0)";
wenzelm@23164
   491
 
wenzelm@23164
   492
test "Suc (Suc (Suc (Suc (Suc (Suc (length l1 + length l2)))))) <= length l1";
wenzelm@23164
   493
wenzelm@23164
   494
test "( (Suc (Suc (Suc (Suc (Suc (length (compT P E A ST mxr e) + length l3)))))) <= length (compT P E A ST mxr e))";
wenzelm@23164
   495
wenzelm@23164
   496
test "( (Suc (Suc (Suc (Suc (Suc (length (compT P E A ST mxr e) + length (compT P E (A Un \<A> e) ST mxr c))))))) <= length (compT P E A ST mxr e))";
wenzelm@23164
   497
wenzelm@23164
   498
wenzelm@23164
   499
(*negative numerals: FAIL*)
wenzelm@23164
   500
test "(i + j + -23 + (k::nat)) < u + 15 + y";
wenzelm@23164
   501
test "(i + j + 3 + (k::nat)) < u + -15 + y";
wenzelm@23164
   502
test "(i + j + -12 + (k::nat)) - 15 = y";
wenzelm@23164
   503
test "(i + j + 12 + (k::nat)) - -15 = y";
wenzelm@23164
   504
test "(i + j + -12 + (k::nat)) - -15 = y";
wenzelm@23164
   505
wenzelm@23164
   506
(*combine_numerals*)
wenzelm@23164
   507
test "k + 3*k = (u::nat)";
wenzelm@23164
   508
test "Suc (i + 3) = u";
wenzelm@23164
   509
test "Suc (i + j + 3 + k) = u";
wenzelm@23164
   510
test "k + j + 3*k + j = (u::nat)";
wenzelm@23164
   511
test "Suc (j*i + i + k + 5 + 3*k + i*j*4) = (u::nat)";
wenzelm@23164
   512
test "(2*n*m) + (3*(m*n)) = (u::nat)";
wenzelm@23164
   513
(*negative numerals: FAIL*)
wenzelm@23164
   514
test "Suc (i + j + -3 + k) = u";
wenzelm@23164
   515
wenzelm@23164
   516
(*cancel_numeral_factors*)
wenzelm@23164
   517
test "9*x = 12 * (y::nat)";
wenzelm@23164
   518
test "(9*x) div (12 * (y::nat)) = z";
wenzelm@23164
   519
test "9*x < 12 * (y::nat)";
wenzelm@23164
   520
test "9*x <= 12 * (y::nat)";
wenzelm@23164
   521
wenzelm@23164
   522
(*cancel_factor*)
wenzelm@23164
   523
test "x*k = k*(y::nat)";
wenzelm@23164
   524
test "k = k*(y::nat)";
wenzelm@23164
   525
test "a*(b*c) = (b::nat)";
wenzelm@23164
   526
test "a*(b*c) = d*(b::nat)*(x*a)";
wenzelm@23164
   527
wenzelm@23164
   528
test "x*k < k*(y::nat)";
wenzelm@23164
   529
test "k < k*(y::nat)";
wenzelm@23164
   530
test "a*(b*c) < (b::nat)";
wenzelm@23164
   531
test "a*(b*c) < d*(b::nat)*(x*a)";
wenzelm@23164
   532
wenzelm@23164
   533
test "x*k <= k*(y::nat)";
wenzelm@23164
   534
test "k <= k*(y::nat)";
wenzelm@23164
   535
test "a*(b*c) <= (b::nat)";
wenzelm@23164
   536
test "a*(b*c) <= d*(b::nat)*(x*a)";
wenzelm@23164
   537
wenzelm@23164
   538
test "(x*k) div (k*(y::nat)) = (uu::nat)";
wenzelm@23164
   539
test "(k) div (k*(y::nat)) = (uu::nat)";
wenzelm@23164
   540
test "(a*(b*c)) div ((b::nat)) = (uu::nat)";
wenzelm@23164
   541
test "(a*(b*c)) div (d*(b::nat)*(x*a)) = (uu::nat)";
wenzelm@23164
   542
*)
wenzelm@23164
   543
wenzelm@23164
   544
wenzelm@23164
   545
(*** Prepare linear arithmetic for nat numerals ***)
wenzelm@23164
   546
wenzelm@23164
   547
local
wenzelm@23164
   548
wenzelm@23164
   549
(* reduce contradictory <= to False *)
nipkow@24431
   550
val add_rules = @{thms ring_distribs} @
huffman@23471
   551
  [@{thm Let_number_of}, @{thm Let_0}, @{thm Let_1}, @{thm nat_0}, @{thm nat_1},
huffman@23471
   552
   @{thm add_nat_number_of}, @{thm diff_nat_number_of}, @{thm mult_nat_number_of},
huffman@23471
   553
   @{thm eq_nat_number_of}, @{thm less_nat_number_of}, @{thm le_number_of_eq_not_less},
huffman@23471
   554
   @{thm le_Suc_number_of}, @{thm le_number_of_Suc},
huffman@23471
   555
   @{thm less_Suc_number_of}, @{thm less_number_of_Suc},
huffman@23471
   556
   @{thm Suc_eq_number_of}, @{thm eq_number_of_Suc},
huffman@23471
   557
   @{thm mult_Suc}, @{thm mult_Suc_right},
nipkow@24431
   558
   @{thm add_Suc}, @{thm add_Suc_right},
huffman@23471
   559
   @{thm eq_number_of_0}, @{thm eq_0_number_of}, @{thm less_0_number_of},
huffman@23471
   560
   @{thm of_int_number_of_eq}, @{thm of_nat_number_of_eq}, @{thm nat_number_of}, @{thm if_True}, @{thm if_False}];
wenzelm@23164
   561
nipkow@24431
   562
(* Products are multiplied out during proof (re)construction via
nipkow@24431
   563
ring_distribs. Ideally they should remain atomic. But that is
nipkow@24431
   564
currently not possible because 1 is replaced by Suc 0, and then some
nipkow@24431
   565
simprocs start to mess around with products like (n+1)*m. The rule
nipkow@24431
   566
1 == Suc 0 is necessary for early parts of HOL where numerals and
nipkow@24431
   567
simprocs are not yet available. But then it is difficult to remove
nipkow@24431
   568
that rule later on, because it may find its way back in when theories
nipkow@24431
   569
(and thus lin-arith simpsets) are merged. Otherwise one could turn the
nipkow@24431
   570
rule around (Suc n = n+1) and see if that helps products being left
nipkow@24431
   571
alone. *)
nipkow@24431
   572
wenzelm@23164
   573
val simprocs = Nat_Numeral_Simprocs.combine_numerals
wenzelm@23164
   574
  :: Nat_Numeral_Simprocs.cancel_numerals;
wenzelm@23164
   575
wenzelm@23164
   576
in
wenzelm@23164
   577
wenzelm@23164
   578
val nat_simprocs_setup =
wenzelm@24093
   579
  LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
wenzelm@23164
   580
   {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms,
wenzelm@23164
   581
    inj_thms = inj_thms, lessD = lessD, neqE = neqE,
wenzelm@23164
   582
    simpset = simpset addsimps add_rules
wenzelm@23164
   583
                      addsimprocs simprocs});
wenzelm@23164
   584
wenzelm@23164
   585
end;