--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Imperative_HOL/Overview.thy Mon Sep 13 14:54:05 2010 +0200
@@ -0,0 +1,245 @@
+(* Title: HOL/Imperative_HOL/Overview.thy
+ Author: Florian Haftmann, TU Muenchen
+*)
+
+(*<*)
+theory Overview
+imports Imperative_HOL LaTeXsugar
+begin
+
+(* type constraints with spacing *)
+setup {*
+let
+ val typ = Simple_Syntax.read_typ;
+ val typeT = Syntax.typeT;
+ val spropT = Syntax.spropT;
+in
+ Sign.del_modesyntax_i (Symbol.xsymbolsN, false) [
+ ("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)),
+ ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_\<Colon>_", [4, 0], 3))]
+ #> Sign.add_modesyntax_i (Symbol.xsymbolsN, false) [
+ ("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon> _", [4, 0], 3)),
+ ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_ \<Colon> _", [4, 0], 3))]
+end
+*}(*>*)
+
+text {*
+ @{text "Imperative HOL"} is a leightweight framework for reasoning
+ about imperative data structures in @{text "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 constructions. For details study of the theory sources is
+ encouraged.
+*}
+
+
+section {* A polymorphic heap inside a monad *}
+
+text {*
+ Heaps (@{type heap}) can be populated by values of class @{class
+ heap}; HOL's default types are already instantiated to class @{class
+ heap}.
+
+ The heap is wrapped up in a monad @{typ "'a Heap"} by means of the
+ following specification:
+
+ \begin{quote}
+ @{datatype Heap}
+ \end{quote}
+
+ Unwrapping of this monad type happens through
+
+ \begin{quote}
+ @{term_type execute} \\
+ @{thm execute.simps [no_vars]}
+ \end{quote}
+
+ This allows for equational reasoning about monadic expressions; the
+ fact collection @{text execute_simps} contains appropriate rewrites
+ for all fundamental operations.
+
+ Primitive fine-granular control over heaps is avialable through rule
+ @{text Heap_cases}:
+
+ \begin{quote}
+ @{thm [break] Heap_cases [no_vars]}
+ \end{quote}
+
+ Monadic expression involve the usual combinators:
+
+ \begin{quote}
+ @{term_type return} \\
+ @{term_type bind} \\
+ @{term_type raise}
+ \end{quote}
+
+ This is also associated with nice monad do-syntax. The @{typ
+ string} argument to @{const raise} is just a codified comment.
+
+ Among a couple of generic combinators the following is helpful for
+ establishing invariants:
+
+ \begin{quote}
+ @{term_type assert} \\
+ @{thm assert_def [no_vars]}
+ \end{quote}
+*}
+
+
+section {* Relational reasoning about @{type Heap} expressions *}
+
+text {*
+ To establish correctness of imperative programs, predicate
+
+ \begin{quote}
+ @{term_type crel}
+ \end{quote}
+
+ provides a simple relational calculus. Primitive rules are @{text
+ crelI} and @{text crelE}, rules appropriate for reasoning about
+ imperative operation are available in the @{text crel_intros} and
+ @{text crel_elims} fact collections.
+
+ Often non-failure of imperative computations does not depend
+ on the heap at all; reasoning then can be easier using predicate
+
+ \begin{quote}
+ @{term_type success}
+ \end{quote}
+
+ Introduction rules for @{const success} are available in the
+ @{text success_intro} fact collection.
+
+ @{const execute}, @{const crel}, @{const success} and @{const bind}
+ are related by rules @{text execute_bind_success}, @{text
+ success_bind_executeI}, @{text success_bind_crelI}, @{text
+ crel_bindI}, @{text crel_bindE} and @{text execute_bind_eq_SomeI}.
+*}
+
+
+section {* Monadic data structures *}
+
+text {*
+ The operations for monadic data structures (arrays and references)
+ come in two flavours:
+
+ \begin{itemize}
+
+ \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.
+
+ \end{itemize}
+
+ Provided proof rules are such that they reduce monad operations to
+ operations on bare heaps.
+*}
+
+subsection {* Arrays *}
+
+text {*
+ Heap operations:
+
+ \begin{quote}
+ @{term_type Array.alloc} \\
+ @{term_type Array.present} \\
+ @{term_type Array.get} \\
+ @{term_type Array.set} \\
+ @{term_type Array.length} \\
+ @{term_type Array.update} \\
+ @{term_type Array.noteq}
+ \end{quote}
+
+ Monad operations:
+
+ \begin{quote}
+ @{term_type Array.new} \\
+ @{term_type Array.of_list} \\
+ @{term_type Array.make} \\
+ @{term_type Array.len} \\
+ @{term_type Array.nth} \\
+ @{term_type Array.upd} \\
+ @{term_type Array.map_entry} \\
+ @{term_type Array.swap} \\
+ @{term_type Array.freeze}
+ \end{quote}
+*}
+
+subsection {* References *}
+
+text {*
+ Heap operations:
+
+ \begin{quote}
+ @{term_type Ref.alloc} \\
+ @{term_type Ref.present} \\
+ @{term_type Ref.get} \\
+ @{term_type Ref.set} \\
+ @{term_type Ref.noteq}
+ \end{quote}
+
+ Monad operations:
+
+ \begin{quote}
+ @{term_type Ref.ref} \\
+ @{term_type Ref.lookup} \\
+ @{term_type Ref.update} \\
+ @{term_type Ref.change}
+ \end{quote}
+*}
+
+
+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 @{text Haskell}, a suitable @{text ST} monad is used;
+ for @{text SML}, @{text Ocaml} and @{text 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 @{text SML_imp}, @{text Ocaml_imp} and
+ @{text 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:
+
+ \begin{itemize}
+
+ \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 @{text execute_simps} or relational reasoning (fact
+ collections @{text crel_intros} and @{text crel_elims}) dependes
+ on the problems. For complex expressions or expressions
+ involving binders, the relation style usually is superior but
+ requires more proof text.
+
+ \item Note that you can extend the fact collections of Imperative
+ HOL yourself.
+
+ \end{itemize}
+*}
+
+end
\ No newline at end of file