--- a/src/HOLCF/Adm.thy Wed Nov 10 13:22:39 2010 -0800
+++ b/src/HOLCF/Adm.thy Wed Nov 10 14:20:47 2010 -0800
@@ -146,7 +146,7 @@
lemma compact_below_lub_iff:
"\<lbrakk>compact x; chain Y\<rbrakk> \<Longrightarrow> x \<sqsubseteq> (\<Squnion>i. Y i) \<longleftrightarrow> (\<exists>i. x \<sqsubseteq> Y i)"
-by (fast intro: compactD2 elim: below_trans is_ub_thelub)
+by (fast intro: compactD2 elim: below_lub)
lemma compact_chfin [simp]: "compact (x::'a::chfin)"
by (rule compactI [OF adm_chfin])
--- a/src/HOLCF/Completion.thy Wed Nov 10 13:22:39 2010 -0800
+++ b/src/HOLCF/Completion.thy Wed Nov 10 14:20:47 2010 -0800
@@ -351,11 +351,9 @@
apply (rule ub_imageI, rename_tac a)
apply (clarsimp simp add: rep_x)
apply (drule f_mono)
- apply (erule below_trans)
- apply (rule is_ub_thelub [OF chain])
- apply (rule is_lub_thelub [OF chain])
- apply (rule ub_rangeI)
- apply (drule_tac x="Y i" in ub_imageD)
+ apply (erule below_lub [OF chain])
+ apply (rule lub_below [OF chain])
+ apply (drule_tac x="Y n" in ub_imageD)
apply (simp add: rep_x, fast intro: r_refl)
apply assumption
done
--- a/src/HOLCF/Fix.thy Wed Nov 10 13:22:39 2010 -0800
+++ b/src/HOLCF/Fix.thy Wed Nov 10 14:20:47 2010 -0800
@@ -82,9 +82,8 @@
lemma fix_least_below: "F\<cdot>x \<sqsubseteq> x \<Longrightarrow> fix\<cdot>F \<sqsubseteq> x"
apply (simp add: fix_def2)
-apply (rule is_lub_thelub)
+apply (rule lub_below)
apply (rule chain_iterate)
-apply (rule ub_rangeI)
apply (induct_tac i)
apply simp
apply simp
--- a/src/HOLCF/Pcpo.thy Wed Nov 10 13:22:39 2010 -0800
+++ b/src/HOLCF/Pcpo.thy Wed Nov 10 14:20:47 2010 -0800
@@ -36,11 +36,16 @@
lemma lub_below_iff: "chain S \<Longrightarrow> (\<Squnion>i. S i) \<sqsubseteq> x \<longleftrightarrow> (\<forall>i. S i \<sqsubseteq> x)"
by (simp add: is_lub_below_iff [OF cpo_lubI] is_ub_def)
+lemma lub_below: "\<lbrakk>chain S; \<And>i. S i \<sqsubseteq> x\<rbrakk> \<Longrightarrow> (\<Squnion>i. S i) \<sqsubseteq> x"
+ by (simp add: lub_below_iff)
+
+lemma below_lub: "\<lbrakk>chain S; x \<sqsubseteq> S i\<rbrakk> \<Longrightarrow> x \<sqsubseteq> (\<Squnion>i. S i)"
+ by (erule below_trans, erule is_ub_thelub)
+
lemma lub_range_mono:
"\<lbrakk>range X \<subseteq> range Y; chain Y; chain X\<rbrakk>
\<Longrightarrow> (\<Squnion>i. X i) \<sqsubseteq> (\<Squnion>i. Y i)"
-apply (erule is_lub_thelub)
-apply (rule ub_rangeI)
+apply (erule lub_below)
apply (subgoal_tac "\<exists>j. X i = Y j")
apply clarsimp
apply (erule is_ub_thelub)
@@ -54,14 +59,12 @@
apply fast
apply assumption
apply (erule chain_shift)
-apply (rule is_lub_thelub)
+apply (rule lub_below)
apply assumption
-apply (rule ub_rangeI)
-apply (rule_tac y="Y (i + j)" in below_trans)
+apply (rule_tac i="i" in below_lub)
+apply (erule chain_shift)
apply (erule chain_mono)
apply (rule le_add1)
-apply (rule is_ub_thelub)
-apply (erule chain_shift)
done
lemma maxinch_is_thelub:
@@ -80,52 +83,14 @@
lemma lub_mono:
"\<lbrakk>chain X; chain Y; \<And>i. X i \<sqsubseteq> Y i\<rbrakk>
\<Longrightarrow> (\<Squnion>i. X i) \<sqsubseteq> (\<Squnion>i. Y i)"
-apply (erule is_lub_thelub)
-apply (rule ub_rangeI)
-apply (rule below_trans)
-apply (erule meta_spec)
-apply (erule is_ub_thelub)
-done
+by (fast elim: lub_below below_lub)
text {* the = relation between two chains is preserved by their lubs *}
-lemma lub_equal:
- "\<lbrakk>chain X; chain Y; \<forall>k. X k = Y k\<rbrakk>
- \<Longrightarrow> (\<Squnion>i. X i) = (\<Squnion>i. Y i)"
- by (simp only: fun_eq_iff [symmetric])
-
lemma lub_eq:
"(\<And>i. X i = Y i) \<Longrightarrow> (\<Squnion>i. X i) = (\<Squnion>i. Y i)"
by simp
-text {* more results about mono and = of lubs of chains *}
-
-lemma lub_mono2:
- "\<lbrakk>\<exists>j. \<forall>i>j. X i = Y i; chain X; chain Y\<rbrakk>
- \<Longrightarrow> (\<Squnion>i. X i) \<sqsubseteq> (\<Squnion>i. Y i)"
-apply (erule exE)
-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
-done
-
-lemma lub_equal2:
- "\<lbrakk>\<exists>j. \<forall>i>j. X i = Y i; chain X; chain Y\<rbrakk>
- \<Longrightarrow> (\<Squnion>i. X i) = (\<Squnion>i. Y i)"
- by (blast intro: below_antisym lub_mono2 sym)
-
-lemma lub_mono3:
- "\<lbrakk>chain Y; chain X; \<forall>i. \<exists>j. Y i \<sqsubseteq> X j\<rbrakk>
- \<Longrightarrow> (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. X i)"
-apply (erule is_lub_thelub)
-apply (rule ub_rangeI)
-apply (erule allE)
-apply (erule exE)
-apply (erule below_trans)
-apply (erule is_ub_thelub)
-done
-
lemma ch2ch_lub:
assumes 1: "\<And>j. chain (\<lambda>i. Y i j)"
assumes 2: "\<And>i. chain (\<lambda>j. Y i j)"
@@ -149,10 +114,9 @@
have 4: "chain (\<lambda>i. \<Squnion>j. Y i j)"
by (rule ch2ch_lub [OF 1 2])
show "(\<Squnion>i. \<Squnion>j. Y i j) \<sqsubseteq> (\<Squnion>i. Y i i)"
- apply (rule is_lub_thelub [OF 4])
- apply (rule ub_rangeI)
- apply (rule lub_mono3 [rule_format, OF 2 3])
- apply (rule exI)
+ apply (rule lub_below [OF 4])
+ apply (rule lub_below [OF 2])
+ apply (rule below_lub [OF 3])
apply (rule below_trans)
apply (rule chain_mono [OF 1 le_maxI1])
apply (rule chain_mono [OF 2 le_maxI2])
--- a/src/HOLCF/Universal.thy Wed Nov 10 13:22:39 2010 -0800
+++ b/src/HOLCF/Universal.thy Wed Nov 10 14:20:47 2010 -0800
@@ -851,7 +851,7 @@
unfolding approximants_def
apply safe
apply (simp add: compactD2 [OF compact_Rep_compact_basis Y])
- apply (erule below_trans, rule is_ub_thelub [OF Y])
+ apply (erule below_lub [OF Y])
done
next
fix a :: "'a compact_basis"
@@ -990,14 +990,12 @@
lemma lub_udom_approx [simp]: "(\<Squnion>i. udom_approx i) = ID"
apply (rule cfun_eqI, simp add: contlub_cfun_fun)
apply (rule below_antisym)
-apply (rule is_lub_thelub)
+apply (rule lub_below)
apply (simp)
-apply (rule ub_rangeI)
apply (rule udom_approx.below)
apply (rule_tac x=x in udom.principal_induct)
apply (simp add: lub_distribs)
-apply (rule rev_below_trans)
-apply (rule_tac x=a in is_ub_thelub)
+apply (rule_tac i=a in below_lub)
apply simp
apply (simp add: udom_approx_principal)
apply (simp add: ubasis_until_same ubasis_le_refl)