src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
changeset 51811 1461426e2bf1
parent 51810 7b75fab5ebf5
child 51813 ca201253e7bb
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Apr 29 11:46:03 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Apr 29 13:40:26 2013 +0200
     1.3 @@ -7,6 +7,26 @@
     1.4  
     1.5  signature BNF_FP_DEF_SUGAR =
     1.6  sig
     1.7 +  val derive_induct_fold_rec_thms_for_types: int -> BNF_Def.BNF list -> thm -> thm list ->
     1.8 +    thm list -> BNF_Def.BNF list -> BNF_Def.BNF list -> typ list -> typ list ->
     1.9 +    typ list list list -> int list list -> int list -> term list list -> term list list ->
    1.10 +    term list list -> term list list list -> thm list list -> term list -> term list -> thm list ->
    1.11 +    thm list -> Proof.context ->
    1.12 +    (thm * thm list * Args.src list) * (thm list list * Args.src list)
    1.13 +      * (thm list list * Args.src list)
    1.14 +  val derive_coinduct_unfold_corec_thms_for_types: Proof.context -> Proof.context -> int ->
    1.15 +    BNF_Def.BNF list -> thm -> thm -> thm list -> thm list -> thm list -> BNF_Def.BNF list ->
    1.16 +    BNF_Def.BNF list -> typ list -> typ list -> typ list -> int list list -> int list list ->
    1.17 +    int list -> term list -> term list list -> term list list -> term list list list list ->
    1.18 +    term list list list list -> term list list -> term list list list list ->
    1.19 +    term list list list list -> term list list -> thm list list ->
    1.20 +    (term list * term list list * thm * 'a * 'b * 'c * thm list list * thm list
    1.21 +       * thm list list) list ->
    1.22 +    term list -> term list -> thm list -> thm list -> Proof.context ->
    1.23 +    (thm * thm list * thm * thm list * Args.src list) * (thm list list * thm list list * 'e list)
    1.24 +    * (thm list list * thm list list) * (thm list list * thm list list * Args.src list)
    1.25 +    * (thm list list * thm list list * Args.src list) *
    1.26 +    (thm list list * thm list list * Args.src list)
    1.27    val datatypes: bool ->
    1.28      (mixfix list -> (string * sort) list option -> binding list -> binding list -> binding list ->
    1.29        binding list list -> typ list * typ list list -> BNF_Def.BNF list -> local_theory ->
    1.30 @@ -56,6 +76,13 @@
    1.31      let val (xs1, xs2, xs3, xs4) = split_list4 xs;
    1.32      in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4) end;
    1.33  
    1.34 +fun add_components_of_typ (Type (s, Ts)) =
    1.35 +    fold add_components_of_typ Ts
    1.36 +    #> cons s
    1.37 +  | add_components_of_typ _ = I;
    1.38 +
    1.39 +fun name_of_typ T = space_implode "_" (add_components_of_typ T []);
    1.40 +
    1.41  fun exists_subtype_in Ts = exists_subtype (member (op =) Ts);
    1.42  
    1.43  fun resort_tfree S (TFree (s, _)) = TFree (s, S);
    1.44 @@ -173,9 +200,9 @@
    1.45      val Ts' = map domain_type (fst (strip_typeN live (fastype_of rel)));
    1.46    in Term.list_comb (rel, map build_arg Ts') end;
    1.47  
    1.48 -fun derive_induct_fold_rec_thms_for_types nn fp_b_names pre_bnfs fp_induct fp_fold_thms fp_rec_thms
    1.49 -    nesting_bnfs nested_bnfs fpTs Cs ctr_Tsss mss ns gss hss
    1.50 -    ((ctrss, xsss, ctr_defss, _), (folds, recs, fold_defs, rec_defs)) lthy =
    1.51 +fun derive_induct_fold_rec_thms_for_types nn pre_bnfs fp_induct fp_fold_thms fp_rec_thms
    1.52 +    nesting_bnfs nested_bnfs fpTs Cs ctr_Tsss mss ns gss hss ctrss xsss ctr_defss folds recs
    1.53 +    fold_defs rec_defs lthy =
    1.54    let
    1.55      val pre_map_defs = map map_def_of_bnf pre_bnfs;
    1.56      val pre_set_defss = map set_defs_of_bnf pre_bnfs;
    1.57 @@ -184,10 +211,12 @@
    1.58      val nested_set_map's = maps set_map'_of_bnf nested_bnfs;
    1.59      val nesting_map_ids'' = map (unfold_thms lthy @{thms id_def} o map_id_of_bnf) nesting_bnfs;
    1.60  
    1.61 +    val fp_T_names = map name_of_typ fpTs;
    1.62 +
    1.63      val (((ps, ps'), us'), names_lthy) =
    1.64        lthy
    1.65        |> mk_Frees' "P" (map mk_pred1T fpTs)
    1.66 -      ||>> Variable.variant_fixes fp_b_names;
    1.67 +      ||>> Variable.variant_fixes fp_T_names;
    1.68  
    1.69      val us = map2 (curry Free) us' fpTs;
    1.70  
    1.71 @@ -324,10 +353,10 @@
    1.72       (fold_thmss, code_simp_attrs), (rec_thmss, code_simp_attrs))
    1.73    end;
    1.74  
    1.75 -fun derive_coinduct_unfold_corec_thms_for_types names_lthy0 no_defs_lthy nn fp_b_names pre_bnfs
    1.76 -    fp_induct fp_strong_induct dtor_ctors fp_fold_thms fp_rec_thms nesting_bnfs nested_bnfs fpTs Cs
    1.77 -    As kss mss ns cs cpss pgss crssss cgssss phss csssss chssss
    1.78 -    ((ctrss, _, ctr_defss, ctr_wrap_ress), (unfolds, corecs, unfold_defs, corec_defs)) lthy =
    1.79 +fun derive_coinduct_unfold_corec_thms_for_types names_lthy0 no_defs_lthy nn pre_bnfs fp_induct
    1.80 +    fp_strong_induct dtor_ctors fp_fold_thms fp_rec_thms nesting_bnfs nested_bnfs fpTs Cs As kss mss
    1.81 +    ns cs cpss pgss crssss cgssss phss csssss chssss ctrss ctr_defss ctr_wrap_ress unfolds corecs
    1.82 +    unfold_defs corec_defs lthy =
    1.83    let
    1.84      val pre_map_defs = map map_def_of_bnf pre_bnfs;
    1.85      val pre_rel_defs = map rel_def_of_bnf pre_bnfs;
    1.86 @@ -337,6 +366,8 @@
    1.87      val nesting_map_ids'' = map (unfold_thms lthy @{thms id_def} o map_id_of_bnf) nesting_bnfs;
    1.88      val nesting_rel_eqs = map rel_eq_of_bnf nesting_bnfs;
    1.89  
    1.90 +    val fp_T_names = map name_of_typ fpTs;
    1.91 +
    1.92      val discss = map (map (mk_disc_or_sel As) o #1) ctr_wrap_ress;
    1.93      val selsss = map (map (map (mk_disc_or_sel As)) o #2) ctr_wrap_ress;
    1.94      val exhaust_thms = map #3 ctr_wrap_ress;
    1.95 @@ -347,8 +378,8 @@
    1.96      val (((rs, us'), vs'), names_lthy) =
    1.97        lthy
    1.98        |> mk_Frees "R" (map (fn T => mk_pred2T T T) fpTs)
    1.99 -      ||>> Variable.variant_fixes fp_b_names
   1.100 -      ||>> Variable.variant_fixes (map (suffix "'") fp_b_names);
   1.101 +      ||>> Variable.variant_fixes fp_T_names
   1.102 +      ||>> Variable.variant_fixes (map (suffix "'") fp_T_names);
   1.103  
   1.104      val us = map2 (curry Free) us' fpTs;
   1.105      val udiscss = map2 (map o rapp) us discss;
   1.106 @@ -433,7 +464,7 @@
   1.107          flat (map2 append disc_concls ctr_concls)
   1.108        end;
   1.109  
   1.110 -    val coinduct_cases = quasi_unambiguous_case_names (map (prefix EqN) fp_b_names);
   1.111 +    val coinduct_cases = quasi_unambiguous_case_names (map (prefix EqN) fp_T_names);
   1.112      val coinduct_conclss =
   1.113        map3 (quasi_unambiguous_case_names ooo mk_coinduct_concls) mss discss ctrss;
   1.114  
   1.115 @@ -1173,13 +1204,14 @@
   1.116          injects @ distincts @ cases @ rec_likes @ fold_likes);
   1.117  
   1.118      fun derive_and_note_induct_fold_rec_thms_for_types
   1.119 -        (info as ((_, _, _, ctr_wrap_ress), _), lthy) =
   1.120 +        (((ctrss, xsss, ctr_defss, ctr_wrap_ress), (folds, recs, fold_defs, rec_defs)), lthy) =
   1.121        let
   1.122          val ((induct_thm, induct_thms, induct_attrs),
   1.123               (fold_thmss, fold_attrs),
   1.124               (rec_thmss, rec_attrs)) =
   1.125 -          derive_induct_fold_rec_thms_for_types nn fp_b_names pre_bnfs fp_induct fp_fold_thms
   1.126 -            fp_rec_thms nesting_bnfs nested_bnfs fpTs Cs ctr_Tsss mss ns gss hss info lthy;
   1.127 +          derive_induct_fold_rec_thms_for_types nn pre_bnfs fp_induct fp_fold_thms fp_rec_thms
   1.128 +            nesting_bnfs nested_bnfs fpTs Cs ctr_Tsss mss ns gss hss ctrss xsss ctr_defss folds recs
   1.129 +            fold_defs rec_defs lthy;
   1.130  
   1.131          fun induct_type_attr T_name = Attrib.internal (K (Induct.induct_type T_name));
   1.132  
   1.133 @@ -1200,7 +1232,7 @@
   1.134        end;
   1.135  
   1.136      fun derive_and_note_coinduct_unfold_corec_thms_for_types
   1.137 -        (info as ((_, _, _, ctr_wrap_ress), _), lthy) =
   1.138 +        (((ctrss, _, ctr_defss, ctr_wrap_ress), (unfolds, corecs, unfold_defs, corec_defs)), lthy) =
   1.139        let
   1.140          val ((coinduct_thm, coinduct_thms, strong_coinduct_thm, strong_coinduct_thms,
   1.141                coinduct_attrs),
   1.142 @@ -1209,10 +1241,10 @@
   1.143               (disc_unfold_thmss, disc_corec_thmss, disc_corec_like_attrs),
   1.144               (disc_unfold_iff_thmss, disc_corec_iff_thmss, disc_corec_like_iff_attrs),
   1.145               (sel_unfold_thmss, sel_corec_thmss, sel_corec_like_attrs)) =
   1.146 -          derive_coinduct_unfold_corec_thms_for_types names_lthy0 no_defs_lthy nn fp_b_names
   1.147 -            pre_bnfs fp_induct fp_strong_induct dtor_ctors fp_fold_thms fp_rec_thms nesting_bnfs
   1.148 -            nested_bnfs fpTs Cs As kss mss ns cs cpss pgss crssss cgssss phss csssss chssss info
   1.149 -            lthy;
   1.150 +          derive_coinduct_unfold_corec_thms_for_types names_lthy0 no_defs_lthy nn pre_bnfs fp_induct
   1.151 +            fp_strong_induct dtor_ctors fp_fold_thms fp_rec_thms nesting_bnfs nested_bnfs fpTs Cs As
   1.152 +            kss mss ns cs cpss pgss crssss cgssss phss csssss chssss ctrss ctr_defss ctr_wrap_ress
   1.153 +            unfolds corecs unfold_defs corec_defs lthy;
   1.154  
   1.155          fun coinduct_type_attr T_name = Attrib.internal (K (Induct.coinduct_type T_name));
   1.156