src/HOL/Tools/numeral_simprocs.ML
author wenzelm
Tue Sep 26 20:54:40 2017 +0200 (23 months ago)
changeset 66695 91500c024c7f
parent 64240 eabf80376aab
child 67560 0fa87bd86566
permissions -rw-r--r--
tuned;
haftmann@31068
     1
(* Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
haftmann@31068
     2
   Copyright   2000  University of Cambridge
wenzelm@23164
     3
haftmann@36751
     4
Simprocs for the (integer) numerals.
wenzelm@23164
     5
*)
wenzelm@23164
     6
wenzelm@23164
     7
(*To quote from Provers/Arith/cancel_numeral_factor.ML:
wenzelm@23164
     8
wenzelm@23164
     9
Cancels common coefficients in balanced expressions:
wenzelm@23164
    10
wenzelm@23164
    11
     u*#m ~~ u'*#m'  ==  #n*u ~~ #n'*u'
wenzelm@23164
    12
wenzelm@23164
    13
where ~~ is an appropriate balancing operation (e.g. =, <=, <, div, /)
wenzelm@23164
    14
and d = gcd(m,m') and n=m/d and n'=m'/d.
wenzelm@23164
    15
*)
wenzelm@23164
    16
haftmann@31068
    17
signature NUMERAL_SIMPROCS =
haftmann@31068
    18
sig
wenzelm@59530
    19
  val trans_tac: Proof.context -> thm option -> tactic
wenzelm@51717
    20
  val assoc_fold: Proof.context -> cterm -> thm option
wenzelm@51717
    21
  val combine_numerals: Proof.context -> cterm -> thm option
wenzelm@51717
    22
  val eq_cancel_numerals: Proof.context -> cterm -> thm option
wenzelm@51717
    23
  val less_cancel_numerals: Proof.context -> cterm -> thm option
wenzelm@51717
    24
  val le_cancel_numerals: Proof.context -> cterm -> thm option
wenzelm@51717
    25
  val eq_cancel_factor: Proof.context -> cterm -> thm option
wenzelm@51717
    26
  val le_cancel_factor: Proof.context -> cterm -> thm option
wenzelm@51717
    27
  val less_cancel_factor: Proof.context -> cterm -> thm option
wenzelm@51717
    28
  val div_cancel_factor: Proof.context -> cterm -> thm option
wenzelm@51717
    29
  val mod_cancel_factor: Proof.context -> cterm -> thm option
wenzelm@51717
    30
  val dvd_cancel_factor: Proof.context -> cterm -> thm option
wenzelm@51717
    31
  val divide_cancel_factor: Proof.context -> cterm -> thm option
wenzelm@51717
    32
  val eq_cancel_numeral_factor: Proof.context -> cterm -> thm option
wenzelm@51717
    33
  val less_cancel_numeral_factor: Proof.context -> cterm -> thm option
wenzelm@51717
    34
  val le_cancel_numeral_factor: Proof.context -> cterm -> thm option
wenzelm@51717
    35
  val div_cancel_numeral_factor: Proof.context -> cterm -> thm option
wenzelm@51717
    36
  val divide_cancel_numeral_factor: Proof.context -> cterm -> thm option
wenzelm@51717
    37
  val field_combine_numerals: Proof.context -> cterm -> thm option
wenzelm@61144
    38
  val field_divide_cancel_numeral_factor: simproc
haftmann@31068
    39
  val num_ss: simpset
wenzelm@51717
    40
  val field_comp_conv: Proof.context -> conv
haftmann@31068
    41
end;
haftmann@31068
    42
haftmann@31068
    43
structure Numeral_Simprocs : NUMERAL_SIMPROCS =
haftmann@31068
    44
struct
haftmann@31068
    45
wenzelm@59530
    46
fun trans_tac _ NONE  = all_tac
wenzelm@59530
    47
  | trans_tac ctxt (SOME th) = ALLGOALS (resolve_tac ctxt [th RS trans]);
haftmann@44945
    48
haftmann@33359
    49
val mk_number = Arith_Data.mk_number;
haftmann@33359
    50
val mk_sum = Arith_Data.mk_sum;
haftmann@33359
    51
val long_mk_sum = Arith_Data.long_mk_sum;
haftmann@33359
    52
val dest_sum = Arith_Data.dest_sum;
haftmann@31068
    53
haftmann@35267
    54
val mk_times = HOLogic.mk_binop @{const_name Groups.times};
haftmann@31068
    55
haftmann@35267
    56
fun one_of T = Const(@{const_name Groups.one}, T);
haftmann@31068
    57
haftmann@31068
    58
(* build product with trailing 1 rather than Numeral 1 in order to avoid the
haftmann@31068
    59
   unnecessary restriction to type class number_ring
haftmann@31068
    60
   which is not required for cancellation of common factors in divisions.
huffman@47108
    61
   UPDATE: this reasoning no longer applies (number_ring is gone)
haftmann@31068
    62
*)
wenzelm@61144
    63
fun mk_prod T =
haftmann@31068
    64
  let val one = one_of T
haftmann@31068
    65
  fun mk [] = one
haftmann@31068
    66
    | mk [t] = t
haftmann@31068
    67
    | mk (t :: ts) = if t = one then mk ts else mk_times (t, mk ts)
haftmann@31068
    68
  in mk end;
haftmann@31068
    69
haftmann@31068
    70
(*This version ALWAYS includes a trailing one*)
haftmann@31068
    71
fun long_mk_prod T []        = one_of T
haftmann@31068
    72
  | long_mk_prod T (t :: ts) = mk_times (t, mk_prod T ts);
haftmann@31068
    73
wenzelm@49323
    74
val dest_times = HOLogic.dest_bin @{const_name Groups.times} dummyT;
haftmann@31068
    75
haftmann@31068
    76
fun dest_prod t =
haftmann@31068
    77
      let val (t,u) = dest_times t
haftmann@31068
    78
      in dest_prod t @ dest_prod u end
haftmann@31068
    79
      handle TERM _ => [t];
haftmann@31068
    80
haftmann@33359
    81
fun find_first_numeral past (t::terms) =
haftmann@33359
    82
        ((snd (HOLogic.dest_number t), rev past @ terms)
haftmann@33359
    83
         handle TERM _ => find_first_numeral (t::past) terms)
haftmann@33359
    84
  | find_first_numeral past [] = raise TERM("find_first_numeral", []);
haftmann@33359
    85
haftmann@31068
    86
(*DON'T do the obvious simplifications; that would create special cases*)
haftmann@31068
    87
fun mk_coeff (k, t) = mk_times (mk_number (Term.fastype_of t) k, t);
haftmann@31068
    88
haftmann@31068
    89
(*Express t as a product of (possibly) a numeral with other sorted terms*)
haftmann@35267
    90
fun dest_coeff sign (Const (@{const_name Groups.uminus}, _) $ t) = dest_coeff (~sign) t
haftmann@31068
    91
  | dest_coeff sign t =
wenzelm@35408
    92
    let val ts = sort Term_Ord.term_ord (dest_prod t)
haftmann@31068
    93
        val (n, ts') = find_first_numeral [] ts
haftmann@31068
    94
                          handle TERM _ => (1, ts)
haftmann@31068
    95
    in (sign*n, mk_prod (Term.fastype_of t) ts') end;
haftmann@31068
    96
haftmann@31068
    97
(*Find first coefficient-term THAT MATCHES u*)
haftmann@31068
    98
fun find_first_coeff past u [] = raise TERM("find_first_coeff", [])
haftmann@31068
    99
  | find_first_coeff past u (t::terms) =
haftmann@31068
   100
        let val (n,u') = dest_coeff 1 t
haftmann@31068
   101
        in if u aconv u' then (n, rev past @ terms)
haftmann@31068
   102
                         else find_first_coeff (t::past) u terms
haftmann@31068
   103
        end
haftmann@31068
   104
        handle TERM _ => find_first_coeff (t::past) u terms;
haftmann@31068
   105
haftmann@31068
   106
(*Fractions as pairs of ints. Can't use Rat.rat because the representation
haftmann@31068
   107
  needs to preserve negative values in the denominator.*)
haftmann@31068
   108
fun mk_frac (p, q) = if q = 0 then raise Div else (p, q);
haftmann@31068
   109
haftmann@31068
   110
(*Don't reduce fractions; sums must be proved by rule add_frac_eq.
haftmann@31068
   111
  Fractions are reduced later by the cancel_numeral_factor simproc.*)
haftmann@31068
   112
fun add_frac ((p1, q1), (p2, q2)) = (p1 * q2 + p2 * q1, q1 * q2);
haftmann@31068
   113
haftmann@60352
   114
val mk_divide = HOLogic.mk_binop @{const_name Rings.divide};
haftmann@31068
   115
haftmann@31068
   116
(*Build term (p / q) * t*)
haftmann@31068
   117
fun mk_fcoeff ((p, q), t) =
haftmann@31068
   118
  let val T = Term.fastype_of t
haftmann@31068
   119
  in mk_times (mk_divide (mk_number T p, mk_number T q), t) end;
haftmann@31068
   120
haftmann@31068
   121
(*Express t as a product of a fraction with other sorted terms*)
haftmann@35267
   122
fun dest_fcoeff sign (Const (@{const_name Groups.uminus}, _) $ t) = dest_fcoeff (~sign) t
haftmann@60352
   123
  | dest_fcoeff sign (Const (@{const_name Rings.divide}, _) $ t $ u) =
haftmann@31068
   124
    let val (p, t') = dest_coeff sign t
haftmann@31068
   125
        val (q, u') = dest_coeff 1 u
haftmann@31068
   126
    in (mk_frac (p, q), mk_divide (t', u')) end
haftmann@31068
   127
  | dest_fcoeff sign t =
haftmann@31068
   128
    let val (p, t') = dest_coeff sign t
haftmann@31068
   129
        val T = Term.fastype_of t
haftmann@31068
   130
    in (mk_frac (p, 1), mk_divide (t', one_of T)) end;
haftmann@31068
   131
haftmann@31068
   132
haftmann@31068
   133
(** New term ordering so that AC-rewriting brings numerals to the front **)
haftmann@31068
   134
haftmann@31068
   135
(*Order integers by absolute value and then by sign. The standard integer
haftmann@31068
   136
  ordering is not well-founded.*)
haftmann@31068
   137
fun num_ord (i,j) =
haftmann@31068
   138
  (case int_ord (abs i, abs j) of
wenzelm@61144
   139
    EQUAL => int_ord (Int.sign i, Int.sign j)
haftmann@31068
   140
  | ord => ord);
haftmann@31068
   141
wenzelm@35408
   142
(*This resembles Term_Ord.term_ord, but it puts binary numerals before other
haftmann@31068
   143
  non-atomic terms.*)
huffman@47108
   144
local open Term
huffman@47108
   145
in
huffman@47108
   146
fun numterm_ord (t, u) =
huffman@47108
   147
    case (try HOLogic.dest_number t, try HOLogic.dest_number u) of
huffman@47108
   148
      (SOME (_, i), SOME (_, j)) => num_ord (i, j)
huffman@47108
   149
    | (SOME _, NONE) => LESS
huffman@47108
   150
    | (NONE, SOME _) => GREATER
huffman@47108
   151
    | _ => (
huffman@47108
   152
      case (t, u) of
huffman@47108
   153
        (Abs (_, T, t), Abs(_, U, u)) =>
huffman@47108
   154
        (prod_ord numterm_ord Term_Ord.typ_ord ((t, T), (u, U)))
huffman@47108
   155
      | _ => (
huffman@47108
   156
        case int_ord (size_of_term t, size_of_term u) of
huffman@47108
   157
          EQUAL =>
haftmann@31068
   158
          let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
huffman@47108
   159
            (prod_ord Term_Ord.hd_ord numterms_ord ((f, ts), (g, us)))
haftmann@31068
   160
          end
huffman@47108
   161
        | ord => ord))
haftmann@31068
   162
and numterms_ord (ts, us) = list_ord numterm_ord (ts, us)
haftmann@31068
   163
end;
haftmann@31068
   164
haftmann@31068
   165
fun numtermless tu = (numterm_ord tu = LESS);
haftmann@31068
   166
wenzelm@51717
   167
val num_ss =
wenzelm@51717
   168
  simpset_of (put_simpset HOL_basic_ss @{context}
wenzelm@51717
   169
    |> Simplifier.set_termless numtermless);
haftmann@31068
   170
huffman@47108
   171
(*Maps 1 to Numeral1 so that arithmetic isn't complicated by the abstract 1.*)
lp15@61694
   172
val numeral_syms = [@{thm numeral_One} RS sym];
haftmann@31068
   173
huffman@47108
   174
(*Simplify 0+n, n+0, Numeral1*n, n*Numeral1, 1*x, x*1, x/1 *)
haftmann@59556
   175
val add_0s =  @{thms add_0_left add_0_right};
haftmann@64240
   176
val mult_1s = @{thms mult_1s divide_numeral_1 mult_1_left mult_1_right mult_minus1 mult_minus1_right div_by_1};
haftmann@31068
   177
huffman@45437
   178
(* For post-simplification of the rhs of simproc-generated rules *)
huffman@45437
   179
val post_simps =
lp15@61694
   180
    [@{thm numeral_One},
huffman@45437
   181
     @{thm add_0_left}, @{thm add_0_right},
huffman@45437
   182
     @{thm mult_zero_left}, @{thm mult_zero_right},
huffman@45437
   183
     @{thm mult_1_left}, @{thm mult_1_right},
huffman@45437
   184
     @{thm mult_minus1}, @{thm mult_minus1_right}]
huffman@45437
   185
huffman@45437
   186
val field_post_simps =
haftmann@64240
   187
    post_simps @ [@{thm div_0}, @{thm div_by_1}]
wenzelm@61144
   188
haftmann@54489
   189
(*Simplify inverse Numeral1*)
haftmann@31068
   190
val inverse_1s = [@{thm inverse_numeral_1}];
haftmann@31068
   191
haftmann@31068
   192
(*To perform binary arithmetic.  The "left" rewriting handles patterns
haftmann@31068
   193
  created by the Numeral_Simprocs, such as 3 * (5 * x). *)
huffman@47108
   194
val simps =
lp15@61694
   195
    [@{thm numeral_One} RS sym] @
huffman@47108
   196
    @{thms add_numeral_left} @
huffman@47108
   197
    @{thms add_neg_numeral_left} @
huffman@47108
   198
    @{thms mult_numeral_left} @
huffman@47108
   199
    @{thms arith_simps} @ @{thms rel_simps};
wenzelm@61144
   200
haftmann@31068
   201
(*Binary arithmetic BUT NOT ADDITION since it may collapse adjacent terms
haftmann@31068
   202
  during re-arrangement*)
haftmann@31068
   203
val non_add_simps =
huffman@47108
   204
  subtract Thm.eq_thm
huffman@47108
   205
    (@{thms add_numeral_left} @
huffman@47108
   206
     @{thms add_neg_numeral_left} @
huffman@47108
   207
     @{thms numeral_plus_numeral} @
huffman@47108
   208
     @{thms add_neg_numeral_simps}) simps;
wenzelm@23164
   209
haftmann@31068
   210
(*To evaluate binary negations of coefficients*)
haftmann@54489
   211
val minus_simps = [@{thm minus_zero}, @{thm minus_minus}];
haftmann@31068
   212
haftmann@31068
   213
(*To let us treat subtraction as addition*)
haftmann@54230
   214
val diff_simps = [@{thm diff_conv_add_uminus}, @{thm minus_add_distrib}, @{thm minus_minus}];
haftmann@31068
   215
haftmann@31068
   216
(*To let us treat division as multiplication*)
haftmann@31068
   217
val divide_simps = [@{thm divide_inverse}, @{thm inverse_mult_distrib}, @{thm inverse_inverse_eq}];
haftmann@31068
   218
haftmann@31068
   219
(*to extract again any uncancelled minuses*)
haftmann@31068
   220
val minus_from_mult_simps =
haftmann@31068
   221
    [@{thm minus_minus}, @{thm mult_minus_left}, @{thm mult_minus_right}];
haftmann@31068
   222
haftmann@31068
   223
(*combine unary minus with numeric literals, however nested within a product*)
haftmann@31068
   224
val mult_minus_simps =
lp15@59757
   225
    [@{thm mult.assoc}, @{thm minus_mult_right}, @{thm minus_mult_commute}, @{thm numeral_times_minus_swap}];
haftmann@31068
   226
wenzelm@51717
   227
val norm_ss1 =
wenzelm@51717
   228
  simpset_of (put_simpset num_ss @{context}
wenzelm@51717
   229
    addsimps numeral_syms @ add_0s @ mult_1s @
haftmann@57514
   230
    diff_simps @ minus_simps @ @{thms ac_simps})
wenzelm@51717
   231
wenzelm@51717
   232
val norm_ss2 =
wenzelm@51717
   233
  simpset_of (put_simpset num_ss @{context}
wenzelm@51717
   234
    addsimps non_add_simps @ mult_minus_simps)
wenzelm@51717
   235
wenzelm@51717
   236
val norm_ss3 =
wenzelm@51717
   237
  simpset_of (put_simpset num_ss @{context}
haftmann@57514
   238
    addsimps minus_from_mult_simps @ @{thms ac_simps} @ @{thms ac_simps minus_mult_commute})
haftmann@31068
   239
haftmann@31068
   240
structure CancelNumeralsCommon =
haftmann@44945
   241
struct
haftmann@44945
   242
  val mk_sum = mk_sum
haftmann@44945
   243
  val dest_sum = dest_sum
haftmann@44945
   244
  val mk_coeff = mk_coeff
haftmann@44945
   245
  val dest_coeff = dest_coeff 1
haftmann@44945
   246
  val find_first_coeff = find_first_coeff []
haftmann@44947
   247
  val trans_tac = trans_tac
haftmann@31068
   248
wenzelm@51717
   249
  fun norm_tac ctxt =
wenzelm@51717
   250
    ALLGOALS (simp_tac (put_simpset norm_ss1 ctxt))
wenzelm@51717
   251
    THEN ALLGOALS (simp_tac (put_simpset norm_ss2 ctxt))
wenzelm@51717
   252
    THEN ALLGOALS (simp_tac (put_simpset norm_ss3 ctxt))
haftmann@31068
   253
wenzelm@51717
   254
  val numeral_simp_ss =
wenzelm@51717
   255
    simpset_of (put_simpset HOL_basic_ss @{context} addsimps add_0s @ simps)
wenzelm@51717
   256
  fun numeral_simp_tac ctxt =
wenzelm@51717
   257
    ALLGOALS (simp_tac (put_simpset numeral_simp_ss ctxt))
huffman@45437
   258
  val simplify_meta_eq = Arith_Data.simplify_meta_eq post_simps
haftmann@44945
   259
  val prove_conv = Arith_Data.prove_conv
haftmann@44945
   260
end;
haftmann@31068
   261
haftmann@31068
   262
structure EqCancelNumerals = CancelNumeralsFun
haftmann@31068
   263
 (open CancelNumeralsCommon
haftmann@31068
   264
  val mk_bal   = HOLogic.mk_eq
wenzelm@49323
   265
  val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} dummyT
haftmann@31068
   266
  val bal_add1 = @{thm eq_add_iff1} RS trans
haftmann@31068
   267
  val bal_add2 = @{thm eq_add_iff2} RS trans
haftmann@31068
   268
);
haftmann@31068
   269
haftmann@31068
   270
structure LessCancelNumerals = CancelNumeralsFun
haftmann@31068
   271
 (open CancelNumeralsCommon
haftmann@35092
   272
  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
wenzelm@49323
   273
  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} dummyT
haftmann@31068
   274
  val bal_add1 = @{thm less_add_iff1} RS trans
haftmann@31068
   275
  val bal_add2 = @{thm less_add_iff2} RS trans
haftmann@31068
   276
);
haftmann@31068
   277
haftmann@31068
   278
structure LeCancelNumerals = CancelNumeralsFun
haftmann@31068
   279
 (open CancelNumeralsCommon
haftmann@35092
   280
  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
wenzelm@49323
   281
  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} dummyT
haftmann@31068
   282
  val bal_add1 = @{thm le_add_iff1} RS trans
haftmann@31068
   283
  val bal_add2 = @{thm le_add_iff2} RS trans
haftmann@31068
   284
);
haftmann@31068
   285
wenzelm@61144
   286
val eq_cancel_numerals = EqCancelNumerals.proc
wenzelm@61144
   287
val less_cancel_numerals = LessCancelNumerals.proc
wenzelm@61144
   288
val le_cancel_numerals = LeCancelNumerals.proc
haftmann@31068
   289
haftmann@31068
   290
structure CombineNumeralsData =
haftmann@44945
   291
struct
haftmann@44945
   292
  type coeff = int
haftmann@44945
   293
  val iszero = (fn x => x = 0)
haftmann@44945
   294
  val add  = op +
haftmann@44945
   295
  val mk_sum = long_mk_sum    (*to work for e.g. 2*x + 3*x *)
haftmann@44945
   296
  val dest_sum = dest_sum
haftmann@44945
   297
  val mk_coeff = mk_coeff
haftmann@44945
   298
  val dest_coeff = dest_coeff 1
haftmann@44945
   299
  val left_distrib = @{thm combine_common_factor} RS trans
haftmann@44945
   300
  val prove_conv = Arith_Data.prove_conv_nohyps
haftmann@44947
   301
  val trans_tac = trans_tac
haftmann@31068
   302
wenzelm@51717
   303
  fun norm_tac ctxt =
wenzelm@51717
   304
    ALLGOALS (simp_tac (put_simpset norm_ss1 ctxt))
wenzelm@51717
   305
    THEN ALLGOALS (simp_tac (put_simpset norm_ss2 ctxt))
wenzelm@51717
   306
    THEN ALLGOALS (simp_tac (put_simpset norm_ss3 ctxt))
haftmann@31068
   307
wenzelm@51717
   308
  val numeral_simp_ss =
wenzelm@51717
   309
    simpset_of (put_simpset HOL_basic_ss @{context} addsimps add_0s @ simps)
wenzelm@51717
   310
  fun numeral_simp_tac ctxt =
wenzelm@51717
   311
    ALLGOALS (simp_tac (put_simpset numeral_simp_ss ctxt))
huffman@45437
   312
  val simplify_meta_eq = Arith_Data.simplify_meta_eq post_simps
haftmann@44945
   313
end;
haftmann@31068
   314
haftmann@31068
   315
structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
haftmann@31068
   316
haftmann@31068
   317
(*Version for fields, where coefficients can be fractions*)
haftmann@31068
   318
structure FieldCombineNumeralsData =
haftmann@44945
   319
struct
haftmann@44945
   320
  type coeff = int * int
haftmann@54489
   321
  val iszero = (fn (p, _) => p = 0)
haftmann@44945
   322
  val add = add_frac
haftmann@44945
   323
  val mk_sum = long_mk_sum
haftmann@44945
   324
  val dest_sum = dest_sum
haftmann@44945
   325
  val mk_coeff = mk_fcoeff
haftmann@44945
   326
  val dest_coeff = dest_fcoeff 1
haftmann@44945
   327
  val left_distrib = @{thm combine_common_factor} RS trans
haftmann@44945
   328
  val prove_conv = Arith_Data.prove_conv_nohyps
haftmann@44947
   329
  val trans_tac = trans_tac
haftmann@31068
   330
wenzelm@51717
   331
  val norm_ss1a =
wenzelm@51717
   332
    simpset_of (put_simpset norm_ss1 @{context} addsimps inverse_1s @ divide_simps)
wenzelm@51717
   333
  fun norm_tac ctxt =
wenzelm@51717
   334
    ALLGOALS (simp_tac (put_simpset norm_ss1a ctxt))
wenzelm@51717
   335
    THEN ALLGOALS (simp_tac (put_simpset norm_ss2 ctxt))
wenzelm@51717
   336
    THEN ALLGOALS (simp_tac (put_simpset norm_ss3 ctxt))
haftmann@31068
   337
wenzelm@51717
   338
  val numeral_simp_ss =
wenzelm@51717
   339
    simpset_of (put_simpset HOL_basic_ss @{context}
wenzelm@51717
   340
      addsimps add_0s @ simps @ [@{thm add_frac_eq}, @{thm not_False_eq_True}])
wenzelm@51717
   341
  fun numeral_simp_tac ctxt =
wenzelm@51717
   342
    ALLGOALS (simp_tac (put_simpset numeral_simp_ss ctxt))
huffman@45437
   343
  val simplify_meta_eq = Arith_Data.simplify_meta_eq field_post_simps
haftmann@44945
   344
end;
haftmann@31068
   345
haftmann@31068
   346
structure FieldCombineNumerals = CombineNumeralsFun(FieldCombineNumeralsData);
haftmann@31068
   347
wenzelm@61144
   348
val combine_numerals = CombineNumerals.proc
haftmann@31068
   349
wenzelm@61144
   350
val field_combine_numerals = FieldCombineNumerals.proc
wenzelm@51717
   351
haftmann@31068
   352
haftmann@31068
   353
(** Constant folding for multiplication in semirings **)
haftmann@31068
   354
haftmann@31068
   355
(*We do not need folding for addition: combine_numerals does the same thing*)
haftmann@31068
   356
haftmann@31068
   357
structure Semiring_Times_Assoc_Data : ASSOC_FOLD_DATA =
haftmann@31068
   358
struct
haftmann@57514
   359
  val assoc_ss = simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms ac_simps minus_mult_commute})
haftmann@31068
   360
  val eq_reflection = eq_reflection
boehmes@35983
   361
  val is_numeral = can HOLogic.dest_number
haftmann@31068
   362
end;
haftmann@31068
   363
haftmann@31068
   364
structure Semiring_Times_Assoc = Assoc_Fold (Semiring_Times_Assoc_Data);
haftmann@31068
   365
wenzelm@59582
   366
fun assoc_fold ctxt ct = Semiring_Times_Assoc.proc ctxt (Thm.term_of ct)
wenzelm@23164
   367
wenzelm@23164
   368
structure CancelNumeralFactorCommon =
haftmann@44945
   369
struct
haftmann@44945
   370
  val mk_coeff = mk_coeff
haftmann@44945
   371
  val dest_coeff = dest_coeff 1
haftmann@44947
   372
  val trans_tac = trans_tac
wenzelm@23164
   373
wenzelm@51717
   374
  val norm_ss1 =
wenzelm@51717
   375
    simpset_of (put_simpset HOL_basic_ss @{context} addsimps minus_from_mult_simps @ mult_1s)
wenzelm@51717
   376
  val norm_ss2 =
wenzelm@51717
   377
    simpset_of (put_simpset HOL_basic_ss @{context} addsimps simps @ mult_minus_simps)
wenzelm@51717
   378
  val norm_ss3 =
lp15@59757
   379
    simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms ac_simps minus_mult_commute numeral_times_minus_swap})
wenzelm@51717
   380
  fun norm_tac ctxt =
wenzelm@51717
   381
    ALLGOALS (simp_tac (put_simpset norm_ss1 ctxt))
wenzelm@51717
   382
    THEN ALLGOALS (simp_tac (put_simpset norm_ss2 ctxt))
wenzelm@51717
   383
    THEN ALLGOALS (simp_tac (put_simpset norm_ss3 ctxt))
wenzelm@23164
   384
huffman@45668
   385
  (* simp_thms are necessary because some of the cancellation rules below
huffman@45668
   386
  (e.g. mult_less_cancel_left) introduce various logical connectives *)
wenzelm@51717
   387
  val numeral_simp_ss =
wenzelm@51717
   388
    simpset_of (put_simpset HOL_basic_ss @{context} addsimps simps @ @{thms simp_thms})
wenzelm@51717
   389
  fun numeral_simp_tac ctxt =
wenzelm@51717
   390
    ALLGOALS (simp_tac (put_simpset numeral_simp_ss ctxt))
haftmann@30518
   391
  val simplify_meta_eq = Arith_Data.simplify_meta_eq
huffman@45437
   392
    ([@{thm Nat.add_0}, @{thm Nat.add_0_right}] @ post_simps)
haftmann@44945
   393
  val prove_conv = Arith_Data.prove_conv
haftmann@44945
   394
end
wenzelm@23164
   395
haftmann@30931
   396
(*Version for semiring_div*)
haftmann@30931
   397
structure DivCancelNumeralFactor = CancelNumeralFactorFun
wenzelm@23164
   398
 (open CancelNumeralFactorCommon
haftmann@60352
   399
  val mk_bal   = HOLogic.mk_binop @{const_name Rings.divide}
haftmann@60352
   400
  val dest_bal = HOLogic.dest_bin @{const_name Rings.divide} dummyT
haftmann@30931
   401
  val cancel = @{thm div_mult_mult1} RS trans
wenzelm@23164
   402
  val neg_exchanges = false
wenzelm@23164
   403
)
wenzelm@23164
   404
wenzelm@23164
   405
(*Version for fields*)
wenzelm@23164
   406
structure DivideCancelNumeralFactor = CancelNumeralFactorFun
wenzelm@23164
   407
 (open CancelNumeralFactorCommon
haftmann@60352
   408
  val mk_bal   = HOLogic.mk_binop @{const_name Rings.divide}
haftmann@60352
   409
  val dest_bal = HOLogic.dest_bin @{const_name Rings.divide} dummyT
nipkow@23413
   410
  val cancel = @{thm mult_divide_mult_cancel_left} RS trans
wenzelm@23164
   411
  val neg_exchanges = false
wenzelm@23164
   412
)
wenzelm@23164
   413
wenzelm@23164
   414
structure EqCancelNumeralFactor = CancelNumeralFactorFun
wenzelm@23164
   415
 (open CancelNumeralFactorCommon
wenzelm@23164
   416
  val mk_bal   = HOLogic.mk_eq
wenzelm@49323
   417
  val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} dummyT
wenzelm@23164
   418
  val cancel = @{thm mult_cancel_left} RS trans
wenzelm@23164
   419
  val neg_exchanges = false
wenzelm@23164
   420
)
wenzelm@23164
   421
wenzelm@23164
   422
structure LessCancelNumeralFactor = CancelNumeralFactorFun
wenzelm@23164
   423
 (open CancelNumeralFactorCommon
haftmann@35092
   424
  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
wenzelm@49323
   425
  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} dummyT
wenzelm@23164
   426
  val cancel = @{thm mult_less_cancel_left} RS trans
wenzelm@23164
   427
  val neg_exchanges = true
wenzelm@23164
   428
)
wenzelm@23164
   429
wenzelm@23164
   430
structure LeCancelNumeralFactor = CancelNumeralFactorFun
wenzelm@61144
   431
(
wenzelm@61144
   432
  open CancelNumeralFactorCommon
wenzelm@61144
   433
  val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq}
wenzelm@49323
   434
  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} dummyT
wenzelm@23164
   435
  val cancel = @{thm mult_le_cancel_left} RS trans
wenzelm@23164
   436
  val neg_exchanges = true
wenzelm@23164
   437
)
wenzelm@23164
   438
