simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
--- a/NEWS Fri Jul 03 16:19:45 2015 +0200
+++ b/NEWS Sun Jul 05 15:02:30 2015 +0200
@@ -234,6 +234,12 @@
command. Minor INCOMPATIBILITY, use 'function' instead.
+** ML **
+
+* Thm.instantiate (and derivatives) no longer require the LHS of the
+instantiation to be certified: plain variables are given directly.
+
+
New in Isabelle2015 (May 2015)
------------------------------
--- a/src/Doc/Implementation/Logic.thy Fri Jul 03 16:19:45 2015 +0200
+++ b/src/Doc/Implementation/Logic.thy Sun Jul 05 15:02:30 2015 +0200
@@ -656,7 +656,8 @@
@{index_ML Thm.implies_intr: "cterm -> thm -> thm"} \\
@{index_ML Thm.implies_elim: "thm -> thm -> thm"} \\
@{index_ML Thm.generalize: "string list * string list -> int -> thm -> thm"} \\
- @{index_ML Thm.instantiate: "(ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm"} \\
+ @{index_ML Thm.instantiate: "((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list
+ -> thm -> thm"} \\
@{index_ML Thm.add_axiom: "Proof.context ->
binding * term -> theory -> (string * thm) * theory"} \\
@{index_ML Thm.add_oracle: "binding * ('a -> cterm) -> theory ->
--- a/src/Doc/Implementation/Proof.thy Fri Jul 03 16:19:45 2015 +0200
+++ b/src/Doc/Implementation/Proof.thy Sun Jul 05 15:02:30 2015 +0200
@@ -108,7 +108,7 @@
@{index_ML Variable.export: "Proof.context -> Proof.context -> thm list -> thm list"} \\
@{index_ML Variable.polymorphic: "Proof.context -> term list -> term list"} \\
@{index_ML Variable.import: "bool -> thm list -> Proof.context ->
- (((ctyp * ctyp) list * (cterm * cterm) list) * thm list) * Proof.context"} \\
+ ((((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list) * thm list) * Proof.context"} \\
@{index_ML Variable.focus: "term -> Proof.context ->
((string * (string * typ)) list * term) * Proof.context"} \\
\end{mldecls}
--- a/src/HOL/Decision_Procs/approximation.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Decision_Procs/approximation.ML Sun Jul 05 15:02:30 2015 +0200
@@ -78,9 +78,9 @@
|> HOLogic.mk_list @{typ nat}
|> Thm.cterm_of ctxt
in
- (rtac (Thm.instantiate ([], [(@{cpat "?n::nat"}, n),
- (@{cpat "?prec::nat"}, p),
- (@{cpat "?ss::nat list"}, s)])
+ (rtac (Thm.instantiate ([], [((("n", 0), @{typ nat}), n),
+ ((("prec", 0), @{typ nat}), p),
+ ((("ss", 0), @{typ "nat list"}), s)])
@{thm "approx_form"}) i
THEN simp_tac (put_simpset (simpset_of @{context}) ctxt) i) st
end
@@ -95,9 +95,9 @@
val s = vs |> map lookup_splitting |> hd
|> Thm.cterm_of ctxt
in
- rtac (Thm.instantiate ([], [(@{cpat "?s::nat"}, s),
- (@{cpat "?t::nat"}, t),
- (@{cpat "?prec::nat"}, p)])
+ rtac (Thm.instantiate ([], [((("s", 0), @{typ nat}), s),
+ ((("t", 0), @{typ nat}), t),
+ ((("prec", 0), @{typ nat}), p)])
@{thm "approx_tse_form"}) i st
end
end
--- a/src/HOL/Decision_Procs/ferrante_rackoff.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML Sun Jul 05 15:02:30 2015 +0200
@@ -58,6 +58,7 @@
funpow 2 (Thm.dest_arg o snd o Thm.dest_abs NONE)
(funpow 4 Thm.dest_arg (Thm.cprop_of (hd minf)))
|> Thm.dest_binop |> apply2 Thm.dest_binop |> apfst (apply2 Thm.dest_fun)
+ |> apply2 (apply2 (dest_Var o Thm.term_of))
fun myfwd (th1, th2, th3, th4, th5) p1 p2
[(th_1,th_2,th_3,th_4,th_5), (th_1',th_2',th_3',th_4',th_5')] =
@@ -73,7 +74,7 @@
in (fw true th1 th_1 th_1', fw false th2 th_2 th_2',
fw true th3 th_3 th_3', fw false th4 th_4 th_4', fw true th5 th_5 th_5')
end
- val U_v = (Thm.dest_arg o Thm.dest_arg o Thm.dest_arg1) (Thm.cprop_of qe)
+ val U_v = dest_Var (Thm.term_of (Thm.dest_arg (Thm.dest_arg (Thm.dest_arg1 (Thm.cprop_of qe)))))
fun main vs p =
let
val ((xn,ce),(x,fm)) = (case Thm.term_of p of
--- a/src/HOL/Eisbach/eisbach_rule_insts.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Eisbach/eisbach_rule_insts.ML Sun Jul 05 15:02:30 2015 +0200
@@ -57,7 +57,7 @@
fun add_inst (xi, t) (Ts, ts) =
(case AList.lookup (op =) tyvars xi of
- SOME S => ((certT (TVar (xi, S)), certT (Logic.dest_type t)) :: Ts, ts)
+ SOME S => (((xi, S), certT (Logic.dest_type t)) :: Ts, ts)
| NONE =>
(case AList.lookup (op =) tvars xi of
SOME T => (Ts, (cert (Var (xi, T)), cert t) :: ts)
--- a/src/HOL/Eisbach/match_method.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Eisbach/match_method.ML Sun Jul 05 15:02:30 2015 +0200
@@ -440,10 +440,9 @@
val focus_schematics = #2 o Focus_Data.get;
-fun add_focus_schematics cterms =
+fun add_focus_schematics schematics =
(Focus_Data.map o @{apply 3(2)})
- (fold (fn (Var (xi, T), t) => Vartab.update_new (xi, (T, t)))
- (map (apply2 Thm.term_of) cterms));
+ (fold (fn ((xi, T), ct) => Vartab.update_new (xi, (T, Thm.term_of ct))) schematics);
(* focus params *)
--- a/src/HOL/Import/import_rule.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Import/import_rule.ML Sun Jul 05 15:02:30 2015 +0200
@@ -161,11 +161,9 @@
let
val tvars = Term.add_tvars (Thm.prop_of thm) []
val tfrees = map (fn ((t, _), s) => TFree (t, s)) tvars
- val tvars = map TVar tvars
val thy = Thm.theory_of_thm thm
- fun inst ty = Thm.global_ctyp_of thy ty
in
- Thm.instantiate ((map inst tvars ~~ map inst tfrees), []) thm
+ Thm.instantiate ((tvars ~~ map (Thm.global_ctyp_of thy) tfrees), []) thm
end
fun def' constname rhs thy =
@@ -264,11 +262,12 @@
val tys_before = Term.add_tfrees (Thm.prop_of th) []
val th1 = Thm.varifyT_global th
val tys_after = Term.add_tvars (Thm.prop_of th1) []
- val tyinst = map2 (fn bef => fn iS =>
- (case try (assoc (TFree bef)) lambda of
- SOME cty => (Thm.global_ctyp_of thy (TVar iS), cty)
- | NONE => (Thm.global_ctyp_of thy (TVar iS), Thm.global_ctyp_of thy (TFree bef))
- )) tys_before tys_after
+ val tyinst =
+ map2 (fn bef => fn iS =>
+ (case try (assoc (TFree bef)) lambda of
+ SOME cty => (iS, cty)
+ | NONE => (iS, Thm.global_ctyp_of thy (TFree bef))))
+ tys_before tys_after
in
Thm.instantiate (tyinst,[]) th1
end
@@ -334,9 +333,7 @@
val tns = map (fn (_, _) => "'") tvs
val nms = fst (fold_map Name.variant tns (Variable.names_of ctxt))
val vs = map TVar ((nms ~~ (map (snd o fst) tvs)) ~~ (map snd tvs))
- val cvs = map (Thm.ctyp_of ctxt) vs
- val ctvs = map (Thm.ctyp_of ctxt) (map TVar tvs)
- val thm' = Thm.instantiate ((ctvs ~~ cvs), []) thm
+ val thm' = Thm.instantiate ((tvs ~~ map (Thm.ctyp_of ctxt) vs), []) thm
in
snd (Global_Theory.add_thm ((binding, thm'), []) thy)
end
--- a/src/HOL/Library/Old_SMT/old_smt_normalize.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Library/Old_SMT/old_smt_normalize.ML Sun Jul 05 15:02:30 2015 +0200
@@ -34,7 +34,7 @@
fun inst f ct thm =
let val cv = f (Drule.strip_imp_concl (Thm.cprop_of thm))
- in Thm.instantiate ([], [(cv, ct)]) thm end
+ in Thm.instantiate ([], [(dest_Var (Thm.term_of cv), ct)]) thm end
in
fun instantiate_elim thm =
@@ -215,7 +215,7 @@
fun insert_trigger_conv [] ct = Conv.all_conv ct
| insert_trigger_conv ctss ct =
let val (ctr, cp) = Thm.dest_binop (Thm.rhs_of trigger_eq) ||> rpair ct
- in Thm.instantiate ([], [cp, (ctr, mk_trigger ctss)]) trigger_eq end
+ in Thm.instantiate ([], map (apfst (dest_Var o Thm.term_of)) [cp, (ctr, mk_trigger ctss)]) trigger_eq end
fun infer_trigger_eq_conv outer_ctxt (ctxt, cvs) ct =
let
@@ -298,7 +298,8 @@
fun mk_weight_eq w =
let val cv = Thm.dest_arg1 (Thm.rhs_of weight_eq)
in
- Thm.instantiate ([], [(cv, Numeral.mk_cnumber @{ctyp int} w)]) weight_eq
+ Thm.instantiate ([], [(dest_Var (Thm.term_of cv), Numeral.mk_cnumber @{ctyp int} w)])
+ weight_eq
end
fun add_weight_conv NONE _ = Conv.all_conv
--- a/src/HOL/Library/Old_SMT/old_smt_utils.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Library/Old_SMT/old_smt_utils.ML Sun Jul 05 15:02:30 2015 +0200
@@ -152,7 +152,7 @@
val destT1 = hd o Thm.dest_ctyp
val destT2 = hd o tl o Thm.dest_ctyp
-fun instTs cUs (cTs, ct) = Thm.instantiate_cterm (cTs ~~ cUs, []) ct
+fun instTs cUs (cTs, ct) = Thm.instantiate_cterm (map (dest_TVar o Thm.typ_of) cTs ~~ cUs, []) ct
fun instT cU (cT, ct) = instTs [cU] ([cT], ct)
fun instT' ct = instT (Thm.ctyp_of_cterm ct)
--- a/src/HOL/Library/Old_SMT/old_z3_proof_literals.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Library/Old_SMT/old_z3_proof_literals.ML Sun Jul 05 15:02:30 2015 +0200
@@ -195,7 +195,9 @@
fun on_cprop f thm = f (Thm.cprop_of thm)
fun precomp2 f g thm = (on_cprem 1 f thm, on_cprem 2 g thm, f, g, thm)
fun comp2 (cv1, cv2, f, g, rule) thm1 thm2 =
- Thm.instantiate ([], [(cv1, on_cprop f thm1), (cv2, on_cprop g thm2)]) rule
+ Thm.instantiate ([],
+ [(dest_Var (Thm.term_of cv1), on_cprop f thm1),
+ (dest_Var (Thm.term_of cv2), on_cprop g thm2)]) rule
|> Old_Z3_Proof_Tools.discharge thm1 |> Old_Z3_Proof_Tools.discharge thm2
fun d1 ct = Thm.dest_arg ct and d2 ct = Thm.dest_arg (Thm.dest_arg ct)
@@ -303,7 +305,7 @@
|> (fn (nlit, plit) => nlit COMP (plit COMP contra_rule)))
end
- val falseE_v = Thm.dest_arg (Thm.dest_arg (Thm.cprop_of @{thm FalseE}))
+ val falseE_v = dest_Var (Thm.term_of (Thm.dest_arg (Thm.dest_arg (Thm.cprop_of @{thm FalseE}))))
fun contra_right ct = Thm.instantiate ([], [(falseE_v, ct)]) @{thm FalseE}
in
fun contradict conj ct =
--- a/src/HOL/Library/Old_SMT/old_z3_proof_parser.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Library/Old_SMT/old_z3_proof_parser.ML Sun Jul 05 15:02:30 2015 +0200
@@ -109,7 +109,7 @@
val max = fold (Integer.max o fst) vars 0
val ns = fst (Variable.variant_fixes (replicate (max + 1) var_prefix) ctxt)
fun mk (i, v) =
- (v, Thm.cterm_of ctxt (Free (nth ns i, Thm.typ_of_cterm v)))
+ (dest_Var (Thm.term_of v), Thm.cterm_of ctxt (Free (nth ns i, Thm.typ_of_cterm v)))
in map mk vars end
fun close ctxt (ct, vars) =
@@ -161,7 +161,10 @@
if null vars then ([], vars)
else fold part vars ([], [])
- in (Thm.instantiate_cterm ([], inst) ct, (maxidx', vars' @ all_vars)) end
+ in
+ (Thm.instantiate_cterm ([], map (apfst (dest_Var o Thm.term_of)) inst) ct,
+ (maxidx', vars' @ all_vars))
+ end
in
fun mk_fun f ts =
let val (cts, (_, vars)) = fold_map prep ts (0, [])
--- a/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML Sun Jul 05 15:02:30 2015 +0200
@@ -625,7 +625,10 @@
val vs = frees_of ctxt (Thm.term_of ct)
val (thm, ctxt') = f (fold_rev mk_forall vs ct) ctxt
val vars_of = get_vars Term.add_vars Var (K true) ctxt'
- in (Thm.instantiate ([], vars_of (Thm.prop_of thm) ~~ vs) thm, ctxt') end
+ in
+ (Thm.instantiate ([], map (dest_Var o Thm.term_of) (vars_of (Thm.prop_of thm)) ~~ vs) thm,
+ ctxt')
+ end
val sk_rules = @{lemma
"c = (SOME x. P x) ==> (EX x. P x) = P c"
--- a/src/HOL/Library/Old_SMT/old_z3_proof_tools.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Library/Old_SMT/old_z3_proof_tools.ML Sun Jul 05 15:02:30 2015 +0200
@@ -27,7 +27,7 @@
(Proof.context -> cterm -> thm) -> cterm -> thm
(*a faster COMP*)
- type compose_data
+ type compose_data = cterm list * (cterm -> cterm list) * thm
val precompose: (cterm -> cterm list) -> thm -> compose_data
val precompose2: (cterm -> cterm * cterm) -> thm -> compose_data
val compose: compose_data -> thm -> thm
@@ -257,11 +257,11 @@
fun list2 (x, y) = [x, y]
-fun precompose f rule = (f (Thm.cprem_of rule 1), f, rule)
-fun precompose2 f rule = precompose (list2 o f) rule
+fun precompose f rule : compose_data = (f (Thm.cprem_of rule 1), f, rule)
+fun precompose2 f rule : compose_data = precompose (list2 o f) rule
fun compose (cvs, f, rule) thm =
- discharge thm (Thm.instantiate ([], cvs ~~ f (Thm.cprop_of thm)) rule)
+ discharge thm (Thm.instantiate ([], map (dest_Var o Thm.term_of) cvs ~~ f (Thm.cprop_of thm)) rule)
--- a/src/HOL/Library/cconv.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Library/cconv.ML Sun Jul 05 15:02:30 2015 +0200
@@ -182,7 +182,7 @@
((if n = 1 then fun_cconv else I) o arg_cconv) (prems_cconv (n-1) cv) ct
| _ => cv ct)
-fun inst_imp_cong ct = Thm.instantiate ([], [(@{cpat "?A :: prop"}, ct)]) Drule.imp_cong
+fun inst_imp_cong ct = Thm.instantiate ([], [((("A", 0), propT), ct)]) Drule.imp_cong
(*rewrite B in A1 \<Longrightarrow> ... \<Longrightarrow> An \<Longrightarrow> B*)
fun concl_cconv 0 cv ct = cv ct
@@ -202,10 +202,10 @@
NONE => (As, B)
| SOME (A,B) => strip_prems (i - 1) (A::As) B
val (prem, (prems, concl)) = ct |> Thm.dest_implies ||> strip_prems n []
- val rewr_imp_concl = Thm.instantiate ([], [(@{cpat "?C :: prop"}, concl)]) @{thm rewr_imp}
+ val rewr_imp_concl = Thm.instantiate ([], [((("C", 0), propT), concl)]) @{thm rewr_imp}
val th1 = cv prem RS rewr_imp_concl
val nprems = Thm.nprems_of th1
- fun inst_cut_rl ct = Thm.instantiate ([], [(@{cpat "?psi :: prop"}, ct)]) cut_rl
+ fun inst_cut_rl ct = Thm.instantiate ([], [((("psi", 0), propT), ct)]) cut_rl
fun f p th = (th RS inst_cut_rl p)
|> Conv.fconv_rule (Conv.concl_conv nprems (Conv.rewr_conv @{thm imp_cong_eq}))
in fold f prems th1 end
--- a/src/HOL/Library/old_recdef.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Library/old_recdef.ML Sun Jul 05 15:02:30 2015 +0200
@@ -304,15 +304,15 @@
(Pv, Dv,
Sign.typ_match thy (Dty, ty) Vartab.empty)
| _ => error "not a valid case thm";
- val type_cinsts = map (fn (ixn, (S, T)) => apply2 (Thm.ctyp_of ctxt) (TVar (ixn, S), T))
+ val type_cinsts = map (fn (ixn, (S, T)) => ((ixn, S), Thm.ctyp_of ctxt T))
(Vartab.dest type_insts);
- val cPv = Thm.cterm_of ctxt (Envir.subst_term_types type_insts Pv);
- val cDv = Thm.cterm_of ctxt (Envir.subst_term_types type_insts Dv);
+ val Pv = dest_Var (Envir.subst_term_types type_insts Pv);
+ val Dv = dest_Var (Envir.subst_term_types type_insts Dv);
in
Conv.fconv_rule Drule.beta_eta_conversion
(case_thm
|> Thm.instantiate (type_cinsts, [])
- |> Thm.instantiate ([], [(cPv, abs_ct), (cDv, free_ct)]))
+ |> Thm.instantiate ([], [(Pv, abs_ct), (Dv, free_ct)]))
end;
@@ -1124,11 +1124,11 @@
local (* this is fragile *)
val prop = Thm.prop_of spec
val x = hd (tl (Misc_Legacy.term_vars prop))
- val cTV = Thm.ctyp_of @{context} (type_of x)
+ val TV = dest_TVar (type_of x)
val gspec = Thm.forall_intr (Thm.cterm_of @{context} x) spec
in
fun SPEC tm thm =
- let val gspec' = Drule.instantiate_normalize ([(cTV, Thm.ctyp_of_cterm tm)], []) gspec
+ let val gspec' = Drule.instantiate_normalize ([(TV, Thm.ctyp_of_cterm tm)], []) gspec
in thm RS (Thm.forall_elim tm gspec') end
end;
@@ -1141,11 +1141,11 @@
local
val prop = Thm.prop_of allI
val [P] = Misc_Legacy.add_term_vars (prop, [])
- fun cty_theta ctxt = map (fn (i, (S, ty)) => apply2 (Thm.ctyp_of ctxt) (TVar (i, S), ty))
+ fun cty_theta ctxt = map (fn (i, (S, ty)) => ((i, S), Thm.ctyp_of ctxt ty))
fun ctm_theta ctxt =
map (fn (i, (_, tm2)) =>
let val ctm2 = Thm.cterm_of ctxt tm2
- in (Thm.cterm_of ctxt (Var (i, Thm.typ_of_cterm ctm2)), ctm2) end)
+ in ((i, Thm.typ_of_cterm ctm2), ctm2) end)
fun certify ctxt (ty_theta,tm_theta) =
(cty_theta ctxt (Vartab.dest ty_theta),
ctm_theta ctxt (Vartab.dest tm_theta))
--- a/src/HOL/Library/positivstellensatz.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Library/positivstellensatz.ML Sun Jul 05 15:02:30 2015 +0200
@@ -483,7 +483,7 @@
fun real_not_eq_conv ct =
let
val (l,r) = dest_eq (Thm.dest_arg ct)
- val th = Thm.instantiate ([],[(@{cpat "?x::real"},l),(@{cpat "?y::real"},r)]) neq_th
+ val th = Thm.instantiate ([],[((("x", 0), @{typ real}),l),((("y", 0), @{typ real}),r)]) neq_th
val th_p = poly_conv(Thm.dest_arg(Thm.dest_arg1(Thm.rhs_of th)))
val th_x = Drule.arg_cong_rule @{cterm "uminus :: real => _"} th_p
val th_n = fconv_rule (arg_conv poly_neg_conv) th_x
@@ -729,9 +729,9 @@
val pth_max = instantiate' [SOME @{ctyp real}] [] max_split
val pth_min = instantiate' [SOME @{ctyp real}] [] min_split
val abs_tm = @{cterm "abs :: real => _"}
- val p_tm = @{cpat "?P :: real => bool"}
- val x_tm = @{cpat "?x :: real"}
- val y_tm = @{cpat "?y::real"}
+ val p_v = (("P", 0), @{typ "real \<Rightarrow> bool"})
+ val x_v = (("x", 0), @{typ real})
+ val y_v = (("y", 0), @{typ real})
val is_max = is_binop @{cterm "max :: real => _"}
val is_min = is_binop @{cterm "min :: real => _"}
fun is_abs t = is_comb t andalso Thm.dest_fun t aconvc abs_tm
@@ -746,16 +746,16 @@
val elim_abs = eliminate_construct is_abs
(fn p => fn ax =>
- Thm.instantiate ([], [(p_tm,p), (x_tm, Thm.dest_arg ax)]) pth_abs)
+ Thm.instantiate ([], [(p_v,p), (x_v, Thm.dest_arg ax)]) pth_abs)
val elim_max = eliminate_construct is_max
(fn p => fn ax =>
let val (ax,y) = Thm.dest_comb ax
- in Thm.instantiate ([], [(p_tm,p), (x_tm, Thm.dest_arg ax), (y_tm,y)])
+ in Thm.instantiate ([], [(p_v,p), (x_v, Thm.dest_arg ax), (y_v,y)])
pth_max end)
val elim_min = eliminate_construct is_min
(fn p => fn ax =>
let val (ax,y) = Thm.dest_comb ax
- in Thm.instantiate ([], [(p_tm,p), (x_tm, Thm.dest_arg ax), (y_tm,y)])
+ in Thm.instantiate ([], [(p_v,p), (x_v, Thm.dest_arg ax), (y_v,y)])
pth_min end)
in first_conv [elim_abs, elim_max, elim_min, all_conv]
end;
--- a/src/HOL/Library/rewrite.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Library/rewrite.ML Sun Jul 05 15:02:30 2015 +0200
@@ -265,15 +265,13 @@
let
fun instantiate_normalize_env ctxt env thm =
let
- fun certs f = map (apply2 (f ctxt))
val prop = Thm.prop_of thm
val norm_type = Envir.norm_type o Envir.type_env
val insts = Term.add_vars prop []
- |> map (fn x as (s,T) => (Var (s, norm_type env T), Envir.norm_term env (Var x)))
- |> certs Thm.cterm_of
+ |> map (fn x as (s, T) =>
+ ((s, norm_type env T), Thm.cterm_of ctxt (Envir.norm_term env (Var x))))
val tyinsts = Term.add_tvars prop []
- |> map (fn x => (TVar x, norm_type env (TVar x)))
- |> certs Thm.ctyp_of
+ |> map (fn x => (x, Thm.ctyp_of ctxt (norm_type env (TVar x))))
in Drule.instantiate_normalize (tyinsts, insts) thm end
fun unify_with_rhs context to env thm =
--- a/src/HOL/Matrix_LP/Compute_Oracle/linker.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Matrix_LP/Compute_Oracle/linker.ML Sun Jul 05 15:02:30 2015 +0200
@@ -315,8 +315,8 @@
end
fun conv_subst thy (subst : Type.tyenv) =
- map (fn (iname, (sort, ty)) => (Thm.global_ctyp_of thy (TVar (iname, sort)), Thm.global_ctyp_of thy ty))
- (Vartab.dest subst)
+ map (fn (iname, (sort, ty)) => ((iname, sort), Thm.global_ctyp_of thy ty))
+ (Vartab.dest subst)
fun add_monos thy monocs pats ths =
let
--- a/src/HOL/Multivariate_Analysis/normarith.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/normarith.ML Sun Jul 05 15:02:30 2015 +0200
@@ -258,8 +258,9 @@
local
val pth_zero = @{thm norm_zero}
- val tv_n = (Thm.ctyp_of_cterm o Thm.dest_arg o Thm.dest_arg1 o Thm.dest_arg o Thm.cprop_of)
- pth_zero
+ val tv_n =
+ (dest_TVar o Thm.typ_of_cterm o Thm.dest_arg o Thm.dest_arg1 o Thm.dest_arg o Thm.cprop_of)
+ pth_zero
val concl = Thm.dest_arg o Thm.cprop_of
fun real_vector_combo_prover ctxt translator (nubs,ges,gts) =
let
@@ -356,7 +357,7 @@
val shs = filter (member (fn (t,th) => t aconvc Thm.cprop_of th) asl) (#hyps (Thm.crep_thm th1))
val th11 = hd (Variable.export ctxt' ctxt [fold Thm.implies_intr shs th1])
val cps = map (swap o Thm.dest_equals) (cprems_of th11)
- val th12 = Drule.instantiate_normalize ([], cps) th11
+ val th12 = Drule.instantiate_normalize ([], map (apfst (dest_Var o Thm.term_of)) cps) th11
val th13 = fold Thm.elim_implies (map (Thm.reflexive o snd) cps) th12;
in hd (Variable.export ctxt' ctxt [th13])
end
--- a/src/HOL/Nominal/nominal_datatype.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Sun Jul 05 15:02:30 2015 +0200
@@ -1390,13 +1390,13 @@
end);
val induct_aux' = Thm.instantiate ([],
- map (fn (s, v as Var (_, T)) =>
- (Thm.global_cterm_of thy9 v, Thm.global_cterm_of thy9 (Free (s, T))))
+ map (fn (s, Var (v as (_, T))) =>
+ (v, Thm.global_cterm_of thy9 (Free (s, T))))
(pnames ~~ map head_of (HOLogic.dest_conj
(HOLogic.dest_Trueprop (Thm.concl_of induct_aux)))) @
map (fn (_, f) =>
let val f' = Logic.varify_global f
- in (Thm.global_cterm_of thy9 f',
+ in (dest_Var f',
Thm.global_cterm_of thy9 (Const (@{const_name Nominal.supp}, fastype_of f')))
end) fresh_fs) induct_aux;
@@ -1562,7 +1562,7 @@
(augment_sort thy1 pt_cp_sort
(Logic.mk_implies (HOLogic.mk_Trueprop Q, HOLogic.mk_Trueprop P)))
(fn {context = ctxt, ...} => dtac (Thm.instantiate ([],
- [(Thm.global_cterm_of thy11 (Var (("pi", 0), permT)),
+ [((("pi", 0), permT),
Thm.global_cterm_of thy11 (Const (@{const_name rev}, permT --> permT) $ pi))]) th) 1 THEN
NominalPermeq.perm_simp_tac (put_simpset HOL_ss ctxt) 1)) (ps ~~ ths)
in (ths, ths') end) dt_atomTs);
@@ -1653,7 +1653,7 @@
SUBPROOF (fn {prems = prems', params = [(_, a), (_, b)], ...} => EVERY
[cut_facts_tac [rec_prem] 1,
rtac (Thm.instantiate ([],
- [(Thm.global_cterm_of thy11 (Var (("pi", 0), mk_permT aT)),
+ [((("pi", 0), mk_permT aT),
Thm.global_cterm_of thy11
(perm_of_pair (Thm.term_of a, Thm.term_of b)))]) eqvt_th) 1,
asm_simp_tac (put_simpset HOL_ss context addsimps
@@ -1872,8 +1872,7 @@
val l = find_index (equal T) dt_atomTs;
val th = nth (nth rec_equiv_thms' l) k;
val th' = Thm.instantiate ([],
- [(Thm.global_cterm_of thy11 (Var (("pi", 0), U)),
- Thm.global_cterm_of thy11 p)]) th;
+ [((("pi", 0), U), Thm.global_cterm_of thy11 p)]) th;
in rtac th' 1 end;
val th' = Goal.prove context'' [] []
(HOLogic.mk_Trueprop (S $ mk_pi x $ mk_pi y))
--- a/src/HOL/Nominal/nominal_fresh_fun.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML Sun Jul 05 15:02:30 2015 +0200
@@ -31,7 +31,10 @@
(* FIXME proper SUBGOAL/CSUBGOAL instead of cprems_of etc. *)
fun res_inst_tac_term ctxt =
- gen_res_inst_tac_term ctxt (curry Thm.instantiate);
+ gen_res_inst_tac_term ctxt (fn instT => fn inst =>
+ Thm.instantiate
+ (map (apfst (dest_TVar o Thm.typ_of)) instT,
+ map (apfst (dest_Var o Thm.term_of)) inst));
fun res_inst_tac_term' ctxt =
gen_res_inst_tac_term ctxt (K Drule.cterm_instantiate) [];
@@ -146,10 +149,10 @@
fun inst_fresh vars params i st =
let val vars' = Misc_Legacy.term_vars (Thm.prop_of st);
in case subtract (op =) vars vars' of
- [x] =>
+ [Var v] =>
Seq.single
(Thm.instantiate ([],
- [apply2 (Thm.cterm_of ctxt) (x, fold_rev Term.abs params (Bound 0))]) st)
+ [(v, Thm.cterm_of ctxt (fold_rev Term.abs params (Bound 0)))]) st)
| _ => error "fresh_fun_simp: Too many variables, please report."
end
in
--- a/src/HOL/Nominal/nominal_inductive.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML Sun Jul 05 15:02:30 2015 +0200
@@ -338,7 +338,8 @@
val pis'' = fold (concat_perm #> map) pis' pis;
val env = Pattern.first_order_match thy (ihypt, Thm.prop_of ihyp)
(Vartab.empty, Vartab.empty);
- val ihyp' = Thm.instantiate ([], map (apply2 (Thm.global_cterm_of thy))
+ val ihyp' = Thm.instantiate ([],
+ map (fn (v, t) => (dest_Var v, Thm.global_cterm_of thy t))
(map (Envir.subst_term env) vs ~~
map (fold_rev (NominalDatatype.mk_perm [])
(rev pis' @ pis)) params' @ [z])) ihyp;
--- a/src/HOL/Nominal/nominal_inductive2.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML Sun Jul 05 15:02:30 2015 +0200
@@ -146,9 +146,7 @@
fun inst_params thy (vs, p) th cts =
let val env = Pattern.first_order_match thy (p, Thm.prop_of th)
(Vartab.empty, Vartab.empty)
- in Thm.instantiate ([],
- map (Envir.subst_term env #> Thm.global_cterm_of thy) vs ~~ cts) th
- end;
+ in Thm.instantiate ([], map (dest_Var o Envir.subst_term env) vs ~~ cts) th end;
fun prove_strong_ind s alt_name avoids ctxt =
let
--- a/src/HOL/Statespace/distinct_tree_prover.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Statespace/distinct_tree_prover.ML Sun Jul 05 15:02:30 2015 +0200
@@ -95,7 +95,11 @@
fun mapT_and_recertify ct =
(Thm.cterm_of ctxt (Term.map_types (Term.map_type_tvar substT) (Thm.term_of ct)));
val insts' = map (apfst mapT_and_recertify) insts;
- in Thm.instantiate (instTs, insts') end;
+ in
+ Thm.instantiate
+ (map (apfst (dest_TVar o Thm.typ_of)) instTs,
+ map (apfst (dest_Var o Thm.term_of)) insts')
+ end;
fun tvar_clash ixn S S' =
raise TYPE ("Type variable has two distinct sorts", [TVar (ixn, S), TVar (ixn, S')], []);
@@ -145,9 +149,9 @@
val (tyinsts,insts) =
fold naive_cterm_first_order_match (Thm.prems_of rule ~~ map Thm.cprop_of prems) ([], []);
val tyinsts' =
- map (fn (v, (S, U)) => apply2 (Thm.ctyp_of ctxt) (TVar (v, S), U)) tyinsts;
+ map (fn (v, (S, U)) => ((v, S), Thm.ctyp_of ctxt U)) tyinsts;
val insts' =
- map (fn (idxn, ct) => (Thm.cterm_of ctxt (Var (idxn, Thm.typ_of_cterm ct)), ct)) insts;
+ map (fn (idxn, ct) => ((idxn, Thm.typ_of_cterm ct), ct)) insts;
val rule' = Thm.instantiate (tyinsts', insts') rule;
in fold Thm.elim_implies prems rule' end;
@@ -286,7 +290,7 @@
@{thm subtract_Tip} |> Thm.cprop_of |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2
|> Thm.dest_comb |> #2;
val [alpha] = ct |> Thm.ctyp_of_cterm |> Thm.dest_ctyp;
- in (alpha, #1 (dest_Var (Thm.term_of ct))) end;
+ in (dest_TVar (Thm.typ_of alpha), #1 (dest_Var (Thm.term_of ct))) end;
in
fun subtractProver ctxt (Const (@{const_name Tip}, T)) ct dist_thm =
@@ -296,7 +300,7 @@
in
Thm.instantiate
([(alpha, Thm.ctyp_of ctxt alphaI)],
- [(Thm.cterm_of ctxt (Var (v, treeT alphaI)), ct')]) @{thm subtract_Tip}
+ [((v, treeT alphaI), ct')]) @{thm subtract_Tip}
end
| subtractProver ctxt (Const (@{const_name Node}, nT) $ l $ x $ d $ r) ct dist_thm =
let
--- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML Sun Jul 05 15:02:30 2015 +0200
@@ -570,14 +570,14 @@
diff (Proof_Context.theory_of ctxt) (scheme_t, instance_t)
(*valuation of type variables*)
- val typeval = map (apply2 (Thm.ctyp_of ctxt)) type_pairing
+ val typeval = map (fn (v, T) => (dest_TVar v, Thm.ctyp_of ctxt T)) type_pairing
val typeval_env =
map (apfst dest_TVar) type_pairing
(*valuation of term variables*)
val termval =
- map (apfst (type_devar typeval_env)) term_pairing
- |> map (apply2 (Thm.cterm_of ctxt))
+ map (apfst (dest_Var o type_devar typeval_env)) term_pairing
+ |> map (apsnd (Thm.cterm_of ctxt))
in
Thm.instantiate (typeval, termval) scheme_thm
end
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Sun Jul 05 15:02:30 2015 +0200
@@ -950,8 +950,8 @@
val tactic =
if is_none var_opt then no_tac
else
- fold (curry (op APPEND)) (map (instantiate_tac (the var_opt)) skolem_cts) no_tac
-
+ fold (curry (op APPEND))
+ (map (instantiate_tac (dest_Var (Thm.term_of (the var_opt)))) skolem_cts) no_tac
in
tactic st
end
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Sun Jul 05 15:02:30 2015 +0200
@@ -607,9 +607,9 @@
let
val n = Thm.nprems_of coind;
val m = Thm.nprems_of (hd rel_monos) - n;
- fun mk_inst phi = (phi, mk_union (phi, HOLogic.eq_const (fst (dest_pred2T (fastype_of phi)))))
- |> apply2 (Thm.cterm_of ctxt);
- val insts = Term.add_vars (Thm.prop_of coind) [] |> rev |> take n |> map (mk_inst o Var);
+ fun mk_inst phi =
+ (phi, Thm.cterm_of ctxt (mk_union (Var phi, HOLogic.eq_const (fst (dest_pred2T (#2 phi))))))
+ val insts = Term.add_vars (Thm.prop_of coind) [] |> rev |> take n |> map mk_inst;
fun mk_unfold rel_eq rel_mono =
let
val eq = iffD2 OF [rel_eq RS @{thm predicate2_eqD}, refl];
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Sun Jul 05 15:02:30 2015 +0200
@@ -685,7 +685,9 @@
let
val ((inject_thms, inject_thmss), half_distinct_thmss) = chop n thmss |>> `flat;
- val rho_As = map (apply2 (Thm.ctyp_of lthy)) (map Logic.varifyT_global As ~~ As);
+ val rho_As =
+ map (fn (T, U) => (dest_TVar T, Thm.ctyp_of lthy U))
+ (map Logic.varifyT_global As ~~ As);
fun inst_thm t thm =
Drule.instantiate' [] [SOME (Thm.cterm_of lthy t)]
--- a/src/HOL/Tools/Function/partial_function.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Tools/Function/partial_function.ML Sun Jul 05 15:02:30 2015 +0200
@@ -200,7 +200,8 @@
val (P_var, x_var) =
Thm.prop_of inst_rule |> Logic.strip_imp_concl |> HOLogic.dest_Trueprop
|> strip_comb |> apsnd hd
- val P_rangeT = range_type (snd (Term.dest_Var P_var))
+ |> apply2 dest_Var
+ val P_rangeT = range_type (snd P_var)
val PT = map (snd o dest_Free) args ---> P_rangeT
val x_inst = cert (foldl1 HOLogic.mk_prod args)
val P_inst = cert (uncurry_n (length args) (Free (P, PT)))
@@ -211,7 +212,7 @@
THEN Simplifier.simp_tac (put_simpset curry_uncurry_ss ctxt) 3
THEN CONVERSION (split_params_conv ctxt
then_conv (Conv.forall_conv (K split_paired_all_conv) ctxt)) 3)
- |> Thm.instantiate ([], [(cert P_var, P_inst), (cert x_var, x_inst)])
+ |> Thm.instantiate ([], [(P_var, P_inst), (x_var, x_inst)])
|> Simplifier.full_simplify (put_simpset split_conv_ss ctxt)
|> singleton (Variable.export ctxt' ctxt)
in
--- a/src/HOL/Tools/Function/relation.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Tools/Function/relation.ML Sun Jul 05 15:02:30 2015 +0200
@@ -18,8 +18,7 @@
fun inst_state_tac ctxt inst =
SUBGOAL (fn (goal, _) =>
(case Term.add_vars goal [] of
- [v as (_, T)] =>
- PRIMITIVE (Thm.instantiate ([], [(Thm.cterm_of ctxt (Var v), Thm.cterm_of ctxt (inst T))]))
+ [v as (_, T)] => PRIMITIVE (Thm.instantiate ([], [(v, Thm.cterm_of ctxt (inst T))]))
| _ => no_tac));
fun relation_tac ctxt rel i =
@@ -39,9 +38,7 @@
|> map_types Type_Infer.paramify_vars
|> Type.constraint T
|> Syntax.check_term ctxt;
- in
- PRIMITIVE (Thm.instantiate ([], [(Thm.cterm_of ctxt (Var v), Thm.cterm_of ctxt rel')]))
- end
+ in PRIMITIVE (Thm.instantiate ([], [(v, Thm.cterm_of ctxt rel')])) end
| _ => no_tac));
fun relation_infer_tac ctxt rel i =
--- a/src/HOL/Tools/Lifting/lifting_bnf.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Tools/Lifting/lifting_bnf.ML Sun Jul 05 15:02:30 2015 +0200
@@ -23,7 +23,7 @@
fun get_lhs thm = thm |> Thm.concl_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> fst
val vars = get_lhs rel_Grp |> strip_comb |> snd |> map_filter (try (strip_comb #> snd #> hd))
val UNIVs = map (fn var => HOLogic.mk_UNIV (var |> dest_Var |> snd |> dest_Type |> snd |> hd)) vars
- val inst = map2 (curry (apply2 (Thm.cterm_of ctxt))) vars UNIVs
+ val inst = map dest_Var vars ~~ map (Thm.cterm_of ctxt) UNIVs
val rel_Grp_UNIV_sym = rel_Grp |> Drule.instantiate_normalize ([], inst)
|> Local_Defs.unfold ctxt @{thms subset_UNIV[THEN eqTrueI] UNIV_def[symmetric] simp_thms(21)}
|> (fn thm => thm RS sym)
--- a/src/HOL/Tools/Lifting/lifting_term.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Tools/Lifting/lifting_term.ML Sun Jul 05 15:02:30 2015 +0200
@@ -310,7 +310,7 @@
val thy = Proof_Context.theory_of ctxt
val (_, qty_schematic) = quot_thm_rty_qty quot_thm
val match_env = Sign.typ_match thy (qty_schematic, qty) Vartab.empty
- fun prep_ty (x, (S, ty)) = apply2 (Thm.ctyp_of ctxt) (TVar (x, S), ty)
+ fun prep_ty (x, (S, ty)) = ((x, S), Thm.ctyp_of ctxt ty)
val ty_inst = Vartab.fold (cons o prep_ty) match_env []
in
Thm.instantiate (ty_inst, []) quot_thm
--- a/src/HOL/Tools/Lifting/lifting_util.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Tools/Lifting/lifting_util.ML Sun Jul 05 15:02:30 2015 +0200
@@ -145,7 +145,7 @@
fun instT_thm ctxt env =
let
val cinst = env |> Vartab.dest
- |> map (fn (x, (S, T)) => (Thm.ctyp_of ctxt (TVar (x, S)), Thm.ctyp_of ctxt T));
+ |> map (fn (x, (S, T)) => ((x, S), Thm.ctyp_of ctxt T));
in
Thm.instantiate (cinst, [])
end;
--- a/src/HOL/Tools/Meson/meson.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Tools/Meson/meson.ML Sun Jul 05 15:02:30 2015 +0200
@@ -346,16 +346,17 @@
(*Replaces universally quantified variables by FREE variables -- because
assumptions may not contain scheme variables. Later, generalize using Variable.export. *)
local
- val spec_var = Thm.dest_arg (Thm.dest_arg (#2 (Thm.dest_implies (Thm.cprop_of spec))));
- val spec_varT = Thm.typ_of_cterm spec_var;
- fun name_of (Const (@{const_name All}, _) $ Abs(x,_,_)) = x | name_of _ = Name.uu;
+ val spec_var =
+ Thm.dest_arg (Thm.dest_arg (#2 (Thm.dest_implies (Thm.cprop_of spec))))
+ |> Thm.term_of |> dest_Var;
+ fun name_of (Const (@{const_name All}, _) $ Abs(x, _, _)) = x | name_of _ = Name.uu;
in
fun freeze_spec th ctxt =
let
val ([x], ctxt') =
Variable.variant_fixes [name_of (HOLogic.dest_Trueprop (Thm.concl_of th))] ctxt;
val spec' = spec
- |> Thm.instantiate ([], [(spec_var, Thm.cterm_of ctxt' (Free (x, spec_varT)))]);
+ |> Thm.instantiate ([], [(spec_var, Thm.cterm_of ctxt' (Free (x, snd spec_var)))]);
in (th RS spec', ctxt') end
end;
--- a/src/HOL/Tools/Meson/meson_clausify.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Tools/Meson/meson_clausify.ML Sun Jul 05 15:02:30 2015 +0200
@@ -44,10 +44,10 @@
"Sledgehammer_Util".) *)
fun transform_elim_theorem th =
(case Thm.concl_of th of (*conclusion variable*)
- @{const Trueprop} $ (v as Var (_, @{typ bool})) =>
- Thm.instantiate ([], [(Thm.cterm_of @{theory_context HOL} v, cfalse)]) th
- | v as Var(_, @{typ prop}) =>
- Thm.instantiate ([], [(Thm.cterm_of @{theory_context HOL} v, ctp_false)]) th
+ @{const Trueprop} $ (Var (v as (_, @{typ bool}))) =>
+ Thm.instantiate ([], [(v, cfalse)]) th
+ | Var (v as (_, @{typ prop})) =>
+ Thm.instantiate ([], [(v, ctp_false)]) th
| _ => th)
@@ -375,9 +375,7 @@
th ctxt
val (cnf_ths, ctxt) = clausify nnf_th
fun intr_imp ct th =
- Thm.instantiate ([], map (apply2 (Thm.cterm_of ctxt))
- [(Var (("i", 0), @{typ nat}),
- HOLogic.mk_nat ax_no)])
+ Thm.instantiate ([], [((("i", 0), @{typ nat}), Thm.cterm_of ctxt (HOLogic.mk_nat ax_no))])
(zero_var_indexes @{thm skolem_COMBK_D})
RS Thm.implies_intr ct th
in
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Sun Jul 05 15:02:30 2015 +0200
@@ -174,7 +174,7 @@
fun incr_type_indexes ctxt inc th =
let
val tvs = Term.add_tvars (Thm.full_prop_of th) []
- fun inc_tvar ((a, i), s) = apply2 (Thm.ctyp_of ctxt) (TVar ((a, i), s), TVar ((a, i + inc), s))
+ fun inc_tvar ((a, i), s) = (((a, i), s), Thm.ctyp_of ctxt (TVar ((a, i + inc), s)))
in
Thm.instantiate (map inc_tvar tvs, []) th
end
@@ -211,7 +211,7 @@
|> rpair (Envir.empty ~1)
|-> fold (Pattern.unify (Context.Proof ctxt))
|> Envir.type_env |> Vartab.dest
- |> map (fn (x, (S, T)) => apply2 (Thm.ctyp_of ctxt) (TVar (x, S), T))
+ |> map (fn (x, (S, T)) => ((x, S), Thm.ctyp_of ctxt T))
in
(* The unifier, which is invoked from "Thm.bicompose", will sometimes refuse to unify
"?a::?'a" with "?a::?'b" or "?a::nat" and throw a "TERM" exception (with "add_ffpair" as
@@ -400,8 +400,8 @@
val thy = Proof_Context.theory_of ctxt
val (tyenv, tenv) = fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty)
- fun mkT (v, (S, T)) = apply2 (Thm.ctyp_of ctxt) (TVar (v, S), T)
- fun mk (v, (T, t)) = apply2 (Thm.cterm_of ctxt) (Var (v, Envir.subst_type tyenv T), t)
+ fun mkT (v, (S, T)) = ((v, S), Thm.ctyp_of ctxt T)
+ fun mk (v, (T, t)) = ((v, Envir.subst_type tyenv T), Thm.cterm_of ctxt t)
val instsT = Vartab.fold (cons o mkT) tyenv []
val insts = Vartab.fold (cons o mk) tenv []
@@ -570,11 +570,11 @@
Envir.Envir {maxidx = Vartab.fold (Integer.max o snd o fst) tyenv 0,
tenv = Vartab.empty, tyenv = tyenv}
val ty_inst =
- Vartab.fold (fn (x, (S, T)) => cons (apply2 (Thm.ctyp_of ctxt) (TVar (x, S), T)))
+ Vartab.fold (fn (x, (S, T)) => cons (((x, S), Thm.ctyp_of ctxt T)))
tyenv []
val t_inst = [apply2 (Thm.cterm_of ctxt o Envir.norm_term env) (Var var, t')]
in
- Drule.instantiate_normalize (ty_inst, t_inst) th
+ Drule.instantiate_normalize (ty_inst, map (apfst (dest_Var o Thm.term_of)) t_inst) th
end
| _ => raise Fail "expected a single non-zapped, non-Metis Var")
in
--- a/src/HOL/Tools/Predicate_Compile/core_data.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Tools/Predicate_Compile/core_data.ML Sun Jul 05 15:02:30 2015 +0200
@@ -232,10 +232,10 @@
fun instantiate i n ({context = ctxt2, prems, ...}: Subgoal.focus) =
let
- fun term_pair_of (ix, (ty, t)) = (Var (ix, ty), t)
+ fun inst_pair_of (ix, (ty, t)) = ((ix, ty), t)
fun inst_of_matches tts =
fold (Pattern.match thy) tts (Vartab.empty, Vartab.empty)
- |> snd |> Vartab.dest |> map (apply2 (Thm.cterm_of ctxt2) o term_pair_of)
+ |> snd |> Vartab.dest |> map (apsnd (Thm.cterm_of ctxt2) o inst_pair_of)
val (cases, (eqs, prems1)) = apsnd (chop (nargs - nparams)) (chop n prems)
val case_th =
rewrite_rule ctxt2 (@{thm Predicate.eq_is_eq} :: map meta_eq_of eqs) (nth cases (i - 1))
--- a/src/HOL/Tools/Qelim/cooper.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML Sun Jul 05 15:02:30 2015 +0200
@@ -150,10 +150,10 @@
val get_pmi = get_pmi_term o Thm.cprop_of;
-val p_v' = @{cpat "?P' :: int => bool"};
-val q_v' = @{cpat "?Q' :: int => bool"};
-val p_v = @{cpat "?P:: int => bool"};
-val q_v = @{cpat "?Q:: int => bool"};
+val p_v' = (("P'", 0), @{typ "int \<Rightarrow> bool"});
+val q_v' = (("Q'", 0), @{typ "int \<Rightarrow> bool"});
+val p_v = (("P", 0), @{typ "int \<Rightarrow> bool"});
+val q_v = (("Q", 0), @{typ "int \<Rightarrow> bool"});
fun myfwd (th1, th2, th3) p q
[(th_1,th_2,th_3), (th_1',th_2',th_3')] =
@@ -430,11 +430,13 @@
val insert_tm = @{cterm "insert :: int => _"};
fun mkISet cts = fold_rev (Thm.apply insert_tm #> Thm.apply) cts emptyIS;
val eqelem_imp_imp = @{thm eqelem_imp_iff} RS iffD1;
-val [A_tm,B_tm] = map (fn th => Thm.cprop_of th |> funpow 2 Thm.dest_arg |> Thm.dest_abs NONE |> snd |> Thm.dest_arg1 |> Thm.dest_arg
- |> Thm.dest_abs NONE |> snd |> Thm.dest_fun |> Thm.dest_arg)
- [asetP,bsetP];
+val [A_v,B_v] =
+ map (fn th => Thm.cprop_of th |> funpow 2 Thm.dest_arg
+ |> Thm.dest_abs NONE |> snd |> Thm.dest_arg1 |> Thm.dest_arg
+ |> Thm.dest_abs NONE |> snd |> Thm.dest_fun |> Thm.dest_arg
+ |> Thm.term_of |> dest_Var) [asetP, bsetP];
-val D_tm = @{cpat "?D::int"};
+val D_v = (("D", 0), @{typ int});
fun cooperex_conv ctxt vs q =
let
@@ -501,16 +503,16 @@
if length (distinct (op aconv) bl) <= length (distinct (op aconv) al)
then
(bl,b0,decomp_minf,
- fn B => (map (fn th => Thm.implies_elim (Thm.instantiate ([],[(B_tm,B), (D_tm,cd)]) th) dp)
+ fn B => (map (fn th => Thm.implies_elim (Thm.instantiate ([],[(B_v,B), (D_v,cd)]) th) dp)
[bseteq,bsetneq,bsetlt, bsetle, bsetgt,bsetge])@
- (map (Thm.instantiate ([],[(B_tm,B), (D_tm,cd)]))
+ (map (Thm.instantiate ([],[(B_v,B), (D_v,cd)]))
[bsetdvd,bsetndvd,bsetP,infDdvd, infDndvd,bsetconj,
bsetdisj,infDconj, infDdisj]),
cpmi)
else (al,a0,decomp_pinf,fn A =>
- (map (fn th => Thm.implies_elim (Thm.instantiate ([],[(A_tm,A), (D_tm,cd)]) th) dp)
+ (map (fn th => Thm.implies_elim (Thm.instantiate ([],[(A_v,A), (D_v,cd)]) th) dp)
[aseteq,asetneq,asetlt, asetle, asetgt,asetge])@
- (map (Thm.instantiate ([],[(A_tm,A), (D_tm,cd)]))
+ (map (Thm.instantiate ([],[(A_v,A), (D_v,cd)]))
[asetdvd,asetndvd, asetP, infDdvd, infDndvd,asetconj,
asetdisj,infDconj, infDdisj]),cppi)
val cpth =
--- a/src/HOL/Tools/Quickcheck/random_generators.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML Sun Jul 05 15:02:30 2015 +0200
@@ -73,7 +73,9 @@
val lhs = eq |> Thm.dest_arg1;
val pt_random_aux = lhs |> Thm.dest_fun;
val pt_rhs = eq |> Thm.dest_arg |> Thm.dest_fun;
-val aT = pt_random_aux |> Thm.ctyp_of_cterm |> dest_ctyp_nth 1;
+val a_v =
+ pt_random_aux |> Thm.ctyp_of_cterm |> dest_ctyp_nth 1
+ |> Thm.typ_of |> dest_TVar;
val rew_thms = map mk_meta_eq [@{thm natural_zero_minus_one},
@{thm Suc_natural_minus_one}, @{thm select_weight_cons_zero}, @{thm beyond_zero}];
@@ -89,7 +91,7 @@
(HOLogic.dest_eq o HOLogic.dest_Trueprop) eq;
val Type (_, [_, iT]) = T;
val icT = Thm.ctyp_of lthy iT;
- val inst = Thm.instantiate_cterm ([(aT, icT)], []);
+ val inst = Thm.instantiate_cterm ([(a_v, icT)], []);
fun subst_v t' = map_aterms (fn t as Free (w, _) => if v = w then t' else t | t => t);
val t_rhs = lambda t_k proto_t_rhs;
val eqs0 = [subst_v @{term "0::natural"} eq,
@@ -98,11 +100,11 @@
val ((_, (_, eqs2)), lthy') = lthy
|> BNF_LFP_Compat.primrec_simple
[((Binding.concealed (Binding.name random_aux), T), NoSyn)] eqs1;
- val cT_random_aux = inst pt_random_aux;
- val cT_rhs = inst pt_rhs;
+ val cT_random_aux = inst pt_random_aux |> Thm.term_of |> dest_Var;
+ val cT_rhs = inst pt_rhs |> Thm.term_of |> dest_Var;
val rule = @{thm random_aux_rec}
|> Drule.instantiate_normalize
- ([(aT, icT)],
+ ([(a_v, icT)],
[(cT_random_aux, Thm.cterm_of lthy' t_random_aux),
(cT_rhs, Thm.cterm_of lthy' t_rhs)]);
fun tac ctxt =
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Sun Jul 05 15:02:30 2015 +0200
@@ -72,20 +72,16 @@
| _ => error "Solve_quotient_assm failed. Possibly a quotient theorem is missing."
-fun prep_trm thy (x, (T, t)) =
- (Thm.global_cterm_of thy (Var (x, T)), Thm.global_cterm_of thy t)
-
-fun prep_ty thy (x, (S, ty)) =
- (Thm.global_ctyp_of thy (TVar (x, S)), Thm.global_ctyp_of thy ty)
-
fun get_match_inst thy pat trm =
let
val univ = Unify.matchers (Context.Theory thy) [(pat, trm)]
val SOME (env, _) = Seq.pull univ (* raises Bind, if no unifier *) (* FIXME fragile *)
val tenv = Vartab.dest (Envir.term_env env)
val tyenv = Vartab.dest (Envir.type_env env)
+ fun prep_ty (x, (S, ty)) = ((x, S), Thm.global_ctyp_of thy ty)
+ fun prep_trm (x, (T, t)) = ((x, T), Thm.global_cterm_of thy t)
in
- (map (prep_ty thy) tyenv, map (prep_trm thy) tenv)
+ (map prep_ty tyenv, map prep_trm tenv)
end
(* Calculates the instantiations for the lemmas:
@@ -480,7 +476,7 @@
then make_inst_id (Thm.term_of (Thm.lhs_of thm3)) (Thm.term_of ctrm)
else make_inst (Thm.term_of (Thm.lhs_of thm3)) (Thm.term_of ctrm)
val thm4 =
- Drule.instantiate_normalize ([], [(Thm.cterm_of ctxt insp, Thm.cterm_of ctxt inst)]) thm3
+ Drule.instantiate_normalize ([], [(dest_Var insp, Thm.cterm_of ctxt inst)]) thm3
in
Conv.rewr_conv thm4 ctrm
end
--- a/src/HOL/Tools/SMT/smt_normalize.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Tools/SMT/smt_normalize.ML Sun Jul 05 15:02:30 2015 +0200
@@ -35,7 +35,7 @@
fun inst f ct thm =
let val cv = f (Drule.strip_imp_concl (Thm.cprop_of thm))
- in Thm.instantiate ([], [(cv, ct)]) thm end
+ in Thm.instantiate ([], [(dest_Var (Thm.term_of cv), ct)]) thm end
in
fun instantiate_elim thm =
@@ -199,8 +199,10 @@
fun insert_trigger_conv [] ct = Conv.all_conv ct
| insert_trigger_conv ctss ct =
- let val (ctr, cp) = Thm.dest_binop (Thm.rhs_of trigger_eq) ||> rpair ct
- in Thm.instantiate ([], [cp, (ctr, mk_trigger ctss)]) trigger_eq end
+ let
+ val (ctr, cp) = Thm.dest_binop (Thm.rhs_of trigger_eq) ||> rpair ct
+ val inst = map (apfst (dest_Var o Thm.term_of)) [cp, (ctr, mk_trigger ctss)]
+ in Thm.instantiate ([], inst) trigger_eq end
fun infer_trigger_eq_conv outer_ctxt (ctxt, cvs) ct =
let
--- a/src/HOL/Tools/SMT/smt_util.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Tools/SMT/smt_util.ML Sun Jul 05 15:02:30 2015 +0200
@@ -171,7 +171,7 @@
val destT1 = hd o Thm.dest_ctyp
val destT2 = hd o tl o Thm.dest_ctyp
-fun instTs cUs (cTs, ct) = Thm.instantiate_cterm (cTs ~~ cUs, []) ct
+fun instTs cUs (cTs, ct) = Thm.instantiate_cterm (map (dest_TVar o Thm.typ_of) cTs ~~ cUs, []) ct
fun instT cU (cT, ct) = instTs [cU] ([cT], ct)
fun instT' ct = instT (Thm.ctyp_of_cterm ct)
--- a/src/HOL/Tools/SMT/z3_replay_methods.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Tools/SMT/z3_replay_methods.ML Sun Jul 05 15:02:30 2015 +0200
@@ -100,20 +100,20 @@
(Vartab.empty, Vartab.empty)
|> Pattern.first_order_match (Proof_Context.theory_of ctxt) (pat, t)
-fun gen_certify_inst sel mk cert ctxt thm t =
+fun gen_certify_inst sel cert ctxt thm t =
let
val inst = match ctxt (dest_thm thm) (dest_prop t)
- fun cert_inst (ix, (a, b)) = (cert (mk (ix, a)), cert b)
+ fun cert_inst (ix, (a, b)) = ((ix, a), cert b)
in Vartab.fold (cons o cert_inst) (sel inst) [] end
fun match_instantiateT ctxt t thm =
if Term.exists_type (Term.exists_subtype Term.is_TVar) (dest_thm thm) then
- Thm.instantiate (gen_certify_inst fst TVar (Thm.ctyp_of ctxt) ctxt thm t, []) thm
+ Thm.instantiate (gen_certify_inst fst (Thm.ctyp_of ctxt) ctxt thm t, []) thm
else thm
fun match_instantiate ctxt t thm =
let val thm' = match_instantiateT ctxt t thm in
- Thm.instantiate ([], gen_certify_inst snd Var (Thm.cterm_of ctxt) ctxt thm' t) thm'
+ Thm.instantiate ([], gen_certify_inst snd (Thm.cterm_of ctxt) ctxt thm' t) thm'
end
fun apply_rule ctxt t =
--- a/src/HOL/Tools/SMT/z3_replay_util.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Tools/SMT/z3_replay_util.ML Sun Jul 05 15:02:30 2015 +0200
@@ -15,7 +15,7 @@
val discharge: thm -> thm -> thm
(*a faster COMP*)
- type compose_data
+ type compose_data = cterm list * (cterm -> cterm list) * thm
val precompose: (cterm -> cterm list) -> thm -> compose_data
val precompose2: (cterm -> cterm * cterm) -> thm -> compose_data
val compose: compose_data -> thm -> thm
@@ -71,11 +71,12 @@
fun list2 (x, y) = [x, y]
-fun precompose f rule = (f (Thm.cprem_of rule 1), f, rule)
-fun precompose2 f rule = precompose (list2 o f) rule
+fun precompose f rule : compose_data = (f (Thm.cprem_of rule 1), f, rule)
+fun precompose2 f rule : compose_data = precompose (list2 o f) rule
fun compose (cvs, f, rule) thm =
- discharge thm (Thm.instantiate ([], cvs ~~ f (Thm.cprop_of thm)) rule)
+ discharge thm
+ (Thm.instantiate ([], map (dest_Var o Thm.term_of) cvs ~~ f (Thm.cprop_of thm)) rule)
(* simpset *)
--- a/src/HOL/Tools/Transfer/transfer.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Tools/Transfer/transfer.ML Sun Jul 05 15:02:30 2015 +0200
@@ -592,11 +592,10 @@
fun prep a = the (AList.lookup (op =) tab a)
val thm = transfer_rule_of_terms fst ctxt' tab s t
val binsts = bool_insts (if equiv then 0 else 1) (s, t)
- val cbool = @{ctyp bool}
- val relT = @{typ "bool => bool => bool"}
val idx = Thm.maxidx_of thm + 1
- fun tinst (a, _) = (Thm.ctyp_of ctxt' (TVar ((a, idx), @{sort type})), cbool)
- fun inst (a, t) = apply2 (Thm.cterm_of ctxt') (Var (Name.clean_index (prep a, idx), relT), t)
+ fun tinst (a, _) = (((a, idx), @{sort type}), @{ctyp bool})
+ fun inst (a, t) =
+ ((Name.clean_index (prep a, idx), @{typ "bool \<Rightarrow> bool \<Rightarrow> bool"}), Thm.cterm_of ctxt' t)
in
thm
|> Thm.generalize (tfrees, rnames @ frees) idx
@@ -616,11 +615,10 @@
fun prep a = the (AList.lookup (op =) tab a)
val thm = transfer_rule_of_terms snd ctxt' tab t s
val binsts = bool_insts 1 (s, t)
- val cbool = @{ctyp bool}
- val relT = @{typ "bool => bool => bool"}
val idx = Thm.maxidx_of thm + 1
- fun tinst (a, _) = (Thm.ctyp_of ctxt' (TVar ((a, idx), @{sort type})), cbool)
- fun inst (a, t) = apply2 (Thm.cterm_of ctxt') (Var (Name.clean_index (prep a, idx), relT), t)
+ fun tinst (a, _) = (((a, idx), @{sort type}), @{ctyp bool})
+ fun inst (a, t) =
+ ((Name.clean_index (prep a, idx), @{typ "bool \<Rightarrow> bool \<Rightarrow> bool"}), Thm.cterm_of ctxt' t)
in
thm
|> Thm.generalize (tfrees, rnames @ frees) idx
--- a/src/HOL/Tools/coinduction.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Tools/coinduction.ML Sun Jul 05 15:02:30 2015 +0200
@@ -61,9 +61,9 @@
|> fold Variable.declare_names vars
|> fold Variable.declare_thm (raw_thm :: prems);
val thm_concl = Thm.cprop_of raw_thm |> strip_imp_concl;
- val (rhoTs, rhots) = Thm.match (thm_concl, concl)
- |>> map (apply2 Thm.typ_of)
- ||> map (apply2 Thm.term_of);
+ val (instT, inst) = Thm.match (thm_concl, concl);
+ val rhoTs = map (fn (v, T) => (TVar v, Thm.typ_of T)) instT;
+ val rhots = map (fn (v, t) => (Var v, Thm.term_of t)) inst;
val xs = hd (Thm.prems_of raw_thm) |> HOLogic.dest_Trueprop |> strip_comb |> snd
|> map (subst_atomic_types rhoTs);
val raw_eqs = map (fn x => (x, AList.lookup op aconv rhots x |> the)) xs;
@@ -160,4 +160,3 @@
end;
end;
-
--- a/src/HOL/Tools/hologic.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Tools/hologic.ML Sun Jul 05 15:02:30 2015 +0200
@@ -207,14 +207,14 @@
let
val (P, Q) = apply2 (Object_Logic.dest_judgment ctxt o Thm.cprop_of) (thP, thQ)
handle CTERM (msg, _) => raise THM (msg, 0, [thP, thQ]);
- val inst = Thm.instantiate ([], [(@{cpat "?P::bool"}, P), (@{cpat "?Q::bool"}, Q)]);
+ val inst = Thm.instantiate ([], [((("P", 0), boolT), P), ((("Q", 0), boolT), Q)]);
in Drule.implies_elim_list (inst @{thm conjI}) [thP, thQ] end;
fun conj_elim ctxt thPQ =
let
val (P, Q) = Thm.dest_binop (Object_Logic.dest_judgment ctxt (Thm.cprop_of thPQ))
handle CTERM (msg, _) => raise THM (msg, 0, [thPQ]);
- val inst = Thm.instantiate ([], [(@{cpat "?P::bool"}, P), (@{cpat "?Q::bool"}, Q)]);
+ val inst = Thm.instantiate ([], [((("P", 0), boolT), P), ((("Q", 0), boolT), Q)]);
val thP = Thm.implies_elim (inst @{thm conjunct1}) thPQ;
val thQ = Thm.implies_elim (inst @{thm conjunct2}) thPQ;
in (thP, thQ) end;
--- a/src/HOL/Tools/inductive_set.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Tools/inductive_set.ML Sun Jul 05 15:02:30 2015 +0200
@@ -205,7 +205,7 @@
val x' = map_type
(K (Ts @ HOLogic.strip_ptupleT ps U ---> HOLogic.boolT)) x;
in
- (Thm.cterm_of ctxt x,
+ (dest_Var x,
Thm.cterm_of ctxt (fold_rev (Term.abs o pair "x") Ts
(HOLogic.Collect_const U $
HOLogic.mk_psplits ps U HOLogic.boolT
@@ -367,7 +367,7 @@
val T = HOLogic.mk_ptupleT ps Us;
val x' = map_type (K (Rs ---> HOLogic.mk_setT T)) x
in
- (Thm.cterm_of ctxt x,
+ (dest_Var x,
Thm.cterm_of ctxt (fold_rev (Term.abs o pair "x") Ts
(HOLogic.mk_mem (HOLogic.mk_ptuple ps T (map Bound (k downto 0)),
list_comb (x', map Bound (l - 1 downto k + 1))))))
--- a/src/HOL/Tools/lin_arith.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Tools/lin_arith.ML Sun Jul 05 15:02:30 2015 +0200
@@ -60,10 +60,8 @@
fun is_nat t = (fastype_of1 t = HOLogic.natT);
fun mk_nat_thm thy t =
- let
- val cn = Thm.global_cterm_of thy (Var (("n", 0), HOLogic.natT))
- and ct = Thm.global_cterm_of thy t
- in Drule.instantiate_normalize ([], [(cn, ct)]) @{thm le0} end;
+ let val ct = Thm.global_cterm_of thy t
+ in Drule.instantiate_normalize ([], [((("n", 0), HOLogic.natT), ct)]) @{thm le0} end;
end;
--- a/src/HOL/Tools/monomorph.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Tools/monomorph.ML Sun Jul 05 15:02:30 2015 +0200
@@ -159,7 +159,7 @@
fun instantiate ctxt subst =
let
- fun cert (ix, (S, T)) = apply2 (Thm.ctyp_of ctxt) (TVar (ix, S), T)
+ fun cert (ix, (S, T)) = ((ix, S), Thm.ctyp_of ctxt T)
fun cert' subst = Vartab.fold (cons o cert) subst []
in Thm.instantiate (cert' subst, []) end
--- a/src/HOL/Tools/numeral.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Tools/numeral.ML Sun Jul 05 15:02:30 2015 +0200
@@ -49,7 +49,7 @@
val uminus = @{cpat "uminus"};
val uminusT = Thm.ctyp_of @{context} (Term.range_type (Thm.typ_of_cterm uminus));
-fun instT T V = Thm.instantiate_cterm ([(V, T)], []);
+fun instT T V = Thm.instantiate_cterm ([(dest_TVar (Thm.typ_of V), T)], []);
in
--- a/src/HOL/Tools/numeral_simprocs.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Tools/numeral_simprocs.ML Sun Jul 05 15:02:30 2015 +0200
@@ -595,8 +595,8 @@
fun prove_nz ctxt T t =
let
- val z = Thm.instantiate_cterm ([(zT,T)],[]) zr
- val eq = Thm.instantiate_cterm ([(eqT,T)],[]) geq
+ val z = Thm.instantiate_cterm ([(dest_TVar (Thm.typ_of zT), T)],[]) zr
+ val eq = Thm.instantiate_cterm ([(dest_TVar (Thm.typ_of eqT), T)],[]) geq
val th = Simplifier.rewrite (ctxt addsimps @{thms simp_thms})
(Thm.apply @{cterm "Trueprop"} (Thm.apply @{cterm "Not"}
(Thm.apply (Thm.apply eq t) z)))
--- a/src/HOL/Tools/record.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Tools/record.ML Sun Jul 05 15:02:30 2015 +0200
@@ -1755,7 +1755,7 @@
fun mk_eq_refl thy =
@{thm equal_refl}
|> Thm.instantiate
- ([apply2 (Thm.global_ctyp_of thy) (TVar (("'a", 0), @{sort equal}), Logic.varifyT_global extT)], [])
+ ([((("'a", 0), @{sort equal}), Thm.global_ctyp_of thy (Logic.varifyT_global extT))], [])
|> Axclass.unoverload thy;
val ensure_random_record = ensure_sort_record (@{sort random}, mk_random_eq);
val ensure_exhaustive_record =
--- a/src/HOL/Tools/reification.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Tools/reification.ML Sun Jul 05 15:02:30 2015 +0200
@@ -169,9 +169,9 @@
val (fnvs, invs) = List.partition (fn ((vn, _),_) => member (op =) vns vn) (Vartab.dest tmenv);
val (fts, its) =
(map (snd o snd) fnvs,
- map (fn ((vn, vi), (tT, t)) => apply2 (Thm.cterm_of ctxt) (Var ((vn, vi), tT), t)) invs);
+ map (fn ((vn, vi), (tT, t)) => (((vn, vi), tT), Thm.cterm_of ctxt t)) invs);
val ctyenv =
- map (fn ((vn, vi), (s, ty)) => apply2 (Thm.ctyp_of ctxt) (TVar ((vn, vi), s), ty))
+ map (fn ((vn, vi), (s, ty)) => (((vn, vi), s), Thm.ctyp_of ctxt ty))
(Vartab.dest tyenv);
in
((map (Thm.cterm_of ctxt) fts ~~ replicate (length fts) ctxt,
@@ -203,7 +203,7 @@
val sbst = Envir.subst_term (tyenv, tmenv);
val sbsT = Envir.subst_type tyenv;
val subst_ty =
- map (fn (n, (s, t)) => apply2 (Thm.ctyp_of ctxt'') (TVar (n, s), t)) (Vartab.dest tyenv)
+ map (fn (n, (s, t)) => ((n, s), Thm.ctyp_of ctxt'' t)) (Vartab.dest tyenv)
val tml = Vartab.dest tmenv;
val (subst_ns, bds) = fold_map
(fn (Const _ $ _ $ n, Var (xn0, _)) => fn bds =>
@@ -230,7 +230,9 @@
let
val ih = Drule.cterm_rule (Thm.instantiate (subst_ty, []));
in map (apply2 ih) (subst_ns @ subst_vs @ cts) end;
- val th = (Drule.instantiate_normalize (subst_ty, substt) eq) RS sym;
+ val th =
+ (Drule.instantiate_normalize (subst_ty, map (apfst (dest_Var o Thm.term_of)) substt) eq)
+ RS sym;
in (hd (Variable.export ctxt'' ctxt [th]), bds) end)
handle Pattern.MATCH => tryeqs eqs (ct, ctxt) bds);
@@ -266,10 +268,7 @@
let
val (_, _ :: vs) = eq |> Thm.prop_of |> HOLogic.dest_Trueprop
|> HOLogic.dest_eq |> fst |> strip_comb;
- val subst =
- map_filter
- (fn (v as Var (_, T)) => SOME (Thm.cterm_of ctxt' v, subst T)
- | _ => NONE) vs;
+ val subst = map_filter (fn Var v => SOME (v, subst (#2 v)) | _ => NONE) vs;
in Thm.instantiate ([], subst) eq end;
val (ps, congs) = map_split (mk_congeq ctxt' fs o prep_eq) eqs;
val bds = AList.make (K ([], [])) tys;
@@ -285,9 +284,10 @@
| is_list_var _ = false;
val vars = th |> Thm.prop_of |> Logic.dest_equals |> snd
|> strip_comb |> snd |> filter is_list_var;
- val vs = map (fn v as Var (_, T) =>
+ val vs = map (fn Var (v as (_, T)) =>
(v, the (AList.lookup Type.could_unify bds' T) |> snd |> HOLogic.mk_list (dest_listT T))) vars;
- val th' = Drule.instantiate_normalize ([], map (apply2 (Thm.cterm_of ctxt)) vs) th;
+ val th' =
+ Drule.instantiate_normalize ([], map (apsnd (Thm.cterm_of ctxt)) vs) th;
val th'' = Thm.symmetric (dereify ctxt [] (Thm.lhs_of th'));
in Thm.transitive th'' th' end;
--- a/src/HOL/Tools/sat.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Tools/sat.ML Sun Jul 05 15:02:30 2015 +0200
@@ -73,8 +73,6 @@
val resolution_thm =
@{lemma "(P ==> False) ==> (~ P ==> False) ==> False" by (rule case_split)}
-val cP = Thm.cterm_of @{context} (Var (("P", 0), HOLogic.boolT));
-
(* ------------------------------------------------------------------------- *)
(* lit_ord: an order on integers that considers their absolute values only, *)
(* thereby treating integers that represent the same atom (positively *)
@@ -173,7 +171,7 @@
val cLit =
snd (Thm.dest_comb (if hyp1_is_neg then hyp2 else hyp1)) (* strip Trueprop *)
in
- Thm.instantiate ([], [(cP, cLit)]) resolution_thm
+ Thm.instantiate ([], [((("P", 0), HOLogic.boolT), cLit)]) resolution_thm
end
val _ =
--- a/src/HOL/Tools/semiring_normalizer.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Tools/semiring_normalizer.ML Sun Jul 05 15:02:30 2015 +0200
@@ -238,7 +238,7 @@
if is_binop ct ct' then Thm.dest_binop ct'
else raise CTERM ("dest_binop: bad binop", [ct, ct'])
-fun inst_thm inst = Thm.instantiate ([], inst);
+fun inst_thm inst = Thm.instantiate ([], map (apfst (dest_Var o Thm.term_of)) inst);
val dest_number = Thm.term_of #> HOLogic.dest_number #> snd;
val is_number = can dest_number;
@@ -300,7 +300,7 @@
val sub_tm = Thm.dest_fun (Thm.dest_fun sub_pat)
val neg_tm = Thm.dest_fun neg_pat
val dest_sub = dest_binop sub_tm
- in (neg_mul,sub_add,sub_tm,neg_tm,dest_sub, neg_mul |> concl |> Thm.dest_arg,
+ in (neg_mul, sub_add, sub_tm, neg_tm, dest_sub, neg_mul |> concl |> Thm.dest_arg,
sub_add |> concl |> Thm.dest_arg |> Thm.dest_arg)
end
| _ => (TrueI, TrueI, true_tm, true_tm, (fn t => (t,t)), true_tm, true_tm));
@@ -760,7 +760,7 @@
fun polynomial_neg_conv ctxt tm =
let val (l,r) = Thm.dest_comb tm in
if not (l aconvc neg_tm) then raise CTERM ("polynomial_neg_conv",[tm]) else
- let val th1 = inst_thm [(cx',r)] neg_mul
+ let val th1 = inst_thm [(cx', r)] neg_mul
val th2 = Thm.transitive th1 (Conv.arg1_conv semiring_mul_conv (concl th1))
in Thm.transitive th2 (polynomial_monomial_mul_conv ctxt (concl th2))
end
@@ -770,7 +770,7 @@
(* Subtraction. *)
fun polynomial_sub_conv ctxt tm =
let val (l,r) = dest_sub tm
- val th1 = inst_thm [(cx',l),(cy',r)] sub_add
+ val th1 = inst_thm [(cx', l), (cy', r)] sub_add
val (tm1,tm2) = Thm.dest_comb(concl th1)
val th2 = Drule.arg_cong_rule tm1 (polynomial_neg_conv ctxt tm2)
in Thm.transitive th1 (Thm.transitive th2 (polynomial_add_conv ctxt (concl th2)))
--- a/src/HOL/Tools/split_rule.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Tools/split_rule.ML Sun Jul 05 15:02:30 2015 +0200
@@ -42,7 +42,7 @@
fun split_rule_var' ctxt (t as Var (v, Type ("fun", [T1, T2]))) rl =
let val T' = HOLogic.flatten_tupleT T1 ---> T2;
val newt = ap_split T1 T2 (Var (v, T'));
- in Thm.instantiate ([], [apply2 (Thm.cterm_of ctxt) (t, newt)]) rl end
+ in Thm.instantiate ([], [(dest_Var t, Thm.cterm_of ctxt newt)]) rl end
| split_rule_var' _ _ rl = rl;
@@ -65,15 +65,15 @@
val ys = Name.variant_list xs (replicate (length Ts) a);
in
(xs @ ys,
- apply2 (Thm.cterm_of ctxt)
- (v, HOLogic.mk_ptuple (HOLogic.flat_tupleT_paths T) T
- (map (Var o apfst (rpair 0)) (ys ~~ Ts))) :: insts)
+ (dest_Var v,
+ Thm.cterm_of ctxt (HOLogic.mk_ptuple (HOLogic.flat_tupleT_paths T) T
+ (map (Var o apfst (rpair 0)) (ys ~~ Ts)))) :: insts)
end
| mk_tuple _ x = x;
val newt = ap_split' Us U (Var (v, T'));
val (vs', insts) = fold mk_tuple ts (vs, []);
in
- (Drule.instantiate_normalize ([], [apply2 (Thm.cterm_of ctxt) (t, newt)] @ insts) rl, vs')
+ (Drule.instantiate_normalize ([], ((v, T), Thm.cterm_of ctxt newt) :: insts) rl, vs')
end
| complete_split_rule_var _ _ x = x;
--- a/src/Provers/Arith/fast_lin_arith.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML Sun Jul 05 15:02:30 2015 +0200
@@ -424,7 +424,7 @@
val T = Thm.typ_of_cterm cv
in
mth
- |> Thm.instantiate ([], [(cv, number_of T n)])
+ |> Thm.instantiate ([], [(dest_Var (Thm.term_of cv), number_of T n)])
|> rewrite_concl
|> discharge_prem
handle CTERM _ => mult_by_add n thm
--- a/src/Provers/hypsubst.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/Provers/hypsubst.ML Sun Jul 05 15:02:30 2015 +0200
@@ -186,10 +186,10 @@
val (instT, _) = Thm.match (apply2 (Thm.cterm_of ctxt o Logic.mk_type) (V, U));
in
compose_tac ctxt (true, Drule.instantiate_normalize (instT,
- map (apply2 (Thm.cterm_of ctxt))
- [(Var (ixn, Ts ---> U --> body_type T), u),
- (Var (fst (dest_Var (head_of v1)), Ts ---> U), fold_rev Term.abs ps t),
- (Var (fst (dest_Var (head_of v2)), Ts ---> U), fold_rev Term.abs ps t')]) rl',
+ map (apsnd (Thm.cterm_of ctxt))
+ [((ixn, Ts ---> U --> body_type T), u),
+ ((fst (dest_Var (head_of v1)), Ts ---> U), fold_rev Term.abs ps t),
+ ((fst (dest_Var (head_of v2)), Ts ---> U), fold_rev Term.abs ps t')]) rl',
Thm.nprems_of rl) i
end
| NONE => no_tac);
--- a/src/Pure/Isar/element.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/Pure/Isar/element.ML Sun Jul 05 15:02:30 2015 +0200
@@ -201,7 +201,7 @@
SOME C =>
let
val thesis = Var ((Auto_Bind.thesisN, Thm.maxidx_of th + 1), fastype_of C);
- val th' = Thm.instantiate ([], [apply2 (Thm.cterm_of ctxt) (C, thesis)]) th;
+ val th' = Thm.instantiate ([], [(Term.dest_Var C, Thm.cterm_of ctxt thesis)]) th;
in (th', true) end
| NONE => (th, false));
@@ -340,7 +340,7 @@
fun instantiate_tfrees thy subst th =
let
val idx = Thm.maxidx_of th + 1;
- fun cert_inst (a, (S, T)) = apply2 (Thm.global_ctyp_of thy) (TVar ((a, idx), S), T);
+ fun cert_inst (a, (S, T)) = (((a, idx), S), Thm.global_ctyp_of thy T);
fun add_inst (a, S) insts =
if AList.defined (op =) insts a then insts
--- a/src/Pure/Isar/generic_target.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/Pure/Isar/generic_target.ML Sun Jul 05 15:02:30 2015 +0200
@@ -271,12 +271,13 @@
|>> map Logic.dest_type;
val instT = map_filter (fn (TVar v, T) => SOME (v, T) | _ => NONE) (tvars ~~ tfrees);
- val inst = filter (is_Var o fst) (vars ~~ frees);
- val cinstT = instT
- |> map (apply2 (Thm.ctyp_of ctxt) o apfst TVar);
- val cinst = inst
- |> map (apply2 (Thm.cterm_of ctxt o Term.map_types (Term_Subst.instantiateT instT)));
- val result' = Thm.instantiate (cinstT, cinst) result;
+ val inst =
+ map_filter
+ (fn (Var (xi, T), t) =>
+ SOME ((xi, Term_Subst.instantiateT instT T),
+ Thm.cterm_of ctxt (Term.map_types (Term_Subst.instantiateT instT) t))
+ | _ => NONE) (vars ~~ frees);
+ val result' = Thm.instantiate (map (apsnd (Thm.ctyp_of ctxt)) instT, inst) result;
(*import assumes/defines*)
val result'' =
--- a/src/Pure/Isar/obtain.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/Pure/Isar/obtain.ML Sun Jul 05 15:02:30 2015 +0200
@@ -334,7 +334,7 @@
val instT =
fold (Term.add_tvarsT o #2) params []
- |> map (TVar #> (fn T => apply2 (Thm.ctyp_of ctxt) (T, norm_type T)));
+ |> map (fn v => (v, Thm.ctyp_of ctxt (norm_type (TVar v))));
val closed_rule = rule
|> Thm.forall_intr (Thm.cterm_of ctxt (Free thesis_var))
|> Thm.instantiate (instT, []);
--- a/src/Pure/Isar/subgoal.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/Pure/Isar/subgoal.ML Sun Jul 05 15:02:30 2015 +0200
@@ -12,8 +12,9 @@
signature SUBGOAL =
sig
- type focus = {context: Proof.context, params: (string * cterm) list, prems: thm list,
- asms: cterm list, concl: cterm, schematics: (ctyp * ctyp) list * (cterm * cterm) list}
+ type focus =
+ {context: Proof.context, params: (string * cterm) list, prems: thm list, asms: cterm list,
+ concl: cterm, schematics: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list}
val focus_params: Proof.context -> int -> thm -> focus * thm
val focus_params_fixed: Proof.context -> int -> thm -> focus * thm
val focus_prems: Proof.context -> int -> thm -> focus * thm
@@ -36,8 +37,9 @@
(* focus *)
-type focus = {context: Proof.context, params: (string * cterm) list, prems: thm list,
- asms: cterm list, concl: cterm, schematics: (ctyp * ctyp) list * (cterm * cterm) list};
+type focus =
+ {context: Proof.context, params: (string * cterm) list, prems: thm list, asms: cterm list,
+ concl: cterm, schematics: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list};
fun gen_focus (do_prems, do_concl) ctxt i raw_st =
let
@@ -100,7 +102,7 @@
val (inst1, inst2) =
split_list (map (apply2 (apply2 (Thm.cterm_of ctxt))) (map2 var_inst vars ys));
- val th'' = Thm.instantiate ([], inst1) th';
+ val th'' = Thm.instantiate ([], map (apfst (Term.dest_Var o Thm.term_of)) inst1) th';
in ((inst2, th''), ctxt'') end;
(*
--- a/src/Pure/Proof/proof_checker.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/Pure/Proof/proof_checker.ML Sun Jul 05 15:02:30 2015 +0200
@@ -78,8 +78,8 @@
let
val tvars = Term.add_tvars (Thm.full_prop_of thm) [] |> rev;
val (fmap, thm') = Thm.varifyT_global' [] thm;
- val ctye = map (apply2 (Thm.global_ctyp_of thy))
- (map TVar tvars @ map (fn ((_, S), ixn) => TVar (ixn, S)) fmap ~~ Ts)
+ val ctye =
+ (tvars @ map (fn ((_, S), ixn) => (ixn, S)) fmap ~~ map (Thm.global_ctyp_of thy) Ts);
in
Thm.instantiate (ctye, []) (forall_intr_vars (Thm.forall_intr_frees thm'))
end;
@@ -118,7 +118,7 @@
handle THM (s, _, _) => appl_error thy pretty_term vs Hs s prf t
end
- | thm_of (vs, names) Hs (AbsP (s, SOME t, prf)) =
+ | thm_of (vs, names) Hs (AbsP (_, SOME t, prf)) =
let
val ct = Thm.global_cterm_of thy (Term.subst_bounds (map Free vs, t));
val thm = thm_of (vs, names) (Thm.assume ct :: Hs) prf;
--- a/src/Pure/Tools/rule_insts.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/Pure/Tools/rule_insts.ML Sun Jul 05 15:02:30 2015 +0200
@@ -149,8 +149,8 @@
in
thm
|> Drule.instantiate_normalize
- (map (apply2 (Thm.ctyp_of ctxt') o apfst TVar) inst_tvars,
- map (apply2 (Thm.cterm_of ctxt') o apfst Var) inst_vars)
+ (map (apsnd (Thm.ctyp_of ctxt')) inst_tvars,
+ map (apsnd (Thm.cterm_of ctxt')) inst_vars)
|> singleton (Variable.export ctxt' ctxt)
|> Rule_Cases.save thm
end;
@@ -240,13 +240,13 @@
val inc = Thm.maxidx_of st + 1;
val lift_type = Logic.incr_tvar inc;
- fun lift_var ((a, j), T) = Var ((a, j + inc), paramTs ---> lift_type T);
+ fun lift_var ((a, j), T) = ((a, j + inc), paramTs ---> lift_type T);
fun lift_term t = fold_rev Term.absfree params (Logic.incr_indexes (fixed, paramTs, inc) t);
val inst_tvars' = inst_tvars
- |> map (apply2 (Thm.ctyp_of inst_ctxt o lift_type) o apfst TVar);
+ |> map (fn (((a, i), S), T) => (((a, i + inc), S), Thm.ctyp_of inst_ctxt (lift_type T)));
val inst_vars' = inst_vars
- |> map (fn (v, t) => apply2 (Thm.cterm_of inst_ctxt) (lift_var v, lift_term t));
+ |> map (fn (v, t) => (lift_var v, Thm.cterm_of inst_ctxt (lift_term t)));
val thm' = Thm.lift_rule cgoal thm
|> Drule.instantiate_normalize (inst_tvars', inst_vars')
@@ -262,10 +262,11 @@
fun make_elim_preserve ctxt rl =
let
val maxidx = Thm.maxidx_of rl;
+ fun var x = ((x, 0), propT);
fun cvar xi = Thm.cterm_of ctxt (Var (xi, propT));
val revcut_rl' =
- Drule.instantiate_normalize ([], [(cvar ("V", 0), cvar ("V", maxidx + 1)),
- (cvar ("W", 0), cvar ("W", maxidx + 1))]) Drule.revcut_rl;
+ Drule.instantiate_normalize ([], [(var "V", cvar ("V", maxidx + 1)),
+ (var "W", cvar ("W", maxidx + 1))]) Drule.revcut_rl;
in
(case Seq.list_of
(Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = false}
--- a/src/Pure/conjunction.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/Pure/conjunction.ML Sun Jul 05 15:02:30 2015 +0200
@@ -69,8 +69,8 @@
local
-val A = read_prop "A" and vA = read_prop "?A";
-val B = read_prop "B" and vB = read_prop "?B";
+val A = read_prop "A" and vA = (("A", 0), propT);
+val B = read_prop "B" and vB = (("B", 0), propT);
val C = read_prop "C";
val ABC = read_prop "A ==> B ==> C";
val A_B = read_prop "A &&& B";
--- a/src/Pure/drule.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/Pure/drule.ML Sun Jul 05 15:02:30 2015 +0200
@@ -20,7 +20,8 @@
val lift_all: Proof.context -> cterm -> thm -> thm
val implies_elim_list: thm -> thm list -> thm
val implies_intr_list: cterm list -> thm -> thm
- val instantiate_normalize: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm
+ val instantiate_normalize: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list ->
+ thm -> thm
val zero_var_indexes_list: thm list -> thm list
val zero_var_indexes: thm -> thm
val implies_intr_hyps: thm -> thm
@@ -613,11 +614,9 @@
fun mk_term ct =
let
- val thy = Thm.theory_of_cterm ct;
- val T = Thm.typ_of_cterm ct;
- val instT = apply2 (Thm.global_ctyp_of thy) (TVar (("'a", 0), []), T);
- val x = Thm.global_cterm_of thy (Var (("x", 0), T));
- in Thm.instantiate ([instT], [(x, ct)]) termI end;
+ val cT = Thm.ctyp_of_cterm ct;
+ val T = Thm.typ_of cT;
+ in Thm.instantiate ([((("'a", 0), []), cT)], [((("x", 0), T), ct)]) termI end;
fun dest_term th =
let val cprop = strip_imp_concl (Thm.cprop_of th) in
@@ -767,9 +766,9 @@
val (thy, tye, _) = fold_rev add_types ctpairs (Thm.theory_of_thm th, Vartab.empty, 0);
val instT =
Vartab.fold (fn (xi, (S, T)) =>
- cons (apply2 (Thm.global_ctyp_of thy) (TVar (xi, S), Envir.norm_type tye T))) tye [];
+ cons ((xi, S), Thm.global_ctyp_of thy (Envir.norm_type tye T))) tye [];
val inst = map (apply2 (Thm.instantiate_cterm (instT, []))) ctpairs;
- in instantiate_normalize (instT, inst) th end
+ in instantiate_normalize (instT, map (apfst (Thm.term_of #> dest_Var)) inst) th end
handle TERM (msg, _) => raise THM (msg, 0, [th])
| TYPE (msg, _, _) => raise THM (msg, 0, [th]);
end;
@@ -784,27 +783,18 @@
map_filter (Option.map Thm.typ_of) cTs,
map_filter (Option.map Thm.term_of) cts);
- fun inst_of (v, ct) =
- (Thm.global_cterm_of (Thm.theory_of_cterm ct) (Var v), ct)
- handle TYPE (msg, _, _) => err msg;
-
- fun tyinst_of (v, cT) =
- (Thm.global_ctyp_of (Thm.theory_of_ctyp cT) (TVar v), cT)
- handle TYPE (msg, _, _) => err msg;
-
fun zip_vars xs ys =
zip_options xs ys handle ListPair.UnequalLengths =>
err "more instantiations than variables in thm";
- (*instantiate types first!*)
val thm' =
if forall is_none cTs then thm
- else Thm.instantiate
- (map tyinst_of (zip_vars (rev (Thm.fold_terms Term.add_tvars thm [])) cTs), []) thm;
+ else
+ Thm.instantiate ((zip_vars (rev (Thm.fold_terms Term.add_tvars thm [])) cTs), []) thm;
val thm'' =
if forall is_none cts then thm'
- else Thm.instantiate
- ([], map inst_of (zip_vars (rev (Thm.fold_terms Term.add_vars thm' [])) cts)) thm';
+ else
+ Thm.instantiate ([], zip_vars (rev (Thm.fold_terms Term.add_vars thm' [])) cts) thm';
in thm'' end;
--- a/src/Pure/goal.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/Pure/goal.ML Sun Jul 05 15:02:30 2015 +0200
@@ -60,9 +60,7 @@
-------- (init)
C ==> #C
*)
-val init =
- let val A = #1 (Thm.dest_implies (Thm.cprop_of Drule.protectI))
- in fn C => Thm.instantiate ([], [(A, C)]) Drule.protectI end;
+fun init C = Thm.instantiate ([], [((("A", 0), propT), C)]) Drule.protectI;
(*
A1 ==> ... ==> An ==> C
@@ -134,8 +132,7 @@
val fixes = map (Thm.cterm_of ctxt) xs;
val tfrees = fold Term.add_tfrees (prop :: As) [];
- val instT =
- map (fn (a, S) => apply2 (Thm.ctyp_of ctxt) (TVar ((a, 0), S), TFree (a, S))) tfrees;
+ val instT = map (fn (a, S) => (((a, 0), S), Thm.ctyp_of ctxt (TFree (a, S)))) tfrees;
val global_prop =
Logic.varify_types_global (fold_rev Logic.all xs (Logic.list_implies (As, prop)))
--- a/src/Pure/more_thm.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/Pure/more_thm.ML Sun Jul 05 15:02:30 2015 +0200
@@ -62,12 +62,12 @@
val forall_elim_vars: int -> thm -> thm
val global_certify_inst: theory ->
((indexname * sort) * typ) list * ((indexname * typ) * term) list ->
- (ctyp * ctyp) list * (cterm * cterm) list
+ ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list
val global_certify_instantiate: theory ->
((indexname * sort) * typ) list * ((indexname * typ) * term) list -> thm -> thm
val certify_inst: Proof.context ->
((indexname * sort) * typ) list * ((indexname * typ) * term) list ->
- (ctyp * ctyp) list * (cterm * cterm) list
+ ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list
val certify_instantiate: Proof.context ->
((indexname * sort) * typ) list * ((indexname * typ) * term) list -> thm -> thm
val forall_intr_frees: thm -> thm
@@ -357,15 +357,15 @@
(* certify_instantiate *)
fun global_certify_inst thy (instT, inst) =
- (map (fn (v, T) => apply2 (Thm.global_ctyp_of thy) (TVar v, T)) instT,
- map (fn (v, t) => apply2 (Thm.global_cterm_of thy) (Var v, t)) inst);
+ (map (apsnd (Thm.global_ctyp_of thy)) instT,
+ map (apsnd (Thm.global_cterm_of thy)) inst);
fun global_certify_instantiate thy insts th =
Thm.instantiate (global_certify_inst thy insts) th;
fun certify_inst ctxt (instT, inst) =
- (map (fn (v, T) => apply2 (Thm.ctyp_of ctxt) (TVar v, T)) instT,
- map (fn (v, t) => apply2 (Thm.cterm_of ctxt) (Var v, t)) inst);
+ (map (apsnd (Thm.ctyp_of ctxt)) instT,
+ map (apsnd (Thm.cterm_of ctxt)) inst);
fun certify_instantiate ctxt insts th =
Thm.instantiate (certify_inst ctxt insts) th;
@@ -446,10 +446,12 @@
fun stripped_sorts thy t =
let
- val tfrees = rev (map TFree (Term.add_tfrees t []));
- val tfrees' = map (fn a => TFree (a, [])) (Name.invent Name.context Name.aT (length tfrees));
- val strip = tfrees ~~ tfrees';
- val recover = map (apply2 (Thm.global_ctyp_of thy o Logic.varifyT_global) o swap) strip;
+ val tfrees = rev (Term.add_tfrees t []);
+ val tfrees' = map (fn a => (a, [])) (Name.invent Name.context Name.aT (length tfrees));
+ val recover =
+ map2 (fn (a', S') => fn (a, S) => (((a', 0), S'), Thm.global_ctyp_of thy (TVar ((a, 0), S))))
+ tfrees' tfrees;
+ val strip = map (apply2 TFree) (tfrees ~~ tfrees');
val t' = Term.map_types (Term.map_atyps (perhaps (AList.lookup (op =) strip))) t;
in (strip, recover, t') end;
--- a/src/Pure/raw_simplifier.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/Pure/raw_simplifier.ML Sun Jul 05 15:02:30 2015 +0200
@@ -1044,8 +1044,9 @@
then NONE else SOME thm2'))
end;
-val (cA, (cB, cC)) =
- apsnd Thm.dest_equals (Thm.dest_implies (hd (cprems_of Drule.imp_cong)));
+val vA = (("A", 0), propT);
+val vB = (("B", 0), propT);
+val vC = (("C", 0), propT);
fun transitive1 NONE NONE = NONE
| transitive1 (SOME thm1) NONE = SOME thm1
@@ -1177,7 +1178,7 @@
val (lhs, rhs) = Thm.dest_equals (Thm.cprop_of eq);
val eq' =
Thm.implies_elim
- (Thm.instantiate ([], [(cA, prem), (cB, lhs), (cC, rhs)]) Drule.imp_cong)
+ (Thm.instantiate ([], [(vA, prem), (vB, lhs), (vC, rhs)]) Drule.imp_cong)
(Thm.implies_intr prem eq);
in
if not r then eq'
@@ -1188,9 +1189,9 @@
in
Thm.transitive
(Thm.transitive
- (Thm.instantiate ([], [(cA, prem'), (cB, prem), (cC, concl)]) Drule.swap_prems_eq)
+ (Thm.instantiate ([], [(vA, prem'), (vB, prem), (vC, concl)]) Drule.swap_prems_eq)
eq')
- (Thm.instantiate ([], [(cA, prem), (cB, prem''), (cC, concl)]) Drule.swap_prems_eq)
+ (Thm.instantiate ([], [(vA, prem), (vB, prem''), (vC, concl)]) Drule.swap_prems_eq)
end
end
--- a/src/Pure/thm.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/Pure/thm.ML Sun Jul 05 15:02:30 2015 +0200
@@ -47,8 +47,10 @@
val lambda: cterm -> cterm -> cterm
val adjust_maxidx_cterm: int -> cterm -> cterm
val incr_indexes_cterm: int -> cterm -> cterm
- val match: cterm * cterm -> (ctyp * ctyp) list * (cterm * cterm) list
- val first_order_match: cterm * cterm -> (ctyp * ctyp) list * (cterm * cterm) list
+ val match: cterm * cterm ->
+ ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list
+ val first_order_match: cterm * cterm ->
+ ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list
(*theorems*)
val rep_thm: thm ->
{thy: theory,
@@ -120,8 +122,10 @@
val equal_elim: thm -> thm -> thm
val flexflex_rule: Proof.context option -> thm -> thm Seq.seq
val generalize: string list * string list -> int -> thm -> thm
- val instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm
- val instantiate_cterm: (ctyp * ctyp) list * (cterm * cterm) list -> cterm -> cterm
+ val instantiate: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list ->
+ thm -> thm
+ val instantiate_cterm: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list ->
+ cterm -> cterm
val trivial: cterm -> thm
val of_class: ctyp * class -> thm
val strip_shyps: thm -> thm
@@ -312,12 +316,10 @@
val (Tinsts, tinsts) = match thy (t1, t2) (Vartab.empty, Vartab.empty);
val sorts = Sorts.union sorts1 sorts2;
fun mk_cTinst ((a, i), (S, T)) =
- (Ctyp {T = TVar ((a, i), S), thy = thy, maxidx = i, sorts = sorts},
- Ctyp {T = T, thy = thy, maxidx = maxidx2, sorts = sorts});
- fun mk_ctinst ((x, i), (T, t)) =
- let val T = Envir.subst_type Tinsts T in
- (Cterm {t = Var ((x, i), T), T = T, thy = thy, maxidx = i, sorts = sorts},
- Cterm {t = t, T = T, thy = thy, maxidx = maxidx2, sorts = sorts})
+ (((a, i), S), Ctyp {T = T, thy = thy, maxidx = maxidx2, sorts = sorts});
+ fun mk_ctinst ((x, i), (U, t)) =
+ let val T = Envir.subst_type Tinsts U in
+ (((x, i), T), Cterm {t = t, T = T, thy = thy, maxidx = maxidx2, sorts = sorts})
end;
in (Vartab.fold (cons o mk_cTinst) Tinsts [], Vartab.fold (cons o mk_ctinst) tinsts []) end;
@@ -1091,37 +1093,28 @@
fun pretty_typing thy t T = Pretty.block
[Syntax.pretty_term_global thy t, Pretty.str " ::", Pretty.brk 1, Syntax.pretty_typ_global thy T];
-fun add_inst (ct, cu) (thy, sorts) =
+fun add_inst (v as (_, T), cu) (thy, sorts) =
let
- val Cterm {t = t, T = T, ...} = ct;
- val Cterm {t = u, T = U, sorts = sorts_u, maxidx = maxidx_u, ...} = cu;
- val thy' = Theory.merge (thy, merge_thys0 ct cu);
+ val Cterm {t = u, T = U, thy = thy2, sorts = sorts_u, maxidx = maxidx_u, ...} = cu;
+ val thy' = Theory.merge (thy, thy2);
val sorts' = Sorts.union sorts_u sorts;
in
- (case t of Var v =>
- if T = U then ((v, (u, maxidx_u)), (thy', sorts'))
- else raise TYPE (Pretty.string_of (Pretty.block
+ if T = U then ((v, (u, maxidx_u)), (thy', sorts'))
+ else
+ raise TYPE (Pretty.string_of (Pretty.block
[Pretty.str "instantiate: type conflict",
- Pretty.fbrk, pretty_typing thy' t T,
- Pretty.fbrk, pretty_typing thy' u U]), [T, U], [t, u])
- | _ => raise TYPE (Pretty.string_of (Pretty.block
- [Pretty.str "instantiate: not a variable",
- Pretty.fbrk, Syntax.pretty_term_global thy' t]), [], [t]))
+ Pretty.fbrk, pretty_typing thy' (Var v) T,
+ Pretty.fbrk, pretty_typing thy' u U]), [T, U], [Var v, u])
end;
-fun add_instT (cT, cU) (thy, sorts) =
+fun add_instT (v as (_, S), cU) (thy, sorts) =
let
- val Ctyp {T, thy = thy1, ...} = cT
- and Ctyp {T = U, thy = thy2, sorts = sorts_U, maxidx = maxidx_U, ...} = cU;
- val thy' = Theory.merge (thy, Theory.merge (thy1, thy2));
+ val Ctyp {T = U, thy = thy2, sorts = sorts_U, maxidx = maxidx_U, ...} = cU;
+ val thy' = Theory.merge (thy, thy2);
val sorts' = Sorts.union sorts_U sorts;
in
- (case T of TVar (v as (_, S)) =>
- if Sign.of_sort thy' (U, S) then ((v, (U, maxidx_U)), (thy', sorts'))
- else raise TYPE ("Type not of sort " ^ Syntax.string_of_sort_global thy' S, [U], [])
- | _ => raise TYPE (Pretty.string_of (Pretty.block
- [Pretty.str "instantiate: not a type variable",
- Pretty.fbrk, Syntax.pretty_typ_global thy' T]), [T], []))
+ if Sign.of_sort thy' (U, S) then ((v, (U, maxidx_U)), (thy', sorts'))
+ else raise TYPE ("Type not of sort " ^ Syntax.string_of_sort_global thy' S, [U], [])
end;
in
--- a/src/Pure/variable.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/Pure/variable.ML Sun Jul 05 15:02:30 2015 +0200
@@ -71,10 +71,11 @@
(((indexname * sort) * typ) list * ((indexname * typ) * term) list) * Proof.context
val importT_terms: term list -> Proof.context -> term list * Proof.context
val import_terms: bool -> term list -> Proof.context -> term list * Proof.context
- val importT: thm list -> Proof.context -> ((ctyp * ctyp) list * thm list) * Proof.context
+ val importT: thm list -> Proof.context ->
+ (((indexname * sort) * ctyp) list * thm list) * Proof.context
val import_prf: bool -> Proofterm.proof -> Proof.context -> Proofterm.proof * Proof.context
val import: bool -> thm list -> Proof.context ->
- (((ctyp * ctyp) list * (cterm * cterm) list) * thm list) * Proof.context
+ ((((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list) * thm list) * Proof.context
val tradeT: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
val trade: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
val focus_params: term -> Proof.context -> (string list * (string * typ) list) * Proof.context
--- a/src/Tools/IsaPlanner/rw_inst.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/Tools/IsaPlanner/rw_inst.ML Sun Jul 05 15:02:30 2015 +0200
@@ -174,7 +174,7 @@
val typinsts = cross_inst_typs (nonfixed_typinsts @ fixtyinsts);
(* certified instantiations for types *)
- val ctyp_insts = map (fn (ix, (s, ty)) => apply2 (Thm.ctyp_of ctxt) (TVar (ix, s), ty)) typinsts;
+ val ctyp_insts = map (fn (ix, (s, ty)) => ((ix, s), Thm.ctyp_of ctxt ty)) typinsts;
(* type instantiated versions *)
val tgt_th_tyinst = Thm.instantiate (ctyp_insts,[]) target_thm;
@@ -198,7 +198,7 @@
(* create certms of instantiations *)
val cinsts_tyinst =
- map (fn (ix, (ty, t)) => apply2 (Thm.cterm_of ctxt) (Var (ix, ty), t)) insts_tyinst_inst;
+ map (fn (ix, (ty, t)) => ((ix, ty), Thm.cterm_of ctxt t)) insts_tyinst_inst;
(* The instantiated rule *)
val rule_inst = rule_tyinst |> Thm.instantiate ([], cinsts_tyinst);
@@ -217,7 +217,7 @@
val couter_inst = Thm.reflexive (Thm.cterm_of ctxt outerterm_inst);
val (cprems, abstract_rule_inst) =
rule_inst
- |> Thm.instantiate ([], cterm_renamings)
+ |> Thm.instantiate ([], map (apfst (dest_Var o Thm.term_of)) cterm_renamings)
|> mk_abstractedrule ctxt FakeTs_tyinst Ts_tyinst;
val specific_tgt_rule =
Conv.fconv_rule Drule.beta_eta_conversion
@@ -227,7 +227,7 @@
val tgt_th_inst =
tgt_th_tyinst
|> Thm.instantiate ([], cinsts_tyinst)
- |> Thm.instantiate ([], cterm_renamings);
+ |> Thm.instantiate ([], map (apfst (dest_Var o Thm.term_of)) cterm_renamings);
val (vars,frees_of_fixed_vars) = Library.split_list cterm_renamings;
in
--- a/src/Tools/coherent.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/Tools/coherent.ML Sun Jul 05 15:02:30 2015 +0200
@@ -179,10 +179,10 @@
val th' =
Drule.implies_elim_list
(Thm.instantiate
- (map (fn (ixn, (S, T)) => apply2 (Thm.ctyp_of ctxt) (TVar (ixn, S), T)) (Vartab.dest tye),
+ (map (fn (ixn, (S, T)) => ((ixn, S), Thm.ctyp_of ctxt T)) (Vartab.dest tye),
map (fn (ixn, (T, t)) =>
- apply2 (Thm.cterm_of ctxt) (Var (ixn, Envir.subst_type tye T), t)) (Vartab.dest env) @
- map (fn (ixnT, t) => apply2 (Thm.cterm_of ctxt) (Var ixnT, t)) insts) th)
+ ((ixn, Envir.subst_type tye T), Thm.cterm_of ctxt t)) (Vartab.dest env) @
+ map (fn (ixnT, t) => (ixnT, Thm.cterm_of ctxt t)) insts) th)
(map (nth asms) is);
val (_, cases) = dest_elim (Thm.prop_of th');
in
--- a/src/Tools/induct.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/Tools/induct.ML Sun Jul 05 15:02:30 2015 +0200
@@ -573,8 +573,8 @@
val pairs = Vartab.dest (Envir.term_env env);
val types = Vartab.dest (Envir.type_env env);
val ts = map (Thm.cterm_of ctxt o Envir.norm_term env o #2 o #2) pairs;
- val xs = map2 (curry (Thm.cterm_of ctxt o Var)) (map #1 pairs) (map Thm.typ_of_cterm ts);
- in (map (fn (xi, (S, T)) => apply2 (Thm.ctyp_of ctxt) (TVar (xi, S), T)) types, xs ~~ ts) end;
+ val xs = map #1 pairs ~~ map Thm.typ_of_cterm ts;
+ in (map (fn (ai, (S, T)) => ((ai, S), Thm.ctyp_of ctxt T)) types, xs ~~ ts) end;
in
--- a/src/Tools/misc_legacy.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/Tools/misc_legacy.ML Sun Jul 05 15:02:30 2015 +0200
@@ -173,9 +173,9 @@
then ((v, T), true, free_of "METAHYP2_" (v, T))
else ((v, T), false, free_of "METAHYP2_" (v, map #2 params ---> T))
(*Instantiate subgoal vars by Free applied to params*)
- fun mk_ctpair (v, in_concl, u) =
- if in_concl then apply2 (Thm.cterm_of ctxt) (Var v, u)
- else apply2 (Thm.cterm_of ctxt) (Var v, list_comb (u, fparams))
+ fun mk_inst (v, in_concl, u) =
+ if in_concl then (v, Thm.cterm_of ctxt u)
+ else (v, Thm.cterm_of ctxt (list_comb (u, fparams)))
(*Restore Vars with higher type and index*)
fun mk_subgoal_swap_ctpair (((a, i), T), in_concl, u as Free (_, U)) =
if in_concl then apply2 (Thm.cterm_of ctxt) (u, Var ((a, i), T))
@@ -191,7 +191,7 @@
fold Term.add_vars (Logic.strip_imp_prems prop) []
and concl_vars = Term.add_vars (Logic.strip_imp_concl prop) []
val subgoal_insts = map (mk_subgoal_inst concl_vars) subgoal_vars
- val st' = Thm.instantiate ([], map mk_ctpair subgoal_insts) st
+ val st' = Thm.instantiate ([], map mk_inst subgoal_insts) st
val emBs = map (Thm.cterm_of ctxt o embed) (Thm.prems_of st')
val Cth = implies_elim_list st' (map (elim o Thm.assume) emBs)
in (*restore the unknowns to the hypotheses*)
@@ -269,7 +269,7 @@
fun thaw i th' = (*i is non-negative increment for Var indexes*)
th' |> forall_intr_list (map #2 insts)
|> forall_elim_list (map (Thm.incr_indexes_cterm i o #1) insts)
- in (Thm.instantiate ([],insts) fth, thaw) end
+ in (Thm.instantiate ([], map (apfst (dest_Var o Thm.term_of)) insts) fth, thaw) end
end;
(*Basic version of the function above. No option to rename Vars apart in thaw.
@@ -291,7 +291,7 @@
fun thaw th' =
th' |> forall_intr_list (map #2 insts)
|> forall_elim_list (map #1 insts)
- in (Thm.instantiate ([],insts) fth, thaw) end
+ in (Thm.instantiate ([], map (apfst (dest_Var o Thm.term_of)) insts) fth, thaw) end
end;
end;
--- a/src/Tools/nbe.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/Tools/nbe.ML Sun Jul 05 15:02:30 2015 +0200
@@ -101,11 +101,10 @@
val vs_tab = map mk_entry (Term.add_tfrees (Thm.term_of ct) []);
fun instantiate thm =
let
- val cert_tvars = map (Thm.ctyp_of ctxt o TVar) (Term.add_tvars
- ((fst o Logic.dest_equals o Logic.strip_imp_concl o Thm.prop_of) thm) []);
- val instantiation =
- map2 (fn cert_tvar => fn (_, (_, (cT, _))) => (cert_tvar, cT)) cert_tvars vs_tab;
- in Thm.instantiate (instantiation, []) thm end;
+ val tvars =
+ Term.add_tvars (#1 (Logic.dest_equals (Logic.strip_imp_concl (Thm.prop_of thm)))) [];
+ val instT = map2 (fn v => fn (_, (_, (cT, _))) => (v, cT)) tvars vs_tab;
+ in Thm.instantiate (instT, []) thm end;
fun of_class (TFree (v, _), class) =
the (AList.lookup (op =) ((snd o snd o the o AList.lookup (op =) vs_tab) v) class)
| of_class (T, _) = error ("Bad type " ^ Syntax.string_of_typ ctxt T);
--- a/src/ZF/Tools/cartprod.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/ZF/Tools/cartprod.ML Sun Jul 05 15:02:30 2015 +0200
@@ -109,7 +109,7 @@
in
remove_split ctxt
(Drule.instantiate_normalize ([],
- [apply2 (Thm.cterm_of ctxt) (Var(v, Ind_Syntax.iT-->T2), newt)]) rl)
+ [((v, Ind_Syntax.iT-->T2), Thm.cterm_of ctxt newt)]) rl)
end
| split_rule_var _ (t,T,rl) = rl;
--- a/src/ZF/Tools/inductive_package.ML Fri Jul 03 16:19:45 2015 +0200
+++ b/src/ZF/Tools/inductive_package.ML Sun Jul 05 15:02:30 2015 +0200
@@ -495,7 +495,7 @@
The name "x.1" comes from the "RS spec" !*)
val inst =
case elem_frees of [_] => I
- | _ => Drule.instantiate_normalize ([], [(Thm.global_cterm_of thy (Var(("x",1), Ind_Syntax.iT)),
+ | _ => Drule.instantiate_normalize ([], [(((("x",1), Ind_Syntax.iT)),
Thm.global_cterm_of thy elem_tuple)]);
(*strip quantifier and the implication*)