src/HOL/Tools/typedef_package.ML

 signature TYPEDEF_PACKAGE =
 sig
   val quiet_mode: bool ref
   val add_typedecls: (bstring * string list * mixfix) list -> theory -> theory
   val add_typedef: bool -> string option -> bstring * string list * mixfix ->
-    string -> (bstring * bstring) option -> tactic -> theory -> theory *
+    string -> (bstring * bstring) option -> tactic -> 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}
+      Rep_induct: thm, Abs_induct: thm} * theory
   val add_typedef_i: bool -> string option -> bstring * string list * mixfix ->
-    term -> (bstring * bstring) option -> tactic -> theory -> theory *
+    term -> (bstring * bstring) option -> tactic -> 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}
+      Rep_induct: thm, Abs_induct: thm} * theory
   val typedef: (bool * string) * (bstring * string list * mixfix) * string
     * (string * string) option -> theory -> Proof.state
   val typedef_i: (bool * string) * (bstring * string list * mixfix) * term
     * (string * string) option -> theory -> Proof.state
   val setup: theory -> theory
+  structure TypedefData : THEORY_DATA
 end;
 
 structure TypedefPackage: TYPEDEF_PACKAGE =
 struct
 

 (* theory data *)
 
 structure TypedefData = TheoryDataFun
 (struct
   val name = "HOL/typedef";
-  type T = (typ * typ * string * string) Symtab.table;
+  type T = ((typ * typ * string * string) * (thm option * thm * thm)) Symtab.table;
   val empty = Symtab.empty;
   val copy = I;
   val extend = I;
   fun merge _ (tabs: T * T) = Symtab.merge (op =) tabs;
   fun print _ _ = ();
 end);
 
