src/HOL/Imperative_HOL/Overview.thy
author wenzelm
Wed, 12 Mar 2025 11:39:00 +0100
changeset 82265 4b875a4c83b0
parent 81136 2b949a3bfaac
permissions -rw-r--r--
update for release;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
39307
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
     1
(*  Title:      HOL/Imperative_HOL/Overview.thy
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
     2
    Author:     Florian Haftmann, TU Muenchen
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
     3
*)
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
     4
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
     5
(*<*)
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
     6
theory Overview
66453
cc19f7ca2ed6 session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents: 63167
diff changeset
     7
imports Imperative_HOL "HOL-Library.LaTeXsugar"
39307
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
     8
begin
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
     9
81136
2b949a3bfaac more syntax bundles;
wenzelm
parents: 80914
diff changeset
    10
unbundle constrain_space_syntax
61143
5f898411ce87 eliminated \<Colon> from syntax of constraints;
wenzelm
parents: 58622
diff changeset
    11
(*>*)
39307
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
    12
63167
0909deb8059b isabelle update_cartouches -c -t;
wenzelm
parents: 62390
diff changeset
    13
text \<open>
71847
da12452c9be2 corrected spelling and tuned whitespace
haftmann
parents: 69597
diff changeset
    14
  \<open>Imperative HOL\<close> is a lightweight framework for reasoning
63167
0909deb8059b isabelle update_cartouches -c -t;
wenzelm
parents: 62390
diff changeset
    15
  about imperative data structures in \<open>Isabelle/HOL\<close>
76987
4c275405faae isabelle update -u cite;
wenzelm
parents: 71847
diff changeset
    16
  \<^cite>\<open>"Nipkow-et-al:2002:tutorial"\<close>.  Its basic ideas are described in
4c275405faae isabelle update -u cite;
wenzelm
parents: 71847
diff changeset
    17
  \<^cite>\<open>"Bulwahn-et-al:2008:imp_HOL"\<close>.  However their concrete
39307
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
    18
  realisation has changed since, due to both extensions and
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
    19
  refinements.  Therefore this overview wants to present the framework
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
    20
  \qt{as it is} by now.  It focusses on the user-view, less on matters
40358
b6ed3364753d added note on countable types
haftmann
parents: 39717
diff changeset
    21
  of construction.  For details study of the theory sources is
39307
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
    22
  encouraged.
63167
0909deb8059b isabelle update_cartouches -c -t;
wenzelm
parents: 62390
diff changeset
    23
\<close>
39307
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
    24
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
    25
63167
0909deb8059b isabelle update_cartouches -c -t;
wenzelm
parents: 62390
diff changeset
    26
section \<open>A polymorphic heap inside a monad\<close>
39307
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
    27
63167
0909deb8059b isabelle update_cartouches -c -t;
wenzelm
parents: 62390
diff changeset
    28
text \<open>
71847
da12452c9be2 corrected spelling and tuned whitespace
haftmann
parents: 69597
diff changeset
    29
  Heaps (\<^type>\<open>heap\<close>) can be populated by values of class \<^class>\<open>heap\<close>; HOL's default types are
da12452c9be2 corrected spelling and tuned whitespace
haftmann
parents: 69597
diff changeset
    30
  already instantiated to class \<^class>\<open>heap\<close>.  Class \<^class>\<open>heap\<close> is a subclass of \<^class>\<open>countable\<close>;
da12452c9be2 corrected spelling and tuned whitespace
haftmann
parents: 69597
diff changeset
    31
  see theory \<open>Countable\<close> for ways to instantiate types as \<^class>\<open>countable\<close>.
39307
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
    32
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 66453
diff changeset
    33
  The heap is wrapped up in a monad \<^typ>\<open>'a Heap\<close> by means of the
39307
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
    34
  following specification:
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
    35
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
    36
  \begin{quote}
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 66453
diff changeset
    37
    \<^datatype>\<open>Heap\<close>
39307
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
    38
  \end{quote}
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
    39
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
    40
  Unwrapping of this monad type happens through
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
    41
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
    42
  \begin{quote}
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 66453
diff changeset
    43
    \<^term_type>\<open>execute\<close> \\
39307
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
    44
    @{thm execute.simps [no_vars]}
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
    45
  \end{quote}
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
    46
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
    47
  This allows for equational reasoning about monadic expressions; the
63167
0909deb8059b isabelle update_cartouches -c -t;
wenzelm
parents: 62390
diff changeset
    48
  fact collection \<open>execute_simps\<close> contains appropriate rewrites
39307
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
    49
  for all fundamental operations.
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
    50
