src/Doc/Logics_ZF/ZF_Isar.thy
author wenzelm
Tue, 31 Mar 2015 22:31:05 +0200
changeset 59886 e0dc738eb08c
parent 58620 7435b6a3f72e
child 62969 9f394a16c557
permissions -rw-r--r--
support for explicit scope of private entries;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
48956
d54a3d39ba85 prefer doc-src/pdfsetup.sty;
wenzelm
parents: 42705
diff changeset
     1
theory ZF_Isar
d54a3d39ba85 prefer doc-src/pdfsetup.sty;
wenzelm
parents: 42705
diff changeset
     2
imports Main
26840
ec46381f149d added logic-specific sessions;
wenzelm
parents:
diff changeset
     3
begin
ec46381f149d added logic-specific sessions;
wenzelm
parents:
diff changeset
     4
48956
d54a3d39ba85 prefer doc-src/pdfsetup.sty;
wenzelm
parents: 42705
diff changeset
     5
(*<*)
d54a3d39ba85 prefer doc-src/pdfsetup.sty;
wenzelm
parents: 42705
diff changeset
     6
ML_file "../antiquote_setup.ML"
d54a3d39ba85 prefer doc-src/pdfsetup.sty;
wenzelm
parents: 42705
diff changeset
     7
(*>*)
d54a3d39ba85 prefer doc-src/pdfsetup.sty;
wenzelm
parents: 42705
diff changeset
     8
d54a3d39ba85 prefer doc-src/pdfsetup.sty;
wenzelm
parents: 42705
diff changeset
     9
chapter {* Some Isar language elements *}
26845
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
    10
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
    11
section {* Type checking *}
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
    12
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
    13
