Zili Wang (Dec 04 2024 at 22:28): Zili Wang (Dec 04 2024 at 22:28):I learned about working with custom induction rules not too long ago, and was wondering if it is possible to also define custom case rules? For instance, I'm working with a formula datatype and if x is an object of this type, I can do
proof(cases x)
to have Isabelle generate all the formula shapes that x can take on. But what if I wanted to split some of the cases even finer, without having to manually do case splitting? Can I define something to do this for instance:
proof(cases x rule: custom_defined_rule)
Yes, the rule needs this shape:
(⋀x1 x2 x3. x = Case1 x1 x2 x3 ==> P) ==>
(⋀x1 x2. x = Case2 x1 x2==> P) ==> P
You can prove such a theorem and then use it just like you described earlier
Zili Wang (Dec 05 2024 at 00:20):Thank you very much!
Mathias Fleury (Dec 05 2024 at 06:10):(look at case_names to pick the name of the different cases as for example in combine_options_cases from https://isabelle.in.tum.de/library/HOL/HOL/Option.html)
Last updated: Dec 21 2024 at 16:20 UTC