# HG changeset patch
# User wenzelm
# Date 1028281795 -7200
# Node ID 1c3327c348b30c0b57ae059434430f738f887d06
# Parent  70479ec9f44f83e96aa16bb207f6723b99fb9f1f
typedef: "open" option;

diff -r 70479ec9f44f -r 1c3327c348b3 NEWS
--- a/NEWS	Fri Aug 02 11:12:34 2002 +0200
+++ b/NEWS	Fri Aug 02 11:49:55 2002 +0200
@@ -28,16 +28,23 @@
 
 *** HOL ***
 
-* attribute [symmetric] now works for relations as well. It turns
-  (x,y) : R^-1 into (y,x) : R, and vice versa.
-
-* arith(_tac) does now know about div k and mod k where k is a numeral of
-  type nat or int. It can solve simple goals like
+* 'typedef' command has new option "open" to suppress the set
+definition;
+
+* attribute [symmetric] now works for relations as well; it turns
+(x,y) : R^-1 into (y,x) : R, and vice versa;
+
+* arith(_tac) does now know about div k and mod k where k is a numeral
+of type nat or int. It can solve simple goals like
+
   "0 < n ==> n div 2 < (n::nat)"
-  but fails if divisibility plays a role like in
-  "n div 2 + (n+1) div 2 = (n::nat)".
-* simp's arithmetic capabilities have been enhanced a bit:
-  it now takes ~= in premises into account (by performing a case split).
+
+but fails if divisibility plays a role like in
+
+  "n div 2 + (n+1) div 2 = (n::nat)"
+
+* simp's arithmetic capabilities have been enhanced a bit: it now
+takes ~= in premises into account (by performing a case split);
 
 
 
diff -r 70479ec9f44f -r 1c3327c348b3 doc-src/IsarRef/logics.tex
--- a/doc-src/IsarRef/logics.tex	Fri Aug 02 11:12:34 2002 +0200
+++ b/doc-src/IsarRef/logics.tex	Fri Aug 02 11:49:55 2002 +0200
@@ -97,9 +97,11 @@
 \begin{rail}
   'typedecl' typespec infix?
   ;
-  'typedef' parname? abstype '=' repset
+  'typedef' altname? abstype '=' repset
   ;
 
+  altname = '(' (name | 'open' name?) ')'
+  ;
   abstype: typespec infix?
   ;
   repset: term ('morphisms' name name)?
@@ -132,6 +134,10 @@
   $Rep_t_cases/Rep_t_induct$, and $Abs_t_cases/Abs_t_induct$ provide
   alternative views on surjectivity; these are already declared as set or type
   rules for the generic $cases$ and $induct$ methods.
+  
+  An alternative name may be specified in parentheses; the default is to use
+  $t$ as indicated before.  The $open$ declaration suppresses a separate
+  constant definition for the representing set.
 \end{descr}
 
 Note that raw type declarations are rarely used in practice; the main
diff -r 70479ec9f44f -r 1c3327c348b3 src/HOL/Tools/typedef_package.ML
--- a/src/HOL/Tools/typedef_package.ML	Fri Aug 02 11:12:34 2002 +0200
+++ b/src/HOL/Tools/typedef_package.ML	Fri Aug 02 11:49:55 2002 +0200
@@ -22,10 +22,10 @@
     {type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm,
       Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm,
       Rep_induct: thm, Abs_induct: thm}
-  val typedef_proof: string * (bstring * string list * mixfix) * string * (string * string) option
-    -> bool -> theory -> ProofHistory.T
-  val typedef_proof_i: string * (bstring * string list * mixfix) * term * (string * string) option
-    -> bool -> theory -> ProofHistory.T
+  val typedef_proof: (bool * string) * (bstring * string list * mixfix) * string
+    * (string * string) option -> bool -> theory -> ProofHistory.T
+  val typedef_proof_i: (bool * string) * (bstring * string list * mixfix) * term
+    * (string * string) option -> bool -> theory -> ProofHistory.T
 end;
 
 structure TypedefPackage: TYPEDEF_PACKAGE =
@@ -238,10 +238,10 @@
 
 (* typedef_proof interface *)
 
-fun gen_typedef_proof prep_term (name, typ, set, opt_morphs) int thy =
+fun gen_typedef_proof prep_term ((def, name), typ, set, opt_morphs) int thy =
   let
     val (_, goal, goal_pat, att_result) =
-      prepare_typedef prep_term true name typ set opt_morphs thy;
+      prepare_typedef prep_term def name typ set opt_morphs thy;
     val att = #1 o att_result;
   in thy |> IsarThy.theorem_i Drule.internalK (("", [att]), (goal, ([goal_pat], []))) int end;
 
@@ -261,12 +261,14 @@
 
 
 val typedef_proof_decl =
-  Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") --
+  Scan.optional (P.$$$ "(" |-- P.!!!
+      (((P.$$$ "open" >> K false) -- Scan.option P.name || P.name >> (fn s => (true, Some s)))
+        --| P.$$$ ")")) (true, None) --
     (P.type_args -- P.name) -- P.opt_infix -- (P.$$$ "=" |-- P.term) --
     Scan.option (P.$$$ "morphisms" |-- P.!!! (P.name -- P.name));
 
-fun mk_typedef_proof ((((opt_name, (vs, t)), mx), A), morphs) =
-  typedef_proof (if_none opt_name (Syntax.type_name t mx), (t, vs, mx), A, morphs);
+fun mk_typedef_proof ((((((def, opt_name), (vs, t)), mx), A), morphs)) =
+  typedef_proof ((def, if_none opt_name (Syntax.type_name t mx)), (t, vs, mx), A, morphs);
 
 val typedefP =
   OuterSyntax.command "typedef" "HOL type definition (requires non-emptiness proof)" K.thy_goal