1.1 --- a/src/Pure/Isar/attrib.ML Sat Jan 26 17:08:41 2008 +0100
1.2 +++ b/src/Pure/Isar/attrib.ML Sat Jan 26 17:08:42 2008 +0100
1.3 @@ -27,7 +27,15 @@
1.4 (('c * 'att list) * ('d * 'att list) list) list
1.5 val crude_closure: Proof.context -> src -> src
1.6 val add_attributes: (bstring * (src -> attribute) * string) list -> theory -> theory
1.7 + val syntax: (Context.generic * Args.T list ->
1.8 + attribute * (Context.generic * Args.T list)) -> src -> attribute
1.9 + val no_args: attribute -> src -> attribute
1.10 + val add_del_args: attribute -> attribute -> src -> attribute
1.11 + val thm: Context.generic * Args.T list -> thm * (Context.generic * Args.T list)
1.12 + val thms: Context.generic * Args.T list -> thm list * (Context.generic * Args.T list)
1.13 + val multi_thm: Context.generic * Args.T list -> thm list * (Context.generic * Args.T list)
1.14 val print_configs: Proof.context -> unit
1.15 + val internal: (morphism -> attribute) -> src
1.16 val register_config: Config.value Config.T -> theory -> theory
1.17 val config_bool: bstring -> bool -> bool Config.T * (theory -> theory)
1.18 val config_int: bstring -> int -> int Config.T * (theory -> theory)
1.19 @@ -35,14 +43,6 @@
1.20 val config_bool_global: bstring -> bool -> bool Config.T * (theory -> theory)
1.21 val config_int_global: bstring -> int -> int Config.T * (theory -> theory)
1.22 val config_string_global: bstring -> string -> string Config.T * (theory -> theory)
1.23 - val thm: Context.generic * Args.T list -> thm * (Context.generic * Args.T list)
1.24 - val thms: Context.generic * Args.T list -> thm list * (Context.generic * Args.T list)
1.25 - val multi_thm: Context.generic * Args.T list -> thm list * (Context.generic * Args.T list)
1.26 - val syntax: (Context.generic * Args.T list ->
1.27 - attribute * (Context.generic * Args.T list)) -> src -> attribute
1.28 - val no_args: attribute -> src -> attribute
1.29 - val add_del_args: attribute -> attribute -> src -> attribute
1.30 - val internal: (morphism -> attribute) -> src
1.31 end;
1.32
1.33 structure Attrib: ATTRIB =
1.34 @@ -50,7 +50,6 @@
1.35
1.36 type src = Args.src;
1.37
1.38 -
1.39 (** named attributes **)
1.40
1.41 (* theory data *)
1.42 @@ -141,15 +140,20 @@
1.43 in Attributes.map add thy end;
1.44
1.45
1.46 +(* attribute syntax *)
1.47
1.48 -(** attribute parsers **)
1.49 +fun syntax scan src (st, th) =
1.50 + let val (f: attribute, st') = Args.syntax "attribute" scan src st
1.51 + in f (st', th) end;
1.52
1.53 -(* tags *)
1.54 +fun no_args x = syntax (Scan.succeed x);
1.55
1.56 -fun tag x = Scan.lift (Args.name -- Args.name) x;
1.57 +fun add_del_args add del = syntax
1.58 + (Scan.lift (Args.add >> K add || Args.del >> K del || Scan.succeed add));
1.59
1.60
1.61 -(* theorems *)
1.62 +
1.63 +(** parsing attributed theorems **)
1.64
1.65 local
1.66
1.67 @@ -188,16 +192,114 @@
1.68
1.69
1.70
1.71 -(** attribute syntax **)
1.72 +(** basic attributes **)
1.73
1.74 -fun syntax scan src (st, th) =
1.75 - let val (f, st') = Args.syntax "attribute" scan src st
1.76 - in f (st', th) end;
1.77 +(* internal *)
1.78
1.79 -fun no_args x = syntax (Scan.succeed x);
1.80 +fun internal att = Args.src (("Pure.attribute", [Args.mk_attribute att]), Position.none);
1.81
1.82 -fun add_del_args add del x = syntax
1.83 - (Scan.lift (Args.add >> K add || Args.del >> K del || Scan.succeed add)) x;
1.84 +val internal_att =
1.85 + syntax (Scan.lift Args.internal_attribute >> Morphism.form);
1.86 +
1.87 +
1.88 +(* tags *)
1.89 +
1.90 +val tagged = syntax (Scan.lift (Args.name -- Args.name) >> PureThy.tag);
1.91 +val untagged = syntax (Scan.lift Args.name >> PureThy.untag);
1.92 +
1.93 +val kind = syntax (Scan.lift Args.name >> PureThy.kind);
1.94 +
1.95 +
1.96 +(* rule composition *)
1.97 +
1.98 +val COMP_att =
1.99 + syntax (Scan.lift (Scan.optional (Args.bracks Args.nat) 1) -- thm
1.100 + >> (fn (i, B) => Thm.rule_attribute (fn _ => fn A => Drule.compose_single (A, i, B))));
1.101 +
1.102 +val THEN_att =
1.103 + syntax (Scan.lift (Scan.optional (Args.bracks Args.nat) 1) -- thm
1.104 + >> (fn (i, B) => Thm.rule_attribute (fn _ => fn A => A RSN (i, B))));
1.105 +
1.106 +val OF_att =
1.107 + syntax (thms >> (fn Bs => Thm.rule_attribute (fn _ => fn A => Bs MRS A)));
1.108 +
1.109 +
1.110 +(* rename_abs *)
1.111 +
1.112 +val rename_abs = syntax
1.113 + (Scan.lift (Scan.repeat (Args.maybe Args.name) >> (apsnd o Drule.rename_bvars')));
1.114 +
1.115 +
1.116 +(* unfold / fold definitions *)
1.117 +
1.118 +fun unfolded_syntax rule =
1.119 + syntax (thms >>
1.120 + (fn ths => Thm.rule_attribute (fn context => rule (Context.proof_of context) ths)));
1.121 +
1.122 +val unfolded = unfolded_syntax LocalDefs.unfold;
1.123 +val folded = unfolded_syntax LocalDefs.fold;
1.124 +
1.125 +
1.126 +(* rule cases *)
1.127 +
1.128 +val consumes = syntax (Scan.lift (Scan.optional Args.nat 1) >> RuleCases.consumes);
1.129 +val case_names = syntax (Scan.lift (Scan.repeat1 Args.name) >> RuleCases.case_names);
1.130 +val case_conclusion =
1.131 + syntax (Scan.lift (Args.name -- Scan.repeat Args.name) >> RuleCases.case_conclusion);
1.132 +val params = syntax (Args.and_list1 (Scan.lift (Scan.repeat Args.name)) >> RuleCases.params);
1.133 +
1.134 +
1.135 +(* rule format *)
1.136 +
1.137 +val rule_format = syntax (Args.mode "no_asm"
1.138 + >> (fn true => ObjectLogic.rule_format_no_asm | false => ObjectLogic.rule_format));
1.139 +
1.140 +val elim_format = no_args (Thm.rule_attribute (K Tactic.make_elim));
1.141 +
1.142 +
1.143 +(* misc rules *)
1.144 +
1.145 +val standard = no_args (Thm.rule_attribute (K Drule.standard));
1.146 +
1.147 +val no_vars = no_args (Thm.rule_attribute (fn ctxt => fn th =>
1.148 + let val ((_, [th']), _) = Variable.import_thms true [th] (Context.proof_of ctxt)
1.149 + in th' end));
1.150 +
1.151 +val eta_long =
1.152 + no_args (Thm.rule_attribute (K (Conv.fconv_rule Drule.eta_long_conversion)));
1.153 +
1.154 +val rotated = syntax
1.155 + (Scan.lift (Scan.optional Args.int 1) >> (fn n => Thm.rule_attribute (K (rotate_prems n))));
1.156 +
1.157 +
1.158 +(* theory setup *)
1.159 +
1.160 +val _ = Context.add_setup
1.161 + (add_attributes
1.162 + [("attribute", internal_att, "internal attribute"),
1.163 + ("tagged", tagged, "tagged theorem"),
1.164 + ("untagged", untagged, "untagged theorem"),
1.165 + ("kind", kind, "theorem kind"),
1.166 + ("COMP", COMP_att, "direct composition with rules (no lifting)"),
1.167 + ("THEN", THEN_att, "resolution with rule"),
1.168 + ("OF", OF_att, "rule applied to facts"),
1.169 + ("rename_abs", rename_abs, "rename bound variables in abstractions"),
1.170 + ("unfolded", unfolded, "unfolded definitions"),
1.171 + ("folded", folded, "folded definitions"),
1.172 + ("standard", standard, "result put into standard form"),
1.173 + ("elim_format", elim_format, "destruct rule turned into elimination rule format"),
1.174 + ("no_vars", no_vars, "frozen schematic vars"),
1.175 + ("eta_long", eta_long, "put theorem into eta long beta normal form"),
1.176 + ("consumes", consumes, "number of consumed facts"),
1.177 + ("case_names", case_names, "named rule cases"),
1.178 + ("case_conclusion", case_conclusion, "named conclusion of rule cases"),
1.179 + ("params", params, "named rule parameters"),
1.180 + ("atomize", no_args ObjectLogic.declare_atomize, "declaration of atomize rule"),
1.181 + ("rulify", no_args ObjectLogic.declare_rulify, "declaration of rulify rule"),
1.182 + ("rule_format", rule_format, "result put into standard rule format"),
1.183 + ("rotated", rotated, "rotated theorem premises"),
1.184 + ("defn", add_del_args LocalDefs.defn_add LocalDefs.defn_del,
1.185 + "declaration of definitional transformations")]);
1.186
1.187
1.188
1.189 @@ -273,91 +375,6 @@
1.190 end;
1.191
1.192
1.193 -
1.194 -(** basic attributes **)
1.195 -
1.196 -(* tags *)
1.197 -
1.198 -fun tagged x = syntax (tag >> PureThy.tag) x;
1.199 -fun untagged x = syntax (Scan.lift Args.name >> PureThy.untag) x;
1.200 -
1.201 -fun kind x = syntax (Scan.lift Args.name >> PureThy.kind) x;
1.202 -
1.203 -
1.204 -(* rule composition *)
1.205 -
1.206 -val COMP_att =
1.207 - syntax (Scan.lift (Scan.optional (Args.bracks Args.nat) 1) -- thm
1.208 - >> (fn (i, B) => Thm.rule_attribute (fn _ => fn A => Drule.compose_single (A, i, B))));
1.209 -
1.210 -val THEN_att =
1.211 - syntax (Scan.lift (Scan.optional (Args.bracks Args.nat) 1) -- thm
1.212 - >> (fn (i, B) => Thm.rule_attribute (fn _ => fn A => A RSN (i, B))));
1.213 -
1.214 -val OF_att =
1.215 - syntax (thms >> (fn Bs => Thm.rule_attribute (fn _ => fn A => Bs MRS A)));
1.216 -
1.217 -
1.218 -(* rename_abs *)
1.219 -
1.220 -fun rename_abs src = syntax
1.221 - (Scan.lift (Scan.repeat (Args.maybe Args.name) >> (apsnd o Drule.rename_bvars'))) src;
1.222 -
1.223 -
1.224 -(* unfold / fold definitions *)
1.225 -
1.226 -fun unfolded_syntax rule =
1.227 - syntax (thms >>
1.228 - (fn ths => Thm.rule_attribute (fn context => rule (Context.proof_of context) ths)));
1.229 -
1.230 -val unfolded = unfolded_syntax LocalDefs.unfold;
1.231 -val folded = unfolded_syntax LocalDefs.fold;
1.232 -
1.233 -
1.234 -(* rule cases *)
1.235 -
1.236 -fun consumes x = syntax (Scan.lift (Scan.optional Args.nat 1) >> RuleCases.consumes) x;
1.237 -fun case_names x = syntax (Scan.lift (Scan.repeat1 Args.name) >> RuleCases.case_names) x;
1.238 -fun case_conclusion x =
1.239 - syntax (Scan.lift (Args.name -- Scan.repeat Args.name) >> RuleCases.case_conclusion) x;
1.240 -fun params x = syntax (Args.and_list1 (Scan.lift (Scan.repeat Args.name)) >> RuleCases.params) x;
1.241 -
1.242 -
1.243 -(* rule format *)
1.244 -
1.245 -fun rule_format_att x = syntax (Args.mode "no_asm"
1.246 - >> (fn true => ObjectLogic.rule_format_no_asm | false => ObjectLogic.rule_format)) x;
1.247 -
1.248 -fun elim_format x = no_args (Thm.rule_attribute (K Tactic.make_elim)) x;
1.249 -
1.250 -
1.251 -(* misc rules *)
1.252 -
1.253 -fun standard x = no_args (Thm.rule_attribute (K Drule.standard)) x;
1.254 -
1.255 -fun no_vars x = no_args (Thm.rule_attribute (fn ctxt => fn th =>
1.256 - let val ((_, [th']), _) = Variable.import_thms true [th] (Context.proof_of ctxt)
1.257 - in th' end)) x;
1.258 -
1.259 -fun eta_long x =
1.260 - no_args (Thm.rule_attribute (K (Conv.fconv_rule Drule.eta_long_conversion))) x;
1.261 -
1.262 -
1.263 -(* internal attribute *)
1.264 -
1.265 -fun internal att = Args.src (("Pure.attribute", [Args.mk_attribute att]), Position.none);
1.266 -
1.267 -fun internal_att x =
1.268 - syntax (Scan.lift Args.internal_attribute >> Morphism.form) x;
1.269 -
1.270 -
1.271 -(* attribute rotated *)
1.272 -
1.273 -fun rotated_att x =
1.274 - syntax (Scan.lift (Scan.optional Args.int 1) >>
1.275 - (fn n => Thm.rule_attribute (fn _ => rotate_prems n))) x
1.276 -
1.277 -
1.278 (* theory setup *)
1.279
1.280 val _ = Context.add_setup
1.281 @@ -365,32 +382,7 @@
1.282 register_config Unify.search_bound_value #>
1.283 register_config Unify.trace_simp_value #>
1.284 register_config Unify.trace_types_value #>
1.285 - register_config MetaSimplifier.simp_depth_limit_value #>
1.286 - add_attributes
1.287 - [("tagged", tagged, "tagged theorem"),
1.288 - ("untagged", untagged, "untagged theorem"),
1.289 - ("kind", kind, "theorem kind"),
1.290 - ("COMP", COMP_att, "direct composition with rules (no lifting)"),
1.291 - ("THEN", THEN_att, "resolution with rule"),
1.292 - ("OF", OF_att, "rule applied to facts"),
1.293 - ("rename_abs", rename_abs, "rename bound variables in abstractions"),
1.294 - ("unfolded", unfolded, "unfolded definitions"),
1.295 - ("folded", folded, "folded definitions"),
1.296 - ("standard", standard, "result put into standard form"),
1.297 - ("elim_format", elim_format, "destruct rule turned into elimination rule format"),
1.298 - ("no_vars", no_vars, "frozen schematic vars"),
1.299 - ("eta_long", eta_long, "put theorem into eta long beta normal form"),
1.300 - ("consumes", consumes, "number of consumed facts"),
1.301 - ("case_names", case_names, "named rule cases"),
1.302 - ("case_conclusion", case_conclusion, "named conclusion of rule cases"),
1.303 - ("params", params, "named rule parameters"),
1.304 - ("atomize", no_args ObjectLogic.declare_atomize, "declaration of atomize rule"),
1.305 - ("rulify", no_args ObjectLogic.declare_rulify, "declaration of rulify rule"),
1.306 - ("rule_format", rule_format_att, "result put into standard rule format"),
1.307 - ("rotated", rotated_att, "rotated theorem premises"),
1.308 - ("defn", add_del_args LocalDefs.defn_add LocalDefs.defn_del,
1.309 - "declaration of definitional transformations"),
1.310 - ("attribute", internal_att, "internal attribute")]);
1.311 + register_config MetaSimplifier.simp_depth_limit_value);
1.312
1.313 end;
1.314