wenzelm@61144
   439
val eq_cancel_numeral_factor = EqCancelNumeralFactor.proc
wenzelm@61144
   440
val less_cancel_numeral_factor = LessCancelNumeralFactor.proc
wenzelm@61144
   441
val le_cancel_numeral_factor = LeCancelNumeralFactor.proc
wenzelm@61144
   442
val div_cancel_numeral_factor = DivCancelNumeralFactor.proc
wenzelm@61144
   443
val divide_cancel_numeral_factor = DivideCancelNumeralFactor.proc
wenzelm@23164
   444
nipkow@57136
   445
val field_divide_cancel_numeral_factor =
wenzelm@61144
   446
  Simplifier.make_simproc @{context} "field_divide_cancel_numeral_factor"
wenzelm@61144
   447
   {lhss =
wenzelm@61144
   448
     [@{term "((l::'a::field) * m) / n"},
wenzelm@61144
   449
      @{term "(l::'a::field) / (m * n)"},
wenzelm@61144
   450
      @{term "((numeral v)::'a::field) / (numeral w)"},
wenzelm@61144
   451
      @{term "((numeral v)::'a::field) / (- numeral w)"},
wenzelm@61144
   452
      @{term "((- numeral v)::'a::field) / (numeral w)"},
wenzelm@61144
   453
      @{term "((- numeral v)::'a::field) / (- numeral w)"}],
wenzelm@62913
   454
    proc = K DivideCancelNumeralFactor.proc}
