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