author  wenzelm 
Wed, 23 Nov 2011 22:59:39 +0100  
changeset 45620  f2a587696afb 
parent 45437  958d19d3405b 
child 45625  750c5a47400b 
permissions  rwrr 
31068
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

1 
(* Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

2 
Copyright 2000 University of Cambridge 
23164  3 

36751
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

4 
Simprocs for the (integer) numerals. 
23164  5 
*) 
6 

7 
(*To quote from Provers/Arith/cancel_numeral_factor.ML: 

8 

9 
Cancels common coefficients in balanced expressions: 

10 

11 
u*#m ~~ u'*#m' == #n*u ~~ #n'*u' 

12 

13 
where ~~ is an appropriate balancing operation (e.g. =, <=, <, div, /) 

14 
and d = gcd(m,m') and n=m/d and n'=m'/d. 

15 
*) 

16 

31068
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

17 
signature NUMERAL_SIMPROCS = 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

18 
sig 
44945  19 
val prep_simproc: theory > string * string list * (theory > simpset > term > thm option) 
20 
> simproc 

21 
val trans_tac: thm option > tactic 

45284
ae78a4ffa81d
use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents:
45270
diff
changeset

22 
val assoc_fold: simpset > cterm > thm option 
ae78a4ffa81d
use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents:
45270
diff
changeset

23 
val combine_numerals: simpset > cterm > thm option 
ae78a4ffa81d
use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents:
45270
diff
changeset

24 
val eq_cancel_numerals: simpset > cterm > thm option 
ae78a4ffa81d
use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents:
45270
diff
changeset

25 
val less_cancel_numerals: simpset > cterm > thm option 
ae78a4ffa81d
use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents:
45270
diff
changeset

26 
val le_cancel_numerals: simpset > cterm > thm option 
ae78a4ffa81d
use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents:
45270
diff
changeset

27 
val eq_cancel_factor: simpset > cterm > thm option 
ae78a4ffa81d
use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents:
45270
diff
changeset

28 
val le_cancel_factor: simpset > cterm > thm option 
ae78a4ffa81d
use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents:
45270
diff
changeset

29 
val less_cancel_factor: simpset > cterm > thm option 
ae78a4ffa81d
use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents:
45270
diff
changeset

30 
val div_cancel_factor: simpset > cterm > thm option 
ae78a4ffa81d
use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents:
45270
diff
changeset

31 
val mod_cancel_factor: simpset > cterm > thm option 
ae78a4ffa81d
use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents:
45270
diff
changeset

32 
val dvd_cancel_factor: simpset > cterm > thm option 
ae78a4ffa81d
use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents:
45270
diff
changeset

33 
val divide_cancel_factor: simpset > cterm > thm option 
ae78a4ffa81d
use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents:
45270
diff
changeset

34 
val eq_cancel_numeral_factor: simpset > cterm > thm option 
ae78a4ffa81d
use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents:
45270
diff
changeset

35 
val less_cancel_numeral_factor: simpset > cterm > thm option 
ae78a4ffa81d
use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents:
45270
diff
changeset

36 
val le_cancel_numeral_factor: simpset > cterm > thm option 
ae78a4ffa81d
use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents:
45270
diff
changeset

37 
val div_cancel_numeral_factor: simpset > cterm > thm option 
ae78a4ffa81d
use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents:
45270
diff
changeset

38 
val divide_cancel_numeral_factor: simpset > cterm > thm option 
ae78a4ffa81d
use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents:
45270
diff
changeset

39 
val field_combine_numerals: simpset > cterm > thm option 
31068
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

40 
val field_cancel_numeral_factors: simproc list 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

41 
val num_ss: simpset 
36751
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

42 
val field_comp_conv: conv 
31068
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

43 
end; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

44 

f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

45 
structure Numeral_Simprocs : NUMERAL_SIMPROCS = 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

46 
struct 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

47 

44945  48 
fun prep_simproc thy (name, pats, proc) = 
49 
Simplifier.simproc_global thy name pats proc; 

50 

51 
fun trans_tac NONE = all_tac 

52 
 trans_tac (SOME th) = ALLGOALS (rtac (th RS trans)); 

53 

33359  54 
val mk_number = Arith_Data.mk_number; 
55 
val mk_sum = Arith_Data.mk_sum; 

56 
val long_mk_sum = Arith_Data.long_mk_sum; 

57 
val dest_sum = Arith_Data.dest_sum; 

31068
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

58 

35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset

59 
val mk_diff = HOLogic.mk_binop @{const_name Groups.minus}; 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset

60 
val dest_diff = HOLogic.dest_bin @{const_name Groups.minus} Term.dummyT; 
31068
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

61 

35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset

62 
val mk_times = HOLogic.mk_binop @{const_name Groups.times}; 
31068
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

63 

35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset

64 
fun one_of T = Const(@{const_name Groups.one}, T); 
31068
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

65 

f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

66 
(* build product with trailing 1 rather than Numeral 1 in order to avoid the 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

67 
unnecessary restriction to type class number_ring 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

68 
which is not required for cancellation of common factors in divisions. 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

69 
*) 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

70 
fun mk_prod T = 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

71 
let val one = one_of T 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

72 
fun mk [] = one 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

73 
 mk [t] = t 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

74 
 mk (t :: ts) = if t = one then mk ts else mk_times (t, mk ts) 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

75 
in mk end; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

76 

f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

77 
(*This version ALWAYS includes a trailing one*) 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

78 
fun long_mk_prod T [] = one_of T 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

79 
 long_mk_prod T (t :: ts) = mk_times (t, mk_prod T ts); 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

80 

35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset

81 
val dest_times = HOLogic.dest_bin @{const_name Groups.times} Term.dummyT; 
31068
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

82 

f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

83 
fun dest_prod t = 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

84 
let val (t,u) = dest_times t 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

85 
in dest_prod t @ dest_prod u end 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

86 
handle TERM _ => [t]; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

87 

33359  88 
fun find_first_numeral past (t::terms) = 
89 
((snd (HOLogic.dest_number t), rev past @ terms) 

90 
handle TERM _ => find_first_numeral (t::past) terms) 

91 
 find_first_numeral past [] = raise TERM("find_first_numeral", []); 

92 

31068
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

93 
(*DON'T do the obvious simplifications; that would create special cases*) 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

94 
fun mk_coeff (k, t) = mk_times (mk_number (Term.fastype_of t) k, t); 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

95 

f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

96 
(*Express t as a product of (possibly) a numeral with other sorted terms*) 
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset

97 
fun dest_coeff sign (Const (@{const_name Groups.uminus}, _) $ t) = dest_coeff (~sign) t 
31068
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

98 
 dest_coeff sign t = 
35408  99 
let val ts = sort Term_Ord.term_ord (dest_prod t) 
31068
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

100 
val (n, ts') = find_first_numeral [] ts 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

101 
handle TERM _ => (1, ts) 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

102 
in (sign*n, mk_prod (Term.fastype_of t) ts') end; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

103 

f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

104 
(*Find first coefficientterm THAT MATCHES u*) 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

105 
fun find_first_coeff past u [] = raise TERM("find_first_coeff", []) 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

106 
 find_first_coeff past u (t::terms) = 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

107 
let val (n,u') = dest_coeff 1 t 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

108 
in if u aconv u' then (n, rev past @ terms) 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

109 
else find_first_coeff (t::past) u terms 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

110 
end 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

111 
handle TERM _ => find_first_coeff (t::past) u terms; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

112 

f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

113 
(*Fractions as pairs of ints. Can't use Rat.rat because the representation 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

114 
needs to preserve negative values in the denominator.*) 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

115 
fun mk_frac (p, q) = if q = 0 then raise Div else (p, q); 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

116 

f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

117 
(*Don't reduce fractions; sums must be proved by rule add_frac_eq. 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

118 
Fractions are reduced later by the cancel_numeral_factor simproc.*) 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

119 
fun add_frac ((p1, q1), (p2, q2)) = (p1 * q2 + p2 * q1, q1 * q2); 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

120 

44064
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
40878
diff
changeset

121 
val mk_divide = HOLogic.mk_binop @{const_name Fields.divide}; 
31068
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

122 

f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

123 
(*Build term (p / q) * t*) 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

124 
fun mk_fcoeff ((p, q), t) = 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

125 
let val T = Term.fastype_of t 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

126 
in mk_times (mk_divide (mk_number T p, mk_number T q), t) end; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

127 

f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

128 
(*Express t as a product of a fraction with other sorted terms*) 
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset

129 
fun dest_fcoeff sign (Const (@{const_name Groups.uminus}, _) $ t) = dest_fcoeff (~sign) t 
44064
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
40878
diff
changeset

130 
 dest_fcoeff sign (Const (@{const_name Fields.divide}, _) $ t $ u) = 
31068
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

131 
let val (p, t') = dest_coeff sign t 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

132 
val (q, u') = dest_coeff 1 u 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

133 
in (mk_frac (p, q), mk_divide (t', u')) end 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

134 
 dest_fcoeff sign t = 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

135 
let val (p, t') = dest_coeff sign t 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

136 
val T = Term.fastype_of t 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

137 
in (mk_frac (p, 1), mk_divide (t', one_of T)) end; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

138 

f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

139 

f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

140 
(** New term ordering so that ACrewriting brings numerals to the front **) 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

141 

f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

142 
(*Order integers by absolute value and then by sign. The standard integer 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

143 
ordering is not wellfounded.*) 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

144 
fun num_ord (i,j) = 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

145 
(case int_ord (abs i, abs j) of 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

146 
EQUAL => int_ord (Int.sign i, Int.sign j) 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

147 
 ord => ord); 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

148 

35408  149 
(*This resembles Term_Ord.term_ord, but it puts binary numerals before other 
31068
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

150 
nonatomic terms.*) 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

151 
local open Term 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

152 
in 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

153 
fun numterm_ord (Abs (_, T, t), Abs(_, U, u)) = 
35408  154 
(case numterm_ord (t, u) of EQUAL => Term_Ord.typ_ord (T, U)  ord => ord) 
31068
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

155 
 numterm_ord 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

156 
(Const(@{const_name Int.number_of}, _) $ v, Const(@{const_name Int.number_of}, _) $ w) = 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

157 
num_ord (HOLogic.dest_numeral v, HOLogic.dest_numeral w) 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

158 
 numterm_ord (Const(@{const_name Int.number_of}, _) $ _, _) = LESS 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

159 
 numterm_ord (_, Const(@{const_name Int.number_of}, _) $ _) = GREATER 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

160 
 numterm_ord (t, u) = 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

161 
(case int_ord (size_of_term t, size_of_term u) of 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

162 
EQUAL => 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

163 
let val (f, ts) = strip_comb t and (g, us) = strip_comb u in 
35408  164 
(case Term_Ord.hd_ord (f, g) of EQUAL => numterms_ord (ts, us)  ord => ord) 
31068
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

165 
end 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

166 
 ord => ord) 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

167 
and numterms_ord (ts, us) = list_ord numterm_ord (ts, us) 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

168 
end; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

169 

f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

170 
fun numtermless tu = (numterm_ord tu = LESS); 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

171 

f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

172 
val num_ss = HOL_ss settermless numtermless; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

173 

f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

174 
(*Maps 0 to Numeral0 and 1 to Numeral1 so that arithmetic isn't complicated by the abstract 0 and 1.*) 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

175 
val numeral_syms = [@{thm numeral_0_eq_0} RS sym, @{thm numeral_1_eq_1} RS sym]; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

176 

f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

177 
(*Simplify Numeral0+n, n+Numeral0, Numeral1*n, n*Numeral1, 1*x, x*1, x/1 *) 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

178 
val add_0s = @{thms add_0s}; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

179 
val mult_1s = @{thms mult_1s mult_1_left mult_1_right divide_1}; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

180 

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

181 
(* For postsimplification of the rhs of simprocgenerated rules *) 
958d19d3405b
tune postprocessing of simprocgenerated rules so they won't produce Numeral0 or Numeral1
huffman
parents:
45306
diff
changeset

182 
val post_simps = 
958d19d3405b
tune postprocessing of simprocgenerated rules so they won't produce Numeral0 or Numeral1
huffman
parents:
45306
diff
changeset

183 
[@{thm numeral_0_eq_0}, @{thm numeral_1_eq_1}, 
958d19d3405b
tune postprocessing of simprocgenerated rules so they won't produce Numeral0 or Numeral1
huffman
parents:
45306
diff
changeset

184 
@{thm add_0_left}, @{thm add_0_right}, 
958d19d3405b
tune postprocessing of simprocgenerated rules so they won't produce Numeral0 or Numeral1
huffman
parents:
45306
diff
changeset

185 
@{thm mult_zero_left}, @{thm mult_zero_right}, 
958d19d3405b
tune postprocessing of simprocgenerated rules so they won't produce Numeral0 or Numeral1
huffman
parents:
45306
diff
changeset

186 
@{thm mult_1_left}, @{thm mult_1_right}, 
958d19d3405b
tune postprocessing of simprocgenerated rules so they won't produce Numeral0 or Numeral1
huffman
parents:
45306
diff
changeset

187 
@{thm mult_minus1}, @{thm mult_minus1_right}] 
958d19d3405b
tune postprocessing of simprocgenerated rules so they won't produce Numeral0 or Numeral1
huffman
parents:
45306
diff
changeset

188 

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

189 
val field_post_simps = 
958d19d3405b
tune postprocessing of simprocgenerated rules so they won't produce Numeral0 or Numeral1
huffman
parents:
45306
diff
changeset

190 
post_simps @ [@{thm divide_zero_left}, @{thm divide_1}] 
958d19d3405b
tune postprocessing of simprocgenerated rules so they won't produce Numeral0 or Numeral1
huffman
parents:
45306
diff
changeset

191 

31068
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

192 
(*Simplify inverse Numeral1, a/Numeral1*) 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

193 
val inverse_1s = [@{thm inverse_numeral_1}]; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

194 
val divide_1s = [@{thm divide_numeral_1}]; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

195 

f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

196 
(*To perform binary arithmetic. The "left" rewriting handles patterns 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

197 
created by the Numeral_Simprocs, such as 3 * (5 * x). *) 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

198 
val simps = [@{thm numeral_0_eq_0} RS sym, @{thm numeral_1_eq_1} RS sym, 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

199 
@{thm add_number_of_left}, @{thm mult_number_of_left}] @ 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

200 
@{thms arith_simps} @ @{thms rel_simps}; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

201 

f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

202 
(*Binary arithmetic BUT NOT ADDITION since it may collapse adjacent terms 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

203 
during rearrangement*) 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

204 
val non_add_simps = 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

205 
subtract Thm.eq_thm [@{thm add_number_of_left}, @{thm number_of_add} RS sym] simps; 
23164  206 

31068
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

207 
(*To evaluate binary negations of coefficients*) 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

208 
val minus_simps = [@{thm numeral_m1_eq_minus_1} RS sym, @{thm number_of_minus} RS sym] @ 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

209 
@{thms minus_bin_simps} @ @{thms pred_bin_simps}; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

210 

f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

211 
(*To let us treat subtraction as addition*) 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

212 
val diff_simps = [@{thm diff_minus}, @{thm minus_add_distrib}, @{thm minus_minus}]; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

213 

f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

214 
(*To let us treat division as multiplication*) 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

215 
val divide_simps = [@{thm divide_inverse}, @{thm inverse_mult_distrib}, @{thm inverse_inverse_eq}]; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

216 

35020
862a20ffa8e2
prefer explicit @{lemma} over adhoc forward reasoning;
wenzelm
parents:
34974
diff
changeset

217 
(*push the unary minus down*) 
862a20ffa8e2
prefer explicit @{lemma} over adhoc forward reasoning;
wenzelm
parents:
34974
diff
changeset

218 
val minus_mult_eq_1_to_2 = @{lemma " (a::'a::ring) * b = a *  b" by simp}; 
31068
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

219 

f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

220 
(*to extract again any uncancelled minuses*) 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

221 
val minus_from_mult_simps = 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

222 
[@{thm minus_minus}, @{thm mult_minus_left}, @{thm mult_minus_right}]; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

223 

f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

224 
(*combine unary minus with numeric literals, however nested within a product*) 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

225 
val mult_minus_simps = 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

226 
[@{thm mult_assoc}, @{thm minus_mult_left}, minus_mult_eq_1_to_2]; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

227 

f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

228 
val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @ 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

229 
diff_simps @ minus_simps @ @{thms add_ac} 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

230 
val norm_ss2 = num_ss addsimps non_add_simps @ mult_minus_simps 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

231 
val norm_ss3 = num_ss addsimps minus_from_mult_simps @ @{thms add_ac} @ @{thms mult_ac} 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

232 

f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

233 
structure CancelNumeralsCommon = 
44945  234 
struct 
235 
val mk_sum = mk_sum 

236 
val dest_sum = dest_sum 

237 
val mk_coeff = mk_coeff 

238 
val dest_coeff = dest_coeff 1 

239 
val find_first_coeff = find_first_coeff [] 

44947
8ae418dfe561
dropped unused argument â€“ avoids problem with SML/NJ
haftmann
parents:
44945
diff
changeset

240 
val trans_tac = trans_tac 
31068
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

241 

f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

242 
fun norm_tac ss = 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

243 
ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1)) 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

244 
THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2)) 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

245 
THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3)) 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

246 

f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

247 
val numeral_simp_ss = HOL_ss addsimps add_0s @ simps 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

248 
fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) 
45437
958d19d3405b
tune postprocessing of simprocgenerated rules so they won't produce Numeral0 or Numeral1
huffman
parents:
45306
diff
changeset

249 
val simplify_meta_eq = Arith_Data.simplify_meta_eq post_simps 
44945  250 
val prove_conv = Arith_Data.prove_conv 
251 
end; 

31068
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

252 

f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

253 
structure EqCancelNumerals = CancelNumeralsFun 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

254 
(open CancelNumeralsCommon 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

255 
val mk_bal = HOLogic.mk_eq 
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38549
diff
changeset

256 
val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} Term.dummyT 
31068
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

257 
val bal_add1 = @{thm eq_add_iff1} RS trans 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

258 
val bal_add2 = @{thm eq_add_iff2} RS trans 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

259 
); 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

260 

f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

261 
structure LessCancelNumerals = CancelNumeralsFun 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

262 
(open CancelNumeralsCommon 
35092
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35084
diff
changeset

263 
val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less} 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35084
diff
changeset

264 
val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} Term.dummyT 
31068
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

265 
val bal_add1 = @{thm less_add_iff1} RS trans 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

266 
val bal_add2 = @{thm less_add_iff2} RS trans 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

267 
); 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

268 

f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

269 
structure LeCancelNumerals = CancelNumeralsFun 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

270 
(open CancelNumeralsCommon 
35092
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35084
diff
changeset

271 
val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq} 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35084
diff
changeset

272 
val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} Term.dummyT 
31068
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

