tuned whitespace;
authorwenzelm
Sun Mar 24 17:23:48 2019 +0100 (3 weeks ago)
changeset 69964699ffc7cbab8
parent 69963 396e0120f7b8
child 69965 da5e7278286b
tuned whitespace;
src/HOL/Unix/Unix.thy
     1.1 --- a/src/HOL/Unix/Unix.thy	Sun Mar 24 17:19:30 2019 +0100
     1.2 +++ b/src/HOL/Unix/Unix.thy	Sun Mar 24 17:23:48 2019 +0100
     1.3 @@ -93,8 +93,9 @@
     1.4    as ``binaries''), or control actual lookup of directory entries (recall that
     1.5    mere directory browsing is controlled via \<^term>\<open>Readable\<close>). Note that the
     1.6    latter means that in order to perform any file-system operation whatsoever,
     1.7 -  all directories encountered on the path would have to grant \<^term>\<open>Executable\<close>. We ignore this detail and pretend that all directories give
     1.8 -  \<^term>\<open>Executable\<close> permission to anybody.
     1.9 +  all directories encountered on the path would have to grant
    1.10 +  \<^term>\<open>Executable\<close>. We ignore this detail and pretend that all directories
    1.11 +  give \<^term>\<open>Executable\<close> permission to anybody.
    1.12  \<close>
    1.13  
    1.14  
    1.15 @@ -115,10 +116,11 @@
    1.16    \<^medskip>
    1.17  
    1.18    Here the parameter \<^typ>\<open>'a\<close> refers to plain values occurring at leaf
    1.19 -  positions, parameter \<^typ>\<open>'b\<close> to information kept with inner branch nodes,
    1.20 -  and parameter \<^typ>\<open>'c\<close> to the branching type of the tree structure. For our
    1.21 -  purpose we use the type instance with \<^typ>\<open>att \<times> string\<close> (representing
    1.22 -  plain files), \<^typ>\<open>att\<close> (for attributes of directory nodes), and \<^typ>\<open>name\<close> (for the index type of directory nodes).
    1.23 +  positions, parameter \<^typ>\<open>'b\<close> to information kept with inner branch
    1.24 +  nodes, and parameter \<^typ>\<open>'c\<close> to the branching type of the tree
    1.25 +  structure. For our purpose we use the type instance with \<^typ>\<open>att \<times>
    1.26 +  string\<close> (representing plain files), \<^typ>\<open>att\<close> (for attributes of
    1.27 +  directory nodes), and \<^typ>\<open>name\<close> (for the index type of directory nodes).
    1.28  \<close>
    1.29  
    1.30  type_synonym "file" = "(att \<times> string, att, name) env"
    1.31 @@ -226,7 +228,8 @@
    1.32    \<^medskip>
    1.33    Successful access to a certain file is the main prerequisite for
    1.34    system-calls to be applicable (cf.\ \secref{sec:unix-trans}). Any
    1.35 -  modification of the file-system is then performed using the basic \<^term>\<open>update\<close> operation.
    1.36 +  modification of the file-system is then performed using the basic
    1.37 +  \<^term>\<open>update\<close> operation.
    1.38  
    1.39    \<^medskip>
    1.40    We see that \<^term>\<open>access\<close> is just a wrapper for the basic \<^term>\<open>lookup\<close>
    1.41 @@ -396,11 +399,11 @@
    1.42  
    1.43  text \<open>
    1.44    The transition system \<open>root \<midarrow>x\<rightarrow> root'\<close> defined above determines a unique
    1.45 -  result \<^term>\<open>root'\<close> from given \<^term>\<open>root\<close> and \<^term>\<open>x\<close> (this is holds
    1.46 -  rather trivially, since there is even only one clause for each operation).
    1.47 -  This uniqueness statement will simplify our subsequent development to some
    1.48 -  extent, since we only have to reason about a partial function rather than a
    1.49 -  general relation.
    1.50 +  result \<^term>\<open>root'\<close> from given \<^term>\<open>root\<close> and \<^term>\<open>x\<close> (this is
    1.51 +  holds rather trivially, since there is even only one clause for each
    1.52 +  operation). This uniqueness statement will simplify our subsequent
    1.53 +  development to some extent, since we only have to reason about a partial
    1.54 +  function rather than a general relation.
    1.55  \<close>
    1.56  
    1.57  theorem transition_uniq:
    1.58 @@ -531,7 +534,8 @@
    1.59    \<^medskip>
    1.60    The following fact shows how an invariant \<^term>\<open>Q\<close> of single transitions
    1.61    with property \<^term>\<open>P\<close> may be transferred to iterated transitions. The
    1.62 -  proof is rather obvious by rule induction over the definition of \<^term>\<open>root \<Midarrow>xs\<Rightarrow> root'\<close>.
    1.63 +  proof is rather obvious by rule induction over the definition of
    1.64 +  \<^term>\<open>root \<Midarrow>xs\<Rightarrow> root'\<close>.
    1.65  \<close>
    1.66  
    1.67  lemma transitions_invariant:
    1.68 @@ -827,7 +831,8 @@
    1.69    will now establish the three key lemmas required to yield the final result.
    1.70  
    1.71      \<^enum> The invariant is sufficiently strong to entail the pathological case
    1.72 -    that \<^term>\<open>user\<^sub>1\<close> is unable to remove the (owned) directory at \<^term>\<open>[user\<^sub>1, name\<^sub>1]\<close>.
    1.73 +    that \<^term>\<open>user\<^sub>1\<close> is unable to remove the (owned) directory at
    1.74 +    \<^term>\<open>[user\<^sub>1, name\<^sub>1]\<close>.
    1.75  
    1.76      \<^enum> The invariant does hold after having executed the \<^term>\<open>bogus\<close> list of
    1.77      operations (starting with an initial file-system configuration).
    1.78 @@ -880,8 +885,9 @@
    1.79  text \<open>
    1.80    \<^medskip>
    1.81    At last we are left with the main effort to show that the ``bogosity''
    1.82 -  invariant is preserved by any file-system operation performed by \<^term>\<open>user\<^sub>1\<close> alone. Note that this holds for any \<^term>\<open>path\<close> given, the
    1.83 -  particular \<^term>\<open>bogus_path\<close> is not required here.
    1.84 +  invariant is preserved by any file-system operation performed by
    1.85 +  \<^term>\<open>user\<^sub>1\<close> alone. Note that this holds for any \<^term>\<open>path\<close> given,
    1.86 +  the particular \<^term>\<open>bogus_path\<close> is not required here.
    1.87  \<close>
    1.88  
    1.89  lemma preserve_invariant: