--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Fri Oct 18 10:35:55 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Fri Oct 18 10:35:56 2013 +0200
@@ -207,8 +207,8 @@
val id_def = @{thm id_def};
val mp_conj = @{thm mp_conj};
-val nitpick_attrs = @{attributes [nitpick_simp]};
-val code_nitpick_simp_attrs = Code.add_default_eqn_attrib :: nitpick_attrs;
+val nitpicksimp_attrs = @{attributes [nitpick_simp]};
+val code_nitpicksimp_attrs = Code.add_default_eqn_attrib :: nitpicksimp_attrs;
val simp_attrs = @{attributes [simp]};
fun tvar_subst thy Ts Us =
@@ -763,7 +763,7 @@
val rec_thmss = mk_iter_thmss rec_args_types recs rec_defs (map co_rec_of ctor_iter_thmss);
in
((induct_thms, induct_thm, [induct_case_names_attr]),
- (fold_thmss, rec_thmss, code_nitpick_simp_attrs @ simp_attrs))
+ (fold_thmss, rec_thmss, code_nitpicksimp_attrs @ simp_attrs))
end;
fun derive_coinduct_coiters_thms_for_types pre_bnfs (z, cs, cpss,
@@ -1024,7 +1024,7 @@
coinduct_consumes_attr :: coinduct_case_names_attr :: coinduct_case_concl_attrs;
in
((coinduct_thms_pairs, coinduct_case_attrs),
- (unfold_thmss, corec_thmss, code_nitpick_simp_attrs),
+ (unfold_thmss, corec_thmss, code_nitpicksimp_attrs),
(disc_unfold_thmss, disc_corec_thmss, []),
(disc_unfold_iff_thmss, disc_corec_iff_thmss, simp_attrs),
(sel_unfold_thmsss, sel_corec_thmsss, simp_attrs))
@@ -1380,15 +1380,22 @@
val (rel_distinct_thms, _) =
join_halves n half_rel_distinct_thmss other_half_rel_distinct_thmss;
+ val anonymous_notes =
+ [(map (fn th => th RS @{thm eq_False[THEN iffD2]}) rel_distinct_thms,
+ code_nitpicksimp_attrs),
+ (map2 (fn th => fn 0 => th RS @{thm eq_True[THEN iffD2]} | _ => th)
+ rel_inject_thms ms, code_nitpicksimp_attrs)]
+ |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
+
val notes =
- [(mapN, map_thms, code_nitpick_simp_attrs @ simp_attrs),
- (rel_distinctN, rel_distinct_thms, code_nitpick_simp_attrs @ simp_attrs),
- (rel_injectN, rel_inject_thms, code_nitpick_simp_attrs @ simp_attrs),
- (setN, flat set_thmss, code_nitpick_simp_attrs @ simp_attrs)]
+ [(mapN, map_thms, code_nitpicksimp_attrs @ simp_attrs),
+ (rel_distinctN, rel_distinct_thms, simp_attrs),
+ (rel_injectN, rel_inject_thms, simp_attrs),
+ (setN, flat set_thmss, code_nitpicksimp_attrs @ simp_attrs)]
|> massage_simple_notes fp_b_name;
in
(((map_thms, rel_inject_thms, rel_distinct_thms, set_thmss), ctr_sugar),
- lthy |> Local_Theory.notes notes |> snd)
+ lthy |> Local_Theory.notes (anonymous_notes @ notes) |> snd)
end;
fun mk_binding suf = qualify false fp_b_name (Binding.suffix_name ("_" ^ suf) fp_b);
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML Fri Oct 18 10:35:55 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML Fri Oct 18 10:35:56 2013 +0200
@@ -39,10 +39,10 @@
val discN = "disc";
val selN = "sel";
-val nitpick_attrs = @{attributes [nitpick_simp]};
+val nitpicksimp_attrs = @{attributes [nitpick_simp]};
val simp_attrs = @{attributes [simp]};
-val code_nitpick_attrs = Code.add_default_eqn_attrib :: nitpick_attrs;
-val code_nitpick_simp_attrs = Code.add_default_eqn_attrib :: nitpick_attrs @ simp_attrs;
+val code_nitpicksimp_attrs = Code.add_default_eqn_attrib :: nitpicksimp_attrs;
+val code_nitpicksimp_simp_attrs = Code.add_default_eqn_attrib :: nitpicksimp_attrs @ simp_attrs;
exception Primrec_Error of string * term list;
@@ -407,7 +407,7 @@
val (bs, attrss) = map_split (fst o nth specs) poss;
val notes =
map3 (fn b => fn attrs => fn thm =>
- ((Binding.qualify false prefix b, code_nitpick_simp_attrs @ attrs), [([thm], [])]))
+ ((Binding.qualify false prefix b, code_nitpicksimp_simp_attrs @ attrs), [([thm], [])]))
bs attrss thms;
in
((Binding.qualify true prefix (Binding.name simpsN), []), [(thms, [])]) :: notes
@@ -1039,7 +1039,7 @@
val notes =
[(coinductN, map (if n2m then single else K []) coinduct_thms, []),
- (codeN, code_thmss, code_nitpick_attrs),
+ (codeN, code_thmss, code_nitpicksimp_attrs),
(ctrN, ctr_thmss, []),
(discN, disc_thmss, simp_attrs),
(selN, sel_thmss, simp_attrs),
--- a/src/HOL/BNF/Tools/ctr_sugar.ML Fri Oct 18 10:35:55 2013 +0200
+++ b/src/HOL/BNF/Tools/ctr_sugar.ML Fri Oct 18 10:35:56 2013 +0200
@@ -174,10 +174,10 @@
val dest_attrs = @{attributes [dest]};
val safe_elim_attrs = @{attributes [elim!]};
val iff_attrs = @{attributes [iff]};
-val induct_simp_attrs = @{attributes [induct_simp]};
-val nitpick_attrs = @{attributes [nitpick_simp]};
+val inductsimp_attrs = @{attributes [induct_simp]};
+val nitpicksimp_attrs = @{attributes [nitpick_simp]};
val simp_attrs = @{attributes [simp]};
-val code_nitpick_simp_simp_attrs = Code.add_default_eqn_attrib :: nitpick_attrs @ simp_attrs;
+val code_nitpicksimp_simp_attrs = Code.add_default_eqn_attrib :: nitpicksimp_attrs @ simp_attrs;
fun unflat_lookup eq xs ys = map (fn xs' => permute_like eq xs xs' ys);
@@ -870,7 +870,7 @@
val cases_type_attr = Attrib.internal (K (Induct.cases_type fcT_name));
val notes =
- [(caseN, case_thms, code_nitpick_simp_simp_attrs),
+ [(caseN, case_thms, code_nitpicksimp_simp_attrs),
(case_congN, [case_cong_thm], []),
(case_conv_ifN, case_conv_if_thms, []),
(collapseN, safe_collapse_thms, simp_attrs),
@@ -878,12 +878,12 @@
(discIN, nontriv_discI_thms, []),
(disc_excludeN, disc_exclude_thms, dest_attrs),
(disc_exhaustN, disc_exhaust_thms, [exhaust_case_names_attr]),
- (distinctN, distinct_thms, simp_attrs @ induct_simp_attrs),
+ (distinctN, distinct_thms, simp_attrs @ inductsimp_attrs),
(exhaustN, [exhaust_thm], [exhaust_case_names_attr, cases_type_attr]),
(expandN, expand_thms, []),
- (injectN, inject_thms, iff_attrs @ induct_simp_attrs),
+ (injectN, inject_thms, iff_attrs @ inductsimp_attrs),
(nchotomyN, [nchotomy_thm], []),
- (selN, all_sel_thms, code_nitpick_simp_simp_attrs),
+ (selN, all_sel_thms, code_nitpicksimp_simp_attrs),
(sel_exhaustN, sel_exhaust_thms, [exhaust_case_names_attr]),
(sel_splitN, sel_split_thms, []),
(sel_split_asmN, sel_split_asm_thms, []),
@@ -895,7 +895,7 @@
|> map (fn (thmN, thms, attrs) =>
((qualify true (Binding.name thmN), attrs), [(thms, [])]));
- val notes' =
+ val anonymous_notes =
[(map (fn th => th RS notE) distinct_thms, safe_elim_attrs)]
|> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
@@ -915,7 +915,7 @@
(Local_Theory.declaration {syntax = false, pervasive = true}
(fn phi => Case_Translation.register
(Morphism.term phi casex) (map (Morphism.term phi) ctrs)))
- |> Local_Theory.notes (notes' @ notes) |> snd
+ |> Local_Theory.notes (anonymous_notes @ notes) |> snd
|> register_ctr_sugar fcT_name ctr_sugar)
end;
in