273 
val bal_add1 = @{thm le_add_iff1} RS trans 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

274 
val bal_add2 = @{thm le_add_iff2} RS trans 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

275 
); 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

276 

45284
ae78a4ffa81d
use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents:
45270
diff
changeset

277 
fun eq_cancel_numerals ss ct = EqCancelNumerals.proc ss (term_of ct) 
ae78a4ffa81d
use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents:
45270
diff
changeset

278 
fun less_cancel_numerals ss ct = LessCancelNumerals.proc ss (term_of ct) 
ae78a4ffa81d
use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents:
45270
diff
changeset

279 
fun le_cancel_numerals ss ct = LeCancelNumerals.proc ss (term_of ct) 
31068
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

280 

f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

281 
structure CombineNumeralsData = 
44945  282 
struct 
283 
type coeff = int 

284 
val iszero = (fn x => x = 0) 

285 
val add = op + 

286 
val mk_sum = long_mk_sum (*to work for e.g. 2*x + 3*x *) 

287 
val dest_sum = dest_sum 

288 
val mk_coeff = mk_coeff 

289 
val dest_coeff = dest_coeff 1 

290 
val left_distrib = @{thm combine_common_factor} RS trans 

291 
val prove_conv = Arith_Data.prove_conv_nohyps 

