src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
changeset 51810 7b75fab5ebf5
parent 51808 355dcd6a9b3c
child 51811 1461426e2bf1
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Apr 29 11:04:56 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Apr 29 11:46:03 2013 +0200
     1.3 @@ -173,16 +173,16 @@
     1.4      val Ts' = map domain_type (fst (strip_typeN live (fastype_of rel)));
     1.5    in Term.list_comb (rel, map build_arg Ts') end;
     1.6  
     1.7 -fun derive_induct_fold_rec_thms_for_types
     1.8 -    nn fp_b_names pre_bnfs fp_induct fp_fold_thms fp_rec_thms nesting_bnfs nested_bnfs fpTs Cs
     1.9 -    ctr_Tsss mss ns gss hss ((ctrss, xsss, ctr_defss, _), (folds, recs, fold_defs, rec_defs)) lthy =
    1.10 +fun derive_induct_fold_rec_thms_for_types nn fp_b_names pre_bnfs fp_induct fp_fold_thms fp_rec_thms
    1.11 +    nesting_bnfs nested_bnfs fpTs Cs ctr_Tsss mss ns gss hss
    1.12 +    ((ctrss, xsss, ctr_defss, _), (folds, recs, fold_defs, rec_defs)) lthy =
    1.13    let
    1.14      val pre_map_defs = map map_def_of_bnf pre_bnfs;
    1.15      val pre_set_defss = map set_defs_of_bnf pre_bnfs;
    1.16      val nested_map_comp's = map map_comp'_of_bnf nested_bnfs;
    1.17      val nested_map_ids'' = map (unfold_thms lthy @{thms id_def} o map_id_of_bnf) nested_bnfs;
    1.18 +    val nested_set_map's = maps set_map'_of_bnf nested_bnfs;
    1.19      val nesting_map_ids'' = map (unfold_thms lthy @{thms id_def} o map_id_of_bnf) nesting_bnfs;
    1.20 -    val nested_set_map's = maps set_map'_of_bnf nested_bnfs;
    1.21  
    1.22      val (((ps, ps'), us'), names_lthy) =
    1.23        lthy
    1.24 @@ -319,13 +319,276 @@
    1.25        end;
    1.26  
    1.27      val induct_case_names_attr = Attrib.internal (K (Rule_Cases.case_names induct_cases));
    1.28 -    fun induct_type_attr T_name = Attrib.internal (K (Induct.induct_type T_name));
    1.29    in
    1.30 -    ((induct_thm, [induct_case_names_attr]),
    1.31 -     (induct_thms, fn T_name => [induct_case_names_attr, induct_type_attr T_name]),
    1.32 +    ((induct_thm, induct_thms, [induct_case_names_attr]),
    1.33       (fold_thmss, code_simp_attrs), (rec_thmss, code_simp_attrs))
    1.34    end;
    1.35  
    1.36 +fun derive_coinduct_unfold_corec_thms_for_types names_lthy0 no_defs_lthy nn fp_b_names pre_bnfs
    1.37 +    fp_induct fp_strong_induct dtor_ctors fp_fold_thms fp_rec_thms nesting_bnfs nested_bnfs fpTs Cs
    1.38 +    As kss mss ns cs cpss pgss crssss cgssss phss csssss chssss
    1.39 +    ((ctrss, _, ctr_defss, ctr_wrap_ress), (unfolds, corecs, unfold_defs, corec_defs)) lthy =
    1.40 +  let
    1.41 +    val pre_map_defs = map map_def_of_bnf pre_bnfs;
    1.42 +    val pre_rel_defs = map rel_def_of_bnf pre_bnfs;
    1.43 +    val nested_map_comp's = map map_comp'_of_bnf nested_bnfs;
    1.44 +    val nested_map_comps'' = map ((fn thm => thm RS sym) o map_comp_of_bnf) nested_bnfs;
    1.45 +    val nested_map_ids'' = map (unfold_thms lthy @{thms id_def} o map_id_of_bnf) nested_bnfs;
    1.46 +    val nesting_map_ids'' = map (unfold_thms lthy @{thms id_def} o map_id_of_bnf) nesting_bnfs;
    1.47 +    val nesting_rel_eqs = map rel_eq_of_bnf nesting_bnfs;
    1.48 +
    1.49 +    val discss = map (map (mk_disc_or_sel As) o #1) ctr_wrap_ress;
    1.50 +    val selsss = map (map (map (mk_disc_or_sel As)) o #2) ctr_wrap_ress;
    1.51 +    val exhaust_thms = map #3 ctr_wrap_ress;
    1.52 +    val disc_thmsss = map #7 ctr_wrap_ress;
    1.53 +    val discIss = map #8 ctr_wrap_ress;
    1.54 +    val sel_thmsss = map #9 ctr_wrap_ress;
    1.55 +
    1.56 +    val (((rs, us'), vs'), names_lthy) =
    1.57 +      lthy
    1.58 +      |> mk_Frees "R" (map (fn T => mk_pred2T T T) fpTs)
    1.59 +      ||>> Variable.variant_fixes fp_b_names
    1.60 +      ||>> Variable.variant_fixes (map (suffix "'") fp_b_names);
    1.61 +
    1.62 +    val us = map2 (curry Free) us' fpTs;
    1.63 +    val udiscss = map2 (map o rapp) us discss;
    1.64 +    val uselsss = map2 (map o map o rapp) us selsss;
    1.65 +
    1.66 +    val vs = map2 (curry Free) vs' fpTs;
    1.67 +    val vdiscss = map2 (map o rapp) vs discss;
    1.68 +    val vselsss = map2 (map o map o rapp) vs selsss;
    1.69 +
    1.70 +    val ((coinduct_thms, coinduct_thm), (strong_coinduct_thms, strong_coinduct_thm)) =
    1.71 +      let
    1.72 +        val uvrs = map3 (fn r => fn u => fn v => r $ u $ v) rs us vs;
    1.73 +        val uv_eqs = map2 (curry HOLogic.mk_eq) us vs;
    1.74 +        val strong_rs =
    1.75 +          map4 (fn u => fn v => fn uvr => fn uv_eq =>
    1.76 +            fold_rev Term.lambda [u, v] (HOLogic.mk_disj (uvr, uv_eq))) us vs uvrs uv_eqs;
    1.77 +
    1.78 +        fun build_rel rs' T =
    1.79 +          (case find_index (curry (op =) T) fpTs of
    1.80 +            ~1 =>
    1.81 +            if exists_subtype_in fpTs T then build_rel_step lthy (build_rel rs') T
    1.82 +            else HOLogic.eq_const T
    1.83 +          | kk => nth rs' kk);
    1.84 +
    1.85 +        fun build_rel_app rs' usel vsel =
    1.86 +          fold rapp [usel, vsel] (build_rel rs' (fastype_of usel));
    1.87 +
    1.88 +        fun mk_prem_ctr_concls rs' n k udisc usels vdisc vsels =
    1.89 +          (if k = n then [] else [HOLogic.mk_eq (udisc, vdisc)]) @
    1.90 +          (if null usels then
    1.91 +             []
    1.92 +           else
    1.93 +             [Library.foldr HOLogic.mk_imp (if n = 1 then [] else [udisc, vdisc],
    1.94 +                Library.foldr1 HOLogic.mk_conj (map2 (build_rel_app rs') usels vsels))]);
    1.95 +
    1.96 +        fun mk_prem_concl rs' n udiscs uselss vdiscs vselss =
    1.97 +          Library.foldr1 HOLogic.mk_conj
    1.98 +            (flat (map5 (mk_prem_ctr_concls rs' n) (1 upto n) udiscs uselss vdiscs vselss))
    1.99 +          handle List.Empty => @{term True};
   1.100 +
   1.101 +        fun mk_prem rs' uvr u v n udiscs uselss vdiscs vselss =
   1.102 +          fold_rev Logic.all [u, v] (Logic.mk_implies (HOLogic.mk_Trueprop uvr,
   1.103 +            HOLogic.mk_Trueprop (mk_prem_concl rs' n udiscs uselss vdiscs vselss)));
   1.104 +
   1.105 +        val concl =
   1.106 +          HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
   1.107 +            (map3 (fn uvr => fn u => fn v => HOLogic.mk_imp (uvr, HOLogic.mk_eq (u, v)))
   1.108 +               uvrs us vs));
   1.109 +
   1.110 +        fun mk_goal rs' =
   1.111 +          Logic.list_implies (map8 (mk_prem rs') uvrs us vs ns udiscss uselsss vdiscss vselsss,
   1.112 +            concl);
   1.113 +
   1.114 +        val goal = mk_goal rs;
   1.115 +        val strong_goal = mk_goal strong_rs;
   1.116 +
   1.117 +        fun prove dtor_coinduct' goal =
   1.118 +          Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
   1.119 +            mk_coinduct_tac ctxt nesting_rel_eqs nn ns dtor_coinduct' pre_rel_defs dtor_ctors
   1.120 +              exhaust_thms ctr_defss disc_thmsss sel_thmsss)
   1.121 +          |> singleton (Proof_Context.export names_lthy lthy)
   1.122 +          |> Thm.close_derivation;
   1.123 +
   1.124 +        fun postproc nn thm =
   1.125 +          Thm.permute_prems 0 nn
   1.126 +            (if nn = 1 then thm RS mp
   1.127 +             else funpow nn (fn thm => reassoc_conjs (thm RS mp_conj)) thm)
   1.128 +          |> Drule.zero_var_indexes
   1.129 +          |> `(conj_dests nn);
   1.130 +      in
   1.131 +        (postproc nn (prove fp_induct goal), postproc nn (prove fp_strong_induct strong_goal))
   1.132 +      end;
   1.133 +
   1.134 +    fun mk_coinduct_concls ms discs ctrs =
   1.135 +      let
   1.136 +        fun mk_disc_concl disc = [name_of_disc disc];
   1.137 +        fun mk_ctr_concl 0 _ = []
   1.138 +          | mk_ctr_concl _ ctor = [name_of_ctr ctor];
   1.139 +        val disc_concls = map mk_disc_concl (fst (split_last discs)) @ [[]];
   1.140 +        val ctr_concls = map2 mk_ctr_concl ms ctrs;
   1.141 +      in
   1.142 +        flat (map2 append disc_concls ctr_concls)
   1.143 +      end;
   1.144 +
   1.145 +    val coinduct_cases = quasi_unambiguous_case_names (map (prefix EqN) fp_b_names);
   1.146 +    val coinduct_conclss =
   1.147 +      map3 (quasi_unambiguous_case_names ooo mk_coinduct_concls) mss discss ctrss;
   1.148 +
   1.149 +    fun mk_maybe_not pos = not pos ? HOLogic.mk_not;
   1.150 +
   1.151 +    val gunfolds = map (lists_bmoc pgss) unfolds;
   1.152 +    val hcorecs = map (lists_bmoc phss) corecs;
   1.153 +
   1.154 +    val (unfold_thmss, corec_thmss, safe_unfold_thmss, safe_corec_thmss) =
   1.155 +      let
   1.156 +        fun mk_goal pfss c cps fcorec_like n k ctr m cfs' =
   1.157 +          fold_rev (fold_rev Logic.all) ([c] :: pfss)
   1.158 +            (Logic.list_implies (seq_conds (HOLogic.mk_Trueprop oo mk_maybe_not) n k cps,
   1.159 +               mk_Trueprop_eq (fcorec_like $ c, Term.list_comb (ctr, take m cfs'))));
   1.160 +
   1.161 +        fun build_corec_like fcorec_likes (T, U) =
   1.162 +          if T = U then
   1.163 +            id_const T
   1.164 +          else
   1.165 +            (case find_index (curry (op =) U) fpTs of
   1.166 +              ~1 => build_map lthy (build_corec_like fcorec_likes) T U
   1.167 +            | kk => nth fcorec_likes kk);
   1.168 +
   1.169 +        val mk_U = typ_subst (map2 pair Cs fpTs);
   1.170 +
   1.171 +        fun intr_corec_likes fcorec_likes [] [cf] =
   1.172 +            let val T = fastype_of cf in
   1.173 +              if exists_subtype_in Cs T then build_corec_like fcorec_likes (T, mk_U T) $ cf
   1.174 +              else cf
   1.175 +            end
   1.176 +          | intr_corec_likes fcorec_likes [cq] [cf, cf'] =
   1.177 +            mk_If cq (intr_corec_likes fcorec_likes [] [cf])
   1.178 +              (intr_corec_likes fcorec_likes [] [cf']);
   1.179 +
   1.180 +        val crgsss = map2 (map2 (map2 (intr_corec_likes gunfolds))) crssss cgssss;
   1.181 +        val cshsss = map2 (map2 (map2 (intr_corec_likes hcorecs))) csssss chssss;
   1.182 +
   1.183 +        val unfold_goalss =
   1.184 +          map8 (map4 oooo mk_goal pgss) cs cpss gunfolds ns kss ctrss mss crgsss;
   1.185 +        val corec_goalss =
   1.186 +          map8 (map4 oooo mk_goal phss) cs cpss hcorecs ns kss ctrss mss cshsss;
   1.187 +
   1.188 +        fun mk_map_if_distrib bnf =
   1.189 +          let
   1.190 +            val mapx = map_of_bnf bnf;
   1.191 +            val live = live_of_bnf bnf;
   1.192 +            val ((Ts, T), U) = strip_typeN (live + 1) (fastype_of mapx) |>> split_last;
   1.193 +            val fs = Variable.variant_frees lthy [mapx] (map (pair "f") Ts);
   1.194 +            val t = Term.list_comb (mapx, map (Var o apfst (rpair 0)) fs);
   1.195 +          in
   1.196 +            Drule.instantiate' (map (SOME o certifyT lthy) [U, T]) [SOME (certify lthy t)]
   1.197 +              @{thm if_distrib}
   1.198 +          end;
   1.199 +
   1.200 +        val nested_map_if_distribs = map mk_map_if_distrib nested_bnfs;
   1.201 +
   1.202 +        val unfold_tacss =
   1.203 +          map3 (map oo mk_corec_like_tac unfold_defs [] [] nesting_map_ids'' [])
   1.204 +            fp_fold_thms pre_map_defs ctr_defss;
   1.205 +        val corec_tacss =
   1.206 +          map3 (map oo mk_corec_like_tac corec_defs nested_map_comps'' nested_map_comp's
   1.207 +              (nested_map_ids'' @ nesting_map_ids'') nested_map_if_distribs)
   1.208 +            fp_rec_thms pre_map_defs ctr_defss;
   1.209 +
   1.210 +        fun prove goal tac =
   1.211 +          Goal.prove_sorry lthy [] [] goal (tac o #context) |> Thm.close_derivation;
   1.212 +
   1.213 +        val unfold_thmss = map2 (map2 prove) unfold_goalss unfold_tacss;
   1.214 +        val corec_thmss = map2 (map2 prove) corec_goalss corec_tacss;
   1.215 +
   1.216 +        val filter_safesss =
   1.217 +          map2 (map_filter (fn (safes, thm) => if forall I safes then SOME thm else NONE) oo
   1.218 +            curry (op ~~)) (map2 (map2 (map2 (member (op =)))) cgssss crgsss);
   1.219 +
   1.220 +        val safe_unfold_thmss = filter_safesss unfold_thmss;
   1.221 +        val safe_corec_thmss = filter_safesss corec_thmss;
   1.222 +      in
   1.223 +        (unfold_thmss, corec_thmss, safe_unfold_thmss, safe_corec_thmss)
   1.224 +      end;
   1.225 +
   1.226 +    val (disc_unfold_iff_thmss, disc_corec_iff_thmss) =
   1.227 +      let
   1.228 +        fun mk_goal c cps fcorec_like n k disc =
   1.229 +          mk_Trueprop_eq (disc $ (fcorec_like $ c),
   1.230 +            if n = 1 then @{const True}
   1.231 +            else Library.foldr1 HOLogic.mk_conj (seq_conds mk_maybe_not n k cps));
   1.232 +
   1.233 +        val unfold_goalss = map6 (map2 oooo mk_goal) cs cpss gunfolds ns kss discss;
   1.234 +        val corec_goalss = map6 (map2 oooo mk_goal) cs cpss hcorecs ns kss discss;
   1.235 +
   1.236 +        fun mk_case_split' cp =
   1.237 +          Drule.instantiate' [] [SOME (certify lthy cp)] @{thm case_split};
   1.238 +
   1.239 +        val case_splitss' = map (map mk_case_split') cpss;
   1.240 +
   1.241 +        val unfold_tacss =
   1.242 +          map3 (map oo mk_disc_corec_like_iff_tac) case_splitss' unfold_thmss disc_thmsss;
   1.243 +        val corec_tacss =
   1.244 +          map3 (map oo mk_disc_corec_like_iff_tac) case_splitss' corec_thmss disc_thmsss;
   1.245 +
   1.246 +        fun prove goal tac =
   1.247 +          Goal.prove_sorry lthy [] [] goal (tac o #context)
   1.248 +          |> singleton (Proof_Context.export names_lthy0 no_defs_lthy)
   1.249 +          |> Thm.close_derivation;
   1.250 +
   1.251 +        fun proves [_] [_] = []
   1.252 +          | proves goals tacs = map2 prove goals tacs;
   1.253 +      in
   1.254 +        (map2 proves unfold_goalss unfold_tacss,
   1.255 +         map2 proves corec_goalss corec_tacss)
   1.256 +      end;
   1.257 +
   1.258 +    val is_triv_discI = is_triv_implies orf is_concl_refl;
   1.259 +
   1.260 +    fun mk_disc_corec_like_thms corec_likes discIs =
   1.261 +      map (op RS) (filter_out (is_triv_discI o snd) (corec_likes ~~ discIs));
   1.262 +
   1.263 +    val disc_unfold_thmss = map2 mk_disc_corec_like_thms unfold_thmss discIss;
   1.264 +    val disc_corec_thmss = map2 mk_disc_corec_like_thms corec_thmss discIss;
   1.265 +
   1.266 +    fun mk_sel_corec_like_thm corec_like_thm sel sel_thm =
   1.267 +      let
   1.268 +        val (domT, ranT) = dest_funT (fastype_of sel);
   1.269 +        val arg_cong' =
   1.270 +          Drule.instantiate' (map (SOME o certifyT lthy) [domT, ranT])
   1.271 +            [NONE, NONE, SOME (certify lthy sel)] arg_cong
   1.272 +          |> Thm.varifyT_global;
   1.273 +        val sel_thm' = sel_thm RSN (2, trans);
   1.274 +      in
   1.275 +        corec_like_thm RS arg_cong' RS sel_thm'
   1.276 +      end;
   1.277 +
   1.278 +    fun mk_sel_corec_like_thms corec_likess =
   1.279 +      map3 (map3 (map2 o mk_sel_corec_like_thm)) corec_likess selsss sel_thmsss |> map flat;
   1.280 +
   1.281 +    val sel_unfold_thmss = mk_sel_corec_like_thms unfold_thmss;
   1.282 +    val sel_corec_thmss = mk_sel_corec_like_thms corec_thmss;
   1.283 +
   1.284 +    val coinduct_consumes_attr = Attrib.internal (K (Rule_Cases.consumes nn));
   1.285 +    val coinduct_case_names_attr = Attrib.internal (K (Rule_Cases.case_names coinduct_cases));
   1.286 +    val coinduct_case_concl_attrs =
   1.287 +      map2 (fn casex => fn concls =>
   1.288 +          Attrib.internal (K (Rule_Cases.case_conclusion (casex, concls))))
   1.289 +        coinduct_cases coinduct_conclss;
   1.290 +    val coinduct_case_attrs =
   1.291 +      coinduct_consumes_attr :: coinduct_case_names_attr :: coinduct_case_concl_attrs;
   1.292 +  in
   1.293 +    ((coinduct_thm, coinduct_thms, strong_coinduct_thm, strong_coinduct_thms, coinduct_case_attrs),
   1.294 +     (unfold_thmss, corec_thmss, []),
   1.295 +     (safe_unfold_thmss, safe_corec_thmss),
   1.296 +     (disc_unfold_thmss, disc_corec_thmss, simp_attrs),
   1.297 +     (disc_unfold_iff_thmss, disc_corec_iff_thmss, simp_attrs),
   1.298 +     (sel_unfold_thmss, sel_corec_thmss, simp_attrs))
   1.299 +  end;
   1.300 +
   1.301  fun define_datatypes prepare_constraint prepare_typ prepare_term lfp construct_fp
   1.302      (wrap_opts as (no_dests, rep_compat), specs) no_defs_lthy0 =
   1.303    let
   1.304 @@ -453,10 +716,6 @@
   1.305      val pre_map_defs = map map_def_of_bnf pre_bnfs;
   1.306      val pre_set_defss = map set_defs_of_bnf pre_bnfs;
   1.307      val pre_rel_defs = map rel_def_of_bnf pre_bnfs;
   1.308 -    val nested_map_comps'' = map ((fn thm => thm RS sym) o map_comp_of_bnf) nested_bnfs;
   1.309 -    val nested_map_comp's = map map_comp'_of_bnf nested_bnfs;
   1.310 -    val nested_map_ids'' = map (unfold_thms lthy @{thms id_def} o map_id_of_bnf) nested_bnfs;
   1.311 -    val nesting_map_ids'' = map (unfold_thms lthy @{thms id_def} o map_id_of_bnf) nesting_bnfs;
   1.312      val nested_set_map's = maps set_map'_of_bnf nested_bnfs;
   1.313      val nesting_set_map's = maps set_map'_of_bnf nesting_bnfs;
   1.314  
   1.315 @@ -699,7 +958,7 @@
   1.316                (sel_bindingss, sel_defaultss))) lthy
   1.317            end;
   1.318  
   1.319 -        fun derive_maps_sets_rels (wrap_res, lthy) =
   1.320 +        fun derive_maps_sets_rels (ctr_wrap_res, lthy) =
   1.321            let
   1.322              val rel_flip = rel_flip_of_bnf fp_bnf;
   1.323              val nones = replicate live NONE;
   1.324 @@ -775,7 +1034,7 @@
   1.325                 (setsN, flat set_thmss, code_simp_attrs)]
   1.326                |> massage_simple_notes fp_b_name;
   1.327            in
   1.328 -            (wrap_res, lthy |> Local_Theory.notes notes |> snd)
   1.329 +            (ctr_wrap_res, lthy |> Local_Theory.notes notes |> snd)
   1.330            end;
   1.331  
   1.332          fun define_fold_rec no_defs_lthy =
   1.333 @@ -898,8 +1157,8 @@
   1.334  
   1.335          val define_rec_likes = if lfp then define_fold_rec else define_unfold_corec;
   1.336  
   1.337 -        fun massage_res ((wrap_res, rec_like_res), lthy) =
   1.338 -          (((ctrs, xss, ctr_defs, wrap_res), rec_like_res), lthy);
   1.339 +        fun massage_res ((ctr_wrap_res, rec_like_res), lthy) =
   1.340 +          (((ctrs, xss, ctr_defs, ctr_wrap_res), rec_like_res), lthy);
   1.341        in
   1.342          (wrap #> (live > 0 ? derive_maps_sets_rels) ##>> define_rec_likes #> massage_res, lthy')
   1.343        end;
   1.344 @@ -913,14 +1172,18 @@
   1.345        map3 (fn (_, _, _, injects, distincts, cases, _, _, _) => fn rec_likes => fn fold_likes =>
   1.346          injects @ distincts @ cases @ rec_likes @ fold_likes);
   1.347  
   1.348 -    fun derive_and_note_induct_fold_rec_thms_for_types (info as ((_, _, _, wrap_ress), _), lthy) =
   1.349 +    fun derive_and_note_induct_fold_rec_thms_for_types
   1.350 +        (info as ((_, _, _, ctr_wrap_ress), _), lthy) =
   1.351        let
   1.352 -        val ((induct_thm, induct_attrs), (induct_thms, inducts_attrs), (fold_thmss, fold_attrs),
   1.353 +        val ((induct_thm, induct_thms, induct_attrs),
   1.354 +             (fold_thmss, fold_attrs),
   1.355               (rec_thmss, rec_attrs)) =
   1.356            derive_induct_fold_rec_thms_for_types nn fp_b_names pre_bnfs fp_induct fp_fold_thms
   1.357              fp_rec_thms nesting_bnfs nested_bnfs fpTs Cs ctr_Tsss mss ns gss hss info lthy;
   1.358  
   1.359 -        val simp_thmss = mk_simp_thmss wrap_ress rec_thmss fold_thmss;
   1.360 +        fun induct_type_attr T_name = Attrib.internal (K (Induct.induct_type T_name));
   1.361 +
   1.362 +        val simp_thmss = mk_simp_thmss ctr_wrap_ress rec_thmss fold_thmss;
   1.363  
   1.364          val common_notes =
   1.365            (if nn > 1 then [(inductN, [induct_thm], induct_attrs)] else [])
   1.366 @@ -928,7 +1191,7 @@
   1.367  
   1.368          val notes =
   1.369            [(foldN, fold_thmss, K fold_attrs),
   1.370 -           (inductN, map single induct_thms, inducts_attrs),
   1.371 +           (inductN, map single induct_thms, fn T_name => induct_attrs @ [induct_type_attr T_name]),
   1.372             (recN, rec_thmss, K rec_attrs),
   1.373             (simpsN, simp_thmss, K [])]
   1.374            |> massage_multi_notes;
   1.375 @@ -936,251 +1199,28 @@
   1.376          lthy |> Local_Theory.notes (common_notes @ notes) |> snd
   1.377        end;
   1.378  
   1.379 -    fun derive_and_note_coinduct_unfold_corec_thms_for_types (((ctrss, _, ctr_defss, wrap_ress),
   1.380 -        (unfolds, corecs, unfold_defs, corec_defs)), lthy) =
   1.381 +    fun derive_and_note_coinduct_unfold_corec_thms_for_types
   1.382 +        (info as ((_, _, _, ctr_wrap_ress), _), lthy) =
   1.383        let
   1.384 -        val nesting_rel_eqs = map rel_eq_of_bnf nesting_bnfs;
   1.385 -
   1.386 -        val discss = map (map (mk_disc_or_sel As) o #1) wrap_ress;
   1.387 -        val selsss = map (map (map (mk_disc_or_sel As)) o #2) wrap_ress;
   1.388 -        val exhaust_thms = map #3 wrap_ress;
   1.389 -        val disc_thmsss = map #7 wrap_ress;
   1.390 -        val discIss = map #8 wrap_ress;
   1.391 -        val sel_thmsss = map #9 wrap_ress;
   1.392 -
   1.393 -        val (((rs, us'), vs'), names_lthy) =
   1.394 -          lthy
   1.395 -          |> mk_Frees "R" (map (fn T => mk_pred2T T T) fpTs)
   1.396 -          ||>> Variable.variant_fixes fp_b_names
   1.397 -          ||>> Variable.variant_fixes (map (suffix "'") fp_b_names);
   1.398 -
   1.399 -        val us = map2 (curry Free) us' fpTs;
   1.400 -        val udiscss = map2 (map o rapp) us discss;
   1.401 -        val uselsss = map2 (map o map o rapp) us selsss;
   1.402 -
   1.403 -        val vs = map2 (curry Free) vs' fpTs;
   1.404 -        val vdiscss = map2 (map o rapp) vs discss;
   1.405 -        val vselsss = map2 (map o map o rapp) vs selsss;
   1.406 -
   1.407 -        val ((coinduct_thms, coinduct_thm), (strong_coinduct_thms, strong_coinduct_thm)) =
   1.408 -          let
   1.409 -            val uvrs = map3 (fn r => fn u => fn v => r $ u $ v) rs us vs;
   1.410 -            val uv_eqs = map2 (curry HOLogic.mk_eq) us vs;
   1.411 -            val strong_rs =
   1.412 -              map4 (fn u => fn v => fn uvr => fn uv_eq =>
   1.413 -                fold_rev Term.lambda [u, v] (HOLogic.mk_disj (uvr, uv_eq))) us vs uvrs uv_eqs;
   1.414 -
   1.415 -            fun build_rel rs' T =
   1.416 -              (case find_index (curry (op =) T) fpTs of
   1.417 -                ~1 =>
   1.418 -                if exists_subtype_in fpTs T then build_rel_step lthy (build_rel rs') T
   1.419 -                else HOLogic.eq_const T
   1.420 -              | kk => nth rs' kk);
   1.421 -
   1.422 -            fun build_rel_app rs' usel vsel =
   1.423 -              fold rapp [usel, vsel] (build_rel rs' (fastype_of usel));
   1.424 -
   1.425 -            fun mk_prem_ctr_concls rs' n k udisc usels vdisc vsels =
   1.426 -              (if k = n then [] else [HOLogic.mk_eq (udisc, vdisc)]) @
   1.427 -              (if null usels then
   1.428 -                 []
   1.429 -               else
   1.430 -                 [Library.foldr HOLogic.mk_imp (if n = 1 then [] else [udisc, vdisc],
   1.431 -                    Library.foldr1 HOLogic.mk_conj (map2 (build_rel_app rs') usels vsels))]);
   1.432 -
   1.433 -            fun mk_prem_concl rs' n udiscs uselss vdiscs vselss =
   1.434 -              Library.foldr1 HOLogic.mk_conj
   1.435 -                (flat (map5 (mk_prem_ctr_concls rs' n) (1 upto n) udiscs uselss vdiscs vselss))
   1.436 -              handle List.Empty => @{term True};
   1.437 -
   1.438 -            fun mk_prem rs' uvr u v n udiscs uselss vdiscs vselss =
   1.439 -              fold_rev Logic.all [u, v] (Logic.mk_implies (HOLogic.mk_Trueprop uvr,
   1.440 -                HOLogic.mk_Trueprop (mk_prem_concl rs' n udiscs uselss vdiscs vselss)));
   1.441 -
   1.442 -            val concl =
   1.443 -              HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
   1.444 -                (map3 (fn uvr => fn u => fn v => HOLogic.mk_imp (uvr, HOLogic.mk_eq (u, v)))
   1.445 -                   uvrs us vs));
   1.446 -
   1.447 -            fun mk_goal rs' =
   1.448 -              Logic.list_implies (map8 (mk_prem rs') uvrs us vs ns udiscss uselsss vdiscss vselsss,
   1.449 -                concl);
   1.450 -
   1.451 -            val goal = mk_goal rs;
   1.452 -            val strong_goal = mk_goal strong_rs;
   1.453 -
   1.454 -            fun prove dtor_coinduct' goal =
   1.455 -              Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
   1.456 -                mk_coinduct_tac ctxt nesting_rel_eqs nn ns dtor_coinduct' pre_rel_defs dtor_ctors
   1.457 -                  exhaust_thms ctr_defss disc_thmsss sel_thmsss)
   1.458 -              |> singleton (Proof_Context.export names_lthy lthy)
   1.459 -              |> Thm.close_derivation;
   1.460 -
   1.461 -            fun postproc nn thm =
   1.462 -              Thm.permute_prems 0 nn
   1.463 -                (if nn = 1 then thm RS mp
   1.464 -                 else funpow nn (fn thm => reassoc_conjs (thm RS mp_conj)) thm)
   1.465 -              |> Drule.zero_var_indexes
   1.466 -              |> `(conj_dests nn);
   1.467 -          in
   1.468 -            (postproc nn (prove fp_induct goal), postproc nn (prove fp_strong_induct strong_goal))
   1.469 -          end;
   1.470 -
   1.471 -        fun mk_coinduct_concls ms discs ctrs =
   1.472 -          let
   1.473 -            fun mk_disc_concl disc = [name_of_disc disc];
   1.474 -            fun mk_ctr_concl 0 _ = []
   1.475 -              | mk_ctr_concl _ ctor = [name_of_ctr ctor];
   1.476 -            val disc_concls = map mk_disc_concl (fst (split_last discs)) @ [[]];
   1.477 -            val ctr_concls = map2 mk_ctr_concl ms ctrs;
   1.478 -          in
   1.479 -            flat (map2 append disc_concls ctr_concls)
   1.480 -          end;
   1.481 -
   1.482 -        val coinduct_cases = quasi_unambiguous_case_names (map (prefix EqN) fp_b_names);
   1.483 -        val coinduct_conclss =
   1.484 -          map3 (quasi_unambiguous_case_names ooo mk_coinduct_concls) mss discss ctrss;
   1.485 -
   1.486 -        fun mk_maybe_not pos = not pos ? HOLogic.mk_not;
   1.487 -
   1.488 -        val gunfolds = map (lists_bmoc pgss) unfolds;
   1.489 -        val hcorecs = map (lists_bmoc phss) corecs;
   1.490 -
   1.491 -        val (unfold_thmss, corec_thmss, safe_unfold_thmss, safe_corec_thmss) =
   1.492 -          let
   1.493 -            fun mk_goal pfss c cps fcorec_like n k ctr m cfs' =
   1.494 -              fold_rev (fold_rev Logic.all) ([c] :: pfss)
   1.495 -                (Logic.list_implies (seq_conds (HOLogic.mk_Trueprop oo mk_maybe_not) n k cps,
   1.496 -                   mk_Trueprop_eq (fcorec_like $ c, Term.list_comb (ctr, take m cfs'))));
   1.497 +        val ((coinduct_thm, coinduct_thms, strong_coinduct_thm, strong_coinduct_thms,
   1.498 +              coinduct_attrs),
   1.499 +             (unfold_thmss, corec_thmss, corec_like_attrs),
   1.500 +             (safe_unfold_thmss, safe_corec_thmss),
   1.501 +             (disc_unfold_thmss, disc_corec_thmss, disc_corec_like_attrs),
   1.502 +             (disc_unfold_iff_thmss, disc_corec_iff_thmss, disc_corec_like_iff_attrs),
   1.503 +             (sel_unfold_thmss, sel_corec_thmss, sel_corec_like_attrs)) =
   1.504 +          derive_coinduct_unfold_corec_thms_for_types names_lthy0 no_defs_lthy nn fp_b_names
   1.505 +            pre_bnfs fp_induct fp_strong_induct dtor_ctors fp_fold_thms fp_rec_thms nesting_bnfs
   1.506 +            nested_bnfs fpTs Cs As kss mss ns cs cpss pgss crssss cgssss phss csssss chssss info
   1.507 +            lthy;
   1.508  
   1.509 -            fun build_corec_like fcorec_likes (T, U) =
   1.510 -              if T = U then
   1.511 -                id_const T
   1.512 -              else
   1.513 -                (case find_index (curry (op =) U) fpTs of
   1.514 -                  ~1 => build_map lthy (build_corec_like fcorec_likes) T U
   1.515 -                | kk => nth fcorec_likes kk);
   1.516 -
   1.517 -            val mk_U = typ_subst (map2 pair Cs fpTs);
   1.518 -
   1.519 -            fun intr_corec_likes fcorec_likes [] [cf] =
   1.520 -                let val T = fastype_of cf in
   1.521 -                  if exists_subtype_in Cs T then build_corec_like fcorec_likes (T, mk_U T) $ cf
   1.522 -                  else cf
   1.523 -                end
   1.524 -              | intr_corec_likes fcorec_likes [cq] [cf, cf'] =
   1.525 -                mk_If cq (intr_corec_likes fcorec_likes [] [cf])
   1.526 -                  (intr_corec_likes fcorec_likes [] [cf']);
   1.527 -
   1.528 -            val crgsss = map2 (map2 (map2 (intr_corec_likes gunfolds))) crssss cgssss;
   1.529 -            val cshsss = map2 (map2 (map2 (intr_corec_likes hcorecs))) csssss chssss;
   1.530 -
   1.531 -            val unfold_goalss =
   1.532 -              map8 (map4 oooo mk_goal pgss) cs cpss gunfolds ns kss ctrss mss crgsss;
   1.533 -            val corec_goalss =
   1.534 -              map8 (map4 oooo mk_goal phss) cs cpss hcorecs ns kss ctrss mss cshsss;
   1.535 -
   1.536 -            fun mk_map_if_distrib bnf =
   1.537 -              let
   1.538 -                val mapx = map_of_bnf bnf;
   1.539 -                val live = live_of_bnf bnf;
   1.540 -                val ((Ts, T), U) = strip_typeN (live + 1) (fastype_of mapx) |>> split_last;
   1.541 -                val fs = Variable.variant_frees lthy [mapx] (map (pair "f") Ts);
   1.542 -                val t = Term.list_comb (mapx, map (Var o apfst (rpair 0)) fs);
   1.543 -              in
   1.544 -                Drule.instantiate' (map (SOME o certifyT lthy) [U, T]) [SOME (certify lthy t)]
   1.545 -                  @{thm if_distrib}
   1.546 -              end;
   1.547 -
   1.548 -            val nested_map_if_distribs = map mk_map_if_distrib nested_bnfs;
   1.549 -
   1.550 -            val unfold_tacss =
   1.551 -              map3 (map oo mk_corec_like_tac unfold_defs [] [] nesting_map_ids'' [])
   1.552 -                fp_fold_thms pre_map_defs ctr_defss;
   1.553 -            val corec_tacss =
   1.554 -              map3 (map oo mk_corec_like_tac corec_defs nested_map_comps'' nested_map_comp's
   1.555 -                  (nested_map_ids'' @ nesting_map_ids'') nested_map_if_distribs)
   1.556 -                fp_rec_thms pre_map_defs ctr_defss;
   1.557 -
   1.558 -            fun prove goal tac =
   1.559 -              Goal.prove_sorry lthy [] [] goal (tac o #context) |> Thm.close_derivation;
   1.560 -
   1.561 -            val unfold_thmss = map2 (map2 prove) unfold_goalss unfold_tacss;
   1.562 -            val corec_thmss = map2 (map2 prove) corec_goalss corec_tacss;
   1.563 -
   1.564 -            val filter_safesss =
   1.565 -              map2 (map_filter (fn (safes, thm) => if forall I safes then SOME thm else NONE) oo
   1.566 -                curry (op ~~)) (map2 (map2 (map2 (member (op =)))) cgssss crgsss);
   1.567 -
   1.568 -            val safe_unfold_thmss = filter_safesss unfold_thmss;
   1.569 -            val safe_corec_thmss = filter_safesss corec_thmss;
   1.570 -          in
   1.571 -            (unfold_thmss, corec_thmss, safe_unfold_thmss, safe_corec_thmss)
   1.572 -          end;
   1.573 -
   1.574 -        val (disc_unfold_iff_thmss, disc_corec_iff_thmss) =
   1.575 -          let
   1.576 -            fun mk_goal c cps fcorec_like n k disc =
   1.577 -              mk_Trueprop_eq (disc $ (fcorec_like $ c),
   1.578 -                if n = 1 then @{const True}
   1.579 -                else Library.foldr1 HOLogic.mk_conj (seq_conds mk_maybe_not n k cps));
   1.580 -
   1.581 -            val unfold_goalss = map6 (map2 oooo mk_goal) cs cpss gunfolds ns kss discss;
   1.582 -            val corec_goalss = map6 (map2 oooo mk_goal) cs cpss hcorecs ns kss discss;
   1.583 -
   1.584 -            fun mk_case_split' cp =
   1.585 -              Drule.instantiate' [] [SOME (certify lthy cp)] @{thm case_split};
   1.586 -
   1.587 -            val case_splitss' = map (map mk_case_split') cpss;
   1.588 -
   1.589 -            val unfold_tacss =
   1.590 -              map3 (map oo mk_disc_corec_like_iff_tac) case_splitss' unfold_thmss disc_thmsss;
   1.591 -            val corec_tacss =
   1.592 -              map3 (map oo mk_disc_corec_like_iff_tac) case_splitss' corec_thmss disc_thmsss;
   1.593 -
   1.594 -            fun prove goal tac =
   1.595 -              Goal.prove_sorry lthy [] [] goal (tac o #context)
   1.596 -              |> singleton (Proof_Context.export names_lthy0 no_defs_lthy)
   1.597 -              |> Thm.close_derivation;
   1.598 -
   1.599 -            fun proves [_] [_] = []
   1.600 -              | proves goals tacs = map2 prove goals tacs;
   1.601 -          in
   1.602 -            (map2 proves unfold_goalss unfold_tacss,
   1.603 -             map2 proves corec_goalss corec_tacss)
   1.604 -          end;
   1.605 -
   1.606 -        val is_triv_discI = is_triv_implies orf is_concl_refl;
   1.607 -
   1.608 -        fun mk_disc_corec_like_thms corec_likes discIs =
   1.609 -          map (op RS) (filter_out (is_triv_discI o snd) (corec_likes ~~ discIs));
   1.610 -
   1.611 -        val disc_unfold_thmss = map2 mk_disc_corec_like_thms unfold_thmss discIss;
   1.612 -        val disc_corec_thmss = map2 mk_disc_corec_like_thms corec_thmss discIss;
   1.613 -
   1.614 -        fun mk_sel_corec_like_thm corec_like_thm sel sel_thm =
   1.615 -          let
   1.616 -            val (domT, ranT) = dest_funT (fastype_of sel);
   1.617 -            val arg_cong' =
   1.618 -              Drule.instantiate' (map (SOME o certifyT lthy) [domT, ranT])
   1.619 -                [NONE, NONE, SOME (certify lthy sel)] arg_cong
   1.620 -              |> Thm.varifyT_global;
   1.621 -            val sel_thm' = sel_thm RSN (2, trans);
   1.622 -          in
   1.623 -            corec_like_thm RS arg_cong' RS sel_thm'
   1.624 -          end;
   1.625 -
   1.626 -        fun mk_sel_corec_like_thms corec_likess =
   1.627 -          map3 (map3 (map2 o mk_sel_corec_like_thm)) corec_likess selsss sel_thmsss |> map flat;
   1.628 -
   1.629 -        val sel_unfold_thmss = mk_sel_corec_like_thms unfold_thmss;
   1.630 -        val sel_corec_thmss = mk_sel_corec_like_thms corec_thmss;
   1.631 +        fun coinduct_type_attr T_name = Attrib.internal (K (Induct.coinduct_type T_name));
   1.632  
   1.633          fun flat_corec_like_thms corec_likes disc_corec_likes sel_corec_likes =
   1.634            corec_likes @ disc_corec_likes @ sel_corec_likes;
   1.635  
   1.636          val simp_thmss =
   1.637 -          mk_simp_thmss wrap_ress
   1.638 +          mk_simp_thmss ctr_wrap_ress
   1.639              (map3 flat_corec_like_thms safe_corec_thmss disc_corec_thmss sel_corec_thmss)
   1.640              (map3 flat_corec_like_thms safe_unfold_thmss disc_unfold_thmss sel_unfold_thmss);
   1.641  
   1.642 @@ -1188,37 +1228,27 @@
   1.643            [(flat safe_unfold_thmss @ flat safe_corec_thmss, simp_attrs)]
   1.644            |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
   1.645  
   1.646 -        val coinduct_consumes_attr = Attrib.internal (K (Rule_Cases.consumes nn));
   1.647 -        val coinduct_case_names_attr = Attrib.internal (K (Rule_Cases.case_names coinduct_cases));
   1.648 -        val coinduct_case_concl_attrs =
   1.649 -          map2 (fn casex => fn concls =>
   1.650 -              Attrib.internal (K (Rule_Cases.case_conclusion (casex, concls))))
   1.651 -            coinduct_cases coinduct_conclss;
   1.652 -        val coinduct_case_attrs =
   1.653 -          coinduct_consumes_attr :: coinduct_case_names_attr :: coinduct_case_concl_attrs;
   1.654 -        fun coinduct_type_attr T_name = Attrib.internal (K (Induct.coinduct_type T_name));
   1.655 -
   1.656          val common_notes =
   1.657            (if nn > 1 then
   1.658 -             [(coinductN, [coinduct_thm], coinduct_case_attrs),
   1.659 -              (strong_coinductN, [strong_coinduct_thm], coinduct_case_attrs)]
   1.660 +             [(coinductN, [coinduct_thm], coinduct_attrs),
   1.661 +              (strong_coinductN, [strong_coinduct_thm], coinduct_attrs)]
   1.662             else
   1.663               [])
   1.664            |> massage_simple_notes fp_common_name;
   1.665  
   1.666          val notes =
   1.667            [(coinductN, map single coinduct_thms,
   1.668 -            fn T_name => coinduct_case_attrs @ [coinduct_type_attr T_name]),
   1.669 -           (corecN, corec_thmss, K []),
   1.670 -           (disc_corecN, disc_corec_thmss, K simp_attrs),
   1.671 -           (disc_corec_iffN, disc_corec_iff_thmss, K simp_attrs),
   1.672 -           (disc_unfoldN, disc_unfold_thmss, K simp_attrs),
   1.673 -           (disc_unfold_iffN, disc_unfold_iff_thmss, K simp_attrs),
   1.674 -           (sel_corecN, sel_corec_thmss, K simp_attrs),
   1.675 -           (sel_unfoldN, sel_unfold_thmss, K simp_attrs),
   1.676 +            fn T_name => coinduct_attrs @ [coinduct_type_attr T_name]),
   1.677 +           (corecN, corec_thmss, K corec_like_attrs),
   1.678 +           (disc_corecN, disc_corec_thmss, K disc_corec_like_attrs),
   1.679 +           (disc_corec_iffN, disc_corec_iff_thmss, K disc_corec_like_iff_attrs),
   1.680 +           (disc_unfoldN, disc_unfold_thmss, K disc_corec_like_attrs),
   1.681 +           (disc_unfold_iffN, disc_unfold_iff_thmss, K disc_corec_like_iff_attrs),
   1.682 +           (sel_corecN, sel_corec_thmss, K sel_corec_like_attrs),
   1.683 +           (sel_unfoldN, sel_unfold_thmss, K sel_corec_like_attrs),
   1.684             (simpsN, simp_thmss, K []),
   1.685 -           (strong_coinductN, map single strong_coinduct_thms, K coinduct_case_attrs),
   1.686 -           (unfoldN, unfold_thmss, K [])]
   1.687 +           (strong_coinductN, map single strong_coinduct_thms, K coinduct_attrs),
   1.688 +           (unfoldN, unfold_thmss, K corec_like_attrs)]
   1.689            |> massage_multi_notes;
   1.690        in
   1.691          lthy |> Local_Theory.notes (anonymous_notes @ common_notes @ notes) |> snd