diff -r 4af8a92396ce -r c4f31f1564b7 Nominal/nominal_dt_quot.ML --- 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)