44947
8ae418dfe561
dropped unused argument â€“ avoids problem with SML/NJ
haftmann
parents:
44945
diff
changeset

292 
val trans_tac = trans_tac 
31068
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

293 

f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

294 
fun norm_tac ss = 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

295 
ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1)) 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

296 
THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2)) 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

297 
THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3)) 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

298 

f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

299 
val numeral_simp_ss = HOL_ss addsimps add_0s @ simps 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

300 
fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) 
45437
958d19d3405b
tune postprocessing of simprocgenerated rules so they won't produce Numeral0 or Numeral1
huffman
parents:
45306
diff
changeset

301 
val simplify_meta_eq = Arith_Data.simplify_meta_eq post_simps 
44945  302 
end; 
31068
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

303 

f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

304 
structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData); 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

305 

f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

306 
(*Version for fields, where coefficients can be fractions*) 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

307 
structure FieldCombineNumeralsData = 
44945  308 
struct 
309 
type coeff = int * int 

310 
val iszero = (fn (p, q) => p = 0) 

311 
val add = add_frac 

312 
val mk_sum = long_mk_sum 

313 
val dest_sum = dest_sum 

314 
val mk_coeff = mk_fcoeff 

315 
val dest_coeff = dest_fcoeff 1 

316 
val left_distrib = @{thm combine_common_factor} RS trans 

