equal
deleted
inserted
replaced
448 next |
448 next |
449 case rmdir |
449 case rmdir |
450 with root' show ?thesis by cases auto |
450 with root' show ?thesis by cases auto |
451 next |
451 next |
452 case readdir |
452 case readdir |
453 with root' show ?thesis by cases fastforce+ |
453 with root' show ?thesis by cases blast+ |
454 qed |
454 qed |
455 |
455 |
456 text {* |
456 text {* |
457 \medskip Apparently, file-system transitions are \emph{type-safe} in |
457 \medskip Apparently, file-system transitions are \emph{type-safe} in |
458 the sense that the result of transforming an actual directory yields |
458 the sense that the result of transforming an actual directory yields |
1026 also from lookup have "\<dots> = lookup root (path @ [y])" |
1026 also from lookup have "\<dots> = lookup root (path @ [y])" |
1027 by (simp only: lookup_append_some) |
1027 by (simp only: lookup_append_some) |
1028 also have "\<dots> \<noteq> None" |
1028 also have "\<dots> \<noteq> None" |
1029 proof - |
1029 proof - |
1030 from ys obtain us u where rev_ys: "ys = us @ [u]" |
1030 from ys obtain us u where rev_ys: "ys = us @ [u]" |
1031 by (cases ys rule: rev_cases) fastforce+ |
1031 by (cases ys rule: rev_cases) simp |
1032 with tr path |
1032 with tr path |
1033 have "lookup root ((path @ [y]) @ (us @ [u])) \<noteq> None \<or> |
1033 have "lookup root ((path @ [y]) @ (us @ [u])) \<noteq> None \<or> |
1034 lookup root ((path @ [y]) @ us) \<noteq> None" |
1034 lookup root ((path @ [y]) @ us) \<noteq> None" |
1035 by cases (auto dest: access_some_lookup) |
1035 by cases (auto dest: access_some_lookup) |
1036 then show ?thesis |
1036 then show ?thesis |