--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Fri Jun 07 12:00:29 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Fri Jun 07 12:11:55 2013 +0200
@@ -53,7 +53,7 @@
(term list * thm list) * Proof.context
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 ->
+ thm list -> 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)
@@ -61,7 +61,7 @@
val derive_coinduct_coiters_thms_for_types: BNF_Def.bnf list -> term list list ->
term list * term list list
* ((term list list * term list list list list * term list list list list) * 'a) list ->
- thm -> thm -> thm list -> thm list list -> BNF_Def.bnf list -> BNF_Def.bnf list -> typ list ->
+ thm list -> 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 ->
(thm * thm list * thm * thm list * Args.src list)
@@ -520,7 +520,7 @@
end;
fun derive_induct_iters_thms_for_types pre_bnfs (ctor_iters1 :: _) [fold_args_types, rec_args_types]
- ctor_induct ctor_iter_thmss nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss ctrss ctr_defss
+ [ctor_induct] ctor_iter_thmss nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss ctrss ctr_defss
iterss iter_defss lthy =
let
val iterss' = transpose iterss;
@@ -682,8 +682,8 @@
fun derive_coinduct_coiters_thms_for_types pre_bnfs (dtor_coiters1 :: _)
(cs, cpss,
[(unfold_args as (pgss, crssss, cgssss), _), (corec_args as (phss, csssss, chssss), _)])
- dtor_coinduct dtor_strong_induct dtor_ctors dtor_coiter_thmss nesting_bnfs nested_bnfs fpTs Cs
- As kss mss ns ctr_defss ctr_sugars coiterss coiter_defss lthy =
+ dtor_coinducts dtor_ctors dtor_coiter_thmss nesting_bnfs nested_bnfs fpTs Cs As kss mss ns
+ ctr_defss ctr_sugars coiterss coiter_defss lthy =
let
val coiterss' = transpose coiterss;
val coiter_defss' = transpose coiter_defss;
@@ -794,7 +794,8 @@
|> Drule.zero_var_indexes
|> `(conj_dests nn);
in
- (postproc nn (prove dtor_coinduct goal), postproc nn (prove dtor_strong_induct strong_goal))
+ (postproc nn (prove (co_induct_of dtor_coinducts) goal),
+ postproc nn (prove (strong_co_induct_of dtor_coinducts) strong_goal))
end;
fun mk_coinduct_concls ms discs ctrs =
@@ -1057,9 +1058,8 @@
map dest_TFree Xs ~~ map (Term.typ_subst_atomic (As ~~ unsorted_As)) ctrXs_sum_prod_Ts;
val (pre_bnfs, (fp_res as {bnfs = fp_bnfs as any_fp_bnf :: _, ctors = ctors0, dtors = dtors0,
- xtor_co_iterss = xtor_co_iterss0, xtor_co_induct, xtor_strong_co_induct, dtor_ctors,
- ctor_dtors, ctor_injects, xtor_map_thms, xtor_set_thmss, xtor_rel_thms,
- xtor_co_iter_thmss, ...}, lthy)) =
+ xtor_co_iterss = xtor_co_iterss0, xtor_co_inducts, dtor_ctors, ctor_dtors, ctor_injects,
+ xtor_map_thms, xtor_set_thmss, xtor_rel_thms, xtor_co_iter_thmss, ...}, lthy)) =
fp_bnf (construct_fp mixfixes map_bs rel_bs set_bss) fp_bs (map dest_TFree unsorted_As) fp_eqs
no_defs_lthy0;
@@ -1324,7 +1324,7 @@
val ((induct_thm, induct_thms, induct_attrs), (fold_thmss, fold_attrs),
(rec_thmss, rec_attrs)) =
derive_induct_iters_thms_for_types pre_bnfs xtor_co_iterss (the iters_args_types)
- xtor_co_induct xtor_co_iter_thmss nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss ctrss
+ xtor_co_inducts 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;
@@ -1360,10 +1360,9 @@
(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_coiters_thms_for_types pre_bnfs xtor_co_iterss
- (the coiters_args_types) xtor_co_induct xtor_strong_co_induct dtor_ctors
- xtor_co_iter_thmss nesting_bnfs nested_bnfs fpTs Cs As kss mss ns ctr_defss ctr_sugars
- coiterss coiter_defss lthy;
+ derive_coinduct_coiters_thms_for_types pre_bnfs xtor_co_iterss (the coiters_args_types)
+ xtor_co_inducts dtor_ctors xtor_co_iter_thmss nesting_bnfs nested_bnfs fpTs Cs As kss
+ mss ns ctr_defss ctr_sugars coiterss coiter_defss lthy;
val coinduct_type_attr = Attrib.internal o K o Induct.coinduct_type;
--- a/src/HOL/BNF/Tools/bnf_fp_util.ML Fri Jun 07 12:00:29 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_util.ML Fri Jun 07 12:11:55 2013 +0200
@@ -16,8 +16,7 @@
ctors: term list,
dtors: term list,
xtor_co_iterss: term list list,
- xtor_co_induct: thm,
- xtor_strong_co_induct: thm,
+ xtor_co_inducts: thm list,
dtor_ctors: thm list,
ctor_dtors: thm list,
ctor_injects: thm list,
@@ -28,7 +27,7 @@
val morph_fp_result: morphism -> fp_result -> fp_result
val eq_fp_result: fp_result * fp_result -> bool
- val weak_co_induct_of: 'a list -> 'a
+ val co_induct_of: 'a list -> 'a
val strong_co_induct_of: 'a list -> 'a
val un_fold_of: 'a list -> 'a
val co_rec_of: 'a list -> 'a
@@ -188,8 +187,7 @@
ctors: term list,
dtors: term list,
xtor_co_iterss: term list list,
- xtor_co_induct: thm,
- xtor_strong_co_induct: thm,
+ xtor_co_inducts: thm list,
dtor_ctors: thm list,
ctor_dtors: thm list,
ctor_injects: thm list,
@@ -198,16 +196,14 @@
xtor_rel_thms: thm list,
xtor_co_iter_thmss: thm list list};
-fun morph_fp_result phi {Ts, bnfs, ctors, dtors, xtor_co_iterss, xtor_co_induct,
- xtor_strong_co_induct, dtor_ctors, ctor_dtors, ctor_injects, xtor_map_thms, xtor_set_thmss,
- xtor_rel_thms, xtor_co_iter_thmss} =
+fun morph_fp_result phi {Ts, bnfs, ctors, dtors, xtor_co_iterss, xtor_co_inducts, dtor_ctors,
+ ctor_dtors, ctor_injects, xtor_map_thms, xtor_set_thmss, xtor_rel_thms, xtor_co_iter_thmss} =
{Ts = map (Morphism.typ phi) Ts,
bnfs = map (morph_bnf phi) bnfs,
ctors = map (Morphism.term phi) ctors,
dtors = map (Morphism.term phi) dtors,
xtor_co_iterss = map (map (Morphism.term phi)) xtor_co_iterss,
- xtor_co_induct = Morphism.thm phi xtor_co_induct,
- xtor_strong_co_induct = Morphism.thm phi xtor_strong_co_induct,
+ xtor_co_inducts = map (Morphism.thm phi) xtor_co_inducts,
dtor_ctors = map (Morphism.thm phi) dtor_ctors,
ctor_dtors = map (Morphism.thm phi) ctor_dtors,
ctor_injects = map (Morphism.thm phi) ctor_injects,
@@ -219,7 +215,7 @@
fun eq_fp_result ({bnfs = bnfs1, ...} : fp_result, {bnfs = bnfs2, ...} : fp_result) =
eq_list eq_bnf (bnfs1, bnfs2);
-fun weak_co_induct_of [w, _] = w;
+fun co_induct_of (i :: _) = i;
fun strong_co_induct_of [_, s] = s;
fun un_fold_of [f, _] = f;
--- a/src/HOL/BNF/Tools/bnf_gfp.ML Fri Jun 07 12:00:29 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML Fri Jun 07 12:11:55 2013 +0200
@@ -3108,8 +3108,8 @@
in
timer;
({Ts = Ts, bnfs = Jbnfs, ctors = ctors, dtors = dtors,
- xtor_co_iterss = transpose [unfolds, corecs], xtor_co_induct = dtor_coinduct_thm,
- xtor_strong_co_induct = dtor_strong_coinduct_thm, dtor_ctors = dtor_ctor_thms,
+ xtor_co_iterss = transpose [unfolds, corecs],
+ xtor_co_inducts = [dtor_coinduct_thm, dtor_strong_coinduct_thm], dtor_ctors = dtor_ctor_thms,
ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms,
xtor_map_thms = folded_dtor_map_thms, xtor_set_thmss = folded_dtor_set_thmss',
xtor_rel_thms = dtor_Jrel_thms,
--- a/src/HOL/BNF/Tools/bnf_lfp.ML Fri Jun 07 12:00:29 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML Fri Jun 07 12:11:55 2013 +0200
@@ -1857,11 +1857,9 @@
in
timer;
({Ts = Ts, bnfs = Ibnfs, ctors = ctors, dtors = dtors, xtor_co_iterss = transpose [folds, recs],
- xtor_co_induct = ctor_induct_thm,
- xtor_strong_co_induct = ctor_induct_thm, dtor_ctors = dtor_ctor_thms,
- ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms,
- xtor_map_thms = folded_ctor_map_thms, xtor_set_thmss = folded_ctor_set_thmss',
- xtor_rel_thms = ctor_Irel_thms,
+ xtor_co_inducts = [ctor_induct_thm], dtor_ctors = dtor_ctor_thms, ctor_dtors = ctor_dtor_thms,
+ ctor_injects = ctor_inject_thms, xtor_map_thms = folded_ctor_map_thms,
+ xtor_set_thmss = folded_ctor_set_thmss', xtor_rel_thms = ctor_Irel_thms,
xtor_co_iter_thmss = transpose [ctor_fold_thms, ctor_rec_thms]},
lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
end;