tuned whitespace;
authorwenzelm
Mon Nov 21 14:47:15 2016 +0100 (2016-11-21)
changeset 6451762832c7df18f
parent 64516 2c45b7af9173
child 64518 b87697eec2ac
tuned whitespace;
src/HOL/Unix/Unix.thy
     1.1 --- a/src/HOL/Unix/Unix.thy	Mon Nov 21 10:13:46 2016 +0100
     1.2 +++ b/src/HOL/Unix/Unix.thy	Mon Nov 21 14:47:15 2016 +0100
     1.3 @@ -5,9 +5,9 @@
     1.4  section \<open>Unix file-systems \label{sec:unix-file-system}\<close>
     1.5  
     1.6  theory Unix
     1.7 -imports
     1.8 -  Nested_Environment
     1.9 -  "~~/src/HOL/Library/Sublist"
    1.10 +  imports
    1.11 +    Nested_Environment
    1.12 +    "~~/src/HOL/Library/Sublist"
    1.13  begin
    1.14  
    1.15  text \<open>
    1.16 @@ -296,26 +296,26 @@
    1.17  \<close>
    1.18  
    1.19  primrec uid_of :: "operation \<Rightarrow> uid"
    1.20 -where
    1.21 -  "uid_of (Read uid text path) = uid"
    1.22 -| "uid_of (Write uid text path) = uid"
    1.23 -| "uid_of (Chmod uid perms path) = uid"
    1.24 -| "uid_of (Creat uid perms path) = uid"
    1.25 -| "uid_of (Unlink uid path) = uid"
    1.26 -| "uid_of (Mkdir uid path perms) = uid"
    1.27 -| "uid_of (Rmdir uid path) = uid"
    1.28 -| "uid_of (Readdir uid names path) = uid"
    1.29 +  where
    1.30 +    "uid_of (Read uid text path) = uid"
    1.31 +  | "uid_of (Write uid text path) = uid"
    1.32 +  | "uid_of (Chmod uid perms path) = uid"
    1.33 +  | "uid_of (Creat uid perms path) = uid"
    1.34 +  | "uid_of (Unlink uid path) = uid"
    1.35 +  | "uid_of (Mkdir uid path perms) = uid"
    1.36 +  | "uid_of (Rmdir uid path) = uid"
    1.37 +  | "uid_of (Readdir uid names path) = uid"
    1.38  
    1.39  primrec path_of :: "operation \<Rightarrow> path"
    1.40 -where
    1.41 -  "path_of (Read uid text path) = path"
    1.42 -| "path_of (Write uid text path) = path"
    1.43 -| "path_of (Chmod uid perms path) = path"
    1.44 -| "path_of (Creat uid perms path) = path"
    1.45 -| "path_of (Unlink uid path) = path"
    1.46 -| "path_of (Mkdir uid perms path) = path"
    1.47 -| "path_of (Rmdir uid path) = path"
    1.48 -| "path_of (Readdir uid names path) = path"
    1.49 +  where
    1.50 +    "path_of (Read uid text path) = path"
    1.51 +  | "path_of (Write uid text path) = path"
    1.52 +  | "path_of (Chmod uid perms path) = path"
    1.53 +  | "path_of (Creat uid perms path) = path"
    1.54 +  | "path_of (Unlink uid path) = path"
    1.55 +  | "path_of (Mkdir uid perms path) = path"
    1.56 +  | "path_of (Rmdir uid path) = path"
    1.57 +  | "path_of (Readdir uid names path) = path"
    1.58  
    1.59  text \<open>
    1.60    \<^medskip>
    1.61 @@ -340,45 +340,43 @@
    1.62  
    1.63  inductive transition :: "file \<Rightarrow> operation \<Rightarrow> file \<Rightarrow> bool"
    1.64    ("_ \<midarrow>_\<rightarrow> _" [90, 1000, 90] 100)
    1.65 -where
    1.66 -  read:
    1.67 -    "root \<midarrow>(Read uid text path)\<rightarrow> root"
    1.68 -    if "access root path uid {Readable} = Some (Val (att, text))"
    1.69 -| "write":
    1.70 -    "root \<midarrow>(Write uid text path)\<rightarrow> update path (Some (Val (att, text))) root"
    1.71 -    if "access root path uid {Writable} = Some (Val (att, text'))"
    1.72 -| chmod:
    1.73 -    "root \<midarrow>(Chmod uid perms path)\<rightarrow>
    1.74 -      update path (Some (map_attributes (others_update (\<lambda>_. perms)) file)) root"
    1.75 -    if "access root path uid {} = Some file" and "uid = 0 \<or> uid = owner (attributes file)"
    1.76 -| creat:
    1.77 -    "root \<midarrow>(Creat uid perms path)\<rightarrow>
    1.78 -      update path (Some (Val (\<lparr>owner = uid, others = perms\<rparr>, []))) root"
    1.79 -    if "path = parent_path @ [name]"
    1.80 -    and "access root parent_path uid {Writable} = Some (Env att parent)"
    1.81 -    and "access root path uid {} = None"
    1.82 -| unlink:
    1.83 -    "root \<midarrow>(Unlink uid path)\<rightarrow> update path None root"
    1.84 -    if "path = parent_path @ [name]"
    1.85 -    and "access root parent_path uid {Writable} = Some (Env att parent)"
    1.86 -    and "access root path uid {} = Some (Val plain)"
    1.87 -| mkdir:
    1.88 -    "root \<midarrow>(Mkdir uid perms path)\<rightarrow>
    1.89 -      update path (Some (Env \<lparr>owner = uid, others = perms\<rparr> empty)) root"
    1.90 -    if "path = parent_path @ [name]"
    1.91 -    and "access root parent_path uid {Writable} = Some (Env att parent)"
    1.92 -    and "access root path uid {} = None"
    1.93 -|
    1.94 -  rmdir:
    1.95 -    "root \<midarrow>(Rmdir uid path)\<rightarrow> update path None root"
    1.96 -    if "path = parent_path @ [name]"
    1.97 -    and "access root parent_path uid {Writable} = Some (Env att parent)"
    1.98 -    and "access root path uid {} = Some (Env att' empty)"
    1.99 -|
   1.100 -  readdir:
   1.101 -    "root \<midarrow>(Readdir uid names path)\<rightarrow> root"
   1.102 -    if "access root path uid {Readable} = Some (Env att dir)"
   1.103 -    and "names = dom dir"
   1.104 +  where
   1.105 +    read:
   1.106 +      "root \<midarrow>(Read uid text path)\<rightarrow> root"
   1.107 +      if "access root path uid {Readable} = Some (Val (att, text))"
   1.108 +  | "write":
   1.109 +      "root \<midarrow>(Write uid text path)\<rightarrow> update path (Some (Val (att, text))) root"
   1.110 +      if "access root path uid {Writable} = Some (Val (att, text'))"
   1.111 +  | chmod:
   1.112 +      "root \<midarrow>(Chmod uid perms path)\<rightarrow>
   1.113 +        update path (Some (map_attributes (others_update (\<lambda>_. perms)) file)) root"
   1.114 +      if "access root path uid {} = Some file" and "uid = 0 \<or> uid = owner (attributes file)"
   1.115 +  | creat:
   1.116 +      "root \<midarrow>(Creat uid perms path)\<rightarrow>
   1.117 +        update path (Some (Val (\<lparr>owner = uid, others = perms\<rparr>, []))) root"
   1.118 +      if "path = parent_path @ [name]"
   1.119 +      and "access root parent_path uid {Writable} = Some (Env att parent)"
   1.120 +      and "access root path uid {} = None"
   1.121 +  | unlink:
   1.122 +      "root \<midarrow>(Unlink uid path)\<rightarrow> update path None root"
   1.123 +      if "path = parent_path @ [name]"
   1.124 +      and "access root parent_path uid {Writable} = Some (Env att parent)"
   1.125 +      and "access root path uid {} = Some (Val plain)"
   1.126 +  | mkdir:
   1.127 +      "root \<midarrow>(Mkdir uid perms path)\<rightarrow>
   1.128 +        update path (Some (Env \<lparr>owner = uid, others = perms\<rparr> empty)) root"
   1.129 +      if "path = parent_path @ [name]"
   1.130 +      and "access root parent_path uid {Writable} = Some (Env att parent)"
   1.131 +      and "access root path uid {} = None"
   1.132 +  | rmdir:
   1.133 +      "root \<midarrow>(Rmdir uid path)\<rightarrow> update path None root"
   1.134 +      if "path = parent_path @ [name]"
   1.135 +      and "access root parent_path uid {Writable} = Some (Env att parent)"
   1.136 +      and "access root path uid {} = Some (Env att' empty)"
   1.137 +  | readdir:
   1.138 +      "root \<midarrow>(Readdir uid names path)\<rightarrow> root"
   1.139 +      if "access root path uid {Readable} = Some (Env att dir)"
   1.140 +      and "names = dom dir"
   1.141  
   1.142  text \<open>
   1.143    \<^medskip>
   1.144 @@ -480,11 +478,10 @@
   1.145    running processes over a finite amount of time.
   1.146  \<close>
   1.147  
   1.148 -inductive transitions :: "file \<Rightarrow> operation list \<Rightarrow> file \<Rightarrow> bool"
   1.149 -  ("_ \<Midarrow>_\<Rightarrow> _" [90, 1000, 90] 100)
   1.150 -where
   1.151 -  nil: "root \<Midarrow>[]\<Rightarrow> root"
   1.152 -| cons: "root \<Midarrow>(x # xs)\<Rightarrow> root''" if "root \<midarrow>x\<rightarrow> root'" and "root' \<Midarrow>xs\<Rightarrow> root''"
   1.153 +inductive transitions :: "file \<Rightarrow> operation list \<Rightarrow> file \<Rightarrow> bool"  ("_ \<Midarrow>_\<Rightarrow> _" [90, 1000, 90] 100)
   1.154 +  where
   1.155 +    nil: "root \<Midarrow>[]\<Rightarrow> root"
   1.156 +  | cons: "root \<Midarrow>(x # xs)\<Rightarrow> root''" if "root \<midarrow>x\<rightarrow> root'" and "root' \<Midarrow>xs\<Rightarrow> root''"
   1.157  
   1.158  text \<open>
   1.159    \<^medskip>
   1.160 @@ -750,8 +747,7 @@
   1.161      fix xs
   1.162      assume Ps: "\<forall>x \<in> set xs. P x"
   1.163      assume can_exec: "can_exec root (xs @ [y])"
   1.164 -    then obtain root' root'' where
   1.165 -        xs: "root \<Midarrow>xs\<Rightarrow> root'" and y: "root' \<midarrow>y\<rightarrow> root''"
   1.166 +    then obtain root' root'' where xs: "root \<Midarrow>xs\<Rightarrow> root'" and y: "root' \<midarrow>y\<rightarrow> root''"
   1.167        by (blast dest: can_exec_snocD)
   1.168      from init_result have "Q root" by (rule init_inv)
   1.169      from preserve_inv xs this Ps have "Q root'"
   1.170 @@ -864,8 +860,7 @@
   1.171    from inv obtain "file" where "access root bogus_path user\<^sub>1 {} = Some file"
   1.172      unfolding invariant_def by blast
   1.173    moreover
   1.174 -  from rmdir obtain att where
   1.175 -      "access root [user\<^sub>1, name\<^sub>1] user\<^sub>1 {} = Some (Env att empty)"
   1.176 +  from rmdir obtain att where "access root [user\<^sub>1, name\<^sub>1] user\<^sub>1 {} = Some (Env att empty)"
   1.177      by cases auto
   1.178    then have "access root ([user\<^sub>1, name\<^sub>1] @ [name\<^sub>2]) user\<^sub>1 {} = empty name\<^sub>2"
   1.179      by (simp only: access_empty_lookup lookup_append_some) simp