author  chaieb 
Sun, 22 Jul 2007 17:53:42 +0200  
changeset 23901  7392193f9ecf 
parent 23881  851c74f1bb69 
child 24075  366d4d234814 
permissions  rwrr 
23462  1 
(* Title: HOL/Arith_Tools.thy 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Author: Amine Chaieb, TU Muenchen 

5 
*) 

6 

7 
header {* Setup of arithmetic tools *} 

8 

9 
theory Arith_Tools 

23465  10 
imports Groebner_Basis Dense_Linear_Order 
23462  11 
uses 
12 
"~~/src/Provers/Arith/cancel_numeral_factor.ML" 

13 
"~~/src/Provers/Arith/extract_common_term.ML" 

14 
"int_factor_simprocs.ML" 

15 
"nat_simprocs.ML" 

16 
begin 

17 

18 
subsection {* Simprocs for the Naturals *} 

19 

20 
setup nat_simprocs_setup 

21 

22 
subsubsection{*For simplifying @{term "Suc m  K"} and @{term "K  Suc m"}*} 

23 

24 
text{*Where K above is a literal*} 

25 

26 
lemma Suc_diff_eq_diff_pred: "Numeral0 < n ==> Suc m  n = m  (n  Numeral1)" 

27 
by (simp add: numeral_0_eq_0 numeral_1_eq_1 split add: nat_diff_split) 

28 

29 
text {*Now just instantiating @{text n} to @{text "number_of v"} does 

30 
the right simplification, but with some redundant inequality 

31 
tests.*} 

32 
lemma neg_number_of_pred_iff_0: 

33 
"neg (number_of (Numeral.pred v)::int) = (number_of v = (0::nat))" 

34 
apply (subgoal_tac "neg (number_of (Numeral.pred v)) = (number_of v < Suc 0) ") 

35 
apply (simp only: less_Suc_eq_le le_0_eq) 

36 
apply (subst less_number_of_Suc, simp) 

37 
done 

38 

39 
text{*No longer required as a simprule because of the @{text inverse_fold} 

40 
simproc*} 

41 
lemma Suc_diff_number_of: 

42 
"neg (number_of (uminus v)::int) ==> 

43 
Suc m  (number_of v) = m  (number_of (Numeral.pred v))" 

44 
apply (subst Suc_diff_eq_diff_pred) 

45 
apply simp 

46 
apply (simp del: nat_numeral_1_eq_1) 

47 
apply (auto simp only: diff_nat_number_of less_0_number_of [symmetric] 

48 
neg_number_of_pred_iff_0) 

49 
done 

50 

51 
lemma diff_Suc_eq_diff_pred: "m  Suc n = (m  1)  n" 

52 
by (simp add: numerals split add: nat_diff_split) 

53 

54 

55 
subsubsection{*For @{term nat_case} and @{term nat_rec}*} 

56 

57 
lemma nat_case_number_of [simp]: 

58 
"nat_case a f (number_of v) = 

59 
(let pv = number_of (Numeral.pred v) in 

60 
if neg pv then a else f (nat pv))" 

61 
by (simp split add: nat.split add: Let_def neg_number_of_pred_iff_0) 

62 

63 
lemma nat_case_add_eq_if [simp]: 

64 
"nat_case a f ((number_of v) + n) = 

65 
(let pv = number_of (Numeral.pred v) in 

66 
if neg pv then nat_case a f n else f (nat pv + n))" 

67 
apply (subst add_eq_if) 

68 
apply (simp split add: nat.split 

69 
del: nat_numeral_1_eq_1 

70 
add: numeral_1_eq_Suc_0 [symmetric] Let_def 

71 
neg_imp_number_of_eq_0 neg_number_of_pred_iff_0) 

72 
done 

73 

74 
lemma nat_rec_number_of [simp]: 

75 
"nat_rec a f (number_of v) = 

76 
(let pv = number_of (Numeral.pred v) in 

77 
if neg pv then a else f (nat pv) (nat_rec a f (nat pv)))" 

78 
apply (case_tac " (number_of v) ::nat") 

79 
apply (simp_all (no_asm_simp) add: Let_def neg_number_of_pred_iff_0) 

80 
apply (simp split add: split_if_asm) 

81 
done 

82 

83 
lemma nat_rec_add_eq_if [simp]: 

84 
"nat_rec a f (number_of v + n) = 

85 
(let pv = number_of (Numeral.pred v) in 

86 
if neg pv then nat_rec a f n 

87 
else f (nat pv + n) (nat_rec a f (nat pv + n)))" 

88 
apply (subst add_eq_if) 

89 
apply (simp split add: nat.split 

90 
del: nat_numeral_1_eq_1 

91 
add: numeral_1_eq_Suc_0 [symmetric] Let_def neg_imp_number_of_eq_0 

92 
neg_number_of_pred_iff_0) 

93 
done 

94 

95 

96 
subsubsection{*Various Other Lemmas*} 

97 

98 
text {*Evens and Odds, for Mutilated Chess Board*} 

99 

100 
text{*Lemmas for specialist use, NOT as default simprules*} 

101 
lemma nat_mult_2: "2 * z = (z+z::nat)" 

102 
proof  

103 
have "2*z = (1 + 1)*z" by simp 

104 
also have "... = z+z" by (simp add: left_distrib) 

105 
finally show ?thesis . 

106 
qed 

107 

108 
lemma nat_mult_2_right: "z * 2 = (z+z::nat)" 

109 
by (subst mult_commute, rule nat_mult_2) 

110 

111 
text{*Case analysis on @{term "n<2"}*} 

112 
lemma less_2_cases: "(n::nat) < 2 ==> n = 0  n = Suc 0" 

113 
by arith 

114 

115 
lemma div2_Suc_Suc [simp]: "Suc(Suc m) div 2 = Suc (m div 2)" 

116 
by arith 

117 

118 
lemma add_self_div_2 [simp]: "(m + m) div 2 = (m::nat)" 

119 
by (simp add: nat_mult_2 [symmetric]) 

