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.

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

Yes, thanks. Already doing that.

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

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.

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

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

Thanks, I'll play around with that :)

Last updated: Nov 11 2024 at 01:24 UTC