author  huffman 
Wed, 16 Nov 2011 15:20:27 +0100  
changeset 45530  0c4853bb77bf 
parent 45464  5a5a6e6c6789 
child 46240  933f35c4e126 
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 

45464
5a5a6e6c6789
abel_cancel.ML: avoid canceling zeros, which would cause the simproc to return a trivial rewrite;
huffman
parents:
45463
diff
changeset

24 
subsection {* Abelian group cancellation simprocs *} 
5a5a6e6c6789
abel_cancel.ML: avoid canceling zeros, which would cause the simproc to return a trivial rewrite;
huffman
parents:
45463
diff
changeset

25 

5a5a6e6c6789
abel_cancel.ML: avoid canceling zeros, which would cause the simproc to return a trivial rewrite;
huffman
parents:
45463
diff
changeset

26 
notepad begin 
5a5a6e6c6789
abel_cancel.ML: avoid canceling zeros, which would cause the simproc to return a trivial rewrite;
huffman
parents:
45463
diff
changeset

27 
fix a b c u :: "'a::ab_group_add" 
5a5a6e6c6789
abel_cancel.ML: avoid canceling zeros, which would cause the simproc to return a trivial rewrite;
huffman
parents:
45463
diff
changeset

28 
{ 
5a5a6e6c6789
abel_cancel.ML: avoid canceling zeros, which would cause the simproc to return a trivial rewrite;
huffman
parents:
45463
diff
changeset

29 
assume "(a + 0)  (b + 0) = u" have "(a + c)  (b + c) = u" 
5a5a6e6c6789
abel_cancel.ML: avoid canceling zeros, which would cause the simproc to return a trivial rewrite;
huffman
parents:
45463
diff
changeset

30 
by (tactic {* test [@{simproc abel_cancel_sum}] *}) fact 
5a5a6e6c6789
abel_cancel.ML: avoid canceling zeros, which would cause the simproc to return a trivial rewrite;
huffman
parents:
45463
diff
changeset

31 
next 
5a5a6e6c6789
abel_cancel.ML: avoid canceling zeros, which would cause the simproc to return a trivial rewrite;
huffman
parents:
45463
diff
changeset

32 
assume "a + 0 = b + 0" have "a + c = b + c" 
5a5a6e6c6789
abel_cancel.ML: avoid canceling zeros, which would cause the simproc to return a trivial rewrite;
huffman
parents:
45463
diff
changeset

33 
by (tactic {* test [@{simproc abel_cancel_relation}] *}) fact 
5a5a6e6c6789
abel_cancel.ML: avoid canceling zeros, which would cause the simproc to return a trivial rewrite;
huffman
parents:
45463
diff
changeset

34 
} 
5a5a6e6c6789
abel_cancel.ML: avoid canceling zeros, which would cause the simproc to return a trivial rewrite;
huffman
parents:
45463
diff
changeset

35 
end 
5a5a6e6c6789
abel_cancel.ML: avoid canceling zeros, which would cause the simproc to return a trivial rewrite;
huffman
parents:
45463
diff
changeset

36 
(* TODO: more tests for Groups.abel_cancel_{sum,relation} *) 
45224
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

37 

b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

38 
subsection {* @{text int_combine_numerals} *} 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

39 

45464
5a5a6e6c6789
abel_cancel.ML: avoid canceling zeros, which would cause the simproc to return a trivial rewrite;
huffman
parents:
45463
diff
changeset

40 
(* FIXME: int_combine_numerals often unnecessarily regroups addition 
5a5a6e6c6789
abel_cancel.ML: avoid canceling zeros, which would cause the simproc to return a trivial rewrite;
huffman
parents:
45463
diff
changeset

41 
and rewrites subtraction to negation. Ideally it should behave more 
5a5a6e6c6789
abel_cancel.ML: avoid canceling zeros, which would cause the simproc to return a trivial rewrite;
huffman
parents:
45463
diff
changeset

42 
like Groups.abel_cancel_sum, preserving the shape of terms as much as 
5a5a6e6c6789
abel_cancel.ML: avoid canceling zeros, which would cause the simproc to return a trivial rewrite;
huffman
parents:
45463
diff
changeset

43 
possible. *) 
5a5a6e6c6789
abel_cancel.ML: avoid canceling zeros, which would cause the simproc to return a trivial rewrite;
huffman
parents:
45463
diff
changeset

44 

45435
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

45 
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

46 
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

