--- a/src/HOL/Inductive.thy Sat Jul 04 23:25:28 2009 +0200
+++ b/src/HOL/Inductive.thy Mon Jul 06 14:19:13 2009 +0200
@@ -258,38 +258,6 @@
subsection {* Inductive predicates and sets *}
-text {* 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 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
-
-
text {* Package setup. *}
theorems basic_monos =