Theory ZF_Isar

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"}‹⇧*› & : & ‹context →› \\
    @{method_def (ZF) typecheck} & : & ‹method› \\
    @{attribute_def (ZF) TC} & : & ‹attribute› \\
  \end{matharray}

  \<^rail>‹
    @@{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› \\
    @{command_def (ZF) "datatype"} & : & ‹theory → theory› \\
    @{command_def (ZF) "codatatype"} & : & ‹theory → theory› \\
  \end{matharray}

  \<^rail>‹
    (@@{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.

  \<^rail>‹
    (@@{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 \<^cite>‹"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}

  \<^rail>‹
    @@{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› \\
    @{method_def (ZF) induct_tac}‹⇧*› & : & ‹method› \\
    @{method_def (ZF) ind_cases}‹⇧*› & : & ‹method› \\
    @{command_def (ZF) "inductive_cases"} & : & ‹theory → theory› \\
  \end{matharray}

  \<^rail>‹
    (@@{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