# HG changeset patch
# User wenzelm
# Date 1349883803 -7200
# Node ID e3945ddcb9aa8c707ae0f915471147fa9c77e086
# Parent  3fc6b3289c31a2204748fe04fb219a140ada5a2e
eliminated some remaining uses of typedef with implicit set definition;

diff -r 3fc6b3289c31 -r e3945ddcb9aa src/Doc/IsarRef/HOL_Specific.thy
--- a/src/Doc/IsarRef/HOL_Specific.thy	Wed Oct 10 16:41:19 2012 +0200
+++ b/src/Doc/IsarRef/HOL_Specific.thy	Wed Oct 10 17:43:23 2012 +0200
@@ -1189,7 +1189,7 @@
   \medskip The following trivial example pulls a three-element type
   into existence within the formal logical environment of HOL. *}
 
-typedef three = "{(True, True), (True, False), (False, True)}"
+typedef (open) three = "{(True, True), (True, False), (False, True)}"
   by blast
 
 definition "One = Abs_three (True, True)"
@@ -1197,11 +1197,11 @@
 definition "Three = Abs_three (False, True)"
 
 lemma three_distinct: "One \<noteq> Two"  "One \<noteq> Three"  "Two \<noteq> Three"
-  by (simp_all add: One_def Two_def Three_def Abs_three_inject three_def)
+  by (simp_all add: One_def Two_def Three_def Abs_three_inject)
 
 lemma three_cases:
   fixes x :: three obtains "x = One" | "x = Two" | "x = Three"
-  by (cases x) (auto simp: One_def Two_def Three_def Abs_three_inject three_def)
+  by (cases x) (auto simp: One_def Two_def Three_def Abs_three_inject)
 
 text {* Note that such trivial constructions are better done with
   derived specification mechanisms such as @{command datatype}: *}
diff -r 3fc6b3289c31 -r e3945ddcb9aa src/Doc/Tutorial/Types/Typedefs.thy
--- a/src/Doc/Tutorial/Types/Typedefs.thy	Wed Oct 10 16:41:19 2012 +0200
+++ b/src/Doc/Tutorial/Types/Typedefs.thy	Wed Oct 10 17:43:23 2012 +0200
@@ -69,7 +69,7 @@
 It is easily represented by the first three natural numbers:
 *}
 
-typedef three = "{0::nat, 1, 2}"
+typedef (open) three = "{0::nat, 1, 2}"
 
 txt{*\noindent
 In order to enforce that the representing set on the right-hand side is
@@ -90,22 +90,17 @@
 constants behind the scenes:
 \begin{center}
 \begin{tabular}{rcl}
-@{term three} &::& @{typ"nat set"} \\
 @{term Rep_three} &::& @{typ"three \<Rightarrow> nat"}\\
 @{term Abs_three} &::& @{typ"nat \<Rightarrow> three"}
 \end{tabular}
 \end{center}
-where constant @{term three} is explicitly defined as the representing set:
-\begin{center}
-@{thm three_def}\hfill(@{thm[source]three_def})
-\end{center}
 The situation is best summarized with the help of the following diagram,
 where squares denote types and the irregular region denotes a set:
 \begin{center}
 \includegraphics[scale=.8]{typedef}
 \end{center}
 Finally, \isacommand{typedef} asserts that @{term Rep_three} is
-surjective on the subset @{term three} and @{term Abs_three} and @{term
+surjective on the subset and @{term Abs_three} and @{term
 Rep_three} are inverses of each other:
 \begin{center}
 \begin{tabular}{@ {}r@ {\qquad\qquad}l@ {}}
@@ -153,7 +148,7 @@
 \begin{tabular}{@ {}r@ {\qquad}l@ {}}
 @{thm Rep_three_inject[no_vars]} & (@{thm[source]Rep_three_inject}) \\
 \begin{tabular}{@ {}l@ {}}
-@{text"\<lbrakk>x \<in> three; y \<in> three \<rbrakk>"} \\
+@{text"\<lbrakk>x \<in> {0, 1, 2}; y \<in> {0, 1, 2} \<rbrakk>"} \\
 @{text"\<Longrightarrow> (Abs_three x = Abs_three y) = (x = y)"}
 \end{tabular} & (@{thm[source]Abs_three_inject}) \\
 \end{tabular}
@@ -168,7 +163,7 @@
 @{thm Abs_three_induct[no_vars]} & (@{thm[source]Abs_three_induct}) \\
 \end{tabular}
 \end{center}
-These theorems are proved for any type definition, with @{term three}
+These theorems are proved for any type definition, with @{text three}
 replaced by the name of the type in question.
 
 Distinctness of @{term A}, @{term B} and @{term C} follows immediately
@@ -177,7 +172,7 @@
 *}
 
 lemma "A \<noteq> B \<and> B \<noteq> A \<and> A \<noteq> C \<and> C \<noteq> A \<and> B \<noteq> C \<and> C \<noteq> B"
-by(simp add: Abs_three_inject A_def B_def C_def three_def)
+by(simp add: Abs_three_inject A_def B_def C_def)
 
 text{*\noindent
 Of course we rely on the simplifier to solve goals like @{prop"(0::nat) \<noteq> 1"}.
@@ -195,11 +190,11 @@
 
 txt{*
 @{subgoals[display,indent=0]}
-Simplification with @{thm[source]three_def} leads to the disjunction @{prop"y
+Simplification leads to the disjunction @{prop"y
 = 0 \<or> y = 1 \<or> y = (2::nat)"} which \isa{auto} separates into three
 subgoals, each of which is easily solved by simplification: *}
 
-apply(auto simp add: three_def A_def B_def C_def)
+apply(auto simp add: A_def B_def C_def)
 done
 
 text{*\noindent
diff -r 3fc6b3289c31 -r e3945ddcb9aa src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Wed Oct 10 16:41:19 2012 +0200
+++ b/src/HOL/Library/Float.thy	Wed Oct 10 17:43:23 2012 +0200
@@ -9,9 +9,11 @@
 imports Complex_Main "~~/src/HOL/Library/Lattice_Algebras"
 begin
 
-typedef float = "{m * 2 powr e | (m :: int) (e :: int). True }"
+definition "float = {m * 2 powr e | (m :: int) (e :: int). True}"
+
+typedef (open) float = float
   morphisms real_of_float float_of
-  by auto
+  unfolding float_def by auto
 
 defs (overloaded)
   real_of_float_def[code_unfold]: "real \<equiv> real_of_float"
diff -r 3fc6b3289c31 -r e3945ddcb9aa src/HOL/Nitpick_Examples/Manual_Nits.thy
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Wed Oct 10 16:41:19 2012 +0200
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Wed Oct 10 17:43:23 2012 +0200
@@ -94,8 +94,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"