(* rationals, fractions of multivariate polynomials over the real field

   author: isac team

   Copyright (c) isac team 2002, 2013

   Use is subject to license terms.

   depends on Poly (and not on Atools), because 

   fractions with _normalised_ polynomials are canceled, added, etc.

*)

theory Rational 

imports Poly GCD_Poly_ML

begin

section \<open>Constants for evaluation by "Rule.Calc"\<close>

consts

  is'_expanded    :: "real => bool" ("_ is'_expanded")     (*RL->Poly.thy*)

  is'_ratpolyexp  :: "real => bool" ("_ is'_ratpolyexp") 

  get_denominator :: "real => real"

  get_numerator   :: "real => real"

ML \<open>

(*.the expression contains + - * ^ / only ?.*)

fun is_ratpolyexp (Free _) = true

  | is_ratpolyexp (Const ("Groups.plus_class.plus",_) $ Free _ $ Free _) = true

  | is_ratpolyexp (Const ("Groups.minus_class.minus",_) $ Free _ $ Free _) = true

  | is_ratpolyexp (Const ("Groups.times_class.times",_) $ Free _ $ Free _) = true

  | is_ratpolyexp (Const ("Prog_Expr.pow",_) $ Free _ $ Free _) = true

  | is_ratpolyexp (Const ("Rings.divide_class.divide",_) $ Free _ $ Free _) = true

  | is_ratpolyexp (Const ("Groups.plus_class.plus",_) $ t1 $ t2) = 

               ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))

  | is_ratpolyexp (Const ("Groups.minus_class.minus",_) $ t1 $ t2) = 

               ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))

  | is_ratpolyexp (Const ("Groups.times_class.times",_) $ t1 $ t2) = 

               ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))

  | is_ratpolyexp (Const ("Prog_Expr.pow",_) $ t1 $ t2) = 

               ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))

  | is_ratpolyexp (Const ("Rings.divide_class.divide",_) $ t1 $ t2) = 

               ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))

  | is_ratpolyexp _ = false;

(*("is_ratpolyexp", ("Rational.is'_ratpolyexp", eval_is_ratpolyexp ""))*)

fun eval_is_ratpolyexp (thmid:string) _ 

		       (t as (Const("Rational.is'_ratpolyexp", _) $ arg)) thy =

    if is_ratpolyexp arg

    then SOME (TermC.mk_thmid thmid (Rule.term_to_string''' thy arg) "", 

	         HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))

    else SOME (TermC.mk_thmid thmid (Rule.term_to_string''' thy arg) "", 

	         HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))

  | eval_is_ratpolyexp _ _ _ _ = NONE; 

(*("get_denominator", ("Rational.get_denominator", eval_get_denominator ""))*)

fun eval_get_denominator (thmid:string) _ 

		      (t as Const ("Rational.get_denominator", _) $

              (Const ("Rings.divide_class.divide", _) $ _(*num*) $

                denom)) thy = 

      SOME (TermC.mk_thmid thmid (Rule.term_to_string''' thy denom) "", 

	            HOLogic.Trueprop $ (TermC.mk_equality (t, denom)))

  | eval_get_denominator _ _ _ _ = NONE; 

(*("get_numerator", ("Rational.get_numerator", eval_get_numerator ""))*)

fun eval_get_numerator (thmid:string) _ 

      (t as Const ("Rational.get_numerator", _) $

          (Const ("Rings.divide_class.divide", _) $num

            $denom )) thy = 

    SOME (TermC.mk_thmid thmid (Rule.term_to_string''' thy num) "", 

	    HOLogic.Trueprop $ (TermC.mk_equality (t, num)))

  | eval_get_numerator _ _ _ _ = NONE; 

\<close>

section \<open>Theorems for rewriting\<close>

axiomatization (* naming due to Isabelle2002, but not contained in Isabelle2002; 

                  many thms are due to RL and can be removed with updating the equation solver;

                  TODO: replace by equivalent thms in recent Isabelle201x *) 

where

  mult_cross:      "[| b ~= 0; d ~= 0 |] ==> (a / b = c / d) = (a * d = b * c)" and

  mult_cross1:     "   b ~= 0            ==> (a / b = c    ) = (a     = b * c)" and

  mult_cross2:     "           d ~= 0    ==> (a     = c / d) = (a * d =     c)" and

  add_minus:       "a + b - b = a"(*RL->Poly.thy*) and

  add_minus1:      "a - b + b = a"(*RL->Poly.thy*) and

  rat_mult:        "a / b * (c / d) = a * c / (b * d)"(*?Isa02*)  and

  rat_mult2:       "a / b *  c      = a * c /  b     "(*?Isa02*) and

  rat_mult_poly_l: "c is_polyexp ==> c * (a / b) = c * a /  b" and

  rat_mult_poly_r: "c is_polyexp ==> (a / b) * c = a * c /  b" and

(*real_times_divide1_eq .. Isa02*) 

  real_times_divide_1_eq:  "-1 * (c / d) = -1 * c / d " and

  real_times_divide_num:   "a is_const ==> a * (c / d) = a * c / d " and

  real_mult_div_cancel2:   "k ~= 0 ==> m * k / (n * k) = m / n" and

(*real_mult_div_cancel1:   "k ~= 0 ==> k * m / (k * n) = m / n"..Isa02*)

  real_divide_divide1:     "y ~= 0 ==> (u / v) / (y / z) = (u / v) * (z / y)" and

  real_divide_divide1_mg:  "y ~= 0 ==> (u / v) / (y / z) = (u * z) / (y * v)" and

(*real_divide_divide2_eq:  "x / y / z = x / (y * z)"..Isa02*)

  rat_power:               "(a / b)^^^n = (a^^^n) / (b^^^n)" and

  rat_add:         "[| a is_const; b is_const; c is_const; d is_const |] ==> 

	           a / c + b / d = (a * d + b * c) / (c * d)" and

  rat_add_assoc:   "[| a is_const; b is_const; c is_const; d is_const |] ==> 

	           a / c +(b / d + e) = (a * d + b * c)/(d * c) + e" and

  rat_add1:        "[| a is_const; b is_const; c is_const |] ==> 

	           a / c + b / c = (a + b) / c" and

  rat_add1_assoc:   "[| a is_const; b is_const; c is_const |] ==> 

	           a / c + (b / c + e) = (a + b) / c + e" and

  rat_add2:        "[| a is_const; b is_const; c is_const |] ==> 

	           a / c + b = (a + b * c) / c" and

  rat_add2_assoc:  "[| a is_const; b is_const; c is_const |] ==> 

	           a / c + (b + e) = (a + b * c) / c + e" and

  rat_add3:        "[| a is_const; b is_const; c is_const |] ==> 

	           a + b / c = (a * c + b) / c" and

  rat_add3_assoc:   "[| a is_const; b is_const; c is_const |] ==> 

	           a + (b / c + e) = (a * c + b) / c + e"

