src/HOL/ex/Simproc_Tests.thy
 author hoelzl Thu Jan 31 11:31:27 2013 +0100 (2013-01-31) changeset 50999 3de230ed0547 parent 48559 686cc7c47589 child 51717 9e7d1c139569 permissions -rw-r--r--
introduce order topology
```     1 (*  Title:      HOL/ex/Simproc_Tests.thy
```
```     2     Author:     Brian Huffman
```
```     3 *)
```
```     4
```
```     5 header {* Testing of arithmetic simprocs *}
```
```     6
```
```     7 theory Simproc_Tests
```
```     8 imports Main
```
```     9 begin
```
```    10
```
```    11 text {*
```
```    12   This theory tests the various simprocs defined in @{file
```
```    13   "~~/src/HOL/Nat.thy"} and @{file "~~/src/HOL/Numeral_Simprocs.thy"}.
```
```    14   Many of the tests are derived from commented-out code originally
```
```    15   found in @{file "~~/src/HOL/Tools/numeral_simprocs.ML"}.
```
```    16 *}
```
```    17
```
```    18 subsection {* ML bindings *}
```
```    19
```
```    20 ML {*
```
```    21   fun test ps = CHANGED (asm_simp_tac (HOL_basic_ss addsimprocs ps) 1)
```
```    22 *}
```
```    23
```
```    24 subsection {* Cancellation simprocs from @{text Nat.thy} *}
```
```    25
```
```    26 notepad begin
```
```    27   fix a b c d :: nat
```
```    28   {
```
```    29     assume "b = Suc c" have "a + b = Suc (c + a)"
```
```    30       by (tactic {* test [@{simproc nateq_cancel_sums}] *}) fact
```
```    31   next
```
```    32     assume "b < Suc c" have "a + b < Suc (c + a)"
```
```    33       by (tactic {* test [@{simproc natless_cancel_sums}] *}) fact
```
```    34   next
```
```    35     assume "b \<le> Suc c" have "a + b \<le> Suc (c + a)"
```
```    36       by (tactic {* test [@{simproc natle_cancel_sums}] *}) fact
```
```    37   next
```
```    38     assume "b - Suc c = d" have "a + b - Suc (c + a) = d"
```
```    39       by (tactic {* test [@{simproc natdiff_cancel_sums}] *}) fact
```
```    40   }
```
```    41 end
```
```    42
```
```    43 schematic_lemma "\<And>(y::?'b::size). size (?x::?'a::size) \<le> size y + size ?x"
```
```    44   by (tactic {* test [@{simproc natle_cancel_sums}] *}) (rule le0)
```
```    45 (* TODO: test more simprocs with schematic variables *)
```
```    46
```
```    47 subsection {* Abelian group cancellation simprocs *}
```
```    48
```
```    49 notepad begin
```
```    50   fix a b c u :: "'a::ab_group_add"
```
```    51   {
```
```    52     assume "(a + 0) - (b + 0) = u" have "(a + c) - (b + c) = u"
```
```    53       by (tactic {* test [@{simproc group_cancel_diff}] *}) fact
```
```    54   next
```
```    55     assume "a + 0 = b + 0" have "a + c = b + c"
```
```    56       by (tactic {* test [@{simproc group_cancel_eq}] *}) fact
```
```    57   }
```
```    58 end
```
```    59 (* TODO: more tests for Groups.group_cancel_{add,diff,eq,less,le} *)
```
```    60
```
```    61 subsection {* @{text int_combine_numerals} *}
```
```    62
```
```    63 (* FIXME: int_combine_numerals often unnecessarily regroups addition
```
```    64 and rewrites subtraction to negation. Ideally it should behave more
```
```    65 like Groups.abel_cancel_sum, preserving the shape of terms as much as
```
```    66 possible. *)
```
```    67
```
```    68 notepad begin
```
```    69   fix a b c d oo uu i j k l u v w x y z :: "'a::comm_ring_1"
```
```    70   {
```
```    71     assume "a + - b = u" have "(a + c) - (b + c) = u"
```
```    72       by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
```
```    73   next
```
```    74     assume "10 + (2 * l + oo) = uu"
```
```    75     have "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = uu"
```
```    76       by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
```
```    77   next
```
```    78     assume "-3 + (i + (j + k)) = y"
```
```    79     have "(i + j + 12 + k) - 15 = y"
```
```    80       by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
```
```    81   next
```
```    82     assume "7 + (i + (j + k)) = y"
```
```    83     have "(i + j + 12 + k) - 5 = y"
```
```    84       by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
```
```    85   next
```
```    86     assume "-4 * (u * v) + (2 * x + y) = w"
```
```    87     have "(2*x - (u*v) + y) - v*3*u = w"
```
```    88       by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
```
```    89   next
```
```    90     assume "2 * x * u * v + y = w"
```
```    91     have "(2*x*u*v + (u*v)*4 + y) - v*u*4 = w"
```
```    92       by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
```
```    93   next
```
```    94     assume "3 * (u * v) + (2 * x * u * v + y) = w"
```
```    95     have "(2*x*u*v + (u*v)*4 + y) - v*u = w"
```
```    96       by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
```
```    97   next
```
```    98     assume "-3 * (u * v) + (- (x * u * v) + - y) = w"
```
```    99     have "u*v - (x*u*v + (u*v)*4 + y) = w"
```
```   100       by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
```
```   101   next
```
```   102     assume "a + - c = d"
```
```   103     have "a + -(b+c) + b = d"
```
```   104       apply (simp only: minus_add_distrib)
```
```   105       by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
```
```   106   next
```
```   107     assume "-2 * b + (a + - c) = d"
```
```   108     have "a + -(b+c) - b = d"
```
```   109       apply (simp only: minus_add_distrib)
```
```   110       by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
```
```   111   next
```
```   112     assume "-7 + (i + (j + (k + (- u + - y)))) = z"
```
```   113     have "(i + j + -2 + k) - (u + 5 + y) = z"
```
```   114       by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
```
```   115   next
```
```   116     assume "-27 + (i + (j + k)) = y"
```
```   117     have "(i + j + -12 + k) - 15 = y"
```
```   118       by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
```
```   119   next
```
```   120     assume "27 + (i + (j + k)) = y"
```
```   121     have "(i + j + 12 + k) - -15 = y"
```
```   122       by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
```
```   123   next
```
```   124     assume "3 + (i + (j + k)) = y"
```
```   125     have "(i + j + -12 + k) - -15 = y"
```
```   126       by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
```
```   127   }
```
```   128 end
```
```   129
```
```   130 subsection {* @{text inteq_cancel_numerals} *}
```
```   131
```
```   132 notepad begin
```
```   133   fix i j k u vv w y z w' y' z' :: "'a::comm_ring_1"
```
```   134   {
```
```   135     assume "u = 0" have "2*u = u"
```
```   136       by (tactic {* test [@{simproc inteq_cancel_numerals}] *}) fact
```
```   137 (* conclusion matches Rings.ring_1_no_zero_divisors_class.mult_cancel_right2 *)
```
```   138   next
```
```   139     assume "i + (j + k) = 3 + (u + y)"
```
```   140     have "(i + j + 12 + k) = u + 15 + y"
```
```   141       by (tactic {* test [@{simproc inteq_cancel_numerals}] *}) fact
```
```   142   next
```
```   143     assume "7 + (j + (i + k)) = y"
```
```   144     have "(i + j*2 + 12 + k) = j + 5 + y"
```
```   145       by (tactic {* test [@{simproc inteq_cancel_numerals}] *}) fact
```
```   146   next
```
```   147     assume "u + (6*z + (4*y + 6*w)) = 6*z' + (4*y' + (6*w' + vv))"
```
```   148     have "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = 2*y' + 3*z' + 6*w' + 2*y' + 3*z' + u + vv"
```
```   149       by (tactic {* test [@{simproc int_combine_numerals}, @{simproc inteq_cancel_numerals}] *}) fact
```
```   150   }
```
```   151 end
```
```   152
```
```   153 subsection {* @{text intless_cancel_numerals} *}
```
```   154
```
```   155 notepad begin
```
```   156   fix b c i j k u y :: "'a::linordered_idom"
```
```   157   {
```
```   158     assume "y < 2 * b" have "y - b < b"
```
```   159       by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact
```
```   160   next
```
```   161     assume "c + y < 4 * b" have "y - (3*b + c) < b - 2*c"
```
```   162       by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact
```
```   163   next
```
```   164     assume "i + (j + k) < 8 + (u + y)"
```
```   165     have "(i + j + -3 + k) < u + 5 + y"
```
```   166       by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact
```
```   167   next
```
```   168     assume "9 + (i + (j + k)) < u + y"
```
```   169     have "(i + j + 3 + k) < u + -6 + y"
```
```   170       by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact
```
```   171   }
```
```   172 end
```
```   173
```
```   174 subsection {* @{text ring_eq_cancel_numeral_factor} *}
```
```   175
```
```   176 notepad begin
```
```   177   fix x y :: "'a::{idom,ring_char_0}"
```
```   178   {
```
```   179     assume "3*x = 4*y" have "9*x = 12 * y"
```
```   180       by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
```
```   181   next
```
```   182     assume "-3*x = 4*y" have "-99*x = 132 * y"
```
```   183       by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
```
```   184   next
```
```   185     assume "111*x = -44*y" have "999*x = -396 * y"
```
```   186       by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
```
```   187   next
```
```   188     assume "11*x = 9*y" have "-99*x = -81 * y"
```
```   189       by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
```
```   190   next
```
```   191     assume "2*x = y" have "-2 * x = -1 * y"
```
```   192       by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
```
```   193   next
```
```   194     assume "2*x = y" have "-2 * x = -y"
```
```   195       by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
```
```   196   }
```
```   197 end
```
```   198
```
```   199 subsection {* @{text int_div_cancel_numeral_factors} *}
```
```   200
```
```   201 notepad begin
```
```   202   fix x y z :: "'a::{semiring_div,comm_ring_1,ring_char_0}"
```
```   203   {
```
```   204     assume "(3*x) div (4*y) = z" have "(9*x) div (12*y) = z"
```
```   205       by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact
```
```   206   next
```
```   207     assume "(-3*x) div (4*y) = z" have "(-99*x) div (132*y) = z"
```
```   208       by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact
```
```   209   next
```
```   210     assume "(111*x) div (-44*y) = z" have "(999*x) div (-396*y) = z"
```
```   211       by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact
```
```   212   next
```
```   213     assume "(11*x) div (9*y) = z" have "(-99*x) div (-81*y) = z"
```
```   214       by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact
```
```   215   next
```
```   216     assume "(2*x) div y = z"
```
```   217     have "(-2 * x) div (-1 * y) = z"
```
```   218       by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact
```
```   219   }
```
```   220 end
```
```   221
```
```   222 subsection {* @{text ring_less_cancel_numeral_factor} *}
```
```   223
```
```   224 notepad begin
```
```   225   fix x y :: "'a::linordered_idom"
```
```   226   {
```
```   227     assume "3*x < 4*y" have "9*x < 12 * y"
```
```   228       by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
```
```   229   next
```
```   230     assume "-3*x < 4*y" have "-99*x < 132 * y"
```
```   231       by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
```
```   232   next
```
```   233     assume "111*x < -44*y" have "999*x < -396 * y"
```
```   234       by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
```
```   235   next
```
```   236     assume "9*y < 11*x" have "-99*x < -81 * y"
```
```   237       by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
```
```   238   next
```
```   239     assume "y < 2*x" have "-2 * x < -y"
```
```   240       by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
```
```   241   next
```
```   242     assume "23*y < x" have "-x < -23 * y"
```
```   243       by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
```
```   244   }
```
```   245 end
```
```   246
```
```   247 subsection {* @{text ring_le_cancel_numeral_factor} *}
```
```   248
```
```   249 notepad begin
```
```   250   fix x y :: "'a::linordered_idom"
```
```   251   {
```
```   252     assume "3*x \<le> 4*y" have "9*x \<le> 12 * y"
```
```   253       by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
```
```   254   next
```
```   255     assume "-3*x \<le> 4*y" have "-99*x \<le> 132 * y"
```
```   256       by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
```
```   257   next
```
```   258     assume "111*x \<le> -44*y" have "999*x \<le> -396 * y"
```
```   259       by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
```
```   260   next
```
```   261     assume "9*y \<le> 11*x" have "-99*x \<le> -81 * y"
```
```   262       by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
```
```   263   next
```
```   264     assume "y \<le> 2*x" have "-2 * x \<le> -1 * y"
```
```   265       by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
```
```   266   next
```
```   267     assume "23*y \<le> x" have "-x \<le> -23 * y"
```
```   268       by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
```
```   269   next
```
```   270     assume "y \<le> 0" have "0 \<le> y * -2"
```
```   271       by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
```
```   272   next
```
```   273     assume "- x \<le> y" have "- (2 * x) \<le> 2*y"
```
```   274       by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
```
```   275   }
```
```   276 end
```
```   277
```
```   278 subsection {* @{text divide_cancel_numeral_factor} *}
```
```   279
```
```   280 notepad begin
```
```   281   fix x y z :: "'a::{field_inverse_zero,ring_char_0}"
```
```   282   {
```
```   283     assume "(3*x) / (4*y) = z" have "(9*x) / (12 * y) = z"
```
```   284       by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact
```
```   285   next
```
```   286     assume "(-3*x) / (4*y) = z" have "(-99*x) / (132 * y) = z"
```
```   287       by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact
```
```   288   next
```
```   289     assume "(111*x) / (-44*y) = z" have "(999*x) / (-396 * y) = z"
```
```   290       by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact
```
```   291   next
```
```   292     assume "(11*x) / (9*y) = z" have "(-99*x) / (-81 * y) = z"
```
```   293       by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact
```
```   294   next
```
```   295     assume "(2*x) / y = z" have "(-2 * x) / (-1 * y) = z"
```
```   296       by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact
```
```   297   }
```
```   298 end
```
```   299
```
```   300 subsection {* @{text ring_eq_cancel_factor} *}
```
```   301
```
```   302 notepad begin
```
```   303   fix a b c d k x y :: "'a::idom"
```
```   304   {
```
```   305     assume "k = 0 \<or> x = y" have "x*k = k*y"
```
```   306       by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
```
```   307   next
```
```   308     assume "k = 0 \<or> 1 = y" have "k = k*y"
```
```   309       by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
```
```   310   next
```
```   311     assume "b = 0 \<or> a*c = 1" have "a*(b*c) = b"
```
```   312       by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
```
```   313   next
```
```   314     assume "a = 0 \<or> b = 0 \<or> c = d*x" have "a*(b*c) = d*b*(x*a)"
```
```   315       by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
```
```   316   next
```
```   317     assume "k = 0 \<or> x = y" have "x*k = k*y"
```
```   318       by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
```
```   319   next
```
```   320     assume "k = 0 \<or> 1 = y" have "k = k*y"
```
```   321       by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
```
```   322   }
```
```   323 end
```
```   324
```
```   325 subsection {* @{text int_div_cancel_factor} *}
```
```   326
```
```   327 notepad begin
```
```   328   fix a b c d k uu x y :: "'a::semiring_div"
```
```   329   {
```
```   330     assume "(if k = 0 then 0 else x div y) = uu"
```
```   331     have "(x*k) div (k*y) = uu"
```
```   332       by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact
```
```   333   next
```
```   334     assume "(if k = 0 then 0 else 1 div y) = uu"
```
```   335     have "(k) div (k*y) = uu"
```
```   336       by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact
```
```   337   next
```
```   338     assume "(if b = 0 then 0 else a * c) = uu"
```
```   339     have "(a*(b*c)) div b = uu"
```
```   340       by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact
```
```   341   next
```
```   342     assume "(if a = 0 then 0 else if b = 0 then 0 else c div (d * x)) = uu"
```
```   343     have "(a*(b*c)) div (d*b*(x*a)) = uu"
```
```   344       by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact
```
```   345   }
```
```   346 end
```
```   347
```
```   348 lemma shows "a*(b*c)/(y*z) = d*(b::'a::linordered_field_inverse_zero)*(x*a)/z"
```
```   349 oops -- "FIXME: need simproc to cover this case"
```
```   350
```
```   351 subsection {* @{text divide_cancel_factor} *}
```
```   352
```
```   353 notepad begin
```
```   354   fix a b c d k uu x y :: "'a::field_inverse_zero"
```
```   355   {
```
```   356     assume "(if k = 0 then 0 else x / y) = uu"
```
```   357     have "(x*k) / (k*y) = uu"
```
```   358       by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact
```
```   359   next
```
```   360     assume "(if k = 0 then 0 else 1 / y) = uu"
```
```   361     have "(k) / (k*y) = uu"
```
```   362       by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact
```
```   363   next
```
```   364     assume "(if b = 0 then 0 else a * c / 1) = uu"
```
```   365     have "(a*(b*c)) / b = uu"
```
```   366       by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact
```
```   367   next
```
```   368     assume "(if a = 0 then 0 else if b = 0 then 0 else c / (d * x)) = uu"
```
```   369     have "(a*(b*c)) / (d*b*(x*a)) = uu"
```
```   370       by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact
```
```   371   }
```
```   372 end
```
```   373
```
```   374 lemma
```
```   375   fixes a b c d x y z :: "'a::linordered_field_inverse_zero"
```
```   376   shows "a*(b*c)/(y*z) = d*(b)*(x*a)/z"
```
```   377 oops -- "FIXME: need simproc to cover this case"
```
```   378
```
```   379 subsection {* @{text linordered_ring_less_cancel_factor} *}
```
```   380
```
```   381 notepad begin
```
```   382   fix x y z :: "'a::linordered_idom"
```
```   383   {
```
```   384     assume "0 < z \<Longrightarrow> x < y" have "0 < z \<Longrightarrow> x*z < y*z"
```
```   385       by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact
```
```   386   next
```
```   387     assume "0 < z \<Longrightarrow> x < y" have "0 < z \<Longrightarrow> x*z < z*y"
```
```   388       by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact
```
```   389   next
```
```   390     assume "0 < z \<Longrightarrow> x < y" have "0 < z \<Longrightarrow> z*x < y*z"
```
```   391       by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact
```
```   392   next
```
```   393     assume "0 < z \<Longrightarrow> x < y" have "0 < z \<Longrightarrow> z*x < z*y"
```
```   394       by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact
```
```   395   next
```
```   396     txt "This simproc now uses the simplifier to prove that terms to
```
```   397       be canceled are positive/negative."
```
```   398     assume z_pos: "0 < z"
```
```   399     assume "x < y" have "z*x < z*y"
```
```   400       by (tactic {* CHANGED (asm_simp_tac (HOL_basic_ss
```
```   401         addsimprocs [@{simproc linordered_ring_less_cancel_factor}]
```
```   402         addsimps [@{thm z_pos}]) 1) *}) fact
```
```   403   }
```
```   404 end
```
```   405
```
```   406 subsection {* @{text linordered_ring_le_cancel_factor} *}
```
```   407
```
```   408 notepad begin
```
```   409   fix x y z :: "'a::linordered_idom"
```
```   410   {
```
```   411     assume "0 < z \<Longrightarrow> x \<le> y" have "0 < z \<Longrightarrow> x*z \<le> y*z"
```
```   412       by (tactic {* test [@{simproc linordered_ring_le_cancel_factor}] *}) fact
```
```   413   next
```
```   414     assume "0 < z \<Longrightarrow> x \<le> y" have "0 < z \<Longrightarrow> z*x \<le> z*y"
```
```   415       by (tactic {* test [@{simproc linordered_ring_le_cancel_factor}] *}) fact
```
```   416   }
```
```   417 end
```
```   418
```
```   419 subsection {* @{text field_combine_numerals} *}
```
```   420
```
```   421 notepad begin
```
```   422   fix x y z uu :: "'a::{field_inverse_zero,ring_char_0}"
```
```   423   {
```
```   424     assume "5 / 6 * x = uu" have "x / 2 + x / 3 = uu"
```
```   425       by (tactic {* test [@{simproc field_combine_numerals}] *}) fact
```
```   426   next
```
```   427     assume "6 / 9 * x + y = uu" have "x / 3 + y + x / 3 = uu"
```
```   428       by (tactic {* test [@{simproc field_combine_numerals}] *}) fact
```
```   429   next
```
```   430     assume "9 / 9 * x = uu" have "2 * x / 3 + x / 3 = uu"
```
```   431       by (tactic {* test [@{simproc field_combine_numerals}] *}) fact
```
```   432   next
```
```   433     assume "y + z = uu"
```
```   434     have "x / 2 + y - 3 * x / 6 + z = uu"
```
```   435       by (tactic {* test [@{simproc field_combine_numerals}] *}) fact
```
```   436   next
```
```   437     assume "1 / 15 * x + y = uu"
```
```   438     have "7 * x / 5 + y - 4 * x / 3 = uu"
```
```   439       by (tactic {* test [@{simproc field_combine_numerals}] *}) fact
```
```   440   }
```
```   441 end
```
```   442
```
```   443 lemma
```
```   444   fixes x :: "'a::{linordered_field_inverse_zero}"
```
```   445   shows "2/3 * x + x / 3 = uu"
```
```   446 apply (tactic {* test [@{simproc field_combine_numerals}] *})?
```
```   447 oops -- "FIXME: test fails"
```
```   448
```
```   449 subsection {* @{text nat_combine_numerals} *}
```
```   450
```
```   451 notepad begin
```
```   452   fix i j k m n u :: nat
```
```   453   {
```
```   454     assume "4*k = u" have "k + 3*k = u"
```
```   455       by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact
```
```   456   next
```
```   457     (* FIXME "Suc (i + 3) \<equiv> i + 4" *)
```
```   458     assume "4 * Suc 0 + i = u" have "Suc (i + 3) = u"
```
```   459       by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact
```
```   460   next
```
```   461     (* FIXME "Suc (i + j + 3 + k) \<equiv> i + j + 4 + k" *)
```
```   462     assume "4 * Suc 0 + (i + (j + k)) = u" have "Suc (i + j + 3 + k) = u"
```
```   463       by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact
```
```   464   next
```
```   465     assume "2 * j + 4 * k = u" have "k + j + 3*k + j = u"
```
```   466       by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact
```
```   467   next
```
```   468     assume "6 * Suc 0 + (5 * (i * j) + (4 * k + i)) = u"
```
```   469     have "Suc (j*i + i + k + 5 + 3*k + i*j*4) = u"
```
```   470       by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact
```
```   471   next
```
```   472     assume "5 * (m * n) = u" have "(2*n*m) + (3*(m*n)) = u"
```
```   473       by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact
```
```   474   }
```
```   475 end
```
```   476
```
```   477 subsection {* @{text nateq_cancel_numerals} *}
```
```   478
```
```   479 notepad begin
```
```   480   fix i j k l oo u uu vv w y z w' y' z' :: "nat"
```
```   481   {
```
```   482     assume "Suc 0 * u = 0" have "2*u = (u::nat)"
```
```   483       by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
```
```   484   next
```
```   485     assume "Suc 0 * u = Suc 0" have "2*u = Suc (u)"
```
```   486       by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
```
```   487   next
```
```   488     assume "i + (j + k) = 3 * Suc 0 + (u + y)"
```
```   489     have "(i + j + 12 + k) = u + 15 + y"
```
```   490       by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
```
```   491   next
```
```   492     assume "7 * Suc 0 + (i + (j + k)) = u + y"
```
```   493     have "(i + j + 12 + k) = u + 5 + y"
```
```   494       by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
```
```   495   next
```
```   496     assume "11 * Suc 0 + (i + (j + k)) = u + y"
```
```   497     have "(i + j + 12 + k) = Suc (u + y)"
```
```   498       by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
```
```   499   next
```
```   500     assume "i + (j + k) = 2 * Suc 0 + (u + y)"
```
```   501     have "(i + j + 5 + k) = Suc (Suc (Suc (Suc (Suc (Suc (Suc (u + y)))))))"
```
```   502       by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
```
```   503   next
```
```   504     assume "Suc 0 * u + (2 * y + 3 * z) = Suc 0"
```
```   505     have "2*y + 3*z + 2*u = Suc (u)"
```
```   506       by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
```
```   507   next
```
```   508     assume "Suc 0 * u + (2 * y + (3 * z + (6 * w + (2 * y + 3 * z)))) = Suc 0"
```
```   509     have "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = Suc (u)"
```
```   510       by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
```
```   511   next
```
```   512     assume "Suc 0 * u + (2 * y + (3 * z + (6 * w + (2 * y + 3 * z)))) =
```
```   513       2 * y' + (3 * z' + (6 * w' + (2 * y' + (3 * z' + vv))))"
```
```   514     have "2*y + 3*z + 6*w + 2*y + 3*z + 2*u =
```
```   515       2*y' + 3*z' + 6*w' + 2*y' + 3*z' + u + vv"
```
```   516       by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
```
```   517   next
```
```   518     assume "2 * u + (2 * z + (5 * Suc 0 + 2 * y)) = vv"
```
```   519     have "6 + 2*y + 3*z + 4*u = Suc (vv + 2*u + z)"
```
```   520       by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
```
```   521   }
```
```   522 end
```
```   523
```
```   524 subsection {* @{text natless_cancel_numerals} *}
```
```   525
```
```   526 notepad begin
```
```   527   fix length :: "'a \<Rightarrow> nat" and l1 l2 xs :: "'a" and f :: "nat \<Rightarrow> 'a"
```
```   528   fix c i j k l m oo u uu vv w y z w' y' z' :: "nat"
```
```   529   {
```
```   530     assume "0 < j" have "(2*length xs < 2*length xs + j)"
```
```   531       by (tactic {* test [@{simproc natless_cancel_numerals}] *}) fact
```
```   532   next
```
```   533     assume "0 < j" have "(2*length xs < length xs * 2 + j)"
```
```   534       by (tactic {* test [@{simproc natless_cancel_numerals}] *}) fact
```
```   535   next
```
```   536     assume "i + (j + k) < u + y"
```
```   537     have "(i + j + 5 + k) < Suc (Suc (Suc (Suc (Suc (u + y)))))"
```
```   538       by (tactic {* test [@{simproc natless_cancel_numerals}] *}) fact
```
```   539   next
```
```   540     assume "0 < Suc 0 * (m * n) + u" have "(2*n*m) < (3*(m*n)) + u"
```
```   541       by (tactic {* test [@{simproc natless_cancel_numerals}] *}) fact
```
```   542   }
```
```   543 end
```
```   544
```
```   545 subsection {* @{text natle_cancel_numerals} *}
```
```   546
```
```   547 notepad begin
```
```   548   fix length :: "'a \<Rightarrow> nat" and l2 l3 :: "'a" and f :: "nat \<Rightarrow> 'a"
```
```   549   fix c e i j k l oo u uu vv w y z w' y' z' :: "nat"
```
```   550   {
```
```   551     assume "u + y \<le> 36 * Suc 0 + (i + (j + k))"
```
```   552     have "Suc (Suc (Suc (Suc (Suc (u + y))))) \<le> ((i + j) + 41 + k)"
```
```   553       by (tactic {* test [@{simproc natle_cancel_numerals}] *}) fact
```
```   554   next
```
```   555     assume "5 * Suc 0 + (case length (f c) of 0 \<Rightarrow> 0 | Suc k \<Rightarrow> k) = 0"
```
```   556     have "(Suc (Suc (Suc (Suc (Suc (Suc (case length (f c) of 0 => 0 | Suc k => k)))))) \<le> Suc 0)"
```
```   557       by (tactic {* test [@{simproc natle_cancel_numerals}] *}) fact
```
```   558   next
```
```   559     assume "6 + length l2 = 0" have "Suc (Suc (Suc (Suc (Suc (Suc (length l1 + length l2)))))) \<le> length l1"
```
```   560       by (tactic {* test [@{simproc natle_cancel_numerals}] *}) fact
```
```   561   next
```
```   562     assume "5 + length l3 = 0"
```
```   563     have "( (Suc (Suc (Suc (Suc (Suc (length (compT P E A ST mxr e) + length l3)))))) \<le> length (compT P E A ST mxr e))"
```
```   564       by (tactic {* test [@{simproc natle_cancel_numerals}] *}) fact
```
```   565   next
```
```   566     assume "5 + length (compT P E (A \<union> A' e) ST mxr c) = 0"
```
```   567     have "( (Suc (Suc (Suc (Suc (Suc (length (compT P E A ST mxr e) + length (compT P E (A Un A' e) ST mxr c))))))) \<le> length (compT P E A ST mxr e))"
```
```   568       by (tactic {* test [@{simproc natle_cancel_numerals}] *}) fact
```
```   569   }
```
```   570 end
```
```   571
```
```   572 subsection {* @{text natdiff_cancel_numerals} *}
```
```   573
```
```   574 notepad begin
```
```   575   fix length :: "'a \<Rightarrow> nat" and l2 l3 :: "'a" and f :: "nat \<Rightarrow> 'a"
```
```   576   fix c e i j k l oo u uu vv v w x y z zz w' y' z' :: "nat"
```
```   577   {
```
```   578     assume "i + (j + k) - 3 * Suc 0 = y" have "(i + j + 12 + k) - 15 = y"
```
```   579       by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
```
```   580   next
```
```   581     assume "7 * Suc 0 + (i + (j + k)) - 0 = y" have "(i + j + 12 + k) - 5 = y"
```
```   582       by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
```
```   583   next
```
```   584     assume "u - Suc 0 * Suc 0 = y" have "Suc u - 2 = y"
```
```   585       by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
```
```   586   next
```
```   587     assume "Suc 0 * Suc 0 + u - 0 = y" have "Suc (Suc (Suc u)) - 2 = y"
```
```   588       by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
```
```   589   next
```
```   590     assume "Suc 0 * Suc 0 + (i + (j + k)) - 0 = y"
```
```   591     have "(i + j + 2 + k) - 1 = y"
```
```   592       by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
```
```   593   next
```
```   594     assume "i + (j + k) - Suc 0 * Suc 0 = y"
```
```   595     have "(i + j + 1 + k) - 2 = y"
```
```   596       by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
```
```   597   next
```
```   598     assume "2 * x + y - 2 * (u * v) = w"
```
```   599     have "(2*x + (u*v) + y) - v*3*u = w"
```
```   600       by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
```
```   601   next
```
```   602     assume "2 * x * u * v + (5 + y) - 0 = w"
```
```   603     have "(2*x*u*v + 5 + (u*v)*4 + y) - v*u*4 = w"
```
```   604       by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
```
```   605   next
```
```   606     assume "3 * (u * v) + (2 * x * u * v + y) - 0 = w"
```
```   607     have "(2*x*u*v + (u*v)*4 + y) - v*u = w"
```
```   608       by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
```
```   609   next
```
```   610     assume "3 * u + (2 + (2 * x * u * v + y)) - 0 = w"
```
```   611     have "Suc (Suc (2*x*u*v + u*4 + y)) - u = w"
```
```   612       by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
```
```   613   next
```
```   614     assume "Suc (Suc 0 * (u * v)) - 0 = w"
```
```   615     have "Suc ((u*v)*4) - v*3*u = w"
```
```   616       by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
```
```   617   next
```
```   618     assume "2 - 0 = w" have "Suc (Suc ((u*v)*3)) - v*3*u = w"
```
```   619       by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
```
```   620   next
```
```   621     assume "17 * Suc 0 + (i + (j + k)) - (u + y) = zz"
```
```   622     have "(i + j + 32 + k) - (u + 15 + y) = zz"
```
```   623       by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
```
```   624   next
```
```   625     assume "u + y - 0 = v" have "Suc (Suc (Suc (Suc (Suc (u + y))))) - 5 = v"
```
```   626       by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
```
```   627   }
```
```   628 end
```
```   629
```
```   630 subsection {* Factor-cancellation simprocs for type @{typ nat} *}
```
```   631
```
```   632 text {* @{text nat_eq_cancel_factor}, @{text nat_less_cancel_factor},
```
```   633 @{text nat_le_cancel_factor}, @{text nat_divide_cancel_factor}, and
```
```   634 @{text nat_dvd_cancel_factor}. *}
```
```   635
```
```   636 notepad begin
```
```   637   fix a b c d k x y uu :: nat
```
```   638   {
```
```   639     assume "k = 0 \<or> x = y" have "x*k = k*y"
```
```   640       by (tactic {* test [@{simproc nat_eq_cancel_factor}] *}) fact
```
```   641   next
```
```   642     assume "k = 0 \<or> Suc 0 = y" have "k = k*y"
```
```   643       by (tactic {* test [@{simproc nat_eq_cancel_factor}] *}) fact
```
```   644   next
```
```   645     assume "b = 0 \<or> a * c = Suc 0" have "a*(b*c) = b"
```
```   646       by (tactic {* test [@{simproc nat_eq_cancel_factor}] *}) fact
```
```   647   next
```
```   648     assume "a = 0 \<or> b = 0 \<or> c = d * x" have "a*(b*c) = d*b*(x*a)"
```
```   649       by (tactic {* test [@{simproc nat_eq_cancel_factor}] *}) fact
```
```   650   next
```
```   651     assume "0 < k \<and> x < y" have "x*k < k*y"
```
```   652       by (tactic {* test [@{simproc nat_less_cancel_factor}] *}) fact
```
```   653   next
```
```   654     assume "0 < k \<and> Suc 0 < y" have "k < k*y"
```
```   655       by (tactic {* test [@{simproc nat_less_cancel_factor}] *}) fact
```
```   656   next
```
```   657     assume "0 < b \<and> a * c < Suc 0" have "a*(b*c) < b"
```
```   658       by (tactic {* test [@{simproc nat_less_cancel_factor}] *}) fact
```
```   659   next
```
```   660     assume "0 < a \<and> 0 < b \<and> c < d * x" have "a*(b*c) < d*b*(x*a)"
```
```   661       by (tactic {* test [@{simproc nat_less_cancel_factor}] *}) fact
```
```   662   next
```
```   663     assume "0 < k \<longrightarrow> x \<le> y" have "x*k \<le> k*y"
```
```   664       by (tactic {* test [@{simproc nat_le_cancel_factor}] *}) fact
```
```   665   next
```
```   666     assume "0 < k \<longrightarrow> Suc 0 \<le> y" have "k \<le> k*y"
```
```   667       by (tactic {* test [@{simproc nat_le_cancel_factor}] *}) fact
```
```   668   next
```
```   669     assume "0 < b \<longrightarrow> a * c \<le> Suc 0" have "a*(b*c) \<le> b"
```
```   670       by (tactic {* test [@{simproc nat_le_cancel_factor}] *}) fact
```
```   671   next
```
```   672     assume "0 < a \<longrightarrow> 0 < b \<longrightarrow> c \<le> d * x" have "a*(b*c) \<le> d*b*(x*a)"
```
```   673       by (tactic {* test [@{simproc nat_le_cancel_factor}] *}) fact
```
```   674   next
```
```   675     assume "(if k = 0 then 0 else x div y) = uu" have "(x*k) div (k*y) = uu"
```
```   676       by (tactic {* test [@{simproc nat_div_cancel_factor}] *}) fact
```
```   677   next
```
```   678     assume "(if k = 0 then 0 else Suc 0 div y) = uu" have "k div (k*y) = uu"
```
```   679       by (tactic {* test [@{simproc nat_div_cancel_factor}] *}) fact
```
```   680   next
```
```   681     assume "(if b = 0 then 0 else a * c) = uu" have "(a*(b*c)) div (b) = uu"
```
```   682       by (tactic {* test [@{simproc nat_div_cancel_factor}] *}) fact
```
```   683   next
```
```   684     assume "(if a = 0 then 0 else if b = 0 then 0 else c div (d * x)) = uu"
```
```   685     have "(a*(b*c)) div (d*b*(x*a)) = uu"
```
```   686       by (tactic {* test [@{simproc nat_div_cancel_factor}] *}) fact
```
```   687   next
```
```   688     assume "k = 0 \<or> x dvd y" have "(x*k) dvd (k*y)"
```
```   689       by (tactic {* test [@{simproc nat_dvd_cancel_factor}] *}) fact
```
```   690   next
```
```   691     assume "k = 0 \<or> Suc 0 dvd y" have "k dvd (k*y)"
```
```   692       by (tactic {* test [@{simproc nat_dvd_cancel_factor}] *}) fact
```
```   693   next
```
```   694     assume "b = 0 \<or> a * c dvd Suc 0" have "(a*(b*c)) dvd (b)"
```
```   695       by (tactic {* test [@{simproc nat_dvd_cancel_factor}] *}) fact
```
```   696   next
```
```   697     assume "b = 0 \<or> Suc 0 dvd a * c" have "b dvd (a*(b*c))"
```
```   698       by (tactic {* test [@{simproc nat_dvd_cancel_factor}] *}) fact
```
```   699   next
```
```   700     assume "a = 0 \<or> b = 0 \<or> c dvd d * x" have "(a*(b*c)) dvd (d*b*(x*a))"
```
```   701       by (tactic {* test [@{simproc nat_dvd_cancel_factor}] *}) fact
```
```   702   }
```
```   703 end
```
```   704
```
```   705 subsection {* Numeral-cancellation simprocs for type @{typ nat} *}
```
```   706
```
```   707 notepad begin
```
```   708   fix x y z :: nat
```
```   709   {
```
```   710     assume "3 * x = 4 * y" have "9*x = 12 * y"
```
```   711       by (tactic {* test [@{simproc nat_eq_cancel_numeral_factor}] *}) fact
```
```   712   next
```
```   713     assume "3 * x < 4 * y" have "9*x < 12 * y"
```
```   714       by (tactic {* test [@{simproc nat_less_cancel_numeral_factor}] *}) fact
```
```   715   next
```
```   716     assume "3 * x \<le> 4 * y" have "9*x \<le> 12 * y"
```
```   717       by (tactic {* test [@{simproc nat_le_cancel_numeral_factor}] *}) fact
```
```   718   next
```
```   719     assume "(3 * x) div (4 * y) = z" have "(9*x) div (12 * y) = z"
```
```   720       by (tactic {* test [@{simproc nat_div_cancel_numeral_factor}] *}) fact
```
```   721   next
```
```   722     assume "(3 * x) dvd (4 * y)" have "(9*x) dvd (12 * y)"
```
```   723       by (tactic {* test [@{simproc nat_dvd_cancel_numeral_factor}] *}) fact
```
```   724   }
```
```   725 end
```
```   726
```
```   727 subsection {* Integer numeral div/mod simprocs *}
```
```   728
```
```   729 notepad begin
```
```   730   have "(10::int) div 3 = 3"
```
```   731     by (tactic {* test [@{simproc binary_int_div}] *})
```
```   732   have "(10::int) mod 3 = 1"
```
```   733     by (tactic {* test [@{simproc binary_int_mod}] *})
```
```   734   have "(10::int) div -3 = -4"
```
```   735     by (tactic {* test [@{simproc binary_int_div}] *})
```
```   736   have "(10::int) mod -3 = -2"
```
```   737     by (tactic {* test [@{simproc binary_int_mod}] *})
```
```   738   have "(-10::int) div 3 = -4"
```
```   739     by (tactic {* test [@{simproc binary_int_div}] *})
```
```   740   have "(-10::int) mod 3 = 2"
```
```   741     by (tactic {* test [@{simproc binary_int_mod}] *})
```
```   742   have "(-10::int) div -3 = 3"
```
```   743     by (tactic {* test [@{simproc binary_int_div}] *})
```
```   744   have "(-10::int) mod -3 = -1"
```
```   745     by (tactic {* test [@{simproc binary_int_mod}] *})
```
```   746   have "(8452::int) mod 3 = 1"
```
```   747     by (tactic {* test [@{simproc binary_int_mod}] *})
```
```   748   have "(59485::int) div 434 = 137"
```
```   749     by (tactic {* test [@{simproc binary_int_div}] *})
```
```   750   have "(1000006::int) mod 10 = 6"
```
```   751     by (tactic {* test [@{simproc binary_int_mod}] *})
```
```   752   have "10000000 div 2 = (5000000::int)"
```
```   753     by (tactic {* test [@{simproc binary_int_div}] *})
```
```   754   have "10000001 mod 2 = (1::int)"
```
```   755     by (tactic {* test [@{simproc binary_int_mod}] *})
```
```   756   have "10000055 div 32 = (312501::int)"
```
```   757     by (tactic {* test [@{simproc binary_int_div}] *})
```
```   758   have "10000055 mod 32 = (23::int)"
```
```   759     by (tactic {* test [@{simproc binary_int_mod}] *})
```
```   760   have "100094 div 144 = (695::int)"
```
```   761     by (tactic {* test [@{simproc binary_int_div}] *})
```
```   762   have "100094 mod 144 = (14::int)"
```
```   763     by (tactic {* test [@{simproc binary_int_mod}] *})
```
```   764 end
```
```   765
```
```   766 end
```