[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Here's Sam Owre's response to a similar question 2 years ago. Perhaps
Sam or Shankar can comment further?
--- Forwarded mail from Sam Owre <email@example.com>
I was playing around with strings, trying to find a nice way to deal with
them, and it looks like I have a reasonably nice solution. Here is the
l1, l2: VAR list[(char?)]
f1, f2: VAR finseq[(char?)]
c1, c2: VAR (char?)
= (l1 = l2)
cons_lem: LEMMA (cons(c1,l1) = cons(c2,l2)) = (c1 = c2 & l1 = l2)
char_lem: LEMMA (c1 = c2) = (code(c1) = code(c2))
Note that the actuals need to be carefully constructed. This will
disappear in the future, but is needed for now.
To use this theory, e.g., to prove rubbish in
test : THEORY
C : string = "hello"
D : string = "hellq"
NOT C = D
You simply issue
(auto-rewrite "C" "D")
Note that you do *not* want to use grind (or auto-rewrite-defs), as this
will expand list2finseq and make the rest of the proof difficult.
Shankar and I have been talking about ways to make string handling nicer,
so this will probably be obsolete before too long, but I thought you might
be interested anyway.
---End of forwarded mail from Sam Owre <firstname.lastname@example.org>
Dave Stringer-Calvert, MEng MACM, Department of Computer Science,
University of York, Heslington, York, YO1 5DD. [+44|0] 1904 432764