src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
changeset 51823 38996458bc5c
parent 51819 9df935196be9
child 51824 27d073b0876c
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Apr 29 16:50:01 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Apr 29 17:37:00 2013 +0200
     1.3 @@ -7,6 +7,13 @@
     1.4  
     1.5  signature BNF_FP_DEF_SUGAR =
     1.6  sig
     1.7 +  type fp =
     1.8 +    {fp_index: int,
     1.9 +     fp_res: BNF_FP.fp_result,
    1.10 +     ctr_wrap_res: BNF_Ctr_Sugar.ctr_wrap_result};
    1.11 +
    1.12 +  val fp_of: Proof.context -> string -> fp option
    1.13 +
    1.14    val derive_induct_fold_rec_thms_for_types: BNF_Def.BNF list -> thm -> thm list -> thm list ->
    1.15      BNF_Def.BNF list -> BNF_Def.BNF list -> typ list -> typ list -> typ list list list ->
    1.16      int list list -> int list -> term list list -> term list list -> term list list -> term list
    1.17 @@ -25,6 +32,7 @@
    1.18      * (thm list list * thm list list) * (thm list list * thm list list * Args.src list)
    1.19      * (thm list list * thm list list * Args.src list) *
    1.20      (thm list list * thm list list * Args.src list)
    1.21 +
    1.22    val datatypes: bool ->
    1.23      (mixfix list -> (string * sort) list option -> binding list -> binding list -> binding list ->
    1.24        binding list list -> typ list * typ list list -> BNF_Def.BNF list -> local_theory ->
    1.25 @@ -51,6 +59,33 @@
    1.26  
    1.27  val EqN = "Eq_";
    1.28  
    1.29 +type fp =
    1.30 +  {fp_index: int,
    1.31 +   fp_res: fp_result,
    1.32 +   ctr_wrap_res: ctr_wrap_result};
    1.33 +
    1.34 +fun eq_fp ({fp_index = fp_index1, fp_res = fp_res1, ...} : fp,
    1.35 +    {fp_index = fp_index2, fp_res = fp_res2, ...} : fp) =
    1.36 +  fp_index1 = fp_index2 andalso eq_fp_result (fp_res1, fp_res2);
    1.37 +
    1.38 +fun morph_fp phi {fp_index, fp_res, ctr_wrap_res} =
    1.39 +  {fp_index = fp_index, fp_res = morph_fp_result phi fp_res,
    1.40 +   ctr_wrap_res = morph_ctr_wrap_result phi ctr_wrap_res};
    1.41 +
    1.42 +structure Data = Generic_Data
    1.43 +(
    1.44 +  type T = fp Symtab.table;
    1.45 +  val empty = Symtab.empty;
    1.46 +  val extend = I;
    1.47 +  val merge = Symtab.merge eq_fp;
    1.48 +);
    1.49 +
    1.50 +val fp_of = Symtab.lookup o Data.get o Context.Proof;
    1.51 +
    1.52 +fun register_fp key fp =
    1.53 +  Local_Theory.declaration {syntax = false, pervasive = true}
    1.54 +    (fn phi => Data.map (Symtab.update_new (key, morph_fp phi fp)));
    1.55 +
    1.56  (* This function could produce clashes in contrived examples (e.g., "x.A", "x.x_A", "y.A"). *)
    1.57  fun quasi_unambiguous_case_names names =
    1.58    let