# HG changeset patch
# User wenzelm
# Date 1126958551 -7200
# Node ID 151e76f0e3c78d7c41c7b5732b928349e2bd5be4
# Parent  a9adc5099c437ba839ea4a8b0f97e39ebf0d87db
tuned document;

diff -r a9adc5099c43 -r 151e76f0e3c7 src/HOL/Unix/Unix.thy
--- a/src/HOL/Unix/Unix.thy	Sat Sep 17 12:51:03 2005 +0200
+++ b/src/HOL/Unix/Unix.thy	Sat Sep 17 14:02:31 2005 +0200
@@ -5,7 +5,9 @@
 
 header {* Unix file-systems \label{sec:unix-file-system} *}
 
-theory Unix imports Nested_Environment List_Prefix begin
+theory Unix
+imports Nested_Environment List_Prefix
+begin
 
 text {*
   We give a simple mathematical model of the basic structures
@@ -463,7 +465,7 @@
     with root show ?thesis by cases auto
   next
     case readdir
-    with root show ?thesis by cases (simp (asm_lr))+
+    with root show ?thesis by cases fastsimp+
   qed
 qed
 
@@ -626,14 +628,13 @@
 section {* Executable sequences *}
 
 text {*
-  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 @{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.
 
   \medskip Subsequently, we explore our transition system in an
   experimental style, mainly using the introduction rules with basic
@@ -755,27 +756,27 @@
   apply (rule can_exec_nil)
   done
 
-theorem "u \<in> users \<Longrightarrow> Writable \<in> perms1 \<Longrightarrow>
-  Readable \<in> perms2 \<Longrightarrow> name3 \<noteq> name4 \<Longrightarrow>
+theorem "u \<in> users \<Longrightarrow> Writable \<in> perms\<^isub>1 \<Longrightarrow>
+  Readable \<in> perms\<^isub>2 \<Longrightarrow> name\<^isub>3 \<noteq> name\<^isub>4 \<Longrightarrow>
   can_exec (init users)
-   [Mkdir u perms1 [u, name1],
-    Mkdir u' perms2 [u, name1, name2],
-    Creat u' perms3 [u, name1, name2, name3],
-    Creat u' perms3 [u, name1, name2, name4],
-    Readdir u {name3, name4} [u, name1, name2]]"
+   [Mkdir u perms\<^isub>1 [u, name\<^isub>1],
+    Mkdir u' perms\<^isub>2 [u, name\<^isub>1, name\<^isub>2],
+    Creat u' perms\<^isub>3 [u, name\<^isub>1, name\<^isub>2, name\<^isub>3],
+    Creat u' perms\<^isub>3 [u, name\<^isub>1, name\<^isub>2, name\<^isub>4],
+    Readdir u {name\<^isub>3, name\<^isub>4} [u, name\<^isub>1, name\<^isub>2]]"
   apply (rule can_exec_cons, rule transition.intros,
     (force simp add: eval)+, (simp add: eval)?)+
   txt {* peek at result: @{subgoals [display]} *}
   apply (rule can_exec_nil)
   done
 
-theorem "u \<in> users \<Longrightarrow> Writable \<in> perms1 \<Longrightarrow> Readable \<in> perms3 \<Longrightarrow>
+theorem "u \<in> users \<Longrightarrow> Writable \<in> perms\<^isub>1 \<Longrightarrow> Readable \<in> perms\<^isub>3 \<Longrightarrow>
   can_exec (init users)
-   [Mkdir u perms1 [u, name1],
-    Mkdir u' perms2 [u, name1, name2],
-    Creat u' perms3 [u, name1, name2, name3],
-    Write u' ''foo'' [u, name1, name2, name3],
-    Read u ''foo'' [u, name1, name2, name3]]"
+   [Mkdir u perms\<^isub>1 [u, name\<^isub>1],
+    Mkdir u' perms\<^isub>2 [u, name\<^isub>1, name\<^isub>2],
+    Creat u' perms\<^isub>3 [u, name\<^isub>1, name\<^isub>2, name\<^isub>3],
+    Write u' ''foo'' [u, name\<^isub>1, name\<^isub>2, name\<^isub>3],
+    Read u ''foo'' [u, name\<^isub>1, name\<^isub>2, name\<^isub>3]]"
   apply (rule can_exec_cons, rule transition.intros,
     (force simp add: eval)+, (simp add: eval)?)+
   txt {* peek at result: @{subgoals [display]} *}
@@ -831,12 +832,12 @@
   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 = user1"} 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}).
+  become @{prop "uid_of x = user\<^isub>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}).
 *}
 
 
@@ -850,28 +851,28 @@
 
 locale situation =
   fixes users :: "uid set"
-    and user1 :: uid
-    and user2 :: uid
-    and name1 :: name
-    and name2 :: name
-    and name3 :: name
-    and perms1 :: perms
-    and perms2 :: perms
-  assumes user1_known: "user1 \<in> users"
-    and user1_not_root: "user1 \<noteq> 0"
-    and users_neq: "user1 \<noteq> user2"
-    and perms1_writable: "Writable \<in> perms1"
-    and perms2_not_writable: "Writable \<notin> perms2"
-  notes facts = user1_known user1_not_root users_neq
-    perms1_writable perms2_not_writable
+    and user\<^isub>1 :: uid
+    and user\<^isub>2 :: uid
+    and name\<^isub>1 :: name
+    and name\<^isub>2 :: name
+    and name\<^isub>3 :: name
+    and perms\<^isub>1 :: perms
+    and perms\<^isub>2 :: perms
+  assumes user\<^isub>1_known: "user\<^isub>1 \<in> users"
+    and user\<^isub>1_not_root: "user\<^isub>1 \<noteq> 0"
+    and users_neq: "user\<^isub>1 \<noteq> user\<^isub>2"
+    and perms\<^isub>1_writable: "Writable \<in> perms\<^isub>1"
+    and perms\<^isub>2_not_writable: "Writable \<notin> perms\<^isub>2"
+  notes facts = user\<^isub>1_known user\<^isub>1_not_root users_neq
+    perms\<^isub>1_writable perms\<^isub>2_not_writable
 
   fixes bogus :: "operation list"
     and bogus_path :: path
   defines "bogus \<equiv>
-     [Mkdir user1 perms1 [user1, name1],
-      Mkdir user2 perms2 [user1, name1, name2],
-      Creat user2 perms2 [user1, name1, name2, name3]]"
-    and "bogus_path \<equiv> [user1, name1, name2]"
+     [Mkdir user\<^isub>1 perms\<^isub>1 [user\<^isub>1, name\<^isub>1],
+      Mkdir user\<^isub>2 perms\<^isub>2 [user\<^isub>1, name\<^isub>1, name\<^isub>2],
+      Creat user\<^isub>2 perms\<^isub>2 [user\<^isub>1, name\<^isub>1, name\<^isub>2, name\<^isub>3]]"
+    and "bogus_path \<equiv> [user\<^isub>1, name\<^isub>1, name\<^isub>2]"
 
 text {*
   The @{term bogus} operations are the ones that lead into the uncouth
@@ -886,35 +887,35 @@
   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 and nor writable by @{term user1}.
+  neither owned and nor writable by @{term user\<^isub>1}.
 *}
 
 locale invariant = situation +
   fixes invariant :: "file \<Rightarrow> path \<Rightarrow> bool"
   defines "invariant root path \<equiv>
     (\<exists>att dir.
-      access root path user1 {} = Some (Env att dir) \<and> dir \<noteq> empty \<and>
-      user1 \<noteq> owner att \<and>
-      access root path user1 {Writable} = None)"
+      access root path user\<^isub>1 {} = Some (Env att dir) \<and> dir \<noteq> empty \<and>
+      user\<^isub>1 \<noteq> owner att \<and>
+      access root path user\<^isub>1 {Writable} = None)"
 
 text {*
   Following the general procedure (see
-  \secref{sec:unix-inv-procedure}) we
-  will now establish the three key lemmas required to yield the final
-  result.
+  \secref{sec:unix-inv-procedure}) we will now establish the three key
+  lemmas required to yield the final result.
 
   \begin{enumerate}
 
   \item The invariant is sufficiently strong to entail the
-  pathological case that @{term user1} is unable to remove the (owned)
-  directory at @{term "[user1, name1]"}.
+  pathological case that @{term user\<^isub>1} is unable to remove the
+  (owned) directory at @{term "[user\<^isub>1, name\<^isub>1]"}.
 
   \item 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 user1} alone, without any help by other users.
+  performed by @{term user\<^isub>1} alone, without any help by other
+  users.
 
   \end{enumerate}
 
@@ -931,17 +932,17 @@
 
 lemma (in invariant)
   cannot_rmdir: "invariant root bogus_path \<Longrightarrow>
-    root \<midarrow>(Rmdir user1 [user1, name1])\<rightarrow> root' \<Longrightarrow> False"
+    root \<midarrow>(Rmdir user\<^isub>1 [user\<^isub>1, name\<^isub>1])\<rightarrow> root' \<Longrightarrow> False"
 proof -
   assume "invariant root bogus_path"
-  then obtain "file" where "access root bogus_path user1 {} = Some file"
+  then obtain "file" where "access root bogus_path user\<^isub>1 {} = Some file"
     by (unfold invariant_def) blast
   moreover
-  assume "root \<midarrow>(Rmdir user1 [user1, name1])\<rightarrow> root'"
+  assume "root \<midarrow>(Rmdir user\<^isub>1 [user\<^isub>1, name\<^isub>1])\<rightarrow> root'"
   then obtain att where
-      "access root [user1, name1] user1 {} = Some (Env att empty)"
+      "access root [user\<^isub>1, name\<^isub>1] user\<^isub>1 {} = Some (Env att empty)"
     by cases auto
-  hence "access root ([user1, name1] @ [name2]) user1 {} = empty name2"
+  hence "access root ([user\<^isub>1, name\<^isub>1] @ [name\<^isub>2]) user\<^isub>1 {} = empty name\<^isub>2"
     by (simp only: access_empty_lookup lookup_append_some) simp
   ultimately show False by (simp add: bogus_path_def)
 qed
@@ -965,30 +966,30 @@
 text {*
   \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 user1} alone.  Note that this holds for any
-  @{term path} given, the particular @{term bogus_path} is not
+  performed by @{term user\<^isub>1} alone.  Note that this holds for
+  any @{term path} given, the particular @{term bogus_path} is not
   required here.
 *}
 
 lemma (in invariant)
   preserve_invariant: "root \<midarrow>x\<rightarrow> root' \<Longrightarrow>
