# HG changeset patch # User wenzelm # Date 1185836189 -7200 # Node ID ae946f751c4493f8cda16a8e27a9507e79d574c4 # Parent 366d4d234814d071dc1c18324597f9ed498d1c8e arith method setup: proper context; turned fast_arith_split/neq_limit into configuration options; tuned signatures; misc cleanup; diff -r 366d4d234814 -r ae946f751c44 src/HOL/arith_data.ML --- a/src/HOL/arith_data.ML Tue Jul 31 00:56:26 2007 +0200 +++ b/src/HOL/arith_data.ML Tue Jul 31 00:56:29 2007 +0200 @@ -176,7 +176,7 @@ val mk_Trueprop = HOLogic.mk_Trueprop; -fun atomize thm = case #prop(rep_thm thm) of +fun atomize thm = case Thm.prop_of thm of Const("Trueprop",_) $ (Const("op &",_) $ _ $ _) => atomize(thm RS conjunct1) @ atomize(thm RS conjunct2) | _ => [thm]; @@ -186,7 +186,7 @@ | neg_prop t = raise TERM ("neg_prop", [t]); fun is_False thm = - let val _ $ t = #prop(rep_thm thm) + let val _ $ t = Thm.prop_of thm in t = Const("False",HOLogic.boolT) end; fun is_nat(t) = fastype_of1 t = HOLogic.natT; @@ -206,14 +206,13 @@ fun eq_arith_tactic (ArithTactic {id = id1, ...}, ArithTactic {id = id2, ...}) = (id1 = id2); -structure ArithTheoryData = TheoryDataFun +structure ArithContextData = GenericDataFun ( type T = {splits: thm list, inj_consts: (string * typ) list, discrete: string list, tactics: arithtactic list}; val empty = {splits = [], inj_consts = [], discrete = [], tactics = []}; - val copy = I; val extend = I; fun merge _ ({splits= splits1, inj_consts= inj_consts1, discrete= discrete1, tactics= tactics1}, {splits= splits2, inj_consts= inj_consts2, discrete= discrete2, tactics= tactics2}) = @@ -223,29 +222,41 @@ tactics = Library.merge eq_arith_tactic (tactics1, tactics2)}; ); +val get_arith_data = ArithContextData.get o Context.Proof; + val arith_split_add = Thm.declaration_attribute (fn thm => - Context.mapping (ArithTheoryData.map (fn {splits,inj_consts,discrete,tactics} => - {splits= insert Thm.eq_thm_prop thm splits, inj_consts= inj_consts, discrete= discrete, tactics= tactics})) I); + ArithContextData.map (fn {splits, inj_consts, discrete, tactics} => + {splits = insert Thm.eq_thm_prop thm splits, + inj_consts = inj_consts, discrete = discrete, tactics = tactics})); -fun arith_discrete d = ArithTheoryData.map (fn {splits,inj_consts,discrete,tactics} => - {splits = splits, inj_consts = inj_consts, discrete = insert (op =) d discrete, tactics= tactics}); +fun arith_discrete d = ArithContextData.map (fn {splits, inj_consts, discrete, tactics} => + {splits = splits, inj_consts = inj_consts, + discrete = insert (op =) d discrete, tactics = tactics}); -fun arith_inj_const c = ArithTheoryData.map (fn {splits,inj_consts,discrete,tactics} => - {splits = splits, inj_consts = insert (op =) c inj_consts, discrete = discrete, tactics= tactics}); +fun arith_inj_const c = ArithContextData.map (fn {splits, inj_consts, discrete, tactics} => + {splits = splits, inj_consts = insert (op =) c inj_consts, + discrete = discrete, tactics= tactics}); -fun arith_tactic_add tac = ArithTheoryData.map (fn {splits,inj_consts,discrete,tactics} => - {splits= splits, inj_consts= inj_consts, discrete= discrete, tactics= insert eq_arith_tactic tac tactics}); +fun arith_tactic_add tac = ArithContextData.map (fn {splits, inj_consts, discrete, tactics} => + {splits = splits, inj_consts = inj_consts, discrete = discrete, + tactics = insert eq_arith_tactic tac tactics}); signature HOL_LIN_ARITH_DATA = sig include LIN_ARITH_DATA - val fast_arith_split_limit : int ref + val fast_arith_split_limit: int ConfigOption.T + val setup_options: theory -> theory end; structure LA_Data_Ref: HOL_LIN_ARITH_DATA = struct +val (fast_arith_split_limit, setup1) = ConfigOption.int "fast_arith_split_limit" 9; +val (fast_arith_neq_limit, setup2) = ConfigOption.int "fast_arith_neq_limit" 9; +val setup_options = setup1 #> setup2; + + (* internal representation of linear (in-)equations *) type decompT = ((term * Rat.rat) list * Rat.rat * string * (term * Rat.rat) list * Rat.rat * bool); @@ -387,10 +398,10 @@ | allows_lin_arith sg discrete U = (of_lin_arith_sort sg U, false); -fun decomp_typecheck (sg, discrete, inj_consts) (T : typ, xxx) : decompT option = +fun decomp_typecheck (thy, discrete, inj_consts) (T : typ, xxx) : decompT option = case T of Type ("fun", [U, _]) => - (case allows_lin_arith sg discrete U of + (case allows_lin_arith thy discrete U of (true, d) => (case decomp0 inj_consts xxx of NONE => NONE @@ -411,12 +422,11 @@ | decomp_negation data _ = NONE; -fun decomp sg : term -> decompT option = -let - val {discrete, inj_consts, ...} = ArithTheoryData.get sg -in - decomp_negation (sg, discrete, inj_consts) -end; +fun decomp ctxt : term -> decompT option = + let + val thy = ProofContext.theory_of ctxt + val {discrete, inj_consts, ...} = get_arith_data ctxt + in decomp_negation (thy, discrete, inj_consts) end; fun domain_is_nat (_ $ (Const (_, T) $ _ $ _)) = nT T | domain_is_nat (_ $ (Const ("Not", _) $ (Const (_, T) $ _ $ _))) = nT T @@ -425,23 +435,11 @@ fun number_of (n, T) = HOLogic.mk_number T n; (*---------------------------------------------------------------------------*) -(* code that performs certain goal transformations for linear arithmetic *) -(*---------------------------------------------------------------------------*) - -(* A "do nothing" variant of pre_decomp and pre_tac: - -fun pre_decomp sg Ts termitems = [termitems]; -fun pre_tac i = all_tac; -*) - -(*---------------------------------------------------------------------------*) (* the following code performs splitting of certain constants (e.g. min, *) (* max) in a linear arithmetic problem; similar to what split_tac later does *) (* to the proof state *) (*---------------------------------------------------------------------------*) -val fast_arith_split_limit = ref 9; - (* checks if splitting with 'thm' is implemented *) fun is_split_thm (thm : thm) : bool = @@ -493,24 +491,24 @@ (* former can have a faster implementation as it does not need to be *) (* proof-producing). *) -fun split_once_items (sg : theory) (Ts : typ list, terms : term list) : +fun split_once_items ctxt (Ts : typ list, terms : term list) : (typ list * term list) list option = let + val thy = ProofContext.theory_of ctxt (* takes a list [t1, ..., tn] to the term *) (* tn' --> ... --> t1' --> False , *) (* where ti' = HOLogic.dest_Trueprop ti *) - (* term list -> term *) fun REPEAT_DETERM_etac_rev_mp terms' = fold (curry HOLogic.mk_imp) (map HOLogic.dest_Trueprop terms') HOLogic.false_const - val split_thms = filter is_split_thm (#splits (ArithTheoryData.get sg)) + val split_thms = filter is_split_thm (#splits (get_arith_data ctxt)) val cmap = Splitter.cmap_of_split_thms split_thms - val splits = Splitter.split_posns cmap sg Ts (REPEAT_DETERM_etac_rev_mp terms) + val splits = Splitter.split_posns cmap thy Ts (REPEAT_DETERM_etac_rev_mp terms) + val split_limit = ConfigOption.get ctxt fast_arith_split_limit in - if length splits > !fast_arith_split_limit then ( - tracing ("fast_arith_split_limit exceeded (current value is " ^ - string_of_int (!fast_arith_split_limit) ^ ")"); - NONE - ) else ( + if length splits > split_limit then + (tracing ("fast_arith_split_limit exceeded (current value is " ^ + string_of_int split_limit ^ ")"); NONE) + else ( case splits of [] => (* split_tac would fail: no possible split *) NONE @@ -784,8 +782,8 @@ (* implemented above, or 'is_split_thm' should be modified to filter it *) (* out *) | (t, ts) => ( - warning ("Lin. Arith.: split rule for " ^ Sign.string_of_term sg t ^ - " (with " ^ Int.toString (length ts) ^ + warning ("Lin. Arith.: split rule for " ^ ProofContext.string_of_term ctxt t ^ + " (with " ^ string_of_int (length ts) ^ " argument(s)) not implemented; proof reconstruction is likely to fail"); NONE )) @@ -813,17 +811,17 @@ | _ => false) terms; -fun pre_decomp sg (Ts : typ list, terms : term list) : (typ list * term list) list = +fun pre_decomp ctxt (Ts : typ list, terms : term list) : (typ list * term list) list = let (* repeatedly split (including newly emerging subgoals) until no further *) (* splitting is possible *) fun split_loop ([] : (typ list * term list) list) = ([] : (typ list * term list) list) | split_loop (subgoal::subgoals) = ( - case split_once_items sg subgoal of + case split_once_items ctxt subgoal of SOME new_subgoals => split_loop (new_subgoals @ subgoals) | NONE => subgoal :: split_loop subgoals ) - fun is_relevant t = isSome (decomp sg t) + fun is_relevant t = isSome (decomp ctxt t) (* filter_prems_tac is_relevant: *) val relevant_terms = filter_prems_tac_items is_relevant terms (* split_tac, NNF normalization: *) @@ -855,30 +853,29 @@ full_simp_tac (Simplifier.theory_context (Thm.theory_of_thm st) nnf_simpset) i st in -fun split_once_tac (split_thms : thm list) (i : int) : tactic = -let - fun cond_split_tac i st = - let - val subgoal = Logic.nth_prem (i, Thm.prop_of st) - val Ts = rev (map snd (Logic.strip_params subgoal)) - val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl subgoal) - val cmap = Splitter.cmap_of_split_thms split_thms - val splits = Splitter.split_posns cmap (theory_of_thm st) Ts concl - in - if length splits > !fast_arith_split_limit then - no_tac st - else - split_tac split_thms i st - end -in - EVERY' [ - REPEAT_DETERM o etac rev_mp, - cond_split_tac, - rtac ccontr, - prem_nnf_tac, - TRY o REPEAT_ALL_NEW (DETERM o (eresolve_tac [conjE, exE] ORELSE' etac disjE)) - ] i -end +fun split_once_tac ctxt split_thms = + let + val thy = ProofContext.theory_of ctxt + val cond_split_tac = SUBGOAL (fn (subgoal, i) => + let + val Ts = rev (map snd (Logic.strip_params subgoal)) + val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl subgoal) + val cmap = Splitter.cmap_of_split_thms split_thms + val splits = Splitter.split_posns cmap thy Ts concl + val split_limit = ConfigOption.get ctxt fast_arith_split_limit + in + if length splits > split_limit then no_tac + else split_tac split_thms i + end) + in + EVERY' [ + REPEAT_DETERM o etac rev_mp, + cond_split_tac, + rtac ccontr, + prem_nnf_tac, + TRY o REPEAT_ALL_NEW (DETERM o (eresolve_tac [conjE, exE] ORELSE' etac disjE)) + ] + end; end; (* local *) @@ -887,22 +884,21 @@ (* subgoals and finally attempt to solve them by finding an immediate *) (* contradiction (i.e. a term and its negation) in their premises. *) -fun pre_tac i st = +fun pre_tac ctxt i = let - val sg = theory_of_thm st - val split_thms = filter is_split_thm (#splits (ArithTheoryData.get sg)) - fun is_relevant t = isSome (decomp sg t) + val split_thms = filter is_split_thm (#splits (get_arith_data ctxt)) + fun is_relevant t = isSome (decomp ctxt t) in DETERM ( TRY (filter_prems_tac is_relevant i) THEN ( - (TRY o REPEAT_ALL_NEW (split_once_tac split_thms)) + (TRY o REPEAT_ALL_NEW (split_once_tac ctxt split_thms)) THEN_ALL_NEW (CONVERSION Drule.beta_eta_conversion THEN' (TRY o (etac notE THEN' eq_assume_tac))) ) i - ) st + ) end; end; (* LA_Data_Ref *) @@ -911,16 +907,14 @@ 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 false; +fun fast_arith_tac ctxt = Fast_Arith.lin_arith_tac ctxt false; val fast_ex_arith_tac = Fast_Arith.lin_arith_tac; val trace_arith = Fast_Arith.trace; -val fast_arith_neq_limit = Fast_Arith.fast_arith_neq_limit; -val fast_arith_split_limit = LA_Data_Ref.fast_arith_split_limit; (* reduce contradictory <= to False. Most of the work is done by the cancel tactics. *) -val init_lin_arith_data = +val init_arith_data = Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, ...} => {add_mono_thms = add_mono_thms @ @{thms add_mono_thms_ordered_semiring} @ @{thms add_mono_thms_ordered_field}, @@ -929,7 +923,9 @@ lessD = lessD @ [thm "Suc_leI"], neqE = [@{thm linorder_neqE_nat}, @{thm linorder_neqE_ordered_idom}], simpset = HOL_basic_ss - addsimps [@{thm "monoid_add_class.zero_plus.add_0_left"}, @{thm "monoid_add_class.zero_plus.add_0_right"}, + addsimps + [@{thm "monoid_add_class.zero_plus.add_0_left"}, + @{thm "monoid_add_class.zero_plus.add_0_right"}, @{thm "Zero_not_Suc"}, @{thm "Suc_not_Zero"}, @{thm "le_0_eq"}, @{thm "One_nat_def"}, @{thm "order_less_irrefl"}, @{thm "zero_neq_one"}, @{thm "zero_less_one"}, @{thm "zero_le_one"}, @{thm "zero_neq_one"} RS not_sym, @{thm "not_one_le_zero"}, @@ -941,7 +937,7 @@ val fast_nat_arith_simproc = Simplifier.simproc (the_context ()) "fast_nat_arith" - ["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"] Fast_Arith.lin_arith_prover; + ["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"] (K Fast_Arith.lin_arith_simproc); (* Because of fast_nat_arith_simproc, the arithmetic solver is really only useful to detect inconsistencies among the premises for subgoals which are @@ -954,7 +950,7 @@ local -fun raw_arith_tac ex i st = +fun raw_arith_tac ctxt ex = (* FIXME: K true should be replaced by a sensible test (perhaps "isSome o decomp sg"? -- but note that the test is applied to terms already before they are split/normalized) to speed things up in case there are lots of @@ -969,32 +965,30 @@ (* fast_arith_split_limit may trigger. *) (* Therefore splitting outside of fast_arith_tac may allow us to prove *) (* some goals that fast_arith_tac alone would fail on. *) - (REPEAT_DETERM o split_tac (#splits (ArithTheoryData.get (Thm.theory_of_thm st)))) - (fast_ex_arith_tac ex) - i st; + (REPEAT_DETERM o split_tac (#splits (get_arith_data ctxt))) + (fast_ex_arith_tac ctxt ex); -fun arith_theory_tac i st = -let - val tactics = #tactics (ArithTheoryData.get (Thm.theory_of_thm st)) -in - FIRST' (map (fn ArithTactic {tactic, ...} => tactic) tactics) i st -end; +fun more_arith_tacs ctxt = + let val tactics = #tactics (get_arith_data ctxt) + in FIRST' (map (fn ArithTactic {tactic, ...} => tactic) tactics) end; in - val simple_arith_tac = FIRST' [fast_arith_tac, - ObjectLogic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_arith_tac true]; +fun simple_arith_tac ctxt = FIRST' [fast_arith_tac ctxt, + ObjectLogic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_arith_tac ctxt true]; - val arith_tac = FIRST' [fast_arith_tac, - ObjectLogic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_arith_tac true, - arith_theory_tac]; +fun arith_tac ctxt = FIRST' [fast_arith_tac ctxt, + ObjectLogic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_arith_tac ctxt true, + more_arith_tacs ctxt]; - val silent_arith_tac = FIRST' [fast_arith_tac, - ObjectLogic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_arith_tac false, - arith_theory_tac]; +fun silent_arith_tac ctxt = FIRST' [fast_arith_tac ctxt, + ObjectLogic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_arith_tac ctxt false, + more_arith_tacs ctxt]; - fun arith_method prems = - Method.METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ facts) THEN' arith_tac)); +fun arith_method src = + Method.syntax Args.bang_facts src + #> (fn (prems, ctxt) => Method.METHOD (fn facts => + HEADGOAL (Method.insert_tac (prems @ facts) THEN' arith_tac ctxt))); end; @@ -1045,12 +1039,14 @@ (* theory setup *) val arith_setup = - init_lin_arith_data #> - (fn thy => (Simplifier.change_simpset_of thy (fn ss => ss + init_arith_data #> + Simplifier.map_ss (fn ss => ss addsimprocs (nat_cancel_sums @ [fast_nat_arith_simproc]) - addSolver (mk_solver' "lin. arith." Fast_Arith.cut_lin_arith_tac)); thy)) #> - Method.add_methods - [("arith", (arith_method o fst) oo Method.syntax Args.bang_facts, - "decide linear arithmethic")] #> - Attrib.add_attributes [("arith_split", Attrib.no_args arith_split_add, - "declaration of split rules for arithmetic procedure")]; + addSolver (mk_solver' "lin. arith." Fast_Arith.cut_lin_arith_tac)) #> + Context.mapping + (LA_Data_Ref.setup_options #> + Method.add_methods + [("arith", arith_method, + "decide linear arithmethic")] #> + Attrib.add_attributes [("arith_split", Attrib.no_args arith_split_add, + "declaration of split rules for arithmetic procedure")]) I; diff -r 366d4d234814 -r ae946f751c44 src/Provers/Arith/fast_lin_arith.ML --- a/src/Provers/Arith/fast_lin_arith.ML Tue Jul 31 00:56:26 2007 +0200 +++ b/src/Provers/Arith/fast_lin_arith.ML Tue Jul 31 00:56:29 2007 +0200 @@ -1,20 +1,14 @@ (* Title: Provers/Arith/fast_lin_arith.ML ID: $Id$ - Author: Tobias Nipkow - Copyright 1998 TU Munich - -A generic linear arithmetic package. -It provides two tactics + Author: Tobias Nipkow and Tjark Weber - lin_arith_tac: int -> tactic -cut_lin_arith_tac: thms -> int -> tactic - -and a simplification procedure +A generic linear arithmetic package. It provides two tactics +(cut_lin_arith_tac, lin_arith_tac) and a simplification procedure +(lin_arith_simproc). - lin_arith_prover: theory -> simpset -> term -> thm option - -Only take premises and conclusions into account that are already (negated) -(in)equations. lin_arith_prover tries to prove or disprove the term. +Only take premises and conclusions into account that are already +(negated) (in)equations. lin_arith_simproc tries to prove or disprove +the term. *) (* Debugging: set Fast_Arith.trace *) @@ -54,15 +48,21 @@ signature LIN_ARITH_DATA = sig - (* internal representation of linear (in-)equations: *) + (*internal representation of linear (in-)equations:*) type decompT = (term * Rat.rat) list * Rat.rat * string * (term * Rat.rat) list * Rat.rat * bool - val decomp: theory -> term -> decompT option - val domain_is_nat : term -> bool - (* preprocessing, performed on a representation of subgoals as list of premises: *) - val pre_decomp: theory -> typ list * term list -> (typ list * term list) list - (* preprocessing, performed on the goal -- must do the same as 'pre_decomp': *) - val pre_tac : int -> Tactical.tactic - val number_of : IntInf.int * typ -> term + val decomp: Proof.context -> term -> decompT option + val domain_is_nat: term -> bool + + (*preprocessing, performed on a representation of subgoals as list of premises:*) + val pre_decomp: Proof.context -> typ list * term list -> (typ list * term list) list + + (*preprocessing, performed on the goal -- must do the same as 'pre_decomp':*) + val pre_tac: Proof.context -> int -> tactic + val number_of: IntInf.int * typ -> term + + (*the limit on the number of ~= allowed; because each ~= is split + into two cases, this can lead to an explosion*) + val fast_arith_neq_limit: int ConfigOption.T end; (* decomp(`x Rel y') should yield (p,i,Rel,q,j,d) @@ -92,31 +92,33 @@ lessD: thm list, neqE: thm list, simpset: Simplifier.simpset} -> {add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list, lessD: thm list, neqE: thm list, simpset: Simplifier.simpset}) - -> theory -> theory + -> Context.generic -> Context.generic val trace: bool ref - val fast_arith_neq_limit: int ref - val lin_arith_prover: theory -> simpset -> term -> thm option - val lin_arith_tac: bool -> int -> tactic 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 end; -functor Fast_Lin_Arith(structure LA_Logic:LIN_ARITH_LOGIC - and LA_Data:LIN_ARITH_DATA) : FAST_LIN_ARITH = +functor Fast_Lin_Arith + (structure LA_Logic: LIN_ARITH_LOGIC and LA_Data: LIN_ARITH_DATA): FAST_LIN_ARITH = struct (** theory data **) -structure Data = TheoryDataFun +structure Data = GenericDataFun ( - type T = {add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list, - lessD: thm list, neqE: thm list, simpset: Simplifier.simpset}; + type T = + {add_mono_thms: thm list, + mult_mono_thms: thm list, + inj_thms: thm list, + lessD: thm list, + neqE: thm list, + simpset: Simplifier.simpset}; val empty = {add_mono_thms = [], mult_mono_thms = [], inj_thms = [], lessD = [], neqE = [], simpset = Simplifier.empty_ss}; - val copy = I; 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}, @@ -131,6 +133,7 @@ ); val map_data = Data.map; +val get_data = Data.get o Context.Proof; @@ -409,11 +412,14 @@ (* Translate back a proof. *) (* ------------------------------------------------------------------------- *) -fun trace_thm (msg : string) (th : thm) : thm = - (if !trace then (tracing msg; tracing (Display.string_of_thm th)) else (); th); +fun trace_thm msg th = + (if !trace then (tracing msg; tracing (Display.string_of_thm th)) else (); th); -fun trace_msg (msg : string) : unit = - if !trace then tracing msg else (); +fun trace_term ctxt msg t = + (if !trace then tracing (cat_lines [msg, ProofContext.string_of_term ctxt t]) else (); t) + +fun trace_msg msg = + if !trace then tracing msg else (); (* FIXME OPTIMIZE!!!! (partly done already) Addition/Multiplication need i*t representation rather than t+t+... @@ -425,16 +431,18 @@ with 0 <= n. *) local - exception FalseE of thm + exception FalseE of thm in -fun mkthm (sg:theory, ss) (asms:thm list) (just:injust) : thm = - let val {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset, ...} = - Data.get sg; - val simpset' = Simplifier.inherit_context ss simpset; - val atoms = Library.foldl (fn (ats, (lhs,_,_,rhs,_,_)) => +fun mkthm ss asms (just: injust) = + let + val ctxt = Simplifier.the_context ss; + val thy = ProofContext.theory_of ctxt; + val {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset, ...} = get_data ctxt; + val simpset' = Simplifier.inherit_context ss simpset; + val atoms = Library.foldl (fn (ats, (lhs,_,_,rhs,_,_)) => map fst lhs union (map fst rhs union ats)) ([], List.mapPartial (fn thm => if Thm.no_prems thm - then LA_Data.decomp sg (concl_of thm) + then LA_Data.decomp ctxt (Thm.concl_of thm) else NONE) asms) fun add2 thm1 thm2 = @@ -465,15 +473,15 @@ get_first (fn th => SOME(thm RS th) handle THM _ => NONE) mult_mono_thms fun cvar(th,_ $ (_ $ _ $ var)) = cterm_of (Thm.theory_of_thm th) var; val cv = cvar(mth, hd(prems_of mth)); - val ct = cterm_of sg (LA_Data.number_of(n,#T(rep_cterm cv))) + val ct = cterm_of thy (LA_Data.number_of(n,#T(rep_cterm cv))) in instantiate ([],[(cv,ct)]) mth end fun simp thm = let val thm' = trace_thm "Simplified:" (full_simplify simpset' thm) in if LA_Logic.is_False thm' then raise FalseE thm' else thm' end - fun mk (Asm i) = trace_thm ("Asm " ^ Int.toString i) (nth asms i) - | mk (Nat i) = trace_thm ("Nat " ^ Int.toString i) (LA_Logic.mk_nat_thm sg (nth atoms i)) + fun mk (Asm i) = trace_thm ("Asm " ^ string_of_int i) (nth asms i) + | mk (Nat i) = trace_thm ("Nat " ^ string_of_int i) (LA_Logic.mk_nat_thm thy (nth atoms i)) | mk (LessD j) = trace_thm "L" (hd ([mk j] RL lessD)) | mk (NotLeD j) = trace_thm "NLe" (mk j RS LA_Logic.not_leD) | mk (NotLeDD j) = trace_thm "NLeD" (hd ([mk j RS LA_Logic.not_leD] RL lessD)) @@ -550,22 +558,24 @@ #> commas #> curry (op ^) "Counterexample (possibly spurious):\n"; -fun trace_ex (sg, params, atoms, discr, n, hist : history) = +fun trace_ex ctxt params atoms discr n (hist: history) = case hist of [] => () | (v, lineqs) :: hist' => - let val frees = map Free params - fun s_of_t t = Sign.string_of_term sg (subst_bounds (frees, t)) - val start = if v = ~1 then (hist', findex0 discr n lineqs) + let + val frees = map Free params + fun show_term t = ProofContext.string_of_term ctxt (subst_bounds (frees, t)) + val start = + if v = ~1 then (hist', findex0 discr n lineqs) else (hist, replicate n Rat.zero) - val ex = SOME (produce_ex ((map s_of_t atoms) ~~ discr) - (uncurry (fold (findex1 discr)) start)) + val ex = SOME (produce_ex (map show_term atoms ~~ discr) + (uncurry (fold (findex1 discr)) start)) handle NoEx => NONE - in - case ex of - SOME s => (warning "arith failed - see trace for a counterexample"; tracing s) - | NONE => warning "arith failed" - end; + in + case ex of + SOME s => (warning "arith failed - see trace for a counterexample"; tracing s) + | NONE => warning "arith failed" + end; (* ------------------------------------------------------------------------- *) @@ -594,8 +604,7 @@ (* failure as soon as a case could not be refuted; i.e. delay further *) (* splitting until after a refutation for other cases has been found. *) -fun split_items sg (do_pre : bool) (Ts, terms) : - (typ list * (LA_Data.decompT * int) list) list = +fun split_items ctxt do_pre (Ts, terms) : (typ list * (LA_Data.decompT * int) list) list = let (* splits inequalities '~=' into '<' and '>'; this corresponds to *) (* 'REPEAT_DETERM (eresolve_tac neqE i)' at the theorem/tactic *) @@ -632,11 +641,11 @@ val result = (Ts, terms) |> (* user-defined preprocessing of the subgoal *) - (if do_pre then LA_Data.pre_decomp sg else Library.single) + (if do_pre then LA_Data.pre_decomp ctxt else Library.single) |> tap (fn subgoals => trace_msg ("Preprocessing yields " ^ string_of_int (length subgoals) ^ " subgoal(s) total.")) |> (* produce the internal encoding of (in-)equalities *) - map (apsnd (map (fn t => (LA_Data.decomp sg t, LA_Data.domain_is_nat t)))) + map (apsnd (map (fn t => (LA_Data.decomp ctxt t, LA_Data.domain_is_nat t)))) |> (* splitting of inequalities *) map (apsnd elim_neq) |> maps (fn (Ts, subgoals) => map (pair Ts o map fst) subgoals) @@ -658,21 +667,22 @@ fun discr (initems : (LA_Data.decompT * int) list) : bool list = map fst (Library.foldl add_datoms ([],initems)); -fun refutes (sg : theory) (params : (string * typ) list) (show_ex : bool) : +fun refutes ctxt params show_ex : (typ list * (LA_Data.decompT * int) list) list -> injust list -> injust list option = let fun refute ((Ts : typ list, initems : (LA_Data.decompT * int) list)::initemss) (js : injust list) : injust list option = - let val atoms = Library.foldl add_atoms ([], initems) - val n = length atoms - val mkleq = mklineq n atoms - val ixs = 0 upto (n-1) - val iatoms = atoms ~~ ixs - val natlineqs = List.mapPartial (mknat Ts ixs) iatoms - val ineqs = map mkleq initems @ natlineqs + let + val atoms = Library.foldl add_atoms ([], initems) + val n = length atoms + val mkleq = mklineq n atoms + val ixs = 0 upto (n - 1) + val iatoms = atoms ~~ ixs + val natlineqs = List.mapPartial (mknat Ts ixs) iatoms + val ineqs = map mkleq initems @ natlineqs in case elim (ineqs, []) of Success j => - (trace_msg ("Contradiction! (" ^ Int.toString (length js + 1) ^ ")"); + (trace_msg ("Contradiction! (" ^ string_of_int (length js + 1) ^ ")"); refute initemss (js@[j])) | Failure hist => (if not show_ex then @@ -685,25 +695,18 @@ val new_names = map Name.bound (0 upto new_count) val params' = (new_names @ map fst params) ~~ Ts in - trace_ex (sg, params', atoms, discr initems, n, hist) + trace_ex ctxt params' atoms (discr initems) n hist end; NONE) end | refute [] js = SOME js in refute end; -fun refute (sg : theory) (params : (string * Term.typ) list) (show_ex : bool) - (do_pre : bool) (terms : term list) : injust list option = - refutes sg params show_ex (split_items sg do_pre (map snd params, terms)) []; +fun refute ctxt params show_ex do_pre terms : injust list option = + refutes ctxt params show_ex (split_items ctxt do_pre (map snd params, terms)) []; fun count P xs = length (filter P xs); -(* The limit on the number of ~= allowed. - Because each ~= is split into two cases, this can lead to an explosion. -*) -val fast_arith_neq_limit = ref 9; - -fun prove (sg : theory) (params : (string * Term.typ) list) (show_ex : bool) - (do_pre : bool) (Hs : term list) (concl : term) : injust list option = +fun prove ctxt (params : (string * Term.typ) list) show_ex do_pre Hs concl : injust list option = let val _ = trace_msg "prove:" (* append the negated conclusion to 'Hs' -- this corresponds to *) @@ -712,14 +715,13 @@ val Hs' = Hs @ [LA_Logic.neg_prop concl] fun is_neq NONE = false | is_neq (SOME (_,_,r,_,_,_)) = (r = "~=") + val neq_limit = ConfigOption.get ctxt LA_Data.fast_arith_neq_limit; in - if count is_neq (map (LA_Data.decomp sg) Hs') - > !fast_arith_neq_limit then ( - trace_msg ("fast_arith_neq_limit exceeded (current value is " ^ - string_of_int (!fast_arith_neq_limit) ^ ")"); - NONE - ) else - refute sg params show_ex do_pre Hs' + if count is_neq (map (LA_Data.decomp ctxt) Hs') > neq_limit then + (trace_msg ("fast_arith_neq_limit exceeded (current value is " ^ + string_of_int neq_limit ^ ")"); NONE) + else + refute ctxt params show_ex do_pre Hs' end handle TERM ("neg_prop", _) => (* since no meta-logic negation is available, we can only fail if *) (* the conclusion is not of the form 'Trueprop $ _' (simply *) @@ -729,48 +731,52 @@ fun refute_tac ss (i, justs) = fn state => - let val _ = trace_thm ("refute_tac (on subgoal " ^ Int.toString i ^ ", with " ^ - Int.toString (length justs) ^ " justification(s)):") state - val sg = theory_of_thm state - val {neqE, ...} = Data.get sg - fun just1 j = - (* eliminate inequalities *) - REPEAT_DETERM (eresolve_tac neqE i) THEN - PRIMITIVE (trace_thm "State after neqE:") THEN - (* use theorems generated from the actual justifications *) - METAHYPS (fn asms => rtac (mkthm (sg, ss) asms j) 1) i - in (* rewrite "[| A1; ...; An |] ==> B" to "[| A1; ...; An; ~B |] ==> False" *) - DETERM (resolve_tac [LA_Logic.notI, LA_Logic.ccontr] i) THEN - (* user-defined preprocessing of the subgoal *) - DETERM (LA_Data.pre_tac i) THEN - PRIMITIVE (trace_thm "State after pre_tac:") THEN - (* prove every resulting subgoal, using its justification *) - EVERY (map just1 justs) + let + val ctxt = Simplifier.the_context ss; + val _ = trace_thm ("refute_tac (on subgoal " ^ string_of_int i ^ ", with " ^ + string_of_int (length justs) ^ " justification(s)):") state + val {neqE, ...} = get_data ctxt; + fun just1 j = + (* eliminate inequalities *) + REPEAT_DETERM (eresolve_tac neqE i) THEN + PRIMITIVE (trace_thm "State after neqE:") THEN + (* use theorems generated from the actual justifications *) + METAHYPS (fn asms => rtac (mkthm ss asms j) 1) i + in + (* rewrite "[| A1; ...; An |] ==> B" to "[| A1; ...; An; ~B |] ==> False" *) + DETERM (resolve_tac [LA_Logic.notI, LA_Logic.ccontr] i) THEN + (* user-defined preprocessing of the subgoal *) + DETERM (LA_Data.pre_tac ctxt i) THEN + PRIMITIVE (trace_thm "State after pre_tac:") THEN + (* prove every resulting subgoal, using its justification *) + EVERY (map just1 justs) end state; (* Fast but very incomplete decider. Only premises and conclusions that are already (negated) (in)equations are taken into account. *) -fun simpset_lin_arith_tac (ss : simpset) (show_ex : bool) (i : int) (st : thm) = - SUBGOAL (fn (A,_) => - let val params = rev (Logic.strip_params A) - val Hs = Logic.strip_assums_hyp A - val concl = Logic.strip_assums_concl A - in trace_thm ("Trying to refute subgoal " ^ string_of_int i) st; - case prove (Thm.theory_of_thm st) params show_ex true Hs concl of - NONE => (trace_msg "Refutation failed."; no_tac) - | SOME js => (trace_msg "Refutation succeeded."; refute_tac ss (i, js)) - end) i st; +fun simpset_lin_arith_tac ss show_ex = SUBGOAL (fn (A, i) => + let + val ctxt = Simplifier.the_context ss + val params = rev (Logic.strip_params A) + val Hs = Logic.strip_assums_hyp A + val concl = Logic.strip_assums_concl A + val _ = trace_term ctxt ("Trying to refute subgoal " ^ string_of_int i) A + in + case prove ctxt params show_ex true Hs concl of + NONE => (trace_msg "Refutation failed."; no_tac) + | SOME js => (trace_msg "Refutation succeeded."; refute_tac ss (i, js)) + end); -fun lin_arith_tac (show_ex : bool) (i : int) (st : thm) = - simpset_lin_arith_tac - (Simplifier.theory_context (Thm.theory_of_thm st) Simplifier.empty_ss) - show_ex i st; +fun cut_lin_arith_tac ss = + cut_facts_tac (Simplifier.prems_of_ss ss) THEN' + simpset_lin_arith_tac ss false; -fun cut_lin_arith_tac (ss : simpset) (i : int) = - cut_facts_tac (Simplifier.prems_of_ss ss) i THEN - simpset_lin_arith_tac ss false i; +fun lin_arith_tac ctxt = + simpset_lin_arith_tac (Simplifier.context ctxt Simplifier.empty_ss); + + (** Forward proof from theorems **) @@ -794,8 +800,8 @@ val (_, ct2) = Thm.dest_comb Ict2 in (ct1, ct2) end; -fun splitasms (sg : theory) (asms : thm list) : splittree = -let val {neqE, ...} = Data.get sg +fun splitasms ctxt (asms : thm list) : splittree = +let val {neqE, ...} = get_data ctxt fun elim_neq (asms', []) = Tip (rev asms') | elim_neq (asms', asm::asms) = (case get_first (fn th => SOME (asm COMP th) handle THM _ => NONE) neqE of @@ -808,70 +814,52 @@ | NONE => elim_neq (asm::asms', asms)) in elim_neq ([], asms) end; -fun fwdproof (ctxt : theory * simpset) (Tip asms : splittree) (j::js : injust list) = - (mkthm ctxt asms j, js) - | fwdproof ctxt (Spl (thm, ct1, tree1, ct2, tree2)) js = - let val (thm1, js1) = fwdproof ctxt tree1 js - val (thm2, js2) = fwdproof ctxt tree2 js1 +fun fwdproof ss (Tip asms : splittree) (j::js : injust list) = (mkthm ss asms j, js) + | fwdproof ss (Spl (thm, ct1, tree1, ct2, tree2)) js = + let + val (thm1, js1) = fwdproof ss tree1 js + val (thm2, js2) = fwdproof ss tree2 js1 val thm1' = implies_intr ct1 thm1 val thm2' = implies_intr ct2 thm2 - in (thm2' COMP (thm1' COMP thm), js2) end; -(* needs handle THM _ => NONE ? *) + in (thm2' COMP (thm1' COMP thm), js2) end; + (* FIXME needs handle THM _ => NONE ? *) -fun prover (ctxt as (sg, ss)) thms (Tconcl : term) (js : injust list) (pos : bool) : thm option = -let -(* vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv *) -(* Use this code instead if lin_arith_prover calls prove with do_pre set to true *) -(* but beware: this can be a significant performance issue. *) - (* There is no "forward version" of 'pre_tac'. Therefore we combine the *) - (* available theorems into a single proof state and perform "backward proof" *) - (* using 'refute_tac'. *) -(* - val Hs = map prop_of thms - val Prop = fold (curry Logic.mk_implies) (rev Hs) Tconcl - val cProp = cterm_of sg Prop - val concl = Goal.init cProp - |> refute_tac ss (1, js) - |> Seq.hd - |> Goal.finish - |> fold (fn thA => fn thAB => implies_elim thAB thA) thms -*) -(* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ *) - val nTconcl = LA_Logic.neg_prop Tconcl - val cnTconcl = cterm_of sg nTconcl - val nTconclthm = assume cnTconcl - val tree = splitasms sg (thms @ [nTconclthm]) - val (Falsethm, _) = fwdproof ctxt tree js - val contr = if pos then LA_Logic.ccontr else LA_Logic.notI - val concl = implies_intr cnTconcl Falsethm COMP contr -in SOME (trace_thm "Proved by lin. arith. prover:" - (LA_Logic.mk_Eq concl)) end -(* in case concl contains ?-var, which makes assume fail: *) -handle THM _ => NONE; +fun prover ss thms Tconcl (js : injust list) pos : thm option = + let + val ctxt = Simplifier.the_context ss + val thy = ProofContext.theory_of ctxt + val nTconcl = LA_Logic.neg_prop Tconcl + val cnTconcl = cterm_of thy nTconcl + val nTconclthm = assume cnTconcl + val tree = splitasms ctxt (thms @ [nTconclthm]) + val (Falsethm, _) = fwdproof ss tree js + val contr = if pos then LA_Logic.ccontr else LA_Logic.notI + val concl = implies_intr cnTconcl Falsethm COMP contr + in SOME (trace_thm "Proved by lin. arith. prover:" (LA_Logic.mk_Eq concl)) end + (*in case concl contains ?-var, which makes assume fail:*) (* FIXME Variable.import_terms *) + handle THM _ => NONE; (* PRE: concl is not negated! This assumption is OK because - 1. lin_arith_prover tries both to prove and disprove concl and - 2. lin_arith_prover is applied by the simplifier which + 1. lin_arith_simproc tries both to prove and disprove concl and + 2. lin_arith_simproc is applied by the Simplifier which dives into terms and will thus try the non-negated concl anyway. *) - -fun lin_arith_prover sg ss (concl : term) : thm option = -let val thms = List.concat (map LA_Logic.atomize (prems_of_ss ss)); - val Hs = map prop_of thms +fun lin_arith_simproc ss concl = + let + val ctxt = Simplifier.the_context ss + val thms = List.concat (map LA_Logic.atomize (Simplifier.prems_of_ss ss)) + val Hs = map Thm.prop_of thms val Tconcl = LA_Logic.mk_Trueprop concl -(* - val _ = trace_msg "lin_arith_prover" - val _ = map (trace_thm "thms:") thms - val _ = trace_msg ("concl:" ^ Sign.string_of_term sg concl) -*) -in case prove sg [] false false Hs Tconcl of (* concl provable? *) - SOME js => prover (sg, ss) thms Tconcl js true - | NONE => let val nTconcl = LA_Logic.neg_prop Tconcl - in case prove sg [] false false Hs nTconcl of (* ~concl provable? *) - SOME js => prover (sg, ss) thms nTconcl js false - | NONE => NONE - end -end; + in + case prove ctxt [] false false Hs Tconcl of (* concl provable? *) + SOME js => prover ss thms Tconcl js true + | NONE => + let val nTconcl = LA_Logic.neg_prop Tconcl in + case prove ctxt [] false false Hs nTconcl of (* ~concl provable? *) + SOME js => prover ss thms nTconcl js false + | NONE => NONE + end + end; end;