src/Pure/Isar/attrib.ML
changeset 5879 18b8f048d93a
parent 5823 ee7c198a2154
child 5894 71667e5c2ff8
equal deleted inserted replaced
5878:769abc29bb8e 5879:18b8f048d93a
     6 *)
     6 *)
     7 
     7 
     8 signature BASIC_ATTRIB =
     8 signature BASIC_ATTRIB =
     9 sig
     9 sig
    10   val print_attributes: theory -> unit
    10   val print_attributes: theory -> unit
       
    11   val Attribute: bstring -> (Args.src -> theory attribute) * (Args.src -> Proof.context attribute)
       
    12     -> string -> unit
    11 end;
    13 end;
    12 
    14 
    13 signature ATTRIB =
    15 signature ATTRIB =
    14 sig
    16 sig
    15   include BASIC_ATTRIB
    17   include BASIC_ATTRIB
    16   val global_attribute: theory -> Args.src -> theory attribute
    18   val global_attribute: theory -> Args.src -> theory attribute
    17   val local_attribute: theory -> Args.src -> Proof.context attribute
    19   val local_attribute: theory -> Args.src -> Proof.context attribute
    18   val add_attributes: (bstring * ((Args.src -> theory attribute) *
    20   val add_attributes: (bstring * ((Args.src -> theory attribute) *
    19       (Args.src -> Proof.context attribute)) * string) list -> theory -> theory
    21       (Args.src -> Proof.context attribute)) * string) list -> theory -> theory
    20   val syntax: (Args.T list -> 'a * Args.T list) -> ('a -> 'b) -> Args.src -> 'b
    22   val global_thm: theory * Args.T list -> tthm * (theory * Args.T list)
       
    23   val global_thms: theory * Args.T list -> tthm list * (theory * Args.T list)
       
    24   val global_thmss: theory * Args.T list -> tthm list * (theory * Args.T list)
       
    25   val local_thm: Proof.context * Args.T list -> tthm * (Proof.context * Args.T list)
       
    26   val local_thms: Proof.context * Args.T list -> tthm list * (Proof.context * Args.T list)
       
    27   val local_thmss: Proof.context * Args.T list -> tthm list * (Proof.context * Args.T list)
       
    28   val syntax: ('a * Args.T list -> 'a attribute * ('a * Args.T list)) -> Args.src -> 'a attribute
    21   val no_args: 'a attribute -> Args.src -> 'a attribute
    29   val no_args: 'a attribute -> Args.src -> 'a attribute
    22   val thm_args: ('a -> string list -> tthm list)
       
    23     -> (tthm list -> 'a attribute) -> Args.src -> 'a attribute
       
    24   val global_thm_args: (tthm list -> theory attribute) -> Args.src -> theory attribute
       
    25   val local_thm_args: (tthm list -> Proof.context attribute)
       
    26     -> Args.src -> Proof.context attribute
       
    27   val setup: (theory -> theory) list
    30   val setup: (theory -> theory) list
    28 end;
    31 end;
    29 
    32 
    30 structure Attrib: ATTRIB =
    33 structure Attrib: ATTRIB =
    31 struct
    34 struct
    70 
    73 
    71 fun gen_attribute which thy =
    74 fun gen_attribute which thy =
    72   let
    75   let
    73     val {space, attrs} = AttributesData.get thy;
    76     val {space, attrs} = AttributesData.get thy;
    74 
    77 
    75     fun attr ((raw_name, args), pos) =
    78     fun attr src =
    76       let val name = NameSpace.intern space raw_name in
    79       let
       
    80         val ((raw_name, _), pos) = Args.dest_src src;
       
    81         val name = NameSpace.intern space raw_name;
       
    82       in
    77         (case Symtab.lookup (attrs, name) of
    83         (case Symtab.lookup (attrs, name) of
    78           None => error ("Unknown attribute: " ^ quote name ^ Position.str_of pos)
    84           None => error ("Unknown attribute: " ^ quote name ^ Position.str_of pos)
    79         | Some ((p, _), _) => which p ((name, args), pos))
    85         | Some ((p, _), _) => which p src)
    80       end;
    86       end;
    81   in attr end;
    87   in attr end;
    82 
    88 
    83 val global_attribute = gen_attribute fst;
    89 val global_attribute = gen_attribute fst;
    84 val local_attribute = gen_attribute snd;
    90 val local_attribute = gen_attribute snd;
       
    91 val local_attribute' = local_attribute o ProofContext.theory_of;
    85 
    92 
    86 
    93 
    87 (* add_attributes *)
    94 (* add_attributes *)
    88 
    95 
    89 fun add_attributes raw_attrs thy =
    96 fun add_attributes raw_attrs thy =
    96     val space' = NameSpace.extend (space, map fst new_attrs);
   103     val space' = NameSpace.extend (space, map fst new_attrs);
    97     val attrs' = Symtab.extend (attrs, new_attrs) handle Symtab.DUPS dups =>
   104     val attrs' = Symtab.extend (attrs, new_attrs) handle Symtab.DUPS dups =>
    98       error ("Duplicate declaration of attributes(s) " ^ commas_quote dups);
   105       error ("Duplicate declaration of attributes(s) " ^ commas_quote dups);
    99   in thy |> AttributesData.put {space = space', attrs = attrs'} end;
   106   in thy |> AttributesData.put {space = space', attrs = attrs'} end;
   100 
   107 
   101 
   108 (*implicit version*)
   102 (* attribute syntax *)
   109 fun Attribute name att cmt = Context.>> (add_attributes [(name, att, cmt)]);
   103 
   110 
   104 val attributeN = "attribute";
   111 
   105 fun syntax scan = Args.syntax attributeN scan;
   112 
   106 
   113 (** attribute parsers **)
   107 fun no_args x = syntax (Scan.succeed x) I;
   114 
   108 
   115 (* tags *)
   109 fun thm_args get f = syntax (Scan.repeat Args.name)
   116 
   110   (fn names => fn (x, ths) => f (get x names) (x, ths));
   117 fun tag x = Scan.lift (Args.name -- Scan.repeat Args.name) x;
   111 
   118 
   112 fun global_thm_args f = thm_args PureThy.get_tthmss f;
   119 
   113 fun local_thm_args f = thm_args ProofContext.get_tthmss f;
   120 (* theorems *)
       
   121 
       
   122 fun gen_thm get attrib app =
       
   123   Scan.depend (fn st => Args.name -- Args.opt_attribs >>
       
   124     (fn (name, srcs) => app ((st, get st name), map (attrib st) srcs)));
       
   125 
       
   126 val global_thm = gen_thm PureThy.get_tthm global_attribute Attribute.apply;
       
   127 val global_thms = gen_thm PureThy.get_tthms global_attribute Attribute.applys;
       
   128 val global_thmss = Scan.repeat global_thms >> flat;
       
   129 
       
   130 val local_thm = gen_thm ProofContext.get_tthm local_attribute' Attribute.apply;
       
   131 val local_thms = gen_thm ProofContext.get_tthms local_attribute' Attribute.applys;
       
   132 val local_thmss = Scan.repeat local_thms >> flat;
       
   133 
       
   134 
       
   135 
       
   136 (** attribute syntax **)
       
   137 
       
   138 fun syntax scan src (st, th) =
       
   139   let val (st', f) = Args.syntax "attribute" scan st src
       
   140   in f (st', th) end;
       
   141 
       
   142 fun no_args x = syntax (Scan.succeed x);
   114 
   143 
   115 
   144 
   116 
   145 
   117 (** Pure attributes **)
   146 (** Pure attributes **)
   118 
   147 
   119 (* tags *)
   148 (* tags *)
   120 
   149 
   121 fun gen_tag x = syntax (Args.name -- Scan.repeat Args.name) Attribute.tag x;
   150 fun gen_tag x = syntax (tag >> Attribute.tag) x;
   122 fun gen_untag x = syntax (Args.name -- Scan.repeat Args.name) Attribute.untag x;
   151 fun gen_untag x = syntax (tag >> Attribute.untag) x;
   123 fun gen_lemma x = no_args Attribute.tag_lemma x;
   152 fun gen_lemma x = no_args Attribute.tag_lemma x;
   124 fun gen_assumption x = no_args Attribute.tag_assumption x;
   153 fun gen_assumption x = no_args Attribute.tag_assumption x;
   125 
   154 
   126 
   155 
   127 (* resolution *)
   156 (* transfer *)
   128 
   157 
   129 fun gen_RS get = syntax Args.name
   158 fun gen_transfer theory_of = no_args (Attribute.rule (fn st => Thm.transfer (theory_of st)));
   130   (fn name => fn (x, (thm, tags)) => (x, (thm RS (Attribute.thm_of (get x name)), tags)));
   159 
   131 
   160 val global_transfer = gen_transfer I;
   132 fun RS_global x = gen_RS PureThy.get_tthm x;
   161 val local_transfer = gen_transfer ProofContext.theory_of;
   133 fun RS_local x = gen_RS ProofContext.get_tthm x;
   162 
   134 
   163 
       
   164 (* RS *)
       
   165 
       
   166 fun resolve (i, B) (x, A) =
       
   167   (x, Attribute.tthm_of (Attribute.thm_of A RSN (i, Attribute.thm_of B)));
       
   168 
       
   169 fun gen_RS thm = syntax (Scan.lift (Scan.optional Args.nat 1) -- thm >> resolve);
       
   170 val global_RS = gen_RS global_thm;
       
   171 val local_RS = gen_RS local_thm;
       
   172 
       
   173 
       
   174 (* APP *)
       
   175 
       
   176 fun apply Bs (x, A) =
       
   177   (x, Attribute.tthm_of (Attribute.thms_of Bs MRS Attribute.thm_of A));
       
   178 
       
   179 val global_APP = syntax (global_thmss >> apply);
       
   180 val local_APP = syntax (local_thmss >> apply);
       
   181 
       
   182 
       
   183 (* instantiations *)
       
   184 
       
   185 (* FIXME assumes non var hyps *)  (* FIXME move (see also drule.ML) *)
       
   186 val add_vars = foldl_aterms (fn (vs, Var v) => v ins vs | (vs, _) => vs);
       
   187 fun vars_of thm = (add_vars ([], #prop (Thm.rep_thm thm)));
       
   188 
       
   189 fun read_instantiate context_of raw_insts x thm =
       
   190   let
       
   191     val ctxt = context_of x;
       
   192     val sign = ProofContext.sign_of ctxt;
       
   193 
       
   194     val vars = vars_of thm;
       
   195     fun get_typ xi =
       
   196       (case assoc (vars, xi) of
       
   197         Some T => T
       
   198       | None => error ("No such variable in theorem: " ^ Syntax.string_of_vname xi));
       
   199 
       
   200     val (xs, ss) = Library.split_list raw_insts;
       
   201     val Ts = map get_typ xs;
       
   202 
       
   203     (* FIXME really declare_thm (!!!!??????) *)
       
   204     val (ts, envT) = ProofContext.read_termTs (ctxt |> ProofContext.declare_thm thm) (ss ~~ Ts);
       
   205 
       
   206     val cenvT = map (apsnd (Thm.ctyp_of sign)) envT;
       
   207     val cenv = map2 (fn (xi, t) => pairself (Thm.cterm_of sign) (Var (xi, fastype_of t), t)) (xs, ts);
       
   208   in Thm.instantiate (cenvT, cenv) thm end;
       
   209 
       
   210 
       
   211 val insts = Scan.lift (Args.enum1 "and" (Args.var --| Args.$$$ "=" -- Args.name));
       
   212 fun gen_where context_of = syntax (insts >> (Attribute.rule o read_instantiate context_of));
       
   213 
       
   214 val global_where = gen_where ProofContext.init;
       
   215 val local_where = gen_where I;
       
   216 
       
   217 
       
   218 (* misc rules *)
       
   219 
       
   220 fun standard x = no_args (Attribute.rule (K Drule.standard)) x;
       
   221 fun elimify x = no_args (Attribute.rule (K Tactic.make_elim)) x;
       
   222 
       
   223 
       
   224 
       
   225 (** theory setup **)
   135 
   226 
   136 (* pure_attributes *)
   227 (* pure_attributes *)
   137 
   228 
   138 val pure_attributes =
   229 val pure_attributes =
   139  [("tag", (gen_tag, gen_tag), "tag theorem"),
   230  [("tag", (gen_tag, gen_tag), "tag theorem"),
   140   ("untag", (gen_untag, gen_untag), "untag theorem"),
   231   ("untag", (gen_untag, gen_untag), "untag theorem"),
   141   ("lemma", (gen_lemma, gen_lemma), "tag as lemma"),
   232   ("lemma", (gen_lemma, gen_lemma), "tag as lemma"),
   142   ("assumption", (gen_assumption, gen_assumption), "tag as assumption"),
   233   ("assumption", (gen_assumption, gen_assumption), "tag as assumption"),
   143   ("RS", (RS_global, RS_local), "resolve with rule")];
   234   ("RS", (global_RS, local_RS), "resolve with rule"),
   144 
   235   ("APP", (global_APP, local_APP), "resolve rule with"),
   145 
   236   ("where", (global_where, local_where), "instantiate theorem (named vars)"),
   146 
   237   ("standard", (standard, standard), "put theorem into standard form"),
   147 (** theory setup **)
   238   ("elimify", (elimify, elimify), "turn destruct rule into elimination rule"),
       
   239   ("transfer", (global_transfer, local_transfer), "transfer theorem to this theory")];
       
   240 
       
   241 
       
   242 (* setup *)
   148 
   243 
   149 val setup = [AttributesData.init, add_attributes pure_attributes];
   244 val setup = [AttributesData.init, add_attributes pure_attributes];
   150 
   245 
   151 
   246 
   152 end;
   247 end;