author wenzelm Wed Oct 10 17:43:23 2012 +0200 (2012-10-10) changeset 49812 e3945ddcb9aa parent 49811 3fc6b3289c31 child 49813 fe9eb2b5c1ec
eliminated some remaining uses of typedef with implicit set definition;
 src/Doc/IsarRef/HOL_Specific.thy file | annotate | diff | revisions src/Doc/Tutorial/Types/Typedefs.thy file | annotate | diff | revisions src/HOL/Library/Float.thy file | annotate | diff | revisions src/HOL/Nitpick_Examples/Manual_Nits.thy file | annotate | diff | revisions
1.1 --- a/src/Doc/IsarRef/HOL_Specific.thy	Wed Oct 10 16:41:19 2012 +0200
1.2 +++ b/src/Doc/IsarRef/HOL_Specific.thy	Wed Oct 10 17:43:23 2012 +0200
1.3 @@ -1189,7 +1189,7 @@
1.4    \medskip The following trivial example pulls a three-element type
1.5    into existence within the formal logical environment of HOL. *}
1.7 -typedef three = "{(True, True), (True, False), (False, True)}"
1.8 +typedef (open) three = "{(True, True), (True, False), (False, True)}"
1.9    by blast
1.11  definition "One = Abs_three (True, True)"
1.12 @@ -1197,11 +1197,11 @@
1.13  definition "Three = Abs_three (False, True)"
1.15  lemma three_distinct: "One \<noteq> Two"  "One \<noteq> Three"  "Two \<noteq> Three"
1.16 -  by (simp_all add: One_def Two_def Three_def Abs_three_inject three_def)
1.17 +  by (simp_all add: One_def Two_def Three_def Abs_three_inject)
1.19  lemma three_cases:
1.20    fixes x :: three obtains "x = One" | "x = Two" | "x = Three"
1.21 -  by (cases x) (auto simp: One_def Two_def Three_def Abs_three_inject three_def)
1.22 +  by (cases x) (auto simp: One_def Two_def Three_def Abs_three_inject)
1.24  text {* Note that such trivial constructions are better done with
1.25    derived specification mechanisms such as @{command datatype}: *}
2.1 --- a/src/Doc/Tutorial/Types/Typedefs.thy	Wed Oct 10 16:41:19 2012 +0200
2.2 +++ b/src/Doc/Tutorial/Types/Typedefs.thy	Wed Oct 10 17:43:23 2012 +0200
2.3 @@ -69,7 +69,7 @@
2.4  It is easily represented by the first three natural numbers:
2.5  *}
2.7 -typedef three = "{0::nat, 1, 2}"
2.8 +typedef (open) three = "{0::nat, 1, 2}"
2.10  txt{*\noindent
2.11  In order to enforce that the representing set on the right-hand side is
2.12 @@ -90,22 +90,17 @@
2.13  constants behind the scenes:
2.14  \begin{center}
2.15  \begin{tabular}{rcl}
2.16 -@{term three} &::& @{typ"nat set"} \\
2.17  @{term Rep_three} &::& @{typ"three \<Rightarrow> nat"}\\
2.18  @{term Abs_three} &::& @{typ"nat \<Rightarrow> three"}
2.19  \end{tabular}
2.20  \end{center}
2.21 -where constant @{term three} is explicitly defined as the representing set:
2.22 -\begin{center}
2.23 -@{thm three_def}\hfill(@{thm[source]three_def})
2.24 -\end{center}
2.25  The situation is best summarized with the help of the following diagram,
2.26  where squares denote types and the irregular region denotes a set:
2.27  \begin{center}
2.28  \includegraphics[scale=.8]{typedef}
2.29  \end{center}
2.30  Finally, \isacommand{typedef} asserts that @{term Rep_three} is
2.31 -surjective on the subset @{term three} and @{term Abs_three} and @{term
2.32 +surjective on the subset and @{term Abs_three} and @{term
2.33  Rep_three} are inverses of each other:
2.34  \begin{center}
2.36 @@ -153,7 +148,7 @@
2.37  \begin{tabular}{@ {}r@ {\qquad}l@ {}}
2.38  @{thm Rep_three_inject[no_vars]} & (@{thm[source]Rep_three_inject}) \\
2.39  \begin{tabular}{@ {}l@ {}}
2.40 -@{text"\<lbrakk>x \<in> three; y \<in> three \<rbrakk>"} \\
2.41 +@{text"\<lbrakk>x \<in> {0, 1, 2}; y \<in> {0, 1, 2} \<rbrakk>"} \\
2.42  @{text"\<Longrightarrow> (Abs_three x = Abs_three y) = (x = y)"}
2.43  \end{tabular} & (@{thm[source]Abs_three_inject}) \\
2.44  \end{tabular}
2.45 @@ -168,7 +163,7 @@
2.46  @{thm Abs_three_induct[no_vars]} & (@{thm[source]Abs_three_induct}) \\
2.47  \end{tabular}
2.48  \end{center}
2.49 -These theorems are proved for any type definition, with @{term three}
2.50 +These theorems are proved for any type definition, with @{text three}
2.51  replaced by the name of the type in question.
2.53  Distinctness of @{term A}, @{term B} and @{term C} follows immediately
2.54 @@ -177,7 +172,7 @@
2.55  *}
2.57  lemma "A \<noteq> B \<and> B \<noteq> A \<and> A \<noteq> C \<and> C \<noteq> A \<and> B \<noteq> C \<and> C \<noteq> B"
2.58 -by(simp add: Abs_three_inject A_def B_def C_def three_def)
2.59 +by(simp add: Abs_three_inject A_def B_def C_def)
2.61  text{*\noindent
2.62  Of course we rely on the simplifier to solve goals like @{prop"(0::nat) \<noteq> 1"}.
2.63 @@ -195,11 +190,11 @@
2.65  txt{*
2.66  @{subgoals[display,indent=0]}
2.67 -Simplification with @{thm[source]three_def} leads to the disjunction @{prop"y
2.68 +Simplification leads to the disjunction @{prop"y
2.69  = 0 \<or> y = 1 \<or> y = (2::nat)"} which \isa{auto} separates into three
2.70  subgoals, each of which is easily solved by simplification: *}
2.72 -apply(auto simp add: three_def A_def B_def C_def)
2.73 +apply(auto simp add: A_def B_def C_def)
2.74  done
2.76  text{*\noindent
3.1 --- a/src/HOL/Library/Float.thy	Wed Oct 10 16:41:19 2012 +0200
3.2 +++ b/src/HOL/Library/Float.thy	Wed Oct 10 17:43:23 2012 +0200
3.3 @@ -9,9 +9,11 @@
3.4  imports Complex_Main "~~/src/HOL/Library/Lattice_Algebras"
3.5  begin
3.7 -typedef float = "{m * 2 powr e | (m :: int) (e :: int). True }"
3.8 +definition "float = {m * 2 powr e | (m :: int) (e :: int). True}"
3.9 +
3.10 +typedef (open) float = float
3.11    morphisms real_of_float float_of
3.12 -  by auto
3.13 +  unfolding float_def by auto