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