-    invariant root path \<Longrightarrow> uid_of x = user1 \<Longrightarrow> invariant root' path"
+    invariant root path \<Longrightarrow> uid_of x = user\<^isub>1 \<Longrightarrow> invariant root' path"
 proof -
   assume tr: "root \<midarrow>x\<rightarrow> root'"
   assume inv: "invariant root path"
-  assume uid: "uid_of x = user1"
+  assume uid: "uid_of x = user\<^isub>1"
 
   from inv obtain att dir where
-      inv1: "access root path user1 {} = Some (Env att dir)" and
+      inv1: "access root path user\<^isub>1 {} = Some (Env att dir)" and
       inv2: "dir \<noteq> empty" and
-      inv3: "user1 \<noteq> owner att" and
-      inv4: "access root path user1 {Writable} = None"
+      inv3: "user\<^isub>1 \<noteq> owner att" and
+      inv4: "access root path user\<^isub>1 {Writable} = None"
     by (auto simp add: invariant_def)
 
   from inv1 have lookup: "lookup root path = Some (Env att dir)"
     by (simp only: access_empty_lookup)
 
-  from inv1 inv3 inv4 and user1_not_root
+  from inv1 inv3 inv4 and user\<^isub>1_not_root
   have not_writable: "Writable \<notin> others att"
     by (auto simp add: access_def split: option.splits if_splits)
 
