# HG changeset patch
# User webertj
# Date 1154372209 -7200
# Node ID e76e77e0d615fe447ebf6aefac50ce4c52ac39f2
# Parent  3abe7dae681e934b6e41ea438cec974b0949ba49
fixed a bug in function poly: decomposition of products

diff -r 3abe7dae681e -r e76e77e0d615 src/HOL/arith_data.ML
--- a/src/HOL/arith_data.ML	Mon Jul 31 18:07:42 2006 +0200
+++ b/src/HOL/arith_data.ML	Mon Jul 31 20:56:49 2006 +0200
@@ -250,13 +250,14 @@
 fun nT (Type ("fun", [N, _])) = (N = HOLogic.natT)
   | nT _                      = false;
 
-fun add_atom (t, m, (p, i)) =
+fun add_atom (t : term) (m : Rat.rat) (p : (term * Rat.rat) list, i : Rat.rat) :
+             (term * Rat.rat) list * Rat.rat =
   case AList.lookup (op =) p t of NONE   => ((t, m) :: p, i)
                                 | SOME n => (AList.update (op =) (t, Rat.add (n, m)) p, i);
 
 exception Zero;
 
-fun rat_of_term (numt, dent) =
+fun rat_of_term (numt : term, dent : term) : Rat.rat =
 let
   val num = HOLogic.dest_binum numt
   val den = HOLogic.dest_binum dent
@@ -267,42 +268,41 @@
 (* Warning: in rare cases number_of encloses a non-numeral,
    in which case dest_binum raises TERM; hence all the handles below.
    Same for Suc-terms that turn out not to be numerals -
-   although the simplifier should eliminate those anyway...
+   although the simplifier should eliminate those anyway ...
 *)
+fun number_of_Sucs (Const ("Suc", _) $ n) : int =
+      number_of_Sucs n + 1
+  | number_of_Sucs t =
+      if HOLogic.is_zero t then 0 else raise TERM ("number_of_Sucs", []);
 
-fun number_of_Sucs (Const("Suc",_) $ n) = number_of_Sucs n + 1
-  | number_of_Sucs t = if HOLogic.is_zero t then 0
-                       else raise TERM("number_of_Sucs",[])
-
-(* decompose nested multiplications, bracketing them to the right and combining all
-   their coefficients
+(* decompose nested multiplications, bracketing them to the right and combining
+   all their coefficients
 *)
-
-fun demult (inj_consts : (string * Term.typ) list) =
+fun demult (inj_consts : (string * typ) list) : term * Rat.rat -> term option * Rat.rat =
 let
   fun demult ((mC as Const ("HOL.times", _)) $ s $ t, m) = (
-      (case s of
-        Const ("Numeral.number_of", _) $ n =>
-          demult (t, Rat.mult (m, Rat.rat_of_intinf (HOLogic.dest_binum n)))
-      | Const ("HOL.uminus", _) $ (Const ("Numeral.number_of", _) $ n) =>
-          demult (t, Rat.mult (m, Rat.rat_of_intinf (~(HOLogic.dest_binum n))))
-      | Const("Suc", _) $ _ =>
-          demult (t, Rat.mult (m, Rat.rat_of_int (number_of_Sucs s)))
-      | Const ("HOL.times", _) $ s1 $ s2 =>
-          demult (mC $ s1 $ (mC $ s2 $ t), m)
-      | Const ("HOL.divide", _) $ numt $ (Const ("Numeral.number_of", _) $ dent) =>
-          let
-            val den = HOLogic.dest_binum dent
-          in
-            if den = 0 then
-              raise Zero
-            else
-              demult (mC $ numt $ t, Rat.mult (m, Rat.inv (Rat.rat_of_intinf den)))
-          end
-      | _ =>
-          atomult (mC, s, t, m)
-      ) handle TERM _ => atomult (mC, s, t, m)
-    )
+    (case s of
+      Const ("Numeral.number_of", _) $ n =>
+        demult (t, Rat.mult (m, Rat.rat_of_intinf (HOLogic.dest_binum n)))
+    | Const ("HOL.uminus", _) $ (Const ("Numeral.number_of", _) $ n) =>
+        demult (t, Rat.mult (m, Rat.rat_of_intinf (~(HOLogic.dest_binum n))))
+    | Const("Suc", _) $ _ =>
+        demult (t, Rat.mult (m, Rat.rat_of_int (number_of_Sucs s)))
+    | Const ("HOL.times", _) $ s1 $ s2 =>
+        demult (mC $ s1 $ (mC $ s2 $ t), m)
+    | Const ("HOL.divide", _) $ numt $ (Const ("Numeral.number_of", _) $ dent) =>
+        let
+          val den = HOLogic.dest_binum dent
+        in
+          if den = 0 then
+            raise Zero
+          else
+            demult (mC $ numt $ t, Rat.mult (m, Rat.inv (Rat.rat_of_intinf den)))
+        end
+    | _ =>
+        atomult (mC, s, t, m)
+    ) handle TERM _ => atomult (mC, s, t, m)
+  )
     | demult (atom as Const("HOL.divide", _) $ t $ (Const ("Numeral.number_of", _) $ dent), m) =
       (let
         val den = HOLogic.dest_binum dent
@@ -329,31 +329,37 @@
   )
 in demult end;
 