317 
val prove_conv = Arith_Data.prove_conv_nohyps 

44947
8ae418dfe561
dropped unused argument â€“ avoids problem with SML/NJ
haftmann
parents:
44945
diff
changeset

318 
val trans_tac = trans_tac 
31068
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

319 

f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

320 
val norm_ss1a = norm_ss1 addsimps inverse_1s @ divide_simps 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

321 
fun norm_tac ss = 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

322 
ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1a)) 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

323 
THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2)) 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

324 
THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3)) 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

325 

f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

326 
val numeral_simp_ss = HOL_ss addsimps add_0s @ simps @ [@{thm add_frac_eq}] 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

327 
fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) 
45437
958d19d3405b
tune postprocessing of simprocgenerated rules so they won't produce Numeral0 or Numeral1
huffman
parents:
45306
diff
changeset

328 
val simplify_meta_eq = Arith_Data.simplify_meta_eq field_post_simps 
44945  329 
end; 
31068
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

330 

f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

331 
structure FieldCombineNumerals = CombineNumeralsFun(FieldCombineNumeralsData); 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

332 

45284
ae78a4ffa81d
use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents:
45270
diff
changeset

333 
fun combine_numerals ss ct = CombineNumerals.proc ss (term_of ct) 
31068
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

334 

45284
ae78a4ffa81d
use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents:
45270
diff
changeset

335 
fun field_combine_numerals ss ct = FieldCombineNumerals.proc ss (term_of ct) 
31068
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

336 

f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

337 
(** Constant folding for multiplication in semirings **) 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

338 

f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

339 
(*We do not need folding for addition: combine_numerals does the same thing*) 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

340 

f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

341 
structure Semiring_Times_Assoc_Data : ASSOC_FOLD_DATA = 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

342 
struct 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

343 
val assoc_ss = HOL_ss addsimps @{thms mult_ac} 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

344 
val eq_reflection = eq_reflection 
35983
27e2fa7d4ce7
slightly more general simproc (avoids errors of linarith)
boehmes
parents:
35408
diff
changeset

345 
val is_numeral = can HOLogic.dest_number 
31068
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

346 
end; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

347 

f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

348 
structure Semiring_Times_Assoc = Assoc_Fold (Semiring_Times_Assoc_Data); 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

349 

45284
ae78a4ffa81d
use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents:
45270
diff
changeset

350 
fun assoc_fold ss ct = Semiring_Times_Assoc.proc ss (term_of ct) 
23164  351 

352 
structure CancelNumeralFactorCommon = 

44945  353 
struct 
354 
val mk_coeff = mk_coeff 

355 
val dest_coeff = dest_coeff 1 

44947
8ae418dfe561
dropped unused argument â€“ avoids problem with SML/NJ
haftmann
parents:
44945
diff
changeset

356 
val trans_tac = trans_tac 
23164  357 

44983
b36eedcd1633
numeral_simprocs.ML: use HOL_basic_ss instead of HOL_ss for internal normalization proofs of cancel_factor simprocs, to avoid splitting ifthenelse
huffman
parents:
44064
diff
changeset

358 
val norm_ss1 = HOL_basic_ss addsimps minus_from_mult_simps @ mult_1s 
b36eedcd1633
numeral_simprocs.ML: use HOL_basic_ss instead of HOL_ss for internal normalization proofs of cancel_factor simprocs, to avoid splitting ifthenelse
huffman
parents:
44064
diff
changeset

359 
val norm_ss2 = HOL_basic_ss addsimps simps @ mult_minus_simps 
b36eedcd1633
numeral_simprocs.ML: use HOL_basic_ss instead of HOL_ss for internal normalization proofs of cancel_factor simprocs, to avoid splitting ifthenelse
huffman
parents:
44064
diff
changeset

360 
val norm_ss3 = HOL_basic_ss addsimps @{thms mult_ac} 
23164  361 
fun norm_tac ss = 
362 
ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1)) 

363 
THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2)) 

364 
THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3)) 

365 

31068
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

366 
val numeral_simp_ss = HOL_ss addsimps 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

367 
[@{thm eq_number_of_eq}, @{thm less_number_of}, @{thm le_number_of}] @ simps 
23164  368 
fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) 
30518  369 
val simplify_meta_eq = Arith_Data.simplify_meta_eq 
45437
958d19d3405b
tune postprocessing of simprocgenerated rules so they won't produce Numeral0 or Numeral1
huffman
parents:
45306
diff
changeset

370 
([@{thm Nat.add_0}, @{thm Nat.add_0_right}] @ post_simps) 
44945  371 
val prove_conv = Arith_Data.prove_conv 
372 
end 

23164  373 

30931
86ca651da03e
generalized some simprocs from int to semiring_div
haftmann
parents:
30685
diff
changeset

374 
(*Version for semiring_div*) 
86ca651da03e
generalized some simprocs from int to semiring_div
haftmann
parents:
30685
diff
changeset

375 
structure DivCancelNumeralFactor = CancelNumeralFactorFun 
23164  376 
(open CancelNumeralFactorCommon 
377 
val mk_bal = HOLogic.mk_binop @{const_name Divides.div} 

30931
86ca651da03e
generalized some simprocs from int to semiring_div
haftmann
parents:
30685
diff
changeset

378 
val dest_bal = HOLogic.dest_bin @{const_name Divides.div} Term.dummyT 
86ca651da03e
generalized some simprocs from int to semiring_div
haftmann
parents:
30685
diff
changeset

379 
val cancel = @{thm div_mult_mult1} RS trans 
23164  380 
val neg_exchanges = false 
381 
) 

382 

383 
(*Version for fields*) 

384 
structure DivideCancelNumeralFactor = CancelNumeralFactorFun 

385 
(open CancelNumeralFactorCommon 

44064
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
40878
diff
changeset

386 
val mk_bal = HOLogic.mk_binop @{const_name Fields.divide} 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
40878
diff
changeset

387 
val dest_bal = HOLogic.dest_bin @{const_name Fields.divide} Term.dummyT 
23413
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23401
diff
changeset

388 
val cancel = @{thm mult_divide_mult_cancel_left} RS trans 
23164  389 
val neg_exchanges = false 
390 
) 

391 

392 
structure EqCancelNumeralFactor = CancelNumeralFactorFun 

393 
(open CancelNumeralFactorCommon 

394 
val mk_bal = HOLogic.mk_eq 

38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38549
diff
changeset

395 
val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} Term.dummyT 
23164  396 
val cancel = @{thm mult_cancel_left} RS trans 
397 
val neg_exchanges = false 

398 
) 

399 

400 
structure LessCancelNumeralFactor = CancelNumeralFactorFun 

401 
(open CancelNumeralFactorCommon 

35092
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35084
diff
changeset

402 
val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less} 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35084
diff
changeset

403 
val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} Term.dummyT 
23164  404 
val cancel = @{thm mult_less_cancel_left} RS trans 
405 
val neg_exchanges = true 

406 
) 

407 

408 
structure LeCancelNumeralFactor = CancelNumeralFactorFun 

