What is the difference between split and cases? Both are doing case splitting.
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.
split rules for
auto automatically perform case distinctions whenever there is a certain matching expression in the goal. This mostly concerns
cases tactic, on the other hand, allows you to do case distinctions on specific terms manually.
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