		Search-engine friendly clone of the ACL2 documentation.

Clex

Def-sin-progress

Prove basic progress properties of a lexing function.

The macro def-sin-progress can be used to prove basic progress properties about a function that updates sin.

Typically for any function (f ... sin) --> (mv ... sin) you will want to prove:

(defthm f-progress-weak
  (<= (len (strin-left (mv-nth ... (f ... sin))))
      (len (strin-left sin)))
  :rule-classes ((:rewrite) (:linear)))

(defthm f-progress-strong
  (implies hyp
           (< (len (strin-left (mv-nth ... (f ... sin))))
              (len (strin-left sin))))
  :rule-classes ((:rewrite) (:linear)))

Where hyp is some suitable hypothesis involving the inputs and/or other values returned by the function, e.g., frequently, that F produced a token instead of failing.

(def-sin-progress name &key (hyp 't)) just tries to prove these theorems automatically about the function named name, with the given hyp. See the example-lexer for some examples of using it.