@@ -1004,7 +1005,7 @@
     proof (rule prefix_cases)
       assume "path_of x \<parallel> path"
       with inv root'
-      have "\<And>perms. access root' path user1 perms = access root path user1 perms"
+      have "\<And>perms. access root' path user\<^isub>1 perms = access root path user\<^isub>1 perms"
         by (simp only: access_update_other)
       with inv show "invariant root' path"
         by (simp only: invariant_def)
@@ -1015,7 +1016,7 @@
       show ?thesis
       proof (cases ys)
         assume "ys = []"
-        with tr uid inv2 inv3 lookup changed path and user1_not_root
+        with tr uid inv2 inv3 lookup changed path and user\<^isub>1_not_root
         have False
           by cases (auto simp add: access_empty_lookup dest: access_some_lookup)
         thus ?thesis ..
@@ -1095,11 +1096,11 @@
         ultimately show ?thesis ..
       qed
 
-      from lookup' have inv1': "access root' path user1 {} = Some (Env att dir')"
+      from lookup' have inv1': "access root' path user\<^isub>1 {} = Some (Env att dir')"
         by (simp only: access_empty_lookup)
 
-      from inv3 lookup' and not_writable user1_not_root
-      have "access root' path user1 {Writable} = None"
+      from inv3 lookup' and not_writable user\<^isub>1_not_root
+      have "access root' path user\<^isub>1 {Writable} = None"
         by (simp add: access_def)
       with inv1' inv2' inv3 show ?thesis by (unfold invariant_def) blast
     qed
@@ -1118,8 +1119,8 @@
 corollary result:
   includes invariant
   assumes bogus: "init users =bogus\<Rightarrow> root"
-  shows "\<not> (\<exists>xs. (\<forall>x \<in> set xs. uid_of x = user1) \<and>
-    can_exec root (xs @ [Rmdir user1 [user1, name1]]))"
+  shows "\<not> (\<exists>xs. (\<forall>x \<in> set xs. uid_of x = user\<^isub>1) \<and>
+    can_exec root (xs @ [Rmdir user\<^isub>1 [user\<^isub>1, name\<^isub>1]]))"
 proof -
   from cannot_rmdir init_invariant preserve_invariant
     and bogus show ?thesis by (rule general_procedure)
@@ -1128,7 +1129,8 @@
 text {*
   So this is our final result:
 
-  @{thm [display] result [OF invariant.intro, OF situation.intro, no_vars]}
+  @{thm [display, show_question_marks = false] result [OF
+  invariant.intro, OF situation.intro]}
 *}
 
 end