1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Tue Sep 11 23:27:19 2012 +0200
1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Wed Sep 12 00:20:37 2012 +0200
1.3 @@ -34,6 +34,8 @@
1.4 val sel_coitersN = "sel_coiters";
1.5 val sel_corecsN = "sel_corecs";
1.6
1.7 +val simp_attrs = @{attributes [simp]};
1.8 +
1.9 fun split_list11 xs =
1.10 (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.11 map #9 xs, map #10 xs, map #11 xs);
1.12 @@ -424,12 +426,14 @@
1.13 map2 (mk_sum_caseN_balanced oo map2 mk_uncurried2_fun) fss xssss));
1.14 in (binder, spec) end;
1.15
1.16 - val iter_like_bundles =
1.17 + val iter_like_infos =
1.18 [(iterN, fp_iter, iter_only),
1.19 (recN, fp_rec, rec_only)];
1.20
1.21 - val (binders, specs) = map generate_iter_like iter_like_bundles |> split_list;
1.22 + val (binders, specs) = map generate_iter_like iter_like_infos |> split_list;
1.23
1.24 + (* TODO: Allow same constructor (and selector/discriminator) names for different
1.25 + types (cf. old "datatype" package) *)
1.26 val ((csts, defs), (lthy', lthy)) = no_defs_lthy
1.27 |> apfst split_list o fold_map2 (fn b => fn spec =>
1.28 Specification.definition (SOME (b, NONE, NoSyn), ((Thm.def_binding b, []), spec))
1.29 @@ -468,11 +472,11 @@
1.30 map5 mk_preds_getterss_join cs ns cpss f_sum_prod_Ts cqfsss));
1.31 in (binder, spec) end;
1.32
1.33 - val coiter_like_bundles =
1.34 + val coiter_like_infos =
1.35 [(coiterN, fp_iter, coiter_only),
1.36 (corecN, fp_rec, corec_only)];
1.37
1.38 - val (binders, specs) = map generate_coiter_like coiter_like_bundles |> split_list;
1.39 + val (binders, specs) = map generate_coiter_like coiter_like_infos |> split_list;
1.40
1.41 val ((csts, defs), (lthy', lthy)) = no_defs_lthy
1.42 |> apfst split_list o fold_map2 (fn b => fn spec =>
1.43 @@ -569,12 +573,12 @@
1.44 end;
1.45
1.46 val notes =
1.47 - [(itersN, iter_thmss),
1.48 - (recsN, rec_thmss)]
1.49 - |> maps (fn (thmN, thmss) =>
1.50 + [(itersN, iter_thmss, simp_attrs),
1.51 + (recsN, rec_thmss, Code.add_default_eqn_attrib :: simp_attrs)]
1.52 + |> maps (fn (thmN, thmss, attrs) =>
1.53 map2 (fn b => fn thms =>
1.54 - ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
1.55 - bs thmss);
1.56 + ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), attrs),
1.57 + [(thms, [])])) bs thmss);
1.58 in
1.59 lthy |> Local_Theory.notes notes |> snd
1.60 end;
1.61 @@ -663,15 +667,15 @@
1.62 map3 (map3 (map2 o mk_sel_coiter_like_thm)) corec_thmss selsss sel_thmsss;
1.63
1.64 val notes =
1.65 - [(coitersN, coiter_thmss),
1.66 - (disc_coitersN, disc_coiter_thmss),
1.67 - (sel_coitersN, map flat sel_coiter_thmsss),
1.68 - (corecsN, corec_thmss),
1.69 - (disc_corecsN, disc_corec_thmss),
1.70 - (sel_corecsN, map flat sel_corec_thmsss)]
1.71 - |> maps (fn (thmN, thmss) =>
1.72 + [(coitersN, coiter_thmss, []),
1.73 + (disc_coitersN, disc_coiter_thmss, []),
1.74 + (sel_coitersN, map flat sel_coiter_thmsss, []),
1.75 + (corecsN, corec_thmss, []),
1.76 + (disc_corecsN, disc_corec_thmss, []),
1.77 + (sel_corecsN, map flat sel_corec_thmsss, [])]
1.78 + |> maps (fn (thmN, thmss, attrs) =>
1.79 map_filter (fn (_, []) => NONE | (b, thms) =>
1.80 - SOME ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []),
1.81 + SOME ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), attrs),
1.82 [(thms, [])])) (bs ~~ thmss));
1.83 in
1.84 lthy |> Local_Theory.notes notes |> snd
2.1 --- a/src/HOL/Codatatype/Tools/bnf_wrap.ML Tue Sep 11 23:27:19 2012 +0200
2.2 +++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML Wed Sep 12 00:20:37 2012 +0200
2.3 @@ -46,7 +46,13 @@
2.4 val weak_case_cong_thmsN = "weak_case_cong";
2.5
2.6 val no_binder = @{binding ""};
2.7 -val fallback_binder = @{binding _};
2.8 +val std_binder = @{binding _};
2.9 +
2.10 +val induct_simp_attrs = @{attributes [induct_simp]};
2.11 +val cong_attrs = @{attributes [cong]};
2.12 +val iff_attrs = @{attributes [iff]};
2.13 +val safe_elim_attrs = @{attributes [elim!]};
2.14 +val simp_attrs = @{attributes [simp]};
2.15
2.16 fun pad_list x n xs = xs @ replicate (n - length xs) x;
2.17
2.18 @@ -67,11 +73,11 @@
2.19
2.20 fun eta_expand_case_arg xs f_xs = fold_rev Term.lambda xs f_xs;
2.21
2.22 -fun name_of_ctr c =
2.23 - (case head_of c of
2.24 - Const (s, _) => s
2.25 - | Free (s, _) => s
2.26 - | _ => error "Cannot extract name of constructor");
2.27 +fun base_name_of_ctr c =
2.28 + Long_Name.base_name (case head_of c of
2.29 + Const (s, _) => s
2.30 + | Free (s, _) => s
2.31 + | _ => error "Cannot extract name of constructor");
2.32
2.33 fun prepare_wrap_datatype prep_term (((no_dests, raw_ctrs), raw_case),
2.34 (raw_disc_binders, (raw_sel_binderss, raw_sel_defaultss))) no_defs_lthy =
2.35 @@ -91,15 +97,15 @@
2.36 val sel_defaultss =
2.37 pad_list [] n (map (map (apsnd (prep_term no_defs_lthy))) raw_sel_defaultss);
2.38
2.39 - val Type (fpT_name, As0) = body_type (fastype_of (hd ctrs0));
2.40 - val b = Binding.qualified_name fpT_name;
2.41 + val Type (dataT_name, As0) = body_type (fastype_of (hd ctrs0));
2.42 + val b = Binding.qualified_name dataT_name;
2.43
2.44 val (As, B) =
2.45 no_defs_lthy
2.46 |> mk_TFrees' (map Type.sort_of_atyp As0)
2.47 ||> the_single o fst o mk_TFrees 1;
2.48
2.49 - val fpT = Type (fpT_name, As);
2.50 + val dataT = Type (dataT_name, As);
2.51 val ctrs = map (mk_ctr As) ctrs0;
2.52 val ctr_Tss = map (binder_types o fastype_of) ctrs;
2.53
2.54 @@ -114,28 +120,28 @@
2.55 fun can_omit_disc_binder k m =
2.56 n = 1 orelse m = 0 orelse (n = 2 andalso can_rely_on_disc (3 - k));
2.57
2.58 - val fallback_disc_binder = Binding.name o prefix isN o Long_Name.base_name o name_of_ctr;
2.59 + val std_disc_binder = Binding.name o prefix isN o base_name_of_ctr;
2.60
2.61 val disc_binders =
2.62 raw_disc_binders'
2.63 |> map4 (fn k => fn m => fn ctr => fn disc =>
2.64 if Binding.eq_name (disc, no_binder) then
2.65 - if can_omit_disc_binder k m then NONE else SOME (fallback_disc_binder ctr)
2.66 - else if Binding.eq_name (disc, fallback_binder) then
2.67 - SOME (fallback_disc_binder ctr)
2.68 + if can_omit_disc_binder k m then NONE else SOME (std_disc_binder ctr)
2.69 + else if Binding.eq_name (disc, std_binder) then
2.70 + SOME (std_disc_binder ctr)
2.71 else
2.72 SOME disc) ks ms ctrs0;
2.73
2.74 val no_discs = map is_none disc_binders;
2.75 val no_discs_at_all = forall I no_discs;
2.76
2.77 - fun fallback_sel_binder m l = Binding.name o mk_unN m l o Long_Name.base_name o name_of_ctr;
2.78 + fun std_sel_binder m l = Binding.name o mk_unN m l o base_name_of_ctr;
2.79
2.80 val sel_binderss =
2.81 pad_list [] n raw_sel_binderss
2.82 |> map3 (fn ctr => fn m => map2 (fn l => fn sel =>
2.83 - if Binding.eq_name (sel, no_binder) orelse Binding.eq_name (sel, fallback_binder) then
2.84 - fallback_sel_binder m l ctr
2.85 + if Binding.eq_name (sel, no_binder) orelse Binding.eq_name (sel, std_binder) then
2.86 + std_sel_binder m l ctr
2.87 else
2.88 sel) (1 upto m) o pad_list no_binder m) ctrs0 ms;
2.89
2.90 @@ -153,8 +159,8 @@
2.91 ||>> mk_Freess "y" ctr_Tss
2.92 ||>> mk_Frees "f" case_Ts
2.93 ||>> mk_Frees "g" case_Ts
2.94 - ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "v") fpT
2.95 - ||>> yield_singleton (mk_Frees "w") fpT
2.96 + ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "v") dataT
2.97 + ||>> yield_singleton (mk_Frees "w") dataT
2.98 ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "P") HOLogic.boolT;
2.99
2.100 val q = Free (fst p', B --> HOLogic.boolT);
2.101 @@ -191,7 +197,7 @@
2.102 (true, [], [], [], [], [], no_defs_lthy)
2.103 else
2.104 let
2.105 - fun disc_free b = Free (Binding.name_of b, fpT --> HOLogic.boolT);
2.106 + fun disc_free b = Free (Binding.name_of b, dataT --> HOLogic.boolT);
2.107
2.108 fun disc_spec b exist_xs_v_eq_ctr = mk_Trueprop_eq (disc_free b $ v, exist_xs_v_eq_ctr);
2.109
2.110 @@ -224,7 +230,7 @@
2.111 quote (Binding.name_of b) ^ ": " ^ quote (Syntax.string_of_typ no_defs_lthy T) ^
2.112 " vs. " ^ quote (Syntax.string_of_typ no_defs_lthy T')));
2.113 in
2.114 - mk_Trueprop_eq (Free (Binding.name_of b, fpT --> T) $ v,
2.115 + mk_Trueprop_eq (Free (Binding.name_of b, dataT --> T) $ v,
2.116 Term.list_comb (mk_case As T, mk_sel_case_args b proto_sels T) $ v)
2.117 end;
2.118
2.119 @@ -237,11 +243,11 @@
2.120 else map (fn b => find_index (curry Binding.eq_name b) uniq_sel_binders) sel_binders;
2.121
2.122 val proto_sels = flat (map3 (fn k => fn xs => map (fn x => (k, (xs, x)))) ks xss xss);
2.123 - val sel_bundles =
2.124 + val sel_infos =
2.125 AList.group (op =) (sel_binder_index ~~ proto_sels)
2.126 |> sort (int_ord o pairself fst)
2.127 |> map snd |> curry (op ~~) uniq_sel_binders;
2.128 - val sel_binders = map fst sel_bundles;
2.129 + val sel_binders = map fst sel_infos;
2.130
2.131 fun unflat_selss xs = unflat_lookup Binding.eq_name sel_binders xs sel_binderss;
2.132
2.133 @@ -257,7 +263,7 @@
2.134 ks ms exist_xs_v_eq_ctrs disc_binders
2.135 ||>> apfst split_list o fold_map (fn (b, proto_sels) =>
2.136 Specification.definition (SOME (b, NONE, NoSyn),
2.137 - ((Thm.def_binding b, []), sel_spec b proto_sels)) #>> apsnd snd) sel_bundles
2.138 + ((Thm.def_binding b, []), sel_spec b proto_sels)) #>> apsnd snd) sel_infos
2.139 ||> `Local_Theory.restore;
2.140
2.141 (*transforms defined frees into consts (and more)*)
2.142 @@ -322,6 +328,8 @@
2.143 (Thm.instantiate (Tinst, []) (Drule.zero_var_indexes exhaust_thm))
2.144 end;
2.145
2.146 + val exhaust_cases = map base_name_of_ctr ctrs;
2.147 +
2.148 val other_half_distinct_thmss = map (map (fn thm => thm RS not_sym)) half_distinct_thmss;
2.149
2.150 val (distinct_thmsss', distinct_thmsss) =
2.151 @@ -425,8 +433,8 @@
2.152 HOLogic.mk_Trueprop (HOLogic.mk_not (betapply (disc', v)))))];
2.153 fun prove tac goal = Skip_Proof.prove lthy [] [] goal (K tac);
2.154
2.155 - val bundles = ms ~~ discD_thms ~~ discs ~~ no_discs;
2.156 - val half_pairss = mk_half_pairss bundles;
2.157 + val infos = ms ~~ discD_thms ~~ discs ~~ no_discs;
2.158 + val half_pairss = mk_half_pairss infos;
2.159
2.160 val goal_halvess = map mk_goal half_pairss;
2.161 val half_thmss =
2.162 @@ -542,27 +550,34 @@
2.163 (split_thm, split_asm_thm)
2.164 end;
2.165
2.166 + val cases_type_attr = Attrib.internal (K (Induct.cases_type dataT_name));
2.167 + val exhaust_case_names_attr = Attrib.internal (K (Rule_Cases.case_names exhaust_cases));
2.168 +
2.169 val notes =
2.170 - [(case_congN, [case_cong_thm]),
2.171 - (case_eqN, case_eq_thms),
2.172 - (casesN, case_thms),
2.173 - (collapseN, collapse_thms),
2.174 - (discsN, disc_thms),
2.175 - (disc_excludeN, disc_exclude_thms),
2.176 - (disc_exhaustN, disc_exhaust_thms),
2.177 - (distinctN, distinct_thms),
2.178 - (exhaustN, [exhaust_thm]),
2.179 - (injectN, flat inject_thmss),
2.180 - (nchotomyN, [nchotomy_thm]),
2.181 - (selsN, all_sel_thms),
2.182 - (splitN, [split_thm]),
2.183 - (split_asmN, [split_asm_thm]),
2.184 - (weak_case_cong_thmsN, [weak_case_cong_thm])]
2.185 - |> filter_out (null o snd)
2.186 - |> map (fn (thmN, thms) =>
2.187 - ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
2.188 + [(case_congN, [case_cong_thm], []),
2.189 + (case_eqN, case_eq_thms, []),
2.190 + (casesN, case_thms, simp_attrs),
2.191 + (collapseN, collapse_thms, simp_attrs),
2.192 + (discsN, disc_thms, simp_attrs),
2.193 + (disc_excludeN, disc_exclude_thms, []),
2.194 + (disc_exhaustN, disc_exhaust_thms, [exhaust_case_names_attr]),
2.195 + (distinctN, distinct_thms, simp_attrs @ induct_simp_attrs),
2.196 + (exhaustN, [exhaust_thm], [exhaust_case_names_attr, cases_type_attr]),
2.197 + (injectN, flat inject_thmss, iff_attrs @ induct_simp_attrs),
2.198 + (nchotomyN, [nchotomy_thm], []),
2.199 + (selsN, all_sel_thms, simp_attrs),
2.200 + (splitN, [split_thm], []),
2.201 + (split_asmN, [split_asm_thm], []),
2.202 + (weak_case_cong_thmsN, [weak_case_cong_thm], cong_attrs)]
2.203 + |> filter_out (null o #2)
2.204 + |> map (fn (thmN, thms, attrs) =>
2.205 + ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), attrs), [(thms, [])]));
2.206 +
2.207 + val notes' =
2.208 + [(map (fn th => th RS notE) distinct_thms, safe_elim_attrs)]
2.209 + |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
2.210 in
2.211 - ((selss, discI_thms, sel_thmss), lthy |> Local_Theory.notes notes |> snd)
2.212 + ((selss, discI_thms, sel_thmss), lthy |> Local_Theory.notes (notes' @ notes) |> snd)
2.213 end;
2.214 in
2.215 (goalss, after_qed, lthy')