author  huffman 
Fri, 11 Nov 2011 11:30:31 +0100  
changeset 45463  9a588a835c1e 
parent 45462  aba629d6cee5 
child 45464  5a5a6e6c6789 
permissions  rwrr 
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 commentedout 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 postprocessing of simprocgenerated 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 postprocessing of simprocgenerated 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 postprocessing of simprocgenerated 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 postprocessing of simprocgenerated 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 postprocessing of simprocgenerated 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 postprocessing of simprocgenerated 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 postprocessing of simprocgenerated 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 postprocessing of simprocgenerated 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 postprocessing of simprocgenerated 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 postprocessing of simprocgenerated 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 postprocessing of simprocgenerated 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 postprocessing of simprocgenerated 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  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 postprocessing of simprocgenerated 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 postprocessing of simprocgenerated 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 postprocessing of simprocgenerated rules so they won't produce Numeral0 or Numeral1
huffman
parents:
45436
diff
changeset

377 
next 
958d19d3405b
tune postprocessing of simprocgenerated rules so they won't produce Numeral0 or Numeral1
huffman
parents:
45436
diff
changeset

378 
assume "y + z = uu" 
958d19d3405b
tune postprocessing of simprocgenerated 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 postprocessing of simprocgenerated 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 postprocessing of simprocgenerated rules so they won't produce Numeral0 or Numeral1
huffman
parents:
45436
diff
changeset

381 
next 
958d19d3405b
tune postprocessing of simprocgenerated rules so they won't produce Numeral0 or Numeral1
huffman
parents:
45436
diff
changeset

382 
assume "1 / 15 * x + y = uu" 
958d19d3405b
tune postprocessing of simprocgenerated 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 postprocessing of simprocgenerated 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 {* Factorcancellation 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 {* Numeralcancellation 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 