# HG changeset patch
# User traytel
# Date 1395386003 -3600
# Node ID 69a9dfe71aed821d1c67debe08ef6d6e31fb71ab
# Parent  713ae0c9e652c042d3b6eac5b5f8d07e213bff8c
simplified internal datatype construction

diff -r 713ae0c9e652 -r 69a9dfe71aed src/HOL/BNF_LFP.thy
--- a/src/HOL/BNF_LFP.thy	Thu Mar 20 23:38:34 2014 +0100
+++ b/src/HOL/BNF_LFP.thy	Fri Mar 21 08:13:23 2014 +0100
@@ -60,88 +60,19 @@
   moreover have "\<dots> \<longleftrightarrow> <g, h> = f" by (subst (2) *[symmetric]) (auto simp: convol_def fun_eq_iff)
   ultimately show ?thesis by simp
 qed
-
-definition inver where
-  "inver g f A = (ALL a : A. g (f a) = a)"
-
-lemma bij_betw_iff_ex:
-  "bij_betw f A B = (EX g. g ` B = A \<and> inver g f A \<and> inver f g B)" (is "?L = ?R")
-proof (rule iffI)
-  assume ?L
-  hence f: "f ` A = B" and inj_f: "inj_on f A" unfolding bij_betw_def by auto
-  let ?phi = "% b a. a : A \<and> f a = b"
-  have "ALL b : B. EX a. ?phi b a" using f by blast
-  then obtain g where g: "ALL b : B. g b : A \<and> f (g b) = b"
-    using bchoice[of B ?phi] by blast
-  hence gg: "ALL b : f ` A. g b : A \<and> f (g b) = b" using f by blast
-  have gf: "inver g f A" unfolding inver_def
-  proof
-    fix a assume "a \<in> A"
-    then show "g (f a) = a" using the_inv_into_f_f[OF inj_f, of "g (f a)"]
-      the_inv_into_f_f[OF inj_f, of a] gg imageI[of a A f] by auto
-  qed
-  moreover have "g ` B \<le> A \<and> inver f g B" using g unfolding inver_def by blast
-  moreover have "A \<le> g ` B"
-  proof safe
-    fix a assume a: "a : A"
-    hence "f a : B" using f by auto
-    moreover have "a = g (f a)" using a gf unfolding inver_def by auto
-    ultimately show "a : g ` B" by blast
-  qed
-  ultimately show ?R by blast
-next
-  assume ?R
-  then obtain g where g: "g ` B = A \<and> inver g f A \<and> inver f g B" by blast
-  show ?L unfolding bij_betw_def
-  proof safe
-    show "inj_on f A" unfolding inj_on_def
-    proof safe
-      fix a1 a2 assume a: "a1 : A"  "a2 : A" and "f a1 = f a2"
-      hence "g (f a1) = g (f a2)" by simp
-      thus "a1 = a2" using a g unfolding inver_def by simp
-    qed
-  next
-    fix a assume "a : A"
-    then obtain b where b: "b : B" and a: "a = g b" using g by blast
-    hence "b = f (g b)" using g unfolding inver_def by auto
-    thus "f a : B" unfolding a using b by simp
-  next
-    fix b assume "b : B"
-    hence "g b : A \<and> b = f (g b)" using g unfolding inver_def by auto
-    thus "b : f ` A" by auto
-  qed
-qed
-
-lemma bij_betw_ex_weakE:
-  "\<lbrakk>bij_betw f A B\<rbrakk> \<Longrightarrow> \<exists>g. g ` B \<subseteq> A \<and> inver g f A \<and> inver f g B"
-by (auto simp only: bij_betw_iff_ex)
-
-lemma inver_surj: "\<lbrakk>g ` B \<subseteq> A; f ` A \<subseteq> B; inver g f A\<rbrakk> \<Longrightarrow> g ` B = A"
-unfolding inver_def by auto (rule rev_image_eqI, auto)
-
-lemma inver_mono: "\<lbrakk>A \<subseteq> B; inver f g B\<rbrakk> \<Longrightarrow> inver f g A"
-unfolding inver_def by auto
-
-lemma inver_pointfree: "inver f g A = (\<forall>a \<in> A. (f o g) a = a)"
-unfolding inver_def by simp
-
 lemma bij_betwE: "bij_betw f A B \<Longrightarrow> \<forall>a\<in>A. f a \<in> B"
 unfolding bij_betw_def by auto
 
 lemma bij_betw_imageE: "bij_betw f A B \<Longrightarrow> f ` A = B"
 unfolding bij_betw_def by auto
 
-lemma inverE: "\<lbrakk>inver f f' A; x \<in> A\<rbrakk> \<Longrightarrow> f (f' x) = x"
-unfolding inver_def by auto
-
-lemma bij_betw_inver1: "bij_betw f A B \<Longrightarrow> inver (inv_into A f) f A"
-unfolding bij_betw_def inver_def by auto
+lemma f_the_inv_into_f_bij_betw: "bij_betw f A B \<Longrightarrow>
+  (bij_betw f A B \<Longrightarrow> x \<in> B) \<Longrightarrow> f (the_inv_into A f x) = x"
+  unfolding bij_betw_def by (blast intro: f_the_inv_into_f)
 
