# HG changeset patch
# User chaieb
# Date 1187795621 -7200
# Node ID b7c3ee2ca184c838ed0da080aa2684fa7b912735
# Parent  382f67ffbda51fd474208caa377a541be49c9ecf
More selective generalization : a*b is generalized whenever none of a and b is a number

diff -r 382f67ffbda5 -r b7c3ee2ca184 src/HOL/Tools/Qelim/presburger.ML
--- a/src/HOL/Tools/Qelim/presburger.ML	Wed Aug 22 17:13:40 2007 +0200
+++ b/src/HOL/Tools/Qelim/presburger.ML	Wed Aug 22 17:13:41 2007 +0200
@@ -52,10 +52,27 @@
 end;
 
 local
+ fun isnum t = case t of 
+   Const(@{const_name "HOL.zero"},_) => true
+ | Const(@{const_name "HOL.one"},_) => true
+ | @{term "Suc"}$s => isnum s
+ | @{term "nat"}$s => isnum s
+ | @{term "int"}$s => isnum s
+ | Const(@{const_name "uminus"},_)$s => isnum s
+ | Const(@{const_name "HOL.plus"},_)$l$r => isnum l andalso isnum r
+ | Const(@{const_name "HOL.times"},_)$l$r => isnum l andalso isnum r
+ | Const(@{const_name "HOL.minus"},_)$l$r => isnum l andalso isnum r
+ | Const(@{const_name "Nat.power"},_)$l$r => isnum l andalso isnum r
+ | Const(@{const_name "Divides.mod"},_)$l$r => isnum l andalso isnum r
+ | Const(@{const_name "Divides.div"},_)$l$r => isnum l andalso isnum r
+ | _ => can HOLogic.dest_number t orelse can HOLogic.dest_nat t
+
  fun ty cts t = 
  if not (typ_of (ctyp_of_term t) mem [HOLogic.intT, HOLogic.natT]) then false 
     else case term_of t of 
-      c$_$_ => not (member (op aconv) cts c)
+      c$l$r => if c mem [@{term"op *::int => _"}, @{term"op *::nat => _"}] 
+               then not (isnum l orelse isnum r)
+               else not (member (op aconv) cts c)
     | c$_ => not (member (op aconv) cts c)
     | c => not (member (op aconv) cts c)