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