Max W. Haslbeck (Nov 02 2020 at 16:01): 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
Yes, thanks. Already doing that.
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
(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: Apr 20 2024 at 12:26 UTC