39610
23bdf736d84f tuned text
haftmann
parents: 39307
diff changeset
    51
  Primitive fine-granular control over heaps is available through rule
63167
0909deb8059b isabelle update_cartouches -c -t;
wenzelm
parents: 62390
diff changeset
    52
  \<open>Heap_cases\<close>:
39307
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
    53
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
    54
  \begin{quote}
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
    55
    @{thm [break] Heap_cases [no_vars]}
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
    56
  \end{quote}
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
    57
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
    58
  Monadic expression involve the usual combinators:
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
    59
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
    60
  \begin{quote}
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 66453
diff changeset
    61
    \<^term_type>\<open>return\<close> \\
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 66453
diff changeset
    62
    \<^term_type>\<open>bind\<close> \\
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 66453
diff changeset
    63
    \<^term_type>\<open>raise\<close>
39307
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
    64
  \end{quote}
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
    65
71847
da12452c9be2 corrected spelling and tuned whitespace
haftmann
parents: 69597
diff changeset
    66
  This is also associated with nice monad do-syntax.  The \<^typ>\<open>string\<close> argument to \<^const>\<open>raise\<close> is
da12452c9be2 corrected spelling and tuned whitespace
haftmann
parents: 69597
diff changeset
    67
  just a codified comment.
39307
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
    68
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
    69
  Among a couple of generic combinators the following is helpful for
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
    70
  establishing invariants:
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
    71
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
    72
  \begin{quote}
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 66453
diff changeset
    73
    \<^term_type>\<open>assert\<close> \\
39307
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
    74
    @{thm assert_def [no_vars]}
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
    75
  \end{quote}
63167
0909deb8059b isabelle update_cartouches -c -t;
wenzelm
parents: 62390
diff changeset
    76
\<close>
39307
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
    77
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
    78
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 66453
diff changeset
    79
section \<open>Relational reasoning about \<^type>\<open>Heap\<close> expressions\<close>
39307
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
    80
63167
0909deb8059b isabelle update_cartouches -c -t;
wenzelm
parents: 62390
diff changeset
    81
text \<open>
39307
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
    82
  To establish correctness of imperative programs, predicate
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
    83
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
    84
  \begin{quote}
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 66453
diff changeset
    85
    \<^term_type>\<open>effect\<close>
39307
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
    86
  \end{quote}
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
    87
71847
da12452c9be2 corrected spelling and tuned whitespace
haftmann
parents: 69597
diff changeset
    88
  provides a simple relational calculus.  Primitive rules are \<open>effectI\<close> and \<open>effectE\<close>, rules
da12452c9be2 corrected spelling and tuned whitespace
haftmann
parents: 69597
diff changeset
    89
  appropriate for reasoning about imperative operations are available in the \<open>effect_intros\<close> and
63167
0909deb8059b isabelle update_cartouches -c -t;
wenzelm
parents: 62390
diff changeset
    90
  \<open>effect_elims\<close> fact collections.
39307
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
    91
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
    92
  Often non-failure of imperative computations does not depend
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
    93
  on the heap at all;  reasoning then can be easier using predicate
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
    94
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
    95
  \begin{quote}
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 66453
diff changeset
    96
    \<^term_type>\<open>success\<close>
39307
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
    97
  \end{quote}
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
    98
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 66453
diff changeset
    99
  Introduction rules for \<^const>\<open>success\<close> are available in the
63167
0909deb8059b isabelle update_cartouches -c -t;
wenzelm
parents: 62390
diff changeset
   100
  \<open>success_intro\<close> fact collection.
39307
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   101
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 66453
diff changeset
   102
  \<^const>\<open>execute\<close>, \<^const>\<open>effect\<close>, \<^const>\<open>success\<close> and \<^const>\<open>bind\<close>
71847
da12452c9be2 corrected spelling and tuned whitespace
haftmann
parents: 69597
diff changeset
   103
  are related by rules \<open>execute_bind_success\<close>, \<open>success_bind_executeI\<close>, \<open>success_bind_effectI\<close>,
da12452c9be2 corrected spelling and tuned whitespace
haftmann
parents: 69597
diff changeset
   104
  \<open>effect_bindI\<close>, \<open>effect_bindE\<close> and \<open>execute_bind_eq_SomeI\<close>.
63167
0909deb8059b isabelle update_cartouches -c -t;
wenzelm
parents: 62390
diff changeset
   105
\<close>
39307
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   106
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   107
63167
0909deb8059b isabelle update_cartouches -c -t;
wenzelm
parents: 62390
diff changeset
   108
