279 map (RuleCases.case_names o exhaust_cases descr o #1) |
279 map (RuleCases.case_names o exhaust_cases descr o #1) |
280 (List.filter (fn ((_, (name, _, _))) => name mem_string new) descr); |
280 (List.filter (fn ((_, (name, _, _))) => name mem_string new) descr); |
281 |
281 |
282 end; |
282 end; |
283 |
283 |
|
284 fun name_notE th = |
|
285 Thm.name_thm (Thm.name_of_thm th ^ "_E", th RS notE); |
|
286 |
284 fun add_rules simps case_thms size_thms rec_thms inject distinct |
287 fun add_rules simps case_thms size_thms rec_thms inject distinct |
285 weak_case_congs cong_att = |
288 weak_case_congs cong_att = |
286 (#1 o PureThy.add_thmss [(("simps", simps), []), |
289 (#1 o PureThy.add_thmss [(("simps", simps), []), |
287 (("", List.concat case_thms @ size_thms @ |
290 (("", List.concat case_thms @ size_thms @ |
288 List.concat distinct @ rec_thms), [Simplifier.simp_add_global]), |
291 List.concat distinct @ rec_thms), [Simplifier.simp_add_global]), |
289 (("", size_thms @ rec_thms), [RecfunCodegen.add NONE]), |
292 (("", size_thms @ rec_thms), [RecfunCodegen.add NONE]), |
290 (("", List.concat inject), [iff_add_global]), |
293 (("", List.concat inject), [iff_add_global]), |
291 (("", List.concat distinct RL [notE]), [Classical.safe_elim_global]), |
294 (("", map name_notE (List.concat distinct)), [Classical.safe_elim_global]), |
292 (("", weak_case_congs), [cong_att])]); |
295 (("", weak_case_congs), [cong_att])]); |
293 |
296 |
294 |
297 |
295 (* add_cases_induct *) |
298 (* add_cases_induct *) |
296 |
299 |