47 
{ 
45464
5a5a6e6c6789
abel_cancel.ML: avoid canceling zeros, which would cause the simproc to return a trivial rewrite;
huffman
parents:
45463
diff
changeset

48 
assume "a +  b = u" have "(a + c)  (b + c) = u" 
5a5a6e6c6789
abel_cancel.ML: avoid canceling zeros, which would cause the simproc to return a trivial rewrite;
huffman
parents:
45463
diff
changeset

49 
by (tactic {* test [@{simproc int_combine_numerals}] *}) fact 
5a5a6e6c6789
abel_cancel.ML: avoid canceling zeros, which would cause the simproc to return a trivial rewrite;
huffman
parents:
45463
diff
changeset

50 
next 
45435
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

51 
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

52 
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

53 
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

54 
next 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

55 
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

56 
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

57 
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

58 
next 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

59 
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

60 
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

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 "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

64 
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

65 
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

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

67 
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

68 
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

69 
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

70 
next 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

71 
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

72 
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

73 
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

74 
next 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

75 
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

76 
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

77 
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

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

79 
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

80 
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

81 
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

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 
next 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

84 
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

85 
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

86 
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

87 
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

88 
next 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

89 
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

90 
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

91 
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

92 
next 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

93 
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

94 
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

95 
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

96 
next 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

97 
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

98 
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

99 
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

100 
next 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

101 
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

102 
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

103 
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

104 
} 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

105 
end 
45224
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

106 

b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

107 
subsection {* @{text inteq_cancel_numerals} *} 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

108 

45435
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

109 
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

110 
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

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

112 
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

113 
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

114 
(* 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

115 
next 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

116 
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

117 
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

118 
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

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 "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

121 
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

122 
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

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 "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

125 
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

126 
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

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 intless_cancel_numerals} *} 
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 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

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 "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

136 
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

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 "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

139 
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

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 "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

142 
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

143 
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

144 
next 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

145 
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

146 
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

147 
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

148 
} 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

149 
end 
45224
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

150 

b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

151 
subsection {* @{text ring_eq_cancel_numeral_factor} *} 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

152 

45435
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

153 
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

154 
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

155 
{ 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

156 
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

157 
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

158 
next 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

159 
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

160 
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

161 
next 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

162 
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

163 
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

164 
next 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

165 
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

166 
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

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

168 
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

169 
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

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

171 
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

172 
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

173 
} 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

174 
end 
45224
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

175 

b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

176 
subsection {* @{text int_div_cancel_numeral_factors} *} 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

177 

45435
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

178 
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

179 
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

180 
{ 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

181 
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

182 
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

183 
next 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

184 
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

185 
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

186 
next 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

187 
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

188 
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

189 
next 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

190 
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

191 
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

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

193 
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

194 
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

195 
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

196 
} 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

197 
end 
45224
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

198 

b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

199 
subsection {* @{text ring_less_cancel_numeral_factor} *} 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

200 

45435
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

201 
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

202 
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

203 
{ 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

204 
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

205 
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

206 
next 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

207 
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

208 
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

209 
next 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

210 
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

211 
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

212 
next 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

213 
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

214 
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

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

216 
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

217 
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

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

219 
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

220 
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

221 
} 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

222 
end 
45224
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

223 

b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

224 
subsection {* @{text ring_le_cancel_numeral_factor} *} 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

225 

45435
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

226 
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

227 
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

228 
{ 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

229 
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

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 
next 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

232 
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

233 
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

234 
next 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

235 
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

236 
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

237 
next 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

238 
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

239 
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

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

241 
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

242 
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

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

244 
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

245 
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

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

247 
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

248 
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

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

250 
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

251 
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

252 
} 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

253 
end 
45224
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

254 

45285  255 
subsection {* @{text divide_cancel_numeral_factor} *} 
45224
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

256 

45435
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

257 
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

258 
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

259 
{ 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

260 
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

261 
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

262 
next 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

263 
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

264 
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

265 
next 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

266 
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

267 
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

268 
next 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

269 
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

270 
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

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

272 
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

273 
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

274 
} 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

275 
end 
45224
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

276 

b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

277 
subsection {* @{text ring_eq_cancel_factor} *} 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

278 

45435
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

279 
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

280 
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

281 
{ 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

282 
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

283 
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

284 
next 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

285 
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

286 
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

287 
next 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

288 
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

289 
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

290 
next 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

291 
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

292 
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

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 "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

295 
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

296 
next 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

297 
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

298 
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

299 
} 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

