summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Fri, 20 Jul 2001 22:00:06 +0200 | |

changeset 11436 | 3f74b80d979f |

parent 11435 | bd1a7f53c11b |

child 11437 | 2338bce575ae |

private "myinv" (uses "The" instead of "Eps");

--- a/src/HOL/Inductive.thy Fri Jul 20 21:59:11 2001 +0200 +++ b/src/HOL/Inductive.thy Fri Jul 20 22:00:06 2001 +0200 @@ -56,6 +56,38 @@ hide const forall implies equal conj +(* inversion of injective functions *) + +constdefs + myinv :: "('a => 'b) => ('b => 'a)" + "myinv (f :: 'a => 'b) == \<lambda>y. THE x. f x = y" + +lemma myinv_f_f: "inj f ==> myinv f (f x) = x" +proof - + assume "inj f" + hence "(THE x'. f x' = f x) = (THE x'. x' = x)" + by (simp only: inj_eq) + also have "... = x" by (rule the_eq_trivial) + finally (trans) show ?thesis by (unfold myinv_def) +qed + +lemma f_myinv_f: "inj f ==> y \<in> range f ==> f (myinv f y) = y" +proof (unfold myinv_def) + assume inj: "inj f" + assume "y \<in> range f" + then obtain x where "y = f x" .. + hence x: "f x = y" .. + thus "f (THE x. f x = y) = y" + proof (rule theI) + fix x' assume "f x' = y" + with x have "f x' = f x" by simp + with inj show "x' = x" by (rule injD) + qed +qed + +hide const myinv + + (* setup packages *) use "Tools/induct_method.ML"