src/HOL/Imperative_HOL/Overview.thy
author paulson <lp15@cam.ac.uk>
Tue Apr 25 16:39:54 2017 +0100 (2017-04-25)
changeset 65578 e4997c181cce
parent 63167 0909deb8059b
child 66453 cc19f7ca2ed6
permissions -rw-r--r--
New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
haftmann@39307
     1
(*  Title:      HOL/Imperative_HOL/Overview.thy
haftmann@39307
     2
    Author:     Florian Haftmann, TU Muenchen
haftmann@39307
     3
*)
haftmann@39307
     4
haftmann@39307
     5
(*<*)
haftmann@39307
     6
theory Overview
wenzelm@41413
     7
imports Imperative_HOL "~~/src/HOL/Library/LaTeXsugar"
haftmann@39307
     8
begin
haftmann@39307
     9
haftmann@39307
    10
(* type constraints with spacing *)
wenzelm@61143
    11
no_syntax (output)
wenzelm@61143
    12
  "_constrain" :: "logic => type => logic"  ("_::_" [4, 0] 3)
wenzelm@61143
    13
  "_constrain" :: "prop' => type => prop'"  ("_::_" [4, 0] 3)
wenzelm@61143
    14
wenzelm@61143
    15
syntax (output)
wenzelm@61143
    16
  "_constrain" :: "logic => type => logic"  ("_ :: _" [4, 0] 3)
wenzelm@61143
    17
  "_constrain" :: "prop' => type => prop'"  ("_ :: _" [4, 0] 3)
wenzelm@61143
    18
(*>*)
haftmann@39307
    19
wenzelm@63167
    20
text \<open>
wenzelm@63167
    21
  \<open>Imperative HOL\<close> is a leightweight framework for reasoning
wenzelm@63167
    22
  about imperative data structures in \<open>Isabelle/HOL\<close>
wenzelm@58622
    23
  @{cite "Nipkow-et-al:2002:tutorial"}.  Its basic ideas are described in
wenzelm@58622
    24
  @{cite "Bulwahn-et-al:2008:imp_HOL"}.  However their concrete
haftmann@39307
    25
  realisation has changed since, due to both extensions and
haftmann@39307
    26
  refinements.  Therefore this overview wants to present the framework
haftmann@39307
    27
  \qt{as it is} by now.  It focusses on the user-view, less on matters
haftmann@40358
    28
  of construction.  For details study of the theory sources is
haftmann@39307
    29
  encouraged.
wenzelm@63167
    30
\<close>
haftmann@39307
    31
haftmann@39307
    32
wenzelm@63167
    33
section \<open>A polymorphic heap inside a monad\<close>
haftmann@39307
    34
wenzelm@63167
    35
text \<open>
haftmann@39307
    36
  Heaps (@{type heap}) can be populated by values of class @{class
haftmann@39307
    37
  heap}; HOL's default types are already instantiated to class @{class
haftmann@40358
    38
  heap}.  Class @{class heap} is a subclass of @{class countable};  see
wenzelm@63167
    39
  theory \<open>Countable\<close> for ways to instantiate types as @{class countable}.
haftmann@39307
    40
haftmann@39307
    41
  The heap is wrapped up in a monad @{typ "'a Heap"} by means of the
haftmann@39307
    42
  following specification:
haftmann@39307
    43
haftmann@39307
    44
  \begin{quote}
haftmann@39307
    45
    @{datatype Heap}
haftmann@39307
    46
  \end{quote}
haftmann@39307
    47
haftmann@39307
    48
  Unwrapping of this monad type happens through
haftmann@39307
    49
haftmann@39307
    50
  \begin{quote}
haftmann@39307
    51
    @{term_type execute} \\
haftmann@39307
    52
    @{thm execute.simps [no_vars]}
haftmann@39307
    53
  \end{quote}
haftmann@39307
    54
haftmann@39307
    55
  This allows for equational reasoning about monadic expressions; the
wenzelm@63167
    56
  fact collection \<open>execute_simps\<close> contains appropriate rewrites
haftmann@39307
    57
  for all fundamental operations.
haftmann@39307
    58
haftmann@39610
    59
  Primitive fine-granular control over heaps is available through rule
wenzelm@63167
    60
  \<open>Heap_cases\<close>:
haftmann@39307
    61
haftmann@39307
    62
  \begin{quote}
haftmann@39307
    63
    @{thm [break] Heap_cases [no_vars]}
haftmann@39307
    64
  \end{quote}
haftmann@39307
    65
haftmann@39307
    66
  Monadic expression involve the usual combinators:
haftmann@39307
    67
haftmann@39307
    68
  \begin{quote}
haftmann@39307
    69
    @{term_type return} \\
haftmann@39307
    70
    @{term_type bind} \\
haftmann@39307
    71
    @{term_type raise}
haftmann@39307
    72
  \end{quote}
