summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Unix/Unix.thy

changeset 11004 | af8008e4de96 |

parent 10979 | 3da4543034e7 |

child 11072 | 8f47967ecc80 |

equal
deleted
inserted
replaced

11003:ee0838d89deb | 11004:af8008e4de96 |
---|---|

973 \medskip At last we are left with the main effort to show that the |
973 \medskip At last we are left with the main effort to show that the |

974 ``bogosity'' invariant is preserved by any file-system operation |
974 ``bogosity'' invariant is preserved by any file-system operation |

975 performed by @{term user1} alone. Note that this holds for any |
975 performed by @{term user1} alone. Note that this holds for any |

976 @{term path} given, the particular @{term bogus_path} is not |
976 @{term path} given, the particular @{term bogus_path} is not |

977 required here. |
977 required here. |

978 *} (* FIXME The overall structure of the proof is as follows \dots *) |
978 *} |

979 |
979 |

980 lemma preserve_invariant: "root \<midarrow>x\<rightarrow> root' \<Longrightarrow> |
980 lemma preserve_invariant: "root \<midarrow>x\<rightarrow> root' \<Longrightarrow> |

981 invariant root path \<Longrightarrow> uid_of x = user1 \<Longrightarrow> invariant root' path" |
981 invariant root path \<Longrightarrow> uid_of x = user1 \<Longrightarrow> invariant root' path" |

982 proof - |
982 proof - |

983 assume tr: "root \<midarrow>x\<rightarrow> root'" |
983 assume tr: "root \<midarrow>x\<rightarrow> root'" |