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