equal
deleted
inserted
replaced
1497 | is_conj @{const induct_false} = true |
1497 | is_conj @{const induct_false} = true |
1498 | is_conj _ = false |
1498 | is_conj _ = false |
1499 in if is_conj P then SOME @{thm induct_conj_curry} else NONE end |
1499 in if is_conj P then SOME @{thm induct_conj_curry} else NONE end |
1500 | _ => NONE))] |
1500 | _ => NONE))] |
1501 |> Simplifier.set_mksimps (fn ss => Simpdata.mksimps Simpdata.mksimps_pairs ss #> |
1501 |> Simplifier.set_mksimps (fn ss => Simpdata.mksimps Simpdata.mksimps_pairs ss #> |
1502 map (Simplifier.rewrite_rule (map Thm.symmetric |
1502 map (rewrite_rule (map Thm.symmetric @{thms induct_rulify_fallback}))))) |
1503 @{thms induct_rulify_fallback}))))) |
|
1504 *} |
1503 *} |
1505 |
1504 |
1506 text {* Pre-simplification of induction and cases rules *} |
1505 text {* Pre-simplification of induction and cases rules *} |
1507 |
1506 |
1508 lemma [induct_simp]: "(!!x. induct_equal x t ==> PROP P x) == PROP P t" |
1507 lemma [induct_simp]: "(!!x. induct_equal x t ==> PROP P x) == PROP P t" |