haftmann@39307
    73
haftmann@39307
    74
  This is also associated with nice monad do-syntax.  The @{typ
haftmann@39307
    75
  string} argument to @{const raise} is just a codified comment.
haftmann@39307
    76
haftmann@39307
    77
  Among a couple of generic combinators the following is helpful for
haftmann@39307
    78
  establishing invariants:
haftmann@39307
    79
haftmann@39307
    80
  \begin{quote}
haftmann@39307
    81
    @{term_type assert} \\
haftmann@39307
    82
    @{thm assert_def [no_vars]}
haftmann@39307
    83
  \end{quote}
wenzelm@63167
    84
\<close>
haftmann@39307
    85
haftmann@39307
    86
wenzelm@63167
    87
section \<open>Relational reasoning about @{type Heap} expressions\<close>
haftmann@39307
    88
wenzelm@63167
    89
text \<open>
haftmann@39307
    90
  To establish correctness of imperative programs, predicate
haftmann@39307
    91
haftmann@39307
    92
  \begin{quote}
haftmann@40671
    93
    @{term_type effect}
haftmann@39307
    94
  \end{quote}
haftmann@39307
    95
wenzelm@63167
    96
  provides a simple relational calculus.  Primitive rules are \<open>effectI\<close> and \<open>effectE\<close>, rules appropriate for reasoning about
wenzelm@63167
    97
  imperative operations are available in the \<open>effect_intros\<close> and
wenzelm@63167
    98
  \<open>effect_elims\<close> fact collections.
haftmann@39307
    99
haftmann@39307
   100
  Often non-failure of imperative computations does not depend
haftmann@39307
   101
  on the heap at all;  reasoning then can be easier using predicate
haftmann@39307
   102
haftmann@39307
   103
  \begin{quote}
haftmann@39307
   104
    @{term_type success}
haftmann@39307
   105
  \end{quote}
haftmann@39307
   106
haftmann@39307
   107
  Introduction rules for @{const success} are available in the
wenzelm@63167
   108
  \<open>success_intro\<close> fact collection.
haftmann@39307
   109
haftmann@40671
   110
  @{const execute}, @{const effect}, @{const success} and @{const bind}
wenzelm@63167
   111
  are related by rules \<open>execute_bind_success\<close>, \<open>success_bind_executeI\<close>, \<open>success_bind_effectI\<close>, \<open>effect_bindI\<close>, \<open>effect_bindE\<close> and \<open>execute_bind_eq_SomeI\<close>.
wenzelm@63167
   112
\<close>
haftmann@39307
   113
haftmann@39307
   114
wenzelm@63167
   115
section \<open>Monadic data structures\<close>
haftmann@39307
   116
wenzelm@63167
   117
text \<open>
haftmann@39307
   118
  The operations for monadic data structures (arrays and references)
haftmann@39307
   119
  come in two flavours:
haftmann@39307
   120
haftmann@39307
   121
  \begin{itemize}
haftmann@39307
   122
haftmann@39307
   123
     \item Operations on the bare heap; their number is kept minimal
haftmann@39307
   124
       to facilitate proving.
haftmann@39307
   125
haftmann@39307
   126
     \item Operations on the heap wrapped up in a monad; these are designed
haftmann@39307
   127
       for executing.
haftmann@39307
   128
haftmann@39307
   129
  \end{itemize}
haftmann@39307
   130
haftmann@39307
   131
  Provided proof rules are such that they reduce monad operations to
haftmann@39307
   132
  operations on bare heaps.
haftmann@39717
   133
haftmann@39717
   134
  Note that HOL equality coincides with reference equality and may be
haftmann@39717
   135
  used as primitive executable operation.
wenzelm@63167
   136
\<close>
haftmann@39307
   137
wenzelm@63167
   138
subsection \<open>Arrays\<close>
haftmann@39307
   139
wenzelm@63167
   140
text \<open>
haftmann@39307
   141
  Heap operations:
haftmann@39307
   142
haftmann@39307
   143
  \begin{quote}
haftmann@39307
   144
    @{term_type Array.alloc} \\
haftmann@39307
   145
    @{term_type Array.present} \\
haftmann@39307
   146
    @{term_type Array.get} \\
haftmann@39307
   147
    @{term_type Array.set} \\
haftmann@39307
   148
    @{term_type Array.length} \\
haftmann@39307
   149
    @{term_type Array.update} \\
haftmann@39307
   150
    @{term_type Array.noteq}
haftmann@39307
   151
  \end{quote}
haftmann@39307
   152
haftmann@39307
   153
  Monad operations:
haftmann@39307
   154
haftmann@39307
   155
  \begin{quote}
haftmann@39307
   156
    @{term_type Array.new} \\
haftmann@39307
   157
    @{term_type Array.of_list} \\
haftmann@39307
   158
    @{term_type Array.make} \\
