src/HOL/Library/Nested_Environment.thy
author oheimb
Wed Jan 31 10:15:55 2001 +0100 (2001-01-31)
changeset 11008 f7333f055ef6
parent 10948 1bd100c82300
child 11809 c9ffdd63dd93
permissions -rw-r--r--
improved theory reference in comment
wenzelm@10943
     1
(*  Title:      HOL/Library/Nested_Environment.thy
wenzelm@10943
     2
    ID:         $Id$
wenzelm@10943
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@10943
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
wenzelm@10943
     5
*)
wenzelm@10943
     6
wenzelm@10943
     7
header {*
wenzelm@10943
     8
  \title{Nested environments}
wenzelm@10943
     9
  \author{Markus Wenzel}
wenzelm@10943
    10
*}
wenzelm@10943
    11
wenzelm@10943
    12
theory Nested_Environment = Main:
wenzelm@10943
    13
wenzelm@10943
    14
text {*
wenzelm@10943
    15
  Consider a partial function @{term [source] "e :: 'a => 'b option"};
wenzelm@10943
    16
  this may be understood as an \emph{environment} mapping indexes
wenzelm@10943
    17
  @{typ 'a} to optional entry values @{typ 'b} (cf.\ the basic theory
wenzelm@10948
    18
  @{text Map} of Isabelle/HOL).  This basic idea is easily generalized
wenzelm@10948
    19
  to that of a \emph{nested environment}, where entries may be either
wenzelm@10948
    20
  basic values or again proper environments.  Then each entry is
wenzelm@10948
    21
  accessed by a \emph{path}, i.e.\ a list of indexes leading to its
wenzelm@10948
    22
  position within the structure.
wenzelm@10943
    23
*}
wenzelm@10943
    24
wenzelm@10943
    25
