--- a/src/Pure/Isar/attrib.ML Thu Apr 07 12:08:02 2016 +0200
+++ b/src/Pure/Isar/attrib.ML Thu Apr 07 12:13:11 2016 +0200
@@ -500,7 +500,78 @@
(* theory setup *)
val _ = Theory.setup
- (register_config Goal.quick_and_dirty_raw #>
+ (setup @{binding tagged} (Scan.lift (Args.name -- Args.name) >> Thm.tag) "tagged theorem" #>
+ setup @{binding untagged} (Scan.lift Args.name >> Thm.untag) "untagged theorem" #>
+ setup @{binding kind} (Scan.lift Args.name >> Thm.kind) "theorem kind" #>
+ setup @{binding THEN}
+ (Scan.lift (Scan.optional (Args.bracks Parse.nat) 1) -- thm
+ >> (fn (i, B) => Thm.rule_attribute [B] (fn _ => fn A => A RSN (i, B))))
+ "resolution with rule" #>
+ setup @{binding OF}
+ (thms >> (fn Bs => Thm.rule_attribute Bs (fn _ => fn A => A OF Bs)))
+ "rule resolved with facts" #>
+ setup @{binding rename_abs}
+ (Scan.lift (Scan.repeat (Args.maybe Args.name)) >> (fn vs =>
+ Thm.rule_attribute [] (K (Drule.rename_bvars' vs))))
+ "rename bound variables in abstractions" #>
+ setup @{binding unfolded}
+ (thms >> (fn ths =>
+ Thm.rule_attribute ths (fn context => Local_Defs.unfold (Context.proof_of context) ths)))
+ "unfolded definitions" #>
+ setup @{binding folded}
+ (thms >> (fn ths =>
+ Thm.rule_attribute ths (fn context => Local_Defs.fold (Context.proof_of context) ths)))
+ "folded definitions" #>
+ setup @{binding consumes}
+ (Scan.lift (Scan.optional Parse.int 1) >> Rule_Cases.consumes)
+ "number of consumed facts" #>
+ setup @{binding constraints}
+ (Scan.lift Parse.nat >> Rule_Cases.constraints)
+ "number of equality constraints" #>
+ setup @{binding case_names}
+ (Scan.lift (Scan.repeat1 (Args.name --
+ Scan.optional (Parse.$$$ "[" |-- Scan.repeat1 (Args.maybe Args.name) --| Parse.$$$ "]") []))
+ >> (fn cs =>
+ Rule_Cases.cases_hyp_names
+ (map #1 cs)
+ (map (map (the_default Rule_Cases.case_hypsN) o #2) cs)))
+ "named rule cases" #>
+ setup @{binding case_conclusion}
+ (Scan.lift (Args.name -- Scan.repeat Args.name) >> Rule_Cases.case_conclusion)
+ "named conclusion of rule cases" #>
+ setup @{binding params}
+ (Scan.lift (Parse.and_list1 (Scan.repeat Args.name)) >> Rule_Cases.params)
+ "named rule parameters" #>
+ setup @{binding rule_format}
+ (Scan.lift (Args.mode "no_asm")
+ >> (fn true => Object_Logic.rule_format_no_asm | false => Object_Logic.rule_format))
+ "result put into canonical rule format" #>
+ setup @{binding elim_format}
+ (Scan.succeed (Thm.rule_attribute [] (K Tactic.make_elim)))
+ "destruct rule turned into elimination rule format" #>
+ setup @{binding no_vars}
+ (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;
+ in th' end)))
+ "imported schematic variables" #>
+ setup @{binding atomize}
+ (Scan.succeed Object_Logic.declare_atomize) "declaration of atomize rule" #>
+ setup @{binding rulify}
+ (Scan.succeed Object_Logic.declare_rulify) "declaration of rulify rule" #>
+ setup @{binding rotated}
+ (Scan.lift (Scan.optional Parse.int 1
+ >> (fn n => Thm.rule_attribute [] (fn _ => rotate_prems n)))) "rotated theorem premises" #>
+ setup @{binding defn}
+ (add_del Local_Defs.defn_add Local_Defs.defn_del)
+ "declaration of definitional transformations" #>
+ setup @{binding abs_def}
+ (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" #>
+
+ register_config Goal.quick_and_dirty_raw #>
register_config Ast.trace_raw #>
register_config Ast.stats_raw #>
register_config Printer.show_brackets_raw #>