300 
end 
45224
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

301 

b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

302 
subsection {* @{text int_div_cancel_factor} *} 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

303 

45435
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

304 
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

305 
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

306 
{ 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

307 
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

308 
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

309 
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

310 
next 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

311 
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

312 
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

313 
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

314 
next 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

315 
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

316 
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

317 
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

318 
next 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

319 
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

320 
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

321 
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

322 
} 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

323 
end 
45224
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

324 

b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

325 
subsection {* @{text divide_cancel_factor} *} 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

326 

45435
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

327 
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

328 
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

329 
{ 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

330 
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

331 
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

332 
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

333 
next 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

334 
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

335 
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

336 
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

337 
next 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

338 
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

339 
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

340 
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

341 
next 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

342 
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

343 
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

344 
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

345 
} 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

346 
end 
45224
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

347 

45462
aba629d6cee5
use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents:
45437
diff
changeset

348 
lemma 
aba629d6cee5
use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents:
45437
diff
changeset

349 
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

350 
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

351 
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

352 

b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

353 
subsection {* @{text linordered_ring_less_cancel_factor} *} 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

354 

45435
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

355 
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

356 
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

357 
{ 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

358 
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

359 
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

360 
next 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

361 
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

362 
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

363 
next 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

364 
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

365 
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

366 
next 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

367 
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

368 
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

369 
} 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

370 
end 
45224
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

371 

b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

372 
subsection {* @{text linordered_ring_le_cancel_factor} *} 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

373 

45435
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

374 
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

375 
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

376 
{ 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

377 
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

378 
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

379 
next 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

380 
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

381 
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

382 
} 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

383 
end 
45224
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

384 

b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

385 
subsection {* @{text field_combine_numerals} *} 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

386 

45435
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

387 
notepad begin 
45437
958d19d3405b
tune postprocessing of simprocgenerated rules so they won't produce Numeral0 or Numeral1
huffman
parents:
45436
diff
changeset

388 
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

389 
{ 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

390 
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

391 
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

392 
next 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

393 
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

394 
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

395 
next 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

396 
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

397 
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

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

399 
assume "y + z = uu" 
958d19d3405b
tune postprocessing of simprocgenerated rules so they won't produce Numeral0 or Numeral1
huffman
parents:
45436
diff
changeset

400 
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

401 
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

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

403 
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

404 
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

405 
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

406 
} 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

407 
end 
45224
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

408 

45462
aba629d6cee5
use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents:
45437
diff
changeset

409 
lemma 
aba629d6cee5
use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents:
45437
diff
changeset

410 
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

411 
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

412 
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

413 
oops  "FIXME: test fails" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

414 

45462
aba629d6cee5
use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents:
45437
diff
changeset

415 
subsection {* @{text nat_combine_numerals} *} 
aba629d6cee5
use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents:
45437
diff
changeset

416 

aba629d6cee5
use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents:
45437
diff
changeset

417 
notepad begin 
aba629d6cee5
use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents:
45437
diff
changeset

418 
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

419 
{ 
aba629d6cee5
use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents:
45437
diff
changeset

420 
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

421 
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

422 
next 
45530
0c4853bb77bf
rewrite integer numeral div/mod simprocs to not return conditional rewrites; add regression tests
huffman
parents:
45464
diff
changeset

423 
(* FIXME "Suc (i + 3) \<equiv> i + 4" *) 
45462
aba629d6cee5
use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents:
45437
diff
changeset

424 
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

425 
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

426 
next 
45530
0c4853bb77bf
rewrite integer numeral div/mod simprocs to not return conditional rewrites; add regression tests
huffman
parents:
45464
diff
changeset

427 
(* FIXME "Suc (i + j + 3 + k) \<equiv> i + j + 4 + k" *) 
45462
aba629d6cee5
use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents:
45437
diff
changeset

428 
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

429 
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

430 
next 
aba629d6cee5
use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents:
45437
diff
changeset

431 
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

432 
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

433 
next 
aba629d6cee5
use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents:
45437
diff
changeset

434 
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

435 
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

436 
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

437 
next 
aba629d6cee5
use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents:
45437
diff
changeset

438 
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

439 
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

440 
} 
aba629d6cee5
use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents:
45437
diff
changeset

441 
end 
aba629d6cee5
use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents:
45437
diff
changeset

442 

