Fast_Lin_Arith.number_of: more conventional merge that prefers the left side -- note that former ordering wrt. serial numbers makes it depend on accidental load order;
authorwenzelm
Thu Aug 26 20:42:09 2010 +0200 (2010-08-26)
changeset 38763283f1f9969ba
parent 38762 996afaa9254a
child 38764 e6a18808873c
Fast_Lin_Arith.number_of: more conventional merge that prefers the left side -- note that former ordering wrt. serial numbers makes it depend on accidental load order;
src/HOL/Tools/int_arith.ML
src/HOL/Tools/lin_arith.ML
src/Provers/Arith/fast_lin_arith.ML
     1.1 --- a/src/HOL/Tools/int_arith.ML	Thu Aug 26 17:37:26 2010 +0200
     1.2 +++ b/src/HOL/Tools/int_arith.ML	Thu Aug 26 20:42:09 2010 +0200
     1.3 @@ -91,7 +91,7 @@
     1.4  fun number_of thy T n =
     1.5    if not (Sign.of_sort thy (T, @{sort number}))
     1.6    then raise CTERM ("number_of", [])
     1.7 -  else Numeral.mk_cnumber (Thm.ctyp_of thy T) n
     1.8 +  else Numeral.mk_cnumber (Thm.ctyp_of thy T) n;
     1.9  
    1.10  val setup =
    1.11    Lin_Arith.add_inj_thms [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2]
     2.1 --- a/src/HOL/Tools/lin_arith.ML	Thu Aug 26 17:37:26 2010 +0200
     2.2 +++ b/src/HOL/Tools/lin_arith.ML	Thu Aug 26 20:42:09 2010 +0200
     2.3 @@ -16,8 +16,7 @@
     2.4    val add_simprocs: simproc list -> Context.generic -> Context.generic
     2.5    val add_inj_const: string * typ -> Context.generic -> Context.generic
     2.6    val add_discrete_type: string -> Context.generic -> Context.generic
     2.7 -  val set_number_of: (theory -> typ -> int -> cterm) -> Context.generic ->
     2.8 -    Context.generic
     2.9 +  val set_number_of: (theory -> typ -> int -> cterm) -> Context.generic -> Context.generic
    2.10    val setup: Context.generic -> Context.generic
    2.11    val global_setup: theory -> theory
    2.12    val split_limit: int Config.T
     3.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Thu Aug 26 17:37:26 2010 +0200
     3.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Thu Aug 26 20:42:09 2010 +0200
     3.3 @@ -88,13 +88,14 @@
     3.4    val cut_lin_arith_tac: simpset -> int -> tactic
     3.5    val lin_arith_tac: Proof.context -> bool -> int -> tactic
     3.6    val lin_arith_simproc: simpset -> term -> thm option
     3.7 -  val map_data: ({add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
     3.8 -                 lessD: thm list, neqE: thm list, simpset: Simplifier.simpset,
     3.9 -                 number_of : serial * (theory -> typ -> int -> cterm)}
    3.10 -                 -> {add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
    3.11 -                     lessD: thm list, neqE: thm list, simpset: Simplifier.simpset,
    3.12 -                     number_of : serial * (theory -> typ -> int -> cterm)})
    3.13 -                -> Context.generic -> Context.generic
    3.14 +  val map_data:
    3.15 +    ({add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
    3.16 +      lessD: thm list, neqE: thm list, simpset: Simplifier.simpset,
    3.17 +      number_of: (theory -> typ -> int -> cterm) option} ->
    3.18 +     {add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
    3.19 +      lessD: thm list, neqE: thm list, simpset: Simplifier.simpset,
    3.20 +      number_of: (theory -> typ -> int -> cterm) option}) ->
    3.21 +      Context.generic -> Context.generic
    3.22    val add_inj_thms: thm list -> Context.generic -> Context.generic
    3.23    val add_lessD: thm -> Context.generic -> Context.generic
    3.24    val add_simps: thm list -> Context.generic -> Context.generic
    3.25 @@ -110,8 +111,6 @@
    3.26  
    3.27  (** theory data **)
    3.28  
    3.29 -fun no_number_of _ _ _ = raise CTERM ("number_of", [])
    3.30 -
    3.31  structure Data = Generic_Data
    3.32  (
    3.33    type T =
    3.34 @@ -121,27 +120,25 @@
    3.35      lessD: thm list,
    3.36      neqE: thm list,
    3.37      simpset: Simplifier.simpset,
    3.38 -    number_of : serial * (theory -> typ -> int -> cterm)};
    3.39 +    number_of: (theory -> typ -> int -> cterm) option};
    3.40  
    3.41 -  val empty = {add_mono_thms = [], mult_mono_thms = [], inj_thms = [],
    3.42 -               lessD = [], neqE = [], simpset = Simplifier.empty_ss,
    3.43 -               number_of = (serial (), no_number_of) } : T;
    3.44 +  val empty : T =
    3.45 +   {add_mono_thms = [], mult_mono_thms = [], inj_thms = [],
    3.46 +    lessD = [], neqE = [], simpset = Simplifier.empty_ss,
    3.47 +    number_of = NONE};
    3.48    val extend = I;
    3.49    fun merge
    3.50 -    ({add_mono_thms= add_mono_thms1, mult_mono_thms= mult_mono_thms1, inj_thms= inj_thms1,
    3.51 -      lessD = lessD1, neqE=neqE1, simpset = simpset1,
    3.52 -      number_of = (number_of1 as (s1, _))},
    3.53 -     {add_mono_thms= add_mono_thms2, mult_mono_thms= mult_mono_thms2, inj_thms= inj_thms2,
    3.54 -      lessD = lessD2, neqE=neqE2, simpset = simpset2,
    3.55 -      number_of = (number_of2 as (s2, _))}) =
    3.56 +    ({add_mono_thms = add_mono_thms1, mult_mono_thms = mult_mono_thms1, inj_thms = inj_thms1,
    3.57 +      lessD = lessD1, neqE = neqE1, simpset = simpset1, number_of = number_of1},
    3.58 +     {add_mono_thms = add_mono_thms2, mult_mono_thms = mult_mono_thms2, inj_thms = inj_thms2,
    3.59 +      lessD = lessD2, neqE = neqE2, simpset = simpset2, number_of = number_of2}) : T =
    3.60      {add_mono_thms = Thm.merge_thms (add_mono_thms1, add_mono_thms2),
    3.61       mult_mono_thms = Thm.merge_thms (mult_mono_thms1, mult_mono_thms2),
    3.62       inj_thms = Thm.merge_thms (inj_thms1, inj_thms2),
    3.63       lessD = Thm.merge_thms (lessD1, lessD2),
    3.64       neqE = Thm.merge_thms (neqE1, neqE2),
    3.65       simpset = Simplifier.merge_ss (simpset1, simpset2),
    3.66 -     (* FIXME depends on accidental load order !?! *)  (* FIXME *)
    3.67 -     number_of = if s1 > s2 then number_of1 else number_of2};
    3.68 +     number_of = if is_some number_of1 then number_of1 else number_of2};
    3.69  );
    3.70  
    3.71  val map_data = Data.map;
    3.72 @@ -159,16 +156,21 @@
    3.73    {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = inj_thms,
    3.74      lessD = lessD, neqE = neqE, simpset = f simpset, number_of = number_of};
    3.75  
    3.76 -fun map_number_of f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, number_of} =
    3.77 -  {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = inj_thms,
    3.78 -    lessD = lessD, neqE = neqE, simpset = simpset, number_of = f number_of};
    3.79 -
    3.80  fun add_inj_thms thms = map_data (map_inj_thms (append thms));
    3.81  fun add_lessD thm = map_data (map_lessD (fn thms => thms @ [thm]));
    3.82  fun add_simps thms = map_data (map_simpset (fn simpset => simpset addsimps thms));
    3.83  fun add_simprocs procs = map_data (map_simpset (fn simpset => simpset addsimprocs procs));
    3.84  
    3.85 -fun set_number_of f = map_data (map_number_of (K (serial (), f)));
    3.86 +fun set_number_of f =
    3.87 +  map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, ...} =>
    3.88 +   {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = inj_thms,
    3.89 +    lessD = lessD, neqE = neqE, simpset = simpset, number_of = SOME f});
    3.90 +
    3.91 +fun number_of ctxt =
    3.92 +  (case Data.get (Context.Proof ctxt) of
    3.93 +    {number_of = SOME f, ...} => f (ProofContext.theory_of ctxt)
    3.94 +  | _ => fn _ => fn _ => raise CTERM ("number_of", []));
    3.95 +
    3.96  
    3.97  
    3.98  (*** A fast decision procedure ***)
    3.99 @@ -473,8 +475,8 @@
   3.100    let
   3.101      val ctxt = Simplifier.the_context ss;
   3.102      val thy = ProofContext.theory_of ctxt;
   3.103 -    val {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset,
   3.104 -      number_of = (_, num_of), ...} = get_data ctxt;
   3.105 +    val {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset, ...} = get_data ctxt;
   3.106 +    val number_of = number_of ctxt;
   3.107      val simpset' = Simplifier.inherit_context ss simpset;
   3.108      fun only_concl f thm =
   3.109        if Thm.no_prems thm then f (Thm.concl_of thm) else NONE;
   3.110 @@ -520,7 +522,7 @@
   3.111              val T = #T (Thm.rep_cterm cv)
   3.112            in
   3.113              mth
   3.114 -            |> Thm.instantiate ([], [(cv, num_of thy T n)])
   3.115 +            |> Thm.instantiate ([], [(cv, number_of T n)])
   3.116              |> rewrite_concl
   3.117              |> discharge_prem
   3.118              handle CTERM _ => mult_by_add n thm