I have a function definition that is not recursive, but takes about five minutes to be processed (lose its purple background) on a relatively beefy machine. I already tried factoring it at the `Plus`

`Plus`

case. This is enough for the definition to be processed immediately, but I'd like to understand why Isabelle struggles with it so much and how in general I'd go about seeing where time is being spent. After five minutes, it also reports redundant equations and it is not clear to me why these are redundant.

Definitions:

```
datatype aexp = N int | V string | Plus aexp aexp
fun plus_full :: "aexp ⇒ aexp ⇒ aexp" where
"plus_full (N a) (N b) = N (a + b)" |
"plus_full (Plus p (N a)) (N b) = Plus p (N (a + b))" |
"plus_full (N b) (Plus p (N a)) = Plus p (N (a + b))" |
"plus_full (Plus p (N a)) (Plus q (N b)) = Plus (Plus p q) (N (a + b))" |
"plus_full (Plus p (N a)) (Plus (N b) q) = Plus (Plus p q) (N (a + b))" |
"plus_full (Plus (N a) p) (Plus (N b) q) = Plus (Plus p q) (N (a + b))" |
"plus_full (Plus (N a) p) (Plus q (N b)) = Plus (Plus p q) (N (a + b))" |
"plus_full (Plus p (N a)) q = Plus (Plus p q) (N a)" |
"plus_full q (Plus p (N a)) = Plus (Plus p q) (N a)" |
"plus_full p (N i) = (if i = 0 then p else Plus p (N i))" |
"plus_full (N i) p = (if i = 0 then p else Plus p (N i))" |
"plus_full p q = (Plus p q)"
```

Redundant equations after five minutes:

```
Ignoring duplicate rewrite rule:
plus_full (Plus (V ?vc1) (V ?vd1)) (Plus ?v1 (V ?vb1)) ≡
Plus (Plus (V ?vc1) (V ?vd1)) (Plus ?v1 (V ?vb1))
Ignoring duplicate rewrite rule:
plus_full (Plus (Plus ?vc1 ?ve1) (V ?vd1)) (Plus ?v1 (V ?vb1)) ≡
Plus (Plus (Plus ?vc1 ?ve1) (V ?vd1)) (Plus ?v1 (V ?vb1))
Ignoring duplicate rewrite rule:
plus_full (Plus (V ?vc1) (Plus ?vd1 ?ve1)) (Plus ?v1 (V ?vb1)) ≡
Plus (Plus (V ?vc1) (Plus ?vd1 ?ve1)) (Plus ?v1 (V ?vb1))
Ignoring duplicate rewrite rule:
plus_full (Plus (Plus ?vc1 ?vf1) (Plus ?vd1 ?ve1)) (Plus ?v1 (V ?vb1)) ≡
Plus (Plus (Plus ?vc1 ?vf1) (Plus ?vd1 ?ve1)) (Plus ?v1 (V ?vb1))
Ignoring duplicate rewrite rule:
plus_full (Plus ?v1 (V ?vd1)) (Plus (V ?va1) (V ?vb1)) ≡
Plus (Plus ?v1 (V ?vd1)) (Plus (V ?va1) (V ?vb1))
Ignoring duplicate rewrite rule:
plus_full (Plus ?v1 (Plus ?vd1 ?ve1)) (Plus (V ?va1) (V ?vb1)) ≡
Plus (Plus ?v1 (Plus ?vd1 ?ve1)) (Plus (V ?va1) (V ?vb1))
```

Thanks in advance for the help!

Internally the function packages deduplicates patterns (like `plus_full (N i) p`

and `plus p q`

are duplicates) to generate the right definitions and simplification rules.

The easiest solution in your case is to do the case distinction using `case ... of .. \<Rightarrow> ...`

@Mathias Fleury aha, thanks! That explains the redundant equations and it makes sense. It is unfortunate that the definition of the function package leaks its implementation in that way. I might go as far as to say that it is a bug.

Is that also somehow related to the definition taking a long time to be processed?

You really need to do the disambiguation of the patterns, so not really a bug. Imagine that you would not do that and simply take the rules as simp rules. Then you could define the following:

```
fun f where
"f 0 = 0"
"f _ = 1"
```

Without further work on the equations, both can be applied to `f n `

but you get different results depending on which equation you use, which is obviously wrong.

Anyway the disambiguation is the reason why the definitions takes such a long time.

I guess I have the wrong mindset. I figured the second equation on `f`

would implicitly be on `Suc n`

due to the existence of the first equation. I guess such fall through reasoning is not appropriate in Isabelle? Is that right? If that's the case, I'd have expected your definition of `f`

to be rejected due to patterns not being orthogonal.

Yeah indeed the second pattern becomes Suc:

```
fun f :: ‹nat ⇒ nat› where
"f 0 = 0" |
"f _ = 1"
thm f.simps
(* f 0 = 0
f (Suc ?v) = 1*)
```

My point is that this transformation from `f _ = 1`

to `f (Suc _) = 1`

becomes slow if you have too many patterns

(but it will eventually succeed as your large example illustrates)

Perfect, I think I understand now. Thanks a lot for your explanations!

Maybe at some point there will be someone who is motivated enough to investigate whether the disambiguation can be sped up :)

If I recall correctly, if you use `function`

instead of `fun`

, you can have overlapping patterns and will be required to prove that whenever you have an overlap, you have the same result on the right-hand side. Unfortunately, you will be unable to do so when recursion is involved, so it is not too helpful in practice.

Last updated: Sep 22 2023 at 08:19 UTC