# HG changeset patch
# User nipkow
# Date 1182343104 -7200
# Node ID c2c10abd2a1e5f244c65ee84a99a700adf82da23
# Parent  cec811764a388cd6908ff401d88b8d4af263a060
added lemmas

diff -r cec811764a38 -r c2c10abd2a1e src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Wed Jun 20 08:09:56 2007 +0200
+++ b/src/HOL/Hilbert_Choice.thy	Wed Jun 20 14:38:24 2007 +0200
@@ -126,6 +126,16 @@
 apply (blast intro: inj_on_inverseI inv_f_f)
 done
 
+lemma inv_o_cancel[simp]: "inj f ==> inv f o f = id"
+by (simp add: inj_iff)
+
+lemma o_inv_o_cancel[simp]: "inj f ==> g o inv f o f = g"
+by (simp add: o_assoc[symmetric])
+
+lemma inv_image_cancel[simp]:
+  "inj f ==> inv f ` f ` S = S"
+by (simp add: image_compose[symmetric])
+ 
 lemma inj_imp_surj_inv: "inj f ==> surj (inv f)"
 by (blast intro: surjI inv_f_f)
 
diff -r cec811764a38 -r c2c10abd2a1e src/HOL/Typedef.thy
--- a/src/HOL/Typedef.thy	Wed Jun 20 08:09:56 2007 +0200
+++ b/src/HOL/Typedef.thy	Wed Jun 20 14:38:24 2007 +0200
@@ -90,6 +90,23 @@
   finally show "P x" .
 qed
 
+lemma Rep_range:
+assumes "type_definition Rep Abs A"
+shows "range Rep = A"
+proof -
+  from assms have A1: "!!x. Rep x : A"
+              and A2: "!!y. y : A ==> y = Rep(Abs y)"
+     by (auto simp add: type_definition_def)
+  have "range Rep <= A" using A1 by (auto simp add: image_def)
+  moreover have "A <= range Rep"
+  proof
+    fix x assume "x : A"
+    hence "x = Rep (Abs x)" by (rule A2)
+    thus "x : range Rep" by (auto simp add: image_def)
+  qed
+  ultimately show ?thesis ..
+qed
+
 end
 
 use "Tools/typedef_package.ML"