-lemma bij_betw_inver2: "bij_betw f A B \<Longrightarrow> inver f (inv_into A f) B"
-unfolding bij_betw_def inver_def by auto
-
-lemma bij_betwI: "\<lbrakk>bij_betw g B A; inver g f A; inver f g B\<rbrakk> \<Longrightarrow> bij_betw f A B"
-by (drule bij_betw_imageE, unfold bij_betw_iff_ex) blast
+lemma ex_bij_betw: "|A| \<le>o (r :: 'b rel) \<Longrightarrow> \<exists>f B :: 'b set. bij_betw f B A"
+  by (subst (asm) internalize_card_of_ordLeq)
+    (auto dest!: iffD2[OF card_of_ordIso ordIso_symmetric])
 
 lemma bij_betwI':
   "\<lbrakk>\<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> (f x = f y) = (x = y);
diff -r 713ae0c9e652 -r 69a9dfe71aed src/HOL/Main.thy
--- a/src/HOL/Main.thy	Thu Mar 20 23:38:34 2014 +0100
+++ b/src/HOL/Main.thy	Fri Mar 21 08:13:23 2014 +0100
@@ -31,7 +31,7 @@
 hide_const (open)
   czero cinfinite cfinite csum cone ctwo Csum cprod cexp
   image2 image2p vimage2p Gr Grp collect fsts snds setl setr
-  convol pick_middlep fstOp sndOp csquare inver relImage relInvImage
+  convol pick_middlep fstOp sndOp csquare relImage relInvImage
   Succ Shift shift proj
 
 no_syntax (xsymbols)
diff -r 713ae0c9e652 -r 69a9dfe71aed src/HOL/Tools/BNF/bnf_lfp.ML
--- a/src/HOL/Tools/BNF/bnf_lfp.ML	Thu Mar 20 23:38:34 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Fri Mar 21 08:13:23 2014 +0100
@@ -104,7 +104,6 @@
     (* terms *)
     val mapsAsAs = map4 mk_map_of_bnf Dss Ass Ass bnfs;
     val mapsAsBs = map4 mk_map_of_bnf Dss Ass Bss bnfs;
-    val mapsBsAs = map4 mk_map_of_bnf Dss Bss Ass bnfs;
     val mapsBsCs' = map4 mk_map_of_bnf Dss Bss Css' bnfs;
     val mapsAsCs' = map4 mk_map_of_bnf Dss Ass Css' bnfs;
     val map_fsts = map4 mk_map_of_bnf Dss (replicate n (passiveAs @ prodBsAs)) Bss bnfs;
@@ -288,18 +287,6 @@
         goals
       end;
 
