132 val safe_elim_attrs = @{attributes [elim!]}; |
132 val safe_elim_attrs = @{attributes [elim!]}; |
133 val iff_attrs = @{attributes [iff]}; |
133 val iff_attrs = @{attributes [iff]}; |
134 val induct_simp_attrs = @{attributes [induct_simp]}; |
134 val induct_simp_attrs = @{attributes [induct_simp]}; |
135 val nitpick_attrs = @{attributes [nitpick_simp]}; |
135 val nitpick_attrs = @{attributes [nitpick_simp]}; |
136 val simp_attrs = @{attributes [simp]}; |
136 val simp_attrs = @{attributes [simp]}; |
137 val code_nitpick_simp_attrs = Code.add_default_eqn_attrib :: nitpick_attrs @ simp_attrs; |
137 val code_nitpick_simp_simp_attrs = Code.add_default_eqn_attrib :: nitpick_attrs @ simp_attrs; |
138 |
138 |
139 fun unflat_lookup eq xs ys = map (fn xs' => permute_like eq xs xs' ys); |
139 fun unflat_lookup eq xs ys = map (fn xs' => permute_like eq xs xs' ys); |
140 |
140 |
141 fun mk_half_pairss' _ ([], []) = [] |
141 fun mk_half_pairss' _ ([], []) = [] |
142 | mk_half_pairss' indent (x :: xs, _ :: ys) = |
142 | mk_half_pairss' indent (x :: xs, _ :: ys) = |
758 |
758 |
759 val exhaust_case_names_attr = Attrib.internal (K (Rule_Cases.case_names exhaust_cases)); |
759 val exhaust_case_names_attr = Attrib.internal (K (Rule_Cases.case_names exhaust_cases)); |
760 val cases_type_attr = Attrib.internal (K (Induct.cases_type dataT_name)); |
760 val cases_type_attr = Attrib.internal (K (Induct.cases_type dataT_name)); |
761 |
761 |
762 val notes = |
762 val notes = |
763 [(caseN, case_thms, code_nitpick_simp_attrs), |
763 [(caseN, case_thms, code_nitpick_simp_simp_attrs), |
764 (case_congN, [case_cong_thm], []), |
764 (case_congN, [case_cong_thm], []), |
765 (case_convN, case_conv_thms, []), |
765 (case_convN, case_conv_thms, []), |
766 (collapseN, safe_collapse_thms, simp_attrs), |
766 (collapseN, safe_collapse_thms, simp_attrs), |
767 (discN, nontriv_disc_thms, simp_attrs), |
767 (discN, nontriv_disc_thms, simp_attrs), |
768 (discIN, nontriv_discI_thms, []), |
768 (discIN, nontriv_discI_thms, []), |
771 (distinctN, distinct_thms, simp_attrs @ induct_simp_attrs), |
771 (distinctN, distinct_thms, simp_attrs @ induct_simp_attrs), |
772 (exhaustN, [exhaust_thm], [exhaust_case_names_attr, cases_type_attr]), |
772 (exhaustN, [exhaust_thm], [exhaust_case_names_attr, cases_type_attr]), |
773 (expandN, expand_thms, []), |
773 (expandN, expand_thms, []), |
774 (injectN, inject_thms, iff_attrs @ induct_simp_attrs), |
774 (injectN, inject_thms, iff_attrs @ induct_simp_attrs), |
775 (nchotomyN, [nchotomy_thm], []), |
775 (nchotomyN, [nchotomy_thm], []), |
776 (selN, all_sel_thms, code_nitpick_simp_attrs), |
776 (selN, all_sel_thms, code_nitpick_simp_simp_attrs), |
777 (splitN, [split_thm], []), |
777 (splitN, [split_thm], []), |
778 (split_asmN, [split_asm_thm], []), |
778 (split_asmN, [split_asm_thm], []), |
779 (splitsN, [split_thm, split_asm_thm], []), |
779 (splitsN, [split_thm, split_asm_thm], []), |
780 (weak_case_cong_thmsN, [weak_case_cong_thm], cong_attrs)] |
780 (weak_case_cong_thmsN, [weak_case_cong_thm], cong_attrs)] |
781 |> filter_out (null o #2) |
781 |> filter_out (null o #2) |