src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
changeset 52349 07fd21c01e93
parent 52348 740923a6e530
child 52351 40136fcb5e7a
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Fri Jun 07 16:19:52 2013 +0100
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Fri Jun 07 17:04:55 2013 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4  (*  Title:      HOL/BNF/Tools/bnf_fp_def_sugar.ML
     1.5      Author:     Jasmin Blanchette, TU Muenchen
     1.6 -    Copyright   2012
     1.7 +    Copyright   2012, 2013
     1.8  
     1.9  Sugared datatype and codatatype constructions.
    1.10  *)
    1.11 @@ -36,8 +36,7 @@
    1.12       * (typ list list * typ list list list list * term list list
    1.13          * term list list list list) list option
    1.14       * (string * term list * term list list
    1.15 -        * ((term list list * term list list list)
    1.16 -           * (typ list * typ list list list * typ list list)) list) option)
    1.17 +        * ((term list list * term list list list) * (typ list * typ list list)) list) option)
    1.18      * Proof.context
    1.19  
    1.20    val mk_iter_fun_arg_typessss: typ list -> int list -> int list list -> term ->
    1.21 @@ -47,8 +46,7 @@
    1.22      (string -> binding) -> typ list -> typ list -> term list -> Proof.context ->
    1.23      (term list * thm list) * Proof.context
    1.24    val define_coiters: string list -> string * term list * term list list
    1.25 -    * ((term list list * term list list list)
    1.26 -       * (typ list * typ list list list * typ list list)) list ->
    1.27 +    * ((term list list * term list list list) * (typ list * typ list list)) list ->
    1.28      (string -> binding) -> typ list -> typ list -> term list -> Proof.context ->
    1.29      (term list * thm list) * Proof.context
    1.30    val derive_induct_iters_thms_for_types: BNF_Def.bnf list ->
    1.31 @@ -379,10 +377,10 @@
    1.32          val q_Tssss =
    1.33            map (map (map (fn [_] => [] | [_, T] => [mk_pred1T (domain_type T)]))) f_Tssss;
    1.34          val pf_Tss = map3 flat_preds_predsss_gettersss p_Tss q_Tssss f_Tssss;
    1.35 -      in (q_Tssss, f_Tssss, (f_sum_prod_Ts, f_Tsss, pf_Tss)) end;
    1.36 +      in (q_Tssss, f_Tsss, f_Tssss, (f_sum_prod_Ts, pf_Tss)) end;
    1.37  
    1.38 -    val (r_Tssss, g_Tssss, unfold_types) = mk_types single un_fold_of;
    1.39 -    val (s_Tssss, h_Tssss, corec_types) = mk_types unzip_corecT co_rec_of;
    1.40 +    val (r_Tssss, g_Tsss, g_Tssss, unfold_types) = mk_types single un_fold_of;
    1.41 +    val (s_Tssss, h_Tsss, h_Tssss, corec_types) = mk_types unzip_corecT co_rec_of;
    1.42  
    1.43      val ((((Free (z, _), cs), pss), gssss), lthy) =
    1.44        lthy
    1.45 @@ -408,7 +406,7 @@
    1.46          mk_If cq (build_sum_inj Inl_const (fastype_of cf, T) $ cf)
    1.47            (build_sum_inj Inr_const (fastype_of cf', T) $ cf');
    1.48  
    1.49 -    fun mk_args qssss fssss (_, f_Tsss, _) =
    1.50 +    fun mk_args qssss fssss f_Tsss =
    1.51        let
    1.52          val pfss = map3 flat_preds_predsss_gettersss pss qssss fssss;
    1.53          val cqssss = map2 (map o map o map o rapp) cs qssss;
    1.54 @@ -416,8 +414,8 @@
    1.55          val cqfsss = map3 (map3 (map3 build_dtor_coiter_arg)) f_Tsss cqssss cfssss;
    1.56        in (pfss, cqfsss) end;
    1.57  
    1.58 -    val unfold_args = mk_args rssss gssss unfold_types;
    1.59 -    val corec_args = mk_args sssss hssss corec_types;
    1.60 +    val unfold_args = mk_args rssss gssss g_Tsss;
    1.61 +    val corec_args = mk_args sssss hssss h_Tsss;
    1.62    in
    1.63      ((z, cs, cpss, [(unfold_args, unfold_types), (corec_args, corec_types)]), lthy)
    1.64    end;
    1.65 @@ -494,7 +492,7 @@
    1.66  
    1.67      val C_to_fpT as Type (_, [_, fpT]) = snd (strip_typeN nn (fastype_of (hd dtor_coiters)));
    1.68  
    1.69 -    fun generate_coiter suf ((pfss, cqfsss), (f_sum_prod_Ts, _, pf_Tss)) dtor_coiter =
    1.70 +    fun generate_coiter suf ((pfss, cqfsss), (f_sum_prod_Ts, pf_Tss)) dtor_coiter =
    1.71        let
    1.72          val res_T = fold_rev (curry (op --->)) pf_Tss C_to_fpT;
    1.73          val b = mk_binding suf;
    1.74 @@ -862,11 +860,10 @@
    1.75          val nested_map_if_distribs = map mk_map_if_distrib nested_bnfs;
    1.76  
    1.77          val unfold_tacss =
    1.78 -          map3 (map oo mk_coiter_tac unfold_defs [] nesting_map_ids'' [])
    1.79 +          map3 (map oo mk_coiter_tac unfold_defs nesting_map_ids'')
    1.80              (map un_fold_of dtor_coiter_thmss) pre_map_defs ctr_defss;
    1.81          val corec_tacss =
    1.82 -          map3 (map oo mk_coiter_tac corec_defs nested_map_comp's
    1.83 -              (nested_map_ids'' @ nesting_map_ids'') nested_map_if_distribs)
    1.84 +          map3 (map oo mk_coiter_tac corec_defs nesting_map_ids'')
    1.85              (map co_rec_of dtor_coiter_thmss) pre_map_defs ctr_defss;
    1.86  
    1.87          fun prove goal tac =