# HG changeset patch # User wenzelm # Date 1450279896 -3600 # Node ID fb77560871015e1d394da4d392fc93411e73fd8f # Parent d273c24b577626427c8d04f0320a7279653f6bb6 rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy; diff -r d273c24b5776 -r fb7756087101 src/Doc/Eisbach/Manual.thy --- 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 = \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)))\ diff -r d273c24b5776 -r fb7756087101 src/Doc/Implementation/Isar.thy --- 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 \ \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}~\(fn context => rule)\ wraps - a context-dependent rule (mapping on @{ML_type thm}) as attribute. + \<^descr> @{ML Thm.rule_attribute}~\thms (fn context => rule)\ wraps a + context-dependent rule (mapping on @{ML_type thm}) as attribute. + + The \thms\ 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, \rule\ is bypassed. - \<^descr> @{ML Thm.declaration_attribute}~\(fn thm => decl)\ - wraps a theorem-dependent declaration (mapping on @{ML_type - Context.generic}) as attribute. + \<^descr> @{ML Thm.declaration_attribute}~\(fn thm => decl)\ 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 + \thm\. In that case, \decl\ is bypassed. \<^descr> @{ML Attrib.setup}~\name parser description\ provides the functionality of the Isar command @{command attribute_setup} as diff -r d273c24b5776 -r fb7756087101 src/Doc/Isar_Ref/Spec.thy --- 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 = \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))\ diff -r d273c24b5776 -r fb7756087101 src/HOL/Eisbach/Eisbach.thy --- 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 \ - 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}] -\ - method solves methods m = (m; fail) end diff -r d273c24b5776 -r fb7756087101 src/HOL/Eisbach/Eisbach_Tools.thy --- 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; \ -attribute_setup uncurry = \Scan.succeed (Thm.rule_attribute (K uncurry_rule))\ -attribute_setup curry = \Scan.succeed (Thm.rule_attribute (K curry_rule))\ +attribute_setup uncurry = \Scan.succeed (Thm.rule_attribute [] (K uncurry_rule))\ +attribute_setup curry = \Scan.succeed (Thm.rule_attribute [] (K curry_rule))\ end diff -r d273c24b5776 -r fb7756087101 src/HOL/Eisbach/eisbach_rule_insts.ML --- 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"); diff -r d273c24b5776 -r fb7756087101 src/HOL/Eisbach/method_closure.ML --- 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 = diff -r d273c24b5776 -r fb7756087101 src/HOL/TLA/Action.thy --- 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 @@ \ attribute_setup action_unlift = - \Scan.succeed (Thm.rule_attribute (action_unlift o Context.proof_of))\ + \Scan.succeed (Thm.rule_attribute [] (action_unlift o Context.proof_of))\ attribute_setup action_rewrite = - \Scan.succeed (Thm.rule_attribute (action_rewrite o Context.proof_of))\ + \Scan.succeed (Thm.rule_attribute [] (action_rewrite o Context.proof_of))\ attribute_setup action_use = - \Scan.succeed (Thm.rule_attribute (action_use o Context.proof_of))\ + \Scan.succeed (Thm.rule_attribute [] (action_use o Context.proof_of))\ (* =========================== square / angle brackets =========================== *) diff -r d273c24b5776 -r fb7756087101 src/HOL/TLA/Intensional.thy --- 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 @@ \ attribute_setup int_unlift = - \Scan.succeed (Thm.rule_attribute (int_unlift o Context.proof_of))\ + \Scan.succeed (Thm.rule_attribute [] (int_unlift o Context.proof_of))\ attribute_setup int_rewrite = - \Scan.succeed (Thm.rule_attribute (int_rewrite o Context.proof_of))\ -attribute_setup flatten = \Scan.succeed (Thm.rule_attribute (K flatten))\ + \Scan.succeed (Thm.rule_attribute [] (int_rewrite o Context.proof_of))\ +attribute_setup flatten = + \Scan.succeed (Thm.rule_attribute [] (K flatten))\ attribute_setup int_use = - \Scan.succeed (Thm.rule_attribute (int_use o Context.proof_of))\ + \Scan.succeed (Thm.rule_attribute [] (int_use o Context.proof_of))\ lemma Not_Rall: "\ (\(\x. F x)) = (\x. \F x)" by (simp add: Valid_def) diff -r d273c24b5776 -r fb7756087101 src/HOL/TLA/TLA.thy --- 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 @@ \ attribute_setup temp_unlift = - \Scan.succeed (Thm.rule_attribute (temp_unlift o Context.proof_of))\ + \Scan.succeed (Thm.rule_attribute [] (temp_unlift o Context.proof_of))\ attribute_setup temp_rewrite = - \Scan.succeed (Thm.rule_attribute (temp_rewrite o Context.proof_of))\ + \Scan.succeed (Thm.rule_attribute [] (temp_rewrite o Context.proof_of))\ attribute_setup temp_use = - \Scan.succeed (Thm.rule_attribute (temp_use o Context.proof_of))\ + \Scan.succeed (Thm.rule_attribute [] (temp_use o Context.proof_of))\ attribute_setup try_rewrite = - \Scan.succeed (Thm.rule_attribute (try_rewrite o Context.proof_of))\ + \Scan.succeed (Thm.rule_attribute [] (try_rewrite o Context.proof_of))\ (* ------------------------------------------------------------------------- *) diff -r d273c24b5776 -r fb7756087101 src/HOL/Tools/Quotient/quotient_tacs.ML --- 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) diff -r d273c24b5776 -r fb7756087101 src/HOL/Tools/Transfer/transfer.ML --- 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 diff -r d273c24b5776 -r fb7756087101 src/HOL/Tools/inductive_set.ML --- 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 ****) diff -r d273c24b5776 -r fb7756087101 src/HOL/Tools/legacy_transfer.ML --- 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"); diff -r d273c24b5776 -r fb7756087101 src/HOL/Tools/split_rule.ML --- 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; diff -r d273c24b5776 -r fb7756087101 src/HOL/UNITY/Comp/Alloc.thy --- 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 *} diff -r d273c24b5776 -r fb7756087101 src/Provers/classical.ML --- 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. *) diff -r d273c24b5776 -r fb7756087101 src/Pure/Isar/calculation.ML --- 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 *) diff -r d273c24b5776 -r fb7756087101 src/Pure/Isar/object_logic.ML --- 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; diff -r d273c24b5776 -r fb7756087101 src/Pure/Isar/rule_cases.ML --- 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)); diff -r d273c24b5776 -r fb7756087101 src/Pure/Pure.thy --- 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 = \Scan.lift (Scan.optional (Args.bracks Parse.nat) 1) -- Attrib.thm - >> (fn (i, B) => Thm.rule_attribute (fn _ => fn A => A RSN (i, B)))\ + >> (fn (i, B) => Thm.rule_attribute [B] (fn _ => fn A => A RSN (i, B)))\ "resolution with rule" attribute_setup OF = - \Attrib.thms >> (fn Bs => Thm.rule_attribute (fn _ => fn A => A OF Bs))\ + \Attrib.thms >> (fn Bs => Thm.rule_attribute Bs (fn _ => fn A => A OF Bs))\ "rule resolved with facts" attribute_setup rename_abs = \Scan.lift (Scan.repeat (Args.maybe Args.name)) >> (fn vs => - Thm.rule_attribute (K (Drule.rename_bvars' vs)))\ + Thm.rule_attribute [] (K (Drule.rename_bvars' vs)))\ "rename bound variables in abstractions" attribute_setup unfolded = \Attrib.thms >> (fn ths => - Thm.rule_attribute (fn context => Local_Defs.unfold (Context.proof_of context) ths))\ + Thm.rule_attribute ths (fn context => Local_Defs.unfold (Context.proof_of context) ths))\ "unfolded definitions" attribute_setup folded = \Attrib.thms >> (fn ths => - Thm.rule_attribute (fn context => Local_Defs.fold (Context.proof_of context) ths))\ + Thm.rule_attribute ths (fn context => Local_Defs.fold (Context.proof_of context) ths))\ "folded definitions" attribute_setup consumes = @@ -181,11 +181,11 @@ "result put into canonical rule format" attribute_setup elim_format = - \Scan.succeed (Thm.rule_attribute (K Tactic.make_elim))\ + \Scan.succeed (Thm.rule_attribute [] (K Tactic.make_elim))\ "destruct rule turned into elimination rule format" attribute_setup no_vars = - \Scan.succeed (Thm.rule_attribute (fn context => fn th => + \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 = \Scan.lift (Scan.optional Parse.int 1 - >> (fn n => Thm.rule_attribute (fn _ => rotate_prems n)))\ + >> (fn n => Thm.rule_attribute [] (fn _ => rotate_prems n)))\ "rotated theorem premises" attribute_setup defn = @@ -210,7 +210,7 @@ "declaration of definitional transformations" attribute_setup abs_def = - \Scan.succeed (Thm.rule_attribute (fn context => + \Scan.succeed (Thm.rule_attribute [] (fn context => Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def))\ "abstract over free variables of definitional theorem" diff -r d273c24b5776 -r fb7756087101 src/Pure/Tools/rule_insts.ML --- 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; diff -r d273c24b5776 -r fb7756087101 src/Pure/more_thm.ML --- 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 *) diff -r d273c24b5776 -r fb7756087101 src/Pure/simplifier.ML --- 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))); diff -r d273c24b5776 -r fb7756087101 src/Tools/case_product.ML --- 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") diff -r d273c24b5776 -r fb7756087101 src/Tools/induct.ML --- 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 =