src/HOL/ex/Simproc_Tests.thy
author huffman
Fri, 11 Nov 2011 11:30:31 +0100
changeset 45463 9a588a835c1e
parent 45462 aba629d6cee5
child 45464 5a5a6e6c6789
permissions -rw-r--r--
use simproc_setup for the remaining nat_numeral simprocs
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
45224
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
     1
(*  Title:      HOL/ex/Simproc_Tests.thy
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
     2
    Author:     Brian Huffman
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
     3
*)
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
     4
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
     5
header {* Testing of arithmetic simprocs *}
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
     6
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
     7
theory Simproc_Tests
45462
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
     8
imports Main
45224
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
     9
begin
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
    10
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
    11
text {*
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
    12
  This theory tests the various simprocs defined in
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
    13
  @{file "~~/src/HOL/Numeral_Simprocs.thy"}. Many of the tests
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
    14
  are derived from commented-out code originally found in
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
    15
  @{file "~~/src/HOL/Tools/numeral_simprocs.ML"}.
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
    16
*}
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
    17
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
    18
subsection {* ML bindings *}
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
    19
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
    20
ML {*
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
    21
  fun test ps = CHANGED (asm_simp_tac (HOL_basic_ss addsimprocs ps) 1)
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
    22
*}
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
    23
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
    24
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
    25
subsection {* @{text int_combine_numerals} *}
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
    26
45435
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    27
notepad begin
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    28
  fix a b c d oo uu i j k l u v w x y z :: "'a::number_ring"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    29
  {
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    30
    assume "10 + (2 * l + oo) = uu"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    31
    have "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = uu"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    32
      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    33
  next
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    34
    assume "-3 + (i + (j + k)) = y"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    35
    have "(i + j + 12 + k) - 15 = y"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    36
      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    37
  next
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    38
    assume "7 + (i + (j + k)) = y"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    39
    have "(i + j + 12 + k) - 5 = y"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    40
      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    41
  next
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    42
    assume "-4 * (u * v) + (2 * x + y) = w"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    43
    have "(2*x - (u*v) + y) - v*3*u = w"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    44
      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    45
  next
45437
958d19d3405b tune post-processing of simproc-generated rules so they won't produce Numeral0 or Numeral1
huffman
parents: 45436
diff changeset
    46
    assume "2 * x * u * v + y = w"
45435
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    47
    have "(2*x*u*v + (u*v)*4 + y) - v*u*4 = w"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    48
      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    49
  next
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    50
    assume "3 * (u * v) + (2 * x * u * v + y) = w"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    51
    have "(2*x*u*v + (u*v)*4 + y) - v*u = w"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    52
      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    53
  next
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    54
    assume "-3 * (u * v) + (- (x * u * v) + - y) = w"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    55
    have "u*v - (x*u*v + (u*v)*4 + y) = w"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    56
      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    57
  next
45437
958d19d3405b tune post-processing of simproc-generated rules so they won't produce Numeral0 or Numeral1
huffman
parents: 45436
diff changeset
    58
    assume "a + - c = d"
45435
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    59
    have "a + -(b+c) + b = d"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    60
      apply (simp only: minus_add_distrib)
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    61
      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    62
  next
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    63
    assume "-2 * b + (a + - c) = d"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    64
    have "a + -(b+c) - b = d"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    65
      apply (simp only: minus_add_distrib)
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    66
      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    67
  next
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    68
    assume "-7 + (i + (j + (k + (- u + - y)))) = z"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    69
    have "(i + j + -2 + k) - (u + 5 + y) = z"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    70
      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    71
  next
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    72
    assume "-27 + (i + (j + k)) = y"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    73
    have "(i + j + -12 + k) - 15 = y"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    74
      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    75
  next
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    76
    assume "27 + (i + (j + k)) = y"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    77
    have "(i + j + 12 + k) - -15 = y"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    78
      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    79
  next
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    80
    assume "3 + (i + (j + k)) = y"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    81
    have "(i + j + -12 + k) - -15 = y"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    82
      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    83
  }
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    84
end
45224
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
    85
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
    86
subsection {* @{text inteq_cancel_numerals} *}
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
    87
