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