Mark2 Prover Documentation

M. Randall Holmes

• Contents
• Copyright Notice
• Introduction; the Basic Session Model
• The Internal Language
  • General Syntax
    • Atomic Terms
    • Operators
    • Compound Terms
  • Navigation within Terms
  • Declarations
    • Relative Type and Stratification
    • Predicativity and Opacity
    • Refinements: Embedded Theorems and Type Retractions
    • The Definition Facility
• The Tactic Language
  • Predeclared Operators
  • Basic Semantics of Rule Infixes
  • Execution Order of the Tactic Language
  • Semantics of Alternative Rule Infixes
  • Semantics of Other Special Operators
  • Theorems with Parameters
  • Functional Programming in the Tactic Language
  • The Special Theorems RAISE and VALUE
  • The Special Theorems EVAL and BIND
  • Arithmetic Operators
  • The Special Theorems INPUT and OUTPUT
  • The Special Theorem ORDERED
  • The Hypothesis Facility
• The Proof Environment
  • Proving Theorems
    • Declaring Pretheorems
  • Applying Theorems as Rewrite Rules
  • Features of the Proof Environment
  • Starting Out
  • Simple Permutations
  • Term Display
  • Local Term Manipulation
  • Global Variable Assignment
  • Finishing Up
  • The Module System
• The Theory Environment
  • Components of the Theory Environment
  • The Syntax Lists
  • Declarations and Comments
  • Special Declarations
  • Theorems
  • Reaxiomatization and Redefinition
• The Desktop Environment
  • Loading and Saving Theories
  • Proof Environment Management
  • Theory Management
  • Views and Theorem Export
• Places where bugs are likely to be found
• Logical and Programming Style
  • Logical Style
    • The Main Points
    • The Logic of an Old Version
    • Implementation of EFT
    • The Logical Preamble
  • Programming Style
    • Basic Control Structures
    • Recursion
    • Abstraction and Reduction Algorithms
• Command Reference
  • Command Line
  • List Scanning Commands
  • Command Abbreviations
  • Desktop
  • Workspace
  • Proof Environment and Theorem
  • Theory
  • Term Syntax and Display
  • The Logic of the Definition Facility
  • List of Error Messages
• Tutorial
  • Building the Prover if You are Somewhere Else
  • The Platform
  • The Input Language
  • Navigation within Terms
  • Starting to Prove Something
  • Definitions
  • Simple Programming and Debugging
  • Appendix: Reference for Individual Commands
    • Interfaces
    • Theory Loading and Saving Commands
    • Environment Starting and other Modification Commands
    • Environment Display Commands
    • Display Control Commands
    • Movement Commands
    • Declaration Commands
    • Theorem Display Commands
    • Proof Commands
    • Editing Commands
    • Definition Commands
    • Rule Introduction Commands
    • Assignment Commands
    • Tactic Language Interpreter
    • Theory Desktop Commands
    • Environment Desktop Commands
    • View Management Commands
    • Theorem Export Commands
    • Command Abbreviations
• About this document ...