author wenzelm Sun, 24 Mar 2019 17:23:48 +0100 changeset 70146 699ffc7cbab8 parent 70145 396e0120f7b8 child 70147 da5e7278286b
tuned whitespace;
 src/HOL/Unix/Unix.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Unix/Unix.thy	Sun Mar 24 17:19:30 2019 +0100
+++ b/src/HOL/Unix/Unix.thy	Sun Mar 24 17:23:48 2019 +0100
@@ -93,8 +93,9 @@
as ``binaries''), or control actual lookup of directory entries (recall that
mere directory browsing is controlled via \<^term>\<open>Readable\<close>). 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>\<open>Executable\<close>. We ignore this detail and pretend that all directories give
-  \<^term>\<open>Executable\<close> permission to anybody.
+  all directories encountered on the path would have to grant
+  \<^term>\<open>Executable\<close>. We ignore this detail and pretend that all directories
+  give \<^term>\<open>Executable\<close> permission to anybody.
\<close>

@@ -115,10 +116,11 @@
\<^medskip>

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

type_synonym "file" = "(att \<times> string, att, name) env"
@@ -226,7 +228,8 @@
\<^medskip>
system-calls to be applicable (cf.\ \secref{sec:unix-trans}). Any
-  modification of the file-system is then performed using the basic \<^term>\<open>update\<close> operation.
+  modification of the file-system is then performed using the basic
+  \<^term>\<open>update\<close> operation.

\<^medskip>
We see that \<^term>\<open>access\<close> is just a wrapper for the basic \<^term>\<open>lookup\<close>
@@ -396,11 +399,11 @@

text \<open>
The transition system \<open>root \<midarrow>x\<rightarrow> root'\<close> defined above determines a unique
-  result \<^term>\<open>root'\<close> from given \<^term>\<open>root\<close> and \<^term>\<open>x\<close> (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.
+  result \<^term>\<open>root'\<close> from given \<^term>\<open>root\<close> and \<^term>\<open>x\<close> (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:
@@ -531,7 +534,8 @@
\<^medskip>
The following fact shows how an invariant \<^term>\<open>Q\<close> of single transitions
with property \<^term>\<open>P\<close> may be transferred to iterated transitions. The
-  proof is rather obvious by rule induction over the definition of \<^term>\<open>root \<Midarrow>xs\<Rightarrow> root'\<close>.
+  proof is rather obvious by rule induction over the definition of
+  \<^term>\<open>root \<Midarrow>xs\<Rightarrow> root'\<close>.
\<close>

lemma transitions_invariant:
@@ -827,7 +831,8 @@
will now establish the three key lemmas required to yield the final result.

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

\<^enum> The invariant does hold after having executed the \<^term>\<open>bogus\<close> list of
operations (starting with an initial file-system configuration).
@@ -880,8 +885,9 @@
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>\<open>user\<^sub>1\<close> alone. Note that this holds for any \<^term>\<open>path\<close> given, the
-  particular \<^term>\<open>bogus_path\<close> is not required here.
+  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 particular \<^term>\<open>bogus_path\<close> is not required here.
\<close>

lemma preserve_invariant:```