author wenzelm Fri, 20 Oct 2000 19:46:53 +0200 changeset 10284 ec98fc455272 parent 10283 ff003e2b790c child 10285 6949e17f314a
tuned;
 src/HOL/subset.thy file | annotate | diff | comparison | revisions
```--- 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 -```