Thanks, John! I'll read p 34 more carefully. Your example shows the behavior
I'd want from REWRITE_TAC. You theorem is
# ADD_AC;;
val it : thm =
|- m + n = n + m /\ (m + n) + p = m + n + p /\ m + n + p = n + m + p
This is a good exercise for my right associativity skill. and that's what it
takes to prove your
`(x + 1) + y + z = z + (1 + y) + x`
I'd guess that REWRITE_TAC did
(x + 1) + y + z = (y + z) + x + 1 = (z + y) + x + 1 = z + y + x + 1
= z + y + 1 + x = z + (y + 1) + x = z + (1 + y) + x
using the 1st, 3rd, 2nd, 1st, 2nd & 1st clauses of ADD_AC respectively. That's
a nice example of the power of REWRITE_TAC. But my example was quite
different, I think. REWRITE_TAC[DIST_SYM] did exactly what I wanted,
symmetrizing only the middle of three dist expressions
`∀x e x'.
dist (x,x') < e
⇒ (∃e'. &0 < e' ∧ (∀x''. dist (x'',x') < e' ⇒ dist (x,x'') < e))`
I guess I understood that REWRITE_TAC used a complicated algorithm in order to
avoid infinite looping. So I think I didn't express my question very well. I
tend to think that it's not good coding on my part to rely on features that I
don't even understand. I would think that the only sensible way to handle my
code above was to find a different way of solving the problem, such as your
solution of using ONCE_REWRITE_TAC to symmetry all three dist expressions. Any
thoughts? For instance, isn't it possible that you would change the
REWRITE_TAC algorithm?
BTW I think there isn't an pdf available for Ursula Martin and Tobias Nipkow's
paper,
http://www21.in.tum.de/~nipkow/pubs/cade90.html
But it sounds pretty complicated.
In any case, thanks, as you answered my question: this behavior of REWRITE_TAC
that I didn't understand is caused by REWRITE_TAC being quite ingenious and
complicated! That's a perfectly acceptable answer to me right now.
--
Best,
Bill
------------------------------------------------------------------------------
Android apps run on BlackBerry 10
Introducing the new BlackBerry 10.2.1 Runtime for Android apps.
Now with support for Jelly Bean, Bluetooth, Mapview and more.
Get your Android app in front of a whole new audience. Start now.
http://pubads.g.doubleclick.net/gampad/clk?id=124407151&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
