Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/Isabelle/Doc/Logics_ZF/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 4 kB

Quelle ZF_Isar.thy

Sprache: Isabelle

theory ZF_Isar
imports ZF
begin

(*<*)
ML_file ‹../antiquote_setup.ML›
(*>*)

chapter ‹Some Isar language elements›

section ‹Type checking›

text ‹
The ZF logic is essentially untyped, so the concept of ``type
checking'' is performed as logical reasoning about set-membership
statements. A special method assists users in this task; a version
of this is already declared as a ``solver'' in the standard
Simplifier setup.

\begin{matharray}{rcl}
@{command_def (ZF) "print_tcset"}‹🪙*› &
    @{method_def (ZF) typecheck} & : & ‹method› java.lang.NullPointerException
    @{attribute_def (ZF) TC} & : & ‹attribute› java.lang.NullPointerException
  \end{matharray}

  🪙‹
@@{attribute (ZF) TC} (() | 'add' | 'del')
›

  \begin{description}

  \item @{command (ZF) "print_tcset"} prints the collection of
  typechecking rules of the current context.

  \item @{method (ZF) typecheck} attempts to solve any pending
  type-checking problems in subgoals.

  \item @{attribute (ZF) TC} adds or deletes type-checking rules from
  the context.

  \end{description}
›

section ‹(Co)Inductive sets and datatypes›

subsection ‹Set definitions›

text ‹
In ZF everything is a set. The generic inductive package also
provides a specific view for ``datatype'' specifications.
Coinductive definitions are available in both cases, too.

\begin{matharray}{rcl}
@{command_def (ZF) "inductive"} & : & ‹theory → theory› \
    @{command_def (ZF) "coinductive"} & : & ‹theory → theory› java.lang.NullPointerException
    @{command_def (ZF) "datatype"} & : & ‹theory → theory› java.lang.NullPointerException
    @{command_def (ZF) "codatatype"} & : & ‹theory → theory› java.lang.NullPointerException
  \end{matharray}

  🪙‹
(@@{command (ZF) inductive} | @@{command (ZF) coinductive}) domains intros hints
;

domains: @'domains' (@{syntax term} + '+') ('🚫 | '⊆') @{syntax term}
;
intros: @'intros' (@{syntax thmdecl}? @{syntax prop} +)
;
hints: @{syntax (ZF) "monos"}? condefs? 🍋
@{syntax (ZF) typeintros}? @{syntax (ZF) typeelims}?
;
@{syntax_def (ZF) "monos"}: @'monos' @{syntax thms}
;
condefs: @'con_defs' @{syntax thms}
;
@{syntax_def (ZF) typeintros}: @'type_intros' @{syntax thms}
;
@{syntax_def (ZF) typeelims}: @'type_elims' @{syntax thms}
›

  In the following syntax specification ‹monos›, ‹typeintros›, and ‹typeelims› are the same as above.

  🪙‹
(@@{command (ZF) datatype} | @@{command (ZF) codatatype}) domain? (dtspec + @'and') hints
;

domain: ('🚫 | '⊆') @{syntax term}
;
dtspec: @{syntax term} '=' (con + '|')
;
con: @{syntax name} ('(' (@{syntax term} ',' +) ')')?
;
hints: @{syntax (ZF) "monos"}? @{syntax (ZF) typeintros}? @{syntax (ZF) typeelims}?
›

  See 🍋‹"isabelle-ZF"› for further information on inductive
  definitions in ZF, but note that this covers the old-style theory
  format.
›

subsection ‹Primitive recursive functions›

text ‹
\begin{matharray}{rcl}
@{command_def (ZF) "primrec"} & : & ‹theory → theory› \
  \end{matharray}

  🪙‹
@@{command (ZF) primrec} (@{syntax thmdecl}? @{syntax prop} +)
›
›

subsection ‹Cases and induction: emulating tactic scripts›

text ‹
The following important tactical tools of Isabelle/ZF have been
ported to Isar. These should not be used in proper proof texts.

\begin{matharray}{rcl}
@{method_def (ZF) case_tac}‹🪙*› &
    @{method_def (ZF) induct_tac}‹🪙*› & : & ‹method› java.lang.NullPointerException
    @{method_def (ZF) ind_cases}‹🪙*› & : & ‹method› java.lang.NullPointerException
    @{command_def (ZF) "inductive_cases"} & : & ‹theory → theory› java.lang.NullPointerException
  \end{matharray}

  🪙‹
(@@{method (ZF) case_tac} | @@{method (ZF) induct_tac}) @{syntax goal_spec}? @{syntax name}
;
@@{method (ZF) ind_cases} (@{syntax prop} +)
;
@@{command (ZF) inductive_cases} (@{syntax thmdecl}? (@{syntax prop} +) + @'and')
›
›

end

Messung V0.5 in Prozent

¤ Dauer der Verarbeitung: 0.10 Sekunden (vorverarbeitet am 2026-05-01) ¤

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.