		Search-engine friendly clone of the ACL2 documentation.

Syntax-abstraction

Abs-transition-declaration

Abstract a transition-declaration to a function declaration.

Signature
(abs-transition-declaration tree) → fundef
Arguments: tree — Guard (abnf::treep tree).
Returns: fundef — Type (fundecl-resultp fundef).

A transition is a function of sort fun-sort-transition.

Definitions and Theorems

Function: abs-transition-declaration

(defun abs-transition-declaration (tree)
 (declare (xargs :guard (abnf::treep tree)))
 (let ((__function__ 'abs-transition-declaration))
  (declare (ignorable __function__))
  (b* (((okf (abnf::tree-list-tuple10 sub))
        (abnf::check-tree-nonleaf-10 tree "transition-declaration"))
       ((okf anns) (abs-*-annotation sub.1st))
       ((okf tree)
        (abnf::check-tree-list-1 sub.2nd))
       ((okf &)
        (abnf::check-tree-schars tree "transition"))
       ((okf tree)
        (abnf::check-tree-list-1 sub.3rd))
       ((okf name) (abs-identifier tree))
       ((okf tree)
        (abnf::check-tree-list-1 sub.4th))
       ((okf &)
        (abnf::check-tree-schars tree "("))
       ((okf tree)
        (abnf::check-tree-list-1 sub.5th))
       ((okf params)
        (abs-?-function-parameters tree))
       ((okf tree)
        (abnf::check-tree-list-1 sub.6th))
       ((okf &)
        (abnf::check-tree-schars tree ")"))
       ((okf tree)
        (abnf::check-tree-list-1 sub.7th))
       ((okf &)
        (abnf::check-tree-schars tree "->"))
       ((okf tree)
        (abnf::check-tree-list-1 sub.8th))
       ((okf type) (abs-type tree))
       ((okf tree)
        (abnf::check-tree-list-1 sub.9th))
       ((okf body) (abs-block tree))
       ((okf tree)
        (abnf::check-tree-list-1 sub.10th))
       ((okf finalizer?)
        (abs-?-finalizer tree)))
    (make-fundecl :annotations anns
                  :sort (fun-sort-transition)
                  :name name
                  :inputs params
                  :output type
                  :body body
                  :finalizer finalizer?))))

Theorem: fundecl-resultp-of-abs-transition-declaration

(defthm fundecl-resultp-of-abs-transition-declaration
  (b* ((fundef (abs-transition-declaration tree)))
    (fundecl-resultp fundef))
  :rule-classes :rewrite)

Theorem: abs-transition-declaration-of-tree-fix-tree

(defthm abs-transition-declaration-of-tree-fix-tree
  (equal (abs-transition-declaration (abnf::tree-fix tree))
         (abs-transition-declaration tree)))

Theorem: abs-transition-declaration-tree-equiv-congruence-on-tree

(defthm abs-transition-declaration-tree-equiv-congruence-on-tree
  (implies (abnf::tree-equiv tree tree-equiv)
           (equal (abs-transition-declaration tree)
                  (abs-transition-declaration tree-equiv)))
  :rule-classes :congruence)