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)`

?

how about `auto elim: rl`

?

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.

Is it always about `o_literal_cases`

? If so, I'd just prove the split rule form the case rule and then use it.

Yes, that would work but shouldn't there be an automatic conversion?

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.

I don't think you need non-overlapping. The problem is rather that a split rule requires an if-and-only-if

which is more specific than an "elim" rule

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: Dec 07 2023 at 20:16 UTC