section \<open>Cancellation and addition of fractions\<close>

subsection \<open>Conversion term <--> poly\<close>

subsubsection \<open>Convert a term to the internal representation of a multivariate polynomial\<close>

ML \<open>

fun monom_of_term vs (c, es) (t as Const _) =

    (c, list_update es (find_index (curry op = t) vs) 1)

  | monom_of_term  vs (c, es) (t as Free (id, _)) =

    if TermC.is_num' id 

    then (id |> TermC.int_of_str_opt |> the |> curry op * c, es) (*several numerals in one monom*)

    else (c, list_update es (find_index (curry op = t) vs) 1)

  | monom_of_term  vs (c, es) (Const ("Prog_Expr.pow", _) $ (t as Free _) $ Free (e, _)) =

    (c, list_update es (find_index (curry op = t) vs) (the (TermC.int_of_str_opt e)))

  | monom_of_term vs (c, es) (Const ("Groups.times_class.times", _) $ m1 $ m2) =

    let val (c', es') = monom_of_term vs (c, es) m1

    in monom_of_term vs (c', es') m2 end

  | monom_of_term _ _ t = raise ERROR ("poly malformed 1 with " ^ Rule.term2str t)

fun monoms_of_term vs (t as Const _) =

    [monom_of_term  vs (1, replicate (length vs) 0) t]

  | monoms_of_term vs (t as Free _) =

    [monom_of_term  vs (1, replicate (length vs) 0) t]

  | monoms_of_term vs (t as Const ("Prog_Expr.pow", _) $ _ $  _) =

    [monom_of_term  vs (1, replicate (length vs) 0) t]

  | monoms_of_term vs (t as Const ("Groups.times_class.times", _) $ _ $  _) =

    [monom_of_term  vs (1, replicate (length vs) 0) t]

  | monoms_of_term vs (Const ("Groups.plus_class.plus", _) $ ms1 $ ms2) =

    (monoms_of_term vs ms1) @ (monoms_of_term vs ms2)

  | monoms_of_term _ t = raise ERROR ("poly malformed 2 with " ^ Rule.term2str t)

(* convert a term to the internal representation of a multivariate polynomial;

  the conversion is quite liberal, see test --- fun poly_of_term ---:

* the order of variables and the parentheses within a monomial are arbitrary

* the coefficient may be somewhere

* he order and the parentheses within monomials are arbitrary

But the term must be completely expand + over * (laws of distributivity are not applicable).

The function requires the free variables as strings already given, 

because the gcd involves 2 polynomials (with the same length for their list of exponents).

*)

fun poly_of_term vs (t as Const ("Groups.plus_class.plus", _) $ _ $ _) =

    (SOME (t |> monoms_of_term vs |> order)

      handle ERROR _ => NONE)

  | poly_of_term vs t =

    (SOME [monom_of_term vs (1, replicate (length vs) 0) t]

      handle ERROR _ => NONE)

fun is_poly t =

  let

    val vs = TermC.vars_of t

  in 

    case poly_of_term vs t of SOME _ => true | NONE => false

  end

val is_expanded = is_poly   (* TODO: check names *)

val is_polynomial = is_poly (* TODO: check names *)

\<close>

subsubsection \<open>Convert internal representation of a multivariate polynomial to a term\<close>

ML \<open>

fun term_of_es _ _ _ [] = [] (*assumes same length for vs and es*)

  | term_of_es baseT expT (_ :: vs) (0 :: es) = [] @ term_of_es baseT expT vs es

  | term_of_es baseT expT (v :: vs) (1 :: es) = v :: term_of_es baseT expT vs es

  | term_of_es baseT expT (v :: vs) (e :: es) =

    Const ("Prog_Expr.pow", [baseT, expT] ---> baseT) $ v $  (Free (TermC.isastr_of_int e, expT))

    :: term_of_es baseT expT vs es

  | term_of_es _ _ _ _ = raise ERROR "term_of_es: length vs <> length es"

