--- 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 ***
--- 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 \<dots> x\<^sub>n}"} prints a constant abbreviation
@{text "c x\<^sub>1 \<dots> x\<^sub>n \<equiv> rhs"} as defined in the current context.
+
\item @{text "@{typ \<tau>}"} prints a well-formed type @{text "\<tau>"}.
-
+
+ \item @{text "@{type \<kappa>}"} prints a type constructor
+ (logical or abbreviation) @{text "\<kappa>"}.
+
+ \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,
--- 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
--- 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
--- /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 ("_\<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 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"];
--- /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
+}
--- /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}
--- 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
--- 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);