1(* Title: HOL/Unix/Nested_Environment.thy 2 Author: Markus Wenzel, TU Muenchen 3*) 4 5section \<open>Nested environments\<close> 6 7theory Nested_Environment 8imports Main 9begin 10 11text \<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 21datatype (dead 'a, dead 'b, dead 'c) env = 22 Val 'a 23 | Env 'b "'c \<Rightarrow> ('a, 'b, 'c) env option" 24 25text \<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 36subsection \<open>The lookup operation\<close> 37 38text \<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 45primrec 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" 47where 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 56hide_const lookup_option 57 58text \<open> 59 \<^medskip> 60 The characteristic cases of @{term lookup} are expressed by the following 61 equalities. 62\<close> 63 64theorem lookup_nil: "lookup e [] = Some e" 65 by (cases e) simp_all 66 67theorem lookup_val_cons: "lookup (Val a) (x # xs) = None" 68 by simp 69 70theorem 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 77lemmas lookup.simps [simp del] lookup_option.simps [simp del] 78 and lookup_simps [simp] = lookup_nil lookup_val_cons lookup_env_cons 79 80theorem 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 93text \<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 100theorem lookup_append_none: 101 assumes "lookup env xs = None" 102 shows "lookup env (xs @ ys) = None" 103 using assms 104proof (induct xs arbitrary: env) 105 case Nil 106 then have False by simp 107 then show ?case .. 108next 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 135qed 136 137theorem lookup_append_some: 138 assumes "lookup env xs = Some e" 139 shows "lookup env (xs @ ys) = lookup e ys" 140 using assms 141proof (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 145next 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 177qed 178 179text \<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 186theorem lookup_some_append: 187 assumes "lookup env (xs @ ys) = Some e" 188 shows "\<exists>e. lookup env xs = Some e" 189proof - 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) 194qed 195 196text \<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 202theorem 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 209proof (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 220next 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 236qed 237 238 239subsection \<open>The update operation\<close> 240 241text \<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 247primrec 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" 251where 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 264hide_const update_option 265 266text \<open> 267 \<^medskip> 268 The characteristic cases of @{term update} are expressed by the following 269 equalities. 270\<close> 271 272theorem update_nil_none: "update [] None env = env" 273 by (cases env) simp_all 274 275theorem update_nil_some: "update [] (Some e) env = e" 276 by (cases env) simp_all 277 278theorem update_cons_val: "update (x # xs) opt (Val a) = Val a" 279 by simp 280 281theorem update_cons_nil_env: 282 "update [x] opt (Env b es) = Env b (es (x := opt))" 283 by (cases "es x") simp_all 284 285theorem 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 293lemmas 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 297lemma 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 317text \<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 324theorem lookup_update_some: 325 assumes "lookup env xs = Some e" 326 shows "lookup (update xs (Some env') env) xs = Some env'" 327 using assms 328proof (induct xs arbitrary: env e) 329 case Nil 330 then have "env = e" by simp 331 then show ?case by simp 332next 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 363qed 364 365text \<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 373theorem update_append_none: 374 assumes "lookup env xs = None" 375 shows "update (xs @ y # ys) opt env = env" 376 using assms 377proof (induct xs arbitrary: env) 378 case Nil 379 then have False by simp 380 then show ?case .. 381next 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 414qed 415 416theorem 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 420proof (induct xs arbitrary: env e) 421 case Nil 422 then have "env = e" by simp 423 then show ?case by simp 424next 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 458qed 459 460text \<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 467theorem 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)" 471proof (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 488next 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 520qed 521 522 523subsection \<open>Code generation\<close> 524 525lemma 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" 537proof (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 559qed simp_all 560 561lemma [code nbe]: "HOL.equal (x :: (_, _, _) env) x \<longleftrightarrow> True" 562 by (fact equal_refl) 563 564end 565