1.1 --- a/src/HOL/Unix/Nested_Environment.thy	Tue Aug 30 17:02:06 2011 +0200
     1.2 +++ b/src/HOL/Unix/Nested_Environment.thy	Tue Aug 30 17:36:12 2011 +0200
     1.3 @@ -43,9 +43,9 @@
     1.4    @{term None}.
     1.5  *}
     1.6  
     1.7 -primrec
     1.8 -  lookup :: "('a, 'b, 'c) env => 'c list => ('a, 'b, 'c) env option"
     1.9 -  and lookup_option :: "('a, 'b, 'c) env option => 'c list => ('a, 'b, 'c) env option" where
    1.10 +primrec lookup :: "('a, 'b, 'c) env => 'c list => ('a, 'b, 'c) env option"
    1.11 +  and lookup_option :: "('a, 'b, 'c) env option => 'c list => ('a, 'b, 'c) env option"
    1.12 +where
    1.13      "lookup (Val a) xs = (if xs = [] then Some (Val a) else None)"
    1.14    | "lookup (Env b es) xs =
    1.15        (case xs of
    1.16 @@ -245,22 +245,22 @@
    1.17    environment is left unchanged.
    1.18  *}
    1.19  
    1.20 -primrec
    1.21 -  update :: "'c list => ('a, 'b, 'c) env option
    1.22 -    => ('a, 'b, 'c) env => ('a, 'b, 'c) env"
    1.23 -  and update_option :: "'c list => ('a, 'b, 'c) env option
    1.24 -    => ('a, 'b, 'c) env option => ('a, 'b, 'c) env option" where
    1.25 -    "update xs opt (Val a) =
    1.26 -      (if xs = [] then (case opt of None => Val a | Some e => e)
    1.27 -      else Val a)"
    1.28 -  | "update xs opt (Env b es) =
    1.29 -      (case xs of
    1.30 -        [] => (case opt of None => Env b es | Some e => e)
    1.31 -      | y # ys => Env b (es (y := update_option ys opt (es y))))"
    1.32 -  | "update_option xs opt None =
    1.33 -      (if xs = [] then opt else None)"
    1.34 -  | "update_option xs opt (Some e) =
    1.35 -      (if xs = [] then opt else Some (update xs opt e))"
    1.36 +primrec update :: "'c list => ('a, 'b, 'c) env option =>
    1.37 +    ('a, 'b, 'c) env => ('a, 'b, 'c) env"
    1.38 +  and update_option :: "'c list => ('a, 'b, 'c) env option =>
    1.39 +    ('a, 'b, 'c) env option => ('a, 'b, 'c) env option"
    1.40 +where
    1.41 +  "update xs opt (Val a) =
    1.42 +    (if xs = [] then (case opt of None => Val a | Some e => e)
    1.43 +     else Val a)"
    1.44 +| "update xs opt (Env b es) =
    1.45 +    (case xs of
    1.46 +      [] => (case opt of None => Env b es | Some e => e)
    1.47 +    | y # ys => Env b (es (y := update_option ys opt (es y))))"
    1.48 +| "update_option xs opt None =
    1.49 +    (if xs = [] then opt else None)"
    1.50 +| "update_option xs opt (Some e) =
    1.51 +    (if xs = [] then opt else Some (update xs opt e))"
    1.52  
    1.53  hide_const update_option
    1.54  

     2.1 --- a/src/HOL/Unix/Unix.thy	Tue Aug 30 17:02:06 2011 +0200
     2.2 +++ b/src/HOL/Unix/Unix.thy	Tue Aug 30 17:36:12 2011 +0200
     2.3 @@ -302,8 +302,7 @@
     2.4    to all kinds of system-calls.
     2.5  *}
     2.6  
     2.7 -primrec
     2.8 -  uid_of :: "operation \<Rightarrow> uid"
     2.9 +primrec uid_of :: "operation \<Rightarrow> uid"
    2.10  where
    2.11      "uid_of (Read uid text path) = uid"
    2.12    | "uid_of (Write uid text path) = uid"
    2.13 @@ -314,8 +313,7 @@
    2.14    | "uid_of (Rmdir uid path) = uid"
    2.15    | "uid_of (Readdir uid names path) = uid"
    2.16  
    2.17 -primrec
    2.18 -  path_of :: "operation \<Rightarrow> path"
    2.19 +primrec path_of :: "operation \<Rightarrow> path"
    2.20  where
    2.21      "path_of (Read uid text path) = path"
    2.22    | "path_of (Write uid text path) = path"
    2.23 @@ -349,11 +347,9 @@
    2.24    involved here).
    2.25  *}
    2.26  
    2.27 -inductive
    2.28 -  transition :: "file \<Rightarrow> operation \<Rightarrow> file \<Rightarrow> bool"
    2.29 -    ("_ \<midarrow>_\<rightarrow> _" [90, 1000, 90] 100)
    2.30 +inductive transition :: "file \<Rightarrow> operation \<Rightarrow> file \<Rightarrow> bool"
    2.31 +  ("_ \<midarrow>_\<rightarrow> _" [90, 1000, 90] 100)
    2.32  where
    2.33 -
    2.34    read:
    2.35      "access root path uid {Readable} = Some (Val (att, text)) \<Longrightarrow>
    2.36        root \<midarrow>(Read uid text path)\<rightarrow> root" |
    2.37 @@ -500,9 +496,8 @@
    2.38    amount of time.
    2.39  *}
    2.40  
    2.41 -inductive
    2.42 -  transitions :: "file \<Rightarrow> operation list \<Rightarrow> file \<Rightarrow> bool"
    2.43 -    ("_ =_\<Rightarrow> _" [90, 1000, 90] 100)
    2.44 +inductive transitions :: "file \<Rightarrow> operation list \<Rightarrow> file \<Rightarrow> bool"
    2.45 +  ("_ =_\<Rightarrow> _" [90, 1000, 90] 100)
    2.46  where
    2.47      nil: "root =[]\<Rightarrow> root"
    2.48    | cons: "root \<midarrow>x\<rightarrow> root' \<Longrightarrow> root' =xs\<Rightarrow> root'' \<Longrightarrow> root =(x # xs)\<Rightarrow> root''"
    2.49 @@ -630,8 +625,7 @@
    2.50    transition.
    2.51  *}
    2.52  
    2.53 -definition
    2.54 -  "can_exec root xs = (\<exists>root'. root =xs\<Rightarrow> root')"
    2.55 +definition "can_exec root xs = (\<exists>root'. root =xs\<Rightarrow> root')"
    2.56  
    2.57  lemma can_exec_nil: "can_exec root []"
    2.58    unfolding can_exec_def by (blast intro: transitions.intros)