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