## Stream: General

### Topic: split all case expressions

#### Max W. Haslbeck (Nov 02 2020 at 16:01):

I have a lemma/code with lots of case expressions. To split each one of them I have to add the corresponding `splits` rule for every type that appears. For example:

``````lemma "(case xs of [] ⇒ (case n of 0 ⇒ True | Suc x ⇒ True) | (x#xs) ⇒ True) = True"
by (auto split: list.splits nat.splits)
``````

Does someone know of a way to do this automatically? I want a method that does: Split all case expression in the current subgoal.

#### Mathias Fleury (Nov 02 2020 at 16:08):

If you can live with declaring the splitting rules once:

``````named_theorems mysplit "Theorems used by mysplit"
declare list.splits[mysplit] nat.splits[mysplit]
method mysplit = (split list.splits nat.splits)+

lemma "(case xs of [] ⇒ (case n of 0 ⇒ True | Suc x ⇒ True) | (x#xs) ⇒ True) = True"
apply mysplit
``````

#### Max W. Haslbeck (Nov 02 2020 at 16:38):

I still would like to know if such a method is generally possible.

#### Mathias Fleury (Nov 02 2020 at 17:03):

A very low-tech: find all constants that contain the name `case_`. The part after the `_` of the name contains the type name. Therefore the theorem `[stuff_after_the_underscore].splits` will give the theorem you want to use.

#### Mathias Fleury (Nov 02 2020 at 17:30):

``````ML ‹
fun split_thms ctxt t =
(case first_field "case_" t of
NONE => []
| SOME (_, stuff) =>
(Proof_Context.get_thms ctxt (stuff ^ ".splits") handle _ => [])
)

fun find_split_rules ctxt (a \$ b) = find_split_rules ctxt a @ find_split_rules ctxt b
| find_split_rules _ (Free (_, _)) = []
| find_split_rules ctxt (Const (name, _)) = split_thms ctxt name
| find_split_rules ctxt (Abs (_, _, a)) = find_split_rules ctxt a
| find_split_rules _ (Bound _) = []
| find_split_rules _ (Var _) = []

(*taken from the definition of the split tactic*)
fun gen_split_tac _ [] = K no_tac
| gen_split_tac ctxt (split::splits) =
split_tac ctxt [split] ORELSE'
gen_split_tac ctxt splits;

fun splitter ctxt i thm =
(CHANGED_PROP o gen_split_tac ctxt (@{thms if_splits} @ find_split_rules ctxt (Thm.prop_of thm))) i thm
›

method_setup mysplit = ‹
Scan.optional Attrib.thms [] >>
(fn thms => fn ctxt =>
METHOD (fn facts => REPEAT (HEADGOAL (splitter ctxt))))
› "apply splits the goal"

lemma "(case case_xs of [] ⇒ (case n of 0 ⇒ True | Suc x ⇒ True) | (x#xs) ⇒ True) = True"
apply mysplit
``````

#### Mathias Fleury (Nov 02 2020 at 17:47):

(some clean-up is required: I copy-pasted the setup for smt to define the `mysplit` tactic, but I am too lazy to do it)

#### Max W. Haslbeck (Nov 02 2020 at 17:50):

Thanks, I'll play around with that :)

Last updated: Aug 15 2022 at 02:13 UTC