--- 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
--- 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)"
--- 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
--- 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 (\<lambda>_. 0::'a)" by (rule boundI) (rule refl)
--- 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 \<equiv> Rep_cset"
--- 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
--- 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;
--- 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;
--- 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
--- 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 \<Colon> nat set"
+typedef code_numeral = "UNIV \<Colon> nat set"
morphisms nat_of of_nat ..
lemma of_nat_nat_of [simp]:
--- 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
--- 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 \<rightarrow> 'a. finite_deflation d}"
+typedef 'a fin_defl = "{d::'a \<rightarrow> '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
--- 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 \<and> S \<noteq> {}}"
-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
--- 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)
--- 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)
--- 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
--- 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
--- 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)"
--- 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)
--- 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))
--- 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)
--- 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)
--- 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)
--- 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
--- 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 \<times> 'value) list. (distinct o map fst) xs}"
+typedef ('key, 'value) alist = "{xs :: ('key \<times> 'value) list. (distinct o map fst) xs}"
morphisms impl_of Alist
proof
show "[] \<in> {xs. (distinct o map fst) xs}" by simp
--- 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 "[] \<in> {xs. distinct xs}" by simp
--- 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 \<Rightarrow> enat" where
"enat n = Abs_enat (Some n)"
--- 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\<Rightarrow>'b. \<exists>b. finite {a. f a \<noteq> 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 "\<exists>f. finite {x. f x \<noteq> undefined}"
--- 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
--- 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 \<Rightarrow> 'a. True}"
+typedef 'a fps = "{f :: nat \<Rightarrow> 'a. True}"
morphisms fps_nth Abs_fps
by simp
--- 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\<times>'a). snd x \<noteq> (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) \<in> {x. snd x \<noteq> 0}" by simp
--- 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 \<rightharpoonup> 'b) set"
+typedef ('a, 'b) mapping = "UNIV :: ('a \<rightharpoonup> 'b) set"
morphisms lookup Mapping ..
lemma lookup_Mapping [simp]:
--- 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
--- 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 \<in> {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 \<in> {0 ..< 1 + 2 * int CARD('a)}"
by simp
--- 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 \<Rightarrow> 'a::zero. \<exists>n. \<forall>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
--- 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 \<sim> 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 \<sim> x} \<in> quot"
--- 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\<Colon>linorder, 'b) RBT_Impl.rbt. is_rbt t}"
+typedef ('a, 'b) rbt = "{t :: ('a\<Colon>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 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
--- 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 \<Colon> int set"
+typedef int = "UNIV \<Colon> int set"
morphisms int_of of_int ..
hide_type (open) int
--- 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 (\<lambda>x. P x) \<Longrightarrow> F (\<lambda>x. Q x) \<Longrightarrow> F (\<lambda>x. P x \<and> Q x)"
assumes mono: "\<forall>x. P x \<longrightarrow> Q x \<Longrightarrow> F (\<lambda>x. P x) \<Longrightarrow> F (\<lambda>x. Q x)"
-typedef (open) 'a filter = "{F :: ('a \<Rightarrow> bool) \<Rightarrow> bool. is_filter F}"
+typedef 'a filter = "{F :: ('a \<Rightarrow> bool) \<Rightarrow> bool. is_filter F}"
proof
show "(\<lambda>x. True) \<in> ?filter" by (auto intro: is_filter.intro)
qed
--- 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 \<Rightarrow> nat \<Rightarrow> 'a::zero)). finite (nonzero_positions f)}"
-typedef (open) 'a matrix = "matrix :: (nat \<Rightarrow> nat \<Rightarrow> 'a::zero) set"
+typedef '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/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) \<Rightarrow> 'a) set"
+typedef ('a, 'b) vec = "UNIV :: (('b::finite) \<Rightarrow> 'a) set"
morphisms vec_nth vec_lambda ..
notation
--- 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 \<longleftrightarrow> L {} \<and> (\<forall>S T. L S \<longrightarrow> L T \<longrightarrow> L (S \<inter> T)) \<and> (\<forall>K. Ball K L \<longrightarrow> L (\<Union> K))"
-typedef (open) 'a topology = "{L::('a set) \<Rightarrow> bool. istopology L}"
+typedef 'a topology = "{L::('a set) \<Rightarrow> bool. istopology L}"
morphisms "openin" "topology"
unfolding istopology_def by blast
--- 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 \<Rightarrow> 'a) set) // starrel"
-typedef (open) 'a star = "star :: (nat \<Rightarrow> 'a) set set"
+typedef 'a star = "star :: (nat \<Rightarrow> 'a) set set"
unfolding star_def by (auto intro: quotientI)
definition
--- 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 \<Longrightarrow> 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
--- 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\<Colon>nat, 1, 2}"
-typedef (open) three = three
+typedef three = three
unfolding three_def by blast
definition A :: three where "A \<equiv> Abs_three 0"
@@ -201,7 +201,7 @@
(* BEGIN LAZY LIST SETUP *)
definition "llist = (UNIV\<Colon>('a list + (nat \<Rightarrow> 'a)) set)"
-typedef (open) 'a llist = "llist\<Colon>('a list + (nat \<Rightarrow> 'a)) set"
+typedef 'a llist = "llist\<Colon>('a list + (nat \<Rightarrow> 'a)) set"
unfolding llist_def by auto
definition LNil where
--- 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\<Colon>'a myTdef) = y"
@@ -552,7 +552,7 @@
definition "T_bij = {(f::'a\<Rightarrow>'a). \<forall>y. \<exists>!x. f x = y}"
-typedef (open) 'a T_bij = "T_bij :: ('a \<Rightarrow> 'a) set"
+typedef 'a T_bij = "T_bij :: ('a \<Rightarrow> 'a) set"
unfolding T_bij_def by auto
lemma "P (f\<Colon>(myTdecl myTdef) T_bij)"
--- 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\<Colon>nat, 1, 2}"
-typedef (open) three = three
+typedef three = three
unfolding three_def by blast
definition A :: three where "A \<equiv> Abs_three 0"
@@ -28,7 +28,7 @@
definition "one_or_two = {undefined False\<Colon>'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\<Colon>unit one_or_two)"
@@ -54,7 +54,7 @@
definition "bounded = {n\<Colon>nat. finite (UNIV \<Colon> 'a set) \<longrightarrow> n < card (UNIV \<Colon> '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")
--- 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 ("\<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 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
--- 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 \<Rightarrow> 'a set set \<Rightarrow> ('a set \<Rightarrow> ereal) \<Rightarrow> bool" where
"measure_space \<Omega> A \<mu> \<longleftrightarrow> sigma_algebra \<Omega> A \<and> positive A \<mu> \<and> countably_additive A \<mu>"
-typedef (open) 'a measure = "{(\<Omega>::'a set, A, \<mu>). (\<forall>a\<in>-A. \<mu> a = 0) \<and> measure_space \<Omega> A \<mu> }"
+typedef 'a measure = "{(\<Omega>::'a set, A, \<mu>). (\<forall>a\<in>-A. \<mu> a = 0) \<and> measure_space \<Omega> A \<mu> }"
proof
have "sigma_algebra UNIV {{}, UNIV}"
by (auto simp: sigma_algebra_iff2)
--- 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. \<exists>a b. f = Pair_Rep (a\<Colon>'a) (b\<Colon>'b)}"
-typedef (open) ('a, 'b) prod (infixr "*" 20) = "prod :: ('a \<Rightarrow> 'b \<Rightarrow> bool) set"
+typedef ('a, 'b) prod (infixr "*" 20) = "prod :: ('a \<Rightarrow> 'b \<Rightarrow> bool) set"
unfolding prod_def by auto
type_notation (xsymbols)
--- 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 \<Colon> int set"
+typedef code_int = "UNIV \<Colon> int set"
morphisms int_of of_int by rule
lemma of_int_int_of [simp]:
--- 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 "[] \<in> {xs. distinct xs}" by simp
--- 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 \<Rightarrow> bool) set)"
-typedef (open) 'a set = "set :: ('a \<Rightarrow> bool) set"
+typedef 'a set = "set :: ('a \<Rightarrow> bool) set"
morphisms member Set
unfolding set_def by auto
--- 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"
--- 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
--- 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. (\<exists>a. f = Inl_Rep (a::'a)) \<or> (\<exists>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 \<in> sum"
--- 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)
--- 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 \<in> 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
--- 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
--- 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;
--- 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;
--- 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 \<in> 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
--- 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:
--- 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 \<Rightarrow> 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"
--- 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 \<and> f ` A \<subseteq> 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 \<Rightarrow> 'a zet \<Rightarrow> bool" where
--- 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)
--- 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
--- 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 \<sim> 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 \<sim> x} \<in> quot"
--- 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\<Rightarrow>'a). \<forall>y. \<exists>!x. f x = y}"
-typedef (open) 'a T_bij = "T_bij :: ('a \<Rightarrow> 'a) set"
+typedef 'a T_bij = "T_bij :: ('a \<Rightarrow> 'a) set"
unfolding T_bij_def by auto
lemma "P (f::(myTdecl myTdef) T_bij)"