src/HOL/Tools/numeral_simprocs.ML
author wenzelm
Wed, 23 Nov 2011 22:59:39 +0100
changeset 45620 f2a587696afb
parent 45437 958d19d3405b
child 45625 750c5a47400b
permissions -rw-r--r--
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
31068
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
     1
(* Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
     2
   Copyright   2000  University of Cambridge
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
     3
36751
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
     4
Simprocs for the (integer) numerals.
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
     5
*)
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
     6
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
     7
(*To quote from Provers/Arith/cancel_numeral_factor.ML:
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
     8
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
     9
Cancels common coefficients in balanced expressions:
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    10
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    11
     u*#m ~~ u'*#m'  ==  #n*u ~~ #n'*u'
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    12
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    13
where ~~ is an appropriate balancing operation (e.g. =, <=, <, div, /)
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    14
and d = gcd(m,m') and n=m/d and n'=m'/d.
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    15
*)
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    16
31068
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
    17
signature NUMERAL_SIMPROCS =
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
    18
sig
44945
haftmann
parents: 44064
diff changeset
    19
  val prep_simproc: theory -> string * string list * (theory -> simpset -> term -> thm option)
haftmann
parents: 44064
diff changeset
    20
    -> simproc
haftmann
parents: 44064
diff changeset
    21
  val trans_tac: thm option -> tactic
45284
ae78a4ffa81d use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents: 45270
diff changeset
    22
  val assoc_fold: simpset -> cterm -> thm option
ae78a4ffa81d use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents: 45270
diff changeset
    23
  val combine_numerals: simpset -> cterm -> thm option
ae78a4ffa81d use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents: 45270
diff changeset
    24
  val eq_cancel_numerals: simpset -> cterm -> thm option
ae78a4ffa81d use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents: 45270
diff changeset
    25
  val less_cancel_numerals: simpset -> cterm -> thm option
ae78a4ffa81d use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents: 45270
diff changeset
    26
  val le_cancel_numerals: simpset -> cterm -> thm option
ae78a4ffa81d use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents: 45270
diff changeset
    27
  val eq_cancel_factor: simpset -> cterm -> thm option
ae78a4ffa81d use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents: 45270
diff changeset
    28
  val le_cancel_factor: simpset -> cterm -> thm option
ae78a4ffa81d use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents: 45270
diff changeset
    29
  val less_cancel_factor: simpset -> cterm -> thm option
ae78a4ffa81d use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents: 45270
diff changeset
    30
  val div_cancel_factor: simpset -> cterm -> thm option
ae78a4ffa81d use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents: 45270
diff changeset
    31
  val mod_cancel_factor: simpset -> cterm -> thm option
ae78a4ffa81d use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents: 45270
diff changeset
    32
  val dvd_cancel_factor: simpset -> cterm -> thm option
ae78a4ffa81d use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents: 45270
diff changeset
    33
  val divide_cancel_factor: simpset -> cterm -> thm option
ae78a4ffa81d use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents: 45270
diff changeset
    34
  val eq_cancel_numeral_factor: simpset -> cterm -> thm option
ae78a4ffa81d use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents: 45270
diff changeset
    35
  val less_cancel_numeral_factor: simpset -> cterm -> thm option
ae78a4ffa81d use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents: 45270
diff changeset
    36
  val le_cancel_numeral_factor: simpset -> cterm -> thm option
ae78a4ffa81d use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents: 45270
diff changeset
    37
  val div_cancel_numeral_factor: simpset -> cterm -> thm option
ae78a4ffa81d use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents: 45270
diff changeset
    38
  val divide_cancel_numeral_factor: simpset -> cterm -> thm option
ae78a4ffa81d use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents: 45270
diff changeset
    39
  val field_combine_numerals: simpset -> cterm -> thm option
31068
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
    40
  val field_cancel_numeral_factors: simproc list
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
    41
  val num_ss: simpset
36751
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
    42
  val field_comp_conv: conv
31068
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
    43
end;
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
    44
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
    45
structure Numeral_Simprocs : NUMERAL_SIMPROCS =
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
    46
struct
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
    47
44945
haftmann
parents: 44064
diff changeset
    48
fun prep_simproc thy (name, pats, proc) =
haftmann
parents: 44064
diff changeset
    49
  Simplifier.simproc_global thy name pats proc;
haftmann
parents: 44064
diff changeset
    50
haftmann
parents: 44064
diff changeset
    51
fun trans_tac NONE  = all_tac
haftmann
parents: 44064
diff changeset
    52
  | trans_tac (SOME th) = ALLGOALS (rtac (th RS trans));
haftmann
parents: 44064
diff changeset
    53
33359
8b673ae1bf39 dedicated theory for loading numeral simprocs
haftmann
parents: 32957
diff changeset
    54
val mk_number = Arith_Data.mk_number;
8b673ae1bf39 dedicated theory for loading numeral simprocs
haftmann
parents: 32957
diff changeset
    55
val mk_sum = Arith_Data.mk_sum;
8b673ae1bf39 dedicated theory for loading numeral simprocs
haftmann
parents: 32957
diff changeset
    56
val long_mk_sum = Arith_Data.long_mk_sum;
8b673ae1bf39 dedicated theory for loading numeral simprocs
haftmann
parents: 32957
diff changeset
    57
val dest_sum = Arith_Data.dest_sum;
31068
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
    58
35267
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35092
diff changeset
    59
val mk_diff = HOLogic.mk_binop @{const_name Groups.minus};
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35092
diff changeset
    60
val dest_diff = HOLogic.dest_bin @{const_name Groups.minus} Term.dummyT;
31068
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
    61
35267
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35092
diff changeset
    62
val mk_times = HOLogic.mk_binop @{const_name Groups.times};
31068
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
    63
35267
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35092
diff changeset
    64
fun one_of T = Const(@{const_name Groups.one}, T);
31068
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
    65
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
    66
(* build product with trailing 1 rather than Numeral 1 in order to avoid the
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
    67
   unnecessary restriction to type class number_ring
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
    68
   which is not required for cancellation of common factors in divisions.
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
    69
*)
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
    70
fun mk_prod T = 
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
    71
  let val one = one_of T
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
    72
  fun mk [] = one
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
    73
    | mk [t] = t
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
    74
    | mk (t :: ts) = if t = one then mk ts else mk_times (t, mk ts)
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
    75
  in mk end;
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
    76
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
    77
(*This version ALWAYS includes a trailing one*)
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
    78
fun long_mk_prod T []        = one_of T
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
    79
  | long_mk_prod T (t :: ts) = mk_times (t, mk_prod T ts);
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
    80
35267
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35092
diff changeset
    81
val dest_times = HOLogic.dest_bin @{const_name Groups.times} Term.dummyT;
31068
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
    82
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
    83
fun dest_prod t =
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
    84
      let val (t,u) = dest_times t
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
    85
      in dest_prod t @ dest_prod u end
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
    86
      handle TERM _ => [t];
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
    87
33359
8b673ae1bf39 dedicated theory for loading numeral simprocs
haftmann
parents: 32957
diff changeset
    88
fun find_first_numeral past (t::terms) =
8b673ae1bf39 dedicated theory for loading numeral simprocs
haftmann
parents: 32957
diff changeset
    89
        ((snd (HOLogic.dest_number t), rev past @ terms)
8b673ae1bf39 dedicated theory for loading numeral simprocs
haftmann
parents: 32957
diff changeset
    90
         handle TERM _ => find_first_numeral (t::past) terms)
8b673ae1bf39 dedicated theory for loading numeral simprocs
haftmann
parents: 32957
diff changeset
    91
  | find_first_numeral past [] = raise TERM("find_first_numeral", []);
8b673ae1bf39 dedicated theory for loading numeral simprocs
haftmann
parents: 32957
diff changeset
    92
31068
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
    93
(*DON'T do the obvious simplifications; that would create special cases*)
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
    94
fun mk_coeff (k, t) = mk_times (mk_number (Term.fastype_of t) k, t);
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
    95
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
    96
(*Express t as a product of (possibly) a numeral with other sorted terms*)
35267
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35092
diff changeset
    97
fun dest_coeff sign (Const (@{const_name Groups.uminus}, _) $ t) = dest_coeff (~sign) t
31068
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
    98
  | dest_coeff sign t =
35408
b48ab741683b modernized structure Term_Ord;
wenzelm
parents: 35267
diff changeset
    99
    let val ts = sort Term_Ord.term_ord (dest_prod t)
31068
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   100
        val (n, ts') = find_first_numeral [] ts
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   101
                          handle TERM _ => (1, ts)
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   102
    in (sign*n, mk_prod (Term.fastype_of t) ts') end;
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   103
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   104
(*Find first coefficient-term THAT MATCHES u*)
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   105
fun find_first_coeff past u [] = raise TERM("find_first_coeff", [])
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   106
  | find_first_coeff past u (t::terms) =
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   107
        let val (n,u') = dest_coeff 1 t
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   108
        in if u aconv u' then (n, rev past @ terms)
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   109
                         else find_first_coeff (t::past) u terms
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   110
        end
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   111
        handle TERM _ => find_first_coeff (t::past) u terms;
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   112
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   113
(*Fractions as pairs of ints. Can't use Rat.rat because the representation
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   114
  needs to preserve negative values in the denominator.*)
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   115
fun mk_frac (p, q) = if q = 0 then raise Div else (p, q);
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   116
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   117
(*Don't reduce fractions; sums must be proved by rule add_frac_eq.
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   118
  Fractions are reduced later by the cancel_numeral_factor simproc.*)
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   119
fun add_frac ((p1, q1), (p2, q2)) = (p1 * q2 + p2 * q1, q1 * q2);
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   120
44064
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 40878
diff changeset
   121
val mk_divide = HOLogic.mk_binop @{const_name Fields.divide};
31068
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   122
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   123
(*Build term (p / q) * t*)
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   124
fun mk_fcoeff ((p, q), t) =
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   125
  let val T = Term.fastype_of t
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   126
  in mk_times (mk_divide (mk_number T p, mk_number T q), t) end;
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   127
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   128
(*Express t as a product of a fraction with other sorted terms*)
35267
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35092
diff changeset
   129
fun dest_fcoeff sign (Const (@{const_name Groups.uminus}, _) $ t) = dest_fcoeff (~sign) t
44064
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 40878
diff changeset
   130
  | dest_fcoeff sign (Const (@{const_name Fields.divide}, _) $ t $ u) =
31068
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   131
    let val (p, t') = dest_coeff sign t
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   132
        val (q, u') = dest_coeff 1 u
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   133
    in (mk_frac (p, q), mk_divide (t', u')) end
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   134
  | dest_fcoeff sign t =
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   135
    let val (p, t') = dest_coeff sign t
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   136
        val T = Term.fastype_of t
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   137
    in (mk_frac (p, 1), mk_divide (t', one_of T)) end;
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   138
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   139
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   140
(** New term ordering so that AC-rewriting brings numerals to the front **)
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   141
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   142
(*Order integers by absolute value and then by sign. The standard integer
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   143
  ordering is not well-founded.*)
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   144
fun num_ord (i,j) =
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   145
  (case int_ord (abs i, abs j) of
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   146
    EQUAL => int_ord (Int.sign i, Int.sign j) 
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   147
  | ord => ord);
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   148
35408
b48ab741683b modernized structure Term_Ord;
wenzelm
parents: 35267
diff changeset
   149
(*This resembles Term_Ord.term_ord, but it puts binary numerals before other
31068
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   150
  non-atomic terms.*)
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   151
local open Term 
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   152
in 
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   153
fun numterm_ord (Abs (_, T, t), Abs(_, U, u)) =
35408
b48ab741683b modernized structure Term_Ord;
wenzelm
parents: 35267
diff changeset
   154
      (case numterm_ord (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord)
31068
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   155
  | numterm_ord
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   156
     (Const(@{const_name Int.number_of}, _) $ v, Const(@{const_name Int.number_of}, _) $ w) =
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   157
     num_ord (HOLogic.dest_numeral v, HOLogic.dest_numeral w)
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   158
  | numterm_ord (Const(@{const_name Int.number_of}, _) $ _, _) = LESS
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   159
  | numterm_ord (_, Const(@{const_name Int.number_of}, _) $ _) = GREATER
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   160
  | numterm_ord (t, u) =
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   161
      (case int_ord (size_of_term t, size_of_term u) of
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   162
        EQUAL =>
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   163
          let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
35408
b48ab741683b modernized structure Term_Ord;
wenzelm
parents: 35267
diff changeset
   164
            (case Term_Ord.hd_ord (f, g) of EQUAL => numterms_ord (ts, us) | ord => ord)
31068
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   165
          end
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   166
      | ord => ord)
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   167
and numterms_ord (ts, us) = list_ord numterm_ord (ts, us)
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   168
end;
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   169
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   170
fun numtermless tu = (numterm_ord tu = LESS);
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   171
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   172
val num_ss = HOL_ss settermless numtermless;
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   173
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   174
(*Maps 0 to Numeral0 and 1 to Numeral1 so that arithmetic isn't complicated by the abstract 0 and 1.*)
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   175
val numeral_syms = [@{thm numeral_0_eq_0} RS sym, @{thm numeral_1_eq_1} RS sym];
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   176
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   177
(*Simplify Numeral0+n, n+Numeral0, Numeral1*n, n*Numeral1, 1*x, x*1, x/1 *)
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   178
val add_0s =  @{thms add_0s};
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   179
val mult_1s = @{thms mult_1s mult_1_left mult_1_right divide_1};
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   180
45437
958d19d3405b tune post-processing of simproc-generated rules so they won't produce Numeral0 or Numeral1
huffman
parents: 45306
diff changeset
   181
(* For post-simplification of the rhs of simproc-generated rules *)
958d19d3405b tune post-processing of simproc-generated rules so they won't produce Numeral0 or Numeral1
huffman
parents: 45306
diff changeset
   182
val post_simps =
958d19d3405b tune post-processing of simproc-generated rules so they won't produce Numeral0 or Numeral1
huffman
parents: 45306
diff changeset
   183
    [@{thm numeral_0_eq_0}, @{thm numeral_1_eq_1},
958d19d3405b tune post-processing of simproc-generated rules so they won't produce Numeral0 or Numeral1
huffman
parents: 45306
diff changeset
   184
     @{thm add_0_left}, @{thm add_0_right},
958d19d3405b tune post-processing of simproc-generated rules so they won't produce Numeral0 or Numeral1
huffman
parents: 45306
diff changeset
   185
     @{thm mult_zero_left}, @{thm mult_zero_right},
958d19d3405b tune post-processing of simproc-generated rules so they won't produce Numeral0 or Numeral1
huffman
parents: 45306
diff changeset
   186
     @{thm mult_1_left}, @{thm mult_1_right},
958d19d3405b tune post-processing of simproc-generated rules so they won't produce Numeral0 or Numeral1
huffman
parents: 45306
diff changeset
   187
     @{thm mult_minus1}, @{thm mult_minus1_right}]
958d19d3405b tune post-processing of simproc-generated rules so they won't produce Numeral0 or Numeral1
huffman
parents: 45306
diff changeset
   188
958d19d3405b tune post-processing of simproc-generated rules so they won't produce Numeral0 or Numeral1
huffman
parents: 45306
diff changeset
   189
val field_post_simps =
958d19d3405b tune post-processing of simproc-generated rules so they won't produce Numeral0 or Numeral1
huffman
parents: 45306
diff changeset
   190
    post_simps @ [@{thm divide_zero_left}, @{thm divide_1}]
958d19d3405b tune post-processing of simproc-generated rules so they won't produce Numeral0 or Numeral1
huffman
parents: 45306
diff changeset
   191
                      
31068
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   192
(*Simplify inverse Numeral1, a/Numeral1*)
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   193
val inverse_1s = [@{thm inverse_numeral_1}];
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   194
val divide_1s = [@{thm divide_numeral_1}];
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   195
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   196
(*To perform binary arithmetic.  The "left" rewriting handles patterns
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   197
  created by the Numeral_Simprocs, such as 3 * (5 * x). *)
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   198
val simps = [@{thm numeral_0_eq_0} RS sym, @{thm numeral_1_eq_1} RS sym,
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   199
                 @{thm add_number_of_left}, @{thm mult_number_of_left}] @
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   200
                @{thms arith_simps} @ @{thms rel_simps};
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   201
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   202
(*Binary arithmetic BUT NOT ADDITION since it may collapse adjacent terms
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   203
  during re-arrangement*)
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   204
val non_add_simps =
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   205
  subtract Thm.eq_thm [@{thm add_number_of_left}, @{thm number_of_add} RS sym] simps;
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   206
31068
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   207
(*To evaluate binary negations of coefficients*)
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   208
val minus_simps = [@{thm numeral_m1_eq_minus_1} RS sym, @{thm number_of_minus} RS sym] @
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   209
                   @{thms minus_bin_simps} @ @{thms pred_bin_simps};
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   210
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   211
(*To let us treat subtraction as addition*)
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   212
val diff_simps = [@{thm diff_minus}, @{thm minus_add_distrib}, @{thm minus_minus}];
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   213
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   214
(*To let us treat division as multiplication*)
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   215
val divide_simps = [@{thm divide_inverse}, @{thm inverse_mult_distrib}, @{thm inverse_inverse_eq}];
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   216
35020
862a20ffa8e2 prefer explicit @{lemma} over adhoc forward reasoning;
wenzelm
parents: 34974
diff changeset
   217
(*push the unary minus down*)
862a20ffa8e2 prefer explicit @{lemma} over adhoc forward reasoning;
wenzelm
parents: 34974
diff changeset
   218
val minus_mult_eq_1_to_2 = @{lemma "- (a::'a::ring) * b = a * - b" by simp};
31068
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   219
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   220
(*to extract again any uncancelled minuses*)
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   221
val minus_from_mult_simps =
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   222
    [@{thm minus_minus}, @{thm mult_minus_left}, @{thm mult_minus_right}];
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   223
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   224
(*combine unary minus with numeric literals, however nested within a product*)
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   225
val mult_minus_simps =
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   226
    [@{thm mult_assoc}, @{thm minus_mult_left}, minus_mult_eq_1_to_2];
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   227
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   228
val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   229
  diff_simps @ minus_simps @ @{thms add_ac}
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   230
val norm_ss2 = num_ss addsimps non_add_simps @ mult_minus_simps
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   231
val norm_ss3 = num_ss addsimps minus_from_mult_simps @ @{thms add_ac} @ @{thms mult_ac}
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   232
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   233
structure CancelNumeralsCommon =
44945
haftmann
parents: 44064
diff changeset
   234
struct
haftmann
parents: 44064
diff changeset
   235
  val mk_sum = mk_sum
haftmann
parents: 44064
diff changeset
   236
  val dest_sum = dest_sum
haftmann
parents: 44064
diff changeset
   237
  val mk_coeff = mk_coeff
haftmann
parents: 44064
diff changeset
   238
  val dest_coeff = dest_coeff 1
haftmann
parents: 44064
diff changeset
   239
  val find_first_coeff = find_first_coeff []
44947
8ae418dfe561 dropped unused argument – avoids problem with SML/NJ
haftmann
parents: 44945
diff changeset
   240
  val trans_tac = trans_tac
31068
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   241
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   242
  fun norm_tac ss =
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   243
    ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   244
    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   245
    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3))
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   246
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   247
  val numeral_simp_ss = HOL_ss addsimps add_0s @ simps
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   248
  fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
45437
958d19d3405b tune post-processing of simproc-generated rules so they won't produce Numeral0 or Numeral1
huffman
parents: 45306
diff changeset
   249
  val simplify_meta_eq = Arith_Data.simplify_meta_eq post_simps
44945
haftmann
parents: 44064
diff changeset
   250
  val prove_conv = Arith_Data.prove_conv
haftmann
parents: 44064
diff changeset
   251
end;
31068
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   252
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   253
structure EqCancelNumerals = CancelNumeralsFun
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   254
 (open CancelNumeralsCommon
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   255
  val mk_bal   = HOLogic.mk_eq
38864
4abe644fcea5 formerly unnamed infix equality now named HOL.eq
haftmann
parents: 38549
diff changeset
   256
  val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} Term.dummyT
31068
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   257
  val bal_add1 = @{thm eq_add_iff1} RS trans
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   258
  val bal_add2 = @{thm eq_add_iff2} RS trans
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   259
);
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   260
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   261
structure LessCancelNumerals = CancelNumeralsFun
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   262
 (open CancelNumeralsCommon
35092
cfe605c54e50 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents: 35084
diff changeset
   263
  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
cfe605c54e50 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents: 35084
diff changeset
   264
  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} Term.dummyT
31068
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   265
  val bal_add1 = @{thm less_add_iff1} RS trans
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   266
  val bal_add2 = @{thm less_add_iff2} RS trans
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   267
);
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   268
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   269
structure LeCancelNumerals = CancelNumeralsFun
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   270
 (open CancelNumeralsCommon
35092
cfe605c54e50 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents: 35084
diff changeset
   271
  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
cfe605c54e50 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents: 35084
diff changeset
   272
  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} Term.dummyT
31068
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   273
  val bal_add1 = @{thm le_add_iff1} RS trans
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   274
  val bal_add2 = @{thm le_add_iff2} RS trans
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   275
);
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   276
45284
ae78a4ffa81d use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents: 45270
diff changeset
   277
fun eq_cancel_numerals ss ct = EqCancelNumerals.proc ss (term_of ct)
ae78a4ffa81d use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents: 45270
diff changeset
   278
fun less_cancel_numerals ss ct = LessCancelNumerals.proc ss (term_of ct)
ae78a4ffa81d use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents: 45270
diff changeset
   279
fun le_cancel_numerals ss ct = LeCancelNumerals.proc ss (term_of ct)
31068
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   280
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   281
structure CombineNumeralsData =
44945
haftmann
parents: 44064
diff changeset
   282
struct
haftmann
parents: 44064
diff changeset
   283
  type coeff = int
haftmann
parents: 44064
diff changeset
   284
  val iszero = (fn x => x = 0)
haftmann
parents: 44064
diff changeset
   285
  val add  = op +
haftmann
parents: 44064
diff changeset
   286
  val mk_sum = long_mk_sum    (*to work for e.g. 2*x + 3*x *)
haftmann
parents: 44064
diff changeset
   287
  val dest_sum = dest_sum
haftmann
parents: 44064
diff changeset
   288
  val mk_coeff = mk_coeff
haftmann
parents: 44064
diff changeset
   289
  val dest_coeff = dest_coeff 1
haftmann
parents: 44064
diff changeset
   290
  val left_distrib = @{thm combine_common_factor} RS trans
haftmann
parents: 44064
diff changeset
   291
  val prove_conv = Arith_Data.prove_conv_nohyps
44947
8ae418dfe561 dropped unused argument – avoids problem with SML/NJ
haftmann
parents: 44945
diff changeset
   292
  val trans_tac = trans_tac
31068
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   293
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   294
  fun norm_tac ss =
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   295
    ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   296
    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   297
    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3))
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   298
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   299
  val numeral_simp_ss = HOL_ss addsimps add_0s @ simps
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   300
  fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
45437
958d19d3405b tune post-processing of simproc-generated rules so they won't produce Numeral0 or Numeral1
huffman
parents: 45306
diff changeset
   301
  val simplify_meta_eq = Arith_Data.simplify_meta_eq post_simps
44945
haftmann
parents: 44064
diff changeset
   302
end;
31068
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   303
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   304
structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   305
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   306
(*Version for fields, where coefficients can be fractions*)
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   307
structure FieldCombineNumeralsData =
44945
haftmann
parents: 44064
diff changeset
   308
struct
haftmann
parents: 44064
diff changeset
   309
  type coeff = int * int
haftmann
parents: 44064
diff changeset
   310
  val iszero = (fn (p, q) => p = 0)
haftmann
parents: 44064
diff changeset
   311
  val add = add_frac
haftmann
parents: 44064
diff changeset
   312
  val mk_sum = long_mk_sum
haftmann
parents: 44064
diff changeset
   313
  val dest_sum = dest_sum
haftmann
parents: 44064
diff changeset
   314
  val mk_coeff = mk_fcoeff
haftmann
parents: 44064
diff changeset
   315
  val dest_coeff = dest_fcoeff 1
haftmann
parents: 44064
diff changeset
   316
  val left_distrib = @{thm combine_common_factor} RS trans
haftmann
parents: 44064
diff changeset
   317
  val prove_conv = Arith_Data.prove_conv_nohyps
44947
8ae418dfe561 dropped unused argument – avoids problem with SML/NJ
haftmann
parents: 44945
diff changeset
   318
  val trans_tac = trans_tac
31068
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   319
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   320
  val norm_ss1a = norm_ss1 addsimps inverse_1s @ divide_simps
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   321
  fun norm_tac ss =
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   322
    ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1a))
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   323
    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   324
    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3))
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   325
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   326
  val numeral_simp_ss = HOL_ss addsimps add_0s @ simps @ [@{thm add_frac_eq}]
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   327
  fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
45437
958d19d3405b tune post-processing of simproc-generated rules so they won't produce Numeral0 or Numeral1
huffman
parents: 45306
diff changeset
   328
  val simplify_meta_eq = Arith_Data.simplify_meta_eq field_post_simps
44945
haftmann
parents: 44064
diff changeset
   329
end;
31068
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   330
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   331
structure FieldCombineNumerals = CombineNumeralsFun(FieldCombineNumeralsData);
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   332
45284
ae78a4ffa81d use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents: 45270
diff changeset
   333
fun combine_numerals ss ct = CombineNumerals.proc ss (term_of ct)
31068
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   334
45284
ae78a4ffa81d use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents: 45270
diff changeset
   335
fun field_combine_numerals ss ct = FieldCombineNumerals.proc ss (term_of ct)
31068
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   336
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   337
(** Constant folding for multiplication in semirings **)
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   338
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   339
(*We do not need folding for addition: combine_numerals does the same thing*)
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   340
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   341
structure Semiring_Times_Assoc_Data : ASSOC_FOLD_DATA =
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   342
struct
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   343
  val assoc_ss = HOL_ss addsimps @{thms mult_ac}
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   344
  val eq_reflection = eq_reflection
35983
27e2fa7d4ce7 slightly more general simproc (avoids errors of linarith)
boehmes
parents: 35408
diff changeset
   345
  val is_numeral = can HOLogic.dest_number
31068
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   346
end;
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   347
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   348
structure Semiring_Times_Assoc = Assoc_Fold (Semiring_Times_Assoc_Data);
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   349
45284
ae78a4ffa81d use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents: 45270
diff changeset
   350
fun assoc_fold ss ct = Semiring_Times_Assoc.proc ss (term_of ct)
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   351
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   352
structure CancelNumeralFactorCommon =
44945
haftmann
parents: 44064
diff changeset
   353
struct
haftmann
parents: 44064
diff changeset
   354
  val mk_coeff = mk_coeff
haftmann
parents: 44064
diff changeset
   355
  val dest_coeff = dest_coeff 1
44947
8ae418dfe561 dropped unused argument – avoids problem with SML/NJ
haftmann
parents: 44945
diff changeset
   356
  val trans_tac = trans_tac
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   357
44983
b36eedcd1633 numeral_simprocs.ML: use HOL_basic_ss instead of HOL_ss for internal normalization proofs of cancel_factor simprocs, to avoid splitting if-then-else
huffman
parents: 44064
diff changeset
   358
  val norm_ss1 = HOL_basic_ss addsimps minus_from_mult_simps @ mult_1s
b36eedcd1633 numeral_simprocs.ML: use HOL_basic_ss instead of HOL_ss for internal normalization proofs of cancel_factor simprocs, to avoid splitting if-then-else
huffman
parents: 44064
diff changeset
   359
  val norm_ss2 = HOL_basic_ss addsimps simps @ mult_minus_simps
b36eedcd1633 numeral_simprocs.ML: use HOL_basic_ss instead of HOL_ss for internal normalization proofs of cancel_factor simprocs, to avoid splitting if-then-else
huffman
parents: 44064
diff changeset
   360
  val norm_ss3 = HOL_basic_ss addsimps @{thms mult_ac}
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   361
  fun norm_tac ss =
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   362
    ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   363
    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   364
    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3))
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   365
31068
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   366
  val numeral_simp_ss = HOL_ss addsimps
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   367
    [@{thm eq_number_of_eq}, @{thm less_number_of}, @{thm le_number_of}] @ simps
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   368
  fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