120 

121 
lemma mod2_Suc_Suc [simp]: "Suc(Suc(m)) mod 2 = m mod 2" 

122 
apply (subgoal_tac "m mod 2 < 2") 

123 
apply (erule less_2_cases [THEN disjE]) 

124 
apply (simp_all (no_asm_simp) add: Let_def mod_Suc nat_1) 

125 
done 

126 

127 
lemma mod2_gr_0 [simp]: "!!m::nat. (0 < m mod 2) = (m mod 2 = 1)" 

128 
apply (subgoal_tac "m mod 2 < 2") 

129 
apply (force simp del: mod_less_divisor, simp) 

130 
done 

131 

132 
text{*Removal of Small Numerals: 0, 1 and (in additive positions) 2*} 

133 

134 
lemma add_2_eq_Suc [simp]: "2 + n = Suc (Suc n)" 

135 
by simp 

136 

137 
lemma add_2_eq_Suc' [simp]: "n + 2 = Suc (Suc n)" 

138 
by simp 

139 

140 
text{*Can be used to eliminate long strings of Sucs, but not by default*} 

141 
lemma Suc3_eq_add_3: "Suc (Suc (Suc n)) = 3 + n" 

142 
by simp 

143 

144 

145 
text{*These lemmas collapse some needless occurrences of Suc: 

146 
at least three Sucs, since two and fewer are rewritten back to Suc again! 

147 
We already have some rules to simplify operands smaller than 3.*} 

148 

149 
lemma div_Suc_eq_div_add3 [simp]: "m div (Suc (Suc (Suc n))) = m div (3+n)" 

150 
by (simp add: Suc3_eq_add_3) 

151 

152 
lemma mod_Suc_eq_mod_add3 [simp]: "m mod (Suc (Suc (Suc n))) = m mod (3+n)" 

153 
by (simp add: Suc3_eq_add_3) 

154 

155 
lemma Suc_div_eq_add3_div: "(Suc (Suc (Suc m))) div n = (3+m) div n" 

156 
by (simp add: Suc3_eq_add_3) 

157 

158 
lemma Suc_mod_eq_add3_mod: "(Suc (Suc (Suc m))) mod n = (3+m) mod n" 

159 
by (simp add: Suc3_eq_add_3) 

160 

161 
lemmas Suc_div_eq_add3_div_number_of = 

162 
Suc_div_eq_add3_div [of _ "number_of v", standard] 

163 
declare Suc_div_eq_add3_div_number_of [simp] 

164 

165 
lemmas Suc_mod_eq_add3_mod_number_of = 

166 
Suc_mod_eq_add3_mod [of _ "number_of v", standard] 

167 
declare Suc_mod_eq_add3_mod_number_of [simp] 

168 

169 

170 
subsubsection{*Special Simplification for Constants*} 

171 

172 
text{*These belong here, late in the development of HOL, to prevent their 

173 
interfering with proofs of abstract properties of instances of the function 

174 
@{term number_of}*} 

175 

176 
text{*These distributive laws move literals inside sums and differences.*} 

177 
lemmas left_distrib_number_of = left_distrib [of _ _ "number_of v", standard] 

178 
declare left_distrib_number_of [simp] 

179 

180 
lemmas right_distrib_number_of = right_distrib [of "number_of v", standard] 

181 
declare right_distrib_number_of [simp] 

182 

183 

184 
lemmas left_diff_distrib_number_of = 

185 
left_diff_distrib [of _ _ "number_of v", standard] 

186 
declare left_diff_distrib_number_of [simp] 

187 

188 
lemmas right_diff_distrib_number_of = 

189 
right_diff_distrib [of "number_of v", standard] 

190 
declare right_diff_distrib_number_of [simp] 

191 

192 

193 
text{*These are actually for fields, like real: but where else to put them?*} 

194 
lemmas zero_less_divide_iff_number_of = 

195 
zero_less_divide_iff [of "number_of w", standard] 

196 
declare zero_less_divide_iff_number_of [simp] 

197 

198 
lemmas divide_less_0_iff_number_of = 

199 
divide_less_0_iff [of "number_of w", standard] 

200 
declare divide_less_0_iff_number_of [simp] 

201 

202 
lemmas zero_le_divide_iff_number_of = 

203 
zero_le_divide_iff [of "number_of w", standard] 

204 
declare zero_le_divide_iff_number_of [simp] 

205 

206 
lemmas divide_le_0_iff_number_of = 

207 
divide_le_0_iff [of "number_of w", standard] 

208 
declare divide_le_0_iff_number_of [simp] 

209 

210 

211 
(**** 

212 
IF times_divide_eq_right and times_divide_eq_left are removed as simprules, 

213 
then these specialcase declarations may be useful. 

214 

215 
text{*These simprules move numerals into numerators and denominators.*} 

216 
lemma times_recip_eq_right [simp]: "a * (1/c) = a / (c::'a::field)" 

217 
by (simp add: times_divide_eq) 

218 

219 
lemma times_recip_eq_left [simp]: "(1/c) * a = a / (c::'a::field)" 

220 
by (simp add: times_divide_eq) 

221 

222 
lemmas times_divide_eq_right_number_of = 

223 
times_divide_eq_right [of "number_of w", standard] 

224 
declare times_divide_eq_right_number_of [simp] 

225 

226 
lemmas times_divide_eq_right_number_of = 

227 
times_divide_eq_right [of _ _ "number_of w", standard] 

228 
declare times_divide_eq_right_number_of [simp] 

229 

230 
lemmas times_divide_eq_left_number_of = 

231 
times_divide_eq_left [of _ "number_of w", standard] 

232 
declare times_divide_eq_left_number_of [simp] 

233 

234 
lemmas times_divide_eq_left_number_of = 

235 
times_divide_eq_left [of _ _ "number_of w", standard] 

236 
declare times_divide_eq_left_number_of [simp] 

237 

238 
****) 

239 

240 
text {*Replaces @{text "inverse #nn"} by @{text "1/#nn"}. It looks 

241 
strange, but then other simprocs simplify the quotient.*} 

