Quelle Preface.thy

Sprache: Isabelle

(*:maxLineLen=78:*)

theory Preface
imports Main Base
begin

text ‹
The 🪙‹Isabelle› system essentially provides a generic
infrastructure for building deductive systems (programmed in
Standard ML), with a special focus on interactive theorem proving in
higher-order logics. Many years ago, even end-users would refer to
certain ML functions (goal commands, tactics, tacticals etc.) to
pursue their everyday theorem proving tasks.

In contrast 🪙‹Isar› provides an interpreted language environment
of its own, which has been specifically tailored for the needs of
theory and proof development. Compared to raw ML, the Isabelle/Isar
top-level provides a more robust and comfortable development
platform, with proper support for theory development graphs, managed
transactions with unlimited undo etc.

In its pioneering times, the Isabelle/Isar version of the
🪙‹Proof~General› user interface cite‹proofgeneral and
"Aspinall:TACAS:2000"› has contributed to the
success of for interactive theory and proof development in this
advanced theorem proving environment, even though it was somewhat
biased towards old-style proof scripts. The more recent
Isabelle/jEdit Prover IDE cite‹"Wenzel:2012"› emphasizes the
document-oriented approach of Isabelle/Isar again more explicitly.

🪙
Apart from the technical advances over bare-bones ML
programming, the main purpose of the Isar language is to provide a
conceptually different view on machine-checked proofs
cite‹"Wenzel:1999:TPHOL" and "Wenzel-PhD"›. 🪙‹Isar› stands for
🪙‹Intelligible semi-automated reasoning›. Drawing from both the
traditions of informal mathematical proof texts and high-level
programming languages, Isar offers a versatile environment for
structured formal proof documents. Thus properly written Isar
proofs become accessible to a broader audience than unstructured
tactic scripts (which typically only provide operational information
for the machine). Writing human-readable proof texts certainly
requires some additional efforts by the writer to achieve a good
presentation, both of formal and informal parts of the text. On the
other hand, human-readable formal texts gain some value in their own
right, independently of the mechanic proof-checking process.

Despite its grand design of structured proof texts, Isar is able to
assimilate the old tactical style as an ``improper'' sub-language.
This provides an easy upgrade path for existing tactic scripts, as
well as some means for interactive experimentation and debugging of
structured proofs. Isabelle/Isar supports a broad range of proof
styles, both readable and unreadable ones.

🪙
The generic Isabelle/Isar framework (see
\chref{ch:isar-framework}) works reasonably well for any Isabelle
object-logic that conforms to the natural deduction view of the
Isabelle/Pure framework. Specific language elements introduced by
Isabelle/HOL are described in \partref{part:hol}. Although the main
language elements are already provided by the Isabelle/Pure
framework, examples given in the generic parts will usually refer to
Isabelle/HOL.

🪙
Isar commands may be either 🪙‹proper› document
constructors, or 🪙‹improper commands›. Some proof methods and
attributes introduced later are classified as improper as well.
Improper Isar language elements, which are marked by ``‹^*›'' in the subsequent chapters; they are often helpful
when developing proof documents, but their use is discouraged for
the final human-readable outcome. Typical examples are diagnostic
commands that print terms or theorems according to the current
context; other commands emulate old-style tactical theorem proving.
›

end

Messung V0.5 in Prozent

¤ Dauer der Verarbeitung: 0.9 Sekunden (vorverarbeitet am 2026-06-10) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.