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