src/HOL/Tools/nat_numeral_simprocs.ML
author huffman
Fri, 11 Nov 2011 11:30:31 +0100
changeset 45463 9a588a835c1e
parent 45462 aba629d6cee5
child 45668 0ea1c705eebb
permissions -rw-r--r--
use simproc_setup for the remaining nat_numeral simprocs
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: 30685
diff changeset
     1
(* Author: Lawrence C Paulson, Cambridge University Computer Laboratory
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
     2
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
     3
Simprocs for nat numerals.
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
     4
*)
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
     5
31068
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 30685
diff changeset
     6
signature NAT_NUMERAL_SIMPROCS =
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 30685
diff changeset
     7
sig
45462
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45436
diff changeset
     8
  val combine_numerals: simpset -> cterm -> thm option
45436
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45306
diff changeset
     9
  val eq_cancel_numerals: simpset -> cterm -> thm option
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45306
diff changeset
    10
  val less_cancel_numerals: simpset -> cterm -> thm option
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45306
diff changeset
    11
  val le_cancel_numerals: simpset -> cterm -> thm option
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45306
diff changeset
    12
  val diff_cancel_numerals: simpset -> cterm -> thm option
45463
9a588a835c1e use simproc_setup for the remaining nat_numeral simprocs
huffman
parents: 45462
diff changeset
    13
  val eq_cancel_numeral_factor: simpset -> cterm -> thm option
9a588a835c1e use simproc_setup for the remaining nat_numeral simprocs
huffman
parents: 45462
diff changeset
    14
  val less_cancel_numeral_factor: simpset -> cterm -> thm option
9a588a835c1e use simproc_setup for the remaining nat_numeral simprocs
huffman
parents: 45462
diff changeset
    15
  val le_cancel_numeral_factor: simpset -> cterm -> thm option
9a588a835c1e use simproc_setup for the remaining nat_numeral simprocs
huffman
parents: 45462
diff changeset
    16
  val div_cancel_numeral_factor: simpset -> cterm -> thm option
9a588a835c1e use simproc_setup for the remaining nat_numeral simprocs
huffman
parents: 45462
diff changeset
    17
  val dvd_cancel_numeral_factor: simpset -> cterm -> thm option
45462
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45436
diff changeset
    18
  val eq_cancel_factor: simpset -> cterm -> thm option
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45436
diff changeset
    19
  val less_cancel_factor: simpset -> cterm -> thm option
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45436
diff changeset
    20
  val le_cancel_factor: simpset -> cterm -> thm option
45463
9a588a835c1e use simproc_setup for the remaining nat_numeral simprocs
huffman
parents: 45462
diff changeset
    21
  val div_cancel_factor: simpset -> cterm -> thm option
45462
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45436
diff changeset
    22
  val dvd_cancel_factor: simpset -> cterm -> thm option
31068
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 30685
diff changeset
    23
end;
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 30685
diff changeset
    24
45462
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45436
diff changeset
    25
