## Stream: Beginner Questions

### Topic: split vs cases

#### Gergely Buday (Jan 22 2021 at 08:37):

What is the difference between split and cases? Both are doing case splitting.

#### Mathias Fleury (Jan 22 2021 at 08:45):

Not really. `split` looks at the structure of the goal while `cases` looks for terms to split on. Hence, this fails:

``````lemma"P xs" for xs :: "nat list"
apply(split list.split)
``````

#### Mathias Fleury (Jan 22 2021 at 08:46):

I have never used split in my life... only as argument for simp/auto. I don't believe it is really useful.

#### Gergely Buday (Jan 22 2021 at 08:51):

Concrete Semantics recommends it feeding a .split rule for a datatype:

``````type_synonym vname = string
datatype aexp = N int | V vname | Plus aexp aexp

type_synonym val = int
type_synonym state = "vname ⇒ val"

fun aval :: "aexp ⇒ state ⇒ val" where
"aval (N n) s = n" |
"aval (V x ) s = s x" |
"aval (Plus a1 a2 ) s = aval a1 s + aval a2 s"

fun asimp_const :: "aexp ⇒ aexp" where
"asimp_const (N n) = N n"
| "asimp_const (V x ) = V x"
| "asimp_const (Plus a1 a2 ) =
(case (asimp_const a1 , asimp_const a2 ) of
(N n1, N n2) ⇒ N (n1+n2)
| (b1, b2)     ⇒ Plus b1 b2)"

lemma "aval (asimp_const a) s = aval a s"
by (induction a) (auto split: aexp.split)
``````

#### Mathias Fleury (Jan 22 2021 at 08:54):

list is a datatype... The theorem `if_split` can be useful as argument for split.

#### Manuel Eberl (Jan 22 2021 at 08:57):

The `split` rules for `simp`/`auto` automatically perform case distinctions whenever there is a certain matching expression in the goal. This mostly concerns `if` and `case` expressions.

The `cases` tactic, on the other hand, allows you to do case distinctions on specific terms manually.

#### Manuel Eberl (Jan 22 2021 at 08:57):

The `split` tactic that Mathias mentioned is unrelated (but also uses `split` rules, I think) and indeed I've never seen anyone use it. But that's probably not what you meant.

Last updated: Dec 07 2023 at 20:16 UTC