# HG changeset patch # User blanchet # Date 1347402037 -7200 # Node ID c707df2e20830aba8062a49b5cd81024dab58eb3 # Parent f9f240dfb50bb2226d91c2a880f78d128ef3ea28 added attributes to theorems diff -r f9f240dfb50b -r c707df2e2083 src/HOL/Codatatype/Tools/bnf_fp_sugar.ML --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Tue Sep 11 23:27:19 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Wed Sep 12 00:20:37 2012 +0200 @@ -34,6 +34,8 @@ val sel_coitersN = "sel_coiters"; val sel_corecsN = "sel_corecs"; +val simp_attrs = @{attributes [simp]}; + fun split_list11 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, map #11 xs); @@ -424,12 +426,14 @@ map2 (mk_sum_caseN_balanced oo map2 mk_uncurried2_fun) fss xssss)); in (binder, spec) end; - val iter_like_bundles = + val iter_like_infos = [(iterN, fp_iter, iter_only), (recN, fp_rec, rec_only)]; - val (binders, specs) = map generate_iter_like iter_like_bundles |> split_list; + val (binders, specs) = map generate_iter_like iter_like_infos |> split_list; + (* TODO: Allow same constructor (and selector/discriminator) names for different + types (cf. old "datatype" package) *) val ((csts, defs), (lthy', lthy)) = no_defs_lthy |> apfst split_list o fold_map2 (fn b => fn spec => Specification.definition (SOME (b, NONE, NoSyn), ((Thm.def_binding b, []), spec)) @@ -468,11 +472,11 @@ map5 mk_preds_getterss_join cs ns cpss f_sum_prod_Ts cqfsss)); in (binder, spec) end; - val coiter_like_bundles = + val coiter_like_infos = [(coiterN, fp_iter, coiter_only), (corecN, fp_rec, corec_only)]; - val (binders, specs) = map generate_coiter_like coiter_like_bundles |> split_list; + val (binders, specs) = map generate_coiter_like coiter_like_infos |> split_list; val ((csts, defs), (lthy', lthy)) = no_defs_lthy |> apfst split_list o fold_map2 (fn b => fn spec => @@ -569,12 +573,12 @@ end; val notes = - [(itersN, iter_thmss), - (recsN, rec_thmss)] - |> maps (fn (thmN, thmss) => + [(itersN, iter_thmss, simp_attrs), + (recsN, rec_thmss, Code.add_default_eqn_attrib :: simp_attrs)] + |> maps (fn (thmN, thmss, attrs) => map2 (fn b => fn thms => - ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])) - bs thmss); + ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), attrs), + [(thms, [])])) bs thmss); in lthy |> Local_Theory.notes notes |> snd end; @@ -663,15 +667,15 @@ map3 (map3 (map2 o mk_sel_coiter_like_thm)) corec_thmss selsss sel_thmsss; val notes = - [(coitersN, coiter_thmss), - (disc_coitersN, disc_coiter_thmss), - (sel_coitersN, map flat sel_coiter_thmsss), - (corecsN, corec_thmss), - (disc_corecsN, disc_corec_thmss), - (sel_corecsN, map flat sel_corec_thmsss)] - |> maps (fn (thmN, thmss) => + [(coitersN, coiter_thmss, []), + (disc_coitersN, disc_coiter_thmss, []), + (sel_coitersN, map flat sel_coiter_thmsss, []), + (corecsN, corec_thmss, []), + (disc_corecsN, disc_corec_thmss, []), + (sel_corecsN, map flat sel_corec_thmsss, [])] + |> maps (fn (thmN, thmss, attrs) => map_filter (fn (_, []) => NONE | (b, thms) => - SOME ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), + SOME ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), attrs), [(thms, [])])) (bs ~~ thmss)); in lthy |> Local_Theory.notes notes |> snd diff -r f9f240dfb50b -r c707df2e2083 src/HOL/Codatatype/Tools/bnf_wrap.ML --- a/src/HOL/Codatatype/Tools/bnf_wrap.ML Tue Sep 11 23:27:19 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML Wed Sep 12 00:20:37 2012 +0200 @@ -46,7 +46,13 @@ val weak_case_cong_thmsN = "weak_case_cong"; val no_binder = @{binding ""}; -val fallback_binder = @{binding _}; +val std_binder = @{binding _}; + +val induct_simp_attrs = @{attributes [induct_simp]}; +val cong_attrs = @{attributes [cong]}; +val iff_attrs = @{attributes [iff]}; +val safe_elim_attrs = @{attributes [elim!]}; +val simp_attrs = @{attributes [simp]}; fun pad_list x n xs = xs @ replicate (n - length xs) x; @@ -67,11 +73,11 @@ fun eta_expand_case_arg xs f_xs = fold_rev Term.lambda xs f_xs; -fun name_of_ctr c = - (case head_of c of - Const (s, _) => s - | Free (s, _) => s - | _ => error "Cannot extract name of constructor"); +fun base_name_of_ctr c = + Long_Name.base_name (case head_of c of + Const (s, _) => s + | Free (s, _) => s + | _ => error "Cannot extract name of constructor"); fun prepare_wrap_datatype prep_term (((no_dests, raw_ctrs), raw_case), (raw_disc_binders, (raw_sel_binderss, raw_sel_defaultss))) no_defs_lthy = @@ -91,15 +97,15 @@ val sel_defaultss = pad_list [] n (map (map (apsnd (prep_term no_defs_lthy))) raw_sel_defaultss); - val Type (fpT_name, As0) = body_type (fastype_of (hd ctrs0)); - val b = Binding.qualified_name fpT_name; + val Type (dataT_name, As0) = body_type (fastype_of (hd ctrs0)); + val b = Binding.qualified_name dataT_name; val (As, B) = no_defs_lthy |> mk_TFrees' (map Type.sort_of_atyp As0) ||> the_single o fst o mk_TFrees 1; - val fpT = Type (fpT_name, As); + val dataT = Type (dataT_name, As); val ctrs = map (mk_ctr As) ctrs0; val ctr_Tss = map (binder_types o fastype_of) ctrs; @@ -114,28 +120,28 @@ fun can_omit_disc_binder k m = n = 1 orelse m = 0 orelse (n = 2 andalso can_rely_on_disc (3 - k)); - val fallback_disc_binder = Binding.name o prefix isN o Long_Name.base_name o name_of_ctr; + val std_disc_binder = Binding.name o prefix isN o base_name_of_ctr; val disc_binders = raw_disc_binders' |> map4 (fn k => fn m => fn ctr => fn disc => if Binding.eq_name (disc, no_binder) then - if can_omit_disc_binder k m then NONE else SOME (fallback_disc_binder ctr) - else if Binding.eq_name (disc, fallback_binder) then - SOME (fallback_disc_binder ctr) + if can_omit_disc_binder k m then NONE else SOME (std_disc_binder ctr) + else if Binding.eq_name (disc, std_binder) then + SOME (std_disc_binder ctr) else SOME disc) ks ms ctrs0; val no_discs = map is_none disc_binders; val no_discs_at_all = forall I no_discs; - fun fallback_sel_binder m l = Binding.name o mk_unN m l o Long_Name.base_name o name_of_ctr; + fun std_sel_binder m l = Binding.name o mk_unN m l o base_name_of_ctr; val sel_binderss = pad_list [] n raw_sel_binderss |> map3 (fn ctr => fn m => map2 (fn l => fn sel => - if Binding.eq_name (sel, no_binder) orelse Binding.eq_name (sel, fallback_binder) then - fallback_sel_binder m l ctr + if Binding.eq_name (sel, no_binder) orelse Binding.eq_name (sel, std_binder) then + std_sel_binder m l ctr else sel) (1 upto m) o pad_list no_binder m) ctrs0 ms; @@ -153,8 +159,8 @@ ||>> mk_Freess "y" ctr_Tss ||>> mk_Frees "f" case_Ts ||>> mk_Frees "g" case_Ts - ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "v") fpT - ||>> yield_singleton (mk_Frees "w") fpT + ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "v") dataT + ||>> yield_singleton (mk_Frees "w") dataT ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "P") HOLogic.boolT; val q = Free (fst p', B --> HOLogic.boolT); @@ -191,7 +197,7 @@ (true, [], [], [], [], [], no_defs_lthy) else let - fun disc_free b = Free (Binding.name_of b, fpT --> HOLogic.boolT); + fun disc_free b = Free (Binding.name_of b, dataT --> HOLogic.boolT); fun disc_spec b exist_xs_v_eq_ctr = mk_Trueprop_eq (disc_free b $ v, exist_xs_v_eq_ctr); @@ -224,7 +230,7 @@ quote (Binding.name_of b) ^ ": " ^ quote (Syntax.string_of_typ no_defs_lthy T) ^ " vs. " ^ quote (Syntax.string_of_typ no_defs_lthy T'))); in - mk_Trueprop_eq (Free (Binding.name_of b, fpT --> T) $ v, + mk_Trueprop_eq (Free (Binding.name_of b, dataT --> T) $ v, Term.list_comb (mk_case As T, mk_sel_case_args b proto_sels T) $ v) end; @@ -237,11 +243,11 @@ else map (fn b => find_index (curry Binding.eq_name b) uniq_sel_binders) sel_binders; val proto_sels = flat (map3 (fn k => fn xs => map (fn x => (k, (xs, x)))) ks xss xss); - val sel_bundles = + val sel_infos = AList.group (op =) (sel_binder_index ~~ proto_sels) |> sort (int_ord o pairself fst) |> map snd |> curry (op ~~) uniq_sel_binders; - val sel_binders = map fst sel_bundles; + val sel_binders = map fst sel_infos; fun unflat_selss xs = unflat_lookup Binding.eq_name sel_binders xs sel_binderss; @@ -257,7 +263,7 @@ ks ms exist_xs_v_eq_ctrs disc_binders ||>> apfst split_list o fold_map (fn (b, proto_sels) => Specification.definition (SOME (b, NONE, NoSyn), - ((Thm.def_binding b, []), sel_spec b proto_sels)) #>> apsnd snd) sel_bundles + ((Thm.def_binding b, []), sel_spec b proto_sels)) #>> apsnd snd) sel_infos ||> `Local_Theory.restore; (*transforms defined frees into consts (and more)*) @@ -322,6 +328,8 @@ (Thm.instantiate (Tinst, []) (Drule.zero_var_indexes exhaust_thm)) end; + val exhaust_cases = map base_name_of_ctr ctrs; + val other_half_distinct_thmss = map (map (fn thm => thm RS not_sym)) half_distinct_thmss; val (distinct_thmsss', distinct_thmsss) = @@ -425,8 +433,8 @@ HOLogic.mk_Trueprop (HOLogic.mk_not (betapply (disc', v)))))]; fun prove tac goal = Skip_Proof.prove lthy [] [] goal (K tac); - val bundles = ms ~~ discD_thms ~~ discs ~~ no_discs; - val half_pairss = mk_half_pairss bundles; + val infos = ms ~~ discD_thms ~~ discs ~~ no_discs; + val half_pairss = mk_half_pairss infos; val goal_halvess = map mk_goal half_pairss; val half_thmss = @@ -542,27 +550,34 @@ (split_thm, split_asm_thm) end; + val cases_type_attr = Attrib.internal (K (Induct.cases_type dataT_name)); + val exhaust_case_names_attr = Attrib.internal (K (Rule_Cases.case_names exhaust_cases)); + val notes = - [(case_congN, [case_cong_thm]), - (case_eqN, case_eq_thms), - (casesN, case_thms), - (collapseN, collapse_thms), - (discsN, disc_thms), - (disc_excludeN, disc_exclude_thms), - (disc_exhaustN, disc_exhaust_thms), - (distinctN, distinct_thms), - (exhaustN, [exhaust_thm]), - (injectN, flat inject_thmss), - (nchotomyN, [nchotomy_thm]), - (selsN, all_sel_thms), - (splitN, [split_thm]), - (split_asmN, [split_asm_thm]), - (weak_case_cong_thmsN, [weak_case_cong_thm])] - |> filter_out (null o snd) - |> map (fn (thmN, thms) => - ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])); + [(case_congN, [case_cong_thm], []), + (case_eqN, case_eq_thms, []), + (casesN, case_thms, simp_attrs), + (collapseN, collapse_thms, simp_attrs), + (discsN, disc_thms, simp_attrs), + (disc_excludeN, disc_exclude_thms, []), + (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), + (nchotomyN, [nchotomy_thm], []), + (selsN, all_sel_thms, simp_attrs), + (splitN, [split_thm], []), + (split_asmN, [split_asm_thm], []), + (weak_case_cong_thmsN, [weak_case_cong_thm], cong_attrs)] + |> filter_out (null o #2) + |> map (fn (thmN, thms, attrs) => + ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), attrs), [(thms, [])])); + + val notes' = + [(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 |> snd) + ((selss, discI_thms, sel_thmss), lthy |> Local_Theory.notes (notes' @ notes) |> snd) end; in (goalss, after_qed, lthy')