*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Extreme processing time for function definition*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Wed, 7 Jul 2021 22:02:12 +0200*Authentication-results*: cam.ac.uk; iprev=pass (mail-out2.in.tum.de) smtp.remote-ip=131.159.0.36; spf=pass smtp.mailfrom=in.tum.de; arc=none*In-reply-to*: <e1b6d191-a42c-1bf8-1739-288e6668f2d0@starkeffect.com>*References*: <e1b6d191-a42c-1bf8-1739-288e6668f2d0@starkeffect.com>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.14; rv:78.0) Gecko/20100101 Thunderbird/78.11.0

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**

**Follow-Ups**:**Re: [isabelle] Extreme processing time for function definition***From:*Eugene W. Stark

**References**:**[isabelle] Extreme processing time for function definition***From:*Eugene W. Stark

- Previous by Date: [isabelle] Extreme processing time for function definition
- Next by Date: Re: [isabelle] Extreme processing time for function definition
- Previous by Thread: [isabelle] Extreme processing time for function definition
- Next by Thread: Re: [isabelle] Extreme processing time for function definition
- Cl-isabelle-users July 2021 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list