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