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