--- a/src/HOL/Unix/Nested_Environment.thy Tue Aug 30 17:02:06 2011 +0200
+++ b/src/HOL/Unix/Nested_Environment.thy Tue Aug 30 17:36:12 2011 +0200
@@ -43,9 +43,9 @@
@{term None}.
*}
-primrec
- lookup :: "('a, 'b, 'c) env => 'c list => ('a, 'b, 'c) env option"
- and lookup_option :: "('a, 'b, 'c) env option => 'c list => ('a, 'b, 'c) env option" where
+primrec lookup :: "('a, 'b, 'c) env => 'c list => ('a, 'b, 'c) env option"
+ and lookup_option :: "('a, 'b, 'c) env option => 'c list => ('a, 'b, 'c) env option"
+where
"lookup (Val a) xs = (if xs = [] then Some (Val a) else None)"
| "lookup (Env b es) xs =
(case xs of
@@ -245,22 +245,22 @@
environment is left unchanged.
*}
-primrec
- update :: "'c list => ('a, 'b, 'c) env option
- => ('a, 'b, 'c) env => ('a, 'b, 'c) env"
- and update_option :: "'c list => ('a, 'b, 'c) env option
- => ('a, 'b, 'c) env option => ('a, 'b, 'c) env option" where
- "update xs opt (Val a) =
- (if xs = [] then (case opt of None => Val a | Some e => e)
- else Val a)"
- | "update xs opt (Env b es) =
- (case xs of
- [] => (case opt of None => Env b es | Some e => e)
- | y # ys => Env b (es (y := update_option ys opt (es y))))"
- | "update_option xs opt None =
- (if xs = [] then opt else None)"
- | "update_option xs opt (Some e) =
- (if xs = [] then opt else Some (update xs opt e))"
+primrec update :: "'c list => ('a, 'b, 'c) env option =>
+ ('a, 'b, 'c) env => ('a, 'b, 'c) env"
+ and update_option :: "'c list => ('a, 'b, 'c) env option =>
+ ('a, 'b, 'c) env option => ('a, 'b, 'c) env option"
+where
+ "update xs opt (Val a) =
+ (if xs = [] then (case opt of None => Val a | Some e => e)
+ else Val a)"
+| "update xs opt (Env b es) =
+ (case xs of
+ [] => (case opt of None => Env b es | Some e => e)
+ | y # ys => Env b (es (y := update_option ys opt (es y))))"
+| "update_option xs opt None =
+ (if xs = [] then opt else None)"
+| "update_option xs opt (Some e) =
+ (if xs = [] then opt else Some (update xs opt e))"
hide_const update_option
--- a/src/HOL/Unix/Unix.thy Tue Aug 30 17:02:06 2011 +0200
+++ b/src/HOL/Unix/Unix.thy Tue Aug 30 17:36:12 2011 +0200
@@ -302,8 +302,7 @@
to all kinds of system-calls.
*}
-primrec
- uid_of :: "operation \<Rightarrow> uid"
+primrec uid_of :: "operation \<Rightarrow> uid"
where
"uid_of (Read uid text path) = uid"
| "uid_of (Write uid text path) = uid"
@@ -314,8 +313,7 @@
| "uid_of (Rmdir uid path) = uid"
| "uid_of (Readdir uid names path) = uid"
-primrec
- path_of :: "operation \<Rightarrow> path"
+primrec path_of :: "operation \<Rightarrow> path"
where
"path_of (Read uid text path) = path"
| "path_of (Write uid text path) = path"
@@ -349,11 +347,9 @@
involved here).
*}
-inductive
- transition :: "file \<Rightarrow> operation \<Rightarrow> file \<Rightarrow> bool"
- ("_ \<midarrow>_\<rightarrow> _" [90, 1000, 90] 100)
+inductive transition :: "file \<Rightarrow> operation \<Rightarrow> file \<Rightarrow> bool"
+ ("_ \<midarrow>_\<rightarrow> _" [90, 1000, 90] 100)
where
-
read:
"access root path uid {Readable} = Some (Val (att, text)) \<Longrightarrow>
root \<midarrow>(Read uid text path)\<rightarrow> root" |
@@ -500,9 +496,8 @@
amount of time.
*}
-inductive
- transitions :: "file \<Rightarrow> operation list \<Rightarrow> file \<Rightarrow> bool"
- ("_ =_\<Rightarrow> _" [90, 1000, 90] 100)
+inductive transitions :: "file \<Rightarrow> operation list \<Rightarrow> file \<Rightarrow> bool"
+ ("_ =_\<Rightarrow> _" [90, 1000, 90] 100)
where
nil: "root =[]\<Rightarrow> root"
| cons: "root \<midarrow>x\<rightarrow> root' \<Longrightarrow> root' =xs\<Rightarrow> root'' \<Longrightarrow> root =(x # xs)\<Rightarrow> root''"
@@ -630,8 +625,7 @@
transition.
*}
-definition
- "can_exec root xs = (\<exists>root'. root =xs\<Rightarrow> root')"
+definition "can_exec root xs = (\<exists>root'. root =xs\<Rightarrow> root')"
lemma can_exec_nil: "can_exec root []"
unfolding can_exec_def by (blast intro: transitions.intros)