		Search-engine friendly clone of the ACL2 documentation.

Semantics

Parse-treep

Recognize the parse trees of a string, with respect to a rule name and a list of rules.

Signature
(parse-treep tree 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).

Given a list of rules, a rule name, and a string, a parse tree for the string is a tree that matches the rule name (viewed as an element) and such that the string is the one at the leaves of the tree. A parse tree describes how a string is an ``instance'' of the rule name, given the rules.

Definitions and Theorems

Function: parse-treep

(defun parse-treep (tree string rulename rules)
  (declare (xargs :guard (and (stringp string)
                              (rulenamep rulename)
                              (rulelistp rules))))
  (and (treep tree)
       (tree-match-element-p tree (element-rulename rulename)
                             rules)
       (equal (tree->string tree)
              (string-fix string))))

Theorem: booleanp-of-parse-treep

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

Theorem: treep-when-parse-treep

(defthm treep-when-parse-treep
  (implies (parse-treep tree string rulename rules)
           (treep tree)))

Theorem: parse-treep-of-string-fix-string

(defthm parse-treep-of-string-fix-string
  (equal (parse-treep tree (string-fix string)
                      rulename rules)
         (parse-treep tree string rulename rules)))

Theorem: parse-treep-string-equiv-congruence-on-string

(defthm parse-treep-string-equiv-congruence-on-string
  (implies (string-equiv string string-equiv)
           (equal (parse-treep tree string rulename rules)
                  (parse-treep tree string-equiv rulename rules)))
  :rule-classes :congruence)

Theorem: parse-treep-of-rulename-fix-rulename

(defthm parse-treep-of-rulename-fix-rulename
  (equal (parse-treep tree string (rulename-fix rulename)
                      rules)
         (parse-treep tree string rulename rules)))

Theorem: parse-treep-rulename-equiv-congruence-on-rulename

(defthm parse-treep-rulename-equiv-congruence-on-rulename
  (implies (rulename-equiv rulename rulename-equiv)
           (equal (parse-treep tree string rulename rules)
                  (parse-treep tree string rulename-equiv rules)))
  :rule-classes :congruence)

Theorem: parse-treep-of-rulelist-fix-rules

(defthm parse-treep-of-rulelist-fix-rules
  (equal (parse-treep tree
                      string rulename (rulelist-fix rules))
         (parse-treep tree string rulename rules)))

Theorem: parse-treep-rulelist-equiv-congruence-on-rules

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