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