neuper@52105: (* rationals, fractions of multivariate polynomials over the real field
neuper@37906:    author: isac team
neuper@52105:    Copyright (c) isac team 2002, 2013
neuper@37906:    Use is subject to license terms.
neuper@37906: 
neuper@37906:    depends on Poly (and not on Atools), because 
wneuper@59370:    fractions with _normalised_ polynomials are canceled, added, etc.
neuper@37906: *)
neuper@37906: 
neuper@48884: theory Rational 
wneuper@59553: imports Poly GCD_Poly_ML
neuper@48884: begin
neuper@37906: 
walther@60358: section \<open>Constants for evaluation by \ <^rule_eval>\<close>
neuper@37906: consts
neuper@37906: 
walther@60278:   is_expanded    :: "real => bool" ("_ is'_expanded")     (*RL->Poly.thy*)
walther@60278:   is_ratpolyexp  :: "real => bool" ("_ is'_ratpolyexp") 
jan@42300:   get_denominator :: "real => real"
walther@60017:   get_numerator   :: "real => real"           
neuper@37906: 
wneuper@59472: ML \<open>
neuper@52105: (*.the expression contains + - * ^ / only ?.*)
neuper@52105: fun is_ratpolyexp (Free _) = true
wenzelm@60309:   | is_ratpolyexp (Const (\<^const_name>\<open>plus\<close>,_) $ Free _ $ Free _) = true
wenzelm@60309:   | is_ratpolyexp (Const (\<^const_name>\<open>minus\<close>,_) $ Free _ $ Free _) = true
wenzelm@60309:   | is_ratpolyexp (Const (\<^const_name>\<open>times\<close>,_) $ Free _ $ Free _) = true
wenzelm@60405:   | is_ratpolyexp (Const (\<^const_name>\<open>realpow\<close>,_) $ Free _ $ Free _) = true
wenzelm@60309:   | is_ratpolyexp (Const (\<^const_name>\<open>divide\<close>,_) $ Free _ $ Free _) = true
wenzelm@60309:   | is_ratpolyexp (Const (\<^const_name>\<open>plus\<close>,_) $ t1 $ t2) = 
neuper@52105:                ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
wenzelm@60309:   | is_ratpolyexp (Const (\<^const_name>\<open>minus\<close>,_) $ t1 $ t2) = 
neuper@52105:                ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
wenzelm@60309:   | is_ratpolyexp (Const (\<^const_name>\<open>times\<close>,_) $ t1 $ t2) = 
neuper@52105:                ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
wenzelm@60405:   | is_ratpolyexp (Const (\<^const_name>\<open>realpow\<close>,_) $ t1 $ t2) = 
neuper@52105:                ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
wenzelm@60309:   | is_ratpolyexp (Const (\<^const_name>\<open>divide\<close>,_) $ t1 $ t2) = 
neuper@52105:                ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
walther@60355:   | is_ratpolyexp t = if TermC.is_num t then true else false;
neuper@37950: 
walther@60278: (*("is_ratpolyexp", ("Rational.is_ratpolyexp", eval_is_ratpolyexp ""))*)
neuper@52105: fun eval_is_ratpolyexp (thmid:string) _ 
Walther@60504: 		       (t as (Const (\<^const_name>\<open>Rational.is_ratpolyexp\<close>, _) $ arg)) ctxt =
neuper@52105:     if is_ratpolyexp arg
Walther@60504:     then SOME (TermC.mk_thmid thmid (UnparseC.term_in_ctxt ctxt arg) "", 
wneuper@59390: 	         HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
Walther@60504:     else SOME (TermC.mk_thmid thmid (UnparseC.term_in_ctxt ctxt arg) "", 
wneuper@59390: 	         HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
neuper@52105:   | eval_is_ratpolyexp _ _ _ _ = NONE; 
neuper@52105: 
neuper@52105: (*("get_denominator", ("Rational.get_denominator", eval_get_denominator ""))*)
neuper@52105: fun eval_get_denominator (thmid:string) _ 
walther@60335: 		      (t as Const (\<^const_name>\<open>Rational.get_denominator\<close>, _) $
wenzelm@60309:               (Const (\<^const_name>\<open>divide\<close>, _) $ _(*num*) $
Walther@60504:                 denom)) ctxt = 
Walther@60504:       SOME (TermC.mk_thmid thmid (UnparseC.term_in_ctxt ctxt denom) "", 
wneuper@59390: 	            HOLogic.Trueprop $ (TermC.mk_equality (t, denom)))
neuper@52105:   | eval_get_denominator _ _ _ _ = NONE; 
neuper@52105: 
neuper@52105: (*("get_numerator", ("Rational.get_numerator", eval_get_numerator ""))*)
neuper@52105: fun eval_get_numerator (thmid:string) _ 
walther@60335:       (t as Const (\<^const_name>\<open>Rational.get_numerator\<close>, _) $
wenzelm@60309:           (Const (\<^const_name>\<open>divide\<close>, _) $num
Walther@60504:             $denom )) ctxt = 
Walther@60504:     SOME (TermC.mk_thmid thmid (UnparseC.term_in_ctxt ctxt num) "", 
wneuper@59390: 	    HOLogic.Trueprop $ (TermC.mk_equality (t, num)))
neuper@52105:   | eval_get_numerator _ _ _ _ = NONE; 
wneuper@59472: \<close>
neuper@52105: 
wneuper@59472: section \<open>Theorems for rewriting\<close>
neuper@52105: 
neuper@52105: axiomatization (* naming due to Isabelle2002, but not contained in Isabelle2002; 
neuper@52105:                   many thms are due to RL and can be removed with updating the equation solver;
neuper@52105:                   TODO: replace by equivalent thms in recent Isabelle201x *) 
neuper@52105: where
neuper@52105:   mult_cross:      "[| b ~= 0; d ~= 0 |] ==> (a / b = c / d) = (a * d = b * c)" and
neuper@52105:   mult_cross1:     "   b ~= 0            ==> (a / b = c    ) = (a     = b * c)" and
neuper@52105:   mult_cross2:     "           d ~= 0    ==> (a     = c / d) = (a * d =     c)" and
neuper@37950:                   
neuper@52105:   add_minus:       "a + b - b = a"(*RL->Poly.thy*) and
neuper@52105:   add_minus1:      "a - b + b = a"(*RL->Poly.thy*) and
neuper@37950:                   
neuper@52105:   rat_mult:        "a / b * (c / d) = a * c / (b * d)"(*?Isa02*)  and
neuper@52105:   rat_mult2:       "a / b *  c      = a * c /  b     "(*?Isa02*) and
t@42211: 
neuper@52105:   rat_mult_poly_l: "c is_polyexp ==> c * (a / b) = c * a /  b" and
neuper@52105:   rat_mult_poly_r: "c is_polyexp ==> (a / b) * c = a * c /  b" and
neuper@37906: 
neuper@37906: (*real_times_divide1_eq .. Isa02*) 
neuper@52105:   real_times_divide_1_eq:  "-1 * (c / d) = -1 * c / d " and
walther@60385:   real_times_divide_num:   "a is_num ==> a * (c / d) = a * c / d " and
t@42211: 
neuper@52105:   real_mult_div_cancel2:   "k ~= 0 ==> m * k / (n * k) = m / n" and
neuper@37978: (*real_mult_div_cancel1:   "k ~= 0 ==> k * m / (k * n) = m / n"..Isa02*)
neuper@37906: 			  
neuper@52105:   real_divide_divide1:     "y ~= 0 ==> (u / v) / (y / z) = (u / v) * (z / y)" and
neuper@52105:   real_divide_divide1_mg:  "y ~= 0 ==> (u / v) / (y / z) = (u * z) / (y * v)" and
neuper@37978: (*real_divide_divide2_eq:  "x / y / z = x / (y * z)"..Isa02*)
neuper@37906: 			  
walther@60242:   rat_power:               "(a / b) \<up> n = (a \<up> n) / (b \<up> n)" and
neuper@37978: 
walther@60385:   rat_add:         "[| a is_num; b is_num; c is_num; d is_num |] ==> 
neuper@52105: 	           a / c + b / d = (a * d + b * c) / (c * d)" and
walther@60385:   rat_add_assoc:   "[| a is_num; b is_num; c is_num; d is_num |] ==> 
neuper@52105: 	           a / c +(b / d + e) = (a * d + b * c)/(d * c) + e" and
walther@60385:   rat_add1:        "[| a is_num; b is_num; c is_num |] ==> 
neuper@52105: 	           a / c + b / c = (a + b) / c" and
walther@60385:   rat_add1_assoc:   "[| a is_num; b is_num; c is_num |] ==> 
neuper@52105: 	           a / c + (b / c + e) = (a + b) / c + e" and
walther@60385:   rat_add2:        "[| a is_num; b is_num; c is_num |] ==> 
neuper@52105: 	           a / c + b = (a + b * c) / c" and
walther@60385:   rat_add2_assoc:  "[| a is_num; b is_num; c is_num |] ==> 
neuper@52105: 	           a / c + (b + e) = (a + b * c) / c + e" and
walther@60385:   rat_add3:        "[| a is_num; b is_num; c is_num |] ==> 
neuper@52105: 	           a + b / c = (a * c + b) / c" and
walther@60385:   rat_add3_assoc:   "[| a is_num; b is_num; c is_num |] ==> 
neuper@37950: 	           a + (b / c + e) = (a * c + b) / c + e"
neuper@37950: 
wneuper@59472: section \<open>Cancellation and addition of fractions\<close>
wneuper@59472: subsection \<open>Conversion term <--> poly\<close>
wneuper@59472: subsubsection \<open>Convert a term to the internal representation of a multivariate polynomial\<close>
wneuper@59472: ML \<open>
walther@60347: fun monom_of_term vs (_, es) (t as Const (\<^const_name>\<open>zero_class.zero\<close>, _)) =
walther@60347:     (0, list_update es (find_index (curry op = t) vs) 1)
walther@60347:   | monom_of_term vs (c, es) (t as Const _) =
wneuper@59532:     (c, list_update es (find_index (curry op = t) vs) 1)
walther@60335:   | monom_of_term _ (c, es) (t as (Const (\<^const_name>\<open>numeral\<close>, _) $ _)) =
walther@60319:     (t |> HOLogic.dest_number |> snd |> curry op * c, es) (*several numerals in one monom*)
walther@60335:   | monom_of_term _ (c, es) (t as (Const (\<^const_name>\<open>uminus\<close>, _) $ _)) =
walther@60319:     (t |> HOLogic.dest_number |> snd |> curry op * c, es) (*several numerals in one monom*)
walther@60318:   | monom_of_term  vs (c, es) (t as Free _) =
walther@60318:     (c, list_update es (find_index (curry op = t) vs) 1)
wenzelm@60405:   | monom_of_term  vs (c, es) (Const (\<^const_name>\<open>realpow\<close>, _) $ (b as Free _) $
walther@60335:       (e as Const (\<^const_name>\<open>numeral\<close>, _) $ _)) =
walther@60319:     (c, list_update es (find_index (curry op = b) vs) (e |> HOLogic.dest_number |> snd))
wenzelm@60405:   | monom_of_term  vs (c, es) (Const (\<^const_name>\<open>realpow\<close>, _) $ (b as Free _) $
walther@60335:       (e as Const (\<^const_name>\<open>uminus\<close>, _) $ _)) =
walther@60319:     (c, list_update es (find_index (curry op = b) vs) (e |> HOLogic.dest_number |> snd))
walther@60331: 
wenzelm@60309:   | monom_of_term vs (c, es) (Const (\<^const_name>\<open>times\<close>, _) $ m1 $ m2) =
neuper@52087:     let val (c', es') = monom_of_term vs (c, es) m1
neuper@52087:     in monom_of_term vs (c', es') m2 end
walther@59868:   | monom_of_term _ _ t = raise ERROR ("poly malformed 1 with " ^ UnparseC.term t)
neuper@52087: 
walther@60318: (*-------v------*)
walther@60347: fun monoms_of_term vs (t as Const (\<^const_name>\<open>zero_class.zero\<close>, _)) =
walther@60347:     [monom_of_term  vs (0, replicate (length vs) 0) t]
walther@60347:   | monoms_of_term vs (t as Const _) =
wneuper@59531:     [monom_of_term  vs (1, replicate (length vs) 0) t]
walther@60335:   | monoms_of_term vs (t as Const (\<^const_name>\<open>numeral\<close>, _) $ _) =
walther@60319:     [monom_of_term  vs (1, replicate (length vs) 0) t]
walther@60335:   | monoms_of_term vs (t as Const (\<^const_name>\<open>uminus\<close>, _) $ _) =
walther@60319:     [monom_of_term  vs (1, replicate (length vs) 0) t]
wneuper@59531:   | monoms_of_term vs (t as Free _) =
neuper@52087:     [monom_of_term  vs (1, replicate (length vs) 0) t]
wenzelm@60405:   | monoms_of_term vs (t as Const (\<^const_name>\<open>realpow\<close>, _) $ _ $  _) =
neuper@52087:     [monom_of_term  vs (1, replicate (length vs) 0) t]
wenzelm@60309:   | monoms_of_term vs (t as Const (\<^const_name>\<open>times\<close>, _) $ _ $  _) =
neuper@52087:     [monom_of_term  vs (1, replicate (length vs) 0) t]
wenzelm@60309:   | monoms_of_term vs (Const (\<^const_name>\<open>plus\<close>, _) $ ms1 $ ms2) =
neuper@52087:     (monoms_of_term vs ms1) @ (monoms_of_term vs ms2)
walther@59868:   | monoms_of_term _ t = raise ERROR ("poly malformed 2 with " ^ UnparseC.term t)
neuper@52087: 
neuper@52087: (* convert a term to the internal representation of a multivariate polynomial;
neuper@52087:   the conversion is quite liberal, see test --- fun poly_of_term ---:
neuper@52087: * the order of variables and the parentheses within a monomial are arbitrary
neuper@52087: * the coefficient may be somewhere
neuper@52087: * he order and the parentheses within monomials are arbitrary
neuper@52087: But the term must be completely expand + over * (laws of distributivity are not applicable).
neuper@52087: 
neuper@52087: The function requires the free variables as strings already given, 
neuper@52087: because the gcd involves 2 polynomials (with the same length for their list of exponents).
neuper@52087: *)
wenzelm@60309: fun poly_of_term vs (t as Const (\<^const_name>\<open>plus\<close>, _) $ _ $ _) =
neuper@52101:     (SOME (t |> monoms_of_term vs |> order)
neuper@52087:       handle ERROR _ => NONE)
walther@60347:   | poly_of_term vs t =   (* 0 for zero polynomial *)
neuper@52101:     (SOME [monom_of_term vs (1, replicate (length vs) 0) t]
neuper@52087:       handle ERROR _ => NONE)
neuper@52087: 
neuper@52087: fun is_poly t =
wneuper@59532:   let
wneuper@59532:     val vs = TermC.vars_of t
neuper@52087:   in 
neuper@52087:     case poly_of_term vs t of SOME _ => true | NONE => false
neuper@52087:   end
neuper@52105: val is_expanded = is_poly   (* TODO: check names *)
neuper@52105: val is_polynomial = is_poly (* TODO: check names *)
wneuper@59472: \<close>
neuper@52087: 
wneuper@59472: subsubsection \<open>Convert internal representation of a multivariate polynomial to a term\<close>
wneuper@59472: ML \<open>
neuper@52087: fun term_of_es _ _ _ [] = [] (*assumes same length for vs and es*)
wneuper@59532:   | term_of_es baseT expT (_ :: vs) (0 :: es) = [] @ term_of_es baseT expT vs es
wneuper@59532:   | term_of_es baseT expT (v :: vs) (1 :: es) = v :: term_of_es baseT expT vs es
neuper@52087:   | term_of_es baseT expT (v :: vs) (e :: es) =
wenzelm@60405:     Const (\<^const_name>\<open>realpow\<close>, [baseT, expT] ---> baseT) $ v $ (HOLogic.mk_number expT e)
wneuper@59532:     :: term_of_es baseT expT vs es
wneuper@59532:   | term_of_es _ _ _ _ = raise ERROR "term_of_es: length vs <> length es"
neuper@52087: 
neuper@52087: fun term_of_monom baseT expT vs ((c, es): monom) =
neuper@52087:     let val es' = term_of_es baseT expT vs es
neuper@52087:     in 
neuper@52087:       if c = 1 
neuper@52087:       then 
neuper@52087:         if es' = [] (*if es = [0,0,0,...]*)
walther@60317:         then HOLogic.mk_number baseT c
neuper@52087:         else foldl (HOLogic.mk_binop "Groups.times_class.times") (hd es', tl es')
walther@60317:       else foldl (HOLogic.mk_binop "Groups.times_class.times")
walther@60317:         (HOLogic.mk_number baseT c, es') 
neuper@52087:     end
neuper@52087: 
neuper@52087: fun term_of_poly baseT expT vs p =
wneuper@59190:   let val monos = map (term_of_monom baseT expT vs) p
wenzelm@60309:   in foldl (HOLogic.mk_binop \<^const_name>\<open>plus\<close>) (hd monos, tl monos) end
wneuper@59472: \<close>
neuper@52087: 
wneuper@59472: subsection \<open>Apply gcd_poly for cancelling and adding fractions as terms\<close>
wneuper@59472: ML \<open>
neuper@52091: fun mk_noteq_0 baseT t = 
walther@60335:   Const (\<^const_name>\<open>Not\<close>, HOLogic.boolT --> HOLogic.boolT) $ 
walther@60335:     (Const (\<^const_name>\<open>HOL.eq\<close>, [baseT, baseT] ---> HOLogic.boolT) $ t $ HOLogic.mk_number HOLogic.realT 0)
neuper@52091: 
neuper@52094: fun mk_asms baseT ts =
wneuper@59389:   let val as' = filter_out TermC.is_num ts (* asm like "2 ~= 0" is needless *)
neuper@52094:   in map (mk_noteq_0 baseT) as' end
wneuper@59472: \<close>
neuper@52094: 
wneuper@59472: subsubsection \<open>Factor out gcd for cancellation\<close>
wneuper@59472: ML \<open>
neuper@52091: fun check_fraction t =
walther@60269:   case t of
wenzelm@60309:     Const (\<^const_name>\<open>divide\<close>, _) $ numerator $ denominator
walther@60269:       => SOME (numerator, denominator)
walther@60269:   | _ => NONE
neuper@52091: 
neuper@52091: (* prepare a term for cancellation by factoring out the gcd
neuper@52091:   assumes: is a fraction with outmost "/"*)
walther@60372: fun factout_p_ (_: theory) t =
neuper@52091:   let val opt = check_fraction t
neuper@52091:   in
neuper@52091:     case opt of 
neuper@52091:       NONE => NONE
neuper@52091:     | SOME (numerator, denominator) =>
wneuper@59532:       let
wneuper@59532:         val vs = TermC.vars_of t
neuper@52091:         val baseT = type_of numerator
neuper@52091:         val expT = HOLogic.realT
neuper@52091:       in
neuper@52091:         case (poly_of_term vs numerator, poly_of_term vs denominator) of
neuper@52091:           (SOME a, SOME b) =>
neuper@52091:             let
neuper@52091:               val ((a', b'), c) = gcd_poly a b
neuper@52096:               val es = replicate (length vs) 0 
neuper@52096:             in
neuper@52096:               if c = [(1, es)] orelse c = [(~1, es)]
neuper@52096:               then NONE
neuper@52096:               else 
neuper@52096:                 let
neuper@52096:                   val b't = term_of_poly baseT expT vs b'
neuper@52096:                   val ct = term_of_poly baseT expT vs c
neuper@52096:                   val t' = 
wenzelm@60309:                     HOLogic.mk_binop \<^const_name>\<open>divide\<close> 
wenzelm@60309:                       (HOLogic.mk_binop \<^const_name>\<open>times\<close>
wneuper@59190:                         (term_of_poly baseT expT vs a', ct),
wenzelm@60309:                        HOLogic.mk_binop \<^const_name>\<open>times\<close> (b't, ct))
neuper@52105:                 in SOME (t', mk_asms baseT [b't, ct]) end
neuper@52096:             end
neuper@52091:         | _ => NONE : (term * term list) option
neuper@52091:       end
neuper@52091:   end
wneuper@59472: \<close>
neuper@52091: 
wneuper@59472: subsubsection \<open>Cancel a fraction\<close>
wneuper@59472: ML \<open>
neuper@52096: (* cancel a term by the gcd ("" denote terms with internal algebraic structure)
walther@60347:   cancel_p_ : theory \<Rightarrow> term  \<Rightarrow> (term \<times> term list) option
neuper@52096:   cancel_p_ thy "a / b" = SOME ("a' / b'", ["b' \<noteq> 0"])
neuper@52096:   assumes: a is_polynomial  \<and>  b is_polynomial  \<and>  b \<noteq> 0
neuper@52096:   yields
neuper@52096:     SOME ("a' / b'", ["b' \<noteq> 0"]). gcd_poly a b \<noteq> 1  \<and>  gcd_poly a b \<noteq> -1  \<and>  
neuper@52096:       a' * gcd_poly a b = a  \<and>  b' * gcd_poly a b = b
neuper@52096:     \<or> NONE *)
neuper@52101: fun cancel_p_ (_: theory) t =
neuper@52091:   let val opt = check_fraction t
neuper@52091:   in
neuper@52091:     case opt of 
neuper@52091:       NONE => NONE
neuper@52091:     | SOME (numerator, denominator) =>
wneuper@59532:       let
wneuper@59532:         val vs = TermC.vars_of t
neuper@52091:         val baseT = type_of numerator
neuper@52091:         val expT = HOLogic.realT
neuper@52091:       in
neuper@52091:         case (poly_of_term vs numerator, poly_of_term vs denominator) of
neuper@52091:           (SOME a, SOME b) =>
neuper@52091:             let
neuper@52091:               val ((a', b'), c) = gcd_poly a b
neuper@52096:               val es = replicate (length vs) 0 
neuper@52096:             in
neuper@52096:               if c = [(1, es)] orelse c = [(~1, es)]
neuper@52096:               then NONE
neuper@52096:               else 
neuper@52096:                 let
neuper@52096:                   val bt' = term_of_poly baseT expT vs b'
neuper@52096:                   val ct = term_of_poly baseT expT vs c
neuper@52096:                   val t' = 
wenzelm@60309:                     HOLogic.mk_binop \<^const_name>\<open>divide\<close> 
wneuper@59190:                       (term_of_poly baseT expT vs a', bt')
neuper@52096:                   val asm = mk_asms baseT [bt']
neuper@52096:                 in SOME (t', asm) end
neuper@52096:             end
neuper@52091:         | _ => NONE : (term * term list) option
neuper@52091:       end
neuper@52091:   end
wneuper@59472: \<close>
neuper@52091: 
wneuper@59472: subsubsection \<open>Factor out to a common denominator for addition\<close>
wneuper@59472: ML \<open>
neuper@52101: (* addition of fractions allows (at most) one non-fraction (a monomial) *)
neuper@52101: fun check_frac_sum 
wenzelm@60309:     (Const (\<^const_name>\<open>plus\<close>, _) $ 
wenzelm@60309:       (Const (\<^const_name>\<open>divide\<close>, _) $ n1 $ d1) $
wenzelm@60309:       (Const (\<^const_name>\<open>divide\<close>, _) $ n2 $ d2))
neuper@52091:     = SOME ((n1, d1), (n2, d2))
neuper@52101:   | check_frac_sum 
wenzelm@60309:     (Const (\<^const_name>\<open>plus\<close>, _) $ 
neuper@52091:       nofrac $ 
wenzelm@60309:       (Const (\<^const_name>\<open>divide\<close>, _) $ n2 $ d2))
walther@60347:     = SOME ((nofrac, HOLogic.mk_number HOLogic.realT 1), (n2, d2))
neuper@52101:   | check_frac_sum 
wenzelm@60309:     (Const (\<^const_name>\<open>plus\<close>, _) $ 
wenzelm@60309:       (Const (\<^const_name>\<open>divide\<close>, _) $ n1 $ d1) $ 
neuper@52091:       nofrac)
walther@60317:     = SOME ((n1, d1), (nofrac, HOLogic.mk_number HOLogic.realT 1))
neuper@52101:   | check_frac_sum _ = NONE  
neuper@52091: 
neuper@52091: (* prepare a term for addition by providing the least common denominator as a product
neuper@52091:   assumes: is a term with outmost "+" and at least one outmost "/" in respective summands*)
neuper@52101: fun common_nominator_p_ (_: theory) t =
neuper@52101:   let val opt = check_frac_sum t
neuper@52091:   in
neuper@52091:     case opt of 
neuper@52091:       NONE => NONE
neuper@52091:     | SOME ((n1, d1), (n2, d2)) =>
wneuper@59532:       let
wneuper@59532:         val vs = TermC.vars_of t
neuper@52091:       in
neuper@52091:         case (poly_of_term vs d1, poly_of_term vs d2) of
neuper@52091:           (SOME a, SOME b) =>
neuper@52091:             let
neuper@52091:               val ((a', b'), c) = gcd_poly a b
neuper@52101:               val (baseT, expT) = (type_of n1, HOLogic.realT)
wneuper@59190:               val [d1', d2', c'] = map (term_of_poly baseT expT vs) [a', b', c]
neuper@52091:               (*----- minimum of parentheses & nice result, but breaks tests: -------------
wenzelm@60309:               val denom = HOLogic.mk_binop \<^const_name>\<open>times\<close> 
wenzelm@60309:                 (HOLogic.mk_binop \<^const_name>\<open>times\<close> (d1', d2'), c') -------------*)
neuper@52101:               val denom =
neuper@52101:                 if c = [(1, replicate (length vs) 0)]
wenzelm@60309:                 then HOLogic.mk_binop \<^const_name>\<open>times\<close> (d1', d2')
neuper@52101:                 else
wenzelm@60309:                   HOLogic.mk_binop \<^const_name>\<open>times\<close> (c',
wenzelm@60309:                   HOLogic.mk_binop \<^const_name>\<open>times\<close> (d1', d2')) (*--------------*)
neuper@52091:               val t' =
wenzelm@60309:                 HOLogic.mk_binop \<^const_name>\<open>plus\<close>
wenzelm@60309:                   (HOLogic.mk_binop \<^const_name>\<open>divide\<close>
wenzelm@60309:                     (HOLogic.mk_binop \<^const_name>\<open>times\<close> (n1, d2'), denom),
wenzelm@60309:                   HOLogic.mk_binop \<^const_name>\<open>divide\<close> 
wenzelm@60309:                     (HOLogic.mk_binop \<^const_name>\<open>times\<close> (n2, d1'), denom))
neuper@52094:               val asm = mk_asms baseT [d1', d2', c']
neuper@52091:             in SOME (t', asm) end
neuper@52091:         | _ => NONE : (term * term list) option
neuper@52091:       end
neuper@52091:   end
wneuper@59472: \<close>
neuper@52105: 
wneuper@59472: subsubsection \<open>Addition of at least one fraction within a sum\<close>
wneuper@59472: ML \<open>
neuper@52091: (* add fractions
neuper@52100:   assumes: is a term with outmost "+" and at least one outmost "/" in respective summands
walther@60347:   \<and> NONE of the summands is zero.
walther@60347:   NOTE: the case "(_ + _) + _" need not be considered due to iterated addition *)
neuper@52105: fun add_fraction_p_ (_: theory) t =
neuper@52101:   case check_frac_sum t of 
neuper@52101:     NONE => NONE
neuper@52101:   | SOME ((n1, d1), (n2, d2)) =>
wneuper@59532:     let
wneuper@59532:       val vs = TermC.vars_of t
neuper@52101:     in
neuper@52101:       case (poly_of_term vs n1, poly_of_term vs d1, poly_of_term vs n2, poly_of_term vs d2) of
neuper@52101:         (SOME _, SOME a, SOME _, SOME b) =>
neuper@52101:           let
neuper@52101:             val ((a', b'), c) = gcd_poly a b
neuper@52101:             val (baseT, expT) = (type_of n1, HOLogic.realT)
neuper@52101:             val nomin = term_of_poly baseT expT vs 
neuper@52101:               (((the (poly_of_term vs n1)) %%*%% b') %%+%% ((the (poly_of_term vs n2)) %%*%% a')) 
neuper@52101:             val denom = term_of_poly baseT expT vs ((c %%*%% a') %%*%% b')
wenzelm@60309:             val t' = HOLogic.mk_binop \<^const_name>\<open>divide\<close> (nomin, denom)
neuper@52101:           in SOME (t', mk_asms baseT [denom]) end
neuper@52101:       | _ => NONE : (term * term list) option
neuper@52101:     end
wneuper@59472: \<close>
neuper@52091: 
wneuper@59472: section \<open>Embed cancellation and addition into rewriting\<close>
wenzelm@60291: 
wneuper@59472: subsection \<open>Rulesets and predicate for embedding\<close>
wneuper@59472: ML \<open>
neuper@52105: (* evaluates conditions in calculate_Rational *)
neuper@52105: val calc_rat_erls =
s1210629013@55444:   prep_rls'
Walther@60509:     (Rule_Def.Repeat {id = "calc_rat_erls", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), 
walther@60389:       erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
walther@60358:       rules = [
walther@60358:         \<^rule_eval>\<open>matches\<close> (Prog_Expr.eval_matches "#matches_"),
walther@60358:         \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
walther@60385:         \<^rule_eval>\<open>is_num\<close> (Prog_Expr.eval_is_num "#is_num_"),
walther@60358:         \<^rule_thm>\<open>not_true\<close>,
walther@60358:         \<^rule_thm>\<open>not_false\<close>], 
walther@59878:       scr = Rule.Empty_Prog});
neuper@37950: 
neuper@52105: (* simplifies expressions with numerals;
neuper@52105:    does NOT rearrange the term by AC-rewriting; thus terms with variables 
neuper@52105:    need to have constants to be commuted together respectively           *)
neuper@52105: val calculate_Rational =
walther@59852:   prep_rls' (Rule_Set.merge "calculate_Rational"
Walther@60509:     (Rule_Def.Repeat {id = "divide", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), 
walther@59851:       erls = calc_rat_erls, srls = Rule_Set.Empty,
neuper@52105:       calc = [], errpatts = [],
walther@60358:       rules = [
walther@60358:         \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
neuper@37950: 
walther@60358:         \<^rule_thm_sym>\<open>minus_divide_left\<close>, (*SYM - ?x / ?y = - (?x / ?y)  may come from subst*)
wenzelm@60297:         \<^rule_thm>\<open>rat_add\<close>,
walther@60385:           (*"[| a is_num; b is_num; c is_num; d is_num |] ==> a / c + b / d = (a * d) / (c * d) + (b * c ) / (d * c)"*)
walther@60385:         \<^rule_thm>\<open>rat_add1\<close>, (*"[| a is_num; b is_num; c is_num |] ==> a / c + b / c = (a + b) / c"*)
walther@60385:         \<^rule_thm>\<open>rat_add2\<close>, (*"[| ?a is_num; ?b is_num; ?c is_num |] ==> ?a / ?c + ?b = (?a + ?b * ?c) / ?c"*)
walther@60385:         \<^rule_thm>\<open>rat_add3\<close>, (*"[| a is_num; b is_num; c is_num |] ==> a + b / c = (a * c) / c + b / c" *)
neuper@52105:         
walther@60358:         \<^rule_thm>\<open>rat_mult\<close>, (*a / b * (c / d) = a * c / (b * d)*)
walther@60358:         \<^rule_thm>\<open>times_divide_eq_right\<close>, (*?x * (?y / ?z) = ?x * ?y / ?z*)
walther@60358:         \<^rule_thm>\<open>times_divide_eq_left\<close>, (*?y / ?z * ?x = ?y * ?x / ?z*)
neuper@52105:         
walther@60358:         \<^rule_thm>\<open>real_divide_divide1\<close>, (*"?y ~= 0 ==> ?u / ?v / (?y / ?z) = ?u / ?v * (?z / ?y)"*)
walther@60358:         \<^rule_thm>\<open>divide_divide_eq_left\<close>, (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
neuper@52105:         
walther@60358:         \<^rule_thm>\<open>rat_power\<close>, (*"(?a / ?b)  \<up>  ?n = ?a  \<up>  ?n / ?b  \<up>  ?n"*)
neuper@52105:         
walther@60358:         \<^rule_thm>\<open>mult_cross\<close>,  (*"[| b ~= 0; d ~= 0 |] ==> (a / b = c / d) = (a * d = b * c)*)
walther@60358:         \<^rule_thm>\<open>mult_cross1\<close>, (*"   b ~= 0            ==> (a / b = c    ) = (a     = b * c)*)
walther@60358:         \<^rule_thm>\<open>mult_cross2\<close>  (*"           d ~= 0    ==> (a     = c / d) = (a * d =     c)*)], 
walther@59878:       scr = Rule.Empty_Prog})
neuper@52105:     calculate_Poly);
neuper@37950: 
walther@60278: (*("is_expanded", ("Rational.is_expanded", eval_is_expanded ""))*)
neuper@37950: fun eval_is_expanded (thmid:string) _ 
Walther@60504: 		       (t as (Const (\<^const_name>\<open>Rational.is_expanded\<close>, _) $ arg)) ctxt = 
neuper@37950:     if is_expanded arg
Walther@60504:     then SOME (TermC.mk_thmid thmid (UnparseC.term_in_ctxt ctxt arg) "", 
wneuper@59390: 	         HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
Walther@60504:     else SOME (TermC.mk_thmid thmid (UnparseC.term_in_ctxt ctxt arg) "", 
wneuper@59390: 	         HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
s1210629013@52159:   | eval_is_expanded _ _ _ _ = NONE;
wneuper@59472: \<close>
wenzelm@60313: calculation is_expanded = \<open>eval_is_expanded ""\<close>
wneuper@59472: ML \<open>
neuper@37950: val rational_erls = 
walther@59852:   Rule_Set.merge "rational_erls" calculate_Rational 
walther@60358:     (Rule_Set.append_rules "is_expanded" Atools_erls [
walther@60358:       \<^rule_eval>\<open>is_expanded\<close> (eval_is_expanded "")]);
wneuper@59472: \<close>
neuper@37950: 
wneuper@59472: subsection \<open>Embed cancellation into rewriting\<close>
wneuper@59472: ML \<open>
walther@59603: (**)local (* cancel_p *)
neuper@37950: 
walther@59852: val {rules = rules, rew_ord = (_, ro), ...} = Rule_Set.rep (assoc_rls' @{theory} "rev_rew_p");
neuper@37950: 
neuper@52105: fun init_state thy eval_rls ro t =
neuper@52105:   let
neuper@52105:     val SOME (t', _) = factout_p_ thy t;
neuper@52105:     val SOME (t'', asm) = cancel_p_ thy t;
Walther@60500:     val der = Derive.steps_reverse (Proof_Context.init_global thy) eval_rls rules ro NONE t';
neuper@52105:     val der = der @ 
wenzelm@60297:       [(\<^rule_thm>\<open>real_mult_div_cancel2\<close>, (t'', asm))]
walther@60017:     val rs = (Rule.distinct' o (map #1)) der
walther@60017:   	val rs = filter_out (ThmC.member'
neuper@52105:   	  ["sym_real_add_zero_left", "sym_real_mult_0", "sym_real_mult_1"]) rs
neuper@52105:   in (t, t'', [rs(*one in order to ease locate_rule*)], der) end;
neuper@37950: 
neuper@52105: fun locate_rule thy eval_rls ro [rs] t r =
walther@59876:     if member op = ((map (Rule.thm_id)) rs) (Rule.thm_id r)
neuper@52105:     then 
Walther@60500:       let val ropt = Rewrite.rewrite_ (Proof_Context.init_global thy) ro eval_rls true (Rule.thm r) t;
neuper@52105:       in
neuper@52105:         case ropt of SOME ta => [(r, ta)]
walther@59733: 	      | NONE => ((*tracing 
walther@59876: 	          ("### locate_rule:  rewrite " ^ Rule.thm_id r ^ " " ^ UnparseC.term t ^ " = NONE");*) []) 
neuper@52105: 			end
walther@59876:     else ((*tracing ("### locate_rule:  " ^ Rule.thm_id r ^ " not mem rrls");*) [])
walther@59962:   | locate_rule _ _ _ _ _ _ = raise ERROR "locate_rule: doesnt match rev-sets in istate";
neuper@37950: 
neuper@52105: fun next_rule thy eval_rls ro [rs] t =
neuper@52105:     let
Walther@60500:       val der = Derive.do_one (Proof_Context.init_global thy) eval_rls rs ro NONE t;
neuper@52105:     in case der of (_, r, _) :: _ => SOME r | _ => NONE end
walther@59962:   | next_rule _ _ _ _ _ = raise ERROR ("next_rule: doesnt match rev-sets in istate");
neuper@37950: 
wneuper@59416: fun attach_form (_: Rule.rule list list) (_: term) (_: term) = 
wneuper@59416:   [(*TODO*)]: ( Rule.rule * (term * term list)) list;
neuper@37950: 
walther@59861: (**)in(**)
neuper@37950: 
neuper@52105: val cancel_p = 
walther@59850:   Rule_Set.Rrls {id = "cancel_p", prepat = [],
Walther@60506: 	rew_ord = ("ord_make_polynomial", ord_make_polynomial false \<^theory>),
neuper@52105: 	erls = rational_erls, 
neuper@52105: 	calc = 
wenzelm@60309: 	  [("PLUS", (\<^const_name>\<open>plus\<close>, (**)eval_binop "#add_")),
wenzelm@60309: 	  ("TIMES" , (\<^const_name>\<open>times\<close>, (**)eval_binop "#mult_")),
wenzelm@60309: 	  ("DIVIDE", (\<^const_name>\<open>divide\<close>, Prog_Expr.eval_cancel "#divide_e")),
wenzelm@60405: 	  ("POWER", (\<^const_name>\<open>realpow\<close>, (**)eval_binop "#power_"))],
neuper@52105:     errpatts = [],
neuper@52105: 	scr =
wenzelm@60291: 	  Rule.Rfuns {init_state  = init_state \<^theory> Atools_erls ro,
wenzelm@60291: 		normal_form = cancel_p_ \<^theory>, 
wenzelm@60291: 		locate_rule = locate_rule \<^theory> Atools_erls ro,
wenzelm@60291: 		next_rule   = next_rule \<^theory> Atools_erls ro,
neuper@52105: 		attach_form = attach_form}}
walther@59861: (**)end(* local cancel_p *)
wneuper@59472: \<close>
neuper@37950: 
wneuper@59472: subsection \<open>Embed addition into rewriting\<close>
wneuper@59472: ML \<open>
walther@59861: (**)local (* add_fractions_p *)
neuper@37950: 
walther@59852: (*val {rules = rules, rew_ord = (_, ro), ...} = Rule_Set.rep (assoc_rls "make_polynomial");*)
walther@59852: val {rules, rew_ord=(_,ro),...} = Rule_Set.rep (assoc_rls' @{theory} "rev_rew_p");
neuper@37950: 
neuper@52105: fun init_state thy eval_rls ro t =
neuper@52105:   let 
walther@60358:     val SOME (t', _) = common_nominator_p_ thy t;
neuper@52105:     val SOME (t'', asm) = add_fraction_p_ thy t;
Walther@60500:     val der = Derive.steps_reverse (Proof_Context.init_global thy) eval_rls rules ro NONE t';
neuper@52105:     val der = der @ 
wenzelm@60297:       [(\<^rule_thm>\<open>real_mult_div_cancel2\<close>, (t'',asm))]
walther@60017:     val rs = (Rule.distinct' o (map #1)) der;
walther@60017:     val rs = filter_out (ThmC.member'
neuper@52105:       ["sym_real_add_zero_left", "sym_real_mult_0", "sym_real_mult_1"]) rs;
neuper@52105:   in (t, t'', [rs(*here only _ONE_*)], der) end;
neuper@37950: 
neuper@52105: fun locate_rule thy eval_rls ro [rs] t r =
walther@59876:     if member op = ((map (Rule.thm_id)) rs) (Rule.thm_id r)
neuper@52105:     then 
Walther@60500:       let val ropt = Rewrite.rewrite_ (Proof_Context.init_global thy) ro eval_rls true (Rule.thm r) t;
neuper@52105:       in 
neuper@52105:         case ropt of
neuper@52105:           SOME ta => [(r, ta)]
neuper@52105: 	      | NONE => 
walther@59876: 	        ((*tracing ("### locate_rule:  rewrite " ^ Rule.thm_id r ^ " " ^ UnparseC.term t ^ " = NONE");*)
neuper@52105: 	        []) end
walther@59876:     else ((*tracing ("### locate_rule:  " ^ Rule.thm_id r ^ " not mem rrls");*) [])
walther@59962:   | locate_rule _ _ _ _ _ _ = raise ERROR "locate_rule: doesnt match rev-sets in istate";
neuper@37950: 
neuper@37950: fun next_rule thy eval_rls ro [rs] t =
Walther@60500:     let val der = Derive.do_one (Proof_Context.init_global thy) eval_rls rs ro NONE t;
neuper@52105:     in 
neuper@52105:       case der of
neuper@52105: 	      (_,r,_)::_ => SOME r
neuper@52105: 	    | _ => NONE
neuper@37950:     end
walther@59962:   | next_rule _ _ _ _ _ = raise ERROR ("next_rule: doesnt match rev-sets in istate");
neuper@37950: 
wenzelm@60291: val pat0 = TermC.parse_patt \<^theory> "?r/?s+?u/?v :: real";
wenzelm@60291: val pat1 = TermC.parse_patt \<^theory> "?r/?s+?u    :: real";
wenzelm@60291: val pat2 = TermC.parse_patt \<^theory> "?r   +?u/?v :: real";
neuper@48760: val prepat = [([@{term True}], pat0),
neuper@48760: 	      ([@{term True}], pat1),
neuper@48760: 	      ([@{term True}], pat2)];
walther@59861: (**)in(**)
neuper@37950: 
neuper@52105: val add_fractions_p =
walther@59850:   Rule_Set.Rrls {id = "add_fractions_p", prepat=prepat,
wenzelm@60291:     rew_ord = ("ord_make_polynomial", ord_make_polynomial false \<^theory>),
neuper@52105:     erls = rational_erls,
wenzelm@60309:     calc = [("PLUS", (\<^const_name>\<open>plus\<close>, (**)eval_binop "#add_")),
wenzelm@60309:       ("TIMES", (\<^const_name>\<open>times\<close>, (**)eval_binop "#mult_")),
wenzelm@60309:       ("DIVIDE", (\<^const_name>\<open>divide\<close>, Prog_Expr.eval_cancel "#divide_e")),
wenzelm@60405:       ("POWER", (\<^const_name>\<open>realpow\<close>, (**)eval_binop "#power_"))],
neuper@52105:     errpatts = [],
wenzelm@60291:     scr = Rule.Rfuns {init_state  = init_state \<^theory> Atools_erls ro,
wenzelm@60291:       normal_form = add_fraction_p_ \<^theory>,
wenzelm@60291:       locate_rule = locate_rule \<^theory> Atools_erls ro,
wenzelm@60291:       next_rule   = next_rule \<^theory> Atools_erls ro,
neuper@52105:       attach_form = attach_form}}
walther@59861: (**)end(*local add_fractions_p *)
wneuper@59472: \<close>
neuper@37950: 
wneuper@59472: subsection \<open>Cancelling and adding all occurrences in a term /////////////////////////////\<close>
wneuper@59472: ML \<open>
neuper@52105: (*copying cancel_p_rls + add her caused error in interface.sml*)
wneuper@59472: \<close>
neuper@42451: 
wneuper@59472: section \<open>Rulesets for general simplification\<close>
wneuper@59472: ML \<open>
neuper@37950: (*.all powers over + distributed; atoms over * collected, other distributed
neuper@37950:    contains absolute minimum of thms for context in norm_Rational .*)
s1210629013@55444: val powers = prep_rls'(
Walther@60509:   Rule_Def.Repeat {id = "powers", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.function_empty), 
walther@59851:       erls = powers_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
walther@60358:       rules = [
walther@60358:         \<^rule_thm>\<open>realpow_multI\<close>, (*"(r * s)  \<up>  n = r  \<up>  n * s  \<up>  n"*)
walther@60358:         \<^rule_thm>\<open>realpow_pow\<close>, (*"(a  \<up>  b)  \<up>  c = a  \<up>  (b * c)"*)
walther@60358:         \<^rule_thm>\<open>realpow_oneI\<close>, (*"r  \<up>  1 = r"*)
walther@60358:         \<^rule_thm>\<open>realpow_minus_even\<close>, (*"n is_even ==> (- r)  \<up>  n = r  \<up>  n" ?-->discard_minus?*)
walther@60358:         \<^rule_thm>\<open>realpow_minus_odd\<close>, (*"Not (n is_even) ==> (- r)  \<up>  n = -1 * r  \<up>  n"*)
neuper@37950: 
walther@60358:         (*----- collect atoms over * -----*)
walther@60358:         \<^rule_thm>\<open>realpow_two_atom\<close>, (*"r is_atom ==> r * r = r  \<up>  2"*)
walther@60358:         \<^rule_thm>\<open>realpow_plus_1\<close>, (*"r is_atom ==> r * r  \<up>  n = r  \<up>  (n + 1)"*)
walther@60358:         \<^rule_thm>\<open>realpow_addI_atom\<close>, (*"r is_atom ==> r  \<up>  n * r  \<up>  m = r  \<up>  (n + m)"*)
walther@60358: 
walther@60358:         (*----- distribute none-atoms -----*)
walther@60358:         \<^rule_thm>\<open>realpow_def_atom\<close>, (*"[| 1 < n; ~ (r is_atom) |]==>r  \<up>  n = r * r  \<up>  (n + -1)"*)
walther@60358:         \<^rule_thm>\<open>realpow_eq_oneI\<close>, (*"1  \<up>  n = 1"*)
walther@60358:         \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")],
walther@60358:       scr = Rule.Empty_Prog});
walther@60358: 
walther@60385: \<close> ML \<open>
neuper@37950: (*.contains absolute minimum of thms for context in norm_Rational.*)
s1210629013@55444: val rat_mult_divide = prep_rls'(
walther@59851:   Rule_Def.Repeat {id = "rat_mult_divide", preconds = [], 
Walther@60509:       rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), 
walther@59852:       erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
walther@60358:       rules = [
walther@60358:        \<^rule_thm>\<open>rat_mult\<close>, (*(1)"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
walther@60358: 	       \<^rule_thm>\<open>times_divide_eq_right\<close>, (*(2)"?a * (?c / ?d) = ?a * ?c / ?d" must be [2],
walther@60358: 	         otherwise inv.to a / b / c = ...*)
walther@60358: 	       \<^rule_thm>\<open>times_divide_eq_left\<close>, (*"?a / ?b * ?c = ?a * ?c / ?b" order weights x \<up> n too much
walther@60358: 		       and does not commute a / b * c  \<up>  2 !*)
neuper@37950: 	       
walther@60358: 	       \<^rule_thm>\<open>divide_divide_eq_right\<close>, (*"?x / (?y / ?z) = ?x * ?z / ?y"*)
walther@60358: 	       \<^rule_thm>\<open>divide_divide_eq_left\<close>, (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
walther@60358: 	       \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e")],
walther@60358:       scr = Rule.Empty_Prog});
neuper@37979: 
walther@60385: \<close> ML \<open>
neuper@37950: (*.contains absolute minimum of thms for context in norm_Rational.*)
s1210629013@55444: val reduce_0_1_2 = prep_rls'(
Walther@60509:   Rule_Def.Repeat{id = "reduce_0_1_2", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
walther@60358:     erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
walther@60358:     rules = [
walther@60393:       \<^rule_thm>\<open>div_by_1\<close>, (*"?x / 1 = ?x"*)
walther@60358: 	    \<^rule_thm>\<open>mult_1_left\<close>, (*"1 * z = z"*)
walther@60389: 	    \<^rule_thm>\<open>minus_zero\<close>, (*"- 0 = 0"*)
walther@60358: 	    (*\<^rule_thm>\<open>real_mult_minus1\<close>, "-1 * z = - z"*)
walther@60358: 	    (*\<^rule_thm>\<open>real_minus_mult_cancel\<close>, "- ?x * - ?y = ?x * ?y"*)
walther@60358:     
walther@60358:     
walther@60358:       \<^rule_thm>\<open>mult_zero_left\<close>, (*"0 * z = 0"*)
walther@60358:       \<^rule_thm>\<open>add_0_left\<close>, (*"0 + z = z"*)
walther@60358:       (*\<^rule_thm>\<open>right_minus\<close>, "?z + - ?z = 0"*)
walther@60358:     
walther@60358:       \<^rule_thm_sym>\<open>real_mult_2\<close>,	 (*"z1 + z1 = 2 * z1"*)
walther@60358:       \<^rule_thm>\<open>real_mult_2_assoc\<close>, (*"z1 + (z1 + k) = 2 * z1 + k"*)
walther@60358:     
walther@60358:       \<^rule_thm>\<open>division_ring_divide_zero\<close> (*"0 / ?x = 0"*)],
walther@60358:     scr = Rule.Empty_Prog});
neuper@37950: 
neuper@37950: (*erls for calculate_Rational; 
neuper@37950:   make local with FIXX@ME result:term *term list WN0609???SKMG*)
s1210629013@55444: val norm_rat_erls = prep_rls'(
Walther@60509:   Rule_Def.Repeat {id = "norm_rat_erls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.function_empty), 
walther@60358:     erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
walther@60358:     rules = [
walther@60385:       \<^rule_eval>\<open>Prog_Expr.is_num\<close> (Prog_Expr.eval_is_num "#is_num_")
walther@60385: ],
walther@60358:     scr = Rule.Empty_Prog});
neuper@37979: 
walther@60385: \<close> ML \<open>
neuper@52105: (* consists of rls containing the absolute minimum of thms *)
walther@60358: (*
walther@60358:   which is now replaced by MGs version "norm_Rational" below
walther@60358: *)
s1210629013@55444: val norm_Rational_min = prep_rls'(
Walther@60509:   Rule_Def.Repeat {id = "norm_Rational_min", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.function_empty), 
walther@60358:     erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
walther@60358:     rules = [(*sequence given by operator precedence*)
walther@60358: 	     Rule.Rls_ discard_minus,
walther@60358: 	     Rule.Rls_ powers,
walther@60358: 	     Rule.Rls_ rat_mult_divide,
walther@60358: 	     Rule.Rls_ expand,
walther@60358: 	     Rule.Rls_ reduce_0_1_2,
walther@60358: 	     Rule.Rls_ order_add_mult,
walther@60358: 	     Rule.Rls_ collect_numerals,
walther@60358: 	     Rule.Rls_ add_fractions_p,
walther@60358: 	     Rule.Rls_ cancel_p
walther@60358: 	     ],
walther@60358:     scr = Rule.Empty_Prog});
neuper@37979: 
walther@60385: \<close> ML \<open>
s1210629013@55444: val norm_Rational_parenthesized = prep_rls'(
walther@59878:   Rule_Set.Sequence {id = "norm_Rational_parenthesized", preconds = []:term list, 
Walther@60509:     rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
walther@60358:     erls = Atools_erls, srls = Rule_Set.Empty,
walther@60358:     calc = [], errpatts = [],
walther@60358:     rules = [
walther@60393:       Rule.Rls_ norm_Rational_min,
walther@60358: 	    Rule.Rls_ discard_parentheses],
walther@60358:     scr = Rule.Empty_Prog});      
neuper@37950: 
neuper@37950: (*WN030318???SK: simplifies all but cancel and common_nominator*)
neuper@37950: val simplify_rational = 
walther@60358:   Rule_Set.merge "simplify_rational" expand_binoms
walther@60358:     (Rule_Set.append_rules "divide" calculate_Rational [
walther@60358:       \<^rule_thm>\<open>div_by_1\<close>, (*"?x / 1 = ?x"*)
walther@60358:       \<^rule_thm>\<open>rat_mult\<close>, (*(1)"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
walther@60358:       \<^rule_thm>\<open>times_divide_eq_right\<close>, (*(2)"?a * (?c / ?d) = ?a * ?c / ?d" must be [2],
walther@60358:   		   otherwise inv.to a / b / c = ...*)
walther@60358:       \<^rule_thm>\<open>times_divide_eq_left\<close>, (*"?a / ?b * ?c = ?a * ?c / ?b"*)
walther@60358:       \<^rule_thm>\<open>add_minus\<close>, (*"?a + ?b - ?b = ?a"*)
walther@60358:       \<^rule_thm>\<open>add_minus1\<close>, (*"?a - ?b + ?b = ?a"*)
walther@60358:       \<^rule_thm>\<open>divide_minus1\<close> (*"?x / -1 = - ?x"*)]);
walther@60358: 
s1210629013@55444: val add_fractions_p_rls = prep_rls'(
Walther@60509:   Rule_Def.Repeat {id = "add_fractions_p_rls", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), 
walther@59852: 	  erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
wneuper@59416: 	  rules = [Rule.Rls_ add_fractions_p], 
walther@59878: 	  scr = Rule.Empty_Prog});
neuper@37950: 
walther@59851: (* "Rule_Def.Repeat" causes repeated application of cancel_p to one and the same term *)
s1210629013@55444: val cancel_p_rls = prep_rls'(
walther@59851:   Rule_Def.Repeat 
Walther@60509:     {id = "cancel_p_rls", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), 
walther@59852:     erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
wneuper@59416:     rules = [Rule.Rls_ cancel_p], 
walther@59878: 	  scr = Rule.Empty_Prog});
neuper@52105: 
neuper@37950: (*. makes 'normal' fractions; 'is_polyexp' inhibits double fractions;
neuper@37950:     used in initial part norm_Rational_mg, see example DA-M02-main.p.60.*)
s1210629013@55444: val rat_mult_poly = prep_rls'(
Walther@60509:   Rule_Def.Repeat {id = "rat_mult_poly", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), 
walther@60358: 	  erls = Rule_Set.append_rules "Rule_Set.empty-is_polyexp" Rule_Set.empty [
walther@60358:      \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp "")],
walther@59851: 	  srls = Rule_Set.Empty, calc = [], errpatts = [],
walther@60358: 	  rules = [
walther@60358:       \<^rule_thm>\<open>rat_mult_poly_l\<close>, (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*)
walther@60358: 	    \<^rule_thm>\<open>rat_mult_poly_r\<close> (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*)], 
walther@59878: 	  scr = Rule.Empty_Prog});
neuper@37979: 
neuper@37950: (*. makes 'normal' fractions; 'is_polyexp' inhibits double fractions;
neuper@37950:     used in looping part norm_Rational_rls, see example DA-M02-main.p.60 
walther@59852:     .. WHERE THE LATTER DOES ALWAYS WORK, BECAUSE erls = Rule_Set.empty, 
wneuper@59416:     I.E. THE RESPECTIVE ASSUMPTION IS STORED AND Rule.Thm APPLIED; WN051028 
neuper@37950:     ... WN0609???MG.*)
s1210629013@55444: val rat_mult_div_pow = prep_rls'(
Walther@60509:   Rule_Def.Repeat {id = "rat_mult_div_pow", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.function_empty), 
walther@59852:     erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
walther@60358:     rules = [
walther@60358:       \<^rule_thm>\<open>rat_mult\<close>, (*"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
walther@60358:       \<^rule_thm>\<open>rat_mult_poly_l\<close>, (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*)
walther@60358:       \<^rule_thm>\<open>rat_mult_poly_r\<close>, (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*)
neuper@52105:       
walther@60358:       \<^rule_thm>\<open>real_divide_divide1_mg\<close>, (*"y ~= 0 ==> (u / v) / (y / z) = (u * z) / (y * v)"*)
walther@60358:       \<^rule_thm>\<open>divide_divide_eq_right\<close>, (*"?x / (?y / ?z) = ?x * ?z / ?y"*)
walther@60358:       \<^rule_thm>\<open>divide_divide_eq_left\<close>, (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
wenzelm@60294:       \<^rule_eval>\<open>divide\<close> (Prog_Expr.eval_cancel "#divide_e"),
neuper@52105:       
walther@60358:       \<^rule_thm>\<open>rat_power\<close> (*"(?a / ?b)  \<up>  ?n = ?a  \<up>  ?n / ?b  \<up>  ?n"*)],
walther@59878:     scr = Rule.Empty_Prog});
neuper@37950: 
s1210629013@55444: val rat_reduce_1 = prep_rls'(
Walther@60509:   Rule_Def.Repeat {id = "rat_reduce_1", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), 
walther@59852:     erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [], 
walther@60358:     rules = [
walther@60358:       \<^rule_thm>\<open>div_by_1\<close>, (*"?x / 1 = ?x"*)
walther@60358:       \<^rule_thm>\<open>mult_1_left\<close> (*"1 * z = z"*)],
walther@59878:     scr = Rule.Empty_Prog});
neuper@52105: 
neuper@52105: (* looping part of norm_Rational *)
s1210629013@55444: val norm_Rational_rls = prep_rls' (
Walther@60509:   Rule_Def.Repeat {id = "norm_Rational_rls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.function_empty), 
walther@59851:     erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
walther@60358:     rules = [
walther@60358:       Rule.Rls_ add_fractions_p_rls,
wneuper@59416:       Rule.Rls_ rat_mult_div_pow,
wneuper@59416:       Rule.Rls_ make_rat_poly_with_parentheses,
wneuper@59416:       Rule.Rls_ cancel_p_rls,
walther@60358:       Rule.Rls_ rat_reduce_1],
walther@59878:     scr = Rule.Empty_Prog});
neuper@52105: 
s1210629013@55444: val norm_Rational = prep_rls' (
walther@59878:   Rule_Set.Sequence 
Walther@60509:     {id = "norm_Rational", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty), 
walther@59851:     erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
walther@60358:     rules = [
walther@60358:       Rule.Rls_ discard_minus,
wneuper@59416:       Rule.Rls_ rat_mult_poly,             (* removes double fractions like a/b/c *)
wneuper@59416:       Rule.Rls_ make_rat_poly_with_parentheses,
wneuper@59416:       Rule.Rls_ cancel_p_rls,
wneuper@59416:       Rule.Rls_ norm_Rational_rls,         (* the main rls, looping (#) *)
walther@60358:       Rule.Rls_ discard_parentheses1],     (* mult only *)
walther@59878:     scr = Rule.Empty_Prog});
wneuper@59472: \<close>
neuper@52125: 
wenzelm@60289: rule_set_knowledge
wenzelm@60286:   calculate_Rational = calculate_Rational and
wenzelm@60286:   calc_rat_erls = calc_rat_erls and
wenzelm@60286:   rational_erls = rational_erls and
wenzelm@60286:   cancel_p = cancel_p and
wenzelm@60286:   add_fractions_p = add_fractions_p and
wenzelm@60286: 
wenzelm@60286:   add_fractions_p_rls = add_fractions_p_rls and
wenzelm@60286:   powers_erls = powers_erls and
wenzelm@60286:   powers = powers and
wenzelm@60286:   rat_mult_divide = rat_mult_divide and
wenzelm@60286:   reduce_0_1_2 = reduce_0_1_2 and
wenzelm@60286: 
wenzelm@60286:   rat_reduce_1 = rat_reduce_1 and
wenzelm@60286:   norm_rat_erls = norm_rat_erls and
wenzelm@60286:   norm_Rational = norm_Rational and
wenzelm@60286:   norm_Rational_rls = norm_Rational_rls and
wenzelm@60286:   norm_Rational_min = norm_Rational_min and
wenzelm@60286:   norm_Rational_parenthesized = norm_Rational_parenthesized and
wenzelm@60286: 
wenzelm@60286:   rat_mult_poly = rat_mult_poly and
wenzelm@60286:   rat_mult_div_pow = rat_mult_div_pow and
wenzelm@60286:   cancel_p_rls = cancel_p_rls
neuper@37950: 
wneuper@59472: section \<open>A problem for simplification of rationals\<close>
wenzelm@60306: 
wenzelm@60306: problem pbl_simp_rat : "rational/simplification" =
wenzelm@60306:   \<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)]\<close>
Walther@60449:   Method_Ref: "simplification/of_rationals"
wenzelm@60306:   CAS: "Simplify t_t"
wenzelm@60306:   Given: "Term t_t"
wenzelm@60306:   Where: "t_t is_ratpolyexp"
wenzelm@60306:   Find: "normalform n_n"
neuper@37950: 
wneuper@59472: section \<open>A methods for simplification of rationals\<close>
s1210629013@55373: (*WN061025 this methods script is copied from (auto-generated) script
s1210629013@55373:   of norm_Rational in order to ease repair on inform*)
wneuper@59545: 
wneuper@59504: partial_function (tailrec) simplify :: "real \<Rightarrow> real"
wneuper@59504:   where
walther@59716: "simplify term = (
walther@59637:   (Try (Rewrite_Set ''discard_minus'') #>
walther@59637:    Try (Rewrite_Set ''rat_mult_poly'') #>
walther@59637:    Try (Rewrite_Set ''make_rat_poly_with_parentheses'') #>
walther@59637:    Try (Rewrite_Set ''cancel_p_rls'') #>
walther@59635:    (Repeat (
walther@59637:      Try (Rewrite_Set ''add_fractions_p_rls'') #>
walther@59637:      Try (Rewrite_Set ''rat_mult_div_pow'') #>
walther@59637:      Try (Rewrite_Set ''make_rat_poly_with_parentheses'') #>
walther@59637:      Try (Rewrite_Set ''cancel_p_rls'') #>
walther@59637:      Try (Rewrite_Set ''rat_reduce_1''))) #>
walther@59635:    Try (Rewrite_Set ''discard_parentheses1''))
walther@59716:    term)"
wenzelm@60303: 
wenzelm@60303: 
wenzelm@60303: method met_simp_rat : "simplification/of_rationals" =
wenzelm@60303:   \<open>{rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty, 
wenzelm@60303:     prls = Rule_Set.append_rules "simplification_of_rationals_prls" Rule_Set.empty 
wenzelm@60303:       [(*for preds in where_*) \<^rule_eval>\<open>is_ratpolyexp\<close> (eval_is_ratpolyexp "")],
wenzelm@60303:     crls = Rule_Set.empty, errpats = [], nrls = norm_Rational_rls}\<close>
wenzelm@60303:   Program: simplify.simps
wenzelm@60303:   Given: "Term t_t"
wenzelm@60303:   Where: "t_t is_ratpolyexp"
wenzelm@60303:   Find: "normalform n_n"
wenzelm@60303: ML \<open>
walther@60278: \<close> ML \<open>
walther@60384: \<close> ML \<open>
wneuper@59472: \<close>
neuper@52105: end