# HG changeset patch # User wenzelm # Date 1282848129 -7200 # Node ID 283f1f9969babecb3db4aac46485537048973a4d # Parent 996afaa9254a16490444de01800fc3e699d078b5 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; diff -r 996afaa9254a -r 283f1f9969ba src/HOL/Tools/int_arith.ML --- a/src/HOL/Tools/int_arith.ML Thu Aug 26 17:37:26 2010 +0200 +++ b/src/HOL/Tools/int_arith.ML Thu Aug 26 20:42:09 2010 +0200 @@ -91,7 +91,7 @@ fun number_of thy T n = if not (Sign.of_sort thy (T, @{sort number})) then raise CTERM ("number_of", []) - else Numeral.mk_cnumber (Thm.ctyp_of thy T) n + else Numeral.mk_cnumber (Thm.ctyp_of thy T) n; val setup = Lin_Arith.add_inj_thms [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2] diff -r 996afaa9254a -r 283f1f9969ba src/HOL/Tools/lin_arith.ML --- a/src/HOL/Tools/lin_arith.ML Thu Aug 26 17:37:26 2010 +0200 +++ b/src/HOL/Tools/lin_arith.ML Thu Aug 26 20:42:09 2010 +0200 @@ -16,8 +16,7 @@ val add_simprocs: simproc list -> Context.generic -> Context.generic val add_inj_const: string * typ -> Context.generic -> Context.generic val add_discrete_type: string -> Context.generic -> Context.generic - val set_number_of: (theory -> typ -> int -> cterm) -> Context.generic -> - Context.generic + val set_number_of: (theory -> typ -> int -> cterm) -> Context.generic -> Context.generic val setup: Context.generic -> Context.generic val global_setup: theory -> theory val split_limit: int Config.T diff -r 996afaa9254a -r 283f1f9969ba src/Provers/Arith/fast_lin_arith.ML --- a/src/Provers/Arith/fast_lin_arith.ML Thu Aug 26 17:37:26 2010 +0200 +++ b/src/Provers/Arith/fast_lin_arith.ML Thu Aug 26 20:42:09 2010 +0200 @@ -88,13 +88,14 @@ val cut_lin_arith_tac: simpset -> int -> tactic val lin_arith_tac: Proof.context -> bool -> int -> tactic val lin_arith_simproc: simpset -> term -> thm option - val map_data: ({add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list, - lessD: thm list, neqE: thm list, simpset: Simplifier.simpset, - number_of : serial * (theory -> typ -> int -> cterm)} - -> {add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list, - lessD: thm list, neqE: thm list, simpset: Simplifier.simpset, - number_of : serial * (theory -> typ -> int -> cterm)}) - -> Context.generic -> Context.generic + val map_data: + ({add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list, + lessD: thm list, neqE: thm list, simpset: Simplifier.simpset, + number_of: (theory -> typ -> int -> cterm) option} -> + {add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list, + lessD: thm list, neqE: thm list, simpset: Simplifier.simpset, + number_of: (theory -> typ -> int -> cterm) option}) -> + Context.generic -> Context.generic val add_inj_thms: thm list -> Context.generic -> Context.generic val add_lessD: thm -> Context.generic -> Context.generic val add_simps: thm list -> Context.generic -> Context.generic @@ -110,8 +111,6 @@ (** theory data **) -fun no_number_of _ _ _ = raise CTERM ("number_of", []) - structure Data = Generic_Data ( type T = @@ -121,27 +120,25 @@ lessD: thm list, neqE: thm list, simpset: Simplifier.simpset, - number_of : serial * (theory -> typ -> int -> cterm)}; + number_of: (theory -> typ -> int -> cterm) option}; - val empty = {add_mono_thms = [], mult_mono_thms = [], inj_thms = [], - lessD = [], neqE = [], simpset = Simplifier.empty_ss, - number_of = (serial (), no_number_of) } : T; + val empty : T = + {add_mono_thms = [], mult_mono_thms = [], inj_thms = [], + lessD = [], neqE = [], simpset = Simplifier.empty_ss, + number_of = NONE}; val extend = I; fun merge - ({add_mono_thms= add_mono_thms1, mult_mono_thms= mult_mono_thms1, inj_thms= inj_thms1, - lessD = lessD1, neqE=neqE1, simpset = simpset1, - number_of = (number_of1 as (s1, _))}, - {add_mono_thms= add_mono_thms2, mult_mono_thms= mult_mono_thms2, inj_thms= inj_thms2, - lessD = lessD2, neqE=neqE2, simpset = simpset2, - number_of = (number_of2 as (s2, _))}) = + ({add_mono_thms = add_mono_thms1, mult_mono_thms = mult_mono_thms1, inj_thms = inj_thms1, + lessD = lessD1, neqE = neqE1, simpset = simpset1, number_of = number_of1}, + {add_mono_thms = add_mono_thms2, mult_mono_thms = mult_mono_thms2, inj_thms = inj_thms2, + lessD = lessD2, neqE = neqE2, simpset = simpset2, number_of = number_of2}) : T = {add_mono_thms = Thm.merge_thms (add_mono_thms1, add_mono_thms2), mult_mono_thms = Thm.merge_thms (mult_mono_thms1, mult_mono_thms2), inj_thms = Thm.merge_thms (inj_thms1, inj_thms2), lessD = Thm.merge_thms (lessD1, lessD2), neqE = Thm.merge_thms (neqE1, neqE2), simpset = Simplifier.merge_ss (simpset1, simpset2), - (* FIXME depends on accidental load order !?! *) (* FIXME *) - number_of = if s1 > s2 then number_of1 else number_of2}; + number_of = if is_some number_of1 then number_of1 else number_of2}; ); val map_data = Data.map; @@ -159,16 +156,21 @@ {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = inj_thms, lessD = lessD, neqE = neqE, simpset = f simpset, number_of = number_of}; -fun map_number_of f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, number_of} = - {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = inj_thms, - lessD = lessD, neqE = neqE, simpset = simpset, number_of = f number_of}; - fun add_inj_thms thms = map_data (map_inj_thms (append thms)); fun add_lessD thm = map_data (map_lessD (fn thms => thms @ [thm])); fun add_simps thms = map_data (map_simpset (fn simpset => simpset addsimps thms)); fun add_simprocs procs = map_data (map_simpset (fn simpset => simpset addsimprocs procs)); -fun set_number_of f = map_data (map_number_of (K (serial (), f))); +fun set_number_of f = + map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, ...} => + {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = inj_thms, + lessD = lessD, neqE = neqE, simpset = simpset, number_of = SOME f}); + +fun number_of ctxt = + (case Data.get (Context.Proof ctxt) of + {number_of = SOME f, ...} => f (ProofContext.theory_of ctxt) + | _ => fn _ => fn _ => raise CTERM ("number_of", [])); + (*** A fast decision procedure ***) @@ -473,8 +475,8 @@ let val ctxt = Simplifier.the_context ss; val thy = ProofContext.theory_of ctxt; - val {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset, - number_of = (_, num_of), ...} = get_data ctxt; + val {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset, ...} = get_data ctxt; + val number_of = number_of ctxt; val simpset' = Simplifier.inherit_context ss simpset; fun only_concl f thm = if Thm.no_prems thm then f (Thm.concl_of thm) else NONE; @@ -520,7 +522,7 @@ val T = #T (Thm.rep_cterm cv) in mth - |> Thm.instantiate ([], [(cv, num_of thy T n)]) + |> Thm.instantiate ([], [(cv, number_of T n)]) |> rewrite_concl |> discharge_prem handle CTERM _ => mult_by_add n thm