--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Tue Aug 20 17:39:07 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Tue Aug 20 17:39:08 2013 +0200
@@ -24,6 +24,9 @@
val morph_fp_sugar: morphism -> fp_sugar -> fp_sugar
val fp_sugar_of: Proof.context -> string -> fp_sugar option
+ val co_induct_of: 'a list -> 'a
+ val strong_co_induct_of: 'a list -> 'a
+
val tvar_subst: theory -> typ list -> typ list -> ((string * int) * typ) list
val exists_subtype_in: typ list -> typ -> bool
val flat_rec_arg_args: 'a list list -> 'a list
@@ -59,7 +62,7 @@
(term list * thm list) * Proof.context
val derive_induct_iters_thms_for_types: BNF_Def.bnf list ->
(typ list list * typ list list list list * term list list * term list list list list) list ->
- thm list -> thm list list -> BNF_Def.bnf list -> BNF_Def.bnf list -> typ list -> typ 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 list * thm * Args.src list) * (thm list list * Args.src list)
@@ -67,7 +70,7 @@
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 list -> thm list -> thm list list -> BNF_Def.bnf list -> typ list -> typ list -> typ 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 list * thm) list * Args.src list)
@@ -139,6 +142,9 @@
val fp_sugar_of = Symtab.lookup o Data.get o Context.Proof;
+fun co_induct_of (i :: _) = i;
+fun strong_co_induct_of [_, s] = s;
+
fun register_fp_sugar key fp_sugar =
Local_Theory.declaration {syntax = false, pervasive = true}
(fn phi => Data.map (Symtab.default (key, morph_fp_sugar phi fp_sugar)));
@@ -557,7 +563,7 @@
(map3 generate_coiter coiterNs coiter_args_typess' dtor_coiters) lthy
end;
-fun derive_induct_iters_thms_for_types pre_bnfs [fold_args_types, rec_args_types] [ctor_induct]
+fun derive_induct_iters_thms_for_types pre_bnfs [fold_args_types, rec_args_types] ctor_induct
ctor_iter_thmss nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss ctrss ctr_defss iterss iter_defss
lthy =
let
@@ -718,7 +724,7 @@
fun derive_coinduct_coiters_thms_for_types pre_bnfs (z, cs, cpss,
coiters_args_types as [((pgss, crgsss), _), ((phss, cshsss), _)])
- dtor_coinducts dtor_ctors dtor_coiter_thmss nesting_bnfs fpTs Cs As kss mss ns ctr_defss
+ 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 =
let
val coiterss' = transpose coiterss;
@@ -823,6 +829,11 @@
(if nn = 1 then thm RS mp else funpow nn (fn thm => reassoc_conjs (thm RS mp_conj)) thm)
|> Drule.zero_var_indexes
|> `(conj_dests nn);
+
+ val rel_eqs = map rel_eq_of_bnf pre_bnfs;
+ val rel_monos = map rel_mono_of_bnf pre_bnfs;
+ val dtor_coinducts =
+ [dtor_coinduct, mk_strong_coinduct_thm dtor_coinduct rel_eqs rel_monos lthy];
in
map2 (postproc nn oo prove) dtor_coinducts goals
end;
@@ -1096,7 +1107,7 @@
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_inducts, dtor_ctors, ctor_dtors, ctor_injects,
+ 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)) =
fp_bnf (construct_fp mixfixes map_bs rel_bs set_bss) fp_bs (map dest_TFree unsorted_As) fp_eqs
no_defs_lthy0;
@@ -1351,7 +1362,7 @@
let
val ((induct_thms, induct_thm, induct_attrs), (fold_thmss, fold_attrs),
(rec_thmss, rec_attrs)) =
- derive_induct_iters_thms_for_types pre_bnfs (the iters_args_types) xtor_co_inducts
+ derive_induct_iters_thms_for_types pre_bnfs (the iters_args_types) xtor_co_induct
xtor_co_iter_thmss nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss ctrss ctr_defss iterss
iter_defss lthy;
@@ -1388,7 +1399,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_coiters_thms_for_types pre_bnfs (the coiters_args_types) xtor_co_inducts
+ 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;
--- a/src/HOL/BNF/Tools/bnf_fp_util.ML Tue Aug 20 17:39:07 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_util.ML Tue Aug 20 17:39:08 2013 +0200
@@ -17,7 +17,7 @@
ctors: term list,
dtors: term list,
xtor_co_iterss: term list list,
- xtor_co_inducts: thm list,
+ xtor_co_induct: thm,
dtor_ctors: thm list,
ctor_dtors: thm list,
ctor_injects: thm list,
@@ -29,8 +29,6 @@
val morph_fp_result: morphism -> fp_result -> fp_result
val eq_fp_result: fp_result * fp_result -> bool
- 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
@@ -179,7 +177,7 @@
val mk_xtor_un_fold_o_map_thms: fp_kind -> bool -> int -> thm -> thm list -> thm list ->
thm list -> thm list -> thm list
- val mk_strong_coinduct_thm: int -> thm -> thm list -> thm list -> Proof.context -> thm
+ val mk_strong_coinduct_thm: thm -> thm list -> thm list -> Proof.context -> thm
val fp_bnf: (binding list -> (string * sort) list -> typ list * typ list list ->
BNF_Def.bnf list -> local_theory -> 'a) ->
@@ -205,7 +203,7 @@
ctors: term list,
dtors: term list,
xtor_co_iterss: term list list,
- xtor_co_inducts: thm list,
+ xtor_co_induct: thm,
dtor_ctors: thm list,
ctor_dtors: thm list,
ctor_injects: thm list,
@@ -215,7 +213,7 @@
xtor_co_iter_thmss: thm list list,
rel_co_induct_thm: thm};
-fun morph_fp_result phi {Ts, bnfs, ctors, dtors, xtor_co_iterss, xtor_co_inducts, dtor_ctors,
+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,
rel_co_induct_thm} =
{Ts = map (Morphism.typ phi) Ts,
@@ -223,7 +221,7 @@
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_inducts = map (Morphism.thm phi) xtor_co_inducts,
+ xtor_co_induct = Morphism.thm phi xtor_co_induct,
dtor_ctors = map (Morphism.thm phi) dtor_ctors,
ctor_dtors = map (Morphism.thm phi) ctor_dtors,
ctor_injects = map (Morphism.thm phi) ctor_injects,
@@ -236,9 +234,6 @@
fun eq_fp_result ({bnfs = bnfs1, ...} : fp_result, {bnfs = bnfs2, ...} : fp_result) =
eq_list eq_bnf (bnfs1, bnfs2);
-fun co_induct_of (i :: _) = i;
-fun strong_co_induct_of [_, s] = s;
-
fun un_fold_of [f, _] = f;
fun co_rec_of [_, r] = r;
@@ -554,9 +549,10 @@
split_conj_thm (un_fold_unique OF map (fp_case fp I mk_sym) unique_prems)
end;
-fun mk_strong_coinduct_thm m coind rel_eqs rel_monos ctxt =
+fun mk_strong_coinduct_thm coind rel_eqs rel_monos ctxt =
let
val n = Thm.nprems_of coind;
+ val m = Thm.nprems_of (hd rel_monos) - n;
fun mk_inst phi = (phi, mk_union (phi, HOLogic.eq_const (fst (dest_pred2T (fastype_of phi)))))
|> pairself (certify ctxt);
val insts = Term.add_vars (Thm.prop_of coind) [] |> rev |> take n |> map (mk_inst o Var);
--- a/src/HOL/BNF/Tools/bnf_gfp.ML Tue Aug 20 17:39:07 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML Tue Aug 20 17:39:08 2013 +0200
@@ -2080,10 +2080,6 @@
(dtor_map_coinduct, rev (Term.add_tfrees dtor_map_coinduct_goal []), dtor_coinduct)
end;
- (* TODO: Get rid of strong versions (since these can easily be derived from the weak ones). *)
- val dtor_strong_coinduct_thm =
- mk_strong_coinduct_thm m dtor_coinduct_thm rel_eqs rel_monos lthy;
-
val timer = time (timer "coinduction");
fun mk_dtor_map_DEADID_thm dtor_inject map_id =
@@ -2901,7 +2897,7 @@
timer;
({Ts = Ts, bnfs = Jbnfs, ctors = ctors, dtors = dtors,
xtor_co_iterss = transpose [unfolds, corecs],
- xtor_co_inducts = [dtor_coinduct_thm, dtor_strong_coinduct_thm], dtor_ctors = dtor_ctor_thms,
+ xtor_co_induct = dtor_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 Tue Aug 20 17:39:07 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML Tue Aug 20 17:39:08 2013 +0200
@@ -1858,7 +1858,7 @@
in
timer;
({Ts = Ts, bnfs = Ibnfs, ctors = ctors, dtors = dtors, xtor_co_iterss = transpose [folds, recs],
- xtor_co_inducts = [ctor_induct_thm], dtor_ctors = dtor_ctor_thms, ctor_dtors = ctor_dtor_thms,
+ 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,
xtor_co_iter_thmss = transpose [ctor_fold_thms, ctor_rec_thms],