--- 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;