# HG changeset patch # User wenzelm # Date 1201363722 -3600 # Node ID 111d2ed164f41436489e4e133889c7008bee7373 # Parent caee173104d3918ecc53246035a9cdb68fd39d9d misc tuning and internal rearrangement; tuned attribute syntax -- no need for eta-expansion; diff -r caee173104d3 -r 111d2ed164f4 src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Sat Jan 26 17:08:41 2008 +0100 +++ b/src/Pure/Isar/attrib.ML Sat Jan 26 17:08:42 2008 +0100 @@ -27,7 +27,15 @@ (('c * 'att list) * ('d * 'att list) list) list val crude_closure: Proof.context -> src -> src val add_attributes: (bstring * (src -> attribute) * string) list -> theory -> theory + val syntax: (Context.generic * Args.T list -> + attribute * (Context.generic * Args.T list)) -> src -> attribute + val no_args: attribute -> src -> attribute + val add_del_args: attribute -> attribute -> src -> attribute + val thm: Context.generic * Args.T list -> thm * (Context.generic * Args.T list) + val thms: Context.generic * Args.T list -> thm list * (Context.generic * Args.T list) + val multi_thm: Context.generic * Args.T list -> thm list * (Context.generic * Args.T list) val print_configs: Proof.context -> unit + val internal: (morphism -> attribute) -> src val register_config: Config.value Config.T -> theory -> theory val config_bool: bstring -> bool -> bool Config.T * (theory -> theory) val config_int: bstring -> int -> int Config.T * (theory -> theory) @@ -35,14 +43,6 @@ val config_bool_global: bstring -> bool -> bool Config.T * (theory -> theory) val config_int_global: bstring -> int -> int Config.T * (theory -> theory) val config_string_global: bstring -> string -> string Config.T * (theory -> theory) - val thm: Context.generic * Args.T list -> thm * (Context.generic * Args.T list) - val thms: Context.generic * Args.T list -> thm list * (Context.generic * Args.T list) - val multi_thm: Context.generic * Args.T list -> thm list * (Context.generic * Args.T list) - val syntax: (Context.generic * Args.T list -> - attribute * (Context.generic * Args.T list)) -> src -> attribute - val no_args: attribute -> src -> attribute - val add_del_args: attribute -> attribute -> src -> attribute - val internal: (morphism -> attribute) -> src end; structure Attrib: ATTRIB = @@ -50,7 +50,6 @@ type src = Args.src; - (** named attributes **) (* theory data *) @@ -141,15 +140,20 @@ in Attributes.map add thy end; - -(** attribute parsers **) +(* attribute syntax *) -(* tags *) +fun syntax scan src (st, th) = + let val (f: attribute, st') = Args.syntax "attribute" scan src st + in f (st', th) end; -fun tag x = Scan.lift (Args.name -- Args.name) x; +fun no_args x = syntax (Scan.succeed x); + +fun add_del_args add del = syntax + (Scan.lift (Args.add >> K add || Args.del >> K del || Scan.succeed add)); -(* theorems *) + +(** parsing attributed theorems **) local @@ -188,16 +192,114 @@ -(** attribute syntax **) +(** basic attributes **) + +(* internal *) + +fun internal att = Args.src (("Pure.attribute", [Args.mk_attribute att]), Position.none); + +val internal_att = + syntax (Scan.lift Args.internal_attribute >> Morphism.form); + + +(* tags *) + +val tagged = syntax (Scan.lift (Args.name -- Args.name) >> PureThy.tag); +val untagged = syntax (Scan.lift Args.name >> PureThy.untag); + +val kind = syntax (Scan.lift Args.name >> PureThy.kind); + + +(* rule composition *) + +val COMP_att = + syntax (Scan.lift (Scan.optional (Args.bracks Args.nat) 1) -- thm + >> (fn (i, B) => Thm.rule_attribute (fn _ => fn A => Drule.compose_single (A, i, B)))); + +val THEN_att = + syntax (Scan.lift (Scan.optional (Args.bracks Args.nat) 1) -- thm + >> (fn (i, B) => Thm.rule_attribute (fn _ => fn A => A RSN (i, B)))); + +val OF_att = + syntax (thms >> (fn Bs => Thm.rule_attribute (fn _ => fn A => Bs MRS A))); + + +(* rename_abs *) + +val rename_abs = syntax + (Scan.lift (Scan.repeat (Args.maybe Args.name) >> (apsnd o Drule.rename_bvars'))); + + +(* unfold / fold definitions *) + +fun unfolded_syntax rule = + syntax (thms >> + (fn ths => Thm.rule_attribute (fn context => rule (Context.proof_of context) ths))); + +val unfolded = unfolded_syntax LocalDefs.unfold; +val folded = unfolded_syntax LocalDefs.fold; + + +(* rule cases *) -fun syntax scan src (st, th) = - let val (f, st') = Args.syntax "attribute" scan src st - in f (st', th) end; +val consumes = syntax (Scan.lift (Scan.optional Args.nat 1) >> RuleCases.consumes); +val case_names = syntax (Scan.lift (Scan.repeat1 Args.name) >> RuleCases.case_names); +val case_conclusion = + syntax (Scan.lift (Args.name -- Scan.repeat Args.name) >> RuleCases.case_conclusion); +val params = syntax (Args.and_list1 (Scan.lift (Scan.repeat Args.name)) >> RuleCases.params); + + +(* rule format *) + +val rule_format = syntax (Args.mode "no_asm" + >> (fn true => ObjectLogic.rule_format_no_asm | false => ObjectLogic.rule_format)); + +val elim_format = no_args (Thm.rule_attribute (K Tactic.make_elim)); + + +(* misc rules *) + +val standard = no_args (Thm.rule_attribute (K Drule.standard)); + +val no_vars = no_args (Thm.rule_attribute (fn ctxt => fn th => + let val ((_, [th']), _) = Variable.import_thms true [th] (Context.proof_of ctxt) + in th' end)); + +val eta_long = + no_args (Thm.rule_attribute (K (Conv.fconv_rule Drule.eta_long_conversion))); + +val rotated = syntax + (Scan.lift (Scan.optional Args.int 1) >> (fn n => Thm.rule_attribute (K (rotate_prems n)))); -fun no_args x = syntax (Scan.succeed x); + +(* theory setup *) -fun add_del_args add del x = syntax - (Scan.lift (Args.add >> K add || Args.del >> K del || Scan.succeed add)) x; +val _ = Context.add_setup + (add_attributes + [("attribute", internal_att, "internal attribute"), + ("tagged", tagged, "tagged theorem"), + ("untagged", untagged, "untagged theorem"), + ("kind", kind, "theorem kind"), + ("COMP", COMP_att, "direct composition with rules (no lifting)"), + ("THEN", THEN_att, "resolution with rule"), + ("OF", OF_att, "rule applied to facts"), + ("rename_abs", rename_abs, "rename bound variables in abstractions"), + ("unfolded", unfolded, "unfolded definitions"), + ("folded", folded, "folded definitions"), + ("standard", standard, "result put into standard form"), + ("elim_format", elim_format, "destruct rule turned into elimination rule format"), + ("no_vars", no_vars, "frozen schematic vars"), + ("eta_long", eta_long, "put theorem into eta long beta normal form"), + ("consumes", consumes, "number of consumed facts"), + ("case_names", case_names, "named rule cases"), + ("case_conclusion", case_conclusion, "named conclusion of rule cases"), + ("params", params, "named rule parameters"), + ("atomize", no_args ObjectLogic.declare_atomize, "declaration of atomize rule"), + ("rulify", no_args ObjectLogic.declare_rulify, "declaration of rulify rule"), + ("rule_format", rule_format, "result put into standard rule format"), + ("rotated", rotated, "rotated theorem premises"), + ("defn", add_del_args LocalDefs.defn_add LocalDefs.defn_del, + "declaration of definitional transformations")]); @@ -273,91 +375,6 @@ end; - -(** basic attributes **) - -(* tags *) - -fun tagged x = syntax (tag >> PureThy.tag) x; -fun untagged x = syntax (Scan.lift Args.name >> PureThy.untag) x; - -fun kind x = syntax (Scan.lift Args.name >> PureThy.kind) x; - - -(* rule composition *) - -val COMP_att = - syntax (Scan.lift (Scan.optional (Args.bracks Args.nat) 1) -- thm - >> (fn (i, B) => Thm.rule_attribute (fn _ => fn A => Drule.compose_single (A, i, B)))); - -val THEN_att = - syntax (Scan.lift (Scan.optional (Args.bracks Args.nat) 1) -- thm - >> (fn (i, B) => Thm.rule_attribute (fn _ => fn A => A RSN (i, B)))); - -val OF_att = - syntax (thms >> (fn Bs => Thm.rule_attribute (fn _ => fn A => Bs MRS A))); - - -(* rename_abs *) - -fun rename_abs src = syntax - (Scan.lift (Scan.repeat (Args.maybe Args.name) >> (apsnd o Drule.rename_bvars'))) src; - - -(* unfold / fold definitions *) - -fun unfolded_syntax rule = - syntax (thms >> - (fn ths => Thm.rule_attribute (fn context => rule (Context.proof_of context) ths))); - -val unfolded = unfolded_syntax LocalDefs.unfold; -val folded = unfolded_syntax LocalDefs.fold; - - -(* rule cases *) - -fun consumes x = syntax (Scan.lift (Scan.optional Args.nat 1) >> RuleCases.consumes) x; -fun case_names x = syntax (Scan.lift (Scan.repeat1 Args.name) >> RuleCases.case_names) x; -fun case_conclusion x = - syntax (Scan.lift (Args.name -- Scan.repeat Args.name) >> RuleCases.case_conclusion) x; -fun params x = syntax (Args.and_list1 (Scan.lift (Scan.repeat Args.name)) >> RuleCases.params) x; - - -(* rule format *) - -fun rule_format_att x = syntax (Args.mode "no_asm" - >> (fn true => ObjectLogic.rule_format_no_asm | false => ObjectLogic.rule_format)) x; - -fun elim_format x = no_args (Thm.rule_attribute (K Tactic.make_elim)) x; - - -(* misc rules *) - -fun standard x = no_args (Thm.rule_attribute (K Drule.standard)) x; - -fun no_vars x = no_args (Thm.rule_attribute (fn ctxt => fn th => - let val ((_, [th']), _) = Variable.import_thms true [th] (Context.proof_of ctxt) - in th' end)) x; - -fun eta_long x = - no_args (Thm.rule_attribute (K (Conv.fconv_rule Drule.eta_long_conversion))) x; - - -(* internal attribute *) - -fun internal att = Args.src (("Pure.attribute", [Args.mk_attribute att]), Position.none); - -fun internal_att x = - syntax (Scan.lift Args.internal_attribute >> Morphism.form) x; - - -(* attribute rotated *) - -fun rotated_att x = - syntax (Scan.lift (Scan.optional Args.int 1) >> - (fn n => Thm.rule_attribute (fn _ => rotate_prems n))) x - - (* theory setup *) val _ = Context.add_setup @@ -365,32 +382,7 @@ register_config Unify.search_bound_value #> register_config Unify.trace_simp_value #> register_config Unify.trace_types_value #> - register_config MetaSimplifier.simp_depth_limit_value #> - add_attributes - [("tagged", tagged, "tagged theorem"), - ("untagged", untagged, "untagged theorem"), - ("kind", kind, "theorem kind"), - ("COMP", COMP_att, "direct composition with rules (no lifting)"), - ("THEN", THEN_att, "resolution with rule"), - ("OF", OF_att, "rule applied to facts"), - ("rename_abs", rename_abs, "rename bound variables in abstractions"), - ("unfolded", unfolded, "unfolded definitions"), - ("folded", folded, "folded definitions"), - ("standard", standard, "result put into standard form"), - ("elim_format", elim_format, "destruct rule turned into elimination rule format"), - ("no_vars", no_vars, "frozen schematic vars"), - ("eta_long", eta_long, "put theorem into eta long beta normal form"), - ("consumes", consumes, "number of consumed facts"), - ("case_names", case_names, "named rule cases"), - ("case_conclusion", case_conclusion, "named conclusion of rule cases"), - ("params", params, "named rule parameters"), - ("atomize", no_args ObjectLogic.declare_atomize, "declaration of atomize rule"), - ("rulify", no_args ObjectLogic.declare_rulify, "declaration of rulify rule"), - ("rule_format", rule_format_att, "result put into standard rule format"), - ("rotated", rotated_att, "rotated theorem premises"), - ("defn", add_del_args LocalDefs.defn_add LocalDefs.defn_del, - "declaration of definitional transformations"), - ("attribute", internal_att, "internal attribute")]); + register_config MetaSimplifier.simp_depth_limit_value); end;