409 
(open CancelNumeralFactorCommon 

35092
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35084
diff
changeset

410 
val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq} 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35084
diff
changeset

411 
val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} Term.dummyT 
23164  412 
val cancel = @{thm mult_le_cancel_left} RS trans 
413 
val neg_exchanges = true 

414 
) 

415 

45284
ae78a4ffa81d
use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents:
45270
diff
changeset

416 
fun eq_cancel_numeral_factor ss ct = EqCancelNumeralFactor.proc ss (term_of ct) 
ae78a4ffa81d
use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents:
45270
diff
changeset

417 
fun less_cancel_numeral_factor ss ct = LessCancelNumeralFactor.proc ss (term_of ct) 
ae78a4ffa81d
use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents:
45270
diff
changeset

418 
fun le_cancel_numeral_factor ss ct = LeCancelNumeralFactor.proc ss (term_of ct) 
ae78a4ffa81d
use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents:
45270
diff
changeset

419 
fun div_cancel_numeral_factor ss ct = DivCancelNumeralFactor.proc ss (term_of ct) 
ae78a4ffa81d
use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents:
45270
diff
changeset

420 
fun divide_cancel_numeral_factor ss ct = DivideCancelNumeralFactor.proc ss (term_of ct) 
23164  421 

422 
val field_cancel_numeral_factors = 

44945  423 
map (prep_simproc @{theory}) 
23164  424 
[("field_eq_cancel_numeral_factor", 
425 
["(l::'a::{field,number_ring}) * m = n", 

426 
"(l::'a::{field,number_ring}) = m * n"], 

427 
K EqCancelNumeralFactor.proc), 

428 
("field_cancel_numeral_factor", 

36409  429 
["((l::'a::{field_inverse_zero,number_ring}) * m) / n", 
430 
"(l::'a::{field_inverse_zero,number_ring}) / (m * n)", 

431 
"((number_of v)::'a::{field_inverse_zero,number_ring}) / (number_of w)"], 

23164  432 
K DivideCancelNumeralFactor.proc)] 
433 

434 

435 
(** Declarations for ExtractCommonTerm **) 

436 

437 
(*Find first term that matches u*) 

438 
fun find_first_t past u [] = raise TERM ("find_first_t", []) 

439 
 find_first_t past u (t::terms) = 

440 
if u aconv t then (rev past @ terms) 

441 
else find_first_t (t::past) u terms 

442 
handle TERM _ => find_first_t (t::past) u terms; 

443 

444 
(** Final simplification for the CancelFactor simprocs **) 

30518  445 
val simplify_one = Arith_Data.simplify_meta_eq 
30031  446 
[@{thm mult_1_left}, @{thm mult_1_right}, @{thm div_by_1}, @{thm numeral_1_eq_1}]; 
23164  447 

30649
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset

448 
fun cancel_simplify_meta_eq ss cancel_th th = 
23164  449 
simplify_one ss (([th, cancel_th]) MRS trans); 
450 

30649
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset

451 
local 
31067  452 
val Tp_Eq = Thm.reflexive (Thm.cterm_of @{theory HOL} HOLogic.Trueprop) 
30649
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset

453 
fun Eq_True_elim Eq = 
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset

454 
Thm.equal_elim (Thm.combination Tp_Eq (Thm.symmetric Eq)) @{thm TrueI} 
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset

455 
in 
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset

456 
fun sign_conv pos_th neg_th ss t = 
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset

457 
let val T = fastype_of t; 
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset

458 
val zero = Const(@{const_name Groups.zero}, T); 
35092
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35084
diff
changeset

459 
val less = Const(@{const_name Orderings.less}, [T,T] > HOLogic.boolT); 
30649
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset

460 
val pos = less $ zero $ t and neg = less $ t $ zero 
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset

461 
fun prove p = 
31101
26c7bb764a38
qualified names for Lin_Arith tactics and simprocs
haftmann
parents:
31068
diff
changeset

462 
Option.map Eq_True_elim (Lin_Arith.simproc ss p) 
30649
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset

463 
handle THM _ => NONE 
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset

464 
in case prove pos of 
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset

465 
SOME th => SOME(th RS pos_th) 
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset

466 
 NONE => (case prove neg of 
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset

467 
SOME th => SOME(th RS neg_th) 
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset

468 
 NONE => NONE) 
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset

469 
end; 
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset

470 
end 
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset

471 

23164  472 
structure CancelFactorCommon = 
44945  473 
struct 
474 
val mk_sum = long_mk_prod 

475 
val dest_sum = dest_prod 

476 
val mk_coeff = mk_coeff 

477 
val dest_coeff = dest_coeff 

478 
val find_first = find_first_t [] 

44947
8ae418dfe561
dropped unused argument â€“ avoids problem with SML/NJ
haftmann
parents:
44945
diff
changeset

479 
val trans_tac = trans_tac 
23881  480 
val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac} 
23164  481 
fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss)) 
30649
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset

482 
val simplify_meta_eq = cancel_simplify_meta_eq 
45270
d5b5c9259afd
fix bug in cancel_factor simprocs so they will work on goals like 'x * y < x * z' where the common term is already on the left
huffman
parents:
44984
diff
changeset

483 
fun mk_eq (a, b) = HOLogic.mk_Trueprop (HOLogic.mk_eq (a, b)) 
44945  484 
end; 
23164  485 

486 
(*mult_cancel_left requires a ring with no zero divisors.*) 

487 
structure EqCancelFactor = ExtractCommonTermFun 

488 
(open CancelFactorCommon 

489 
val mk_bal = HOLogic.mk_eq 

38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38549
diff
changeset

490 
val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} Term.dummyT 
31368  491 
fun simp_conv _ _ = SOME @{thm mult_cancel_left} 
30649
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset

492 
); 
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset

493 

57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset

494 
(*for ordered rings*) 
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset

495 
structure LeCancelFactor = ExtractCommonTermFun 
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset

496 
(open CancelFactorCommon 
35092
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35084
diff
changeset

497 
val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq} 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35084
diff
changeset

498 
val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} Term.dummyT 
30649
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset

499 
val simp_conv = sign_conv 
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset

500 
@{thm mult_le_cancel_left_pos} @{thm mult_le_cancel_left_neg} 
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset

501 
); 
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset

502 

57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset

503 
(*for ordered rings*) 
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset

504 
structure LessCancelFactor = ExtractCommonTermFun 
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset

505 
(open CancelFactorCommon 
35092
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35084
diff
changeset

506 
val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less} 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35084
diff
changeset

507 
val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} Term.dummyT 
30649
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset

508 
val simp_conv = sign_conv 
57753e0ec1d4
1. New cancellation simprocs for common factors in inequations
nipkow
parents:
30518
diff
changeset

509 
@{thm mult_less_cancel_left_pos} @{thm mult_less_cancel_left_neg} 
23164  510 
); 
511 

30931
86ca651da03e
generalized some simprocs from int to semiring_div
haftmann
parents:
30685
diff
changeset

512 
(*for semirings with division*) 
86ca651da03e
generalized some simprocs from int to semiring_div
haftmann
parents:
30685
diff
changeset