section \<open>Monadic data structures\<close>
39307
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   109
63167
0909deb8059b isabelle update_cartouches -c -t;
wenzelm
parents: 62390
diff changeset
   110
text \<open>
39307
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   111
  The operations for monadic data structures (arrays and references)
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   112
  come in two flavours:
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   113
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   114
  \begin{itemize}
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   115
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   116
     \item Operations on the bare heap; their number is kept minimal
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   117
       to facilitate proving.
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   118
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   119
     \item Operations on the heap wrapped up in a monad; these are designed
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   120
       for executing.
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   121
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   122
  \end{itemize}
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   123
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   124
  Provided proof rules are such that they reduce monad operations to
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   125
  operations on bare heaps.
39717
e9bec0b43449 added hint on reference equality
haftmann
parents: 39610
diff changeset
   126
e9bec0b43449 added hint on reference equality
haftmann
parents: 39610
diff changeset
   127
  Note that HOL equality coincides with reference equality and may be
e9bec0b43449 added hint on reference equality
haftmann
parents: 39610
diff changeset
   128
  used as primitive executable operation.
63167
0909deb8059b isabelle update_cartouches -c -t;
wenzelm
parents: 62390
diff changeset
   129
\<close>
39307
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   130
63167
0909deb8059b isabelle update_cartouches -c -t;
wenzelm
parents: 62390
diff changeset
   131
subsection \<open>Arrays\<close>
39307
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   132
63167
0909deb8059b isabelle update_cartouches -c -t;
wenzelm
parents: 62390
diff changeset
   133
text \<open>
39307
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   134
  Heap operations:
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   135
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   136
  \begin{quote}
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 66453
diff changeset
   137
    \<^term_type>\<open>Array.alloc\<close> \\
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 66453
diff changeset
   138
    \<^term_type>\<open>Array.present\<close> \\
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 66453
diff changeset
   139
    \<^term_type>\<open>Array.get\<close> \\
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 66453
diff changeset
   140
    \<^term_type>\<open>Array.set\<close> \\
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 66453
diff changeset
   141
    \<^term_type>\<open>Array.length\<close> \\
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 66453
diff changeset
   142
    \<^term_type>\<open>Array.update\<close> \\
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 66453
diff changeset
   143
    \<^term_type>\<open>Array.noteq\<close>
39307
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   144
  \end{quote}
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   145
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   146
  Monad operations:
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   147
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   148
  \begin{quote}
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 66453
diff changeset
   149
    \<^term_type>\<open>Array.new\<close> \\
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 66453
diff changeset
   150
    \<^term_type>\<open>Array.of_list\<close> \\
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 66453
diff changeset
   151
    \<^term_type>\<open>Array.make\<close> \\
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 66453
diff changeset
   152
    \<^term_type>\<open>Array.len\<close> \\
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 66453
diff changeset
   153
    \<^term_type>\<open>Array.nth\<close> \\
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 66453
diff changeset
   154
    \<^term_type>\<open>Array.upd\<close> \\
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 66453
diff changeset
   155
    \<^term_type>\<open>Array.map_entry\<close> \\
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 66453
diff changeset
   156
    \<^term_type>\<open>Array.swap\<close> \\
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 66453
diff changeset
   157
    \<^term_type>\<open>Array.freeze\<close>
39307
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   158
  \end{quote}
63167
0909deb8059b isabelle update_cartouches -c -t;
wenzelm
parents: 62390
diff changeset
   159
\<close>
39307
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   160
63167
0909deb8059b isabelle update_cartouches -c -t;
wenzelm
parents: 62390
diff changeset
   161
subsection \<open>References\<close>
39307
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   162
63167
0909deb8059b isabelle update_cartouches -c -t;
wenzelm
parents: 62390
diff changeset
   163
text \<open>
39307
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   164
  Heap operations:
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   165
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   166
  \begin{quote}
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 66453
diff changeset
   167
    \<^term_type>\<open>Ref.alloc\<close> \\
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 66453
diff changeset
   168
    \<^term_type>\<open>Ref.present\<close> \\
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 66453
diff changeset
   169
    \<^term_type>\<open>Ref.get\<close> \\
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 66453
diff changeset
   170
    \<^term_type>\<open>Ref.set\<close> \\
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 66453
diff changeset
   171
    \<^term_type>\<open>Ref.noteq\<close>
39307
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   172
  \end{quote}
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   173
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   174
  Monad operations:
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   175
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   176
  \begin{quote}
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 66453
diff changeset
   177
    \<^term_type>\<open>Ref.ref\<close> \\
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 66453
diff changeset
   178
    \<^term_type>\<open>Ref.lookup\<close> \\
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 66453
diff changeset
   179
    \<^term_type>\<open>Ref.update\<close> \\
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 66453
diff changeset
   180
    \<^term_type>\<open>Ref.change\<close>