-fun decomp2 inj_consts (rel, lhs, rhs) =
+fun decomp0 (inj_consts : (string * typ) list) (rel : string, lhs : term, rhs : term) :
+            ((term * Rat.rat) list * Rat.rat * string * (term * Rat.rat) list * Rat.rat) option =
 let
   (* Turn term into list of summand * multiplicity plus a constant *)
-  fun poly(Const("HOL.plus",_) $ s $ t, m, pi) = poly(s,m,poly(t,m,pi))
-    | poly(all as Const("HOL.minus",T) $ s $ t, m, pi) =
-        if nT T then add_atom(all,m,pi) else poly(s,m,poly(t,Rat.neg m,pi))
-    | poly(all as Const("HOL.uminus",T) $ t, m, pi) =
-        if nT T then add_atom(all,m,pi) else poly(t,Rat.neg m,pi)
-    | poly(Const("0",_), _, pi) = pi
-    | poly(Const("1",_), m, (p,i)) = (p,Rat.add(i,m))
-    | poly(Const("Suc",_)$t, m, (p,i)) = poly(t, m, (p,Rat.add(i,m)))
-    | poly(t as Const("HOL.times",_) $ _ $ _, m, pi as (p,i)) =
-        (case demult inj_consts (t,m) of
-           (NONE,m') => (p,Rat.add(i,m))
-         | (SOME u,m') => add_atom(u,m',pi))
-    | poly(t as Const("HOL.divide",_) $ _ $ _, m, pi as (p,i)) =
-        (case demult inj_consts (t,m) of
-           (NONE,m') => (p,Rat.add(i,m'))
-         | (SOME u,m') => add_atom(u,m',pi))
-    | poly(all as (Const("Numeral.number_of",_)$t,m,(p,i))) =
-        ((p,Rat.add(i,Rat.mult(m,Rat.rat_of_intinf(HOLogic.dest_binum t))))
-         handle TERM _ => add_atom all)
-    | poly(all as Const f $ x, m, pi) =
-        if f mem inj_consts then poly(x,m,pi) else add_atom(all,m,pi)
-    | poly x  = add_atom x
+  fun poly (Const ("HOL.plus", _) $ s $ t, m : Rat.rat, pi : (term * Rat.rat) list * Rat.rat) =
+        poly (s, m, poly (t, m, pi))
+    | poly (all as Const ("HOL.minus", T) $ s $ t, m, pi) =
+        if nT T then add_atom all m pi else poly (s, m, poly (t, Rat.neg m, pi))
+    | poly (all as Const ("HOL.uminus", T) $ t, m, pi) =
+        if nT T then add_atom all m pi else poly (t, Rat.neg m, pi)
+    | poly (Const ("0", _), _, pi) =
+        pi
+    | poly (Const ("1", _), m, (p, i)) =
+        (p, Rat.add (i, m))
+    | poly (Const ("Suc", _) $ t, m, (p, i)) =
+        poly (t, m, (p, Rat.add (i, m)))
+    | poly (all as Const ("HOL.times", _) $ _ $ _, m, pi as (p, i)) =
+        (case demult inj_consts (all, m) of
+           (NONE,   m') => (p, Rat.add (i, m'))
+         | (SOME u, m') => add_atom u m' pi)
+    | poly (all as Const ("HOL.divide", _) $ _ $ _, m, pi as (p, i)) =
+        (case demult inj_consts (all, m) of
+           (NONE,   m') => (p, Rat.add (i, m'))
+         | (SOME u, m') => add_atom u m' pi)
+    | poly (all as Const ("Numeral.number_of", _) $ t, m, pi as (p, i)) =
+        ((p, Rat.add (i, Rat.mult (m, Rat.rat_of_intinf (HOLogic.dest_binum t))))
+         handle TERM _ => add_atom all m pi)
+    | poly (all as Const f $ x, m, pi) =
+        if f mem inj_consts then poly (x, m, pi) else add_atom all m pi
+    | poly (all, m, pi) =
+        add_atom all m pi
   val (p, i) = poly (lhs, Rat.rat_of_int 1, ([], Rat.rat_of_int 0))
   val (q, j) = poly (rhs, Rat.rat_of_int 1, ([], Rat.rat_of_int 0))
 in
