[isabelle-dev] Remaining uses of defer_recdef?

[Andreas Lochbihler]

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