src/Pure/Isar/rule_insts.ML
author wenzelm
Sat Jun 14 23:20:12 2008 +0200 (2008-06-14)
changeset 27219 a248dba028ff
parent 27120 b21eec437295
child 27236 80356567e7ad
permissions -rw-r--r--
export subgoal_tac, subgoals_tac, thin_tac;
     1 (*  Title:      Pure/Isar/rule_insts.ML
     2     ID:         $Id$
     3     Author:     Makarius
     4 
     5 Rule instantiations -- operations within a rule/subgoal context.
     6 *)
     7 
     8 signature RULE_INSTS =
     9 sig
    10   val bires_inst_tac: bool -> Proof.context -> (indexname * string) list ->
    11     thm -> int -> tactic
    12   val res_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic
    13   val eres_inst_tac: Proof.context -> (indexname * string) list -> thm -> int -> tactic
    14   val subgoal_tac: Proof.context -> string -> int -> tactic
    15   val subgoals_tac: Proof.context -> string list -> int -> tactic
    16   val thin_tac: Proof.context -> string -> int -> tactic
    17 end;
    18 
    19 structure RuleInsts: RULE_INSTS =
    20 struct
    21 
    22 
    23 (** reading instantiations **)
    24 
    25 local
    26 
    27 fun is_tvar (x, _) = String.isPrefix "'" x;
    28 
    29 fun error_var msg xi = error (msg ^ Term.string_of_vname xi);
    30 
    31 fun the_sort tvars xi = the (AList.lookup (op =) tvars xi)
    32   handle Option.Option => error_var "No such type variable in theorem: " xi;
    33 
    34 fun the_type vars xi = the (AList.lookup (op =) vars xi)
    35   handle Option.Option => error_var "No such variable in theorem: " xi;
    36 
    37 fun unify_vartypes thy vars (xi, u) (unifier, maxidx) =
    38   let
    39     val T = the_type vars xi;
    40     val U = Term.fastype_of u;
    41     val maxidx' = Term.maxidx_term u (Int.max (#2 xi, maxidx));
    42   in
    43     Sign.typ_unify thy (T, U) (unifier, maxidx')
    44       handle Type.TUNIFY => error_var "Incompatible type for instantiation of " xi
    45   end;
    46 
    47 fun instantiate inst =
    48   TermSubst.instantiate ([], map (fn (xi, t) => ((xi, Term.fastype_of t), t)) inst) #>
    49   Envir.beta_norm;
    50 
    51 fun make_instT f v =
    52   let
    53     val T = TVar v;
    54     val T' = f T;
    55   in if T = T' then NONE else SOME (T, T') end;
    56 
    57 fun make_inst f v =
    58   let
    59     val t = Var v;
    60     val t' = f t;
    61   in if t aconv t' then NONE else SOME (t, t') end;
    62 
    63 in
    64 
    65 fun read_termTs ctxt schematic ss Ts =
    66   let
    67     fun parse T = if T = propT then Syntax.parse_prop ctxt else Syntax.parse_term ctxt;
    68     val ts = map2 parse Ts ss;
    69     val ts' =
    70       map2 (TypeInfer.constrain o TypeInfer.paramify_vars) Ts ts
    71       |> Syntax.check_terms ((schematic ? ProofContext.set_mode ProofContext.mode_schematic) ctxt)
    72       |> Variable.polymorphic ctxt;
    73     val Ts' = map Term.fastype_of ts';
    74     val tyenv = fold Type.raw_match (Ts ~~ Ts') Vartab.empty;
    75   in (ts', map (apsnd snd) (Vartab.dest tyenv)) end;
    76 
    77 fun read_insts ctxt mixed_insts (tvars, vars) =
    78   let
    79     val thy = ProofContext.theory_of ctxt;
    80     val cert = Thm.cterm_of thy;
    81     val certT = Thm.ctyp_of thy;
    82 
    83     val (type_insts, term_insts) = List.partition (is_tvar o fst) mixed_insts;
    84     val internal_insts = term_insts |> map_filter
    85       (fn (xi, Args.Term t) => SOME (xi, t)
    86         | (_, Args.Text _) => NONE
    87         | (xi, _) => error_var "Term argument expected for " xi);
    88     val external_insts = term_insts |> map_filter
    89       (fn (xi, Args.Text s) => SOME (xi, s) | _ => NONE);
    90 
    91 
    92     (* mixed type instantiations *)
    93 
    94     fun readT (xi, arg) =
    95       let
    96         val S = the_sort tvars xi;
    97         val T =
    98           (case arg of
    99             Args.Text s => Syntax.read_typ ctxt s
   100           | Args.Typ T => T
   101           | _ => error_var "Type argument expected for " xi);
   102       in
   103         if Sign.of_sort thy (T, S) then ((xi, S), T)
   104         else error_var "Incompatible sort for typ instantiation of " xi
   105       end;
   106 
   107     val type_insts1 = map readT type_insts;
   108     val instT1 = TermSubst.instantiateT type_insts1;
   109     val vars1 = map (apsnd instT1) vars;
   110 
   111 
   112     (* internal term instantiations *)
   113 
   114     val instT2 = Envir.norm_type
   115       (#1 (fold (unify_vartypes thy vars1) internal_insts (Vartab.empty, 0)));
   116     val vars2 = map (apsnd instT2) vars1;
   117     val internal_insts2 = map (apsnd (map_types instT2)) internal_insts;
   118     val inst2 = instantiate internal_insts2;
   119 
   120 
   121     (* external term instantiations *)
   122 
   123     val (xs, strs) = split_list external_insts;
   124     val Ts = map (the_type vars2) xs;
   125     val (ts, inferred) = read_termTs ctxt false strs Ts;
   126 
   127     val instT3 = Term.typ_subst_TVars inferred;
   128     val vars3 = map (apsnd instT3) vars2;
   129     val internal_insts3 = map (apsnd (map_types instT3)) internal_insts2;
   130     val external_insts3 = xs ~~ ts;
   131     val inst3 = instantiate external_insts3;
   132 
   133 
   134     (* results *)
   135 
   136     val type_insts3 = map (fn ((a, _), T) => (a, instT3 (instT2 T))) type_insts1;
   137     val term_insts3 = internal_insts3 @ external_insts3;
   138 
   139     val inst_tvars = map_filter (make_instT (instT3 o instT2 o instT1)) tvars;
   140     val inst_vars = map_filter (make_inst (inst3 o inst2)) vars3;
   141   in
   142     ((type_insts3, term_insts3),
   143       (map (pairself certT) inst_tvars, map (pairself cert) inst_vars))
   144   end;
   145 
   146 fun read_instantiate ctxt mixed_insts thm =
   147   let
   148     val ctxt' = ctxt |> Variable.declare_thm thm
   149       |> fold (fn a => Variable.declare_internal (Logic.mk_type (TFree (a, [])))) (Drule.add_used thm []);  (* FIXME tmp *)
   150     val tvars = Thm.fold_terms Term.add_tvars thm [];
   151     val vars = Thm.fold_terms Term.add_vars thm [];
   152     val ((type_insts, term_insts), insts) = read_insts ctxt' (map snd mixed_insts) (tvars, vars);
   153 
   154     val _ = (*assign internalized values*)
   155       mixed_insts |> List.app (fn (arg, (xi, _)) =>
   156         if is_tvar xi then
   157           Args.assign (SOME (Args.Typ (the (AList.lookup (op =) type_insts xi)))) arg
   158         else
   159           Args.assign (SOME (Args.Term (the (AList.lookup (op =) term_insts xi)))) arg);
   160   in
   161     Drule.instantiate insts thm |> RuleCases.save thm
   162   end;
   163 
   164 fun read_instantiate' ctxt (args, concl_args) thm =
   165   let
   166     fun zip_vars _ [] = []
   167       | zip_vars (_ :: xs) ((_, NONE) :: rest) = zip_vars xs rest
   168       | zip_vars ((x, _) :: xs) ((arg, SOME t) :: rest) = (arg, (x, t)) :: zip_vars xs rest
   169       | zip_vars [] _ = error "More instantiations than variables in theorem";
   170     val insts =
   171       zip_vars (rev (Term.add_vars (Thm.full_prop_of thm) [])) args @
   172       zip_vars (rev (Term.add_vars (Thm.concl_of thm) [])) concl_args;
   173   in read_instantiate ctxt insts thm end;
   174 
   175 end;
   176 
   177 
   178 
   179 (** attributes **)
   180 
   181 (* where: named instantiation *)
   182 
   183 local
   184 
   185 val value =
   186   Args.internal_typ >> Args.Typ ||
   187   Args.internal_term >> Args.Term ||
   188   Args.name >> Args.Text;
   189 
   190 val inst = Args.var -- (Args.$$$ "=" |-- Args.ahead -- value)
   191   >> (fn (xi, (a, v)) => (a, (xi, v)));
   192 
   193 in
   194 
   195 val where_att = Attrib.syntax (Args.and_list (Scan.lift inst) >> (fn args =>
   196   Thm.rule_attribute (fn context => read_instantiate (Context.proof_of context) args)));
   197 
   198 end;
   199 
   200 
   201 (* of: positional instantiation (terms only) *)
   202 
   203 local
   204 
   205 val value =
   206   Args.internal_term >> Args.Term ||
   207   Args.name >> Args.Text;
   208 
   209 val inst = Args.ahead -- Args.maybe value;
   210 val concl = Args.$$$ "concl" -- Args.colon;
   211 
   212 val insts =
   213   Scan.repeat (Scan.unless concl inst) --
   214   Scan.optional (concl |-- Scan.repeat inst) [];
   215 
   216 in
   217 
   218 val of_att = Attrib.syntax (Scan.lift insts >> (fn args =>
   219   Thm.rule_attribute (fn context => read_instantiate' (Context.proof_of context) args)));
   220 
   221 end;
   222 
   223 
   224 (* setup *)
   225 
   226 val _ = Context.>> (Context.map_theory
   227   (Attrib.add_attributes
   228    [("where", where_att, "named instantiation of theorem"),
   229     ("of", of_att, "positional instantiation of theorem")]));
   230 
   231 
   232 
   233 (** methods **)
   234 
   235 (* rule_tac etc. -- refer to dynamic goal state!! *)   (* FIXME cleanup this mess!!! *)
   236 
   237 fun bires_inst_tac bires_flag ctxt insts thm =
   238   let
   239     val thy = ProofContext.theory_of ctxt;
   240     (* Separate type and term insts *)
   241     fun has_type_var ((x, _), _) = (case Symbol.explode x of
   242           "'"::cs => true | cs => false);
   243     val Tinsts = List.filter has_type_var insts;
   244     val tinsts = filter_out has_type_var insts;
   245 
   246     (* Tactic *)
   247     fun tac i st =
   248       let
   249         val (_, _, Bi, _) = Thm.dest_state (st, i);
   250         val params = Logic.strip_params Bi;  (*params of subgoal i as string typ pairs*)
   251         val params = rev (Term.rename_wrt_term Bi params)
   252           (*as they are printed: bound variables with*)
   253           (*the same name are renamed during printing*)
   254 
   255         val (param_names, ctxt') = ctxt
   256           |> Variable.declare_thm thm
   257           |> Thm.fold_terms Variable.declare_constraints st
   258           |> ProofContext.add_fixes_i (map (fn (x, T) => (x, SOME T, NoSyn)) params);
   259 
   260         (* Process type insts: Tinsts_env *)
   261         fun absent xi = error
   262               ("No such variable in theorem: " ^ Term.string_of_vname xi);
   263         val (rtypes, rsorts) = Drule.types_sorts thm;
   264         fun readT (xi, s) =
   265             let val S = case rsorts xi of SOME S => S | NONE => absent xi;
   266                 val T = Syntax.read_typ ctxt' s;
   267                 val U = TVar (xi, S);
   268             in if Sign.typ_instance thy (T, U) then (U, T)
   269                else error ("Instantiation of " ^ Term.string_of_vname xi ^ " fails")
   270             end;
   271         val Tinsts_env = map readT Tinsts;
   272         (* Preprocess rule: extract vars and their types, apply Tinsts *)
   273         fun get_typ xi =
   274           (case rtypes xi of
   275                SOME T => typ_subst_atomic Tinsts_env T
   276              | NONE => absent xi);
   277         val (xis, ss) = Library.split_list tinsts;
   278         val Ts = map get_typ xis;
   279 
   280         val (ts, envT) = read_termTs ctxt' true ss Ts;
   281         val envT' = map (fn (ixn, T) =>
   282           (TVar (ixn, the (rsorts ixn)), T)) envT @ Tinsts_env;
   283         val cenv =
   284           map
   285             (fn (xi, t) =>
   286               pairself (Thm.cterm_of thy) (Var (xi, fastype_of t), t))
   287             (distinct
   288               (fn ((x1, t1), (x2, t2)) => x1 = x2 andalso t1 aconv t2)
   289               (xis ~~ ts));
   290         (* Lift and instantiate rule *)
   291         val {maxidx, ...} = rep_thm st;
   292         val paramTs = map #2 params
   293         and inc = maxidx+1
   294         fun liftvar (Var ((a,j), T)) =
   295               Var((a, j+inc), paramTs ---> Logic.incr_tvar inc T)
   296           | liftvar t = raise TERM("Variable expected", [t]);
   297         fun liftterm t = list_abs_free
   298               (param_names ~~ paramTs, Logic.incr_indexes(paramTs,inc) t)
   299         fun liftpair (cv,ct) =
   300               (cterm_fun liftvar cv, cterm_fun liftterm ct)
   301         val lifttvar = pairself (ctyp_of thy o Logic.incr_tvar inc);
   302         val rule = Drule.instantiate
   303               (map lifttvar envT', map liftpair cenv)
   304               (Thm.lift_rule (Thm.cprem_of st i) thm)
   305       in
   306         if i > nprems_of st then no_tac st
   307         else st |>
   308           compose_tac (bires_flag, rule, nprems_of thm) i
   309       end
   310            handle TERM (msg,_)   => (warning msg; no_tac st)
   311                 | THM  (msg,_,_) => (warning msg; no_tac st);
   312   in tac end;
   313 
   314 val res_inst_tac = bires_inst_tac false;
   315 val eres_inst_tac = bires_inst_tac true;
   316 
   317 
   318 local
   319 
   320 fun gen_inst _ tac _ (quant, ([], thms)) =
   321       Method.METHOD (fn facts => quant (Method.insert_tac facts THEN' tac thms))
   322   | gen_inst inst_tac _ ctxt (quant, (insts, [thm])) =
   323       Method.METHOD (fn facts =>
   324         quant (Method.insert_tac facts THEN' inst_tac ctxt insts thm))
   325   | gen_inst _ _ _ _ = error "Cannot have instantiations with multiple rules";
   326 
   327 in
   328 
   329 val res_inst_meth = gen_inst res_inst_tac Tactic.resolve_tac;
   330 val eres_inst_meth = gen_inst eres_inst_tac Tactic.eresolve_tac;
   331 
   332 val cut_inst_meth =
   333   gen_inst
   334     (fn ctxt => fn insts => res_inst_tac ctxt insts o Tactic.make_elim_preserve)
   335     Tactic.cut_rules_tac;
   336 
   337 val dres_inst_meth =
   338   gen_inst
   339     (fn ctxt => fn insts => eres_inst_tac ctxt insts o Tactic.make_elim_preserve)
   340     Tactic.dresolve_tac;
   341 
   342 val forw_inst_meth =
   343   gen_inst
   344     (fn ctxt => fn insts => fn rule =>
   345        res_inst_tac ctxt insts (Tactic.make_elim_preserve rule) THEN' assume_tac)
   346     Tactic.forward_tac;
   347 
   348 fun subgoal_tac ctxt sprop = DETERM o res_inst_tac ctxt [(("psi", 0), sprop)] cut_rl;
   349 fun subgoals_tac ctxt sprops = EVERY' (map (subgoal_tac ctxt) sprops);
   350 
   351 fun thin_tac ctxt s = eres_inst_tac ctxt [(("V", 0), s)] thin_rl;
   352 
   353 
   354 (* method syntax *)
   355 
   356 val insts =
   357   Scan.optional
   358     (Args.enum1 "and" (Scan.lift (Args.name -- (Args.$$$ "=" |-- Args.!!! Args.name))) --|
   359       Scan.lift (Args.$$$ "in")) [] -- Attrib.thms;
   360 
   361 fun inst_args f src ctxt =
   362   f ctxt (fst (Method.syntax (Args.goal_spec HEADGOAL -- insts) src ctxt));
   363 
   364 val insts_var =
   365   Scan.optional
   366     (Args.enum1 "and" (Scan.lift (Args.var -- (Args.$$$ "=" |-- Args.!!! Args.name))) --|
   367       Scan.lift (Args.$$$ "in")) [] -- Attrib.thms;
   368 
   369 fun inst_args_var f src ctxt =
   370   f ctxt (fst (Method.syntax (Args.goal_spec HEADGOAL -- insts_var) src ctxt));
   371 
   372 
   373 (* setup *)
   374 
   375 val _ = Context.>> (Context.map_theory
   376   (Method.add_methods
   377    [("rule_tac", inst_args_var res_inst_meth,
   378       "apply rule (dynamic instantiation)"),
   379     ("erule_tac", inst_args_var eres_inst_meth,
   380       "apply rule in elimination manner (dynamic instantiation)"),
   381     ("drule_tac", inst_args_var dres_inst_meth,
   382       "apply rule in destruct manner (dynamic instantiation)"),
   383     ("frule_tac", inst_args_var forw_inst_meth,
   384       "apply rule in forward manner (dynamic instantiation)"),
   385     ("cut_tac", inst_args_var cut_inst_meth,
   386       "cut rule (dynamic instantiation)"),
   387     ("subgoal_tac", Method.goal_args_ctxt (Scan.repeat1 Args.name) subgoals_tac,
   388       "insert subgoal (dynamic instantiation)"),
   389     ("thin_tac", Method.goal_args_ctxt Args.name thin_tac,
   390       "remove premise (dynamic instantiation)")]));
   391 
   392 end;
   393 
   394 end;