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