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