-    fun mk_talg BTs = mk_alg (map HOLogic.mk_UNIV BTs);
-
-    val talg_thm =
-      let
-        val goal = fold_rev Logic.all ss
-          (HOLogic.mk_Trueprop (mk_talg activeAs ss))
-      in
-        Goal.prove_sorry lthy [] [] goal
-          (K (rtac (alg_def RS iffD2) 1 THEN CONJ_WRAP (K (EVERY' [rtac ballI, rtac UNIV_I] 1)) ss))
-        |> Thm.close_derivation
-      end;
-
     val timer = time (timer "Algebra definition & thms");
 
     val alg_not_empty_thms =
@@ -362,12 +349,9 @@
         Term.list_comb (Const (mor, morT), args)
       end;
 
-    val (mor_image_thms, morE_thms) =
+    val morE_thms =
       let
         val prem = HOLogic.mk_Trueprop (mk_mor Bs ss B's s's fs);
-        fun mk_image_goal f B1 B2 = fold_rev Logic.all (Bs @ ss @ B's @ s's @ fs)
-          (Logic.mk_implies (prem, HOLogic.mk_Trueprop (mk_leq (mk_image f $ B1) B2)));
-        val image_goals = map3 mk_image_goal fs Bs B's;
         fun mk_elim_prem sets x T = HOLogic.mk_Trueprop
           (HOLogic.mk_mem (x, mk_in (passive_UNIVs @ Bs) sets T));
         fun mk_elim_goal sets mapAsBs f s s' x T =
@@ -378,7 +362,7 @@
         fun prove goal =
           Goal.prove_sorry lthy [] [] goal (K (mk_mor_elim_tac mor_def)) |> Thm.close_derivation;
       in
-        (map prove image_goals, map prove elim_goals)
+        map prove elim_goals
       end;
 
     val mor_incl_thm =
@@ -407,22 +391,6 @@
         |> Thm.close_derivation
       end;
 
-    val mor_inv_thm =
-      let
-        fun mk_inv_prem f inv_f B B' = HOLogic.mk_conj (mk_leq (mk_image inv_f $ B') B,
-          HOLogic.mk_conj (mk_inver inv_f f B, mk_inver f inv_f B'));
-        val prems = map HOLogic.mk_Trueprop
-          ([mk_mor Bs ss B's s's fs, mk_alg Bs ss, mk_alg B's s's] @
-          map4 mk_inv_prem fs inv_fs Bs B's);
-        val concl = HOLogic.mk_Trueprop (mk_mor B's s's Bs ss inv_fs);
-      in
-        Goal.prove_sorry lthy [] []
-          (fold_rev Logic.all (Bs @ ss @ B's @ s's @ fs @ inv_fs)
-            (Logic.list_implies (prems, concl)))
-          (K (mk_mor_inv_tac alg_def mor_def set_mapss morE_thms map_comp_id_thms map_cong0L_thms))
-        |> Thm.close_derivation
-      end;
-
     val mor_cong_thm =
       let
         val prems = map HOLogic.mk_Trueprop
@@ -476,80 +444,6 @@
 
     val timer = time (timer "Morphism definition & thms");
 
-    (* isomorphism *)
-
-    (*mor Bs1 ss1 Bs2 ss2 fs \<and> (\<exists>gs. mor Bs2 ss2 Bs1 ss1 fs \<and>
-       forall i = 1 ... n. (inver gs[i] fs[i] Bs1[i] \<and> inver fs[i] gs[i] Bs2[i]))*)
-    fun mk_iso Bs1 ss1 Bs2 ss2 fs gs =
-      let
-        val ex_inv_mor = list_exists_free gs
-          (HOLogic.mk_conj (mk_mor Bs2 ss2 Bs1 ss1 gs,
-            Library.foldr1 HOLogic.mk_conj (map2 (curry HOLogic.mk_conj)
-              (map3 mk_inver gs fs Bs1) (map3 mk_inver fs gs Bs2))));
-      in
-        HOLogic.mk_conj (mk_mor Bs1 ss1 Bs2 ss2 fs, ex_inv_mor)
-      end;
-
-    val iso_alt_thm =
-      let
-        val prems = map HOLogic.mk_Trueprop [mk_alg Bs ss, mk_alg B's s's]
-        val concl = mk_Trueprop_eq (mk_iso Bs ss B's s's fs inv_fs,
-          HOLogic.mk_conj (mk_mor Bs ss B's s's fs,
-            Library.foldr1 HOLogic.mk_conj (map3 mk_bij_betw fs Bs B's)));
-      in
-        Goal.prove_sorry lthy [] []
-          (fold_rev Logic.all (Bs @ ss @ B's @ s's @ fs) (Logic.list_implies (prems, concl)))
-          (K (mk_iso_alt_tac mor_image_thms mor_inv_thm))
-        |> Thm.close_derivation
-      end;
-
-    val timer = time (timer "Isomorphism definition & thms");
-
-    (* algebra copies *)
-
-    val (copy_alg_thm, ex_copy_alg_thm) =
-      let
-        val prems = map HOLogic.mk_Trueprop
-         (mk_alg Bs ss :: map3 mk_bij_betw inv_fs B's Bs);
-        val inver_prems = map HOLogic.mk_Trueprop
-          (map3 mk_inver inv_fs fs Bs @ map3 mk_inver fs inv_fs B's);
-        val all_prems = prems @ inver_prems;
-        fun mk_s f s mapT = Library.foldl1 HOLogic.mk_comp [f, s,
-          Term.list_comb (mapT, passive_ids @ inv_fs)];
-
-        val alg = HOLogic.mk_Trueprop
-          (mk_alg B's (map3 mk_s fs ss mapsBsAs));
-        val copy_str_thm = Goal.prove_sorry lthy [] []
-          (fold_rev Logic.all (Bs @ ss @ B's @ inv_fs @ fs)
-            (Logic.list_implies (all_prems, alg)))
-          (K (mk_copy_str_tac set_mapss alg_def alg_set_thms))
-          |> Thm.close_derivation;
-
-        val iso = HOLogic.mk_Trueprop
-          (mk_iso B's (map3 mk_s fs ss mapsBsAs) Bs ss inv_fs fs_copy);
-        val copy_alg_thm = Goal.prove_sorry lthy [] []
-          (fold_rev Logic.all (Bs @ ss @ B's @ inv_fs @ fs)
-            (Logic.list_implies (all_prems, iso)))
-          (fn {context = ctxt, prems = _} =>
-            mk_copy_alg_tac ctxt set_mapss alg_set_thms mor_def iso_alt_thm copy_str_thm)
-          |> Thm.close_derivation;
-
-        val ex = HOLogic.mk_Trueprop
-          (list_exists_free s's
-            (HOLogic.mk_conj (mk_alg B's s's,
-              mk_iso B's s's Bs ss inv_fs fs_copy)));
-        val ex_copy_alg_thm = Goal.prove_sorry lthy [] []
-          (fold_rev Logic.all (Bs @ ss @ B's @ inv_fs @ fs)
-             (Logic.list_implies (prems, ex)))
-          (K (mk_ex_copy_alg_tac n copy_str_thm copy_alg_thm))
-          |> Thm.close_derivation;
-      in
-        (copy_alg_thm, ex_copy_alg_thm)
-      end;
-
-    val timer = time (timer "Copy thms");
-
-
     (* bounds *)
 
     val sum_bd = Library.foldr1 (uncurry mk_csum) bds;
@@ -782,10 +676,10 @@
         Term.list_comb (Const (nth min_algs (i - 1), min_algT), ss)
       end;
 
+    val min_algs = map (mk_min_alg ss) ks;
+
     val (alg_min_alg_thm, card_of_min_alg_thms, least_min_alg_thms, mor_incl_min_alg_thm) =
       let
-        val min_algs = map (mk_min_alg ss) ks;
-
         val goal = fold_rev Logic.all ss (HOLogic.mk_Trueprop (mk_alg min_algs ss));
         val alg_min_alg = Goal.prove_sorry lthy [] [] goal
           (K (mk_alg_min_alg_tac m alg_def min_alg_defs suc_bd_limit_thm sbd_Cinfinite
@@ -793,8 +687,7 @@
           |> Thm.close_derivation;
 
         fun mk_card_of_thm min_alg def = Goal.prove_sorry lthy [] []
-          (fold_rev Logic.all ss
-            (HOLogic.mk_Trueprop (mk_ordLeq (mk_card_of min_alg) Asuc_bd)))
+          (HOLogic.mk_Trueprop (mk_ordLeq (mk_card_of min_alg) Asuc_bd))
           (K (mk_card_of_min_alg_tac def card_of_min_algs_thm
             suc_bd_Card_order suc_bd_Asuc_bd Asuc_bd_Cinfinite))
           |> Thm.close_derivation;
@@ -809,11 +702,10 @@
         val leasts = map3 mk_least_thm min_algs Bs min_alg_defs;
 
         val incl_prem = HOLogic.mk_Trueprop (mk_alg Bs ss);
-        val incl_min_algs = map (mk_min_alg ss) ks;
         val incl = Goal.prove_sorry lthy [] []
           (fold_rev Logic.all (Bs @ ss)
             (Logic.mk_implies (incl_prem,
-              HOLogic.mk_Trueprop (mk_mor incl_min_algs ss Bs ss active_ids))))
+              HOLogic.mk_Trueprop (mk_mor min_algs ss Bs ss active_ids))))
           (K (EVERY' (rtac mor_incl_thm :: map etac leasts) 1))
           |> Thm.close_derivation;
       in
@@ -904,33 +796,22 @@
 
     val mor_select_thm =
       let
-        val alg_prem = HOLogic.mk_Trueprop (mk_alg Bs ss);
         val i_prem = HOLogic.mk_Trueprop (HOLogic.mk_mem (iidx, II));
-        val mor_prem = HOLogic.mk_Trueprop (mk_mor select_Bs select_ss Bs ss Asuc_fs);
-        val prems = [alg_prem, i_prem, mor_prem];
+        val mor_prem = HOLogic.mk_Trueprop (mk_mor select_Bs select_ss active_UNIVs ss Asuc_fs);
+        val prems = [i_prem, mor_prem];
         val concl = HOLogic.mk_Trueprop
-          (mk_mor car_inits str_inits Bs ss
+          (mk_mor car_inits str_inits active_UNIVs ss
             (map (fn f => HOLogic.mk_comp (f, mk_rapp iidx Asuc_bdT)) Asuc_fs));
       in
         Goal.prove_sorry lthy [] []
-          (fold_rev Logic.all (iidx :: Bs @ ss @ Asuc_fs) (Logic.list_implies (prems, concl)))
+          (fold_rev Logic.all (iidx :: ss @ Asuc_fs) (Logic.list_implies (prems, concl)))
           (K (mk_mor_select_tac mor_def mor_cong_thm mor_comp_thm mor_incl_min_alg_thm alg_def
             alg_select_thm alg_set_thms set_mapss str_init_defs))
         |> Thm.close_derivation
       end;
 
-    val (init_ex_mor_thm, init_unique_mor_thms) =
+    val init_unique_mor_thms =
       let
-        val prem = HOLogic.mk_Trueprop (mk_alg Bs ss);
-        val concl = HOLogic.mk_Trueprop
-          (list_exists_free init_fs (mk_mor car_inits str_inits Bs ss init_fs));
-        val ex_mor = Goal.prove_sorry lthy [] []
-          (fold_rev Logic.all (Bs @ ss) (Logic.mk_implies (prem, concl)))
-          (fn {context = ctxt, prems = _} => mk_init_ex_mor_tac ctxt Abs_IIT_inverse_thm
-            ex_copy_alg_thm alg_min_alg_thm card_of_min_alg_thms mor_comp_thm mor_select_thm
-            mor_incl_min_alg_thm)
-          |> Thm.close_derivation;
-
         val prems = map2 (HOLogic.mk_Trueprop oo curry HOLogic.mk_mem) init_xs car_inits
         val mor_prems = map HOLogic.mk_Trueprop
           [mk_mor car_inits str_inits Bs ss init_fs,
@@ -945,7 +826,7 @@
             in_mono'_thms alg_set_thms morE_thms map_cong0s))
           |> Thm.close_derivation;
       in
-        (ex_mor, split_conj_thm unique_mor)
+        split_conj_thm unique_mor
       end;
 
     val init_setss = mk_setss (passiveAs @ active_initTs);
@@ -997,20 +878,9 @@
 
     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;
-    val Rep_injects = map #Rep_inject T_loc_infos;
     val Rep_inverses = map #Rep_inverse T_loc_infos;
     val Abs_inverses = map #Abs_inverse T_loc_infos;
 
-    fun mk_inver_thm mk_tac rep abs X thm =
-      Goal.prove_sorry lthy [] []
-        (HOLogic.mk_Trueprop (mk_inver rep abs X))
-        (K (EVERY' [rtac iffD2, rtac @{thm inver_def}, rtac ballI, mk_tac thm] 1))
-      |> 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 Abs_inverses;
-
     val timer = time (timer "THE TYPEDEFs & Rep/Abs thms");
 
     val UNIVs = map HOLogic.mk_UNIV Ts;
@@ -1071,21 +941,23 @@
 
     val (mor_Rep_thm, mor_Abs_thm) =
       let
-        val copy = alg_init_thm RS copy_alg_thm;
-        fun mk_bij inj Rep cases = @{thm bij_betwI'} OF [inj, Rep, cases];
-        val bijs = map3 mk_bij Rep_injects Reps Rep_casess;
+        val defs = mor_def :: ctor_defs;
+
         val mor_Rep =
           Goal.prove_sorry lthy [] []
             (HOLogic.mk_Trueprop (mk_mor UNIVs ctors car_inits str_inits Rep_Ts))
-            (fn {context = ctxt, prems = _} => mk_mor_Rep_tac ctxt ctor_defs copy bijs inver_Abss
-              inver_Reps)
+            (fn {context = ctxt, prems = _} => mk_mor_Rep_tac ctxt m defs Reps Abs_inverses
+              alg_min_alg_thm alg_set_thms set_mapss)
           |> Thm.close_derivation;
 
-        val inv = mor_inv_thm OF [mor_Rep, talg_thm, alg_init_thm];
+        fun mk_ct initFT str abs = Term.absdummy initFT (abs $ (str $ Bound 0))
+        val cts = map3 (SOME o certify lthy ooo mk_ct) init_FTs str_inits Abs_Ts;
+
         val mor_Abs =
           Goal.prove_sorry lthy [] []
             (HOLogic.mk_Trueprop (mk_mor car_inits str_inits UNIVs ctors Abs_Ts))
-            (K (mk_mor_Abs_tac inv inver_Abss inver_Reps))
+            (fn {context = ctxt, prems = _} => mk_mor_Abs_tac ctxt cts defs Abs_inverses
+              map_comp_id_thms map_cong0L_thms)
           |> Thm.close_derivation;
       in
         (mor_Rep, mor_Abs)
@@ -1122,18 +994,44 @@
     val fold_defs = map (fn def =>
       mk_unabs_def n (Morphism.thm phi def RS meta_eq_to_obj_eq)) fold_def_frees;
 
+    (* algebra copies *)
+
+    val copy_thm =
+      let
+        val prems = HOLogic.mk_Trueprop (mk_alg Bs ss) ::
+          map3 (HOLogic.mk_Trueprop ooo mk_bij_betw) inv_fs B's Bs;
+        val concl = HOLogic.mk_Trueprop (list_exists_free s's
+          (HOLogic.mk_conj (mk_alg B's s's, mk_mor B's s's Bs ss inv_fs)));
+      in
+        Goal.prove_sorry lthy [] []
+          (fold_rev Logic.all (Bs @ ss @ B's @ inv_fs) (Logic.list_implies (prems, concl)))
+          (K (mk_copy_tac m alg_def mor_def alg_set_thms set_mapss))
+          |> Thm.close_derivation
+      end;
+
+    val init_ex_mor_thm =
+      let
+        val goal = HOLogic.mk_Trueprop
+          (list_exists_free fs (mk_mor UNIVs ctors active_UNIVs ss fs));
+      in
+        singleton (Proof_Context.export names_lthy lthy)
+          (Goal.prove_sorry lthy [] [] goal
+            (fn {context = ctxt, prems = _} =>
+              mk_init_ex_mor_tac ctxt Abs_IIT_inverse_thm (alg_min_alg_thm RS copy_thm)
+                card_of_min_alg_thms mor_Rep_thm mor_comp_thm mor_select_thm mor_incl_thm)
+            |> Thm.close_derivation)
+      end;
+
     val mor_fold_thm =
       let
-        val ex_mor = talg_thm RS init_ex_mor_thm;
         val mor_cong = mor_cong_thm OF (map (mk_nth_conv n) ks);
-        val mor_comp = mor_Rep_thm RS mor_comp_thm;
         val cT = certifyT lthy foldT;
         val ct = certify lthy fold_fun
       in
         singleton (Proof_Context.export names_lthy lthy)
           (Goal.prove_sorry lthy [] []
             (HOLogic.mk_Trueprop (mk_mor UNIVs ctors active_UNIVs ss (map (mk_fold Ts ss) ks)))
-            (K (mk_mor_fold_tac cT ct fold_defs ex_mor (mor_comp RS mor_cong))))
+            (K (mk_mor_fold_tac cT ct fold_defs init_ex_mor_thm mor_cong)))
         |> Thm.close_derivation
       end;
 
diff -r 713ae0c9e652 -r 69a9dfe71aed src/HOL/Tools/BNF/bnf_lfp_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Thu Mar 20 23:38:34 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Fri Mar 21 08:13:23 2014 +0100
@@ -16,8 +16,7 @@
   val mk_bd_card_order_tac: thm list -> tactic
   val mk_bd_limit_tac: int -> thm -> tactic
   val mk_card_of_min_alg_tac: thm -> thm -> thm -> thm -> thm -> tactic
-  val mk_copy_alg_tac: Proof.context -> thm list list -> thm list -> thm -> thm -> thm -> tactic
-  val mk_copy_str_tac: thm list list -> thm -> thm list -> tactic
+  val mk_copy_tac: int -> thm -> thm -> thm list -> thm list list -> tactic
   val mk_ctor_induct_tac: Proof.context -> int -> thm list list -> thm -> thm list -> thm ->
     thm list -> thm list -> thm list -> tactic
   val mk_ctor_induct2_tac: Proof.context -> ctyp option list -> cterm option list -> thm ->
@@ -26,13 +25,11 @@
   val mk_ctor_rel_tac: Proof.context -> thm list -> int -> thm -> thm -> thm -> thm -> thm list ->
     thm -> thm -> thm list -> thm list -> thm list list -> tactic
   val mk_dtor_o_ctor_tac: thm -> thm -> thm -> thm -> thm list -> tactic
-  val mk_ex_copy_alg_tac: int -> thm -> thm -> tactic
-  val mk_init_ex_mor_tac: Proof.context -> thm -> thm -> thm -> thm list -> thm -> thm -> thm ->
+  val mk_init_ex_mor_tac: Proof.context -> thm -> thm -> thm list -> thm -> thm -> thm -> thm ->
     tactic
   val mk_init_induct_tac: int -> thm -> thm -> thm list -> thm list -> tactic
   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_fold_unique_mor_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> tactic
   val mk_fold_transfer_tac: Proof.context -> int -> thm -> thm list -> thm list -> tactic
   val mk_least_min_alg_tac: thm -> thm -> tactic
@@ -49,14 +46,15 @@
   val mk_min_algs_least_tac: ctyp -> cterm -> thm -> thm list -> thm list -> tactic
   val mk_min_algs_mono_tac: Proof.context -> thm -> tactic
   val mk_min_algs_tac: thm -> thm list -> tactic
-  val mk_mor_Abs_tac: thm -> thm list -> thm list -> tactic
-  val mk_mor_Rep_tac: Proof.context -> thm list -> thm -> thm list -> thm list -> thm list -> tactic
+  val mk_mor_Abs_tac: Proof.context -> cterm option list -> thm list -> thm list -> thm list ->
+    thm list -> tactic
+  val mk_mor_Rep_tac: Proof.context -> int -> thm list -> thm list -> thm list -> thm -> thm list ->
+    thm list list -> tactic
   val mk_mor_UNIV_tac: int -> thm list -> thm -> tactic
   val mk_mor_comp_tac: thm -> thm list list -> thm list -> tactic
   val mk_mor_convol_tac: 'a list -> thm -> tactic
   val mk_mor_elim_tac: thm -> tactic
   val mk_mor_incl_tac: thm -> thm list -> tactic
-  val mk_mor_inv_tac: thm -> thm -> thm list list -> thm list -> thm list -> thm list -> tactic
   val mk_mor_fold_tac: ctyp -> cterm -> thm list -> thm -> thm -> tactic
   val mk_mor_select_tac: thm -> thm -> thm -> thm -> thm -> thm -> thm list -> thm list list ->
     thm list -> tactic
@@ -138,32 +136,6 @@
     CONJ_WRAP' mor_tac (set_maps ~~ map_comp_ids)) 1
   end;
 
-fun mk_mor_inv_tac alg_def mor_def set_maps morEs map_comp_ids map_cong0Ls =
-  let
-    val fbetw_tac = EVERY' [rtac ballI, etac set_mp, etac imageI];
-    fun Collect_tac set_map =
-      CONJ_WRAP' (fn thm =>
-        FIRST' [rtac subset_UNIV,
-          (EVERY' [rtac ord_eq_le_trans, rtac thm, rtac subset_trans,
-            etac @{thm image_mono}, atac])]) set_map;
-    fun mor_tac (set_map, ((morE, map_comp_id), map_cong0L)) =
-      EVERY' [rtac ballI, ftac rev_bspec, atac,
-         REPEAT o eresolve_tac [CollectE, conjE], rtac sym, rtac trans, rtac sym,
-         etac @{thm inverE}, etac bspec, rtac CollectI, Collect_tac set_map,
-         rtac trans, etac (morE RS arg_cong), rtac CollectI, Collect_tac set_map,
-         rtac trans, rtac (map_comp_id RS arg_cong), rtac (map_cong0L RS arg_cong),
-         REPEAT_DETERM_N (length morEs) o
-           (EVERY' [rtac iffD1, rtac @{thm inver_pointfree}, etac @{thm inver_mono}, atac])];
-  in
-    (rtac (mor_def RS iffD2) THEN'
-    dtac (alg_def RS iffD1) THEN'
-    dtac (alg_def RS iffD1) THEN'
-    REPEAT o etac conjE THEN'
-    rtac conjI THEN'
-    CONJ_WRAP' (K fbetw_tac) set_maps THEN'
-    CONJ_WRAP' mor_tac (set_maps ~~ (morEs ~~ map_comp_ids ~~ map_cong0Ls))) 1
-  end;
-
 fun mk_mor_str_tac ks mor_def =
   (rtac (mor_def RS iffD2) THEN' rtac conjI THEN'
   CONJ_WRAP' (K (EVERY' [rtac ballI, rtac UNIV_I])) ks THEN'
@@ -188,74 +160,30 @@
       etac (o_apply RS sym RS trans), rtac o_apply])) morEs] 1
   end;
 
-fun mk_iso_alt_tac mor_images mor_inv =
-  let
-    val n = length mor_images;
-    fun if_wrap_tac thm =
-      EVERY' [rtac iffD2, rtac @{thm bij_betw_iff_ex}, rtac exI, rtac conjI,
-        rtac @{thm inver_surj}, etac thm, etac thm, atac, etac conjI, atac]
-    val if_tac =
-      EVERY' [etac thin_rl, etac thin_rl, REPEAT o eresolve_tac [conjE, exE],
-        rtac conjI, atac, CONJ_WRAP' if_wrap_tac mor_images];
-    val only_if_tac =
-      EVERY' [rtac conjI, etac conjunct1, EVERY' (map (fn thm =>
-        EVERY' [rtac exE, rtac @{thm bij_betw_ex_weakE}, etac (conjunct2 RS thm)])
-        (map (mk_conjunctN n) (1 upto n))), REPEAT o rtac exI, rtac conjI, rtac mor_inv,
-        etac conjunct1, atac, atac, REPEAT_DETERM_N n o atac,
-        CONJ_WRAP' (K (etac conjunct2)) mor_images];
-  in
-    (rtac iffI THEN' if_tac THEN' only_if_tac) 1
-  end;
-
-fun mk_copy_str_tac set_maps alg_def alg_sets =
+fun mk_copy_tac m alg_def mor_def alg_sets set_mapss =
   let
     val n = length alg_sets;
-    val bij_betw_inv_tac =
-      EVERY' [etac thin_rl, REPEAT_DETERM_N n o EVERY' [dtac @{thm bij_betwI}, atac, atac],
-        REPEAT_DETERM_N (2 * n) o etac thin_rl, REPEAT_DETERM_N (n - 1) o etac conjI, atac];
-    fun set_tac thms =
-      EVERY' [rtac ord_eq_le_trans, resolve_tac thms, rtac subset_trans,
-          etac @{thm image_mono}, rtac equalityD1, etac @{thm bij_betw_imageE}];
-    val copy_str_tac =
-      CONJ_WRAP' (fn (thms, thm) =>
+    fun set_tac thm =
+      EVERY' [rtac ord_eq_le_trans, rtac thm, rtac subset_trans, etac @{thm image_mono},
+        rtac equalityD1, etac @{thm bij_betw_imageE}];
+    val alg_tac =
+      CONJ_WRAP' (fn (set_maps, alg_set) =>
         EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac set_mp,
-          rtac equalityD1, etac @{thm bij_betw_imageE},
-          REPEAT_DETERM_N 2 o rtac @{thm ssubst_mem[OF o_apply]}, rtac imageI, etac thm,
-          REPEAT_DETERM_N n o set_tac thms])
-      (set_maps ~~ alg_sets);
-  in
-    (rtac rev_mp THEN' DETERM o bij_betw_inv_tac THEN' rtac impI THEN'
-    rtac (alg_def RS iffD2) THEN' copy_str_tac) 1
-  end;
+          rtac equalityD1, etac @{thm bij_betw_imageE[OF bij_betw_the_inv_into]},
+          rtac imageI, etac alg_set, EVERY' (map set_tac (drop m set_maps))])
+      (set_mapss ~~ alg_sets);
 
-fun mk_copy_alg_tac ctxt set_maps alg_sets mor_def iso_alt copy_str =
-  let
-    val n = length alg_sets;
-    val fbetw_tac = CONJ_WRAP' (K (etac @{thm bij_betwE})) alg_sets;
-    fun set_tac thms =
-      EVERY' [rtac ord_eq_le_trans, resolve_tac thms, rtac subset_trans,
-        REPEAT_DETERM o etac conjE, etac @{thm image_mono},
-        rtac equalityD1, etac @{thm bij_betw_imageE}];
-    val mor_tac =
-      CONJ_WRAP' (fn (thms, thm) =>
-        EVERY' [rtac ballI, etac CollectE, SELECT_GOAL (unfold_thms_tac ctxt [o_apply]),
-          etac @{thm inverE}, etac thm, REPEAT_DETERM_N n o set_tac thms])
-      (set_maps ~~ alg_sets);
+    val mor_tac = rtac conjI THEN' CONJ_WRAP' (K (etac @{thm bij_betwE})) alg_sets THEN'
+      CONJ_WRAP' (fn (set_maps, alg_set) =>
+        EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, conjE],
+          etac @{thm f_the_inv_into_f_bij_betw}, etac alg_set,
+          EVERY' (map set_tac (drop m set_maps))])
+      (set_mapss ~~ alg_sets);
   in
-    (rtac (iso_alt RS iffD2) THEN' etac copy_str THEN' REPEAT_DETERM o atac THEN'
-    rtac conjI THEN' rtac (mor_def RS iffD2) THEN' rtac conjI THEN' fbetw_tac THEN' mor_tac THEN'
-    CONJ_WRAP' (K atac) alg_sets) 1
+    (REPEAT_DETERM_N n o rtac exI THEN' rtac conjI THEN'
+    rtac (alg_def RS iffD2) THEN' alg_tac THEN' rtac (mor_def RS iffD2) THEN' mor_tac) 1
   end;
 
-fun mk_ex_copy_alg_tac n copy_str copy_alg =
-  EVERY' [REPEAT_DETERM_N n o rtac exI, rtac conjI, etac copy_str,
-    REPEAT_DETERM_N n o atac,
-    REPEAT_DETERM_N n o etac @{thm bij_betw_inver2},
-    REPEAT_DETERM_N n o etac @{thm bij_betw_inver1}, etac copy_alg,
-    REPEAT_DETERM_N n o atac,
-    REPEAT_DETERM_N n o etac @{thm bij_betw_inver2},
-    REPEAT_DETERM_N n o etac @{thm bij_betw_inver1}] 1;
-
 fun mk_bd_limit_tac n bd_Cinfinite =
   EVERY' [REPEAT_DETERM o etac conjE, rtac rev_mp, rtac @{thm Cinfinite_limit_finite},
     REPEAT_DETERM_N n o rtac @{thm finite.insertI}, rtac @{thm finite.emptyI},
@@ -408,30 +336,17 @@
       rtac (alg_def RS iffD2), CONJ_WRAP' alg_epi_tac ((alg_sets ~~ str_init_defs) ~~ set_maps)] 1
   end;
 
-fun mk_init_ex_mor_tac ctxt Abs_inverse copy_alg_ex alg_min_alg card_of_min_algs
-    mor_comp mor_select mor_incl_min_alg =
+fun mk_init_ex_mor_tac ctxt Abs_inverse copy card_of_min_algs mor_Rep mor_comp mor_select mor_incl =
   let
     val n = length card_of_min_algs;
-    val card_of_ordIso_tac = EVERY' [rtac iffD2, rtac @{thm card_of_ordIso},
-      rtac @{thm ordIso_symmetric}, rtac conjunct1, rtac conjunct2, atac];
-    fun internalize_tac card_of = EVERY' [rtac iffD1, rtac @{thm internalize_card_of_ordLeq2},
-      rtac @{thm ordLeq_ordIso_trans}, rtac card_of, rtac iffD1,
-      rtac @{thm Card_order_iff_ordIso_card_of}, rtac @{thm Card_order_cexp}];
   in
-    (rtac rev_mp THEN'
-    REPEAT_DETERM_N (2 * n) o (rtac mp THEN' rtac @{thm ex_mono} THEN' rtac impI) THEN'
-    REPEAT_DETERM_N (n + 1) o etac thin_rl THEN' rtac (alg_min_alg RS copy_alg_ex) THEN'
-    REPEAT_DETERM_N n o atac THEN'
-    REPEAT_DETERM_N n o card_of_ordIso_tac THEN'
-    EVERY' (map internalize_tac card_of_min_algs) THEN'
-    rtac impI THEN'
-    REPEAT_DETERM o eresolve_tac [exE, conjE] THEN'
-    REPEAT_DETERM o rtac exI THEN'
-    rtac mor_select THEN' atac THEN' rtac CollectI THEN'
-    REPEAT_DETERM o rtac exI THEN'
-    rtac conjI THEN' rtac refl THEN' atac THEN'
-    K (unfold_thms_tac ctxt (Abs_inverse :: fst_snd_convs)) THEN'
-    etac mor_comp THEN' etac mor_incl_min_alg) 1
+    EVERY' [Method.insert_tac (map (fn thm => thm RS @{thm ex_bij_betw}) card_of_min_algs),
+      REPEAT_DETERM o etac exE, rtac rev_mp, rtac copy, REPEAT_DETERM_N n o atac,
+      rtac impI, REPEAT_DETERM o eresolve_tac [exE, conjE], REPEAT_DETERM_N n o rtac exI,
+      rtac mor_comp, rtac mor_Rep, rtac mor_select, rtac CollectI, REPEAT_DETERM o rtac exI,
+      rtac conjI, rtac refl, atac,
+      SELECT_GOAL (unfold_thms_tac ctxt (Abs_inverse :: fst_snd_convs)),
+      etac mor_comp, rtac mor_incl, REPEAT_DETERM_N n o rtac subset_UNIV] 1
   end;
 
 fun mk_init_unique_mor_tac m
@@ -482,17 +397,28 @@
     CONJ_WRAP' mk_induct_tac least_min_algs 1
   end;
 
-fun mk_mor_Rep_tac ctxt ctor_defs copy bijs inver_Abss inver_Reps =
-  (K (unfold_thms_tac ctxt ctor_defs) THEN' rtac conjunct1 THEN' rtac copy THEN'
-  EVERY' (map (fn bij => EVERY' [rtac bij, atac, etac bexI, rtac UNIV_I]) bijs) THEN'
-  EVERY' (map rtac inver_Abss) THEN'
-  EVERY' (map rtac inver_Reps)) 1;
+fun mk_mor_Rep_tac ctxt m defs Reps Abs_inverses alg_min_alg alg_sets set_mapss =
+  unfold_thms_tac ctxt (@{thm o_apply} :: defs) THEN
+  EVERY' [rtac conjI,
+    CONJ_WRAP' (fn thm => rtac ballI THEN' rtac thm) Reps,
+    CONJ_WRAP' (fn (Abs_inverse, (set_maps, alg_set)) =>
+      EVERY' [rtac ballI, rtac Abs_inverse, rtac (alg_min_alg RS alg_set),
+        EVERY' (map2 (fn Rep => fn set_map =>
+          EVERY' [rtac (set_map RS ord_eq_le_trans), rtac @{thm image_subsetI}, rtac Rep])
+        Reps (drop m set_maps))])
+    (Abs_inverses ~~ (set_mapss ~~ alg_sets))] 1;
 
-fun mk_mor_Abs_tac inv inver_Abss inver_Reps =
-  (rtac inv THEN'
-  EVERY' (map2 (fn inver_Abs => fn inver_Rep =>
-    EVERY' [rtac conjI, rtac subset_UNIV, rtac conjI, rtac inver_Rep, rtac inver_Abs])
-    inver_Abss inver_Reps)) 1;
+fun mk_mor_Abs_tac ctxt cts defs Abs_inverses map_comp_ids map_congLs =
+  unfold_thms_tac ctxt (@{thm o_apply} :: defs) THEN
+  EVERY' [rtac conjI,
+    CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) Abs_inverses,
+    CONJ_WRAP' (fn (ct, thm) =>
+      EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, conjE],
+        rtac (thm RS (cterm_instantiate_pos [NONE, NONE, ct] arg_cong) RS sym),
+        EVERY' (map (fn Abs_inverse =>
+          EVERY' [rtac (o_apply RS trans RS ballI), etac (set_mp RS Abs_inverse), atac])
+        Abs_inverses)])
+    (cts ~~ map2 mk_trans map_comp_ids map_congLs)] 1;;
 
 fun mk_mor_fold_tac cT ct fold_defs ex_mor mor =
   (EVERY' (map stac fold_defs) THEN' EVERY' [rtac rev_mp, rtac ex_mor, rtac impI] THEN'
diff -r 713ae0c9e652 -r 69a9dfe71aed src/HOL/Tools/BNF/bnf_lfp_util.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_util.ML	Thu Mar 20 23:38:34 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_util.ML	Fri Mar 21 08:13:23 2014 +0100
@@ -12,7 +12,6 @@
 
   val mk_bij_betw: term -> term -> term -> term
   val mk_cardSuc: term -> term
-  val mk_inver: term -> term -> term -> term
   val mk_not_empty: term -> term
   val mk_not_eq: term -> term -> term
   val mk_rapp: term -> typ -> term
@@ -52,10 +51,6 @@
  Const (@{const_name bij_betw},
    fastype_of f --> fastype_of A --> fastype_of B --> HOLogic.boolT) $ f $ A $ B;
 
-fun mk_inver f g A =
- Const (@{const_name inver}, fastype_of f --> fastype_of g --> fastype_of A --> HOLogic.boolT) $
-   f $ g $ A;
-
 fun mk_not_eq x y = HOLogic.mk_not (HOLogic.mk_eq (x, y));
 
 fun mk_not_empty B = mk_not_eq B (HOLogic.mk_set (HOLogic.dest_setT (fastype_of B)) []);