		Search-engine friendly clone of the ACL2 documentation.

Def-gl-thm

Defthm-using-gl

Prove a theorem using GL, including GL only locally.

This macro generates (1) a local theorem proved via GL and (2) a non-local theorem proved trivially from the previous one. GL must be included at least locally in order for the first theorem to work, but GL may be included just locally, and the second theorem will work. This helps reduce dependencies among books.

Macro: defthm-using-gl

(defmacro defthm-using-gl
          (name &key hyp concl g-bindings rule-classes)
 (if
  (and hyp concl g-bindings)
  (let ((gl-name (add-suffix name "-GL")))
   (cons
    'progn
    (cons
     (cons
      'def-gl-ruledl
      (cons
         gl-name
         (cons ':hyp
               (cons hyp
                     (cons ':concl
                           (cons concl
                                 (cons ':g-bindings
                                       (cons g-bindings 'nil))))))))
     (cons
      (cons
       'defthm
       (cons
        name
        (cons
         (cons 'implies
               (cons hyp (cons concl 'nil)))
         (cons
          ':hints
          (cons
           (cons
            (cons
             '"Goal"
             (cons
              ':in-theory
              (cons
               '(theory 'minimal-theory)
               (cons
                   ':use
                   (cons (cons (cons ':instance (cons gl-name 'nil))
                               'nil)
                         'nil)))))
            'nil)
           (cons ':rule-classes
                 (cons (or rule-classes :rewrite)
                       'nil)))))))
      'nil))))
  nil))