Rule instantiations -- operations within a rule/subgoal context.
authorwenzelm
Thu Aug 03 17:30:44 2006 +0200 (2006-08-03)
changeset 20336aac494583949
parent 20335 b5eca86ef9cc
child 20337 36e2fae2c68a
Rule instantiations -- operations within a rule/subgoal context.
src/Pure/Isar/rule_insts.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Isar/rule_insts.ML	Thu Aug 03 17:30:44 2006 +0200
     1.3 @@ -0,0 +1,363 @@
     1.4 +(*  Title:      Pure/Isar/rule_insts.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Makarius
     1.7 +
     1.8 +Rule instantiations -- operations within a rule/subgoal context.
     1.9 +*)
    1.10 +
    1.11 +signature RULE_INSTS =
    1.12 +sig
    1.13 +  val bires_inst_tac: bool -> Proof.context -> (indexname * string) list ->
    1.14 +    thm -> int -> tactic
    1.15 +end;
    1.16 +
    1.17 +structure RuleInsts: RULE_INSTS =
    1.18 +struct
    1.19 +
    1.20 +
    1.21 +(** attributes **)
    1.22 +
    1.23 +(* read_instantiate: named instantiation of type and term variables *)
    1.24 +
    1.25 +local
    1.26 +
    1.27 +fun is_tvar (x, _) = (case Symbol.explode x of "'" :: _ => true | _ => false);
    1.28 +
    1.29 +fun error_var msg xi = error (msg ^ Syntax.string_of_vname xi);
    1.30 +
    1.31 +fun the_sort sorts xi = the (sorts xi)
    1.32 +  handle Option.Option => error_var "No such type variable in theorem: " xi;
    1.33 +
    1.34 +fun the_type types xi = the (types xi)
    1.35 +  handle Option.Option => error_var "No such variable in theorem: " xi;
    1.36 +
    1.37 +fun unify_types thy types (xi, u) (unifier, maxidx) =
    1.38 +  let
    1.39 +    val T = the_type types xi;
    1.40 +    val U = Term.fastype_of u;
    1.41 +    val maxidx' = Int.max (maxidx, Int.max (#2 xi, Term.maxidx_of_term u));
    1.42 +  in
    1.43 +    Sign.typ_unify thy (T, U) (unifier, maxidx')
    1.44 +      handle Type.TUNIFY => error_var "Incompatible type for instantiation of " xi
    1.45 +  end;
    1.46 +
    1.47 +fun typ_subst env = apsnd (Term.typ_subst_TVars env);
    1.48 +fun subst env = apsnd (Term.subst_TVars env);
    1.49 +
    1.50 +fun instantiate thy envT env thm =
    1.51 +  let
    1.52 +    val (_, sorts) = Drule.types_sorts thm;
    1.53 +    fun prepT (a, T) = (Thm.ctyp_of thy (TVar (a, the_sort sorts a)), Thm.ctyp_of thy T);
    1.54 +    fun prep (xi, t) = pairself (Thm.cterm_of thy) (Var (xi, Term.fastype_of t), t);
    1.55 +  in
    1.56 +    Drule.instantiate (map prepT (distinct (op =) envT),
    1.57 +      map prep (distinct (fn ((xi, t), (yj, u)) => xi = yj andalso t aconv u) env)) thm
    1.58 +  end;
    1.59 +
    1.60 +in
    1.61 +
    1.62 +fun read_instantiate mixed_insts (context, thm) =
    1.63 +  let
    1.64 +    val thy = Context.theory_of context;
    1.65 +    val ctxt = Context.proof_of context;
    1.66 +
    1.67 +    val (type_insts, term_insts) = List.partition (is_tvar o fst) (map snd mixed_insts);
    1.68 +    val internal_insts = term_insts |> map_filter
    1.69 +      (fn (xi, Args.Term t) => SOME (xi, t)
    1.70 +      | (_, Args.Name _) => NONE
    1.71 +      | (xi, _) => error_var "Term argument expected for " xi);
    1.72 +    val external_insts = term_insts |> map_filter
    1.73 +      (fn (xi, Args.Name s) => SOME (xi, s) | _ => NONE);
    1.74 +
    1.75 +
    1.76 +    (* type instantiations *)
    1.77 +
    1.78 +    val sorts = #2 (Drule.types_sorts thm);
    1.79 +
    1.80 +    fun readT (xi, arg) =
    1.81 +      let
    1.82 +        val S = the_sort sorts xi;
    1.83 +        val T =
    1.84 +          (case arg of
    1.85 +            Args.Name s => ProofContext.read_typ ctxt s
    1.86 +          | Args.Typ T => T
    1.87 +          | _ => error_var "Type argument expected for " xi);
    1.88 +      in
    1.89 +        if Sign.of_sort thy (T, S) then (xi, T)
    1.90 +        else error_var "Incompatible sort for typ instantiation of " xi
    1.91 +      end;
    1.92 +
    1.93 +    val type_insts' = map readT type_insts;
    1.94 +    val thm' = instantiate thy type_insts' [] thm;
    1.95 +
    1.96 +
    1.97 +    (* internal term instantiations *)
    1.98 +
    1.99 +    val types' = #1 (Drule.types_sorts thm');
   1.100 +    val unifier = map (apsnd snd) (Vartab.dest (#1
   1.101 +      (fold (unify_types thy types') internal_insts (Vartab.empty, 0))));
   1.102 +
   1.103 +    val type_insts'' = map (typ_subst unifier) type_insts';
   1.104 +    val internal_insts'' = map (subst unifier) internal_insts;
   1.105 +    val thm'' = instantiate thy unifier internal_insts'' thm';
   1.106 +
   1.107 +
   1.108 +    (* external term instantiations *)
   1.109 +
   1.110 +    val types'' = #1 (Drule.types_sorts thm'');
   1.111 +
   1.112 +    val (xs, ss) = split_list external_insts;
   1.113 +    val Ts = map (the_type types'') xs;
   1.114 +    val (ts, inferred) = ProofContext.read_termTs ctxt (K false)
   1.115 +        (K NONE) (K NONE) (Drule.add_used thm'' []) (ss ~~ Ts);
   1.116 +
   1.117 +    val type_insts''' = map (typ_subst inferred) type_insts'';
   1.118 +    val internal_insts''' = map (subst inferred) internal_insts'';
   1.119 +
   1.120 +    val external_insts''' = xs ~~ ts;
   1.121 +    val term_insts''' = internal_insts''' @ external_insts''';
   1.122 +    val thm''' = instantiate thy inferred external_insts''' thm'';
   1.123 +
   1.124 +
   1.125 +    (* assign internalized values *)
   1.126 +
   1.127 +    val _ =
   1.128 +      mixed_insts |> List.app (fn (arg, (xi, _)) =>
   1.129 +        if is_tvar xi then
   1.130 +          Args.assign (SOME (Args.Typ (the (AList.lookup (op =) type_insts''' xi)))) arg
   1.131 +        else
   1.132 +          Args.assign (SOME (Args.Term (the (AList.lookup (op =) term_insts''' xi)))) arg);
   1.133 +
   1.134 +  in (context, thm''' |> RuleCases.save thm) end;
   1.135 +
   1.136 +end;
   1.137 +
   1.138 +
   1.139 +(* where: named instantiation *)
   1.140 +
   1.141 +local
   1.142 +
   1.143 +val value =
   1.144 +  Args.internal_typ >> Args.Typ ||
   1.145 +  Args.internal_term >> Args.Term ||
   1.146 +  Args.name >> Args.Name;
   1.147 +
   1.148 +val inst = Args.var -- (Args.$$$ "=" |-- Args.ahead -- value)
   1.149 +  >> (fn (xi, (a, v)) => (a, (xi, v)));
   1.150 +
   1.151 +in
   1.152 +
   1.153 +val where_att = Attrib.syntax (Args.and_list (Scan.lift inst) >> read_instantiate);
   1.154 +
   1.155 +end;
   1.156 +
   1.157 +
   1.158 +(* of: positional instantiation (term arguments only) *)
   1.159 +
   1.160 +local
   1.161 +
   1.162 +fun read_instantiate' (args, concl_args) (context, thm) =
   1.163 +  let
   1.164 +    fun zip_vars _ [] = []
   1.165 +      | zip_vars (_ :: xs) ((_, NONE) :: rest) = zip_vars xs rest
   1.166 +      | zip_vars ((x, _) :: xs) ((arg, SOME t) :: rest) = (arg, (x, t)) :: zip_vars xs rest
   1.167 +      | zip_vars [] _ = error "More instantiations than variables in theorem";
   1.168 +    val insts =
   1.169 +      zip_vars (rev (Term.add_vars (Thm.full_prop_of thm) [])) args @
   1.170 +      zip_vars (rev (Term.add_vars (Thm.concl_of thm) [])) concl_args;
   1.171 +  in read_instantiate insts (context, thm) end;
   1.172 +
   1.173 +val value =
   1.174 +  Args.internal_term >> Args.Term ||
   1.175 +  Args.name >> Args.Name;
   1.176 +
   1.177 +val inst = Args.ahead -- Args.maybe value;
   1.178 +val concl = Args.$$$ "concl" -- Args.colon;
   1.179 +
   1.180 +val insts =
   1.181 +  Scan.repeat (Scan.unless concl inst) --
   1.182 +  Scan.optional (concl |-- Scan.repeat inst) [];
   1.183 +
   1.184 +in
   1.185 +
   1.186 +val of_att = Attrib.syntax (Scan.lift insts >> read_instantiate');
   1.187 +
   1.188 +end;
   1.189 +
   1.190 +
   1.191 +(* setup *)
   1.192 +
   1.193 +val _ = Context.add_setup (Attrib.add_attributes
   1.194 + [("where", where_att, "named instantiation of theorem"),
   1.195 +  ("of", of_att, "rule applied to terms")]);
   1.196 +
   1.197 +
   1.198 +
   1.199 +(** methods **)
   1.200 +
   1.201 +(* rule_tac etc. -- refer to dynamic goal state!! *)   (* FIXME cleanup!! *)
   1.202 +
   1.203 +fun bires_inst_tac bires_flag ctxt insts thm =
   1.204 +  let
   1.205 +    val thy = ProofContext.theory_of ctxt;
   1.206 +    (* Separate type and term insts *)
   1.207 +    fun has_type_var ((x, _), _) = (case Symbol.explode x of
   1.208 +          "'"::cs => true | cs => false);
   1.209 +    val Tinsts = List.filter has_type_var insts;
   1.210 +    val tinsts = filter_out has_type_var insts;
   1.211 +    (* Tactic *)
   1.212 +    fun tac i st =
   1.213 +      let
   1.214 +        (* Preprocess state: extract environment information:
   1.215 +           - variables and their types
   1.216 +           - type variables and their sorts
   1.217 +           - parameters and their types *)
   1.218 +        val (types, sorts) = types_sorts st;
   1.219 +    (* Process type insts: Tinsts_env *)
   1.220 +    fun absent xi = error
   1.221 +          ("No such variable in theorem: " ^ Syntax.string_of_vname xi);
   1.222 +    val (rtypes, rsorts) = types_sorts thm;
   1.223 +    fun readT (xi, s) =
   1.224 +        let val S = case rsorts xi of SOME S => S | NONE => absent xi;
   1.225 +            val T = Sign.read_typ (thy, sorts) s;
   1.226 +            val U = TVar (xi, S);
   1.227 +        in if Sign.typ_instance thy (T, U) then (U, T)
   1.228 +           else error
   1.229 +             ("Instantiation of " ^ Syntax.string_of_vname xi ^ " fails")
   1.230 +        end;
   1.231 +    val Tinsts_env = map readT Tinsts;
   1.232 +    (* Preprocess rule: extract vars and their types, apply Tinsts *)
   1.233 +    fun get_typ xi =
   1.234 +      (case rtypes xi of
   1.235 +           SOME T => typ_subst_atomic Tinsts_env T
   1.236 +         | NONE => absent xi);
   1.237 +    val (xis, ss) = Library.split_list tinsts;
   1.238 +    val Ts = map get_typ xis;
   1.239 +        val (_, _, Bi, _) = dest_state(st,i)
   1.240 +        val params = Logic.strip_params Bi
   1.241 +                             (* params of subgoal i as string typ pairs *)
   1.242 +        val params = rev(Term.rename_wrt_term Bi params)
   1.243 +                           (* as they are printed: bound variables with *)
   1.244 +                           (* the same name are renamed during printing *)
   1.245 +        fun types' (a, ~1) = (case AList.lookup (op =) params a of
   1.246 +                NONE => types (a, ~1)
   1.247 +              | some => some)
   1.248 +          | types' xi = types xi;
   1.249 +        fun internal x = is_some (types' (x, ~1));
   1.250 +        val used = Drule.add_used thm (Drule.add_used st []);
   1.251 +        val (ts, envT) =
   1.252 +          ProofContext.read_termTs_schematic ctxt internal types' sorts used (ss ~~ Ts);
   1.253 +        val envT' = map (fn (ixn, T) =>
   1.254 +          (TVar (ixn, the (rsorts ixn)), T)) envT @ Tinsts_env;
   1.255 +        val cenv =
   1.256 +          map
   1.257 +            (fn (xi, t) =>
   1.258 +              pairself (Thm.cterm_of thy) (Var (xi, fastype_of t), t))
   1.259 +            (distinct
   1.260 +              (fn ((x1, t1), (x2, t2)) => x1 = x2 andalso t1 aconv t2)
   1.261 +              (xis ~~ ts));
   1.262 +        (* Lift and instantiate rule *)
   1.263 +        val {maxidx, ...} = rep_thm st;
   1.264 +        val paramTs = map #2 params
   1.265 +        and inc = maxidx+1
   1.266 +        fun liftvar (Var ((a,j), T)) =
   1.267 +              Var((a, j+inc), paramTs ---> Logic.incr_tvar inc T)
   1.268 +          | liftvar t = raise TERM("Variable expected", [t]);
   1.269 +        fun liftterm t = list_abs_free
   1.270 +              (params, Logic.incr_indexes(paramTs,inc) t)
   1.271 +        fun liftpair (cv,ct) =
   1.272 +              (cterm_fun liftvar cv, cterm_fun liftterm ct)
   1.273 +        val lifttvar = pairself (ctyp_of thy o Logic.incr_tvar inc);
   1.274 +        val rule = Drule.instantiate
   1.275 +              (map lifttvar envT', map liftpair cenv)
   1.276 +              (Thm.lift_rule (Thm.cprem_of st i) thm)
   1.277 +      in
   1.278 +        if i > nprems_of st then no_tac st
   1.279 +        else st |>
   1.280 +          compose_tac (bires_flag, rule, nprems_of thm) i
   1.281 +      end
   1.282 +           handle TERM (msg,_)   => (warning msg; no_tac st)
   1.283 +                | THM  (msg,_,_) => (warning msg; no_tac st);
   1.284 +  in tac end;
   1.285 +
   1.286 +local
   1.287 +
   1.288 +fun gen_inst _ tac _ (quant, ([], thms)) =
   1.289 +      Method.METHOD (fn facts => quant (Method.insert_tac facts THEN' tac thms))
   1.290 +  | gen_inst inst_tac _ ctxt (quant, (insts, [thm])) =
   1.291 +      Method.METHOD (fn facts =>
   1.292 +        quant (Method.insert_tac facts THEN' inst_tac ctxt insts thm))
   1.293 +  | gen_inst _ _ _ _ = error "Cannot have instantiations with multiple rules";
   1.294 +
   1.295 +in
   1.296 +
   1.297 +val res_inst_meth = gen_inst (bires_inst_tac false) Tactic.resolve_tac;
   1.298 +
   1.299 +val eres_inst_meth = gen_inst (bires_inst_tac true) Tactic.eresolve_tac;
   1.300 +
   1.301 +val cut_inst_meth =
   1.302 +  gen_inst
   1.303 +    (fn ctxt => fn insts => bires_inst_tac false ctxt insts o Tactic.make_elim_preserve)
   1.304 +    Tactic.cut_rules_tac;
   1.305 +
   1.306 +val dres_inst_meth =
   1.307 +  gen_inst
   1.308 +    (fn ctxt => fn insts => bires_inst_tac true ctxt insts o Tactic.make_elim_preserve)
   1.309 +    Tactic.dresolve_tac;
   1.310 +
   1.311 +val forw_inst_meth =
   1.312 +  gen_inst
   1.313 +    (fn ctxt => fn insts => fn rule =>
   1.314 +       bires_inst_tac false ctxt insts (Tactic.make_elim_preserve rule) THEN'
   1.315 +       assume_tac)
   1.316 +    Tactic.forward_tac;
   1.317 +
   1.318 +fun subgoal_tac ctxt sprop =
   1.319 +  DETERM o bires_inst_tac false ctxt [(("psi", 0), sprop)] cut_rl;
   1.320 +
   1.321 +fun subgoals_tac ctxt sprops = EVERY' (map (subgoal_tac ctxt) sprops);
   1.322 +
   1.323 +fun thin_tac ctxt s =
   1.324 +  bires_inst_tac true ctxt [(("V", 0), s)] thin_rl;
   1.325 +
   1.326 +
   1.327 +(* method syntax *)
   1.328 +
   1.329 +val insts =
   1.330 +  Scan.optional
   1.331 +    (Args.enum1 "and" (Scan.lift (Args.name -- (Args.$$$ "=" |-- Args.!!! Args.name))) --|
   1.332 +      Scan.lift (Args.$$$ "in")) [] -- Attrib.thms;
   1.333 +
   1.334 +fun inst_args f src ctxt =
   1.335 +  f ctxt (#2 (Method.syntax (Args.goal_spec HEADGOAL -- insts) src ctxt));
   1.336 +
   1.337 +val insts_var =
   1.338 +  Scan.optional
   1.339 +    (Args.enum1 "and" (Scan.lift (Args.var -- (Args.$$$ "=" |-- Args.!!! Args.name))) --|
   1.340 +      Scan.lift (Args.$$$ "in")) [] -- Attrib.thms;
   1.341 +
   1.342 +fun inst_args_var f src ctxt =
   1.343 +  f ctxt (#2 (Method.syntax (Args.goal_spec HEADGOAL -- insts_var) src ctxt));
   1.344 +
   1.345 +
   1.346 +(* setup *)
   1.347 +
   1.348 +val _ = Context.add_setup (Method.add_methods
   1.349 + [("rule_tac", inst_args_var res_inst_meth,
   1.350 +    "apply rule (dynamic instantiation)"),
   1.351 +  ("erule_tac", inst_args_var eres_inst_meth,
   1.352 +    "apply rule in elimination manner (dynamic instantiation)"),
   1.353 +  ("drule_tac", inst_args_var dres_inst_meth,
   1.354 +    "apply rule in destruct manner (dynamic instantiation)"),
   1.355 +  ("frule_tac", inst_args_var forw_inst_meth,
   1.356 +    "apply rule in forward manner (dynamic instantiation)"),
   1.357 +  ("cut_tac", inst_args_var cut_inst_meth,
   1.358 +    "cut rule (dynamic instantiation)"),
   1.359 +  ("subgoal_tac", Method.goal_args_ctxt (Scan.repeat1 Args.name) subgoals_tac,
   1.360 +    "insert subgoal (dynamic instantiation)"),
   1.361 +  ("thin_tac", Method.goal_args_ctxt Args.name thin_tac,
   1.362 +    "remove premise (dynamic instantiation)")]);
   1.363 +
   1.364 +end;
   1.365 +
   1.366 +end;