# HG changeset patch # User wenzelm # Date 1425896460 -3600 # Node ID ddc5411c1cb9577169967f485c44d1452660b266 # Parent 5d1b4ab7d173c930d6f3f5c9eae0ca8e764ba268 eliminated dead code (cf. 5e5c36b051af); diff -r 5d1b4ab7d173 -r ddc5411c1cb9 src/HOL/Tools/lin_arith.ML --- a/src/HOL/Tools/lin_arith.ML Mon Mar 09 10:52:23 2015 +0100 +++ b/src/HOL/Tools/lin_arith.ML Mon Mar 09 11:21:00 2015 +0100 @@ -778,8 +778,7 @@ val add_simprocs = Fast_Arith.add_simprocs; val set_number_of = Fast_Arith.set_number_of; -fun simple_tac ctxt = Fast_Arith.lin_arith_tac ctxt false; -val lin_arith_tac = Fast_Arith.lin_arith_tac; +val simple_tac = Fast_Arith.lin_arith_tac; (* reduce contradictory <= to False. Most of the work is done by the cancel tactics. *) @@ -853,7 +852,7 @@ local -fun raw_tac ctxt ex = +fun raw_tac ctxt = (* FIXME: K true should be replaced by a sensible test (perhaps "is_some 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 @@ -869,16 +868,14 @@ (* Therefore splitting outside of simple_tac may allow us to prove *) (* some goals that simple_tac alone would fail on. *) (REPEAT_DETERM o split_tac ctxt (#splits (get_arith_data ctxt))) - (lin_arith_tac ctxt ex); + (Fast_Arith.lin_arith_tac ctxt); in -fun gen_tac ex ctxt = +fun tac ctxt = FIRST' [simple_tac ctxt, Object_Logic.full_atomize_tac ctxt THEN' - (REPEAT_DETERM o resolve_tac ctxt [impI]) THEN' raw_tac ctxt ex]; - -val tac = gen_tac true; + (REPEAT_DETERM o resolve_tac ctxt [impI]) THEN' raw_tac ctxt]; end; @@ -895,7 +892,7 @@ METHOD (fn facts => HEADGOAL (Method.insert_tac (rev (Named_Theorems.get ctxt @{named_theorems arith}) @ facts) THEN' tac ctxt)))) "linear arithmetic" #> - Arith_Data.add_tactic "linear arithmetic" gen_tac; + Arith_Data.add_tactic "linear arithmetic" (K tac); val setup = init_arith_data diff -r 5d1b4ab7d173 -r ddc5411c1cb9 src/Provers/Arith/fast_lin_arith.ML --- a/src/Provers/Arith/fast_lin_arith.ML Mon Mar 09 10:52:23 2015 +0100 +++ b/src/Provers/Arith/fast_lin_arith.ML Mon Mar 09 11:21:00 2015 +0100 @@ -59,7 +59,6 @@ into two cases, this can lead to an explosion*) val neq_limit: int Config.T - val verbose: bool Config.T val trace: bool Config.T end; (* @@ -87,7 +86,7 @@ signature FAST_LIN_ARITH = sig val prems_lin_arith_tac: Proof.context -> int -> tactic - val lin_arith_tac: Proof.context -> bool -> int -> tactic + val lin_arith_tac: Proof.context -> int -> tactic val lin_arith_simproc: Proof.context -> term -> thm option val map_data: ({add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list, @@ -735,10 +734,7 @@ fun add_datoms ((lhs,_,_,rhs,_,d) : LA_Data.decomp, _) (dats : (bool * term) list) = union_bterm (map (pair d o fst) lhs) (union_bterm (map (pair d o fst) rhs) dats); -fun discr (initems : (LA_Data.decomp * int) list) : bool list = - map fst (fold add_datoms initems []); - -fun refutes ctxt params show_ex : +fun refutes ctxt : (typ list * (LA_Data.decomp * int) list) list -> injust list -> injust list option = let fun refute ((Ts, initems : (LA_Data.decomp * int) list) :: initemss) (js: injust list) = @@ -750,32 +746,22 @@ val iatoms = atoms ~~ ixs val natlineqs = map_filter (mknat Ts ixs) iatoms val ineqs = map mkleq initems @ natlineqs - in case elim ctxt (ineqs, []) of + in + (case elim ctxt (ineqs, []) of Success j => (trace_msg ctxt ("Contradiction! (" ^ string_of_int (length js + 1) ^ ")"); refute initemss (js @ [j])) - | Failure hist => - (if not show_ex orelse not (Config.get ctxt LA_Data.verbose) then () - else - let - val (param_names, ctxt') = ctxt |> Variable.variant_fixes (map fst params) - val (more_names, ctxt'') = ctxt' |> Variable.variant_fixes - (Name.invent (Variable.names_of ctxt') Name.uu (length Ts - length params)) - val params' = (more_names @ param_names) ~~ Ts - in - () (*trace_ex ctxt'' params' atoms (discr initems) n hist*) - end; NONE) + | Failure _ => NONE) end | refute [] js = SOME js in refute end; -fun refute ctxt params show_ex do_pre split_neq terms : injust list option = - refutes ctxt params show_ex (split_items ctxt do_pre split_neq - (map snd params, terms)) []; +fun refute ctxt params do_pre split_neq terms : injust list option = + refutes ctxt (split_items ctxt do_pre split_neq (map snd params, terms)) []; fun count P xs = length (filter P xs); -fun prove ctxt params show_ex do_pre Hs concl : bool * injust list option = +fun prove ctxt params do_pre Hs concl : bool * injust list option = let val _ = trace_msg ctxt "prove:" (* append the negated conclusion to 'Hs' -- this corresponds to *) @@ -791,7 +777,7 @@ else trace_msg ctxt ("neq_limit exceeded (current value is " ^ string_of_int neq_limit ^ "), ignoring all inequalities"); - (split_neq, refute ctxt params show_ex do_pre split_neq Hs') + (split_neq, refute ctxt params do_pre split_neq 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 *) @@ -830,14 +816,14 @@ Fast but very incomplete decider. Only premises and conclusions that are already (negated) (in)equations are taken into account. *) -fun simpset_lin_arith_tac ctxt show_ex = SUBGOAL (fn (A, i) => +fun simpset_lin_arith_tac ctxt = SUBGOAL (fn (A, i) => let 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 + case prove ctxt params true Hs concl of (_, NONE) => (trace_msg ctxt "Refutation failed."; no_tac) | (split_neq, SOME js) => (trace_msg ctxt "Refutation succeeded."; refute_tac ctxt (i, split_neq, js)) @@ -845,7 +831,7 @@ fun prems_lin_arith_tac ctxt = Method.insert_tac (Simplifier.prems_of ctxt) THEN' - simpset_lin_arith_tac ctxt false; + simpset_lin_arith_tac ctxt; fun lin_arith_tac ctxt = simpset_lin_arith_tac (empty_simpset ctxt); @@ -926,11 +912,11 @@ val Hs = map Thm.prop_of thms val Tconcl = LA_Logic.mk_Trueprop concl in - case prove ctxt [] false false Hs Tconcl of (* concl provable? *) + case prove ctxt [] false Hs Tconcl of (* concl provable? *) (split_neq, SOME js) => prover ctxt thms Tconcl js split_neq true | (_, NONE) => let val nTconcl = LA_Logic.neg_prop Tconcl in - case prove ctxt [] false false Hs nTconcl of (* ~concl provable? *) + case prove ctxt [] false Hs nTconcl of (* ~concl provable? *) (split_neq, SOME js) => prover ctxt thms nTconcl js split_neq false | (_, NONE) => NONE end