aba629d6cee5
use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents:
45437
diff
changeset

443 
(*negative numerals: FAIL*) 
aba629d6cee5
use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents:
45437
diff
changeset

444 
lemma "Suc (i + j + 3 + k) = u" 
aba629d6cee5
use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents:
45437
diff
changeset

445 
apply (tactic {* test [@{simproc nat_combine_numerals}] *})? 
aba629d6cee5
use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents:
45437
diff
changeset

446 
oops 
aba629d6cee5
use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents:
45437
diff
changeset

447 

45436
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

448 
subsection {* @{text nateq_cancel_numerals} *} 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

449 

62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

450 
notepad begin 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

451 
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

452 
{ 
45462
aba629d6cee5
use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents:
45437
diff
changeset

453 
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

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 = Suc 0" have "2*u = Suc (u)" 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

457 
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

458 
next 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

459 
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

460 
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

461 
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

462 
next 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

463 
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

464 
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

465 
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

466 
next 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

467 
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

468 
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

469 
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

470 
next 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

471 
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

472 
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

473 
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

474 
next 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

475 
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

476 
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

477 
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

478 
next 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

479 
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

480 
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

481 
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

482 
next 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

483 
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

484 
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

485 
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

486 
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

487 
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

488 
next 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

489 
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

490 
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

491 
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

492 
} 
45224
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

493 
end 
45436
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

494 

62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

495 
subsection {* @{text natless_cancel_numerals} *} 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

496 

62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

497 
notepad begin 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

498 
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

499 
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

500 
{ 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

501 
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

502 
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

503 
next 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

504 
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

505 
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

506 
next 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

507 
assume "i + (j + k) < u + y" 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

508 
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

509 
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

510 
next 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

511 
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

512 
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

513 
next 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

514 
(* FIXME: negative numerals fail 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

515 
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

516 
apply (tactic {* test [@{simproc natless_cancel_numerals}] *})? 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

517 
sorry 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

518 
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

519 
apply (tactic {* test [@{simproc natless_cancel_numerals}] *})? 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

520 
sorry*) 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

521 
} 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

522 
end 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

523 

62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

524 
subsection {* @{text natle_cancel_numerals} *} 
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 
notepad begin 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

527 
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

528 
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

529 
{ 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

530 
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

531 
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

532 
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

533 
next 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

534 
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

535 
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

536 
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

537 
next 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

538 
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

539 
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

540 
next 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

541 
assume "5 + length l3 = 0" 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

542 
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

543 
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

544 
next 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

545 
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

546 
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

547 
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

548 
} 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

549 
end 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

550 

62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

551 
subsection {* @{text natdiff_cancel_numerals} *} 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

552 

62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

553 
notepad begin 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

554 
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

555 
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

556 
{ 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

557 
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

558 
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

559 
next 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

560 
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

561 
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

562 
next 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

563 
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

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 "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

567 
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

568 
next 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

569 
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

570 
have "(i + j + 2 + k)  1 = y" 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

571 
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

572 
next 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

573 
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

574 
have "(i + j + 1 + k)  2 = y" 
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 "2 * x + y  2 * (u * v) = w" 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

578 
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

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 "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

582 
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

583 
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

584 
next 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

585 
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

586 
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

587 
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

588 
next 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

589 
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

590 
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

591 
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

592 
next 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

593 
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

594 
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

595 
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

596 
next 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

597 
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

598 
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

599 
next 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

600 
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

601 
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

602 
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

603 
next 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

604 
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

605 
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

606 
next 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

607 
(* FIXME: negative numerals fail 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

608 
have "(i + j + 12 + k)  15 = y" 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

609 
apply (tactic {* test [@{simproc natdiff_cancel_numerals}] *})? 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

610 
sorry 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

611 
have "(i + j + 12 + k)  15 = y" 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

612 
apply (tactic {* test [@{simproc natdiff_cancel_numerals}] *})? 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

613 
sorry 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

614 
have "(i + j + 12 + k)  15 = y" 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

615 
apply (tactic {* test [@{simproc natdiff_cancel_numerals}] *})? 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

616 
sorry*) 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

617 
} 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

618 
end 
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

619 

45462
aba629d6cee5
use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents:
45437
diff
changeset

620 
subsection {* Factorcancellation simprocs for type @{typ nat} *} 
aba629d6cee5
use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents:
45437
diff
changeset

621 

aba629d6cee5
use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents:
45437
diff
changeset

622 
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

