1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Fri Sep 14 12:09:27 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Fri Sep 14 12:09:27 2012 +0200
     1.3 @@ -52,7 +52,6 @@
     1.4  val lists_bmoc = fold (fn xs => fn t => Term.list_comb (t, xs));
     1.5  
     1.6  fun mk_id T = Const (@{const_name id}, T --> T);
     1.7 -fun mk_id_fun T = Abs (Name.uu, T, Bound 0);
     1.8  
     1.9  fun mk_tupled_fun x f xs = HOLogic.tupled_lambda x (Term.list_comb (f, xs));
    1.10  fun mk_uncurried_fun f xs = mk_tupled_fun (HOLogic.mk_tuple xs) f xs;
    1.11 @@ -66,8 +65,6 @@
    1.12      Term.lambda z (mk_sum_case (Term.lambda v v, Term.lambda c (f $ c)) $ z)
    1.13    end;
    1.14  
    1.15 -fun fold_def_rule n thm = funpow n (fn thm => thm RS fun_cong) (thm RS meta_eq_to_obj_eq) RS sym;
    1.16 -
    1.17  fun cannot_merge_types () = error "Mutually recursive types must have the same type parameters";
    1.18  
    1.19  fun merge_type_arg T T' = if T = T' then T else cannot_merge_types ();
    1.20 @@ -184,7 +181,7 @@
    1.21              let val (needs, ss') = fold_map add Ts ss in
    1.22                if exists I needs then (true, insert (op =) s ss') else (false, ss')
    1.23              end
    1.24 -          | add T ss = (member (op =) As T, ss);
    1.25 +          | add T ss = (member (op =) Bs T, ss);
    1.26        in snd oo add end;
    1.27  
    1.28      val nested_bnfs =
    1.29 @@ -204,6 +201,9 @@
    1.30      val flds = map (mk_fld As) flds0;
    1.31  
    1.32      val fpTs = map (domain_type o fastype_of) unfs;
    1.33 +
    1.34 +    val exists_fp_subtype = exists_subtype (member (op =) fpTs);
    1.35 +
    1.36      val vs = map2 (curry Free) vs' fpTs;
    1.37  
    1.38      val ctr_Tsss = map (map (map (Term.typ_subst_atomic (Bs ~~ fpTs)))) ctr_TsssBs;
    1.39 @@ -516,34 +516,76 @@
    1.40      fun derive_induct_iter_rec_thms_for_types ((ctrss, _, iters, recs, vs, xsss, ctr_defss, _, _,
    1.41          iter_defs, rec_defs), lthy) =
    1.42        let
    1.43 +        fun mk_sets_nested bnf =
    1.44 +          let
    1.45 +            val Type (T_name, Us) = T_of_bnf bnf;
    1.46 +            val lives = lives_of_bnf bnf;
    1.47 +            val sets = sets_of_bnf bnf;
    1.48 +            fun mk_set U =
    1.49 +              (case find_index (curry (op =) U) lives of
    1.50 +                ~1 => Term.dummy
    1.51 +              | i => nth sets i);
    1.52 +          in
    1.53 +            (T_name, map mk_set Us)
    1.54 +          end;
    1.55 +
    1.56 +        val setss_nested = map mk_sets_nested nested_bnfs;
    1.57 +
    1.58          val (induct_thms, induct_thm) =
    1.59            let
    1.60 -            val (ps, names_lthy) =
    1.61 +            val ((phis, phis'), names_lthy) =
    1.62                lthy
    1.63 -              |> mk_Frees "P" (map mk_predT fpTs);
    1.64 +              |> mk_Frees' "P" (map mk_predT fpTs);
    1.65  
    1.66 -            fun mk_prem_prem (x as Free (_, T)) =
    1.67 -              map HOLogic.mk_Trueprop
    1.68 +            fun mk_set Ts t =
    1.69 +              let val Type (_, Ts0) = domain_type (fastype_of t) in
    1.70 +                Term.subst_atomic_types (Ts0 ~~ Ts) t
    1.71 +              end;
    1.72 +
    1.73 +            fun mk_prem_prems names_lthy (x as Free (s, T as Type (T_name, Ts0))) =
    1.74                  (case find_index (curry (op =) T) fpTs of
    1.75 -                  ~1 => []
    1.76 -                | i => [nth ps i $ x]);
    1.77 +                  ~1 =>
    1.78 +                  (case AList.lookup (op =) setss_nested T_name of
    1.79 +                    NONE => []
    1.80 +                  | SOME raw_sets0 =>
    1.81 +                    let
    1.82 +                      val (Ts, raw_sets) =
    1.83 +                        split_list (filter (exists_fp_subtype o fst) (Ts0 ~~ raw_sets0));
    1.84 +                      val sets = map (mk_set Ts0) raw_sets;
    1.85 +                      val (ys, names_lthy') = names_lthy |> mk_Frees s Ts;
    1.86 +                      val heads =
    1.87 +                        map2 (fn y => fn set => HOLogic.mk_Trueprop (HOLogic.mk_mem (y, set $ x)))
    1.88 +                          ys sets;
    1.89 +                      val bodies = flat (map (mk_prem_prems names_lthy') ys);
    1.90 +                    in
    1.91 +                      map2 (curry Logic.mk_implies) heads bodies
    1.92 +                    end)
    1.93 +                | i => [HOLogic.mk_Trueprop (nth phis i $ x)])
    1.94 +              | mk_prem_prems _ _ = [];
    1.95  
    1.96 -            fun mk_prem p ctr ctr_Ts =
    1.97 -              let val (xs, _) = names_lthy |> mk_Frees "x" ctr_Ts in
    1.98 +            fun close_prem_prem (Free x') t =
    1.99 +              fold_rev Logic.all (map Free (drop (N + 1) (rev (Term.add_frees t (x' :: phis'))))) t;
   1.100 +
   1.101 +            fun mk_prem phi ctr ctr_Ts =
   1.102 +              let
   1.103 +                val (xs, names_lthy') = names_lthy |> mk_Frees "x" ctr_Ts;
   1.104 +                val prem_prems =
   1.105 +                  maps (fn x => map (close_prem_prem x) (mk_prem_prems names_lthy' x)) xs;
   1.106 +              in
   1.107                  fold_rev Logic.all xs
   1.108 -                  (Logic.list_implies (maps mk_prem_prem xs,
   1.109 -                     HOLogic.mk_Trueprop (p $ Term.list_comb (ctr, xs))))
   1.110 +                  (Logic.list_implies (prem_prems,
   1.111 +                     HOLogic.mk_Trueprop (phi $ Term.list_comb (ctr, xs))))
   1.112                end;
   1.113  
   1.114              val goal =
   1.115 -              fold_rev (fold_rev Logic.all) [ps, vs]
   1.116 -                (Library.foldr Logic.list_implies (map3 (map2 o mk_prem) ps ctrss ctr_Tsss,
   1.117 +              fold_rev (fold_rev Logic.all) [phis, vs]
   1.118 +                (Library.foldr Logic.list_implies (map3 (map2 o mk_prem) phis ctrss ctr_Tsss,
   1.119                     HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
   1.120 -                     (map2 (curry (op $)) ps vs))));
   1.121 +                     (map2 (curry (op $)) phis vs))));
   1.122  
   1.123              val induct_thm =
   1.124                Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
   1.125 -                Skip_Proof.cheat_tac (Proof_Context.theory_of ctxt));
   1.126 +                mk_induct_tac ctxt);
   1.127            in
   1.128              `(conj_dests N) induct_thm
   1.129            end;
   1.130 @@ -572,7 +614,7 @@
   1.131              fun intr_calls fiter_likes maybe_cons maybe_tick maybe_mk_prodT (x as Free (_, T)) =
   1.132                if member (op =) fpTs T then
   1.133                  maybe_cons x [build_call fiter_likes (K I) (T, mk_U (K I) T) $ x]
   1.134 -              else if exists_subtype (member (op =) fpTs) T then
   1.135 +              else if exists_fp_subtype T then
   1.136                  [build_call fiter_likes maybe_tick (T, mk_U maybe_mk_prodT T) $ x]
   1.137                else
   1.138                  [x];

     2.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Fri Sep 14 12:09:27 2012 +0200
     2.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Fri Sep 14 12:09:27 2012 +0200
     2.3 @@ -13,6 +13,7 @@
     2.4    val mk_fld_iff_unf_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm
     2.5      -> tactic
     2.6    val mk_half_distinct_tac: Proof.context -> thm -> thm list -> tactic
     2.7 +  val mk_induct_tac: Proof.context -> tactic
     2.8    val mk_inject_tac: Proof.context -> thm -> thm -> tactic
     2.9    val mk_iter_like_tac: thm list -> thm list -> thm list -> thm -> thm -> Proof.context -> tactic
    2.10  end;
    2.11 @@ -51,6 +52,9 @@
    2.12    Local_Defs.unfold_tac ctxt [ctr_def] THEN rtac (fld_inject RS ssubst) 1 THEN
    2.13    Local_Defs.unfold_tac ctxt @{thms sum.inject Pair_eq conj_assoc} THEN rtac refl 1;
    2.14  
    2.15 +fun mk_induct_tac ctxt =
    2.16 +  Skip_Proof.cheat_tac (Proof_Context.theory_of ctxt)(*###*);
    2.17 +
    2.18  val iter_like_thms =
    2.19    @{thms case_unit comp_def convol_def id_apply map_pair_def sum.simps(5,6) sum_map.simps
    2.20        split_conv};
    2.21 @@ -67,6 +71,6 @@
    2.22    subst_tac ctxt [fld_unf_coiter_like] 1 THEN asm_simp_tac coiter_like_ss 1 THEN
    2.23    Local_Defs.unfold_tac ctxt (pre_map_def :: coiter_like_thms @ map_ids) THEN
    2.24    Local_Defs.unfold_tac ctxt @{thms id_def} THEN
    2.25 -  (rtac refl ORELSE' subst_tac ctxt @{thms unit_eq} THEN' rtac refl) 1;
    2.26 +  TRY ((rtac refl ORELSE' subst_tac ctxt @{thms unit_eq} THEN' rtac refl) 1);
    2.27  
    2.28  end;

     3.1 --- a/src/HOL/Codatatype/Tools/bnf_gfp.ML	Fri Sep 14 12:09:27 2012 +0200
     3.2 +++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML	Fri Sep 14 12:09:27 2012 +0200
     3.3 @@ -1873,7 +1873,7 @@
     3.4        ||>> mk_Frees "f" coiter_fTs
     3.5        ||>> mk_Frees "g" coiter_fTs
     3.6        ||>> mk_Frees "s" corec_sTs
     3.7 -      ||>> mk_Frees "phi" (map (fn T => T --> mk_predT T) Ts);
     3.8 +      ||>> mk_Frees "P" (map (fn T => T --> mk_predT T) Ts);
     3.9  
    3.10      fun unf_bind i = Binding.suffix_name ("_" ^ unfN) (nth bs (i - 1));
    3.11      val unf_name = Binding.name_of o unf_bind;
    3.12 @@ -2309,9 +2309,9 @@
    3.13            ||>> mk_Frees "u" uTs
    3.14            ||>> mk_Frees' "b" Ts'
    3.15            ||>> mk_Frees' "b" Ts'
    3.16 -          ||>> mk_Freess "phi" (map (fn T => map (fn U => T --> mk_predT U) Ts) passiveAs)
    3.17 +          ||>> mk_Freess "P" (map (fn T => map (fn U => T --> mk_predT U) Ts) passiveAs)
    3.18            ||>> mk_Frees "R" JRTs
    3.19 -          ||>> mk_Frees "phi" JphiTs
    3.20 +          ||>> mk_Frees "P" JphiTs
    3.21            ||>> mk_Frees "B1" B1Ts
    3.22            ||>> mk_Frees "B2" B2Ts
    3.23            ||>> mk_Frees "A" AXTs

     4.1 --- a/src/HOL/Codatatype/Tools/bnf_lfp.ML	Fri Sep 14 12:09:27 2012 +0200
     4.2 +++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML	Fri Sep 14 12:09:27 2012 +0200
     4.3 @@ -794,7 +794,7 @@
     4.4        ||>> mk_Frees' "x" init_FTs
     4.5        ||>> mk_Frees "f" init_fTs
     4.6        ||>> mk_Frees "f" init_fTs
     4.7 -      ||>> mk_Frees "phi" (replicate n (mk_predT initT));
     4.8 +      ||>> mk_Frees "P" (replicate n (mk_predT initT));
     4.9  
    4.10      val II = HOLogic.mk_Collect (fst iidx', IIT, list_exists_free (II_Bs @ II_ss)
    4.11        (HOLogic.mk_conj (HOLogic.mk_eq (iidx,
    4.12 @@ -1374,7 +1374,7 @@
    4.13            ||>> mk_Frees "p2" p2Ts
    4.14            ||>> mk_Frees' "y" passiveAs
    4.15            ||>> mk_Frees "R" IRTs
    4.16 -          ||>> mk_Frees "phi" IphiTs;
    4.17 +          ||>> mk_Frees "P" IphiTs;
    4.18  
    4.19          val map_FTFT's = map2 (fn Ds =>
    4.20            mk_map_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;