eliminated some remaining uses of typedef with implicit set definition;
authorwenzelm
Wed Oct 10 17:43:23 2012 +0200 (2012-10-10)
changeset 49812e3945ddcb9aa
parent 49811 3fc6b3289c31
child 49813 fe9eb2b5c1ec
eliminated some remaining uses of typedef with implicit set definition;
src/Doc/IsarRef/HOL_Specific.thy
src/Doc/Tutorial/Types/Typedefs.thy
src/HOL/Library/Float.thy
src/HOL/Nitpick_Examples/Manual_Nits.thy
     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.6  
     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.10  
    1.11  definition "One = Abs_three (True, True)"
    1.12 @@ -1197,11 +1197,11 @@
    1.13  definition "Three = Abs_three (False, True)"
    1.14  
    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.18  
    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.23  
    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.6  
     2.7 -typedef three = "{0::nat, 1, 2}"
     2.8 +typedef (open) three = "{0::nat, 1, 2}"
     2.9  
    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.35  \begin{tabular}{@ {}r@ {\qquad\qquad}l@ {}}
    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.52  
    2.53  Distinctness of @{term A}, @{term B} and @{term C} follows immediately
    2.54 @@ -177,7 +172,7 @@
    2.55  *}
    2.56  
    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.60  
    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.64  
    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.71  
    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.75  
    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.6  
     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
    3.14  
    3.15  defs (overloaded)
    3.16    real_of_float_def[code_unfold]: "real \<equiv> real_of_float"
     4.1 --- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Wed Oct 10 16:41:19 2012 +0200
     4.2 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Wed Oct 10 17:43:23 2012 +0200
     4.3 @@ -94,8 +94,9 @@
     4.4  
     4.5  subsection {* 2.7. Typedefs, Records, Rationals, and Reals *}
     4.6  
     4.7 -typedef three = "{0\<Colon>nat, 1, 2}"
     4.8 -by blast
     4.9 +definition "three = {0\<Colon>nat, 1, 2}"
    4.10 +typedef (open) three = three
    4.11 +  unfolding three_def by blast
    4.12  
    4.13  definition A :: three where "A \<equiv> Abs_three 0"
    4.14  definition B :: three where "B \<equiv> Abs_three 1"