stringless

(in-package "STR")

(include-book "std/basic/defs" :dir :system)

(local (defthm lemma
    (implies (and (character-listp x)
        (character-listp y)
        (character-listp z)
        (string<-l x y n)
        (string<-l y z n))
      (string<-l x z n))
    :hints (("Goal" :in-theory (enable string<-l)))))

(local (defthm equal-of-char-code
    (implies (and (characterp x) (characterp y))
      (equal (equal (char-code x) (char-code y))
        (equal x y)))
    :hints (("goal" :use ((:instance code-char-char-code-is-identity
          (c x)) (:instance code-char-char-code-is-identity
           (c y)))
       :in-theory (disable code-char-char-code-is-identity)))))

(local (defthm lemma2
    (implies (and (character-listp x)
        (character-listp y)
        (character-listp z)
        (integerp n)
        (not (string<-l x y n))
        (not (string<-l y z n)))
      (not (string<-l x z n)))
    :hints (("Goal" :in-theory (enable string<-l)))))

(defthm transitivity-of-string<
  (implies (and (string< x y) (string< y z))
    (string< x z))
  :hints (("Goal" :in-theory (enable string<))))

(defthm transitivity-of-string<-negated
  (implies (and (not (string< x y))
      (not (string< y z)))
    (not (string< x z)))
  :hints (("Goal" :in-theory (enable string<))))

(defthm string<-of-str-fix-1
  (equal (string< (str-fix x) y)
    (string< x y))
  :hints (("Goal" :in-theory (enable string< str-fix))))

(defthm string<-of-str-fix-2
  (equal (string< x (str-fix y))
    (string< x y))
  :hints (("Goal" :in-theory (enable string< str-fix))))