--- 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)