--- a/src/HOL/Imperative_HOL/Overview.thy Thu May 26 16:57:14 2016 +0200
+++ b/src/HOL/Imperative_HOL/Overview.thy Thu May 26 17:51:22 2016 +0200
@@ -17,9 +17,9 @@
"_constrain" :: "prop' => type => prop'" ("_ :: _" [4, 0] 3)
(*>*)
-text {*
- @{text "Imperative HOL"} is a leightweight framework for reasoning
- about imperative data structures in @{text "Isabelle/HOL"}
+text \<open>
+ \<open>Imperative HOL\<close> is a leightweight framework for reasoning
+ about imperative data structures in \<open>Isabelle/HOL\<close>
@{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
@@ -27,16 +27,16 @@
\qt{as it is} by now. It focusses on the user-view, less on matters
of construction. For details study of the theory sources is
encouraged.
-*}
+\<close>
-section {* A polymorphic heap inside a monad *}
+section \<open>A polymorphic heap inside a monad\<close>
-text {*
+text \<open>
Heaps (@{type heap}) can be populated by values of class @{class
heap}; HOL's default types are already instantiated to class @{class
heap}. Class @{class heap} is a subclass of @{class countable}; see
- theory @{text Countable} for ways to instantiate types as @{class countable}.
+ theory \<open>Countable\<close> for ways to instantiate types as @{class countable}.
The heap is wrapped up in a monad @{typ "'a Heap"} by means of the
following specification:
@@ -53,11 +53,11 @@
\end{quote}
This allows for equational reasoning about monadic expressions; the
- fact collection @{text execute_simps} contains appropriate rewrites
+ fact collection \<open>execute_simps\<close> contains appropriate rewrites
for all fundamental operations.
Primitive fine-granular control over heaps is available through rule
- @{text Heap_cases}:
+ \<open>Heap_cases\<close>:
\begin{quote}
@{thm [break] Heap_cases [no_vars]}
@@ -81,22 +81,21 @@
@{term_type assert} \\
@{thm assert_def [no_vars]}
\end{quote}
-*}
+\<close>
-section {* Relational reasoning about @{type Heap} expressions *}
+section \<open>Relational reasoning about @{type Heap} expressions\<close>
-text {*
+text \<open>
To establish correctness of imperative programs, predicate
\begin{quote}
@{term_type effect}
\end{quote}
- provides a simple relational calculus. Primitive rules are @{text
- effectI} and @{text effectE}, rules appropriate for reasoning about
- imperative operations are available in the @{text effect_intros} and
- @{text effect_elims} fact collections.
+ provides a simple relational calculus. Primitive rules are \<open>effectI\<close> and \<open>effectE\<close>, rules appropriate for reasoning about
+ imperative operations are available in the \<open>effect_intros\<close> and
+ \<open>effect_elims\<close> fact collections.
Often non-failure of imperative computations does not depend
on the heap at all; reasoning then can be easier using predicate
@@ -106,18 +105,16 @@
\end{quote}
Introduction rules for @{const success} are available in the
- @{text success_intro} fact collection.
+ \<open>success_intro\<close> fact collection.
@{const execute}, @{const effect}, @{const success} and @{const bind}
- are related by rules @{text execute_bind_success}, @{text
- success_bind_executeI}, @{text success_bind_effectI}, @{text
- effect_bindI}, @{text effect_bindE} and @{text execute_bind_eq_SomeI}.
-*}
+ are related by rules \<open>execute_bind_success\<close>, \<open>success_bind_executeI\<close>, \<open>success_bind_effectI\<close>, \<open>effect_bindI\<close>, \<open>effect_bindE\<close> and \<open>execute_bind_eq_SomeI\<close>.
+\<close>
-section {* Monadic data structures *}
+section \<open>Monadic data structures\<close>
-text {*
+text \<open>
The operations for monadic data structures (arrays and references)
come in two flavours:
@@ -136,11 +133,11 @@
Note that HOL equality coincides with reference equality and may be
used as primitive executable operation.
-*}
+\<close>
-subsection {* Arrays *}
+subsection \<open>Arrays\<close>
-text {*
+text \<open>
Heap operations:
\begin{quote}
@@ -166,11 +163,11 @@
@{term_type Array.swap} \\
@{term_type Array.freeze}
\end{quote}
-*}
+\<close>
-subsection {* References *}
+subsection \<open>References\<close>
-text {*
+text \<open>
Heap operations:
\begin{quote}
@@ -189,26 +186,26 @@
@{term_type Ref.update} \\
@{term_type Ref.change}
\end{quote}
-*}
+\<close>
-section {* Code generation *}
+section \<open>Code generation\<close>
-text {*
+text \<open>
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
+ language. For \<open>Haskell\<close>, a suitable \<open>ST\<close> monad is used;
+ for \<open>SML\<close>, \<open>Ocaml\<close> and \<open>Scala\<close> 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.
-*}
+ target language variants \<open>SML_imp\<close>, \<open>Ocaml_imp\<close> and
+ \<open>Scala_imp\<close> make some effort to optimize some of them away.
+\<close>
-section {* Some hints for using the framework *}
+section \<open>Some hints for using the framework\<close>
-text {*
+text \<open>
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:
@@ -228,8 +225,8 @@
consists of composing those.
\item Whether one should prefer equational reasoning (fact
- collection @{text execute_simps} or relational reasoning (fact
- collections @{text effect_intros} and @{text effect_elims}) depends
+ collection \<open>execute_simps\<close> or relational reasoning (fact
+ collections \<open>effect_intros\<close> and \<open>effect_elims\<close>) depends
on the problems to solve. For complex expressions or
expressions involving binders, the relation style usually is
superior but requires more proof text.
@@ -238,6 +235,6 @@
HOL yourself whenever appropriate.
\end{itemize}
-*}
+\<close>
end