diff -r b2e1a7b83e05 -r 67370521c09c Nominal/nominal_dt_alpha.ML --- 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 =