242 

243 
lemmas inverse_eq_divide_number_of = 

244 
inverse_eq_divide [of "number_of w", standard] 

245 
declare inverse_eq_divide_number_of [simp] 

246 

247 

248 
text {*These laws simplify inequalities, moving unary minus from a term 

249 
into the literal.*} 

250 
lemmas less_minus_iff_number_of = 

251 
less_minus_iff [of "number_of v", standard] 

252 
declare less_minus_iff_number_of [simp] 

253 

254 
lemmas le_minus_iff_number_of = 

255 
le_minus_iff [of "number_of v", standard] 

256 
declare le_minus_iff_number_of [simp] 

257 

258 
lemmas equation_minus_iff_number_of = 

259 
equation_minus_iff [of "number_of v", standard] 

260 
declare equation_minus_iff_number_of [simp] 

261 

262 

263 
lemmas minus_less_iff_number_of = 

264 
minus_less_iff [of _ "number_of v", standard] 

265 
declare minus_less_iff_number_of [simp] 

266 

267 
lemmas minus_le_iff_number_of = 

268 
minus_le_iff [of _ "number_of v", standard] 

269 
declare minus_le_iff_number_of [simp] 

270 

271 
lemmas minus_equation_iff_number_of = 

272 
minus_equation_iff [of _ "number_of v", standard] 

273 
declare minus_equation_iff_number_of [simp] 

274 

275 

276 
text{*To Simplify Inequalities Where One Side is the Constant 1*} 

277 

278 
lemma less_minus_iff_1 [simp]: 

279 
fixes b::"'b::{ordered_idom,number_ring}" 

280 
shows "(1 <  b) = (b < 1)" 

281 
by auto 

282 

283 
lemma le_minus_iff_1 [simp]: 

284 
fixes b::"'b::{ordered_idom,number_ring}" 

285 
shows "(1 \<le>  b) = (b \<le> 1)" 

286 
by auto 

287 

288 
lemma equation_minus_iff_1 [simp]: 

289 
fixes b::"'b::number_ring" 

290 
shows "(1 =  b) = (b = 1)" 

291 
by (subst equation_minus_iff, auto) 

292 

293 
lemma minus_less_iff_1 [simp]: 

294 
fixes a::"'b::{ordered_idom,number_ring}" 

295 
shows "( a < 1) = (1 < a)" 

296 
by auto 

297 

298 
lemma minus_le_iff_1 [simp]: 

299 
fixes a::"'b::{ordered_idom,number_ring}" 

300 
shows "( a \<le> 1) = (1 \<le> a)" 

301 
by auto 

302 

303 
lemma minus_equation_iff_1 [simp]: 

304 
fixes a::"'b::number_ring" 

305 
shows "( a = 1) = (a = 1)" 

306 
by (subst minus_equation_iff, auto) 

307 

308 

309 
text {*Cancellation of constant factors in comparisons (@{text "<"} and @{text "\<le>"}) *} 

310 

311 
lemmas mult_less_cancel_left_number_of = 

312 
mult_less_cancel_left [of "number_of v", standard] 

313 
declare mult_less_cancel_left_number_of [simp] 

314 

315 
lemmas mult_less_cancel_right_number_of = 

316 
mult_less_cancel_right [of _ "number_of v", standard] 

317 
declare mult_less_cancel_right_number_of [simp] 

318 

319 
lemmas mult_le_cancel_left_number_of = 

320 
mult_le_cancel_left [of "number_of v", standard] 

321 
declare mult_le_cancel_left_number_of [simp] 

322 

323 
lemmas mult_le_cancel_right_number_of = 

324 
mult_le_cancel_right [of _ "number_of v", standard] 

325 
declare mult_le_cancel_right_number_of [simp] 

326 

327 

328 
text {*Multiplying out constant divisors in comparisons (@{text "<"}, @{text "\<le>"} and @{text "="}) *} 

329 

330 
lemmas le_divide_eq_number_of = le_divide_eq [of _ _ "number_of w", standard] 

331 
declare le_divide_eq_number_of [simp] 

332 

333 
lemmas divide_le_eq_number_of = divide_le_eq [of _ "number_of w", standard] 

334 
declare divide_le_eq_number_of [simp] 

335 

336 
lemmas less_divide_eq_number_of = less_divide_eq [of _ _ "number_of w", standard] 

337 
declare less_divide_eq_number_of [simp] 

338 

339 
lemmas divide_less_eq_number_of = divide_less_eq [of _ "number_of w", standard] 

340 
declare divide_less_eq_number_of [simp] 

341 

342 
lemmas eq_divide_eq_number_of = eq_divide_eq [of _ _ "number_of w", standard] 

343 
declare eq_divide_eq_number_of [simp] 

344 

345 
lemmas divide_eq_eq_number_of = divide_eq_eq [of _ "number_of w", standard] 

346 
declare divide_eq_eq_number_of [simp] 

347 

348 

349 

350 
subsubsection{*Optional Simplification Rules Involving Constants*} 

351 

352 
text{*Simplify quotients that are compared with a literal constant.*} 

353 

354 
lemmas le_divide_eq_number_of = le_divide_eq [of "number_of w", standard] 

355 
lemmas divide_le_eq_number_of = divide_le_eq [of _ _ "number_of w", standard] 

356 
lemmas less_divide_eq_number_of = less_divide_eq [of "number_of w", standard] 

357 
lemmas divide_less_eq_number_of = divide_less_eq [of _ _ "number_of w", standard] 

358 
lemmas eq_divide_eq_number_of = eq_divide_eq [of "number_of w", standard] 

359 
lemmas divide_eq_eq_number_of = divide_eq_eq [of _ _ "number_of w", standard] 

360 

361 

362 
text{*Not good as automatic simprules because they cause case splits.*} 

363 
lemmas divide_const_simps = 

364 
le_divide_eq_number_of divide_le_eq_number_of less_divide_eq_number_of 

