# HG changeset patch
# User huffman
# Date 1213984740 -7200
# Node ID eec7a1889ca5d154ec7cb0c9bb8ef91c3857e51a
# Parent  cfe5244301dd661c78eaf38d0234dc5cd63bc38a
moved Abs_image to Typedef.thy; prove finite_UNIV outside the locale

diff -r cfe5244301dd -r eec7a1889ca5 src/HOLCF/Pcpodef.thy
--- a/src/HOLCF/Pcpodef.thy	Fri Jun 20 19:57:45 2008 +0200
+++ b/src/HOLCF/Pcpodef.thy	Fri Jun 20 19:59:00 2008 +0200
@@ -31,36 +31,23 @@
 
 subsection {* Proving a subtype is finite *}
 
-context type_definition
-begin
-
-lemma Abs_image:
-  shows "Abs ` A = UNIV"
-proof
-  show "Abs ` A <= UNIV" by simp
-  show "UNIV <= Abs ` A"
-  proof
-    fix x
-    have "x = Abs (Rep x)" by (rule Rep_inverse [symmetric])
-    thus "x : Abs ` A" using Rep by (rule image_eqI)
-  qed
-qed
-
-lemma finite_UNIV: "finite A \<Longrightarrow> finite (UNIV :: 'b set)"
+lemma typedef_finite_UNIV:
+  fixes Abs :: "'a::type \<Rightarrow> 'b::type"
+  assumes type: "type_definition Rep Abs A"
+  shows "finite A \<Longrightarrow> finite (UNIV :: 'b set)"
 proof -
   assume "finite A"
   hence "finite (Abs ` A)" by (rule finite_imageI)
-  thus "finite (UNIV :: 'b set)" by (simp only: Abs_image)
+  thus "finite (UNIV :: 'b set)"
+    by (simp only: type_definition.Abs_image [OF type])
 qed
 
-end
-
 theorem typedef_finite_po:
   fixes Abs :: "'a::finite_po \<Rightarrow> 'b::po"
   assumes type: "type_definition Rep Abs A"
   shows "OFCLASS('b, finite_po_class)"
  apply (intro_classes)
- apply (rule type_definition.finite_UNIV [OF type])
+ apply (rule typedef_finite_UNIV [OF type])
  apply (rule finite)
 done