nipkow@57136
   455
nipkow@57136
   456
val field_cancel_numeral_factors =
wenzelm@61144
   457
  [Simplifier.make_simproc @{context} "field_eq_cancel_numeral_factor"
wenzelm@61144
   458
    {lhss =
wenzelm@61144
   459
       [@{term "(l::'a::field) * m = n"},
wenzelm@61144
   460
        @{term "(l::'a::field) = m * n"}],
wenzelm@62913
   461
      proc = K EqCancelNumeralFactor.proc},
wenzelm@61144
   462
   field_divide_cancel_numeral_factor]
wenzelm@23164
   463
wenzelm@23164
   464
wenzelm@23164
   465
(** Declarations for ExtractCommonTerm **)
wenzelm@23164
   466
wenzelm@23164
   467
(*Find first term that matches u*)
wenzelm@23164
   468
fun find_first_t past u []         = raise TERM ("find_first_t", [])
wenzelm@23164
   469
  | find_first_t past u (t::terms) =
wenzelm@23164
   470
        if u aconv t then (rev past @ terms)
wenzelm@23164
   471
        else find_first_t (t::past) u terms
wenzelm@23164
   472
        handle TERM _ => find_first_t (t::past) u terms;
wenzelm@23164
   473
wenzelm@23164
   474