30518
07b45c1aa788 moved some generic nonsense to arith_data.ML
haftmann
parents: 30496
diff changeset
   369
  val simplify_meta_eq = Arith_Data.simplify_meta_eq
45437
958d19d3405b tune post-processing of simproc-generated rules so they won't produce Numeral0 or Numeral1
huffman
parents: 45306
diff changeset
   370
    ([@{thm Nat.add_0}, @{thm Nat.add_0_right}] @ post_simps)
44945
haftmann
parents: 44064
diff changeset
   371
  val prove_conv = Arith_Data.prove_conv
haftmann
parents: 44064
diff changeset
   372
end
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   373
30931
86ca651da03e generalized some simprocs from int to semiring_div
haftmann
parents: 30685
diff changeset
   374
(*Version for semiring_div*)
86ca651da03e generalized some simprocs from int to semiring_div
haftmann
parents: 30685
diff changeset
   375
structure DivCancelNumeralFactor = CancelNumeralFactorFun
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   376
 (open CancelNumeralFactorCommon
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   377
  val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
30931
86ca651da03e generalized some simprocs from int to semiring_div
haftmann
parents: 30685
diff changeset
   378
  val dest_bal = HOLogic.dest_bin @{const_name Divides.div} Term.dummyT
86ca651da03e generalized some simprocs from int to semiring_div
haftmann
parents: 30685
diff changeset
   379
  val cancel = @{thm div_mult_mult1} RS trans
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   380
  val neg_exchanges = false
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   381
)
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   382
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   383
(*Version for fields*)
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   384
structure DivideCancelNumeralFactor = CancelNumeralFactorFun
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   385
 (open CancelNumeralFactorCommon
44064
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 40878
diff changeset
   386
  val mk_bal   = HOLogic.mk_binop @{const_name Fields.divide}
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 40878
diff changeset
   387
  val dest_bal = HOLogic.dest_bin @{const_name Fields.divide} Term.dummyT
23413
5caa2710dd5b tuned laws for cancellation in divisions for fields.
nipkow
parents: 23401
diff changeset
   388
  val cancel = @{thm mult_divide_mult_cancel_left} RS trans
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   389
  val neg_exchanges = false
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   390
)
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   391
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   392
structure EqCancelNumeralFactor = CancelNumeralFactorFun
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   393
 (open CancelNumeralFactorCommon
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   394
  val mk_bal   = HOLogic.mk_eq
38864
4abe644fcea5 formerly unnamed infix equality now named HOL.eq
haftmann
parents: 38549
diff changeset
   395
  val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} Term.dummyT
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   396
  val cancel = @{thm mult_cancel_left} RS trans
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   397
  val neg_exchanges = false
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   398
)
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   399
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   400
structure LessCancelNumeralFactor = CancelNumeralFactorFun
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   401
 (open CancelNumeralFactorCommon
35092
cfe605c54e50 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents: 35084
diff changeset
   402
  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
cfe605c54e50 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents: 35084
diff changeset
   403
  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} Term.dummyT
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   404
  val cancel = @{thm mult_less_cancel_left} RS trans
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   405
  val neg_exchanges = true
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   406
)
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   407
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   408
structure LeCancelNumeralFactor = CancelNumeralFactorFun
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   409
 (open CancelNumeralFactorCommon
35092
cfe605c54e50 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents: 35084
diff changeset
   410
  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
cfe605c54e50 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents: 35084
diff changeset
   411
  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} Term.dummyT
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   412
  val cancel = @{thm mult_le_cancel_left} RS trans
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   413
  val neg_exchanges = true
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   414
)
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   415
45284
ae78a4ffa81d use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents: 45270
diff changeset
   416
