src/HOL/Library/Nested_Environment.thy
author wenzelm
Thu Oct 16 22:44:24 2008 +0200 (2008-10-16)
changeset 28615 4c8fa015ec7f
parent 28562 4e74209f113e
child 30663 0b6aff7451b2
permissions -rw-r--r--
explicit SORT_CONSTRAINT for proofs depending implicitly on certain sorts;
     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 imports Plain "~~/src/HOL/List" "~~/src/HOL/Code_Eval"
    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   assumes "lookup env xs = None"
   105   shows "lookup env (xs @ ys) = None"
   106   using assms
   107 proof (induct xs arbitrary: env)
   108   case Nil
   109   then have False by simp
   110   then show ?case ..
   111 next
   112   case (Cons x xs)
   113   show ?case
   114   proof (cases env)
   115     case Val
   116     then show ?thesis by simp
   117   next
   118     case (Env b es)
   119     show ?thesis
   120     proof (cases "es x")
   121       case None
   122       with Env show ?thesis by simp
   123     next
   124       case (Some e)
   125       note es = `es x = Some e`
   126       show ?thesis
   127       proof (cases "lookup e xs")
   128         case None
   129         then have "lookup e (xs @ ys) = None" by (rule Cons.hyps)
   130         with Env Some show ?thesis by simp
   131       next
   132         case Some
   133         with Env es have False using Cons.prems by simp
   134         then show ?thesis ..
   135       qed
   136     qed
   137   qed
   138 qed
   139 
   140 theorem lookup_append_some:
   141   assumes "lookup env xs = Some e"
   142   shows "lookup env (xs @ ys) = lookup e ys"
   143   using assms
   144 proof (induct xs arbitrary: env e)
   145   case Nil
   146   then have "env = e" by simp
   147   then show "lookup env ([] @ ys) = lookup e ys" by simp
   148 next
   149   case (Cons x xs)
   150   note asm = `lookup env (x # xs) = Some e`
   151   show "lookup env ((x # xs) @ ys) = lookup e ys"
   152   proof (cases env)
   153     case (Val a)
   154     with asm have False by simp
   155     then show ?thesis ..
   156   next
   157     case (Env b es)
   158     show ?thesis
   159     proof (cases "es x")
   160       case None
   161       with asm Env have False by simp
   162       then show ?thesis ..
   163     next
   164       case (Some e')
   165       note es = `es x = Some e'`
   166       show ?thesis
   167       proof (cases "lookup e' xs")
   168         case None
   169         with asm Env es have False by simp
   170         then show ?thesis ..
   171       next
   172         case Some
   173         with asm Env es have "lookup e' xs = Some e"
   174           by simp
   175         then have "lookup e' (xs @ ys) = lookup e ys" by (rule Cons.hyps)
   176         with Env es show ?thesis by simp
   177       qed
   178     qed
   179   qed
   180 qed
   181 
   182 text {*
   183   \medskip Successful @{term lookup} deeper down an environment
   184   structure means we are able to peek further up as well.  Note that
   185   this is basically just the contrapositive statement of @{thm
   186   [source] lookup_append_none} above.
   187 *}
   188 
   189 theorem lookup_some_append:
   190   assumes "lookup env (xs @ ys) = Some e"
   191   shows "\<exists>e. lookup env xs = Some e"
   192 proof -
   193   from assms have "lookup env (xs @ ys) \<noteq> None" by simp
   194   then have "lookup env xs \<noteq> None"
   195     by (rule contrapos_nn) (simp only: lookup_append_none)
   196   then show ?thesis by (simp)
   197 qed
   198 
   199 text {*
   200   The subsequent statement describes in more detail how a successful
   201   @{term lookup} with a non-empty path results in a certain situation
   202   at any upper position.
   203 *}
   204 
   205 theorem lookup_some_upper:
   206   assumes "lookup env (xs @ y # ys) = Some e"
   207   shows "\<exists>b' es' env'.
   208     lookup env xs = Some (Env b' es') \<and>
   209     es' y = Some env' \<and>
   210     lookup env' ys = Some e"
   211   using assms
   212 proof (induct xs arbitrary: env e)
   213   case Nil
   214   from Nil.prems have "lookup env (y # ys) = Some e"
   215     by simp
   216   then obtain b' es' env' where
   217       env: "env = Env b' es'" and
   218       es': "es' y = Some env'" and
   219       look': "lookup env' ys = Some e"
   220     by (auto simp add: lookup_eq split: option.splits env.splits)
   221   from env have "lookup env [] = Some (Env b' es')" by simp
   222   with es' look' show ?case by blast
   223 next
   224   case (Cons x xs)
   225   from Cons.prems
   226   obtain b' es' env' where
   227       env: "env = Env b' es'" and
   228       es': "es' x = Some env'" and
   229       look': "lookup env' (xs @ y # ys) = Some e"
   230     by (auto simp add: lookup_eq split: option.splits env.splits)
   231   from Cons.hyps [OF look'] obtain b'' es'' env'' where
   232       upper': "lookup env' xs = Some (Env b'' es'')" and
   233       es'': "es'' y = Some env''" and
   234       look'': "lookup env'' ys = Some e"
   235     by blast
   236   from env es' upper' have "lookup env (x # xs) = Some (Env b'' es'')"
   237     by simp
   238   with es'' look'' show ?case by blast
   239 qed
   240 
   241 
   242 subsection {* The update operation *}
   243 
   244 text {*
   245   Update at a certain position in a nested environment may either
   246   delete an existing entry, or overwrite an existing one.  Note that
   247   update at undefined positions is simple absorbed, i.e.\ the
   248   environment is left unchanged.
   249 *}
   250 
   251 consts
   252   update :: "'c list => ('a, 'b, 'c) env option
   253     => ('a, 'b, 'c) env => ('a, 'b, 'c) env"
   254   update_option :: "'c list => ('a, 'b, 'c) env option
   255     => ('a, 'b, 'c) env option => ('a, 'b, 'c) env option"
   256 
   257 primrec (update)
   258   "update xs opt (Val a) =
   259     (if xs = [] then (case opt of None => Val a | Some e => e)
   260     else Val a)"
   261   "update xs opt (Env b es) =
   262     (case xs of
   263       [] => (case opt of None => Env b es | Some e => e)
   264     | y # ys => Env b (es (y := update_option ys opt (es y))))"
   265   "update_option xs opt None =
   266     (if xs = [] then opt else None)"
   267   "update_option xs opt (Some e) =
   268     (if xs = [] then opt else Some (update xs opt e))"
   269 
   270 hide const update_option
   271 
   272 text {*
   273   \medskip The characteristic cases of @{term update} are expressed by
   274   the following equalities.
   275 *}
   276 
   277 theorem update_nil_none: "update [] None env = env"
   278   by (cases env) simp_all
   279 
   280 theorem update_nil_some: "update [] (Some e) env = e"
   281   by (cases env) simp_all
   282 
   283 theorem update_cons_val: "update (x # xs) opt (Val a) = Val a"
   284   by simp
   285 
   286 theorem update_cons_nil_env:
   287     "update [x] opt (Env b es) = Env b (es (x := opt))"
   288   by (cases "es x") simp_all
   289 
   290 theorem update_cons_cons_env:
   291   "update (x # y # ys) opt (Env b es) =
   292     Env b (es (x :=
   293       (case es x of
   294         None => None
   295       | Some e => Some (update (y # ys) opt e))))"
   296   by (cases "es x") simp_all
   297 
   298 lemmas update.simps [simp del]
   299   and update_simps [simp] = update_nil_none update_nil_some
   300     update_cons_val update_cons_nil_env update_cons_cons_env
   301 
   302 lemma update_eq:
   303   "update xs opt env =
   304     (case xs of
   305       [] =>
   306         (case opt of
   307           None => env
   308         | Some e => e)
   309     | x # xs =>
   310         (case env of
   311           Val a => Val a
   312         | Env b es =>
   313             (case xs of
   314               [] => Env b (es (x := opt))
   315             | y # ys =>
   316                 Env b (es (x :=
   317                   (case es x of
   318                     None => None
   319                   | Some e => Some (update (y # ys) opt e)))))))"
   320   by (simp split: list.split env.split option.split)
   321 
   322 text {*
   323   \medskip The most basic correspondence of @{term lookup} and @{term
   324   update} states that after @{term update} at a defined position,
   325   subsequent @{term lookup} operations would yield the new value.
   326 *}
   327 
   328 theorem lookup_update_some:
   329   assumes "lookup env xs = Some e"
   330   shows "lookup (update xs (Some env') env) xs = Some env'"
   331   using assms
   332 proof (induct xs arbitrary: env e)
   333   case Nil
   334   then have "env = e" by simp
   335   then show ?case by simp
   336 next
   337   case (Cons x xs)
   338   note hyp = Cons.hyps
   339     and asm = `lookup env (x # xs) = Some e`
   340   show ?case
   341   proof (cases env)
   342     case (Val a)
   343     with asm have False by simp
   344     then show ?thesis ..
   345   next
   346     case (Env b es)
   347     show ?thesis
   348     proof (cases "es x")
   349       case None
   350       with asm Env have False by simp
   351       then show ?thesis ..
   352     next
   353       case (Some e')
   354       note es = `es x = Some e'`
   355       show ?thesis
   356       proof (cases xs)
   357         case Nil
   358         with Env show ?thesis by simp
   359       next
   360         case (Cons x' xs')
   361         from asm Env es have "lookup e' xs = Some e" by simp
   362         then have "lookup (update xs (Some env') e') xs = Some env'" by (rule hyp)
   363         with Env es Cons show ?thesis by simp
   364       qed
   365     qed
   366   qed
   367 qed
   368 
   369 text {*
   370   \medskip The properties of displaced @{term update} operations are
   371   analogous to those of @{term lookup} above.  There are two cases:
   372   below an undefined position @{term update} is absorbed altogether,
   373   and below a defined positions @{term update} affects subsequent
   374   @{term lookup} operations in the obvious way.
   375 *}
   376 
   377 theorem update_append_none:
   378   assumes "lookup env xs = None"
   379   shows "update (xs @ y # ys) opt env = env"
   380   using assms
   381 proof (induct xs arbitrary: env)
   382   case Nil
   383   then have False by simp
   384   then show ?case ..
   385 next
   386   case (Cons x xs)
   387   note hyp = Cons.hyps
   388     and asm = `lookup env (x # xs) = None`
   389   show "update ((x # xs) @ y # ys) opt env = env"
   390   proof (cases env)
   391     case (Val a)
   392     then show ?thesis by simp
   393   next
   394     case (Env b es)
   395     show ?thesis
   396     proof (cases "es x")
   397       case None
   398       note es = `es x = None`
   399       show ?thesis
   400         by (cases xs) (simp_all add: es Env fun_upd_idem_iff)
   401     next
   402       case (Some e)
   403       note es = `es x = Some e`
   404       show ?thesis
   405       proof (cases xs)
   406         case Nil
   407         with asm Env Some have False by simp
   408         then show ?thesis ..
   409       next
   410         case (Cons x' xs')
   411         from asm Env es have "lookup e xs = None" by simp
   412         then have "update (xs @ y # ys) opt e = e" by (rule hyp)
   413         with Env es Cons show "update ((x # xs) @ y # ys) opt env = env"
   414           by (simp add: fun_upd_idem_iff)
   415       qed
   416     qed
   417   qed
   418 qed
   419 
   420 theorem update_append_some:
   421   assumes "lookup env xs = Some e"
   422   shows "lookup (update (xs @ y # ys) opt env) xs = Some (update (y # ys) opt e)"
   423   using assms
   424 proof (induct xs arbitrary: env e)
   425   case Nil
   426   then have "env = e" by simp
   427   then show ?case by simp
   428 next
   429   case (Cons x xs)
   430   note hyp = Cons.hyps
   431     and asm = `lookup env (x # xs) = Some e`
   432   show "lookup (update ((x # xs) @ y # ys) opt env) (x # xs) =
   433       Some (update (y # ys) opt e)"
   434   proof (cases env)
   435     case (Val a)
   436     with asm have False by simp
   437     then show ?thesis ..
   438   next
   439     case (Env b es)
   440     show ?thesis
   441     proof (cases "es x")
   442       case None
   443       with asm Env have False by simp
   444       then show ?thesis ..
   445     next
   446       case (Some e')
   447       note es = `es x = Some e'`
   448       show ?thesis
   449       proof (cases xs)
   450         case Nil
   451         with asm Env es have "e = e'" by simp
   452         with Env es Nil show ?thesis by simp
   453       next
   454         case (Cons x' xs')
   455         from asm Env es have "lookup e' xs = Some e" by simp
   456         then have "lookup (update (xs @ y # ys) opt e') xs =
   457           Some (update (y # ys) opt e)" by (rule hyp)
   458         with Env es Cons show ?thesis by simp
   459       qed
   460     qed
   461   qed
   462 qed
   463 
   464 text {*
   465   \medskip Apparently, @{term update} does not affect the result of
   466   subsequent @{term lookup} operations at independent positions, i.e.\
   467   in case that the paths for @{term update} and @{term lookup} fork at
   468   a certain point.
   469 *}
   470 
   471 theorem lookup_update_other:
   472   assumes neq: "y \<noteq> (z::'c)"
   473   shows "lookup (update (xs @ z # zs) opt env) (xs @ y # ys) =
   474     lookup env (xs @ y # ys)"
   475 proof (induct xs arbitrary: env)
   476   case Nil
   477   show ?case
   478   proof (cases env)
   479     case Val
   480     then show ?thesis by simp
   481   next
   482     case Env
   483     show ?thesis
   484     proof (cases zs)
   485       case Nil
   486       with neq Env show ?thesis by simp
   487     next
   488       case Cons
   489       with neq Env show ?thesis by simp
   490     qed
   491   qed
   492 next
   493   case (Cons x xs)
   494   note hyp = Cons.hyps
   495   show ?case
   496   proof (cases env)
   497     case Val
   498     then show ?thesis by simp
   499   next
   500     case (Env y es)
   501     show ?thesis
   502     proof (cases xs)
   503       case Nil
   504       show ?thesis
   505       proof (cases "es x")
   506         case None
   507         with Env Nil show ?thesis by simp
   508       next
   509         case Some
   510         with neq hyp and Env Nil show ?thesis by simp
   511       qed
   512     next
   513       case (Cons x' xs')
   514       show ?thesis
   515       proof (cases "es x")
   516         case None
   517         with Env Cons show ?thesis by simp
   518       next
   519         case Some
   520         with neq hyp and Env Cons show ?thesis by simp
   521       qed
   522     qed
   523   qed
   524 qed
   525 
   526 text {* Environments and code generation *}
   527 
   528 lemma [code, code del]:
   529   fixes e1 e2 :: "('b\<Colon>eq, 'a\<Colon>eq, 'c\<Colon>eq) env"
   530   shows "eq_class.eq e1 e2 \<longleftrightarrow> eq_class.eq e1 e2" ..
   531 
   532 lemma eq_env_code [code]:
   533   fixes x y :: "'a\<Colon>eq"
   534     and f g :: "'c\<Colon>{eq, finite} \<Rightarrow> ('b\<Colon>eq, 'a, 'c) env option"
   535   shows "eq_class.eq (Env x f) (Env y g) \<longleftrightarrow>
   536   eq_class.eq x y \<and> (\<forall>z\<in>UNIV. case f z
   537    of None \<Rightarrow> (case g z
   538         of None \<Rightarrow> True | Some _ \<Rightarrow> False)
   539     | Some a \<Rightarrow> (case g z
   540         of None \<Rightarrow> False | Some b \<Rightarrow> eq_class.eq a b))" (is ?env)
   541     and "eq_class.eq (Val a) (Val b) \<longleftrightarrow> eq_class.eq a b"
   542     and "eq_class.eq (Val a) (Env y g) \<longleftrightarrow> False"
   543     and "eq_class.eq (Env x f) (Val b) \<longleftrightarrow> False"
   544 proof (unfold eq)
   545   have "f = g \<longleftrightarrow> (\<forall>z. case f z
   546    of None \<Rightarrow> (case g z
   547         of None \<Rightarrow> True | Some _ \<Rightarrow> False)
   548     | Some a \<Rightarrow> (case g z
   549         of None \<Rightarrow> False | Some b \<Rightarrow> a = b))" (is "?lhs = ?rhs")
   550   proof
   551     assume ?lhs
   552     then show ?rhs by (auto split: option.splits)
   553   next
   554     assume assm: ?rhs (is "\<forall>z. ?prop z")
   555     show ?lhs 
   556     proof
   557       fix z
   558       from assm have "?prop z" ..
   559       then show "f z = g z" by (auto split: option.splits)
   560     qed
   561   qed
   562   then show "Env x f = Env y g \<longleftrightarrow>
   563     x = y \<and> (\<forall>z\<in>UNIV. case f z
   564      of None \<Rightarrow> (case g z
   565           of None \<Rightarrow> True | Some _ \<Rightarrow> False)
   566       | Some a \<Rightarrow> (case g z
   567           of None \<Rightarrow> False | Some b \<Rightarrow> a = b))" by simp
   568 qed simp_all
   569 
   570 lemma [code, code del]:
   571   "(Code_Eval.term_of :: ('a::{term_of, type}, 'b::{term_of, type}, 'c::{term_of, type}) env \<Rightarrow> term) = Code_Eval.term_of" ..
   572 
   573 end