[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

(Fwd) Strings




Here's Sam Owre's response to a similar question 2 years ago. Perhaps
Sam or Shankar can comment further?

Dave


--- Forwarded mail from Sam Owre <owre@neon.csl.sri.com>

To: davesc@minster.cs.york.ac.uk

Dave,

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
useful theory:

string_lemmas: THEORY
 BEGIN

  l1, l2: VAR list[(char?)]

  f1, f2: VAR finseq[(char?)]

  c1, c2: VAR (char?)

  fseq_lem: LEMMA
    =[finseq[character]](list2finseq[(char?)](l1),list2finseq[(char?)](l2))
          = (l1 = l2)

  cons_lem: LEMMA (cons(c1,l1) = cons(c2,l2)) = (c1 = c2 & l1 = l2)

  char_lem: LEMMA (c1 = c2) = (code(c1) = code(c2))
 END string_lemmas

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
 BEGIN
  IMPORTING string_lemmas
  C : string = "hello"
  D : string = "hellq"

  rubbish: THEOREM
	NOT C = D

 END test

You simply issue
 (auto-rewrite-theory "string_lemmas")
 (auto-rewrite "C" "D")
 (assert)

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.

Cheers,

Sam


---End of forwarded mail from Sam Owre <owre@neon.csl.sri.com>

--
Dave Stringer-Calvert, MEng MACM,  Department of Computer Science,
University of York, Heslington, York, YO1 5DD. [+44|0] 1904 432764