1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Mon Sep 10 18:50:27 2012 +0200
1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Mon Sep 10 21:44:43 2012 +0200
1.3 @@ -24,11 +24,16 @@
1.4 val caseN = "case";
1.5 val coitersN = "coiters";
1.6 val corecsN = "corecs";
1.7 +val disc_coitersN = "disc_coiters";
1.8 +val disc_corecsN = "disc_corecs";
1.9 val itersN = "iters";
1.10 val recsN = "recs";
1.11 +val sel_coitersN = "sel_coiters";
1.12 +val sel_corecsN = "sel_corecs";
1.13
1.14 -fun split_list8 xs =
1.15 - (map #1 xs, map #2 xs, map #3 xs, map #4 xs, map #5 xs, map #6 xs, map #7 xs, map #8 xs);
1.16 +fun split_list11 xs =
1.17 + (map #1 xs, map #2 xs, map #3 xs, map #4 xs, map #5 xs, map #6 xs, map #7 xs, map #8 xs,
1.18 + map #9 xs, map #10 xs, map #11 xs);
1.19
1.20 fun strip_map_type (Type (@{type_name fun}, [T as Type _, T'])) = strip_map_type T' |>> cons T
1.21 | strip_map_type T = ([], T);
1.22 @@ -362,7 +367,7 @@
1.23
1.24 val tacss = [exhaust_tac] :: inject_tacss @ half_distinct_tacss @ [case_tacs];
1.25
1.26 - fun some_lfp_sugar no_defs_lthy =
1.27 + fun some_lfp_sugar ((selss, discIs, sel_thmss), no_defs_lthy) =
1.28 let
1.29 val fpT_to_C = fpT --> C;
1.30
1.31 @@ -397,10 +402,11 @@
1.32
1.33 val [iter, recx] = map (mk_iter_like As Cs o Morphism.term phi) csts;
1.34 in
1.35 - ((ctrs, iter, recx, v, xss, ctr_defs, iter_def, rec_def), lthy)
1.36 + ((ctrs, selss, iter, recx, v, xss, ctr_defs, discIs, sel_thmss, iter_def, rec_def),
1.37 + lthy)
1.38 end;
1.39
1.40 - fun some_gfp_sugar no_defs_lthy =
1.41 + fun some_gfp_sugar ((selss, discIs, sel_thmss), no_defs_lthy) =
1.42 let
1.43 val B_to_fpT = C --> fpT;
1.44
1.45 @@ -439,7 +445,8 @@
1.46
1.47 val [coiter, corec] = map (mk_iter_like As Cs o Morphism.term phi) csts;
1.48 in
1.49 - ((ctrs, coiter, corec, v, xss, ctr_defs, coiter_def, corec_def), lthy)
1.50 + ((ctrs, selss, coiter, corec, v, xss, ctr_defs, discIs, sel_thmss, coiter_def,
1.51 + corec_def), lthy)
1.52 end;
1.53 in
1.54 wrap_datatype tacss ((ctrs0, casex0), (disc_binders, sel_binderss)) lthy'
1.55 @@ -462,8 +469,8 @@
1.56 val args = map build_arg TUs;
1.57 in Term.list_comb (mapx, args) end;
1.58
1.59 - fun pour_more_sugar_on_lfps ((ctrss, iters, recs, vs, xsss, ctr_defss, iter_defs, rec_defs),
1.60 - lthy) =
1.61 + fun pour_more_sugar_on_lfps ((ctrss, _, iters, recs, vs, xsss, ctr_defss, _, _, iter_defs,
1.62 + 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 @@ -506,9 +513,11 @@
1.67 val rec_tacss =
1.68 map2 (map o mk_iter_like_tac pre_map_defs map_ids rec_defs) fp_rec_thms ctr_defss;
1.69 in
1.70 - (map2 (map2 (fn goal => fn tac => Skip_Proof.prove lthy [] [] goal (tac o #context)))
1.71 + (map2 (map2 (fn goal => fn tac =>
1.72 + Skip_Proof.prove lthy [] [] goal (tac o #context) |> Thm.close_derivation))
1.73 goal_iterss iter_tacss,
1.74 - map2 (map2 (fn goal => fn tac => Skip_Proof.prove lthy [] [] goal (tac o #context)))
1.75 + map2 (map2 (fn goal => fn tac =>
1.76 + Skip_Proof.prove lthy [] [] goal (tac o #context) |> Thm.close_derivation))
1.77 goal_recss rec_tacss)
1.78 end;
1.79
1.80 @@ -523,8 +532,8 @@
1.81 lthy |> Local_Theory.notes notes |> snd
1.82 end;
1.83
1.84 - fun pour_more_sugar_on_gfps ((ctrss, coiters, corecs, vs, _, ctr_defss, coiter_defs,
1.85 - corec_defs), lthy) =
1.86 + fun pour_more_sugar_on_gfps ((ctrss, selsss, coiters, corecs, vs, _, ctr_defss, discIss,
1.87 + sel_thmsss, coiter_defs, corec_defs), lthy) =
1.88 let
1.89 val z = the_single zs;
1.90
1.91 @@ -579,13 +588,39 @@
1.92 goal_corecss corec_tacss)
1.93 end;
1.94
1.95 + fun mk_disc_coiter_like_thms [_] = K []
1.96 + | mk_disc_coiter_like_thms thms = map2 (curry (op RS)) thms;
1.97 +
1.98 + val disc_coiter_thmss = map2 mk_disc_coiter_like_thms coiter_thmss discIss;
1.99 + val disc_corec_thmss = map2 mk_disc_coiter_like_thms corec_thmss discIss;
1.100 +
1.101 + fun mk_sel_coiter_like_thm coiter_like_thm sel sel_thm =
1.102 + let
1.103 + val (domT, ranT) = dest_funT (fastype_of sel);
1.104 + val arg_cong' =
1.105 + Drule.instantiate' (map (SOME o certifyT lthy) [domT, ranT])
1.106 + [NONE, NONE, SOME (certify lthy sel)] arg_cong;
1.107 + val sel_thm' = sel_thm RSN (2, trans);
1.108 + in
1.109 + (coiter_like_thm RS arg_cong') RS sel_thm'
1.110 + end;
1.111 +
1.112 + val sel_coiter_thmsss =
1.113 + map3 (map3 (map2 o mk_sel_coiter_like_thm)) coiter_thmss selsss sel_thmsss;
1.114 + val sel_corec_thmsss =
1.115 + map3 (map3 (map2 o mk_sel_coiter_like_thm)) coiter_thmss selsss sel_thmsss;
1.116 +
1.117 val notes =
1.118 [(coitersN, coiter_thmss),
1.119 - (corecsN, corec_thmss)]
1.120 + (disc_coitersN, disc_coiter_thmss),
1.121 + (sel_coitersN, map flat sel_coiter_thmsss),
1.122 + (corecsN, corec_thmss),
1.123 + (disc_corecsN, disc_corec_thmss),
1.124 + (sel_corecsN, map flat sel_corec_thmsss)]
1.125 |> maps (fn (thmN, thmss) =>
1.126 - map2 (fn b => fn thms =>
1.127 - ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
1.128 - bs thmss);
1.129 + map_filter (fn (_, []) => NONE | (b, thms) =>
1.130 + SOME ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []),
1.131 + [(thms, [])])) (bs ~~ thmss));
1.132 in
1.133 lthy |> Local_Theory.notes notes |> snd
1.134 end;
1.135 @@ -594,7 +629,7 @@
1.136 |> fold_map pour_some_sugar_on_type (bs ~~ fpTs ~~ Cs ~~ flds ~~ unfs ~~ fp_iters ~~
1.137 fp_recs ~~ fld_unfs ~~ unf_flds ~~ fld_injects ~~ ns ~~ kss ~~ mss ~~ ctr_binderss ~~
1.138 ctr_mixfixess ~~ ctr_Tsss ~~ disc_binderss ~~ sel_bindersss)
1.139 - |>> split_list8
1.140 + |>> split_list11
1.141 |> (if lfp then pour_more_sugar_on_lfps else pour_more_sugar_on_gfps);
1.142
1.143 val timer = time (timer ("Constructors, discriminators, selectors, etc., for the new " ^