513 
structure DivCancelFactor = ExtractCommonTermFun 
23164  514 
(open CancelFactorCommon 
515 
val mk_bal = HOLogic.mk_binop @{const_name Divides.div} 

30931
86ca651da03e
generalized some simprocs from int to semiring_div
haftmann
parents:
30685
diff
changeset

516 
val dest_bal = HOLogic.dest_bin @{const_name Divides.div} Term.dummyT 
31368  517 
fun simp_conv _ _ = SOME @{thm div_mult_mult1_if} 
23164  518 
); 
519 

30931
86ca651da03e
generalized some simprocs from int to semiring_div
haftmann
parents:
30685
diff
changeset

520 
structure ModCancelFactor = ExtractCommonTermFun 
24395  521 
(open CancelFactorCommon 
522 
val mk_bal = HOLogic.mk_binop @{const_name Divides.mod} 

31067  523 
val dest_bal = HOLogic.dest_bin @{const_name Divides.mod} Term.dummyT 
31368  524 
fun simp_conv _ _ = SOME @{thm mod_mult_mult1} 
24395  525 
); 
526 

30931
86ca651da03e
generalized some simprocs from int to semiring_div
haftmann
parents:
30685
diff
changeset

527 
(*for idoms*) 
86ca651da03e
generalized some simprocs from int to semiring_div
haftmann
parents:
30685
diff
changeset

528 
structure DvdCancelFactor = ExtractCommonTermFun 
23969  529 
(open CancelFactorCommon 
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35043
diff
changeset

530 
val mk_bal = HOLogic.mk_binrel @{const_name Rings.dvd} 
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35043
diff
changeset

531 
val dest_bal = HOLogic.dest_bin @{const_name Rings.dvd} Term.dummyT 
31368  532 
fun simp_conv _ _ = SOME @{thm dvd_mult_cancel_left} 
23969  533 
); 
534 

23164  535 
(*Version for all fields, including unordered ones (type complex).*) 
536 
structure DivideCancelFactor = ExtractCommonTermFun 

537 
(open CancelFactorCommon 

44064
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
40878
diff
changeset

538 
val mk_bal = HOLogic.mk_binop @{const_name Fields.divide} 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
40878
diff
changeset

539 
val dest_bal = HOLogic.dest_bin @{const_name Fields.divide} Term.dummyT 
31368  540 
fun simp_conv _ _ = SOME @{thm mult_divide_mult_cancel_left_if} 
23164  541 
); 
542 

45284
ae78a4ffa81d
use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents:
45270
diff
changeset

543 
fun eq_cancel_factor ss ct = EqCancelFactor.proc ss (term_of ct) 
ae78a4ffa81d
use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents:
45270
diff
changeset

544 
fun le_cancel_factor ss ct = LeCancelFactor.proc ss (term_of ct) 
ae78a4ffa81d
use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents:
45270
diff
changeset

545 
fun less_cancel_factor ss ct = LessCancelFactor.proc ss (term_of ct) 
ae78a4ffa81d
use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents:
45270
diff
changeset

546 
fun div_cancel_factor ss ct = DivCancelFactor.proc ss (term_of ct) 
ae78a4ffa81d
use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents:
45270
diff
changeset

547 
fun mod_cancel_factor ss ct = ModCancelFactor.proc ss (term_of ct) 
ae78a4ffa81d
use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents:
45270
diff
changeset

548 
fun dvd_cancel_factor ss ct = DvdCancelFactor.proc ss (term_of ct) 
ae78a4ffa81d
use simproc_setup for cancellation simprocs, to get proper name bindings
huffman
parents:
45270
diff
changeset

549 
fun divide_cancel_factor ss ct = DivideCancelFactor.proc ss (term_of ct) 
23164  550 

36751
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

551 
local 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

552 
val zr = @{cpat "0"} 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

553 
val zT = ctyp_of_term zr 
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38549
diff
changeset

554 
val geq = @{cpat HOL.eq} 
36751
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

555 
val eqT = Thm.dest_ctyp (ctyp_of_term geq) > hd 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

556 
val add_frac_eq = mk_meta_eq @{thm "add_frac_eq"} 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

557 
val add_frac_num = mk_meta_eq @{thm "add_frac_num"} 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

558 
val add_num_frac = mk_meta_eq @{thm "add_num_frac"} 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

559 

7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

560 
fun prove_nz ss T t = 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

561 
let 
36945  562 
val z = Thm.instantiate_cterm ([(zT,T)],[]) zr 
563 
val eq = Thm.instantiate_cterm ([(eqT,T)],[]) geq 

36751
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

564 
val th = Simplifier.rewrite (ss addsimps @{thms simp_thms}) 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

565 
(Thm.capply @{cterm "Trueprop"} (Thm.capply @{cterm "Not"} 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

566 
(Thm.capply (Thm.capply eq t) z))) 
36945  567 
in Thm.equal_elim (Thm.symmetric th) TrueI 
36751
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

568 
end 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

569 

7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

570 
fun proc phi ss ct = 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

571 
let 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

572 
val ((x,y),(w,z)) = 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

