# HG changeset patch # User wenzelm # Date 1350071485 -7200 # Node ID 2328a5197e77830020a94b10da9eb3b03794eaa7 # Parent 9cbec40e88eab064f22c58ce06887a288993b1cb# Parent c13b3954297248173493578b1e63efea0560c8c0 merged diff -r 9cbec40e88ea -r 2328a5197e77 NEWS --- a/NEWS Fri Oct 12 15:52:55 2012 +0200 +++ b/NEWS Fri Oct 12 21:51:25 2012 +0200 @@ -62,6 +62,13 @@ *** HOL *** +* Simplified 'typedef' specifications: historical options for implicit +set definition and alternative name have been discontinued. The +former behavior of "typedef (open) t = A" is now the default, but +written just "typedef t = A". INCOMPATIBILITY, need to adapt theories +accordingly. + + * Theory "Library/Multiset": - Renamed constants diff -r 9cbec40e88ea -r 2328a5197e77 src/Doc/IsarRef/HOL_Specific.thy --- a/src/Doc/IsarRef/HOL_Specific.thy Fri Oct 12 15:52:55 2012 +0200 +++ b/src/Doc/IsarRef/HOL_Specific.thy Fri Oct 12 21:51:25 2012 +0200 @@ -1089,11 +1089,9 @@ abbreviations, without any logical significance. @{rail " - @@{command (HOL) typedef} alt_name? abs_type '=' rep_set + @@{command (HOL) typedef} abs_type '=' rep_set ; - alt_name: '(' (@{syntax name} | @'open' | @'open' @{syntax name}) ')' - ; abs_type: @{syntax typespec_sorts} @{syntax mixfix}? ; rep_set: @{syntax term} (@'morphisms' @{syntax name} @{syntax name})? @@ -1117,13 +1115,12 @@ and the new type @{text t} may then change in different application contexts. - By default, @{command (HOL) "typedef"} defines both a type - constructor @{text t} for the new type, and a term constant @{text - t} for the representing set within the old type. Use the ``@{text - "(open)"}'' option to suppress a separate constant definition - altogether. The injection from type to set is called @{text Rep_t}, - its inverse @{text Abs_t}, unless explicit @{keyword (HOL) - "morphisms"} specification provides alternative names. + For @{command (HOL) "typedef"}~@{text "t = A"} the newly introduced + type @{text t} is accompanied by a pair of morphisms to relate it to + the representing set over the old type. By default, the injection + from type to set is called @{text Rep_t} and its inverse @{text + Abs_t}: An explicit @{keyword (HOL) "morphisms"} specification + allows to provide alternative names. The core axiomatization uses the locale predicate @{const type_definition} as defined in Isabelle/HOL. Various basic @@ -1147,10 +1144,6 @@ for the generic @{method cases} and @{method induct} methods, respectively. - An alternative name for the set definition (and other derived - entities) may be specified in parentheses; the default is to use - @{text t} directly. - \end{description} \begin{warn} @@ -1160,8 +1153,7 @@ HOL logic. Moreover, one needs to demonstrate that the interpretation of such free-form axiomatizations can coexist with that of the regular @{command_def typedef} scheme, and any extension - that other people might have introduced elsewhere (e.g.\ in HOLCF - \cite{MuellerNvOS99}). + that other people might have introduced elsewhere. \end{warn} *} @@ -1189,7 +1181,7 @@ \medskip The following trivial example pulls a three-element type into existence within the formal logical environment of HOL. *} -typedef (open) three = "{(True, True), (True, False), (False, True)}" +typedef three = "{(True, True), (True, False), (False, True)}" by blast definition "One = Abs_three (True, True)" diff -r 9cbec40e88ea -r 2328a5197e77 src/Doc/Tutorial/Types/Typedefs.thy --- a/src/Doc/Tutorial/Types/Typedefs.thy Fri Oct 12 15:52:55 2012 +0200 +++ b/src/Doc/Tutorial/Types/Typedefs.thy Fri Oct 12 21:51:25 2012 +0200 @@ -69,7 +69,7 @@ It is easily represented by the first three natural numbers: *} -typedef (open) three = "{0::nat, 1, 2}" +typedef three = "{0::nat, 1, 2}" txt{*\noindent In order to enforce that the representing set on the right-hand side is diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/Algebra/poly/UnivPoly2.thy --- a/src/HOL/Algebra/poly/UnivPoly2.thy Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/Algebra/poly/UnivPoly2.thy Fri Oct 12 21:51:25 2012 +0200 @@ -42,7 +42,7 @@ definition "UP = {f :: nat => 'a::zero. EX n. bound n f}" -typedef (open) 'a up = "UP :: (nat => 'a::zero) set" +typedef 'a up = "UP :: (nat => 'a::zero) set" morphisms Rep_UP Abs_UP proof - have "bound 0 (\_. 0::'a)" by (rule boundI) (rule refl) diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/BNF/Countable_Set.thy --- a/src/HOL/BNF/Countable_Set.thy Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/BNF/Countable_Set.thy Fri Oct 12 21:51:25 2012 +0200 @@ -315,7 +315,7 @@ subsection{* The type of countable sets *} -typedef (open) 'a cset = "{A :: 'a set. countable A}" +typedef 'a cset = "{A :: 'a set. countable A}" apply(rule exI[of _ "{}"]) by simp abbreviation rcset where "rcset \ Rep_cset" diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/BNF/Tools/bnf_comp.ML --- a/src/HOL/BNF/Tools/bnf_comp.ML Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/BNF/Tools/bnf_comp.ML Fri Oct 12 21:51:25 2012 +0200 @@ -625,7 +625,7 @@ val deads = map TFree params; val ((bdT_name, (bdT_glob_info, bdT_loc_info)), lthy) = - typedef false NONE (bdT_bind, params, NoSyn) + typedef (bdT_bind, params, NoSyn) (HOLogic.mk_UNIV bd_repT) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy; val bnf_bd' = mk_dir_image bnf_bd diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/BNF/Tools/bnf_gfp.ML --- a/src/HOL/BNF/Tools/bnf_gfp.ML Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML Fri Oct 12 21:51:25 2012 +0200 @@ -1023,7 +1023,7 @@ val sbdT_bind = Binding.suffix_name ("_" ^ sum_bdTN) b; val ((sbdT_name, (sbdT_glob_info, sbdT_loc_info)), lthy) = - typedef false NONE (sbdT_bind, dead_params, NoSyn) + typedef (sbdT_bind, dead_params, NoSyn) (HOLogic.mk_UNIV sum_bdT) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy; val sbdT = Type (sbdT_name, dead_params'); @@ -1824,7 +1824,7 @@ val ((T_names, (T_glob_infos, T_loc_infos)), lthy) = lthy |> fold_map4 (fn b => fn mx => fn car_final => fn in_car_final => - typedef false NONE (b, params, mx) car_final NONE + typedef (b, params, mx) car_final NONE (EVERY' [rtac exI, rtac in_car_final] 1)) bs mixfixes car_finals in_car_final_thms |>> apsnd split_list o split_list; diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/BNF/Tools/bnf_lfp.ML --- a/src/HOL/BNF/Tools/bnf_lfp.ML Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML Fri Oct 12 21:51:25 2012 +0200 @@ -776,7 +776,7 @@ val IIT_bind = Binding.suffix_name ("_" ^ IITN) b; val ((IIT_name, (IIT_glob_info, IIT_loc_info)), lthy) = - typedef false NONE (IIT_bind, params, NoSyn) + typedef (IIT_bind, params, NoSyn) (HOLogic.mk_UNIV II_repT) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy; val IIT = Type (IIT_name, params'); @@ -936,7 +936,7 @@ val ((T_names, (T_glob_infos, T_loc_infos)), lthy) = lthy - |> fold_map3 (fn b => fn mx => fn car_init => typedef false NONE (b, params, mx) car_init NONE + |> fold_map3 (fn b => fn mx => fn car_init => typedef (b, params, mx) car_init NONE (EVERY' [rtac ssubst, rtac @{thm ex_in_conv}, resolve_tac alg_not_empty_thms, rtac alg_init_thm] 1)) bs mixfixes car_inits |>> apsnd split_list o split_list; diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/BNF/Tools/bnf_util.ML --- a/src/HOL/BNF/Tools/bnf_util.ML Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/BNF/Tools/bnf_util.ML Fri Oct 12 21:51:25 2012 +0200 @@ -154,7 +154,7 @@ val parse_binding_colon: Token.T list -> binding * Token.T list val parse_opt_binding_colon: Token.T list -> binding * Token.T list - val typedef: bool -> binding option -> binding * (string * sort) list * mixfix -> term -> + val typedef: binding * (string * sort) list * mixfix -> term -> (binding * binding) option -> tactic -> local_theory -> (string * Typedef.info) * local_theory val WRAP: ('a -> tactic) -> ('a -> tactic) -> 'a list -> tactic -> tactic @@ -280,11 +280,11 @@ val parse_opt_binding_colon = Scan.optional parse_binding_colon Binding.empty; (*TODO: is this really different from Typedef.add_typedef_global?*) -fun typedef def opt_name typ set opt_morphs tac lthy = +fun typedef typ set opt_morphs tac lthy = let val ((name, info), (lthy, lthy_old)) = lthy - |> Typedef.add_typedef def opt_name typ set opt_morphs tac + |> Typedef.add_typedef typ set opt_morphs tac ||> `Local_Theory.restore; val phi = Proof_Context.export_morphism lthy_old lthy; in diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/Code_Numeral.thy --- a/src/HOL/Code_Numeral.thy Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/Code_Numeral.thy Fri Oct 12 21:51:25 2012 +0200 @@ -13,7 +13,7 @@ subsection {* Datatype of target language numerals *} -typedef (open) code_numeral = "UNIV \ nat set" +typedef code_numeral = "UNIV \ nat set" morphisms nat_of of_nat .. lemma of_nat_nat_of [simp]: diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/Datatype.thy --- a/src/HOL/Datatype.thy Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/Datatype.thy Fri Oct 12 21:51:25 2012 +0200 @@ -14,7 +14,7 @@ definition "Node = {p. EX f x k. p = (f :: nat => 'b + nat, x ::'a + nat) & f k = Inr 0}" -typedef (open) ('a, 'b) node = "Node :: ((nat => 'b + nat) * ('a + nat)) set" +typedef ('a, 'b) node = "Node :: ((nat => 'b + nat) * ('a + nat)) set" morphisms Rep_Node Abs_Node unfolding Node_def by auto diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/HOLCF/Algebraic.thy --- a/src/HOL/HOLCF/Algebraic.thy Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/HOLCF/Algebraic.thy Fri Oct 12 21:51:25 2012 +0200 @@ -12,7 +12,7 @@ subsection {* Type constructor for finite deflations *} -typedef (open) 'a fin_defl = "{d::'a \ 'a. finite_deflation d}" +typedef 'a fin_defl = "{d::'a \ 'a. finite_deflation d}" by (fast intro: finite_deflation_bottom) instantiation fin_defl :: (bifinite) below @@ -74,7 +74,7 @@ subsection {* Defining algebraic deflations by ideal completion *} -typedef (open) 'a defl = "{S::'a fin_defl set. below.ideal S}" +typedef 'a defl = "{S::'a fin_defl set. below.ideal S}" by (rule below.ex_ideal) instantiation defl :: (bifinite) below diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/HOLCF/Compact_Basis.thy --- a/src/HOL/HOLCF/Compact_Basis.thy Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/HOLCF/Compact_Basis.thy Fri Oct 12 21:51:25 2012 +0200 @@ -14,7 +14,7 @@ definition "pd_basis = {S::'a compact_basis set. finite S \ S \ {}}" -typedef (open) 'a pd_basis = "pd_basis :: 'a compact_basis set set" +typedef 'a pd_basis = "pd_basis :: 'a compact_basis set set" unfolding pd_basis_def apply (rule_tac x="{arbitrary}" in exI) apply simp diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/HOLCF/ConvexPD.thy --- a/src/HOL/HOLCF/ConvexPD.thy Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/HOLCF/ConvexPD.thy Fri Oct 12 21:51:25 2012 +0200 @@ -119,7 +119,7 @@ subsection {* Type definition *} -typedef (open) 'a convex_pd = +typedef 'a convex_pd = "{S::'a pd_basis set. convex_le.ideal S}" by (rule convex_le.ex_ideal) diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/HOLCF/LowerPD.thy --- a/src/HOL/HOLCF/LowerPD.thy Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/HOLCF/LowerPD.thy Fri Oct 12 21:51:25 2012 +0200 @@ -74,7 +74,7 @@ subsection {* Type definition *} -typedef (open) 'a lower_pd = +typedef 'a lower_pd = "{S::'a pd_basis set. lower_le.ideal S}" by (rule lower_le.ex_ideal) diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/HOLCF/Tools/cpodef.ML --- a/src/HOL/HOLCF/Tools/cpodef.ML Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/HOLCF/Tools/cpodef.ML Fri Oct 12 21:51:25 2012 +0200 @@ -58,18 +58,6 @@ fun below_const T = Const (@{const_name below}, T --> T --> HOLogic.boolT) -(* manipulating theorems *) - -fun fold_adm_mem thm NONE = thm - | fold_adm_mem thm (SOME set_def) = - let val rule = @{lemma "A == B ==> adm (%x. x : B) ==> adm (%x. x : A)" by simp} - in rule OF [set_def, thm] end - -fun fold_bottom_mem thm NONE = thm - | fold_bottom_mem thm (SOME set_def) = - let val rule = @{lemma "A == B ==> bottom : B ==> bottom : A" by simp} - in rule OF [set_def, thm] end - (* proving class instances *) fun prove_cpo @@ -77,14 +65,12 @@ (newT: typ) (Rep_name: binding, Abs_name: binding) (type_definition: thm) (* type_definition Rep Abs A *) - (set_def: thm option) (* A == set *) (below_def: thm) (* op << == %x y. Rep x << Rep y *) (admissible: thm) (* adm (%x. x : set) *) (thy: theory) = let - val admissible' = fold_adm_mem admissible set_def - val cpo_thms = map (Thm.transfer thy) [type_definition, below_def, admissible'] + val cpo_thms = map (Thm.transfer thy) [type_definition, below_def, admissible] val (full_tname, Ts) = dest_Type newT val lhs_sorts = map (snd o dest_TFree) Ts val tac = Tactic.rtac (@{thm typedef_cpo} OF cpo_thms) 1 @@ -100,14 +86,14 @@ thy |> Sign.add_path (Binding.name_of name) |> Global_Theory.add_thms - ([((Binding.prefix_name "adm_" name, admissible'), []), - ((Binding.prefix_name "cont_" Rep_name, cont_Rep ), []), - ((Binding.prefix_name "cont_" Abs_name, cont_Abs ), []), - ((Binding.prefix_name "lub_" name, lub ), []), - ((Binding.prefix_name "compact_" name, compact ), [])]) + ([((Binding.prefix_name "adm_" name, admissible), []), + ((Binding.prefix_name "cont_" Rep_name, cont_Rep ), []), + ((Binding.prefix_name "cont_" Abs_name, cont_Abs ), []), + ((Binding.prefix_name "lub_" name, lub ), []), + ((Binding.prefix_name "compact_" name, compact ), [])]) ||> Sign.parent_path val cpo_info : cpo_info = - { below_def = below_def, adm = admissible', cont_Rep = cont_Rep, + { below_def = below_def, adm = admissible, cont_Rep = cont_Rep, cont_Abs = cont_Abs, lub = lub, compact = compact } in (cpo_info, thy) @@ -118,14 +104,12 @@ (newT: typ) (Rep_name: binding, Abs_name: binding) (type_definition: thm) (* type_definition Rep Abs A *) - (set_def: thm option) (* A == set *) (below_def: thm) (* op << == %x y. Rep x << Rep y *) (bottom_mem: thm) (* bottom : set *) (thy: theory) = let - val bottom_mem' = fold_bottom_mem bottom_mem set_def - val pcpo_thms = map (Thm.transfer thy) [type_definition, below_def, bottom_mem'] + val pcpo_thms = map (Thm.transfer thy) [type_definition, below_def, bottom_mem] val (full_tname, Ts) = dest_Type newT val lhs_sorts = map (snd o dest_TFree) Ts val tac = Tactic.rtac (@{thm typedef_pcpo} OF pcpo_thms) 1 @@ -184,7 +168,7 @@ let val name = #1 typ val ((full_tname, info as ({Rep_name, ...}, {type_definition, ...})), thy) = thy - |> Typedef.add_typedef_global false NONE typ set opt_morphs tac + |> Typedef.add_typedef_global typ set opt_morphs tac val oldT = #rep_type (#1 info) val newT = #abs_type (#1 info) val lhs_tfrees = map dest_TFree (snd (dest_Type newT)) @@ -222,10 +206,10 @@ fun cpodef_result nonempty admissible thy = let - val ((info as (_, {type_definition, set_def, ...}), below_def), thy) = thy + val ((info as (_, {type_definition, ...}), below_def), thy) = thy |> add_podef typ set opt_morphs (Tactic.rtac nonempty 1) val (cpo_info, thy) = thy - |> prove_cpo name newT morphs type_definition set_def below_def admissible + |> prove_cpo name newT morphs type_definition below_def admissible in ((info, cpo_info), thy) end @@ -256,12 +240,12 @@ fun pcpodef_result bottom_mem admissible thy = let val tac = Tactic.rtac exI 1 THEN Tactic.rtac bottom_mem 1 - val ((info as (_, {type_definition, set_def, ...}), below_def), thy) = thy + val ((info as (_, {type_definition, ...}), below_def), thy) = thy |> add_podef typ set opt_morphs tac val (cpo_info, thy) = thy - |> prove_cpo name newT morphs type_definition set_def below_def admissible + |> prove_cpo name newT morphs type_definition below_def admissible val (pcpo_info, thy) = thy - |> prove_pcpo name newT morphs type_definition set_def below_def bottom_mem + |> prove_pcpo name newT morphs type_definition below_def bottom_mem in ((info, cpo_info, pcpo_info), thy) end diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/HOLCF/Tools/domaindef.ML --- a/src/HOL/HOLCF/Tools/domaindef.ML Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/HOLCF/Tools/domaindef.ML Fri Oct 12 21:51:25 2012 +0200 @@ -162,12 +162,8 @@ val liftemb_def = singleton (Proof_Context.export lthy ctxt_thy) liftemb_ldef val liftprj_def = singleton (Proof_Context.export lthy ctxt_thy) liftprj_ldef val liftdefl_def = singleton (Proof_Context.export lthy ctxt_thy) liftdefl_ldef - val type_definition_thm = - Raw_Simplifier.rewrite_rule - (the_list (#set_def (#2 info))) - (#type_definition (#2 info)) val typedef_thms = - [type_definition_thm, #below_def cpo_info, emb_def, prj_def, defl_def, + [#type_definition (#2 info), #below_def cpo_info, emb_def, prj_def, defl_def, liftemb_def, liftprj_def, liftdefl_def] val thy = lthy |> Class.prove_instantiation_instance diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/HOLCF/Universal.thy --- a/src/HOL/HOLCF/Universal.thy Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/HOLCF/Universal.thy Fri Oct 12 21:51:25 2012 +0200 @@ -198,7 +198,7 @@ subsection {* Defining the universal domain by ideal completion *} -typedef (open) udom = "{S. udom.ideal S}" +typedef udom = "{S. udom.ideal S}" by (rule udom.ex_ideal) instantiation udom :: below @@ -247,7 +247,7 @@ subsection {* Compact bases of domains *} -typedef (open) 'a compact_basis = "{x::'a::pcpo. compact x}" +typedef 'a compact_basis = "{x::'a::pcpo. compact x}" by auto lemma Rep_compact_basis' [simp]: "compact (Rep_compact_basis a)" diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/HOLCF/UpperPD.thy --- a/src/HOL/HOLCF/UpperPD.thy Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/HOLCF/UpperPD.thy Fri Oct 12 21:51:25 2012 +0200 @@ -72,7 +72,7 @@ subsection {* Type definition *} -typedef (open) 'a upper_pd = +typedef 'a upper_pd = "{S::'a pd_basis set. upper_le.ideal S}" by (rule upper_le.ex_ideal) diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/Import/import_rule.ML --- a/src/HOL/Import/import_rule.ML Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/Import/import_rule.ML Fri Oct 12 21:51:25 2012 +0200 @@ -220,9 +220,8 @@ val tfrees = Term.add_tfrees c [] val tnames = sort_strings (map fst tfrees) val ((_, typedef_info), thy') = - Typedef.add_typedef_global false NONE - (Binding.name tycname, map (rpair dummyS) tnames, NoSyn) c - (SOME(Binding.name rep_name,Binding.name abs_name)) (rtac th2 1) thy + Typedef.add_typedef_global (Binding.name tycname, map (rpair dummyS) tnames, NoSyn) c + (SOME (Binding.name rep_name, Binding.name abs_name)) (rtac th2 1) thy val aty = #abs_type (#1 typedef_info) val th = freezeT (#type_definition (#2 typedef_info)) val (th_s, _) = Thm.dest_comb (Thm.dest_arg (cprop_of th)) diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/Induct/QuoDataType.thy --- a/src/HOL/Induct/QuoDataType.thy Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/Induct/QuoDataType.thy Fri Oct 12 21:51:25 2012 +0200 @@ -125,7 +125,7 @@ definition "Msg = UNIV//msgrel" -typedef (open) msg = Msg +typedef msg = Msg morphisms Rep_Msg Abs_Msg unfolding Msg_def by (auto simp add: quotient_def) diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/Induct/QuoNestedDataType.thy --- a/src/HOL/Induct/QuoNestedDataType.thy Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/Induct/QuoNestedDataType.thy Fri Oct 12 21:51:25 2012 +0200 @@ -144,7 +144,7 @@ definition "Exp = UNIV//exprel" -typedef (open) exp = Exp +typedef exp = Exp morphisms Rep_Exp Abs_Exp unfolding Exp_def by (auto simp add: quotient_def) diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/Induct/SList.thy --- a/src/HOL/Induct/SList.thy Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/Induct/SList.thy Fri Oct 12 21:51:25 2012 +0200 @@ -55,7 +55,7 @@ definition "List = list (range Leaf)" -typedef (open) 'a list = "List :: 'a item set" +typedef 'a list = "List :: 'a item set" morphisms Rep_List Abs_List unfolding List_def by (blast intro: list.NIL_I) diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/Library/Bit.thy --- a/src/HOL/Library/Bit.thy Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/Library/Bit.thy Fri Oct 12 21:51:25 2012 +0200 @@ -10,7 +10,7 @@ subsection {* Bits as a datatype *} -typedef (open) bit = "UNIV :: bool set" .. +typedef bit = "UNIV :: bool set" .. instantiation bit :: "{zero, one}" begin diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/Library/DAList.thy --- a/src/HOL/Library/DAList.thy Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/Library/DAList.thy Fri Oct 12 21:51:25 2012 +0200 @@ -17,7 +17,7 @@ subsection {* Type @{text "('key, 'value) alist" } *} -typedef (open) ('key, 'value) alist = "{xs :: ('key \ 'value) list. (distinct o map fst) xs}" +typedef ('key, 'value) alist = "{xs :: ('key \ 'value) list. (distinct o map fst) xs}" morphisms impl_of Alist proof show "[] \ {xs. (distinct o map fst) xs}" by simp diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/Library/Dlist.thy --- a/src/HOL/Library/Dlist.thy Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/Library/Dlist.thy Fri Oct 12 21:51:25 2012 +0200 @@ -8,7 +8,7 @@ subsection {* The type of distinct lists *} -typedef (open) 'a dlist = "{xs::'a list. distinct xs}" +typedef 'a dlist = "{xs::'a list. distinct xs}" morphisms list_of_dlist Abs_dlist proof show "[] \ {xs. distinct xs}" by simp diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/Library/Extended_Nat.thy --- a/src/HOL/Library/Extended_Nat.thy Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/Library/Extended_Nat.thy Fri Oct 12 21:51:25 2012 +0200 @@ -25,7 +25,7 @@ infinity. *} -typedef (open) enat = "UNIV :: nat option set" .. +typedef enat = "UNIV :: nat option set" .. definition enat :: "nat \ enat" where "enat n = Abs_enat (Some n)" diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/Library/FinFun.thy --- a/src/HOL/Library/FinFun.thy Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/Library/FinFun.thy Fri Oct 12 21:51:25 2012 +0200 @@ -83,7 +83,7 @@ definition "finfun = {f::'a\'b. \b. finite {a. f a \ b}}" -typedef (open) ('a,'b) finfun ("(_ =>f /_)" [22, 21] 21) = "finfun :: ('a => 'b) set" +typedef ('a,'b) finfun ("(_ =>f /_)" [22, 21] 21) = "finfun :: ('a => 'b) set" morphisms finfun_apply Abs_finfun proof - have "\f. finite {x. f x \ undefined}" diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/Library/Float.thy --- a/src/HOL/Library/Float.thy Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/Library/Float.thy Fri Oct 12 21:51:25 2012 +0200 @@ -11,7 +11,7 @@ definition "float = {m * 2 powr e | (m :: int) (e :: int). True}" -typedef (open) float = float +typedef float = float morphisms real_of_float float_of unfolding float_def by auto diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/Library/Formal_Power_Series.thy --- a/src/HOL/Library/Formal_Power_Series.thy Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/Library/Formal_Power_Series.thy Fri Oct 12 21:51:25 2012 +0200 @@ -11,7 +11,7 @@ subsection {* The type of formal power series*} -typedef (open) 'a fps = "{f :: nat \ 'a. True}" +typedef 'a fps = "{f :: nat \ 'a. True}" morphisms fps_nth Abs_fps by simp diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/Library/Fraction_Field.thy --- a/src/HOL/Library/Fraction_Field.thy Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/Library/Fraction_Field.thy Fri Oct 12 21:51:25 2012 +0200 @@ -55,7 +55,7 @@ definition "fract = {(x::'a\'a). snd x \ (0::'a::idom)} // fractrel" -typedef (open) 'a fract = "fract :: ('a * 'a::idom) set set" +typedef 'a fract = "fract :: ('a * 'a::idom) set set" unfolding fract_def proof have "(0::'a, 1::'a) \ {x. snd x \ 0}" by simp diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/Library/Mapping.thy --- a/src/HOL/Library/Mapping.thy Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/Library/Mapping.thy Fri Oct 12 21:51:25 2012 +0200 @@ -8,7 +8,7 @@ subsection {* Type definition and primitive operations *} -typedef (open) ('a, 'b) mapping = "UNIV :: ('a \ 'b) set" +typedef ('a, 'b) mapping = "UNIV :: ('a \ 'b) set" morphisms lookup Mapping .. lemma lookup_Mapping [simp]: diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/Library/Multiset.thy Fri Oct 12 21:51:25 2012 +0200 @@ -12,7 +12,7 @@ definition "multiset = {f :: 'a => nat. finite {x. f x > 0}}" -typedef (open) 'a multiset = "multiset :: ('a => nat) set" +typedef 'a multiset = "multiset :: ('a => nat) set" morphisms count Abs_multiset unfolding multiset_def proof diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/Library/Numeral_Type.thy --- a/src/HOL/Library/Numeral_Type.thy Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/Library/Numeral_Type.thy Fri Oct 12 21:51:25 2012 +0200 @@ -10,16 +10,16 @@ subsection {* Numeral Types *} -typedef (open) num0 = "UNIV :: nat set" .. -typedef (open) num1 = "UNIV :: unit set" .. +typedef num0 = "UNIV :: nat set" .. +typedef num1 = "UNIV :: unit set" .. -typedef (open) 'a bit0 = "{0 ..< 2 * int CARD('a::finite)}" +typedef 'a bit0 = "{0 ..< 2 * int CARD('a::finite)}" proof show "0 \ {0 ..< 2 * int CARD('a)}" by simp qed -typedef (open) 'a bit1 = "{0 ..< 1 + 2 * int CARD('a::finite)}" +typedef 'a bit1 = "{0 ..< 1 + 2 * int CARD('a::finite)}" proof show "0 \ {0 ..< 1 + 2 * int CARD('a)}" by simp diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/Library/Polynomial.thy --- a/src/HOL/Library/Polynomial.thy Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/Library/Polynomial.thy Fri Oct 12 21:51:25 2012 +0200 @@ -13,7 +13,7 @@ definition "Poly = {f::nat \ 'a::zero. \n. \i>n. f i = 0}" -typedef (open) 'a poly = "Poly :: (nat => 'a::zero) set" +typedef 'a poly = "Poly :: (nat => 'a::zero) set" morphisms coeff Abs_poly unfolding Poly_def by auto diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/Library/Quotient_Type.thy --- a/src/HOL/Library/Quotient_Type.thy Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/Library/Quotient_Type.thy Fri Oct 12 21:51:25 2012 +0200 @@ -60,7 +60,7 @@ definition "quot = {{x. a \ x} | a::'a::eqv. True}" -typedef (open) 'a quot = "quot :: 'a::eqv set set" +typedef 'a quot = "quot :: 'a::eqv set set" unfolding quot_def by blast lemma quotI [intro]: "{x. a \ x} \ quot" diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/Library/RBT.thy --- a/src/HOL/Library/RBT.thy Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/Library/RBT.thy Fri Oct 12 21:51:25 2012 +0200 @@ -10,7 +10,7 @@ subsection {* Type definition *} -typedef (open) ('a, 'b) rbt = "{t :: ('a\linorder, 'b) RBT_Impl.rbt. is_rbt t}" +typedef ('a, 'b) rbt = "{t :: ('a\linorder, 'b) RBT_Impl.rbt. is_rbt t}" morphisms impl_of RBT proof - have "RBT_Impl.Empty \ ?rbt" by simp diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/Library/Saturated.thy --- a/src/HOL/Library/Saturated.thy Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/Library/Saturated.thy Fri Oct 12 21:51:25 2012 +0200 @@ -12,7 +12,7 @@ subsection {* The type of saturated naturals *} -typedef (open) ('a::len) sat = "{.. len_of TYPE('a)}" +typedef ('a::len) sat = "{.. len_of TYPE('a)}" morphisms nat_of Abs_sat by auto diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/Library/Target_Numeral.thy --- a/src/HOL/Library/Target_Numeral.thy Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/Library/Target_Numeral.thy Fri Oct 12 21:51:25 2012 +0200 @@ -4,7 +4,7 @@ subsection {* Type of target language numerals *} -typedef (open) int = "UNIV \ int set" +typedef int = "UNIV \ int set" morphisms int_of of_int .. hide_type (open) int diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/Limits.thy --- a/src/HOL/Limits.thy Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/Limits.thy Fri Oct 12 21:51:25 2012 +0200 @@ -20,7 +20,7 @@ assumes conj: "F (\x. P x) \ F (\x. Q x) \ F (\x. P x \ Q x)" assumes mono: "\x. P x \ Q x \ F (\x. P x) \ F (\x. Q x)" -typedef (open) 'a filter = "{F :: ('a \ bool) \ bool. is_filter F}" +typedef 'a filter = "{F :: ('a \ bool) \ bool. is_filter F}" proof show "(\x. True) \ ?filter" by (auto intro: is_filter.intro) qed diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/Matrix_LP/Matrix.thy --- a/src/HOL/Matrix_LP/Matrix.thy Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/Matrix_LP/Matrix.thy Fri Oct 12 21:51:25 2012 +0200 @@ -13,7 +13,7 @@ definition "matrix = {(f::(nat \ nat \ 'a::zero)). finite (nonzero_positions f)}" -typedef (open) 'a matrix = "matrix :: (nat \ nat \ 'a::zero) set" +typedef 'a matrix = "matrix :: (nat \ nat \ 'a::zero) set" unfolding matrix_def proof show "(\j i. 0) \ {(f::(nat \ nat \ 'a::zero)). finite (nonzero_positions f)}" diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy --- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Fri Oct 12 21:51:25 2012 +0200 @@ -13,7 +13,7 @@ subsection {* Finite Cartesian products, with indexing and lambdas. *} -typedef (open) ('a, 'b) vec = "UNIV :: (('b::finite) \ 'a) set" +typedef ('a, 'b) vec = "UNIV :: (('b::finite) \ 'a) set" morphisms vec_nth vec_lambda .. notation diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Oct 12 21:51:25 2012 +0200 @@ -13,7 +13,7 @@ subsection {* General notion of a topology as a value *} definition "istopology L \ L {} \ (\S T. L S \ L T \ L (S \ T)) \ (\K. Ball K L \ L (\ K))" -typedef (open) 'a topology = "{L::('a set) \ bool. istopology L}" +typedef 'a topology = "{L::('a set) \ bool. istopology L}" morphisms "openin" "topology" unfolding istopology_def by blast diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/NSA/StarDef.thy --- a/src/HOL/NSA/StarDef.thy Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/NSA/StarDef.thy Fri Oct 12 21:51:25 2012 +0200 @@ -40,7 +40,7 @@ definition "star = (UNIV :: (nat \ 'a) set) // starrel" -typedef (open) 'a star = "star :: (nat \ 'a) set set" +typedef 'a star = "star :: (nat \ 'a) set set" unfolding star_def by (auto intro: quotientI) definition diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/Nat.thy --- a/src/HOL/Nat.thy Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/Nat.thy Fri Oct 12 21:51:25 2012 +0200 @@ -33,7 +33,7 @@ Zero_RepI: "Nat Zero_Rep" | Suc_RepI: "Nat i \ Nat (Suc_Rep i)" -typedef (open) nat = "{n. Nat n}" +typedef nat = "{n. Nat n}" morphisms Rep_Nat Abs_Nat using Nat.Zero_RepI by auto diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/Nitpick_Examples/Manual_Nits.thy --- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Fri Oct 12 21:51:25 2012 +0200 @@ -95,7 +95,7 @@ subsection {* 2.7. Typedefs, Records, Rationals, and Reals *} definition "three = {0\nat, 1, 2}" -typedef (open) three = three +typedef three = three unfolding three_def by blast definition A :: three where "A \ Abs_three 0" @@ -201,7 +201,7 @@ (* BEGIN LAZY LIST SETUP *) definition "llist = (UNIV\('a list + (nat \ 'a)) set)" -typedef (open) 'a llist = "llist\('a list + (nat \ 'a)) set" +typedef 'a llist = "llist\('a list + (nat \ 'a)) set" unfolding llist_def by auto definition LNil where diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/Nitpick_Examples/Refute_Nits.thy --- a/src/HOL/Nitpick_Examples/Refute_Nits.thy Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy Fri Oct 12 21:51:25 2012 +0200 @@ -541,7 +541,7 @@ definition "myTdef = insert (undefined::'a) (undefined::'a set)" -typedef (open) 'a myTdef = "myTdef :: 'a set" +typedef 'a myTdef = "myTdef :: 'a set" unfolding myTdef_def by auto lemma "(x\'a myTdef) = y" @@ -552,7 +552,7 @@ definition "T_bij = {(f::'a\'a). \y. \!x. f x = y}" -typedef (open) 'a T_bij = "T_bij :: ('a \ 'a) set" +typedef 'a T_bij = "T_bij :: ('a \ 'a) set" unfolding T_bij_def by auto lemma "P (f\(myTdecl myTdef) T_bij)" diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/Nitpick_Examples/Typedef_Nits.thy --- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy Fri Oct 12 21:51:25 2012 +0200 @@ -15,7 +15,7 @@ timeout = 240] definition "three = {0\nat, 1, 2}" -typedef (open) three = three +typedef three = three unfolding three_def by blast definition A :: three where "A \ Abs_three 0" @@ -28,7 +28,7 @@ definition "one_or_two = {undefined False\'a, undefined True}" -typedef (open) 'a one_or_two = "one_or_two :: 'a set" +typedef 'a one_or_two = "one_or_two :: 'a set" unfolding one_or_two_def by auto lemma "x = (y\unit one_or_two)" @@ -54,7 +54,7 @@ definition "bounded = {n\nat. finite (UNIV \ 'a set) \ n < card (UNIV \ 'a set)}" -typedef (open) 'a bounded = "bounded(TYPE('a))" +typedef 'a bounded = "bounded(TYPE('a))" unfolding bounded_def apply (rule_tac x = 0 in exI) apply (case_tac "card UNIV = 0") diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/Nominal/Nominal.thy --- a/src/HOL/Nominal/Nominal.thy Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/Nominal/Nominal.thy Fri Oct 12 21:51:25 2012 +0200 @@ -3376,7 +3376,7 @@ definition "ABS = ABS_set" -typedef (open) ('x,'a) ABS ("\_\_" [1000,1000] 1000) = +typedef ('x,'a) ABS ("\_\_" [1000,1000] 1000) = "ABS::('x\('a noption)) set" morphisms Rep_ABS Abs_ABS unfolding ABS_def diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/Nominal/nominal_datatype.ML --- a/src/HOL/Nominal/nominal_datatype.ML Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/Nominal/nominal_datatype.ML Fri Oct 12 21:51:25 2012 +0200 @@ -572,7 +572,7 @@ val (typedefs, thy6) = thy4 |> fold_map (fn (((name, mx), tvs), (cname, U)) => fn thy => - Typedef.add_typedef_global false NONE + Typedef.add_typedef_global (name, map (fn (v, _) => (v, dummyS)) tvs, mx) (* FIXME keep constraints!? *) (Const (@{const_name Collect}, (U --> HOLogic.boolT) --> HOLogic.mk_setT U) $ Const (cname, U --> HOLogic.boolT)) NONE diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/Probability/Sigma_Algebra.thy --- a/src/HOL/Probability/Sigma_Algebra.thy Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/Probability/Sigma_Algebra.thy Fri Oct 12 21:51:25 2012 +0200 @@ -997,7 +997,7 @@ definition measure_space :: "'a set \ 'a set set \ ('a set \ ereal) \ bool" where "measure_space \ A \ \ sigma_algebra \ A \ positive A \ \ countably_additive A \" -typedef (open) 'a measure = "{(\::'a set, A, \). (\a\-A. \ a = 0) \ measure_space \ A \ }" +typedef 'a measure = "{(\::'a set, A, \). (\a\-A. \ a = 0) \ measure_space \ A \ }" proof have "sigma_algebra UNIV {{}, UNIV}" by (auto simp: sigma_algebra_iff2) diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/Product_Type.thy --- a/src/HOL/Product_Type.thy Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/Product_Type.thy Fri Oct 12 21:51:25 2012 +0200 @@ -43,7 +43,7 @@ subsection {* The @{text unit} type *} -typedef (open) unit = "{True}" +typedef unit = "{True}" by auto definition Unity :: unit ("'(')") @@ -132,7 +132,7 @@ definition "prod = {f. \a b. f = Pair_Rep (a\'a) (b\'b)}" -typedef (open) ('a, 'b) prod (infixr "*" 20) = "prod :: ('a \ 'b \ bool) set" +typedef ('a, 'b) prod (infixr "*" 20) = "prod :: ('a \ 'b \ bool) set" unfolding prod_def by auto type_notation (xsymbols) diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/Quickcheck_Narrowing.thy --- a/src/HOL/Quickcheck_Narrowing.thy Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/Quickcheck_Narrowing.thy Fri Oct 12 21:51:25 2012 +0200 @@ -25,7 +25,7 @@ subsubsection {* Type @{text "code_int"} for Haskell Quickcheck's Int type *} -typedef (open) code_int = "UNIV \ int set" +typedef code_int = "UNIV \ int set" morphisms int_of of_int by rule lemma of_int_int_of [simp]: diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/Quotient_Examples/Lift_DList.thy --- a/src/HOL/Quotient_Examples/Lift_DList.thy Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/Quotient_Examples/Lift_DList.thy Fri Oct 12 21:51:25 2012 +0200 @@ -8,7 +8,7 @@ subsection {* The type of distinct lists *} -typedef (open) 'a dlist = "{xs::'a list. distinct xs}" +typedef 'a dlist = "{xs::'a list. distinct xs}" morphisms list_of_dlist Abs_dlist proof show "[] \ {xs. distinct xs}" by simp diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/Quotient_Examples/Lift_Set.thy --- a/src/HOL/Quotient_Examples/Lift_Set.thy Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/Quotient_Examples/Lift_Set.thy Fri Oct 12 21:51:25 2012 +0200 @@ -10,7 +10,7 @@ definition set where "set = (UNIV :: ('a \ bool) set)" -typedef (open) 'a set = "set :: ('a \ bool) set" +typedef 'a set = "set :: ('a \ bool) set" morphisms member Set unfolding set_def by auto diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/SMT_Examples/SMT_Tests.thy --- a/src/HOL/SMT_Examples/SMT_Tests.thy Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/SMT_Examples/SMT_Tests.thy Fri Oct 12 21:51:25 2012 +0200 @@ -760,7 +760,7 @@ definition "three = {1, 2, 3::int}" -typedef (open) three = three +typedef three = three unfolding three_def by auto definition n1 where "n1 = Abs_three 1" diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/String.thy --- a/src/HOL/String.thy Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/String.thy Fri Oct 12 21:51:25 2012 +0200 @@ -152,7 +152,7 @@ subsection {* Strings as dedicated type *} -typedef (open) literal = "UNIV :: string set" +typedef literal = "UNIV :: string set" morphisms explode STR .. instantiation literal :: size diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/Sum_Type.thy --- a/src/HOL/Sum_Type.thy Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/Sum_Type.thy Fri Oct 12 21:51:25 2012 +0200 @@ -19,7 +19,7 @@ definition "sum = {f. (\a. f = Inl_Rep (a::'a)) \ (\b. f = Inr_Rep (b::'b))}" -typedef (open) ('a, 'b) sum (infixr "+" 10) = "sum :: ('a => 'b => bool => bool) set" +typedef ('a, 'b) sum (infixr "+" 10) = "sum :: ('a => 'b => bool => bool) set" unfolding sum_def by auto lemma Inl_RepI: "Inl_Rep a \ sum" diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/Tools/Datatype/datatype.ML --- a/src/HOL/Tools/Datatype/datatype.ML Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/Tools/Datatype/datatype.ML Fri Oct 12 21:51:25 2012 +0200 @@ -190,7 +190,7 @@ |> Sign.parent_path |> fold_map (fn (((name, mx), tvs), c) => - Typedef.add_typedef_global false NONE (name, tvs, mx) + Typedef.add_typedef_global (name, tvs, mx) (Collect $ Const (c, UnivT')) NONE (rtac exI 1 THEN rtac CollectI 1 THEN QUIET_BREADTH_FIRST (has_fewer_prems 1) diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Oct 12 21:51:25 2012 +0200 @@ -559,15 +559,13 @@ type typedef_info = {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string, - set_def: thm option, prop_of_Rep: thm, set_name: string, - Abs_inverse: thm option, Rep_inverse: thm option} + prop_of_Rep: thm, set_name: string, Abs_inverse: thm option, Rep_inverse: thm option} fun typedef_info ctxt s = if is_frac_type ctxt (Type (s, [])) then SOME {abs_type = Type (s, []), rep_type = @{typ "int * int"}, Abs_name = @{const_name Nitpick.Abs_Frac}, Rep_name = @{const_name Nitpick.Rep_Frac}, - set_def = NONE, prop_of_Rep = @{prop "Nitpick.Rep_Frac x \ Collect Nitpick.Frac"} |> Logic.varify_global, set_name = @{const_name Nitpick.Frac}, Abs_inverse = NONE, @@ -579,10 +577,10 @@ types's type variables sometimes clash with locally fixed type variables. Remove these calls once "Typedef" is fully localized. *) ({abs_type, rep_type, Abs_name, Rep_name, ...}, - {set_def, Rep, Abs_inverse, Rep_inverse, ...}) :: _ => + {Rep, Abs_inverse, Rep_inverse, ...}) :: _ => SOME {abs_type = Logic.varifyT_global abs_type, rep_type = Logic.varifyT_global rep_type, Abs_name = Abs_name, - Rep_name = Rep_name, set_def = set_def, prop_of_Rep = prop_of Rep, + Rep_name = Rep_name, prop_of_Rep = prop_of Rep, set_name = set_prefix ^ s, Abs_inverse = SOME Abs_inverse, Rep_inverse = SOME Rep_inverse} | _ => NONE @@ -683,13 +681,10 @@ | is_pure_typedef _ _ = false fun is_univ_typedef ctxt (Type (s, _)) = (case typedef_info ctxt s of - SOME {set_def, prop_of_Rep, ...} => + SOME {prop_of_Rep, ...} => let val t_opt = - case set_def of - SOME thm => try (snd o Logic.dest_equals o prop_of) thm - | NONE => try (snd o HOLogic.dest_mem o HOLogic.dest_Trueprop) - prop_of_Rep + try (snd o HOLogic.dest_mem o HOLogic.dest_Trueprop) prop_of_Rep in case t_opt of SOME (Const (@{const_name top}, _)) => true diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/Tools/Quotient/quotient_type.ML --- a/src/HOL/Tools/Quotient/quotient_type.ML Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/Tools/Quotient/quotient_type.ML Fri Oct 12 21:51:25 2012 +0200 @@ -45,7 +45,7 @@ val typedef_tac = EVERY1 (map rtac [@{thm part_equivp_typedef}, equiv_thm]) in - Typedef.add_typedef false NONE (qty_name, map (rpair dummyS) vs, mx) + Typedef.add_typedef (qty_name, map (rpair dummyS) vs, mx) (typedef_term rel rty lthy) NONE typedef_tac lthy end diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/Tools/record.ML Fri Oct 12 21:51:25 2012 +0200 @@ -112,7 +112,7 @@ val vs = map (Proof_Context.check_tfree ctxt) raw_vs; in thy - |> Typedef.add_typedef_global false (SOME raw_tyco) (raw_tyco, vs, NoSyn) + |> Typedef.add_typedef_global (raw_tyco, vs, NoSyn) (HOLogic.mk_UNIV repT) NONE (rtac UNIV_witness 1) |-> (fn (tyco, info) => get_typedef_info tyco vs info) end; diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/Tools/typedef.ML --- a/src/HOL/Tools/typedef.ML Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/Tools/typedef.ML Fri Oct 12 21:51:25 2012 +0200 @@ -9,21 +9,21 @@ sig type info = {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string, axiom_name: string} * - {inhabited: thm, type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm, - Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm, + {inhabited: thm, type_definition: thm, Rep: thm, Rep_inverse: thm, Abs_inverse: thm, + Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm, Rep_induct: thm, Abs_induct: thm} val transform_info: morphism -> info -> info val get_info: Proof.context -> string -> info list val get_info_global: theory -> string -> info list val interpretation: (string -> theory -> theory) -> theory -> theory val setup: theory -> theory - val add_typedef: bool -> binding option -> binding * (string * sort) list * mixfix -> + val add_typedef: binding * (string * sort) list * mixfix -> term -> (binding * binding) option -> tactic -> local_theory -> (string * info) * local_theory - val add_typedef_global: bool -> binding option -> binding * (string * sort) list * mixfix -> + val add_typedef_global: binding * (string * sort) list * mixfix -> term -> (binding * binding) option -> tactic -> theory -> (string * info) * theory - val typedef: (bool * binding) * (binding * (string * sort) list * mixfix) * term * + val typedef: (binding * (string * sort) list * mixfix) * term * (binding * binding) option -> local_theory -> Proof.state - val typedef_cmd: (bool * binding) * (binding * (string * string option) list * mixfix) * string * + val typedef_cmd: (binding * (string * string option) list * mixfix) * string * (binding * binding) option -> local_theory -> Proof.state end; @@ -38,23 +38,22 @@ (*global part*) {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string, axiom_name: string} * (*local part*) - {inhabited: thm, type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm, - Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm, + {inhabited: thm, type_definition: thm, Rep: thm, Rep_inverse: thm, Abs_inverse: thm, + Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm, Rep_induct: thm, Abs_induct: thm}; fun transform_info phi (info: info) = let val thm = Morphism.thm phi; - val (global_info, {inhabited, type_definition, - set_def, Rep, Rep_inverse, Abs_inverse, Rep_inject, Abs_inject, - Rep_cases, Abs_cases, Rep_induct, Abs_induct}) = info; + val (global_info, {inhabited, type_definition, Rep, Rep_inverse, Abs_inverse, + Rep_inject, Abs_inject, Rep_cases, Abs_cases, Rep_induct, Abs_induct}) = info; in (global_info, {inhabited = thm inhabited, type_definition = thm type_definition, - set_def = Option.map thm set_def, Rep = thm Rep, Rep_inverse = thm Rep_inverse, - Abs_inverse = thm Abs_inverse, Rep_inject = thm Rep_inject, Abs_inject = thm Abs_inject, - Rep_cases = thm Rep_cases, Abs_cases = thm Abs_cases, Rep_induct = thm Rep_induct, - Abs_induct = thm Abs_induct}) + Rep = thm Rep, Rep_inverse = thm Rep_inverse, Abs_inverse = thm Abs_inverse, + Rep_inject = thm Rep_inject, Abs_inject = thm Abs_inject, + Rep_cases = thm Rep_cases, Abs_cases = thm Abs_cases, + Rep_induct = thm Rep_induct, Abs_induct = thm Abs_induct}) end; structure Data = Generic_Data @@ -129,9 +128,8 @@ (* prepare_typedef *) -fun prepare_typedef prep_term def_set name (tname, raw_args, mx) raw_set opt_morphs lthy = +fun prepare_typedef prep_term (name, raw_args, mx) raw_set opt_morphs lthy = let - val full_name = Local_Theory.full_name lthy name; val bname = Binding.name_of name; @@ -153,23 +151,13 @@ val args = map (Proof_Context.check_tfree tmp_ctxt') raw_args; val (newT, typedecl_lthy) = lthy - |> Typedecl.typedecl (tname, args, mx) + |> Typedecl.typedecl (name, args, mx) ||> Variable.declare_term set; - val Type (full_tname, type_args) = newT; + val Type (full_name, type_args) = newT; val lhs_tfrees = map Term.dest_TFree type_args; - (* set definition *) - - val ((set', set_def), set_lthy) = - if def_set then - typedecl_lthy - |> Local_Theory.define ((name, NoSyn), ((Thm.def_binding name, []), set)) - |>> (fn (set', (_, set_def)) => (set', SOME set_def)) - else ((set, NONE), typedecl_lthy); - - (* axiomatization *) val (Rep_name, Abs_name) = @@ -179,21 +167,8 @@ val typedef_name = Binding.prefix_name "type_definition_" name; - val ((RepC, AbsC, axiom_name, typedef), typedef_lthy) = - let - val thy = Proof_Context.theory_of set_lthy; - val cert = Thm.cterm_of thy; - val ((defs, _), A) = - Local_Defs.export_cterm set_lthy (Proof_Context.init_global thy) (cert set') - ||> Thm.term_of; - - val ((RepC, AbsC, axiom_name, axiom), axiom_lthy) = set_lthy - |> primitive_typedef typedef_name newT oldT Rep_name Abs_name A; - - val cert = Thm.cterm_of (Proof_Context.theory_of axiom_lthy); - val typedef = - Local_Defs.contract defs (cert (mk_typedef newT oldT RepC AbsC set')) axiom; - in ((RepC, AbsC, axiom_name, typedef), axiom_lthy) end; + val ((RepC, AbsC, axiom_name, typedef), typedef_lthy) = typedecl_lthy + |> primitive_typedef typedef_name newT oldT Rep_name Abs_name set; val alias_lthy = typedef_lthy |> Local_Theory.const_alias Rep_name (#1 (Term.dest_Const RepC)) @@ -209,9 +184,7 @@ fun typedef_result inhabited lthy1 = let val cert = Thm.cterm_of (Proof_Context.theory_of lthy1); - val inhabited' = - Local_Defs.contract (the_list set_def) (cert (mk_inhabited set')) inhabited; - val typedef' = inhabited' RS typedef; + val typedef' = inhabited RS typedef; fun make th = Goal.norm_result (typedef' RS th); val (((((((((((_, [type_definition]), Rep), Rep_inverse), Abs_inverse), Rep_inject), Abs_inject), Rep_cases), Abs_cases), Rep_induct), Abs_induct), lthy2) = lthy1 @@ -229,28 +202,28 @@ [Rule_Cases.case_names [Binding.name_of Rep_name], Induct.cases_pred full_name]), make @{thm type_definition.Rep_cases}) ||>> note_qualify ((Binding.suffix_name "_cases" Abs_name, - [Rule_Cases.case_names [Binding.name_of Abs_name], Induct.cases_type full_tname]), + [Rule_Cases.case_names [Binding.name_of Abs_name], Induct.cases_type full_name]), make @{thm type_definition.Abs_cases}) ||>> note_qualify ((Binding.suffix_name "_induct" Rep_name, [Rule_Cases.case_names [Binding.name_of Rep_name], Induct.induct_pred full_name]), make @{thm type_definition.Rep_induct}) ||>> note_qualify ((Binding.suffix_name "_induct" Abs_name, - [Rule_Cases.case_names [Binding.name_of Abs_name], Induct.induct_type full_tname]), + [Rule_Cases.case_names [Binding.name_of Abs_name], Induct.induct_type full_name]), make @{thm type_definition.Abs_induct}); val info = ({rep_type = oldT, abs_type = newT, Rep_name = #1 (Term.dest_Const RepC), Abs_name = #1 (Term.dest_Const AbsC), axiom_name = axiom_name}, - {inhabited = inhabited, type_definition = type_definition, set_def = set_def, + {inhabited = inhabited, type_definition = type_definition, Rep = Rep, Rep_inverse = Rep_inverse, Abs_inverse = Abs_inverse, Rep_inject = Rep_inject, Abs_inject = Abs_inject, Rep_cases = Rep_cases, Abs_cases = Abs_cases, Rep_induct = Rep_induct, Abs_induct = Abs_induct}); in lthy2 |> Local_Theory.declaration {syntax = false, pervasive = true} - (fn phi => put_info full_tname (transform_info phi info)) - |> Local_Theory.background_theory (Typedef_Interpretation.data full_tname) - |> pair (full_tname, info) + (fn phi => put_info full_name (transform_info phi info)) + |> Local_Theory.background_theory (Typedef_Interpretation.data full_name) + |> pair (full_name, info) end; in ((goal, goal_pat, typedef_result), alias_lthy) end @@ -260,19 +233,18 @@ (* add_typedef: tactic interface *) -fun add_typedef def opt_name typ set opt_morphs tac lthy = +fun add_typedef typ set opt_morphs tac lthy = let - val name = the_default (#1 typ) opt_name; val ((goal, _, typedef_result), lthy') = - prepare_typedef Syntax.check_term def name typ set opt_morphs lthy; + prepare_typedef Syntax.check_term typ set opt_morphs lthy; val inhabited = Goal.prove lthy' [] [] goal (K tac) |> Goal.norm_result |> Thm.close_derivation; in typedef_result inhabited lthy' end; -fun add_typedef_global def opt_name typ set opt_morphs tac = +fun add_typedef_global typ set opt_morphs tac = Named_Target.theory_init - #> add_typedef def opt_name typ set opt_morphs tac + #> add_typedef typ set opt_morphs tac #> Local_Theory.exit_result_global (apsnd o transform_info); @@ -280,11 +252,11 @@ local -fun gen_typedef prep_term prep_constraint ((def, name), (b, raw_args, mx), set, opt_morphs) lthy = +fun gen_typedef prep_term prep_constraint ((b, raw_args, mx), set, opt_morphs) lthy = let val args = map (apsnd (prep_constraint lthy)) raw_args; val ((goal, goal_pat, typedef_result), lthy') = - prepare_typedef prep_term def name (b, args, mx) set opt_morphs lthy; + prepare_typedef prep_term (b, args, mx) set opt_morphs lthy; fun after_qed [[th]] = snd o typedef_result th; in Proof.theorem NONE after_qed [[(goal, [goal_pat])]] lthy' end; @@ -302,17 +274,10 @@ val _ = Outer_Syntax.local_theory_to_proof @{command_spec "typedef"} "HOL type definition (requires non-emptiness proof)" - (Scan.optional (@{keyword "("} |-- - ((@{keyword "open"} >> K false) -- Scan.option Parse.binding || - Parse.binding >> (fn s => (true, SOME s))) --| @{keyword ")"}) (true, NONE) -- - (Parse.type_args_constrained -- Parse.binding) -- - Parse.opt_mixfix -- (@{keyword "="} |-- Parse.term) -- - Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding)) - >> (fn ((((((def, opt_name), (args, t)), mx), A), morphs)) => fn lthy => - (if def then - legacy_feature "typedef with implicit set definition -- use \"typedef (open)\" instead" - else (); - typedef_cmd ((def, the_default t opt_name), (t, args, mx), A, morphs) lthy))); + (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), morphs) => fn lthy => typedef_cmd ((t, vs, mx), A, morphs) lthy)); end; diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/UNITY/UNITY.thy --- a/src/HOL/UNITY/UNITY.thy Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/UNITY/UNITY.thy Fri Oct 12 21:51:25 2012 +0200 @@ -17,7 +17,7 @@ {(init:: 'a set, acts :: ('a * 'a)set set, allowed :: ('a * 'a)set set). Id \ acts & Id: allowed}" -typedef (open) 'a program = "Program :: ('a set * ('a * 'a) set set * ('a * 'a) set set) set" +typedef 'a program = "Program :: ('a set * ('a * 'a) set set * ('a * 'a) set set) set" morphisms Rep_Program Abs_Program unfolding Program_def by blast diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/Word/Word.thy --- a/src/HOL/Word/Word.thy Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/Word/Word.thy Fri Oct 12 21:51:25 2012 +0200 @@ -16,7 +16,7 @@ subsection {* Type definition *} -typedef (open) 'a word = "{(0::int) ..< 2^len_of TYPE('a::len0)}" +typedef 'a word = "{(0::int) ..< 2^len_of TYPE('a::len0)}" morphisms uint Abs_word by auto lemma uint_nonnegative: diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/ZF/Games.thy --- a/src/HOL/ZF/Games.thy Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/ZF/Games.thy Fri Oct 12 21:51:25 2012 +0200 @@ -191,7 +191,7 @@ definition "game = games_lfp" -typedef (open) game = game +typedef game = game unfolding game_def by (blast intro: games_lfp_nonempty) definition left_options :: "game \ game zet" where @@ -843,7 +843,7 @@ definition "Pg = UNIV//eq_game_rel" -typedef (open) Pg = Pg +typedef Pg = Pg unfolding Pg_def by (auto simp add: quotient_def) lemma equiv_eq_game[simp]: "equiv UNIV eq_game_rel" diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/ZF/Zet.thy --- a/src/HOL/ZF/Zet.thy Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/ZF/Zet.thy Fri Oct 12 21:51:25 2012 +0200 @@ -11,7 +11,7 @@ definition "zet = {A :: 'a set | A f z. inj_on f A \ f ` A \ explode z}" -typedef (open) 'a zet = "zet :: 'a set set" +typedef 'a zet = "zet :: 'a set set" unfolding zet_def by blast definition zin :: "'a \ 'a zet \ bool" where diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/ex/Dedekind_Real.thy --- a/src/HOL/ex/Dedekind_Real.thy Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/ex/Dedekind_Real.thy Fri Oct 12 21:51:25 2012 +0200 @@ -46,7 +46,7 @@ definition "preal = {A. cut A}" -typedef (open) preal = preal +typedef preal = preal unfolding preal_def by (blast intro: cut_of_rat [OF zero_less_one]) definition @@ -1171,7 +1171,7 @@ definition "Real = UNIV//realrel" -typedef (open) real = Real +typedef real = Real morphisms Rep_Real Abs_Real unfolding Real_def by (auto simp add: quotient_def) diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/ex/Executable_Relation.thy --- a/src/HOL/ex/Executable_Relation.thy Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/ex/Executable_Relation.thy Fri Oct 12 21:51:25 2012 +0200 @@ -6,7 +6,7 @@ subsubsection {* Definition of the dedicated type for relations *} -typedef (open) 'a rel = "UNIV :: (('a * 'a) set) set" +typedef 'a rel = "UNIV :: (('a * 'a) set) set" morphisms set_of_rel rel_of_set by simp setup_lifting type_definition_rel diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/ex/PER.thy --- a/src/HOL/ex/PER.thy Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/ex/PER.thy Fri Oct 12 21:51:25 2012 +0200 @@ -153,7 +153,7 @@ definition "quot = {{x. a \ x}| a::'a::partial_equiv. True}" -typedef (open) 'a quot = "quot :: 'a::partial_equiv set set" +typedef 'a quot = "quot :: 'a::partial_equiv set set" unfolding quot_def by blast lemma quotI [intro]: "{x. a \ x} \ quot" diff -r 9cbec40e88ea -r 2328a5197e77 src/HOL/ex/Refute_Examples.thy --- a/src/HOL/ex/Refute_Examples.thy Fri Oct 12 15:52:55 2012 +0200 +++ b/src/HOL/ex/Refute_Examples.thy Fri Oct 12 21:51:25 2012 +0200 @@ -485,7 +485,7 @@ definition "myTdef = insert (undefined::'a) (undefined::'a set)" -typedef (open) 'a myTdef = "myTdef :: 'a set" +typedef 'a myTdef = "myTdef :: 'a set" unfolding myTdef_def by auto lemma "(x::'a myTdef) = y" @@ -496,7 +496,7 @@ definition "T_bij = {(f::'a\'a). \y. \!x. f x = y}" -typedef (open) 'a T_bij = "T_bij :: ('a \ 'a) set" +typedef 'a T_bij = "T_bij :: ('a \ 'a) set" unfolding T_bij_def by auto lemma "P (f::(myTdecl myTdef) T_bij)"