started work on generation of "rel" theorems
authorblanchet
Sun Sep 23 14:52:53 2012 +0200 (2012-09-23)
changeset 49536898aea2e7a94
parent 49535 e016736fbe0a
child 49537 fe1deee434b6
started work on generation of "rel" theorems
src/HOL/BNF/Tools/bnf_def.ML
src/HOL/BNF/Tools/bnf_fp.ML
src/HOL/BNF/Tools/bnf_fp_sugar.ML
src/HOL/BNF/Tools/bnf_gfp.ML
src/HOL/BNF/Tools/bnf_lfp.ML
src/HOL/BNF/Tools/bnf_util.ML
src/HOL/BNF/Tools/bnf_wrap.ML
     1.1 --- a/src/HOL/BNF/Tools/bnf_def.ML	Sun Sep 23 08:24:19 2012 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_def.ML	Sun Sep 23 14:52:53 2012 +0200
     1.3 @@ -692,9 +692,9 @@
     1.4        ||>> mk_Frees "p1" (map2 (curry (op -->)) domTs B1Ts)
     1.5        ||>> mk_Frees "p2" (map2 (curry (op -->)) domTs B2Ts)
     1.6        ||>> mk_Frees "b" As'
     1.7 -      ||>> mk_Frees' "R" setRTs
     1.8 -      ||>> mk_Frees "R" setRTs
     1.9 -      ||>> mk_Frees "S" setRTsBsCs
    1.10 +      ||>> mk_Frees' "S" setRTs
    1.11 +      ||>> mk_Frees "S" setRTs
    1.12 +      ||>> mk_Frees "T" setRTsBsCs
    1.13        ||>> mk_Frees' "Q" QTs;
    1.14  
    1.15      (*Gr (in R1 .. Rn) (map fst .. fst)^-1 O Gr (in R1 .. Rn) (map snd .. snd)*)
     2.1 --- a/src/HOL/BNF/Tools/bnf_fp.ML	Sun Sep 23 08:24:19 2012 +0200
     2.2 +++ b/src/HOL/BNF/Tools/bnf_fp.ML	Sun Sep 23 14:52:53 2012 +0200
     2.3 @@ -70,9 +70,11 @@
     2.4    val recsN: string
     2.5    val rel_coinductN: string
     2.6    val rel_strong_coinductN: string
     2.7 +  val relsN: string
     2.8    val rvN: string
     2.9 +  val sel_corecsN: string
    2.10 +  val sel_relsN: string
    2.11    val sel_unfoldsN: string
    2.12 -  val sel_corecsN: string
    2.13    val set_inclN: string
    2.14    val set_set_inclN: string
    2.15    val simpsN: string
    2.16 @@ -226,7 +228,6 @@
    2.17  val dtor_coinductN = dtorN ^ "_" ^ coinductN
    2.18  val rel_coinductN = relN ^ "_" ^ coinductN
    2.19  val srel_coinductN = srelN ^ "_" ^ coinductN
    2.20 -val simpN = "_simp";
    2.21  val ctor_srelN = ctorN ^ "_" ^ srelN
    2.22  val dtor_srelN = dtorN ^ "_" ^ srelN
    2.23  val ctor_relN = ctorN ^ "_" ^ relN
    2.24 @@ -247,7 +248,9 @@
    2.25  val iffN = "_iff"
    2.26  val disc_unfold_iffN = discN ^ "_" ^ unfoldN ^ iffN
    2.27  val disc_corec_iffN = discN ^ "_" ^ corecN ^ iffN
    2.28 +val relsN = relN ^ "s"
    2.29  val selN = "sel"
    2.30 +val sel_relsN = selN ^ "_" ^ relsN
    2.31  val sel_unfoldsN = selN ^ "_" ^ unfoldsN
    2.32  val sel_corecsN = selN ^ "_" ^ corecsN
    2.33  
     3.1 --- a/src/HOL/BNF/Tools/bnf_fp_sugar.ML	Sun Sep 23 08:24:19 2012 +0200
     3.2 +++ b/src/HOL/BNF/Tools/bnf_fp_sugar.ML	Sun Sep 23 14:52:53 2012 +0200
     3.3 @@ -7,19 +7,19 @@
     3.4  
     3.5  signature BNF_FP_SUGAR =
     3.6  sig
     3.7 -  val datatyp: bool ->
     3.8 +  val datatypes: bool ->
     3.9      (mixfix list -> (string * sort) list option -> binding list -> typ list * typ list list ->
    3.10        BNF_Def.BNF list -> local_theory ->
    3.11 -      (term list * term list * term list * term list * thm * thm list * thm list * thm list *
    3.12 -         thm list * thm list) * local_theory) ->
    3.13 +      (term list * term list * term list *term list * term list * thm * thm list * thm list *
    3.14 +         thm list * thm list * thm list) * local_theory) ->
    3.15      bool * ((((typ * sort) list * binding) * mixfix) * ((((binding * binding) *
    3.16        (binding * typ) list) * (binding * term) list) * mixfix) list) list ->
    3.17      local_theory -> local_theory
    3.18    val parse_datatype_cmd: bool ->
    3.19      (mixfix list -> (string * sort) list option -> binding list -> typ list * typ list list ->
    3.20        BNF_Def.BNF list -> local_theory ->
    3.21 -      (term list * term list * term list * term list * thm * thm list * thm list * thm list *
    3.22 -         thm list * thm list) * local_theory) ->
    3.23 +      (term list * term list * term list * term list * term list * thm * thm list * thm list *
    3.24 +         thm list * thm list * thm list) * local_theory) ->
    3.25      (local_theory -> local_theory) parser
    3.26  end;
    3.27  
    3.28 @@ -34,8 +34,9 @@
    3.29  
    3.30  val simp_attrs = @{attributes [simp]};
    3.31  
    3.32 -fun split_list8 xs =
    3.33 -  (map #1 xs, map #2 xs, map #3 xs, map #4 xs, map #5 xs, map #6 xs, map #7 xs, map #8 xs);
    3.34 +fun split_list9 xs =
    3.35 +  (map #1 xs, map #2 xs, map #3 xs, map #4 xs, map #5 xs, map #6 xs, map #7 xs, map #8 xs,
    3.36 +   map #9 xs);
    3.37  
    3.38  fun resort_tfree S (TFree (s, _)) = TFree (s, S);
    3.39  
    3.40 @@ -52,6 +53,38 @@
    3.41  fun mk_uncurried2_fun f xss =
    3.42    mk_tupled_fun (HOLogic.mk_tuple (map HOLogic.mk_tuple xss)) f (flat xss);
    3.43  
    3.44 +fun mk_ctor_or_dtor get_T Ts t =
    3.45 +  let val Type (_, Ts0) = get_T (fastype_of t) in
    3.46 +    Term.subst_atomic_types (Ts0 ~~ Ts) t
    3.47 +  end;
    3.48 +
    3.49 +val mk_ctor = mk_ctor_or_dtor range_type;
    3.50 +val mk_dtor = mk_ctor_or_dtor domain_type;
    3.51 +
    3.52 +fun mk_rec_like lfp Ts Us t =
    3.53 +  let
    3.54 +    val (bindings, body) = strip_type (fastype_of t);
    3.55 +    val (f_Us, prebody) = split_last bindings;
    3.56 +    val Type (_, Ts0) = if lfp then prebody else body;
    3.57 +    val Us0 = distinct (op =) (map (if lfp then body_type else domain_type) f_Us);
    3.58 +  in
    3.59 +    Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
    3.60 +  end;
    3.61 +
    3.62 +fun mk_map live Ts Us t =
    3.63 +  let val (Type (_, Ts0), Type (_, Us0)) = strip_typeN (live + 1) (fastype_of t) |>> List.last in
    3.64 +    Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
    3.65 +  end;
    3.66 +
    3.67 +fun mk_rel Ts Us t =
    3.68 +  let
    3.69 +    val ((Type (_, Ts0), Type (_, Us0)), body) =
    3.70 +      strip_type (fastype_of t) |>> split_last |>> apfst List.last;
    3.71 +val _ = tracing ("*** " ^ PolyML.makestring (Ts, "***", Us, "***", t, Ts0, Us0)) (*###*)
    3.72 +  in
    3.73 +    Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
    3.74 +  end;
    3.75 +
    3.76  fun tick u f = Term.lambda u (HOLogic.mk_prod (u, f $ u));
    3.77  
    3.78  fun tack z_name (c, u) f =
    3.79 @@ -81,7 +114,7 @@
    3.80  fun defaults_of ((_, ds), _) = ds;
    3.81  fun ctr_mixfix_of (_, mx) = mx;
    3.82  
    3.83 -fun define_datatype prepare_constraint prepare_typ prepare_term lfp construct (no_dests, specs)
    3.84 +fun define_datatypes prepare_constraint prepare_typ prepare_term lfp construct (no_dests, specs)
    3.85      no_defs_lthy0 =
    3.86    let
    3.87      (* TODO: sanity checks on arguments *)
    3.88 @@ -104,7 +137,7 @@
    3.89      val unsorted_Ass0 = map (map (resort_tfree HOLogic.typeS)) Ass0;
    3.90      val unsorted_As = Library.foldr1 merge_type_args unsorted_Ass0;
    3.91  
    3.92 -    val ((Bs, Cs), no_defs_lthy) =
    3.93 +    val ((Xs, Cs), no_defs_lthy) =
    3.94        no_defs_lthy0
    3.95        |> fold (Variable.declare_typ o resort_tfree dummyS) unsorted_As
    3.96        |> mk_TFrees nn
    3.97 @@ -160,16 +193,16 @@
    3.98        | eq_fpT _ _ = false;
    3.99  
   3.100      fun freeze_fp (T as Type (s, Us)) =
   3.101 -        (case find_index (eq_fpT T) fake_Ts of ~1 => Type (s, map freeze_fp Us) | j => nth Bs j)
   3.102 +        (case find_index (eq_fpT T) fake_Ts of ~1 => Type (s, map freeze_fp Us) | j => nth Xs j)
   3.103        | freeze_fp T = T;
   3.104  
   3.105 -    val ctr_TsssBs = map (map (map freeze_fp)) fake_ctr_Tsss;
   3.106 -    val ctr_sum_prod_TsBs = map (mk_sumTN_balanced o map HOLogic.mk_tupleT) ctr_TsssBs;
   3.107 +    val ctr_TsssXs = map (map (map freeze_fp)) fake_ctr_Tsss;
   3.108 +    val ctr_sum_prod_TsXs = map (mk_sumTN_balanced o map HOLogic.mk_tupleT) ctr_TsssXs;
   3.109  
   3.110      val fp_eqs =
   3.111 -      map dest_TFree Bs ~~ map (Term.typ_subst_atomic (As ~~ unsorted_As)) ctr_sum_prod_TsBs;
   3.112 +      map dest_TFree Xs ~~ map (Term.typ_subst_atomic (As ~~ unsorted_As)) ctr_sum_prod_TsXs;
   3.113  
   3.114 -    val (pre_bnfs, ((dtors0, ctors0, fp_folds0, fp_recs0, fp_induct, dtor_ctors, ctor_dtors,
   3.115 +    val (pre_bnfs, ((dtors0, ctors0, rels0, fp_folds0, fp_recs0, fp_induct, dtor_ctors, ctor_dtors,
   3.116             ctor_injects, fp_fold_thms, fp_rec_thms), lthy)) =
   3.117        fp_bnf construct fp_bs mixfixes (map dest_TFree unsorted_As) fp_eqs no_defs_lthy0;
   3.118  
   3.119 @@ -183,46 +216,29 @@
   3.120        in snd oo add end;
   3.121  
   3.122      fun nesty_bnfs Us =
   3.123 -      map_filter (bnf_of lthy) (fold (fold (fold (add_nesty_bnf_names Us))) ctr_TsssBs []);
   3.124 +      map_filter (bnf_of lthy) (fold (fold (fold (add_nesty_bnf_names Us))) ctr_TsssXs []);
   3.125  
   3.126      val nesting_bnfs = nesty_bnfs As;
   3.127 -    val nested_bnfs = nesty_bnfs Bs;
   3.128 +    val nested_bnfs = nesty_bnfs Xs;
   3.129  
   3.130      val timer = time (Timer.startRealTimer ());
   3.131  
   3.132 -    fun mk_ctor_or_dtor get_T Ts t =
   3.133 -      let val Type (_, Ts0) = get_T (fastype_of t) in
   3.134 -        Term.subst_atomic_types (Ts0 ~~ Ts) t
   3.135 -      end;
   3.136 -
   3.137 -    val mk_ctor = mk_ctor_or_dtor range_type;
   3.138 -    val mk_dtor = mk_ctor_or_dtor domain_type;
   3.139 -
   3.140      val ctors = map (mk_ctor As) ctors0;
   3.141      val dtors = map (mk_dtor As) dtors0;
   3.142 +    val rels = map (mk_rel As As) rels0; (*FIXME*)
   3.143  
   3.144      val fpTs = map (domain_type o fastype_of) dtors;
   3.145  
   3.146      val exists_fp_subtype = exists_subtype (member (op =) fpTs);
   3.147  
   3.148 -    val ctr_Tsss = map (map (map (Term.typ_subst_atomic (Bs ~~ fpTs)))) ctr_TsssBs;
   3.149 +    val ctr_Tsss = map (map (map (Term.typ_subst_atomic (Xs ~~ fpTs)))) ctr_TsssXs;
   3.150      val ns = map length ctr_Tsss;
   3.151      val kss = map (fn n => 1 upto n) ns;
   3.152      val mss = map (map length) ctr_Tsss;
   3.153      val Css = map2 replicate ns Cs;
   3.154  
   3.155 -    fun mk_rec_like Ts Us t =
   3.156 -      let
   3.157 -        val (bindings, body) = strip_type (fastype_of t);
   3.158 -        val (f_Us, prebody) = split_last bindings;
   3.159 -        val Type (_, Ts0) = if lfp then prebody else body;
   3.160 -        val Us0 = distinct (op =) (map (if lfp then body_type else domain_type) f_Us);
   3.161 -      in
   3.162 -        Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
   3.163 -      end;
   3.164 -
   3.165 -    val fp_folds as fp_fold1 :: _ = map (mk_rec_like As Cs) fp_folds0;
   3.166 -    val fp_recs as fp_rec1 :: _ = map (mk_rec_like As Cs) fp_recs0;
   3.167 +    val fp_folds as fp_fold1 :: _ = map (mk_rec_like lfp As Cs) fp_folds0;
   3.168 +    val fp_recs as fp_rec1 :: _ = map (mk_rec_like lfp As Cs) fp_recs0;
   3.169  
   3.170      val fp_fold_fun_Ts = fst (split_last (binder_types (fastype_of fp_fold1)));
   3.171      val fp_rec_fun_Ts = fst (split_last (binder_types (fastype_of fp_rec1)));
   3.172 @@ -340,11 +356,12 @@
   3.173          val ctr_sum_prod_T = mk_sumTN_balanced ctr_prod_Ts;
   3.174          val case_Ts = map (fn Ts => Ts ---> C) ctr_Tss;
   3.175  
   3.176 -        val ((((w, fs), xss), u'), _) =
   3.177 +        val (((((w, fs), xss), yss), u'), _) =
   3.178            no_defs_lthy
   3.179            |> yield_singleton (mk_Frees "w") dtorT
   3.180            ||>> mk_Frees "f" case_Ts
   3.181            ||>> mk_Freess "x" ctr_Tss
   3.182 +          ||>> mk_Freess "y" ctr_Tss
   3.183            ||>> yield_singleton Variable.variant_fixes fp_b_name;
   3.184  
   3.185          val u = Free (u', fpT);
   3.186 @@ -443,9 +460,9 @@
   3.187  
   3.188              val [fold_def, rec_def] = map (Morphism.thm phi) defs;
   3.189  
   3.190 -            val [foldx, recx] = map (mk_rec_like As Cs o Morphism.term phi) csts;
   3.191 +            val [foldx, recx] = map (mk_rec_like lfp As Cs o Morphism.term phi) csts;
   3.192            in
   3.193 -            ((wrap_res, ctrs, foldx, recx, xss, ctr_defs, fold_def, rec_def), lthy)
   3.194 +            ((wrap_res, ctrs, foldx, recx, xss, yss, ctr_defs, fold_def, rec_def), lthy)
   3.195            end;
   3.196  
   3.197          fun define_unfold_corec (wrap_res, no_defs_lthy) =
   3.198 @@ -483,9 +500,9 @@
   3.199  
   3.200              val [unfold_def, corec_def] = map (Morphism.thm phi) defs;
   3.201  
   3.202 -            val [unfold, corec] = map (mk_rec_like As Cs o Morphism.term phi) csts;
   3.203 +            val [unfold, corec] = map (mk_rec_like lfp As Cs o Morphism.term phi) csts;
   3.204            in
   3.205 -            ((wrap_res, ctrs, unfold, corec, xss, ctr_defs, unfold_def, corec_def), lthy)
   3.206 +            ((wrap_res, ctrs, unfold, corec, xss, yss, ctr_defs, unfold_def, corec_def), lthy)
   3.207            end;
   3.208  
   3.209          fun wrap lthy =
   3.210 @@ -500,20 +517,13 @@
   3.211        end;
   3.212  
   3.213      fun wrap_types_and_define_rec_likes ((wraps, define_rec_likess), lthy) =
   3.214 -      fold_map2 (curry (op o)) define_rec_likess wraps lthy |>> split_list8
   3.215 +      fold_map2 (curry (op o)) define_rec_likess wraps lthy |>> split_list9
   3.216  
   3.217      val pre_map_defs = map map_def_of_bnf pre_bnfs;
   3.218      val pre_set_defss = map set_defs_of_bnf pre_bnfs;
   3.219      val nested_set_natural's = maps set_natural'_of_bnf nested_bnfs;
   3.220      val nesting_map_ids = map map_id_of_bnf nesting_bnfs;
   3.221  
   3.222 -    fun mk_map live Ts Us t =
   3.223 -      let
   3.224 -        val (Type (_, Ts0), Type (_, Us0)) = strip_typeN (live + 1) (fastype_of t) |>> List.last
   3.225 -      in
   3.226 -        Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
   3.227 -      end;
   3.228 -
   3.229      fun build_map build_arg (Type (s, Ts)) (Type (_, Us)) =
   3.230        let
   3.231          val bnf = the (bnf_of lthy s);
   3.232 @@ -527,7 +537,7 @@
   3.233        map3 (fn (_, _, injects, distincts, cases, _, _, _) => fn rec_likes => fn fold_likes =>
   3.234          injects @ distincts @ cases @ rec_likes @ fold_likes);
   3.235  
   3.236 -    fun derive_induct_fold_rec_thms_for_types ((wrap_ress, ctrss, folds, recs, xsss, ctr_defss,
   3.237 +    fun derive_induct_fold_rec_thms_for_types ((wrap_ress, ctrss, folds, recs, xsss, _, ctr_defss,
   3.238          fold_defs, rec_defs), lthy) =
   3.239        let
   3.240          val (((phis, phis'), us'), names_lthy) =
   3.241 @@ -683,7 +693,7 @@
   3.242              fn T_name => [induct_case_names_attr, induct_type_attr T_name]),
   3.243             (foldsN, fold_thmss, K (Code.add_default_eqn_attrib :: simp_attrs)),
   3.244             (recsN, rec_thmss, K (Code.add_default_eqn_attrib :: simp_attrs)),
   3.245 -           (simpsN, simp_thmss, K [])]
   3.246 +           (simpsN, simp_thmss, K [])] (* TODO: Add relator simps *)
   3.247            |> maps (fn (thmN, thmss, attrs) =>
   3.248              map3 (fn b => fn Type (T_name, _) => fn thms =>
   3.249                ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), attrs T_name),
   3.250 @@ -692,7 +702,7 @@
   3.251          lthy |> Local_Theory.notes (common_notes @ notes) |> snd
   3.252        end;
   3.253  
   3.254 -    fun derive_coinduct_unfold_corec_thms_for_types ((wrap_ress, ctrss, unfolds, corecs, _,
   3.255 +    fun derive_coinduct_unfold_corec_thms_for_types ((wrap_ress, ctrss, unfolds, corecs, _, _,
   3.256          ctr_defss, unfold_defs, corec_defs), lthy) =
   3.257        let
   3.258          val discss = map (map (mk_disc_or_sel As) o #1) wrap_ress;
   3.259 @@ -864,7 +874,7 @@
   3.260             (disc_corecsN, disc_corec_thmss, simp_attrs),
   3.261             (sel_unfoldsN, sel_unfold_thmss, simp_attrs),
   3.262             (sel_corecsN, sel_corec_thmss, simp_attrs),
   3.263 -           (simpsN, simp_thmss, []),
   3.264 +           (simpsN, simp_thmss, []), (* TODO: Add relator simps *)
   3.265             (unfoldsN, unfold_thmss, [])]
   3.266            |> maps (fn (thmN, thmss, attrs) =>
   3.267              map_filter (fn (_, []) => NONE | (b, thms) =>
   3.268 @@ -874,9 +884,76 @@
   3.269          lthy |> Local_Theory.notes (anonymous_notes @ common_notes @ notes) |> snd
   3.270        end;
   3.271  
   3.272 -    fun derive_pred_thms_for_types ((wrap_ress, ctrss, unfolds, corecs, _, ctr_defss, unfold_defs,
   3.273 -        corec_defs), lthy) =
   3.274 -      lthy;
   3.275 +    fun derive_rel_thms_for_types ((wrap_ress, ctrss, unfolds, corecs, xsss, ysss, ctr_defss,
   3.276 +        unfold_defs, corec_defs), lthy) =
   3.277 +      let
   3.278 +        val selsss = map #2 wrap_ress;
   3.279 +
   3.280 +        val theta_Ts =  [] (*###*)
   3.281 +
   3.282 +        val (thetas, _) =
   3.283 +          lthy
   3.284 +          |> mk_Frees "Q" (map mk_pred1T theta_Ts);
   3.285 +
   3.286 +        val (rel_thmss, rel_thmsss) =
   3.287 +          let
   3.288 +            val xctrss = map2 (map2 (curry Term.list_comb)) ctrss xsss;
   3.289 +            val yctrss = map2 (map2 (curry Term.list_comb)) ctrss ysss;
   3.290 +            val threls = map (fold_rev rapp thetas) rels;
   3.291 +
   3.292 +            fun mk_goal threl (xctr, xs) (yctr, ys) =
   3.293 +              let
   3.294 +                val lhs = threl $ xctr $ yctr;
   3.295 +
   3.296 +                (* ### fixme: lift rel *)
   3.297 +                fun mk_conjunct x y = HOLogic.mk_eq (x, y);
   3.298 +
   3.299 +                fun mk_rhs () =
   3.300 +                  Library.foldr1 HOLogic.mk_conj (map2 mk_conjunct xs ys);
   3.301 +              in
   3.302 +                HOLogic.mk_Trueprop
   3.303 +                  (if Term.head_of xctr = Term.head_of yctr then
   3.304 +                     if null xs then
   3.305 +                       lhs
   3.306 +                     else
   3.307 +                       HOLogic.mk_eq (lhs, mk_rhs ())
   3.308 +                   else
   3.309 +                     HOLogic.mk_not lhs)
   3.310 +              end;
   3.311 +
   3.312 +(*###*)
   3.313 +          (* TODO: Prove and exploit symmetry of relators to halve the number of goals. *)
   3.314 +          fun mk_goals threl xctrs xss yctrs yss =
   3.315 +            map_product (mk_goal threl) (xctrs ~~ xss) (yctrs ~~ yss);
   3.316 +
   3.317 +          val goalsss = map5 mk_goals threls xctrss xsss yctrss ysss;
   3.318 +
   3.319 +(*###
   3.320 +            val goalsss = map6 (fn threl =>
   3.321 +              map5 (fn xctr => fn xs => fn sels =>
   3.322 +                map2 (mk_goal threl xctr xs sels))) threls xctrss xsss selsss yctrss ysss;
   3.323 +*)
   3.324 +val _ = tracing ("goalsss: " ^ PolyML.makestring goalsss) (*###*)
   3.325 +          in
   3.326 +            ([], [])
   3.327 +          end;
   3.328 +
   3.329 +        val (sel_rel_thmss, sel_rel_thmsss) =
   3.330 +          let
   3.331 +          in
   3.332 +            ([], [])
   3.333 +          end;
   3.334 +
   3.335 +        val notes =
   3.336 +          [(* (relsN, rel_thmss, []),
   3.337 +           (sel_relsN, sel_rel_thmss, []) *)]
   3.338 +          |> maps (fn (thmN, thmss, attrs) =>
   3.339 +            map2 (fn b => fn thms =>
   3.340 +                ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), attrs),
   3.341 +              [(thms, [])])) fp_bs thmss);
   3.342 +      in
   3.343 +        lthy |> Local_Theory.notes notes |> snd
   3.344 +      end;
   3.345  
   3.346      val lthy' = lthy
   3.347        |> fold_map define_ctrs_case_for_type (fp_bs ~~ fpTs ~~ Cs ~~ ctors ~~ dtors ~~ fp_folds ~~
   3.348 @@ -886,7 +963,7 @@
   3.349        |> `(if lfp then derive_induct_fold_rec_thms_for_types
   3.350             else derive_coinduct_unfold_corec_thms_for_types)
   3.351        |> swap |>> fst
   3.352 -      |> derive_pred_thms_for_types;
   3.353 +      |> (if null rels then snd else derive_rel_thms_for_types);
   3.354  
   3.355      val timer = time (timer ("Constructors, discriminators, selectors, etc., for the new " ^
   3.356        (if lfp then "" else "co") ^ "datatype"));
   3.357 @@ -894,9 +971,9 @@
   3.358      timer; lthy'
   3.359    end;
   3.360  
   3.361 -val datatyp = define_datatype (K I) (K I) (K I);
   3.362 +val datatypes = define_datatypes (K I) (K I) (K I);
   3.363  
   3.364 -val datatype_cmd = define_datatype Typedecl.read_constraint Syntax.parse_typ Syntax.read_term;
   3.365 +val datatype_cmd = define_datatypes Typedecl.read_constraint Syntax.parse_typ Syntax.read_term;
   3.366  
   3.367  val parse_ctr_arg =
   3.368    @{keyword "("} |-- parse_binding_colon -- Parse.typ --| @{keyword ")"} ||
     4.1 --- a/src/HOL/BNF/Tools/bnf_gfp.ML	Sun Sep 23 08:24:19 2012 +0200
     4.2 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Sun Sep 23 14:52:53 2012 +0200
     4.3 @@ -11,8 +11,8 @@
     4.4  sig
     4.5    val bnf_gfp: mixfix list -> (string * sort) list option -> binding list ->
     4.6      typ list * typ list list -> BNF_Def.BNF list -> local_theory ->
     4.7 -    (term list * term list * term list * term list * thm * thm list * thm list * thm list *
     4.8 -      thm list * thm list) * local_theory
     4.9 +    (term list * term list * term list * term list * term list * thm * thm list * thm list *
    4.10 +      thm list * thm list * thm list) * local_theory
    4.11  end;
    4.12  
    4.13  structure BNF_GFP : BNF_GFP =
    4.14 @@ -2282,7 +2282,7 @@
    4.15      val timer = time (timer "coinduction");
    4.16  
    4.17      (*register new codatatypes as BNFs*)
    4.18 -    val lthy = if m = 0 then lthy else
    4.19 +    val (Jrels, lthy) = if m = 0 then ([], lthy) else
    4.20        let
    4.21          val fTs = map2 (curry op -->) passiveAs passiveBs;
    4.22          val gTs = map2 (curry op -->) passiveBs passiveCs;
    4.23 @@ -2952,7 +2952,7 @@
    4.24                ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
    4.25              bs thmss)
    4.26        in
    4.27 -        timer; lthy |> Local_Theory.notes (Jbnf_common_notes @ Jbnf_notes) |> snd
    4.28 +        timer; (Jrels, lthy |> Local_Theory.notes (Jbnf_common_notes @ Jbnf_notes) |> snd)
    4.29        end;
    4.30  
    4.31        val common_notes =
    4.32 @@ -2983,7 +2983,7 @@
    4.33              ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
    4.34            bs thmss)
    4.35    in
    4.36 -    ((dtors, ctors, unfolds, corecs, dtor_coinduct_thm, dtor_ctor_thms, ctor_dtor_thms,
    4.37 +    ((dtors, ctors, Jrels, unfolds, corecs, dtor_coinduct_thm, dtor_ctor_thms, ctor_dtor_thms,
    4.38        ctor_inject_thms, ctor_dtor_unfold_thms, ctor_dtor_corec_thms),
    4.39       lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
    4.40    end;
     5.1 --- a/src/HOL/BNF/Tools/bnf_lfp.ML	Sun Sep 23 08:24:19 2012 +0200
     5.2 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Sun Sep 23 14:52:53 2012 +0200
     5.3 @@ -10,8 +10,8 @@
     5.4  sig
     5.5    val bnf_lfp: mixfix list -> (string * sort) list option -> binding list ->
     5.6      typ list * typ list list -> BNF_Def.BNF list -> local_theory ->
     5.7 -    (term list * term list * term list * term list * thm * thm list * thm list * thm list *
     5.8 -      thm list * thm list) * local_theory
     5.9 +    (term list * term list * term list * term list * term list * thm * thm list * thm list *
    5.10 +      thm list * thm list * thm list) * local_theory
    5.11  end;
    5.12  
    5.13  structure BNF_LFP : BNF_LFP =
    5.14 @@ -1343,7 +1343,7 @@
    5.15      val timer = time (timer "induction");
    5.16  
    5.17      (*register new datatypes as BNFs*)
    5.18 -    val lthy = if m = 0 then lthy else
    5.19 +    val (Irels, lthy) = if m = 0 then ([], lthy) else
    5.20        let
    5.21          val fTs = map2 (curry op -->) passiveAs passiveBs;
    5.22          val f1Ts = map2 (curry op -->) passiveAs passiveYs;
    5.23 @@ -1374,8 +1374,8 @@
    5.24            ||>> mk_Frees "p1" p1Ts
    5.25            ||>> mk_Frees "p2" p2Ts
    5.26            ||>> mk_Frees' "y" passiveAs
    5.27 -          ||>> mk_Frees "R" IRTs
    5.28 -          ||>> mk_Frees "P" IphiTs;
    5.29 +          ||>> mk_Frees "S" IRTs
    5.30 +          ||>> mk_Frees "R" IphiTs;
    5.31  
    5.32          val map_FTFT's = map2 (fn Ds =>
    5.33            mk_map_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
    5.34 @@ -1794,7 +1794,7 @@
    5.35                ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
    5.36              bs thmss)
    5.37        in
    5.38 -        timer; lthy |> Local_Theory.notes (Ibnf_common_notes @ Ibnf_notes) |> snd
    5.39 +        timer; (Irels, lthy |> Local_Theory.notes (Ibnf_common_notes @ Ibnf_notes) |> snd)
    5.40        end;
    5.41  
    5.42        val common_notes =
    5.43 @@ -1819,8 +1819,8 @@
    5.44              ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
    5.45            bs thmss)
    5.46    in
    5.47 -    ((dtors, ctors, folds, recs, ctor_induct_thm, dtor_ctor_thms, ctor_dtor_thms, ctor_inject_thms,
    5.48 -      ctor_fold_thms, ctor_rec_thms),
    5.49 +    ((dtors, ctors, Irels, folds, recs, ctor_induct_thm, dtor_ctor_thms, ctor_dtor_thms,
    5.50 +      ctor_inject_thms, ctor_fold_thms, ctor_rec_thms),
    5.51       lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
    5.52    end;
    5.53  
     6.1 --- a/src/HOL/BNF/Tools/bnf_util.ML	Sun Sep 23 08:24:19 2012 +0200
     6.2 +++ b/src/HOL/BNF/Tools/bnf_util.ML	Sun Sep 23 14:52:53 2012 +0200
     6.3 @@ -102,6 +102,8 @@
     6.4    val mk_subset: term -> term -> term
     6.5    val mk_wpull: term -> term -> term -> term -> term -> (term * term) option -> term -> term -> term
     6.6  
     6.7 +  val rapp: term -> term -> term
     6.8 +
     6.9    val list_all_free: term list -> term -> term
    6.10    val list_exists_free: term list -> term -> term
    6.11  
    6.12 @@ -504,6 +506,8 @@
    6.13  
    6.14  fun mk_permute src dest xs = map (nth xs o (fn x => find_index ((curry op =) x) src)) dest;
    6.15  
    6.16 +fun rapp u t = betapply (t, u);
    6.17 +
    6.18  val list_all_free =
    6.19    fold_rev (fn free => fn P =>
    6.20      let val (x, T) = Term.dest_Free free;
     7.1 --- a/src/HOL/BNF/Tools/bnf_wrap.ML	Sun Sep 23 08:24:19 2012 +0200
     7.2 +++ b/src/HOL/BNF/Tools/bnf_wrap.ML	Sun Sep 23 14:52:53 2012 +0200
     7.3 @@ -84,14 +84,17 @@
     7.4  fun mk_disc_or_sel Ts t =
     7.5    Term.subst_atomic_types (snd (Term.dest_Type (domain_type (fastype_of t))) ~~ Ts) t;
     7.6  
     7.7 +fun mk_case Ts T t =
     7.8 +  let val (Type (_, Ts0), body) = strip_type (fastype_of t) |>> List.last in
     7.9 +    Term.subst_atomic_types ((body, T) :: (Ts0 ~~ Ts)) t
    7.10 +  end;
    7.11 +
    7.12  fun base_name_of_ctr c =
    7.13    Long_Name.base_name (case head_of c of
    7.14        Const (s, _) => s
    7.15      | Free (s, _) => s
    7.16      | _ => error "Cannot extract name of constructor");
    7.17  
    7.18 -fun rapp u t = betapply (t, u);
    7.19 -
    7.20  fun eta_expand_arg xs f_xs = fold_rev Term.lambda xs f_xs;
    7.21  
    7.22  fun prepare_wrap_datatype prep_term (((no_dests, raw_ctrs), raw_case),
    7.23 @@ -163,13 +166,7 @@
    7.24            else
    7.25              sel)) (1 upto m) o pad_list Binding.empty m) ctrs0 ms;
    7.26  
    7.27 -    fun mk_case Ts T =
    7.28 -      let
    7.29 -        val (bindings, body) = strip_type (fastype_of case0)
    7.30 -        val Type (_, Ts0) = List.last bindings
    7.31 -      in Term.subst_atomic_types ((body, T) :: (Ts0 ~~ Ts)) case0 end;
    7.32 -
    7.33 -    val casex = mk_case As B;
    7.34 +    val casex = mk_case As B case0;
    7.35      val case_Ts = map (fn Ts => Ts ---> B) ctr_Tss;
    7.36  
    7.37      val (((((((xss, xss'), yss), fs), gs), [u', v']), (p, p')), names_lthy) = no_defs_lthy |>
    7.38 @@ -260,7 +257,7 @@
    7.39                      " vs. " ^ quote (Syntax.string_of_typ no_defs_lthy T')));
    7.40              in
    7.41                mk_Trueprop_eq (Free (Binding.name_of b, dataT --> T) $ u,
    7.42 -                Term.list_comb (mk_case As T, mk_sel_case_args b proto_sels T) $ u)
    7.43 +                Term.list_comb (mk_case As T case0, mk_sel_case_args b proto_sels T) $ u)
    7.44              end;
    7.45  
    7.46            val sel_bindings = flat sel_bindingss;