# HG changeset patch # User haftmann # Date 1284382521 -7200 # Node ID c2c9bb3c52c6edfef6df2ffd47fde7901696a9db # Parent 2f38fa28e124f772ed40d4aef381271e1c41fa2c# Parent 8d42d668b5b05b37a33729b0a19c6bc8b5c4e19a merged diff -r 2f38fa28e124 -r c2c9bb3c52c6 NEWS --- a/NEWS Mon Sep 13 13:33:44 2010 +0200 +++ b/NEWS Mon Sep 13 14:55:21 2010 +0200 @@ -68,6 +68,9 @@ * Discontinued ancient 'constdefs' command. INCOMPATIBILITY, use 'definition' instead. +* Document antiquotations 'class' and 'type' for printing classes +and type constructors. + *** HOL *** diff -r 2f38fa28e124 -r c2c9bb3c52c6 doc-src/IsarRef/Thy/Document_Preparation.thy --- a/doc-src/IsarRef/Thy/Document_Preparation.thy Mon Sep 13 13:33:44 2010 +0200 +++ b/doc-src/IsarRef/Thy/Document_Preparation.thy Mon Sep 13 14:55:21 2010 +0200 @@ -146,6 +146,8 @@ @{antiquotation_def const} & : & @{text antiquotation} \\ @{antiquotation_def abbrev} & : & @{text antiquotation} \\ @{antiquotation_def typ} & : & @{text antiquotation} \\ + @{antiquotation_def type} & : & @{text antiquotation} \\ + @{antiquotation_def class} & : & @{text antiquotation} \\ @{antiquotation_def "text"} & : & @{text antiquotation} \\ @{antiquotation_def goals} & : & @{text antiquotation} \\ @{antiquotation_def subgoals} & : & @{text antiquotation} \\ @@ -190,6 +192,8 @@ 'const' options term | 'abbrev' options term | 'typ' options type | + 'type' options name | + 'class' options name | 'text' options name | 'goals' options | 'subgoals' options | @@ -243,8 +247,14 @@ \item @{text "@{abbrev c x\<^sub>1 \ x\<^sub>n}"} prints a constant abbreviation @{text "c x\<^sub>1 \ x\<^sub>n \ rhs"} as defined in the current context. + \item @{text "@{typ \}"} prints a well-formed type @{text "\"}. - + + \item @{text "@{type \}"} prints a type constructor + (logical or abbreviation) @{text "\"}. + + \item @{text "@{class c}"} prints a class @{text c}. + \item @{text "@{text s}"} prints uninterpreted source text @{text s}. This is particularly useful to print portions of text according to the Isabelle document style, without demanding well-formedness, diff -r 2f38fa28e124 -r c2c9bb3c52c6 doc-src/more_antiquote.ML --- a/doc-src/more_antiquote.ML Mon Sep 13 13:33:44 2010 +0200 +++ b/doc-src/more_antiquote.ML Mon Sep 13 14:55:21 2010 +0200 @@ -47,29 +47,6 @@ end -(* class and type constructor antiquotation *) - -local - -val pr_text = enclose "\\isa{" "}" o Pretty.output NONE o Pretty.str; - -fun pr_class ctxt = ProofContext.read_class ctxt - #> Type.extern_class (ProofContext.tsig_of ctxt) - #> pr_text; - -fun pr_type ctxt = ProofContext.read_type_name_proper ctxt true - #> (#1 o Term.dest_Type) - #> Type.extern_type (ProofContext.tsig_of ctxt) - #> pr_text; - -in - -val _ = Thy_Output.antiquotation "class" (Scan.lift Args.name) (pr_class o #context); -val _ = Thy_Output.antiquotation "type" (Scan.lift Args.name) (pr_type o #context); - -end; - - (* code theorem antiquotation *) local diff -r 2f38fa28e124 -r c2c9bb3c52c6 src/HOL/Imperative_HOL/Imperative_HOL_ex.thy --- a/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy Mon Sep 13 13:33:44 2010 +0200 +++ b/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy Mon Sep 13 14:55:21 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 2f38fa28e124 -r c2c9bb3c52c6 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:55:21 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 2f38fa28e124 -r c2c9bb3c52c6 src/HOL/Imperative_HOL/ROOT.ML --- a/src/HOL/Imperative_HOL/ROOT.ML Mon Sep 13 13:33:44 2010 +0200 +++ b/src/HOL/Imperative_HOL/ROOT.ML Mon Sep 13 14:55:21 2010 +0200 @@ -1,1 +1,4 @@ + +no_document use_thys ["Countable", "Monad_Syntax", "Code_Natural", "LaTeXsugar"]; + use_thys ["Imperative_HOL_ex"]; diff -r 2f38fa28e124 -r c2c9bb3c52c6 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:55:21 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 2f38fa28e124 -r c2c9bb3c52c6 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:55:21 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} diff -r 2f38fa28e124 -r c2c9bb3c52c6 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Mon Sep 13 13:33:44 2010 +0200 +++ b/src/HOL/IsaMakefile Mon Sep 13 14:55:21 2010 +0200 @@ -787,7 +787,7 @@ HOL-ZF: HOL $(LOG)/HOL-ZF.gz -$(LOG)/HOL-ZF.gz: $(OUT)/HOL ZF/ROOT.ML ZF/LProd.thy \ +$(LOG)/HOL-ZF.gz: $(OUT)/HOL ZF/ROOT.ML ZF/LProd.thy \ ZF/HOLZF.thy ZF/MainZF.thy ZF/Games.thy ZF/document/root.tex @$(ISABELLE_TOOL) usedir $(OUT)/HOL ZF @@ -796,18 +796,23 @@ HOL-Imperative_HOL: HOL $(LOG)/HOL-Imperative_HOL.gz -$(LOG)/HOL-Imperative_HOL.gz: $(OUT)/HOL Imperative_HOL/Array.thy \ - Imperative_HOL/Heap.thy Imperative_HOL/Heap_Monad.thy \ - Imperative_HOL/Imperative_HOL.thy Imperative_HOL/Imperative_HOL_ex.thy\ - Imperative_HOL/Mrec.thy Imperative_HOL/Ref.thy \ - Imperative_HOL/ex/Imperative_Quicksort.thy \ - Imperative_HOL/ex/Imperative_Reverse.thy \ - Imperative_HOL/ex/Linked_Lists.thy \ - Imperative_HOL/ex/SatChecker.thy \ - Imperative_HOL/ex/Sorted_List.thy \ - Imperative_HOL/ex/Subarray.thy \ +$(LOG)/HOL-Imperative_HOL.gz: $(OUT)/HOL \ + Imperative_HOL/Array.thy \ + Imperative_HOL/Heap.thy \ + Imperative_HOL/Heap_Monad.thy \ + Imperative_HOL/Imperative_HOL.thy \ + Imperative_HOL/Imperative_HOL_ex.thy \ + Imperative_HOL/Mrec.thy \ + Imperative_HOL/Ref.thy \ + Imperative_HOL/ROOT.ML \ + Imperative_HOL/ex/Imperative_Quicksort.thy \ + Imperative_HOL/ex/Imperative_Reverse.thy \ + Imperative_HOL/ex/Linked_Lists.thy \ + Imperative_HOL/ex/SatChecker.thy \ + Imperative_HOL/ex/Sorted_List.thy \ + Imperative_HOL/ex/Subarray.thy \ Imperative_HOL/ex/Sublist.thy - @$(ISABELLE_TOOL) usedir $(OUT)/HOL Imperative_HOL + @$(ISABELLE_TOOL) usedir -g true -m iff -m no_brackets $(OUT)/HOL Imperative_HOL ## HOL-Decision_Procs diff -r 2f38fa28e124 -r c2c9bb3c52c6 src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Mon Sep 13 13:33:44 2010 +0200 +++ b/src/Pure/Thy/thy_output.ML Mon Sep 13 14:55:21 2010 +0200 @@ -507,6 +507,12 @@ val ctxt' = Variable.auto_fixes eq ctxt; in ProofContext.pretty_term_abbrev ctxt' eq end; +fun pretty_class ctxt = + Pretty.str o Type.extern_class (ProofContext.tsig_of ctxt) o ProofContext.read_class ctxt; + +fun pretty_type ctxt = Pretty.str o Type.extern_type (ProofContext.tsig_of ctxt) + o fst o dest_Type o ProofContext.read_type_name_proper ctxt false; + fun pretty_prf full ctxt = Proof_Syntax.pretty_proof_of ctxt full; fun pretty_theory ctxt name = @@ -561,6 +567,8 @@ val _ = basic_entity "const" (Args.const_proper false) pretty_const; val _ = basic_entity "abbrev" (Scan.lift Args.name_source) pretty_abbrev; val _ = basic_entity "typ" Args.typ_abbrev Syntax.pretty_typ; +val _ = basic_entity "class" (Scan.lift Args.name) pretty_class; +val _ = basic_entity "type" (Scan.lift Args.name) pretty_type; val _ = basic_entity "text" (Scan.lift Args.name) pretty_text; val _ = basic_entities "prf" Attrib.thms (pretty_prf false); val _ = basic_entities "full_prf" Attrib.thms (pretty_prf true);