structure Nat_Numeral_Simprocs : NAT_NUMERAL_SIMPROCS =
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    26
struct
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    27
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    28
(*Maps n to #n for n = 0, 1, 2*)
30496
7cdcc9dd95cb vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents: 29269
diff changeset
    29
val numeral_syms = [@{thm nat_numeral_0_eq_0} RS sym, @{thm nat_numeral_1_eq_1} RS sym, @{thm numeral_2_eq_2} RS sym];
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    30
val numeral_sym_ss = HOL_ss addsimps numeral_syms;
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    31
44945
haftmann
parents: 40878
diff changeset
    32
val rename_numerals = simplify numeral_sym_ss o Thm.transfer @{theory};
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    33
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    34
(*Utilities*)
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    35
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    36
fun mk_number n = HOLogic.number_of_const HOLogic.natT $ HOLogic.mk_numeral n;
24630
351a308ab58d simplified type int (eliminated IntInf.int, integer);
wenzelm
parents: 24431
diff changeset
    37
fun dest_number t = Int.max (0, snd (HOLogic.dest_number t));
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    38
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    39
fun find_first_numeral past (t::terms) =
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    40
        ((dest_number t, t, rev past @ terms)
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    41
         handle TERM _ => find_first_numeral (t::past) terms)
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    42
  | find_first_numeral past [] = raise TERM("find_first_numeral", []);
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    43
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    44
val zero = mk_number 0;
35267
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35092
diff changeset
    45
val mk_plus = HOLogic.mk_binop @{const_name Groups.plus};
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    46
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    47
(*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*)
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    48
fun mk_sum []        = zero
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    49
  | mk_sum [t,u]     = mk_plus (t, u)
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    50
  | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    51
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    52
(*this version ALWAYS includes a trailing zero*)
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    53
fun long_mk_sum []        = HOLogic.zero
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    54
  | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    55
35267
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35092
diff changeset
    56
val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} HOLogic.natT;
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    57
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    58
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    59
(** Other simproc items **)
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    60
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    61
val bin_simps =
23471
08e6c03b2a72 add thm antiquotations
huffman
parents: 23164
diff changeset
    62
     [@{thm nat_numeral_0_eq_0} RS sym, @{thm nat_numeral_1_eq_1} RS sym,
08e6c03b2a72 add thm antiquotations
huffman
parents: 23164
diff changeset
    63
      @{thm add_nat_number_of}, @{thm nat_number_of_add_left}, 
08e6c03b2a72 add thm antiquotations
huffman
parents: 23164
diff changeset
    64
      @{thm diff_nat_number_of}, @{thm le_number_of_eq_not_less},
08e6c03b2a72 add thm antiquotations
huffman
parents: 23164
diff changeset
    65
      @{thm mult_nat_number_of}, @{thm nat_number_of_mult_left}, 
08e6c03b2a72 add thm antiquotations
huffman
parents: 23164
diff changeset
    66
      @{thm less_nat_number_of}, 
08e6c03b2a72 add thm antiquotations
huffman
parents: 23164
diff changeset
    67
      @{thm Let_number_of}, @{thm nat_number_of}] @
29039
8b9207f82a78 separate neg_simps from rel_simps
huffman
parents: 28952
diff changeset
    68
     @{thms arith_simps} @ @{thms rel_simps} @ @{thms neg_simps};
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    69
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    70
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    71
(*** CancelNumerals simprocs ***)
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    72
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    73
val one = mk_number 1;
35267
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35092
diff changeset
    74
