open typedefs everywhere in the package

--- a/src/HOL/Codatatype/Tools/bnf_comp.ML	Sun Sep 09 10:15:58 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_comp.ML	Sun Sep 09 10:58:11 2012 +0200
@@ -658,23 +658,15 @@
     val params = fold Term.add_tfreesT Ds [];
     val deads = map TFree params;
 
-    val ((bdT_name, (bdT_glob_info, bdT_loc_info)), (lthy', lthy)) =
-      lthy
-      |> Typedef.add_typedef true NONE (bdT_bind, params, NoSyn)
-        (HOLogic.mk_UNIV bd_repT) NONE (EVERY' [rtac exI, rtac UNIV_I] 1)
-      ||> `Local_Theory.restore;
-
-    val phi = Proof_Context.export_morphism lthy lthy';
+    val ((bdT_name, (bdT_glob_info, bdT_loc_info)), lthy) =
+      typedef false NONE (bdT_bind, params, NoSyn)
+        (HOLogic.mk_UNIV bd_repT) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy;
 
     val bnf_bd' = mk_dir_image bnf_bd
       (Const (#Abs_name bdT_glob_info, bd_repT --> Type (bdT_name, deads)))
 
-    val set_def = Morphism.thm phi (the (#set_def bdT_loc_info));
-    val Abs_inject = Morphism.thm phi (#Abs_inject bdT_loc_info);
-    val Abs_cases = Morphism.thm phi (#Abs_cases bdT_loc_info);
-
-    val Abs_bdT_inj = mk_Abs_inj_thm set_def Abs_inject;
-    val Abs_bdT_bij = mk_Abs_bij_thm lthy' set_def Abs_inject Abs_cases;
+    val Abs_bdT_inj = mk_Abs_inj_thm (#Abs_inject bdT_loc_info);
+    val Abs_bdT_bij = mk_Abs_bij_thm lthy Abs_bdT_inj (#Abs_cases bdT_loc_info);
 
     val bd_ordIso = @{thm dir_image} OF [Abs_bdT_inj, bd_Card_order_of_bnf bnf];
     val bd_card_order =

--- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Sun Sep 09 10:15:58 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Sun Sep 09 10:58:11 2012 +0200
@@ -77,9 +77,6 @@
   val mk_set_minimalN: int -> string
   val mk_set_inductN: int -> string
 
-  val typedef: bool -> binding option -> binding * (string * sort) list * mixfix -> term ->
-    (binding * binding) option -> tactic -> local_theory -> (string * Typedef.info) * local_theory
-
   val split_conj_thm: thm -> thm list
   val split_conj_prems: int -> thm -> thm
 
@@ -126,18 +123,6 @@
   then warning (msg ^ ": " ^ ATP_Util.string_from_time (Timer.checkRealTimer timer))
   else (); Timer.startRealTimer ());
 
-(*TODO: is this really different from Typedef.add_typedef_global?*)
-fun typedef def opt_name typ set opt_morphs tac lthy =
-  let
-    val ((name, info), (lthy, lthy_old)) =
-      lthy
-      |> Typedef.add_typedef def opt_name typ set opt_morphs tac
-      ||> `Local_Theory.restore;
-    val phi = Proof_Context.export_morphism lthy_old lthy;
-  in
-    ((name, Typedef.transform_info phi info), lthy)
-  end;
-
 val preN = "pre_"
 val rawN = "raw_"
 

--- a/src/HOL/Codatatype/Tools/bnf_gfp.ML	Sun Sep 09 10:15:58 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML	Sun Sep 09 10:58:11 2012 +0200
@@ -1028,7 +1028,7 @@
           val sbdT_bind = Binding.suffix_name ("_" ^ sum_bdTN) b;
 
           val ((sbdT_name, (sbdT_glob_info, sbdT_loc_info)), lthy) =
-            typedef true NONE (sbdT_bind, params, NoSyn)
+            typedef false NONE (sbdT_bind, params, NoSyn)
               (HOLogic.mk_UNIV sum_bdT) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy;
 
           val sbdT = Type (sbdT_name, params');
@@ -1052,12 +1052,8 @@
           val sbd_def = Morphism.thm phi sbd_def_free;
           val sbd = Const (fst (Term.dest_Const (Morphism.term phi sbd_free)), mk_relT (`I sbdT));
 
-          val sbdT_set_def = the (#set_def sbdT_loc_info);
-          val sbdT_Abs_inject = #Abs_inject sbdT_loc_info;
-          val sbdT_Abs_cases = #Abs_cases sbdT_loc_info;
-
-          val Abs_sbdT_inj = mk_Abs_inj_thm sbdT_set_def sbdT_Abs_inject;
-          val Abs_sbdT_bij = mk_Abs_bij_thm lthy sbdT_set_def sbdT_Abs_inject sbdT_Abs_cases;
+          val Abs_sbdT_inj = mk_Abs_inj_thm (#Abs_inject sbdT_loc_info);
+          val Abs_sbdT_bij = mk_Abs_bij_thm lthy Abs_sbdT_inj (#Abs_cases sbdT_loc_info);
 
           fun mk_sum_Cinfinite [thm] = thm
             | mk_sum_Cinfinite (thm :: thms) =

--- a/src/HOL/Codatatype/Tools/bnf_lfp.ML	Sun Sep 09 10:15:58 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML	Sun Sep 09 10:58:11 2012 +0200
@@ -774,14 +774,13 @@
     val IIT_bind = Binding.suffix_name ("_" ^ IITN) b;
 
     val ((IIT_name, (IIT_glob_info, IIT_loc_info)), lthy) =
-      typedef true NONE (IIT_bind, params, NoSyn)
+      typedef false NONE (IIT_bind, params, NoSyn)
         (HOLogic.mk_UNIV II_repT) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy;
 
     val IIT = Type (IIT_name, params');
     val Abs_IIT = Const (#Abs_name IIT_glob_info, II_repT --> IIT);
     val Rep_IIT = Const (#Rep_name IIT_glob_info, IIT --> II_repT);
-    val Abs_IIT_inverse_thm =
-      mk_Abs_inverse_thm (the (#set_def IIT_loc_info)) (#Abs_inverse IIT_loc_info);
+    val Abs_IIT_inverse_thm = UNIV_I RS #Abs_inverse IIT_loc_info;
 
     val initT = IIT --> Asuc_bdT;
     val active_initTs = replicate n initT;

--- a/src/HOL/Codatatype/Tools/bnf_tactics.ML	Sun Sep 09 10:15:58 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_tactics.ML	Sun Sep 09 10:58:11 2012 +0200
@@ -20,12 +20,8 @@
   val mk_rotate_eq_tac: (int -> tactic) -> thm -> thm -> thm -> thm -> ''a list -> ''a list ->
     int -> tactic
 
-  val mk_Abs_bij_thm: Proof.context -> thm -> thm -> thm -> thm
-  val mk_Abs_inj_thm: thm -> thm -> thm
-  val mk_Abs_inverse_thm: thm -> thm -> thm
-  val mk_T_I: thm -> thm
-  val mk_T_subset1: thm -> thm
-  val mk_T_subset2: thm -> thm
+  val mk_Abs_bij_thm: Proof.context -> thm -> thm -> thm
+  val mk_Abs_inj_thm: thm -> thm
 
   val mk_Card_order_tac: thm -> tactic
   val mk_collect_set_natural_tac: Proof.context -> thm list -> tactic
@@ -81,17 +77,11 @@
 
 
 
-(* Theorems for typedefs with UNIV as representing set *)
+(* Theorems for open typedefs with UNIV as representing set *)
 
-(*equivalent to UNIV_I for the representing set of the particular type T*)
-fun mk_T_subset1 def = set_mp OF [def RS meta_eq_to_obj_eq RS equalityD2];
-fun mk_T_subset2 def = set_mp OF [def RS meta_eq_to_obj_eq RS equalityD1];
-fun mk_T_I def = UNIV_I RS mk_T_subset1 def;
-
-fun mk_Abs_inverse_thm def inv = mk_T_I def RS inv;
-fun mk_Abs_inj_thm def inj = inj OF (replicate 2 (mk_T_I def));
-fun mk_Abs_bij_thm ctxt def inj surj = rule_by_tactic ctxt ((rtac surj THEN' etac exI) 1)
-  (mk_Abs_inj_thm def inj RS @{thm bijI});
+fun mk_Abs_inj_thm inj = inj OF (replicate 2 UNIV_I);
+fun mk_Abs_bij_thm ctxt Abs_inj_thm surj = rule_by_tactic ctxt ((rtac surj THEN' etac exI) 1)
+  (Abs_inj_thm RS @{thm bijI});
 
 
 

--- a/src/HOL/Codatatype/Tools/bnf_util.ML	Sun Sep 09 10:15:58 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_util.ML	Sun Sep 09 10:58:11 2012 +0200
@@ -124,6 +124,9 @@
   val certifyT: Proof.context -> typ -> ctyp
   val certify: Proof.context -> term -> cterm
 
+  val typedef: bool -> binding option -> binding * (string * sort) list * mixfix -> term ->
+    (binding * binding) option -> tactic -> local_theory -> (string * Typedef.info) * local_theory
+
   val WRAP: ('a -> tactic) -> ('a -> tactic) -> 'a list -> tactic -> tactic
   val WRAP': ('a -> int -> tactic) -> ('a -> int -> tactic) -> 'a list -> (int -> tactic) -> int ->
     tactic
@@ -243,6 +246,18 @@
 fun certify ctxt = Thm.cterm_of (Proof_Context.theory_of ctxt);
 fun certifyT ctxt = Thm.ctyp_of (Proof_Context.theory_of ctxt);
 
+(*TODO: is this really different from Typedef.add_typedef_global?*)
+fun typedef def opt_name typ set opt_morphs tac lthy =
+  let
+    val ((name, info), (lthy, lthy_old)) =
+      lthy
+      |> Typedef.add_typedef def opt_name typ set opt_morphs tac
+      ||> `Local_Theory.restore;
+    val phi = Proof_Context.export_morphism lthy_old lthy;
+  in
+    ((name, Typedef.transform_info phi info), lthy)
+  end;
+
 (*Tactical WRAP surrounds a static given tactic (core) with two deterministic chains of tactics*)
 fun WRAP gen_before gen_after xs core_tac =
   fold_rev (fn x => fn tac => gen_before x THEN tac THEN gen_after x) xs core_tac;