# HG changeset patch
# User berghofe
# Date 901277705 -7200
# Node ID d82a70766af0393a0dfe378cc519b5c5724a9289
# Parent  819f90f278db83daaf6c06ee7f72e3e69eee6005
Added new function add_typedef_i_no_def which doesn't add
definition of representing set to theory.

diff -r 819f90f278db -r d82a70766af0 src/HOL/Tools/typedef_package.ML
--- a/src/HOL/Tools/typedef_package.ML	Fri Jul 24 12:53:04 1998 +0200
+++ b/src/HOL/Tools/typedef_package.ML	Fri Jul 24 12:55:05 1998 +0200
@@ -13,6 +13,8 @@
     string -> string list -> thm list -> tactic option -> theory -> theory
   val add_typedef_i: string -> bstring * string list * mixfix ->
     term -> string list -> thm list -> tactic option -> theory -> theory
+  val add_typedef_i_no_def: string -> bstring * string list * mixfix ->
+    term -> string list -> thm list -> tactic option -> theory -> theory
 end;
 
 structure TypedefPackage: TYPEDEF_PACKAGE =
@@ -60,7 +62,7 @@
 
 (* gen_add_typedef *)
 
-fun gen_add_typedef prep_term name (t, vs, mx) raw_set axms thms usr_tac thy =
+fun gen_add_typedef prep_term no_def name (t, vs, mx) raw_set axms thms usr_tac thy =
   let
     val _ = Theory.requires thy "Set" "typedefs";
     val sign = sign_of thy;
@@ -87,11 +89,12 @@
     val AbsC = Const (full_name Abs_name, oldT --> newT);
     val x_new = Free ("x", newT);
     val y_old = Free ("y", oldT);
+    val set' = if no_def then set else setC;
 
     (*axioms*)
-    val rep_type = HOLogic.mk_Trueprop (HOLogic.mk_mem (RepC $ x_new, setC));
+    val rep_type = HOLogic.mk_Trueprop (HOLogic.mk_mem (RepC $ x_new, set'));
     val rep_type_inv = HOLogic.mk_Trueprop (HOLogic.mk_eq (AbsC $ (RepC $ x_new), x_new));
-    val abs_type_inv = Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (y_old, setC)),
+    val abs_type_inv = Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (y_old, set')),
       HOLogic.mk_Trueprop (HOLogic.mk_eq (RepC $ (AbsC $ y_old), y_old)));
 
 
@@ -128,11 +131,11 @@
     |> Theory.add_arities_i
      [(full_name tname, replicate (length vs) HOLogic.termS, HOLogic.termS)]
     |> Theory.add_consts_i
-     [(name, setT, NoSyn),
-      (Rep_name, newT --> oldT, NoSyn),
-      (Abs_name, oldT --> newT, NoSyn)]
-    |> (PureThy.add_defs_i o map Attribute.none)
-     [(name ^ "_def", Logic.mk_equals (setC, set))]
+     ((if no_def then [] else [(name, setT, NoSyn)]) @
+      [(Rep_name, newT --> oldT, NoSyn),
+       (Abs_name, oldT --> newT, NoSyn)])
+    |> (if no_def then I else (PureThy.add_defs_i o map Attribute.none)
+     [(name ^ "_def", Logic.mk_equals (setC, set))])
     |> (PureThy.add_axioms_i o map Attribute.none)
      [(Rep_name, rep_type),
       (Rep_name ^ "_inverse", rep_type_inv),
@@ -150,8 +153,9 @@
 fun cert_term sg tm =
   cterm_of sg tm handle TERM (msg, _) => error msg;
 
-val add_typedef = gen_add_typedef read_term;
-val add_typedef_i = gen_add_typedef cert_term;
+val add_typedef = gen_add_typedef read_term false;
+val add_typedef_i = gen_add_typedef cert_term false;
+val add_typedef_i_no_def = gen_add_typedef cert_term true;
 
 
 end;