rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
--- a/src/Doc/Eisbach/Manual.thy Tue Dec 15 16:57:10 2015 +0100
+++ b/src/Doc/Eisbach/Manual.thy Wed Dec 16 16:31:36 2015 +0100
@@ -931,7 +931,7 @@
attribute_setup get_split_rule =
\<open>Args.term >> (fn t =>
- Thm.rule_attribute (fn context => fn _ =>
+ Thm.rule_attribute [] (fn context => fn _ =>
(case get_split_rule (Context.proof_of context) t of
SOME thm => thm
| NONE => Drule.dummy_thm)))\<close>
--- a/src/Doc/Implementation/Isar.thy Tue Dec 15 16:57:10 2015 +0100
+++ b/src/Doc/Implementation/Isar.thy Wed Dec 16 16:31:36 2015 +0100
@@ -512,7 +512,8 @@
text %mlref \<open>
\begin{mldecls}
@{index_ML_type attribute} \\
- @{index_ML Thm.rule_attribute: "(Context.generic -> thm -> thm) -> attribute"} \\
+ @{index_ML Thm.rule_attribute: "thm list ->
+ (Context.generic -> thm -> thm) -> attribute"} \\
@{index_ML Thm.declaration_attribute: "
(thm -> Context.generic -> Context.generic) -> attribute"} \\
@{index_ML Attrib.setup: "binding -> attribute context_parser ->
@@ -522,12 +523,19 @@
\<^descr> Type @{ML_type attribute} represents attributes as concrete
type alias.
- \<^descr> @{ML Thm.rule_attribute}~\<open>(fn context => rule)\<close> wraps
- a context-dependent rule (mapping on @{ML_type thm}) as attribute.
+ \<^descr> @{ML Thm.rule_attribute}~\<open>thms (fn context => rule)\<close> wraps a
+ context-dependent rule (mapping on @{ML_type thm}) as attribute.
+
+ The \<open>thms\<close> are additional parameters: when forming an abstract closure, the
+ system may provide dummy facts that are propagated according to strict
+ evaluation discipline. In that case, \<open>rule\<close> is bypassed.
- \<^descr> @{ML Thm.declaration_attribute}~\<open>(fn thm => decl)\<close>
- wraps a theorem-dependent declaration (mapping on @{ML_type
- Context.generic}) as attribute.
+ \<^descr> @{ML Thm.declaration_attribute}~\<open>(fn thm => decl)\<close> wraps a
+ theorem-dependent declaration (mapping on @{ML_type Context.generic}) as
+ attribute.
+
+ When forming an abstract closure, the system may provide a dummy fact as
+ \<open>thm\<close>. In that case, \<open>decl\<close> is bypassed.
\<^descr> @{ML Attrib.setup}~\<open>name parser description\<close> provides
the functionality of the Isar command @{command attribute_setup} as
--- a/src/Doc/Isar_Ref/Spec.thy Tue Dec 15 16:57:10 2015 +0100
+++ b/src/Doc/Isar_Ref/Spec.thy Wed Dec 16 16:31:36 2015 +0100
@@ -1066,7 +1066,7 @@
(*<*)experiment begin(*>*)
attribute_setup my_rule =
\<open>Attrib.thms >> (fn ths =>
- Thm.rule_attribute
+ Thm.rule_attribute ths
(fn context: Context.generic => fn th: thm =>
let val th' = th OF ths
in th' end))\<close>
--- a/src/HOL/Eisbach/Eisbach.thy Tue Dec 15 16:57:10 2015 +0100
+++ b/src/HOL/Eisbach/Eisbach.thy Wed Dec 16 16:31:36 2015 +0100
@@ -21,14 +21,6 @@
ML_file "match_method.ML"
ML_file "eisbach_antiquotations.ML"
-(* FIXME reform Isabelle/Pure attributes to make this work by default *)
-setup \<open>
- fold (Method_Closure.wrap_attribute {handle_all_errs = true, declaration = true})
- [@{binding intro}, @{binding elim}, @{binding dest}, @{binding simp}] #>
- fold (Method_Closure.wrap_attribute {handle_all_errs = false, declaration = false})
- [@{binding THEN}, @{binding OF}, @{binding rotated}, @{binding simplified}]
-\<close>
-
method solves methods m = (m; fail)
end
--- a/src/HOL/Eisbach/Eisbach_Tools.thy Tue Dec 15 16:57:10 2015 +0100
+++ b/src/HOL/Eisbach/Eisbach_Tools.thy Wed Dec 16 16:31:36 2015 +0100
@@ -76,7 +76,7 @@
in Conjunction.curry_balanced (length conjs) thm end;
\<close>
-attribute_setup uncurry = \<open>Scan.succeed (Thm.rule_attribute (K uncurry_rule))\<close>
-attribute_setup curry = \<open>Scan.succeed (Thm.rule_attribute (K curry_rule))\<close>
+attribute_setup uncurry = \<open>Scan.succeed (Thm.rule_attribute [] (K uncurry_rule))\<close>
+attribute_setup curry = \<open>Scan.succeed (Thm.rule_attribute [] (K curry_rule))\<close>
end
--- a/src/HOL/Eisbach/eisbach_rule_insts.ML Tue Dec 15 16:57:10 2015 +0100
+++ b/src/HOL/Eisbach/eisbach_rule_insts.ML Wed Dec 16 16:31:36 2015 +0100
@@ -228,8 +228,11 @@
(Attrib.setup @{binding "where"}
(Scan.lift
(Parse.and_list1 (Args.var -- (Args.$$$ "=" |-- Parse_Tools.name_term)) -- Parse.for_fixes)
- >> (fn args => let val args' = read_where_insts args in Thm.rule_attribute (fn context =>
- read_instantiate_closed (Context.proof_of context) args') end))
+ >> (fn args =>
+ let val args' = read_where_insts args in
+ Thm.mixed_attribute (fn (context, thm) =>
+ (context, read_instantiate_closed (Context.proof_of context) args' thm))
+ end))
"named instantiation of theorem");
val _ =
@@ -244,10 +247,12 @@
let
val read_insts = read_of_insts (not unchecked) context args;
in
- Thm.rule_attribute (fn context => fn thm =>
- if Thm.is_free_dummy thm andalso unchecked
- then Drule.free_dummy_thm
- else read_instantiate_closed (Context.proof_of context) (read_insts thm) thm)
+ Thm.mixed_attribute (fn (context, thm) =>
+ let val thm' =
+ if Thm.is_free_dummy thm andalso unchecked
+ then Drule.free_dummy_thm
+ else read_instantiate_closed (Context.proof_of context) (read_insts thm) thm
+ in (context, thm') end)
end))
"positional instantiation of theorem");
--- a/src/HOL/Eisbach/method_closure.ML Tue Dec 15 16:57:10 2015 +0100
+++ b/src/HOL/Eisbach/method_closure.ML Wed Dec 16 16:31:36 2015 +0100
@@ -10,8 +10,6 @@
signature METHOD_CLOSURE =
sig
- val wrap_attribute: {handle_all_errs : bool, declaration : bool} ->
- Binding.binding -> theory -> theory
val read: Proof.context -> Token.src -> Method.text
val read_closure: Proof.context -> Token.src -> Method.text * Token.src
val read_closure_input: Proof.context -> Input.source -> Method.text * Token.src
@@ -64,40 +62,6 @@
val put_recursive_method = Local_Data.map o apsnd o K;
-(* free thm *)
-
-fun free_aware_attribute thy {handle_all_errs, declaration} src (context, thm) =
- let
- val src' = map Token.init_assignable src;
- fun apply_att thm = (Attrib.attribute_global thy src') (context, thm);
- val _ =
- if handle_all_errs then (try apply_att Drule.dummy_thm; ())
- else (apply_att Drule.dummy_thm; ()) handle THM _ => () | TERM _ => () | TYPE _ => ();
-
- val src'' = map Token.closure src';
- val thms =
- map_filter Token.get_value (Token.args_of_src src'')
- |> map_filter (fn (Token.Fact (_, f)) => SOME f | _ => NONE)
- |> flat;
- in
- if exists Thm.is_free_dummy (thm :: thms) then
- if declaration then (NONE, NONE)
- else (NONE, SOME Drule.free_dummy_thm)
- else apply_att thm
- end;
-
-fun wrap_attribute args binding thy =
- let
- val name = Binding.name_of binding;
- val name' = Attrib.check_name_generic (Context.Theory thy) (name, Position.none);
- fun get_src src =
- Token.make_src (name', Position.set_range (Token.range_of src)) (Token.args_of_src src);
- in
- Attrib.define_global binding (free_aware_attribute thy args o get_src) "" thy
- |> snd
- end;
-
-
(* read method text *)
fun read ctxt src =
--- a/src/HOL/TLA/Action.thy Tue Dec 15 16:57:10 2015 +0100
+++ b/src/HOL/TLA/Action.thy Wed Dec 16 16:31:36 2015 +0100
@@ -123,11 +123,11 @@
\<close>
attribute_setup action_unlift =
- \<open>Scan.succeed (Thm.rule_attribute (action_unlift o Context.proof_of))\<close>
+ \<open>Scan.succeed (Thm.rule_attribute [] (action_unlift o Context.proof_of))\<close>
attribute_setup action_rewrite =
- \<open>Scan.succeed (Thm.rule_attribute (action_rewrite o Context.proof_of))\<close>
+ \<open>Scan.succeed (Thm.rule_attribute [] (action_rewrite o Context.proof_of))\<close>
attribute_setup action_use =
- \<open>Scan.succeed (Thm.rule_attribute (action_use o Context.proof_of))\<close>
+ \<open>Scan.succeed (Thm.rule_attribute [] (action_use o Context.proof_of))\<close>
(* =========================== square / angle brackets =========================== *)
--- a/src/HOL/TLA/Intensional.thy Tue Dec 15 16:57:10 2015 +0100
+++ b/src/HOL/TLA/Intensional.thy Wed Dec 16 16:31:36 2015 +0100
@@ -256,12 +256,13 @@
\<close>
attribute_setup int_unlift =
- \<open>Scan.succeed (Thm.rule_attribute (int_unlift o Context.proof_of))\<close>
+ \<open>Scan.succeed (Thm.rule_attribute [] (int_unlift o Context.proof_of))\<close>
attribute_setup int_rewrite =
- \<open>Scan.succeed (Thm.rule_attribute (int_rewrite o Context.proof_of))\<close>
-attribute_setup flatten = \<open>Scan.succeed (Thm.rule_attribute (K flatten))\<close>
+ \<open>Scan.succeed (Thm.rule_attribute [] (int_rewrite o Context.proof_of))\<close>
+attribute_setup flatten =
+ \<open>Scan.succeed (Thm.rule_attribute [] (K flatten))\<close>
attribute_setup int_use =
- \<open>Scan.succeed (Thm.rule_attribute (int_use o Context.proof_of))\<close>
+ \<open>Scan.succeed (Thm.rule_attribute [] (int_use o Context.proof_of))\<close>
lemma Not_Rall: "\<turnstile> (\<not>(\<forall>x. F x)) = (\<exists>x. \<not>F x)"
by (simp add: Valid_def)
--- a/src/HOL/TLA/TLA.thy Tue Dec 15 16:57:10 2015 +0100
+++ b/src/HOL/TLA/TLA.thy Wed Dec 16 16:31:36 2015 +0100
@@ -124,13 +124,13 @@
\<close>
attribute_setup temp_unlift =
- \<open>Scan.succeed (Thm.rule_attribute (temp_unlift o Context.proof_of))\<close>
+ \<open>Scan.succeed (Thm.rule_attribute [] (temp_unlift o Context.proof_of))\<close>
attribute_setup temp_rewrite =
- \<open>Scan.succeed (Thm.rule_attribute (temp_rewrite o Context.proof_of))\<close>
+ \<open>Scan.succeed (Thm.rule_attribute [] (temp_rewrite o Context.proof_of))\<close>
attribute_setup temp_use =
- \<open>Scan.succeed (Thm.rule_attribute (temp_use o Context.proof_of))\<close>
+ \<open>Scan.succeed (Thm.rule_attribute [] (temp_use o Context.proof_of))\<close>
attribute_setup try_rewrite =
- \<open>Scan.succeed (Thm.rule_attribute (try_rewrite o Context.proof_of))\<close>
+ \<open>Scan.succeed (Thm.rule_attribute [] (try_rewrite o Context.proof_of))\<close>
(* ------------------------------------------------------------------------- *)
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML Tue Dec 15 16:57:10 2015 +0100
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Wed Dec 16 16:31:36 2015 +0100
@@ -755,7 +755,7 @@
(* lifting as an attribute *)
-val lifted_attrib = Thm.rule_attribute (fn context =>
+val lifted_attrib = Thm.rule_attribute [] (fn context =>
let
val ctxt = Context.proof_of context
val qtys = map #qtyp (Quotient_Info.dest_quotients ctxt)
--- a/src/HOL/Tools/Transfer/transfer.ML Tue Dec 15 16:57:10 2015 +0100
+++ b/src/HOL/Tools/Transfer/transfer.ML Wed Dec 16 16:31:36 2015 +0100
@@ -847,11 +847,11 @@
(* Attributes for transferred rules *)
-fun transferred_attribute thms = Thm.rule_attribute
- (fn context => transferred (Context.proof_of context) thms)
+fun transferred_attribute thms =
+ Thm.rule_attribute thms (fn context => transferred (Context.proof_of context) thms)
-fun untransferred_attribute thms = Thm.rule_attribute
- (fn context => untransferred (Context.proof_of context) thms)
+fun untransferred_attribute thms =
+ Thm.rule_attribute thms (fn context => untransferred (Context.proof_of context) thms)
val transferred_attribute_parser =
Attrib.thms >> transferred_attribute
--- a/src/HOL/Tools/inductive_set.ML Tue Dec 15 16:57:10 2015 +0100
+++ b/src/HOL/Tools/inductive_set.ML Wed Dec 16 16:31:36 2015 +0100
@@ -349,7 +349,7 @@
Rule_Cases.save thm
end;
-val to_pred_att = Thm.rule_attribute o to_pred;
+val to_pred_att = Thm.rule_attribute [] o to_pred;
(**** convert theorem in predicate notation to set notation ****)
@@ -385,7 +385,7 @@
Rule_Cases.save thm
end;
-val to_set_att = Thm.rule_attribute o to_set;
+val to_set_att = Thm.rule_attribute [] o to_set;
(**** definition of inductive sets ****)
--- a/src/HOL/Tools/legacy_transfer.ML Tue Dec 15 16:57:10 2015 +0100
+++ b/src/HOL/Tools/legacy_transfer.ML Wed Dec 16 16:31:36 2015 +0100
@@ -253,7 +253,7 @@
"install transfer data" #>
Attrib.setup @{binding transferred}
(selection -- these (keyword_colon leavingN |-- names)
- >> (fn (selection, leave) => Thm.rule_attribute (fn context =>
+ >> (fn (selection, leave) => Thm.rule_attribute [] (fn context =>
Conjunction.intr_balanced o transfer context selection leave)))
"transfer theorems");
--- a/src/HOL/Tools/split_rule.ML Tue Dec 15 16:57:10 2015 +0100
+++ b/src/HOL/Tools/split_rule.ML Wed Dec 16 16:31:36 2015 +0100
@@ -113,10 +113,10 @@
Theory.setup
(Attrib.setup @{binding split_format}
(Scan.lift (Args.parens (Args.$$$ "complete")
- >> K (Thm.rule_attribute (complete_split_rule o Context.proof_of))))
+ >> K (Thm.rule_attribute [] (complete_split_rule o Context.proof_of))))
"split pair-typed subterms in premises, or function arguments" #>
Attrib.setup @{binding split_rule}
- (Scan.succeed (Thm.rule_attribute (split_rule o Context.proof_of)))
+ (Scan.succeed (Thm.rule_attribute [] (split_rule o Context.proof_of)))
"curries ALL function variables occurring in a rule's conclusion");
end;
--- a/src/HOL/UNITY/Comp/Alloc.thy Tue Dec 15 16:57:10 2015 +0100
+++ b/src/HOL/UNITY/Comp/Alloc.thy Wed Dec 16 16:31:36 2015 +0100
@@ -321,7 +321,7 @@
handle THM _ => th RS (@{thm guarantees_INT_right_iff} RS iffD1))
handle THM _ => th;
in
- Scan.succeed (Thm.rule_attribute (K normalized))
+ Scan.succeed (Thm.rule_attribute [] (K normalized))
end
*}
--- a/src/Provers/classical.ML Tue Dec 15 16:57:10 2015 +0100
+++ b/src/Provers/classical.ML Wed Dec 16 16:31:36 2015 +0100
@@ -190,7 +190,7 @@
(*Creates rules to eliminate ~A, from rules to introduce A*)
fun swapify intrs = intrs RLN (2, [Data.swap]);
-val swapped = Thm.rule_attribute (fn _ => fn th => th RSN (2, Data.swap));
+val swapped = Thm.rule_attribute [] (fn _ => fn th => th RSN (2, Data.swap));
(*Uses introduction rules in the normal way, or on negated assumptions,
trying rules in order. *)
--- a/src/Pure/Isar/calculation.ML Tue Dec 15 16:57:10 2015 +0100
+++ b/src/Pure/Isar/calculation.ML Wed Dec 16 16:31:36 2015 +0100
@@ -85,12 +85,13 @@
(* symmetric *)
-val symmetric = Thm.rule_attribute (fn context => fn th =>
- (case Seq.chop 2
- (Drule.multi_resolves (SOME (Context.proof_of context)) [th] (#2 (#1 (Data.get context)))) of
- ([th'], _) => Drule.zero_var_indexes th'
- | ([], _) => raise THM ("symmetric: no unifiers", 1, [th])
- | _ => raise THM ("symmetric: multiple unifiers", 1, [th])));
+val symmetric =
+ Thm.rule_attribute [] (fn context => fn th =>
+ (case Seq.chop 2
+ (Drule.multi_resolves (SOME (Context.proof_of context)) [th] (#2 (#1 (Data.get context)))) of
+ ([th'], _) => Drule.zero_var_indexes th'
+ | ([], _) => raise THM ("symmetric: no unifiers", 1, [th])
+ | _ => raise THM ("symmetric: multiple unifiers", 1, [th])));
(* concrete syntax *)
--- a/src/Pure/Isar/object_logic.ML Tue Dec 15 16:57:10 2015 +0100
+++ b/src/Pure/Isar/object_logic.ML Wed Dec 16 16:31:36 2015 +0100
@@ -213,7 +213,7 @@
val rulify = gen_rulify true;
val rulify_no_asm = gen_rulify false;
-val rule_format = Thm.rule_attribute (rulify o Context.proof_of);
-val rule_format_no_asm = Thm.rule_attribute (rulify_no_asm o Context.proof_of);
+val rule_format = Thm.rule_attribute [] (rulify o Context.proof_of);
+val rule_format_no_asm = Thm.rule_attribute [] (rulify_no_asm o Context.proof_of);
end;
--- a/src/Pure/Isar/rule_cases.ML Tue Dec 15 16:57:10 2015 +0100
+++ b/src/Pure/Isar/rule_cases.ML Wed Dec 16 16:31:36 2015 +0100
@@ -404,7 +404,7 @@
|> fold_index (fn (i, xs) => Thm.rename_params_rule (xs, i + 1)) xss
|> save th;
-fun params xss = Thm.rule_attribute (K (rename_params xss));
+fun params xss = Thm.rule_attribute [] (K (rename_params xss));
--- a/src/Pure/Pure.thy Tue Dec 15 16:57:10 2015 +0100
+++ b/src/Pure/Pure.thy Wed Dec 16 16:31:36 2015 +0100
@@ -128,26 +128,26 @@
attribute_setup THEN =
\<open>Scan.lift (Scan.optional (Args.bracks Parse.nat) 1) -- Attrib.thm
- >> (fn (i, B) => Thm.rule_attribute (fn _ => fn A => A RSN (i, B)))\<close>
+ >> (fn (i, B) => Thm.rule_attribute [B] (fn _ => fn A => A RSN (i, B)))\<close>
"resolution with rule"
attribute_setup OF =
- \<open>Attrib.thms >> (fn Bs => Thm.rule_attribute (fn _ => fn A => A OF Bs))\<close>
+ \<open>Attrib.thms >> (fn Bs => Thm.rule_attribute Bs (fn _ => fn A => A OF Bs))\<close>
"rule resolved with facts"
attribute_setup rename_abs =
\<open>Scan.lift (Scan.repeat (Args.maybe Args.name)) >> (fn vs =>
- Thm.rule_attribute (K (Drule.rename_bvars' vs)))\<close>
+ Thm.rule_attribute [] (K (Drule.rename_bvars' vs)))\<close>
"rename bound variables in abstractions"
attribute_setup unfolded =
\<open>Attrib.thms >> (fn ths =>
- Thm.rule_attribute (fn context => Local_Defs.unfold (Context.proof_of context) ths))\<close>
+ Thm.rule_attribute ths (fn context => Local_Defs.unfold (Context.proof_of context) ths))\<close>
"unfolded definitions"
attribute_setup folded =
\<open>Attrib.thms >> (fn ths =>
- Thm.rule_attribute (fn context => Local_Defs.fold (Context.proof_of context) ths))\<close>
+ Thm.rule_attribute ths (fn context => Local_Defs.fold (Context.proof_of context) ths))\<close>
"folded definitions"
attribute_setup consumes =
@@ -181,11 +181,11 @@
"result put into canonical rule format"
attribute_setup elim_format =
- \<open>Scan.succeed (Thm.rule_attribute (K Tactic.make_elim))\<close>
+ \<open>Scan.succeed (Thm.rule_attribute [] (K Tactic.make_elim))\<close>
"destruct rule turned into elimination rule format"
attribute_setup no_vars =
- \<open>Scan.succeed (Thm.rule_attribute (fn context => fn th =>
+ \<open>Scan.succeed (Thm.rule_attribute [] (fn context => fn th =>
let
val ctxt = Variable.set_body false (Context.proof_of context);
val ((_, [th']), _) = Variable.import true [th] ctxt;
@@ -202,7 +202,7 @@
attribute_setup rotated =
\<open>Scan.lift (Scan.optional Parse.int 1
- >> (fn n => Thm.rule_attribute (fn _ => rotate_prems n)))\<close>
+ >> (fn n => Thm.rule_attribute [] (fn _ => rotate_prems n)))\<close>
"rotated theorem premises"
attribute_setup defn =
@@ -210,7 +210,7 @@
"declaration of definitional transformations"
attribute_setup abs_def =
- \<open>Scan.succeed (Thm.rule_attribute (fn context =>
+ \<open>Scan.succeed (Thm.rule_attribute [] (fn context =>
Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def))\<close>
"abstract over free variables of definitional theorem"
--- a/src/Pure/Tools/rule_insts.ML Tue Dec 15 16:57:10 2015 +0100
+++ b/src/Pure/Tools/rule_insts.ML Wed Dec 16 16:31:36 2015 +0100
@@ -182,7 +182,7 @@
val _ = Theory.setup
(Attrib.setup @{binding "where"}
(Scan.lift named_insts >> (fn args =>
- Thm.rule_attribute (fn context => uncurry (where_rule (Context.proof_of context)) args)))
+ Thm.rule_attribute [] (fn context => uncurry (where_rule (Context.proof_of context)) args)))
"named instantiation of theorem");
@@ -202,7 +202,7 @@
val _ = Theory.setup
(Attrib.setup @{binding "of"}
(Scan.lift (insts -- Parse.for_fixes) >> (fn args =>
- Thm.rule_attribute (fn context => uncurry (of_rule (Context.proof_of context)) args)))
+ Thm.rule_attribute [] (fn context => uncurry (of_rule (Context.proof_of context)) args)))
"positional instantiation of theorem");
end;
--- a/src/Pure/more_thm.ML Tue Dec 15 16:57:10 2015 +0100
+++ b/src/Pure/more_thm.ML Wed Dec 16 16:31:36 2015 +0100
@@ -84,19 +84,8 @@
type attribute = Context.generic * thm -> Context.generic option * thm option
type binding = binding * attribute list
val empty_binding: binding
- val rule_attribute: (Context.generic -> thm -> thm) -> attribute
- val declaration_attribute: (thm -> Context.generic -> Context.generic) -> attribute
- val mixed_attribute: (Context.generic * thm -> Context.generic * thm) -> attribute
- val apply_attribute: attribute -> thm -> Context.generic -> thm * Context.generic
- val attribute_declaration: attribute -> thm -> Context.generic -> Context.generic
- val theory_attributes: attribute list -> thm -> theory -> thm * theory
- val proof_attributes: attribute list -> thm -> Proof.context -> thm * Proof.context
- val no_attributes: 'a -> 'a * 'b list
- val simple_fact: 'a -> ('a * 'b list) list
val tag_rule: string * string -> thm -> thm
val untag_rule: string -> thm -> thm
- val tag: string * string -> attribute
- val untag: string -> attribute
val is_free_dummy: thm -> bool
val tag_free_dummy: thm -> thm
val def_name: string -> string
@@ -109,6 +98,17 @@
val theoremK: string
val legacy_get_kind: thm -> string
val kind_rule: string -> thm -> thm
+ val rule_attribute: thm list -> (Context.generic -> thm -> thm) -> attribute
+ val declaration_attribute: (thm -> Context.generic -> Context.generic) -> attribute
+ val mixed_attribute: (Context.generic * thm -> Context.generic * thm) -> attribute
+ val apply_attribute: attribute -> thm -> Context.generic -> thm * Context.generic
+ val attribute_declaration: attribute -> thm -> Context.generic -> Context.generic
+ val theory_attributes: attribute list -> thm -> theory -> thm * theory
+ val proof_attributes: attribute list -> thm -> Proof.context -> thm * Proof.context
+ val no_attributes: 'a -> 'a * 'b list
+ val simple_fact: 'a -> ('a * 'b list) list
+ val tag: string * string -> attribute
+ val untag: string -> attribute
val kind: string -> attribute
val register_proofs: thm list -> theory -> theory
val join_theory_proofs: theory -> unit
@@ -543,38 +543,6 @@
-(** attributes **)
-
-(*attributes subsume any kind of rules or context modifiers*)
-type attribute = Context.generic * thm -> Context.generic option * thm option;
-
-type binding = binding * attribute list;
-val empty_binding: binding = (Binding.empty, []);
-
-fun rule_attribute f (x, th) = (NONE, SOME (f x th));
-fun declaration_attribute f (x, th) = (SOME (f th x), NONE);
-fun mixed_attribute f (x, th) = let val (x', th') = f (x, th) in (SOME x', SOME th') end;
-
-fun apply_attribute (att: attribute) th x =
- let val (x', th') = att (x, check_hyps x (Thm.transfer (Context.theory_of x) th))
- in (the_default th th', the_default x x') end;
-
-fun attribute_declaration att th x = #2 (apply_attribute att th x);
-
-fun apply_attributes mk dest =
- let
- fun app [] th x = (th, x)
- | app (att :: atts) th x = apply_attribute att th (mk x) ||> dest |-> app atts;
- in app end;
-
-val theory_attributes = apply_attributes Context.Theory Context.the_theory;
-val proof_attributes = apply_attributes Context.Proof Context.the_proof;
-
-fun no_attributes x = (x, []);
-fun simple_fact x = [(x, [])];
-
-
-
(*** theorem tags ***)
(* add / delete tags *)
@@ -582,9 +550,6 @@
fun tag_rule tg = Thm.map_tags (insert (op =) tg);
fun untag_rule s = Thm.map_tags (filter_out (fn (s', _) => s = s'));
-fun tag tg = rule_attribute (K (tag_rule tg));
-fun untag s = rule_attribute (K (untag_rule s));
-
(* free dummy thm -- for abstract closure *)
@@ -623,7 +588,50 @@
fun legacy_get_kind thm = the_default "" (Properties.get (Thm.get_tags thm) Markup.kindN);
fun kind_rule k = tag_rule (Markup.kindN, k) o untag_rule Markup.kindN;
-fun kind k = rule_attribute (K (k <> "" ? kind_rule k));
+
+
+
+(** attributes **)
+
+(*attributes subsume any kind of rules or context modifiers*)
+type attribute = Context.generic * thm -> Context.generic option * thm option;
+
+type binding = binding * attribute list;
+val empty_binding: binding = (Binding.empty, []);
+
+fun rule_attribute ths f (x, th) =
+ (NONE,
+ (case find_first is_free_dummy (th :: ths) of
+ SOME th' => SOME th'
+ | NONE => SOME (f x th)));
+
+fun declaration_attribute f (x, th) =
+ (if is_free_dummy th then NONE else SOME (f th x), NONE);
+
+fun mixed_attribute f (x, th) =
+ let val (x', th') = f (x, th) in (SOME x', SOME th') end;
+
+fun apply_attribute (att: attribute) th x =
+ let val (x', th') = att (x, check_hyps x (Thm.transfer (Context.theory_of x) th))
+ in (the_default th th', the_default x x') end;
+
+fun attribute_declaration att th x = #2 (apply_attribute att th x);
+
+fun apply_attributes mk dest =
+ let
+ fun app [] th x = (th, x)
+ | app (att :: atts) th x = apply_attribute att th (mk x) ||> dest |-> app atts;
+ in app end;
+
+val theory_attributes = apply_attributes Context.Theory Context.the_theory;
+val proof_attributes = apply_attributes Context.Proof Context.the_proof;
+
+fun no_attributes x = (x, []);
+fun simple_fact x = [(x, [])];
+
+fun tag tg = rule_attribute [] (K (tag_rule tg));
+fun untag s = rule_attribute [] (K (untag_rule s));
+fun kind k = rule_attribute [] (K (k <> "" ? kind_rule k));
(* forked proofs *)
--- a/src/Pure/simplifier.ML Tue Dec 15 16:57:10 2015 +0100
+++ b/src/Pure/simplifier.ML Wed Dec 16 16:31:36 2015 +0100
@@ -309,7 +309,7 @@
in
val simplified = conv_mode -- Attrib.thms >>
- (fn (f, ths) => Thm.rule_attribute (fn context =>
+ (fn (f, ths) => Thm.rule_attribute ths (fn context =>
f ((if null ths then I else Raw_Simplifier.clear_simpset)
(Context.proof_of context) addsimps ths)));
--- a/src/Tools/case_product.ML Tue Dec 15 16:57:10 2015 +0100
+++ b/src/Tools/case_product.ML Wed Dec 16 16:31:36 2015 +0100
@@ -96,7 +96,8 @@
Rule_Cases.name names o Rule_Cases.put_consumes (SOME (cons1 + cons2))
end
-fun annotation thm1 thm2 = Thm.rule_attribute (K (annotation_rule thm1 thm2))
+fun annotation thm1 thm2 =
+ Thm.rule_attribute [thm1, thm2] (K (annotation_rule thm1 thm2))
fun combine_annotated ctxt thm1 thm2 =
combine ctxt thm1 thm2
@@ -111,7 +112,7 @@
let
fun combine_list ctxt = fold (fn x => fn y => combine_annotated ctxt y x)
in
- Attrib.thms >> (fn thms => Thm.rule_attribute (fn ctxt => fn thm =>
+ Attrib.thms >> (fn thms => Thm.rule_attribute thms (fn ctxt => fn thm =>
combine_list (Context.proof_of ctxt) thms thm))
end
"product with other case rules")
--- a/src/Tools/induct.ML Tue Dec 15 16:57:10 2015 +0100
+++ b/src/Tools/induct.ML Wed Dec 16 16:31:36 2015 +0100
@@ -312,7 +312,9 @@
Thm.mixed_attribute (fn (context, thm) =>
let
val thm' = g thm;
- val context' = Data.map (f (name, Thm.trim_context thm')) context;
+ val context' =
+ if Thm.is_free_dummy thm then context
+ else Data.map (f (name, Thm.trim_context thm')) context;
in (context', thm') end);
fun del_att which =