[isabelle] A congruence rule proven by 'presburger'?



(This is not an April Fool's joke ...)

Dear list,

I have a weird fold combinator, let's call it "fold-left-right". Here's
its definition:

fun foldlr where
"foldlr f [] init = init" |
"foldlr f (x # xs) init = f init x (foldlr f xs)"

In order to use it in functions, I stated a congruence rule:

lemma foldlr_cong[fundef_cong]:
  assumes "init1 = init2" "xs1 = xs2"
  assumes "âacc x. x â set xs1 â f acc x = g acc x"
  shows "foldlr f xs1 init1 = foldlr g xs2 init2"

I started the proof as follows:

using assms
apply (induction f xs1 init1 arbitrary: init2 xs2 rule: foldlr.induct)
apply auto

... but got stuck and well, tried 'try0', which offered me to try
'presburger' (and nothing else!). What is it about 'presburger' that it
can solve that goal, but other provers can't?

Can anyone suggest a more elegant proof?

Cheers
Lars




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