datatype ('a, 'b, 'c) env =
wenzelm@10943
    26
    Val 'a
wenzelm@10943
    27
  | Env 'b  "'c => ('a, 'b, 'c) env option"
wenzelm@10943
    28
wenzelm@10943
    29
text {*
wenzelm@10943
    30
  \medskip In the type @{typ "('a, 'b, 'c) env"} the parameter @{typ
wenzelm@10943
    31
  'a} refers to basic values (occurring in terminal positions), type
wenzelm@10943
    32
  @{typ 'b} to values associated with proper (inner) environments, and
wenzelm@10943
    33
  type @{typ 'c} with the index type for branching.  Note that there
wenzelm@10943
    34
  is no restriction on any of these types.  In particular, arbitrary
wenzelm@10943
    35
  branching may yield rather large (transfinite) tree structures.
wenzelm@10943
    36
*}
wenzelm@10943
    37
wenzelm@10943
    38
wenzelm@10943
    39
subsection {* The lookup operation *}
wenzelm@10943
    40
wenzelm@10943
    41
text {*
wenzelm@10943
    42
  Lookup in nested environments works by following a given path of
wenzelm@10943
    43
  index elements, leading to an optional result (a terminal value or
wenzelm@10943
    44
  nested environment).  A \emph{defined position} within a nested
wenzelm@10943
    45
  environment is one where @{term lookup} at its path does not yield
wenzelm@10943
    46
  @{term None}.
wenzelm@10943
    47
*}
wenzelm@10943
    48
wenzelm@10943
    49
consts
wenzelm@10943
    50
  lookup :: "('a, 'b, 'c) env => 'c list => ('a, 'b, 'c) env option"
wenzelm@10943
    51
  lookup_option :: "('a, 'b, 'c) env option => 'c list => ('a, 'b, 'c) env option"
wenzelm@10943
    52
wenzelm@10943
    53
primrec (lookup)
wenzelm@10943
    54
  "lookup (Val a) xs = (if xs = [] then Some (Val a) else None)"
wenzelm@10943
    55
  "lookup (Env b es) xs =
wenzelm@10943
    56
    (case xs of
wenzelm@10943
    57
      [] => Some (Env b es)
wenzelm@10943
    58
    | y # ys => lookup_option (es y) ys)"
wenzelm@10943
    59
  "lookup_option None xs = None"
wenzelm@10943
    60
  "lookup_option (Some e) xs = lookup e xs"
wenzelm@10943
    61
wenzelm@10943
    62
hide const lookup_option
wenzelm@10943
    63
wenzelm@10943
    64
text {*
wenzelm@10943
    65
  \medskip The characteristic cases of @{term lookup} are expressed by
wenzelm@10943
    66
  the following equalities.
wenzelm@10943
    67
*}
wenzelm@10943
    68
wenzelm@10943
    69
theorem lookup_nil: "lookup e [] = Some e"
wenzelm@10943
    70
  by (cases e) simp_all
wenzelm@10943
    71
wenzelm@10943
    72
theorem lookup_val_cons: "lookup (Val a) (x # xs) = None"
wenzelm@10943
    73
  by simp
wenzelm@10943
    74
wenzelm@10943
    75
theorem lookup_env_cons:
wenzelm@10943
    76
  "lookup (Env b es) (x # xs) =
wenzelm@10943
    77
    (case es x of
wenzelm@10943
    78
      None => None
wenzelm@10943
    79
    | Some e => lookup e xs)"
wenzelm@10943
    80
  by (cases "es x") simp_all
wenzelm@10943
    81
wenzelm@10943
    82
lemmas lookup.simps [simp del]
wenzelm@10943
    83
  and lookup_simps [simp] = lookup_nil lookup_val_cons lookup_env_cons
wenzelm@10943
    84
wenzelm@10943
    85
theorem lookup_eq:
wenzelm@10943
    86
  "lookup env xs =
wenzelm@10943
    87
    (case xs of
wenzelm@10943
    88
      [] => Some env
wenzelm@10943
    89
    | x # xs =>
wenzelm@10943
    90
      (case env of
wenzelm@10943
    91
        Val a => None
wenzelm@10943
    92
      | Env b es =>
wenzelm@10943
    93
          (case es x of
wenzelm@10943
    94
            None => None
wenzelm@10943
    95
          | Some e => lookup e xs)))"
wenzelm@10943
    96
  by (simp split: list.split env.split)
wenzelm@10943
    97
wenzelm@10943
    98
text {*
wenzelm@10943
    99
  \medskip Displaced @{term lookup} operations, relative to a certain
wenzelm@10943
   100
  base path prefix, may be reduced as follows.  There are two cases,
wenzelm@10943
   101
  depending whether the environment actually extends far enough to
wenzelm@10943
   102
  follow the base path.
wenzelm@10943
   103
*}
wenzelm@10943
   104
wenzelm@10943
   105
theorem lookup_append_none:
wenzelm@10943
   106
  "!!env. lookup env xs = None ==> lookup env (xs @ ys) = None"
wenzelm@10943
   107
  (is "PROP ?P xs")
wenzelm@10943
   108
proof (induct xs)
wenzelm@10943
   109
  fix env :: "('a, 'b, 'c) env"
wenzelm@10943
   110
  {
wenzelm@10943
   111
    assume "lookup env [] = None"
wenzelm@10943
   112
    hence False by simp
wenzelm@10943
   113
    thus "lookup env ([] @ ys) = None" ..
wenzelm@10943
   114
  next
wenzelm@10943
   115
    fix x xs
wenzelm@10943
   116
    assume hyp: "PROP ?P xs"
wenzelm@10943
   117
    assume asm: "lookup env (x # xs) = None"
wenzelm@10943
   118
    show "lookup env ((x # xs) @ ys) = None"
wenzelm@10943
   119
    proof (cases env)
wenzelm@10943
   120
      case Val
wenzelm@10943
   121
      thus ?thesis by simp
wenzelm@10943
   122
    next
wenzelm@10943
   123
      fix b es assume env: "env = Env b es"
wenzelm@10943
   124
      show ?thesis
wenzelm@10943
   125
      proof (cases "es x")
wenzelm@10943
   126
        assume "es x = None"
wenzelm@10943
   127
        with env show ?thesis by simp
wenzelm@10943
   128
      next
wenzelm@10943
   129
        fix e assume es: "es x = Some e"
wenzelm@10943
   130
        show ?thesis
wenzelm@10943
   131
        proof (cases "lookup e xs")
wenzelm@10943
   132
          case None
wenzelm@10943
   133
          hence "lookup e (xs @ ys) = None" by (rule hyp)
wenzelm@10943
   134
          with env es show ?thesis by simp
wenzelm@10943
   135
        next
wenzelm@10943
   136
          case Some
wenzelm@10943
   137
          with asm env es have False by simp
wenzelm@10943
   138
          thus ?thesis ..
wenzelm@10943
   139
        qed
wenzelm@10943
   140
      qed
wenzelm@10943
   141
    qed
wenzelm@10943
   142
  }
wenzelm@10943
   143
qed
wenzelm@10943
   144
wenzelm@10943
   145
theorem lookup_append_some:
wenzelm@10943
   146
  "!!env e. lookup env xs = Some e ==> lookup env (xs @ ys) = lookup e ys"
wenzelm@10943
   147
  (is "PROP ?P xs")
wenzelm@10943
   148
proof (induct xs)
wenzelm@10943
   149
  fix env e :: "('a, 'b, 'c) env"
wenzelm@10943
   150
  {
wenzelm@10943
   151
    assume "lookup env [] = Some e"
wenzelm@10943
   152
    hence "env = e" by simp
wenzelm@10943
   153
    thus "lookup env ([] @ ys) = lookup e ys" by simp
wenzelm@10943
   154
  next
wenzelm@10943
   155
    fix x xs
wenzelm@10943
   156
    assume hyp: "PROP ?P xs"
wenzelm@10943
   157
    assume asm: "lookup env (x # xs) = Some e"
wenzelm@10943
   158
    show "lookup env ((x # xs) @ ys) = lookup e ys"
wenzelm@10943
   159
    proof (cases env)
wenzelm@10943
   160
      fix a assume "env = Val a"
wenzelm@10943
   161
      with asm have False by simp
wenzelm@10943
   162
      thus ?thesis ..
wenzelm@10943
   163
    next
wenzelm@10943
   164
      fix b es assume env: "env = Env b es"
wenzelm@10943
   165
      show ?thesis
wenzelm@10943
   166
      proof (cases "es x")
wenzelm@10943
   167
        assume "es x = None"
wenzelm@10943
   168
        with asm env have False by simp
wenzelm@10943
   169
        thus ?thesis ..
wenzelm@10943
   170
      next
wenzelm@10943
   171
        fix e' assume es: "es x = Some e'"
wenzelm@10943
   172
        show ?thesis
wenzelm@10943
   173
        proof (cases "lookup e' xs")
wenzelm@10943
   174
          case None
wenzelm@10943
   175
          with asm env es have False by simp
wenzelm@10943
   176
          thus ?thesis ..
wenzelm@10943
   177
        next
wenzelm@10943
   178
          case Some
wenzelm@10943
   179
          with asm env es have "lookup e' xs = Some e"
wenzelm@10943
   180
            by simp
wenzelm@10943
   181
          hence "lookup e' (xs @ ys) = lookup e ys" by (rule hyp)
wenzelm@10943
   182
          with env es show ?thesis by simp
wenzelm@10943
   183
        qed
wenzelm@10943
   184
      qed
wenzelm@10943
   185
    qed
wenzelm@10943
   186
  }
wenzelm@10943
   187
qed
wenzelm@10943
   188
wenzelm@10943
   189
text {*
wenzelm@10943
   190
  \medskip Successful @{term lookup} deeper down an environment
wenzelm@10943
   191
  structure means we are able to peek further up as well.  Note that
wenzelm@10943
   192
  this is basically just the contrapositive statement of @{thm
wenzelm@10943
   193
  [source] lookup_append_none} above.
wenzelm@10943
   194
*}
wenzelm@10943
   195
wenzelm@10943
   196
theorem lookup_some_append:
wenzelm@10943
   197
  "lookup env (xs @ ys) = Some e ==> \<exists>e. lookup env xs = Some e"
wenzelm@10943
   198
proof -
wenzelm@10943
   199
  assume "lookup env (xs @ ys) = Some e"
wenzelm@10943
   200
  hence "lookup env (xs @ ys) \<noteq> None" by simp
wenzelm@10943
   201
  hence "lookup env xs \<noteq> None"
wenzelm@10943
   202
    by (rule contrapos_nn) (simp only: lookup_append_none)
wenzelm@10943
   203
  thus ?thesis by simp
wenzelm@10943
   204
qed
wenzelm@10943
   205
wenzelm@10943
   206
text {*
wenzelm@10943
   207
  The subsequent statement describes in more detail how a successful
wenzelm@10943
   208
  @{term lookup} with a non-empty path results in a certain situation
wenzelm@10943
   209
  at any upper position.
wenzelm@10943
   210
*}
wenzelm@10943
   211
wenzelm@10943
   212
theorem lookup_some_upper: "!!env e.
wenzelm@10943
   213
  lookup env (xs @ y # ys) = Some e ==>
wenzelm@10943
   214
    \<exists>b' es' env'.
wenzelm@10943
   215
      lookup env xs = Some (Env b' es') \<and>
wenzelm@10943
   216
      es' y = Some env' \<and>
wenzelm@10943
   217
      lookup env' ys = Some e"
wenzelm@10943
   218
  (is "PROP ?P xs" is "!!env e. ?A env e xs ==> ?C env e xs")
wenzelm@10943
   219
proof (induct ?P xs)
wenzelm@10948
   220
  fix env e let ?A = "?A env e" and ?C = "?C env e"
wenzelm@10943
   221
  {
wenzelm@10943
   222
    assume "?A []"
wenzelm@10943
   223
    hence "lookup env (y # ys) = Some e" by simp
wenzelm@10943
   224
    then obtain b' es' env' where
wenzelm@10948
   225
        env: "env = Env b' es'" and
wenzelm@10948
   226
        es': "es' y = Some env'" and
wenzelm@10948
   227
        look': "lookup env' ys = Some e"
wenzelm@10943
   228
      by (auto simp add: lookup_eq split: option.splits env.splits)
wenzelm@10943
   229
    from env have "lookup env [] = Some (Env b' es')" by simp
wenzelm@10943
   230
    with es' look' show "?C []" by blast
wenzelm@10943
   231
  next
wenzelm@10943
   232
    fix x xs
wenzelm@10943
   233
    assume hyp: "PROP ?P xs"
wenzelm@10943
   234
    assume "?A (x # xs)"
wenzelm@10943
   235
    then obtain b' es' env' where
wenzelm@10948
   236
        env: "env = Env b' es'" and
wenzelm@10948
   237
        es': "es' x = Some env'" and
wenzelm@10948
   238
        look': "lookup env' (xs @ y # ys) = Some e"
wenzelm@10943
   239
      by (auto simp add: lookup_eq split: option.splits env.splits)
wenzelm@10943
   240
    from hyp [OF look'] obtain b'' es'' env'' where
wenzelm@10948
   241
        upper': "lookup env' xs = Some (Env b'' es'')" and
wenzelm@10948
   242
        es'': "es'' y = Some env''" and
wenzelm@10948
   243
        look'': "lookup env'' ys = Some e"
wenzelm@10943
   244
      by blast
wenzelm@10943
   245
    from env es' upper' have "lookup env (x # xs) = Some (Env b'' es'')"
wenzelm@10943
   246
      by simp
wenzelm@10943
   247
    with es'' look'' show "?C (x # xs)" by blast
wenzelm@10943
   248
  }
wenzelm@10943
   249
qed
wenzelm@10943
   250
wenzelm@10943
   251
wenzelm@10943
   252
subsection {* The update operation *}
wenzelm@10943
   253
wenzelm@10943
   254
text {*
wenzelm@10943
   255
  Update at a certain position in a nested environment may either
wenzelm@10943
   256
  delete an existing entry, or overwrite an existing one.  Note that
wenzelm@10943
   257
  update at undefined positions is simple absorbed, i.e.\ the
wenzelm@10943
   258
  environment is left unchanged.
wenzelm@10943
   259
*}
wenzelm@10943
   260
wenzelm@10943
   261
consts
wenzelm@10943
   262
  update :: "'c list => ('a, 'b, 'c) env option
wenzelm@10943
   263
    => ('a, 'b, 'c) env => ('a, 'b, 'c) env"
wenzelm@10943
   264
  update_option :: "'c list => ('a, 'b, 'c) env option
wenzelm@10943
   265
    => ('a, 'b, 'c) env option => ('a, 'b, 'c) env option"
wenzelm@10943
   266
wenzelm@10943
   267
primrec (update)
wenzelm@10943
   268
  "update xs opt (Val a) =
wenzelm@10943
   269
    (if xs = [] then (case opt of None => Val a | Some e => e)
wenzelm@10943
   270
    else Val a)"
wenzelm@10943
   271
  "update xs opt (Env b es) =
wenzelm@10943
   272
    (case xs of
wenzelm@10943
   273
      [] => (case opt of None => Env b es | Some e => e)
wenzelm@10943
   274
    | y # ys => Env b (es (y := update_option ys opt (es y))))"
wenzelm@10943
   275
  "update_option xs opt None =
wenzelm@10943
   276
    (if xs = [] then opt else None)"
wenzelm@10943
   277
  "update_option xs opt (Some e) =
wenzelm@10943
   278
    (if xs = [] then opt else Some (update xs opt e))"
wenzelm@10943
   279
wenzelm@10943
   280
hide const update_option
wenzelm@10943
   281
wenzelm@10943
   282
text {*
wenzelm@10943
   283
  \medskip The characteristic cases of @{term update} are expressed by
wenzelm@10943
   284
  the following equalities.
wenzelm@10943
   285
*}
wenzelm@10943
   286
wenzelm@10943
   287
theorem update_nil_none: "update [] None env = env"
wenzelm@10943
   288
  by (cases env) simp_all
wenzelm@10943
   289
wenzelm@10943
   290
theorem update_nil_some: "update [] (Some e) env = e"
wenzelm@10943
   291
  by (cases env) simp_all
wenzelm@10943
   292
wenzelm@10943
   293
theorem update_cons_val: "update (x # xs) opt (Val a) = Val a"
wenzelm@10943
   294
  by simp
wenzelm@10943
   295
wenzelm@10943
   296
theorem update_cons_nil_env:
wenzelm@10943
   297
    "update [x] opt (Env b es) = Env b (es (x := opt))"
wenzelm@10943
   298
  by (cases "es x") simp_all
wenzelm@10943
   299
wenzelm@10943
   300
theorem update_cons_cons_env:
wenzelm@10943
   301
  "update (x # y # ys) opt (Env b es) =
wenzelm@10943
   302
    Env b (es (x :=
wenzelm@10943
   303
      (case es x of
wenzelm@10943
   304
        None => None
wenzelm@10943
   305
      | Some e => Some (update (y # ys) opt e))))"
wenzelm@10943
   306
  by (cases "es x") simp_all
wenzelm@10943
   307
wenzelm@10943
   308
lemmas update.simps [simp del]
wenzelm@10943
   309
  and update_simps [simp] = update_nil_none update_nil_some
wenzelm@10943
   310
    update_cons_val update_cons_nil_env update_cons_cons_env
wenzelm@10943
   311
wenzelm@10943
   312
lemma update_eq:
wenzelm@10943
   313
  "update xs opt env =
wenzelm@10943
   314
    (case xs of
wenzelm@10943
   315
      [] =>
wenzelm@10943
   316
        (case opt of
wenzelm@10943
   317
          None => env
wenzelm@10943
   318
        | Some e => e)
wenzelm@10943
   319
    | x # xs =>
wenzelm@10943
   320
        (case env of
wenzelm@10943
   321
          Val a => Val a
wenzelm@10943
   322
        | Env b es =>
wenzelm@10943
   323
            (case xs of
wenzelm@10943
   324
              [] => Env b (es (x := opt))
wenzelm@10943
   325
            | y # ys =>
wenzelm@10943
   326
                Env b (es (x :=
wenzelm@10943
   327
                  (case es x of
wenzelm@10943
   328
                    None => None
wenzelm@10943
   329
                  | Some e => Some (update (y # ys) opt e)))))))"
wenzelm@10943
   330
  by (simp split: list.split env.split option.split)
wenzelm@10943
   331
wenzelm@10943
   332
text {*
wenzelm@10943
   333
  \medskip The most basic correspondence of @{term lookup} and @{term
wenzelm@10943
   334
  update} states that after @{term update} at a defined position,
wenzelm@10943
   335
  subsequent @{term lookup} operations would yield the new value.
wenzelm@10943
   336
*}
wenzelm@10943
   337
wenzelm@10943
   338
theorem lookup_update_some:
wenzelm@10943
   339
  "!!env e. lookup env xs = Some e ==>
wenzelm@10943
   340
    lookup (update xs (Some env') env) xs = Some env'"
wenzelm@10943
   341
  (is "PROP ?P xs")
wenzelm@10943
   342
proof (induct xs)
wenzelm@10943
   343
  fix env e :: "('a, 'b, 'c) env"
wenzelm@10943
   344
  {
wenzelm@10943
   345
    assume "lookup env [] = Some e"
wenzelm@10943
   346
    hence "env = e" by simp
wenzelm@10943
   347
    thus "lookup (update [] (Some env') env) [] = Some env'"
wenzelm@10943
   348
      by simp
wenzelm@10943
   349
  next
wenzelm@10943
   350
    fix x xs
wenzelm@10943
   351
    assume hyp: "PROP ?P xs"
wenzelm@10943
   352
    assume asm: "lookup env (x # xs) = Some e"
wenzelm@10943
   353
    show "lookup (update (x # xs) (Some env') env) (x # xs) = Some env'"
wenzelm@10943
   354
    proof (cases env)
wenzelm@10943
   355
      fix a assume "env = Val a"
wenzelm@10943
   356
      with asm have False by simp
wenzelm@10943
   357
      thus ?thesis ..
wenzelm@10943
   358
    next
wenzelm@10943
   359
      fix b es assume env: "env = Env b es"
wenzelm@10943
   360
      show ?thesis
wenzelm@10943
   361
      proof (cases "es x")
wenzelm@10943
   362
        assume "es x = None"
wenzelm@10943
   363
        with asm env have False by simp
wenzelm@10943
   364
        thus ?thesis ..
wenzelm@10943
   365
      next
wenzelm@10943
   366
        fix e' assume es: "es x = Some e'"
wenzelm@10943
   367
        show ?thesis
wenzelm@10943
   368
        proof (cases xs)
wenzelm@10943
   369
          assume "xs = []"
wenzelm@10943
   370
          with env show ?thesis by simp
wenzelm@10943
   371
        next
wenzelm@10943
   372
          fix x' xs' assume xs: "xs = x' # xs'"
wenzelm@10943
   373
          from asm env es have "lookup e' xs = Some e" by simp
wenzelm@10943
   374
          hence "lookup (update xs (Some env') e') xs = Some env'" by (rule hyp)
wenzelm@10943
   375
          with env es xs show ?thesis by simp
wenzelm@10943
   376
        qed
wenzelm@10943
   377
      qed
wenzelm@10943
   378
    qed
wenzelm@10943
   379
  }
wenzelm@10943
   380
qed
wenzelm@10943
   381
wenzelm@10943
   382
text {*
wenzelm@10943
   383
  \medskip The properties of displaced @{term update} operations are
wenzelm@10943
   384
  analogous to those of @{term lookup} above.  There are two cases:
wenzelm@10943
   385
  below an undefined position @{term update} is absorbed altogether,
wenzelm@10943
   386
  and below a defined positions @{term update} affects subsequent
wenzelm@10943
   387
  @{term lookup} operations in the obvious way.
wenzelm@10943
   388
*}
wenzelm@10943
   389
wenzelm@10943
   390
theorem update_append_none:
wenzelm@10943
   391
  "!!env. lookup env xs = None ==> update (xs @ y # ys) opt env = env"
wenzelm@10943
   392
  (is "PROP ?P xs")
wenzelm@10943
   393
proof (induct xs)
wenzelm@10943
   394
  fix env :: "('a, 'b, 'c) env"
wenzelm@10943
   395
  {
wenzelm@10943
   396
    assume "lookup env [] = None"
wenzelm@10943
   397
    hence False by simp
wenzelm@10943
   398
    thus "update ([] @ y # ys) opt env = env" ..
wenzelm@10943
   399
  next
wenzelm@10943
   400
    fix x xs
wenzelm@10943
   401
    assume hyp: "PROP ?P xs"
wenzelm@10943
   402
    assume asm: "lookup env (x # xs) = None"
wenzelm@10943
   403
    show "update ((x # xs) @ y # ys) opt env = env"
wenzelm@10943
   404
    proof (cases env)
wenzelm@10943
   405
      fix a assume "env = Val a"
wenzelm@10943
   406
      thus ?thesis by simp
wenzelm@10943
   407
    next
wenzelm@10943
   408
      fix b es assume env: "env = Env b es"
wenzelm@10943
   409
      show ?thesis
wenzelm@10943
   410
      proof (cases "es x")
wenzelm@10943
   411
        assume es: "es x = None"
wenzelm@10943
   412
        show ?thesis
wenzelm@10943
   413
          by (cases xs) (simp_all add: es env fun_upd_idem_iff)
wenzelm@10943
   414
      next
wenzelm@10943
   415
        fix e assume es: "es x = Some e"
wenzelm@10943
   416
        show ?thesis
wenzelm@10943
   417
        proof (cases xs)
wenzelm@10943
   418
          assume "xs = []"
wenzelm@10943
   419
          with asm env es have False by simp
wenzelm@10943
   420
          thus ?thesis ..
wenzelm@10943
   421
        next
wenzelm@10943
   422
          fix x' xs' assume xs: "xs = x' # xs'"
wenzelm@10943
   423
          from asm env es have "lookup e xs = None" by simp
wenzelm@10943
   424
          hence "update (xs @ y # ys) opt e = e" by (rule hyp)
wenzelm@10943
   425
          with env es xs show "update ((x # xs) @ y # ys) opt env = env"
wenzelm@10943
   426
            by (simp add: fun_upd_idem_iff)
wenzelm@10943
   427
        qed
wenzelm@10943
   428
      qed
wenzelm@10943
   429
    qed
wenzelm@10943
   430
  }
wenzelm@10943
   431
qed
wenzelm@10943
   432
wenzelm@10943
   433
theorem update_append_some:
wenzelm@10943
   434
  "!!env e. lookup env xs = Some e ==>
wenzelm@10943
   435
    lookup (update (xs @ y # ys) opt env) xs = Some (update (y # ys) opt e)"
wenzelm@10943
   436
  (is "PROP ?P xs")
wenzelm@10943
   437
proof (induct xs)
wenzelm@10943
   438
  fix env e :: "('a, 'b, 'c) env"
wenzelm@10943
   439
  {
wenzelm@10943
   440
    assume "lookup env [] = Some e"
wenzelm@10943
   441
    hence "env = e" by simp
wenzelm@10943
   442
    thus "lookup (update ([] @ y # ys) opt env) [] = Some (update (y # ys) opt e)"
wenzelm@10943
   443
      by simp
wenzelm@10943
   444
  next
wenzelm@10943
   445
    fix x xs
wenzelm@10943
   446
    assume hyp: "PROP ?P xs"
wenzelm@10943
   447
    assume asm: "lookup env (x # xs) = Some e"
wenzelm@10943
   448
    show "lookup (update ((x # xs) @ y # ys) opt env) (x # xs)
wenzelm@10943
   449
      = Some (update (y # ys) opt e)"
wenzelm@10943
   450
    proof (cases env)
wenzelm@10943
   451
      fix a assume "env = Val a"
wenzelm@10943
   452
      with asm have False by simp
wenzelm@10943
   453
      thus ?thesis ..
wenzelm@10943
   454
    next
wenzelm@10943
   455
      fix b es assume env: "env = Env b es"
wenzelm@10943
   456
      show ?thesis
wenzelm@10943
   457
      proof (cases "es x")
wenzelm@10943
   458
        assume "es x = None"
wenzelm@10943
   459
        with asm env have False by simp
wenzelm@10943
   460
        thus ?thesis ..
wenzelm@10943
   461
      next
wenzelm@10943
   462
        fix e' assume es: "es x = Some e'"
wenzelm@10943
   463
        show ?thesis
wenzelm@10943
   464
        proof (cases xs)
wenzelm@10943
   465
          assume xs: "xs = []"
wenzelm@10943
   466
          from asm env es xs have "e = e'" by simp
wenzelm@10943
   467
          with env es xs show ?thesis by simp
wenzelm@10943
   468
        next
wenzelm@10943
   469
          fix x' xs' assume xs: "xs = x' # xs'"
wenzelm@10943
   470
          from asm env es have "lookup e' xs = Some e" by simp
wenzelm@10943
   471
          hence "lookup (update (xs @ y # ys) opt e') xs =
wenzelm@10943
   472
            Some (update (y # ys) opt e)" by (rule hyp)
wenzelm@10943
   473
          with env es xs show ?thesis by simp
wenzelm@10943
   474
        qed
wenzelm@10943
   475
      qed
wenzelm@10943
   476
    qed
wenzelm@10943
   477
  }
wenzelm@10943
   478
qed
wenzelm@10943
   479
wenzelm@10943
   480
text {*
wenzelm@10943
   481
  \medskip Apparently, @{term update} does not affect the result of
wenzelm@10943
   482
  subsequent @{term lookup} operations at independent positions, i.e.\
wenzelm@10943
   483
  in case that the paths for @{term update} and @{term lookup} fork at
wenzelm@10943
   484
  a certain point.
wenzelm@10943
   485
*}
wenzelm@10943
   486
wenzelm@10943
   487
theorem lookup_update_other:
wenzelm@10943
   488
  "!!env. y \<noteq> (z::'c) ==> lookup (update (xs @ z # zs) opt env) (xs @ y # ys) =
wenzelm@10943
   489
    lookup env (xs @ y # ys)"
wenzelm@10943
   490
  (is "PROP ?P xs")
wenzelm@10943
   491
proof (induct xs)
wenzelm@10943
   492
  fix env :: "('a, 'b, 'c) env"
wenzelm@10943
   493
  assume neq: "y \<noteq> z"
wenzelm@10943
   494
  {
wenzelm@10943
   495
    show "lookup (update ([] @ z # zs) opt env) ([] @ y # ys) =
wenzelm@10943
   496
      lookup env ([] @ y # ys)"
wenzelm@10943
   497
    proof (cases env)
wenzelm@10943
   498
      case Val
wenzelm@10943
   499
      thus ?thesis by simp
wenzelm@10943
   500
    next
wenzelm@10943
   501
      case Env
wenzelm@10943
   502
      show ?thesis
wenzelm@10943
   503
      proof (cases zs)
wenzelm@10943
   504
        case Nil
wenzelm@10943
   505
        with neq Env show ?thesis by simp
wenzelm@10943
   506
      next
wenzelm@10943
   507
        case Cons
wenzelm@10943
   508
        with neq Env show ?thesis by simp
wenzelm@10943
   509
      qed
wenzelm@10943
   510
    qed
wenzelm@10943
   511
  next
wenzelm@10943
   512
    fix x xs
wenzelm@10943
   513
    assume hyp: "PROP ?P xs"
wenzelm@10943
   514
    show "lookup (update ((x # xs) @ z # zs) opt env) ((x # xs) @ y # ys) =
wenzelm@10943
   515
      lookup env ((x # xs) @ y # ys)"
wenzelm@10943
   516
    proof (cases env)
wenzelm@10943
   517
      case Val
wenzelm@10943
   518
      thus ?thesis by simp
wenzelm@10943
   519
    next
wenzelm@10943
   520
      fix y es assume env: "env = Env y es"
wenzelm@10943
   521
      show ?thesis
wenzelm@10943
   522
      proof (cases xs)
wenzelm@10943
   523
        assume xs: "xs = []"
wenzelm@10943
   524
        show ?thesis
wenzelm@10943
   525
        proof (cases "es x")
wenzelm@10943
   526
          case None
wenzelm@10943
   527
          with env xs show ?thesis by simp
wenzelm@10943
   528
        next
wenzelm@10943
   529
          case Some
wenzelm@10943
   530
          with hyp env xs and neq show ?thesis by simp
wenzelm@10943
   531
        qed
wenzelm@10943
   532
      next
wenzelm@10943
   533
        fix x' xs' assume xs: "xs = x' # xs'"
wenzelm@10943
   534
        show ?thesis
wenzelm@10943
   535
        proof (cases "es x")
wenzelm@10943
   536
          case None
wenzelm@10943
   537
          with env xs show ?thesis by simp
wenzelm@10943
   538
        next
wenzelm@10943
   539
          case Some
wenzelm@10943
   540
          with hyp env xs neq show ?thesis by simp
wenzelm@10943
   541
        qed
wenzelm@10943
   542
      qed
wenzelm@10943
   543
    qed
wenzelm@10943
   544
  }
wenzelm@10943
   545
qed
wenzelm@10943
   546
wenzelm@10943
   547
end