[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.