src/HOL/arith_data.ML
changeset 10718 c058f78c3544
parent 10693 9e4a0e84d0d6
child 10766 ace2ba2d4fd1
     1.1 --- a/src/HOL/arith_data.ML	Thu Dec 21 16:18:40 2000 +0100
     1.2 +++ b/src/HOL/arith_data.ML	Thu Dec 21 16:19:39 2000 +0100
     1.3 @@ -306,9 +306,39 @@
     1.4  fun rat_of_term(numt,dent) =
     1.5    let val num = HOLogic.dest_binum numt and den = HOLogic.dest_binum dent
     1.6    in if den = 0 then raise Zero else int_ratdiv(num,den) end;
     1.7 - 
     1.8 +
     1.9 +(* Warning: in rare cases number_of encloses a non-numeral,
    1.10 +   in which case dest_binum raises TERM; hence all the handles below.
    1.11 +*)
    1.12 +
    1.13 +(* decompose nested multiplications, bracketing them to the right and combining all
    1.14 +   their coefficients
    1.15 +*)
    1.16 +
    1.17 +fun demult((mC as Const("op *",_)) $ s $ t,m) = ((case s of
    1.18 +        Const("Numeral.number_of",_)$n
    1.19 +        => demult(t,ratmul(m,rat_of_int(HOLogic.dest_binum n)))
    1.20 +      | Const("op *",_) $ s1 $ s2 => demult(mC $ s1 $ (mC $ s2 $ t),m)
    1.21 +      | Const("HOL.divide",_) $ numt $ (Const("Numeral.number_of",_)$dent) =>
    1.22 +          let val den = HOLogic.dest_binum dent
    1.23 +          in if den = 0 then raise Zero
    1.24 +             else demult(mC $ numt $ t,ratmul(m, ratinv(rat_of_int den)))
    1.25 +          end
    1.26 +      | _ => atomult(mC,s,t,m)
    1.27 +      ) handle TERM _ => atomult(mC,s,t,m))
    1.28 +  | demult(atom as Const("HOL.divide",_) $ t $ (Const("Numeral.number_of",_)$dent), m) =
    1.29 +      (let val den = HOLogic.dest_binum dent
    1.30 +       in if den = 0 then raise Zero else demult(t,ratmul(m, ratinv(rat_of_int den))) end
    1.31 +       handle TERM _ => (Some atom,m))
    1.32 +  | demult(t as Const("Numeral.number_of",_)$n,m) =
    1.33 +      ((None,ratmul(m,rat_of_int(HOLogic.dest_binum n)))
    1.34 +       handle TERM _ => (Some t,m))
    1.35 +  | demult(atom,m) = (Some atom,m)
    1.36 +
    1.37 +and atomult(mC,atom,t,m) = (case demult(t,m) of (None,m') => (Some atom,m')
    1.38 +                            | (Some t',m') => (Some(mC $ atom $ t'),m'))
    1.39 +
    1.40  fun decomp2 inj_consts (rel,lhs,rhs) =
    1.41 -
    1.42  let
    1.43  (* Turn term into list of summand * multiplicity plus a constant *)
    1.44  fun poly(Const("op +",_) $ s $ t, m, pi) = poly(s,m,poly(t,m,pi))
    1.45 @@ -318,33 +348,23 @@
    1.46    | poly(Const("uminus",_) $ t, m, pi) = poly(t,ratneg m,pi)
    1.47    | poly(Const("0",_), _, pi) = pi
    1.48    | poly(Const("Suc",_)$t, m, (p,i)) = poly(t, m, (p,ratadd(i,m)))
    1.49 -  | poly(all as Const("op *",_) $ (Const("Numeral.number_of",_)$c) $ t, m, pi)=
    1.50 -      (poly(t,ratmul(m, rat_of_int(HOLogic.dest_binum c)),pi)
    1.51 -       handle TERM _ => add_atom(all,m,pi))
    1.52 -  | poly(all as Const("op *",_) $ t $ (Const("Numeral.number_of",_)$c), m, pi)=
    1.53 -      (poly(t,ratmul(m, rat_of_int(HOLogic.dest_binum c)),pi)
    1.54 -       handle TERM _ => add_atom(all,m,pi))
    1.55 -  | poly(Const("op *",_) $ (Const("HOL.divide",_) $ (Const("Numeral.number_of",_)$numt) $
    1.56 -                                               (Const("Numeral.number_of",_)$dent)) $ t, m, pi) =
    1.57 -      poly(t,ratmul(m,rat_of_term(numt,dent)),pi)
    1.58 -  | poly(Const("op *",_) $ t $ (Const("HOL.divide",_) $ (Const("Numeral.number_of",_)$numt) $
    1.59 -                                               (Const("Numeral.number_of",_)$dent)), m, pi) =
    1.60 -      poly(t,ratmul(m,rat_of_term(numt,dent)),pi)
    1.61 -  | poly(all as Const("HOL.divide",_) $ t $ (Const("Numeral.number_of",_)$dent), m, pi) =
    1.62 -      let val den = HOLogic.dest_binum dent
    1.63 -      in if den = 0 then raise Zero else poly(t,ratmul(m, ratinv(rat_of_int den)),pi) end
    1.64 -  | poly(all as Const("Numeral.number_of",_)$t,m,(p,i)) =
    1.65 -     ((p,ratadd(i,ratmul(m,rat_of_int(HOLogic.dest_binum t))))
    1.66 -      handle TERM _ => add_atom(all,m,(p,i)))
    1.67 -  | poly(Const("HOL.divide",_) $ (Const("Numeral.number_of",_)$numt) $
    1.68 -                                 (Const("Numeral.number_of",_)$dent), m, (p,i)) =
    1.69 -      (p,ratadd(i,ratmul(m,rat_of_term(numt,dent))))
    1.70 +  | poly(t as Const("op *",_) $ _ $ _, m, pi as (p,i)) =
    1.71 +      (case demult(t,m) of
    1.72 +         (None,m') => (p,ratadd(i,m))
    1.73 +       | (Some u,m') => add_atom(u,m',pi))
    1.74 +  | poly(t as Const("HOL.divide",_) $ _ $ _, m, pi as (p,i)) =
    1.75 +      (case demult(t,m) of
    1.76 +         (None,m') => (p,ratadd(i,m))
    1.77 +       | (Some u,m') => add_atom(u,m',pi))
    1.78 +  | poly(all as (Const("Numeral.number_of",_)$t,m,(p,i))) =
    1.79 +      ((p,ratadd(i,ratmul(m,rat_of_int(HOLogic.dest_binum t))))
    1.80 +       handle TERM _ => add_atom all)
    1.81    | poly(all as Const f $ x, m, pi) =
    1.82        if f mem inj_consts then poly(x,m,pi) else add_atom(all,m,pi)
    1.83    | poly x  = add_atom x;
    1.84  
    1.85 -  val (p,i) = poly(lhs,rat_of_int 1,([],rat_of_int 0))
    1.86 -  and (q,j) = poly(rhs,rat_of_int 1,([],rat_of_int 0))
    1.87 +val (p,i) = poly(lhs,rat_of_int 1,([],rat_of_int 0))
    1.88 +and (q,j) = poly(rhs,rat_of_int 1,([],rat_of_int 0))
    1.89  
    1.90    in case rel of
    1.91         "op <"  => Some(p,i,"<",q,j)