Parse an option
Function:
(defun parse-?%i (input) (declare (xargs :guard (nat-listp input))) (seq-backtrack input ((tree := (parse-ichar2 #\% #\i input)) (return (make-tree-nonleaf :rulename? nil :branches (list (list tree))))) ((return-raw (mv nil (make-tree-nonleaf :rulename? nil :branches nil) (nat-list-fix input))))))
Theorem:
(defthm not-of-parse-?%i.error? (b* (((mv ?error? ?tree ?rest-input) (parse-?%i input))) (not error?)) :rule-classes :rewrite)
Theorem:
(defthm treep-of-parse-?%i.tree (b* (((mv ?error? ?tree ?rest-input) (parse-?%i input))) (treep tree)) :rule-classes :rewrite)
Theorem:
(defthm nat-listp-of-parse-?%i.rest-input (b* (((mv ?error? ?tree ?rest-input) (parse-?%i input))) (nat-listp rest-input)) :rule-classes :rewrite)
Theorem:
(defthm len-of-parse-?%i-rest-linear (b* (((mv ?error? ?tree ?rest-input) (parse-?%i input))) (<= (len rest-input) (len input))) :rule-classes :linear)
Theorem:
(defthm parse-?%i-of-nat-list-fix-input (equal (parse-?%i (nat-list-fix input)) (parse-?%i input)))
Theorem:
(defthm parse-?%i-nat-list-equiv-congruence-on-input (implies (acl2::nat-list-equiv input input-equiv) (equal (parse-?%i input) (parse-?%i input-equiv))) :rule-classes :congruence)