573 
(Thm.dest_binop #> (fn (a,b) => (Thm.dest_binop a, Thm.dest_binop b))) ct 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

574 
val _ = map (HOLogic.dest_number o term_of) [x,y,z,w] 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

575 
val T = ctyp_of_term x 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

576 
val [y_nz, z_nz] = map (prove_nz ss T) [y, z] 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

577 
val th = instantiate' [SOME T] (map SOME [y,z,x,w]) add_frac_eq 
36945  578 
in SOME (Thm.implies_elim (Thm.implies_elim th y_nz) z_nz) 
36751
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

579 
end 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

580 
handle CTERM _ => NONE  TERM _ => NONE  THM _ => NONE 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

581 

7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

582 
fun proc2 phi ss ct = 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

583 
let 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

584 
val (l,r) = Thm.dest_binop ct 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

585 
val T = ctyp_of_term l 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

586 
in (case (term_of l, term_of r) of 
44064
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
40878
diff
changeset

587 
(Const(@{const_name Fields.divide},_)$_$_, _) => 
36751
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

588 
let val (x,y) = Thm.dest_binop l val z = r 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

589 
val _ = map (HOLogic.dest_number o term_of) [x,y,z] 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

590 
val ynz = prove_nz ss T y 
36945  591 
in SOME (Thm.implies_elim (instantiate' [SOME T] (map SOME [y,x,z]) add_frac_num) ynz) 
36751
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

592 
end 
44064
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
40878
diff
changeset

593 
 (_, Const (@{const_name Fields.divide},_)$_$_) => 
36751
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

594 
let val (x,y) = Thm.dest_binop r val z = l 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

595 
val _ = map (HOLogic.dest_number o term_of) [x,y,z] 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

596 
val ynz = prove_nz ss T y 
36945  597 
in SOME (Thm.implies_elim (instantiate' [SOME T] (map SOME [y,z,x]) add_num_frac) ynz) 
36751
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

598 
end 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

599 
 _ => NONE) 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

600 
end 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

601 
handle CTERM _ => NONE  TERM _ => NONE  THM _ => NONE 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

602 

44064
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
40878
diff
changeset

603 
fun is_number (Const(@{const_name Fields.divide},_)$a$b) = is_number a andalso is_number b 
36751
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

604 
 is_number t = can HOLogic.dest_number t 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

605 

7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

606 
val is_number = is_number o term_of 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

607 

7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

608 
fun proc3 phi ss ct = 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

609 
(case term_of ct of 
44064
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
40878
diff
changeset

610 
Const(@{const_name Orderings.less},_)$(Const(@{const_name Fields.divide},_)$_$_)$_ => 
36751
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

611 
let 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

612 
val ((a,b),c) = Thm.dest_binop ct >> Thm.dest_binop 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

613 
val _ = map is_number [a,b,c] 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

614 
val T = ctyp_of_term c 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

615 
val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_less_eq"} 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

616 
in SOME (mk_meta_eq th) end 
44064
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
40878
diff
changeset

617 
 Const(@{const_name Orderings.less_eq},_)$(Const(@{const_name Fields.divide},_)$_$_)$_ => 
36751
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

618 
let 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

619 
val ((a,b),c) = Thm.dest_binop ct >> Thm.dest_binop 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

620 
val _ = map is_number [a,b,c] 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

621 
val T = ctyp_of_term c 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

622 
val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_le_eq"} 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

623 
in SOME (mk_meta_eq th) end 
44064
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
40878
diff
changeset

624 
 Const(@{const_name HOL.eq},_)$(Const(@{const_name Fields.divide},_)$_$_)$_ => 
36751
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

625 
let 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

626 
val ((a,b),c) = Thm.dest_binop ct >> Thm.dest_binop 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

627 
val _ = map is_number [a,b,c] 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

628 
val T = ctyp_of_term c 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

629 
val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_eq_eq"} 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

630 
in SOME (mk_meta_eq th) end 
44064
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
40878
diff
changeset

631 
 Const(@{const_name Orderings.less},_)$_$(Const(@{const_name Fields.divide},_)$_$_) => 
36751
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

632 
let 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

633 
val (a,(b,c)) = Thm.dest_binop ct > Thm.dest_binop 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

634 
val _ = map is_number [a,b,c] 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

635 
val T = ctyp_of_term c 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

636 
val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "less_divide_eq"} 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

637 
in SOME (mk_meta_eq th) end 
44064
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
40878
diff
changeset

638 
 Const(@{const_name Orderings.less_eq},_)$_$(Const(@{const_name Fields.divide},_)$_$_) => 
36751
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

639 
let 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

640 
val (a,(b,c)) = Thm.dest_binop ct > Thm.dest_binop 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

641 
val _ = map is_number [a,b,c] 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

642 
val T = ctyp_of_term c 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

643 
val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "le_divide_eq"} 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

644 
in SOME (mk_meta_eq th) end 
44064
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
40878
diff
changeset

645 
 Const(@{const_name HOL.eq},_)$_$(Const(@{const_name Fields.divide},_)$_$_) => 
36751
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

646 
let 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

647 
val (a,(b,c)) = Thm.dest_binop ct > Thm.dest_binop 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

648 
val _ = map is_number [a,b,c] 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

649 
val T = ctyp_of_term c 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

650 
val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "eq_divide_eq"} 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

651 
in SOME (mk_meta_eq th) end 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

652 
 _ => NONE) 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

653 
handle TERM _ => NONE  CTERM _ => NONE  THM _ => NONE 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

654 

7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

655 
val add_frac_frac_simproc = 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

656 
make_simproc {lhss = [@{cpat "(?x::?'a::field)/?y + (?w::?'a::field)/?z"}], 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

657 
name = "add_frac_frac_simproc", 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

658 
proc = proc, identifier = []} 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

659 

7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

660 
val add_frac_num_simproc = 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

661 
make_simproc {lhss = [@{cpat "(?x::?'a::field)/?y + ?z"}, @{cpat "?z + (?x::?'a::field)/?y"}], 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

662 
name = "add_frac_num_simproc", 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

663 
proc = proc2, identifier = []} 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

664 

7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

665 
val ord_frac_simproc = 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

666 
make_simproc 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

667 
{lhss = [@{cpat "(?a::(?'a::{field, ord}))/?b < ?c"}, 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

668 
@{cpat "(?a::(?'a::{field, ord}))/?b <= ?c"}, 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

669 
@{cpat "?c < (?a::(?'a::{field, ord}))/?b"}, 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

670 
@{cpat "?c <= (?a::(?'a::{field, ord}))/?b"}, 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

671 
@{cpat "?c = ((?a::(?'a::{field, ord}))/?b)"}, 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

672 
@{cpat "((?a::(?'a::{field, ord}))/ ?b) = ?c"}], 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

673 
name = "ord_frac_simproc", proc = proc3, identifier = []} 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

674 

7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

675 
val ths = [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"}, 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

676 
@{thm "divide_Numeral1"}, 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

677 
@{thm "divide_zero"}, @{thm "divide_Numeral0"}, 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

678 
@{thm "divide_divide_eq_left"}, 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

679 
@{thm "times_divide_eq_left"}, @{thm "times_divide_eq_right"}, 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

680 
@{thm "times_divide_times_eq"}, 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

681 
@{thm "divide_divide_eq_right"}, 
37887  682 
@{thm "diff_minus"}, @{thm "minus_divide_left"}, 
36751
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

683 
@{thm "Numeral1_eq1_nat"}, @{thm "add_divide_distrib"} RS sym, 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

684 
@{thm field_divide_inverse} RS sym, @{thm inverse_divide}, 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

685 
Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv (Conv.rewr_conv (mk_meta_eq @{thm mult_commute})))) 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

686 
(@{thm field_divide_inverse} RS sym)] 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

687 

7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

688 
in 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

689 

45620
f2a587696afb
modernized some oldstyle infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45437
diff
changeset

690 
val field_comp_conv = 
f2a587696afb
modernized some oldstyle infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45437
diff
changeset

691 
Simplifier.rewrite 
f2a587696afb
modernized some oldstyle infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45437
diff
changeset

692 
(HOL_basic_ss addsimps @{thms "semiring_norm"} 
f2a587696afb
modernized some oldstyle infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45437
diff
changeset

693 
addsimps ths addsimps @{thms simp_thms} 
f2a587696afb
modernized some oldstyle infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45437
diff
changeset

694 
addsimprocs field_cancel_numeral_factors 
f2a587696afb
modernized some oldstyle infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45437
diff
changeset

695 
addsimprocs [add_frac_frac_simproc, add_frac_num_simproc, ord_frac_simproc] 
f2a587696afb
modernized some oldstyle infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45437
diff
changeset

696 
> Simplifier.add_cong @{thm "if_weak_cong"}) 
f2a587696afb
modernized some oldstyle infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45437
diff
changeset

697 
then_conv 
f2a587696afb
modernized some oldstyle infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45437
diff
changeset

698 
Simplifier.rewrite (HOL_basic_ss addsimps 
f2a587696afb
modernized some oldstyle infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45437
diff
changeset

699 
[@{thm numeral_1_eq_1},@{thm numeral_0_eq_0}] @ @{thms numerals(12)}) 
36751
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

700 

7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

701 
end 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36409
diff
changeset

702 

23164  703 
end; 
704 

31068
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

