Stream: Beginner Questions

Topic: split vs cases


view this post on Zulip Gergely Buday (Jan 22 2021 at 08:37):

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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Mathias Fleury (Jan 22 2021 at 08:54):

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

view this post on Zulip 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.

view this post on Zulip 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: Mar 28 2024 at 16:17 UTC