src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
changeset 52329 932014a2fe53
parent 52328 2f286a2b7f98
child 52330 8ce7fba90bb3
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Fri Jun 07 08:48:59 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Fri Jun 07 08:57:44 2013 +0200
     1.3 @@ -54,14 +54,14 @@
     1.4         * (typ list * typ list list list * typ list list)) list ->
     1.5      (string -> binding) -> typ list -> typ list -> term list -> Proof.context ->
     1.6      (term list * thm list) * Proof.context
     1.7 -  val derive_induct_fold_rec_thms_for_types: BNF_Def.bnf list -> term list list ->
     1.8 +  val derive_induct_iters_thms_for_types: BNF_Def.bnf list -> term list list ->
     1.9      (typ list list * typ list list list list * term list list * term list list list list) list ->
    1.10      thm -> thm list list -> BNF_Def.bnf list -> BNF_Def.bnf list -> typ list -> typ list ->
    1.11      typ list -> typ list list list -> term list list -> thm list list -> term list list ->
    1.12      thm list list -> local_theory ->
    1.13      (thm * thm list * Args.src list) * (thm list list * Args.src list)
    1.14      * (thm list list * Args.src list)
    1.15 -  val derive_coinduct_unfold_corec_thms_for_types: BNF_Def.bnf list -> term list list -> thm ->
    1.16 +  val derive_coinduct_coiters_thms_for_types: BNF_Def.bnf list -> term list list -> thm ->
    1.17      thm -> thm list -> thm list list -> BNF_Def.bnf list -> BNF_Def.bnf list -> typ list ->
    1.18      typ list -> typ list -> int list list -> int list list -> int list -> thm list list ->
    1.19      BNF_Ctr_Sugar.ctr_sugar list -> term list list -> thm list list -> local_theory ->
    1.20 @@ -269,7 +269,7 @@
    1.21    #> map3 mk_fun_arg_typess ns mss
    1.22    #> map (map (map (unzip_recT Cs)));
    1.23  
    1.24 -fun mk_fold_rec_args_types Cs ns mss [ctor_fold_fun_Ts, ctor_rec_fun_Ts] lthy =
    1.25 +fun mk_iters_args_types Cs ns mss [ctor_fold_fun_Ts, ctor_rec_fun_Ts] lthy =
    1.26    let
    1.27      val Css = map2 replicate ns Cs;
    1.28      val y_Tsss = map3 mk_fun_arg_typess ns mss ctor_fold_fun_Ts;
    1.29 @@ -300,7 +300,7 @@
    1.30      ([(g_Tss, y_Tssss, gss, yssss), (h_Tss, z_Tssss, hss, zssss)], lthy)
    1.31    end;
    1.32  
    1.33 -fun mk_unfold_corec_args_types Cs ns mss [dtor_unfold_fun_Ts, dtor_corec_fun_Ts] lthy =
    1.34 +fun mk_coiters_args_types Cs ns mss [dtor_unfold_fun_Ts, dtor_corec_fun_Ts] lthy =
    1.35    let
    1.36      (*avoid "'a itself" arguments in coiterators and corecursors*)
    1.37      fun repair_arity [0] = [1]
    1.38 @@ -355,21 +355,21 @@
    1.39      ((cs, cpss, [(unfold_args, unfold_types), (corec_args, corec_types)]), lthy)
    1.40    end;
    1.41  
    1.42 -fun mk_un_fold_co_rec_prelims fp fpTs Cs ns mss xtor_co_iterss0' lthy =
    1.43 +fun mk_un_fold_co_rec_prelims fp fpTs Cs ns mss xtor_co_iterss0 lthy =
    1.44    let
    1.45      val thy = Proof_Context.theory_of lthy;
    1.46  
    1.47      val (xtor_co_iter_fun_Tss', xtor_co_iterss') =
    1.48 -      map (mk_co_iters thy fp fpTs Cs #> `(mk_fp_iter_fun_types o hd)) xtor_co_iterss0'
    1.49 +      map (mk_co_iters thy fp fpTs Cs #> `(mk_fp_iter_fun_types o hd)) (transpose xtor_co_iterss0)
    1.50        |> split_list;
    1.51  
    1.52 -    val ((fold_rec_args_types, unfold_corec_args_types), lthy') =
    1.53 +    val ((iters_args_types, coiters_args_types), lthy') =
    1.54        if fp = Least_FP then
    1.55 -        mk_fold_rec_args_types Cs ns mss xtor_co_iter_fun_Tss' lthy |>> (rpair NONE o SOME)
    1.56 +        mk_iters_args_types Cs ns mss xtor_co_iter_fun_Tss' lthy |>> (rpair NONE o SOME)
    1.57        else
    1.58 -        mk_unfold_corec_args_types Cs ns mss xtor_co_iter_fun_Tss' lthy |>> (pair NONE o SOME)
    1.59 +        mk_coiters_args_types Cs ns mss xtor_co_iter_fun_Tss' lthy |>> (pair NONE o SOME)
    1.60    in
    1.61 -    ((xtor_co_iterss', fold_rec_args_types, unfold_corec_args_types), lthy')
    1.62 +    ((xtor_co_iterss', iters_args_types, coiters_args_types), lthy')
    1.63    end;
    1.64  
    1.65  fun mk_map live Ts Us t =
    1.66 @@ -523,7 +523,7 @@
    1.67        (map3 generate_coiter coiterNs coiter_args_typess' dtor_coiters) lthy
    1.68    end;
    1.69  
    1.70 -fun derive_induct_fold_rec_thms_for_types pre_bnfs [ctor_folds, ctor_recs]
    1.71 +fun derive_induct_iters_thms_for_types pre_bnfs [ctor_folds, ctor_recs]
    1.72      [fold_args_types, rec_args_types] ctor_induct [ctor_fold_thms, ctor_rec_thms] nesting_bnfs
    1.73      nested_bnfs fpTs Cs Xs ctrXs_Tsss ctrss ctr_defss [folds, recs] [fold_defs, rec_defs] lthy =
    1.74    let
    1.75 @@ -677,7 +677,7 @@
    1.76       (fold_thmss, code_simp_attrs), (rec_thmss, code_simp_attrs))
    1.77    end;
    1.78  
    1.79 -fun derive_coinduct_unfold_corec_thms_for_types pre_bnfs [dtor_unfolds, dtor_corecs] dtor_coinduct
    1.80 +fun derive_coinduct_coiters_thms_for_types pre_bnfs [dtor_unfolds, dtor_corecs] dtor_coinduct
    1.81      dtor_strong_induct dtor_ctors [dtor_unfold_thms, dtor_corec_thms] nesting_bnfs nested_bnfs fpTs
    1.82      Cs As kss mss ns ctr_defss ctr_sugars [unfolds, corecs] [unfold_defs, corec_defs] lthy =
    1.83    let
    1.84 @@ -705,7 +705,7 @@
    1.85      val sel_thmsss = map #sel_thmss ctr_sugars;
    1.86  
    1.87      val ((cs, cpss, [((pgss, crssss, cgssss), _), ((phss, csssss, chssss), _)]), names_lthy0) =
    1.88 -      mk_unfold_corec_args_types Cs ns mss [dtor_unfold_fun_Ts, dtor_corec_fun_Ts] lthy;
    1.89 +      mk_coiters_args_types Cs ns mss [dtor_unfold_fun_Ts, dtor_corec_fun_Ts] lthy;
    1.90  
    1.91      val (((rs, us'), vs'), names_lthy) =
    1.92        names_lthy0
    1.93 @@ -1099,8 +1099,8 @@
    1.94      val kss = map (fn n => 1 upto n) ns;
    1.95      val mss = map (map length) ctr_Tsss;
    1.96  
    1.97 -    val ((xtor_co_iterss', fold_rec_args_types, unfold_corec_args_types), lthy) =
    1.98 -      mk_un_fold_co_rec_prelims fp fpTs Cs ns mss (transpose xtor_co_iterss0) lthy;
    1.99 +    val ((xtor_co_iterss', iters_args_types, coiters_args_types), lthy) =
   1.100 +      mk_un_fold_co_rec_prelims fp fpTs Cs ns mss xtor_co_iterss0 lthy;
   1.101  
   1.102      fun define_ctrs_case_for_type ((((((((((((((((((((((((fp_bnf, fp_b), fpT), C), ctor), dtor),
   1.103                xtor_co_iters), ctor_dtor), dtor_ctor), ctor_inject), pre_map_def), pre_set_defs),
   1.104 @@ -1293,8 +1293,8 @@
   1.105          (wrap_ctrs
   1.106           #> derive_maps_sets_rels
   1.107           ##>>
   1.108 -           (if fp = Least_FP then define_iters [foldN, recN] (the fold_rec_args_types)
   1.109 -            else define_coiters [unfoldN, corecN] (the unfold_corec_args_types))
   1.110 +           (if fp = Least_FP then define_iters [foldN, recN] (the iters_args_types)
   1.111 +            else define_coiters [unfoldN, corecN] (the coiters_args_types))
   1.112               mk_binding fpTs Cs xtor_co_iters
   1.113           #> massage_res, lthy')
   1.114        end;
   1.115 @@ -1310,15 +1310,15 @@
   1.116            injects @ distincts @ case_thms @ co_recs @ un_folds @ mapsx @ rel_injects
   1.117            @ rel_distincts @ flat setss);
   1.118  
   1.119 -    fun derive_and_note_induct_fold_rec_thms_for_types
   1.120 +    fun derive_and_note_induct_iters_thms_for_types
   1.121          ((((mapsx, rel_injects, rel_distincts, setss), (ctrss, _, ctr_defss, ctr_sugars)),
   1.122            (iterss', iter_defss')), lthy) =
   1.123        let
   1.124          val ((induct_thm, induct_thms, induct_attrs), (fold_thmss, fold_attrs),
   1.125               (rec_thmss, rec_attrs)) =
   1.126 -          derive_induct_fold_rec_thms_for_types pre_bnfs xtor_co_iterss'
   1.127 -            (the fold_rec_args_types) xtor_co_induct (transpose xtor_co_iter_thmss) nesting_bnfs
   1.128 -            nested_bnfs fpTs Cs Xs ctrXs_Tsss ctrss ctr_defss iterss' iter_defss' lthy;
   1.129 +          derive_induct_iters_thms_for_types pre_bnfs xtor_co_iterss' (the iters_args_types)
   1.130 +            xtor_co_induct (transpose xtor_co_iter_thmss) nesting_bnfs nested_bnfs fpTs Cs Xs
   1.131 +            ctrXs_Tsss ctrss ctr_defss iterss' iter_defss' lthy;
   1.132  
   1.133          val induct_type_attr = Attrib.internal o K o Induct.induct_type;
   1.134  
   1.135 @@ -1342,7 +1342,7 @@
   1.136            induct_thm [fold_thmss, rec_thmss]
   1.137        end;
   1.138  
   1.139 -    fun derive_and_note_coinduct_unfold_corec_thms_for_types
   1.140 +    fun derive_and_note_coinduct_coiters_thms_for_types
   1.141          ((((mapsx, rel_injects, rel_distincts, setss), (_, _, ctr_defss, ctr_sugars)),
   1.142            (coiterss', coiter_defss')), lthy) =
   1.143        let
   1.144 @@ -1353,7 +1353,7 @@
   1.145               (disc_unfold_thmss, disc_corec_thmss, disc_coiter_attrs),
   1.146               (disc_unfold_iff_thmss, disc_corec_iff_thmss, disc_coiter_iff_attrs),
   1.147               (sel_unfold_thmss, sel_corec_thmss, sel_coiter_attrs)) =
   1.148 -          derive_coinduct_unfold_corec_thms_for_types pre_bnfs xtor_co_iterss' xtor_co_induct
   1.149 +          derive_coinduct_coiters_thms_for_types pre_bnfs xtor_co_iterss' xtor_co_induct
   1.150              xtor_strong_co_induct dtor_ctors (transpose xtor_co_iter_thmss) nesting_bnfs nested_bnfs
   1.151              fpTs Cs As kss mss ns ctr_defss ctr_sugars coiterss' coiter_defss' lthy;
   1.152  
   1.153 @@ -1408,8 +1408,8 @@
   1.154          kss ~~ mss ~~ ctr_bindingss ~~ ctr_mixfixess ~~ ctr_Tsss ~~ disc_bindingss ~~
   1.155          sel_bindingsss ~~ raw_sel_defaultsss)
   1.156        |> wrap_types_etc
   1.157 -      |> (if fp = Least_FP then derive_and_note_induct_fold_rec_thms_for_types
   1.158 -          else derive_and_note_coinduct_unfold_corec_thms_for_types);
   1.159 +      |> (if fp = Least_FP then derive_and_note_induct_iters_thms_for_types
   1.160 +          else derive_and_note_coinduct_coiters_thms_for_types);
   1.161  
   1.162      val timer = time (timer ("Constructors, discriminators, selectors, etc., for the new " ^
   1.163        datatype_word fp));