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