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