fun eq_cancel_numeral_factor ss ct = EqCancelNumeralFactor.proc ss (term_of ct)
ae78a4ffa81d use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents: 45270
diff changeset
   417
fun less_cancel_numeral_factor ss ct = LessCancelNumeralFactor.proc ss (term_of ct)
ae78a4ffa81d use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents: 45270
diff changeset
   418
fun le_cancel_numeral_factor ss ct = LeCancelNumeralFactor.proc ss (term_of ct)
ae78a4ffa81d use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents: 45270
diff changeset
   419
fun div_cancel_numeral_factor ss ct = DivCancelNumeralFactor.proc ss (term_of ct)
ae78a4ffa81d use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents: 45270
diff changeset
   420
fun divide_cancel_numeral_factor ss ct = DivideCancelNumeralFactor.proc ss (term_of ct)
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   421
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   422
val field_cancel_numeral_factors =
44945
haftmann
parents: 44064
diff changeset
   423
  map (prep_simproc @{theory})
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   424
   [("field_eq_cancel_numeral_factor",
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   425
     ["(l::'a::{field,number_ring}) * m = n",
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   426
      "(l::'a::{field,number_ring}) = m * n"],
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   427
     K EqCancelNumeralFactor.proc),
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   428
    ("field_cancel_numeral_factor",
36409
d323e7773aa8 use new classes (linordered_)field_inverse_zero
haftmann
parents: 36349
diff changeset
   429
     ["((l::'a::{field_inverse_zero,number_ring}) * m) / n",
d323e7773aa8 use new classes (linordered_)field_inverse_zero
haftmann
parents: 36349
diff changeset
   430
      "(l::'a::{field_inverse_zero,number_ring}) / (m * n)",
d323e7773aa8 use new classes (linordered_)field_inverse_zero
haftmann
parents: 36349
diff changeset
   431
      "((number_of v)::'a::{field_inverse_zero,number_ring}) / (number_of w)"],
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   432
     K DivideCancelNumeralFactor.proc)]
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   433
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   434
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   435
(** Declarations for ExtractCommonTerm **)
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   436
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   437
(*Find first term that matches u*)
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   438
fun find_first_t past u []         = raise TERM ("find_first_t", [])
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   439
  | find_first_t past u (t::terms) =
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   440
        if u aconv t then (rev past @ terms)
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   441
        else find_first_t (t::past) u terms
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   442
        handle TERM _ => find_first_t (t::past) u terms;
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   443
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   444
(** Final simplification for the CancelFactor simprocs **)
30518
07b45c1aa788 moved some generic nonsense to arith_data.ML
haftmann
parents: 30496
diff changeset
   445
