# HG changeset patch # User haftmann # Date 1284382445 -7200 # Node ID 8d42d668b5b05b37a33729b0a19c6bc8b5c4e19a # Parent c1f3992c90975b69a180e21df4b0adf7e49b5892 added Imperative HOL overview diff -r c1f3992c9097 -r 8d42d668b5b0 src/HOL/Imperative_HOL/Imperative_HOL_ex.thy --- 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 diff -r c1f3992c9097 -r 8d42d668b5b0 src/HOL/Imperative_HOL/Overview.thy --- /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 ("_\_", [4, 0], 3)), + ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_\_", [4, 0], 3))] + #> Sign.add_modesyntax_i (Symbol.xsymbolsN, false) [ + ("_constrain", typ "logic => type => logic", Mixfix ("_ \ _", [4, 0], 3)), + ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_ \ _", [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 diff -r c1f3992c9097 -r 8d42d668b5b0 src/HOL/Imperative_HOL/ROOT.ML --- 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"]; diff -r c1f3992c9097 -r 8d42d668b5b0 src/HOL/Imperative_HOL/document/root.bib --- /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 +} diff -r c1f3992c9097 -r 8d42d668b5b0 src/HOL/Imperative_HOL/document/root.tex --- /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}