365 
divide_less_eq_number_of eq_divide_eq_number_of divide_eq_eq_number_of 

366 
le_divide_eq_1 divide_le_eq_1 less_divide_eq_1 divide_less_eq_1 

367 

368 
text{*Division By @{text "1"}*} 

369 

370 
lemma divide_minus1 [simp]: 

371 
"x/1 = (x::'a::{field,division_by_zero,number_ring})" 

372 
by simp 

373 

374 
lemma minus1_divide [simp]: 

375 
"1 / (x::'a::{field,division_by_zero,number_ring}) =  (1/x)" 

376 
by (simp add: divide_inverse inverse_minus_eq) 

377 

378 
lemma half_gt_zero_iff: 

379 
"(0 < r/2) = (0 < (r::'a::{ordered_field,division_by_zero,number_ring}))" 

380 
by auto 

381 

382 
lemmas half_gt_zero = half_gt_zero_iff [THEN iffD2, standard] 

383 
declare half_gt_zero [simp] 

384 

385 
(* The following lemma should appear in Divides.thy, but there the proof 

386 
doesn't work. *) 

387 

388 
lemma nat_dvd_not_less: 

389 
"[ 0 < m; m < n ] ==> \<not> n dvd (m::nat)" 

390 
by (unfold dvd_def) auto 

391 

392 
ML {* 

393 
val divide_minus1 = @{thm divide_minus1}; 

394 
val minus1_divide = @{thm minus1_divide}; 

395 
*} 

396 

397 

398 
subsection{* Groebner Bases for fields *} 

399 

400 
interpretation class_fieldgb: 

401 
fieldgb["op +" "op *" "op ^" "0::'a::{field,recpower,number_ring}" "1" "op " "uminus" "op /" "inverse"] apply (unfold_locales) by (simp_all add: divide_inverse) 

402 

403 
lemma divide_Numeral1: "(x::'a::{field,number_ring}) / Numeral1 = x" by simp 

404 
lemma divide_Numeral0: "(x::'a::{field,number_ring, division_by_zero}) / Numeral0 = 0" 

405 
by simp 

406 
lemma mult_frac_frac: "((x::'a::{field,division_by_zero}) / y) * (z / w) = (x*z) / (y*w)" 

407 
by simp 

408 
lemma mult_frac_num: "((x::'a::{field, division_by_zero}) / y) * z = (x*z) / y" 

409 
by simp 

410 
lemma mult_num_frac: "((x::'a::{field, division_by_zero}) / y) * z = (x*z) / y" 

411 
by simp 

412 

413 
lemma Numeral1_eq1_nat: "(1::nat) = Numeral1" by simp 

414 

415 
lemma add_frac_num: "y\<noteq> 0 \<Longrightarrow> (x::'a::{field, division_by_zero}) / y + z = (x + z*y) / y" 

416 
by (simp add: add_divide_distrib) 

417 
lemma add_num_frac: "y\<noteq> 0 \<Longrightarrow> z + (x::'a::{field, division_by_zero}) / y = (x + z*y) / y" 

418 
by (simp add: add_divide_distrib) 

419 

420 
declaration{* 

421 
let 

422 
val zr = @{cpat "0"} 

423 
val zT = ctyp_of_term zr 

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

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

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

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

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

429 

430 
fun prove_nz ctxt = 

431 
let val ss = local_simpset_of ctxt 

432 
in fn T => fn t => 

433 
let 

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

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

436 
val th = Simplifier.rewrite (ss addsimps simp_thms) 

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

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

439 
in equal_elim (symmetric th) TrueI 

440 
end 

441 
end 

442 

443 
fun proc ctxt phi ss ct = 

444 
let 

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

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

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

448 
val T = ctyp_of_term x 

449 
val [y_nz, z_nz] = map (prove_nz ctxt T) [y, z] 

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

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

452 
end 

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

454 

455 
fun proc2 ctxt phi ss ct = 

456 
let 

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

458 
val T = ctyp_of_term l 

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

460 
(Const(@{const_name "HOL.divide"},_)$_$_, _) => 

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

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

463 
val ynz = prove_nz ctxt T y 

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

465 
end 

466 
 (_, Const (@{const_name "HOL.divide"},_)$_$_) => 

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

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

469 
val ynz = prove_nz ctxt T y 

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

471 
end 

472 
 _ => NONE) 

473 
end 

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

475 

476 
fun is_number (Const(@{const_name "HOL.divide"},_)$a$b) = is_number a andalso is_number b 

477 
 is_number t = can HOLogic.dest_number t 

478 

479 
val is_number = is_number o term_of 

480 

481 
fun proc3 phi ss ct = 

482 
(case term_of ct of 

23881  483 
Const(@{const_name HOL.less},_)$(Const(@{const_name "HOL.divide"},_)$_$_)$_ => 
23462  484 
let 
485 
val ((a,b),c) = Thm.dest_binop ct >> Thm.dest_binop 

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

487 
val T = ctyp_of_term c 

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

489 
in SOME (mk_meta_eq th) end 

23881  490 
 Const(@{const_name HOL.less_eq},_)$(Const(@{const_name "HOL.divide"},_)$_$_)$_ => 
23462  491 
let 
492 
val ((a,b),c) = Thm.dest_binop ct >> Thm.dest_binop 

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

494 
val T = ctyp_of_term c 

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

496 
in SOME (mk_meta_eq th) end 

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

498 
let 

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

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

501 
val T = ctyp_of_term c 

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

503 
in SOME (mk_meta_eq th) end 

23881  504 
 Const(@{const_name HOL.less},_)$_$(Const(@{const_name "HOL.divide"},_)$_$_) => 
23462  505 
let 
506 
val (a,(b,c)) = Thm.dest_binop ct > Thm.dest_binop 

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

508 
val T = ctyp_of_term c 

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

510 
in SOME (mk_meta_eq th) end 

23881  511 
 Const(@{const_name HOL.less_eq},_)$_$(Const(@{const_name "HOL.divide"},_)$_$_) => 
23462  512 
let 
513 
val (a,(b,c)) = Thm.dest_binop ct > Thm.dest_binop 

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

515 
val T = ctyp_of_term c 

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

517 
in SOME (mk_meta_eq th) end 

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

519 
let 

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

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

522 
val T = ctyp_of_term c 

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

524 
in SOME (mk_meta_eq th) end 

525 
 _ => NONE) 

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

527 

528 
fun add_frac_frac_simproc ctxt = 

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

530 
name = "add_frac_frac_simproc", 

531 
proc = proc ctxt, identifier = []} 

