added infer_instantiate, which is meant to supersede cterm_instantiate;
authorwenzelm
Sat Jul 25 21:37:09 2015 +0200 (2015-07-25)
changeset 60778682c0dd89b26
parent 60777 ee811a49c8f6
child 60779 c4d3da84d884
added infer_instantiate, which is meant to supersede cterm_instantiate;
src/Pure/drule.ML
     1.1 --- a/src/Pure/drule.ML	Fri Jul 24 22:29:06 2015 +0200
     1.2 +++ b/src/Pure/drule.ML	Sat Jul 25 21:37:09 2015 +0200
     1.3 @@ -22,6 +22,7 @@
     1.4    val implies_intr_list: cterm list -> thm -> thm
     1.5    val instantiate_normalize: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list ->
     1.6      thm -> thm
     1.7 +  val infer_instantiate: Proof.context -> (indexname * cterm) list -> thm -> thm
     1.8    val zero_var_indexes_list: thm list -> thm list
     1.9    val zero_var_indexes: thm -> thm
    1.10    val implies_intr_hyps: thm -> thm
    1.11 @@ -739,6 +740,55 @@
    1.12  fun instantiate_normalize instpair th =
    1.13    Thm.adjust_maxidx_thm ~1 (Thm.instantiate instpair th COMP_INCR asm_rl);
    1.14  
    1.15 +(*instantiation with type-inference for variables*)
    1.16 +fun infer_instantiate _ [] th = th
    1.17 +  | infer_instantiate ctxt args th =
    1.18 +      let
    1.19 +        val thy = Proof_Context.theory_of ctxt;
    1.20 +
    1.21 +        val vars = Term.add_vars (Thm.full_prop_of th) [];
    1.22 +        val dups = duplicates (eq_fst op =) vars;
    1.23 +        val _ = null dups orelse
    1.24 +          raise THM ("infer_instantiate: inconsistent types for variables " ^
    1.25 +            commas_quote (map (Syntax.string_of_term (Config.put show_types true ctxt) o Var) dups),
    1.26 +            0, [th]);
    1.27 +        fun var_type xi =
    1.28 +          (case AList.lookup (op =) vars xi of
    1.29 +            SOME T => T
    1.30 +          | NONE => raise THM ("infer_instantiate: no variable " ^ string_of_indexname xi, 0, [th]));
    1.31 +
    1.32 +        fun infer (xi, cu) (tyenv, maxidx) =
    1.33 +          let
    1.34 +            val T = var_type xi;
    1.35 +            val U = Thm.typ_of_cterm cu;
    1.36 +            val (tyenv', maxidx') =
    1.37 +              Sign.typ_unify thy (T, U)
    1.38 +                (tyenv, maxidx |> Integer.max (#2 xi) |> Integer.max (Thm.maxidx_of_cterm cu))
    1.39 +              handle Type.TUNIFY =>
    1.40 +                let
    1.41 +                  val t = Var (xi, T);
    1.42 +                  val u = Thm.term_of cu;
    1.43 +                in
    1.44 +                  raise TYPE ("Ill-typed instantiation:\nType\n" ^
    1.45 +                    Syntax.string_of_typ ctxt (Envir.norm_type tyenv T) ^
    1.46 +                    "\nof variable " ^
    1.47 +                    Syntax.string_of_term ctxt (Term.map_types (Envir.norm_type tyenv) t) ^
    1.48 +                    "\ncannot be unified with type\n" ^
    1.49 +                    Syntax.string_of_typ ctxt (Envir.norm_type tyenv U) ^ "\nof term " ^
    1.50 +                    Syntax.string_of_term ctxt (Term.map_types (Envir.norm_type tyenv) u),
    1.51 +                    [T, U], [t, u])
    1.52 +                end;
    1.53 +          in (((xi, T), cu), (tyenv', maxidx')) end;
    1.54 +
    1.55 +        val (args', (tyenv, _)) = fold_map infer args (Vartab.empty, 0);
    1.56 +        val instT =
    1.57 +          Vartab.fold (fn (xi, (S, T)) =>
    1.58 +            cons ((xi, S), Thm.ctyp_of ctxt (Envir.norm_type tyenv T))) tyenv [];
    1.59 +        val inst = args' |> map (fn ((xi, T), cu) =>
    1.60 +          ((xi, Envir.norm_type tyenv T),
    1.61 +            Thm.instantiate_cterm (instT, []) (Thm.transfer_cterm thy cu)));
    1.62 +      in instantiate_normalize (instT, inst) th end;
    1.63 +
    1.64  (*Left-to-right replacements: tpairs = [..., (vi, ti), ...].
    1.65    Instantiates distinct Vars by terms, inferring type instantiations.*)
    1.66  local