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