623 
@{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

624 
@{text nat_dvd_cancel_factor}. *} 
aba629d6cee5
use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents:
45437
diff
changeset

625 

aba629d6cee5
use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents:
45437
diff
changeset

626 
notepad begin 
aba629d6cee5
use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents:
45437
diff
changeset

627 
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

628 
{ 
aba629d6cee5
use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents:
45437
diff
changeset

629 
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

630 
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

631 
next 
aba629d6cee5
use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents:
45437
diff
changeset

632 
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

633 
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

634 
next 
aba629d6cee5
use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents:
45437
diff
changeset

635 
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

636 
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

637 
next 
aba629d6cee5
use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents:
45437
diff
changeset

638 
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

639 
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

640 
next 
aba629d6cee5
use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents:
45437
diff
changeset

641 
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

642 
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

643 
next 
aba629d6cee5
use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents:
45437
diff
changeset

644 
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

645 
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

646 
next 
aba629d6cee5
use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents:
45437
diff
changeset

647 
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

648 
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

649 
next 
aba629d6cee5
use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents:
45437
diff
changeset

650 
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

651 
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

652 
next 
aba629d6cee5
use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents:
45437
diff
changeset

653 
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

654 
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

655 
next 
aba629d6cee5
use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents:
45437
diff
changeset

656 
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

657 
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

658 
next 
aba629d6cee5
use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents:
45437
diff
changeset

659 
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

660 
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

661 
next 
aba629d6cee5
use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents:
45437
diff
changeset

662 
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

663 
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

664 
next 
aba629d6cee5
use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents:
45437
diff
changeset

665 
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

666 
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

667 
next 
aba629d6cee5
use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents:
45437
diff
changeset

668 
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

669 
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

670 
next 
aba629d6cee5
use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents:
45437
diff
changeset

671 
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

672 
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

673 
next 
aba629d6cee5
use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents:
45437
diff
changeset

674 
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

675 
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

676 
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

677 
next 
aba629d6cee5
use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents:
45437
diff
changeset

678 
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

679 
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

680 
next 
aba629d6cee5
use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents:
45437
diff
changeset

681 
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

682 
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

683 
next 
aba629d6cee5
use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents:
45437
diff
changeset

684 
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

685 
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

686 
next 
aba629d6cee5
use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents:
45437
diff
changeset

687 
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

688 
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

689 
next 
aba629d6cee5
use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents:
45437
diff
changeset

690 
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

691 
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

692 
} 
45436
62bc9474d04b
use simproc_setup for some nat_numeral simprocs; add simproc tests
huffman
parents:
45435
diff
changeset

693 
end 
45462
aba629d6cee5
use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents:
45437
diff
changeset

694 

45463
9a588a835c1e
use simproc_setup for the remaining nat_numeral simprocs
huffman
parents:
45462
diff
changeset

695 
subsection {* Numeralcancellation simprocs for type @{typ nat} *} 
9a588a835c1e
use simproc_setup for the remaining nat_numeral simprocs
huffman
parents:
45462
diff
changeset

696 

9a588a835c1e
use simproc_setup for the remaining nat_numeral simprocs
huffman
parents:
45462
diff
changeset

697 
notepad begin 
9a588a835c1e
use simproc_setup for the remaining nat_numeral simprocs
huffman
parents:
45462
diff
changeset

698 
fix x y z :: nat 
9a588a835c1e
use simproc_setup for the remaining nat_numeral simprocs
huffman
parents:
45462
diff
changeset

699 
{ 
9a588a835c1e
use simproc_setup for the remaining nat_numeral simprocs
huffman
parents:
45462
diff
changeset

700 
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

701 
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

702 
next 
9a588a835c1e
use simproc_setup for the remaining nat_numeral simprocs
huffman
parents:
45462
diff
changeset

703 
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

704 
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

705 
next 
9a588a835c1e
use simproc_setup for the remaining nat_numeral simprocs
huffman
parents:
45462
diff
changeset

706 
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

707 
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

708 
next 
9a588a835c1e
use simproc_setup for the remaining nat_numeral simprocs
huffman
parents:
45462
diff
changeset

709 
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

710 
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

711 
next 
9a588a835c1e
use simproc_setup for the remaining nat_numeral simprocs
huffman
parents:
45462
diff
changeset

712 
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

713 
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

714 
} 
45462
aba629d6cee5
use simproc_setup for more nat_numeral simprocs; add simproc tests
huffman
parents:
45437
diff
changeset

