--- a/NEWS Fri Apr 12 17:02:55 2013 +0200
+++ b/NEWS Fri Apr 12 17:21:51 2013 +0200
@@ -129,6 +129,11 @@
* Antiquotation @{theory_context A} is similar to @{theory A}, but
presents the result as initial Proof.context.
+* Modifiers for classical wrappers (e.g. addWrapper, delWrapper)
+operate on Proof.context instead of claset, for uniformity with addIs,
+addEs, addDs etc. Note that claset_of and put_claset allow to manage
+clasets separately from the context.
+
*** System ***
--- a/src/Doc/IsarRef/Generic.thy Fri Apr 12 17:02:55 2013 +0200
+++ b/src/Doc/IsarRef/Generic.thy Fri Apr 12 17:21:51 2013 +0200
@@ -1814,16 +1814,20 @@
text {*
\begin{mldecls}
@{index_ML_type wrapper: "(int -> tactic) -> (int -> tactic)"} \\[0.5ex]
- @{index_ML_op addSWrapper: "claset * (string * (Proof.context -> wrapper))
- -> claset"} \\
- @{index_ML_op addSbefore: "claset * (string * (int -> tactic)) -> claset"} \\
- @{index_ML_op addSafter: "claset * (string * (int -> tactic)) -> claset"} \\
- @{index_ML_op delSWrapper: "claset * string -> claset"} \\[0.5ex]
- @{index_ML_op addWrapper: "claset * (string * (Proof.context -> wrapper))
- -> claset"} \\
- @{index_ML_op addbefore: "claset * (string * (int -> tactic)) -> claset"} \\
- @{index_ML_op addafter: "claset * (string * (int -> tactic)) -> claset"} \\
- @{index_ML_op delWrapper: "claset * string -> claset"} \\[0.5ex]
+ @{index_ML_op addSWrapper: "Proof.context *
+ (string * (Proof.context -> wrapper)) -> Proof.context"} \\
+ @{index_ML_op addSbefore: "Proof.context *
+ (string * (int -> tactic)) -> Proof.context"} \\
+ @{index_ML_op addSafter: "Proof.context *
+ (string * (int -> tactic)) -> Proof.context"} \\
+ @{index_ML_op delSWrapper: "Proof.context * string -> Proof.context"} \\[0.5ex]
+ @{index_ML_op addWrapper: "Proof.context *
+ (string * (Proof.context -> wrapper)) -> Proof.context"} \\
+ @{index_ML_op addbefore: "Proof.context *
+ (string * (int -> tactic)) -> Proof.context"} \\
+ @{index_ML_op addafter: "Proof.context *
+ (string * (int -> tactic)) -> Proof.context"} \\
+ @{index_ML_op delWrapper: "Proof.context * string -> Proof.context"} \\[0.5ex]
@{index_ML addSss: "Proof.context -> Proof.context"} \\
@{index_ML addss: "Proof.context -> Proof.context"} \\
\end{mldecls}
@@ -1856,33 +1860,33 @@
\begin{description}
- \item @{text "cs addSWrapper (name, wrapper)"} adds a new wrapper,
+ \item @{text "ctxt addSWrapper (name, wrapper)"} adds a new wrapper,
which should yield a safe tactic, to modify the existing safe step
tactic.
- \item @{text "cs addSbefore (name, tac)"} adds the given tactic as a
+ \item @{text "ctxt addSbefore (name, tac)"} adds the given tactic as a
safe wrapper, such that it is tried \emph{before} each safe step of
the search.
- \item @{text "cs addSafter (name, tac)"} adds the given tactic as a
+ \item @{text "ctxt addSafter (name, tac)"} adds the given tactic as a
safe wrapper, such that it is tried when a safe step of the search
would fail.
- \item @{text "cs delSWrapper name"} deletes the safe wrapper with
+ \item @{text "ctxt delSWrapper name"} deletes the safe wrapper with
the given name.
- \item @{text "cs addWrapper (name, wrapper)"} adds a new wrapper to
+ \item @{text "ctxt addWrapper (name, wrapper)"} adds a new wrapper to
modify the existing (unsafe) step tactic.
- \item @{text "cs addbefore (name, tac)"} adds the given tactic as an
+ \item @{text "ctxt addbefore (name, tac)"} adds the given tactic as an
unsafe wrapper, such that it its result is concatenated
\emph{before} the result of each unsafe step.
- \item @{text "cs addafter (name, tac)"} adds the given tactic as an
+ \item @{text "ctxt addafter (name, tac)"} adds the given tactic as an
unsafe wrapper, such that it its result is concatenated \emph{after}
the result of each unsafe step.
- \item @{text "cs delWrapper name"} deletes the unsafe wrapper with
+ \item @{text "ctxt delWrapper name"} deletes the unsafe wrapper with
the given name.
\item @{text "addSss"} adds the simpset of the context to its
--- a/src/HOL/Bali/AxSem.thy Fri Apr 12 17:02:55 2013 +0200
+++ b/src/HOL/Bali/AxSem.thy Fri Apr 12 17:21:51 2013 +0200
@@ -465,7 +465,7 @@
declare split_if [split del] split_if_asm [split del]
option.split [split del] option.split_asm [split del]
declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
-declaration {* K (Classical.map_cs (fn cs => cs delSWrapper "split_all_tac")) *}
+setup {* map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac") *}
inductive
ax_derivs :: "prog \<Rightarrow> 'a triples \<Rightarrow> 'a triples \<Rightarrow> bool" ("_,_|\<turnstile>_" [61,58,58] 57)
--- a/src/HOL/Bali/TypeSafe.thy Fri Apr 12 17:02:55 2013 +0200
+++ b/src/HOL/Bali/TypeSafe.thy Fri Apr 12 17:21:51 2013 +0200
@@ -727,7 +727,7 @@
declare split_if [split del] split_if_asm [split del]
option.split [split del] option.split_asm [split del]
declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
-declaration {* K (Classical.map_cs (fn cs => cs delSWrapper "split_all_tac")) *}
+setup {* map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac") *}
lemma FVar_lemma:
"\<lbrakk>((v, f), Norm s2') = fvar statDeclC (static field) fn a (x2, s2);
@@ -755,7 +755,7 @@
declare split_paired_All [simp] split_paired_Ex [simp]
declare split_if [split] split_if_asm [split]
option.split [split] option.split_asm [split]
-declaration {* K (Classical.map_cs (fn cs => cs addSbefore ("split_all_tac", split_all_tac))) *}
+setup {* map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac)) *}
declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
@@ -872,7 +872,7 @@
declare split_if [split del] split_if_asm [split del]
option.split [split del] option.split_asm [split del]
declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
-declaration {* K (Classical.map_cs (fn cs => cs delSWrapper "split_all_tac")) *}
+setup {* map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac") *}
lemma conforms_init_lvars:
"\<lbrakk>wf_mhead G (pid declC) sig (mhead (mthd dm)); wf_prog G;
@@ -924,7 +924,7 @@
declare split_paired_All [simp] split_paired_Ex [simp]
declare split_if [split] split_if_asm [split]
option.split [split] option.split_asm [split]
-declaration {* K (Classical.map_cs (fn cs => cs addSbefore ("split_all_tac", split_all_tac))) *}
+setup {* map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac)) *}
declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
--- a/src/HOL/Bali/WellForm.thy Fri Apr 12 17:02:55 2013 +0200
+++ b/src/HOL/Bali/WellForm.thy Fri Apr 12 17:21:51 2013 +0200
@@ -2128,7 +2128,7 @@
declare split_paired_All [simp del] split_paired_Ex [simp del]
declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
-declaration {* K (Classical.map_cs (fn cs => cs delSWrapper "split_all_tac")) *}
+setup {* map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac") *}
lemma dynamic_mheadsD:
"\<lbrakk>emh \<in> mheads G S statT sig;
@@ -2257,7 +2257,7 @@
qed
qed
declare split_paired_All [simp] split_paired_Ex [simp]
-declaration {* K (Classical.map_cs (fn cs => cs addSbefore ("split_all_tac", split_all_tac))) *}
+setup {* map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac)) *}
declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
(* Tactical version *)
@@ -2402,7 +2402,7 @@
declare split_paired_All [simp del] split_paired_Ex [simp del]
declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
-declaration {* K (Classical.map_cs (fn cs => cs delSWrapper "split_all_tac")) *}
+setup {* map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac") *}
lemma wt_is_type: "E,dt\<Turnstile>v\<Colon>T \<Longrightarrow> wf_prog (prg E) \<longrightarrow>
dt=empty_dt \<longrightarrow> (case T of
@@ -2426,7 +2426,7 @@
)
done
declare split_paired_All [simp] split_paired_Ex [simp]
-declaration {* K (Classical.map_cs (fn cs => cs addSbefore ("split_all_tac", split_all_tac))) *}
+setup {* map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac)) *}
declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
lemma ty_expr_is_type:
--- a/src/HOL/HOLCF/IOA/NTP/Correctness.thy Fri Apr 12 17:02:55 2013 +0200
+++ b/src/HOL/HOLCF/IOA/NTP/Correctness.thy Fri Apr 12 17:21:51 2013 +0200
@@ -13,10 +13,7 @@
"hom s = rq(rec(s)) @ (if rbit(rec s) = sbit(sen s) then sq(sen s)
else tl(sq(sen s)))"
-declaration {* fn _ =>
- (* repeated from Traces.ML *)
- Classical.map_cs (fn cs => cs delSWrapper "split_all_tac")
-*}
+setup {* map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac") *}
lemmas hom_ioas = Spec.ioa_def Spec.trans_def sender_trans_def receiver_trans_def impl_ioas
and impl_asigs = sender_asig_def receiver_asig_def srch_asig_def rsch_asig_def
--- a/src/HOL/HOLCF/IOA/meta_theory/TLS.thy Fri Apr 12 17:02:55 2013 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/TLS.thy Fri Apr 12 17:21:51 2013 +0200
@@ -92,7 +92,7 @@
lemmas [simp del] = HOL.ex_simps HOL.all_simps split_paired_Ex
-declaration {* fn _ => Classical.map_cs (fn cs => cs delSWrapper "split_all_tac") *}
+setup {* map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac") *}
subsection {* ex2seqC *}
--- a/src/HOL/HOLCF/IOA/meta_theory/Traces.thy Fri Apr 12 17:02:55 2013 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/Traces.thy Fri Apr 12 17:21:51 2013 +0200
@@ -203,7 +203,7 @@
lemmas [simp del] = HOL.ex_simps HOL.all_simps split_paired_Ex
declare Let_def [simp]
-declaration {* fn _ => Classical.map_cs (fn cs => cs delSWrapper "split_all_tac") *}
+setup {* map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac") *}
lemmas exec_rws = executions_def is_exec_frag_def
--- a/src/HOL/Option.thy Fri Apr 12 17:02:55 2013 +0200
+++ b/src/HOL/Option.thy Fri Apr 12 17:21:51 2013 +0200
@@ -46,9 +46,7 @@
lemma ospec [dest]: "(ALL x:set A. P x) ==> A = Some x ==> P x"
by simp
-declaration {* fn _ =>
- Classical.map_cs (fn cs => cs addSD2 ("ospec", @{thm ospec}))
-*}
+setup {* map_theory_claset (fn ctxt => ctxt addSD2 ("ospec", @{thm ospec})) *}
lemma elem_set [iff]: "(x : set xo) = (xo = Some x)"
by (cases xo) auto
--- a/src/HOL/Product_Type.thy Fri Apr 12 17:02:55 2013 +0200
+++ b/src/HOL/Product_Type.thy Fri Apr 12 17:21:51 2013 +0200
@@ -428,9 +428,7 @@
end;
*}
-declaration {* fn _ =>
- Classical.map_cs (fn cs => cs addSbefore ("split_all_tac", split_all_tac))
-*}
+setup {* map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac)) *}
lemma split_paired_All [simp, no_atp]: "(ALL x. P x) = (ALL a b. P (a, b))"
-- {* @{text "[iff]"} is not a good idea because it makes @{text blast} loop *}
@@ -583,9 +581,7 @@
(* This prevents applications of splitE for already splitted arguments leading
to quite time-consuming computations (in particular for nested tuples) *)
-declaration {* fn _ =>
- Classical.map_cs (fn cs => cs addSbefore ("split_conv_tac", split_conv_tac))
-*}
+setup {* map_theory_claset (fn ctxt => ctxt addSbefore ("split_conv_tac", split_conv_tac)) *}
lemma split_eta_SetCompr [simp,no_atp]: "(%u. EX x y. u = (x, y) & P (x, y)) = P"
by (rule ext) fast
--- a/src/HOL/Set.thy Fri Apr 12 17:02:55 2013 +0200
+++ b/src/HOL/Set.thy Fri Apr 12 17:21:51 2013 +0200
@@ -379,8 +379,8 @@
Gives better instantiation for bound:
*}
-declaration {* fn _ =>
- Classical.map_cs (fn cs => cs addbefore ("bspec", dtac @{thm bspec} THEN' assume_tac))
+setup {*
+ map_theory_claset (fn ctxt => ctxt addbefore ("bspec", dtac @{thm bspec} THEN' assume_tac))
*}
ML {*
--- a/src/HOL/UNITY/Comp/Alloc.thy Fri Apr 12 17:02:55 2013 +0200
+++ b/src/HOL/UNITY/Comp/Alloc.thy Fri Apr 12 17:21:51 2013 +0200
@@ -329,8 +329,7 @@
ML {*
fun record_auto_tac ctxt =
let val ctxt' =
- ctxt
- |> map_claset (fn cs => cs addSWrapper Record.split_wrapper)
+ (ctxt addSWrapper Record.split_wrapper)
|> map_simpset (fn ss => ss addsimps
[@{thm sysOfAlloc_def}, @{thm sysOfClient_def},
@{thm client_map_def}, @{thm non_dummy_def}, @{thm funPair_def},
--- a/src/Provers/clasimp.ML Fri Apr 12 17:02:55 2013 +0200
+++ b/src/Provers/clasimp.ML Fri Apr 12 17:21:51 2013 +0200
@@ -44,8 +44,7 @@
(* simp as classical wrapper *)
-fun clasimp f name tac ctxt =
- Classical.map_claset (fn cs => f (cs, (name, CHANGED o tac (simpset_of ctxt)))) ctxt;
+fun clasimp f name tac ctxt = f (ctxt, (name, CHANGED o tac (simpset_of ctxt)));
(*Add a simpset to the claset!*)
(*Caution: only one simpset added can be added by each of addSss and addss*)
--- a/src/Provers/classical.ML Fri Apr 12 17:02:55 2013 +0200
+++ b/src/Provers/classical.ML Fri Apr 12 17:21:51 2013 +0200
@@ -41,18 +41,18 @@
val addSEs: Proof.context * thm list -> Proof.context
val addSIs: Proof.context * thm list -> Proof.context
val delrules: Proof.context * thm list -> Proof.context
- val addSWrapper: claset * (string * (Proof.context -> wrapper)) -> claset
- val delSWrapper: claset * string -> claset
- val addWrapper: claset * (string * (Proof.context -> wrapper)) -> claset
- val delWrapper: claset * string -> claset
- val addSbefore: claset * (string * (int -> tactic)) -> claset
- val addSafter: claset * (string * (int -> tactic)) -> claset
- val addbefore: claset * (string * (int -> tactic)) -> claset
- val addafter: claset * (string * (int -> tactic)) -> claset
- val addD2: claset * (string * thm) -> claset
- val addE2: claset * (string * thm) -> claset
- val addSD2: claset * (string * thm) -> claset
- val addSE2: claset * (string * thm) -> claset
+ val addSWrapper: Proof.context * (string * (Proof.context -> wrapper)) -> Proof.context
+ val delSWrapper: Proof.context * string -> Proof.context
+ val addWrapper: Proof.context * (string * (Proof.context -> wrapper)) -> Proof.context
+ val delWrapper: Proof.context * string -> Proof.context
+ val addSbefore: Proof.context * (string * (int -> tactic)) -> Proof.context
+ val addSafter: Proof.context * (string * (int -> tactic)) -> Proof.context
+ val addbefore: Proof.context * (string * (int -> tactic)) -> Proof.context
+ val addafter: Proof.context * (string * (int -> tactic)) -> Proof.context
+ val addD2: Proof.context * (string * thm) -> Proof.context
+ val addE2: Proof.context * (string * thm) -> Proof.context
+ val addSD2: Proof.context * (string * thm) -> Proof.context
+ val addSE2: Proof.context * (string * thm) -> Proof.context
val appSWrappers: Proof.context -> wrapper
val appWrappers: Proof.context -> wrapper
@@ -60,6 +60,8 @@
val map_claset: (claset -> claset) -> Proof.context -> Proof.context
val put_claset: claset -> Proof.context -> Proof.context
+ val map_theory_claset: (Proof.context -> Proof.context) -> theory -> theory
+
val fast_tac: Proof.context -> int -> tactic
val slow_tac: Proof.context -> int -> tactic
val astar_tac: Proof.context -> int -> tactic
@@ -601,6 +603,12 @@
val get_cs = Claset.get;
val map_cs = Claset.map;
+fun map_theory_claset f thy =
+ let
+ val ctxt' = f (Proof_Context.init_global thy);
+ val thy' = Proof_Context.theory_of ctxt';
+ in Context.theory_map (Claset.map (K (claset_of ctxt'))) thy' end;
+
fun map_claset f = Context.proof_map (map_cs f);
fun put_claset cs = map_claset (K cs);
@@ -646,33 +654,33 @@
else (warning msg; xs);
(*Add/replace a safe wrapper*)
-fun cs addSWrapper new_swrapper =
- map_swrappers (update_warn ("Overwriting safe wrapper " ^ fst new_swrapper) new_swrapper) cs;
+fun ctxt addSWrapper new_swrapper = ctxt |> map_claset
+ (map_swrappers (update_warn ("Overwriting safe wrapper " ^ fst new_swrapper) new_swrapper));
(*Add/replace an unsafe wrapper*)
-fun cs addWrapper new_uwrapper =
- map_uwrappers (update_warn ("Overwriting unsafe wrapper " ^ fst new_uwrapper) new_uwrapper) cs;
+fun ctxt addWrapper new_uwrapper = ctxt |> map_claset
+ (map_uwrappers (update_warn ("Overwriting unsafe wrapper " ^ fst new_uwrapper) new_uwrapper));
(*Remove a safe wrapper*)
-fun cs delSWrapper name =
- map_swrappers (delete_warn ("No such safe wrapper in claset: " ^ name) name) cs;
+fun ctxt delSWrapper name = ctxt |> map_claset
+ (map_swrappers (delete_warn ("No such safe wrapper in claset: " ^ name) name));
(*Remove an unsafe wrapper*)
-fun cs delWrapper name =
- map_uwrappers (delete_warn ("No such unsafe wrapper in claset: " ^ name) name) cs;
+fun ctxt delWrapper name = ctxt |> map_claset
+ (map_uwrappers (delete_warn ("No such unsafe wrapper in claset: " ^ name) name));
(* compose a safe tactic alternatively before/after safe_step_tac *)
-fun cs addSbefore (name, tac1) = cs addSWrapper (name, fn _ => fn tac2 => tac1 ORELSE' tac2);
-fun cs addSafter (name, tac2) = cs addSWrapper (name, fn _ => fn tac1 => tac1 ORELSE' tac2);
+fun ctxt addSbefore (name, tac1) = ctxt addSWrapper (name, fn _ => fn tac2 => tac1 ORELSE' tac2);
+fun ctxt addSafter (name, tac2) = ctxt addSWrapper (name, fn _ => fn tac1 => tac1 ORELSE' tac2);
(*compose a tactic alternatively before/after the step tactic *)
-fun cs addbefore (name, tac1) = cs addWrapper (name, fn _ => fn tac2 => tac1 APPEND' tac2);
-fun cs addafter (name, tac2) = cs addWrapper (name, fn _ => fn tac1 => tac1 APPEND' tac2);
+fun ctxt addbefore (name, tac1) = ctxt addWrapper (name, fn _ => fn tac2 => tac1 APPEND' tac2);
+fun ctxt addafter (name, tac2) = ctxt addWrapper (name, fn _ => fn tac1 => tac1 APPEND' tac2);
-fun cs addD2 (name, thm) = cs addafter (name, dtac thm THEN' assume_tac);
-fun cs addE2 (name, thm) = cs addafter (name, etac thm THEN' assume_tac);
-fun cs addSD2 (name, thm) = cs addSafter (name, dmatch_tac [thm] THEN' eq_assume_tac);
-fun cs addSE2 (name, thm) = cs addSafter (name, ematch_tac [thm] THEN' eq_assume_tac);
+fun ctxt addD2 (name, thm) = ctxt addafter (name, dtac thm THEN' assume_tac);
+fun ctxt addE2 (name, thm) = ctxt addafter (name, etac thm THEN' assume_tac);
+fun ctxt addSD2 (name, thm) = ctxt addSafter (name, dmatch_tac [thm] THEN' eq_assume_tac);
+fun ctxt addSE2 (name, thm) = ctxt addSafter (name, ematch_tac [thm] THEN' eq_assume_tac);