continued changing type of corec type
authorblanchet
Tue Oct 02 01:00:18 2012 +0200 (2012-10-02)
changeset 4968378a3d5006cf1
parent 49682 f57af1c46f99
child 49684 1cf810b8f600
continued changing type of corec type
src/HOL/BNF/BNF_FP.thy
src/HOL/BNF/Examples/Infinite_Derivation_Trees/Tree.thy
src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML
     1.1 --- a/src/HOL/BNF/BNF_FP.thy	Tue Oct 02 01:00:18 2012 +0200
     1.2 +++ b/src/HOL/BNF/BNF_FP.thy	Tue Oct 02 01:00:18 2012 +0200
     1.3 @@ -47,11 +47,11 @@
     1.4  lemma Un_cong: "\<lbrakk>A = B; C = D\<rbrakk> \<Longrightarrow> A \<union> C = B \<union> D"
     1.5  by simp
     1.6  
     1.7 -lemma pointfree_idE: "f o g = id \<Longrightarrow> f (g x) = x"
     1.8 +lemma pointfree_idE: "f \<circ> g = id \<Longrightarrow> f (g x) = x"
     1.9  unfolding o_def fun_eq_iff by simp
    1.10  
    1.11  lemma o_bij:
    1.12 -  assumes gf: "g o f = id" and fg: "f o g = id"
    1.13 +  assumes gf: "g \<circ> f = id" and fg: "f \<circ> g = id"
    1.14    shows "bij f"
    1.15  unfolding bij_def inj_on_def surj_def proof safe
    1.16    fix a1 a2 assume "f a1 = f a2"
    1.17 @@ -67,8 +67,8 @@
    1.18  lemma ssubst_mem: "\<lbrakk>t = s; s \<in> X\<rbrakk> \<Longrightarrow> t \<in> X" by simp
    1.19  
    1.20  lemma sum_case_step:
    1.21 -  "sum_case (sum_case f' g') g (Inl p) = sum_case f' g' p"
    1.22 -  "sum_case f (sum_case f' g') (Inr p) = sum_case f' g' p"
    1.23 +"sum_case (sum_case f' g') g (Inl p) = sum_case f' g' p"
    1.24 +"sum_case f (sum_case f' g') (Inr p) = sum_case f' g' p"
    1.25  by auto
    1.26  
    1.27  lemma one_pointE: "\<lbrakk>\<And>x. s = x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
    1.28 @@ -100,6 +100,14 @@
    1.29  "sum_case f g (if p then Inl x else Inr y) = (if p then f x else g y)"
    1.30  by simp
    1.31  
    1.32 +lemma sum_case_o_inj:
    1.33 +"sum_case f g \<circ> Inl = f"
    1.34 +"sum_case f g \<circ> Inr = g"
    1.35 +by auto
    1.36 +
    1.37 +lemma ident_o_ident: "(\<lambda>x. x) \<circ> (\<lambda>x. x) = (\<lambda>x. x)"
    1.38 +by (rule o_def)
    1.39 +
    1.40  lemma mem_UN_compreh_eq: "(z : \<Union>{y. \<exists>x\<in>A. y = F x}) = (\<exists>x\<in>A. z : F x)"
    1.41  by blast
    1.42  
     2.1 --- a/src/HOL/BNF/Examples/Infinite_Derivation_Trees/Tree.thy	Tue Oct 02 01:00:18 2012 +0200
     2.2 +++ b/src/HOL/BNF/Examples/Infinite_Derivation_Trees/Tree.thy	Tue Oct 02 01:00:18 2012 +0200
     2.3 @@ -69,7 +69,7 @@
     2.4  definition "Node n as \<equiv> NNode n (the_inv fset as)"
     2.5  definition "cont \<equiv> fset o ccont"
     2.6  definition "unfold rt ct \<equiv> Tree_unfold rt (the_inv fset o ct)"
     2.7 -definition "corec rt ct \<equiv> Tree_corec rt (the_inv fset o ct)"
     2.8 +definition "corec rt qt ct dt \<equiv> Tree_corec rt qt (the_inv fset o ct) (the_inv fset o dt)"
     2.9  
    2.10  definition lift ("_ ^#" 200) where
    2.11  "lift \<phi> as \<longleftrightarrow> (\<forall> tr. Inr tr \<in> as \<longrightarrow> \<phi> tr)"
    2.12 @@ -179,9 +179,11 @@
    2.13  by (metis (no_types) fset_to_fset map_fset_image)
    2.14  
    2.15  theorem corec:
    2.16 -"root (corec rt ct b) = rt b"
    2.17 -"finite (ct b) \<Longrightarrow> cont (corec rt ct b) = image (id \<oplus> ([[id, corec rt ct]])) (ct b)"
    2.18 -using Tree.sel_corec[of rt "the_inv fset \<circ> ct" b] unfolding corec_def
    2.19 +"root (corec rt qt ct dt b) = rt b"
    2.20 +"\<lbrakk>finite (ct b); finite (dt b)\<rbrakk> \<Longrightarrow>
    2.21 + cont (corec rt qt ct dt b) =
    2.22 + (if qt b then ct b else image (id \<oplus> corec rt qt ct dt) (dt b))"
    2.23 +using Tree.sel_corec[of rt qt "the_inv fset \<circ> ct" "the_inv fset \<circ> dt" b] unfolding corec_def
    2.24  apply -
    2.25  apply simp
    2.26  unfolding cont_def comp_def id_def
     3.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue Oct 02 01:00:18 2012 +0200
     3.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue Oct 02 01:00:18 2012 +0200
     3.3 @@ -113,11 +113,6 @@
     3.4      Type (_, Ts) => map (not o member (op =) (deads_of_bnf bnf)) Ts
     3.5    | _ => replicate n false);
     3.6  
     3.7 -fun tack z_name (c, u) f =
     3.8 -  let val z = Free (z_name, mk_sumT (fastype_of u, fastype_of c)) in
     3.9 -    Term.lambda z (mk_sum_case (Term.lambda u u, Term.lambda c (f $ c)) $ z)
    3.10 -  end;
    3.11 -
    3.12  fun cannot_merge_types () = error "Mutually recursive types must have the same type parameters";
    3.13  
    3.14  fun merge_type_arg T T' = if T = T' then T else cannot_merge_types ();
    3.15 @@ -277,6 +272,7 @@
    3.16      val pre_map_defs = map map_def_of_bnf pre_bnfs;
    3.17      val pre_set_defss = map set_defs_of_bnf pre_bnfs;
    3.18      val pre_rel_defs = map rel_def_of_bnf pre_bnfs;
    3.19 +    val nested_map_comps'' = map ((fn thm => thm RS sym) o map_comp_of_bnf) nested_bnfs;
    3.20      val nested_map_comp's = map map_comp'_of_bnf nested_bnfs;
    3.21      val nested_map_ids'' = map (unfold_thms lthy @{thms id_def} o map_id_of_bnf) nested_bnfs;
    3.22      val nesting_map_ids'' = map (unfold_thms lthy @{thms id_def} o map_id_of_bnf) nesting_bnfs;
    3.23 @@ -312,8 +308,8 @@
    3.24      val fp_rec_fun_Ts = fst (split_last (binder_types (fastype_of any_fp_rec)));
    3.25  
    3.26      val (((fold_only as (gss, _, _), rec_only as (hss, _, _)),
    3.27 -          (zs, cs, cpss, unfold_only as ((pgss, crgsss), _), corec_only as ((phss, cshsss), _))),
    3.28 -         names_lthy0) =
    3.29 +          (cs, cpss, unfold_only as ((pgss, crssss, cgssss), (_, g_Tsss, _)),
    3.30 +           corec_only as ((phss, csssss, chssss), (_, h_Tsss, _)))), names_lthy0) =
    3.31        if lfp then
    3.32          let
    3.33            val y_Tsss =
    3.34 @@ -344,7 +340,7 @@
    3.35            val zsss = map2 (map2 (map2 retype_free)) z_Tsss ysss;
    3.36          in
    3.37            ((((gss, g_Tss, ysss), (hss, h_Tss, zsss)),
    3.38 -            ([], [], [], (([], []), ([], [])), (([], []), ([], [])))), lthy)
    3.39 +            ([], [], (([], [], []), ([], [], [])), (([], [], []), ([], [], [])))), lthy)
    3.40          end
    3.41        else
    3.42          let
    3.43 @@ -373,10 +369,9 @@
    3.44  
    3.45            val (r_Tssss, g_sum_prod_Ts, g_Tsss, g_Tssss, pg_Tss) = mk_types single fp_fold_fun_Ts;
    3.46  
    3.47 -          val ((((Free (z, _), cs), pss), gssss), lthy) =
    3.48 +          val (((cs, pss), gssss), lthy) =
    3.49              lthy
    3.50 -            |> yield_singleton (mk_Frees "z") dummyT
    3.51 -            ||>> mk_Frees "a" Cs
    3.52 +            |> mk_Frees "a" Cs
    3.53              ||>> mk_Freess "p" p_Tss
    3.54              ||>> mk_Freessss "g" g_Tssss;
    3.55            val rssss = map (map (map (fn [] => []))) r_Tssss;
    3.56 @@ -401,32 +396,16 @@
    3.57  
    3.58            val cpss = map2 (map o rapp) cs pss;
    3.59  
    3.60 -          fun build_sum_inj mk_inj (T, U) =
    3.61 -            if T = U then
    3.62 -              id_const T
    3.63 -            else
    3.64 -              (case (T, U) of
    3.65 -                (Type (s, _), Type (s', _)) =>
    3.66 -                if s = s' then build_map (build_sum_inj mk_inj) T U
    3.67 -                else uncurry mk_inj (dest_sumT U)
    3.68 -              | _ => uncurry mk_inj (dest_sumT U));
    3.69 -
    3.70 -          fun build_dtor_corec_arg _ [] [cf] = cf
    3.71 -            | build_dtor_corec_arg T [cq] [cf, cf'] =
    3.72 -              mk_If cq (build_sum_inj Inl_const (fastype_of cf, T) $ cf)
    3.73 -                (build_sum_inj Inr_const (fastype_of cf', T) $ cf')
    3.74 -
    3.75 -          fun mk_terms f_Tsss qssss fssss =
    3.76 +          fun mk_terms qssss fssss =
    3.77              let
    3.78                val pfss = map3 flat_preds_predsss_gettersss pss qssss fssss;
    3.79                val cqssss = map2 (map o map o map o rapp) cs qssss;
    3.80                val cfssss = map2 (map o map o map o rapp) cs fssss;
    3.81 -              val cqfsss = map3 (map3 (map3 build_dtor_corec_arg)) f_Tsss cqssss cfssss;
    3.82 -            in (pfss, cqfsss) end;
    3.83 +            in (pfss, cqssss, cfssss) end;
    3.84          in
    3.85            (((([], [], []), ([], [], [])),
    3.86 -            ([z], cs, cpss, (mk_terms g_Tsss rssss gssss, (g_sum_prod_Ts, pg_Tss)),
    3.87 -             (mk_terms h_Tsss sssss hssss, (h_sum_prod_Ts, ph_Tss)))), lthy)
    3.88 +            (cs, cpss, (mk_terms rssss gssss, (g_sum_prod_Ts, g_Tsss, pg_Tss)),
    3.89 +             (mk_terms sssss hssss, (h_sum_prod_Ts, h_Tsss, ph_Tss)))), lthy)
    3.90          end;
    3.91  
    3.92      fun define_ctrs_case_for_type (((((((((((((((((((((((((fp_bnf, fp_b), fpT), C), ctor), dtor),
    3.93 @@ -668,12 +647,30 @@
    3.94            let
    3.95              val B_to_fpT = C --> fpT;
    3.96  
    3.97 +            fun build_sum_inj mk_inj (T, U) =
    3.98 +              if T = U then
    3.99 +                id_const T
   3.100 +              else
   3.101 +                (case (T, U) of
   3.102 +                  (Type (s, _), Type (s', _)) =>
   3.103 +                  if s = s' then build_map (build_sum_inj mk_inj) T U
   3.104 +                  else uncurry mk_inj (dest_sumT U)
   3.105 +                | _ => uncurry mk_inj (dest_sumT U));
   3.106 +
   3.107 +            fun build_dtor_corec_like_arg _ [] [cf] = cf
   3.108 +              | build_dtor_corec_like_arg T [cq] [cf, cf'] =
   3.109 +                mk_If cq (build_sum_inj Inl_const (fastype_of cf, T) $ cf)
   3.110 +                  (build_sum_inj Inr_const (fastype_of cf', T) $ cf')
   3.111 +
   3.112 +            val crgsss = map3 (map3 (map3 build_dtor_corec_like_arg)) g_Tsss crssss cgssss;
   3.113 +            val cshsss = map3 (map3 (map3 build_dtor_corec_like_arg)) h_Tsss csssss chssss;
   3.114 +
   3.115              fun mk_preds_getterss_join c n cps sum_prod_T cqfss =
   3.116                Term.lambda c (mk_IfN sum_prod_T cps
   3.117                  (map2 (mk_InN_balanced sum_prod_T n) (map HOLogic.mk_tuple cqfss) (1 upto n)));
   3.118  
   3.119 -            fun generate_corec_like (suf, fp_rec_like, ((pfss, cqfsss), (f_sum_prod_Ts,
   3.120 -                pf_Tss))) =
   3.121 +            fun generate_corec_like (suf, fp_rec_like, (cqfsss, ((pfss, _, _), (f_sum_prod_Ts, _,
   3.122 +                pf_Tss)))) =
   3.123                let
   3.124                  val res_T = fold_rev (curry (op --->)) pf_Tss B_to_fpT;
   3.125                  val binding = qualify false fp_b_name (Binding.suffix_name ("_" ^ suf) fp_b);
   3.126 @@ -684,8 +681,8 @@
   3.127                in (binding, spec) end;
   3.128  
   3.129              val corec_like_infos =
   3.130 -              [(unfoldN, fp_fold, unfold_only),
   3.131 -               (corecN, fp_rec, corec_only)];
   3.132 +              [(unfoldN, fp_fold, (crgsss, unfold_only)),
   3.133 +               (corecN, fp_rec, (cshsss, corec_only))];
   3.134  
   3.135              val (bindings, specs) = map generate_corec_like corec_like_infos |> split_list;
   3.136  
   3.137 @@ -919,8 +916,7 @@
   3.138              fun build_rel rs' T =
   3.139                (case find_index (curry (op =) T) fpTs of
   3.140                  ~1 =>
   3.141 -                if exists_fp_subtype T then build_rel_step (build_rel rs') T
   3.142 -                else HOLogic.eq_const T
   3.143 +                if exists_fp_subtype T then build_rel_step (build_rel rs') T else HOLogic.eq_const T
   3.144                | kk => nth rs' kk);
   3.145  
   3.146              fun build_rel_app rs' usel vsel =
   3.147 @@ -974,7 +970,6 @@
   3.148  
   3.149          fun mk_maybe_not pos = not pos ? HOLogic.mk_not;
   3.150  
   3.151 -        val z = the_single zs;
   3.152          val gunfolds = map (lists_bmoc pgss) unfolds;
   3.153          val hcorecs = map (lists_bmoc phss) corecs;
   3.154  
   3.155 @@ -985,58 +980,66 @@
   3.156                  (Logic.list_implies (seq_conds (HOLogic.mk_Trueprop oo mk_maybe_not) n k cps,
   3.157                     mk_Trueprop_eq (fcorec_like $ c, Term.list_comb (ctr, take m cfs'))));
   3.158  
   3.159 -            fun build_corec_like fcorec_likes maybe_tack (T, U) =
   3.160 +            fun build_corec_like fcorec_likes (T, U) =
   3.161                if T = U then
   3.162                  id_const T
   3.163                else
   3.164                  (case find_index (curry (op =) U) fpTs of
   3.165 -                  ~1 => build_map (build_corec_like fcorec_likes maybe_tack) T U
   3.166 -                | kk => maybe_tack (nth cs kk, nth us kk) (nth fcorec_likes kk));
   3.167 +                  ~1 => build_map (build_corec_like fcorec_likes) T U
   3.168 +                | kk => nth fcorec_likes kk);
   3.169 +
   3.170 +            val mk_U = typ_subst (map2 pair Cs fpTs);
   3.171  
   3.172 -            fun mk_U maybe_mk_sumT =
   3.173 -              typ_subst (map2 (fn C => fn fpT => (maybe_mk_sumT fpT C, fpT)) Cs fpTs);
   3.174 +            fun intr_corec_likes fcorec_likes [] [cf] =
   3.175 +                let val T = fastype_of cf in
   3.176 +                  if exists_Cs_subtype T then build_corec_like fcorec_likes (T, mk_U T) $ cf else cf
   3.177 +                end
   3.178 +              | intr_corec_likes fcorec_likes [cq] [cf, cf'] =
   3.179 +                mk_If cq (intr_corec_likes fcorec_likes [] [cf])
   3.180 +                  (intr_corec_likes fcorec_likes [] [cf']);
   3.181 +
   3.182 +            val crgsss = map2 (map2 (map2 (intr_corec_likes gunfolds))) crssss cgssss;
   3.183 +            val cshsss = map2 (map2 (map2 (intr_corec_likes hcorecs))) csssss chssss;
   3.184  
   3.185 -            fun intr_corec_likes fcorec_likes maybe_mk_sumT maybe_tack cqf =
   3.186 -              let val T = fastype_of cqf in
   3.187 -                if exists_Cs_subtype T then
   3.188 -                  build_corec_like fcorec_likes maybe_tack (T, mk_U maybe_mk_sumT T) $ cqf
   3.189 -                else
   3.190 -                  cqf
   3.191 +            val unfold_goalss =
   3.192 +              map8 (map4 oooo mk_goal pgss) cs cpss gunfolds ns kss ctrss mss crgsss;
   3.193 +            val corec_goalss =
   3.194 +              map8 (map4 oooo mk_goal phss) cs cpss hcorecs ns kss ctrss mss cshsss;
   3.195 +
   3.196 +            fun mk_map_if_distrib bnf =
   3.197 +              let
   3.198 +                val mapx = map_of_bnf bnf;
   3.199 +                val live = live_of_bnf bnf;
   3.200 +                val ((Ts, T), U) = strip_typeN (live + 1) (fastype_of mapx) |>> split_last;
   3.201 +                val fs = Variable.variant_frees lthy [mapx] (map (pair "f") Ts);
   3.202 +                val t = Term.list_comb (mapx, map (Var o apfst (rpair 0)) fs);
   3.203 +              in
   3.204 +                Drule.instantiate' (map (SOME o certifyT lthy) [U, T]) [SOME (certify lthy t)]
   3.205 +                  @{thm if_distrib}
   3.206                end;
   3.207  
   3.208 -            val crgsss' = map (map (map (intr_corec_likes gunfolds (K I) (K I)))) crgsss;
   3.209 -            val cshsss' =
   3.210 -              map (map (map (intr_corec_likes hcorecs (curry mk_sumT) (tack z)))) cshsss;
   3.211 -
   3.212 -            val unfold_goalss =
   3.213 -              map8 (map4 oooo mk_goal pgss) cs cpss gunfolds ns kss ctrss mss crgsss';
   3.214 -            val corec_goalss =
   3.215 -              map8 (map4 oooo mk_goal phss) cs cpss hcorecs ns kss ctrss mss cshsss';
   3.216 +            val nested_map_if_distribs = map mk_map_if_distrib nested_bnfs;
   3.217  
   3.218              val unfold_tacss =
   3.219 -              map3 (map oo mk_corec_like_tac unfold_defs nesting_map_ids'') fp_fold_thms
   3.220 -                pre_map_defs ctr_defss;
   3.221 +              map3 (map oo mk_corec_like_tac unfold_defs [] [] nesting_map_ids'' [])
   3.222 +                fp_fold_thms pre_map_defs ctr_defss;
   3.223              val corec_tacss =
   3.224 -              map3 (map oo mk_corec_like_tac corec_defs nesting_map_ids'') fp_rec_thms pre_map_defs
   3.225 -                ctr_defss;
   3.226 +              map3 (map oo mk_corec_like_tac corec_defs nested_map_comps'' nested_map_comp's
   3.227 +                  (nested_map_ids'' @ nesting_map_ids'') nested_map_if_distribs)
   3.228 +                fp_rec_thms pre_map_defs ctr_defss;
   3.229  
   3.230              fun prove goal tac =
   3.231                Skip_Proof.prove lthy [] [] goal (tac o #context) |> Thm.close_derivation;
   3.232  
   3.233              val unfold_thmss = map2 (map2 prove) unfold_goalss unfold_tacss;
   3.234 -            val corec_thmss =
   3.235 -              map2 (map2 prove) corec_goalss corec_tacss
   3.236 -              |> map (map (unfold_thms lthy @{thms sum_case_if}));
   3.237 -
   3.238 -            val unfold_safesss = map2 (map2 (map2 (curry (op =)))) crgsss' crgsss;
   3.239 -            val corec_safesss = map2 (map2 (map2 (curry (op =)))) cshsss' cshsss;
   3.240 +            val corec_thmss = map2 (map2 prove) corec_goalss corec_tacss;
   3.241  
   3.242              val filter_safesss =
   3.243                map2 (map_filter (fn (safes, thm) => if forall I safes then SOME thm else NONE) oo
   3.244 -                curry (op ~~));
   3.245 +                curry (op ~~)) (map2 (map2 (map2 (member (op =)))) cgssss crgsss);
   3.246  
   3.247 -            val safe_unfold_thmss = filter_safesss unfold_safesss unfold_thmss;
   3.248 -            val safe_corec_thmss = filter_safesss corec_safesss corec_thmss;
   3.249 +            val safe_unfold_thmss = filter_safesss unfold_thmss;
   3.250 +            val safe_corec_thmss = filter_safesss corec_thmss;
   3.251            in
   3.252              (unfold_thmss, corec_thmss, safe_unfold_thmss, safe_corec_thmss)
   3.253            end;
     4.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Tue Oct 02 01:00:18 2012 +0200
     4.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Tue Oct 02 01:00:18 2012 +0200
     4.3 @@ -14,7 +14,8 @@
     4.4    val mk_case_tac: Proof.context -> int -> int -> int -> thm -> thm -> thm -> tactic
     4.5    val mk_coinduct_tac: Proof.context -> thm list -> int -> int list -> thm -> thm list ->
     4.6      thm list -> thm list -> thm list list -> thm list list list -> thm list list list -> tactic
     4.7 -  val mk_corec_like_tac: thm list -> thm list -> thm -> thm -> thm -> Proof.context -> tactic
     4.8 +  val mk_corec_like_tac: thm list -> thm list -> thm list -> thm list -> thm list -> thm -> thm ->
     4.9 +    thm -> Proof.context -> tactic
    4.10    val mk_ctor_iff_dtor_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm ->
    4.11      tactic
    4.12    val mk_disc_corec_like_iff_tac: thm list -> thm list -> thm list -> Proof.context -> tactic
    4.13 @@ -37,7 +38,7 @@
    4.14  val basic_simp_thms = @{thms simp_thms(7,8,12,14,22,24)};
    4.15  val more_simp_thms = basic_simp_thms @ @{thms simp_thms(11,15,16,21)};
    4.16  
    4.17 -val sum_prod_thms_map = @{thms id_apply map_pair_simp sum_map.simps prod.cases};
    4.18 +val sum_prod_thms_map = @{thms id_apply map_pair_simp prod.cases sum.cases sum_map.simps};
    4.19  val sum_prod_thms_set0 =
    4.20    @{thms SUP_empty Sup_empty Sup_insert UN_insert Un_empty_left Un_empty_right Un_iff
    4.21        Union_Un_distrib collect_def[abs_def] image_def o_apply map_pair_simp
    4.22 @@ -107,10 +108,16 @@
    4.23    unfold_thms_tac ctxt (ctr_def :: ctor_rec_like :: rec_like_defs @ pre_map_defs @ map_comp's @
    4.24      map_ids'' @ rec_like_unfold_thms) THEN rtac refl 1;
    4.25  
    4.26 -fun mk_corec_like_tac corec_like_defs map_ids'' ctor_dtor_corec_like pre_map_def ctr_def ctxt =
    4.27 +(*TODO: sum_case_if needed?*)
    4.28 +val corec_like_unfold_thms =
    4.29 +  @{thms id_def ident_o_ident sum_case_if sum_case_o_inj} @ sum_prod_thms_map;
    4.30 +
    4.31 +fun mk_corec_like_tac corec_like_defs map_comps'' map_comp's map_ids'' map_if_distribs
    4.32 +    ctor_dtor_corec_like pre_map_def ctr_def ctxt =
    4.33    unfold_thms_tac ctxt (ctr_def :: corec_like_defs) THEN
    4.34    (rtac (ctor_dtor_corec_like RS trans) THEN' asm_simp_tac ss_if_True_False) 1 THEN_MAYBE
    4.35 -  (unfold_thms_tac ctxt (pre_map_def :: @{thm id_def} :: sum_prod_thms_map @ map_ids'') THEN
    4.36 +  (unfold_thms_tac ctxt (pre_map_def :: map_comp's @ map_comps'' @ map_ids'' @ map_if_distribs @
    4.37 +    corec_like_unfold_thms) THEN
    4.38     (rtac refl ORELSE' rtac (@{thm unit_eq} RS arg_cong)) 1);
    4.39  
    4.40  fun mk_disc_corec_like_iff_tac case_splits' corec_likes discs ctxt =