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