author  huffman 
Wed, 09 Nov 2011 10:58:08 +0100  
changeset 45435  d660c4b9daa6 
parent 45285  299abd2931d5 
child 45436  62bc9474d04b 
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 
fun test ps = CHANGED (asm_simp_tac (HOL_basic_ss addsimprocs ps) 1) 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

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

23 

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

24 

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

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

26 

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

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

28 
fix a b c d oo uu i j k l u v w x y z :: "'a::number_ring" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

30 
assume "10 + (2 * l + oo) = uu" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

31 
have "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = uu" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

32 
by (tactic {* test [@{simproc int_combine_numerals}] *}) fact 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

34 
assume "3 + (i + (j + k)) = y" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

35 
have "(i + j + 12 + k)  15 = y" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

36 
by (tactic {* test [@{simproc int_combine_numerals}] *}) fact 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

38 
assume "7 + (i + (j + k)) = y" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

39 
have "(i + j + 12 + k)  5 = y" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

40 
by (tactic {* test [@{simproc int_combine_numerals}] *}) fact 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

42 
assume "4 * (u * v) + (2 * x + y) = w" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

43 
have "(2*x  (u*v) + y)  v*3*u = w" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

44 
by (tactic {* test [@{simproc int_combine_numerals}] *}) fact 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

46 
assume "Numeral0 * (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

47 
have "(2*x*u*v + (u*v)*4 + y)  v*u*4 = w" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

48 
by (tactic {* test [@{simproc int_combine_numerals}] *}) fact 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

50 
assume "3 * (u * v) + (2 * x * u * v + y) = w" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

51 
have "(2*x*u*v + (u*v)*4 + y)  v*u = w" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

52 
by (tactic {* test [@{simproc int_combine_numerals}] *}) fact 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

54 
assume "3 * (u * v) + ( (x * u * v) +  y) = w" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

55 
have "u*v  (x*u*v + (u*v)*4 + y) = w" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

56 
by (tactic {* test [@{simproc int_combine_numerals}] *}) fact 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

58 
assume "Numeral0 * 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

59 
have "a + (b+c) + b = d" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

60 
apply (simp only: minus_add_distrib) 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

61 
by (tactic {* test [@{simproc int_combine_numerals}] *}) fact 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

63 
assume "2 * b + (a +  c) = d" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

64 
have "a + (b+c)  b = d" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

65 
apply (simp only: minus_add_distrib) 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

66 
by (tactic {* test [@{simproc int_combine_numerals}] *}) fact 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

68 
assume "7 + (i + (j + (k + ( u +  y)))) = z" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

69 
have "(i + j + 2 + k)  (u + 5 + y) = z" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

70 
by (tactic {* test [@{simproc int_combine_numerals}] *}) fact 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

72 
assume "27 + (i + (j + k)) = y" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

73 
have "(i + j + 12 + k)  15 = y" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

74 
by (tactic {* test [@{simproc int_combine_numerals}] *}) fact 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

76 
assume "27 + (i + (j + k)) = y" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

77 
have "(i + j + 12 + k)  15 = y" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

78 
by (tactic {* test [@{simproc int_combine_numerals}] *}) fact 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

80 
assume "3 + (i + (j + k)) = y" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

81 
have "(i + j + 12 + k)  15 = y" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

82 
by (tactic {* test [@{simproc int_combine_numerals}] *}) fact 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

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

85 

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

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

87 

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

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

89 
fix i j k u vv w y z w' y' z' :: "'a::number_ring" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

91 
assume "u = Numeral0" have "2*u = u" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

93 
(* conclusion matches Rings.ring_1_no_zero_divisors_class.mult_cancel_right2 *) 
45435
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

95 
assume "i + (j + k) = 3 + (u + y)" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

96 
have "(i + j + 12 + k) = u + 15 + y" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

97 
by (tactic {* test [@{simproc inteq_cancel_numerals}] *}) fact 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

99 
assume "7 + (j + (i + k)) = y" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

