simplified internal datatype construction
authortraytel
Fri Mar 21 08:13:23 2014 +0100 (2014-03-21)
changeset 5623769a9dfe71aed
parent 56236 713ae0c9e652
child 56238 5d147e1e18d1
child 56239 17df7145a871
simplified internal datatype construction
src/HOL/BNF_LFP.thy
src/HOL/Main.thy
src/HOL/Tools/BNF/bnf_lfp.ML
src/HOL/Tools/BNF/bnf_lfp_tactics.ML
src/HOL/Tools/BNF/bnf_lfp_util.ML
     1.1 --- a/src/HOL/BNF_LFP.thy	Thu Mar 20 23:38:34 2014 +0100
     1.2 +++ b/src/HOL/BNF_LFP.thy	Fri Mar 21 08:13:23 2014 +0100
     1.3 @@ -60,88 +60,19 @@
     1.4    moreover have "\<dots> \<longleftrightarrow> <g, h> = f" by (subst (2) *[symmetric]) (auto simp: convol_def fun_eq_iff)
     1.5    ultimately show ?thesis by simp
     1.6  qed
     1.7 -
     1.8 -definition inver where
     1.9 -  "inver g f A = (ALL a : A. g (f a) = a)"
    1.10 -
    1.11 -lemma bij_betw_iff_ex:
    1.12 -  "bij_betw f A B = (EX g. g ` B = A \<and> inver g f A \<and> inver f g B)" (is "?L = ?R")
    1.13 -proof (rule iffI)
    1.14 -  assume ?L
    1.15 -  hence f: "f ` A = B" and inj_f: "inj_on f A" unfolding bij_betw_def by auto
    1.16 -  let ?phi = "% b a. a : A \<and> f a = b"
    1.17 -  have "ALL b : B. EX a. ?phi b a" using f by blast
    1.18 -  then obtain g where g: "ALL b : B. g b : A \<and> f (g b) = b"
    1.19 -    using bchoice[of B ?phi] by blast
    1.20 -  hence gg: "ALL b : f ` A. g b : A \<and> f (g b) = b" using f by blast
    1.21 -  have gf: "inver g f A" unfolding inver_def
    1.22 -  proof
    1.23 -    fix a assume "a \<in> A"
    1.24 -    then show "g (f a) = a" using the_inv_into_f_f[OF inj_f, of "g (f a)"]
    1.25 -      the_inv_into_f_f[OF inj_f, of a] gg imageI[of a A f] by auto
    1.26 -  qed
    1.27 -  moreover have "g ` B \<le> A \<and> inver f g B" using g unfolding inver_def by blast
    1.28 -  moreover have "A \<le> g ` B"
    1.29 -  proof safe
    1.30 -    fix a assume a: "a : A"
    1.31 -    hence "f a : B" using f by auto
    1.32 -    moreover have "a = g (f a)" using a gf unfolding inver_def by auto
    1.33 -    ultimately show "a : g ` B" by blast
    1.34 -  qed
    1.35 -  ultimately show ?R by blast
    1.36 -next
    1.37 -  assume ?R
    1.38 -  then obtain g where g: "g ` B = A \<and> inver g f A \<and> inver f g B" by blast
    1.39 -  show ?L unfolding bij_betw_def
    1.40 -  proof safe
    1.41 -    show "inj_on f A" unfolding inj_on_def
    1.42 -    proof safe
    1.43 -      fix a1 a2 assume a: "a1 : A"  "a2 : A" and "f a1 = f a2"
    1.44 -      hence "g (f a1) = g (f a2)" by simp
    1.45 -      thus "a1 = a2" using a g unfolding inver_def by simp
    1.46 -    qed
    1.47 -  next
    1.48 -    fix a assume "a : A"
    1.49 -    then obtain b where b: "b : B" and a: "a = g b" using g by blast
    1.50 -    hence "b = f (g b)" using g unfolding inver_def by auto
    1.51 -    thus "f a : B" unfolding a using b by simp
    1.52 -  next
    1.53 -    fix b assume "b : B"
    1.54 -    hence "g b : A \<and> b = f (g b)" using g unfolding inver_def by auto
    1.55 -    thus "b : f ` A" by auto
    1.56 -  qed
    1.57 -qed
    1.58 -
    1.59 -lemma bij_betw_ex_weakE:
    1.60 -  "\<lbrakk>bij_betw f A B\<rbrakk> \<Longrightarrow> \<exists>g. g ` B \<subseteq> A \<and> inver g f A \<and> inver f g B"
    1.61 -by (auto simp only: bij_betw_iff_ex)
    1.62 -
    1.63 -lemma inver_surj: "\<lbrakk>g ` B \<subseteq> A; f ` A \<subseteq> B; inver g f A\<rbrakk> \<Longrightarrow> g ` B = A"
    1.64 -unfolding inver_def by auto (rule rev_image_eqI, auto)
    1.65 -
    1.66 -lemma inver_mono: "\<lbrakk>A \<subseteq> B; inver f g B\<rbrakk> \<Longrightarrow> inver f g A"
    1.67 -unfolding inver_def by auto
    1.68 -
    1.69 -lemma inver_pointfree: "inver f g A = (\<forall>a \<in> A. (f o g) a = a)"
    1.70 -unfolding inver_def by simp
    1.71 -
    1.72  lemma bij_betwE: "bij_betw f A B \<Longrightarrow> \<forall>a\<in>A. f a \<in> B"
    1.73  unfolding bij_betw_def by auto
    1.74  
    1.75  lemma bij_betw_imageE: "bij_betw f A B \<Longrightarrow> f ` A = B"
    1.76  unfolding bij_betw_def by auto
    1.77  
    1.78 -lemma inverE: "\<lbrakk>inver f f' A; x \<in> A\<rbrakk> \<Longrightarrow> f (f' x) = x"
    1.79 -unfolding inver_def by auto
    1.80 -
    1.81 -lemma bij_betw_inver1: "bij_betw f A B \<Longrightarrow> inver (inv_into A f) f A"
    1.82 -unfolding bij_betw_def inver_def by auto
    1.83 +lemma f_the_inv_into_f_bij_betw: "bij_betw f A B \<Longrightarrow>
    1.84 +  (bij_betw f A B \<Longrightarrow> x \<in> B) \<Longrightarrow> f (the_inv_into A f x) = x"
    1.85 +  unfolding bij_betw_def by (blast intro: f_the_inv_into_f)
    1.86  
    1.87 -lemma bij_betw_inver2: "bij_betw f A B \<Longrightarrow> inver f (inv_into A f) B"
    1.88 -unfolding bij_betw_def inver_def by auto
    1.89 -
    1.90 -lemma bij_betwI: "\<lbrakk>bij_betw g B A; inver g f A; inver f g B\<rbrakk> \<Longrightarrow> bij_betw f A B"
    1.91 -by (drule bij_betw_imageE, unfold bij_betw_iff_ex) blast
    1.92 +lemma ex_bij_betw: "|A| \<le>o (r :: 'b rel) \<Longrightarrow> \<exists>f B :: 'b set. bij_betw f B A"
    1.93 +  by (subst (asm) internalize_card_of_ordLeq)
    1.94 +    (auto dest!: iffD2[OF card_of_ordIso ordIso_symmetric])
    1.95  
    1.96  lemma bij_betwI':
    1.97    "\<lbrakk>\<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> (f x = f y) = (x = y);
     2.1 --- a/src/HOL/Main.thy	Thu Mar 20 23:38:34 2014 +0100
     2.2 +++ b/src/HOL/Main.thy	Fri Mar 21 08:13:23 2014 +0100
     2.3 @@ -31,7 +31,7 @@
     2.4  hide_const (open)
     2.5    czero cinfinite cfinite csum cone ctwo Csum cprod cexp
     2.6    image2 image2p vimage2p Gr Grp collect fsts snds setl setr
     2.7 -  convol pick_middlep fstOp sndOp csquare inver relImage relInvImage
     2.8 +  convol pick_middlep fstOp sndOp csquare relImage relInvImage
     2.9    Succ Shift shift proj
    2.10  
    2.11  no_syntax (xsymbols)
     3.1 --- a/src/HOL/Tools/BNF/bnf_lfp.ML	Thu Mar 20 23:38:34 2014 +0100
     3.2 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Fri Mar 21 08:13:23 2014 +0100
     3.3 @@ -104,7 +104,6 @@
     3.4      (* terms *)
     3.5      val mapsAsAs = map4 mk_map_of_bnf Dss Ass Ass bnfs;
     3.6      val mapsAsBs = map4 mk_map_of_bnf Dss Ass Bss bnfs;
     3.7 -    val mapsBsAs = map4 mk_map_of_bnf Dss Bss Ass bnfs;
     3.8      val mapsBsCs' = map4 mk_map_of_bnf Dss Bss Css' bnfs;
     3.9      val mapsAsCs' = map4 mk_map_of_bnf Dss Ass Css' bnfs;
    3.10      val map_fsts = map4 mk_map_of_bnf Dss (replicate n (passiveAs @ prodBsAs)) Bss bnfs;
    3.11 @@ -288,18 +287,6 @@
    3.12          goals
    3.13        end;
    3.14  
    3.15 -    fun mk_talg BTs = mk_alg (map HOLogic.mk_UNIV BTs);
    3.16 -
    3.17 -    val talg_thm =
    3.18 -      let
    3.19 -        val goal = fold_rev Logic.all ss
    3.20 -          (HOLogic.mk_Trueprop (mk_talg activeAs ss))
    3.21 -      in
    3.22 -        Goal.prove_sorry lthy [] [] goal
    3.23 -          (K (rtac (alg_def RS iffD2) 1 THEN CONJ_WRAP (K (EVERY' [rtac ballI, rtac UNIV_I] 1)) ss))
    3.24 -        |> Thm.close_derivation
    3.25 -      end;
    3.26 -
    3.27      val timer = time (timer "Algebra definition & thms");
    3.28  
    3.29      val alg_not_empty_thms =
    3.30 @@ -362,12 +349,9 @@
    3.31          Term.list_comb (Const (mor, morT), args)
    3.32        end;
    3.33  
    3.34 -    val (mor_image_thms, morE_thms) =
    3.35 +    val morE_thms =
    3.36        let
    3.37          val prem = HOLogic.mk_Trueprop (mk_mor Bs ss B's s's fs);
    3.38 -        fun mk_image_goal f B1 B2 = fold_rev Logic.all (Bs @ ss @ B's @ s's @ fs)
    3.39 -          (Logic.mk_implies (prem, HOLogic.mk_Trueprop (mk_leq (mk_image f $ B1) B2)));
    3.40 -        val image_goals = map3 mk_image_goal fs Bs B's;
    3.41          fun mk_elim_prem sets x T = HOLogic.mk_Trueprop
    3.42            (HOLogic.mk_mem (x, mk_in (passive_UNIVs @ Bs) sets T));
    3.43          fun mk_elim_goal sets mapAsBs f s s' x T =
    3.44 @@ -378,7 +362,7 @@
    3.45          fun prove goal =
    3.46            Goal.prove_sorry lthy [] [] goal (K (mk_mor_elim_tac mor_def)) |> Thm.close_derivation;
    3.47        in
    3.48 -        (map prove image_goals, map prove elim_goals)
    3.49 +        map prove elim_goals
    3.50        end;
    3.51  
    3.52      val mor_incl_thm =
    3.53 @@ -407,22 +391,6 @@
    3.54          |> Thm.close_derivation
    3.55        end;
    3.56  
    3.57 -    val mor_inv_thm =
    3.58 -      let
    3.59 -        fun mk_inv_prem f inv_f B B' = HOLogic.mk_conj (mk_leq (mk_image inv_f $ B') B,
    3.60 -          HOLogic.mk_conj (mk_inver inv_f f B, mk_inver f inv_f B'));
    3.61 -        val prems = map HOLogic.mk_Trueprop
    3.62 -          ([mk_mor Bs ss B's s's fs, mk_alg Bs ss, mk_alg B's s's] @
    3.63 -          map4 mk_inv_prem fs inv_fs Bs B's);
    3.64 -        val concl = HOLogic.mk_Trueprop (mk_mor B's s's Bs ss inv_fs);
    3.65 -      in
    3.66 -        Goal.prove_sorry lthy [] []
    3.67 -          (fold_rev Logic.all (Bs @ ss @ B's @ s's @ fs @ inv_fs)
    3.68 -            (Logic.list_implies (prems, concl)))
    3.69 -          (K (mk_mor_inv_tac alg_def mor_def set_mapss morE_thms map_comp_id_thms map_cong0L_thms))
    3.70 -        |> Thm.close_derivation
    3.71 -      end;
    3.72 -
    3.73      val mor_cong_thm =
    3.74        let
    3.75          val prems = map HOLogic.mk_Trueprop
    3.76 @@ -476,80 +444,6 @@
    3.77  
    3.78      val timer = time (timer "Morphism definition & thms");
    3.79  
    3.80 -    (* isomorphism *)
    3.81 -
    3.82 -    (*mor Bs1 ss1 Bs2 ss2 fs \<and> (\<exists>gs. mor Bs2 ss2 Bs1 ss1 fs \<and>
    3.83 -       forall i = 1 ... n. (inver gs[i] fs[i] Bs1[i] \<and> inver fs[i] gs[i] Bs2[i]))*)
    3.84 -    fun mk_iso Bs1 ss1 Bs2 ss2 fs gs =
    3.85 -      let
    3.86 -        val ex_inv_mor = list_exists_free gs
    3.87 -          (HOLogic.mk_conj (mk_mor Bs2 ss2 Bs1 ss1 gs,
    3.88 -            Library.foldr1 HOLogic.mk_conj (map2 (curry HOLogic.mk_conj)
    3.89 -              (map3 mk_inver gs fs Bs1) (map3 mk_inver fs gs Bs2))));
    3.90 -      in
    3.91 -        HOLogic.mk_conj (mk_mor Bs1 ss1 Bs2 ss2 fs, ex_inv_mor)
    3.92 -      end;
    3.93 -
    3.94 -    val iso_alt_thm =
    3.95 -      let
    3.96 -        val prems = map HOLogic.mk_Trueprop [mk_alg Bs ss, mk_alg B's s's]
    3.97 -        val concl = mk_Trueprop_eq (mk_iso Bs ss B's s's fs inv_fs,
    3.98 -          HOLogic.mk_conj (mk_mor Bs ss B's s's fs,
    3.99 -            Library.foldr1 HOLogic.mk_conj (map3 mk_bij_betw fs Bs B's)));
   3.100 -      in
   3.101 -        Goal.prove_sorry lthy [] []
   3.102 -          (fold_rev Logic.all (Bs @ ss @ B's @ s's @ fs) (Logic.list_implies (prems, concl)))
   3.103 -          (K (mk_iso_alt_tac mor_image_thms mor_inv_thm))
   3.104 -        |> Thm.close_derivation
   3.105 -      end;
   3.106 -
   3.107 -    val timer = time (timer "Isomorphism definition & thms");
   3.108 -
   3.109 -    (* algebra copies *)
   3.110 -
   3.111 -    val (copy_alg_thm, ex_copy_alg_thm) =
   3.112 -      let
   3.113 -        val prems = map HOLogic.mk_Trueprop
   3.114 -         (mk_alg Bs ss :: map3 mk_bij_betw inv_fs B's Bs);
   3.115 -        val inver_prems = map HOLogic.mk_Trueprop
   3.116 -          (map3 mk_inver inv_fs fs Bs @ map3 mk_inver fs inv_fs B's);
   3.117 -        val all_prems = prems @ inver_prems;
   3.118 -        fun mk_s f s mapT = Library.foldl1 HOLogic.mk_comp [f, s,
   3.119 -          Term.list_comb (mapT, passive_ids @ inv_fs)];
   3.120 -
   3.121 -        val alg = HOLogic.mk_Trueprop
   3.122 -          (mk_alg B's (map3 mk_s fs ss mapsBsAs));
   3.123 -        val copy_str_thm = Goal.prove_sorry lthy [] []
   3.124 -          (fold_rev Logic.all (Bs @ ss @ B's @ inv_fs @ fs)
   3.125 -            (Logic.list_implies (all_prems, alg)))
   3.126 -          (K (mk_copy_str_tac set_mapss alg_def alg_set_thms))
   3.127 -          |> Thm.close_derivation;
   3.128 -
   3.129 -        val iso = HOLogic.mk_Trueprop
   3.130 -          (mk_iso B's (map3 mk_s fs ss mapsBsAs) Bs ss inv_fs fs_copy);
   3.131 -        val copy_alg_thm = Goal.prove_sorry lthy [] []
   3.132 -          (fold_rev Logic.all (Bs @ ss @ B's @ inv_fs @ fs)
   3.133 -            (Logic.list_implies (all_prems, iso)))
   3.134 -          (fn {context = ctxt, prems = _} =>
   3.135 -            mk_copy_alg_tac ctxt set_mapss alg_set_thms mor_def iso_alt_thm copy_str_thm)
   3.136 -          |> Thm.close_derivation;
   3.137 -
   3.138 -        val ex = HOLogic.mk_Trueprop
   3.139 -          (list_exists_free s's
   3.140 -            (HOLogic.mk_conj (mk_alg B's s's,
   3.141 -              mk_iso B's s's Bs ss inv_fs fs_copy)));
   3.142 -        val ex_copy_alg_thm = Goal.prove_sorry lthy [] []
   3.143 -          (fold_rev Logic.all (Bs @ ss @ B's @ inv_fs @ fs)
   3.144 -             (Logic.list_implies (prems, ex)))
   3.145 -          (K (mk_ex_copy_alg_tac n copy_str_thm copy_alg_thm))
   3.146 -          |> Thm.close_derivation;
   3.147 -      in
   3.148 -        (copy_alg_thm, ex_copy_alg_thm)
   3.149 -      end;
   3.150 -
   3.151 -    val timer = time (timer "Copy thms");
   3.152 -
   3.153 -
   3.154      (* bounds *)
   3.155  
   3.156      val sum_bd = Library.foldr1 (uncurry mk_csum) bds;
   3.157 @@ -782,10 +676,10 @@
   3.158          Term.list_comb (Const (nth min_algs (i - 1), min_algT), ss)
   3.159        end;
   3.160  
   3.161 +    val min_algs = map (mk_min_alg ss) ks;
   3.162 +
   3.163      val (alg_min_alg_thm, card_of_min_alg_thms, least_min_alg_thms, mor_incl_min_alg_thm) =
   3.164        let
   3.165 -        val min_algs = map (mk_min_alg ss) ks;
   3.166 -
   3.167          val goal = fold_rev Logic.all ss (HOLogic.mk_Trueprop (mk_alg min_algs ss));
   3.168          val alg_min_alg = Goal.prove_sorry lthy [] [] goal
   3.169            (K (mk_alg_min_alg_tac m alg_def min_alg_defs suc_bd_limit_thm sbd_Cinfinite
   3.170 @@ -793,8 +687,7 @@
   3.171            |> Thm.close_derivation;
   3.172  
   3.173          fun mk_card_of_thm min_alg def = Goal.prove_sorry lthy [] []
   3.174 -          (fold_rev Logic.all ss
   3.175 -            (HOLogic.mk_Trueprop (mk_ordLeq (mk_card_of min_alg) Asuc_bd)))
   3.176 +          (HOLogic.mk_Trueprop (mk_ordLeq (mk_card_of min_alg) Asuc_bd))
   3.177            (K (mk_card_of_min_alg_tac def card_of_min_algs_thm
   3.178              suc_bd_Card_order suc_bd_Asuc_bd Asuc_bd_Cinfinite))
   3.179            |> Thm.close_derivation;
   3.180 @@ -809,11 +702,10 @@
   3.181          val leasts = map3 mk_least_thm min_algs Bs min_alg_defs;
   3.182  
   3.183          val incl_prem = HOLogic.mk_Trueprop (mk_alg Bs ss);
   3.184 -        val incl_min_algs = map (mk_min_alg ss) ks;
   3.185          val incl = Goal.prove_sorry lthy [] []
   3.186            (fold_rev Logic.all (Bs @ ss)
   3.187              (Logic.mk_implies (incl_prem,
   3.188 -              HOLogic.mk_Trueprop (mk_mor incl_min_algs ss Bs ss active_ids))))
   3.189 +              HOLogic.mk_Trueprop (mk_mor min_algs ss Bs ss active_ids))))
   3.190            (K (EVERY' (rtac mor_incl_thm :: map etac leasts) 1))
   3.191            |> Thm.close_derivation;
   3.192        in
   3.193 @@ -904,33 +796,22 @@
   3.194  
   3.195      val mor_select_thm =
   3.196        let
   3.197 -        val alg_prem = HOLogic.mk_Trueprop (mk_alg Bs ss);
   3.198          val i_prem = HOLogic.mk_Trueprop (HOLogic.mk_mem (iidx, II));
   3.199 -        val mor_prem = HOLogic.mk_Trueprop (mk_mor select_Bs select_ss Bs ss Asuc_fs);
   3.200 -        val prems = [alg_prem, i_prem, mor_prem];
   3.201 +        val mor_prem = HOLogic.mk_Trueprop (mk_mor select_Bs select_ss active_UNIVs ss Asuc_fs);
   3.202 +        val prems = [i_prem, mor_prem];
   3.203          val concl = HOLogic.mk_Trueprop
   3.204 -          (mk_mor car_inits str_inits Bs ss
   3.205 +          (mk_mor car_inits str_inits active_UNIVs ss
   3.206              (map (fn f => HOLogic.mk_comp (f, mk_rapp iidx Asuc_bdT)) Asuc_fs));
   3.207        in
   3.208          Goal.prove_sorry lthy [] []
   3.209 -          (fold_rev Logic.all (iidx :: Bs @ ss @ Asuc_fs) (Logic.list_implies (prems, concl)))
   3.210 +          (fold_rev Logic.all (iidx :: ss @ Asuc_fs) (Logic.list_implies (prems, concl)))
   3.211            (K (mk_mor_select_tac mor_def mor_cong_thm mor_comp_thm mor_incl_min_alg_thm alg_def
   3.212              alg_select_thm alg_set_thms set_mapss str_init_defs))
   3.213          |> Thm.close_derivation
   3.214        end;
   3.215  
   3.216 -    val (init_ex_mor_thm, init_unique_mor_thms) =
   3.217 +    val init_unique_mor_thms =
   3.218        let
   3.219 -        val prem = HOLogic.mk_Trueprop (mk_alg Bs ss);
   3.220 -        val concl = HOLogic.mk_Trueprop
   3.221 -          (list_exists_free init_fs (mk_mor car_inits str_inits Bs ss init_fs));
   3.222 -        val ex_mor = Goal.prove_sorry lthy [] []
   3.223 -          (fold_rev Logic.all (Bs @ ss) (Logic.mk_implies (prem, concl)))
   3.224 -          (fn {context = ctxt, prems = _} => mk_init_ex_mor_tac ctxt Abs_IIT_inverse_thm
   3.225 -            ex_copy_alg_thm alg_min_alg_thm card_of_min_alg_thms mor_comp_thm mor_select_thm
   3.226 -            mor_incl_min_alg_thm)
   3.227 -          |> Thm.close_derivation;
   3.228 -
   3.229          val prems = map2 (HOLogic.mk_Trueprop oo curry HOLogic.mk_mem) init_xs car_inits
   3.230          val mor_prems = map HOLogic.mk_Trueprop
   3.231            [mk_mor car_inits str_inits Bs ss init_fs,
   3.232 @@ -945,7 +826,7 @@
   3.233              in_mono'_thms alg_set_thms morE_thms map_cong0s))
   3.234            |> Thm.close_derivation;
   3.235        in
   3.236 -        (ex_mor, split_conj_thm unique_mor)
   3.237 +        split_conj_thm unique_mor
   3.238        end;
   3.239  
   3.240      val init_setss = mk_setss (passiveAs @ active_initTs);
   3.241 @@ -997,20 +878,9 @@
   3.242  
   3.243      val type_defs = map #type_definition T_loc_infos;
   3.244      val Reps = map #Rep T_loc_infos;
   3.245 -    val Rep_casess = map #Rep_cases T_loc_infos;
   3.246 -    val Rep_injects = map #Rep_inject T_loc_infos;
   3.247      val Rep_inverses = map #Rep_inverse T_loc_infos;
   3.248      val Abs_inverses = map #Abs_inverse T_loc_infos;
   3.249  
   3.250 -    fun mk_inver_thm mk_tac rep abs X thm =
   3.251 -      Goal.prove_sorry lthy [] []
   3.252 -        (HOLogic.mk_Trueprop (mk_inver rep abs X))
   3.253 -        (K (EVERY' [rtac iffD2, rtac @{thm inver_def}, rtac ballI, mk_tac thm] 1))
   3.254 -      |> Thm.close_derivation;
   3.255 -
   3.256 -    val inver_Reps = map4 (mk_inver_thm rtac) Abs_Ts Rep_Ts (map HOLogic.mk_UNIV Ts) Rep_inverses;
   3.257 -    val inver_Abss = map4 (mk_inver_thm etac) Rep_Ts Abs_Ts car_inits Abs_inverses;
   3.258 -
   3.259      val timer = time (timer "THE TYPEDEFs & Rep/Abs thms");
   3.260  
   3.261      val UNIVs = map HOLogic.mk_UNIV Ts;
   3.262 @@ -1071,21 +941,23 @@
   3.263  
   3.264      val (mor_Rep_thm, mor_Abs_thm) =
   3.265        let
   3.266 -        val copy = alg_init_thm RS copy_alg_thm;
   3.267 -        fun mk_bij inj Rep cases = @{thm bij_betwI'} OF [inj, Rep, cases];
   3.268 -        val bijs = map3 mk_bij Rep_injects Reps Rep_casess;
   3.269 +        val defs = mor_def :: ctor_defs;
   3.270 +
   3.271          val mor_Rep =
   3.272            Goal.prove_sorry lthy [] []
   3.273              (HOLogic.mk_Trueprop (mk_mor UNIVs ctors car_inits str_inits Rep_Ts))
   3.274 -            (fn {context = ctxt, prems = _} => mk_mor_Rep_tac ctxt ctor_defs copy bijs inver_Abss
   3.275 -              inver_Reps)
   3.276 +            (fn {context = ctxt, prems = _} => mk_mor_Rep_tac ctxt m defs Reps Abs_inverses
   3.277 +              alg_min_alg_thm alg_set_thms set_mapss)
   3.278            |> Thm.close_derivation;
   3.279  
   3.280 -        val inv = mor_inv_thm OF [mor_Rep, talg_thm, alg_init_thm];
   3.281 +        fun mk_ct initFT str abs = Term.absdummy initFT (abs $ (str $ Bound 0))
   3.282 +        val cts = map3 (SOME o certify lthy ooo mk_ct) init_FTs str_inits Abs_Ts;
   3.283 +
   3.284          val mor_Abs =
   3.285            Goal.prove_sorry lthy [] []
   3.286              (HOLogic.mk_Trueprop (mk_mor car_inits str_inits UNIVs ctors Abs_Ts))
   3.287 -            (K (mk_mor_Abs_tac inv inver_Abss inver_Reps))
   3.288 +            (fn {context = ctxt, prems = _} => mk_mor_Abs_tac ctxt cts defs Abs_inverses
   3.289 +              map_comp_id_thms map_cong0L_thms)
   3.290            |> Thm.close_derivation;
   3.291        in
   3.292          (mor_Rep, mor_Abs)
   3.293 @@ -1122,18 +994,44 @@
   3.294      val fold_defs = map (fn def =>
   3.295        mk_unabs_def n (Morphism.thm phi def RS meta_eq_to_obj_eq)) fold_def_frees;
   3.296  
   3.297 +    (* algebra copies *)
   3.298 +
   3.299 +    val copy_thm =
   3.300 +      let
   3.301 +        val prems = HOLogic.mk_Trueprop (mk_alg Bs ss) ::
   3.302 +          map3 (HOLogic.mk_Trueprop ooo mk_bij_betw) inv_fs B's Bs;
   3.303 +        val concl = HOLogic.mk_Trueprop (list_exists_free s's
   3.304 +          (HOLogic.mk_conj (mk_alg B's s's, mk_mor B's s's Bs ss inv_fs)));
   3.305 +      in
   3.306 +        Goal.prove_sorry lthy [] []
   3.307 +          (fold_rev Logic.all (Bs @ ss @ B's @ inv_fs) (Logic.list_implies (prems, concl)))
   3.308 +          (K (mk_copy_tac m alg_def mor_def alg_set_thms set_mapss))
   3.309 +          |> Thm.close_derivation
   3.310 +      end;
   3.311 +
   3.312 +    val init_ex_mor_thm =
   3.313 +      let
   3.314 +        val goal = HOLogic.mk_Trueprop
   3.315 +          (list_exists_free fs (mk_mor UNIVs ctors active_UNIVs ss fs));
   3.316 +      in
   3.317 +        singleton (Proof_Context.export names_lthy lthy)
   3.318 +          (Goal.prove_sorry lthy [] [] goal
   3.319 +            (fn {context = ctxt, prems = _} =>
   3.320 +              mk_init_ex_mor_tac ctxt Abs_IIT_inverse_thm (alg_min_alg_thm RS copy_thm)
   3.321 +                card_of_min_alg_thms mor_Rep_thm mor_comp_thm mor_select_thm mor_incl_thm)
   3.322 +            |> Thm.close_derivation)
   3.323 +      end;
   3.324 +
   3.325      val mor_fold_thm =
   3.326        let
   3.327 -        val ex_mor = talg_thm RS init_ex_mor_thm;
   3.328          val mor_cong = mor_cong_thm OF (map (mk_nth_conv n) ks);
   3.329 -        val mor_comp = mor_Rep_thm RS mor_comp_thm;
   3.330          val cT = certifyT lthy foldT;
   3.331          val ct = certify lthy fold_fun
   3.332        in
   3.333          singleton (Proof_Context.export names_lthy lthy)
   3.334            (Goal.prove_sorry lthy [] []
   3.335              (HOLogic.mk_Trueprop (mk_mor UNIVs ctors active_UNIVs ss (map (mk_fold Ts ss) ks)))
   3.336 -            (K (mk_mor_fold_tac cT ct fold_defs ex_mor (mor_comp RS mor_cong))))
   3.337 +            (K (mk_mor_fold_tac cT ct fold_defs init_ex_mor_thm mor_cong)))
   3.338          |> Thm.close_derivation
   3.339        end;
   3.340  
     4.1 --- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Thu Mar 20 23:38:34 2014 +0100
     4.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Fri Mar 21 08:13:23 2014 +0100
     4.3 @@ -16,8 +16,7 @@
     4.4    val mk_bd_card_order_tac: thm list -> tactic
     4.5    val mk_bd_limit_tac: int -> thm -> tactic
     4.6    val mk_card_of_min_alg_tac: thm -> thm -> thm -> thm -> thm -> tactic
     4.7 -  val mk_copy_alg_tac: Proof.context -> thm list list -> thm list -> thm -> thm -> thm -> tactic
     4.8 -  val mk_copy_str_tac: thm list list -> thm -> thm list -> tactic
     4.9 +  val mk_copy_tac: int -> thm -> thm -> thm list -> thm list list -> tactic
    4.10    val mk_ctor_induct_tac: Proof.context -> int -> thm list list -> thm -> thm list -> thm ->
    4.11      thm list -> thm list -> thm list -> tactic
    4.12    val mk_ctor_induct2_tac: Proof.context -> ctyp option list -> cterm option list -> thm ->
    4.13 @@ -26,13 +25,11 @@
    4.14    val mk_ctor_rel_tac: Proof.context -> thm list -> int -> thm -> thm -> thm -> thm -> thm list ->
    4.15      thm -> thm -> thm list -> thm list -> thm list list -> tactic
    4.16    val mk_dtor_o_ctor_tac: thm -> thm -> thm -> thm -> thm list -> tactic
    4.17 -  val mk_ex_copy_alg_tac: int -> thm -> thm -> tactic
    4.18 -  val mk_init_ex_mor_tac: Proof.context -> thm -> thm -> thm -> thm list -> thm -> thm -> thm ->
    4.19 +  val mk_init_ex_mor_tac: Proof.context -> thm -> thm -> thm list -> thm -> thm -> thm -> thm ->
    4.20      tactic
    4.21    val mk_init_induct_tac: int -> thm -> thm -> thm list -> thm list -> tactic
    4.22    val mk_init_unique_mor_tac: int -> thm -> thm -> thm list -> thm list -> thm list -> thm list ->
    4.23      thm list -> tactic
    4.24 -  val mk_iso_alt_tac: thm list -> thm -> tactic
    4.25    val mk_fold_unique_mor_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> tactic
    4.26    val mk_fold_transfer_tac: Proof.context -> int -> thm -> thm list -> thm list -> tactic
    4.27    val mk_least_min_alg_tac: thm -> thm -> tactic
    4.28 @@ -49,14 +46,15 @@
    4.29    val mk_min_algs_least_tac: ctyp -> cterm -> thm -> thm list -> thm list -> tactic
    4.30    val mk_min_algs_mono_tac: Proof.context -> thm -> tactic
    4.31    val mk_min_algs_tac: thm -> thm list -> tactic
    4.32 -  val mk_mor_Abs_tac: thm -> thm list -> thm list -> tactic
    4.33 -  val mk_mor_Rep_tac: Proof.context -> thm list -> thm -> thm list -> thm list -> thm list -> tactic
    4.34 +  val mk_mor_Abs_tac: Proof.context -> cterm option list -> thm list -> thm list -> thm list ->
    4.35 +    thm list -> tactic
    4.36 +  val mk_mor_Rep_tac: Proof.context -> int -> thm list -> thm list -> thm list -> thm -> thm list ->
    4.37 +    thm list list -> tactic
    4.38    val mk_mor_UNIV_tac: int -> thm list -> thm -> tactic
    4.39    val mk_mor_comp_tac: thm -> thm list list -> thm list -> tactic
    4.40    val mk_mor_convol_tac: 'a list -> thm -> tactic
    4.41    val mk_mor_elim_tac: thm -> tactic
    4.42    val mk_mor_incl_tac: thm -> thm list -> tactic
    4.43 -  val mk_mor_inv_tac: thm -> thm -> thm list list -> thm list -> thm list -> thm list -> tactic
    4.44    val mk_mor_fold_tac: ctyp -> cterm -> thm list -> thm -> thm -> tactic
    4.45    val mk_mor_select_tac: thm -> thm -> thm -> thm -> thm -> thm -> thm list -> thm list list ->
    4.46      thm list -> tactic
    4.47 @@ -138,32 +136,6 @@
    4.48      CONJ_WRAP' mor_tac (set_maps ~~ map_comp_ids)) 1
    4.49    end;
    4.50  
    4.51 -fun mk_mor_inv_tac alg_def mor_def set_maps morEs map_comp_ids map_cong0Ls =
    4.52 -  let
    4.53 -    val fbetw_tac = EVERY' [rtac ballI, etac set_mp, etac imageI];
    4.54 -    fun Collect_tac set_map =
    4.55 -      CONJ_WRAP' (fn thm =>
    4.56 -        FIRST' [rtac subset_UNIV,
    4.57 -          (EVERY' [rtac ord_eq_le_trans, rtac thm, rtac subset_trans,
    4.58 -            etac @{thm image_mono}, atac])]) set_map;
    4.59 -    fun mor_tac (set_map, ((morE, map_comp_id), map_cong0L)) =
    4.60 -      EVERY' [rtac ballI, ftac rev_bspec, atac,
    4.61 -         REPEAT o eresolve_tac [CollectE, conjE], rtac sym, rtac trans, rtac sym,
    4.62 -         etac @{thm inverE}, etac bspec, rtac CollectI, Collect_tac set_map,
    4.63 -         rtac trans, etac (morE RS arg_cong), rtac CollectI, Collect_tac set_map,
    4.64 -         rtac trans, rtac (map_comp_id RS arg_cong), rtac (map_cong0L RS arg_cong),
    4.65 -         REPEAT_DETERM_N (length morEs) o
    4.66 -           (EVERY' [rtac iffD1, rtac @{thm inver_pointfree}, etac @{thm inver_mono}, atac])];
    4.67 -  in
    4.68 -    (rtac (mor_def RS iffD2) THEN'
    4.69 -    dtac (alg_def RS iffD1) THEN'
    4.70 -    dtac (alg_def RS iffD1) THEN'
    4.71 -    REPEAT o etac conjE THEN'
    4.72 -    rtac conjI THEN'
    4.73 -    CONJ_WRAP' (K fbetw_tac) set_maps THEN'
    4.74 -    CONJ_WRAP' mor_tac (set_maps ~~ (morEs ~~ map_comp_ids ~~ map_cong0Ls))) 1
    4.75 -  end;
    4.76 -
    4.77  fun mk_mor_str_tac ks mor_def =
    4.78    (rtac (mor_def RS iffD2) THEN' rtac conjI THEN'
    4.79    CONJ_WRAP' (K (EVERY' [rtac ballI, rtac UNIV_I])) ks THEN'
    4.80 @@ -188,74 +160,30 @@
    4.81        etac (o_apply RS sym RS trans), rtac o_apply])) morEs] 1
    4.82    end;
    4.83  
    4.84 -fun mk_iso_alt_tac mor_images mor_inv =
    4.85 -  let
    4.86 -    val n = length mor_images;
    4.87 -    fun if_wrap_tac thm =
    4.88 -      EVERY' [rtac iffD2, rtac @{thm bij_betw_iff_ex}, rtac exI, rtac conjI,
    4.89 -        rtac @{thm inver_surj}, etac thm, etac thm, atac, etac conjI, atac]
    4.90 -    val if_tac =
    4.91 -      EVERY' [etac thin_rl, etac thin_rl, REPEAT o eresolve_tac [conjE, exE],
    4.92 -        rtac conjI, atac, CONJ_WRAP' if_wrap_tac mor_images];
    4.93 -    val only_if_tac =
    4.94 -      EVERY' [rtac conjI, etac conjunct1, EVERY' (map (fn thm =>
    4.95 -        EVERY' [rtac exE, rtac @{thm bij_betw_ex_weakE}, etac (conjunct2 RS thm)])
    4.96 -        (map (mk_conjunctN n) (1 upto n))), REPEAT o rtac exI, rtac conjI, rtac mor_inv,
    4.97 -        etac conjunct1, atac, atac, REPEAT_DETERM_N n o atac,
    4.98 -        CONJ_WRAP' (K (etac conjunct2)) mor_images];
    4.99 -  in
   4.100 -    (rtac iffI THEN' if_tac THEN' only_if_tac) 1
   4.101 -  end;
   4.102 -
   4.103 -fun mk_copy_str_tac set_maps alg_def alg_sets =
   4.104 +fun mk_copy_tac m alg_def mor_def alg_sets set_mapss =
   4.105    let
   4.106      val n = length alg_sets;
   4.107 -    val bij_betw_inv_tac =
   4.108 -      EVERY' [etac thin_rl, REPEAT_DETERM_N n o EVERY' [dtac @{thm bij_betwI}, atac, atac],
   4.109 -        REPEAT_DETERM_N (2 * n) o etac thin_rl, REPEAT_DETERM_N (n - 1) o etac conjI, atac];
   4.110 -    fun set_tac thms =
   4.111 -      EVERY' [rtac ord_eq_le_trans, resolve_tac thms, rtac subset_trans,
   4.112 -          etac @{thm image_mono}, rtac equalityD1, etac @{thm bij_betw_imageE}];
   4.113 -    val copy_str_tac =
   4.114 -      CONJ_WRAP' (fn (thms, thm) =>
   4.115 +    fun set_tac thm =
   4.116 +      EVERY' [rtac ord_eq_le_trans, rtac thm, rtac subset_trans, etac @{thm image_mono},
   4.117 +        rtac equalityD1, etac @{thm bij_betw_imageE}];
   4.118 +    val alg_tac =
   4.119 +      CONJ_WRAP' (fn (set_maps, alg_set) =>
   4.120          EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac set_mp,
   4.121 -          rtac equalityD1, etac @{thm bij_betw_imageE},
   4.122 -          REPEAT_DETERM_N 2 o rtac @{thm ssubst_mem[OF o_apply]}, rtac imageI, etac thm,
   4.123 -          REPEAT_DETERM_N n o set_tac thms])
   4.124 -      (set_maps ~~ alg_sets);
   4.125 -  in
   4.126 -    (rtac rev_mp THEN' DETERM o bij_betw_inv_tac THEN' rtac impI THEN'
   4.127 -    rtac (alg_def RS iffD2) THEN' copy_str_tac) 1
   4.128 -  end;
   4.129 +          rtac equalityD1, etac @{thm bij_betw_imageE[OF bij_betw_the_inv_into]},
   4.130 +          rtac imageI, etac alg_set, EVERY' (map set_tac (drop m set_maps))])
   4.131 +      (set_mapss ~~ alg_sets);
   4.132  
   4.133 -fun mk_copy_alg_tac ctxt set_maps alg_sets mor_def iso_alt copy_str =
   4.134 -  let
   4.135 -    val n = length alg_sets;
   4.136 -    val fbetw_tac = CONJ_WRAP' (K (etac @{thm bij_betwE})) alg_sets;
   4.137 -    fun set_tac thms =
   4.138 -      EVERY' [rtac ord_eq_le_trans, resolve_tac thms, rtac subset_trans,
   4.139 -        REPEAT_DETERM o etac conjE, etac @{thm image_mono},
   4.140 -        rtac equalityD1, etac @{thm bij_betw_imageE}];
   4.141 -    val mor_tac =
   4.142 -      CONJ_WRAP' (fn (thms, thm) =>
   4.143 -        EVERY' [rtac ballI, etac CollectE, SELECT_GOAL (unfold_thms_tac ctxt [o_apply]),
   4.144 -          etac @{thm inverE}, etac thm, REPEAT_DETERM_N n o set_tac thms])
   4.145 -      (set_maps ~~ alg_sets);
   4.146 +    val mor_tac = rtac conjI THEN' CONJ_WRAP' (K (etac @{thm bij_betwE})) alg_sets THEN'
   4.147 +      CONJ_WRAP' (fn (set_maps, alg_set) =>
   4.148 +        EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, conjE],
   4.149 +          etac @{thm f_the_inv_into_f_bij_betw}, etac alg_set,
   4.150 +          EVERY' (map set_tac (drop m set_maps))])
   4.151 +      (set_mapss ~~ alg_sets);
   4.152    in
   4.153 -    (rtac (iso_alt RS iffD2) THEN' etac copy_str THEN' REPEAT_DETERM o atac THEN'
   4.154 -    rtac conjI THEN' rtac (mor_def RS iffD2) THEN' rtac conjI THEN' fbetw_tac THEN' mor_tac THEN'
   4.155 -    CONJ_WRAP' (K atac) alg_sets) 1
   4.156 +    (REPEAT_DETERM_N n o rtac exI THEN' rtac conjI THEN'
   4.157 +    rtac (alg_def RS iffD2) THEN' alg_tac THEN' rtac (mor_def RS iffD2) THEN' mor_tac) 1
   4.158    end;
   4.159  
   4.160 -fun mk_ex_copy_alg_tac n copy_str copy_alg =
   4.161 -  EVERY' [REPEAT_DETERM_N n o rtac exI, rtac conjI, etac copy_str,
   4.162 -    REPEAT_DETERM_N n o atac,
   4.163 -    REPEAT_DETERM_N n o etac @{thm bij_betw_inver2},
   4.164 -    REPEAT_DETERM_N n o etac @{thm bij_betw_inver1}, etac copy_alg,
   4.165 -    REPEAT_DETERM_N n o atac,
   4.166 -    REPEAT_DETERM_N n o etac @{thm bij_betw_inver2},
   4.167 -    REPEAT_DETERM_N n o etac @{thm bij_betw_inver1}] 1;
   4.168 -
   4.169  fun mk_bd_limit_tac n bd_Cinfinite =
   4.170    EVERY' [REPEAT_DETERM o etac conjE, rtac rev_mp, rtac @{thm Cinfinite_limit_finite},
   4.171      REPEAT_DETERM_N n o rtac @{thm finite.insertI}, rtac @{thm finite.emptyI},
   4.172 @@ -408,30 +336,17 @@
   4.173        rtac (alg_def RS iffD2), CONJ_WRAP' alg_epi_tac ((alg_sets ~~ str_init_defs) ~~ set_maps)] 1
   4.174    end;
   4.175  
   4.176 -fun mk_init_ex_mor_tac ctxt Abs_inverse copy_alg_ex alg_min_alg card_of_min_algs
   4.177 -    mor_comp mor_select mor_incl_min_alg =
   4.178 +fun mk_init_ex_mor_tac ctxt Abs_inverse copy card_of_min_algs mor_Rep mor_comp mor_select mor_incl =
   4.179    let
   4.180      val n = length card_of_min_algs;
   4.181 -    val card_of_ordIso_tac = EVERY' [rtac iffD2, rtac @{thm card_of_ordIso},
   4.182 -      rtac @{thm ordIso_symmetric}, rtac conjunct1, rtac conjunct2, atac];
   4.183 -    fun internalize_tac card_of = EVERY' [rtac iffD1, rtac @{thm internalize_card_of_ordLeq2},
   4.184 -      rtac @{thm ordLeq_ordIso_trans}, rtac card_of, rtac iffD1,
   4.185 -      rtac @{thm Card_order_iff_ordIso_card_of}, rtac @{thm Card_order_cexp}];
   4.186    in
   4.187 -    (rtac rev_mp THEN'
   4.188 -    REPEAT_DETERM_N (2 * n) o (rtac mp THEN' rtac @{thm ex_mono} THEN' rtac impI) THEN'
   4.189 -    REPEAT_DETERM_N (n + 1) o etac thin_rl THEN' rtac (alg_min_alg RS copy_alg_ex) THEN'
   4.190 -    REPEAT_DETERM_N n o atac THEN'
   4.191 -    REPEAT_DETERM_N n o card_of_ordIso_tac THEN'
   4.192 -    EVERY' (map internalize_tac card_of_min_algs) THEN'
   4.193 -    rtac impI THEN'
   4.194 -    REPEAT_DETERM o eresolve_tac [exE, conjE] THEN'
   4.195 -    REPEAT_DETERM o rtac exI THEN'
   4.196 -    rtac mor_select THEN' atac THEN' rtac CollectI THEN'
   4.197 -    REPEAT_DETERM o rtac exI THEN'
   4.198 -    rtac conjI THEN' rtac refl THEN' atac THEN'
   4.199 -    K (unfold_thms_tac ctxt (Abs_inverse :: fst_snd_convs)) THEN'
   4.200 -    etac mor_comp THEN' etac mor_incl_min_alg) 1
   4.201 +    EVERY' [Method.insert_tac (map (fn thm => thm RS @{thm ex_bij_betw}) card_of_min_algs),
   4.202 +      REPEAT_DETERM o etac exE, rtac rev_mp, rtac copy, REPEAT_DETERM_N n o atac,
   4.203 +      rtac impI, REPEAT_DETERM o eresolve_tac [exE, conjE], REPEAT_DETERM_N n o rtac exI,
   4.204 +      rtac mor_comp, rtac mor_Rep, rtac mor_select, rtac CollectI, REPEAT_DETERM o rtac exI,
   4.205 +      rtac conjI, rtac refl, atac,
   4.206 +      SELECT_GOAL (unfold_thms_tac ctxt (Abs_inverse :: fst_snd_convs)),
   4.207 +      etac mor_comp, rtac mor_incl, REPEAT_DETERM_N n o rtac subset_UNIV] 1
   4.208    end;
   4.209  
   4.210  fun mk_init_unique_mor_tac m
   4.211 @@ -482,17 +397,28 @@
   4.212      CONJ_WRAP' mk_induct_tac least_min_algs 1
   4.213    end;
   4.214  
   4.215 -fun mk_mor_Rep_tac ctxt ctor_defs copy bijs inver_Abss inver_Reps =
   4.216 -  (K (unfold_thms_tac ctxt ctor_defs) THEN' rtac conjunct1 THEN' rtac copy THEN'
   4.217 -  EVERY' (map (fn bij => EVERY' [rtac bij, atac, etac bexI, rtac UNIV_I]) bijs) THEN'
   4.218 -  EVERY' (map rtac inver_Abss) THEN'
   4.219 -  EVERY' (map rtac inver_Reps)) 1;
   4.220 +fun mk_mor_Rep_tac ctxt m defs Reps Abs_inverses alg_min_alg alg_sets set_mapss =
   4.221 +  unfold_thms_tac ctxt (@{thm o_apply} :: defs) THEN
   4.222 +  EVERY' [rtac conjI,
   4.223 +    CONJ_WRAP' (fn thm => rtac ballI THEN' rtac thm) Reps,
   4.224 +    CONJ_WRAP' (fn (Abs_inverse, (set_maps, alg_set)) =>
   4.225 +      EVERY' [rtac ballI, rtac Abs_inverse, rtac (alg_min_alg RS alg_set),
   4.226 +        EVERY' (map2 (fn Rep => fn set_map =>
   4.227 +          EVERY' [rtac (set_map RS ord_eq_le_trans), rtac @{thm image_subsetI}, rtac Rep])
   4.228 +        Reps (drop m set_maps))])
   4.229 +    (Abs_inverses ~~ (set_mapss ~~ alg_sets))] 1;
   4.230  
   4.231 -fun mk_mor_Abs_tac inv inver_Abss inver_Reps =
   4.232 -  (rtac inv THEN'
   4.233 -  EVERY' (map2 (fn inver_Abs => fn inver_Rep =>
   4.234 -    EVERY' [rtac conjI, rtac subset_UNIV, rtac conjI, rtac inver_Rep, rtac inver_Abs])
   4.235 -    inver_Abss inver_Reps)) 1;
   4.236 +fun mk_mor_Abs_tac ctxt cts defs Abs_inverses map_comp_ids map_congLs =
   4.237 +  unfold_thms_tac ctxt (@{thm o_apply} :: defs) THEN
   4.238 +  EVERY' [rtac conjI,
   4.239 +    CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) Abs_inverses,
   4.240 +    CONJ_WRAP' (fn (ct, thm) =>
   4.241 +      EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, conjE],
   4.242 +        rtac (thm RS (cterm_instantiate_pos [NONE, NONE, ct] arg_cong) RS sym),
   4.243 +        EVERY' (map (fn Abs_inverse =>
   4.244 +          EVERY' [rtac (o_apply RS trans RS ballI), etac (set_mp RS Abs_inverse), atac])
   4.245 +        Abs_inverses)])
   4.246 +    (cts ~~ map2 mk_trans map_comp_ids map_congLs)] 1;;
   4.247  
   4.248  fun mk_mor_fold_tac cT ct fold_defs ex_mor mor =
   4.249    (EVERY' (map stac fold_defs) THEN' EVERY' [rtac rev_mp, rtac ex_mor, rtac impI] THEN'
     5.1 --- a/src/HOL/Tools/BNF/bnf_lfp_util.ML	Thu Mar 20 23:38:34 2014 +0100
     5.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_util.ML	Fri Mar 21 08:13:23 2014 +0100
     5.3 @@ -12,7 +12,6 @@
     5.4  
     5.5    val mk_bij_betw: term -> term -> term -> term
     5.6    val mk_cardSuc: term -> term
     5.7 -  val mk_inver: term -> term -> term -> term
     5.8    val mk_not_empty: term -> term
     5.9    val mk_not_eq: term -> term -> term
    5.10    val mk_rapp: term -> typ -> term
    5.11 @@ -52,10 +51,6 @@
    5.12   Const (@{const_name bij_betw},
    5.13     fastype_of f --> fastype_of A --> fastype_of B --> HOLogic.boolT) $ f $ A $ B;
    5.14  
    5.15 -fun mk_inver f g A =
    5.16 - Const (@{const_name inver}, fastype_of f --> fastype_of g --> fastype_of A --> HOLogic.boolT) $
    5.17 -   f $ g $ A;
    5.18 -
    5.19  fun mk_not_eq x y = HOLogic.mk_not (HOLogic.mk_eq (x, y));
    5.20  
    5.21  fun mk_not_empty B = mk_not_eq B (HOLogic.mk_set (HOLogic.dest_setT (fastype_of B)) []);