prefer typedef without extra definition and alternative name;
authorwenzelm
Wed Nov 30 16:27:10 2011 +0100 (2011-11-30 ago)
changeset 456944a8743618257
parent 45693 bbd2c7ffc02c
child 45695 b108b3d7c49e
prefer typedef without extra definition and alternative name;
tuned proofs;
src/HOL/Algebra/poly/UnivPoly2.thy
src/HOL/Code_Numeral.thy
src/HOL/Datatype.thy
src/HOL/HOLCF/Compact_Basis.thy
src/HOL/Induct/QuoDataType.thy
src/HOL/Induct/QuoNestedDataType.thy
src/HOL/Induct/SList.thy
src/HOL/Int.thy
src/HOL/Library/Dlist.thy
src/HOL/Library/Fraction_Field.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/Polynomial.thy
src/HOL/Library/Quotient_Type.thy
src/HOL/Library/RBT.thy
src/HOL/Matrix/Matrix.thy
src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
src/HOL/NSA/StarDef.thy
src/HOL/Nitpick_Examples/Manual_Nits.thy
src/HOL/Nitpick_Examples/Refute_Nits.thy
src/HOL/Nitpick_Examples/Typedef_Nits.thy
src/HOL/Nominal/Nominal.thy
src/HOL/Product_Type.thy
src/HOL/Quotient_Examples/Lift_Set.thy
src/HOL/Rat.thy
src/HOL/SMT_Examples/SMT_Tests.thy
src/HOL/Sum_Type.thy
src/HOL/UNITY/UNITY.thy
src/HOL/Word/Word.thy
src/HOL/ZF/Games.thy
src/HOL/ZF/Zet.thy
src/HOL/ex/Dedekind_Real.thy
src/HOL/ex/PER.thy
src/HOL/ex/Refute_Examples.thy
     1.1 --- a/src/HOL/Algebra/poly/UnivPoly2.thy	Wed Nov 30 16:05:15 2011 +0100
     1.2 +++ b/src/HOL/Algebra/poly/UnivPoly2.thy	Wed Nov 30 16:27:10 2011 +0100
     1.3 @@ -39,9 +39,15 @@
     1.4    with nonzero show ?thesis by contradiction
     1.5  qed
     1.6  
     1.7 -typedef (UP)
     1.8 -    ('a) up = "{f :: nat => 'a::zero. EX n. bound n f}"
     1.9 -  by (rule+)   (* Question: what does trace_rule show??? *)
    1.10 +
    1.11 +definition "UP = {f :: nat => 'a::zero. EX n. bound n f}"
    1.12 +
    1.13 +typedef (open) 'a up = "UP :: (nat => 'a::zero) set"
    1.14 +  morphisms Rep_UP Abs_UP
    1.15 +proof -
    1.16 +  have "bound 0 (\<lambda>_. 0::'a)" by (rule boundI) (rule refl)
    1.17 +  then show ?thesis unfolding UP_def by blast
    1.18 +qed
    1.19  
    1.20  
    1.21  section {* Constants *}
     2.1 --- a/src/HOL/Code_Numeral.thy	Wed Nov 30 16:05:15 2011 +0100
     2.2 +++ b/src/HOL/Code_Numeral.thy	Wed Nov 30 16:27:10 2011 +0100
     2.3 @@ -14,7 +14,7 @@
     2.4  subsection {* Datatype of target language numerals *}
     2.5  
     2.6  typedef (open) code_numeral = "UNIV \<Colon> nat set"
     2.7 -  morphisms nat_of of_nat by rule
     2.8 +  morphisms nat_of of_nat ..
     2.9  
    2.10  lemma of_nat_nat_of [simp]:
    2.11    "of_nat (nat_of k) = k"
     3.1 --- a/src/HOL/Datatype.thy	Wed Nov 30 16:05:15 2011 +0100
     3.2 +++ b/src/HOL/Datatype.thy	Wed Nov 30 16:27:10 2011 +0100
     3.3 @@ -21,10 +21,11 @@
     3.4  
     3.5  subsection {* The datatype universe *}
     3.6  
     3.7 -typedef (Node)
     3.8 -  ('a,'b) node = "{p. EX f x k. p = (f::nat=>'b+nat, x::'a+nat) & f k = Inr 0}"
     3.9 -    --{*it is a subtype of @{text "(nat=>'b+nat) * ('a+nat)"}*}
    3.10 -  by auto
    3.11 +definition "Node = {p. EX f x k. p = (f :: nat => 'b + nat, x ::'a + nat) & f k = Inr 0}"
    3.12 +
    3.13 +typedef (open) ('a, 'b) node = "Node :: ((nat => 'b + nat) * ('a + nat)) set"
    3.14 +  morphisms Rep_Node Abs_Node
    3.15 +  unfolding Node_def by auto
    3.16  
    3.17  text{*Datatypes will be represented by sets of type @{text node}*}
    3.18  
     4.1 --- a/src/HOL/HOLCF/Compact_Basis.thy	Wed Nov 30 16:05:15 2011 +0100
     4.2 +++ b/src/HOL/HOLCF/Compact_Basis.thy	Wed Nov 30 16:27:10 2011 +0100
     4.3 @@ -12,9 +12,13 @@
     4.4  
     4.5  subsection {* A compact basis for powerdomains *}
     4.6  
     4.7 -typedef 'a pd_basis =
     4.8 -  "{S::'a compact_basis set. finite S \<and> S \<noteq> {}}"
     4.9 -by (rule_tac x="{arbitrary}" in exI, simp)
    4.10 +definition "pd_basis = {S::'a compact_basis set. finite S \<and> S \<noteq> {}}"
    4.11 +
    4.12 +typedef (open) 'a pd_basis = "pd_basis :: 'a compact_basis set set"
    4.13 +  unfolding pd_basis_def
    4.14 +  apply (rule_tac x="{arbitrary}" in exI)
    4.15 +  apply simp
    4.16 +  done
    4.17  
    4.18  lemma finite_Rep_pd_basis [simp]: "finite (Rep_pd_basis u)"
    4.19  by (insert Rep_pd_basis [of u, unfolded pd_basis_def]) simp
     5.1 --- a/src/HOL/Induct/QuoDataType.thy	Wed Nov 30 16:05:15 2011 +0100
     5.2 +++ b/src/HOL/Induct/QuoDataType.thy	Wed Nov 30 16:27:10 2011 +0100
     5.3 @@ -123,8 +123,11 @@
     5.4  
     5.5  subsection{*The Initial Algebra: A Quotiented Message Type*}
     5.6  
     5.7 -typedef (Msg)  msg = "UNIV//msgrel"
     5.8 -  by (auto simp add: quotient_def)
     5.9 +definition "Msg = UNIV//msgrel"
    5.10 +
    5.11 +typedef (open) msg = Msg
    5.12 +  morphisms Rep_Msg Abs_Msg
    5.13 +  unfolding Msg_def by (auto simp add: quotient_def)
    5.14  
    5.15  
    5.16  text{*The abstract message constructors*}
     6.1 --- a/src/HOL/Induct/QuoNestedDataType.thy	Wed Nov 30 16:05:15 2011 +0100
     6.2 +++ b/src/HOL/Induct/QuoNestedDataType.thy	Wed Nov 30 16:27:10 2011 +0100
     6.3 @@ -142,9 +142,11 @@
     6.4  
     6.5  subsection{*The Initial Algebra: A Quotiented Message Type*}
     6.6  
     6.7 +definition "Exp = UNIV//exprel"
     6.8  
     6.9 -typedef (Exp)  exp = "UNIV//exprel"
    6.10 -    by (auto simp add: quotient_def)
    6.11 +typedef (open) exp = Exp
    6.12 +  morphisms Rep_Exp Abs_Exp
    6.13 +  unfolding Exp_def by (auto simp add: quotient_def)
    6.14  
    6.15  text{*The abstract message constructors*}
    6.16  
     7.1 --- a/src/HOL/Induct/SList.thy	Wed Nov 30 16:05:15 2011 +0100
     7.2 +++ b/src/HOL/Induct/SList.thy	Wed Nov 30 16:27:10 2011 +0100
     7.3 @@ -53,9 +53,11 @@
     7.4    | CONS_I: "[| a: A;  M: list A |] ==> CONS a M : list A"
     7.5  
     7.6  
     7.7 -typedef (List)
     7.8 -    'a list = "list(range Leaf) :: 'a item set" 
     7.9 -  by (blast intro: list.NIL_I)
    7.10 +definition "List = list (range Leaf)"
    7.11 +
    7.12 +typedef (open) 'a list = "List :: 'a item set"
    7.13 +  morphisms Rep_List Abs_List
    7.14 +  unfolding List_def by (blast intro: list.NIL_I)
    7.15  
    7.16  abbreviation "Case == Datatype.Case"
    7.17  abbreviation "Split == Datatype.Split"
    7.18 @@ -224,7 +226,7 @@
    7.19  lemmas Cons_inject2 = Cons_Cons_eq [THEN iffD1, THEN conjE]
    7.20  
    7.21  lemma CONS_D: "CONS M N: list(A) ==> M: A & N: list(A)"
    7.22 -  by (induct L == "CONS M N" set: list) auto
    7.23 +  by (induct L == "CONS M N" rule: list.induct) auto
    7.24  
    7.25  lemma sexp_CONS_D: "CONS M N: sexp ==> M: sexp & N: sexp"
    7.26  apply (simp add: CONS_def In1_def)
     8.1 --- a/src/HOL/Int.thy	Wed Nov 30 16:05:15 2011 +0100
     8.2 +++ b/src/HOL/Int.thy	Wed Nov 30 16:27:10 2011 +0100
     8.3 @@ -18,9 +18,11 @@
     8.4  definition intrel :: "((nat \<times> nat) \<times> (nat \<times> nat)) set" where
     8.5    "intrel = {((x, y), (u, v)) | x y u v. x + v = u +y }"
     8.6  
     8.7 -typedef (Integ)
     8.8 -  int = "UNIV//intrel"
     8.9 -  by (auto simp add: quotient_def)
    8.10 +definition "Integ = UNIV//intrel"
    8.11 +
    8.12 +typedef (open) int = Integ
    8.13 +  morphisms Rep_Integ Abs_Integ
    8.14 +  unfolding Integ_def by (auto simp add: quotient_def)
    8.15  
    8.16  instantiation int :: "{zero, one, plus, minus, uminus, times, ord, abs, sgn}"
    8.17  begin
     9.1 --- a/src/HOL/Library/Dlist.thy	Wed Nov 30 16:05:15 2011 +0100
     9.2 +++ b/src/HOL/Library/Dlist.thy	Wed Nov 30 16:27:10 2011 +0100
     9.3 @@ -11,7 +11,7 @@
     9.4  typedef (open) 'a dlist = "{xs::'a list. distinct xs}"
     9.5    morphisms list_of_dlist Abs_dlist
     9.6  proof
     9.7 -  show "[] \<in> ?dlist" by simp
     9.8 +  show "[] \<in> {xs. distinct xs}" by simp
     9.9  qed
    9.10  
    9.11  lemma dlist_eq_iff:
    10.1 --- a/src/HOL/Library/Fraction_Field.thy	Wed Nov 30 16:05:15 2011 +0100
    10.2 +++ b/src/HOL/Library/Fraction_Field.thy	Wed Nov 30 16:27:10 2011 +0100
    10.3 @@ -53,7 +53,10 @@
    10.4    shows "fractrel `` {x} = fractrel `` {y} \<longleftrightarrow> (x, y) \<in> fractrel"
    10.5    by (rule eq_equiv_class_iff, rule equiv_fractrel) (auto simp add: assms)
    10.6  
    10.7 -typedef 'a fract = "{(x::'a\<times>'a). snd x \<noteq> (0::'a::idom)} // fractrel"
    10.8 +definition "fract = {(x::'a\<times>'a). snd x \<noteq> (0::'a::idom)} // fractrel"
    10.9 +
   10.10 +typedef (open) 'a fract = "fract :: ('a * 'a::idom) set set"
   10.11 +  unfolding fract_def
   10.12  proof
   10.13    have "(0::'a, 1::'a) \<in> {x. snd x \<noteq> 0}" by simp
   10.14    then show "fractrel `` {(0::'a, 1)} \<in> {x. snd x \<noteq> 0} // fractrel" by (rule quotientI)
    11.1 --- a/src/HOL/Library/Multiset.thy	Wed Nov 30 16:05:15 2011 +0100
    11.2 +++ b/src/HOL/Library/Multiset.thy	Wed Nov 30 16:27:10 2011 +0100
    11.3 @@ -10,10 +10,13 @@
    11.4  
    11.5  subsection {* The type of multisets *}
    11.6  
    11.7 -typedef 'a multiset = "{f :: 'a => nat. finite {x. f x > 0}}"
    11.8 +definition "multiset = {f :: 'a => nat. finite {x. f x > 0}}"
    11.9 +
   11.10 +typedef (open) 'a multiset = "multiset :: ('a => nat) set"
   11.11    morphisms count Abs_multiset
   11.12 +  unfolding multiset_def
   11.13  proof
   11.14 -  show "(\<lambda>x. 0::nat) \<in> ?multiset" by simp
   11.15 +  show "(\<lambda>x. 0::nat) \<in> {f. finite {x. f x > 0}}" by simp
   11.16  qed
   11.17  
   11.18  lemmas multiset_typedef = Abs_multiset_inverse count_inverse count
    12.1 --- a/src/HOL/Library/Polynomial.thy	Wed Nov 30 16:05:15 2011 +0100
    12.2 +++ b/src/HOL/Library/Polynomial.thy	Wed Nov 30 16:27:10 2011 +0100
    12.3 @@ -11,15 +11,17 @@
    12.4  
    12.5  subsection {* Definition of type @{text poly} *}
    12.6  
    12.7 -typedef (Poly) 'a poly = "{f::nat \<Rightarrow> 'a::zero. \<exists>n. \<forall>i>n. f i = 0}"
    12.8 +definition "Poly = {f::nat \<Rightarrow> 'a::zero. \<exists>n. \<forall>i>n. f i = 0}"
    12.9 +
   12.10 +typedef (open) 'a poly = "Poly :: (nat => 'a::zero) set"
   12.11    morphisms coeff Abs_poly
   12.12 -  by auto
   12.13 +  unfolding Poly_def by auto
   12.14  
   12.15  lemma expand_poly_eq: "p = q \<longleftrightarrow> (\<forall>n. coeff p n = coeff q n)"
   12.16 -by (simp add: coeff_inject [symmetric] fun_eq_iff)
   12.17 +  by (simp add: coeff_inject [symmetric] fun_eq_iff)
   12.18  
   12.19  lemma poly_ext: "(\<And>n. coeff p n = coeff q n) \<Longrightarrow> p = q"
   12.20 -by (simp add: expand_poly_eq)
   12.21 +  by (simp add: expand_poly_eq)
   12.22  
   12.23  
   12.24  subsection {* Degree of a polynomial *}
    13.1 --- a/src/HOL/Library/Quotient_Type.thy	Wed Nov 30 16:05:15 2011 +0100
    13.2 +++ b/src/HOL/Library/Quotient_Type.thy	Wed Nov 30 16:27:10 2011 +0100
    13.3 @@ -58,8 +58,10 @@
    13.4   \emph{equivalence classes} over elements of the base type @{typ 'a}.
    13.5  *}
    13.6  
    13.7 -typedef 'a quot = "{{x. a \<sim> x} | a::'a::eqv. True}"
    13.8 -  by blast
    13.9 +definition "quot = {{x. a \<sim> x} | a::'a::eqv. True}"
   13.10 +
   13.11 +typedef (open) 'a quot = "quot :: 'a::eqv set set"
   13.12 +  unfolding quot_def by blast
   13.13  
   13.14  lemma quotI [intro]: "{x. a \<sim> x} \<in> quot"
   13.15    unfolding quot_def by blast
    14.1 --- a/src/HOL/Library/RBT.thy	Wed Nov 30 16:05:15 2011 +0100
    14.2 +++ b/src/HOL/Library/RBT.thy	Wed Nov 30 16:27:10 2011 +0100
    14.3 @@ -11,9 +11,8 @@
    14.4  
    14.5  typedef (open) ('a, 'b) rbt = "{t :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt. is_rbt t}"
    14.6    morphisms impl_of RBT
    14.7 -proof -
    14.8 -  have "RBT_Impl.Empty \<in> ?rbt" by simp
    14.9 -  then show ?thesis ..
   14.10 +proof
   14.11 +  show "RBT_Impl.Empty \<in> {t. is_rbt t}" by simp
   14.12  qed
   14.13  
   14.14  lemma rbt_eq_iff:
    15.1 --- a/src/HOL/Matrix/Matrix.thy	Wed Nov 30 16:05:15 2011 +0100
    15.2 +++ b/src/HOL/Matrix/Matrix.thy	Wed Nov 30 16:27:10 2011 +0100
    15.3 @@ -11,18 +11,19 @@
    15.4  definition nonzero_positions :: "(nat \<Rightarrow> nat \<Rightarrow> 'a::zero) \<Rightarrow> (nat \<times> nat) set" where
    15.5    "nonzero_positions A = {pos. A (fst pos) (snd pos) ~= 0}"
    15.6  
    15.7 -typedef 'a matrix = "{(f::(nat \<Rightarrow> nat \<Rightarrow> 'a::zero)). finite (nonzero_positions f)}"
    15.8 -proof -
    15.9 -  have "(\<lambda>j i. 0) \<in> {(f::(nat \<Rightarrow> nat \<Rightarrow> 'a::zero)). finite (nonzero_positions f)}"
   15.10 +definition "matrix = {(f::(nat \<Rightarrow> nat \<Rightarrow> 'a::zero)). finite (nonzero_positions f)}"
   15.11 +
   15.12 +typedef (open) 'a matrix = "matrix :: (nat \<Rightarrow> nat \<Rightarrow> 'a::zero) set"
   15.13 +  unfolding matrix_def
   15.14 +proof
   15.15 +  show "(\<lambda>j i. 0) \<in> {(f::(nat \<Rightarrow> nat \<Rightarrow> 'a::zero)). finite (nonzero_positions f)}"
   15.16      by (simp add: nonzero_positions_def)
   15.17 -  then show ?thesis by auto
   15.18  qed
   15.19  
   15.20  declare Rep_matrix_inverse[simp]
   15.21  
   15.22  lemma finite_nonzero_positions : "finite (nonzero_positions (Rep_matrix A))"
   15.23 -apply (rule Abs_matrix_induct)
   15.24 -by (simp add: Abs_matrix_inverse matrix_def)
   15.25 +  by (induct A) (simp add: Abs_matrix_inverse matrix_def)
   15.26  
   15.27  definition nrows :: "('a::zero) matrix \<Rightarrow> nat" where
   15.28    "nrows A == if nonzero_positions(Rep_matrix A) = {} then 0 else Suc(Max ((image fst) (nonzero_positions (Rep_matrix A))))"
    16.1 --- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Wed Nov 30 16:05:15 2011 +0100
    16.2 +++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Wed Nov 30 16:27:10 2011 +0100
    16.3 @@ -13,8 +13,7 @@
    16.4  
    16.5  subsection {* Finite Cartesian products, with indexing and lambdas. *}
    16.6  
    16.7 -typedef (open)
    16.8 -  ('a, 'b) vec = "UNIV :: (('b::finite) \<Rightarrow> 'a) set"
    16.9 +typedef (open) ('a, 'b) vec = "UNIV :: (('b::finite) \<Rightarrow> 'a) set"
   16.10    morphisms vec_nth vec_lambda ..
   16.11  
   16.12  notation
    17.1 --- a/src/HOL/NSA/StarDef.thy	Wed Nov 30 16:05:15 2011 +0100
    17.2 +++ b/src/HOL/NSA/StarDef.thy	Wed Nov 30 16:27:10 2011 +0100
    17.3 @@ -39,8 +39,10 @@
    17.4    starrel :: "((nat \<Rightarrow> 'a) \<times> (nat \<Rightarrow> 'a)) set" where
    17.5    "starrel = {(X,Y). {n. X n = Y n} \<in> \<U>}"
    17.6  
    17.7 -typedef 'a star = "(UNIV :: (nat \<Rightarrow> 'a) set) // starrel"
    17.8 -by (auto intro: quotientI)
    17.9 +definition "star = (UNIV :: (nat \<Rightarrow> 'a) set) // starrel"
   17.10 +
   17.11 +typedef (open) 'a star = "star :: (nat \<Rightarrow> 'a) set set"
   17.12 +  unfolding star_def by (auto intro: quotientI)
   17.13  
   17.14  definition
   17.15    star_n :: "(nat \<Rightarrow> 'a) \<Rightarrow> 'a star" where
    18.1 --- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Wed Nov 30 16:05:15 2011 +0100
    18.2 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Wed Nov 30 16:27:10 2011 +0100
    18.3 @@ -95,8 +95,9 @@
    18.4  
    18.5  subsection {* 2.7. Typedefs, Records, Rationals, and Reals *}
    18.6  
    18.7 -typedef three = "{0\<Colon>nat, 1, 2}"
    18.8 -by blast
    18.9 +definition "three = {0\<Colon>nat, 1, 2}"
   18.10 +typedef (open) three = three
   18.11 +unfolding three_def by blast
   18.12  
   18.13  definition A :: three where "A \<equiv> Abs_three 0"
   18.14  definition B :: three where "B \<equiv> Abs_three 1"
   18.15 @@ -197,7 +198,10 @@
   18.16     axiomatization. The examples also work unchanged with Lochbihler's
   18.17     "Coinductive_List" theory. *)
   18.18  
   18.19 -typedef 'a llist = "UNIV\<Colon>('a list + (nat \<Rightarrow> 'a)) set" by auto
   18.20 +definition "llist = (UNIV\<Colon>('a list + (nat \<Rightarrow> 'a)) set)"
   18.21 +
   18.22 +typedef (open) 'a llist = "llist\<Colon>('a list + (nat \<Rightarrow> 'a)) set"
   18.23 +unfolding llist_def by auto
   18.24  
   18.25  definition LNil where
   18.26  "LNil = Abs_llist (Inl [])"
    19.1 --- a/src/HOL/Nitpick_Examples/Refute_Nits.thy	Wed Nov 30 16:05:15 2011 +0100
    19.2 +++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy	Wed Nov 30 16:27:10 2011 +0100
    19.3 @@ -539,8 +539,10 @@
    19.4  
    19.5  text {* A completely unspecified non-empty subset of @{typ "'a"}: *}
    19.6  
    19.7 -typedef 'a myTdef = "insert (undefined\<Colon>'a) (undefined\<Colon>'a set)"
    19.8 -by auto
    19.9 +definition "myTdef = insert (undefined::'a) (undefined::'a set)"
   19.10 +
   19.11 +typedef (open) 'a myTdef = "myTdef :: 'a set"
   19.12 +unfolding myTdef_def by auto
   19.13  
   19.14  lemma "(x\<Colon>'a myTdef) = y"
   19.15  nitpick [expect = genuine]
   19.16 @@ -548,8 +550,10 @@
   19.17  
   19.18  typedecl myTdecl
   19.19  
   19.20 -typedef 'a T_bij = "{(f\<Colon>'a\<Rightarrow>'a). \<forall>y. \<exists>!x. f x = y}"
   19.21 -by auto
   19.22 +definition "T_bij = {(f::'a\<Rightarrow>'a). \<forall>y. \<exists>!x. f x = y}"
   19.23 +
   19.24 +typedef (open) 'a T_bij = "T_bij :: ('a \<Rightarrow> 'a) set"
   19.25 +unfolding T_bij_def by auto
   19.26  
   19.27  lemma "P (f\<Colon>(myTdecl myTdef) T_bij)"
   19.28  nitpick [expect = genuine]
    20.1 --- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Wed Nov 30 16:05:15 2011 +0100
    20.2 +++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Wed Nov 30 16:27:10 2011 +0100
    20.3 @@ -14,8 +14,9 @@
    20.4  nitpick_params [verbose, card = 1\<emdash>4, sat_solver = MiniSat_JNI, max_threads = 1,
    20.5                  timeout = 240]
    20.6  
    20.7 -typedef three = "{0\<Colon>nat, 1, 2}"
    20.8 -by blast
    20.9 +definition "three = {0\<Colon>nat, 1, 2}"
   20.10 +typedef (open) three = three
   20.11 +unfolding three_def by blast
   20.12  
   20.13  definition A :: three where "A \<equiv> Abs_three 0"
   20.14  definition B :: three where "B \<equiv> Abs_three 1"
   20.15 @@ -25,8 +26,10 @@
   20.16  nitpick [expect = genuine]
   20.17  oops
   20.18  
   20.19 -typedef 'a one_or_two = "{undefined False\<Colon>'a, undefined True}"
   20.20 -by auto
   20.21 +definition "one_or_two = {undefined False\<Colon>'a, undefined True}"
   20.22 +
   20.23 +typedef (open) 'a one_or_two = "one_or_two :: 'a set"
   20.24 +unfolding one_or_two_def by auto
   20.25  
   20.26  lemma "x = (y\<Colon>unit one_or_two)"
   20.27  nitpick [expect = none]
   20.28 @@ -49,8 +52,9 @@
   20.29  nitpick [card = 2, expect = none]
   20.30  oops
   20.31  
   20.32 -typedef 'a bounded =
   20.33 -        "{n\<Colon>nat. finite (UNIV\<Colon>'a \<Rightarrow> bool) \<longrightarrow> n < card (UNIV\<Colon>'a \<Rightarrow> bool)}"
   20.34 +definition "bounded = {n\<Colon>nat. finite (UNIV\<Colon>'a \<Rightarrow> bool) \<longrightarrow> n < card (UNIV\<Colon>'a \<Rightarrow> bool)}"
   20.35 +typedef (open) 'a bounded = "bounded(TYPE('a))"
   20.36 +unfolding bounded_def
   20.37  apply (rule_tac x = 0 in exI)
   20.38  apply (case_tac "card UNIV = 0")
   20.39  by auto
    21.1 --- a/src/HOL/Nominal/Nominal.thy	Wed Nov 30 16:05:15 2011 +0100
    21.2 +++ b/src/HOL/Nominal/Nominal.thy	Wed Nov 30 16:27:10 2011 +0100
    21.3 @@ -3395,8 +3395,12 @@
    21.4    where
    21.5    ABS_in: "(abs_fun a x)\<in>ABS_set"
    21.6  
    21.7 -typedef (ABS) ('x,'a) ABS ("\<guillemotleft>_\<guillemotright>_" [1000,1000] 1000) =
    21.8 -  "ABS_set::('x\<Rightarrow>('a noption)) set"
    21.9 +definition "ABS = ABS_set"
   21.10 +
   21.11 +typedef (open) ('x,'a) ABS ("\<guillemotleft>_\<guillemotright>_" [1000,1000] 1000) =
   21.12 +    "ABS::('x\<Rightarrow>('a noption)) set"
   21.13 +  morphisms Rep_ABS Abs_ABS
   21.14 +  unfolding ABS_def
   21.15  proof 
   21.16    fix x::"'a" and a::"'x"
   21.17    show "(abs_fun a x)\<in> ABS_set" by (rule ABS_in)
    22.1 --- a/src/HOL/Product_Type.thy	Wed Nov 30 16:05:15 2011 +0100
    22.2 +++ b/src/HOL/Product_Type.thy	Wed Nov 30 16:27:10 2011 +0100
    22.3 @@ -46,14 +46,10 @@
    22.4  subsection {* The @{text unit} type *}
    22.5  
    22.6  typedef (open) unit = "{True}"
    22.7 -proof
    22.8 -  show "True : ?unit" ..
    22.9 -qed
   22.10 +  by auto
   22.11  
   22.12 -definition
   22.13 -  Unity :: unit    ("'(')")
   22.14 -where
   22.15 -  "() = Abs_unit True"
   22.16 +definition Unity :: unit  ("'(')")
   22.17 +  where "() = Abs_unit True"
   22.18  
   22.19  lemma unit_eq [no_atp]: "u = ()"
   22.20    by (induct u) (simp add: Unity_def)
   22.21 @@ -136,12 +132,8 @@
   22.22  definition Pair_Rep :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" where
   22.23    "Pair_Rep a b = (\<lambda>x y. x = a \<and> y = b)"
   22.24  
   22.25 -typedef ('a, 'b) prod (infixr "*" 20)
   22.26 -  = "{f. \<exists>a b. f = Pair_Rep (a\<Colon>'a) (b\<Colon>'b)}"
   22.27 -proof
   22.28 -  fix a b show "Pair_Rep a b \<in> ?prod"
   22.29 -    by rule+
   22.30 -qed
   22.31 +typedef ('a, 'b) prod (infixr "*" 20) = "{f. \<exists>a b. f = Pair_Rep (a\<Colon>'a) (b\<Colon>'b)}"
   22.32 +  by auto
   22.33  
   22.34  type_notation (xsymbols)
   22.35    "prod"  ("(_ \<times>/ _)" [21, 20] 20)
    23.1 --- a/src/HOL/Quotient_Examples/Lift_Set.thy	Wed Nov 30 16:05:15 2011 +0100
    23.2 +++ b/src/HOL/Quotient_Examples/Lift_Set.thy	Wed Nov 30 16:27:10 2011 +0100
    23.3 @@ -8,21 +8,29 @@
    23.4  imports Main
    23.5  begin
    23.6  
    23.7 -typedef 'a set = "(UNIV :: ('a => bool) => bool)"
    23.8 -morphisms member Set by auto
    23.9 +definition set where "set = (UNIV :: ('a => bool) => bool)"
   23.10 +
   23.11 +typedef (open) 'a set = "set :: 'a set set"
   23.12 +  morphisms member Set
   23.13 +  unfolding set_def by auto
   23.14  
   23.15  text {* Here is some ML setup that should eventually be incorporated in the typedef command. *}
   23.16  
   23.17  local_setup {* fn lthy =>
   23.18 -let
   23.19 -  val quotients = {qtyp = @{typ "'a set"}, rtyp = @{typ "'a => bool"}, equiv_rel = @{term "dummy"}, equiv_thm = @{thm refl}}
   23.20 -  val qty_full_name = @{type_name "set"}
   23.21 +  let
   23.22 +    val quotients =
   23.23 +      {qtyp = @{typ "'a set"}, rtyp = @{typ "'a => bool"},
   23.24 +        equiv_rel = @{term "dummy"}, equiv_thm = @{thm refl}}
   23.25 +    val qty_full_name = @{type_name "set"}
   23.26  
   23.27 -  fun qinfo phi = Quotient_Info.transform_quotients phi quotients
   23.28 -  in lthy
   23.29 +    fun qinfo phi = Quotient_Info.transform_quotients phi quotients
   23.30 +  in
   23.31 +    lthy
   23.32      |> Local_Theory.declaration {syntax = false, pervasive = true}
   23.33 -        (fn phi => Quotient_Info.update_quotients qty_full_name (qinfo phi)
   23.34 -       #> Quotient_Info.update_abs_rep qty_full_name (Quotient_Info.transform_abs_rep phi {abs = @{term "Set"}, rep = @{term "member"}}))
   23.35 +        (fn phi =>
   23.36 +          Quotient_Info.update_quotients qty_full_name (qinfo phi) #>
   23.37 +          Quotient_Info.update_abs_rep qty_full_name
   23.38 +            (Quotient_Info.transform_abs_rep phi {abs = @{term "Set"}, rep = @{term "member"}}))
   23.39    end
   23.40  *}
   23.41  
    24.1 --- a/src/HOL/Rat.thy	Wed Nov 30 16:05:15 2011 +0100
    24.2 +++ b/src/HOL/Rat.thy	Wed Nov 30 16:27:10 2011 +0100
    24.3 @@ -54,7 +54,11 @@
    24.4    shows "ratrel `` {x} = ratrel `` {y} \<longleftrightarrow> (x, y) \<in> ratrel"
    24.5    by (rule eq_equiv_class_iff, rule equiv_ratrel) (auto simp add: assms)
    24.6  
    24.7 -typedef (Rat) rat = "{x. snd x \<noteq> 0} // ratrel"
    24.8 +definition "Rat = {x. snd x \<noteq> 0} // ratrel"
    24.9 +
   24.10 +typedef (open) rat = Rat
   24.11 +  morphisms Rep_Rat Abs_Rat
   24.12 +  unfolding Rat_def
   24.13  proof
   24.14    have "(0::int, 1::int) \<in> {x. snd x \<noteq> 0}" by simp
   24.15    then show "ratrel `` {(0, 1)} \<in> {x. snd x \<noteq> 0} // ratrel" by (rule quotientI)
    25.1 --- a/src/HOL/SMT_Examples/SMT_Tests.thy	Wed Nov 30 16:05:15 2011 +0100
    25.2 +++ b/src/HOL/SMT_Examples/SMT_Tests.thy	Wed Nov 30 16:27:10 2011 +0100
    25.3 @@ -762,7 +762,10 @@
    25.4  
    25.5  subsubsection {* Type definitions *}
    25.6  
    25.7 -typedef three = "{1, 2, 3::int}" by auto
    25.8 +definition "three = {1, 2, 3::int}"
    25.9 +
   25.10 +typedef (open) three = three
   25.11 +  unfolding three_def by auto
   25.12  
   25.13  definition n1 where "n1 = Abs_three 1"
   25.14  definition n2 where "n2 = Abs_three 2"
    26.1 --- a/src/HOL/Sum_Type.thy	Wed Nov 30 16:05:15 2011 +0100
    26.2 +++ b/src/HOL/Sum_Type.thy	Wed Nov 30 16:27:10 2011 +0100
    26.3 @@ -17,8 +17,10 @@
    26.4  definition Inr_Rep :: "'b \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool \<Rightarrow> bool" where
    26.5    "Inr_Rep b x y p \<longleftrightarrow> y = b \<and> \<not> p"
    26.6  
    26.7 -typedef ('a, 'b) sum (infixr "+" 10) = "{f. (\<exists>a. f = Inl_Rep (a::'a)) \<or> (\<exists>b. f = Inr_Rep (b::'b))}"
    26.8 -  by auto
    26.9 +definition "sum = {f. (\<exists>a. f = Inl_Rep (a::'a)) \<or> (\<exists>b. f = Inr_Rep (b::'b))}"
   26.10 +
   26.11 +typedef (open) ('a, 'b) sum (infixr "+" 10) = "sum :: ('a => 'b => bool => bool) set"
   26.12 +  unfolding sum_def by auto
   26.13  
   26.14  lemma Inl_RepI: "Inl_Rep a \<in> sum"
   26.15    by (auto simp add: sum_def)
    27.1 --- a/src/HOL/UNITY/UNITY.thy	Wed Nov 30 16:05:15 2011 +0100
    27.2 +++ b/src/HOL/UNITY/UNITY.thy	Wed Nov 30 16:27:10 2011 +0100
    27.3 @@ -12,10 +12,14 @@
    27.4  
    27.5  theory UNITY imports Main begin
    27.6  
    27.7 -typedef (Program)
    27.8 -  'a program = "{(init:: 'a set, acts :: ('a * 'a)set set,
    27.9 -                   allowed :: ('a * 'a)set set). Id \<in> acts & Id: allowed}" 
   27.10 -  by blast
   27.11 +definition
   27.12 +  "Program =
   27.13 +    {(init:: 'a set, acts :: ('a * 'a)set set,
   27.14 +      allowed :: ('a * 'a)set set). Id \<in> acts & Id: allowed}"
   27.15 +
   27.16 +typedef (open) 'a program = "Program :: ('a set * ('a * 'a) set set * ('a * 'a) set set) set"
   27.17 +  morphisms Rep_Program Abs_Program
   27.18 +  unfolding Program_def by blast
   27.19  
   27.20  definition Acts :: "'a program => ('a * 'a)set set" where
   27.21      "Acts F == (%(init, acts, allowed). acts) (Rep_Program F)"
    28.1 --- a/src/HOL/Word/Word.thy	Wed Nov 30 16:05:15 2011 +0100
    28.2 +++ b/src/HOL/Word/Word.thy	Wed Nov 30 16:27:10 2011 +0100
    28.3 @@ -17,7 +17,7 @@
    28.4  
    28.5  subsection {* Type definition *}
    28.6  
    28.7 -typedef (open word) 'a word = "{(0::int) ..< 2^len_of TYPE('a::len0)}"
    28.8 +typedef (open) 'a word = "{(0::int) ..< 2^len_of TYPE('a::len0)}"
    28.9    morphisms uint Abs_word by auto
   28.10  
   28.11  definition word_of_int :: "int \<Rightarrow> 'a\<Colon>len0 word" where
    29.1 --- a/src/HOL/ZF/Games.thy	Wed Nov 30 16:05:15 2011 +0100
    29.2 +++ b/src/HOL/ZF/Games.thy	Wed Nov 30 16:27:10 2011 +0100
    29.3 @@ -189,8 +189,10 @@
    29.4    apply (simp add: games_lfp_unfold[symmetric])
    29.5    done
    29.6  
    29.7 -typedef game = games_lfp
    29.8 -  by (blast intro: games_lfp_nonempty)
    29.9 +definition "game = games_lfp"
   29.10 +
   29.11 +typedef (open) game = game
   29.12 +  unfolding game_def by (blast intro: games_lfp_nonempty)
   29.13  
   29.14  definition left_options :: "game \<Rightarrow> game zet" where
   29.15    "left_options g \<equiv> zimage Abs_game (zexplode (Fst (Rep_game g)))"
   29.16 @@ -839,8 +841,10 @@
   29.17  definition eq_game_rel :: "(game * game) set" where
   29.18    "eq_game_rel \<equiv> { (p, q) . eq_game p q }"
   29.19  
   29.20 -typedef Pg = "UNIV//eq_game_rel"
   29.21 -  by (auto simp add: quotient_def)
   29.22 +definition "Pg = UNIV//eq_game_rel"
   29.23 +
   29.24 +typedef (open) Pg = Pg
   29.25 +  unfolding Pg_def by (auto simp add: quotient_def)
   29.26  
   29.27  lemma equiv_eq_game[simp]: "equiv UNIV eq_game_rel"
   29.28    by (auto simp add: equiv_def refl_on_def sym_def trans_def eq_game_rel_def
    30.1 --- a/src/HOL/ZF/Zet.thy	Wed Nov 30 16:05:15 2011 +0100
    30.2 +++ b/src/HOL/ZF/Zet.thy	Wed Nov 30 16:27:10 2011 +0100
    30.3 @@ -9,8 +9,10 @@
    30.4  imports HOLZF
    30.5  begin
    30.6  
    30.7 -typedef 'a zet = "{A :: 'a set | A f z. inj_on f A \<and> f ` A \<subseteq> explode z}"
    30.8 -  by blast
    30.9 +definition "zet = {A :: 'a set | A f z. inj_on f A \<and> f ` A \<subseteq> explode z}"
   30.10 +
   30.11 +typedef (open) 'a zet = "zet :: 'a set set"
   30.12 +  unfolding zet_def by blast
   30.13  
   30.14  definition zin :: "'a \<Rightarrow> 'a zet \<Rightarrow> bool" where
   30.15    "zin x A == x \<in> (Rep_zet A)"
    31.1 --- a/src/HOL/ex/Dedekind_Real.thy	Wed Nov 30 16:05:15 2011 +0100
    31.2 +++ b/src/HOL/ex/Dedekind_Real.thy	Wed Nov 30 16:27:10 2011 +0100
    31.3 @@ -44,8 +44,10 @@
    31.4  qed
    31.5  
    31.6  
    31.7 -typedef preal = "{A. cut A}"
    31.8 -  by (blast intro: cut_of_rat [OF zero_less_one])
    31.9 +definition "preal = {A. cut A}"
   31.10 +
   31.11 +typedef (open) preal = preal
   31.12 +  unfolding preal_def by (blast intro: cut_of_rat [OF zero_less_one])
   31.13  
   31.14  definition
   31.15    psup :: "preal set => preal" where
   31.16 @@ -113,22 +115,26 @@
   31.17  by (simp add: preal_def cut_of_rat)
   31.18  
   31.19  lemma preal_nonempty: "A \<in> preal ==> \<exists>x\<in>A. 0 < x"
   31.20 -by (unfold preal_def cut_def, blast)
   31.21 +  unfolding preal_def cut_def_raw by blast
   31.22  
   31.23  lemma preal_Ex_mem: "A \<in> preal \<Longrightarrow> \<exists>x. x \<in> A"
   31.24 -by (drule preal_nonempty, fast)
   31.25 +  apply (drule preal_nonempty)
   31.26 +  apply fast
   31.27 +  done
   31.28  
   31.29  lemma preal_imp_psubset_positives: "A \<in> preal ==> A < {r. 0 < r}"
   31.30 -by (force simp add: preal_def cut_def)
   31.31 +  by (force simp add: preal_def cut_def)
   31.32  
   31.33  lemma preal_exists_bound: "A \<in> preal ==> \<exists>x. 0 < x & x \<notin> A"
   31.34 -by (drule preal_imp_psubset_positives, auto)
   31.35 +  apply (drule preal_imp_psubset_positives)
   31.36 +  apply auto
   31.37 +  done
   31.38  
   31.39  lemma preal_exists_greater: "[| A \<in> preal; y \<in> A |] ==> \<exists>u \<in> A. y < u"
   31.40 -by (unfold preal_def cut_def, blast)
   31.41 +  unfolding preal_def cut_def_raw by blast
   31.42  
   31.43  lemma preal_downwards_closed: "[| A \<in> preal; y \<in> A; 0 < z; z < y |] ==> z \<in> A"
   31.44 -by (unfold preal_def cut_def, blast)
   31.45 +  unfolding preal_def cut_def_raw by blast
   31.46  
   31.47  text{*Relaxing the final premise*}
   31.48  lemma preal_downwards_closed':
   31.49 @@ -960,7 +966,7 @@
   31.50  
   31.51  lemma mem_diff_set:
   31.52       "R < S ==> diff_set (Rep_preal S) (Rep_preal R) \<in> preal"
   31.53 -apply (unfold preal_def cut_def)
   31.54 +apply (unfold preal_def cut_def_raw)
   31.55  apply (blast intro!: diff_set_not_empty diff_set_not_rat_set
   31.56                       diff_set_lemma3 diff_set_lemma4)
   31.57  done
   31.58 @@ -1129,7 +1135,7 @@
   31.59  
   31.60  lemma preal_sup:
   31.61       "[|P \<noteq> {}; \<forall>X \<in> P. X \<le> Y|] ==> (\<Union>X \<in> P. Rep_preal(X)) \<in> preal"
   31.62 -apply (unfold preal_def cut_def)
   31.63 +apply (unfold preal_def cut_def_raw)
   31.64  apply (blast intro!: preal_sup_set_not_empty preal_sup_set_not_rat_set
   31.65                       preal_sup_set_lemma3 preal_sup_set_lemma4)
   31.66  done
   31.67 @@ -1163,8 +1169,11 @@
   31.68    realrel   ::  "((preal * preal) * (preal * preal)) set" where
   31.69    "realrel = {p. \<exists>x1 y1 x2 y2. p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1}"
   31.70  
   31.71 -typedef (Real)  real = "UNIV//realrel"
   31.72 -  by (auto simp add: quotient_def)
   31.73 +definition "Real = UNIV//realrel"
   31.74 +
   31.75 +typedef (open) real = Real
   31.76 +  morphisms Rep_Real Abs_Real
   31.77 +  unfolding Real_def by (auto simp add: quotient_def)
   31.78  
   31.79  definition
   31.80    (** these don't use the overloaded "real" function: users don't see them **)
    32.1 --- a/src/HOL/ex/PER.thy	Wed Nov 30 16:05:15 2011 +0100
    32.2 +++ b/src/HOL/ex/PER.thy	Wed Nov 30 16:27:10 2011 +0100
    32.3 @@ -151,8 +151,10 @@
    32.4    \emph{equivalence classes} over elements of the base type @{typ 'a}.
    32.5  *}
    32.6  
    32.7 -typedef 'a quot = "{{x. a \<sim> x}| a::'a::partial_equiv. True}"
    32.8 -  by blast
    32.9 +definition "quot = {{x. a \<sim> x}| a::'a::partial_equiv. True}"
   32.10 +
   32.11 +typedef (open) 'a quot = "quot :: 'a::partial_equiv set set"
   32.12 +  unfolding quot_def by blast
   32.13  
   32.14  lemma quotI [intro]: "{x. a \<sim> x} \<in> quot"
   32.15    unfolding quot_def by blast
    33.1 --- a/src/HOL/ex/Refute_Examples.thy	Wed Nov 30 16:05:15 2011 +0100
    33.2 +++ b/src/HOL/ex/Refute_Examples.thy	Wed Nov 30 16:27:10 2011 +0100
    33.3 @@ -494,8 +494,10 @@
    33.4  
    33.5  text {* A completely unspecified non-empty subset of @{typ "'a"}: *}
    33.6  
    33.7 -typedef 'a myTdef = "insert (undefined::'a) (undefined::'a set)"
    33.8 -  by auto
    33.9 +definition "myTdef = insert (undefined::'a) (undefined::'a set)"
   33.10 +
   33.11 +typedef (open) 'a myTdef = "myTdef :: 'a set"
   33.12 +  unfolding myTdef_def by auto
   33.13  
   33.14  lemma "(x::'a myTdef) = y"
   33.15    refute
   33.16 @@ -503,8 +505,10 @@
   33.17  
   33.18  typedecl myTdecl
   33.19  
   33.20 -typedef 'a T_bij = "{(f::'a\<Rightarrow>'a). \<forall>y. \<exists>!x. f x = y}"
   33.21 -  by auto
   33.22 +definition "T_bij = {(f::'a\<Rightarrow>'a). \<forall>y. \<exists>!x. f x = y}"
   33.23 +
   33.24 +typedef (open) 'a T_bij = "T_bij :: ('a \<Rightarrow> 'a) set"
   33.25 +  unfolding T_bij_def by auto
   33.26  
   33.27  lemma "P (f::(myTdecl myTdef) T_bij)"
   33.28    refute