haftmann@39307
   159
    @{term_type Array.len} \\
haftmann@39307
   160
    @{term_type Array.nth} \\
haftmann@39307
   161
    @{term_type Array.upd} \\
haftmann@39307
   162
    @{term_type Array.map_entry} \\
haftmann@39307
   163
    @{term_type Array.swap} \\
haftmann@39307
   164
    @{term_type Array.freeze}
haftmann@39307
   165
  \end{quote}
wenzelm@63167
   166
\<close>
haftmann@39307
   167
wenzelm@63167
   168
subsection \<open>References\<close>
haftmann@39307
   169
wenzelm@63167
   170
text \<open>
haftmann@39307
   171
  Heap operations:
haftmann@39307
   172
haftmann@39307
   173
  \begin{quote}
haftmann@39307
   174
    @{term_type Ref.alloc} \\
haftmann@39307
   175
    @{term_type Ref.present} \\
haftmann@39307
   176
    @{term_type Ref.get} \\
haftmann@39307
   177
    @{term_type Ref.set} \\
haftmann@39307
   178
    @{term_type Ref.noteq}
haftmann@39307
   179
  \end{quote}
haftmann@39307
   180
haftmann@39307
   181
  Monad operations:
haftmann@39307
   182
haftmann@39307
   183
  \begin{quote}
haftmann@39307
   184
    @{term_type Ref.ref} \\
haftmann@39307
   185
    @{term_type Ref.lookup} \\
haftmann@39307
   186
    @{term_type Ref.update} \\
haftmann@39307
   187
    @{term_type Ref.change}
haftmann@39307
   188
  \end{quote}
wenzelm@63167
   189
\<close>
haftmann@39307
   190
haftmann@39307
   191
wenzelm@63167
   192
section \<open>Code generation\<close>
haftmann@39307
   193
wenzelm@63167
   194
text \<open>
haftmann@39307
   195
  Imperative HOL sets up the code generator in a way that imperative
haftmann@39307
   196
  operations are mapped to suitable counterparts in the target
wenzelm@63167
   197
  language.  For \<open>Haskell\<close>, a suitable \<open>ST\<close> monad is used;
wenzelm@63167
   198
  for \<open>SML\<close>, \<open>Ocaml\<close> and \<open>Scala\<close> unit values ensure
haftmann@39307
   199
  that the evaluation order is the same as you would expect from the
haftmann@39307
   200
  original monadic expressions.  These units may look cumbersome; the
wenzelm@63167
   201
  target language variants \<open>SML_imp\<close>, \<open>Ocaml_imp\<close> and
wenzelm@63167
   202
  \<open>Scala_imp\<close> make some effort to optimize some of them away.
wenzelm@63167
   203
\<close>
haftmann@39307
   204
haftmann@39307
   205
wenzelm@63167
   206
section \<open>Some hints for using the framework\<close>
haftmann@39307
   207
wenzelm@63167
   208
text \<open>
haftmann@39307
   209
  Of course a framework itself does not by itself indicate how to make
haftmann@39307
   210
  best use of it.  Here some hints drawn from prior experiences with
haftmann@39307
   211
  Imperative HOL:
haftmann@39307
   212
haftmann@39307
   213
  \begin{itemize}
haftmann@39307
   214
haftmann@39307
   215
    \item Proofs on bare heaps should be strictly separated from those
haftmann@39307
   216
      for monadic expressions.  The first capture the essence, while the
haftmann@39307
   217
      latter just describe a certain wrapping-up.
haftmann@39307
   218
haftmann@39307
   219
    \item A good methodology is to gradually improve an imperative
haftmann@39307
   220
      program from a functional one.  In the extreme case this means
haftmann@39307
   221
      that an original functional program is decomposed into suitable
haftmann@39307
   222
      operations with exactly one corresponding imperative operation.
haftmann@39307
   223
      Having shown suitable correspondence lemmas between those, the
haftmann@39307
   224
      correctness prove of the whole imperative program simply
haftmann@39307
   225
      consists of composing those.
haftmann@39307
   226
      
haftmann@39307
   227
    \item Whether one should prefer equational reasoning (fact
wenzelm@63167
   228
      collection \<open>execute_simps\<close> or relational reasoning (fact
wenzelm@63167
   229
      collections \<open>effect_intros\<close> and \<open>effect_elims\<close>) depends
haftmann@39610
   230
      on the problems to solve.  For complex expressions or
haftmann@39610
   231
      expressions involving binders, the relation style usually is
haftmann@39610
   232
      superior but requires more proof text.
haftmann@39307
   233
haftmann@39307
   234
    \item Note that you can extend the fact collections of Imperative
haftmann@39610
   235
      HOL yourself whenever appropriate.
haftmann@39307
   236
haftmann@39307
   237
  \end{itemize}
wenzelm@63167
   238
\<close>
haftmann@39307
   239
nipkow@62390
   240
end