author  haftmann 
Thu, 06 May 2010 23:11:57 +0200  
changeset 36720  41da7025e59c 
parent 36718  30cdc863a4f8 
child 36731  08cd7eccb043 
child 36751  7f1da69cacb3 
permissions  rwrr 
23252  1 
(* Title: HOL/Tools/Groebner_Basis/normalizer.ML 
2 
Author: Amine Chaieb, TU Muenchen 

36700
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

3 

9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

4 
Normalization of expressions in semirings. 
23252  5 
*) 
6 

7 
signature NORMALIZER = 

8 
sig 

36700
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

9 
type entry 
36703
6e870d7f32e5
removed former algebra presimpset from signature
haftmann
parents:
36702
diff
changeset

10 
val get: Proof.context > (thm * entry) list 
36700
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

11 
val match: Proof.context > cterm > entry option 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

12 
val del: attribute 
36711  13 
val add: {semiring: cterm list * thm list, ring: cterm list * thm list, 
14 
field: cterm list * thm list, idom: thm list, ideal: thm list} > attribute 

36700
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

15 
val funs: thm > {is_const: morphism > cterm > bool, 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

16 
dest_const: morphism > cterm > Rat.rat, 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

17 
mk_const: morphism > ctyp > Rat.rat > cterm, 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

18 
conv: morphism > Proof.context > cterm > thm} > declaration 
36720  19 
val semiring_funs: thm > declaration 
20 
val field_funs: thm > declaration 

36700
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

21 

36711  22 
val semiring_normalize_conv: Proof.context > conv 
23 
val semiring_normalize_ord_conv: Proof.context > (cterm > cterm > bool) > conv 

24 
val semiring_normalize_wrapper: Proof.context > entry > conv 

25 
val semiring_normalize_ord_wrapper: Proof.context > entry 

26 
> (cterm > cterm > bool) > conv 

27 
val semiring_normalizers_conv: cterm list > cterm list * thm list 

28 
> cterm list * thm list > cterm list * thm list > 

36700
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

29 
(cterm > bool) * conv * conv * conv > (cterm > cterm > bool) > 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

30 
{add: conv, mul: conv, neg: conv, main: conv, pow: conv, sub: conv} 
36711  31 
val semiring_normalizers_ord_wrapper: Proof.context > entry > 
32 
(cterm > cterm > bool) > 

27222  33 
{add: conv, mul: conv, neg: conv, main: conv, pow: conv, sub: conv} 
36720  34 
val field_comp_conv: conv 
36700
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

35 

9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

36 
val setup: theory > theory 
23252  37 
end 
38 

39 
structure Normalizer: NORMALIZER = 

40 
struct 

23559  41 

36720  42 
(** some conversion **) 
43 

44 
local 

45 
val zr = @{cpat "0"} 

46 
val zT = ctyp_of_term zr 

47 
val geq = @{cpat "op ="} 

48 
val eqT = Thm.dest_ctyp (ctyp_of_term geq) > hd 

49 
val add_frac_eq = mk_meta_eq @{thm "add_frac_eq"} 

50 
val add_frac_num = mk_meta_eq @{thm "add_frac_num"} 

51 
val add_num_frac = mk_meta_eq @{thm "add_num_frac"} 

52 

53 
fun prove_nz ss T t = 

54 
let 

55 
val z = instantiate_cterm ([(zT,T)],[]) zr 

56 
val eq = instantiate_cterm ([(eqT,T)],[]) geq 

57 
val th = Simplifier.rewrite (ss addsimps @{thms simp_thms}) 

58 
(Thm.capply @{cterm "Trueprop"} (Thm.capply @{cterm "Not"} 

59 
(Thm.capply (Thm.capply eq t) z))) 

60 
in equal_elim (symmetric th) TrueI 

61 
end 

62 

63 
fun proc phi ss ct = 

64 
let 

65 
val ((x,y),(w,z)) = 

