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