src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
changeset 51824 27d073b0876c
parent 51823 38996458bc5c
child 51827 836257faaad5
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Apr 29 17:37:00 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Apr 29 18:52:18 2013 +0200
     1.3 @@ -8,7 +8,8 @@
     1.4  signature BNF_FP_DEF_SUGAR =
     1.5  sig
     1.6    type fp =
     1.7 -    {fp_index: int,
     1.8 +    {lfp: bool,
     1.9 +     fp_index: int,
    1.10       fp_res: BNF_FP.fp_result,
    1.11       ctr_wrap_res: BNF_Ctr_Sugar.ctr_wrap_result};
    1.12  
    1.13 @@ -30,8 +31,8 @@
    1.14      Proof.context ->
    1.15      (thm * thm list * thm * thm list * Args.src list) * (thm list list * thm list list * 'e list)
    1.16      * (thm list list * thm list list) * (thm list list * thm list list * Args.src list)
    1.17 -    * (thm list list * thm list list * Args.src list) *
    1.18 -    (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 @@ -60,16 +61,17 @@
    1.25  val EqN = "Eq_";
    1.26  
    1.27  type fp =
    1.28 -  {fp_index: int,
    1.29 +  {lfp: bool,
    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 +fun eq_fp ({lfp = lfp1, fp_index = fp_index1, fp_res = fp_res1, ...} : fp,
    1.38 +    {lfp = lfp2, fp_index = fp_index2, fp_res = fp_res2, ...} : fp) =
    1.39 +  lfp1 = lfp2 andalso fp_index1 = fp_index2 andalso eq_fp_result (fp_res1, fp_res2);
    1.40  
    1.41 -fun morph_fp phi {fp_index, fp_res, ctr_wrap_res} =
    1.42 -  {fp_index = fp_index, fp_res = morph_fp_result phi fp_res,
    1.43 +fun morph_fp phi {lfp, fp_index, fp_res, ctr_wrap_res} =
    1.44 +  {lfp = lfp, fp_index = fp_index, fp_res = morph_fp_result phi fp_res,
    1.45     ctr_wrap_res = morph_ctr_wrap_result phi ctr_wrap_res};
    1.46  
    1.47  structure Data = Generic_Data
    1.48 @@ -86,6 +88,15 @@
    1.49    Local_Theory.declaration {syntax = false, pervasive = true}
    1.50      (fn phi => Data.map (Symtab.update_new (key, morph_fp phi fp)));
    1.51  
    1.52 +val fp_name_of_ctor = fst o dest_Type o range_type o fastype_of;
    1.53 +
    1.54 +fun register_fps lfp (fp_res as {ctors, ...}) ctr_wrap_ress lthy =
    1.55 +  ((1, ctors), lthy)
    1.56 +  |> fold (fn ctr_wrap_res => fn ((kk, ctor :: ctors), lthy) =>
    1.57 +    ((kk + 1, ctors), register_fp (fp_name_of_ctor ctor) {lfp = lfp, fp_index = kk,
    1.58 +       fp_res = fp_res, ctr_wrap_res = ctr_wrap_res} lthy)) ctr_wrap_ress
    1.59 +  |> snd;
    1.60 +
    1.61  (* This function could produce clashes in contrived examples (e.g., "x.A", "x.x_A", "y.A"). *)
    1.62  fun quasi_unambiguous_case_names names =
    1.63    let
    1.64 @@ -757,7 +768,7 @@
    1.65      val fp_eqs =
    1.66        map dest_TFree Xs ~~ map (Term.typ_subst_atomic (As ~~ unsorted_As)) ctr_sum_prod_TsXs;
    1.67  
    1.68 -    val (pre_bnfs, ({bnfs = fp_bnfs as any_fp_bnf :: _, dtors = dtors0, ctors = ctors0,
    1.69 +    val (pre_bnfs, (fp_res as {bnfs = fp_bnfs as any_fp_bnf :: _, dtors = dtors0, ctors = ctors0,
    1.70             folds = fp_folds0, recs = fp_recs0, induct = fp_induct, strong_induct = fp_strong_induct,
    1.71             dtor_ctors, ctor_dtors, ctor_injects, map_thms = fp_map_thms, set_thmss = fp_set_thmss,
    1.72             rel_thms = fp_rel_thms, fold_thms = fp_fold_thms, rec_thms = fp_rec_thms}, lthy)) =
    1.73 @@ -1265,7 +1276,9 @@
    1.74             (simpsN, simp_thmss, K [])]
    1.75            |> massage_multi_notes;
    1.76        in
    1.77 -        lthy |> Local_Theory.notes (common_notes @ notes) |> snd
    1.78 +        lthy
    1.79 +        |> Local_Theory.notes (common_notes @ notes) |> snd
    1.80 +        |> register_fps true fp_res ctr_wrap_ress
    1.81        end;
    1.82  
    1.83      fun derive_and_note_coinduct_unfold_corec_thms_for_types
    1.84 @@ -1320,7 +1333,9 @@
    1.85             (unfoldN, unfold_thmss, K corec_like_attrs)]
    1.86            |> massage_multi_notes;
    1.87        in
    1.88 -        lthy |> Local_Theory.notes (anonymous_notes @ common_notes @ notes) |> snd
    1.89 +        lthy
    1.90 +        |> Local_Theory.notes (anonymous_notes @ common_notes @ notes) |> snd
    1.91 +        |> register_fps false fp_res ctr_wrap_ress
    1.92        end;
    1.93  
    1.94      val lthy' = lthy