# HG changeset patch # User blanchet # Date 1347961342 -7200 # Node ID 5bc80d96241ea390045b8d4ee15d9cf92218e754 # Parent c139da00fb4ab0666864047254b74b48dacc4d92 group "simps" together diff -r c139da00fb4a -r 5bc80d96241e src/HOL/Codatatype/Tools/bnf_fp_sugar.ML --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Tue Sep 18 11:42:11 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Tue Sep 18 11:42:22 2012 +0200 @@ -34,9 +34,8 @@ val simp_attrs = @{attributes [simp]}; -fun split_list10 xs = - (map #1 xs, map #2 xs, map #3 xs, map #4 xs, map #5 xs, map #6 xs, map #7 xs, map #8 xs, - map #9 xs, map #10 xs); +fun split_list8 xs = + (map #1 xs, map #2 xs, map #3 xs, map #4 xs, map #5 xs, map #6 xs, map #7 xs, map #8 xs); fun resort_tfree S (TFree (s, _)) = TFree (s, S); @@ -406,7 +405,7 @@ val tacss = [exhaust_tac] :: inject_tacss @ half_distinct_tacss @ [case_tacs]; - fun define_iter_rec ((selss0, discIs, sel_thmss), no_defs_lthy) = + fun define_iter_rec (wrap_res, no_defs_lthy) = let val fpT_to_C = fpT --> C; @@ -438,10 +437,10 @@ val [iter, recx] = map (mk_iter_like As Cs o Morphism.term phi) csts; in - ((ctrs, selss0, iter, recx, xss, ctr_defs, discIs, sel_thmss, iter_def, rec_def), lthy) + ((wrap_res, ctrs, iter, recx, xss, ctr_defs, iter_def, rec_def), lthy) end; - fun define_coiter_corec ((selss0, discIs, sel_thmss), no_defs_lthy) = + fun define_coiter_corec (wrap_res, no_defs_lthy) = let val B_to_fpT = C --> fpT; @@ -478,8 +477,7 @@ val [coiter, corec] = map (mk_iter_like As Cs o Morphism.term phi) csts; in - ((ctrs, selss0, coiter, corec, xss, ctr_defs, discIs, sel_thmss, coiter_def, corec_def), - lthy) + ((wrap_res, ctrs, coiter, corec, xss, ctr_defs, coiter_def, corec_def), lthy) end; fun wrap lthy = @@ -514,9 +512,13 @@ val args = map build_arg TUs; in Term.list_comb (mapx, args) end; - fun derive_induct_iter_rec_thms_for_types ((ctrss, _, iters, recs, xsss, ctr_defss, _, _, + fun derive_induct_iter_rec_thms_for_types ((wrap_ress, ctrss, iters, recs, xsss, ctr_defss, iter_defs, rec_defs), lthy) = let + val inject_thmss = map #2 wrap_ress; + val distinct_thmss = map #3 wrap_ress; + val case_thmss = map #4 wrap_ress; + val (((phis, phis'), vs'), names_lthy) = lthy |> mk_Frees' "P" (map mk_predT fpTs) @@ -603,6 +605,7 @@ `(conj_dests nn) induct_thm end; + (* TODO: Generate nicer names in case of clashes *) val induct_cases = Datatype_Prop.indexify_names (maps (map base_name_of_ctr) ctrss); val (iter_thmss, rec_thmss) = @@ -653,6 +656,10 @@ goal_recss rec_tacss) end; + val simp_thmss = + map4 (fn injects => fn distincts => fn cases => fn recs => + injects @ distincts @ cases @ recs) inject_thmss distinct_thmss case_thmss rec_thmss; + val induct_case_names_attr = Attrib.internal (K (Rule_Cases.case_names induct_cases)); fun induct_type_attr T_name = Attrib.internal (K (Induct.induct_type T_name)); @@ -665,7 +672,8 @@ [(inductN, map single induct_thms, fn T_name => [induct_case_names_attr, induct_type_attr T_name]), (itersN, iter_thmss, K simp_attrs), - (recsN, rec_thmss, K (Code.add_default_eqn_attrib :: simp_attrs))] + (recsN, rec_thmss, K (Code.add_default_eqn_attrib :: simp_attrs)), + (simpsN, simp_thmss, K [])] |> maps (fn (thmN, thmss, attrs) => map3 (fn b => fn Type (T_name, _) => fn thms => ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), attrs T_name), @@ -674,9 +682,13 @@ lthy |> Local_Theory.notes (common_notes @ notes) |> snd end; - fun derive_coinduct_coiter_corec_thms_for_types ((ctrss, selsss, coiters, corecs, _, ctr_defss, - discIss, sel_thmsss, coiter_defs, corec_defs), lthy) = + fun derive_coinduct_coiter_corec_thms_for_types ((wrap_ress, ctrss, coiters, corecs, _, + ctr_defss, coiter_defs, corec_defs), lthy) = let + val selsss0 = map #1 wrap_ress; + val discIss = map #5 wrap_ress; + val sel_thmsss = map #6 wrap_ress; + val (vs', _) = lthy |> Variable.variant_fixes (map Binding.name_of fp_bs); @@ -765,9 +777,9 @@ end; val sel_coiter_thmsss = - map3 (map3 (map2 o mk_sel_coiter_like_thm)) coiter_thmss selsss sel_thmsss; + map3 (map3 (map2 o mk_sel_coiter_like_thm)) coiter_thmss selsss0 sel_thmsss; val sel_corec_thmsss = - map3 (map3 (map2 o mk_sel_coiter_like_thm)) corec_thmss selsss sel_thmsss; + map3 (map3 (map2 o mk_sel_coiter_like_thm)) corec_thmss selsss0 sel_thmsss; val common_notes = (if nn > 1 then [(coinductN, [coinduct_thm], [])] (* FIXME: attribs *) else []) @@ -791,7 +803,7 @@ end; fun wrap_types_and_define_iter_likes ((wraps, define_iter_likess), lthy) = - fold_map2 (curry (op o)) define_iter_likess wraps lthy |>> split_list10 + fold_map2 (curry (op o)) define_iter_likess wraps lthy |>> split_list8 val lthy' = lthy |> fold_map define_ctrs_case_for_type (fp_bs ~~ fpTs ~~ Cs ~~ flds ~~ unfs ~~ fp_iters ~~ diff -r c139da00fb4a -r 5bc80d96241e src/HOL/Codatatype/Tools/bnf_fp_util.ML --- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML Tue Sep 18 11:42:11 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML Tue Sep 18 11:42:22 2012 +0200 @@ -62,6 +62,7 @@ val sel_corecsN: string val set_inclN: string val set_set_inclN: string + val simpsN: string val strTN: string val str_initN: string val sum_bdN: string @@ -164,6 +165,7 @@ val coiterN = coN ^ iterN val coitersN = coiterN ^ "s" val uniqueN = "_unique" +val simpsN = "simps" val fldN = "fld" val unfN = "unf" val fld_iterN = fldN ^ "_" ^ iterN @@ -173,7 +175,7 @@ val fld_iter_uniqueN = fld_iterN ^ uniqueN val unf_coiter_uniqueN = unf_coiterN ^ uniqueN val fld_unf_coitersN = fldN ^ "_" ^ unf_coiterN ^ "s" -val map_simpsN = mapN ^ "_simps" +val map_simpsN = mapN ^ "_" ^ simpsN val map_uniqueN = mapN ^ uniqueN val min_algN = "min_alg" val morN = "mor" @@ -187,7 +189,7 @@ val LevN = "Lev" val rvN = "recover" val behN = "beh" -fun mk_set_simpsN i = mk_setN i ^ "_simps" +fun mk_set_simpsN i = mk_setN i ^ "_" ^ simpsN fun mk_set_minimalN i = mk_setN i ^ "_minimal" fun mk_set_inductN i = mk_setN i ^ "_induct" diff -r c139da00fb4a -r 5bc80d96241e src/HOL/Codatatype/Tools/bnf_wrap.ML --- a/src/HOL/Codatatype/Tools/bnf_wrap.ML Tue Sep 18 11:42:11 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML Tue Sep 18 11:42:22 2012 +0200 @@ -13,7 +13,7 @@ val wrap_datatype: ({prems: thm list, context: Proof.context} -> tactic) list list -> ((bool * term list) * term) * (binding list * (binding list list * (binding * term) list list)) -> local_theory -> - (term list list * thm list * thm list list) * local_theory + (term list list * thm list * thm list * thm list * thm list * thm list list) * local_theory val parse_wrap_options: bool parser val parse_bound_term: (binding * string) parser end; @@ -327,6 +327,8 @@ val ([exhaust_thm], (inject_thmss, (half_distinct_thmss, [case_thms]))) = (hd thmss, apsnd (chop (n * n)) (chop n (tl thmss))); + val inject_thms = flat inject_thmss; + val exhaust_thm' = let val Tinst = map (pairself (certifyT lthy)) (map Logic.varifyT_global As ~~ As) in Drule.instantiate' [] [SOME (certify lthy v)] @@ -571,7 +573,7 @@ (disc_exhaustN, disc_exhaust_thms, [exhaust_case_names_attr]), (distinctN, distinct_thms, simp_attrs @ induct_simp_attrs), (exhaustN, [exhaust_thm], [exhaust_case_names_attr, cases_type_attr]), - (injectN, flat inject_thmss, iff_attrs @ induct_simp_attrs), + (injectN, inject_thms, iff_attrs @ induct_simp_attrs), (nchotomyN, [nchotomy_thm], []), (selsN, all_sel_thms, simp_attrs), (splitN, [split_thm], []), @@ -586,7 +588,8 @@ [(map (fn th => th RS notE) distinct_thms, safe_elim_attrs)] |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])])); in - ((selss, discI_thms, sel_thmss), lthy |> Local_Theory.notes (notes' @ notes) |> snd) + ((selss, inject_thms, distinct_thms, case_thms, discI_thms, sel_thmss), + lthy |> Local_Theory.notes (notes' @ notes) |> snd) end; in (goalss, after_qed, lthy')