# HG changeset patch
# User huffman
# Date 1146439283 -7200
# Node ID 8134024166b83bd6ee1ae4e1b6b1dc743eaeea59
# Parent  5204c73a4d4625c92b6bcda18ec534b9265517c9
add theorem typdef_flat

diff -r 5204c73a4d46 -r 8134024166b8 src/HOLCF/Pcpodef.thy
--- a/src/HOLCF/Pcpodef.thy	Sun Apr 30 22:50:12 2006 +0200
+++ b/src/HOLCF/Pcpodef.thy	Mon May 01 01:21:23 2006 +0200
@@ -249,6 +249,21 @@
  apply (simp add: type_definition.Rep_inject [OF type])
 done
 
+subsection {* Proving a subtype is flat *}
+
+theorem typedef_flat:
+  fixes Abs :: "'a::flat \<Rightarrow> 'b::pcpo"
+  assumes type: "type_definition Rep Abs A"
+    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+    and UU_in_A: "\<bottom> \<in> A"
+  shows "OFCLASS('b, flat_class)"
+ apply (intro_classes)
+ apply (unfold less)
+ apply (simp add: type_definition.Rep_inject [OF type, symmetric])
+ apply (simp add: typedef_Rep_strict [OF type less UU_in_A])
+ apply (simp add: ax_flat)
+done
+
 subsection {* HOLCF type definition package *}
 
 use "pcpodef_package.ML"