--- a/Nominal/nominal_dt_quot.ML Mon Jul 20 11:21:59 2015 +0100
+++ b/Nominal/nominal_dt_quot.ML Sat Mar 19 21:06:48 2016 +0000
@@ -61,7 +61,7 @@
val qty_args2 = map2 (fn descr => fn args1 => (descr, args1, (NONE, NONE))) qtys_descr qty_args1
val qty_args3 = qty_args2 ~~ alpha_equivp_thms
in
- fold_map Quotient_Type.add_quotient_type qty_args3 lthy
+ fold_map (Quotient_Type.add_quotient_type {overloaded = false}) qty_args3 lthy
end
(* a wrapper for lifting a raw constant *)
@@ -73,7 +73,7 @@
val rhs_raw = rconst
val raw_var = (Binding.name qconst_name, NONE, mx')
- val ([(binding, _, mx)], ctxt) = Proof_Context.cert_vars [raw_var] lthy
+ val ((binding, _, mx), ctxt) = Proof_Context.cert_var raw_var lthy
val lhs = Syntax.check_term ctxt lhs_raw
val rhs = Syntax.check_term ctxt rhs_raw
@@ -91,7 +91,9 @@
let
val (qconst_infos, lthy') =
fold_map (lift_raw_const qtys) consts_specs lthy
- val phi = Proof_Context.export_morphism lthy' lthy
+ val phi =
+ Proof_Context.export_morphism lthy'
+ (Proof_Context.transfer (Proof_Context.theory_of lthy') lthy)
in
(map (Quotient_Info.transform_quotconsts phi) qconst_infos, lthy')
end
@@ -153,14 +155,14 @@
|> fst
end
-fun unraw_vars_thm thm =
+fun unraw_vars_thm ctxt thm =
let
fun unraw_var_str ((s, i), T) = ((unraw_str s, i), T)
val vars = Term.add_vars (Thm.prop_of thm) []
- val vars' = map (Var o unraw_var_str) vars
+ val vars' = map (Thm.cterm_of ctxt o Var o unraw_var_str) vars
in
- Thm.certify_instantiate ([], (vars ~~ vars')) thm
+ Thm.instantiate ([], (vars ~~ vars')) thm
end
fun unraw_bounds_thm th =
@@ -174,7 +176,7 @@
fun lift_thms qtys simps thms ctxt =
(map (Quotient_Tacs.lifted ctxt qtys simps
#> unraw_bounds_thm
- #> unraw_vars_thm
+ #> unraw_vars_thm ctxt
#> Drule.zero_var_indexes) thms, ctxt)
@@ -228,13 +230,13 @@
|> HOLogic.mk_Trueprop
val tac =
- EVERY' [ rtac @{thm supports_finite},
+ EVERY' [ resolve_tac ctxt' @{thms supports_finite},
resolve_tac ctxt' qsupports_thms,
asm_simp_tac (put_simpset HOL_ss ctxt'
addsimps @{thms finite_supp supp_Pair finite_Un}) ]
in
Goal.prove ctxt' [] [] goals
- (K (HEADGOAL (rtac qinduct THEN_ALL_NEW tac)))
+ (K (HEADGOAL (resolve_tac ctxt' [qinduct] THEN_ALL_NEW tac)))
|> singleton (Proof_Context.export ctxt' ctxt)
|> Old_Datatype_Aux.split_conj_thm
|> map zero_var_indexes
@@ -500,7 +502,7 @@
@ @{thms finite.intros finite_Un finite_set finite_fset}
in
Goal.prove ctxt [] [] goal
- (K (HEADGOAL (rtac @{thm at_set_avoiding1}
+ (K (HEADGOAL (resolve_tac ctxt @{thms at_set_avoiding1}
THEN_ALL_NEW (simp_tac (put_simpset HOL_ss ctxt addsimps ss)))))
end
@@ -559,7 +561,7 @@
let
fun aux_tac prem bclauses =
case (get_all_binders bclauses) of
- [] => EVERY' [rtac prem, assume_tac ctxt]
+ [] => EVERY' [resolve_tac ctxt [prem], assume_tac ctxt]
| binders => Subgoal.SUBPROOF (fn {params, prems, concl, context = ctxt, ...} =>
let
val parms = map (Thm.term_of o snd) params
@@ -567,18 +569,18 @@
val ss = @{thms fresh_star_Pair union_eqvt fresh_star_Un}
val (([(_, fperm)], fprops), ctxt') = Obtain.result
- (fn ctxt' => EVERY1 [etac exE,
+ (fn ctxt' => EVERY1 [eresolve_tac ctxt [exE],
full_simp_tac (put_simpset HOL_basic_ss ctxt' addsimps ss),
- REPEAT o (etac @{thm conjE})]) [fthm] ctxt
+ REPEAT o (eresolve_tac ctxt @{thms conjE})]) [fthm] ctxt
val abs_eq_thms = flat
(map (abs_eq_thm ctxt' fprops (Thm.term_of fperm) parms bn_eqvt permute_bns) bclauses)
val ((_, eqs), ctxt'') = Obtain.result
(fn ctxt'' => EVERY1
- [ REPEAT o (etac @{thm exE}),
- REPEAT o (etac @{thm conjE}),
- REPEAT o (dtac setify),
+ [ REPEAT o (eresolve_tac ctxt @{thms exE}),
+ REPEAT o (eresolve_tac ctxt @{thms conjE}),
+ REPEAT o (dresolve_tac ctxt [setify]),
full_simp_tac (put_simpset HOL_basic_ss ctxt''
addsimps @{thms set_append set_simps})]) abs_eq_thms ctxt'
@@ -592,24 +594,24 @@
val tac1 = SOLVED' (EVERY'
[ simp_tac (put_simpset HOL_basic_ss ctxt'' addsimps peqs),
rewrite_goal_tac ctxt'' (@{thms fresh_star_Un[THEN eq_reflection]}),
- conj_tac (DETERM o resolve_tac ctxt'' fprops') ])
+ conj_tac ctxt'' (DETERM o resolve_tac ctxt'' fprops') ])
(* for equalities between constructors *)
val tac2 = SOLVED' (EVERY'
- [ rtac (@{thm ssubst} OF prems),
+ [ resolve_tac ctxt [@{thm ssubst} OF prems],
rewrite_goal_tac ctxt'' (map safe_mk_equiv eq_iff_thms),
rewrite_goal_tac ctxt'' (map safe_mk_equiv abs_eqs),
- conj_tac (DETERM o resolve_tac ctxt'' (@{thms refl} @ perm_bn_alphas)) ])
+ conj_tac ctxt'' (DETERM o resolve_tac ctxt'' (@{thms refl} @ perm_bn_alphas)) ])
(* proves goal "P" *)
val side_thm = Goal.prove ctxt'' [] [] (Thm.term_of concl)
- (K (EVERY1 [ rtac prem, RANGE [tac1, tac2] ]))
+ (K (EVERY1 [ resolve_tac ctxt'' [prem], RANGE [tac1, tac2] ]))
|> singleton (Proof_Context.export ctxt'' ctxt)
in
- rtac side_thm 1
+ resolve_tac ctxt [side_thm] 1
end) ctxt
in
- EVERY1 [rtac qexhaust_thm, RANGE (map2 aux_tac prems bclausess)]
+ EVERY1 [resolve_tac ctxt [qexhaust_thm], RANGE (map2 aux_tac prems bclausess)]
end
@@ -726,12 +728,10 @@
val ty_parms = map (fn (_, ct) => (fastype_of (Thm.term_of ct), ct)) params
val vs = Term.add_vars (Thm.prop_of thm) []
val vs_tys = map (Type.legacy_freeze_type o snd) vs
- val vs_ctrms = map (Thm.cterm_of ctxt' o Var) vs
val assigns = map (lookup ty_parms) vs_tys
-
- val thm' = cterm_instantiate (vs_ctrms ~~ assigns) thm
+ val thm' = infer_instantiate ctxt' (map #1 vs ~~ assigns) thm
in
- rtac thm' 1
+ resolve_tac ctxt' [thm'] 1
end) ctxt
THEN_ALL_NEW asm_full_simp_tac (put_simpset HOL_basic_ss ctxt)