author wenzelm Mon, 21 Dec 2015 21:48:36 +0100 changeset 61893 4121cc8479f8 parent 61889 42d902e074e8 child 61894 f5a2aed23206
misc tuning and modernization;
 src/HOL/Unix/Nested_Environment.thy file | annotate | diff | comparison | revisions src/HOL/Unix/Unix.thy file | annotate | diff | comparison | revisions
--- a/src/HOL/Unix/Nested_Environment.thy	Mon Dec 21 17:20:57 2015 +0100
+++ b/src/HOL/Unix/Nested_Environment.thy	Mon Dec 21 21:48:36 2015 +0100
@@ -9,13 +9,12 @@
begin

text \<open>
-  Consider a partial function @{term [source] "e :: 'a \<Rightarrow> 'b option"};
-  this may be understood as an \emph{environment} mapping indexes
-  @{typ 'a} to optional entry values @{typ 'b} (cf.\ the basic theory
-  @{text Map} of Isabelle/HOL).  This basic idea is easily generalized
-  to that of a \emph{nested environment}, where entries may be either
-  basic values or again proper environments.  Then each entry is
-  accessed by a \emph{path}, i.e.\ a list of indexes leading to its
+  Consider a partial function @{term [source] "e :: 'a \<Rightarrow> 'b option"}; this may
+  be understood as an \<^emph>\<open>environment\<close> mapping indexes @{typ 'a} to optional
+  entry values @{typ 'b} (cf.\ the basic theory \<open>Map\<close> of Isabelle/HOL). This
+  basic idea is easily generalized to that of a \<^emph>\<open>nested environment\<close>, where
+  entries may be either basic values or again proper environments. Then each
+  entry is accessed by a \<^emph>\<open>path\<close>, i.e.\ a list of indexes leading to its
position within the structure.
\<close>

@@ -24,23 +23,23 @@
| Env 'b  "'c \<Rightarrow> ('a, 'b, 'c) env option"

text \<open>
-  \medskip In the type @{typ "('a, 'b, 'c) env"} the parameter @{typ
-  'a} refers to basic values (occurring in terminal positions), type
-  @{typ 'b} to values associated with proper (inner) environments, and
-  type @{typ 'c} with the index type for branching.  Note that there
-  is no restriction on any of these types.  In particular, arbitrary
-  branching may yield rather large (transfinite) tree structures.
+  \<^medskip>
+  In the type @{typ "('a, 'b, 'c) env"} the parameter @{typ 'a} refers to
+  basic values (occurring in terminal positions), type @{typ 'b} to values
+  associated with proper (inner) environments, and type @{typ 'c} with the
+  index type for branching. Note that there is no restriction on any of these
+  types. In particular, arbitrary branching may yield rather large
+  (transfinite) tree structures.
\<close>

subsection \<open>The lookup operation\<close>

text \<open>
-  Lookup in nested environments works by following a given path of
-  index elements, leading to an optional result (a terminal value or
-  nested environment).  A \emph{defined position} within a nested
-  environment is one where @{term lookup} at its path does not yield
-  @{term None}.
+  Lookup in nested environments works by following a given path of index
+  elements, leading to an optional result (a terminal value or nested
+  environment). A \<^emph>\<open>defined position\<close> within a nested environment is one where
+  @{term lookup} at its path does not yield @{term None}.
\<close>

primrec lookup :: "('a, 'b, 'c) env \<Rightarrow> 'c list \<Rightarrow> ('a, 'b, 'c) env option"
@@ -57,8 +56,9 @@
hide_const lookup_option

text \<open>
-  \medskip The characteristic cases of @{term lookup} are expressed by
-  the following equalities.
+  \<^medskip>
+  The characteristic cases of @{term lookup} are expressed by the following
+  equalities.
\<close>

theorem lookup_nil: "lookup e [] = Some e"
@@ -91,10 +91,10 @@
by (simp split: list.split env.split)

text \<open>
-  \medskip Displaced @{term lookup} operations, relative to a certain
-  base path prefix, may be reduced as follows.  There are two cases,
-  depending whether the environment actually extends far enough to
+  \<^medskip>
+  Displaced @{term lookup} operations, relative to a certain base path prefix,
+  may be reduced as follows. There are two cases, depending whether the
+  environment actually extends far enough to follow the base path.
\<close>

theorem lookup_append_none:
@@ -177,10 +177,10 @@
qed

text \<open>
-  \medskip Successful @{term lookup} deeper down an environment
-  structure means we are able to peek further up as well.  Note that
-  this is basically just the contrapositive statement of @{thm
-  [source] lookup_append_none} above.
+  \<^medskip>
+  Successful @{term lookup} deeper down an environment structure means we are
+  able to peek further up as well. Note that this is basically just the
+  contrapositive statement of @{thm [source] lookup_append_none} above.
\<close>

theorem lookup_some_append:
@@ -194,9 +194,9 @@
qed

text \<open>
-  The subsequent statement describes in more detail how a successful
-  @{term lookup} with a non-empty path results in a certain situation
-  at any upper position.
+  The subsequent statement describes in more detail how a successful @{term
+  lookup} with a non-empty path results in a certain situation at any upper
+  position.
\<close>

theorem lookup_some_upper:
@@ -239,10 +239,9 @@
subsection \<open>The update operation\<close>

text \<open>
-  Update at a certain position in a nested environment may either
-  delete an existing entry, or overwrite an existing one.  Note that
-  update at undefined positions is simple absorbed, i.e.\ the
-  environment is left unchanged.
+  Update at a certain position in a nested environment may either delete an
+  existing entry, or overwrite an existing one. Note that update at undefined
+  positions is simple absorbed, i.e.\ the environment is left unchanged.
\<close>

primrec update :: "'c list \<Rightarrow> ('a, 'b, 'c) env option \<Rightarrow>
@@ -265,8 +264,9 @@
hide_const update_option

text \<open>
-  \medskip The characteristic cases of @{term update} are expressed by
-  the following equalities.
+  \<^medskip>
+  The characteristic cases of @{term update} are expressed by the following
+  equalities.
\<close>

theorem update_nil_none: "update [] None env = env"
@@ -315,9 +315,10 @@
by (simp split: list.split env.split option.split)

text \<open>
-  \medskip The most basic correspondence of @{term lookup} and @{term
-  update} states that after @{term update} at a defined position,
-  subsequent @{term lookup} operations would yield the new value.
+  \<^medskip>
+  The most basic correspondence of @{term lookup} and @{term update} states
+  that after @{term update} at a defined position, subsequent @{term lookup}
+  operations would yield the new value.
\<close>

theorem lookup_update_some:
@@ -362,11 +363,11 @@
qed

text \<open>
-  \medskip The properties of displaced @{term update} operations are
-  analogous to those of @{term lookup} above.  There are two cases:
-  below an undefined position @{term update} is absorbed altogether,
-  and below a defined positions @{term update} affects subsequent
-  @{term lookup} operations in the obvious way.
+  \<^medskip>
+  The properties of displaced @{term update} operations are analogous to those
+  of @{term lookup} above. There are two cases: below an undefined position
+  @{term update} is absorbed altogether, and below a defined positions @{term
+  update} affects subsequent @{term lookup} operations in the obvious way.
\<close>

theorem update_append_none:
@@ -457,10 +458,10 @@
qed

text \<open>
-  \medskip Apparently, @{term update} does not affect the result of
-  subsequent @{term lookup} operations at independent positions, i.e.\
-  in case that the paths for @{term update} and @{term lookup} fork at
-  a certain point.
+  \<^medskip>
+  Apparently, @{term update} does not affect the result of subsequent @{term
+  lookup} operations at independent positions, i.e.\ in case that the paths
+  for @{term update} and @{term lookup} fork at a certain point.
\<close>

theorem lookup_update_other:
--- a/src/HOL/Unix/Unix.thy	Mon Dec 21 17:20:57 2015 +0100
+++ b/src/HOL/Unix/Unix.thy	Mon Dec 21 21:48:36 2015 +0100
@@ -11,39 +11,37 @@
begin

text \<open>
-  We give a simple mathematical model of the basic structures
-  underlying the Unix file-system, together with a few fundamental
-  operations that could be imagined to be performed internally by the
-  Unix kernel.  This forms the basis for the set of Unix system-calls
-  to be introduced later (see \secref{sec:unix-trans}), which are the
-  actual interface offered to processes running in user-space.
+  We give a simple mathematical model of the basic structures underlying the
+  Unix file-system, together with a few fundamental operations that could be
+  imagined to be performed internally by the Unix kernel. This forms the basis
+  for the set of Unix system-calls to be introduced later (see
+  \secref{sec:unix-trans}), which are the actual interface offered to
+  processes running in user-space.

-  \medskip Basically, any Unix file is either a \emph{plain file} or a
-  \emph{directory}, consisting of some \emph{content} plus
-  \emph{attributes}.  The content of a plain file is plain text.  The
-  content of a directory is a mapping from names to further
-  files.\footnote{In fact, this is the only way that names get
-  associated with files.  In Unix files do \emph{not} have a name in
-  itself.  Even more, any number of names may be associated with the
-  very same file due to \emph{hard links} (although this is excluded
-  from our model).}  Attributes include information to control various
-  ways to access the file (read, write etc.).
+  \<^medskip>
+  Basically, any Unix file is either a \<^emph>\<open>plain file\<close> or a \<^emph>\<open>directory\<close>,
+  consisting of some \<^emph>\<open>content\<close> plus \<^emph>\<open>attributes\<close>. The content of a plain
+  file is plain text. The content of a directory is a mapping from names to
+  further files.\<^footnote>\<open>In fact, this is the only way that names get associated with
+  files. In Unix files do \<^emph>\<open>not\<close> have a name in itself. Even more, any number
+  of names may be associated with the very same file due to \<^emph>\<open>hard links\<close>
+  (although this is excluded from our model).\<close> Attributes include information
+  to control various ways to access the file (read, write etc.).

-  Our model will be quite liberal in omitting excessive detail that is
-  easily seen to be irrelevant'' for the aspects of Unix
-  file-systems to be discussed here.  First of all, we ignore
-  character and block special files, pipes, sockets, hard links,
-  symbolic links, and mount points.
+  Our model will be quite liberal in omitting excessive detail that is easily
+  seen to be irrelevant'' for the aspects of Unix file-systems to be
+  discussed here. First of all, we ignore character and block special files,
\<close>

subsection \<open>Names\<close>

text \<open>
-  User ids and file name components shall be represented by natural
-  numbers (without loss of generality).  We do not bother about
-  encoding of actual names (e.g.\ strings), nor a mapping between user
-  names and user ids as would be present in a reality.
+  User ids and file name components shall be represented by natural numbers
+  (without loss of generality). We do not bother about encoding of actual
+  names (e.g.\ strings), nor a mapping between user names and user ids as
+  would be present in a reality.
\<close>

type_synonym uid = nat
@@ -54,29 +52,28 @@
subsection \<open>Attributes\<close>

text \<open>
-  Unix file attributes mainly consist of \emph{owner} information and
-  a number of \emph{permission} bits which control access for
-  user'', group'', and others'' (see the Unix man pages @{text
-  "chmod(2)"} and @{text "stat(2)"} for more details).
+  Unix file attributes mainly consist of \<^emph>\<open>owner\<close> information and a number of
+  \<^emph>\<open>permission\<close> bits which control access for user'', group'', and
+  others'' (see the Unix man pages \<open>chmod(2)\<close> and \<open>stat(2)\<close> for more
+  details).

-  \medskip Our model of file permissions only considers the others''
-  part.  The user'' field may be omitted without loss of overall
-  generality, since the owner is usually able to change it anyway by
-  performing @{text chmod}.\footnote{The inclined Unix expert may try
-  to figure out some exotic arrangements of a real-world Unix
-  file-system such that the owner of a file is unable to apply the
-  @{text chmod} system call.}  We omit group'' permissions as a
-  genuine simplification as we just do not intend to discuss a model
-  of multiple groups and group membership, but pretend that everyone
-  is member of a single global group.\footnote{A general HOL model of
-  user group structures and related issues is given in
-  @{cite "Naraschewski:2001"}.}
+  \<^medskip>
+  Our model of file permissions only considers the others'' part. The
+  user'' field may be omitted without loss of overall generality, since the
+  owner is usually able to change it anyway by performing \<open>chmod\<close>.\<^footnote>\<open>The
+  inclined Unix expert may try to figure out some exotic arrangements of a
+  real-world Unix file-system such that the owner of a file is unable to apply
+  the \<open>chmod\<close> system call.\<close> We omit group'' permissions as a genuine
+  simplification as we just do not intend to discuss a model of multiple
+  groups and group membership, but pretend that everyone is member of a single
+  global group.\<^footnote>\<open>A general HOL model of user group structures and related
+  issues is given in @{cite "Naraschewski:2001"}.\<close>
\<close>

datatype perm =
| Writable
-  | Executable    -- "(ignored)"
+  | Executable    \<comment> "(ignored)"

type_synonym perms = "perm set"

@@ -85,59 +82,56 @@
others :: perms

text \<open>
-  and write access to the actual content, i.e.\ the string of text
-  stored here.  For directories @{term Readable} determines if the set
-  of entry names may be accessed, and @{term Writable} controls the
-  ability to create or delete any entries (both plain files or
-  sub-directories).
+  For plain files @{term Readable} and @{term Writable} specify read and write
+  access to the actual content, i.e.\ the string of text stored here. For
+  directories @{term Readable} determines if the set of entry names may be
+  accessed, and @{term Writable} controls the ability to create or delete any
+  entries (both plain files or sub-directories).

-  As another simplification, we ignore the @{term Executable}
-  permission altogether.  In reality it would indicate executable
-  plain files (also known as binaries''), or control actual lookup
-  of directory entries (recall that mere directory browsing is
-  controlled via @{term Readable}).  Note that the latter means that
-  in order to perform any file-system operation whatsoever, all
-  directories encountered on the path would have to grant @{term
-  Executable}.  We ignore this detail and pretend that all directories
-  give @{term Executable} permission to anybody.
+  As another simplification, we ignore the @{term Executable} permission
+  altogether. In reality it would indicate executable plain files (also known
+  as binaries''), or control actual lookup of directory entries (recall that
+  mere directory browsing is controlled via @{term Readable}). Note that the
+  latter means that in order to perform any file-system operation whatsoever,
+  all directories encountered on the path would have to grant @{term
+  Executable}. We ignore this detail and pretend that all directories give
+  @{term Executable} permission to anybody.
\<close>

subsection \<open>Files\<close>

text \<open>
-  In order to model the general tree structure of a Unix file-system
-  we use the arbitrarily branching datatype @{typ "('a, 'b, 'c) env"}
-  from the standard library of Isabelle/HOL
-  @{cite "Bauer-et-al:2002:HOL-Library"}.  This type provides
-  constructors @{term Val} and @{term Env} as follows:
+  In order to model the general tree structure of a Unix file-system we use
+  the arbitrarily branching datatype @{typ "('a, 'b, 'c) env"} from the
+  standard library of Isabelle/HOL @{cite "Bauer-et-al:2002:HOL-Library"}.
+  This type provides constructors @{term Val} and @{term Env} as follows:

-  \medskip
+  \<^medskip>
{\def\isastyleminor{\isastyle}
\begin{tabular}{l}
@{term [source] "Val :: 'a \<Rightarrow> ('a, 'b, 'c) env"} \\
@{term [source] "Env :: 'b \<Rightarrow> ('c \<Rightarrow> ('a, 'b, 'c) env option) \<Rightarrow> ('a, 'b, 'c) env"} \\
\end{tabular}}
-  \medskip
+  \<^medskip>

-  Here the parameter @{typ 'a} refers to plain values occurring at
-  leaf positions, parameter @{typ 'b} to information kept with inner
-  branch nodes, and parameter @{typ 'c} to the branching type of the
-  tree structure.  For our purpose we use the type instance with @{typ
-  "att \<times> string"} (representing plain files), @{typ att} (for
-  attributes of directory nodes), and @{typ name} (for the index type
-  of directory nodes).
+  Here the parameter @{typ 'a} refers to plain values occurring at leaf
+  positions, parameter @{typ 'b} to information kept with inner branch nodes,
+  and parameter @{typ 'c} to the branching type of the tree structure. For our
+  purpose we use the type instance with @{typ "att \<times> string"} (representing
+  plain files), @{typ att} (for attributes of directory nodes), and @{typ
+  name} (for the index type of directory nodes).
\<close>

type_synonym "file" = "(att \<times> string, att, name) env"

text \<open>
-  \medskip The HOL library also provides @{term lookup} and @{term
-  update} operations for general tree structures with the subsequent
-  primitive recursive characterizations.
+  \<^medskip>
+  The HOL library also provides @{term lookup} and @{term update} operations
+  for general tree structures with the subsequent primitive recursive
+  characterizations.

-  \medskip
+  \<^medskip>
{\def\isastyleminor{\isastyle}
\begin{tabular}{l}
@{term [source] "lookup :: ('a, 'b, 'c) env \<Rightarrow> 'c list \<Rightarrow> ('a, 'b, 'c) env option"} \\
@@ -148,15 +142,15 @@
@{thm [display, indent = 2, eta_contract = false] lookup_eq [no_vars]}
@{thm [display, indent = 2, eta_contract = false] update_eq [no_vars]}

-  Several further properties of these operations are proven in
-  @{cite "Bauer-et-al:2002:HOL-Library"}.  These will be routinely used
-  later on without further notice.
+  Several further properties of these operations are proven in @{cite
+  "Bauer-et-al:2002:HOL-Library"}. These will be routinely used later on
+  without further notice.

-  \bigskip Apparently, the elements of type @{typ "file"} contain an
-  @{typ att} component in either case.  We now define a few auxiliary
-  operations to manipulate this field uniformly, following the
-  conventions for record types in Isabelle/HOL
-  @{cite "Nipkow-et-al:2000:HOL"}.
+  \<^bigskip>
+  Apparently, the elements of type @{typ "file"} contain an @{typ att}
+  component in either case. We now define a few auxiliary operations to
+  manipulate this field uniformly, following the conventions for record types
+  in Isabelle/HOL @{cite "Nipkow-et-al:2000:HOL"}.
\<close>

definition
@@ -191,12 +185,11 @@
subsection \<open>Initial file-systems\<close>

text \<open>
-  Given a set of \emph{known users} a file-system shall be initialized
-  by providing an empty home directory for each user, with read-only
-  access for everyone else.  (Note that we may directly use the user
-  id as home directory name, since both types have been identified.)
-  Certainly, the very root directory is owned by the super user (who
-  has user id 0).
+  Given a set of \<^emph>\<open>known users\<close> a file-system shall be initialized by
+  providing an empty home directory for each user, with read-only access for
+  everyone else. (Note that we may directly use the user id as home directory
+  name, since both types have been identified.) Certainly, the very root
+  directory is owned by the super user (who has user id 0).
\<close>

definition
@@ -209,15 +202,15 @@
subsection \<open>Accessing file-systems\<close>

text \<open>
-  The main internal file-system operation is access of a file by a
-  user, requesting a certain set of permissions.  The resulting @{typ
-  "file option"} indicates if a file had been present at the
-  corresponding @{typ path} and if access was granted according to the
-  permissions recorded within the file-system.
+  The main internal file-system operation is access of a file by a user,
+  requesting a certain set of permissions. The resulting @{typ "file option"}
+  indicates if a file had been present at the corresponding @{typ path} and if
+  access was granted according to the permissions recorded within the
+  file-system.

-  Note that by the rules of Unix file-system security (e.g.\
-  @{cite "Tanenbaum:1992"}) both the super-user and owner may always
-  access a file unconditionally (in our simplified model).
+  Note that by the rules of Unix file-system security (e.g.\ @{cite
+  "Tanenbaum:1992"}) both the super-user and owner may always access a file
+  unconditionally (in our simplified model).
\<close>

definition
@@ -232,15 +225,17 @@
else None)"

text \<open>
-  prerequisite for system-calls to be applicable (cf.\
-  \secref{sec:unix-trans}).  Any modification of the file-system is
-  then performed using the basic @{term update} operation.
+  \<^medskip>
+  Successful access to a certain file is the main prerequisite for
+  system-calls to be applicable (cf.\ \secref{sec:unix-trans}). Any
+  modification of the file-system is then performed using the basic @{term
+  update} operation.

-  \medskip We see that @{term access} is just a wrapper for the basic
-  @{term lookup} function, with additional checking of
-  attributes. Subsequently we establish a few auxiliary facts that
-  stem from the primitive @{term lookup} used within @{term access}.
+  \<^medskip>
+  We see that @{term access} is just a wrapper for the basic @{term lookup}
+  function, with additional checking of attributes. Subsequently we establish
+  a few auxiliary facts that stem from the primitive @{term lookup} used
+  within @{term access}.
\<close>

lemma access_empty_lookup: "access root path uid {} = lookup root path"
@@ -269,19 +264,18 @@
subsection \<open>Unix system calls \label{sec:unix-syscall}\<close>

text \<open>
-  According to established operating system design (cf.\
-  @{cite "Tanenbaum:1992"}) user space processes may only initiate system
-  operations by a fixed set of \emph{system-calls}.  This enables the
-  kernel to enforce certain security policies in the first
-  place.\footnote{Incidently, this is the very same principle employed
-  by any LCF-style'' theorem proving system according to Milner's
-  principle of correctness by construction'', such as Isabelle/HOL
-  itself.}
+  According to established operating system design (cf.\ @{cite
+  "Tanenbaum:1992"}) user space processes may only initiate system operations
+  by a fixed set of \<^emph>\<open>system-calls\<close>. This enables the kernel to enforce
+  certain security policies in the first place.\<^footnote>\<open>Incidently, this is the very
+  same principle employed by any LCF-style'' theorem proving system
+  according to Milner's principle of correctness by construction'', such as
+  Isabelle/HOL itself.\<close>

-  \medskip In our model of Unix we give a fixed datatype @{text
-  operation} for the syntax of system-calls, together with an
-  inductive definition of file-system state transitions of the form
-  @{text "root \<midarrow>x\<rightarrow> root'"} for the operational semantics.
+  \<^medskip>
+  In our model of Unix we give a fixed datatype \<open>operation\<close> for the syntax of
+  system-calls, together with an inductive definition of file-system state
+  transitions of the form \<open>root \<midarrow>x\<rightarrow> root'\<close> for the operational semantics.
\<close>

datatype operation =
@@ -295,11 +289,10 @@
| Readdir uid "name set" path

text \<open>
-  The @{typ uid} field of an operation corresponds to the
-  \emph{effective user id} of the underlying process, although our
-  model never mentions processes explicitly.  The other parameters are
-  provided as arguments by the caller; the @{term path} one is common
-  to all kinds of system-calls.
+  The @{typ uid} field of an operation corresponds to the \<^emph>\<open>effective user id\<close>
+  of the underlying process, although our model never mentions processes
+  explicitly. The other parameters are provided as arguments by the caller;
+  the @{term path} one is common to all kinds of system-calls.
\<close>

primrec uid_of :: "operation \<Rightarrow> uid"
@@ -325,26 +318,24 @@
| "path_of (Readdir uid names path) = path"

text \<open>
-  \medskip Note that we have omitted explicit @{text Open} and @{text
-  Close} operations, pretending that @{term Read} and @{term Write}
-  would already take care of this behind the scenes.  Thus we have
-  basically treated actual sequences of real system-calls @{text
-  "open"}--@{text read}/@{text write}--@{text close} as atomic.
+  \<^medskip>
+  Note that we have omitted explicit \<open>Open\<close> and \<open>Close\<close> operations, pretending
+  that @{term Read} and @{term Write} would already take care of this behind
+  the scenes. Thus we have basically treated actual sequences of real

-  In principle, this could make big a difference in a model with
-  explicit concurrent processes.  On the other hand, even on a real
-  Unix system the exact scheduling of concurrent @{text "open"} and
-  @{text close} operations does \emph{not} directly affect the success
-  of corresponding @{text read} or @{text write}.  Unix allows several
-  processes to have files opened at the same time, even for writing!
+  In principle, this could make big a difference in a model with explicit
+  concurrent processes. On the other hand, even on a real Unix system the
+  exact scheduling of concurrent \<open>open\<close> and \<open>close\<close> operations does \<^emph>\<open>not\<close>
+  directly affect the success of corresponding \<open>read\<close> or \<open>write\<close>. Unix allows
+  several processes to have files opened at the same time, even for writing!
Certainly, the result from reading the contents later may be hard to
-  predict, but the system-calls involved here will succeed in any
-  case.
+  predict, but the system-calls involved here will succeed in any case.

-  \bigskip The operational semantics of system calls is now specified
-  via transitions of the file-system configuration.  This is expressed
-  as an inductive relation (although there is no actual recursion
-  involved here).
+  \<^bigskip>
+  The operational semantics of system calls is now specified via transitions
+  of the file-system configuration. This is expressed as an inductive relation
+  (although there is no actual recursion involved here).
\<close>

inductive transition :: "file \<Rightarrow> operation \<Rightarrow> file \<Rightarrow> bool"
@@ -393,19 +384,18 @@
root \<midarrow>(Readdir uid names path)\<rightarrow> root"

text \<open>
-  \medskip Certainly, the above specification is central to the whole
-  formal development.  Any of the results to be established later on
-  are only meaningful to the outside world if this transition system
-  provides an adequate model of real Unix systems.  This kind of
-  reality-check'' of a formal model is the well-known problem of
-  \emph{validation}.
+  \<^medskip>
+  Certainly, the above specification is central to the whole formal
+  development. Any of the results to be established later on are only
+  meaningful to the outside world if this transition system provides an
+  adequate model of real Unix systems. This kind of reality-check'' of a
+  formal model is the well-known problem of \<^emph>\<open>validation\<close>.

-  If in doubt, one may consider to compare our definition with the
-  informal specifications given the corresponding Unix man pages, or
-  even peek at an actual implementation such as
-  @{cite "Torvalds-et-al:Linux"}.  Another common way to gain confidence
-  into the formal model is to run simple simulations (see
-  \secref{sec:unix-examples}), and check the results with that of
+  If in doubt, one may consider to compare our definition with the informal
+  specifications given the corresponding Unix man pages, or even peek at an
+  actual implementation such as @{cite "Torvalds-et-al:Linux"}. Another common
+  way to gain confidence into the formal model is to run simple simulations
+  (see \secref{sec:unix-examples}), and check the results with that of
experiments performed on a real Unix system.
\<close>

@@ -413,13 +403,12 @@
subsection \<open>Basic properties of single transitions \label{sec:unix-single-trans}\<close>

text \<open>
-  The transition system @{text "root \<midarrow>x\<rightarrow> root'"} defined above
-  determines a unique result @{term root'} from given @{term root} and
-  @{term x} (this is holds rather trivially, since there is even only
-  one clause for each operation).  This uniqueness statement will
-  simplify our subsequent development to some extent, since we only
-  have to reason about a partial function rather than a general
-  relation.
+  The transition system \<open>root \<midarrow>x\<rightarrow> root'\<close> defined above determines a unique
+  result @{term root'} from given @{term root} and @{term x} (this is holds
+  rather trivially, since there is even only one clause for each operation).
+  This uniqueness statement will simplify our subsequent development to some
+  extent, since we only have to reason about a partial function rather than a
+  general relation.
\<close>

theorem transition_uniq:
@@ -454,9 +443,9 @@
qed

text \<open>
-  \medskip Apparently, file-system transitions are \emph{type-safe} in
-  the sense that the result of transforming an actual directory yields
-  again a directory.
+  \<^medskip>
+  Apparently, file-system transitions are \<^emph>\<open>type-safe\<close> in the sense that the
+  result of transforming an actual directory yields again a directory.
\<close>

theorem transition_type_safe:
@@ -478,22 +467,20 @@

text \<open>
The previous result may be seen as the most basic invariant on the
-  file-system state that is enforced by any proper kernel
-  implementation.  So user processes --- being bound to the
-  system-call interface --- may never mess up a file-system such that
-  the root becomes a plain file instead of a directory, which would be
-  a strange situation indeed.
+  file-system state that is enforced by any proper kernel implementation. So
+  user processes --- being bound to the system-call interface --- may never
+  mess up a file-system such that the root becomes a plain file instead of a
+  directory, which would be a strange situation indeed.
\<close>

subsection \<open>Iterated transitions\<close>

text \<open>
-  Iterated system transitions via finite sequences of system
-  operations are modeled inductively as follows.  In a sense, this
-  relation describes the cumulative effect of the sequence of
-  system-calls issued by a number of running processes over a finite
-  amount of time.
+  Iterated system transitions via finite sequences of system operations are
+  modeled inductively as follows. In a sense, this relation describes the
+  cumulative effect of the sequence of system-calls issued by a number of
+  running processes over a finite amount of time.
\<close>

inductive transitions :: "file \<Rightarrow> operation list \<Rightarrow> file \<Rightarrow> bool"
@@ -503,9 +490,9 @@
| cons: "root \<midarrow>x\<rightarrow> root' \<Longrightarrow> root' =xs\<Rightarrow> root'' \<Longrightarrow> root =(x # xs)\<Rightarrow> root''"

text \<open>
-  \medskip We establish a few basic facts relating iterated
-  transitions with single ones, according to the recursive structure
-  of lists.
+  \<^medskip>
+  We establish a few basic facts relating iterated transitions with single
+  ones, according to the recursive structure of lists.
\<close>

lemma transitions_nil_eq: "root =[]\<Rightarrow> root' = (root = root')"
@@ -530,10 +517,9 @@
qed

text \<open>
-  The next two rules show how to destruct'' known transition
-  sequences.  Note that the second one actually relies on the
-  uniqueness property of the basic transition system (see
-  \secref{sec:unix-single-trans}).
+  The next two rules show how to destruct'' known transition sequences. Note
+  that the second one actually relies on the uniqueness property of the basic
+  transition system (see \secref{sec:unix-single-trans}).
\<close>

lemma transitions_nilD: "root =[]\<Rightarrow> root' \<Longrightarrow> root' = root"
@@ -551,10 +537,11 @@
qed

text \<open>
-  \medskip The following fact shows how an invariant @{term Q} of
-  single transitions with property @{term P} may be transferred to
-  iterated transitions.  The proof is rather obvious by rule induction
-  over the definition of @{term "root =xs\<Rightarrow> root'"}.
+  \<^medskip>
+  The following fact shows how an invariant @{term Q} of single transitions
+  with property @{term P} may be transferred to iterated transitions. The
+  proof is rather obvious by rule induction over the definition of @{term
+  "root =xs\<Rightarrow> root'"}.
\<close>

lemma transitions_invariant:
@@ -576,9 +563,8 @@

text \<open>
As an example of applying the previous result, we transfer the basic
-  type-safety property (see \secref{sec:unix-single-trans}) from
-  single transitions to iterated ones, which is a rather obvious
-  result indeed.
+  type-safety property (see \secref{sec:unix-single-trans}) from single
+  transitions to iterated ones, which is a rather obvious result indeed.
\<close>

theorem transitions_type_safe:
@@ -594,35 +580,32 @@
section \<open>Executable sequences\<close>

text \<open>
-  An inductively defined relation such as the one of @{text "root \<midarrow>x\<rightarrow>
-  root'"} (see \secref{sec:unix-syscall}) has two main aspects.  First
-  of all, the resulting system admits a certain set of transition
-  rules (introductions) as given in the specification.  Furthermore,
-  there is an explicit least-fixed-point construction involved, which
-  results in induction (and case-analysis) rules to eliminate known
-  transitions in an exhaustive manner.
+  An inductively defined relation such as the one of \<open>root \<midarrow>x\<rightarrow> root'\<close> (see
+  \secref{sec:unix-syscall}) has two main aspects. First of all, the resulting
+  system admits a certain set of transition rules (introductions) as given in
+  the specification. Furthermore, there is an explicit least-fixed-point
+  construction involved, which results in induction (and case-analysis) rules
+  to eliminate known transitions in an exhaustive manner.

-  \medskip Subsequently, we explore our transition system in an
-  experimental style, mainly using the introduction rules with basic
-  algebraic properties of the underlying structures.  The technique
-  closely resembles that of Prolog combined with functional evaluation
-  in a very simple manner.
+  \<^medskip>
+  Subsequently, we explore our transition system in an experimental style,
+  mainly using the introduction rules with basic algebraic properties of the
+  underlying structures. The technique closely resembles that of Prolog
+  combined with functional evaluation in a very simple manner.

-  Just as the closed-world assumption'' is left implicit in Prolog,
-  we do not refer to induction over the whole transition system here.
-  So this is still purely positive reasoning about possible
-  executions; exhaustive reasoning will be employed only later on (see
-  \secref{sec:unix-bogosity}), when we shall demonstrate that certain
-  behavior is \emph{not} possible.
+  Just as the closed-world assumption'' is left implicit in Prolog, we do
+  not refer to induction over the whole transition system here. So this is
+  still purely positive reasoning about possible executions; exhaustive
+  reasoning will be employed only later on (see \secref{sec:unix-bogosity}),
+  when we shall demonstrate that certain behavior is \<^emph>\<open>not\<close> possible.
\<close>

subsection \<open>Possible transitions\<close>

text \<open>
-  Rather obviously, a list of system operations can be executed within
-  a certain state if there is a result state reached by an iterated
-  transition.
+  Rather obviously, a list of system operations can be executed within a
+  certain state if there is a result state reached by an iterated transition.
\<close>

definition "can_exec root xs = (\<exists>root'. root =xs\<Rightarrow> root')"
@@ -635,8 +618,9 @@
unfolding can_exec_def by (blast intro: transitions.intros)

text \<open>
-  \medskip In case that we already know that a certain sequence can be
-  executed we may destruct it backwardly into individual transitions.
+  \<^medskip>
+  In case that we already know that a certain sequence can be executed we may
+  destruct it backwardly into individual transitions.
\<close>

lemma can_exec_snocD: "can_exec root (xs @ [y])
@@ -651,7 +635,8 @@
x: "root \<midarrow>x\<rightarrow> r" and
xs_y: "r =(xs @ [y])\<Rightarrow> root''"
by (auto simp add: can_exec_def transitions_nil_eq transitions_cons_eq)
-  from xs_y Cons.hyps obtain root' r' where xs: "r =xs\<Rightarrow> root'" and y: "root' \<midarrow>y\<rightarrow> r'"
+  from xs_y Cons.hyps obtain root' r'
+    where xs: "r =xs\<Rightarrow> root'" and y: "root' \<midarrow>y\<rightarrow> r'"
unfolding can_exec_def by blast
from x xs have "root =(x # xs)\<Rightarrow> root'"
by (rule transitions.cons)
@@ -662,12 +647,11 @@
subsection \<open>Example executions \label{sec:unix-examples}\<close>

text \<open>
-  We are now ready to perform a few experiments within our formal
-  model of Unix system-calls.  The common technique is to alternate
-  introduction rules of the transition system (see
-  \secref{sec:unix-trans}), and steps to solve any emerging side
-  conditions using algebraic properties of the underlying file-system
-  structures (see \secref{sec:unix-file-system}).
+  We are now ready to perform a few experiments within our formal model of
+  Unix system-calls. The common technique is to alternate introduction rules
+  of the transition system (see \secref{sec:unix-trans}), and steps to solve
+  any emerging side conditions using algebraic properties of the underlying
+  file-system structures (see \secref{sec:unix-file-system}).
\<close>

lemmas eval = access_def init_def
@@ -675,26 +659,26 @@
theorem "u \<in> users \<Longrightarrow> can_exec (init users)
[Mkdir u perms [u, name]]"
apply (rule can_exec_cons)
-    -- \<open>back-chain @{term can_exec} (of @{term [source] Cons})\<close>
+    \<comment> \<open>back-chain @{term can_exec} (of @{term [source] Cons})\<close>
apply (rule mkdir)
-    -- \<open>back-chain @{term Mkdir}\<close>
+    \<comment> \<open>back-chain @{term Mkdir}\<close>
-    -- \<open>solve preconditions of @{term Mkdir}\<close>
+    \<comment> \<open>solve preconditions of @{term Mkdir}\<close>
-    -- \<open>peek at resulting dir (optional)\<close>
+    \<comment> \<open>peek at resulting dir (optional)\<close>
txt \<open>@{subgoals [display]}\<close>
apply (rule can_exec_nil)
-    -- \<open>back-chain @{term can_exec} (of @{term [source] Nil})\<close>
+    \<comment> \<open>back-chain @{term can_exec} (of @{term [source] Nil})\<close>
done

text \<open>
-  By inspecting the result shown just before the final step above, we
-  may gain confidence that our specification of Unix system-calls
-  actually makes sense.  Further common errors are usually exhibited
-  when preconditions of transition rules fail unexpectedly.
+  By inspecting the result shown just before the final step above, we may gain
+  confidence that our specification of Unix system-calls actually makes sense.
+  Further common errors are usually exhibited when preconditions of transition
+  rules fail unexpectedly.

-  \medskip Here are a few further experiments, using the same
-  techniques as before.
+  \<^medskip>
+  Here are a few further experiments, using the same techniques as before.
\<close>

theorem "u \<in> users \<Longrightarrow> can_exec (init users)
@@ -743,19 +727,19 @@
section \<open>Odd effects --- treated formally \label{sec:unix-bogosity}\<close>

text \<open>
-  We are now ready to give a completely formal treatment of the
-  slightly odd situation discussed in the introduction (see
-  \secref{sec:unix-intro}): the file-system can easily reach a state
-  where a user is unable to remove his very own directory, because it
-  is still populated by items placed there by another user in an
-  uncouth manner.
+  We are now ready to give a completely formal treatment of the slightly odd
+  situation discussed in the introduction (see \secref{sec:unix-intro}): the
+  file-system can easily reach a state where a user is unable to remove his
+  very own directory, because it is still populated by items placed there by
+  another user in an uncouth manner.
\<close>

+
subsection \<open>The general procedure \label{sec:unix-inv-procedure}\<close>

text \<open>
-  The following theorem expresses the general procedure we are
-  following to achieve the main result.
+  The following theorem expresses the general procedure we are following to
+  achieve the main result.
\<close>

theorem general_procedure:
@@ -781,24 +765,23 @@
qed

text \<open>
-  Here @{prop "P x"} refers to the restriction on file-system
-  operations that are admitted after having reached the critical
-  configuration; according to the problem specification this will
-  become @{prop "uid_of x = user\<^sub>1"} later on.  Furthermore,
-  @{term y} refers to the operations we claim to be impossible to
-  perform afterwards, we will take @{term Rmdir} later.  Moreover
-  @{term Q} is a suitable (auxiliary) invariant over the file-system;
-  choosing @{term Q} adequately is very important to make the proof
-  work (see \secref{sec:unix-inv-lemmas}).
+  Here @{prop "P x"} refers to the restriction on file-system operations that
+  are admitted after having reached the critical configuration; according to
+  the problem specification this will become @{prop "uid_of x = user\<^sub>1"} later
+  on. Furthermore, @{term y} refers to the operations we claim to be
+  impossible to perform afterwards, we will take @{term Rmdir} later. Moreover
+  @{term Q} is a suitable (auxiliary) invariant over the file-system; choosing
+  @{term Q} adequately is very important to make the proof work (see
+  \secref{sec:unix-inv-lemmas}).
\<close>

subsection \<open>The particular situation\<close>

text \<open>
-  We introduce a few global declarations and axioms to describe our
-  particular situation considered here.  Thus we avoid excessive use
-  of local parameters in the subsequent development.
+  We introduce a few global declarations and axioms to describe our particular
+  situation considered here. Thus we avoid excessive use of local parameters
+  in the subsequent development.
\<close>

context
@@ -829,18 +812,18 @@

text \<open>
The @{term bogus} operations are the ones that lead into the uncouth
-  situation; @{term bogus_path} is the key position within the
-  file-system where things go awry.
+  situation; @{term bogus_path} is the key position within the file-system
+  where things go awry.
\<close>

subsection \<open>Invariance lemmas \label{sec:unix-inv-lemmas}\<close>

text \<open>
-  The following invariant over the root file-system describes the
-  bogus situation in an abstract manner: located at a certain @{term
-  path} within the file-system is a non-empty directory that is
-  neither owned nor writable by @{term user\<^sub>1}.
+  The following invariant over the root file-system describes the bogus
+  situation in an abstract manner: located at a certain @{term path} within
+  the file-system is a non-empty directory that is neither owned nor writable
+  by @{term user\<^sub>1}.
\<close>

definition
@@ -851,35 +834,29 @@
access root path user\<^sub>1 {Writable} = None)"

text \<open>
-  Following the general procedure (see
-  \secref{sec:unix-inv-procedure}) we will now establish the three key
-  lemmas required to yield the final result.
-
-  \begin{enumerate}
+  Following the general procedure (see \secref{sec:unix-inv-procedure}) we
+  will now establish the three key lemmas required to yield the final result.

-  \item The invariant is sufficiently strong to entail the
-  pathological case that @{term user\<^sub>1} is unable to remove the
-  (owned) directory at @{term "[user\<^sub>1, name\<^sub>1]"}.
+    \<^enum> The invariant is sufficiently strong to entail the pathological case
+    that @{term user\<^sub>1} is unable to remove the (owned) directory at @{term
+    "[user\<^sub>1, name\<^sub>1]"}.

-  \item The invariant does hold after having executed the @{term
-  bogus} list of operations (starting with an initial file-system
-  configuration).
+    \<^enum> The invariant does hold after having executed the @{term bogus} list of
+    operations (starting with an initial file-system configuration).

-  \item The invariant is preserved by any file-system operation
-  performed by @{term user\<^sub>1} alone, without any help by other
-  users.
-
-  \end{enumerate}
+    \<^enum> The invariant is preserved by any file-system operation performed by
+    @{term user\<^sub>1} alone, without any help by other users.

-  As the invariant appears both as assumptions and conclusions in the
-  course of proof, its formulation is rather critical for the whole
-  development to work out properly.  In particular, the third step is
-  very sensitive to the invariant being either too strong or too weak.
-  Moreover the invariant has to be sufficiently abstract, lest the
-  proof become cluttered by confusing detail.
+  As the invariant appears both as assumptions and conclusions in the course
+  of proof, its formulation is rather critical for the whole development to
+  work out properly. In particular, the third step is very sensitive to the
+  invariant being either too strong or too weak. Moreover the invariant has to
+  be sufficiently abstract, lest the proof become cluttered by confusing
+  detail.

-  \medskip The first two lemmas are technically straight forward ---
-  we just have to inspect rather special cases.
+  \<^medskip>
+  The first two lemmas are technically straight forward --- we just have to
+  inspect rather special cases.
\<close>

lemma cannot_rmdir:
@@ -906,19 +883,19 @@
apply (unfold bogus_def bogus_path_def)
apply (drule transitions_consD, rule transition.intros,
-    -- "evaluate all operations"
+    \<comment> "evaluate all operations"
apply (drule transitions_nilD)
-    -- "reach final result"
+    \<comment> "reach final result"
-    -- "check the invariant"
+    \<comment> "check the invariant"
done

text \<open>
-  \medskip At last we are left with the main effort to show that the
-  bogosity'' invariant is preserved by any file-system operation
-  performed by @{term user\<^sub>1} alone.  Note that this holds for
-  any @{term path} given, the particular @{term bogus_path} is not
-  required here.
+  \<^medskip>
+  At last we are left with the main effort to show that the bogosity''
+  invariant is preserved by any file-system operation performed by @{term
+  user\<^sub>1} alone. Note that this holds for any @{term path} given, the
+  particular @{term bogus_path} is not required here.
\<close>

lemma preserve_invariant:
@@ -1059,9 +1036,9 @@
subsection \<open>Putting it all together \label{sec:unix-main-result}\<close>

text \<open>
-  The main result is now imminent, just by composing the three
-  invariance lemmas (see \secref{sec:unix-inv-lemmas}) according the the
-  overall procedure (see \secref{sec:unix-inv-procedure}).
+  The main result is now imminent, just by composing the three invariance
+  lemmas (see \secref{sec:unix-inv-lemmas}) according the the overall
+  procedure (see \secref{sec:unix-inv-procedure}).
\<close>

corollary