444 val R = #Rand(S.dest_comb WFR) |
444 val R = #Rand(S.dest_comb WFR) |
445 val corollary' = R.UNDISCH corollary (* put WF R on assums *) |
445 val corollary' = R.UNDISCH corollary (* put WF R on assums *) |
446 val corollaries = map (fn pat => R.SPEC (tych pat) corollary') |
446 val corollaries = map (fn pat => R.SPEC (tych pat) corollary') |
447 given_pats |
447 given_pats |
448 val (case_rewrites,context_congs) = extraction_thms theory |
448 val (case_rewrites,context_congs) = extraction_thms theory |
449 val corollaries' = map(rewrite_rule case_rewrites) corollaries |
449 val case_ss = HOL_basic_ss addcongs |
|
450 DatatypePackage.weak_case_congs_of theory addsimps case_rewrites |
|
451 val corollaries' = map (Simplifier.simplify case_ss) corollaries |
450 val extract = R.CONTEXT_REWRITE_RULE |
452 val extract = R.CONTEXT_REWRITE_RULE |
451 (f, [R], cut_apply, meta_tflCongs@context_congs) |
453 (f, [R], cut_apply, meta_tflCongs@context_congs) |
452 val (rules, TCs) = ListPair.unzip (map extract corollaries') |
454 val (rules, TCs) = ListPair.unzip (map extract corollaries') |
453 val rules0 = map (rewrite_rule [Thms.CUT_DEF]) rules |
455 val rules0 = map (rewrite_rule [Thms.CUT_DEF]) rules |
454 val mk_cond_rule = R.FILTER_DISCH_ALL(not o curry (op aconv) WFR) |
456 val mk_cond_rule = R.FILTER_DISCH_ALL(not o curry (op aconv) WFR) |