# HG changeset patch
# User huffman
# Date 1287334427 25200
# Node ID a12d35795cb9090c91955164f24acd520de93eb8
# Parent  57e7f651fc70622f1954512b53922f2328130af1
simplify some proofs

diff -r 57e7f651fc70 -r a12d35795cb9 src/HOLCF/Pcpodef.thy
--- a/src/HOLCF/Pcpodef.thy	Sat Oct 16 17:10:23 2010 -0700
+++ b/src/HOLCF/Pcpodef.thy	Sun Oct 17 09:53:47 2010 -0700
@@ -57,13 +57,10 @@
 
 subsection {* Proving a subtype is chain-finite *}
 
-lemma monofun_Rep:
+lemma ch2ch_Rep:
   assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
-  shows "monofun Rep"
-by (rule monofunI, unfold below)
-
-lemmas ch2ch_Rep = ch2ch_monofun [OF monofun_Rep]
-lemmas ub2ub_Rep = ub2ub_monofun [OF monofun_Rep]
+  shows "chain S \<Longrightarrow> chain (\<lambda>i. Rep (S i))"
+unfolding chain_def below .
 
 theorem typedef_chfin:
   fixes Abs :: "'a::chfin \<Rightarrow> 'b::po"
@@ -87,6 +84,11 @@
   admissible predicate.
 *}
 
+lemma typedef_is_lubI:
+  assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
+  shows "range (\<lambda>i. Rep (S i)) <<| Rep x \<Longrightarrow> range S <<| x"
+unfolding is_lub_def is_ub_def below by simp
+
 lemma Abs_inverse_lub_Rep:
   fixes Abs :: "'a::cpo \<Rightarrow> 'b::po"
   assumes type: "type_definition Rep Abs A"
@@ -104,15 +106,15 @@
     and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
     and adm: "adm (\<lambda>x. x \<in> A)"
   shows "chain S \<Longrightarrow> range S <<| Abs (\<Squnion>i. Rep (S i))"
- apply (frule ch2ch_Rep [OF below])
- apply (rule is_lubI)
-  apply (rule ub_rangeI)
-  apply (simp only: below Abs_inverse_lub_Rep [OF type below adm])
-  apply (erule is_ub_thelub)
- apply (simp only: below Abs_inverse_lub_Rep [OF type below adm])
- apply (erule is_lub_thelub)
- apply (erule ub2ub_Rep [OF below])
-done
+proof -
+  assume S: "chain S"
+  hence "chain (\<lambda>i. Rep (S i))" by (rule ch2ch_Rep [OF below])
+  hence "range (\<lambda>i. Rep (S i)) <<| (\<Squnion>i. Rep (S i))" by (rule cpo_lubI)
+  hence "range (\<lambda>i. Rep (S i)) <<| Rep (Abs (\<Squnion>i. Rep (S i)))"
+    by (simp only: Abs_inverse_lub_Rep [OF type below adm S])
+  thus "range S <<| Abs (\<Squnion>i. Rep (S i))"
+    by (rule typedef_is_lubI [OF below])
+qed
 
 lemmas typedef_thelub = typedef_lub [THEN thelubI, standard]
 
@@ -152,18 +154,6 @@
   composing it with another continuous function.
 *}
 
-theorem typedef_is_lubI:
-  assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
-  shows "range (\<lambda>i. Rep (S i)) <<| Rep x \<Longrightarrow> range S <<| x"
- apply (rule is_lubI)
-  apply (rule ub_rangeI)
-  apply (subst below)
-  apply (erule is_ub_lub)
- apply (subst below)
- apply (erule is_lub_lub)
- apply (erule ub2ub_Rep [OF below])
-done
-
 theorem typedef_cont_Abs:
   fixes Abs :: "'a::cpo \<Rightarrow> 'b::cpo"
   fixes f :: "'c::cpo \<Rightarrow> 'a::cpo"