[isabelle] A congruence rule proven by 'presburger'?
(This is not an April Fool's joke ...)
I have a weird fold combinator, let's call it "fold-left-right". Here's
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:
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:
apply (induction f xs1 init1 arbitrary: init2 xs2 rule: foldlr.induct)
... 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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and