acl2-books-certs 6.3-5 / usr / share / acl2-6.3 / books / tools / flag.cert

(IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
(DEFPKG "FLAG" (SET-DIFFERENCE-EQ (UNION-EQ (QUOTE (GETPROP ACCESS DEF-BODY JUSTIFICATION CURRENT-ACL2-WORLD FORMALS RECURSIVEP DEF-BODIES MAKE-FLAG FLAG-PRESENT FLAG-FN-NAME FLAG-ALIST FLAG-DEFTHM-MACRO FLAG-EQUIVS-NAME EXPAND-CALLS-COMPUTED-HINT FIND-CALLS-OF-FNS-TERM FIND-CALLS-OF-FNS-LIST DEFXDOC DEFSECTION)) (UNION-EQ *ACL2-EXPORTS* *COMMON-LISP-SYMBOLS-FROM-MAIN-LISP-PACKAGE*)) (QUOTE (ID))))
(DEFPKG "XDOC" (SET-DIFFERENCE-EQ (UNION-EQ (UNION-EQ *ACL2-EXPORTS* *COMMON-LISP-SYMBOLS-FROM-MAIN-LISP-PACKAGE*) (QUOTE (B* QUIT EXIT VALUE DEFXDOC DEFXDOC-RAW MACRO-ARGS XDOC-EXTEND DEFSECTION DEFSECTION-PROGN CUTIL LNFIX SET-DEFAULT-PARENTS GETPROP FORMALS JUSTIFICATION DEF-BODIES CURRENT-ACL2-WORLD DEF-BODY ACCESS THEOREM UNTRANSLATED-THEOREM GUARD XDOC XDOC! UNQUOTE UNDOCUMENTED ASSERT! TOP EXPLODE IMPLODE))) (QUOTE NIL)) NIL ((:SYSTEM . "xdoc/portcullis.lisp") (:SYSTEM . "xdoc/top.lisp")) T)
:END-PORTCULLIS-CMDS
:EXPANSION-ALIST
((2 RECORD-EXPANSION (DEFXDOC MAKE-FLAG :PARENTS (MUTUAL-RECURSION) :SHORT "Create a flag-based @(see induction) scheme for a @(see
mutual-recursion)." :LONG "<p>The @('make-flag') macro lets you quickly introduce:</p>

<ul>

<li>a \"flag function\" that mimics a @(see mutual-recursion), and</li>

<li>a macro for proving properties by induction according to the flag
function.</li>

</ul>

<p>Generally speaking, writing a corresponding flag function is the first step
toward proving any inductive property about mutually recursive definitions;
more discussion below.</p>

<h3>Using @('make-flag')</h3>

<p>Example:</p>

@({
 (make-flag flag-pseudo-termp               ; flag function name
            pseudo-termp                    ; any member of the clique
            ;; optional arguments:
            :flag-mapping ((pseudo-termp      . term)
                           (pseudo-term-listp . list))
            :defthm-macro-name defthm-pseudo-termp
            :flag-var flag
            :hints ((\"Goal\" ...))         ; for the measure theorem
                                          ; usually not necessary
            )
})

<p>Here @('pseudo-termp') is the name of a function in a mutually recursive
clique.  In this case, the clique has two functions, @('pseudo-termp') and
@('pseudo-term-listp').  name of the newly generated flag function will be
@('flag-pseudo-termp').</p>

<p>The other arguments are optional:</p>

<ul>

<li>@(':flag-mapping') specifies short names to identify with each of the
functions of the clique.  By default we just use the function names themselves,
but it's usually nice to pick shorter names since you'll have to mention them
in the theorems you prove.</li>

<li>@(':defthm-macro-name') lets you name the new macro that will be generated
for proving theorems by inducting with the flag function.  By default it is
named @('defthm-[flag-function-name]'), i.e., for the above example, it would
be called @('defthm-flag-psuedo-termp').</li>

<li>@(':flag-var') specifies the name of the variable to use for the flag.  By
default it is just called @('flag'), and we rarely change it.  To be more
precise, it is @('pkg::flag') where @('pkg') is the package of the new flag
function's name; usually this means you don't have to think about the
package.</li>

</ul>


<h3>Proving Theorems with @('make-flag')</h3>

<p>To prove an inductive theorem about a mutually-recursive function, usually
one has to effectively prove a big ugly formula that has a different case for
different theorem about each function in the clique.</p>

<p>Normally, even with the flag function written for you, this would be a
tedious process.  Here is an example of how you might prove by induction that
@('pseudo-termp') and @('pseudo-term-listp') return Booleans:</p>

@({
 ;; ACL2 can prove these are Booleans even without induction due to
 ;; type reasoning, so for illustration we'll turn these off so that
 ;; induction is required:

 (in-theory (disable (:type-prescription pseudo-termp)
                     (:type-prescription pseudo-term-listp)
                     (:executable-counterpart tau-system)))

 ;; Main part of the proof, ugly lemma with cases.  Note that we
 ;; have to use :rule-classes nil here because this isn't a valid
 ;; rewrite rule.

 (local (defthm crux
          (cond ((equal flag 'term)
                 (booleanp (pseudo-termp x)))
                ((equal flag 'list)
                 (booleanp (pseudo-term-listp lst)))
                (t
                 t))
          :rule-classes nil
          :hints((\"Goal\" :induct (flag-pseudo-termp flag x lst)))))

 ;; Now we have to re-prove each part of the lemma so that we can use
 ;; it as a proper rule.

 (defthm type-of-pseudo-termp
   (booleanp (pseudo-termp x))
   :rule-classes :type-prescription
   :hints((\"Goal\" :use ((:instance crux (flag 'term))))))

 (defthm type-of-pseudo-term-listp
   (booleanp (pseudo-term-listp lst))
   :rule-classes :type-prescription
   :hints((\"Goal\" :use ((:instance crux (flag 'list))))))
})

<p>Obviously this is tedious and makes you say everything twice.  Since the
steps are so standard, @('make-flag') automatically gives you a macro to
automate the process.  Here's the same proof, done with the new macro:</p>

@({
 (defthm-pseudo-termp
   (defthm type-of-pseudo-termp
     (booleanp (pseudo-termp x))
     :rule-classes :type-prescription
     :flag term)
   (defthm type-of-pseudo-term-listp
     (booleanp (pseudo-term-listp lst))
     :rule-classes :type-prescription
     :flag list))
})

<p>It's worth understanding some of the details of what's going on here.</p>

<p>The macro automatically tries to induct using the induction scheme.  But
<color rgb=\"#ff0000\">this only works if you're using the formals of the
flag function as the variable names in the theorems.</color>  In the case of
@('pseudo-termp'), this is pretty subtle: ACL2's definition uses different
variables for the term/list cases, i.e.,</p>

@({
 (mutual-recursion
   (defun pseudo-termp (x) ...)
   (defun pseudo-term-listp (lst) ...))
})

<p>So the theorem above only works without hints because we happened to choose
@('x') and @('lst') as our variables.  If, instead, we wanted to use different
variable names in our theorems, we'd have to give an explicit induction hint.
For example:</p>

@({
 (defthm-pseudo-termp
   (defthm type-of-pseudo-termp
     (booleanp (pseudo-termp term))
     :rule-classes :type-prescription
     :flag term)
   (defthm type-of-pseudo-term-listp
     (booleanp (pseudo-term-listp termlist))
     :rule-classes :type-prescription
     :flag list)
   :hints((\"Goal\" :induct (flag-pseudo-termp flag term termlist))))
})


<h3>Bells and Whistles</h3>

<p>Sometimes you may only want to export one of the theorems.  For instance, if
we only want to add a rule about the term case, but no the list case, we could
do this:</p>

@({
 (defthm-pseudo-termp
   (defthm type-of-pseudo-termp
     (booleanp (pseudo-termp x))
     :rule-classes :type-prescription
     :flag term)
   (defthm type-of-pseudo-term-listp
     (booleanp (pseudo-term-listp lst))
     :flag list
     :skip t))
})

<p>Sometimes the theorem you want is inductive in such a way that some
functions are irrelevant; nothing needs to be proved about them in order to
prove the desired theorem about the others.  The :skip keyword can be used with
a theorem of T to do this:</p>
@({
 (defthm-pseudo-termp
   (defthm type-of-pseudo-termp
     (booleanp (pseudo-termp x))
     :rule-classes :type-prescription
     :flag term)
   (defthm type-of-pseudo-term-listp
     t
     :flag list
     :skip t))
})
<p>Alternatively, you can provide the :skip-others keyword to the top-level
macro and simply leave out the trivial parts:</p>
@({
 (defthm-pseudo-termp
   (defthm type-of-pseudo-termp
     (booleanp (pseudo-termp x))
     :rule-classes :type-prescription
     :flag term)
   :skip-others t)
})


<p>There is an older, alternate syntax for @('make-flag') that is still
available.  To encourage transitioning to the new syntax, the old syntax is not
documented and should usually not be used.</p>

<h3>Advanced Hints</h3>

<p>For advanced users, note that each individual \"theorem\" can have its own
computed hints.  For instance we can write:</p>

@({
 (defthm-pseudo-termp
   (defthm type-of-pseudo-termp
     (booleanp (pseudo-termp term))
     :rule-classes :type-prescription
     :flag term
     :hints ('(:expand ((pseudo-termp x))))
   (defthm type-of-pseudo-term-listp
     (booleanp (pseudo-term-listp termlist))
     :rule-classes :type-prescription
     :flag list
     :hints ('(:expand ((pseudo-term-listp lst)))))
   :hints((\"Goal\" :induct (flag-pseudo-termp flag term termlist))))
})

<p>These hints are used <b>during the mutually inductive proof</b>.  Under the
top-level induction, we check the clause for the current subgoal to determine
the hypothesized setting of the flag variable, and provide the computed hints
for the appropriate case.</p>

<p>If you provide both a top-level hints form and hints on some or all of the
separate theorems, both sets of hints have an effect; try @(':trans1') on such
a defthm-flag-fn form to see what you get.</p>

<p>You may use subgoal hints as well as computed hints, but they will not have
any effect if the particular subgoal does not occur when those hints are in
effect.  We simply translate subgoal hints to computed hints:</p>

@({
 (\"Subgoal *1/5.2\" :in-theory (theory 'foo))
   --->
 (and (equal id (parse-clause-id \"Subgoal *1/5.2\"))
      '(:in-theory (theory 'foo)))
})") (WITH-OUTPUT :OFF (EVENT SUMMARY) (PROGN (TABLE XDOC (QUOTE DOC) (CONS (QUOTE ((:NAME . MAKE-FLAG) (:BASE-PKG . FLAG::ACL2-PKG-WITNESS) (:PARENTS MUTUAL-RECURSION) (:SHORT . "Create a flag-based @(see induction) scheme for a @(see
mutual-recursion).") (:LONG . "<p>The @('make-flag') macro lets you quickly introduce:</p>

<ul>

<li>a \"flag function\" that mimics a @(see mutual-recursion), and</li>

<li>a macro for proving properties by induction according to the flag
function.</li>

</ul>

<p>Generally speaking, writing a corresponding flag function is the first step
toward proving any inductive property about mutually recursive definitions;
more discussion below.</p>

<h3>Using @('make-flag')</h3>

<p>Example:</p>

@({
 (make-flag flag-pseudo-termp               ; flag function name
            pseudo-termp                    ; any member of the clique
            ;; optional arguments:
            :flag-mapping ((pseudo-termp      . term)
                           (pseudo-term-listp . list))
            :defthm-macro-name defthm-pseudo-termp
            :flag-var flag
            :hints ((\"Goal\" ...))         ; for the measure theorem
                                          ; usually not necessary
            )
})

<p>Here @('pseudo-termp') is the name of a function in a mutually recursive
clique.  In this case, the clique has two functions, @('pseudo-termp') and
@('pseudo-term-listp').  name of the newly generated flag function will be
@('flag-pseudo-termp').</p>

<p>The other arguments are optional:</p>

<ul>

<li>@(':flag-mapping') specifies short names to identify with each of the
functions of the clique.  By default we just use the function names themselves,
but it's usually nice to pick shorter names since you'll have to mention them
in the theorems you prove.</li>

<li>@(':defthm-macro-name') lets you name the new macro that will be generated
for proving theorems by inducting with the flag function.  By default it is
named @('defthm-[flag-function-name]'), i.e., for the above example, it would
be called @('defthm-flag-psuedo-termp').</li>

<li>@(':flag-var') specifies the name of the variable to use for the flag.  By
default it is just called @('flag'), and we rarely change it.  To be more
precise, it is @('pkg::flag') where @('pkg') is the package of the new flag
function's name; usually this means you don't have to think about the
package.</li>

</ul>


<h3>Proving Theorems with @('make-flag')</h3>

<p>To prove an inductive theorem about a mutually-recursive function, usually
one has to effectively prove a big ugly formula that has a different case for
different theorem about each function in the clique.</p>

<p>Normally, even with the flag function written for you, this would be a
tedious process.  Here is an example of how you might prove by induction that
@('pseudo-termp') and @('pseudo-term-listp') return Booleans:</p>

@({
 ;; ACL2 can prove these are Booleans even without induction due to
 ;; type reasoning, so for illustration we'll turn these off so that
 ;; induction is required:

 (in-theory (disable (:type-prescription pseudo-termp)
                     (:type-prescription pseudo-term-listp)
                     (:executable-counterpart tau-system)))

 ;; Main part of the proof, ugly lemma with cases.  Note that we
 ;; have to use :rule-classes nil here because this isn't a valid
 ;; rewrite rule.

 (local (defthm crux
          (cond ((equal flag 'term)
                 (booleanp (pseudo-termp x)))
                ((equal flag 'list)
                 (booleanp (pseudo-term-listp lst)))
                (t
                 t))
          :rule-classes nil
          :hints((\"Goal\" :induct (flag-pseudo-termp flag x lst)))))

 ;; Now we have to re-prove each part of the lemma so that we can use
 ;; it as a proper rule.

 (defthm type-of-pseudo-termp
   (booleanp (pseudo-termp x))
   :rule-classes :type-prescription
   :hints((\"Goal\" :use ((:instance crux (flag 'term))))))

 (defthm type-of-pseudo-term-listp
   (booleanp (pseudo-term-listp lst))
   :rule-classes :type-prescription
   :hints((\"Goal\" :use ((:instance crux (flag 'list))))))
})

<p>Obviously this is tedious and makes you say everything twice.  Since the
steps are so standard, @('make-flag') automatically gives you a macro to
automate the process.  Here's the same proof, done with the new macro:</p>

@({
 (defthm-pseudo-termp
   (defthm type-of-pseudo-termp
     (booleanp (pseudo-termp x))
     :rule-classes :type-prescription
     :flag term)
   (defthm type-of-pseudo-term-listp
     (booleanp (pseudo-term-listp lst))
     :rule-classes :type-prescription
     :flag list))
})

<p>It's worth understanding some of the details of what's going on here.</p>

<p>The macro automatically tries to induct using the induction scheme.  But
<color rgb=\"#ff0000\">this only works if you're using the formals of the
flag function as the variable names in the theorems.</color>  In the case of
@('pseudo-termp'), this is pretty subtle: ACL2's definition uses different
variables for the term/list cases, i.e.,</p>

@({
 (mutual-recursion
   (defun pseudo-termp (x) ...)
   (defun pseudo-term-listp (lst) ...))
})

<p>So the theorem above only works without hints because we happened to choose
@('x') and @('lst') as our variables.  If, instead, we wanted to use different
variable names in our theorems, we'd have to give an explicit induction hint.
For example:</p>

@({
 (defthm-pseudo-termp
   (defthm type-of-pseudo-termp
     (booleanp (pseudo-termp term))
     :rule-classes :type-prescription
     :flag term)
   (defthm type-of-pseudo-term-listp
     (booleanp (pseudo-term-listp termlist))
     :rule-classes :type-prescription
     :flag list)
   :hints((\"Goal\" :induct (flag-pseudo-termp flag term termlist))))
})


<h3>Bells and Whistles</h3>

<p>Sometimes you may only want to export one of the theorems.  For instance, if
we only want to add a rule about the term case, but no the list case, we could
do this:</p>

@({
 (defthm-pseudo-termp
   (defthm type-of-pseudo-termp
     (booleanp (pseudo-termp x))
     :rule-classes :type-prescription
     :flag term)
   (defthm type-of-pseudo-term-listp
     (booleanp (pseudo-term-listp lst))
     :flag list
     :skip t))
})

<p>Sometimes the theorem you want is inductive in such a way that some
functions are irrelevant; nothing needs to be proved about them in order to
prove the desired theorem about the others.  The :skip keyword can be used with
a theorem of T to do this:</p>
@({
 (defthm-pseudo-termp
   (defthm type-of-pseudo-termp
     (booleanp (pseudo-termp x))
     :rule-classes :type-prescription
     :flag term)
   (defthm type-of-pseudo-term-listp
     t
     :flag list
     :skip t))
})
<p>Alternatively, you can provide the :skip-others keyword to the top-level
macro and simply leave out the trivial parts:</p>
@({
 (defthm-pseudo-termp
   (defthm type-of-pseudo-termp
     (booleanp (pseudo-termp x))
     :rule-classes :type-prescription
     :flag term)
   :skip-others t)
})


<p>There is an older, alternate syntax for @('make-flag') that is still
available.  To encourage transitioning to the new syntax, the old syntax is not
documented and should usually not be used.</p>

<h3>Advanced Hints</h3>

<p>For advanced users, note that each individual \"theorem\" can have its own
computed hints.  For instance we can write:</p>

@({
 (defthm-pseudo-termp
   (defthm type-of-pseudo-termp
     (booleanp (pseudo-termp term))
     :rule-classes :type-prescription
     :flag term
     :hints ('(:expand ((pseudo-termp x))))
   (defthm type-of-pseudo-term-listp
     (booleanp (pseudo-term-listp termlist))
     :rule-classes :type-prescription
     :flag list
     :hints ('(:expand ((pseudo-term-listp lst)))))
   :hints((\"Goal\" :induct (flag-pseudo-termp flag term termlist))))
})

<p>These hints are used <b>during the mutually inductive proof</b>.  Under the
top-level induction, we check the clause for the current subgoal to determine
the hypothesized setting of the flag variable, and provide the computed hints
for the appropriate case.</p>

<p>If you provide both a top-level hints form and hints on some or all of the
separate theorems, both sets of hints have an effect; try @(':trans1') on such
a defthm-flag-fn form to see what you get.</p>

<p>You may use subgoal hints as well as computed hints, but they will not have
any effect if the particular subgoal does not occur when those hints are in
effect.  We simply translate subgoal hints to computed hints:</p>

@({
 (\"Subgoal *1/5.2\" :in-theory (theory 'foo))
   --->
 (and (equal id (parse-clause-id \"Subgoal *1/5.2\"))
      '(:in-theory (theory 'foo)))
})") (:FROM . "[books]/tools/flag.lisp"))) (XDOC::GET-XDOC-TABLE WORLD))) (VALUE-TRIPLE (QUOTE (DEFXDOC MAKE-FLAG)))))) (6 RECORD-EXPANSION (DEFEVALUATOR FLAG::FLAG-IS-CP-EV FLAG::FLAG-IS-CP-EV-LST ((IF FLAG::A FLAG::B FLAG::C) (FLAG-IS FLAG::X) (NOT FLAG::X))) (PROGN (RECORD-EXPANSION (WITH-OUTPUT :OFF ERROR :STACK :PUSH (MAKE-EVENT (ER-PROGN (WITH-OUTPUT :STACK :POP (DEFEVALUATOR-CHECK (QUOTE (DEFEVALUATOR FLAG::FLAG-IS-CP-EV FLAG::FLAG-IS-CP-EV-LST ((IF FLAG::A FLAG::B FLAG::C) (FLAG-IS FLAG::X) (NOT FLAG::X)))) (QUOTE FLAG::FLAG-IS-CP-EV) (QUOTE FLAG::FLAG-IS-CP-EV-LST) (QUOTE ((IF FLAG::A FLAG::B FLAG::C) (FLAG-IS FLAG::X) (NOT FLAG::X))) (QUOTE (DEFEVALUATOR . FLAG::FLAG-IS-CP-EV)) STATE)) (VALUE (QUOTE (VALUE-TRIPLE NIL)))))) (WITH-OUTPUT :OFF ERROR :STACK :PUSH (VALUE-TRIPLE NIL))) (ENCAPSULATE (((FLAG::FLAG-IS-CP-EV * *) => *) ((FLAG::FLAG-IS-CP-EV-LST * *) => *)) (SET-INHIBIT-WARNINGS "theory") (LOCAL (IN-THEORY *DEFEVALUATOR-FORM-BASE-THEORY*)) (LOCAL (MUTUAL-RECURSION (DEFUN-NX FLAG::FLAG-IS-CP-EV (X A) (DECLARE (XARGS :VERIFY-GUARDS NIL :MEASURE (ACL2-COUNT X) :WELL-FOUNDED-RELATION O< :MODE :LOGIC)) (COND ((SYMBOLP X) (AND X (CDR (ASSOC-EQ X A)))) ((ATOM X) NIL) ((EQ (CAR X) (QUOTE QUOTE)) (CAR (CDR X))) ((CONSP (CAR X)) (FLAG::FLAG-IS-CP-EV (CAR (CDR (CDR (CAR X)))) (PAIRLIS$ (CAR (CDR (CAR X))) (FLAG::FLAG-IS-CP-EV-LST (CDR X) A)))) ((EQUAL (CAR X) (QUOTE IF)) (IF (FLAG::FLAG-IS-CP-EV (CAR (CDR X)) A) (FLAG::FLAG-IS-CP-EV (CAR (CDR (CDR X))) A) (FLAG::FLAG-IS-CP-EV (CAR (CDR (CDR (CDR X)))) A))) ((EQUAL (CAR X) (QUOTE FLAG-IS)) (FLAG-IS (FLAG::FLAG-IS-CP-EV (CAR (CDR X)) A))) ((EQUAL (CAR X) (QUOTE NOT)) (NOT (FLAG::FLAG-IS-CP-EV (CAR (CDR X)) A))) (T NIL))) (DEFUN-NX FLAG::FLAG-IS-CP-EV-LST (X-LST A) (DECLARE (XARGS :MEASURE (ACL2-COUNT X-LST) :WELL-FOUNDED-RELATION O<)) (COND ((ENDP X-LST) NIL) (T (CONS (FLAG::FLAG-IS-CP-EV (CAR X-LST) A) (FLAG::FLAG-IS-CP-EV-LST (CDR X-LST) A))))))) (LOCAL (DEFTHM EVAL-LIST-KWOTE-LST (EQUAL (FLAG::FLAG-IS-CP-EV-LST (KWOTE-LST ARGS) A) (FIX-TRUE-LIST ARGS)))) (DEFTHMD FLAG::FLAG-IS-CP-EV-CONSTRAINT-0 (IMPLIES (AND (CONSP X) (SYNTAXP (NOT (EQUAL A (QUOTE (QUOTE NIL))))) (NOT (EQUAL (CAR X) (QUOTE QUOTE)))) (EQUAL (FLAG::FLAG-IS-CP-EV X A) (FLAG::FLAG-IS-CP-EV (CONS (CAR X) (KWOTE-LST (FLAG::FLAG-IS-CP-EV-LST (CDR X) A))) NIL))) :HINTS (("Goal" :EXPAND ((:FREE (X) (HIDE X)) (FLAG::FLAG-IS-CP-EV X A)) :IN-THEORY (DISABLE (:EXECUTABLE-COUNTERPART FLAG::FLAG-IS-CP-EV))))) (DEFTHM FLAG::FLAG-IS-CP-EV-CONSTRAINT-1 (IMPLIES (SYMBOLP X) (EQUAL (FLAG::FLAG-IS-CP-EV X A) (AND X (CDR (ASSOC-EQUAL X A)))))) (DEFTHM FLAG::FLAG-IS-CP-EV-CONSTRAINT-2 (IMPLIES (AND (CONSP X) (EQUAL (CAR X) (QUOTE QUOTE))) (EQUAL (FLAG::FLAG-IS-CP-EV X A) (CADR X)))) (DEFTHM FLAG::FLAG-IS-CP-EV-CONSTRAINT-3 (IMPLIES (AND (CONSP X) (CONSP (CAR X))) (EQUAL (FLAG::FLAG-IS-CP-EV X A) (FLAG::FLAG-IS-CP-EV (CADDAR X) (PAIRLIS$ (CADAR X) (FLAG::FLAG-IS-CP-EV-LST (CDR X) A)))))) (DEFTHM FLAG::FLAG-IS-CP-EV-CONSTRAINT-4 (IMPLIES (NOT (CONSP X-LST)) (EQUAL (FLAG::FLAG-IS-CP-EV-LST X-LST A) NIL))) (DEFTHM FLAG::FLAG-IS-CP-EV-CONSTRAINT-5 (IMPLIES (CONSP X-LST) (EQUAL (FLAG::FLAG-IS-CP-EV-LST X-LST A) (CONS (FLAG::FLAG-IS-CP-EV (CAR X-LST) A) (FLAG::FLAG-IS-CP-EV-LST (CDR X-LST) A))))) (DEFTHM FLAG::FLAG-IS-CP-EV-CONSTRAINT-6 (IMPLIES (AND (CONSP X) (EQUAL (CAR X) (QUOTE IF))) (EQUAL (FLAG::FLAG-IS-CP-EV X A) (IF (FLAG::FLAG-IS-CP-EV (CADR X) A) (FLAG::FLAG-IS-CP-EV (CADDR X) A) (FLAG::FLAG-IS-CP-EV (CADDDR X) A))))) (DEFTHM FLAG::FLAG-IS-CP-EV-CONSTRAINT-7 (IMPLIES (AND (CONSP X) (EQUAL (CAR X) (QUOTE FLAG-IS))) (EQUAL (FLAG::FLAG-IS-CP-EV X A) (FLAG-IS (FLAG::FLAG-IS-CP-EV (CADR X) A))))) (DEFTHM FLAG::FLAG-IS-CP-EV-CONSTRAINT-8 (IMPLIES (AND (CONSP X) (EQUAL (CAR X) (QUOTE NOT))) (EQUAL (FLAG::FLAG-IS-CP-EV X A) (NOT (FLAG::FLAG-IS-CP-EV (CADR X) A)))))))) (53 RECORD-EXPANSION (LOCAL (ENCAPSULATE NIL (MAKE-FLAG FLAG-PSEUDO-TERMP PSEUDO-TERMP :FLAG-VAR FLAG :FLAG-MAPPING ((PSEUDO-TERMP . TERM) (PSEUDO-TERM-LISTP . LIST)) :DEFTHM-MACRO-NAME DEFTHM-PSEUDO-TERMP) (IN-THEORY (DISABLE (:TYPE-PRESCRIPTION PSEUDO-TERMP) (:TYPE-PRESCRIPTION PSEUDO-TERM-LISTP))) (ENCAPSULATE NIL (LOCAL (DEFTHM-PSEUDO-TERMP TYPE-OF-PSEUDO-TERMP (TERM (BOOLEANP (PSEUDO-TERMP X)) :RULE-CLASSES :REWRITE :DOC NIL) (LIST (BOOLEANP (PSEUDO-TERM-LISTP LST)))))) (ENCAPSULATE NIL (LOCAL (DEFTHM-PSEUDO-TERMP TYPE-OF-PSEUDO-TERMP2 (DEFTHM BOOLEANP-OF-PSEUDO-TERMP (BOOLEANP (PSEUDO-TERMP X)) :RULE-CLASSES :REWRITE :DOC NIL :FLAG TERM) :SKIP-OTHERS T))) (ENCAPSULATE NIL (LOCAL (IN-THEORY (DISABLE PSEUDO-TERMP PSEUDO-TERM-LISTP))) (LOCAL (DEFTHM-PSEUDO-TERMP TYPE-OF-PSEUDO-TERMP (TERM (BOOLEANP (PSEUDO-TERMP X)) :HINTS ((QUOTE (:EXPAND ((PSEUDO-TERMP X))))) :RULE-CLASSES :REWRITE :DOC NIL) (LIST (BOOLEANP (PSEUDO-TERM-LISTP LST)) :HINTS ((QUOTE (:EXPAND ((PSEUDO-TERM-LISTP LST))))))))) (ENCAPSULATE NIL (LOCAL (DEFTHM-PSEUDO-TERMP (TERM (BOOLEANP (PSEUDO-TERMP X)) :RULE-CLASSES :REWRITE :DOC NIL :NAME TYPE-OF-PSEUDO-TERMP) (LIST (BOOLEANP (PSEUDO-TERM-LISTP LST)) :SKIP T)))) (ENCAPSULATE NIL (LOCAL (DEFTHM-PSEUDO-TERMP (DEFTHM TYPE-OF-PSEUDO-TERMP (BOOLEANP (PSEUDO-TERMP X)) :RULE-CLASSES :REWRITE :DOC NIL :FLAG TERM) (DEFTHM TYPE-OF-PSEUDO-TERM-LISTP (BOOLEANP (PSEUDO-TERM-LISTP LST)) :FLAG LIST :SKIP T)))) (ENCAPSULATE NIL (LOCAL (DEFTHM-PSEUDO-TERMP (DEFTHM TYPE-OF-PSEUDO-TERMP (BOOLEANP (PSEUDO-TERMP X)) :RULE-CLASSES :REWRITE :DOC NIL :FLAG TERM) (LIST (BOOLEANP (PSEUDO-TERM-LISTP LST)) :SKIP T)))) (DEFSTOBJ TERM-BUCKET (TERMS)) (MUTUAL-RECURSION (DEFUN TERMS-INTO-BUCKET (X TERM-BUCKET) (DECLARE (XARGS :STOBJS (TERM-BUCKET) :VERIFY-GUARDS NIL)) (COND ((OR (ATOM X) (QUOTEP X)) (LET ((TERM-BUCKET (UPDATE-TERMS (CONS X (TERMS TERM-BUCKET)) TERM-BUCKET))) (MV 1 TERM-BUCKET))) (T (MV-LET (NUMTERMS TERM-BUCKET) (TERMS-INTO-BUCKET-LIST (CDR X) TERM-BUCKET) (LET ((TERM-BUCKET (UPDATE-TERMS (CONS X (TERMS TERM-BUCKET)) TERM-BUCKET))) (MV (+ NUMTERMS 1) TERM-BUCKET)))))) (DEFUN TERMS-INTO-BUCKET-LIST (X TERM-BUCKET) (DECLARE (XARGS :STOBJS (TERM-BUCKET))) (IF (ATOM X) (MV 0 TERM-BUCKET) (MV-LET (NUM-CAR TERM-BUCKET) (TERMS-INTO-BUCKET (CAR X) TERM-BUCKET) (MV-LET (NUM-CDR TERM-BUCKET) (TERMS-INTO-BUCKET-LIST (CDR X) TERM-BUCKET) (MV (+ NUM-CAR NUM-CDR) TERM-BUCKET)))))) (MAKE-FLAG FLAG-TERMS-INTO-BUCKET TERMS-INTO-BUCKET) (ENCAPSULATE NIL (SET-IGNORE-OK T) (MUTUAL-RECURSION (DEFUN IGNORE-TEST-F (X) (IF (CONSP X) (LET ((Y (+ X 1))) (IGNORE-TEST-G (CDR X))) NIL)) (DEFUN IGNORE-TEST-G (X) (IF (CONSP X) (IGNORE-TEST-F (CDR X)) NIL)))) (MAKE-FLAG FLAG-IGNORE-TEST IGNORE-TEST-F))) (LOCAL (VALUE-TRIPLE :ELIDED))))
NIL
(("/usr/share/acl2-6.3/books/tools/flag.lisp" "flag" "flag" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1308242620) ("/usr/share/acl2-6.3/books/xdoc/top.lisp" "xdoc/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1214825095) ("/usr/share/acl2-6.3/books/xdoc/book-thms.lisp" "book-thms" "book-thms" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1105796063) ("/usr/share/acl2-6.3/books/xdoc/base.lisp" "base" "base" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 454271148) ("/usr/share/acl2-6.3/books/xdoc/portcullis.lisp" "portcullis" "portcullis" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1473208573))
1444395294