src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
changeset 49370 be6e749fd003
parent 49368 df359ce891ac
child 49371 9fa21648d0a1
     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 @@ -34,9 +34,9 @@
     1.4  
     1.5  val simp_attrs = @{attributes [simp]};
     1.6  
     1.7 -fun split_list11 xs =
     1.8 +fun split_list10 xs =
     1.9    (map #1 xs, map #2 xs, map #3 xs, map #4 xs, map #5 xs, map #6 xs, map #7 xs, map #8 xs,
    1.10 -   map #9 xs, map #10 xs, map #11 xs);
    1.11 +   map #9 xs, map #10 xs);
    1.12  
    1.13  fun strip_map_type (Type (@{type_name fun}, [T as Type _, T'])) = strip_map_type T' |>> cons T
    1.14    | strip_map_type T = ([], T);
    1.15 @@ -102,12 +102,11 @@
    1.16      val unsorted_Ass0 = map (map (resort_tfree HOLogic.typeS)) Ass0;
    1.17      val unsorted_As = Library.foldr1 merge_type_args unsorted_Ass0;
    1.18  
    1.19 -    val (((Bs, Cs), vs'), no_defs_lthy) =
    1.20 +    val ((Bs, Cs), no_defs_lthy) =
    1.21        no_defs_lthy0
    1.22        |> fold (Variable.declare_typ o resort_tfree dummyS) unsorted_As
    1.23        |> mk_TFrees nn
    1.24 -      ||>> mk_TFrees nn
    1.25 -      ||>> Variable.variant_fixes (map Binding.name_of fp_bs);
    1.26 +      ||>> mk_TFrees nn;
    1.27  
    1.28      (* TODO: cleaner handling of fake contexts, without "background_theory" *)
    1.29      (*the "perhaps o try" below helps gracefully handles the case where the new type is defined in a
    1.30 @@ -205,8 +204,6 @@
    1.31  
    1.32      val exists_fp_subtype = exists_subtype (member (op =) fpTs);
    1.33  
    1.34 -    val vs = map2 (curry Free) vs' fpTs;
    1.35 -
    1.36      val ctr_Tsss = map (map (map (Term.typ_subst_atomic (Bs ~~ fpTs)))) ctr_TsssBs;
    1.37      val ns = map length ctr_Tsss;
    1.38      val kss = map (fn n => 1 upto n) ns;
    1.39 @@ -330,20 +327,23 @@
    1.40              (mk_terms sssss hssss, (h_sum_prod_Ts, ph_Tss))))
    1.41          end;
    1.42  
    1.43 -    fun define_ctrs_case_for_type (((((((((((((((((((fp_b, fpT), C), v), fld), unf), fp_iter),
    1.44 -          fp_rec), fld_unf), unf_fld), fld_inject), n), ks), ms), ctr_bindings), ctr_mixfixes),
    1.45 -        ctr_Tss), disc_bindings), sel_bindingss), raw_sel_defaultss) no_defs_lthy =
    1.46 +    fun define_ctrs_case_for_type ((((((((((((((((((fp_b, fpT), C), fld), unf), fp_iter), fp_rec),
    1.47 +          fld_unf), unf_fld), fld_inject), n), ks), ms), ctr_bindings), ctr_mixfixes), ctr_Tss),
    1.48 +        disc_bindings), sel_bindingss), raw_sel_defaultss) no_defs_lthy =
    1.49        let
    1.50          val unfT = domain_type (fastype_of fld);
    1.51          val ctr_prod_Ts = map HOLogic.mk_tupleT ctr_Tss;
    1.52          val ctr_sum_prod_T = mk_sumTN_balanced ctr_prod_Ts;
    1.53          val case_Ts = map (fn Ts => Ts ---> C) ctr_Tss;
    1.54  
    1.55 -        val (((u, fs), xss), _) =
    1.56 +        val ((((u, fs), xss), v'), _) =
    1.57            no_defs_lthy
    1.58            |> yield_singleton (mk_Frees "u") unfT
    1.59            ||>> mk_Frees "f" case_Ts
    1.60 -          ||>> mk_Freess "x" ctr_Tss;
    1.61 +          ||>> mk_Freess "x" ctr_Tss
    1.62 +          ||>> yield_singleton (Variable.variant_fixes) (Binding.name_of fp_b);
    1.63 +
    1.64 +        val v = Free (v', fpT);
    1.65  
    1.66          val ctr_rhss =
    1.67            map2 (fn k => fn xs => fold_rev Term.lambda xs (fld $
    1.68 @@ -441,8 +441,7 @@
    1.69  
    1.70              val [iter, recx] = map (mk_iter_like As Cs o Morphism.term phi) csts;
    1.71            in
    1.72 -            ((ctrs, selss0, iter, recx, v, xss, ctr_defs, discIs, sel_thmss, iter_def, rec_def),
    1.73 -             lthy)
    1.74 +            ((ctrs, selss0, iter, recx, xss, ctr_defs, discIs, sel_thmss, iter_def, rec_def), lthy)
    1.75            end;
    1.76  
    1.77          fun define_coiter_corec ((selss0, discIs, sel_thmss), no_defs_lthy) =
    1.78 @@ -482,8 +481,8 @@
    1.79  
    1.80              val [coiter, corec] = map (mk_iter_like As Cs o Morphism.term phi) csts;
    1.81            in
    1.82 -            ((ctrs, selss0, coiter, corec, v, xss, ctr_defs, discIs, sel_thmss, coiter_def,
    1.83 -              corec_def), lthy)
    1.84 +            ((ctrs, selss0, coiter, corec, xss, ctr_defs, discIs, sel_thmss, coiter_def, corec_def),
    1.85 +             lthy)
    1.86            end;
    1.87  
    1.88          fun wrap lthy =
    1.89 @@ -516,9 +515,16 @@
    1.90          val args = map build_arg TUs;
    1.91        in Term.list_comb (mapx, args) end;
    1.92  
    1.93 -    fun derive_induct_iter_rec_thms_for_types ((ctrss, _, iters, recs, vs, xsss, ctr_defss, _, _,
    1.94 +    fun derive_induct_iter_rec_thms_for_types ((ctrss, _, iters, recs, xsss, ctr_defss, _, _,
    1.95          iter_defs, rec_defs), lthy) =
    1.96        let
    1.97 +        val (((phis, phis'), vs'), names_lthy) =
    1.98 +          lthy
    1.99 +          |> mk_Frees' "P" (map mk_predT fpTs)
   1.100 +          ||>> Variable.variant_fixes (map Binding.name_of fp_bs);
   1.101 +
   1.102 +        val vs = map2 (curry Free) vs' fpTs;
   1.103 +
   1.104          fun mk_sets_nested bnf =
   1.105            let
   1.106              val Type (T_name, Us) = T_of_bnf bnf;
   1.107 @@ -536,10 +542,6 @@
   1.108  
   1.109          val (induct_thms, induct_thm) =
   1.110            let
   1.111 -            val ((phis, phis'), names_lthy) =
   1.112 -              lthy
   1.113 -              |> mk_Frees' "P" (map mk_predT fpTs);
   1.114 -
   1.115              fun mk_set Ts t =
   1.116                let val Type (_, Ts0) = domain_type (fastype_of t) in
   1.117                  Term.subst_atomic_types (Ts0 ~~ Ts) t
   1.118 @@ -597,9 +599,7 @@
   1.119                Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
   1.120                  mk_induct_tac ctxt ns mss rss (flat ctr_defss) fld_induct' pre_set_defss
   1.121                    nested_set_natural's)
   1.122 -              (* TODO: thread name context properly ### *)
   1.123                |> singleton (Proof_Context.export names_lthy lthy)
   1.124 -              |> singleton (Proof_Context.export no_defs_lthy no_defs_lthy0)
   1.125            in
   1.126              `(conj_dests nn) induct_thm
   1.127            end;
   1.128 @@ -669,9 +669,15 @@
   1.129          lthy |> Local_Theory.notes (common_notes @ notes) |> snd
   1.130        end;
   1.131  
   1.132 -    fun derive_coinduct_coiter_corec_thms_for_types ((ctrss, selsss, coiters, corecs, vs, _,
   1.133 -        ctr_defss, discIss, sel_thmsss, coiter_defs, corec_defs), lthy) =
   1.134 +    fun derive_coinduct_coiter_corec_thms_for_types ((ctrss, selsss, coiters, corecs, _, ctr_defss,
   1.135 +        discIss, sel_thmsss, coiter_defs, corec_defs), lthy) =
   1.136        let
   1.137 +        val (vs', names_lthy) =
   1.138 +          lthy
   1.139 +          |> Variable.variant_fixes (map Binding.name_of fp_bs);
   1.140 +
   1.141 +        val vs = map2 (curry Free) vs' fpTs;
   1.142 +
   1.143          val (coinduct_thms, coinduct_thm) =
   1.144            let
   1.145              val coinduct_thm = fp_induct;
   1.146 @@ -780,13 +786,12 @@
   1.147        end;
   1.148  
   1.149      fun wrap_types_and_define_iter_likes ((wraps, define_iter_likess), lthy) =
   1.150 -      fold_map2 (curry (op o)) define_iter_likess wraps lthy |>> split_list11
   1.151 +      fold_map2 (curry (op o)) define_iter_likess wraps lthy |>> split_list10
   1.152  
   1.153      val lthy' = lthy
   1.154 -      |> fold_map define_ctrs_case_for_type (fp_bs ~~ fpTs ~~ Cs ~~ vs ~~ flds ~~ unfs ~~
   1.155 -        fp_iters ~~ fp_recs ~~ fld_unfs ~~ unf_flds ~~ fld_injects ~~ ns ~~ kss ~~ mss ~~
   1.156 -        ctr_bindingss ~~ ctr_mixfixess ~~ ctr_Tsss ~~ disc_bindingss ~~ sel_bindingsss ~~
   1.157 -        raw_sel_defaultsss)
   1.158 +      |> fold_map define_ctrs_case_for_type (fp_bs ~~ fpTs ~~ Cs ~~ flds ~~ unfs ~~ fp_iters ~~
   1.159 +        fp_recs ~~ fld_unfs ~~ unf_flds ~~ fld_injects ~~ ns ~~ kss ~~ mss ~~ ctr_bindingss ~~
   1.160 +        ctr_mixfixess ~~ ctr_Tsss ~~ disc_bindingss ~~ sel_bindingsss ~~ raw_sel_defaultsss)
   1.161        |>> split_list |> wrap_types_and_define_iter_likes
   1.162        |> (if lfp then derive_induct_iter_rec_thms_for_types
   1.163            else derive_coinduct_coiter_corec_thms_for_types);