Mercurial Mercurial > repos > isabelle / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/ex/Simproc_Tests.thy
changeset 45284 ae78a4ffa81d
parent 45270 d5b5c9259afd
child 45285 299abd2931d5
equal deleted inserted replaced
45283:9e8616978d99 45284:ae78a4ffa81d 
    16 *}
 
    16 *}
 
    17 
    17 
    18 subsection {* ML bindings *}
 
    18 subsection {* ML bindings *}
 
    19 
    19 
    20 ML {*
 
    20 ML {*
 
    21   val semiring_assoc_fold = Numeral_Simprocs.assoc_fold_simproc
 
       
    22   val int_combine_numerals = Numeral_Simprocs.combine_numerals
 
       
    23   val field_combine_numerals = Numeral_Simprocs.field_combine_numerals
 
       
    24   val [inteq_cancel_numerals, intless_cancel_numerals, intle_cancel_numerals]
 
       
    25     = Numeral_Simprocs.cancel_numerals
 
       
    26   val [ring_eq_cancel_factor, linordered_ring_le_cancel_factor,
 
       
    27       linordered_ring_less_cancel_factor, int_div_cancel_factor,
 
       
    28       int_mod_cancel_factor, dvd_cancel_factor, divide_cancel_factor]
 
       
    29     = Numeral_Simprocs.cancel_factors
 
       
    30   val [ring_eq_cancel_numeral_factor, ring_less_cancel_numeral_factor,
 
       
    31       ring_le_cancel_numeral_factor, int_div_cancel_numeral_factors,
 
       
    32       divide_cancel_numeral_factor]
 
       
    33     = Numeral_Simprocs.cancel_numeral_factors
 
       
    34   val field_combine_numerals = Numeral_Simprocs.field_combine_numerals
 
       
    35   val [field_eq_cancel_numeral_factor, field_cancel_numeral_factor]
 
    21   val [field_eq_cancel_numeral_factor, field_cancel_numeral_factor]
 
    36     = Numeral_Simprocs.field_cancel_numeral_factors
 
    22     = Numeral_Simprocs.field_cancel_numeral_factors
 
    37 
    23 
    38   fun test ps = CHANGED (asm_simp_tac (HOL_basic_ss addsimprocs ps) 1)
 
    24   fun test ps = CHANGED (asm_simp_tac (HOL_basic_ss addsimprocs ps) 1)
 
    39 *}
 
    25 *}
 
    41 
    27 
    42 subsection {* @{text int_combine_numerals} *}
 
    28 subsection {* @{text int_combine_numerals} *}
 
    43 
    29 
    44 lemma assumes "10 + (2 * l + oo) = uu"
 
    30 lemma assumes "10 + (2 * l + oo) = uu"
 
    45   shows "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::int)"
 
    31   shows "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::int)"
 
    46 by (tactic {* test [int_combine_numerals] *}) fact
 
    32 by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
 
    47 
    33 
    48 lemma assumes "-3 + (i + (j + k)) = y"
 
    34 lemma assumes "-3 + (i + (j + k)) = y"
 
    49   shows "(i + j + 12 + (k::int)) - 15 = y"
 
    35   shows "(i + j + 12 + (k::int)) - 15 = y"
 
    50 by (tactic {* test [int_combine_numerals] *}) fact
 
    36 by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
 
    51 
    37 
    52 lemma assumes "7 + (i + (j + k)) = y"
 
    38 lemma assumes "7 + (i + (j + k)) = y"
 
    53   shows "(i + j + 12 + (k::int)) - 5 = y"
 
    39   shows "(i + j + 12 + (k::int)) - 5 = y"
 
    54 by (tactic {* test [int_combine_numerals] *}) fact
 
    40 by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
 
    55 
    41 
    56 lemma assumes "-4 * (u * v) + (2 * x + y) = w"
 
    42 lemma assumes "-4 * (u * v) + (2 * x + y) = w"
 
    57   shows "(2*x - (u*v) + y) - v*3*u = (w::int)"
 
    43   shows "(2*x - (u*v) + y) - v*3*u = (w::int)"
 
    58 by (tactic {* test [int_combine_numerals] *}) fact
 
    44 by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
 
    59 
    45 
    60 lemma assumes "Numeral0 * (u*v) + (2 * x * u * v + y) = w"
 
    46 lemma assumes "Numeral0 * (u*v) + (2 * x * u * v + y) = w"
 
    61   shows "(2*x*u*v + (u*v)*4 + y) - v*u*4 = (w::int)"
 
    47   shows "(2*x*u*v + (u*v)*4 + y) - v*u*4 = (w::int)"
 
    62 by (tactic {* test [int_combine_numerals] *}) fact
 
    48 by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
 
    63 
    49 
    64 lemma assumes "3 * (u * v) + (2 * x * u * v + y) = w"
 
    50 lemma assumes "3 * (u * v) + (2 * x * u * v + y) = w"
 
    65   shows "(2*x*u*v + (u*v)*4 + y) - v*u = (w::int)"
 
    51   shows "(2*x*u*v + (u*v)*4 + y) - v*u = (w::int)"
 
    66 by (tactic {* test [int_combine_numerals] *}) fact
 
    52 by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
 
    67 
    53 
    68 lemma assumes "-3 * (u * v) + (- (x * u * v) + - y) = w"
 
    54 lemma assumes "-3 * (u * v) + (- (x * u * v) + - y) = w"
 
    69   shows "u*v - (x*u*v + (u*v)*4 + y) = (w::int)"
 
    55   shows "u*v - (x*u*v + (u*v)*4 + y) = (w::int)"
 
    70 by (tactic {* test [int_combine_numerals] *}) fact
 
    56 by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
 
    71 
    57 
    72 lemma assumes "Numeral0 * b + (a + - c) = d"
 
    58 lemma assumes "Numeral0 * b + (a + - c) = d"
 
    73   shows "a + -(b+c) + b = (d::int)"
 
    59   shows "a + -(b+c) + b = (d::int)"
 
    74 apply (simp only: minus_add_distrib)
 
    60 apply (simp only: minus_add_distrib)
 
    75 by (tactic {* test [int_combine_numerals] *}) fact
 
    61 by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
 
    76 
    62 
    77 lemma assumes "-2 * b + (a + - c) = d"
 
    63 lemma assumes "-2 * b + (a + - c) = d"
 
    78   shows "a + -(b+c) - b = (d::int)"
 
    64   shows "a + -(b+c) - b = (d::int)"
 
    79 apply (simp only: minus_add_distrib)
 
    65 apply (simp only: minus_add_distrib)
 
    80 by (tactic {* test [int_combine_numerals] *}) fact
 
    66 by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
 
    81 
    67 
    82 lemma assumes "-7 + (i + (j + (k + (- u + - y)))) = zz"
 
    68 lemma assumes "-7 + (i + (j + (k + (- u + - y)))) = zz"
 
    83   shows "(i + j + -2 + (k::int)) - (u + 5 + y) = zz"
 
    69   shows "(i + j + -2 + (k::int)) - (u + 5 + y) = zz"
 
    84 by (tactic {* test [int_combine_numerals] *}) fact
 
    70 by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
 
    85 
    71 
    86 lemma assumes "-27 + (i + (j + k)) = y"
 
    72 lemma assumes "-27 + (i + (j + k)) = y"
 
    87   shows "(i + j + -12 + (k::int)) - 15 = y"
 
    73   shows "(i + j + -12 + (k::int)) - 15 = y"
 
    88 by (tactic {* test [int_combine_numerals] *}) fact
 
    74 by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
 
    89 
    75 
    90 lemma assumes "27 + (i + (j + k)) = y"
 
    76 lemma assumes "27 + (i + (j + k)) = y"
 
    91   shows "(i + j + 12 + (k::int)) - -15 = y"
 
    77   shows "(i + j + 12 + (k::int)) - -15 = y"
 
    92 by (tactic {* test [int_combine_numerals] *}) fact
 
    78 by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
 
    93 
    79 
    94 lemma assumes "3 + (i + (j + k)) = y"
 
    80 lemma assumes "3 + (i + (j + k)) = y"
 
    95   shows "(i + j + -12 + (k::int)) - -15 = y"
 
    81   shows "(i + j + -12 + (k::int)) - -15 = y"
 
    96 by (tactic {* test [int_combine_numerals] *}) fact
 
    82 by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
 
    97 
    83 
    98 
    84 
    99 subsection {* @{text inteq_cancel_numerals} *}
 
    85 subsection {* @{text inteq_cancel_numerals} *}
 
   100 
    86 
   101 lemma assumes "u = Numeral0" shows "2*u = (u::int)"
 
    87 lemma assumes "u = Numeral0" shows "2*u = (u::int)"
 
   102 by (tactic {* test [inteq_cancel_numerals] *}) fact
 
    88 by (tactic {* test [@{simproc inteq_cancel_numerals}] *}) fact
 
   103 (* conclusion matches Rings.ring_1_no_zero_divisors_class.mult_cancel_right2 *)
 
    89 (* conclusion matches Rings.ring_1_no_zero_divisors_class.mult_cancel_right2 *)
 
   104 
    90 
   105 lemma assumes "i + (j + k) = 3 + (u + y)"
 
    91 lemma assumes "i + (j + k) = 3 + (u + y)"
 
   106   shows "(i + j + 12 + (k::int)) = u + 15 + y"
 
    92   shows "(i + j + 12 + (k::int)) = u + 15 + y"
 
   107 by (tactic {* test [inteq_cancel_numerals] *}) fact
 
    93 by (tactic {* test [@{simproc inteq_cancel_numerals}] *}) fact
 
   108 
    94 
   109 lemma assumes "7 + (j + (i + k)) = y"
 
    95 lemma assumes "7 + (j + (i + k)) = y"
 
   110   shows "(i + j*2 + 12 + (k::int)) = j + 5 + y"
 
    96   shows "(i + j*2 + 12 + (k::int)) = j + 5 + y"
 
   111 by (tactic {* test [inteq_cancel_numerals] *}) fact
 
    97 by (tactic {* test [@{simproc inteq_cancel_numerals}] *}) fact
 
   112 
    98 
   113 lemma assumes "u + (6*z + (4*y + 6*w)) = 6*z' + (4*y' + (6*w' + vv))"
 
    99 lemma assumes "u + (6*z + (4*y + 6*w)) = 6*z' + (4*y' + (6*w' + vv))"
 
   114   shows "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = 2*y' + 3*z' + 6*w' + 2*y' + 3*z' + u + (vv::int)"
 
   100   shows "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = 2*y' + 3*z' + 6*w' + 2*y' + 3*z' + u + (vv::int)"
 
   115 by (tactic {* test [int_combine_numerals, inteq_cancel_numerals] *}) fact
 
   101 by (tactic {* test [@{simproc int_combine_numerals}, @{simproc inteq_cancel_numerals}] *}) fact
 
   116 
   102 
   117 
   103 
   118 subsection {* @{text intless_cancel_numerals} *}
 
   104 subsection {* @{text intless_cancel_numerals} *}
 
   119 
   105 
   120 lemma assumes "y < 2 * b" shows "y - b < (b::int)"
 
   106 lemma assumes "y < 2 * b" shows "y - b < (b::int)"
 
   121 by (tactic {* test [intless_cancel_numerals] *}) fact
 
   107 by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact
 
   122 
   108 
   123 lemma assumes "c + y < 4 * b" shows "y - (3*b + c) < (b::int) - 2*c"
 
   109 lemma assumes "c + y < 4 * b" shows "y - (3*b + c) < (b::int) - 2*c"
 
   124 by (tactic {* test [intless_cancel_numerals] *}) fact
 
   110 by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact
 
   125 
   111 
   126 lemma assumes "i + (j + k) < 8 + (u + y)"
 
   112 lemma assumes "i + (j + k) < 8 + (u + y)"
 
   127   shows "(i + j + -3 + (k::int)) < u + 5 + y"
 
   113   shows "(i + j + -3 + (k::int)) < u + 5 + y"
 
   128 by (tactic {* test [intless_cancel_numerals] *}) fact
 
   114 by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact
 
   129 
   115 
   130 lemma assumes "9 + (i + (j + k)) < u + y"
 
   116 lemma assumes "9 + (i + (j + k)) < u + y"
 
   131   shows "(i + j + 3 + (k::int)) < u + -6 + y"
 
   117   shows "(i + j + 3 + (k::int)) < u + -6 + y"
 
   132 by (tactic {* test [intless_cancel_numerals] *}) fact
 
   118 by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact
 
   133 
   119 
   134 
   120 
   135 subsection {* @{text ring_eq_cancel_numeral_factor} *}
 
   121 subsection {* @{text ring_eq_cancel_numeral_factor} *}
 
   136 
   122 
   137 lemma assumes "3*x = 4*y" shows "9*x = 12 * (y::int)"
 
   123 lemma assumes "3*x = 4*y" shows "9*x = 12 * (y::int)"
 
   138 by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact
 
   124 by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
 
   139 
   125 
   140 lemma assumes "-3*x = 4*y" shows "-99*x = 132 * (y::int)"
 
   126 lemma assumes "-3*x = 4*y" shows "-99*x = 132 * (y::int)"
 
   141 by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact
 
   127 by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
 
   142 
   128 
   143 
   129 
   144 subsection {* @{text int_div_cancel_numeral_factors} *}
 
   130 subsection {* @{text int_div_cancel_numeral_factors} *}
 
   145 
   131 
   146 lemma assumes "(3*x) div (4*y) = z" shows "(9*x) div (12*y) = (z::int)"
 
   132 lemma assumes "(3*x) div (4*y) = z" shows "(9*x) div (12*y) = (z::int)"
 
   147 by (tactic {* test [int_div_cancel_numeral_factors] *}) fact
 
   133 by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact
 
   148 
   134 
   149 lemma assumes "(-3*x) div (4*y) = z" shows "(-99*x) div (132*y) = (z::int)"
 
   135 lemma assumes "(-3*x) div (4*y) = z" shows "(-99*x) div (132*y) = (z::int)"
 
   150 by (tactic {* test [int_div_cancel_numeral_factors] *}) fact
 
   136 by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact
 
   151 
   137 
   152 lemma assumes "(111*x) div (-44*y) = z" shows "(999*x) div (-396*y) = (z::int)"
 
   138 lemma assumes "(111*x) div (-44*y) = z" shows "(999*x) div (-396*y) = (z::int)"
 
   153 by (tactic {* test [int_div_cancel_numeral_factors] *}) fact
 
   139 by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact
 
   154 
   140 
   155 lemma assumes "(11*x) div (9*y) = z" shows "(-99*x) div (-81*y) = (z::int)"
 
   141 lemma assumes "(11*x) div (9*y) = z" shows "(-99*x) div (-81*y) = (z::int)"
 
   156 by (tactic {* test [int_div_cancel_numeral_factors] *}) fact
 
   142 by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact
 
   157 
   143 
   158 lemma assumes "(2*x) div (Numeral1*y) = z"
 
   144 lemma assumes "(2*x) div (Numeral1*y) = z"
 
   159   shows "(-2 * x) div (-1 * (y::int)) = z"
 
   145   shows "(-2 * x) div (-1 * (y::int)) = z"
 
   160 by (tactic {* test [int_div_cancel_numeral_factors] *}) fact
 
   146 by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact
 
   161 
   147 
   162 
   148 
   163 subsection {* @{text ring_less_cancel_numeral_factor} *}
 
   149 subsection {* @{text ring_less_cancel_numeral_factor} *}
 
   164 
   150 
   165 lemma assumes "3*x < 4*y" shows "9*x < 12 * (y::int)"
 
   151 lemma assumes "3*x < 4*y" shows "9*x < 12 * (y::int)"
 
   166 by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact
 
   152 by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
 
   167 
   153 
   168 lemma assumes "-3*x < 4*y" shows "-99*x < 132 * (y::int)"
 
   154 lemma assumes "-3*x < 4*y" shows "-99*x < 132 * (y::int)"
 
   169 by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact
 
   155 by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
 
   170 
   156 
   171 lemma assumes "111*x < -44*y" shows "999*x < -396 * (y::int)"
 
   157 lemma assumes "111*x < -44*y" shows "999*x < -396 * (y::int)"
 
   172 by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact
 
   158 by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
 
   173 
   159 
   174 lemma assumes "9*y < 11*x" shows "-99*x < -81 * (y::int)"
 
   160 lemma assumes "9*y < 11*x" shows "-99*x < -81 * (y::int)"
 
   175 by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact
 
   161 by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
 
   176 
   162 
   177 lemma assumes "Numeral1*y < 2*x" shows "-2 * x < -(y::int)"
 
   163 lemma assumes "Numeral1*y < 2*x" shows "-2 * x < -(y::int)"
 
   178 by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact
 
   164 by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
 
   179 
   165 
   180 lemma assumes "23*y < Numeral1*x" shows "-x < -23 * (y::int)"
 
   166 lemma assumes "23*y < Numeral1*x" shows "-x < -23 * (y::int)"
 
   181 by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact
 
   167 by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
 
   182 
   168 
   183 lemma assumes "3*x < 4*y" shows "9*x < 12 * (y::rat)"
 
   169 lemma assumes "3*x < 4*y" shows "9*x < 12 * (y::rat)"
 
   184 by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact
 
   170 by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
 
   185 
   171 
   186 lemma assumes "-3*x < 4*y" shows "-99*x < 132 * (y::rat)"
 
   172 lemma assumes "-3*x < 4*y" shows "-99*x < 132 * (y::rat)"
 
   187 by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact
 
   173 by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
 
   188 
   174 
   189 lemma assumes "111*x < -44*y" shows "999*x < -396 * (y::rat)"
 
   175 lemma assumes "111*x < -44*y" shows "999*x < -396 * (y::rat)"
 
   190 by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact
 
   176 by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
 
   191 
   177 
   192 lemma assumes "9*y < 11*x" shows "-99*x < -81 * (y::rat)"
 
   178 lemma assumes "9*y < 11*x" shows "-99*x < -81 * (y::rat)"
 
   193 by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact
 
   179 by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
 
   194 
   180 
   195 lemma assumes "Numeral1*y < 2*x" shows "-2 * x < -(y::rat)"
 
   181 lemma assumes "Numeral1*y < 2*x" shows "-2 * x < -(y::rat)"
 
   196 by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact
 
   182 by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
 
   197 
   183 
   198 lemma assumes "23*y < Numeral1*x" shows "-x < -23 * (y::rat)"
 
   184 lemma assumes "23*y < Numeral1*x" shows "-x < -23 * (y::rat)"
 
   199 by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact
 
   185 by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
 
   200 
   186 
   201 
   187 
   202 subsection {* @{text ring_le_cancel_numeral_factor} *}
 
   188 subsection {* @{text ring_le_cancel_numeral_factor} *}
 
   203 
   189 
   204 lemma assumes "3*x \<le> 4*y" shows "9*x \<le> 12 * (y::int)"
 
   190 lemma assumes "3*x \<le> 4*y" shows "9*x \<le> 12 * (y::int)"
 
   205 by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
 
   191 by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
 
   206 
   192 
   207 lemma assumes "-3*x \<le> 4*y" shows "-99*x \<le> 132 * (y::int)"
 
   193 lemma assumes "-3*x \<le> 4*y" shows "-99*x \<le> 132 * (y::int)"
 
   208 by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
 
   194 by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
 
   209 
   195 
   210 lemma assumes "111*x \<le> -44*y" shows "999*x \<le> -396 * (y::int)"
 
   196 lemma assumes "111*x \<le> -44*y" shows "999*x \<le> -396 * (y::int)"
 
   211 by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
 
   197 by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
 
   212 
   198 
   213 lemma assumes "9*y \<le> 11*x" shows "-99*x \<le> -81 * (y::int)"
 
   199 lemma assumes "9*y \<le> 11*x" shows "-99*x \<le> -81 * (y::int)"
 
   214 by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
 
   200 by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
 
   215 
   201 
   216 lemma assumes "Numeral1*y \<le> 2*x" shows "-2 * x \<le> -1 * (y::int)"
 
   202 lemma assumes "Numeral1*y \<le> 2*x" shows "-2 * x \<le> -1 * (y::int)"
 
   217 by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
 
   203 by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
 
   218 
   204 
   219 lemma assumes "23*y \<le> Numeral1*x" shows "-x \<le> -23 * (y::int)"
 
   205 lemma assumes "23*y \<le> Numeral1*x" shows "-x \<le> -23 * (y::int)"
 
   220 by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
 
   206 by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
 
   221 
   207 
   222 lemma assumes "Numeral1*y \<le> Numeral0" shows "0 \<le> (y::rat) * -2"
 
   208 lemma assumes "Numeral1*y \<le> Numeral0" shows "0 \<le> (y::rat) * -2"
 
   223 by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
 
   209 by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
 
   224 
   210 
   225 lemma assumes "3*x \<le> 4*y" shows "9*x \<le> 12 * (y::rat)"
 
   211 lemma assumes "3*x \<le> 4*y" shows "9*x \<le> 12 * (y::rat)"
 
   226 by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
 
   212 by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
 
   227 
   213 
   228 lemma assumes "-3*x \<le> 4*y" shows "-99*x \<le> 132 * (y::rat)"
 
   214 lemma assumes "-3*x \<le> 4*y" shows "-99*x \<le> 132 * (y::rat)"
 
   229 by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
 
   215 by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
 
   230 
   216 
   231 lemma assumes "111*x \<le> -44*y" shows "999*x \<le> -396 * (y::rat)"
 
   217 lemma assumes "111*x \<le> -44*y" shows "999*x \<le> -396 * (y::rat)"
 
   232 by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
 
   218 by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
 
   233 
   219 
   234 lemma assumes "-1*x \<le> Numeral1*y" shows "- ((2::rat) * x) \<le> 2*y"
 
   220 lemma assumes "-1*x \<le> Numeral1*y" shows "- ((2::rat) * x) \<le> 2*y"
 
   235 by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
 
   221 by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
 
   236 
   222 
   237 lemma assumes "9*y \<le> 11*x" shows "-99*x \<le> -81 * (y::rat)"
 
   223 lemma assumes "9*y \<le> 11*x" shows "-99*x \<le> -81 * (y::rat)"
 
   238 by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
 
   224 by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
 
   239 
   225 
   240 lemma assumes "Numeral1*y \<le> 2*x" shows "-2 * x \<le> -1 * (y::rat)"
 
   226 lemma assumes "Numeral1*y \<le> 2*x" shows "-2 * x \<le> -1 * (y::rat)"
 
   241 by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
 
   227 by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
 
   242 
   228 
   243 lemma assumes "23*y \<le> Numeral1*x" shows "-x \<le> -23 * (y::rat)"
 
   229 lemma assumes "23*y \<le> Numeral1*x" shows "-x \<le> -23 * (y::rat)"
 
   244 by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
 
   230 by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
 
   245 
   231 
   246 
   232 
   247 subsection {* @{text ring_eq_cancel_numeral_factor} *}
 
   233 subsection {* @{text ring_eq_cancel_numeral_factor} *}
 
   248 
   234 
   249 lemma assumes "111*x = -44*y" shows "999*x = -396 * (y::int)"
 
   235 lemma assumes "111*x = -44*y" shows "999*x = -396 * (y::int)"
 
   250 by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact
 
   236 by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
 
   251 
   237 
   252 lemma assumes "11*x = 9*y" shows "-99*x = -81 * (y::int)"
 
   238 lemma assumes "11*x = 9*y" shows "-99*x = -81 * (y::int)"
 
   253 by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact
 
   239 by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
 
   254 
   240 
   255 lemma assumes "2*x = Numeral1*y" shows "-2 * x = -1 * (y::int)"
 
   241 lemma assumes "2*x = Numeral1*y" shows "-2 * x = -1 * (y::int)"
 
   256 by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact
 
   242 by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
 
   257 
   243 
   258 lemma assumes "2*x = Numeral1*y" shows "-2 * x = -(y::int)"
 
   244 lemma assumes "2*x = Numeral1*y" shows "-2 * x = -(y::int)"
 
   259 by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact
 
   245 by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
 
   260 
   246 
   261 lemma assumes "3*x = 4*y" shows "9*x = 12 * (y::rat)"
 
   247 lemma assumes "3*x = 4*y" shows "9*x = 12 * (y::rat)"
 
   262 by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact
 
   248 by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
 
   263 
   249 
   264 lemma assumes "-3*x = 4*y" shows "-99*x = 132 * (y::rat)"
 
   250 lemma assumes "-3*x = 4*y" shows "-99*x = 132 * (y::rat)"
 
   265 by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact
 
   251 by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
 
   266 
   252 
   267 lemma assumes "111*x = -44*y" shows "999*x = -396 * (y::rat)"
 
   253 lemma assumes "111*x = -44*y" shows "999*x = -396 * (y::rat)"
 
   268 by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact
 
   254 by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
 
   269 
   255 
   270 lemma assumes "11*x = 9*y" shows "-99*x = -81 * (y::rat)"
 
   256 lemma assumes "11*x = 9*y" shows "-99*x = -81 * (y::rat)"
 
   271 by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact
 
   257 by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
 
   272 
   258 
   273 lemma assumes "2*x = Numeral1*y" shows "-2 * x = -1 * (y::rat)"
 
   259 lemma assumes "2*x = Numeral1*y" shows "-2 * x = -1 * (y::rat)"
 
   274 by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact
 
   260 by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
 
   275 
   261 
   276 lemma assumes "2*x = Numeral1*y" shows "-2 * x = -(y::rat)"
 
   262 lemma assumes "2*x = Numeral1*y" shows "-2 * x = -(y::rat)"
 
   277 by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact
 
   263 by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
 
   278 
   264 
   279 
   265 
   280 subsection {* @{text field_cancel_numeral_factor} *}
 
   266 subsection {* @{text field_cancel_numeral_factor} *}
 
   281 
   267 
   282 lemma assumes "(3*x) / (4*y) = z" shows "(9*x) / (12 * (y::rat)) = z"
 
   268 lemma assumes "(3*x) / (4*y) = z" shows "(9*x) / (12 * (y::rat)) = z"
 
   296 
   282 
   297 
   283 
   298 subsection {* @{text ring_eq_cancel_factor} *}
 
   284 subsection {* @{text ring_eq_cancel_factor} *}
 
   299 
   285 
   300 lemma assumes "k = 0 \<or> x = y" shows "x*k = k*(y::int)"
 
   286 lemma assumes "k = 0 \<or> x = y" shows "x*k = k*(y::int)"
 
   301 by (tactic {* test [ring_eq_cancel_factor] *}) fact
 
   287 by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
 
   302 
   288 
   303 lemma assumes "k = 0 \<or> 1 = y" shows "k = k*(y::int)"
 
   289 lemma assumes "k = 0 \<or> 1 = y" shows "k = k*(y::int)"
 
   304 by (tactic {* test [ring_eq_cancel_factor] *}) fact
 
   290 by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
 
   305 
   291 
   306 lemma assumes "b = 0 \<or> a*c = 1" shows "a*(b*c) = (b::int)"
 
   292 lemma assumes "b = 0 \<or> a*c = 1" shows "a*(b*c) = (b::int)"
 
   307 by (tactic {* test [ring_eq_cancel_factor] *}) fact
 
   293 by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
 
   308 
   294 
   309 lemma assumes "a = 0 \<or> b = 0 \<or> c = d*x" shows "a*(b*c) = d*(b::int)*(x*a)"
 
   295 lemma assumes "a = 0 \<or> b = 0 \<or> c = d*x" shows "a*(b*c) = d*(b::int)*(x*a)"
 
   310 by (tactic {* test [ring_eq_cancel_factor] *}) fact
 
   296 by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
 
   311 
   297 
   312 lemma assumes "k = 0 \<or> x = y" shows "x*k = k*(y::rat)"
 
   298 lemma assumes "k = 0 \<or> x = y" shows "x*k = k*(y::rat)"
 
   313 by (tactic {* test [ring_eq_cancel_factor] *}) fact
 
   299 by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
 
   314 
   300 
   315 lemma assumes "k = 0 \<or> 1 = y" shows "k = k*(y::rat)"
 
   301 lemma assumes "k = 0 \<or> 1 = y" shows "k = k*(y::rat)"
 
   316 by (tactic {* test [ring_eq_cancel_factor] *}) fact
 
   302 by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
 
   317 
   303 
   318 lemma assumes "b = 0 \<or> a*c = 1" shows "a*(b*c) = (b::rat)"
 
   304 lemma assumes "b = 0 \<or> a*c = 1" shows "a*(b*c) = (b::rat)"
 
   319 by (tactic {* test [ring_eq_cancel_factor] *}) fact
 
   305 by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
 
   320 
   306 
   321 lemma assumes "a = 0 \<or> b = 0 \<or> c = d*x" shows "a*(b*c) = d*(b::rat)*(x*a)"
 
   307 lemma assumes "a = 0 \<or> b = 0 \<or> c = d*x" shows "a*(b*c) = d*(b::rat)*(x*a)"
 
   322 by (tactic {* test [ring_eq_cancel_factor] *}) fact
 
   308 by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
 
   323 
   309 
   324 
   310 
   325 subsection {* @{text int_div_cancel_factor} *}
 
   311 subsection {* @{text int_div_cancel_factor} *}
 
   326 
   312 
   327 lemma assumes "(if k = 0 then 0 else x div y) = uu"
 
   313 lemma assumes "(if k = 0 then 0 else x div y) = uu"
 
   328   shows "(x*k) div (k*(y::int)) = (uu::int)"
 
   314   shows "(x*k) div (k*(y::int)) = (uu::int)"
 
   329 by (tactic {* test [int_div_cancel_factor] *}) fact
 
   315 by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact
 
   330 
   316 
   331 lemma assumes "(if k = 0 then 0 else 1 div y) = uu"
 
   317 lemma assumes "(if k = 0 then 0 else 1 div y) = uu"
 
   332   shows "(k) div (k*(y::int)) = (uu::int)"
 
   318   shows "(k) div (k*(y::int)) = (uu::int)"
 
   333 by (tactic {* test [int_div_cancel_factor] *}) fact
 
   319 by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact
 
   334 
   320 
   335 lemma assumes "(if b = 0 then 0 else a * c) = uu"
 
   321 lemma assumes "(if b = 0 then 0 else a * c) = uu"
 
   336   shows "(a*(b*c)) div ((b::int)) = (uu::int)"
 
   322   shows "(a*(b*c)) div ((b::int)) = (uu::int)"
 
   337 by (tactic {* test [int_div_cancel_factor] *}) fact
 
   323 by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact
 
   338 
   324 
   339 lemma assumes "(if a = 0 then 0 else if b = 0 then 0 else c div (d * x)) = uu"
 
   325 lemma assumes "(if a = 0 then 0 else if b = 0 then 0 else c div (d * x)) = uu"
 
   340   shows "(a*(b*c)) div (d*(b::int)*(x*a)) = (uu::int)"
 
   326   shows "(a*(b*c)) div (d*(b::int)*(x*a)) = (uu::int)"
 
   341 by (tactic {* test [int_div_cancel_factor] *}) fact
 
   327 by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact
 
   342 
   328 
   343 
   329 
   344 subsection {* @{text divide_cancel_factor} *}
 
   330 subsection {* @{text divide_cancel_factor} *}
 
   345 
   331 
   346 lemma assumes "(if k = 0 then 0 else x / y) = uu"
 
   332 lemma assumes "(if k = 0 then 0 else x / y) = uu"
 
   347   shows "(x*k) / (k*(y::rat)) = (uu::rat)"
 
   333   shows "(x*k) / (k*(y::rat)) = (uu::rat)"
 
   348 by (tactic {* test [divide_cancel_factor] *}) fact
 
   334 by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact
 
   349 
   335 
   350 lemma assumes "(if k = 0 then 0 else 1 / y) = uu"
 
   336 lemma assumes "(if k = 0 then 0 else 1 / y) = uu"
 
   351   shows "(k) / (k*(y::rat)) = (uu::rat)"
 
   337   shows "(k) / (k*(y::rat)) = (uu::rat)"
 
   352 by (tactic {* test [divide_cancel_factor] *}) fact
 
   338 by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact
 
   353 
   339 
   354 lemma assumes "(if b = 0 then 0 else a * c / 1) = uu"
 
   340 lemma assumes "(if b = 0 then 0 else a * c / 1) = uu"
 
   355   shows "(a*(b*c)) / ((b::rat)) = (uu::rat)"
 
   341   shows "(a*(b*c)) / ((b::rat)) = (uu::rat)"
 
   356 by (tactic {* test [divide_cancel_factor] *}) fact
 
   342 by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact
 
   357 
   343 
   358 lemma assumes "(if a = 0 then 0 else if b = 0 then 0 else c / (d * x)) = uu"
 
   344 lemma assumes "(if a = 0 then 0 else if b = 0 then 0 else c / (d * x)) = uu"
 
   359   shows "(a*(b*c)) / (d*(b::rat)*(x*a)) = (uu::rat)"
 
   345   shows "(a*(b*c)) / (d*(b::rat)*(x*a)) = (uu::rat)"
 
   360 by (tactic {* test [divide_cancel_factor] *}) fact
 
   346 by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact
 
   361 
   347 
   362 lemma shows "a*(b*c)/(y*z) = d*(b::rat)*(x*a)/z"
 
   348 lemma shows "a*(b*c)/(y*z) = d*(b::rat)*(x*a)/z"
 
   363 oops -- "FIXME: need simproc to cover this case"
 
   349 oops -- "FIXME: need simproc to cover this case"
 
   364 
   350 
   365 
   351 
   366 subsection {* @{text linordered_ring_less_cancel_factor} *}
 
   352 subsection {* @{text linordered_ring_less_cancel_factor} *}
 
   367 
   353 
   368 lemma assumes "0 < z \<Longrightarrow> x < y" shows "(0::rat) < z \<Longrightarrow> x*z < y*z"
 
   354 lemma assumes "0 < z \<Longrightarrow> x < y" shows "(0::rat) < z \<Longrightarrow> x*z < y*z"
 
   369 by (tactic {* test [linordered_ring_less_cancel_factor] *}) fact
 
   355 by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact
 
   370 
   356 
   371 lemma assumes "0 < z \<Longrightarrow> x < y" shows "(0::rat) < z \<Longrightarrow> x*z < z*y"
 
   357 lemma assumes "0 < z \<Longrightarrow> x < y" shows "(0::rat) < z \<Longrightarrow> x*z < z*y"
 
   372 by (tactic {* test [linordered_ring_less_cancel_factor] *}) fact
 
   358 by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact
 
   373 
   359 
   374 lemma assumes "0 < z \<Longrightarrow> x < y" shows "(0::rat) < z \<Longrightarrow> z*x < y*z"
 
   360 lemma assumes "0 < z \<Longrightarrow> x < y" shows "(0::rat) < z \<Longrightarrow> z*x < y*z"
 
   375 by (tactic {* test [linordered_ring_less_cancel_factor] *}) fact
 
   361 by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact
 
   376 
   362 
   377 lemma assumes "0 < z \<Longrightarrow> x < y" shows "(0::rat) < z \<Longrightarrow> z*x < z*y"
 
   363 lemma assumes "0 < z \<Longrightarrow> x < y" shows "(0::rat) < z \<Longrightarrow> z*x < z*y"
 
   378 by (tactic {* test [linordered_ring_less_cancel_factor] *}) fact
 
   364 by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact
 
   379 
   365 
   380 
   366 
   381 subsection {* @{text linordered_ring_le_cancel_factor} *}
 
   367 subsection {* @{text linordered_ring_le_cancel_factor} *}
 
   382 
   368 
   383 lemma assumes "0 < z \<Longrightarrow> x \<le> y" shows "(0::rat) < z \<Longrightarrow> x*z \<le> y*z"
 
   369 lemma assumes "0 < z \<Longrightarrow> x \<le> y" shows "(0::rat) < z \<Longrightarrow> x*z \<le> y*z"
 
   384 by (tactic {* test [linordered_ring_le_cancel_factor] *}) fact
 
   370 by (tactic {* test [@{simproc linordered_ring_le_cancel_factor}] *}) fact
 
   385 
   371 
   386 lemma assumes "0 < z \<Longrightarrow> x \<le> y" shows "(0::rat) < z \<Longrightarrow> z*x \<le> z*y"
 
   372 lemma assumes "0 < z \<Longrightarrow> x \<le> y" shows "(0::rat) < z \<Longrightarrow> z*x \<le> z*y"
 
   387 by (tactic {* test [linordered_ring_le_cancel_factor] *}) fact
 
   373 by (tactic {* test [@{simproc linordered_ring_le_cancel_factor}] *}) fact
 
   388 
   374 
   389 
   375 
   390 subsection {* @{text field_combine_numerals} *}
 
   376 subsection {* @{text field_combine_numerals} *}
 
   391 
   377 
   392 lemma assumes "5 / 6 * x = uu" shows "(x::rat) / 2 + x / 3 = uu"
 
   378 lemma assumes "5 / 6 * x = uu" shows "(x::rat) / 2 + x / 3 = uu"
 
   393 by (tactic {* test [field_combine_numerals] *}) fact
 
   379 by (tactic {* test [@{simproc field_combine_numerals}] *}) fact
 
   394 
   380 
   395 lemma assumes "6 / 9 * x + y = uu" shows "(x::rat) / 3 + y + x / 3 = uu"
 
   381 lemma assumes "6 / 9 * x + y = uu" shows "(x::rat) / 3 + y + x / 3 = uu"
 
   396 by (tactic {* test [field_combine_numerals] *}) fact
 
   382 by (tactic {* test [@{simproc field_combine_numerals}] *}) fact
 
   397 
   383 
   398 lemma assumes "9 / 9 * x = uu" shows "2 * (x::rat) / 3 + x / 3 = uu"
 
   384 lemma assumes "9 / 9 * x = uu" shows "2 * (x::rat) / 3 + x / 3 = uu"
 
   399 by (tactic {* test [field_combine_numerals] *}) fact
 
   385 by (tactic {* test [@{simproc field_combine_numerals}] *}) fact
 
   400 
   386 
   401 lemma "2/3 * (x::rat) + x / 3 = uu"
 
   387 lemma "2/3 * (x::rat) + x / 3 = uu"
 
   402 apply (tactic {* test [field_combine_numerals] *})?
 
   388 apply (tactic {* test [@{simproc field_combine_numerals}] *})?
 
   403 oops -- "FIXME: test fails"
 
   389 oops -- "FIXME: test fails"
 
   404 
   390 
   405 
   391 
   406 subsection {* @{text field_eq_cancel_numeral_factor} *}
 
   392 subsection {* @{text field_eq_cancel_numeral_factor} *}
 
   407 
   393
isabelle