705 
(*examples: 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

706 
print_depth 22; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

707 
set timing; 
40878
7695e4de4d86
renamed trace_simp to simp_trace, and debug_simp to simp_debug;
wenzelm
parents:
38864
diff
changeset

708 
set simp_trace; 
31068
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

709 
fun test s = (Goal s, by (Simp_tac 1)); 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

710 

f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

711 
test "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::int)"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

712 

f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

713 
test "2*u = (u::int)"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

714 
test "(i + j + 12 + (k::int))  15 = y"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

715 
test "(i + j + 12 + (k::int))  5 = y"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

716 

f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

717 
test "y  b < (b::int)"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

718 
test "y  (3*b + c) < (b::int)  2*c"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

719 

f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

720 
test "(2*x  (u*v) + y)  v*3*u = (w::int)"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

721 
test "(2*x*u*v + (u*v)*4 + y)  v*u*4 = (w::int)"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

722 
test "(2*x*u*v + (u*v)*4 + y)  v*u = (w::int)"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

723 
test "u*v  (x*u*v + (u*v)*4 + y) = (w::int)"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

724 

f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

725 
test "(i + j + 12 + (k::int)) = u + 15 + y"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

726 
test "(i + j*2 + 12 + (k::int)) = j + 5 + y"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

727 

f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

728 
test "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)"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

729 

f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

730 
test "a + (b+c) + b = (d::int)"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

731 
test "a + (b+c)  b = (d::int)"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

732 

f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

733 
(*negative numerals*) 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

734 
test "(i + j + 2 + (k::int))  (u + 5 + y) = zz"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

735 
test "(i + j + 3 + (k::int)) < u + 5 + y"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

736 
test "(i + j + 3 + (k::int)) < u + 6 + y"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

737 
test "(i + j + 12 + (k::int))  15 = y"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

738 
test "(i + j + 12 + (k::int))  15 = y"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

739 
test "(i + j + 12 + (k::int))  15 = y"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

740 
*) 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

741 

f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

742 
(*examples: 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

743 
print_depth 22; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

744 
set timing; 
40878
7695e4de4d86
renamed trace_simp to simp_trace, and debug_simp to simp_debug;
wenzelm
parents:
38864
diff
changeset

745 
set simp_trace; 
31068
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

746 
fun test s = (Goal s; by (Simp_tac 1)); 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

747 

f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

748 
test "9*x = 12 * (y::int)"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

749 
test "(9*x) div (12 * (y::int)) = z"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

750 
test "9*x < 12 * (y::int)"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

751 
test "9*x <= 12 * (y::int)"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

752 

f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

753 
test "99*x = 132 * (y::int)"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

754 
test "(99*x) div (132 * (y::int)) = z"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

755 
test "99*x < 132 * (y::int)"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

756 
test "99*x <= 132 * (y::int)"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

757 

f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

758 
test "999*x = 396 * (y::int)"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

759 
test "(999*x) div (396 * (y::int)) = z"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

760 
test "999*x < 396 * (y::int)"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

761 
test "999*x <= 396 * (y::int)"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

762 

f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

763 
test "99*x = 81 * (y::int)"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

764 
test "(99*x) div (81 * (y::int)) = z"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

765 
test "99*x <= 81 * (y::int)"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

766 
test "99*x < 81 * (y::int)"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

767 

f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

768 
test "2 * x = 1 * (y::int)"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

769 
test "2 * x = (y::int)"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

770 
test "(2 * x) div (1 * (y::int)) = z"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

771 
test "2 * x < (y::int)"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

772 
test "2 * x <= 1 * (y::int)"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

773 
test "x < 23 * (y::int)"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

774 
test "x <= 23 * (y::int)"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

775 
*) 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

776 

f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

777 
(*And the same examples for fields such as rat or real: 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

778 
test "0 <= (y::rat) * 2"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

779 
test "9*x = 12 * (y::rat)"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

780 
test "(9*x) / (12 * (y::rat)) = z"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

781 
test "9*x < 12 * (y::rat)"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

782 
test "9*x <= 12 * (y::rat)"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

783 

f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

784 
test "99*x = 132 * (y::rat)"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

785 
test "(99*x) / (132 * (y::rat)) = z"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

786 
test "99*x < 132 * (y::rat)"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

787 
test "99*x <= 132 * (y::rat)"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

788 

f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

789 
test "999*x = 396 * (y::rat)"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

790 
test "(999*x) / (396 * (y::rat)) = z"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

791 
test "999*x < 396 * (y::rat)"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

792 
test "999*x <= 396 * (y::rat)"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

793 

f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

794 
test "( ((2::rat) * x) <= 2 * y)"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

795 
test "99*x = 81 * (y::rat)"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

796 
test "(99*x) / (81 * (y::rat)) = z"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

797 
test "99*x <= 81 * (y::rat)"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

798 
test "99*x < 81 * (y::rat)"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

799 

f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

800 
test "2 * x = 1 * (y::rat)"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

801 
test "2 * x = (y::rat)"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

802 
test "(2 * x) / (1 * (y::rat)) = z"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

803 
test "2 * x < (y::rat)"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

804 
test "2 * x <= 1 * (y::rat)"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

805 
test "x < 23 * (y::rat)"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

806 
test "x <= 23 * (y::rat)"; 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

807 
*) 
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31067
diff
changeset

808 

23164  809 
(*examples: 
810 
print_depth 22; 

811 
set timing; 

40878
7695e4de4d86
renamed trace_simp to simp_trace, and debug_simp to simp_debug;
wenzelm
parents:
38864
diff
changeset

812 
set simp_trace; 
23164  813 
fun test s = (Goal s; by (Asm_simp_tac 1)); 
814 

815 
test "x*k = k*(y::int)"; 

816 
test "k = k*(y::int)"; 

817 
test "a*(b*c) = (b::int)"; 

818 
test "a*(b*c) = d*(b::int)*(x*a)"; 

819 

820 
test "(x*k) div (k*(y::int)) = (uu::int)"; 

821 
test "(k) div (k*(y::int)) = (uu::int)"; 

822 
test "(a*(b*c)) div ((b::int)) = (uu::int)"; 

823 
test "(a*(b*c)) div (d*(b::int)*(x*a)) = (uu::int)"; 

824 
*) 

825 

826 
(*And the same examples for fields such as rat or real: 

827 
print_depth 22; 

828 
set timing; 

40878
7695e4de4d86
renamed trace_simp to simp_trace, and debug_simp to simp_debug;
wenzelm
parents:
38864
diff
changeset

829 
set simp_trace; 
23164  830 
fun test s = (Goal s; by (Asm_simp_tac 1)); 
831 

832 
test "x*k = k*(y::rat)"; 

833 
test "k = k*(y::rat)"; 

834 
test "a*(b*c) = (b::rat)"; 

835 
test "a*(b*c) = d*(b::rat)*(x*a)"; 

836 

837 

838 
test "(x*k) / (k*(y::rat)) = (uu::rat)"; 

839 
test "(k) / (k*(y::rat)) = (uu::rat)"; 

840 
test "(a*(b*c)) / ((b::rat)) = (uu::rat)"; 

841 
test "(a*(b*c)) / (d*(b::rat)*(x*a)) = (uu::rat)"; 

842 

843 
(*FIXME: what do we do about this?*) 

844 
test "a*(b*c)/(y*z) = d*(b::rat)*(x*a)/z"; 

845 
*) 