explicit indication of overloaded typedefs;
authorwenzelm
Thu Sep 24 13:33:42 2015 +0200 (2015-09-24)
changeset 61260e6f03fae14d5
parent 61259 6dc3d5d50e57
child 61261 ddb2da7cb2e4
explicit indication of overloaded typedefs;
src/Doc/Isar_Ref/HOL_Specific.thy
src/HOL/Datatype_Examples/Misc_N2M.thy
src/HOL/Datatype_Examples/Stream_Processor.thy
src/HOL/HOLCF/Porder.thy
src/HOL/HOLCF/Tools/cpodef.ML
src/HOL/IMP/Abs_State.thy
src/HOL/Import/import_rule.ML
src/HOL/Library/Fraction_Field.thy
src/HOL/Library/Polynomial.thy
src/HOL/Library/Quotient_Type.thy
src/HOL/Library/RBT.thy
src/HOL/Library/Saturated.thy
src/HOL/Matrix_LP/Matrix.thy
src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy
src/HOL/Nominal/Nominal.thy
src/HOL/Nominal/nominal_datatype.ML
src/HOL/SPARK/Tools/spark_vcs.ML
src/HOL/Tools/BNF/bnf_util.ML
src/HOL/Tools/Old_Datatype/old_datatype.ML
src/HOL/Tools/Quotient/quotient_type.ML
src/HOL/Tools/record.ML
src/HOL/Tools/typedef.ML
src/HOL/Word/Word.thy
src/HOL/ex/PER.thy
src/Pure/Isar/parse_spec.ML
src/Pure/defs.ML
     1.1 --- a/src/Doc/Isar_Ref/HOL_Specific.thy	Wed Sep 23 09:50:38 2015 +0200
     1.2 +++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Thu Sep 24 13:33:42 2015 +0200
     1.3 @@ -932,7 +932,7 @@
     1.4    \end{matharray}
     1.5  
     1.6    @{rail \<open>
     1.7 -    @@{command (HOL) record} @{syntax typespec_sorts} '=' \<newline>
     1.8 +    @@{command (HOL) record} @{syntax "overloaded"}? @{syntax typespec_sorts} '=' \<newline>
     1.9        (@{syntax type} '+')? (constdecl +)
    1.10      ;
    1.11      constdecl: @{syntax name} '::' @{syntax type} @{syntax mixfix}?
    1.12 @@ -1131,7 +1131,9 @@
    1.13    definition, but less powerful in practice.
    1.14  
    1.15    @{rail \<open>
    1.16 -    @@{command (HOL) typedef} abs_type '=' rep_set
    1.17 +    @@{command (HOL) typedef} @{syntax "overloaded"}? abs_type '=' rep_set
    1.18 +    ;
    1.19 +    @{syntax_def "overloaded"}: ('(' @'overloaded' ')')
    1.20      ;
    1.21      abs_type: @{syntax typespec_sorts} @{syntax mixfix}?
    1.22      ;
    1.23 @@ -1185,6 +1187,13 @@
    1.24    for the generic @{method cases} and @{method induct} methods,
    1.25    respectively.
    1.26  
    1.27 +  \medskip The ``@{text "(overloaded)"}'' option allows the @{command
    1.28 +  "typedef"} specification to depend on constants that are not (yet)
    1.29 +  specified and thus left open as parameters. In particular, a @{command
    1.30 +  typedef} depending on type-class parameters (cf.\ \secref{sec:class}) is
    1.31 +  semantically like a dependent type: its meaning is determined for
    1.32 +  different type-class instances according to their respective operations.
    1.33 +
    1.34    \end{description}
    1.35  \<close>
    1.36  
    1.37 @@ -1299,8 +1308,9 @@
    1.38    \end{matharray}
    1.39  
    1.40    @{rail \<open>
    1.41 -    @@{command (HOL) quotient_type} @{syntax typespec} @{syntax mixfix}? '='
    1.42 -      quot_type \<newline> quot_morphisms? quot_parametric?
    1.43 +    @@{command (HOL) quotient_type} @{syntax "overloaded"}? \<newline>
    1.44 +      @{syntax typespec} @{syntax mixfix}? '=' quot_type \<newline>
    1.45 +      quot_morphisms? quot_parametric?
    1.46      ;
    1.47      quot_type: @{syntax type} '/' ('partial' ':')? @{syntax term}
    1.48      ;
     2.1 --- a/src/HOL/Datatype_Examples/Misc_N2M.thy	Wed Sep 23 09:50:38 2015 +0200
     2.2 +++ b/src/HOL/Datatype_Examples/Misc_N2M.thy	Thu Sep 24 13:33:42 2015 +0200
     2.3 @@ -11,6 +11,9 @@
     2.4  imports "~~/src/HOL/Library/BNF_Axiomatization"
     2.5  begin
     2.6  
     2.7 +declare [[typedef_overloaded]]
     2.8 +
     2.9 +
    2.10  locale misc
    2.11  begin
    2.12  
     3.1 --- a/src/HOL/Datatype_Examples/Stream_Processor.thy	Wed Sep 23 09:50:38 2015 +0200
     3.2 +++ b/src/HOL/Datatype_Examples/Stream_Processor.thy	Thu Sep 24 13:33:42 2015 +0200
     3.3 @@ -12,6 +12,9 @@
     3.4  imports "~~/src/HOL/Library/Stream" "~~/src/HOL/Library/BNF_Axiomatization"
     3.5  begin
     3.6  
     3.7 +declare [[typedef_overloaded]]
     3.8 +
     3.9 +
    3.10  section {* Continuous Functions on Streams *}
    3.11  
    3.12  datatype ('a, 'b, 'c) sp\<^sub>\<mu> = Get "'a \<Rightarrow> ('a, 'b, 'c) sp\<^sub>\<mu>" | Put "'b" "'c"
     4.1 --- a/src/HOL/HOLCF/Porder.thy	Wed Sep 23 09:50:38 2015 +0200
     4.2 +++ b/src/HOL/HOLCF/Porder.thy	Thu Sep 24 13:33:42 2015 +0200
     4.3 @@ -8,6 +8,9 @@
     4.4  imports Main
     4.5  begin
     4.6  
     4.7 +declare [[typedef_overloaded]]
     4.8 +
     4.9 +
    4.10  subsection {* Type class for partial orders *}
    4.11  
    4.12  class below =
     5.1 --- a/src/HOL/HOLCF/Tools/cpodef.ML	Wed Sep 23 09:50:38 2015 +0200
     5.2 +++ b/src/HOL/HOLCF/Tools/cpodef.ML	Thu Sep 24 13:33:42 2015 +0200
     5.3 @@ -165,7 +165,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 typ set opt_bindings tac
     5.8 +      |> Typedef.add_typedef_global {overloaded = false} typ set opt_bindings 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/IMP/Abs_State.thy	Wed Sep 23 09:50:38 2015 +0200
     6.2 +++ b/src/HOL/IMP/Abs_State.thy	Thu Sep 24 13:33:42 2015 +0200
     6.3 @@ -19,7 +19,7 @@
     6.4  
     6.5  hide_type st  --"hide previous def to avoid long names"
     6.6  
     6.7 -quotient_type 'a st = "('a::top) st_rep" / eq_st
     6.8 +quotient_type (overloaded) 'a st = "('a::top) st_rep" / eq_st
     6.9  morphisms rep_st St
    6.10  by (metis eq_st_def equivpI reflpI sympI transpI)
    6.11  
     7.1 --- a/src/HOL/Import/import_rule.ML	Wed Sep 23 09:50:38 2015 +0200
     7.2 +++ b/src/HOL/Import/import_rule.ML	Thu Sep 24 13:33:42 2015 +0200
     7.3 @@ -222,7 +222,8 @@
     7.4        Typedef.make_morphisms (Binding.name tycname)
     7.5          (SOME (Binding.name rep_name, Binding.name abs_name))
     7.6      val ((_, typedef_info), thy') =
     7.7 -     Typedef.add_typedef_global (Binding.name tycname, map (rpair dummyS) tnames, NoSyn) c
     7.8 +     Typedef.add_typedef_global {overloaded = false}
     7.9 +       (Binding.name tycname, map (rpair dummyS) tnames, NoSyn) c
    7.10         (SOME typedef_bindings) (fn ctxt => resolve_tac ctxt [th2] 1) thy
    7.11      val aty = #abs_type (#1 typedef_info)
    7.12      val th = freezeT thy' (#type_definition (#2 typedef_info))
     8.1 --- a/src/HOL/Library/Fraction_Field.thy	Wed Sep 23 09:50:38 2015 +0200
     8.2 +++ b/src/HOL/Library/Fraction_Field.thy	Thu Sep 24 13:33:42 2015 +0200
     8.3 @@ -47,7 +47,7 @@
     8.4  
     8.5  end
     8.6  
     8.7 -quotient_type 'a fract = "'a :: idom \<times> 'a" / partial: "fractrel"
     8.8 +quotient_type (overloaded) 'a fract = "'a :: idom \<times> 'a" / partial: "fractrel"
     8.9  by(rule part_equivp_fractrel)
    8.10  
    8.11  subsubsection \<open>Representation and basic operations\<close>
     9.1 --- a/src/HOL/Library/Polynomial.thy	Wed Sep 23 09:50:38 2015 +0200
     9.2 +++ b/src/HOL/Library/Polynomial.thy	Thu Sep 24 13:33:42 2015 +0200
     9.3 @@ -52,7 +52,7 @@
     9.4  
     9.5  subsection \<open>Definition of type @{text poly}\<close>
     9.6  
     9.7 -typedef 'a poly = "{f :: nat \<Rightarrow> 'a::zero. \<forall>\<^sub>\<infinity> n. f n = 0}"
     9.8 +typedef (overloaded) 'a poly = "{f :: nat \<Rightarrow> 'a::zero. \<forall>\<^sub>\<infinity> n. f n = 0}"
     9.9    morphisms coeff Abs_poly by (auto intro!: ALL_MOST)
    9.10  
    9.11  setup_lifting type_definition_poly
    10.1 --- a/src/HOL/Library/Quotient_Type.thy	Wed Sep 23 09:50:38 2015 +0200
    10.2 +++ b/src/HOL/Library/Quotient_Type.thy	Thu Sep 24 13:33:42 2015 +0200
    10.3 @@ -62,7 +62,7 @@
    10.4  
    10.5  definition (in eqv) "quot = {{x. a \<sim> x} | a. True}"
    10.6  
    10.7 -typedef 'a quot = "quot :: 'a::eqv set set"
    10.8 +typedef (overloaded) 'a quot = "quot :: 'a::eqv set set"
    10.9    unfolding quot_def by blast
   10.10  
   10.11  lemma quotI [intro]: "{x. a \<sim> x} \<in> quot"
    11.1 --- a/src/HOL/Library/RBT.thy	Wed Sep 23 09:50:38 2015 +0200
    11.2 +++ b/src/HOL/Library/RBT.thy	Thu Sep 24 13:33:42 2015 +0200
    11.3 @@ -10,7 +10,7 @@
    11.4  
    11.5  subsection \<open>Type definition\<close>
    11.6  
    11.7 -typedef ('a, 'b) rbt = "{t :: ('a::linorder, 'b) RBT_Impl.rbt. is_rbt t}"
    11.8 +typedef (overloaded) ('a, 'b) rbt = "{t :: ('a::linorder, 'b) RBT_Impl.rbt. is_rbt t}"
    11.9    morphisms impl_of RBT
   11.10  proof -
   11.11    have "RBT_Impl.Empty \<in> ?rbt" by simp
    12.1 --- a/src/HOL/Library/Saturated.thy	Wed Sep 23 09:50:38 2015 +0200
    12.2 +++ b/src/HOL/Library/Saturated.thy	Thu Sep 24 13:33:42 2015 +0200
    12.3 @@ -12,7 +12,7 @@
    12.4  
    12.5  subsection \<open>The type of saturated naturals\<close>
    12.6  
    12.7 -typedef ('a::len) sat = "{.. len_of TYPE('a)}"
    12.8 +typedef (overloaded) ('a::len) sat = "{.. len_of TYPE('a)}"
    12.9    morphisms nat_of Abs_sat
   12.10    by auto
   12.11  
    13.1 --- a/src/HOL/Matrix_LP/Matrix.thy	Wed Sep 23 09:50:38 2015 +0200
    13.2 +++ b/src/HOL/Matrix_LP/Matrix.thy	Thu Sep 24 13:33:42 2015 +0200
    13.3 @@ -13,7 +13,7 @@
    13.4  
    13.5  definition "matrix = {(f::(nat \<Rightarrow> nat \<Rightarrow> 'a::zero)). finite (nonzero_positions f)}"
    13.6  
    13.7 -typedef 'a matrix = "matrix :: (nat \<Rightarrow> nat \<Rightarrow> 'a::zero) set"
    13.8 +typedef (overloaded) 'a matrix = "matrix :: (nat \<Rightarrow> nat \<Rightarrow> 'a::zero) set"
    13.9    unfolding matrix_def
   13.10  proof
   13.11    show "(\<lambda>j i. 0) \<in> {(f::(nat \<Rightarrow> nat \<Rightarrow> 'a::zero)). finite (nonzero_positions f)}"
    14.1 --- a/src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy	Wed Sep 23 09:50:38 2015 +0200
    14.2 +++ b/src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy	Thu Sep 24 13:33:42 2015 +0200
    14.3 @@ -9,7 +9,8 @@
    14.4  definition bcontfun :: "('a::topological_space \<Rightarrow> 'b::metric_space) set"
    14.5    where "bcontfun = {f. continuous_on UNIV f \<and> bounded (range f)}"
    14.6  
    14.7 -typedef ('a, 'b) bcontfun = "bcontfun :: ('a::topological_space \<Rightarrow> 'b::metric_space) set"
    14.8 +typedef (overloaded) ('a, 'b) bcontfun =
    14.9 +    "bcontfun :: ('a::topological_space \<Rightarrow> 'b::metric_space) set"
   14.10    by (auto simp: bcontfun_def intro: continuous_intros simp: bounded_def)
   14.11  
   14.12  lemma bcontfunE:
    15.1 --- a/src/HOL/Nominal/Nominal.thy	Wed Sep 23 09:50:38 2015 +0200
    15.2 +++ b/src/HOL/Nominal/Nominal.thy	Thu Sep 24 13:33:42 2015 +0200
    15.3 @@ -6,6 +6,9 @@
    15.4    "avoids"
    15.5  begin
    15.6  
    15.7 +declare [[typedef_overloaded]]
    15.8 +
    15.9 +
   15.10  section {* Permutations *}
   15.11  (*======================*)
   15.12  
   15.13 @@ -3378,7 +3381,7 @@
   15.14  
   15.15  definition "ABS = ABS_set"
   15.16  
   15.17 -typedef ('x,'a) ABS ("\<guillemotleft>_\<guillemotright>_" [1000,1000] 1000) =
   15.18 +typedef ('x, 'a) ABS ("\<guillemotleft>_\<guillemotright>_" [1000,1000] 1000) =
   15.19      "ABS::('x\<Rightarrow>('a noption)) set"
   15.20    morphisms Rep_ABS Abs_ABS
   15.21    unfolding ABS_def
    16.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Wed Sep 23 09:50:38 2015 +0200
    16.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Thu Sep 24 13:33:42 2015 +0200
    16.3 @@ -586,7 +586,7 @@
    16.4      val (typedefs, thy6) =
    16.5        thy4
    16.6        |> fold_map (fn (((name, mx), tvs), (cname, U)) => fn thy =>
    16.7 -          Typedef.add_typedef_global
    16.8 +          Typedef.add_typedef_global {overloaded = false}
    16.9              (name, map (fn (v, _) => (v, dummyS)) tvs, mx)  (* FIXME keep constraints!? *)
   16.10              (Const (@{const_name Collect}, (U --> HOLogic.boolT) --> HOLogic.mk_setT U) $
   16.11                 Const (cname, U --> HOLogic.boolT)) NONE
    17.1 --- a/src/HOL/SPARK/Tools/spark_vcs.ML	Wed Sep 23 09:50:38 2015 +0200
    17.2 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Thu Sep 24 13:33:42 2015 +0200
    17.3 @@ -359,7 +359,7 @@
    17.4           map (rpair (mk_type thy prfx ty)) flds) fldtys
    17.5         in case get_type thy prfx s of
    17.6             NONE =>
    17.7 -             Record.add_record ([], Binding.name s) NONE
    17.8 +             Record.add_record {overloaded = false} ([], Binding.name s) NONE
    17.9                 (map (fn (fld, T) => (Binding.name fld, T, NoSyn)) fldTs) thy
   17.10           | SOME (rT, cmap) =>
   17.11               (case get_record_info thy rT of
    18.1 --- a/src/HOL/Tools/BNF/bnf_util.ML	Wed Sep 23 09:50:38 2015 +0200
    18.2 +++ b/src/HOL/Tools/BNF/bnf_util.ML	Thu Sep 24 13:33:42 2015 +0200
    18.3 @@ -156,7 +156,7 @@
    18.4      val ((name, info), (lthy, lthy_old)) =
    18.5        lthy
    18.6        |> Local_Theory.open_target |> snd
    18.7 -      |> Typedef.add_typedef (b', Ts, mx) set (SOME bindings) tac
    18.8 +      |> Typedef.add_typedef {overloaded = false} (b', Ts, mx) set (SOME bindings) tac
    18.9        ||> `Local_Theory.close_target;
   18.10      val phi = Proof_Context.export_morphism lthy_old lthy;
   18.11    in
    19.1 --- a/src/HOL/Tools/Old_Datatype/old_datatype.ML	Wed Sep 23 09:50:38 2015 +0200
    19.2 +++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML	Thu Sep 24 13:33:42 2015 +0200
    19.3 @@ -186,7 +186,7 @@
    19.4        |> Sign.parent_path
    19.5        |> fold_map
    19.6          (fn (((name, mx), tvs), c) =>
    19.7 -          Typedef.add_typedef_global (name, tvs, mx)
    19.8 +          Typedef.add_typedef_global {overloaded = false} (name, tvs, mx)
    19.9              (Collect $ Const (c, UnivT')) NONE
   19.10              (fn ctxt =>
   19.11                resolve_tac ctxt [exI] 1 THEN
    20.1 --- a/src/HOL/Tools/Quotient/quotient_type.ML	Wed Sep 23 09:50:38 2015 +0200
    20.2 +++ b/src/HOL/Tools/Quotient/quotient_type.ML	Thu Sep 24 13:33:42 2015 +0200
    20.3 @@ -6,14 +6,17 @@
    20.4  
    20.5  signature QUOTIENT_TYPE =
    20.6  sig
    20.7 -  val add_quotient_type: ((string list * binding * mixfix) * (typ * term * bool) *
    20.8 -    ((binding * binding) option * thm option)) * thm -> local_theory -> Quotient_Info.quotients * local_theory
    20.9 -
   20.10 -  val quotient_type: (string list * binding * mixfix) * (typ * term * bool) *
   20.11 -    ((binding * binding) option * thm option) -> Proof.context -> Proof.state
   20.12 -
   20.13 -  val quotient_type_cmd: (((((string list * binding) * mixfix) * string) * (bool * string)) *
   20.14 -    (binding * binding) option) * (Facts.ref * Token.src list) option -> Proof.context -> Proof.state
   20.15 +  val add_quotient_type: {overloaded: bool} ->
   20.16 +    ((string list * binding * mixfix) * (typ * term * bool) *
   20.17 +      ((binding * binding) option * thm option)) * thm -> local_theory ->
   20.18 +      Quotient_Info.quotients * local_theory
   20.19 +  val quotient_type:  {overloaded: bool} ->
   20.20 +    (string list * binding * mixfix) * (typ * term * bool) *
   20.21 +      ((binding * binding) option * thm option) -> Proof.context -> Proof.state
   20.22 +  val quotient_type_cmd:  {overloaded: bool} ->
   20.23 +    (((((string list * binding) * mixfix) * string) * (bool * string)) *
   20.24 +      (binding * binding) option) * (Facts.ref * Token.src list) option ->
   20.25 +      Proof.context -> Proof.state
   20.26  end;
   20.27  
   20.28  structure Quotient_Type: QUOTIENT_TYPE =
   20.29 @@ -40,12 +43,12 @@
   20.30  
   20.31  
   20.32  (* makes the new type definitions and proves non-emptyness *)
   20.33 -fun typedef_make (vs, qty_name, mx, rel, rty) equiv_thm lthy =
   20.34 +fun typedef_make overloaded (vs, qty_name, mx, rel, rty) equiv_thm lthy =
   20.35    let
   20.36      fun typedef_tac ctxt =
   20.37        EVERY1 (map (resolve_tac ctxt o single) [@{thm part_equivp_typedef}, equiv_thm])
   20.38    in
   20.39 -    Typedef.add_typedef (qty_name, map (rpair dummyS) vs, mx)
   20.40 +    Typedef.add_typedef overloaded (qty_name, map (rpair dummyS) vs, mx)
   20.41        (typedef_term rel rty lthy) NONE typedef_tac lthy
   20.42    end
   20.43  
   20.44 @@ -152,7 +155,8 @@
   20.45    end
   20.46  
   20.47  (* main function for constructing a quotient type *)
   20.48 -fun add_quotient_type (((vs, qty_name, mx), (rty, rel, partial), (opt_morphs, opt_par_thm)), equiv_thm) lthy =
   20.49 +fun add_quotient_type overloaded
   20.50 +    (((vs, qty_name, mx), (rty, rel, partial), (opt_morphs, opt_par_thm)), equiv_thm) lthy =
   20.51    let
   20.52      val part_equiv =
   20.53        if partial
   20.54 @@ -161,7 +165,7 @@
   20.55  
   20.56      (* generates the typedef *)
   20.57      val ((_, typedef_info), lthy1) =
   20.58 -      typedef_make (vs, qty_name, mx, rel, rty) part_equiv lthy
   20.59 +      typedef_make overloaded (vs, qty_name, mx, rel, rty) part_equiv lthy
   20.60  
   20.61      (* abs and rep functions from the typedef *)
   20.62      val Abs_ty = #abs_type (#1 typedef_info)
   20.63 @@ -290,7 +294,7 @@
   20.64   relations are equivalence relations
   20.65  *)
   20.66  
   20.67 -fun quotient_type quot lthy =
   20.68 +fun quotient_type overloaded quot lthy =
   20.69    let
   20.70      (* sanity check *)
   20.71      val _ = sanity_check quot
   20.72 @@ -307,12 +311,12 @@
   20.73  
   20.74      val goal = (mk_goal o #2) quot
   20.75  
   20.76 -    fun after_qed [[thm]] = (snd oo add_quotient_type) (quot, thm)
   20.77 +    fun after_qed [[thm]] = (snd oo add_quotient_type overloaded) (quot, thm)
   20.78    in
   20.79      Proof.theorem NONE after_qed [[(goal, [])]] lthy
   20.80    end
   20.81  
   20.82 -fun quotient_type_cmd spec lthy =
   20.83 +fun quotient_type_cmd overloaded spec lthy =
   20.84    let
   20.85      fun parse_spec ((((((vs, qty_name), mx), rty_str), (partial, rel_str)), opt_morphs), opt_par_xthm) lthy =
   20.86        let
   20.87 @@ -330,7 +334,7 @@
   20.88  
   20.89      val (spec', _) = parse_spec spec lthy
   20.90    in
   20.91 -    quotient_type spec' lthy
   20.92 +    quotient_type overloaded spec' lthy
   20.93    end
   20.94  
   20.95  
   20.96 @@ -340,11 +344,11 @@
   20.97    Outer_Syntax.local_theory_to_proof @{command_keyword quotient_type}
   20.98      "quotient type definitions (require equivalence proofs)"
   20.99        (* FIXME Parse.type_args_constrained and standard treatment of sort constraints *)
  20.100 -      (Parse.type_args -- Parse.binding --
  20.101 +      (Parse_Spec.overloaded -- (Parse.type_args -- Parse.binding --
  20.102          Parse.opt_mixfix -- (@{keyword "="} |-- Parse.typ) -- (@{keyword "/"} |--
  20.103            Scan.optional (Parse.reserved "partial" -- @{keyword ":"} >> K true) false -- Parse.term) --
  20.104          Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding)) --
  20.105 -        Scan.option (@{keyword "parametric"} |-- Parse.!!! Parse.xthm)
  20.106 -      >> quotient_type_cmd)
  20.107 +        Scan.option (@{keyword "parametric"} |-- Parse.!!! Parse.xthm))
  20.108 +      >> (fn (overloaded, spec) => quotient_type_cmd {overloaded = overloaded} spec))
  20.109  
  20.110  end
    21.1 --- a/src/HOL/Tools/record.ML	Wed Sep 23 09:50:38 2015 +0200
    21.2 +++ b/src/HOL/Tools/record.ML	Thu Sep 24 13:33:42 2015 +0200
    21.3 @@ -26,8 +26,8 @@
    21.4    val get_info: theory -> string -> info option
    21.5    val the_info: theory -> string -> info
    21.6    val get_hierarchy: theory -> (string * typ list) -> (string * ((string * sort) * typ) list) list
    21.7 -  val add_record: (string * sort) list * binding -> (typ list * string) option ->
    21.8 -    (binding * typ * mixfix) list -> theory -> theory
    21.9 +  val add_record: {overloaded: bool} -> (string * sort) list * binding ->
   21.10 +    (typ list * string) option -> (binding * typ * mixfix) list -> theory -> theory
   21.11  
   21.12    val last_extT: typ -> (string * typ list) option
   21.13    val dest_recTs: typ -> (string * typ list) list
   21.14 @@ -55,7 +55,7 @@
   21.15  
   21.16  signature ISO_TUPLE_SUPPORT =
   21.17  sig
   21.18 -  val add_iso_tuple_type: binding * (string * sort) list ->
   21.19 +  val add_iso_tuple_type: {overloaded: bool} -> binding * (string * sort) list ->
   21.20      typ * typ -> theory -> (term * term) * theory
   21.21    val mk_cons_tuple: term * term -> term
   21.22    val dest_cons_tuple: term -> term * term
   21.23 @@ -93,13 +93,13 @@
   21.24      |> pair (tyco, ((Rep_inject, proj_constr), Const (Abs_name, rep_type --> absT), absT))
   21.25    end
   21.26  
   21.27 -fun do_typedef raw_tyco repT raw_vs thy =
   21.28 +fun do_typedef overloaded raw_tyco repT raw_vs thy =
   21.29    let
   21.30      val ctxt = Proof_Context.init_global thy |> Variable.declare_typ repT;
   21.31      val vs = map (Proof_Context.check_tfree ctxt) raw_vs;
   21.32    in
   21.33      thy
   21.34 -    |> Typedef.add_typedef_global (raw_tyco, vs, NoSyn)
   21.35 +    |> Typedef.add_typedef_global overloaded (raw_tyco, vs, NoSyn)
   21.36          (HOLogic.mk_UNIV repT) NONE (fn ctxt' => resolve_tac ctxt' [UNIV_witness] 1)
   21.37      |-> (fn (tyco, info) => get_typedef_info tyco vs info)
   21.38    end;
   21.39 @@ -117,13 +117,13 @@
   21.40  fun dest_cons_tuple (Const (@{const_name Record.iso_tuple_cons}, _) $ Const _ $ t $ u) = (t, u)
   21.41    | dest_cons_tuple t = raise TERM ("dest_cons_tuple", [t]);
   21.42  
   21.43 -fun add_iso_tuple_type (b, alphas) (leftT, rightT) thy =
   21.44 +fun add_iso_tuple_type overloaded (b, alphas) (leftT, rightT) thy =
   21.45    let
   21.46      val repT = HOLogic.mk_prodT (leftT, rightT);
   21.47  
   21.48      val ((_, ((rep_inject, abs_inverse), absC, absT)), typ_thy) =
   21.49        thy
   21.50 -      |> do_typedef b repT alphas
   21.51 +      |> do_typedef overloaded b repT alphas
   21.52        ||> Sign.add_path (Binding.name_of b); (*FIXME proper prefixing instead*)
   21.53      val typ_ctxt = Proof_Context.init_global typ_thy;
   21.54  
   21.55 @@ -1499,7 +1499,7 @@
   21.56    in compose_tac ctxt (false, rule'', Thm.nprems_of rule) i end);
   21.57  
   21.58  
   21.59 -fun extension_definition name fields alphas zeta moreT more vars thy =
   21.60 +fun extension_definition overloaded name fields alphas zeta moreT more vars thy =
   21.61    let
   21.62      val ctxt = Proof_Context.init_global thy;
   21.63  
   21.64 @@ -1525,7 +1525,7 @@
   21.65        let
   21.66          val suff = if i = 0 then ext_typeN else inner_typeN ^ string_of_int i;
   21.67          val ((_, cons), thy') = thy
   21.68 -          |> Iso_Tuple_Support.add_iso_tuple_type
   21.69 +          |> Iso_Tuple_Support.add_iso_tuple_type overloaded
   21.70              (Binding.suffix_name suff (Binding.name base_name), alphas_zeta)
   21.71                (fastype_of left, fastype_of right);
   21.72        in
   21.73 @@ -1808,7 +1808,7 @@
   21.74  
   21.75  (* definition *)
   21.76  
   21.77 -fun definition (alphas, binding) parent (parents: parent_info list) raw_fields thy0 =
   21.78 +fun definition overloaded (alphas, binding) parent (parents: parent_info list) raw_fields thy0 =
   21.79    let
   21.80      val ctxt0 = Proof_Context.init_global thy0;
   21.81  
   21.82 @@ -1867,7 +1867,7 @@
   21.83          extT, ext_induct, ext_inject, ext_surjective, ext_split, ext_def), ext_thy) =
   21.84        thy0
   21.85        |> Sign.qualified_path false binding
   21.86 -      |> extension_definition extension_name fields alphas_ext zeta moreT more vars;
   21.87 +      |> extension_definition overloaded extension_name fields alphas_ext zeta moreT more vars;
   21.88      val ext_ctxt = Proof_Context.init_global ext_thy;
   21.89  
   21.90      val _ = timing_msg ext_ctxt "record preparing definitions";
   21.91 @@ -2277,7 +2277,7 @@
   21.92  
   21.93  in
   21.94  
   21.95 -fun add_record (params, binding) raw_parent raw_fields thy =
   21.96 +fun add_record overloaded (params, binding) raw_parent raw_fields thy =
   21.97    let
   21.98      val ctxt = Proof_Context.init_global thy;
   21.99      fun cert_typ T = Type.no_tvars (Proof_Context.cert_typ ctxt T)
  21.100 @@ -2327,11 +2327,11 @@
  21.101        err_dup_record @ err_extra_frees @ err_no_fields @ err_dup_fields @ err_bad_fields;
  21.102      val _ = if null errs then () else error (cat_lines errs);
  21.103    in
  21.104 -    thy |> definition (params, binding) parent parents bfields
  21.105 +    thy |> definition overloaded (params, binding) parent parents bfields
  21.106    end
  21.107    handle ERROR msg => cat_error msg ("Failed to define record " ^ Binding.print binding);
  21.108  
  21.109 -fun add_record_cmd (raw_params, binding) raw_parent raw_fields thy =
  21.110 +fun add_record_cmd overloaded (raw_params, binding) raw_parent raw_fields thy =
  21.111    let
  21.112      val ctxt = Proof_Context.init_global thy;
  21.113      val params = map (apsnd (Typedecl.read_constraint ctxt)) raw_params;
  21.114 @@ -2339,7 +2339,7 @@
  21.115      val (parent, ctxt2) = read_parent raw_parent ctxt1;
  21.116      val (fields, ctxt3) = read_fields raw_fields ctxt2;
  21.117      val params' = map (Proof_Context.check_tfree ctxt3) params;
  21.118 -  in thy |> add_record (params', binding) parent fields end;
  21.119 +  in thy |> add_record overloaded (params', binding) parent fields end;
  21.120  
  21.121  end;
  21.122  
  21.123 @@ -2348,9 +2348,10 @@
  21.124  
  21.125  val _ =
  21.126    Outer_Syntax.command @{command_keyword record} "define extensible record"
  21.127 -    (Parse.type_args_constrained -- Parse.binding --
  21.128 +    (Parse_Spec.overloaded -- (Parse.type_args_constrained -- Parse.binding) --
  21.129        (@{keyword "="} |-- Scan.option (Parse.typ --| @{keyword "+"}) --
  21.130          Scan.repeat1 Parse.const_binding)
  21.131 -    >> (fn (x, (y, z)) => Toplevel.theory (add_record_cmd x y z)));
  21.132 +    >> (fn ((overloaded, x), (y, z)) =>
  21.133 +        Toplevel.theory (add_record_cmd {overloaded = overloaded} x y z)));
  21.134  
  21.135  end;
    22.1 --- a/src/HOL/Tools/typedef.ML	Wed Sep 23 09:50:38 2015 +0200
    22.2 +++ b/src/HOL/Tools/typedef.ML	Thu Sep 24 13:33:42 2015 +0200
    22.3 @@ -20,16 +20,17 @@
    22.4    val default_bindings: binding -> bindings
    22.5    val make_bindings: binding -> bindings option -> bindings
    22.6    val make_morphisms: binding -> (binding * binding) option -> bindings
    22.7 -  val add_typedef: binding * (string * sort) list * mixfix ->
    22.8 +  val overloaded: bool Config.T
    22.9 +  val add_typedef: {overloaded: bool} -> binding * (string * sort) list * mixfix ->
   22.10      term -> bindings option -> (Proof.context -> tactic) -> local_theory ->
   22.11      (string * info) * local_theory
   22.12 -  val add_typedef_global: binding * (string * sort) list * mixfix ->
   22.13 +  val add_typedef_global: {overloaded: bool} -> binding * (string * sort) list * mixfix ->
   22.14      term -> bindings option -> (Proof.context -> tactic) -> theory ->
   22.15      (string * info) * theory
   22.16 -  val typedef: binding * (string * sort) list * mixfix -> term -> bindings option ->
   22.17 -    local_theory -> Proof.state
   22.18 -  val typedef_cmd: binding * (string * string option) list * mixfix -> string -> bindings option ->
   22.19 -    local_theory -> Proof.state
   22.20 +  val typedef: {overloaded: bool} -> binding * (string * sort) list * mixfix ->
   22.21 +    term -> bindings option -> local_theory -> Proof.state
   22.22 +  val typedef_cmd: {overloaded: bool} -> binding * (string * string option) list * mixfix ->
   22.23 +    string -> bindings option -> local_theory -> Proof.state
   22.24  end;
   22.25  
   22.26  structure Typedef: TYPEDEF =
   22.27 @@ -98,6 +99,8 @@
   22.28  
   22.29  (* primitive typedef axiomatization -- for fresh typedecl *)
   22.30  
   22.31 +val typedef_overloaded = Attrib.setup_config_bool @{binding typedef_overloaded} (K false);
   22.32 +
   22.33  fun mk_inhabited A =
   22.34    let val T = HOLogic.dest_setT (Term.fastype_of A)
   22.35    in HOLogic.mk_Trueprop (HOLogic.exists_const T $ Abs ("x", T, HOLogic.mk_mem (Bound 0, A))) end;
   22.36 @@ -109,7 +112,7 @@
   22.37          (newT --> oldT) --> (oldT --> newT) --> HOLogic.mk_setT oldT --> HOLogic.boolT);
   22.38    in Logic.mk_implies (mk_inhabited A, HOLogic.mk_Trueprop (typedefC $ RepC $ AbsC $ A)) end;
   22.39  
   22.40 -fun primitive_typedef type_definition_name newT oldT Rep_name Abs_name A lthy =
   22.41 +fun primitive_typedef {overloaded} type_definition_name newT oldT Rep_name Abs_name A lthy =
   22.42    let
   22.43      (* errors *)
   22.44  
   22.45 @@ -118,11 +121,13 @@
   22.46      val lhs_tfrees = Term.add_tfreesT newT [];
   22.47      val rhs_tfrees = Term.add_tfreesT oldT [];
   22.48      val _ =
   22.49 -      (case fold (remove (op =)) lhs_tfrees rhs_tfrees of [] => ()
   22.50 +      (case fold (remove (op =)) lhs_tfrees rhs_tfrees of
   22.51 +        [] => ()
   22.52        | extras => error ("Extra type variables in representing set: " ^ show_names extras));
   22.53  
   22.54      val _ =
   22.55 -      (case Term.add_frees A [] of [] => []
   22.56 +      (case Term.add_frees A [] of [] =>
   22.57 +        []
   22.58        | xs => error ("Illegal variables in representing set: " ^ show_names xs));
   22.59  
   22.60  
   22.61 @@ -148,6 +153,20 @@
   22.62            Theory.add_deps consts_lthy "" (const_dep (dest_Const RepC)) [newT_dep] ##>
   22.63            Theory.add_deps consts_lthy "" (const_dep (dest_Const AbsC)) [newT_dep]);
   22.64  
   22.65 +    val axiom_defs = Theory.defs_of (Proof_Context.theory_of axiom_lthy);
   22.66 +    val newT_deps = maps #2 (Defs.get_deps axiom_defs (#1 newT_dep));
   22.67 +    val _ =
   22.68 +      if null newT_deps orelse overloaded orelse Config.get lthy typedef_overloaded then ()
   22.69 +      else
   22.70 +        error (Pretty.string_of (Pretty.chunks
   22.71 +          [Pretty.paragraph
   22.72 +            (Pretty.text "Type definition with open dependencies, use" @
   22.73 +             [Pretty.brk 1, Pretty.str "\"", Pretty.keyword1 "typedef", Pretty.brk 1,
   22.74 +              Pretty.str "(", Pretty.keyword2 "overloaded", Pretty.str ")\"", Pretty.brk 1] @
   22.75 +             Pretty.text "or enable configuration option \"typedef_overloaded\" in the context."),
   22.76 +           Pretty.block [Pretty.str "  Type:", Pretty.brk 2, Syntax.pretty_typ axiom_lthy newT],
   22.77 +           Pretty.block (Pretty.str "  Deps:" :: Pretty.brk 2 ::
   22.78 +             Pretty.commas (map (Defs.pretty_entry axiom_lthy) newT_deps))]))
   22.79    in ((RepC, AbsC, axiom_name, axiom), axiom_lthy) end;
   22.80  
   22.81  
   22.82 @@ -171,7 +190,7 @@
   22.83  
   22.84  (* prepare_typedef *)
   22.85  
   22.86 -fun prepare_typedef prep_term (name, raw_args, mx) raw_set opt_bindings lthy =
   22.87 +fun prepare_typedef prep_term overloaded (name, raw_args, mx) raw_set opt_bindings lthy =
   22.88    let
   22.89      val bname = Binding.name_of name;
   22.90  
   22.91 @@ -205,7 +224,7 @@
   22.92      val {Rep_name, Abs_name, type_definition_name} = make_bindings name opt_bindings;
   22.93  
   22.94      val ((RepC, AbsC, axiom_name, typedef), typedef_lthy) = typedecl_lthy
   22.95 -      |> primitive_typedef type_definition_name newT oldT Rep_name Abs_name set;
   22.96 +      |> primitive_typedef overloaded type_definition_name newT oldT Rep_name Abs_name set;
   22.97  
   22.98      val alias_lthy = typedef_lthy
   22.99        |> Local_Theory.const_alias Rep_name (#1 (Term.dest_Const RepC))
  22.100 @@ -269,18 +288,18 @@
  22.101  
  22.102  (* add_typedef: tactic interface *)
  22.103  
  22.104 -fun add_typedef typ set opt_bindings tac lthy =
  22.105 +fun add_typedef overloaded typ set opt_bindings tac lthy =
  22.106    let
  22.107      val ((goal, _, typedef_result), lthy') =
  22.108 -      prepare_typedef Syntax.check_term typ set opt_bindings lthy;
  22.109 +      prepare_typedef Syntax.check_term overloaded typ set opt_bindings lthy;
  22.110      val inhabited =
  22.111        Goal.prove lthy' [] [] goal (tac o #context)
  22.112        |> Goal.norm_result lthy' |> Thm.close_derivation;
  22.113    in typedef_result inhabited lthy' end;
  22.114  
  22.115 -fun add_typedef_global typ set opt_bindings tac =
  22.116 +fun add_typedef_global overloaded typ set opt_bindings tac =
  22.117    Named_Target.theory_init
  22.118 -  #> add_typedef typ set opt_bindings tac
  22.119 +  #> add_typedef overloaded typ set opt_bindings tac
  22.120    #> Local_Theory.exit_result_global (apsnd o transform_info);
  22.121  
  22.122  
  22.123 @@ -288,11 +307,11 @@
  22.124  
  22.125  local
  22.126  
  22.127 -fun gen_typedef prep_term prep_constraint (b, raw_args, mx) set opt_bindings lthy =
  22.128 +fun gen_typedef prep_term prep_constraint overloaded (b, raw_args, mx) set opt_bindings lthy =
  22.129    let
  22.130      val args = map (apsnd (prep_constraint lthy)) raw_args;
  22.131      val ((goal, goal_pat, typedef_result), lthy') =
  22.132 -      prepare_typedef prep_term (b, args, mx) set opt_bindings lthy;
  22.133 +      prepare_typedef prep_term overloaded (b, args, mx) set opt_bindings lthy;
  22.134      fun after_qed [[th]] = snd o typedef_result th;
  22.135    in Proof.theorem NONE after_qed [[(goal, [goal_pat])]] lthy' end;
  22.136  
  22.137 @@ -310,10 +329,14 @@
  22.138  val _ =
  22.139    Outer_Syntax.local_theory_to_proof @{command_keyword typedef}
  22.140      "HOL type definition (requires non-emptiness proof)"
  22.141 -    (Parse.type_args_constrained -- Parse.binding -- Parse.opt_mixfix --
  22.142 +    (Parse_Spec.overloaded -- Parse.type_args_constrained -- Parse.binding -- Parse.opt_mixfix --
  22.143        (@{keyword "="} |-- Parse.term) --
  22.144        Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding))
  22.145 -    >> (fn ((((vs, t), mx), A), opt_morphs) => fn lthy =>
  22.146 -        typedef_cmd (t, vs, mx) A (SOME (make_morphisms t opt_morphs)) lthy));
  22.147 +    >> (fn (((((overloaded, vs), t), mx), A), opt_morphs) => fn lthy =>
  22.148 +        typedef_cmd {overloaded = overloaded} (t, vs, mx) A
  22.149 +          (SOME (make_morphisms t opt_morphs)) lthy));
  22.150 +
  22.151 +
  22.152 +val overloaded = typedef_overloaded;
  22.153  
  22.154  end;
    23.1 --- a/src/HOL/Word/Word.thy	Wed Sep 23 09:50:38 2015 +0200
    23.2 +++ b/src/HOL/Word/Word.thy	Thu Sep 24 13:33:42 2015 +0200
    23.3 @@ -18,7 +18,7 @@
    23.4  
    23.5  subsection {* Type definition *}
    23.6  
    23.7 -typedef 'a word = "{(0::int) ..< 2 ^ len_of TYPE('a::len0)}"
    23.8 +typedef (overloaded) 'a word = "{(0::int) ..< 2 ^ len_of TYPE('a::len0)}"
    23.9    morphisms uint Abs_word by auto
   23.10  
   23.11  lemma uint_nonnegative:
    24.1 --- a/src/HOL/ex/PER.thy	Wed Sep 23 09:50:38 2015 +0200
    24.2 +++ b/src/HOL/ex/PER.thy	Thu Sep 24 13:33:42 2015 +0200
    24.3 @@ -154,7 +154,7 @@
    24.4  
    24.5  definition "quot = {{x. a \<sim> x}| a::'a::partial_equiv. True}"
    24.6  
    24.7 -typedef 'a quot = "quot :: 'a::partial_equiv set set"
    24.8 +typedef (overloaded) 'a quot = "quot :: 'a::partial_equiv set set"
    24.9    unfolding quot_def by blast
   24.10  
   24.11  lemma quotI [intro]: "{x. a \<sim> x} \<in> quot"
    25.1 --- a/src/Pure/Isar/parse_spec.ML	Wed Sep 23 09:50:38 2015 +0200
    25.2 +++ b/src/Pure/Isar/parse_spec.ML	Thu Sep 24 13:33:42 2015 +0200
    25.3 @@ -29,6 +29,7 @@
    25.4    val obtains: Element.obtains parser
    25.5    val general_statement: (Element.context list * Element.statement) parser
    25.6    val statement_keyword: string parser
    25.7 +  val overloaded: bool parser
    25.8  end;
    25.9  
   25.10  structure Parse_Spec: PARSE_SPEC =
   25.11 @@ -155,4 +156,10 @@
   25.12  
   25.13  val statement_keyword = Parse.$$$ "obtains" || Parse.$$$ "shows";
   25.14  
   25.15 +
   25.16 +(* options *)
   25.17 +
   25.18 +val overloaded =
   25.19 +  Scan.optional (Parse.$$$ "(" -- Parse.$$$ "overloaded" -- Parse.$$$ ")" >> K true) false;
   25.20 +
   25.21  end;
    26.1 --- a/src/Pure/defs.ML	Wed Sep 23 09:50:38 2015 +0200
    26.2 +++ b/src/Pure/defs.ML	Thu Sep 24 13:33:42 2015 +0200
    26.3 @@ -12,6 +12,7 @@
    26.4    val item_ord: item * item -> order
    26.5    type entry = item * typ list
    26.6    val pretty_args: Proof.context -> typ list -> Pretty.T list
    26.7 +  val pretty_entry: Proof.context -> entry -> Pretty.T
    26.8    val plain_args: typ list -> bool
    26.9    type T
   26.10    type spec =
   26.11 @@ -28,6 +29,7 @@
   26.12    val empty: T
   26.13    val merge: Proof.context -> T * T -> T
   26.14    val define: Proof.context -> bool -> string option -> string -> entry -> entry list -> T -> T
   26.15 +  val get_deps: T -> item -> (typ list * entry list) list
   26.16  end;
   26.17  
   26.18  structure Defs: DEFS =
   26.19 @@ -241,4 +243,6 @@
   26.20      val defs' = defs |> update_specs c spec;
   26.21    in Defs (defs' |> (if unchecked then I else dependencies ctxt (c, args) restr deps)) end;
   26.22  
   26.23 +fun get_deps (Defs defs) c = reducts_of defs c;
   26.24 +
   26.25  end;