src/HOLCF/Pcpo.thy

--- a/src/HOLCF/Pcpo.thy	Mon Oct 10 04:00:40 2005 +0200
+++ b/src/HOLCF/Pcpo.thy	Mon Oct 10 04:03:09 2005 +0200
@@ -1,8 +1,6 @@
 (*  Title:      HOLCF/Pcpo.thy
     ID:         $Id$
     Author:     Franz Regensburger
-
-Introduction of the classes cpo and pcpo.
 *)
 
 header {* Classes cpo and pcpo *}
@@ -54,11 +52,11 @@
 apply (rule is_lub_thelub)
 apply assumption
 apply (rule ub_rangeI)
-apply (rule trans_less)
-apply (rule_tac [2] is_ub_thelub)
-apply (erule_tac [2] chain_shift)
+apply (rule_tac y="Y (i + j)" in trans_less)
 apply (erule chain_mono3)
 apply (rule le_add1)
+apply (rule is_ub_thelub)
+apply (erule chain_shift)
 done
 
 lemma maxinch_is_thelub:
@@ -94,22 +92,13 @@
 text {* more results about mono and = of lubs of chains *}
 
 lemma lub_mono2:
-  "\<lbrakk>\<exists>j::nat. \<forall>i>j. X i = Y i; chain (X::nat=>'a::cpo); chain Y\<rbrakk>
+  "\<lbrakk>\<exists>j. \<forall>i>j. X i = Y i; chain (X::nat \<Rightarrow> 'a::cpo); chain Y\<rbrakk>
     \<Longrightarrow> (\<Squnion>i. X i) \<sqsubseteq> (\<Squnion>i. Y i)"
 apply (erule exE)
-apply (rule is_lub_thelub)
-apply assumption
-apply (rule ub_rangeI)
-apply (case_tac "j < i")
-apply (rule_tac s="Y i" and t="X i" in subst)
+apply (subgoal_tac "(\<Squnion>i. X (i + Suc j)) \<sqsubseteq> (\<Squnion>i. Y (i + Suc j))")
+apply (thin_tac "\<forall>i>j. X i = Y i")
+apply (simp only: lub_range_shift)
 apply simp
-apply (erule is_ub_thelub)
-apply (rule_tac y = "X (Suc j)" in trans_less)
-apply (erule chain_mono)
-apply (erule not_less_eq [THEN iffD1])
-apply (rule_tac s="Y (Suc j)" and t="X (Suc j)" in subst)
-apply simp
-apply (erule is_ub_thelub)
 done
 
 lemma lub_equal2:
@@ -120,8 +109,7 @@
 lemma lub_mono3:
   "\<lbrakk>chain (Y::nat \<Rightarrow> 'a::cpo); chain X; \<forall>i. \<exists>j. Y i \<sqsubseteq> X j\<rbrakk>
     \<Longrightarrow> (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. X i)"
-apply (rule is_lub_thelub)
-apply assumption
+apply (erule is_lub_thelub)
 apply (rule ub_rangeI)
 apply (erule allE)
 apply (erule exE)
@@ -185,7 +173,7 @@
 
 constdefs
   UU :: "'a::pcpo"
-  "UU \<equiv> THE x. ALL y. x \<sqsubseteq> y"
+  "UU \<equiv> THE x. \<forall>y. x \<sqsubseteq> y"
 
 syntax (xsymbols)
   UU :: "'a::pcpo" ("\<bottom>")
@@ -225,13 +213,7 @@
 text {* useful lemmas about @{term \<bottom>} *}
 
 lemma eq_UU_iff: "(x = \<bottom>) = (x \<sqsubseteq> \<bottom>)"
-apply (rule iffI)
-apply (erule ssubst)
-apply (rule refl_less)
-apply (rule antisym_less)
-apply assumption
-apply (rule minimal)
-done
+by (simp add: po_eq_conv)
 
 lemma UU_I: "x \<sqsubseteq> \<bottom> \<Longrightarrow> x = \<bottom>"
 by (subst eq_UU_iff)
@@ -296,9 +278,7 @@
 apply (erule exE)
 apply (rule_tac x="i" in exI)
 apply clarify
-apply (erule le_imp_less_or_eq [THEN disjE])
-apply safe
-apply (blast dest: chain_mono ax_flat [rule_format])
+apply (blast dest: chain_mono3 ax_flat [rule_format])
 done
 
 instance flat < chfin