src/HOL/Imperative_HOL/Overview.thy
author haftmann
Wed Sep 22 10:30:24 2010 +0200 (2010-09-22)
changeset 39610 23bdf736d84f
parent 39307 8d42d668b5b0
child 39717 e9bec0b43449
permissions -rw-r--r--
tuned text
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
haftmann@39307
     7
imports Imperative_HOL 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@39307
    34
  of constructions.  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@39307
    44
  heap}.
haftmann@39307
    45
haftmann@39307
    46
  The heap is wrapped up in a monad @{typ "'a Heap"} by means of the
haftmann@39307
    47
  following specification:
haftmann@39307
    48
haftmann@39307
    49
  \begin{quote}
haftmann@39307
    50
    @{datatype Heap}
haftmann@39307
    51
  \end{quote}
haftmann@39307
    52
haftmann@39307
    53
  Unwrapping of this monad type happens through
haftmann@39307
    54
haftmann@39307
    55
  \begin{quote}
haftmann@39307
    56
    @{term_type execute} \\
haftmann@39307
    57
    @{thm execute.simps [no_vars]}
haftmann@39307
    58
  \end{quote}
haftmann@39307
    59
haftmann@39307
    60
  This allows for equational reasoning about monadic expressions; the
haftmann@39307
    61
  fact collection @{text execute_simps} contains appropriate rewrites
haftmann@39307
    62
  for all fundamental operations.
haftmann@39307
    63
haftmann@39610
    64
  Primitive fine-granular control over heaps is available through rule
haftmann@39307
    65
  @{text Heap_cases}:
haftmann@39307
    66
haftmann@39307
    67
  \begin{quote}
haftmann@39307
    68
    @{thm [break] Heap_cases [no_vars]}
haftmann@39307
    69
  \end{quote}
haftmann@39307
    70
haftmann@39307
    71
  Monadic expression involve the usual combinators:
haftmann@39307
    72
haftmann@39307
    73
  \begin{quote}
haftmann@39307
    74
    @{term_type return} \\
haftmann@39307
    75
    @{term_type bind} \\
haftmann@39307
    76
    @{term_type raise}
haftmann@39307
    77
  \end{quote}
haftmann@39307
    78
haftmann@39307
    79
  This is also associated with nice monad do-syntax.  The @{typ
haftmann@39307
    80
  string} argument to @{const raise} is just a codified comment.
haftmann@39307
    81
haftmann@39307
    82
  Among a couple of generic combinators the following is helpful for
haftmann@39307
    83
  establishing invariants:
haftmann@39307
    84
haftmann@39307
    85
  \begin{quote}
haftmann@39307
    86
    @{term_type assert} \\
haftmann@39307
    87
    @{thm assert_def [no_vars]}
haftmann@39307
    88
  \end{quote}
haftmann@39307
    89
*}
haftmann@39307
    90
haftmann@39307
    91
haftmann@39307
    92
section {* Relational reasoning about @{type Heap} expressions *}
haftmann@39307
    93
haftmann@39307
    94
text {*
haftmann@39307
    95
  To establish correctness of imperative programs, predicate
haftmann@39307
    96
haftmann@39307
    97
  \begin{quote}
haftmann@39307
    98
    @{term_type crel}
haftmann@39307
    99
  \end{quote}
haftmann@39307
   100
haftmann@39307
   101
  provides a simple relational calculus.  Primitive rules are @{text
haftmann@39307
   102
  crelI} and @{text crelE}, rules appropriate for reasoning about
haftmann@39307
   103
  imperative operation are available in the @{text crel_intros} and
haftmann@39307
   104
  @{text crel_elims} fact collections.
haftmann@39307
   105
haftmann@39307
   106
  Often non-failure of imperative computations does not depend
haftmann@39307
   107
  on the heap at all;  reasoning then can be easier using predicate
haftmann@39307
   108
haftmann@39307
   109
  \begin{quote}
haftmann@39307
   110
    @{term_type success}
haftmann@39307
   111
  \end{quote}
haftmann@39307
   112
haftmann@39307
   113
  Introduction rules for @{const success} are available in the
haftmann@39307
   114
  @{text success_intro} fact collection.
haftmann@39307
   115
haftmann@39307
   116
  @{const execute}, @{const crel}, @{const success} and @{const bind}
haftmann@39307
   117
  are related by rules @{text execute_bind_success}, @{text
haftmann@39307
   118
  success_bind_executeI}, @{text success_bind_crelI}, @{text
haftmann@39307
   119
  crel_bindI}, @{text crel_bindE} and @{text execute_bind_eq_SomeI}.
haftmann@39307
   120
*}
haftmann@39307
   121
haftmann@39307
   122
haftmann@39307
   123
section {* Monadic data structures *}
haftmann@39307
   124
haftmann@39307
   125
text {*
haftmann@39307
   126
  The operations for monadic data structures (arrays and references)
haftmann@39307
   127
  come in two flavours:
haftmann@39307
   128
haftmann@39307
   129
  \begin{itemize}
haftmann@39307
   130
haftmann@39307
   131
     \item Operations on the bare heap; their number is kept minimal
haftmann@39307
   132
       to facilitate proving.
haftmann@39307
   133
haftmann@39307
   134
     \item Operations on the heap wrapped up in a monad; these are designed
haftmann@39307
   135
       for executing.
haftmann@39307
   136
haftmann@39307
   137
  \end{itemize}
haftmann@39307
   138
haftmann@39307
   139
  Provided proof rules are such that they reduce monad operations to
haftmann@39307
   140
  operations on bare heaps.
haftmann@39307
   141
*}
haftmann@39307
   142
haftmann@39307
   143
subsection {* Arrays *}
haftmann@39307
   144
