1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Wed Sep 12 17:26:05 2012 +0200
1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Wed Sep 12 17:26:05 2012 +0200
1.3 @@ -10,16 +10,16 @@
1.4 val datatyp: bool ->
1.5 (mixfix list -> (string * sort) list option -> binding list -> typ list * typ list list ->
1.6 BNF_Def.BNF list -> local_theory ->
1.7 - (term list * term list * term list * term list * thm list * thm list * thm list * thm list *
1.8 - thm list) * local_theory) ->
1.9 + (term list * term list * term list * term list * thm * thm list * thm list * thm list *
1.10 + thm list * thm list) * local_theory) ->
1.11 bool * ((((typ * sort) list * binding) * mixfix) * ((((binding * binding) *
1.12 (binding * typ) list) * (binding * term) list) * mixfix) list) list ->
1.13 local_theory -> local_theory
1.14 val parse_datatype_cmd: bool ->
1.15 (mixfix list -> (string * sort) list option -> binding list -> typ list * typ list list ->
1.16 BNF_Def.BNF list -> local_theory ->
1.17 - (term list * term list * term list * term list * thm list * thm list * thm list * thm list *
1.18 - thm list) * local_theory) ->
1.19 + (term list * term list * term list * term list * thm * thm list * thm list * thm list *
1.20 + thm list * thm list) * local_theory) ->
1.21 (local_theory -> local_theory) parser
1.22 end;
1.23
1.24 @@ -33,10 +33,12 @@
1.25 open BNF_FP_Sugar_Tactics
1.26
1.27 val caseN = "case";
1.28 +val coinductsN = "coinducts";
1.29 val coitersN = "coiters";
1.30 val corecsN = "corecs";
1.31 val disc_coitersN = "disc_coiters";
1.32 val disc_corecsN = "disc_corecs";
1.33 +val inductsN = "inducts";
1.34 val itersN = "iters";
1.35 val recsN = "recs";
1.36 val sel_coitersN = "sel_coiters";
1.37 @@ -131,6 +133,8 @@
1.38 unsorted_As);
1.39
1.40 val fp_bs = map type_binding_of specs;
1.41 + val fp_common_name = mk_common_name fp_bs;
1.42 +
1.43 val fake_Ts = map mk_fake_T fp_bs;
1.44
1.45 val mixfixes = map mixfix_of specs;
1.46 @@ -179,7 +183,7 @@
1.47 val fp_eqs =
1.48 map dest_TFree Bs ~~ map (Term.typ_subst_atomic (As ~~ unsorted_As)) ctr_sum_prod_TsBs;
1.49
1.50 - val (pre_bnfs, ((unfs0, flds0, fp_iters0, fp_recs0, unf_flds, fld_unfs, fld_injects,
1.51 + val (pre_bnfs, ((unfs0, flds0, fp_iters0, fp_recs0, fp_induct, unf_flds, fld_unfs, fld_injects,
1.52 fp_iter_thms, fp_rec_thms), lthy)) =
1.53 fp_bnf construct fp_bs mixfixes (map dest_TFree unsorted_As) fp_eqs no_defs_lthy0;
1.54
1.55 @@ -517,15 +521,22 @@
1.56 val args = map build_arg TUs;
1.57 in Term.list_comb (mapx, args) end;
1.58
1.59 - fun derive_iter_rec_thms_for_types ((ctrss, _, iters, recs, vs, xsss, ctr_defss, _, _, iter_defs,
1.60 - rec_defs), lthy) =
1.61 + fun derive_induct_iter_rec_thms_for_types ((ctrss, _, iters, recs, vs, xsss, ctr_defss, _, _,
1.62 + iter_defs, rec_defs), lthy) =
1.63 let
1.64 - val xctrss = map2 (map2 (curry Term.list_comb)) ctrss xsss;
1.65 - val giters = map (lists_bmoc gss) iters;
1.66 - val hrecs = map (lists_bmoc hss) recs;
1.67 + val (induct_thms, induct_thm) =
1.68 + let
1.69 + val induct_thm = fp_induct;
1.70 + in
1.71 + `(conj_dests N) induct_thm
1.72 + end;
1.73
1.74 val (iter_thmss, rec_thmss) =
1.75 let
1.76 + val xctrss = map2 (map2 (curry Term.list_comb)) ctrss xsss;
1.77 + val giters = map (lists_bmoc gss) iters;
1.78 + val hrecs = map (lists_bmoc hss) recs;
1.79 +
1.80 fun mk_goal_iter_like fss fiter_like xctr f xs fxs =
1.81 fold_rev (fold_rev Logic.all) (xs :: fss)
1.82 (mk_Trueprop_eq (fiter_like $ xctr, Term.list_comb (f, fxs)));
1.83 @@ -567,6 +578,12 @@
1.84 goal_recss rec_tacss)
1.85 end;
1.86
1.87 + val common_notes =
1.88 + [(inductN, [induct_thm], []), (*### attribs *)
1.89 + (inductsN, induct_thms, [])] (*### attribs *)
1.90 + |> map (fn (thmN, thms, attrs) =>
1.91 + ((Binding.qualify true fp_common_name (Binding.name thmN), attrs), [(thms, [])]));
1.92 +
1.93 val notes =
1.94 [(itersN, iter_thmss, simp_attrs),
1.95 (recsN, rec_thmss, Code.add_default_eqn_attrib :: simp_attrs)]
1.96 @@ -575,19 +592,25 @@
1.97 ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), attrs),
1.98 [(thms, [])])) fp_bs thmss);
1.99 in
1.100 - lthy |> Local_Theory.notes notes |> snd
1.101 + lthy |> Local_Theory.notes (common_notes @ notes) |> snd
1.102 end;
1.103
1.104 - fun derive_coiter_corec_thms_for_types ((ctrss, selsss, coiters, corecs, vs, _, ctr_defss,
1.105 - discIss, sel_thmsss, coiter_defs, corec_defs), lthy) =
1.106 + fun derive_coinduct_coiter_corec_thms_for_types ((ctrss, selsss, coiters, corecs, vs, _,
1.107 + ctr_defss, discIss, sel_thmsss, coiter_defs, corec_defs), lthy) =
1.108 let
1.109 - val z = the_single zs;
1.110 -
1.111 - val gcoiters = map (lists_bmoc pgss) coiters;
1.112 - val hcorecs = map (lists_bmoc phss) corecs;
1.113 + val (coinduct_thms, coinduct_thm) =
1.114 + let
1.115 + val coinduct_thm = fp_induct;
1.116 + in
1.117 + `(conj_dests N) coinduct_thm
1.118 + end;
1.119
1.120 val (coiter_thmss, corec_thmss) =
1.121 let
1.122 + val z = the_single zs;
1.123 + val gcoiters = map (lists_bmoc pgss) coiters;
1.124 + val hcorecs = map (lists_bmoc phss) corecs;
1.125 +
1.126 fun mk_goal_cond pos = HOLogic.mk_Trueprop o (not pos ? HOLogic.mk_not);
1.127
1.128 fun mk_goal_coiter_like pfss c cps fcoiter_like n k ctr m cfs' =
1.129 @@ -684,7 +707,8 @@
1.130 fp_recs ~~ fld_unfs ~~ unf_flds ~~ fld_injects ~~ ns ~~ kss ~~ mss ~~ ctr_bindingss ~~
1.131 ctr_mixfixess ~~ ctr_Tsss ~~ disc_bindingss ~~ sel_bindingsss ~~ raw_sel_defaultsss)
1.132 |>> split_list |> wrap_types_and_define_iter_likes
1.133 - |> (if lfp then derive_iter_rec_thms_for_types else derive_coiter_corec_thms_for_types);
1.134 + |> (if lfp then derive_induct_iter_rec_thms_for_types
1.135 + else derive_coinduct_coiter_corec_thms_for_types);
1.136
1.137 val timer = time (timer ("Constructors, discriminators, selectors, etc., for the new " ^
1.138 (if lfp then "" else "co") ^ "datatype"));