# HG changeset patch # User wenzelm # Date 1437949038 -7200 # Node ID f21f70d24844094102e8390cc1b935d38eadc357 # Parent bbcd4ab6d26ee2bf845012852d6b9feae0f85267 added infer_instantiate_vars, which allows inconsistent types for variables, as required for Metis proof reconstruction; diff -r bbcd4ab6d26e -r f21f70d24844 src/HOL/Tools/Metis/metis_reconstruct.ML --- a/src/HOL/Tools/Metis/metis_reconstruct.ML Sun Jul 26 22:26:11 2015 +0200 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Mon Jul 27 00:17:18 2015 +0200 @@ -105,9 +105,8 @@ let val th = EXCLUDED_MIDDLE val [vx] = Term.add_vars (Thm.prop_of th) [] - val substs = [(Thm.cterm_of ctxt (Var vx), Thm.cterm_of ctxt i_atom)] in - cterm_instantiate substs th + infer_instantiate_vars ctxt [(vx, Thm.cterm_of ctxt i_atom)] th end fun assume_inference ctxt type_enc concealed sym_tab atom = @@ -163,7 +162,7 @@ Syntax.string_of_term ctxt (Thm.term_of x) ^ " |-> " ^ Syntax.string_of_term ctxt (Thm.term_of y))))) in - cterm_instantiate substs' i_th + infer_instantiate_vars ctxt (map (apfst (dest_Var o Thm.term_of)) substs') i_th end handle THM (msg, _, _) => raise METIS_RECONSTRUCT ("inst_inference", msg) | ERROR msg => raise METIS_RECONSTRUCT ("inst_inference", msg) @@ -309,7 +308,7 @@ val i_t = singleton (hol_terms_of_metis ctxt type_enc concealed sym_tab) t val _ = trace_msg ctxt (fn () => " term: " ^ Syntax.string_of_term ctxt i_t) val c_t = cterm_incr_types ctxt refl_idx i_t - in cterm_instantiate [(refl_x, c_t)] REFL_THM end + in infer_instantiate_vars ctxt [(dest_Var (Thm.term_of refl_x), c_t)] REFL_THM end (* INFERENCE RULE: EQUALITY *) @@ -375,7 +374,7 @@ map (apply2 (Thm.cterm_of ctxt)) (ListPair.zip (Misc_Legacy.term_vars (Thm.prop_of subst'), [tm_abs, tm_subst, i_tm])) in - cterm_instantiate eq_terms subst' + infer_instantiate_vars ctxt (map (apfst (dest_Var o Thm.term_of)) eq_terms) subst' end val factor = Seq.hd o distinct_subgoals_tac @@ -521,7 +520,7 @@ [] |> try (unify_terms (prem, concl) #> map (apply2 (Thm.cterm_of ctxt))) |> the_default [] (* FIXME *) in - cterm_instantiate t_inst th + infer_instantiate_vars ctxt (map (apfst (dest_Var o Thm.term_of)) t_inst) th end val copy_prem = @{lemma "P ==> (P ==> P ==> Q) ==> Q" by fast} diff -r bbcd4ab6d26e -r f21f70d24844 src/Pure/drule.ML --- a/src/Pure/drule.ML Sun Jul 26 22:26:11 2015 +0200 +++ b/src/Pure/drule.ML Mon Jul 27 00:17:18 2015 +0200 @@ -22,6 +22,7 @@ val implies_intr_list: cterm list -> thm -> thm val instantiate_normalize: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list -> thm -> thm + val infer_instantiate_vars: Proof.context -> ((indexname * typ) * cterm) list -> thm -> thm val infer_instantiate: Proof.context -> (indexname * cterm) list -> thm -> thm val cterm_instantiate: (cterm * cterm) list -> thm -> thm val instantiate': ctyp option list -> cterm option list -> thm -> thm @@ -742,55 +743,58 @@ Thm.adjust_maxidx_thm ~1 (Thm.instantiate instpair th COMP_INCR asm_rl); (*instantiation with type-inference for variables*) +fun infer_instantiate_vars _ [] th = th + | infer_instantiate_vars ctxt args th = + let + val thy = Proof_Context.theory_of ctxt; + + fun infer ((xi, T), cu) (tyenv, maxidx) = + let + val U = Thm.typ_of_cterm cu; + val maxidx' = maxidx + |> Integer.max (#2 xi) + |> Term.maxidx_typ T + |> Integer.max (Thm.maxidx_of_cterm cu); + val (tyenv', maxidx'') = Sign.typ_unify thy (T, U) (tyenv, maxidx') + handle Type.TUNIFY => + let + val t = Var (xi, T); + val u = Thm.term_of cu; + in + raise THM ("infer_instantiate: type " ^ + Syntax.string_of_typ ctxt (Envir.norm_type tyenv T) ^ " of variable " ^ + Syntax.string_of_term ctxt (Term.map_types (Envir.norm_type tyenv) t) ^ + "\ncannot be unified with type " ^ + Syntax.string_of_typ ctxt (Envir.norm_type tyenv U) ^ " of term " ^ + Syntax.string_of_term ctxt (Term.map_types (Envir.norm_type tyenv) u), + 0, [th]) + end; + in (tyenv', maxidx'') end; + + val (tyenv, _) = fold infer args (Vartab.empty, 0); + val instT = + Vartab.fold (fn (xi, (S, T)) => + cons ((xi, S), Thm.ctyp_of ctxt (Envir.norm_type tyenv T))) tyenv []; + val inst = args |> map (fn ((xi, T), cu) => + ((xi, Envir.norm_type tyenv T), + Thm.instantiate_cterm (instT, []) (Thm.transfer_cterm thy cu))); + in instantiate_normalize (instT, inst) th end + handle CTERM (msg, _) => raise THM (msg, 0, [th]) + | TERM (msg, _) => raise THM (msg, 0, [th]) + | TYPE (msg, _, _) => raise THM (msg, 0, [th]); + fun infer_instantiate _ [] th = th | infer_instantiate ctxt args th = let - val thy = Proof_Context.theory_of ctxt; - val vars = Term.add_vars (Thm.full_prop_of th) []; val dups = duplicates (eq_fst op =) vars; val _ = null dups orelse raise THM ("infer_instantiate: inconsistent types for variables " ^ commas_quote (map (Syntax.string_of_term (Config.put show_types true ctxt) o Var) dups), 0, [th]); - - fun infer (xi, cu) (inst, tyenv, maxidx) = - (case AList.lookup (op =) vars xi of - NONE => (inst, tyenv, maxidx) - | SOME T => - let - val U = Thm.typ_of_cterm cu; - val maxidx' = maxidx - |> Integer.max (#2 xi) - |> Term.maxidx_typ T - |> Integer.max (Thm.maxidx_of_cterm cu); - val (tyenv', maxidx'') = Sign.typ_unify thy (T, U) (tyenv, maxidx') - handle Type.TUNIFY => - let - val t = Var (xi, T); - val u = Thm.term_of cu; - in - raise THM ("infer_instantiate: type " ^ - Syntax.string_of_typ ctxt (Envir.norm_type tyenv T) ^ " of variable " ^ - Syntax.string_of_term ctxt (Term.map_types (Envir.norm_type tyenv) t) ^ - "\ncannot be unified with type " ^ - Syntax.string_of_typ ctxt (Envir.norm_type tyenv U) ^ " of term " ^ - Syntax.string_of_term ctxt (Term.map_types (Envir.norm_type tyenv) u), - 0, [th]) - end; - in (((xi, T), cu) :: inst, tyenv', maxidx'') end); - - val (inst0, tyenv, _) = fold infer args ([], Vartab.empty, 0); - val instT = - Vartab.fold (fn (xi, (S, T)) => - cons ((xi, S), Thm.ctyp_of ctxt (Envir.norm_type tyenv T))) tyenv []; - val inst = inst0 |> map (fn ((xi, T), cu) => - ((xi, Envir.norm_type tyenv T), - Thm.instantiate_cterm (instT, []) (Thm.transfer_cterm thy cu))); - in instantiate_normalize (instT, inst) th end - handle CTERM (msg, _) => raise THM (msg, 0, [th]) - | TERM (msg, _) => raise THM (msg, 0, [th]) - | TYPE (msg, _, _) => raise THM (msg, 0, [th]); + val args' = args |> map_filter (fn (xi, cu) => + AList.lookup (op =) vars xi |> Option.map (fn T => ((xi, T), cu))); + in infer_instantiate_vars ctxt args' th end; (*Left-to-right replacements: tpairs = [..., (vi, ti), ...]. Instantiates distinct Vars by terms, inferring type instantiations.*) @@ -848,11 +852,11 @@ fun infer_instantiate' ctxt args th = let - val vars = rev (Term.add_var_names (Thm.full_prop_of th) []); + val vars = rev (Term.add_vars (Thm.full_prop_of th) []); val args' = zip_options vars args handle ListPair.UnequalLengths => raise THM ("infer_instantiate': more instantiations than variables in thm", 0, [th]); - in infer_instantiate ctxt args' th end; + in infer_instantiate_vars ctxt args' th end;