# HG changeset patch # User wenzelm # Date 1368718778 -7200 # Node ID 837211662fb83585955fcb299d93e27f92f3d7b9 # Parent 1aa2e40df9ff36052c0a686df37e7a71c37e5443 tuned signature -- depend on context by default; diff -r 1aa2e40df9ff -r 837211662fb8 src/CCL/Term.thy --- a/src/CCL/Term.thy Thu May 16 15:21:12 2013 +0200 +++ b/src/CCL/Term.thy Thu May 16 17:39:38 2013 +0200 @@ -204,7 +204,7 @@ method_setup beta_rl = {* Scan.succeed (fn ctxt => SIMPLE_METHOD' (CHANGED o - simp_tac (ctxt addsimps @{thms rawBs} setloop (stac @{thm letrecB})))) + simp_tac (ctxt addsimps @{thms rawBs} setloop (fn _ => stac @{thm letrecB})))) *} lemma ifBtrue: "if true then t else u = t" diff -r 1aa2e40df9ff -r 837211662fb8 src/Doc/IsarRef/Generic.thy --- a/src/Doc/IsarRef/Generic.thy Thu May 16 15:21:12 2013 +0200 +++ b/src/Doc/IsarRef/Generic.thy Thu May 16 17:39:38 2013 +0200 @@ -1143,12 +1143,8 @@ text {* \begin{mldecls} @{index_ML_op setloop: "Proof.context * - (int -> tactic) -> Proof.context"} \\ - @{index_ML_op setloop': "Proof.context * (Proof.context -> int -> tactic) -> Proof.context"} \\ @{index_ML_op addloop: "Proof.context * - (string * (int -> tactic)) -> Proof.context"} \\ - @{index_ML_op addloop': "Proof.context * (string * (Proof.context -> int -> tactic)) -> Proof.context"} \\ @{index_ML_op delloop: "Proof.context * string -> Proof.context"} \\ @@ -1169,15 +1165,13 @@ \begin{description} \item @{text "ctxt setloop tac"} installs @{text "tac"} as the only - looper tactic of @{text "ctxt"}. The variant @{text "setloop'"} - allows the tactic to depend on the running Simplifier context. + looper tactic of @{text "ctxt"}. \item @{text "ctxt addloop (name, tac)"} adds @{text "tac"} as an additional looper tactic with name @{text "name"}, which is significant for managing the collection of loopers. The tactic will be tried after the looper tactics that had already been present in - @{text "ctxt"}. The variant @{text "addloop'"} allows the tactic to - depend on the running Simplifier context. + @{text "ctxt"}. \item @{text "ctxt delloop name"} deletes the looper tactic that was associated with @{text "name"} from @{text "ctxt"}. diff -r 1aa2e40df9ff -r 837211662fb8 src/HOL/Bali/Basis.thy --- a/src/HOL/Bali/Basis.thy Thu May 16 15:21:12 2013 +0200 +++ b/src/HOL/Bali/Basis.thy Thu May 16 17:39:38 2013 +0200 @@ -12,7 +12,7 @@ ML {* fun strip_tac i = REPEAT (resolve_tac [impI, allI] i) *} declare split_if_asm [split] option.split [split] option.split_asm [split] -setup {* map_theory_simpset (fn ctxt => ctxt addloop' ("split_all_tac", split_all_tac)) *} +setup {* map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac)) *} declare if_weak_cong [cong del] option.weak_case_cong [cong del] declare length_Suc_conv [iff] diff -r 1aa2e40df9ff -r 837211662fb8 src/HOL/Bali/DefiniteAssignment.thy --- a/src/HOL/Bali/DefiniteAssignment.thy Thu May 16 15:21:12 2013 +0200 +++ b/src/HOL/Bali/DefiniteAssignment.thy Thu May 16 17:39:38 2013 +0200 @@ -884,7 +884,7 @@ declare inj_term_sym_simps [simp del] declare assigns_if.simps [simp] declare split_paired_All [simp] split_paired_Ex [simp] -setup {* map_theory_simpset (fn ctxt => ctxt addloop' ("split_all_tac", split_all_tac)) *} +setup {* map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac)) *} (* To be able to eliminate both the versions with the overloaded brackets: (B \\Skip\\ A) and with the explicit constructor (B \In1r Skip\ A), diff -r 1aa2e40df9ff -r 837211662fb8 src/HOL/Bali/Eval.thy --- a/src/HOL/Bali/Eval.thy Thu May 16 15:21:12 2013 +0200 +++ b/src/HOL/Bali/Eval.thy Thu May 16 17:39:38 2013 +0200 @@ -818,7 +818,7 @@ "G\Norm s \In1r (Init C) \\ (x, s')" declare not_None_eq [simp] (* IntDef.Zero_def [simp] *) declare split_paired_All [simp] split_paired_Ex [simp] -declaration {* K (Simplifier.map_ss (fn ss => ss addloop' ("split_all_tac", split_all_tac))) *} +declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *} declare split_if [split] split_if_asm [split] option.split [split] option.split_asm [split] diff -r 1aa2e40df9ff -r 837211662fb8 src/HOL/Bali/Evaln.thy --- a/src/HOL/Bali/Evaln.thy Thu May 16 15:21:12 2013 +0200 +++ b/src/HOL/Bali/Evaln.thy Thu May 16 17:39:38 2013 +0200 @@ -238,7 +238,7 @@ option.split [split] option.split_asm [split] not_None_eq [simp] split_paired_All [simp] split_paired_Ex [simp] -declaration {* K (Simplifier.map_ss (fn ss => ss addloop' ("split_all_tac", split_all_tac))) *} +declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *} lemma evaln_Inj_elim: "G\s \t\\n\ (w,s') \ case t of In1 ec \ (case ec of Inl e \ (\v. w = In1 v) | Inr c \ w = \) diff -r 1aa2e40df9ff -r 837211662fb8 src/HOL/Bali/TypeSafe.thy --- a/src/HOL/Bali/TypeSafe.thy Thu May 16 15:21:12 2013 +0200 +++ b/src/HOL/Bali/TypeSafe.thy Thu May 16 17:39:38 2013 +0200 @@ -756,7 +756,7 @@ declare split_if [split] split_if_asm [split] option.split [split] option.split_asm [split] setup {* map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac)) *} -setup {* map_theory_simpset (fn ctxt => ctxt addloop' ("split_all_tac", split_all_tac)) *} +setup {* map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac)) *} lemma AVar_lemma1: "\globs s (Inl a) = Some obj;tag obj=Arr ty i; @@ -925,7 +925,7 @@ declare split_if [split] split_if_asm [split] option.split [split] option.split_asm [split] setup {* map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac)) *} -setup {* map_theory_simpset (fn ctxt => ctxt addloop' ("split_all_tac", split_all_tac)) *} +setup {* map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac)) *} subsection "accessibility" diff -r 1aa2e40df9ff -r 837211662fb8 src/HOL/Bali/WellForm.thy --- a/src/HOL/Bali/WellForm.thy Thu May 16 15:21:12 2013 +0200 +++ b/src/HOL/Bali/WellForm.thy Thu May 16 17:39:38 2013 +0200 @@ -2258,7 +2258,7 @@ qed declare split_paired_All [simp] split_paired_Ex [simp] setup {* map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac)) *} -setup {* map_theory_simpset (fn ctxt => ctxt addloop' ("split_all_tac", split_all_tac)) *} +setup {* map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac)) *} (* Tactical version *) (* @@ -2427,7 +2427,7 @@ done declare split_paired_All [simp] split_paired_Ex [simp] setup {* map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac)) *} -setup {* map_theory_simpset (fn ctxt => ctxt addloop' ("split_all_tac", split_all_tac)) *} +setup {* map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac)) *} lemma ty_expr_is_type: "\E\e\-T; wf_prog (prg E)\ \ is_type (prg E) T" diff -r 1aa2e40df9ff -r 837211662fb8 src/HOL/Bali/WellType.thy --- a/src/HOL/Bali/WellType.thy Thu May 16 15:21:12 2013 +0200 +++ b/src/HOL/Bali/WellType.thy Thu May 16 17:39:38 2013 +0200 @@ -494,7 +494,7 @@ declare not_None_eq [simp] declare split_if [split] split_if_asm [split] declare split_paired_All [simp] split_paired_Ex [simp] -setup {* map_theory_simpset (fn ctxt => ctxt addloop' ("split_all_tac", split_all_tac)) *} +setup {* map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac)) *} lemma is_acc_class_is_accessible: "is_acc_class G P C \ G\(Class C) accessible_in P" diff -r 1aa2e40df9ff -r 837211662fb8 src/HOL/TLA/Action.thy --- a/src/HOL/TLA/Action.thy Thu May 16 15:21:12 2013 +0200 +++ b/src/HOL/TLA/Action.thy Thu May 16 17:39:38 2013 +0200 @@ -260,7 +260,7 @@ *) fun action_simp_tac ss intros elims = asm_full_simp_tac - (ss setloop ((resolve_tac ((map action_use intros) + (ss setloop (fn _ => (resolve_tac ((map action_use intros) @ [refl,impI,conjI,@{thm actionI},@{thm intI},allI])) ORELSE' (eresolve_tac ((map action_use elims) @ [conjE,disjE,exE])))); diff -r 1aa2e40df9ff -r 837211662fb8 src/Provers/splitter.ML --- a/src/Provers/splitter.ML Thu May 16 15:21:12 2013 +0200 +++ b/src/Provers/splitter.ML Thu May 16 17:39:38 2013 +0200 @@ -430,7 +430,7 @@ let val (name, asm) = split_thm_info split val tac = (if asm then split_asm_tac else split_tac) [split] - in Simplifier.addloop (ctxt, (split_name name asm, tac)) end; + in Simplifier.addloop (ctxt, (split_name name asm, K tac)) end; fun del_split split ctxt = let val (name, asm) = split_thm_info split diff -r 1aa2e40df9ff -r 837211662fb8 src/Pure/raw_simplifier.ML --- a/src/Pure/raw_simplifier.ML Thu May 16 15:21:12 2013 +0200 +++ b/src/Pure/raw_simplifier.ML Thu May 16 17:39:38 2013 +0200 @@ -6,7 +6,7 @@ infix 4 addsimps delsimps addsimprocs delsimprocs - setloop' setloop addloop addloop' delloop + setloop addloop delloop setSSolver addSSolver setSolver addSolver; signature BASIC_RAW_SIMPLIFIER = @@ -49,10 +49,8 @@ val delsimps: Proof.context * thm list -> Proof.context val addsimprocs: Proof.context * simproc list -> Proof.context val delsimprocs: Proof.context * simproc list -> Proof.context - val setloop': Proof.context * (Proof.context -> int -> tactic) -> Proof.context - val setloop: Proof.context * (int -> tactic) -> Proof.context - val addloop': Proof.context * (string * (Proof.context -> int -> tactic)) -> Proof.context - val addloop: Proof.context * (string * (int -> tactic)) -> Proof.context + val setloop: Proof.context * (Proof.context -> int -> tactic) -> Proof.context + val addloop: Proof.context * (string * (Proof.context -> int -> tactic)) -> Proof.context val delloop: Proof.context * string -> Proof.context val setSSolver: Proof.context * solver -> Proof.context val addSSolver: Proof.context * solver -> Proof.context @@ -821,19 +819,15 @@ map_simpset2 (fn (congs, procs, mk_rews, termless, _, loop_tacs, solvers) => (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers)); -fun ctxt setloop' tac = ctxt |> +fun ctxt setloop tac = ctxt |> map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, _, solvers) => (congs, procs, mk_rews, termless, subgoal_tac, [("", tac)], solvers)); -fun ctxt setloop tac = ctxt setloop' (K tac); - -fun ctxt addloop' (name, tac) = ctxt |> +fun ctxt addloop (name, tac) = ctxt |> map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) => (congs, procs, mk_rews, termless, subgoal_tac, AList.update (op =) (name, tac) loop_tacs, solvers)); -fun ctxt addloop (name, tac) = ctxt addloop' (name, K tac); - fun ctxt delloop name = ctxt |> map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) => (congs, procs, mk_rews, termless, subgoal_tac,