66 
(Thm.dest_binop #> (fn (a,b) => (Thm.dest_binop a, Thm.dest_binop b))) ct 

67 
val _ = map (HOLogic.dest_number o term_of) [x,y,z,w] 

68 
val T = ctyp_of_term x 

69 
val [y_nz, z_nz] = map (prove_nz ss T) [y, z] 

70 
val th = instantiate' [SOME T] (map SOME [y,z,x,w]) add_frac_eq 

71 
in SOME (implies_elim (implies_elim th y_nz) z_nz) 

72 
end 

73 
handle CTERM _ => NONE  TERM _ => NONE  THM _ => NONE 

74 

75 
fun proc2 phi ss ct = 

76 
let 

77 
val (l,r) = Thm.dest_binop ct 

78 
val T = ctyp_of_term l 

79 
in (case (term_of l, term_of r) of 

80 
(Const(@{const_name Rings.divide},_)$_$_, _) => 

81 
let val (x,y) = Thm.dest_binop l val z = r 

82 
val _ = map (HOLogic.dest_number o term_of) [x,y,z] 

83 
val ynz = prove_nz ss T y 

84 
in SOME (implies_elim (instantiate' [SOME T] (map SOME [y,x,z]) add_frac_num) ynz) 

85 
end 

86 
 (_, Const (@{const_name Rings.divide},_)$_$_) => 

87 
let val (x,y) = Thm.dest_binop r val z = l 

88 
val _ = map (HOLogic.dest_number o term_of) [x,y,z] 

89 
val ynz = prove_nz ss T y 

90 
in SOME (implies_elim (instantiate' [SOME T] (map SOME [y,z,x]) add_num_frac) ynz) 

91 
end 

92 
 _ => NONE) 

93 
end 

94 
handle CTERM _ => NONE  TERM _ => NONE  THM _ => NONE 

95 

96 
fun is_number (Const(@{const_name Rings.divide},_)$a$b) = is_number a andalso is_number b 

97 
 is_number t = can HOLogic.dest_number t 

98 

99 
val is_number = is_number o term_of 

100 

101 
fun proc3 phi ss ct = 

102 
(case term_of ct of 

103 
Const(@{const_name Orderings.less},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ => 

104 
let 

105 
val ((a,b),c) = Thm.dest_binop ct >> Thm.dest_binop 

106 
val _ = map is_number [a,b,c] 

107 
val T = ctyp_of_term c 

108 
val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_less_eq"} 

109 
in SOME (mk_meta_eq th) end 

110 
 Const(@{const_name Orderings.less_eq},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ => 

111 
let 

112 
val ((a,b),c) = Thm.dest_binop ct >> Thm.dest_binop 

113 
val _ = map is_number [a,b,c] 

114 
val T = ctyp_of_term c 

115 
val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_le_eq"} 

116 
in SOME (mk_meta_eq th) end 

117 
 Const("op =",_)$(Const(@{const_name Rings.divide},_)$_$_)$_ => 

118 
let 

119 
val ((a,b),c) = Thm.dest_binop ct >> Thm.dest_binop 

120 
val _ = map is_number [a,b,c] 

121 
val T = ctyp_of_term c 

122 
val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_eq_eq"} 

123 
in SOME (mk_meta_eq th) end 

124 
 Const(@{const_name Orderings.less},_)$_$(Const(@{const_name Rings.divide},_)$_$_) => 

125 
let 

126 
val (a,(b,c)) = Thm.dest_binop ct > Thm.dest_binop 

127 
val _ = map is_number [a,b,c] 

128 
val T = ctyp_of_term c 

129 
val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "less_divide_eq"} 

130 
in SOME (mk_meta_eq th) end 

131 
 Const(@{const_name Orderings.less_eq},_)$_$(Const(@{const_name Rings.divide},_)$_$_) => 

132 
let 

133 
val (a,(b,c)) = Thm.dest_binop ct > Thm.dest_binop 

134 
val _ = map is_number [a,b,c] 

135 
val T = ctyp_of_term c 

136 
val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "le_divide_eq"} 

137 
in SOME (mk_meta_eq th) end 

138 
 Const("op =",_)$_$(Const(@{const_name Rings.divide},_)$_$_) => 

139 
let 

140 
val (a,(b,c)) = Thm.dest_binop ct > Thm.dest_binop 

141 
val _ = map is_number [a,b,c] 

142 
val T = ctyp_of_term c 

143 
val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "eq_divide_eq"} 

144 
in SOME (mk_meta_eq th) end 

145 
 _ => NONE) 

146 
handle TERM _ => NONE  CTERM _ => NONE  THM _ => NONE 

147 

148 
val add_frac_frac_simproc = 

149 
make_simproc {lhss = [@{cpat "(?x::?'a::field)/?y + (?w::?'a::field)/?z"}], 

150 
name = "add_frac_frac_simproc", 

151 
proc = proc, identifier = []} 

152 

153 
val add_frac_num_simproc = 

154 
make_simproc {lhss = [@{cpat "(?x::?'a::field)/?y + ?z"}, @{cpat "?z + (?x::?'a::field)/?y"}], 

155 
name = "add_frac_num_simproc", 

156 
proc = proc2, identifier = []} 

157 

158 
val ord_frac_simproc = 

159 
make_simproc 

160 
{lhss = [@{cpat "(?a::(?'a::{field, ord}))/?b < ?c"}, 

161 
@{cpat "(?a::(?'a::{field, ord}))/?b <= ?c"}, 

162 
@{cpat "?c < (?a::(?'a::{field, ord}))/?b"}, 

163 
@{cpat "?c <= (?a::(?'a::{field, ord}))/?b"}, 

164 
@{cpat "?c = ((?a::(?'a::{field, ord}))/?b)"}, 

165 
@{cpat "((?a::(?'a::{field, ord}))/ ?b) = ?c"}], 

166 
name = "ord_frac_simproc", proc = proc3, identifier = []} 

167 

168 
val ths = [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"}, 

169 
@{thm "divide_Numeral1"}, 

170 
@{thm "divide_zero"}, @{thm "divide_Numeral0"}, 

171 
@{thm "divide_divide_eq_left"}, 

172 
@{thm "times_divide_eq_left"}, @{thm "times_divide_eq_right"}, 

173 
@{thm "times_divide_times_eq"}, 

174 
@{thm "divide_divide_eq_right"}, 

175 
@{thm "diff_def"}, @{thm "minus_divide_left"}, 

176 
@{thm "Numeral1_eq1_nat"}, @{thm "add_divide_distrib"} RS sym, 

177 
@{thm field_divide_inverse} RS sym, @{thm inverse_divide}, 

178 
Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv (Conv.rewr_conv (mk_meta_eq @{thm mult_commute})))) 

179 
(@{thm field_divide_inverse} RS sym)] 

180 

181 
in 

182 

183 
val field_comp_conv = (Simplifier.rewrite 

184 
(HOL_basic_ss addsimps @{thms "semiring_norm"} 

185 
addsimps ths addsimps @{thms simp_thms} 

186 
addsimprocs Numeral_Simprocs.field_cancel_numeral_factors 

187 
addsimprocs [add_frac_frac_simproc, add_frac_num_simproc, 

188 
ord_frac_simproc] 

189 
addcongs [@{thm "if_weak_cong"}])) 

190 
then_conv (Simplifier.rewrite (HOL_basic_ss addsimps 

191 
[@{thm numeral_1_eq_1},@{thm numeral_0_eq_0}] @ @{thms numerals(12)})) 

192 

193 
end 

194 

195 

36708  196 
(** data **) 
36700
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

197 

9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

198 
type entry = 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

199 
{vars: cterm list, 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

200 
semiring: cterm list * thm list, 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

201 
ring: cterm list * thm list, 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

202 
field: cterm list * thm list, 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

203 
idom: thm list, 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

204 
ideal: thm list} * 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

205 
{is_const: cterm > bool, 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

206 
dest_const: cterm > Rat.rat, 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

207 
mk_const: ctyp > Rat.rat > cterm, 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

208 
conv: Proof.context > cterm > thm}; 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

209 

9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

210 
structure Data = Generic_Data 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

211 
( 
36705  212 
type T = (thm * entry) list; 
213 
val empty = []; 

36700
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

214 
val extend = I; 
36718  215 
val merge = AList.merge Thm.eq_thm (K true); 
36700
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

216 
); 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

217 

36705  218 
val get = Data.get o Context.Proof; 
36700
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

219 

9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

220 
fun match ctxt tm = 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

221 
let 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

222 
fun match_inst 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

223 
({vars, semiring = (sr_ops, sr_rules), 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

224 
ring = (r_ops, r_rules), field = (f_ops, f_rules), idom, ideal}, 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

225 
fns as {is_const, dest_const, mk_const, conv}) pat = 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

226 
let 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

227 
fun h instT = 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

228 
let 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

229 
val substT = Thm.instantiate (instT, []); 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

230 
val substT_cterm = Drule.cterm_rule substT; 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

231 

9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

232 
val vars' = map substT_cterm vars; 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

233 
val semiring' = (map substT_cterm sr_ops, map substT sr_rules); 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

234 
val ring' = (map substT_cterm r_ops, map substT r_rules); 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

235 
val field' = (map substT_cterm f_ops, map substT f_rules); 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

236 
val idom' = map substT idom; 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

237 
val ideal' = map substT ideal; 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

238 

9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

239 
val result = ({vars = vars', semiring = semiring', 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

240 
ring = ring', field = field', idom = idom', ideal = ideal'}, fns); 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

241 
in SOME result end 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

242 
in (case try Thm.match (pat, tm) of 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

243 
NONE => NONE 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

244 
 SOME (instT, _) => h instT) 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

245 
end; 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

246 

9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

247 
fun match_struct (_, 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

248 
entry as ({semiring = (sr_ops, _), ring = (r_ops, _), field = (f_ops, _), ...}, _): entry) = 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

249 
get_first (match_inst entry) (sr_ops @ r_ops @ f_ops); 
36704  250 
in get_first match_struct (get ctxt) end; 
36700
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

251 

9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

252 

9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

253 
(* logical content *) 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

254 

9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

255 
val semiringN = "semiring"; 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

256 
val ringN = "ring"; 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

257 
val idomN = "idom"; 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

258 
val idealN = "ideal"; 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

259 
val fieldN = "field"; 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

260 

9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

261 
fun undefined _ = raise Match; 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

262 

36706  263 
val del = Thm.declaration_attribute (Data.map o AList.delete Thm.eq_thm); 
36700
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

264 

9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

265 
fun add {semiring = (sr_ops, sr_rules), ring = (r_ops, r_rules), 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

266 
field = (f_ops, f_rules), idom, ideal} = 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

267 
Thm.declaration_attribute (fn key => fn context => context > Data.map 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

268 
let 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

269 
val ctxt = Context.proof_of context; 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

270 

9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

271 
fun check kind name xs n = 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

272 
null xs orelse length xs = n orelse 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

273 
error ("Expected " ^ string_of_int n ^ " " ^ kind ^ " for " ^ name); 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

274 
val check_ops = check "operations"; 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

275 
val check_rules = check "rules"; 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

276 

9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

277 
val _ = 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

278 
check_ops semiringN sr_ops 5 andalso 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

279 
check_rules semiringN sr_rules 37 andalso 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

280 
check_ops ringN r_ops 2 andalso 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

281 
check_rules ringN r_rules 2 andalso 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

282 
check_ops fieldN f_ops 2 andalso 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

283 
check_rules fieldN f_rules 2 andalso 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

284 
check_rules idomN idom 2; 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

285 

9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

286 
val mk_meta = Local_Defs.meta_rewrite_rule ctxt; 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

287 
val sr_rules' = map mk_meta sr_rules; 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

288 
val r_rules' = map mk_meta r_rules; 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

289 
val f_rules' = map mk_meta f_rules; 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

290 

9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

291 
fun rule i = nth sr_rules' (i  1); 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

292 

9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

293 
val (cx, cy) = Thm.dest_binop (hd sr_ops); 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

294 
val cz = rule 34 > Thm.rhs_of > Thm.dest_arg > Thm.dest_arg; 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

295 
val cn = rule 36 > Thm.rhs_of > Thm.dest_arg > Thm.dest_arg; 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

296 
val ((clx, crx), (cly, cry)) = 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

297 
rule 13 > Thm.rhs_of > Thm.dest_binop > pairself Thm.dest_binop; 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

298 
val ((ca, cb), (cc, cd)) = 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

299 
rule 20 > Thm.lhs_of > Thm.dest_binop > pairself Thm.dest_binop; 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

300 
val cm = rule 1 > Thm.rhs_of > Thm.dest_arg; 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

301 
val (cp, cq) = rule 26 > Thm.lhs_of > Thm.dest_binop > pairself Thm.dest_arg; 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

302 

9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

303 
val vars = [ca, cb, cc, cd, cm, cn, cp, cq, cx, cy, cz, clx, crx, cly, cry]; 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

304 
val semiring = (sr_ops, sr_rules'); 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

305 
val ring = (r_ops, r_rules'); 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

306 
val field = (f_ops, f_rules'); 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

307 
val ideal' = map (symmetric o mk_meta) ideal 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

308 
in 
36706  309 
AList.delete Thm.eq_thm key #> 
36705  310 
cons (key, ({vars = vars, semiring = semiring, 
36700
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

311 
ring = ring, field = field, idom = idom, ideal = ideal'}, 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

312 
{is_const = undefined, dest_const = undefined, mk_const = undefined, 
36705  313 
conv = undefined})) 
36700
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

314 
end); 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

315 

9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

316 

9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

317 
(* extralogical functions *) 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

318 

9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

319 
fun funs raw_key {is_const, dest_const, mk_const, conv} phi = 
36705  320 
Data.map (fn data => 
36700
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

321 
let 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

322 
val key = Morphism.thm phi raw_key; 
36706  323 
val _ = AList.defined Thm.eq_thm data key orelse 
36700
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

324 
raise THM ("No data entry for structure key", 0, [key]); 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

325 
val fns = {is_const = is_const phi, dest_const = dest_const phi, 
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

326 
mk_const = mk_const phi, conv = conv phi}; 
36706  327 
in AList.map_entry Thm.eq_thm key (apsnd (K fns)) data end); 
36700
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

328 

36720  329 
fun semiring_funs key = funs key 
330 
{is_const = fn phi => can HOLogic.dest_number o Thm.term_of, 

331 
dest_const = fn phi => fn ct => 

332 
Rat.rat_of_int (snd 

333 
(HOLogic.dest_number (Thm.term_of ct) 

334 
handle TERM _ => error "ring_dest_const")), 

335 
mk_const = fn phi => fn cT => fn x => Numeral.mk_cnumber cT 

336 
(case Rat.quotient_of_rat x of (i, 1) => i  _ => error "int_of_rat: bad int"), 

337 
conv = fn phi => fn _ => Simplifier.rewrite (HOL_basic_ss addsimps @{thms semiring_norm}) 

338 
then_conv Simplifier.rewrite (HOL_basic_ss addsimps 

339 
(@{thms numeral_1_eq_1} @ @{thms numeral_0_eq_0} @ @{thms numerals(12)}))}; 

340 

341 
fun field_funs key = 

342 
let 

343 
fun numeral_is_const ct = 

344 
case term_of ct of 

345 
Const (@{const_name Rings.divide},_) $ a $ b => 

346 
can HOLogic.dest_number a andalso can HOLogic.dest_number b 

347 
 Const (@{const_name Rings.inverse},_)$t => can HOLogic.dest_number t 

348 
 t => can HOLogic.dest_number t 

349 
fun dest_const ct = ((case term_of ct of 

350 
Const (@{const_name Rings.divide},_) $ a $ b=> 

351 
Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b)) 

352 
 Const (@{const_name Rings.inverse},_)$t => 

353 
Rat.inv (Rat.rat_of_int (snd (HOLogic.dest_number t))) 

354 
 t => Rat.rat_of_int (snd (HOLogic.dest_number t))) 

355 
handle TERM _ => error "ring_dest_const") 

356 
fun mk_const phi cT x = 

357 
let val (a, b) = Rat.quotient_of_rat x 

358 
in if b = 1 then Numeral.mk_cnumber cT a 

359 
else Thm.capply 

360 
(Thm.capply (Drule.cterm_rule (instantiate' [SOME cT] []) @{cpat "op /"}) 

361 
(Numeral.mk_cnumber cT a)) 

362 
(Numeral.mk_cnumber cT b) 

363 
end 

364 
in funs key 

365 
{is_const = K numeral_is_const, 

366 
dest_const = K dest_const, 

367 
mk_const = mk_const, 

368 
conv = K (K field_comp_conv)} 

369 
end; 

370 

371 

36700
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

372 

36710  373 
(** auxiliary **) 
25253  374 

375 
fun is_comb ct = 

376 
(case Thm.term_of ct of 

377 
_ $ _ => true 

378 
 _ => false); 

379 

380 
val concl = Thm.cprop_of #> Thm.dest_arg; 

381 

382 
fun is_binop ct ct' = 

383 
(case Thm.term_of ct' of 

384 
c $ _ $ _ => term_of ct aconv c 

385 
 _ => false); 

386 

387 
fun dest_binop ct ct' = 

388 
if is_binop ct ct' then Thm.dest_binop ct' 

389 
else raise CTERM ("dest_binop: bad binop", [ct, ct']) 

390 

391 
fun inst_thm inst = Thm.instantiate ([], inst); 

392 

23252  393 
val dest_numeral = term_of #> HOLogic.dest_number #> snd; 
394 
val is_numeral = can dest_numeral; 

395 

396 
val numeral01_conv = Simplifier.rewrite 

25481  397 
(HOL_basic_ss addsimps [@{thm numeral_1_eq_1}, @{thm numeral_0_eq_0}]); 
23252  398 
val zero1_numeral_conv = 
25481  399 
Simplifier.rewrite (HOL_basic_ss addsimps [@{thm numeral_1_eq_1} RS sym, @{thm numeral_0_eq_0} RS sym]); 
23580
998a6fda9bb6
moved mk_cnumeral/mk_cnumber to Tools/numeral.ML;
wenzelm
parents:
23559
diff
changeset

400 
fun zerone_conv cv = zero1_numeral_conv then_conv cv then_conv numeral01_conv; 
23252  401 
val natarith = [@{thm "add_nat_number_of"}, @{thm "diff_nat_number_of"}, 
402 
@{thm "mult_nat_number_of"}, @{thm "eq_nat_number_of"}, 

403 
@{thm "less_nat_number_of"}]; 

36700
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

404 

23252  405 
val nat_add_conv = 
406 
zerone_conv 

407 
(Simplifier.rewrite 

408 
(HOL_basic_ss 

25481  409 
addsimps @{thms arith_simps} @ natarith @ @{thms rel_simps} 
35410  410 
@ [@{thm if_False}, @{thm if_True}, @{thm Nat.add_0}, @{thm add_Suc}, 
31790  411 
@{thm add_number_of_left}, @{thm Suc_eq_plus1}] 
25481  412 
@ map (fn th => th RS sym) @{thms numerals})); 
23252  413 

414 
val zeron_tm = @{cterm "0::nat"}; 

415 
val onen_tm = @{cterm "1::nat"}; 

416 
val true_tm = @{cterm "True"}; 

417 

418 

36710  419 
(** normalizing conversions **) 
420 

421 
(* core conversion *) 

422 

30866  423 
fun semiring_normalizers_conv vars (sr_ops, sr_rules) (r_ops, r_rules) (f_ops, f_rules) 
23252  424 
(is_semiring_constant, semiring_add_conv, semiring_mul_conv, semiring_pow_conv) = 
425 
let 

426 

427 
val [pthm_02, pthm_03, pthm_04, pthm_05, pthm_07, pthm_08, 

428 
pthm_09, pthm_10, pthm_11, pthm_12, pthm_13, pthm_14, pthm_15, pthm_16, 

429 
pthm_17, pthm_18, pthm_19, pthm_21, pthm_22, pthm_23, pthm_24, 

430 
pthm_25, pthm_26, pthm_27, pthm_28, pthm_29, pthm_30, pthm_31, pthm_32, 

431 
pthm_33, pthm_34, pthm_35, pthm_36, pthm_37, pthm_38,pthm_39,pthm_40] = sr_rules; 

432 

433 
val [ca, cb, cc, cd, cm, cn, cp, cq, cx, cy, cz, clx, crx, cly, cry] = vars; 

434 
val [add_pat, mul_pat, pow_pat, zero_tm, one_tm] = sr_ops; 

435 
val [add_tm, mul_tm, pow_tm] = map (Thm.dest_fun o Thm.dest_fun) [add_pat, mul_pat, pow_pat]; 

436 

437 
val dest_add = dest_binop add_tm 

438 
val dest_mul = dest_binop mul_tm 

439 
fun dest_pow tm = 

440 
let val (l,r) = dest_binop pow_tm tm 

441 
in if is_numeral r then (l,r) else raise CTERM ("dest_pow",[tm]) 

442 
end; 

443 
val is_add = is_binop add_tm 

444 
val is_mul = is_binop mul_tm 

445 
fun is_pow tm = is_binop pow_tm tm andalso is_numeral(Thm.dest_arg tm); 

446 

447 
val (neg_mul,sub_add,sub_tm,neg_tm,dest_sub,is_sub,cx',cy') = 

448 
(case (r_ops, r_rules) of 

30866  449 
([sub_pat, neg_pat], [neg_mul, sub_add]) => 
23252  450 
let 
451 
val sub_tm = Thm.dest_fun (Thm.dest_fun sub_pat) 

452 
val neg_tm = Thm.dest_fun neg_pat 

453 
val dest_sub = dest_binop sub_tm 

454 
val is_sub = is_binop sub_tm 

455 
in (neg_mul,sub_add,sub_tm,neg_tm,dest_sub,is_sub, neg_mul > concl > Thm.dest_arg, 

456 
sub_add > concl > Thm.dest_arg > Thm.dest_arg) 

30866  457 
end 
458 
 _ => (TrueI, TrueI, true_tm, true_tm, (fn t => (t,t)), K false, true_tm, true_tm)); 

459 

460 
val (divide_inverse, inverse_divide, divide_tm, inverse_tm, is_divide) = 

461 
(case (f_ops, f_rules) of 

462 
([divide_pat, inverse_pat], [div_inv, inv_div]) => 

463 
let val div_tm = funpow 2 Thm.dest_fun divide_pat 

464 
val inv_tm = Thm.dest_fun inverse_pat 

465 
in (div_inv, inv_div, div_tm, inv_tm, is_binop div_tm) 

466 
end 

467 
 _ => (TrueI, TrueI, true_tm, true_tm, K false)); 

468 

23252  469 
in fn variable_order => 
470 
let 

471 

472 
(* Conversion for "x^n * x^m", with either x^n = x and/or x^m = x possible. *) 

473 
(* Also deals with "const * const", but both terms must involve powers of *) 

474 
(* the same variable, or both be constants, or behaviour may be incorrect. *) 

475 

476 
fun powvar_mul_conv tm = 

477 
let 

478 
val (l,r) = dest_mul tm 

479 
in if is_semiring_constant l andalso is_semiring_constant r 

480 
then semiring_mul_conv tm 

481 
else 

482 
((let 

483 
val (lx,ln) = dest_pow l 

484 
in 

485 
((let val (rx,rn) = dest_pow r 

486 
val th1 = inst_thm [(cx,lx),(cp,ln),(cq,rn)] pthm_29 

487 
val (tm1,tm2) = Thm.dest_comb(concl th1) in 

488 
transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end) 

489 
handle CTERM _ => 

490 
(let val th1 = inst_thm [(cx,lx),(cq,ln)] pthm_31 

491 
val (tm1,tm2) = Thm.dest_comb(concl th1) in 

492 
transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end)) end) 

493 
handle CTERM _ => 

494 
((let val (rx,rn) = dest_pow r 

495 
val th1 = inst_thm [(cx,rx),(cq,rn)] pthm_30 

496 
val (tm1,tm2) = Thm.dest_comb(concl th1) in 

497 
transitive th1 (Drule.arg_cong_rule tm1 (nat_add_conv tm2)) end) 

498 
handle CTERM _ => inst_thm [(cx,l)] pthm_32 

499 

500 
)) 

501 
end; 

502 

503 
(* Remove "1 * m" from a monomial, and just leave m. *) 

504 

505 
fun monomial_deone th = 

506 
(let val (l,r) = dest_mul(concl th) in 

507 
if l aconvc one_tm 

508 
then transitive th (inst_thm [(ca,r)] pthm_13) else th end) 

509 
handle CTERM _ => th; 

510 

511 
(* Conversion for "(monomial)^n", where n is a numeral. *) 

512 

513 
val monomial_pow_conv = 

514 
let 

515 
fun monomial_pow tm bod ntm = 

516 
if not(is_comb bod) 

517 
then reflexive tm 

518 
else 

519 
if is_semiring_constant bod 

520 
then semiring_pow_conv tm 

521 
else 

522 
let 

523 
val (lopr,r) = Thm.dest_comb bod 

524 
in if not(is_comb lopr) 

525 
then reflexive tm 

526 
else 

527 
let 

528 
val (opr,l) = Thm.dest_comb lopr 

529 
in 

530 
if opr aconvc pow_tm andalso is_numeral r 

531 
then 

532 
let val th1 = inst_thm [(cx,l),(cp,r),(cq,ntm)] pthm_34 

533 
val (l,r) = Thm.dest_comb(concl th1) 

36700
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

534 
in transitive th1 (Drule.arg_cong_rule l (nat_add_conv r)) 
23252  535 
end 
536 
else 

537 
if opr aconvc mul_tm 

538 
then 

539 
let 

540 
val th1 = inst_thm [(cx,l),(cy,r),(cq,ntm)] pthm_33 

541 
val (xy,z) = Thm.dest_comb(concl th1) 

542 
val (x,y) = Thm.dest_comb xy 

543 
val thl = monomial_pow y l ntm 

544 
val thr = monomial_pow z r ntm 

545 
in transitive th1 (combination (Drule.arg_cong_rule x thl) thr) 

546 
end 

547 
else reflexive tm 

548 
end 

549 
end 

550 
in fn tm => 

551 
let 

552 
val (lopr,r) = Thm.dest_comb tm 

553 
val (opr,l) = Thm.dest_comb lopr 

554 
in if not (opr aconvc pow_tm) orelse not(is_numeral r) 

555 
then raise CTERM ("monomial_pow_conv", [tm]) 

556 
else if r aconvc zeron_tm 

557 
then inst_thm [(cx,l)] pthm_35 

558 
else if r aconvc onen_tm 

559 
then inst_thm [(cx,l)] pthm_36 

560 
else monomial_deone(monomial_pow tm l r) 

561 
end 

562 
end; 

563 

564 
(* Multiplication of canonical monomials. *) 

565 
val monomial_mul_conv = 

566 
let 

567 
fun powvar tm = 

568 
if is_semiring_constant tm then one_tm 

569 
else 

570 
((let val (lopr,r) = Thm.dest_comb tm 

571 
val (opr,l) = Thm.dest_comb lopr 

572 
in if opr aconvc pow_tm andalso is_numeral r then l 

573 
else raise CTERM ("monomial_mul_conv",[tm]) end) 

574 
handle CTERM _ => tm) (* FIXME !? *) 

575 
fun vorder x y = 

576 
if x aconvc y then 0 

577 
else 

578 
if x aconvc one_tm then ~1 

579 
else if y aconvc one_tm then 1 

580 
else if variable_order x y then ~1 else 1 

581 
fun monomial_mul tm l r = 

582 
((let val (lx,ly) = dest_mul l val vl = powvar lx 

583 
in 

584 
((let 

585 
val (rx,ry) = dest_mul r 

586 
val vr = powvar rx 

587 
val ord = vorder vl vr 

588 
in 

589 
if ord = 0 

590 
then 

591 
let 

592 
val th1 = inst_thm [(clx,lx),(cly,ly),(crx,rx),(cry,ry)] pthm_15 

593 
val (tm1,tm2) = Thm.dest_comb(concl th1) 

594 
val (tm3,tm4) = Thm.dest_comb tm1 

595 
val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2 

596 
val th3 = transitive th1 th2 

597 
val (tm5,tm6) = Thm.dest_comb(concl th3) 

598 
val (tm7,tm8) = Thm.dest_comb tm6 

599 
val th4 = monomial_mul tm6 (Thm.dest_arg tm7) tm8 

600 
in transitive th3 (Drule.arg_cong_rule tm5 th4) 

601 
end 

602 
else 

603 
let val th0 = if ord < 0 then pthm_16 else pthm_17 

604 
val th1 = inst_thm [(clx,lx),(cly,ly),(crx,rx),(cry,ry)] th0 

605 
val (tm1,tm2) = Thm.dest_comb(concl th1) 

606 
val (tm3,tm4) = Thm.dest_comb tm2 

607 
in transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4)) 

608 
end 

609 
end) 

610 
handle CTERM _ => 

611 
(let val vr = powvar r val ord = vorder vl vr 

612 
in 

613 
if ord = 0 then 

614 
let 

615 
val th1 = inst_thm [(clx,lx),(cly,ly),(crx,r)] pthm_18 

616 
val (tm1,tm2) = Thm.dest_comb(concl th1) 

617 
val (tm3,tm4) = Thm.dest_comb tm1 

618 
val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2 

619 
in transitive th1 th2 

620 
end 

621 
else 

622 
if ord < 0 then 

623 
let val th1 = inst_thm [(clx,lx),(cly,ly),(crx,r)] pthm_19 

624 
val (tm1,tm2) = Thm.dest_comb(concl th1) 

625 
val (tm3,tm4) = Thm.dest_comb tm2 

626 
in transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4)) 

627 
end 

628 
else inst_thm [(ca,l),(cb,r)] pthm_09 

629 
end)) end) 

630 
handle CTERM _ => 

631 
(let val vl = powvar l in 

632 
((let 

633 
val (rx,ry) = dest_mul r 

634 
val vr = powvar rx 

635 
val ord = vorder vl vr 

636 
in if ord = 0 then 

637 
let val th1 = inst_thm [(clx,l),(crx,rx),(cry,ry)] pthm_21 

638 
val (tm1,tm2) = Thm.dest_comb(concl th1) 

639 
val (tm3,tm4) = Thm.dest_comb tm1 

640 
in transitive th1 (Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (powvar_mul_conv tm4)) tm2) 

641 
end 

642 
else if ord > 0 then 

643 
let val th1 = inst_thm [(clx,l),(crx,rx),(cry,ry)] pthm_22 

644 
val (tm1,tm2) = Thm.dest_comb(concl th1) 

645 
val (tm3,tm4) = Thm.dest_comb tm2 

646 
in transitive th1 (Drule.arg_cong_rule tm1 (monomial_mul tm2 (Thm.dest_arg tm3) tm4)) 

647 
end 

648 
else reflexive tm 

649 
end) 

650 
handle CTERM _ => 

651 
(let val vr = powvar r 

652 
val ord = vorder vl vr 

653 
in if ord = 0 then powvar_mul_conv tm 

654 
else if ord > 0 then inst_thm [(ca,l),(cb,r)] pthm_09 

655 
else reflexive tm 

656 
end)) end)) 

657 
in fn tm => let val (l,r) = dest_mul tm in monomial_deone(monomial_mul tm l r) 

658 
end 

659 
end; 

660 
(* Multiplication by monomial of a polynomial. *) 

661 

662 
val polynomial_monomial_mul_conv = 

663 
let 

664 
fun pmm_conv tm = 

665 
let val (l,r) = dest_mul tm 

666 
in 

667 
((let val (y,z) = dest_add r 

668 
val th1 = inst_thm [(cx,l),(cy,y),(cz,z)] pthm_37 

669 
val (tm1,tm2) = Thm.dest_comb(concl th1) 

670 
val (tm3,tm4) = Thm.dest_comb tm1 

671 
val th2 = combination (Drule.arg_cong_rule tm3 (monomial_mul_conv tm4)) (pmm_conv tm2) 

672 
in transitive th1 th2 

673 
end) 

674 
handle CTERM _ => monomial_mul_conv tm) 

675 
end 

676 
in pmm_conv 

677 
end; 

678 

679 
(* Addition of two monomials identical except for constant multiples. *) 

680 

681 
fun monomial_add_conv tm = 

682 
let val (l,r) = dest_add tm 

683 
in if is_semiring_constant l andalso is_semiring_constant r 

684 
then semiring_add_conv tm 

685 
else 

686 
let val th1 = 

687 
if is_mul l andalso is_semiring_constant(Thm.dest_arg1 l) 

688 
then if is_mul r andalso is_semiring_constant(Thm.dest_arg1 r) then 

689 
inst_thm [(ca,Thm.dest_arg1 l),(cm,Thm.dest_arg r), (cb,Thm.dest_arg1 r)] pthm_02 

690 
else inst_thm [(ca,Thm.dest_arg1 l),(cm,r)] pthm_03 

691 
else if is_mul r andalso is_semiring_constant(Thm.dest_arg1 r) 

692 
then inst_thm [(cm,l),(ca,Thm.dest_arg1 r)] pthm_04 

693 
else inst_thm [(cm,r)] pthm_05 

694 
val (tm1,tm2) = Thm.dest_comb(concl th1) 

695 
val (tm3,tm4) = Thm.dest_comb tm1 

696 
val th2 = Drule.arg_cong_rule tm3 (semiring_add_conv tm4) 

697 
val th3 = transitive th1 (Drule.fun_cong_rule th2 tm2) 

698 
val tm5 = concl th3 

699 
in 

700 
if (Thm.dest_arg1 tm5) aconvc zero_tm 

701 
then transitive th3 (inst_thm [(ca,Thm.dest_arg tm5)] pthm_11) 

702 
else monomial_deone th3 

703 
end 

704 
end; 

705 

706 
(* Ordering on monomials. *) 

707 

708 
fun striplist dest = 

709 
let fun strip x acc = 

710 
((let val (l,r) = dest x in 

711 
strip l (strip r acc) end) 

712 
handle CTERM _ => x::acc) (* FIXME !? *) 

713 
in fn x => strip x [] 

714 
end; 

715 

716 

717 
fun powervars tm = 

718 
let val ptms = striplist dest_mul tm 

719 
in if is_semiring_constant (hd ptms) then tl ptms else ptms 

720 
end; 

721 
val num_0 = 0; 

722 
val num_1 = 1; 

723 
fun dest_varpow tm = 

724 
((let val (x,n) = dest_pow tm in (x,dest_numeral n) end) 

725 
handle CTERM _ => 

726 
(tm,(if is_semiring_constant tm then num_0 else num_1))); 

727 

728 
val morder = 

729 
let fun lexorder l1 l2 = 

730 
case (l1,l2) of 

731 
([],[]) => 0 

732 
 (vps,[]) => ~1 

733 
 ([],vps) => 1 

734 
 (((x1,n1)::vs1),((x2,n2)::vs2)) => 

735 
if variable_order x1 x2 then 1 

736 
else if variable_order x2 x1 then ~1 

737 
else if n1 < n2 then ~1 

738 
else if n2 < n1 then 1 

739 
else lexorder vs1 vs2 

740 
in fn tm1 => fn tm2 => 

741 
let val vdegs1 = map dest_varpow (powervars tm1) 

742 
val vdegs2 = map dest_varpow (powervars tm2) 

33002  743 
val deg1 = fold (Integer.add o snd) vdegs1 num_0 
744 
val deg2 = fold (Integer.add o snd) vdegs2 num_0 

23252  745 
in if deg1 < deg2 then ~1 else if deg1 > deg2 then 1 
746 
else lexorder vdegs1 vdegs2 

747 
end 

748 
end; 

749 

750 
(* Addition of two polynomials. *) 

751 

752 
val polynomial_add_conv = 

753 
let 

754 
fun dezero_rule th = 

755 
let 

756 
val tm = concl th 

757 
in 

758 
if not(is_add tm) then th else 

759 
let val (lopr,r) = Thm.dest_comb tm 

760 
val l = Thm.dest_arg lopr 

761 
in 

762 
if l aconvc zero_tm 

763 
then transitive th (inst_thm [(ca,r)] pthm_07) else 

764 
if r aconvc zero_tm 

765 
then transitive th (inst_thm [(ca,l)] pthm_08) else th 

766 
end 

767 
end 

768 
fun padd tm = 

769 
let 

770 
val (l,r) = dest_add tm 

771 
in 

772 
if l aconvc zero_tm then inst_thm [(ca,r)] pthm_07 

773 
else if r aconvc zero_tm then inst_thm [(ca,l)] pthm_08 

774 
else 

775 
if is_add l 

776 
then 

777 
let val (a,b) = dest_add l 

778 
in 

779 
if is_add r then 

780 
let val (c,d) = dest_add r 

781 
val ord = morder a c 

782 
in 

783 
if ord = 0 then 

784 
let val th1 = inst_thm [(ca,a),(cb,b),(cc,c),(cd,d)] pthm_23 

785 
val (tm1,tm2) = Thm.dest_comb(concl th1) 

786 
val (tm3,tm4) = Thm.dest_comb tm1 

787 
val th2 = Drule.arg_cong_rule tm3 (monomial_add_conv tm4) 

788 
in dezero_rule (transitive th1 (combination th2 (padd tm2))) 

789 
end 

790 
else (* ord <> 0*) 

791 
let val th1 = 

792 
if ord > 0 then inst_thm [(ca,a),(cb,b),(cc,r)] pthm_24 

793 
else inst_thm [(ca,l),(cc,c),(cd,d)] pthm_25 

794 
val (tm1,tm2) = Thm.dest_comb(concl th1) 

795 
in dezero_rule (transitive th1 (Drule.arg_cong_rule tm1 (padd tm2))) 

796 
end 

797 
end 

798 
else (* not (is_add r)*) 

799 
let val ord = morder a r 

800 
in 

801 
if ord = 0 then 

802 
let val th1 = inst_thm [(ca,a),(cb,b),(cc,r)] pthm_26 

803 
val (tm1,tm2) = Thm.dest_comb(concl th1) 

804 
val (tm3,tm4) = Thm.dest_comb tm1 

805 
val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (monomial_add_conv tm4)) tm2 

806 
in dezero_rule (transitive th1 th2) 

807 
end 

808 
else (* ord <> 0*) 

809 
if ord > 0 then 

810 
let val th1 = inst_thm [(ca,a),(cb,b),(cc,r)] pthm_24 

811 
val (tm1,tm2) = Thm.dest_comb(concl th1) 

812 
in dezero_rule (transitive th1 (Drule.arg_cong_rule tm1 (padd tm2))) 

813 
end 

814 
else dezero_rule (inst_thm [(ca,l),(cc,r)] pthm_27) 

815 
end 

816 
end 

817 
else (* not (is_add l)*) 

818 
if is_add r then 

819 
let val (c,d) = dest_add r 

820 
val ord = morder l c 

821 
in 

822 
if ord = 0 then 

823 
let val th1 = inst_thm [(ca,l),(cc,c),(cd,d)] pthm_28 

824 
val (tm1,tm2) = Thm.dest_comb(concl th1) 

825 
val (tm3,tm4) = Thm.dest_comb tm1 

826 
val th2 = Drule.fun_cong_rule (Drule.arg_cong_rule tm3 (monomial_add_conv tm4)) tm2 

827 
in dezero_rule (transitive th1 th2) 

828 
end 

829 
else 

830 
if ord > 0 then reflexive tm 

831 
else 

832 
let val th1 = inst_thm [(ca,l),(cc,c),(cd,d)] pthm_25 

833 
val (tm1,tm2) = Thm.dest_comb(concl th1) 

834 
in dezero_rule (transitive th1 (Drule.arg_cong_rule tm1 (padd tm2))) 

835 
end 

836 
end 

837 
else 

838 
let val ord = morder l r 

839 
in 

840 
if ord = 0 then monomial_add_conv tm 

841 
else if ord > 0 then dezero_rule(reflexive tm) 

842 
else dezero_rule (inst_thm [(ca,l),(cc,r)] pthm_27) 

843 
end 

844 
end 

845 
in padd 

846 
end; 

847 

848 
(* Multiplication of two polynomials. *) 

849 

850 
val polynomial_mul_conv = 

851 
let 

852 
fun pmul tm = 

853 
let val (l,r) = dest_mul tm 

854 
in 

855 
if not(is_add l) then polynomial_monomial_mul_conv tm 

856 
else 

857 
if not(is_add r) then 

858 
let val th1 = inst_thm [(ca,l),(cb,r)] pthm_09 

859 
in transitive th1 (polynomial_monomial_mul_conv(concl th1)) 

860 
end 

861 
else 

862 
let val (a,b) = dest_add l 

863 
val th1 = inst_thm [(ca,a),(cb,b),(cc,r)] pthm_10 

864 
val (tm1,tm2) = Thm.dest_comb(concl th1) 

865 
val (tm3,tm4) = Thm.dest_comb tm1 

866 
val th2 = Drule.arg_cong_rule tm3 (polynomial_monomial_mul_conv tm4) 

867 
val th3 = transitive th1 (combination th2 (pmul tm2)) 

868 
in transitive th3 (polynomial_add_conv (concl th3)) 

869 
end 

870 
end 

871 
in fn tm => 

872 
let val (l,r) = dest_mul tm 

873 
in 

874 
if l aconvc zero_tm then inst_thm [(ca,r)] pthm_11 

875 
else if r aconvc zero_tm then inst_thm [(ca,l)] pthm_12 

876 
else if l aconvc one_tm then inst_thm [(ca,r)] pthm_13 

877 
else if r aconvc one_tm then inst_thm [(ca,l)] pthm_14 

878 
else pmul tm 

879 
end 

880 
end; 

881 

882 
(* Power of polynomial (optimized for the monomial and trivial cases). *) 

883 

23580
998a6fda9bb6
moved mk_cnumeral/mk_cnumber to Tools/numeral.ML;
wenzelm
parents:
23559
diff
changeset

884 
fun num_conv n = 
998a6fda9bb6
moved mk_cnumeral/mk_cnumber to Tools/numeral.ML;
wenzelm
parents:
23559
diff
changeset

885 
nat_add_conv (Thm.capply @{cterm Suc} (Numeral.mk_cnumber @{ctyp nat} (dest_numeral n  1))) 
998a6fda9bb6
moved mk_cnumeral/mk_cnumber to Tools/numeral.ML;
wenzelm
parents:
23559
diff
changeset

886 
> Thm.symmetric; 
23252  887 

888 

889 
val polynomial_pow_conv = 

890 
let 

891 
fun ppow tm = 

892 
let val (l,n) = dest_pow tm 

893 
in 

894 
if n aconvc zeron_tm then inst_thm [(cx,l)] pthm_35 

895 
else if n aconvc onen_tm then inst_thm [(cx,l)] pthm_36 

896 
else 

897 
let val th1 = num_conv n 

898 
val th2 = inst_thm [(cx,l),(cq,Thm.dest_arg (concl th1))] pthm_38 

899 
val (tm1,tm2) = Thm.dest_comb(concl th2) 

900 
val th3 = transitive th2 (Drule.arg_cong_rule tm1 (ppow tm2)) 

901 
val th4 = transitive (Drule.arg_cong_rule (Thm.dest_fun tm) th1) th3 

902 
in transitive th4 (polynomial_mul_conv (concl th4)) 

903 
end 

904 
end 

905 
in fn tm => 

906 
if is_add(Thm.dest_arg1 tm) then ppow tm else monomial_pow_conv tm 

907 
end; 

908 

909 
(* Negation. *) 

910 

23580
998a6fda9bb6
moved mk_cnumeral/mk_cnumber to Tools/numeral.ML;
wenzelm
parents:
23559
diff
changeset

911 
fun polynomial_neg_conv tm = 
23252  912 
let val (l,r) = Thm.dest_comb tm in 
913 
if not (l aconvc neg_tm) then raise CTERM ("polynomial_neg_conv",[tm]) else 

914 
let val th1 = inst_thm [(cx',r)] neg_mul 

36709  915 
val th2 = transitive th1 (Conv.arg1_conv semiring_mul_conv (concl th1)) 
23252  916 
in transitive th2 (polynomial_monomial_mul_conv (concl th2)) 
917 
end 

918 
end; 

919 

920 

921 
(* Subtraction. *) 

23580
998a6fda9bb6
moved mk_cnumeral/mk_cnumber to Tools/numeral.ML;
wenzelm
parents:
23559
diff
changeset

922 
fun polynomial_sub_conv tm = 
23252  923 
let val (l,r) = dest_sub tm 
924 
val th1 = inst_thm [(cx',l),(cy',r)] sub_add 

925 
val (tm1,tm2) = Thm.dest_comb(concl th1) 

926 
val th2 = Drule.arg_cong_rule tm1 (polynomial_neg_conv tm2) 

927 
in transitive th1 (transitive th2 (polynomial_add_conv (concl th2))) 

928 
end; 

929 

930 
(* Conversion from HOL term. *) 

931 

932 
fun polynomial_conv tm = 

23407
0e4452fcbeb8
normalizer conversions depend on the proof context; added functions for conversion and wrapper that sill depend on the variable ordering (_ord)
chaieb
parents:
23330
diff
changeset

933 
if is_semiring_constant tm then semiring_add_conv tm 
0e4452fcbeb8
normalizer conversions depend on the proof context; added functions for conversion and wrapper that sill depend on the variable ordering (_ord)
chaieb
parents:
23330
diff
changeset

934 
else if not(is_comb tm) then reflexive tm 
23252  935 
else 
936 
let val (lopr,r) = Thm.dest_comb tm 

937 
in if lopr aconvc neg_tm then 

938 
let val th1 = Drule.arg_cong_rule lopr (polynomial_conv r) 

939 
in transitive th1 (polynomial_neg_conv (concl th1)) 

940 
end 

30866  941 
else if lopr aconvc inverse_tm then 
942 
let val th1 = Drule.arg_cong_rule lopr (polynomial_conv r) 

943 
in transitive th1 (semiring_mul_conv (concl th1)) 

944 
end 

23252  945 
else 
946 
if not(is_comb lopr) then reflexive tm 

947 
else 

948 
let val (opr,l) = Thm.dest_comb lopr 

949 
in if opr aconvc pow_tm andalso is_numeral r 

950 
then 

951 
let val th1 = Drule.fun_cong_rule (Drule.arg_cong_rule opr (polynomial_conv l)) r 

952 
in transitive th1 (polynomial_pow_conv (concl th1)) 

953 
end 

30866  954 
else if opr aconvc divide_tm 
955 
then 

956 
let val th1 = combination (Drule.arg_cong_rule opr (polynomial_conv l)) 

957 
(polynomial_conv r) 

36709  958 
val th2 = (Conv.rewr_conv divide_inverse then_conv polynomial_mul_conv) 
30866  959 
(Thm.rhs_of th1) 
960 
in transitive th1 th2 

961 
end 

23252  962 
else 
963 
if opr aconvc add_tm orelse opr aconvc mul_tm orelse opr aconvc sub_tm 

964 
then 

965 
let val th1 = combination (Drule.arg_cong_rule opr (polynomial_conv l)) (polynomial_conv r) 

966 
val f = if opr aconvc add_tm then polynomial_add_conv 

967 
else if opr aconvc mul_tm then polynomial_mul_conv 

968 
else polynomial_sub_conv 

969 
in transitive th1 (f (concl th1)) 

970 
end 

971 
else reflexive tm 

972 
end 

973 
end; 

974 
in 

975 
{main = polynomial_conv, 

976 
add = polynomial_add_conv, 

977 
mul = polynomial_mul_conv, 

978 
pow = polynomial_pow_conv, 

979 
neg = polynomial_neg_conv, 

980 
sub = polynomial_sub_conv} 

981 
end 

982 
end; 

983 

35410  984 
val nat_exp_ss = 
985 
HOL_basic_ss addsimps (@{thms nat_number} @ @{thms nat_arith} @ @{thms arith_simps} @ @{thms rel_simps}) 

986 
addsimps [@{thm Let_def}, @{thm if_False}, @{thm if_True}, @{thm Nat.add_0}, @{thm add_Suc}]; 

23252  987 

35408  988 
fun simple_cterm_ord t u = Term_Ord.term_ord (term_of t, term_of u) = LESS; 
27222  989 

36710  990 

991 
(* various normalizing conversions *) 

992 

30866  993 
fun semiring_normalizers_ord_wrapper ctxt ({vars, semiring, ring, field, idom, ideal}, 
23407
0e4452fcbeb8
normalizer conversions depend on the proof context; added functions for conversion and wrapper that sill depend on the variable ordering (_ord)
chaieb
parents:
23330
diff
changeset

994 
{conv, dest_const, mk_const, is_const}) ord = 
23252  995 
let 
996 
val pow_conv = 

36709  997 
Conv.arg_conv (Simplifier.rewrite nat_exp_ss) 
23252  998 
then_conv Simplifier.rewrite 
999 
(HOL_basic_ss addsimps [nth (snd semiring) 31, nth (snd semiring) 34]) 

23330
01c09922ce59
Conversion for computation on constants now depends on the context
chaieb
parents:
23259
diff
changeset

1000 
then_conv conv ctxt 
01c09922ce59
Conversion for computation on constants now depends on the context
chaieb
parents:
23259
diff
changeset

1001 
val dat = (is_const, conv ctxt, conv ctxt, pow_conv) 
30866  1002 
in semiring_normalizers_conv vars semiring ring field dat ord end; 
27222  1003 

30866  1004 
fun semiring_normalize_ord_wrapper ctxt ({vars, semiring, ring, field, idom, ideal}, {conv, dest_const, mk_const, is_const}) ord = 
1005 
#main (semiring_normalizers_ord_wrapper ctxt ({vars = vars, semiring = semiring, ring = ring, field = field, idom = idom, ideal = ideal},{conv = conv, dest_const = dest_const, mk_const = mk_const, is_const = is_const}) ord); 

23252  1006 

23407
0e4452fcbeb8
normalizer conversions depend on the proof context; added functions for conversion and wrapper that sill depend on the variable ordering (_ord)
chaieb
parents:
23330
diff
changeset

1007 
fun semiring_normalize_wrapper ctxt data = 
0e4452fcbeb8
normalizer conversions depend on the proof context; added functions for conversion and wrapper that sill depend on the variable ordering (_ord)
chaieb
parents:
23330
diff
changeset

1008 
semiring_normalize_ord_wrapper ctxt data simple_cterm_ord; 
0e4452fcbeb8
normalizer conversions depend on the proof context; added functions for conversion and wrapper that sill depend on the variable ordering (_ord)
chaieb
parents:
23330
diff
changeset

1009 

0e4452fcbeb8
normalizer conversions depend on the proof context; added functions for conversion and wrapper that sill depend on the variable ordering (_ord)
chaieb
parents:
23330
diff
changeset

1010 
fun semiring_normalize_ord_conv ctxt ord tm = 
36700
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

1011 
(case match ctxt tm of 
23252  1012 
NONE => reflexive tm 
23407
0e4452fcbeb8
normalizer conversions depend on the proof context; added functions for conversion and wrapper that sill depend on the variable ordering (_ord)
chaieb
parents:
23330
diff
changeset

1013 
 SOME res => semiring_normalize_ord_wrapper ctxt res ord tm); 
0e4452fcbeb8
normalizer conversions depend on the proof context; added functions for conversion and wrapper that sill depend on the variable ordering (_ord)
chaieb
parents:
23330
diff
changeset

1014 

0e4452fcbeb8
normalizer conversions depend on the proof context; added functions for conversion and wrapper that sill depend on the variable ordering (_ord)
chaieb
parents:
23330
diff
changeset

1015 
fun semiring_normalize_conv ctxt = semiring_normalize_ord_conv ctxt simple_cterm_ord; 
23252  1016 

36708  1017 

1018 
(** Isar setup **) 

1019 

1020 
local 

1021 

1022 
fun keyword k = Scan.lift (Args.$$$ k  Args.colon) >> K (); 

1023 
fun keyword2 k1 k2 = Scan.lift (Args.$$$ k1  Args.$$$ k2  Args.colon) >> K (); 

1024 
fun keyword3 k1 k2 k3 = 

1025 
Scan.lift (Args.$$$ k1  Args.$$$ k2  Args.$$$ k3  Args.colon) >> K (); 

1026 

1027 
val opsN = "ops"; 

1028 
val rulesN = "rules"; 

1029 

1030 
val normN = "norm"; 

1031 
val constN = "const"; 

1032 
val delN = "del"; 

36700
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

1033 

36708  1034 
val any_keyword = 
1035 
keyword2 semiringN opsN  keyword2 semiringN rulesN  

1036 
keyword2 ringN opsN  keyword2 ringN rulesN  

1037 
keyword2 fieldN opsN  keyword2 fieldN rulesN  

1038 
keyword2 idomN rulesN  keyword2 idealN rulesN; 

1039 

1040 
val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat; 

1041 
val terms = thms >> map Drule.dest_term; 

1042 

1043 
fun optional scan = Scan.optional scan []; 

1044 

1045 
in 

1046 

1047 
val setup = 

1048 
Attrib.setup @{binding normalizer} 

1049 
(Scan.lift (Args.$$$ delN >> K del)  

1050 
((keyword2 semiringN opsN  terms)  

1051 
(keyword2 semiringN rulesN  thms))  

1052 
(optional (keyword2 ringN opsN  terms)  

1053 
optional (keyword2 ringN rulesN  thms))  

1054 
(optional (keyword2 fieldN opsN  terms)  

1055 
optional (keyword2 fieldN rulesN  thms))  

1056 
optional (keyword2 idomN rulesN  thms)  

1057 
optional (keyword2 idealN rulesN  thms) 

1058 
>> (fn ((((sr, r), f), id), idl) => 

1059 
add {semiring = sr, ring = r, field = f, idom = id, ideal = idl})) 

1060 
"semiring normalizer data"; 

36700
9b85b9d74b83
dropped auxiliary method sring_norm; integrated normalizer.ML and normalizer_data.ML
haftmann
parents:
35410
diff
changeset

1061 

23252  1062 
end; 
36708  1063 

1064 
end; 