• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Recursion-and-induction
    • Hons-and-memoization
    • Events
    • Parallelism
    • History
    • Programming
    • Operational-semantics
    • Real
    • Start-here
      • Gentle-introduction-to-ACL2-programming
      • ACL2-tutorial
        • Introduction-to-the-theorem-prover
        • Pages Written Especially for the Tours
          • A Tiny Warning Sign
          • About the Prompt
          • ACL2 Symbols
          • Common Lisp
          • About Types
          • The Event Summary
          • Tours
          • An Example of ACL2 in Use
          • Corroborating Models
          • The Proof of the Associativity of App
          • Guards in ACL2
          • Numbers in ACL2
          • About the Admission of Recursive Definitions
          • Free Variables in Top-Level Input
          • Common Lisp as a Modeling Language
          • ACL2 as an Interactive Theorem Prover (cont)
          • A Flying Tour of ACL2
          • Analyzing Common Lisp Models
          • A Walking Tour of ACL2
          • About the ACL2 Home Page
          • The Theorem that App is Associative
          • The End of the Walking Tour
          • Proving Theorems about Models
          • Functions for Manipulating these Objects
          • ACL2 Conses or Ordered Pairs
          • The Associativity of App
          • Models of Computer Hardware and Software
          • How To Find Out about ACL2 Functions (cont)
          • A Sketch of How the Rewriter Works
          • ACL2 System Architecture
          • Running Models
          • ACL2 is an Untyped Language
          • How To Find Out about ACL2 Functions
          • How Long Does It Take to Become an Effective User(Q)
          • The Admission of App
          • Guiding the ACL2 Theorem Prover
          • What Is ACL2(Q)
          • Conversion
          • An Example Common Lisp Function Definition
          • ACL2 Characters
          • You Must Think about the Use of a Formula as a Rule
          • The WARNING about the Trivial Consequence
          • Guessing the Type of a Newly Admitted Function
          • ACL2 Strings
          • What is a Mathematical Logic(Q)
          • Revisiting the Admission of App
          • What is a Mechanical Theorem Prover(Q)
          • About Models
          • What is Required of the User(Q)
          • Hey Wait! Is ACL2 Typed or Untyped(Q)
          • The Falling Body Model
          • Rewrite Rules are Generated from DEFTHM Events
          • Other Requirements
          • A Typical State
          • The Time Taken to do the Associativity of App Proof
          • The Simplification of the Induction Conclusion (Step 1)
          • The Rules used in the Associativity of App Proof
          • Subsumption of Induction Candidates in App Example
          • Models in Engineering
          • Symbolic Execution of Models
          • Suggested Inductions in the Associativity of App Example
          • Overview of the Proof of a Trivial Consequence
          • Evaluating App on Sample Input
          • The Induction Step in the App Example
          • Modeling in ACL2
          • The Simplification of the Induction Conclusion (Step 9)
          • The Induction Scheme Selected for the App Example
          • The First Application of the Associativity Rule
          • Overview of the Expansion of ENDP in the Induction Step
          • Flawed Induction Candidates in App Example
          • ACL2 as an Interactive Theorem Prover
          • Using the Associativity of App to Prove a Trivial Consequence
          • The Simplification of the Induction Conclusion (Step 8)
          • The Instantiation of the Induction Scheme
          • The Final Simplification in the Base Case (Step 0)
          • Overview of the Simplification of the Induction Step to T
          • Overview of the Simplification of the Induction Conclusion
          • On the Naming of Subgoals
          • Nontautological Subgoals
          • What is a Mechanical Theorem Prover(Q) (cont)
          • The Simplification of the Induction Conclusion (Step 12)
          • The Simplification of the Induction Conclusion (Step 10)
          • The End of the Flying Tour
          • The Base Case in the App Example
          • The Simplification of the Induction Conclusion (Step 11)
          • The Final Simplification in the Base Case (Step 3)
          • The Expansion of ENDP in the Induction Step (Step 1)
          • The Expansion of ENDP in the Induction Step (Step 0)
          • The End of the Proof of the Associativity of App
          • Overview of the Simplification of the Base Case to T
          • The Summary of the Proof of the Trivial Consequence
          • The Simplification of the Induction Conclusion (Step 7)
          • The Simplification of the Induction Conclusion (Step 6)
          • The Simplification of the Induction Conclusion (Step 5)
          • The Simplification of the Induction Conclusion (Step 4)
          • The Simplification of the Induction Conclusion (Step 2)
          • The Simplification of the Induction Conclusion (Step 0)
          • The Justification of the Induction Scheme
          • The Final Simplification in the Base Case (Step 1)
          • The Expansion of ENDP in the Induction Step (Step 2)
          • Popping out of an Inductive Proof
          • Overview of the Expansion of ENDP in the Base Case
          • The Simplification of the Induction Conclusion (Step 3)
          • The Q.E.D. Message
          • Overview of the Final Simplification in the Base Case
          • The Final Simplification in the Base Case (Step 2)
          • Perhaps
          • Name the Formula Above
          • A Trivial Proof
        • The-method
        • Advanced-features
        • Interesting-applications
        • Tips
        • Alternative-introduction
        • Tidbits
        • Annotated-ACL2-scripts
        • Startup
        • ACL2-as-standalone-program
        • ACL2-sedan
        • Talks
        • Nqthm-to-ACL2
        • Tours
        • Emacs
      • About-ACL2
        • Recursion-and-induction
        • Operational-semantics
        • Soundness
        • Release-notes
        • Workshops
        • ACL2-tutorial
          • Introduction-to-the-theorem-prover
          • Pages Written Especially for the Tours
            • A Tiny Warning Sign
            • About the Prompt
            • ACL2 Symbols
            • Common Lisp
            • About Types
            • The Event Summary
            • Tours
            • An Example of ACL2 in Use
            • Corroborating Models
            • The Proof of the Associativity of App
            • Guards in ACL2
            • Numbers in ACL2
            • About the Admission of Recursive Definitions
            • Free Variables in Top-Level Input
            • Common Lisp as a Modeling Language
            • ACL2 as an Interactive Theorem Prover (cont)
            • A Flying Tour of ACL2
            • Analyzing Common Lisp Models
            • A Walking Tour of ACL2
            • About the ACL2 Home Page
            • The Theorem that App is Associative
            • The End of the Walking Tour
            • Proving Theorems about Models
            • Functions for Manipulating these Objects
            • ACL2 Conses or Ordered Pairs
            • The Associativity of App
            • Models of Computer Hardware and Software
            • How To Find Out about ACL2 Functions (cont)
            • A Sketch of How the Rewriter Works
            • ACL2 System Architecture
            • Running Models
            • ACL2 is an Untyped Language
            • How To Find Out about ACL2 Functions
            • How Long Does It Take to Become an Effective User(Q)
            • The Admission of App
            • Guiding the ACL2 Theorem Prover
            • What Is ACL2(Q)
            • Conversion
            • An Example Common Lisp Function Definition
            • ACL2 Characters
            • You Must Think about the Use of a Formula as a Rule
            • The WARNING about the Trivial Consequence
            • Guessing the Type of a Newly Admitted Function
            • ACL2 Strings
            • What is a Mathematical Logic(Q)
            • Revisiting the Admission of App
            • What is a Mechanical Theorem Prover(Q)
            • About Models
            • What is Required of the User(Q)
            • Hey Wait! Is ACL2 Typed or Untyped(Q)
            • The Falling Body Model
            • Rewrite Rules are Generated from DEFTHM Events
            • Other Requirements
            • A Typical State
            • The Time Taken to do the Associativity of App Proof
            • The Simplification of the Induction Conclusion (Step 1)
            • The Rules used in the Associativity of App Proof
            • Subsumption of Induction Candidates in App Example
            • Models in Engineering
            • Symbolic Execution of Models
            • Suggested Inductions in the Associativity of App Example
            • Overview of the Proof of a Trivial Consequence
            • Evaluating App on Sample Input
            • The Induction Step in the App Example
            • Modeling in ACL2
            • The Simplification of the Induction Conclusion (Step 9)
            • The Induction Scheme Selected for the App Example
            • The First Application of the Associativity Rule
            • Overview of the Expansion of ENDP in the Induction Step
            • Flawed Induction Candidates in App Example
            • ACL2 as an Interactive Theorem Prover
            • Using the Associativity of App to Prove a Trivial Consequence
            • The Simplification of the Induction Conclusion (Step 8)
            • The Instantiation of the Induction Scheme
            • The Final Simplification in the Base Case (Step 0)
            • Overview of the Simplification of the Induction Step to T
            • Overview of the Simplification of the Induction Conclusion
            • On the Naming of Subgoals
            • Nontautological Subgoals
            • What is a Mechanical Theorem Prover(Q) (cont)
            • The Simplification of the Induction Conclusion (Step 12)
            • The Simplification of the Induction Conclusion (Step 10)
            • The End of the Flying Tour
            • The Base Case in the App Example
            • The Simplification of the Induction Conclusion (Step 11)
            • The Final Simplification in the Base Case (Step 3)
            • The Expansion of ENDP in the Induction Step (Step 1)
            • The Expansion of ENDP in the Induction Step (Step 0)
            • The End of the Proof of the Associativity of App
            • Overview of the Simplification of the Base Case to T
            • The Summary of the Proof of the Trivial Consequence
            • The Simplification of the Induction Conclusion (Step 7)
            • The Simplification of the Induction Conclusion (Step 6)
            • The Simplification of the Induction Conclusion (Step 5)
            • The Simplification of the Induction Conclusion (Step 4)
            • The Simplification of the Induction Conclusion (Step 2)
            • The Simplification of the Induction Conclusion (Step 0)
            • The Justification of the Induction Scheme
            • The Final Simplification in the Base Case (Step 1)
            • The Expansion of ENDP in the Induction Step (Step 2)
            • Popping out of an Inductive Proof
            • Overview of the Expansion of ENDP in the Base Case
            • The Simplification of the Induction Conclusion (Step 3)
            • The Q.E.D. Message
            • Overview of the Final Simplification in the Base Case
            • The Final Simplification in the Base Case (Step 2)
            • Perhaps
            • Name the Formula Above
            • A Trivial Proof
          • The-method
          • Advanced-features
          • Interesting-applications
          • Tips
          • Alternative-introduction
          • Tidbits
          • Annotated-ACL2-scripts
          • Startup
          • ACL2-as-standalone-program
          • ACL2-sedan
          • Talks
          • Nqthm-to-ACL2
          • Tours
          • Emacs
        • Version
        • How-to-contribute
        • Acknowledgments
        • Using-ACL2
        • Releases
        • Pre-built-binary-distributions
        • Common-lisp
        • Installation
        • Mailing-lists
        • Git-quick-start
        • Copyright
        • ACL2-help
    • Miscellaneous
    • Output-controls
    • Bdd
    • Macros
    • Installation
    • Mailing-lists
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Pages Written Especially for the Tours

Functions for Manipulating these Objects

Functions for Manipulating these Objects

Consider a typical ``stack'' of control frames.

Suppose the model required that we express the idea of ``the most recent frame whose return program counter points into MAIN.''

The natural expression of this notion involves

function application — ``fetch the return-pc of this frame''

case analysis — ``if the pc is MAIN, then ...''

iteration or recursion — ``pop this frame off and repeat.''

The designers of ACL2 have taken the position that a programming language is the natural language in which to define such notions, provided the language has a mathematical foundation so that models can be analyzed and properties derived logically.

Common Lisp is the language supported by ACL2. To be precise, a small applicative subset of Common Lisp is the language supported by ACL2.