(** Final simplification for the CancelFactor simprocs **)
wenzelm@61144
   475
val simplify_one = Arith_Data.simplify_meta_eq
lp15@61694
   476
  [@{thm mult_1_left}, @{thm mult_1_right}, @{thm div_by_1}, @{thm numeral_One}];
wenzelm@23164
   477
wenzelm@51717
   478
fun cancel_simplify_meta_eq ctxt cancel_th th =
wenzelm@51717
   479
    simplify_one ctxt (([th, cancel_th]) MRS trans);
wenzelm@23164
   480
nipkow@30649
   481
local
wenzelm@59642
   482
  val Tp_Eq = Thm.reflexive (Thm.cterm_of @{theory_context HOL} HOLogic.Trueprop)
wenzelm@61144
   483
  fun Eq_True_elim Eq =
nipkow@30649
   484
    Thm.equal_elim (Thm.combination Tp_Eq (Thm.symmetric Eq)) @{thm TrueI}
nipkow@30649
   485
in
wenzelm@51717
   486
fun sign_conv pos_th neg_th ctxt t =
nipkow@30649
   487
  let val T = fastype_of t;
haftmann@35267
   488
      val zero = Const(@{const_name Groups.zero}, T);
haftmann@35092
   489
      val less = Const(@{const_name Orderings.less}, [T,T] ---> HOLogic.boolT);
