tuned signature -- depend on context by default;
authorwenzelm
Thu May 16 17:39:38 2013 +0200 (2013-05-16)
changeset 52037837211662fb8
parent 52036 1aa2e40df9ff
child 52038 a354c83dee43
child 52039 d0ba73d11e32
tuned signature -- depend on context by default;
src/CCL/Term.thy
src/Doc/IsarRef/Generic.thy
src/HOL/Bali/Basis.thy
src/HOL/Bali/DefiniteAssignment.thy
src/HOL/Bali/Eval.thy
src/HOL/Bali/Evaln.thy
src/HOL/Bali/TypeSafe.thy
src/HOL/Bali/WellForm.thy
src/HOL/Bali/WellType.thy
src/HOL/TLA/Action.thy
src/Provers/splitter.ML
src/Pure/raw_simplifier.ML
     1.1 --- a/src/CCL/Term.thy	Thu May 16 15:21:12 2013 +0200
     1.2 +++ b/src/CCL/Term.thy	Thu May 16 17:39:38 2013 +0200
     1.3 @@ -204,7 +204,7 @@
     1.4  method_setup beta_rl = {*
     1.5    Scan.succeed (fn ctxt =>
     1.6      SIMPLE_METHOD' (CHANGED o
     1.7 -      simp_tac (ctxt addsimps @{thms rawBs} setloop (stac @{thm letrecB}))))
     1.8 +      simp_tac (ctxt addsimps @{thms rawBs} setloop (fn _ => stac @{thm letrecB}))))
     1.9  *}
    1.10  
    1.11  lemma ifBtrue: "if true then t else u = t"
     2.1 --- a/src/Doc/IsarRef/Generic.thy	Thu May 16 15:21:12 2013 +0200
     2.2 +++ b/src/Doc/IsarRef/Generic.thy	Thu May 16 17:39:38 2013 +0200
     2.3 @@ -1143,12 +1143,8 @@
     2.4  text {*
     2.5    \begin{mldecls}
     2.6    @{index_ML_op setloop: "Proof.context *
     2.7 -  (int -> tactic) -> Proof.context"} \\
     2.8 -  @{index_ML_op setloop': "Proof.context *
     2.9    (Proof.context -> int -> tactic) -> Proof.context"} \\
    2.10    @{index_ML_op addloop: "Proof.context *
    2.11 -  (string * (int -> tactic)) -> Proof.context"} \\
    2.12 -  @{index_ML_op addloop': "Proof.context *
    2.13    (string * (Proof.context -> int -> tactic))
    2.14    -> Proof.context"} \\
    2.15    @{index_ML_op delloop: "Proof.context * string -> Proof.context"} \\
    2.16 @@ -1169,15 +1165,13 @@
    2.17    \begin{description}
    2.18  
    2.19    \item @{text "ctxt setloop tac"} installs @{text "tac"} as the only
    2.20 -  looper tactic of @{text "ctxt"}.  The variant @{text "setloop'"}
    2.21 -  allows the tactic to depend on the running Simplifier context.
    2.22 +  looper tactic of @{text "ctxt"}.
    2.23  
    2.24    \item @{text "ctxt addloop (name, tac)"} adds @{text "tac"} as an
    2.25    additional looper tactic with name @{text "name"}, which is
    2.26    significant for managing the collection of loopers.  The tactic will
    2.27    be tried after the looper tactics that had already been present in
    2.28 -  @{text "ctxt"}.  The variant @{text "addloop'"} allows the tactic to
    2.29 -  depend on the running Simplifier context.
    2.30 +  @{text "ctxt"}.
    2.31  
    2.32    \item @{text "ctxt delloop name"} deletes the looper tactic that was
    2.33    associated with @{text "name"} from @{text "ctxt"}.
     3.1 --- a/src/HOL/Bali/Basis.thy	Thu May 16 15:21:12 2013 +0200
     3.2 +++ b/src/HOL/Bali/Basis.thy	Thu May 16 17:39:38 2013 +0200
     3.3 @@ -12,7 +12,7 @@
     3.4  ML {* fun strip_tac i = REPEAT (resolve_tac [impI, allI] i) *}
     3.5  
     3.6  declare split_if_asm  [split] option.split [split] option.split_asm [split]
     3.7 -setup {* map_theory_simpset (fn ctxt => ctxt addloop' ("split_all_tac", split_all_tac)) *}
     3.8 +setup {* map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac)) *}
     3.9  declare if_weak_cong [cong del] option.weak_case_cong [cong del]
    3.10  declare length_Suc_conv [iff]
    3.11  
     4.1 --- a/src/HOL/Bali/DefiniteAssignment.thy	Thu May 16 15:21:12 2013 +0200
     4.2 +++ b/src/HOL/Bali/DefiniteAssignment.thy	Thu May 16 17:39:38 2013 +0200
     4.3 @@ -884,7 +884,7 @@
     4.4  declare inj_term_sym_simps [simp del]
     4.5  declare assigns_if.simps [simp]
     4.6  declare split_paired_All [simp] split_paired_Ex [simp]
     4.7 -setup {* map_theory_simpset (fn ctxt => ctxt addloop' ("split_all_tac", split_all_tac)) *}
     4.8 +setup {* map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac)) *}
     4.9  
    4.10  (* To be able to eliminate both the versions with the overloaded brackets: 
    4.11     (B \<guillemotright>\<langle>Skip\<rangle>\<guillemotright> A) and with the explicit constructor (B \<guillemotright>In1r Skip\<guillemotright> A), 
     5.1 --- a/src/HOL/Bali/Eval.thy	Thu May 16 15:21:12 2013 +0200
     5.2 +++ b/src/HOL/Bali/Eval.thy	Thu May 16 17:39:38 2013 +0200
     5.3 @@ -818,7 +818,7 @@
     5.4          "G\<turnstile>Norm s \<midarrow>In1r (Init C)                       \<succ>\<rightarrow> (x, s')"
     5.5  declare not_None_eq [simp]  (* IntDef.Zero_def [simp] *)
     5.6  declare split_paired_All [simp] split_paired_Ex [simp]
     5.7 -declaration {* K (Simplifier.map_ss (fn ss => ss addloop' ("split_all_tac", split_all_tac))) *}
     5.8 +declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
     5.9  declare split_if     [split] split_if_asm     [split] 
    5.10          option.split [split] option.split_asm [split]
    5.11  
     6.1 --- a/src/HOL/Bali/Evaln.thy	Thu May 16 15:21:12 2013 +0200
     6.2 +++ b/src/HOL/Bali/Evaln.thy	Thu May 16 17:39:38 2013 +0200
     6.3 @@ -238,7 +238,7 @@
     6.4          option.split [split] option.split_asm [split]
     6.5          not_None_eq [simp] 
     6.6          split_paired_All [simp] split_paired_Ex [simp]
     6.7 -declaration {* K (Simplifier.map_ss (fn ss => ss addloop' ("split_all_tac", split_all_tac))) *}
     6.8 +declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
     6.9  
    6.10  lemma evaln_Inj_elim: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (w,s') \<Longrightarrow> case t of In1 ec \<Rightarrow>  
    6.11    (case ec of Inl e \<Rightarrow> (\<exists>v. w = In1 v) | Inr c \<Rightarrow> w = \<diamondsuit>)  
     7.1 --- a/src/HOL/Bali/TypeSafe.thy	Thu May 16 15:21:12 2013 +0200
     7.2 +++ b/src/HOL/Bali/TypeSafe.thy	Thu May 16 17:39:38 2013 +0200
     7.3 @@ -756,7 +756,7 @@
     7.4  declare split_if     [split] split_if_asm     [split] 
     7.5          option.split [split] option.split_asm [split]
     7.6  setup {* map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac)) *}
     7.7 -setup {* map_theory_simpset (fn ctxt => ctxt addloop' ("split_all_tac", split_all_tac)) *}
     7.8 +setup {* map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac)) *}
     7.9  
    7.10  
    7.11  lemma AVar_lemma1: "\<lbrakk>globs s (Inl a) = Some obj;tag obj=Arr ty i; 
    7.12 @@ -925,7 +925,7 @@
    7.13  declare split_if     [split] split_if_asm     [split] 
    7.14          option.split [split] option.split_asm [split]
    7.15  setup {* map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac)) *}
    7.16 -setup {* map_theory_simpset (fn ctxt => ctxt addloop' ("split_all_tac", split_all_tac)) *}
    7.17 +setup {* map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac)) *}
    7.18  
    7.19  
    7.20  subsection "accessibility"
     8.1 --- a/src/HOL/Bali/WellForm.thy	Thu May 16 15:21:12 2013 +0200
     8.2 +++ b/src/HOL/Bali/WellForm.thy	Thu May 16 17:39:38 2013 +0200
     8.3 @@ -2258,7 +2258,7 @@
     8.4  qed
     8.5  declare split_paired_All [simp] split_paired_Ex [simp]
     8.6  setup {* map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac)) *}
     8.7 -setup {* map_theory_simpset (fn ctxt => ctxt addloop' ("split_all_tac", split_all_tac)) *}
     8.8 +setup {* map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac)) *}
     8.9  
    8.10  (* Tactical version *)
    8.11  (*
    8.12 @@ -2427,7 +2427,7 @@
    8.13  done
    8.14  declare split_paired_All [simp] split_paired_Ex [simp]
    8.15  setup {* map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac)) *}
    8.16 -setup {* map_theory_simpset (fn ctxt => ctxt addloop' ("split_all_tac", split_all_tac)) *}
    8.17 +setup {* map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac)) *}
    8.18  
    8.19  lemma ty_expr_is_type: 
    8.20  "\<lbrakk>E\<turnstile>e\<Colon>-T; wf_prog (prg E)\<rbrakk> \<Longrightarrow> is_type (prg E) T"
     9.1 --- a/src/HOL/Bali/WellType.thy	Thu May 16 15:21:12 2013 +0200
     9.2 +++ b/src/HOL/Bali/WellType.thy	Thu May 16 17:39:38 2013 +0200
     9.3 @@ -494,7 +494,7 @@
     9.4  declare not_None_eq [simp] 
     9.5  declare split_if [split] split_if_asm [split]
     9.6  declare split_paired_All [simp] split_paired_Ex [simp]
     9.7 -setup {* map_theory_simpset (fn ctxt => ctxt addloop' ("split_all_tac", split_all_tac)) *}
     9.8 +setup {* map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac)) *}
     9.9  
    9.10  lemma is_acc_class_is_accessible: 
    9.11    "is_acc_class G P C \<Longrightarrow> G\<turnstile>(Class C) accessible_in P"
    10.1 --- a/src/HOL/TLA/Action.thy	Thu May 16 15:21:12 2013 +0200
    10.2 +++ b/src/HOL/TLA/Action.thy	Thu May 16 17:39:38 2013 +0200
    10.3 @@ -260,7 +260,7 @@
    10.4  *)
    10.5  fun action_simp_tac ss intros elims =
    10.6      asm_full_simp_tac
    10.7 -         (ss setloop ((resolve_tac ((map action_use intros)
    10.8 +         (ss setloop (fn _ => (resolve_tac ((map action_use intros)
    10.9                                      @ [refl,impI,conjI,@{thm actionI},@{thm intI},allI]))
   10.10                        ORELSE' (eresolve_tac ((map action_use elims)
   10.11                                               @ [conjE,disjE,exE]))));
    11.1 --- a/src/Provers/splitter.ML	Thu May 16 15:21:12 2013 +0200
    11.2 +++ b/src/Provers/splitter.ML	Thu May 16 17:39:38 2013 +0200
    11.3 @@ -430,7 +430,7 @@
    11.4    let
    11.5      val (name, asm) = split_thm_info split
    11.6      val tac = (if asm then split_asm_tac else split_tac) [split]
    11.7 -  in Simplifier.addloop (ctxt, (split_name name asm, tac)) end;
    11.8 +  in Simplifier.addloop (ctxt, (split_name name asm, K tac)) end;
    11.9  
   11.10  fun del_split split ctxt =
   11.11    let val (name, asm) = split_thm_info split
    12.1 --- a/src/Pure/raw_simplifier.ML	Thu May 16 15:21:12 2013 +0200
    12.2 +++ b/src/Pure/raw_simplifier.ML	Thu May 16 17:39:38 2013 +0200
    12.3 @@ -6,7 +6,7 @@
    12.4  
    12.5  infix 4
    12.6    addsimps delsimps addsimprocs delsimprocs
    12.7 -  setloop' setloop addloop addloop' delloop
    12.8 +  setloop addloop delloop
    12.9    setSSolver addSSolver setSolver addSolver;
   12.10  
   12.11  signature BASIC_RAW_SIMPLIFIER =
   12.12 @@ -49,10 +49,8 @@
   12.13    val delsimps: Proof.context * thm list -> Proof.context
   12.14    val addsimprocs: Proof.context * simproc list -> Proof.context
   12.15    val delsimprocs: Proof.context * simproc list -> Proof.context
   12.16 -  val setloop': Proof.context * (Proof.context -> int -> tactic) -> Proof.context
   12.17 -  val setloop: Proof.context * (int -> tactic) -> Proof.context
   12.18 -  val addloop': Proof.context * (string * (Proof.context -> int -> tactic)) -> Proof.context
   12.19 -  val addloop: Proof.context * (string * (int -> tactic)) -> Proof.context
   12.20 +  val setloop: Proof.context * (Proof.context -> int -> tactic) -> Proof.context
   12.21 +  val addloop: Proof.context * (string * (Proof.context -> int -> tactic)) -> Proof.context
   12.22    val delloop: Proof.context * string -> Proof.context
   12.23    val setSSolver: Proof.context * solver -> Proof.context
   12.24    val addSSolver: Proof.context * solver -> Proof.context
   12.25 @@ -821,19 +819,15 @@
   12.26    map_simpset2 (fn (congs, procs, mk_rews, termless, _, loop_tacs, solvers) =>
   12.27     (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers));
   12.28  
   12.29 -fun ctxt setloop' tac = ctxt |>
   12.30 +fun ctxt setloop tac = ctxt |>
   12.31    map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, _, solvers) =>
   12.32     (congs, procs, mk_rews, termless, subgoal_tac, [("", tac)], solvers));
   12.33  
   12.34 -fun ctxt setloop tac = ctxt setloop' (K tac);
   12.35 -
   12.36 -fun ctxt addloop' (name, tac) = ctxt |>
   12.37 +fun ctxt addloop (name, tac) = ctxt |>
   12.38    map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
   12.39      (congs, procs, mk_rews, termless, subgoal_tac,
   12.40       AList.update (op =) (name, tac) loop_tacs, solvers));
   12.41  
   12.42 -fun ctxt addloop (name, tac) = ctxt addloop' (name, K tac);
   12.43 -
   12.44  fun ctxt delloop name = ctxt |>
   12.45    map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
   12.46      (congs, procs, mk_rews, termless, subgoal_tac,