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 ("Groups.plus_class.plus",_) $ Free _ $ Free _) = true
26 | is_ratpolyexp (Const ("Groups.minus_class.minus",_) $ Free _ $ Free _) = true
27 | is_ratpolyexp (Const ("Groups.times_class.times",_) $ Free _ $ Free _) = true
28 | is_ratpolyexp (Const ("Transcendental.powr",_) $ Free _ $ Free _) = true
29 | is_ratpolyexp (Const ("Rings.divide_class.divide",_) $ Free _ $ Free _) = true
30 | is_ratpolyexp (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
31 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
32 | is_ratpolyexp (Const ("Groups.minus_class.minus",_) $ t1 $ t2) =
33 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
34 | is_ratpolyexp (Const ("Groups.times_class.times",_) $ t1 $ t2) =
35 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
36 | is_ratpolyexp (Const ("Transcendental.powr",_) $ t1 $ t2) =
37 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
38 | is_ratpolyexp (Const ("Rings.divide_class.divide",_) $ 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 ("Rings.divide_class.divide", _) $ _(*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 ("Rings.divide_class.divide", _) $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 (Const ("Num.numeral_class.numeral", _) $ _)) =
128 then (t |> HOLogic.dest_number |> snd |> string_of_int
129 |> TermC.int_opt_of_string |> the |> curry op * c, es) (*several numerals in one monom*)
130 else (c, list_update es (find_index (curry op = t) vs) 1)
131 | monom_of_term vs (c, es) (Const ("Transcendental.powr", _) $
132 (t as (Const ("Num.numeral_class.numeral", _) $ _)) $
133 (Const ("Num.numeral_class.numeral", _) $ num)) =
134 (c, list_update es (find_index (curry op = t) vs) (num |> HOLogic.dest_numeral))
135 | monom_of_term vs (c, es) (Const ("Groups.times_class.times", _) $ m1 $ m2) =
136 let val (c', es') = monom_of_term vs (c, es) m1
137 in monom_of_term vs (c', es') m2 end
138 | monom_of_term _ _ t = raise ERROR ("poly malformed 1 with " ^ UnparseC.term t)
140 fun monoms_of_term vs (t as Const _) =
141 [monom_of_term vs (1, replicate (length vs) 0) t]
142 | monoms_of_term vs (t as Free _) =
143 [monom_of_term vs (1, replicate (length vs) 0) t]
144 | monoms_of_term vs (t as Const ("Transcendental.powr", _) $ _ $ _) =
145 [monom_of_term vs (1, replicate (length vs) 0) t]
146 | monoms_of_term vs (t as Const ("Groups.times_class.times", _) $ _ $ _) =
147 [monom_of_term vs (1, replicate (length vs) 0) t]
148 | monoms_of_term vs (Const ("Groups.plus_class.plus", _) $ ms1 $ ms2) =
149 (monoms_of_term vs ms1) @ (monoms_of_term vs ms2)
150 | monoms_of_term _ t = raise ERROR ("poly malformed 2 with " ^ UnparseC.term t)
152 (* convert a term to the internal representation of a multivariate polynomial;
153 the conversion is quite liberal, see test --- fun poly_of_term ---:
154 * the order of variables and the parentheses within a monomial are arbitrary
155 * the coefficient may be somewhere
156 * he order and the parentheses within monomials are arbitrary
157 But the term must be completely expand + over * (laws of distributivity are not applicable).
159 The function requires the free variables as strings already given,
160 because the gcd involves 2 polynomials (with the same length for their list of exponents).
162 fun poly_of_term vs (t as Const ("Groups.plus_class.plus", _) $ _ $ _) =
163 (SOME (t |> monoms_of_term vs |> order)
164 handle ERROR _ => NONE)
165 | poly_of_term vs t =
166 (SOME [monom_of_term vs (1, replicate (length vs) 0) t]
167 handle ERROR _ => NONE)
171 val vs = TermC.vars_of t
173 case poly_of_term vs t of SOME _ => true | NONE => false
175 val is_expanded = is_poly (* TODO: check names *)
176 val is_polynomial = is_poly (* TODO: check names *)
179 subsubsection \<open>Convert internal representation of a multivariate polynomial to a term\<close>
181 fun term_of_es _ _ _ [] = [] (*assumes same length for vs and es*)
182 | term_of_es baseT expT (_ :: vs) (0 :: es) = [] @ term_of_es baseT expT vs es
183 | term_of_es baseT expT (v :: vs) (1 :: es) = v :: term_of_es baseT expT vs es
184 | term_of_es baseT expT (v :: vs) (e :: es) =
185 Const ("Transcendental.powr", [baseT, expT] ---> baseT) $ v $ (HOLogic.mk_number expT e)
186 :: term_of_es baseT expT vs es
187 | term_of_es _ _ _ _ = raise ERROR "term_of_es: length vs <> length es"
189 fun term_of_monom baseT expT vs ((c, es): monom) =
190 let val es' = term_of_es baseT expT vs es
194 if es' = [] (*if es = [0,0,0,...]*)
195 then HOLogic.mk_number baseT c
196 else foldl (HOLogic.mk_binop "Groups.times_class.times") (hd es', tl es')
197 else foldl (HOLogic.mk_binop "Groups.times_class.times")
198 (HOLogic.mk_number baseT c, es')
201 fun term_of_poly baseT expT vs p =
202 let val monos = map (term_of_monom baseT expT vs) p
203 in foldl (HOLogic.mk_binop "Groups.plus_class.plus") (hd monos, tl monos) end
206 subsection \<open>Apply gcd_poly for cancelling and adding fractions as terms\<close>
208 fun mk_noteq_0 baseT t =
209 Const ("HOL.Not", HOLogic.boolT --> HOLogic.boolT) $
210 (Const ("HOL.eq", [baseT, baseT] ---> HOLogic.boolT) $ t $ HOLogic.mk_number HOLogic.realT 0)
212 fun mk_asms baseT ts =
213 let val as' = filter_out TermC.is_num ts (* asm like "2 ~= 0" is needless *)
214 in map (mk_noteq_0 baseT) as' end
217 subsubsection \<open>Factor out gcd for cancellation\<close>
219 fun check_fraction t =
221 Const ("Rings.divide_class.divide", _) $ numerator $ denominator
222 => SOME (numerator, denominator)
225 (* prepare a term for cancellation by factoring out the gcd
226 assumes: is a fraction with outmost "/"*)
227 fun factout_p_ (thy: theory) t =
228 let val opt = check_fraction t
232 | SOME (numerator, denominator) =>
234 val vs = TermC.vars_of t
235 val baseT = type_of numerator
236 val expT = HOLogic.realT
238 case (poly_of_term vs numerator, poly_of_term vs denominator) of
241 val ((a', b'), c) = gcd_poly a b
242 val es = replicate (length vs) 0
244 if c = [(1, es)] orelse c = [(~1, es)]
248 val b't = term_of_poly baseT expT vs b'
249 val ct = term_of_poly baseT expT vs c
251 HOLogic.mk_binop "Rings.divide_class.divide"
252 (HOLogic.mk_binop "Groups.times_class.times"
253 (term_of_poly baseT expT vs a', ct),
254 HOLogic.mk_binop "Groups.times_class.times" (b't, ct))
255 in SOME (t', mk_asms baseT [b't, ct]) end
257 | _ => NONE : (term * term list) option
262 subsubsection \<open>Cancel a fraction\<close>
264 (* cancel a term by the gcd ("" denote terms with internal algebraic structure)
265 cancel_p_ :: theory \<Rightarrow> term \<Rightarrow> (term \<times> term list) option
266 cancel_p_ thy "a / b" = SOME ("a' / b'", ["b' \<noteq> 0"])
267 assumes: a is_polynomial \<and> b is_polynomial \<and> b \<noteq> 0
269 SOME ("a' / b'", ["b' \<noteq> 0"]). gcd_poly a b \<noteq> 1 \<and> gcd_poly a b \<noteq> -1 \<and>
270 a' * gcd_poly a b = a \<and> b' * gcd_poly a b = b
272 fun cancel_p_ (_: theory) t =
273 let val opt = check_fraction t
277 | SOME (numerator, denominator) =>
279 val vs = TermC.vars_of t
280 val baseT = type_of numerator
281 val expT = HOLogic.realT
283 case (poly_of_term vs numerator, poly_of_term vs denominator) of
286 val ((a', b'), c) = gcd_poly a b
287 val es = replicate (length vs) 0
289 if c = [(1, es)] orelse c = [(~1, es)]
293 val bt' = term_of_poly baseT expT vs b'
294 val ct = term_of_poly baseT expT vs c
296 HOLogic.mk_binop "Rings.divide_class.divide"
297 (term_of_poly baseT expT vs a', bt')
298 val asm = mk_asms baseT [bt']
299 in SOME (t', asm) end
301 | _ => NONE : (term * term list) option
306 subsubsection \<open>Factor out to a common denominator for addition\<close>
308 (* addition of fractions allows (at most) one non-fraction (a monomial) *)
310 (Const ("Groups.plus_class.plus", _) $
311 (Const ("Rings.divide_class.divide", _) $ n1 $ d1) $
312 (Const ("Rings.divide_class.divide", _) $ n2 $ d2))
313 = SOME ((n1, d1), (n2, d2))
315 (Const ("Groups.plus_class.plus", _) $
317 (Const ("Rings.divide_class.divide", _) $ n2 $ d2))
318 = SOME ((nofrac, HOLogic.mk_number HOLogic.realT 1), (n2, d2))
320 (Const ("Groups.plus_class.plus", _) $
321 (Const ("Rings.divide_class.divide", _) $ n1 $ d1) $
323 = SOME ((n1, d1), (nofrac, HOLogic.mk_number HOLogic.realT 1))
324 | check_frac_sum _ = NONE
326 (* prepare a term for addition by providing the least common denominator as a product
327 assumes: is a term with outmost "+" and at least one outmost "/" in respective summands*)
328 fun common_nominator_p_ (_: theory) t =
329 let val opt = check_frac_sum t
333 | SOME ((n1, d1), (n2, d2)) =>
335 val vs = TermC.vars_of t
337 case (poly_of_term vs d1, poly_of_term vs d2) of
340 val ((a', b'), c) = gcd_poly a b
341 val (baseT, expT) = (type_of n1, HOLogic.realT)
342 val [d1', d2', c'] = map (term_of_poly baseT expT vs) [a', b', c]
343 (*----- minimum of parentheses & nice result, but breaks tests: -------------
344 val denom = HOLogic.mk_binop "Groups.times_class.times"
345 (HOLogic.mk_binop "Groups.times_class.times" (d1', d2'), c') -------------*)
347 if c = [(1, replicate (length vs) 0)]
348 then HOLogic.mk_binop "Groups.times_class.times" (d1', d2')
350 HOLogic.mk_binop "Groups.times_class.times" (c',
351 HOLogic.mk_binop "Groups.times_class.times" (d1', d2')) (*--------------*)
353 HOLogic.mk_binop "Groups.plus_class.plus"
354 (HOLogic.mk_binop "Rings.divide_class.divide"
355 (HOLogic.mk_binop "Groups.times_class.times" (n1, d2'), denom),
356 HOLogic.mk_binop "Rings.divide_class.divide"
357 (HOLogic.mk_binop "Groups.times_class.times" (n2, d1'), denom))
358 val asm = mk_asms baseT [d1', d2', c']
359 in SOME (t', asm) end
360 | _ => NONE : (term * term list) option
365 subsubsection \<open>Addition of at least one fraction within a sum\<close>
368 assumes: is a term with outmost "+" and at least one outmost "/" in respective summands
369 NOTE: the case "(_ + _) + _" need not be considered due to iterated addition.*)
370 fun add_fraction_p_ (_: theory) t =
371 case check_frac_sum t of
373 | SOME ((n1, d1), (n2, d2)) =>
375 val vs = TermC.vars_of t
377 case (poly_of_term vs n1, poly_of_term vs d1, poly_of_term vs n2, poly_of_term vs d2) of
378 (SOME _, SOME a, SOME _, SOME b) =>
380 val ((a', b'), c) = gcd_poly a b
381 val (baseT, expT) = (type_of n1, HOLogic.realT)
382 val nomin = term_of_poly baseT expT vs
383 (((the (poly_of_term vs n1)) %%*%% b') %%+%% ((the (poly_of_term vs n2)) %%*%% a'))
384 val denom = term_of_poly baseT expT vs ((c %%*%% a') %%*%% b')
385 val t' = HOLogic.mk_binop "Rings.divide_class.divide" (nomin, denom)
386 in SOME (t', mk_asms baseT [denom]) end
387 | _ => NONE : (term * term list) option
391 section \<open>Embed cancellation and addition into rewriting\<close>
392 ML \<open>val thy = @{theory}\<close>
393 subsection \<open>Rulesets and predicate for embedding\<close>
395 (* evaluates conditions in calculate_Rational *)
398 (Rule_Def.Repeat {id = "calc_rat_erls", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
399 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
401 [Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
402 Rule.Eval ("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_"),
403 Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
404 Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false})],
405 scr = Rule.Empty_Prog});
407 (* simplifies expressions with numerals;
408 does NOT rearrange the term by AC-rewriting; thus terms with variables
409 need to have constants to be commuted together respectively *)
410 val calculate_Rational =
411 prep_rls' (Rule_Set.merge "calculate_Rational"
412 (Rule_Def.Repeat {id = "divide", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
413 erls = calc_rat_erls, srls = Rule_Set.Empty,
414 calc = [], errpatts = [],
416 [Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),
418 Rule.Thm ("minus_divide_left", ThmC.numerals_to_Free (@{thm minus_divide_left} RS @{thm sym})),
419 (*SYM - ?x / ?y = - (?x / ?y) may come from subst*)
420 Rule.Thm ("rat_add", ThmC.numerals_to_Free @{thm rat_add}),
421 (*"[| a is_const; b is_const; c is_const; d is_const |] ==> \
422 \a / c + b / d = (a * d) / (c * d) + (b * c ) / (d * c)"*)
423 Rule.Thm ("rat_add1", ThmC.numerals_to_Free @{thm rat_add1}),
424 (*"[| a is_const; b is_const; c is_const |] ==> a / c + b / c = (a + b) / c"*)
425 Rule.Thm ("rat_add2", ThmC.numerals_to_Free @{thm rat_add2}),
426 (*"[| ?a is_const; ?b is_const; ?c is_const |] ==> ?a / ?c + ?b = (?a + ?b * ?c) / ?c"*)
427 Rule.Thm ("rat_add3", ThmC.numerals_to_Free @{thm rat_add3}),
428 (*"[| a is_const; b is_const; c is_const |] ==> a + b / c = (a * c) / c + b / c"\
429 .... is_const to be omitted here FIXME*)
431 Rule.Thm ("rat_mult", ThmC.numerals_to_Free @{thm rat_mult}),
432 (*a / b * (c / d) = a * c / (b * d)*)
433 Rule.Thm ("times_divide_eq_right", ThmC.numerals_to_Free @{thm times_divide_eq_right}),
434 (*?x * (?y / ?z) = ?x * ?y / ?z*)
435 Rule.Thm ("times_divide_eq_left", ThmC.numerals_to_Free @{thm times_divide_eq_left}),
436 (*?y / ?z * ?x = ?y * ?x / ?z*)
438 Rule.Thm ("real_divide_divide1", ThmC.numerals_to_Free @{thm real_divide_divide1}),
439 (*"?y ~= 0 ==> ?u / ?v / (?y / ?z) = ?u / ?v * (?z / ?y)"*)
440 Rule.Thm ("divide_divide_eq_left", ThmC.numerals_to_Free @{thm divide_divide_eq_left}),
441 (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
443 Rule.Thm ("rat_power", ThmC.numerals_to_Free @{thm rat_power}),
444 (*"(?a / ?b) \<up> ?n = ?a \<up> ?n / ?b \<up> ?n"*)
446 Rule.Thm ("mult_cross", ThmC.numerals_to_Free @{thm mult_cross}),
447 (*"[| b ~= 0; d ~= 0 |] ==> (a / b = c / d) = (a * d = b * c)*)
448 Rule.Thm ("mult_cross1", ThmC.numerals_to_Free @{thm mult_cross1}),
449 (*" b ~= 0 ==> (a / b = c ) = (a = b * c)*)
450 Rule.Thm ("mult_cross2", ThmC.numerals_to_Free @{thm mult_cross2})
451 (*" d ~= 0 ==> (a = c / d) = (a * d = c)*)],
452 scr = Rule.Empty_Prog})
455 (*("is_expanded", ("Rational.is_expanded", eval_is_expanded ""))*)
456 fun eval_is_expanded (thmid:string) _
457 (t as (Const("Rational.is_expanded", _) $ arg)) thy =
459 then SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",
460 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
461 else SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",
462 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
463 | eval_is_expanded _ _ _ _ = NONE;
465 setup \<open>KEStore_Elems.add_calcs
466 [("is_expanded", ("Rational.is_expanded", eval_is_expanded ""))]\<close>
469 Rule_Set.merge "rational_erls" calculate_Rational
470 (Rule_Set.append_rules "is_expanded" Atools_erls
471 [Rule.Eval ("Rational.is_expanded", eval_is_expanded "")]);
474 subsection \<open>Embed cancellation into rewriting\<close>
476 (**)local (* cancel_p *)
478 val {rules = rules, rew_ord = (_, ro), ...} = Rule_Set.rep (assoc_rls' @{theory} "rev_rew_p");
480 fun init_state thy eval_rls ro t =
482 val SOME (t', _) = factout_p_ thy t;
483 val SOME (t'', asm) = cancel_p_ thy t;
484 val der = Derive.steps_reverse thy eval_rls rules ro NONE t';
486 [(Rule.Thm ("real_mult_div_cancel2", ThmC.numerals_to_Free @{thm real_mult_div_cancel2}), (t'', asm))]
487 val rs = (Rule.distinct' o (map #1)) der
488 val rs = filter_out (ThmC.member'
489 ["sym_real_add_zero_left", "sym_real_mult_0", "sym_real_mult_1"]) rs
490 in (t, t'', [rs(*one in order to ease locate_rule*)], der) end;
492 fun locate_rule thy eval_rls ro [rs] t r =
493 if member op = ((map (Rule.thm_id)) rs) (Rule.thm_id r)
495 let val ropt = Rewrite.rewrite_ thy ro eval_rls true (Rule.thm r) t;
497 case ropt of SOME ta => [(r, ta)]
499 ("### locate_rule: rewrite " ^ Rule.thm_id r ^ " " ^ UnparseC.term t ^ " = NONE");*) [])
501 else ((*tracing ("### locate_rule: " ^ Rule.thm_id r ^ " not mem rrls");*) [])
502 | locate_rule _ _ _ _ _ _ = raise ERROR "locate_rule: doesnt match rev-sets in istate";
504 fun next_rule thy eval_rls ro [rs] t =
506 val der = Derive.do_one thy eval_rls rs ro NONE t;
507 in case der of (_, r, _) :: _ => SOME r | _ => NONE end
508 | next_rule _ _ _ _ _ = raise ERROR ("next_rule: doesnt match rev-sets in istate");
510 fun attach_form (_: Rule.rule list list) (_: term) (_: term) =
511 [(*TODO*)]: ( Rule.rule * (term * term list)) list;
516 Rule_Set.Rrls {id = "cancel_p", prepat = [],
517 rew_ord=("ord_make_polynomial", ord_make_polynomial false thy),
518 erls = rational_erls,
520 [("PLUS", ("Groups.plus_class.plus", (**)eval_binop "#add_")),
521 ("TIMES" , ("Groups.times_class.times", (**)eval_binop "#mult_")),
522 ("DIVIDE", ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")),
523 ("POWER", ("Transcendental.powr", (**)eval_binop "#power_"))],
526 Rule.Rfuns {init_state = init_state thy Atools_erls ro,
527 normal_form = cancel_p_ thy,
528 locate_rule = locate_rule thy Atools_erls ro,
529 next_rule = next_rule thy Atools_erls ro,
530 attach_form = attach_form}}
531 (**)end(* local cancel_p *)
534 subsection \<open>Embed addition into rewriting\<close>
536 (**)local (* add_fractions_p *)
538 (*val {rules = rules, rew_ord = (_, ro), ...} = Rule_Set.rep (assoc_rls "make_polynomial");*)
539 val {rules, rew_ord=(_,ro),...} = Rule_Set.rep (assoc_rls' @{theory} "rev_rew_p");
541 fun init_state thy eval_rls ro t =
543 val SOME (t',_) = common_nominator_p_ thy t;
544 val SOME (t'', asm) = add_fraction_p_ thy t;
545 val der = Derive.steps_reverse thy eval_rls rules ro NONE t';
547 [(Rule.Thm ("real_mult_div_cancel2", ThmC.numerals_to_Free @{thm real_mult_div_cancel2}), (t'',asm))]
548 val rs = (Rule.distinct' o (map #1)) der;
549 val rs = filter_out (ThmC.member'
550 ["sym_real_add_zero_left", "sym_real_mult_0", "sym_real_mult_1"]) rs;
551 in (t, t'', [rs(*here only _ONE_*)], der) end;
553 fun locate_rule thy eval_rls ro [rs] t r =
554 if member op = ((map (Rule.thm_id)) rs) (Rule.thm_id r)
556 let val ropt = Rewrite.rewrite_ thy ro eval_rls true (Rule.thm r) t;
561 ((*tracing ("### locate_rule: rewrite " ^ Rule.thm_id r ^ " " ^ UnparseC.term t ^ " = NONE");*)
563 else ((*tracing ("### locate_rule: " ^ Rule.thm_id r ^ " not mem rrls");*) [])
564 | locate_rule _ _ _ _ _ _ = raise ERROR "locate_rule: doesnt match rev-sets in istate";
566 fun next_rule thy eval_rls ro [rs] t =
567 let val der = Derive.do_one thy eval_rls rs ro NONE t;
573 | next_rule _ _ _ _ _ = raise ERROR ("next_rule: doesnt match rev-sets in istate");
575 val pat0 = TermC.parse_patt thy "?r/?s+?u/?v :: real";
576 val pat1 = TermC.parse_patt thy "?r/?s+?u :: real";
577 val pat2 = TermC.parse_patt thy "?r +?u/?v :: real";
578 val prepat = [([@{term True}], pat0),
579 ([@{term True}], pat1),
580 ([@{term True}], pat2)];
583 val add_fractions_p =
584 Rule_Set.Rrls {id = "add_fractions_p", prepat=prepat,
585 rew_ord = ("ord_make_polynomial", ord_make_polynomial false thy),
586 erls = rational_erls,
587 calc = [("PLUS", ("Groups.plus_class.plus", (**)eval_binop "#add_")),
588 ("TIMES", ("Groups.times_class.times", (**)eval_binop "#mult_")),
589 ("DIVIDE", ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")),
590 ("POWER", ("Transcendental.powr", (**)eval_binop "#power_"))],
592 scr = Rule.Rfuns {init_state = init_state thy Atools_erls ro,
593 normal_form = add_fraction_p_ thy,
594 locate_rule = locate_rule thy Atools_erls ro,
595 next_rule = next_rule thy Atools_erls ro,
596 attach_form = attach_form}}
597 (**)end(*local add_fractions_p *)
600 subsection \<open>Cancelling and adding all occurrences in a term /////////////////////////////\<close>
602 (*copying cancel_p_rls + add her caused error in interface.sml*)
605 section \<open>Rulesets for general simplification\<close>
607 (*erls for calculate_Rational; make local with FIXX@ME result:term *term list*)
608 val powers_erls = prep_rls'(
609 Rule_Def.Repeat {id = "powers_erls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
610 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
611 rules = [Rule.Eval ("Prog_Expr.is_atom", Prog_Expr.eval_is_atom "#is_atom_"),
612 Rule.Eval ("Prog_Expr.is_even", Prog_Expr.eval_is_even "#is_even_"),
613 Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
614 Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false}),
615 Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
616 Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_")
618 scr = Rule.Empty_Prog
620 (*.all powers over + distributed; atoms over * collected, other distributed
621 contains absolute minimum of thms for context in norm_Rational .*)
622 val powers = prep_rls'(
623 Rule_Def.Repeat {id = "powers", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
624 erls = powers_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
625 rules = [Rule.Thm ("realpow_multI", ThmC.numerals_to_Free @{thm realpow_multI}),
626 (*"(r * s) \<up> n = r \<up> n * s \<up> n"*)
627 Rule.Thm ("realpow_pow",ThmC.numerals_to_Free @{thm realpow_pow}),
628 (*"(a \<up> b) \<up> c = a \<up> (b * c)"*)
629 Rule.Thm ("realpow_oneI",ThmC.numerals_to_Free @{thm realpow_oneI}),
631 Rule.Thm ("realpow_minus_even",ThmC.numerals_to_Free @{thm realpow_minus_even}),
632 (*"n is_even ==> (- r) \<up> n = r \<up> n" ?-->discard_minus?*)
633 Rule.Thm ("realpow_minus_odd",ThmC.numerals_to_Free @{thm realpow_minus_odd}),
634 (*"Not (n is_even) ==> (- r) \<up> n = -1 * r \<up> n"*)
636 (*----- collect atoms over * -----*)
637 Rule.Thm ("realpow_two_atom",ThmC.numerals_to_Free @{thm realpow_two_atom}),
638 (*"r is_atom ==> r * r = r \<up> 2"*)
639 Rule.Thm ("realpow_plus_1",ThmC.numerals_to_Free @{thm realpow_plus_1}),
640 (*"r is_atom ==> r * r \<up> n = r \<up> (n + 1)"*)
641 Rule.Thm ("realpow_addI_atom",ThmC.numerals_to_Free @{thm realpow_addI_atom}),
642 (*"r is_atom ==> r \<up> n * r \<up> m = r \<up> (n + m)"*)
644 (*----- distribute none-atoms -----*)
645 Rule.Thm ("realpow_def_atom",ThmC.numerals_to_Free @{thm realpow_def_atom}),
646 (*"[| 1 < n; ~ (r is_atom) |]==>r \<up> n = r * r \<up> (n + -1)"*)
647 Rule.Thm ("realpow_eq_oneI",ThmC.numerals_to_Free @{thm realpow_eq_oneI}),
649 Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_")
651 scr = Rule.Empty_Prog
653 (*.contains absolute minimum of thms for context in norm_Rational.*)
654 val rat_mult_divide = prep_rls'(
655 Rule_Def.Repeat {id = "rat_mult_divide", preconds = [],
656 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
657 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
658 rules = [Rule.Thm ("rat_mult",ThmC.numerals_to_Free @{thm rat_mult}),
659 (*(1)"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
660 Rule.Thm ("times_divide_eq_right",ThmC.numerals_to_Free @{thm times_divide_eq_right}),
661 (*(2)"?a * (?c / ?d) = ?a * ?c / ?d" must be [2],
662 otherwise inv.to a / b / c = ...*)
663 Rule.Thm ("times_divide_eq_left",ThmC.numerals_to_Free @{thm times_divide_eq_left}),
664 (*"?a / ?b * ?c = ?a * ?c / ?b" order weights x \<up> n too much
665 and does not commute a / b * c \<up> 2 !*)
667 Rule.Thm ("divide_divide_eq_right",
668 ThmC.numerals_to_Free @{thm divide_divide_eq_right}),
669 (*"?x / (?y / ?z) = ?x * ?z / ?y"*)
670 Rule.Thm ("divide_divide_eq_left",
671 ThmC.numerals_to_Free @{thm divide_divide_eq_left}),
672 (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
673 Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")
675 scr = Rule.Empty_Prog
678 (*.contains absolute minimum of thms for context in norm_Rational.*)
679 val reduce_0_1_2 = prep_rls'(
680 Rule_Def.Repeat{id = "reduce_0_1_2", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
681 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
682 rules = [(*Rule.Thm ("divide_1",ThmC.numerals_to_Free @{thm divide_1}),
683 "?x / 1 = ?x" unnecess.for normalform*)
684 Rule.Thm ("mult_1_left",ThmC.numerals_to_Free @{thm mult_1_left}),
686 (*Rule.Thm ("real_mult_minus1",ThmC.numerals_to_Free @{thm real_mult_minus1}),
688 (*Rule.Thm ("real_minus_mult_cancel",ThmC.numerals_to_Free @{thm real_minus_mult_cancel}),
689 "- ?x * - ?y = ?x * ?y"*)
691 Rule.Thm ("mult_zero_left",ThmC.numerals_to_Free @{thm mult_zero_left}),
693 Rule.Thm ("add_0_left",ThmC.numerals_to_Free @{thm add_0_left}),
695 (*Rule.Thm ("right_minus",ThmC.numerals_to_Free @{thm right_minus}),
698 Rule.Thm ("sym_real_mult_2",
699 ThmC.numerals_to_Free (@{thm real_mult_2} RS @{thm sym})),
700 (*"z1 + z1 = 2 * z1"*)
701 Rule.Thm ("real_mult_2_assoc",ThmC.numerals_to_Free @{thm real_mult_2_assoc}),
702 (*"z1 + (z1 + k) = 2 * z1 + k"*)
704 Rule.Thm ("division_ring_divide_zero",ThmC.numerals_to_Free @{thm division_ring_divide_zero})
706 ], scr = Rule.Empty_Prog});
708 (*erls for calculate_Rational;
709 make local with FIXX@ME result:term *term list WN0609???SKMG*)
710 val norm_rat_erls = prep_rls'(
711 Rule_Def.Repeat {id = "norm_rat_erls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
712 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
713 rules = [Rule.Eval ("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_")
714 ], scr = Rule.Empty_Prog});
716 (* consists of rls containing the absolute minimum of thms *)
717 (*040209: this version has been used by RL for his equations,
718 which is now replaced by MGs version "norm_Rational" below *)
719 val norm_Rational_min = prep_rls'(
720 Rule_Def.Repeat {id = "norm_Rational_min", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
721 erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
722 rules = [(*sequence given by operator precedence*)
723 Rule.Rls_ discard_minus,
725 Rule.Rls_ rat_mult_divide,
727 Rule.Rls_ reduce_0_1_2,
728 Rule.Rls_ order_add_mult,
729 Rule.Rls_ collect_numerals,
730 Rule.Rls_ add_fractions_p,
733 scr = Rule.Empty_Prog});
735 val norm_Rational_parenthesized = prep_rls'(
736 Rule_Set.Sequence {id = "norm_Rational_parenthesized", preconds = []:term list,
737 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
738 erls = Atools_erls, srls = Rule_Set.Empty,
739 calc = [], errpatts = [],
740 rules = [Rule.Rls_ norm_Rational_min,
741 Rule.Rls_ discard_parentheses
743 scr = Rule.Empty_Prog});
745 (*WN030318???SK: simplifies all but cancel and common_nominator*)
746 val simplify_rational =
747 Rule_Set.merge "simplify_rational" expand_binoms
748 (Rule_Set.append_rules "divide" calculate_Rational
749 [Rule.Thm ("div_by_1",ThmC.numerals_to_Free @{thm div_by_1}),
751 Rule.Thm ("rat_mult",ThmC.numerals_to_Free @{thm rat_mult}),
752 (*(1)"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
753 Rule.Thm ("times_divide_eq_right",ThmC.numerals_to_Free @{thm times_divide_eq_right}),
754 (*(2)"?a * (?c / ?d) = ?a * ?c / ?d" must be [2],
755 otherwise inv.to a / b / c = ...*)
756 Rule.Thm ("times_divide_eq_left",ThmC.numerals_to_Free @{thm times_divide_eq_left}),
757 (*"?a / ?b * ?c = ?a * ?c / ?b"*)
758 Rule.Thm ("add_minus",ThmC.numerals_to_Free @{thm add_minus}),
759 (*"?a + ?b - ?b = ?a"*)
760 Rule.Thm ("add_minus1",ThmC.numerals_to_Free @{thm add_minus1}),
761 (*"?a - ?b + ?b = ?a"*)
762 Rule.Thm ("divide_minus1",ThmC.numerals_to_Free @{thm divide_minus1})
767 val add_fractions_p_rls = prep_rls'(
768 Rule_Def.Repeat {id = "add_fractions_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_ add_fractions_p],
771 scr = Rule.Empty_Prog});
773 (* "Rule_Def.Repeat" causes repeated application of cancel_p to one and the same term *)
774 val cancel_p_rls = prep_rls'(
776 {id = "cancel_p_rls", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
777 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
778 rules = [Rule.Rls_ cancel_p],
779 scr = Rule.Empty_Prog});
781 (*. makes 'normal' fractions; 'is_polyexp' inhibits double fractions;
782 used in initial part norm_Rational_mg, see example DA-M02-main.p.60.*)
783 val rat_mult_poly = prep_rls'(
784 Rule_Def.Repeat {id = "rat_mult_poly", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
785 erls = Rule_Set.append_rules "Rule_Set.empty-is_polyexp" Rule_Set.empty [Rule.Eval ("Poly.is_polyexp", eval_is_polyexp "")],
786 srls = Rule_Set.Empty, calc = [], errpatts = [],
788 [Rule.Thm ("rat_mult_poly_l",ThmC.numerals_to_Free @{thm rat_mult_poly_l}),
789 (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*)
790 Rule.Thm ("rat_mult_poly_r",ThmC.numerals_to_Free @{thm rat_mult_poly_r})
791 (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*) ],
792 scr = Rule.Empty_Prog});
794 (*. makes 'normal' fractions; 'is_polyexp' inhibits double fractions;
795 used in looping part norm_Rational_rls, see example DA-M02-main.p.60
796 .. WHERE THE LATTER DOES ALWAYS WORK, BECAUSE erls = Rule_Set.empty,
797 I.E. THE RESPECTIVE ASSUMPTION IS STORED AND Rule.Thm APPLIED; WN051028
799 val rat_mult_div_pow = prep_rls'(
800 Rule_Def.Repeat {id = "rat_mult_div_pow", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
801 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
802 rules = [Rule.Thm ("rat_mult", ThmC.numerals_to_Free @{thm rat_mult}),
803 (*"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
804 Rule.Thm ("rat_mult_poly_l", ThmC.numerals_to_Free @{thm rat_mult_poly_l}),
805 (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*)
806 Rule.Thm ("rat_mult_poly_r", ThmC.numerals_to_Free @{thm rat_mult_poly_r}),
807 (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*)
809 Rule.Thm ("real_divide_divide1_mg", ThmC.numerals_to_Free @{thm real_divide_divide1_mg}),
810 (*"y ~= 0 ==> (u / v) / (y / z) = (u * z) / (y * v)"*)
811 Rule.Thm ("divide_divide_eq_right", ThmC.numerals_to_Free @{thm divide_divide_eq_right}),
812 (*"?x / (?y / ?z) = ?x * ?z / ?y"*)
813 Rule.Thm ("divide_divide_eq_left", ThmC.numerals_to_Free @{thm divide_divide_eq_left}),
814 (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
815 Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),
817 Rule.Thm ("rat_power", ThmC.numerals_to_Free @{thm rat_power})
818 (*"(?a / ?b) \<up> ?n = ?a \<up> ?n / ?b \<up> ?n"*)
820 scr = Rule.Empty_Prog});
822 val rat_reduce_1 = prep_rls'(
823 Rule_Def.Repeat {id = "rat_reduce_1", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
824 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
826 [Rule.Thm ("div_by_1", ThmC.numerals_to_Free @{thm div_by_1}),
828 Rule.Thm ("mult_1_left", ThmC.numerals_to_Free @{thm mult_1_left})
831 scr = Rule.Empty_Prog});
833 (* looping part of norm_Rational *)
834 val norm_Rational_rls = prep_rls' (
835 Rule_Def.Repeat {id = "norm_Rational_rls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
836 erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
837 rules = [Rule.Rls_ add_fractions_p_rls,
838 Rule.Rls_ rat_mult_div_pow,
839 Rule.Rls_ make_rat_poly_with_parentheses,
840 Rule.Rls_ cancel_p_rls,
841 Rule.Rls_ rat_reduce_1
843 scr = Rule.Empty_Prog});
845 val norm_Rational = prep_rls' (
847 {id = "norm_Rational", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
848 erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
849 rules = [Rule.Rls_ discard_minus,
850 Rule.Rls_ rat_mult_poly, (* removes double fractions like a/b/c *)
851 Rule.Rls_ make_rat_poly_with_parentheses,
852 Rule.Rls_ cancel_p_rls,
853 Rule.Rls_ norm_Rational_rls, (* the main rls, looping (#) *)
854 Rule.Rls_ discard_parentheses1 (* mult only *)
856 scr = Rule.Empty_Prog});
859 setup \<open>KEStore_Elems.add_rlss
860 [("calculate_Rational", (Context.theory_name @{theory}, calculate_Rational)),
861 ("calc_rat_erls", (Context.theory_name @{theory}, calc_rat_erls)),
862 ("rational_erls", (Context.theory_name @{theory}, rational_erls)),
863 ("cancel_p", (Context.theory_name @{theory}, cancel_p)),
864 ("add_fractions_p", (Context.theory_name @{theory}, add_fractions_p)),
866 ("add_fractions_p_rls", (Context.theory_name @{theory}, add_fractions_p_rls)),
867 ("powers_erls", (Context.theory_name @{theory}, powers_erls)),
868 ("powers", (Context.theory_name @{theory}, powers)),
869 ("rat_mult_divide", (Context.theory_name @{theory}, rat_mult_divide)),
870 ("reduce_0_1_2", (Context.theory_name @{theory}, reduce_0_1_2)),
872 ("rat_reduce_1", (Context.theory_name @{theory}, rat_reduce_1)),
873 ("norm_rat_erls", (Context.theory_name @{theory}, norm_rat_erls)),
874 ("norm_Rational", (Context.theory_name @{theory}, norm_Rational)),
875 ("norm_Rational_rls", (Context.theory_name @{theory}, norm_Rational_rls)),
876 ("norm_Rational_min", (Context.theory_name @{theory}, norm_Rational_min)),
877 ("norm_Rational_parenthesized", (Context.theory_name @{theory}, norm_Rational_parenthesized)),
879 ("rat_mult_poly", (Context.theory_name @{theory}, rat_mult_poly)),
880 ("rat_mult_div_pow", (Context.theory_name @{theory}, rat_mult_div_pow)),
881 ("cancel_p_rls", (Context.theory_name @{theory}, cancel_p_rls))]\<close>
883 section \<open>A problem for simplification of rationals\<close>
884 setup \<open>KEStore_Elems.add_pbts
885 [(Problem.prep_input thy "pbl_simp_rat" [] Problem.id_empty
886 (["rational", "simplification"],
887 [("#Given" ,["Term t_t"]),
888 ("#Where" ,["t_t is_ratpolyexp"]),
889 ("#Find" ,["normalform n_n"])],
890 Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)],
891 SOME "Simplify t_t", [["simplification", "of_rationals"]]))]\<close>
893 section \<open>A methods for simplification of rationals\<close>
894 (*WN061025 this methods script is copied from (auto-generated) script
895 of norm_Rational in order to ease repair on inform*)
897 partial_function (tailrec) simplify :: "real \<Rightarrow> real"
900 (Try (Rewrite_Set ''discard_minus'') #>
901 Try (Rewrite_Set ''rat_mult_poly'') #>
902 Try (Rewrite_Set ''make_rat_poly_with_parentheses'') #>
903 Try (Rewrite_Set ''cancel_p_rls'') #>
905 Try (Rewrite_Set ''add_fractions_p_rls'') #>
906 Try (Rewrite_Set ''rat_mult_div_pow'') #>
907 Try (Rewrite_Set ''make_rat_poly_with_parentheses'') #>
908 Try (Rewrite_Set ''cancel_p_rls'') #>
909 Try (Rewrite_Set ''rat_reduce_1''))) #>
910 Try (Rewrite_Set ''discard_parentheses1''))
912 setup \<open>KEStore_Elems.add_mets
913 [MethodC.prep_input thy "met_simp_rat" [] MethodC.id_empty
914 (["simplification", "of_rationals"],
915 [("#Given" ,["Term t_t"]),
916 ("#Where" ,["t_t is_ratpolyexp"]),
917 ("#Find" ,["normalform n_n"])],
918 {rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
919 prls = Rule_Set.append_rules "simplification_of_rationals_prls" Rule_Set.empty
920 [(*for preds in where_*) Rule.Eval ("Rational.is_ratpolyexp", eval_is_ratpolyexp "")],
921 crls = Rule_Set.empty, errpats = [], nrls = norm_Rational_rls},
922 @{thm simplify.simps})]