nipkow@30649
   490
      val pos = less $ zero $ t and neg = less $ t $ zero
nipkow@30649
   491
      fun prove p =
wenzelm@59642
   492
        SOME (Eq_True_elim (Simplifier.asm_rewrite ctxt (Thm.cterm_of ctxt p)))
nipkow@30649
   493
        handle THM _ => NONE
nipkow@30649
   494
    in case prove pos of
nipkow@30649
   495
         SOME th => SOME(th RS pos_th)
nipkow@30649
   496
       | NONE => (case prove neg of
nipkow@30649
   497
                    SOME th => SOME(th RS neg_th)
nipkow@30649
   498
                  | NONE => NONE)
nipkow@30649
   499
    end;
nipkow@30649
   500
end
nipkow@30649
   501
wenzelm@23164
   502
structure CancelFactorCommon =
haftmann@44945
   503
struct
haftmann@44945
   504
  val mk_sum = long_mk_prod
haftmann@44945
   505
  val dest_sum = dest_prod
haftmann@44945
   506
  val mk_coeff = mk_coeff
haftmann@44945
   507
  val dest_coeff = dest_coeff
haftmann@44945
   508
  val find_first = find_first_t []
haftmann@44947
   509
  val trans_tac = trans_tac
wenzelm@51717
   510
  val norm_ss =
