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>realpow\<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>realpow\<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 t = if TermC.is_num t then true else false;
42 (*("is_ratpolyexp", ("Rational.is_ratpolyexp", eval_is_ratpolyexp ""))*)
43 fun eval_is_ratpolyexp (thmid:string) _
44 (t as (Const (\<^const_name>\<open>Rational.is_ratpolyexp\<close>, _) $ arg)) ctxt =
46 then SOME (TermC.mk_thmid thmid (UnparseC.term ctxt arg) "",
47 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
48 else SOME (TermC.mk_thmid thmid (UnparseC.term ctxt 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 (\<^const_name>\<open>Rational.get_denominator\<close>, _) $
55 (Const (\<^const_name>\<open>divide\<close>, _) $ _(*num*) $
57 SOME (TermC.mk_thmid thmid (UnparseC.term ctxt 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 (\<^const_name>\<open>Rational.get_numerator\<close>, _) $
64 (Const (\<^const_name>\<open>divide\<close>, _) $num
66 SOME (TermC.mk_thmid thmid (UnparseC.term ctxt 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_num ==> 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_num; b is_num; c is_num; d is_num |] ==>
104 a / c + b / d = (a * d + b * c) / (c * d)" and
105 rat_add_assoc: "[| a is_num; b is_num; c is_num; d is_num |] ==>
106 a / c +(b / d + e) = (a * d + b * c)/(d * c) + e" and
107 rat_add1: "[| a is_num; b is_num; c is_num |] ==>
108 a / c + b / c = (a + b) / c" and
109 rat_add1_assoc: "[| a is_num; b is_num; c is_num |] ==>
110 a / c + (b / c + e) = (a + b) / c + e" and
111 rat_add2: "[| a is_num; b is_num; c is_num |] ==>
112 a / c + b = (a + b * c) / c" and
113 rat_add2_assoc: "[| a is_num; b is_num; c is_num |] ==>
114 a / c + (b + e) = (a + b * c) / c + e" and
115 rat_add3: "[| a is_num; b is_num; c is_num |] ==>
116 a + b / c = (a * c + b) / c" and
117 rat_add3_assoc: "[| a is_num; b is_num; c is_num |] ==>
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 (_, es) (t as Const (\<^const_name>\<open>zero_class.zero\<close>, _)) =
125 (0, list_update es (find_index (curry op = t) vs) 1)
126 | monom_of_term vs (c, es) (t as Const _) =
127 (c, list_update es (find_index (curry op = t) vs) 1)
128 | monom_of_term _ (c, es) (t as (Const (\<^const_name>\<open>numeral\<close>, _) $ _)) =
129 (t |> HOLogic.dest_number |> snd |> curry op * c, es) (*several numerals in one monom*)
130 | monom_of_term _ (c, es) (t as (Const (\<^const_name>\<open>uminus\<close>, _) $ _)) =
131 (t |> HOLogic.dest_number |> snd |> curry op * c, es) (*several numerals in one monom*)
132 | monom_of_term vs (c, es) (t as Free _) =
133 (c, list_update es (find_index (curry op = t) vs) 1)
134 | monom_of_term vs (c, es) (Const (\<^const_name>\<open>realpow\<close>, _) $ (b as Free _) $
135 (e as Const (\<^const_name>\<open>numeral\<close>, _) $ _)) =
136 (c, list_update es (find_index (curry op = b) vs) (e |> HOLogic.dest_number |> snd))
137 | monom_of_term vs (c, es) (Const (\<^const_name>\<open>realpow\<close>, _) $ (b as Free _) $
138 (e as Const (\<^const_name>\<open>uminus\<close>, _) $ _)) =
139 (c, list_update es (find_index (curry op = b) vs) (e |> HOLogic.dest_number |> snd))
141 | monom_of_term vs (c, es) (Const (\<^const_name>\<open>times\<close>, _) $ m1 $ m2) =
142 let val (c', es') = monom_of_term vs (c, es) m1
143 in monom_of_term vs (c', es') m2 end
144 | monom_of_term _ _ t = raise ERROR ("poly malformed 1 with " ^ UnparseC.term @{context} t)
147 fun monoms_of_term vs (t as Const (\<^const_name>\<open>zero_class.zero\<close>, _)) =
148 [monom_of_term vs (0, replicate (length vs) 0) t]
149 | monoms_of_term vs (t as Const _) =
150 [monom_of_term vs (1, replicate (length vs) 0) t]
151 | monoms_of_term vs (t as Const (\<^const_name>\<open>numeral\<close>, _) $ _) =
152 [monom_of_term vs (1, replicate (length vs) 0) t]
153 | monoms_of_term vs (t as Const (\<^const_name>\<open>uminus\<close>, _) $ _) =
154 [monom_of_term vs (1, replicate (length vs) 0) t]
155 | monoms_of_term vs (t as Free _) =
156 [monom_of_term vs (1, replicate (length vs) 0) t]
157 | monoms_of_term vs (t as Const (\<^const_name>\<open>realpow\<close>, _) $ _ $ _) =
158 [monom_of_term vs (1, replicate (length vs) 0) t]
159 | monoms_of_term vs (t as Const (\<^const_name>\<open>times\<close>, _) $ _ $ _) =
160 [monom_of_term vs (1, replicate (length vs) 0) t]
161 | monoms_of_term vs (Const (\<^const_name>\<open>plus\<close>, _) $ ms1 $ ms2) =
162 (monoms_of_term vs ms1) @ (monoms_of_term vs ms2)
163 | monoms_of_term _ t = raise ERROR ("poly malformed 2 with " ^ UnparseC.term @{context} t)
165 (* convert a term to the internal representation of a multivariate polynomial;
166 the conversion is quite liberal, see test --- fun poly_of_term ---:
167 * the order of variables and the parentheses within a monomial are arbitrary
168 * the coefficient may be somewhere
169 * he order and the parentheses within monomials are arbitrary
170 But the term must be completely expand + over * (laws of distributivity are not applicable).
172 The function requires the free variables as strings already given,
173 because the gcd involves 2 polynomials (with the same length for their list of exponents).
175 fun poly_of_term vs (t as Const (\<^const_name>\<open>plus\<close>, _) $ _ $ _) =
176 (SOME (t |> monoms_of_term vs |> order)
177 handle ERROR _ => NONE)
178 | poly_of_term vs t = (* 0 for zero polynomial *)
179 (SOME [monom_of_term vs (1, replicate (length vs) 0) t]
180 handle ERROR _ => NONE)
184 val vs = TermC.vars_of t
186 case poly_of_term vs t of SOME _ => true | NONE => false
188 val is_expanded = is_poly (* TODO: check names *)
189 val is_polynomial = is_poly (* TODO: check names *)
192 subsubsection \<open>Convert internal representation of a multivariate polynomial to a term\<close>
194 fun term_of_es _ _ _ [] = [] (*assumes same length for vs and es*)
195 | term_of_es baseT expT (_ :: vs) (0 :: es) = [] @ term_of_es baseT expT vs es
196 | term_of_es baseT expT (v :: vs) (1 :: es) = v :: term_of_es baseT expT vs es
197 | term_of_es baseT expT (v :: vs) (e :: es) =
198 Const (\<^const_name>\<open>realpow\<close>, [baseT, expT] ---> baseT) $ v $ (HOLogic.mk_number expT e)
199 :: term_of_es baseT expT vs es
200 | term_of_es _ _ _ _ = raise ERROR "term_of_es: length vs <> length es"
202 fun term_of_monom baseT expT vs ((c, es): monom) =
203 let val es' = term_of_es baseT expT vs es
207 if es' = [] (*if es = [0,0,0,...]*)
208 then HOLogic.mk_number baseT c
209 else foldl (HOLogic.mk_binop "Groups.times_class.times") (hd es', tl es')
210 else foldl (HOLogic.mk_binop "Groups.times_class.times")
211 (HOLogic.mk_number baseT c, es')
214 fun term_of_poly baseT expT vs p =
215 let val monos = map (term_of_monom baseT expT vs) p
216 in foldl (HOLogic.mk_binop \<^const_name>\<open>plus\<close>) (hd monos, tl monos) end
219 subsection \<open>Apply gcd_poly for cancelling and adding fractions as terms\<close>
221 fun mk_noteq_0 baseT t =
222 Const (\<^const_name>\<open>Not\<close>, HOLogic.boolT --> HOLogic.boolT) $
223 (Const (\<^const_name>\<open>HOL.eq\<close>, [baseT, baseT] ---> HOLogic.boolT) $ t $ HOLogic.mk_number HOLogic.realT 0)
225 fun mk_asms baseT ts =
226 let val as' = filter_out TermC.is_num ts (* asm like "2 ~= 0" is needless *)
227 in map (mk_noteq_0 baseT) as' end
230 subsubsection \<open>Factor out gcd for cancellation\<close>
232 fun check_fraction t =
234 Const (\<^const_name>\<open>divide\<close>, _) $ numerator $ denominator
235 => SOME (numerator, denominator)
238 (* prepare a term for cancellation by factoring out the gcd
239 assumes: is a fraction with outmost "/"*)
240 fun factout_p_ (_: theory) t =
241 let val opt = check_fraction t
245 | SOME (numerator, denominator) =>
247 val vs = TermC.vars_of t
248 val baseT = type_of numerator
249 val expT = HOLogic.realT
251 case (poly_of_term vs numerator, poly_of_term vs denominator) of
254 val ((a', b'), c) = gcd_poly a b
255 val es = replicate (length vs) 0
257 if c = [(1, es)] orelse c = [(~1, es)]
261 val b't = term_of_poly baseT expT vs b'
262 val ct = term_of_poly baseT expT vs c
264 HOLogic.mk_binop \<^const_name>\<open>divide\<close>
265 (HOLogic.mk_binop \<^const_name>\<open>times\<close>
266 (term_of_poly baseT expT vs a', ct),
267 HOLogic.mk_binop \<^const_name>\<open>times\<close> (b't, ct))
268 in SOME (t', mk_asms baseT [b't, ct]) end
270 | _ => NONE : (term * term list) option
275 subsubsection \<open>Cancel a fraction\<close>
277 (* cancel a term by the gcd ("" denote terms with internal algebraic structure)
278 cancel_p_ : theory \<Rightarrow> term \<Rightarrow> (term \<times> term list) option
279 cancel_p_ thy "a / b" = SOME ("a' / b'", ["b' \<noteq> 0"])
280 assumes: a is_polynomial \<and> b is_polynomial \<and> b \<noteq> 0
282 SOME ("a' / b'", ["b' \<noteq> 0"]). gcd_poly a b \<noteq> 1 \<and> gcd_poly a b \<noteq> -1 \<and>
283 a' * gcd_poly a b = a \<and> b' * gcd_poly a b = b
285 fun cancel_p_ (_: theory) t =
286 let val opt = check_fraction t
290 | SOME (numerator, denominator) =>
292 val vs = TermC.vars_of t
293 val baseT = type_of numerator
294 val expT = HOLogic.realT
296 case (poly_of_term vs numerator, poly_of_term vs denominator) of
299 val ((a', b'), c) = gcd_poly a b
300 val es = replicate (length vs) 0
302 if c = [(1, es)] orelse c = [(~1, es)]
306 val bt' = term_of_poly baseT expT vs b'
307 val ct = term_of_poly baseT expT vs c
309 HOLogic.mk_binop \<^const_name>\<open>divide\<close>
310 (term_of_poly baseT expT vs a', bt')
311 val asm = mk_asms baseT [bt']
312 in SOME (t', asm) end
314 | _ => NONE : (term * term list) option
319 subsubsection \<open>Factor out to a common denominator for addition\<close>
321 (* addition of fractions allows (at most) one non-fraction (a monomial) *)
323 (Const (\<^const_name>\<open>plus\<close>, _) $
324 (Const (\<^const_name>\<open>divide\<close>, _) $ n1 $ d1) $
325 (Const (\<^const_name>\<open>divide\<close>, _) $ n2 $ d2))
326 = SOME ((n1, d1), (n2, d2))
328 (Const (\<^const_name>\<open>plus\<close>, _) $
330 (Const (\<^const_name>\<open>divide\<close>, _) $ n2 $ d2))
331 = SOME ((nofrac, HOLogic.mk_number HOLogic.realT 1), (n2, d2))
333 (Const (\<^const_name>\<open>plus\<close>, _) $
334 (Const (\<^const_name>\<open>divide\<close>, _) $ n1 $ d1) $
336 = SOME ((n1, d1), (nofrac, HOLogic.mk_number HOLogic.realT 1))
337 | check_frac_sum _ = NONE
339 (* prepare a term for addition by providing the least common denominator as a product
340 assumes: is a term with outmost "+" and at least one outmost "/" in respective summands*)
341 fun common_nominator_p_ (_: theory) t =
342 let val opt = check_frac_sum t
346 | SOME ((n1, d1), (n2, d2)) =>
348 val vs = TermC.vars_of t
350 case (poly_of_term vs d1, poly_of_term vs d2) of
353 val ((a', b'), c) = gcd_poly a b
354 val (baseT, expT) = (type_of n1, HOLogic.realT)
355 val [d1', d2', c'] = map (term_of_poly baseT expT vs) [a', b', c]
356 (*----- minimum of parentheses & nice result, but breaks tests: -------------
357 val denom = HOLogic.mk_binop \<^const_name>\<open>times\<close>
358 (HOLogic.mk_binop \<^const_name>\<open>times\<close> (d1', d2'), c') -------------*)
360 if c = [(1, replicate (length vs) 0)]
361 then HOLogic.mk_binop \<^const_name>\<open>times\<close> (d1', d2')
363 HOLogic.mk_binop \<^const_name>\<open>times\<close> (c',
364 HOLogic.mk_binop \<^const_name>\<open>times\<close> (d1', d2')) (*--------------*)
366 HOLogic.mk_binop \<^const_name>\<open>plus\<close>
367 (HOLogic.mk_binop \<^const_name>\<open>divide\<close>
368 (HOLogic.mk_binop \<^const_name>\<open>times\<close> (n1, d2'), denom),
369 HOLogic.mk_binop \<^const_name>\<open>divide\<close>
370 (HOLogic.mk_binop \<^const_name>\<open>times\<close> (n2, d1'), denom))
371 val asm = mk_asms baseT [d1', d2', c']
372 in SOME (t', asm) end
373 | _ => NONE : (term * term list) option
378 subsubsection \<open>Addition of at least one fraction within a sum\<close>
381 assumes: is a term with outmost "+" and at least one outmost "/" in respective summands
382 \<and> NONE of the summands is zero.
383 NOTE: the case "(_ + _) + _" need not be considered due to iterated addition *)
384 fun add_fraction_p_ (_: theory) t =
385 case check_frac_sum t of
387 | SOME ((n1, d1), (n2, d2)) =>
389 val vs = TermC.vars_of t
391 case (poly_of_term vs n1, poly_of_term vs d1, poly_of_term vs n2, poly_of_term vs d2) of
392 (SOME _, SOME a, SOME _, SOME b) =>
394 val ((a', b'), c) = gcd_poly a b
395 val (baseT, expT) = (type_of n1, HOLogic.realT)
396 val nomin = term_of_poly baseT expT vs
397 (((the (poly_of_term vs n1)) %%*%% b') %%+%% ((the (poly_of_term vs n2)) %%*%% a'))
398 val denom = term_of_poly baseT expT vs ((c %%*%% a') %%*%% b')
399 val t' = HOLogic.mk_binop \<^const_name>\<open>divide\<close> (nomin, denom)
400 in SOME (t', mk_asms baseT [denom]) end
401 | _ => NONE : (term * term list) option
405 section \<open>Embed cancellation and addition into rewriting\<close>
407 subsection \<open>Rulesets and predicate for embedding\<close>
409 (* evaluates conditions in calculate_Rational *)
412 (Rule_Def.Repeat {id = "calc_rat_erls", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
413 asm_rls = Rule_Set.Empty, prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
415 \<^rule_eval>\<open>matches\<close> (Prog_Expr.eval_matches "#matches_"),
416 \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
417 \<^rule_eval>\<open>is_num\<close> (Prog_Expr.eval_is_num "#is_num_"),
418 \<^rule_thm>\<open>not_true\<close>,
419 \<^rule_thm>\<open>not_false\<close>],
420 program = Rule.Empty_Prog});
422 (* simplifies expressions with numerals;
423 does NOT rearrange the term by AC-rewriting; thus terms with variables
424 need to have constants to be commuted together respectively *)
425 val calculate_Rational =
426 prep_rls' (Rule_Set.merge "calculate_Rational"
427 (Rule_Def.Repeat {id = "divide", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
428 asm_rls = calc_rat_erls, prog_rls = Rule_Set.Empty,
429 calc = [], errpatts = [],
431 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
433 \<^rule_thm_sym>\<open>minus_divide_left\<close>, (*SYM - ?x / ?y = - (?x / ?y) may come from subst*)
434 \<^rule_thm>\<open>rat_add\<close>,
435 (*"[| a is_num; b is_num; c is_num; d is_num |] ==> a / c + b / d = (a * d) / (c * d) + (b * c ) / (d * c)"*)
436 \<^rule_thm>\<open>rat_add1\<close>, (*"[| a is_num; b is_num; c is_num |] ==> a / c + b / c = (a + b) / c"*)
437 \<^rule_thm>\<open>rat_add2\<close>, (*"[| ?a is_num; ?b is_num; ?c is_num |] ==> ?a / ?c + ?b = (?a + ?b * ?c) / ?c"*)
438 \<^rule_thm>\<open>rat_add3\<close>, (*"[| a is_num; b is_num; c is_num |] ==> a + b / c = (a * c) / c + b / c" *)
440 \<^rule_thm>\<open>rat_mult\<close>, (*a / b * (c / d) = a * c / (b * d)*)
441 \<^rule_thm>\<open>times_divide_eq_right\<close>, (*?x * (?y / ?z) = ?x * ?y / ?z*)
442 \<^rule_thm>\<open>times_divide_eq_left\<close>, (*?y / ?z * ?x = ?y * ?x / ?z*)
444 \<^rule_thm>\<open>real_divide_divide1\<close>, (*"?y ~= 0 ==> ?u / ?v / (?y / ?z) = ?u / ?v * (?z / ?y)"*)
445 \<^rule_thm>\<open>divide_divide_eq_left\<close>, (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
447 \<^rule_thm>\<open>rat_power\<close>, (*"(?a / ?b) \<up> ?n = ?a \<up> ?n / ?b \<up> ?n"*)
449 \<^rule_thm>\<open>mult_cross\<close>, (*"[| b ~= 0; d ~= 0 |] ==> (a / b = c / d) = (a * d = b * c)*)
450 \<^rule_thm>\<open>mult_cross1\<close>, (*" b ~= 0 ==> (a / b = c ) = (a = b * c)*)
451 \<^rule_thm>\<open>mult_cross2\<close> (*" d ~= 0 ==> (a = c / d) = (a * d = c)*)],
452 program = Rule.Empty_Prog})
455 (*("is_expanded", ("Rational.is_expanded", eval_is_expanded ""))*)
456 fun eval_is_expanded (thmid:string) _
457 (t as (Const (\<^const_name>\<open>Rational.is_expanded\<close>, _) $ arg)) ctxt =
459 then SOME (TermC.mk_thmid thmid (UnparseC.term ctxt arg) "",
460 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
461 else SOME (TermC.mk_thmid thmid (UnparseC.term ctxt arg) "",
462 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
463 | eval_is_expanded _ _ _ _ = NONE;
465 calculation is_expanded = \<open>eval_is_expanded ""\<close>
468 Rule_Set.merge "rational_erls" calculate_Rational
469 (Rule_Set.append_rules "is_expanded" Atools_erls [
470 \<^rule_eval>\<open>is_expanded\<close> (eval_is_expanded "")]);
473 subsection \<open>Embed cancellation into rewriting\<close>
475 (**)local (* cancel_p *)
477 val {rules = rules, rew_ord = (_, ro), ...} = Rule_Set.rep (get_rls @{context} "rev_rew_p");
479 fun init_state thy eval_rls ro t =
481 val SOME (t', _) = factout_p_ thy t;
482 val SOME (t'', asm) = cancel_p_ thy t;
483 val der = Derive.steps_reverse (Proof_Context.init_global thy) eval_rls rules ro NONE t';
485 [(\<^rule_thm>\<open>real_mult_div_cancel2\<close>, (t'', asm))]
486 val rs = (Rule.distinct' o (map #1)) der
487 val rs = filter_out (ThmC.member'
488 ["sym_real_add_zero_left", "sym_real_mult_0", "sym_real_mult_1"]) rs
489 in (t, t'', [rs(*one in order to ease locate_rule*)], der) end;
491 fun locate_rule thy eval_rls ro [rs] t r =
492 if member op = ((map (Rule.thm_id)) rs) (Rule.thm_id r)
495 val ctxt = Proof_Context.init_global thy
496 val ropt = Rewrite.rewrite_ ctxt ro eval_rls true (Rule.thm ctxt r) t;
498 case ropt of SOME ta => [(r, ta)]
500 ("### locate_rule: rewrite " ^ Rule.thm_id r ^ " " ^ UnparseC.term @{context} t ^ " = NONE");*) [])
502 else ((*tracing ("### locate_rule: " ^ Rule.thm_id r ^ " not mem rrls");*) [])
503 | locate_rule _ _ _ _ _ _ = raise ERROR "locate_rule: doesnt match rev-sets in istate";
505 fun next_rule thy eval_rls ro [rs] t =
507 val der = Derive.do_one (Proof_Context.init_global thy) eval_rls rs ro NONE t;
508 in case der of (_, r, _) :: _ => SOME r | _ => NONE end
509 | next_rule _ _ _ _ _ = raise ERROR ("next_rule: doesnt match rev-sets in istate");
511 fun attach_form (_: Rule.rule list list) (_: term) (_: term) =
512 [(*TODO*)]: ( Rule.rule * (term * term list)) list;
517 Rule_Set.Rrls {id = "cancel_p", prepat = [],
518 rew_ord = ("ord_make_polynomial", ord_make_polynomial false),
519 asm_rls = rational_erls,
521 [("PLUS", (\<^const_name>\<open>plus\<close>, (**)Calc_Binop.numeric "#add_")),
522 ("TIMES" , (\<^const_name>\<open>times\<close>, (**)Calc_Binop.numeric "#mult_")),
523 ("DIVIDE", (\<^const_name>\<open>divide\<close>, Prog_Expr.eval_cancel "#divide_e")),
524 ("POWER", (\<^const_name>\<open>realpow\<close>, (**)Calc_Binop.numeric "#power_"))],
527 Rule.Rfuns {init_state = init_state \<^theory> Atools_erls ro,
528 normal_form = cancel_p_ \<^theory>,
529 locate_rule = locate_rule \<^theory> Atools_erls ro,
530 next_rule = next_rule \<^theory> Atools_erls ro,
531 attach_form = attach_form}}
532 (**)end(* local cancel_p *)
535 subsection \<open>Embed addition into rewriting\<close>
537 (**)local (* add_fractions_p *)
539 (*val {rules = rules, rew_ord = (_, ro), ...} = Rule_Set.rep (get_rls "make_polynomial");*)
540 val {rules, rew_ord = (_, ro), ...} = Rule_Set.rep (get_rls @{context} "rev_rew_p");
542 fun init_state thy eval_rls ro t =
544 val SOME (t', _) = common_nominator_p_ thy t;
545 val SOME (t'', asm) = add_fraction_p_ thy t;
546 val der = Derive.steps_reverse (Proof_Context.init_global thy) eval_rls rules ro NONE t';
548 [(\<^rule_thm>\<open>real_mult_div_cancel2\<close>, (t'',asm))]
549 val rs = (Rule.distinct' o (map #1)) der;
550 val rs = filter_out (ThmC.member'
551 ["sym_real_add_zero_left", "sym_real_mult_0", "sym_real_mult_1"]) rs;
552 in (t, t'', [rs(*here only _ONE_*)], der) end;
554 fun locate_rule thy eval_rls ro [rs] t r =
555 if member op = ((map (Rule.thm_id)) rs) (Rule.thm_id r)
558 val ctxt = Proof_Context.init_global thy
559 val ropt = Rewrite.rewrite_ ctxt ro eval_rls true (Rule.thm ctxt r) t;
564 ((*tracing ("### locate_rule: rewrite " ^ Rule.thm_id r ^ " " ^ UnparseC.term @{context} t ^ " = NONE");*)
566 else ((*tracing ("### locate_rule: " ^ Rule.thm_id r ^ " not mem rrls");*) [])
567 | locate_rule _ _ _ _ _ _ = raise ERROR "locate_rule: doesnt match rev-sets in istate";
569 fun next_rule thy eval_rls ro [rs] t =
570 let val der = Derive.do_one (Proof_Context.init_global thy) eval_rls rs ro NONE t;
576 | next_rule _ _ _ _ _ = raise ERROR ("next_rule: doesnt match rev-sets in istate");
578 val SOME pat0 = ParseC.patt_opt \<^theory> "?r/?s+?u/?v :: real";
579 val SOME pat1 = ParseC.patt_opt \<^theory> "?r/?s+?u :: real";
580 val SOME pat2 = ParseC.patt_opt \<^theory> "?r +?u/?v :: real";
581 val prepat = [([@{term True}], pat0),
582 ([@{term True}], pat1),
583 ([@{term True}], pat2)];
586 val add_fractions_p =
587 Rule_Set.Rrls {id = "add_fractions_p", prepat=prepat,
588 rew_ord = ("ord_make_polynomial", ord_make_polynomial false),
589 asm_rls = rational_erls,
590 calc = [("PLUS", (\<^const_name>\<open>plus\<close>, (**)Calc_Binop.numeric "#add_")),
591 ("TIMES", (\<^const_name>\<open>times\<close>, (**)Calc_Binop.numeric "#mult_")),
592 ("DIVIDE", (\<^const_name>\<open>divide\<close>, Prog_Expr.eval_cancel "#divide_e")),
593 ("POWER", (\<^const_name>\<open>realpow\<close>, (**)Calc_Binop.numeric "#power_"))],
595 program = Rule.Rfuns {init_state = init_state \<^theory> Atools_erls ro,
596 normal_form = add_fraction_p_ \<^theory>,
597 locate_rule = locate_rule \<^theory> Atools_erls ro,
598 next_rule = next_rule \<^theory> Atools_erls ro,
599 attach_form = attach_form}}
600 (**)end(*local add_fractions_p *)
603 subsection \<open>Cancelling and adding all occurrences in a term /////////////////////////////\<close>
605 (*copying cancel_p_rls + add her caused error in interface.sml*)
608 section \<open>Rulesets for general simplification\<close>
610 (*.all powers over + distributed; atoms over * collected, other distributed
611 contains absolute minimum of thms for context in norm_Rational .*)
612 val powers = prep_rls'(
613 Rule_Def.Repeat {id = "powers", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.function_empty),
614 asm_rls = powers_erls, prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
616 \<^rule_thm>\<open>realpow_multI\<close>, (*"(r * s) \<up> n = r \<up> n * s \<up> n"*)
617 \<^rule_thm>\<open>realpow_pow\<close>, (*"(a \<up> b) \<up> c = a \<up> (b * c)"*)
618 \<^rule_thm>\<open>realpow_oneI\<close>, (*"r \<up> 1 = r"*)
619 \<^rule_thm>\<open>realpow_minus_even\<close>, (*"n is_even ==> (- r) \<up> n = r \<up> n" ?-->discard_minus?*)
620 \<^rule_thm>\<open>realpow_minus_odd\<close>, (*"Not (n is_even) ==> (- r) \<up> n = -1 * r \<up> n"*)
622 (*----- collect atoms over * -----*)
623 \<^rule_thm>\<open>realpow_two_atom\<close>, (*"r is_atom ==> r * r = r \<up> 2"*)
624 \<^rule_thm>\<open>realpow_plus_1\<close>, (*"r is_atom ==> r * r \<up> n = r \<up> (n + 1)"*)
625 \<^rule_thm>\<open>realpow_addI_atom\<close>, (*"r is_atom ==> r \<up> n * r \<up> m = r \<up> (n + m)"*)
627 (*----- distribute none-atoms -----*)
628 \<^rule_thm>\<open>realpow_def_atom\<close>, (*"[| 1 < n; ~ (r is_atom) |]==>r \<up> n = r * r \<up> (n + -1)"*)
629 \<^rule_thm>\<open>realpow_eq_oneI\<close>, (*"1 \<up> n = 1"*)
630 \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_")],
631 program = Rule.Empty_Prog});
634 (*.contains absolute minimum of thms for context in norm_Rational.*)
635 val rat_mult_divide = prep_rls'(
636 Rule_Def.Repeat {id = "rat_mult_divide", preconds = [],
637 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
638 asm_rls = Rule_Set.empty, prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
640 \<^rule_thm>\<open>rat_mult\<close>, (*(1)"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
641 \<^rule_thm>\<open>times_divide_eq_right\<close>, (*(2)"?a * (?c / ?d) = ?a * ?c / ?d" must be [2],
642 otherwise inv.to a / b / c = ...*)
643 \<^rule_thm>\<open>times_divide_eq_left\<close>, (*"?a / ?b * ?c = ?a * ?c / ?b" order weights x \<up> n too much
644 and does not commute a / b * c \<up> 2 !*)
646 \<^rule_thm>\<open>divide_divide_eq_right\<close>, (*"?x / (?y / ?z) = ?x * ?z / ?y"*)
647 \<^rule_thm>\<open>divide_divide_eq_left\<close>, (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
648 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e")],
649 program = Rule.Empty_Prog});
652 (*.contains absolute minimum of thms for context in norm_Rational.*)
653 val reduce_0_1_2 = prep_rls'(
654 Rule_Def.Repeat{id = "reduce_0_1_2", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
655 asm_rls = Rule_Set.empty, prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
657 \<^rule_thm>\<open>div_by_1\<close>, (*"?x / 1 = ?x"*)
658 \<^rule_thm>\<open>mult_1_left\<close>, (*"1 * z = z"*)
659 \<^rule_thm>\<open>minus_zero\<close>, (*"- 0 = 0"*)
660 (*\<^rule_thm>\<open>real_mult_minus1\<close>, "-1 * z = - z"*)
661 (*\<^rule_thm>\<open>real_minus_mult_cancel\<close>, "- ?x * - ?y = ?x * ?y"*)
664 \<^rule_thm>\<open>mult_zero_left\<close>, (*"0 * z = 0"*)
665 \<^rule_thm>\<open>add_0_left\<close>, (*"0 + z = z"*)
666 (*\<^rule_thm>\<open>right_minus\<close>, "?z + - ?z = 0"*)
668 \<^rule_thm_sym>\<open>real_mult_2\<close>, (*"z1 + z1 = 2 * z1"*)
669 \<^rule_thm>\<open>real_mult_2_assoc\<close>, (*"z1 + (z1 + k) = 2 * z1 + k"*)
671 \<^rule_thm>\<open>division_ring_divide_zero\<close> (*"0 / ?x = 0"*)],
672 program = Rule.Empty_Prog});
674 (*asm_rls for calculate_Rational;
675 make local with FIXX@ME result:term *term list WN0609???SKMG*)
676 val norm_rat_erls = prep_rls'(
677 Rule_Def.Repeat {id = "norm_rat_erls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.function_empty),
678 asm_rls = Rule_Set.empty, prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
680 \<^rule_eval>\<open>Prog_Expr.is_num\<close> (Prog_Expr.eval_is_num "#is_num_")
682 program = Rule.Empty_Prog});
685 (* consists of rls containing the absolute minimum of thms *)
687 which is now replaced by MGs version "norm_Rational" below
689 val norm_Rational_min = prep_rls'(
690 Rule_Def.Repeat {id = "norm_Rational_min", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.function_empty),
691 asm_rls = norm_rat_erls, prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
692 rules = [(*sequence given by operator precedence*)
693 Rule.Rls_ discard_minus,
695 Rule.Rls_ rat_mult_divide,
697 Rule.Rls_ reduce_0_1_2,
698 Rule.Rls_ order_add_mult,
699 Rule.Rls_ collect_numerals,
700 Rule.Rls_ add_fractions_p,
703 program = Rule.Empty_Prog});
706 val norm_Rational_parenthesized = prep_rls'(
707 Rule_Set.Sequence {id = "norm_Rational_parenthesized", preconds = []:term list,
708 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
709 asm_rls = Atools_erls, prog_rls = Rule_Set.Empty,
710 calc = [], errpatts = [],
712 Rule.Rls_ norm_Rational_min,
713 Rule.Rls_ discard_parentheses],
714 program = Rule.Empty_Prog});
716 (*WN030318???SK: simplifies all but cancel and common_nominator*)
717 val simplify_rational =
718 Rule_Set.merge "simplify_rational" expand_binoms
719 (Rule_Set.append_rules "divide" calculate_Rational [
720 \<^rule_thm>\<open>div_by_1\<close>, (*"?x / 1 = ?x"*)
721 \<^rule_thm>\<open>rat_mult\<close>, (*(1)"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
722 \<^rule_thm>\<open>times_divide_eq_right\<close>, (*(2)"?a * (?c / ?d) = ?a * ?c / ?d" must be [2],
723 otherwise inv.to a / b / c = ...*)
724 \<^rule_thm>\<open>times_divide_eq_left\<close>, (*"?a / ?b * ?c = ?a * ?c / ?b"*)
725 \<^rule_thm>\<open>add_minus\<close>, (*"?a + ?b - ?b = ?a"*)
726 \<^rule_thm>\<open>add_minus1\<close>, (*"?a - ?b + ?b = ?a"*)
727 \<^rule_thm>\<open>divide_minus1\<close> (*"?x / -1 = - ?x"*)]);
729 val add_fractions_p_rls = prep_rls'(
730 Rule_Def.Repeat {id = "add_fractions_p_rls", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
731 asm_rls = Rule_Set.empty, prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
732 rules = [Rule.Rls_ add_fractions_p],
733 program = Rule.Empty_Prog});
735 (* "Rule_Def.Repeat" causes repeated application of cancel_p to one and the same term *)
736 val cancel_p_rls = prep_rls'(
738 {id = "cancel_p_rls", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
739 asm_rls = Rule_Set.empty, prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
740 rules = [Rule.Rls_ cancel_p],
741 program = Rule.Empty_Prog});
743 (*. makes 'normal' fractions; 'is_polyexp' inhibits double fractions;
744 used in initial part norm_Rational_mg, see example DA-M02-main.p.60.*)
745 val rat_mult_poly = prep_rls'(
746 Rule_Def.Repeat {id = "rat_mult_poly", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
747 asm_rls = Rule_Set.append_rules "Rule_Set.empty-is_polyexp" Rule_Set.empty [
748 \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp "")],
749 prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
751 \<^rule_thm>\<open>rat_mult_poly_l\<close>, (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*)
752 \<^rule_thm>\<open>rat_mult_poly_r\<close> (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*)],
753 program = Rule.Empty_Prog});
755 (*. makes 'normal' fractions; 'is_polyexp' inhibits double fractions;
756 used in looping part norm_Rational_rls, see example DA-M02-main.p.60
757 .. WHERE THE LATTER DOES ALWAYS WORK, BECAUSE asm_rls = Rule_Set.empty,
758 I.E. THE RESPECTIVE ASSUMPTION IS STORED AND Rule.Thm APPLIED; WN051028
760 val rat_mult_div_pow = prep_rls'(
761 Rule_Def.Repeat {id = "rat_mult_div_pow", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.function_empty),
762 asm_rls = Rule_Set.empty, prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
764 \<^rule_thm>\<open>rat_mult\<close>, (*"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
765 \<^rule_thm>\<open>rat_mult_poly_l\<close>, (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*)
766 \<^rule_thm>\<open>rat_mult_poly_r\<close>, (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*)
768 \<^rule_thm>\<open>real_divide_divide1_mg\<close>, (*"y ~= 0 ==> (u / v) / (y / z) = (u * z) / (y * v)"*)
769 \<^rule_thm>\<open>divide_divide_eq_right\<close>, (*"?x / (?y / ?z) = ?x * ?z / ?y"*)
770 \<^rule_thm>\<open>divide_divide_eq_left\<close>, (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
771 \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
773 \<^rule_thm>\<open>rat_power\<close> (*"(?a / ?b) \<up> ?n = ?a \<up> ?n / ?b \<up> ?n"*)],
774 program = Rule.Empty_Prog});
776 val rat_reduce_1 = prep_rls'(
777 Rule_Def.Repeat {id = "rat_reduce_1", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
778 asm_rls = Rule_Set.empty, prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
780 \<^rule_thm>\<open>div_by_1\<close>, (*"?x / 1 = ?x"*)
781 \<^rule_thm>\<open>mult_1_left\<close> (*"1 * z = z"*)],
782 program = Rule.Empty_Prog});
784 (* looping part of norm_Rational *)
785 val norm_Rational_rls = prep_rls' (
786 Rule_Def.Repeat {id = "norm_Rational_rls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.function_empty),
787 asm_rls = norm_rat_erls, prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
789 Rule.Rls_ add_fractions_p_rls,
790 Rule.Rls_ rat_mult_div_pow,
791 Rule.Rls_ make_rat_poly_with_parentheses,
792 Rule.Rls_ cancel_p_rls,
793 Rule.Rls_ rat_reduce_1],
794 program = Rule.Empty_Prog});
796 val norm_Rational = prep_rls' (
798 {id = "norm_Rational", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
799 asm_rls = norm_rat_erls, prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
801 Rule.Rls_ discard_minus,
802 Rule.Rls_ rat_mult_poly, (* removes double fractions like a/b/c *)
803 Rule.Rls_ make_rat_poly_with_parentheses,
804 Rule.Rls_ cancel_p_rls,
805 Rule.Rls_ norm_Rational_rls, (* the main rls, looping (#) *)
806 Rule.Rls_ discard_parentheses1], (* mult only *)
807 program = Rule.Empty_Prog});
811 calculate_Rational = calculate_Rational and
812 calc_rat_erls = calc_rat_erls and
813 rational_erls = rational_erls and
814 cancel_p = cancel_p and
815 add_fractions_p = add_fractions_p and
817 add_fractions_p_rls = add_fractions_p_rls and
818 powers_erls = powers_erls and
820 rat_mult_divide = rat_mult_divide and
821 reduce_0_1_2 = reduce_0_1_2 and
823 rat_reduce_1 = rat_reduce_1 and
824 norm_rat_erls = norm_rat_erls and
825 norm_Rational = norm_Rational and
826 norm_Rational_rls = norm_Rational_rls and
827 norm_Rational_min = norm_Rational_min and
828 norm_Rational_parenthesized = norm_Rational_parenthesized and
830 rat_mult_poly = rat_mult_poly and
831 rat_mult_div_pow = rat_mult_div_pow and
832 cancel_p_rls = cancel_p_rls
834 section \<open>A problem for simplification of rationals\<close>
836 problem pbl_simp_rat : "rational/simplification" =
837 \<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)]\<close>
838 Method_Ref: "simplification/of_rationals"
841 Where: "t_t is_ratpolyexp"
842 Find: "normalform n_n"
844 section \<open>A methods for simplification of rationals\<close>
845 (*WN061025 this methods script is copied from (auto-generated) script
846 of norm_Rational in order to ease repair on inform*)
848 partial_function (tailrec) simplify :: "real \<Rightarrow> real"
851 (Try (Rewrite_Set ''discard_minus'') #>
852 Try (Rewrite_Set ''rat_mult_poly'') #>
853 Try (Rewrite_Set ''make_rat_poly_with_parentheses'') #>
854 Try (Rewrite_Set ''cancel_p_rls'') #>
856 Try (Rewrite_Set ''add_fractions_p_rls'') #>
857 Try (Rewrite_Set ''rat_mult_div_pow'') #>
858 Try (Rewrite_Set ''make_rat_poly_with_parentheses'') #>
859 Try (Rewrite_Set ''cancel_p_rls'') #>
860 Try (Rewrite_Set ''rat_reduce_1''))) #>
861 Try (Rewrite_Set ''discard_parentheses1''))
865 method met_simp_rat : "simplification/of_rationals" =
866 \<open>{rew_ord="tless_true", rls' = Rule_Set.empty, calc = [], prog_rls = Rule_Set.empty,
867 where_rls = Rule_Set.append_rules "simplification_of_rationals_prls" Rule_Set.empty
868 [(*for preds in where_*) \<^rule_eval>\<open>is_ratpolyexp\<close> (eval_is_ratpolyexp "")],
869 errpats = [], rew_rls = norm_Rational_rls}\<close>
870 Program: simplify.simps
872 Where: "t_t is_ratpolyexp"
873 Find: "normalform n_n"
876 section \<open>Error_Patterns\<close>
878 declare [[check_unique = false]]
879 setup \<open>Know_Store.add_mets @{context}
880 [Pbl_Met_Hierarchy.add_errpats @{theory} ["simplification", "of_rationals"]
881 [("addition-of-fractions",
882 [ParseC.patt_opt @{theory} "(?a / ?b + ?c / ?d) = (?a + ?c)/(?b + ?d)" |> the,
883 ParseC.patt_opt @{theory} "(?a / ?b + ?c / ?d) = (?a + ?c)/(?b * ?d)" |> the,
884 ParseC.patt_opt @{theory} "(?a / ?b + ?c / ?d) = (?c * ?a)/(?d * ?b)" |> the,
885 ParseC.patt_opt @{theory} "?a + (?b /?c)= (?a + ?b)/ ?c" |> the,
886 ParseC.patt_opt @{theory} "?a + (?b /?c)= (?a * ?b)/ ?c" |> the],
887 [@{thm rat_add}, @{thm rat_add_assoc}, @{thm rat_add1}, @{thm rat_add1_assoc},
888 @{thm rat_add2}, @{thm rat_add2_assoc}, @{thm rat_add3}, @{thm rat_add3_assoc}])]
890 declare [[check_unique = true]]
892 (*TODO insert_fillpats ["IsacKnowledge", "Rational", "Theorems", "???"]*)
894 (* TODO insert_errpats overwrites instead of appending
895 insert_errpats ["simplification", "of_rationals"]
896 (("cancel", (*see master thesis gdarocy*)
897 [(*a*)parse_patt @{theory Rational} "(?a + ?b)/?a = ?b",
898 (*b*)parse_patt @{theory Rational} "(?a + ?b)/?b = ?a",
899 (*c*)parse_patt @{theory Rational} "(?a + ?b)/(?b + ?c) = ?a / ?c",
900 (*d*)parse_patt @{theory Rational} "(?a + ?c)/(?b + ?c) = ?a / ?b",
901 (*e*)parse_patt @{theory Rational} "(?a + ?c)/(?b + ?c) = ?a / ?c",
902 (*f*)parse_patt @{theory Rational} "(?a + ?b)/(?c + ?a) = ?b / ?c",
903 (*g*)parse_patt @{theory Rational} "(?a*?b + ?c)/?a = ?b + ?c",
904 (*h*)parse_patt @{theory Rational} "(?a*?b + ?c)/?b = ?a + ?c",
905 (*i*)parse_patt @{theory Rational} "(?a + ?b*?c)/?b = ?a + ?c",
906 (*j*)parse_patt @{theory Rational} "(?a + ?b*?c)/?b = ?a + ?b",
907 (*k*)parse_patt @{theory Rational} "(?a + ?b*?e)/(?c + ?d*?e) = (?a + ?b)/(?c + ?d)"],
908 [@{thm real_times_divide_1_eq}, (*TODO*) @{thm real_times_divide_1_eq}]));
911 ("fill-cancel-left-num",
912 parse_patt @{theory Rational} "(?a * ?b) / (?a * ?c) = _ / ?c", "cancel"),
913 ("fill-cancel-left-den",
914 parse_patt @{theory Rational} "(?a * ?b) / (?a * ?c) = ?b / _", "cancel"),
916 parse_patt @{theory Rational} "(?a * ?b) / (?a * ?c) = ?b / ?c", "cancel"),
918 ("fill-cancel-left-add-num1",
919 parse_patt @{theory Rational} "(?a * (?b + ?c)) / (?a * ?d) = (_ + ?c) / ?d", "cancel"),
920 ("fill-cancel-left-add-num2",
921 parse_patt @{theory Rational} "(?a * (?b + ?c)) / (?a * ?d) = (?b + _) / ?d", "cancel"),
922 ("fill-cancel-left-add-num3",
923 parse_patt @{theory Rational} "(?a * (?b + ?c)) / (?a * ?d) = (_ + _) / ?d", "cancel"),
924 ("fill-cancel-left-add-num4",
925 parse_patt @{theory Rational} "(?a * (?b + ?c)) / (?a * ?d) = (?b + ?c) / _", "cancel"),
926 ("fill-cancel-left-add-num5",
927 parse_patt @{theory Rational} "(?a * (?b + ?c)) / (?a * ?d) = (_ + ?c) / _", "cancel"),
928 ("fill-cancel-left-add-num6",
929 parse_patt @{theory Rational} "(?a * (?b + ?c)) / (?a * ?d) = (?b + _) / _", "cancel"),
930 ("fill-cancel-left-add-none",
931 parse_patt @{theory Rational} "(?a * (?b + ?c)) / (?a * ?d) = (?b + ?c) / ?d", "cancel"),
933 ("fill-cancel-left-add-den1",
934 parse_patt @{theory Rational} "(?a * ?b) / (?a * (?c + ?d)) = ?b / (?c + ?d)", "cancel"),
935 ("fill-cancel-left-add-den2",
936 parse_patt @{theory Rational} "(?a * ?b) / (?a * (?c + ?d)) = ?b / (?c + ?d)", "cancel"),
937 ("fill-cancel-left-add-den3",
938 parse_patt @{theory Rational} "(?a * ?b) / (?a * (?c + ?d)) = ?b / (?c + ?d)", "cancel"),
939 ("fill-cancel-left-add-den4",
940 parse_patt @{theory Rational} "(?a * ?b) / (?a * (?c + ?d)) = ?b / (?c + ?d)", "cancel"),
941 ("fill-cancel-left-add-den5",
942 parse_patt @{theory Rational} "(?a * ?b) / (?a * (?c + ?d)) = ?b / (?c + ?d)", "cancel"),
943 ("fill-cancel-left-add-den6",
944 parse_patt @{theory Rational} "(?a * ?b) / (?a * (?c + ?d)) = ?b / (?c + ?d)", "cancel"),
945 ("fill-cancel-left-add-none",
946 parse_patt @{theory Rational} "(?a * ?b) / (?a * (?c + ?d)) = ?b / (?c + ?d)", "cancel")