tuned document;
authorwenzelm
Sun Sep 04 17:50:19 2011 +0200 (2011-09-04)
changeset 44703f2bfe19239bc
parent 44702 eb00752507c7
child 44704 528d635ef6f0
tuned document;
src/HOL/Unix/Nested_Environment.thy
     1.1 --- a/src/HOL/Unix/Nested_Environment.thy	Sun Sep 04 17:35:34 2011 +0200
     1.2 +++ b/src/HOL/Unix/Nested_Environment.thy	Sun Sep 04 17:50:19 2011 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  begin
     1.5  
     1.6  text {*
     1.7 -  Consider a partial function @{term [source] "e :: 'a => 'b option"};
     1.8 +  Consider a partial function @{term [source] "e :: 'a \<Rightarrow> 'b option"};
     1.9    this may be understood as an \emph{environment} mapping indexes
    1.10    @{typ 'a} to optional entry values @{typ 'b} (cf.\ the basic theory
    1.11    @{text Map} of Isabelle/HOL).  This basic idea is easily generalized
    1.12 @@ -21,7 +21,7 @@
    1.13  
    1.14  datatype ('a, 'b, 'c) env =
    1.15      Val 'a
    1.16 -  | Env 'b  "'c => ('a, 'b, 'c) env option"
    1.17 +  | Env 'b  "'c \<Rightarrow> ('a, 'b, 'c) env option"
    1.18  
    1.19  text {*
    1.20    \medskip In the type @{typ "('a, 'b, 'c) env"} the parameter @{typ
    1.21 @@ -43,14 +43,14 @@
    1.22    @{term None}.
    1.23  *}
    1.24  
    1.25 -primrec lookup :: "('a, 'b, 'c) env => 'c list => ('a, 'b, 'c) env option"
    1.26 -  and lookup_option :: "('a, 'b, 'c) env option => 'c list => ('a, 'b, 'c) env option"
    1.27 +primrec lookup :: "('a, 'b, 'c) env \<Rightarrow> 'c list \<Rightarrow> ('a, 'b, 'c) env option"
    1.28 +  and lookup_option :: "('a, 'b, 'c) env option \<Rightarrow> 'c list \<Rightarrow> ('a, 'b, 'c) env option"
    1.29  where
    1.30      "lookup (Val a) xs = (if xs = [] then Some (Val a) else None)"
    1.31    | "lookup (Env b es) xs =
    1.32        (case xs of
    1.33 -        [] => Some (Env b es)
    1.34 -      | y # ys => lookup_option (es y) ys)"
    1.35 +        [] \<Rightarrow> Some (Env b es)
    1.36 +      | y # ys \<Rightarrow> lookup_option (es y) ys)"
    1.37    | "lookup_option None xs = None"
    1.38    | "lookup_option (Some e) xs = lookup e xs"
    1.39  
    1.40 @@ -70,8 +70,8 @@
    1.41  theorem lookup_env_cons:
    1.42    "lookup (Env b es) (x # xs) =
    1.43      (case es x of
    1.44 -      None => None
    1.45 -    | Some e => lookup e xs)"
    1.46 +      None \<Rightarrow> None
    1.47 +    | Some e \<Rightarrow> lookup e xs)"
    1.48    by (cases "es x") simp_all
    1.49  
    1.50  lemmas lookup_lookup_option.simps [simp del]
    1.51 @@ -80,14 +80,14 @@
    1.52  theorem lookup_eq:
    1.53    "lookup env xs =
    1.54      (case xs of
    1.55 -      [] => Some env
    1.56 -    | x # xs =>
    1.57 +      [] \<Rightarrow> Some env
    1.58 +    | x # xs \<Rightarrow>
    1.59        (case env of
    1.60 -        Val a => None
    1.61 -      | Env b es =>
    1.62 +        Val a \<Rightarrow> None
    1.63 +      | Env b es \<Rightarrow>
    1.64            (case es x of
    1.65 -            None => None
    1.66 -          | Some e => lookup e xs)))"
    1.67 +            None \<Rightarrow> None
    1.68 +          | Some e \<Rightarrow> lookup e xs)))"
    1.69    by (simp split: list.split env.split)
    1.70  
    1.71  text {*
    1.72 @@ -245,18 +245,18 @@
    1.73    environment is left unchanged.
    1.74  *}
    1.75  
    1.76 -primrec update :: "'c list => ('a, 'b, 'c) env option =>
    1.77 -    ('a, 'b, 'c) env => ('a, 'b, 'c) env"
    1.78 -  and update_option :: "'c list => ('a, 'b, 'c) env option =>
    1.79 -    ('a, 'b, 'c) env option => ('a, 'b, 'c) env option"
    1.80 +primrec update :: "'c list \<Rightarrow> ('a, 'b, 'c) env option \<Rightarrow>
    1.81 +    ('a, 'b, 'c) env \<Rightarrow> ('a, 'b, 'c) env"
    1.82 +  and update_option :: "'c list \<Rightarrow> ('a, 'b, 'c) env option \<Rightarrow>
    1.83 +    ('a, 'b, 'c) env option \<Rightarrow> ('a, 'b, 'c) env option"
    1.84  where
    1.85    "update xs opt (Val a) =
    1.86 -    (if xs = [] then (case opt of None => Val a | Some e => e)
    1.87 +    (if xs = [] then (case opt of None \<Rightarrow> Val a | Some e \<Rightarrow> e)
    1.88       else Val a)"
    1.89  | "update xs opt (Env b es) =
    1.90      (case xs of
    1.91 -      [] => (case opt of None => Env b es | Some e => e)
    1.92 -    | y # ys => Env b (es (y := update_option ys opt (es y))))"
    1.93 +      [] \<Rightarrow> (case opt of None \<Rightarrow> Env b es | Some e \<Rightarrow> e)
    1.94 +    | y # ys \<Rightarrow> Env b (es (y := update_option ys opt (es y))))"
    1.95  | "update_option xs opt None =
    1.96      (if xs = [] then opt else None)"
    1.97  | "update_option xs opt (Some e) =
    1.98 @@ -286,8 +286,8 @@
    1.99    "update (x # y # ys) opt (Env b es) =
   1.100      Env b (es (x :=
   1.101        (case es x of
   1.102 -        None => None
   1.103 -      | Some e => Some (update (y # ys) opt e))))"
   1.104 +        None \<Rightarrow> None
   1.105 +      | Some e \<Rightarrow> Some (update (y # ys) opt e))))"
   1.106    by (cases "es x") simp_all
   1.107  
   1.108  lemmas update_update_option.simps [simp del]
   1.109 @@ -297,21 +297,21 @@
   1.110  lemma update_eq:
   1.111    "update xs opt env =
   1.112      (case xs of
   1.113 -      [] =>
   1.114 +      [] \<Rightarrow>
   1.115          (case opt of
   1.116 -          None => env
   1.117 -        | Some e => e)
   1.118 -    | x # xs =>
   1.119 +          None \<Rightarrow> env
   1.120 +        | Some e \<Rightarrow> e)
   1.121 +    | x # xs \<Rightarrow>
   1.122          (case env of
   1.123 -          Val a => Val a
   1.124 -        | Env b es =>
   1.125 +          Val a \<Rightarrow> Val a
   1.126 +        | Env b es \<Rightarrow>
   1.127              (case xs of
   1.128 -              [] => Env b (es (x := opt))
   1.129 -            | y # ys =>
   1.130 +              [] \<Rightarrow> Env b (es (x := opt))
   1.131 +            | y # ys \<Rightarrow>
   1.132                  Env b (es (x :=
   1.133                    (case es x of
   1.134 -                    None => None
   1.135 -                  | Some e => Some (update (y # ys) opt e)))))))"
   1.136 +                    None \<Rightarrow> None
   1.137 +                  | Some e \<Rightarrow> Some (update (y # ys) opt e)))))))"
   1.138    by (simp split: list.split env.split option.split)
   1.139  
   1.140  text {*