# HG changeset patch
# User haftmann
# Date 1156854673 -7200
# Node ID 9ffea7a8b31c56765b083d9100ec3e88d6b407fe
# Parent  dc1e8c24a475c0dc77162a05933d9400d527eaea
added typecopy_package

diff -r dc1e8c24a475 -r 9ffea7a8b31c src/HOL/Tools/datatype_codegen.ML
--- a/src/HOL/Tools/datatype_codegen.ML	Tue Aug 29 14:31:12 2006 +0200
+++ b/src/HOL/Tools/datatype_codegen.ML	Tue Aug 29 14:31:13 2006 +0200
@@ -2,11 +2,12 @@
     ID:         $Id$
     Author:     Stefan Berghofer & Florian Haftmann, TU Muenchen
 
-Code generator for inductive datatypes.
+Code generator for inductive datatypes and type copies ("code types").
 *)
 
 signature DATATYPE_CODEGEN =
 sig
+  val get_eq: theory -> string -> thm list
   val get_datatype_spec_thms: theory -> string
     -> (((string * sort) list * (string * typ list) list) * tactic) option
   val datatype_tac: theory -> string -> tactic
@@ -14,15 +15,19 @@
     -> ((string * typ) list * ((term * typ) * (term * term) list)) option
   val add_datatype_case_const: string -> theory -> theory
   val add_datatype_case_defs: string -> theory -> theory
-  val datatypes_dependency: theory -> string list list
-  val add_hook_bootstrap: DatatypeHooks.hook -> theory -> theory
-  val get_datatype_mut_specs: theory -> string list
-    -> ((string * sort) list * (string * (string * typ list) list) list)
-  val get_datatype_arities: theory -> string list -> sort
+
+  type hook = (string * (bool * ((string * sort) list * (string * typ list) list))) list
+    -> theory -> theory
+  val codetypes_dependency: theory -> (string * bool) list list
+  val add_codetypes_hook_bootstrap: hook -> theory -> theory
+  val the_codetypes_mut_specs: theory -> (string * bool) list
+    -> ((string * sort) list * (string * (bool * (string * typ list) list)) list)
+  val get_codetypes_arities: theory -> (string * bool) list -> sort
     -> (string * (((string * sort list) * sort) * term list)) list option
-  val prove_arities: (thm list -> tactic) -> string list -> sort
+  val prove_codetypes_arities: (thm list -> tactic) -> (string * bool) list -> sort
     -> (theory -> ((string * sort list) * sort) list -> (string * term list) list
     -> ((bstring * attribute list) * term) list) -> theory -> theory
+
   val setup: theory -> theory
 end;
 
@@ -313,87 +318,7 @@
   | datatype_tycodegen _ _ _ _ _ _ _ = NONE;
 
 
