# HG changeset patch # User blanchet # Date 1367330312 -7200 # Node ID 5c552de1d8d1c4ac674bb403ab4a6a5a60562313 # Parent 1999b2e0b15787518c82d8ceaf5c91d3532e5d7d added constructors to data structure diff -r 1999b2e0b157 -r 5c552de1d8d1 src/HOL/BNF/Tools/bnf_ctr_sugar.ML --- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Tue Apr 30 13:45:43 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Tue Apr 30 15:58:32 2013 +0200 @@ -8,7 +8,8 @@ signature BNF_CTR_SUGAR = sig type ctr_wrap_result = - {discs: term list, + {ctrs: term list, + discs: term list, selss: term list list, exhaust: thm, injects: thm list, @@ -46,7 +47,8 @@ open BNF_Ctr_Sugar_Tactics type ctr_wrap_result = - {discs: term list, + {ctrs: term list, + discs: term list, selss: term list list, exhaust: thm, injects: thm list, @@ -56,9 +58,10 @@ discIs: thm list, sel_thmss: thm list list}; -fun morph_ctr_wrap_result phi {discs, selss, exhaust, injects, distincts, case_thms, disc_thmss, - discIs, sel_thmss} = - {discs = map (Morphism.term phi) discs, +fun morph_ctr_wrap_result phi {ctrs, discs, selss, exhaust, injects, distincts, case_thms, + disc_thmss, discIs, sel_thmss} = + {ctrs = map (Morphism.term phi) ctrs, + discs = map (Morphism.term phi) discs, selss = map (map (Morphism.term phi)) selss, exhaust = Morphism.thm phi exhaust, injects = map (Morphism.thm phi) injects, @@ -699,7 +702,7 @@ [(map (fn th => th RS notE) distinct_thms, safe_elim_attrs)] |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])])); in - ({discs = discs, selss = selss, exhaust = exhaust_thm, injects = inject_thms, + ({ctrs = ctrs, discs = discs, selss = selss, exhaust = exhaust_thm, injects = inject_thms, distincts = distinct_thms, case_thms = case_thms, disc_thmss = disc_thmss, discIs = discI_thms, sel_thmss = sel_thmss}, lthy diff -r 1999b2e0b157 -r 5c552de1d8d1 src/HOL/BNF/Tools/bnf_fp.ML --- a/src/HOL/BNF/Tools/bnf_fp.ML Tue Apr 30 13:45:43 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp.ML Tue Apr 30 15:58:32 2013 +0200 @@ -10,8 +10,8 @@ sig type fp_result = {bnfs: BNF_Def.bnf list, + ctors: term list, dtors: term list, - ctors: term list, folds: term list, recs: term list, induct: thm, @@ -25,6 +25,7 @@ fold_thms: thm list, rec_thms: thm list} + val fp_name_of_ctor: term -> string val morph_fp_result: morphism -> fp_result -> fp_result val eq_fp_result: fp_result * fp_result -> bool @@ -173,8 +174,8 @@ type fp_result = {bnfs: BNF_Def.bnf list, + ctors: term list, dtors: term list, - ctors: term list, folds: term list, recs: term list, induct: thm, @@ -188,11 +189,13 @@ fold_thms: thm list, rec_thms: thm list}; -fun morph_fp_result phi {bnfs, dtors, ctors, folds, recs, induct, strong_induct, dtor_ctors, +val fp_name_of_ctor = fst o dest_Type o range_type o fastype_of; + +fun morph_fp_result phi {bnfs, ctors, dtors, folds, recs, induct, strong_induct, dtor_ctors, ctor_dtors, ctor_injects, map_thms, set_thmss, rel_thms, fold_thms, rec_thms} = {bnfs = map (morph_bnf phi) bnfs, + ctors = map (Morphism.term phi) ctors, dtors = map (Morphism.term phi) dtors, - ctors = map (Morphism.term phi) ctors, folds = map (Morphism.term phi) folds, recs = map (Morphism.term phi) recs, induct = Morphism.thm phi induct, diff -r 1999b2e0b157 -r 5c552de1d8d1 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Tue Apr 30 13:45:43 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Tue Apr 30 15:58:32 2013 +0200 @@ -25,9 +25,10 @@ val derive_coinduct_unfold_corec_thms_for_types: BNF_Def.bnf list -> term list -> term list -> thm -> thm -> thm list -> thm list -> thm list -> BNF_Def.bnf list -> BNF_Def.bnf list -> typ list -> typ list -> typ list -> int list list -> int list list -> int list -> - term list list -> thm list list -> BNF_Ctr_Sugar.ctr_wrap_result list -> term list -> - term list -> thm list -> thm list -> Proof.context -> - (thm * thm list * thm * thm list * Args.src list) * (thm list list * thm list list * 'e list) + thm list list -> BNF_Ctr_Sugar.ctr_wrap_result list -> term list -> term list -> thm list -> + thm list -> Proof.context -> + (thm * thm list * thm * 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) * (thm list list * thm list list * Args.src list) * (thm list list * thm list list * Args.src list) @@ -87,8 +88,6 @@ Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => Data.map (Symtab.update_new (key, morph_fp phi fp))); -val fp_name_of_ctor = fst o dest_Type o range_type o fastype_of; - fun register_fps lfp pre_bnfs (fp_res as {ctors, ...}) ctr_wrap_ress lthy = ((1, ctors), lthy) |> fold (fn ctr_wrap_res => fn ((kk, ctor :: ctors), lthy) => @@ -526,7 +525,7 @@ fun derive_coinduct_unfold_corec_thms_for_types pre_bnfs dtor_unfolds0 dtor_corecs0 dtor_coinduct dtor_strong_induct dtor_ctors dtor_unfold_thms dtor_corec_thms nesting_bnfs nested_bnfs fpTs Cs - As kss mss ns ctrss ctr_defss ctr_wrap_ress unfolds corecs unfold_defs corec_defs lthy = + As kss mss ns ctr_defss ctr_wrap_ress unfolds corecs unfold_defs corec_defs lthy = let val nn = length pre_bnfs; @@ -543,6 +542,7 @@ val (_, dtor_unfold_fun_Ts) = mk_fp_rec_like false As Cs dtor_unfolds0; val (_, dtor_corec_fun_Ts) = mk_fp_rec_like false As Cs dtor_corecs0; + val ctrss = map (map (mk_ctr As) o #ctrs) ctr_wrap_ress; val discss = map (map (mk_disc_or_sel As) o #discs) ctr_wrap_ress; val selsss = map (map (map (mk_disc_or_sel As)) o #selss) ctr_wrap_ress; val exhausts = map #exhaust ctr_wrap_ress; @@ -893,7 +893,7 @@ val fp_eqs = map dest_TFree Xs ~~ map (Term.typ_subst_atomic (As ~~ unsorted_As)) ctr_sum_prod_TsXs; - val (pre_bnfs, (fp_res as {bnfs = fp_bnfs as any_fp_bnf :: _, dtors = dtors0, ctors = ctors0, + val (pre_bnfs, (fp_res as {bnfs = fp_bnfs as any_fp_bnf :: _, ctors = ctors0, dtors = dtors0, folds = fp_folds0, recs = fp_recs0, induct = fp_induct, strong_induct = fp_strong_induct, dtor_ctors, ctor_dtors, ctor_injects, map_thms = fp_map_thms, set_thmss = fp_set_thmss, rel_thms = fp_rel_thms, fold_thms = fp_fold_thms, rec_thms = fp_rec_thms}, lthy)) = @@ -1334,7 +1334,7 @@ (sel_unfold_thmss, sel_corec_thmss, sel_corec_like_attrs)) = derive_coinduct_unfold_corec_thms_for_types pre_bnfs fp_folds0 fp_recs0 fp_induct fp_strong_induct dtor_ctors fp_fold_thms fp_rec_thms nesting_bnfs nested_bnfs fpTs Cs As - kss mss ns ctrss ctr_defss ctr_wrap_ress unfolds corecs unfold_defs corec_defs lthy; + kss mss ns ctr_defss ctr_wrap_ress unfolds corecs unfold_defs corec_defs lthy; val coinduct_type_attr = Attrib.internal o K o Induct.coinduct_type; diff -r 1999b2e0b157 -r 5c552de1d8d1 src/HOL/BNF/Tools/bnf_gfp.ML --- a/src/HOL/BNF/Tools/bnf_gfp.ML Tue Apr 30 13:45:43 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML Tue Apr 30 15:58:32 2013 +0200 @@ -3029,7 +3029,7 @@ ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])) bs thmss) in - ({bnfs = Jbnfs, dtors = dtors, ctors = ctors, folds = unfolds, recs = corecs, + ({bnfs = Jbnfs, ctors = ctors, dtors = dtors, folds = unfolds, recs = corecs, induct = dtor_coinduct_thm, strong_induct = dtor_strong_coinduct_thm, dtor_ctors = dtor_ctor_thms, ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms, map_thms = folded_dtor_map_thms, set_thmss = folded_dtor_set_thmss', diff -r 1999b2e0b157 -r 5c552de1d8d1 src/HOL/BNF/Tools/bnf_lfp.ML --- a/src/HOL/BNF/Tools/bnf_lfp.ML Tue Apr 30 13:45:43 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML Tue Apr 30 15:58:32 2013 +0200 @@ -1852,7 +1852,7 @@ ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])) bs thmss) in - ({bnfs = Ibnfs, dtors = dtors, ctors = ctors, folds = folds, recs = recs, + ({bnfs = Ibnfs, ctors = ctors, dtors = dtors, folds = folds, recs = recs, induct = ctor_induct_thm, strong_induct = ctor_induct_thm, dtor_ctors = dtor_ctor_thms, ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms, map_thms = folded_ctor_map_thms, set_thmss = folded_ctor_set_thmss', rel_thms = ctor_Irel_thms, fold_thms = ctor_fold_thms,