100 
have "(i + j*2 + 12 + k) = j + 5 + y" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

101 
by (tactic {* test [@{simproc inteq_cancel_numerals}] *}) fact 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

103 
assume "u + (6*z + (4*y + 6*w)) = 6*z' + (4*y' + (6*w' + vv))" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

104 
have "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = 2*y' + 3*z' + 6*w' + 2*y' + 3*z' + u + vv" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

105 
by (tactic {* test [@{simproc int_combine_numerals}, @{simproc inteq_cancel_numerals}] *}) fact 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

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

108 

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

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

110 

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

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

112 
fix b c i j k u y :: "'a::{linordered_idom,number_ring}" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

114 
assume "y < 2 * b" have "y  b < b" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

115 
by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

117 
assume "c + y < 4 * b" have "y  (3*b + c) < b  2*c" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

118 
by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

120 
assume "i + (j + k) < 8 + (u + y)" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

121 
have "(i + j + 3 + k) < u + 5 + y" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

122 
by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

124 
assume "9 + (i + (j + k)) < u + y" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

125 
have "(i + j + 3 + k) < u + 6 + y" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

126 
by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

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

129 

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

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

131 

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

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

133 
fix x y :: "'a::{idom,ring_char_0,number_ring}" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

135 
assume "3*x = 4*y" have "9*x = 12 * y" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

136 
by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

138 
assume "3*x = 4*y" have "99*x = 132 * y" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

139 
by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

141 
assume "111*x = 44*y" have "999*x = 396 * y" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

142 
by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

144 
assume "11*x = 9*y" have "99*x = 81 * y" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

145 
by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

147 
assume "2*x = Numeral1*y" have "2 * x = 1 * y" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

148 
by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

150 
assume "2*x = Numeral1*y" have "2 * x = y" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

151 
by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

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

154 

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

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

156 

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

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

158 
fix x y z :: "'a::{semiring_div,ring_char_0,number_ring}" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

160 
assume "(3*x) div (4*y) = z" have "(9*x) div (12*y) = z" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

161 
by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

163 
assume "(3*x) div (4*y) = z" have "(99*x) div (132*y) = z" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

164 
by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

166 
assume "(111*x) div (44*y) = z" have "(999*x) div (396*y) = z" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

167 
by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

169 
assume "(11*x) div (9*y) = z" have "(99*x) div (81*y) = z" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

170 
by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

172 
assume "(2*x) div (Numeral1*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

173 
have "(2 * x) div (1 * y) = z" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

174 
by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

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

177 

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

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

179 

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

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

181 
fix x y :: "'a::{linordered_idom,number_ring}" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

183 
assume "3*x < 4*y" have "9*x < 12 * y" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

184 
by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

186 
assume "3*x < 4*y" have "99*x < 132 * y" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

187 
by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

189 
assume "111*x < 44*y" have "999*x < 396 * y" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

190 
by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

192 
assume "9*y < 11*x" have "99*x < 81 * y" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

193 
by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

195 
assume "Numeral1*y < 2*x" have "2 * x < y" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

196 
by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

198 
assume "23*y < Numeral1*x" have "x < 23 * y" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

199 
by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

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

202 

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

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

204 

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

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

206 
fix x y :: "'a::{linordered_idom,number_ring}" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

208 
assume "3*x \<le> 4*y" have "9*x \<le> 12 * y" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

209 
by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

211 
assume "3*x \<le> 4*y" have "99*x \<le> 132 * y" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

212 
by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

214 
assume "111*x \<le> 44*y" have "999*x \<le> 396 * y" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

215 
by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

217 
assume "9*y \<le> 11*x" have "99*x \<le> 81 * y" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

218 
by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

220 
assume "Numeral1*y \<le> 2*x" have "2 * x \<le> 1 * y" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

221 
by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

223 
assume "23*y \<le> Numeral1*x" have "x \<le> 23 * y" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

224 
by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

226 
assume "Numeral1*y \<le> Numeral0" have "0 \<le> y * 2" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