-fun put_typedef newT oldT Abs_name Rep_name =
-  TypedefData.map (Symtab.update_new (fst (dest_Type newT), (newT, oldT, Abs_name, Rep_name)));
+fun put_typedef newT oldT Abs_name Rep_name def inject inverse =
+  TypedefData.map (Symtab.update_new (fst (dest_Type newT),
+    ((newT, oldT, Abs_name, Rep_name), (def, inject, inverse))));
 
 
 (* prepare_typedef *)
 
 fun read_term thy used s =

         |> PureThy.add_defs_i false [Thm.no_attributes def']
         |-> (fn [def'] => pair (SOME def'))
       else
         (NONE, thy);
 
-    fun typedef_result (context, nonempty) =
+    fun typedef_result nonempty context =
       Context.the_theory context
-      |> put_typedef newT oldT (full Abs_name) (full Rep_name)
       |> add_typedecls [(t, vs, mx)]
       |> Theory.add_consts_i
        ((if def then [(name, setT', NoSyn)] else []) @
         [(Rep_name, newT --> oldT, NoSyn),
          (Abs_name, oldT --> newT, NoSyn)])

           [apsnd (fn cond_axm => Drule.standard (nonempty RS cond_axm))])]
       ||> Theory.add_finals_i false [RepC, AbsC]
       |-> (fn (set_def, [type_definition]) => fn theory' =>
         let
           fun make th = Drule.standard (th OF [type_definition]);
+          val abs_inject = make Abs_inject;
+          val abs_inverse = make Abs_inverse;
           val ([Rep, Rep_inverse, Abs_inverse, Rep_inject, Abs_inject,
               Rep_cases, Abs_cases, Rep_induct, Abs_induct], theory'') =
             theory'
             |> Theory.add_path name
             |> PureThy.add_thms
               ([((Rep_name, make Rep), []),
                 ((Rep_name ^ "_inverse", make Rep_inverse), []),
-                ((Abs_name ^ "_inverse", make Abs_inverse), []),
+                ((Abs_name ^ "_inverse", abs_inverse), []),
                 ((Rep_name ^ "_inject", make Rep_inject), []),
-                ((Abs_name ^ "_inject", make Abs_inject), []),
+                ((Abs_name ^ "_inject", abs_inject), []),
                 ((Rep_name ^ "_cases", make Rep_cases),
                   [RuleCases.case_names [Rep_name], InductAttrib.cases_set full_name]),
                 ((Abs_name ^ "_cases", make Abs_cases),
                   [RuleCases.case_names [Abs_name], InductAttrib.cases_type full_tname]),
                 ((Rep_name ^ "_induct", make Rep_induct),
                   [RuleCases.case_names [Rep_name], InductAttrib.induct_set full_name]),
                 ((Abs_name ^ "_induct", make Abs_induct),
                   [RuleCases.case_names [Abs_name], InductAttrib.induct_type full_tname])])
-            ||> Theory.parent_path;
+            ||> Theory.parent_path
+            ||> put_typedef newT oldT (full Abs_name) (full Rep_name)
+                 set_def abs_inject abs_inverse
           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 ((Context.Theory theory'', type_definition), result) end);
+        in ((type_definition, result), Context.Theory theory'') end);
 
 
     (* errors *)
 
     fun show_names pairs = commas_quote (map fst pairs);

     val errs = illegal_vars @ dup_lhs_tfrees @ extra_rhs_tfrees @ illegal_frees;
     val _ = if null errs then () else error (cat_lines errs);
 
     (*test theory errors now!*)
     val test_thy = Theory.copy thy;
-    val _ = (Context.Theory test_thy,
-      setmp quick_and_dirty true (SkipProof.make_thm test_thy) goal) |> typedef_result;
+    val _ = 
+      Context.Theory test_thy
+      |> typedef_result (setmp quick_and_dirty true (SkipProof.make_thm test_thy) goal);
 
   in (cset, goal, goal_pat, typedef_result) end
   handle ERROR msg => err_in_typedef msg name;
 
 

     val (cset, goal, _, typedef_result) =
       prepare_typedef prep_term def name typ set opt_morphs thy;
     val _ = message ("Proving non-emptiness of set " ^ quote (string_of_cterm cset) ^ " ...");
     val non_empty = Goal.prove thy [] [] goal (K tac) handle ERROR msg =>
       cat_error msg ("Failed to prove non-emptiness of " ^ quote (string_of_cterm cset));
-    val (thy', result) =
-      (Context.Theory thy, non_empty) |> typedef_result |>> (Context.the_theory o fst);
-  in (thy', result) end;
+  in
+    Context.Theory thy
+    |> typedef_result non_empty
+    ||> Context.the_theory
+    |-> (fn (_, result) => pair result)
+  end;
 
 in
 
 val add_typedef = gen_typedef read_term;
 val add_typedef_i = gen_typedef cert_term;

 
 fun gen_typedef prep_term ((def, name), typ, set, opt_morphs) thy =
   let
     val (_, goal, goal_pat, att_result) =
       prepare_typedef prep_term def name typ set opt_morphs thy;
-    val att = #1 o att_result;
+    fun att (thy, th) =
+      let val ((th', _), thy') = att_result th thy
+      in (thy', th') end;
   in IsarThy.theorem_i PureThy.internalK ("", [att]) (goal, ([goal_pat], [])) thy end;
 
 in
 
 val typedef = gen_typedef read_term;

         val id = Codegen.mk_qual_id module (Codegen.get_const_id s gr'')
       in SOME (gr'', Codegen.mk_app brack (Pretty.str id) ps) end;
     fun lookup f T =
       (case Symtab.lookup (TypedefData.get thy) (get_name T) of
         NONE => ""
-      | SOME s => f s);
+      | SOME (s, _) => f s);
   in
     (case strip_comb t of
        (Const (s, Type ("fun", [T, U])), ts) =>
          if lookup #4 T = s andalso
            is_none (Codegen.get_assoc_type thy (get_name T))

   | mk_tyexpr ps s = Pretty.list "(" (") " ^ s) ps;
 
 fun typedef_tycodegen thy defs gr dep module brack (Type (s, Ts)) =
       (case Symtab.lookup (TypedefData.get thy) s of
          NONE => NONE
-       | SOME (newT as Type (tname, Us), oldT, Abs_name, Rep_name) =>
+       | SOME ((newT as Type (tname, Us), oldT, Abs_name, Rep_name), _) =>
            if is_some (Codegen.get_assoc_type thy tname) then NONE else
            let
              val module' = Codegen.if_library
                (Codegen.thyname_of_type tname thy) module;
              val node_id = tname ^ " (type)";

                in Codegen.map_node node_id (K (NONE, module', s)) gr'' end
              | SOME _ => Codegen.add_edge (node_id, dep) gr', tyexpr)
            end)
   | typedef_tycodegen thy defs gr dep module brack _ = NONE;
 
+fun typedef_type_extr thy tyco =
+  case Symtab.lookup (TypedefData.get thy) tyco
+   of SOME ((ty_abs, ty_rep, c_abs, c_rep), (SOME def, inject, _)) =>
+        let
+          val exists_thm =
+            UNIV_I
+            |> Drule.instantiate' [SOME (ctyp_of thy ty_rep)] []
+            |> rewrite_rule [symmetric def];
+        in case try (Tactic.rule_by_tactic ((ALLGOALS o resolve_tac) [exists_thm])) inject
+         of SOME eq_thm => SOME (((Term.typ_tfrees o Type.no_tvars) ty_abs, [(c_abs, [ty_rep])]),
+             (ALLGOALS o resolve_tac) [eq_reflection]
+            THEN (ALLGOALS o resolve_tac) [eq_thm])
+          | NONE => NONE
+        end
+    | _ => NONE;
+
+fun typedef_fun_extr thy (c, ty) =
+  case (fst o strip_type) ty
+   of Type (tyco, _) :: _ =>
+    (case Symtab.lookup (TypedefData.get thy) tyco
+     of SOME ((ty_abs, ty_rep, c_abs, c_rep), (SOME def, _, inverse)) =>
+          if c = c_rep then
+            let
+              val exists_thm =
+                UNIV_I
+                |> Drule.instantiate' [SOME (ctyp_of thy ty_rep)] []
+                |> rewrite_rule [symmetric def]
+            in case try (Tactic.rule_by_tactic ((ALLGOALS o resolve_tac) [exists_thm])) inverse
+             of SOME eq_thm => SOME [eq_thm]
+              | NONE => NONE
+            end
+          else NONE
+      | _ => NONE)
+    | _ => NONE;
+
 val setup =
-  TypedefData.init #>
-  Codegen.add_codegen "typedef" typedef_codegen #>
-  Codegen.add_tycodegen "typedef" typedef_tycodegen;
+  TypedefData.init
+  #> Codegen.add_codegen "typedef" typedef_codegen
+  #> Codegen.add_tycodegen "typedef" typedef_tycodegen
+  #> CodegenTheorems.add_fun_extr (these oo typedef_fun_extr)
+  #> CodegenTheorems.add_datatype_extr typedef_type_extr
 
 
 
 (** outer syntax **)