val simplify_one = Arith_Data.simplify_meta_eq  
30031
bd786c37af84 Removed redundant lemmas
nipkow
parents: 29981
diff changeset
   446
  [@{thm mult_1_left}, @{thm mult_1_right}, @{thm div_by_1}, @{thm numeral_1_eq_1}];
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   447
30649
57753e0ec1d4 1. New cancellation simprocs for common factors in inequations
nipkow
parents: 30518
diff changeset
   448
fun cancel_simplify_meta_eq ss cancel_th th =
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   449
    simplify_one ss (([th, cancel_th]) MRS trans);
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   450
30649
57753e0ec1d4 1. New cancellation simprocs for common factors in inequations
nipkow
parents: 30518
diff changeset
   451
local
31067
fd7ec31f850c generalized simproc for mod
haftmann
parents: 30931
diff changeset
   452
  val Tp_Eq = Thm.reflexive (Thm.cterm_of @{theory HOL} HOLogic.Trueprop)
30649
57753e0ec1d4 1. New cancellation simprocs for common factors in inequations
nipkow
parents: 30518
diff changeset
   453
  fun Eq_True_elim Eq = 
57753e0ec1d4 1. New cancellation simprocs for common factors in inequations
nipkow
parents: 30518
diff changeset
   454
    Thm.equal_elim (Thm.combination Tp_Eq (Thm.symmetric Eq)) @{thm TrueI}
