discontinued typedef with alternative name;
authorwenzelm
Fri Oct 12 21:22:35 2012 +0200 (2012-10-12)
changeset 4983531f32ec4d766
parent 49834 b27bbb021df1
child 49836 c13b39542972
discontinued typedef with alternative name;
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/Import/import_rule.ML
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Tools/Datatype/datatype.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 18:58:20 2012 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_comp.ML	Fri Oct 12 21:22:35 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 NONE (bdT_bind, params, NoSyn)
     1.8 +      typedef (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 18:58:20 2012 +0200
     2.2 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Fri Oct 12 21:22:35 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 NONE (sbdT_bind, dead_params, NoSyn)
     2.8 +            typedef (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 NONE (b, params, mx) car_final NONE
    2.17 +        typedef (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 18:58:20 2012 +0200
     3.2 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Fri Oct 12 21:22:35 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 NONE (IIT_bind, params, NoSyn)
     3.8 +      typedef (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 NONE (b, params, mx) car_init NONE
    3.17 +      |> fold_map3 (fn b => fn mx => fn car_init => typedef (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 18:58:20 2012 +0200
     4.2 +++ b/src/HOL/BNF/Tools/bnf_util.ML	Fri Oct 12 21:22:35 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: binding option -> binding * (string * sort) list * mixfix -> term ->
     4.8 +  val typedef: 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 opt_name typ set opt_morphs tac lthy =
    4.17 +fun typedef 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 opt_name typ set opt_morphs tac
    4.22 +      |> Typedef.add_typedef 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 18:58:20 2012 +0200
     5.2 +++ b/src/HOL/HOLCF/Tools/cpodef.ML	Fri Oct 12 21:22:35 2012 +0200
     5.3 @@ -168,7 +168,7 @@
     5.4    let
     5.5      val name = #1 typ
     5.6      val ((full_tname, info as ({Rep_name, ...}, {type_definition, ...})), thy) = thy
     5.7 -      |> Typedef.add_typedef_global NONE typ set opt_morphs tac
     5.8 +      |> Typedef.add_typedef_global typ set opt_morphs tac
     5.9      val oldT = #rep_type (#1 info)
    5.10      val newT = #abs_type (#1 info)
    5.11      val lhs_tfrees = map dest_TFree (snd (dest_Type newT))
     6.1 --- a/src/HOL/Import/import_rule.ML	Fri Oct 12 18:58:20 2012 +0200
     6.2 +++ b/src/HOL/Import/import_rule.ML	Fri Oct 12 21:22:35 2012 +0200
     6.3 @@ -220,9 +220,8 @@
     6.4      val tfrees = Term.add_tfrees c []
     6.5      val tnames = sort_strings (map fst tfrees)
     6.6      val ((_, typedef_info), thy') =
     6.7 -     Typedef.add_typedef_global NONE
     6.8 -       (Binding.name tycname, map (rpair dummyS) tnames, NoSyn) c
     6.9 -       (SOME(Binding.name rep_name,Binding.name abs_name)) (rtac th2 1) thy
    6.10 +     Typedef.add_typedef_global (Binding.name tycname, map (rpair dummyS) tnames, NoSyn) c
    6.11 +       (SOME (Binding.name rep_name, Binding.name abs_name)) (rtac th2 1) thy
    6.12      val aty = #abs_type (#1 typedef_info)
    6.13      val th = freezeT (#type_definition (#2 typedef_info))
    6.14      val (th_s, _) = Thm.dest_comb (Thm.dest_arg (cprop_of th))
     7.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Fri Oct 12 18:58:20 2012 +0200
     7.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Fri Oct 12 21:22:35 2012 +0200
     7.3 @@ -572,7 +572,7 @@
     7.4      val (typedefs, thy6) =
     7.5        thy4
     7.6        |> fold_map (fn (((name, mx), tvs), (cname, U)) => fn thy =>
     7.7 -          Typedef.add_typedef_global NONE
     7.8 +          Typedef.add_typedef_global
     7.9              (name, map (fn (v, _) => (v, dummyS)) tvs, mx)  (* FIXME keep constraints!? *)
    7.10              (Const (@{const_name Collect}, (U --> HOLogic.boolT) --> HOLogic.mk_setT U) $
    7.11                 Const (cname, U --> HOLogic.boolT)) NONE
     8.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Fri Oct 12 18:58:20 2012 +0200
     8.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Fri Oct 12 21:22:35 2012 +0200
     8.3 @@ -190,7 +190,7 @@
     8.4        |> Sign.parent_path
     8.5        |> fold_map
     8.6          (fn (((name, mx), tvs), c) =>
     8.7 -          Typedef.add_typedef_global NONE (name, tvs, mx)
     8.8 +          Typedef.add_typedef_global (name, tvs, mx)
     8.9              (Collect $ Const (c, UnivT')) NONE
    8.10              (rtac exI 1 THEN rtac CollectI 1 THEN
    8.11                QUIET_BREADTH_FIRST (has_fewer_prems 1)
     9.1 --- a/src/HOL/Tools/Quotient/quotient_type.ML	Fri Oct 12 18:58:20 2012 +0200
     9.2 +++ b/src/HOL/Tools/Quotient/quotient_type.ML	Fri Oct 12 21:22:35 2012 +0200
     9.3 @@ -45,7 +45,7 @@
     9.4      val typedef_tac =
     9.5        EVERY1 (map rtac [@{thm part_equivp_typedef}, equiv_thm])
     9.6    in
     9.7 -    Typedef.add_typedef NONE (qty_name, map (rpair dummyS) vs, mx)
     9.8 +    Typedef.add_typedef (qty_name, map (rpair dummyS) vs, mx)
     9.9        (typedef_term rel rty lthy) NONE typedef_tac lthy
    9.10    end
    9.11  
    10.1 --- a/src/HOL/Tools/record.ML	Fri Oct 12 18:58:20 2012 +0200
    10.2 +++ b/src/HOL/Tools/record.ML	Fri Oct 12 21:22:35 2012 +0200
    10.3 @@ -112,7 +112,7 @@
    10.4      val vs = map (Proof_Context.check_tfree ctxt) raw_vs;
    10.5    in
    10.6      thy
    10.7 -    |> Typedef.add_typedef_global (SOME raw_tyco) (raw_tyco, vs, NoSyn)
    10.8 +    |> Typedef.add_typedef_global (raw_tyco, vs, NoSyn)
    10.9          (HOLogic.mk_UNIV repT) NONE (rtac UNIV_witness 1)
   10.10      |-> (fn (tyco, info) => get_typedef_info tyco vs info)
   10.11    end;
    11.1 --- a/src/HOL/Tools/typedef.ML	Fri Oct 12 18:58:20 2012 +0200
    11.2 +++ b/src/HOL/Tools/typedef.ML	Fri Oct 12 21:22:35 2012 +0200
    11.3 @@ -17,13 +17,13 @@
    11.4    val get_info_global: theory -> string -> info list
    11.5    val interpretation: (string -> theory -> theory) -> theory -> theory
    11.6    val setup: theory -> theory
    11.7 -  val add_typedef: binding option -> binding * (string * sort) list * mixfix ->
    11.8 +  val add_typedef: binding * (string * sort) list * mixfix ->
    11.9      term -> (binding * binding) option -> tactic -> local_theory -> (string * info) * local_theory
   11.10 -  val add_typedef_global: binding option -> binding * (string * sort) list * mixfix ->
   11.11 +  val add_typedef_global: binding * (string * sort) list * mixfix ->
   11.12      term -> (binding * binding) option -> tactic -> theory -> (string * info) * theory
   11.13 -  val typedef: binding * (binding * (string * sort) list * mixfix) * term *
   11.14 +  val typedef: (binding * (string * sort) list * mixfix) * term *
   11.15      (binding * binding) option -> local_theory -> Proof.state
   11.16 -  val typedef_cmd: binding * (binding * (string * string option) list * mixfix) * string *
   11.17 +  val typedef_cmd: (binding * (string * string option) list * mixfix) * string *
   11.18      (binding * binding) option -> local_theory -> Proof.state
   11.19  end;
   11.20  
   11.21 @@ -128,9 +128,8 @@
   11.22  
   11.23  (* prepare_typedef *)
   11.24  
   11.25 -fun prepare_typedef prep_term name (tname, raw_args, mx) raw_set opt_morphs lthy =
   11.26 +fun prepare_typedef prep_term (name, raw_args, mx) raw_set opt_morphs lthy =
   11.27    let
   11.28 -    val full_name = Local_Theory.full_name lthy name;
   11.29      val bname = Binding.name_of name;
   11.30  
   11.31  
   11.32 @@ -152,10 +151,10 @@
   11.33  
   11.34      val args = map (Proof_Context.check_tfree tmp_ctxt') raw_args;
   11.35      val (newT, typedecl_lthy) = lthy
   11.36 -      |> Typedecl.typedecl (tname, args, mx)
   11.37 +      |> Typedecl.typedecl (name, args, mx)
   11.38        ||> Variable.declare_term set;
   11.39  
   11.40 -    val Type (full_tname, type_args) = newT;
   11.41 +    val Type (full_name, type_args) = newT;
   11.42      val lhs_tfrees = map Term.dest_TFree type_args;
   11.43  
   11.44  
   11.45 @@ -203,13 +202,13 @@
   11.46                  [Rule_Cases.case_names [Binding.name_of Rep_name], Induct.cases_pred full_name]),
   11.47                make @{thm type_definition.Rep_cases})
   11.48            ||>> note_qualify ((Binding.suffix_name "_cases" Abs_name,
   11.49 -                [Rule_Cases.case_names [Binding.name_of Abs_name], Induct.cases_type full_tname]),
   11.50 +                [Rule_Cases.case_names [Binding.name_of Abs_name], Induct.cases_type full_name]),
   11.51                make @{thm type_definition.Abs_cases})
   11.52            ||>> note_qualify ((Binding.suffix_name "_induct" Rep_name,
   11.53                  [Rule_Cases.case_names [Binding.name_of Rep_name], Induct.induct_pred full_name]),
   11.54                make @{thm type_definition.Rep_induct})
   11.55            ||>> note_qualify ((Binding.suffix_name "_induct" Abs_name,
   11.56 -                [Rule_Cases.case_names [Binding.name_of Abs_name], Induct.induct_type full_tname]),
   11.57 +                [Rule_Cases.case_names [Binding.name_of Abs_name], Induct.induct_type full_name]),
   11.58                make @{thm type_definition.Abs_induct});
   11.59  
   11.60          val info =
   11.61 @@ -222,9 +221,9 @@
   11.62        in
   11.63          lthy2
   11.64          |> Local_Theory.declaration {syntax = false, pervasive = true}
   11.65 -          (fn phi => put_info full_tname (transform_info phi info))
   11.66 -        |> Local_Theory.background_theory (Typedef_Interpretation.data full_tname)
   11.67 -        |> pair (full_tname, info)
   11.68 +          (fn phi => put_info full_name (transform_info phi info))
   11.69 +        |> Local_Theory.background_theory (Typedef_Interpretation.data full_name)
   11.70 +        |> pair (full_name, info)
   11.71        end;
   11.72  
   11.73    in ((goal, goal_pat, typedef_result), alias_lthy) end
   11.74 @@ -234,19 +233,18 @@
   11.75  
   11.76  (* add_typedef: tactic interface *)
   11.77  
   11.78 -fun add_typedef opt_name typ set opt_morphs tac lthy =
   11.79 +fun add_typedef typ set opt_morphs tac lthy =
   11.80    let
   11.81 -    val name = the_default (#1 typ) opt_name;
   11.82      val ((goal, _, typedef_result), lthy') =
   11.83 -      prepare_typedef Syntax.check_term name typ set opt_morphs lthy;
   11.84 +      prepare_typedef Syntax.check_term typ set opt_morphs lthy;
   11.85      val inhabited =
   11.86        Goal.prove lthy' [] [] goal (K tac)
   11.87        |> Goal.norm_result |> Thm.close_derivation;
   11.88    in typedef_result inhabited lthy' end;
   11.89  
   11.90 -fun add_typedef_global opt_name typ set opt_morphs tac =
   11.91 +fun add_typedef_global typ set opt_morphs tac =
   11.92    Named_Target.theory_init
   11.93 -  #> add_typedef opt_name typ set opt_morphs tac
   11.94 +  #> add_typedef typ set opt_morphs tac
   11.95    #> Local_Theory.exit_result_global (apsnd o transform_info);
   11.96  
   11.97  
   11.98 @@ -254,11 +252,11 @@
   11.99  
  11.100  local
  11.101  
  11.102 -fun gen_typedef prep_term prep_constraint (name, (b, raw_args, mx), set, opt_morphs) lthy =
  11.103 +fun gen_typedef prep_term prep_constraint ((b, raw_args, mx), set, opt_morphs) lthy =
  11.104    let
  11.105      val args = map (apsnd (prep_constraint lthy)) raw_args;
  11.106      val ((goal, goal_pat, typedef_result), lthy') =
  11.107 -      prepare_typedef prep_term name (b, args, mx) set opt_morphs lthy;
  11.108 +      prepare_typedef prep_term (b, args, mx) set opt_morphs lthy;
  11.109      fun after_qed [[th]] = snd o typedef_result th;
  11.110    in Proof.theorem NONE after_qed [[(goal, [goal_pat])]] lthy' end;
  11.111  
  11.112 @@ -276,12 +274,10 @@
  11.113  val _ =
  11.114    Outer_Syntax.local_theory_to_proof @{command_spec "typedef"}
  11.115      "HOL type definition (requires non-emptiness proof)"
  11.116 -    (Scan.option (@{keyword "("} |-- Parse.binding --| @{keyword ")"}) --
  11.117 -      (Parse.type_args_constrained -- Parse.binding) --
  11.118 -        Parse.opt_mixfix -- (@{keyword "="} |-- Parse.term) --
  11.119 -        Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding))
  11.120 -    >> (fn (((((opt_name, (args, t)), mx), A), morphs)) => fn lthy =>
  11.121 -           typedef_cmd (the_default t opt_name, (t, args, mx), A, morphs) lthy));
  11.122 +    (Parse.type_args_constrained -- Parse.binding -- Parse.opt_mixfix --
  11.123 +      (@{keyword "="} |-- Parse.term) --
  11.124 +      Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding))
  11.125 +    >> (fn ((((vs, t), mx), A), morphs) => fn lthy => typedef_cmd ((t, vs, mx), A, morphs) lthy));
  11.126  
  11.127  end;
  11.128