# [isabelle] Extreme processing time for function definition

```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"

function (sequential) 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 (Var 0))) (Eta M') =
(if 0 \<in> FV M' \<or> resid M M' = Nil then Nil else resid M M')"
| "resid (Eta M) (Lam (App M' (Var 0))) =
(if 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 (Var 0)) N) (App (Eta M') N') =
(if 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' (Var 0)) N') =
(if 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' (Var 0))) =
(if 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 (Var 0))) (Eta (Lam M')) =
(if 0 \<in> FV (Lam M') \<or> resid M M' = Nil then Nil else resid M M')"
| "resid (Lam (Beta (App M (Var 0)) (Var 0))) (Eta (Eta M')) =
(if 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' (Var 0)) (Var 0))) =
(if 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 (Var 0)) (Var 0))) (Eta (Eta M')) =
(if 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' (Var 0)) (Var 0))) =
(if 0 \<in> FV M \<or> 0 \<in> FV (Eta M) \<or> resid M M' = Nil then Nil
else resid M M')"
| "resid _  _ = Nil"
by pat_completeness auto

termination resid
by lexicographic_order

end
```

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