@@ -364,42 +370,48 @@
   | _                   => NONE
 end handle Zero => NONE;
 
-fun negate (SOME (x, i, rel, y, j, d)) = SOME (x, i, "~" ^ rel, y, j, d)
-  | negate NONE                        = NONE;
-
-fun of_lin_arith_sort sg U =
+fun of_lin_arith_sort sg (U : typ) : bool =
   Type.of_sort (Sign.tsig_of sg) (U, ["Ring_and_Field.ordered_idom"])
 
-fun allows_lin_arith sg discrete (U as Type (D, [])) =
+fun allows_lin_arith sg (discrete : string list) (U as Type (D, [])) : bool * bool =
   if of_lin_arith_sort sg U then
     (true, D mem discrete)
   else (* special cases *)
-    if D mem discrete then  (true, true)  else (false, false)
+    if D mem discrete then  (true, true)  else  (false, false)
   | allows_lin_arith sg discrete U =
   (of_lin_arith_sort sg U, false);
 
-fun decomp1 (sg, discrete, inj_consts) (T, xxx) =
-  (case T of
-     Type("fun",[U,_]) =>
-       (case allows_lin_arith sg discrete U of
-          (true,d) => (case decomp2 inj_consts xxx of NONE => NONE
-                       | SOME(p,i,rel,q,j) => SOME(p,i,rel,q,j,d))
-        | (false,_) => NONE)
-   | _ => NONE);
+fun decomp_typecheck (sg, discrete, inj_consts) (T : typ, xxx) : decompT option =
+  case T of
+    Type ("fun", [U, _]) =>
+      (case allows_lin_arith sg discrete U of
+        (true, d) =>
+          (case decomp0 inj_consts xxx of
+            NONE                   => NONE
+          | SOME (p, i, rel, q, j) => SOME (p, i, rel, q, j, d))
+      | (false, _) =>
+          NONE)
+  | _ => NONE;
 
-fun decomp2 data (_$(Const(rel,T)$lhs$rhs)) = decomp1 data (T,(rel,lhs,rhs))
-  | decomp2 data (_$(Const("Not",_)$(Const(rel,T)$lhs$rhs))) =
-      negate(decomp1 data (T,(rel,lhs,rhs)))
-  | decomp2 data _ = NONE
+fun negate (SOME (x, i, rel, y, j, d)) = SOME (x, i, "~" ^ rel, y, j, d)
+  | negate NONE                        = NONE;
 
-fun decomp sg =
+fun decomp_negation data (_ $ (Const (rel, T) $ lhs $ rhs)) : decompT option =
+      decomp_typecheck data (T, (rel, lhs, rhs))
+  | decomp_negation data (_ $ (Const ("Not", _) $ (Const (rel, T) $ lhs $ rhs))) =
+      negate (decomp_typecheck data (T, (rel, lhs, rhs)))
+  | decomp_negation data _ =
+      NONE;
+
+fun decomp sg : term -> decompT option =
 let
   val {discrete, inj_consts, ...} = ArithTheoryData.get sg
 in
-  decomp2 (sg,discrete,inj_consts)
+  decomp_negation (sg, discrete, inj_consts)
 end;
 
-fun number_of (n, T) = HOLogic.number_of_const T $ (HOLogic.mk_binum n);
+fun number_of (n : int, T : typ) =
+  HOLogic.number_of_const T $ (HOLogic.mk_binum n);
 
 (*---------------------------------------------------------------------------*)
 (* code that performs certain goal transformations for linear arithmetic     *)
@@ -794,7 +806,7 @@
 let
   (* repeatedly split (including newly emerging subgoals) until no further   *)
   (* splitting is possible                                                   *)
-  fun split_loop ([] : (typ list * term list) list) = []
+  fun split_loop ([] : (typ list * term list) list) = ([] : (typ list * term list) list)
     | split_loop (subgoal::subgoals)                = (
         case split_once_items sg subgoal of
           SOME new_subgoals => split_loop (new_subgoals @ subgoals)