# HG changeset patch # User traytel # Date 1377013148 -7200 # Node ID d81211f61a1b4e6bb07c8b8c19f23acd0b328383 # Parent ec38e9f4352f19240dc7dad9367bc6ddb33e10bc moved derivation of strong coinduction to sugar diff -r ec38e9f4352f -r d81211f61a1b src/HOL/BNF/Tools/bnf_fp_def_sugar.ML --- 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; diff -r ec38e9f4352f -r d81211f61a1b src/HOL/BNF/Tools/bnf_fp_util.ML --- 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); diff -r ec38e9f4352f -r d81211f61a1b src/HOL/BNF/Tools/bnf_gfp.ML --- 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, diff -r ec38e9f4352f -r d81211f61a1b src/HOL/BNF/Tools/bnf_lfp.ML --- 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],