# HG changeset patch # User wenzelm # Date 1309372781 -7200 # Node ID 78211f66cf8d6b9e3274e3cbbcd24ca61e024917 # Parent 7ae4a23b5be69c0314588b918569678e662f760a simplified/unified Simplifier.mk_solver; diff -r 7ae4a23b5be6 -r 78211f66cf8d src/FOL/simpdata.ML --- a/src/FOL/simpdata.ML Wed Jun 29 18:12:34 2011 +0200 +++ b/src/FOL/simpdata.ML Wed Jun 29 20:39:41 2011 +0200 @@ -108,10 +108,10 @@ val triv_rls = [@{thm TrueI}, @{thm refl}, reflexive_thm, @{thm iff_refl}, @{thm notFalseI}]; -fun unsafe_solver prems = FIRST'[resolve_tac (triv_rls @ prems), +fun unsafe_solver ss = FIRST'[resolve_tac (triv_rls @ prems_of_ss ss), atac, etac @{thm FalseE}]; (*No premature instantiation of variables during simplification*) -fun safe_solver prems = FIRST'[match_tac (triv_rls @ prems), +fun safe_solver ss = FIRST'[match_tac (triv_rls @ prems_of_ss ss), eq_assume_tac, ematch_tac [@{thm FalseE}]]; (*No simprules, but basic infastructure for simplification*) diff -r 7ae4a23b5be6 -r 78211f66cf8d src/HOL/Orderings.thy --- a/src/HOL/Orderings.thy Wed Jun 29 18:12:34 2011 +0200 +++ b/src/HOL/Orderings.thy Wed Jun 29 20:39:41 2011 +0200 @@ -570,7 +570,7 @@ fun add_solver name tac = Simplifier.map_simpset_global (fn ss => ss addSolver - mk_solver' name (fn ss => tac (Simplifier.the_context ss) (Simplifier.prems_of_ss ss))); + mk_solver name (fn ss => tac (Simplifier.the_context ss) (prems_of_ss ss))); in add_simprocs [ diff -r 7ae4a23b5be6 -r 78211f66cf8d src/HOL/Statespace/distinct_tree_prover.ML --- a/src/HOL/Statespace/distinct_tree_prover.ML Wed Jun 29 18:12:34 2011 +0200 +++ b/src/HOL/Statespace/distinct_tree_prover.ML Wed Jun 29 20:39:41 2011 +0200 @@ -352,10 +352,8 @@ | NONE => no_tac) | _ => no_tac)) -fun distinctFieldSolver names = mk_solver' "distinctFieldSolver" - (fn ss => case try Simplifier.the_context ss of - SOME ctxt => distinctTree_tac names ctxt - | NONE => K no_tac) +fun distinctFieldSolver names = mk_solver "distinctFieldSolver" + (distinctTree_tac names o Simplifier.the_context) fun distinct_simproc names = Simplifier.simproc_global @{theory HOL} "DistinctTreeProver.distinct_simproc" ["x = y"] diff -r 7ae4a23b5be6 -r 78211f66cf8d src/HOL/Statespace/state_space.ML --- a/src/HOL/Statespace/state_space.ML Wed Jun 29 18:12:34 2011 +0200 +++ b/src/HOL/Statespace/state_space.ML Wed Jun 29 20:39:41 2011 +0200 @@ -225,10 +225,8 @@ | NONE => no_tac) | _ => no_tac)); -val distinctNameSolver = mk_solver' "distinctNameSolver" - (fn ss => case try Simplifier.the_context ss of - SOME ctxt => distinctTree_tac ctxt - | NONE => K no_tac) +val distinctNameSolver = mk_solver "distinctNameSolver" + (distinctTree_tac o Simplifier.the_context) val distinct_simproc = Simplifier.simproc_global @{theory HOL} "StateSpace.distinct_simproc" ["x = y"] diff -r 7ae4a23b5be6 -r 78211f66cf8d src/HOL/TLA/Memory/MemoryImplementation.thy --- a/src/HOL/TLA/Memory/MemoryImplementation.thy Wed Jun 29 18:12:34 2011 +0200 +++ b/src/HOL/TLA/Memory/MemoryImplementation.thy Wed Jun 29 20:39:41 2011 +0200 @@ -225,7 +225,7 @@ *) ML {* val config_fast_solver = Attrib.setup_config_bool @{binding fast_solver} (K false); - val fast_solver = mk_solver' "fast_solver" (fn ss => + val fast_solver = mk_solver "fast_solver" (fn ss => if Config.get (Simplifier.the_context ss) config_fast_solver then assume_tac ORELSE' (etac notE) else K no_tac); diff -r 7ae4a23b5be6 -r 78211f66cf8d src/HOL/Tools/Quotient/quotient_tacs.ML --- a/src/HOL/Tools/Quotient/quotient_tacs.ML Wed Jun 29 18:12:34 2011 +0200 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Wed Jun 29 20:39:41 2011 +0200 @@ -55,7 +55,7 @@ REPEAT_ALL_NEW (resolve_tac (Quotient_Info.equiv_rules_get ctxt)) fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss) -val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac +val equiv_solver = mk_solver "Equivalence goal solver" equiv_solver_tac fun quotient_tac ctxt = (REPEAT_ALL_NEW (FIRST' @@ -63,8 +63,7 @@ resolve_tac (Quotient_Info.quotient_rules_get ctxt)])) fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss) -val quotient_solver = - Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac +val quotient_solver = mk_solver "Quotient goal solver" quotient_solver_tac fun solve_quotient_assm ctxt thm = case Seq.pull (quotient_tac ctxt 1 thm) of diff -r 7ae4a23b5be6 -r 78211f66cf8d src/HOL/Tools/lin_arith.ML --- a/src/HOL/Tools/lin_arith.ML Wed Jun 29 18:12:34 2011 +0200 +++ b/src/HOL/Tools/lin_arith.ML Wed Jun 29 20:39:41 2011 +0200 @@ -895,7 +895,7 @@ val setup = init_arith_data #> Simplifier.map_ss (fn ss => ss - addSolver (mk_solver' "lin_arith" (add_arith_facts #> Fast_Arith.cut_lin_arith_tac))); + addSolver (mk_solver "lin_arith" (add_arith_facts #> Fast_Arith.cut_lin_arith_tac))); val global_setup = Attrib.setup @{binding arith_split} (Scan.succeed (Thm.declaration_attribute add_split)) diff -r 7ae4a23b5be6 -r 78211f66cf8d src/HOL/Tools/simpdata.ML --- a/src/HOL/Tools/simpdata.ML Wed Jun 29 18:12:34 2011 +0200 +++ b/src/HOL/Tools/simpdata.ML Wed Jun 29 20:39:41 2011 +0200 @@ -112,18 +112,18 @@ fun mksimps pairs (_: simpset) = map_filter (try mk_eq) o mk_atomize pairs o gen_all; -fun unsafe_solver_tac prems = +fun unsafe_solver_tac ss = (fn i => REPEAT_DETERM (match_tac @{thms simp_impliesI} i)) THEN' - FIRST' [resolve_tac (reflexive_thm :: @{thm TrueI} :: @{thm refl} :: prems), atac, + FIRST' [resolve_tac (reflexive_thm :: @{thm TrueI} :: @{thm refl} :: prems_of_ss ss), atac, etac @{thm FalseE}]; val unsafe_solver = mk_solver "HOL unsafe" unsafe_solver_tac; (*No premature instantiation of variables during simplification*) -fun safe_solver_tac prems = +fun safe_solver_tac ss = (fn i => REPEAT_DETERM (match_tac @{thms simp_impliesI} i)) THEN' - FIRST' [match_tac (reflexive_thm :: @{thm TrueI} :: @{thm refl} :: prems), + FIRST' [match_tac (reflexive_thm :: @{thm TrueI} :: @{thm refl} :: prems_of_ss ss), eq_assume_tac, ematch_tac @{thms FalseE}]; val safe_solver = mk_solver "HOL safe" safe_solver_tac; diff -r 7ae4a23b5be6 -r 78211f66cf8d src/HOL/Transitive_Closure.thy --- a/src/HOL/Transitive_Closure.thy Wed Jun 29 18:12:34 2011 +0200 +++ b/src/HOL/Transitive_Closure.thy Wed Jun 29 20:39:41 2011 +0200 @@ -1029,10 +1029,10 @@ setup {* Simplifier.map_simpset_global (fn ss => ss - addSolver (mk_solver' "Trancl" (Trancl_Tac.trancl_tac o Simplifier.the_context)) - addSolver (mk_solver' "Rtrancl" (Trancl_Tac.rtrancl_tac o Simplifier.the_context)) - addSolver (mk_solver' "Tranclp" (Tranclp_Tac.trancl_tac o Simplifier.the_context)) - addSolver (mk_solver' "Rtranclp" (Tranclp_Tac.rtrancl_tac o Simplifier.the_context))) + addSolver (mk_solver "Trancl" (Trancl_Tac.trancl_tac o Simplifier.the_context)) + addSolver (mk_solver "Rtrancl" (Trancl_Tac.rtrancl_tac o Simplifier.the_context)) + addSolver (mk_solver "Tranclp" (Tranclp_Tac.trancl_tac o Simplifier.the_context)) + addSolver (mk_solver "Rtranclp" (Tranclp_Tac.rtrancl_tac o Simplifier.the_context))) *} diff -r 7ae4a23b5be6 -r 78211f66cf8d src/Pure/raw_simplifier.ML --- a/src/Pure/raw_simplifier.ML Wed Jun 29 18:12:34 2011 +0200 +++ b/src/Pure/raw_simplifier.ML Wed Jun 29 20:39:41 2011 +0200 @@ -20,8 +20,7 @@ type simpset type proc type solver - val mk_solver': string -> (simpset -> int -> tactic) -> solver - val mk_solver: string -> (thm list -> int -> tactic) -> solver + val mk_solver: string -> (simpset -> int -> tactic) -> solver val empty_ss: simpset val merge_ss: simpset * simpset -> simpset val dest_ss: simpset -> @@ -242,8 +241,7 @@ s1 = s2 andalso eq_list Thm.eq_thm (ths1, ths2); fun eq_proc (Proc {id = id1, ...}, Proc {id = id2, ...}) = eq_procid (id1, id2); -fun mk_solver' name solver = Solver {name = name, solver = solver, id = stamp ()}; -fun mk_solver name solver = mk_solver' name (solver o prems_of_ss); +fun mk_solver name solver = Solver {name = name, solver = solver, id = stamp ()}; fun solver_name (Solver {name, ...}) = name; fun solver ss (Solver {solver = tac, ...}) = tac ss; diff -r 7ae4a23b5be6 -r 78211f66cf8d src/Pure/simplifier.ML --- a/src/Pure/simplifier.ML Wed Jun 29 18:12:34 2011 +0200 +++ b/src/Pure/simplifier.ML Wed Jun 29 20:39:41 2011 +0200 @@ -396,11 +396,11 @@ let val trivialities = Drule.reflexive_thm :: trivs; - fun unsafe_solver_tac prems = FIRST' [resolve_tac (trivialities @ prems), assume_tac]; + fun unsafe_solver_tac ss = FIRST' [resolve_tac (trivialities @ prems_of_ss ss), assume_tac]; val unsafe_solver = mk_solver "easy unsafe" unsafe_solver_tac; (*no premature instantiation of variables during simplification*) - fun safe_solver_tac prems = FIRST' [match_tac (trivialities @ prems), eq_assume_tac]; + fun safe_solver_tac ss = FIRST' [match_tac (trivialities @ prems_of_ss ss), eq_assume_tac]; val safe_solver = mk_solver "easy safe" safe_solver_tac; fun mk_eq thm = diff -r 7ae4a23b5be6 -r 78211f66cf8d src/Sequents/simpdata.ML --- a/src/Sequents/simpdata.ML Wed Jun 29 18:12:34 2011 +0200 +++ b/src/Sequents/simpdata.ML Wed Jun 29 20:39:41 2011 +0200 @@ -58,12 +58,12 @@ val triv_rls = [@{thm FalseL}, @{thm TrueR}, @{thm basic}, @{thm refl}, @{thm iff_refl}, reflexive_thm]; -fun unsafe_solver prems = - FIRST' [resolve_tac (triv_rls @ prems), assume_tac]; +fun unsafe_solver ss = + FIRST' [resolve_tac (triv_rls @ prems_of_ss ss), assume_tac]; (*No premature instantiation of variables during simplification*) -fun safe_solver prems = - FIRST' [fn i => DETERM (match_tac (triv_rls @ prems) i), eq_assume_tac]; +fun safe_solver ss = + FIRST' [fn i => DETERM (match_tac (triv_rls @ prems_of_ss ss) i), eq_assume_tac]; (*No simprules, but basic infrastructure for simplification*) val LK_basic_ss = diff -r 7ae4a23b5be6 -r 78211f66cf8d src/ZF/Tools/inductive_package.ML --- a/src/ZF/Tools/inductive_package.ML Wed Jun 29 18:12:34 2011 +0200 +++ b/src/ZF/Tools/inductive_package.ML Wed Jun 29 20:39:41 2011 +0200 @@ -329,7 +329,7 @@ val min_ss = Simplifier.global_context thy empty_ss setmksimps (K (map mk_eq o ZF_atomize o gen_all)) setSolver (mk_solver "minimal" - (fn prems => resolve_tac (triv_rls@prems) + (fn ss => resolve_tac (triv_rls @ prems_of_ss ss) ORELSE' assume_tac ORELSE' etac @{thm FalseE})); diff -r 7ae4a23b5be6 -r 78211f66cf8d src/ZF/Tools/typechk.ML --- a/src/ZF/Tools/typechk.ML Wed Jun 29 18:12:34 2011 +0200 +++ b/src/ZF/Tools/typechk.ML Wed Jun 29 20:39:41 2011 +0200 @@ -105,8 +105,9 @@ ORELSE (ares_tac hyps 1 APPEND typecheck_step_tac (tcset_of ctxt)))); -val type_solver = Simplifier.mk_solver' "ZF typecheck" (fn ss => - type_solver_tac (Simplifier.the_context ss) (Simplifier.prems_of_ss ss)); +val type_solver = + Simplifier.mk_solver "ZF typecheck" (fn ss => + type_solver_tac (Simplifier.the_context ss) (prems_of_ss ss)); (* concrete syntax *)