39307
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   181
  \end{quote}
63167
0909deb8059b isabelle update_cartouches -c -t;
wenzelm
parents: 62390
diff changeset
   182
\<close>
39307
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   183
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   184
63167
0909deb8059b isabelle update_cartouches -c -t;
wenzelm
parents: 62390
diff changeset
   185
section \<open>Code generation\<close>
39307
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   186
63167
0909deb8059b isabelle update_cartouches -c -t;
wenzelm
parents: 62390
diff changeset
   187
text \<open>
39307
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   188
  Imperative HOL sets up the code generator in a way that imperative
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   189
  operations are mapped to suitable counterparts in the target
63167
0909deb8059b isabelle update_cartouches -c -t;
wenzelm
parents: 62390
diff changeset
   190
  language.  For \<open>Haskell\<close>, a suitable \<open>ST\<close> monad is used;
0909deb8059b isabelle update_cartouches -c -t;
wenzelm
parents: 62390
diff changeset
   191
  for \<open>SML\<close>, \<open>Ocaml\<close> and \<open>Scala\<close> unit values ensure
39307
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   192
  that the evaluation order is the same as you would expect from the
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   193
  original monadic expressions.  These units may look cumbersome; the
63167
0909deb8059b isabelle update_cartouches -c -t;
wenzelm
parents: 62390
diff changeset
   194
  target language variants \<open>SML_imp\<close>, \<open>Ocaml_imp\<close> and
0909deb8059b isabelle update_cartouches -c -t;
wenzelm
parents: 62390
diff changeset
   195
  \<open>Scala_imp\<close> make some effort to optimize some of them away.
0909deb8059b isabelle update_cartouches -c -t;
wenzelm
parents: 62390
diff changeset
   196
\<close>
39307
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   197
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   198
63167
0909deb8059b isabelle update_cartouches -c -t;
wenzelm
parents: 62390
diff changeset
   199
section \<open>Some hints for using the framework\<close>
39307
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   200
63167
0909deb8059b isabelle update_cartouches -c -t;
wenzelm
parents: 62390
diff changeset
   201
text \<open>
39307
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   202
  Of course a framework itself does not by itself indicate how to make
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   203
  best use of it.  Here some hints drawn from prior experiences with
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   204
  Imperative HOL:
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   205
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   206
  \begin{itemize}
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   207
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   208
    \item Proofs on bare heaps should be strictly separated from those
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   209
      for monadic expressions.  The first capture the essence, while the
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   210
      latter just describe a certain wrapping-up.
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   211
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   212
    \item A good methodology is to gradually improve an imperative
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   213
      program from a functional one.  In the extreme case this means
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   214
      that an original functional program is decomposed into suitable
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   215
      operations with exactly one corresponding imperative operation.
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   216
      Having shown suitable correspondence lemmas between those, the
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   217
      correctness prove of the whole imperative program simply
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   218
      consists of composing those.
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   219
      
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   220
    \item Whether one should prefer equational reasoning (fact
63167
0909deb8059b isabelle update_cartouches -c -t;
wenzelm
parents: 62390
diff changeset
   221
      collection \<open>execute_simps\<close> or relational reasoning (fact
0909deb8059b isabelle update_cartouches -c -t;
wenzelm
parents: 62390
diff changeset
   222
      collections \<open>effect_intros\<close> and \<open>effect_elims\<close>) depends
39610
23bdf736d84f tuned text
haftmann
parents: 39307
diff changeset
   223
      on the problems to solve.  For complex expressions or
71847
da12452c9be2 corrected spelling and tuned whitespace
haftmann
parents: 69597
diff changeset
   224
      expressions involving binders, the relation style is usually
39610
23bdf736d84f tuned text
haftmann
parents: 39307
diff changeset
   225
      superior but requires more proof text.
39307
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   226
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   227
    \item Note that you can extend the fact collections of Imperative
39610
23bdf736d84f tuned text
haftmann
parents: 39307
diff changeset
   228
      HOL yourself whenever appropriate.
39307
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   229
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   230
  \end{itemize}
63167
0909deb8059b isabelle update_cartouches -c -t;
wenzelm
parents: 62390
diff changeset
   231
\<close>
39307
8d42d668b5b0 added Imperative HOL overview
haftmann
parents:
diff changeset
   232
62390
842917225d56 more canonical names
nipkow
parents: 61143
diff changeset
   233
end