haftmann@57514
   511
    simpset_of (put_simpset HOL_basic_ss @{context} addsimps mult_1s @ @{thms ac_simps minus_mult_commute})
wenzelm@51717
   512
  fun norm_tac ctxt =
wenzelm@51717
   513
    ALLGOALS (simp_tac (put_simpset norm_ss ctxt))
wenzelm@61144
   514
  val simplify_meta_eq  = cancel_simplify_meta_eq
huffman@45270
   515
  fun mk_eq (a, b) = HOLogic.mk_Trueprop (HOLogic.mk_eq (a, b))
haftmann@44945
   516
end;
wenzelm@23164
   517
wenzelm@23164
   518
(*mult_cancel_left requires a ring with no zero divisors.*)
wenzelm@23164
   519
structure EqCancelFactor = ExtractCommonTermFun
wenzelm@23164
   520
 (open CancelFactorCommon
wenzelm@23164
   521
  val mk_bal   = HOLogic.mk_eq
wenzelm@49323
   522
  val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} dummyT
wenzelm@31368
   523
  fun simp_conv _ _ = SOME @{thm mult_cancel_left}
nipkow@30649
   524
);
nipkow@30649
   525
nipkow@30649
   526
(*for ordered rings*)
nipkow@30649
   527
structure LeCancelFactor = ExtractCommonTermFun
nipkow@30649
   528
 (open CancelFactorCommon
haftmann@35092
   529
  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
wenzelm@49323
   530
  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} dummyT
nipkow@30649
   531
  val simp_conv = sign_conv
nipkow@30649
   532
    @{thm mult_le_cancel_left_pos} @{thm mult_le_cancel_left_neg}
nipkow@30649
   533
);
nipkow@30649
   534
nipkow@30649
   535
(*for ordered rings*)
nipkow@30649
   536
structure LessCancelFactor = ExtractCommonTermFun
nipkow@30649
   537
 (open CancelFactorCommon
haftmann@35092
   538
  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
wenzelm@49323
   539
  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} dummyT
nipkow@30649
   540
  val simp_conv = sign_conv
nipkow@30649
   541
    @{thm mult_less_cancel_left_pos} @{thm mult_less_cancel_left_neg}
wenzelm@23164
   542
);
wenzelm@23164
   543
haftmann@30931
   544
(*for semirings with division*)
haftmann@30931
   545
structure DivCancelFactor = ExtractCommonTermFun
wenzelm@23164
   546
 (open CancelFactorCommon
haftmann@60352
   547
  val mk_bal   = HOLogic.mk_binop @{const_name Rings.divide}
haftmann@60352
   548
  val dest_bal = HOLogic.dest_bin @{const_name Rings.divide} dummyT
wenzelm@31368
   549
  fun simp_conv _ _ = SOME @{thm div_mult_mult1_if}
wenzelm@23164
   550
);
wenzelm@23164
   551
haftmann@30931
   552
structure ModCancelFactor = ExtractCommonTermFun
nipkow@24395
   553
 (open CancelFactorCommon
haftmann@63950
   554
  val mk_bal   = HOLogic.mk_binop @{const_name modulo}
haftmann@63950
   555
  val dest_bal = HOLogic.dest_bin @{const_name modulo} dummyT
wenzelm@31368
   556
  fun simp_conv _ _ = SOME @{thm mod_mult_mult1}
nipkow@24395
   557
);
nipkow@24395
   558
haftmann@30931
   559
(*for idoms*)
haftmann@30931
   560
structure DvdCancelFactor = ExtractCommonTermFun
nipkow@23969
   561
 (open CancelFactorCommon
haftmann@35050
   562
  val mk_bal   = HOLogic.mk_binrel @{const_name Rings.dvd}
wenzelm@49323
   563
  val dest_bal = HOLogic.dest_bin @{const_name Rings.dvd} dummyT
wenzelm@31368
   564
  fun simp_conv _ _ = SOME @{thm dvd_mult_cancel_left}
nipkow@23969
   565
);
nipkow@23969
   566