715 
end 
45463
9a588a835c1e
use simproc_setup for the remaining nat_numeral simprocs
huffman
parents:
45462
diff
changeset

716 

45530
0c4853bb77bf
rewrite integer numeral div/mod simprocs to not return conditional rewrites; add regression tests
huffman
parents:
45464
diff
changeset

717 
subsection {* Integer numeral div/mod simprocs *} 
0c4853bb77bf
rewrite integer numeral div/mod simprocs to not return conditional rewrites; add regression tests
huffman
parents:
45464
diff
changeset

718 

0c4853bb77bf
rewrite integer numeral div/mod simprocs to not return conditional rewrites; add regression tests
huffman
parents:
45464
diff
changeset

719 
notepad begin 
0c4853bb77bf
rewrite integer numeral div/mod simprocs to not return conditional rewrites; add regression tests
huffman
parents:
45464
diff
changeset

720 
have "(10::int) div 3 = 3" 
0c4853bb77bf
rewrite integer numeral div/mod simprocs to not return conditional rewrites; add regression tests
huffman
parents:
45464
diff
changeset

721 
by (tactic {* test [@{simproc binary_int_div}] *}) 
0c4853bb77bf
rewrite integer numeral div/mod simprocs to not return conditional rewrites; add regression tests
huffman
parents:
45464
diff
changeset

722 
have "(10::int) mod 3 = 1" 
0c4853bb77bf
rewrite integer numeral div/mod simprocs to not return conditional rewrites; add regression tests
huffman
parents:
45464
diff
changeset

723 
by (tactic {* test [@{simproc binary_int_mod}] *}) 
0c4853bb77bf
rewrite integer numeral div/mod simprocs to not return conditional rewrites; add regression tests
huffman
parents:
45464
diff
changeset

724 
have "(10::int) div 3 = 4" 
0c4853bb77bf
rewrite integer numeral div/mod simprocs to not return conditional rewrites; add regression tests
huffman
parents:
45464
diff
changeset

725 
by (tactic {* test [@{simproc binary_int_div}] *}) 
0c4853bb77bf
rewrite integer numeral div/mod simprocs to not return conditional rewrites; add regression tests
huffman
parents:
45464
diff
changeset

726 
have "(10::int) mod 3 = 2" 
0c4853bb77bf
rewrite integer numeral div/mod simprocs to not return conditional rewrites; add regression tests
huffman
parents:
45464
diff
changeset

727 
by (tactic {* test [@{simproc binary_int_mod}] *}) 
0c4853bb77bf
rewrite integer numeral div/mod simprocs to not return conditional rewrites; add regression tests
huffman
parents:
45464
diff
changeset

728 
have "(10::int) div 3 = 4" 
0c4853bb77bf
rewrite integer numeral div/mod simprocs to not return conditional rewrites; add regression tests
huffman
parents:
45464
diff
changeset

729 
by (tactic {* test [@{simproc binary_int_div}] *}) 
0c4853bb77bf
rewrite integer numeral div/mod simprocs to not return conditional rewrites; add regression tests
huffman
parents:
45464
diff
changeset

730 
have "(10::int) mod 3 = 2" 
0c4853bb77bf
rewrite integer numeral div/mod simprocs to not return conditional rewrites; add regression tests
huffman
parents:
45464
diff
changeset

731 
by (tactic {* test [@{simproc binary_int_mod}] *}) 
0c4853bb77bf
rewrite integer numeral div/mod simprocs to not return conditional rewrites; add regression tests
huffman
parents:
45464
diff
changeset

732 
have "(10::int) div 3 = 3" 
0c4853bb77bf
rewrite integer numeral div/mod simprocs to not return conditional rewrites; add regression tests
huffman
parents:
45464
diff
changeset

733 
by (tactic {* test [@{simproc binary_int_div}] *}) 
0c4853bb77bf
rewrite integer numeral div/mod simprocs to not return conditional rewrites; add regression tests
huffman
parents:
45464
diff
changeset

734 
have "(10::int) mod 3 = 1" 
0c4853bb77bf
rewrite integer numeral div/mod simprocs to not return conditional rewrites; add regression tests
huffman
parents:
45464
diff
changeset

735 
by (tactic {* test [@{simproc binary_int_mod}] *}) 
0c4853bb77bf
rewrite integer numeral div/mod simprocs to not return conditional rewrites; add regression tests
huffman
parents:
45464
diff
changeset

