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