val mk_times = HOLogic.mk_binop @{const_name Groups.times};
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    75
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    76
fun mk_prod [] = one
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    77
  | mk_prod [t] = t
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    78
  | mk_prod (t :: ts) = if t = one then mk_prod ts
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    79
                        else mk_times (t, mk_prod ts);
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
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} HOLogic.natT;
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    82
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    83
fun dest_prod t =
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    84
      let val (t,u) = dest_times t
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    85
      in  dest_prod t @ dest_prod u  end
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    86
      handle TERM _ => [t];
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    87
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    88
(*DON'T do the obvious simplifications; that would create special cases*)
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    89
fun mk_coeff (k,t) = mk_times (mk_number k, t);
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    90
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    91
(*Express t as a product of (possibly) a numeral with other factors, sorted*)
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    92
fun dest_coeff t =
35408
b48ab741683b modernized structure Term_Ord;
wenzelm
parents: 35267
diff changeset
    93
    let val ts = sort Term_Ord.term_ord (dest_prod t)
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    94
        val (n, _, ts') = find_first_numeral [] ts
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    95
                          handle TERM _ => (1, one, ts)
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    96
    in (n, mk_prod ts') end;
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    97
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    98
(*Find first coefficient-term THAT MATCHES u*)
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    99
fun find_first_coeff past u [] = raise TERM("find_first_coeff", [])
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   100
  | find_first_coeff past u (t::terms) =
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   101
        let val (n,u') = dest_coeff t
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   102
        in  if u aconv u' then (n, rev past @ terms)
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   103
                          else find_first_coeff (t::past) u terms
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   104
        end
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   105
        handle TERM _ => find_first_coeff (t::past) u terms;
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   106
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   107
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   108
(*Split up a sum into the list of its constituent terms, on the way removing any
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   109
  Sucs and counting them.*)
37388
793618618f78 tuned quotes, antiquotations and whitespace
haftmann
parents: 35408
diff changeset
   110
fun dest_Suc_sum (Const (@{const_name Suc}, _) $ t, (k,ts)) = dest_Suc_sum (t, (k+1,ts))
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   111
  | dest_Suc_sum (t, (k,ts)) = 
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   112
      let val (t1,t2) = dest_plus t
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   113
      in  dest_Suc_sum (t1, dest_Suc_sum (t2, (k,ts)))  end
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   114
      handle TERM _ => (k, t::ts);
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   115
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   116
(*Code for testing whether numerals are already used in the goal*)
25919
8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int
haftmann
parents: 25481
diff changeset
   117
fun is_numeral (Const(@{const_name Int.number_of}, _) $ w) = true
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   118
  | is_numeral _ = false;
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   119
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   120
fun prod_has_numeral t = exists is_numeral (dest_prod t);
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   121
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   122
(*The Sucs found in the term are converted to a binary numeral. If relaxed is false,
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   123
  an exception is raised unless the original expression contains at least one
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   124
  numeral in a coefficient position.  This prevents nat_combine_numerals from 
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   125
  introducing numerals to goals.*)
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   126
fun dest_Sucs_sum relaxed t = 
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   127
  let val (k,ts) = dest_Suc_sum (t,(0,[]))
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   128
  in
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   129
     if relaxed orelse exists prod_has_numeral ts then 
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   130
       if k=0 then ts
24630
351a308ab58d simplified type int (eliminated IntInf.int, integer);
wenzelm
parents: 24431
diff changeset
   131
       else mk_number k :: ts
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   132
     else raise TERM("Nat_Numeral_Simprocs.dest_Sucs_sum", [t])
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   133
  end;
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   134
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   135
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   136
(*Simplify 1*n and n*1 to n*)
35064
1bdef0c013d3 hide fact names clashing with fact names from Group.thy
haftmann
parents: 35050
diff changeset
   137
val add_0s  = map rename_numerals [@{thm Nat.add_0}, @{thm Nat.add_0_right}];
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   138
val mult_1s = map rename_numerals [@{thm nat_mult_1}, @{thm nat_mult_1_right}];
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   139
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   140
(*Final simplification: cancel + and *; replace Numeral0 by 0 and Numeral1 by 1*)
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   141
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   142
(*And these help the simproc return False when appropriate, which helps
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   143
  the arith prover.*)
23881
851c74f1bb69 moved class ord from Orderings.thy to HOL.thy
haftmann
parents: 23471
diff changeset
   144
val contra_rules = [@{thm add_Suc}, @{thm add_Suc_right}, @{thm Zero_not_Suc},
851c74f1bb69 moved class ord from Orderings.thy to HOL.thy
haftmann
parents: 23471
diff changeset
   145
  @{thm Suc_not_Zero}, @{thm le_0_eq}];
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   146
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   147
val simplify_meta_eq =
30518
07b45c1aa788 moved some generic nonsense to arith_data.ML
haftmann
parents: 30496
diff changeset
   148
    Arith_Data.simplify_meta_eq
35064
1bdef0c013d3 hide fact names clashing with fact names from Group.thy
haftmann
parents: 35050
diff changeset
   149
        ([@{thm nat_numeral_0_eq_0}, @{thm numeral_1_eq_Suc_0}, @{thm Nat.add_0}, @{thm Nat.add_0_right},
23471
08e6c03b2a72 add thm antiquotations
huffman
parents: 23164
diff changeset
   150
          @{thm mult_0}, @{thm mult_0_right}, @{thm mult_1}, @{thm mult_1_right}] @ contra_rules);
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   151
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   152
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   153
(*** Applying CancelNumeralsFun ***)
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   154
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   155
structure CancelNumeralsCommon =
44945
haftmann
parents: 40878
diff changeset
   156
struct
haftmann
parents: 40878
diff changeset
   157
  val mk_sum = (fn T : typ => mk_sum)
haftmann
parents: 40878
diff changeset
   158
  val dest_sum = dest_Sucs_sum true
haftmann
parents: 40878
diff changeset
   159
  val mk_coeff = mk_coeff
haftmann
parents: 40878
diff changeset
   160
  val dest_coeff = dest_coeff
haftmann
parents: 40878
diff changeset
   161
  val find_first_coeff = find_first_coeff []
44947
8ae418dfe561 dropped unused argument – avoids problem with SML/NJ
haftmann
parents: 44945
diff changeset
   162
  val trans_tac = Numeral_Simprocs.trans_tac
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   163
31068
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 30685
diff changeset
   164
  val norm_ss1 = Numeral_Simprocs.num_ss addsimps numeral_syms @ add_0s @ mult_1s @
31790
05c92381363c corrected and unified thm names
nipkow
parents: 31368
diff changeset
   165
    [@{thm Suc_eq_plus1_left}] @ @{thms add_ac}
31068
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 30685
diff changeset
   166
  val norm_ss2 = Numeral_Simprocs.num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   167
  fun norm_tac ss = 
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   168
    ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   169
    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   170
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   171
  val numeral_simp_ss = HOL_ss addsimps add_0s @ bin_simps;
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   172
  fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss));
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   173
  val simplify_meta_eq  = simplify_meta_eq
44945
haftmann
parents: 40878
diff changeset
   174
  val prove_conv = Arith_Data.prove_conv
haftmann
parents: 40878
diff changeset
   175
end;
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   176
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   177
structure EqCancelNumerals = CancelNumeralsFun
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   178
 (open CancelNumeralsCommon
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   179
  val mk_bal   = HOLogic.mk_eq
38864
4abe644fcea5 formerly unnamed infix equality now named HOL.eq
haftmann
parents: 37388
diff changeset
   180
  val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} HOLogic.natT
23471
08e6c03b2a72 add thm antiquotations
huffman
parents: 23164
diff changeset
   181
  val bal_add1 = @{thm nat_eq_add_iff1} RS trans
08e6c03b2a72 add thm antiquotations
huffman
parents: 23164
diff changeset
   182
  val bal_add2 = @{thm nat_eq_add_iff2} RS trans
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   183
);
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   184
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   185
structure LessCancelNumerals = CancelNumeralsFun
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   186
 (open CancelNumeralsCommon
35092
cfe605c54e50 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents: 35064
diff changeset
   187
  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: 35064
diff changeset
   188
  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT
23471
08e6c03b2a72 add thm antiquotations
huffman
parents: 23164
diff changeset
   189
  val bal_add1 = @{thm nat_less_add_iff1} RS trans
08e6c03b2a72 add thm antiquotations
huffman
parents: 23164
diff changeset
   190
  val bal_add2 = @{thm nat_less_add_iff2} RS trans
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   191
);
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   192
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   193
structure LeCancelNumerals = CancelNumeralsFun
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   194
 (open CancelNumeralsCommon
35092
cfe605c54e50 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents: 35064
diff changeset
   195
  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: 35064
diff changeset
   196
  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT
23471
08e6c03b2a72 add thm antiquotations
huffman
parents: 23164
diff changeset
   197
  val bal_add1 = @{thm nat_le_add_iff1} RS trans
08e6c03b2a72 add thm antiquotations
huffman
parents: 23164
diff changeset
   198
  val bal_add2 = @{thm nat_le_add_iff2} RS trans
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   199
);
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   200
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   201
structure DiffCancelNumerals = CancelNumeralsFun
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   202
 (open CancelNumeralsCommon
35267
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35092
diff changeset
   203
  val mk_bal   = HOLogic.mk_binop @{const_name Groups.minus}
8dfd816713c6 moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents: 35092
diff changeset
   204
  val dest_bal = HOLogic.dest_bin @{const_name Groups.minus} HOLogic.natT
23471
08e6c03b2a72 add thm antiquotations
huffman
parents: 23164
diff changeset
   205
  val bal_add1 = @{thm nat_diff_add_eq1} RS trans
08e6c03b2a72 add thm antiquotations
huffman
parents: 23164
diff changeset
   206
  val bal_add2 = @{thm nat_diff_add_eq2} RS trans
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   207
);
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   208
45436
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45306
diff changeset
   209
fun eq_cancel_numerals ss ct = EqCancelNumerals.proc ss (term_of ct)
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45306
diff changeset
   210
fun less_cancel_numerals ss ct = LessCancelNumerals.proc ss (term_of ct)
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45306
diff changeset
   211
fun le_cancel_numerals ss ct = LeCancelNumerals.proc ss (term_of ct)
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45306
diff changeset
   212
fun diff_cancel_numerals ss ct = DiffCancelNumerals.proc ss (term_of ct)
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   213
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   214
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   215
(*** Applying CombineNumeralsFun ***)
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   216
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   217
structure CombineNumeralsData =
44945
haftmann
parents: 40878
diff changeset
   218
struct
haftmann
parents: 40878
diff changeset
   219
  type coeff = int
haftmann
parents: 40878
diff changeset
   220
  val iszero = (fn x => x = 0)
haftmann
parents: 40878
diff changeset
   221
  val add = op +
haftmann
parents: 40878
diff changeset
   222
  val mk_sum = (fn T : typ => long_mk_sum)  (*to work for 2*x + 3*x *)
haftmann
parents: 40878
diff changeset
   223
  val dest_sum = dest_Sucs_sum false
haftmann
parents: 40878
diff changeset
   224
  val mk_coeff = mk_coeff
haftmann
parents: 40878
diff changeset
   225
  val dest_coeff = dest_coeff
haftmann
parents: 40878
diff changeset
   226
  val left_distrib = @{thm left_add_mult_distrib} RS trans
haftmann
parents: 40878
diff changeset
   227
  val prove_conv = Arith_Data.prove_conv_nohyps
44947
8ae418dfe561 dropped unused argument – avoids problem with SML/NJ
haftmann
parents: 44945
diff changeset
   228
  val trans_tac = Numeral_Simprocs.trans_tac
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   229
31790
05c92381363c corrected and unified thm names
nipkow
parents: 31368
diff changeset
   230
  val norm_ss1 = Numeral_Simprocs.num_ss addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_plus1}] @ @{thms add_ac}
