added HOL/Library/Nested_Environment.thy;
authorwenzelm
Fri Jan 19 23:53:07 2001 +0100 (2001-01-19)
changeset 109433a610d34eb9e
parent 10942 6bbc41330b68
child 10944 710ddb9e8b5e
added HOL/Library/Nested_Environment.thy;
src/HOL/IsaMakefile
src/HOL/Library/Library.thy
src/HOL/Library/Nested_Environment.thy
     1.1 --- a/src/HOL/IsaMakefile	Fri Jan 19 23:28:50 2001 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Fri Jan 19 23:53:07 2001 +0100
     1.3 @@ -179,7 +179,7 @@
     1.4  $(LOG)/HOL-Library.gz: $(OUT)/HOL Library/Accessible_Part.thy \
     1.5    Library/Library.thy Library/List_Prefix.thy Library/Multiset.thy \
     1.6    Library/Quotient.thy Library/Ring_and_Field.thy Library/README.html \
     1.7 -  Library/Rational_Numbers.thy Library/ROOT.ML \
     1.8 +  Library/Nested_Environment.thy Library/Rational_Numbers.thy Library/ROOT.ML \
     1.9    Library/While_Combinator.thy Library/While_Combinator_Example.thy
    1.10  	@$(ISATOOL) usedir $(OUT)/HOL Library
    1.11  
     2.1 --- a/src/HOL/Library/Library.thy	Fri Jan 19 23:28:50 2001 +0100
     2.2 +++ b/src/HOL/Library/Library.thy	Fri Jan 19 23:53:07 2001 +0100
     2.3 @@ -4,6 +4,7 @@
     2.4    Ring_and_Field +
     2.5    Rational_Numbers +
     2.6    List_Prefix +
     2.7 +  Nested_Environment +
     2.8    Accessible_Part +
     2.9    Multiset +
    2.10    While_Combinator + While_Combinator_Example:
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Library/Nested_Environment.thy	Fri Jan 19 23:53:07 2001 +0100
     3.3 @@ -0,0 +1,550 @@
     3.4 +(*  Title:      HOL/Library/Nested_Environment.thy
     3.5 +    ID:         $Id$
     3.6 +    Author:     Markus Wenzel, TU Muenchen
     3.7 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     3.8 +*)
     3.9 +
    3.10 +header {*
    3.11 +  \title{Nested environments}
    3.12 +  \author{Markus Wenzel}
    3.13 +*}
    3.14 +
    3.15 +theory Nested_Environment = Main:
    3.16 +
    3.17 +text {*
    3.18 +  Consider a partial function @{term [source] "e :: 'a => 'b option"};
    3.19 +  this may be understood as an \emph{environment} mapping indexes
    3.20 +  @{typ 'a} to optional entry values @{typ 'b} (cf.\ the basic theory
    3.21 +  @{text
    3.22 +  Map}\footnote{\url{http://isabelle.in.tum.de/library/HOL/Map.html}}
    3.23 +  of Isabelle/HOL).  This basic idea is easily generalized to that of
    3.24 +  a \emph{nested environment}, where entries may be either basic
    3.25 +  values or again proper environments.  Then each entry is accessed by
    3.26 +  a \emph{path}, i.e.\ a list of indexes leading to its position
    3.27 +  within the structure.
    3.28 +*}
    3.29 +
    3.30 +datatype ('a, 'b, 'c) env =
    3.31 +    Val 'a
    3.32 +  | Env 'b  "'c => ('a, 'b, 'c) env option"
    3.33 +
    3.34 +text {*
    3.35 +  \medskip In the type @{typ "('a, 'b, 'c) env"} the parameter @{typ
    3.36 +  'a} refers to basic values (occurring in terminal positions), type
    3.37 +  @{typ 'b} to values associated with proper (inner) environments, and
    3.38 +  type @{typ 'c} with the index type for branching.  Note that there
    3.39 +  is no restriction on any of these types.  In particular, arbitrary
    3.40 +  branching may yield rather large (transfinite) tree structures.
    3.41 +*}
    3.42 +
    3.43 +
    3.44 +subsection {* The lookup operation *}
    3.45 +
    3.46 +text {*
    3.47 +  Lookup in nested environments works by following a given path of
    3.48 +  index elements, leading to an optional result (a terminal value or
    3.49 +  nested environment).  A \emph{defined position} within a nested
    3.50 +  environment is one where @{term lookup} at its path does not yield
    3.51 +  @{term None}.
    3.52 +*}
    3.53 +
    3.54 +consts
    3.55 +  lookup :: "('a, 'b, 'c) env => 'c list => ('a, 'b, 'c) env option"
    3.56 +  lookup_option :: "('a, 'b, 'c) env option => 'c list => ('a, 'b, 'c) env option"
    3.57 +
    3.58 +primrec (lookup)
    3.59 +  "lookup (Val a) xs = (if xs = [] then Some (Val a) else None)"
    3.60 +  "lookup (Env b es) xs =
    3.61 +    (case xs of
    3.62 +      [] => Some (Env b es)
    3.63 +    | y # ys => lookup_option (es y) ys)"
    3.64 +  "lookup_option None xs = None"
    3.65 +  "lookup_option (Some e) xs = lookup e xs"
    3.66 +
    3.67 +hide const lookup_option
    3.68 +
    3.69 +text {*
    3.70 +  \medskip The characteristic cases of @{term lookup} are expressed by
    3.71 +  the following equalities.
    3.72 +*}
    3.73 +
    3.74 +theorem lookup_nil: "lookup e [] = Some e"
    3.75 +  by (cases e) simp_all
    3.76 +
    3.77 +theorem lookup_val_cons: "lookup (Val a) (x # xs) = None"
    3.78 +  by simp
    3.79 +
    3.80 +theorem lookup_env_cons:
    3.81 +  "lookup (Env b es) (x # xs) =
    3.82 +    (case es x of
    3.83 +      None => None
    3.84 +    | Some e => lookup e xs)"
    3.85 +  by (cases "es x") simp_all
    3.86 +
    3.87 +lemmas lookup.simps [simp del]
    3.88 +  and lookup_simps [simp] = lookup_nil lookup_val_cons lookup_env_cons
    3.89 +
    3.90 +theorem lookup_eq:
    3.91 +  "lookup env xs =
    3.92 +    (case xs of
    3.93 +      [] => Some env
    3.94 +    | x # xs =>
    3.95 +      (case env of
    3.96 +        Val a => None
    3.97 +      | Env b es =>
    3.98 +          (case es x of
    3.99 +            None => None
   3.100 +          | Some e => lookup e xs)))"
   3.101 +  by (simp split: list.split env.split)
   3.102 +
   3.103 +text {*
   3.104 +  \medskip Displaced @{term lookup} operations, relative to a certain
   3.105 +  base path prefix, may be reduced as follows.  There are two cases,
   3.106 +  depending whether the environment actually extends far enough to
   3.107 +  follow the base path.
   3.108 +*}
   3.109 +
   3.110 +theorem lookup_append_none:
   3.111 +  "!!env. lookup env xs = None ==> lookup env (xs @ ys) = None"
   3.112 +  (is "PROP ?P xs")
   3.113 +proof (induct xs)
   3.114 +  fix env :: "('a, 'b, 'c) env"
   3.115 +  {
   3.116 +    assume "lookup env [] = None"
   3.117 +    hence False by simp
   3.118 +    thus "lookup env ([] @ ys) = None" ..
   3.119 +  next
   3.120 +    fix x xs
   3.121 +    assume hyp: "PROP ?P xs"
   3.122 +    assume asm: "lookup env (x # xs) = None"
   3.123 +    show "lookup env ((x # xs) @ ys) = None"
   3.124 +    proof (cases env)
   3.125 +      case Val
   3.126 +      thus ?thesis by simp
   3.127 +    next
   3.128 +      fix b es assume env: "env = Env b es"
   3.129 +      show ?thesis
   3.130 +      proof (cases "es x")
   3.131 +        assume "es x = None"
   3.132 +        with env show ?thesis by simp
   3.133 +      next
   3.134 +        fix e assume es: "es x = Some e"
   3.135 +        show ?thesis
   3.136 +        proof (cases "lookup e xs")
   3.137 +          case None
   3.138 +          hence "lookup e (xs @ ys) = None" by (rule hyp)
   3.139 +          with env es show ?thesis by simp
   3.140 +        next
   3.141 +          case Some
   3.142 +          with asm env es have False by simp
   3.143 +          thus ?thesis ..
   3.144 +        qed
   3.145 +      qed
   3.146 +    qed
   3.147 +  }
   3.148 +qed
   3.149 +
   3.150 +theorem lookup_append_some:
   3.151 +  "!!env e. lookup env xs = Some e ==> lookup env (xs @ ys) = lookup e ys"
   3.152 +  (is "PROP ?P xs")
   3.153 +proof (induct xs)
   3.154 +  fix env e :: "('a, 'b, 'c) env"
   3.155 +  {
   3.156 +    assume "lookup env [] = Some e"
   3.157 +    hence "env = e" by simp
   3.158 +    thus "lookup env ([] @ ys) = lookup e ys" by simp
   3.159 +  next
   3.160 +    fix x xs
   3.161 +    assume hyp: "PROP ?P xs"
   3.162 +    assume asm: "lookup env (x # xs) = Some e"
   3.163 +    show "lookup env ((x # xs) @ ys) = lookup e ys"
   3.164 +    proof (cases env)
   3.165 +      fix a assume "env = Val a"
   3.166 +      with asm have False by simp
   3.167 +      thus ?thesis ..
   3.168 +    next
   3.169 +      fix b es assume env: "env = Env b es"
   3.170 +      show ?thesis
   3.171 +      proof (cases "es x")
   3.172 +        assume "es x = None"
   3.173 +        with asm env have False by simp
   3.174 +        thus ?thesis ..
   3.175 +      next
   3.176 +        fix e' assume es: "es x = Some e'"
   3.177 +        show ?thesis
   3.178 +        proof (cases "lookup e' xs")
   3.179 +          case None
   3.180 +          with asm env es have False by simp
   3.181 +          thus ?thesis ..
   3.182 +        next
   3.183 +          case Some
   3.184 +          with asm env es have "lookup e' xs = Some e"
   3.185 +            by simp
   3.186 +          hence "lookup e' (xs @ ys) = lookup e ys" by (rule hyp)
   3.187 +          with env es show ?thesis by simp
   3.188 +        qed
   3.189 +      qed
   3.190 +    qed
   3.191 +  }
   3.192 +qed
   3.193 +
   3.194 +text {*
   3.195 +  \medskip Successful @{term lookup} deeper down an environment
   3.196 +  structure means we are able to peek further up as well.  Note that
   3.197 +  this is basically just the contrapositive statement of @{thm
   3.198 +  [source] lookup_append_none} above.
   3.199 +*}
   3.200 +
   3.201 +theorem lookup_some_append:
   3.202 +  "lookup env (xs @ ys) = Some e ==> \<exists>e. lookup env xs = Some e"
   3.203 +proof -
   3.204 +  assume "lookup env (xs @ ys) = Some e"
   3.205 +  hence "lookup env (xs @ ys) \<noteq> None" by simp
   3.206 +  hence "lookup env xs \<noteq> None"
   3.207 +    by (rule contrapos_nn) (simp only: lookup_append_none)
   3.208 +  thus ?thesis by simp
   3.209 +qed
   3.210 +
   3.211 +text {*
   3.212 +  The subsequent statement describes in more detail how a successful
   3.213 +  @{term lookup} with a non-empty path results in a certain situation
   3.214 +  at any upper position.
   3.215 +*}
   3.216 +
   3.217 +theorem lookup_some_upper: "!!env e.
   3.218 +  lookup env (xs @ y # ys) = Some e ==>
   3.219 +    \<exists>b' es' env'.
   3.220 +      lookup env xs = Some (Env b' es') \<and>
   3.221 +      es' y = Some env' \<and>
   3.222 +      lookup env' ys = Some e"
   3.223 +  (is "PROP ?P xs" is "!!env e. ?A env e xs ==> ?C env e xs")
   3.224 +proof (induct ?P xs)
   3.225 +  fix env e
   3.226 +  let ?A = "?A env e" and ?C = "?C env e"
   3.227 +  {
   3.228 +    assume "?A []"
   3.229 +    hence "lookup env (y # ys) = Some e" by simp
   3.230 +    then obtain b' es' env' where
   3.231 +          env: "env = Env b' es'"
   3.232 +        and es': "es' y = Some env'"
   3.233 +        and look': "lookup env' ys = Some e"
   3.234 +      by (auto simp add: lookup_eq split: option.splits env.splits)
   3.235 +    from env have "lookup env [] = Some (Env b' es')" by simp
   3.236 +    with es' look' show "?C []" by blast
   3.237 +  next
   3.238 +    fix x xs
   3.239 +    assume hyp: "PROP ?P xs"
   3.240 +    assume "?A (x # xs)"
   3.241 +    then obtain b' es' env' where
   3.242 +          env: "env = Env b' es'"
   3.243 +        and es': "es' x = Some env'"
   3.244 +        and look': "lookup env' (xs @ y # ys) = Some e"
   3.245 +      by (auto simp add: lookup_eq split: option.splits env.splits)
   3.246 +    from hyp [OF look'] obtain b'' es'' env'' where
   3.247 +          upper': "lookup env' xs = Some (Env b'' es'')"
   3.248 +        and es'': "es'' y = Some env''"
   3.249 +        and look'': "lookup env'' ys = Some e"
   3.250 +      by blast
   3.251 +    from env es' upper' have "lookup env (x # xs) = Some (Env b'' es'')"
   3.252 +      by simp
   3.253 +    with es'' look'' show "?C (x # xs)" by blast
   3.254 +  }
   3.255 +qed
   3.256 +
   3.257 +
   3.258 +subsection {* The update operation *}
   3.259 +
   3.260 +text {*
   3.261 +  Update at a certain position in a nested environment may either
   3.262 +  delete an existing entry, or overwrite an existing one.  Note that
   3.263 +  update at undefined positions is simple absorbed, i.e.\ the
   3.264 +  environment is left unchanged.
   3.265 +*}
   3.266 +
   3.267 +consts
   3.268 +  update :: "'c list => ('a, 'b, 'c) env option
   3.269 +    => ('a, 'b, 'c) env => ('a, 'b, 'c) env"
   3.270 +  update_option :: "'c list => ('a, 'b, 'c) env option
   3.271 +    => ('a, 'b, 'c) env option => ('a, 'b, 'c) env option"
   3.272 +
   3.273 +primrec (update)
   3.274 +  "update xs opt (Val a) =
   3.275 +    (if xs = [] then (case opt of None => Val a | Some e => e)
   3.276 +    else Val a)"
   3.277 +  "update xs opt (Env b es) =
   3.278 +    (case xs of
   3.279 +      [] => (case opt of None => Env b es | Some e => e)
   3.280 +    | y # ys => Env b (es (y := update_option ys opt (es y))))"
   3.281 +  "update_option xs opt None =
   3.282 +    (if xs = [] then opt else None)"
   3.283 +  "update_option xs opt (Some e) =
   3.284 +    (if xs = [] then opt else Some (update xs opt e))"
   3.285 +
   3.286 +hide const update_option
   3.287 +
   3.288 +text {*
   3.289 +  \medskip The characteristic cases of @{term update} are expressed by
   3.290 +  the following equalities.
   3.291 +*}
   3.292 +
   3.293 +theorem update_nil_none: "update [] None env = env"
   3.294 +  by (cases env) simp_all
   3.295 +
   3.296 +theorem update_nil_some: "update [] (Some e) env = e"
   3.297 +  by (cases env) simp_all
   3.298 +
   3.299 +theorem update_cons_val: "update (x # xs) opt (Val a) = Val a"
   3.300 +  by simp
   3.301 +
   3.302 +theorem update_cons_nil_env:
   3.303 +    "update [x] opt (Env b es) = Env b (es (x := opt))"
   3.304 +  by (cases "es x") simp_all
   3.305 +
   3.306 +theorem update_cons_cons_env:
   3.307 +  "update (x # y # ys) opt (Env b es) =
   3.308 +    Env b (es (x :=
   3.309 +      (case es x of
   3.310 +        None => None
   3.311 +      | Some e => Some (update (y # ys) opt e))))"
   3.312 +  by (cases "es x") simp_all
   3.313 +
   3.314 +lemmas update.simps [simp del]
   3.315 +  and update_simps [simp] = update_nil_none update_nil_some
   3.316 +    update_cons_val update_cons_nil_env update_cons_cons_env
   3.317 +
   3.318 +lemma update_eq:
   3.319 +  "update xs opt env =
   3.320 +    (case xs of
   3.321 +      [] =>
   3.322 +        (case opt of
   3.323 +          None => env
   3.324 +        | Some e => e)
   3.325 +    | x # xs =>
   3.326 +        (case env of
   3.327 +          Val a => Val a
   3.328 +        | Env b es =>
   3.329 +            (case xs of
   3.330 +              [] => Env b (es (x := opt))
   3.331 +            | y # ys =>
   3.332 +                Env b (es (x :=
   3.333 +                  (case es x of
   3.334 +                    None => None
   3.335 +                  | Some e => Some (update (y # ys) opt e)))))))"
   3.336 +  by (simp split: list.split env.split option.split)
   3.337 +
   3.338 +text {*
   3.339 +  \medskip The most basic correspondence of @{term lookup} and @{term
   3.340 +  update} states that after @{term update} at a defined position,
   3.341 +  subsequent @{term lookup} operations would yield the new value.
   3.342 +*}
   3.343 +
   3.344 +theorem lookup_update_some:
   3.345 +  "!!env e. lookup env xs = Some e ==>
   3.346 +    lookup (update xs (Some env') env) xs = Some env'"
   3.347 +  (is "PROP ?P xs")
   3.348 +proof (induct xs)
   3.349 +  fix env e :: "('a, 'b, 'c) env"
   3.350 +  {
   3.351 +    assume "lookup env [] = Some e"
   3.352 +    hence "env = e" by simp
   3.353 +    thus "lookup (update [] (Some env') env) [] = Some env'"
   3.354 +      by simp
   3.355 +  next
   3.356 +    fix x xs
   3.357 +    assume hyp: "PROP ?P xs"
   3.358 +    assume asm: "lookup env (x # xs) = Some e"
   3.359 +    show "lookup (update (x # xs) (Some env') env) (x # xs) = Some env'"
   3.360 +    proof (cases env)
   3.361 +      fix a assume "env = Val a"
   3.362 +      with asm have False by simp
   3.363 +      thus ?thesis ..
   3.364 +    next
   3.365 +      fix b es assume env: "env = Env b es"
   3.366 +      show ?thesis
   3.367 +      proof (cases "es x")
   3.368 +        assume "es x = None"
   3.369 +        with asm env have False by simp
   3.370 +        thus ?thesis ..
   3.371 +      next
   3.372 +        fix e' assume es: "es x = Some e'"
   3.373 +        show ?thesis
   3.374 +        proof (cases xs)
   3.375 +          assume "xs = []"
   3.376 +          with env show ?thesis by simp
   3.377 +        next
   3.378 +          fix x' xs' assume xs: "xs = x' # xs'"
   3.379 +          from asm env es have "lookup e' xs = Some e" by simp
   3.380 +          hence "lookup (update xs (Some env') e') xs = Some env'" by (rule hyp)
   3.381 +          with env es xs show ?thesis by simp
   3.382 +        qed
   3.383 +      qed
   3.384 +    qed
   3.385 +  }
   3.386 +qed
   3.387 +
   3.388 +text {*
   3.389 +  \medskip The properties of displaced @{term update} operations are
   3.390 +  analogous to those of @{term lookup} above.  There are two cases:
   3.391 +  below an undefined position @{term update} is absorbed altogether,
   3.392 +  and below a defined positions @{term update} affects subsequent
   3.393 +  @{term lookup} operations in the obvious way.
   3.394 +*}
   3.395 +
   3.396 +theorem update_append_none:
   3.397 +  "!!env. lookup env xs = None ==> update (xs @ y # ys) opt env = env"
   3.398 +  (is "PROP ?P xs")
   3.399 +proof (induct xs)
   3.400 +  fix env :: "('a, 'b, 'c) env"
   3.401 +  {
   3.402 +    assume "lookup env [] = None"
   3.403 +    hence False by simp
   3.404 +    thus "update ([] @ y # ys) opt env = env" ..
   3.405 +  next
   3.406 +    fix x xs
   3.407 +    assume hyp: "PROP ?P xs"
   3.408 +    assume asm: "lookup env (x # xs) = None"
   3.409 +    show "update ((x # xs) @ y # ys) opt env = env"
   3.410 +    proof (cases env)
   3.411 +      fix a assume "env = Val a"
   3.412 +      thus ?thesis by simp
   3.413 +    next
   3.414 +      fix b es assume env: "env = Env b es"
   3.415 +      show ?thesis
   3.416 +      proof (cases "es x")
   3.417 +        assume es: "es x = None"
   3.418 +        show ?thesis
   3.419 +          by (cases xs) (simp_all add: es env fun_upd_idem_iff)
   3.420 +      next
   3.421 +        fix e assume es: "es x = Some e"
   3.422 +        show ?thesis
   3.423 +        proof (cases xs)
   3.424 +          assume "xs = []"
   3.425 +          with asm env es have False by simp
   3.426 +          thus ?thesis ..
   3.427 +        next
   3.428 +          fix x' xs' assume xs: "xs = x' # xs'"
   3.429 +          from asm env es have "lookup e xs = None" by simp
   3.430 +          hence "update (xs @ y # ys) opt e = e" by (rule hyp)
   3.431 +          with env es xs show "update ((x # xs) @ y # ys) opt env = env"
   3.432 +            by (simp add: fun_upd_idem_iff)
   3.433 +        qed
   3.434 +      qed
   3.435 +    qed
   3.436 +  }
   3.437 +qed
   3.438 +
   3.439 +theorem update_append_some:
   3.440 +  "!!env e. lookup env xs = Some e ==>
   3.441 +    lookup (update (xs @ y # ys) opt env) xs = Some (update (y # ys) opt e)"
   3.442 +  (is "PROP ?P xs")
   3.443 +proof (induct xs)
   3.444 +  fix env e :: "('a, 'b, 'c) env"
   3.445 +  {
   3.446 +    assume "lookup env [] = Some e"
   3.447 +    hence "env = e" by simp
   3.448 +    thus "lookup (update ([] @ y # ys) opt env) [] = Some (update (y # ys) opt e)"
   3.449 +      by simp
   3.450 +  next
   3.451 +    fix x xs
   3.452 +    assume hyp: "PROP ?P xs"
   3.453 +    assume asm: "lookup env (x # xs) = Some e"
   3.454 +    show "lookup (update ((x # xs) @ y # ys) opt env) (x # xs)
   3.455 +      = Some (update (y # ys) opt e)"
   3.456 +    proof (cases env)
   3.457 +      fix a assume "env = Val a"
   3.458 +      with asm have False by simp
   3.459 +      thus ?thesis ..
   3.460 +    next
   3.461 +      fix b es assume env: "env = Env b es"
   3.462 +      show ?thesis
   3.463 +      proof (cases "es x")
   3.464 +        assume "es x = None"
   3.465 +        with asm env have False by simp
   3.466 +        thus ?thesis ..
   3.467 +      next
   3.468 +        fix e' assume es: "es x = Some e'"
   3.469 +        show ?thesis
   3.470 +        proof (cases xs)
   3.471 +          assume xs: "xs = []"
   3.472 +          from asm env es xs have "e = e'" by simp
   3.473 +          with env es xs show ?thesis by simp
   3.474 +        next
   3.475 +          fix x' xs' assume xs: "xs = x' # xs'"
   3.476 +          from asm env es have "lookup e' xs = Some e" by simp
   3.477 +          hence "lookup (update (xs @ y # ys) opt e') xs =
   3.478 +            Some (update (y # ys) opt e)" by (rule hyp)
   3.479 +          with env es xs show ?thesis by simp
   3.480 +        qed
   3.481 +      qed
   3.482 +    qed
   3.483 +  }
   3.484 +qed
   3.485 +
   3.486 +text {*
   3.487 +  \medskip Apparently, @{term update} does not affect the result of
   3.488 +  subsequent @{term lookup} operations at independent positions, i.e.\
   3.489 +  in case that the paths for @{term update} and @{term lookup} fork at
   3.490 +  a certain point.
   3.491 +*}
   3.492 +
   3.493 +theorem lookup_update_other:
   3.494 +  "!!env. y \<noteq> (z::'c) ==> lookup (update (xs @ z # zs) opt env) (xs @ y # ys) =
   3.495 +    lookup env (xs @ y # ys)"
   3.496 +  (is "PROP ?P xs")
   3.497 +proof (induct xs)
   3.498 +  fix env :: "('a, 'b, 'c) env"
   3.499 +  assume neq: "y \<noteq> z"
   3.500 +  {
   3.501 +    show "lookup (update ([] @ z # zs) opt env) ([] @ y # ys) =
   3.502 +      lookup env ([] @ y # ys)"
   3.503 +    proof (cases env)
   3.504 +      case Val
   3.505 +      thus ?thesis by simp
   3.506 +    next
   3.507 +      case Env
   3.508 +      show ?thesis
   3.509 +      proof (cases zs)
   3.510 +        case Nil
   3.511 +        with neq Env show ?thesis by simp
   3.512 +      next
   3.513 +        case Cons
   3.514 +        with neq Env show ?thesis by simp
   3.515 +      qed
   3.516 +    qed
   3.517 +  next
   3.518 +    fix x xs
   3.519 +    assume hyp: "PROP ?P xs"
   3.520 +    show "lookup (update ((x # xs) @ z # zs) opt env) ((x # xs) @ y # ys) =
   3.521 +      lookup env ((x # xs) @ y # ys)"
   3.522 +    proof (cases env)
   3.523 +      case Val
   3.524 +      thus ?thesis by simp
   3.525 +    next
   3.526 +      fix y es assume env: "env = Env y es"
   3.527 +      show ?thesis
   3.528 +      proof (cases xs)
   3.529 +        assume xs: "xs = []"
   3.530 +        show ?thesis
   3.531 +        proof (cases "es x")
   3.532 +          case None
   3.533 +          with env xs show ?thesis by simp
   3.534 +        next
   3.535 +          case Some
   3.536 +          with hyp env xs and neq show ?thesis by simp
   3.537 +        qed
   3.538 +      next
   3.539 +        fix x' xs' assume xs: "xs = x' # xs'"
   3.540 +        show ?thesis
   3.541 +        proof (cases "es x")
   3.542 +          case None
   3.543 +          with env xs show ?thesis by simp
   3.544 +        next
   3.545 +          case Some
   3.546 +          with hyp env xs neq show ?thesis by simp
   3.547 +        qed
   3.548 +      qed
   3.549 +    qed
   3.550 +  }
   3.551 +qed
   3.552 +
   3.553 +end