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

src/HOL/Inductive.thy

changeset 11436 | 3f74b80d979f |

parent 11325 | a5e0289dd56c |

child 11439 | 9aaab1a160a5 |

--- 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"