--- a/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy Mon Sep 13 14:54:02 2010 +0200
+++ b/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy Mon Sep 13 14:54:05 2010 +0200
@@ -6,7 +6,7 @@
header {* Monadic imperative HOL with examples *}
theory Imperative_HOL_ex
-imports Imperative_HOL
+imports Imperative_HOL Overview
"ex/Imperative_Quicksort" "ex/Imperative_Reverse" "ex/Linked_Lists" "ex/SatChecker"
begin
--- /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
--- a/src/HOL/Imperative_HOL/ROOT.ML Mon Sep 13 14:54:02 2010 +0200
+++ b/src/HOL/Imperative_HOL/ROOT.ML Mon Sep 13 14:54:05 2010 +0200
@@ -1,1 +1,4 @@
+
+no_document use_thys ["Countable", "Monad_Syntax", "Code_Natural", "LaTeXsugar"];
+
use_thys ["Imperative_HOL_ex"];
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Imperative_HOL/document/root.bib Mon Sep 13 14:54:05 2010 +0200
@@ -0,0 +1,25 @@
+
+@string{LNCS="Lecture Notes in Computer Science"}
+@string{Springer="Springer-Verlag"}
+
+@inproceedings{Bulwahn-et-al:2008:imp_HOL,
+ author = {Lukas Bulwahn and Alexander Krauss and Florian Haftmann and Levent Erk{\"o}k and John Matthews},
+ title = {Imperative Functional Programming with {Isabelle/HOL}},
+ booktitle = {TPHOLs '08: Proceedings of the 21th International Conference on Theorem Proving in Higher Order Logics},
+ year = {2008},
+ isbn = {978-3-540-71065-3},
+ pages = {352--367},
+ publisher = Springer,
+ series = LNCS,
+ volume = {5170},
+ editor = {Otmane A\"{\i}t Mohamed and C{\'e}sar Mu{\~n}oz and Sofi{\`e}ne Tahar}
+}
+
+@book{Nipkow-et-al:2002:tutorial,
+ author = {T. Nipkow and L. C. Paulson and M. Wenzel},
+ title = {{Isabelle/HOL} --- A Proof Assistant for Higher-Order Logic},
+ series = LNCS,
+ volume = 2283,
+ year = 2002,
+ publisher = Springer
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Imperative_HOL/document/root.tex Mon Sep 13 14:54:05 2010 +0200
@@ -0,0 +1,80 @@
+
+\documentclass[11pt,a4paper]{article}
+\usepackage{graphicx,isabelle,isabellesym,latexsym}
+\usepackage{amssymb}
+\usepackage[english]{babel}
+\usepackage[only,bigsqcap]{stmaryrd}
+\usepackage{pdfsetup}
+\usepackage{ifthen}
+
+\urlstyle{rm}
+\isabellestyle{it}
+\pagestyle{myheadings}
+
+
+% symbols
+\newcommand{\isasymbind}{\isamath{\mathbin{>\!\!\!>\mkern-6.7mu=}}}
+
+% canonical quotes
+\newcommand{\qt}[1]{``{#1}''}
+
+% xdash
+\renewcommand{\=}{\ ---\ }
+
+% ellipsis
+\newcommand{\dotspace}{\kern0.01ex}
+\renewcommand{\isasymdots}{.\dotspace.\dotspace.}
+\renewcommand{\isasymcdots}{$\cdot$\dotspace$\cdot$\dotspace$\cdot$}
+\newcommand{\isasymellipsis}{\isasymdots}
+
+% logical markup
+\newcommand{\strong}[1]{{\upshape\bfseries {#1}}}
+
+% description lists
+\newcommand{\ditem}[1]{\item[\isastyletext #1]}
+
+% quote environment
+\isakeeptag{quote}
+\renewenvironment{quote}
+ {\list{}{\leftmargin2em\rightmargin0pt}\parindent0pt\parskip0pt\item\relax}
+ {\endlist}
+\renewcommand{\isatagquote}{\begin{quote}}
+\renewcommand{\endisatagquote}{\end{quote}}
+\newcommand{\quotebreak}{\\[1.2ex]}
+
+% typographic conventions
+\newcommand{\qn}[1]{\emph{#1}}
+\newcommand{\secref}[1]{\S\ref{#1}}
+\newcommand{\figref}[1]{figure~\ref{#1}}
+
+% plain digits
+\renewcommand{\isadigit}[1]{\isamath{#1}}
+
+% invisibility
+\isadroptag{theory}
+
+% vectors
+\newcommand{\isactrlvec}[1]{\emph{$\overline{#1}$}}
+\newcommand{\isactrlbvec}{\emph\bgroup\begin{math}{}\overline\bgroup\mbox\bgroup\isastylescript}
+\newcommand{\isactrlevec}{\egroup\egroup\end{math}\egroup}
+
+% Isar proof
+\newcommand{\isasymproof}{$\;\langle\mathit{proof}\rangle$}
+
+% Isar sorry
+\renewcommand{\isacommand}[1]{\ifthenelse{\equal{sorry}{#1}}{\isasymproof}{\isakeyword{#1}}}
+
+
+\begin{document}
+
+\title{Imperative HOL -- a leightweight framework for imperative data structures in Isabelle/HOL}
+\maketitle
+
+\parindent 0pt\parskip 0.5ex
+\input{Overview}
+
+\pagestyle{headings}
+\bibliographystyle{abbrv}
+\bibliography{root}
+
+\end{document}