57753e0ec1d4 1. New cancellation simprocs for common factors in inequations
nipkow
parents: 30518
diff changeset
   455
in
57753e0ec1d4 1. New cancellation simprocs for common factors in inequations
nipkow
parents: 30518
diff changeset
   456
fun sign_conv pos_th neg_th ss t =
57753e0ec1d4 1. New cancellation simprocs for common factors in inequations
nipkow
parents: 30518
diff changeset
   457
  let val T = fastype_of t;
35267
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35092
diff changeset
   458
      val zero = Const(@{const_name Groups.zero}, T);
35092
cfe605c54e50 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents: 35084
diff changeset
   459
      val less = Const(@{const_name Orderings.less}, [T,T] ---> HOLogic.boolT);
30649
57753e0ec1d4 1. New cancellation simprocs for common factors in inequations
nipkow
parents: 30518
diff changeset
   460
      val pos = less $ zero $ t and neg = less $ t $ zero
57753e0ec1d4 1. New cancellation simprocs for common factors in inequations
nipkow
parents: 30518
diff changeset
   461
      fun prove p =
31101
26c7bb764a38 qualified names for Lin_Arith tactics and simprocs
haftmann
parents: 31068
diff changeset
   462
        Option.map Eq_True_elim (Lin_Arith.simproc ss p)
30649
57753e0ec1d4 1. New cancellation simprocs for common factors in inequations
nipkow
parents: 30518
diff changeset
   463
        handle THM _ => NONE
57753e0ec1d4 1. New cancellation simprocs for common factors in inequations
nipkow
parents: 30518
diff changeset
   464
    in case prove pos of
57753e0ec1d4 1. New cancellation simprocs for common factors in inequations
nipkow
parents: 30518
diff changeset
   465
         SOME th => SOME(th RS pos_th)
57753e0ec1d4 1. New cancellation simprocs for common factors in inequations
nipkow
parents: 30518
diff changeset
   466
       | NONE => (case prove neg of
57753e0ec1d4 1. New cancellation simprocs for common factors in inequations
nipkow
parents: 30518
diff changeset
   467
                    SOME th => SOME(th RS neg_th)
57753e0ec1d4 1. New cancellation simprocs for common factors in inequations
nipkow
parents: 30518
diff changeset
   468
                  | NONE => NONE)
57753e0ec1d4 1. New cancellation simprocs for common factors in inequations
nipkow
parents: 30518
diff changeset
   469
    end;
57753e0ec1d4 1. New cancellation simprocs for common factors in inequations
nipkow
parents: 30518
diff changeset
   470
end
57753e0ec1d4 1. New cancellation simprocs for common factors in inequations
nipkow
parents: 30518
diff changeset
   471
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   472
structure CancelFactorCommon =
44945
haftmann
parents: 44064
diff changeset
   473
struct
haftmann
parents: 44064
diff changeset
   474
  val mk_sum = long_mk_prod
haftmann
parents: 44064
diff changeset
   475
  val dest_sum = dest_prod
haftmann
parents: 44064
diff changeset
   476
  val mk_coeff = mk_coeff
haftmann
parents: 44064
diff changeset
   477
  val dest_coeff = dest_coeff
haftmann
parents: 44064
diff changeset
   478
  val find_first = find_first_t []
44947
8ae418dfe561 dropped unused argument – avoids problem with SML/NJ
haftmann
parents: 44945
diff changeset
   479
  val trans_tac = trans_tac
23881
851c74f1bb69 moved class ord from Orderings.thy to HOL.thy
haftmann
parents: 23413
diff changeset
   480
  val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac}
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   481
  fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
30649
57753e0ec1d4 1. New cancellation simprocs for common factors in inequations
nipkow
parents: 30518
diff changeset
   482
  val simplify_meta_eq  = cancel_simplify_meta_eq 
45270
d5b5c9259afd fix bug in cancel_factor simprocs so they will work on goals like 'x * y < x * z' where the common term is already on the left
huffman
parents: 44984
diff changeset
   483
  fun mk_eq (a, b) = HOLogic.mk_Trueprop (HOLogic.mk_eq (a, b))
44945
haftmann
parents: 44064
diff changeset
   484
end;
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   485
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   486
(*mult_cancel_left requires a ring with no zero divisors.*)
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   487
structure EqCancelFactor = ExtractCommonTermFun
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   488
 (open CancelFactorCommon
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   489
  val mk_bal   = HOLogic.mk_eq
38864
4abe644fcea5 formerly unnamed infix equality now named HOL.eq
haftmann
parents: 38549
diff changeset
   490
  val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} Term.dummyT
31368
763f4b0fd579 made SML/NJ happy;
wenzelm
parents: 31101
diff changeset
   491
  fun simp_conv _ _ = SOME @{thm mult_cancel_left}