fun term_of_monom baseT expT vs ((c, es): monom) =

    let val es' = term_of_es baseT expT vs es

    in 

      if c = 1 

      then 

        if es' = [] (*if es = [0,0,0,...]*)

        then Free (TermC.isastr_of_int c, baseT)

        else foldl (HOLogic.mk_binop "Groups.times_class.times") (hd es', tl es')

      else foldl (HOLogic.mk_binop "Groups.times_class.times") (Free (TermC.isastr_of_int c, baseT), es') 

    end

fun term_of_poly baseT expT vs p =

  let val monos = map (term_of_monom baseT expT vs) p

  in foldl (HOLogic.mk_binop "Groups.plus_class.plus") (hd monos, tl monos) end

\<close>

subsection \<open>Apply gcd_poly for cancelling and adding fractions as terms\<close>

ML \<open>

fun mk_noteq_0 baseT t = 

  Const ("HOL.Not", HOLogic.boolT --> HOLogic.boolT) $ 

    (Const ("HOL.eq", [baseT, baseT] ---> HOLogic.boolT) $ t $ Free ("0", HOLogic.realT))

fun mk_asms baseT ts =

  let val as' = filter_out TermC.is_num ts (* asm like "2 ~= 0" is needless *)

  in map (mk_noteq_0 baseT) as' end

\<close>

subsubsection \<open>Factor out gcd for cancellation\<close>

ML \<open>

fun check_fraction t =

  let val Const ("Rings.divide_class.divide", _) $ numerator $ denominator = t

  in SOME (numerator, denominator) end

  handle Bind => NONE

(* prepare a term for cancellation by factoring out the gcd

  assumes: is a fraction with outmost "/"*)

fun factout_p_ (thy: theory) t =

  let val opt = check_fraction t

  in

    case opt of 

      NONE => NONE

    | SOME (numerator, denominator) =>

      let

        val vs = TermC.vars_of t

        val baseT = type_of numerator

        val expT = HOLogic.realT

      in

        case (poly_of_term vs numerator, poly_of_term vs denominator) of

          (SOME a, SOME b) =>

            let

              val ((a', b'), c) = gcd_poly a b

              val es = replicate (length vs) 0 

            in

              if c = [(1, es)] orelse c = [(~1, es)]

              then NONE

              else 

                let

                  val b't = term_of_poly baseT expT vs b'

                  val ct = term_of_poly baseT expT vs c

                  val t' = 

                    HOLogic.mk_binop "Rings.divide_class.divide" 

                      (HOLogic.mk_binop "Groups.times_class.times"

                        (term_of_poly baseT expT vs a', ct),

                       HOLogic.mk_binop "Groups.times_class.times" (b't, ct))

                in SOME (t', mk_asms baseT [b't, ct]) end

            end

        | _ => NONE : (term * term list) option

      end

  end

\<close>

subsubsection \<open>Cancel a fraction\<close>

ML \<open>

(* cancel a term by the gcd ("" denote terms with internal algebraic structure)

  cancel_p_ :: theory \<Rightarrow> term  \<Rightarrow> (term \<times> term list) option

  cancel_p_ thy "a / b" = SOME ("a' / b'", ["b' \<noteq> 0"])

  assumes: a is_polynomial  \<and>  b is_polynomial  \<and>  b \<noteq> 0

  yields

    SOME ("a' / b'", ["b' \<noteq> 0"]). gcd_poly a b \<noteq> 1  \<and>  gcd_poly a b \<noteq> -1  \<and>  

      a' * gcd_poly a b = a  \<and>  b' * gcd_poly a b = b

    \<or> NONE *)

fun cancel_p_ (_: theory) t =

  let val opt = check_fraction t

  in

    case opt of 

      NONE => NONE

    | SOME (numerator, denominator) =>

      let

        val vs = TermC.vars_of t

        val baseT = type_of numerator

        val expT = HOLogic.realT

      in

        case (poly_of_term vs numerator, poly_of_term vs denominator) of

          (SOME a, SOME b) =>

            let

              val ((a', b'), c) = gcd_poly a b

              val es = replicate (length vs) 0 

            in

              if c = [(1, es)] orelse c = [(~1, es)]

              then NONE

              else 

                let

                  val bt' = term_of_poly baseT expT vs b'

                  val ct = term_of_poly baseT expT vs c

                  val t' = 

                    HOLogic.mk_binop "Rings.divide_class.divide" 

                      (term_of_poly baseT expT vs a', bt')

                  val asm = mk_asms baseT [bt']

                in SOME (t', asm) end

            end

        | _ => NONE : (term * term list) option

      end

  end

\<close>

subsubsection \<open>Factor out to a common denominator for addition\<close>

ML \<open>

(* addition of fractions allows (at most) one non-fraction (a monomial) *)

fun check_frac_sum 

    (Const ("Groups.plus_class.plus", _) $ 

      (Const ("Rings.divide_class.divide", _) $ n1 $ d1) $

      (Const ("Rings.divide_class.divide", _) $ n2 $ d2))

    = SOME ((n1, d1), (n2, d2))

  | check_frac_sum 

    (Const ("Groups.plus_class.plus", _) $ 

      nofrac $ 

      (Const ("Rings.divide_class.divide", _) $ n2 $ d2))

    = SOME ((nofrac, Free ("1", HOLogic.realT)), (n2, d2))

  | check_frac_sum 

    (Const ("Groups.plus_class.plus", _) $ 

      (Const ("Rings.divide_class.divide", _) $ n1 $ d1) $ 

      nofrac)

    = SOME ((n1, d1), (nofrac, Free ("1", HOLogic.realT)))

  | check_frac_sum _ = NONE  

(* prepare a term for addition by providing the least common denominator as a product

  assumes: is a term with outmost "+" and at least one outmost "/" in respective summands*)

fun common_nominator_p_ (_: theory) t =

  let val opt = check_frac_sum t

  in

    case opt of 

      NONE => NONE

    | SOME ((n1, d1), (n2, d2)) =>

      let

        val vs = TermC.vars_of t

      in

        case (poly_of_term vs d1, poly_of_term vs d2) of

          (SOME a, SOME b) =>

            let

              val ((a', b'), c) = gcd_poly a b

              val (baseT, expT) = (type_of n1, HOLogic.realT)

              val [d1', d2', c'] = map (term_of_poly baseT expT vs) [a', b', c]

              (*----- minimum of parentheses & nice result, but breaks tests: -------------

              val denom = HOLogic.mk_binop "Groups.times_class.times" 

                (HOLogic.mk_binop "Groups.times_class.times" (d1', d2'), c') -------------*)

              val denom =

                if c = [(1, replicate (length vs) 0)]

                then HOLogic.mk_binop "Groups.times_class.times" (d1', d2')

                else

                  HOLogic.mk_binop "Groups.times_class.times" (c',

                  HOLogic.mk_binop "Groups.times_class.times" (d1', d2')) (*--------------*)

              val t' =

                HOLogic.mk_binop "Groups.plus_class.plus"

                  (HOLogic.mk_binop "Rings.divide_class.divide"

                    (HOLogic.mk_binop "Groups.times_class.times" (n1, d2'), denom),

                  HOLogic.mk_binop "Rings.divide_class.divide" 

                    (HOLogic.mk_binop "Groups.times_class.times" (n2, d1'), denom))

              val asm = mk_asms baseT [d1', d2', c']

            in SOME (t', asm) end

        | _ => NONE : (term * term list) option

      end

  end

\<close>

subsubsection \<open>Addition of at least one fraction within a sum\<close>

ML \<open>

(* add fractions

  assumes: is a term with outmost "+" and at least one outmost "/" in respective summands

  NOTE: the case "(_ + _) + _" need not be considered due to iterated addition.*)

fun add_fraction_p_ (_: theory) t =

  case check_frac_sum t of 

    NONE => NONE

  | SOME ((n1, d1), (n2, d2)) =>

    let

      val vs = TermC.vars_of t

    in

      case (poly_of_term vs n1, poly_of_term vs d1, poly_of_term vs n2, poly_of_term vs d2) of

        (SOME _, SOME a, SOME _, SOME b) =>

          let

            val ((a', b'), c) = gcd_poly a b

            val (baseT, expT) = (type_of n1, HOLogic.realT)

            val nomin = term_of_poly baseT expT vs 

              (((the (poly_of_term vs n1)) %%*%% b') %%+%% ((the (poly_of_term vs n2)) %%*%% a')) 

            val denom = term_of_poly baseT expT vs ((c %%*%% a') %%*%% b')

            val t' = HOLogic.mk_binop "Rings.divide_class.divide" (nomin, denom)

          in SOME (t', mk_asms baseT [denom]) end

      | _ => NONE : (term * term list) option

    end

\<close>

section \<open>Embed cancellation and addition into rewriting\<close>

ML \<open>val thy = @{theory}\<close>

subsection \<open>Rulesets and predicate for embedding\<close>

ML \<open>

(* evaluates conditions in calculate_Rational *)

val calc_rat_erls =

  prep_rls'

    (Rule.Rls {id = "calc_rat_erls", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord), 

      erls = Rule.e_rls, srls = Rule.Erls, calc = [], errpatts = [],

      rules = 

        [Rule.Calc ("HOL.eq", Prog_Expr.eval_equal "#equal_"),

        Rule.Calc ("Prog_Expr.is'_const", Prog_Expr.eval_const "#is_const_"),

        Rule.Thm ("not_true", TermC.num_str @{thm not_true}),

        Rule.Thm ("not_false", TermC.num_str @{thm not_false})], 

      scr = Rule.EmptyScr});

(* simplifies expressions with numerals;

   does NOT rearrange the term by AC-rewriting; thus terms with variables 

   need to have constants to be commuted together respectively           *)

val calculate_Rational =

  prep_rls' (Rule.merge_rls "calculate_Rational"

    (Rule.Rls {id = "divide", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord), 

      erls = calc_rat_erls, srls = Rule.Erls,

      calc = [], errpatts = [],

      rules = 

        [Rule.Calc ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),

        Rule.Thm ("minus_divide_left", TermC.num_str (@{thm minus_divide_left} RS @{thm sym})),

          (*SYM - ?x / ?y = - (?x / ?y)  may come from subst*)

        Rule.Thm ("rat_add", TermC.num_str @{thm rat_add}),

          (*"[| a is_const; b is_const; c is_const; d is_const |] ==> \

          \a / c + b / d = (a * d) / (c * d) + (b * c ) / (d * c)"*)

        Rule.Thm ("rat_add1", TermC.num_str @{thm rat_add1}),

          (*"[| a is_const; b is_const; c is_const |] ==> a / c + b / c = (a + b) / c"*)

        Rule.Thm ("rat_add2", TermC.num_str @{thm rat_add2}),

          (*"[| ?a is_const; ?b is_const; ?c is_const |] ==> ?a / ?c + ?b = (?a + ?b * ?c) / ?c"*)

        Rule.Thm ("rat_add3", TermC.num_str @{thm rat_add3}),

          (*"[| a is_const; b is_const; c is_const |] ==> a + b / c = (a * c) / c + b / c"\

          .... is_const to be omitted here FIXME*)

        Rule.Thm ("rat_mult", TermC.num_str @{thm rat_mult}), 

          (*a / b * (c / d) = a * c / (b * d)*)

        Rule.Thm ("times_divide_eq_right", TermC.num_str @{thm times_divide_eq_right}),

          (*?x * (?y / ?z) = ?x * ?y / ?z*)

        Rule.Thm ("times_divide_eq_left", TermC.num_str @{thm times_divide_eq_left}),

          (*?y / ?z * ?x = ?y * ?x / ?z*)

        Rule.Thm ("real_divide_divide1", TermC.num_str @{thm real_divide_divide1}),

          (*"?y ~= 0 ==> ?u / ?v / (?y / ?z) = ?u / ?v * (?z / ?y)"*)

        Rule.Thm ("divide_divide_eq_left", TermC.num_str @{thm divide_divide_eq_left}),

          (*"?x / ?y / ?z = ?x / (?y * ?z)"*)

        Rule.Thm ("rat_power", TermC.num_str @{thm rat_power}),

          (*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*)

        Rule.Thm ("mult_cross", TermC.num_str @{thm mult_cross}),

          (*"[| b ~= 0; d ~= 0 |] ==> (a / b = c / d) = (a * d = b * c)*)

        Rule.Thm ("mult_cross1", TermC.num_str @{thm mult_cross1}),

          (*"   b ~= 0            ==> (a / b = c    ) = (a     = b * c)*)

        Rule.Thm ("mult_cross2", TermC.num_str @{thm mult_cross2})

          (*"           d ~= 0    ==> (a     = c / d) = (a * d =     c)*)], 

      scr = Rule.EmptyScr})

    calculate_Poly);

(*("is_expanded", ("Rational.is'_expanded", eval_is_expanded ""))*)

fun eval_is_expanded (thmid:string) _ 

		       (t as (Const("Rational.is'_expanded", _) $ arg)) thy = 

    if is_expanded arg

    then SOME (TermC.mk_thmid thmid (Rule.term_to_string''' thy arg) "", 

	         HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))

    else SOME (TermC.mk_thmid thmid (Rule.term_to_string''' thy arg) "", 

	         HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))

  | eval_is_expanded _ _ _ _ = NONE;

\<close>

setup \<open>KEStore_Elems.add_calcs

  [("is_expanded", ("Rational.is'_expanded", eval_is_expanded ""))]\<close>

ML \<open>

val rational_erls = 

  Rule.merge_rls "rational_erls" calculate_Rational 

    (Rule.append_rls "is_expanded" Atools_erls 

      [Rule.Calc ("Rational.is'_expanded", eval_is_expanded "")]);

\<close>

subsection \<open>Embed cancellation into rewriting\<close>

ML \<open>

(**)local (* cancel_p *)

val {rules = rules, rew_ord = (_, ro), ...} = Rule.rep_rls (assoc_rls' @{theory} "rev_rew_p");

fun init_state thy eval_rls ro t =

  let

    val SOME (t', _) = factout_p_ thy t;

    val SOME (t'', asm) = cancel_p_ thy t;

    val der = Rtools.reverse_deriv thy eval_rls rules ro NONE t';

    val der = der @ 

      [(Rule.Thm ("real_mult_div_cancel2", TermC.num_str @{thm real_mult_div_cancel2}), (t'', asm))]

    val rs = (Rtools.distinct_Thm o (map #1)) der

  	val rs = filter_out (Rtools.eq_Thms 

  	  ["sym_real_add_zero_left", "sym_real_mult_0", "sym_real_mult_1"]) rs

  in (t, t'', [rs(*one in order to ease locate_rule*)], der) end;

fun locate_rule thy eval_rls ro [rs] t r =

    if member op = ((map (Celem.id_of_thm)) rs) (Celem.id_of_thm r)

    then 

      let val ropt = Rewrite.rewrite_ thy ro eval_rls true (Celem.thm_of_thm r) t;

      in

        case ropt of SOME ta => [(r, ta)]

	      | NONE => (tracing 

	          ("### locate_rule:  rewrite " ^ Celem.id_of_thm r ^ " " ^ Rule.term2str t ^ " = NONE"); []) 

			end

    else (tracing ("### locate_rule:  " ^ Celem.id_of_thm r ^ " not mem rrls"); [])

  | locate_rule _ _ _ _ _ _ = error "locate_rule: doesnt match rev-sets in istate";

fun next_rule thy eval_rls ro [rs] t =

    let

      val der = Rtools.make_deriv thy eval_rls rs ro NONE t;

    in case der of (_, r, _) :: _ => SOME r | _ => NONE end

  | next_rule _ _ _ _ _ = error ("next_rule: doesnt match rev-sets in istate");

fun attach_form (_: Rule.rule list list) (_: term) (_: term) = 

  [(*TODO*)]: ( Rule.rule * (term * term list)) list;

in

val cancel_p = 

  Rule.Rrls {id = "cancel_p", prepat = [],

	rew_ord=("ord_make_polynomial", ord_make_polynomial false thy),

	erls = rational_erls, 

	calc = 

	  [("PLUS", ("Groups.plus_class.plus", (**)eval_binop "#add_")),

	  ("TIMES" , ("Groups.times_class.times", (**)eval_binop "#mult_")),

	  ("DIVIDE", ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")),

	  ("POWER", ("Prog_Expr.pow", (**)eval_binop "#power_"))],

    errpatts = [],

	scr =

	  Rule.Rfuns {init_state  = init_state thy Atools_erls ro,

		normal_form = cancel_p_ thy, 

		locate_rule = locate_rule thy Atools_erls ro,

		next_rule   = next_rule thy Atools_erls ro,

		attach_form = attach_form}}

end; (* local cancel_p *)

\<close>

subsection \<open>Embed addition into rewriting\<close>

ML \<open>

(** )local ( * add_fractions_p *)

(*val {rules = rules, rew_ord = (_, ro), ...} = Rule.rep_rls (assoc_rls "make_polynomial");*)

val {rules, rew_ord=(_,ro),...} = Rule.rep_rls (assoc_rls' @{theory} "rev_rew_p");

fun init_state thy eval_rls ro t =

  let 

    val SOME (t',_) = common_nominator_p_ thy t;

    val SOME (t'', asm) = add_fraction_p_ thy t;

    val der = Rtools.reverse_deriv thy eval_rls rules ro NONE t';

    val der = der @ 

      [(Rule.Thm ("real_mult_div_cancel2", TermC.num_str @{thm real_mult_div_cancel2}), (t'',asm))]

    val rs = (Rtools.distinct_Thm o (map #1)) der;

    val rs = filter_out (Rtools.eq_Thms 

      ["sym_real_add_zero_left", "sym_real_mult_0", "sym_real_mult_1"]) rs;

  in (t, t'', [rs(*here only _ONE_*)], der) end;

\<close> ML \<open>

fun locate_rule thy eval_rls ro [rs] t r =

    if member op = ((map (Celem.id_of_thm)) rs) (Celem.id_of_thm r)

    then 

      let val ropt = Rewrite.rewrite_ thy ro eval_rls true (Celem.thm_of_thm r) t;

      in 

        case ropt of

          SOME ta => [(r, ta)]

	      | NONE => 

	        (tracing ("### locate_rule:  rewrite " ^ Celem.id_of_thm r ^ " " ^ Rule.term2str t ^ " = NONE");

	        []) end

    else (tracing ("### locate_rule:  " ^ Celem.id_of_thm r ^ " not mem rrls"); [])

  | locate_rule _ _ _ _ _ _ = error "locate_rule: doesnt match rev-sets in istate";

fun next_rule thy eval_rls ro [rs] t =

    let val der = Rtools.make_deriv thy eval_rls rs ro NONE t;

    in 

      case der of

	      (_,r,_)::_ => SOME r

	    | _ => NONE

    end

  | next_rule _ _ _ _ _ = error ("next_rule: doesnt match rev-sets in istate");

val pat0 = TermC.parse_patt thy "?r/?s+?u/?v :: real";

val pat1 = TermC.parse_patt thy "?r/?s+?u    :: real";

val pat2 = TermC.parse_patt thy "?r   +?u/?v :: real";

val prepat = [([@{term True}], pat0),

	      ([@{term True}], pat1),

	      ([@{term True}], pat2)];

(** )in( **)

val add_fractions_p =

  Rule.Rrls {id = "add_fractions_p", prepat=prepat,

    rew_ord = ("ord_make_polynomial", ord_make_polynomial false thy),

    erls = rational_erls,

    calc = [("PLUS", ("Groups.plus_class.plus", (**)eval_binop "#add_")),

      ("TIMES", ("Groups.times_class.times", (**)eval_binop "#mult_")),

      ("DIVIDE", ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")),

      ("POWER", ("Prog_Expr.pow", (**)eval_binop "#power_"))],

    errpatts = [],

    scr = Rule.Rfuns {init_state  = init_state thy Atools_erls ro,

      normal_form = add_fraction_p_ thy,

      locate_rule = locate_rule thy Atools_erls ro,

      next_rule   = next_rule thy Atools_erls ro,

      attach_form = attach_form}}

(** )end; ( *local add_fractions_p *)

\<close>

subsection \<open>Cancelling and adding all occurrences in a term /////////////////////////////\<close>

ML \<open>

(*copying cancel_p_rls + add her caused error in interface.sml*)

\<close>

section \<open>Rulesets for general simplification\<close>

ML \<open>

(*erls for calculate_Rational; make local with FIXX@ME result:term *term list*)

val powers_erls = prep_rls'(

  Rule.Rls {id = "powers_erls", preconds = [], rew_ord = ("dummy_ord",Rule.dummy_ord), 

      erls = Rule.e_rls, srls = Rule.Erls, calc = [], errpatts = [],

      rules = [Rule.Calc ("Prog_Expr.is'_atom", Prog_Expr.eval_is_atom "#is_atom_"),

	       Rule.Calc ("Prog_Expr.is'_even", Prog_Expr.eval_is_even "#is_even_"),

	       Rule.Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),

	       Rule.Thm ("not_false", TermC.num_str @{thm not_false}),

	       Rule.Thm ("not_true", TermC.num_str @{thm not_true}),

	       Rule.Calc ("Groups.plus_class.plus", (**)eval_binop "#add_")

	       ],

      scr = Rule.EmptyScr

      });

(*.all powers over + distributed; atoms over * collected, other distributed

   contains absolute minimum of thms for context in norm_Rational .*)

val powers = prep_rls'(

  Rule.Rls {id = "powers", preconds = [], rew_ord = ("dummy_ord",Rule.dummy_ord), 

      erls = powers_erls, srls = Rule.Erls, calc = [], errpatts = [],

      rules = [Rule.Thm ("realpow_multI", TermC.num_str @{thm realpow_multI}),

	       (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*)

	       Rule.Thm ("realpow_pow",TermC.num_str @{thm realpow_pow}),

	       (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*)

	       Rule.Thm ("realpow_oneI",TermC.num_str @{thm realpow_oneI}),

	       (*"r ^^^ 1 = r"*)

	       Rule.Thm ("realpow_minus_even",TermC.num_str @{thm realpow_minus_even}),

	       (*"n is_even ==> (- r) ^^^ n = r ^^^ n" ?-->discard_minus?*)

	       Rule.Thm ("realpow_minus_odd",TermC.num_str @{thm realpow_minus_odd}),

	       (*"Not (n is_even) ==> (- r) ^^^ n = -1 * r ^^^ n"*)

	       (*----- collect atoms over * -----*)

	       Rule.Thm ("realpow_two_atom",TermC.num_str @{thm realpow_two_atom}),	

	       (*"r is_atom ==> r * r = r ^^^ 2"*)

	       Rule.Thm ("realpow_plus_1",TermC.num_str @{thm realpow_plus_1}),		

	       (*"r is_atom ==> r * r ^^^ n = r ^^^ (n + 1)"*)

	       Rule.Thm ("realpow_addI_atom",TermC.num_str @{thm realpow_addI_atom}),

	       (*"r is_atom ==> r ^^^ n * r ^^^ m = r ^^^ (n + m)"*)

	       (*----- distribute none-atoms -----*)

	       Rule.Thm ("realpow_def_atom",TermC.num_str @{thm realpow_def_atom}),

	       (*"[| 1 < n; not(r is_atom) |]==>r ^^^ n = r * r ^^^ (n + -1)"*)

	       Rule.Thm ("realpow_eq_oneI",TermC.num_str @{thm realpow_eq_oneI}),

	       (*"1 ^^^ n = 1"*)

	       Rule.Calc ("Groups.plus_class.plus", (**)eval_binop "#add_")

	       ],

      scr = Rule.EmptyScr

      });

(*.contains absolute minimum of thms for context in norm_Rational.*)

val rat_mult_divide = prep_rls'(

  Rule.Rls {id = "rat_mult_divide", preconds = [], 

      rew_ord = ("dummy_ord", Rule.dummy_ord), 

      erls = Rule.e_rls, srls = Rule.Erls, calc = [], errpatts = [],

      rules = [Rule.Thm ("rat_mult",TermC.num_str @{thm rat_mult}),

	       (*(1)"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)

	       Rule.Thm ("times_divide_eq_right",TermC.num_str @{thm times_divide_eq_right}),

	       (*(2)"?a * (?c / ?d) = ?a * ?c / ?d" must be [2],

	       otherwise inv.to a / b / c = ...*)

	       Rule.Thm ("times_divide_eq_left",TermC.num_str @{thm times_divide_eq_left}),

	       (*"?a / ?b * ?c = ?a * ?c / ?b" order weights x^^^n too much

		     and does not commute a / b * c ^^^ 2 !*)

	       Rule.Thm ("divide_divide_eq_right", 

                     TermC.num_str @{thm divide_divide_eq_right}),

	       (*"?x / (?y / ?z) = ?x * ?z / ?y"*)

	       Rule.Thm ("divide_divide_eq_left",

                     TermC.num_str @{thm divide_divide_eq_left}),

	       (*"?x / ?y / ?z = ?x / (?y * ?z)"*)

	       Rule.Calc ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")

	       ],

      scr = Rule.EmptyScr

      });

(*.contains absolute minimum of thms for context in norm_Rational.*)

val reduce_0_1_2 = prep_rls'(

  Rule.Rls{id = "reduce_0_1_2", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord),

      erls = Rule.e_rls, srls = Rule.Erls, calc = [], errpatts = [],

      rules = [(*Rule.Thm ("divide_1",TermC.num_str @{thm divide_1}),

		 "?x / 1 = ?x" unnecess.for normalform*)

	       Rule.Thm ("mult_1_left",TermC.num_str @{thm mult_1_left}),                 

	       (*"1 * z = z"*)

	       (*Rule.Thm ("real_mult_minus1",TermC.num_str @{thm real_mult_minus1}),

	       "-1 * z = - z"*)

	       (*Rule.Thm ("real_minus_mult_cancel",TermC.num_str @{thm real_minus_mult_cancel}),

	       "- ?x * - ?y = ?x * ?y"*)

	       Rule.Thm ("mult_zero_left",TermC.num_str @{thm mult_zero_left}),        

	       (*"0 * z = 0"*)

	       Rule.Thm ("add_0_left",TermC.num_str @{thm add_0_left}),

	       (*"0 + z = z"*)

	       (*Rule.Thm ("right_minus",TermC.num_str @{thm right_minus}),

	       "?z + - ?z = 0"*)

	       Rule.Thm ("sym_real_mult_2",

                     TermC.num_str (@{thm real_mult_2} RS @{thm sym})),	

	       (*"z1 + z1 = 2 * z1"*)

	       Rule.Thm ("real_mult_2_assoc",TermC.num_str @{thm real_mult_2_assoc}),

	       (*"z1 + (z1 + k) = 2 * z1 + k"*)

	       Rule.Thm ("division_ring_divide_zero",TermC.num_str @{thm division_ring_divide_zero})

	       (*"0 / ?x = 0"*)

	       ], scr = Rule.EmptyScr});

(*erls for calculate_Rational; 

  make local with FIXX@ME result:term *term list WN0609???SKMG*)

val norm_rat_erls = prep_rls'(

  Rule.Rls {id = "norm_rat_erls", preconds = [], rew_ord = ("dummy_ord",Rule.dummy_ord), 

      erls = Rule.e_rls, srls = Rule.Erls, calc = [], errpatts = [],

      rules = [Rule.Calc ("Prog_Expr.is'_const", Prog_Expr.eval_const "#is_const_")

	       ], scr = Rule.EmptyScr});

(* consists of rls containing the absolute minimum of thms *)

(*040209: this version has been used by RL for his equations,

which is now replaced by MGs version "norm_Rational" below *)

val norm_Rational_min = prep_rls'(

  Rule.Rls {id = "norm_Rational_min", preconds = [], rew_ord = ("dummy_ord",Rule.dummy_ord), 

      erls = norm_rat_erls, srls = Rule.Erls, calc = [], errpatts = [],

      rules = [(*sequence given by operator precedence*)

	       Rule.Rls_ discard_minus,

	       Rule.Rls_ powers,

	       Rule.Rls_ rat_mult_divide,

	       Rule.Rls_ expand,

	       Rule.Rls_ reduce_0_1_2,

	       Rule.Rls_ order_add_mult,

	       Rule.Rls_ collect_numerals,

	       Rule.Rls_ add_fractions_p,

	       Rule.Rls_ cancel_p

	       ],

      scr = Rule.EmptyScr});

val norm_Rational_parenthesized = prep_rls'(

  Rule.Seq {id = "norm_Rational_parenthesized", preconds = []:term list, 

       rew_ord = ("dummy_ord", Rule.dummy_ord),

      erls = Atools_erls, srls = Rule.Erls,

      calc = [], errpatts = [],

      rules = [Rule.Rls_  norm_Rational_min,

	       Rule.Rls_ discard_parentheses

	       ],

      scr = Rule.EmptyScr});      

(*WN030318???SK: simplifies all but cancel and common_nominator*)

val simplify_rational = 

    Rule.merge_rls "simplify_rational" expand_binoms

    (Rule.append_rls "divide" calculate_Rational

		[Rule.Thm ("div_by_1",TermC.num_str @{thm div_by_1}),

		 (*"?x / 1 = ?x"*)

		 Rule.Thm ("rat_mult",TermC.num_str @{thm rat_mult}),

		 (*(1)"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)

		 Rule.Thm ("times_divide_eq_right",TermC.num_str @{thm times_divide_eq_right}),

		 (*(2)"?a * (?c / ?d) = ?a * ?c / ?d" must be [2],

		 otherwise inv.to a / b / c = ...*)

		 Rule.Thm ("times_divide_eq_left",TermC.num_str @{thm times_divide_eq_left}),

		 (*"?a / ?b * ?c = ?a * ?c / ?b"*)

		 Rule.Thm ("add_minus",TermC.num_str @{thm add_minus}),

		 (*"?a + ?b - ?b = ?a"*)

		 Rule.Thm ("add_minus1",TermC.num_str @{thm add_minus1}),

		 (*"?a - ?b + ?b = ?a"*)

		 Rule.Thm ("divide_minus1",TermC.num_str @{thm divide_minus1})

		 (*"?x / -1 = - ?x"*)

		 ]);

\<close>

ML \<open>

val add_fractions_p_rls = prep_rls'(

  Rule.Rls {id = "add_fractions_p_rls", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord), 

	  erls = Rule.e_rls, srls = Rule.Erls, calc = [], errpatts = [],

	  rules = [Rule.Rls_ add_fractions_p], 

	  scr = Rule.EmptyScr});

(* "Rule.Rls" causes repeated application of cancel_p to one and the same term *)

val cancel_p_rls = prep_rls'(

  Rule.Rls 

    {id = "cancel_p_rls", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord), 

    erls = Rule.e_rls, srls = Rule.Erls, calc = [], errpatts = [],

    rules = [Rule.Rls_ cancel_p], 

	  scr = Rule.EmptyScr});

(*. makes 'normal' fractions; 'is_polyexp' inhibits double fractions;

    used in initial part norm_Rational_mg, see example DA-M02-main.p.60.*)

val rat_mult_poly = prep_rls'(

  Rule.Rls {id = "rat_mult_poly", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord), 

	  erls = Rule.append_rls "Rule.e_rls-is_polyexp" Rule.e_rls [Rule.Calc ("Poly.is'_polyexp", eval_is_polyexp "")], 

	  srls = Rule.Erls, calc = [], errpatts = [],

	  rules = 

	    [Rule.Thm ("rat_mult_poly_l",TermC.num_str @{thm rat_mult_poly_l}),

	    (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*)

	    Rule.Thm ("rat_mult_poly_r",TermC.num_str @{thm rat_mult_poly_r})

	    (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*) ], 

	  scr = Rule.EmptyScr});

(*. makes 'normal' fractions; 'is_polyexp' inhibits double fractions;

    used in looping part norm_Rational_rls, see example DA-M02-main.p.60 

    .. WHERE THE LATTER DOES ALWAYS WORK, BECAUSE erls = Rule.e_rls, 

    I.E. THE RESPECTIVE ASSUMPTION IS STORED AND Rule.Thm APPLIED; WN051028 

    ... WN0609???MG.*)

val rat_mult_div_pow = prep_rls'(

  Rule.Rls {id = "rat_mult_div_pow", preconds = [], rew_ord = ("dummy_ord",Rule.dummy_ord), 

    erls = Rule.e_rls, srls = Rule.Erls, calc = [], errpatts = [],

    rules = [Rule.Thm ("rat_mult", TermC.num_str @{thm rat_mult}),

      (*"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)

      Rule.Thm ("rat_mult_poly_l", TermC.num_str @{thm rat_mult_poly_l}),

      (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*)

      Rule.Thm ("rat_mult_poly_r", TermC.num_str @{thm rat_mult_poly_r}),

      (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*)

      Rule.Thm ("real_divide_divide1_mg", TermC.num_str @{thm real_divide_divide1_mg}),

      (*"y ~= 0 ==> (u / v) / (y / z) = (u * z) / (y * v)"*)

      Rule.Thm ("divide_divide_eq_right", TermC.num_str @{thm divide_divide_eq_right}),

      (*"?x / (?y / ?z) = ?x * ?z / ?y"*)

      Rule.Thm ("divide_divide_eq_left", TermC.num_str @{thm divide_divide_eq_left}),

      (*"?x / ?y / ?z = ?x / (?y * ?z)"*)

      Rule.Calc ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),

      Rule.Thm ("rat_power", TermC.num_str @{thm rat_power})

      (*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*)

      ],

    scr = Rule.EmptyScr});

val rat_reduce_1 = prep_rls'(

  Rule.Rls {id = "rat_reduce_1", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord), 

    erls = Rule.e_rls, srls = Rule.Erls, calc = [], errpatts = [], 

    rules = 

      [Rule.Thm ("div_by_1", TermC.num_str @{thm div_by_1}),

      (*"?x / 1 = ?x"*)

      Rule.Thm ("mult_1_left", TermC.num_str @{thm mult_1_left})           

      (*"1 * z = z"*)

      ],

    scr = Rule.EmptyScr});

(* looping part of norm_Rational *)

val norm_Rational_rls = prep_rls' (

  Rule.Rls {id = "norm_Rational_rls", preconds = [], rew_ord = ("dummy_ord",Rule.dummy_ord), 

    erls = norm_rat_erls, srls = Rule.Erls, calc = [], errpatts = [],

    rules = [Rule.Rls_ add_fractions_p_rls,

      Rule.Rls_ rat_mult_div_pow,

      Rule.Rls_ make_rat_poly_with_parentheses,

      Rule.Rls_ cancel_p_rls,

      Rule.Rls_ rat_reduce_1

      ],

    scr = Rule.EmptyScr});

val norm_Rational = prep_rls' (

  Rule.Seq 

    {id = "norm_Rational", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord), 

    erls = norm_rat_erls, srls = Rule.Erls, calc = [], errpatts = [],

    rules = [Rule.Rls_ discard_minus,

      Rule.Rls_ rat_mult_poly,             (* removes double fractions like a/b/c *)

      Rule.Rls_ make_rat_poly_with_parentheses,

      Rule.Rls_ cancel_p_rls,

      Rule.Rls_ norm_Rational_rls,         (* the main rls, looping (#) *)

      Rule.Rls_ discard_parentheses1       (* mult only *)

      ],

    scr = Rule.EmptyScr});

\<close>

setup \<open>KEStore_Elems.add_rlss 

  [("calculate_Rational", (Context.theory_name @{theory}, calculate_Rational)), 

  ("calc_rat_erls", (Context.theory_name @{theory}, calc_rat_erls)), 

  ("rational_erls", (Context.theory_name @{theory}, rational_erls)), 

  ("cancel_p", (Context.theory_name @{theory}, cancel_p)), 

  ("add_fractions_p", (Context.theory_name @{theory}, add_fractions_p)),

  ("add_fractions_p_rls", (Context.theory_name @{theory}, add_fractions_p_rls)), 

  ("powers_erls", (Context.theory_name @{theory}, powers_erls)), 

  ("powers", (Context.theory_name @{theory}, powers)), 

  ("rat_mult_divide", (Context.theory_name @{theory}, rat_mult_divide)), 

  ("reduce_0_1_2", (Context.theory_name @{theory}, reduce_0_1_2)),

  ("rat_reduce_1", (Context.theory_name @{theory}, rat_reduce_1)), 

  ("norm_rat_erls", (Context.theory_name @{theory}, norm_rat_erls)), 

  ("norm_Rational", (Context.theory_name @{theory}, norm_Rational)), 

  ("norm_Rational_rls", (Context.theory_name @{theory}, norm_Rational_rls)), 

  ("norm_Rational_min", (Context.theory_name @{theory}, norm_Rational_min)),

  ("norm_Rational_parenthesized", (Context.theory_name @{theory}, norm_Rational_parenthesized)),

  ("rat_mult_poly", (Context.theory_name @{theory}, rat_mult_poly)), 

  ("rat_mult_div_pow", (Context.theory_name @{theory}, rat_mult_div_pow)), 

  ("cancel_p_rls", (Context.theory_name @{theory}, cancel_p_rls))]\<close>

section \<open>A problem for simplification of rationals\<close>

setup \<open>KEStore_Elems.add_pbts

  [(Specify.prep_pbt thy "pbl_simp_rat" [] Celem.e_pblID

      (["rational","simplification"],

        [("#Given" ,["Term t_t"]),

          ("#Where" ,["t_t is_ratpolyexp"]),

          ("#Find"  ,["normalform n_n"])],

        Rule.append_rls "e_rls" Rule.e_rls [(*for preds in where_*)], 

        SOME "Simplify t_t", [["simplification","of_rationals"]]))]\<close>

section \<open>A methods for simplification of rationals\<close>

(*WN061025 this methods script is copied from (auto-generated) script

  of norm_Rational in order to ease repair on inform*)

partial_function (tailrec) simplify :: "real \<Rightarrow> real"

  where

"simplify t_t =

  ((Try (Rewrite_Set ''discard_minus'' False) @@

    Try (Rewrite_Set ''rat_mult_poly'' False) @@

    Try (Rewrite_Set ''make_rat_poly_with_parentheses'' False) @@

    Try (Rewrite_Set ''cancel_p_rls'' False) @@

    (Repeat

     ((Try (Rewrite_Set ''add_fractions_p_rls'' False) @@

       Try (Rewrite_Set ''rat_mult_div_pow'' False) @@

       Try (Rewrite_Set ''make_rat_poly_with_parentheses'' False) @@

       Try (Rewrite_Set ''cancel_p_rls'' False) @@

       Try (Rewrite_Set ''rat_reduce_1'' False)))) @@

    Try (Rewrite_Set ''discard_parentheses1'' False))

   t_t)"

setup \<open>KEStore_Elems.add_mets

    [Specify.prep_met thy "met_simp_rat" [] Celem.e_metID

      (["simplification","of_rationals"],

        [("#Given" ,["Term t_t"]),

          ("#Where" ,["t_t is_ratpolyexp"]),

          ("#Find"  ,["normalform n_n"])],

	      {rew_ord'="tless_true", rls' = Rule.e_rls, calc = [], srls = Rule.e_rls, 

	        prls = Rule.append_rls "simplification_of_rationals_prls" Rule.e_rls 

				    [(*for preds in where_*) Rule.Calc ("Rational.is'_ratpolyexp", eval_is_ratpolyexp "")],

				  crls = Rule.e_rls, errpats = [], nrls = norm_Rational_rls},

				  @{thm simplify.simps})]

\<close>

end