text {*
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
    14
  The ZF logic is essentially untyped, so the concept of ``type
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
    15
  checking'' is performed as logical reasoning about set-membership
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
    16
  statements.  A special method assists users in this task; a version
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
    17
  of this is already declared as a ``solver'' in the standard
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
    18
  Simplifier setup.
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
    19
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
    20
  \begin{matharray}{rcl}
28761
9ec4482c9201 updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents: 28760
diff changeset
    21
    @{command_def (ZF) "print_tcset"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
9ec4482c9201 updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents: 28760
diff changeset
    22
    @{method_def (ZF) typecheck} & : & @{text method} \\
9ec4482c9201 updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents: 28760
diff changeset
    23
    @{attribute_def (ZF) TC} & : & @{text attribute} \\
26845
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
    24
  \end{matharray}
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
    25
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 55029
diff changeset
    26
  @{rail \<open>
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40255
diff changeset
    27
    @@{attribute (ZF) TC} (() | 'add' | 'del')
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 55029
diff changeset
    28
  \<close>}
26845
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
    29
28760
cbc435f7b16b unified use of declaration environment with IsarImplementation;
wenzelm
parents: 26894
diff changeset
    30
  \begin{description}
26845
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
    31
  
28760
cbc435f7b16b unified use of declaration environment with IsarImplementation;
wenzelm
parents: 26894
diff changeset
    32
  \item @{command (ZF) "print_tcset"} prints the collection of
26845
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
    33
  typechecking rules of the current context.
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
    34
  
28760
cbc435f7b16b unified use of declaration environment with IsarImplementation;
wenzelm
parents: 26894
diff changeset
    35
  \item @{method (ZF) typecheck} attempts to solve any pending
26845
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
    36
  type-checking problems in subgoals.
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
    37
  
28760
cbc435f7b16b unified use of declaration environment with IsarImplementation;
wenzelm
parents: 26894
diff changeset
    38
  \item @{attribute (ZF) TC} adds or deletes type-checking rules from
cbc435f7b16b unified use of declaration environment with IsarImplementation;
wenzelm
parents: 26894
diff changeset
    39
  the context.
26845
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
    40
28760
cbc435f7b16b unified use of declaration environment with IsarImplementation;
wenzelm
parents: 26894
diff changeset
    41
  \end{description}
26845
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
    42
*}
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
    43
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
    44
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
    45
section {* (Co)Inductive sets and datatypes *}
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
    46
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
    47
subsection {* Set definitions *}
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
    48
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
    49
text {*
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
    50
  In ZF everything is a set.  The generic inductive package also
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
    51
  provides a specific view for ``datatype'' specifications.
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
    52
  Coinductive definitions are available in both cases, too.
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
    53
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
    54
  \begin{matharray}{rcl}
28761
9ec4482c9201 updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents: 28760
diff changeset
    55
    @{command_def (ZF) "inductive"} & : & @{text "theory \<rightarrow> theory"} \\
9ec4482c9201 updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents: 28760
diff changeset
    56
    @{command_def (ZF) "coinductive"} & : & @{text "theory \<rightarrow> theory"} \\
9ec4482c9201 updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents: 28760
diff changeset
    57
    @{command_def (ZF) "datatype"} & : & @{text "theory \<rightarrow> theory"} \\
9ec4482c9201 updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents: 28760
diff changeset
    58
    @{command_def (ZF) "codatatype"} & : & @{text "theory \<rightarrow> theory"} \\
26845
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
    59
  \end{matharray}
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
    60
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 55029
diff changeset
    61
  @{rail \<open>
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40255
diff changeset
    62
    (@@{command (ZF) inductive} | @@{command (ZF) coinductive}) domains intros hints
26845
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
    63
    ;
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
    64
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40255
diff changeset
    65
    domains: @'domains' (@{syntax term} + '+') ('<=' | '\<subseteq>') @{syntax term}
26845
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
    66
    ;
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40255
diff changeset
    67
    intros: @'intros' (@{syntax thmdecl}? @{syntax prop} +)
26845
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
    68
    ;
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 55029
diff changeset
    69
    hints: @{syntax (ZF) "monos"}? condefs? \<newline>
42704
3f19e324ff59 tuned rail diagrams and layout;
wenzelm
parents: 42651
diff changeset
    70
      @{syntax (ZF) typeintros}? @{syntax (ZF) typeelims}?
26845
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
    71
    ;
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 55029
diff changeset
    72
    @{syntax_def (ZF) "monos"}: @'monos' @{syntax thmrefs}
26845
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
    73
    ;
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40255
diff changeset
    74
    condefs: @'con_defs' @{syntax thmrefs}
26845
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
    75
    ;
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40255
diff changeset
    76
    @{syntax_def (ZF) typeintros}: @'type_intros' @{syntax thmrefs}
26845
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
    77
    ;
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40255
diff changeset
    78
    @{syntax_def (ZF) typeelims}: @'type_elims' @{syntax thmrefs}
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 55029
diff changeset
    79
  \<close>}
26845
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
    80
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
    81
  In the following syntax specification @{text "monos"}, @{text
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
    82
  typeintros}, and @{text typeelims} are the same as above.
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
    83
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 55029
diff changeset
    84
  @{rail \<open>
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40255
diff changeset
    85
    (@@{command (ZF) datatype} | @@{command (ZF) codatatype}) domain? (dtspec + @'and') hints
26845
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
    86
    ;
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
    87
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40255
diff changeset
    88
    domain: ('<=' | '\<subseteq>') @{syntax term}
26845
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
    89
    ;
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40255
diff changeset
    90
    dtspec: @{syntax term} '=' (con + '|')
26845
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
    91
    ;
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40255
diff changeset
    92
    con: @{syntax name} ('(' (@{syntax term} ',' +) ')')?
26845
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
    93
    ;
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 55029
diff changeset
    94
    hints: @{syntax (ZF) "monos"}? @{syntax (ZF) typeintros}? @{syntax (ZF) typeelims}?
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 55029
diff changeset
    95
  \<close>}
26845
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
    96
58620
7435b6a3f72e more antiquotations;
wenzelm
parents: 56451
diff changeset
    97
  See @{cite "isabelle-ZF"} for further information on inductive
26845
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
    98
  definitions in ZF, but note that this covers the old-style theory
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
    99
  format.
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
   100
*}
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
   101
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
   102
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
   103
subsection {* Primitive recursive functions *}
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
   104
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
   105
text {*
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
   106
  \begin{matharray}{rcl}
28761
9ec4482c9201 updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents: 28760
diff changeset
   107
    @{command_def (ZF) "primrec"} & : & @{text "theory \<rightarrow> theory"} \\
26845
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
   108
  \end{matharray}
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
   109
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 55029
diff changeset
   110
  @{rail \<open>
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40255
diff changeset
   111
    @@{command (ZF) primrec} (@{syntax thmdecl}? @{syntax prop} +)
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 55029
diff changeset
   112
  \<close>}
26845
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
   113
*}
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
   114
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
   115
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
   116
subsection {* Cases and induction: emulating tactic scripts *}
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
   117
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
   118
text {*
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
   119
  The following important tactical tools of Isabelle/ZF have been
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
   120
  ported to Isar.  These should not be used in proper proof texts.
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
   121
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
   122
  \begin{matharray}{rcl}
28761
9ec4482c9201 updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents: 28760
diff changeset
   123
    @{method_def (ZF) case_tac}@{text "\<^sup>*"} & : & @{text method} \\
9ec4482c9201 updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents: 28760
diff changeset
   124
    @{method_def (ZF) induct_tac}@{text "\<^sup>*"} & : & @{text method} \\
9ec4482c9201 updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents: 28760
diff changeset
   125
    @{method_def (ZF) ind_cases}@{text "\<^sup>*"} & : & @{text method} \\
9ec4482c9201 updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents: 28760
diff changeset
   126
    @{command_def (ZF) "inductive_cases"} & : & @{text "theory \<rightarrow> theory"} \\
26845
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
   127
  \end{matharray}
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
   128
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 55029
diff changeset
   129
  @{rail \<open>
42705
528a2ba8fa74 tuned some syntax names;
wenzelm
parents: 42704
diff changeset
   130
    (@@{method (ZF) case_tac} | @@{method (ZF) induct_tac}) @{syntax goal_spec}? @{syntax name}
26845
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
   131
    ;
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40255
diff changeset
   132
    @@{method (ZF) ind_cases} (@{syntax prop} +)
26845
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
   133
    ;
42596
6c621a9d612a modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents: 40255
diff changeset
   134
    @@{command (ZF) inductive_cases} (@{syntax thmdecl}? (@{syntax prop} +) + @'and')
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 55029
diff changeset
   135
  \<close>}
26845
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
   136
*}
d86eb226ecba converted ZF specific elements;
wenzelm
parents: 26840
diff changeset
   137
26840
ec46381f149d added logic-specific sessions;
wenzelm
parents:
diff changeset
   138
end