31068
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 30685
diff changeset
   231
  val norm_ss2 = Numeral_Simprocs.num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   232
  fun norm_tac ss =
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   233
    ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   234
    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   235
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   236
  val numeral_simp_ss = HOL_ss addsimps add_0s @ bin_simps;
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   237
  fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
44945
haftmann
parents: 40878
diff changeset
   238
  val simplify_meta_eq = simplify_meta_eq
haftmann
parents: 40878
diff changeset
   239
end;
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   240
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   241
structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   242
45462
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45436
diff changeset
   243
fun combine_numerals ss ct = CombineNumerals.proc ss (term_of ct)
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   244
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   245
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   246
(*** Applying CancelNumeralFactorFun ***)
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   247
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   248
structure CancelNumeralFactorCommon =
44945
haftmann
parents: 40878
diff changeset
   249
struct
haftmann
parents: 40878
diff changeset
   250
  val mk_coeff = mk_coeff
haftmann
parents: 40878
diff changeset
   251
  val dest_coeff = dest_coeff
44947
8ae418dfe561 dropped unused argument – avoids problem with SML/NJ
haftmann
parents: 44945
diff changeset
   252
  val trans_tac = Numeral_Simprocs.trans_tac
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   253
31068
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 30685
diff changeset
   254
  val norm_ss1 = Numeral_Simprocs.num_ss addsimps
