# HG changeset patch # User wenzelm # Date 1415562113 -3600 # Node ID 1f195ed9994126474d40897e1f2cd5edb26248c5 # Parent 114255dce178f100e20277361774abe01aaab21b proper proof context for typedef; diff -r 114255dce178 -r 1f195ed99941 src/HOL/HOLCF/Tools/cpodef.ML --- a/src/HOL/HOLCF/Tools/cpodef.ML Sun Nov 09 18:27:43 2014 +0100 +++ b/src/HOL/HOLCF/Tools/cpodef.ML Sun Nov 09 20:41:53 2014 +0100 @@ -15,14 +15,14 @@ Rep_bottom_iff: thm, Abs_bottom_iff: thm } val add_podef: binding * (string * sort) list * mixfix -> - term -> (binding * binding) option -> tactic -> theory -> + term -> (binding * binding) option -> (Proof.context -> tactic) -> theory -> (Typedef.info * thm) * theory val add_cpodef: binding * (string * sort) list * mixfix -> - term -> (binding * binding) option -> tactic * tactic -> theory -> - (Typedef.info * cpo_info) * theory + term -> (binding * binding) option -> (Proof.context -> tactic) * (Proof.context -> tactic) -> + theory -> (Typedef.info * cpo_info) * theory val add_pcpodef: binding * (string * sort) list * mixfix -> - term -> (binding * binding) option -> tactic * tactic -> theory -> - (Typedef.info * cpo_info * pcpo_info) * theory + term -> (binding * binding) option -> (Proof.context -> tactic) * (Proof.context -> tactic) -> + theory -> (Typedef.info * cpo_info * pcpo_info) * theory val cpodef_proof: (binding * (string * sort) list * mixfix) * term @@ -205,7 +205,7 @@ fun cpodef_result nonempty admissible thy = let val ((info as (_, {type_definition, ...}), below_def), thy) = thy - |> add_podef typ set opt_morphs (rtac nonempty 1) + |> add_podef typ set opt_morphs (fn _ => rtac nonempty 1) val (cpo_info, thy) = thy |> prove_cpo name newT morphs type_definition below_def admissible in @@ -237,7 +237,7 @@ fun pcpodef_result bottom_mem admissible thy = let - val tac = rtac exI 1 THEN rtac bottom_mem 1 + fun tac _ = rtac exI 1 THEN rtac bottom_mem 1 val ((info as (_, {type_definition, ...}), below_def), thy) = thy |> add_podef typ set opt_morphs tac val (cpo_info, thy) = thy @@ -260,10 +260,10 @@ let val (goal1, goal2, cpodef_result) = prepare_cpodef Syntax.check_term typ set opt_morphs thy - val thm1 = Goal.prove_global thy [] [] goal1 (K tac1) + val thm1 = Goal.prove_global thy [] [] goal1 (tac1 o #context) handle ERROR msg => cat_error msg ("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set)) - val thm2 = Goal.prove_global thy [] [] goal2 (K tac2) + val thm2 = Goal.prove_global thy [] [] goal2 (tac2 o #context) handle ERROR msg => cat_error msg ("Failed to prove admissibility of " ^ quote (Syntax.string_of_term_global thy set)) in cpodef_result thm1 thm2 thy end @@ -272,10 +272,10 @@ let val (goal1, goal2, pcpodef_result) = prepare_pcpodef Syntax.check_term typ set opt_morphs thy - val thm1 = Goal.prove_global thy [] [] goal1 (K tac1) + val thm1 = Goal.prove_global thy [] [] goal1 (tac1 o #context) handle ERROR msg => cat_error msg ("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set)) - val thm2 = Goal.prove_global thy [] [] goal2 (K tac2) + val thm2 = Goal.prove_global thy [] [] goal2 (tac2 o #context) handle ERROR msg => cat_error msg ("Failed to prove admissibility of " ^ quote (Syntax.string_of_term_global thy set)) in pcpodef_result thm1 thm2 thy end diff -r 114255dce178 -r 1f195ed99941 src/HOL/HOLCF/Tools/domaindef.ML --- a/src/HOL/HOLCF/Tools/domaindef.ML Sun Nov 09 18:27:43 2014 +0100 +++ b/src/HOL/HOLCF/Tools/domaindef.ML Sun Nov 09 20:41:53 2014 +0100 @@ -108,8 +108,8 @@ val set = @{term "defl_set :: udom defl => udom set"} $ defl (*pcpodef*) - val tac1 = rtac @{thm defl_set_bottom} 1 - val tac2 = rtac @{thm adm_defl_set} 1 + fun tac1 _ = rtac @{thm defl_set_bottom} 1 + fun tac2 _ = rtac @{thm adm_defl_set} 1 val ((info, cpo_info, pcpo_info), thy) = thy |> Cpodef.add_pcpodef typ set (SOME morphs) (tac1, tac2) diff -r 114255dce178 -r 1f195ed99941 src/HOL/Nominal/nominal_datatype.ML --- a/src/HOL/Nominal/nominal_datatype.ML Sun Nov 09 18:27:43 2014 +0100 +++ b/src/HOL/Nominal/nominal_datatype.ML Sun Nov 09 20:41:53 2014 +0100 @@ -578,7 +578,7 @@ (name, map (fn (v, _) => (v, dummyS)) tvs, mx) (* FIXME keep constraints!? *) (Const (@{const_name Collect}, (U --> HOLogic.boolT) --> HOLogic.mk_setT U) $ Const (cname, U --> HOLogic.boolT)) NONE - (rtac exI 1 THEN rtac CollectI 1 THEN + (fn _ => rtac exI 1 THEN rtac CollectI 1 THEN QUIET_BREADTH_FIRST (has_fewer_prems 1) (resolve_tac rep_intrs 1)) thy |> (fn ((_, r), thy) => let diff -r 114255dce178 -r 1f195ed99941 src/HOL/Tools/BNF/bnf_comp.ML --- a/src/HOL/Tools/BNF/bnf_comp.ML Sun Nov 09 18:27:43 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_comp.ML Sun Nov 09 20:41:53 2014 +0100 @@ -770,7 +770,7 @@ val TA_params = Term.add_tfreesT repTA (if has_live_phantoms then As' else []); val ((TA, (Rep_name, Abs_name, type_definition, Abs_inverse, Abs_inject, _)), lthy) = maybe_typedef has_live_phantoms (T_bind, TA_params, NoSyn) (HOLogic.mk_UNIV repTA) NONE - (EVERY' [rtac exI, rtac UNIV_I] 1) lthy; + (fn _ => EVERY' [rtac exI, rtac UNIV_I] 1) lthy; val repTB = mk_T_of_bnf Ds Bs bnf; val TB = Term.typ_subst_atomic (As ~~ Bs) TA; @@ -800,7 +800,7 @@ val ((bdT, (_, Abs_bd_name, _, _, Abs_bdT_inject, Abs_bdT_cases)), lthy) = maybe_typedef false (bdT_bind, params, NoSyn) - (HOLogic.mk_UNIV bd_repT) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy; + (HOLogic.mk_UNIV bd_repT) NONE (fn _ => EVERY' [rtac exI, rtac UNIV_I] 1) lthy; val (bnf_bd', bd_ordIso, bd_card_order, bd_cinfinite) = if bdT = bd_repT then (bnf_bd, bd_Card_order_of_bnf bnf RS @{thm ordIso_refl}, diff -r 114255dce178 -r 1f195ed99941 src/HOL/Tools/BNF/bnf_gfp.ML --- a/src/HOL/Tools/BNF/bnf_gfp.ML Sun Nov 09 18:27:43 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML Sun Nov 09 20:41:53 2014 +0100 @@ -719,7 +719,7 @@ val ((sbdT_name, (sbdT_glob_info, sbdT_loc_info)), lthy) = typedef (sbdT_bind, sum_bdT_params', NoSyn) - (HOLogic.mk_UNIV sum_bdT) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy; + (HOLogic.mk_UNIV sum_bdT) NONE (fn _ => EVERY' [rtac exI, rtac UNIV_I] 1) lthy; val sbdT = Type (sbdT_name, sum_bdT_params); val Abs_sbdT = Const (#Abs_name sbdT_glob_info, sum_bdT --> sbdT); @@ -1269,7 +1269,7 @@ lthy |> @{fold_map 4} (fn b => fn mx => fn car_final => fn in_car_final => typedef (b, params, mx) car_final NONE - (EVERY' [rtac exI, rtac in_car_final] 1)) bs mixfixes car_finals in_car_final_thms + (fn _ => EVERY' [rtac exI, rtac in_car_final] 1)) bs mixfixes car_finals in_car_final_thms |>> apsnd split_list o split_list; val Ts = map (fn name => Type (name, params')) T_names; diff -r 114255dce178 -r 1f195ed99941 src/HOL/Tools/BNF/bnf_lfp.ML --- a/src/HOL/Tools/BNF/bnf_lfp.ML Sun Nov 09 18:27:43 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML Sun Nov 09 20:41:53 2014 +0100 @@ -457,7 +457,7 @@ val ((sbdT_name, (sbdT_glob_info, sbdT_loc_info)), lthy) = typedef (sbdT_bind, sum_bdT_params', NoSyn) - (HOLogic.mk_UNIV sum_bdT) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy; + (HOLogic.mk_UNIV sum_bdT) NONE (fn _ => EVERY' [rtac exI, rtac UNIV_I] 1) lthy; val sbdT = Type (sbdT_name, sum_bdT_params); val Abs_sbdT = Const (#Abs_name sbdT_glob_info, sum_bdT --> sbdT); @@ -716,7 +716,7 @@ val ((IIT_name, (IIT_glob_info, IIT_loc_info)), lthy) = typedef (IIT_bind, params, NoSyn) - (HOLogic.mk_UNIV II_repT) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy; + (HOLogic.mk_UNIV II_repT) NONE (fn _ => EVERY' [rtac exI, rtac UNIV_I] 1) lthy; val IIT = Type (IIT_name, params'); val Abs_IIT = Const (#Abs_name IIT_glob_info, II_repT --> IIT); @@ -860,7 +860,7 @@ lthy |> @{fold_map 3} (fn b => fn mx => fn car_init => typedef (b, params, mx) car_init NONE - (EVERY' [rtac iffD2, rtac @{thm ex_in_conv}, resolve_tac alg_not_empty_thms, + (fn _ => EVERY' [rtac iffD2, rtac @{thm ex_in_conv}, resolve_tac alg_not_empty_thms, rtac alg_init_thm] 1)) bs mixfixes car_inits |>> apsnd split_list o split_list; @@ -1393,7 +1393,7 @@ val ((sbd0T_name, (sbd0T_glob_info, sbd0T_loc_info)), lthy) = typedef (sbd0T_bind, sum_bd0T_params', NoSyn) - (HOLogic.mk_UNIV sum_bd0T) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy; + (HOLogic.mk_UNIV sum_bd0T) NONE (fn _ => EVERY' [rtac exI, rtac UNIV_I] 1) lthy; val sbd0T = Type (sbd0T_name, sum_bd0T_params); val Abs_sbd0T = Const (#Abs_name sbd0T_glob_info, sum_bd0T --> sbd0T); diff -r 114255dce178 -r 1f195ed99941 src/HOL/Tools/BNF/bnf_util.ML --- a/src/HOL/Tools/BNF/bnf_util.ML Sun Nov 09 18:27:43 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_util.ML Sun Nov 09 20:41:53 2014 +0100 @@ -104,7 +104,8 @@ val parse_map_rel_bindings: (binding * binding) parser val typedef: binding * (string * sort) list * mixfix -> term -> - (binding * binding) option -> tactic -> local_theory -> (string * Typedef.info) * local_theory + (binding * binding) option -> (Proof.context -> tactic) -> + local_theory -> (string * Typedef.info) * local_theory end; structure BNF_Util : BNF_UTIL = diff -r 114255dce178 -r 1f195ed99941 src/HOL/Tools/Old_Datatype/old_datatype.ML --- a/src/HOL/Tools/Old_Datatype/old_datatype.ML Sun Nov 09 18:27:43 2014 +0100 +++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML Sun Nov 09 20:41:53 2014 +0100 @@ -188,7 +188,7 @@ (fn (((name, mx), tvs), c) => Typedef.add_typedef_global false (name, tvs, mx) (Collect $ Const (c, UnivT')) NONE - (rtac exI 1 THEN rtac CollectI 1 THEN + (fn _ => rtac exI 1 THEN rtac CollectI 1 THEN QUIET_BREADTH_FIRST (has_fewer_prems 1) (resolve_tac rep_intrs 1))) (types_syntax ~~ tyvars ~~ take (length newTs) rep_set_names) diff -r 114255dce178 -r 1f195ed99941 src/HOL/Tools/Quotient/quotient_type.ML --- a/src/HOL/Tools/Quotient/quotient_type.ML Sun Nov 09 18:27:43 2014 +0100 +++ b/src/HOL/Tools/Quotient/quotient_type.ML Sun Nov 09 20:41:53 2014 +0100 @@ -42,7 +42,7 @@ (* makes the new type definitions and proves non-emptyness *) fun typedef_make (vs, qty_name, mx, rel, rty) equiv_thm lthy = let - val typedef_tac = + fun typedef_tac _ = EVERY1 (map rtac [@{thm part_equivp_typedef}, equiv_thm]) in Typedef.add_typedef false (qty_name, map (rpair dummyS) vs, mx) diff -r 114255dce178 -r 1f195ed99941 src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Sun Nov 09 18:27:43 2014 +0100 +++ b/src/HOL/Tools/record.ML Sun Nov 09 20:41:53 2014 +0100 @@ -112,7 +112,7 @@ in thy |> Typedef.add_typedef_global false (raw_tyco, vs, NoSyn) - (HOLogic.mk_UNIV repT) NONE (rtac UNIV_witness 1) + (HOLogic.mk_UNIV repT) NONE (fn _ => rtac UNIV_witness 1) |-> (fn (tyco, info) => get_typedef_info tyco vs info) end; diff -r 114255dce178 -r 1f195ed99941 src/HOL/Tools/typedef.ML --- a/src/HOL/Tools/typedef.ML Sun Nov 09 18:27:43 2014 +0100 +++ b/src/HOL/Tools/typedef.ML Sun Nov 09 20:41:53 2014 +0100 @@ -17,9 +17,11 @@ val get_info_global: theory -> string -> info list val interpretation: (string -> local_theory -> local_theory) -> theory -> theory val add_typedef: bool -> binding * (string * sort) list * mixfix -> - term -> (binding * binding) option -> tactic -> local_theory -> (string * info) * local_theory + term -> (binding * binding) option -> (Proof.context -> tactic) -> local_theory -> + (string * info) * local_theory val add_typedef_global: bool -> binding * (string * sort) list * mixfix -> - term -> (binding * binding) option -> tactic -> theory -> (string * info) * theory + term -> (binding * binding) option -> (Proof.context -> tactic) -> theory -> + (string * info) * theory val typedef: (binding * (string * sort) list * mixfix) * term * (binding * binding) option -> local_theory -> Proof.state val typedef_cmd: (binding * (string * string option) list * mixfix) * string * @@ -245,7 +247,7 @@ val ((goal, _, typedef_result), lthy') = prepare_typedef conceal Syntax.check_term typ set opt_morphs lthy; val inhabited = - Goal.prove lthy' [] [] goal (K tac) + Goal.prove lthy' [] [] goal (tac o #context) |> Goal.norm_result lthy' |> Thm.close_derivation; in typedef_result inhabited lthy' end;