--- a/src/Doc/Isar_Ref/Generic.thy Thu Apr 07 22:09:23 2016 +0200
+++ b/src/Doc/Isar_Ref/Generic.thy Fri Apr 08 20:15:20 2016 +0200
@@ -794,8 +794,7 @@
@{rail \<open>
@@{command simproc_setup} @{syntax name} '(' (@{syntax term} + '|') ')' '='
- @{syntax text} \<newline> (@'identifier' (@{syntax nameref}+))?
- ;
+ @{syntax text};
@@{attribute simproc} (('add' ':')? | 'del' ':') (@{syntax name}+)
\<close>}
@@ -810,12 +809,10 @@
NONE} to indicate failure. The @{ML_type Proof.context} argument holds the
full context of the current Simplifier invocation. The @{ML_type morphism}
informs about the difference of the original compilation context wrt.\ the
- one of the actual application later on. The optional @{keyword "identifier"}
- specifies theorems that represent the logical content of the abstract theory
- of this simproc.
+ one of the actual application later on.
- Morphisms and identifiers are only relevant for simprocs that are defined
- within a local target context, e.g.\ in a locale.
+ Morphisms are only relevant for simprocs that are defined within a local
+ target context, e.g.\ in a locale.
\<^descr> \<open>simproc add: name\<close> and \<open>simproc del: name\<close> add or delete named simprocs
to the current Simplifier context. The default is to add a simproc. Note
--- a/src/HOL/Decision_Procs/langford.ML Thu Apr 07 22:09:23 2016 +0200
+++ b/src/HOL/Decision_Procs/langford.ML Fri Apr 08 20:15:20 2016 +0200
@@ -171,7 +171,7 @@
val reduce_ex_simproc =
Simplifier.make_simproc @{context} "reduce_ex_simproc"
- {lhss = [@{term "\<exists>x. P x"}], proc = K proc, identifier = []};
+ {lhss = [@{term "\<exists>x. P x"}], proc = K proc};
end;
--- a/src/HOL/HOL.thy Thu Apr 07 22:09:23 2016 +0200
+++ b/src/HOL/HOL.thy Fri Apr 08 20:15:20 2016 +0200
@@ -1444,8 +1444,7 @@
(case Thm.term_of ct of
_ $ (P as _ $ @{const induct_false}) $ (_ $ Q $ _) =>
if P <> Q then SOME Drule.swap_prems_eq else NONE
- | _ => NONE),
- identifier = []},
+ | _ => NONE)},
Simplifier.make_simproc @{context} "induct_equal_conj_curry"
{lhss = [@{term "induct_conj P Q \<Longrightarrow> PROP R"}],
proc = fn _ => fn _ => fn ct =>
@@ -1459,8 +1458,7 @@
| is_conj @{const induct_false} = true
| is_conj _ = false
in if is_conj P then SOME @{thm induct_conj_curry} else NONE end
- | _ => NONE),
- identifier = []}]
+ | _ => NONE)}]
|> Simplifier.set_mksimps (fn ctxt =>
Simpdata.mksimps Simpdata.mksimps_pairs ctxt #>
map (rewrite_rule ctxt (map Thm.symmetric @{thms induct_rulify_fallback}))))
@@ -1759,8 +1757,7 @@
proc = fn _ => fn _ => fn ct =>
(case Thm.term_of ct of
Const (_, Type (@{type_name fun}, [Type _, _])) => SOME @{thm eq_equal}
- | _ => NONE),
- identifier = []}])
+ | _ => NONE)}])
\<close>
--- a/src/HOL/HOLCF/Tools/cont_proc.ML Thu Apr 07 22:09:23 2016 +0200
+++ b/src/HOL/HOLCF/Tools/cont_proc.ML Fri Apr 08 20:15:20 2016 +0200
@@ -127,7 +127,7 @@
in
val cont_proc =
Simplifier.make_simproc @{context} "cont_proc"
- {lhss = [@{term "cont f"}], proc = K solve_cont, identifier = []}
+ {lhss = [@{term "cont f"}], proc = K solve_cont}
end
val setup = map_theory_simpset (fn ctxt => ctxt addsimprocs [cont_proc])
--- a/src/HOL/Library/Old_SMT/old_smt_real.ML Thu Apr 07 22:09:23 2016 +0200
+++ b/src/HOL/Library/Old_SMT/old_smt_real.ML Fri Apr 08 20:15:20 2016 +0200
@@ -117,7 +117,7 @@
val real_linarith_proc =
Simplifier.make_simproc @{context} "fast_real_arith"
{lhss = [@{term "(m::real) < n"}, @{term "(m::real) \<le> n"}, @{term "(m::real) = n"}],
- proc = K Lin_Arith.simproc, identifier = []}
+ proc = K Lin_Arith.simproc}
(* setup *)
--- a/src/HOL/Library/Old_SMT/old_z3_proof_tools.ML Thu Apr 07 22:09:23 2016 +0200
+++ b/src/HOL/Library/Old_SMT/old_z3_proof_tools.ML Fri Apr 08 20:15:20 2016 +0200
@@ -345,13 +345,13 @@
addsimprocs [
Simplifier.make_simproc @{context} "fast_int_arith"
{lhss = [@{term "(m::int) < n"}, @{term "(m::int) \<le> n"}, @{term "(m::int) = n"}],
- proc = K Lin_Arith.simproc, identifier = []},
+ proc = K Lin_Arith.simproc},
Simplifier.make_simproc @{context} "antisym_le"
{lhss = [@{term "(x::'a::order) \<le> y"}],
- proc = K prove_antisym_le, identifier = []},
+ proc = K prove_antisym_le},
Simplifier.make_simproc @{context} "antisym_less"
{lhss = [@{term "\<not> (x::'a::linorder) < y"}],
- proc = K prove_antisym_less, identifier = []}])
+ proc = K prove_antisym_less}])
structure Simpset = Generic_Data
(
--- a/src/HOL/Nominal/nominal_datatype.ML Thu Apr 07 22:09:23 2016 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Fri Apr 08 20:15:20 2016 +0200
@@ -122,7 +122,7 @@
val perm_simproc =
Simplifier.make_simproc @{context} "perm_simp"
- {lhss = [@{term "pi1 \<bullet> (pi2 \<bullet> x)"}], proc = K perm_simproc', identifier = []};
+ {lhss = [@{term "pi1 \<bullet> (pi2 \<bullet> x)"}], proc = K perm_simproc'};
fun projections ctxt rule =
Project_Rule.projections ctxt rule
--- a/src/HOL/Nominal/nominal_inductive.ML Thu Apr 07 22:09:23 2016 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML Fri Apr 08 20:15:20 2016 +0200
@@ -47,8 +47,7 @@
Const (@{const_name Nominal.perm}, _) $ _ $ t =>
if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t))
then SOME perm_bool else NONE
- | _ => NONE),
- identifier = []};
+ | _ => NONE)};
fun transp ([] :: _) = []
| transp xs = map hd xs :: transp (map tl xs);
--- a/src/HOL/Nominal/nominal_inductive2.ML Thu Apr 07 22:09:23 2016 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML Fri Apr 08 20:15:20 2016 +0200
@@ -51,8 +51,7 @@
Const (@{const_name Nominal.perm}, _) $ _ $ t =>
if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t))
then SOME perm_bool else NONE
- | _ => NONE),
- identifier = []};
+ | _ => NONE)};
fun transp ([] :: _) = []
| transp xs = map hd xs :: transp (map tl xs);
--- a/src/HOL/Nominal/nominal_permeq.ML Thu Apr 07 22:09:23 2016 +0200
+++ b/src/HOL/Nominal/nominal_permeq.ML Fri Apr 08 20:15:20 2016 +0200
@@ -114,7 +114,7 @@
val perm_simproc_app =
Simplifier.make_simproc @{context} "perm_simproc_app"
- {lhss = [@{term "Nominal.perm pi x"}], proc = K perm_simproc_app', identifier = []}
+ {lhss = [@{term "Nominal.perm pi x"}], proc = K perm_simproc_app'}
(* a simproc that deals with permutation instances in front of functions *)
fun perm_simproc_fun' ctxt ct =
@@ -136,7 +136,7 @@
val perm_simproc_fun =
Simplifier.make_simproc @{context} "perm_simproc_fun"
- {lhss = [@{term "Nominal.perm pi x"}], proc = K perm_simproc_fun', identifier = []}
+ {lhss = [@{term "Nominal.perm pi x"}], proc = K perm_simproc_fun'}
(* function for simplyfying permutations *)
(* stac contains the simplifiation tactic that is *)
@@ -219,7 +219,7 @@
val perm_compose_simproc =
Simplifier.make_simproc @{context} "perm_compose"
{lhss = [@{term "Nominal.perm pi1 (Nominal.perm pi2 t)"}],
- proc = K perm_compose_simproc', identifier = []}
+ proc = K perm_compose_simproc'}
fun perm_compose_tac ctxt i =
("analysing permutation compositions on the lhs",
--- a/src/HOL/Product_Type.thy Thu Apr 07 22:09:23 2016 +0200
+++ b/src/HOL/Product_Type.thy Fri Apr 08 20:15:20 2016 +0200
@@ -1327,8 +1327,7 @@
Code_Preproc.map_pre (fn ctxt => ctxt addsimprocs
[Simplifier.make_simproc @{context} "set comprehension"
{lhss = [@{term "Collect P"}],
- proc = K Set_Comprehension_Pointfree.code_simproc,
- identifier = []}])
+ proc = K Set_Comprehension_Pointfree.code_simproc}])
\<close>
--- a/src/HOL/Statespace/distinct_tree_prover.ML Thu Apr 07 22:09:23 2016 +0200
+++ b/src/HOL/Statespace/distinct_tree_prover.ML Fri Apr 08 20:15:20 2016 +0200
@@ -360,8 +360,7 @@
Const (@{const_name HOL.eq}, _) $ x $ y =>
Option.map (fn neq => @{thm neq_to_eq_False} OF [neq])
(get_fst_success (neq_x_y ctxt x y) names)
- | _ => NONE),
- identifier = []};
+ | _ => NONE)};
end;
--- a/src/HOL/Statespace/state_fun.ML Thu Apr 07 22:09:23 2016 +0200
+++ b/src/HOL/Statespace/state_fun.ML Fri Apr 08 20:15:20 2016 +0200
@@ -72,8 +72,7 @@
else SOME (conj_cong OF [P_P', Q_Q'])
end
end
- | _ => NONE),
- identifier = []};
+ | _ => NONE)};
fun string_eq_simp_tac ctxt =
simp_tac (put_simpset HOL_basic_ss ctxt
@@ -154,8 +153,7 @@
else SOME thm
end
handle Option.Option => NONE)
- | _ => NONE),
- identifier = []};
+ | _ => NONE)};
local
@@ -260,8 +258,7 @@
in SOME (Thm.transitive eq1 eq2) end
| _ => NONE)
end
- | _ => NONE),
- identifier = []};
+ | _ => NONE)};
end;
@@ -326,8 +323,7 @@
val thm' = if swap then swap_ex_eq OF [thm] else thm
in SOME thm' end handle TERM _ => NONE)
| _ => NONE)
- end handle Option.Option => NONE,
- identifier = []};
+ end handle Option.Option => NONE};
end;
--- a/src/HOL/Statespace/state_space.ML Thu Apr 07 22:09:23 2016 +0200
+++ b/src/HOL/Statespace/state_space.ML Fri Apr 08 20:15:20 2016 +0200
@@ -218,8 +218,7 @@
Const (@{const_name HOL.eq},_) $ (x as Free _) $ (y as Free _) =>
Option.map (fn neq => DistinctTreeProver.neq_to_eq_False OF [neq])
(neq_x_y ctxt x y)
- | _ => NONE),
- identifier = []};
+ | _ => NONE)};
fun interprete_parent name dist_thm_name parent_expr thy =
let
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML Thu Apr 07 22:09:23 2016 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Fri Apr 08 20:15:20 2016 +0200
@@ -150,8 +150,7 @@
val regularize_simproc =
Simplifier.make_simproc @{context} "regularize"
{lhss = [@{term "Ball (Respects (R1 ===> R2)) P"}, @{term "Bex (Respects (R1 ===> R2)) P"}],
- proc = K ball_bex_range_simproc,
- identifier = []};
+ proc = K ball_bex_range_simproc};
fun regularize_tac ctxt =
let
--- a/src/HOL/Tools/SMT/smt_real.ML Thu Apr 07 22:09:23 2016 +0200
+++ b/src/HOL/Tools/SMT/smt_real.ML Fri Apr 08 20:15:20 2016 +0200
@@ -101,7 +101,7 @@
val real_linarith_proc =
Simplifier.make_simproc @{context} "fast_real_arith"
{lhss = [@{term "(m::real) < n"}, @{term "(m::real) \<le> n"}, @{term "(m::real) = n"}],
- proc = K Lin_Arith.simproc, identifier = []}
+ proc = K Lin_Arith.simproc}
(* setup *)
--- a/src/HOL/Tools/SMT/z3_replay_util.ML Thu Apr 07 22:09:23 2016 +0200
+++ b/src/HOL/Tools/SMT/z3_replay_util.ML Fri Apr 08 20:15:20 2016 +0200
@@ -126,13 +126,13 @@
addsimprocs [@{simproc numeral_divmod},
Simplifier.make_simproc @{context} "fast_int_arith"
{lhss = [@{term "(m::int) < n"}, @{term "(m::int) \<le> n"}, @{term "(m::int) = n"}],
- proc = K Lin_Arith.simproc, identifier = []},
+ proc = K Lin_Arith.simproc},
Simplifier.make_simproc @{context} "antisym_le"
{lhss = [@{term "(x::'a::order) \<le> y"}],
- proc = K prove_antisym_le, identifier = []},
+ proc = K prove_antisym_le},
Simplifier.make_simproc @{context} "antisym_less"
{lhss = [@{term "\<not> (x::'a::linorder) < y"}],
- proc = K prove_antisym_less, identifier = []}])
+ proc = K prove_antisym_less}])
structure Simpset = Generic_Data
(
--- a/src/HOL/Tools/groebner.ML Thu Apr 07 22:09:23 2016 +0200
+++ b/src/HOL/Tools/groebner.ML Fri Apr 08 20:15:20 2016 +0200
@@ -787,7 +787,7 @@
in
Simplifier.cert_simproc (Thm.theory_of_thm idl_sub) "poly_eq_simproc"
{lhss = [Thm.term_of (Thm.lhs_of idl_sub)],
- proc = fn _ => fn _ => proc, identifier = []}
+ proc = fn _ => fn _ => proc}
end;
val poly_eq_ss =
--- a/src/HOL/Tools/inductive_set.ML Thu Apr 07 22:09:23 2016 +0200
+++ b/src/HOL/Tools/inductive_set.ML Fri Apr 08 20:15:20 2016 +0200
@@ -98,8 +98,7 @@
end
else NONE
| _ => NONE)
- end,
- identifier = []};
+ end};
(* only eta contract terms occurring as arguments of functions satisfying p *)
fun eta_contract p =
@@ -319,8 +318,7 @@
{lhss = [anyt],
proc = fn _ => fn ctxt => fn ct =>
lookup_rule (Proof_Context.theory_of ctxt)
- (Thm.prop_of #> Logic.dest_equals) rules' (Thm.term_of ct),
- identifier = []}
+ (Thm.prop_of #> Logic.dest_equals) rules' (Thm.term_of ct)}
end;
fun to_pred_proc thy rules t =
--- a/src/HOL/Tools/int_arith.ML Thu Apr 07 22:09:23 2016 +0200
+++ b/src/HOL/Tools/int_arith.ML Fri Apr 08 20:15:20 2016 +0200
@@ -29,8 +29,7 @@
let val T = Thm.ctyp_of_cterm ct in
if Thm.typ_of T = @{typ int} then NONE
else SOME (Thm.instantiate' [SOME T] [] zeroth)
- end,
- identifier = []};
+ end};
val oneth = Thm.symmetric (mk_meta_eq @{thm of_int_1});
@@ -41,8 +40,7 @@
let val T = Thm.ctyp_of_cterm ct in
if Thm.typ_of T = @{typ int} then NONE
else SOME (Thm.instantiate' [SOME T] [] oneth)
- end,
- identifier = []};
+ end};
fun check (Const (@{const_name Groups.one}, @{typ int})) = false
| check (Const (@{const_name Groups.one}, _)) = true
@@ -71,8 +69,7 @@
proc = fn _ => fn ctxt => fn ct =>
if check (Thm.term_of ct)
then SOME (Simplifier.rewrite (put_simpset conv_ss ctxt) ct)
- else NONE,
- identifier = []};
+ else NONE};
fun number_of ctxt T n =
--- a/src/HOL/Tools/numeral_simprocs.ML Thu Apr 07 22:09:23 2016 +0200
+++ b/src/HOL/Tools/numeral_simprocs.ML Fri Apr 08 20:15:20 2016 +0200
@@ -451,16 +451,14 @@
@{term "((numeral v)::'a::field) / (- numeral w)"},
@{term "((- numeral v)::'a::field) / (numeral w)"},
@{term "((- numeral v)::'a::field) / (- numeral w)"}],
- proc = K DivideCancelNumeralFactor.proc,
- identifier = []}
+ proc = K DivideCancelNumeralFactor.proc}
val field_cancel_numeral_factors =
[Simplifier.make_simproc @{context} "field_eq_cancel_numeral_factor"
{lhss =
[@{term "(l::'a::field) * m = n"},
@{term "(l::'a::field) = m * n"}],
- proc = K EqCancelNumeralFactor.proc,
- identifier = []},
+ proc = K EqCancelNumeralFactor.proc},
field_divide_cancel_numeral_factor]
@@ -693,12 +691,12 @@
val add_frac_frac_simproc =
Simplifier.make_simproc @{context} "add_frac_frac_simproc"
{lhss = [@{term "(x::'a::field) / y + (w::'a::field) / z"}],
- proc = K proc, identifier = []}
+ proc = K proc}
val add_frac_num_simproc =
Simplifier.make_simproc @{context} "add_frac_num_simproc"
{lhss = [@{term "(x::'a::field) / y + z"}, @{term "z + (x::'a::field) / y"}],
- proc = K proc2, identifier = []}
+ proc = K proc2}
val ord_frac_simproc =
Simplifier.make_simproc @{context} "ord_frac_simproc"
@@ -709,7 +707,7 @@
@{term "c \<le> (a::'a::{field,ord}) / b"},
@{term "c = (a::'a::{field,ord}) / b"},
@{term "(a::'a::{field, ord}) / b = c"}],
- proc = K proc3, identifier = []}
+ proc = K proc3}
val ths =
[@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"},
--- a/src/HOL/Tools/record.ML Thu Apr 07 22:09:23 2016 +0200
+++ b/src/HOL/Tools/record.ML Fri Apr 08 20:15:20 2016 +0200
@@ -1116,8 +1116,7 @@
end
else NONE
| _ => NONE)
- end,
- identifier = []};
+ end};
fun get_upd_acc_cong_thm upd acc thy ss =
let
@@ -1250,8 +1249,7 @@
(prove_unfold_defs thy noops' [simproc]
(Logic.list_all (vars, Logic.mk_equals (lhs, rhs))))
else NONE
- end,
- identifier = []};
+ end};
end;
@@ -1282,8 +1280,7 @@
(case get_equalities (Proof_Context.theory_of ctxt) name of
NONE => NONE
| SOME thm => SOME (thm RS @{thm Eq_TrueI})))
- | _ => NONE),
- identifier = []};
+ | _ => NONE)};
(* split_simproc *)
@@ -1320,8 +1317,7 @@
else NONE
end)
else NONE
- | _ => NONE),
- identifier = []};
+ | _ => NONE)};
val ex_sel_eq_simproc =
Simplifier.make_simproc @{context} "ex_sel_eq"
@@ -1362,8 +1358,7 @@
addsimps @{thms simp_thms} addsimprocs [split_simproc (K ~1)]) 1))
end handle TERM _ => NONE)
| _ => NONE)
- end,
- identifier = []};
+ end};
(* split_simp_tac *)
--- a/src/HOL/Word/WordBitwise.thy Thu Apr 07 22:09:23 2016 +0200
+++ b/src/HOL/Word/WordBitwise.thy Fri Apr 08 20:15:20 2016 +0200
@@ -525,7 +525,7 @@
val expand_upt_simproc =
Simplifier.make_simproc @{context} "expand_upt"
- {lhss = [@{term "upt x y"}], proc = K upt_conv, identifier = []};
+ {lhss = [@{term "upt x y"}], proc = K upt_conv};
fun word_len_simproc_fn ctxt ct =
case Thm.term_of ct of
@@ -541,7 +541,7 @@
val word_len_simproc =
Simplifier.make_simproc @{context} "word_len"
- {lhss = [@{term "len_of x"}], proc = K word_len_simproc_fn, identifier = []};
+ {lhss = [@{term "len_of x"}], proc = K word_len_simproc_fn};
(* convert 5 or nat 5 to Suc 4 when n_sucs = 1, Suc (Suc 4) when n_sucs = 2,
or just 5 (discarding nat) when n_sucs = 0 *)
@@ -568,7 +568,7 @@
fun nat_get_Suc_simproc n_sucs ts =
Simplifier.make_simproc @{context} "nat_get_Suc"
{lhss = map (fn t => t $ @{term "n :: nat"}) ts,
- proc = K (nat_get_Suc_simproc_fn n_sucs), identifier = []};
+ proc = K (nat_get_Suc_simproc_fn n_sucs)};
val no_split_ss =
simpset_of (put_simpset HOL_ss @{context}
--- a/src/Pure/Isar/isar_cmd.ML Thu Apr 07 22:09:23 2016 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Fri Apr 08 20:15:20 2016 +0200
@@ -18,7 +18,7 @@
val oracle: bstring * Position.range -> Input.source -> theory -> theory
val declaration: {syntax: bool, pervasive: bool} -> Input.source -> local_theory -> local_theory
val simproc_setup: string * Position.T -> string list -> Input.source ->
- string list -> local_theory -> local_theory
+ local_theory -> local_theory
val qed: Method.text_range option -> Toplevel.transition -> Toplevel.transition
val terminal_proof: Method.text_range * Method.text_range option ->
Toplevel.transition -> Toplevel.transition
@@ -151,14 +151,13 @@
(* simprocs *)
-fun simproc_setup name lhss source identifier =
+fun simproc_setup name lhss source =
ML_Lex.read_source false source
|> ML_Context.expression (Input.range_of source) "proc"
"Morphism.morphism -> Proof.context -> cterm -> thm option"
("Context.map_proof (Simplifier.define_simproc_cmd " ^
ML_Syntax.atomic (ML_Syntax.make_binding name) ^
- "{lhss = " ^ ML_Syntax.print_strings lhss ^ ", proc = proc, \
- \identifier = Library.maps ML_Context.thms " ^ ML_Syntax.print_strings identifier ^ "})")
+ "{lhss = " ^ ML_Syntax.print_strings lhss ^ ", proc = proc})")
|> Context.proof_map;
--- a/src/Pure/ML/ml_context.ML Thu Apr 07 22:09:23 2016 +0200
+++ b/src/Pure/ML/ml_context.ML Fri Apr 08 20:15:20 2016 +0200
@@ -6,9 +6,6 @@
signature ML_CONTEXT =
sig
- val thm: xstring -> thm
- val thms: xstring -> thm list
- val exec: (unit -> unit) -> Context.generic -> Context.generic
val check_antiquotation: Proof.context -> xstring * Position.T -> string
val struct_name: Proof.context -> string
val variant: string -> Proof.context -> string * Proof.context
@@ -23,6 +20,7 @@
val eval_in: Proof.context option -> ML_Compiler.flags -> Position.T ->
ML_Lex.token Antiquote.antiquote list -> unit
val eval_source_in: Proof.context option -> ML_Compiler.flags -> Input.source -> unit
+ val exec: (unit -> unit) -> Context.generic -> Context.generic
val expression: Position.range -> string -> string -> string ->
ML_Lex.token Antiquote.antiquote list -> Context.generic -> Context.generic
end
@@ -30,19 +28,6 @@
structure ML_Context: ML_CONTEXT =
struct
-(** implicit ML context **)
-
-fun thm name = Proof_Context.get_thm (Context.the_local_context ()) name;
-fun thms name = Proof_Context.get_thms (Context.the_local_context ()) name;
-
-fun exec (e: unit -> unit) context =
- (case Context.setmp_generic_context (SOME context)
- (fn () => (e (); Context.get_generic_context ())) () of
- SOME context' => context'
- | NONE => error "Missing context after execution");
-
-
-
(** ML antiquotations **)
(* names for generated environment *)
@@ -220,6 +205,12 @@
Context.setmp_generic_context (Option.map Context.Proof ctxt)
(fn () => eval_source flags source) ();
+fun exec (e: unit -> unit) context =
+ (case Context.setmp_generic_context (SOME context)
+ (fn () => (e (); Context.get_generic_context ())) () of
+ SOME context' => context'
+ | NONE => error "Missing context after execution");
+
fun expression range name constraint body ants =
exec (fn () =>
eval ML_Compiler.flags (#1 range)
--- a/src/Pure/Pure.thy Thu Apr 07 22:09:23 2016 +0200
+++ b/src/Pure/Pure.thy Fri Apr 08 20:15:20 2016 +0200
@@ -9,7 +9,7 @@
"!!" "!" "+" "--" ":" ";" "<" "<=" "=" "=>" "?" "[" "\<comment>" "\<equiv>"
"\<leftharpoondown>" "\<rightharpoonup>" "\<rightleftharpoons>"
"\<subseteq>" "]" "assumes" "attach" "binder" "constrains"
- "defines" "rewrites" "fixes" "for" "identifier" "if" "in" "includes" "infix"
+ "defines" "rewrites" "fixes" "for" "if" "in" "includes" "infix"
"infixl" "infixr" "is" "notes" "obtains" "open" "output"
"overloaded" "pervasive" "premises" "private" "qualified" "rewrites"
"shows" "structure" "unchecked" "where" "when" "|"
@@ -210,8 +210,7 @@
Outer_Syntax.local_theory @{command_keyword simproc_setup} "define simproc in ML"
(Parse.position Parse.name --
(@{keyword "("} |-- Parse.enum1 "|" Parse.term --| @{keyword ")"} --| @{keyword "="}) --
- Parse.ML_source -- Scan.optional (@{keyword "identifier"} |-- Scan.repeat1 Parse.xname) []
- >> (fn (((a, b), c), d) => Isar_Cmd.simproc_setup a b c d));
+ Parse.ML_source >> (fn ((a, b), c) => Isar_Cmd.simproc_setup a b c));
in end\<close>
--- a/src/Pure/raw_simplifier.ML Thu Apr 07 22:09:23 2016 +0200
+++ b/src/Pure/raw_simplifier.ML Fri Apr 08 20:15:20 2016 +0200
@@ -36,8 +36,7 @@
type simproc
val eq_simproc: simproc * simproc -> bool
val cert_simproc: theory -> string ->
- {lhss: term list, proc: morphism -> Proof.context -> cterm -> thm option, identifier: thm list}
- -> simproc
+ {lhss: term list, proc: morphism -> Proof.context -> cterm -> thm option} -> simproc
val transform_simproc: morphism -> simproc -> simproc
val simpset_of: Proof.context -> simpset
val put_simpset: simpset -> Proof.context -> Proof.context
@@ -220,12 +219,9 @@
{name: string,
lhs: term,
proc: Proof.context -> cterm -> thm option,
- id: stamp * thm list};
+ stamp: stamp};
-fun eq_procid ((s1: stamp, ths1: thm list), (s2, ths2)) =
- s1 = s2 andalso eq_list Thm.eq_thm (ths1, ths2);
-
-fun eq_proc (Proc {id = id1, ...}, Proc {id = id2, ...}) = eq_procid (id1, id2);
+fun eq_proc (Proc {stamp = stamp1, ...}, Proc {stamp = stamp2, ...}) = stamp1 = stamp2;
(* solvers *)
@@ -298,8 +294,8 @@
{simps = Net.entries rules
|> map (fn {name, thm, ...} => (name, thm)),
procs = Net.entries procs
- |> map (fn Proc {name, lhs, id, ...} => ((name, lhs), id))
- |> partition_eq (eq_snd eq_procid)
+ |> map (fn Proc {name, lhs, stamp, ...} => ((name, lhs), stamp))
+ |> partition_eq (eq_snd op =)
|> map (fn ps => (fst (fst (hd ps)), map (snd o fst) ps)),
congs = #1 congs,
weak_congs = #2 congs,
@@ -667,20 +663,19 @@
{name: string,
lhss: term list,
proc: morphism -> Proof.context -> cterm -> thm option,
- id: stamp * thm list};
+ stamp: stamp};
-fun eq_simproc (Simproc {id = id1, ...}, Simproc {id = id2, ...}) = eq_procid (id1, id2);
+fun eq_simproc (Simproc {stamp = stamp1, ...}, Simproc {stamp = stamp2, ...}) = stamp1 = stamp2;
-fun cert_simproc thy name {lhss, proc, identifier} =
- Simproc {name = name, lhss = map (Sign.cert_term thy) lhss, proc = proc,
- id = (stamp (), map Thm.trim_context identifier)};
+fun cert_simproc thy name {lhss, proc} =
+ Simproc {name = name, lhss = map (Sign.cert_term thy) lhss, proc = proc, stamp = stamp ()};
-fun transform_simproc phi (Simproc {name, lhss, proc, id = (s, ths)}) =
+fun transform_simproc phi (Simproc {name, lhss, proc, stamp}) =
Simproc
{name = name,
lhss = map (Morphism.term phi) lhss,
proc = Morphism.transform phi proc,
- id = (s, Morphism.fact phi ths)};
+ stamp = stamp};
local
@@ -704,8 +699,8 @@
(cond_warning ctxt (fn () => "Simplification procedure " ^ quote name ^ " not in simpset");
ctxt);
-fun prep_procs (Simproc {name, lhss, proc, id}) =
- lhss |> map (fn lhs => Proc {name = name, lhs = lhs, proc = Morphism.form proc, id = id});
+fun prep_procs (Simproc {name, lhss, proc, stamp}) =
+ lhss |> map (fn lhs => Proc {name = name, lhs = lhs, proc = Morphism.form proc, stamp = stamp});
in
--- a/src/Pure/simplifier.ML Thu Apr 07 22:09:23 2016 +0200
+++ b/src/Pure/simplifier.ML Fri Apr 08 20:15:20 2016 +0200
@@ -36,8 +36,7 @@
val cong_del: attribute
val check_simproc: Proof.context -> xstring * Position.T -> string
val the_simproc: Proof.context -> string -> simproc
- type 'a simproc_spec =
- {lhss: 'a list, proc: morphism -> Proof.context -> cterm -> thm option, identifier: thm list}
+ type 'a simproc_spec = {lhss: 'a list, proc: morphism -> Proof.context -> cterm -> thm option}
val make_simproc: Proof.context -> string -> term simproc_spec -> simproc
val define_simproc: binding -> term simproc_spec -> local_theory -> local_theory
val define_simproc_cmd: binding -> string simproc_spec -> local_theory -> local_theory
@@ -117,25 +116,22 @@
(* define simprocs *)
-type 'a simproc_spec =
- {lhss: 'a list, proc: morphism -> Proof.context -> cterm -> thm option, identifier: thm list};
+type 'a simproc_spec = {lhss: 'a list, proc: morphism -> Proof.context -> cterm -> thm option};
-fun make_simproc ctxt name {lhss, proc, identifier} =
+fun make_simproc ctxt name {lhss, proc} =
let
val ctxt' = fold Variable.auto_fixes lhss ctxt;
val lhss' = Variable.export_terms ctxt' ctxt lhss;
in
- cert_simproc (Proof_Context.theory_of ctxt) name
- {lhss = lhss', proc = proc, identifier = identifier}
+ cert_simproc (Proof_Context.theory_of ctxt) name {lhss = lhss', proc = proc}
end;
local
-fun def_simproc prep b {lhss, proc, identifier} lthy =
+fun def_simproc prep b {lhss, proc} lthy =
let
val simproc =
- make_simproc lthy (Local_Theory.full_name lthy b)
- {lhss = prep lthy lhss, proc = proc, identifier = identifier};
+ make_simproc lthy (Local_Theory.full_name lthy b) {lhss = prep lthy lhss, proc = proc};
in
lthy |> Local_Theory.declaration {syntax = false, pervasive = false} (fn phi => fn context =>
let
--- a/src/Tools/induct.ML Thu Apr 07 22:09:23 2016 +0200
+++ b/src/Tools/induct.ML Fri Apr 08 20:15:20 2016 +0200
@@ -173,8 +173,7 @@
val rearrange_eqs_simproc =
Simplifier.make_simproc @{context} "rearrange_eqs"
{lhss = [@{term "Pure.all(t)"}],
- proc = fn _ => fn ctxt => fn ct => mk_swap_rrule ctxt ct,
- identifier = []};
+ proc = fn _ => fn ctxt => fn ct => mk_swap_rrule ctxt ct};
(* rotate k premises to the left by j, skipping over first j premises *)
--- a/src/ZF/Datatype_ZF.thy Thu Apr 07 22:09:23 2016 +0200
+++ b/src/ZF/Datatype_ZF.thy Fri Apr 08 20:15:20 2016 +0200
@@ -107,7 +107,7 @@
val conv =
Simplifier.make_simproc @{context} "data_free"
- {lhss = [@{term "(x::i) = y"}], proc = K proc, identifier = []};
+ {lhss = [@{term "(x::i) = y"}], proc = K proc};
end;
\<close>
--- a/src/ZF/arith_data.ML Thu Apr 07 22:09:23 2016 +0200
+++ b/src/ZF/arith_data.ML Fri Apr 08 20:15:20 2016 +0200
@@ -204,19 +204,19 @@
[@{term "l #+ m = n"}, @{term "l = m #+ n"},
@{term "l #* m = n"}, @{term "l = m #* n"},
@{term "succ(m) = n"}, @{term "m = succ(n)"}],
- proc = K EqCancelNumerals.proc, identifier = []},
+ proc = K EqCancelNumerals.proc},
Simplifier.make_simproc @{context} "natless_cancel_numerals"
{lhss =
[@{term "l #+ m < n"}, @{term "l < m #+ n"},
@{term "l #* m < n"}, @{term "l < m #* n"},
@{term "succ(m) < n"}, @{term "m < succ(n)"}],
- proc = K LessCancelNumerals.proc, identifier = []},
+ proc = K LessCancelNumerals.proc},
Simplifier.make_simproc @{context} "natdiff_cancel_numerals"
{lhss =
[@{term "(l #+ m) #- n"}, @{term "l #- (m #+ n)"},
@{term "(l #* m) #- n"}, @{term "l #- (m #* n)"},
@{term "succ(m) #- n"}, @{term "m #- succ(n)"}],
- proc = K DiffCancelNumerals.proc, identifier = []}];
+ proc = K DiffCancelNumerals.proc}];
end;
--- a/src/ZF/int_arith.ML Thu Apr 07 22:09:23 2016 +0200
+++ b/src/ZF/int_arith.ML Fri Apr 08 20:15:20 2016 +0200
@@ -212,19 +212,19 @@
[@{term "l $+ m = n"}, @{term "l = m $+ n"},
@{term "l $- m = n"}, @{term "l = m $- n"},
@{term "l $* m = n"}, @{term "l = m $* n"}],
- proc = K EqCancelNumerals.proc, identifier = []},
+ proc = K EqCancelNumerals.proc},
Simplifier.make_simproc @{context} "intless_cancel_numerals"
{lhss =
[@{term "l $+ m $< n"}, @{term "l $< m $+ n"},
@{term "l $- m $< n"}, @{term "l $< m $- n"},
@{term "l $* m $< n"}, @{term "l $< m $* n"}],
- proc = K LessCancelNumerals.proc, identifier = []},
+ proc = K LessCancelNumerals.proc},
Simplifier.make_simproc @{context} "intle_cancel_numerals"
{lhss =
[@{term "l $+ m $\<le> n"}, @{term "l $\<le> m $+ n"},
@{term "l $- m $\<le> n"}, @{term "l $\<le> m $- n"},
@{term "l $* m $\<le> n"}, @{term "l $\<le> m $* n"}],
- proc = K LeCancelNumerals.proc, identifier = []}];
+ proc = K LeCancelNumerals.proc}];
(*version without the hyps argument*)
@@ -269,7 +269,7 @@
val combine_numerals =
Simplifier.make_simproc @{context} "int_combine_numerals"
{lhss = [@{term "i $+ j"}, @{term "i $- j"}],
- proc = K CombineNumerals.proc, identifier = []};
+ proc = K CombineNumerals.proc};
@@ -315,7 +315,7 @@
val combine_numerals_prod =
Simplifier.make_simproc @{context} "int_combine_numerals_prod"
- {lhss = [@{term "i $* j"}], proc = K CombineNumeralsProd.proc, identifier = []};
+ {lhss = [@{term "i $* j"}], proc = K CombineNumeralsProd.proc};
end;