--- a/src/Doc/Isar_Ref/HOL_Specific.thy Wed Sep 23 09:50:38 2015 +0200
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy Thu Sep 24 13:33:42 2015 +0200
@@ -932,7 +932,7 @@
\end{matharray}
@{rail \<open>
- @@{command (HOL) record} @{syntax typespec_sorts} '=' \<newline>
+ @@{command (HOL) record} @{syntax "overloaded"}? @{syntax typespec_sorts} '=' \<newline>
(@{syntax type} '+')? (constdecl +)
;
constdecl: @{syntax name} '::' @{syntax type} @{syntax mixfix}?
@@ -1131,7 +1131,9 @@
definition, but less powerful in practice.
@{rail \<open>
- @@{command (HOL) typedef} abs_type '=' rep_set
+ @@{command (HOL) typedef} @{syntax "overloaded"}? abs_type '=' rep_set
+ ;
+ @{syntax_def "overloaded"}: ('(' @'overloaded' ')')
;
abs_type: @{syntax typespec_sorts} @{syntax mixfix}?
;
@@ -1185,6 +1187,13 @@
for the generic @{method cases} and @{method induct} methods,
respectively.
+ \medskip The ``@{text "(overloaded)"}'' option allows the @{command
+ "typedef"} specification to depend on constants that are not (yet)
+ specified and thus left open as parameters. In particular, a @{command
+ typedef} depending on type-class parameters (cf.\ \secref{sec:class}) is
+ semantically like a dependent type: its meaning is determined for
+ different type-class instances according to their respective operations.
+
\end{description}
\<close>
@@ -1299,8 +1308,9 @@
\end{matharray}
@{rail \<open>
- @@{command (HOL) quotient_type} @{syntax typespec} @{syntax mixfix}? '='
- quot_type \<newline> quot_morphisms? quot_parametric?
+ @@{command (HOL) quotient_type} @{syntax "overloaded"}? \<newline>
+ @{syntax typespec} @{syntax mixfix}? '=' quot_type \<newline>
+ quot_morphisms? quot_parametric?
;
quot_type: @{syntax type} '/' ('partial' ':')? @{syntax term}
;
--- a/src/HOL/Datatype_Examples/Misc_N2M.thy Wed Sep 23 09:50:38 2015 +0200
+++ b/src/HOL/Datatype_Examples/Misc_N2M.thy Thu Sep 24 13:33:42 2015 +0200
@@ -11,6 +11,9 @@
imports "~~/src/HOL/Library/BNF_Axiomatization"
begin
+declare [[typedef_overloaded]]
+
+
locale misc
begin
--- a/src/HOL/Datatype_Examples/Stream_Processor.thy Wed Sep 23 09:50:38 2015 +0200
+++ b/src/HOL/Datatype_Examples/Stream_Processor.thy Thu Sep 24 13:33:42 2015 +0200
@@ -12,6 +12,9 @@
imports "~~/src/HOL/Library/Stream" "~~/src/HOL/Library/BNF_Axiomatization"
begin
+declare [[typedef_overloaded]]
+
+
section {* Continuous Functions on Streams *}
datatype ('a, 'b, 'c) sp\<^sub>\<mu> = Get "'a \<Rightarrow> ('a, 'b, 'c) sp\<^sub>\<mu>" | Put "'b" "'c"
--- a/src/HOL/HOLCF/Porder.thy Wed Sep 23 09:50:38 2015 +0200
+++ b/src/HOL/HOLCF/Porder.thy Thu Sep 24 13:33:42 2015 +0200
@@ -8,6 +8,9 @@
imports Main
begin
+declare [[typedef_overloaded]]
+
+
subsection {* Type class for partial orders *}
class below =
--- a/src/HOL/HOLCF/Tools/cpodef.ML Wed Sep 23 09:50:38 2015 +0200
+++ b/src/HOL/HOLCF/Tools/cpodef.ML Thu Sep 24 13:33:42 2015 +0200
@@ -165,7 +165,7 @@
let
val name = #1 typ
val ((full_tname, info as ({Rep_name, ...}, {type_definition, ...})), thy) = thy
- |> Typedef.add_typedef_global typ set opt_bindings tac
+ |> Typedef.add_typedef_global {overloaded = false} typ set opt_bindings tac
val oldT = #rep_type (#1 info)
val newT = #abs_type (#1 info)
val lhs_tfrees = map dest_TFree (snd (dest_Type newT))
--- a/src/HOL/IMP/Abs_State.thy Wed Sep 23 09:50:38 2015 +0200
+++ b/src/HOL/IMP/Abs_State.thy Thu Sep 24 13:33:42 2015 +0200
@@ -19,7 +19,7 @@
hide_type st --"hide previous def to avoid long names"
-quotient_type 'a st = "('a::top) st_rep" / eq_st
+quotient_type (overloaded) 'a st = "('a::top) st_rep" / eq_st
morphisms rep_st St
by (metis eq_st_def equivpI reflpI sympI transpI)
--- a/src/HOL/Import/import_rule.ML Wed Sep 23 09:50:38 2015 +0200
+++ b/src/HOL/Import/import_rule.ML Thu Sep 24 13:33:42 2015 +0200
@@ -222,7 +222,8 @@
Typedef.make_morphisms (Binding.name tycname)
(SOME (Binding.name rep_name, Binding.name abs_name))
val ((_, typedef_info), thy') =
- Typedef.add_typedef_global (Binding.name tycname, map (rpair dummyS) tnames, NoSyn) c
+ Typedef.add_typedef_global {overloaded = false}
+ (Binding.name tycname, map (rpair dummyS) tnames, NoSyn) c
(SOME typedef_bindings) (fn ctxt => resolve_tac ctxt [th2] 1) thy
val aty = #abs_type (#1 typedef_info)
val th = freezeT thy' (#type_definition (#2 typedef_info))
--- a/src/HOL/Library/Fraction_Field.thy Wed Sep 23 09:50:38 2015 +0200
+++ b/src/HOL/Library/Fraction_Field.thy Thu Sep 24 13:33:42 2015 +0200
@@ -47,7 +47,7 @@
end
-quotient_type 'a fract = "'a :: idom \<times> 'a" / partial: "fractrel"
+quotient_type (overloaded) 'a fract = "'a :: idom \<times> 'a" / partial: "fractrel"
by(rule part_equivp_fractrel)
subsubsection \<open>Representation and basic operations\<close>
--- a/src/HOL/Library/Polynomial.thy Wed Sep 23 09:50:38 2015 +0200
+++ b/src/HOL/Library/Polynomial.thy Thu Sep 24 13:33:42 2015 +0200
@@ -52,7 +52,7 @@
subsection \<open>Definition of type @{text poly}\<close>
-typedef 'a poly = "{f :: nat \<Rightarrow> 'a::zero. \<forall>\<^sub>\<infinity> n. f n = 0}"
+typedef (overloaded) 'a poly = "{f :: nat \<Rightarrow> 'a::zero. \<forall>\<^sub>\<infinity> n. f n = 0}"
morphisms coeff Abs_poly by (auto intro!: ALL_MOST)
setup_lifting type_definition_poly
--- a/src/HOL/Library/Quotient_Type.thy Wed Sep 23 09:50:38 2015 +0200
+++ b/src/HOL/Library/Quotient_Type.thy Thu Sep 24 13:33:42 2015 +0200
@@ -62,7 +62,7 @@
definition (in eqv) "quot = {{x. a \<sim> x} | a. True}"
-typedef 'a quot = "quot :: 'a::eqv set set"
+typedef (overloaded) 'a quot = "quot :: 'a::eqv set set"
unfolding quot_def by blast
lemma quotI [intro]: "{x. a \<sim> x} \<in> quot"
--- a/src/HOL/Library/RBT.thy Wed Sep 23 09:50:38 2015 +0200
+++ b/src/HOL/Library/RBT.thy Thu Sep 24 13:33:42 2015 +0200
@@ -10,7 +10,7 @@
subsection \<open>Type definition\<close>
-typedef ('a, 'b) rbt = "{t :: ('a::linorder, 'b) RBT_Impl.rbt. is_rbt t}"
+typedef (overloaded) ('a, 'b) rbt = "{t :: ('a::linorder, 'b) RBT_Impl.rbt. is_rbt t}"
morphisms impl_of RBT
proof -
have "RBT_Impl.Empty \<in> ?rbt" by simp
--- a/src/HOL/Library/Saturated.thy Wed Sep 23 09:50:38 2015 +0200
+++ b/src/HOL/Library/Saturated.thy Thu Sep 24 13:33:42 2015 +0200
@@ -12,7 +12,7 @@
subsection \<open>The type of saturated naturals\<close>
-typedef ('a::len) sat = "{.. len_of TYPE('a)}"
+typedef (overloaded) ('a::len) sat = "{.. len_of TYPE('a)}"
morphisms nat_of Abs_sat
by auto
--- a/src/HOL/Matrix_LP/Matrix.thy Wed Sep 23 09:50:38 2015 +0200
+++ b/src/HOL/Matrix_LP/Matrix.thy Thu Sep 24 13:33:42 2015 +0200
@@ -13,7 +13,7 @@
definition "matrix = {(f::(nat \<Rightarrow> nat \<Rightarrow> 'a::zero)). finite (nonzero_positions f)}"
-typedef 'a matrix = "matrix :: (nat \<Rightarrow> nat \<Rightarrow> 'a::zero) set"
+typedef (overloaded) 'a matrix = "matrix :: (nat \<Rightarrow> nat \<Rightarrow> 'a::zero) set"
unfolding matrix_def
proof
show "(\<lambda>j i. 0) \<in> {(f::(nat \<Rightarrow> nat \<Rightarrow> 'a::zero)). finite (nonzero_positions f)}"
--- a/src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy Wed Sep 23 09:50:38 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy Thu Sep 24 13:33:42 2015 +0200
@@ -9,7 +9,8 @@
definition bcontfun :: "('a::topological_space \<Rightarrow> 'b::metric_space) set"
where "bcontfun = {f. continuous_on UNIV f \<and> bounded (range f)}"
-typedef ('a, 'b) bcontfun = "bcontfun :: ('a::topological_space \<Rightarrow> 'b::metric_space) set"
+typedef (overloaded) ('a, 'b) bcontfun =
+ "bcontfun :: ('a::topological_space \<Rightarrow> 'b::metric_space) set"
by (auto simp: bcontfun_def intro: continuous_intros simp: bounded_def)
lemma bcontfunE:
--- a/src/HOL/Nominal/Nominal.thy Wed Sep 23 09:50:38 2015 +0200
+++ b/src/HOL/Nominal/Nominal.thy Thu Sep 24 13:33:42 2015 +0200
@@ -6,6 +6,9 @@
"avoids"
begin
+declare [[typedef_overloaded]]
+
+
section {* Permutations *}
(*======================*)
@@ -3378,7 +3381,7 @@
definition "ABS = ABS_set"
-typedef ('x,'a) ABS ("\<guillemotleft>_\<guillemotright>_" [1000,1000] 1000) =
+typedef ('x, 'a) ABS ("\<guillemotleft>_\<guillemotright>_" [1000,1000] 1000) =
"ABS::('x\<Rightarrow>('a noption)) set"
morphisms Rep_ABS Abs_ABS
unfolding ABS_def
--- a/src/HOL/Nominal/nominal_datatype.ML Wed Sep 23 09:50:38 2015 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Thu Sep 24 13:33:42 2015 +0200
@@ -586,7 +586,7 @@
val (typedefs, thy6) =
thy4
|> fold_map (fn (((name, mx), tvs), (cname, U)) => fn thy =>
- Typedef.add_typedef_global
+ Typedef.add_typedef_global {overloaded = false}
(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
--- a/src/HOL/SPARK/Tools/spark_vcs.ML Wed Sep 23 09:50:38 2015 +0200
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML Thu Sep 24 13:33:42 2015 +0200
@@ -359,7 +359,7 @@
map (rpair (mk_type thy prfx ty)) flds) fldtys
in case get_type thy prfx s of
NONE =>
- Record.add_record ([], Binding.name s) NONE
+ Record.add_record {overloaded = false} ([], Binding.name s) NONE
(map (fn (fld, T) => (Binding.name fld, T, NoSyn)) fldTs) thy
| SOME (rT, cmap) =>
(case get_record_info thy rT of
--- a/src/HOL/Tools/BNF/bnf_util.ML Wed Sep 23 09:50:38 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_util.ML Thu Sep 24 13:33:42 2015 +0200
@@ -156,7 +156,7 @@
val ((name, info), (lthy, lthy_old)) =
lthy
|> Local_Theory.open_target |> snd
- |> Typedef.add_typedef (b', Ts, mx) set (SOME bindings) tac
+ |> Typedef.add_typedef {overloaded = false} (b', Ts, mx) set (SOME bindings) tac
||> `Local_Theory.close_target;
val phi = Proof_Context.export_morphism lthy_old lthy;
in
--- a/src/HOL/Tools/Old_Datatype/old_datatype.ML Wed Sep 23 09:50:38 2015 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML Thu Sep 24 13:33:42 2015 +0200
@@ -186,7 +186,7 @@
|> Sign.parent_path
|> fold_map
(fn (((name, mx), tvs), c) =>
- Typedef.add_typedef_global (name, tvs, mx)
+ Typedef.add_typedef_global {overloaded = false} (name, tvs, mx)
(Collect $ Const (c, UnivT')) NONE
(fn ctxt =>
resolve_tac ctxt [exI] 1 THEN
--- a/src/HOL/Tools/Quotient/quotient_type.ML Wed Sep 23 09:50:38 2015 +0200
+++ b/src/HOL/Tools/Quotient/quotient_type.ML Thu Sep 24 13:33:42 2015 +0200
@@ -6,14 +6,17 @@
signature QUOTIENT_TYPE =
sig
- val add_quotient_type: ((string list * binding * mixfix) * (typ * term * bool) *
- ((binding * binding) option * thm option)) * thm -> local_theory -> Quotient_Info.quotients * local_theory
-
- val quotient_type: (string list * binding * mixfix) * (typ * term * bool) *
- ((binding * binding) option * thm option) -> Proof.context -> Proof.state
-
- val quotient_type_cmd: (((((string list * binding) * mixfix) * string) * (bool * string)) *
- (binding * binding) option) * (Facts.ref * Token.src list) option -> Proof.context -> Proof.state
+ val add_quotient_type: {overloaded: bool} ->
+ ((string list * binding * mixfix) * (typ * term * bool) *
+ ((binding * binding) option * thm option)) * thm -> local_theory ->
+ Quotient_Info.quotients * local_theory
+ val quotient_type: {overloaded: bool} ->
+ (string list * binding * mixfix) * (typ * term * bool) *
+ ((binding * binding) option * thm option) -> Proof.context -> Proof.state
+ val quotient_type_cmd: {overloaded: bool} ->
+ (((((string list * binding) * mixfix) * string) * (bool * string)) *
+ (binding * binding) option) * (Facts.ref * Token.src list) option ->
+ Proof.context -> Proof.state
end;
structure Quotient_Type: QUOTIENT_TYPE =
@@ -40,12 +43,12 @@
(* makes the new type definitions and proves non-emptyness *)
-fun typedef_make (vs, qty_name, mx, rel, rty) equiv_thm lthy =
+fun typedef_make overloaded (vs, qty_name, mx, rel, rty) equiv_thm lthy =
let
fun typedef_tac ctxt =
EVERY1 (map (resolve_tac ctxt o single) [@{thm part_equivp_typedef}, equiv_thm])
in
- Typedef.add_typedef (qty_name, map (rpair dummyS) vs, mx)
+ Typedef.add_typedef overloaded (qty_name, map (rpair dummyS) vs, mx)
(typedef_term rel rty lthy) NONE typedef_tac lthy
end
@@ -152,7 +155,8 @@
end
(* main function for constructing a quotient type *)
-fun add_quotient_type (((vs, qty_name, mx), (rty, rel, partial), (opt_morphs, opt_par_thm)), equiv_thm) lthy =
+fun add_quotient_type overloaded
+ (((vs, qty_name, mx), (rty, rel, partial), (opt_morphs, opt_par_thm)), equiv_thm) lthy =
let
val part_equiv =
if partial
@@ -161,7 +165,7 @@
(* generates the typedef *)
val ((_, typedef_info), lthy1) =
- typedef_make (vs, qty_name, mx, rel, rty) part_equiv lthy
+ typedef_make overloaded (vs, qty_name, mx, rel, rty) part_equiv lthy
(* abs and rep functions from the typedef *)
val Abs_ty = #abs_type (#1 typedef_info)
@@ -290,7 +294,7 @@
relations are equivalence relations
*)
-fun quotient_type quot lthy =
+fun quotient_type overloaded quot lthy =
let
(* sanity check *)
val _ = sanity_check quot
@@ -307,12 +311,12 @@
val goal = (mk_goal o #2) quot
- fun after_qed [[thm]] = (snd oo add_quotient_type) (quot, thm)
+ fun after_qed [[thm]] = (snd oo add_quotient_type overloaded) (quot, thm)
in
Proof.theorem NONE after_qed [[(goal, [])]] lthy
end
-fun quotient_type_cmd spec lthy =
+fun quotient_type_cmd overloaded spec lthy =
let
fun parse_spec ((((((vs, qty_name), mx), rty_str), (partial, rel_str)), opt_morphs), opt_par_xthm) lthy =
let
@@ -330,7 +334,7 @@
val (spec', _) = parse_spec spec lthy
in
- quotient_type spec' lthy
+ quotient_type overloaded spec' lthy
end
@@ -340,11 +344,11 @@
Outer_Syntax.local_theory_to_proof @{command_keyword quotient_type}
"quotient type definitions (require equivalence proofs)"
(* FIXME Parse.type_args_constrained and standard treatment of sort constraints *)
- (Parse.type_args -- Parse.binding --
+ (Parse_Spec.overloaded -- (Parse.type_args -- Parse.binding --
Parse.opt_mixfix -- (@{keyword "="} |-- Parse.typ) -- (@{keyword "/"} |--
Scan.optional (Parse.reserved "partial" -- @{keyword ":"} >> K true) false -- Parse.term) --
Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding)) --
- Scan.option (@{keyword "parametric"} |-- Parse.!!! Parse.xthm)
- >> quotient_type_cmd)
+ Scan.option (@{keyword "parametric"} |-- Parse.!!! Parse.xthm))
+ >> (fn (overloaded, spec) => quotient_type_cmd {overloaded = overloaded} spec))
end
--- a/src/HOL/Tools/record.ML Wed Sep 23 09:50:38 2015 +0200
+++ b/src/HOL/Tools/record.ML Thu Sep 24 13:33:42 2015 +0200
@@ -26,8 +26,8 @@
val get_info: theory -> string -> info option
val the_info: theory -> string -> info
val get_hierarchy: theory -> (string * typ list) -> (string * ((string * sort) * typ) list) list
- val add_record: (string * sort) list * binding -> (typ list * string) option ->
- (binding * typ * mixfix) list -> theory -> theory
+ val add_record: {overloaded: bool} -> (string * sort) list * binding ->
+ (typ list * string) option -> (binding * typ * mixfix) list -> theory -> theory
val last_extT: typ -> (string * typ list) option
val dest_recTs: typ -> (string * typ list) list
@@ -55,7 +55,7 @@
signature ISO_TUPLE_SUPPORT =
sig
- val add_iso_tuple_type: binding * (string * sort) list ->
+ val add_iso_tuple_type: {overloaded: bool} -> binding * (string * sort) list ->
typ * typ -> theory -> (term * term) * theory
val mk_cons_tuple: term * term -> term
val dest_cons_tuple: term -> term * term
@@ -93,13 +93,13 @@
|> pair (tyco, ((Rep_inject, proj_constr), Const (Abs_name, rep_type --> absT), absT))
end
-fun do_typedef raw_tyco repT raw_vs thy =
+fun do_typedef overloaded raw_tyco repT raw_vs thy =
let
val ctxt = Proof_Context.init_global thy |> Variable.declare_typ repT;
val vs = map (Proof_Context.check_tfree ctxt) raw_vs;
in
thy
- |> Typedef.add_typedef_global (raw_tyco, vs, NoSyn)
+ |> Typedef.add_typedef_global overloaded (raw_tyco, vs, NoSyn)
(HOLogic.mk_UNIV repT) NONE (fn ctxt' => resolve_tac ctxt' [UNIV_witness] 1)
|-> (fn (tyco, info) => get_typedef_info tyco vs info)
end;
@@ -117,13 +117,13 @@
fun dest_cons_tuple (Const (@{const_name Record.iso_tuple_cons}, _) $ Const _ $ t $ u) = (t, u)
| dest_cons_tuple t = raise TERM ("dest_cons_tuple", [t]);
-fun add_iso_tuple_type (b, alphas) (leftT, rightT) thy =
+fun add_iso_tuple_type overloaded (b, alphas) (leftT, rightT) thy =
let
val repT = HOLogic.mk_prodT (leftT, rightT);
val ((_, ((rep_inject, abs_inverse), absC, absT)), typ_thy) =
thy
- |> do_typedef b repT alphas
+ |> do_typedef overloaded b repT alphas
||> Sign.add_path (Binding.name_of b); (*FIXME proper prefixing instead*)
val typ_ctxt = Proof_Context.init_global typ_thy;
@@ -1499,7 +1499,7 @@
in compose_tac ctxt (false, rule'', Thm.nprems_of rule) i end);
-fun extension_definition name fields alphas zeta moreT more vars thy =
+fun extension_definition overloaded name fields alphas zeta moreT more vars thy =
let
val ctxt = Proof_Context.init_global thy;
@@ -1525,7 +1525,7 @@
let
val suff = if i = 0 then ext_typeN else inner_typeN ^ string_of_int i;
val ((_, cons), thy') = thy
- |> Iso_Tuple_Support.add_iso_tuple_type
+ |> Iso_Tuple_Support.add_iso_tuple_type overloaded
(Binding.suffix_name suff (Binding.name base_name), alphas_zeta)
(fastype_of left, fastype_of right);
in
@@ -1808,7 +1808,7 @@
(* definition *)
-fun definition (alphas, binding) parent (parents: parent_info list) raw_fields thy0 =
+fun definition overloaded (alphas, binding) parent (parents: parent_info list) raw_fields thy0 =
let
val ctxt0 = Proof_Context.init_global thy0;
@@ -1867,7 +1867,7 @@
extT, ext_induct, ext_inject, ext_surjective, ext_split, ext_def), ext_thy) =
thy0
|> Sign.qualified_path false binding
- |> extension_definition extension_name fields alphas_ext zeta moreT more vars;
+ |> extension_definition overloaded extension_name fields alphas_ext zeta moreT more vars;
val ext_ctxt = Proof_Context.init_global ext_thy;
val _ = timing_msg ext_ctxt "record preparing definitions";
@@ -2277,7 +2277,7 @@
in
-fun add_record (params, binding) raw_parent raw_fields thy =
+fun add_record overloaded (params, binding) raw_parent raw_fields thy =
let
val ctxt = Proof_Context.init_global thy;
fun cert_typ T = Type.no_tvars (Proof_Context.cert_typ ctxt T)
@@ -2327,11 +2327,11 @@
err_dup_record @ err_extra_frees @ err_no_fields @ err_dup_fields @ err_bad_fields;
val _ = if null errs then () else error (cat_lines errs);
in
- thy |> definition (params, binding) parent parents bfields
+ thy |> definition overloaded (params, binding) parent parents bfields
end
handle ERROR msg => cat_error msg ("Failed to define record " ^ Binding.print binding);
-fun add_record_cmd (raw_params, binding) raw_parent raw_fields thy =
+fun add_record_cmd overloaded (raw_params, binding) raw_parent raw_fields thy =
let
val ctxt = Proof_Context.init_global thy;
val params = map (apsnd (Typedecl.read_constraint ctxt)) raw_params;
@@ -2339,7 +2339,7 @@
val (parent, ctxt2) = read_parent raw_parent ctxt1;
val (fields, ctxt3) = read_fields raw_fields ctxt2;
val params' = map (Proof_Context.check_tfree ctxt3) params;
- in thy |> add_record (params', binding) parent fields end;
+ in thy |> add_record overloaded (params', binding) parent fields end;
end;
@@ -2348,9 +2348,10 @@
val _ =
Outer_Syntax.command @{command_keyword record} "define extensible record"
- (Parse.type_args_constrained -- Parse.binding --
+ (Parse_Spec.overloaded -- (Parse.type_args_constrained -- Parse.binding) --
(@{keyword "="} |-- Scan.option (Parse.typ --| @{keyword "+"}) --
Scan.repeat1 Parse.const_binding)
- >> (fn (x, (y, z)) => Toplevel.theory (add_record_cmd x y z)));
+ >> (fn ((overloaded, x), (y, z)) =>
+ Toplevel.theory (add_record_cmd {overloaded = overloaded} x y z)));
end;
--- a/src/HOL/Tools/typedef.ML Wed Sep 23 09:50:38 2015 +0200
+++ b/src/HOL/Tools/typedef.ML Thu Sep 24 13:33:42 2015 +0200
@@ -20,16 +20,17 @@
val default_bindings: binding -> bindings
val make_bindings: binding -> bindings option -> bindings
val make_morphisms: binding -> (binding * binding) option -> bindings
- val add_typedef: binding * (string * sort) list * mixfix ->
+ val overloaded: bool Config.T
+ val add_typedef: {overloaded: bool} -> binding * (string * sort) list * mixfix ->
term -> bindings option -> (Proof.context -> tactic) -> local_theory ->
(string * info) * local_theory
- val add_typedef_global: binding * (string * sort) list * mixfix ->
+ val add_typedef_global: {overloaded: bool} -> binding * (string * sort) list * mixfix ->
term -> bindings option -> (Proof.context -> tactic) -> theory ->
(string * info) * theory
- val typedef: binding * (string * sort) list * mixfix -> term -> bindings option ->
- local_theory -> Proof.state
- val typedef_cmd: binding * (string * string option) list * mixfix -> string -> bindings option ->
- local_theory -> Proof.state
+ val typedef: {overloaded: bool} -> binding * (string * sort) list * mixfix ->
+ term -> bindings option -> local_theory -> Proof.state
+ val typedef_cmd: {overloaded: bool} -> binding * (string * string option) list * mixfix ->
+ string -> bindings option -> local_theory -> Proof.state
end;
structure Typedef: TYPEDEF =
@@ -98,6 +99,8 @@
(* primitive typedef axiomatization -- for fresh typedecl *)
+val typedef_overloaded = Attrib.setup_config_bool @{binding typedef_overloaded} (K false);
+
fun mk_inhabited A =
let val T = HOLogic.dest_setT (Term.fastype_of A)
in HOLogic.mk_Trueprop (HOLogic.exists_const T $ Abs ("x", T, HOLogic.mk_mem (Bound 0, A))) end;
@@ -109,7 +112,7 @@
(newT --> oldT) --> (oldT --> newT) --> HOLogic.mk_setT oldT --> HOLogic.boolT);
in Logic.mk_implies (mk_inhabited A, HOLogic.mk_Trueprop (typedefC $ RepC $ AbsC $ A)) end;
-fun primitive_typedef type_definition_name newT oldT Rep_name Abs_name A lthy =
+fun primitive_typedef {overloaded} type_definition_name newT oldT Rep_name Abs_name A lthy =
let
(* errors *)
@@ -118,11 +121,13 @@
val lhs_tfrees = Term.add_tfreesT newT [];
val rhs_tfrees = Term.add_tfreesT oldT [];
val _ =
- (case fold (remove (op =)) lhs_tfrees rhs_tfrees of [] => ()
+ (case fold (remove (op =)) lhs_tfrees rhs_tfrees of
+ [] => ()
| extras => error ("Extra type variables in representing set: " ^ show_names extras));
val _ =
- (case Term.add_frees A [] of [] => []
+ (case Term.add_frees A [] of [] =>
+ []
| xs => error ("Illegal variables in representing set: " ^ show_names xs));
@@ -148,6 +153,20 @@
Theory.add_deps consts_lthy "" (const_dep (dest_Const RepC)) [newT_dep] ##>
Theory.add_deps consts_lthy "" (const_dep (dest_Const AbsC)) [newT_dep]);
+ val axiom_defs = Theory.defs_of (Proof_Context.theory_of axiom_lthy);
+ val newT_deps = maps #2 (Defs.get_deps axiom_defs (#1 newT_dep));
+ val _ =
+ if null newT_deps orelse overloaded orelse Config.get lthy typedef_overloaded then ()
+ else
+ error (Pretty.string_of (Pretty.chunks
+ [Pretty.paragraph
+ (Pretty.text "Type definition with open dependencies, use" @
+ [Pretty.brk 1, Pretty.str "\"", Pretty.keyword1 "typedef", Pretty.brk 1,
+ Pretty.str "(", Pretty.keyword2 "overloaded", Pretty.str ")\"", Pretty.brk 1] @
+ Pretty.text "or enable configuration option \"typedef_overloaded\" in the context."),
+ Pretty.block [Pretty.str " Type:", Pretty.brk 2, Syntax.pretty_typ axiom_lthy newT],
+ Pretty.block (Pretty.str " Deps:" :: Pretty.brk 2 ::
+ Pretty.commas (map (Defs.pretty_entry axiom_lthy) newT_deps))]))
in ((RepC, AbsC, axiom_name, axiom), axiom_lthy) end;
@@ -171,7 +190,7 @@
(* prepare_typedef *)
-fun prepare_typedef prep_term (name, raw_args, mx) raw_set opt_bindings lthy =
+fun prepare_typedef prep_term overloaded (name, raw_args, mx) raw_set opt_bindings lthy =
let
val bname = Binding.name_of name;
@@ -205,7 +224,7 @@
val {Rep_name, Abs_name, type_definition_name} = make_bindings name opt_bindings;
val ((RepC, AbsC, axiom_name, typedef), typedef_lthy) = typedecl_lthy
- |> primitive_typedef type_definition_name newT oldT Rep_name Abs_name set;
+ |> primitive_typedef overloaded type_definition_name newT oldT Rep_name Abs_name set;
val alias_lthy = typedef_lthy
|> Local_Theory.const_alias Rep_name (#1 (Term.dest_Const RepC))
@@ -269,18 +288,18 @@
(* add_typedef: tactic interface *)
-fun add_typedef typ set opt_bindings tac lthy =
+fun add_typedef overloaded typ set opt_bindings tac lthy =
let
val ((goal, _, typedef_result), lthy') =
- prepare_typedef Syntax.check_term typ set opt_bindings lthy;
+ prepare_typedef Syntax.check_term overloaded typ set opt_bindings lthy;
val inhabited =
Goal.prove lthy' [] [] goal (tac o #context)
|> Goal.norm_result lthy' |> Thm.close_derivation;
in typedef_result inhabited lthy' end;
-fun add_typedef_global typ set opt_bindings tac =
+fun add_typedef_global overloaded typ set opt_bindings tac =
Named_Target.theory_init
- #> add_typedef typ set opt_bindings tac
+ #> add_typedef overloaded typ set opt_bindings tac
#> Local_Theory.exit_result_global (apsnd o transform_info);
@@ -288,11 +307,11 @@
local
-fun gen_typedef prep_term prep_constraint (b, raw_args, mx) set opt_bindings lthy =
+fun gen_typedef prep_term prep_constraint overloaded (b, raw_args, mx) set opt_bindings lthy =
let
val args = map (apsnd (prep_constraint lthy)) raw_args;
val ((goal, goal_pat, typedef_result), lthy') =
- prepare_typedef prep_term (b, args, mx) set opt_bindings lthy;
+ prepare_typedef prep_term overloaded (b, args, mx) set opt_bindings lthy;
fun after_qed [[th]] = snd o typedef_result th;
in Proof.theorem NONE after_qed [[(goal, [goal_pat])]] lthy' end;
@@ -310,10 +329,14 @@
val _ =
Outer_Syntax.local_theory_to_proof @{command_keyword typedef}
"HOL type definition (requires non-emptiness proof)"
- (Parse.type_args_constrained -- Parse.binding -- Parse.opt_mixfix --
+ (Parse_Spec.overloaded -- Parse.type_args_constrained -- Parse.binding -- Parse.opt_mixfix --
(@{keyword "="} |-- Parse.term) --
Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding))
- >> (fn ((((vs, t), mx), A), opt_morphs) => fn lthy =>
- typedef_cmd (t, vs, mx) A (SOME (make_morphisms t opt_morphs)) lthy));
+ >> (fn (((((overloaded, vs), t), mx), A), opt_morphs) => fn lthy =>
+ typedef_cmd {overloaded = overloaded} (t, vs, mx) A
+ (SOME (make_morphisms t opt_morphs)) lthy));
+
+
+val overloaded = typedef_overloaded;
end;
--- a/src/HOL/Word/Word.thy Wed Sep 23 09:50:38 2015 +0200
+++ b/src/HOL/Word/Word.thy Thu Sep 24 13:33:42 2015 +0200
@@ -18,7 +18,7 @@
subsection {* Type definition *}
-typedef 'a word = "{(0::int) ..< 2 ^ len_of TYPE('a::len0)}"
+typedef (overloaded) 'a word = "{(0::int) ..< 2 ^ len_of TYPE('a::len0)}"
morphisms uint Abs_word by auto
lemma uint_nonnegative:
--- a/src/HOL/ex/PER.thy Wed Sep 23 09:50:38 2015 +0200
+++ b/src/HOL/ex/PER.thy Thu Sep 24 13:33:42 2015 +0200
@@ -154,7 +154,7 @@
definition "quot = {{x. a \<sim> x}| a::'a::partial_equiv. True}"
-typedef 'a quot = "quot :: 'a::partial_equiv set set"
+typedef (overloaded) 'a quot = "quot :: 'a::partial_equiv set set"
unfolding quot_def by blast
lemma quotI [intro]: "{x. a \<sim> x} \<in> quot"
--- a/src/Pure/Isar/parse_spec.ML Wed Sep 23 09:50:38 2015 +0200
+++ b/src/Pure/Isar/parse_spec.ML Thu Sep 24 13:33:42 2015 +0200
@@ -29,6 +29,7 @@
val obtains: Element.obtains parser
val general_statement: (Element.context list * Element.statement) parser
val statement_keyword: string parser
+ val overloaded: bool parser
end;
structure Parse_Spec: PARSE_SPEC =
@@ -155,4 +156,10 @@
val statement_keyword = Parse.$$$ "obtains" || Parse.$$$ "shows";
+
+(* options *)
+
+val overloaded =
+ Scan.optional (Parse.$$$ "(" -- Parse.$$$ "overloaded" -- Parse.$$$ ")" >> K true) false;
+
end;
--- a/src/Pure/defs.ML Wed Sep 23 09:50:38 2015 +0200
+++ b/src/Pure/defs.ML Thu Sep 24 13:33:42 2015 +0200
@@ -12,6 +12,7 @@
val item_ord: item * item -> order
type entry = item * typ list
val pretty_args: Proof.context -> typ list -> Pretty.T list
+ val pretty_entry: Proof.context -> entry -> Pretty.T
val plain_args: typ list -> bool
type T
type spec =
@@ -28,6 +29,7 @@
val empty: T
val merge: Proof.context -> T * T -> T
val define: Proof.context -> bool -> string option -> string -> entry -> entry list -> T -> T
+ val get_deps: T -> item -> (typ list * entry list) list
end;
structure Defs: DEFS =
@@ -241,4 +243,6 @@
val defs' = defs |> update_specs c spec;
in Defs (defs' |> (if unchecked then I else dependencies ctxt (c, args) restr deps)) end;
+fun get_deps (Defs defs) c = reducts_of defs c;
+
end;