30649
57753e0ec1d4 1. New cancellation simprocs for common factors in inequations
nipkow
parents: 30518
diff changeset
   492
);
57753e0ec1d4 1. New cancellation simprocs for common factors in inequations
nipkow
parents: 30518
diff changeset
   493
57753e0ec1d4 1. New cancellation simprocs for common factors in inequations
nipkow
parents: 30518
diff changeset
   494
(*for ordered rings*)
57753e0ec1d4 1. New cancellation simprocs for common factors in inequations
nipkow
parents: 30518
diff changeset
   495
structure LeCancelFactor = ExtractCommonTermFun
57753e0ec1d4 1. New cancellation simprocs for common factors in inequations
nipkow
parents: 30518
diff changeset
   496
 (open CancelFactorCommon
35092
cfe605c54e50 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents: 35084
diff changeset
   497
  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
cfe605c54e50 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents: 35084
diff changeset
   498
  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} Term.dummyT
30649
57753e0ec1d4 1. New cancellation simprocs for common factors in inequations
nipkow
parents: 30518
diff changeset
   499
  val simp_conv = sign_conv
57753e0ec1d4 1. New cancellation simprocs for common factors in inequations
nipkow
parents: 30518
diff changeset
   500
    @{thm mult_le_cancel_left_pos} @{thm mult_le_cancel_left_neg}
57753e0ec1d4 1. New cancellation simprocs for common factors in inequations
nipkow
parents: 30518
diff changeset
   501
);
57753e0ec1d4 1. New cancellation simprocs for common factors in inequations
nipkow
parents: 30518
diff changeset
   502
57753e0ec1d4 1. New cancellation simprocs for common factors in inequations
nipkow
parents: 30518
diff changeset
   503
(*for ordered rings*)
57753e0ec1d4 1. New cancellation simprocs for common factors in inequations
nipkow
parents: 30518
diff changeset
   504
structure LessCancelFactor = ExtractCommonTermFun
57753e0ec1d4 1. New cancellation simprocs for common factors in inequations
nipkow
parents: 30518
diff changeset
   505
 (open CancelFactorCommon
35092
cfe605c54e50 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents: 35084
diff changeset
   506
  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
cfe605c54e50 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents: 35084
diff changeset
   507
  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} Term.dummyT
30649
57753e0ec1d4 1. New cancellation simprocs for common factors in inequations
nipkow
parents: 30518
diff changeset
   508
  val simp_conv = sign_conv
57753e0ec1d4 1. New cancellation simprocs for common factors in inequations
nipkow
parents: 30518
diff changeset
   509
    @{thm mult_less_cancel_left_pos} @{thm mult_less_cancel_left_neg}
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   510
);
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   511
30931
86ca651da03e generalized some simprocs from int to semiring_div
haftmann
parents: 30685
diff changeset
   512
(*for semirings with division*)
86ca651da03e generalized some simprocs from int to semiring_div
haftmann
parents: 30685
diff changeset
   513
structure DivCancelFactor = ExtractCommonTermFun
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   514
 (open CancelFactorCommon
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   515
  val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
30931
86ca651da03e generalized some simprocs from int to semiring_div
haftmann
parents: 30685
diff changeset
   516
  val dest_bal = HOLogic.dest_bin @{const_name Divides.div} Term.dummyT
31368
763f4b0fd579 made SML/NJ happy;
wenzelm
parents: 31101
diff changeset
   517
  fun simp_conv _ _ = SOME @{thm div_mult_mult1_if}
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   518
);
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   519
30931
86ca651da03e generalized some simprocs from int to semiring_div
haftmann
parents: 30685
diff changeset
   520
structure ModCancelFactor = ExtractCommonTermFun
24395
8df021f79e0b Added mod cancellation simproc
nipkow
parents: 23969
diff changeset
   521
 (open CancelFactorCommon
8df021f79e0b Added mod cancellation simproc
nipkow
parents: 23969
diff changeset
   522
  val mk_bal   = HOLogic.mk_binop @{const_name Divides.mod}
31067
fd7ec31f850c generalized simproc for mod
haftmann
parents: 30931
diff changeset
   523
  val dest_bal = HOLogic.dest_bin @{const_name Divides.mod} Term.dummyT
31368
763f4b0fd579 made SML/NJ happy;
wenzelm
parents: 31101
diff changeset
   524
  fun simp_conv _ _ = SOME @{thm mod_mult_mult1}
24395
8df021f79e0b Added mod cancellation simproc
nipkow
parents: 23969
diff changeset
   525
);
8df021f79e0b Added mod cancellation simproc
nipkow
parents: 23969
diff changeset
   526
30931
86ca651da03e generalized some simprocs from int to semiring_div
haftmann
parents: 30685
diff changeset
   527
(*for idoms*)
86ca651da03e generalized some simprocs from int to semiring_div
haftmann
parents: 30685
diff changeset
   528
structure DvdCancelFactor = ExtractCommonTermFun
23969
ef782bbf2d09 Added cancel simprocs for dvd on nat and int
nipkow
parents: 23881
diff changeset
   529
 (open CancelFactorCommon
35050
9f841f20dca6 renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents: 35043
diff changeset
   530
  val mk_bal   = HOLogic.mk_binrel @{const_name Rings.dvd}
9f841f20dca6 renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents: 35043
diff changeset
   531
  val dest_bal = HOLogic.dest_bin @{const_name Rings.dvd} Term.dummyT
31368
763f4b0fd579 made SML/NJ happy;
wenzelm
parents: 31101
diff changeset
   532
  fun simp_conv _ _ = SOME @{thm dvd_mult_cancel_left}
23969
ef782bbf2d09 Added cancel simprocs for dvd on nat and int
nipkow
parents: 23881
diff changeset
   533
);
ef782bbf2d09 Added cancel simprocs for dvd on nat and int
nipkow
parents: 23881
diff changeset
   534
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   535
(*Version for all fields, including unordered ones (type complex).*)
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   536
structure DivideCancelFactor = ExtractCommonTermFun
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   537
 (open CancelFactorCommon
44064
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 40878
diff changeset
   538
  val mk_bal   = HOLogic.mk_binop @{const_name Fields.divide}
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 40878
diff changeset
   539
  val dest_bal = HOLogic.dest_bin @{const_name Fields.divide} Term.dummyT
31368
763f4b0fd579 made SML/NJ happy;
wenzelm
parents: 31101
diff changeset
   540
  fun simp_conv _ _ = SOME @{thm mult_divide_mult_cancel_left_if}
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   541
);
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   542
45284
ae78a4ffa81d use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents: 45270
diff changeset
   543
fun eq_cancel_factor ss ct = EqCancelFactor.proc ss (term_of ct)
ae78a4ffa81d use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents: 45270
diff changeset
   544
fun le_cancel_factor ss ct = LeCancelFactor.proc ss (term_of ct)
ae78a4ffa81d use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents: 45270
diff changeset
   545
fun less_cancel_factor ss ct = LessCancelFactor.proc ss (term_of ct)
ae78a4ffa81d use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents: 45270
diff changeset
   546
fun div_cancel_factor ss ct = DivCancelFactor.proc ss (term_of ct)
ae78a4ffa81d use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents: 45270
diff changeset
   547
fun mod_cancel_factor ss ct = ModCancelFactor.proc ss (term_of ct)
ae78a4ffa81d use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents: 45270
diff changeset
   548
fun dvd_cancel_factor ss ct = DvdCancelFactor.proc ss (term_of ct)
ae78a4ffa81d use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents: 45270
diff changeset
   549
fun divide_cancel_factor ss ct = DivideCancelFactor.proc ss (term_of ct)
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   550
36751
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   551
local
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   552
 val zr = @{cpat "0"}
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   553
 val zT = ctyp_of_term zr
38864
4abe644fcea5 formerly unnamed infix equality now named HOL.eq
haftmann
parents: 38549
diff changeset
   554
 val geq = @{cpat HOL.eq}
36751
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   555
 val eqT = Thm.dest_ctyp (ctyp_of_term geq) |> hd
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   556
 val add_frac_eq = mk_meta_eq @{thm "add_frac_eq"}
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   557
 val add_frac_num = mk_meta_eq @{thm "add_frac_num"}
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   558
 val add_num_frac = mk_meta_eq @{thm "add_num_frac"}
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   559
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   560
 fun prove_nz ss T t =
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   561
    let
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36751
diff changeset
   562
      val z = Thm.instantiate_cterm ([(zT,T)],[]) zr
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36751
diff changeset
   563
      val eq = Thm.instantiate_cterm ([(eqT,T)],[]) geq
