--- a/Nominal/nominal_dt_alpha.ML Mon Jul 20 11:21:59 2015 +0100
+++ b/Nominal/nominal_dt_alpha.ML Tue Mar 22 12:18:30 2016 +0000
@@ -248,16 +248,19 @@
(alpha_names @ alpha_bn_names ~~ alpha_tys @ alpha_bn_tys)
val all_alpha_intros = map (pair Attrib.empty_binding) (flat alpha_intros @ flat alpha_bn_intros)
- val (alpha_info, lthy') = Inductive.add_inductive_i
+ val (alpha_info, lthy') = lthy
+ |> Inductive.add_inductive_i
{quiet_mode = true, verbose = false, alt_name = Binding.empty,
coind = false, no_elim = false, no_ind = false, skip_mono = false}
- all_alpha_names [] all_alpha_intros [] lthy
+ all_alpha_names [] all_alpha_intros []
val all_alpha_trms_loc = #preds alpha_info;
val alpha_raw_induct_loc = #raw_induct alpha_info;
val alpha_intros_loc = #intrs alpha_info;
val alpha_cases_loc = #elims alpha_info;
- val phi = Proof_Context.export_morphism lthy' lthy;
+ val phi =
+ Proof_Context.export_morphism lthy'
+ (Proof_Context.transfer (Proof_Context.theory_of lthy') lthy);
val all_alpha_trms = all_alpha_trms_loc
|> map (Morphism.term phi)
@@ -313,7 +316,7 @@
fun tac ctxt =
HEADGOAL
- (DETERM o (rtac induct_thm)
+ (DETERM o (resolve_tac ctxt [induct_thm])
THEN_ALL_NEW
(REPEAT_ALL_NEW (FIRST' [resolve_tac ctxt @{thms TrueI conjI}, cases_tac ctxt])))
in
@@ -360,8 +363,8 @@
fun tac ctxt =
HEADGOAL
- (DETERM o (rtac alpha_induct_thm)
- THEN_ALL_NEW FIRST' [rtac @{thm TrueI}, cases_tac ctxt])
+ (DETERM o (resolve_tac ctxt [alpha_induct_thm])
+ THEN_ALL_NEW FIRST' [resolve_tac ctxt @{thms TrueI}, cases_tac ctxt])
in
Goal.prove ctxt' [] [] goals (fn {context, ...} => tac context)
|> singleton (Proof_Context.export ctxt' ctxt)
@@ -392,7 +395,7 @@
end
fun distinct_tac ctxt cases_thms distinct_thms =
- rtac notI THEN' eresolve_tac ctxt cases_thms
+ resolve_tac ctxt [notI] THEN' eresolve_tac ctxt cases_thms
THEN_ALL_NEW asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps distinct_thms)
fun raw_prove_alpha_distincts ctxt alpha_result raw_dt_info =
@@ -427,7 +430,7 @@
fun alpha_eq_iff_tac ctxt dist_inj intros elims =
SOLVED' (asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps intros)) ORELSE'
- (rtac @{thm iffI} THEN'
+ (resolve_tac ctxt @{thms iffI} THEN'
RANGE [eresolve_tac ctxt elims THEN_ALL_NEW asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps dist_inj),
asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps intros)])
@@ -465,14 +468,15 @@
let
val prod_simps = @{thms split_conv prod_alpha_def rel_prod_conv}
- val unbound_tac = REPEAT o (etac @{thm conjE}) THEN' assume_tac ctxt
+ val unbound_tac = REPEAT o (eresolve_tac ctxt @{thms conjE}) THEN' assume_tac ctxt
val bound_tac =
- EVERY' [ rtac exi_zero,
+ EVERY' [ resolve_tac ctxt [exi_zero],
resolve_tac ctxt @{thms alpha_refl},
asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps prod_simps) ]
in
- resolve_tac ctxt intros THEN_ALL_NEW FIRST' [rtac @{thm refl}, unbound_tac, bound_tac]
+ resolve_tac ctxt intros THEN_ALL_NEW
+ FIRST' [resolve_tac ctxt @{thms refl}, unbound_tac, bound_tac]
end
fun raw_prove_refl ctxt alpha_result raw_dt_induct =
@@ -498,19 +502,20 @@
fun prem_bound_tac pred_names alpha_eqvt ctxt =
let
fun trans_prem_tac pred_names ctxt =
- SUBPROOF (fn {prems, context, ...} =>
+ SUBPROOF (fn {prems, context = ctxt', ...} =>
let
- val prems' = map (transform_prem1 context pred_names) prems
+ val prems' = map (transform_prem1 ctxt' pred_names) prems
in
- resolve_tac ctxt prems' 1
+ resolve_tac ctxt' prems' 1
end) ctxt
val prod_simps = @{thms split_conv permute_prod.simps prod_alpha_def rel_prod_conv alphas}
in
EVERY'
- [ etac exi_neg,
+ [ eresolve_tac ctxt [exi_neg],
resolve_tac ctxt @{thms alpha_sym_eqvt},
asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps prod_simps),
- eqvt_tac ctxt (eqvt_relaxed_config addpres alpha_eqvt) THEN' rtac @{thm refl},
+ eqvt_tac ctxt (eqvt_relaxed_config addpres alpha_eqvt) THEN'
+ resolve_tac ctxt @{thms refl},
trans_prem_tac pred_names ctxt]
end
@@ -527,7 +532,7 @@
fun tac ctxt =
resolve_tac ctxt alpha_intros THEN_ALL_NEW
FIRST' [assume_tac ctxt,
- rtac @{thm sym} THEN' assume_tac ctxt,
+ resolve_tac ctxt @{thms sym} THEN' assume_tac ctxt,
prem_bound_tac alpha_names alpha_eqvt ctxt]
in
alpha_prove alpha_trms (alpha_trms ~~ props) alpha_raw_induct tac ctxt
@@ -539,7 +544,7 @@
(* applies cases rules and resolves them with the last premise *)
fun ecases_tac cases =
Subgoal.FOCUS (fn {context = ctxt, prems, ...} =>
- HEADGOAL (resolve_tac ctxt cases THEN' rtac (List.last prems)))
+ HEADGOAL (resolve_tac ctxt cases THEN' resolve_tac ctxt [List.last prems]))
fun aatac pred_names =
SUBPROOF (fn {context = ctxt, prems, ...} =>
@@ -547,13 +552,13 @@
(* instantiates exI with the permutation p + q *)
val perm_inst_tac =
- Subgoal.FOCUS (fn {params, ...} =>
+ Subgoal.FOCUS (fn {context = ctxt, params, ...} =>
let
val (p, q) = apply2 snd (last2 params)
val pq_inst = foldl1 (uncurry Thm.apply) [@{cterm "plus::perm => perm => perm"}, p, q]
- val exi_inst = Drule.instantiate' [SOME (@{ctyp "perm"})] [NONE, SOME pq_inst] @{thm exI}
+ val exi_inst = Thm.instantiate' [SOME (@{ctyp "perm"})] [NONE, SOME pq_inst] @{thm exI}
in
- HEADGOAL (rtac exi_inst)
+ HEADGOAL (resolve_tac ctxt [exi_inst])
end)
fun non_trivial_cases_tac pred_names intros alpha_eqvt ctxt =
@@ -563,13 +568,14 @@
resolve_tac ctxt intros
THEN_ALL_NEW (asm_simp_tac (put_simpset HOL_basic_ss ctxt) THEN'
TRY o EVERY' (* if binders are present *)
- [ etac @{thm exE},
- etac @{thm exE},
+ [ eresolve_tac ctxt @{thms exE},
+ eresolve_tac ctxt @{thms exE},
perm_inst_tac ctxt,
resolve_tac ctxt @{thms alpha_trans_eqvt},
assume_tac ctxt,
aatac pred_names ctxt,
- eqvt_tac ctxt (eqvt_relaxed_config addpres alpha_eqvt) THEN' rtac @{thm refl},
+ eqvt_tac ctxt (eqvt_relaxed_config addpres alpha_eqvt) THEN'
+ resolve_tac ctxt @{thms refl},
asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps prod_simps) ])
end
@@ -582,8 +588,9 @@
asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps raw_dt_thms)
THEN' TRY o non_trivial_cases_tac alpha_names alpha_intros alpha_eqvt ctxt
in
- EVERY' [ rtac @{thm allI}, rtac @{thm impI},
- ecases_tac alpha_cases ctxt THEN_ALL_NEW all_cases ctxt ]
+ EVERY' [ resolve_tac ctxt @{thms allI},
+ resolve_tac ctxt @{thms impI},
+ ecases_tac alpha_cases ctxt THEN_ALL_NEW all_cases ctxt ]
end
fun prep_trans_goal alpha_trm (arg1, arg2) =
@@ -633,7 +640,7 @@
HOLogic.mk_Trueprop (Const (@{const_name "equivp"}, fastype_of t --> @{typ bool}) $ t)
in
Goal.prove_common ctxt NONE [] [] (map prep_goal (alpha_trms @ alpha_bn_trms))
- (K (HEADGOAL (Goal.conjunction_tac THEN_ALL_NEW (rtac @{thm equivpI} THEN'
+ (K (HEADGOAL (Goal.conjunction_tac THEN_ALL_NEW (resolve_tac ctxt @{thms equivpI} THEN'
RANGE [resolve_tac ctxt refl', resolve_tac ctxt symm', resolve_tac ctxt trans']))))
|> chop (length alpha_trms)
end
@@ -642,20 +649,20 @@
(* proves that alpha_raw implies alpha_bn *)
fun raw_prove_bn_imp_tac alpha_result ctxt =
- SUBPROOF (fn {prems, context, ...} =>
+ SUBPROOF (fn {prems, context = ctxt', ...} =>
let
val AlphaResult {alpha_names, alpha_intros, ...} = alpha_result
val prems' = flat (map Old_Datatype_Aux.split_conj_thm prems)
- val prems'' = map (transform_prem1 context alpha_names) prems'
+ val prems'' = map (transform_prem1 ctxt' alpha_names) prems'
in
HEADGOAL
(REPEAT_ALL_NEW
- (FIRST' [ rtac @{thm TrueI},
- rtac @{thm conjI},
- resolve_tac ctxt prems',
- resolve_tac ctxt prems'',
- resolve_tac ctxt alpha_intros ]))
+ (FIRST' [ resolve_tac ctxt' @{thms TrueI},
+ resolve_tac ctxt' @{thms conjI},
+ resolve_tac ctxt' prems',
+ resolve_tac ctxt' prems'',
+ resolve_tac ctxt' alpha_intros ]))
end) ctxt
@@ -711,7 +718,7 @@
put_simpset HOL_ss ctxt addsimps (simps @ @{thms alphas prod_alpha_def rel_prod_conv
permute_prod_def prod.case prod.rec})
- val tac = (TRY o REPEAT o etac @{thm exE}) THEN' asm_full_simp_tac simpset
+ val tac = (TRY o REPEAT o eresolve_tac ctxt @{thms exE}) THEN' asm_full_simp_tac simpset
in
alpha_prove (alpha_trms @ alpha_bn_trms) props alpha_raw_induct (K tac) ctxt
end
@@ -728,7 +735,7 @@
asm_full_simp_tac pre_simpset
THEN' REPEAT o (resolve_tac ctxt @{thms allI impI})
THEN' resolve_tac ctxt alpha_intros
- THEN_ALL_NEW (TRY o (rtac exi_zero) THEN' asm_full_simp_tac post_simpset)
+ THEN_ALL_NEW (TRY o (resolve_tac ctxt [exi_zero]) THEN' asm_full_simp_tac post_simpset)
end
fun raw_constrs_rsp ctxt alpha_result constrs simps =
@@ -796,21 +803,21 @@
by (simp add: rel_fun_def)}
fun raw_prove_perm_bn_tac alpha_result simps ctxt =
- SUBPROOF (fn {prems, context, ...} =>
+ SUBPROOF (fn {prems, context = ctxt', ...} =>
let
val AlphaResult {alpha_names, alpha_bn_names, alpha_intros, ...} = alpha_result
val prems' = flat (map Old_Datatype_Aux.split_conj_thm prems)
- val prems'' = map (transform_prem1 context (alpha_names @ alpha_bn_names)) prems'
+ val prems'' = map (transform_prem1 ctxt' (alpha_names @ alpha_bn_names)) prems'
in
HEADGOAL
- (simp_tac (put_simpset HOL_basic_ss ctxt addsimps (simps @ prems'))
+ (simp_tac (put_simpset HOL_basic_ss ctxt' addsimps (simps @ prems'))
THEN' TRY o REPEAT_ALL_NEW
- (FIRST' [ rtac @{thm TrueI},
- rtac @{thm conjI},
- rtac @{thm refl},
- resolve_tac ctxt prems',
- resolve_tac ctxt prems'',
- resolve_tac ctxt alpha_intros ]))
+ (FIRST' [ resolve_tac ctxt' @{thms TrueI},
+ resolve_tac ctxt' @{thms conjI},
+ resolve_tac ctxt' @{thms refl},
+ resolve_tac ctxt' prems',
+ resolve_tac ctxt' prems'',
+ resolve_tac ctxt' alpha_intros ]))
end) ctxt
fun raw_perm_bn_rsp ctxt alpha_result perm_bns simps =