31790
05c92381363c corrected and unified thm names
nipkow
parents: 31368
diff changeset
   255
    numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_plus1_left}] @ @{thms add_ac}
31068
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 30685
diff changeset
   256
  val norm_ss2 = Numeral_Simprocs.num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   257
  fun norm_tac ss =
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   258
    ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   259
    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   260
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   261
  val numeral_simp_ss = HOL_ss addsimps bin_simps
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   262
  fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
44945
haftmann
parents: 40878
diff changeset
   263
  val simplify_meta_eq = simplify_meta_eq
haftmann
parents: 40878
diff changeset
   264
  val prove_conv = Arith_Data.prove_conv
haftmann
parents: 40878
diff changeset
   265
end;
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   266
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   267
structure DivCancelNumeralFactor = CancelNumeralFactorFun
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   268
 (open CancelNumeralFactorCommon
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   269
  val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   270
  val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.natT
23471
08e6c03b2a72 add thm antiquotations
huffman
parents: 23164
diff changeset
   271
  val cancel = @{thm nat_mult_div_cancel1} RS trans
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   272
  val neg_exchanges = false
44945
haftmann
parents: 40878
diff changeset
   273
);
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   274
23969
ef782bbf2d09 Added cancel simprocs for dvd on nat and int
nipkow
parents: 23881
diff changeset
   275
