discontinued typedef with implicit set_def;
authorwenzelm
Fri Oct 12 15:08:29 2012 +0200 (2012-10-12)
changeset 498331d80798e8d8a
parent 49832 2af09163cba1
child 49834 b27bbb021df1
discontinued typedef with implicit set_def;
src/HOL/BNF/Tools/bnf_comp.ML
src/HOL/BNF/Tools/bnf_gfp.ML
src/HOL/BNF/Tools/bnf_lfp.ML
src/HOL/BNF/Tools/bnf_util.ML
src/HOL/HOLCF/Tools/cpodef.ML
src/HOL/HOLCF/Tools/domaindef.ML
src/HOL/Import/import_rule.ML
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Tools/Datatype/datatype.ML
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Quotient/quotient_type.ML
src/HOL/Tools/record.ML
src/HOL/Tools/typedef.ML
     1.1 --- a/src/HOL/BNF/Tools/bnf_comp.ML	Fri Oct 12 14:05:30 2012 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_comp.ML	Fri Oct 12 15:08:29 2012 +0200
     1.3 @@ -625,7 +625,7 @@
     1.4      val deads = map TFree params;
     1.5  
     1.6      val ((bdT_name, (bdT_glob_info, bdT_loc_info)), lthy) =
     1.7 -      typedef false NONE (bdT_bind, params, NoSyn)
     1.8 +      typedef NONE (bdT_bind, params, NoSyn)
     1.9          (HOLogic.mk_UNIV bd_repT) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy;
    1.10  
    1.11      val bnf_bd' = mk_dir_image bnf_bd
     2.1 --- a/src/HOL/BNF/Tools/bnf_gfp.ML	Fri Oct 12 14:05:30 2012 +0200
     2.2 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Fri Oct 12 15:08:29 2012 +0200
     2.3 @@ -1023,7 +1023,7 @@
     2.4            val sbdT_bind = Binding.suffix_name ("_" ^ sum_bdTN) b;
     2.5  
     2.6            val ((sbdT_name, (sbdT_glob_info, sbdT_loc_info)), lthy) =
     2.7 -            typedef false NONE (sbdT_bind, dead_params, NoSyn)
     2.8 +            typedef NONE (sbdT_bind, dead_params, NoSyn)
     2.9                (HOLogic.mk_UNIV sum_bdT) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy;
    2.10  
    2.11            val sbdT = Type (sbdT_name, dead_params');
    2.12 @@ -1824,7 +1824,7 @@
    2.13      val ((T_names, (T_glob_infos, T_loc_infos)), lthy) =
    2.14        lthy
    2.15        |> fold_map4 (fn b => fn mx => fn car_final => fn in_car_final =>
    2.16 -        typedef false NONE (b, params, mx) car_final NONE
    2.17 +        typedef NONE (b, params, mx) car_final NONE
    2.18            (EVERY' [rtac exI, rtac in_car_final] 1)) bs mixfixes car_finals in_car_final_thms
    2.19        |>> apsnd split_list o split_list;
    2.20  
     3.1 --- a/src/HOL/BNF/Tools/bnf_lfp.ML	Fri Oct 12 14:05:30 2012 +0200
     3.2 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Fri Oct 12 15:08:29 2012 +0200
     3.3 @@ -776,7 +776,7 @@
     3.4      val IIT_bind = Binding.suffix_name ("_" ^ IITN) b;
     3.5  
     3.6      val ((IIT_name, (IIT_glob_info, IIT_loc_info)), lthy) =
     3.7 -      typedef false NONE (IIT_bind, params, NoSyn)
     3.8 +      typedef NONE (IIT_bind, params, NoSyn)
     3.9          (HOLogic.mk_UNIV II_repT) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy;
    3.10  
    3.11      val IIT = Type (IIT_name, params');
    3.12 @@ -936,7 +936,7 @@
    3.13  
    3.14      val ((T_names, (T_glob_infos, T_loc_infos)), lthy) =
    3.15        lthy
    3.16 -      |> fold_map3 (fn b => fn mx => fn car_init => typedef false NONE (b, params, mx) car_init NONE
    3.17 +      |> fold_map3 (fn b => fn mx => fn car_init => typedef NONE (b, params, mx) car_init NONE
    3.18            (EVERY' [rtac ssubst, rtac @{thm ex_in_conv}, resolve_tac alg_not_empty_thms,
    3.19              rtac alg_init_thm] 1)) bs mixfixes car_inits
    3.20        |>> apsnd split_list o split_list;
     4.1 --- a/src/HOL/BNF/Tools/bnf_util.ML	Fri Oct 12 14:05:30 2012 +0200
     4.2 +++ b/src/HOL/BNF/Tools/bnf_util.ML	Fri Oct 12 15:08:29 2012 +0200
     4.3 @@ -154,7 +154,7 @@
     4.4    val parse_binding_colon: Token.T list -> binding * Token.T list
     4.5    val parse_opt_binding_colon: Token.T list -> binding * Token.T list
     4.6  
     4.7 -  val typedef: bool -> binding option -> binding * (string * sort) list * mixfix -> term ->
     4.8 +  val typedef: binding option -> binding * (string * sort) list * mixfix -> term ->
     4.9      (binding * binding) option -> tactic -> local_theory -> (string * Typedef.info) * local_theory
    4.10  
    4.11    val WRAP: ('a -> tactic) -> ('a -> tactic) -> 'a list -> tactic -> tactic
    4.12 @@ -280,11 +280,11 @@
    4.13  val parse_opt_binding_colon = Scan.optional parse_binding_colon Binding.empty;
    4.14  
    4.15  (*TODO: is this really different from Typedef.add_typedef_global?*)
    4.16 -fun typedef def opt_name typ set opt_morphs tac lthy =
    4.17 +fun typedef opt_name typ set opt_morphs tac lthy =
    4.18    let
    4.19      val ((name, info), (lthy, lthy_old)) =
    4.20        lthy
    4.21 -      |> Typedef.add_typedef def opt_name typ set opt_morphs tac
    4.22 +      |> Typedef.add_typedef opt_name typ set opt_morphs tac
    4.23        ||> `Local_Theory.restore;
    4.24      val phi = Proof_Context.export_morphism lthy_old lthy;
    4.25    in
     5.1 --- a/src/HOL/HOLCF/Tools/cpodef.ML	Fri Oct 12 14:05:30 2012 +0200
     5.2 +++ b/src/HOL/HOLCF/Tools/cpodef.ML	Fri Oct 12 15:08:29 2012 +0200
     5.3 @@ -58,18 +58,6 @@
     5.4  
     5.5  fun below_const T = Const (@{const_name below}, T --> T --> HOLogic.boolT)
     5.6  
     5.7 -(* manipulating theorems *)
     5.8 -
     5.9 -fun fold_adm_mem thm NONE = thm
    5.10 -  | fold_adm_mem thm (SOME set_def) =
    5.11 -    let val rule = @{lemma "A == B ==> adm (%x. x : B) ==> adm (%x. x : A)" by simp}
    5.12 -    in rule OF [set_def, thm] end
    5.13 -
    5.14 -fun fold_bottom_mem thm NONE = thm
    5.15 -  | fold_bottom_mem thm (SOME set_def) =
    5.16 -    let val rule = @{lemma "A == B ==> bottom : B ==> bottom : A" by simp}
    5.17 -    in rule OF [set_def, thm] end
    5.18 -
    5.19  (* proving class instances *)
    5.20  
    5.21  fun prove_cpo
    5.22 @@ -77,14 +65,12 @@
    5.23        (newT: typ)
    5.24        (Rep_name: binding, Abs_name: binding)
    5.25        (type_definition: thm)  (* type_definition Rep Abs A *)
    5.26 -      (set_def: thm option)   (* A == set *)
    5.27        (below_def: thm)        (* op << == %x y. Rep x << Rep y *)
    5.28        (admissible: thm)       (* adm (%x. x : set) *)
    5.29        (thy: theory)
    5.30      =
    5.31    let
    5.32 -    val admissible' = fold_adm_mem admissible set_def
    5.33 -    val cpo_thms = map (Thm.transfer thy) [type_definition, below_def, admissible']
    5.34 +    val cpo_thms = map (Thm.transfer thy) [type_definition, below_def, admissible]
    5.35      val (full_tname, Ts) = dest_Type newT
    5.36      val lhs_sorts = map (snd o dest_TFree) Ts
    5.37      val tac = Tactic.rtac (@{thm typedef_cpo} OF cpo_thms) 1
    5.38 @@ -100,14 +86,14 @@
    5.39        thy
    5.40        |> Sign.add_path (Binding.name_of name)
    5.41        |> Global_Theory.add_thms
    5.42 -        ([((Binding.prefix_name "adm_"      name, admissible'), []),
    5.43 -          ((Binding.prefix_name "cont_" Rep_name, cont_Rep   ), []),
    5.44 -          ((Binding.prefix_name "cont_" Abs_name, cont_Abs   ), []),
    5.45 -          ((Binding.prefix_name "lub_"      name, lub        ), []),
    5.46 -          ((Binding.prefix_name "compact_"  name, compact    ), [])])
    5.47 +        ([((Binding.prefix_name "adm_"      name, admissible), []),
    5.48 +          ((Binding.prefix_name "cont_" Rep_name, cont_Rep  ), []),
    5.49 +          ((Binding.prefix_name "cont_" Abs_name, cont_Abs  ), []),
    5.50 +          ((Binding.prefix_name "lub_"      name, lub       ), []),
    5.51 +          ((Binding.prefix_name "compact_"  name, compact   ), [])])
    5.52        ||> Sign.parent_path
    5.53      val cpo_info : cpo_info =
    5.54 -      { below_def = below_def, adm = admissible', cont_Rep = cont_Rep,
    5.55 +      { below_def = below_def, adm = admissible, cont_Rep = cont_Rep,
    5.56          cont_Abs = cont_Abs, lub = lub, compact = compact }
    5.57    in
    5.58      (cpo_info, thy)
    5.59 @@ -118,14 +104,12 @@
    5.60        (newT: typ)
    5.61        (Rep_name: binding, Abs_name: binding)
    5.62        (type_definition: thm)  (* type_definition Rep Abs A *)
    5.63 -      (set_def: thm option)   (* A == set *)
    5.64        (below_def: thm)        (* op << == %x y. Rep x << Rep y *)
    5.65        (bottom_mem: thm)       (* bottom : set *)
    5.66        (thy: theory)
    5.67      =
    5.68    let
    5.69 -    val bottom_mem' = fold_bottom_mem bottom_mem set_def
    5.70 -    val pcpo_thms = map (Thm.transfer thy) [type_definition, below_def, bottom_mem']
    5.71 +    val pcpo_thms = map (Thm.transfer thy) [type_definition, below_def, bottom_mem]
    5.72      val (full_tname, Ts) = dest_Type newT
    5.73      val lhs_sorts = map (snd o dest_TFree) Ts
    5.74      val tac = Tactic.rtac (@{thm typedef_pcpo} OF pcpo_thms) 1
    5.75 @@ -184,7 +168,7 @@
    5.76    let
    5.77      val name = #1 typ
    5.78      val ((full_tname, info as ({Rep_name, ...}, {type_definition, ...})), thy) = thy
    5.79 -      |> Typedef.add_typedef_global false NONE typ set opt_morphs tac
    5.80 +      |> Typedef.add_typedef_global NONE typ set opt_morphs tac
    5.81      val oldT = #rep_type (#1 info)
    5.82      val newT = #abs_type (#1 info)
    5.83      val lhs_tfrees = map dest_TFree (snd (dest_Type newT))
    5.84 @@ -222,10 +206,10 @@
    5.85  
    5.86      fun cpodef_result nonempty admissible thy =
    5.87        let
    5.88 -        val ((info as (_, {type_definition, set_def, ...}), below_def), thy) = thy
    5.89 +        val ((info as (_, {type_definition, ...}), below_def), thy) = thy
    5.90            |> add_podef typ set opt_morphs (Tactic.rtac nonempty 1)
    5.91          val (cpo_info, thy) = thy
    5.92 -          |> prove_cpo name newT morphs type_definition set_def below_def admissible
    5.93 +          |> prove_cpo name newT morphs type_definition below_def admissible
    5.94        in
    5.95          ((info, cpo_info), thy)
    5.96        end
    5.97 @@ -256,12 +240,12 @@
    5.98      fun pcpodef_result bottom_mem admissible thy =
    5.99        let
   5.100          val tac = Tactic.rtac exI 1 THEN Tactic.rtac bottom_mem 1
   5.101 -        val ((info as (_, {type_definition, set_def, ...}), below_def), thy) = thy
   5.102 +        val ((info as (_, {type_definition, ...}), below_def), thy) = thy
   5.103            |> add_podef typ set opt_morphs tac
   5.104          val (cpo_info, thy) = thy
   5.105 -          |> prove_cpo name newT morphs type_definition set_def below_def admissible
   5.106 +          |> prove_cpo name newT morphs type_definition below_def admissible
   5.107          val (pcpo_info, thy) = thy
   5.108 -          |> prove_pcpo name newT morphs type_definition set_def below_def bottom_mem
   5.109 +          |> prove_pcpo name newT morphs type_definition below_def bottom_mem
   5.110        in
   5.111          ((info, cpo_info, pcpo_info), thy)
   5.112        end
     6.1 --- a/src/HOL/HOLCF/Tools/domaindef.ML	Fri Oct 12 14:05:30 2012 +0200
     6.2 +++ b/src/HOL/HOLCF/Tools/domaindef.ML	Fri Oct 12 15:08:29 2012 +0200
     6.3 @@ -162,12 +162,8 @@
     6.4      val liftemb_def = singleton (Proof_Context.export lthy ctxt_thy) liftemb_ldef
     6.5      val liftprj_def = singleton (Proof_Context.export lthy ctxt_thy) liftprj_ldef
     6.6      val liftdefl_def = singleton (Proof_Context.export lthy ctxt_thy) liftdefl_ldef
     6.7 -    val type_definition_thm =
     6.8 -      Raw_Simplifier.rewrite_rule
     6.9 -        (the_list (#set_def (#2 info)))
    6.10 -        (#type_definition (#2 info))
    6.11      val typedef_thms =
    6.12 -      [type_definition_thm, #below_def cpo_info, emb_def, prj_def, defl_def,
    6.13 +      [#type_definition (#2 info), #below_def cpo_info, emb_def, prj_def, defl_def,
    6.14        liftemb_def, liftprj_def, liftdefl_def]
    6.15      val thy = lthy
    6.16        |> Class.prove_instantiation_instance
     7.1 --- a/src/HOL/Import/import_rule.ML	Fri Oct 12 14:05:30 2012 +0200
     7.2 +++ b/src/HOL/Import/import_rule.ML	Fri Oct 12 15:08:29 2012 +0200
     7.3 @@ -220,7 +220,7 @@
     7.4      val tfrees = Term.add_tfrees c []
     7.5      val tnames = sort_strings (map fst tfrees)
     7.6      val ((_, typedef_info), thy') =
     7.7 -     Typedef.add_typedef_global false NONE
     7.8 +     Typedef.add_typedef_global NONE
     7.9         (Binding.name tycname, map (rpair dummyS) tnames, NoSyn) c
    7.10         (SOME(Binding.name rep_name,Binding.name abs_name)) (rtac th2 1) thy
    7.11      val aty = #abs_type (#1 typedef_info)
     8.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Fri Oct 12 14:05:30 2012 +0200
     8.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Fri Oct 12 15:08:29 2012 +0200
     8.3 @@ -572,7 +572,7 @@
     8.4      val (typedefs, thy6) =
     8.5        thy4
     8.6        |> fold_map (fn (((name, mx), tvs), (cname, U)) => fn thy =>
     8.7 -          Typedef.add_typedef_global false NONE
     8.8 +          Typedef.add_typedef_global NONE
     8.9              (name, map (fn (v, _) => (v, dummyS)) tvs, mx)  (* FIXME keep constraints!? *)
    8.10              (Const (@{const_name Collect}, (U --> HOLogic.boolT) --> HOLogic.mk_setT U) $
    8.11                 Const (cname, U --> HOLogic.boolT)) NONE
     9.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Fri Oct 12 14:05:30 2012 +0200
     9.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Fri Oct 12 15:08:29 2012 +0200
     9.3 @@ -190,7 +190,7 @@
     9.4        |> Sign.parent_path
     9.5        |> fold_map
     9.6          (fn (((name, mx), tvs), c) =>
     9.7 -          Typedef.add_typedef_global false NONE (name, tvs, mx)
     9.8 +          Typedef.add_typedef_global NONE (name, tvs, mx)
     9.9              (Collect $ Const (c, UnivT')) NONE
    9.10              (rtac exI 1 THEN rtac CollectI 1 THEN
    9.11                QUIET_BREADTH_FIRST (has_fewer_prems 1)
    10.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Oct 12 14:05:30 2012 +0200
    10.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Oct 12 15:08:29 2012 +0200
    10.3 @@ -559,15 +559,13 @@
    10.4  
    10.5  type typedef_info =
    10.6    {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string,
    10.7 -   set_def: thm option, prop_of_Rep: thm, set_name: string,
    10.8 -   Abs_inverse: thm option, Rep_inverse: thm option}
    10.9 +   prop_of_Rep: thm, set_name: string, Abs_inverse: thm option, Rep_inverse: thm option}
   10.10  
   10.11  fun typedef_info ctxt s =
   10.12    if is_frac_type ctxt (Type (s, [])) then
   10.13      SOME {abs_type = Type (s, []), rep_type = @{typ "int * int"},
   10.14            Abs_name = @{const_name Nitpick.Abs_Frac},
   10.15            Rep_name = @{const_name Nitpick.Rep_Frac},
   10.16 -          set_def = NONE,
   10.17            prop_of_Rep = @{prop "Nitpick.Rep_Frac x \<in> Collect Nitpick.Frac"}
   10.18                          |> Logic.varify_global,
   10.19            set_name = @{const_name Nitpick.Frac}, Abs_inverse = NONE,
   10.20 @@ -579,10 +577,10 @@
   10.21         types's type variables sometimes clash with locally fixed type variables.
   10.22         Remove these calls once "Typedef" is fully localized. *)
   10.23      ({abs_type, rep_type, Abs_name, Rep_name, ...},
   10.24 -     {set_def, Rep, Abs_inverse, Rep_inverse, ...}) :: _ =>
   10.25 +     {Rep, Abs_inverse, Rep_inverse, ...}) :: _ =>
   10.26      SOME {abs_type = Logic.varifyT_global abs_type,
   10.27            rep_type = Logic.varifyT_global rep_type, Abs_name = Abs_name,
   10.28 -          Rep_name = Rep_name, set_def = set_def, prop_of_Rep = prop_of Rep,
   10.29 +          Rep_name = Rep_name, prop_of_Rep = prop_of Rep,
   10.30            set_name = set_prefix ^ s, Abs_inverse = SOME Abs_inverse,
   10.31            Rep_inverse = SOME Rep_inverse}
   10.32    | _ => NONE
   10.33 @@ -683,13 +681,10 @@
   10.34    | is_pure_typedef _ _ = false
   10.35  fun is_univ_typedef ctxt (Type (s, _)) =
   10.36      (case typedef_info ctxt s of
   10.37 -       SOME {set_def, prop_of_Rep, ...} =>
   10.38 +       SOME {prop_of_Rep, ...} =>
   10.39         let
   10.40           val t_opt =
   10.41 -           case set_def of
   10.42 -             SOME thm => try (snd o Logic.dest_equals o prop_of) thm
   10.43 -           | NONE => try (snd o HOLogic.dest_mem o HOLogic.dest_Trueprop)
   10.44 -                         prop_of_Rep
   10.45 +           try (snd o HOLogic.dest_mem o HOLogic.dest_Trueprop) prop_of_Rep
   10.46         in
   10.47           case t_opt of
   10.48             SOME (Const (@{const_name top}, _)) => true
    11.1 --- a/src/HOL/Tools/Quotient/quotient_type.ML	Fri Oct 12 14:05:30 2012 +0200
    11.2 +++ b/src/HOL/Tools/Quotient/quotient_type.ML	Fri Oct 12 15:08:29 2012 +0200
    11.3 @@ -45,7 +45,7 @@
    11.4      val typedef_tac =
    11.5        EVERY1 (map rtac [@{thm part_equivp_typedef}, equiv_thm])
    11.6    in
    11.7 -    Typedef.add_typedef false NONE (qty_name, map (rpair dummyS) vs, mx)
    11.8 +    Typedef.add_typedef NONE (qty_name, map (rpair dummyS) vs, mx)
    11.9        (typedef_term rel rty lthy) NONE typedef_tac lthy
   11.10    end
   11.11  
    12.1 --- a/src/HOL/Tools/record.ML	Fri Oct 12 14:05:30 2012 +0200
    12.2 +++ b/src/HOL/Tools/record.ML	Fri Oct 12 15:08:29 2012 +0200
    12.3 @@ -112,7 +112,7 @@
    12.4      val vs = map (Proof_Context.check_tfree ctxt) raw_vs;
    12.5    in
    12.6      thy
    12.7 -    |> Typedef.add_typedef_global false (SOME raw_tyco) (raw_tyco, vs, NoSyn)
    12.8 +    |> Typedef.add_typedef_global (SOME raw_tyco) (raw_tyco, vs, NoSyn)
    12.9          (HOLogic.mk_UNIV repT) NONE (rtac UNIV_witness 1)
   12.10      |-> (fn (tyco, info) => get_typedef_info tyco vs info)
   12.11    end;
    13.1 --- a/src/HOL/Tools/typedef.ML	Fri Oct 12 14:05:30 2012 +0200
    13.2 +++ b/src/HOL/Tools/typedef.ML	Fri Oct 12 15:08:29 2012 +0200
    13.3 @@ -9,21 +9,21 @@
    13.4  sig
    13.5    type info =
    13.6     {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string, axiom_name: string} *
    13.7 -   {inhabited: thm, type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm,
    13.8 -    Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm,
    13.9 +   {inhabited: thm, type_definition: thm, Rep: thm, Rep_inverse: thm, Abs_inverse: thm,
   13.10 +    Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm,
   13.11      Rep_induct: thm, Abs_induct: thm}
   13.12    val transform_info: morphism -> info -> info
   13.13    val get_info: Proof.context -> string -> info list
   13.14    val get_info_global: theory -> string -> info list
   13.15    val interpretation: (string -> theory -> theory) -> theory -> theory
   13.16    val setup: theory -> theory
   13.17 -  val add_typedef: bool -> binding option -> binding * (string * sort) list * mixfix ->
   13.18 +  val add_typedef: binding option -> binding * (string * sort) list * mixfix ->
   13.19      term -> (binding * binding) option -> tactic -> local_theory -> (string * info) * local_theory
   13.20 -  val add_typedef_global: bool -> binding option -> binding * (string * sort) list * mixfix ->
   13.21 +  val add_typedef_global: binding option -> binding * (string * sort) list * mixfix ->
   13.22      term -> (binding * binding) option -> tactic -> theory -> (string * info) * theory
   13.23 -  val typedef: (bool * binding) * (binding * (string * sort) list * mixfix) * term *
   13.24 +  val typedef: binding * (binding * (string * sort) list * mixfix) * term *
   13.25      (binding * binding) option -> local_theory -> Proof.state
   13.26 -  val typedef_cmd: (bool * binding) * (binding * (string * string option) list * mixfix) * string *
   13.27 +  val typedef_cmd: binding * (binding * (string * string option) list * mixfix) * string *
   13.28      (binding * binding) option -> local_theory -> Proof.state
   13.29  end;
   13.30  
   13.31 @@ -38,23 +38,22 @@
   13.32    (*global part*)
   13.33    {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string, axiom_name: string} *
   13.34    (*local part*)
   13.35 -  {inhabited: thm, type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm,
   13.36 -    Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm,
   13.37 +  {inhabited: thm, type_definition: thm, Rep: thm, Rep_inverse: thm, Abs_inverse: thm,
   13.38 +    Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm,
   13.39      Rep_induct: thm, Abs_induct: thm};
   13.40  
   13.41  fun transform_info phi (info: info) =
   13.42    let
   13.43      val thm = Morphism.thm phi;
   13.44 -    val (global_info, {inhabited, type_definition,
   13.45 -      set_def, Rep, Rep_inverse, Abs_inverse, Rep_inject, Abs_inject,
   13.46 -      Rep_cases, Abs_cases, Rep_induct, Abs_induct}) = info;
   13.47 +    val (global_info, {inhabited, type_definition, Rep, Rep_inverse, Abs_inverse,
   13.48 +      Rep_inject, Abs_inject, Rep_cases, Abs_cases, Rep_induct, Abs_induct}) = info;
   13.49    in
   13.50      (global_info,
   13.51       {inhabited = thm inhabited, type_definition = thm type_definition,
   13.52 -      set_def = Option.map thm set_def, Rep = thm Rep, Rep_inverse = thm Rep_inverse,
   13.53 -      Abs_inverse = thm Abs_inverse, Rep_inject = thm Rep_inject, Abs_inject = thm Abs_inject,
   13.54 -      Rep_cases = thm Rep_cases, Abs_cases = thm Abs_cases, Rep_induct = thm Rep_induct,
   13.55 -      Abs_induct = thm Abs_induct})
   13.56 +      Rep = thm Rep, Rep_inverse = thm Rep_inverse, Abs_inverse = thm Abs_inverse,
   13.57 +      Rep_inject = thm Rep_inject, Abs_inject = thm Abs_inject,
   13.58 +      Rep_cases = thm Rep_cases, Abs_cases = thm Abs_cases,
   13.59 +      Rep_induct = thm Rep_induct, Abs_induct = thm Abs_induct})
   13.60    end;
   13.61  
   13.62  structure Data = Generic_Data
   13.63 @@ -129,7 +128,7 @@
   13.64  
   13.65  (* prepare_typedef *)
   13.66  
   13.67 -fun prepare_typedef prep_term def_set name (tname, raw_args, mx) raw_set opt_morphs lthy =
   13.68 +fun prepare_typedef prep_term name (tname, raw_args, mx) raw_set opt_morphs lthy =
   13.69    let
   13.70      val full_name = Local_Theory.full_name lthy name;
   13.71      val bname = Binding.name_of name;
   13.72 @@ -160,16 +159,6 @@
   13.73      val lhs_tfrees = map Term.dest_TFree type_args;
   13.74  
   13.75  
   13.76 -    (* set definition *)
   13.77 -
   13.78 -    val ((set', set_def), set_lthy) =
   13.79 -      if def_set then
   13.80 -        typedecl_lthy
   13.81 -        |> Local_Theory.define ((name, NoSyn), ((Thm.def_binding name, []), set))
   13.82 -        |>> (fn (set', (_, set_def)) => (set', SOME set_def))
   13.83 -      else ((set, NONE), typedecl_lthy);
   13.84 -
   13.85 -
   13.86      (* axiomatization *)
   13.87  
   13.88      val (Rep_name, Abs_name) =
   13.89 @@ -179,21 +168,8 @@
   13.90  
   13.91      val typedef_name = Binding.prefix_name "type_definition_" name;
   13.92  
   13.93 -    val ((RepC, AbsC, axiom_name, typedef), typedef_lthy) =
   13.94 -      let
   13.95 -        val thy = Proof_Context.theory_of set_lthy;
   13.96 -        val cert = Thm.cterm_of thy;
   13.97 -        val ((defs, _), A) =
   13.98 -          Local_Defs.export_cterm set_lthy (Proof_Context.init_global thy) (cert set')
   13.99 -          ||> Thm.term_of;
  13.100 -
  13.101 -        val ((RepC, AbsC, axiom_name, axiom), axiom_lthy) = set_lthy
  13.102 -          |> primitive_typedef typedef_name newT oldT Rep_name Abs_name A;
  13.103 -
  13.104 -        val cert = Thm.cterm_of (Proof_Context.theory_of axiom_lthy);
  13.105 -        val typedef =
  13.106 -          Local_Defs.contract defs (cert (mk_typedef newT oldT RepC AbsC set')) axiom;
  13.107 -      in ((RepC, AbsC, axiom_name, typedef), axiom_lthy) end;
  13.108 +    val ((RepC, AbsC, axiom_name, typedef), typedef_lthy) = typedecl_lthy
  13.109 +      |> primitive_typedef typedef_name newT oldT Rep_name Abs_name set;
  13.110  
  13.111      val alias_lthy = typedef_lthy
  13.112        |> Local_Theory.const_alias Rep_name (#1 (Term.dest_Const RepC))
  13.113 @@ -209,9 +185,7 @@
  13.114      fun typedef_result inhabited lthy1 =
  13.115        let
  13.116          val cert = Thm.cterm_of (Proof_Context.theory_of lthy1);
  13.117 -        val inhabited' =
  13.118 -          Local_Defs.contract (the_list set_def) (cert (mk_inhabited set')) inhabited;
  13.119 -        val typedef' = inhabited' RS typedef;
  13.120 +        val typedef' = inhabited RS typedef;
  13.121          fun make th = Goal.norm_result (typedef' RS th);
  13.122          val (((((((((((_, [type_definition]), Rep), Rep_inverse), Abs_inverse), Rep_inject),
  13.123              Abs_inject), Rep_cases), Abs_cases), Rep_induct), Abs_induct), lthy2) = lthy1
  13.124 @@ -241,7 +215,7 @@
  13.125          val info =
  13.126            ({rep_type = oldT, abs_type = newT, Rep_name = #1 (Term.dest_Const RepC),
  13.127              Abs_name = #1 (Term.dest_Const AbsC), axiom_name = axiom_name},
  13.128 -           {inhabited = inhabited, type_definition = type_definition, set_def = set_def,
  13.129 +           {inhabited = inhabited, type_definition = type_definition,
  13.130              Rep = Rep, Rep_inverse = Rep_inverse, Abs_inverse = Abs_inverse,
  13.131              Rep_inject = Rep_inject, Abs_inject = Abs_inject, Rep_cases = Rep_cases,
  13.132            Abs_cases = Abs_cases, Rep_induct = Rep_induct, Abs_induct = Abs_induct});
  13.133 @@ -260,19 +234,19 @@
  13.134  
  13.135  (* add_typedef: tactic interface *)
  13.136  
  13.137 -fun add_typedef def opt_name typ set opt_morphs tac lthy =
  13.138 +fun add_typedef opt_name typ set opt_morphs tac lthy =
  13.139    let
  13.140      val name = the_default (#1 typ) opt_name;
  13.141      val ((goal, _, typedef_result), lthy') =
  13.142 -      prepare_typedef Syntax.check_term def name typ set opt_morphs lthy;
  13.143 +      prepare_typedef Syntax.check_term name typ set opt_morphs lthy;
  13.144      val inhabited =
  13.145        Goal.prove lthy' [] [] goal (K tac)
  13.146        |> Goal.norm_result |> Thm.close_derivation;
  13.147    in typedef_result inhabited lthy' end;
  13.148  
  13.149 -fun add_typedef_global def opt_name typ set opt_morphs tac =
  13.150 +fun add_typedef_global opt_name typ set opt_morphs tac =
  13.151    Named_Target.theory_init
  13.152 -  #> add_typedef def opt_name typ set opt_morphs tac
  13.153 +  #> add_typedef opt_name typ set opt_morphs tac
  13.154    #> Local_Theory.exit_result_global (apsnd o transform_info);
  13.155  
  13.156  
  13.157 @@ -280,11 +254,11 @@
  13.158  
  13.159  local
  13.160  
  13.161 -fun gen_typedef prep_term prep_constraint ((def, name), (b, raw_args, mx), set, opt_morphs) lthy =
  13.162 +fun gen_typedef prep_term prep_constraint (name, (b, raw_args, mx), set, opt_morphs) lthy =
  13.163    let
  13.164      val args = map (apsnd (prep_constraint lthy)) raw_args;
  13.165      val ((goal, goal_pat, typedef_result), lthy') =
  13.166 -      prepare_typedef prep_term def name (b, args, mx) set opt_morphs lthy;
  13.167 +      prepare_typedef prep_term name (b, args, mx) set opt_morphs lthy;
  13.168      fun after_qed [[th]] = snd o typedef_result th;
  13.169    in Proof.theorem NONE after_qed [[(goal, [goal_pat])]] lthy' end;
  13.170  
  13.171 @@ -310,9 +284,9 @@
  13.172          Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding))
  13.173      >> (fn ((((((def, opt_name), (args, t)), mx), A), morphs)) => fn lthy =>
  13.174            (if def then
  13.175 -            legacy_feature "typedef with implicit set definition -- use \"typedef (open)\" instead"
  13.176 +            error "typedef with implicit set definition -- use \"typedef (open)\" instead"
  13.177             else ();
  13.178 -           typedef_cmd ((def, the_default t opt_name), (t, args, mx), A, morphs) lthy)));
  13.179 +           typedef_cmd (the_default t opt_name, (t, args, mx), A, morphs) lthy)));
  13.180  
  13.181  end;
  13.182