doc-src/IsarRef/Thy/Synopsis.thy
author wenzelm
Tue May 31 22:47:18 2011 +0200 (2011-05-31)
changeset 42917 ba23e83b0868
child 42918 36daee4cc9c9
permissions -rw-r--r--
added Synopsis, with some "Notepad" material;
wenzelm@42917
     1
theory Synopsis
wenzelm@42917
     2
imports Base Main
wenzelm@42917
     3
begin
wenzelm@42917
     4
wenzelm@42917
     5
chapter {* Synopsis *}
wenzelm@42917
     6
wenzelm@42917
     7
section {* Notepad *}
wenzelm@42917
     8
wenzelm@42917
     9
text {*
wenzelm@42917
    10
  An Isar proof body serves as mathematical notepad to compose logical
wenzelm@42917
    11
  content, consisting of facts, terms, types.
wenzelm@42917
    12
*}
wenzelm@42917
    13
wenzelm@42917
    14
wenzelm@42917
    15
subsection {* Facts *}
wenzelm@42917
    16
wenzelm@42917
    17
text {*
wenzelm@42917
    18
  A fact is a simultaneous list of theorems.
wenzelm@42917
    19
*}
wenzelm@42917
    20
wenzelm@42917
    21
wenzelm@42917
    22
subsubsection {* Producing facts *}
wenzelm@42917
    23
wenzelm@42917
    24
notepad
wenzelm@42917
    25
begin
wenzelm@42917
    26
wenzelm@42917
    27
  txt {* Via assumption (``lambda''): *}
wenzelm@42917
    28
  assume a: A
wenzelm@42917
    29
wenzelm@42917
    30
  txt {* Via proof (``let''): *}
wenzelm@42917
    31
  have b: B sorry
wenzelm@42917
    32
wenzelm@42917
    33
  txt {* Via abbreviation (``let''): *}
wenzelm@42917
    34
  note c = a b
wenzelm@42917
    35
wenzelm@42917
    36
end
wenzelm@42917
    37
wenzelm@42917
    38
wenzelm@42917
    39
subsubsection {* Referencing facts *}
wenzelm@42917
    40
wenzelm@42917
    41
notepad
wenzelm@42917
    42
begin
wenzelm@42917
    43
  txt {* Via explicit name: *}
wenzelm@42917
    44
  assume a: A
wenzelm@42917
    45
  note a
wenzelm@42917
    46
wenzelm@42917
    47
  txt {* Via implicit name: *}
wenzelm@42917
    48
  assume A
wenzelm@42917
    49
  note this
wenzelm@42917
    50
wenzelm@42917
    51
  txt {* Via literal proposition (unification with results from the proof text): *}
wenzelm@42917
    52
  assume A
wenzelm@42917
    53
  note `A`
wenzelm@42917
    54
wenzelm@42917
    55
  assume "\<And>x. B x"
wenzelm@42917
    56
  note `B a`
wenzelm@42917
    57
  note `B b`
wenzelm@42917
    58
end
wenzelm@42917
    59
wenzelm@42917
    60
wenzelm@42917
    61
subsubsection {* Manipulating facts *}
wenzelm@42917
    62
wenzelm@42917
    63
notepad
wenzelm@42917
    64
begin
wenzelm@42917
    65
  txt {* Instantiation: *}
wenzelm@42917
    66
  assume a: "\<And>x. B x"
wenzelm@42917
    67
  note a
wenzelm@42917
    68
  note a [of b]
wenzelm@42917
    69
  note a [where x = b]
wenzelm@42917
    70
wenzelm@42917
    71
  txt {* Backchaining: *}
wenzelm@42917
    72
  assume 1: A
wenzelm@42917
    73
  assume 2: "A \<Longrightarrow> C"
wenzelm@42917
    74
  note 2 [OF 1]
wenzelm@42917
    75
  note 1 [THEN 2]
wenzelm@42917
    76
wenzelm@42917
    77
  txt {* Symmetric results: *}
wenzelm@42917
    78
  assume "x = y"
wenzelm@42917
    79
  note this [symmetric]
wenzelm@42917
    80
wenzelm@42917
    81
  assume "x \<noteq> y"
wenzelm@42917
    82
  note this [symmetric]
wenzelm@42917
    83
wenzelm@42917
    84
  txt {* Adhoc-simplication (take care!): *}
wenzelm@42917
    85
  assume "P ([] @ xs)"
wenzelm@42917
    86
  note this [simplified]
wenzelm@42917
    87
end
wenzelm@42917
    88
wenzelm@42917
    89
wenzelm@42917
    90
subsubsection {* Projections *}
wenzelm@42917
    91
wenzelm@42917
    92
text {*
wenzelm@42917
    93
  Isar facts consist of multiple theorems.  There is notation to project
wenzelm@42917
    94
  interval ranges.
wenzelm@42917
    95
*}
wenzelm@42917
    96
wenzelm@42917
    97
notepad
wenzelm@42917
    98
begin
wenzelm@42917
    99
  assume stuff: A B C D
wenzelm@42917
   100
  note stuff(1)
wenzelm@42917
   101
  note stuff(2-3)
wenzelm@42917
   102
  note stuff(2-)
wenzelm@42917
   103
end
wenzelm@42917
   104
wenzelm@42917
   105
wenzelm@42917
   106
subsubsection {* Naming conventions *}
wenzelm@42917
   107
wenzelm@42917
   108
