## Stream: General

### Topic: Convert case rules into split rules

#### 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: Dec 07 2023 at 08:19 UTC