Isar command 'calculation' as front-end for KEStore_Elems.add_calcs, without change of semantics;
1 (* rationals, fractions of multivariate polynomials over the real field
3 Copyright (c) isac team 2002, 2013
4 Use is subject to license terms.
6 depends on Poly (and not on Atools), because
7 fractions with _normalised_ polynomials are canceled, added, etc.
11 imports Poly GCD_Poly_ML
14 section \<open>Constants for evaluation by "Rule.Eval"\<close>
17 is_expanded :: "real => bool" ("_ is'_expanded") (*RL->Poly.thy*)
18 is_ratpolyexp :: "real => bool" ("_ is'_ratpolyexp")
19 get_denominator :: "real => real"
20 get_numerator :: "real => real"
23 (*.the expression contains + - * ^ / only ?.*)
24 fun is_ratpolyexp (Free _) = true
25 | is_ratpolyexp (Const (\<^const_name>\<open>plus\<close>,_) $ Free _ $ Free _) = true
26 | is_ratpolyexp (Const (\<^const_name>\<open>minus\<close>,_) $ Free _ $ Free _) = true
27 | is_ratpolyexp (Const (\<^const_name>\<open>times\<close>,_) $ Free _ $ Free _) = true
28 | is_ratpolyexp (Const (\<^const_name>\<open>powr\<close>,_) $ Free _ $ Free _) = true
29 | is_ratpolyexp (Const (\<^const_name>\<open>divide\<close>,_) $ Free _ $ Free _) = true
30 | is_ratpolyexp (Const (\<^const_name>\<open>plus\<close>,_) $ t1 $ t2) =
31 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
32 | is_ratpolyexp (Const (\<^const_name>\<open>minus\<close>,_) $ t1 $ t2) =
33 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
34 | is_ratpolyexp (Const (\<^const_name>\<open>times\<close>,_) $ t1 $ t2) =
35 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
36 | is_ratpolyexp (Const (\<^const_name>\<open>powr\<close>,_) $ t1 $ t2) =
37 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
38 | is_ratpolyexp (Const (\<^const_name>\<open>divide\<close>,_) $ t1 $ t2) =
39 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
40 | is_ratpolyexp _ = false;
42 (*("is_ratpolyexp", ("Rational.is_ratpolyexp", eval_is_ratpolyexp ""))*)
43 fun eval_is_ratpolyexp (thmid:string) _
44 (t as (Const("Rational.is_ratpolyexp", _) $ arg)) thy =
46 then SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",
47 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
48 else SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",
49 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
50 | eval_is_ratpolyexp _ _ _ _ = NONE;
52 (*("get_denominator", ("Rational.get_denominator", eval_get_denominator ""))*)
53 fun eval_get_denominator (thmid:string) _
54 (t as Const ("Rational.get_denominator", _) $
55 (Const (\<^const_name>\<open>divide\<close>, _) $ _(*num*) $
57 SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy denom) "",
58 HOLogic.Trueprop $ (TermC.mk_equality (t, denom)))
59 | eval_get_denominator _ _ _ _ = NONE;
61 (*("get_numerator", ("Rational.get_numerator", eval_get_numerator ""))*)
62 fun eval_get_numerator (thmid:string) _
63 (t as Const ("Rational.get_numerator", _) $
64 (Const (\<^const_name>\<open>divide\<close>, _) $num
66 SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy num) "",
67 HOLogic.Trueprop $ (TermC.mk_equality (t, num)))
68 | eval_get_numerator _ _ _ _ = NONE;
71 section \<open>Theorems for rewriting\<close>
73 axiomatization (* naming due to Isabelle2002, but not contained in Isabelle2002;
74 many thms are due to RL and can be removed with updating the equation solver;
75 TODO: replace by equivalent thms in recent Isabelle201x *)
77 mult_cross: "[| b ~= 0; d ~= 0 |] ==> (a / b = c / d) = (a * d = b * c)" and
78 mult_cross1: " b ~= 0 ==> (a / b = c ) = (a = b * c)" and
79 mult_cross2: " d ~= 0 ==> (a = c / d) = (a * d = c)" and
81 add_minus: "a + b - b = a"(*RL->Poly.thy*) and
82 add_minus1: "a - b + b = a"(*RL->Poly.thy*) and
84 rat_mult: "a / b * (c / d) = a * c / (b * d)"(*?Isa02*) and
85 rat_mult2: "a / b * c = a * c / b "(*?Isa02*) and
87 rat_mult_poly_l: "c is_polyexp ==> c * (a / b) = c * a / b" and
88 rat_mult_poly_r: "c is_polyexp ==> (a / b) * c = a * c / b" and
90 (*real_times_divide1_eq .. Isa02*)
91 real_times_divide_1_eq: "-1 * (c / d) = -1 * c / d " and
92 real_times_divide_num: "a is_const ==> a * (c / d) = a * c / d " and
94 real_mult_div_cancel2: "k ~= 0 ==> m * k / (n * k) = m / n" and
95 (*real_mult_div_cancel1: "k ~= 0 ==> k * m / (k * n) = m / n"..Isa02*)
97 real_divide_divide1: "y ~= 0 ==> (u / v) / (y / z) = (u / v) * (z / y)" and
98 real_divide_divide1_mg: "y ~= 0 ==> (u / v) / (y / z) = (u * z) / (y * v)" and
99 (*real_divide_divide2_eq: "x / y / z = x / (y * z)"..Isa02*)
101 rat_power: "(a / b) \<up> n = (a \<up> n) / (b \<up> n)" and
103 rat_add: "[| a is_const; b is_const; c is_const; d is_const |] ==>
104 a / c + b / d = (a * d + b * c) / (c * d)" and
105 rat_add_assoc: "[| a is_const; b is_const; c is_const; d is_const |] ==>
106 a / c +(b / d + e) = (a * d + b * c)/(d * c) + e" and
107 rat_add1: "[| a is_const; b is_const; c is_const |] ==>
108 a / c + b / c = (a + b) / c" and
109 rat_add1_assoc: "[| a is_const; b is_const; c is_const |] ==>
110 a / c + (b / c + e) = (a + b) / c + e" and
111 rat_add2: "[| a is_const; b is_const; c is_const |] ==>
112 a / c + b = (a + b * c) / c" and
113 rat_add2_assoc: "[| a is_const; b is_const; c is_const |] ==>
114 a / c + (b + e) = (a + b * c) / c + e" and
115 rat_add3: "[| a is_const; b is_const; c is_const |] ==>
116 a + b / c = (a * c + b) / c" and
117 rat_add3_assoc: "[| a is_const; b is_const; c is_const |] ==>
118 a + (b / c + e) = (a * c + b) / c + e"
120 section \<open>Cancellation and addition of fractions\<close>
121 subsection \<open>Conversion term <--> poly\<close>
122 subsubsection \<open>Convert a term to the internal representation of a multivariate polynomial\<close>
124 fun monom_of_term vs (c, es) (t as Const _) =
125 (c, list_update es (find_index (curry op = t) vs) 1)
126 | monom_of_term vs (c, es) (t as Free (id, _)) =
128 then (id |> TermC.int_opt_of_string |> the |> curry op * c, es) (*several numerals in one monom*)
129 else (c, list_update es (find_index (curry op = t) vs) 1)
130 | monom_of_term vs (c, es) (Const (\<^const_name>\<open>powr\<close>, _) $ (t as Free _) $ Free (e, _)) =
131 (c, list_update es (find_index (curry op = t) vs) (the (TermC.int_opt_of_string e)))
132 | monom_of_term vs (c, es) (Const (\<^const_name>\<open>times\<close>, _) $ m1 $ m2) =
133 let val (c', es') = monom_of_term vs (c, es) m1
134 in monom_of_term vs (c', es') m2 end
135 | monom_of_term _ _ t = raise ERROR ("poly malformed 1 with " ^ UnparseC.term t)
137 fun monoms_of_term vs (t as Const _) =
138 [monom_of_term vs (1, replicate (length vs) 0) t]
139 | monoms_of_term vs (t as Free _) =
140 [monom_of_term vs (1, replicate (length vs) 0) t]
141 | monoms_of_term vs (t as Const (\<^const_name>\<open>powr\<close>, _) $ _ $ _) =
142 [monom_of_term vs (1, replicate (length vs) 0) t]
143 | monoms_of_term vs (t as Const (\<^const_name>\<open>times\<close>, _) $ _ $ _) =
144 [monom_of_term vs (1, replicate (length vs) 0) t]
145 | monoms_of_term vs (Const (\<^const_name>\<open>plus\<close>, _) $ ms1 $ ms2) =
146 (monoms_of_term vs ms1) @ (monoms_of_term vs ms2)
147 | monoms_of_term _ t = raise ERROR ("poly malformed 2 with " ^ UnparseC.term t)
149 (* convert a term to the internal representation of a multivariate polynomial;
150 the conversion is quite liberal, see test --- fun poly_of_term ---:
151 * the order of variables and the parentheses within a monomial are arbitrary
152 * the coefficient may be somewhere
153 * he order and the parentheses within monomials are arbitrary
154 But the term must be completely expand + over * (laws of distributivity are not applicable).
156 The function requires the free variables as strings already given,
157 because the gcd involves 2 polynomials (with the same length for their list of exponents).
159 fun poly_of_term vs (t as Const (\<^const_name>\<open>plus\<close>, _) $ _ $ _) =
160 (SOME (t |> monoms_of_term vs |> order)
161 handle ERROR _ => NONE)
162 | poly_of_term vs t =
163 (SOME [monom_of_term vs (1, replicate (length vs) 0) t]
164 handle ERROR _ => NONE)
168 val vs = TermC.vars_of t
170 case poly_of_term vs t of SOME _ => true | NONE => false
172 val is_expanded = is_poly (* TODO: check names *)
173 val is_polynomial = is_poly (* TODO: check names *)
176 subsubsection \<open>Convert internal representation of a multivariate polynomial to a term\<close>
178 fun term_of_es _ _ _ [] = [] (*assumes same length for vs and es*)
179 | term_of_es baseT expT (_ :: vs) (0 :: es) = [] @ term_of_es baseT expT vs es
180 | term_of_es baseT expT (v :: vs) (1 :: es) = v :: term_of_es baseT expT vs es
181 | term_of_es baseT expT (v :: vs) (e :: es) =
182 Const (\<^const_name>\<open>powr\<close>, [baseT, expT] ---> baseT) $ v $ (Free (TermC.isastr_of_int e, expT))
183 :: term_of_es baseT expT vs es
184 | term_of_es _ _ _ _ = raise ERROR "term_of_es: length vs <> length es"
186 fun term_of_monom baseT expT vs ((c, es): monom) =
187 let val es' = term_of_es baseT expT vs es
191 if es' = [] (*if es = [0,0,0,...]*)
192 then Free (TermC.isastr_of_int c, baseT)
193 else foldl (HOLogic.mk_binop \<^const_name>\<open>times\<close>) (hd es', tl es')
194 else foldl (HOLogic.mk_binop \<^const_name>\<open>times\<close>) (Free (TermC.isastr_of_int c, baseT), es')
197 fun term_of_poly baseT expT vs p =
198 let val monos = map (term_of_monom baseT expT vs) p
199 in foldl (HOLogic.mk_binop \<^const_name>\<open>plus\<close>) (hd monos, tl monos) end
202 subsection \<open>Apply gcd_poly for cancelling and adding fractions as terms\<close>
204 fun mk_noteq_0 baseT t =
205 Const (\<^const_name>\<open>Not\<close>, HOLogic.boolT --> HOLogic.boolT) $
206 (Const (\<^const_name>\<open>HOL.eq\<close>, [baseT, baseT] ---> HOLogic.boolT) $ t $ Free ("0", HOLogic.realT))
208 fun mk_asms baseT ts =
209 let val as' = filter_out TermC.is_num ts (* asm like "2 ~= 0" is needless *)
210 in map (mk_noteq_0 baseT) as' end
213 subsubsection \<open>Factor out gcd for cancellation\<close>
215 fun check_fraction t =
217 Const (\<^const_name>\<open>divide\<close>, _) $ numerator $ denominator
218 => SOME (numerator, denominator)
221 (* prepare a term for cancellation by factoring out the gcd
222 assumes: is a fraction with outmost "/"*)
223 fun factout_p_ (thy: theory) t =
224 let val opt = check_fraction t
228 | SOME (numerator, denominator) =>
230 val vs = TermC.vars_of t
231 val baseT = type_of numerator
232 val expT = HOLogic.realT
234 case (poly_of_term vs numerator, poly_of_term vs denominator) of
237 val ((a', b'), c) = gcd_poly a b
238 val es = replicate (length vs) 0
240 if c = [(1, es)] orelse c = [(~1, es)]
244 val b't = term_of_poly baseT expT vs b'
245 val ct = term_of_poly baseT expT vs c
247 HOLogic.mk_binop \<^const_name>\<open>divide\<close>
248 (HOLogic.mk_binop \<^const_name>\<open>times\<close>
249 (term_of_poly baseT expT vs a', ct),
250 HOLogic.mk_binop \<^const_name>\<open>times\<close> (b't, ct))
251 in SOME (t', mk_asms baseT [b't, ct]) end
253 | _ => NONE : (term * term list) option
258 subsubsection \<open>Cancel a fraction\<close>
260 (* cancel a term by the gcd ("" denote terms with internal algebraic structure)
261 cancel_p_ :: theory \<Rightarrow> term \<Rightarrow> (term \<times> term list) option
262 cancel_p_ thy "a / b" = SOME ("a' / b'", ["b' \<noteq> 0"])
263 assumes: a is_polynomial \<and> b is_polynomial \<and> b \<noteq> 0
265 SOME ("a' / b'", ["b' \<noteq> 0"]). gcd_poly a b \<noteq> 1 \<and> gcd_poly a b \<noteq> -1 \<and>
266 a' * gcd_poly a b = a \<and> b' * gcd_poly a b = b
268 fun cancel_p_ (_: theory) t =
269 let val opt = check_fraction t
273 | SOME (numerator, denominator) =>
275 val vs = TermC.vars_of t
276 val baseT = type_of numerator
277 val expT = HOLogic.realT
279 case (poly_of_term vs numerator, poly_of_term vs denominator) of
282 val ((a', b'), c) = gcd_poly a b
283 val es = replicate (length vs) 0
285 if c = [(1, es)] orelse c = [(~1, es)]
289 val bt' = term_of_poly baseT expT vs b'
290 val ct = term_of_poly baseT expT vs c
292 HOLogic.mk_binop \<^const_name>\<open>divide\<close>
293 (term_of_poly baseT expT vs a', bt')
294 val asm = mk_asms baseT [bt']
295 in SOME (t', asm) end
297 | _ => NONE : (term * term list) option
302 subsubsection \<open>Factor out to a common denominator for addition\<close>
304 (* addition of fractions allows (at most) one non-fraction (a monomial) *)
306 (Const (\<^const_name>\<open>plus\<close>, _) $
307 (Const (\<^const_name>\<open>divide\<close>, _) $ n1 $ d1) $
308 (Const (\<^const_name>\<open>divide\<close>, _) $ n2 $ d2))
309 = SOME ((n1, d1), (n2, d2))
311 (Const (\<^const_name>\<open>plus\<close>, _) $
313 (Const (\<^const_name>\<open>divide\<close>, _) $ n2 $ d2))
314 = SOME ((nofrac, Free ("1", HOLogic.realT)), (n2, d2))
316 (Const (\<^const_name>\<open>plus\<close>, _) $
317 (Const (\<^const_name>\<open>divide\<close>, _) $ n1 $ d1) $
319 = SOME ((n1, d1), (nofrac, Free ("1", HOLogic.realT)))
320 | check_frac_sum _ = NONE
322 (* prepare a term for addition by providing the least common denominator as a product
323 assumes: is a term with outmost "+" and at least one outmost "/" in respective summands*)
324 fun common_nominator_p_ (_: theory) t =
325 let val opt = check_frac_sum t
329 | SOME ((n1, d1), (n2, d2)) =>
331 val vs = TermC.vars_of t
333 case (poly_of_term vs d1, poly_of_term vs d2) of
336 val ((a', b'), c) = gcd_poly a b
337 val (baseT, expT) = (type_of n1, HOLogic.realT)
338 val [d1', d2', c'] = map (term_of_poly baseT expT vs) [a', b', c]
339 (*----- minimum of parentheses & nice result, but breaks tests: -------------
340 val denom = HOLogic.mk_binop \<^const_name>\<open>times\<close>
341 (HOLogic.mk_binop \<^const_name>\<open>times\<close> (d1', d2'), c') -------------*)
343 if c = [(1, replicate (length vs) 0)]
344 then HOLogic.mk_binop \<^const_name>\<open>times\<close> (d1', d2')
346 HOLogic.mk_binop \<^const_name>\<open>times\<close> (c',
347 HOLogic.mk_binop \<^const_name>\<open>times\<close> (d1', d2')) (*--------------*)
349 HOLogic.mk_binop \<^const_name>\<open>plus\<close>
350 (HOLogic.mk_binop \<^const_name>\<open>divide\<close>
351 (HOLogic.mk_binop \<^const_name>\<open>times\<close> (n1, d2'), denom),
352 HOLogic.mk_binop \<^const_name>\<open>divide\<close>
353 (HOLogic.mk_binop \<^const_name>\<open>times\<close> (n2, d1'), denom))
354 val asm = mk_asms baseT [d1', d2', c']
355 in SOME (t', asm) end
356 | _ => NONE : (term * term list) option
361 subsubsection \<open>Addition of at least one fraction within a sum\<close>
364 assumes: is a term with outmost "+" and at least one outmost "/" in respective summands
365 NOTE: the case "(_ + _) + _" need not be considered due to iterated addition.*)
366 fun add_fraction_p_ (_: theory) t =
367 case check_frac_sum t of
369 | SOME ((n1, d1), (n2, d2)) =>
371 val vs = TermC.vars_of t
373 case (poly_of_term vs n1, poly_of_term vs d1, poly_of_term vs n2, poly_of_term vs d2) of
374 (SOME _, SOME a, SOME _, SOME b) =>
376 val ((a', b'), c) = gcd_poly a b
377 val (baseT, expT) = (type_of n1, HOLogic.realT)
378 val nomin = term_of_poly baseT expT vs
379 (((the (poly_of_term vs n1)) %%*%% b') %%+%% ((the (poly_of_term vs n2)) %%*%% a'))
380 val denom = term_of_poly baseT expT vs ((c %%*%% a') %%*%% b')
381 val t' = HOLogic.mk_binop \<^const_name>\<open>divide\<close> (nomin, denom)
382 in SOME (t', mk_asms baseT [denom]) end
383 | _ => NONE : (term * term list) option
387 section \<open>Embed cancellation and addition into rewriting\<close>
389 subsection \<open>Rulesets and predicate for embedding\<close>
391 (* evaluates conditions in calculate_Rational *)
394 (Rule_Def.Repeat {id = "calc_rat_erls", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
395 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
397 [\<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
398 \<^rule_eval>\<open>Prog_Expr.is_const\<close> (Prog_Expr.eval_const "#is_const_"),
399 \<^rule_thm>\<open>not_true\<close>,
400 \<^rule_thm>\<open>not_false\<close>],
401 scr = Rule.Empty_Prog});
403 (* simplifies expressions with numerals;
404 does NOT rearrange the term by AC-rewriting; thus terms with variables
405 need to have constants to be commuted together respectively *)
406 val calculate_Rational =
407 prep_rls' (Rule_Set.merge "calculate_Rational"
408 (Rule_Def.Repeat {id = "divide", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
409 erls = calc_rat_erls, srls = Rule_Set.Empty,
410 calc = [], errpatts = [],
412 [\<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
414 Rule.Thm ("minus_divide_left", ThmC.numerals_to_Free (@{thm minus_divide_left} RS @{thm sym})),
415 (*SYM - ?x / ?y = - (?x / ?y) may come from subst*)
416 \<^rule_thm>\<open>rat_add\<close>,
417 (*"[| a is_const; b is_const; c is_const; d is_const |] ==> \
418 \a / c + b / d = (a * d) / (c * d) + (b * c ) / (d * c)"*)
419 \<^rule_thm>\<open>rat_add1\<close>,
420 (*"[| a is_const; b is_const; c is_const |] ==> a / c + b / c = (a + b) / c"*)
421 \<^rule_thm>\<open>rat_add2\<close>,
422 (*"[| ?a is_const; ?b is_const; ?c is_const |] ==> ?a / ?c + ?b = (?a + ?b * ?c) / ?c"*)
423 \<^rule_thm>\<open>rat_add3\<close>,
424 (*"[| a is_const; b is_const; c is_const |] ==> a + b / c = (a * c) / c + b / c"\
425 .... is_const to be omitted here FIXME*)
427 \<^rule_thm>\<open>rat_mult\<close>,
428 (*a / b * (c / d) = a * c / (b * d)*)
429 \<^rule_thm>\<open>times_divide_eq_right\<close>,
430 (*?x * (?y / ?z) = ?x * ?y / ?z*)
431 \<^rule_thm>\<open>times_divide_eq_left\<close>,
432 (*?y / ?z * ?x = ?y * ?x / ?z*)
434 \<^rule_thm>\<open>real_divide_divide1\<close>,
435 (*"?y ~= 0 ==> ?u / ?v / (?y / ?z) = ?u / ?v * (?z / ?y)"*)
436 \<^rule_thm>\<open>divide_divide_eq_left\<close>,
437 (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
439 \<^rule_thm>\<open>rat_power\<close>,
440 (*"(?a / ?b) \<up> ?n = ?a \<up> ?n / ?b \<up> ?n"*)
442 \<^rule_thm>\<open>mult_cross\<close>,
443 (*"[| b ~= 0; d ~= 0 |] ==> (a / b = c / d) = (a * d = b * c)*)
444 \<^rule_thm>\<open>mult_cross1\<close>,
445 (*" b ~= 0 ==> (a / b = c ) = (a = b * c)*)
446 \<^rule_thm>\<open>mult_cross2\<close>
447 (*" d ~= 0 ==> (a = c / d) = (a * d = c)*)],
448 scr = Rule.Empty_Prog})
451 (*("is_expanded", ("Rational.is_expanded", eval_is_expanded ""))*)
452 fun eval_is_expanded (thmid:string) _
453 (t as (Const("Rational.is_expanded", _) $ arg)) thy =
455 then SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",
456 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
457 else SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",
458 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
459 | eval_is_expanded _ _ _ _ = NONE;
461 calculation is_expanded = \<open>eval_is_expanded ""\<close>
464 Rule_Set.merge "rational_erls" calculate_Rational
465 (Rule_Set.append_rules "is_expanded" Atools_erls
466 [\<^rule_eval>\<open>is_expanded\<close> (eval_is_expanded "")]);
469 subsection \<open>Embed cancellation into rewriting\<close>
471 (**)local (* cancel_p *)
473 val {rules = rules, rew_ord = (_, ro), ...} = Rule_Set.rep (assoc_rls' @{theory} "rev_rew_p");
475 fun init_state thy eval_rls ro t =
477 val SOME (t', _) = factout_p_ thy t;
478 val SOME (t'', asm) = cancel_p_ thy t;
479 val der = Derive.steps_reverse thy eval_rls rules ro NONE t';
481 [(\<^rule_thm>\<open>real_mult_div_cancel2\<close>, (t'', asm))]
482 val rs = (Rule.distinct' o (map #1)) der
483 val rs = filter_out (ThmC.member'
484 ["sym_real_add_zero_left", "sym_real_mult_0", "sym_real_mult_1"]) rs
485 in (t, t'', [rs(*one in order to ease locate_rule*)], der) end;
487 fun locate_rule thy eval_rls ro [rs] t r =
488 if member op = ((map (Rule.thm_id)) rs) (Rule.thm_id r)
490 let val ropt = Rewrite.rewrite_ thy ro eval_rls true (Rule.thm r) t;
492 case ropt of SOME ta => [(r, ta)]
494 ("### locate_rule: rewrite " ^ Rule.thm_id r ^ " " ^ UnparseC.term t ^ " = NONE");*) [])
496 else ((*tracing ("### locate_rule: " ^ Rule.thm_id r ^ " not mem rrls");*) [])
497 | locate_rule _ _ _ _ _ _ = raise ERROR "locate_rule: doesnt match rev-sets in istate";
499 fun next_rule thy eval_rls ro [rs] t =
501 val der = Derive.do_one thy eval_rls rs ro NONE t;
502 in case der of (_, r, _) :: _ => SOME r | _ => NONE end
503 | next_rule _ _ _ _ _ = raise ERROR ("next_rule: doesnt match rev-sets in istate");
505 fun attach_form (_: Rule.rule list list) (_: term) (_: term) =
506 [(*TODO*)]: ( Rule.rule * (term * term list)) list;
511 Rule_Set.Rrls {id = "cancel_p", prepat = [],
512 rew_ord=("ord_make_polynomial", ord_make_polynomial false \<^theory>),
513 erls = rational_erls,
515 [("PLUS", (\<^const_name>\<open>plus\<close>, (**)eval_binop "#add_")),
516 ("TIMES" , (\<^const_name>\<open>times\<close>, (**)eval_binop "#mult_")),
517 ("DIVIDE", (\<^const_name>\<open>divide\<close>, Prog_Expr.eval_cancel "#divide_e")),
518 ("POWER", (\<^const_name>\<open>powr\<close>, (**)eval_binop "#power_"))],
521 Rule.Rfuns {init_state = init_state \<^theory> Atools_erls ro,
522 normal_form = cancel_p_ \<^theory>,
523 locate_rule = locate_rule \<^theory> Atools_erls ro,
524 next_rule = next_rule \<^theory> Atools_erls ro,
525 attach_form = attach_form}}
526 (**)end(* local cancel_p *)
529 subsection \<open>Embed addition into rewriting\<close>
531 (**)local (* add_fractions_p *)
533 (*val {rules = rules, rew_ord = (_, ro), ...} = Rule_Set.rep (assoc_rls "make_polynomial");*)
534 val {rules, rew_ord=(_,ro),...} = Rule_Set.rep (assoc_rls' @{theory} "rev_rew_p");
536 fun init_state thy eval_rls ro t =
538 val SOME (t',_) = common_nominator_p_ thy t;
539 val SOME (t'', asm) = add_fraction_p_ thy t;
540 val der = Derive.steps_reverse thy eval_rls rules ro NONE t';
542 [(\<^rule_thm>\<open>real_mult_div_cancel2\<close>, (t'',asm))]
543 val rs = (Rule.distinct' o (map #1)) der;
544 val rs = filter_out (ThmC.member'
545 ["sym_real_add_zero_left", "sym_real_mult_0", "sym_real_mult_1"]) rs;
546 in (t, t'', [rs(*here only _ONE_*)], der) end;
548 fun locate_rule thy eval_rls ro [rs] t r =
549 if member op = ((map (Rule.thm_id)) rs) (Rule.thm_id r)
551 let val ropt = Rewrite.rewrite_ thy ro eval_rls true (Rule.thm r) t;
556 ((*tracing ("### locate_rule: rewrite " ^ Rule.thm_id r ^ " " ^ UnparseC.term t ^ " = NONE");*)
558 else ((*tracing ("### locate_rule: " ^ Rule.thm_id r ^ " not mem rrls");*) [])
559 | locate_rule _ _ _ _ _ _ = raise ERROR "locate_rule: doesnt match rev-sets in istate";
561 fun next_rule thy eval_rls ro [rs] t =
562 let val der = Derive.do_one thy eval_rls rs ro NONE t;
568 | next_rule _ _ _ _ _ = raise ERROR ("next_rule: doesnt match rev-sets in istate");
570 val pat0 = TermC.parse_patt \<^theory> "?r/?s+?u/?v :: real";
571 val pat1 = TermC.parse_patt \<^theory> "?r/?s+?u :: real";
572 val pat2 = TermC.parse_patt \<^theory> "?r +?u/?v :: real";
573 val prepat = [([@{term True}], pat0),
574 ([@{term True}], pat1),
575 ([@{term True}], pat2)];
578 val add_fractions_p =
579 Rule_Set.Rrls {id = "add_fractions_p", prepat=prepat,
580 rew_ord = ("ord_make_polynomial", ord_make_polynomial false \<^theory>),
581 erls = rational_erls,
582 calc = [("PLUS", (\<^const_name>\<open>plus\<close>, (**)eval_binop "#add_")),
583 ("TIMES", (\<^const_name>\<open>times\<close>, (**)eval_binop "#mult_")),
584 ("DIVIDE", (\<^const_name>\<open>divide\<close>, Prog_Expr.eval_cancel "#divide_e")),
585 ("POWER", (\<^const_name>\<open>powr\<close>, (**)eval_binop "#power_"))],
587 scr = Rule.Rfuns {init_state = init_state \<^theory> Atools_erls ro,
588 normal_form = add_fraction_p_ \<^theory>,
589 locate_rule = locate_rule \<^theory> Atools_erls ro,
590 next_rule = next_rule \<^theory> Atools_erls ro,
591 attach_form = attach_form}}
592 (**)end(*local add_fractions_p *)
595 subsection \<open>Cancelling and adding all occurrences in a term /////////////////////////////\<close>
597 (*copying cancel_p_rls + add her caused error in interface.sml*)
600 section \<open>Rulesets for general simplification\<close>
602 (*erls for calculate_Rational; make local with FIXX@ME result:term *term list*)
603 val powers_erls = prep_rls'(
604 Rule_Def.Repeat {id = "powers_erls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
605 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
606 rules = [\<^rule_eval>\<open>Prog_Expr.is_atom\<close> (Prog_Expr.eval_is_atom "#is_atom_"),
607 \<^rule_eval>\<open>Prog_Expr.is_even\<close> (Prog_Expr.eval_is_even "#is_even_"),
608 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
609 \<^rule_thm>\<open>not_false\<close>,
610 \<^rule_thm>\<open>not_true\<close>,
611 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")
613 scr = Rule.Empty_Prog
615 (*.all powers over + distributed; atoms over * collected, other distributed
616 contains absolute minimum of thms for context in norm_Rational .*)
617 val powers = prep_rls'(
618 Rule_Def.Repeat {id = "powers", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
619 erls = powers_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
620 rules = [\<^rule_thm>\<open>realpow_multI\<close>,
621 (*"(r * s) \<up> n = r \<up> n * s \<up> n"*)
622 \<^rule_thm>\<open>realpow_pow\<close>,
623 (*"(a \<up> b) \<up> c = a \<up> (b * c)"*)
624 \<^rule_thm>\<open>realpow_oneI\<close>,
626 \<^rule_thm>\<open>realpow_minus_even\<close>,
627 (*"n is_even ==> (- r) \<up> n = r \<up> n" ?-->discard_minus?*)
628 \<^rule_thm>\<open>realpow_minus_odd\<close>,
629 (*"Not (n is_even) ==> (- r) \<up> n = -1 * r \<up> n"*)
631 (*----- collect atoms over * -----*)
632 \<^rule_thm>\<open>realpow_two_atom\<close>,
633 (*"r is_atom ==> r * r = r \<up> 2"*)
634 \<^rule_thm>\<open>realpow_plus_1\<close>,
635 (*"r is_atom ==> r * r \<up> n = r \<up> (n + 1)"*)
636 \<^rule_thm>\<open>realpow_addI_atom\<close>,
637 (*"r is_atom ==> r \<up> n * r \<up> m = r \<up> (n + m)"*)
639 (*----- distribute none-atoms -----*)
640 \<^rule_thm>\<open>realpow_def_atom\<close>,
641 (*"[| 1 < n; ~ (r is_atom) |]==>r \<up> n = r * r \<up> (n + -1)"*)
642 \<^rule_thm>\<open>realpow_eq_oneI\<close>,
644 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")
646 scr = Rule.Empty_Prog
648 (*.contains absolute minimum of thms for context in norm_Rational.*)
649 val rat_mult_divide = prep_rls'(
650 Rule_Def.Repeat {id = "rat_mult_divide", preconds = [],
651 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
652 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
653 rules = [\<^rule_thm>\<open>rat_mult\<close>,
654 (*(1)"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
655 \<^rule_thm>\<open>times_divide_eq_right\<close>,
656 (*(2)"?a * (?c / ?d) = ?a * ?c / ?d" must be [2],
657 otherwise inv.to a / b / c = ...*)
658 \<^rule_thm>\<open>times_divide_eq_left\<close>,
659 (*"?a / ?b * ?c = ?a * ?c / ?b" order weights x \<up> n too much
660 and does not commute a / b * c \<up> 2 !*)
662 \<^rule_thm>\<open>divide_divide_eq_right\<close>,
663 (*"?x / (?y / ?z) = ?x * ?z / ?y"*)
664 \<^rule_thm>\<open>divide_divide_eq_left\<close>,
665 (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
666 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e")
668 scr = Rule.Empty_Prog
671 (*.contains absolute minimum of thms for context in norm_Rational.*)
672 val reduce_0_1_2 = prep_rls'(
673 Rule_Def.Repeat{id = "reduce_0_1_2", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
674 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
675 rules = [(*\<^rule_thm>\<open>divide_1\<close>,
676 "?x / 1 = ?x" unnecess.for normalform*)
677 \<^rule_thm>\<open>mult_1_left\<close>,
679 (*\<^rule_thm>\<open>real_mult_minus1\<close>,
681 (*\<^rule_thm>\<open>real_minus_mult_cancel\<close>,
682 "- ?x * - ?y = ?x * ?y"*)
684 \<^rule_thm>\<open>mult_zero_left\<close>,
686 \<^rule_thm>\<open>add_0_left\<close>,
688 (*\<^rule_thm>\<open>right_minus\<close>,
691 \<^rule_thm_sym>\<open>real_mult_2\<close>,
692 (*"z1 + z1 = 2 * z1"*)
693 \<^rule_thm>\<open>real_mult_2_assoc\<close>,
694 (*"z1 + (z1 + k) = 2 * z1 + k"*)
696 \<^rule_thm>\<open>division_ring_divide_zero\<close>
698 ], scr = Rule.Empty_Prog});
700 (*erls for calculate_Rational;
701 make local with FIXX@ME result:term *term list WN0609???SKMG*)
702 val norm_rat_erls = prep_rls'(
703 Rule_Def.Repeat {id = "norm_rat_erls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
704 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
705 rules = [\<^rule_eval>\<open>Prog_Expr.is_const\<close> (Prog_Expr.eval_const "#is_const_")
706 ], scr = Rule.Empty_Prog});
708 (* consists of rls containing the absolute minimum of thms *)
709 (*040209: this version has been used by RL for his equations,
710 which is now replaced by MGs version "norm_Rational" below *)
711 val norm_Rational_min = prep_rls'(
712 Rule_Def.Repeat {id = "norm_Rational_min", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
713 erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
714 rules = [(*sequence given by operator precedence*)
715 Rule.Rls_ discard_minus,
717 Rule.Rls_ rat_mult_divide,
719 Rule.Rls_ reduce_0_1_2,
720 Rule.Rls_ order_add_mult,
721 Rule.Rls_ collect_numerals,
722 Rule.Rls_ add_fractions_p,
725 scr = Rule.Empty_Prog});
727 val norm_Rational_parenthesized = prep_rls'(
728 Rule_Set.Sequence {id = "norm_Rational_parenthesized", preconds = []:term list,
729 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
730 erls = Atools_erls, srls = Rule_Set.Empty,
731 calc = [], errpatts = [],
732 rules = [Rule.Rls_ norm_Rational_min,
733 Rule.Rls_ discard_parentheses
735 scr = Rule.Empty_Prog});
737 (*WN030318???SK: simplifies all but cancel and common_nominator*)
738 val simplify_rational =
739 Rule_Set.merge "simplify_rational" expand_binoms
740 (Rule_Set.append_rules "divide" calculate_Rational
741 [\<^rule_thm>\<open>div_by_1\<close>,
743 \<^rule_thm>\<open>rat_mult\<close>,
744 (*(1)"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
745 \<^rule_thm>\<open>times_divide_eq_right\<close>,
746 (*(2)"?a * (?c / ?d) = ?a * ?c / ?d" must be [2],
747 otherwise inv.to a / b / c = ...*)
748 \<^rule_thm>\<open>times_divide_eq_left\<close>,
749 (*"?a / ?b * ?c = ?a * ?c / ?b"*)
750 \<^rule_thm>\<open>add_minus\<close>,
751 (*"?a + ?b - ?b = ?a"*)
752 \<^rule_thm>\<open>add_minus1\<close>,
753 (*"?a - ?b + ?b = ?a"*)
754 \<^rule_thm>\<open>divide_minus1\<close>
759 val add_fractions_p_rls = prep_rls'(
760 Rule_Def.Repeat {id = "add_fractions_p_rls", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
761 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
762 rules = [Rule.Rls_ add_fractions_p],
763 scr = Rule.Empty_Prog});
765 (* "Rule_Def.Repeat" causes repeated application of cancel_p to one and the same term *)
766 val cancel_p_rls = prep_rls'(
768 {id = "cancel_p_rls", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
769 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
770 rules = [Rule.Rls_ cancel_p],
771 scr = Rule.Empty_Prog});
773 (*. makes 'normal' fractions; 'is_polyexp' inhibits double fractions;
774 used in initial part norm_Rational_mg, see example DA-M02-main.p.60.*)
775 val rat_mult_poly = prep_rls'(
776 Rule_Def.Repeat {id = "rat_mult_poly", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
777 erls = Rule_Set.append_rules "Rule_Set.empty-is_polyexp" Rule_Set.empty
778 [\<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp "")],
779 srls = Rule_Set.Empty, calc = [], errpatts = [],
781 [\<^rule_thm>\<open>rat_mult_poly_l\<close>,
782 (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*)
783 \<^rule_thm>\<open>rat_mult_poly_r\<close>
784 (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*) ],
785 scr = Rule.Empty_Prog});
787 (*. makes 'normal' fractions; 'is_polyexp' inhibits double fractions;
788 used in looping part norm_Rational_rls, see example DA-M02-main.p.60
789 .. WHERE THE LATTER DOES ALWAYS WORK, BECAUSE erls = Rule_Set.empty,
790 I.E. THE RESPECTIVE ASSUMPTION IS STORED AND Rule.Thm APPLIED; WN051028
792 val rat_mult_div_pow = prep_rls'(
793 Rule_Def.Repeat {id = "rat_mult_div_pow", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
794 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
795 rules = [\<^rule_thm>\<open>rat_mult\<close>,
796 (*"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
797 \<^rule_thm>\<open>rat_mult_poly_l\<close>,
798 (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*)
799 \<^rule_thm>\<open>rat_mult_poly_r\<close>,
800 (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*)
802 \<^rule_thm>\<open>real_divide_divide1_mg\<close>,
803 (*"y ~= 0 ==> (u / v) / (y / z) = (u * z) / (y * v)"*)
804 \<^rule_thm>\<open>divide_divide_eq_right\<close>,
805 (*"?x / (?y / ?z) = ?x * ?z / ?y"*)
806 \<^rule_thm>\<open>divide_divide_eq_left\<close>,
807 (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
808 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
810 \<^rule_thm>\<open>rat_power\<close>
811 (*"(?a / ?b) \<up> ?n = ?a \<up> ?n / ?b \<up> ?n"*)
813 scr = Rule.Empty_Prog});
815 val rat_reduce_1 = prep_rls'(
816 Rule_Def.Repeat {id = "rat_reduce_1", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
817 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
819 [\<^rule_thm>\<open>div_by_1\<close>,
821 \<^rule_thm>\<open>mult_1_left\<close>
824 scr = Rule.Empty_Prog});
826 (* looping part of norm_Rational *)
827 val norm_Rational_rls = prep_rls' (
828 Rule_Def.Repeat {id = "norm_Rational_rls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
829 erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
830 rules = [Rule.Rls_ add_fractions_p_rls,
831 Rule.Rls_ rat_mult_div_pow,
832 Rule.Rls_ make_rat_poly_with_parentheses,
833 Rule.Rls_ cancel_p_rls,
834 Rule.Rls_ rat_reduce_1
836 scr = Rule.Empty_Prog});
838 val norm_Rational = prep_rls' (
840 {id = "norm_Rational", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
841 erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
842 rules = [Rule.Rls_ discard_minus,
843 Rule.Rls_ rat_mult_poly, (* removes double fractions like a/b/c *)
844 Rule.Rls_ make_rat_poly_with_parentheses,
845 Rule.Rls_ cancel_p_rls,
846 Rule.Rls_ norm_Rational_rls, (* the main rls, looping (#) *)
847 Rule.Rls_ discard_parentheses1 (* mult only *)
849 scr = Rule.Empty_Prog});
853 calculate_Rational = calculate_Rational and
854 calc_rat_erls = calc_rat_erls and
855 rational_erls = rational_erls and
856 cancel_p = cancel_p and
857 add_fractions_p = add_fractions_p and
859 add_fractions_p_rls = add_fractions_p_rls and
860 powers_erls = powers_erls and
862 rat_mult_divide = rat_mult_divide and
863 reduce_0_1_2 = reduce_0_1_2 and
865 rat_reduce_1 = rat_reduce_1 and
866 norm_rat_erls = norm_rat_erls and
867 norm_Rational = norm_Rational and
868 norm_Rational_rls = norm_Rational_rls and
869 norm_Rational_min = norm_Rational_min and
870 norm_Rational_parenthesized = norm_Rational_parenthesized and
872 rat_mult_poly = rat_mult_poly and
873 rat_mult_div_pow = rat_mult_div_pow and
874 cancel_p_rls = cancel_p_rls
876 section \<open>A problem for simplification of rationals\<close>
878 problem pbl_simp_rat : "rational/simplification" =
879 \<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)]\<close>
880 Method: "simplification/of_rationals"
883 Where: "t_t is_ratpolyexp"
884 Find: "normalform n_n"
886 section \<open>A methods for simplification of rationals\<close>
887 (*WN061025 this methods script is copied from (auto-generated) script
888 of norm_Rational in order to ease repair on inform*)
890 partial_function (tailrec) simplify :: "real \<Rightarrow> real"
893 (Try (Rewrite_Set ''discard_minus'') #>
894 Try (Rewrite_Set ''rat_mult_poly'') #>
895 Try (Rewrite_Set ''make_rat_poly_with_parentheses'') #>
896 Try (Rewrite_Set ''cancel_p_rls'') #>
898 Try (Rewrite_Set ''add_fractions_p_rls'') #>
899 Try (Rewrite_Set ''rat_mult_div_pow'') #>
900 Try (Rewrite_Set ''make_rat_poly_with_parentheses'') #>
901 Try (Rewrite_Set ''cancel_p_rls'') #>
902 Try (Rewrite_Set ''rat_reduce_1''))) #>
903 Try (Rewrite_Set ''discard_parentheses1''))
907 method met_simp_rat : "simplification/of_rationals" =
908 \<open>{rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
909 prls = Rule_Set.append_rules "simplification_of_rationals_prls" Rule_Set.empty
910 [(*for preds in where_*) \<^rule_eval>\<open>is_ratpolyexp\<close> (eval_is_ratpolyexp "")],
911 crls = Rule_Set.empty, errpats = [], nrls = norm_Rational_rls}\<close>
912 Program: simplify.simps
914 Where: "t_t is_ratpolyexp"
915 Find: "normalform n_n"