On 06/06/15 17:11, Florian Haftmann wrote:
So are there any experience reports that the combinatorial explosion in
pattern matching in fun/function had to be worked around somehow? Or do
we have to conclude that the pattern complexity of the applications in
src/HOL/Decision_Procs is indeed domain-specific?
I regularly have to work around this explosion problem. One example is in
JinjaThreads/Common/BinOp.thy where I was not able to define the function binop as a
whole, but I had to split it up into several definitions - fortunately, there was no
recursion involved, so this was possible. There must also be a mailing list thread between
Alexander Krauss and me on this topic, but I was not able to unearth it.
I have run into the same problem (with similar workarounds) a number of times. In case of
a recursive function, I nowadays write
"f x y z = (case x of ... => (case y of ... => | _ => ...) | _ => ...)"
and let simps_of_case split the equations by the pattern. In big cases, simps_of_case runs
for a minute or two, but there is no hope to get these definitions through with the
function. Of course, this does not work with overlapping patterns, but I rarely use them
anyway. The main drawback here is that I do not get a suitable cases rule for the function
definitions and the proofs accordingly look ugly (especially if I have nested patterns,
i.e., nested case distinctions and lots of rename_tac+case_tac).
Andreas
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
