# HG changeset patch # User wenzelm # Date 1350047309 -7200 # Node ID 1d80798e8d8a7b4333c325a733f8f81d2490e0f6 # Parent 2af09163cba18ed8a8b7acdb1b53046b39d8e7f2 discontinued typedef with implicit set_def; diff -r 2af09163cba1 -r 1d80798e8d8a src/HOL/BNF/Tools/bnf_comp.ML --- a/src/HOL/BNF/Tools/bnf_comp.ML Fri Oct 12 14:05:30 2012 +0200 +++ b/src/HOL/BNF/Tools/bnf_comp.ML Fri Oct 12 15:08:29 2012 +0200 @@ -625,7 +625,7 @@ val deads = map TFree params; val ((bdT_name, (bdT_glob_info, bdT_loc_info)), lthy) = - typedef false NONE (bdT_bind, params, NoSyn) + typedef NONE (bdT_bind, params, NoSyn) (HOLogic.mk_UNIV bd_repT) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy; val bnf_bd' = mk_dir_image bnf_bd diff -r 2af09163cba1 -r 1d80798e8d8a src/HOL/BNF/Tools/bnf_gfp.ML --- a/src/HOL/BNF/Tools/bnf_gfp.ML Fri Oct 12 14:05:30 2012 +0200 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML Fri Oct 12 15:08:29 2012 +0200 @@ -1023,7 +1023,7 @@ val sbdT_bind = Binding.suffix_name ("_" ^ sum_bdTN) b; val ((sbdT_name, (sbdT_glob_info, sbdT_loc_info)), lthy) = - typedef false NONE (sbdT_bind, dead_params, NoSyn) + typedef NONE (sbdT_bind, dead_params, NoSyn) (HOLogic.mk_UNIV sum_bdT) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy; val sbdT = Type (sbdT_name, dead_params'); @@ -1824,7 +1824,7 @@ val ((T_names, (T_glob_infos, T_loc_infos)), lthy) = lthy |> fold_map4 (fn b => fn mx => fn car_final => fn in_car_final => - typedef false NONE (b, params, mx) car_final NONE + typedef NONE (b, params, mx) car_final NONE (EVERY' [rtac exI, rtac in_car_final] 1)) bs mixfixes car_finals in_car_final_thms |>> apsnd split_list o split_list; diff -r 2af09163cba1 -r 1d80798e8d8a src/HOL/BNF/Tools/bnf_lfp.ML --- a/src/HOL/BNF/Tools/bnf_lfp.ML Fri Oct 12 14:05:30 2012 +0200 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML Fri Oct 12 15:08:29 2012 +0200 @@ -776,7 +776,7 @@ val IIT_bind = Binding.suffix_name ("_" ^ IITN) b; val ((IIT_name, (IIT_glob_info, IIT_loc_info)), lthy) = - typedef false NONE (IIT_bind, params, NoSyn) + typedef NONE (IIT_bind, params, NoSyn) (HOLogic.mk_UNIV II_repT) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy; val IIT = Type (IIT_name, params'); @@ -936,7 +936,7 @@ val ((T_names, (T_glob_infos, T_loc_infos)), lthy) = lthy - |> fold_map3 (fn b => fn mx => fn car_init => typedef false NONE (b, params, mx) car_init NONE + |> fold_map3 (fn b => fn mx => fn car_init => typedef NONE (b, params, mx) car_init NONE (EVERY' [rtac ssubst, 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; diff -r 2af09163cba1 -r 1d80798e8d8a src/HOL/BNF/Tools/bnf_util.ML --- a/src/HOL/BNF/Tools/bnf_util.ML Fri Oct 12 14:05:30 2012 +0200 +++ b/src/HOL/BNF/Tools/bnf_util.ML Fri Oct 12 15:08:29 2012 +0200 @@ -154,7 +154,7 @@ val parse_binding_colon: Token.T list -> binding * Token.T list val parse_opt_binding_colon: Token.T list -> binding * Token.T list - val typedef: bool -> binding option -> binding * (string * sort) list * mixfix -> term -> + val typedef: binding option -> binding * (string * sort) list * mixfix -> term -> (binding * binding) option -> tactic -> local_theory -> (string * Typedef.info) * local_theory val WRAP: ('a -> tactic) -> ('a -> tactic) -> 'a list -> tactic -> tactic @@ -280,11 +280,11 @@ val parse_opt_binding_colon = Scan.optional parse_binding_colon Binding.empty; (*TODO: is this really different from Typedef.add_typedef_global?*) -fun typedef def opt_name typ set opt_morphs tac lthy = +fun typedef opt_name typ set opt_morphs tac lthy = let val ((name, info), (lthy, lthy_old)) = lthy - |> Typedef.add_typedef def opt_name typ set opt_morphs tac + |> Typedef.add_typedef opt_name typ set opt_morphs tac ||> `Local_Theory.restore; val phi = Proof_Context.export_morphism lthy_old lthy; in diff -r 2af09163cba1 -r 1d80798e8d8a src/HOL/HOLCF/Tools/cpodef.ML --- a/src/HOL/HOLCF/Tools/cpodef.ML Fri Oct 12 14:05:30 2012 +0200 +++ b/src/HOL/HOLCF/Tools/cpodef.ML Fri Oct 12 15:08:29 2012 +0200 @@ -58,18 +58,6 @@ fun below_const T = Const (@{const_name below}, T --> T --> HOLogic.boolT) -(* manipulating theorems *) - -fun fold_adm_mem thm NONE = thm - | fold_adm_mem thm (SOME set_def) = - let val rule = @{lemma "A == B ==> adm (%x. x : B) ==> adm (%x. x : A)" by simp} - in rule OF [set_def, thm] end - -fun fold_bottom_mem thm NONE = thm - | fold_bottom_mem thm (SOME set_def) = - let val rule = @{lemma "A == B ==> bottom : B ==> bottom : A" by simp} - in rule OF [set_def, thm] end - (* proving class instances *) fun prove_cpo @@ -77,14 +65,12 @@ (newT: typ) (Rep_name: binding, Abs_name: binding) (type_definition: thm) (* type_definition Rep Abs A *) - (set_def: thm option) (* A == set *) (below_def: thm) (* op << == %x y. Rep x << Rep y *) (admissible: thm) (* adm (%x. x : set) *) (thy: theory) = let - val admissible' = fold_adm_mem admissible set_def - val cpo_thms = map (Thm.transfer thy) [type_definition, below_def, admissible'] + val cpo_thms = map (Thm.transfer thy) [type_definition, below_def, admissible] val (full_tname, Ts) = dest_Type newT val lhs_sorts = map (snd o dest_TFree) Ts val tac = Tactic.rtac (@{thm typedef_cpo} OF cpo_thms) 1 @@ -100,14 +86,14 @@ thy |> Sign.add_path (Binding.name_of name) |> Global_Theory.add_thms - ([((Binding.prefix_name "adm_" name, admissible'), []), - ((Binding.prefix_name "cont_" Rep_name, cont_Rep ), []), - ((Binding.prefix_name "cont_" Abs_name, cont_Abs ), []), - ((Binding.prefix_name "lub_" name, lub ), []), - ((Binding.prefix_name "compact_" name, compact ), [])]) + ([((Binding.prefix_name "adm_" name, admissible), []), + ((Binding.prefix_name "cont_" Rep_name, cont_Rep ), []), + ((Binding.prefix_name "cont_" Abs_name, cont_Abs ), []), + ((Binding.prefix_name "lub_" name, lub ), []), + ((Binding.prefix_name "compact_" name, compact ), [])]) ||> Sign.parent_path val cpo_info : cpo_info = - { below_def = below_def, adm = admissible', cont_Rep = cont_Rep, + { below_def = below_def, adm = admissible, cont_Rep = cont_Rep, cont_Abs = cont_Abs, lub = lub, compact = compact } in (cpo_info, thy) @@ -118,14 +104,12 @@ (newT: typ) (Rep_name: binding, Abs_name: binding) (type_definition: thm) (* type_definition Rep Abs A *) - (set_def: thm option) (* A == set *) (below_def: thm) (* op << == %x y. Rep x << Rep y *) (bottom_mem: thm) (* bottom : set *) (thy: theory) = let - val bottom_mem' = fold_bottom_mem bottom_mem set_def - val pcpo_thms = map (Thm.transfer thy) [type_definition, below_def, bottom_mem'] + val pcpo_thms = map (Thm.transfer thy) [type_definition, below_def, bottom_mem] val (full_tname, Ts) = dest_Type newT val lhs_sorts = map (snd o dest_TFree) Ts val tac = Tactic.rtac (@{thm typedef_pcpo} OF pcpo_thms) 1 @@ -184,7 +168,7 @@ let val name = #1 typ val ((full_tname, info as ({Rep_name, ...}, {type_definition, ...})), thy) = thy - |> Typedef.add_typedef_global false NONE typ set opt_morphs tac + |> Typedef.add_typedef_global NONE typ set opt_morphs tac val oldT = #rep_type (#1 info) val newT = #abs_type (#1 info) val lhs_tfrees = map dest_TFree (snd (dest_Type newT)) @@ -222,10 +206,10 @@ fun cpodef_result nonempty admissible thy = let - val ((info as (_, {type_definition, set_def, ...}), below_def), thy) = thy + val ((info as (_, {type_definition, ...}), below_def), thy) = thy |> add_podef typ set opt_morphs (Tactic.rtac nonempty 1) val (cpo_info, thy) = thy - |> prove_cpo name newT morphs type_definition set_def below_def admissible + |> prove_cpo name newT morphs type_definition below_def admissible in ((info, cpo_info), thy) end @@ -256,12 +240,12 @@ fun pcpodef_result bottom_mem admissible thy = let val tac = Tactic.rtac exI 1 THEN Tactic.rtac bottom_mem 1 - val ((info as (_, {type_definition, set_def, ...}), below_def), thy) = thy + val ((info as (_, {type_definition, ...}), below_def), thy) = thy |> add_podef typ set opt_morphs tac val (cpo_info, thy) = thy - |> prove_cpo name newT morphs type_definition set_def below_def admissible + |> prove_cpo name newT morphs type_definition below_def admissible val (pcpo_info, thy) = thy - |> prove_pcpo name newT morphs type_definition set_def below_def bottom_mem + |> prove_pcpo name newT morphs type_definition below_def bottom_mem in ((info, cpo_info, pcpo_info), thy) end diff -r 2af09163cba1 -r 1d80798e8d8a src/HOL/HOLCF/Tools/domaindef.ML --- a/src/HOL/HOLCF/Tools/domaindef.ML Fri Oct 12 14:05:30 2012 +0200 +++ b/src/HOL/HOLCF/Tools/domaindef.ML Fri Oct 12 15:08:29 2012 +0200 @@ -162,12 +162,8 @@ val liftemb_def = singleton (Proof_Context.export lthy ctxt_thy) liftemb_ldef val liftprj_def = singleton (Proof_Context.export lthy ctxt_thy) liftprj_ldef val liftdefl_def = singleton (Proof_Context.export lthy ctxt_thy) liftdefl_ldef - val type_definition_thm = - Raw_Simplifier.rewrite_rule - (the_list (#set_def (#2 info))) - (#type_definition (#2 info)) val typedef_thms = - [type_definition_thm, #below_def cpo_info, emb_def, prj_def, defl_def, + [#type_definition (#2 info), #below_def cpo_info, emb_def, prj_def, defl_def, liftemb_def, liftprj_def, liftdefl_def] val thy = lthy |> Class.prove_instantiation_instance diff -r 2af09163cba1 -r 1d80798e8d8a src/HOL/Import/import_rule.ML --- a/src/HOL/Import/import_rule.ML Fri Oct 12 14:05:30 2012 +0200 +++ b/src/HOL/Import/import_rule.ML Fri Oct 12 15:08:29 2012 +0200 @@ -220,7 +220,7 @@ val tfrees = Term.add_tfrees c [] val tnames = sort_strings (map fst tfrees) val ((_, typedef_info), thy') = - Typedef.add_typedef_global false NONE + Typedef.add_typedef_global NONE (Binding.name tycname, map (rpair dummyS) tnames, NoSyn) c (SOME(Binding.name rep_name,Binding.name abs_name)) (rtac th2 1) thy val aty = #abs_type (#1 typedef_info) diff -r 2af09163cba1 -r 1d80798e8d8a src/HOL/Nominal/nominal_datatype.ML --- a/src/HOL/Nominal/nominal_datatype.ML Fri Oct 12 14:05:30 2012 +0200 +++ b/src/HOL/Nominal/nominal_datatype.ML Fri Oct 12 15:08:29 2012 +0200 @@ -572,7 +572,7 @@ val (typedefs, thy6) = thy4 |> fold_map (fn (((name, mx), tvs), (cname, U)) => fn thy => - Typedef.add_typedef_global false NONE + Typedef.add_typedef_global NONE (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 diff -r 2af09163cba1 -r 1d80798e8d8a src/HOL/Tools/Datatype/datatype.ML --- a/src/HOL/Tools/Datatype/datatype.ML Fri Oct 12 14:05:30 2012 +0200 +++ b/src/HOL/Tools/Datatype/datatype.ML Fri Oct 12 15:08:29 2012 +0200 @@ -190,7 +190,7 @@ |> Sign.parent_path |> fold_map (fn (((name, mx), tvs), c) => - Typedef.add_typedef_global false NONE (name, tvs, mx) + Typedef.add_typedef_global NONE (name, tvs, mx) (Collect $ Const (c, UnivT')) NONE (rtac exI 1 THEN rtac CollectI 1 THEN QUIET_BREADTH_FIRST (has_fewer_prems 1) diff -r 2af09163cba1 -r 1d80798e8d8a src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Oct 12 14:05:30 2012 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Oct 12 15:08:29 2012 +0200 @@ -559,15 +559,13 @@ type typedef_info = {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string, - set_def: thm option, prop_of_Rep: thm, set_name: string, - Abs_inverse: thm option, Rep_inverse: thm option} + prop_of_Rep: thm, set_name: string, Abs_inverse: thm option, Rep_inverse: thm option} fun typedef_info ctxt s = if is_frac_type ctxt (Type (s, [])) then SOME {abs_type = Type (s, []), rep_type = @{typ "int * int"}, Abs_name = @{const_name Nitpick.Abs_Frac}, Rep_name = @{const_name Nitpick.Rep_Frac}, - set_def = NONE, prop_of_Rep = @{prop "Nitpick.Rep_Frac x \ Collect Nitpick.Frac"} |> Logic.varify_global, set_name = @{const_name Nitpick.Frac}, Abs_inverse = NONE, @@ -579,10 +577,10 @@ types's type variables sometimes clash with locally fixed type variables. Remove these calls once "Typedef" is fully localized. *) ({abs_type, rep_type, Abs_name, Rep_name, ...}, - {set_def, Rep, Abs_inverse, Rep_inverse, ...}) :: _ => + {Rep, Abs_inverse, Rep_inverse, ...}) :: _ => SOME {abs_type = Logic.varifyT_global abs_type, rep_type = Logic.varifyT_global rep_type, Abs_name = Abs_name, - Rep_name = Rep_name, set_def = set_def, prop_of_Rep = prop_of Rep, + Rep_name = Rep_name, prop_of_Rep = prop_of Rep, set_name = set_prefix ^ s, Abs_inverse = SOME Abs_inverse, Rep_inverse = SOME Rep_inverse} | _ => NONE @@ -683,13 +681,10 @@ | is_pure_typedef _ _ = false fun is_univ_typedef ctxt (Type (s, _)) = (case typedef_info ctxt s of - SOME {set_def, prop_of_Rep, ...} => + SOME {prop_of_Rep, ...} => let val t_opt = - case set_def of - SOME thm => try (snd o Logic.dest_equals o prop_of) thm - | NONE => try (snd o HOLogic.dest_mem o HOLogic.dest_Trueprop) - prop_of_Rep + try (snd o HOLogic.dest_mem o HOLogic.dest_Trueprop) prop_of_Rep in case t_opt of SOME (Const (@{const_name top}, _)) => true diff -r 2af09163cba1 -r 1d80798e8d8a src/HOL/Tools/Quotient/quotient_type.ML --- a/src/HOL/Tools/Quotient/quotient_type.ML Fri Oct 12 14:05:30 2012 +0200 +++ b/src/HOL/Tools/Quotient/quotient_type.ML Fri Oct 12 15:08:29 2012 +0200 @@ -45,7 +45,7 @@ val typedef_tac = EVERY1 (map rtac [@{thm part_equivp_typedef}, equiv_thm]) in - Typedef.add_typedef false NONE (qty_name, map (rpair dummyS) vs, mx) + Typedef.add_typedef NONE (qty_name, map (rpair dummyS) vs, mx) (typedef_term rel rty lthy) NONE typedef_tac lthy end diff -r 2af09163cba1 -r 1d80798e8d8a src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Fri Oct 12 14:05:30 2012 +0200 +++ b/src/HOL/Tools/record.ML Fri Oct 12 15:08:29 2012 +0200 @@ -112,7 +112,7 @@ val vs = map (Proof_Context.check_tfree ctxt) raw_vs; in thy - |> Typedef.add_typedef_global false (SOME raw_tyco) (raw_tyco, vs, NoSyn) + |> Typedef.add_typedef_global (SOME raw_tyco) (raw_tyco, vs, NoSyn) (HOLogic.mk_UNIV repT) NONE (rtac UNIV_witness 1) |-> (fn (tyco, info) => get_typedef_info tyco vs info) end; diff -r 2af09163cba1 -r 1d80798e8d8a src/HOL/Tools/typedef.ML --- a/src/HOL/Tools/typedef.ML Fri Oct 12 14:05:30 2012 +0200 +++ b/src/HOL/Tools/typedef.ML Fri Oct 12 15:08:29 2012 +0200 @@ -9,21 +9,21 @@ sig type info = {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string, axiom_name: string} * - {inhabited: thm, type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm, - Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm, + {inhabited: thm, type_definition: thm, Rep: thm, Rep_inverse: thm, Abs_inverse: thm, + Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm, Rep_induct: thm, Abs_induct: thm} val transform_info: morphism -> info -> info val get_info: Proof.context -> string -> info list val get_info_global: theory -> string -> info list val interpretation: (string -> theory -> theory) -> theory -> theory val setup: theory -> theory - val add_typedef: bool -> binding option -> binding * (string * sort) list * mixfix -> + val add_typedef: binding option -> binding * (string * sort) list * mixfix -> term -> (binding * binding) option -> tactic -> local_theory -> (string * info) * local_theory - val add_typedef_global: bool -> binding option -> binding * (string * sort) list * mixfix -> + val add_typedef_global: binding option -> binding * (string * sort) list * mixfix -> term -> (binding * binding) option -> tactic -> theory -> (string * info) * theory - val typedef: (bool * binding) * (binding * (string * sort) list * mixfix) * term * + val typedef: binding * (binding * (string * sort) list * mixfix) * term * (binding * binding) option -> local_theory -> Proof.state - val typedef_cmd: (bool * binding) * (binding * (string * string option) list * mixfix) * string * + val typedef_cmd: binding * (binding * (string * string option) list * mixfix) * string * (binding * binding) option -> local_theory -> Proof.state end; @@ -38,23 +38,22 @@ (*global part*) {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string, axiom_name: string} * (*local part*) - {inhabited: thm, type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm, - Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm, + {inhabited: thm, type_definition: thm, Rep: thm, Rep_inverse: thm, Abs_inverse: thm, + Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm, Rep_induct: thm, Abs_induct: thm}; fun transform_info phi (info: info) = let val thm = Morphism.thm phi; - val (global_info, {inhabited, type_definition, - set_def, Rep, Rep_inverse, Abs_inverse, Rep_inject, Abs_inject, - Rep_cases, Abs_cases, Rep_induct, Abs_induct}) = info; + val (global_info, {inhabited, type_definition, Rep, Rep_inverse, Abs_inverse, + Rep_inject, Abs_inject, Rep_cases, Abs_cases, Rep_induct, Abs_induct}) = info; in (global_info, {inhabited = thm inhabited, type_definition = thm type_definition, - set_def = Option.map thm set_def, Rep = thm Rep, Rep_inverse = thm Rep_inverse, - Abs_inverse = thm Abs_inverse, Rep_inject = thm Rep_inject, Abs_inject = thm Abs_inject, - Rep_cases = thm Rep_cases, Abs_cases = thm Abs_cases, Rep_induct = thm Rep_induct, - Abs_induct = thm Abs_induct}) + Rep = thm Rep, Rep_inverse = thm Rep_inverse, Abs_inverse = thm Abs_inverse, + Rep_inject = thm Rep_inject, Abs_inject = thm Abs_inject, + Rep_cases = thm Rep_cases, Abs_cases = thm Abs_cases, + Rep_induct = thm Rep_induct, Abs_induct = thm Abs_induct}) end; structure Data = Generic_Data @@ -129,7 +128,7 @@ (* prepare_typedef *) -fun prepare_typedef prep_term def_set name (tname, raw_args, mx) raw_set opt_morphs lthy = +fun prepare_typedef prep_term name (tname, raw_args, mx) raw_set opt_morphs lthy = let val full_name = Local_Theory.full_name lthy name; val bname = Binding.name_of name; @@ -160,16 +159,6 @@ val lhs_tfrees = map Term.dest_TFree type_args; - (* set definition *) - - val ((set', set_def), set_lthy) = - if def_set then - typedecl_lthy - |> Local_Theory.define ((name, NoSyn), ((Thm.def_binding name, []), set)) - |>> (fn (set', (_, set_def)) => (set', SOME set_def)) - else ((set, NONE), typedecl_lthy); - - (* axiomatization *) val (Rep_name, Abs_name) = @@ -179,21 +168,8 @@ val typedef_name = Binding.prefix_name "type_definition_" name; - val ((RepC, AbsC, axiom_name, typedef), typedef_lthy) = - let - val thy = Proof_Context.theory_of set_lthy; - val cert = Thm.cterm_of thy; - val ((defs, _), A) = - Local_Defs.export_cterm set_lthy (Proof_Context.init_global thy) (cert set') - ||> Thm.term_of; - - val ((RepC, AbsC, axiom_name, axiom), axiom_lthy) = set_lthy - |> primitive_typedef typedef_name newT oldT Rep_name Abs_name A; - - val cert = Thm.cterm_of (Proof_Context.theory_of axiom_lthy); - val typedef = - Local_Defs.contract defs (cert (mk_typedef newT oldT RepC AbsC set')) axiom; - in ((RepC, AbsC, axiom_name, typedef), axiom_lthy) end; + val ((RepC, AbsC, axiom_name, typedef), typedef_lthy) = typedecl_lthy + |> primitive_typedef typedef_name newT oldT Rep_name Abs_name set; val alias_lthy = typedef_lthy |> Local_Theory.const_alias Rep_name (#1 (Term.dest_Const RepC)) @@ -209,9 +185,7 @@ fun typedef_result inhabited lthy1 = let val cert = Thm.cterm_of (Proof_Context.theory_of lthy1); - val inhabited' = - Local_Defs.contract (the_list set_def) (cert (mk_inhabited set')) inhabited; - val typedef' = inhabited' RS typedef; + val typedef' = inhabited RS typedef; fun make th = Goal.norm_result (typedef' RS th); val (((((((((((_, [type_definition]), Rep), Rep_inverse), Abs_inverse), Rep_inject), Abs_inject), Rep_cases), Abs_cases), Rep_induct), Abs_induct), lthy2) = lthy1 @@ -241,7 +215,7 @@ val info = ({rep_type = oldT, abs_type = newT, Rep_name = #1 (Term.dest_Const RepC), Abs_name = #1 (Term.dest_Const AbsC), axiom_name = axiom_name}, - {inhabited = inhabited, type_definition = type_definition, set_def = set_def, + {inhabited = inhabited, type_definition = type_definition, Rep = Rep, Rep_inverse = Rep_inverse, Abs_inverse = Abs_inverse, Rep_inject = Rep_inject, Abs_inject = Abs_inject, Rep_cases = Rep_cases, Abs_cases = Abs_cases, Rep_induct = Rep_induct, Abs_induct = Abs_induct}); @@ -260,19 +234,19 @@ (* add_typedef: tactic interface *) -fun add_typedef def opt_name typ set opt_morphs tac lthy = +fun add_typedef opt_name typ set opt_morphs tac lthy = let val name = the_default (#1 typ) opt_name; val ((goal, _, typedef_result), lthy') = - prepare_typedef Syntax.check_term def name typ set opt_morphs lthy; + prepare_typedef Syntax.check_term name typ set opt_morphs lthy; val inhabited = Goal.prove lthy' [] [] goal (K tac) |> Goal.norm_result |> Thm.close_derivation; in typedef_result inhabited lthy' end; -fun add_typedef_global def opt_name typ set opt_morphs tac = +fun add_typedef_global opt_name typ set opt_morphs tac = Named_Target.theory_init - #> add_typedef def opt_name typ set opt_morphs tac + #> add_typedef opt_name typ set opt_morphs tac #> Local_Theory.exit_result_global (apsnd o transform_info); @@ -280,11 +254,11 @@ local -fun gen_typedef prep_term prep_constraint ((def, name), (b, raw_args, mx), set, opt_morphs) lthy = +fun gen_typedef prep_term prep_constraint (name, (b, raw_args, mx), set, opt_morphs) lthy = let val args = map (apsnd (prep_constraint lthy)) raw_args; val ((goal, goal_pat, typedef_result), lthy') = - prepare_typedef prep_term def name (b, args, mx) set opt_morphs lthy; + prepare_typedef prep_term name (b, args, mx) set opt_morphs lthy; fun after_qed [[th]] = snd o typedef_result th; in Proof.theorem NONE after_qed [[(goal, [goal_pat])]] lthy' end; @@ -310,9 +284,9 @@ Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding)) >> (fn ((((((def, opt_name), (args, t)), mx), A), morphs)) => fn lthy => (if def then - legacy_feature "typedef with implicit set definition -- use \"typedef (open)\" instead" + error "typedef with implicit set definition -- use \"typedef (open)\" instead" else (); - typedef_cmd ((def, the_default t opt_name), (t, args, mx), A, morphs) lthy))); + typedef_cmd (the_default t opt_name, (t, args, mx), A, morphs) lthy))); end;