haftmann@39307
   145
text {*
haftmann@39307
   146
  Heap operations:
haftmann@39307
   147
haftmann@39307
   148
  \begin{quote}
haftmann@39307
   149
    @{term_type Array.alloc} \\
haftmann@39307
   150
    @{term_type Array.present} \\
haftmann@39307
   151
    @{term_type Array.get} \\
haftmann@39307
   152
    @{term_type Array.set} \\
haftmann@39307
   153
    @{term_type Array.length} \\
haftmann@39307
   154
    @{term_type Array.update} \\
haftmann@39307
   155
    @{term_type Array.noteq}
haftmann@39307
   156
  \end{quote}
haftmann@39307
   157
haftmann@39307
   158
  Monad operations:
haftmann@39307
   159
haftmann@39307
   160
  \begin{quote}
haftmann@39307
   161
    @{term_type Array.new} \\
haftmann@39307
   162
    @{term_type Array.of_list} \\
haftmann@39307
   163
    @{term_type Array.make} \\
haftmann@39307
   164
    @{term_type Array.len} \\
haftmann@39307
   165
    @{term_type Array.nth} \\
haftmann@39307
   166
    @{term_type Array.upd} \\
haftmann@39307
   167
    @{term_type Array.map_entry} \\
haftmann@39307
   168
    @{term_type Array.swap} \\
haftmann@39307
   169
    @{term_type Array.freeze}
haftmann@39307
   170
  \end{quote}
haftmann@39307
   171
*}
haftmann@39307
   172
haftmann@39307
   173
subsection {* References *}
haftmann@39307
   174
haftmann@39307
   175
text {*
haftmann@39307
   176
  Heap operations:
haftmann@39307
   177
haftmann@39307
   178
  \begin{quote}
haftmann@39307
   179
    @{term_type Ref.alloc} \\
haftmann@39307
   180
    @{term_type Ref.present} \\
haftmann@39307
   181
    @{term_type Ref.get} \\
haftmann@39307
   182
    @{term_type Ref.set} \\
haftmann@39307
   183
    @{term_type Ref.noteq}
haftmann@39307
   184
  \end{quote}
haftmann@39307
   185
haftmann@39307
   186
  Monad operations:
haftmann@39307
   187
haftmann@39307
   188
  \begin{quote}
haftmann@39307
   189
    @{term_type Ref.ref} \\
haftmann@39307
   190
    @{term_type Ref.lookup} \\
haftmann@39307
   191
    @{term_type Ref.update} \\
haftmann@39307
   192
    @{term_type Ref.change}
haftmann@39307
   193
  \end{quote}
haftmann@39307
   194
*}
haftmann@39307
   195
haftmann@39307
   196
haftmann@39307
   197
section {* Code generation *}
haftmann@39307
   198
haftmann@39307
   199
text {*
haftmann@39307
   200
  Imperative HOL sets up the code generator in a way that imperative
haftmann@39307
   201
  operations are mapped to suitable counterparts in the target
haftmann@39307
   202
  language.  For @{text Haskell}, a suitable @{text ST} monad is used;
haftmann@39307
   203
  for @{text SML}, @{text Ocaml} and @{text Scala} unit values ensure
haftmann@39307
   204
  that the evaluation order is the same as you would expect from the
haftmann@39307
   205
  original monadic expressions.  These units may look cumbersome; the
haftmann@39307
   206
  target language variants @{text SML_imp}, @{text Ocaml_imp} and
haftmann@39307
   207
  @{text Scala_imp} make some effort to optimize some of them away.
haftmann@39307
   208
*}
haftmann@39307
   209
haftmann@39307
   210
haftmann@39307
   211
section {* Some hints for using the framework *}
haftmann@39307
   212
haftmann@39307
   213
text {*
haftmann@39307
   214
  Of course a framework itself does not by itself indicate how to make
haftmann@39307
   215
  best use of it.  Here some hints drawn from prior experiences with
haftmann@39307
   216
  Imperative HOL:
haftmann@39307
   217
haftmann@39307
   218
  \begin{itemize}
haftmann@39307
   219
haftmann@39307
   220
    \item Proofs on bare heaps should be strictly separated from those
haftmann@39307
   221
      for monadic expressions.  The first capture the essence, while the
haftmann@39307
   222
      latter just describe a certain wrapping-up.
haftmann@39307
   223
haftmann@39307
   224
    \item A good methodology is to gradually improve an imperative
haftmann@39307
   225
      program from a functional one.  In the extreme case this means
haftmann@39307
   226
      that an original functional program is decomposed into suitable
haftmann@39307
   227
      operations with exactly one corresponding imperative operation.
haftmann@39307
   228
      Having shown suitable correspondence lemmas between those, the
haftmann@39307
   229
      correctness prove of the whole imperative program simply
haftmann@39307
   230
      consists of composing those.
haftmann@39307
   231
      
haftmann@39307
   232
    \item Whether one should prefer equational reasoning (fact
haftmann@39307
   233
      collection @{text execute_simps} or relational reasoning (fact
haftmann@39610
   234
      collections @{text crel_intros} and @{text crel_elims}) depends
haftmann@39610
   235
      on the problems to solve.  For complex expressions or
haftmann@39610
   236
      expressions involving binders, the relation style usually is
haftmann@39610
   237
      superior but requires more proof text.
haftmann@39307
   238
haftmann@39307
   239
    \item Note that you can extend the fact collections of Imperative
haftmann@39610
   240
      HOL yourself whenever appropriate.
haftmann@39307
   241
haftmann@39307
   242
  \end{itemize}
haftmann@39307
   243
*}
haftmann@39307
   244
haftmann@39307
   245
end