		Search-engine friendly clone of the ACL2 documentation.

Semantics

String-unambiguousp

Notion of unambiguous string.

Signature
(string-unambiguousp string rulename rules) → yes/no
Arguments: string — Guard (stringp string).; rulename — Guard (rulenamep rulename).; rules — Guard (rulelistp rules).
Returns: yes/no — Type (booleanp yes/no).

A string is unambiguous iff it has exactly one parse tree.

Definitions and Theorems

Function: string-unambiguousp

(defun string-unambiguousp (string rulename rules)
  (declare (xargs :guard (and (stringp string)
                              (rulenamep rulename)
                              (rulelistp rules))))
  (and (string-parsablep string rulename rules)
       (not (string-ambiguousp string rulename rules))))

Theorem: booleanp-of-string-unambiguousp

(defthm booleanp-of-string-unambiguousp
  (b* ((yes/no (string-unambiguousp string rulename rules)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: parse-treep-when-string-unambiguousp

(defthm parse-treep-when-string-unambiguousp
 (implies
  (string-unambiguousp string rulename rules)
  (equal (parse-treep tree string rulename rules)
         (equal tree
                (string-parsablep-witness string rulename rules)))))

Theorem: treep-of-string-parsablep-witness-when-string-unambiguousp

(defthm treep-of-string-parsablep-witness-when-string-unambiguousp
 (implies (string-unambiguousp string rulename rules)
          (treep (string-parsablep-witness string rulename rules))))

Theorem: string-unambiguousp-of-string-fix-string

(defthm string-unambiguousp-of-string-fix-string
  (equal (string-unambiguousp (string-fix string)
                              rulename rules)
         (string-unambiguousp string rulename rules)))

Theorem: string-unambiguousp-string-equiv-congruence-on-string

(defthm string-unambiguousp-string-equiv-congruence-on-string
 (implies (string-equiv string string-equiv)
          (equal (string-unambiguousp string rulename rules)
                 (string-unambiguousp string-equiv rulename rules)))
 :rule-classes :congruence)

Theorem: string-unambiguousp-of-rulename-fix-rulename

(defthm string-unambiguousp-of-rulename-fix-rulename
  (equal (string-unambiguousp string (rulename-fix rulename)
                              rules)
         (string-unambiguousp string rulename rules)))

Theorem: string-unambiguousp-rulename-equiv-congruence-on-rulename

(defthm string-unambiguousp-rulename-equiv-congruence-on-rulename
 (implies (rulename-equiv rulename rulename-equiv)
          (equal (string-unambiguousp string rulename rules)
                 (string-unambiguousp string rulename-equiv rules)))
 :rule-classes :congruence)

Theorem: string-unambiguousp-of-rulelist-fix-rules

(defthm string-unambiguousp-of-rulelist-fix-rules
  (equal (string-unambiguousp string rulename (rulelist-fix rules))
         (string-unambiguousp string rulename rules)))

Theorem: string-unambiguousp-rulelist-equiv-congruence-on-rules

(defthm string-unambiguousp-rulelist-equiv-congruence-on-rules
 (implies (rulelist-equiv rules rules-equiv)
          (equal (string-unambiguousp string rulename rules)
                 (string-unambiguousp string rulename rules-equiv)))
 :rule-classes :congruence)