-(** code 2nd generation **)
-
-fun datatypes_dependency thy =
-  let
-    val dtnames = DatatypePackage.get_datatypes thy;
-    fun add_node (dtname, _) =
-      let
-        fun add_tycos (Type (tyco, tys)) = insert (op =) tyco #> fold add_tycos tys
-          | add_tycos _ = I;
-        val deps = (filter (Symtab.defined dtnames) o maps (fn ty =>
-          add_tycos ty [])
-            o maps snd o snd o the o DatatypePackage.get_datatype_spec thy) dtname
-      in
-        Graph.default_node (dtname, ())
-        #> fold (fn dtname' =>
-             Graph.default_node (dtname', ())
-             #> Graph.add_edge (dtname', dtname)
-           ) deps
-      end
-  in
-    Graph.empty
-    |> Symtab.fold add_node dtnames
-    |> Graph.strong_conn
-  end;
-
-fun add_hook_bootstrap hook thy =
-  thy
-  |> fold hook (datatypes_dependency thy)
-  |> DatatypeHooks.add hook;
-
-fun get_datatype_mut_specs thy (tycos as tyco :: _) =
-  let
-    val tycos' = (map (#1 o snd) o #descr o DatatypePackage.the_datatype thy) tyco;
-    val _ = if gen_subset (op =) (tycos, tycos') then () else
-      error ("datatype constructors are not mutually recursive: " ^ (commas o map quote) tycos);
-    val (vs::_, css) = split_list (map (the o DatatypePackage.get_datatype_spec thy) tycos);
-  in (vs, tycos ~~ css) end;
-
-fun get_datatype_arities thy tycos sort =
-  let
-    val algebra = Sign.classes_of thy;
-    val (vs_proto, css_proto) = get_datatype_mut_specs thy tycos;
-    val vs = map (fn (v, vsort) => (v, Sorts.inter_sort algebra (vsort, sort))) vs_proto;
-    fun inst_type tyco (c, tys) =
-      let
-        val tys' = (map o map_atyps)
-          (fn TFree (v, _) => TFree (v, the (AList.lookup (op =) vs v))) tys
-      in (c, tys') end;
-    val css = map (fn (tyco, cs) => (tyco, (map (inst_type tyco) cs))) css_proto;
-    fun mk_arity tyco =
-      ((tyco, map snd vs), sort);
-    fun typ_of_sort ty =
-      let
-        val arities = map (fn (tyco, _) => ((tyco, map snd vs), sort)) css;
-      in ClassPackage.assume_arities_of_sort thy arities (ty, sort) end;
-    fun mk_cons tyco (c, tys) =
-      let
-        val ts = Name.names Name.context "a" tys;
-        val ty = tys ---> Type (tyco, map TFree vs);
-      in list_comb (Const (c, ty), map Free ts) end;
-  in if forall (fn (_, cs) => forall (fn (_, tys) => forall typ_of_sort tys) cs) css
-    then SOME (
-      map (fn (tyco, cs) => (tyco, (mk_arity tyco, map (mk_cons tyco) cs))) css
-    ) else NONE
-  end;
-
-fun prove_arities tac tycos sort f thy =
-  case get_datatype_arities thy tycos sort
-   of NONE => thy
-    | SOME insts => let
-        fun proven ((tyco, asorts), sort) =
-          Sorts.of_sort (Sign.classes_of thy)
-            (Type (tyco, map TFree (Name.names Name.context "'a" asorts)), sort);
-        val (arities, css) = (split_list o map_filter
-          (fn (tyco, (arity, cs)) => if proven arity
-            then NONE else SOME (arity, (tyco, cs)))) insts;
-      in
-        thy
-        |> K ((not o null) arities) ? ClassPackage.prove_instance_arity tac
-             arities ("", []) (f thy arities css)
-      end;
+(** datatypes for code 2nd generation **)
 
 fun dtyp_of_case_const thy c =
   get_first (fn (dtco, { case_name, ... }) => if case_name = c then SOME dtco else NONE)
@@ -423,6 +348,57 @@
           | _ => NONE)
     | _ => NONE;
 
+fun mk_distinct cos =
+  let
+    fun sym_product [] = []
+      | sym_product (x::xs) = map (pair x) xs @ sym_product xs;
+    fun mk_co_args (co, tys) ctxt =
+      let
+        val names = Name.invents ctxt "a" (length tys);
+        val ctxt' = fold Name.declare names ctxt;
+        val vs = map2 (curry Free) names tys;
+      in (vs, ctxt) end;
+    fun mk_dist ((co1, tys1), (co2, tys2)) =
+      let
+        val ((xs1, xs2), _) = Name.context
+          |> mk_co_args (co1, tys1)
+          ||>> mk_co_args (co2, tys2);
+        val prem = HOLogic.mk_eq
+          (list_comb (co1, xs1), list_comb (co2, xs2));
+        val t = HOLogic.mk_not prem;
+      in HOLogic.mk_Trueprop t end;
+  in map mk_dist (sym_product cos) end;
+
+local
+  val not_false_true = iffD2 OF [nth (thms "HOL.simp_thms") 7, TrueI];
+in fun get_eq thy dtco =
+  let
+    val SOME (vs, cs) = DatatypePackage.get_datatype_spec thy dtco;
+    fun mk_triv_inject co =
+      let
+        val ct' = Thm.cterm_of thy
+          (Const (co, Type (dtco, map (fn (v, sort) => TVar ((v, 0), sort)) vs)))
+        val cty' = Thm.ctyp_of_term ct';
+        val refl = Thm.prop_of HOL.refl;
+        val SOME (ct, cty) = fold_aterms (fn Var (v, ty) =>
+          (K o SOME) (Thm.cterm_of thy (Var (v, Thm.typ_of cty')), Thm.ctyp_of thy ty) | _ => I)
+          refl NONE;
+      in eqTrueI OF [Thm.instantiate ([(cty, cty')], [(ct, ct')]) HOL.refl] end;
+    val inject1 = map_filter (fn (co, []) => SOME (mk_triv_inject co) | _ => NONE) cs
+    val inject2 = (#inject o DatatypePackage.the_datatype thy) dtco;
+    val ctxt = Context.init_proof thy;
+    val simpset = Simplifier.context ctxt
+      (MetaSimplifier.empty_ss addsimprocs [distinct_simproc]);
+    val cos = map (fn (co, tys) =>
+        (Const (co, tys ---> Type (dtco, map TFree vs)), tys)) cs;
+    val tac = ALLGOALS (simp_tac simpset)
+      THEN ALLGOALS (ProofContext.fact_tac [not_false_true, TrueI]);
+    val distinct =
+      mk_distinct cos
+      |> map (fn t => Goal.prove_global thy [] [] t (K tac))
+  in inject1 @ inject2 @ distinct end;
+end (*local*);
+
 fun datatype_tac thy dtco =
   let
     val ctxt = Context.init_proof thy;
@@ -458,6 +434,126 @@
     fold CodegenTheorems.add_fun case_rewrites thy
   end;
 
+
+(** codetypes for code 2nd generation **)
+
+type hook = (string * (bool * ((string * sort) list * (string * typ list) list))) list
+  -> theory -> theory;
+
+fun codetypes_dependency thy =
+  let
+    val names =
+      map (rpair true) (Symtab.keys (DatatypePackage.get_datatypes thy))
+        @ map (rpair false) (TypecopyPackage.get_typecopies thy);
+    fun add_node (name, is_dt) =
+      let
+        fun add_tycos (Type (tyco, tys)) = insert (op =) tyco #> fold add_tycos tys
+          | add_tycos _ = I;
+        val tys = if is_dt then
+            (maps snd o snd o the o DatatypePackage.get_datatype_spec thy) name
+          else
+            [(#typ o the o TypecopyPackage.get_typecopy_info thy) name]
+        val deps = (filter (AList.defined (op =) names) o maps (fn ty =>
+          add_tycos ty [])) tys;
+      in
+        Graph.default_node (name, ())
+        #> fold (fn name' =>
+             Graph.default_node (name', ())
+             #> Graph.add_edge (name', name)
+           ) deps
+      end
+  in
+    Graph.empty
+    |> fold add_node names
+    |> Graph.strong_conn
+    |> map (AList.make (the o AList.lookup (op =) names))
+  end;
+
+fun mk_typecopy_spec ({ vs, constr, typ, ... } : TypecopyPackage.info) =
+  (vs, [(constr, [typ])]);
+
+fun get_spec thy (dtco, true) =
+      (the o DatatypePackage.get_datatype_spec thy) dtco
+  | get_spec thy (tyco, false) =
+      (mk_typecopy_spec o the o TypecopyPackage.get_typecopy_info thy) tyco;
+
+fun add_spec thy (tyco, is_dt) =
+  (tyco, (is_dt, get_spec thy (tyco, is_dt)));
+
+fun add_codetypes_hook_bootstrap hook thy =
+  let
+    fun datatype_hook dtcos thy =
+      hook (map (add_spec thy) (map (rpair true) dtcos)) thy;
+    fun typecopy_hook ((tyco, info )) thy =
+      hook ([(tyco, (false, mk_typecopy_spec info))]) thy;
+  in
+    thy
+    |> fold hook ((map o map) (add_spec thy) (codetypes_dependency thy))
+    |> DatatypeHooks.add datatype_hook
+    |> TypecopyPackage.add_hook typecopy_hook
+  end;
+
+fun the_codetypes_mut_specs thy ([(tyco, is_dt)]) =
+      let
+        val (vs, cs) = get_spec thy (tyco, is_dt)
+      in (vs, [(tyco, (is_dt, cs))]) end
+  | the_codetypes_mut_specs thy (tycos' as (tyco, true) :: _) =
+      let
+        val tycos = map fst tycos';
+        val tycos'' = (map (#1 o snd) o #descr o DatatypePackage.the_datatype thy) tyco;
+        val _ = if gen_subset (op =) (tycos, tycos'') then () else
+          error ("datatype constructors are not mutually recursive: " ^ (commas o map quote) tycos);
+        val (vs::_, css) = split_list (map (the o DatatypePackage.get_datatype_spec thy) tycos);
+      in (vs, map2 (fn (tyco, is_dt) => fn cs => (tyco, (is_dt, cs))) tycos' css) end;
+
+fun get_codetypes_arities thy tycos sort =
+  let
+    val algebra = Sign.classes_of thy;
+    val (vs_proto, css_proto) = the_codetypes_mut_specs thy tycos;
+    val vs = map (fn (v, vsort) => (v, Sorts.inter_sort algebra (vsort, sort))) vs_proto;
+    fun inst_type tyco (c, tys) =
+      let
+        val tys' = (map o map_atyps)
+          (fn TFree (v, _) => TFree (v, the (AList.lookup (op =) vs v))) tys
+      in (c, tys') end;
+    val css = map (fn (tyco, (_, cs)) => (tyco, (map (inst_type tyco) cs))) css_proto;
+    fun mk_arity tyco =
+      ((tyco, map snd vs), sort);
+    fun typ_of_sort ty =
+      let
+        val arities = map (fn (tyco, _) => ((tyco, map snd vs), sort)) css;
+      in ClassPackage.assume_arities_of_sort thy arities (ty, sort) end;
+    fun mk_cons tyco (c, tys) =
+      let
+        val ts = Name.names Name.context "a" tys;
+        val ty = tys ---> Type (tyco, map TFree vs);
+      in list_comb (Const (c, ty), map Free ts) end;
+  in if forall (fn (_, cs) => forall (fn (_, tys) => forall typ_of_sort tys) cs) css
+    then SOME (
+      map (fn (tyco, cs) => (tyco, (mk_arity tyco, map (mk_cons tyco) cs))) css
+    ) else NONE
+  end;
+
+fun prove_codetypes_arities tac tycos sort f thy =
+  case get_codetypes_arities thy tycos sort
+   of NONE => thy
+    | SOME insts => let
+        fun proven ((tyco, asorts), sort) =
+          Sorts.of_sort (Sign.classes_of thy)
+            (Type (tyco, map TFree (Name.names Name.context "'a" asorts)), sort);
+        val (arities, css) = (split_list o map_filter
+          (fn (tyco, (arity, cs)) => if proven arity
+            then NONE else SOME (arity, (tyco, cs)))) insts;
+      in
+        thy
+        |> K ((not o null) arities) ? ClassPackage.prove_instance_arity tac
+             arities ("", []) (f thy arities css)
+      end;
+
+
+
+(** theory setup **)
+
 val setup = 
   add_codegen "datatype" datatype_codegen #>
   add_tycodegen "datatype" datatype_tycodegen #>
diff -r dc1e8c24a475 -r 9ffea7a8b31c src/HOL/Tools/typecopy_package.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/typecopy_package.ML	Tue Aug 29 14:31:13 2006 +0200
@@ -0,0 +1,163 @@
+(*  Title:      HOL/Tools/typecopy_package.ML
+    ID:         $Id$
+    Author:     Florian Haftmann, TU Muenchen
+
+Introducing copies of types using trivial typedefs.
+*)
+
+signature TYPECOPY_PACKAGE =
+sig
+  type info = {
+    vs: (string * sort) list,
+    constr: string,
+    typ: typ,
+    inject: thm,
+    proj: string * typ,
+    proj_def: thm
+  }
+  val add_typecopy: bstring * string list -> typ -> (bstring * bstring) option
+    -> theory -> info * theory
+  val get_typecopies: theory -> string list
+  val get_typecopy_info: theory -> string -> info option
+  type hook = string * info -> theory -> theory;
+  val add_hook: hook -> theory -> theory;
+  val typecopy_fun_extr: theory -> string * typ -> thm list option
+  val typecopy_type_extr: theory -> string
+    -> (((string * sort) list * (string * typ list) list) * tactic) option
+  val print: theory -> unit
+  val setup: theory -> theory
+end;
+
+structure TypecopyPackage: TYPECOPY_PACKAGE =
+struct
+
+(* theory context reference *)
+
+val univ_witness = thm "Set.UNIV_witness"
+
+
+(* theory data *)
+
+type info = {
+  vs: (string * sort) list,
+  constr: string,
+  typ: typ,
+  inject: thm,
+  proj: string * typ,
+  proj_def: thm
+};
+
+type hook = string * info -> theory -> theory;
+
+structure TypecopyData = TheoryDataFun
+(struct
+  val name = "HOL/typecopy_package";
+  type T = info Symtab.table * (serial * hook) list;
+  val empty = (Symtab.empty, []);
+  val copy = I;
+  val extend = I;
+  fun merge _ ((tab1, hooks1), (tab2, hooks2) : T) =
+    (Symtab.merge (K true) (tab1, tab2), AList.merge (op =) (K true) (hooks1, hooks2));
+  fun print thy (tab, _) =
+    let
+      fun mk (tyco, { vs, constr, typ, proj = (proj, _), ... } : info) =
+        (Pretty.block o Pretty.breaks) [
+          Sign.pretty_typ thy (Type (tyco, map TFree vs)),
+          Pretty.str "=",
+          (Pretty.str o Sign.extern_const thy) constr,
+          Sign.pretty_typ thy typ,
+          Pretty.block [Pretty.str "(", (Pretty.str o Sign.extern_const thy) proj, Pretty.str  ")"]
+        ];
+    in
+      (Pretty.writeln o Pretty.block o Pretty.fbreaks) (
+        Pretty.str "type copies:"
+        :: map mk (Symtab.dest tab)
+      )
+    end;
+end);
+
+val print = TypecopyData.print;
+val get_typecopies = Symtab.keys o fst o TypecopyData.get;
+val get_typecopy_info = Symtab.lookup o fst o TypecopyData.get;
+
+
+(* hook management *)
+
+fun add_hook hook =
+  (TypecopyData.map o apsnd o cons) (serial (), hook);
+
+fun invoke_hooks tyco_info thy =
+  fold (fn (_, f) => f tyco_info) ((snd o TypecopyData.get) thy) thy;
+
+
+(* add a type copy *)
+
+local
+
+fun gen_add_typecopy prep_typ (tyco, raw_vs) raw_ty constr_proj thy =
+  let
+    val ty = prep_typ thy raw_ty;
+    val vs = AList.make (the_default HOLogic.typeS o AList.lookup (op =) (typ_tfrees ty)) raw_vs;
+    val tac = Tactic.rtac UNIV_witness 1;
+    fun add_info ( { abs_type = ty_abs, rep_type = ty_rep, Abs_name = c_abs,
+      Rep_name = c_rep, Abs_inject = inject,
+      Abs_inverse = inverse, ... } : TypedefPackage.info ) thy = 
+        let
+          val Type (tyco', _) = ty_abs;
+          val exists_thm =
+            UNIV_I
+            |> Drule.instantiate' [SOME (ctyp_of thy (Logic.varifyT ty_rep))] [];
+          val inject' = inject OF [exists_thm, exists_thm];
+          val proj_def = inverse OF [exists_thm];
+          val info = {
+            vs = vs,
+            constr = c_abs,
+            typ = ty_rep,
+            inject = inject',
+            proj = (c_rep, ty_abs --> ty_rep),
+            proj_def = proj_def
+          };
+        in
+          thy
+          |> (TypecopyData.map o apfst o Symtab.update_new) (tyco', info)
+          |> invoke_hooks (tyco', info)
+          |> pair info
+        end
+  in
+    thy
+    |> TypedefPackage.add_typedef_i false (SOME tyco) (tyco, map fst vs, NoSyn)
+          (HOLogic.mk_UNIV ty) (Option.map swap constr_proj) tac
+    |-> (fn info => add_info info)
+  end;
+
+in
+
+val add_typecopy = gen_add_typecopy Sign.certify_typ;
+
+end; (*local*)
+
+
+(* theory setup *)
+
+fun typecopy_type_extr thy tyco =
+  case get_typecopy_info thy tyco
+   of SOME { vs, constr, typ, inject, ... } => SOME ((vs, [(constr, [typ])]),
+       (ALLGOALS o match_tac) [eq_reflection]
+          THEN (ALLGOALS o match_tac) [inject])
+    | NONE => NONE;
+
+fun typecopy_fun_extr thy (c, ty) =
+  case (fst o strip_type) ty
+   of Type (tyco, _) :: _ =>
+        (case get_typecopy_info thy tyco
+          of SOME { proj_def, proj as (c', _), ... } =>
+              if c = c' then SOME [proj_def] else NONE
+           | NONE => NONE)
+    | _ => NONE;
+
+val setup =
+  TypecopyData.init
+  #> CodegenTheorems.add_fun_extr (these oo typecopy_fun_extr)
+  #> CodegenTheorems.add_datatype_extr typecopy_type_extr;
+
+end; (*struct*)
diff -r dc1e8c24a475 -r 9ffea7a8b31c src/HOL/Typedef.thy
--- a/src/HOL/Typedef.thy	Tue Aug 29 14:31:12 2006 +0200
+++ b/src/HOL/Typedef.thy	Tue Aug 29 14:31:13 2006 +0200
@@ -7,7 +7,10 @@
 
 theory Typedef
 imports Set
-uses ("Tools/typedef_package.ML") ("Tools/typedef_codegen.ML")
+uses
+  ("Tools/typedef_package.ML")
+  ("Tools/typecopy_package.ML")
+  ("Tools/typedef_codegen.ML")
 begin
 
 locale type_definition =
@@ -83,8 +86,13 @@
 qed
 
 use "Tools/typedef_package.ML"
+use "Tools/typecopy_package.ML"
 use "Tools/typedef_codegen.ML"
 
-setup {* TypedefPackage.setup #> TypedefCodegen.setup *}
+setup {*
+  TypedefPackage.setup
+  #> TypecopyPackage.setup
+  #> TypedefCodegen.setup
+*}
 
 end