1.1 --- a/src/HOL/arith_data.ML	Fri Dec 01 19:44:48 2000 +0100
     1.2 +++ b/src/HOL/arith_data.ML	Fri Dec 01 19:53:29 2000 +0100
     1.3 @@ -265,24 +265,29 @@
     1.4  structure ArithTheoryDataArgs =
     1.5  struct
     1.6    val name = "HOL/arith";
     1.7 -  type T = {splits: thm list, discrete: (string * bool) list};
     1.8 +  type T = {splits: thm list, inj_consts: (string * typ)list, discrete: (string * bool) list};
     1.9  
    1.10 -  val empty = {splits = [], discrete = []};
    1.11 +  val empty = {splits = [], inj_consts = [], discrete = []};
    1.12    val copy = I;
    1.13    val prep_ext = I;
    1.14 -  fun merge ({splits = splits1, discrete = discrete1}, {splits = splits2, discrete = discrete2}) =
    1.15 +  fun merge ({splits= splits1, inj_consts= inj_consts1, discrete= discrete1},
    1.16 +             {splits= splits2, inj_consts= inj_consts2, discrete= discrete2}) =
    1.17     {splits = Drule.merge_rules (splits1, splits2),
    1.18 +    inj_consts = merge_lists inj_consts1 inj_consts2,
    1.19      discrete = merge_alists discrete1 discrete2};
    1.20    fun print _ _ = ();
    1.21  end;
    1.22  
    1.23  structure ArithTheoryData = TheoryDataFun(ArithTheoryDataArgs);
    1.24  
    1.25 -fun arith_split_add (thy, thm) = (ArithTheoryData.map (fn {splits, discrete} =>
    1.26 -  {splits = thm :: splits, discrete = discrete}) thy, thm);
    1.27 +fun arith_split_add (thy, thm) = (ArithTheoryData.map (fn {splits,inj_consts,discrete} =>
    1.28 +  {splits= thm::splits, inj_consts= inj_consts, discrete= discrete}) thy, thm);
    1.29  
    1.30 -fun arith_discrete d = ArithTheoryData.map (fn {splits, discrete} =>
    1.31 -  {splits = splits, discrete = d :: discrete});
    1.32 +fun arith_discrete d = ArithTheoryData.map (fn {splits,inj_consts,discrete} =>
    1.33 +  {splits = splits, inj_consts = inj_consts, discrete = d :: discrete});
    1.34 +
    1.35 +fun arith_inj_const c = ArithTheoryData.map (fn {splits,inj_consts,discrete} =>
    1.36 +  {splits = splits, inj_consts = c :: inj_consts, discrete = discrete});
    1.37  
    1.38  
    1.39  structure LA_Data_Ref: LIN_ARITH_DATA =
    1.40 @@ -296,6 +301,9 @@
    1.41  fun add_atom(t,m,(p,i)) = (case assoc(p,t) of None => ((t,m)::p,i)
    1.42                             | Some n => (overwrite(p,(t,n+m:int)), i));
    1.43  
    1.44 +fun decomp2 inj_consts (rel,lhs,rhs) =
    1.45 +
    1.46 +let
    1.47  (* Turn term into list of summand * multiplicity plus a constant *)
    1.48  fun poly(Const("op +",_) $ s $ t, m, pi) = poly(s,m,poly(t,m,pi))
    1.49    | poly(all as Const("op -",T) $ s $ t, m, pi) =
    1.50 @@ -313,10 +321,11 @@
    1.51    | poly(all as Const("Numeral.number_of",_)$t,m,(p,i)) =
    1.52       ((p,i + m*HOLogic.dest_binum t)
    1.53        handle TERM _ => add_atom(all,m,(p,i)))
    1.54 +  | poly(all as Const f $ x, m, pi) =
    1.55 +      if f mem inj_consts then poly(x,m,pi) else add_atom(all,m,pi)
    1.56    | poly x  = add_atom x;
    1.57  
    1.58 -fun decomp2(rel,lhs,rhs) =
    1.59 -  let val (p,i) = poly(lhs,1,([],0)) and (q,j) = poly(rhs,1,([],0))
    1.60 +  val (p,i) = poly(lhs,1,([],0)) and (q,j) = poly(rhs,1,([],0))
    1.61    in case rel of
    1.62         "op <"  => Some(p,i,"<",q,j)
    1.63       | "op <=" => Some(p,i,"<=",q,j)
    1.64 @@ -327,22 +336,24 @@
    1.65  fun negate(Some(x,i,rel,y,j,d)) = Some(x,i,"~"^rel,y,j,d)
    1.66    | negate None = None;
    1.67  
    1.68 -fun decomp1 discrete (T,xxx) =
    1.69 +fun decomp1 (discrete,inj_consts) (T,xxx) =
    1.70    (case T of
    1.71       Type("fun",[Type(D,[]),_]) =>
    1.72         (case assoc(discrete,D) of
    1.73            None => None
    1.74 -        | Some d => (case decomp2 xxx of
    1.75 +        | Some d => (case decomp2 inj_consts xxx of
    1.76                         None => None
    1.77                       | Some(p,i,rel,q,j) => Some(p,i,rel,q,j,d)))
    1.78     | _ => None);
    1.79  
    1.80 -fun decomp2 discrete (_$(Const(rel,T)$lhs$rhs)) = decomp1 discrete (T,(rel,lhs,rhs))
    1.81 -  | decomp2 discrete (_$(Const("Not",_)$(Const(rel,T)$lhs$rhs))) =
    1.82 -      negate(decomp1 discrete (T,(rel,lhs,rhs)))
    1.83 -  | decomp2 discrete _ = None
    1.84 +fun decomp2 data (_$(Const(rel,T)$lhs$rhs)) = decomp1 data (T,(rel,lhs,rhs))
    1.85 +  | decomp2 data (_$(Const("Not",_)$(Const(rel,T)$lhs$rhs))) =
    1.86 +      negate(decomp1 data (T,(rel,lhs,rhs)))
    1.87 +  | decomp2 data _ = None
    1.88  
    1.89 -val decomp = decomp2 o #discrete o ArithTheoryData.get_sg;
    1.90 +fun decomp sg =
    1.91 +  let val {discrete, inj_consts, ...} = ArithTheoryData.get_sg sg
    1.92 +  in decomp2 (discrete,inj_consts) end
    1.93  
    1.94  end;
    1.95  
    1.96 @@ -373,8 +384,9 @@
    1.97  
    1.98  val init_lin_arith_data =
    1.99   Fast_Arith.setup @
   1.100 - [Fast_Arith.map_data (fn {add_mono_thms, lessD, simpset = _} =>
   1.101 + [Fast_Arith.map_data (fn {add_mono_thms, inj_thms, lessD, simpset = _} =>
   1.102     {add_mono_thms = add_mono_thms @ add_mono_thms_nat,
   1.103 +    inj_thms = inj_thms,
   1.104      lessD = lessD @ [Suc_leI],
   1.105      simpset = HOL_basic_ss addsimps add_rules addsimprocs nat_cancel_sums_add}),
   1.106    ArithTheoryData.init, arith_discrete ("nat", true)];
   1.107 @@ -416,7 +428,7 @@
   1.108  
   1.109  in
   1.110  
   1.111 -val arith_tac = atomize_tac THEN' raw_arith_tac;
   1.112 +val arith_tac = fast_arith_tac ORELSE' (atomize_tac THEN' raw_arith_tac);
   1.113  
   1.114  fun arith_method prems =
   1.115    Method.METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ facts) THEN' arith_tac));