diff -r 2f286a2b7f98 -r 932014a2fe53 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Fri Jun 07 08:48:59 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Fri Jun 07 08:57:44 2013 +0200 @@ -54,14 +54,14 @@ * (typ list * typ list list list * typ list list)) list -> (string -> binding) -> typ list -> typ list -> term list -> Proof.context -> (term list * thm list) * Proof.context - val derive_induct_fold_rec_thms_for_types: BNF_Def.bnf list -> term list list -> + val derive_induct_iters_thms_for_types: BNF_Def.bnf list -> term list list -> (typ list list * typ list list list list * term list list * term list list list list) list -> thm -> thm list list -> BNF_Def.bnf list -> BNF_Def.bnf list -> typ list -> typ list -> typ list -> typ list list list -> term list list -> thm list list -> term list list -> thm list list -> local_theory -> (thm * thm list * Args.src list) * (thm list list * Args.src list) * (thm list list * Args.src list) - val derive_coinduct_unfold_corec_thms_for_types: BNF_Def.bnf list -> term list list -> thm -> + val derive_coinduct_coiters_thms_for_types: BNF_Def.bnf list -> term list list -> thm -> thm -> thm list -> thm list list -> BNF_Def.bnf list -> BNF_Def.bnf list -> typ list -> typ list -> typ list -> int list list -> int list list -> int list -> thm list list -> BNF_Ctr_Sugar.ctr_sugar list -> term list list -> thm list list -> local_theory -> @@ -269,7 +269,7 @@ #> map3 mk_fun_arg_typess ns mss #> map (map (map (unzip_recT Cs))); -fun mk_fold_rec_args_types Cs ns mss [ctor_fold_fun_Ts, ctor_rec_fun_Ts] lthy = +fun mk_iters_args_types Cs ns mss [ctor_fold_fun_Ts, ctor_rec_fun_Ts] lthy = let val Css = map2 replicate ns Cs; val y_Tsss = map3 mk_fun_arg_typess ns mss ctor_fold_fun_Ts; @@ -300,7 +300,7 @@ ([(g_Tss, y_Tssss, gss, yssss), (h_Tss, z_Tssss, hss, zssss)], lthy) end; -fun mk_unfold_corec_args_types Cs ns mss [dtor_unfold_fun_Ts, dtor_corec_fun_Ts] lthy = +fun mk_coiters_args_types Cs ns mss [dtor_unfold_fun_Ts, dtor_corec_fun_Ts] lthy = let (*avoid "'a itself" arguments in coiterators and corecursors*) fun repair_arity [0] = [1] @@ -355,21 +355,21 @@ ((cs, cpss, [(unfold_args, unfold_types), (corec_args, corec_types)]), lthy) end; -fun mk_un_fold_co_rec_prelims fp fpTs Cs ns mss xtor_co_iterss0' lthy = +fun mk_un_fold_co_rec_prelims fp fpTs Cs ns mss xtor_co_iterss0 lthy = let val thy = Proof_Context.theory_of lthy; val (xtor_co_iter_fun_Tss', xtor_co_iterss') = - map (mk_co_iters thy fp fpTs Cs #> `(mk_fp_iter_fun_types o hd)) xtor_co_iterss0' + map (mk_co_iters thy fp fpTs Cs #> `(mk_fp_iter_fun_types o hd)) (transpose xtor_co_iterss0) |> split_list; - val ((fold_rec_args_types, unfold_corec_args_types), lthy') = + val ((iters_args_types, coiters_args_types), lthy') = if fp = Least_FP then - mk_fold_rec_args_types Cs ns mss xtor_co_iter_fun_Tss' lthy |>> (rpair NONE o SOME) + mk_iters_args_types Cs ns mss xtor_co_iter_fun_Tss' lthy |>> (rpair NONE o SOME) else - mk_unfold_corec_args_types Cs ns mss xtor_co_iter_fun_Tss' lthy |>> (pair NONE o SOME) + mk_coiters_args_types Cs ns mss xtor_co_iter_fun_Tss' lthy |>> (pair NONE o SOME) in - ((xtor_co_iterss', fold_rec_args_types, unfold_corec_args_types), lthy') + ((xtor_co_iterss', iters_args_types, coiters_args_types), lthy') end; fun mk_map live Ts Us t = @@ -523,7 +523,7 @@ (map3 generate_coiter coiterNs coiter_args_typess' dtor_coiters) lthy end; -fun derive_induct_fold_rec_thms_for_types pre_bnfs [ctor_folds, ctor_recs] +fun derive_induct_iters_thms_for_types pre_bnfs [ctor_folds, ctor_recs] [fold_args_types, rec_args_types] ctor_induct [ctor_fold_thms, ctor_rec_thms] nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss ctrss ctr_defss [folds, recs] [fold_defs, rec_defs] lthy = let @@ -677,7 +677,7 @@ (fold_thmss, code_simp_attrs), (rec_thmss, code_simp_attrs)) end; -fun derive_coinduct_unfold_corec_thms_for_types pre_bnfs [dtor_unfolds, dtor_corecs] dtor_coinduct +fun derive_coinduct_coiters_thms_for_types pre_bnfs [dtor_unfolds, dtor_corecs] dtor_coinduct dtor_strong_induct dtor_ctors [dtor_unfold_thms, dtor_corec_thms] nesting_bnfs nested_bnfs fpTs Cs As kss mss ns ctr_defss ctr_sugars [unfolds, corecs] [unfold_defs, corec_defs] lthy = let @@ -705,7 +705,7 @@ val sel_thmsss = map #sel_thmss ctr_sugars; val ((cs, cpss, [((pgss, crssss, cgssss), _), ((phss, csssss, chssss), _)]), names_lthy0) = - mk_unfold_corec_args_types Cs ns mss [dtor_unfold_fun_Ts, dtor_corec_fun_Ts] lthy; + mk_coiters_args_types Cs ns mss [dtor_unfold_fun_Ts, dtor_corec_fun_Ts] lthy; val (((rs, us'), vs'), names_lthy) = names_lthy0 @@ -1099,8 +1099,8 @@ val kss = map (fn n => 1 upto n) ns; val mss = map (map length) ctr_Tsss; - val ((xtor_co_iterss', fold_rec_args_types, unfold_corec_args_types), lthy) = - mk_un_fold_co_rec_prelims fp fpTs Cs ns mss (transpose xtor_co_iterss0) lthy; + val ((xtor_co_iterss', iters_args_types, coiters_args_types), lthy) = + mk_un_fold_co_rec_prelims fp fpTs Cs ns mss xtor_co_iterss0 lthy; fun define_ctrs_case_for_type ((((((((((((((((((((((((fp_bnf, fp_b), fpT), C), ctor), dtor), xtor_co_iters), ctor_dtor), dtor_ctor), ctor_inject), pre_map_def), pre_set_defs), @@ -1293,8 +1293,8 @@ (wrap_ctrs #> derive_maps_sets_rels ##>> - (if fp = Least_FP then define_iters [foldN, recN] (the fold_rec_args_types) - else define_coiters [unfoldN, corecN] (the unfold_corec_args_types)) + (if fp = Least_FP then define_iters [foldN, recN] (the iters_args_types) + else define_coiters [unfoldN, corecN] (the coiters_args_types)) mk_binding fpTs Cs xtor_co_iters #> massage_res, lthy') end; @@ -1310,15 +1310,15 @@ injects @ distincts @ case_thms @ co_recs @ un_folds @ mapsx @ rel_injects @ rel_distincts @ flat setss); - fun derive_and_note_induct_fold_rec_thms_for_types + fun derive_and_note_induct_iters_thms_for_types ((((mapsx, rel_injects, rel_distincts, setss), (ctrss, _, ctr_defss, ctr_sugars)), (iterss', iter_defss')), lthy) = let val ((induct_thm, induct_thms, induct_attrs), (fold_thmss, fold_attrs), (rec_thmss, rec_attrs)) = - derive_induct_fold_rec_thms_for_types pre_bnfs xtor_co_iterss' - (the fold_rec_args_types) xtor_co_induct (transpose xtor_co_iter_thmss) nesting_bnfs - nested_bnfs fpTs Cs Xs ctrXs_Tsss ctrss ctr_defss iterss' iter_defss' lthy; + derive_induct_iters_thms_for_types pre_bnfs xtor_co_iterss' (the iters_args_types) + xtor_co_induct (transpose xtor_co_iter_thmss) nesting_bnfs nested_bnfs fpTs Cs Xs + ctrXs_Tsss ctrss ctr_defss iterss' iter_defss' lthy; val induct_type_attr = Attrib.internal o K o Induct.induct_type; @@ -1342,7 +1342,7 @@ induct_thm [fold_thmss, rec_thmss] end; - fun derive_and_note_coinduct_unfold_corec_thms_for_types + fun derive_and_note_coinduct_coiters_thms_for_types ((((mapsx, rel_injects, rel_distincts, setss), (_, _, ctr_defss, ctr_sugars)), (coiterss', coiter_defss')), lthy) = let @@ -1353,7 +1353,7 @@ (disc_unfold_thmss, disc_corec_thmss, disc_coiter_attrs), (disc_unfold_iff_thmss, disc_corec_iff_thmss, disc_coiter_iff_attrs), (sel_unfold_thmss, sel_corec_thmss, sel_coiter_attrs)) = - derive_coinduct_unfold_corec_thms_for_types pre_bnfs xtor_co_iterss' xtor_co_induct + derive_coinduct_coiters_thms_for_types pre_bnfs xtor_co_iterss' xtor_co_induct xtor_strong_co_induct dtor_ctors (transpose xtor_co_iter_thmss) nesting_bnfs nested_bnfs fpTs Cs As kss mss ns ctr_defss ctr_sugars coiterss' coiter_defss' lthy; @@ -1408,8 +1408,8 @@ kss ~~ mss ~~ ctr_bindingss ~~ ctr_mixfixess ~~ ctr_Tsss ~~ disc_bindingss ~~ sel_bindingsss ~~ raw_sel_defaultsss) |> wrap_types_etc - |> (if fp = Least_FP then derive_and_note_induct_fold_rec_thms_for_types - else derive_and_note_coinduct_unfold_corec_thms_for_types); + |> (if fp = Least_FP then derive_and_note_induct_iters_thms_for_types + else derive_and_note_coinduct_coiters_thms_for_types); val timer = time (timer ("Constructors, discriminators, selectors, etc., for the new " ^ datatype_word fp));