532 

533 
fun add_frac_num_simproc ctxt = 

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

535 
name = "add_frac_num_simproc", 

536 
proc = proc2 ctxt, identifier = []} 

537 

538 
val ord_frac_simproc = 

539 
make_simproc 

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

541 
@{cpat "(?a::(?'a::{field, ord}))/?b \<le> ?c"}, 

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

543 
@{cpat "?c \<le> (?a::(?'a::{field, ord}))/?b"}, 

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

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

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

547 

548 
val nat_arith = map thm ["add_nat_number_of", "diff_nat_number_of", 

549 
"mult_nat_number_of", "eq_nat_number_of", "less_nat_number_of"] 

550 

551 
val comp_arith = (map thm ["Let_def", "if_False", "if_True", "add_0", 

552 
"add_Suc", "add_number_of_left", "mult_number_of_left", 

553 
"Suc_eq_add_numeral_1"])@ 

554 
(map (fn s => thm s RS sym) ["numeral_1_eq_1", "numeral_0_eq_0"]) 

555 
@ arith_simps@ nat_arith @ rel_simps 

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

557 
@{thm "divide_Numeral1"}, 

558 
@{thm "Ring_and_Field.divide_zero"}, @{thm "divide_Numeral0"}, 

559 
@{thm "divide_divide_eq_left"}, @{thm "mult_frac_frac"}, 

560 
@{thm "mult_num_frac"}, @{thm "mult_frac_num"}, 

561 
@{thm "mult_frac_frac"}, @{thm "times_divide_eq_right"}, 

562 
@{thm "times_divide_eq_left"}, @{thm "divide_divide_eq_right"}, 

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

564 
@{thm "Numeral1_eq1_nat"}, @{thm "add_divide_distrib"} RS sym] 

565 

566 
local 

567 
open Conv 

568 
in 

