src/Doc/Logics_ZF/ZF_Isar.thy
author haftmann
Sun Oct 08 22:28:22 2017 +0200 (23 months ago)
changeset 66816 212a3334e7da
parent 65449 c82e63b11b8b
child 67406 23307fd33906
permissions -rw-r--r--
more fundamental definition of div and mod on int
     1 theory ZF_Isar
     2 imports ZF
     3 begin
     4 
     5 (*<*)
     6 ML_file "../antiquote_setup.ML"
     7 (*>*)
     8 
     9 chapter {* Some Isar language elements *}
    10 
    11 section {* Type checking *}
    12 
    13 text {*
    14   The ZF logic is essentially untyped, so the concept of ``type
    15   checking'' is performed as logical reasoning about set-membership
    16   statements.  A special method assists users in this task; a version
    17   of this is already declared as a ``solver'' in the standard
    18   Simplifier setup.
    19 
    20   \begin{matharray}{rcl}
    21     @{command_def (ZF) "print_tcset"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
    22     @{method_def (ZF) typecheck} & : & @{text method} \\
    23     @{attribute_def (ZF) TC} & : & @{text attribute} \\
    24   \end{matharray}
    25 
    26   @{rail \<open>
    27     @@{attribute (ZF) TC} (() | 'add' | 'del')
    28   \<close>}
    29 
    30   \begin{description}
    31   
    32   \item @{command (ZF) "print_tcset"} prints the collection of
    33   typechecking rules of the current context.
    34   
    35   \item @{method (ZF) typecheck} attempts to solve any pending
    36   type-checking problems in subgoals.
    37   
    38   \item @{attribute (ZF) TC} adds or deletes type-checking rules from
    39   the context.
    40 
    41   \end{description}
    42 *}
    43 
    44 
    45 section {* (Co)Inductive sets and datatypes *}
    46 
    47 subsection {* Set definitions *}
    48 
    49 text {*
    50   In ZF everything is a set.  The generic inductive package also
    51   provides a specific view for ``datatype'' specifications.
    52   Coinductive definitions are available in both cases, too.
    53 
    54   \begin{matharray}{rcl}
    55     @{command_def (ZF) "inductive"} & : & @{text "theory \<rightarrow> theory"} \\
    56     @{command_def (ZF) "coinductive"} & : & @{text "theory \<rightarrow> theory"} \\
    57     @{command_def (ZF) "datatype"} & : & @{text "theory \<rightarrow> theory"} \\
    58     @{command_def (ZF) "codatatype"} & : & @{text "theory \<rightarrow> theory"} \\
    59   \end{matharray}
    60 
    61   @{rail \<open>
    62     (@@{command (ZF) inductive} | @@{command (ZF) coinductive}) domains intros hints
    63     ;
    64 
    65     domains: @'domains' (@{syntax term} + '+') ('<=' | '\<subseteq>') @{syntax term}
    66     ;
    67     intros: @'intros' (@{syntax thmdecl}? @{syntax prop} +)
    68     ;
    69     hints: @{syntax (ZF) "monos"}? condefs? \<newline>
    70       @{syntax (ZF) typeintros}? @{syntax (ZF) typeelims}?
    71     ;
    72     @{syntax_def (ZF) "monos"}: @'monos' @{syntax thms}
    73     ;
    74     condefs: @'con_defs' @{syntax thms}
    75     ;
    76     @{syntax_def (ZF) typeintros}: @'type_intros' @{syntax thms}
    77     ;
    78     @{syntax_def (ZF) typeelims}: @'type_elims' @{syntax thms}
    79   \<close>}
    80 
    81   In the following syntax specification @{text "monos"}, @{text
    82   typeintros}, and @{text typeelims} are the same as above.
    83 
    84   @{rail \<open>
    85     (@@{command (ZF) datatype} | @@{command (ZF) codatatype}) domain? (dtspec + @'and') hints
    86     ;
    87 
    88     domain: ('<=' | '\<subseteq>') @{syntax term}
    89     ;
    90     dtspec: @{syntax term} '=' (con + '|')
    91     ;
    92     con: @{syntax name} ('(' (@{syntax term} ',' +) ')')?
    93     ;
    94     hints: @{syntax (ZF) "monos"}? @{syntax (ZF) typeintros}? @{syntax (ZF) typeelims}?
    95   \<close>}
    96 
    97   See @{cite "isabelle-ZF"} for further information on inductive
    98   definitions in ZF, but note that this covers the old-style theory
    99   format.
   100 *}
   101 
   102 
   103 subsection {* Primitive recursive functions *}
   104 
   105 text {*
   106   \begin{matharray}{rcl}
   107     @{command_def (ZF) "primrec"} & : & @{text "theory \<rightarrow> theory"} \\
   108   \end{matharray}
   109 
   110   @{rail \<open>
   111     @@{command (ZF) primrec} (@{syntax thmdecl}? @{syntax prop} +)
   112   \<close>}
   113 *}
   114 
   115 
   116 subsection {* Cases and induction: emulating tactic scripts *}
   117 
   118 text {*
   119   The following important tactical tools of Isabelle/ZF have been
   120   ported to Isar.  These should not be used in proper proof texts.
   121 
   122   \begin{matharray}{rcl}
   123     @{method_def (ZF) case_tac}@{text "\<^sup>*"} & : & @{text method} \\
   124     @{method_def (ZF) induct_tac}@{text "\<^sup>*"} & : & @{text method} \\
   125     @{method_def (ZF) ind_cases}@{text "\<^sup>*"} & : & @{text method} \\
   126     @{command_def (ZF) "inductive_cases"} & : & @{text "theory \<rightarrow> theory"} \\
   127   \end{matharray}
   128 
   129   @{rail \<open>
   130     (@@{method (ZF) case_tac} | @@{method (ZF) induct_tac}) @{syntax goal_spec}? @{syntax name}
   131     ;
   132     @@{method (ZF) ind_cases} (@{syntax prop} +)
   133     ;
   134     @@{command (ZF) inductive_cases} (@{syntax thmdecl}? (@{syntax prop} +) + @'and')
   135   \<close>}
   136 *}
   137 
   138 end