src/HOL/Tools/int_factor_simprocs.ML
author huffman
Tue, 09 Dec 2008 20:35:31 -0800
changeset 29038 90f42c138585
parent 28952 15a4b2cf8c34
child 29981 7d0ed261b712
child 30240 5b25fee0362c
permissions -rw-r--r--
use {less,le}_number_of in integer simprocs
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
     1
(*  Title:      HOL/int_factor_simprocs.ML
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
     4
    Copyright   2000  University of Cambridge
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
     5
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
     6
Factor cancellation simprocs for the integers (and for fields).
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
     7
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
     8
This file can't be combined with int_arith1 because it requires IntDiv.thy.
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
     9
*)
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    10
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    11
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    12
(*To quote from Provers/Arith/cancel_numeral_factor.ML:
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    13
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    14
Cancels common coefficients in balanced expressions:
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    15
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    16
     u*#m ~~ u'*#m'  ==  #n*u ~~ #n'*u'
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    17
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    18
where ~~ is an appropriate balancing operation (e.g. =, <=, <, div, /)
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    19
and d = gcd(m,m') and n=m/d and n'=m'/d.
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    20
*)
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    21
29038
90f42c138585 use {less,le}_number_of in integer simprocs
huffman
parents: 28952
diff changeset
    22
val rel_number_of = [@{thm eq_number_of_eq}, @{thm less_number_of}, @{thm le_number_of}];
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    23
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    24
local
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    25
  open Int_Numeral_Simprocs
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    26
in
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    27
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    28
structure CancelNumeralFactorCommon =
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    29
  struct
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    30
  val mk_coeff          = mk_coeff
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    31
  val dest_coeff        = dest_coeff 1
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    32
  val trans_tac         = fn _ => trans_tac
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    33
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    34
  val norm_ss1 = HOL_ss addsimps minus_from_mult_simps @ mult_1s
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    35
  val norm_ss2 = HOL_ss addsimps simps @ mult_minus_simps
23881
851c74f1bb69 moved class ord from Orderings.thy to HOL.thy
haftmann
parents: 23413
diff changeset
    36
  val norm_ss3 = HOL_ss addsimps @{thms mult_ac}
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    37
  fun norm_tac ss =
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    38
    ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    39
    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    40
    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3))
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    41
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    42
  val numeral_simp_ss = HOL_ss addsimps rel_number_of @ simps
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    43
  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
    44
  val simplify_meta_eq = Int_Numeral_Simprocs.simplify_meta_eq
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    45
    [@{thm add_0}, @{thm add_0_right}, @{thm mult_zero_left},
26086
3c243098b64a New simpler representation of numerals, using Bit0 and Bit1 instead of BIT, B0, and B1
huffman
parents: 25481
diff changeset
    46
      @{thm mult_zero_right}, @{thm mult_Bit1}, @{thm mult_1_right}];
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    47
  end
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    48
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    49
(*Version for integer division*)
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    50
structure IntDivCancelNumeralFactor = CancelNumeralFactorFun
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    51
 (open CancelNumeralFactorCommon
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    52
  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    53
  val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    54
  val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.intT
23401
nipkow
parents: 23400
diff changeset
    55
  val cancel = @{thm zdiv_zmult_zmult1} RS trans
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    56
  val neg_exchanges = false
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
(*Version for fields*)
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    60
structure DivideCancelNumeralFactor = CancelNumeralFactorFun
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    61
 (open CancelNumeralFactorCommon
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    62
  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    63
  val mk_bal   = HOLogic.mk_binop @{const_name HOL.divide}
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    64
  val dest_bal = HOLogic.dest_bin @{const_name HOL.divide} Term.dummyT
23413
5caa2710dd5b tuned laws for cancellation in divisions for fields.
nipkow
parents: 23401
diff changeset
    65
  val cancel = @{thm mult_divide_mult_cancel_left} RS trans
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    66
  val neg_exchanges = false
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    67
)
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    68
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    69
structure EqCancelNumeralFactor = CancelNumeralFactorFun
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    70
 (open CancelNumeralFactorCommon
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    71
  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    72
  val mk_bal   = HOLogic.mk_eq
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    73
  val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    74
  val cancel = @{thm mult_cancel_left} RS trans
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    75
  val neg_exchanges = false
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    76
)
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    77
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    78
structure LessCancelNumeralFactor = CancelNumeralFactorFun
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    79
 (open CancelNumeralFactorCommon
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    80
  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
23881
851c74f1bb69 moved class ord from Orderings.thy to HOL.thy
haftmann
parents: 23413
diff changeset
    81
  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
851c74f1bb69 moved class ord from Orderings.thy to HOL.thy
haftmann
parents: 23413
diff changeset
    82
  val dest_bal = HOLogic.dest_bin @{const_name HOL.less} Term.dummyT
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    83
  val cancel = @{thm mult_less_cancel_left} RS trans
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    84
  val neg_exchanges = true
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    85
)
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    86
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    87
structure LeCancelNumeralFactor = CancelNumeralFactorFun
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    88
 (open CancelNumeralFactorCommon
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    89
  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
23881
851c74f1bb69 moved class ord from Orderings.thy to HOL.thy
haftmann
parents: 23413
diff changeset
    90
  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
851c74f1bb69 moved class ord from Orderings.thy to HOL.thy
haftmann
parents: 23413
diff changeset
    91
  val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} Term.dummyT
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    92
  val cancel = @{thm mult_le_cancel_left} RS trans
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    93
  val neg_exchanges = true
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    94
)
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    95
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    96
val cancel_numeral_factors =
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    97
  map Int_Numeral_Base_Simprocs.prep_simproc
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    98
   [("ring_eq_cancel_numeral_factor",
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
    99
     ["(l::'a::{idom,number_ring}) * m = n",
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   100
      "(l::'a::{idom,number_ring}) = m * n"],
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   101
     K EqCancelNumeralFactor.proc),
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   102
    ("ring_less_cancel_numeral_factor",
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   103
     ["(l::'a::{ordered_idom,number_ring}) * m < n",
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   104
      "(l::'a::{ordered_idom,number_ring}) < m * n"],
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   105
     K LessCancelNumeralFactor.proc),
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   106
    ("ring_le_cancel_numeral_factor",
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   107
     ["(l::'a::{ordered_idom,number_ring}) * m <= n",
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   108
      "(l::'a::{ordered_idom,number_ring}) <= m * n"],
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   109
     K LeCancelNumeralFactor.proc),
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   110
    ("int_div_cancel_numeral_factors",
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   111
     ["((l::int) * m) div n", "(l::int) div (m * n)"],
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   112
     K IntDivCancelNumeralFactor.proc),
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   113
    ("divide_cancel_numeral_factor",
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   114
     ["((l::'a::{division_by_zero,field,number_ring}) * m) / n",
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   115
      "(l::'a::{division_by_zero,field,number_ring}) / (m * n)",
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   116
      "((number_of v)::'a::{division_by_zero,field,number_ring}) / (number_of w)"],
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   117
     K DivideCancelNumeralFactor.proc)];
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   118
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   119
(* referenced by rat_arith.ML *)
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   120
val field_cancel_numeral_factors =
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   121
  map Int_Numeral_Base_Simprocs.prep_simproc
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   122
   [("field_eq_cancel_numeral_factor",
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   123
     ["(l::'a::{field,number_ring}) * m = n",
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   124
      "(l::'a::{field,number_ring}) = m * n"],
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   125
     K EqCancelNumeralFactor.proc),
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   126
    ("field_cancel_numeral_factor",
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   127
     ["((l::'a::{division_by_zero,field,number_ring}) * m) / n",
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   128
      "(l::'a::{division_by_zero,field,number_ring}) / (m * n)",
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   129
      "((number_of v)::'a::{division_by_zero,field,number_ring}) / (number_of w)"],
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   130
     K DivideCancelNumeralFactor.proc)]
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   131
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   132
end;
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   133
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   134
Addsimprocs cancel_numeral_factors;
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   135
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   136
(*examples:
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   137
print_depth 22;
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   138
set timing;
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   139
set trace_simp;
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   140
fun test s = (Goal s; by (Simp_tac 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
test "9*x = 12 * (y::int)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   143
test "(9*x) div (12 * (y::int)) = z";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   144
test "9*x < 12 * (y::int)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   145
test "9*x <= 12 * (y::int)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   146
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   147
test "-99*x = 132 * (y::int)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   148
test "(-99*x) div (132 * (y::int)) = z";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   149
test "-99*x < 132 * (y::int)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   150
test "-99*x <= 132 * (y::int)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   151
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   152
test "999*x = -396 * (y::int)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   153
test "(999*x) div (-396 * (y::int)) = z";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   154
test "999*x < -396 * (y::int)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   155
test "999*x <= -396 * (y::int)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   156
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   157
test "-99*x = -81 * (y::int)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   158
test "(-99*x) div (-81 * (y::int)) = z";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   159
test "-99*x <= -81 * (y::int)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   160
test "-99*x < -81 * (y::int)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   161
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   162
test "-2 * x = -1 * (y::int)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   163
test "-2 * x = -(y::int)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   164
test "(-2 * x) div (-1 * (y::int)) = z";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   165
test "-2 * x < -(y::int)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   166
test "-2 * x <= -1 * (y::int)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   167
test "-x < -23 * (y::int)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   168
test "-x <= -23 * (y::int)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   169
*)
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   170
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   171
(*And the same examples for fields such as rat or real:
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   172
test "0 <= (y::rat) * -2";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   173
test "9*x = 12 * (y::rat)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   174
test "(9*x) / (12 * (y::rat)) = z";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   175
test "9*x < 12 * (y::rat)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   176
test "9*x <= 12 * (y::rat)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   177
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   178
test "-99*x = 132 * (y::rat)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   179
test "(-99*x) / (132 * (y::rat)) = z";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   180
test "-99*x < 132 * (y::rat)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   181
test "-99*x <= 132 * (y::rat)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   182
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   183
test "999*x = -396 * (y::rat)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   184
test "(999*x) / (-396 * (y::rat)) = z";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   185
test "999*x < -396 * (y::rat)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   186
test "999*x <= -396 * (y::rat)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   187
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   188
test  "(- ((2::rat) * x) <= 2 * y)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   189
test "-99*x = -81 * (y::rat)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   190
test "(-99*x) / (-81 * (y::rat)) = z";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   191
test "-99*x <= -81 * (y::rat)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   192
test "-99*x < -81 * (y::rat)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   193
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   194
test "-2 * x = -1 * (y::rat)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   195
test "-2 * x = -(y::rat)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   196
test "(-2 * x) / (-1 * (y::rat)) = z";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   197
test "-2 * x < -(y::rat)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   198
test "-2 * x <= -1 * (y::rat)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   199
test "-x < -23 * (y::rat)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   200
test "-x <= -23 * (y::rat)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   201
*)
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   202
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   203
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   204
(** Declarations for ExtractCommonTerm **)
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   205
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   206
local
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   207
  open Int_Numeral_Simprocs
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   208
in
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   209
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   210
(*Find first term that matches u*)
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   211
fun find_first_t past u []         = raise TERM ("find_first_t", [])
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   212
  | find_first_t past u (t::terms) =
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   213
        if u aconv t then (rev past @ terms)
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   214
        else find_first_t (t::past) u terms
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   215
        handle TERM _ => find_first_t (t::past) u terms;
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   216
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   217
(** Final simplification for the CancelFactor simprocs **)
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   218
val simplify_one = Int_Numeral_Simprocs.simplify_meta_eq  
25481
aa16cd919dcc dropped legacy ml bindings
haftmann
parents: 24395
diff changeset
   219
  [@{thm mult_1_left}, @{thm mult_1_right}, @{thm zdiv_1}, @{thm numeral_1_eq_1}];
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   220
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   221
fun cancel_simplify_meta_eq cancel_th ss th =
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   222
    simplify_one ss (([th, cancel_th]) MRS trans);
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   223
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   224
structure CancelFactorCommon =
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   225
  struct
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   226
  val mk_sum            = long_mk_prod
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   227
  val dest_sum          = dest_prod
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   228
  val mk_coeff          = mk_coeff
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   229
  val dest_coeff        = dest_coeff
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   230
  val find_first        = find_first_t []
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   231
  val trans_tac         = fn _ => trans_tac
23881
851c74f1bb69 moved class ord from Orderings.thy to HOL.thy
haftmann
parents: 23413
diff changeset
   232
  val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac}
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   233
  fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   234
  end;
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   235
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   236
(*mult_cancel_left requires a ring with no zero divisors.*)
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   237
structure EqCancelFactor = ExtractCommonTermFun
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   238
 (open CancelFactorCommon
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   239
  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   240
  val mk_bal   = HOLogic.mk_eq
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   241
  val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   242
  val simplify_meta_eq  = cancel_simplify_meta_eq @{thm mult_cancel_left}
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   243
);
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   244
23401
nipkow
parents: 23400
diff changeset
   245
(*zdiv_zmult_zmult1_if is for integer division (div).*)
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   246
structure IntDivCancelFactor = ExtractCommonTermFun
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   247
 (open CancelFactorCommon
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   248
  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   249
  val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   250
  val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.intT
23401
nipkow
parents: 23400
diff changeset
   251
  val simplify_meta_eq  = cancel_simplify_meta_eq @{thm zdiv_zmult_zmult1_if}
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   252
);
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   253
24395
8df021f79e0b Added mod cancellation simproc
nipkow
parents: 23969
diff changeset
   254
structure IntModCancelFactor = ExtractCommonTermFun
8df021f79e0b Added mod cancellation simproc
nipkow
parents: 23969
diff changeset
   255
 (open CancelFactorCommon
8df021f79e0b Added mod cancellation simproc
nipkow
parents: 23969
diff changeset
   256
  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
8df021f79e0b Added mod cancellation simproc
nipkow
parents: 23969
diff changeset
   257
  val mk_bal   = HOLogic.mk_binop @{const_name Divides.mod}
8df021f79e0b Added mod cancellation simproc
nipkow
parents: 23969
diff changeset
   258
  val dest_bal = HOLogic.dest_bin @{const_name Divides.mod} HOLogic.intT
8df021f79e0b Added mod cancellation simproc
nipkow
parents: 23969
diff changeset
   259
  val simplify_meta_eq  = cancel_simplify_meta_eq @{thm zmod_zmult_zmult1}
8df021f79e0b Added mod cancellation simproc
nipkow
parents: 23969
diff changeset
   260
);
8df021f79e0b Added mod cancellation simproc
nipkow
parents: 23969
diff changeset
   261
23969
ef782bbf2d09 Added cancel simprocs for dvd on nat and int
nipkow
parents: 23881
diff changeset
   262
structure IntDvdCancelFactor = ExtractCommonTermFun
ef782bbf2d09 Added cancel simprocs for dvd on nat and int
nipkow
parents: 23881
diff changeset
   263
 (open CancelFactorCommon
ef782bbf2d09 Added cancel simprocs for dvd on nat and int
nipkow
parents: 23881
diff changeset
   264
  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: 26086
diff changeset
   265
  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: 26086
diff changeset
   266
  val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} HOLogic.intT
23969
ef782bbf2d09 Added cancel simprocs for dvd on nat and int
nipkow
parents: 23881
diff changeset
   267
  val simplify_meta_eq  = cancel_simplify_meta_eq @{thm zdvd_zmult_cancel_disj}
ef782bbf2d09 Added cancel simprocs for dvd on nat and int
nipkow
parents: 23881
diff changeset
   268
);
ef782bbf2d09 Added cancel simprocs for dvd on nat and int
nipkow
parents: 23881
diff changeset
   269
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   270
(*Version for all fields, including unordered ones (type complex).*)
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   271
structure DivideCancelFactor = ExtractCommonTermFun
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   272
 (open CancelFactorCommon
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   273
  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   274
  val mk_bal   = HOLogic.mk_binop @{const_name HOL.divide}
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   275
  val dest_bal = HOLogic.dest_bin @{const_name HOL.divide} Term.dummyT
23413
5caa2710dd5b tuned laws for cancellation in divisions for fields.
nipkow
parents: 23401
diff changeset
   276
  val simplify_meta_eq  = cancel_simplify_meta_eq @{thm mult_divide_mult_cancel_left_if}
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   277
);
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   278
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   279
val cancel_factors =
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   280
  map Int_Numeral_Base_Simprocs.prep_simproc
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   281
   [("ring_eq_cancel_factor",
23400
a64b39e5809b The simprocs "divide_cancel_factor" and "ring_eq_cancel_factor" no
nipkow
parents: 23398
diff changeset
   282
     ["(l::'a::{idom}) * m = n",
a64b39e5809b The simprocs "divide_cancel_factor" and "ring_eq_cancel_factor" no
nipkow
parents: 23398
diff changeset
   283
      "(l::'a::{idom}) = m * n"],
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   284
    K EqCancelFactor.proc),
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   285
    ("int_div_cancel_factor",
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   286
     ["((l::int) * m) div n", "(l::int) div (m * n)"],
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   287
     K IntDivCancelFactor.proc),
24395
8df021f79e0b Added mod cancellation simproc
nipkow
parents: 23969
diff changeset
   288
    ("int_mod_cancel_factor",
8df021f79e0b Added mod cancellation simproc
nipkow
parents: 23969
diff changeset
   289
     ["((l::int) * m) mod n", "(l::int) mod (m * n)"],
8df021f79e0b Added mod cancellation simproc
nipkow
parents: 23969
diff changeset
   290
     K IntModCancelFactor.proc),
23969
ef782bbf2d09 Added cancel simprocs for dvd on nat and int
nipkow
parents: 23881
diff changeset
   291
    ("int_dvd_cancel_factor",
ef782bbf2d09 Added cancel simprocs for dvd on nat and int
nipkow
parents: 23881
diff changeset
   292
     ["((l::int) * m) dvd n", "(l::int) dvd (m * n)"],
ef782bbf2d09 Added cancel simprocs for dvd on nat and int
nipkow
parents: 23881
diff changeset
   293
     K IntDvdCancelFactor.proc),
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   294
    ("divide_cancel_factor",
23400
a64b39e5809b The simprocs "divide_cancel_factor" and "ring_eq_cancel_factor" no
nipkow
parents: 23398
diff changeset
   295
     ["((l::'a::{division_by_zero,field}) * m) / n",
a64b39e5809b The simprocs "divide_cancel_factor" and "ring_eq_cancel_factor" no
nipkow
parents: 23398
diff changeset
   296
      "(l::'a::{division_by_zero,field}) / (m * n)"],
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   297
     K DivideCancelFactor.proc)];
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   298
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   299
end;
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   300
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   301
Addsimprocs cancel_factors;
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   302
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   303
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   304
(*examples:
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   305
print_depth 22;
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   306
set timing;
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   307
set trace_simp;
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   308
fun test s = (Goal s; by (Asm_simp_tac 1));
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   309
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   310
test "x*k = k*(y::int)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   311
test "k = k*(y::int)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   312
test "a*(b*c) = (b::int)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   313
test "a*(b*c) = d*(b::int)*(x*a)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   314
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   315
test "(x*k) div (k*(y::int)) = (uu::int)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   316
test "(k) div (k*(y::int)) = (uu::int)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   317
test "(a*(b*c)) div ((b::int)) = (uu::int)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   318
test "(a*(b*c)) div (d*(b::int)*(x*a)) = (uu::int)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   319
*)
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   320
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   321
(*And the same examples for fields such as rat or real:
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   322
print_depth 22;
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   323
set timing;
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   324
set trace_simp;
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   325
fun test s = (Goal s; by (Asm_simp_tac 1));
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   326
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   327
test "x*k = k*(y::rat)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   328
test "k = k*(y::rat)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   329
test "a*(b*c) = (b::rat)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   330
test "a*(b*c) = d*(b::rat)*(x*a)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   331
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   332
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   333
test "(x*k) / (k*(y::rat)) = (uu::rat)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   334
test "(k) / (k*(y::rat)) = (uu::rat)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   335
test "(a*(b*c)) / ((b::rat)) = (uu::rat)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   336
test "(a*(b*c)) / (d*(b::rat)*(x*a)) = (uu::rat)";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   337
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   338
(*FIXME: what do we do about this?*)
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   339
test "a*(b*c)/(y*z) = d*(b::rat)*(x*a)/z";
69e55066dbca moved Integ files to canonical place;
wenzelm
parents:
diff changeset
   340
*)