# HG changeset patch
# User wenzelm
# Date 995659206 -7200
# Node ID 3f74b80d979f7d3ffe2d7bc3c4029ea862ce3591
# Parent  bd1a7f53c11b759bf148ef5cad68415990b6db24
private "myinv" (uses "The" instead of "Eps");

diff -r bd1a7f53c11b -r 3f74b80d979f src/HOL/Inductive.thy
--- 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"