Gergely Buday (Jan 22 2021 at 08:37): 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)
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)
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: Nov 13 2025 at 04:27 UTC