		Search-engine friendly clone of the ACL2 documentation.

Atj-types

Atj-type-to-pred

ACL2 predicate denoted by an ATJ type.

Signature
(atj-type-to-pred type) → pred
Arguments: type — Guard (atj-typep type).
Returns: pred — Type (pseudo-termfnp pred).

The predicate recognizes the values of the type.

The predicates for the :acl2 types are straightforward. The predicates for the :jprim types are the recognizers of the corresponding Java primitive values in our Java language formalization. The predicates for the :jprimarr types are the recognizers of the corresponding Java primitive arrays in our ATJ's model of primitive arrays. Also see here and here.

Definitions and Theorems

Function: atj-type-to-pred

(defun atj-type-to-pred (type)
  (declare (xargs :guard (atj-typep type)))
  (let ((__function__ 'atj-type-to-pred))
    (declare (ignorable __function__))
    (atj-type-case
         type
         :acl2 (atj-atype-case type.get
                               :integer 'integerp
                               :rational 'rationalp
                               :number 'acl2-numberp
                               :character 'characterp
                               :string 'stringp
                               :symbol 'symbolp
                               :boolean 'booleanp
                               :cons 'consp
                               :value '(lambda (_) 't))
         :jprim (primitive-type-case type.get
                                     :boolean 'boolean-valuep
                                     :char 'char-valuep
                                     :byte 'byte-valuep
                                     :short 'short-valuep
                                     :int 'int-valuep
                                     :long 'long-valuep
                                     :float 'float-valuep
                                     :double 'double-valuep)
         :jprimarr (primitive-type-case type.comp
                                        :boolean 'boolean-arrayp
                                        :char 'char-arrayp
                                        :byte 'byte-arrayp
                                        :short 'short-arrayp
                                        :int 'int-arrayp
                                        :long 'long-arrayp
                                        :float 'float-arrayp
                                        :double 'double-arrayp))))

Theorem: pseudo-termfnp-of-atj-type-to-pred

(defthm pseudo-termfnp-of-atj-type-to-pred
  (b* ((pred (atj-type-to-pred type)))
    (pseudo-termfnp pred))
  :rule-classes :rewrite)

Theorem: atj-type-to-pred-of-atj-type-fix-type

(defthm atj-type-to-pred-of-atj-type-fix-type
  (equal (atj-type-to-pred (atj-type-fix type))
         (atj-type-to-pred type)))

Theorem: atj-type-to-pred-atj-type-equiv-congruence-on-type

(defthm atj-type-to-pred-atj-type-equiv-congruence-on-type
  (implies (atj-type-equiv type type-equiv)
           (equal (atj-type-to-pred type)
                  (atj-type-to-pred type-equiv)))
  :rule-classes :congruence)