src/HOL/Unix/Nested_Environment.thy
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (20 months ago)
changeset 67003 49850a679c2c
parent 66148 5e60c2d0a1f1
child 69597 ff784d5a5bfb
permissions -rw-r--r--
more robust sorted_entries;
     1 (*  Title:      HOL/Unix/Nested_Environment.thy
     2     Author:     Markus Wenzel, TU Muenchen
     3 *)
     4 
     5 section \<open>Nested environments\<close>
     6 
     7 theory Nested_Environment
     8 imports Main
     9 begin
    10 
    11 text \<open>
    12   Consider a partial function @{term [source] "e :: 'a \<Rightarrow> 'b option"}; this may
    13   be understood as an \<^emph>\<open>environment\<close> mapping indexes @{typ 'a} to optional
    14   entry values @{typ 'b} (cf.\ the basic theory \<open>Map\<close> of Isabelle/HOL). This
    15   basic idea is easily generalized to that of a \<^emph>\<open>nested environment\<close>, where
    16   entries may be either basic values or again proper environments. Then each
    17   entry is accessed by a \<^emph>\<open>path\<close>, i.e.\ a list of indexes leading to its
    18   position within the structure.
    19 \<close>
    20 
    21 datatype (dead 'a, dead 'b, dead 'c) env =
    22     Val 'a
    23   | Env 'b  "'c \<Rightarrow> ('a, 'b, 'c) env option"
    24 
    25 text \<open>
    26   \<^medskip>
    27   In the type @{typ "('a, 'b, 'c) env"} the parameter @{typ 'a} refers to
    28   basic values (occurring in terminal positions), type @{typ 'b} to values
    29   associated with proper (inner) environments, and type @{typ 'c} with the
    30   index type for branching. Note that there is no restriction on any of these
    31   types. In particular, arbitrary branching may yield rather large
    32   (transfinite) tree structures.
    33 \<close>
    34 
    35 
    36 subsection \<open>The lookup operation\<close>
    37 
    38 text \<open>
    39   Lookup in nested environments works by following a given path of index
    40   elements, leading to an optional result (a terminal value or nested
    41   environment). A \<^emph>\<open>defined position\<close> within a nested environment is one where
    42   @{term lookup} at its path does not yield @{term None}.
    43 \<close>
    44 
    45 primrec lookup :: "('a, 'b, 'c) env \<Rightarrow> 'c list \<Rightarrow> ('a, 'b, 'c) env option"
    46   and lookup_option :: "('a, 'b, 'c) env option \<Rightarrow> 'c list \<Rightarrow> ('a, 'b, 'c) env option"
    47 where
    48     "lookup (Val a) xs = (if xs = [] then Some (Val a) else None)"
    49   | "lookup (Env b es) xs =
    50       (case xs of
    51         [] \<Rightarrow> Some (Env b es)
    52       | y # ys \<Rightarrow> lookup_option (es y) ys)"
    53   | "lookup_option None xs = None"
    54   | "lookup_option (Some e) xs = lookup e xs"
    55 
    56 hide_const lookup_option
    57 
    58 text \<open>
    59   \<^medskip>
    60   The characteristic cases of @{term lookup} are expressed by the following
    61   equalities.
    62 \<close>
    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 \<Rightarrow> None
    74     | Some e \<Rightarrow> lookup e xs)"
    75   by (cases "es x") simp_all
    76 
    77 lemmas lookup.simps [simp del] 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       [] \<Rightarrow> Some env
    84     | x # xs \<Rightarrow>
    85       (case env of
    86         Val a \<Rightarrow> None
    87       | Env b es \<Rightarrow>
    88           (case es x of
    89             None \<Rightarrow> None
    90           | Some e \<Rightarrow> lookup e xs)))"
    91   by (simp split: list.split env.split)
    92 
    93 text \<open>
    94   \<^medskip>
    95   Displaced @{term lookup} operations, relative to a certain base path prefix,
    96   may be reduced as follows. There are two cases, depending whether the
    97   environment actually extends far enough to follow the base path.
    98 \<close>
    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 = \<open>es x = Some e\<close>
   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 = \<open>lookup env (x # xs) = Some e\<close>
   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 = \<open>es x = Some e'\<close>
   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 \<open>
   180   \<^medskip>
   181   Successful @{term lookup} deeper down an environment structure means we are
   182   able to peek further up as well. Note that this is basically just the
   183   contrapositive statement of @{thm [source] lookup_append_none} above.
   184 \<close>
   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 \<open>
   197   The subsequent statement describes in more detail how a successful @{term
   198   lookup} with a non-empty path results in a certain situation at any upper
   199   position.
   200 \<close>
   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 \<open>The update operation\<close>
   240 
   241 text \<open>
   242   Update at a certain position in a nested environment may either delete an
   243   existing entry, or overwrite an existing one. Note that update at undefined
   244   positions is simple absorbed, i.e.\ the environment is left unchanged.
   245 \<close>
   246 
   247 primrec update :: "'c list \<Rightarrow> ('a, 'b, 'c) env option \<Rightarrow>
   248     ('a, 'b, 'c) env \<Rightarrow> ('a, 'b, 'c) env"
   249   and update_option :: "'c list \<Rightarrow> ('a, 'b, 'c) env option \<Rightarrow>
   250     ('a, 'b, 'c) env option \<Rightarrow> ('a, 'b, 'c) env option"
   251 where
   252   "update xs opt (Val a) =
   253     (if xs = [] then (case opt of None \<Rightarrow> Val a | Some e \<Rightarrow> e)
   254      else Val a)"
   255 | "update xs opt (Env b es) =
   256     (case xs of
   257       [] \<Rightarrow> (case opt of None \<Rightarrow> Env b es | Some e \<Rightarrow> e)
   258     | y # ys \<Rightarrow> Env b (es (y := update_option ys opt (es y))))"
   259 | "update_option xs opt None =
   260     (if xs = [] then opt else None)"
   261 | "update_option xs opt (Some e) =
   262     (if xs = [] then opt else Some (update xs opt e))"
   263 
   264 hide_const update_option
   265 
   266 text \<open>
   267   \<^medskip>
   268   The characteristic cases of @{term update} are expressed by the following
   269   equalities.
   270 \<close>
   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 \<Rightarrow> None
   290       | Some e \<Rightarrow> Some (update (y # ys) opt e))))"
   291   by (cases "es x") simp_all
   292 
   293 lemmas update.simps [simp del] 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       [] \<Rightarrow>
   301         (case opt of
   302           None \<Rightarrow> env
   303         | Some e \<Rightarrow> e)
   304     | x # xs \<Rightarrow>
   305         (case env of
   306           Val a \<Rightarrow> Val a
   307         | Env b es \<Rightarrow>
   308             (case xs of
   309               [] \<Rightarrow> Env b (es (x := opt))
   310             | y # ys \<Rightarrow>
   311                 Env b (es (x :=
   312                   (case es x of
   313                     None \<Rightarrow> None
   314                   | Some e \<Rightarrow> Some (update (y # ys) opt e)))))))"
   315   by (simp split: list.split env.split option.split)
   316 
   317 text \<open>
   318   \<^medskip>
   319   The most basic correspondence of @{term lookup} and @{term update} states
   320   that after @{term update} at a defined position, subsequent @{term lookup}
   321   operations would yield the new value.
   322 \<close>
   323 
   324 theorem lookup_update_some:
   325   assumes "lookup env xs = Some e"
   326   shows "lookup (update xs (Some env') env) xs = Some env'"
   327   using assms
   328 proof (induct xs arbitrary: env e)
   329   case Nil
   330   then have "env = e" by simp
   331   then show ?case by simp
   332 next
   333   case (Cons x xs)
   334   note hyp = Cons.hyps
   335     and asm = \<open>lookup env (x # xs) = Some e\<close>
   336   show ?case
   337   proof (cases env)
   338     case (Val a)
   339     with asm have False by simp
   340     then show ?thesis ..
   341   next
   342     case (Env b es)
   343     show ?thesis
   344     proof (cases "es x")
   345       case None
   346       with asm Env have False by simp
   347       then show ?thesis ..
   348     next
   349       case (Some e')
   350       note es = \<open>es x = Some e'\<close>
   351       show ?thesis
   352       proof (cases xs)
   353         case Nil
   354         with Env show ?thesis by simp
   355       next
   356         case (Cons x' xs')
   357         from asm Env es have "lookup e' xs = Some e" by simp
   358         then have "lookup (update xs (Some env') e') xs = Some env'" by (rule hyp)
   359         with Env es Cons show ?thesis by simp
   360       qed
   361     qed
   362   qed
   363 qed
   364 
   365 text \<open>
   366   \<^medskip>
   367   The properties of displaced @{term update} operations are analogous to those
   368   of @{term lookup} above. There are two cases: below an undefined position
   369   @{term update} is absorbed altogether, and below a defined positions @{term
   370   update} affects subsequent @{term lookup} operations in the obvious way.
   371 \<close>
   372 
   373 theorem update_append_none:
   374   assumes "lookup env xs = None"
   375   shows "update (xs @ y # ys) opt env = env"
   376   using assms
   377 proof (induct xs arbitrary: env)
   378   case Nil
   379   then have False by simp
   380   then show ?case ..
   381 next
   382   case (Cons x xs)
   383   note hyp = Cons.hyps
   384     and asm = \<open>lookup env (x # xs) = None\<close>
   385   show "update ((x # xs) @ y # ys) opt env = env"
   386   proof (cases env)
   387     case (Val a)
   388     then show ?thesis by simp
   389   next
   390     case (Env b es)
   391     show ?thesis
   392     proof (cases "es x")
   393       case None
   394       note es = \<open>es x = None\<close>
   395       show ?thesis
   396         by (cases xs) (simp_all add: es Env fun_upd_idem_iff)
   397     next
   398       case (Some e)
   399       note es = \<open>es x = Some e\<close>
   400       show ?thesis
   401       proof (cases xs)
   402         case Nil
   403         with asm Env Some have False by simp
   404         then show ?thesis ..
   405       next
   406         case (Cons x' xs')
   407         from asm Env es have "lookup e xs = None" by simp
   408         then have "update (xs @ y # ys) opt e = e" by (rule hyp)
   409         with Env es Cons show "update ((x # xs) @ y # ys) opt env = env"
   410           by (simp add: fun_upd_idem_iff)
   411       qed
   412     qed
   413   qed
   414 qed
   415 
   416 theorem update_append_some:
   417   assumes "lookup env xs = Some e"
   418   shows "lookup (update (xs @ y # ys) opt env) xs = Some (update (y # ys) opt e)"
   419   using assms
   420 proof (induct xs arbitrary: env e)
   421   case Nil
   422   then have "env = e" by simp
   423   then show ?case by simp
   424 next
   425   case (Cons x xs)
   426   note hyp = Cons.hyps
   427     and asm = \<open>lookup env (x # xs) = Some e\<close>
   428   show "lookup (update ((x # xs) @ y # ys) opt env) (x # xs) =
   429       Some (update (y # ys) opt e)"
   430   proof (cases env)
   431     case (Val a)
   432     with asm have False by simp
   433     then show ?thesis ..
   434   next
   435     case (Env b es)
   436     show ?thesis
   437     proof (cases "es x")
   438       case None
   439       with asm Env have False by simp
   440       then show ?thesis ..
   441     next
   442       case (Some e')
   443       note es = \<open>es x = Some e'\<close>
   444       show ?thesis
   445       proof (cases xs)
   446         case Nil
   447         with asm Env es have "e = e'" by simp
   448         with Env es Nil show ?thesis by simp
   449       next
   450         case (Cons x' xs')
   451         from asm Env es have "lookup e' xs = Some e" by simp
   452         then have "lookup (update (xs @ y # ys) opt e') xs =
   453           Some (update (y # ys) opt e)" by (rule hyp)
   454         with Env es Cons show ?thesis by simp
   455       qed
   456     qed
   457   qed
   458 qed
   459 
   460 text \<open>
   461   \<^medskip>
   462   Apparently, @{term update} does not affect the result of subsequent @{term
   463   lookup} operations at independent positions, i.e.\ in case that the paths
   464   for @{term update} and @{term lookup} fork at a certain point.
   465 \<close>
   466 
   467 theorem lookup_update_other:
   468   assumes neq: "y \<noteq> (z::'c)"
   469   shows "lookup (update (xs @ z # zs) opt env) (xs @ y # ys) =
   470     lookup env (xs @ y # ys)"
   471 proof (induct xs arbitrary: env)
   472   case Nil
   473   show ?case
   474   proof (cases env)
   475     case Val
   476     then show ?thesis by simp
   477   next
   478     case Env
   479     show ?thesis
   480     proof (cases zs)
   481       case Nil
   482       with neq Env show ?thesis by simp
   483     next
   484       case Cons
   485       with neq Env show ?thesis by simp
   486     qed
   487   qed
   488 next
   489   case (Cons x xs)
   490   note hyp = Cons.hyps
   491   show ?case
   492   proof (cases env)
   493     case Val
   494     then show ?thesis by simp
   495   next
   496     case (Env y es)
   497     show ?thesis
   498     proof (cases xs)
   499       case Nil
   500       show ?thesis
   501       proof (cases "es x")
   502         case None
   503         with Env Nil show ?thesis by simp
   504       next
   505         case Some
   506         with neq hyp and Env Nil show ?thesis by simp
   507       qed
   508     next
   509       case (Cons x' xs')
   510       show ?thesis
   511       proof (cases "es x")
   512         case None
   513         with Env Cons show ?thesis by simp
   514       next
   515         case Some
   516         with neq hyp and Env Cons show ?thesis by simp
   517       qed
   518     qed
   519   qed
   520 qed
   521 
   522 
   523 subsection \<open>Code generation\<close>
   524 
   525 lemma equal_env_code [code]:
   526   fixes x y :: "'a::equal"
   527     and f g :: "'c::{equal, finite} \<Rightarrow> ('b::equal, 'a, 'c) env option"
   528   shows
   529     "HOL.equal (Env x f) (Env y g) \<longleftrightarrow>
   530       HOL.equal x y \<and> (\<forall>z \<in> UNIV.
   531         case f z of
   532           None \<Rightarrow> (case g z of None \<Rightarrow> True | Some _ \<Rightarrow> False)
   533         | Some a \<Rightarrow> (case g z of None \<Rightarrow> False | Some b \<Rightarrow> HOL.equal a b))" (is ?env)
   534     and "HOL.equal (Val a) (Val b) \<longleftrightarrow> HOL.equal a b"
   535     and "HOL.equal (Val a) (Env y g) \<longleftrightarrow> False"
   536     and "HOL.equal (Env x f) (Val b) \<longleftrightarrow> False"
   537 proof (unfold equal)
   538   have "f = g \<longleftrightarrow>
   539     (\<forall>z. case f z of
   540       None \<Rightarrow> (case g z of None \<Rightarrow> True | Some _ \<Rightarrow> False)
   541     | Some a \<Rightarrow> (case g z of None \<Rightarrow> False | Some b \<Rightarrow> a = b))" (is "?lhs = ?rhs")
   542   proof
   543     assume ?lhs
   544     then show ?rhs by (auto split: option.splits)
   545   next
   546     assume ?rhs (is "\<forall>z. ?prop z")
   547     show ?lhs
   548     proof
   549       fix z
   550       from \<open>?rhs\<close> have "?prop z" ..
   551       then show "f z = g z" by (auto split: option.splits)
   552     qed
   553   qed
   554   then show "Env x f = Env y g \<longleftrightarrow>
   555     x = y \<and> (\<forall>z \<in> UNIV.
   556       case f z of
   557         None \<Rightarrow> (case g z of None \<Rightarrow> True | Some _ \<Rightarrow> False)
   558       | Some a \<Rightarrow> (case g z of None \<Rightarrow> False | Some b \<Rightarrow> a = b))" by simp
   559 qed simp_all
   560 
   561 lemma [code nbe]: "HOL.equal (x :: (_, _, _) env) x \<longleftrightarrow> True"
   562   by (fact equal_refl)
   563 
   564 end