Counter example generation mods.

--- a/src/HOL/Integ/int_arith1.ML	Tue Aug 13 21:55:58 2002 +0200
+++ b/src/HOL/Integ/int_arith1.ML	Tue Aug 13 21:57:15 2002 +0200
@@ -404,7 +404,7 @@
      zmult_1, zmult_1_right,
      zmult_zminus, zmult_zminus_right,
      zminus_zadd_distrib, zminus_zminus, zmult_assoc,
-     int_0, int_1, zadd_int RS sym, int_Suc];
+     int_0, int_1, int_Suc, zadd_int RS sym, zmult_int RS sym];
 
 val simprocs = [Int_Times_Assoc.conv, Int_Numeral_Simprocs.combine_numerals]@
                Int_Numeral_Simprocs.cancel_numerals @

--- a/src/HOL/NatArith.thy	Tue Aug 13 21:55:58 2002 +0200
+++ b/src/HOL/NatArith.thy	Tue Aug 13 21:57:15 2002 +0200
@@ -32,9 +32,10 @@
 ML {*
  val nat_diff_split = thm "nat_diff_split";
  val nat_diff_split_asm = thm "nat_diff_split_asm";
-
+*}
+(* Careful: arith_tac produces counter examples!
 fun add_arith cs = cs addafter ("arith_tac", arith_tac);
-*} (* TODO: use arith_tac for force_tac in Provers/clasip.ML *)
+TODO: use arith_tac for force_tac in Provers/clasip.ML *)
 
 lemmas [arith_split] = nat_diff_split split_min split_max
 

--- a/src/HOL/arith_data.ML	Tue Aug 13 21:55:58 2002 +0200
+++ b/src/HOL/arith_data.ML	Tue Aug 13 21:57:15 2002 +0200
@@ -256,6 +256,8 @@
    their coefficients
 *)
 
+fun demult inj_consts =
+let
 fun demult((mC as Const("op *",_)) $ s $ t,m) = ((case s of
         Const("Numeral.number_of",_)$n
         => demult(t,ratmul(m,rat_of_int(HOLogic.dest_binum n)))
@@ -279,10 +281,13 @@
       ((None,ratmul(m,rat_of_int(HOLogic.dest_binum n)))
        handle TERM _ => (Some t,m))
   | demult(Const("uminus",_)$t, m) = demult(t,ratmul(m,rat_of_int(~1)))
+  | demult(t as Const f $ x, m) =
+      (if f mem inj_consts then Some x else Some t,m)
   | demult(atom,m) = (Some atom,m)
 
 and atomult(mC,atom,t,m) = (case demult(t,m) of (None,m') => (Some atom,m')
                             | (Some t',m') => (Some(mC $ atom $ t'),m'))
+in demult end;
 
 fun decomp2 inj_consts (rel,lhs,rhs) =
 let
@@ -296,11 +301,11 @@
   | poly(Const("1",_), m, (p,i)) = (p,ratadd(i,m))
   | poly(Const("Suc",_)$t, m, (p,i)) = poly(t, m, (p,ratadd(i,m)))
   | poly(t as Const("op *",_) $ _ $ _, m, pi as (p,i)) =
-      (case demult(t,m) of
+      (case demult inj_consts (t,m) of
          (None,m') => (p,ratadd(i,m))
        | (Some u,m') => add_atom(u,m',pi))
   | poly(t as Const("HOL.divide",_) $ _ $ _, m, pi as (p,i)) =
-      (case demult(t,m) of
+      (case demult inj_consts (t,m) of
          (None,m') => (p,ratadd(i,m))
        | (Some u,m') => add_atom(u,m',pi))
   | poly(all as (Const("Numeral.number_of",_)$t,m,(p,i))) =
@@ -350,7 +355,8 @@
 structure Fast_Arith =
   Fast_Lin_Arith(structure LA_Logic=LA_Logic and LA_Data=LA_Data_Ref);
 
-val fast_arith_tac = Fast_Arith.lin_arith_tac
+val fast_arith_tac    = Fast_Arith.lin_arith_tac false
+and fast_ex_arith_tac = Fast_Arith.lin_arith_tac
 and trace_arith    = Fast_Arith.trace;
 
 local
@@ -407,13 +413,18 @@
 *)
 local
 
-fun raw_arith_tac i st =
-  refute_tac (K true) (REPEAT o split_tac (#splits (ArithTheoryData.get_sg (Thm.sign_of_thm st))))
-             ((REPEAT_DETERM o etac linorder_neqE) THEN' fast_arith_tac) i st;
+fun raw_arith_tac ex i st =
+  refute_tac (K true)
+   (REPEAT o split_tac (#splits (ArithTheoryData.get_sg (Thm.sign_of_thm st))))
+   ((REPEAT_DETERM o etac linorder_neqE) THEN' fast_ex_arith_tac ex)
+   i st;
 
 in
 
-val arith_tac = fast_arith_tac ORELSE' (ObjectLogic.atomize_tac THEN' raw_arith_tac);
+val arith_tac = fast_arith_tac ORELSE'
+                (ObjectLogic.atomize_tac THEN' raw_arith_tac true);
+val silent_arith_tac = fast_arith_tac ORELSE'
+                       (ObjectLogic.atomize_tac THEN' raw_arith_tac false);
 
 fun arith_method prems =
   Method.METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ facts) THEN' arith_tac));