--- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Mon Apr 29 17:17:20 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Mon Apr 29 18:52:35 2013 +0200
@@ -18,6 +18,8 @@
discIs: thm list,
sel_thmss: thm list list};
+ val morph_ctr_wrap_result: morphism -> ctr_wrap_result -> ctr_wrap_result
+
val rep_compat_prefix: string
val mk_half_pairss: 'a list * 'a list -> ('a * 'a) list list
@@ -54,6 +56,18 @@
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,
+ selss = map (map (Morphism.term phi)) selss,
+ exhaust = Morphism.thm phi exhaust,
+ injects = map (Morphism.thm phi) injects,
+ distincts = map (Morphism.thm phi) distincts,
+ case_thms = map (Morphism.thm phi) case_thms,
+ disc_thmss = map (map (Morphism.thm phi)) disc_thmss,
+ discIs = map (Morphism.thm phi) discIs,
+ sel_thmss = map (map (Morphism.thm phi)) sel_thmss};
+
val rep_compat_prefix = "new";
val isN = "is_";
--- a/src/HOL/BNF/Tools/bnf_def.ML Mon Apr 29 17:17:20 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML Mon Apr 29 18:52:35 2013 +0200
@@ -11,6 +11,8 @@
type BNF
type nonemptiness_witness = {I: int list, wit: term, prop: thm list}
+ val morph_bnf: morphism -> BNF -> BNF
+ val eq_bnf: BNF * BNF -> bool
val bnf_of: Proof.context -> string -> BNF option
val register_bnf: string -> (BNF * local_theory) -> (BNF * local_theory)
--- a/src/HOL/BNF/Tools/bnf_fp.ML Mon Apr 29 17:17:20 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp.ML Mon Apr 29 18:52:35 2013 +0200
@@ -1,6 +1,7 @@
(* Title: HOL/BNF/Tools/bnf_fp.ML
Author: Dmitriy Traytel, TU Muenchen
- Copyright 2012
+ Author: Jasmin Blanchette, TU Muenchen
+ Copyright 2012, 2013
Shared library for the datatype and codatatype constructions.
*)
@@ -24,6 +25,9 @@
fold_thms: thm list,
rec_thms: thm list}
+ val morph_fp_result: morphism -> fp_result -> fp_result
+ val eq_fp_result: fp_result * fp_result -> bool
+
val time: Timer.real_timer -> string -> Timer.real_timer
val IITN: string
@@ -184,6 +188,27 @@
fold_thms: thm list,
rec_thms: thm list};
+fun morph_fp_result phi {bnfs, dtors, ctors, 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,
+ 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,
+ strong_induct = Morphism.thm phi strong_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,
+ map_thms = map (Morphism.thm phi) map_thms,
+ set_thmss = map (map (Morphism.thm phi)) set_thmss,
+ rel_thms = map (Morphism.thm phi) rel_thms,
+ fold_thms = map (Morphism.thm phi) fold_thms,
+ rec_thms = map (Morphism.thm phi) rec_thms};
+
+fun eq_fp_result ({bnfs = bnfs1, ...} : fp_result, {bnfs = bnfs2, ...} : fp_result) =
+ eq_list eq_bnf (bnfs1, bnfs2);
+
val timing = true;
fun time timer msg = (if timing
then warning (msg ^ ": " ^ ATP_Util.string_from_time (Timer.checkRealTimer timer))
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Mon Apr 29 17:17:20 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Mon Apr 29 18:52:35 2013 +0200
@@ -7,6 +7,14 @@
signature BNF_FP_DEF_SUGAR =
sig
+ type fp =
+ {lfp: bool,
+ fp_index: int,
+ fp_res: BNF_FP.fp_result,
+ ctr_wrap_res: BNF_Ctr_Sugar.ctr_wrap_result};
+
+ val fp_of: Proof.context -> string -> fp option
+
val derive_induct_fold_rec_thms_for_types: BNF_Def.BNF list -> thm -> thm list -> thm list ->
BNF_Def.BNF list -> BNF_Def.BNF list -> typ list -> typ list -> typ list list list ->
int list list -> int list -> term list list -> term list list -> term list list -> term list
@@ -23,8 +31,9 @@
Proof.context ->
(thm * thm list * thm * thm list * Args.src list) * (thm list list * thm list list * 'e 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)
+ * (thm list list * thm list list * Args.src list)
+ * (thm list list * thm list list * Args.src list)
+
val datatypes: bool ->
(mixfix list -> (string * sort) list option -> binding list -> binding list -> binding list ->
binding list list -> typ list * typ list list -> BNF_Def.BNF list -> local_theory ->
@@ -51,6 +60,43 @@
val EqN = "Eq_";
+type fp =
+ {lfp: bool,
+ fp_index: int,
+ fp_res: fp_result,
+ ctr_wrap_res: ctr_wrap_result};
+
+fun eq_fp ({lfp = lfp1, fp_index = fp_index1, fp_res = fp_res1, ...} : fp,
+ {lfp = lfp2, fp_index = fp_index2, fp_res = fp_res2, ...} : fp) =
+ lfp1 = lfp2 andalso fp_index1 = fp_index2 andalso eq_fp_result (fp_res1, fp_res2);
+
+fun morph_fp phi {lfp, fp_index, fp_res, ctr_wrap_res} =
+ {lfp = lfp, fp_index = fp_index, fp_res = morph_fp_result phi fp_res,
+ ctr_wrap_res = morph_ctr_wrap_result phi ctr_wrap_res};
+
+structure Data = Generic_Data
+(
+ type T = fp Symtab.table;
+ val empty = Symtab.empty;
+ val extend = I;
+ val merge = Symtab.merge eq_fp;
+);
+
+val fp_of = Symtab.lookup o Data.get o Context.Proof;
+
+fun register_fp key fp =
+ 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 (fp_res as {ctors, ...}) ctr_wrap_ress lthy =
+ ((1, ctors), lthy)
+ |> fold (fn ctr_wrap_res => fn ((kk, ctor :: ctors), lthy) =>
+ ((kk + 1, ctors), register_fp (fp_name_of_ctor ctor) {lfp = lfp, fp_index = kk,
+ fp_res = fp_res, ctr_wrap_res = ctr_wrap_res} lthy)) ctr_wrap_ress
+ |> snd;
+
(* This function could produce clashes in contrived examples (e.g., "x.A", "x.x_A", "y.A"). *)
fun quasi_unambiguous_case_names names =
let
@@ -722,7 +768,7 @@
val fp_eqs =
map dest_TFree Xs ~~ map (Term.typ_subst_atomic (As ~~ unsorted_As)) ctr_sum_prod_TsXs;
- val (pre_bnfs, ({bnfs = fp_bnfs as any_fp_bnf :: _, dtors = dtors0, ctors = ctors0,
+ val (pre_bnfs, (fp_res as {bnfs = fp_bnfs as any_fp_bnf :: _, dtors = dtors0, ctors = ctors0,
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)) =
@@ -1230,7 +1276,9 @@
(simpsN, simp_thmss, K [])]
|> massage_multi_notes;
in
- lthy |> Local_Theory.notes (common_notes @ notes) |> snd
+ lthy
+ |> Local_Theory.notes (common_notes @ notes) |> snd
+ |> register_fps true fp_res ctr_wrap_ress
end;
fun derive_and_note_coinduct_unfold_corec_thms_for_types
@@ -1285,7 +1333,9 @@
(unfoldN, unfold_thmss, K corec_like_attrs)]
|> massage_multi_notes;
in
- lthy |> Local_Theory.notes (anonymous_notes @ common_notes @ notes) |> snd
+ lthy
+ |> Local_Theory.notes (anonymous_notes @ common_notes @ notes) |> snd
+ |> register_fps false fp_res ctr_wrap_ress
end;
val lthy' = lthy