structure DvdCancelNumeralFactor = CancelNumeralFactorFun
ef782bbf2d09 Added cancel simprocs for dvd on nat and int
nipkow
parents: 23881
diff changeset
   276
 (open CancelNumeralFactorCommon
35050
9f841f20dca6 renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents: 34974
diff changeset
   277
  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: 34974
diff changeset
   278
  val dest_bal = HOLogic.dest_bin @{const_name Rings.dvd} HOLogic.natT
23969
ef782bbf2d09 Added cancel simprocs for dvd on nat and int
nipkow
parents: 23881
diff changeset
   279
  val cancel = @{thm nat_mult_dvd_cancel1} RS trans
ef782bbf2d09 Added cancel simprocs for dvd on nat and int
nipkow
parents: 23881
diff changeset
   280
  val neg_exchanges = false
44945
haftmann
parents: 40878
diff changeset
   281
);
23969
ef782bbf2d09 Added cancel simprocs for dvd on nat and int
nipkow
parents: 23881
diff changeset
   282
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   283
structure EqCancelNumeralFactor = CancelNumeralFactorFun
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   284
 (open CancelNumeralFactorCommon
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   285
  val mk_bal   = HOLogic.mk_eq
38864
4abe644fcea5 formerly unnamed infix equality now named HOL.eq
haftmann
parents: 37388
diff changeset
   286
  val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} HOLogic.natT
23471
08e6c03b2a72 add thm antiquotations
huffman
parents: 23164
diff changeset
   287
  val cancel = @{thm nat_mult_eq_cancel1} RS trans
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   288
  val neg_exchanges = false
44945
haftmann
parents: 40878
diff changeset
   289
);
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   290
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   291
structure LessCancelNumeralFactor = CancelNumeralFactorFun
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   292
 (open CancelNumeralFactorCommon
35092
cfe605c54e50 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents: 35064
diff changeset
   293
  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: 35064
diff changeset
   294
  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT
23471
08e6c03b2a72 add thm antiquotations
huffman
parents: 23164
diff changeset
   295
  val cancel = @{thm nat_mult_less_cancel1} RS trans
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   296
  val neg_exchanges = true
44945
haftmann
parents: 40878
diff changeset
   297
);
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   298
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   299
structure LeCancelNumeralFactor = CancelNumeralFactorFun
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   300
 (open CancelNumeralFactorCommon
35092
cfe605c54e50 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents: 35064
diff changeset
   301
  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: 35064
diff changeset
   302
  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT
23471
08e6c03b2a72 add thm antiquotations
huffman
parents: 23164
diff changeset
   303
  val cancel = @{thm nat_mult_le_cancel1} RS trans
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   304
  val neg_exchanges = true
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   305
)
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   306
45463
9a588a835c1e use simproc_setup for the remaining nat_numeral simprocs
huffman
parents: 45462
diff changeset
   307
