# Re: [isabelle] Extreme processing time for function definition

Attached you find a version that works in reasonable time. I reduced the size of the patterns by replacing all "Var 0" by "vn" and testing if "vn ~= Var 0 \/ ...". This got the number of cases just below 10.000. [I believe I did not change the meaning of the equations as a result]
```
```
Note that the problem of minimizing the number of cases is hard: https://www21.in.tum.de/~krauss/publication/2008-patterns/
```
Tobias

On 07/07/2021 16:51, Eugene W. Stark wrote:
```
```The 45-line definition of function "resid" in the attached theory takes between 30 and 40 minutes
to process.  This time increased very rapidly from a previous value of about 3 minutes when I added
four clauses (the four preceding the final default clause).  The original definition was stated with
"fun" but I split it up using "function" to try to see which part was consuming the time.
About one minute is used to process the "function (sequential)" declaration, with the remainder of
the time going to the proof of 46057 subgoals "by pat_completeness auto".  The termination proof
does not take significant time.  I note that the time-consuming portion appears to be single-threaded.

Is there anything I can do, or am I out of luck?  The 30-40 minute processing time is probably
prohibitive for what I was trying to do, so it looks like I will have to abandon the generalization
I was trying to make and revert to a simpler version that processes in reasonable time.

Thanks for any suggestions.

```
```theory Barf
imports Main
begin

datatype (discs_sels) lambda =
Nil
| Var nat
| Lam lambda
| App lambda lambda
| Beta lambda lambda
| Eta lambda

fun FV
where "FV Nil = {}"
| "FV (Var i) = {i}"
| "FV (Lam M) = (\<lambda>n. n - 1) ` (FV M - {0})"
| "FV (App M N) = FV M \<union> FV N"
| "FV (Beta M N) = (\<lambda>n. n - 1) ` (FV M - {0}) \<union> FV N"
| "FV (Eta M) = (\<lambda>n. n - 1) ` (FV M - {0})"

fun Raise
where "Raise _ _ Nil = Nil"
| "Raise d n (Var i) = (if i \<ge> d then Var (i + n) else Var i)"
| "Raise d n (Lam M) = Lam (Raise (Suc d) n M)"
| "Raise d n (App M N) = App (Raise d n M) (Raise d n N)"
| "Raise d n (Beta M N) = Beta (Raise (Suc d) n M) (Raise d n N)"
| "Raise d n (Eta M) = Eta (Raise (Suc d) n M)"

abbreviation raise
where "raise == Raise 0"

fun Subst
where "Subst _ _ Nil = Nil"
| "Subst n X (Var i) = (if n < i then Var (i - 1)
else if n = i then raise n X
else Var i)"
| "Subst n X (Lam M) = Lam (Subst (Suc n) X M)"
| "Subst n X (App M N) = App (Subst n X M) (Subst n X N)"
| "Subst n X (Beta M N) = Beta (Subst (Suc n) X M) (Subst n X N)"
| "Subst n X (Eta M) = Eta (Subst (Suc n) X M)"

abbreviation subst
where "subst \<equiv> Subst 0"

fun resid
where "resid (Var i) (Var i') = (if i = i' then Var i' else Nil)"
| "resid (Lam M) (Lam M') = (if resid M M' = Nil then Nil else Lam (resid M M'))"
| "resid (App M N) (App M' N') =
(if resid M M' = Nil \<or> resid N N' = Nil then Nil
else App (resid M M') (resid N N'))"
| "resid (Beta M N) (App (Lam M') N') =
(if resid M M' = Nil \<or> resid N N' = Nil then Nil
else Beta (resid M M') (resid N N'))"
| "resid (App (Lam M) N) (Beta M' N') =
(if resid M M' = Nil \<or> resid N N' = Nil then Nil
else subst (resid N N') (resid M M'))"
| "resid (Beta M N) (Beta M' N') =
(if resid M M' = Nil \<or> resid N N' = Nil then Nil
else subst (resid N N') (resid M M'))"
| "resid (Lam (App M vn)) (Eta M') =
(if vn \<noteq> Var 0 \<or> 0 \<in> FV M' \<or> resid M M' = Nil then Nil else resid M M')"
| "resid (Eta M) (Lam (App M' vn)) =
(if vn \<noteq> Var 0 \<or> 0 \<in> FV M \<or> resid M M' = Nil then Nil else Eta (resid M M'))"
| "resid (Eta M) (Eta M') =
(if 0 \<in> FV M \<or> 0 \<in> FV M' \<or> resid M M' = Nil then Nil else resid M M')"
| "resid (Beta (App M vn) N) (App (Eta M') N') =
(if vn \<noteq> Var 0 \<or> 0 \<in> FV M' \<or> resid M M' = Nil \<or> resid N N' = Nil then Nil
else Beta (resid M M') (resid N N'))"
| "resid (App (Eta M) N) (Beta (App M' vn) N') =
(if vn \<noteq> Var 0 \<or> 0 \<in> FV M \<or> resid M M' = Nil \<or> resid N N' = Nil then Nil
else subst (resid N N') (Eta (resid M M')))"
| "resid (Eta (Lam M)) (Lam (Beta M' vn)) =
(if vn \<noteq> Var 0 \<or> 0 \<in> FV (Lam M) \<or> resid M M' = Nil then Nil
else Eta (subst (Var 0) (Lam (resid M M'))))"
| "resid (Lam (Beta M vn)) (Eta (Lam M')) =
(if vn \<noteq> Var 0 \<or> 0 \<in> FV (Lam M') \<or> resid M M' = Nil then Nil else resid M M')"
| "resid (Lam (Beta (App M vm) vn)) (Eta (Eta M')) =
(if vm \<noteq> Var 0 \<or> vn \<noteq> Var 0 \<or> 0 \<in> FV M' \<or> 0 \<in> FV (Eta M') \<or> resid M M' = Nil then Nil
else resid M M')"
| "resid (Eta (Eta M)) (Lam (Beta (App M' vm) vn)) =
(if vm \<noteq> Var 0 \<or> vn \<noteq> Var 0 \<or> 0 \<in> FV M \<or> 0 \<in> FV (Eta M) \<or> resid M M' = Nil then Nil
else Eta (resid M M'))"
| "resid (Lam (Beta (Beta M vm) vn)) (Eta (Eta M')) =
(if vm \<noteq> Var 0 \<or> vn \<noteq> Var 0 \<or> 0 \<in> FV M' \<or> 0 \<in> FV (Eta M') \<or> resid M M' = Nil then Nil
else resid M M')"
| "resid (Eta (Eta M)) (Lam (Beta (Beta M' vm) vn)) =
(if vm \<noteq> Var 0 \<or> vn \<noteq> Var 0 \<or> 0 \<in> FV M \<or> 0 \<in> FV (Eta M) \<or> resid M M' = Nil then Nil
else resid M M')"
| "resid _  _ = Nil"

end
```

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.