36751
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   564
      val th = Simplifier.rewrite (ss addsimps @{thms simp_thms})
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   565
           (Thm.capply @{cterm "Trueprop"} (Thm.capply @{cterm "Not"}
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   566
                  (Thm.capply (Thm.capply eq t) z)))
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36751
diff changeset
   567
    in Thm.equal_elim (Thm.symmetric th) TrueI
36751
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   568
    end
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   569
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   570
 fun proc phi ss ct =
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   571
  let
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   572
    val ((x,y),(w,z)) =
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   573
         (Thm.dest_binop #> (fn (a,b) => (Thm.dest_binop a, Thm.dest_binop b))) ct
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   574
    val _ = map (HOLogic.dest_number o term_of) [x,y,z,w]
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   575
    val T = ctyp_of_term x
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   576
    val [y_nz, z_nz] = map (prove_nz ss T) [y, z]
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   577
    val th = instantiate' [SOME T] (map SOME [y,z,x,w]) add_frac_eq
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36751
diff changeset
   578
  in SOME (Thm.implies_elim (Thm.implies_elim th y_nz) z_nz)
36751
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   579
  end
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   580
  handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   581
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   582
 fun proc2 phi ss ct =
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   583
  let
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   584
    val (l,r) = Thm.dest_binop ct
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   585
    val T = ctyp_of_term l
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   586
  in (case (term_of l, term_of r) of
44064
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 40878
diff changeset
   587
      (Const(@{const_name Fields.divide},_)$_$_, _) =>
36751
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   588
        let val (x,y) = Thm.dest_binop l val z = r
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   589
            val _ = map (HOLogic.dest_number o term_of) [x,y,z]
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   590
            val ynz = prove_nz ss T y
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36751
diff changeset
   591
        in SOME (Thm.implies_elim (instantiate' [SOME T] (map SOME [y,x,z]) add_frac_num) ynz)
36751
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   592
        end
44064
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 40878
diff changeset
   593
     | (_, Const (@{const_name Fields.divide},_)$_$_) =>
36751
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   594
        let val (x,y) = Thm.dest_binop r val z = l
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   595
            val _ = map (HOLogic.dest_number o term_of) [x,y,z]
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   596
            val ynz = prove_nz ss T y
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36751
diff changeset
   597
        in SOME (Thm.implies_elim (instantiate' [SOME T] (map SOME [y,z,x]) add_num_frac) ynz)
36751
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   598
        end
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   599
     | _ => NONE)
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   600
  end
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   601
  handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   602
44064
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 40878
diff changeset
   603
 fun is_number (Const(@{const_name Fields.divide},_)$a$b) = is_number a andalso is_number b
36751
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   604
   | is_number t = can HOLogic.dest_number t
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   605
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   606
 val is_number = is_number o term_of
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   607
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   608
 fun proc3 phi ss ct =
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   609
  (case term_of ct of
44064
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 40878
diff changeset
   610
    Const(@{const_name Orderings.less},_)$(Const(@{const_name Fields.divide},_)$_$_)$_ =>
36751
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   611
      let
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   612
        val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   613
        val _ = map is_number [a,b,c]
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   614
        val T = ctyp_of_term c
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   615
        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_less_eq"}
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   616
      in SOME (mk_meta_eq th) end
44064
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 40878
diff changeset
   617
  | Const(@{const_name Orderings.less_eq},_)$(Const(@{const_name Fields.divide},_)$_$_)$_ =>
36751
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   618
      let
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   619
        val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   620
        val _ = map is_number [a,b,c]
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   621
        val T = ctyp_of_term c
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   622
        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_le_eq"}
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   623
      in SOME (mk_meta_eq th) end
44064
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 40878
diff changeset
   624
  | Const(@{const_name HOL.eq},_)$(Const(@{const_name Fields.divide},_)$_$_)$_ =>
36751
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   625
      let
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   626
        val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   627
        val _ = map is_number [a,b,c]
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   628
        val T = ctyp_of_term c
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   629
        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_eq_eq"}
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   630
      in SOME (mk_meta_eq th) end
44064
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 40878
diff changeset
   631
  | Const(@{const_name Orderings.less},_)$_$(Const(@{const_name Fields.divide},_)$_$_) =>
36751
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   632
    let
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   633
      val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   634
        val _ = map is_number [a,b,c]
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   635
        val T = ctyp_of_term c
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   636
        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "less_divide_eq"}
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   637
      in SOME (mk_meta_eq th) end
44064
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 40878
diff changeset
   638
  | Const(@{const_name Orderings.less_eq},_)$_$(Const(@{const_name Fields.divide},_)$_$_) =>
36751
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   639
    let
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   640
      val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   641
        val _ = map is_number [a,b,c]
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   642
        val T = ctyp_of_term c
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   643
        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "le_divide_eq"}
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   644
      in SOME (mk_meta_eq th) end
44064
5bce8ff0d9ae moved division ring stuff from Rings.thy to Fields.thy
huffman
parents: 40878
diff changeset
   645
  | Const(@{const_name HOL.eq},_)$_$(Const(@{const_name Fields.divide},_)$_$_) =>
36751
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   646
    let
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   647
      val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   648
        val _ = map is_number [a,b,c]
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   649
        val T = ctyp_of_term c
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   650
        val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "eq_divide_eq"}
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   651
      in SOME (mk_meta_eq th) end
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   652
  | _ => NONE)
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   653
  handle TERM _ => NONE | CTERM _ => NONE | THM _ => NONE
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   654
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   655
val add_frac_frac_simproc =
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   656
       make_simproc {lhss = [@{cpat "(?x::?'a::field)/?y + (?w::?'a::field)/?z"}],
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   657
                     name = "add_frac_frac_simproc",
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   658
                     proc = proc, identifier = []}
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   659
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   660
val add_frac_num_simproc =
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   661
       make_simproc {lhss = [@{cpat "(?x::?'a::field)/?y + ?z"}, @{cpat "?z + (?x::?'a::field)/?y"}],
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   662
                     name = "add_frac_num_simproc",
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   663
                     proc = proc2, identifier = []}
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   664
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   665
val ord_frac_simproc =
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   666
  make_simproc
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   667
    {lhss = [@{cpat "(?a::(?'a::{field, ord}))/?b < ?c"},
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   668
             @{cpat "(?a::(?'a::{field, ord}))/?b <= ?c"},
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   669
             @{cpat "?c < (?a::(?'a::{field, ord}))/?b"},
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   670
             @{cpat "?c <= (?a::(?'a::{field, ord}))/?b"},
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   671
             @{cpat "?c = ((?a::(?'a::{field, ord}))/?b)"},
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   672
             @{cpat "((?a::(?'a::{field, ord}))/ ?b) = ?c"}],
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   673
             name = "ord_frac_simproc", proc = proc3, identifier = []}
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   674
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   675
val ths = [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"},
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   676
           @{thm "divide_Numeral1"},
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   677
           @{thm "divide_zero"}, @{thm "divide_Numeral0"},
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   678
           @{thm "divide_divide_eq_left"}, 
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   679
           @{thm "times_divide_eq_left"}, @{thm "times_divide_eq_right"},
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   680
           @{thm "times_divide_times_eq"},
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   681
           @{thm "divide_divide_eq_right"},
37887
2ae085b07f2f diff_minus subsumes diff_def
haftmann
parents: 36945
diff changeset
   682
           @{thm "diff_minus"}, @{thm "minus_divide_left"},
36751
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   683
           @{thm "Numeral1_eq1_nat"}, @{thm "add_divide_distrib"} RS sym,
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   684
           @{thm field_divide_inverse} RS sym, @{thm inverse_divide}, 
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   685
           Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv (Conv.rewr_conv (mk_meta_eq @{thm mult_commute}))))   
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   686
           (@{thm field_divide_inverse} RS sym)]
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   687
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   688
in
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   689
45620
f2a587696afb modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents: 45437
diff changeset
   690
val field_comp_conv =
f2a587696afb modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents: 45437
diff changeset
   691
  Simplifier.rewrite