wenzelm@23164
   567
(*Version for all fields, including unordered ones (type complex).*)
wenzelm@23164
   568
structure DivideCancelFactor = ExtractCommonTermFun
wenzelm@23164
   569
 (open CancelFactorCommon
haftmann@60352
   570
  val mk_bal   = HOLogic.mk_binop @{const_name Rings.divide}
haftmann@60352
   571
  val dest_bal = HOLogic.dest_bin @{const_name Rings.divide} dummyT
wenzelm@31368
   572
  fun simp_conv _ _ = SOME @{thm mult_divide_mult_cancel_left_if}
wenzelm@23164
   573
);
wenzelm@23164
   574
wenzelm@59582
   575
fun eq_cancel_factor ctxt ct = EqCancelFactor.proc ctxt (Thm.term_of ct)
wenzelm@59582
   576
fun le_cancel_factor ctxt ct = LeCancelFactor.proc ctxt (Thm.term_of ct)
wenzelm@59582
   577
fun less_cancel_factor ctxt ct = LessCancelFactor.proc ctxt (Thm.term_of ct)
wenzelm@59582
   578
fun div_cancel_factor ctxt ct = DivCancelFactor.proc ctxt (Thm.term_of ct)
wenzelm@59582
   579
fun mod_cancel_factor ctxt ct = ModCancelFactor.proc ctxt (Thm.term_of ct)
wenzelm@59582
   580
fun dvd_cancel_factor ctxt ct = DvdCancelFactor.proc ctxt (Thm.term_of ct)
wenzelm@59582
   581
fun divide_cancel_factor ctxt ct = DivideCancelFactor.proc ctxt (Thm.term_of ct)
wenzelm@23164
   582
haftmann@36751
   583
local
wenzelm@61144
   584
wenzelm@61150
   585
val cterm_of = Thm.cterm_of @{context};
wenzelm@61150
   586
fun tvar S = (("'a", 0), S);
wenzelm@61150
   587
wenzelm@61150
   588
val zero_tvar = tvar @{sort zero};
wenzelm@61150
   589
val zero = cterm_of (Const (@{const_name zero_class.zero}, TVar zero_tvar));
wenzelm@61150
   590
wenzelm@61150
   591
val type_tvar = tvar @{sort type};
wenzelm@61150
   592
val geq = cterm_of (Const (@{const_name HOL.eq}, TVar type_tvar --> TVar type_tvar --> @{typ bool}));
wenzelm@61150
   593
wenzelm@61144
   594
val add_frac_eq = mk_meta_eq @{thm "add_frac_eq"}
wenzelm@61144
   595
val add_frac_num = mk_meta_eq @{thm "add_frac_num"}
wenzelm@61144
   596
val add_num_frac = mk_meta_eq @{thm "add_num_frac"}
haftmann@36751
   597
wenzelm@61144
   598
fun prove_nz ctxt T t =
wenzelm@61144
   599
  let
wenzelm@61150
   600
    val z = Thm.instantiate_cterm ([(zero_tvar, T)], []) zero
wenzelm@61150
   601
    val eq = Thm.instantiate_cterm ([(type_tvar, T)], []) geq
wenzelm@61150
   602
    val th =
wenzelm@61150
   603
      Simplifier.rewrite (ctxt addsimps @{thms simp_thms})
wenzelm@61150
   604
        (Thm.apply @{cterm "Trueprop"} (Thm.apply @{cterm "Not"}
wenzelm@61150
   605
          (Thm.apply (Thm.apply eq t) z)))
wenzelm@61150
   606
  in Thm.equal_elim (Thm.symmetric th) TrueI end
haftmann@36751
   607
wenzelm@61144
   608
fun proc ctxt ct =
haftmann@36751
   609
  let
haftmann@36751
   610
    val ((x,y),(w,z)) =
