src/Pure/Isar/attrib.ML
changeset 18636 cb068cfdcac8
parent 18418 bf448d999b7e
child 18678 dd0c569fa43d
     1.1 --- a/src/Pure/Isar/attrib.ML	Tue Jan 10 19:33:34 2006 +0100
     1.2 +++ b/src/Pure/Isar/attrib.ML	Tue Jan 10 19:33:35 2006 +0100
     1.3 @@ -16,7 +16,14 @@
     1.4  signature ATTRIB =
     1.5  sig
     1.6    include BASIC_ATTRIB
     1.7 +  val rule: ('a -> thm -> thm) -> 'a attribute
     1.8 +  val declaration: (thm -> 'a -> 'a) -> 'a attribute
     1.9    type src
    1.10 +  val theory: Context.generic attribute -> theory attribute
    1.11 +  val context: Context.generic attribute -> ProofContext.context attribute
    1.12 +  val generic: theory attribute * ProofContext.context attribute -> Context.generic attribute
    1.13 +  val common: (src -> Context.generic attribute) ->
    1.14 +    (src -> theory attribute) * (src -> ProofContext.context attribute)
    1.15    exception ATTRIB_FAIL of (string * Position.T) * exn
    1.16    val intern: theory -> xstring -> string
    1.17    val intern_src: theory -> src -> src
    1.18 @@ -28,6 +35,8 @@
    1.19    val context_attribute: ProofContext.context -> Args.src -> ProofContext.context attribute
    1.20    val undef_global_attribute: theory attribute
    1.21    val undef_local_attribute: ProofContext.context attribute
    1.22 +  val generic_attribute_i: theory -> src -> Context.generic attribute
    1.23 +  val generic_attribute: theory -> src -> Context.generic attribute
    1.24    val map_specs: ('a -> 'b attribute) ->
    1.25      (('c * 'a list) * 'd) list -> (('c * 'b attribute list) * 'd) list
    1.26    val map_facts: ('a -> 'b attribute) ->
    1.27 @@ -45,18 +54,38 @@
    1.28      thm list * (ProofContext.context * Args.T list)
    1.29    val local_thmss: ProofContext.context * Args.T list ->
    1.30      thm list * (ProofContext.context * Args.T list)
    1.31 +  val thm: Context.generic * Args.T list -> thm * (Context.generic * Args.T list)
    1.32 +  val thms: Context.generic * Args.T list -> thm list * (Context.generic * Args.T list)
    1.33 +  val thmss: Context.generic * Args.T list -> thm list * (Context.generic * Args.T list)
    1.34    val syntax: ('a * Args.T list -> 'a attribute * ('a * Args.T list)) -> src -> 'a attribute
    1.35    val no_args: 'a attribute -> src -> 'a attribute
    1.36    val add_del_args: 'a attribute -> 'a attribute -> src -> 'a attribute
    1.37 -  val attribute: (theory attribute * ProofContext.context attribute) -> src
    1.38 +  val attribute: Context.generic attribute -> src
    1.39  end;
    1.40  
    1.41  structure Attrib: ATTRIB =
    1.42  struct
    1.43  
    1.44 +val rule = Drule.rule_attribute;
    1.45 +val declaration = Drule.declaration_attribute;
    1.46 +
    1.47  type src = Args.src;
    1.48  
    1.49  
    1.50 +
    1.51 +(** generic attributes **)
    1.52 +
    1.53 +fun generic (global_att, local_att) =
    1.54 +   fn (Context.Theory thy, th) => apfst Context.Theory (global_att (thy, th))
    1.55 +    | (Context.Proof ctxt, th) => apfst Context.Proof (local_att (ctxt, th));
    1.56 +
    1.57 +fun theory att (thy, th) = apfst Context.the_theory (att (Context.Theory thy, th));
    1.58 +fun context att (ctxt, th) = apfst Context.the_proof (att (Context.Proof ctxt, th));
    1.59 +
    1.60 +fun common att = (theory o att, context o att);
    1.61 +
    1.62 +
    1.63 +
    1.64  (** attributes theory data **)
    1.65  
    1.66  (* datatype attributes *)
    1.67 @@ -125,6 +154,9 @@
    1.68  val undef_local_attribute: ProofContext.context attribute =
    1.69    fn _ => error "attribute undefined in proof context";
    1.70  
    1.71 +fun generic_attribute thy src = generic (global_attribute thy src, local_attribute thy src);
    1.72 +fun generic_attribute_i thy src = generic (global_attribute_i thy src, local_attribute_i thy src);
    1.73 +
    1.74  
    1.75  (* attributed declarations *)
    1.76  
    1.77 @@ -168,6 +200,8 @@
    1.78  
    1.79  (* theorems *)
    1.80  
    1.81 +local
    1.82 +
    1.83  fun gen_thm theory_of attrib get pick = Scan.depend (fn st =>
    1.84   (Scan.ahead Args.alt_name -- Args.named_fact (get st o Fact)
    1.85      >> (fn (s, fact) => ("", Fact s, fact)) ||
    1.86 @@ -183,6 +217,10 @@
    1.87        val (st', ths') = Thm.applys_attributes atts (st, ths);
    1.88      in (st', pick name ths') end));
    1.89  
    1.90 +val get_thms = Context.cases PureThy.get_thms ProofContext.get_thms;
    1.91 +
    1.92 +in
    1.93 +
    1.94  val global_thm = gen_thm I global_attribute_i PureThy.get_thms PureThy.single_thm;
    1.95  val global_thms = gen_thm I global_attribute_i PureThy.get_thms (K I);
    1.96  val global_thmss = Scan.repeat global_thms >> List.concat;
    1.97 @@ -193,6 +231,12 @@
    1.98    gen_thm ProofContext.theory_of local_attribute_i ProofContext.get_thms (K I);
    1.99  val local_thmss = Scan.repeat local_thms >> List.concat;
   1.100  
   1.101 +val thm = gen_thm Context.theory_of generic_attribute_i get_thms PureThy.single_thm;
   1.102 +val thms = gen_thm Context.theory_of generic_attribute_i get_thms (K I);
   1.103 +val thmss = Scan.repeat thms >> List.concat;
   1.104 +
   1.105 +end;
   1.106 +
   1.107  
   1.108  
   1.109  (** attribute syntax **)
   1.110 @@ -208,38 +252,26 @@
   1.111  
   1.112  
   1.113  
   1.114 -(** Pure attributes **)
   1.115 +(** basic attributes **)
   1.116  
   1.117  (* tags *)
   1.118  
   1.119 -fun gen_tagged x = syntax (tag >> Drule.tag) x;
   1.120 -fun gen_untagged x = syntax (Scan.lift Args.name >> Drule.untag) x;
   1.121 -
   1.122 -
   1.123 -(* COMP *)
   1.124 -
   1.125 -fun comp (i, B) (x, A) = (x, Drule.compose_single (A, i, B));
   1.126 -
   1.127 -fun gen_COMP thm = syntax (Scan.lift (Scan.optional (Args.bracks Args.nat) 1) -- thm >> comp);
   1.128 -val COMP_global = gen_COMP global_thm;
   1.129 -val COMP_local = gen_COMP local_thm;
   1.130 +fun tagged x = syntax (tag >> Drule.tag) x;
   1.131 +fun untagged x = syntax (Scan.lift Args.name >> Drule.untag) x;
   1.132  
   1.133  
   1.134 -(* THEN, which corresponds to RS *)
   1.135 -
   1.136 -fun resolve (i, B) (x, A) = (x, A RSN (i, B));
   1.137 +(* rule composition *)
   1.138  
   1.139 -fun gen_THEN thm = syntax (Scan.lift (Scan.optional (Args.bracks Args.nat) 1) -- thm >> resolve);
   1.140 -val THEN_global = gen_THEN global_thm;
   1.141 -val THEN_local = gen_THEN local_thm;
   1.142 +val COMP_att =
   1.143 +  syntax (Scan.lift (Scan.optional (Args.bracks Args.nat) 1) -- thm
   1.144 +    >> (fn (i, B) => Drule.rule_attribute (fn _ => fn A => Drule.compose_single (A, i, B))));
   1.145  
   1.146 -
   1.147 -(* OF *)
   1.148 +val THEN_att =
   1.149 +  syntax (Scan.lift (Scan.optional (Args.bracks Args.nat) 1) -- thm
   1.150 +    >> (fn (i, B) => Drule.rule_attribute (fn _ => fn A => A RSN (i, B))));
   1.151  
   1.152 -fun apply Bs (x, A) = (x, Bs MRS A);
   1.153 -
   1.154 -val OF_global = syntax (global_thmss >> apply);
   1.155 -val OF_local = syntax (local_thmss >> apply);
   1.156 +val OF_att =
   1.157 +  syntax (thmss >> (fn Bs => Drule.rule_attribute (fn _ => fn A => Bs MRS A)));
   1.158  
   1.159  
   1.160  (* read_instantiate: named instantiation of type and term variables *)
   1.161 @@ -281,10 +313,10 @@
   1.162  
   1.163  in
   1.164  
   1.165 -fun read_instantiate init mixed_insts (context, thm) =
   1.166 +fun read_instantiate mixed_insts (generic, thm) =
   1.167    let
   1.168 -    val ctxt = init context;
   1.169 -    val thy = ProofContext.theory_of ctxt;
   1.170 +    val thy = Context.theory_of generic;
   1.171 +    val ctxt = Context.proof_of generic;
   1.172  
   1.173      val (type_insts, term_insts) = List.partition (is_tvar o fst) (map snd mixed_insts);
   1.174      val internal_insts = term_insts |> List.mapPartial
   1.175 @@ -353,7 +385,7 @@
   1.176          else
   1.177            Args.assign (SOME (Args.Term (the (AList.lookup (op =) term_insts''' xi)))) arg);
   1.178  
   1.179 -  in (context, thm''' |> RuleCases.save thm) end;
   1.180 +  in (generic, thm''' |> RuleCases.save thm) end;
   1.181  
   1.182  end;
   1.183  
   1.184 @@ -370,13 +402,9 @@
   1.185  val inst = Args.var -- (Args.$$$ "=" |-- Args.ahead -- value)
   1.186    >> (fn (xi, (a, v)) => (a, (xi, v)));
   1.187  
   1.188 -fun gen_where init =
   1.189 -  syntax (Args.and_list (Scan.lift inst) >> read_instantiate init);
   1.190 -
   1.191  in
   1.192  
   1.193 -val where_global = gen_where ProofContext.init;
   1.194 -val where_local = gen_where I;
   1.195 +val where_att = syntax (Args.and_list (Scan.lift inst) >> read_instantiate);
   1.196  
   1.197  end;
   1.198  
   1.199 @@ -385,7 +413,7 @@
   1.200  
   1.201  local
   1.202  
   1.203 -fun read_instantiate' init (args, concl_args) (context, thm) =
   1.204 +fun read_instantiate' (args, concl_args) (generic, thm) =
   1.205    let
   1.206      fun zip_vars _ [] = []
   1.207        | zip_vars (_ :: xs) ((_, NONE) :: rest) = zip_vars xs rest
   1.208 @@ -394,9 +422,7 @@
   1.209      val insts =
   1.210        zip_vars (Drule.vars_of_terms [Thm.prop_of thm]) args @
   1.211        zip_vars (Drule.vars_of_terms [Thm.concl_of thm]) concl_args;
   1.212 -  in
   1.213 -    read_instantiate init insts (context, thm)
   1.214 -  end;
   1.215 +  in read_instantiate insts (generic, thm) end;
   1.216  
   1.217  val value =
   1.218    Args.internal_term >> Args.Term ||
   1.219 @@ -409,12 +435,9 @@
   1.220    Scan.repeat (Scan.unless concl inst) --
   1.221    Scan.optional (concl |-- Scan.repeat inst) [];
   1.222  
   1.223 -fun gen_of init = syntax (Scan.lift insts >> read_instantiate' init);
   1.224 -
   1.225  in
   1.226  
   1.227 -val of_global = gen_of ProofContext.init;
   1.228 -val of_local = gen_of I;
   1.229 +val of_att = syntax (Scan.lift insts >> read_instantiate');
   1.230  
   1.231  end;
   1.232  
   1.233 @@ -427,12 +450,8 @@
   1.234  
   1.235  (* unfold / fold definitions *)
   1.236  
   1.237 -fun gen_rewrite rew defs (x, thm) = (x, rew defs thm);
   1.238 -
   1.239 -val unfolded_global = syntax (global_thmss >> gen_rewrite Tactic.rewrite_rule);
   1.240 -val unfolded_local = syntax (local_thmss >> gen_rewrite Tactic.rewrite_rule);
   1.241 -val folded_global = syntax (global_thmss >> gen_rewrite Tactic.fold_rule);
   1.242 -val folded_local = syntax (local_thmss >> gen_rewrite Tactic.fold_rule);
   1.243 +val unfolded = syntax (thmss >> (fn defs => Drule.rule_attribute (K (Tactic.rewrite_rule defs))));
   1.244 +val folded = syntax (thmss >> (fn defs => Drule.rule_attribute (K (Tactic.fold_rule defs))));
   1.245  
   1.246  
   1.247  (* rule cases *)
   1.248 @@ -458,80 +477,41 @@
   1.249  fun eta_long x = no_args (Drule.rule_attribute (K (Drule.fconv_rule Drule.eta_long_conversion))) x;
   1.250  
   1.251  
   1.252 -(* rule declarations *)
   1.253 -
   1.254 -local
   1.255 -
   1.256 -fun add_args a b c x = syntax
   1.257 -  (Scan.lift ((Args.bang >> K a || Args.query >> K c || Scan.succeed b) -- (Scan.option Args.nat))
   1.258 -    >> (fn (f, n) => f n)) x;
   1.259 -
   1.260 -fun del_args att = syntax (Scan.lift Args.del >> K att);
   1.261 -
   1.262 -open ContextRules;
   1.263 -
   1.264 -in
   1.265 -
   1.266 -val rule_atts =
   1.267 - [("intro",
   1.268 -   (add_args intro_bang_global intro_global intro_query_global,
   1.269 -    add_args intro_bang_local intro_local intro_query_local),
   1.270 -    "declaration of introduction rule"),
   1.271 -  ("elim",
   1.272 -   (add_args elim_bang_global elim_global elim_query_global,
   1.273 -    add_args elim_bang_local elim_local elim_query_local),
   1.274 -    "declaration of elimination rule"),
   1.275 -  ("dest",
   1.276 -   (add_args dest_bang_global dest_global dest_query_global,
   1.277 -    add_args dest_bang_local dest_local dest_query_local),
   1.278 -    "declaration of destruction rule"),
   1.279 -  ("rule", (del_args rule_del_global, del_args rule_del_local),
   1.280 -    "remove declaration of intro/elim/dest rule")];
   1.281 -
   1.282 -end;
   1.283 -
   1.284 -
   1.285  (* internal attribute *)
   1.286  
   1.287  fun attribute att = Args.src (("Pure.attribute", [Args.mk_attribute att]), Position.none);
   1.288  
   1.289 -fun attribute_global x = (syntax (Scan.lift Args.internal_attribute >> #1)) x;
   1.290 -fun attribute_local x = (syntax (Scan.lift Args.internal_attribute >> #2)) x;
   1.291 -
   1.292 -val _ = Context.add_setup
   1.293 - [add_attributes [("attribute", (attribute_global, attribute_local), "internal attribute")]];
   1.294 +fun internal_att x = syntax (Scan.lift Args.internal_attribute) x;
   1.295  
   1.296  
   1.297 -(* pure_attributes *)
   1.298 +(* theory setup *)
   1.299  
   1.300 -val pure_attributes =
   1.301 - [("tagged", (gen_tagged, gen_tagged), "tagged theorem"),
   1.302 -  ("untagged", (gen_untagged, gen_untagged), "untagged theorem"),
   1.303 -  ("COMP", (COMP_global, COMP_local), "direct composition with rules (no lifting)"),
   1.304 -  ("THEN", (THEN_global, THEN_local), "resolution with rule"),
   1.305 -  ("OF", (OF_global, OF_local), "rule applied to facts"),
   1.306 -  ("where", (where_global, where_local), "named instantiation of theorem"),
   1.307 -  ("of", (of_global, of_local), "rule applied to terms"),
   1.308 -  ("rename_abs", (rename_abs, rename_abs), "rename bound variables in abstractions"),
   1.309 -  ("unfolded", (unfolded_global, unfolded_local), "unfolded definitions"),
   1.310 -  ("folded", (folded_global, folded_local), "folded definitions"),
   1.311 -  ("standard", (standard, standard), "result put into standard form"),
   1.312 -  ("elim_format", (elim_format, elim_format), "destruct rule turned into elimination rule format"),
   1.313 -  ("no_vars", (no_vars, no_vars), "frozen schematic vars"),
   1.314 -  ("eta_long", (eta_long, eta_long), "put theorem into eta long beta normal form"),
   1.315 -  ("consumes", (consumes, consumes), "number of consumed facts"),
   1.316 -  ("case_names", (case_names, case_names), "named rule cases"),
   1.317 -  ("case_conclusion", (case_conclusion, case_conclusion), "named conclusion of rule cases"),
   1.318 -  ("params", (params, params), "named rule parameters"),
   1.319 -  ("atomize", (no_args ObjectLogic.declare_atomize, no_args undef_local_attribute),
   1.320 -    "declaration of atomize rule"),
   1.321 -  ("rulify", (no_args ObjectLogic.declare_rulify, no_args undef_local_attribute),
   1.322 -    "declaration of rulify rule"),
   1.323 -  ("rule_format", (rule_format_att, rule_format_att), "result put into standard rule format")] @
   1.324 -  rule_atts;
   1.325 -
   1.326 -val _ = Context.add_setup [add_attributes pure_attributes];
   1.327 -
   1.328 +val _ = Context.add_setup
   1.329 + [add_attributes
   1.330 +   [("tagged", common tagged, "tagged theorem"),
   1.331 +    ("untagged", common untagged, "untagged theorem"),
   1.332 +    ("COMP", common COMP_att, "direct composition with rules (no lifting)"),
   1.333 +    ("THEN", common THEN_att, "resolution with rule"),
   1.334 +    ("OF", common OF_att, "rule applied to facts"),
   1.335 +    ("where", common where_att, "named instantiation of theorem"),
   1.336 +    ("of", common of_att, "rule applied to terms"),
   1.337 +    ("rename_abs", common rename_abs, "rename bound variables in abstractions"),
   1.338 +    ("unfolded", common unfolded, "unfolded definitions"),
   1.339 +    ("folded", common folded, "folded definitions"),
   1.340 +    ("standard", common standard, "result put into standard form"),
   1.341 +    ("elim_format", common elim_format, "destruct rule turned into elimination rule format"),
   1.342 +    ("no_vars", common no_vars, "frozen schematic vars"),
   1.343 +    ("eta_long", common eta_long, "put theorem into eta long beta normal form"),
   1.344 +    ("consumes", common consumes, "number of consumed facts"),
   1.345 +    ("case_names", common case_names, "named rule cases"),
   1.346 +    ("case_conclusion", common case_conclusion, "named conclusion of rule cases"),
   1.347 +    ("params", common params, "named rule parameters"),
   1.348 +    ("atomize", (no_args ObjectLogic.declare_atomize, no_args undef_local_attribute),
   1.349 +      "declaration of atomize rule"),
   1.350 +    ("rulify", (no_args ObjectLogic.declare_rulify, no_args undef_local_attribute),
   1.351 +      "declaration of rulify rule"),
   1.352 +    ("rule_format", common rule_format_att, "result put into standard rule format"),
   1.353 +    ("attribute", common internal_att, "internal attribute")]];
   1.354  
   1.355  end;
   1.356