Lukas Stevens (Mar 17 2020 at 16:33): Lukas Stevens (Mar 17 2020 at 16:33):Is there any way to convert a case rule into a split rule such that the rule can be used with apply(simp split: rl)?
Kevin Kappelmann (Mar 17 2020 at 17:02):how about auto elim: rl?
Lukas Stevens (Mar 17 2020 at 17:14):That does not work. For reference, my proof looks like follows:
proof(induction φ)
case (Atom x)
then show ?case
apply(cases x rule: o_literal_cases) by auto
qed (auto simp: and_def or_def neg_def split: if_splits)
What I want to have is:
apply(induction φ) by (auto simp: and_def or_def neg_def split: if_splits o_literal_cases)
I have several proofs of this form and all would go through if the split on x would happen automatically.
Kevin Kappelmann (Mar 17 2020 at 17:23):Is it always about o_literal_cases? If so, I'd just prove the split rule form the case rule and then use it.
Lukas Stevens (Mar 17 2020 at 17:24):Yes, that would work but shouldn't there be an automatic conversion?
Kevin Kappelmann (Mar 17 2020 at 18:47):I think that only works under certain conditions (e.g. non-overlapping cases) and proving the split lemma is the easiest way in this case.
Manuel Eberl (Mar 17 2020 at 18:51):I don't think you need non-overlapping. The problem is rather that a split rule requires an if-and-only-if
Manuel Eberl (Mar 17 2020 at 18:51):which is more specific than an "elim" rule
Kevin Kappelmann (Mar 17 2020 at 19:42):Manuel Eberl said:
I don't think you need non-overlapping. The problem is rather that a split rule requires an if-and-only-if
Yes that's the core problem. I thought that non-overlapping cases would maybe allow you to do some sort of automatic conversion, but idk
Last updated: Oct 12 2024 at 20:18 UTC