227 
by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

228 
next 
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 "1*x \<le> Numeral1*y" have " (2 * x) \<le> 2*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 
} 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

233 

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

235 

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

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

237 
fix x y z :: "'a::{field_inverse_zero,ring_char_0,number_ring}" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

239 
assume "(3*x) / (4*y) = z" have "(9*x) / (12 * y) = z" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

240 
by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

242 
assume "(3*x) / (4*y) = z" have "(99*x) / (132 * y) = z" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

243 
by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

245 
assume "(111*x) / (44*y) = z" have "(999*x) / (396 * y) = z" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

246 
by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

248 
assume "(11*x) / (9*y) = z" have "(99*x) / (81 * y) = z" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

249 
by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

251 
assume "(2*x) / (Numeral1*y) = z" have "(2 * x) / (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

252 
by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

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

255 

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

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

257 

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

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

259 
fix a b c d k x y :: "'a::idom" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

261 
assume "k = 0 \<or> x = y" have "x*k = k*y" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

262 
by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

264 
assume "k = 0 \<or> 1 = y" have "k = k*y" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

265 
by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

267 
assume "b = 0 \<or> a*c = 1" have "a*(b*c) = b" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

268 
by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

270 
assume "a = 0 \<or> b = 0 \<or> c = d*x" have "a*(b*c) = d*b*(x*a)" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

271 
by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

273 
assume "k = 0 \<or> x = y" have "x*k = k*y" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

274 
by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

276 
assume "k = 0 \<or> 1 = y" have "k = k*y" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

277 
by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

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

280 

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

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

282 

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

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

284 
fix a b c d k uu x y :: "'a::semiring_div" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

286 
assume "(if k = 0 then 0 else x div y) = uu" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

287 
have "(x*k) div (k*y) = uu" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

288 
by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

290 
assume "(if k = 0 then 0 else 1 div y) = uu" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

291 
have "(k) div (k*y) = uu" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

292 
by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

294 
assume "(if b = 0 then 0 else a * c) = uu" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

295 
have "(a*(b*c)) div b = uu" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

296 
by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

298 
assume "(if a = 0 then 0 else if b = 0 then 0 else c div (d * x)) = uu" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

299 
have "(a*(b*c)) div (d*b*(x*a)) = uu" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

300 
by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

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

303 

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

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

305 

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

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

307 
fix a b c d k uu x y :: "'a::field_inverse_zero" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

309 
assume "(if k = 0 then 0 else x / y) = uu" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

310 
have "(x*k) / (k*y) = uu" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

311 
by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

313 
assume "(if k = 0 then 0 else 1 / y) = uu" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

314 
have "(k) / (k*y) = uu" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

315 
by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

317 
assume "(if b = 0 then 0 else a * c / 1) = uu" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

318 
have "(a*(b*c)) / b = uu" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

319 
by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

321 
assume "(if a = 0 then 0 else if b = 0 then 0 else c / (d * x)) = uu" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

322 
have "(a*(b*c)) / (d*b*(x*a)) = uu" 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

323 
by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact 
d660c4b9daa6
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
huffman
parents:
45285
diff
changeset

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

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

326 

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

327 
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

328 
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

329 

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

332 

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

333 
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

334 
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

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

336 
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

337 
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

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

339 
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

340 
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

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

343 
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

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

345 
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

346 
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

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

348 
end 
45224
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 
subsection {* @{text linordered_ring_le_cancel_factor} *} 
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
diff
changeset

351 

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

352 
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

353 
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

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

355 
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

356 
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

357 
next 
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 \<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

359 
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

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

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

362 

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

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

364 

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

365 
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

366 
fix x uu :: "'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

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

368 
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

369 
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

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

371 
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

372 
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

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

374 
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

375 
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

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

378 

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

379 
lemma "2/3 * (x::rat) + x / 3 = uu" 
45284
ae78a4ffa81d
use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents:
45270
diff
changeset

380 
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

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

382 

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

383 
end 