--- a/src/HOL/Algebra/poly/UnivPoly2.thy Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/Algebra/poly/UnivPoly2.thy Wed Nov 30 16:27:10 2011 +0100
@@ -39,9 +39,15 @@
with nonzero show ?thesis by contradiction
qed
-typedef (UP)
- ('a) up = "{f :: nat => 'a::zero. EX n. bound n f}"
- by (rule+) (* Question: what does trace_rule show??? *)
+
+definition "UP = {f :: nat => 'a::zero. EX n. bound n f}"
+
+typedef (open) 'a up = "UP :: (nat => 'a::zero) set"
+ morphisms Rep_UP Abs_UP
+proof -
+ have "bound 0 (\<lambda>_. 0::'a)" by (rule boundI) (rule refl)
+ then show ?thesis unfolding UP_def by blast
+qed
section {* Constants *}
--- a/src/HOL/Code_Numeral.thy Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/Code_Numeral.thy Wed Nov 30 16:27:10 2011 +0100
@@ -14,7 +14,7 @@
subsection {* Datatype of target language numerals *}
typedef (open) code_numeral = "UNIV \<Colon> nat set"
- morphisms nat_of of_nat by rule
+ morphisms nat_of of_nat ..
lemma of_nat_nat_of [simp]:
"of_nat (nat_of k) = k"
--- a/src/HOL/Datatype.thy Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/Datatype.thy Wed Nov 30 16:27:10 2011 +0100
@@ -21,10 +21,11 @@
subsection {* The datatype universe *}
-typedef (Node)
- ('a,'b) node = "{p. EX f x k. p = (f::nat=>'b+nat, x::'a+nat) & f k = Inr 0}"
- --{*it is a subtype of @{text "(nat=>'b+nat) * ('a+nat)"}*}
- by auto
+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"
+ morphisms Rep_Node Abs_Node
+ unfolding Node_def by auto
text{*Datatypes will be represented by sets of type @{text node}*}
--- a/src/HOL/HOLCF/Compact_Basis.thy Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/HOLCF/Compact_Basis.thy Wed Nov 30 16:27:10 2011 +0100
@@ -12,9 +12,13 @@
subsection {* A compact basis for powerdomains *}
-typedef 'a pd_basis =
- "{S::'a compact_basis set. finite S \<and> S \<noteq> {}}"
-by (rule_tac x="{arbitrary}" in exI, simp)
+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"
+ unfolding pd_basis_def
+ apply (rule_tac x="{arbitrary}" in exI)
+ apply simp
+ done
lemma finite_Rep_pd_basis [simp]: "finite (Rep_pd_basis u)"
by (insert Rep_pd_basis [of u, unfolded pd_basis_def]) simp
--- a/src/HOL/Induct/QuoDataType.thy Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/Induct/QuoDataType.thy Wed Nov 30 16:27:10 2011 +0100
@@ -123,8 +123,11 @@
subsection{*The Initial Algebra: A Quotiented Message Type*}
-typedef (Msg) msg = "UNIV//msgrel"
- by (auto simp add: quotient_def)
+definition "Msg = UNIV//msgrel"
+
+typedef (open) msg = Msg
+ morphisms Rep_Msg Abs_Msg
+ unfolding Msg_def by (auto simp add: quotient_def)
text{*The abstract message constructors*}
--- a/src/HOL/Induct/QuoNestedDataType.thy Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/Induct/QuoNestedDataType.thy Wed Nov 30 16:27:10 2011 +0100
@@ -142,9 +142,11 @@
subsection{*The Initial Algebra: A Quotiented Message Type*}
+definition "Exp = UNIV//exprel"
-typedef (Exp) exp = "UNIV//exprel"
- by (auto simp add: quotient_def)
+typedef (open) exp = Exp
+ morphisms Rep_Exp Abs_Exp
+ unfolding Exp_def by (auto simp add: quotient_def)
text{*The abstract message constructors*}
--- a/src/HOL/Induct/SList.thy Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/Induct/SList.thy Wed Nov 30 16:27:10 2011 +0100
@@ -53,9 +53,11 @@
| CONS_I: "[| a: A; M: list A |] ==> CONS a M : list A"
-typedef (List)
- 'a list = "list(range Leaf) :: 'a item set"
- by (blast intro: list.NIL_I)
+definition "List = list (range Leaf)"
+
+typedef (open) 'a list = "List :: 'a item set"
+ morphisms Rep_List Abs_List
+ unfolding List_def by (blast intro: list.NIL_I)
abbreviation "Case == Datatype.Case"
abbreviation "Split == Datatype.Split"
@@ -224,7 +226,7 @@
lemmas Cons_inject2 = Cons_Cons_eq [THEN iffD1, THEN conjE]
lemma CONS_D: "CONS M N: list(A) ==> M: A & N: list(A)"
- by (induct L == "CONS M N" set: list) auto
+ by (induct L == "CONS M N" rule: list.induct) auto
lemma sexp_CONS_D: "CONS M N: sexp ==> M: sexp & N: sexp"
apply (simp add: CONS_def In1_def)
--- a/src/HOL/Int.thy Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/Int.thy Wed Nov 30 16:27:10 2011 +0100
@@ -18,9 +18,11 @@
definition intrel :: "((nat \<times> nat) \<times> (nat \<times> nat)) set" where
"intrel = {((x, y), (u, v)) | x y u v. x + v = u +y }"
-typedef (Integ)
- int = "UNIV//intrel"
- by (auto simp add: quotient_def)
+definition "Integ = UNIV//intrel"
+
+typedef (open) int = Integ
+ morphisms Rep_Integ Abs_Integ
+ unfolding Integ_def by (auto simp add: quotient_def)
instantiation int :: "{zero, one, plus, minus, uminus, times, ord, abs, sgn}"
begin
--- a/src/HOL/Library/Dlist.thy Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/Library/Dlist.thy Wed Nov 30 16:27:10 2011 +0100
@@ -11,7 +11,7 @@
typedef (open) 'a dlist = "{xs::'a list. distinct xs}"
morphisms list_of_dlist Abs_dlist
proof
- show "[] \<in> ?dlist" by simp
+ show "[] \<in> {xs. distinct xs}" by simp
qed
lemma dlist_eq_iff:
--- a/src/HOL/Library/Fraction_Field.thy Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/Library/Fraction_Field.thy Wed Nov 30 16:27:10 2011 +0100
@@ -53,7 +53,10 @@
shows "fractrel `` {x} = fractrel `` {y} \<longleftrightarrow> (x, y) \<in> fractrel"
by (rule eq_equiv_class_iff, rule equiv_fractrel) (auto simp add: assms)
-typedef 'a fract = "{(x::'a\<times>'a). snd x \<noteq> (0::'a::idom)} // fractrel"
+definition "fract = {(x::'a\<times>'a). snd x \<noteq> (0::'a::idom)} // fractrel"
+
+typedef (open) '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
then show "fractrel `` {(0::'a, 1)} \<in> {x. snd x \<noteq> 0} // fractrel" by (rule quotientI)
--- a/src/HOL/Library/Multiset.thy Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/Library/Multiset.thy Wed Nov 30 16:27:10 2011 +0100
@@ -10,10 +10,13 @@
subsection {* The type of multisets *}
-typedef 'a multiset = "{f :: 'a => nat. finite {x. f x > 0}}"
+definition "multiset = {f :: 'a => nat. finite {x. f x > 0}}"
+
+typedef (open) 'a multiset = "multiset :: ('a => nat) set"
morphisms count Abs_multiset
+ unfolding multiset_def
proof
- show "(\<lambda>x. 0::nat) \<in> ?multiset" by simp
+ show "(\<lambda>x. 0::nat) \<in> {f. finite {x. f x > 0}}" by simp
qed
lemmas multiset_typedef = Abs_multiset_inverse count_inverse count
--- a/src/HOL/Library/Polynomial.thy Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/Library/Polynomial.thy Wed Nov 30 16:27:10 2011 +0100
@@ -11,15 +11,17 @@
subsection {* Definition of type @{text poly} *}
-typedef (Poly) 'a poly = "{f::nat \<Rightarrow> 'a::zero. \<exists>n. \<forall>i>n. f i = 0}"
+definition "Poly = {f::nat \<Rightarrow> 'a::zero. \<exists>n. \<forall>i>n. f i = 0}"
+
+typedef (open) 'a poly = "Poly :: (nat => 'a::zero) set"
morphisms coeff Abs_poly
- by auto
+ unfolding Poly_def by auto
lemma expand_poly_eq: "p = q \<longleftrightarrow> (\<forall>n. coeff p n = coeff q n)"
-by (simp add: coeff_inject [symmetric] fun_eq_iff)
+ by (simp add: coeff_inject [symmetric] fun_eq_iff)
lemma poly_ext: "(\<And>n. coeff p n = coeff q n) \<Longrightarrow> p = q"
-by (simp add: expand_poly_eq)
+ by (simp add: expand_poly_eq)
subsection {* Degree of a polynomial *}
--- a/src/HOL/Library/Quotient_Type.thy Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/Library/Quotient_Type.thy Wed Nov 30 16:27:10 2011 +0100
@@ -58,8 +58,10 @@
\emph{equivalence classes} over elements of the base type @{typ 'a}.
*}
-typedef 'a quot = "{{x. a \<sim> x} | a::'a::eqv. True}"
- by blast
+definition "quot = {{x. a \<sim> x} | a::'a::eqv. True}"
+
+typedef (open) 'a quot = "quot :: 'a::eqv set set"
+ unfolding quot_def by blast
lemma quotI [intro]: "{x. a \<sim> x} \<in> quot"
unfolding quot_def by blast
--- a/src/HOL/Library/RBT.thy Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/Library/RBT.thy Wed Nov 30 16:27:10 2011 +0100
@@ -11,9 +11,8 @@
typedef (open) ('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
- then show ?thesis ..
+proof
+ show "RBT_Impl.Empty \<in> {t. is_rbt t}" by simp
qed
lemma rbt_eq_iff:
--- a/src/HOL/Matrix/Matrix.thy Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/Matrix/Matrix.thy Wed Nov 30 16:27:10 2011 +0100
@@ -11,18 +11,19 @@
definition nonzero_positions :: "(nat \<Rightarrow> nat \<Rightarrow> 'a::zero) \<Rightarrow> (nat \<times> nat) set" where
"nonzero_positions A = {pos. A (fst pos) (snd pos) ~= 0}"
-typedef 'a matrix = "{(f::(nat \<Rightarrow> nat \<Rightarrow> 'a::zero)). finite (nonzero_positions f)}"
-proof -
- have "(\<lambda>j i. 0) \<in> {(f::(nat \<Rightarrow> nat \<Rightarrow> 'a::zero)). finite (nonzero_positions f)}"
+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"
+ unfolding matrix_def
+proof
+ show "(\<lambda>j i. 0) \<in> {(f::(nat \<Rightarrow> nat \<Rightarrow> 'a::zero)). finite (nonzero_positions f)}"
by (simp add: nonzero_positions_def)
- then show ?thesis by auto
qed
declare Rep_matrix_inverse[simp]
lemma finite_nonzero_positions : "finite (nonzero_positions (Rep_matrix A))"
-apply (rule Abs_matrix_induct)
-by (simp add: Abs_matrix_inverse matrix_def)
+ by (induct A) (simp add: Abs_matrix_inverse matrix_def)
definition nrows :: "('a::zero) matrix \<Rightarrow> nat" where
"nrows A == if nonzero_positions(Rep_matrix A) = {} then 0 else Suc(Max ((image fst) (nonzero_positions (Rep_matrix A))))"
--- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Wed Nov 30 16:27:10 2011 +0100
@@ -13,8 +13,7 @@
subsection {* Finite Cartesian products, with indexing and lambdas. *}
-typedef (open)
- ('a, 'b) vec = "UNIV :: (('b::finite) \<Rightarrow> 'a) set"
+typedef (open) ('a, 'b) vec = "UNIV :: (('b::finite) \<Rightarrow> 'a) set"
morphisms vec_nth vec_lambda ..
notation
--- a/src/HOL/NSA/StarDef.thy Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/NSA/StarDef.thy Wed Nov 30 16:27:10 2011 +0100
@@ -39,8 +39,10 @@
starrel :: "((nat \<Rightarrow> 'a) \<times> (nat \<Rightarrow> 'a)) set" where
"starrel = {(X,Y). {n. X n = Y n} \<in> \<U>}"
-typedef 'a star = "(UNIV :: (nat \<Rightarrow> 'a) set) // starrel"
-by (auto intro: quotientI)
+definition "star = (UNIV :: (nat \<Rightarrow> 'a) set) // starrel"
+
+typedef (open) 'a star = "star :: (nat \<Rightarrow> 'a) set set"
+ unfolding star_def by (auto intro: quotientI)
definition
star_n :: "(nat \<Rightarrow> 'a) \<Rightarrow> 'a star" where
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Wed Nov 30 16:27:10 2011 +0100
@@ -95,8 +95,9 @@
subsection {* 2.7. Typedefs, Records, Rationals, and Reals *}
-typedef three = "{0\<Colon>nat, 1, 2}"
-by blast
+definition "three = {0\<Colon>nat, 1, 2}"
+typedef (open) three = three
+unfolding three_def by blast
definition A :: three where "A \<equiv> Abs_three 0"
definition B :: three where "B \<equiv> Abs_three 1"
@@ -197,7 +198,10 @@
axiomatization. The examples also work unchanged with Lochbihler's
"Coinductive_List" theory. *)
-typedef 'a llist = "UNIV\<Colon>('a list + (nat \<Rightarrow> 'a)) set" by auto
+definition "llist = (UNIV\<Colon>('a list + (nat \<Rightarrow> 'a)) set)"
+
+typedef (open) 'a llist = "llist\<Colon>('a list + (nat \<Rightarrow> 'a)) set"
+unfolding llist_def by auto
definition LNil where
"LNil = Abs_llist (Inl [])"
--- a/src/HOL/Nitpick_Examples/Refute_Nits.thy Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy Wed Nov 30 16:27:10 2011 +0100
@@ -539,8 +539,10 @@
text {* A completely unspecified non-empty subset of @{typ "'a"}: *}
-typedef 'a myTdef = "insert (undefined\<Colon>'a) (undefined\<Colon>'a set)"
-by auto
+definition "myTdef = insert (undefined::'a) (undefined::'a set)"
+
+typedef (open) 'a myTdef = "myTdef :: 'a set"
+unfolding myTdef_def by auto
lemma "(x\<Colon>'a myTdef) = y"
nitpick [expect = genuine]
@@ -548,8 +550,10 @@
typedecl myTdecl
-typedef 'a T_bij = "{(f\<Colon>'a\<Rightarrow>'a). \<forall>y. \<exists>!x. f x = y}"
-by auto
+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"
+unfolding T_bij_def by auto
lemma "P (f\<Colon>(myTdecl myTdef) T_bij)"
nitpick [expect = genuine]
--- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy Wed Nov 30 16:27:10 2011 +0100
@@ -14,8 +14,9 @@
nitpick_params [verbose, card = 1\<emdash>4, sat_solver = MiniSat_JNI, max_threads = 1,
timeout = 240]
-typedef three = "{0\<Colon>nat, 1, 2}"
-by blast
+definition "three = {0\<Colon>nat, 1, 2}"
+typedef (open) three = three
+unfolding three_def by blast
definition A :: three where "A \<equiv> Abs_three 0"
definition B :: three where "B \<equiv> Abs_three 1"
@@ -25,8 +26,10 @@
nitpick [expect = genuine]
oops
-typedef 'a one_or_two = "{undefined False\<Colon>'a, undefined True}"
-by auto
+definition "one_or_two = {undefined False\<Colon>'a, undefined True}"
+
+typedef (open) 'a one_or_two = "one_or_two :: 'a set"
+unfolding one_or_two_def by auto
lemma "x = (y\<Colon>unit one_or_two)"
nitpick [expect = none]
@@ -49,8 +52,9 @@
nitpick [card = 2, expect = none]
oops
-typedef 'a bounded =
- "{n\<Colon>nat. finite (UNIV\<Colon>'a \<Rightarrow> bool) \<longrightarrow> n < card (UNIV\<Colon>'a \<Rightarrow> bool)}"
+definition "bounded = {n\<Colon>nat. finite (UNIV\<Colon>'a \<Rightarrow> bool) \<longrightarrow> n < card (UNIV\<Colon>'a \<Rightarrow> bool)}"
+typedef (open) 'a bounded = "bounded(TYPE('a))"
+unfolding bounded_def
apply (rule_tac x = 0 in exI)
apply (case_tac "card UNIV = 0")
by auto
--- a/src/HOL/Nominal/Nominal.thy Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/Nominal/Nominal.thy Wed Nov 30 16:27:10 2011 +0100
@@ -3395,8 +3395,12 @@
where
ABS_in: "(abs_fun a x)\<in>ABS_set"
-typedef (ABS) ('x,'a) ABS ("\<guillemotleft>_\<guillemotright>_" [1000,1000] 1000) =
- "ABS_set::('x\<Rightarrow>('a noption)) set"
+definition "ABS = ABS_set"
+
+typedef (open) ('x,'a) ABS ("\<guillemotleft>_\<guillemotright>_" [1000,1000] 1000) =
+ "ABS::('x\<Rightarrow>('a noption)) set"
+ morphisms Rep_ABS Abs_ABS
+ unfolding ABS_def
proof
fix x::"'a" and a::"'x"
show "(abs_fun a x)\<in> ABS_set" by (rule ABS_in)
--- a/src/HOL/Product_Type.thy Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/Product_Type.thy Wed Nov 30 16:27:10 2011 +0100
@@ -46,14 +46,10 @@
subsection {* The @{text unit} type *}
typedef (open) unit = "{True}"
-proof
- show "True : ?unit" ..
-qed
+ by auto
-definition
- Unity :: unit ("'(')")
-where
- "() = Abs_unit True"
+definition Unity :: unit ("'(')")
+ where "() = Abs_unit True"
lemma unit_eq [no_atp]: "u = ()"
by (induct u) (simp add: Unity_def)
@@ -136,12 +132,8 @@
definition Pair_Rep :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" where
"Pair_Rep a b = (\<lambda>x y. x = a \<and> y = b)"
-typedef ('a, 'b) prod (infixr "*" 20)
- = "{f. \<exists>a b. f = Pair_Rep (a\<Colon>'a) (b\<Colon>'b)}"
-proof
- fix a b show "Pair_Rep a b \<in> ?prod"
- by rule+
-qed
+typedef ('a, 'b) prod (infixr "*" 20) = "{f. \<exists>a b. f = Pair_Rep (a\<Colon>'a) (b\<Colon>'b)}"
+ by auto
type_notation (xsymbols)
"prod" ("(_ \<times>/ _)" [21, 20] 20)
--- a/src/HOL/Quotient_Examples/Lift_Set.thy Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/Quotient_Examples/Lift_Set.thy Wed Nov 30 16:27:10 2011 +0100
@@ -8,21 +8,29 @@
imports Main
begin
-typedef 'a set = "(UNIV :: ('a => bool) => bool)"
-morphisms member Set by auto
+definition set where "set = (UNIV :: ('a => bool) => bool)"
+
+typedef (open) 'a set = "set :: 'a set set"
+ morphisms member Set
+ unfolding set_def by auto
text {* Here is some ML setup that should eventually be incorporated in the typedef command. *}
local_setup {* fn lthy =>
-let
- val quotients = {qtyp = @{typ "'a set"}, rtyp = @{typ "'a => bool"}, equiv_rel = @{term "dummy"}, equiv_thm = @{thm refl}}
- val qty_full_name = @{type_name "set"}
+ let
+ val quotients =
+ {qtyp = @{typ "'a set"}, rtyp = @{typ "'a => bool"},
+ equiv_rel = @{term "dummy"}, equiv_thm = @{thm refl}}
+ val qty_full_name = @{type_name "set"}
- fun qinfo phi = Quotient_Info.transform_quotients phi quotients
- in lthy
+ fun qinfo phi = Quotient_Info.transform_quotients phi quotients
+ in
+ lthy
|> Local_Theory.declaration {syntax = false, pervasive = true}
- (fn phi => Quotient_Info.update_quotients qty_full_name (qinfo phi)
- #> Quotient_Info.update_abs_rep qty_full_name (Quotient_Info.transform_abs_rep phi {abs = @{term "Set"}, rep = @{term "member"}}))
+ (fn phi =>
+ Quotient_Info.update_quotients qty_full_name (qinfo phi) #>
+ Quotient_Info.update_abs_rep qty_full_name
+ (Quotient_Info.transform_abs_rep phi {abs = @{term "Set"}, rep = @{term "member"}}))
end
*}
--- a/src/HOL/Rat.thy Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/Rat.thy Wed Nov 30 16:27:10 2011 +0100
@@ -54,7 +54,11 @@
shows "ratrel `` {x} = ratrel `` {y} \<longleftrightarrow> (x, y) \<in> ratrel"
by (rule eq_equiv_class_iff, rule equiv_ratrel) (auto simp add: assms)
-typedef (Rat) rat = "{x. snd x \<noteq> 0} // ratrel"
+definition "Rat = {x. snd x \<noteq> 0} // ratrel"
+
+typedef (open) rat = Rat
+ morphisms Rep_Rat Abs_Rat
+ unfolding Rat_def
proof
have "(0::int, 1::int) \<in> {x. snd x \<noteq> 0}" by simp
then show "ratrel `` {(0, 1)} \<in> {x. snd x \<noteq> 0} // ratrel" by (rule quotientI)
--- a/src/HOL/SMT_Examples/SMT_Tests.thy Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/SMT_Examples/SMT_Tests.thy Wed Nov 30 16:27:10 2011 +0100
@@ -762,7 +762,10 @@
subsubsection {* Type definitions *}
-typedef three = "{1, 2, 3::int}" by auto
+definition "three = {1, 2, 3::int}"
+
+typedef (open) three = three
+ unfolding three_def by auto
definition n1 where "n1 = Abs_three 1"
definition n2 where "n2 = Abs_three 2"
--- a/src/HOL/Sum_Type.thy Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/Sum_Type.thy Wed Nov 30 16:27:10 2011 +0100
@@ -17,8 +17,10 @@
definition Inr_Rep :: "'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool \<Rightarrow> bool" where
"Inr_Rep b x y p \<longleftrightarrow> y = b \<and> \<not> p"
-typedef ('a, 'b) sum (infixr "+" 10) = "{f. (\<exists>a. f = Inl_Rep (a::'a)) \<or> (\<exists>b. f = Inr_Rep (b::'b))}"
- by auto
+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"
+ unfolding sum_def by auto
lemma Inl_RepI: "Inl_Rep a \<in> sum"
by (auto simp add: sum_def)
--- a/src/HOL/UNITY/UNITY.thy Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/UNITY/UNITY.thy Wed Nov 30 16:27:10 2011 +0100
@@ -12,10 +12,14 @@
theory UNITY imports Main begin
-typedef (Program)
- 'a program = "{(init:: 'a set, acts :: ('a * 'a)set set,
- allowed :: ('a * 'a)set set). Id \<in> acts & Id: allowed}"
- by blast
+definition
+ "Program =
+ {(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"
+ morphisms Rep_Program Abs_Program
+ unfolding Program_def by blast
definition Acts :: "'a program => ('a * 'a)set set" where
"Acts F == (%(init, acts, allowed). acts) (Rep_Program F)"
--- a/src/HOL/Word/Word.thy Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/Word/Word.thy Wed Nov 30 16:27:10 2011 +0100
@@ -17,7 +17,7 @@
subsection {* Type definition *}
-typedef (open word) 'a word = "{(0::int) ..< 2^len_of TYPE('a::len0)}"
+typedef (open) 'a word = "{(0::int) ..< 2^len_of TYPE('a::len0)}"
morphisms uint Abs_word by auto
definition word_of_int :: "int \<Rightarrow> 'a\<Colon>len0 word" where
--- a/src/HOL/ZF/Games.thy Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/ZF/Games.thy Wed Nov 30 16:27:10 2011 +0100
@@ -189,8 +189,10 @@
apply (simp add: games_lfp_unfold[symmetric])
done
-typedef game = games_lfp
- by (blast intro: games_lfp_nonempty)
+definition "game = games_lfp"
+
+typedef (open) game = game
+ unfolding game_def by (blast intro: games_lfp_nonempty)
definition left_options :: "game \<Rightarrow> game zet" where
"left_options g \<equiv> zimage Abs_game (zexplode (Fst (Rep_game g)))"
@@ -839,8 +841,10 @@
definition eq_game_rel :: "(game * game) set" where
"eq_game_rel \<equiv> { (p, q) . eq_game p q }"
-typedef Pg = "UNIV//eq_game_rel"
- by (auto simp add: quotient_def)
+definition "Pg = UNIV//eq_game_rel"
+
+typedef (open) Pg = Pg
+ unfolding Pg_def by (auto simp add: quotient_def)
lemma equiv_eq_game[simp]: "equiv UNIV eq_game_rel"
by (auto simp add: equiv_def refl_on_def sym_def trans_def eq_game_rel_def
--- a/src/HOL/ZF/Zet.thy Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/ZF/Zet.thy Wed Nov 30 16:27:10 2011 +0100
@@ -9,8 +9,10 @@
imports HOLZF
begin
-typedef 'a zet = "{A :: 'a set | A f z. inj_on f A \<and> f ` A \<subseteq> explode z}"
- by blast
+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"
+ unfolding zet_def by blast
definition zin :: "'a \<Rightarrow> 'a zet \<Rightarrow> bool" where
"zin x A == x \<in> (Rep_zet A)"
--- a/src/HOL/ex/Dedekind_Real.thy Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/ex/Dedekind_Real.thy Wed Nov 30 16:27:10 2011 +0100
@@ -44,8 +44,10 @@
qed
-typedef preal = "{A. cut A}"
- by (blast intro: cut_of_rat [OF zero_less_one])
+definition "preal = {A. cut A}"
+
+typedef (open) preal = preal
+ unfolding preal_def by (blast intro: cut_of_rat [OF zero_less_one])
definition
psup :: "preal set => preal" where
@@ -113,22 +115,26 @@
by (simp add: preal_def cut_of_rat)
lemma preal_nonempty: "A \<in> preal ==> \<exists>x\<in>A. 0 < x"
-by (unfold preal_def cut_def, blast)
+ unfolding preal_def cut_def_raw by blast
lemma preal_Ex_mem: "A \<in> preal \<Longrightarrow> \<exists>x. x \<in> A"
-by (drule preal_nonempty, fast)
+ apply (drule preal_nonempty)
+ apply fast
+ done
lemma preal_imp_psubset_positives: "A \<in> preal ==> A < {r. 0 < r}"
-by (force simp add: preal_def cut_def)
+ by (force simp add: preal_def cut_def)
lemma preal_exists_bound: "A \<in> preal ==> \<exists>x. 0 < x & x \<notin> A"
-by (drule preal_imp_psubset_positives, auto)
+ apply (drule preal_imp_psubset_positives)
+ apply auto
+ done
lemma preal_exists_greater: "[| A \<in> preal; y \<in> A |] ==> \<exists>u \<in> A. y < u"
-by (unfold preal_def cut_def, blast)
+ unfolding preal_def cut_def_raw by blast
lemma preal_downwards_closed: "[| A \<in> preal; y \<in> A; 0 < z; z < y |] ==> z \<in> A"
-by (unfold preal_def cut_def, blast)
+ unfolding preal_def cut_def_raw by blast
text{*Relaxing the final premise*}
lemma preal_downwards_closed':
@@ -960,7 +966,7 @@
lemma mem_diff_set:
"R < S ==> diff_set (Rep_preal S) (Rep_preal R) \<in> preal"
-apply (unfold preal_def cut_def)
+apply (unfold preal_def cut_def_raw)
apply (blast intro!: diff_set_not_empty diff_set_not_rat_set
diff_set_lemma3 diff_set_lemma4)
done
@@ -1129,7 +1135,7 @@
lemma preal_sup:
"[|P \<noteq> {}; \<forall>X \<in> P. X \<le> Y|] ==> (\<Union>X \<in> P. Rep_preal(X)) \<in> preal"
-apply (unfold preal_def cut_def)
+apply (unfold preal_def cut_def_raw)
apply (blast intro!: preal_sup_set_not_empty preal_sup_set_not_rat_set
preal_sup_set_lemma3 preal_sup_set_lemma4)
done
@@ -1163,8 +1169,11 @@
realrel :: "((preal * preal) * (preal * preal)) set" where
"realrel = {p. \<exists>x1 y1 x2 y2. p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1}"
-typedef (Real) real = "UNIV//realrel"
- by (auto simp add: quotient_def)
+definition "Real = UNIV//realrel"
+
+typedef (open) real = Real
+ morphisms Rep_Real Abs_Real
+ unfolding Real_def by (auto simp add: quotient_def)
definition
(** these don't use the overloaded "real" function: users don't see them **)
--- a/src/HOL/ex/PER.thy Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/ex/PER.thy Wed Nov 30 16:27:10 2011 +0100
@@ -151,8 +151,10 @@
\emph{equivalence classes} over elements of the base type @{typ 'a}.
*}
-typedef 'a quot = "{{x. a \<sim> x}| a::'a::partial_equiv. True}"
- by blast
+definition "quot = {{x. a \<sim> x}| a::'a::partial_equiv. True}"
+
+typedef (open) 'a quot = "quot :: 'a::partial_equiv set set"
+ unfolding quot_def by blast
lemma quotI [intro]: "{x. a \<sim> x} \<in> quot"
unfolding quot_def by blast
--- a/src/HOL/ex/Refute_Examples.thy Wed Nov 30 16:05:15 2011 +0100
+++ b/src/HOL/ex/Refute_Examples.thy Wed Nov 30 16:27:10 2011 +0100
@@ -494,8 +494,10 @@
text {* A completely unspecified non-empty subset of @{typ "'a"}: *}
-typedef 'a myTdef = "insert (undefined::'a) (undefined::'a set)"
- by auto
+definition "myTdef = insert (undefined::'a) (undefined::'a set)"
+
+typedef (open) 'a myTdef = "myTdef :: 'a set"
+ unfolding myTdef_def by auto
lemma "(x::'a myTdef) = y"
refute
@@ -503,8 +505,10 @@
typedecl myTdecl
-typedef 'a T_bij = "{(f::'a\<Rightarrow>'a). \<forall>y. \<exists>!x. f x = y}"
- by auto
+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"
+ unfolding T_bij_def by auto
lemma "P (f::(myTdecl myTdef) T_bij)"
refute