fun eq_cancel_numeral_factor ss ct = EqCancelNumeralFactor.proc ss (term_of ct)
9a588a835c1e use simproc_setup for the remaining nat_numeral simprocs
huffman
parents: 45462
diff changeset
   308
fun less_cancel_numeral_factor ss ct = LessCancelNumeralFactor.proc ss (term_of ct)
9a588a835c1e use simproc_setup for the remaining nat_numeral simprocs
huffman
parents: 45462
diff changeset
   309
fun le_cancel_numeral_factor ss ct = LeCancelNumeralFactor.proc ss (term_of ct)
9a588a835c1e use simproc_setup for the remaining nat_numeral simprocs
huffman
parents: 45462
diff changeset
   310
fun div_cancel_numeral_factor ss ct = DivCancelNumeralFactor.proc ss (term_of ct)
9a588a835c1e use simproc_setup for the remaining nat_numeral simprocs
huffman
parents: 45462
diff changeset
   311
fun dvd_cancel_numeral_factor ss ct = DvdCancelNumeralFactor.proc ss (term_of ct)
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   312
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   313
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   314
(*** Applying ExtractCommonTermFun ***)
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   315
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   316
(*this version ALWAYS includes a trailing one*)
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   317
fun long_mk_prod []        = one
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   318
  | long_mk_prod (t :: ts) = mk_times (t, mk_prod ts);
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   319
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   320
(*Find first term that matches u*)
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   321
fun find_first_t past u []         = raise TERM("find_first_t", [])
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   322
  | find_first_t past u (t::terms) =
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   323
        if u aconv t then (rev past @ terms)
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   324
        else find_first_t (t::past) u terms
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   325
        handle TERM _ => find_first_t (t::past) u terms;
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   326
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   327
(** Final simplification for the CancelFactor simprocs **)
30518
07b45c1aa788 moved some generic nonsense to arith_data.ML
haftmann
parents: 30496
diff changeset
   328
val simplify_one = Arith_Data.simplify_meta_eq  
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   329
  [@{thm mult_1_left}, @{thm mult_1_right}, @{thm div_1}, @{thm numeral_1_eq_Suc_0}];
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   330
30649
57753e0ec1d4 1. New cancellation simprocs for common factors in inequations
nipkow
parents: 30518
diff changeset
   331
fun cancel_simplify_meta_eq ss cancel_th th =
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   332
    simplify_one ss (([th, cancel_th]) MRS trans);
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   333
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   334
structure CancelFactorCommon =
44945
haftmann
parents: 40878
diff changeset
   335
struct
haftmann
parents: 40878
diff changeset
   336
  val mk_sum = (fn T : typ => long_mk_prod)
haftmann
parents: 40878
diff changeset
   337
  val dest_sum = dest_prod
haftmann
parents: 40878
diff changeset
   338
  val mk_coeff = mk_coeff
haftmann
parents: 40878
diff changeset
   339
  val dest_coeff = dest_coeff
haftmann
parents: 40878
diff changeset
   340
  val find_first = find_first_t []
44947
8ae418dfe561 dropped unused argument – avoids problem with SML/NJ
haftmann
parents: 44945
diff changeset
   341
  val trans_tac = Numeral_Simprocs.trans_tac
23881
851c74f1bb69 moved class ord from Orderings.thy to HOL.thy
haftmann
parents: 23471
diff changeset
   342
  val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac}
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   343
  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
   344
  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: 44947
diff changeset
   345
  fun mk_eq (a, b) = HOLogic.mk_Trueprop (HOLogic.mk_eq (a, b))
