[isabelle] fun or function (sequential) command lasts long



HI all,

I have a problem with the following function definition:

  fun balance:: "'a tree => 'a tree" where
    "balance (T B (T R (T R a x b) y c) z d) = T R (T B a x b) y (T B c
z d)" |
    "balance (T B (T R a x (T R b y c)) z d) = T R (T B a x b) y (T B c
z d)" |
    "balance (T B a x (T R (T R b y c) z d)) = T R (T B a x b) y (T B c
z d)" |
    "balance (T B a x (T R b y (T R c z d))) = T R (T B a x b) y (T B c
z d)" |
    "balance t = t"

isabelle seems to need really long to process this command, I have
waited for several minutes and finally had to kill isabelle because it
used 1.5GB of memory and my computer started getting unusable due to
very high response times.
Is their any standard approach how speed this command up ?


Best regards,
  Peter





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