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

src/HOL/Inductive.thy

changeset 11439 | 9aaab1a160a5 |

parent 11436 | 3f74b80d979f |

child 11688 | 56833637db2a |

equal
deleted
inserted
replaced

11438:3d9222b80989 | 11439:9aaab1a160a5 |
---|---|

66 proof - |
66 proof - |

67 assume "inj f" |
67 assume "inj f" |

68 hence "(THE x'. f x' = f x) = (THE x'. x' = x)" |
68 hence "(THE x'. f x' = f x) = (THE x'. x' = x)" |

69 by (simp only: inj_eq) |
69 by (simp only: inj_eq) |

70 also have "... = x" by (rule the_eq_trivial) |
70 also have "... = x" by (rule the_eq_trivial) |

71 finally (trans) show ?thesis by (unfold myinv_def) |
71 finally show ?thesis by (unfold myinv_def) |

72 qed |
72 qed |

73 |
73 |

74 lemma f_myinv_f: "inj f ==> y \<in> range f ==> f (myinv f y) = y" |
74 lemma f_myinv_f: "inj f ==> y \<in> range f ==> f (myinv f y) = y" |

75 proof (unfold myinv_def) |
75 proof (unfold myinv_def) |

76 assume inj: "inj f" |
76 assume inj: "inj f" |