# HG changeset patch # User blanchet # Date 1382085356 -7200 # Node ID 297d1c6039993128d003fd324cc7ea20639f4a6f # Parent 0fadd32e8d50425f733eff0f82a387920775b6b1 make sure that registered code equations are actually equations diff -r 0fadd32e8d50 -r 297d1c603999 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML --- 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); diff -r 0fadd32e8d50 -r 297d1c603999 src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML --- 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), diff -r 0fadd32e8d50 -r 297d1c603999 src/HOL/BNF/Tools/ctr_sugar.ML --- 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