Stream: General

Topic: split all case expressions


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

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

view this post on Zulip Max W. Haslbeck (Nov 02 2020 at 16:38):

Yes, thanks. Already doing that.

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

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

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

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

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