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