replaced attributes_update by map_attributes;
authorwenzelm
Thu Oct 12 22:57:24 2006 +0200 (2006-10-12)
changeset 21001408f3a1cef2e
parent 21000 54c42dfbcafa
child 21002 c879f0150db9
replaced attributes_update by map_attributes;
src/HOL/Unix/Unix.thy
     1.1 --- a/src/HOL/Unix/Unix.thy	Thu Oct 12 22:57:20 2006 +0200
     1.2 +++ b/src/HOL/Unix/Unix.thy	Thu Oct 12 22:57:24 2006 +0200
     1.3 @@ -166,10 +166,10 @@
     1.4        Val (att, text) \<Rightarrow> att
     1.5      | Env att dir \<Rightarrow> att)"
     1.6  
     1.7 -  "attributes_update att file =
     1.8 +  "map_attributes f file =
     1.9      (case file of
    1.10 -      Val (att', text) \<Rightarrow> Val (att, text)
    1.11 -    | Env att' dir \<Rightarrow> Env att dir)"
    1.12 +      Val (att, text) \<Rightarrow> Val (f att, text)
    1.13 +    | Env att dir \<Rightarrow> Env (f att) dir)"
    1.14  
    1.15  lemma [simp]: "attributes (Val (att, text)) = att"
    1.16    by (simp add: attributes_def)
    1.17 @@ -177,15 +177,15 @@
    1.18  lemma [simp]: "attributes (Env att dir) = att"
    1.19    by (simp add: attributes_def)
    1.20  
    1.21 -lemma [simp]: "attributes (file \<lparr>attributes := att\<rparr>) = att"
    1.22 -  by (cases "file") (simp_all add: attributes_def attributes_update_def
    1.23 +lemma [simp]: "attributes (map_attributes f file) = f (attributes file)"
    1.24 +  by (cases "file") (simp_all add: attributes_def map_attributes_def
    1.25      split_tupled_all)
    1.26  
    1.27 -lemma [simp]: "(Val (att, text)) \<lparr>attributes := att'\<rparr> = Val (att', text)"
    1.28 -  by (simp add: attributes_update_def)
    1.29 +lemma [simp]: "map_attributes f (Val (att, text)) = Val (f att, text)"
    1.30 +  by (simp add: map_attributes_def)
    1.31  
    1.32 -lemma [simp]: "(Env att dir) \<lparr>attributes := att'\<rparr> = Env att' dir"
    1.33 -  by (simp add: attributes_update_def)
    1.34 +lemma [simp]: "map_attributes f (Env att dir) = Env (f att) dir"
    1.35 +  by (simp add: map_attributes_def)
    1.36  
    1.37  
    1.38  subsection {* Initial file-systems *}
    1.39 @@ -370,7 +370,7 @@
    1.40      "access root path uid {} = Some file \<Longrightarrow>
    1.41        uid = 0 \<or> uid = owner (attributes file) \<Longrightarrow>
    1.42        root \<midarrow>(Chmod uid perms path)\<rightarrow> update path
    1.43 -        (Some (file \<lparr>attributes := attributes file \<lparr>others := perms\<rparr>\<rparr>)) root"
    1.44 +        (Some (map_attributes (others_update perms) file)) root"
    1.45  
    1.46    creat:
    1.47      "path = parent_path @ [name] \<Longrightarrow>