# HG changeset patch
# User wenzelm
# Date 972064013 -7200
# Node ID ec98fc455272244c6afcfcc8fbf7c093d0b6d909
# Parent  ff003e2b790c1f09fe2c534ada25689f06b36752
tuned;

diff -r ff003e2b790c -r ec98fc455272 src/HOL/subset.thy
--- a/src/HOL/subset.thy	Fri Oct 20 14:17:08 2000 +0200
+++ b/src/HOL/subset.thy	Fri Oct 20 19:46:53 2000 +0200
@@ -50,6 +50,24 @@
   qed
 qed
 
+theorem Abs_inject:
+  "type_definition Rep Abs A ==> x \<in> A ==> y \<in> A ==> (Abs x = Abs y) = (x = y)"
+proof -
+  assume tydef: "type_definition Rep Abs A"
+  assume x: "x \<in> A" and y: "y \<in> A"
+  show ?thesis
+  proof
+    assume "Abs x = Abs y"
+    hence "Rep (Abs x) = Rep (Abs y)" by simp
+    moreover note x hence "Rep (Abs x) = x" by (rule Abs_inverse [OF tydef])
+    moreover note y hence "Rep (Abs y) = y" by (rule Abs_inverse [OF tydef])
+    ultimately show "x = y" by (simp only:)
+  next
+    assume "x = y"
+    thus "Abs x = Abs y" by simp
+  qed
+qed
+
 theorem Rep_cases:
   "type_definition Rep Abs A ==> y \<in> A ==> (!!x. y = Rep x ==> P) ==> P"
 proof -
@@ -75,24 +93,6 @@
   qed
 qed
 
-theorem Abs_inject:
-  "type_definition Rep Abs A ==> x \<in> A ==> y \<in> A ==> (Abs x = Abs y) = (x = y)"
-proof -
-  assume tydef: "type_definition Rep Abs A"
-  assume x: "x \<in> A" and y: "y \<in> A"
-  show ?thesis
-  proof
-    assume "Abs x = Abs y"
-    hence "Rep (Abs x) = Rep (Abs y)" by simp
-    moreover note x hence "Rep (Abs x) = x" by (rule Abs_inverse [OF tydef])
-    moreover note y hence "Rep (Abs y) = y" by (rule Abs_inverse [OF tydef])
-    ultimately show "x = y" by (simp only:)
-  next
-    assume "x = y"
-    thus "Abs x = Abs y" by simp
-  qed
-qed
-
 theorem Rep_induct:
   "type_definition Rep Abs A ==> y \<in> A ==> (!!x. P (Rep x)) ==> P y"
 proof -