45435
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    88
notepad begin
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    89
  fix i j k u vv w y z w' y' z' :: "'a::number_ring"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    90
  {
45437
958d19d3405b tune post-processing of simproc-generated rules so they won't produce Numeral0 or Numeral1
huffman
parents: 45436
diff changeset
    91
    assume "u = 0" have "2*u = u"
45435
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    92
      by (tactic {* test [@{simproc inteq_cancel_numerals}] *}) fact
45224
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
    93
(* conclusion matches Rings.ring_1_no_zero_divisors_class.mult_cancel_right2 *)
45435
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    94
  next
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    95
    assume "i + (j + k) = 3 + (u + y)"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    96
    have "(i + j + 12 + k) = u + 15 + y"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    97
      by (tactic {* test [@{simproc inteq_cancel_numerals}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    98
  next
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
    99
    assume "7 + (j + (i + k)) = y"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   100
    have "(i + j*2 + 12 + k) = j + 5 + y"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   101
      by (tactic {* test [@{simproc inteq_cancel_numerals}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   102
  next
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   103
    assume "u + (6*z + (4*y + 6*w)) = 6*z' + (4*y' + (6*w' + vv))"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   104
    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"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   105
      by (tactic {* test [@{simproc int_combine_numerals}, @{simproc inteq_cancel_numerals}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   106
  }
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   107
end
45224
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
   108
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
   109
subsection {* @{text intless_cancel_numerals} *}
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
   110
45435
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   111
notepad begin
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   112
  fix b c i j k u y :: "'a::{linordered_idom,number_ring}"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   113
  {
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   114
    assume "y < 2 * b" have "y - b < b"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   115
      by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   116
  next
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   117
    assume "c + y < 4 * b" have "y - (3*b + c) < b - 2*c"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   118
      by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   119
  next
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   120
    assume "i + (j + k) < 8 + (u + y)"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   121
    have "(i + j + -3 + k) < u + 5 + y"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   122
      by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   123
  next
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   124
    assume "9 + (i + (j + k)) < u + y"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   125
    have "(i + j + 3 + k) < u + -6 + y"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   126
      by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   127
  }
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   128
end
45224
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
   129
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
   130
subsection {* @{text ring_eq_cancel_numeral_factor} *}
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
   131
45435
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   132
notepad begin
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   133
  fix x y :: "'a::{idom,ring_char_0,number_ring}"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   134
  {
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   135
    assume "3*x = 4*y" have "9*x = 12 * y"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   136
      by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   137
  next
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   138
    assume "-3*x = 4*y" have "-99*x = 132 * y"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   139
      by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   140
  next
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   141
    assume "111*x = -44*y" have "999*x = -396 * y"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   142
      by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   143
  next
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   144
    assume "11*x = 9*y" have "-99*x = -81 * y"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   145
      by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   146
  next
45437
958d19d3405b tune post-processing of simproc-generated rules so they won't produce Numeral0 or Numeral1
huffman
parents: 45436
diff changeset
   147
    assume "2*x = y" have "-2 * x = -1 * y"
45435
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   148
      by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   149
  next
45437
958d19d3405b tune post-processing of simproc-generated rules so they won't produce Numeral0 or Numeral1
huffman
parents: 45436
diff changeset
   150
    assume "2*x = y" have "-2 * x = -y"
45435
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   151
      by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   152
  }
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   153
end
45224
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
   154
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
   155
subsection {* @{text int_div_cancel_numeral_factors} *}
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
   156
45435
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   157
notepad begin
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   158
  fix x y z :: "'a::{semiring_div,ring_char_0,number_ring}"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   159
  {
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   160
    assume "(3*x) div (4*y) = z" have "(9*x) div (12*y) = z"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   161
      by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   162
  next
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   163
    assume "(-3*x) div (4*y) = z" have "(-99*x) div (132*y) = z"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   164
      by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   165
  next
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   166
    assume "(111*x) div (-44*y) = z" have "(999*x) div (-396*y) = z"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   167
      by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   168
  next
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   169
    assume "(11*x) div (9*y) = z" have "(-99*x) div (-81*y) = z"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   170
      by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   171
  next
45437
958d19d3405b tune post-processing of simproc-generated rules so they won't produce Numeral0 or Numeral1
huffman
parents: 45436
diff changeset
   172
    assume "(2*x) div y = z"
45435
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   173
    have "(-2 * x) div (-1 * y) = z"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   174
      by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   175
  }
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   176
end
45224
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
   177
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
   178
subsection {* @{text ring_less_cancel_numeral_factor} *}
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
   179
45435
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   180
notepad begin
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   181
  fix x y :: "'a::{linordered_idom,number_ring}"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   182
  {
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   183
    assume "3*x < 4*y" have "9*x < 12 * y"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   184
      by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   185
  next
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   186
    assume "-3*x < 4*y" have "-99*x < 132 * y"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   187
      by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   188
  next
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   189
    assume "111*x < -44*y" have "999*x < -396 * y"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   190
      by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   191
  next
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   192
    assume "9*y < 11*x" have "-99*x < -81 * y"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   193
      by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   194
  next
45437
958d19d3405b tune post-processing of simproc-generated rules so they won't produce Numeral0 or Numeral1
huffman
parents: 45436
diff changeset
   195
    assume "y < 2*x" have "-2 * x < -y"
45435
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   196
      by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   197
  next
45437
958d19d3405b tune post-processing of simproc-generated rules so they won't produce Numeral0 or Numeral1
huffman
parents: 45436
diff changeset
   198
    assume "23*y < x" have "-x < -23 * y"
45435
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   199
      by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   200
  }
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   201
end
45224
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
   202
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
   203
subsection {* @{text ring_le_cancel_numeral_factor} *}
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
   204
45435
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   205
notepad begin
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   206
  fix x y :: "'a::{linordered_idom,number_ring}"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   207
  {
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   208
    assume "3*x \<le> 4*y" have "9*x \<le> 12 * y"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   209
      by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   210
  next
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   211
    assume "-3*x \<le> 4*y" have "-99*x \<le> 132 * y"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   212
      by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   213
  next
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   214
    assume "111*x \<le> -44*y" have "999*x \<le> -396 * y"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   215
      by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   216
  next
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   217
    assume "9*y \<le> 11*x" have "-99*x \<le> -81 * y"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   218
      by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   219
  next
45437
958d19d3405b tune post-processing of simproc-generated rules so they won't produce Numeral0 or Numeral1
huffman
parents: 45436
diff changeset
   220
    assume "y \<le> 2*x" have "-2 * x \<le> -1 * y"
45435
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   221
      by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   222
  next
45437
958d19d3405b tune post-processing of simproc-generated rules so they won't produce Numeral0 or Numeral1
huffman
parents: 45436
diff changeset
   223
    assume "23*y \<le> x" have "-x \<le> -23 * y"
45435
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   224
      by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   225
  next
45437
958d19d3405b tune post-processing of simproc-generated rules so they won't produce Numeral0 or Numeral1
huffman
parents: 45436
diff changeset
   226
    assume "y \<le> 0" have "0 \<le> y * -2"
45435
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   227
      by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   228
  next
45437
958d19d3405b tune post-processing of simproc-generated rules so they won't produce Numeral0 or Numeral1
huffman
parents: 45436
diff changeset
   229
    assume "- x \<le> y" have "- (2 * x) \<le> 2*y"
45435
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   230
      by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   231
  }
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   232
end
45224
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
   233
45285
299abd2931d5 ex/Simproc_Tests.thy: remove duplicate simprocs
huffman
parents: 45284
diff changeset
   234
subsection {* @{text divide_cancel_numeral_factor} *}
45224
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
   235
45435
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   236
notepad begin
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   237
  fix x y z :: "'a::{field_inverse_zero,ring_char_0,number_ring}"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   238
  {
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   239
    assume "(3*x) / (4*y) = z" have "(9*x) / (12 * y) = z"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   240
      by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   241
  next
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   242
    assume "(-3*x) / (4*y) = z" have "(-99*x) / (132 * y) = z"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   243
      by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   244
  next
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   245
    assume "(111*x) / (-44*y) = z" have "(999*x) / (-396 * y) = z"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   246
      by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   247
  next
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   248
    assume "(11*x) / (9*y) = z" have "(-99*x) / (-81 * y) = z"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   249
      by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   250
  next
45437
958d19d3405b tune post-processing of simproc-generated rules so they won't produce Numeral0 or Numeral1
huffman
parents: 45436
diff changeset
   251
    assume "(2*x) / y = z" have "(-2 * x) / (-1 * y) = z"
45435
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   252
      by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   253
  }
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   254
end
45224
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
   255
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
   256
subsection {* @{text ring_eq_cancel_factor} *}
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
   257
45435
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   258
notepad begin
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   259
  fix a b c d k x y :: "'a::idom"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   260
  {
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   261
    assume "k = 0 \<or> x = y" have "x*k = k*y"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   262
      by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   263
  next
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   264
    assume "k = 0 \<or> 1 = y" have "k = k*y"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   265
      by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   266
  next
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   267
    assume "b = 0 \<or> a*c = 1" have "a*(b*c) = b"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   268
      by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   269
  next
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   270
    assume "a = 0 \<or> b = 0 \<or> c = d*x" have "a*(b*c) = d*b*(x*a)"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   271
      by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   272
  next
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   273
    assume "k = 0 \<or> x = y" have "x*k = k*y"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   274
      by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   275
  next
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   276
    assume "k = 0 \<or> 1 = y" have "k = k*y"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   277
      by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   278
  }
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   279
end
45224
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
   280
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
   281
subsection {* @{text int_div_cancel_factor} *}
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
   282
45435
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   283
notepad begin
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   284
  fix a b c d k uu x y :: "'a::semiring_div"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   285
  {
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   286
    assume "(if k = 0 then 0 else x div y) = uu"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   287
    have "(x*k) div (k*y) = uu"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   288
      by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   289
  next
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   290
    assume "(if k = 0 then 0 else 1 div y) = uu"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   291
    have "(k) div (k*y) = uu"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   292
      by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   293
  next
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   294
    assume "(if b = 0 then 0 else a * c) = uu"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   295
    have "(a*(b*c)) div b = uu"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   296
      by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   297
  next
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   298
    assume "(if a = 0 then 0 else if b = 0 then 0 else c div (d * x)) = uu"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   299
    have "(a*(b*c)) div (d*b*(x*a)) = uu"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   300
      by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   301
  }
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   302
end
45224
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
   303
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
   304
subsection {* @{text divide_cancel_factor} *}
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
   305
45435
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   306
notepad begin
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   307
  fix a b c d k uu x y :: "'a::field_inverse_zero"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   308
  {
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   309
    assume "(if k = 0 then 0 else x / y) = uu"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   310
    have "(x*k) / (k*y) = uu"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   311
      by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   312
  next
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   313
    assume "(if k = 0 then 0 else 1 / y) = uu"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   314
    have "(k) / (k*y) = uu"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   315
      by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   316
  next
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   317
    assume "(if b = 0 then 0 else a * c / 1) = uu"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   318
    have "(a*(b*c)) / b = uu"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   319
      by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   320
  next
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   321
    assume "(if a = 0 then 0 else if b = 0 then 0 else c / (d * x)) = uu"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   322
    have "(a*(b*c)) / (d*b*(x*a)) = uu"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   323
      by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   324
  }
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   325
end
45224
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
   326
45462
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   327
lemma
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   328
  fixes a b c d x y z :: "'a::linordered_field_inverse_zero"
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   329
  shows "a*(b*c)/(y*z) = d*(b)*(x*a)/z"
45224
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
   330
oops -- "FIXME: need simproc to cover this case"
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
   331
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
   332
subsection {* @{text linordered_ring_less_cancel_factor} *}
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
   333
45435
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   334
notepad begin
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   335
  fix x y z :: "'a::linordered_idom"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   336
  {
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   337
    assume "0 < z \<Longrightarrow> x < y" have "0 < z \<Longrightarrow> x*z < y*z"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   338
      by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   339
  next
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   340
    assume "0 < z \<Longrightarrow> x < y" have "0 < z \<Longrightarrow> x*z < z*y"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   341
      by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   342
  next
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   343
    assume "0 < z \<Longrightarrow> x < y" have "0 < z \<Longrightarrow> z*x < y*z"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   344
      by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   345
  next
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   346
    assume "0 < z \<Longrightarrow> x < y" have "0 < z \<Longrightarrow> z*x < z*y"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   347
      by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   348
  }
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   349
end
45224
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
   350
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
   351
subsection {* @{text linordered_ring_le_cancel_factor} *}
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
   352
45435
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   353
notepad begin
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   354
  fix x y z :: "'a::linordered_idom"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   355
  {
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   356
    assume "0 < z \<Longrightarrow> x \<le> y" have "0 < z \<Longrightarrow> x*z \<le> y*z"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   357
      by (tactic {* test [@{simproc linordered_ring_le_cancel_factor}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   358
  next
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   359
    assume "0 < z \<Longrightarrow> x \<le> y" have "0 < z \<Longrightarrow> z*x \<le> z*y"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   360
      by (tactic {* test [@{simproc linordered_ring_le_cancel_factor}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   361
  }
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   362
end
45224
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
   363
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
   364
subsection {* @{text field_combine_numerals} *}
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
   365
45435
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   366
notepad begin
45437
958d19d3405b tune post-processing of simproc-generated rules so they won't produce Numeral0 or Numeral1
huffman
parents: 45436
diff changeset
   367
  fix x y z uu :: "'a::{field_inverse_zero,ring_char_0,number_ring}"
45435
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   368
  {
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   369
    assume "5 / 6 * x = uu" have "x / 2 + x / 3 = uu"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   370
      by (tactic {* test [@{simproc field_combine_numerals}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   371
  next
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   372
    assume "6 / 9 * x + y = uu" have "x / 3 + y + x / 3 = uu"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   373
      by (tactic {* test [@{simproc field_combine_numerals}] *}) fact
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   374
  next
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   375
    assume "9 / 9 * x = uu" have "2 * x / 3 + x / 3 = uu"
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   376
      by (tactic {* test [@{simproc field_combine_numerals}] *}) fact
45437
958d19d3405b tune post-processing of simproc-generated rules so they won't produce Numeral0 or Numeral1
huffman
parents: 45436
diff changeset
   377
  next
958d19d3405b tune post-processing of simproc-generated rules so they won't produce Numeral0 or Numeral1
huffman
parents: 45436
diff changeset
   378
    assume "y + z = uu"
958d19d3405b tune post-processing of simproc-generated rules so they won't produce Numeral0 or Numeral1
huffman
parents: 45436
diff changeset
   379
    have "x / 2 + y - 3 * x / 6 + z = uu"
958d19d3405b tune post-processing of simproc-generated rules so they won't produce Numeral0 or Numeral1
huffman
parents: 45436
diff changeset
   380
      by (tactic {* test [@{simproc field_combine_numerals}] *}) fact
958d19d3405b tune post-processing of simproc-generated rules so they won't produce Numeral0 or Numeral1
huffman
parents: 45436
diff changeset
   381
  next
958d19d3405b tune post-processing of simproc-generated rules so they won't produce Numeral0 or Numeral1
huffman
parents: 45436
diff changeset
   382
    assume "1 / 15 * x + y = uu"
958d19d3405b tune post-processing of simproc-generated rules so they won't produce Numeral0 or Numeral1
huffman
parents: 45436
diff changeset
   383
    have "7 * x / 5 + y - 4 * x / 3 = uu"
958d19d3405b tune post-processing of simproc-generated rules so they won't produce Numeral0 or Numeral1
huffman
parents: 45436
diff changeset
   384
      by (tactic {* test [@{simproc field_combine_numerals}] *}) fact
45435
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   385
  }
d660c4b9daa6 add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents: 45285
diff changeset
   386
end
45224
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
   387
45462
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   388
lemma
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   389
  fixes x :: "'a::{linordered_field_inverse_zero,number_ring}"
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   390
  shows "2/3 * x + x / 3 = uu"
45284
ae78a4ffa81d use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents: 45270
diff changeset
   391
apply (tactic {* test [@{simproc field_combine_numerals}] *})?
45224
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
   392
oops -- "FIXME: test fails"
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
   393
45462
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   394
subsection {* @{text nat_combine_numerals} *}
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   395
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   396
notepad begin
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   397
  fix i j k m n u :: nat
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   398
  {
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   399
    assume "4*k = u" have "k + 3*k = u"
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   400
      by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   401
  next
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   402
    assume "4 * Suc 0 + i = u" have "Suc (i + 3) = u"
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   403
      by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   404
  next
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   405
    assume "4 * Suc 0 + (i + (j + k)) = u" have "Suc (i + j + 3 + k) = u"
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   406
      by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   407
  next
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   408
    assume "2 * j + 4 * k = u" have "k + j + 3*k + j = u"
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   409
      by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   410
  next
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   411
    assume "6 * Suc 0 + (5 * (i * j) + (4 * k + i)) = u"
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   412
    have "Suc (j*i + i + k + 5 + 3*k + i*j*4) = u"
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   413
      by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   414
  next
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   415
    assume "5 * (m * n) = u" have "(2*n*m) + (3*(m*n)) = u"
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   416
      by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   417
  }
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   418
end
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   419
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   420
(*negative numerals: FAIL*)
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   421
lemma "Suc (i + j + -3 + k) = u"
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   422
apply (tactic {* test [@{simproc nat_combine_numerals}] *})?
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   423
oops
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   424
45436
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   425
subsection {* @{text nateq_cancel_numerals} *}
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   426
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   427
notepad begin
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   428
  fix i j k l oo u uu vv w y z w' y' z' :: "nat"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   429
  {
45462
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   430
    assume "Suc 0 * u = 0" have "2*u = u"
45436
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   431
      by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   432
  next
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   433
    assume "Suc 0 * u = Suc 0" have "2*u = Suc (u)"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   434
      by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   435
  next
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   436
    assume "i + (j + k) = 3 * Suc 0 + (u + y)"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   437
    have "(i + j + 12 + k) = u + 15 + y"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   438
      by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   439
  next
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   440
    assume "7 * Suc 0 + (i + (j + k)) = u + y"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   441
    have "(i + j + 12 + k) = u + 5 + y"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   442
      by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   443
  next
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   444
    assume "11 * Suc 0 + (i + (j + k)) = u + y"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   445
    have "(i + j + 12 + k) = Suc (u + y)"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   446
      by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   447
  next
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   448
    assume "i + (j + k) = 2 * Suc 0 + (u + y)"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   449
    have "(i + j + 5 + k) = Suc (Suc (Suc (Suc (Suc (Suc (Suc (u + y)))))))"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   450
      by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   451
  next
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   452
    assume "Suc 0 * u + (2 * y + 3 * z) = Suc 0"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   453
    have "2*y + 3*z + 2*u = Suc (u)"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   454
      by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   455
  next
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   456
    assume "Suc 0 * u + (2 * y + (3 * z + (6 * w + (2 * y + 3 * z)))) = Suc 0"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   457
    have "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = Suc (u)"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   458
      by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   459
  next
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   460
    assume "Suc 0 * u + (2 * y + (3 * z + (6 * w + (2 * y + 3 * z)))) =
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   461
      2 * y' + (3 * z' + (6 * w' + (2 * y' + (3 * z' + vv))))"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   462
    have "2*y + 3*z + 6*w + 2*y + 3*z + 2*u =
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   463
      2*y' + 3*z' + 6*w' + 2*y' + 3*z' + u + vv"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   464
      by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   465
  next
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   466
    assume "2 * u + (2 * z + (5 * Suc 0 + 2 * y)) = vv"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   467
    have "6 + 2*y + 3*z + 4*u = Suc (vv + 2*u + z)"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   468
      by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   469
  }
45224
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff changeset
   470
end
45436
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   471
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   472
subsection {* @{text natless_cancel_numerals} *}
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   473
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   474
notepad begin
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   475
  fix length :: "'a \<Rightarrow> nat" and l1 l2 xs :: "'a" and f :: "nat \<Rightarrow> 'a"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   476
  fix c i j k l oo u uu vv w y z w' y' z' :: "nat"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   477
  {
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   478
    assume "0 < j" have "(2*length xs < 2*length xs + j)"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   479
      by (tactic {* test [@{simproc natless_cancel_numerals}] *}) fact
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   480
  next
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   481
    assume "0 < j" have "(2*length xs < length xs * 2 + j)"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   482
      by (tactic {* test [@{simproc natless_cancel_numerals}] *}) fact
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   483
  next
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   484
    assume "i + (j + k) < u + y"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   485
    have "(i + j + 5 + k) < Suc (Suc (Suc (Suc (Suc (u + y)))))"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   486
      by (tactic {* test [@{simproc natless_cancel_numerals}] *}) fact
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   487
  next
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   488
    assume "0 < Suc 0 * (m * n) + u" have "(2*n*m) < (3*(m*n)) + u"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   489
      by (tactic {* test [@{simproc natless_cancel_numerals}] *}) fact
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   490
  next
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   491
    (* FIXME: negative numerals fail
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   492
    have "(i + j + -23 + (k::nat)) < u + 15 + y"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   493
      apply (tactic {* test [@{simproc natless_cancel_numerals}] *})?
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   494
      sorry
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   495
    have "(i + j + 3 + (k::nat)) < u + -15 + y"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   496
      apply (tactic {* test [@{simproc natless_cancel_numerals}] *})?
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   497
      sorry*)
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   498
  }
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   499
end
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   500
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   501
subsection {* @{text natle_cancel_numerals} *}
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   502
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   503
notepad begin
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   504
  fix length :: "'a \<Rightarrow> nat" and l2 l3 :: "'a" and f :: "nat \<Rightarrow> 'a"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   505
  fix c e i j k l oo u uu vv w y z w' y' z' :: "nat"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   506
  {
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   507
    assume "u + y \<le> 36 * Suc 0 + (i + (j + k))"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   508
    have "Suc (Suc (Suc (Suc (Suc (u + y))))) \<le> ((i + j) + 41 + k)"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   509
      by (tactic {* test [@{simproc natle_cancel_numerals}] *}) fact
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   510
  next
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   511
    assume "5 * Suc 0 + (case length (f c) of 0 \<Rightarrow> 0 | Suc k \<Rightarrow> k) = 0"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   512
    have "(Suc (Suc (Suc (Suc (Suc (Suc (case length (f c) of 0 => 0 | Suc k => k)))))) \<le> Suc 0)"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   513
      by (tactic {* test [@{simproc natle_cancel_numerals}] *}) fact
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   514
  next
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   515
    assume "6 + length l2 = 0" have "Suc (Suc (Suc (Suc (Suc (Suc (length l1 + length l2)))))) \<le> length l1"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   516
      by (tactic {* test [@{simproc natle_cancel_numerals}] *}) fact
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   517
  next
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   518
    assume "5 + length l3 = 0"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   519
    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))"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   520
      by (tactic {* test [@{simproc natle_cancel_numerals}] *}) fact
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   521
  next
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   522
    assume "5 + length (compT P E (A \<union> A' e) ST mxr c) = 0"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   523
    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))"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   524
      by (tactic {* test [@{simproc natle_cancel_numerals}] *}) fact
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   525
  }
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   526
end
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   527
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   528
subsection {* @{text natdiff_cancel_numerals} *}
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   529
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   530
notepad begin
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   531
  fix length :: "'a \<Rightarrow> nat" and l2 l3 :: "'a" and f :: "nat \<Rightarrow> 'a"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   532
  fix c e i j k l oo u uu vv v w x y z zz w' y' z' :: "nat"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   533
  {
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   534
    assume "i + (j + k) - 3 * Suc 0 = y" have "(i + j + 12 + k) - 15 = y"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   535
      by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   536
  next
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   537
    assume "7 * Suc 0 + (i + (j + k)) - 0 = y" have "(i + j + 12 + k) - 5 = y"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   538
      by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   539
  next
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   540
    assume "u - Suc 0 * Suc 0 = y" have "Suc u - 2 = y"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   541
      by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   542
  next
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   543
    assume "Suc 0 * Suc 0 + u - 0 = y" have "Suc (Suc (Suc u)) - 2 = y"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   544
      by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   545
  next
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   546
    assume "Suc 0 * Suc 0 + (i + (j + k)) - 0 = y"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   547
    have "(i + j + 2 + k) - 1 = y"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   548
      by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   549
  next
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   550
    assume "i + (j + k) - Suc 0 * Suc 0 = y"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   551
    have "(i + j + 1 + k) - 2 = y"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   552
      by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   553
  next
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   554
    assume "2 * x + y - 2 * (u * v) = w"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   555
    have "(2*x + (u*v) + y) - v*3*u = w"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   556
      by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   557
  next
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   558
    assume "2 * x * u * v + (5 + y) - 0 = w"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   559
    have "(2*x*u*v + 5 + (u*v)*4 + y) - v*u*4 = w"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   560
      by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   561
  next
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   562
    assume "3 * (u * v) + (2 * x * u * v + y) - 0 = w"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   563
    have "(2*x*u*v + (u*v)*4 + y) - v*u = w"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   564
      by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   565
  next
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   566
    assume "3 * u + (2 + (2 * x * u * v + y)) - 0 = w"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   567
    have "Suc (Suc (2*x*u*v + u*4 + y)) - u = w"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   568
      by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   569
  next
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   570
    assume "Suc (Suc 0 * (u * v)) - 0 = w"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   571
    have "Suc ((u*v)*4) - v*3*u = w"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   572
      by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   573
  next
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   574
    assume "2 - 0 = w" have "Suc (Suc ((u*v)*3)) - v*3*u = w"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   575
      by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   576
  next
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   577
    assume "17 * Suc 0 + (i + (j + k)) - (u + y) = zz"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   578
    have "(i + j + 32 + k) - (u + 15 + y) = zz"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   579
      by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   580
  next
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   581
    assume "u + y - 0 = v" have "Suc (Suc (Suc (Suc (Suc (u + y))))) - 5 = v"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   582
      by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   583
  next
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   584
    (* FIXME: negative numerals fail
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   585
    have "(i + j + -12 + k) - 15 = y"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   586
      apply (tactic {* test [@{simproc natdiff_cancel_numerals}] *})?
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   587
      sorry
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   588
    have "(i + j + 12 + k) - -15 = y"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   589
      apply (tactic {* test [@{simproc natdiff_cancel_numerals}] *})?
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   590
      sorry
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   591
    have "(i + j + -12 + k) - -15 = y"
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   592
      apply (tactic {* test [@{simproc natdiff_cancel_numerals}] *})?
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   593
      sorry*)
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   594
  }
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   595
end
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   596
45462
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   597
subsection {* Factor-cancellation simprocs for type @{typ nat} *}
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   598
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   599
text {* @{text nat_eq_cancel_factor}, @{text nat_less_cancel_factor},
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   600
@{text nat_le_cancel_factor}, @{text nat_divide_cancel_factor}, and
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   601
@{text nat_dvd_cancel_factor}. *}
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   602
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   603
notepad begin
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   604
  fix a b c d k x y uu :: nat
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   605
  {
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   606
    assume "k = 0 \<or> x = y" have "x*k = k*y"
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   607
      by (tactic {* test [@{simproc nat_eq_cancel_factor}] *}) fact
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   608
  next
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   609
    assume "k = 0 \<or> Suc 0 = y" have "k = k*y"
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   610
      by (tactic {* test [@{simproc nat_eq_cancel_factor}] *}) fact
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   611
  next
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   612
    assume "b = 0 \<or> a * c = Suc 0" have "a*(b*c) = b"
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   613
      by (tactic {* test [@{simproc nat_eq_cancel_factor}] *}) fact
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   614
  next
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   615
    assume "a = 0 \<or> b = 0 \<or> c = d * x" have "a*(b*c) = d*b*(x*a)"
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   616
      by (tactic {* test [@{simproc nat_eq_cancel_factor}] *}) fact
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   617
  next
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   618
    assume "0 < k \<and> x < y" have "x*k < k*y"
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   619
      by (tactic {* test [@{simproc nat_less_cancel_factor}] *}) fact
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   620
  next
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   621
    assume "0 < k \<and> Suc 0 < y" have "k < k*y"
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   622
      by (tactic {* test [@{simproc nat_less_cancel_factor}] *}) fact
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   623
  next
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   624
    assume "0 < b \<and> a * c < Suc 0" have "a*(b*c) < b"
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   625
      by (tactic {* test [@{simproc nat_less_cancel_factor}] *}) fact
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   626
  next
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   627
    assume "0 < a \<and> 0 < b \<and> c < d * x" have "a*(b*c) < d*b*(x*a)"
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   628
      by (tactic {* test [@{simproc nat_less_cancel_factor}] *}) fact
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   629
  next
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   630
    assume "0 < k \<longrightarrow> x \<le> y" have "x*k \<le> k*y"
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   631
      by (tactic {* test [@{simproc nat_le_cancel_factor}] *}) fact
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   632
  next
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   633
    assume "0 < k \<longrightarrow> Suc 0 \<le> y" have "k \<le> k*y"
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   634
      by (tactic {* test [@{simproc nat_le_cancel_factor}] *}) fact
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   635
  next
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   636
    assume "0 < b \<longrightarrow> a * c \<le> Suc 0" have "a*(b*c) \<le> b"
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   637
      by (tactic {* test [@{simproc nat_le_cancel_factor}] *}) fact
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   638
  next
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   639
    assume "0 < a \<longrightarrow> 0 < b \<longrightarrow> c \<le> d * x" have "a*(b*c) \<le> d*b*(x*a)"
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   640
      by (tactic {* test [@{simproc nat_le_cancel_factor}] *}) fact
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   641
  next
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   642
    assume "(if k = 0 then 0 else x div y) = uu" have "(x*k) div (k*y) = uu"
45463
9a588a835c1e use simproc_setup for the remaining nat_numeral simprocs
huffman
parents: 45462
diff changeset
   643
      by (tactic {* test [@{simproc nat_div_cancel_factor}] *}) fact
45462
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   644
  next
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   645
    assume "(if k = 0 then 0 else Suc 0 div y) = uu" have "k div (k*y) = uu"
45463
9a588a835c1e use simproc_setup for the remaining nat_numeral simprocs
huffman
parents: 45462
diff changeset
   646
      by (tactic {* test [@{simproc nat_div_cancel_factor}] *}) fact
45462
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   647
  next
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   648
    assume "(if b = 0 then 0 else a * c) = uu" have "(a*(b*c)) div (b) = uu"
45463
9a588a835c1e use simproc_setup for the remaining nat_numeral simprocs
huffman
parents: 45462
diff changeset
   649
      by (tactic {* test [@{simproc nat_div_cancel_factor}] *}) fact
45462
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   650
  next
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   651
    assume "(if a = 0 then 0 else if b = 0 then 0 else c div (d * x)) = uu"
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   652
    have "(a*(b*c)) div (d*b*(x*a)) = uu"
45463
9a588a835c1e use simproc_setup for the remaining nat_numeral simprocs
huffman
parents: 45462
diff changeset
   653
      by (tactic {* test [@{simproc nat_div_cancel_factor}] *}) fact
45462
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   654
  next
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   655
    assume "k = 0 \<or> x dvd y" have "(x*k) dvd (k*y)"
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   656
      by (tactic {* test [@{simproc nat_dvd_cancel_factor}] *}) fact
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   657
  next
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   658
    assume "k = 0 \<or> Suc 0 dvd y" have "k dvd (k*y)"
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   659
      by (tactic {* test [@{simproc nat_dvd_cancel_factor}] *}) fact
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   660
  next
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   661
    assume "b = 0 \<or> a * c dvd Suc 0" have "(a*(b*c)) dvd (b)"
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   662
      by (tactic {* test [@{simproc nat_dvd_cancel_factor}] *}) fact
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   663
  next
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   664
    assume "b = 0 \<or> Suc 0 dvd a * c" have "b dvd (a*(b*c))"
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   665
      by (tactic {* test [@{simproc nat_dvd_cancel_factor}] *}) fact
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   666
  next
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   667
    assume "a = 0 \<or> b = 0 \<or> c dvd d * x" have "(a*(b*c)) dvd (d*b*(x*a))"
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   668
      by (tactic {* test [@{simproc nat_dvd_cancel_factor}] *}) fact
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   669
  }
45436
62bc9474d04b use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents: 45435
diff changeset
   670
end
45462
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   671
45463
9a588a835c1e use simproc_setup for the remaining nat_numeral simprocs
huffman
parents: 45462
diff changeset
   672
subsection {* Numeral-cancellation simprocs for type @{typ nat} *}
9a588a835c1e use simproc_setup for the remaining nat_numeral simprocs
huffman
parents: 45462
diff changeset
   673
9a588a835c1e use simproc_setup for the remaining nat_numeral simprocs
huffman
parents: 45462
diff changeset
   674
notepad begin
9a588a835c1e use simproc_setup for the remaining nat_numeral simprocs
huffman
parents: 45462
diff changeset
   675
  fix x y z :: nat
9a588a835c1e use simproc_setup for the remaining nat_numeral simprocs
huffman
parents: 45462
diff changeset
   676
  {
9a588a835c1e use simproc_setup for the remaining nat_numeral simprocs
huffman
parents: 45462
diff changeset
   677
    assume "3 * x = 4 * y" have "9*x = 12 * y"
9a588a835c1e use simproc_setup for the remaining nat_numeral simprocs
huffman
parents: 45462
diff changeset
   678
      by (tactic {* test [@{simproc nat_eq_cancel_numeral_factor}] *}) fact
9a588a835c1e use simproc_setup for the remaining nat_numeral simprocs
huffman
parents: 45462
diff changeset
   679
  next
9a588a835c1e use simproc_setup for the remaining nat_numeral simprocs
huffman
parents: 45462
diff changeset
   680
    assume "3 * x < 4 * y" have "9*x < 12 * y"
9a588a835c1e use simproc_setup for the remaining nat_numeral simprocs
huffman
parents: 45462
diff changeset
   681
      by (tactic {* test [@{simproc nat_less_cancel_numeral_factor}] *}) fact
9a588a835c1e use simproc_setup for the remaining nat_numeral simprocs
huffman
parents: 45462
diff changeset
   682
  next
9a588a835c1e use simproc_setup for the remaining nat_numeral simprocs
huffman
parents: 45462
diff changeset
   683
    assume "3 * x \<le> 4 * y" have "9*x \<le> 12 * y"
9a588a835c1e use simproc_setup for the remaining nat_numeral simprocs
huffman
parents: 45462
diff changeset
   684
      by (tactic {* test [@{simproc nat_le_cancel_numeral_factor}] *}) fact
9a588a835c1e use simproc_setup for the remaining nat_numeral simprocs
huffman
parents: 45462
diff changeset
   685
  next
9a588a835c1e use simproc_setup for the remaining nat_numeral simprocs
huffman
parents: 45462
diff changeset
   686
    assume "(3 * x) div (4 * y) = z" have "(9*x) div (12 * y) = z"
9a588a835c1e use simproc_setup for the remaining nat_numeral simprocs
huffman
parents: 45462
diff changeset
   687
      by (tactic {* test [@{simproc nat_div_cancel_numeral_factor}] *}) fact
9a588a835c1e use simproc_setup for the remaining nat_numeral simprocs
huffman
parents: 45462
diff changeset
   688
  next
9a588a835c1e use simproc_setup for the remaining nat_numeral simprocs
huffman
parents: 45462
diff changeset
   689
    assume "(3 * x) dvd (4 * y)" have "(9*x) dvd (12 * y)"
9a588a835c1e use simproc_setup for the remaining nat_numeral simprocs
huffman
parents: 45462
diff changeset
   690
      by (tactic {* test [@{simproc nat_dvd_cancel_numeral_factor}] *}) fact
9a588a835c1e use simproc_setup for the remaining nat_numeral simprocs
huffman
parents: 45462
diff changeset
   691
  }
45462
aba629d6cee5 use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents: 45437
diff changeset
   692
end
45463
9a588a835c1e use simproc_setup for the remaining nat_numeral simprocs
huffman
parents: 45462
diff changeset
   693
9a588a835c1e use simproc_setup for the remaining nat_numeral simprocs
huffman
parents: 45462
diff changeset
   694
end