		Search-engine friendly clone of the ACL2 documentation.

Term-checkers-common

Atc-check-symbol-5part

Check if a symbol consists of five parts separated by dash.

Signature
(atc-check-symbol-5part sym) → (mv yes/no part1 part2 part3 part4 part5)
Arguments: sym — Guard (symbolp sym).
Returns: yes/no — Type (booleanp yes/no).; part1 — Type (symbolp part1).; part2 — Type (symbolp part2).; part3 — Type (symbolp part3).; part4 — Type (symbolp part4).; part5 — Type (symbolp part5).

If the symbol has the form <part1>-<part2>-<part3>-<part4>-<part5>, with <part1> and <part2> and <part3> and <part4> and <part5> non-empty and without dashes, we return an indication of success and the five parts. Otherwise, we return an indication of failure and nil as the parts. The five returned symbols, when the function is successful, are interned in the same package as the input symbol.

Definitions and Theorems

Function: atc-check-symbol-5part

(defun atc-check-symbol-5part (sym)
  (declare (xargs :guard (symbolp sym)))
  (let ((__function__ 'atc-check-symbol-5part))
    (declare (ignorable __function__))
    (b* ((parts (str::strtok! (symbol-name sym)
                              (list #\-)))
         ((unless (= (len parts) 5))
          (mv nil nil nil nil nil nil))
         (part1 (intern-in-package-of-symbol (first parts)
                                             sym))
         (part2 (intern-in-package-of-symbol (second parts)
                                             sym))
         (part3 (intern-in-package-of-symbol (third parts)
                                             sym))
         (part4 (intern-in-package-of-symbol (fourth parts)
                                             sym))
         (part5 (intern-in-package-of-symbol (fifth parts)
                                             sym)))
      (mv t part1 part2 part3 part4 part5))))

Theorem: booleanp-of-atc-check-symbol-5part.yes/no

(defthm booleanp-of-atc-check-symbol-5part.yes/no
  (b* (((mv ?yes/no
            ?part1 ?part2 ?part3 ?part4 ?part5)
        (atc-check-symbol-5part sym)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: symbolp-of-atc-check-symbol-5part.part1

(defthm symbolp-of-atc-check-symbol-5part.part1
  (b* (((mv ?yes/no
            ?part1 ?part2 ?part3 ?part4 ?part5)
        (atc-check-symbol-5part sym)))
    (symbolp part1))
  :rule-classes :rewrite)

Theorem: symbolp-of-atc-check-symbol-5part.part2

(defthm symbolp-of-atc-check-symbol-5part.part2
  (b* (((mv ?yes/no
            ?part1 ?part2 ?part3 ?part4 ?part5)
        (atc-check-symbol-5part sym)))
    (symbolp part2))
  :rule-classes :rewrite)

Theorem: symbolp-of-atc-check-symbol-5part.part3

(defthm symbolp-of-atc-check-symbol-5part.part3
  (b* (((mv ?yes/no
            ?part1 ?part2 ?part3 ?part4 ?part5)
        (atc-check-symbol-5part sym)))
    (symbolp part3))
  :rule-classes :rewrite)

Theorem: symbolp-of-atc-check-symbol-5part.part4

(defthm symbolp-of-atc-check-symbol-5part.part4
  (b* (((mv ?yes/no
            ?part1 ?part2 ?part3 ?part4 ?part5)
        (atc-check-symbol-5part sym)))
    (symbolp part4))
  :rule-classes :rewrite)

Theorem: symbolp-of-atc-check-symbol-5part.part5

(defthm symbolp-of-atc-check-symbol-5part.part5
  (b* (((mv ?yes/no
            ?part1 ?part2 ?part3 ?part4 ?part5)
        (atc-check-symbol-5part sym)))
    (symbolp part5))
  :rule-classes :rewrite)