44945
haftmann
parents: 40878
diff changeset
   346
end;
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   347
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   348
structure EqCancelFactor = ExtractCommonTermFun
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   349
 (open CancelFactorCommon
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   350
  val mk_bal   = HOLogic.mk_eq
38864
4abe644fcea5 formerly unnamed infix equality now named HOL.eq
haftmann
parents: 37388
diff changeset
   351
  val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} HOLogic.natT
31368
763f4b0fd579 made SML/NJ happy;
wenzelm
parents: 31068
diff changeset
   352
  fun simp_conv _ _ = SOME @{thm nat_mult_eq_cancel_disj}
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   353
);
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   354
44945
haftmann
parents: 40878
diff changeset
   355
structure LeCancelFactor = ExtractCommonTermFun
haftmann
parents: 40878
diff changeset
   356
 (open CancelFactorCommon
haftmann
parents: 40878
diff changeset
   357
  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
haftmann
parents: 40878
diff changeset
   358
  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT
haftmann
parents: 40878
diff changeset
   359
  fun simp_conv _ _ = SOME @{thm nat_mult_le_cancel_disj}
haftmann
parents: 40878
diff changeset
   360
);
haftmann
parents: 40878
diff changeset
   361
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   362
structure LessCancelFactor = ExtractCommonTermFun
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   363
 (open CancelFactorCommon
35092
cfe605c54e50 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents: 35064
diff changeset
   364
  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: 35064
diff changeset
   365
  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT
31368
763f4b0fd579 made SML/NJ happy;
wenzelm
parents: 31068
diff changeset
   366
  fun simp_conv _ _ = SOME @{thm nat_mult_less_cancel_disj}
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   367
);
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   368
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   369
structure DivideCancelFactor = ExtractCommonTermFun
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   370
 (open CancelFactorCommon
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   371
  val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   372
  val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.natT
31368
763f4b0fd579 made SML/NJ happy;
wenzelm
parents: 31068
diff changeset
   373
  fun simp_conv _ _ = SOME @{thm nat_mult_div_cancel_disj}
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   374
);
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   375
23969
ef782bbf2d09 Added cancel simprocs for dvd on nat and int
nipkow
parents: 23881
diff changeset
   376
structure DvdCancelFactor = ExtractCommonTermFun
ef782bbf2d09 Added cancel simprocs for dvd on nat and int
nipkow
parents: 23881
diff changeset
   377
 (open CancelFactorCommon
35050
9f841f20dca6 renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents: 34974
diff changeset
   378
  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: 34974
diff changeset
   379
  val dest_bal = HOLogic.dest_bin @{const_name Rings.dvd} HOLogic.natT
31368
763f4b0fd579 made SML/NJ happy;
wenzelm
parents: 31068
diff changeset
   380
  fun simp_conv _ _ = SOME @{thm nat_mult_dvd_cancel_disj}
23969
ef782bbf2d09 Added cancel simprocs for dvd on nat and int
nipkow
parents: 23881
diff changeset
   381
);
ef782bbf2d09 Added cancel simprocs for dvd on nat and int
nipkow
parents: 23881
diff changeset
   382
45462
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45436
diff changeset
   383
fun eq_cancel_factor ss ct = EqCancelFactor.proc ss (term_of ct)
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45436
diff changeset
   384
fun less_cancel_factor ss ct = LessCancelFactor.proc ss (term_of ct)
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45436
diff changeset
   385
fun le_cancel_factor ss ct = LeCancelFactor.proc ss (term_of ct)
45463
9a588a835c1e use simproc_setup for the remaining nat_numeral simprocs
huffman
parents: 45462
diff changeset
   386
fun div_cancel_factor ss ct = DivideCancelFactor.proc ss (term_of ct)
45462
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45436
diff changeset
   387
fun dvd_cancel_factor ss ct = DvdCancelFactor.proc ss (term_of ct)
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   388
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   389
end;