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

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

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

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

list is a datatype... The theorem `if_split`

can be useful as argument for split.

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.

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