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