--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Mon Aug 26 12:14:41 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Mon Aug 26 13:44:46 2013 +0200
@@ -70,9 +70,10 @@
val derive_coinduct_coiters_thms_for_types: BNF_Def.bnf list ->
string * term list * term list list * ((term list list * term list list list)
* (typ list * typ list list)) list ->
- thm -> thm list -> thm list 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 -> (thm list -> thm list) -> local_theory ->
+ thm -> thm list -> thm list -> thm list 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 -> (thm list -> thm list) ->
+ local_theory ->
((thm list * thm) list * Args.src list)
* (thm list list * thm list list * Args.src list)
* (thm list list * thm list list) * (thm list list * thm list list * Args.src list)
@@ -727,9 +728,15 @@
fun derive_coinduct_coiters_thms_for_types pre_bnfs (z, cs, cpss,
coiters_args_types as [((pgss, crgsss), _), ((phss, cshsss), _)])
- dtor_coinduct dtor_ctors dtor_coiter_thmss nesting_bnfs fpTs Cs As kss mss ns ctr_defss
- ctr_sugars coiterss coiter_defss export_args lthy =
+ dtor_coinduct dtor_injects dtor_ctors dtor_coiter_thmss nesting_bnfs fpTs Cs As kss mss ns
+ ctr_defss ctr_sugars coiterss coiter_defss export_args lthy =
let
+ fun mk_ctor_dtor_coiter_thm dtor_inject dtor_ctor coiter =
+ iffD1 OF [dtor_inject, trans OF [coiter, dtor_ctor RS sym]];
+
+ val ctor_dtor_coiter_thmss =
+ map3 (map oo mk_ctor_dtor_coiter_thm) dtor_injects dtor_ctors dtor_coiter_thmss;
+
val coiterss' = transpose coiterss;
val coiter_defss' = transpose coiter_defss;
@@ -896,10 +903,10 @@
val unfold_tacss =
map3 (map oo mk_coiter_tac unfold_defs nesting_map_ids'')
- (map un_fold_of dtor_coiter_thmss) pre_map_defs ctr_defss;
+ (map un_fold_of ctor_dtor_coiter_thmss) pre_map_defs ctr_defss;
val corec_tacss =
map3 (map oo mk_coiter_tac corec_defs nesting_map_ids'')
- (map co_rec_of dtor_coiter_thmss) pre_map_defs ctr_defss;
+ (map co_rec_of ctor_dtor_coiter_thmss) pre_map_defs ctr_defss;
fun prove goal tac =
Goal.prove_sorry lthy [] [] goal (tac o #context)
@@ -1111,7 +1118,8 @@
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, dtor_ctors, ctor_dtors, ctor_injects,
- xtor_map_thms, xtor_set_thmss, xtor_rel_thms, xtor_co_iter_thmss, ...}, lthy)) =
+ dtor_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;
@@ -1404,8 +1412,8 @@
(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 (the coiters_args_types) xtor_co_induct
- dtor_ctors xtor_co_iter_thmss nesting_bnfs fpTs Cs As kss mss ns ctr_defss ctr_sugars
- coiterss coiter_defss (Proof_Context.export lthy' no_defs_lthy) lthy;
+ dtor_injects dtor_ctors xtor_co_iter_thmss nesting_bnfs fpTs Cs As kss mss ns ctr_defss
+ ctr_sugars coiterss coiter_defss (Proof_Context.export lthy' no_defs_lthy) lthy;
val coinduct_type_attr = Attrib.internal o K o Induct.coinduct_type;
--- a/src/HOL/BNF/Tools/bnf_fp_util.ML Mon Aug 26 12:14:41 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_util.ML Mon Aug 26 13:44:46 2013 +0200
@@ -21,6 +21,7 @@
dtor_ctors: thm list,
ctor_dtors: thm list,
ctor_injects: thm list,
+ dtor_injects: thm list,
xtor_map_thms: thm list,
xtor_set_thmss: thm list list,
xtor_rel_thms: thm list,
@@ -210,6 +211,7 @@
dtor_ctors: thm list,
ctor_dtors: thm list,
ctor_injects: thm list,
+ dtor_injects: thm list,
xtor_map_thms: thm list,
xtor_set_thmss: thm list list,
xtor_rel_thms: thm list,
@@ -218,8 +220,8 @@
rel_co_induct_thm: thm};
fun morph_fp_result phi {Ts, bnfs, ctors, dtors, xtor_co_iterss, xtor_co_induct, dtor_ctors,
- ctor_dtors, ctor_injects, xtor_map_thms, xtor_set_thmss, xtor_rel_thms, xtor_co_iter_thmss,
- xtor_co_iter_o_map_thmss, rel_co_induct_thm} =
+ ctor_dtors, ctor_injects, dtor_injects, xtor_map_thms, xtor_set_thmss, xtor_rel_thms,
+ xtor_co_iter_thmss, xtor_co_iter_o_map_thmss, rel_co_induct_thm} =
{Ts = map (Morphism.typ phi) Ts,
bnfs = map (morph_bnf phi) bnfs,
ctors = map (Morphism.term phi) ctors,
@@ -229,6 +231,7 @@
dtor_ctors = map (Morphism.thm phi) dtor_ctors,
ctor_dtors = map (Morphism.thm phi) ctor_dtors,
ctor_injects = map (Morphism.thm phi) ctor_injects,
+ dtor_injects = map (Morphism.thm phi) dtor_injects,
xtor_map_thms = map (Morphism.thm phi) xtor_map_thms,
xtor_set_thmss = map (map (Morphism.thm phi)) xtor_set_thmss,
xtor_rel_thms = map (Morphism.thm phi) xtor_rel_thms,
--- a/src/HOL/BNF/Tools/bnf_gfp.ML Mon Aug 26 12:14:41 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML Mon Aug 26 13:44:46 2013 +0200
@@ -1923,12 +1923,6 @@
val ctor_inject_thms = map (fn thm => thm RS @{thm inj_eq}) inj_ctor_thms;
val ctor_exhaust_thms = map (fn thm => thm RS exE) ctor_nchotomy_thms;
- fun mk_ctor_dtor_unfold_like_thm dtor_inject dtor_ctor unfold =
- iffD1 OF [dtor_inject, trans OF [unfold, dtor_ctor RS sym]];
-
- val ctor_dtor_unfold_thms =
- map3 mk_ctor_dtor_unfold_like_thm dtor_inject_thms dtor_ctor_thms dtor_unfold_thms;
-
val timer = time (timer "ctor definitions & thms");
val corec_Inl_sum_thms =
@@ -2015,9 +2009,6 @@
|> Local_Defs.unfold lthy (@{thms o_sum_case o_id id_o o_assoc sum_case_o_inj(1)} @
map_ids @ sym_map_comps) OF replicate n @{thm arg_cong2[of _ _ _ _ sum_case, OF refl]});
- val ctor_dtor_corec_thms =
- map3 mk_ctor_dtor_unfold_like_thm dtor_inject_thms dtor_ctor_thms dtor_corec_thms;
-
val timer = time (timer "corec definitions & thms");
val (dtor_map_coinduct_thm, coinduct_params, dtor_coinduct_thm) =
@@ -2876,8 +2867,6 @@
val notes =
[(ctor_dtorN, ctor_dtor_thms),
- (ctor_dtor_corecN, ctor_dtor_corec_thms),
- (ctor_dtor_unfoldN, ctor_dtor_unfold_thms),
(ctor_exhaustN, ctor_exhaust_thms),
(ctor_injectN, ctor_inject_thms),
(dtor_corecN, dtor_corec_thms),
@@ -2899,10 +2888,11 @@
({Ts = Ts, bnfs = Jbnfs, ctors = ctors, dtors = dtors,
xtor_co_iterss = transpose [unfolds, corecs],
xtor_co_induct = dtor_coinduct_thm, dtor_ctors = dtor_ctor_thms,
- ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms,
+ ctor_dtors = ctor_dtor_thms,
+ ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms,
xtor_map_thms = folded_dtor_map_thms, xtor_set_thmss = folded_dtor_set_thmss',
xtor_rel_thms = dtor_Jrel_thms,
- xtor_co_iter_thmss = transpose [ctor_dtor_unfold_thms, ctor_dtor_corec_thms],
+ xtor_co_iter_thmss = transpose [dtor_unfold_thms, dtor_corec_thms],
xtor_co_iter_o_map_thmss = transpose [dtor_unfold_o_map_thms, dtor_corec_o_map_thms],
rel_co_induct_thm = Jrel_coinduct_thm},
lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
--- a/src/HOL/BNF/Tools/bnf_lfp.ML Mon Aug 26 12:14:41 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML Mon Aug 26 13:44:46 2013 +0200
@@ -1860,8 +1860,9 @@
timer;
({Ts = Ts, bnfs = Ibnfs, ctors = ctors, dtors = dtors, xtor_co_iterss = transpose [folds, recs],
xtor_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,
+ ctor_injects = ctor_inject_thms, dtor_injects = dtor_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],
xtor_co_iter_o_map_thmss = transpose [ctor_fold_o_map_thms, ctor_rec_o_map_thms],
rel_co_induct_thm = Irel_induct_thm},