Theory Overview

(*  Title:      HOL/Imperative_HOL/Overview.thy
    Author:     Florian Haftmann, TU Muenchen

theory Overview
imports Imperative_HOL "HOL-Library.LaTeXsugar"

(* type constraints with spacing *)
no_syntax (output)
  "_constrain" :: "logic => type => logic"  ("_::_" [4, 0] 3)
  "_constrain" :: "prop' => type => prop'"  ("_::_" [4, 0] 3)

syntax (output)
  "_constrain" :: "logic => type => logic"  ("_ :: _" [4, 0] 3)
  "_constrain" :: "prop' => type => prop'"  ("_ :: _" [4, 0] 3)

text Imperative HOL› is a lightweight framework for reasoning
  about imperative data structures in Isabelle/HOL›
  cite"Nipkow-et-al:2002:tutorial".  Its basic ideas are described in
  cite"Bulwahn-et-al:2008:imp_HOL".  However their concrete
  realisation has changed since, due to both extensions and
  refinements.  Therefore this overview wants to present the framework
  \qt{as it is} by now.  It focusses on the user-view, less on matters
  of construction.  For details study of the theory sources is

section ‹A polymorphic heap inside a monad›

text ‹
  Heaps (typeheap) can be populated by values of class classheap; HOL's default types are
  already instantiated to class classheap.  Class classheap is a subclass of classcountable;
  see theory Countable› for ways to instantiate types as classcountable.

  The heap is wrapped up in a monad typ'a Heap by means of the
  following specification:


  Unwrapping of this monad type happens through

    term_typeexecute \\
    @{thm execute.simps [no_vars]}

  This allows for equational reasoning about monadic expressions; the
  fact collection execute_simps› contains appropriate rewrites
  for all fundamental operations.

  Primitive fine-granular control over heaps is available through rule

    @{thm [break] Heap_cases [no_vars]}

  Monadic expression involve the usual combinators:

    term_typereturn \\
    term_typebind \\

  This is also associated with nice monad do-syntax.  The typstring argument to constraise is
  just a codified comment.

  Among a couple of generic combinators the following is helpful for
  establishing invariants:

    term_typeassert \\
    @{thm assert_def [no_vars]}

section ‹Relational reasoning about typeHeap expressions›

text ‹
  To establish correctness of imperative programs, predicate


  provides a simple relational calculus.  Primitive rules are effectI› and effectE›, rules
  appropriate for reasoning about imperative operations are available in the effect_intros› and
  effect_elims› fact collections.

  Often non-failure of imperative computations does not depend
  on the heap at all;  reasoning then can be easier using predicate


  Introduction rules for constsuccess are available in the
  success_intro› fact collection.

  constexecute, consteffect, constsuccess and constbind
  are related by rules execute_bind_success›, success_bind_executeI›, success_bind_effectI›,
  effect_bindI›, effect_bindE› and execute_bind_eq_SomeI›.

section ‹Monadic data structures›

text ‹
  The operations for monadic data structures (arrays and references)
  come in two flavours:


     \item Operations on the bare heap; their number is kept minimal
       to facilitate proving.

     \item Operations on the heap wrapped up in a monad; these are designed
       for executing.


  Provided proof rules are such that they reduce monad operations to
  operations on bare heaps.

  Note that HOL equality coincides with reference equality and may be
  used as primitive executable operation.

subsection ‹Arrays›

text ‹
  Heap operations:

    term_typeArray.alloc \\
    term_typeArray.present \\
    term_typeArray.get \\
    term_typeArray.set \\
    term_typeArray.length \\
    term_typeArray.update \\

  Monad operations:

  \begin{quote} \\
    term_typeArray.of_list \\
    term_typeArray.make \\
    term_typeArray.len \\
    term_typeArray.nth \\
    term_typeArray.upd \\
    term_typeArray.map_entry \\
    term_typeArray.swap \\

subsection ‹References›

text ‹
  Heap operations:

    term_typeRef.alloc \\
    term_typeRef.present \\
    term_typeRef.get \\
    term_typeRef.set \\

  Monad operations:

    term_typeRef.ref \\
    term_typeRef.lookup \\
    term_typeRef.update \\

section ‹Code generation›

text ‹
  Imperative HOL sets up the code generator in a way that imperative
  operations are mapped to suitable counterparts in the target
  language.  For Haskell›, a suitable ST› monad is used;
  for SML›, Ocaml› and Scala› unit values ensure
  that the evaluation order is the same as you would expect from the
  original monadic expressions.  These units may look cumbersome; the
  target language variants SML_imp›, Ocaml_imp› and
  Scala_imp› make some effort to optimize some of them away.

section ‹Some hints for using the framework›

text ‹
  Of course a framework itself does not by itself indicate how to make
  best use of it.  Here some hints drawn from prior experiences with
  Imperative HOL:


    \item Proofs on bare heaps should be strictly separated from those
      for monadic expressions.  The first capture the essence, while the
      latter just describe a certain wrapping-up.

    \item A good methodology is to gradually improve an imperative
      program from a functional one.  In the extreme case this means
      that an original functional program is decomposed into suitable
      operations with exactly one corresponding imperative operation.
      Having shown suitable correspondence lemmas between those, the
      correctness prove of the whole imperative program simply
      consists of composing those.
    \item Whether one should prefer equational reasoning (fact
      collection execute_simps› or relational reasoning (fact
      collections effect_intros› and effect_elims›) depends
      on the problems to solve.  For complex expressions or
      expressions involving binders, the relation style is usually
      superior but requires more proof text.

    \item Note that you can extend the fact collections of Imperative
      HOL yourself whenever appropriate.