# HG changeset patch
# User wenzelm
# Date 1003343119 -7200
# Node ID 122834177ec1a329010f8adfdd5ffdf5bab28eed
# Parent  ad32c92435dbeee79d3cd8b14e29ec5e01798b6a
improved internal interface of typedef;

diff -r ad32c92435db -r 122834177ec1 src/HOL/Tools/datatype_rep_proofs.ML
--- a/src/HOL/Tools/datatype_rep_proofs.ML	Wed Oct 17 20:24:37 2001 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Wed Oct 17 20:25:19 2001 +0200
@@ -181,9 +181,9 @@
 
     val thy3 = add_path flat_names big_name (foldl (fn (thy, ((((name, mx), tvs), c), name')) =>
       setmp TypedefPackage.quiet_mode true
-        (TypedefPackage.add_typedef_i_no_def name' (name, tvs, mx) c [] []
-          (Some (QUIET_BREADTH_FIRST (has_fewer_prems 1)
-            (resolve_tac (Funs_nonempty::rep_intrs) 1)))) thy |> #1)
+        (TypedefPackage.add_typedef_i false name' (name, tvs, mx) c None
+          (QUIET_BREADTH_FIRST (has_fewer_prems 1)
+            (resolve_tac (Funs_nonempty::rep_intrs) 1))) thy |> #1)
               (parent_path flat_names thy2, types_syntax ~~ tyvars ~~
                 (take (length newTs, consts)) ~~ new_type_names));
 
diff -r ad32c92435db -r 122834177ec1 src/HOL/Tools/typedef_package.ML
--- a/src/HOL/Tools/typedef_package.ML	Wed Oct 17 20:24:37 2001 +0200
+++ b/src/HOL/Tools/typedef_package.ML	Wed Oct 17 20:25:19 2001 +0200
@@ -10,14 +10,18 @@
 sig
   val quiet_mode: bool ref
   val add_typedecls: (bstring * string list * mixfix) list -> theory -> theory
-  val add_typedef: string -> bstring * string list * mixfix ->
-    string -> string list -> thm list -> tactic option -> theory -> theory * thm
-  val add_typedef_no_result: string -> bstring * string list * mixfix ->
+  val add_typedef_x: string -> bstring * string list * mixfix ->
     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 * thm
-  val add_typedef_i_no_def: string -> bstring * string list * mixfix ->
-    term -> string list -> thm list -> tactic option -> theory -> theory * thm
+  val add_typedef: bool -> string -> bstring * string list * mixfix ->
+    string -> (bstring * bstring) option -> tactic -> theory -> theory *
+    {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 add_typedef_i: bool -> string -> bstring * string list * mixfix ->
+    term -> (bstring * bstring) option -> tactic -> theory -> theory *
+    {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) * Comment.text
     -> bool -> theory -> ProofHistory.T
@@ -100,7 +104,7 @@
 fun err_in_typedef name =
   error ("The error(s) above occurred in typedef " ^ quote name);
 
-fun prepare_typedef prep_term no_def name (t, vs, mx) raw_set opt_morphs thy =
+fun prepare_typedef prep_term def name (t, vs, mx) raw_set opt_morphs thy =
   let
     val _ = Theory.requires thy "Typedef" "typedefs";
     val sign = Theory.sign_of thy;
@@ -133,7 +137,7 @@
     val x_new = Free ("x", newT);
     val y_old = Free ("y", oldT);
 
-    val set' = if no_def then set else setC;
+    val set' = if def then setC else set;
 
     val typedef_name = "type_definition_" ^ name;
     val typedefC =
@@ -141,35 +145,42 @@
     val typedef_prop =
       Logic.mk_implies (goal, HOLogic.mk_Trueprop (typedefC $ RepC $ AbsC $ set'));
 
-    fun typedef_att (theory, nonempty) =
+    fun typedef_result (theory, nonempty) =
       theory
       |> add_typedecls [(t, vs, mx)]
       |> Theory.add_consts_i
-       ((if no_def then [] else [(name, setT, NoSyn)]) @
+       ((if def then [(name, setT, NoSyn)] else []) @
         [(Rep_name, newT --> oldT, NoSyn),
          (Abs_name, oldT --> newT, NoSyn)])
-      |> (if no_def then I else (#1 oo (PureThy.add_defs_i false o map Thm.no_attributes))
-       [Logic.mk_defpair (setC, set)])
-      |> PureThy.add_axioms_i [((typedef_name, typedef_prop),
+      |> (if def then (apsnd (Some o hd) oo (PureThy.add_defs_i false o map Thm.no_attributes))
+           [Logic.mk_defpair (setC, set)]
+          else rpair None)
+      |>> PureThy.add_axioms_i [((typedef_name, typedef_prop),
           [apsnd (fn cond_axm => Drule.standard (nonempty RS cond_axm))])]
-      |> (fn (theory', axm) =>
-        let fun make th = Drule.standard (th OF axm) in
-          rpair (hd axm) (theory'
-          |> (#1 oo PureThy.add_thms)
-            ([((Rep_name, make Rep), []),
-              ((Rep_name ^ "_inverse", make Rep_inverse), []),
-              ((Abs_name ^ "_inverse", make Abs_inverse), []),
-              ((Rep_name ^ "_inject", make Rep_inject), []),
-              ((Abs_name ^ "_inject", make Abs_inject), []),
-              ((Rep_name ^ "_cases", make Rep_cases),
-                [RuleCases.case_names [Rep_name], InductAttrib.cases_set_global full_name]),
-              ((Abs_name ^ "_cases", make Abs_cases),
-                [RuleCases.case_names [Abs_name], InductAttrib.cases_type_global full_tname]),
-              ((Rep_name ^ "_induct", make Rep_induct),
-                [RuleCases.case_names [Rep_name], InductAttrib.induct_set_global full_name]),
-              ((Abs_name ^ "_induct", make Abs_induct),
-                [RuleCases.case_names [Abs_name], InductAttrib.induct_type_global full_tname])]))
-        end);
+      |> (fn ((theory', [type_definition]), set_def) =>
+        let
+          fun make th = Drule.standard (th OF [type_definition]);
+          val (theory'', [Rep, Rep_inverse, Abs_inverse, Rep_inject, Abs_inject,
+              Rep_cases, Abs_cases, Rep_induct, Abs_induct]) =
+            theory' |> PureThy.add_thms
+              ([((Rep_name, make Rep), []),
+                ((Rep_name ^ "_inverse", make Rep_inverse), []),
+                ((Abs_name ^ "_inverse", make Abs_inverse), []),
+                ((Rep_name ^ "_inject", make Rep_inject), []),
+                ((Abs_name ^ "_inject", make Abs_inject), []),
+                ((Rep_name ^ "_cases", make Rep_cases),
+                  [RuleCases.case_names [Rep_name], InductAttrib.cases_set_global full_name]),
+                ((Abs_name ^ "_cases", make Abs_cases),
+                  [RuleCases.case_names [Abs_name], InductAttrib.cases_type_global full_tname]),
+                ((Rep_name ^ "_induct", make Rep_induct),
+                  [RuleCases.case_names [Rep_name], InductAttrib.induct_set_global full_name]),
+                ((Abs_name ^ "_induct", make Abs_induct),
+                  [RuleCases.case_names [Abs_name], InductAttrib.induct_type_global full_tname])]);
+          val result = {type_definition = type_definition, set_def = set_def,
+            Rep = Rep, Rep_inverse = Rep_inverse, Abs_inverse = Abs_inverse,
+            Rep_inject = Rep_inject, Abs_inject = Abs_inject, Rep_cases = Rep_cases,
+            Abs_cases = Abs_cases, Rep_induct = Rep_induct, Abs_induct = Abs_induct};
+        in ((theory'', type_definition), result) end);
 
 
     (* errors *)
@@ -198,32 +209,41 @@
     (*test theory errors now!*)
     val test_thy = Theory.copy thy;
     val _ = (test_thy,
-      setmp quick_and_dirty true (SkipProof.make_thm test_thy) goal) |> typedef_att;
+      setmp quick_and_dirty true (SkipProof.make_thm test_thy) goal) |> typedef_result;
 
-  in (cset, goal, goal_pat, typedef_att) end
+  in (cset, goal, goal_pat, typedef_result) end
   handle ERROR => err_in_typedef name;
 
 
 (* add_typedef interfaces *)
 
-fun gen_add_typedef prep_term no_def name typ set names thms tac thy =
+fun gen_typedef prep_term def name typ set opt_morphs names thms tac thy =
   let
-    val (cset, goal, _, typedef_att) = prepare_typedef prep_term no_def name typ set None thy;
-    val result = prove_nonempty thy cset goal (names, thms, tac);
-  in (thy, result) |> typedef_att end;
+    val (cset, goal, _, typedef_result) =
+      prepare_typedef prep_term def name typ set opt_morphs thy;
+    val non_empty = prove_nonempty thy cset goal (names, thms, tac);
+    val ((thy', _), result) = (thy, non_empty) |> typedef_result;
+  in (thy', result) end;
 
-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;
-fun add_typedef_no_result x y z = #1 oooo add_typedef x y z;
+fun sane_typedef prep_term def name typ set opt_morphs tac =
+  gen_typedef prep_term def name typ set opt_morphs [] [] (Some tac);
+
+fun add_typedef_x name typ set names thms tac =
+  #1 o gen_typedef read_term true name typ set None names thms tac;
+
+val add_typedef = sane_typedef read_term;
+val add_typedef_i = sane_typedef cert_term;
 
 
 (* typedef_proof interface *)
 
 fun gen_typedef_proof prep_term ((name, typ, set, opt_morphs), comment) int thy =
-  let val (_, goal, goal_pat, att) = prepare_typedef prep_term false name typ set opt_morphs thy in
-    thy |>
-    IsarThy.theorem_i Drule.internalK ((("", [att]), (goal, ([goal_pat], []))), comment) int
+  let
+    val (_, goal, goal_pat, att_result) =
+      prepare_typedef prep_term true name typ set opt_morphs thy;
+    val att = #1 o att_result;
+  in
+    thy |> IsarThy.theorem_i Drule.internalK ((("", [att]), (goal, ([goal_pat], []))), comment) int
   end;
 
 val typedef_proof = gen_typedef_proof read_term;
diff -r ad32c92435db -r 122834177ec1 src/HOL/thy_syntax.ML
--- a/src/HOL/thy_syntax.ML	Wed Oct 17 20:24:37 2001 +0200
+++ b/src/HOL/thy_syntax.ML	Wed Oct 17 20:25:19 2001 +0200
@@ -280,7 +280,7 @@
 val _ = ThySyn.add_syntax
  ["intrs", "monos", "con_defs", "congs", "simpset", "|",
   "and", "distinct", "inject", "induct"]
- [axm_section "typedef" "|> TypedefPackage.add_typedef_no_result" typedef_decl,
+ [axm_section "typedef" "|> TypedefPackage.add_typedef_x" typedef_decl,
   section "record" "|> (#1 oooo RecordPackage.add_record)" record_decl,
   section "inductive" 	"" (inductive_decl false),
   section "coinductive"	"" (inductive_decl true),