# HG changeset patch # User wenzelm # Date 1315151419 -7200 # Node ID f2bfe19239bcc015e16ec98f99f5cceb075a02d2 # Parent eb00752507c7be3085b391ccfe111e6cb6e55028 tuned document; diff -r eb00752507c7 -r f2bfe19239bc src/HOL/Unix/Nested_Environment.thy --- a/src/HOL/Unix/Nested_Environment.thy Sun Sep 04 17:35:34 2011 +0200 +++ b/src/HOL/Unix/Nested_Environment.thy Sun Sep 04 17:50:19 2011 +0200 @@ -9,7 +9,7 @@ begin text {* - Consider a partial function @{term [source] "e :: 'a => 'b option"}; + Consider a partial function @{term [source] "e :: 'a \ 'b option"}; this may be understood as an \emph{environment} mapping indexes @{typ 'a} to optional entry values @{typ 'b} (cf.\ the basic theory @{text Map} of Isabelle/HOL). This basic idea is easily generalized @@ -21,7 +21,7 @@ datatype ('a, 'b, 'c) env = Val 'a - | Env 'b "'c => ('a, 'b, 'c) env option" + | Env 'b "'c \ ('a, 'b, 'c) env option" text {* \medskip In the type @{typ "('a, 'b, 'c) env"} the parameter @{typ @@ -43,14 +43,14 @@ @{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" +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 - [] => Some (Env b es) - | y # ys => lookup_option (es y) ys)" + [] \ Some (Env b es) + | y # ys \ lookup_option (es y) ys)" | "lookup_option None xs = None" | "lookup_option (Some e) xs = lookup e xs" @@ -70,8 +70,8 @@ theorem lookup_env_cons: "lookup (Env b es) (x # xs) = (case es x of - None => None - | Some e => lookup e xs)" + None \ None + | Some e \ lookup e xs)" by (cases "es x") simp_all lemmas lookup_lookup_option.simps [simp del] @@ -80,14 +80,14 @@ theorem lookup_eq: "lookup env xs = (case xs of - [] => Some env - | x # xs => + [] \ Some env + | x # xs \ (case env of - Val a => None - | Env b es => + Val a \ None + | Env b es \ (case es x of - None => None - | Some e => lookup e xs)))" + None \ None + | Some e \ lookup e xs)))" by (simp split: list.split env.split) text {* @@ -245,18 +245,18 @@ 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" +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) + (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))))" + [] \ (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) = @@ -286,8 +286,8 @@ "update (x # y # ys) opt (Env b es) = Env b (es (x := (case es x of - None => None - | Some e => Some (update (y # ys) opt e))))" + None \ None + | Some e \ Some (update (y # ys) opt e))))" by (cases "es x") simp_all lemmas update_update_option.simps [simp del] @@ -297,21 +297,21 @@ lemma update_eq: "update xs opt env = (case xs of - [] => + [] \ (case opt of - None => env - | Some e => e) - | x # xs => + None \ env + | Some e \ e) + | x # xs \ (case env of - Val a => Val a - | Env b es => + Val a \ Val a + | Env b es \ (case xs of - [] => Env b (es (x := opt)) - | y # ys => + [] \ Env b (es (x := opt)) + | y # ys \ Env b (es (x := (case es x of - None => None - | Some e => Some (update (y # ys) opt e)))))))" + None \ None + | Some e \ Some (update (y # ys) opt e)))))))" by (simp split: list.split env.split option.split) text {*