*To*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*Subject*: [isabelle] Extreme processing time for function definition*From*: "Eugene W. Stark" <isabelle-users at starkeffect.com>*Date*: Wed, 7 Jul 2021 10:51:36 -0400*Authentication-results*: cam.ac.uk; iprev=pass (cloud2.starkeffect.com) smtp.remote-ip=45.55.83.152; spf=pass smtp.mailfrom=starkeffect.com; arc=none*Reply-to*: stark at cs.stonybrook.edu*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:78.0) Gecko/20100101 Thunderbird/78.8.1

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

**Follow-Ups**:**Re: [isabelle] Extreme processing time for function definition***From:*Tobias Nipkow

- Previous by Date: Re: [isabelle] Printing a term without abbreviations/notation
- Next by Date: Re: [isabelle] Extreme processing time for function definition
- Previous by Thread: Re: [isabelle] Printing a term without abbreviations/notation
- 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