1.1 --- a/src/Tools/isac/Knowledge/Rational.thy	Wed Aug 28 11:48:37 2013 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy	Fri Aug 30 13:43:30 2013 +0200
     1.3 @@ -316,20 +316,34 @@
     1.4            (SOME a, SOME b) =>
     1.5              let
     1.6                val ((a', b'), c) = gcd_poly a b
     1.7 -              val b't = term_of_poly baseT expT vs b'
     1.8 -              val ct = term_of_poly baseT expT vs c
     1.9 -              val t' = 
    1.10 -                HOLogic.mk_binop "Fields.inverse_class.divide" 
    1.11 -                  (HOLogic.mk_binop "Groups.times_class.times" (term_of_poly baseT expT vs a', ct),
    1.12 -                   HOLogic.mk_binop "Groups.times_class.times" (b't, ct))
    1.13 -              val asm = mk_asms baseT [b't, ct]
    1.14 -            in SOME (t', asm) end
    1.15 +              val es = replicate (length vs) 0 
    1.16 +            in
    1.17 +              if c = [(1, es)] orelse c = [(~1, es)]
    1.18 +              then NONE
    1.19 +              else 
    1.20 +                let
    1.21 +                  val b't = term_of_poly baseT expT vs b'
    1.22 +                  val ct = term_of_poly baseT expT vs c
    1.23 +                  val t' = 
    1.24 +                    HOLogic.mk_binop "Fields.inverse_class.divide" 
    1.25 +                      (HOLogic.mk_binop "Groups.times_class.times"
    1.26 +                        (term_of_poly baseT expT vs a', ct),
    1.27 +                       HOLogic.mk_binop "Groups.times_class.times" (b't, ct))
    1.28 +                  val asm = mk_asms baseT [b't, ct]
    1.29 +                in SOME (t', asm) end
    1.30 +            end
    1.31          | _ => NONE : (term * term list) option
    1.32        end
    1.33    end
    1.34  
    1.35 -(* prepare a term for cancellation by factoring out the gcd
    1.36 -  assumes: is a fraction with outmost "/"*)
    1.37 +(* cancel a term by the gcd ("" denote terms with internal algebraic structure)
    1.38 +  cancel_p_ :: theory \<Rightarrow> term  \<Rightarrow> (term \<times> term list) option
    1.39 +  cancel_p_ thy "a / b" = SOME ("a' / b'", ["b' \<noteq> 0"])
    1.40 +  assumes: a is_polynomial  \<and>  b is_polynomial  \<and>  b \<noteq> 0
    1.41 +  yields
    1.42 +    SOME ("a' / b'", ["b' \<noteq> 0"]). gcd_poly a b \<noteq> 1  \<and>  gcd_poly a b \<noteq> -1  \<and>  
    1.43 +      a' * gcd_poly a b = a  \<and>  b' * gcd_poly a b = b
    1.44 +    \<or> NONE *)
    1.45  fun cancel_p_ (thy: theory) t =
    1.46    let val opt = check_fraction t
    1.47    in
    1.48 @@ -345,13 +359,20 @@
    1.49            (SOME a, SOME b) =>
    1.50              let
    1.51                val ((a', b'), c) = gcd_poly a b
    1.52 -              val b't = term_of_poly baseT expT vs b'
    1.53 -              val ct = term_of_poly baseT expT vs c
    1.54 -              val t' = 
    1.55 -                HOLogic.mk_binop "Fields.inverse_class.divide" 
    1.56 -                  (term_of_poly baseT expT vs a', b't)
    1.57 -              val asm = mk_asms baseT [b't]
    1.58 -            in SOME (t', asm) end
    1.59 +              val es = replicate (length vs) 0 
    1.60 +            in
    1.61 +              if c = [(1, es)] orelse c = [(~1, es)]
    1.62 +              then NONE
    1.63 +              else 
    1.64 +                let
    1.65 +                  val bt' = term_of_poly baseT expT vs b'
    1.66 +                  val ct = term_of_poly baseT expT vs c
    1.67 +                  val t' = 
    1.68 +                    HOLogic.mk_binop "Fields.inverse_class.divide" 
    1.69 +                      (term_of_poly baseT expT vs a', bt')
    1.70 +                  val asm = mk_asms baseT [bt']
    1.71 +                in SOME (t', asm) end
    1.72 +            end
    1.73          | _ => NONE : (term * term list) option
    1.74        end
    1.75    end

     2.1 --- a/test/Tools/isac/Knowledge/rational.sml	Wed Aug 28 11:48:37 2013 +0200
     2.2 +++ b/test/Tools/isac/Knowledge/rational.sml	Fri Aug 30 13:43:30 2013 +0200
     2.3 @@ -346,6 +346,11 @@
     2.4  "-------- cancel_p from: Mathematik 1 Schalk Reniets Verlag ------------------";
     2.5  "-------- cancel_p from: Mathematik 1 Schalk Reniets Verlag ------------------";
     2.6  val thy  = @{theory "Rational"};
     2.7 +"-------- WN";
     2.8 +val t = str2term "(2 + -3 * x) / 9";
     2.9 +if NONE = rewrite_set_ thy false cancel_p t then ()
    2.10 +else error "rewrite_set_ cancel_p must return NONE, if the term cannot be cancelled";
    2.11 +
    2.12  "-------- example 186a";
    2.13  val t = str2term "(14 * x * y) / (x * y)";
    2.14    is_expanded (str2term "14 * x * y");