haftmann@36751
   611
         (Thm.dest_binop #> (fn (a,b) => (Thm.dest_binop a, Thm.dest_binop b))) ct
wenzelm@59582
   612
    val _ = map (HOLogic.dest_number o Thm.term_of) [x,y,z,w]
wenzelm@59586
   613
    val T = Thm.ctyp_of_cterm x
wenzelm@51717
   614
    val [y_nz, z_nz] = map (prove_nz ctxt T) [y, z]
wenzelm@60801
   615
    val th = Thm.instantiate' [SOME T] (map SOME [y,z,x,w]) add_frac_eq
wenzelm@61144
   616
  in SOME (Thm.implies_elim (Thm.implies_elim th y_nz) z_nz) end
haftmann@36751
   617
  handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE
haftmann@36751
   618
wenzelm@61144
   619
fun proc2 ctxt ct =
haftmann@36751
   620
  let
haftmann@36751
   621
    val (l,r) = Thm.dest_binop ct
wenzelm@59586
   622
    val T = Thm.ctyp_of_cterm l
wenzelm@59582
   623
  in (case (Thm.term_of l, Thm.term_of r) of
haftmann@60352
   624
      (Const(@{const_name Rings.divide},_)$_$_, _) =>
haftmann@36751
   625
        let val (x,y) = Thm.dest_binop l val z = r
wenzelm@59582
   626
            val _ = map (HOLogic.dest_number o Thm.term_of) [x,y,z]
wenzelm@51717
   627
            val ynz = prove_nz ctxt T y
wenzelm@60801
   628
        in SOME (Thm.implies_elim (Thm.instantiate' [SOME T] (map SOME [y,x,z]) add_frac_num) ynz)
haftmann@36751
   629
        end
haftmann@60352
   630
     | (_, Const (@{const_name Rings.divide},_)$_$_) =>
haftmann@36751
   631
        let val (x,y) = Thm.dest_binop r val z = l
wenzelm@59582
   632
            val _ = map (HOLogic.dest_number o Thm.term_of) [x,y,z]
wenzelm@51717
   633
            val ynz = prove_nz ctxt T y
wenzelm@60801
   634
        in SOME (Thm.implies_elim (Thm.instantiate' [SOME T] (map SOME [y,z,x]) add_num_frac) ynz)
haftmann@36751
   635
        end
haftmann@36751
   636
     | _ => NONE)
haftmann@36751
   637
  end
haftmann@36751
   638
  handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE
haftmann@36751
   639
wenzelm@61144
   640
fun is_number (Const(@{const_name Rings.divide},_)$a$b) = is_number a andalso is_number b
wenzelm@61144
   641
  | is_number t = can HOLogic.dest_number t
haftmann@36751
   642
wenzelm@61144
   643
val is_number = is_number o Thm.term_of
haftmann@36751
   644
wenzelm@61144
   645
fun proc3 ctxt ct =
wenzelm@59582
   646
  (case Thm.term_of ct of
haftmann@60352
   647
    Const(@{const_name Orderings.less},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
haftmann@36751
   648
      let
haftmann@36751
   649
        val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
haftmann@36751
   650
        val _ = map is_number [a,b,c]
wenzelm@59586
   651
        val T = Thm.ctyp_of_cterm c
wenzelm@60801
   652
        val th = Thm.instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_less_eq"}
haftmann@36751
   653
      in SOME (mk_meta_eq th) end
haftmann@60352
   654
  | Const(@{const_name Orderings.less_eq},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
haftmann@36751
   655
      let
haftmann@36751
   656
        val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
haftmann@36751
   657
        val _ = map is_number [a,b,c]
wenzelm@59586
   658
        val T = Thm.ctyp_of_cterm c
wenzelm@60801
   659
        val th = Thm.instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_le_eq"}
haftmann@36751
   660
      in SOME (mk_meta_eq th) end
haftmann@60352
   661
  | Const(@{const_name HOL.eq},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
haftmann@36751
   662
      let
haftmann@36751
   663
        val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
haftmann@36751
   664
        val _ = map is_number [a,b,c]
wenzelm@59586
   665
        val T = Thm.ctyp_of_cterm c
wenzelm@60801
   666
        val th = Thm.instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_eq_eq"}
haftmann@36751
   667
      in SOME (mk_meta_eq th) end
haftmann@60352
   668
  | Const(@{const_name Orderings.less},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
haftmann@36751
   669
    let
haftmann@36751
   670
      val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
haftmann@36751
   671
        val _ = map is_number [a,b,c]
wenzelm@59586
   672
        val T = Thm.ctyp_of_cterm c
wenzelm@60801
   673
        val th = Thm.instantiate' [SOME T] (map SOME [a,b,c]) @{thm "less_divide_eq"}
haftmann@36751
   674
      in SOME (mk_meta_eq th) end
haftmann@60352
   675
  | Const(@{const_name Orderings.less_eq},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
haftmann@36751
   676
    let
haftmann@36751
   677
      val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
haftmann@36751
   678
        val _ = map is_number [a,b,c]
wenzelm@59586
   679
        val T = Thm.ctyp_of_cterm c
wenzelm@60801
   680
        val th = Thm.instantiate' [SOME T] (map SOME [a,b,c]) @{thm "le_divide_eq"}
haftmann@36751
   681
      in SOME (mk_meta_eq th) end
haftmann@60352
   682
  | Const(@{const_name HOL.eq},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
haftmann@36751
   683
    let
haftmann@36751
   684
      val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
haftmann@36751
   685
        val _ = map is_number [a,b,c]
wenzelm@59586
   686
        val T = Thm.ctyp_of_cterm c
wenzelm@60801
   687
        val th = Thm.instantiate' [SOME T] (map SOME [a,b,c]) @{thm "eq_divide_eq"}
haftmann@36751
   688
      in SOME (mk_meta_eq th) end
wenzelm@61144
   689
  | _ => NONE) handle TERM _ => NONE | CTERM _ => NONE | THM _ => NONE
haftmann@36751
   690
haftmann@36751
   691
val add_frac_frac_simproc =
wenzelm@61144
   692
  Simplifier.make_simproc @{context} "add_frac_frac_simproc"
wenzelm@61144
   693
   {lhss = [@{term "(x::'a::field) / y + (w::'a::field) / z"}],
wenzelm@62913
   694
    proc = K proc}
haftmann@36751
   695
haftmann@36751
   696
val add_frac_num_simproc =
wenzelm@61144
   697
  Simplifier.make_simproc @{context} "add_frac_num_simproc"
wenzelm@61144
   698
   {lhss = [@{term "(x::'a::field) / y + z"}, @{term "z + (x::'a::field) / y"}],
wenzelm@62913
   699
    proc = K proc2}
haftmann@36751
   700
haftmann@36751
   701
val ord_frac_simproc =
wenzelm@61144
   702
  Simplifier.make_simproc @{context} "ord_frac_simproc"
wenzelm@61144
   703
   {lhss =
wenzelm@61144
   704
     [@{term "(a::'a::{field,ord}) / b < c"},
wenzelm@61144
   705
      @{term "(a::'a::{field,ord}) / b \<le> c"},
wenzelm@61144
   706
      @{term "c < (a::'a::{field,ord}) / b"},
wenzelm@61144
   707
      @{term "c \<le> (a::'a::{field,ord}) / b"},
wenzelm@61144
   708
      @{term "c = (a::'a::{field,ord}) / b"},
wenzelm@61144
   709
      @{term "(a::'a::{field, ord}) / b = c"}],
wenzelm@62913
   710
    proc = K proc3}
haftmann@36751
   711
wenzelm@61144
   712
val ths =
wenzelm@61144
   713
 [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"},
wenzelm@61144
   714
  @{thm "divide_numeral_1"},
haftmann@64240
   715
  @{thm "div_by_0"}, @{thm div_0},
wenzelm@61144
   716
  @{thm "divide_divide_eq_left"},
wenzelm@61144
   717
  @{thm "times_divide_eq_left"}, @{thm "times_divide_eq_right"},
wenzelm@61144
   718
  @{thm "times_divide_times_eq"},
wenzelm@61144
   719
  @{thm "divide_divide_eq_right"},
wenzelm@61144
   720
  @{thm diff_conv_add_uminus}, @{thm "minus_divide_left"},
wenzelm@61144
   721
  @{thm "add_divide_distrib"} RS sym,
wenzelm@61144
   722
  @{thm Fields.field_divide_inverse} RS sym, @{thm inverse_divide},
wenzelm@61144
   723
  Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv (Conv.rewr_conv (mk_meta_eq @{thm mult.commute}))))
wenzelm@61144
   724
  (@{thm Fields.field_divide_inverse} RS sym)]
haftmann@36751
   725
wenzelm@51717
   726
val field_comp_ss =
wenzelm@51717
   727
  simpset_of
wenzelm@51717
   728
    (put_simpset HOL_basic_ss @{context}
wenzelm@51717
   729
      addsimps @{thms "semiring_norm"}
wenzelm@45620
   730
      addsimps ths addsimps @{thms simp_thms}
wenzelm@45620
   731
      addsimprocs field_cancel_numeral_factors
wenzelm@45620
   732
      addsimprocs [add_frac_frac_simproc, add_frac_num_simproc, ord_frac_simproc]
wenzelm@45620
   733
      |> Simplifier.add_cong @{thm "if_weak_cong"})
wenzelm@51717
   734
wenzelm@51717
   735
in
wenzelm@51717
   736
wenzelm@51717
   737
fun field_comp_conv ctxt =
wenzelm@51717
   738
  Simplifier.rewrite (put_simpset field_comp_ss ctxt)
wenzelm@45620
   739
  then_conv
lp15@61694
   740
  Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps [@{thm numeral_One}])
haftmann@36751
   741
haftmann@36751
   742
end
haftmann@36751
   743
wenzelm@23164
   744
end;