f2a587696afb modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents: 45437
diff changeset
   692
    (HOL_basic_ss addsimps @{thms "semiring_norm"}
f2a587696afb modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents: 45437
diff changeset
   693
      addsimps ths addsimps @{thms simp_thms}
f2a587696afb modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents: 45437
diff changeset
   694
      addsimprocs field_cancel_numeral_factors
f2a587696afb modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents: 45437
diff changeset
   695
      addsimprocs [add_frac_frac_simproc, add_frac_num_simproc, ord_frac_simproc]
f2a587696afb modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents: 45437
diff changeset
   696
      |> Simplifier.add_cong @{thm "if_weak_cong"})
f2a587696afb modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents: 45437
diff changeset
   697
  then_conv
f2a587696afb modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents: 45437
diff changeset
   698
  Simplifier.rewrite (HOL_basic_ss addsimps
f2a587696afb modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents: 45437
diff changeset
   699
    [@{thm numeral_1_eq_1},@{thm numeral_0_eq_0}] @ @{thms numerals(1-2)})
36751
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   700
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   701
end
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36409
diff changeset
   702
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   703
end;
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   704
31068
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   705
(*examples:
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   706
print_depth 22;
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   707
set timing;
40878
7695e4de4d86 renamed trace_simp to simp_trace, and debug_simp to simp_debug;
wenzelm
parents: 38864
diff changeset
   708
set simp_trace;
31068
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   709
fun test s = (Goal s, by (Simp_tac 1));
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   710
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   711
test "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::int)";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   712
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   713
test "2*u = (u::int)";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   714
test "(i + j + 12 + (k::int)) - 15 = y";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   715
test "(i + j + 12 + (k::int)) - 5 = y";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   716
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   717
test "y - b < (b::int)";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   718
test "y - (3*b + c) < (b::int) - 2*c";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   719
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   720
test "(2*x - (u*v) + y) - v*3*u = (w::int)";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   721
test "(2*x*u*v + (u*v)*4 + y) - v*u*4 = (w::int)";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   722
test "(2*x*u*v + (u*v)*4 + y) - v*u = (w::int)";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   723
test "u*v - (x*u*v + (u*v)*4 + y) = (w::int)";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   724
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   725
test "(i + j + 12 + (k::int)) = u + 15 + y";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   726
test "(i + j*2 + 12 + (k::int)) = j + 5 + y";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   727
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   728
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::int)";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   729
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   730
test "a + -(b+c) + b = (d::int)";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   731
test "a + -(b+c) - b = (d::int)";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   732
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   733
(*negative numerals*)
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   734
test "(i + j + -2 + (k::int)) - (u + 5 + y) = zz";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   735
test "(i + j + -3 + (k::int)) < u + 5 + y";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   736
test "(i + j + 3 + (k::int)) < u + -6 + y";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   737
test "(i + j + -12 + (k::int)) - 15 = y";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   738
test "(i + j + 12 + (k::int)) - -15 = y";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   739
test "(i + j + -12 + (k::int)) - -15 = y";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   740
*)
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   741
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   742
(*examples:
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   743
print_depth 22;
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   744
set timing;
40878
7695e4de4d86 renamed trace_simp to simp_trace, and debug_simp to simp_debug;
wenzelm
parents: 38864
diff changeset
   745
set simp_trace;
31068
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   746
fun test s = (Goal s; by (Simp_tac 1));
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   747
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   748
test "9*x = 12 * (y::int)";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   749
test "(9*x) div (12 * (y::int)) = z";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   750
test "9*x < 12 * (y::int)";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   751
test "9*x <= 12 * (y::int)";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   752
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   753
test "-99*x = 132 * (y::int)";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   754
test "(-99*x) div (132 * (y::int)) = z";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   755
test "-99*x < 132 * (y::int)";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   756
test "-99*x <= 132 * (y::int)";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   757
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   758
test "999*x = -396 * (y::int)";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   759
test "(999*x) div (-396 * (y::int)) = z";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   760
test "999*x < -396 * (y::int)";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   761
test "999*x <= -396 * (y::int)";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   762
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   763
test "-99*x = -81 * (y::int)";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   764
test "(-99*x) div (-81 * (y::int)) = z";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   765
test "-99*x <= -81 * (y::int)";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   766
test "-99*x < -81 * (y::int)";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   767
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   768
test "-2 * x = -1 * (y::int)";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   769
test "-2 * x = -(y::int)";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   770
test "(-2 * x) div (-1 * (y::int)) = z";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   771
test "-2 * x < -(y::int)";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   772
test "-2 * x <= -1 * (y::int)";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   773
test "-x < -23 * (y::int)";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   774
test "-x <= -23 * (y::int)";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   775
*)
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   776
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   777
(*And the same examples for fields such as rat or real:
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   778
test "0 <= (y::rat) * -2";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   779
test "9*x = 12 * (y::rat)";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   780
test "(9*x) / (12 * (y::rat)) = z";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   781
test "9*x < 12 * (y::rat)";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   782
test "9*x <= 12 * (y::rat)";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   783
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   784
test "-99*x = 132 * (y::rat)";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   785
test "(-99*x) / (132 * (y::rat)) = z";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   786
test "-99*x < 132 * (y::rat)";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   787
test "-99*x <= 132 * (y::rat)";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   788
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   789
test "999*x = -396 * (y::rat)";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   790
test "(999*x) / (-396 * (y::rat)) = z";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   791
test "999*x < -396 * (y::rat)";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   792
test "999*x <= -396 * (y::rat)";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   793
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   794
test  "(- ((2::rat) * x) <= 2 * y)";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   795
test "-99*x = -81 * (y::rat)";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   796
test "(-99*x) / (-81 * (y::rat)) = z";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   797
test "-99*x <= -81 * (y::rat)";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   798
test "-99*x < -81 * (y::rat)";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   799
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   800
test "-2 * x = -1 * (y::rat)";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   801
test "-2 * x = -(y::rat)";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   802
test "(-2 * x) / (-1 * (y::rat)) = z";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   803
test "-2 * x < -(y::rat)";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   804
test "-2 * x <= -1 * (y::rat)";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   805
test "-x < -23 * (y::rat)";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   806
test "-x <= -23 * (y::rat)";
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   807
*)
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31067
diff changeset
   808
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   809
(*examples:
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   810
print_depth 22;
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   811
set timing;
40878
7695e4de4d86 renamed trace_simp to simp_trace, and debug_simp to simp_debug;
wenzelm
parents: 38864
diff changeset
   812
set simp_trace;
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   813
fun test s = (Goal s; by (Asm_simp_tac 1));
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   814
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   815
test "x*k = k*(y::int)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   816
test "k = k*(y::int)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   817
test "a*(b*c) = (b::int)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   818
test "a*(b*c) = d*(b::int)*(x*a)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   819
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   820
test "(x*k) div (k*(y::int)) = (uu::int)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   821
test "(k) div (k*(y::int)) = (uu::int)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   822
test "(a*(b*c)) div ((b::int)) = (uu::int)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   823
test "(a*(b*c)) div (d*(b::int)*(x*a)) = (uu::int)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   824
*)
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   825
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   826
(*And the same examples for fields such as rat or real:
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   827
print_depth 22;
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   828
set timing;
40878
7695e4de4d86 renamed trace_simp to simp_trace, and debug_simp to simp_debug;
wenzelm
parents: 38864
diff changeset
   829
set simp_trace;
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   830
fun test s = (Goal s; by (Asm_simp_tac 1));
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   831
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   832
test "x*k = k*(y::rat)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   833
test "k = k*(y::rat)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   834
test "a*(b*c) = (b::rat)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   835
test "a*(b*c) = d*(b::rat)*(x*a)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   836
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   837
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   838
test "(x*k) / (k*(y::rat)) = (uu::rat)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   839
test "(k) / (k*(y::rat)) = (uu::rat)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   840
test "(a*(b*c)) / ((b::rat)) = (uu::rat)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   841
test "(a*(b*c)) / (d*(b::rat)*(x*a)) = (uu::rat)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   842
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   843
(*FIXME: what do we do about this?*)
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   844
test "a*(b*c)/(y*z) = d*(b::rat)*(x*a)/z";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   845
*)