429 given_pats |
429 given_pats |
430 val (case_rewrites,context_congs) = extraction_thms theory |
430 val (case_rewrites,context_congs) = extraction_thms theory |
431 (*case_ss causes minimal simplification: bodies of case expressions are |
431 (*case_ss causes minimal simplification: bodies of case expressions are |
432 not simplified. Otherwise large examples (Red-Black trees) are too |
432 not simplified. Otherwise large examples (Red-Black trees) are too |
433 slow.*) |
433 slow.*) |
434 val case_ss = Simplifier.global_context theory |
434 val case_ss = |
435 (HOL_basic_ss addcongs |
435 Simplifier.global_context theory |
436 (map (#weak_case_cong o snd) o Symtab.dest o Datatype.get_all) theory addsimps case_rewrites) |
436 (HOL_basic_ss addsimps case_rewrites |
|
437 |> fold (Simplifier.add_cong o #weak_case_cong o snd) |
|
438 (Symtab.dest (Datatype.get_all theory))) |
437 val corollaries' = map (Simplifier.simplify case_ss) corollaries |
439 val corollaries' = map (Simplifier.simplify case_ss) corollaries |
438 val extract = Rules.CONTEXT_REWRITE_RULE |
440 val extract = Rules.CONTEXT_REWRITE_RULE |
439 (f, [R], @{thm cut_apply}, meta_tflCongs@context_congs) |
441 (f, [R], @{thm cut_apply}, meta_tflCongs@context_congs) |
440 val (rules, TCs) = ListPair.unzip (map extract corollaries') |
442 val (rules, TCs) = ListPair.unzip (map extract corollaries') |
441 val rules0 = map (rewrite_rule [Thms.CUT_DEF]) rules |
443 val rules0 = map (rewrite_rule [Thms.CUT_DEF]) rules |