open typedef for datatypes

--- a/src/HOL/Codatatype/Tools/bnf_lfp.ML	Sat Sep 08 22:54:37 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML	Sun Sep 09 10:15:58 2012 +0200
@@ -936,7 +936,7 @@
 
     val ((T_names, (T_glob_infos, T_loc_infos)), lthy) =
       lthy
-      |> fold_map3 (fn b => fn mx => fn car_init => typedef true NONE (b, params, mx) car_init NONE
+      |> fold_map3 (fn b => fn mx => fn car_init => typedef false NONE (b, params, mx) car_init NONE
           (EVERY' [rtac ssubst, rtac @{thm ex_in_conv}, resolve_tac alg_not_empty_thms,
             rtac alg_init_thm] 1)) bs mixfixes car_inits
       |>> apsnd split_list o split_list;
@@ -947,7 +947,6 @@
     val Rep_Ts = map2 (fn info => fn T => Const (#Rep_name info, T --> initT)) T_glob_infos Ts;
     val Abs_Ts = map2 (fn info => fn T => Const (#Abs_name info, initT --> T)) T_glob_infos Ts;
 
-    val set_defs = map (the o #set_def) T_loc_infos;
     val type_defs = map #type_definition T_loc_infos;
     val Reps = map #Rep T_loc_infos;
     val Rep_casess = map #Rep_cases T_loc_infos;
@@ -955,9 +954,6 @@
     val Rep_inverses = map #Rep_inverse T_loc_infos;
     val Abs_inverses = map #Abs_inverse T_loc_infos;
 
-    val T_subset1s = map mk_T_subset1 set_defs;
-    val T_subset2s = map mk_T_subset2 set_defs;
-
     fun mk_inver_thm mk_tac rep abs X thm =
       Skip_Proof.prove lthy [] []
         (HOLogic.mk_Trueprop (mk_inver rep abs X))
@@ -965,8 +961,7 @@
       |> Thm.close_derivation;
 
     val inver_Reps = map4 (mk_inver_thm rtac) Abs_Ts Rep_Ts (map HOLogic.mk_UNIV Ts) Rep_inverses;
-    val inver_Abss = map4 (mk_inver_thm etac) Rep_Ts Abs_Ts car_inits
-      (map2 (curry op RS) T_subset1s Abs_inverses);
+    val inver_Abss = map4 (mk_inver_thm etac) Rep_Ts Abs_Ts car_inits Abs_inverses;
 
     val timer = time (timer "THE TYPEDEFs & Rep/Abs thms");
 
@@ -1036,9 +1031,8 @@
     val (mor_Rep_thm, mor_Abs_thm) =
       let
         val copy = alg_init_thm RS copy_alg_thm;
-        fun mk_bij inj subset1 subset2 Rep cases = @{thm bij_betwI'} OF
-          [inj, Rep RS subset2, subset1 RS cases];
-        val bijs = map5 mk_bij Rep_injects T_subset1s T_subset2s Reps Rep_casess;
+        fun mk_bij inj Rep cases = @{thm bij_betwI'} OF [inj, Rep, cases];
+        val bijs = map3 mk_bij Rep_injects Reps Rep_casess;
         val mor_Rep =
           Skip_Proof.prove lthy [] []
             (HOLogic.mk_Trueprop (mk_mor UNIVs flds car_inits str_inits Rep_Ts))
@@ -1118,7 +1112,7 @@
         val unique = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_fun_eq fs ks));
         val unique_mor = Skip_Proof.prove lthy [] []
           (fold_rev Logic.all (ss @ fs) (Logic.mk_implies (prem, unique)))
-          (K (mk_iter_unique_mor_tac type_defs init_unique_mor_thms T_subset2s Reps
+          (K (mk_iter_unique_mor_tac type_defs init_unique_mor_thms Reps
             mor_comp_thm mor_Abs_thm mor_iter_thm))
           |> Thm.close_derivation;
       in
@@ -1303,7 +1297,7 @@
         (Skip_Proof.prove lthy [] []
           (fold_rev Logic.all (phis @ Izs) goal)
           (K (mk_fld_induct_tac m set_natural'ss init_induct_thm morE_thms mor_Abs_thm
-            Rep_inverses Abs_inverses Reps T_subset1s T_subset2s))
+            Rep_inverses Abs_inverses Reps))
         |> Thm.close_derivation,
         rev (Term.add_tfrees goal []))
       end;

--- a/src/HOL/Codatatype/Tools/bnf_lfp_tactics.ML	Sat Sep 08 22:54:37 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_lfp_tactics.ML	Sun Sep 09 10:15:58 2012 +0200
@@ -22,7 +22,7 @@
   val mk_fld_induct2_tac: ctyp option list -> cterm option list -> thm -> thm list ->
     {prems: 'a, context: Proof.context} -> tactic
   val mk_fld_induct_tac: int -> thm list list -> thm -> thm list -> thm -> thm list -> thm list ->
-    thm list -> thm list -> thm list -> tactic
+    thm list -> tactic
   val mk_in_bd_tac: thm -> thm -> thm -> thm -> tactic
   val mk_incl_min_alg_tac: (int -> tactic) -> thm list list list -> thm list -> thm ->
     {prems: 'a, context: Proof.context} -> tactic
@@ -32,8 +32,7 @@
   val mk_init_unique_mor_tac: int -> thm -> thm -> thm list -> thm list -> thm list -> thm list ->
     thm list -> tactic
   val mk_iso_alt_tac: thm list -> thm -> tactic
-  val mk_iter_unique_mor_tac: thm list -> thm list -> thm list -> thm list -> thm -> thm -> thm ->
-    tactic
+  val mk_iter_unique_mor_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> tactic
   val mk_least_min_alg_tac: thm -> thm -> tactic
   val mk_lfp_map_wpull_tac: int -> (int -> tactic) -> thm list -> thm list -> thm list list ->
     thm list list list -> thm list -> tactic
@@ -497,12 +496,12 @@
   REPEAT_DETERM_N (length iter_defs) o etac exE THEN'
   rtac (Drule.instantiate' [SOME cT] [SOME ct] @{thm someI}) THEN' etac mor) 1;
 
-fun mk_iter_unique_mor_tac type_defs init_unique_mors subsets Reps mor_comp mor_Abs mor_iter =
+fun mk_iter_unique_mor_tac type_defs init_unique_mors Reps mor_comp mor_Abs mor_iter =
   let
-    fun mk_subset subset Rep = etac subset ORELSE' rtac (Rep RS subset);
     fun mk_unique type_def =
       EVERY' [rtac @{thm surj_fun_eq}, rtac (type_def RS @{thm type_definition.Abs_image}),
-        rtac ballI, resolve_tac init_unique_mors, EVERY' (map2 mk_subset subsets Reps),
+        rtac ballI, resolve_tac init_unique_mors,
+        EVERY' (map (fn thm => atac ORELSE' rtac thm) Reps),
         rtac mor_comp, rtac mor_Abs, atac,
         rtac mor_comp, rtac mor_Abs, rtac mor_iter];
   in
@@ -522,33 +521,30 @@
   EVERY' [rtac trans, rtac o_apply, rtac trans, rtac (iter RS @{thm arg_cong[of _ _ snd]}),
     rtac @{thm snd_convol'}] 1;
 
-fun mk_fld_induct_tac m set_natural'ss init_induct morEs mor_Abs Rep_invs Abs_invs Reps
-    subset1s subset2s =
+fun mk_fld_induct_tac m set_natural'ss init_induct morEs mor_Abs Rep_invs Abs_invs Reps =
   let
     val n = length set_natural'ss;
     val ks = 1 upto n;
 
-    fun mk_IH_tac Rep_inv Abs_inv set_natural' subset =
+    fun mk_IH_tac Rep_inv Abs_inv set_natural' =
       DETERM o EVERY' [dtac @{thm meta_mp}, rtac (Rep_inv RS arg_cong RS subst), etac bspec,
         dtac @{thm set_rev_mp}, rtac equalityD1, rtac set_natural', etac imageE,
-        hyp_subst_tac, rtac (Abs_inv RS ssubst), rtac subset, etac @{thm set_mp},
+        hyp_subst_tac, rtac (Abs_inv RS ssubst), etac @{thm set_mp},
         atac, atac];
 
     fun mk_closed_tac (k, (morE, set_natural's)) =
       EVERY' [select_prem_tac n (dtac asm_rl) k, rtac ballI, rtac impI,
         rtac (mor_Abs RS morE RS arg_cong RS ssubst), atac,
         REPEAT_DETERM o eresolve_tac [CollectE, conjE], dtac @{thm meta_spec},
-        EVERY' (map4 mk_IH_tac Rep_invs Abs_invs (drop m set_natural's) subset1s), atac];
+        EVERY' (map3 mk_IH_tac Rep_invs Abs_invs (drop m set_natural's)), atac];
 
-    fun mk_induct_tac ((Rep, Rep_inv), subset) =
-      EVERY' [rtac (Rep_inv RS arg_cong RS subst), etac (Rep RS subset RSN (2, bspec))];
+    fun mk_induct_tac (Rep, Rep_inv) =
+      EVERY' [rtac (Rep_inv RS arg_cong RS subst), etac (Rep RSN (2, bspec))];
   in
     (rtac mp THEN' rtac impI THEN'
-    DETERM o CONJ_WRAP_GEN' (etac conjE THEN' rtac conjI) mk_induct_tac
-      ((Reps ~~ Rep_invs) ~~ subset2s) THEN'
+    DETERM o CONJ_WRAP_GEN' (etac conjE THEN' rtac conjI) mk_induct_tac (Reps ~~ Rep_invs) THEN'
     rtac init_induct THEN'
-    DETERM o CONJ_WRAP' mk_closed_tac
-      (ks ~~ (morEs ~~ set_natural'ss))) 1
+    DETERM o CONJ_WRAP' mk_closed_tac (ks ~~ (morEs ~~ set_natural'ss))) 1
   end;
 
 fun mk_fld_induct2_tac cTs cts fld_induct weak_fld_inducts {context = ctxt, prems = _} =