# HG changeset patch
# User huffman
# Date 1128909640 -7200
# Node ID 703005988cfec8c46e707f97118fb393d8d1c327
# Parent  10ebcd7032c19ea4f7777eb19d7bfe56c658ab90
added theorem typedef_chfin

diff -r 10ebcd7032c1 -r 703005988cfe src/HOLCF/Pcpodef.thy
--- a/src/HOLCF/Pcpodef.thy	Mon Oct 10 03:55:39 2005 +0200
+++ b/src/HOLCF/Pcpodef.thy	Mon Oct 10 04:00:40 2005 +0200
@@ -30,6 +30,29 @@
 done
 
 
+subsection {* Proving a subtype is chain-finite *}
+
+lemma monofun_Rep:
+  assumes less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+  shows "monofun Rep"
+by (rule monofunI, unfold less)
+
+lemmas ch2ch_Rep = ch2ch_monofun [OF monofun_Rep]
+lemmas ub2ub_Rep = ub2ub_monofun [OF monofun_Rep]
+
+theorem typedef_chfin:
+  fixes Abs :: "'a::chfin \<Rightarrow> 'b::po"
+  assumes type: "type_definition Rep Abs A"
+    and less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+  shows "OFCLASS('b, chfin_class)"
+ apply (intro_classes, clarify)
+ apply (drule ch2ch_Rep [OF less])
+ apply (drule chfin [rule_format])
+ apply (unfold max_in_chain_def)
+ apply (simp add: type_definition.Rep_inject [OF type])
+done
+
+
 subsection {* Proving a subtype is complete *}
 
 text {*
@@ -40,14 +63,6 @@
   admissible predicate.
 *}
 
-lemma monofun_Rep:
-  assumes less: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
-  shows "monofun Rep"
-by (rule monofunI, unfold less)
-
-lemmas ch2ch_Rep = ch2ch_monofun [OF monofun_Rep]
-lemmas ub2ub_Rep = ub2ub_monofun [OF monofun_Rep]
-
 lemma Abs_inverse_lub_Rep:
   fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
   assumes type: "type_definition Rep Abs A"