src/HOL/Library/Nested_Environment.thy
 author haftmann Mon Jul 07 08:47:17 2008 +0200 (2008-07-07) changeset 27487 c8a6ce181805 parent 27368 9f90ac19e32b child 28228 7ebe8dc06cbb permissions -rw-r--r--
absolute imports of HOL/*.thy theories
     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"

    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 {* Equality of environments for code generation *}

   527

   528 lemma [code func, code func 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 func]:

   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 end