736 
have "(8452::int) mod 3 = 1" 
0c4853bb77bf
rewrite integer numeral div/mod simprocs to not return conditional rewrites; add regression tests
huffman
parents:
45464
diff
changeset

737 
by (tactic {* test [@{simproc binary_int_mod}] *}) 
0c4853bb77bf
rewrite integer numeral div/mod simprocs to not return conditional rewrites; add regression tests
huffman
parents:
45464
diff
changeset

738 
have "(59485::int) div 434 = 137" 
0c4853bb77bf
rewrite integer numeral div/mod simprocs to not return conditional rewrites; add regression tests
huffman
parents:
45464
diff
changeset

739 
by (tactic {* test [@{simproc binary_int_div}] *}) 
0c4853bb77bf
rewrite integer numeral div/mod simprocs to not return conditional rewrites; add regression tests
huffman
parents:
45464
diff
changeset

740 
have "(1000006::int) mod 10 = 6" 
0c4853bb77bf
rewrite integer numeral div/mod simprocs to not return conditional rewrites; add regression tests
huffman
parents:
45464
diff
changeset

741 
by (tactic {* test [@{simproc binary_int_mod}] *}) 
0c4853bb77bf
rewrite integer numeral div/mod simprocs to not return conditional rewrites; add regression tests
huffman
parents:
45464
diff
changeset

742 
have "10000000 div 2 = (5000000::int)" 
0c4853bb77bf
rewrite integer numeral div/mod simprocs to not return conditional rewrites; add regression tests
huffman
parents:
45464
diff
changeset

743 
by (tactic {* test [@{simproc binary_int_div}] *}) 
0c4853bb77bf
rewrite integer numeral div/mod simprocs to not return conditional rewrites; add regression tests
huffman
parents:
45464
diff
changeset

744 
have "10000001 mod 2 = (1::int)" 
0c4853bb77bf
rewrite integer numeral div/mod simprocs to not return conditional rewrites; add regression tests
huffman
parents:
45464
diff
changeset

745 
by (tactic {* test [@{simproc binary_int_mod}] *}) 
0c4853bb77bf
rewrite integer numeral div/mod simprocs to not return conditional rewrites; add regression tests
huffman
parents:
45464
diff
changeset

746 
have "10000055 div 32 = (312501::int)" 
0c4853bb77bf
rewrite integer numeral div/mod simprocs to not return conditional rewrites; add regression tests
huffman
parents:
45464
diff
changeset

747 
by (tactic {* test [@{simproc binary_int_div}] *}) 
0c4853bb77bf
rewrite integer numeral div/mod simprocs to not return conditional rewrites; add regression tests
huffman
parents:
45464
diff
changeset

748 
have "10000055 mod 32 = (23::int)" 
0c4853bb77bf
rewrite integer numeral div/mod simprocs to not return conditional rewrites; add regression tests
huffman
parents:
45464
diff
changeset

749 
by (tactic {* test [@{simproc binary_int_mod}] *}) 
0c4853bb77bf
rewrite integer numeral div/mod simprocs to not return conditional rewrites; add regression tests
huffman
parents:
45464
diff
changeset

750 
have "100094 div 144 = (695::int)" 
0c4853bb77bf
rewrite integer numeral div/mod simprocs to not return conditional rewrites; add regression tests
huffman
parents:
45464
diff
changeset

751 
by (tactic {* test [@{simproc binary_int_div}] *}) 
0c4853bb77bf
rewrite integer numeral div/mod simprocs to not return conditional rewrites; add regression tests
huffman
parents:
45464
diff
changeset

752 
have "100094 mod 144 = (14::int)" 
0c4853bb77bf
rewrite integer numeral div/mod simprocs to not return conditional rewrites; add regression tests
huffman
parents:
45464
diff
changeset

753 
by (tactic {* test [@{simproc binary_int_mod}] *}) 
45463
9a588a835c1e
use simproc_setup for the remaining nat_numeral simprocs
huffman
parents:
45462
diff
changeset

754 
end 
45530
0c4853bb77bf
rewrite integer numeral div/mod simprocs to not return conditional rewrites; add regression tests
huffman
parents:
45464
diff
changeset

755 

0c4853bb77bf
rewrite integer numeral div/mod simprocs to not return conditional rewrites; add regression tests
huffman
parents:
45464
diff
changeset

756 
end 