text {*
wenzelm@42917
   109
  \begin{itemize}
wenzelm@42917
   110
wenzelm@42917
   111
  \item Lower-case identifiers are usually preferred.
wenzelm@42917
   112
wenzelm@42917
   113
  \item Facts can be named after the main term within the proposition.
wenzelm@42917
   114
wenzelm@42917
   115
  \item Facts should \emph{not} be named after the command that
wenzelm@42917
   116
  introduced them (@{command "assume"}, @{command "have"}).  This is
wenzelm@42917
   117
  misleading and hard to maintain.
wenzelm@42917
   118
wenzelm@42917
   119
  \item Natural numbers can be used as ``meaningless'' names (more
wenzelm@42917
   120
  appropriate than @{text "a1"}, @{text "a2"} etc.)
wenzelm@42917
   121
wenzelm@42917
   122
  \item Symbolic identifiers are supported (e.g. @{text "*"}, @{text
wenzelm@42917
   123
  "**"}, @{text "***"}).
wenzelm@42917
   124
wenzelm@42917
   125
  \end{itemize}
wenzelm@42917
   126
*}
wenzelm@42917
   127
wenzelm@42917
   128
wenzelm@42917
   129
subsection {* Block structure *}
wenzelm@42917
   130
wenzelm@42917
   131
text {*
wenzelm@42917
   132
  The formal notepad is block structured.  The fact produced by the last
wenzelm@42917
   133
  entry of a block is exported into the outer context.
wenzelm@42917
   134
*}
wenzelm@42917
   135
wenzelm@42917
   136
notepad
wenzelm@42917
   137
begin
wenzelm@42917
   138
  {
wenzelm@42917
   139
    have a: A sorry
wenzelm@42917
   140
    have b: B sorry
wenzelm@42917
   141
    note a b
wenzelm@42917
   142
  }
wenzelm@42917
   143
  note this
wenzelm@42917
   144
  note `A`
wenzelm@42917
   145
  note `B`
wenzelm@42917
   146
end
wenzelm@42917
   147
wenzelm@42917
   148
text {* Explicit blocks as well as implicit blocks of nested goal
wenzelm@42917
   149
  statements (e.g.\ @{command have}) automatically introduce one extra
wenzelm@42917
   150
  pair of parentheses in reserve.  The @{command next} command allows
wenzelm@42917
   151
  to ``jump'' between these sub-blocks. *}
wenzelm@42917
   152
wenzelm@42917
   153
notepad
wenzelm@42917
   154
begin
wenzelm@42917
   155
wenzelm@42917
   156
  {
wenzelm@42917
   157
    have a: A sorry
wenzelm@42917
   158
  next
wenzelm@42917
   159
    have b: B
wenzelm@42917
   160
    proof -
wenzelm@42917
   161
      show B sorry
wenzelm@42917
   162
    next
wenzelm@42917
   163
      have c: C sorry
wenzelm@42917
   164
    next
wenzelm@42917
   165
      have d: D sorry
wenzelm@42917
   166
    qed
wenzelm@42917
   167
  }
wenzelm@42917
   168
wenzelm@42917
   169
  txt {* Alternative version with explicit parentheses everywhere: *}
wenzelm@42917
   170
wenzelm@42917
   171
  {
wenzelm@42917
   172
    {
wenzelm@42917
   173
      have a: A sorry
wenzelm@42917
   174
    }
wenzelm@42917
   175
    {
wenzelm@42917
   176
      have b: B
wenzelm@42917
   177
      proof -
wenzelm@42917
   178
        {
wenzelm@42917
   179
          show B sorry
wenzelm@42917
   180
        }
wenzelm@42917
   181
        {
wenzelm@42917
   182
          have c: C sorry
wenzelm@42917
   183
        }
wenzelm@42917
   184
        {
wenzelm@42917
   185
          have d: D sorry
wenzelm@42917
   186
        }
wenzelm@42917
   187
      qed
wenzelm@42917
   188
    }
wenzelm@42917
   189
  }
wenzelm@42917
   190
wenzelm@42917
   191
end
wenzelm@42917
   192
wenzelm@42917
   193
wenzelm@42917
   194
subsection {* Terms and Types *}
wenzelm@42917
   195
wenzelm@42917
   196
notepad
wenzelm@42917
   197
begin
wenzelm@42917
   198
  txt {* Locally fixed entities: *}
wenzelm@42917
   199
  fix x   -- {* local constant, without any type information yet *}
wenzelm@42917
   200
  fix x :: 'a  -- {* variant with explicit type-constraint for subsequent use*}
wenzelm@42917
   201
wenzelm@42917
   202
  fix a b
wenzelm@42917
   203
  assume "a = b"  -- {* type assignment at first occurrence in concrete term *}
wenzelm@42917
   204
wenzelm@42917
   205
  txt {* Definitions (non-polymorphic): *}
wenzelm@42917
   206
  def x \<equiv> "t::'a"
wenzelm@42917
   207
wenzelm@42917
   208
  txt {* Abbreviations (polymorphic): *}
wenzelm@42917
   209
  let ?f = "\<lambda>x. x"
wenzelm@42917
   210
  term "?f ?f"
wenzelm@42917
   211
wenzelm@42917
   212
  txt {* Notation: *}
wenzelm@42917
   213
  write x  ("***")
wenzelm@42917
   214
end
wenzelm@42917
   215
wenzelm@42917
   216
end