569 
fun comp_conv ctxt = (Simplifier.rewrite 

570 
(HOL_basic_ss addsimps @{thms "Groebner_Basis.comp_arith"} 

571 
addsimps ths addsimps comp_arith addsimps simp_thms 

572 
addsimprocs field_cancel_numeral_factors 

573 
addsimprocs [add_frac_frac_simproc ctxt, add_frac_num_simproc ctxt, 

574 
ord_frac_simproc] 

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

576 
then_conv (Simplifier.rewrite (HOL_basic_ss addsimps 

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

578 
end 

579 

580 
fun numeral_is_const ct = 

581 
case term_of ct of 

582 
Const (@{const_name "HOL.divide"},_) $ a $ b => 

583 
numeral_is_const (Thm.dest_arg1 ct) andalso numeral_is_const (Thm.dest_arg ct) 

584 
 Const (@{const_name "HOL.uminus"},_)$t => numeral_is_const (Thm.dest_arg ct) 

585 
 t => can HOLogic.dest_number t 

586 

587 
fun dest_const ct = case term_of ct of 

588 
Const (@{const_name "HOL.divide"},_) $ a $ b=> 

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

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

591 

592 
fun mk_const phi cT x = 

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

23572  594 
in if b = 1 then Numeral.mk_cnumber cT a 
23462  595 
else Thm.capply 
596 
(Thm.capply (Drule.cterm_rule (instantiate' [SOME cT] []) @{cpat "op /"}) 

23572  597 
(Numeral.mk_cnumber cT a)) 
598 
(Numeral.mk_cnumber cT b) 

23462  599 
end 
600 

601 
in 

602 
NormalizerData.funs @{thm class_fieldgb.axioms} 

603 
{is_const = K numeral_is_const, 

604 
dest_const = K dest_const, 

605 
mk_const = mk_const, 

606 
conv = K comp_conv} 

607 
end 

608 

609 
*} 

610 

611 

612 
subsection {* Ferrante and Rackoff algorithm over ordered fields *} 

613 

614 
lemma neg_prod_lt:"(c\<Colon>'a\<Colon>ordered_field) < 0 \<Longrightarrow> ((c*x < 0) == (x > 0))" 

615 
proof 

616 
assume H: "c < 0" 

23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23465
diff
changeset

617 
have "c*x < 0 = (0/c < x)" by (simp only: neg_divide_less_eq[OF H] ring_simps) 
23462  618 
also have "\<dots> = (0 < x)" by simp 
619 
finally show "(c*x < 0) == (x > 0)" by simp 

620 
qed 

621 

622 
lemma pos_prod_lt:"(c\<Colon>'a\<Colon>ordered_field) > 0 \<Longrightarrow> ((c*x < 0) == (x < 0))" 

623 
proof 

624 
assume H: "c > 0" 

23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23465
diff
changeset

625 
hence "c*x < 0 = (0/c > x)" by (simp only: pos_less_divide_eq[OF H] ring_simps) 
23462  626 
also have "\<dots> = (0 > x)" by simp 
627 
finally show "(c*x < 0) == (x < 0)" by simp 

628 
qed 

629 

630 
lemma neg_prod_sum_lt: "(c\<Colon>'a\<Colon>ordered_field) < 0 \<Longrightarrow> ((c*x + t< 0) == (x > ( 1/c)*t))" 

631 
proof 

632 
assume H: "c < 0" 

633 
have "c*x + t< 0 = (c*x < t)" by (subst less_iff_diff_less_0 [of "c*x" "t"], simp) 

23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23465
diff
changeset

634 
also have "\<dots> = (t/c < x)" by (simp only: neg_divide_less_eq[OF H] ring_simps) 
23462  635 
also have "\<dots> = (( 1/c)*t < x)" by simp 
636 
finally show "(c*x + t < 0) == (x > ( 1/c)*t)" by simp 

637 
qed 

638 

639 
lemma pos_prod_sum_lt:"(c\<Colon>'a\<Colon>ordered_field) > 0 \<Longrightarrow> ((c*x + t < 0) == (x < ( 1/c)*t))" 

640 
proof 

641 
assume H: "c > 0" 

642 
have "c*x + t< 0 = (c*x < t)" by (subst less_iff_diff_less_0 [of "c*x" "t"], simp) 

23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23465
diff
changeset

643 
also have "\<dots> = (t/c > x)" by (simp only: pos_less_divide_eq[OF H] ring_simps) 
23462  644 
also have "\<dots> = (( 1/c)*t > x)" by simp 
645 
finally show "(c*x + t < 0) == (x < ( 1/c)*t)" by simp 

646 
qed 

647 

648 
lemma sum_lt:"((x::'a::pordered_ab_group_add) + t < 0) == (x <  t)" 

649 
using less_diff_eq[where a= x and b=t and c=0] by simp 

650 

651 
lemma neg_prod_le:"(c\<Colon>'a\<Colon>ordered_field) < 0 \<Longrightarrow> ((c*x <= 0) == (x >= 0))" 

652 
proof 

653 
assume H: "c < 0" 

23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23465
diff
changeset

654 
have "c*x <= 0 = (0/c <= x)" by (simp only: neg_divide_le_eq[OF H] ring_simps) 
23462  655 
also have "\<dots> = (0 <= x)" by simp 
656 
finally show "(c*x <= 0) == (x >= 0)" by simp 

657 
qed 

658 

659 
lemma pos_prod_le:"(c\<Colon>'a\<Colon>ordered_field) > 0 \<Longrightarrow> ((c*x <= 0) == (x <= 0))" 

660 
proof 

661 
assume H: "c > 0" 

23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23465
diff
changeset

662 
hence "c*x <= 0 = (0/c >= x)" by (simp only: pos_le_divide_eq[OF H] ring_simps) 
23462  663 
also have "\<dots> = (0 >= x)" by simp 
664 
finally show "(c*x <= 0) == (x <= 0)" by simp 

665 
qed 

666 

667 
lemma neg_prod_sum_le: "(c\<Colon>'a\<Colon>ordered_field) < 0 \<Longrightarrow> ((c*x + t <= 0) == (x >= ( 1/c)*t))" 

668 
proof 

669 
assume H: "c < 0" 

670 
have "c*x + t <= 0 = (c*x <= t)" by (subst le_iff_diff_le_0 [of "c*x" "t"], simp) 

23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23465
diff
changeset

671 
also have "\<dots> = (t/c <= x)" by (simp only: neg_divide_le_eq[OF H] ring_simps) 
23462  672 
also have "\<dots> = (( 1/c)*t <= x)" by simp 
673 
finally show "(c*x + t <= 0) == (x >= ( 1/c)*t)" by simp 

674 
qed 

675 

676 
lemma pos_prod_sum_le:"(c\<Colon>'a\<Colon>ordered_field) > 0 \<Longrightarrow> ((c*x + t <= 0) == (x <= ( 1/c)*t))" 

677 
proof 

678 
assume H: "c > 0" 

679 
have "c*x + t <= 0 = (c*x <= t)" by (subst le_iff_diff_le_0 [of "c*x" "t"], simp) 

23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23465
diff
changeset

680 
also have "\<dots> = (t/c >= x)" by (simp only: pos_le_divide_eq[OF H] ring_simps) 
23462  681 
also have "\<dots> = (( 1/c)*t >= x)" by simp 
682 
finally show "(c*x + t <= 0) == (x <= ( 1/c)*t)" by simp 

683 
qed 

684 

685 
lemma sum_le:"((x::'a::pordered_ab_group_add) + t <= 0) == (x <=  t)" 

686 
using le_diff_eq[where a= x and b=t and c=0] by simp 

687 

688 
lemma nz_prod_eq:"(c\<Colon>'a\<Colon>ordered_field) \<noteq> 0 \<Longrightarrow> ((c*x = 0) == (x = 0))" by simp 

689 
lemma nz_prod_sum_eq: "(c\<Colon>'a\<Colon>ordered_field) \<noteq> 0 \<Longrightarrow> ((c*x + t = 0) == (x = ( 1/c)*t))" 

690 
proof 

691 
assume H: "c \<noteq> 0" 

692 
have "c*x + t = 0 = (c*x = t)" by (subst eq_iff_diff_eq_0 [of "c*x" "t"], simp) 

23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23465
diff
changeset

693 
also have "\<dots> = (x = t/c)" by (simp only: nonzero_eq_divide_eq[OF H] ring_simps) 
23462  694 
finally show "(c*x + t = 0) == (x = ( 1/c)*t)" by simp 
695 
qed 

696 
lemma sum_eq:"((x::'a::pordered_ab_group_add) + t = 0) == (x =  t)" 

697 
using eq_diff_eq[where a= x and b=t and c=0] by simp 

698 

699 

23901  700 
interpretation class_ordered_field_dense_linear_order: constr_dense_linear_order 
23462  701 
["op <=" "op <" 
702 
"\<lambda> x y. 1/2 * ((x::'a::{ordered_field,recpower,number_ring}) + y)"] 

23901  703 
proof (unfold_locales, dlo, dlo, auto) 
23462  704 
fix x y::'a assume lt: "x < y" 
705 
from less_half_sum[OF lt] show "x < (x + y) /2" by simp 

706 
next 

707 
fix x y::'a assume lt: "x < y" 

708 
from gt_half_sum[OF lt] show "(x + y) /2 < y" by simp 

709 
qed 

710 

711 
declaration{* 

712 
let 

713 
fun earlier [] x y = false 

714 
 earlier (h::t) x y = 

715 
if h aconvc y then false else if h aconvc x then true else earlier t x y; 

716 

717 
fun dest_frac ct = case term_of ct of 

718 
Const (@{const_name "HOL.divide"},_) $ a $ b=> 

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

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

721 

722 
fun mk_frac phi cT x = 

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

23572  724 
in if b = 1 then Numeral.mk_cnumber cT a 
23462  725 
else Thm.capply 
726 
(Thm.capply (Drule.cterm_rule (instantiate' [SOME cT] []) @{cpat "op /"}) 

23572  727 
(Numeral.mk_cnumber cT a)) 
728 
(Numeral.mk_cnumber cT b) 

23462  729 
end 
730 

731 
fun whatis x ct = case term_of ct of 

732 
Const(@{const_name "HOL.plus"}, _)$(Const(@{const_name "HOL.times"},_)$_$y)$_ => 

733 
if y aconv term_of x then ("c*x+t",[(funpow 2 Thm.dest_arg1) ct, Thm.dest_arg ct]) 

734 
else ("Nox",[]) 

735 
 Const(@{const_name "HOL.plus"}, _)$y$_ => 

736 
if y aconv term_of x then ("x+t",[Thm.dest_arg ct]) 

737 
else ("Nox",[]) 

738 
 Const(@{const_name "HOL.times"}, _)$_$y => 

739 
if y aconv term_of x then ("c*x",[Thm.dest_arg1 ct]) 

740 
else ("Nox",[]) 

741 
 t => if t aconv term_of x then ("x",[]) else ("Nox",[]); 

742 

743 
fun xnormalize_conv ctxt [] ct = reflexive ct 

744 
 xnormalize_conv ctxt (vs as (x::_)) ct = 

745 
case term_of ct of 

23881  746 
Const(@{const_name HOL.less},_)$_$Const(@{const_name "HOL.zero"},_) => 
23462  747 
(case whatis x (Thm.dest_arg1 ct) of 
748 
("c*x+t",[c,t]) => 

749 
let 

750 
val cr = dest_frac c 

751 
val clt = Thm.dest_fun2 ct 

752 
val cz = Thm.dest_arg ct 

753 
val neg = cr </ Rat.zero 

754 
val cthp = Simplifier.rewrite (local_simpset_of ctxt) 

755 
(Thm.capply @{cterm "Trueprop"} 

756 
(if neg then Thm.capply (Thm.capply clt c) cz 

757 
else Thm.capply (Thm.capply clt cz) c)) 

758 
val cth = equal_elim (symmetric cthp) TrueI 

759 
val th = implies_elim (instantiate' [SOME (ctyp_of_term x)] (map SOME [c,x,t]) 

760 
(if neg then @{thm neg_prod_sum_lt} else @{thm pos_prod_sum_lt})) cth 

761 
val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv 

762 
(Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th 

763 
in rth end 

764 
 ("x+t",[t]) => 

765 
let 

766 
val T = ctyp_of_term x 

767 
val th = instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_lt"} 

768 
val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv 

769 
(Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th 

770 
in rth end 

771 
 ("c*x",[c]) => 

772 
let 

773 
val cr = dest_frac c 

774 
val clt = Thm.dest_fun2 ct 

775 
val cz = Thm.dest_arg ct 

776 
val neg = cr </ Rat.zero 

777 
val cthp = Simplifier.rewrite (local_simpset_of ctxt) 

778 
(Thm.capply @{cterm "Trueprop"} 

779 
(if neg then Thm.capply (Thm.capply clt c) cz 

780 
else Thm.capply (Thm.capply clt cz) c)) 

781 
val cth = equal_elim (symmetric cthp) TrueI 

782 
val th = implies_elim (instantiate' [SOME (ctyp_of_term x)] (map SOME [c,x]) 

783 
(if neg then @{thm neg_prod_lt} else @{thm pos_prod_lt})) cth 

784 
val rth = th 

785 
in rth end 

786 
 _ => reflexive ct) 

787 

788 

23881  789 
 Const(@{const_name HOL.less_eq},_)$_$Const(@{const_name "HOL.zero"},_) => 
23462  790 
(case whatis x (Thm.dest_arg1 ct) of 
791 
("c*x+t",[c,t]) => 

792 
let 

793 
val T = ctyp_of_term x 

794 
val cr = dest_frac c 

795 
val clt = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "op <"} 

796 
val cz = Thm.dest_arg ct 

797 
val neg = cr </ Rat.zero 

798 
val cthp = Simplifier.rewrite (local_simpset_of ctxt) 

799 
(Thm.capply @{cterm "Trueprop"} 

800 
(if neg then Thm.capply (Thm.capply clt c) cz 

801 
else Thm.capply (Thm.capply clt cz) c)) 

802 
val cth = equal_elim (symmetric cthp) TrueI 

803 
val th = implies_elim (instantiate' [SOME T] (map SOME [c,x,t]) 

804 
(if neg then @{thm neg_prod_sum_le} else @{thm pos_prod_sum_le})) cth 

805 
val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv 

806 
(Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th 

807 
in rth end 

808 
 ("x+t",[t]) => 

809 
let 

810 
val T = ctyp_of_term x 

811 
val th = instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_le"} 

812 
val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv 

813 
(Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th 

814 
in rth end 

815 
 ("c*x",[c]) => 

816 
let 

817 
val T = ctyp_of_term x 

818 
val cr = dest_frac c 

819 
val clt = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "op <"} 

820 
val cz = Thm.dest_arg ct 

821 
val neg = cr </ Rat.zero 

822 
val cthp = Simplifier.rewrite (local_simpset_of ctxt) 

823 
(Thm.capply @{cterm "Trueprop"} 

824 
(if neg then Thm.capply (Thm.capply clt c) cz 

825 
else Thm.capply (Thm.capply clt cz) c)) 

826 
val cth = equal_elim (symmetric cthp) TrueI 

827 
val th = implies_elim (instantiate' [SOME (ctyp_of_term x)] (map SOME [c,x]) 

828 
(if neg then @{thm neg_prod_le} else @{thm pos_prod_le})) cth 

829 
val rth = th 

830 
in rth end 

831 
 _ => reflexive ct) 

832 

833 
 Const("op =",_)$_$Const(@{const_name "HOL.zero"},_) => 

834 
(case whatis x (Thm.dest_arg1 ct) of 

835 
("c*x+t",[c,t]) => 

836 
let 

837 
val T = ctyp_of_term x 

838 
val cr = dest_frac c 

839 
val ceq = Thm.dest_fun2 ct 

840 
val cz = Thm.dest_arg ct 

841 
val cthp = Simplifier.rewrite (local_simpset_of ctxt) 

842 
(Thm.capply @{cterm "Trueprop"} 

843 
(Thm.capply @{cterm "Not"} (Thm.capply (Thm.capply ceq c) cz))) 

844 
val cth = equal_elim (symmetric cthp) TrueI 

845 
val th = implies_elim 

846 
(instantiate' [SOME T] (map SOME [c,x,t]) @{thm nz_prod_sum_eq}) cth 

847 
val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv 

848 
(Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th 

849 
in rth end 

850 
 ("x+t",[t]) => 

851 
let 

852 
val T = ctyp_of_term x 

853 
val th = instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_eq"} 

854 
val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv 

855 
(Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th 

856 
in rth end 

857 
 ("c*x",[c]) => 

858 
let 

859 
val T = ctyp_of_term x 

860 
val cr = dest_frac c 

861 
val ceq = Thm.dest_fun2 ct 

862 
val cz = Thm.dest_arg ct 

863 
val cthp = Simplifier.rewrite (local_simpset_of ctxt) 

864 
(Thm.capply @{cterm "Trueprop"} 

865 
(Thm.capply @{cterm "Not"} (Thm.capply (Thm.capply ceq c) cz))) 

866 
val cth = equal_elim (symmetric cthp) TrueI 

867 
val rth = implies_elim 

868 
(instantiate' [SOME T] (map SOME [c,x]) @{thm nz_prod_eq}) cth 

869 
in rth end 

870 
 _ => reflexive ct); 

871 

872 
local 

873 
val less_iff_diff_less_0 = mk_meta_eq @{thm "less_iff_diff_less_0"} 

874 
val le_iff_diff_le_0 = mk_meta_eq @{thm "le_iff_diff_le_0"} 

875 
val eq_iff_diff_eq_0 = mk_meta_eq @{thm "eq_iff_diff_eq_0"} 

876 
in 

877 
fun field_isolate_conv phi ctxt vs ct = case term_of ct of 

23881  878 
Const(@{const_name HOL.less},_)$a$b => 
23462  879 
let val (ca,cb) = Thm.dest_binop ct 
880 
val T = ctyp_of_term ca 

881 
val th = instantiate' [SOME T] [SOME ca, SOME cb] less_iff_diff_less_0 

882 
val nth = Conv.fconv_rule 

883 
(Conv.arg_conv (Conv.arg1_conv 

884 
(Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th 

885 
val rth = transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth)) 

886 
in rth end 

23881  887 
 Const(@{const_name HOL.less_eq},_)$a$b => 
23462  888 
let val (ca,cb) = Thm.dest_binop ct 
889 
val T = ctyp_of_term ca 

890 
val th = instantiate' [SOME T] [SOME ca, SOME cb] le_iff_diff_le_0 

891 
val nth = Conv.fconv_rule 

892 
(Conv.arg_conv (Conv.arg1_conv 

893 
(Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th 

894 
val rth = transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth)) 

895 
in rth end 

896 

897 
 Const("op =",_)$a$b => 

898 
let val (ca,cb) = Thm.dest_binop ct 

899 
val T = ctyp_of_term ca 

900 
val th = instantiate' [SOME T] [SOME ca, SOME cb] eq_iff_diff_eq_0 

901 
val nth = Conv.fconv_rule 

902 
(Conv.arg_conv (Conv.arg1_conv 

903 
(Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th 

904 
val rth = transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth)) 

905 
in rth end 

906 
 @{term "Not"} $(Const("op =",_)$a$b) => Conv.arg_conv (field_isolate_conv phi ctxt vs) ct 

907 
 _ => reflexive ct 

908 
end; 

909 

910 
fun classfield_whatis phi = 

911 
let 

912 
fun h x t = 

913 
case term_of t of 

914 
Const("op =", _)$y$z => if term_of x aconv y then Ferrante_Rackoff_Data.Eq 

915 
else Ferrante_Rackoff_Data.Nox 

916 
 @{term "Not"}$(Const("op =", _)$y$z) => if term_of x aconv y then Ferrante_Rackoff_Data.NEq 

917 
else Ferrante_Rackoff_Data.Nox 

23881  918 
 Const(@{const_name HOL.less},_)$y$z => 
23462  919 
if term_of x aconv y then Ferrante_Rackoff_Data.Lt 
920 
else if term_of x aconv z then Ferrante_Rackoff_Data.Gt 

921 
else Ferrante_Rackoff_Data.Nox 

23881  922 
 Const (@{const_name HOL.less_eq},_)$y$z => 
23462  923 
if term_of x aconv y then Ferrante_Rackoff_Data.Le 
924 
else if term_of x aconv z then Ferrante_Rackoff_Data.Ge 

925 
else Ferrante_Rackoff_Data.Nox 

926 
 _ => Ferrante_Rackoff_Data.Nox 

927 
in h end; 

928 
fun class_field_ss phi = 

929 
HOL_basic_ss addsimps ([@{thm "linorder_not_less"}, @{thm "linorder_not_le"}]) 

930 
addsplits [@{thm "abs_split"},@{thm "split_max"}, @{thm "split_min"}] 

931 

932 
in 

933 
Ferrante_Rackoff_Data.funs @{thm "class_ordered_field_dense_linear_order.ferrack_axiom"} 

934 
{isolate_conv = field_isolate_conv, whatis = classfield_whatis, simpset = class_field_ss} 

935 
end 

936 
*} 

937 

938 
end 