author  huffman 
Fri, 21 Oct 2011 08:42:11 +0200  
changeset 45224  b1d5b3820d82 
child 45270  d5b5c9259afd 
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 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

8 
imports Rat 
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 
val semiring_assoc_fold = Numeral_Simprocs.assoc_fold_simproc 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

22 
val int_combine_numerals = Numeral_Simprocs.combine_numerals 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

23 
val field_combine_numerals = Numeral_Simprocs.field_combine_numerals 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

24 
val [inteq_cancel_numerals, intless_cancel_numerals, intle_cancel_numerals] 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

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

26 
val [ring_eq_cancel_factor, linordered_ring_le_cancel_factor, 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

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

28 
int_mod_cancel_factor, dvd_cancel_factor, divide_cancel_factor] 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

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

30 
val [ring_eq_cancel_numeral_factor, ring_less_cancel_numeral_factor, 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

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

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

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

34 
val field_combine_numerals = Numeral_Simprocs.field_combine_numerals 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

35 
val [field_eq_cancel_numeral_factor, field_cancel_numeral_factor] 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

36 
= Numeral_Simprocs.field_cancel_numeral_factors 
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 
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

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

40 

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

41 

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

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

43 

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

44 
lemma assumes "10 + (2 * l + oo) = uu" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

45 
shows "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::int)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

46 
by (tactic {* test [int_combine_numerals] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

47 

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

48 
lemma assumes "3 + (i + (j + k)) = y" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

49 
shows "(i + j + 12 + (k::int))  15 = y" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

50 
by (tactic {* test [int_combine_numerals] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

51 

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

52 
lemma assumes "7 + (i + (j + k)) = y" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

53 
shows "(i + j + 12 + (k::int))  5 = y" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

54 
by (tactic {* test [int_combine_numerals] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

55 

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

56 
lemma assumes "4 * (u * v) + (2 * x + y) = w" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

57 
shows "(2*x  (u*v) + y)  v*3*u = (w::int)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

58 
by (tactic {* test [int_combine_numerals] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

59 

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

60 
lemma assumes "Numeral0 * (u*v) + (2 * x * u * v + y) = w" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

61 
shows "(2*x*u*v + (u*v)*4 + y)  v*u*4 = (w::int)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

62 
by (tactic {* test [int_combine_numerals] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

63 

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

64 
lemma assumes "3 * (u * v) + (2 * x * u * v + y) = w" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

65 
shows "(2*x*u*v + (u*v)*4 + y)  v*u = (w::int)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

66 
by (tactic {* test [int_combine_numerals] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

67 

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

68 
lemma assumes "3 * (u * v) + ( (x * u * v) +  y) = w" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

69 
shows "u*v  (x*u*v + (u*v)*4 + y) = (w::int)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

70 
by (tactic {* test [int_combine_numerals] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

71 

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

72 
lemma assumes "Numeral0 * b + (a +  c) = d" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

73 
shows "a + (b+c) + b = (d::int)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

74 
apply (simp only: minus_add_distrib) 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

75 
by (tactic {* test [int_combine_numerals] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

76 

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

77 
lemma assumes "2 * b + (a +  c) = d" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

78 
shows "a + (b+c)  b = (d::int)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

79 
apply (simp only: minus_add_distrib) 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

80 
by (tactic {* test [int_combine_numerals] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

81 

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

82 
lemma assumes "7 + (i + (j + (k + ( u +  y)))) = zz" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

83 
shows "(i + j + 2 + (k::int))  (u + 5 + y) = zz" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

84 
by (tactic {* test [int_combine_numerals] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

85 

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

86 
lemma assumes "27 + (i + (j + k)) = y" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

87 
shows "(i + j + 12 + (k::int))  15 = y" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

88 
by (tactic {* test [int_combine_numerals] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

89 

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

90 
lemma assumes "27 + (i + (j + k)) = y" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

91 
shows "(i + j + 12 + (k::int))  15 = y" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

92 
by (tactic {* test [int_combine_numerals] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

93 

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

94 
lemma assumes "3 + (i + (j + k)) = y" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

95 
shows "(i + j + 12 + (k::int))  15 = y" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

96 
by (tactic {* test [int_combine_numerals] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

97 

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

98 

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

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

100 

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

101 
lemma assumes "u = Numeral0" shows "2*u = (u::int)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

102 
by (tactic {* test [inteq_cancel_numerals] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

103 
(* conclusion matches Rings.ring_1_no_zero_divisors_class.mult_cancel_right2 *) 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

104 

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

105 
lemma assumes "i + (j + k) = 3 + (u + y)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

106 
shows "(i + j + 12 + (k::int)) = u + 15 + y" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

107 
by (tactic {* test [inteq_cancel_numerals] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

108 

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

109 
lemma assumes "7 + (j + (i + k)) = y" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

110 
shows "(i + j*2 + 12 + (k::int)) = j + 5 + y" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

111 
by (tactic {* test [inteq_cancel_numerals] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

112 

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

113 
lemma assumes "u + (6*z + (4*y + 6*w)) = 6*z' + (4*y' + (6*w' + vv))" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

114 
shows "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = 2*y' + 3*z' + 6*w' + 2*y' + 3*z' + u + (vv::int)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

115 
by (tactic {* test [int_combine_numerals, inteq_cancel_numerals] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

116 

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

117 

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

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

119 

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

120 
lemma assumes "y < 2 * b" shows "y  b < (b::int)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

121 
by (tactic {* test [intless_cancel_numerals] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

122 

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

123 
lemma assumes "c + y < 4 * b" shows "y  (3*b + c) < (b::int)  2*c" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

124 
by (tactic {* test [intless_cancel_numerals] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

125 

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

126 
lemma assumes "i + (j + k) < 8 + (u + y)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

127 
shows "(i + j + 3 + (k::int)) < u + 5 + y" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

128 
by (tactic {* test [intless_cancel_numerals] *}) fact 
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 
lemma assumes "9 + (i + (j + k)) < u + y" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

131 
shows "(i + j + 3 + (k::int)) < u + 6 + y" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

132 
by (tactic {* test [intless_cancel_numerals] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

133 

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

134 

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

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

136 

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

137 
lemma assumes "3*x = 4*y" shows "9*x = 12 * (y::int)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

138 
by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

139 

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

140 
lemma assumes "3*x = 4*y" shows "99*x = 132 * (y::int)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

141 
by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

142 

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

143 

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

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

145 

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

146 
lemma assumes "(3*x) div (4*y) = z" shows "(9*x) div (12*y) = (z::int)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

147 
by (tactic {* test [int_div_cancel_numeral_factors] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

148 

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

149 
lemma assumes "(3*x) div (4*y) = z" shows "(99*x) div (132*y) = (z::int)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

150 
by (tactic {* test [int_div_cancel_numeral_factors] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

151 

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

152 
lemma assumes "(111*x) div (44*y) = z" shows "(999*x) div (396*y) = (z::int)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

153 
by (tactic {* test [int_div_cancel_numeral_factors] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

154 

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

155 
lemma assumes "(11*x) div (9*y) = z" shows "(99*x) div (81*y) = (z::int)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

156 
by (tactic {* test [int_div_cancel_numeral_factors] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

157 

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

158 
lemma assumes "(2*x) div (Numeral1*y) = z" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

159 
shows "(2 * x) div (1 * (y::int)) = z" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

160 
by (tactic {* test [int_div_cancel_numeral_factors] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

161 

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

162 

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

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

164 

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

165 
lemma assumes "3*x < 4*y" shows "9*x < 12 * (y::int)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

166 
by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

167 

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

168 
lemma assumes "3*x < 4*y" shows "99*x < 132 * (y::int)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

169 
by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

170 

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

171 
lemma assumes "111*x < 44*y" shows "999*x < 396 * (y::int)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

172 
by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

173 

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

174 
lemma assumes "9*y < 11*x" shows "99*x < 81 * (y::int)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

175 
by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

176 

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

177 
lemma assumes "Numeral1*y < 2*x" shows "2 * x < (y::int)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

178 
by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

179 

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

180 
lemma assumes "23*y < Numeral1*x" shows "x < 23 * (y::int)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

181 
by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

182 

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

183 
lemma assumes "3*x < 4*y" shows "9*x < 12 * (y::rat)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

184 
by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

185 

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

186 
lemma assumes "3*x < 4*y" shows "99*x < 132 * (y::rat)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

187 
by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

188 

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

189 
lemma assumes "111*x < 44*y" shows "999*x < 396 * (y::rat)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

190 
by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

191 

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

192 
lemma assumes "9*y < 11*x" shows "99*x < 81 * (y::rat)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

193 
by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

194 

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

195 
lemma assumes "Numeral1*y < 2*x" shows "2 * x < (y::rat)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

196 
by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

197 

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

198 
lemma assumes "23*y < Numeral1*x" shows "x < 23 * (y::rat)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

199 
by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

200 

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

201 

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

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

203 

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

204 
lemma assumes "3*x \<le> 4*y" shows "9*x \<le> 12 * (y::int)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

205 
by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

206 

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

207 
lemma assumes "3*x \<le> 4*y" shows "99*x \<le> 132 * (y::int)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

208 
by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

209 

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

210 
lemma assumes "111*x \<le> 44*y" shows "999*x \<le> 396 * (y::int)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

211 
by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

212 

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

213 
lemma assumes "9*y \<le> 11*x" shows "99*x \<le> 81 * (y::int)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

214 
by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

215 

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

216 
lemma assumes "Numeral1*y \<le> 2*x" shows "2 * x \<le> 1 * (y::int)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

217 
by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

218 

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

219 
lemma assumes "23*y \<le> Numeral1*x" shows "x \<le> 23 * (y::int)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

220 
by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

221 

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

222 
lemma assumes "Numeral1*y \<le> Numeral0" shows "0 \<le> (y::rat) * 2" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

223 
by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

224 

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

225 
lemma assumes "3*x \<le> 4*y" shows "9*x \<le> 12 * (y::rat)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

226 
by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

227 

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

228 
lemma assumes "3*x \<le> 4*y" shows "99*x \<le> 132 * (y::rat)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

229 
by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

230 

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

231 
lemma assumes "111*x \<le> 44*y" shows "999*x \<le> 396 * (y::rat)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

232 
by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

233 

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

234 
lemma assumes "1*x \<le> Numeral1*y" shows " ((2::rat) * x) \<le> 2*y" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

235 
by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

236 

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

237 
lemma assumes "9*y \<le> 11*x" shows "99*x \<le> 81 * (y::rat)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

238 
by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

239 

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

240 
lemma assumes "Numeral1*y \<le> 2*x" shows "2 * x \<le> 1 * (y::rat)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

241 
by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

242 

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

243 
lemma assumes "23*y \<le> Numeral1*x" shows "x \<le> 23 * (y::rat)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

244 
by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

245 

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

246 

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

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

248 

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

249 
lemma assumes "111*x = 44*y" shows "999*x = 396 * (y::int)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

250 
by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

251 

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

252 
lemma assumes "11*x = 9*y" shows "99*x = 81 * (y::int)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

253 
by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

254 

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

255 
lemma assumes "2*x = Numeral1*y" shows "2 * x = 1 * (y::int)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

256 
by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

257 

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

258 
lemma assumes "2*x = Numeral1*y" shows "2 * x = (y::int)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

259 
by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

260 

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

261 
lemma assumes "3*x = 4*y" shows "9*x = 12 * (y::rat)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

262 
by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

263 

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

264 
lemma assumes "3*x = 4*y" shows "99*x = 132 * (y::rat)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

265 
by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

266 

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

267 
lemma assumes "111*x = 44*y" shows "999*x = 396 * (y::rat)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

268 
by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

269 

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

270 
lemma assumes "11*x = 9*y" shows "99*x = 81 * (y::rat)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

271 
by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

272 

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

273 
lemma assumes "2*x = Numeral1*y" shows "2 * x = 1 * (y::rat)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

274 
by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

275 

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

276 
lemma assumes "2*x = Numeral1*y" shows "2 * x = (y::rat)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

277 
by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

278 

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

279 

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

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

281 

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

282 
lemma assumes "(3*x) / (4*y) = z" shows "(9*x) / (12 * (y::rat)) = z" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

283 
by (tactic {* test [field_cancel_numeral_factor] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

284 

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

285 
lemma assumes "(3*x) / (4*y) = z" shows "(99*x) / (132 * (y::rat)) = z" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

286 
by (tactic {* test [field_cancel_numeral_factor] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

287 

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

288 
lemma assumes "(111*x) / (44*y) = z" shows "(999*x) / (396 * (y::rat)) = z" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

289 
by (tactic {* test [field_cancel_numeral_factor] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

290 

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

291 
lemma assumes "(11*x) / (9*y) = z" shows "(99*x) / (81 * (y::rat)) = z" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

292 
by (tactic {* test [field_cancel_numeral_factor] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

293 

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

294 
lemma assumes "(2*x) / (Numeral1*y) = z" shows "(2 * x) / (1 * (y::rat)) = z" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

295 
by (tactic {* test [field_cancel_numeral_factor] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

296 

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

297 

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

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

299 

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

300 
lemma assumes "k = 0 \<or> x = y" shows "x*k = k*(y::int)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

301 
by (tactic {* test [ring_eq_cancel_factor] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

302 

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

303 
lemma assumes "k = 0 \<or> 1 = y" shows "k = k*(y::int)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

304 
by (tactic {* test [ring_eq_cancel_factor] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

305 

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

306 
lemma assumes "b = 0 \<or> a*c = 1" shows "a*(b*c) = (b::int)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

307 
by (tactic {* test [ring_eq_cancel_factor] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

308 

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

309 
lemma assumes "a = 0 \<or> b = 0 \<or> c = d*x" shows "a*(b*c) = d*(b::int)*(x*a)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

310 
by (tactic {* test [ring_eq_cancel_factor] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

311 

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

312 
lemma assumes "k = 0 \<or> x = y" shows "x*k = k*(y::rat)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

313 
by (tactic {* test [ring_eq_cancel_factor] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

314 

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

315 
lemma assumes "k = 0 \<or> 1 = y" shows "k = k*(y::rat)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

316 
by (tactic {* test [ring_eq_cancel_factor] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

317 

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

318 
lemma assumes "b = 0 \<or> a*c = 1" shows "a*(b*c) = (b::rat)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

319 
by (tactic {* test [ring_eq_cancel_factor] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

320 

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

321 
lemma assumes "a = 0 \<or> b = 0 \<or> c = d*x" shows "a*(b*c) = d*(b::rat)*(x*a)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

322 
by (tactic {* test [ring_eq_cancel_factor] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

323 

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 int_div_cancel_factor} *} 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

326 

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

327 
lemma assumes "(if k = 0 then 0 else x div y) = uu" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

328 
shows "(x*k) div (k*(y::int)) = (uu::int)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

329 
by (tactic {* test [int_div_cancel_factor] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

330 

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

331 
lemma assumes "(if k = 0 then 0 else 1 div y) = uu" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

332 
shows "(k) div (k*(y::int)) = (uu::int)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

333 
by (tactic {* test [int_div_cancel_factor] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

334 

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

335 
lemma assumes "(if b = 0 then 0 else a * c) = uu" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

336 
shows "(a*(b*c)) div ((b::int)) = (uu::int)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

337 
by (tactic {* test [int_div_cancel_factor] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

338 

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

339 
lemma assumes "(if a = 0 then 0 else if b = 0 then 0 else c div (d * x)) = uu" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

340 
shows "(a*(b*c)) div (d*(b::int)*(x*a)) = (uu::int)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

341 
by (tactic {* test [int_div_cancel_factor] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

342 

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

343 

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

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

345 

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

346 
lemma assumes "(if k = 0 then 0 else x / y) = uu" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

347 
shows "(x*k) / (k*(y::rat)) = (uu::rat)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

348 
by (tactic {* test [divide_cancel_factor] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

349 

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

350 
lemma assumes "(if k = 0 then 0 else 1 / y) = uu" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

351 
shows "(k) / (k*(y::rat)) = (uu::rat)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

352 
by (tactic {* test [divide_cancel_factor] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

353 

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

354 
lemma assumes "(if b = 0 then 0 else a * c / 1) = uu" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

355 
shows "(a*(b*c)) / ((b::rat)) = (uu::rat)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

356 
by (tactic {* test [divide_cancel_factor] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

357 

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

358 
lemma assumes "(if a = 0 then 0 else if b = 0 then 0 else c / (d * x)) = uu" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

359 
shows "(a*(b*c)) / (d*(b::rat)*(x*a)) = (uu::rat)" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

360 
by (tactic {* test [divide_cancel_factor] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

361 

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

362 
lemma shows "a*(b*c)/(y*z) = d*(b::rat)*(x*a)/z" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

363 
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

364 

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

365 

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

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

367 

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

368 
lemma assumes "0 < z \<Longrightarrow> x < y" shows "(0::rat) < z \<Longrightarrow> x*z < y*z" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

369 
by (tactic {* test [linordered_ring_less_cancel_factor] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

370 

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

371 
lemma assumes "0 < z \<Longrightarrow> x < y" shows "(0::rat) < z \<Longrightarrow> x*z < z*y" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

372 
by (tactic {* test [linordered_ring_less_cancel_factor] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

373 

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

374 
lemma assumes "0 < z \<Longrightarrow> x < y" shows "(0::rat) < z \<Longrightarrow> z*x < y*z" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

375 
by (tactic {* test [linordered_ring_less_cancel_factor] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

376 

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

377 
lemma "(0::rat) < z \<Longrightarrow> z*x < z*y" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

378 
apply (tactic {* test [linordered_ring_less_cancel_factor] *})? 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

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

380 

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

381 

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

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

383 

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

384 
lemma assumes "0 < z \<Longrightarrow> x \<le> y" shows "(0::rat) < z \<Longrightarrow> x*z \<le> y*z" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

385 
by (tactic {* test [linordered_ring_le_cancel_factor] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

386 

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

387 
lemma assumes "0 < z \<Longrightarrow> x \<le> y" shows "(0::rat) < z \<Longrightarrow> z*x \<le> z*y" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

388 
apply (tactic {* test [linordered_ring_le_cancel_factor] *})? 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

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

390 

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

391 

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

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

393 

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

394 
lemma assumes "5 / 6 * x = uu" shows "(x::rat) / 2 + x / 3 = uu" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

395 
by (tactic {* test [field_combine_numerals] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

396 

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

397 
lemma assumes "6 / 9 * x + y = uu" shows "(x::rat) / 3 + y + x / 3 = uu" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

398 
by (tactic {* test [field_combine_numerals] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

399 

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

400 
lemma assumes "9 / 9 * x = uu" shows "2 * (x::rat) / 3 + x / 3 = uu" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

401 
by (tactic {* test [field_combine_numerals] *}) fact 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

402 

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

403 
lemma "2/3 * (x::rat) + x / 3 = uu" 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

404 
apply (tactic {* test [field_combine_numerals] *})? 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

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

406 

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

407 

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

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

409 

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

410 
text {* TODO: tests for @{text field_eq_cancel_numeral_factor} simproc *} 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

411 

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

412 

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

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

414 

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

415 
text {* TODO: tests for @{text field_cancel_numeral_factor} simproc *} 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

416 

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

417 
end 