Theory Named_Simpsets
section ‹Named Simpsets›
theory Named_Simpsets
imports Main
keywords "named_simpset" :: thy_decl and "print_named_simpset" :: diag
begin
subsection ‹Setup›
ML_file "named_simpsets.ML"
ML ‹
val _ =
Outer_Syntax.local_theory \<^command_keyword>‹named_simpset›
"declare named simpset"
(Parse.binding -- Scan.option (\<^keyword>‹=› |-- Parse.position Parse.embedded) >> uncurry Named_Simpsets.declare_cmd);
›
ML ‹
val _ = let
fun print_named_simpset_cmd name_src bang ctxt = let
val name = Named_Simpsets.check ctxt name_src
in
Named_Simpsets.put name ctxt
|> Simplifier.pretty_simpset bang
|> Pretty.writeln
end
in
Outer_Syntax.command \<^command_keyword>‹print_named_simpset›
"print named simpset"
(Parse.position Parse.name -- Parse.opt_bang >> (fn (name_src,b) =>
Toplevel.keep (print_named_simpset_cmd name_src b o Toplevel.context_of)))
end
›
local_setup ‹ I
#> Named_Simpsets.declare @{binding HOL_ss} (SOME HOL_ss)
#> Named_Simpsets.declare @{binding HOL_basic_ss} (SOME HOL_basic_ss)
#> Named_Simpsets.declare @{binding Main_ss} (SOME (simpset_of @{context}))
›
setup ‹let
val named_ss_mod = Args.$$$ "named_ss" |-- Parse.position Parse.name --| Args.colon
>> (fn raw_binding => {
init = (fn ctxt => Named_Simpsets.put (Named_Simpsets.check ctxt raw_binding) ctxt ),
attribute = Simplifier.simp_add,
pos = ⌂
})
in
Simplifier.method_setup (named_ss_mod :: Splitter.split_modifiers)
end
›
named_simpset HOL_basic_ss_nomatch = HOL_basic_ss
declaration ‹fn _ => Named_Simpsets.map_ctxt @{named_simpset HOL_basic_ss_nomatch} (fn ctxt => ctxt addsimprocs [@{simproc NO_MATCH}])›
named_simpset HOL_ss_nomatch = HOL_ss
declaration ‹fn _ => Named_Simpsets.map_ctxt @{named_simpset HOL_ss_nomatch} (fn ctxt => ctxt addsimprocs [@{simproc NO_MATCH}])›
subsection ‹Examples›
experiment
begin
subsubsection ‹Isar Interface›
named_simpset bar
named_simpset foo = HOL_ss
print_named_simpset bar
print_named_simpset foo
print_named_simpset HOL_basic_ss
print_named_simpset HOL_ss
print_named_simpset Main_ss
declare nth_append[named_ss bar]
declare nth_append[named_ss bar del]
declare nth_append[named_ss bar add]
declare if_split[named_ss bar split add]
declare if_split[named_ss bar split del]
declare if_split[named_ss bar split]
declare if_cong[named_ss bar cong add]
declare if_cong[named_ss bar cong del]
declare if_cong[named_ss bar cong]
lemma "([1,2,3]@[4])!1 = 2"
apply (simp named_ss bar:)
by simp
lemma "([1,2,3]@[4])!1 = 2"
supply [[put_named_ss bar]]
apply simp
apply (simp named_ss Main_ss:)
done
lemma "([1,2,3]@[4])!1 = 2"
apply (use [[put_named_ss bar]] in simp)
by simp
subsubsection ‹ML Interface›
local_setup ‹Named_Simpsets.declare @{binding foo2} NONE›
local_setup ‹Named_Simpsets.declare @{binding foo3} (SOME HOL_ss)›
ML_val ‹
val ctxt = @{context}
val ctxt = Named_Simpsets.put @{named_simpset foo} ctxt
val _ = Named_Simpsets.map_ctxt
›
end
end