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