--- a/Nominal/nominal_dt_alpha.ML Tue Jul 08 11:18:31 2014 +0100
+++ b/Nominal/nominal_dt_alpha.ML Thu Jul 09 02:32:46 2015 +0100
@@ -162,7 +162,7 @@
(* produces the introduction rule for an alpha rule *)
fun mk_alpha_intros lthy alpha_map alpha_bn_map (constr, ty, arg_tys, is_rec) bclauses =
let
- val arg_names = Datatype_Prop.make_tnames arg_tys
+ val arg_names = Old_Datatype_Prop.make_tnames arg_tys
val arg_names' = Name.variant_list arg_names arg_names
val args = map Free (arg_names ~~ arg_tys)
val args' = map Free (arg_names' ~~ arg_tys)
@@ -205,7 +205,7 @@
fun mk_alpha_bn_intro lthy bn_trm alpha_map alpha_bn_map (bn_args, (constr, _, arg_tys, is_rec)) bclauses =
let
- val arg_names = Datatype_Prop.make_tnames arg_tys
+ val arg_names = Old_Datatype_Prop.make_tnames arg_tys
val arg_names' = Name.variant_list arg_names arg_names
val args = map Free (arg_names ~~ arg_tys)
val args' = map Free (arg_names' ~~ arg_tys)
@@ -315,14 +315,14 @@
HEADGOAL
(DETERM o (rtac induct_thm)
THEN_ALL_NEW
- (REPEAT_ALL_NEW (FIRST' [resolve_tac @{thms TrueI conjI}, cases_tac ctxt])))
+ (REPEAT_ALL_NEW (FIRST' [resolve_tac ctxt @{thms TrueI conjI}, cases_tac ctxt])))
in
Goal.prove ctxt' [] [] goals (fn {context, ...} => tac context)
|> singleton (Proof_Context.export ctxt' ctxt)
- |> Datatype_Aux.split_conj_thm
- |> map Datatype_Aux.split_conj_thm
+ |> Old_Datatype_Aux.split_conj_thm
+ |> map Old_Datatype_Aux.split_conj_thm
|> flat
- |> filter_out (is_true o concl_of)
+ |> filter_out (is_true o Thm.concl_of)
|> map zero_var_indexes
end
@@ -365,11 +365,11 @@
in
Goal.prove ctxt' [] [] goals (fn {context, ...} => tac context)
|> singleton (Proof_Context.export ctxt' ctxt)
- |> Datatype_Aux.split_conj_thm
+ |> Old_Datatype_Aux.split_conj_thm
|> map (fn th => th RS mp)
- |> map Datatype_Aux.split_conj_thm
+ |> map Old_Datatype_Aux.split_conj_thm
|> flat
- |> filter_out (is_true o concl_of)
+ |> filter_out (is_true o Thm.concl_of)
|> map zero_var_indexes
end
@@ -392,7 +392,7 @@
end
fun distinct_tac ctxt cases_thms distinct_thms =
- rtac notI THEN' eresolve_tac cases_thms
+ rtac 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 =
@@ -410,7 +410,7 @@
(K (distinct_tac ctxt alpha_cases raw_distinct_thms 1))
end
in
- map (mk_alpha_distinct o prop_of) raw_distinct_thms
+ map (mk_alpha_distinct o Thm.prop_of) raw_distinct_thms
end
@@ -421,19 +421,19 @@
rewritten to ((Rel Const = Const) = True)
*)
fun mk_simp_rule thm =
- case (prop_of thm) of
+ case Thm.prop_of thm of
@{term "Trueprop"} $ (_ $ Const _ $ Const _) => thm RS @{thm eqTrueI}
| _ => thm
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'
- RANGE [eresolve_tac elims THEN_ALL_NEW asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps dist_inj),
+ 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)])
fun mk_alpha_eq_iff_goal thm =
let
- val prop = prop_of thm;
+ val prop = Thm.prop_of thm;
val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop);
val hyps = map HOLogic.dest_Trueprop (Logic.strip_imp_prems prop);
fun list_conj l = foldr1 HOLogic.mk_conj l;
@@ -463,16 +463,16 @@
fun cases_tac intros ctxt =
let
- val prod_simps = @{thms split_conv prod_alpha_def rel_prod_def}
+ val prod_simps = @{thms split_conv prod_alpha_def rel_prod_conv}
- val unbound_tac = REPEAT o (etac @{thm conjE}) THEN' atac
+ val unbound_tac = REPEAT o (etac @{thm conjE}) THEN' assume_tac ctxt
val bound_tac =
EVERY' [ rtac exi_zero,
- resolve_tac @{thms alpha_refl},
+ resolve_tac ctxt @{thms alpha_refl},
asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps prod_simps) ]
in
- resolve_tac intros THEN_ALL_NEW FIRST' [rtac @{thm refl}, unbound_tac, bound_tac]
+ resolve_tac ctxt intros THEN_ALL_NEW FIRST' [rtac @{thm refl}, unbound_tac, bound_tac]
end
fun raw_prove_refl ctxt alpha_result raw_dt_induct =
@@ -502,13 +502,13 @@
let
val prems' = map (transform_prem1 context pred_names) prems
in
- resolve_tac prems' 1
+ resolve_tac ctxt prems' 1
end) ctxt
- val prod_simps = @{thms split_conv permute_prod.simps prod_alpha_def rel_prod_def alphas}
+ val prod_simps = @{thms split_conv permute_prod.simps prod_alpha_def rel_prod_conv alphas}
in
EVERY'
[ etac exi_neg,
- resolve_tac @{thms alpha_sym_eqvt},
+ 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},
trans_prem_tac pred_names ctxt]
@@ -525,8 +525,10 @@
val props = map (fn t => fn (x, y) => t $ y $ x) alpha_trms
fun tac ctxt =
- resolve_tac alpha_intros THEN_ALL_NEW
- FIRST' [atac, rtac @{thm sym} THEN' atac, prem_bound_tac alpha_names alpha_eqvt ctxt]
+ resolve_tac ctxt alpha_intros THEN_ALL_NEW
+ FIRST' [assume_tac ctxt,
+ rtac @{thm 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
end
@@ -536,18 +538,18 @@
(* applies cases rules and resolves them with the last premise *)
fun ecases_tac cases =
- Subgoal.FOCUS (fn {prems, ...} =>
- HEADGOAL (resolve_tac cases THEN' rtac (List.last prems)))
+ Subgoal.FOCUS (fn {context = ctxt, prems, ...} =>
+ HEADGOAL (resolve_tac ctxt cases THEN' rtac (List.last prems)))
fun aatac pred_names =
- SUBPROOF (fn {prems, context, ...} =>
- HEADGOAL (resolve_tac (map (transform_prem1 context pred_names) prems)))
+ SUBPROOF (fn {context = ctxt, prems, ...} =>
+ HEADGOAL (resolve_tac ctxt (map (transform_prem1 ctxt pred_names) prems)))
(* instantiates exI with the permutation p + q *)
val perm_inst_tac =
Subgoal.FOCUS (fn {params, ...} =>
let
- val (p, q) = pairself snd (last2 params)
+ 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}
in
@@ -556,16 +558,16 @@
fun non_trivial_cases_tac pred_names intros alpha_eqvt ctxt =
let
- val prod_simps = @{thms split_conv alphas permute_prod.simps prod_alpha_def rel_prod_def}
+ val prod_simps = @{thms split_conv alphas permute_prod.simps prod_alpha_def rel_prod_conv}
in
- resolve_tac intros
+ 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},
perm_inst_tac ctxt,
- resolve_tac @{thms alpha_trans_eqvt},
- atac,
+ 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},
asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps prod_simps) ])
@@ -630,9 +632,9 @@
fun prep_goal t =
HOLogic.mk_Trueprop (Const (@{const_name "equivp"}, fastype_of t --> @{typ bool}) $ t)
in
- Goal.prove_multi ctxt [] [] (map prep_goal (alpha_trms @ alpha_bn_trms))
+ 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'
- RANGE [resolve_tac refl', resolve_tac symm', resolve_tac trans']))))
+ RANGE [resolve_tac ctxt refl', resolve_tac ctxt symm', resolve_tac ctxt trans']))))
|> chop (length alpha_trms)
end
@@ -644,16 +646,16 @@
let
val AlphaResult {alpha_names, alpha_intros, ...} = alpha_result
- val prems' = flat (map Datatype_Aux.split_conj_thm prems)
+ val prems' = flat (map Old_Datatype_Aux.split_conj_thm prems)
val prems'' = map (transform_prem1 context alpha_names) prems'
in
HEADGOAL
(REPEAT_ALL_NEW
(FIRST' [ rtac @{thm TrueI},
rtac @{thm conjI},
- resolve_tac prems',
- resolve_tac prems'',
- resolve_tac alpha_intros ]))
+ resolve_tac ctxt prems',
+ resolve_tac ctxt prems'',
+ resolve_tac ctxt alpha_intros ]))
end) ctxt
@@ -706,7 +708,7 @@
val props = (alpha_trms @ alpha_bn_trms) ~~ (map mk_prop (alpha_tys @ alpha_bn_tys))
val simpset =
- put_simpset HOL_ss ctxt addsimps (simps @ @{thms alphas prod_alpha_def rel_prod_def
+ 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
@@ -720,12 +722,12 @@
fun raw_constr_rsp_tac ctxt alpha_intros simps =
let
val pre_simpset = put_simpset HOL_ss ctxt addsimps @{thms rel_fun_def}
- val post_simpset = put_simpset HOL_ss ctxt addsimps @{thms alphas prod_alpha_def rel_prod_def
+ val post_simpset = put_simpset HOL_ss ctxt addsimps @{thms alphas prod_alpha_def rel_prod_conv
prod_fv.simps fresh_star_zero permute_zero prod.case} @ simps
in
asm_full_simp_tac pre_simpset
- THEN' REPEAT o (resolve_tac @{thms allI impI})
- THEN' resolve_tac alpha_intros
+ 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)
end
@@ -752,7 +754,7 @@
|> HOLogic.mk_Trueprop
in
map (fn constrs =>
- Goal.prove_multi ctxt [] [] (map prep_goal constrs)
+ Goal.prove_common ctxt NONE [] [] (map prep_goal constrs)
(K (HEADGOAL
(Goal.conjunction_tac THEN_ALL_NEW raw_constr_rsp_tac ctxt alpha_intros simps)))) constrs
end
@@ -772,7 +774,7 @@
val AlphaResult {alpha_bn_trms, ...} = alpha_result
fun mk_map thm =
- thm |> `prop_of
+ thm |> `Thm.prop_of
|>> List.last o snd o strip_comb
|>> HOLogic.dest_Trueprop
|>> head_of
@@ -797,7 +799,7 @@
SUBPROOF (fn {prems, context, ...} =>
let
val AlphaResult {alpha_names, alpha_bn_names, alpha_intros, ...} = alpha_result
- val prems' = flat (map Datatype_Aux.split_conj_thm prems)
+ val prems' = flat (map Old_Datatype_Aux.split_conj_thm prems)
val prems'' = map (transform_prem1 context (alpha_names @ alpha_bn_names)) prems'
in
HEADGOAL
@@ -806,9 +808,9 @@
(FIRST' [ rtac @{thm TrueI},
rtac @{thm conjI},
rtac @{thm refl},
- resolve_tac prems',
- resolve_tac prems'',
- resolve_tac alpha_intros ]))
+ 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 =